:: BVFUNC25 semantic presentation

theorem :: BVFUNC25:1
for b1 being non empty set
for b2, b3 being Element of Funcs b1,BOOLEAN holds 'not' (b2 'imp' b3) = b2 '&' ('not' b3)
proof
let c1 be non empty set ;
let c2, c3 be Element of Funcs c1,BOOLEAN ;
thus 'not' (c2 'imp' c3) = 'not' (('not' c2) 'or' c3) by BVFUNC_4:8
.= ('not' ('not' c2)) '&' ('not' c3) by BVFUNC_1:16
.= c2 '&' ('not' c3) by BVFUNC_1:4 ;
end;

theorem E1: :: BVFUNC25:2
for b1 being non empty set
for b2, b3 being Element of Funcs b1,BOOLEAN holds (('not' b2) 'imp' ('not' b3)) 'imp' (b3 'imp' b2) = I_el b1
proof
let c1 be non empty set ;
let c2, c3 be Element of Funcs c1,BOOLEAN ;
(('not' c2) 'imp' ('not' c3)) 'imp' (c3 'imp' c2) = ('not' (('not' c2) 'imp' ('not' c3))) 'or' (c3 'imp' c2) by BVFUNC_4:8
.= ('not' (('not' ('not' c2)) 'or' ('not' c3))) 'or' (c3 'imp' c2) by BVFUNC_4:8
.= ('not' (c2 'or' ('not' c3))) 'or' (c3 'imp' c2) by BVFUNC_1:4
.= (('not' c2) '&' ('not' ('not' c3))) 'or' (c3 'imp' c2) by BVFUNC_1:16
.= (('not' c2) '&' c3) 'or' (c3 'imp' c2) by BVFUNC_1:4
.= (('not' c2) '&' c3) 'or' (('not' c3) 'or' c2) by BVFUNC_4:8
.= ((('not' c2) '&' c3) 'or' ('not' c3)) 'or' c2 by BVFUNC_1:11
.= ((('not' c2) 'or' ('not' c3)) '&' (c3 'or' ('not' c3))) 'or' c2 by BVFUNC_1:14
.= ((('not' c2) 'or' ('not' c3)) '&' (I_el c1)) 'or' c2 by BVFUNC_4:6
.= (('not' c2) 'or' ('not' c3)) 'or' c2 by BVFUNC_1:9
.= ('not' c3) 'or' (('not' c2) 'or' c2) by BVFUNC_1:11
.= ('not' c3) 'or' (I_el c1) by BVFUNC_4:6 ;
hence (('not' c2) 'imp' ('not' c3)) 'imp' (c3 'imp' c2) = I_el c1 by BVFUNC_1:13;
end;

theorem E2: :: BVFUNC25:3
for b1 being non empty set
for b2, b3 being Element of Funcs b1,BOOLEAN holds b2 'imp' b3 = ('not' b3) 'imp' ('not' b2)
proof
let c1 be non empty set ;
let c2, c3 be Element of Funcs c1,BOOLEAN ;
(('not' c3) 'imp' ('not' c2)) 'imp' (c2 'imp' c3) = I_el c1 by E1;
then E3: ('not' c3) 'imp' ('not' c2) '<' c2 'imp' c3 by BVFUNC_1:19;
(c2 'imp' c3) 'imp' (('not' c3) 'imp' ('not' c2)) = I_el c1 by BVFUNC_5:33;
then c2 'imp' c3 '<' ('not' c3) 'imp' ('not' c2) by BVFUNC_1:19;
hence c2 'imp' c3 = ('not' c3) 'imp' ('not' c2) by E3, BVFUNC_1:18;
end;

