BVFUNC_6: Propositional Calculus for Boolean Valued Functions, II

:: Propositional Calculus for Boolean Valued Functions, II
:: by Shunichi Kobayashi and Yatsuka Nakamura
::
:: Received March 13, 1999
:: Copyright (c) 1999-2021 Association of Mizar Users

theorem :: BVFUNC_6:1

for Y being non empty set
for a, b being Function of Y,BOOLEAN holds a 'imp' (b 'imp' (a '&' b)) = I_el Y

proof end;

theorem :: BVFUNC_6:2

for Y being non empty set
for a, b being Function of Y,BOOLEAN holds (a 'imp' b) 'imp' ((b 'imp' a) 'imp' (a 'eqv' b)) = I_el Y

proof end;

theorem :: BVFUNC_6:3

for Y being non empty set
for a, b being Function of Y,BOOLEAN holds (a 'or' b) 'eqv' (b 'or' a) = I_el Y

proof end;

theorem :: BVFUNC_6:4

for Y being non empty set
for a, b, c being Function of Y,BOOLEAN holds ((a '&' b) 'imp' c) 'imp' (a 'imp' (b 'imp' c)) = I_el Y

proof end;

theorem :: BVFUNC_6:5

for Y being non empty set
for a, b, c being Function of Y,BOOLEAN holds (a 'imp' (b 'imp' c)) 'imp' ((a '&' b) 'imp' c) = I_el Y

proof end;

theorem :: BVFUNC_6:6

for Y being non empty set
for a, b, c being Function of Y,BOOLEAN holds (c 'imp' a) 'imp' ((c 'imp' b) 'imp' (c 'imp' (a '&' b))) = I_el Y

proof end;

theorem :: BVFUNC_6:7

for Y being non empty set
for a, b, c being Function of Y,BOOLEAN holds ((a 'or' b) 'imp' c) 'imp' ((a 'imp' c) 'or' (b 'imp' c)) = I_el Y

proof end;

theorem :: BVFUNC_6:8

for Y being non empty set
for a, b, c being Function of Y,BOOLEAN holds (a 'imp' c) 'imp' ((b 'imp' c) 'imp' ((a 'or' b) 'imp' c)) = I_el Y

proof end;

theorem Th9: :: BVFUNC_6:9

for Y being non empty set
for a, b, c being Function of Y,BOOLEAN holds ((a 'imp' c) '&' (b 'imp' c)) 'imp' ((a 'or' b) 'imp' c) = I_el Y

proof end;

theorem :: BVFUNC_6:10

for Y being non empty set
for a, b being Function of Y,BOOLEAN holds (a 'imp' (b '&' ('not' b))) 'imp' ('not' a) = I_el Y

proof end;

theorem :: BVFUNC_6:11

for Y being non empty set
for a, b, c being Function of Y,BOOLEAN holds ((a 'or' b) '&' (a 'or' c)) 'imp' (a 'or' (b '&' c)) = I_el Y

proof end;

theorem :: BVFUNC_6:12

for Y being non empty set
for a, b, c being Function of Y,BOOLEAN holds (a '&' (b 'or' c)) 'imp' ((a '&' b) 'or' (a '&' c)) = I_el Y

proof end;

theorem :: BVFUNC_6:13

for Y being non empty set
for a, b, c being Function of Y,BOOLEAN holds ((a 'or' c) '&' (b 'or' c)) 'imp' ((a '&' b) 'or' c) = I_el Y

proof end;

theorem :: BVFUNC_6:14

for Y being non empty set
for a, b, c being Function of Y,BOOLEAN holds ((a 'or' b) '&' c) 'imp' ((a '&' c) 'or' (b '&' c)) = I_el Y

proof end;

theorem :: BVFUNC_6:15

for Y being non empty set
for a, b being Function of Y,BOOLEAN st a '&' b = I_el Y holds
a 'or' b = I_el Y

proof end;

theorem :: BVFUNC_6:16

for Y being non empty set
for a, b, c being Function of Y,BOOLEAN st a 'imp' b = I_el Y holds
(a 'or' c) 'imp' (b 'or' c) = I_el Y

proof end;

theorem :: BVFUNC_6:17

for Y being non empty set
for a, b, c being Function of Y,BOOLEAN st a 'imp' b = I_el Y holds
(a '&' c) 'imp' (b '&' c) = I_el Y

proof end;

theorem th18: :: BVFUNC_6:18

for Y being non empty set
for a, b, c being Function of Y,BOOLEAN st c 'imp' a = I_el Y & c 'imp' b = I_el Y holds
c 'imp' (a '&' b) = I_el Y

proof end;

theorem :: BVFUNC_6:19

for Y being non empty set
for a, b, c being Function of Y,BOOLEAN st a 'imp' c = I_el Y & b 'imp' c = I_el Y holds
(a 'or' b) 'imp' c = I_el Y

proof end;

theorem :: BVFUNC_6:20

for Y being non empty set
for a, b being Function of Y,BOOLEAN st a 'or' b = I_el Y & 'not' a = I_el Y holds
b = I_el Y

proof end;

theorem tt: :: BVFUNC_6:21

for Y being non empty set
for a, b, c, d being Function of Y,BOOLEAN st a 'imp' b = I_el Y & c 'imp' d = I_el Y holds
(a '&' c) 'imp' (b '&' d) = I_el Y

proof end;

theorem Th22: :: BVFUNC_6:22

for Y being non empty set
for a, b, c, d being Function of Y,BOOLEAN st a 'imp' b = I_el Y & c 'imp' d = I_el Y holds
(a 'or' c) 'imp' (b 'or' d) = I_el Y

proof end;

theorem :: BVFUNC_6:23

