:: BINARI_6 semantic presentation

theorem E1: :: BINARI_6:1
for b1 being boolean set holds TRUE 'imp' b1 = b1
proof
let c1 be boolean set ;
thus TRUE 'imp' c1 = FALSE 'or' c1 by MARGREL1:def 16
.= c1 by BINARITH:7 ;
end;

theorem E2: :: BINARI_6:2
for b1 being boolean set holds FALSE 'imp' b1 = TRUE
proof
let c1 be boolean set ;
thus FALSE 'imp' c1 = TRUE 'or' c1 by MARGREL1:def 16
.= TRUE by BINARITH:19 ;
end;

theorem E3: :: BINARI_6:3
for b1 being boolean set holds
( b1 'imp' b1 = TRUE & 'not' (b1 'imp' b1) = FALSE )
proof
let c1 be boolean set ;
c1 'imp' c1 = TRUE by BINARITH:18;
hence ( c1 'imp' c1 = TRUE & 'not' (c1 'imp' c1) = FALSE ) by MARGREL1:41;
end;

theorem :: BINARI_6:4
for b1, b2 being boolean set holds 'not' (b1 'imp' b2) = b1 '&' ('not' b2)
proof
let c1, c2 be boolean set ;
thus 'not' (c1 'imp' c2) = ('not' ('not' c1)) '&' ('not' c2) by BINARITH:10
.= c1 '&' ('not' c2) by MARGREL1:40 ;
end;

theorem E4: :: BINARI_6:5
for b1 being boolean set holds
( b1 'imp' ('not' b1) = 'not' b1 & 'not' (b1 'imp' ('not' b1)) = b1 )
proof
let c1 be boolean set ;
c1 'imp' ('not' c1) = 'not' c1 by BINARITH:21;
hence ( c1 'imp' ('not' c1) = 'not' c1 & 'not' (c1 'imp' ('not' c1)) = c1 ) by MARGREL1:40;
end;

theorem E5: :: BINARI_6:6
for b1 being boolean set holds ('not' b1) 'imp' b1 = b1
proof
let c1 be boolean set ;
thus ('not' c1) 'imp' c1 = c1 'or' c1 by MARGREL1:40
.= c1 by BINARITH:21 ;
end;

theorem :: BINARI_6:7
for b1 being boolean set holds TRUE 'eqv' b1 = b1
proof
let c1 be boolean set ;
TRUE 'eqv' c1 = (TRUE 'imp' c1) '&' (c1 'imp' TRUE ) by BINARI_5:23
.= c1 '&' (c1 'imp' TRUE ) by E1
.= c1 '&' TRUE by BINARITH:19
.= c1 by MARGREL1:50 ;
hence TRUE 'eqv' c1 = c1 ;
end;

theorem :: BINARI_6:8
for b1 being boolean set holds FALSE 'eqv' b1 = 'not' b1
proof
let c1 be boolean set ;
FALSE 'eqv' c1 = (FALSE 'imp' c1) '&' (c1 'imp' FALSE ) by BINARI_5:23
.= TRUE '&' (c1 'imp' FALSE ) by E2
.= TRUE '&' ('not' c1) by BINARITH:7
.= 'not' c1 by MARGREL1:50 ;
hence FALSE 'eqv' c1 = 'not' c1 ;
end;

theorem :: BINARI_6:9
for b1 being boolean set holds
( b1 'eqv' b1 = TRUE & 'not' (b1 'eqv' b1) = FALSE )
proof
let c1 be boolean set ;
c1 'eqv' c1 = (c1 'imp' c1) '&' (c1 'imp' c1) by BINARI_5:23
.= c1 'imp' c1 by BINARITH:16
.= TRUE by E3 ;
hence ( c1 'eqv' c1 = TRUE & 'not' (c1 'eqv' c1) = FALSE ) by MARGREL1:41;
end;

