:: BINARI_5 semantic presentation

definition
let c1, c2 be boolean set ;
func c1 'nand' c2 -> set equals :: BINARI_5:def 1
 'not' (a1 '&' a2);
correctness
coherence
'not' (c1 '&' c2) is set ;
;
commutativity
for b1 being set
for b2, b3 being boolean set holds
( b1 = 'not' (b2 '&' b3) implies b1 = 'not' (b3 '&' b2) ) ;
end;

:: deftheorem defines 'nand' BINARI_5:def 1 :
for b1, b2 being boolean set holds b1 'nand' b2 = 'not' (b1 '&' b2);

registration
let c1, c2 be boolean set ;
cluster a1 'nand' a2 -> boolean ;
correctness
coherence
c1 'nand' c2 is boolean;
;
end;

definition
let c1, c2 be Element of BOOLEAN ;
redefine func 'nand' as c1 'nand' c2 -> Element of BOOLEAN ;
correctness
coherence
c1 'nand' c2 is Element of BOOLEAN ;
by MARGREL1:def 15;
end;

definition
let c1, c2 be boolean set ;
func c1 'nor' c2 -> set equals :: BINARI_5:def 2
 'not' (a1 'or' a2);
correctness
coherence
'not' (c1 'or' c2) is set ;
;
commutativity
for b1 being set
for b2, b3 being boolean set holds
( b1 = 'not' (b2 'or' b3) implies b1 = 'not' (b3 'or' b2) ) ;
end;

:: deftheorem defines 'nor' BINARI_5:def 2 :
for b1, b2 being boolean set holds b1 'nor' b2 = 'not' (b1 'or' b2);

registration
let c1, c2 be boolean set ;
cluster a1 'nor' a2 -> boolean ;
correctness
coherence
c1 'nor' c2 is boolean;
;
end;

definition
let c1, c2 be Element of BOOLEAN ;
redefine func 'nor' as c1 'nor' c2 -> Element of BOOLEAN ;
correctness
coherence
c1 'nor' c2 is Element of BOOLEAN ;
by MARGREL1:def 15;
end;

definition
let c1, c2 be boolean set ;
func c1 'xnor' c2 -> set equals :: BINARI_5:def 3
 'not' (a1 'xor' a2);
correctness
coherence
'not' (c1 'xor' c2) is set ;
;
commutativity
for b1 being set
for b2, b3 being boolean set holds
( b1 = 'not' (b2 'xor' b3) implies b1 = 'not' (b3 'xor' b2) ) ;
end;

:: deftheorem defines 'xnor' BINARI_5:def 3 :
for b1, b2 being boolean set holds b1 'xnor' b2 = 'not' (b1 'xor' b2);

registration
let c1, c2 be boolean set ;
cluster a1 'xnor' a2 -> boolean ;
correctness
coherence
c1 'xnor' c2 is boolean;
;
end;

definition
let c1, c2 be Element of BOOLEAN ;
redefine func 'xnor' as c1 'xnor' c2 -> Element of BOOLEAN ;
correctness
coherence
c1 'xnor' c2 is Element of BOOLEAN ;
by MARGREL1:def 15;
end;

theorem :: BINARI_5:1
for b1 being boolean set holds TRUE 'nand' b1 = 'not' b1 by MARGREL1:50;

theorem :: BINARI_5:2
for b1 being boolean set holds FALSE 'nand' b1 = TRUE
proof
let c1 be boolean set ;
thus FALSE 'nand' c1 = 'not' (FALSE '&' c1)
.= 'not' FALSE by MARGREL1:49
.= TRUE by MARGREL1:41 ;
end;

theorem :: BINARI_5:3
for b1 being boolean set holds
( b1 'nand' b1 = 'not' b1 & 'not' (b1 'nand' b1) = b1 )
proof
let c1 be boolean set ;
c1 'nand' c1 = 'not' (c1 '&' c1)
.= 'not' c1 by BINARITH:16 ;
hence ( c1 'nand' c1 = 'not' c1 & 'not' (c1 'nand' c1) = c1 ) by MARGREL1:40;
end;

