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