theorem :: BVFUNC25:4
for b1 being non empty set
for b2, b3 being Element of Funcs b1,BOOLEAN holds b2 'eqv' b3 = ('not' b2) 'eqv' ('not' b3)
proof
let c1 be non empty set ;
let c2, c3 be Element of Funcs c1,BOOLEAN ;
thus ('not' c2) 'eqv' ('not' c3) = (('not' c2) 'imp' ('not' c3)) '&' (('not' c3) 'imp' ('not' c2)) by BVFUNC_4:7
.= (c3 'imp' c2) '&' (('not' c3) 'imp' ('not' c2)) by E2
.= (c3 'imp' c2) '&' (c2 'imp' c3) by E2
.= c2 'eqv' c3 by BVFUNC_4:7 ;
end;

theorem E3: :: BVFUNC25:5
for b1 being non empty set
for b2, b3 being Element of Funcs b1,BOOLEAN holds b2 'imp' b3 = b2 'imp' (b2 '&' b3)
proof
let c1 be non empty set ;
let c2, c3 be Element of Funcs c1,BOOLEAN ;
c2 'imp' (c2 '&' c3) = ('not' c2) 'or' (c2 '&' c3) by BVFUNC_4:8
.= (('not' c2) 'or' c2) '&' (('not' c2) 'or' c3) by BVFUNC_1:14
.= (I_el c1) '&' (('not' c2) 'or' c3) by BVFUNC_4:6
.= ('not' c2) 'or' c3 by BVFUNC_1:9 ;
hence c2 'imp' c3 = c2 'imp' (c2 '&' c3) by BVFUNC_4:8;
end;

theorem :: BVFUNC25:6
for b1 being non empty set
for b2, b3 being Element of Funcs b1,BOOLEAN holds b2 'eqv' b3 = (b2 'or' b3) 'imp' (b2 '&' b3)
proof
let c1 be non empty set ;
let c2, c3 be Element of Funcs c1,BOOLEAN ;
thus (c2 'or' c3) 'imp' (c2 '&' c3) = (c2 'imp' (c2 '&' c3)) '&' (c3 'imp' (c2 '&' c3)) by BVFUNC_7:5
.= (c2 'imp' c3) '&' (c3 'imp' (c2 '&' c3)) by E3
.= (c2 'imp' c3) '&' (c3 'imp' c2) by E3
.= c2 'eqv' c3 by BVFUNC_4:7 ;
end;

theorem :: BVFUNC25:7
for b1 being non empty set
for b2 being Element of Funcs b1,BOOLEAN holds b2 'eqv' ('not' b2) = O_el b1
proof
let c1 be non empty set ;
let c2 be Element of Funcs c1,BOOLEAN ;
thus c2 'eqv' ('not' c2) = (c2 'imp' ('not' c2)) '&' (('not' c2) 'imp' c2) by BVFUNC_4:7
.= (('not' c2) 'or' ('not' c2)) '&' (('not' c2) 'imp' c2) by BVFUNC_4:8
.= (('not' c2) 'or' ('not' c2)) '&' (('not' ('not' c2)) 'or' c2) by BVFUNC_4:8
.= ('not' c2) '&' (('not' ('not' c2)) 'or' c2) by BVFUNC_1:10
.= ('not' c2) '&' (c2 'or' c2) by BVFUNC_1:4
.= ('not' c2) '&' c2 by BVFUNC_1:10
.= O_el c1 by BVFUNC_4:5 ;
end;

theorem :: BVFUNC25:8
for b1 being non empty set
for b2, b3, b4 being Element of Funcs b1,BOOLEAN holds b2 'imp' (b3 'imp' b4) = b3 'imp' (b2 'imp' b4)
proof
let c1 be non empty set ;
let c2, c3, c4 be Element of Funcs c1,BOOLEAN ;
thus c2 'imp' (c3 'imp' c4) = ('not' c2) 'or' (c3 'imp' c4) by BVFUNC_4:8
.= ('not' c2) 'or' (('not' c3) 'or' c4) by BVFUNC_4:8
.= ('not' c3) 'or' (('not' c2) 'or' c4) by BVFUNC_1:11
.= ('not' c3) 'or' (c2 'imp' c4) by BVFUNC_4:8
.= c3 'imp' (c2 'imp' c4) by BVFUNC_4:8 ;
end;