theorem :: BINARI_6:10
for b1 being boolean set holds ('not' b1) 'eqv' b1 = FALSE
proof
let c1 be boolean set ;
('not' c1) 'eqv' c1 = (('not' c1) 'imp' c1) '&' (c1 'imp' ('not' c1)) by BINARI_5:23
.= c1 '&' (c1 'imp' ('not' c1)) by E5
.= c1 '&' ('not' c1) by E4
.= FALSE by MARGREL1:46 ;
hence ('not' c1) 'eqv' c1 = FALSE ;
end;

theorem :: BINARI_6:11
for b1, b2, b3 being boolean set holds b1 '&' (b2 'eqv' b3) = (b1 '&' (('not' b2) 'or' b3)) '&' (('not' b3) 'or' b2)
proof
let c1, c2, c3 be boolean set ;
thus c1 '&' (c2 'eqv' c3) = c1 '&' ((c2 'imp' c3) '&' (c3 'imp' c2)) by BINARI_5:23
.= (c1 '&' (('not' c2) 'or' c3)) '&' (('not' c3) 'or' c2) by MARGREL1:52 ;
end;

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

theorem E7: :: BINARI_6:13
for b1, b2, b3 being boolean set holds b1 '&' (b2 'nor' b3) = (b1 '&' ('not' b2)) '&' ('not' b3)
proof
let c1, c2, c3 be boolean set ;
thus c1 '&' (c2 'nor' c3) = c1 '&' (('not' c2) '&' ('not' c3)) by BINARITH:10
.= (c1 '&' ('not' c2)) '&' ('not' c3) by MARGREL1:52 ;
end;

theorem :: BINARI_6:14
for b1, b2 being boolean set holds b1 '&' (b1 '&' b2) = b1 '&' b2
proof
let c1, c2 be boolean set ;
thus c1 '&' (c1 '&' c2) = (c1 '&' c1) '&' c2 by MARGREL1:52
.= c1 '&' c2 by BINARITH:16 ;
end;

theorem :: BINARI_6:15
for b1, b2 being boolean set holds b1 '&' (b1 'or' b2) = b1 'or' (b1 '&' b2)
proof
let c1, c2 be boolean set ;
thus c1 '&' (c1 'or' c2) = (c1 '&' c1) 'or' (c1 '&' c2) by BINARITH:22
.= c1 'or' (c1 '&' c2) by BINARITH:16 ;
end;

theorem :: BINARI_6:16
for b1, b2 being boolean set holds b1 '&' (b1 'xor' b2) = b1 '&' ('not' b2)
proof
let c1, c2 be boolean set ;
thus c1 '&' (c1 'xor' c2) = c1 '&' ((('not' c1) '&' c2) 'or' (c1 '&' ('not' c2))) by BINARITH:def 2
.= (c1 '&' (('not' c1) '&' c2)) 'or' (c1 '&' (c1 '&' ('not' c2))) by BINARITH:22
.= ((c1 '&' ('not' c1)) '&' c2) 'or' (c1 '&' (c1 '&' ('not' c2))) by MARGREL1:52
.= ((c1 '&' ('not' c1)) '&' c2) 'or' ((c1 '&' c1) '&' ('not' c2)) by MARGREL1:52
.= (FALSE '&' c2) 'or' ((c1 '&' c1) '&' ('not' c2)) by MARGREL1:46
.= FALSE 'or' ((c1 '&' c1) '&' ('not' c2)) by MARGREL1:49
.= (c1 '&' c1) '&' ('not' c2) by BINARITH:7
.= c1 '&' ('not' c2) by BINARITH:16 ;
end;

theorem :: BINARI_6:17
for b1, b2 being boolean set holds b1 '&' (b1 'imp' b2) = b1 '&' b2
proof
let c1, c2 be boolean set ;
thus c1 '&' (c1 'imp' c2) = (c1 '&' ('not' c1)) 'or' (c1 '&' c2) by BINARITH:22
.= FALSE 'or' (c1 '&' c2) by MARGREL1:46
.= c1 '&' c2 by BINARITH:7 ;
end;

