Copyright (c) 1999 Association of Mizar Users
environ
vocabulary FUNCT_2, MARGREL1, ZF_LANG, BVFUNC_1, PARTIT1;
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;
theorem 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
let a,b,c be Element of Funcs(Y,BOOLEAN);
for z being Element of Y st
Pj((a '&' b) 'or' (b '&' c) 'or' (c '&' a),z)=TRUE
holds
Pj((a 'or' b) '&' (b 'or' c) '&' (c 'or' a),z)=TRUE
proof
let z be Element of Y;
assume A1:Pj((a '&' b) 'or' (b '&' c) 'or' (c '&' a),z)=TRUE;
A2:Pj((a '&' b) 'or' (b '&' c) 'or' (c '&' a),z)
=Pj((a '&' b) 'or' (b '&' c),z) 'or' Pj(c '&' a,z) by BVFUNC_1:def 7
.=Pj(a '&' b,z) 'or' Pj(b '&' c,z) 'or' Pj(c '&' a,z) by BVFUNC_1:def 7
.=(Pj(a,z) '&' Pj(b,z)) 'or' Pj(b '&' c,z) 'or' Pj(c '&' a,z)
by VALUAT_1:def 6
.=(Pj(a,z) '&' Pj(b,z)) 'or' (Pj(b,z) '&' Pj(c,z)) 'or' Pj(c '&' a,z)
by VALUAT_1:def 6
.=(Pj(a,z) '&' Pj(b,z)) 'or' (Pj(b,z) '&' Pj(c,z)) 'or' (Pj(c,z) '&' Pj(a,z))
by VALUAT_1:def 6;
now assume A3: Pj((a 'or' b) '&' (b 'or' c) '&' (c 'or' a),z)<>TRUE;
Pj((a 'or' b) '&' (b 'or' c) '&' (c 'or' a),z)
=Pj((a 'or' b) '&' (b 'or' c),z) '&' Pj(c 'or' a,z) by VALUAT_1:def 6
.=Pj(a 'or' b,z) '&' Pj(b 'or' c,z) '&' Pj(c 'or' a,z) by VALUAT_1:def 6
.=(Pj(a,z) 'or' Pj(b,z)) '&' Pj(b 'or' c,z) '&' Pj(c 'or' a,z)
by BVFUNC_1:def 7
.=(Pj(a,z) 'or' Pj(b,z)) '&' (Pj(b,z) 'or' Pj(c,z)) '&' Pj(c 'or' a,z)
by BVFUNC_1:def 7
.=(Pj(a,z) 'or' Pj(b,z)) '&' (Pj(b,z) 'or' Pj(c,z)) '&'
(Pj(c,z) 'or' Pj(a,z))
by BVFUNC_1:def 7;
then A4: (Pj(a,z) 'or' Pj(b,z)) '&' (Pj(b,z) 'or' Pj(c,z)) '&'
(Pj(c,z) 'or' Pj(a,z)) = FALSE by A3,MARGREL1:43;
now per cases by A4,MARGREL1:45;
case A5: (Pj(a,z) 'or' Pj(b,z)) '&' (Pj(b,z) 'or' Pj(c,z))=FALSE;
now per cases by A5,MARGREL1:45;
case A6:(Pj(a,z) 'or' Pj(b,z))=FALSE;
A7:Pj(a,z)=TRUE or Pj(a,z)=FALSE by MARGREL1:39;
Pj(b,z)=TRUE or Pj(b,z)=FALSE by MARGREL1:39;
then Pj(a,z)=FALSE & Pj(b,z)=FALSE by A6,A7,BINARITH:19;
then (Pj(a,z) '&' Pj(b,z)) 'or' (Pj(b,z) '&' Pj(c,z)) 'or'
(Pj(c,z) '&' Pj(a,z))
=FALSE 'or' (FALSE '&' Pj(c,z)) 'or'
(Pj(c,z) '&' FALSE) by MARGREL1:49
.=FALSE 'or' FALSE 'or' (FALSE '&' Pj(c,z)) by MARGREL1:49
.=FALSE 'or' (FALSE '&' Pj(c,z)) by BINARITH:7
.=FALSE '&' Pj(c,z) by BINARITH:7
.=FALSE by MARGREL1:49;
hence thesis by A1,A2,MARGREL1:43;
case A8:(Pj(b,z) 'or' Pj(c,z))=FALSE;
A9: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 A8,A9,BINARITH:19;
then (Pj(a,z) '&' Pj(b,z)) 'or' (Pj(b,z) '&' Pj(c,z)) 'or'
(Pj(c,z) '&' Pj(a,z))
=FALSE 'or' (FALSE '&' FALSE) 'or'
(FALSE '&' Pj(a,z)) by MARGREL1:49
.=FALSE 'or' FALSE 'or' (FALSE '&' Pj(a,z)) by MARGREL1:49
.=FALSE 'or' FALSE 'or' FALSE by MARGREL1:49
.=FALSE 'or' FALSE by BINARITH:7
.=FALSE by BINARITH:7;
hence thesis by A1,A2,MARGREL1:43;
end;
hence thesis;
case A10:(Pj(c,z) 'or' Pj(a,z))=FALSE;
A11:Pj(c,z)=TRUE or Pj(c,z)=FALSE by MARGREL1:39;
Pj(a,z)=TRUE or Pj(a,z)=FALSE by MARGREL1:39;
then Pj(c,z)=FALSE & Pj(a,z)=FALSE by A10,A11,BINARITH:19;
then (Pj(a,z) '&' Pj(b,z)) 'or' (Pj(b,z) '&' Pj(c,z)) 'or'
(Pj(c,z) '&' Pj(a,z))
=FALSE 'or' (FALSE '&' Pj(b,z)) 'or'
(FALSE '&' FALSE) by MARGREL1:49
.=FALSE 'or' FALSE 'or'
(FALSE '&' FALSE) by MARGREL1:49
.=FALSE 'or' FALSE 'or' FALSE by MARGREL1:49
.=FALSE 'or' FALSE by BINARITH:7
.=FALSE by BINARITH:7;
hence thesis by A1,A2,MARGREL1:43;
end;
hence thesis;
end;
hence thesis;
end;
then A12:(a '&' b) 'or' (b '&' c) 'or' (c '&' a) '<'
(a 'or' b) '&' (b 'or' c) '&' (c 'or' a) by BVFUNC_1:def 15;
for z being Element of Y st
Pj((a 'or' b) '&' (b 'or' c) '&' (c 'or' a),z)=TRUE
holds
Pj((a '&' b) 'or' (b '&' c) 'or' (c '&' a),z)=TRUE
proof
let z be Element of Y;
assume A13:Pj((a 'or' b) '&' (b 'or' c) '&' (c 'or' a),z)=TRUE;
A14:Pj((a 'or' b) '&' (b 'or' c) '&' (c 'or' a),z)
=Pj((a 'or' b) '&' (b 'or' c),z) '&' Pj(c 'or' a,z) by VALUAT_1:def 6
.=Pj(a 'or' b,z) '&' Pj(b 'or' c,z) '&' Pj(c 'or' a,z) by VALUAT_1:def 6
.=(Pj(a,z) 'or' Pj(b,z)) '&' Pj(b 'or' c,z) '&' Pj(c 'or' a,z)
by BVFUNC_1:def 7
.=(Pj(a,z) 'or' Pj(b,z)) '&' (Pj(b,z) 'or' Pj(c,z)) '&' Pj(c 'or' a,z)
by BVFUNC_1:def 7
.=(Pj(a,z) 'or' Pj(b,z)) '&' (Pj(b,z) 'or' Pj(c,z)) '&'
(Pj(c,z) 'or' Pj(a,z))
by BVFUNC_1:def 7;
now assume A15: Pj((a '&' b) 'or' (b '&' c) 'or' (c '&' a),z)<>TRUE;
A16: Pj((a '&' b) 'or' (b '&' c) 'or' (c '&' a),z)
=Pj((a '&' b) 'or' (b '&' c),z) 'or' Pj(c '&' a,z) by BVFUNC_1:def 7
.=Pj(a '&' b,z) 'or' Pj(b '&' c,z) 'or' Pj(c '&' a,z) by BVFUNC_1:def 7
.=(Pj(a,z) '&' Pj(b,z)) 'or' Pj(b '&' c,z) 'or' Pj(c '&' a,z)
by VALUAT_1:def 6
.=(Pj(a,z) '&' Pj(b,z)) 'or' (Pj(b,z) '&' Pj(c,z)) 'or' Pj(c '&' a,z)
by VALUAT_1:def 6
.=(Pj(a,z) '&' Pj(b,z)) 'or' (Pj(b,z) '&' Pj(c,z)) 'or'
(Pj(c,z) '&' Pj(a,z))
by VALUAT_1:def 6;
A17:((Pj(a,z) '&' Pj(b,z)) 'or' (Pj(b,z) '&' Pj(c,z)))=TRUE or
((Pj(a,z) '&' Pj(b,z)) 'or' (Pj(b,z) '&' Pj(c,z)))=FALSE by MARGREL1:39;
A18: (Pj(c,z) '&' Pj(a,z))=TRUE or (Pj(c,z) '&' Pj(a,z))=FALSE
by MARGREL1:39;
A19:(Pj(a,z) '&' Pj(b,z))=TRUE or (Pj(a,z) '&' Pj(b,z))=FALSE
by MARGREL1:39;
(Pj(b,z) '&' Pj(c,z))=TRUE or (Pj(b,z) '&' Pj(c,z))=FALSE
by MARGREL1:39;
then A20: (Pj(a,z) '&' Pj(b,z))=FALSE & (Pj(b,z) '&' Pj(c,z))=FALSE
by A15,A16,A17,A19,BINARITH:19;
now per cases by A15,A16,A18,A20,BINARITH:19,MARGREL1:45;
case Pj(a,z)=FALSE & Pj(b,z)=FALSE;
then (Pj(a,z) 'or' Pj(b,z)) '&' (Pj(b,z) 'or' Pj(c,z)) '&'
(Pj(c,z) 'or' Pj(a,z))
=FALSE '&' (FALSE 'or' Pj(c,z)) '&'
(Pj(c,z) 'or' FALSE) by BINARITH:7
.=FALSE '&' Pj(c,z) '&'
(Pj(c,z) 'or' FALSE) by BINARITH:7
.=FALSE '&' Pj(c,z) '&' Pj(c,z) by BINARITH:7
.=FALSE '&' (Pj(c,z) '&' Pj(c,z)) by MARGREL1:52
.=FALSE by MARGREL1:49;
hence thesis by A13,A14,MARGREL1:43;
case Pj(b,z)=FALSE & Pj(c,z)=FALSE;
then (Pj(a,z) 'or' Pj(b,z)) '&' (Pj(b,z) 'or' Pj(c,z)) '&'
(Pj(c,z) 'or' Pj(a,z))
=Pj(a,z) '&' (FALSE 'or' FALSE) '&'
(FALSE 'or' Pj(a,z)) by BINARITH:7
.=Pj(a,z) '&' FALSE '&' (FALSE 'or' Pj(a,z)) by BINARITH:7
.=FALSE '&' Pj(a,z) '&' Pj(a,z) by BINARITH:7
.=FALSE '&' (Pj(a,z) '&' Pj(a,z)) by MARGREL1:52
.=FALSE by MARGREL1:49;
hence thesis by A13,A14,MARGREL1:43;
case Pj(c,z)=FALSE & Pj(a,z)=FALSE;
then (Pj(a,z) 'or' Pj(b,z)) '&' (Pj(b,z) 'or' Pj(c,z)) '&'
(Pj(c,z) 'or' Pj(a,z))
=Pj(b,z) '&' (Pj(b,z) 'or' FALSE) '&'
(FALSE 'or' FALSE) by BINARITH:7
.=Pj(b,z) '&' Pj(b,z) '&'
(FALSE 'or' FALSE) by BINARITH:7
.=FALSE '&' (Pj(b,z) '&' Pj(b,z)) by BINARITH:7
.=FALSE by MARGREL1:49;
hence thesis by A13,A14,MARGREL1:43;
end;
hence thesis;
end;
hence thesis;
end;
then (a 'or' b) '&' (b 'or' c) '&' (c 'or' a) '<'
(a '&' b) 'or' (b '&' c) 'or' (c '&' a) by BVFUNC_1:def 15;
hence thesis by A12,BVFUNC_1:18;
end;
Lm1: 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
let a,b,c be Element of Funcs(Y,BOOLEAN);
let z be Element of Y;
assume A1:
Pj((a '&' 'not' b) 'or' (b '&' 'not' c) 'or' (c '&' 'not' a),z)=TRUE;
A2: Pj((a '&' 'not' b) 'or' (b '&' 'not' c) 'or' (c '&' 'not' a),z)
=Pj((a '&' 'not' b) 'or' (b '&' 'not' c),z) 'or' Pj(c '&' 'not'
a,z) by BVFUNC_1:def 7
.=Pj(a '&' 'not' b,z) 'or' Pj(b '&' 'not' c,z) 'or' Pj(c '&' 'not'
a,z) by BVFUNC_1:def 7
.=(Pj(a,z) '&' Pj('not' b,z)) 'or' Pj(b '&' 'not' c,z) 'or'
Pj(c '&' 'not' a,z) by VALUAT_1:def 6
.=(Pj(a,z) '&' Pj('not' b,z)) 'or' (Pj(b,z) '&' Pj('not' c,z)) 'or'
Pj(c '&' 'not' a,z) by VALUAT_1:def 6
.=(Pj(a,z) '&' Pj('not' b,z)) 'or' (Pj(b,z) '&' Pj('not' c,z)) 'or'
(Pj(c,z) '&' Pj('not' a,z)) by VALUAT_1:def 6
.=(Pj(a,z) '&' 'not' Pj(b,z)) 'or' (Pj(b,z) '&' Pj('not' c,z)) 'or'
(Pj(c,z) '&' Pj('not' a,z)) by VALUAT_1:def 5
.=(Pj(a,z) '&' 'not' Pj(b,z)) 'or' (Pj(b,z) '&' 'not' Pj(c,z)) 'or'
(Pj(c,z) '&' Pj('not' a,z)) by VALUAT_1:def 5
.=(Pj(a,z) '&' 'not' Pj(b,z)) 'or' (Pj(b,z) '&' 'not' Pj(c,z)) 'or'
(Pj(c,z) '&' 'not' Pj(a,z)) by VALUAT_1:def 5;
now assume
A3: Pj((b '&' 'not' a) 'or' (c '&' 'not' b) 'or'
(a '&' 'not' c),z)<>TRUE;
A4: Pj((b '&' 'not' a) 'or' (c '&' 'not' b) 'or' (a '&' 'not' c),z)
=Pj((b '&' 'not' a) 'or' (c '&' 'not' b),z) 'or' Pj(a '&' 'not'
c,z) by BVFUNC_1:def 7
.=Pj(b '&' 'not' a,z) 'or' Pj(c '&' 'not' b,z) 'or'
Pj(a '&' 'not' c,z) by BVFUNC_1:def 7
.=(Pj(b,z) '&' Pj('not' a,z)) 'or' Pj(c '&' 'not' b,z) 'or'
Pj(a '&' 'not' c,z) by VALUAT_1:def 6
.=(Pj(b,z) '&' Pj('not' a,z)) 'or' (Pj(c,z) '&' Pj('not' b,z)) 'or'
Pj(a '&' 'not' c,z) by VALUAT_1:def 6
.=(Pj(b,z) '&' Pj('not' a,z)) 'or' (Pj(c,z) '&' Pj('not' b,z)) 'or'
(Pj(a,z) '&' Pj('not' c,z)) by VALUAT_1:def 6;
A5:((Pj(b,z) '&' Pj('not' a,z)) 'or' (Pj(c,z) '&' Pj('not' b,z)))=TRUE or
((Pj(b,z) '&' Pj('not' a,z)) 'or' (Pj(c,z) '&' Pj('not' b,z)))=FALSE
by MARGREL1:39;
A6: (Pj(a,z) '&' Pj('not' c,z))=TRUE or (Pj(a,z) '&' Pj('not' c,z))=FALSE
by MARGREL1:39;
A7:(Pj(b,z) '&' Pj('not' a,z))=TRUE or (Pj(b,z) '&' Pj('not' a,z))=FALSE
by MARGREL1:39;
(Pj(c,z) '&' Pj('not' b,z))=TRUE or (Pj(c,z) '&' Pj('not' b,z))=FALSE
by MARGREL1:39;
then A8: (Pj(b,z) '&' Pj('not' a,z))=FALSE & (Pj(c,z) '&' Pj('not' b,z))=FALSE
by A3,A4,A5,A7,BINARITH:19;
then A9: Pj(b,z)=FALSE or Pj('not' a,z)=FALSE by MARGREL1:45;
A10: Pj(c,z)=FALSE or Pj('not' b,z)=FALSE by A8,MARGREL1:45;
now per cases by A3,A4,A6,BINARITH:19,MARGREL1:45;
case A11:Pj(a,z)=FALSE;
then 'not' Pj(a,z)=TRUE by MARGREL1:41;
then A12: 'not' Pj(a,z)<>FALSE by MARGREL1:43;
then 'not' Pj(b,z)=TRUE by A9,MARGREL1:41,VALUAT_1:def 5;
then 'not' Pj(b,z)<>FALSE by MARGREL1:43;
then 'not' Pj(c,z)=TRUE by A10,MARGREL1:41,VALUAT_1:def 5;
then (Pj(a,z) '&' 'not' Pj(b,z)) 'or' (Pj(b,z) '&' 'not' Pj(c,z)) 'or'
(Pj(c,z) '&' 'not' Pj(a,z))
=FALSE 'or' (FALSE '&' TRUE) 'or'
(FALSE '&' TRUE) by A9,A10,A11,A12,MARGREL1:49,VALUAT_1:def 5
.=FALSE 'or' FALSE 'or'
(FALSE '&' TRUE) by MARGREL1:49
.=FALSE 'or' FALSE 'or' FALSE by MARGREL1:49
.=FALSE 'or' FALSE by BINARITH:7
.=FALSE by BINARITH:7;
hence thesis by A1,A2,MARGREL1:43;
case Pj('not' c,z)=FALSE;
then A13: 'not' Pj(c,z)=FALSE by VALUAT_1:def 5;
then A14: Pj(c,z)=TRUE by MARGREL1:41;
then 'not' Pj(b,z)=FALSE by A10,MARGREL1:43,VALUAT_1:def 5;
then A15: Pj(b,z)=TRUE by MARGREL1:41;
then 'not' Pj(a,z)=FALSE by A9,MARGREL1:43,VALUAT_1:def 5;
then Pj(a,z)=TRUE by MARGREL1:41;
then (Pj(a,z) '&' 'not' Pj(b,z)) 'or' (Pj(b,z) '&' 'not' Pj(c,z)) 'or'
(Pj(c,z) '&' 'not' Pj(a,z))
=FALSE 'or' (TRUE '&' FALSE) 'or'
(TRUE '&' FALSE) by A13,A14,A15,MARGREL1:50
.=FALSE 'or' FALSE 'or'
(TRUE '&' FALSE) by MARGREL1:50
.=FALSE 'or' FALSE 'or' FALSE by MARGREL1:50
.=FALSE 'or' FALSE by BINARITH:7
.=FALSE by BINARITH:7;
hence thesis by A1,A2,MARGREL1:43;
end;
hence thesis;
end;
hence thesis;
end;
theorem 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
let a,b,c be Element of Funcs(Y,BOOLEAN);
A1:(a '&' 'not' b) 'or' (b '&' 'not' c) 'or' (c '&' 'not' a) '<'
(b '&' 'not' a) 'or' (c '&' 'not' b) 'or' (a '&' 'not' c) by Lm1;
(b '&' 'not' a) 'or' (c '&' 'not' b) 'or' (a '&' 'not' c) '<'
(a '&' 'not' b) 'or' (b '&' 'not' c) 'or' (c '&' 'not' a) by Lm1;
hence thesis by A1,BVFUNC_1:18;
end;
Lm2: 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
let a,b,c be Element of Funcs(Y,BOOLEAN);
let z be Element of Y;
assume A1:
Pj((a 'or' 'not' b) '&' (b 'or' 'not' c) '&' (c 'or' 'not' a),z)=TRUE;
A2: Pj((a 'or' 'not' b) '&' (b 'or' 'not' c) '&' (c 'or' 'not' a),z)
=Pj((a 'or' 'not' b) '&' (b 'or' 'not' c),z) '&' Pj(c 'or' 'not'
a,z) by VALUAT_1:def 6
.=Pj(a 'or' 'not' b,z) '&' Pj(b 'or' 'not' c,z) '&' Pj(c 'or' 'not'
a,z) by VALUAT_1:def 6
.=(Pj(a,z) 'or' Pj('not' b,z)) '&' Pj(b 'or' 'not' c,z) '&'
Pj(c 'or' 'not' a,z) by BVFUNC_1:def 7
.=(Pj(a,z) 'or' Pj('not' b,z)) '&' (Pj(b,z) 'or' Pj('not' c,z)) '&'
Pj(c 'or' 'not' a,z) by BVFUNC_1:def 7
.=(Pj(a,z) 'or' Pj('not' b,z)) '&' (Pj(b,z) 'or' Pj('not' c,z)) '&'
(Pj(c,z) 'or' Pj('not' a,z)) by BVFUNC_1:def 7
.=(Pj(a,z) 'or' 'not' Pj(b,z)) '&' (Pj(b,z) 'or' Pj('not' c,z)) '&'
(Pj(c,z) 'or' Pj('not' a,z)) by VALUAT_1:def 5
.=(Pj(a,z) 'or' 'not' Pj(b,z)) '&' (Pj(b,z) 'or' 'not' Pj(c,z)) '&'
(Pj(c,z) 'or' Pj('not' a,z)) by VALUAT_1:def 5
.=(Pj(a,z) 'or' 'not' Pj(b,z)) '&' (Pj(b,z) 'or' 'not' Pj(c,z)) '&'
(Pj(c,z) 'or' 'not' Pj(a,z)) by VALUAT_1:def 5;
now assume
A3: Pj((b 'or' 'not' a) '&' (c 'or' 'not' b) '&'
(a 'or' 'not' c),z)<>TRUE;
Pj((b 'or' 'not' a) '&' (c 'or' 'not' b) '&' (a 'or' 'not' c),z)
=Pj((b 'or' 'not' a) '&' (c 'or' 'not' b),z) '&' Pj(a 'or' 'not'
c,z) by VALUAT_1:def 6
.=Pj(b 'or' 'not' a,z) '&' Pj(c 'or' 'not' b,z) '&'
Pj(a 'or' 'not' c,z) by VALUAT_1:def 6
.=(Pj(b,z) 'or' Pj('not' a,z)) '&' Pj(c 'or' 'not' b,z) '&'
Pj(a 'or' 'not' c,z) by BVFUNC_1:def 7
.=(Pj(b,z) 'or' Pj('not' a,z)) '&' (Pj(c,z) 'or' Pj('not' b,z)) '&'
Pj(a 'or' 'not' c,z) by BVFUNC_1:def 7
.=(Pj(b,z) 'or' Pj('not' a,z)) '&' (Pj(c,z) 'or' Pj('not' b,z)) '&'
(Pj(a,z) 'or' Pj('not' c,z)) by BVFUNC_1:def 7;
then A4: (Pj(b,z) 'or' Pj('not' a,z)) '&' (Pj(c,z) 'or' Pj('not' b,z)) '&'
(Pj(a,z) 'or' Pj('not' c,z))=FALSE by A3,MARGREL1:43;
now per cases by A4,MARGREL1:45;
case A5: ((Pj(b,z) 'or' Pj('not' a,z)) '&'
(Pj(c,z) 'or' Pj('not' b,z)))=FALSE;
now per cases by A5,MARGREL1:45;
case A6:(Pj(b,z) 'or' Pj('not' a,z))=FALSE;
A7:Pj(b,z)=TRUE or Pj(b,z)=FALSE by MARGREL1:39;
Pj('not' a,z)=TRUE or Pj('not' a,z)=FALSE by MARGREL1:39;
then A8: Pj(b,z)=FALSE & Pj('not' a,z)=FALSE by A6,A7,BINARITH:19;
then 'not' Pj(a,z)=FALSE by VALUAT_1:def 5;
then Pj(a,z)=TRUE by MARGREL1:41;
then (Pj(a,z) 'or' 'not' Pj(b,z)) '&' (Pj(b,z) 'or' 'not' Pj(c,z)) '&'
(Pj(c,z) 'or' 'not' Pj(a,z))
=(TRUE 'or' TRUE) '&' (FALSE 'or' 'not' Pj(c,z)) '&'
(Pj(c,z) 'or' 'not' TRUE) by A8,MARGREL1:41
.=(TRUE 'or' TRUE) '&' (FALSE 'or' 'not' Pj(c,z)) '&'
(Pj(c,z) 'or' FALSE) by MARGREL1:41
.=TRUE '&' (FALSE 'or' 'not' Pj(c,z)) '&'
(Pj(c,z) 'or' FALSE) by BINARITH:19
.=TRUE '&' 'not' Pj(c,z) '&'
(Pj(c,z) 'or' FALSE) by BINARITH:7
.=TRUE '&' 'not' Pj(c,z) '&' Pj(c,z) by BINARITH:7
.=TRUE '&' ('not' Pj(c,z) '&' Pj(c,z)) by MARGREL1:52
.=TRUE '&' FALSE by MARGREL1:46
.=FALSE by MARGREL1:50;
hence thesis by A1,A2,MARGREL1:43;
case A9:(Pj(c,z) 'or' Pj('not' b,z))=FALSE;
A10:Pj(c,z)=TRUE or Pj(c,z)=FALSE by MARGREL1:39;
Pj('not' b,z)=TRUE or Pj('not' b,z)=FALSE by MARGREL1:39;
then A11: Pj(c,z)=FALSE & Pj('not' b,z)=FALSE by A9,A10,BINARITH:19;
then 'not' Pj(b,z)=FALSE by VALUAT_1:def 5;
then (Pj(a,z) 'or' 'not' Pj(b,z)) '&' (Pj(b,z) 'or' 'not' Pj(c,z)) '&'
(Pj(c,z) 'or' 'not' Pj(a,z))
=(Pj(a,z) 'or' FALSE) '&' (TRUE 'or' 'not' FALSE) '&'
(FALSE 'or' 'not' Pj(a,z)) by A11,MARGREL1:41
.=(Pj(a,z) 'or' FALSE) '&' TRUE '&'
(FALSE 'or' 'not' Pj(a,z)) by BINARITH:19
.=Pj(a,z) '&' TRUE '&'
(FALSE 'or' 'not' Pj(a,z)) by BINARITH:7
.=TRUE '&' Pj(a,z) '&' 'not' Pj(a,z) by BINARITH:7
.=TRUE '&' (Pj(a,z) '&' 'not' Pj(a,z)) by MARGREL1:52
.=TRUE '&' FALSE by MARGREL1:46
.=FALSE by MARGREL1:50;
hence thesis by A1,A2,MARGREL1:43;
end;
hence thesis;
case A12:(Pj(a,z) 'or' Pj('not' c,z))=FALSE;
A13:Pj(a,z)=TRUE or Pj(a,z)=FALSE by MARGREL1:39;
Pj('not' c,z)=TRUE or Pj('not' c,z)=FALSE by MARGREL1:39;
then A14: Pj(a,z)=FALSE & Pj('not' c,z)=FALSE by A12,A13,BINARITH:19;
then 'not' Pj(c,z)=FALSE by VALUAT_1:def 5;
then (Pj(a,z) 'or' 'not' Pj(b,z)) '&' (Pj(b,z) 'or' 'not' Pj(c,z)) '&'
(Pj(c,z) 'or' 'not' Pj(a,z))
=(FALSE 'or' 'not' Pj(b,z)) '&' (Pj(b,z) 'or' FALSE) '&'
(TRUE 'or' 'not' FALSE) by A14,MARGREL1:41
.=(FALSE 'or' 'not' Pj(b,z)) '&' (Pj(b,z) 'or' FALSE) '&'
TRUE by BINARITH:19
.='not' Pj(b,z) '&' (Pj(b,z) 'or' FALSE) '&'
TRUE by BINARITH:7
.='not' Pj(b,z) '&' Pj(b,z) '&' TRUE by BINARITH:7
.=FALSE '&' TRUE by MARGREL1:46
.=FALSE by MARGREL1:49;
hence thesis by A1,A2,MARGREL1:43;
end;
hence thesis;
end;
hence thesis;
end;
theorem 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
let a,b,c be Element of Funcs(Y,BOOLEAN);
A1:(a 'or' 'not' b) '&' (b 'or' 'not' c) '&' (c 'or' 'not' a) '<'
(b 'or' 'not' a) '&' (c 'or' 'not' b) '&' (a 'or' 'not' c) by Lm2;
(b 'or' 'not' a) '&' (c 'or' 'not' b) '&' (a 'or' 'not' c) '<'
(a 'or' 'not' b) '&' (b 'or' 'not' c) '&' (c 'or' 'not' a) by Lm2;
hence thesis by A1,BVFUNC_1:18;
end;
theorem
for a,b,c being Element of Funcs(Y,BOOLEAN) holds
(c 'imp' a)=I_el(Y) & (c 'imp' b)=I_el(Y) implies
c 'imp' (a 'or' b)=I_el(Y)
proof
let a,b,c be Element of Funcs(Y,BOOLEAN);
assume A1:(c 'imp' a)=I_el(Y) & (c 'imp' b)=I_el(Y);
c 'imp' (a 'or' b)
=(c 'imp' a) 'or' (c 'imp' b) by BVFUNC_7:3
.=I_el(Y) by A1,BVFUNC_1:13;
hence thesis;
end;
theorem for a,b,c being Element of Funcs(Y,BOOLEAN) holds
(a 'imp' c)=I_el(Y) & (b 'imp' c)=I_el(Y) implies
(a '&' b) 'imp' c = I_el(Y)
proof
let a,b,c be Element of Funcs(Y,BOOLEAN);
(a 'imp' c)=I_el(Y) & (b 'imp' c)=I_el(Y) implies
(a '&' b) 'imp' (c '&' c)=I_el(Y) by BVFUNC_6:21;
hence thesis by BVFUNC_1:6;
end;
theorem 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
let a1,a2,b1,b2,c1,c2 be Element of Funcs(Y,BOOLEAN);
let z be Element of Y;
assume A1:
Pj((a1 'imp' a2) '&' (b1 'imp' b2) '&' (c1 'imp' c2) '&'
(a1 'or' b1 'or' c1),z)=TRUE;
A2:Pj((a1 'imp' a2) '&' (b1 'imp' b2) '&' (c1 'imp' c2) '&'
(a1 'or' b1 'or' c1),z)
=Pj((a1 'imp' a2) '&' (b1 'imp' b2) '&' (c1 'imp' c2),z) '&'
Pj(a1 'or' b1 'or' c1,z) by VALUAT_1:def 6
.=Pj((a1 'imp' a2) '&' (b1 'imp' b2),z) '&' Pj(c1 'imp' c2,z) '&'
Pj(a1 'or' b1 'or' c1,z) by VALUAT_1:def 6
.=Pj(a1 'imp' a2,z) '&' Pj(b1 'imp' b2,z) '&' Pj(c1 'imp' c2,z) '&'
Pj(a1 'or' b1 'or' c1,z) by VALUAT_1:def 6
.=Pj('not' a1 'or' a2,z) '&' Pj(b1 'imp' b2,z) '&' Pj(c1 'imp' c2,z) '&'
Pj(a1 'or' b1 'or' c1,z) by BVFUNC_4:8
.=Pj('not' a1 'or' a2,z) '&' Pj('not' b1 'or' b2,z) '&' Pj(c1 'imp' c2,z) '&'
Pj(a1 'or' b1 'or' c1,z) by BVFUNC_4:8
.=Pj('not' a1 'or' a2,z) '&' Pj('not' b1 'or' b2,z) '&' Pj('not'
c1 'or' c2,z) '&'
Pj(a1 'or' b1 'or' c1,z) by BVFUNC_4:8
.=(Pj('not' a1,z) 'or' Pj(a2,z)) '&' Pj('not' b1 'or' b2,z) '&' Pj('not'
c1 'or' c2,z) '&'
Pj(a1 'or' b1 'or' c1,z) by BVFUNC_1:def 7
.=(Pj('not' a1,z) 'or' Pj(a2,z)) '&' (Pj('not' b1,z) 'or' Pj(b2,z)) '&'
Pj('not' c1 'or' c2,z) '&' Pj(a1 'or' b1 'or' c1,z) by BVFUNC_1:def 7
.=(Pj('not' a1,z) 'or' Pj(a2,z)) '&' (Pj('not' b1,z) 'or' Pj(b2,z)) '&'
(Pj('not'
c1,z) 'or' Pj(c2,z)) '&' Pj(a1 'or' b1 'or' c1,z) by BVFUNC_1:def 7
.=(Pj('not' a1,z) 'or' Pj(a2,z)) '&' (Pj('not' b1,z) 'or' Pj(b2,z)) '&'
(Pj('not' c1,z) 'or' Pj(c2,z)) '&' (Pj(a1 'or' b1,z) 'or' Pj(c1,z))
by BVFUNC_1:def 7
.=(Pj('not' a1,z) 'or' Pj(a2,z)) '&' (Pj('not' b1,z) 'or' Pj(b2,z)) '&'
(Pj('not' c1,z) 'or' Pj(c2,z)) '&' (Pj(a1,z) 'or' Pj(b1,z) 'or' Pj(c1,z))
by BVFUNC_1:def 7
.=('not' Pj(a1,z) 'or' Pj(a2,z)) '&' (Pj('not' b1,z) 'or' Pj(b2,z)) '&'
(Pj('not' c1,z) 'or' Pj(c2,z)) '&' (Pj(a1,z) 'or' Pj(b1,z) 'or' Pj(c1,z))
by VALUAT_1:def 5
.=('not' Pj(a1,z) 'or' Pj(a2,z)) '&' ('not' Pj(b1,z) 'or' Pj(b2,z)) '&'
(Pj('not' c1,z) 'or' Pj(c2,z)) '&' (Pj(a1,z) 'or' Pj(b1,z) 'or' Pj(c1,z))
by VALUAT_1:def 5
.=('not' Pj(a1,z) 'or' Pj(a2,z)) '&' ('not' Pj(b1,z) 'or' Pj(b2,z)) '&'
('not' Pj(c1,z) 'or' Pj(c2,z)) '&' (Pj(a1,z) 'or' Pj(b1,z) 'or' Pj(c1,z))
by VALUAT_1:def 5;
now assume A3: Pj(a2 'or' b2 'or' c2,z)<>TRUE;
A4: Pj(a2 'or' b2 'or' c2,z)
=Pj(a2 'or' b2,z) 'or' Pj(c2,z) by BVFUNC_1:def 7
.=Pj(a2,z) 'or' Pj(b2,z) 'or' Pj(c2,z) by BVFUNC_1:def 7;
A5:(Pj(a2,z) 'or' Pj(b2,z))=TRUE or
(Pj(a2,z) 'or' Pj(b2,z))=FALSE by MARGREL1:39;
A6: Pj(c2,z)=TRUE or Pj(c2,z)=FALSE by MARGREL1:39;
A7:Pj(a2,z)=TRUE or Pj(a2,z)=FALSE by MARGREL1:39;
Pj(b2,z)=TRUE or Pj(b2,z)=FALSE by MARGREL1:39;
then Pj(a2,z)=FALSE & Pj(b2,z)=FALSE by A3,A4,A5,A7,BINARITH:19;
then A8: ('not' Pj(a1,z) 'or' Pj(a2,z)) '&' ('not' Pj(b1,z) 'or' Pj(b2,z)) '&'
('not' Pj(c1,z) 'or' Pj(c2,z)) '&' (Pj(a1,z) 'or' Pj(b1,z) 'or' Pj(c1,z))
='not' Pj(a1,z) '&' ('not' Pj(b1,z) 'or' FALSE) '&'
('not' Pj(c1,z) 'or' FALSE) '&' (Pj(a1,z) 'or' Pj(b1,z) 'or' Pj(c1,z))
by A3,A4,A6,BINARITH:7,19
.='not' Pj(a1,z) '&' 'not' Pj(b1,z) '&'
('not' Pj(c1,z) 'or' FALSE) '&' (Pj(a1,z) 'or' Pj(b1,z) 'or' Pj(c1,z))
by BINARITH:7
.=('not' Pj(a1,z) '&' 'not' Pj(b1,z) '&' 'not' Pj(c1,z)) '&'
(Pj(a1,z) 'or' Pj(b1,z) 'or' Pj(c1,z))
by BINARITH:7
.=(Pj('not' a1,z) '&' 'not' Pj(b1,z) '&' 'not' Pj(c1,z)) '&'
(Pj(a1,z) 'or' Pj(b1,z) 'or' Pj(c1,z))
by VALUAT_1:def 5
.=(Pj('not' a1,z) '&' Pj('not' b1,z) '&' 'not' Pj(c1,z)) '&'
(Pj(a1,z) 'or' Pj(b1,z) 'or' Pj(c1,z))
by VALUAT_1:def 5
.=(Pj('not' a1,z) '&' Pj('not' b1,z) '&' Pj('not' c1,z)) '&'
(Pj(a1,z) 'or' Pj(b1,z) 'or' Pj(c1,z))
by VALUAT_1:def 5
.=(Pj('not' a1,z) '&' Pj('not' b1,z) '&' Pj('not' c1,z)) '&'
(Pj(a1 'or' b1,z) 'or' Pj(c1,z))
by BVFUNC_1:def 7
.=(Pj('not' a1,z) '&' Pj('not' b1,z) '&' Pj('not' c1,z)) '&'
(Pj(a1 'or' b1 'or' c1,z))
by BVFUNC_1:def 7
.=(Pj('not' a1 '&' 'not' b1,z) '&' Pj('not' c1,z)) '&'
(Pj(a1 'or' b1 'or' c1,z))
by VALUAT_1:def 6
.=(Pj('not' a1 '&' 'not' b1 '&' 'not' c1,z)) '&' (Pj(a1 'or' b1 'or' c1,z))
by VALUAT_1:def 6
.=Pj(('not' a1 '&' 'not' b1 '&' 'not' c1) '&' (a1 'or' b1 'or' c1),z)
by VALUAT_1:def 6;
('not' a1 '&' 'not' b1 '&' 'not' c1) '&' (a1 'or' b1 'or' c1)
=('not' a1 '&' 'not' b1 '&' 'not' c1) '&' (a1 'or' b1) 'or'
('not' a1 '&' 'not' b1 '&' 'not' c1) '&' c1 by BVFUNC_1:15
.=('not' a1 '&' 'not' b1 '&' 'not' c1) '&' (a1 'or' b1) 'or'
('not' a1 '&' 'not' b1 '&' ('not' c1 '&' c1)) by BVFUNC_1:7
.=('not' a1 '&' 'not' b1 '&' 'not' c1) '&' (a1 'or' b1) 'or'
('not' a1 '&' 'not' b1 '&' O_el(Y)) by BVFUNC_4:5
.=('not' a1 '&' 'not' b1 '&' 'not' c1) '&' (a1 'or' b1) 'or'
O_el(Y) by BVFUNC_1:8
.=('not' a1 '&' 'not' b1 '&' 'not' c1) '&' (a1 'or' b1)
by BVFUNC_1:12
.=('not' a1 '&' 'not' b1 '&' 'not' c1) '&' a1 'or'
('not' a1 '&' 'not' b1 '&' 'not' c1) '&' b1
by BVFUNC_1:15
.=('not' a1 '&' 'not' b1 '&' 'not' c1) '&' a1 'or'
'not' a1 '&' 'not' c1 '&' 'not' b1 '&' b1
by BVFUNC_1:7
.=('not' a1 '&' 'not' b1 '&' 'not' c1) '&' a1 'or'
'not' a1 '&' 'not' c1 '&' ('not' b1 '&' b1)
by BVFUNC_1:7
.=('not' a1 '&' 'not' b1 '&' 'not' c1) '&' a1 'or'
'not' a1 '&' 'not' c1 '&' O_el(Y)
by BVFUNC_4:5
.=('not' a1 '&' 'not' b1 '&' 'not' c1) '&' a1 'or'
O_el(Y)
by BVFUNC_1:8
.=('not' a1 '&' 'not' b1 '&' 'not' c1) '&' a1
by BVFUNC_1:12
.='not' b1 '&' 'not' c1 '&' 'not' a1 '&' a1
by BVFUNC_1:7
.='not' b1 '&' 'not' c1 '&' ('not' a1 '&' a1)
by BVFUNC_1:7
.='not' b1 '&' 'not' c1 '&' O_el(Y)
by BVFUNC_4:5
.=O_el(Y) by BVFUNC_1:8;
then Pj((a1 'imp' a2) '&' (b1 'imp' b2) '&' (c1 'imp' c2) '&'
(a1 'or' b1 'or' c1),z)
=FALSE by A2,A8,BVFUNC_1:def 13;
hence contradiction by A1,MARGREL1:43;
end;
hence thesis;
end;
Lm3: 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
let a1,a2,b1,b2 be Element of Funcs(Y,BOOLEAN);
let z be Element of Y;
assume A1:
Pj((a1 'imp' b1) '&' (a2 'imp' b2) '&' (a1 'or' a2) '&'
'not'( b1 '&' b2),z)=TRUE;
A2: Pj((a1 'imp' b1) '&' (a2 'imp' b2) '&' (a1 'or' a2) '&'
'not'( b1 '&' b2),z)
=Pj(('not' a1 'or' b1) '&' (a2 'imp' b2) '&' (a1 'or' a2) '&' 'not'
(b1 '&' b2),z)
by BVFUNC_4:8
.=Pj(('not' a1 'or' b1) '&' ('not' a2 'or' b2) '&' (a1 'or' a2) '&' 'not'
(b1 '&' b2),z)
by BVFUNC_4:8
.=Pj(('not' a1 'or' b1) '&' ('not' a2 'or' b2) '&' (a1 'or' a2),z) '&'
Pj('not'( b1 '&' b2),z)
by VALUAT_1:def 6
.=Pj(('not' a1 'or' b1) '&' ('not' a2 'or' b2),z) '&'
Pj(a1 'or' a2,z) '&' Pj('not'( b1 '&' b2),z)
by VALUAT_1:def 6
.=Pj(('not' a1 'or' b1) '&' ('not' a2 'or' b2),z) '&'
Pj(a1 'or' a2,z) '&' Pj('not' b1 'or' 'not' b2,z)
by BVFUNC_1:17
.=Pj('not' a1 'or' b1,z) '&' Pj('not' a2 'or' b2,z) '&'
Pj(a1 'or' a2,z) '&' Pj('not' b1 'or' 'not' b2,z)
by VALUAT_1:def 6
.=(Pj('not' a1,z) 'or' Pj(b1,z)) '&' Pj('not' a2 'or' b2,z) '&'
Pj(a1 'or' a2,z) '&' Pj('not' b1 'or' 'not' b2,z)
by BVFUNC_1:def 7
.=(Pj('not' a1,z) 'or' Pj(b1,z)) '&' (Pj('not' a2,z) 'or' Pj(b2,z)) '&'
Pj(a1 'or' a2,z) '&' Pj('not' b1 'or' 'not' b2,z)
by BVFUNC_1:def 7
.=(Pj('not' a1,z) 'or' Pj(b1,z)) '&' (Pj('not' a2,z) 'or' Pj(b2,z)) '&'
(Pj(a1,z) 'or' Pj(a2,z)) '&' Pj('not' b1 'or' 'not' b2,z)
by BVFUNC_1:def 7
.=(Pj('not' a1,z) 'or' Pj(b1,z)) '&' (Pj('not' a2,z) 'or' Pj(b2,z)) '&'
(Pj(a1,z) 'or' Pj(a2,z)) '&' (Pj('not' b1,z) 'or' Pj('not' b2,z))
by BVFUNC_1:def 7
.=('not' Pj(a1,z) 'or' Pj(b1,z)) '&' (Pj('not' a2,z) 'or' Pj(b2,z)) '&'
(Pj(a1,z) 'or' Pj(a2,z)) '&' (Pj('not' b1,z) 'or' Pj('not' b2,z))
by VALUAT_1:def 5
.=('not' Pj(a1,z) 'or' Pj(b1,z)) '&' ('not' Pj(a2,z) 'or' Pj(b2,z)) '&'
(Pj(a1,z) 'or' Pj(a2,z)) '&' (Pj('not' b1,z) 'or' Pj('not' b2,z))
by VALUAT_1:def 5
.=('not' Pj(a1,z) 'or' Pj(b1,z)) '&' ('not' Pj(a2,z) 'or' Pj(b2,z)) '&'
(Pj(a1,z) 'or' Pj(a2,z)) '&' ('not' Pj(b1,z) 'or' Pj('not' b2,z))
by VALUAT_1:def 5
.=('not' Pj(a1,z) 'or' Pj(b1,z)) '&' ('not' Pj(a2,z) 'or' Pj(b2,z)) '&'
(Pj(a1,z) 'or' Pj(a2,z)) '&' ('not' Pj(b1,z) 'or' 'not' Pj(b2,z))
by VALUAT_1:def 5;
now assume A3: Pj((b1 'imp' a1) '&' (b2 'imp' a2) '&' (b1 'or' b2) '&'
'not'( a1 '&' a2),z)<>TRUE;
Pj((b1 'imp' a1) '&' (b2 'imp' a2) '&' (b1 'or' b2) '&'
'not'( a1 '&' a2),z)
=Pj(('not' b1 'or' a1) '&' (b2 'imp' a2) '&' (b1 'or' b2) '&' 'not'
(a1 '&' a2),z)
by BVFUNC_4:8
.=Pj(('not' b1 'or' a1) '&' ('not' b2 'or' a2) '&' (b1 'or' b2) '&' 'not'
(a1 '&' a2),z) by BVFUNC_4:8
.=Pj(('not' b1 'or' a1) '&' ('not' b2 'or' a2) '&' (b1 'or' b2),z) '&'
Pj('not'( a1 '&' a2),z) by VALUAT_1:def 6
.=Pj(('not' b1 'or' a1) '&' ('not' b2 'or' a2),z) '&' Pj(b1 'or' b2,z) '&'
Pj('not'( a1 '&' a2),z) by VALUAT_1:def 6
.=Pj('not' b1 'or' a1,z) '&' Pj('not' b2 'or' a2,z) '&' Pj(b1 'or' b2,z) '&'
Pj('not'( a1 '&' a2),z)
by VALUAT_1:def 6
.=Pj('not' b1 'or' a1,z) '&' Pj('not' b2 'or' a2,z) '&' Pj(b1 'or' b2,z) '&'
Pj(('not' a1 'or' 'not' a2),z)
by BVFUNC_1:17
.=(Pj('not' b1,z) 'or' Pj(a1,z)) '&' Pj('not'
b2 'or' a2,z) '&' Pj(b1 'or' b2,z) '&'
Pj(('not' a1 'or' 'not' a2),z)
by BVFUNC_1:def 7
.=(Pj('not' b1,z) 'or' Pj(a1,z)) '&' (Pj('not' b2,z) 'or' Pj(a2,z)) '&'
Pj(b1 'or' b2,z) '&' Pj(('not' a1 'or' 'not' a2),z)
by BVFUNC_1:def 7
.=(Pj('not' b1,z) 'or' Pj(a1,z)) '&' (Pj('not' b2,z) 'or' Pj(a2,z)) '&'
(Pj(b1,z) 'or' Pj(b2,z)) '&' Pj(('not' a1 'or' 'not' a2),z)
by BVFUNC_1:def 7
.=(Pj('not' b1,z) 'or' Pj(a1,z)) '&' (Pj('not' b2,z) 'or' Pj(a2,z)) '&'
(Pj(b1,z) 'or' Pj(b2,z)) '&' (Pj('not' a1,z) 'or' Pj('not' a2,z))
by BVFUNC_1:def 7;
then A4: (Pj('not' b1,z) 'or' Pj(a1,z)) '&' (Pj('not' b2,z) 'or' Pj(a2,z)) '&'
(Pj(b1,z) 'or' Pj(b2,z)) '&' (Pj('not' a1,z) 'or' Pj('not'
a2,z))=FALSE by A3,MARGREL1:43;
now per cases by A4,MARGREL1:45;
case A5: (Pj('not' b1,z) 'or' Pj(a1,z)) '&' (Pj('not' b2,z) 'or' Pj(a2,z))
'&'
(Pj(b1,z) 'or' Pj(b2,z))=FALSE;
now per cases by A5,MARGREL1:45;
case A6: (Pj('not' b1,z) 'or' Pj(a1,z)) '&' (Pj('not'
b2,z) 'or' Pj(a2,z))=FALSE;
now per cases by A6,MARGREL1:45;
case A7:(Pj('not' b1,z) 'or' Pj(a1,z))=FALSE;
A8:Pj('not' b1,z)=TRUE or Pj('not' b1,z)=FALSE by MARGREL1:39;
Pj(a1,z)=TRUE or Pj(a1,z)=FALSE by MARGREL1:39;
then A9: Pj('not' b1,z)=FALSE & Pj(a1,z)=FALSE by A7,A8,BINARITH:19;
then 'not' Pj(b1,z)=FALSE by VALUAT_1:def 5;
then Pj(b1,z)=TRUE by MARGREL1:41;
then ('not' Pj(a1,z) 'or' Pj(b1,z)) '&' ('not' Pj(a2,z) 'or' Pj(b2,z))
'&'
(Pj(a1,z) 'or' Pj(a2,z)) '&' ('not' Pj(b1,z) 'or' 'not' Pj(b2,z))
=(TRUE 'or' TRUE) '&' ('not' Pj(a2,z) 'or' Pj(b2,z)) '&'
(FALSE 'or' Pj(a2,z)) '&' ('not' TRUE 'or' 'not'
Pj(b2,z)) by A9,MARGREL1:41
.=(TRUE 'or' TRUE) '&' ('not' Pj(a2,z) 'or' Pj(b2,z)) '&'
(FALSE 'or' Pj(a2,z)) '&' (FALSE 'or' 'not' Pj(b2,z)) by MARGREL1:41
.=TRUE '&' ('not' Pj(a2,z) 'or' Pj(b2,z)) '&'
(FALSE 'or' Pj(a2,z)) '&' (FALSE 'or' 'not' Pj(b2,z)) by BINARITH:19
.=TRUE '&' ('not' Pj(a2,z) 'or' Pj(b2,z)) '&'
Pj(a2,z) '&' (FALSE 'or' 'not' Pj(b2,z)) by BINARITH:7
.=TRUE '&' ('not' Pj(a2,z) 'or' Pj(b2,z)) '&'
Pj(a2,z) '&' 'not' Pj(b2,z) by BINARITH:7
.=Pj(a2,z) '&' ('not' Pj(a2,z) 'or' Pj(b2,z))
'&' 'not' Pj(b2,z) by MARGREL1:50
.=(Pj(a2,z) '&' 'not' Pj(a2,z) 'or' Pj(a2,z) '&' Pj(b2,z))
'&' 'not' Pj(b2,z) by BINARITH:22
.=(FALSE 'or' Pj(a2,z) '&' Pj(b2,z))
'&' 'not' Pj(b2,z) by MARGREL1:46
.=(Pj(a2,z) '&' Pj(b2,z)) '&' 'not' Pj(b2,z) by BINARITH:7
.=Pj(a2,z) '&' (Pj(b2,z) '&' 'not' Pj(b2,z)) by MARGREL1:52
.=FALSE '&' Pj(a2,z) by MARGREL1:46
.=FALSE by MARGREL1:49;
hence thesis by A1,A2,MARGREL1:43;
case A10:(Pj('not' b2,z) 'or' Pj(a2,z))=FALSE;
A11:Pj('not' b2,z)=TRUE or Pj('not' b2,z)=FALSE by MARGREL1:39;
Pj(a2,z)=TRUE or Pj(a2,z)=FALSE by MARGREL1:39;
then A12: Pj('not' b2,z)=FALSE & Pj(a2,z)=FALSE by A10,A11,BINARITH:19;
then 'not' Pj(b2,z)=FALSE by VALUAT_1:def 5;
then Pj(b2,z)=TRUE by MARGREL1:41;
then ('not' Pj(a1,z) 'or' Pj(b1,z)) '&' ('not' Pj(a2,z) 'or' Pj(b2,z))
'&'
(Pj(a1,z) 'or' Pj(a2,z)) '&' ('not' Pj(b1,z) 'or' 'not' Pj(b2,z))
=('not' Pj(a1,z) 'or' Pj(b1,z)) '&' (TRUE 'or' TRUE) '&'
(Pj(a1,z) 'or' FALSE) '&' ('not' Pj(b1,z) 'or' 'not'
TRUE) by A12,MARGREL1:41
.=('not' Pj(a1,z) 'or' Pj(b1,z)) '&' (TRUE 'or' TRUE) '&'
(Pj(a1,z) 'or' FALSE) '&' ('not' Pj(b1,z) 'or' FALSE) by MARGREL1:41
.=('not' Pj(a1,z) 'or' Pj(b1,z)) '&' TRUE '&'
(Pj(a1,z) 'or' FALSE) '&' ('not' Pj(b1,z) 'or' FALSE) by BINARITH:19
.=('not' Pj(a1,z) 'or' Pj(b1,z)) '&' TRUE '&'
Pj(a1,z) '&' ('not' Pj(b1,z) 'or' FALSE) by BINARITH:7
.=TRUE '&' ('not' Pj(a1,z) 'or' Pj(b1,z)) '&'
Pj(a1,z) '&' 'not' Pj(b1,z) by BINARITH:7
.=Pj(a1,z) '&' ('not' Pj(a1,z) 'or' Pj(b1,z)) '&'
'not' Pj(b1,z) by MARGREL1:50
.=(Pj(a1,z) '&' 'not' Pj(a1,z) 'or' Pj(a1,z) '&' Pj(b1,z)) '&'
'not' Pj(b1,z) by BINARITH:22
.=(FALSE 'or' Pj(a1,z) '&' Pj(b1,z)) '&'
'not' Pj(b1,z) by MARGREL1:46
.=(Pj(a1,z) '&' Pj(b1,z)) '&'
'not' Pj(b1,z) by BINARITH:7
.=Pj(a1,z) '&' (Pj(b1,z) '&' 'not' Pj(b1,z)) by MARGREL1:52
.=FALSE '&' Pj(a1,z) by MARGREL1:46
.=FALSE by MARGREL1:49;
hence thesis by A1,A2,MARGREL1:43;
end;
hence thesis;
case A13:(Pj(b1,z) 'or' Pj(b2,z))=FALSE;
A14:Pj(b2,z)=TRUE or Pj(b2,z)=FALSE by MARGREL1:39;
Pj(b1,z)=TRUE or Pj(b1,z)=FALSE by MARGREL1:39;
then Pj(b1,z)=FALSE & Pj(b2,z)=FALSE by A13,A14,BINARITH:19;
then ('not' Pj(a1,z) 'or' Pj(b1,z)) '&' ('not' Pj(a2,z) 'or' Pj(b2,z))
'&'
(Pj(a1,z) 'or' Pj(a2,z)) '&' ('not' Pj(b1,z) 'or' 'not' Pj(b2,z))
=('not' Pj(a1,z) 'or' FALSE) '&' ('not' Pj(a2,z) 'or' FALSE) '&'
(Pj(a1,z) 'or' Pj(a2,z)) '&' (TRUE 'or' 'not' FALSE) by MARGREL1:41
.=('not' Pj(a1,z) 'or' FALSE) '&' ('not' Pj(a2,z) 'or' FALSE) '&'
(Pj(a1,z) 'or' Pj(a2,z)) '&' TRUE by BINARITH:19
.='not' Pj(a1,z) '&' ('not' Pj(a2,z) 'or' FALSE) '&'
(Pj(a1,z) 'or' Pj(a2,z)) '&' TRUE by BINARITH:7
.=TRUE '&' ('not' Pj(a1,z) '&' 'not' Pj(a2,z) '&'
(Pj(a1,z) 'or' Pj(a2,z))) by BINARITH:7
.='not' Pj(a1,z) '&' 'not' Pj(a2,z) '&'
(Pj(a1,z) 'or' Pj(a2,z)) by MARGREL1:50
.='not' Pj(a1,z) '&'
('not' Pj(a2,z) '&' (Pj(a1,z) 'or' Pj(a2,z)))
by MARGREL1:52
.='not' Pj(a1,z) '&'
('not' Pj(a2,z) '&' Pj(a1,z) 'or' 'not' Pj(a2,z) '&' Pj(a2,z))
by BINARITH:22
.='not' Pj(a1,z) '&'
('not' Pj(a2,z) '&' Pj(a1,z) 'or' FALSE)
by MARGREL1:46
.='not' Pj(a1,z) '&' (Pj(a1,z) '&' 'not' Pj(a2,z)) by BINARITH:7
.='not' Pj(a1,z) '&' Pj(a1,z) '&' 'not' Pj(a2,z)
by MARGREL1:52
.=FALSE '&' 'not' Pj(a2,z)
by MARGREL1:46
.=FALSE by MARGREL1:49;
hence thesis by A1,A2,MARGREL1:43;
end;
hence thesis;
case A15:(Pj('not' a1,z) 'or' Pj('not' a2,z))=FALSE;
A16:Pj('not' a1,z)=TRUE or Pj('not' a1,z)=FALSE by MARGREL1:39;
Pj('not' a2,z)=TRUE or Pj('not' a2,z)=FALSE by MARGREL1:39;
then A17: Pj('not' a1,z)=FALSE & Pj('not' a2,z)=FALSE by A15,A16,BINARITH:19
;
then A18: 'not' Pj(a1,z)=FALSE by VALUAT_1:def 5;
'not' Pj(a2,z)=FALSE by A17,VALUAT_1:def 5;
then Pj(a2,z)=TRUE by MARGREL1:41;
then ('not' Pj(a1,z) 'or' Pj(b1,z)) '&' ('not' Pj(a2,z) 'or' Pj(b2,z))
'&'
(Pj(a1,z) 'or' Pj(a2,z)) '&' ('not' Pj(b1,z) 'or' 'not' Pj(b2,z))
=(FALSE 'or' Pj(b1,z)) '&' ('not' TRUE 'or' Pj(b2,z)) '&'
(TRUE 'or' TRUE) '&' ('not' Pj(b1,z) 'or' 'not'
Pj(b2,z)) by A18,MARGREL1:41
.=(FALSE 'or' Pj(b1,z)) '&' (FALSE 'or' Pj(b2,z)) '&'
(TRUE 'or' TRUE) '&' ('not' Pj(b1,z) 'or' 'not' Pj(b2,z))
by MARGREL1:41
.=(FALSE 'or' Pj(b1,z)) '&' (FALSE 'or' Pj(b2,z)) '&'
TRUE '&' ('not' Pj(b1,z) 'or' 'not' Pj(b2,z)) by BINARITH:19
.=Pj(b1,z) '&' (FALSE 'or' Pj(b2,z)) '&'
TRUE '&' ('not' Pj(b1,z) 'or' 'not' Pj(b2,z)) by BINARITH:7
.=TRUE '&' (Pj(b1,z) '&' Pj(b2,z)) '&'
('not' Pj(b1,z) 'or' 'not' Pj(b2,z)) by BINARITH:7
.=Pj(b1,z) '&' Pj(b2,z) '&'
('not' Pj(b1,z) 'or' 'not' Pj(b2,z)) by MARGREL1:50
.=Pj(b1,z) '&' (Pj(b2,z) '&'
('not' Pj(b1,z) 'or' 'not' Pj(b2,z))) by MARGREL1:52
.=Pj(b1,z) '&'
(Pj(b2,z) '&' 'not' Pj(b1,z) 'or' Pj(b2,z) '&' 'not'
Pj(b2,z)) by BINARITH:22
.=Pj(b1,z) '&'
(Pj(b2,z) '&' 'not' Pj(b1,z) 'or' FALSE) by MARGREL1:46
.=Pj(b1,z) '&' ('not' Pj(b1,z) '&' Pj(b2,z)) by BINARITH:7
.=Pj(b1,z) '&' 'not' Pj(b1,z) '&' Pj(b2,z) by MARGREL1:52
.=FALSE '&' Pj(b2,z) by MARGREL1:46
.=FALSE by MARGREL1:49;
hence thesis by A1,A2,MARGREL1:43;
end;
hence thesis;
end;
hence thesis;
end;
theorem 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
let a1,a2,b1,b2 be Element of Funcs(Y,BOOLEAN);
A1:(a1 'imp' b1) '&' (a2 'imp' b2) '&' (a1 'or' a2) '&' 'not'( b1 '&' b2) '<'
(b1 'imp' a1) '&' (b2 'imp' a2) '&' (b1 'or' b2) '&' 'not'( a1 '&' a2)
by Lm3;
(b1 'imp' a1) '&' (b2 'imp' a2) '&' (b1 'or' b2) '&' 'not'( a1 '&' a2) '<'
(a1 'imp' b1) '&' (a2 'imp' b2) '&' (a1 'or' a2) '&' 'not'( b1 '&' b2)
by Lm3;
hence thesis by A1,BVFUNC_1:18;
end;
theorem 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
let a,b,c,d be Element of Funcs(Y,BOOLEAN);
(a 'or' b) '&' (c 'or' d)
=((a 'or' b) '&' c) 'or' ((a 'or' b) '&' d) by BVFUNC_1:15
.=(a '&' c) 'or' (b '&' c) 'or' ((a 'or' b) '&' d) by BVFUNC_1:15
.=(a '&' c) 'or' (b '&' c) 'or' ((a '&' d) 'or' (b '&' d)) by BVFUNC_1:15
.=(a '&' c) 'or' (b '&' c) 'or' (a '&' d) 'or' (b '&' d) by BVFUNC_1:11
.=(a '&' c) 'or' (a '&' d) 'or' (b '&' c) 'or' (b '&' d) by BVFUNC_1:11;
hence thesis;
end;
theorem 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
let a1,a2,b1,b2,b3 be Element of Funcs(Y,BOOLEAN);
(a1 'or' b1) '&' (a1 'or' b2) '&' (a1 'or' b3) '&'
(a2 'or' b1) '&' (a2 'or' b2) '&' (a2 'or' b3)
=(a1 'or' (b1 '&' b2)) '&' (a1 'or' b3) '&'
(a2 'or' b1) '&' (a2 'or' b2) '&' (a2 'or' b3) by BVFUNC_1:14
.=(a1 'or' (b1 '&' b2 '&' b3)) '&'
(a2 'or' b1) '&' (a2 'or' b2) '&' (a2 'or' b3) by BVFUNC_1:14
.=(a1 'or' (b1 '&' b2 '&' b3)) '&'
((a2 'or' b1) '&' (a2 'or' b2)) '&' (a2 'or' b3) by BVFUNC_1:7
.=(a1 'or' (b1 '&' b2 '&' b3)) '&'
(((a2 'or' b1) '&' (a2 'or' b2)) '&' (a2 'or' b3)) by BVFUNC_1:7
.=(a1 'or' (b1 '&' b2 '&' b3)) '&'
((a2 'or' (b1 '&' b2)) '&' (a2 'or' b3)) by BVFUNC_1:14
.=(a1 'or' (b1 '&' b2 '&' b3)) '&'
(a2 'or' (b1 '&' b2 '&' b3)) by BVFUNC_1:14
.=(a1 '&' a2) 'or' (b1 '&' b2 '&' b3) by BVFUNC_1:14;
hence thesis;
end;
theorem 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
let a,b,c,d be Element of Funcs(Y,BOOLEAN);
A1:(a 'imp' (b '&' c '&' d)) '&' (b 'imp' (c '&' d)) '&' (c 'imp' d)
=('not' a 'or' (b '&' c '&' d)) '&' (b 'imp' (c '&' d)) '&' (c 'imp' d)
by BVFUNC_4:8
.=('not' a 'or' (b '&' c '&' d)) '&' ('not' b 'or' (c '&' d)) '&' (c 'imp' d)
by BVFUNC_4:8
.=('not' a 'or' (b '&' c '&' d)) '&' ('not' b 'or'
(c '&' d)) '&' ('not' c 'or' d) by BVFUNC_4:8
.=(('not' a 'or' b) '&' ('not' a 'or' c) '&' ('not' a 'or' d))
'&' ('not' b 'or' (c '&' d)) '&' ('not' c 'or' d) by BVFUNC_5:40
.=(('not' a 'or' b) '&' ('not' a 'or' c) '&' ('not' a 'or' d))
'&' (('not' b 'or' c) '&' ('not' b 'or' d)) '&' ('not' c 'or' d)
by BVFUNC_1:14
.=('not' a 'or' b) '&' ('not' a 'or' c) '&' ('not' a 'or' d) '&'
('not' b 'or' c) '&' ('not' b 'or' d) '&' ('not' c 'or' d) by BVFUNC_1:7
.=('not' a 'or' b) '&' ('not' a 'or' c) '&' ('not' b 'or' c) '&'
('not' a 'or' d) '&' ('not' b 'or' d) '&' ('not' c 'or' d) by BVFUNC_1:7
.=('not' a 'or' b) '&' ('not' b 'or' c) '&' ('not' a 'or' c) '&'
('not' a 'or' d) '&' ('not' b 'or' d) '&' ('not' c 'or' d) by BVFUNC_1:7
.=('not' a 'or' b) '&' ('not' b 'or' c) '&' ('not' a 'or' c) '&'
('not' a 'or' d) '&' ('not' c 'or' d) '&' ('not' b 'or' d) by BVFUNC_1:7
.=('not' a 'or' b) '&' ('not' b 'or' c) '&' ('not' a 'or' c) '&'
('not' c 'or' d) '&' ('not' a 'or' d) '&' ('not' b 'or' d) by BVFUNC_1:7
.=('not' a 'or' b) '&' ('not' b 'or' c) '&' ('not' c 'or' d) '&'
('not' a 'or' c) '&' ('not' a 'or' d) '&' ('not' b 'or' d) by BVFUNC_1:7
.=(a 'imp' b) '&' ('not' b 'or' c) '&' ('not' c 'or' d) '&'
('not' a 'or' c) '&' ('not' a 'or' d) '&' ('not' b 'or' d) by BVFUNC_4:8
.=(a 'imp' b) '&' (b 'imp' c) '&' ('not' c 'or' d) '&'
('not' a 'or' c) '&' ('not' a 'or' d) '&' ('not' b 'or' d) by BVFUNC_4:8
.=(a 'imp' b) '&' (b 'imp' c) '&' (c 'imp' d) '&'
('not' a 'or' c) '&' ('not' a 'or' d) '&' ('not' b 'or' d) by BVFUNC_4:8
.=(a 'imp' b) '&' (b 'imp' c) '&' (c 'imp' d) '&'
(a 'imp' c) '&' ('not' a 'or' d) '&' ('not' b 'or' d) by BVFUNC_4:8
.=(a 'imp' b) '&' (b 'imp' c) '&' (c 'imp' d) '&'
(a 'imp' c) '&' (a 'imp' d) '&' ('not' b 'or' d) by BVFUNC_4:8
.=(a 'imp' b) '&' (b 'imp' c) '&' (c 'imp' d) '&'
(a 'imp' c) '&' (a 'imp' d) '&' (b 'imp' d) by BVFUNC_4:8;
(a 'imp' b) '&' (b 'imp' c) '&' (c 'imp' d)
=(a 'imp' b) '&' (b 'imp' c) '&' (a 'imp' c) '&' (c 'imp' d)
by BVFUNC_7:12
.=(a 'imp' b) '&' (b 'imp' c) '&' ((a 'imp' c) '&' (c 'imp' d))
by BVFUNC_1:7
.=(a 'imp' b) '&' (b 'imp' c) '&' ((a 'imp' c) '&'
(c 'imp' d) '&' (a 'imp' d))
by BVFUNC_7:12
.=(a 'imp' b) '&' (b 'imp' c) '&' ((a 'imp' c) '&'
(c 'imp' d)) '&' (a 'imp' d)
by BVFUNC_1:7
.=(a 'imp' b) '&' (b 'imp' c) '&' (c 'imp' d) '&'
(a 'imp' c) '&' (a 'imp' d)
by BVFUNC_1:7
.=(a 'imp' b) '&' ((b 'imp' c) '&' (c 'imp' d)) '&'
(a 'imp' c) '&' (a 'imp' d)
by BVFUNC_1:7
.=(a 'imp' b) '&' (((b 'imp' c) '&' (c 'imp' d)) '&' (b 'imp' d)) '&'
(a 'imp' c) '&' (a 'imp' d)
by BVFUNC_7:12
.=(a 'imp' b) '&' ((b 'imp' c) '&' (c 'imp' d)) '&' (b 'imp' d) '&'
(a 'imp' c) '&' (a 'imp' d)
by BVFUNC_1:7
.=(a 'imp' b) '&' (b 'imp' c) '&' (c 'imp' d) '&' (b 'imp' d) '&'
(a 'imp' c) '&' (a 'imp' d)
by BVFUNC_1:7
.=(a 'imp' b) '&' (b 'imp' c) '&' (c 'imp' d) '&' (a 'imp' c) '&'
(b 'imp' d) '&' (a 'imp' d)
by BVFUNC_1:7
.=(a 'imp' b) '&' (b 'imp' c) '&' (c 'imp' d) '&' (a 'imp' c) '&'
(a 'imp' d) '&' (b 'imp' d)
by BVFUNC_1:7;
hence thesis by A1;
end;
theorem 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
let a,b,c,d be Element of Funcs(Y,BOOLEAN);
let z be Element of Y;
assume A1:
Pj((a 'imp' c) '&' (b 'imp' d) '&' (a 'or' b),z)=TRUE;
A2: Pj((a 'imp' c) '&' (b 'imp' d) '&' (a 'or' b),z)
=Pj((a 'imp' c) '&' (b 'imp' d),z) '&' Pj(a 'or' b,z) by VALUAT_1:def 6
.=Pj(a 'imp' c,z) '&' Pj(b 'imp' d,z) '&' Pj(a 'or' b,z) by VALUAT_1:def 6
.=Pj('not' a 'or' c,z) '&' Pj(b 'imp' d,z) '&' Pj(a 'or' b,z) by BVFUNC_4:8
.=Pj('not' a 'or' c,z) '&' Pj('not'
b 'or' d,z) '&' Pj(a 'or' b,z) by BVFUNC_4:8
.=(Pj('not' a,z) 'or' Pj(c,z)) '&' Pj('not' b 'or' d,z) '&'
Pj(a 'or' b,z) by BVFUNC_1:def 7
.=(Pj('not' a,z) 'or' Pj(c,z)) '&' (Pj('not' b,z) 'or' Pj(d,z)) '&'
Pj(a 'or' b,z) by BVFUNC_1:def 7
.=(Pj('not' a,z) 'or' Pj(c,z)) '&' (Pj('not' b,z) 'or' Pj(d,z)) '&'
(Pj(a,z) 'or' Pj(b,z)) by BVFUNC_1:def 7
.=('not' Pj(a,z) 'or' Pj(c,z)) '&' (Pj('not' b,z) 'or' Pj(d,z)) '&'
(Pj(a,z) 'or' Pj(b,z)) by VALUAT_1:def 5
.=('not' Pj(a,z) 'or' Pj(c,z)) '&' ('not' Pj(b,z) 'or' Pj(d,z)) '&'
(Pj(a,z) 'or' Pj(b,z)) by VALUAT_1:def 5;
now assume
Pj(c 'or' d,z)<>TRUE;
then Pj(c 'or' d,z)=FALSE by MARGREL1:43;
then A3: Pj(c,z) 'or' Pj(d,z)=FALSE by BVFUNC_1:def 7;
A4:Pj(c,z)=TRUE or Pj(c,z)=FALSE by MARGREL1:39;
Pj(d,z)=TRUE or Pj(d,z)=FALSE by MARGREL1:39;
then Pj(c,z)=FALSE & Pj(d,z)=FALSE by A3,A4,BINARITH:19;
then ('not' Pj(a,z) 'or' Pj(c,z)) '&' ('not' Pj(b,z) 'or' Pj(d,z)) '&'
(Pj(a,z) 'or' Pj(b,z))
='not' Pj(a,z) '&' ('not' Pj(b,z) 'or' FALSE) '&'
(Pj(a,z) 'or' Pj(b,z)) by BINARITH:7
.='not' Pj(a,z) '&' 'not' Pj(b,z) '&'
(Pj(b,z) 'or' Pj(a,z)) by BINARITH:7
.='not' Pj(a,z) '&' ('not' Pj(b,z) '&'
(Pj(b,z) 'or' Pj(a,z))) by MARGREL1:52
.='not' Pj(a,z) '&' (
('not' Pj(b,z) '&' Pj(b,z) 'or' 'not' Pj(b,z) '&' Pj(a,z)))
by BINARITH:22
.='not' Pj(a,z) '&' (
(FALSE 'or' 'not' Pj(b,z) '&' Pj(a,z))) by MARGREL1:46
.='not' Pj(a,z) '&' (Pj(a,z) '&' 'not' Pj(b,z)) by BINARITH:7
.='not' Pj(a,z) '&' Pj(a,z) '&' 'not' Pj(b,z) by MARGREL1:52
.=FALSE '&' 'not' Pj(b,z) by MARGREL1:46
.=FALSE by MARGREL1:49;
hence thesis by A1,A2,MARGREL1:43;
end;
hence thesis;
end;
theorem for a,b,c being Element of Funcs(Y,BOOLEAN) holds
((a '&' b) 'imp' 'not' c) '&' a '&' c '<' 'not' b
proof
let a,b,c be Element of Funcs(Y,BOOLEAN);
let z be Element of Y;
assume A1:
Pj(((a '&' b) 'imp' 'not' c) '&' a '&' c,z)=TRUE;
A2: Pj(((a '&' b) 'imp' 'not' c) '&' a '&' c,z)
=Pj(((a '&' b) 'imp' 'not' c) '&' a,z) '&' Pj(c,z) by VALUAT_1:def 6
.=Pj((a '&' b) 'imp' 'not' c,z) '&' Pj(a,z) '&' Pj(c,z) by VALUAT_1:def 6
.=Pj('not'( a '&' b) 'or' 'not' c,z) '&' Pj(a,z) '&' Pj(c,z) by BVFUNC_4:8
.=Pj(('not' a 'or' 'not' b) 'or' 'not'
c,z) '&' Pj(a,z) '&' Pj(c,z) by BVFUNC_1:17
.=(Pj('not' a 'or' 'not' b,z) 'or' Pj('not'
c,z)) '&' Pj(a,z) '&' Pj(c,z) by BVFUNC_1:def 7
.=((Pj('not' a,z) 'or' Pj('not' b,z)) 'or' Pj('not' c,z)) '&'
Pj(a,z) '&' Pj(c,z) by BVFUNC_1:def 7;
now assume Pj('not' b,z)<>TRUE;
then Pj('not' b,z)=FALSE by MARGREL1:43;
then ((Pj('not' a,z) 'or' Pj('not' b,z)) 'or' Pj('not' c,z)) '&'
Pj(a,z) '&' Pj(c,z)
=(Pj('not' a,z) 'or' Pj('not' c,z)) '&'
Pj(a,z) '&' Pj(c,z) by BINARITH:7
.=('not' Pj(a,z) 'or' Pj('not' c,z)) '&'
Pj(a,z) '&' Pj(c,z) by VALUAT_1:def 5
.=Pj(a,z) '&' ('not' Pj(a,z) 'or' 'not' Pj(c,z)) '&'
Pj(c,z) by VALUAT_1:def 5
.=(Pj(a,z) '&' 'not' Pj(a,z) 'or' Pj(a,z) '&' 'not' Pj(c,z)) '&'
Pj(c,z) by BINARITH:22
.=(FALSE 'or' Pj(a,z) '&' 'not' Pj(c,z)) '&'
Pj(c,z) by MARGREL1:46
.=(Pj(a,z) '&' 'not' Pj(c,z)) '&'
Pj(c,z) by BINARITH:7
.=Pj(a,z) '&' ('not' Pj(c,z) '&' Pj(c,z)) by MARGREL1:52
.=FALSE '&' Pj(a,z) by MARGREL1:46
.=FALSE by MARGREL1:49;
hence thesis by A1,A2,MARGREL1:43;
end;
hence thesis;
end;
theorem 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
let a1,a2,a3,b1,b2,b3 be Element of Funcs(Y,BOOLEAN);
('not' b1 '&' 'not' b2 '&' a3) 'imp' ('not' a1 'or' 'not' a2 'or' b3)
='not'( 'not' b1 '&' 'not' b2 '&' a3) 'or' ('not' a1 'or' 'not'
a2 'or' b3) by BVFUNC_4:8
.=('not' 'not' b1 'or' 'not' 'not' b2 'or' 'not' a3) 'or' ('not' a1 'or' 'not'
a2 'or' b3) by BVFUNC_5:38
.=(b1 'or' 'not' 'not' b2 'or' 'not' a3) 'or' ('not' a1 'or' 'not'
a2 'or' b3) by BVFUNC_1:4
.=(b1 'or' b2 'or' 'not' a3) 'or' ('not' a1 'or' 'not' a2 'or' b3)
by BVFUNC_1:4
.=b1 'or' b2 'or' 'not' a3 'or' ('not' a1 'or' 'not' a2) 'or' b3 by BVFUNC_1:11
.=b1 'or' b2 'or' (('not' a1 'or' 'not' a2) 'or' 'not' a3) 'or' b3
by BVFUNC_1:11
.=(('not' a1 'or' 'not' a2) 'or' 'not'
a3) 'or' ((b1 'or' b2) 'or' b3) by BVFUNC_1:11
.='not'( a1 '&' a2 '&' a3) 'or' (b1 'or' b2 'or' b3) by BVFUNC_5:38
.=(a1 '&' a2 '&' a3) 'imp' (b1 'or' b2 'or' b3) by BVFUNC_4:8;
hence thesis;
end;
theorem 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
let a,b,c be Element of Funcs(Y,BOOLEAN);
for z being Element of Y st
Pj((a 'imp' b) '&' (b 'imp' c) '&' (c 'imp' a),z)=TRUE
holds
Pj((a '&' b '&' c) 'or' ('not' a '&' 'not' b '&' 'not' c),z)=TRUE
proof
let z be Element of Y;
assume A1:
Pj((a 'imp' b) '&' (b 'imp' c) '&' (c 'imp' a),z)=TRUE;
A2: Pj((a 'imp' b) '&' (b 'imp' c) '&' (c 'imp' a),z)
=Pj((a 'imp' b) '&' (b 'imp' c),z) '&' Pj(c 'imp' a,z) by VALUAT_1:def 6
.=Pj(a 'imp' b,z) '&' Pj(b 'imp' c,z) '&' Pj(c 'imp' a,z) by VALUAT_1:def 6
.=Pj('not' a 'or' b,z) '&' Pj(b 'imp' c,z) '&' Pj(c 'imp' a,z) by BVFUNC_4:8
.=Pj('not' a 'or' b,z) '&' Pj('not'
b 'or' c,z) '&' Pj(c 'imp' a,z) by BVFUNC_4:8
.=Pj('not' a 'or' b,z) '&' Pj('not' b 'or' c,z) '&' Pj('not'
c 'or' a,z) by BVFUNC_4:8
.=(Pj('not' a,z) 'or' Pj(b,z)) '&' Pj('not' b 'or' c,z) '&'
Pj('not' c 'or' a,z) by BVFUNC_1:def 7
.=(Pj('not' a,z) 'or' Pj(b,z)) '&' (Pj('not' b,z) 'or' Pj(c,z)) '&'
Pj('not' c 'or' a,z) by BVFUNC_1:def 7
.=(Pj('not' a,z) 'or' Pj(b,z)) '&' (Pj('not' b,z) 'or' Pj(c,z)) '&'
(Pj('not' c,z) 'or' Pj(a,z)) by BVFUNC_1:def 7
.=('not' Pj(a,z) 'or' Pj(b,z)) '&' (Pj('not' b,z) 'or' Pj(c,z)) '&'
(Pj('not' c,z) 'or' Pj(a,z)) by VALUAT_1:def 5
.=('not' Pj(a,z) 'or' Pj(b,z)) '&' ('not' Pj(b,z) 'or' Pj(c,z)) '&'
(Pj('not' c,z) 'or' Pj(a,z)) by VALUAT_1:def 5
.=('not' Pj(a,z) 'or' Pj(b,z)) '&' ('not' Pj(b,z) 'or' Pj(c,z)) '&'
('not' Pj(c,z) 'or' Pj(a,z)) by VALUAT_1:def 5;
now assume
A3: Pj((a '&' b '&' c) 'or' ('not' a '&' 'not' b '&' 'not' c),z)<>TRUE;
A4: Pj((a '&' b '&' c) 'or' ('not' a '&' 'not' b '&' 'not' c),z)
=Pj(a '&' b '&' c,z) 'or' Pj('not' a '&' 'not' b '&' 'not'
c,z) by BVFUNC_1:def 7
.=(Pj(a '&' b,z) '&' Pj(c,z)) 'or'
Pj('not' a '&' 'not' b '&' 'not' c,z) by VALUAT_1:def 6
.=(Pj(a,z) '&' Pj(b,z) '&' Pj(c,z)) 'or'
Pj('not' a '&' 'not' b '&' 'not' c,z) by VALUAT_1:def 6
.=(Pj(a,z) '&' Pj(b,z) '&' Pj(c,z)) 'or'
(Pj('not' a '&' 'not' b,z) '&' Pj('not' c,z)) by VALUAT_1:def 6
.=(Pj(a,z) '&' Pj(b,z) '&' Pj(c,z)) 'or'
(Pj('not' a,z) '&' Pj('not' b,z) '&' Pj('not' c,z)) by VALUAT_1:def 6
.=(Pj(a,z) '&' Pj(b,z) '&' Pj(c,z)) 'or'
('not' Pj(a,z) '&' Pj('not' b,z) '&' Pj('not' c,z)) by VALUAT_1:def 5
.=(Pj(a,z) '&' Pj(b,z) '&' Pj(c,z)) 'or'
('not' Pj(a,z) '&' 'not' Pj(b,z) '&' Pj('not' c,z)) by VALUAT_1:def 5
.=(Pj(a,z) '&' Pj(b,z) '&' Pj(c,z)) 'or'
('not' Pj(a,z) '&' 'not' Pj(b,z) '&' 'not' Pj(c,z))
by VALUAT_1:def 5;
A5:(Pj(a,z) '&' Pj(b,z) '&' Pj(c,z))=TRUE or
(Pj(a,z) '&' Pj(b,z) '&' Pj(c,z))=FALSE by MARGREL1:39;
A6: ('not' Pj(a,z) '&' 'not' Pj(b,z) '&' 'not' Pj(c,z))=TRUE or
('not' Pj(a,z) '&' 'not' Pj(b,z) '&' 'not'
Pj(c,z))=FALSE by MARGREL1:39;
now per cases by A3,A4,A5,BINARITH:19,MARGREL1:45;
case A7: (Pj(a,z) '&' Pj(b,z))=FALSE;
now per cases by A7,MARGREL1:45;
case A8:Pj(a,z)=FALSE;
then A9: 'not' Pj(a,z) '&' 'not' Pj(b,z) '&' 'not' Pj(c,z)
=TRUE '&' 'not' Pj(b,z) '&' 'not' Pj(c,z) by MARGREL1:41
.='not' Pj(b,z) '&' 'not' Pj(c,z) by MARGREL1:50;
now per cases by A3,A4,A6,A9,BINARITH:19,MARGREL1:45;
case 'not' Pj(b,z)=FALSE;
then Pj(b,z)=TRUE by MARGREL1:41;
then ('not' Pj(a,z) 'or' Pj(b,z)) '&' ('not' Pj(b,z) 'or' Pj(c,z)) '&'
('not' Pj(c,z) 'or' Pj(a,z))
=(TRUE 'or' TRUE) '&' ('not' TRUE 'or' Pj(c,z)) '&'
('not' Pj(c,z) 'or' FALSE) by A8,MARGREL1:41
.=(TRUE 'or' TRUE) '&' (FALSE 'or' Pj(c,z)) '&'
('not' Pj(c,z) 'or' FALSE) by MARGREL1:41
.=TRUE '&' (FALSE 'or' Pj(c,z)) '&'
('not' Pj(c,z) 'or' FALSE) by BINARITH:19
.=TRUE '&' Pj(c,z) '&'
('not' Pj(c,z) 'or' FALSE) by BINARITH:7
.=TRUE '&' Pj(c,z) '&' 'not' Pj(c,z) by BINARITH:7
.=TRUE '&' (Pj(c,z) '&' 'not' Pj(c,z)) by MARGREL1:52
.=TRUE '&' FALSE by MARGREL1:46
.=FALSE by MARGREL1:50;
hence thesis by A1,A2,MARGREL1:43;
case 'not' Pj(c,z)=FALSE;
then Pj(c,z)=TRUE by MARGREL1:41;
then ('not' Pj(a,z) 'or' Pj(b,z)) '&' ('not' Pj(b,z) 'or' Pj(c,z)) '&'
('not' Pj(c,z) 'or' Pj(a,z))
=(TRUE 'or' Pj(b,z)) '&' ('not' Pj(b,z) 'or' TRUE) '&'
('not' TRUE 'or' FALSE) by A8,MARGREL1:41
.=(TRUE 'or' Pj(b,z)) '&' ('not' Pj(b,z) 'or' TRUE) '&'
(FALSE 'or' FALSE) by MARGREL1:41
.=TRUE '&' ('not' Pj(b,z) 'or' TRUE) '&'
(FALSE 'or' FALSE) by BINARITH:19
.=TRUE '&' TRUE '&'
(FALSE 'or' FALSE) by BINARITH:19
.=FALSE '&' (TRUE '&' TRUE) by BINARITH:7
.=FALSE by MARGREL1:49;
hence thesis by A1,A2,MARGREL1:43;
end;
hence thesis;
case A10:Pj(b,z)=FALSE;
then A11: 'not' Pj(a,z) '&' 'not' Pj(b,z) '&' 'not' Pj(c,z)
=TRUE '&' 'not' Pj(a,z) '&' 'not' Pj(c,z) by MARGREL1:41
.='not' Pj(a,z) '&' 'not' Pj(c,z) by MARGREL1:50;
now per cases by A3,A4,A6,A11,BINARITH:19,MARGREL1:45;
case 'not' Pj(a,z)=FALSE;
then ('not' Pj(a,z) 'or' Pj(b,z)) '&' ('not' Pj(b,z) 'or' Pj(c,z)) '&'
('not' Pj(c,z) 'or' Pj(a,z))
=(FALSE 'or' FALSE) '&' ('not' FALSE 'or' Pj(c,z)) '&'
('not' Pj(c,z) 'or' TRUE) by A10,MARGREL1:41
.=(FALSE 'or' FALSE) '&' (TRUE 'or' Pj(c,z)) '&'
('not' Pj(c,z) 'or' TRUE) by MARGREL1:41
.=FALSE '&' (TRUE 'or' Pj(c,z)) '&'
('not' Pj(c,z) 'or' TRUE) by BINARITH:7
.=FALSE '&' ((TRUE 'or' Pj(c,z)) '&'
('not' Pj(c,z) 'or' TRUE)) by MARGREL1:52
.=FALSE by MARGREL1:49;
hence thesis by A1,A2,MARGREL1:43;
case 'not' Pj(c,z)=FALSE;
then Pj(c,z)=TRUE by MARGREL1:41;
then ('not' Pj(a,z) 'or' Pj(b,z)) '&' ('not' Pj(b,z) 'or' Pj(c,z)) '&'
('not' Pj(c,z) 'or' Pj(a,z))
=('not' Pj(a,z) 'or' FALSE) '&' (TRUE 'or' TRUE) '&'
('not' TRUE 'or' Pj(a,z)) by A10,MARGREL1:41
.=('not' Pj(a,z) 'or' FALSE) '&' (TRUE 'or' TRUE) '&'
(FALSE 'or' Pj(a,z)) by MARGREL1:41
.='not' Pj(a,z) '&' (TRUE 'or' TRUE) '&'
(FALSE 'or' Pj(a,z)) by BINARITH:7
.=(TRUE 'or' TRUE) '&' 'not' Pj(a,z) '&'
Pj(a,z) by BINARITH:7
.=(TRUE 'or' TRUE) '&' ('not' Pj(a,z) '&'
Pj(a,z)) by MARGREL1:52
.=FALSE '&' (TRUE 'or' TRUE) by MARGREL1:46
.=FALSE by MARGREL1:49;
hence thesis by A1,A2,MARGREL1:43;
end;
hence thesis;
end;
hence thesis;
case A12:Pj(c,z)=FALSE;
then A13: 'not' Pj(a,z) '&' 'not' Pj(b,z) '&' 'not' Pj(c,z)
=TRUE '&' ('not' Pj(a,z) '&' 'not' Pj(b,z)) by MARGREL1:41
.='not' Pj(a,z) '&' 'not' Pj(b,z) by MARGREL1:50;
now per cases by A3,A4,A6,A13,BINARITH:19,MARGREL1:45;
case 'not' Pj(a,z)=FALSE;
then ('not' Pj(a,z) 'or' Pj(b,z)) '&' ('not' Pj(b,z) 'or' Pj(c,z)) '&'
('not' Pj(c,z) 'or' Pj(a,z))
=(FALSE 'or' Pj(b,z)) '&' ('not' Pj(b,z) 'or' FALSE) '&'
('not' FALSE 'or' TRUE) by A12,MARGREL1:41
.=(FALSE 'or' Pj(b,z)) '&' ('not' Pj(b,z) 'or' FALSE) '&'
(TRUE 'or' TRUE) by MARGREL1:41
.=Pj(b,z) '&' ('not' Pj(b,z) 'or' FALSE) '&'
(TRUE 'or' TRUE) by BINARITH:7
.=Pj(b,z) '&' 'not' Pj(b,z) '&' (TRUE 'or' TRUE) by BINARITH:7
.=FALSE '&' (TRUE 'or' TRUE) by MARGREL1:46
.=FALSE by MARGREL1:49;
hence thesis by A1,A2,MARGREL1:43;
case 'not' Pj(b,z)=FALSE;
then ('not' Pj(a,z) 'or' Pj(b,z)) '&' ('not' Pj(b,z) 'or' Pj(c,z)) '&'
('not' Pj(c,z) 'or' Pj(a,z))
=('not' Pj(a,z) 'or' TRUE) '&' (FALSE 'or' FALSE) '&'
('not' FALSE 'or' Pj(a,z)) by A12,MARGREL1:41
.=FALSE '&' ('not' Pj(a,z) 'or' TRUE) '&'
('not' FALSE 'or' Pj(a,z)) by BINARITH:7
.=FALSE '&' (('not' Pj(a,z) 'or' TRUE) '&'
('not' FALSE 'or' Pj(a,z))) by MARGREL1:52
.=FALSE by MARGREL1:49;
hence thesis by A1,A2,MARGREL1:43;
end;
hence thesis;
end;
hence thesis;
end;
hence thesis;
end;
then A14:(a 'imp' b) '&' (b 'imp' c) '&' (c 'imp' a) '<'
(a '&' b '&' c) 'or' ('not' a '&' 'not' b '&' 'not' c) by BVFUNC_1:def 15;
for z being Element of Y st
Pj((a '&' b '&' c) 'or' ('not' a '&' 'not' b '&' 'not' c),z)=TRUE
holds
Pj((a 'imp' b) '&' (b 'imp' c) '&' (c 'imp' a),z)=TRUE
proof
let z be Element of Y;
assume A15:
Pj((a '&' b '&' c) 'or' ('not' a '&' 'not' b '&' 'not' c),z)=TRUE;
A16: Pj((a '&' b '&' c) 'or' ('not' a '&' 'not' b '&' 'not' c),z)
=Pj(a '&' b '&' c,z) 'or' Pj('not' a '&' 'not' b '&' 'not'
c,z) by BVFUNC_1:def 7
.=(Pj(a '&' b,z) '&' Pj(c,z)) 'or'
Pj('not' a '&' 'not' b '&' 'not' c,z) by VALUAT_1:def 6
.=(Pj(a,z) '&' Pj(b,z) '&' Pj(c,z)) 'or'
Pj('not' a '&' 'not' b '&' 'not' c,z) by VALUAT_1:def 6
.=(Pj(a,z) '&' Pj(b,z) '&' Pj(c,z)) 'or'
(Pj('not' a '&' 'not' b,z) '&' Pj('not' c,z)) by VALUAT_1:def 6
.=(Pj(a,z) '&' Pj(b,z) '&' Pj(c,z)) 'or'
(Pj('not' a,z) '&' Pj('not' b,z) '&' Pj('not' c,z)) by VALUAT_1:def 6
.=(Pj(a,z) '&' Pj(b,z) '&' Pj(c,z)) 'or'
('not' Pj(a,z) '&' Pj('not' b,z) '&' Pj('not' c,z)) by VALUAT_1:def 5
.=(Pj(a,z) '&' Pj(b,z) '&' Pj(c,z)) 'or'
('not' Pj(a,z) '&' 'not' Pj(b,z) '&' Pj('not' c,z)) by VALUAT_1:def 5
.=(Pj(a,z) '&' Pj(b,z) '&' Pj(c,z)) 'or'
('not' Pj(a,z) '&' 'not' Pj(b,z) '&' 'not' Pj(c,z))
by VALUAT_1:def 5;
now assume
A17: Pj((a 'imp' b) '&' (b 'imp' c) '&' (c 'imp' a),z)<>TRUE;
Pj((a 'imp' b) '&' (b 'imp' c) '&' (c 'imp' a),z)
=Pj((a 'imp' b) '&' (b 'imp' c),z) '&' Pj(c 'imp' a,z) by VALUAT_1:def 6
.=Pj(a 'imp' b,z) '&' Pj(b 'imp' c,z) '&' Pj(c 'imp' a,z) by VALUAT_1:def 6
.=Pj('not' a 'or' b,z) '&' Pj(b 'imp' c,z) '&' Pj(c 'imp' a,z) by BVFUNC_4:8
.=Pj('not' a 'or' b,z) '&' Pj('not'
b 'or' c,z) '&' Pj(c 'imp' a,z) by BVFUNC_4:8
.=Pj('not' a 'or' b,z) '&' Pj('not' b 'or' c,z) '&' Pj('not'
c 'or' a,z) by BVFUNC_4:8
.=(Pj('not' a,z) 'or' Pj(b,z)) '&' Pj('not' b 'or' c,z) '&'
Pj('not' c 'or' a,z) by BVFUNC_1:def 7
.=(Pj('not' a,z) 'or' Pj(b,z)) '&' (Pj('not' b,z) 'or' Pj(c,z)) '&'
Pj('not' c 'or' a,z) by BVFUNC_1:def 7
.=(Pj('not' a,z) 'or' Pj(b,z)) '&' (Pj('not' b,z) 'or' Pj(c,z)) '&'
(Pj('not' c,z) 'or' Pj(a,z)) by BVFUNC_1:def 7
.=('not' Pj(a,z) 'or' Pj(b,z)) '&' (Pj('not' b,z) 'or' Pj(c,z)) '&'
(Pj('not' c,z) 'or' Pj(a,z)) by VALUAT_1:def 5
.=('not' Pj(a,z) 'or' Pj(b,z)) '&' ('not' Pj(b,z) 'or' Pj(c,z)) '&'
(Pj('not' c,z) 'or' Pj(a,z)) by VALUAT_1:def 5
.=('not' Pj(a,z) 'or' Pj(b,z)) '&' ('not' Pj(b,z) 'or' Pj(c,z)) '&'
('not' Pj(c,z) 'or' Pj(a,z)) by VALUAT_1:def 5;
then A18: ('not' Pj(a,z) 'or' Pj(b,z)) '&' ('not' Pj(b,z) 'or' Pj(c,z)) '&'
('not' Pj(c,z) 'or' Pj(a,z))=FALSE by A17,MARGREL1:43;
now per cases by A18,MARGREL1:45;
case A19: ('not' Pj(a,z) 'or' Pj(b,z)) '&' ('not' Pj(b,z) 'or' Pj(c,z))=
FALSE;
now per cases by A19,MARGREL1:45;
case A20:('not' Pj(a,z) 'or' Pj(b,z))=FALSE;
A21:'not' Pj(a,z)=TRUE or 'not' Pj(a,z)=FALSE by MARGREL1:39;
Pj(b,z)=TRUE or Pj(b,z)=FALSE by MARGREL1:39;
then A22: 'not' Pj(a,z)=FALSE & Pj(b,z)=FALSE by A20,A21,BINARITH:19;
then Pj(a,z)=TRUE by MARGREL1:41;
then (Pj(a,z) '&' Pj(b,z) '&' Pj(c,z)) 'or'
('not' Pj(a,z) '&' 'not' Pj(b,z) '&' 'not' Pj(c,z))
=(FALSE '&' (TRUE '&' Pj(c,z))) 'or'
(FALSE '&' 'not' FALSE '&' 'not' Pj(c,z)) by A22,MARGREL1:52
.=(FALSE '&' (TRUE '&' Pj(c,z))) 'or'
(FALSE '&' ('not' FALSE '&' 'not' Pj(c,z))) by MARGREL1:52
.=FALSE 'or' (FALSE '&' ('not' FALSE '&' 'not' Pj(c,z))) by MARGREL1:49
.=FALSE 'or' FALSE by MARGREL1:49
.=FALSE by BINARITH:7;
hence thesis by A15,A16,MARGREL1:43;
case A23:('not' Pj(b,z) 'or' Pj(c,z))=FALSE;
A24:'not' Pj(b,z)=TRUE or 'not' Pj(b,z)=FALSE by MARGREL1:39;
Pj(c,z)=TRUE or Pj(c,z)=FALSE by MARGREL1:39;
then A25: 'not' Pj(b,z)=FALSE & Pj(c,z)=FALSE by A23,A24,BINARITH:19;
then Pj(b,z)=TRUE by MARGREL1:41;
then (Pj(a,z) '&' Pj(b,z) '&' Pj(c,z)) 'or'
('not' Pj(a,z) '&' 'not' Pj(b,z) '&' 'not' Pj(c,z))
=(FALSE '&' (Pj(a,z) '&' TRUE)) 'or'
(FALSE '&' ('not' Pj(a,z) '&' 'not' FALSE)) by A25,MARGREL1:52
.=FALSE 'or' (FALSE '&' ('not' Pj(a,z) '&' 'not' FALSE)) by MARGREL1:49
.=FALSE 'or' FALSE by MARGREL1:49
.=FALSE by BINARITH:7;
hence thesis by A15,A16,MARGREL1:43;
end;
hence thesis;
case A26:('not' Pj(c,z) 'or' Pj(a,z))=FALSE;
A27:'not' Pj(c,z)=TRUE or 'not' Pj(c,z)=FALSE by MARGREL1:39;
Pj(a,z)=TRUE or Pj(a,z)=FALSE by MARGREL1:39;
then A28: 'not' Pj(c,z)=FALSE & Pj(a,z)=FALSE by A26,A27,BINARITH:19;
then Pj(c,z)=TRUE by MARGREL1:41;
then (Pj(a,z) '&' Pj(b,z) '&' Pj(c,z)) 'or'
('not' Pj(a,z) '&' 'not' Pj(b,z) '&' 'not' Pj(c,z))
=(FALSE '&' (Pj(b,z) '&' TRUE)) 'or'
(FALSE '&' ('not' FALSE '&' 'not' Pj(b,z))) by A28,MARGREL1:52
.=FALSE 'or' (FALSE '&' ('not' FALSE '&' 'not' Pj(b,z))) by MARGREL1:49
.=FALSE 'or' FALSE by MARGREL1:49
.=FALSE by BINARITH:7;
hence thesis by A15,A16,MARGREL1:43;
end;
hence thesis;
end;
hence thesis;
end;
then (a '&' b '&' c) 'or' ('not' a '&' 'not' b '&' 'not' c) '<'
(a 'imp' b) '&' (b 'imp' c) '&' (c 'imp' a) by BVFUNC_1:def 15;
hence thesis by A14,BVFUNC_1:18;
end;
theorem 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
let a,b,c be Element of Funcs(Y,BOOLEAN);
(a 'imp' b) '&' (b 'imp' c) '&' (c 'imp' a) '&' (a 'or' b 'or' c)
=('not' a 'or' b) '&' (b 'imp' c) '&' (c 'imp' a) '&' (a 'or' b 'or' c)
by BVFUNC_4:8
.=('not' a 'or' b) '&' ('not' b 'or' c) '&' (c 'imp' a) '&' (a 'or' b 'or' c)
by BVFUNC_4:8
.=('not' a 'or' b) '&' ('not' b 'or' c) '&' ('not' c 'or' a)
'&' (a 'or' b 'or' c)
by BVFUNC_4:8
.=('not' a 'or' b) '&' ('not' b 'or' c) '&' (('not'
c 'or' a) '&' (a 'or' b 'or' c))
by BVFUNC_1:7
.=('not' a 'or' b) '&' ('not' b 'or' c) '&'
(('not' c 'or' a) '&' (a 'or' b) 'or' ('not' c 'or' a) '&' c)
by BVFUNC_1:15
.=('not' a 'or' b) '&' ('not' b 'or' c) '&'
(('not' c 'or' a) '&' (a 'or' b) 'or' ('not' c '&' c 'or' a '&' c))
by BVFUNC_1:15
.=('not' a 'or' b) '&' ('not' b 'or' c) '&'
(('not' c 'or' a) '&' (a 'or' b) 'or' (O_el(Y) 'or' a '&' c))
by BVFUNC_4:5
.=('not' a 'or' b) '&' ('not' b 'or' c) '&'
(('not' c 'or' a) '&' (a 'or' b) 'or' (a '&' c))
by BVFUNC_1:12
.=('not' a 'or' b) '&' ('not' b 'or' c) '&'
(a 'or' ('not' c '&' b) 'or' (a '&' c))
by BVFUNC_1:14
.=('not' a 'or' b) '&' ('not' b 'or' c) '&'
(a 'or' (a '&' c) 'or' ('not' c '&' b))
by BVFUNC_1:11
.=('not' a 'or' b) '&' ('not' b 'or' c) '&'
((a '&' I_el(Y)) 'or' (a '&' c) 'or' ('not' c '&' b))
by BVFUNC_1:9
.=('not' a 'or' b) '&' ('not' b 'or' c) '&'
((a '&' (I_el(Y) 'or' c)) 'or' ('not' c '&' b))
by BVFUNC_1:15
.=('not' a 'or' b) '&' ('not' b 'or' c) '&'
((a '&' I_el(Y)) 'or' ('not' c '&' b))
by BVFUNC_1:13
.=('not' a 'or' b) '&' ('not' b 'or' c) '&'
(a 'or' ('not' c '&' b))
by BVFUNC_1:9
.=('not' a 'or' b) '&' ('not' b 'or' c) '&'
((a 'or' 'not' c) '&' (a 'or' b))
by BVFUNC_1:14
.=(a 'or' b) '&' (('not' a 'or' b) '&' ('not' b 'or' c)) '&'
(a 'or' 'not' c)
by BVFUNC_1:7
.=(a 'or' b) '&' ('not' a 'or' b) '&' ('not' b 'or' c) '&'
(a 'or' 'not' c)
by BVFUNC_1:7
.=((a '&' 'not' a) 'or' b) '&' ('not' b 'or' c) '&'
(a 'or' 'not' c)
by BVFUNC_1:14
.=(O_el(Y) 'or' b) '&' ('not' b 'or' c) '&'
(a 'or' 'not' c)
by BVFUNC_4:5
.=b '&' ('not' b 'or' c) '&' (a 'or' 'not' c)
by BVFUNC_1:12
.=(b '&' 'not' b 'or' b '&' c) '&' (a 'or' 'not' c)
by BVFUNC_1:15
.=(O_el(Y) 'or' b '&' c) '&' (a 'or' 'not' c)
by BVFUNC_4:5
.=(b '&' c) '&' (a 'or' 'not' c)
by BVFUNC_1:12
.=(b '&' c) '&' a 'or' (b '&' c) '&' 'not' c
by BVFUNC_1:15
.=(b '&' c) '&' a 'or' b '&' (c '&' 'not' c)
by BVFUNC_1:7
.=(b '&' c) '&' a 'or' b '&' O_el(Y)
by BVFUNC_4:5
.=(b '&' c) '&' a 'or' O_el(Y)
by BVFUNC_1:8
.=(b '&' c) '&' a
by BVFUNC_1:12
.=(a '&' b '&' c) by BVFUNC_1:7;
hence thesis;
end;
Lm4: 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
let a,b,c be Element of Funcs(Y,BOOLEAN);
let z be Element of Y;
assume A1:
Pj(('not' a '&' b '&' c) 'or' (a '&' 'not' b '&' c) 'or' (a '&' b '&' 'not'
c),z)=TRUE;
A2: Pj(('not' a '&' b '&' c) 'or' (a '&' 'not' b '&' c) 'or' (a '&' b '&'
'not'
c),z)
=Pj(('not' a '&' b '&' c) 'or' (a '&' 'not' b '&' c),z) 'or' Pj(a '&' b '&'
'not' c,z)
by BVFUNC_1:def 7
.=Pj('not' a '&' b '&' c,z) 'or' Pj(a '&' 'not' b '&' c,z) 'or'
Pj(a '&' b '&' 'not' c,z)
by BVFUNC_1:def 7
.=Pj('not' a '&' b '&' c,z) 'or' Pj(a '&' 'not' b '&' c,z) 'or'
(Pj(a '&' b,z) '&' Pj('not' c,z))
by VALUAT_1:def 6
.=Pj('not' a '&' b '&' c,z) 'or' Pj(a '&' 'not' b '&' c,z) 'or'
(Pj(a,z) '&' Pj(b,z) '&' Pj('not' c,z))
by VALUAT_1:def 6
.=Pj('not' a '&' b '&' c,z) 'or'
(Pj(a '&' 'not' b,z) '&' Pj(c,z)) 'or'
(Pj(a,z) '&' Pj(b,z) '&' Pj('not' c,z))
by VALUAT_1:def 6
.=Pj('not' a '&' b '&' c,z) 'or'
(Pj(a,z) '&' Pj('not' b,z) '&' Pj(c,z)) 'or'
(Pj(a,z) '&' Pj(b,z) '&' Pj('not' c,z))
by VALUAT_1:def 6
.=(Pj('not' a '&' b,z) '&' Pj(c,z)) 'or'
(Pj(a,z) '&' Pj('not' b,z) '&' Pj(c,z)) 'or'
(Pj(a,z) '&' Pj(b,z) '&' Pj('not' c,z))
by VALUAT_1:def 6
.=(Pj('not' a,z) '&' Pj(b,z) '&' Pj(c,z)) 'or'
(Pj(a,z) '&' Pj('not' b,z) '&' Pj(c,z)) 'or'
(Pj(a,z) '&' Pj(b,z) '&' Pj('not' c,z))
by VALUAT_1:def 6
.=('not' Pj(a,z) '&' Pj(b,z) '&' Pj(c,z)) 'or'
(Pj(a,z) '&' Pj('not' b,z) '&' Pj(c,z)) 'or'
(Pj(a,z) '&' Pj(b,z) '&' Pj('not' c,z))
by VALUAT_1:def 5
.=('not' Pj(a,z) '&' Pj(b,z) '&' Pj(c,z)) 'or'
(Pj(a,z) '&' 'not' Pj(b,z) '&' Pj(c,z)) 'or'
(Pj(a,z) '&' Pj(b,z) '&' Pj('not' c,z))
by VALUAT_1:def 5
.=('not' Pj(a,z) '&' Pj(b,z) '&' Pj(c,z)) 'or'
(Pj(a,z) '&' 'not' Pj(b,z) '&' Pj(c,z)) 'or'
(Pj(a,z) '&' Pj(b,z) '&' 'not' Pj(c,z))
by VALUAT_1:def 5;
now assume A3: Pj((a 'or' b) '&' 'not'( a '&' b '&' c),z)<>TRUE;
Pj((a 'or' b) '&' 'not'( a '&' b '&' c),z)
=Pj((a 'or' b) '&' ('not' a 'or' 'not' b 'or' 'not' c),z) by BVFUNC_5:38
.=Pj(a 'or' b,z) '&' Pj('not' a 'or' 'not' b 'or' 'not' c,z)
by VALUAT_1:def 6
.=(Pj(a,z) 'or' Pj(b,z)) '&' Pj('not' a 'or' 'not' b 'or' 'not'
c,z) by BVFUNC_1:def 7
.=(Pj(a,z) 'or' Pj(b,z)) '&'
(Pj('not' a 'or' 'not' b,z) 'or' Pj('not' c,z)) by BVFUNC_1:def 7
.=(Pj(a,z) 'or' Pj(b,z)) '&'
(Pj('not' a,z) 'or' Pj('not' b,z) 'or' Pj('not' c,z)) by BVFUNC_1:def 7
.=(Pj(a,z) 'or' Pj(b,z)) '&'
('not' Pj(a,z) 'or' Pj('not' b,z) 'or' Pj('not' c,z)) by VALUAT_1:def 5
.=(Pj(a,z) 'or' Pj(b,z)) '&'
('not' Pj(a,z) 'or' 'not' Pj(b,z) 'or' Pj('not' c,z)) by VALUAT_1:def 5
.=(Pj(a,z) 'or' Pj(b,z)) '&'
('not' Pj(a,z) 'or' 'not' Pj(b,z) 'or' 'not' Pj(c,z))
by VALUAT_1:def 5;
then A4: (Pj(a,z) 'or' Pj(b,z)) '&'
('not' Pj(a,z) 'or' 'not' Pj(b,z) 'or' 'not' Pj(c,z))=FALSE by A3,
MARGREL1:43;
now per cases by A4,MARGREL1:45;
case A5:(Pj(a,z) 'or' Pj(b,z))=FALSE;
A6:Pj(a,z)=TRUE or Pj(a,z)=FALSE by MARGREL1:39;
Pj(b,z)=TRUE or Pj(b,z)=FALSE by MARGREL1:39;
then Pj(a,z)=FALSE & Pj(b,z)=FALSE by A5,A6,BINARITH:19;
then ('not' Pj(a,z) '&' Pj(b,z) '&' Pj(c,z)) 'or'
(Pj(a,z) '&' 'not' Pj(b,z) '&' Pj(c,z)) 'or'
(Pj(a,z) '&' Pj(b,z) '&' 'not' Pj(c,z))
=(FALSE '&' Pj(c,z)) 'or'
(FALSE '&' 'not' FALSE '&' Pj(c,z)) 'or'
(FALSE '&' FALSE '&' 'not' Pj(c,z)) by MARGREL1:49
.=FALSE 'or' (FALSE '&' 'not' FALSE '&' Pj(c,z)) 'or'
(FALSE '&' FALSE '&' 'not' Pj(c,z)) by MARGREL1:49
.=FALSE 'or' (FALSE '&' Pj(c,z)) 'or'
(FALSE '&' FALSE '&' 'not' Pj(c,z)) by MARGREL1:49
.=FALSE 'or' FALSE 'or'
(FALSE '&' FALSE '&' 'not' Pj(c,z)) by MARGREL1:49
.=FALSE 'or' FALSE 'or' (FALSE '&' 'not' Pj(c,z)) by MARGREL1:49
.=FALSE 'or' FALSE 'or' FALSE by MARGREL1:49
.=FALSE 'or' FALSE by BINARITH:7
.=FALSE by BINARITH:7;
hence thesis by A1,A2,MARGREL1:43;
case A7:('not' Pj(a,z) 'or' 'not' Pj(b,z) 'or' 'not' Pj(c,z))=FALSE;
A8:'not' Pj(a,z) 'or' 'not' Pj(b,z)=TRUE or
'not' Pj(a,z) 'or' 'not' Pj(b,z)=FALSE by MARGREL1:39;
'not' Pj(c,z)=TRUE or 'not' Pj(c,z)=FALSE by MARGREL1:39;
then A9: 'not' Pj(a,z) 'or' 'not' Pj(b,z)=FALSE & 'not'
Pj(c,z)=FALSE by A7,A8,BINARITH:19;
A10:'not' Pj(a,z)=TRUE or 'not' Pj(a,z)=FALSE by MARGREL1:39;
'not' Pj(b,z)=TRUE or 'not' Pj(b,z)=FALSE by MARGREL1:39;
then 'not' Pj(a,z)=FALSE & 'not' Pj(b,z)=FALSE by A7,A8,A10,BINARITH:19;
then Pj(a,z)=TRUE & Pj(b,z)=TRUE & Pj(c,z)=TRUE by A9,MARGREL1:41;
then ('not' Pj(a,z) '&' Pj(b,z) '&' Pj(c,z)) 'or'
(Pj(a,z) '&' 'not' Pj(b,z) '&' Pj(c,z)) 'or'
(Pj(a,z) '&' Pj(b,z) '&' 'not' Pj(c,z))
=(FALSE '&' Pj(b,z) '&' Pj(c,z)) 'or'
(Pj(a,z) '&' 'not' TRUE '&' Pj(c,z)) 'or'
(Pj(a,z) '&' Pj(b,z) '&' 'not' TRUE) by MARGREL1:41
.=(FALSE '&' Pj(b,z) '&' Pj(c,z)) 'or'
(Pj(a,z) '&' FALSE '&' Pj(c,z)) 'or'
(Pj(a,z) '&' Pj(b,z) '&' 'not' TRUE) by MARGREL1:41
.=(FALSE '&' Pj(b,z) '&' Pj(c,z)) 'or'
(FALSE '&' Pj(a,z) '&' Pj(c,z)) 'or'
(Pj(a,z) '&' Pj(b,z) '&' FALSE) by MARGREL1:41
.=(FALSE '&' Pj(c,z)) 'or' (FALSE '&' Pj(a,z) '&' Pj(c,z)) 'or'
(FALSE '&' (Pj(a,z) '&' Pj(b,z))) by MARGREL1:49
.=FALSE 'or' (FALSE '&' Pj(a,z) '&' Pj(c,z)) 'or'
(FALSE '&' (Pj(a,z) '&' Pj(b,z))) by MARGREL1:49
.=FALSE 'or' (FALSE '&' Pj(c,z)) 'or'
(FALSE '&' (Pj(a,z) '&' Pj(b,z))) by MARGREL1:49
.=FALSE 'or' FALSE 'or' (FALSE '&' (Pj(a,z) '&' Pj(b,z))) by MARGREL1:49
.=FALSE 'or' FALSE 'or' FALSE by MARGREL1:49
.=FALSE 'or' FALSE by BINARITH:7
.=FALSE by BINARITH:7;
hence thesis by A1,A2,MARGREL1:43;
end;
hence thesis;
end;
hence thesis;
end;
theorem 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
let a,b,c be Element of Funcs(Y,BOOLEAN);
for z being Element of Y st
Pj((a 'or' b) '&' (b 'or' c) '&' (c 'or' a) '&' 'not'
(a '&' b '&' c),z)=TRUE
holds
Pj(('not' a '&' b '&' c) 'or' (a '&' 'not' b '&' c) 'or' (a '&' b '&' 'not'
c),z)=TRUE
proof
let z be Element of Y;
assume A1:
Pj((a 'or' b) '&' (b 'or' c) '&' (c 'or' a) '&' 'not'
(a '&' b '&' c),z)=TRUE;
A2: Pj((a 'or' b) '&' (b 'or' c) '&' (c 'or' a) '&' 'not'( a '&' b '&' c),z
)
=Pj((a 'or' b) '&' (b 'or' c) '&' (c 'or' a),z) '&' Pj('not'
(a '&' b '&' c),z)
by VALUAT_1:def 6
.=Pj((a 'or' b) '&' (b 'or' c),z) '&'
Pj(c 'or' a,z) '&' Pj('not'( a '&' b '&' c),z)
by VALUAT_1:def 6
.=Pj(a 'or' b,z) '&' Pj(b 'or' c,z) '&'
Pj(c 'or' a,z) '&' Pj('not'( a '&' b '&' c),z)
by VALUAT_1:def 6
.=Pj(a 'or' b,z) '&' Pj(b 'or' c,z) '&'
Pj(c 'or' a,z) '&' Pj(('not' a 'or' 'not' b 'or' 'not' c),z)
by BVFUNC_5:38
.=(Pj(a,z) 'or' Pj(b,z)) '&' Pj(b 'or' c,z) '&'
Pj(c 'or' a,z) '&' Pj(('not' a 'or' 'not' b 'or' 'not' c),z)
by BVFUNC_1:def 7
.=(Pj(a,z) 'or' Pj(b,z)) '&' (Pj(b,z) 'or' Pj(c,z)) '&'
Pj(c 'or' a,z) '&' Pj(('not' a 'or' 'not' b 'or' 'not' c),z)
by BVFUNC_1:def 7
.=(Pj(a,z) 'or' Pj(b,z)) '&' (Pj(b,z) 'or' Pj(c,z)) '&'
(Pj(c,z) 'or' Pj(a,z)) '&' Pj(('not' a 'or' 'not' b 'or' 'not' c),z)
by BVFUNC_1:def 7
.=(Pj(a,z) 'or' Pj(b,z)) '&' (Pj(b,z) 'or' Pj(c,z)) '&'
(Pj(c,z) 'or' Pj(a,z)) '&' (Pj('not' a 'or' 'not' b,z) 'or' Pj('not' c,z))
by BVFUNC_1:def 7
.=(Pj(a,z) 'or' Pj(b,z)) '&' (Pj(b,z) 'or' Pj(c,z)) '&'
(Pj(c,z) 'or' Pj(a,z)) '&' (Pj('not' a,z) 'or' Pj('not' b,z) 'or' Pj('not'
c,z))
by BVFUNC_1:def 7
.=(Pj(a,z) 'or' Pj(b,z)) '&' (Pj(b,z) 'or' Pj(c,z)) '&'
(Pj(c,z) 'or' Pj(a,z)) '&' ('not' Pj(a,z) 'or' Pj('not' b,z) 'or' Pj('not'
c,z))
by VALUAT_1:def 5
.=(Pj(a,z) 'or' Pj(b,z)) '&' (Pj(b,z) 'or' Pj(c,z)) '&'
(Pj(c,z) 'or' Pj(a,z)) '&' ('not' Pj(a,z) 'or' 'not' Pj(b,z) 'or' Pj('not'
c,z))
by VALUAT_1:def 5
.=(Pj(a,z) 'or' Pj(b,z)) '&' (Pj(b,z) 'or' Pj(c,z)) '&'
(Pj(c,z) 'or' Pj(a,z)) '&' ('not' Pj(a,z) 'or' 'not' Pj(b,z) 'or' 'not'
Pj(c,z))
by VALUAT_1:def 5;
now assume
A3: Pj(('not' a '&' b '&' c) 'or' (a '&' 'not' b '&' c)
'or' (a '&' b '&' 'not' c),z)<>TRUE;
A4: Pj(('not' a '&' b '&' c) 'or' (a '&' 'not' b '&' c) 'or'
(a '&' b '&' 'not'
c),z)
=Pj(('not' a '&' b '&' c) 'or' (a '&' 'not' b '&' c),z) 'or'
Pj(a '&' b '&'
'not' c,z)
by BVFUNC_1:def 7
.=Pj('not' a '&' b '&' c,z) 'or' Pj(a '&' 'not'
b '&' c,z) 'or' Pj(a '&' b '&' 'not' c,z)
by BVFUNC_1:def 7
.=Pj('not' a '&' b '&' c,z) 'or' Pj(a '&' 'not' b '&' c,z) 'or'
(Pj(a '&' b,z) '&' Pj('not' c,z))
by VALUAT_1:def 6
.=Pj('not' a '&' b '&' c,z) 'or' Pj(a '&' 'not' b '&' c,z) 'or'
(Pj(a,z) '&' Pj(b,z) '&' Pj('not' c,z))
by VALUAT_1:def 6
.=Pj('not' a '&' b '&' c,z) 'or'
(Pj(a '&' 'not' b,z) '&' Pj(c,z)) 'or'
(Pj(a,z) '&' Pj(b,z) '&' Pj('not' c,z))
by VALUAT_1:def 6
.=Pj('not' a '&' b '&' c,z) 'or'
(Pj(a,z) '&' Pj('not' b,z) '&' Pj(c,z)) 'or'
(Pj(a,z) '&' Pj(b,z) '&' Pj('not' c,z))
by VALUAT_1:def 6
.=(Pj('not' a '&' b,z) '&' Pj(c,z)) 'or'
(Pj(a,z) '&' Pj('not' b,z) '&' Pj(c,z)) 'or'
(Pj(a,z) '&' Pj(b,z) '&' Pj('not' c,z))
by VALUAT_1:def 6
.=(Pj('not' a,z) '&' Pj(b,z) '&' Pj(c,z)) 'or'
(Pj(a,z) '&' Pj('not' b,z) '&' Pj(c,z)) 'or'
(Pj(a,z) '&' Pj(b,z) '&' Pj('not' c,z))
by VALUAT_1:def 6
.=('not' Pj(a,z) '&' Pj(b,z) '&' Pj(c,z)) 'or'
(Pj(a,z) '&' Pj('not' b,z) '&' Pj(c,z)) 'or'
(Pj(a,z) '&' Pj(b,z) '&' Pj('not' c,z))
by VALUAT_1:def 5
.=('not' Pj(a,z) '&' Pj(b,z) '&' Pj(c,z)) 'or'
(Pj(a,z) '&' 'not' Pj(b,z) '&' Pj(c,z)) 'or'
(Pj(a,z) '&' Pj(b,z) '&' Pj('not' c,z))
by VALUAT_1:def 5
.=('not' Pj(a,z) '&' Pj(b,z) '&' Pj(c,z)) 'or'
(Pj(a,z) '&' 'not' Pj(b,z) '&' Pj(c,z)) 'or'
(Pj(a,z) '&' Pj(b,z) '&' 'not' Pj(c,z))
by VALUAT_1:def 5;
then A5: ('not' Pj(a,z) '&' Pj(b,z) '&' Pj(c,z)) 'or'
(Pj(a,z) '&' 'not' Pj(b,z) '&' Pj(c,z)) 'or'
(Pj(a,z) '&' Pj(b,z) '&' 'not' Pj(c,z))=FALSE by A3,MARGREL1:43;
A6:('not' Pj(a,z) '&' Pj(b,z) '&' Pj(c,z)) 'or'
(Pj(a,z) '&' 'not' Pj(b,z) '&' Pj(c,z))=TRUE or
('not' Pj(a,z) '&' Pj(b,z) '&' Pj(c,z)) 'or'
(Pj(a,z) '&' 'not' Pj(b,z) '&' Pj(c,z))=FALSE by MARGREL1:39;
A7: (Pj(a,z) '&' Pj(b,z) '&' 'not' Pj(c,z))=TRUE or
(Pj(a,z) '&' Pj(b,z) '&' 'not' Pj(c,z))=FALSE by MARGREL1:39;
A8:('not' Pj(a,z) '&' Pj(b,z) '&' Pj(c,z))=TRUE or
('not' Pj(a,z) '&' Pj(b,z) '&' Pj(c,z))=FALSE by MARGREL1:39;
A9: (Pj(a,z) '&' 'not' Pj(b,z) '&' Pj(c,z))=TRUE or
(Pj(a,z) '&' 'not' Pj(b,z) '&' Pj(c,z))=FALSE by MARGREL1:39;
then A10: ('not' Pj(a,z) '&' Pj(b,z) '&' Pj(c,z))=FALSE &
(Pj(a,z) '&' 'not' Pj(b,z) '&' Pj(c,z))=FALSE &
(Pj(a,z) '&' Pj(b,z) '&' 'not' Pj(c,z))=FALSE
by A3,A4,A6,A7,A8,BINARITH:19;
now per cases by A10,MARGREL1:45;
case A11: 'not' Pj(a,z) '&' Pj(b,z)=FALSE;
now per cases by A11,MARGREL1:45;
case A12:'not' Pj(a,z)=FALSE;
then A13:Pj(a,z)=TRUE by MARGREL1:41;
then A14: 'not' Pj(b,z) '&' Pj(c,z)=FALSE by A10,MARGREL1:50;
now per cases by A14,MARGREL1:45;
case 'not' Pj(b,z)=FALSE;
then A15: Pj(b,z)=TRUE by MARGREL1:41;
then Pj(a,z) '&' Pj(b,z) '&' 'not' Pj(c,z)
=TRUE '&' 'not' Pj(c,z) by A13,MARGREL1:50
.='not' Pj(c,z) by MARGREL1:50;
then Pj(c,z)=TRUE by A3,A4,A7,BINARITH:19,MARGREL1:41;
then (Pj(a,z) 'or' Pj(b,z)) '&' (Pj(b,z) 'or' Pj(c,z)) '&'
(Pj(c,z) 'or' Pj(a,z)) '&' ('not' Pj(a,z) 'or' 'not' Pj(b,z) 'or' 'not'
Pj(c,z))
=(TRUE 'or' TRUE) '&' (TRUE 'or' TRUE) '&'
(TRUE 'or' TRUE) '&' (FALSE 'or' FALSE)
by A12,A13,A15,BINARITH:7
.=FALSE '&' ((TRUE 'or' TRUE) '&' (TRUE 'or' TRUE) '&'
(TRUE 'or' TRUE)) by BINARITH:7
.=FALSE by MARGREL1:49;
hence thesis by A1,A2,MARGREL1:43;
case A16:Pj(c,z)=FALSE;
then Pj(a,z) '&' Pj(b,z) '&' 'not' Pj(c,z)
=TRUE '&' Pj(b,z) '&' TRUE by A13,MARGREL1:41
.=TRUE '&' Pj(b,z) by MARGREL1:50
.=Pj(b,z) by MARGREL1:50;
then (Pj(a,z) 'or' Pj(b,z)) '&' (Pj(b,z) 'or' Pj(c,z)) '&'
(Pj(c,z) 'or' Pj(a,z)) '&' ('not' Pj(a,z) 'or' 'not' Pj(b,z) 'or' 'not'
Pj(c,z))
=FALSE '&'
(Pj(c,z) 'or' Pj(a,z)) '&' ('not' Pj(a,z) 'or' 'not' Pj(b,z) 'or' 'not'
Pj(c,z))
by A5,A6,A13,A16,MARGREL1:49
.=FALSE '&'
('not' Pj(a,z) 'or' 'not' Pj(b,z) 'or' 'not' Pj(c,z))
by MARGREL1:49
.=FALSE by MARGREL1:49;
hence thesis by A1,A2,MARGREL1:43;
end;
hence thesis;
case A17:Pj(b,z)=FALSE;
then Pj(a,z) '&' 'not' Pj(b,z) '&' Pj(c,z)
=TRUE '&' Pj(a,z) '&' Pj(c,z) by MARGREL1:41
.=(Pj(a,z) '&' Pj(c,z)) by MARGREL1:50;
then A18: Pj(a,z) '&' Pj(c,z)=FALSE by A3,A4,A6,A9,BINARITH:19;
now per cases by A18,MARGREL1:45;
case Pj(a,z)=FALSE;
then (Pj(a,z) 'or' Pj(b,z)) '&' (Pj(b,z) 'or' Pj(c,z)) '&'
(Pj(c,z) 'or' Pj(a,z)) '&' ('not' Pj(a,z) 'or' 'not'
Pj(b,z) 'or' 'not'
Pj(c,z))
=FALSE '&' (Pj(b,z) 'or' Pj(c,z)) '&'
(Pj(c,z) 'or' Pj(a,z)) '&' ('not' Pj(a,z) 'or' 'not'
Pj(b,z) 'or' 'not'
Pj(c,z))
by A17,BINARITH:7
.=FALSE '&'
(Pj(c,z) 'or' Pj(a,z)) '&' ('not' Pj(a,z) 'or' 'not'
Pj(b,z) 'or' 'not'
Pj(c,z))
by MARGREL1:49
.=FALSE '&' ('not' Pj(a,z) 'or' 'not' Pj(b,z) 'or' 'not' Pj(c,z))
by MARGREL1:49
.=FALSE by MARGREL1:49;
hence thesis by A1,A2,MARGREL1:43;
case Pj(c,z)=FALSE;
then (Pj(a,z) 'or' Pj(b,z)) '&' (Pj(b,z) 'or' Pj(c,z)) '&'
(Pj(c,z) 'or' Pj(a,z)) '&' ('not' Pj(a,z) 'or' 'not'
Pj(b,z) 'or' 'not'
Pj(c,z))
=FALSE '&' (Pj(a,z) 'or' Pj(b,z)) '&'
(Pj(c,z) 'or' Pj(a,z)) '&' ('not' Pj(a,z) 'or' 'not'
Pj(b,z) 'or' 'not' Pj(c,z)) by A17,BINARITH:7
.=FALSE '&'
(Pj(c,z) 'or' Pj(a,z)) '&' ('not' Pj(a,z) 'or' 'not'
Pj(b,z) 'or' 'not' Pj(c,z)) by MARGREL1:49
.=FALSE '&'
('not' Pj(a,z) 'or' 'not' Pj(b,z) 'or' 'not' Pj(c,z))
by MARGREL1:49
.=FALSE by MARGREL1:49;
hence thesis by A1,A2,MARGREL1:43;
end;
hence thesis;
end;
hence thesis;
case A19:Pj(c,z)=FALSE;
then A20: Pj(a,z) '&' Pj(b,z) '&' 'not' Pj(c,z)
=TRUE '&' (Pj(a,z) '&' Pj(b,z)) by MARGREL1:41
.=(Pj(a,z) '&' Pj(b,z)) by MARGREL1:50;
now per cases by A3,A4,A7,A20,BINARITH:19,MARGREL1:45;
case Pj(a,z)=FALSE;
then (Pj(a,z) 'or' Pj(b,z)) '&' (Pj(b,z) 'or' Pj(c,z)) '&'
(Pj(c,z) 'or' Pj(a,z)) '&' ('not' Pj(a,z) 'or' 'not' Pj(b,z) 'or' 'not'
Pj(c,z))
=FALSE '&' ((Pj(a,z) 'or' Pj(b,z)) '&' (Pj(b,z) 'or' Pj(c,z))) '&'
('not' Pj(a,z) 'or' 'not' Pj(b,z) 'or' 'not' Pj(c,z)) by A19,BINARITH:7
.=FALSE '&' ('not' Pj(a,z) 'or' 'not' Pj(b,z) 'or' 'not' Pj(c,z))
by MARGREL1:49
.=FALSE by MARGREL1:49;
hence thesis by A1,A2,MARGREL1:43;
case Pj(b,z)=FALSE;
then (Pj(a,z) 'or' Pj(b,z)) '&' (Pj(b,z) 'or' Pj(c,z)) '&'
(Pj(c,z) 'or' Pj(a,z)) '&' ('not' Pj(a,z) 'or' 'not' Pj(b,z) 'or' 'not'
Pj(c,z))
= FALSE '&' (Pj(a,z) 'or' Pj(b,z)) '&'
(Pj(c,z) 'or' Pj(a,z)) '&' ('not' Pj(a,z) 'or' 'not' Pj(b,z) 'or' 'not'
Pj(c,z)) by A19,BINARITH:7
.= FALSE '&'
(Pj(c,z) 'or' Pj(a,z)) '&' ('not' Pj(a,z) 'or' 'not' Pj(b,z) 'or' 'not'
Pj(c,z))
by MARGREL1:49
.=FALSE '&' ('not' Pj(a,z) 'or' 'not' Pj(b,z) 'or' 'not' Pj(c,z))
by MARGREL1:49
.=FALSE by MARGREL1:49;
hence thesis by A1,A2,MARGREL1:43;
end;
hence thesis;
end;
hence thesis;
end;
hence thesis;
end;
then A21:(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)
by BVFUNC_1:def 15;
A22:('not' a '&' b '&' c) 'or' (a '&' 'not' b '&' c) 'or' (a '&' b '&' 'not'
c) '<'
(a 'or' b) '&' 'not'( a '&' b '&' c) by Lm4;
('not' b '&' c '&' a) 'or' (b '&' 'not' c '&' a) 'or'
(b '&' c '&' 'not' a) '<'
(b 'or' c) '&' 'not'( b '&' c '&' a) by Lm4;
then ('not' b '&' c '&' a) 'or' (b '&' 'not' c '&' a) 'or'
(b '&' c '&' 'not' a) '<'
(b 'or' c) '&' 'not'( a '&' b '&' c) by BVFUNC_1:7;
then ('not' b '&' c '&' a) 'or' (b '&' 'not' c '&' a) 'or'
('not' a '&' b '&' c) '<'
(b 'or' c) '&' 'not'( a '&' b '&' c) by BVFUNC_1:7;
then (a '&' 'not' b '&' c) 'or' (b '&' 'not' c '&' a) 'or'
('not' a '&' b '&' c) '<'
(b 'or' c) '&' 'not'( a '&' b '&' c) by BVFUNC_1:7;
then (a '&' 'not' b '&' c) 'or' (a '&' b '&' 'not' c) 'or'
('not' a '&' b '&' c) '<'
(b 'or' c) '&' 'not'( a '&' b '&' c) by BVFUNC_1:7;
then A23:('not' a '&' b '&' c) 'or' (a '&' 'not' b '&' c) 'or'
(a '&' b '&' 'not' c) '<'
(b 'or' c) '&' 'not'( a '&' b '&' c) by BVFUNC_1:11;
('not' c '&' a '&' b) 'or' (c '&' 'not' a '&' b) 'or'
(c '&' a '&' 'not' b) '<'
(c 'or' a) '&' 'not'( c '&' a '&' b) by Lm4;
then ('not' c '&' a '&' b) 'or' (c '&' 'not' a '&' b) 'or'
(c '&' a '&' 'not' b) '<'
(c 'or' a) '&' 'not'( a '&' b '&' c) by BVFUNC_1:7;
then (a '&' b '&' 'not' c) 'or' (c '&' 'not' a '&' b) 'or'
(c '&' a '&' 'not' b) '<'
(c 'or' a) '&' 'not'( a '&' b '&' c) by BVFUNC_1:7;
then (a '&' b '&' 'not' c) 'or' ('not' a '&' b '&' c) 'or'
(c '&' a '&' 'not' b) '<'
(c 'or' a) '&' 'not'( a '&' b '&' c) by BVFUNC_1:7;
then (a '&' b '&' 'not' c) 'or' ('not' a '&' b '&' c) 'or'
(a '&' 'not' b '&' c) '<'
(c 'or' a) '&' 'not'( a '&' b '&' c) by BVFUNC_1:7;
then A24:('not' a '&' b '&' c) 'or' (a '&' 'not' b '&' c) 'or'
(a '&' b '&' 'not'
c) '<'
(c 'or' a) '&' 'not'( a '&' b '&' c) by BVFUNC_1:11;
A25:('not' a '&' b '&' c) 'or' (a '&' 'not' b '&' c) 'or'
(a '&' b '&' 'not'
c) 'imp'
(a 'or' b) '&' 'not'( a '&' b '&' c) = I_el(Y) by A22,BVFUNC_1:19;
A26:('not' a '&' b '&' c) 'or' (a '&' 'not' b '&' c) 'or'
(a '&' b '&' 'not' c) 'imp'
(b 'or' c) '&' 'not'( a '&' b '&' c) = I_el(Y) by A23,BVFUNC_1:19;
A27:('not' a '&' b '&' c) 'or' (a '&' 'not' b '&' c) 'or' (a '&' b '&' 'not'
c) 'imp'
(c 'or' a) '&' 'not'( a '&' b '&' c) = I_el(Y) by A24,BVFUNC_1:19;
('not' a '&' b '&' c) 'or' (a '&' 'not' b '&' c) 'or' (a '&' b '&' 'not'
c) 'imp'
(a 'or' b) '&' 'not'( a '&' b '&' c) '&' ((b 'or' c) '&'
'not'( a '&' b '&' c))
= I_el(Y) by A25,A26,BVFUNC_6:18;
then ('not' a '&' b '&' c) 'or' (a '&' 'not' b '&' c) 'or' (a '&' b '&'
'not'
c) 'imp'
(a 'or' b) '&' 'not'( a '&' b '&' c) '&' (b 'or' c) '&' 'not'( a '&' b '&' c)
= I_el(Y) by BVFUNC_1:7;
then ('not' a '&' b '&' c) 'or' (a '&' 'not' b '&' c) 'or' (a '&' b '&'
'not'
c) 'imp'
(a 'or' b) '&' (b 'or' c) '&' 'not'( a '&' b '&' c) '&' 'not'( a '&' b '&' c)
= I_el(Y) by BVFUNC_1:7;
then ('not' a '&' b '&' c) 'or' (a '&' 'not' b '&' c) 'or' (a '&' b '&'
'not'
c) 'imp'
(a 'or' b) '&' (b 'or' c) '&' ('not'( a '&' b '&' c) '&'
'not'( a '&' b '&' c))
= I_el(Y) by BVFUNC_1:7;
then ('not' a '&' b '&' c) 'or' (a '&' 'not' b '&' c) 'or' (a '&' b '&'
'not'
c) 'imp'
(a 'or' b) '&' (b 'or' c) '&' 'not'( a '&' b '&' c)
= I_el(Y) by BVFUNC_1:6;
then A28:('not' a '&' b '&' c) 'or' (a '&' 'not' b '&' c) 'or' (a '&' b '&'
'not'
c) 'imp'
(a 'or' b) '&' (b 'or' c) '&' 'not'( a '&' b '&' c) '&'
((c 'or' a) '&' 'not'( a '&' b '&' c))
= I_el(Y) by A27,BVFUNC_6:18;
(a 'or' b) '&' (b 'or' c) '&' 'not'( a '&' b '&' c) '&'
((c 'or' a) '&' 'not'( a '&' b '&' c))
=(a 'or' b) '&' (b 'or' c) '&' 'not'( a '&' b '&' c) '&'
(c 'or' a) '&' 'not'( a '&' b '&' c) by BVFUNC_1:7
.=(a 'or' b) '&' (b 'or' c) '&' (c 'or' a) '&' 'not'( a '&' b '&' c) '&'
'not'( a '&' b '&' c) by BVFUNC_1:7
.=(a 'or' b) '&' (b 'or' c) '&' (c 'or' a) '&' ('not'( a '&' b '&' c) '&'
'not'( a '&' b '&' c)) by BVFUNC_1:7
.=(a 'or' b) '&' (b 'or' c) '&' (c 'or' a) '&' 'not'( a '&' b '&' c)
by BVFUNC_1:6;
then ('not' a '&' b '&' c) 'or' (a '&' 'not' b '&' c) 'or'
(a '&' b '&' 'not' c) '<'
(a 'or' b) '&' (b 'or' c) '&' (c 'or' a) '&' 'not'( a '&' b '&' c)
by A28,BVFUNC_1:19;
hence thesis by A21,BVFUNC_1:18;
end;
theorem for a,b,c being Element of Funcs(Y,BOOLEAN) holds
(a 'imp' b) '&' (b 'imp' c) '<' (a 'imp' (b '&' c))
proof
let a,b,c be Element of Funcs(Y,BOOLEAN);
let z be Element of Y;
assume A1:
Pj((a 'imp' b) '&' (b 'imp' c),z)=TRUE;
A2: Pj((a 'imp' b) '&' (b 'imp' c),z)
=Pj(a 'imp' b,z) '&' Pj(b 'imp' c,z) by VALUAT_1:def 6
.=Pj('not' a 'or' b,z) '&' Pj(b 'imp' c,z) by BVFUNC_4:8
.=Pj('not' a 'or' b,z) '&' Pj('not' b 'or' c,z) by BVFUNC_4:8
.=(Pj('not' a,z) 'or' Pj(b,z)) '&' Pj('not' b 'or' c,z) by BVFUNC_1:def 7
.=(Pj('not' a,z) 'or' Pj(b,z)) '&' (Pj('not'
b,z) 'or' Pj(c,z)) by BVFUNC_1:def 7;
now assume
A3: Pj(a 'imp' (b '&' c),z)<>TRUE;
A4: 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
.='not' Pj(a,z) 'or' (Pj(b,z) '&' Pj(c,z)) by VALUAT_1:def 5;
A5:'not' Pj(a,z)=TRUE or 'not' Pj(a,z)=FALSE by MARGREL1:39;
A6: (Pj(b,z) '&' Pj(c,z))=TRUE or (Pj(b,z) '&' Pj(c,z))=FALSE
by MARGREL1:39;
A7: Pj('not' a,z)=FALSE by A3,A4,A5,BINARITH:19,VALUAT_1:def 5;
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' b,z) 'or' Pj(c,z))
=FALSE '&' (Pj('not' b,z) 'or' Pj(c,z)) by A7,BINARITH:7
.=FALSE by MARGREL1:49;
hence thesis by A1,A2,MARGREL1:43;
case Pj(c,z)=FALSE;
then (Pj('not' a,z) 'or' Pj(b,z)) '&' (Pj('not' b,z) 'or' Pj(c,z))
=Pj(b,z) '&' (Pj('not' b,z) 'or' FALSE) by A7,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 thesis by A1,A2,MARGREL1:43;
end;
hence thesis;
end;
hence thesis;
end;
theorem for a,b,c being Element of Funcs(Y,BOOLEAN) holds
(a 'imp' b) '&' (b 'imp' c) '<' ((a 'or' b) 'imp' c)
proof
let a,b,c be Element of Funcs(Y,BOOLEAN);
let z be Element of Y;
assume A1:
Pj((a 'imp' b) '&' (b 'imp' c),z)=TRUE;
A2: Pj((a 'imp' b) '&' (b 'imp' c),z)
=Pj(a 'imp' b,z) '&' Pj(b 'imp' c,z) by VALUAT_1:def 6
.=Pj('not' a 'or' b,z) '&' Pj(b 'imp' c,z) by BVFUNC_4:8
.=Pj('not' a 'or' b,z) '&' Pj('not' b 'or' c,z) by BVFUNC_4:8
.=(Pj('not' a,z) 'or' Pj(b,z)) '&' Pj('not' b 'or' c,z) by BVFUNC_1:def 7
.=(Pj('not' a,z) 'or' Pj(b,z)) '&' (Pj('not'
b,z) 'or' Pj(c,z)) by BVFUNC_1:def 7;
now assume
A3: Pj((a 'or' b) 'imp' c,z)<>TRUE;
A4: 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;
A5:(Pj('not' a,z) '&' Pj('not' b,z))=TRUE or (Pj('not' a,z) '&' Pj('not'
b,z))=FALSE
by MARGREL1:39;
A6: Pj(c,z)=TRUE or Pj(c,z)=FALSE
by MARGREL1:39;
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' b,z) 'or' Pj(c,z))
=Pj(b,z) '&' (Pj('not' b,z) 'or' FALSE) by A3,A4,A6,BINARITH:7,19
.=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 thesis by A1,A2,MARGREL1:43;
case Pj('not' b,z)=FALSE;
then (Pj('not' a,z) 'or' Pj(b,z)) '&' (Pj('not' b,z) 'or' Pj(c,z))
=(Pj('not' a,z) 'or' Pj(b,z)) '&' FALSE by A3,A4,A5,BINARITH:19,MARGREL1:
43
.=FALSE by MARGREL1:49;
hence thesis by A1,A2,MARGREL1:43;
end;
hence thesis;
end;
hence thesis;
end;
theorem Th19: for a,b,c being Element of Funcs(Y,BOOLEAN) holds
(a 'imp' b) '&' (b 'imp' c) '<' (a 'imp' (b 'or' c))
proof
let a,b,c be Element of Funcs(Y,BOOLEAN);
let z be Element of Y;
assume A1:
Pj((a 'imp' b) '&' (b 'imp' c),z)=TRUE;
A2: Pj((a 'imp' b) '&' (b 'imp' c),z)
=Pj(a 'imp' b,z) '&' Pj(b 'imp' c,z) by VALUAT_1:def 6
.=Pj('not' a 'or' b,z) '&' Pj(b 'imp' c,z) by BVFUNC_4:8
.=Pj('not' a 'or' b,z) '&' Pj('not' b 'or' c,z) by BVFUNC_4:8
.=(Pj('not' a,z) 'or' Pj(b,z)) '&' Pj('not' b 'or' c,z) by BVFUNC_1:def 7
.=(Pj('not' a,z) 'or' Pj(b,z)) '&' (Pj('not'
b,z) 'or' Pj(c,z)) by BVFUNC_1:def 7;
now assume
A3: Pj(a 'imp' (b 'or' c),z)<>TRUE;
A4: 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;
A5:Pj('not' a,z)=TRUE or Pj('not' a,z)=FALSE
by MARGREL1:39;
A6: (Pj(b,z) 'or' Pj(c,z))=TRUE or (Pj(b,z) 'or' Pj(c,z))=FALSE
by MARGREL1:39;
A7: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,A6,A7,BINARITH:19;
hence thesis by A1,A2,A4,A5,A6,BINARITH:19,MARGREL1:49;
end;
hence thesis;
end;
theorem Th20: for a,b,c being Element of Funcs(Y,BOOLEAN) holds
(a 'imp' b) '&' (b 'imp' c) '<' (a 'imp' (b 'or' 'not' c))
proof
let a,b,c be Element of Funcs(Y,BOOLEAN);
let z be Element of Y;
assume A1:
Pj((a 'imp' b) '&' (b 'imp' c),z)=TRUE;
A2: Pj((a 'imp' b) '&' (b 'imp' c),z)
=Pj(a 'imp' b,z) '&' Pj(b 'imp' c,z) by VALUAT_1:def 6
.=Pj('not' a 'or' b,z) '&' Pj(b 'imp' c,z) by BVFUNC_4:8
.=Pj('not' a 'or' b,z) '&' Pj('not' b 'or' c,z) by BVFUNC_4:8
.=(Pj('not' a,z) 'or' Pj(b,z)) '&' Pj('not' b 'or' c,z) by BVFUNC_1:def 7
.=(Pj('not' a,z) 'or' Pj(b,z)) '&' (Pj('not'
b,z) 'or' Pj(c,z)) by BVFUNC_1:def 7;
now assume
A3: Pj(a 'imp' (b 'or' 'not' c),z)<>TRUE;
A4: Pj(a 'imp' (b 'or' 'not' c),z)
=Pj('not' a 'or' (b 'or' 'not' c),z) by BVFUNC_4:8
.=Pj('not' a,z) 'or' Pj(b 'or' 'not' c,z) by BVFUNC_1:def 7
.=Pj('not' a,z) 'or' (Pj(b,z) 'or' Pj('not' c,z)) by BVFUNC_1:def 7;
A5:Pj('not' a,z)=TRUE or Pj('not' a,z)=FALSE
by MARGREL1:39;
A6: (Pj(b,z) 'or' Pj('not' c,z))=TRUE or (Pj(b,z) 'or' Pj('not' c,z))=
FALSE
by MARGREL1:39;
A7:Pj(b,z)=TRUE or Pj(b,z)=FALSE by MARGREL1:39;
Pj('not' c,z)=TRUE or Pj('not' c,z)=FALSE by MARGREL1:39;
then Pj(b,z)=FALSE & Pj('not' c,z)=FALSE by A3,A4,A6,A7,BINARITH:19;
hence thesis by A1,A2,A4,A5,A6,BINARITH:19,MARGREL1:49;
end;
hence thesis;
end;
theorem Th21: for a,b,c being Element of Funcs(Y,BOOLEAN) holds
(a 'imp' b) '&' (b 'imp' c) '<' (b 'imp' (c 'or' a))
proof
let a,b,c be Element of Funcs(Y,BOOLEAN);
let z be Element of Y;
assume A1:
Pj((a 'imp' b) '&' (b 'imp' c),z)=TRUE;
A2: Pj((a 'imp' b) '&' (b 'imp' c),z)
=Pj(a 'imp' b,z) '&' Pj(b 'imp' c,z) by VALUAT_1:def 6
.=Pj('not' a 'or' b,z) '&' Pj(b 'imp' c,z) by BVFUNC_4:8
.=Pj('not' a 'or' b,z) '&' Pj('not' b 'or' c,z) by BVFUNC_4:8
.=(Pj('not' a,z) 'or' Pj(b,z)) '&' Pj('not' b 'or' c,z) by BVFUNC_1:def 7
.=(Pj('not' a,z) 'or' Pj(b,z)) '&' (Pj('not'
b,z) 'or' Pj(c,z)) by BVFUNC_1:def 7;
now assume
A3: Pj(b 'imp' (c 'or' a),z)<>TRUE;
A4: Pj(b 'imp' (c 'or' a),z)
=Pj('not' b 'or' (c 'or' a),z) by BVFUNC_4:8
.=Pj('not' b,z) 'or' Pj(c 'or' a,z) by BVFUNC_1:def 7
.=Pj('not' b,z) 'or' (Pj(c,z) 'or' Pj(a,z)) by BVFUNC_1:def 7;
A5:Pj('not' b,z)=TRUE or Pj('not' b,z)=FALSE
by MARGREL1:39;
A6: (Pj(c,z) 'or' Pj(a,z))=TRUE or (Pj(c,z) 'or' Pj(a,z))=FALSE
by MARGREL1:39;
A7:Pj(c,z)=TRUE or Pj(c,z)=FALSE by MARGREL1:39;
Pj(a,z)=TRUE or Pj(a,z)=FALSE by MARGREL1:39;
then Pj(c,z)=FALSE & Pj(a,z)=FALSE by A3,A4,A6,A7,BINARITH:19;
hence thesis by A1,A2,A4,A5,A6,BINARITH:19,MARGREL1:49;
end;
hence thesis;
end;
theorem Th22: for a,b,c being Element of Funcs(Y,BOOLEAN) holds
(a 'imp' b) '&' (b 'imp' c) '<' (b 'imp' (c 'or' 'not' a))
proof
let a,b,c be Element of Funcs(Y,BOOLEAN);
let z be Element of Y;
assume A1:
Pj((a 'imp' b) '&' (b 'imp' c),z)=TRUE;
A2: Pj((a 'imp' b) '&' (b 'imp' c),z)
=Pj(a 'imp' b,z) '&' Pj(b 'imp' c,z) by VALUAT_1:def 6
.=Pj('not' a 'or' b,z) '&' Pj(b 'imp' c,z) by BVFUNC_4:8
.=Pj('not' a 'or' b,z) '&' Pj('not' b 'or' c,z) by BVFUNC_4:8
.=(Pj('not' a,z) 'or' Pj(b,z)) '&' Pj('not' b 'or' c,z) by BVFUNC_1:def 7
.=(Pj('not' a,z) 'or' Pj(b,z)) '&' (Pj('not'
b,z) 'or' Pj(c,z)) by BVFUNC_1:def 7;
now assume
A3: Pj(b 'imp' (c 'or' 'not' a),z)<>TRUE;
A4: Pj(b 'imp' (c 'or' 'not' a),z)
=Pj('not' b 'or' (c 'or' 'not' a),z) by BVFUNC_4:8
.=Pj('not' b,z) 'or' Pj(c 'or' 'not' a,z) by BVFUNC_1:def 7
.=Pj('not' b,z) 'or' (Pj(c,z) 'or' Pj('not' a,z)) by BVFUNC_1:def 7;
A5:Pj('not' b,z)=TRUE or Pj('not' b,z)=FALSE
by MARGREL1:39;
A6: (Pj(c,z) 'or' Pj('not' a,z))=TRUE or (Pj(c,z) 'or' Pj('not' a,z))=
FALSE
by MARGREL1:39;
A7:Pj(c,z)=TRUE or Pj(c,z)=FALSE by MARGREL1:39;
Pj('not' a,z)=TRUE or Pj('not' a,z)=FALSE by MARGREL1:39;
then Pj(c,z)=FALSE & Pj('not' a,z)=FALSE by A3,A4,A6,A7,BINARITH:19;
hence thesis by A1,A2,A4,A5,A6,BINARITH:19,MARGREL1:49;
end;
hence thesis;
end;
theorem 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
let a,b,c be Element of Funcs(Y,BOOLEAN);
(a 'imp' b) '&' (b 'imp' c) '<' (b 'imp' (c 'or' a)) by Th21;
then A1:(a 'imp' b) '&' (b 'imp' c) 'imp' (b 'imp' (c 'or' a))=I_el(Y)
by BVFUNC_1:19;
(a 'imp' b) '&' (b 'imp' c) 'imp' (a 'imp' b)=I_el(Y)
by BVFUNC_6:39;
then (a 'imp' b) '&' (b 'imp' c) 'imp'
(a 'imp' b) '&' (b 'imp' (c 'or' a))=I_el(Y)
by A1,BVFUNC_6:18;
hence thesis by BVFUNC_1:19;
end;
theorem 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
let a,b,c be Element of Funcs(Y,BOOLEAN);
(a 'imp' b) '&' (b 'imp' c) '<' (a 'imp' (b 'or' 'not' c)) by Th20;
then A1:(a 'imp' b) '&' (b 'imp' c) 'imp' (a 'imp' (b 'or' 'not' c))=I_el(Y)
by BVFUNC_1:19;
(a 'imp' b) '&' (b 'imp' c) 'imp' (b 'imp' c)=I_el(Y)
by BVFUNC_6:39;
then (a 'imp' b) '&' (b 'imp' c) 'imp'
(a 'imp' (b 'or' 'not' c)) '&' (b 'imp' c)=I_el(Y)
by A1,BVFUNC_6:18;
hence thesis by BVFUNC_1:19;
end;
theorem 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
let a,b,c be Element of Funcs(Y,BOOLEAN);
(a 'imp' b) '&' (b 'imp' c) '<' (a 'imp' (b 'or' c)) by Th19;
then A1:(a 'imp' b) '&' (b 'imp' c) 'imp' (a 'imp' (b 'or' c))=I_el(Y)
by BVFUNC_1:19;
(a 'imp' b) '&' (b 'imp' c) '<' (b 'imp' (c 'or' a)) by Th21;
then (a 'imp' b) '&' (b 'imp' c) 'imp' (b 'imp' (c 'or' a))=I_el(Y)
by BVFUNC_1:19;
then (a 'imp' b) '&' (b 'imp' c) 'imp'
(a 'imp' (b 'or' c)) '&' (b 'imp' (c 'or' a))=I_el(Y)
by A1,BVFUNC_6:18;
hence thesis by BVFUNC_1:19;
end;
theorem 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
let a,b,c be Element of Funcs(Y,BOOLEAN);
(a 'imp' b) '&' (b 'imp' c) '<' (a 'imp' (b 'or' 'not' c)) by Th20;
then A1:(a 'imp' b) '&' (b 'imp' c) 'imp' (a 'imp' (b 'or' 'not' c))=I_el(Y)
by BVFUNC_1:19;
(a 'imp' b) '&' (b 'imp' c) '<' (b 'imp' (c 'or' a)) by Th21;
then (a 'imp' b) '&' (b 'imp' c) 'imp' (b 'imp' (c 'or' a))=I_el(Y)
by BVFUNC_1:19;
then (a 'imp' b) '&' (b 'imp' c) 'imp'
(a 'imp' (b 'or' 'not' c)) '&' (b 'imp' (c 'or' a))=I_el(Y)
by A1,BVFUNC_6:18;
hence thesis by BVFUNC_1:19;
end;
theorem 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
let a,b,c be Element of Funcs(Y,BOOLEAN);
(a 'imp' b) '&' (b 'imp' c) '<' (a 'imp' (b 'or' 'not' c)) by Th20;
then A1:(a 'imp' b) '&' (b 'imp' c) 'imp' (a 'imp' (b 'or' 'not' c))=I_el(Y)
by BVFUNC_1:19;
(a 'imp' b) '&' (b 'imp' c) '<' (b 'imp' (c 'or' 'not' a)) by Th22;
then (a 'imp' b) '&' (b 'imp' c) 'imp' (b 'imp' (c 'or' 'not' a))=I_el(Y)
by BVFUNC_1:19;
then (a 'imp' b) '&' (b 'imp' c) 'imp'
(a 'imp' (b 'or' 'not' c)) '&' (b 'imp' (c 'or' 'not' a))=I_el(Y)
by A1,BVFUNC_6:18;
hence thesis by BVFUNC_1:19;
end;