:: BVFUNC_5 semantic presentation

theorem Th1: :: BVFUNC_5:1
for b1 being non empty set
for b2, b3 being Element of Funcs b1,BOOLEAN holds
( ( b2 = I_el b1 & b3 = I_el b1 ) iff b2 '&' b3 = I_el b1 )
proof
let c1 be non empty set ;
let c2, c3 be Element of Funcs c1,BOOLEAN ;
now
assume E1: c2 '&' c3 = I_el c1 ;
per cases not ( not ( c2 = I_el c1 & c3 = I_el c1 ) & not ( c2 = I_el c1 & c3 <> I_el c1 ) & not ( c2 <> I_el c1 & c3 = I_el c1 ) & not ( c2 <> I_el c1 & c3 <> I_el c1 ) ) ;
suppose ( c2 = I_el c1 & c3 = I_el c1 ) ;
hence ( c2 = I_el c1 & c3 = I_el c1 ) ;
end;
suppose ( c2 = I_el c1 & c3 <> I_el c1 ) ;
hence ( c2 = I_el c1 & c3 = I_el c1 ) by E1, BVFUNC_1:9;
end;
suppose ( c2 <> I_el c1 & c3 = I_el c1 ) ;
hence ( c2 = I_el c1 & c3 = I_el c1 ) by E1, BVFUNC_1:9;
end;
suppose E2: ( c2 <> I_el c1 & c3 <> I_el c1 ) ;
for b1 being Element of c1 holds c2 . b1 = TRUE
proof
let c4 be Element of c1;
(c2 '&' c3) . c4 = TRUE by E1, BVFUNC_1:def 14;
then (c2 . c4) '&' (c3 . c4) = TRUE by VALUAT_1:def 6;
hence c2 . c4 = TRUE by MARGREL1:45;
end;
hence ( c2 = I_el c1 & c3 = I_el c1 ) by E2, BVFUNC_1:def 14;
end;
end;
end;
hence ( ( c2 = I_el c1 & c3 = I_el c1 ) iff c2 '&' c3 = I_el c1 ) by BVFUNC_1:9;
end;

theorem Th2: :: BVFUNC_5:2
for b1 being non empty set
for b2 being Element of Funcs b1,BOOLEAN holds
( (I_el b1) 'imp' b2 = I_el b1 implies b2 = I_el b1 )
proof
let c1 be non empty set ;
set c2 = I_el c1;
let c3 be Element of Funcs c1,BOOLEAN ;
assume E2: (I_el c1) 'imp' c3 = I_el c1 ;
for b1 being Element of c1 holds c3 . b1 = TRUE
proof
let c4 be Element of c1;
E3: (I_el c1) . c4 = TRUE by BVFUNC_1:def 14;
((I_el c1) 'imp' c3) . c4 = TRUE by E2, BVFUNC_1:def 14;
then ('not' ((I_el c1) . c4)) 'or' (c3 . c4) = TRUE by BVFUNC_1:def 11;
then FALSE 'or' (c3 . c4) = TRUE by E3, MARGREL1:41;
hence c3 . c4 = TRUE by BINARITH:7;
end;
hence c3 = I_el c1 by BVFUNC_1:def 14;
end;

theorem Th3: :: BVFUNC_5:3
for b1 being non empty set
for b2, b3 being Element of Funcs b1,BOOLEAN holds
( b2 = I_el b1 implies b2 'or' b3 = I_el b1 )
proof
let c1 be non empty set ;
let c2, c3 be Element of Funcs c1,BOOLEAN ;
assume E2: c2 = I_el c1 ;
for b1 being Element of c1 holds (c2 'or' c3) . b1 = TRUE
proof
let c4 be Element of c1;
c2 . c4 = TRUE by E2, BVFUNC_1:def 14;
then (c2 'or' c3) . c4 = TRUE 'or' (c3 . c4) by BVFUNC_1:def 7
.= TRUE by BINARITH:19 ;
hence (c2 'or' c3) . c4 = TRUE ;
end;
hence c2 'or' c3 = I_el c1 by BVFUNC_1:def 14;
end;