theorem E8: :: BINARI_6:18
for b1, b2 being boolean set holds b1 '&' (b1 'eqv' b2) = b1 '&' b2
proof
let c1, c2 be boolean set ;
thus c1 '&' (c1 'eqv' c2) = c1 '&' ((c1 'imp' c2) '&' (c2 'imp' c1)) by BINARI_5:23
.= (c1 '&' (('not' c1) 'or' c2)) '&' (('not' c2) 'or' c1) by MARGREL1:52
.= ((c1 '&' ('not' c1)) 'or' (c1 '&' c2)) '&' (('not' c2) 'or' c1) by BINARITH:22
.= (FALSE 'or' (c1 '&' c2)) '&' (('not' c2) 'or' c1) by MARGREL1:46
.= (c1 '&' c2) '&' (('not' c2) 'or' c1) by BINARITH:7
.= ((c1 '&' c2) '&' ('not' c2)) 'or' ((c1 '&' c2) '&' c1) by BINARITH:22
.= (c1 '&' (c2 '&' ('not' c2))) 'or' ((c1 '&' c2) '&' c1) by MARGREL1:52
.= (c1 '&' FALSE ) 'or' ((c1 '&' c2) '&' c1) by MARGREL1:46
.= FALSE 'or' ((c1 '&' c2) '&' c1) by MARGREL1:49
.= (c1 '&' c2) '&' c1 by BINARITH:7
.= c2 '&' (c1 '&' c1) by MARGREL1:52
.= c1 '&' c2 by BINARITH:16 ;
end;

theorem :: BINARI_6:19
for b1, b2 being boolean set holds b1 '&' (b1 'nand' b2) = b1 '&' ('not' b2)
proof
let c1, c2 be boolean set ;
thus c1 '&' (c1 'nand' c2) = (c1 '&' ('not' c1)) 'or' (c1 '&' ('not' c2)) by E6
.= FALSE 'or' (c1 '&' ('not' c2)) by MARGREL1:46
.= c1 '&' ('not' c2) by BINARITH:7 ;
end;

theorem :: BINARI_6:20
for b1, b2 being boolean set holds b1 '&' (b1 'nor' b2) = FALSE
proof
let c1, c2 be boolean set ;
thus c1 '&' (c1 'nor' c2) = (c1 '&' ('not' c1)) '&' ('not' c2) by E7
.= FALSE '&' ('not' c2) by MARGREL1:46
.= FALSE by MARGREL1:49 ;
end;

theorem :: BINARI_6:21
for b1, b2, b3 being boolean set holds b1 'or' (b2 'xor' b3) = (b1 'or' (('not' b2) '&' b3)) 'or' (b2 '&' ('not' b3))
proof
let c1, c2, c3 be boolean set ;
thus c1 'or' (c2 'xor' c3) = c1 'or' ((('not' c2) '&' c3) 'or' (c2 '&' ('not' c3))) by BINARITH:def 2
.= (c1 'or' (('not' c2) '&' c3)) 'or' (c2 '&' ('not' c3)) by BINARITH:20 ;
end;

theorem E9: :: BINARI_6:22
for b1, b2, b3 being boolean set holds b1 'or' (b2 'eqv' b3) = ((b1 'or' ('not' b2)) 'or' b3) '&' ((b1 'or' ('not' b3)) 'or' b2)
proof
let c1, c2, c3 be boolean set ;
thus c1 'or' (c2 'eqv' c3) = c1 'or' ((c2 'imp' c3) '&' (c3 'imp' c2)) by BINARI_5:23
.= (c1 'or' (c2 'imp' c3)) '&' (c1 'or' (c3 'imp' c2)) by BINARITH:23
.= ((c1 'or' ('not' c2)) 'or' c3) '&' (c1 'or' (c3 'imp' c2)) by BINARITH:20
.= ((c1 'or' ('not' c2)) 'or' c3) '&' ((c1 'or' ('not' c3)) 'or' c2) by BINARITH:20 ;
end;