theorem :: BINARI_5:4
for b1, b2 being boolean set holds 'not' (b1 'nand' b2) = b1 '&' b2 by MARGREL1:40;

theorem :: BINARI_5:5
for b1 being boolean set holds
( b1 'nand' ('not' b1) = TRUE & 'not' (b1 'nand' ('not' b1)) = FALSE )
proof
let c1 be boolean set ;
c1 'nand' ('not' c1) = 'not' (c1 '&' ('not' c1))
.= 'not' FALSE by MARGREL1:46
.= TRUE by MARGREL1:41 ;
hence ( c1 'nand' ('not' c1) = TRUE & 'not' (c1 'nand' ('not' c1)) = FALSE ) by MARGREL1:41;
end;

theorem :: BINARI_5:6
for b1, b2, b3 being boolean set holds b1 'nand' (b2 '&' b3) = 'not' ((b1 '&' b2) '&' b3) by MARGREL1:52;

theorem :: BINARI_5:7
for b1, b2, b3 being boolean set holds b1 'nand' (b2 '&' b3) = (b1 '&' b2) 'nand' b3 by MARGREL1:52;

theorem :: BINARI_5:8
for b1, b2, b3 being boolean set holds b1 'nand' (b2 'or' b3) = ('not' (b1 '&' b2)) '&' ('not' (b1 '&' b3))
proof
let c1, c2, c3 be boolean set ;
thus c1 'nand' (c2 'or' c3) = 'not' (c1 '&' (c2 'or' c3))
.= 'not' ((c1 '&' c2) 'or' (c1 '&' c3)) by BINARITH:22
.= ('not' (c1 '&' c2)) '&' ('not' (c1 '&' c3)) by BINARITH:10 ;
end;

theorem :: BINARI_5:9
for b1, b2, b3 being boolean set holds b1 'nand' (b2 'xor' b3) = (b1 '&' b2) 'eqv' (b1 '&' b3)
proof
let c1, c2, c3 be boolean set ;
c1 'nand' (c2 'xor' c3) = 'not' (c1 '&' (c2 'xor' c3))
.= 'not' ((c1 '&' c2) 'xor' (c1 '&' c3)) by BINARITH:38 ;
hence c1 'nand' (c2 'xor' c3) = (c1 '&' c2) 'eqv' (c1 '&' c3) by BVFUNC_1:def 2;
end;

theorem :: BINARI_5:10
for b1 being boolean set holds TRUE 'nor' b1 = FALSE
proof
let c1 be boolean set ;
TRUE 'nor' c1 = 'not' (TRUE 'or' c1)
.= 'not' TRUE by BINARITH:19 ;
hence TRUE 'nor' c1 = FALSE by MARGREL1:41;
end;

theorem :: BINARI_5:11
for b1 being boolean set holds FALSE 'nor' b1 = 'not' b1 by BINARITH:7;

theorem :: BINARI_5:12
for b1 being boolean set holds
( b1 'nor' b1 = 'not' b1 & 'not' (b1 'nor' b1) = b1 )
proof
let c1 be boolean set ;
c1 'nor' c1 = 'not' (c1 'or' c1)
.= 'not' c1 by BINARITH:21 ;
hence ( c1 'nor' c1 = 'not' c1 & 'not' (c1 'nor' c1) = c1 ) by MARGREL1:40;
end;

theorem :: BINARI_5:13
for b1, b2 being boolean set holds 'not' (b1 'nor' b2) = b1 'or' b2 by MARGREL1:40;

theorem :: BINARI_5:14
for b1 being boolean set holds
( b1 'nor' ('not' b1) = FALSE & 'not' (b1 'nor' ('not' b1)) = TRUE )
proof
let c1 be boolean set ;
c1 'nor' ('not' c1) = 'not' (c1 'or' ('not' c1))
.= 'not' TRUE by BINARITH:18
.= FALSE by MARGREL1:41 ;
hence ( c1 'nor' ('not' c1) = FALSE & 'not' (c1 'nor' ('not' c1)) = TRUE ) by MARGREL1:41;
end;