for Y being non empty set
for a, b being Function of Y,BOOLEAN st (a '&' ('not' b)) 'imp' ('not' a) = I_el Y holds
a 'imp' b = I_el Y

proof end;

theorem :: BVFUNC_6:24

for Y being non empty set
for a, b being Function of Y,BOOLEAN st a 'imp' ('not' b) = I_el Y holds
b 'imp' ('not' a) = I_el Y

proof end;

theorem :: BVFUNC_6:25

for Y being non empty set
for a, b being Function of Y,BOOLEAN st ('not' a) 'imp' b = I_el Y holds
('not' b) 'imp' a = I_el Y

proof end;

theorem Th26: :: BVFUNC_6:26

for Y being non empty set
for a, b being Function of Y,BOOLEAN holds a 'imp' (a 'or' b) = I_el Y

proof end;

theorem :: BVFUNC_6:27

for Y being non empty set
for a, b being Function of Y,BOOLEAN holds (a 'or' b) 'imp' (('not' a) 'imp' b) = I_el Y

proof end;

theorem Th28: :: BVFUNC_6:28

for Y being non empty set
for a, b being Function of Y,BOOLEAN holds ('not' (a 'or' b)) 'imp' (('not' a) '&' ('not' b)) = I_el Y

proof end;

theorem :: BVFUNC_6:29

for Y being non empty set
for a, b being Function of Y,BOOLEAN holds (('not' a) '&' ('not' b)) 'imp' ('not' (a 'or' b)) = I_el Y

proof end;

theorem :: BVFUNC_6:30

for Y being non empty set
for a, b being Function of Y,BOOLEAN holds ('not' (a 'or' b)) 'imp' ('not' a) = I_el Y

proof end;

theorem :: BVFUNC_6:31

for Y being non empty set
for a being Function of Y,BOOLEAN holds (a 'or' a) 'imp' a = I_el Y

proof end;

theorem :: BVFUNC_6:32

for Y being non empty set
for a, b being Function of Y,BOOLEAN holds (a '&' ('not' a)) 'imp' b = I_el Y

proof end;

theorem :: BVFUNC_6:33

for Y being non empty set
for a, b being Function of Y,BOOLEAN holds (a 'imp' b) 'imp' (('not' a) 'or' b) = I_el Y

proof end;

theorem :: BVFUNC_6:34

for Y being non empty set
for a, b being Function of Y,BOOLEAN holds (a '&' b) 'imp' ('not' (a 'imp' ('not' b))) = I_el Y

proof end;

theorem :: BVFUNC_6:35

for Y being non empty set
for a, b being Function of Y,BOOLEAN holds ('not' (a 'imp' ('not' b))) 'imp' (a '&' b) = I_el Y

proof end;

theorem Th36: :: BVFUNC_6:36

for Y being non empty set
for a, b being Function of Y,BOOLEAN holds ('not' (a '&' b)) 'imp' (('not' a) 'or' ('not' b)) = I_el Y

proof end;

theorem :: BVFUNC_6:37

for Y being non empty set
for a, b being Function of Y,BOOLEAN holds (('not' a) 'or' ('not' b)) 'imp' ('not' (a '&' b)) = I_el Y

proof end;

theorem Th38: :: BVFUNC_6:38

for Y being non empty set
for a, b being Function of Y,BOOLEAN holds (a '&' b) 'imp' a = I_el Y

proof end;

theorem :: BVFUNC_6:39

for Y being non empty set
for a, b being Function of Y,BOOLEAN holds (a '&' b) 'imp' (a 'or' b) = I_el Y

proof end;

theorem :: BVFUNC_6:40

for Y being non empty set
for a, b being Function of Y,BOOLEAN holds (a '&' b) 'imp' b = I_el Y

proof end;

theorem :: BVFUNC_6:41

for Y being non empty set
for a being Function of Y,BOOLEAN holds a 'imp' (a '&' a) = I_el Y

proof end;

theorem Th42: :: BVFUNC_6:42

for Y being non empty set
for a, b being Function of Y,BOOLEAN holds (a 'eqv' b) 'imp' (a 'imp' b) = I_el Y

proof end;

theorem :: BVFUNC_6:43

for Y being non empty set
for a, b being Function of Y,BOOLEAN holds (a 'eqv' b) 'imp' (b 'imp' a) = I_el Y by Th42;

theorem :: BVFUNC_6:44

for Y being non empty set
for a, b, c being Function of Y,BOOLEAN holds ((a 'or' b) 'or' c) 'imp' (a 'or' (b 'or' c)) = I_el Y

proof end;

theorem :: BVFUNC_6:45

for Y being non empty set
for a, b, c being Function of Y,BOOLEAN holds ((a '&' b) '&' c) 'imp' (a '&' (b '&' c)) = I_el Y

proof end;

theorem :: BVFUNC_6:46

for Y being non empty set
for a, b, c being Function of Y,BOOLEAN holds (a 'or' (b 'or' c)) 'imp' ((a 'or' b) 'or' c) = I_el Y

proof end;

theorem :: BVFUNC_6:47

for Y being non empty set
for a, b being Function of Y,BOOLEAN holds (a 'imp' b) '&' (('not' a) 'imp' b) = b

proof end;

theorem :: BVFUNC_6:48

for Y being non empty set
for a, b being Function of Y,BOOLEAN holds (a 'imp' b) '&' (a 'imp' ('not' b)) = 'not' a

proof end;

theorem Th73: :: BVFUNC_6:49

for Y being non empty set
for a, b, c being Function of Y,BOOLEAN holds a 'imp' (b 'or' c) = (a 'imp' b) 'or' (a 'imp' c)

proof end;

theorem :: BVFUNC_6:50

