:: BVFUNC10 semantic presentation

theorem Th1: :: BVFUNC10:1
for b1 being non empty set
for b2, b3, b4 being Element of Funcs b1,BOOLEAN holds ((b2 '&' b3) 'or' (b3 '&' b4)) 'or' (b4 '&' b2) = ((b2 'or' b3) '&' (b3 'or' b4)) '&' (b4 'or' b2)
proof
let c1 be non empty set ;
let c2, c3, c4 be Element of Funcs c1,BOOLEAN ;
for b1 being Element of c1 holds
( (((c2 '&' c3) 'or' (c3 '&' c4)) 'or' (c4 '&' c2)) . b1 = TRUE implies (((c2 'or' c3) '&' (c3 'or' c4)) '&' (c4 'or' c2)) . b1 = TRUE )
proof
let c5 be Element of c1;
assume E1: (((c2 '&' c3) 'or' (c3 '&' c4)) 'or' (c4 '&' c2)) . c5 = TRUE ;
E2: (((c2 '&' c3) 'or' (c3 '&' c4)) 'or' (c4 '&' c2)) . c5 = (((c2 '&' c3) 'or' (c3 '&' c4)) . c5) 'or' ((c4 '&' c2) . c5) by BVFUNC_1:def 7
.= (((c2 '&' c3) . c5) 'or' ((c3 '&' c4) . c5)) 'or' ((c4 '&' c2) . c5) by BVFUNC_1:def 7
.= (((c2 . c5) '&' (c3 . c5)) 'or' ((c3 '&' c4) . c5)) 'or' ((c4 '&' c2) . c5) by VALUAT_1:def 6
.= (((c2 . c5) '&' (c3 . c5)) 'or' ((c3 . c5) '&' (c4 . c5))) 'or' ((c4 '&' c2) . c5) by VALUAT_1:def 6
.= (((c2 . c5) '&' (c3 . c5)) 'or' ((c3 . c5) '&' (c4 . c5))) 'or' ((c4 . c5) '&' (c2 . c5)) by VALUAT_1:def 6 ;
now
assume E3: (((c2 'or' c3) '&' (c3 'or' c4)) '&' (c4 'or' c2)) . c5 <> TRUE ;
(((c2 'or' c3) '&' (c3 'or' c4)) '&' (c4 'or' c2)) . c5 = (((c2 'or' c3) '&' (c3 'or' c4)) . c5) '&' ((c4 'or' c2) . c5) by VALUAT_1:def 6
.= (((c2 'or' c3) . c5) '&' ((c3 'or' c4) . c5)) '&' ((c4 'or' c2) . c5) by VALUAT_1:def 6
.= (((c2 . c5) 'or' (c3 . c5)) '&' ((c3 'or' c4) . c5)) '&' ((c4 'or' c2) . c5) by BVFUNC_1:def 7
.= (((c2 . c5) 'or' (c3 . c5)) '&' ((c3 . c5) 'or' (c4 . c5))) '&' ((c4 'or' c2) . c5) by BVFUNC_1:def 7
.= (((c2 . c5) 'or' (c3 . c5)) '&' ((c3 . c5) 'or' (c4 . c5))) '&' ((c4 . c5) 'or' (c2 . c5)) by BVFUNC_1:def 7 ;
then E4: (((c2 . c5) 'or' (c3 . c5)) '&' ((c3 . c5) 'or' (c4 . c5))) '&' ((c4 . c5) 'or' (c2 . c5)) = FALSE by E3, MARGREL1:43;
now
per cases ( ((c2 . c5) 'or' (c3 . c5)) '&' ((c3 . c5) 'or' (c4 . c5)) = FALSE or (c4 . c5) 'or' (c2 . c5) = FALSE ) by E4, MARGREL1:45;
case E5: ((c2 . c5) 'or' (c3 . c5)) '&' ((c3 . c5) 'or' (c4 . c5)) = FALSE ;
now
per cases ( (c2 . c5) 'or' (c3 . c5) = FALSE or (c3 . c5) 'or' (c4 . c5) = FALSE ) by E5, MARGREL1:45;
case E6: (c2 . c5) 'or' (c3 . c5) = FALSE ;
E7: ( c2 . c5 = TRUE or c2 . c5 = FALSE ) by MARGREL1:39;
( c3 . c5 = TRUE or c3 . c5 = FALSE ) by MARGREL1:39;
then ( c2 . c5 = FALSE & c3 . c5 = FALSE ) by E6, E7, BINARITH:19;
then (((c2 . c5) '&' (c3 . c5)) 'or' ((c3 . c5) '&' (c4 . c5))) 'or' ((c4 . c5) '&' (c2 . c5)) = (FALSE 'or' (FALSE '&' (c4 . c5))) 'or' ((c4 . c5) '&' FALSE ) by MARGREL1:49
.= (FALSE 'or' FALSE ) 'or' (FALSE '&' (c4 . c5)) by MARGREL1:49
.= FALSE 'or' (FALSE '&' (c4 . c5)) by BINARITH:7
.= FALSE '&' (c4 . c5) by BINARITH:7
.= FALSE by MARGREL1:49 ;
hence (((c2 'or' c3) '&' (c3 'or' c4)) '&' (c4 'or' c2)) . c5 = TRUE by E1, E2, MARGREL1:43;
end;
case E6: (c3 . c5) 'or' (c4 . c5) = FALSE ;
E7: ( c3 . c5 = TRUE or c3 . c5 = FALSE ) by MARGREL1:39;
( c4 . c5 = TRUE or c4 . c5 = FALSE ) by MARGREL1:39;
then ( c3 . c5 = FALSE & c4 . c5 = FALSE ) by E6, E7, BINARITH:19;
then (((c2 . c5) '&' (c3 . c5)) 'or' ((c3 . c5) '&' (c4 . c5))) 'or' ((c4 . c5) '&' (c2 . c5)) = (FALSE 'or' (FALSE '&' FALSE )) 'or' (FALSE '&' (c2 . c5)) by MARGREL1:49
.= (FALSE 'or' FALSE ) 'or' (FALSE '&' (c2 . c5)) by MARGREL1:49
.= (FALSE 'or' FALSE ) 'or' FALSE by MARGREL1:49
.= FALSE 'or' FALSE by BINARITH:7
.= FALSE by BINARITH:7 ;
hence (((c2 'or' c3) '&' (c3 'or' c4)) '&' (c4 'or' c2)) . c5 = TRUE by E1, E2, MARGREL1:43;
end;
end;
end;
hence (((c2 'or' c3) '&' (c3 'or' c4)) '&' (c4 'or' c2)) . c5 = TRUE ;
end;
case E5: (c4 . c5) 'or' (c2 . c5) = FALSE ;
E6: ( c4 . c5 = TRUE or c4 . c5 = FALSE ) by MARGREL1:39;
( c2 . c5 = TRUE or c2 . c5 = FALSE ) by MARGREL1:39;
then ( c4 . c5 = FALSE & c2 . c5 = FALSE ) by E5, E6, BINARITH:19;
then (((c2 . c5) '&' (c3 . c5)) 'or' ((c3 . c5) '&' (c4 . c5))) 'or' ((c4 . c5) '&' (c2 . c5)) = (FALSE 'or' (FALSE '&' (c3 . c5))) '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 (((c2 'or' c3) '&' (c3 'or' c4)) '&' (c4 'or' c2)) . c5 = TRUE by E1, E2, MARGREL1:43;
end;
end;
end;
hence (((c2 'or' c3) '&' (c3 'or' c4)) '&' (c4 'or' c2)) . c5 = TRUE ;
end;
hence (((c2 'or' c3) '&' (c3 'or' c4)) '&' (c4 'or' c2)) . c5 = TRUE ;
end;
then E1: ((c2 '&' c3) 'or' (c3 '&' c4)) 'or' (c4 '&' c2) '<' ((c2 'or' c3) '&' (c3 'or' c4)) '&' (c4 'or' c2) by BVFUNC_1:def 15;
for b1 being Element of c1 holds
( (((c2 'or' c3) '&' (c3 'or' c4)) '&' (c4 'or' c2)) . b1 = TRUE implies (((c2 '&' c3) 'or' (c3 '&' c4)) 'or' (c4 '&' c2)) . b1 = TRUE )
proof
let c5 be Element of c1;
assume E2: (((c2 'or' c3) '&' (c3 'or' c4)) '&' (c4 'or' c2)) . c5 = TRUE ;
E3: (((c2 'or' c3) '&' (c3 'or' c4)) '&' (c4 'or' c2)) . c5 = (((c2 'or' c3) '&' (c3 'or' c4)) . c5) '&' ((c4 'or' c2) . c5) by VALUAT_1:def 6
.= (((c2 'or' c3) . c5) '&' ((c3 'or' c4) . c5)) '&' ((c4 'or' c2) . c5) by VALUAT_1:def 6
.= (((c2 . c5) 'or' (c3 . c5)) '&' ((c3 'or' c4) . c5)) '&' ((c4 'or' c2) . c5) by BVFUNC_1:def 7
.= (((c2 . c5) 'or' (c3 . c5)) '&' ((c3 . c5) 'or' (c4 . c5))) '&' ((c4 'or' c2) . c5) by BVFUNC_1:def 7
.= (((c2 . c5) 'or' (c3 . c5)) '&' ((c3 . c5) 'or' (c4 . c5))) '&' ((c4 . c5) 'or' (c2 . c5)) by BVFUNC_1:def 7 ;
now
assume E4: (((c2 '&' c3) 'or' (c3 '&' c4)) 'or' (c4 '&' c2)) . c5 <> TRUE ;
E5: (((c2 '&' c3) 'or' (c3 '&' c4)) 'or' (c4 '&' c2)) . c5 = (((c2 '&' c3) 'or' (c3 '&' c4)) . c5) 'or' ((c4 '&' c2) . c5) by BVFUNC_1:def 7
.= (((c2 '&' c3) . c5) 'or' ((c3 '&' c4) . c5)) 'or' ((c4 '&' c2) . c5) by BVFUNC_1:def 7
.= (((c2 . c5) '&' (c3 . c5)) 'or' ((c3 '&' c4) . c5)) 'or' ((c4 '&' c2) . c5) by VALUAT_1:def 6
.= (((c2 . c5) '&' (c3 . c5)) 'or' ((c3 . c5) '&' (c4 . c5))) 'or' ((c4 '&' c2) . c5) by VALUAT_1:def 6
.= (((c2 . c5) '&' (c3 . c5)) 'or' ((c3 . c5) '&' (c4 . c5))) 'or' ((c4 . c5) '&' (c2 . c5)) by VALUAT_1:def 6 ;
E6: ( ((c2 . c5) '&' (c3 . c5)) 'or' ((c3 . c5) '&' (c4 . c5)) = TRUE or ((c2 . c5) '&' (c3 . c5)) 'or' ((c3 . c5) '&' (c4 . c5)) = FALSE ) by MARGREL1:39;
E7: ( (c4 . c5) '&' (c2 . c5) = TRUE or (c4 . c5) '&' (c2 . c5) = FALSE ) by MARGREL1:39;
E8: ( (c2 . c5) '&' (c3 . c5) = TRUE or (c2 . c5) '&' (c3 . c5) = FALSE ) by MARGREL1:39;
( (c3 . c5) '&' (c4 . c5) = TRUE or (c3 . c5) '&' (c4 . c5) = FALSE ) by MARGREL1:39;
then E9: ( (c2 . c5) '&' (c3 . c5) = FALSE & (c3 . c5) '&' (c4 . c5) = FALSE ) by E4, E5, E6, E8, BINARITH:19;
now
per cases not ( not ( c2 . c5 = FALSE & c3 . c5 = FALSE ) & not ( c3 . c5 = FALSE & c4 . c5 = FALSE ) & not ( c4 . c5 = FALSE & c2 . c5 = FALSE ) ) by E4, E5, E7, E9, BINARITH:19, MARGREL1:45;
case ( c2 . c5 = FALSE & c3 . c5 = FALSE ) ;
then (((c2 . c5) 'or' (c3 . c5)) '&' ((c3 . c5) 'or' (c4 . c5))) '&' ((c4 . c5) 'or' (c2 . c5)) = (FALSE '&' (FALSE 'or' (c4 . c5))) '&' ((c4 . c5) 'or' FALSE ) by BINARITH:7
.= (FALSE '&' (c4 . c5)) '&' ((c4 . c5) 'or' FALSE ) by BINARITH:7
.= (FALSE '&' (c4 . c5)) '&' (c4 . c5) by BINARITH:7
.= FALSE '&' ((c4 . c5) '&' (c4 . c5)) by MARGREL1:52
.= FALSE by MARGREL1:49 ;
hence (((c2 '&' c3) 'or' (c3 '&' c4)) 'or' (c4 '&' c2)) . c5 = TRUE by E2, E3, MARGREL1:43;
end;
case ( c3 . c5 = FALSE & c4 . c5 = FALSE ) ;
then (((c2 . c5) 'or' (c3 . c5)) '&' ((c3 . c5) 'or' (c4 . c5))) '&' ((c4 . c5) 'or' (c2 . c5)) = ((c2 . c5) '&' (FALSE 'or' FALSE )) '&' (FALSE 'or' (c2 . c5)) by BINARITH:7
.= ((c2 . c5) '&' FALSE ) '&' (FALSE 'or' (c2 . c5)) by BINARITH:7
.= (FALSE '&' (c2 . c5)) '&' (c2 . c5) by BINARITH:7
.= FALSE '&' ((c2 . c5) '&' (c2 . c5)) by MARGREL1:52
.= FALSE by MARGREL1:49 ;
hence (((c2 '&' c3) 'or' (c3 '&' c4)) 'or' (c4 '&' c2)) . c5 = TRUE by E2, E3, MARGREL1:43;
end;
case ( c4 . c5 = FALSE & c2 . c5 = FALSE ) ;
then (((c2 . c5) 'or' (c3 . c5)) '&' ((c3 . c5) 'or' (c4 . c5))) '&' ((c4 . c5) 'or' (c2 . c5)) = ((c3 . c5) '&' ((c3 . c5) 'or' FALSE )) '&' (FALSE 'or' FALSE ) by BINARITH:7
.= ((c3 . c5) '&' (c3 . c5)) '&' (FALSE 'or' FALSE ) by BINARITH:7
.= FALSE '&' ((c3 . c5) '&' (c3 . c5)) by BINARITH:7
.= FALSE by MARGREL1:49 ;
hence (((c2 '&' c3) 'or' (c3 '&' c4)) 'or' (c4 '&' c2)) . c5 = TRUE by E2, E3, MARGREL1:43;
end;
end;
end;
hence (((c2 '&' c3) 'or' (c3 '&' c4)) 'or' (c4 '&' c2)) . c5 = TRUE ;
end;
hence (((c2 '&' c3) 'or' (c3 '&' c4)) 'or' (c4 '&' c2)) . c5 = TRUE ;
end;
then ((c2 'or' c3) '&' (c3 'or' c4)) '&' (c4 'or' c2) '<' ((c2 '&' c3) 'or' (c3 '&' c4)) 'or' (c4 '&' c2) by BVFUNC_1:def 15;
hence ((c2 '&' c3) 'or' (c3 '&' c4)) 'or' (c4 '&' c2) = ((c2 'or' c3) '&' (c3 'or' c4)) '&' (c4 'or' c2) by E1, BVFUNC_1:18;
end;

