:: BVFUNC_6 semantic presentation

theorem :: BVFUNC_6:1
for b1 being non empty set
for b2, b3 being Element of Funcs b1,BOOLEAN holds b2 'imp' (b3 'imp' (b2 '&' b3)) = I_el b1
proof
let c1 be non empty set ;
let c2, c3 be Element of Funcs c1,BOOLEAN ;
for b1 being Element of c1 holds (c2 'imp' (c3 'imp' (c2 '&' c3))) . b1 = TRUE
proof
let c4 be Element of c1;
(c2 'imp' (c3 'imp' (c2 '&' c3))) . c4 = ('not' (c2 . c4)) 'or' ((c3 'imp' (c2 '&' c3)) . c4) by BVFUNC_1:def 11
.= ('not' (c2 . c4)) 'or' (('not' (c3 . c4)) 'or' ((c2 '&' c3) . c4)) by BVFUNC_1:def 11
.= ('not' (c2 . c4)) 'or' (('not' (c3 . c4)) 'or' ((c2 . c4) '&' (c3 . c4))) by VALUAT_1:def 6
.= ('not' (c2 . c4)) 'or' ((('not' (c3 . c4)) 'or' (c2 . c4)) '&' (('not' (c3 . c4)) 'or' (c3 . c4))) by BINARITH:23
.= ('not' (c2 . c4)) 'or' (TRUE '&' (('not' (c3 . c4)) 'or' (c2 . c4))) by BINARITH:18
.= ('not' (c2 . c4)) 'or' ((c2 . c4) 'or' ('not' (c3 . c4))) by MARGREL1:50
.= (('not' (c2 . c4)) 'or' (c2 . c4)) 'or' ('not' (c3 . c4)) by BINARITH:20
.= TRUE 'or' ('not' (c3 . c4)) by BINARITH:18
.= TRUE by BINARITH:19 ;
hence (c2 'imp' (c3 'imp' (c2 '&' c3))) . c4 = TRUE ;
end;
hence c2 'imp' (c3 'imp' (c2 '&' c3)) = I_el c1 by BVFUNC_1:def 14;
end;