theorem :: BINARI_5:15
for b1, b2, b3 being boolean set holds b1 'nor' (b2 '&' b3) = ('not' (b1 'or' b2)) 'or' ('not' (b1 'or' b3))
proof
let c1, c2, c3 be boolean set ;
c1 'nor' (c2 '&' c3) = 'not' (c1 'or' (c2 '&' c3))
.= 'not' ((c1 'or' c2) '&' (c1 'or' c3)) by BINARITH:23
.= ('not' (c1 'or' c2)) 'or' ('not' (c1 'or' c3)) by BINARITH:9 ;
hence c1 'nor' (c2 '&' c3) = ('not' (c1 'or' c2)) 'or' ('not' (c1 'or' c3)) ;
end;

theorem :: BINARI_5:16
for b1, b2, b3 being boolean set holds b1 'nor' (b2 'or' b3) = 'not' ((b1 'or' b2) 'or' b3) by BINARITH:20;

theorem :: BINARI_5:17
for b1 being boolean set holds TRUE 'xnor' b1 = b1
proof
let c1 be boolean set ;
TRUE 'xnor' c1 = 'not' (TRUE 'xor' c1)
.= 'not' ('not' c1) by BINARITH:13 ;
hence TRUE 'xnor' c1 = c1 by MARGREL1:40;
end;

theorem :: BINARI_5:18
for b1 being boolean set holds FALSE 'xnor' b1 = 'not' b1 by BINARITH:14;

theorem :: BINARI_5:19
for b1 being boolean set holds
( b1 'xnor' b1 = TRUE & 'not' (b1 'xnor' b1) = FALSE )
proof
let c1 be boolean set ;
c1 'xnor' c1 = 'not' (c1 'xor' c1)
.= 'not' ((('not' c1) '&' c1) 'or' (c1 '&' ('not' c1))) by BINARITH:def 2
.= 'not' (FALSE 'or' (c1 '&' ('not' c1))) by MARGREL1:46
.= 'not' (FALSE 'or' FALSE ) by MARGREL1:46
.= 'not' FALSE by BINARITH:7
.= TRUE by MARGREL1:41 ;
hence ( c1 'xnor' c1 = TRUE & 'not' (c1 'xnor' c1) = FALSE ) by MARGREL1:41;
end;

theorem :: BINARI_5:20
for b1, b2 being boolean set holds 'not' (b1 'xnor' b2) = b1 'xor' b2 by MARGREL1:40;

theorem :: BINARI_5:21
for b1 being boolean set holds
( b1 'xnor' ('not' b1) = FALSE & 'not' (b1 'xnor' ('not' b1)) = TRUE )
proof
let c1 be boolean set ;
c1 'xnor' ('not' c1) = 'not' (c1 'xor' ('not' c1))
.= 'not' TRUE by BINARITH:17
.= FALSE by MARGREL1:41 ;
hence ( c1 'xnor' ('not' c1) = FALSE & 'not' (c1 'xnor' ('not' c1)) = TRUE ) by MARGREL1:41;
end;