for Y being non empty set
for a, b, c being Function of Y,BOOLEAN holds a 'imp' (b '&' c) = (a 'imp' b) '&' (a 'imp' c)

proof end;

theorem Th75: :: BVFUNC_6:51

for Y being non empty set
for a, b, c being Function of Y,BOOLEAN holds (a 'or' b) 'imp' c = (a 'imp' c) '&' (b 'imp' c)

proof end;

theorem Th76: :: BVFUNC_6:52

for Y being non empty set
for a, b, c being Function of Y,BOOLEAN holds (a '&' b) 'imp' c = (a 'imp' c) 'or' (b 'imp' c)

proof end;

theorem Th7: :: BVFUNC_6:53

for Y being non empty set
for a, b, c being Function of Y,BOOLEAN holds (a '&' b) 'imp' c = a 'imp' (b 'imp' c)

proof end;

theorem :: BVFUNC_6:54

for Y being non empty set
for a, b, c being Function of Y,BOOLEAN holds (a '&' b) 'imp' c = a 'imp' (('not' b) 'or' c)

proof end;

theorem :: BVFUNC_6:55

for Y being non empty set
for a, b, c being Function of Y,BOOLEAN holds a 'imp' (b 'or' c) = (a '&' ('not' b)) 'imp' c

proof end;

theorem :: BVFUNC_6:56

for Y being non empty set
for a, b being Function of Y,BOOLEAN holds a '&' (a 'imp' b) = a '&' b

proof end;

theorem :: BVFUNC_6:57

for Y being non empty set
for a, b being Function of Y,BOOLEAN holds (a 'imp' b) '&' ('not' b) = ('not' a) '&' ('not' b)

proof end;

theorem Th12: :: BVFUNC_6:58

for Y being non empty set
for a, b, c being Function of Y,BOOLEAN holds (a 'imp' b) '&' (b 'imp' c) = ((a 'imp' b) '&' (b 'imp' c)) '&' (a 'imp' c)

proof end;

theorem :: BVFUNC_6:59

for Y being non empty set
for a being Function of Y,BOOLEAN holds (I_el Y) 'imp' a = a

proof end;

theorem :: BVFUNC_6:60

for Y being non empty set
for a being Function of Y,BOOLEAN holds a 'imp' (O_el Y) = 'not' a

proof end;

theorem :: BVFUNC_6:61

for Y being non empty set
for a being Function of Y,BOOLEAN holds (O_el Y) 'imp' a = I_el Y

proof end;

theorem :: BVFUNC_6:62

for Y being non empty set
for a being Function of Y,BOOLEAN holds a 'imp' (I_el Y) = I_el Y

proof end;

theorem :: BVFUNC_6:63

for Y being non empty set
for a being Function of Y,BOOLEAN holds a 'imp' ('not' a) = 'not' a

proof end;

theorem :: BVFUNC_6:64

for Y being non empty set
for a, b, c being Function of Y,BOOLEAN holds a 'imp' b '<' (c 'imp' a) 'imp' (c 'imp' b)

proof end;

theorem :: BVFUNC_6:65

for Y being non empty set
for a, b, c being Function of Y,BOOLEAN holds a 'eqv' b '<' (a 'eqv' c) 'eqv' (b 'eqv' c)

proof end;

theorem :: BVFUNC_6:66

for Y being non empty set
for a, b, c being Function of Y,BOOLEAN holds a 'eqv' b '<' (a 'imp' c) 'eqv' (b 'imp' c)

proof end;

theorem :: BVFUNC_6:67

for Y being non empty set
for a, b, c being Function of Y,BOOLEAN holds a 'eqv' b '<' (c 'imp' a) 'eqv' (c 'imp' b)

proof end;

theorem :: BVFUNC_6:68

for Y being non empty set
for a, b, c being Function of Y,BOOLEAN holds a 'eqv' b '<' (a '&' c) 'eqv' (b '&' c)

proof end;

theorem :: BVFUNC_6:69

for Y being non empty set
for a, b, c being Function of Y,BOOLEAN holds a 'eqv' b '<' (a 'or' c) 'eqv' (b 'or' c)

proof end;

theorem :: BVFUNC_6:70

for Y being non empty set
for a, b being Function of Y,BOOLEAN holds a '<' ((a 'eqv' b) 'eqv' (b 'eqv' a)) 'eqv' a

proof end;

theorem :: BVFUNC_6:71

for Y being non empty set
for a, b being Function of Y,BOOLEAN holds a '<' (a 'imp' b) 'eqv' b

proof end;

theorem :: BVFUNC_6:72

for Y being non empty set
for a, b being Function of Y,BOOLEAN holds a '<' (b 'imp' a) 'eqv' a

proof end;

theorem :: BVFUNC_6:73

for Y being non empty set
for a, b being Function of Y,BOOLEAN holds a '<' ((a '&' b) 'eqv' (b '&' a)) 'eqv' a

proof end;

theorem :: BVFUNC_6:74

for Y being non empty set
for a, b, c, d being Function of Y,BOOLEAN holds a 'imp' ((b '&' c) '&' d) = ((a 'imp' b) '&' (a 'imp' c)) '&' (a 'imp' d)

proof end;

theorem :: BVFUNC_6:75

for Y being non empty set
for a, b, c, d being Function of Y,BOOLEAN holds a 'imp' ((b 'or' c) 'or' d) = ((a 'imp' b) 'or' (a 'imp' c)) 'or' (a 'imp' d)

proof end;

theorem :: BVFUNC_6:76

for Y being non empty set
for a, b, c, d being Function of Y,BOOLEAN holds ((a '&' b) '&' c) 'imp' d = ((a 'imp' d) 'or' (b 'imp' d)) 'or' (c 'imp' d)

