:: BVFUNC_9 semantic presentation
E1:
for b1 being non empty set
for b2, b3 being Element of Funcs b1,BOOLEAN holds b2 '&' b3 '<' b2
E2:
for b1 being non empty set
for b2, b3, b4 being Element of Funcs b1,BOOLEAN holds
( (b2 '&' b3) '&' b4 '<' b2 & (b2 '&' b3) '&' b4 '<' b3 )
E3:
for b1 being non empty set
for b2, b3, b4, b5 being Element of Funcs b1,BOOLEAN holds
( ((b2 '&' b3) '&' b4) '&' b5 '<' b2 & ((b2 '&' b3) '&' b4) '&' b5 '<' b3 )
E4:
for b1 being non empty set
for b2, b3, b4, b5, b6 being Element of Funcs b1,BOOLEAN holds
( (((b2 '&' b3) '&' b4) '&' b5) '&' b6 '<' b2 & (((b2 '&' b3) '&' b4) '&' b5) '&' b6 '<' b3 )
E5:
for b1 being non empty set
for b2, b3, b4, b5, b6, b7 being Element of Funcs b1,BOOLEAN holds
( ((((b2 '&' b3) '&' b4) '&' b5) '&' b6) '&' b7 '<' b2 & ((((b2 '&' b3) '&' b4) '&' b5) '&' b6) '&' b7 '<' b3 )
E6:
for b1 being non empty set
for b2, b3, b4, b5, b6, b7, b8 being Element of Funcs b1,BOOLEAN holds
( (((((b2 '&' b3) '&' b4) '&' b5) '&' b6) '&' b7) '&' b8 '<' b2 & (((((b2 '&' b3) '&' b4) '&' b5) '&' b6) '&' b7) '&' b8 '<' b3 )
E7:
for b1 being non empty set
for b2, b3, b4, b5, b6, b7, b8 being Element of Funcs b1,BOOLEAN holds
( ((((((b2 '&' b3) '&' b4) '&' b5) '&' b6) '&' b7) '&' b8) 'imp' b2 = I_el b1 & ((((((b2 '&' b3) '&' b4) '&' b5) '&' b6) '&' b7) '&' b8) 'imp' b3 = I_el b1 & ((((((b2 '&' b3) '&' b4) '&' b5) '&' b6) '&' b7) '&' b8) 'imp' b4 = I_el b1 & ((((((b2 '&' b3) '&' b4) '&' b5) '&' b6) '&' b7) '&' b8) 'imp' b5 = I_el b1 & ((((((b2 '&' b3) '&' b4) '&' b5) '&' b6) '&' b7) '&' b8) 'imp' b6 = I_el b1 & ((((((b2 '&' b3) '&' b4) '&' b5) '&' b6) '&' b7) '&' b8) 'imp' b7 = I_el b1 & ((((((b2 '&' b3) '&' b4) '&' b5) '&' b6) '&' b7) '&' b8) 'imp' b8 = I_el b1 )
proof
let c
1 be non
empty set ;
let c
2, c
3, c
4, c
5, c
6, c
7, c
8 be
Element of
Funcs c
1,
BOOLEAN ;
E8:
(((((c2 '&' c3) '&' c4) '&' c5) '&' c6) '&' c7) '&' c
8 '<' c
2
by E6;
E9:
(((((c2 '&' c3) '&' c4) '&' c5) '&' c6) '&' c7) '&' c
8 '<' c
3
by E6;
E10:
(((((c2 '&' c3) '&' c4) '&' c5) '&' c6) '&' c7) '&' c
8 '<' c
4
by E5;
E11:
(((((c2 '&' c3) '&' c4) '&' c5) '&' c6) '&' c7) '&' c
8 '<' c
5
by E4;
E12:
(((((c2 '&' c3) '&' c4) '&' c5) '&' c6) '&' c7) '&' c
8 '<' c
6
by E3;
E13:
(((((c2 '&' c3) '&' c4) '&' c5) '&' c6) '&' c7) '&' c
8 '<' c
7
by E2;
(((((c2 '&' c3) '&' c4) '&' c5) '&' c6) '&' c7) '&' c
8 '<' c
8
by E1;
hence
(
((((((c2 '&' c3) '&' c4) '&' c5) '&' c6) '&' c7) '&' c8) 'imp' c
2 = I_el c
1 &
((((((c2 '&' c3) '&' c4) '&' c5) '&' c6) '&' c7) '&' c8) 'imp' c
3 = I_el c
1 &
((((((c2 '&' c3) '&' c4) '&' c5) '&' c6) '&' c7) '&' c8) 'imp' c
4 = I_el c
1 &
((((((c2 '&' c3) '&' c4) '&' c5) '&' c6) '&' c7) '&' c8) 'imp' c
5 = I_el c
1 &
((((((c2 '&' c3) '&' c4) '&' c5) '&' c6) '&' c7) '&' c8) 'imp' c
6 = I_el c
1 &
((((((c2 '&' c3) '&' c4) '&' c5) '&' c6) '&' c7) '&' c8) 'imp' c
7 = I_el c
1 &
((((((c2 '&' c3) '&' c4) '&' c5) '&' c6) '&' c7) '&' c8) 'imp' c
8 = I_el c
1 )
by E8, E9, E10, E11, E12, E13, BVFUNC_1:19;
end;
theorem E8: :: BVFUNC_9:1
proof
let c
1 be non
empty set ;
let c
2, c
3, c
4 be
Element of
Funcs c
1,
BOOLEAN ;
let c
5 be
Element of c
1;
:: uses BVFUNC_1:def 15
assume E9:
Pj ((c2 'or' c3) '&' (c3 'imp' c4)),c
5 = TRUE
;
E10:
Pj ((c2 'or' c3) '&' (c3 'imp' c4)),c
5 =
(Pj (c2 'or' c3),c5) '&' (Pj (c3 'imp' c4),c5)
by VALUAT_1:def 6
.=
(Pj (c2 'or' c3),c5) '&' (Pj (('not' c3) 'or' c4),c5)
by BVFUNC_4:8
.=
(Pj (c2 'or' c3),c5) '&' ((Pj ('not' c3),c5) 'or' (Pj c4,c5))
by BVFUNC_1:def 7
.=
((Pj c2,c5) 'or' (Pj c3,c5)) '&' ((Pj ('not' c3),c5) 'or' (Pj c4,c5))
by BVFUNC_1:def 7
;
now
assume
Pj (c2 'or' c4),c
5 <> TRUE
;
then
Pj (c2 'or' c4),c
5 = FALSE
by MARGREL1:43;
then E11:
(Pj c2,c5) 'or' (Pj c4,c5) = FALSE
by BVFUNC_1:def 7;
E12:
(
Pj c
2,c
5 = TRUE or
Pj c
2,c
5 = FALSE )
by MARGREL1:39;
(
Pj c
4,c
5 = TRUE or
Pj c
4,c
5 = FALSE )
by MARGREL1:39;
then
(
Pj c
2,c
5 = FALSE &
Pj c
4,c
5 = FALSE )
by E11, E12, BINARITH:19;
then ((Pj c2,c5) 'or' (Pj c3,c5)) '&' ((Pj ('not' c3),c5) 'or' (Pj c4,c5)) =
(Pj c3,c5) '&' ((Pj ('not' c3),c5) 'or' FALSE )
by BINARITH:7
.=
(Pj c3,c5) '&' (Pj ('not' c3),c5)
by BINARITH:7
.=
(Pj c3,c5) '&' ('not' (Pj c3,c5))
by VALUAT_1:def 5
.=
FALSE
by MARGREL1:46
;
hence
not verum
by E9, E10, MARGREL1:43;
end;
hence
Pj (c2 'or' c4),c
5 = TRUE
;
end;
theorem E9: :: BVFUNC_9:2
proof
let c
1 be non
empty set ;
let c
2, c
3 be
Element of
Funcs c
1,
BOOLEAN ;
let c
4 be
Element of c
1;
:: uses BVFUNC_1:def 15
assume E10:
Pj (c2 '&' (c2 'imp' c3)),c
4 = TRUE
;
E11:
Pj (c2 '&' (c2 'imp' c3)),c
4 =
(Pj c2,c4) '&' (Pj (c2 'imp' c3),c4)
by VALUAT_1:def 6
.=
(Pj c2,c4) '&' (Pj (('not' c2) 'or' c3),c4)
by BVFUNC_4:8
.=
(Pj c2,c4) '&' ((Pj ('not' c2),c4) 'or' (Pj c3,c4))
by BVFUNC_1:def 7
.=
((Pj c2,c4) '&' (Pj ('not' c2),c4)) 'or' ((Pj c2,c4) '&' (Pj c3,c4))
by BINARITH:22
.=
((Pj c2,c4) '&' ('not' (Pj c2,c4))) 'or' ((Pj c2,c4) '&' (Pj c3,c4))
by VALUAT_1:def 5
.=
FALSE 'or' ((Pj c2,c4) '&' (Pj c3,c4))
by MARGREL1:46
.=
(Pj c2,c4) '&' (Pj c3,c4)
by BINARITH:7
;
hence
Pj c
3,c
4 = TRUE
;
end;
theorem :: BVFUNC_9:3
proof
let c
1 be non
empty set ;
let c
2, c
3 be
Element of
Funcs c
1,
BOOLEAN ;
let c
4 be
Element of c
1;
:: uses BVFUNC_1:def 15
assume E10:
Pj ((c2 'imp' c3) '&' ('not' c3)),c
4 = TRUE
;
E11:
Pj ((c2 'imp' c3) '&' ('not' c3)),c
4 =
(Pj (c2 'imp' c3),c4) '&' (Pj ('not' c3),c4)
by VALUAT_1:def 6
.=
(Pj (('not' c2) 'or' c3),c4) '&' (Pj ('not' c3),c4)
by BVFUNC_4:8
.=
(Pj ('not' c3),c4) '&' ((Pj ('not' c2),c4) 'or' (Pj c3,c4))
by BVFUNC_1:def 7
.=
((Pj ('not' c3),c4) '&' (Pj ('not' c2),c4)) 'or' ((Pj ('not' c3),c4) '&' (Pj c3,c4))
by BINARITH:22
.=
((Pj ('not' c3),c4) '&' (Pj ('not' c2),c4)) 'or' (('not' (Pj c3,c4)) '&' (Pj c3,c4))
by VALUAT_1:def 5
.=
((Pj ('not' c3),c4) '&' (Pj ('not' c2),c4)) 'or' FALSE
by MARGREL1:46
.=
(Pj ('not' c3),c4) '&' (Pj ('not' c2),c4)
by BINARITH:7
;
hence
Pj ('not' c2),c
4 = TRUE
;
end;
theorem :: BVFUNC_9:4
proof
let c
1 be non
empty set ;
let c
2, c
3 be
Element of
Funcs c
1,
BOOLEAN ;
let c
4 be
Element of c
1;
:: uses BVFUNC_1:def 15
assume E10:
Pj ((c2 'or' c3) '&' ('not' c2)),c
4 = TRUE
;
E11:
Pj ((c2 'or' c3) '&' ('not' c2)),c
4 =
(Pj (c2 'or' c3),c4) '&' (Pj ('not' c2),c4)
by VALUAT_1:def 6
.=
(Pj ('not' c2),c4) '&' ((Pj c2,c4) 'or' (Pj c3,c4))
by BVFUNC_1:def 7
.=
((Pj ('not' c2),c4) '&' (Pj c2,c4)) 'or' ((Pj ('not' c2),c4) '&' (Pj c3,c4))
by BINARITH:22
.=
(('not' (Pj c2,c4)) '&' (Pj c2,c4)) 'or' ((Pj ('not' c2),c4) '&' (Pj c3,c4))
by VALUAT_1:def 5
.=
FALSE 'or' ((Pj ('not' c2),c4) '&' (Pj c3,c4))
by MARGREL1:46
.=
(Pj ('not' c2),c4) '&' (Pj c3,c4)
by BINARITH:7
;
hence
Pj c
3,c
4 = TRUE
;
end;
theorem :: BVFUNC_9:5
proof
let c
1 be non
empty set ;
let c
2, c
3 be
Element of
Funcs c
1,
BOOLEAN ;
let c
4 be
Element of c
1;
:: uses BVFUNC_1:def 15
assume E10:
Pj ((c2 'imp' c3) '&' (('not' c2) 'imp' c3)),c
4 = TRUE
;
E11:
Pj ((c2 'imp' c3) '&' (('not' c2) 'imp' c3)),c
4 =
(Pj (c2 'imp' c3),c4) '&' (Pj (('not' c2) 'imp' c3),c4)
by VALUAT_1:def 6
.=
(Pj (('not' c2) 'or' c3),c4) '&' (Pj (('not' c2) 'imp' c3),c4)
by BVFUNC_4:8
.=
(Pj (('not' c2) 'or' c3),c4) '&' (Pj (('not' ('not' c2)) 'or' c3),c4)
by BVFUNC_4:8
.=
(Pj (('not' c2) 'or' c3),c4) '&' (Pj (c2 'or' c3),c4)
by BVFUNC_1:4
.=
((Pj ('not' c2),c4) 'or' (Pj c3,c4)) '&' (Pj (c2 'or' c3),c4)
by BVFUNC_1:def 7
.=
((Pj ('not' c2),c4) 'or' (Pj c3,c4)) '&' ((Pj c2,c4) 'or' (Pj c3,c4))
by BVFUNC_1:def 7
;
now
assume
Pj c
3,c
4 <> TRUE
;
then
Pj c
3,c
4 = FALSE
by MARGREL1:43;
then ((Pj ('not' c2),c4) 'or' (Pj c3,c4)) '&' ((Pj c2,c4) 'or' (Pj c3,c4)) =
(Pj ('not' c2),c4) '&' ((Pj c2,c4) 'or' FALSE )
by BINARITH:7
.=
(Pj ('not' c2),c4) '&' (Pj c2,c4)
by BINARITH:7
.=
('not' (Pj c2,c4)) '&' (Pj c2,c4)
by VALUAT_1:def 5
.=
FALSE
by MARGREL1:46
;
hence
not verum
by E10, E11, MARGREL1:43;
end;
hence
Pj c
3,c
4 = TRUE
;
end;
theorem :: BVFUNC_9:6
proof
let c
1 be non
empty set ;
let c
2, c
3 be
Element of
Funcs c
1,
BOOLEAN ;
let c
4 be
Element of c
1;
:: uses BVFUNC_1:def 15
assume E10:
Pj ((c2 'imp' c3) '&' (c2 'imp' ('not' c3))),c
4 = TRUE
;
E11:
Pj ((c2 'imp' c3) '&' (c2 'imp' ('not' c3))),c
4 =
(Pj (c2 'imp' c3),c4) '&' (Pj (c2 'imp' ('not' c3)),c4)
by VALUAT_1:def 6
.=
(Pj (('not' c2) 'or' c3),c4) '&' (Pj (c2 'imp' ('not' c3)),c4)
by BVFUNC_4:8
.=
(Pj (('not' c2) 'or' c3),c4) '&' (Pj (('not' c2) 'or' ('not' c3)),c4)
by BVFUNC_4:8
.=
((Pj ('not' c2),c4) 'or' (Pj c3,c4)) '&' (Pj (('not' c2) 'or' ('not' c3)),c4)
by BVFUNC_1:def 7
.=
((Pj ('not' c2),c4) 'or' (Pj c3,c4)) '&' ((Pj ('not' c2),c4) 'or' (Pj ('not' c3),c4))
by BVFUNC_1:def 7
;
now
assume
Pj ('not' c2),c
4 <> TRUE
;
then
Pj ('not' c2),c
4 = FALSE
by MARGREL1:43;
then ((Pj ('not' c2),c4) 'or' (Pj c3,c4)) '&' ((Pj ('not' c2),c4) 'or' (Pj ('not' c3),c4)) =
(Pj c3,c4) '&' (FALSE 'or' (Pj ('not' c3),c4))
by BINARITH:7
.=
(Pj c3,c4) '&' (Pj ('not' c3),c4)
by BINARITH:7
.=
(Pj c3,c4) '&' ('not' (Pj c3,c4))
by VALUAT_1:def 5
.=
FALSE
by MARGREL1:46
;
hence
not verum
by E10, E11, MARGREL1:43;
end;
hence
Pj ('not' c2),c
4 = TRUE
;
end;
theorem :: BVFUNC_9:7
proof
let c
1 be non
empty set ;
let c
2, c
3, c
4 be
Element of
Funcs c
1,
BOOLEAN ;
let c
5 be
Element of c
1;
:: uses BVFUNC_1:def 15
assume E10:
Pj (c2 'imp' (c3 '&' c4)),c
5 = TRUE
;
E11:
Pj (c2 'imp' (c3 '&' c4)),c
5 =
Pj (('not' c2) 'or' (c3 '&' c4)),c
5
by BVFUNC_4:8
.=
(Pj ('not' c2),c5) 'or' (Pj (c3 '&' c4),c5)
by BVFUNC_1:def 7
.=
(Pj ('not' c2),c5) 'or' ((Pj c3,c5) '&' (Pj c4,c5))
by VALUAT_1:def 6
;
now
assume
Pj (c2 'imp' c3),c
5 <> TRUE
;
then
Pj (c2 'imp' c3),c
5 = FALSE
by MARGREL1:43;
then
Pj (('not' c2) 'or' c3),c
5 = FALSE
by BVFUNC_4:8;
then E12:
(Pj ('not' c2),c5) 'or' (Pj c3,c5) = FALSE
by BVFUNC_1:def 7;
(Pj ('not' c2),c5) 'or' ((Pj c3,c5) '&' (Pj c4,c5)) =
((Pj ('not' c2),c5) 'or' (Pj c3,c5)) '&' ((Pj ('not' c2),c5) 'or' (Pj c4,c5))
by BINARITH:23
.=
FALSE
by E12, MARGREL1:49
;
hence
not verum
by E10, E11, MARGREL1:43;
end;
hence
Pj (c2 'imp' c3),c
5 = TRUE
;
end;
theorem :: BVFUNC_9:8