theorem E10: :: BINARI_6:23
for b1, b2, b3 being boolean set holds b1 'or' (b2 'nand' b3) = (b1 'or' ('not' b2)) 'or' ('not' b3)
proof
let c1, c2, c3 be boolean set ;
thus c1 'or' (c2 'nand' c3) = c1 'or' (('not' c2) 'or' ('not' c3)) by BINARITH:9
.= (c1 'or' ('not' c2)) 'or' ('not' c3) by BINARITH:20 ;
end;

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

theorem :: BINARI_6:25
for b1, b2 being boolean set holds b1 'or' (b1 'or' b2) = b1 'or' b2
proof
let c1, c2 be boolean set ;
thus c1 'or' (c1 'or' c2) = (c1 'or' c1) 'or' c2 by BINARITH:20
.= c1 'or' c2 by BINARITH:21 ;
end;

theorem :: BINARI_6:26
for b1, b2 being boolean set holds b1 'or' (b1 'imp' b2) = TRUE
proof
let c1, c2 be boolean set ;
thus c1 'or' (c1 'imp' c2) = (c1 'or' ('not' c1)) 'or' c2 by BINARITH:20
.= TRUE 'or' c2 by BINARITH:18
.= TRUE by BINARITH:19 ;
end;

theorem :: BINARI_6:27
for b1, b2 being boolean set holds b1 'or' (b1 'eqv' b2) = b2 'imp' b1
proof
let c1, c2 be boolean set ;
c1 'or' (c1 'eqv' c2) = ((c1 'or' ('not' c1)) 'or' c2) '&' ((c1 'or' ('not' c2)) 'or' c1) by E9
.= (TRUE 'or' c2) '&' ((c1 'or' ('not' c2)) 'or' c1) by BINARITH:18
.= TRUE '&' ((c1 'or' ('not' c2)) 'or' c1) by BINARITH:19
.= (c1 'or' ('not' c2)) 'or' c1 by MARGREL1:50
.= ('not' c2) 'or' (c1 'or' c1) by BINARITH:20
.= ('not' c2) 'or' c1 by BINARITH:21 ;
hence c1 'or' (c1 'eqv' c2) = c2 'imp' c1 ;
end;

theorem :: BINARI_6:28
for b1, b2 being boolean set holds b1 'or' (b1 'nand' b2) = TRUE
proof
let c1, c2 be boolean set ;
thus c1 'or' (c1 'nand' c2) = (c1 'or' ('not' c1)) 'or' ('not' c2) by E10
.= TRUE 'or' ('not' c2) by BINARITH:18
.= TRUE by BINARITH:19 ;
end;

theorem :: BINARI_6:29
for b1, b2 being boolean set holds b1 'or' (b1 'nor' b2) = b2 'imp' b1
proof
let c1, c2 be boolean set ;
c1 'or' (c1 'nor' c2) = (c1 'or' ('not' c1)) '&' (c1 'or' ('not' c2)) by E11
.= TRUE '&' (c1 'or' ('not' c2)) by BINARITH:18
.= c1 'or' ('not' c2) by MARGREL1:50 ;
hence c1 'or' (c1 'nor' c2) = c2 'imp' c1 ;
end;

theorem E12: :: BINARI_6:30
for b1, b2, b3 being boolean set holds b1 'imp' (b2 'xor' b3) = (('not' b1) 'or' (('not' b2) '&' b3)) 'or' (b2 '&' ('not' b3))
proof
let c1, c2, c3 be boolean set ;
thus c1 'imp' (c2 'xor' c3) = ('not' c1) 'or' ((('not' c2) '&' c3) 'or' (c2 '&' ('not' c3))) by BINARITH:def 2
.= (('not' c1) 'or' (('not' c2) '&' c3)) 'or' (c2 '&' ('not' c3)) by BINARITH:20 ;
end;

