:: BVFUNC_8 semantic presentation

theorem Th1: :: BVFUNC_8:1
for b1 being non empty set
for b2, b3, b4, b5 being Element of Funcs b1,BOOLEAN holds b2 'imp' ((b3 '&' b4) '&' b5) = ((b2 'imp' b3) '&' (b2 'imp' b4)) '&' (b2 'imp' b5)
proof
let c1 be non empty set ;
let c2, c3, c4, c5 be Element of Funcs c1,BOOLEAN ;
E1: for b1 being Element of c1 holds (c2 'imp' ((c3 '&' c4) '&' c5)) . b1 = (((c2 'imp' c3) '&' (c2 'imp' c4)) '&' (c2 'imp' c5)) . b1
proof
let c6 be Element of c1;
(((c2 'imp' c3) '&' (c2 'imp' c4)) '&' (c2 'imp' c5)) . c6 = (((c2 'imp' c3) '&' (c2 'imp' c4)) . c6) '&' ((c2 'imp' c5) . c6) by VALUAT_1:def 6
.= (((c2 'imp' c3) . c6) '&' ((c2 'imp' c4) . c6)) '&' ((c2 'imp' c5) . c6) by VALUAT_1:def 6
.= ((('not' (c2 . c6)) 'or' (c3 . c6)) '&' ((c2 'imp' c4) . c6)) '&' ((c2 'imp' c5) . c6) by BVFUNC_1:def 11
.= ((('not' (c2 . c6)) 'or' (c3 . c6)) '&' (('not' (c2 . c6)) 'or' (c4 . c6))) '&' ((c2 'imp' c5) . c6) by BVFUNC_1:def 11
.= ((('not' (c2 . c6)) 'or' (c3 . c6)) '&' (('not' (c2 . c6)) 'or' (c4 . c6))) '&' (('not' (c2 . c6)) 'or' (c5 . c6)) by BVFUNC_1:def 11
.= (('not' (c2 . c6)) 'or' ((c3 . c6) '&' (c4 . c6))) '&' (('not' (c2 . c6)) 'or' (c5 . c6)) by BINARITH:23
.= ('not' (c2 . c6)) 'or' (((c3 . c6) '&' (c4 . c6)) '&' (c5 . c6)) by BINARITH:23
.= ('not' (c2 . c6)) 'or' (((c3 '&' c4) . c6) '&' (c5 . c6)) by VALUAT_1:def 6
.= ('not' (c2 . c6)) 'or' (((c3 '&' c4) '&' c5) . c6) by VALUAT_1:def 6
.= (c2 'imp' ((c3 '&' c4) '&' c5)) . c6 by BVFUNC_1:def 11 ;
hence (c2 'imp' ((c3 '&' c4) '&' c5)) . c6 = (((c2 'imp' c3) '&' (c2 'imp' c4)) '&' (c2 'imp' c5)) . c6 ;
end;
consider c6 being Function such that
E2: ( c2 'imp' ((c3 '&' c4) '&' c5) = c6 & dom c6 = c1 & rng c6 c= BOOLEAN ) by FUNCT_2:def 2;
consider c7 being Function such that
E3: ( ((c2 'imp' c3) '&' (c2 'imp' c4)) '&' (c2 'imp' c5) = c7 & dom c7 = c1 & rng c7 c= BOOLEAN ) by FUNCT_2:def 2;
( c1 = dom c6 & c1 = dom c7 & ( for b1 being set holds
( b1 in c1 implies c6 . b1 = c7 . b1 ) ) ) by E1, E2, E3;
hence c2 'imp' ((c3 '&' c4) '&' c5) = ((c2 'imp' c3) '&' (c2 'imp' c4)) '&' (c2 'imp' c5) by E2, E3, FUNCT_1:9;
end;

