:: Propositional Calculus for Boolean Valued Functions, VI
:: by Shunichi Kobayashi
::
:: Received July 14, 1999
:: Copyright (c) 1999-2011 Association of Mizar Users

begin

theorem :: BVFUNC10:1

for Y being non empty set
for a, b, c being Element of Funcs (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 Element of Funcs (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 :: BVFUNC10:2

for Y being non empty set
for a, b, c being Element of Funcs (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 Element of Funcs (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 :: BVFUNC10:3

for Y being non empty set
for a, b, c being Element of Funcs (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 :: BVFUNC10:4

for Y being non empty set
for a, b, c being Element of Funcs (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 :: BVFUNC10:5

for Y being non empty set
for a, b, c being Element of Funcs (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 :: BVFUNC10:6

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

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

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

proof end;

theorem :: BVFUNC10:9

for Y being non empty set
for a1, a2, b1, b2, b3 being Element of Funcs (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 :: BVFUNC10:10

for Y being non empty set
for a, b, c, d being Element of Funcs (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 :: BVFUNC10:11

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

proof end;

theorem :: BVFUNC10:12

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

proof end;

theorem :: BVFUNC10:13

for Y being non empty set
for a1, a2, a3, b1, b2, b3 being Element of Funcs (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 :: BVFUNC10:14

for Y being non empty set
for a, b, c being Element of Funcs (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 :: BVFUNC10:15

for Y being non empty set
for a, b, c being Element of Funcs (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 Element of Funcs (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 :: BVFUNC10:16

for Y being non empty set
for a, b, c being Element of Funcs (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 :: BVFUNC10:17

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

proof end;

theorem :: BVFUNC10:18

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

proof end;

theorem Th19: :: BVFUNC10:19

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

proof end;

theorem Th20: :: BVFUNC10:20

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

proof end;

theorem Th21: :: BVFUNC10:21

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

proof end;

theorem Th22: :: BVFUNC10:22

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

proof end;

theorem :: BVFUNC10:23

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

proof end;

theorem :: BVFUNC10:24

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

proof end;

theorem :: BVFUNC10:25

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

proof end;

theorem :: BVFUNC10:26

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

proof end;

theorem :: BVFUNC10:27

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

proof end;