theorem :: BVFUNC_6:2
for b1 being non empty set
for b2, b3 being Element of Funcs b1,BOOLEAN holds (b2 'imp' b3) 'imp' ((b3 'imp' b2) 'imp' (b2 'eqv' b3)) = I_el b1
proof
let c1 be non empty set ;
let c2, c3 be Element of Funcs c1,BOOLEAN ;
for b1 being Element of c1 holds ((c2 'imp' c3) 'imp' ((c3 'imp' c2) 'imp' (c2 'eqv' c3))) . b1 = TRUE
proof
let c4 be Element of c1;
((c2 'imp' c3) 'imp' ((c3 'imp' c2) 'imp' (c2 'eqv' c3))) . c4 = ('not' ((c2 'imp' c3) . c4)) 'or' (((c3 'imp' c2) 'imp' (c2 'eqv' c3)) . c4) by BVFUNC_1:def 11
.= ('not' (('not' (c2 . c4)) 'or' (c3 . c4))) 'or' (((c3 'imp' c2) 'imp' (c2 'eqv' c3)) . c4) by BVFUNC_1:def 11
.= ('not' (('not' (c2 . c4)) 'or' (c3 . c4))) 'or' (('not' ((c3 'imp' c2) . c4)) 'or' ((c2 'eqv' c3) . c4)) by BVFUNC_1:def 11
.= ('not' (('not' (c2 . c4)) 'or' (c3 . c4))) 'or' (('not' (('not' (c3 . c4)) 'or' (c2 . c4))) 'or' ((c2 'eqv' c3) . c4)) by BVFUNC_1:def 11
.= (('not' ('not' (c2 . c4))) '&' ('not' (c3 . c4))) 'or' (('not' (('not' (c3 . c4)) 'or' (c2 . c4))) 'or' ((c2 'eqv' c3) . c4)) by BINARITH:10
.= (('not' ('not' (c2 . c4))) '&' ('not' (c3 . c4))) 'or' ((('not' ('not' (c3 . c4))) '&' ('not' (c2 . c4))) 'or' ((c2 'eqv' c3) . c4)) by BINARITH:10
.= ((c2 . c4) '&' ('not' (c3 . c4))) 'or' ((('not' ('not' (c3 . c4))) '&' ('not' (c2 . c4))) 'or' ((c2 'eqv' c3) . c4)) by MARGREL1:40
.= ((c2 . c4) '&' ('not' (c3 . c4))) 'or' (((c3 . c4) '&' ('not' (c2 . c4))) 'or' ((c2 'eqv' c3) . c4)) by MARGREL1:40
.= ((c2 . c4) '&' ('not' (c3 . c4))) 'or' (((c3 . c4) '&' ('not' (c2 . c4))) 'or' ('not' ((c2 . c4) 'xor' (c3 . c4)))) by BVFUNC_1:def 12
.= ((c2 . c4) '&' ('not' (c3 . c4))) 'or' (((c3 . c4) '&' ('not' (c2 . c4))) 'or' ('not' ((('not' (c2 . c4)) '&' (c3 . c4)) 'or' ((c2 . c4) '&' ('not' (c3 . c4)))))) by BINARITH:def 2
.= ((c2 . c4) '&' ('not' (c3 . c4))) 'or' ((('not' (c2 . c4)) '&' (c3 . c4)) 'or' (('not' (('not' (c2 . c4)) '&' (c3 . c4))) '&' ('not' ((c2 . c4) '&' ('not' (c3 . c4)))))) by BINARITH:10
.= ((c2 . c4) '&' ('not' (c3 . c4))) 'or' (((('not' (c2 . c4)) '&' (c3 . c4)) 'or' ('not' (('not' (c2 . c4)) '&' (c3 . c4)))) '&' ((('not' (c2 . c4)) '&' (c3 . c4)) 'or' ('not' ((c2 . c4) '&' ('not' (c3 . c4)))))) by BINARITH:23
.= ((c2 . c4) '&' ('not' (c3 . c4))) 'or' (TRUE '&' ((('not' (c2 . c4)) '&' (c3 . c4)) 'or' ('not' ((c2 . c4) '&' ('not' (c3 . c4)))))) by BINARITH:18
.= ((c2 . c4) '&' ('not' (c3 . c4))) 'or' (('not' ((c2 . c4) '&' ('not' (c3 . c4)))) 'or' (('not' (c2 . c4)) '&' (c3 . c4))) by MARGREL1:50
.= (((c2 . c4) '&' ('not' (c3 . c4))) 'or' ('not' ((c2 . c4) '&' ('not' (c3 . c4))))) 'or' (('not' (c2 . c4)) '&' (c3 . c4)) by BINARITH:20
.= TRUE 'or' (('not' (c2 . c4)) '&' (c3 . c4)) by BINARITH:18
.= TRUE by BINARITH:19 ;
hence ((c2 'imp' c3) 'imp' ((c3 'imp' c2) 'imp' (c2 'eqv' c3))) . c4 = TRUE ;
end;
hence (c2 'imp' c3) 'imp' ((c3 'imp' c2) 'imp' (c2 'eqv' c3)) = I_el c1 by BVFUNC_1:def 14;
end;