theorem E13: :: BINARI_6:31
for b1, b2, b3 being boolean set holds b1 'imp' (b2 'eqv' b3) = ((('not' b1) 'or' ('not' b2)) 'or' b3) '&' ((('not' b1) 'or' b2) 'or' ('not' b3))
proof
let c1, c2, c3 be boolean set ;
thus c1 'imp' (c2 'eqv' c3) = ('not' c1) 'or' ((c2 'imp' c3) '&' (c3 'imp' c2)) by BINARI_5:23
.= (('not' c1) 'or' (('not' c2) 'or' c3)) '&' (('not' c1) 'or' (('not' c3) 'or' c2)) by BINARITH:23
.= ((('not' c1) 'or' ('not' c2)) 'or' c3) '&' (('not' c1) 'or' (('not' c3) 'or' c2)) by BINARITH:20
.= ((('not' c1) 'or' ('not' c2)) 'or' c3) '&' ((('not' c1) 'or' c2) 'or' ('not' c3)) by BINARITH:20 ;
end;

theorem E14: :: BINARI_6:32
for b1, b2, b3 being boolean set holds b1 'imp' (b2 'nand' b3) = (('not' b1) 'or' ('not' b2)) 'or' ('not' b3)
proof
let c1, c2, c3 be boolean set ;
thus c1 'imp' (c2 'nand' c3) = ('not' c1) 'or' (('not' c2) 'or' ('not' c3)) by BINARITH:9
.= (('not' c1) 'or' ('not' c2)) 'or' ('not' c3) by BINARITH:20 ;
end;

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

theorem E16: :: BINARI_6:34
for b1, b2 being boolean set holds b1 'imp' (b1 '&' b2) = b1 'imp' b2
proof
let c1, c2 be boolean set ;
c1 'imp' (c1 '&' c2) = (('not' c1) 'or' c1) '&' (('not' c1) 'or' c2) by BINARITH:23
.= TRUE '&' (('not' c1) 'or' c2) by BINARITH:18
.= ('not' c1) 'or' c2 by MARGREL1:50 ;
hence c1 'imp' (c1 '&' c2) = c1 'imp' c2 ;
end;

theorem :: BINARI_6:35
for b1, b2 being boolean set holds b1 'imp' (b1 'or' b2) = TRUE
proof
let c1, c2 be boolean set ;
thus c1 'imp' (c1 'or' c2) = (('not' c1) 'or' c1) 'or' c2 by BINARITH:20
.= TRUE 'or' c2 by BINARITH:18
.= TRUE by BINARITH:19 ;
end;

theorem :: BINARI_6:36
for b1, b2 being boolean set holds b1 'imp' (b1 'xor' b2) = ('not' b1) 'or' ('not' b2)
proof
let c1, c2 be boolean set ;
thus c1 'imp' (c1 'xor' c2) = (('not' c1) 'or' (c1 '&' ('not' c2))) 'or' (('not' c1) '&' c2) by E12
.= ((('not' c1) 'or' c1) '&' (('not' c1) 'or' ('not' c2))) 'or' (('not' c1) '&' c2) by BINARITH:23
.= (TRUE '&' (('not' c1) 'or' ('not' c2))) 'or' (('not' c1) '&' c2) by BINARITH:18
.= (('not' c1) 'or' ('not' c2)) 'or' (('not' c1) '&' c2) by MARGREL1:50
.= ('not' c1) 'or' (('not' c2) 'or' (('not' c1) '&' c2)) by BINARITH:20
.= ('not' c1) 'or' ((('not' c2) 'or' ('not' c1)) '&' (('not' c2) 'or' c2)) by BINARITH:23
.= ('not' c1) 'or' ((('not' c2) 'or' ('not' c1)) '&' TRUE ) by BINARITH:18
.= ('not' c1) 'or' (('not' c1) 'or' ('not' c2)) by MARGREL1:50
.= (('not' c1) 'or' ('not' c1)) 'or' ('not' c2) by BINARITH:20
.= ('not' c1) 'or' ('not' c2) by BINARITH:21 ;
end;

