:: Propositional Calculus for Boolean Valued Functions, { V }
:: by Shunichi Kobayashi
::
:: Received May 5, 1999
:: Copyright (c) 1999-2011 Association of Mizar Users

begin

Lm1: for Y being non empty set
for a, b being Element of Funcs (Y,BOOLEAN) holds a '&' b '<' a

proof end;

Lm2: for Y being non empty set
for a, b, c being Element of Funcs (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 Element of Funcs (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 Element of Funcs (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 Element of Funcs (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 Element of Funcs (Y,BOOLEAN) holds
( (((((a '&' b) '&' c) '&' d) '&' e) '&' f) '&' g '<' a & (((((a '&' b) '&' c) '&' d) '&' e) '&' f) '&' g '<' b )

proof end;

Lm7: for Y being non empty set
for a, b, c, d, e, f, g being Element of Funcs (Y,BOOLEAN) holds
( ((((((a '&' b) '&' c) '&' d) '&' e) '&' f) '&' g) 'imp' a = I_el Y & ((((((a '&' b) '&' c) '&' d) '&' e) '&' f) '&' g) 'imp' b = I_el Y & ((((((a '&' b) '&' c) '&' d) '&' e) '&' f) '&' g) 'imp' c = I_el Y & ((((((a '&' b) '&' c) '&' d) '&' e) '&' f) '&' g) 'imp' d = I_el Y & ((((((a '&' b) '&' c) '&' d) '&' e) '&' f) '&' g) 'imp' e = I_el Y & ((((((a '&' b) '&' c) '&' d) '&' e) '&' f) '&' g) 'imp' f = I_el Y & ((((((a '&' b) '&' c) '&' d) '&' e) '&' f) '&' g) 'imp' g = I_el Y )

proof end;

theorem Th1: :: BVFUNC_9:1

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

proof end;

theorem Th2: :: BVFUNC_9:2

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

proof end;

theorem :: BVFUNC_9:3

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

proof end;

theorem :: BVFUNC_9:4

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

proof end;

theorem :: BVFUNC_9:5

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

proof end;

theorem :: BVFUNC_9:6

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

proof end;

theorem :: BVFUNC_9:7

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

proof end;

theorem :: BVFUNC_9:8

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

proof end;

theorem :: BVFUNC_9:9

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

proof end;

theorem :: BVFUNC_9:10

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

proof end;

theorem :: BVFUNC_9:11

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

proof end;

theorem :: BVFUNC_9:12

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

proof end;

theorem :: BVFUNC_9:13

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

proof end;

theorem :: BVFUNC_9:14

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

proof end;

theorem :: BVFUNC_9:15

for Y being non empty set
for a, b, c being Element of Funcs (Y,BOOLEAN) holds (a 'or' b) '&' (b 'imp' c) '<' a 'or' c by Th1;

theorem :: BVFUNC_9:16

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

proof end;

theorem :: BVFUNC_9:17

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

proof end;

theorem :: BVFUNC_9:18

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

proof end;

theorem Th19: :: BVFUNC_9:19

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

proof end;

theorem :: BVFUNC_9:20

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

proof end;

theorem Th21: :: BVFUNC_9:21

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

proof end;

theorem Th22: :: BVFUNC_9:22

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

proof end;

theorem :: BVFUNC_9:23

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

proof end;

theorem Th24: :: BVFUNC_9:24

for Y being non empty set
for a1, b1, c1, a2, b2, c2 being Element of Funcs (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;

Lm8: for Y being non empty set
for a1, b1, c1, a2, b2, c2 being Element of Funcs (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;

Lm9: for Y being non empty set
for a1, b1, c1, a2, b2, c2 being Element of Funcs (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;

Lm10: for Y being non empty set
for a1, b1, c1, a2, b2, c2 being Element of Funcs (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_9:25

for Y being non empty set
for a1, b1, c1, a2, b2, c2 being Element of Funcs (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 Th26: :: BVFUNC_9:26

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

proof end;

theorem :: BVFUNC_9:27

for Y being non empty set
for a1, b1, c1, a2, b2, c2 being Element of Funcs (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_9:28

for Y being non empty set
for a, b being Element of Funcs (Y,BOOLEAN) holds a '&' b '<' a by Lm1;

theorem :: BVFUNC_9:29

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

theorem :: BVFUNC_9:30

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

theorem :: BVFUNC_9:31

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

theorem :: BVFUNC_9:32

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

theorem :: BVFUNC_9:33

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

theorem Th34: :: BVFUNC_9:34

for Y being non empty set
for a, b, c, d being Element of Funcs (Y,BOOLEAN) st a '<' b & c '<' d holds
a '&' c '<' b '&' d

proof end;

theorem :: BVFUNC_9:35

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

proof end;

theorem :: BVFUNC_9:36

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

proof end;

theorem :: BVFUNC_9:37

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

proof end;

theorem :: BVFUNC_9:38

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

proof end;

theorem Th39: :: BVFUNC_9:39

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

proof end;

theorem :: BVFUNC_9:40

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

proof end;