proof end;

theorem :: BVFUNC_6:77

for Y being non empty set
for a, b, c, d being Function of Y,BOOLEAN holds ((a 'or' b) 'or' c) 'imp' d = ((a 'imp' d) '&' (b 'imp' d)) '&' (c 'imp' d)

proof end;

theorem :: BVFUNC_6:78

for Y being non empty set
for a, b, c being Function of Y,BOOLEAN holds ((a 'imp' b) '&' (b 'imp' c)) '&' (c 'imp' a) = ((((a 'imp' b) '&' (b 'imp' c)) '&' (c 'imp' a)) '&' (b 'imp' a)) '&' (a 'imp' c)

proof end;

theorem :: BVFUNC_6:79

for Y being non empty set
for a, b being Function of Y,BOOLEAN holds a = (a '&' b) 'or' (a '&' ('not' b))

proof end;

theorem :: BVFUNC_6:80

for Y being non empty set
for a, b being Function of Y,BOOLEAN holds a = (a 'or' b) '&' (a 'or' ('not' b))

proof end;

theorem :: BVFUNC_6:81

for Y being non empty set
for a, b, c being Function of Y,BOOLEAN holds a = ((((a '&' b) '&' c) 'or' ((a '&' b) '&' ('not' c))) 'or' ((a '&' ('not' b)) '&' c)) 'or' ((a '&' ('not' b)) '&' ('not' c))

proof end;

theorem :: BVFUNC_6:82

for Y being non empty set
for a, b, c being Function of Y,BOOLEAN holds a = ((((a 'or' b) 'or' c) '&' ((a 'or' b) 'or' ('not' c))) '&' ((a 'or' ('not' b)) 'or' c)) '&' ((a 'or' ('not' b)) 'or' ('not' c))

proof end;

theorem :: BVFUNC_6:83

for Y being non empty set
for a, b being Function of Y,BOOLEAN holds a '&' b = a '&' (('not' a) 'or' b)

proof end;

theorem :: BVFUNC_6:84

for Y being non empty set
for a, b being Function of Y,BOOLEAN holds a 'or' b = a 'or' (('not' a) '&' b)

proof end;

theorem :: BVFUNC_6:85

for Y being non empty set
for a, b being Function of Y,BOOLEAN holds a 'xor' b = 'not' (a 'eqv' b)

proof end;

theorem :: BVFUNC_6:86

for Y being non empty set
for a, b being Function of Y,BOOLEAN holds a 'xor' b = (a 'or' b) '&' (('not' a) 'or' ('not' b))

proof end;

theorem :: BVFUNC_6:87

for Y being non empty set
for a being Function of Y,BOOLEAN holds a 'xor' (I_el Y) = 'not' a

proof end;

theorem :: BVFUNC_6:88

for Y being non empty set
for a being Function of Y,BOOLEAN holds a 'xor' (O_el Y) = a

proof end;

theorem :: BVFUNC_6:89

for Y being non empty set
for a, b being Function of Y,BOOLEAN holds a 'xor' b = ('not' a) 'xor' ('not' b)

proof end;

theorem :: BVFUNC_6:90

for Y being non empty set
for a, b being Function of Y,BOOLEAN holds 'not' (a 'xor' b) = a 'xor' ('not' b)

proof end;

theorem Th18: :: BVFUNC_6:91

for Y being non empty set
for a, b being Function of Y,BOOLEAN holds a 'eqv' b = (a 'or' ('not' b)) '&' (('not' a) 'or' b)

proof end;

theorem :: BVFUNC_6:92

for Y being non empty set
for a, b being Function of Y,BOOLEAN holds a 'eqv' b = (a '&' b) 'or' (('not' a) '&' ('not' b))

proof end;

theorem :: BVFUNC_6:93

for Y being non empty set
for a being Function of Y,BOOLEAN holds a 'eqv' (I_el Y) = a

proof end;

theorem :: BVFUNC_6:94

for Y being non empty set
for a being Function of Y,BOOLEAN holds a 'eqv' (O_el Y) = 'not' a

proof end;

theorem :: BVFUNC_6:95

for Y being non empty set
for a, b being Function of Y,BOOLEAN holds 'not' (a 'eqv' b) = a 'eqv' ('not' b)

proof end;

theorem :: BVFUNC_6:96

for Y being non empty set
for a, b being Function of Y,BOOLEAN holds 'not' a '<' (a 'imp' b) 'eqv' ('not' a)

proof end;

theorem :: BVFUNC_6:97

for Y being non empty set
for a, b being Function of Y,BOOLEAN holds 'not' a '<' (b 'imp' a) 'eqv' ('not' b)

proof end;

theorem :: BVFUNC_6:98

for Y being non empty set
for a, b being Function of Y,BOOLEAN holds a '<' ((a 'or' b) 'eqv' (b 'or' a)) 'eqv' a

proof end;

theorem :: BVFUNC_6:99

for Y being non empty set
for a being Function of Y,BOOLEAN holds a 'imp' (('not' a) 'eqv' ('not' a)) = I_el Y

proof end;

theorem :: BVFUNC_6:100

for Y being non empty set
for a, b being Function of Y,BOOLEAN holds ((a 'imp' b) 'imp' a) 'imp' a = I_el Y

proof end;

theorem :: BVFUNC_6:101

for Y being non empty set
for a, b, c, d being Function of Y,BOOLEAN holds (((a 'imp' c) '&' (b 'imp' d)) '&' (('not' c) 'or' ('not' d))) 'imp' (('not' a) 'or' ('not' b)) = I_el Y

proof end;

theorem :: BVFUNC_6:102