theorem Th4: :: BVFUNC_5:4
canceled;

theorem Th5: :: BVFUNC_5:5
for b1 being non empty set
for b2, b3 being Element of Funcs b1,BOOLEAN holds
( b3 = I_el b1 implies b2 'imp' b3 = I_el b1 )
proof
let c1 be non empty set ;
let c2, c3 be Element of Funcs c1,BOOLEAN ;
assume E2: c3 = I_el c1 ;
for b1 being Element of c1 holds (c2 'imp' c3) . b1 = TRUE
proof
let c4 be Element of c1;
c3 . c4 = TRUE by E2, BVFUNC_1:def 14;
then (c2 'imp' c3) . c4 = ('not' (c2 . c4)) 'or' TRUE by BVFUNC_1:def 11
.= TRUE by BINARITH:19 ;
hence (c2 'imp' c3) . c4 = TRUE ;
end;
hence c2 'imp' c3 = I_el c1 by BVFUNC_1:def 14;
end;

theorem Th6: :: BVFUNC_5:6
for b1 being non empty set
for b2, b3 being Element of Funcs b1,BOOLEAN holds
( 'not' b2 = I_el b1 implies b2 'imp' b3 = I_el b1 )
proof
let c1 be non empty set ;
let c2, c3 be Element of Funcs c1,BOOLEAN ;
assume E2: 'not' c2 = I_el c1 ;
for b1 being Element of c1 holds (c2 'imp' c3) . b1 = TRUE
proof
let c4 be Element of c1;
('not' c2) . c4 = TRUE by E2, BVFUNC_1:def 14;
then 'not' (c2 . c4) = TRUE by VALUAT_1:def 5;
then (c2 'imp' c3) . c4 = TRUE 'or' (c3 . c4) by BVFUNC_1:def 11
.= TRUE by BINARITH:19 ;
hence (c2 'imp' c3) . c4 = TRUE ;
end;
hence c2 'imp' c3 = I_el c1 by BVFUNC_1:def 14;
end;

theorem Th7: :: BVFUNC_5:7
for b1 being non empty set
for b2 being Element of Funcs b1,BOOLEAN holds 'not' (b2 '&' ('not' b2)) = I_el b1
proof
let c1 be non empty set ;
let c2 be Element of Funcs c1,BOOLEAN ;
E2: for b1 being Element of c1 holds (c2 '&' ('not' c2)) . b1 = (O_el c1) . b1
proof
let c3 be Element of c1;
E3: (c2 '&' ('not' c2)) . c3 = (c2 . c3) '&' (('not' c2) . c3) by VALUAT_1:def 6
.= (c2 . c3) '&' ('not' (c2 . c3)) by VALUAT_1:def 5 ;
E4: ( 'not' FALSE = TRUE & 'not' TRUE = FALSE ) by MARGREL1:41;
E5: (O_el c1) . c3 = FALSE by BVFUNC_1:def 13;
now
per cases ( c2 . c3 = TRUE or c2 . c3 = FALSE ) by MARGREL1:39;
case c2 . c3 = TRUE ;
hence (c2 '&' ('not' c2)) . c3 = (O_el c1) . c3 by E3, E4, E5, MARGREL1:45;
end;
case c2 . c3 = FALSE ;
hence (c2 '&' ('not' c2)) . c3 = (O_el c1) . c3 by E3, E5, MARGREL1:45;
end;
end;
end;
hence (c2 '&' ('not' c2)) . c3 = (O_el c1) . c3 ;
end;
consider c3 being Function such that
E3: ( c2 '&' ('not' c2) = c3 & dom c3 = c1 & rng c3 c= BOOLEAN ) by FUNCT_2:def 2;
consider c4 being Function such that
E4: ( O_el c1 = c4 & dom c4 = c1 & rng c4 c= BOOLEAN ) by FUNCT_2:def 2;
( c1 = dom c3 & c1 = dom c4 & ( for b1 being set holds
( b1 in c1 implies c3 . b1 = c4 . b1 ) ) ) by E2, E3, E4;
then c2 '&' ('not' c2) = O_el c1 by E3, E4, FUNCT_1:9;
hence 'not' (c2 '&' ('not' c2)) = I_el c1 by BVFUNC_1:5;
end;