theorem E17: :: BINARI_6:37
for b1, b2 being boolean set holds b1 'imp' (b1 'imp' b2) = b1 'imp' b2
proof
let c1, c2 be boolean set ;
c1 'imp' (c1 'imp' c2) = (('not' c1) 'or' ('not' c1)) 'or' c2 by BINARITH:20
.= ('not' c1) 'or' c2 by BINARITH:21 ;
hence c1 'imp' (c1 'imp' c2) = c1 'imp' c2 ;
end;

theorem :: BINARI_6:38
for b1, b2 being boolean set holds
( b1 'imp' (b1 'eqv' b2) = b1 'imp' b2 & b1 'imp' (b1 'eqv' b2) = b1 'imp' (b1 'imp' b2) )
proof
let c1, c2 be boolean set ;
c1 'imp' (c1 'eqv' c2) = ((('not' c1) 'or' ('not' c1)) 'or' c2) '&' ((('not' c1) 'or' c1) 'or' ('not' c2)) by E13
.= (('not' c1) 'or' c2) '&' ((('not' c1) 'or' c1) 'or' ('not' c2)) by BINARITH:21
.= (('not' c1) 'or' c2) '&' (TRUE 'or' ('not' c2)) by BINARITH:18
.= (('not' c1) 'or' c2) '&' TRUE by BINARITH:19
.= ('not' c1) 'or' c2 by MARGREL1:50 ;
hence ( c1 'imp' (c1 'eqv' c2) = c1 'imp' c2 & c1 'imp' (c1 'eqv' c2) = c1 'imp' (c1 'imp' c2) ) by E17;
end;

theorem :: BINARI_6:39
for b1, b2 being boolean set holds b1 'imp' (b1 'nand' b2) = 'not' (b1 '&' b2)
proof
let c1, c2 be boolean set ;
c1 'imp' (c1 'nand' c2) = (('not' c1) 'or' ('not' c1)) 'or' ('not' c2) by E14
.= ('not' c1) 'or' ('not' c2) by BINARITH:21 ;
hence c1 'imp' (c1 'nand' c2) = 'not' (c1 '&' c2) by BINARITH:9;
end;

theorem :: BINARI_6:40
for b1, b2 being boolean set holds b1 'imp' (b1 'nor' b2) = 'not' b1
proof
let c1, c2 be boolean set ;
thus c1 'imp' (c1 'nor' c2) = (('not' c1) 'or' ('not' c1)) '&' (('not' c1) 'or' ('not' c2)) by E15
.= ('not' c1) '&' (('not' c1) 'or' ('not' c2)) by BINARITH:21
.= 'not' c1 by BINARITH:25 ;
end;

theorem E18: :: BINARI_6:41
for b1, b2, b3 being boolean set holds
( b1 'nand' (b2 'imp' b3) = (('not' b1) 'or' b2) '&' (('not' b1) 'or' ('not' b3)) & b1 'nand' (b2 'imp' b3) = (b1 'imp' b2) '&' (b1 'imp' ('not' b3)) )
proof
let c1, c2, c3 be boolean set ;
c1 'nand' (c2 'imp' c3) = ('not' c1) 'or' ('not' (('not' c2) 'or' c3)) by BINARITH:9
.= ('not' c1) 'or' (('not' ('not' c2)) '&' ('not' c3)) by BINARITH:10
.= ('not' c1) 'or' (c2 '&' ('not' c3)) by MARGREL1:40
.= (('not' c1) 'or' c2) '&' (('not' c1) 'or' ('not' c3)) by BINARITH:23 ;
hence ( c1 'nand' (c2 'imp' c3) = (('not' c1) 'or' c2) '&' (('not' c1) 'or' ('not' c3)) & c1 'nand' (c2 'imp' c3) = (c1 'imp' c2) '&' (c1 'imp' ('not' c3)) ) ;
end;