theorem :: BINARI_5:22
for b1, b2, b3 being boolean set holds
( b1 '<' b2 'imp' b3 iff b1 '&' b2 '<' b3 )
proof
let c1, c2, c3 be boolean set ;
E1: ( c1 '<' c2 'imp' c3 implies c1 '&' c2 '<' c3 )
proof
assume c1 '<' c2 'imp' c3 ;
then E2: c1 'imp' (c2 'imp' c3) = TRUE by BVFUNC_1:def 3;
c1 'imp' (c2 'imp' c3) = ('not' c1) 'or' (c2 'imp' c3) by BVFUNC_1:def 1
.= ('not' c1) 'or' (('not' c2) 'or' c3) by BVFUNC_1:def 1
.= (('not' c1) 'or' ('not' c2)) 'or' c3 by BINARITH:20
.= ('not' (c1 '&' c2)) 'or' c3 by BINARITH:9
.= (c1 '&' c2) 'imp' c3 by BVFUNC_1:def 1 ;
hence c1 '&' c2 '<' c3 by E2, BVFUNC_1:def 3;
end;
( c1 '&' c2 '<' c3 implies c1 '<' c2 'imp' c3 )
proof
assume c1 '&' c2 '<' c3 ;
then E2: (c1 '&' c2) 'imp' c3 = TRUE by BVFUNC_1:def 3;
(c1 '&' c2) 'imp' c3 = ('not' (c1 '&' c2)) 'or' c3 by BVFUNC_1:def 1
.= (('not' c1) 'or' ('not' c2)) 'or' c3 by BINARITH:9
.= ('not' c1) 'or' (('not' c2) 'or' c3) by BINARITH:20
.= ('not' c1) 'or' (c2 'imp' c3) by BVFUNC_1:def 1
.= c1 'imp' (c2 'imp' c3) by BVFUNC_1:def 1 ;
hence c1 '<' c2 'imp' c3 by E2, BVFUNC_1:def 3;
end;
hence ( c1 '<' c2 'imp' c3 iff c1 '&' c2 '<' c3 ) by E1;
end;

theorem E1: :: BINARI_5:23
for b1, b2 being boolean set holds b1 'eqv' b2 = (b1 'imp' b2) '&' (b2 'imp' b1)
proof
let c1, c2 be boolean set ;
thus c1 'eqv' c2 = 'not' (c1 'xor' c2) by BVFUNC_1:def 2
.= 'not' ((('not' c1) '&' c2) 'or' (c1 '&' ('not' c2))) by BINARITH:def 2
.= ('not' (('not' c1) '&' c2)) '&' ('not' (c1 '&' ('not' c2))) by BINARITH:10
.= (('not' ('not' c1)) 'or' ('not' c2)) '&' ('not' (c1 '&' ('not' c2))) by BINARITH:9
.= (('not' ('not' c1)) 'or' ('not' c2)) '&' (('not' c1) 'or' ('not' ('not' c2))) by BINARITH:9
.= (c1 'or' ('not' c2)) '&' (('not' c1) 'or' ('not' ('not' c2))) by MARGREL1:40
.= (c1 'or' ('not' c2)) '&' (('not' c1) 'or' c2) by MARGREL1:40
.= ((c1 'or' ('not' c2)) '&' ('not' c1)) 'or' ((c1 'or' ('not' c2)) '&' c2) by BINARITH:22
.= ((('not' c1) '&' c1) 'or' (('not' c1) '&' ('not' c2))) 'or' (c2 '&' (c1 'or' ('not' c2))) by BINARITH:22
.= ((('not' c1) '&' c1) 'or' (('not' c1) '&' ('not' c2))) 'or' ((c2 '&' c1) 'or' (c2 '&' ('not' c2))) by BINARITH:22
.= (FALSE 'or' (('not' c1) '&' ('not' c2))) 'or' ((c2 '&' c1) 'or' (c2 '&' ('not' c2))) by MARGREL1:46
.= (FALSE 'or' (('not' c1) '&' ('not' c2))) 'or' ((c2 '&' c1) 'or' FALSE ) by MARGREL1:46
.= (('not' c1) '&' ('not' c2)) 'or' ((c2 '&' c1) 'or' FALSE ) by BINARITH:7
.= (('not' c1) '&' ('not' c2)) 'or' (c2 '&' c1) by BINARITH:7
.= ((('not' c1) '&' ('not' c2)) 'or' c2) '&' ((('not' c1) '&' ('not' c2)) 'or' c1) by BINARITH:23
.= ((c2 'or' ('not' c1)) '&' (c2 'or' ('not' c2))) '&' (c1 'or' (('not' c1) '&' ('not' c2))) by BINARITH:23
.= ((c2 'or' ('not' c1)) '&' (c2 'or' ('not' c2))) '&' ((c1 'or' ('not' c1)) '&' (c1 'or' ('not' c2))) by BINARITH:23
.= ((c2 'or' ('not' c1)) '&' TRUE ) '&' ((c1 'or' ('not' c1)) '&' (c1 'or' ('not' c2))) by BINARITH:18
.= ((c2 'or' ('not' c1)) '&' TRUE ) '&' (TRUE '&' (c1 'or' ('not' c2))) by BINARITH:18
.= (c2 'or' ('not' c1)) '&' (TRUE '&' (c1 'or' ('not' c2))) by MARGREL1:50
.= (c2 'or' ('not' c1)) '&' (c1 'or' ('not' c2)) by MARGREL1:50
.= (c1 'imp' c2) '&' (c1 'or' ('not' c2)) by BVFUNC_1:def 1
.= (c1 'imp' c2) '&' (c2 'imp' c1) by BVFUNC_1:def 1 ;
end;