theorem :: BVFUNC_6:3
for b1 being non empty set
for b2, b3 being Element of Funcs b1,BOOLEAN holds (b2 'or' b3) 'eqv' (b3 'or' b2) = I_el b1
proof
let c1 be non empty set ;
let c2, c3 be Element of Funcs c1,BOOLEAN ;
for b1 being Element of c1 holds ((c2 'or' c3) 'eqv' (c3 'or' c2)) . b1 = TRUE
proof
let c4 be Element of c1;
((c2 'or' c3) 'eqv' (c3 'or' c2)) . c4 = 'not' (((c2 'or' c3) . c4) 'xor' ((c3 'or' c2) . c4)) by BVFUNC_1:def 12
.= 'not' ((('not' ((c2 'or' c3) . c4)) '&' ((c3 'or' c2) . c4)) 'or' (((c2 'or' c3) . c4) '&' ('not' ((c3 'or' c2) . c4)))) by BINARITH:def 2
.= ('not' (('not' ((c2 'or' c3) . c4)) '&' ((c3 'or' c2) . c4))) '&' ('not' (((c2 'or' c3) . c4) '&' ('not' ((c3 'or' c2) . c4)))) by BINARITH:10
.= (('not' ('not' ((c2 'or' c3) . c4))) 'or' ('not' ((c3 'or' c2) . c4))) '&' ('not' (((c2 'or' c3) . c4) '&' ('not' ((c3 'or' c2) . c4)))) by BINARITH:9
.= (('not' ('not' ((c2 'or' c3) . c4))) 'or' ('not' ((c3 'or' c2) . c4))) '&' (('not' ((c2 'or' c3) . c4)) 'or' ('not' ('not' ((c3 'or' c2) . c4)))) by BINARITH:9
.= (((c2 'or' c3) . c4) 'or' ('not' ((c3 'or' c2) . c4))) '&' (('not' ((c2 'or' c3) . c4)) 'or' ('not' ('not' ((c3 'or' c2) . c4)))) by MARGREL1:40
.= TRUE '&' (('not' ((c2 'or' c3) . c4)) 'or' ((c2 'or' c3) . c4)) by BINARITH:18
.= TRUE '&' TRUE by BINARITH:18
.= TRUE by MARGREL1:45 ;
hence ((c2 'or' c3) 'eqv' (c3 'or' c2)) . c4 = TRUE ;
end;
hence (c2 'or' c3) 'eqv' (c3 'or' c2) = I_el c1 by BVFUNC_1:def 14;
end;

theorem :: BVFUNC_6:4
for b1 being non empty set
for b2, b3, b4 being Element of Funcs b1,BOOLEAN holds ((b2 '&' b3) 'imp' b4) 'imp' (b2 'imp' (b3 'imp' b4)) = I_el b1
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) 'imp' c4) 'imp' (c2 'imp' (c3 'imp' c4))) . b1 = TRUE
proof
let c5 be Element of c1;
(((c2 '&' c3) 'imp' c4) 'imp' (c2 'imp' (c3 'imp' c4))) . c5 = ('not' (((c2 '&' c3) 'imp' c4) . c5)) 'or' ((c2 'imp' (c3 'imp' c4)) . c5) by BVFUNC_1:def 11
.= ('not' (('not' ((c2 '&' c3) . c5)) 'or' (c4 . c5))) 'or' ((c2 'imp' (c3 'imp' c4)) . c5) by BVFUNC_1:def 11
.= ('not' (('not' ((c2 . c5) '&' (c3 . c5))) 'or' (c4 . c5))) 'or' ((c2 'imp' (c3 'imp' c4)) . c5) by VALUAT_1:def 6
.= ('not' (('not' ((c2 . c5) '&' (c3 . c5))) 'or' (c4 . c5))) 'or' (('not' (c2 . c5)) 'or' ((c3 'imp' c4) . c5)) by BVFUNC_1:def 11
.= ('not' (('not' ((c2 . c5) '&' (c3 . c5))) 'or' (c4 . c5))) 'or' (('not' (c2 . c5)) 'or' (('not' (c3 . c5)) 'or' (c4 . c5))) by BVFUNC_1:def 11
.= ('not' ((('not' (c2 . c5)) 'or' ('not' (c3 . c5))) 'or' (c4 . c5))) 'or' (('not' (c2 . c5)) 'or' (('not' (c3 . c5)) 'or' (c4 . c5))) by BINARITH:9
.= ('not' ((('not' (c2 . c5)) 'or' ('not' (c3 . c5))) 'or' (c4 . c5))) 'or' ((('not' (c2 . c5)) 'or' ('not' (c3 . c5))) 'or' (c4 . c5)) by BINARITH:20
.= TRUE by BINARITH:18 ;
hence (((c2 '&' c3) 'imp' c4) 'imp' (c2 'imp' (c3 'imp' c4))) . c5 = TRUE ;
end;
hence ((c2 '&' c3) 'imp' c4) 'imp' (c2 'imp' (c3 'imp' c4)) = I_el c1 by BVFUNC_1:def 14;
end;