theorem Th8: :: BVFUNC_5:8
for b1 being non empty set
for b2 being Element of Funcs b1,BOOLEAN holds b2 'imp' b2 = I_el b1
proof
let c1 be non empty set ;
let c2 be Element of Funcs c1,BOOLEAN ;
E2: for b1 being Element of c1 holds (c2 'imp' c2) . b1 = (I_el c1) . b1
proof
let c3 be Element of c1;
E3: (c2 'imp' c2) . c3 = ('not' (c2 . c3)) 'or' (c2 . c3) by BVFUNC_1:def 11;
E4: ( 'not' FALSE = TRUE & 'not' TRUE = FALSE ) by MARGREL1:41;
E5: (I_el c1) . c3 = TRUE by BVFUNC_1:def 14;
now
per cases ( c2 . c3 = TRUE or c2 . c3 = FALSE ) by MARGREL1:39;
case c2 . c3 = TRUE ;
hence (c2 'imp' c2) . c3 = (I_el c1) . c3 by E3, E5, BINARITH:19;
end;
case c2 . c3 = FALSE ;
hence (c2 'imp' c2) . c3 = (I_el c1) . c3 by E3, E4, E5, BINARITH:19;
end;
end;
end;
hence (c2 'imp' c2) . c3 = (I_el c1) . c3 ;
end;
consider c3 being Function such that
E3: ( c2 'imp' c2 = c3 & dom c3 = c1 & rng c3 c= BOOLEAN ) by FUNCT_2:def 2;
consider c4 being Function such that
E4: ( I_el c1 = c4 & dom c4 = c1 & rng c4 c= BOOLEAN ) by FUNCT_2:def 2;
for b1 being set holds
( b1 in c1 implies c3 . b1 = c4 . b1 ) by E2, E3, E4;
hence c2 'imp' c2 = I_el c1 by E3, E4, FUNCT_1:9;
end;