theorem :: BVFUNC25:9
for b1 being non empty set
for b2, b3, b4 being Element of Funcs b1,BOOLEAN holds b2 'imp' (b3 'imp' b4) = (b2 'imp' b3) 'imp' (b2 'imp' b4)
proof
let c1 be non empty set ;
let c2, c3, c4 be Element of Funcs c1,BOOLEAN ;
thus (c2 'imp' c3) 'imp' (c2 'imp' c4) = (c2 'imp' c3) 'imp' (('not' c2) 'or' c4) by BVFUNC_4:8
.= ('not' (c2 'imp' c3)) 'or' (('not' c2) 'or' c4) by BVFUNC_4:8
.= ('not' (('not' c2) 'or' c3)) 'or' (('not' c2) 'or' c4) by BVFUNC_4:8
.= (('not' ('not' c2)) '&' ('not' c3)) 'or' (('not' c2) 'or' c4) by BVFUNC_1:16
.= (c2 '&' ('not' c3)) 'or' (('not' c2) 'or' c4) by BVFUNC_1:4
.= ((c2 '&' ('not' c3)) 'or' ('not' c2)) 'or' c4 by BVFUNC_1:11
.= ((c2 'or' ('not' c2)) '&' (('not' c3) 'or' ('not' c2))) 'or' c4 by BVFUNC_1:14
.= ((I_el c1) '&' (('not' c3) 'or' ('not' c2))) 'or' c4 by BVFUNC_4:6
.= (('not' c2) 'or' ('not' c3)) 'or' c4 by BVFUNC_1:9
.= ('not' c2) 'or' (('not' c3) 'or' c4) by BVFUNC_1:11
.= ('not' c2) 'or' (c3 'imp' c4) by BVFUNC_4:8
.= c2 'imp' (c3 'imp' c4) by BVFUNC_4:8 ;
end;

theorem :: BVFUNC25:10
for b1 being non empty set
for b2, b3 being Element of Funcs b1,BOOLEAN holds b2 'eqv' b3 = b2 'xor' ('not' b3)
proof
let c1 be non empty set ;
let c2, c3 be Element of Funcs c1,BOOLEAN ;
'not' (c2 'xor' c3) = 'not' ('not' (c2 'eqv' c3)) by BVFUNC_8:12;
then 'not' (c2 'xor' c3) = c2 'eqv' c3 by BVFUNC_1:4;
hence c2 'eqv' c3 = c2 'xor' ('not' c3) by BVFUNC_8:17;
end;