theorem Th2: :: BVFUNC_8:2
for b1 being non empty set
for b2, b3, b4, b5 being Element of Funcs b1,BOOLEAN holds b2 'imp' ((b3 'or' b4) 'or' b5) = ((b2 'imp' b3) 'or' (b2 'imp' b4)) 'or' (b2 'imp' b5)
proof
let c1 be non empty set ;
let c2, c3, c4, c5 be Element of Funcs c1,BOOLEAN ;
E1: for b1 being Element of c1 holds (c2 'imp' ((c3 'or' c4) 'or' c5)) . b1 = (((c2 'imp' c3) 'or' (c2 'imp' c4)) 'or' (c2 'imp' c5)) . b1
proof
let c6 be Element of c1;
(((c2 'imp' c3) 'or' (c2 'imp' c4)) 'or' (c2 'imp' c5)) . c6 = (((c2 'imp' c3) 'or' (c2 'imp' c4)) . c6) 'or' ((c2 'imp' c5) . c6) by BVFUNC_1:def 7
.= (((c2 'imp' c3) . c6) 'or' ((c2 'imp' c4) . c6)) 'or' ((c2 'imp' c5) . c6) by BVFUNC_1:def 7
.= ((('not' (c2 . c6)) 'or' (c3 . c6)) 'or' ((c2 'imp' c4) . c6)) 'or' ((c2 'imp' c5) . c6) by BVFUNC_1:def 11
.= ((('not' (c2 . c6)) 'or' (c3 . c6)) 'or' (('not' (c2 . c6)) 'or' (c4 . c6))) 'or' ((c2 'imp' c5) . c6) by BVFUNC_1:def 11
.= ((('not' (c2 . c6)) 'or' (c3 . c6)) 'or' (('not' (c2 . c6)) 'or' (c4 . c6))) 'or' (('not' (c2 . c6)) 'or' (c5 . c6)) by BVFUNC_1:def 11
.= ((('not' (c2 . c6)) 'or' (('not' (c2 . c6)) 'or' (c3 . c6))) 'or' (c4 . c6)) 'or' (('not' (c2 . c6)) 'or' (c5 . c6)) by BINARITH:20
.= (((('not' (c2 . c6)) 'or' ('not' (c2 . c6))) 'or' (c3 . c6)) 'or' (c4 . c6)) 'or' (('not' (c2 . c6)) 'or' (c5 . c6)) by BINARITH:20
.= ((('not' (c2 . c6)) 'or' (c3 . c6)) 'or' (c4 . c6)) 'or' (('not' (c2 . c6)) 'or' (c5 . c6)) by BINARITH:21
.= (('not' (c2 . c6)) 'or' ((c3 . c6) 'or' (c4 . c6))) 'or' (('not' (c2 . c6)) 'or' (c5 . c6)) by BINARITH:20
.= (('not' (c2 . c6)) 'or' ((c3 'or' c4) . c6)) 'or' (('not' (c2 . c6)) 'or' (c5 . c6)) by BVFUNC_1:def 7
.= (('not' (c2 . c6)) 'or' (('not' (c2 . c6)) 'or' ((c3 'or' c4) . c6))) 'or' (c5 . c6) by BINARITH:20
.= ((('not' (c2 . c6)) 'or' ('not' (c2 . c6))) 'or' ((c3 'or' c4) . c6)) 'or' (c5 . c6) by BINARITH:20
.= (('not' (c2 . c6)) 'or' ((c3 'or' c4) . c6)) 'or' (c5 . c6) by BINARITH:21
.= ('not' (c2 . c6)) 'or' (((c3 'or' c4) . c6) 'or' (c5 . c6)) by BINARITH:20
.= ('not' (c2 . c6)) 'or' (((c3 'or' c4) 'or' c5) . c6) by BVFUNC_1:def 7
.= (c2 'imp' ((c3 'or' c4) 'or' c5)) . c6 by BVFUNC_1:def 11 ;
hence (c2 'imp' ((c3 'or' c4) 'or' c5)) . c6 = (((c2 'imp' c3) 'or' (c2 'imp' c4)) 'or' (c2 'imp' c5)) . c6 ;
end;
consider c6 being Function such that
E2: ( c2 'imp' ((c3 'or' c4) 'or' c5) = c6 & dom c6 = c1 & rng c6 c= BOOLEAN ) by FUNCT_2:def 2;
consider c7 being Function such that
E3: ( ((c2 'imp' c3) 'or' (c2 'imp' c4)) 'or' (c2 'imp' c5) = c7 & dom c7 = c1 & rng c7 c= BOOLEAN ) by FUNCT_2:def 2;
( c1 = dom c6 & c1 = dom c7 & ( for b1 being set holds
( b1 in c1 implies c6 . b1 = c7 . b1 ) ) ) by E1, E2, E3;
hence c2 'imp' ((c3 'or' c4) 'or' c5) = ((c2 'imp' c3) 'or' (c2 'imp' c4)) 'or' (c2 'imp' c5) by E2, E3, FUNCT_1:9;
end;