theorem E2: :: BINARI_5:24
for b1, b2 being boolean set holds
( b1 'eqv' b2 = TRUE iff ( b1 'imp' b2 = TRUE & b2 'imp' b1 = TRUE ) )
proof
let c1, c2 be boolean set ;
E3: ( c1 'eqv' c2 = TRUE implies ( c1 'imp' c2 = TRUE & c2 'imp' c1 = TRUE ) )
proof
assume c1 'eqv' c2 = TRUE ;
then (c1 'imp' c2) '&' (c2 'imp' c1) = TRUE by E1;
hence ( c1 'imp' c2 = TRUE & c2 'imp' c1 = TRUE ) by MARGREL1:45;
end;
( ( c1 'imp' c2 = TRUE & c2 'imp' c1 = TRUE ) implies ( c1 'eqv' c2 = TRUE ) )
proof
assume ( c1 'imp' c2 = TRUE & c2 'imp' c1 = TRUE ) ;
then (c1 'imp' c2) '&' (c2 'imp' c1) = TRUE by MARGREL1:def 17;
hence c1 'eqv' c2 = TRUE by E1;
end;
hence ( c1 'eqv' c2 = TRUE iff ( c1 'imp' c2 = TRUE & c2 'imp' c1 = TRUE ) ) by E3;
end;

theorem E3: :: BINARI_5:25
for b1, b2 being boolean set holds
( ( b1 'imp' b2 = TRUE & b2 'imp' b1 = TRUE ) implies ( b1 = b2 ) )
proof
let c1, c2 be boolean set ;
assume E4: ( c1 'imp' c2 = TRUE & c2 'imp' c1 = TRUE ) ;
now
per cases not ( not ( c1 = FALSE & c2 = FALSE ) & not ( c1 = FALSE & c2 = TRUE ) & not ( c1 = TRUE & c2 = FALSE ) & not ( c1 = TRUE & c2 = TRUE ) ) by MARGREL1:39;
case ( c1 = FALSE & c2 = FALSE ) ;
hence c1 = c2 ;
end;
case E5: ( c1 = FALSE & c2 = TRUE ) ;
c2 'imp' c1 = ('not' c2) 'or' c1 by BVFUNC_1:def 1
.= FALSE 'or' FALSE by E5, MARGREL1:41
.= FALSE by BINARITH:7 ;
hence not verum by E4, MARGREL1:38;
end;
case E5: ( c1 = TRUE & c2 = FALSE ) ;
c1 'imp' c2 = ('not' c1) 'or' c2 by BVFUNC_1:def 1
.= FALSE 'or' FALSE by E5, MARGREL1:41
.= FALSE by BINARITH:7 ;
hence not verum by E4, MARGREL1:38;
end;
case ( c1 = TRUE & c2 = TRUE ) ;
hence c1 = c2 ;
end;
end;
end;
hence c1 = c2 ;
end;