theorem :: BVFUNC_6:5
for b1 being non empty set
for b2, b3, b4 being Element of Funcs b1,BOOLEAN holds (b2 'imp' (b3 'imp' b4)) 'imp' ((b2 '&' b3) 'imp' b4) = I_el b1
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 'imp' (c3 'imp' c4)) 'imp' ((c2 '&' c3) 'imp' c4)) . b1 = TRUE
proof
let c5 be Element of c1;
((c2 'imp' (c3 'imp' c4)) 'imp' ((c2 '&' c3) 'imp' c4)) . c5 = ('not' ((c2 'imp' (c3 'imp' c4)) . c5)) 'or' (((c2 '&' c3) 'imp' c4) . c5) by BVFUNC_1:def 11
.= ('not' (('not' (c2 . c5)) 'or' ((c3 'imp' c4) . c5))) 'or' (((c2 '&' c3) 'imp' c4) . c5) by BVFUNC_1:def 11
.= ('not' (('not' (c2 . c5)) 'or' (('not' (c3 . c5)) 'or' (c4 . c5)))) 'or' (((c2 '&' c3) 'imp' c4) . c5) by BVFUNC_1:def 11
.= ('not' (('not' (c2 . c5)) 'or' (('not' (c3 . c5)) 'or' (c4 . c5)))) 'or' (('not' ((c2 '&' c3) . c5)) 'or' (c4 . c5)) by BVFUNC_1:def 11
.= ('not' (('not' (c2 . c5)) 'or' (('not' (c3 . c5)) 'or' (c4 . c5)))) 'or' (('not' ((c2 . c5) '&' (c3 . c5))) 'or' (c4 . c5)) by VALUAT_1:def 6
.= ('not' (('not' (c2 . c5)) 'or' (('not' (c3 . c5)) 'or' (c4 . c5)))) 'or' ((('not' (c2 . c5)) 'or' ('not' (c3 . c5))) 'or' (c4 . c5)) by BINARITH:9
.= ('not' ((('not' (c2 . c5)) 'or' ('not' (c3 . c5))) 'or' (c4 . c5))) 'or' ((('not' (c2 . c5)) 'or' ('not' (c3 . c5))) 'or' (c4 . c5)) by BINARITH:20
.= TRUE by BINARITH:18 ;
hence ((c2 'imp' (c3 'imp' c4)) 'imp' ((c2 '&' c3) 'imp' c4)) . c5 = TRUE ;
end;
hence (c2 'imp' (c3 'imp' c4)) 'imp' ((c2 '&' c3) 'imp' c4) = I_el c1 by BVFUNC_1:def 14;
end;