for Y being non empty set
for a, b, c being Function of Y,BOOLEAN holds (a 'imp' b) 'imp' ((a 'imp' (b 'imp' c)) 'imp' (a 'imp' c)) = I_el Y

proof end;

Lm1: for Y being non empty set
for a, b being Function of Y,BOOLEAN holds a '&' b '<' a

proof end;

Lm2: for Y being non empty set
for a, b, c being Function of Y,BOOLEAN holds
( (a '&' b) '&' c '<' a & (a '&' b) '&' c '<' b )

proof end;

Lm3: for Y being non empty set
for a, b, c, d being Function of Y,BOOLEAN holds
( ((a '&' b) '&' c) '&' d '<' a & ((a '&' b) '&' c) '&' d '<' b )

proof end;

Lm4: for Y being non empty set
for a, b, c, d, e being Function of Y,BOOLEAN holds
( (((a '&' b) '&' c) '&' d) '&' e '<' a & (((a '&' b) '&' c) '&' d) '&' e '<' b )

proof end;

Lm5: for Y being non empty set
for a, b, c, d, e, f being Function of Y,BOOLEAN holds
( ((((a '&' b) '&' c) '&' d) '&' e) '&' f '<' a & ((((a '&' b) '&' c) '&' d) '&' e) '&' f '<' b )

proof end;

Lm6: for Y being non empty set
for a, b, c, d, e, f, g being Function of Y,BOOLEAN holds
( (((((a '&' b) '&' c) '&' d) '&' e) '&' f) '&' g '<' a & (((((a '&' b) '&' c) '&' d) '&' e) '&' f) '&' g '<' b )

proof end;

theorem Th1: :: BVFUNC_6:103

for Y being non empty set
for a, b, c being Function of Y,BOOLEAN holds (a 'or' b) '&' (b 'imp' c) '<' a 'or' c

proof end;

theorem Th2: :: BVFUNC_6:104

for Y being non empty set
for a, b being Function of Y,BOOLEAN holds a '&' (a 'imp' b) '<' b

proof end;

theorem :: BVFUNC_6:105

for Y being non empty set
for a, b being Function of Y,BOOLEAN holds (a 'imp' b) '&' ('not' b) '<' 'not' a

proof end;

theorem :: BVFUNC_6:106

for Y being non empty set
for a, b being Function of Y,BOOLEAN holds (a 'or' b) '&' ('not' a) '<' b

proof end;

theorem :: BVFUNC_6:107

for Y being non empty set
for a, b being Function of Y,BOOLEAN holds (a 'imp' b) '&' (('not' a) 'imp' b) '<' b

proof end;

theorem :: BVFUNC_6:108

for Y being non empty set
for a, b being Function of Y,BOOLEAN holds (a 'imp' b) '&' (a 'imp' ('not' b)) '<' 'not' a

proof end;

theorem :: BVFUNC_6:109

for Y being non empty set
for a, b, c being Function of Y,BOOLEAN holds a 'imp' (b '&' c) '<' a 'imp' b

proof end;

theorem :: BVFUNC_6:110

for Y being non empty set
for a, b, c being Function of Y,BOOLEAN holds (a 'or' b) 'imp' c '<' a 'imp' c

proof end;

theorem :: BVFUNC_6:111

for Y being non empty set
for a, b, c being Function of Y,BOOLEAN holds a 'imp' b '<' (a '&' c) 'imp' b

proof end;

theorem :: BVFUNC_6:112

for Y being non empty set
for a, b, c being Function of Y,BOOLEAN holds a 'imp' b '<' (a '&' c) 'imp' (b '&' c)

proof end;

theorem :: BVFUNC_6:113

for Y being non empty set
for a, b, c being Function of Y,BOOLEAN holds a 'imp' b '<' a 'imp' (b 'or' c)

proof end;

theorem :: BVFUNC_6:114

for Y being non empty set
for a, b, c being Function of Y,BOOLEAN holds a 'imp' b '<' (a 'or' c) 'imp' (b 'or' c)

proof end;

theorem :: BVFUNC_6:115

for Y being non empty set
for a, b, c being Function of Y,BOOLEAN holds (a '&' b) 'or' c '<' a 'or' c

proof end;

theorem :: BVFUNC_6:116

for Y being non empty set
for a, b, c, d being Function of Y,BOOLEAN holds (a '&' b) 'or' (c '&' d) '<' a 'or' c

proof end;

theorem :: BVFUNC_6:117

for Y being non empty set
for a, b, c being Function of Y,BOOLEAN holds (a 'imp' b) '&' (('not' a) 'imp' c) '<' b 'or' c

proof end;

theorem :: BVFUNC_6:118

for Y being non empty set
for a, b, c being Function of Y,BOOLEAN holds (a 'imp' c) '&' (b 'imp' ('not' c)) '<' ('not' a) 'or' ('not' b)

proof end;

theorem :: BVFUNC_6:119

for Y being non empty set
for a, b, c being Function of Y,BOOLEAN holds (a 'or' b) '&' (('not' a) 'or' c) '<' b 'or' c

proof end;

theorem Th918: :: BVFUNC_6:120

for Y being non empty set
for a, b, c, d being Function of Y,BOOLEAN holds (a 'imp' b) '&' (c 'imp' d) '<' (a '&' c) 'imp' (b '&' d)

proof end;

theorem :: BVFUNC_6:121

for Y being non empty set
for a, b, c being Function of Y,BOOLEAN holds (a 'imp' b) '&' (a 'imp' c) '<' a 'imp' (b '&' c)

proof end;

theorem Th20: :: BVFUNC_6:122

for Y being non empty set
for a, b, c being Function of Y,BOOLEAN holds (a 'imp' c) '&' (b 'imp' c) '<' (a 'or' b) 'imp' c

