BVFUNC_9: Propositional Calculus for Boolean Valued Functions, { V }

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

begin

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_9:1

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_9:2

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

proof end;

theorem :: BVFUNC_9:3

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_9:4

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_9:5

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_9:6

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_9:7

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_9:8

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_9:9

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_9:10

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_9:11

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_9:12

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_9:13

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_9:14

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_9:15

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 by Th1;

theorem :: BVFUNC_9:16

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_9:17

for Y being non empty set
for a, c, b being Function of 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 Function of 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 Function of 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 Function of 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 Function of 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 Function of 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 Function of 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 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;

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) '&' (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 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;

Lm10: 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_9:25

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 Th26: :: BVFUNC_9:26

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_9:27

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_9:28

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

theorem :: BVFUNC_9:29

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_9:30

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_9:31

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_9:32

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_9:33

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 Th34: :: BVFUNC_9:34

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_9:35

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_9:36

for Y being non empty set
for a, c, b being Function of 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 Function of 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 Function of 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 Function of Y,BOOLEAN holds a '<' a 'or' b

proof end;

theorem :: BVFUNC_9:40

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

proof end;