theorem Th3: :: BVFUNC_8:3
for b1 being non empty set
for b2, b3, b4, b5 being Element of Funcs b1,BOOLEAN holds ((b2 '&' b3) '&' b4) 'imp' b5 = ((b2 'imp' b5) 'or' (b3 'imp' b5)) 'or' (b4 'imp' b5)
proof
let c1 be non empty set ;
let c2, c3, c4, c5 be Element of Funcs c1,BOOLEAN ;
E1: for b1 being Element of c1 holds (((c2 '&' c3) '&' c4) 'imp' c5) . b1 = (((c2 'imp' c5) 'or' (c3 'imp' c5)) 'or' (c4 'imp' c5)) . b1
proof
let c6 be Element of c1;
(((c2 'imp' c5) 'or' (c3 'imp' c5)) 'or' (c4 'imp' c5)) . c6 = (((c2 'imp' c5) 'or' (c3 'imp' c5)) . c6) 'or' ((c4 'imp' c5) . c6) by BVFUNC_1:def 7
.= (((c2 'imp' c5) . c6) 'or' ((c3 'imp' c5) . c6)) 'or' ((c4 'imp' c5) . c6) by BVFUNC_1:def 7
.= ((('not' (c2 . c6)) 'or' (c5 . c6)) 'or' ((c3 'imp' c5) . c6)) 'or' ((c4 'imp' c5) . c6) by BVFUNC_1:def 11
.= ((('not' (c2 . c6)) 'or' (c5 . c6)) 'or' (('not' (c3 . c6)) 'or' (c5 . c6))) 'or' ((c4 'imp' c5) . c6) by BVFUNC_1:def 11
.= ((('not' (c2 . c6)) 'or' (c5 . c6)) 'or' (('not' (c3 . c6)) 'or' (c5 . c6))) 'or' (('not' (c4 . c6)) 'or' (c5 . c6)) by BVFUNC_1:def 11
.= ((('not' (c2 . c6)) 'or' ((c5 . c6) 'or' ('not' (c3 . c6)))) 'or' (c5 . c6)) 'or' (('not' (c4 . c6)) 'or' (c5 . c6)) by BINARITH:20
.= (((('not' (c2 . c6)) 'or' ('not' (c3 . c6))) 'or' (c5 . c6)) 'or' (c5 . c6)) 'or' (('not' (c4 . c6)) 'or' (c5 . c6)) by BINARITH:20
.= ((('not' (c2 . c6)) 'or' ('not' (c3 . c6))) 'or' ((c5 . c6) 'or' (c5 . c6))) 'or' (('not' (c4 . c6)) 'or' (c5 . c6)) by BINARITH:20
.= ((('not' (c2 . c6)) 'or' ('not' (c3 . c6))) 'or' (c5 . c6)) 'or' (('not' (c4 . c6)) 'or' (c5 . c6)) by BINARITH:21
.= (('not' ((c2 . c6) '&' (c3 . c6))) 'or' (c5 . c6)) 'or' (('not' (c4 . c6)) 'or' (c5 . c6)) by BINARITH:9
.= (('not' ((c2 . c6) '&' (c3 . c6))) 'or' ((c5 . c6) 'or' ('not' (c4 . c6)))) 'or' (c5 . c6) by BINARITH:20
.= ((('not' ((c2 . c6) '&' (c3 . c6))) 'or' ('not' (c4 . c6))) 'or' (c5 . c6)) 'or' (c5 . c6) by BINARITH:20
.= (('not' ((c2 . c6) '&' (c3 . c6))) 'or' ('not' (c4 . c6))) 'or' ((c5 . c6) 'or' (c5 . c6)) by BINARITH:20
.= (('not' ((c2 . c6) '&' (c3 . c6))) 'or' ('not' (c4 . c6))) 'or' (c5 . c6) by BINARITH:21
.= ('not' (((c2 . c6) '&' (c3 . c6)) '&' (c4 . c6))) 'or' (c5 . c6) by BINARITH:9
.= ('not' (((c2 '&' c3) . c6) '&' (c4 . c6))) 'or' (c5 . c6) by VALUAT_1:def 6
.= ('not' (((c2 '&' c3) '&' c4) . c6)) 'or' (c5 . c6) by VALUAT_1:def 6
.= (((c2 '&' c3) '&' c4) 'imp' c5) . c6 by BVFUNC_1:def 11 ;
hence (((c2 '&' c3) '&' c4) 'imp' c5) . c6 = (((c2 'imp' c5) 'or' (c3 'imp' c5)) 'or' (c4 'imp' c5)) . c6 ;
end;
consider c6 being Function such that
E2: ( ((c2 '&' c3) '&' c4) 'imp' c5 = c6 & dom c6 = c1 & rng c6 c= BOOLEAN ) by FUNCT_2:def 2;
consider c7 being Function such that
E3: ( ((c2 'imp' c5) 'or' (c3 'imp' c5)) 'or' (c4 'imp' c5) = c7 & dom c7 = c1 & rng c7 c= BOOLEAN ) by FUNCT_2:def 2;
( c1 = dom c6 & c1 = dom c7 & ( for b1 being set holds
( b1 in c1 implies c6 . b1 = c7 . b1 ) ) ) by E1, E2, E3;
hence ((c2 '&' c3) '&' c4) 'imp' c5 = ((c2 'imp' c5) 'or' (c3 'imp' c5)) 'or' (c4 'imp' c5) by E2, E3, FUNCT_1:9;
end;