theorem Th9: :: BVFUNC_5:9
for b1 being non empty set
for b2, b3 being Element of Funcs b1,BOOLEAN holds
( b2 'imp' b3 = I_el b1 iff ('not' b3) 'imp' ('not' b2) = I_el b1 )
proof
let c1 be non empty set ;
let c2, c3 be Element of Funcs c1,BOOLEAN ;
E2: now
assume E3: c2 'imp' c3 = I_el c1 ;
for b1 being Element of c1 holds (('not' c3) 'imp' ('not' c2)) . b1 = TRUE
proof
let c4 be Element of c1;
(c2 'imp' c3) . c4 = TRUE by E3, BVFUNC_1:def 14;
then E4: ('not' (c2 . c4)) 'or' (c3 . c4) = TRUE by BVFUNC_1:def 11;
E5: ( 'not' (c2 . c4) = TRUE or 'not' (c2 . c4) = FALSE ) by MARGREL1:39;
now
per cases ( 'not' (c2 . c4) = TRUE or c3 . c4 = TRUE ) by E4, E5, BINARITH:7;
case E6: 'not' (c2 . c4) = TRUE ;
(('not' c3) 'imp' ('not' c2)) . c4 = ('not' (('not' c3) . c4)) 'or' (('not' c2) . c4) by BVFUNC_1:def 11
.= ('not' (('not' c3) . c4)) 'or' TRUE by E6, VALUAT_1:def 5
.= TRUE by BINARITH:19 ;
hence (('not' c3) 'imp' ('not' c2)) . c4 = TRUE ;
end;
case E6: c3 . c4 = TRUE ;
('not' c3) . c4 = 'not' (c3 . c4) by VALUAT_1:def 5;
then (('not' c3) 'imp' ('not' c2)) . c4 = ('not' ('not' (c3 . c4))) 'or' (('not' c2) . c4) by BVFUNC_1:def 11
.= TRUE 'or' (('not' c2) . c4) by E6
.= TRUE by BINARITH:19 ;
hence (('not' c3) 'imp' ('not' c2)) . c4 = TRUE ;
end;
end;
end;
hence (('not' c3) 'imp' ('not' c2)) . c4 = TRUE ;
end;
hence ('not' c3) 'imp' ('not' c2) = I_el c1 by BVFUNC_1:def 14;
end;
now
assume E3: ('not' c3) 'imp' ('not' c2) = I_el c1 ;
for b1 being Element of c1 holds (c2 'imp' c3) . b1 = TRUE
proof
let c4 be Element of c1;
(('not' c3) 'imp' ('not' c2)) . c4 = TRUE by E3, BVFUNC_1:def 14;
then ('not' (('not' c3) . c4)) 'or' (('not' c2) . c4) = TRUE by BVFUNC_1:def 11;
then ('not' ('not' (c3 . c4))) 'or' (('not' c2) . c4) = TRUE by VALUAT_1:def 5;
then ('not' ('not' (c3 . c4))) 'or' ('not' (c2 . c4)) = TRUE by VALUAT_1:def 5;
then E4: (c3 . c4) 'or' ('not' (c2 . c4)) = TRUE ;
E5: ( 'not' (c2 . c4) = TRUE or 'not' (c2 . c4) = FALSE ) by MARGREL1:39;
now
per cases ( 'not' (c2 . c4) = TRUE or c3 . c4 = TRUE ) by E4, E5, BINARITH:7;
case 'not' (c2 . c4) = TRUE ;
then (c2 'imp' c3) . c4 = TRUE 'or' (c3 . c4) by BVFUNC_1:def 11
.= TRUE by BINARITH:19 ;
hence (c2 'imp' c3) . c4 = TRUE ;
end;
case c3 . c4 = TRUE ;
then (c2 'imp' c3) . c4 = ('not' (c2 . c4)) 'or' TRUE by BVFUNC_1:def 11
.= TRUE by BINARITH:19 ;
hence (c2 'imp' c3) . c4 = TRUE ;
end;
end;
end;
hence (c2 'imp' c3) . c4 = TRUE ;
end;
hence c2 'imp' c3 = I_el c1 by BVFUNC_1:def 14;
end;
hence ( c2 'imp' c3 = I_el c1 iff ('not' c3) 'imp' ('not' c2) = I_el c1 ) by E2;
end;

theorem Th10: :: BVFUNC_5:10
for b1 being non empty set
for b2, b3, b4 being Element of Funcs b1,BOOLEAN holds
( b2 'imp' b3 = I_el b1 & b3 'imp' b4 = I_el b1 implies b2 'imp' b4 = I_el b1 )
proof
let c1 be non empty set ;
let c2, c3, c4 be Element of Funcs c1,BOOLEAN ;
assume E2: ( c2 'imp' c3 = I_el c1 & c3 'imp' c4 = I_el c1 ) ;
for b1 being Element of c1 holds (c2 'imp' c4) . b1 = TRUE
proof
let c5 be Element of c1;
(c2 'imp' c3) . c5 = TRUE by E2, BVFUNC_1:def 14;
then E3: ('not' (c2 . c5)) 'or' (c3 . c5) = TRUE by BVFUNC_1:def 11;
E4: ( 'not' (c2 . c5) = TRUE or 'not' (c2 . c5) = FALSE ) by MARGREL1:39;
(c3 'imp' c4) . c5 = TRUE by E2, BVFUNC_1:def 14;
then E5: ('not' (c3 . c5)) 'or' (c4 . c5) = TRUE by BVFUNC_1:def 11;
E6: ( 'not' (c3 . c5) = TRUE or 'not' (c3 . c5) = FALSE ) by MARGREL1:39;
E7: (c2 'imp' c4) . c5 = ('not' (c2 . c5)) 'or' (c4 . c5) by BVFUNC_1:def 11;
now
per cases not ( not ( 'not' (c2 . c5) = TRUE & 'not' (c3 . c5) = TRUE ) & not ( 'not' (c2 . c5) = TRUE & c4 . c5 = TRUE ) & not ( c3 . c5 = TRUE & 'not' (c3 . c5) = TRUE ) & not ( c3 . c5 = TRUE & c4 . c5 = TRUE ) ) by E3, E4, E5, E6, BINARITH:7;
case ( 'not' (c2 . c5) = TRUE & 'not' (c3 . c5) = TRUE ) ;
hence (c2 'imp' c4) . c5 = TRUE by E7, BINARITH:19;
end;
case ( 'not' (c2 . c5) = TRUE & c4 . c5 = TRUE ) ;
hence (c2 'imp' c4) . c5 = TRUE by E7, BINARITH:19;
end;
case E8: ( c3 . c5 = TRUE & 'not' (c3 . c5) = TRUE ) ;
then c3 . c5 = FALSE by MARGREL1:41;
hence (c2 'imp' c4) . c5 = TRUE by E8, MARGREL1:43;
end;
case ( c3 . c5 = TRUE & c4 . c5 = TRUE ) ;
hence (c2 'imp' c4) . c5 = TRUE by E7, BINARITH:19;
end;
end;
end;
hence (c2 'imp' c4) . c5 = TRUE ;
end;
hence c2 'imp' c4 = I_el c1 by BVFUNC_1:def 14;
end;