theorem E4: :: BINARI_5:26
for b1, b2, b3 being boolean set holds
( ( b1 'imp' b2 = TRUE & b2 'imp' b3 = TRUE ) implies ( b1 'imp' b3 = TRUE ) )
proof
let c1, c2, c3 be boolean set ;
assume E5: ( c1 'imp' c2 = TRUE & c2 'imp' c3 = TRUE ) ;
E6: now
assume E7: c1 = TRUE ;
E8: c1 'imp' c2 = ('not' c1) 'or' c2 by BVFUNC_1:def 1
.= FALSE 'or' c2 by E7, MARGREL1:41
.= c2 by BINARITH:7 ;
c2 'imp' c3 = ('not' c2) 'or' c3 by BVFUNC_1:def 1
.= FALSE 'or' c3 by E5, E8, MARGREL1:41
.= c3 by BINARITH:7 ;
then c1 'imp' c3 = ('not' c1) 'or' TRUE by E5, BVFUNC_1:def 1;
hence c1 'imp' c3 = TRUE by BINARITH:19;
end;
now
assume E7: c1 <> TRUE ;
c1 'imp' c3 = ('not' c1) 'or' c3 by BVFUNC_1:def 1
.= ('not' FALSE ) 'or' c3 by E7, MARGREL1:39
.= TRUE 'or' c3 by MARGREL1:41 ;
hence c1 'imp' c3 = TRUE by BINARITH:19;
end;
hence c1 'imp' c3 = TRUE by E6;
end;

theorem :: BINARI_5:27
for b1, b2, b3 being boolean set holds
( ( b1 'eqv' b2 = TRUE & b2 'eqv' b3 = TRUE ) implies ( b1 'eqv' b3 = TRUE ) )
proof
let c1, c2, c3 be boolean set ;
assume E5: ( c1 'eqv' c2 = TRUE & c2 'eqv' c3 = TRUE ) ;
then E6: ( c1 'imp' c2 = TRUE & c2 'imp' c1 = TRUE ) by E2;
E7: ( c2 'imp' c3 = TRUE & c3 'imp' c2 = TRUE ) by E5, E2;
then E8: c1 'imp' c3 = TRUE by E6, E4;
c3 'imp' c1 = TRUE by E6, E7, E4;
hence c1 'eqv' c3 = TRUE by E8, E2;
end;

theorem E5: :: BINARI_5:28
for b1, b2 being boolean set holds b1 'imp' b2 = ('not' b2) 'imp' ('not' b1)
proof
let c1, c2 be boolean set ;
E6: (('not' c2) 'imp' ('not' c1)) 'imp' (c1 'imp' c2) = ('not' (('not' c2) 'imp' ('not' c1))) 'or' (c1 'imp' c2) by BVFUNC_1:def 1
.= ('not' (('not' ('not' c2)) 'or' ('not' c1))) 'or' (c1 'imp' c2) by BVFUNC_1:def 1
.= ('not' (c2 'or' ('not' c1))) 'or' (c1 'imp' c2) by MARGREL1:40
.= ('not' (c2 'or' ('not' c1))) 'or' (('not' c1) 'or' c2) by BVFUNC_1:def 1
.= TRUE by BINARITH:18 ;
(c1 'imp' c2) 'imp' (('not' c2) 'imp' ('not' c1)) = ('not' (c1 'imp' c2)) 'or' (('not' c2) 'imp' ('not' c1)) by BVFUNC_1:def 1
.= ('not' (c1 'imp' c2)) 'or' (('not' ('not' c2)) 'or' ('not' c1)) by BVFUNC_1:def 1
.= ('not' (c1 'imp' c2)) 'or' (c2 'or' ('not' c1)) by MARGREL1:40
.= ('not' (('not' c1) 'or' c2)) 'or' (c2 'or' ('not' c1)) by BVFUNC_1:def 1
.= TRUE by BINARITH:18 ;
hence c1 'imp' c2 = ('not' c2) 'imp' ('not' c1) by E6, E3;
end;

