:: 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 Pj (c2 'imp' (c3 'imp' (c2 '&' c3))),b1 = TRUE
proof
let c4 be Element of c1;
Pj (c2 'imp' (c3 'imp' (c2 '&' c3))),c4 = ('not' (Pj c2,c4)) 'or' (Pj (c3 'imp' (c2 '&' c3)),c4) by BVFUNC_1:def 11
.= ('not' (Pj c2,c4)) 'or' (('not' (Pj c3,c4)) 'or' (Pj (c2 '&' c3),c4)) by BVFUNC_1:def 11
.= ('not' (Pj c2,c4)) 'or' (('not' (Pj c3,c4)) 'or' ((Pj c2,c4) '&' (Pj c3,c4))) by VALUAT_1:def 6
.= ('not' (Pj c2,c4)) 'or' ((('not' (Pj c3,c4)) 'or' (Pj c2,c4)) '&' (('not' (Pj c3,c4)) 'or' (Pj c3,c4))) by BINARITH:23
.= ('not' (Pj c2,c4)) 'or' (TRUE '&' (('not' (Pj c3,c4)) 'or' (Pj c2,c4))) by BINARITH:18
.= ('not' (Pj c2,c4)) 'or' ((Pj c2,c4) 'or' ('not' (Pj c3,c4))) by MARGREL1:50
.= (('not' (Pj c2,c4)) 'or' (Pj c2,c4)) 'or' ('not' (Pj c3,c4)) by BINARITH:20
.= TRUE 'or' ('not' (Pj c3,c4)) by BINARITH:18
.= TRUE by BINARITH:19 ;
hence Pj (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 Pj ((c2 'imp' c3) 'imp' ((c3 'imp' c2) 'imp' (c2 'eqv' c3))),b1 = TRUE
proof
let c4 be Element of c1;
Pj ((c2 'imp' c3) 'imp' ((c3 'imp' c2) 'imp' (c2 'eqv' c3))),c4 = ('not' (Pj (c2 'imp' c3),c4)) 'or' (Pj ((c3 'imp' c2) 'imp' (c2 'eqv' c3)),c4) by BVFUNC_1:def 11
.= ('not' (('not' (Pj c2,c4)) 'or' (Pj c3,c4))) 'or' (Pj ((c3 'imp' c2) 'imp' (c2 'eqv' c3)),c4) by BVFUNC_1:def 11
.= ('not' (('not' (Pj c2,c4)) 'or' (Pj c3,c4))) 'or' (('not' (Pj (c3 'imp' c2),c4)) 'or' (Pj (c2 'eqv' c3),c4)) by BVFUNC_1:def 11
.= ('not' (('not' (Pj c2,c4)) 'or' (Pj c3,c4))) 'or' (('not' (('not' (Pj c3,c4)) 'or' (Pj c2,c4))) 'or' (Pj (c2 'eqv' c3),c4)) by BVFUNC_1:def 11
.= (('not' ('not' (Pj c2,c4))) '&' ('not' (Pj c3,c4))) 'or' (('not' (('not' (Pj c3,c4)) 'or' (Pj c2,c4))) 'or' (Pj (c2 'eqv' c3),c4)) by BINARITH:10
.= (('not' ('not' (Pj c2,c4))) '&' ('not' (Pj c3,c4))) 'or' ((('not' ('not' (Pj c3,c4))) '&' ('not' (Pj c2,c4))) 'or' (Pj (c2 'eqv' c3),c4)) by BINARITH:10
.= ((Pj c2,c4) '&' ('not' (Pj c3,c4))) 'or' ((('not' ('not' (Pj c3,c4))) '&' ('not' (Pj c2,c4))) 'or' (Pj (c2 'eqv' c3),c4)) by MARGREL1:40
.= ((Pj c2,c4) '&' ('not' (Pj c3,c4))) 'or' (((Pj c3,c4) '&' ('not' (Pj c2,c4))) 'or' (Pj (c2 'eqv' c3),c4)) by MARGREL1:40
.= ((Pj c2,c4) '&' ('not' (Pj c3,c4))) 'or' (((Pj c3,c4) '&' ('not' (Pj c2,c4))) 'or' ('not' ((Pj c2,c4) 'xor' (Pj c3,c4)))) by BVFUNC_1:def 12
.= ((Pj c2,c4) '&' ('not' (Pj c3,c4))) 'or' (((Pj c3,c4) '&' ('not' (Pj c2,c4))) 'or' ('not' ((('not' (Pj c2,c4)) '&' (Pj c3,c4)) 'or' ((Pj c2,c4) '&' ('not' (Pj c3,c4)))))) by BINARITH:def 2
.= ((Pj c2,c4) '&' ('not' (Pj c3,c4))) 'or' ((('not' (Pj c2,c4)) '&' (Pj c3,c4)) 'or' (('not' (('not' (Pj c2,c4)) '&' (Pj c3,c4))) '&' ('not' ((Pj c2,c4) '&' ('not' (Pj c3,c4)))))) by BINARITH:10
.= ((Pj c2,c4) '&' ('not' (Pj c3,c4))) 'or' (((('not' (Pj c2,c4)) '&' (Pj c3,c4)) 'or' ('not' (('not' (Pj c2,c4)) '&' (Pj c3,c4)))) '&' ((('not' (Pj c2,c4)) '&' (Pj c3,c4)) 'or' ('not' ((Pj c2,c4) '&' ('not' (Pj c3,c4)))))) by BINARITH:23
.= ((Pj c2,c4) '&' ('not' (Pj c3,c4))) 'or' (TRUE '&' ((('not' (Pj c2,c4)) '&' (Pj c3,c4)) 'or' ('not' ((Pj c2,c4) '&' ('not' (Pj c3,c4)))))) by BINARITH:18
.= ((Pj c2,c4) '&' ('not' (Pj c3,c4))) 'or' (('not' ((Pj c2,c4) '&' ('not' (Pj c3,c4)))) 'or' (('not' (Pj c2,c4)) '&' (Pj c3,c4))) by MARGREL1:50
.= (((Pj c2,c4) '&' ('not' (Pj c3,c4))) 'or' ('not' ((Pj c2,c4) '&' ('not' (Pj c3,c4))))) 'or' (('not' (Pj c2,c4)) '&' (Pj c3,c4)) by BINARITH:20
.= TRUE 'or' (('not' (Pj c2,c4)) '&' (Pj c3,c4)) by BINARITH:18
.= TRUE by BINARITH:19 ;
hence Pj ((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 Pj ((c2 'or' c3) 'eqv' (c3 'or' c2)),b1 = TRUE
proof
let c4 be Element of c1;
Pj ((c2 'or' c3) 'eqv' (c3 'or' c2)),c4 = 'not' ((Pj (c2 'or' c3),c4) 'xor' (Pj (c3 'or' c2),c4)) by BVFUNC_1:def 12
.= 'not' ((('not' (Pj (c2 'or' c3),c4)) '&' (Pj (c3 'or' c2),c4)) 'or' ((Pj (c2 'or' c3),c4) '&' ('not' (Pj (c3 'or' c2),c4)))) by BINARITH:def 2
.= ('not' (('not' (Pj (c2 'or' c3),c4)) '&' (Pj (c3 'or' c2),c4))) '&' ('not' ((Pj (c2 'or' c3),c4) '&' ('not' (Pj (c3 'or' c2),c4)))) by BINARITH:10
.= (('not' ('not' (Pj (c2 'or' c3),c4))) 'or' ('not' (Pj (c3 'or' c2),c4))) '&' ('not' ((Pj (c2 'or' c3),c4) '&' ('not' (Pj (c3 'or' c2),c4)))) by BINARITH:9
.= (('not' ('not' (Pj (c2 'or' c3),c4))) 'or' ('not' (Pj (c3 'or' c2),c4))) '&' (('not' (Pj (c2 'or' c3),c4)) 'or' ('not' ('not' (Pj (c3 'or' c2),c4)))) by BINARITH:9
.= ((Pj (c2 'or' c3),c4) 'or' ('not' (Pj (c3 'or' c2),c4))) '&' (('not' (Pj (c2 'or' c3),c4)) 'or' ('not' ('not' (Pj (c3 'or' c2),c4)))) by MARGREL1:40
.= TRUE '&' (('not' (Pj (c2 'or' c3),c4)) 'or' (Pj (c2 'or' c3),c4)) by BINARITH:18
.= TRUE '&' TRUE by BINARITH:18
.= TRUE by MARGREL1:45 ;
hence Pj ((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 Pj (((c2 '&' c3) 'imp' c4) 'imp' (c2 'imp' (c3 'imp' c4))),b1 = TRUE
proof
let c5 be Element of c1;
Pj (((c2 '&' c3) 'imp' c4) 'imp' (c2 'imp' (c3 'imp' c4))),c5 = ('not' (Pj ((c2 '&' c3) 'imp' c4),c5)) 'or' (Pj (c2 'imp' (c3 'imp' c4)),c5) by BVFUNC_1:def 11
.= ('not' (('not' (Pj (c2 '&' c3),c5)) 'or' (Pj c4,c5))) 'or' (Pj (c2 'imp' (c3 'imp' c4)),c5) by BVFUNC_1:def 11
.= ('not' (('not' ((Pj c2,c5) '&' (Pj c3,c5))) 'or' (Pj c4,c5))) 'or' (Pj (c2 'imp' (c3 'imp' c4)),c5) by VALUAT_1:def 6
.= ('not' (('not' ((Pj c2,c5) '&' (Pj c3,c5))) 'or' (Pj c4,c5))) 'or' (('not' (Pj c2,c5)) 'or' (Pj (c3 'imp' c4),c5)) by BVFUNC_1:def 11
.= ('not' (('not' ((Pj c2,c5) '&' (Pj c3,c5))) 'or' (Pj c4,c5))) 'or' (('not' (Pj c2,c5)) 'or' (('not' (Pj c3,c5)) 'or' (Pj c4,c5))) by BVFUNC_1:def 11
.= ('not' ((('not' (Pj c2,c5)) 'or' ('not' (Pj c3,c5))) 'or' (Pj c4,c5))) 'or' (('not' (Pj c2,c5)) 'or' (('not' (Pj c3,c5)) 'or' (Pj c4,c5))) by BINARITH:9
.= ('not' ((('not' (Pj c2,c5)) 'or' ('not' (Pj c3,c5))) 'or' (Pj c4,c5))) 'or' ((('not' (Pj c2,c5)) 'or' ('not' (Pj c3,c5))) 'or' (Pj c4,c5)) by BINARITH:20
.= TRUE by BINARITH:18 ;
hence Pj (((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 Pj ((c2 'imp' (c3 'imp' c4)) 'imp' ((c2 '&' c3) 'imp' c4)),b1 = TRUE
proof
let c5 be Element of c1;
Pj ((c2 'imp' (c3 'imp' c4)) 'imp' ((c2 '&' c3) 'imp' c4)),c5 = ('not' (Pj (c2 'imp' (c3 'imp' c4)),c5)) 'or' (Pj ((c2 '&' c3) 'imp' c4),c5) by BVFUNC_1:def 11
.= ('not' (('not' (Pj c2,c5)) 'or' (Pj (c3 'imp' c4),c5))) 'or' (Pj ((c2 '&' c3) 'imp' c4),c5) by BVFUNC_1:def 11
.= ('not' (('not' (Pj c2,c5)) 'or' (('not' (Pj c3,c5)) 'or' (Pj c4,c5)))) 'or' (Pj ((c2 '&' c3) 'imp' c4),c5) by BVFUNC_1:def 11
.= ('not' (('not' (Pj c2,c5)) 'or' (('not' (Pj c3,c5)) 'or' (Pj c4,c5)))) 'or' (('not' (Pj (c2 '&' c3),c5)) 'or' (Pj c4,c5)) by BVFUNC_1:def 11
.= ('not' (('not' (Pj c2,c5)) 'or' (('not' (Pj c3,c5)) 'or' (Pj c4,c5)))) 'or' (('not' ((Pj c2,c5) '&' (Pj c3,c5))) 'or' (Pj c4,c5)) by VALUAT_1:def 6
.= ('not' (('not' (Pj c2,c5)) 'or' (('not' (Pj c3,c5)) 'or' (Pj c4,c5)))) 'or' ((('not' (Pj c2,c5)) 'or' ('not' (Pj c3,c5))) 'or' (Pj c4,c5)) by BINARITH:9
.= ('not' ((('not' (Pj c2,c5)) 'or' ('not' (Pj c3,c5))) 'or' (Pj c4,c5))) 'or' ((('not' (Pj c2,c5)) 'or' ('not' (Pj c3,c5))) 'or' (Pj c4,c5)) by BINARITH:20
.= TRUE by BINARITH:18 ;
hence Pj ((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 Pj ((c4 'imp' c2) 'imp' ((c4 'imp' c3) 'imp' (c4 'imp' (c2 '&' c3)))),b1 = TRUE
proof
let c5 be Element of c1;
Pj ((c4 'imp' c2) 'imp' ((c4 'imp' c3) 'imp' (c4 'imp' (c2 '&' c3)))),c5 = ('not' (Pj (c4 'imp' c2),c5)) 'or' (Pj ((c4 'imp' c3) 'imp' (c4 'imp' (c2 '&' c3))),c5) by BVFUNC_1:def 11
.= ('not' (('not' (Pj c4,c5)) 'or' (Pj c2,c5))) 'or' (Pj ((c4 'imp' c3) 'imp' (c4 'imp' (c2 '&' c3))),c5) by BVFUNC_1:def 11
.= ('not' (('not' (Pj c4,c5)) 'or' (Pj c2,c5))) 'or' (('not' (Pj (c4 'imp' c3),c5)) 'or' (Pj (c4 'imp' (c2 '&' c3)),c5)) by BVFUNC_1:def 11
.= ('not' (('not' (Pj c4,c5)) 'or' (Pj c2,c5))) 'or' (('not' (('not' (Pj c4,c5)) 'or' (Pj c3,c5))) 'or' (Pj (c4 'imp' (c2 '&' c3)),c5)) by BVFUNC_1:def 11
.= ('not' (('not' (Pj c4,c5)) 'or' (Pj c2,c5))) 'or' (('not' (('not' (Pj c4,c5)) 'or' (Pj c3,c5))) 'or' (('not' (Pj c4,c5)) 'or' (Pj (c2 '&' c3),c5))) by BVFUNC_1:def 11
.= ('not' (('not' (Pj c4,c5)) 'or' (Pj c2,c5))) 'or' (('not' (('not' (Pj c4,c5)) 'or' (Pj c3,c5))) 'or' (('not' (Pj c4,c5)) 'or' ((Pj c2,c5) '&' (Pj c3,c5)))) by VALUAT_1:def 6
.= (('not' ('not' (Pj c4,c5))) '&' ('not' (Pj c2,c5))) 'or' (('not' (('not' (Pj c4,c5)) 'or' (Pj c3,c5))) 'or' (('not' (Pj c4,c5)) 'or' ((Pj c2,c5) '&' (Pj c3,c5)))) by BINARITH:10
.= (('not' ('not' (Pj c4,c5))) '&' ('not' (Pj c2,c5))) 'or' ((('not' ('not' (Pj c4,c5))) '&' ('not' (Pj c3,c5))) 'or' (('not' (Pj c4,c5)) 'or' ((Pj c2,c5) '&' (Pj c3,c5)))) by BINARITH:10
.= ((Pj c4,c5) '&' ('not' (Pj c2,c5))) 'or' ((('not' ('not' (Pj c4,c5))) '&' ('not' (Pj c3,c5))) 'or' (('not' (Pj c4,c5)) 'or' ((Pj c2,c5) '&' (Pj c3,c5)))) by MARGREL1:40
.= ((Pj c4,c5) '&' ('not' (Pj c2,c5))) 'or' (((Pj c4,c5) '&' ('not' (Pj c3,c5))) 'or' (('not' (Pj c4,c5)) 'or' ((Pj c2,c5) '&' (Pj c3,c5)))) by MARGREL1:40
.= ((Pj c4,c5) '&' ('not' (Pj c2,c5))) 'or' (((Pj c4,c5) '&' ('not' (Pj c3,c5))) 'or' ((('not' (Pj c4,c5)) 'or' (Pj c2,c5)) '&' (('not' (Pj c4,c5)) 'or' (Pj c3,c5)))) by BINARITH:23
.= ((Pj c4,c5) '&' ('not' (Pj c2,c5))) 'or' ((((Pj c4,c5) '&' ('not' (Pj c3,c5))) 'or' (('not' (Pj c4,c5)) 'or' (Pj c2,c5))) '&' (((Pj c4,c5) '&' ('not' (Pj c3,c5))) 'or' (('not' (Pj c4,c5)) 'or' (Pj c3,c5)))) by BINARITH:23
.= ((Pj c4,c5) '&' ('not' (Pj c2,c5))) 'or' ((((Pj c4,c5) '&' ('not' (Pj c3,c5))) 'or' (('not' (Pj c4,c5)) 'or' (Pj c2,c5))) '&' (((Pj c4,c5) '&' ('not' (Pj c3,c5))) 'or' (('not' (Pj c4,c5)) 'or' ('not' ('not' (Pj c3,c5)))))) by MARGREL1:40
.= ((Pj c4,c5) '&' ('not' (Pj c2,c5))) 'or' ((((Pj c4,c5) '&' ('not' (Pj c3,c5))) 'or' (('not' (Pj c4,c5)) 'or' (Pj c2,c5))) '&' (((Pj c4,c5) '&' ('not' (Pj c3,c5))) 'or' ('not' ((Pj c4,c5) '&' ('not' (Pj c3,c5)))))) by BINARITH:9
.= ((Pj c4,c5) '&' ('not' (Pj c2,c5))) 'or' (TRUE '&' (((Pj c4,c5) '&' ('not' (Pj c3,c5))) 'or' (('not' (Pj c4,c5)) 'or' (Pj c2,c5)))) by BINARITH:18
.= ((Pj c4,c5) '&' ('not' (Pj c2,c5))) 'or' ((('not' (Pj c4,c5)) 'or' (Pj c2,c5)) 'or' ((Pj c4,c5) '&' ('not' (Pj c3,c5)))) by MARGREL1:50
.= (((Pj c4,c5) '&' ('not' (Pj c2,c5))) 'or' (('not' (Pj c4,c5)) 'or' (Pj c2,c5))) 'or' ((Pj c4,c5) '&' ('not' (Pj c3,c5))) by BINARITH:20
.= (((Pj c4,c5) '&' ('not' (Pj c2,c5))) 'or' (('not' (Pj c4,c5)) 'or' ('not' ('not' (Pj c2,c5))))) 'or' ((Pj c4,c5) '&' ('not' (Pj c3,c5))) by MARGREL1:40
.= (((Pj c4,c5) '&' ('not' (Pj c2,c5))) 'or' ('not' ((Pj c4,c5) '&' ('not' (Pj c2,c5))))) 'or' ((Pj c4,c5) '&' ('not' (Pj c3,c5))) by BINARITH:9
.= TRUE 'or' ((Pj c4,c5) '&' ('not' (Pj c3,c5))) by BINARITH:18
.= TRUE by BINARITH:19 ;
hence Pj ((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 Pj (((c2 'or' c3) 'imp' c4) 'imp' ((c2 'imp' c4) 'or' (c3 'imp' c4))),b1 = TRUE
proof
let c5 be Element of c1;
Pj (((c2 'or' c3) 'imp' c4) 'imp' ((c2 'imp' c4) 'or' (c3 'imp' c4))),c5 = ('not' (Pj ((c2 'or' c3) 'imp' c4),c5)) 'or' (Pj ((c2 'imp' c4) 'or' (c3 'imp' c4)),c5) by BVFUNC_1:def 11
.= ('not' (('not' (Pj (c2 'or' c3),c5)) 'or' (Pj c4,c5))) 'or' (Pj ((c2 'imp' c4) 'or' (c3 'imp' c4)),c5) by BVFUNC_1:def 11
.= ('not' (('not' ((Pj c2,c5) 'or' (Pj c3,c5))) 'or' (Pj c4,c5))) 'or' (Pj ((c2 'imp' c4) 'or' (c3 'imp' c4)),c5) by BVFUNC_1:def 7
.= ('not' (('not' ((Pj c2,c5) 'or' (Pj c3,c5))) 'or' (Pj c4,c5))) 'or' ((Pj (c2 'imp' c4),c5) 'or' (Pj (c3 'imp' c4),c5)) by BVFUNC_1:def 7
.= ('not' (('not' ((Pj c2,c5) 'or' (Pj c3,c5))) 'or' (Pj c4,c5))) 'or' ((('not' (Pj c2,c5)) 'or' (Pj c4,c5)) 'or' (Pj (c3 'imp' c4),c5)) by BVFUNC_1:def 11
.= ('not' (('not' ((Pj c2,c5) 'or' (Pj c3,c5))) 'or' (Pj c4,c5))) 'or' ((('not' (Pj c2,c5)) 'or' (Pj c4,c5))