theorem :: BVFUNC25:11
for b1 being non empty set
for b2, b3, b4 being Element of Funcs b1,BOOLEAN holds b2 '&' (b3 'xor' b4) = (b2 '&' b3) 'xor' (b2 '&' b4)
proof
let c1 be non empty set ;
let c2, c3, c4 be Element of Funcs c1,BOOLEAN ;
E4: c2 '&' (c3 'xor' c4) = c2 '&' ((('not' c3) '&' c4) 'or' (c3 '&' ('not' c4))) by BVFUNC_4:9
.= (c2 '&' (('not' c3) '&' c4)) 'or' (c2 '&' (c3 '&' ('not' c4))) by BVFUNC_1:15
.= ((c2 '&' c4) '&' ('not' c3)) 'or' (c2 '&' (c3 '&' ('not' c4))) by BVFUNC_1:7
.= ((c2 '&' c4) '&' ('not' c3)) 'or' ((c2 '&' c3) '&' ('not' c4)) by BVFUNC_1:7 ;
E5: (c2 '&' c3) 'xor' (c2 '&' c4) = (('not' (c2 '&' c3)) '&' (c2 '&' c4)) 'or' ((c2 '&' c3) '&' ('not' (c2 '&' c4))) by BVFUNC_4:9
.= ((('not' c2) 'or' ('not' c3)) '&' (c2 '&' c4)) 'or' ((c2 '&' c3) '&' ('not' (c2 '&' c4))) by BVFUNC_1:17
.= ((c2 '&' c4) '&' (('not' c2) 'or' ('not' c3))) 'or' ((c2 '&' c3) '&' (('not' c2) 'or' ('not' c4))) by BVFUNC_1:17
.= (((c2 '&' c4) '&' ('not' c2)) 'or' ((c2 '&' c4) '&' ('not' c3))) 'or' ((c2 '&' c3) '&' (('not' c2) 'or' ('not' c4))) by BVFUNC_1:15
.= (((c2 '&' c4) '&' ('not' c2)) 'or' ((c2 '&' c4) '&' ('not' c3))) 'or' (((c2 '&' c3) '&' ('not' c2)) 'or' ((c2 '&' c3) '&' ('not' c4))) by BVFUNC_1:15
.= ((c2 '&' c4) '&' ('not' c2)) 'or' (((c2 '&' c4) '&' ('not' c3)) 'or' (((c2 '&' c3) '&' ('not' c4)) 'or' ((c2 '&' c3) '&' ('not' c2)))) by BVFUNC_1:11
.= ((c2 '&' c4) '&' ('not' c2)) 'or' ((((c2 '&' c4) '&' ('not' c3)) 'or' ((c2 '&' c3) '&' ('not' c4))) 'or' ((c2 '&' c3) '&' ('not' c2))) by BVFUNC_1:11
.= (((c2 '&' c4) '&' ('not' c2)) 'or' ((c2 '&' c3) '&' ('not' c2))) 'or' (((c2 '&' c4) '&' ('not' c3)) 'or' ((c2 '&' c3) '&' ('not' c4))) by BVFUNC_1:11 ;
((c4 '&' c2) '&' ('not' c2)) 'or' ((c3 '&' c2) '&' ('not' c2)) = (c4 '&' (c2 '&' ('not' c2))) 'or' ((c3 '&' c2) '&' ('not' c2)) by BVFUNC_1:7
.= (c4 '&' (c2 '&' ('not' c2))) 'or' (c3 '&' (c2 '&' ('not' c2))) by BVFUNC_1:7
.= (c4 '&' (O_el c1)) 'or' (c3 '&' (c2 '&' ('not' c2))) by BVFUNC_4:5
.= (c4 '&' (O_el c1)) 'or' (c3 '&' (O_el c1)) by BVFUNC_4:5
.= (O_el c1) 'or' (c3 '&' (O_el c1)) by BVFUNC_1:8
.= (O_el c1) 'or' (O_el c1) by BVFUNC_1:8
.= O_el c1 by BVFUNC_1:10 ;
hence c2 '&' (c3 'xor' c4) = (c2 '&' c3) 'xor' (c2 '&' c4) by E4, E5, BVFUNC_1:12;
end;

theorem :: BVFUNC25:12
for b1 being non empty set
for b2, b3 being Element of Funcs b1,BOOLEAN holds b2 'eqv' b3 = 'not' (b2 'xor' b3)
proof
let c1 be non empty set ;
let c2, c3 be Element of Funcs c1,BOOLEAN ;
'not' (c2 'xor' c3) = 'not' ('not' (c2 'eqv' c3)) by BVFUNC_8:12;
hence c2 'eqv' c3 = 'not' (c2 'xor' c3) by BVFUNC_1:4;
end;

theorem :: BVFUNC25:13
for b1 being non empty set
for b2 being Element of Funcs b1,BOOLEAN holds b2 'xor' b2 = O_el b1
proof
let c1 be non empty set ;
let c2 be Element of Funcs c1,BOOLEAN ;
thus c2 'xor' c2 = (('not' c2) '&' c2) 'or' (c2 '&' ('not' c2)) by BVFUNC_4:9
.= (O_el c1) 'or' (c2 '&' ('not' c2)) by BVFUNC_4:5
.= (O_el c1) 'or' (O_el c1) by BVFUNC_4:5
.= O_el c1 by BVFUNC_1:10 ;
end;

