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