:: BVFUNC_5 semantic presentation

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

theorem :: 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 E1: 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 E1, 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 :: BVFUNC_5:4
canceled;

theorem :: 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 E1: 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 E1, 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 :: 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 E1: '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 E1, 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 :: 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 ;
E1: for b1 being Element of c1 holds (c2 '&' ('not' c2)) . b1 = (O_el c1) . b1
proof
let c3 be Element of c1;
E2: (c2 '&' ('not' c2)) . c3 = (c2 . c3) '&' (('not' c2) . c3) by VALUAT_1:def 6
.= (c2 . c3) '&' ('not' (c2 . c3)) by VALUAT_1:def 5 ;
E3: ( 'not' FALSE = TRUE & 'not' TRUE = FALSE ) by MARGREL1:41;
E4: (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 E2, E3, E4, MARGREL1:45;
end;
case c2 . c3 = FALSE ;
hence (c2 '&' ('not' c2)) . c3 = (O_el c1) . c3 by E2, E4, MARGREL1:45;
end;
end;
end;
hence (c2 '&' ('not' c2)) . c3 = (O_el c1) . c3 ;
end;
consider c3 being Function such that
E2: ( c2 '&' ('not' c2) = c3 & dom c3 = c1 & rng c3 c= BOOLEAN ) by FUNCT_2:def 2;
consider c4 being Function such that
E3: ( 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 E1, E2, E3;
then c2 '&' ('not' c2) = O_el c1 by E2, E3, FUNCT_1:9;
hence 'not' (c2 '&' ('not' c2)) = I_el c1 by BVFUNC_1:5;
end;

theorem :: 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 ;
E1: for b1 being Element of c1 holds (c2 'imp' c2) . b1 = (I_el c1) . b1
proof
let c3 be Element of c1;
E2: (c2 'imp' c2) . c3 = ('not' (c2 . c3)) 'or' (c2 . c3) by BVFUNC_1:def 11;
E3: ( 'not' FALSE = TRUE & 'not' TRUE = FALSE ) by MARGREL1:41;
E4: (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 E2, E4, BINARITH:19;
end;
case c2 . c3 = FALSE ;
hence (c2 'imp' c2) . c3 = (I_el c1) . c3 by E2, E3, E4, BINARITH:19;
end;
end;
end;
hence (c2 'imp' c2) . c3 = (I_el c1) . c3 ;
end;
consider c3 being Function such that
E2: ( c2 'imp' c2 = c3 & dom c3 = c1 & rng c3 c= BOOLEAN ) by FUNCT_2:def 2;
consider c4 being Function such that
E3: ( 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 E1, E2, E3;
hence c2 'imp' c2 = I_el c1 by E2, E3, FUNCT_1:9;
end;

theorem :: 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 ;
E1: now
assume E2: 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 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;
now
per cases ( 'not' (c2 . c4) = TRUE or c3 . c4 = TRUE ) by E3, E4, BINARITH:7;
case E5: '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 E5, VALUAT_1:def 5
.= TRUE by BINARITH:19 ;
hence (('not' c3) 'imp' ('not' c2)) . c4 = TRUE ;
end;
case E5: 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 E5, MARGREL1:40
.= 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 E2: ('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 E2, 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 E3: (c3 . c4) 'or' ('not' (c2 . c4)) = TRUE by MARGREL1:40;
E4: ( 'not' (c2 . c4) = TRUE or 'not' (c2 . c4) = FALSE ) by MARGREL1:39;
now
per cases ( 'not' (c2 . c4) = TRUE or c3 . c4 = TRUE ) by E3, E4, 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 E1;
end;

theorem :: 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 E1: ( 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 E1, BVFUNC_1:def 14;
then E2: ('not' (c2 . c5)) 'or' (c3 . c5) = TRUE by BVFUNC_1:def 11;
E3: ( 'not' (c2 . c5) = TRUE or 'not' (c2 . c5) = FALSE ) by MARGREL1:39;
(c3 'imp' c4) . c5 = TRUE by E1, BVFUNC_1:def 14;
then E4: ('not' (c3 . c5)) 'or' (c4 . c5) = TRUE by BVFUNC_1:def 11;
E5: ( 'not' (c3 . c5) = TRUE or 'not' (c3 . c5) = FALSE ) by MARGREL1:39;
E6: (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 E2, E3, E4, E5, BINARITH:7;
case ( 'not' (c2 . c5) = TRUE & 'not' (c3 . c5) = TRUE ) ;
hence (c2 'imp' c4) . c5 = TRUE by E6, BINARITH:19;
end;
case ( 'not' (c2 . c5) = TRUE & c4 . c5 = TRUE ) ;
hence (c2 'imp' c4) . c5 = TRUE by E6, BINARITH:19;
end;
case E7: ( c3 . c5 = TRUE & 'not' (c3 . c5) = TRUE ) ;
then c3 . c5 = FALSE by MARGREL1:41;
hence (c2 'imp' c4) . c5 = TRUE by E7, MARGREL1:43;
end;
case ( c3 . c5 = TRUE & c4 . c5 = TRUE ) ;
hence (c2 'imp' c4) . c5 = TRUE by E6, 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 :: 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 E1: ( 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 E1, BVFUNC_1:def 14;
then E2: ('not' (c2 . c4)) 'or' (c3 . c4) = TRUE by BVFUNC_1:def 11;
E3: ( 'not' (c2 . c4) = TRUE or 'not' (c2 . c4) = FALSE ) by MARGREL1:39;
(c2 'imp' ('not' c3)) . c4 = TRUE by E1, BVFUNC_1:def 14;
then E4: ('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 E2, E3, E4, 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 E5: ( 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 E5, MARGREL1:43;
end;
end;
end;
hence ('not' c2) . c4 = TRUE ;
end;
hence 'not' c2 = I_el c1 by BVFUNC_1:def 14;
end;

theorem :: 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 ;
E1: 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;
E2: '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)) by MARGREL1:40
.= 'not' (c2 . c3) by BINARITH:21 ;
E3: ((('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 E2, BVFUNC_1:def 11 ;
E4: (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 E3, E4, BINARITH:19;
end;
case c2 . c3 = FALSE ;
then ((('not' c2) 'imp' c2) 'imp' c2) . c3 = TRUE 'or' FALSE by E3, 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
E2: ( (('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
E3: ( 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 E1, E2, E3;
hence (('not' c2) 'imp' c2) 'imp' c2 = I_el c1 by E2, E3, FUNCT_1:9;
end;

theorem :: 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 ;
E1: 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;
E2: ((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 ;
E3: 'not' (('not' (c3 '&' c4)) . c5) = 'not' ('not' ((c3 '&' c4) . c5)) by VALUAT_1:def 5
.= (c3 '&' c4) . c5 by MARGREL1:40
.= (c3 . c5) '&' (c4 . c5) by VALUAT_1:def 6 ;
E4: ('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 ;
E5: '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)) by MARGREL1:40 ;
E6: ('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 E3, E4, 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 E7: ('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 E5, E6, 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' (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 ;
E8: now
per cases ( c2 . c5 = TRUE or c2 . c5 = FALSE ) by MARGREL1:39;
case c2 . c5 = TRUE ;
hence ('not' (c2 . c5)) 'or' (c2 . c5) = TRUE by BINARITH:19;
end;
case c2 . c5 = FALSE ;
then ('not' (c2 . c5)) 'or' (c2 . c5) = TRUE 'or' FALSE by MARGREL1:41
.= TRUE by BINARITH:19 ;
hence ('not' (c2 . c5)) 'or' (c2 . c5) = TRUE ;
end;
end;
end;
now
per cases ( c3 . c5 = TRUE or c3 . c5 = FALSE ) by MARGREL1:39;
case c3 . c5 = TRUE ;
hence ('not' (c3 . c5)) 'or' (c3 . c5) = TRUE by BINARITH:19;
end;
case c3 . c5 = FALSE ;
then ('not' (c3 . c5)) 'or' (c3 . c5) = TRUE 'or' FALSE by MARGREL1:41
.= TRUE by BINARITH:19 ;
hence ('not' (c3 . c5)) 'or' (c3 . c5) = TRUE ;
end;
end;
end;
then ('not' ((c2 'imp' c3) . c5)) 'or' (('not' (('not' (c3 '&' c4)) . c5)) 'or' (('not' (c2 '&' c4)) . c5)) = (TRUE 'or' (c3 . c5)) '&' ((('not' (c2 . c5)) 'or' ('not' (c4 . c5))) 'or' TRUE ) by E7, E8, BINARITH:19
.= TRUE '&' ((('not' (c2 . c5)) 'or' ('not' (c4 . c5))) 'or' TRUE ) by BINARITH:19
.= TRUE '&' TRUE by BINARITH:19
.= TRUE by MARGREL1:45 ;
hence ((c2 'imp' c3) 'imp' (('not' (c3 '&' c4)) 'imp' ('not' (c2 '&' c4)))) . c5 = (I_el c1) . c5 by E2, BVFUNC_1:def 14;
end;
consider c5 being Function such that
E2: ( (c2 'imp' c3) 'imp' (('not' (c3 '&' c4)) 'imp' ('not' (c2 '&' c4))) = c5 & dom c5 = c1 & rng c5 c=