theorem :: BVFUNC25:14
for b1 being non empty set
for b2 being Element of Funcs b1,BOOLEAN holds b2 'xor' ('not' b2) = I_el b1
proof
let c1 be non empty set ;
let c2 be Element of Funcs c1,BOOLEAN ;
thus c2 'xor' ('not' c2) = (('not' c2) '&' ('not' c2)) 'or' (c2 '&' ('not' ('not' c2))) by BVFUNC_4:9
.= (('not' c2) '&' ('not' c2)) 'or' (c2 '&' c2) by BVFUNC_1:4
.= ('not' c2) 'or' (c2 '&' c2) by BVFUNC_1:6
.= ('not' c2) 'or' c2 by BVFUNC_1:6
.= I_el c1 by BVFUNC_4:6 ;
end;

theorem :: BVFUNC25:15
for b1 being non empty set
for b2, b3 being Element of Funcs b1,BOOLEAN holds (b2 'imp' b3) 'imp' (b3 'imp' b2) = b3 'imp' b2
proof
let c1 be non empty set ;
let c2, c3 be Element of Funcs c1,BOOLEAN ;
(c2 'imp' c3) 'imp' (c3 'imp' c2) = (('not' c2) 'or' c3) 'imp' (c3 'imp' c2) by BVFUNC_4:8
.= (('not' c2) 'or' c3) 'imp' (('not' c3) 'or' c2) by BVFUNC_4:8
.= ('not' (('not' c2) 'or' c3)) 'or' (('not' c3) 'or' c2) by BVFUNC_4:8
.= (('not' ('not' c2)) '&' ('not' c3)) 'or' (('not' c3) 'or' c2) by BVFUNC_1:16
.= (c2 '&' ('not' c3)) 'or' (('not' c3) 'or' c2) by BVFUNC_1:4
.= ((c2 '&' ('not' c3)) 'or' ('not' c3)) 'or' c2 by BVFUNC_1:11
.= ((c2 'or' ('not' c3)) '&' (('not' c3) 'or' ('not' c3))) 'or' c2 by BVFUNC_1:14
.= ((c2 'or' ('not' c3)) '&' ('not' c3)) 'or' c2 by BVFUNC_1:10
.= ((c2 'or' ('not' c3)) 'or' c2) '&' (('not' c3) 'or' c2) by BVFUNC_1:14
.= (('not' c3) 'or' (c2 'or' c2)) '&' (('not' c3) 'or' c2) by BVFUNC_1:11
.= (('not' c3) 'or' c2) '&' (('not' c3) 'or' c2) by BVFUNC_1:10
.= ('not' c3) 'or' c2 by BVFUNC_1:6 ;
hence (c2 'imp' c3) 'imp' (c3 'imp' c2) = c3 'imp' c2 by BVFUNC_4:8;
end;

theorem E4: :: BVFUNC25:16
for b1 being non empty set
for b2, b3 being Element of Funcs b1,BOOLEAN holds (b2 'or' b3) '&' (('not' b2) 'or' ('not' b3)) = (('not' b2) '&' b3) 'or' (b2 '&' ('not' b3))
proof
let c1 be non empty set ;
let c2, c3 be Element of Funcs c1,BOOLEAN ;
c2 'xor' c3 = (('not' c2) '&' c3) 'or' (c2 '&' ('not' c3)) by BVFUNC_4:9;
hence (c2 'or' c3) '&' (('not' c2) 'or' ('not' c3)) = (('not' c2) '&' c3) 'or' (c2 '&' ('not' c3)) by BVFUNC_8:13;
end;

theorem E5: :: BVFUNC25:17
for b1 being non empty set
for b2, b3 being Element of Funcs b1,BOOLEAN holds (b2 '&' b3) 'or' (('not' b2) '&' ('not' b3)) = (('not' b2) 'or' b3) '&' (b2 'or' ('not' b3))
proof
let c1 be non empty set ;
let c2, c3 be Element of Funcs c1,BOOLEAN ;
thus (c2 '&' c3) 'or' (('not' c2) '&' ('not' c3)) = (('not' ('not' c2)) '&' c3) 'or' (('not' c2) '&' ('not' c3)) by BVFUNC_1:4
.= (('not' c2) 'or' c3) '&' (('not' ('not' c2)) 'or' ('not' c3)) by E4
.= (('not' c2) 'or' c3) '&' (c2 'or' ('not' c3)) by BVFUNC_1:4 ;
end;