theorem Th11: :: BVFUNC_5:11
for b1 being non empty set
for b2, b3 being Element of Funcs b1,BOOLEAN holds
( b2 'imp' b3 = I_el b1 & b2 'imp' ('not' b3) = I_el b1 implies 'not' b2 = I_el b1 )
proof
let c1 be non empty set ;
let c2, c3 be Element of Funcs c1,BOOLEAN ;
assume E2: ( c2 'imp' c3 = I_el c1 & c2 'imp' ('not' c3) = I_el c1 ) ;
for b1 being Element of c1 holds ('not' c2) . b1 = TRUE
proof
let c4 be Element of c1;
(c2 'imp' c3) . c4 = TRUE by E2, BVFUNC_1:def 14;
then E3: ('not' (c2 . c4)) 'or' (c3 . c4) = TRUE by BVFUNC_1:def 11;
E4: ( 'not' (c2 . c4) = TRUE or 'not' (c2 . c4) = FALSE ) by MARGREL1:39;
(c2 'imp' ('not' c3)) . c4 = TRUE by E2, BVFUNC_1:def 14;
then E5: ('not' (c2 . c4)) 'or' (('not' c3) . c4) = TRUE by BVFUNC_1:def 11;
now
per cases not ( not ( 'not' (c2 . c4) = TRUE & 'not' (c2 . c4) = TRUE ) & not ( 'not' (c2 . c4) = TRUE & ('not' c3) . c4 = TRUE ) & not ( c3 . c4 = TRUE & 'not' (c2 . c4) = TRUE ) & not ( c3 . c4 = TRUE & ('not' c3) . c4 = TRUE ) ) by E3, E4, E5, BINARITH:7;
case ( 'not' (c2 . c4) = TRUE & 'not' (c2 . c4) = TRUE ) ;
hence ('not' c2) . c4 = TRUE by VALUAT_1:def 5;
end;
case ( 'not' (c2 . c4) = TRUE & ('not' c3) . c4 = TRUE ) ;
hence ('not' c2) . c4 = TRUE by VALUAT_1:def 5;
end;
case ( c3 . c4 = TRUE & 'not' (c2 . c4) = TRUE ) ;
hence ('not' c2) . c4 = TRUE by VALUAT_1:def 5;
end;
case E6: ( c3 . c4 = TRUE & ('not' c3) . c4 = TRUE ) ;
then 'not' (c3 . c4) = TRUE by VALUAT_1:def 5;
then c3 . c4 = FALSE by MARGREL1:41;
hence ('not' c2) . c4 = TRUE by E6, MARGREL1:43;
end;
end;
end;
hence ('not' c2) . c4 = TRUE ;
end;
hence 'not' c2 = I_el c1 by BVFUNC_1:def 14;
end;