Lemma1: for b1 being non empty set
for b2, b3, b4 being Element of Funcs b1,BOOLEAN holds ((b2 '&' ('not' b3)) 'or' (b3 '&' ('not' b4))) 'or' (b4 '&' ('not' b2)) '<' ((b3 '&' ('not' b2)) 'or' (b4 '&' ('not' b3))) 'or' (b2 '&' ('not' b4))
proof
let c1 be non empty set ;
let c2, c3, c4 be Element of Funcs c1,BOOLEAN ;
let c5 be Element of c1; :: according to BVFUNC_1:def 15
assume E2: (((c2 '&' ('not' c3)) 'or' (c3 '&' ('not' c4))) 'or' (c4 '&' ('not' c2))) . c5 = TRUE ;
E3: (((c2 '&' ('not' c3)) 'or' (c3 '&' ('not' c4))) 'or' (c4 '&' ('not' c2))) . c5 = (((c2 '&' ('not' c3)) 'or' (c3 '&' ('not' c4))) . c5) 'or' ((c4 '&' ('not' c2)) . c5) by BVFUNC_1:def 7
.= (((c2 '&' ('not' c3)) . c5) 'or' ((c3 '&' ('not' c4)) . c5)) 'or' ((c4 '&' ('not' c2)) . c5) by BVFUNC_1:def 7
.= (((c2 . c5) '&' (('not' c3) . c5)) 'or' ((c3 '&' ('not' c4)) . c5)) 'or' ((c4 '&' ('not' c2)) . c5) by VALUAT_1:def 6
.= (((c2 . c5) '&' (('not' c3) . c5)) 'or' ((c3 . c5) '&' (('not' c4) . c5))) 'or' ((c4 '&' ('not' c2)) . c5) by VALUAT_1:def 6
.= (((c2 . c5) '&' (('not' c3) . c5)) 'or' ((c3 . c5) '&' (('not' c4) . c5))) 'or' ((c4 . c5) '&' (('not' c2) . c5)) by VALUAT_1:def 6
.= (((c2 . c5) '&' ('not' (c3 . c5))) 'or' ((c3 . c5) '&' (('not' c4) . c5))) 'or' ((c4 . c5) '&' (('not' c2) . c5)) by VALUAT_1:def 5
.= (((c2 . c5) '&' ('not' (c3 . c5))) 'or' ((c3 . c5) '&' ('not' (c4 . c5)))) 'or' ((c4 . c5) '&' (('not' c2) . c5)) by VALUAT_1:def 5
.= (((c2 . c5) '&' ('not' (c3 . c5))) 'or' ((c3 . c5) '&' ('not' (c4 . c5)))) 'or' ((c4 . c5) '&' ('not' (c2 . c5))) by VALUAT_1:def 5 ;
now
assume E4: (((c3 '&' ('not' c2)) 'or' (c4 '&' ('not' c3))) 'or' (c2 '&' ('not' c4))) . c5 <> TRUE ;
E5: (((c3 '&' ('not' c2)) 'or' (c4 '&' ('not' c3))) 'or' (c2 '&' ('not' c4))) . c5 = (((c3 '&' ('not' c2)) 'or' (c4 '&' ('not' c3))) . c5) 'or' ((c2 '&' ('not' c4)) . c5) by BVFUNC_1:def 7
.= (((c3 '&' ('not' c2)) . c5) 'or' ((c4 '&' ('not' c3)) . c5)) 'or' ((c2 '&' ('not' c4)) . c5) by BVFUNC_1:def 7
.= (((c3 . c5) '&' (('not' c2) . c5)) 'or' ((c4 '&' ('not' c3)) . c5)) 'or' ((c2 '&' ('not' c4)) . c5) by VALUAT_1:def 6
.= (((c3 . c5) '&' (('not' c2) . c5)) 'or' ((c4 . c5) '&' (('not' c3) . c5))) 'or' ((c2 '&' ('not' c4)) . c5) by VALUAT_1:def 6
.= (((c3 . c5) '&' (('not' c2) . c5)) 'or' ((c4 . c5) '&' (('not' c3) . c5))) 'or' ((c2 . c5) '&' (('not' c4) . c5)) by VALUAT_1:def 6 ;
E6: ( ((c3 . c5) '&' (('not' c2) . c5)) 'or' ((c4 . c5) '&' (('not' c3) . c5)) = TRUE or ((c3 . c5) '&' (('not' c2) . c5)) 'or' ((c4 . c5) '&' (('not' c3) . c5)) = FALSE ) by MARGREL1:39;
E7: ( (c2 . c5) '&' (('not' c4) . c5) = TRUE or (c2 . c5) '&' (('not' c4) . c5) = FALSE ) by MARGREL1:39;
E8: ( (c3 . c5) '&' (('not' c2) . c5) = TRUE or (c3 . c5) '&' (('not' c2) . c5) = FALSE ) by MARGREL1:39;
( (c4 . c5) '&' (('not' c3) . c5) = TRUE or (c4 . c5) '&' (('not' c3) . c5) = FALSE ) by MARGREL1:39;
then E9: ( (c3 . c5) '&' (('not' c2) . c5) = FALSE & (c4 . c5) '&' (('not' c3) . c5) = FALSE ) by E4, E5, E6, E8, BINARITH:19;
then E10: ( c3 . c5 = FALSE or ('not' c2) . c5 = FALSE ) by MARGREL1:45;
E11: ( c4 . c5 = FALSE or ('not' c3) . c5 = FALSE ) by E9, MARGREL1:45;
now
per cases ( c2 . c5 = FALSE or ('not' c4) . c5 = FALSE ) by E4, E5, E7, BINARITH:19, MARGREL1:45;
case E12: c2 . c5 = FALSE ;
then 'not' (c2 . c5) = TRUE by MARGREL1:41;
then E13: 'not' (c2 . c5) <> FALSE by MARGREL1:43;
then 'not' (c3 . c5) = TRUE by E10, MARGREL1:41, VALUAT_1:def 5;
then 'not' (c3 . c5) <> FALSE by MARGREL1:43;
then 'not' (c4 . c5) = TRUE by E11, MARGREL1:41, VALUAT_1:def 5;
then (((c2 . c5) '&' ('not' (c3 . c5))) 'or' ((c3 . c5) '&' ('not' (c4 . c5)))) 'or' ((c4 . c5) '&' ('not' (c2 . c5))) = (FALSE 'or' (FALSE '&' TRUE )) 'or' (FALSE '&' TRUE ) by E10, E11, E12, E13, 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 (((c3 '&' ('not' c2)) 'or' (c4 '&' ('not' c3))) 'or' (c2 '&' ('not' c4))) . c5 = TRUE by E2, E3, MARGREL1:43;
end;
case ('not' c4) . c5 = FALSE ;
then E12: 'not' (c4 . c5) = FALSE by VALUAT_1:def 5;
then E13: c4 . c5 = TRUE by MARGREL1:41;
then 'not' (c3 . c5) = FALSE by E11, MARGREL1:43, VALUAT_1:def 5;
then E14: c3 . c5 = TRUE by MARGREL1:41;
then 'not' (c2 . c5) = FALSE by E10, MARGREL1:43, VALUAT_1:def 5;
then c2 . c5 = TRUE by MARGREL1:41;
then (((c2 . c5) '&' ('not' (c3 . c5))) 'or' ((c3 . c5) '&' ('not' (c4 . c5)))) 'or' ((c4 . c5) '&' ('not' (c2 . c5))) = (FALSE 'or' (TRUE '&' FALSE )) 'or' (TRUE '&' FALSE ) by E12, E13, E14, 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 (((c3 '&' ('not' c2)) 'or' (c4 '&' ('not' c3))) 'or' (c2 '&' ('not' c4))) . c5 = TRUE by E2, E3, MARGREL1:43;
end;
end;
end;
hence (((c3 '&' ('not' c2)) 'or' (c4 '&' ('not' c3))) 'or' (c2 '&' ('not' c4))) . c5 = TRUE ;
end;
hence (((c3 '&' ('not' c2)) 'or' (c4 '&' ('not' c