theorem :: BVFUNC_6:6
for b1 being non empty set
for b2, b3, b4 being Element of Funcs b1,BOOLEAN holds (b4 'imp' b2) 'imp' ((b4 'imp' b3) 'imp' (b4 'imp' (b2 '&' b3))) = I_el b1
proof
let c1 be non empty set ;
let c2, c3, c4 be Element of Funcs c1,BOOLEAN ;
for b1 being Element of c1 holds ((c4 'imp' c2) 'imp' ((c4 'imp' c3) 'imp' (c4 'imp' (c2 '&' c3)))) . b1 = TRUE
proof
let c5 be Element of c1;
((c4 'imp' c2) 'imp' ((c4 'imp' c3) 'imp' (c4 'imp' (c2 '&' c3)))) . c5 = ('not' ((c4 'imp' c2) . c5)) 'or' (((c4 'imp' c3) 'imp' (c4 'imp' (c2 '&' c3))) . c5) by BVFUNC_1:def 11
.= ('not' (('not' (c4 . c5)) 'or' (c2 . c5))) 'or' (((c4 'imp' c3) 'imp' (c4 'imp' (c2 '&' c3))) . c5) by BVFUNC_1:def 11
.= ('not' (('not' (c4 . c5)) 'or' (c2 . c5))) 'or' (('not' ((c4 'imp' c3) . c5)) 'or' ((c4 'imp' (c2 '&' c3)) . c5)) by BVFUNC_1:def 11
.= ('not' (('not' (c4 . c5)) 'or' (c2 . c5))) 'or' (('not' (('not' (c4 . c5)) 'or' (c3 . c5))) 'or' ((c4 'imp' (c2 '&' c3)) . c5)) by BVFUNC_1:def 11
.= ('not' (('not' (c4 . c5)) 'or' (c2 . c5))) 'or' (('not' (('not' (c4 . c5)) 'or' (c3 . c5))) 'or' (('not' (c4 . c5)) 'or' ((c2 '&' c3) . c5))) by BVFUNC_1:def 11
.= ('not' (('not' (c4 . c5)) 'or' (c2 . c5))) 'or' (('not' (('not' (c4 . c5)) 'or' (c3 . c5))) 'or' (('not' (c4 . c5)) 'or' ((c2 . c5) '&' (c3 . c5)))) by VALUAT_1:def 6
.= (('not' ('not' (c4 . c5))) '&' ('not' (c2 . c5))) 'or' (('not' (('not' (c4 . c5)) 'or' (c3 . c5))) 'or' (('not' (c4 . c5)) 'or' ((c2 . c5) '&' (c3 . c5)))) by BINARITH:10
.= (('not' ('not' (c4 . c5))) '&' ('not' (c2 . c5))) 'or' ((('not' ('not' (c4 . c5))) '&' ('not' (c3 . c5))) 'or' (('not' (c4 . c5)) 'or' ((c2 . c5) '&' (c3 . c5)))) by BINARITH:10
.= ((c4 . c5) '&' ('not' (c2 . c5))) 'or' ((('not' ('not' (c4 . c5))) '&' ('not' (c3 . c5))) 'or' (('not' (c4 . c5)) 'or' ((c2 . c5) '&' (c3 . c5)))) by MARGREL1:40
.= ((c4 . c5) '&' ('not' (c2 . c5))) 'or' (((c4 . c5) '&' ('not' (c3 . c5))) 'or' (('not' (c4 . c5)) 'or' ((c2 . c5) '&' (c3 . c5)))) by MARGREL1:40
.= ((c4 . c5) '&' ('not' (c2 . c5))) 'or' (((c4 . c5) '&' ('not' (c3 . c5))) 'or' ((('not' (c4 . c5)) 'or' (c2 . c5)) '&' (('not' (c4 . c5)) 'or' (c3 . c5)))) by BINARITH:23
.= ((c4 . c5) '&' ('not' (c2 . c5))) 'or' ((((c4 . c5) '&' ('not' (c3 . c5))) 'or' (('not' (c4 . c5)) 'or' (c2 . c5))) '&' (((c4 . c5) '&' ('not' (c3 . c5))) 'or' (('not' (c4 . c5)) 'or' (c3 . c5)))) by BINARITH:23
.= ((c4 . c5) '&' ('not' (c2 . c5))) 'or' ((((c4 . c5) '&' ('not' (c3 . c5))) 'or' (('not' (c4 . c5)) 'or' (c2 . c5))) '&' (((c4 . c5) '&' ('not' (c3 . c5))) 'or' (('not' (c4 . c5)) 'or' ('not' ('not' (c3 . c5)))))) by MARGREL1:40
.= ((c4 . c5) '&' ('not' (c2 . c5))) 'or' ((((c4 . c5) '&' ('not' (c3 . c5))) 'or' (('not' (c4 . c5)) 'or' (c2 . c5))) '&' (((c4 . c5) '&' ('not' (c3 . c5))) 'or' ('not' ((c4 . c5) '&' ('not' (c3 . c5)))))) by BINARITH:9
.= ((c4 . c5) '&' ('not' (c2 . c5))) 'or' (TRUE '&' (((c4 . c5) '&' ('not' (c3 . c5))) 'or' (('not' (c4 . c5)) 'or' (c2 . c5)))) by BINARITH:18
.= ((c4 . c5) '&' ('not' (c2 . c5))) 'or' ((('not' (c4 . c5)) 'or' (c2 . c5)) 'or' ((c4 . c5) '&' ('not' (c3 . c5)))) by MARGREL1:50
.= (((c4 . c5) '&' ('not' (c2 . c5))) 'or' (('not' (c4 . c5)) 'or' (c2 . c5))) 'or' ((c4 . c5) '&' ('not' (c3 . c5))) by BINARITH:20
.= (((c4 . c5) '&' ('not' (c2 . c5))) 'or' (('not' (c4 . c5)) 'or' ('not' ('not' (c2 . c5))))) 'or' ((c4 . c5) '&' ('not' (c3 . c5))) by MARGREL1:40
.= (((c4 . c5) '&' ('not' (c2 . c5))) 'or' ('not' ((c4 . c5) '&' ('not' (c2 . c5))))) 'or' ((c4 . c5) '&' ('not' (c3 . c5))) by BINARITH:9
.= TRUE 'or' ((c4 . c5) '&' ('not' (c3 . c5))) by BINARITH:18
.= TRUE by BINARITH:19 ;
hence ((c4 'imp' c2) 'imp' ((c4 'imp' c3) 'imp' (c4 'imp' (c2 '&' c3)))) . c5 = TRUE ;
end;
hence (c4 'imp' c2) 'imp' ((c4 'imp' c3) 'imp' (c4 'imp' (c2 '&' c3))) = I_el c1 by BVFUNC_1:def 14;
end;