theorem :: BINARI_5:29
for b1, b2 being boolean set holds b1 'eqv' b2 = ('not' b1) 'eqv' ('not' b2)
proof
let c1, c2 be boolean set ;
thus ('not' c1) 'eqv' ('not' c2) = (('not' c1) 'imp' ('not' c2)) '&' (('not' c2) 'imp' ('not' c1)) by E1
.= (c2 'imp' c1) '&' (('not' c2) 'imp' ('not' c1)) by E5
.= (c2 'imp' c1) '&' (c1 'imp' c2) by E5
.= c1 'eqv' c2 by E1 ;
end;

theorem :: BINARI_5:30
for b1, b2, b3, b4 being boolean set holds
( ( b1 'eqv' b2 = TRUE & b3 'eqv' b4 = TRUE ) implies ( (b1 '&' b3) 'eqv' (b2 '&' b4) = TRUE ) )
proof
let c1, c2, c3, c4 be boolean set ;
assume E6: ( c1 'eqv' c2 = TRUE & c3 'eqv' c4 = TRUE ) ;
then E7: ( c1 'imp' c2 = TRUE & c2 'imp' c1 = TRUE ) by E2;
E8: ( c3 'imp' c4 = TRUE & c4 'imp' c3 = TRUE ) by E6, E2;
E9: ('not' c1) 'or' c2 = TRUE by E7, BVFUNC_1:def 1;
E10: ('not' c2) 'or' c1 = TRUE by E7, BVFUNC_1:def 1;
E11: ('not' c3) 'or' c4 = TRUE by E8, BVFUNC_1:def 1;
E12: ('not' c4) 'or' c3 = TRUE by E8, BVFUNC_1:def 1;
(c1 '&' c3) 'eqv' (c2 '&' c4) = ((c1 '&' c3) 'imp' (c2 '&' c4)) '&' ((c2 '&' c4) 'imp' (c1 '&' c3)) by E1
.= (('not' (c1 '&' c3)) 'or' (c2 '&' c4)) '&' ((c2 '&' c4) 'imp' (c1 '&' c3)) by BVFUNC_1:def 1
.= (('not' (c1 '&' c3)) 'or' (c2 '&' c4)) '&' (('not' (c2 '&' c4)) 'or' (c1 '&' c3)) by BVFUNC_1:def 1
.= ((('not' c1) 'or' ('not' c3)) 'or' (c2 '&' c4)) '&' (('not' (c2 '&' c4)) 'or' (c1 '&' c3)) by BINARITH:9
.= ((('not' c1) 'or' ('not' c3)) 'or' (c2 '&' c4)) '&' ((('not' c2) 'or' ('not' c4)) 'or' (c1 '&' c3)) by BINARITH:9
.= (((('not' c1) 'or' ('not' c3)) 'or' c2) '&' ((('not' c1) 'or' ('not' c3)) 'or' c4)) '&' ((('not' c2) 'or' ('not' c4)) 'or' (c1 '&' c3)) by BINARITH:23
.= (((('not' c1) 'or' ('not' c3)) 'or' c2) '&' ((('not' c1) 'or' ('not' c3)) 'or' c4)) '&' (((('not' c2) 'or' ('not' c4)) 'or' c1) '&' ((('not' c2) 'or' ('not' c4)) 'or' c3)) by BINARITH:23
.= (((('not' c1) 'or' c2) 'or' ('not' c3)) '&' ((('not' c1) 'or' ('not' c3)) 'or' c4)) '&' (((('not' c2) 'or' ('not' c4)) 'or' c1) '&' ((('not' c2) 'or' ('not' c4)) 'or' c3)) by BINARITH:20
.= (TRUE '&' ((('not' c1) 'or' ('not' c3)) 'or' c4)) '&' (((('not' c2) 'or' ('not' c4)) 'or' c1) '&' ((('not' c2) 'or' ('not' c4)) 'or' c3)) by E9, BINARITH:19
.= ((('not' c1) 'or' ('not' c3)) 'or' c4) '&' (((('not' c2) 'or' ('not' c4)) 'or' c1) '&' ((('not' c2) 'or' ('not' c4)) 'or' c3)) by MARGREL1:50
.= (('not' c1) 'or' (('not' c3) 'or' c4)) '&' (((('not' c2) 'or' ('not' c4)) 'or' c1) '&' ((('not' c2) 'or' ('not' c4)) 'or' c3)) by BINARITH:20
.= TRUE '&' (((('not' c2) 'or' ('not' c4)) 'or' c1) '&' ((('not' c2) 'or' ('not' c4)) 'or' c3)) by E11, BINARITH:19
.= ((('not' c2) 'or' ('not' c4)) 'or' c1) '&' ((('not' c2) 'or' ('not' c4)) 'or' c3) by MARGREL1:50
.= ((('not' c2) 'or' ('not' c4)) 'or' c1) '&' (('not' c2) 'or' (('not' c4) 'or' c3)) by BINARITH:20
.= ((('not' c2) 'or' ('not' c4)) 'or' c1) '&' TRUE by E12, BINARITH:19
.= (('not' c2) 'or' ('not' c4)) 'or' c1 by MARGREL1:50
.= ('not' c4) 'or' (('not' c2) 'or' c1) by BINARITH:20
.= TRUE by E10, BINARITH:19 ;
hence (c1 '&' c3) 'eqv' (c2 '&' c4) = TRUE ;
end;