theorem E19: :: BINARI_6:42
for b1, b2, b3 being boolean set holds b1 'nand' (b2 'eqv' b3) = 'not' ((b1 '&' (('not' b2) 'or' b3)) '&' (('not' b3) 'or' b2))
proof
let c1, c2, c3 be boolean set ;
thus c1 'nand' (c2 'eqv' c3) = 'not' (c1 '&' ((c2 'imp' c3) '&' (c3 'imp' c2))) by BINARI_5:23
.= 'not' ((c1 '&' (('not' c2) 'or' c3)) '&' (('not' c3) 'or' c2)) by MARGREL1:52 ;
end;

theorem E20: :: BINARI_6:43
for b1, b2, b3 being boolean set holds
( b1 'nand' (b2 'nand' b3) = (('not' b1) 'or' b2) '&' (('not' b1) 'or' b3) & b1 'nand' (b2 'nand' b3) = (b1 'imp' b2) '&' (b1 'imp' b3) )
proof
let c1, c2, c3 be boolean set ;
c1 'nand' (c2 'nand' c3) = ('not' c1) 'or' ('not' ('not' (c2 '&' c3))) by BINARITH:9
.= ('not' c1) 'or' (c2 '&' c3) by MARGREL1:40
.= (('not' c1) 'or' c2) '&' (('not' c1) 'or' c3) by BINARITH:23 ;
hence ( c1 'nand' (c2 'nand' c3) = (('not' c1) 'or' c2) '&' (('not' c1) 'or' c3) & c1 'nand' (c2 'nand' c3) = (c1 'imp' c2) '&' (c1 'imp' c3) ) ;
end;

theorem E21: :: BINARI_6:44
for b1, b2, b3 being boolean set holds b1 'nand' (b2 'nor' b3) = (('not' b1) 'or' b2) 'or' b3
proof
let c1, c2, c3 be boolean set ;
thus c1 'nand' (c2 'nor' c3) = ('not' c1) 'or' ('not' ('not' (c2 'or' c3))) by BINARITH:9
.= ('not' c1) 'or' (c2 'or' c3) by MARGREL1:40
.= (('not' c1) 'or' c2) 'or' c3 by BINARITH:20 ;
end;

theorem :: BINARI_6:45
for b1, b2 being boolean set holds b1 'nand' (b1 '&' b2) = 'not' (b1 '&' b2)
proof
let c1, c2 be boolean set ;
thus c1 'nand' (c1 '&' c2) = 'not' ((c1 '&' c1) '&' c2) by BINARI_5:6
.= 'not' (c1 '&' c2) by BINARITH:16 ;
end;

theorem :: BINARI_6:46
for b1, b2 being boolean set holds b1 'nand' (b1 'xor' b2) = b1 'imp' b2
proof
let c1, c2 be boolean set ;
c1 'nand' (c1 'xor' c2) = (c1 '&' c1) 'eqv' (c1 '&' c2) by BINARI_5:9
.= c1 'eqv' (c1 '&' c2) by BINARITH:16
.= (c1 'imp' (c1 '&' c2)) '&' ((c1 '&' c2) 'imp' c1) by BINARI_5:23
.= (c1 'imp' c2) '&' ((c1 '&' c2) 'imp' c1) by E16
.= (('not' c1) 'or' c2) '&' ((('not' c1) 'or' ('not' c2)) 'or' c1) by BINARITH:9
.= (('not' c1) 'or' c2) '&' (('not' c2) 'or' (('not' c1) 'or' c1)) by BINARITH:20
.= (('not' c1) 'or' c2) '&' (('not' c2) 'or' TRUE ) by BINARITH:18
.= (('not' c1) 'or' c2) '&' TRUE by BINARITH:19
.= ('not' c1) 'or' c2 by MARGREL1:50 ;
hence c1 'nand' (c1 'xor' c2) = c1 'imp' c2 ;
end;

theorem :: BINARI_6:47
for b1, b2 being boolean set holds b1 'nand' (b1 'imp' b2) = 'not' (b1 '&' b2)
proof
let c1, c2 be boolean set ;
thus c1 'nand' (c1 'imp' c2) = (('not' c1) 'or' c1) '&' ((