theorem :: BVFUNC_6:7
for b1 being non empty set
for b2, b3, b4 being Element of Funcs b1,BOOLEAN holds ((b2 'or' b3) 'imp' b4) 'imp' ((b2 'imp' b4) 'or' (b3 'imp' b4)) = I_el b1
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 'or' c3) 'imp' c4) 'imp' ((c2 'imp' c4) 'or' (c3 'imp' c4))) . b1 = TRUE
proof
let c5 be Element of c1;
(((c2 'or' c3) 'imp' c4) 'imp' ((c2 'imp' c4) 'or' (c3 'imp' c4))) . c5 = ('not' (((c2 'or' c3) 'imp' c4) . c5)) 'or' (((c2 'imp' c4) 'or' (c3 'imp' c4)) . c5) by BVFUNC_1:def 11
.= ('not' (('not' ((c2 'or' c3) . c5)) 'or' (c4 . c5))) 'or' (((c2 'imp' c4) 'or' (c3 'imp' c4)) . c5) by BVFUNC_1:def 11
.= ('not' (('not' ((c2 . c5) 'or' (c3 . c5))) 'or' (c4 . c5))) 'or' (((c2 'imp' c4) 'or' (c3 'imp' c4)) . c5) by BVFUNC_1:def 7
.= ('not' (('not' ((c2 . c5) 'or' (c3 . c5))) 'or' (c4 . c5))) 'or' (((c2 'imp' c4) . c5) 'or' ((c3 'imp' c4) . c5)) by BVFUNC_1:def 7
.= ('not' (('not' ((c2 . c5) 'or' (c3 . c5))) 'or' (c4 . c5))) 'or' ((('not' (c2 . c5)) 'or' (c4 . c5)) 'or' ((c3 'imp' c4) . c5)) by BVFUNC_1:def 11
.= ('not' (('not' ((c2 . c5) 'or' (c3 . c5))) 'or' (c4 . c5))) 'or' ((('not' (c2 . c5)) 'or' (c4 . c5)) 'or' (('n