proof end;

theorem Th21: :: BVFUNC_6:123

for Y being non empty set
for a, b, c, d being Function of Y,BOOLEAN holds (a 'imp' b) '&' (c 'imp' d) '<' (a 'or' c) 'imp' (b 'or' d)

proof end;

theorem :: BVFUNC_6:124

for Y being non empty set
for a, b, c being Function of Y,BOOLEAN holds (a 'imp' b) '&' (a 'imp' c) '<' a 'imp' (b 'or' c)

proof end;

theorem Th23: :: BVFUNC_6:125

for Y being non empty set
for a1, b1, c1, a2, b2, c2 being Function of Y,BOOLEAN holds ((((b1 'imp' b2) '&' (c1 'imp' c2)) '&' ((a1 'or' b1) 'or' c1)) '&' ('not' (a2 '&' b2))) '&' ('not' (a2 '&' c2)) '<' a2 'imp' a1

proof end;

Lm7: for Y being non empty set
for a1, b1, c1, a2, b2, c2 being Function of Y,BOOLEAN holds (((((((a1 'imp' a2) '&' (b1 'imp' b2)) '&' (c1 'imp' c2)) '&' ((a1 'or' b1) 'or' c1)) '&' ('not' (a2 '&' b2))) '&' ('not' (a2 '&' c2))) '&' ('not' (b2 '&' c2))) 'imp' (((((a1 'imp' a2) '&' (b1 'imp' b2)) '&' ((a1 'or' b1) 'or' c1)) '&' ('not' (c2 '&' a2))) '&' ('not' (c2 '&' b2))) = I_el Y

proof end;

Lm8: for Y being non empty set
for a1, b1, c1, a2, b2, c2 being Function of Y,BOOLEAN holds (((((((a1 'imp' a2) '&' (b1 'imp' b2)) '&' (c1 'imp' c2)) '&' ((a1 'or' b1) 'or' c1)) '&' ('not' (a2 '&' b2))) '&' ('not' (a2 '&' c2))) '&' ('not' (b2 '&' c2))) 'imp' (((((a1 'imp' a2) '&' (c1 'imp' c2)) '&' ((a1 'or' b1) 'or' c1)) '&' ('not' (b2 '&' a2))) '&' ('not' (b2 '&' c2))) = I_el Y

proof end;

Lm9: for Y being non empty set
for a1, b1, c1, a2, b2, c2 being Function of Y,BOOLEAN holds (((((((a1 'imp' a2) '&' (b1 'imp' b2)) '&' (c1 'imp' c2)) '&' ((a1 'or' b1) 'or' c1)) '&' ('not' (a2 '&' b2))) '&' ('not' (a2 '&' c2))) '&' ('not' (b2 '&' c2))) 'imp' (((((b1 'imp' b2) '&' (c1 'imp' c2)) '&' ((a1 'or' b1) 'or' c1)) '&' ('not' (a2 '&' b2))) '&' ('not' (a2 '&' c2))) = I_el Y

proof end;

theorem :: BVFUNC_6:126

for Y being non empty set
for a1, b1, c1, a2, b2, c2 being Function of Y,BOOLEAN holds ((((((a1 'imp' a2) '&' (b1 'imp' b2)) '&' (c1 'imp' c2)) '&' ((a1 'or' b1) 'or' c1)) '&' ('not' (a2 '&' b2))) '&' ('not' (a2 '&' c2))) '&' ('not' (b2 '&' c2)) '<' ((a2 'imp' a1) '&' (b2 'imp' b1)) '&' (c2 'imp' c1)

proof end;

theorem Th25: :: BVFUNC_6:127

for Y being non empty set
for a1, b1, a2, b2 being Function of Y,BOOLEAN holds (((a1 'imp' a2) '&' (b1 'imp' b2)) '&' ('not' (a2 '&' b2))) 'imp' ('not' (a1 '&' b1)) = I_el Y

proof end;

theorem :: BVFUNC_6:128

for Y being non empty set
for a1, b1, c1, a2, b2, c2 being Function of Y,BOOLEAN holds (((((a1 'imp' a2) '&' (b1 'imp' b2)) '&' (c1 'imp' c2)) '&' ('not' (a2 '&' b2))) '&' ('not' (a2 '&' c2))) '&' ('not' (b2 '&' c2)) '<' (('not' (a1 '&' b1)) '&' ('not' (a1 '&' c1))) '&' ('not' (b1 '&' c1))

proof end;

theorem :: BVFUNC_6:129

for Y being non empty set
for a, b being Function of Y,BOOLEAN holds a '&' b '<' a by Lm1;

theorem :: BVFUNC_6:130

for Y being non empty set
for a, b, c being Function of Y,BOOLEAN holds
( (a '&' b) '&' c '<' a & (a '&' b) '&' c '<' b ) by Lm2;

theorem :: BVFUNC_6:131

for Y being non empty set
for a, b, c, d being Function of Y,BOOLEAN holds
( ((a '&' b) '&' c) '&' d '<' a & ((a '&' b) '&' c) '&' d '<' b ) by Lm3;

theorem :: BVFUNC_6:132

for Y being non empty set
for a, b, c, d, e being Function of Y,BOOLEAN holds
( (((a '&' b) '&' c) '&' d) '&' e '<' a & (((a '&' b) '&' c) '&' d) '&' e '<' b ) by Lm4;

theorem :: BVFUNC_6:133

for Y being non empty set
for a, b, c, d, e, f being Function of Y,BOOLEAN holds
( ((((a '&' b) '&' c) '&' d) '&' e) '&' f '<' a & ((((a '&' b) '&' c) '&' d) '&' e) '&' f '<' b ) by Lm5;