theorem Th4: :: BVFUNC_8:4
for b1 being non empty set
for b2, b3, b4, b5 being Element of Funcs b1,BOOLEAN holds ((b2 'or' b3) 'or' b4) 'imp' b5 = ((b2 'imp' b5) '&' (b3 'imp' b5)) '&' (b4 'imp' b5)
proof
let c1 be non empty set ;
let c2, c3, c4, c5 be Element of Funcs c1,BOOLEAN ;
E1: for b1 being Element of c1 holds (((c2 'or' c3) 'or' c4) 'imp' c5) . b1 = (((c2 'imp' c5) '&' (c3 'imp' c5)) '&' (c4 'imp' c5)) . b1
proof
let c6 be Element of c1;
(((c2 'imp' c5) '&' (c3 'imp' c5)) '&' (c4 'imp' c5)) . c6 = (((c2 'imp' c5) '&' (c3 'imp' c5)) . c6) '&' ((c4 'imp' c5) . c6) by VALUAT_1:def 6
.= (((c2 'imp' c5) . c6) '&' ((c3 'imp' c5) . c6)) '&' ((c4 'imp' c5) . c6) by VALUAT_1:def 6
.= ((('not' (c2 . c6)) 'or' (c5 . c6)) '&' ((c3 'imp' c5) . c6)) '&' ((c4 'imp' c5) . c6) by BVFUNC_1:def 11
.= ((('not' (c2 . c6)) 'or' (c5 . c6)) '&' (('not' (c3 . c6)) 'or' (c5 . c6))) '&' ((c4 'imp' c5) . c6) by BVFUNC_1:def 11
.= (((c5 . c6) 'or' ('not' (c2 . c6))) '&' (('not' (c3 . c6)) 'or' (c5 . c6))) '&' (('not' (c4 . c6)) 'or' (c5 . c6)) by BVFUNC_1:def 11
.= ((c5 . c6) 'or' (('not' (c2 . c6)) '&' ('not' (c3 . c6)))) '&' (('not' (c4 . c6)) 'or' (c5 . c6)) by BINARITH:23
.= (('not' ((c2 . c6) 'or' (c3 . c6))) 'or' (c5 . c6)) '&' (('not' (c4 . c6)) 'or' (c5 . c6)) by BINARITH:10
.= ((c5 . c6) 'or' ('not' ((c2 'or' c3) . c6))) '&' (('not' (c4 . c6)) 'or' (c5 . c6)) by BVFUNC_1:def 7
.= (c5 . c6) 'or' (('not' ((c2 'or' c3) . c6)) '&' ('not' (c4 . c6))) by BINARITH:23
.= ('not' (((c2 'or' c3) . c6) 'or' (c4 . c6))) 'or' (c5 . c6) by BINARITH:10
.= ('not' (((c2 'or' c3) 'or' c4) . c6)) 'or' (c5 . c6) by BVFUNC_1:def 7
.= (((c2 'or' c3) 'or' c4) 'imp' c5) . c6 by BVFUNC_1:def 11 ;
hence (((c2 'or' c3) 'or' c4) 'imp' c5) . c6 = (((c2 'imp' c5) '&' (c3 'imp' c5)) '&' (c4 'imp' c5)) . c6 ;
end;
consider c6 being Function such that
E2: ( ((c2 'or' c3) 'or' c4) 'imp' c5 = c6 & dom c6 = c1 & rng c6 c= BOOLEAN ) by FUNCT_2:def 2;
consider c7 being Function such that
E3: ( ((c2 'imp' c5) '&' (c3 'imp' c5)) '&' (c4 'imp' c5) = c7 & dom c7 = c1 & rng c7 c= BOOLEAN ) by FUNCT_2:def 2;
( c1 = dom c6 & c1 = dom c7 & ( for b1 being set holds
( b1 in c1 implies c6 . b1 = c7 . b1 ) ) ) by E1, E2, E3;
hence ((c2 'or' c3) 'or' c4) 'imp' c5 = ((c2 'imp' c5) '&' (c3 'imp' c5)) '&' (c4 'imp' c5) by E2, E3, FUNCT_1:9;
end;

