Copyright (c) 1999 Association of Mizar Users
environ
vocabulary FUNCT_2, MARGREL1, ZF_LANG, PARTIT1, BVFUNC_1;
notation XBOOLE_0, SUBSET_1, MARGREL1, VALUAT_1, FRAENKEL, BINARITH, BVFUNC_1;
constructors BINARITH, BVFUNC_1;
clusters MARGREL1, VALUAT_1, BINARITH, FRAENKEL;
definitions BVFUNC_1;
theorems MARGREL1, BINARITH, BVFUNC_1, BVFUNC_4, BVFUNC_5, BVFUNC_6, BVFUNC_7,
VALUAT_1;
begin
::Chap. 1 Propositional Calculus
reserve Y for non empty set,
a,b,c,d,e,f,g for Element of Funcs(Y,BOOLEAN);
Lm1: a '&' b '<' a
proof
let x be Element of Y;
assume Pj(a '&' b,x) = TRUE;
then Pj(a,x) '&' Pj(b,x) = TRUE by VALUAT_1:def 6;
hence thesis by MARGREL1:45;
end;
Lm2: a '&' b '&' c '<' a & a '&' b '&' c '<' b
proof
A1:a '&' b '&' c = c '&' b '&' a by BVFUNC_1:7;
c '&' b '&' a 'imp' a = I_el(Y) by BVFUNC_6:39;
hence a '&' b '&' c '<' a by A1,BVFUNC_1:19;
A2:a '&' b '&' c = a '&' c '&' b by BVFUNC_1:7;
a '&' c '&' b 'imp' b = I_el(Y) by BVFUNC_6:39;
hence thesis by A2,BVFUNC_1:19;
end;
Lm3: a '&' b '&' c '&' d '<' a &
a '&' b '&' c '&' d '<' b
proof
thus a '&' b '&' c '&' d '<' a
proof
A1:a '&' b '&' c '&' d = d '&' c '&' (b '&' a) by BVFUNC_1:7
.=d '&' c '&' b '&' a by BVFUNC_1:7;
d '&' c '&' b '&' a 'imp' a = I_el(Y) by BVFUNC_6:39;
hence thesis by A1,BVFUNC_1:19;
end;
A2:a '&' b '&' c '&' d = a '&' c '&' b '&' d by BVFUNC_1:7
.=a '&' c '&' d '&' b by BVFUNC_1:7;
a '&' c '&' d '&' b 'imp' b = I_el(Y) by BVFUNC_6:39;
hence thesis by A2,BVFUNC_1:19;
end;
Lm4: a '&' b '&' c '&' d '&' e '<' a &
a '&' b '&' c '&' d '&' e '<' b
proof
thus a '&' b '&' c '&' d '&' e '<' a
proof
A1:a '&' b '&' c '&' d '&' e =e '&' d '&' (c '&' (b '&' a)) by BVFUNC_1:7
.=e '&' d '&' c '&' (b '&' a) by BVFUNC_1:7
.=e '&' d '&' c '&' b '&' a by BVFUNC_1:7;
e '&' d '&' c '&' b '&' a 'imp' a = I_el(Y) by BVFUNC_6:39;
hence thesis by A1,BVFUNC_1:19;
end;
A2:a '&' b '&' c '&' d '&' e
=a '&' c '&' b '&' d '&' e by BVFUNC_1:7
.=a '&' c '&' d '&' b '&' e by BVFUNC_1:7
.=a '&' c '&' d '&' e '&' b by BVFUNC_1:7;
a '&' c '&' d '&' e '&' b 'imp' b = I_el(Y) by BVFUNC_6:39;
hence thesis by A2,BVFUNC_1:19;
end;
Lm5: a '&' b '&' c '&' d '&' e '&' f '<' a &
a '&' b '&' c '&' d '&' e '&' f '<' b
proof
thus a '&' b '&' c '&' d '&' e '&' f '<' a
proof
A1:a '&' b '&' c '&' d '&' e '&' f
=f '&' e '&' (d '&' (c '&' (b '&' a))) by BVFUNC_1:7
.=f '&' e '&' d '&' (c '&' (b '&' a)) by BVFUNC_1:7
.=f '&' e '&' d '&' c '&' (b '&' a) by BVFUNC_1:7
.=f '&' e '&' d '&' c '&' b '&' a by BVFUNC_1:7;
f '&' e '&' d '&' c '&' b '&' a 'imp' a = I_el(Y) by BVFUNC_6:39;
hence thesis by A1,BVFUNC_1:19;
end;
A2:a '&' b '&' c '&' d '&' e '&' f
=f '&' e '&' (d '&' (c '&' (b '&' a))) by BVFUNC_1:7
.=f '&' e '&' d '&' (c '&' (b '&' a)) by BVFUNC_1:7
.=f '&' e '&' d '&' c '&' (b '&' a) by BVFUNC_1:7
.=f '&' e '&' d '&' c '&' a '&' b by BVFUNC_1:7;
f '&' e '&' d '&' c '&' a '&' b 'imp' b = I_el(Y) by BVFUNC_6:39;
hence thesis by A2,BVFUNC_1:19;
end;
Lm6: a '&' b '&' c '&' d '&' e '&' f '&' g '<' a &
a '&' b '&' c '&' d '&' e '&' f '&' g '<' b
proof
thus a '&' b '&' c '&' d '&' e '&' f '&' g '<' a
proof
A1:a '&' b '&' c '&' d '&' e '&' f '&' g
=g '&' f '&' (e '&' (d '&' (c '&' (b '&' a)))) by BVFUNC_1:7
.=g '&' f '&' e '&' (d '&' (c '&' (b '&' a))) by BVFUNC_1:7
.=g '&' f '&' e '&' d '&' (c '&' (b '&' a)) by BVFUNC_1:7
.=g '&' f '&' e '&' d '&' c '&' (b '&' a) by BVFUNC_1:7
.=g '&' f '&' e '&' d '&' c '&' b '&' a by BVFUNC_1:7;
g '&' f '&' e '&' d '&' c '&' b '&' a 'imp' a = I_el(Y)
by BVFUNC_6:39;
hence thesis by A1,BVFUNC_1:19;
end;
A2:a '&' b '&' c '&' d '&' e '&' f '&' g
=a '&' (c '&' b) '&' d '&' e '&' f '&' g by BVFUNC_1:7
.=a '&' (d '&' (c '&' b)) '&' e '&' f '&' g by BVFUNC_1:7
.=a '&' (e '&' (d '&' (c '&' b))) '&' f '&' g by BVFUNC_1:7
.=a '&' (f '&' (e '&' (d '&' (c '&' b)))) '&' g by BVFUNC_1:7
.=a '&' g '&' (f '&' (e '&' (d '&' (c '&' b)))) by BVFUNC_1:7
.=a '&' g '&' f '&' (e '&' (d '&' (c '&' b))) by BVFUNC_1:7
.=a '&' g '&' f '&' e '&' (d '&' (c '&' b)) by BVFUNC_1:7
.=a '&' g '&' f '&' e '&' d '&' (c '&' b) by BVFUNC_1:7
.=a '&' g '&' f '&' e '&' d '&' c '&' b by BVFUNC_1:7;
a '&' g '&' f '&' e '&' d '&' c '&' b 'imp' b = I_el(Y) by BVFUNC_6:39;
hence thesis by A2,BVFUNC_1:19;
end;
Lm7: 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
let a,b,c,d,e,f,g be Element of Funcs(Y,BOOLEAN);
A1:a '&' b '&' c '&' d '&' e '&' f '&' g '<' a by Lm6;
A2:a '&' b '&' c '&' d '&' e '&' f '&' g '<' b by Lm6;
A3: a '&' b '&' c '&' d '&' e '&' f '&' g '<' c by Lm5;
A4: (a '&' b '&' c '&' d '&' e '&' f '&' g '<' d) by Lm4;
A5: (a '&' b '&' c '&' d '&' e '&' f '&' g '<' e) by Lm3;
A6: (a '&' b '&' c '&' d '&' e '&' f '&' g '<' f) by Lm2;
(a '&' b '&' c '&' d '&' e '&' f '&' g '<' g) by Lm1;
hence thesis by A1,A2,A3,A4,A5,A6,BVFUNC_1:19;
end;
theorem Th1:
(a 'or' b) '&' (b 'imp' c) '<' a 'or' c
proof
let z be Element of Y;
assume A1:Pj((a 'or' b) '&' (b 'imp' c),z)=TRUE;
A2:Pj((a 'or' b) '&' (b 'imp' c),z)
=Pj(a 'or' b,z) '&' Pj(b 'imp' c,z) by VALUAT_1:def 6
.=Pj(a 'or' b,z) '&' Pj('not' b 'or' c,z) by BVFUNC_4:8
.=Pj(a 'or' b,z) '&' (Pj('not' b,z) 'or' Pj(c,z)) by BVFUNC_1:def 7
.=(Pj(a,z) 'or' Pj(b,z)) '&' (Pj('not' b,z) 'or' Pj(c,z)) by BVFUNC_1:def 7;
now assume Pj(a 'or' c,z)<>TRUE;
then Pj(a 'or' c,z)=FALSE by MARGREL1:43;
then A3:Pj(a,z) 'or' Pj(c,z)=FALSE by BVFUNC_1:def 7;
A4:Pj(a,z)=TRUE or Pj(a,z)=FALSE by MARGREL1:39;
Pj(c,z)=TRUE or Pj(c,z)=FALSE by MARGREL1:39;
then Pj(a,z)=FALSE & Pj(c,z)=FALSE
by A3,A4,BINARITH:19;
then (Pj(a,z) 'or' Pj(b,z)) '&' (Pj('not' b,z) 'or' Pj(c,z))
=Pj(b,z) '&' (Pj('not' b,z) 'or' FALSE) by BINARITH:7
.=Pj(b,z) '&' Pj('not' b,z) by BINARITH:7
.=Pj(b,z) '&' 'not' Pj(b,z) by VALUAT_1:def 5
.=FALSE by MARGREL1:46;
hence contradiction by A1,A2,MARGREL1:43;
end;
hence thesis;
end;
theorem Th2:
a '&' (a 'imp' b) '<' b
proof
let z be Element of Y;
assume A1:Pj(a '&' (a 'imp' b),z)=TRUE;
A2: Pj(a '&' (a 'imp' b),z)
=Pj(a,z) '&' Pj(a 'imp' b,z) by VALUAT_1:def 6
.=Pj(a,z) '&' Pj('not' a 'or' b,z) by BVFUNC_4:8
.=Pj(a,z) '&' (Pj('not' a,z) 'or' Pj(b,z)) by BVFUNC_1:def 7
.=Pj(a,z) '&' Pj('not' a,z) 'or' Pj(a,z) '&' Pj(b,z) by BINARITH:22
.=Pj(a,z) '&' 'not' Pj(a,z) 'or' Pj(a,z) '&' Pj(b,z) by VALUAT_1:def 5
.=FALSE 'or' Pj(a,z) '&' Pj(b,z) by MARGREL1:46
.=Pj(a,z) '&' Pj(b,z) by BINARITH:7;
now assume Pj(b,z)<>TRUE;
then Pj(a,z) '&' Pj(b,z)
=FALSE '&' Pj(a,z) by MARGREL1:43
.=FALSE by MARGREL1:49;
hence contradiction by A1,A2,MARGREL1:43;
end;
hence thesis;
end;
theorem
(a 'imp' b) '&' 'not' b '<' 'not' a
proof
let z be Element of Y;
assume A1:Pj((a 'imp' b) '&' 'not' b,z)=TRUE;
A2: Pj((a 'imp' b) '&' 'not' b,z)
=Pj(a 'imp' b,z) '&' Pj('not' b,z) by VALUAT_1:def 6
.=Pj('not' a 'or' b,z) '&' Pj('not' b,z) by BVFUNC_4:8
.=Pj('not' b,z) '&' (Pj('not' a,z) 'or' Pj(b,z)) by BVFUNC_1:def 7
.=Pj('not' b,z) '&' Pj('not' a,z) 'or' Pj('not' b,z) '&' Pj(b,z)
by BINARITH:22
.=Pj('not' b,z) '&' Pj('not' a,z) 'or' 'not'
Pj(b,z) '&' Pj(b,z) by VALUAT_1:def 5
.=Pj('not' b,z) '&' Pj('not' a,z) 'or' FALSE by MARGREL1:46
.=Pj('not' b,z) '&' Pj('not' a,z) by BINARITH:7;
now assume Pj('not' a,z)<>TRUE;
then Pj('not' b,z) '&' Pj('not' a,z)
=FALSE '&' Pj('not' b,z) by MARGREL1:43
.=FALSE by MARGREL1:49;
hence contradiction by A1,A2,MARGREL1:43;
end;
hence thesis;
end;
theorem
(a 'or' b) '&' 'not' a '<' b
proof
let z be Element of Y;
assume A1:Pj((a 'or' b) '&' 'not' a,z)=TRUE;
A2: Pj((a 'or' b) '&' 'not' a,z)
=Pj(a 'or' b,z) '&' Pj('not' a,z) by VALUAT_1:def 6
.=Pj('not' a,z) '&' (Pj(a,z) 'or' Pj(b,z)) by BVFUNC_1:def 7
.=Pj('not' a,z) '&' Pj(a,z) 'or' Pj('not' a,z) '&' Pj(b,z) by BINARITH:22
.='not' Pj(a,z) '&' Pj(a,z) 'or' Pj('not' a,z) '&' Pj(b,z) by VALUAT_1:def 5
.=FALSE 'or' Pj('not' a,z) '&' Pj(b,z) by MARGREL1:46
.=Pj('not' a,z) '&' Pj(b,z) by BINARITH:7;
now assume Pj(b,z)<>TRUE;
then Pj('not' a,z) '&' Pj(b,z)
=FALSE '&' Pj('not' a,z) by MARGREL1:43
.=FALSE by MARGREL1:49;
hence contradiction by A1,A2,MARGREL1:43;
end;
hence thesis;
end;
theorem
(a 'imp' b) '&' ('not' a 'imp' b) '<' b
proof
let z be Element of Y;
assume A1:Pj((a 'imp' b) '&' ('not' a 'imp' b),z)=TRUE;
A2: Pj((a 'imp' b) '&' ('not' a 'imp' b),z)
=Pj(a 'imp' b,z) '&' Pj('not' a 'imp' b,z) by VALUAT_1:def 6
.=Pj('not' a 'or' b,z) '&' Pj('not' a 'imp' b,z) by BVFUNC_4:8
.=Pj('not' a 'or' b,z) '&' Pj('not' 'not' a 'or' b,z) by BVFUNC_4:8
.=Pj('not' a 'or' b,z) '&' Pj(a 'or' b,z) by BVFUNC_1:4
.=(Pj('not' a,z) 'or' Pj(b,z)) '&' Pj(a 'or' b,z) by BVFUNC_1:def 7
.=(Pj('not'
a,z) 'or' Pj(b,z)) '&' (Pj(a,z) 'or' Pj(b,z)) by BVFUNC_1:def 7;
now assume Pj(b,z)<>TRUE;
then Pj(b,z)=FALSE by MARGREL1:43;
then (Pj('not' a,z) 'or' Pj(b,z)) '&' (Pj(a,z) 'or' Pj(b,z))
=Pj('not' a,z) '&' (Pj(a,z) 'or' FALSE) by BINARITH:7
.=Pj('not' a,z) '&' Pj(a,z) by BINARITH:7
.='not' Pj(a,z) '&' Pj(a,z) by VALUAT_1:def 5
.=FALSE by MARGREL1:46;
hence contradiction by A1,A2,MARGREL1:43;
end;
hence thesis;
end;
theorem
(a 'imp' b) '&' (a 'imp' 'not' b) '<' 'not' a
proof
let z be Element of Y;
assume A1:Pj((a 'imp' b) '&' (a 'imp' 'not' b),z)=TRUE;
A2: Pj((a 'imp' b) '&' (a 'imp' 'not' b),z)
=Pj(a 'imp' b,z) '&' Pj(a 'imp' 'not' b,z) by VALUAT_1:def 6
.=Pj('not' a 'or' b,z) '&' Pj(a 'imp' 'not' b,z) by BVFUNC_4:8
.=Pj('not' a 'or' b,z) '&' Pj('not' a 'or' 'not' b,z) by BVFUNC_4:8
.=(Pj('not' a,z) 'or' Pj(b,z)) '&' Pj('not' a 'or' 'not' b,z)
by BVFUNC_1:def 7
.=(Pj('not' a,z) 'or' Pj(b,z)) '&' (Pj('not' a,z) 'or' Pj('not'
b,z)) by BVFUNC_1:def 7;
now assume Pj('not' a,z)<>TRUE;
then Pj('not' a,z)=FALSE by MARGREL1:43;
then (Pj('not' a,z) 'or' Pj(b,z)) '&' (Pj('not' a,z) 'or' Pj('not' b,z))
=Pj(b,z) '&' (FALSE 'or' Pj('not' b,z)) by BINARITH:7
.=Pj(b,z) '&' Pj('not' b,z) by BINARITH:7
.=Pj(b,z) '&' 'not' Pj(b,z) by VALUAT_1:def 5
.=FALSE by MARGREL1:46;
hence contradiction by A1,A2,MARGREL1:43;
end;
hence thesis;
end;
theorem
a 'imp' (b '&' c) '<' a 'imp' b
proof
let z be Element of Y;
assume A1:Pj(a 'imp' (b '&' c),z)=TRUE;
A2: Pj(a 'imp' (b '&' c),z)
=Pj('not' a 'or' (b '&' c),z) by BVFUNC_4:8
.=Pj('not' a,z) 'or' Pj(b '&' c,z) by BVFUNC_1:def 7
.=Pj('not' a,z) 'or' (Pj(b,z) '&' Pj(c,z)) by VALUAT_1:def 6;
now assume Pj(a 'imp' b,z)<>TRUE;
then Pj(a 'imp' b,z)=FALSE by MARGREL1:43;
then Pj('not' a 'or' b,z)=FALSE by BVFUNC_4:8;
then A3:Pj('not' a,z) 'or' Pj(b,z)=FALSE by BVFUNC_1:def 7;
Pj('not' a,z) 'or' (Pj(b,z) '&' Pj(c,z))
=(Pj('not' a,z) 'or' Pj(b,z)) '&' (Pj('not'
a,z) 'or' Pj(c,z)) by BINARITH:23
.=FALSE by A3,MARGREL1:49;
hence contradiction by A1,A2,MARGREL1:43;
end;
hence thesis;
end;
theorem
(a 'or' b) 'imp' c '<' a 'imp' c
proof
let z be Element of Y;
assume A1:Pj((a 'or' b) 'imp' c,z)=TRUE;
A2: Pj((a 'or' b) 'imp' c,z)
=Pj('not'( a 'or' b) 'or' c,z) by BVFUNC_4:8
.=Pj(('not' a '&' 'not' b) 'or' c,z) by BVFUNC_1:16
.=Pj('not' a '&' 'not' b,z) 'or' Pj(c,z) by BVFUNC_1:def 7
.=(Pj('not' a,z) '&' Pj('not' b,z)) 'or' Pj(c,z) by VALUAT_1:def 6;
now assume Pj(a 'imp' c,z)<>TRUE;
then Pj(a 'imp' c,z)=FALSE by MARGREL1:43;
then Pj('not' a 'or' c,z)=FALSE by BVFUNC_4:8;
then A3:Pj('not' a,z) 'or' Pj(c,z)=FALSE by BVFUNC_1:def 7;
(Pj('not' a,z) '&' Pj('not' b,z)) 'or' Pj(c,z)
=(Pj(c,z) 'or' Pj('not' a,z)) '&' (Pj(c,z) 'or' Pj('not'
b,z)) by BINARITH:23
.=FALSE by A3,MARGREL1:49;
hence contradiction by A1,A2,MARGREL1:43;
end;
hence thesis;
end;
theorem
a 'imp' b '<' (a '&' c) 'imp' b
proof
let z be Element of Y;
assume A1:Pj(a 'imp' b,z)=TRUE;
A2: Pj(a 'imp' b,z)
=Pj('not' a 'or' b,z) by BVFUNC_4:8
.=Pj('not' a,z) 'or' Pj(b,z) by BVFUNC_1:def 7;
now assume Pj((a '&' c) 'imp' b,z)<>TRUE;
then Pj((a '&' c) 'imp' b,z)=FALSE by MARGREL1:43;
then Pj('not'( a '&' c) 'or' b,z)=FALSE by BVFUNC_4:8;
then Pj('not'( a '&' c),z) 'or' Pj(b,z)=FALSE by BVFUNC_1:def 7;
then Pj(('not' a 'or' 'not' c),z) 'or' Pj(b,z)=FALSE by BVFUNC_1:17;
then (Pj('not' c,z) 'or' Pj('not' a,z)) 'or' Pj(b,z)=FALSE by BVFUNC_1:
def 7
;
then A3:Pj('not' c,z) 'or' (Pj('not' a,z) 'or' Pj(b,z))=FALSE by BINARITH
:20;
Pj('not' c,z) 'or' (Pj('not' a,z) 'or' Pj(b,z)) =TRUE by A1,A2,BINARITH
:19;
hence contradiction by A3,MARGREL1:43;
end;
hence thesis;
end;
theorem
a 'imp' b '<' (a '&' c) 'imp' (b '&' c)
proof
let z be Element of Y;
assume A1:Pj(a 'imp' b,z)=TRUE;
A2: Pj(a 'imp' b,z)
=Pj('not' a 'or' b,z) by BVFUNC_4:8
.=Pj('not' a,z) 'or' Pj(b,z) by BVFUNC_1:def 7;
now assume Pj((a '&' c) 'imp' (b '&' c),z)<>TRUE;
then Pj((a '&' c) 'imp' (b '&' c),z)=FALSE by MARGREL1:43;
then Pj('not'( a '&' c) 'or' (b '&' c),z)=FALSE by BVFUNC_4:8;
then Pj('not'( a '&' c),z) 'or' Pj(b '&' c,z)=FALSE by BVFUNC_1:def 7;
then Pj(('not' a 'or' 'not' c),z) 'or' Pj(b '&' c,z)=FALSE
by BVFUNC_1:17;
then (Pj('not' c,z) 'or' Pj('not' a,z)) 'or' Pj(b '&' c,z)=FALSE by
BVFUNC_1:def 7;
then Pj('not' c,z) 'or' (Pj('not'
a,z) 'or' Pj(b '&' c,z))=FALSE by BINARITH:20;
then Pj('not' c,z) 'or' (Pj('not' a,z) 'or' (Pj(b,z) '&' Pj(c,z)))=FALSE
by VALUAT_1:def 6;
then A3: Pj('not' c,z) 'or' ((Pj('not' a,z) 'or' Pj(b,z)) '&' (Pj('not'
a,z) 'or' Pj(c,z)))=FALSE
by BINARITH:23;
Pj('not' c,z) 'or' ((Pj('not' a,z) 'or' Pj(b,z)) '&' (Pj('not'
a,z) 'or' Pj(c,z)))
=Pj('not' c,z) 'or' (Pj(c,z) 'or' Pj('not' a,z)) by A1,A2,MARGREL1:50
.=Pj('not' c,z) 'or' Pj(c,z) 'or' Pj('not' a,z) by BINARITH:20
.='not' Pj(c,z) 'or' Pj(c,z) 'or' Pj('not' a,z) by VALUAT_1:def 5
.=TRUE 'or' Pj('not' a,z) by BINARITH:18
.=TRUE by BINARITH:19;
hence contradiction by A3,MARGREL1:43;
end;
hence thesis;
end;
theorem
a 'imp' b '<' a 'imp' (b 'or' c)
proof
let z be Element of Y;
assume A1:Pj(a 'imp' b,z)=TRUE;
A2: Pj(a 'imp' b,z)
=Pj('not' a 'or' b,z) by BVFUNC_4:8
.=Pj('not' a,z) 'or' Pj(b,z) by BVFUNC_1:def 7;
now assume A3: Pj(a 'imp' (b 'or' c),z)<>TRUE;
Pj(a 'imp' (b 'or' c),z)
=Pj('not' a 'or' (b 'or' c),z) by BVFUNC_4:8
.=Pj('not' a,z) 'or' Pj(b 'or' c,z) by BVFUNC_1:def 7
.=Pj('not' a,z) 'or' (Pj(b,z) 'or' Pj(c,z)) by BVFUNC_1:def 7
.=(Pj('not' a,z) 'or' Pj(b,z)) 'or' Pj(c,z) by BINARITH:20
.=TRUE by A1,A2,BINARITH:19;
hence contradiction by A3;
end;
hence thesis;
end;
theorem
a 'imp' b '<' (a 'or' c) 'imp' (b 'or' c)
proof
let z be Element of Y;
assume A1:Pj(a 'imp' b,z)=TRUE;
A2: Pj(a 'imp' b,z)
=Pj('not' a 'or' b,z) by BVFUNC_4:8
.=Pj('not' a,z) 'or' Pj(b,z) by BVFUNC_1:def 7;
now assume A3: Pj((a 'or' c) 'imp' (b 'or' c),z)<>TRUE;
Pj((a 'or' c) 'imp' (b 'or' c),z)
=Pj('not'( a 'or' c) 'or' (b 'or' c),z) by BVFUNC_4:8
.=Pj('not'( a 'or' c),z) 'or' Pj(b 'or' c,z) by BVFUNC_1:def 7
.=Pj('not'( a 'or' c),z) 'or' (Pj(b,z) 'or' Pj(c,z)) by BVFUNC_1:def 7
.=(Pj('not'( a 'or' c),z) 'or' Pj(b,z)) 'or' Pj(c,z) by BINARITH:20
.=(Pj(('not' a '&' 'not' c),z) 'or' Pj(b,z)) 'or' Pj(c,z) by BVFUNC_1:16
.=(Pj(b,z) 'or' (Pj('not' a,z) '&' Pj('not'
c,z))) 'or' Pj(c,z) by VALUAT_1:def 6
.=((Pj('not' a,z) 'or' Pj(b,z)) '&' (Pj(b,z) 'or' Pj('not'
c,z))) 'or' Pj(c,z) by BINARITH:23
.=(Pj(b,z) 'or' Pj('not' c,z)) 'or' Pj(c,z) by A1,A2,MARGREL1:50
.=Pj(b,z) 'or' (Pj('not' c,z) 'or' Pj(c,z)) by BINARITH:20
.=Pj(b,z) 'or' ('not' Pj(c,z) 'or' Pj(c,z)) by VALUAT_1:def 5
.=Pj(b,z) 'or' TRUE by BINARITH:18
.=TRUE by BINARITH:19;
hence contradiction by A3;
end;
hence thesis;
end;
theorem
a '&' b 'or' c '<' a 'or' c
proof
let z be Element of Y;
assume A1:Pj(a '&' b 'or' c,z)=TRUE;
A2: Pj(a '&' b 'or' c,z)
=Pj(a '&' b,z) 'or' Pj(c,z) by BVFUNC_1:def 7
.=(Pj(a,z) '&' Pj(b,z)) 'or' Pj(c,z) by VALUAT_1:def 6;
now assume Pj(a 'or' c,z)<>TRUE;
then Pj(a 'or' c,z)=FALSE by MARGREL1:43;
then A3:Pj(a,z) 'or' Pj(c,z)=FALSE by BVFUNC_1:def 7;
(Pj(a,z) '&' Pj(b,z)) 'or' Pj(c,z)
=(Pj(c,z) 'or' Pj(a,z)) '&' (Pj(c,z) 'or' Pj(b,z)) by BINARITH:23
.=FALSE by A3,MARGREL1:49;
hence contradiction by A1,A2,MARGREL1:43;
end;
hence thesis;
end;
theorem
(a '&' b) 'or' (c '&' d) '<' a 'or' c
proof
let z be Element of Y;
assume A1:Pj((a '&' b) 'or' (c '&' d),z)=TRUE;
A2: Pj((a '&' b) 'or' (c '&' d),z)
=Pj(a '&' b,z) 'or' Pj(c '&' d,z) by BVFUNC_1:def 7
.=(Pj(a,z) '&' Pj(b,z)) 'or' Pj(c '&' d,z) by VALUAT_1:def 6
.=(Pj(a,z) '&' Pj(b,z)) 'or' (Pj(c,z) '&' Pj(d,z))
by VALUAT_1:def 6;
now assume Pj(a 'or' c,z)<>TRUE;
then Pj(a 'or' c,z)=FALSE by MARGREL1:43;
then A3:Pj(a,z) 'or' Pj(c,z)=FALSE by BVFUNC_1:def 7;
(Pj(a,z) '&' Pj(b,z)) 'or' (Pj(c,z) '&' Pj(d,z))
=(Pj(c,z) 'or' (Pj(a,z) '&' Pj(b,z))) '&'
((Pj(a,z) '&' Pj(b,z)) 'or' Pj(d,z)) by BINARITH:23
.=((Pj(a,z) 'or' Pj(c,z)) '&' (Pj(c,z) 'or' Pj(b,z))) '&'
((Pj(a,z) '&' Pj(b,z)) 'or' Pj(d,z)) by BINARITH:23
.=FALSE '&'
((Pj(a,z) '&' Pj(b,z)) 'or' Pj(d,z)) by A3,MARGREL1:49
.=FALSE by MARGREL1:49;
hence contradiction by A1,A2,MARGREL1:43;
end;
hence thesis;
end;
theorem
(a 'or' b) '&' (b 'imp' c) '<' a 'or' c
proof
let z be Element of Y;
assume A1:Pj((a 'or' b) '&' (b 'imp' c),z)=TRUE;
A2: Pj((a 'or' b) '&' (b 'imp' c),z)
=Pj((a 'or' b) '&' ('not' b 'or' c),z) by BVFUNC_4:8
.=Pj(a 'or' b,z) '&' Pj('not' b 'or' c,z) by VALUAT_1:def 6
.=(Pj(a,z) 'or' Pj(b,z)) '&' Pj('not' b 'or' c,z) by BVFUNC_1:def 7
.=(Pj(a,z) 'or' Pj(b,z)) '&' (Pj('not' b,z) 'or' Pj(c,z))
by BVFUNC_1:def 7;
now assume Pj(a 'or' c,z)<>TRUE;
then Pj(a 'or' c,z)=FALSE by MARGREL1:43;
then A3:Pj(a,z) 'or' Pj(c,z)=FALSE by BVFUNC_1:def 7;
A4:Pj(a,z)=TRUE or Pj(a,z)=FALSE by MARGREL1:39;
Pj(c,z)=TRUE or Pj(c,z)=FALSE by MARGREL1:39;
then A5:Pj(a,z)=FALSE & Pj(c,z)=FALSE
by A3,A4,BINARITH:19;
(Pj(a,z) 'or' Pj(b,z)) '&' (Pj('not' b,z) 'or' Pj(c,z))
=(Pj(a,z) 'or' Pj(b,z)) '&' Pj('not' b,z) 'or'
Pj(c,z) '&' (Pj(a,z) 'or' Pj(b,z)) by BINARITH:22
.=(Pj(a,z) 'or' Pj(b,z)) '&' Pj('not' b,z) 'or'
((Pj(a,z) '&' Pj(c,z)) 'or' (Pj(c,z) '&' Pj(b,z))) by BINARITH:22
.=(Pj('not' b,z) '&' Pj(a,z) 'or' Pj('not' b,z) '&' Pj(b,z)) 'or'
((Pj(a,z) '&' Pj(c,z)) 'or' (Pj(c,z) '&' Pj(b,z)))
by BINARITH:22
.=(Pj('not' b,z) '&' Pj(a,z) 'or' 'not' Pj(b,z) '&' Pj(b,z)) 'or'
((Pj(a,z) '&' Pj(c,z)) 'or' (Pj(c,z) '&' Pj(b,z))) by VALUAT_1:def 5
.=(Pj('not' b,z) '&' Pj(a,z) 'or' FALSE) 'or'
((Pj(a,z) '&' Pj(c,z)) 'or' (Pj(c,z) '&' Pj(b,z))) by MARGREL1:46
.=(FALSE '&' Pj('not' b,z)) 'or'
((FALSE '&' FALSE) 'or' (FALSE '&' Pj(b,z))) by A5,BINARITH:7
.=FALSE 'or'
((FALSE '&' FALSE) 'or' (FALSE '&' Pj(b,z))) by MARGREL1:49
.=(FALSE '&' FALSE) 'or' (FALSE '&' Pj(b,z)) by BINARITH:7
.=FALSE 'or' (FALSE '&' Pj(b,z)) by MARGREL1:49
.=FALSE '&' Pj(b,z) by BINARITH:7
.=FALSE by MARGREL1:49;
hence contradiction by A1,A2,MARGREL1:43;
end;
hence thesis;
end;
theorem
(a 'imp' b) '&' ('not' a 'imp' c) '<' b 'or' c
proof
let z be Element of Y;
assume A1:Pj((a 'imp' b) '&' ('not' a 'imp' c),z)=TRUE;
A2: Pj((a 'imp' b) '&' ('not' a 'imp' c),z)
=Pj(('not' a 'or' b) '&' ('not' a 'imp' c),z) by BVFUNC_4:8
.=Pj(('not' a 'or' b) '&' ('not' 'not' a 'or' c),z) by BVFUNC_4:8
.=Pj(('not' a 'or' b) '&' (a 'or' c),z) by BVFUNC_1:4
.=Pj('not' a 'or' b,z) '&' Pj(a 'or' c,z) by VALUAT_1:def 6
.=(Pj('not' a,z) 'or' Pj(b,z)) '&' Pj(a 'or' c,z) by BVFUNC_1:def 7
.=(Pj('not'
a,z) 'or' Pj(b,z)) '&' (Pj(a,z) 'or' Pj(c,z)) by BVFUNC_1:def 7;
now assume Pj(b 'or' c,z)<>TRUE;
then Pj(b 'or' c,z)=FALSE by MARGREL1:43;
then A3:Pj(b,z) 'or' Pj(c,z)=FALSE by BVFUNC_1:def 7;
A4:Pj(b,z)=TRUE or Pj(b,z)=FALSE by MARGREL1:39;
Pj(c,z)=TRUE or Pj(c,z)=FALSE by MARGREL1:39;
then Pj(b,z)=FALSE & Pj(c,z)=FALSE
by A3,A4,BINARITH:19;
then (Pj('not' a,z) 'or' Pj(b,z)) '&' (Pj(a,z) 'or' Pj(c,z))
=Pj('not' a,z) '&' (Pj(a,z) 'or' FALSE) by BINARITH:7
.=Pj('not' a,z) '&' Pj(a,z) by BINARITH:7
.='not' Pj(a,z) '&' Pj(a,z) by VALUAT_1:def 5
.=FALSE by MARGREL1:46;
hence contradiction by A1,A2,MARGREL1:43;
end;
hence thesis;
end;
theorem
(a 'imp' c) '&' (b 'imp' 'not' c) '<' 'not' a 'or' 'not' b
proof
let z be Element of Y;
assume A1:Pj((a 'imp' c) '&' (b 'imp' 'not' c),z)=TRUE;
A2: Pj((a 'imp' c) '&' (b 'imp' 'not' c),z)
=Pj(a 'imp' c,z) '&' Pj(b 'imp' 'not' c,z) by VALUAT_1:def 6
.=Pj('not' a 'or' c,z) '&' Pj(b 'imp' 'not' c,z) by BVFUNC_4:8
.=Pj('not' a 'or' c,z) '&' Pj('not' b 'or' 'not' c,z) by BVFUNC_4:8
.=(Pj('not' a,z) 'or' Pj(c,z)) '&' Pj('not' b 'or' 'not' c,z)
by BVFUNC_1:def 7
.=(Pj('not' a,z) 'or' Pj(c,z)) '&' (Pj('not' b,z) 'or' Pj('not' c,z))
by BVFUNC_1:def 7;
now assume Pj('not' a 'or' 'not' b,z)<>TRUE;
then Pj('not' a 'or' 'not' b,z)=FALSE by MARGREL1:43;
then A3:Pj('not' a,z) 'or' Pj('not' b,z)=FALSE by BVFUNC_1:def 7;
A4:Pj('not' a,z)=TRUE or Pj('not' a,z)=FALSE by MARGREL1:39;
Pj('not' b,z)=TRUE or Pj('not' b,z)=FALSE by MARGREL1:39;
then Pj('not' a,z)=FALSE & Pj('not' b,z)=FALSE
by A3,A4,BINARITH:19;
then (Pj('not' a,z) 'or' Pj(c,z)) '&' (Pj('not' b,z) 'or' Pj('not' c,z))
=Pj(c,z) '&' (FALSE 'or' Pj('not' c,z)) by BINARITH:7
.=Pj(c,z) '&' Pj('not' c,z) by BINARITH:7
.=Pj(c,z) '&' 'not' Pj(c,z) by VALUAT_1:def 5
.=FALSE by MARGREL1:46;
hence contradiction by A1,A2,MARGREL1:43;
end;
hence thesis;
end;
theorem
(a 'or' b) '&' ('not' a 'or' c) '<' b 'or' c
proof
let z be Element of Y;
assume A1:Pj((a 'or' b) '&' ('not' a 'or' c),z)=TRUE;
A2: Pj((a 'or' b) '&' ('not' a 'or' c),z)
=Pj(a 'or' b,z) '&' Pj('not' a 'or' c,z) by VALUAT_1:def 6
.=(Pj(a,z) 'or' Pj(b,z)) '&' Pj('not' a 'or' c,z) by BVFUNC_1:def 7
.=(Pj(a,z) 'or' Pj(b,z)) '&' (Pj('not' a,z) 'or' Pj(c,z))
by BVFUNC_1:def 7;
now assume Pj(b 'or' c,z)<>TRUE;
then Pj(b 'or' c,z)=FALSE by MARGREL1:43;
then A3:Pj(b,z) 'or' Pj(c,z)=FALSE by BVFUNC_1:def 7;
A4:Pj(b,z)=TRUE or Pj(b,z)=FALSE by MARGREL1:39;
Pj(c,z)=TRUE or Pj(c,z)=FALSE by MARGREL1:39;
then Pj(b,z)=FALSE & Pj(c,z)=FALSE
by A3,A4,BINARITH:19;
then (Pj(a,z) 'or' Pj(b,z)) '&' (Pj('not' a,z) 'or' Pj(c,z))
=Pj(a,z) '&' (Pj('not' a,z) 'or' FALSE) by BINARITH:7
.=Pj(a,z) '&' Pj('not' a,z) by BINARITH:7
.=Pj(a,z) '&' 'not' Pj(a,z) by VALUAT_1:def 5
.=FALSE by MARGREL1:46;
hence contradiction by A1,A2,MARGREL1:43;
end;
hence thesis;
end;
theorem Th19:
(a 'imp' b) '&' (c 'imp' d) '<' (a '&' c) 'imp' (b '&' d)
proof
let z be Element of Y;
assume A1:Pj((a 'imp' b) '&' (c 'imp' d),z)=TRUE;
A2: Pj((a 'imp' b) '&' (c 'imp' d),z)
=Pj(a 'imp' b,z) '&' Pj(c 'imp' d,z) by VALUAT_1:def 6
.=Pj('not' a 'or' b,z) '&' Pj(c 'imp' d,z) by BVFUNC_4:8
.=Pj('not' a 'or' b,z) '&' Pj('not' c 'or' d,z) by BVFUNC_4:8
.=(Pj('not' a,z) 'or' Pj(b,z)) '&' Pj('not' c 'or' d,z) by BVFUNC_1:def 7
.=(Pj('not' a,z) 'or' Pj(b,z)) '&' (Pj('not' c,z) 'or' Pj(d,z))
by BVFUNC_1:def 7;
now assume A3: Pj((a '&' c) 'imp' (b '&' d),z)<>TRUE;
A4: Pj((a '&' c) 'imp' (b '&' d),z)
=Pj('not'( a '&' c) 'or' (b '&' d),z) by BVFUNC_4:8
.=Pj('not'( a '&' c),z) 'or' Pj(b '&' d,z) by BVFUNC_1:def 7
.=Pj('not' a 'or' 'not' c,z) 'or' Pj(b '&' d,z) by BVFUNC_1:17
.=(Pj('not' a,z) 'or' Pj('not' c,z)) 'or' Pj(b '&' d,z) by BVFUNC_1:def 7
.=(Pj('not' a,z) 'or' Pj('not' c,z)) 'or' (Pj(b,z) '&' Pj(d,z))
by VALUAT_1:def 6;
A5:(Pj('not' a,z) 'or' Pj('not' c,z))=TRUE or
(Pj('not' a,z) 'or' Pj('not' c,z))=FALSE by MARGREL1:39;
A6: (Pj(b,z) '&' Pj(d,z))=TRUE or (Pj(b,z) '&' Pj(d,z))=FALSE
by MARGREL1:39;
A7:Pj('not' a,z)=TRUE or Pj('not' a,z)=FALSE by MARGREL1:39;
Pj('not' c,z)=TRUE or Pj('not' c,z)=FALSE by MARGREL1:39;
then A8: Pj('not' a,z)=FALSE & Pj('not' c,z)=FALSE by A3,A4,A5,A7,BINARITH:19;
now per cases by A3,A4,A6,BINARITH:19,MARGREL1:45;
case Pj(b,z)=FALSE;
then (Pj('not' a,z) 'or' Pj(b,z)) '&' (Pj('not' c,z) 'or' Pj(d,z))
=FALSE '&' (FALSE 'or' Pj(d,z)) by A8,BINARITH:7
.=FALSE by MARGREL1:49; hence thesis by A1,A2,MARGREL1:43;
case Pj(d,z)=FALSE;
then (Pj('not' a,z) 'or' Pj(b,z)) '&' (Pj('not' c,z) 'or' Pj(d,z))
=Pj(b,z) '&' (FALSE 'or' FALSE) by A8,BINARITH:7
.=FALSE '&' Pj(b,z) by BINARITH:7
.=FALSE by MARGREL1:49;
hence thesis by A1,A2,MARGREL1:43;
end;
hence thesis;
end;
hence thesis;
end;
theorem
(a 'imp' b) '&' (a 'imp' c) '<' a 'imp' (b '&' c)
proof
(a 'imp' b) '&' (a 'imp' c) '<' (a '&' a) 'imp' (b '&' c) by Th19;
hence thesis by BVFUNC_1:6;
end;
theorem Th21:
((a 'imp' c) '&' (b 'imp' c)) '<' (a 'or' b) 'imp' c
proof
((a 'imp' c) '&' (b 'imp' c)) 'imp' ((a 'or' b) 'imp' c) = I_el Y
by BVFUNC_6:9;
hence thesis by BVFUNC_1:19;
end;
theorem Th22:
(a 'imp' b) '&' (c 'imp' d) '<' (a 'or' c) 'imp' (b 'or' d)
proof
let z be Element of Y;
assume A1:Pj((a 'imp' b) '&' (c 'imp' d),z)=TRUE;
A2: Pj((a 'imp' b) '&' (c 'imp' d),z)
=Pj(('not' a 'or' b) '&' (c 'imp' d),z) by BVFUNC_4:8
.=Pj(('not' a 'or' b) '&' ('not' c 'or' d),z) by BVFUNC_4:8
.=Pj('not' a 'or' b,z) '&' Pj('not' c 'or' d,z) by VALUAT_1:def 6
.=(Pj('not' a,z) 'or' Pj(b,z)) '&' Pj('not' c 'or' d,z) by BVFUNC_1:def 7
.=(Pj('not' a,z) 'or' Pj(b,z)) '&' (Pj('not'
c,z) 'or' Pj(d,z)) by BVFUNC_1:def 7;
now assume A3: Pj((a 'or' c) 'imp' (b 'or' d),z)<>TRUE;
A4: Pj((a 'or' c) 'imp' (b 'or' d),z)
=Pj('not'( a 'or' c) 'or' (b 'or' d),z) by BVFUNC_4:8
.=Pj(('not' a '&' 'not' c) 'or' (b 'or' d),z) by BVFUNC_1:16
.=Pj('not' a '&' 'not' c,z) 'or' Pj(b 'or' d,z) by BVFUNC_1:def 7
.=(Pj('not' a,z) '&' Pj('not' c,z)) 'or' Pj(b 'or' d,z) by VALUAT_1:def 6
.=(Pj('not' a,z) '&' Pj('not' c,z)) 'or' (Pj(b,z) 'or' Pj(d,z))
by BVFUNC_1:def 7;
A5:(Pj('not' a,z) '&' Pj('not' c,z))=TRUE or
(Pj('not' a,z) '&' Pj('not' c,z))=FALSE by MARGREL1:39;
A6: (Pj(b,z) 'or' Pj(d,z))=TRUE or (Pj(b,z) 'or' Pj(d,z))=FALSE
by MARGREL1:39;
A7:Pj(b,z)=TRUE or Pj(b,z)=FALSE by MARGREL1:39;
Pj(d,z)=TRUE or Pj(d,z)=FALSE by MARGREL1:39;
then A8: Pj(b,z)=FALSE & Pj(d,z)=FALSE by A3,A4,A6,A7,BINARITH:19;
now per cases by A3,A4,A5,BINARITH:19,MARGREL1:45;
case Pj('not' a,z)=FALSE;
then (Pj('not' a,z) 'or' Pj(b,z)) '&' (Pj('not' c,z) 'or' Pj(d,z))
=FALSE '&' (Pj('not' c,z) 'or' FALSE) by A8,BINARITH:7
.=FALSE by MARGREL1:45; hence thesis by A1,A2,MARGREL1:43;
case Pj('not' c,z)=FALSE;
then (Pj('not' a,z) 'or' Pj(b,z)) '&' (Pj('not' c,z) 'or' Pj(d,z))
=FALSE '&' (Pj('not' a,z) 'or' FALSE) by A8,BINARITH:7
.=FALSE by MARGREL1:49; hence thesis by A1,A2,MARGREL1:43;
end;
hence thesis;
end;
hence thesis;
end;
theorem
(a 'imp' b) '&' (a 'imp' c) '<' a 'imp' (b 'or' c)
proof
(a 'imp' b) '&' (a 'imp' c) '<' (a 'or' a) 'imp' (b 'or' c) by Th22;
hence thesis by BVFUNC_1:10;
end;
theorem Th24: 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
let a1,b1,c1,a2,b2,c2 be Element of Funcs(Y,BOOLEAN);
(b1 'imp' b2) '&' (c1 'imp' c2) '&' (a1 'or' b1 'or' c1) '&'
'not'( a2 '&' b2) '&' 'not'( a2 '&' c2) '<' (b1 'imp' b2) by Lm4;
then A1:(b1 'imp' b2) '&' (c1 'imp' c2) '&' (a1 'or' b1 'or' c1) '&'
'not'( a2 '&' b2) '&' 'not'( a2 '&' c2)
'imp' (b1 'imp' b2) = I_el(Y) by BVFUNC_1:19;
(b1 'imp' b2) '&' (c1 'imp' c2) '&' (a1 'or' b1 'or' c1) '&'
'not'( a2 '&' b2) '&' 'not'( a2 '&' c2) '<' (c1 'imp' c2) by Lm4;
then (b1 'imp' b2) '&' (c1 'imp' c2) '&' (a1 'or' b1 'or' c1) '&'
'not'( a2 '&' b2) '&' 'not'( a2 '&' c2)
'imp' (c1 'imp' c2) = I_el(Y) by BVFUNC_1:19;
then A2:(b1 'imp' b2) '&' (c1 'imp' c2) '&' (a1 'or' b1 'or' c1) '&'
'not'( a2 '&' b2) '&' 'not'( a2 '&' c2) 'imp'
(b1 'imp' b2) '&' (c1 'imp' c2) = I_el(Y) by A1,BVFUNC_6:18;
(b1 'imp' b2) '&' (c1 'imp' c2) '<' (b1 'or' c1) 'imp' (b2 'or' c2)
by Th22;
then ((b1 'imp' b2) '&' (c1 'imp' c2)) 'imp' ((b1 'or' c1) 'imp' (b2 'or' c2
))
= I_el(Y) by BVFUNC_1:19;
then A3:(b1 'imp' b2) '&' (c1 'imp' c2) '&' (a1 'or' b1 'or' c1) '&'
'not'( a2 '&' b2) '&' 'not'( a2 '&' c2)
'imp' ((b1 'or' c1) 'imp' (b2 'or' c2)) = I_el(Y) by A2,BVFUNC_5:10;
(b1 'imp' b2) '&' (c1 'imp' c2) '&'
(a1 'or' b1 'or' c1) '&' 'not'( a2 '&' b2) '&' 'not'( a2 '&' c2)
'<' 'not'( a2 '&' b2) by Lm2;
then A4:(b1 'imp' b2) '&' (c1 'imp' c2) '&'
(a1 'or' b1 'or' c1) '&' 'not'( a2 '&' b2) '&' 'not'( a2 '&' c2)
'imp' 'not'( a2 '&' b2) = I_el(Y) by BVFUNC_1:19;
(b1 'imp' b2) '&' (c1 'imp' c2) '&'
(a1 'or' b1 'or' c1) '&' 'not'( a2 '&' b2) '&' 'not'( a2 '&' c2)
'<' 'not'( a2 '&' c2) by Lm1;
then (b1 'imp' b2) '&' (c1 'imp' c2) '&' (a1 'or' b1 'or' c1) '&'
'not'( a2 '&' b2) '&' 'not'( a2 '&' c2)
'imp' 'not'( a2 '&' c2) = I_el(Y) by BVFUNC_1:19;
then (b1 'imp' b2) '&' (c1 'imp' c2) '&' (a1 'or' b1 'or' c1) '&'
'not'( a2 '&' b2) '&' 'not'( a2 '&' c2)
'imp' ('not'( a2 '&' b2) '&' 'not'( a2 '&' c2)) = I_el(Y) by A4,BVFUNC_6:18;
then A5:(b1 'imp' b2) '&' (c1 'imp' c2) '&'
(a1 'or' b1 'or' c1) '&' 'not'( a2 '&' b2) '&' 'not'( a2 '&' c2)
'imp' ((b1 'or' c1) 'imp' (b2 'or' c2)) '&' ('not'( a2 '&' b2) '&' 'not'
(a2 '&' c2)) = I_el(Y) by A3,BVFUNC_6:18;
'not'( a2 '&' b2) '&' 'not'( a2 '&' c2)
=('not' a2 'or' 'not' b2) '&' 'not'( a2 '&' c2) by BVFUNC_1:17
.=('not' b2 'or' 'not' a2) '&' ('not' c2 'or' 'not' a2) by BVFUNC_1:17
.=(b2 'imp' 'not' a2) '&' ('not' c2 'or' 'not' a2) by BVFUNC_4:8
.=(b2 'imp' 'not' a2) '&' (c2 'imp' 'not' a2) by BVFUNC_4:8
.=(b2 'or' c2) 'imp' 'not' a2 by BVFUNC_7:5;
then A6:(b1 'imp' b2) '&' (c1 'imp' c2) '&' (a1 'or' b1 'or' c1) '&'
'not'( a2 '&' b2) '&' 'not'( a2 '&' c2)
'imp' ((b1 'or' c1) 'imp' (b2 'or' c2)) '&' ((b2 'or' c2) 'imp' 'not' a2) '&'
((b1 'or' c1) 'imp' 'not' a2) = I_el(Y) by A5,BVFUNC_7:12;
((b1 'or' c1) 'imp' (b2 'or' c2)) '&' ((b2 'or' c2) 'imp' 'not' a2) '&'
((b1 'or' c1) 'imp' 'not' a2) 'imp'
((b1 'or' c1) 'imp' 'not' a2) = I_el(Y) by BVFUNC_6:39;
then A7:(b1 'imp' b2) '&' (c1 'imp' c2) '&' (a1 'or' b1 'or' c1) '&'
'not'( a2 '&' b2) '&' 'not'( a2 '&' c2)
'imp' ((b1 'or' c1) 'imp' 'not' a2) = I_el(Y) by A6,BVFUNC_5:10;
(b1 'imp' b2) '&' (c1 'imp' c2) '&' (a1 'or' b1 'or' c1) '&'
'not'( a2 '&' b2) '&' 'not'( a2 '&' c2)
'<' (a1 'or' b1 'or' c1) by Lm3;
then (b1 'imp' b2) '&' (c1 'imp' c2) '&' (a1 'or' b1 'or' c1) '&'
'not'( a2 '&' b2) '&' 'not'( a2 '&' c2)
'imp' (a1 'or' b1 'or' c1) = I_el(Y) by BVFUNC_1:19;
then A8:(b1 'imp' b2) '&' (c1 'imp' c2) '&' (a1 'or' b1 'or' c1) '&'
'not'( a2 '&' b2) '&' 'not'( a2 '&' c2)
'imp' (a1 'or' b1 'or' c1) '&' ((b1 'or' c1) 'imp' 'not' a2) = I_el(Y)
by A7,BVFUNC_6:18;
A9:(a1 'or' b1 'or' c1) '&' ((b1 'or' c1) 'imp' 'not' a2)
=(a1 'or' (b1 'or' c1)) '&' ((b1 'or' c1) 'imp' 'not' a2) by BVFUNC_1:11;
(a1 'or' (b1 'or' c1)) '&' ((b1 'or' c1) 'imp' 'not' a2) '<'
(a1 'or' 'not' a2) by Th1;
then (a1 'or' b1 'or' c1) '&' ((b1 'or' c1) 'imp' 'not' a2) 'imp' (a1 'or'
'not'
a2)
=I_el(Y) by A9,BVFUNC_1:19;
then (b1 'imp' b2) '&' (c1 'imp' c2) '&' (a1 'or' b1 'or' c1) '&'
'not'( a2 '&' b2) '&' 'not'( a2 '&' c2)
'imp' (a1 'or' 'not' a2) = I_el(Y) by A8,BVFUNC_5:10;
then (b1 'imp' b2) '&' (c1 'imp' c2) '&' (a1 'or' b1 'or' c1) '&'
'not'( a2 '&' b2) '&' 'not'( a2 '&' c2)
'imp' (a2 'imp' a1) = I_el(Y) by BVFUNC_4:8;
hence thesis by BVFUNC_1:19;
end;
Lm8: 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
let a1,b1,c1,a2,b2,c2 be Element of Funcs(Y,BOOLEAN);
A1:((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) = I_el(Y) by Lm7;
A2:((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)
= I_el(Y) by Lm7;
A3:((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 'or' b1 'or' c1) = I_el(Y) by Lm7;
A4:((a1 'imp' a2) '&' (b1 'imp' b2) '&' (c1 'imp' c2) '&'
(a1 'or' b1 'or' c1) '&'
'not'( a2 '&' b2) '&' 'not'( a2 '&' c2) '&' 'not'( b2 '&' c2))
'imp' 'not'( a2 '&' c2)
= I_el(Y) by Lm7;
A5:((a1 'imp' a2) '&' (b1 'imp' b2) '&' (c1 'imp' c2) '&'
(a1 'or' b1 'or' c1) '&'
'not'( a2 '&' b2) '&' 'not'( a2 '&' c2) '&' 'not'( b2 '&' c2))
'imp' 'not'( b2 '&' c2)
= I_el(Y) by Lm7;
((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)
= I_el(Y) by A1,A2,BVFUNC_6:18;
then ((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)
= I_el(Y) by A3,BVFUNC_6:18;
then ((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'( a2 '&' c2)
= I_el(Y) by A4,BVFUNC_6:18; hence thesis by A5,BVFUNC_6:18;
end;
Lm9: 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
let a1,b1,c1,a2,b2,c2 be Element of Funcs(Y,BOOLEAN);
A1:((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)
= I_el(Y) by Lm7;
A2:((a1 'imp' a2) '&' (b1 'imp' b2) '&' (c1 'imp' c2) '&'
(a1 'or' b1 'or' c1) '&'
'not'( a2 '&' b2) '&' 'not'( a2 '&' c2) '&' 'not'( b2 '&' c2))
'imp' (c1 'imp' c2)
= I_el(Y) by Lm7;
A3:((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 'or' b1 'or' c1)
= I_el(Y) by Lm7;
A4:((a1 'imp' a2) '&' (b1 'imp' b2) '&' (c1 'imp' c2) '&'
(a1 'or' b1 'or' c1) '&'
'not'( a2 '&' b2) '&' 'not'( a2 '&' c2) '&' 'not'( b2 '&' c2))
'imp' 'not'( a2 '&' b2)
= I_el(Y) by Lm7;
A5:((a1 'imp' a2) '&' (b1 'imp' b2) '&' (c1 'imp' c2) '&'
(a1 'or' b1 'or' c1) '&'
'not'( a2 '&' b2) '&' 'not'( a2 '&' c2) '&' 'not'( b2 '&' c2))
'imp' 'not'( b2 '&' c2)
= I_el(Y) by Lm7;
((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)
= I_el(Y) by A1,A2,BVFUNC_6:18;
then ((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)
= I_el(Y) by A3,BVFUNC_6:18;
then ((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'( a2 '&' b2)
= I_el(Y) by A4,BVFUNC_6:18; hence thesis by A5,BVFUNC_6:18;
end;
Lm10: 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
let a1,b1,c1,a2,b2,c2 be Element of Funcs(Y,BOOLEAN);
A1:((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) = I_el(Y) by Lm7;
A2:((a1 'imp' a2) '&' (b1 'imp' b2) '&' (c1 'imp' c2) '&'
(a1 'or' b1 'or' c1) '&'
'not'( a2 '&' b2) '&' 'not'( a2 '&' c2) '&' 'not'( b2 '&' c2))
'imp' (c1 'imp' c2) = I_el(Y) by Lm7;
A3:((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 'or' b1 'or' c1) = I_el(Y) by Lm7;
A4:((a1 'imp' a2) '&' (b1 'imp' b2) '&' (c1 'imp' c2) '&'
(a1 'or' b1 'or' c1) '&'
'not'( a2 '&' b2) '&' 'not'( a2 '&' c2) '&' 'not'( b2 '&' c2))
'imp' 'not'( a2 '&' b2) = I_el(Y) by Lm7;
A5:((a1 'imp' a2) '&' (b1 'imp' b2) '&' (c1 'imp' c2) '&'
(a1 'or' b1 'or' c1) '&'
'not'( a2 '&' b2) '&' 'not'( a2 '&' c2) '&' 'not'( b2 '&' c2))
'imp' 'not'( a2 '&' c2) = I_el(Y) by Lm7;
((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)
= I_el(Y) by A1,A2,BVFUNC_6:18;
then ((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)
= I_el(Y) by A3,BVFUNC_6:18;
then ((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)
= I_el(Y) by A4,BVFUNC_6:18; hence thesis by A5,BVFUNC_6:18;
end;
theorem 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
let a1,b1,c1,a2,b2,c2 be Element of Funcs(Y,BOOLEAN);
A1:((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) by Lm8;
A2:((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) by Lm9;
A3:((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) by Lm10;
((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)) '&'
((a1 'imp' a2) '&' (c1 'imp' c2) '&'
(a1 'or' b1 'or' c1) '&'
'not'( b2 '&' a2) '&' 'not'( b2 '&' c2))
=I_el(Y) by A1,A2,BVFUNC_6:18;
then A4:((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)) '&'
((a1 'imp' a2) '&' (c1 'imp' c2) '&' (a1 'or' b1 'or' c1) '&'
'not'( a2 '&' b2) '&' 'not'( b2 '&' c2)) '&'
((b1 'imp' b2) '&' (c1 'imp' c2) '&' (a1 'or' b1 'or' c1) '&'
'not'( a2 '&' b2) '&' 'not'( a2 '&' c2))
=I_el(Y) by A3,BVFUNC_6:18;
((a1 'imp' a2) '&' (b1 'imp' b2) '&' (a1 'or' b1 'or' c1) '&'
'not'( c2 '&' a2) '&' 'not'( c2 '&' b2)) '&'
((a1 'imp' a2) '&' (c1 'imp' c2) '&' (a1 'or' b1 'or' c1) '&'
'not'( a2 '&' b2) '&' 'not'( b2 '&' c2)) '&'
((b1 'imp' b2) '&' (c1 'imp' c2) '&' (a1 'or' b1 'or' c1) '&'
'not'( a2 '&' b2) '&' 'not'( a2 '&' c2)) '<'
((a1 'imp' a2) '&' (b1 'imp' b2) '&' (a1 'or' b1 'or' c1) '&'
'not'( c2 '&' a2) '&' 'not'( c2 '&' b2)) by Lm2;
then A5:((a1 'imp' a2) '&' (b1 'imp' b2) '&' (a1 'or' b1 'or' c1) '&'
'not'( c2 '&' a2) '&' 'not'( c2 '&' b2)) '&'
((a1 'imp' a2) '&' (c1 'imp' c2) '&' (a1 'or' b1 'or' c1) '&'
'not'( a2 '&' b2) '&' 'not'( b2 '&' c2)) '&'
((b1 'imp' b2) '&' (c1 'imp' c2) '&' (a1 'or' b1 'or' c1) '&'
'not'( a2 '&' b2) '&' 'not'( a2 '&' c2)) 'imp'
((a1 'imp' a2) '&' (b1 'imp' b2) '&' (a1 'or' b1 'or' c1) '&'
'not'( c2 '&' a2) '&' 'not'( c2 '&' b2)) =I_el(Y) by BVFUNC_1:19;
((a1 'imp' a2) '&' (b1 'imp' b2) '&' (a1 'or' b1 'or' c1) '&'
'not'( c2 '&' a2) '&' 'not'( c2 '&' b2)) '&'
((a1 'imp' a2) '&' (c1 'imp' c2) '&' (a1 'or' b1 'or' c1) '&'
'not'( a2 '&' b2) '&' 'not'( b2 '&' c2)) '&'
((b1 'imp' b2) '&' (c1 'imp' c2) '&' (a1 'or' b1 'or' c1) '&'
'not'( a2 '&' b2) '&' 'not'( a2 '&' c2)) '<'
((a1 'imp' a2) '&' (c1 'imp' c2) '&' (a1 'or' b1 'or' c1) '&'
'not'( a2 '&' b2) '&' 'not'( b2 '&' c2)) by Lm2;
then A6:((a1 'imp' a2) '&' (b1 'imp' b2) '&' (a1 'or' b1 'or' c1) '&'
'not'( c2 '&' a2) '&' 'not'( c2 '&' b2)) '&'
((a1 'imp' a2) '&' (c1 'imp' c2) '&' (a1 'or' b1 'or' c1) '&'
'not'( a2 '&' b2) '&' 'not'( b2 '&' c2)) '&'
((b1 'imp' b2) '&' (c1 'imp' c2) '&' (a1 'or' b1 'or' c1) '&'
'not'( a2 '&' b2) '&' 'not'( a2 '&' c2)) 'imp'
((a1 'imp' a2) '&' (c1 'imp' c2) '&' (a1 'or' b1 'or' c1) '&'
'not'( a2 '&' b2) '&' 'not'( b2 '&' c2)) =I_el(Y) by BVFUNC_1:19;
A7:((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) by A4,A5,BVFUNC_5:10;
A8:((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'( a2 '&' b2) '&' 'not'( b2 '&' c2)) =I_el(Y) by A4,A6,BVFUNC_5:10;
(a1 'imp' a2) '&' (b1 'imp' b2) '&' (a1 'or' c1 'or' b1) '&'
'not'( c2 '&' a2) '&' 'not'( c2 '&' b2) '<' (c2 'imp' c1) by Th24;
then A9:(a1 'imp' a2) '&' (b1 'imp' b2) '&' (a1 'or' b1 'or' c1) '&'
'not'( c2 '&' a2) '&' 'not'( c2 '&' b2) '<' (c2 'imp' c1) by BVFUNC_1:11;
A10:(a1 'imp' a2) '&' (c1 'imp' c2) '&'
(a1 'or' b1 'or' c1) '&' 'not'( a2 '&' b2) '&' 'not'( b2 '&' c2) '<'
(b2 'imp' b1) by Th24;
A11:(b1 'imp' b2) '&' (c1 'imp' c2) '&' (a1 'or' b1 'or' c1) '&'
'not'( a2 '&' b2) '&' 'not'( a2 '&' c2) '<' (a2 'imp' a1) by Th24;
A12:(a1 'imp' a2) '&' (b1 'imp' b2) '&' (a1 'or' b1 'or' c1) '&'
'not'( c2 '&' a2) '&' 'not'( c2 '&' b2) 'imp' (c2 'imp' c1) = I_el(Y)
by A9,BVFUNC_1:19;
A13:(a1 'imp' a2) '&' (c1 'imp' c2) '&' (a1 'or' b1 'or' c1) '&'
'not'( a2 '&' b2) '&' 'not'( b2 '&' c2) 'imp'
(b2 'imp' b1) = I_el(Y) by A10,BVFUNC_1:19;
A14:(b1 'imp' b2) '&' (c1 'imp' c2) '&' (a1 'or' b1 'or' c1) '&'
'not'( a2 '&' b2) '&' 'not'( a2 '&' c2) 'imp' (a2 'imp' a1) = I_el(Y)
by A11,BVFUNC_1:19;
A15:(a1 'imp' a2) '&' (b1 'imp' b2) '&' (c1 'imp' c2) '&'
(a1 'or' b1 'or' c1) '&'
'not'( a2 '&' b2) '&' 'not'( a2 '&' c2) '&' 'not'( b2 '&' c2) 'imp'
(c2 'imp' c1) = I_el(Y) by A7,A12,BVFUNC_5:10;
A16:(a1 'imp' a2) '&' (b1 'imp' b2) '&' (c1 'imp' c2) '&'
(a1 'or' b1 'or' c1) '&'
'not'( a2 '&' b2) '&' 'not'( a2 '&' c2) '&' 'not'( b2 '&' c2) 'imp'
(b2 'imp' b1) = I_el(Y) by A8,A13,BVFUNC_5:10;
(a1 'imp' a2) '&' (b1 'imp' b2) '&' (c1 'imp' c2) '&'
(a1 'or' b1 'or' c1) '&'
'not'( a2 '&' b2) '&' 'not'( a2 '&' c2) '&' 'not' (b2 '&' c2) 'imp'
(a2 'imp' a1) = I_el(Y) by A3,A14,BVFUNC_5:10;
then ((a1 'imp' a2) '&' (b1 'imp' b2) '&' (c1 'imp' c2) '&'
(a1 'or' b1 'or' c1) '&'
'not'( a2 '&' b2) '&' 'not'( a2 '&' c2) '&' 'not'( b2 '&' c2)) 'imp'
(a2 'imp' a1) '&' (b2 'imp' b1) = I_el(Y) by A16,BVFUNC_6:18;
then ((a1 'imp' a2) '&' (b1 'imp' b2) '&' (c1 'imp' c2) '&'
(a1 'or' b1 'or' c1) '&'
'not'( a2 '&' b2) '&' 'not'( a2 '&' c2) '&' 'not'( b2 '&' c2)) 'imp'
(a2 'imp' a1) '&' (b2 'imp' b1) '&' (c2 'imp' c1) = I_el(Y)
by A15,BVFUNC_6:18;
hence thesis by BVFUNC_1:19;
end;
theorem Th26: 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
let a1,b1,a2,b2 be Element of Funcs(Y,BOOLEAN);
for z being Element of Y
st Pj((a1 'imp' a2) '&' (b1 'imp' b2) '&' 'not'( a2 '&' b2),z)=TRUE
holds Pj('not'( a1 '&' b1),z)=TRUE
proof
let z be Element of Y;
assume A1:
Pj((a1 'imp' a2) '&' (b1 'imp' b2) '&' 'not'( a2 '&' b2),z)=TRUE;
A2:Pj((a1 'imp' a2) '&' (b1 'imp' b2) '&' 'not'( a2 '&' b2),z)
=Pj((a1 'imp' a2) '&' (b1 'imp' b2),z) '&' Pj('not'( a2 '&' b2),z)
by VALUAT_1:def 6
.=(Pj(a1 'imp' a2,z) '&' Pj(b1 'imp' b2,z)) '&' Pj('not'( a2 '&' b2),z)
by VALUAT_1:def 6
.=(Pj('not' a1 'or' a2,z) '&' Pj(b1 'imp' b2,z)) '&' Pj('not'( a2 '&' b2),z)
by BVFUNC_4:8
.=(Pj('not' a1 'or' a2,z) '&' Pj('not' b1 'or' b2,z)) '&' Pj('not'
(a2 '&' b2),z) by BVFUNC_4:8
.=((Pj('not' a1,z) 'or' Pj(a2,z)) '&' Pj('not' b1 'or' b2,z)) '&'
Pj('not'( a2 '&' b2),z) by BVFUNC_1:def 7
.=((Pj('not' a1,z) 'or' Pj(a2,z)) '&' (Pj('not' b1,z) 'or' Pj(b2,z))) '&'
Pj('not'( a2 '&' b2),z) by BVFUNC_1:def 7
.=((Pj('not' a1,z) 'or' Pj(a2,z)) '&' (Pj('not' b1,z) 'or' Pj(b2,z))) '&'
(Pj('not' a2 'or' 'not' b2,z)) by BVFUNC_1:17
.=((Pj('not' a1,z) 'or' Pj(a2,z)) '&' (Pj('not' b1,z) 'or' Pj(b2,z))) '&'
(Pj('not' a2,z) 'or' Pj('not' b2,z))
by BVFUNC_1:def 7;
now assume A3: Pj('not'( a1 '&' b1),z)<>TRUE;
A4: Pj('not'( a1 '&' b1),z)
=Pj('not' a1 'or' 'not' b1,z) by BVFUNC_1:17
.=Pj('not' a1,z) 'or' Pj('not' b1,z) by BVFUNC_1:def 7;
A5:Pj('not' a1,z)=TRUE or Pj('not' a1,z)=FALSE by MARGREL1:39;
Pj('not' b1,z)=TRUE or Pj('not' b1,z)=FALSE by MARGREL1:39;
then Pj((a1 'imp' a2) '&' (b1 'imp' b2) '&' 'not'( a2 '&' b2),z)
=(Pj(a2,z) '&' (FALSE 'or' Pj(b2,z))) '&'
(Pj('not' a2,z) 'or' Pj('not' b2,z)) by A2,A3,A4,A5,BINARITH:7,19
.=(Pj(a2,z) '&' Pj(b2,z)) '&'
(Pj('not' a2,z) 'or' Pj('not' b2,z)) by BINARITH:7
.=(Pj(b2,z) '&' Pj(a2,z)) '&' Pj('not' a2,z) 'or'
(Pj(a2,z) '&' Pj(b2,z)) '&' Pj('not' b2,z) by BINARITH:22
.=Pj(b2,z) '&' (Pj(a2,z) '&' Pj('not' a2,z)) 'or'
(Pj(a2,z) '&' Pj(b2,z)) '&' Pj('not' b2,z) by MARGREL1:52
.=Pj(b2,z) '&' (Pj(a2,z) '&' Pj('not' a2,z)) 'or'
Pj(a2,z) '&' (Pj(b2,z) '&' Pj('not' b2,z)) by MARGREL1:52
.=Pj(b2,z) '&' (Pj(a2,z) '&' 'not' Pj(a2,z)) 'or'
Pj(a2,z) '&' (Pj(b2,z) '&' Pj('not' b2,z)) by VALUAT_1:def 5
.=Pj(b2,z) '&' (Pj(a2,z) '&' 'not' Pj(a2,z)) 'or'
Pj(a2,z) '&' (Pj(b2,z) '&' 'not' Pj(b2,z)) by VALUAT_1:def 5
.=Pj(b2,z) '&' FALSE 'or'
Pj(a2,z) '&' (Pj(b2,z) '&' 'not' Pj(b2,z)) by MARGREL1:46
.=FALSE '&' Pj(b2,z) 'or' Pj(a2,z) '&' FALSE by MARGREL1:46
.=FALSE 'or' FALSE '&' Pj(a2,z) by MARGREL1:49
.=FALSE 'or' FALSE by MARGREL1:49
.=FALSE by BINARITH:7;
hence contradiction by A1,MARGREL1:43;
end;
hence thesis;
end;
then (a1 'imp' a2) '&' (b1 'imp' b2) '&' 'not'( a2 '&' b2) '<'
'not'( a1 '&' b1) by BVFUNC_1:def 15;
hence thesis by BVFUNC_1:19;
end;
theorem
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
let a1,b1,c1,a2,b2,c2 be Element of Funcs(Y,BOOLEAN);
A1:(a1 'imp' a2) '&' (b1 'imp' b2) '&' (c1 'imp' c2) '&'
'not'( a2 '&' b2) '&' 'not'( a2 '&' c2) '&' 'not'( b2 '&' c2)
=(a1 'imp' a2) '&' (a1 'imp' a2) '&' (b1 'imp' b2) '&' (c1 'imp' c2) '&'
'not'( a2 '&' b2) '&' 'not'( a2 '&' c2) '&' 'not'( b2 '&' c2)
by BVFUNC_1:6
.=(a1 'imp' a2) '&' (a1 'imp' a2) '&' ((b1 'imp' b2) '&' (b1 'imp' b2))
'&' (c1 'imp' c2) '&'
'not'( a2 '&' b2) '&' 'not'( a2 '&' c2) '&' 'not'( b2 '&' c2)
by BVFUNC_1:6
.=((a1 'imp' a2) '&' (a1 'imp' a2) '&' ((b1 'imp' b2) '&' (b1 'imp' b2))
'&' ((c1 'imp' c2) '&' (c1 'imp' c2))) '&'
'not'( a2 '&' b2) '&' 'not'( a2 '&' c2) '&' 'not'( b2 '&' c2)
by BVFUNC_1:6
.=(((a1 'imp' a2) '&' (a1 'imp' a2) '&' (b1 'imp' b2)) '&' (b1 'imp' b2)
'&' ((c1 'imp' c2) '&' (c1 'imp' c2))) '&'
'not'( a2 '&' b2) '&' 'not'( a2 '&' c2) '&' 'not'( b2 '&' c2)
by BVFUNC_1:7
.=((((a1 'imp' a2) '&' (b1 'imp' b2)) '&' (a1 'imp' a2)) '&' (b1 'imp' b2)
'&' ((c1 'imp' c2) '&' (c1 'imp' c2))) '&'
'not'( a2 '&' b2) '&' 'not'( a2 '&' c2) '&' 'not'( b2 '&' c2)
by BVFUNC_1:7
.=(((a1 'imp' a2) '&' (b1 'imp' b2)) '&' (a1 'imp' a2) '&' (b1 'imp' b2)
'&' (c1 'imp' c2) '&' (c1 'imp' c2)) '&'
'not'( a2 '&' b2) '&' 'not'( a2 '&' c2) '&' 'not'( b2 '&' c2)
by BVFUNC_1:7
.=(((a1 'imp' a2) '&' (b1 'imp' b2)) '&'
(a1 'imp' a2) '&' ((b1 'imp' b2) '&' (c1 'imp' c2)) '&' (c1 'imp' c2)) '&'
'not'( a2 '&' b2) '&' 'not'( a2 '&' c2) '&' 'not'( b2 '&' c2)
by BVFUNC_1:7
.=(((a1 'imp' a2) '&' (b1 'imp' b2)) '&'
((b1 'imp' b2) '&' (c1 'imp' c2)) '&' (a1 'imp' a2) '&' (c1 'imp' c2)) '&'
'not'( a2 '&' b2) '&' 'not'( a2 '&' c2) '&' 'not'( b2 '&' c2)
by BVFUNC_1:7
.=((a1 'imp' a2) '&' (b1 'imp' b2)) '&'
((b1 'imp' b2) '&' (c1 'imp' c2)) '&' ((a1 'imp' a2) '&' (c1 'imp' c2)) '&'
'not'( a2 '&' b2) '&' 'not'( a2 '&' c2) '&' 'not'( b2 '&' c2)
by BVFUNC_1:7
.=((a1 'imp' a2) '&' (b1 'imp' b2)) '&'
((b1 'imp' b2) '&' (c1 'imp' c2)) '&' ((a1 'imp' a2) '&' (c1 'imp' c2)) '&'
'not'( a2 '&' c2) '&' 'not'( a2 '&' b2) '&' 'not'( b2 '&' c2)
by BVFUNC_1:7
.=((a1 'imp' a2) '&' (b1 'imp' b2)) '&'
((b1 'imp' b2) '&' (c1 'imp' c2)) '&'
((a1 'imp' a2) '&' (c1 'imp' c2) '&' 'not'( a2 '&' c2)) '&'
'not'( a2 '&' b2) '&' 'not'( b2 '&' c2)
by BVFUNC_1:7
.=((a1 'imp' a2) '&' (b1 'imp' b2)) '&'
((b1 'imp' b2) '&' (c1 'imp' c2)) '&'
'not'( a2 '&' b2) '&' ((a1 'imp' a2) '&' (c1 'imp' c2) '&' 'not'
(a2 '&' c2)) '&' 'not'( b2 '&' c2) by BVFUNC_1:7
.=((a1 'imp' a2) '&' (b1 'imp' b2)) '&'
'not'( a2 '&' b2) '&' ((b1 'imp' b2) '&' (c1 'imp' c2))
'&' ((a1 'imp' a2) '&' (c1 'imp' c2) '&' 'not'( a2 '&' c2)) '&'
'not'( b2 '&' c2) by BVFUNC_1:7
.=((a1 'imp' a2) '&' (b1 'imp' b2) '&' 'not'( a2 '&' b2)) '&'
((b1 'imp' b2) '&' (c1 'imp' c2))
'&' 'not'( b2 '&' c2) '&' ((a1 'imp' a2) '&' (c1 'imp' c2) '&' 'not'
(a2 '&' c2)) by BVFUNC_1:7
.=((a1 'imp' a2) '&' (b1 'imp' b2) '&' 'not'( a2 '&' b2)) '&'
((b1 'imp' b2) '&' (c1 'imp' c2) '&' 'not'( b2 '&' c2)) '&'
((a1 'imp' a2) '&' (c1 'imp' c2) '&' 'not'( a2 '&' c2)) by BVFUNC_1:7
.=(((a1 'imp' a2) '&' (b1 'imp' b2) '&' 'not'( a2 '&' b2)) '&'
((a1 'imp' a2) '&' (c1 'imp' c2) '&' 'not'( a2 '&' c2)) '&'
((b1 'imp' b2) '&' (c1 'imp' c2) '&' 'not'( b2 '&' c2))) by BVFUNC_1:7;
A2:((a1 'imp' a2) '&' (b1 'imp' b2) '&' 'not'( a2 '&' b2)) '&'
((a1 'imp' a2) '&' (c1 'imp' c2) '&' 'not'( a2 '&' c2)) '&'
((b1 'imp' b2) '&' (c1 'imp' c2) '&' 'not'( b2 '&' c2)) 'imp'
((a1 'imp' a2) '&' (b1 'imp' b2) '&' 'not'( a2 '&' b2)) '&'
((a1 'imp' a2) '&' (c1 'imp' c2) '&' 'not'( a2 '&' c2)) =I_el(Y)
by BVFUNC_6:39;
A3:((a1 'imp' a2) '&' (b1 'imp' b2) '&' 'not'( a2 '&' b2)) '&'
((a1 'imp' a2) '&' (c1 'imp' c2) '&' 'not'( a2 '&' c2)) 'imp'
((a1 'imp' a2) '&' (b1 'imp' b2) '&' 'not'( a2 '&' b2)) =I_el(Y)
by BVFUNC_6:39;
A4:((a1 'imp' a2) '&' (b1 'imp' b2) '&' 'not'( a2 '&' b2)) '&'
((a1 'imp' a2) '&' (c1 'imp' c2) '&' 'not'( a2 '&' c2)) 'imp'
((a1 'imp' a2) '&' (c1 'imp' c2) '&' 'not'( a2 '&' c2)) =I_el(Y)
by BVFUNC_6:39;
A5:((a1 'imp' a2) '&' (b1 'imp' b2) '&' 'not'( a2 '&' b2)) '&'
((a1 'imp' a2) '&' (c1 'imp' c2) '&' 'not'( a2 '&' c2)) '&'
((b1 'imp' b2) '&' (c1 'imp' c2) '&' 'not'( b2 '&' c2)) 'imp'
((a1 'imp' a2) '&' (b1 'imp' b2) '&' 'not'( a2 '&' b2)) =I_el(Y)
by A2,A3,BVFUNC_5:10;
A6:((a1 'imp' a2) '&' (b1 'imp' b2) '&' 'not'( a2 '&' b2)) '&'
((a1 'imp' a2) '&' (c1 'imp' c2) '&' 'not'( a2 '&' c2)) '&'
((b1 'imp' b2) '&' (c1 'imp' c2) '&' 'not'( b2 '&' c2)) 'imp'
((a1 'imp' a2) '&' (c1 'imp' c2) '&' 'not'( a2 '&' c2)) =I_el(Y)
by A2,A4,BVFUNC_5:10;
A7:((a1 'imp' a2) '&' (b1 'imp' b2) '&' 'not'( a2 '&' b2)) '&'
((a1 'imp' a2) '&' (c1 'imp' c2) '&' 'not'( a2 '&' c2)) '&'
((b1 'imp' b2) '&' (c1 'imp' c2) '&' 'not'( b2 '&' c2)) 'imp'
((b1 'imp' b2) '&' (c1 'imp' c2) '&' 'not'( b2 '&' c2)) =I_el(Y)
by BVFUNC_6:39;
A8:((a1 'imp' a2) '&' (b1 'imp' b2) '&' 'not'( a2 '&' b2))
'imp'
'not'( a1 '&' b1)=I_el(Y) by Th26;
A9:((a1 'imp' a2) '&' (c1 'imp' c2) '&' 'not'( a2 '&' c2))
'imp'
'not'( a1 '&' c1)=I_el(Y) by Th26;
A10:((b1 'imp' b2) '&' (c1 'imp' c2) '&' 'not'( b2 '&' c2))
'imp'
'not'( b1 '&' c1)=I_el(Y) by Th26;
A11:((a1 'imp' a2) '&' (b1 'imp' b2) '&' 'not'( a2 '&' b2)) '&'
((a1 'imp' a2) '&' (c1 'imp' c2) '&' 'not'( a2 '&' c2)) '&'
((b1 'imp' b2) '&' (c1 'imp' c2) '&' 'not'( b2 '&' c2))
'imp'
'not'( a1 '&' b1)=I_el(Y)
by A5,A8,BVFUNC_5:10;
A12:((a1 'imp' a2) '&' (b1 'imp' b2) '&' 'not'( a2 '&' b2)) '&'
((a1 'imp' a2) '&' (c1 'imp' c2) '&' 'not'( a2 '&' c2)) '&'
((b1 'imp' b2) '&' (c1 'imp' c2) '&' 'not'( b2 '&' c2))
'imp'
'not'( a1 '&' c1)=I_el(Y)
by A6,A9,BVFUNC_5:10;
A13:((a1 'imp' a2) '&' (b1 'imp' b2) '&' 'not'( a2 '&' b2)) '&'
((a1 'imp' a2) '&' (c1 'imp' c2) '&' 'not'( a2 '&' c2)) '&'
((b1 'imp' b2) '&' (c1 'imp' c2) '&' 'not'( b2 '&' c2))
'imp'
'not'( b1 '&' c1)=I_el(Y)
by A7,A10,BVFUNC_5:10;
((a1 'imp' a2) '&' (b1 'imp' b2) '&' 'not'( a2 '&' b2)) '&'
((a1 'imp' a2) '&' (c1 'imp' c2) '&' 'not'( a2 '&' c2)) '&'
((b1 'imp' b2) '&' (c1 'imp' c2) '&' 'not'( b2 '&' c2)) 'imp'
'not'( a1 '&' b1) '&' 'not'( a1 '&' c1) =I_el(Y) by A11,A12,BVFUNC_6:18;
then ((a1 'imp' a2) '&' (b1 'imp' b2) '&' 'not'( a2 '&' b2)) '&'
((a1 'imp' a2) '&' (c1 'imp' c2) '&' 'not'( a2 '&' c2)) '&'
((b1 'imp' b2) '&' (c1 'imp' c2) '&' 'not'( b2 '&' c2)) 'imp'
'not'( a1 '&' b1) '&' 'not'( a1 '&' c1) '&' 'not'( b1 '&' c1) =I_el(Y)
by A13,BVFUNC_6:18;
hence thesis by A1,BVFUNC_1:19;
end;
theorem
a '&' b '<' a by Lm1;
theorem
a '&' b '&' c '<' a &
a '&' b '&' c '<' b by Lm2;
theorem
a '&' b '&' c '&' d '<' a &
a '&' b '&' c '&' d '<' b by Lm3;
theorem
a '&' b '&' c '&' d '&' e '<' a &
a '&' b '&' c '&' d '&' e '<' b by Lm4;
theorem
a '&' b '&' c '&' d '&' e '&' f '<' a &
a '&' b '&' c '&' d '&' e '&' f '<' b by Lm5;
theorem
a '&' b '&' c '&' d '&' e '&' f '&' g '<' a &
a '&' b '&' c '&' d '&' e '&' f '&' g '<' b by Lm6;
theorem Th34:
a '<' b & c '<' d implies a '&' c '<' b '&' d
proof
assume a '<' b & c '<' d;
then a 'imp' b = I_el Y & c 'imp' d = I_el Y by BVFUNC_1:19;
then (a '&' c) 'imp' (b '&' d) = I_el Y by BVFUNC_6:21;
hence thesis by BVFUNC_1:19;
end;
theorem
a '&' b '<' c implies a '&' 'not' c '<' 'not' b
proof
assume a '&' b '<' c;
then I_el Y = a '&' b 'imp' c by BVFUNC_1:19
.= 'not' (a '&' b) 'or' c by BVFUNC_4:8
.= 'not' a 'or' 'not' b 'or' c by BVFUNC_1:17
.= 'not' a 'or' c 'or' 'not' b by BVFUNC_1:11
.= 'not' a 'or' 'not' 'not' c 'or' 'not' b by BVFUNC_1:4
.= 'not' (a '&' 'not' c) 'or' 'not' b by BVFUNC_1:17
.= a '&' 'not' c 'imp' 'not' b by BVFUNC_4:8;
hence thesis by BVFUNC_1:19;
end;
theorem
(a 'imp' c) '&' (b 'imp' c) '&' (a 'or' b) '<' c
proof
set K1 = (a 'imp' c) '&' (b 'imp' c);
K1 '<' (a 'or' b) 'imp' c by Th21;
then A1:K1 '&' (a 'or' b) '<' ((a 'or' b) 'imp' c) '&' (a 'or' b) by Th34;
((a 'or' b) 'imp' c) '&' (a 'or' b) '<' c by Th2;
hence thesis by A1,BVFUNC_1:18;
end;
theorem
((a 'imp' c) 'or' (b 'imp' c)) '&' (a '&' b) '<' c
proof
(a 'imp' c) 'or' (b 'imp' c) = (a '&' b) 'imp' c by BVFUNC_7:6;
hence thesis by Th2;
end;
theorem
a '<' b & c '<' d implies a 'or' c '<' b 'or' d
proof
assume a '<' b & c '<' d;
then a 'imp' b = I_el(Y) & c 'imp' d = I_el(Y) by BVFUNC_1:19;
then (a 'or' c) 'imp' (b 'or' d) = I_el(Y) by BVFUNC_6:22;
hence thesis by BVFUNC_1:19;
end;
theorem Th39:
a '<' a 'or' b
proof
a 'imp' (a 'or' b) = I_el Y by BVFUNC_6:27;
hence thesis by BVFUNC_1:19;
end;
theorem
a '&' b '<' a 'or' b
proof
A1:a '&' b '<' a by Lm1;
a '<' a 'or' b by Th39;
hence thesis by A1,BVFUNC_1:18;
end;