theorem :: BVFUNC_6:134

for Y being non empty set
for a, b, c, d, e, f, g being Function of Y,BOOLEAN holds
( (((((a '&' b) '&' c) '&' d) '&' e) '&' f) '&' g '<' a & (((((a '&' b) '&' c) '&' d) '&' e) '&' f) '&' g '<' b ) by Lm6;

theorem Th33: :: BVFUNC_6:135

for Y being non empty set
for a, b, c, d being Function of Y,BOOLEAN st a '<' b & c '<' d holds
a '&' c '<' b '&' d

proof end;

theorem :: BVFUNC_6:136

for Y being non empty set
for a, b, c being Function of Y,BOOLEAN st a '&' b '<' c holds
a '&' ('not' c) '<' 'not' b

proof end;

theorem :: BVFUNC_6:137

for Y being non empty set
for a, b, c being Function of Y,BOOLEAN holds ((a 'imp' c) '&' (b 'imp' c)) '&' (a 'or' b) '<' c

proof end;

theorem :: BVFUNC_6:138

for Y being non empty set
for a, b, c being Function of Y,BOOLEAN holds ((a 'imp' c) 'or' (b 'imp' c)) '&' (a '&' b) '<' c

proof end;

theorem :: BVFUNC_6:139

for Y being non empty set
for a, b, c, d being Function of Y,BOOLEAN st a '<' b & c '<' d holds
a 'or' c '<' b 'or' d

proof end;

theorem Th38a: :: BVFUNC_6:140

for Y being non empty set
for a, b being Function of Y,BOOLEAN holds a '<' a 'or' b

proof end;

theorem :: BVFUNC_6:141

for Y being non empty set
for a, b being Function of Y,BOOLEAN holds a '&' b '<' a 'or' b

proof end;

theorem :: BVFUNC_6:142

for Y being non empty set
for a, b, c being Function of Y,BOOLEAN holds ((a '&' b) 'or' (b '&' c)) 'or' (c '&' a) = ((a 'or' b) '&' (b 'or' c)) '&' (c 'or' a)

proof end;

Lm1: for Y being non empty set
for a, b, c being Function of Y,BOOLEAN holds ((a '&' ('not' b)) 'or' (b '&' ('not' c))) 'or' (c '&' ('not' a)) '<' ((b '&' ('not' a)) 'or' (c '&' ('not' b))) 'or' (a '&' ('not' c))

proof end;

theorem :: BVFUNC_6:143

for Y being non empty set
for a, b, c being Function of Y,BOOLEAN holds ((a '&' ('not' b)) 'or' (b '&' ('not' c))) 'or' (c '&' ('not' a)) = ((b '&' ('not' a)) 'or' (c '&' ('not' b))) 'or' (a '&' ('not' c))

proof end;

Lm2: for Y being non empty set
for a, b, c being Function of Y,BOOLEAN holds ((a 'or' ('not' b)) '&' (b 'or' ('not' c))) '&' (c 'or' ('not' a)) '<' ((b 'or' ('not' a)) '&' (c 'or' ('not' b))) '&' (a 'or' ('not' c))

proof end;

theorem :: BVFUNC_6:144

for Y being non empty set
for a, b, c being Function of Y,BOOLEAN holds ((a 'or' ('not' b)) '&' (b 'or' ('not' c))) '&' (c 'or' ('not' a)) = ((b 'or' ('not' a)) '&' (c 'or' ('not' b))) '&' (a 'or' ('not' c))

proof end;

theorem :: BVFUNC_6:145

for Y being non empty set
for a, b, c being Function of Y,BOOLEAN st c 'imp' a = I_el Y & c 'imp' b = I_el Y holds
c 'imp' (a 'or' b) = I_el Y

proof end;

theorem :: BVFUNC_6:146

for Y being non empty set
for a, b, c being Function of Y,BOOLEAN st a 'imp' c = I_el Y & b 'imp' c = I_el Y holds
(a '&' b) 'imp' c = I_el Y

proof end;

theorem :: BVFUNC_6:147

for Y being non empty set
for a1, a2, b1, b2, c1, c2 being Function of Y,BOOLEAN holds (((a1 'imp' a2) '&' (b1 'imp' b2)) '&' (c1 'imp' c2)) '&' ((a1 'or' b1) 'or' c1) '<' (a2 'or' b2) 'or' c2

proof end;

Lm3: for Y being non empty set
for a1, a2, b1, b2 being Function of Y,BOOLEAN holds (((a1 'imp' b1) '&' (a2 'imp' b2)) '&' (a1 'or' a2)) '&' ('not' (b1 '&' b2)) '<' (((b1 'imp' a1) '&' (b2 'imp' a2)) '&' (b1 'or' b2)) '&' ('not' (a1 '&' a2))

proof end;

theorem :: BVFUNC_6:148

for Y being non empty set
for a1, a2, b1, b2 being Function of Y,BOOLEAN holds (((a1 'imp' b1) '&' (a2 'imp' b2)) '&' (a1 'or' a2)) '&' ('not' (b1 '&' b2)) = (((b1 'imp' a1) '&' (b2 'imp' a2)) '&' (b1 'or' b2)) '&' ('not' (a1 '&' a2))

proof end;

theorem :: BVFUNC_6:149

for Y being non empty set
for a, b, c, d being Function of Y,BOOLEAN holds (a 'or' b) '&' (c 'or' d) = (((a '&' c) 'or' (a '&' d)) 'or' (b '&' c)) 'or' (b '&' d)

proof end;

theorem :: BVFUNC_6:150