theorem Th12: :: BVFUNC_5:12
for b1 being non empty set
for b2 being Element of Funcs b1,BOOLEAN holds (('not' b2) 'imp' b2) 'imp' b2 = I_el b1
proof
let c1 be non empty set ;
let c2 be Element of Funcs c1,BOOLEAN ;
E2: for b1 being Element of c1 holds ((('not' c2) 'imp' c2) 'imp' c2) . b1 = (I_el c1) . b1
proof
let c3 be Element of c1;
E3: 'not' (('not' (('not' c2) . c3)) 'or' (c2 . c3)) = 'not' (('not' ('not' (c2 . c3))) 'or' (c2 . c3)) by VALUAT_1:def 5
.= 'not' ((c2 . c3) 'or' (c2 . c3))
.= 'not' (c2 . c3) by BINARITH:21 ;
E4: ((('not' c2) 'imp' c2) 'imp' c2) . c3 = ('not' ((('not' c2) 'imp' c2) . c3)) 'or' (c2 . c3) by BVFUNC_1:def 11
.= ('not' (c2 . c3)) 'or' (c2 . c3) by E3, BVFUNC_1:def 11 ;
E5: (I_el c1) . c3 = TRUE by BVFUNC_1:def 14;
now
per cases ( c2 . c3 = TRUE or c2 . c3 = FALSE ) by MARGREL1:39;
case c2 . c3 = TRUE ;
hence ((('not' c2) 'imp' c2) 'imp' c2) . c3 = (I_el c1) . c3 by E4, E5, BINARITH:19;
end;
case c2 . c3 = FALSE ;
then ((('not' c2) 'imp' c2) 'imp' c2) . c3 = TRUE 'or' FALSE by E4, MARGREL1:41
.= TRUE by BINARITH:19 ;
hence ((('not' c2) 'imp' c2) 'imp' c2) . c3 = (I_el c1) . c3 by BVFUNC_1:def 14;
end;
end;
end;
hence ((('not' c2) 'imp' c2) 'imp' c2) . c3 = (I_el c1) . c3 ;
end;
consider c3 being Function such that
E3: ( (('not' c2) 'imp' c2) 'imp' c2 = c3 & dom c3 = c1 & rng c3 c= BOOLEAN ) by FUNCT_2:def 2;
consider c4 being Function such that
E4: ( I_el c1 = c4 & dom c4 = c1 & rng c4 c= BOOLEAN ) by FUNCT_2:def 2;
( c1 = dom c3 & c1 = dom c4 & ( for b1 being set holds
( b1 in c1 implies c3 . b1 = c4 . b1 ) ) ) by E2, E3, E4;
hence (('not' c2) 'imp' c2) 'imp' c2 = I_el c1 by E3, E4, FUNCT_1:9;
end;