theorem Th5: :: BVFUNC_8:5
for b1 being non empty set
for b2, b3, b4 being Element of Funcs b1,BOOLEAN holds ((b2 'imp' b3) '&' (b3 'imp' b4)) '&' (b4 'imp' b2) = ((((b2 'imp' b3) '&' (b3 'imp' b4)) '&' (b4 'imp' b2)) '&' (b3 'imp' b2)) '&' (b2 'imp' b4)
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) '&' (c3 'imp' c4)) '&' (c4 'imp' c2)) . b1 = (((((c2 'imp' c3) '&' (c3 'imp' c4)) '&' (c4 'imp' c2)) '&' (c3 'imp' c2)) '&' (c2 'imp' c4)) . b1
proof
let c5 be Element of c1;
((c2 'imp' c3) '&' (c3 'imp' c4)) '&' (c4 'imp' c2) = ((('not' c2) 'or' c3) '&' (c3 'imp' c4)) '&' (c4 'imp' c2) by BVFUNC_4:8
.= ((('not' c2) 'or' c3) '&' (('not' c3) 'or' c4)) '&' (c4 'imp' c2) by BVFUNC_4:8
.= ((('not' c2) 'or' c3) '&' (('not' c3) 'or' c4)) '&' (('not' c4) 'or' c2) by BVFUNC_4:8
.= ((('not' c2) '&' (('not' c3) 'or' c4)) 'or' (c3 '&' (('not' c3) 'or' c4))) '&' (('not' c4) 'or' c2) by BVFUNC_1:15
.= ((('not' c2) '&' (('not' c3) 'or' c4)) 'or' ((c3 '&' ('not' c3)) 'or' (c3 '&' c4))) '&' (('not' c4) 'or' c2) by BVFUNC_1:15
.= ((('not' c2) '&' (('not' c3) 'or' c4)) 'or' ((O_el c1) 'or' (c3 '&' c4))) '&' (('not' c4) 'or' c2) by BVFUNC_4:5
.= ((('not' c2) '&' (('not' c3) 'or' c4)) 'or' (c3 '&' c4)) '&' (('not' c4) 'or' c2) by BVFUNC_1:12
.= ((('not' c2) 'or' (c3 '&' c4)) '&' ((('not' c3) 'or' c4) 'or' (c3 '&' c4))) '&' (('not' c4) 'or' c2) by BVFUNC_1:14
.= (((('not' c2) 'or' c3) '&' (('not' c2) 'or' c4)) '&' ((('not' c3) 'or' c4) 'or' (c3 '&' c4))) '&' (('not' c4) 'or' c2) by BVFUNC_1:14
.= (((('not' c2) 'or' c3) '&' (('not' c2) 'or' c4)) '&' (((('not' c3) 'or' c4) 'or' c3) '&' ((('not' c3) 'or' c4) 'or' c4))) '&' (('not' c4) 'or' c2) by BVFUNC_1:14
.= (((('not' c2) 'or' c3) '&' (('not' c2) 'or' c4)) '&' ((c4 'or' (('not' c3) 'or' c3)) '&' ((('not' c3) 'or' c4) 'or' c4))) '&' (('not' c4) 'or' c2) by BVFUNC_1:11
.= (((('not' c2) 'or' c3) '&' (('not' c2) 'or' c4)) '&' ((c4 'or' (I_el c1)) '&' ((('not' c3) 'or' c4) 'or' c4))) '&' (('not' c4) 'or' c2) by BVFUNC_4:6
.= (((('not' c2) 'or' c3) '&' (('not' c2) 'or' c4)) '&' ((I_el c1) '&' ((('not' c3) 'or' c4) 'or' c4))) '&' (('not' c4) 'or' c2) by BVFUNC_1:13
.= (((('not' c2) 'or' c3) '&' (('not' c2) 'or' c4)) '&' ((('not' c3) 'or' c4) 'or' c4)) '&' (('not' c4) 'or' c2) by BVFUNC_1:9
.= (((('not' c2) 'or' c3) '&' (('not' c2) 'or' c4)) '&' (('not' c3) 'or' (c4 'or' c4))) '&' (('not' c4) 'or' c2) by BVFUNC_1:11
.= (((('not' c2) 'or' c3) '&' (('not' c2) 'or' c4)) '&' (('not' c3) 'or' c4)) '&' (('not' c4) 'or' c2) by BVFUNC_1:10
.= ((('not' c2) 'or' c3) '&' (('not' c2) 'or' c4)) '&' ((('not' c3) 'or' c4) '&' (('not' c4) 'or' c2)) by BVFUNC_1:7
.= ((('not' c2) 'or' c3) '&' (('not' c2) 'or' c4)) '&' ((('not' c3) '&' (('not' c4) 'or' c2)) 'or' (c4 '&' (('not' c4) 'or' c2))) by BVFUNC_1:15
.= ((('not' c2) 'or' c3) '&' (('not' c2) 'or' c4)) '&' ((('not' c3) '&' (('not' c4) 'or' c2)) 'or' ((c4 '&' ('not' c4)) 'or' (c4 '&' c2))) by BVFUNC_1:15
.= ((('not' c2) 'or' c3) '&' (('not' c2) 'or' c4)) '&' ((('not' c3) '&' (('not' c4) 'or' c2)) 'or' ((O_el c1) 'or' (c4 '&' c2))) by BVFUNC_4:5
.= ((('not' c2) 'or' c3) '&' (('not' c2) 'or' c4)) '&' ((('not' c3) '&' (('not' c4) 'or' c2)) 'or' (c4 '&' c2)) by BVFUNC_1:12
.= ((('not' c2) 'or' c3) '&' (('not' c2) 'or' c4)) '&' ((('not' c3) 'or' (c4 '&' c2)) '&' ((('not' c4) 'or' c2) 'or' (c4 '&' c2))) by BVFUNC_1:14
.= ((('not' c2) 'or' c3) '&' (('not' c2) 'or' c4)) '&' (((('not' c3) 'or' c4) '&' (('not' c3) 'or' c2)) '&' ((('not' c4) 'or' c2) 'or' (c4 '&' c2))) by BVFUNC_1:14
.= ((('not' c2) 'or' c4) '&' (('not' c2) 'or' c3)) '&' (((('not' c3) 'or' c2) '&' (('not' c3) 'or' c4)) '&' (((('not' c4) 'or' c2) 'or' c4) '&' ((('not' c4) 'or' c2) 'or' c2))) by BVFUNC_1:14
.= ((('not' c2) 'or' c4) '&' (('not' c2) 'or' c3)) '&' (((('not' c3) 'or' c2) '&' (('not' c3) 'or' c4)) '&' ((c2 'or' (('not' c4) 'or' c4)) '&' ((('not' c4) 'or' c2) 'or' c2))) by BVFUNC_1:11
.= ((('not' c2)