for Y being non empty set
for a1, a2, b1, b2, b3 being Function of Y,BOOLEAN holds (a1 '&' a2) 'or' ((b1 '&' b2) '&' b3) = (((((a1 'or' b1) '&' (a1 'or' b2)) '&' (a1 'or' b3)) '&' (a2 'or' b1)) '&' (a2 'or' b2)) '&' (a2 'or' b3)

proof end;

theorem :: BVFUNC_6:151

for Y being non empty set
for a, b, c, d being Function of Y,BOOLEAN holds ((a 'imp' b) '&' (b 'imp' c)) '&' (c 'imp' d) = ((a 'imp' ((b '&' c) '&' d)) '&' (b 'imp' (c '&' d))) '&' (c 'imp' d)

proof end;

theorem :: BVFUNC_6:152

for Y being non empty set
for a, b, c, d being Function of Y,BOOLEAN holds ((a 'imp' c) '&' (b 'imp' d)) '&' (a 'or' b) '<' c 'or' d

proof end;

theorem :: BVFUNC_6:153

for Y being non empty set
for a, b, c being Function of Y,BOOLEAN holds (((a '&' b) 'imp' ('not' c)) '&' a) '&' c '<' 'not' b

proof end;

theorem :: BVFUNC_6:154

for Y being non empty set
for a1, a2, a3, b1, b2, b3 being Function of Y,BOOLEAN holds ((a1 '&' a2) '&' a3) 'imp' ((b1 'or' b2) 'or' b3) = ((('not' b1) '&' ('not' b2)) '&' a3) 'imp' ((('not' a1) 'or' ('not' a2)) 'or' b3)

proof end;

theorem :: BVFUNC_6:155

for Y being non empty set
for a, b, c being Function of Y,BOOLEAN holds ((a 'imp' b) '&' (b 'imp' c)) '&' (c 'imp' a) = ((a '&' b) '&' c) 'or' ((('not' a) '&' ('not' b)) '&' ('not' c))

proof end;

theorem :: BVFUNC_6:156

for Y being non empty set
for a, b, c being Function of Y,BOOLEAN holds (((a 'imp' b) '&' (b 'imp' c)) '&' (c 'imp' a)) '&' ((a 'or' b) 'or' c) = (a '&' b) '&' c

proof end;

Lm4: for Y being non empty set
for a, b, c being Function of Y,BOOLEAN holds (((('not' a) '&' b) '&' c) 'or' ((a '&' ('not' b)) '&' c)) 'or' ((a '&' b) '&' ('not' c)) '<' (a 'or' b) '&' ('not' ((a '&' b) '&' c))

proof end;

theorem :: BVFUNC_6:157

for Y being non empty set
for a, b, c being Function of Y,BOOLEAN holds (((a 'or' b) '&' (b 'or' c)) '&' (c 'or' a)) '&' ('not' ((a '&' b) '&' c)) = (((('not' a) '&' b) '&' c) 'or' ((a '&' ('not' b)) '&' c)) 'or' ((a '&' b) '&' ('not' c))

proof end;

theorem :: BVFUNC_6:158

for Y being non empty set
for a, b, c being Function of Y,BOOLEAN holds (a 'imp' b) '&' (b 'imp' c) '<' a 'imp' (b '&' c)

proof end;

theorem :: BVFUNC_6:159

for Y being non empty set
for a, b, c being Function of Y,BOOLEAN holds (a 'imp' b) '&' (b 'imp' c) '<' (a 'or' b) 'imp' c

proof end;

theorem Th19: :: BVFUNC_6:160

for Y being non empty set
for a, b, c being Function of Y,BOOLEAN holds (a 'imp' b) '&' (b 'imp' c) '<' a 'imp' (b 'or' c)

proof end;

theorem Th20: :: BVFUNC_6:161

for Y being non empty set
for a, b, c being Function of Y,BOOLEAN holds (a 'imp' b) '&' (b 'imp' c) '<' a 'imp' (b 'or' ('not' c))

proof end;

theorem Th21: :: BVFUNC_6:162

for Y being non empty set
for a, b, c being Function of Y,BOOLEAN holds (a 'imp' b) '&' (b 'imp' c) '<' b 'imp' (c 'or' a)

proof end;

theorem Th22: :: BVFUNC_6:163

for Y being non empty set
for a, b, c being Function of Y,BOOLEAN holds (a 'imp' b) '&' (b 'imp' c) '<' b 'imp' (c 'or' ('not' a))

proof end;

theorem :: BVFUNC_6:164

for Y being non empty set
for a, b, c being Function of Y,BOOLEAN holds (a 'imp' b) '&' (b 'imp' c) '<' (a 'imp' b) '&' (b 'imp' (c 'or' a))

proof end;

theorem :: BVFUNC_6:165

for Y being non empty set
for a, b, c being Function of Y,BOOLEAN holds (a 'imp' b) '&' (b 'imp' c) '<' (a 'imp' (b 'or' ('not' c))) '&' (b 'imp' c)

proof end;

theorem :: BVFUNC_6:166

for Y being non empty set
for a, b, c being Function of Y,BOOLEAN holds (a 'imp' b) '&' (b 'imp' c) '<' (a 'imp' (b 'or' c)) '&' (b 'imp' (c 'or' a))

proof end;

theorem :: BVFUNC_6:167

for Y being non empty set
for a, b, c being Function of Y,BOOLEAN holds (a 'imp' b) '&' (b 'imp' c) '<' (a 'imp' (b 'or' ('not' c))) '&' (b 'imp' (c 'or' a))

proof end;

theorem :: BVFUNC_6:168

for Y being non empty set
for a, b, c being Function of Y,BOOLEAN holds (a 'imp' b) '&' (b 'imp' c) '<' (a 'imp' (b 'or' ('not' c))) '&' (b 'imp' (c 'or' ('not' a)))

proof end;