theorem :: BVFUNC25:18
for b1 being non empty set
for b2, b3, b4 being Element of Funcs b1,BOOLEAN holds b2 'xor' (b3 'xor' b4) = (b2 'xor' b3) 'xor' b4
proof
let c1 be non empty set ;
let c2, c3, c4 be Element of Funcs c1,BOOLEAN ;
E6: c2 'xor' (c3 'xor' c4) = (('not' c2) '&' (c3 'xor' c4)) 'or' (c2 '&' ('not' (c3 'xor' c4))) by BVFUNC_4:9
.= (('not' c2) '&' ((('not' c3) '&' c4) 'or' (c3 '&' ('not' c4)))) 'or' (c2 '&' ('not' (c3 'xor' c4))) by BVFUNC_4:9
.= (('not' c2) '&' ((('not' c3) '&' c4) 'or' (c3 '&' ('not' c4)))) 'or' (c2 '&' ('not' ((('not' c3) '&' c4) 'or' (c3 '&' ('not' c4))))) by BVFUNC_4:9
.= ((('not' c2) '&' (('not' c3) '&' c4)) 'or' (('not' c2) '&' (c3 '&' ('not' c4)))) 'or' (c2 '&' ('not' ((('not' c3) '&' c4) 'or' (c3 '&' ('not' c4))))) by BVFUNC_1:15
.= ((('not' c2) '&' (('not' c3) '&' c4)) 'or' (('not' c2) '&' (c3 '&' ('not' c4)))) 'or' (c2 '&' (('not' (('not' c3) '&' c4)) '&' ('not' (c3 '&' ('not' c4))))) by BVFUNC_1:16
.= ((('not' c2) '&' (('not' c3) '&' c4)) 'or' (('not' c2) '&' (c3 '&' ('not' c4)))) 'or' (c2 '&' ((('not' ('not' c3)) 'or' ('not' c4)) '&' ('not' (c3 '&' ('not' c4))))) by BVFUNC_1:17
.= ((('not' c2) '&' (('not' c3) '&' c4)) 'or' (('not' c2) '&' (c3 '&' ('not' c4)))) 'or' (c2 '&' ((c3 'or' ('not' c4)) '&' ('not' (c3 '&' ('not' c4))))) by BVFUNC_1:4
.= ((('not' c2) '&' (('not' c3) '&' c4)) 'or' (('not' c2) '&' (c3 '&' ('not' c4)))) 'or' (c2 '&' ((c3 'or' ('not' c4)) '&' (('not' c3) 'or' ('not' ('not' c4))))) by BVFUNC_1:17
.= ((('not' c2) '&' (('not' c3) '&' c4)) 'or' (('not' c2) '&' (c3 '&' ('not' c4)))) 'or' (c2 '&' ((c3 'or' ('not' c4)) '&' (('not' c3) 'or' c4))) by BVFUNC_1:4
.= ((('not' c2) '&' (('not' c3) '&' c4)) 'or' (('not' c2) '&' (c3 '&' ('not' c4)))) 'or' (c2 '&' ((c3 '&' c4) 'or' (('not' c3) '&' ('not' c4)))) by E5
.= ((('not' c2) '&' (('not' c3) '&' c4)) 'or' (('not' c2) '&' (c3 '&' ('not' c4)))) 'or' ((c2 '&' (c3 '&' c4)) 'or' (c2 '&' (('not' c3) '&' ('not' c4)))) by BVFUNC_1:15
.= (((('not' c2) '&' ('not' c3)) '&' c4) 'or' (('not' c2) '&' (c3 '&' ('not' c4)))) 'or' ((c2 '&' (c3 '&' c4)) 'or' (c2 '&' (('not' c3) '&' ('not' c4)))) by BVFUNC_1:7
.= (((('not' c2) '&' ('not' c3)) '&' c4) 'or' ((('not' c2) '&' c3) '&' ('not' c4))) 'or' ((c2 '&' (c3 '&' c4)) 'or' (c2 '&' (('not' c3) '&' ('not' c4)))) by BVFUNC_1:7
.= (((('not' c2) '&' ('not' c3)) '&' c4) 'or' ((('not' c2) '&' c3) '&' ('not' c4))) 'or' (((c2 '&' c3) '&' c4) 'or' (c2 '&' (('not' c3) '&' ('not' c4)))) by BVFUNC_1:7
.= (((c2 '&' c3) '&' c4) 'or' ((c2 '&' ('not' c3)) '&' ('not' c4))) 'or' (((('not' c2) '&' c3) '&' ('not' c4)) 'or' ((('not' c2) '&' ('not' c3)) '&' c4)) by BVFUNC_1:7
.= ((((c2 '&' c3) '&' c4) 'or' ((c2 '&' ('not' c3)) '&' ('not' c4))) 'or' ((('not' c2) '&' c3) '&' ('not' c4))) 'or' ((('not' c2) '&' ('not' c3)) '&' c4) by BVFUNC_1:11 ;
(c2 'xor' c3) 'xor' c4 = ((('not' c2) '&' c3) 'or' (c2 '&' ('not' c3))) 'xor' c4 by BVFUNC_4:9
.= (('not' ((('not' c2) '&' c3) 'or' (c2 '&' ('not' c3)))) '&' c4) 'or' (((('not' c2) '&' c3) 'or' (c2 '&' ('not' c3))) '&' ('not' c4)) by BVFUNC_4:9
.= ((('not' (('not' c2) '&' c3)) '&' ('not' (c2 '&' ('not' c3)))) '&' c4) 'or' (((('not' c2) '&' c3) 'or' (c2 '&' ('not' c3))) '&' ('not' c4)) by BVFUNC_1:16
.= (((('not' ('not' c2)) 'or' ('not' c3)) '&' ('not' (c2 '&' ('not' c3)))) '&' c4) 'or' (((('not' c2) '&' c3) 'or' (c2 '&' ('not' c3))) '&' ('not' c4)) by BVFUNC_1:17
.= (((c2 'or' ('not' c3)) '&' ('not' (c2 '&' ('not' c3)))) '&' c4) 'or' (((('not' c2) '&' c3) 'or' (c2 '&' ('not' c3))) '&' ('not' c4)) by BVFUNC_1:4
.= (((c2 'or' ('not' c3)) '&' (('not' c2) 'or' ('not' ('not' c3)))) '&' c4) 'or' (((('not' c2) '&' c3) 'or' (c2 '&' ('not' c3))) '&' ('not' c4)) by BVFUNC_1:17
.= (((c2 'or' ('not' c3)) '&' (('not' c2) 'or' c3)) '&' c4) 'or' (((('not' c2) '&' c3) 'or' (c2 '&' ('not' c3))) '&' ('not' c4)) by BVFUNC_1:4
.= (((c2 'or' ('not' c3)) '&' (('not' c2) 'or' c3)) '&' c4) 'or' (((('not' c2) '&' c3) '&' ('not' c4)) 'or' ((c2 '&' ('not' c3)) '&' ('not' c4))) by BVFUNC_1:15
.= (((c2 '&' c3) 'or' (('not' c2) '&' ('not' c3))) '&' c4) 'or' (((('not' c2) '&' c3) '&' ('not' c4)) 'or' ((c2 '&' ('not' c3)) '&' ('not' c4))) by E5
.= (((c2 '&' c3) '&' c4) 'or' ((('not' c2) '&' ('not' c3)) '&' c4)) 'or' (((('not' c2) '&' c3) '&' ('not' c4))