theorem :: BINARI_5:31
for b1, b2, b3, b4 being boolean set holds
( ( b1 'eqv' b2 = TRUE & b3 'eqv' b4 = TRUE ) implies ( (b1 'imp' b3) 'eqv' (b2 'imp' b4) = TRUE ) )
proof
let c1, c2, c3, c4 be boolean set ;
assume E6: ( c1 'eqv' c2 = TRUE & c3 'eqv' c4 = TRUE ) ;
then E7: ( c1 'imp' c2 = TRUE & c2 'imp' c1 = TRUE ) by E2;
E8: ( c3 'imp' c4 = TRUE & c4 'imp' c3 = TRUE ) by E6, E2;
E9: ('not' c1) 'or' c2 = TRUE by E7, BVFUNC_1:def 1;
E10: ('not' c2) 'or' c1 = TRUE by E7, BVFUNC_1:def 1;
E11: ('not' c3) 'or' c4 = TRUE by E8, BVFUNC_1:def 1;
E12: ('not' c4) 'or' c3 = TRUE by E8, BVFUNC_1:def 1;
(c1 'imp' c3) 'eqv' (c2 'imp' c4) = ((c1 'imp' c3) 'imp' (c2 'imp' c4)) '&' ((c2 'imp' c4) 'imp' (c1 'imp' c3)) by E1
.= (('not' (c1 'imp' c3)) 'or' (c2 'imp' c4)) '&' ((c2 'imp' c4) 'imp' (c1 'imp' c3)) by BVFUNC_1:def 1
.= (('not' (c1 'imp' c3)) 'or' (c2 'imp' c4)) '&' (('not' (c2 'imp' c4)) 'or' (c1 'imp' c3)) by BVFUNC_1:def 1
.= (('not' (('not' c1) 'or' c3)) 'or' (c2 'imp' c4)) '&' (('not' (c2 'imp' c4)) 'or' (c1 'imp' c3)) by BVFUNC_1:def 1
.= (('not' (('not' c1) 'or' c3)) 'or' (('not' c2) 'or' c4)) '&' (('not' (c2 'imp' c4)) 'or' (c1 'imp' c3)) by BVFUNC_1:def 1
.= (('not' (('not' c1) 'or' c3)) 'or' (('not' c2) 'or' c4)) '&' (('not' (('not' c2) 'or' c4)) 'or' (c1 'imp' c3)) by BVFUNC_1:def 1
.= (('not' ((<