theorem Th13: :: BVFUNC_5:13
for b1 being non empty set
for b2, b3, b4 being Element of Funcs b1,BOOLEAN holds (b2 'imp' b3) 'imp' (('not' (b3 '&' b4)) 'imp' ('not' (b2 '&' b4))) = I_el b1
proof
let c1 be non empty set ;
let c2, c3, c4 be Element of Funcs c1,BOOLEAN ;
E2: for b1 being Element of c1 holds ((c2 'imp' c3) 'imp' (('not' (c3 '&' c4)) 'imp' ('not' (c2 '&' c4)))) . b1 = (I_el c1) . b1
proof
let c5 be Element of c1;
E3: ((c2 'imp' c3) 'imp' (('not' (c3 '&' c4)) 'imp' ('not' (c2 '&' c4)))) . c5 = ('not' ((c2 'imp' c3) . c5)) 'or' ((('not' (c3 '&' c4)) 'imp' ('not' (c2 '&' c4))) . c5) by BVFUNC_1:def 11
.= ('not' ((c2 'imp' c3) . c5)) 'or' (('not' (('not' (c3 '&' c4)) . c5)) 'or' (('not' (c2 '&' c4)) . c5)) by BVFUNC_1:def 11 ;
E4: 'not' (('not' (c3 '&' c4)) . c5) = 'not' ('not' ((c3 '&' c4) . c5)) by VALUAT_1:def 5
.= (c3 '&' c4) . c5
.= (c3 . c5) '&' (c4 . c5) by VALUAT_1:def 6 ;
E5: ('not' (c2 '&' c4)) . c5 = (('not' c2) 'or' ('not' c4)) . c5 by BVFUNC_1:17
.= (('not' c2) . c5) 'or' (('not' c4) . c5) by BVFUNC_1:def 7
.= ('not' (c2 . c5)) 'or' (('not' c4) . c5) by VALUAT_1:def 5
.= ('not' (c2 . c5)) 'or' ('not' (c4 . c5)) by VALUAT_1:def 5 ;
E6: 'not' ((c2 'imp' c3) . c5) = 'not' (('not' (c2 . c5)) 'or' (c3 . c5)) by BVFUNC_1:def 11
.= ('not' ('not' (c2 . c5))) '&' ('not' (c3 . c5)) by BINARITH:10
.= (c2 . c5) '&' ('not' (c3 . c5)) ;
E7: ('not' (('not' (c3 '&' c4)) . c5)) 'or' (('not' (c2 '&' c4)) . c5) = ((('not' (c2 . c5)) 'or' ('not' (c4 . c5))) 'or' (c3 . c5)) '&' ((('not' (c2 . c5)) 'or' ('not' (c4 . c5))) 'or' (c4 . c5)) by E4, E5, BINARITH:23
.= ((('not' (c2 . c5)) 'or' ('not' (c4 . c5))) 'or' (c3 . c5)) '&' (('not' (c2 . c5)) 'or' (('not' (c4 . c5)) 'or' (c4 . c5))) by BINARITH:20 ;
now
per cases ( c4 . c5 = TRUE or c4 . c5 = FALSE ) by MARGREL1:39;
case c4 . c5 = TRUE ;
hence ('not' (c4 . c5)) 'or' (c4 . c5) = TRUE by BINARITH:19;
end;
case c4 . c5 = FALSE ;
then ('not' (c4 . c5)) 'or' (c4 . c5) = TRUE 'or' FALSE by MARGREL1:41
.= TRUE by BINARITH:19 ;
hence ('not' (c4 . c5)) 'or' (c4 . c5) = TRUE ;
end;
end;
end;
then ('not' (c2 . c5)) 'or' (('not' (c4 . c5)) 'or' (c4 . c5)) = TRUE by BINARITH:19;
then ((('not' (c2 . c5)) 'or' ('not' (c4 . c5))) 'or' (c3 . c5)) '&' (('not' (c2 . c5)) 'or' (('not' (c4 . c5)) 'or' (c4 . c5))) = (('not' (c2 . c5)) 'or' ('not' (c4 . c5))) 'or' (c3 . c5) by MARGREL1:50;
then E8: ('not' ((c2 'imp' c3) . c5)) 'or' (('not' (('not' (c3 '&' c4)) . c5)) 'or' (('not' (c2 '&' c4)) . c5)) = (((('not' (c2 . c5)) 'or' ('not' (c4 . c5))) 'or' (c3 . c5)) 'or' (c2 . c5)) '&' (((('not' (c2 . c5)) 'or' ('not' (c4 . c5))) 'or' (c3 . c5)) 'or' ('not' (c3 . c5))) by E6, E7, BINARITH:23
.= (((('not' (c2 . c5)) 'or' ('not' (c4 . c5))) 'or' (c3 . c5)) 'or' (c2 . c5)) '&' ((('not' (c2 . c5)) 'or' ('not' (c4 . c5))) 'or' ((c3 . c5) 'or' ('not' (c3 . c5)))) by BINARITH:20
.= (((('not' (c4 . c5)) 'or' ('not' (c2 . c5))) 'or' (c2 . c5)) 'or' (c3 . c5)) '&' ((('not' (c2 . c5)) 'or' ('not' (c4 . c5))) 'or' ((c3 . c5) 'or' ('not' (c3 . c5)))) by BINARITH:20
.= ((('not'