:: BINARITH semantic presentation

definition
let c1 be Nat;
let c2 be non empty set ;
mode Tuple is Element of a1 -tuples_on a2;
end;

E1: for b1, b2 being Nat holds addnat . b1,b2 = b1 + b2
by BINOP_2:def 23;

theorem :: BINARITH:1
canceled;

theorem E2: :: BINARITH:2
for b1, b2 being Nat
for b3 being non empty set
for b4 being Element of b3
for b5 being Tuple of b2,b3 holds
( b1 in Seg b2 implies (b5 ^ <*b4*>) /. b1 = b5 /. b1 )
proof
let c1, c2 be Nat;
let c3 be non empty set ;
let c4 be Element of c3;
let c5 be Tuple of c2,c3;
assume E3: c1 in Seg c2 ;
len c5 = c2 by FINSEQ_2:109;
then c1 in dom c5 by E3, FINSEQ_1:def 3;
hence (c5 ^ <*c4*>) /. c1 = c5 /. c1 by FINSEQ_4:83;
end;

theorem E3: :: BINARITH:3
for b1 being Nat
for b2 being non empty set
for b3 being Element of b2
for b4 being Tuple of b1,b2 holds (b4 ^ <*b3*>) /. (b1 + 1) = b3
proof
let c1 be Nat;
let c2 be non empty set ;
let c3 be Element of c2;
let c4 be Tuple of c1,c2;
len <*c3*> = 1 by FINSEQ_1:56;
then 0 + 1 in Seg (len <*c3*>) ;
then E4: 0 + 1 in dom <*c3*> by FINSEQ_1:def 3;
len c4 = c1 by FINSEQ_2:109;
hence (c4 ^ <*c3*>) /. (c1 + 1) = <*c3*> /. 1 by E4, FINSEQ_4:84
.= c3 by FINSEQ_4:25 ;

end;

theorem :: BINARITH:4
canceled;

theorem :: BINARITH:5
for b1, b2 being Nat holds
not ( b1 in Seg b2 & b1 is empty ) by CARD_1:51, FINSEQ_1:3;

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

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

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

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

registration
let c1, c2 be boolean set ;
cluster a1 'or' a2 -> boolean ;
correctness
coherence
c1 'or' c2 is boolean;
proof
c1 'or' c2 = 'not' (('not' c1) '&' ('not' c2)) ;
hence c1 'or' c2 is boolean ;
end;
end;

registration
let c1, c2 be boolean set ;
cluster a1 'xor' a2 -> boolean ;
correctness
coherence
c1 'xor' c2 is boolean;
proof
c1 'xor' c2 = (('not' c1) '&' c2) 'or' (c1 '&' ('not' c2)) ;
hence c1 'xor' c2 is boolean ;
end;
end;

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

theorem :: BINARITH:6
canceled;

theorem E4: :: BINARITH:7
for b1 being boolean set holds b1 'or' FALSE = b1
proof
let c1 be boolean set ;
thus c1 'or' FALSE = 'not' (('not' c1) '&' ('not' FALSE ))
.= 'not' (TRUE '&' ('not' c1)) by MARGREL1:41
.= 'not' ('not' c1) by MARGREL1:50
.= c1 by MARGREL1:40 ;
end;

theorem :: BINARITH:8
canceled;

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

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

theorem :: BINARITH:11
canceled;

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

theorem :: BINARITH:13
for b1 being boolean set holds TRUE 'xor' b1 = 'not' b1
proof
let c1 be boolean set ;
thus TRUE 'xor' c1 = (('not' TRUE ) '&' c1) 'or' (TRUE '&' ('not' c1))
.= (FALSE '&' c1) 'or' (TRUE '&' ('not' c1)) by MARGREL1:def 16
.= FALSE 'or' (TRUE '&' ('not' c1)) by MARGREL1:49
.= FALSE 'or' ('not' c1) by MARGREL1:50
.= 'not' c1 by E4 ;
end;

theorem :: BINARITH:14
for b1 being boolean set holds FALSE 'xor' b1 = b1
proof
let c1 be boolean set ;
thus FALSE 'xor' c1 = (('not' FALSE ) '&' c1) 'or' (FALSE '&' ('not' c1))
.= (TRUE '&' c1) 'or' (FALSE '&' ('not' c1)) by MARGREL1:def 16
.= c1 'or' (FALSE '&' ('not' c1)) by MARGREL1:50
.= c1 'or' FALSE by MARGREL1:49
.= c1 by E4 ;
end;

theorem E7: :: BINARITH:15
for b1 being boolean set holds b1 'xor' b1 = FALSE
proof
let c1 be boolean set ;
thus c1 'xor' c1 = (('not' c1) '&' c1) 'or' (c1 '&' ('not' c1))
.= (c1 '&' ('not' c1)) 'or' FALSE by MARGREL1:46
.= FALSE 'or' FALSE by MARGREL1:46
.= FALSE by E4 ;
end;

theorem E8: :: BINARITH:16
for b1 being boolean set holds b1 '&' b1 = b1
proof
let c1 be boolean set ;
per cases ( c1 = TRUE or c1 = FALSE ) by MARGREL1:39;
suppose c1 = TRUE ;
hence c1 '&' c1 = c1 by MARGREL1:45;
end;
suppose c1 = FALSE ;
hence c1 '&' c1 = c1 by MARGREL1:45;
end;
end;
end;

theorem E9: :: BINARITH:17
for b1 being boolean set holds b1 'xor' ('not' b1) = TRUE
proof
let c1 be boolean set ;
thus c1 'xor' ('not' c1) = (('not' c1) '&' ('not' c1)) 'or' (c1 '&' ('not' ('not' c1)))
.= (('not' c1) '&' ('not' c1)) 'or' (c1 '&' c1) by MARGREL1:40
.= ('not' c1) 'or' (c1 '&' c1) by E8
.= ('not' c1) 'or' c1 by E8
.= 'not' (('not' ('not' c1)) '&' ('not' c1))
.= TRUE by MARGREL1:47 ;
end;

theorem E10: :: BINARITH:18
for b1 being boolean set holds b1 'or' ('not' b1) = TRUE
proof
let c1 be boolean set ;
thus c1 'or' ('not' c1) = 'not' (('not' c1) '&' ('not' ('not' c1)))
.= TRUE by MARGREL1:47 ;
end;

theorem E11: :: BINARITH:19
for b1 being boolean set holds b1 'or' TRUE = TRUE
proof
let c1 be boolean set ;
thus c1 'or' TRUE = 'not' (('not' c1) '&' ('not' TRUE ))
.= 'not' (FALSE '&' ('not' c1)) by MARGREL1:def 16
.= 'not' FALSE by MARGREL1:49
.= TRUE by MARGREL1:def 16 ;
end;

theorem E12: :: BINARITH:20
for b1, b2, b3 being boolean set holds (b1 'or' b2) 'or' b3 = b1 'or' (b2 'or' b3)
proof
let c1, c2, c3 be boolean set ;
thus (c1 'or' c2) 'or' c3 = ('not' (('not' c1) '&' ('not' c2))) 'or' c3
.= 'not' (('not' ('not' (('not' c1) '&' ('not' c2)))) '&' ('not' c3))
.= 'not' ((('not' c1) '&' ('not' c2)) '&' ('not' c3)) by MARGREL1:40
.= 'not' (('not' c1) '&' (('not' c2) '&' ('not' c3))) by MARGREL1:52
.= 'not' (('not' c1) '&' ('not' ('not' (('not' c2) '&' ('not' c3))))) by MARGREL1:40
.= c1 'or' ('not' (('not' c2) '&' ('not' c3)))
.= c1 'or' (c2 'or' c3) ;
end;

theorem E13: :: BINARITH:21
for b1 being boolean set holds b1 'or' b1 = b1
proof
let c1 be boolean set ;
per cases ( c1 = TRUE or c1 = FALSE ) by MARGREL1:39;
suppose c1 = TRUE ;
hence c1 'or' c1 = c1 by E11;
end;
suppose c1 = FALSE ;
hence c1 'or' c1 = c1 by E4;
end;
end;
end;

theorem E14: :: BINARITH:22
for b1, b2, b3 being boolean set holds b1 '&' (b2 'or' b3) = (b1 '&' b2) 'or' (b1 '&' b3)
proof
let c1, c2, c3 be boolean set ;
per cases ( c1 = TRUE or c1 = FALSE ) by MARGREL1:39;
suppose E15: c1 = TRUE ;
hence c1 '&' (c2 'or' c3) = c2 'or' c3 by MARGREL1:50
.= (c1 '&' c2) 'or' c3 by E15, MARGREL1:50
.= (c1 '&' c2) 'or' (c1 '&' c3) by E15, MARGREL1:50 ;

end;
suppose E15: c1 = FALSE ;
hence c1 '&' (c2 'or' c3) = c1 by MARGREL1:49
.= c1 'or' c1 by E15, E4
.= (c1 '&' c2) 'or' c1 by E15, MARGREL1:49
.= (c1 '&' c2) 'or' (c1 '&' c3) by E15, MARGREL1:49 ;

end;
end;
end;

theorem E15: :: BINARITH:23
for b1, b2, b3 being boolean set holds b1 'or' (b2 '&' b3) = (b1 'or' b2) '&' (b1 'or' b3)
proof
let c1, c2, c3 be boolean set ;
per cases ( c1 = TRUE or c1 = FALSE ) by MARGREL1:39;
suppose E16: c1 = TRUE ;
hence c1 'or' (c2 '&' c3) = c1 by E11
.= c1 '&' c1 by E8
.= (c1 'or' c2) '&' c1 by E16, E11
.= (c1 'or' c2) '&' (c1 'or' c3) by E16, E11 ;

end;
suppose E16: c1 = FALSE ;
hence c1 'or' (c2 '&' c3) = c2 '&' c3 by E4
.= (c1 'or' c2) '&' c3 by E16, E4
.= (c1 'or' c2) '&' (c1 'or' c3) by E16, E4 ;

end;
end;
end;

theorem :: BINARITH:24
for b1, b2 being boolean set holds b1 'or' (b1 '&' b2) = b1
proof
let c1, c2 be boolean set ;
per cases ( c1 = TRUE or c1 = FALSE ) by MARGREL1:39;
suppose c1 = TRUE ;
hence c1 'or' (c1 '&' c2) = c1 by E11;
end;
suppose E16: c1 = FALSE ;
then c1 'or' (c1 '&' c2) = c1 '&' c2 by E4
.= c1 by E16, MARGREL1:49 ;
hence c1 'or' (c1 '&' c2) = c1 ;
end;
end;
end;

theorem E16: :: BINARITH:25
for b1, b2 being boolean set holds b1 '&' (b1 'or' b2) = b1
proof
let c1, c2 be boolean set ;
per cases ( c1 = TRUE or c1 = FALSE ) by MARGREL1:39;
suppose E17: c1 = TRUE ;
then c1 '&' (c1 'or' c2) = c1 '&' c1 by E11
.= c1 by E17, MARGREL1:50 ;
hence c1 '&' (c1 'or' c2) = c1 ;
end;
suppose c1 = FALSE ;
hence c1 '&' (c1 'or' c2) = c1 by MARGREL1:49;
end;
end;
end;

theorem E17: :: BINARITH:26
for b1, b2 being boolean set holds b1 'or' (('not' b1) '&' b2) = b1 'or' b2
proof
let c1, c2 be boolean set ;
per cases ( c1 = TRUE or c1 = FALSE ) by MARGREL1:39;
suppose E18: c1 = TRUE ;
then c1 'or' (('not' c1) '&' c2) = c1 'or' (FALSE '&' c2) by MARGREL1:def 16
.= c1 'or' FALSE by MARGREL1:49
.= c1 by E4
.= c1 'or' c2 by E18, E11 ;
hence c1 'or' (('not' c1) '&' c2) = c1 'or' c2 ;
end;
suppose c1 = FALSE ;
then c1 'or' (('not' c1) '&' c2) = c1 'or' (TRUE '&' c2) by MARGREL1:def 16
.= c1 'or' c2 by MARGREL1:50 ;
hence c1 'or' (('not' c1) '&' c2) = c1 'or' c2 ;
end;
end;
end;

theorem :: BINARITH:27
for b1, b2 being boolean set holds b1 '&' (('not' b1) 'or' b2) = b1 '&' b2
proof
let c1, c2 be boolean set ;
per cases ( c1 = TRUE or c1 = FALSE ) by MARGREL1:39;
suppose c1 = TRUE ;
then c1 '&' (('not' c1) 'or' c2) = c1 '&' (FALSE 'or' c2) by MARGREL1:def 16
.= c1 '&' c2 by E4 ;
hence c1 '&' (('not' c1) 'or' c2) = c1 '&' c2 ;
end;
suppose E18: c1 = FALSE ;
then c1 '&' (('not' c1) 'or' c2) = c1 by MARGREL1:49
.= c1 '&' c2 by E18, MARGREL1:49 ;
hence c1 '&' (('not' c1) 'or' c2) = c1 '&' c2 ;
end;
end;
end;

theorem :: BINARITH:28
canceled;

theorem :: BINARITH:29
canceled;

theorem :: BINARITH:30
canceled;

theorem :: BINARITH:31
canceled;

theorem :: BINARITH:32
canceled;

theorem E18: :: BINARITH:33
TRUE 'xor' FALSE = TRUE
proof
thus TRUE 'xor' FALSE = TRUE 'xor' ('not' TRUE ) by MARGREL1:41
.= TRUE by E9 ;
end;

theorem E19: :: BINARITH:34
for b1, b2, b3 being boolean set holds (b1 'xor' b2) 'xor' b3 = b1 'xor' (b2 'xor' b3)
proof
let c1, c2, c3 be boolean set ;
E20: (c1 'xor' c2) 'xor' c3 = ((('not' c1) '&' c2) 'or' (c1 '&' ('not' c2))) 'xor' c3
.= (('not' ((('not' c1) '&' c2) 'or' (c1 '&' ('not' c2)))) '&' c3) 'or' (((('not' c1) '&' c2) 'or' (c1 '&' ('not' c2))) '&' ('not' c3))
.= ((('not' (('not' c1) '&' c2)) '&' ('not' (c1 '&' ('not' c2)))) '&' c3) 'or' (((('not' c1) '&' c2) 'or' (c1 '&' ('not' c2))) '&' ('not' c3)) by E6 ;
E21: 'not' (('not' c1) '&' c2) = ('not' ('not' c1)) 'or' ('not' c2) by E5
.= c1 'or' ('not' c2) by MARGREL1:40 ;
'not' (c1 '&' ('not' c2)) = ('not' c1) 'or' ('not' ('not' c2)) by E5
.= ('not' c1) 'or' c2 by MARGREL1:40 ;
then E22: (('not' (('not' c1) '&' c2)) '&' ('not' (c1 '&' ('not' c2)))) '&' c3 = (c1 'or' ('not' c2)) '&' (c3 '&' (('not' c1) 'or' c2)) by E21, MARGREL1:52
.= (c1 'or' ('not' c2)) '&' ((c3 '&' ('not' c1)) 'or' (c3 '&' c2)) by E14
.= ((c1 'or' ('not' c2)) '&' (c3 '&' ('not' c1))) 'or' ((c1 'or' ('not' c2)) '&' (c3 '&' c2)) by E14 ;
E23: (c1 'or' ('not' c2)) '&' (c3 '&' ('not' c1)) = ((c3 '&' ('not' c1)) '&' c1) 'or' ((c3 '&' ('not' c1)) '&' ('not' c2)) by E14
.= (c3 '&' (('not' c1) '&' c1)) 'or' ((c3 '&' ('not' c1)) '&' ('not' c2)) by MARGREL1:52
.= (c3 '&' FALSE ) 'or' ((c3 '&' ('not' c1)) '&' ('not' c2)) by MARGREL1:46
.= FALSE 'or' ((c3 '&' ('not' c1)) '&' ('not' c2)) by MARGREL1:49
.= (c3 '&' ('not' c1)) '&' ('not' c2) by E4 ;
E24: (c1 'or' ('not' c2)) '&' (c3 '&' c2) = ((c3 '&' c2) '&' c1) 'or' ((c3 '&' c2) '&' ('not' c2)) by E14
.= ((c3 '&' c2) '&' c1) 'or' (c3 '&' (c2 '&' ('not' c2))) by MARGREL1:52
.= ((c3 '&' c2) '&' c1) 'or' (c3 '&' FALSE ) by MARGREL1:46
.= ((c3 '&' c2) '&' c1) 'or' FALSE by MARGREL1:49
.= (c3 '&' c2) '&' c1 by E4 ;
((('not' c1) '&' c2) 'or' (c1 '&' ('not' c2))) '&' ('not' c3) = (('not' c3) '&' (('not' c1) '&' c2)) 'or' (('not' c3) '&' (c1 '&' ('not' c2))) by E14
.= ((('not' c3) '&' ('not' c1)) '&' c2) 'or' (('not' c3) '&' (c1 '&' ('not' c2))) by MARGREL1:52
.= ((('not' c3) '&' ('not' c1)) '&' c2) 'or' ((('not' c3) '&' c1) '&' ('not' c2)) by MARGREL1:52 ;
then E25: (c1 'xor' c2) 'xor' c3 = (((c3 '&' c2) '&' c1) 'or' (((('not' c3) '&' ('not' c1)) '&' c2) 'or' ((('not' c3) '&' c1) '&' ('not' c2)))) 'or' ((c3 '&' ('not' c1)) '&' ('not' c2)) by E20, E22, E23, E24, E12
.= ((((c3 '&' c2) '&' c1) 'or' ((('not' c3) '&' c1) '&' ('not' c2))) 'or' ((('not' c3) '&' ('not' c1)) '&' c2)) 'or' ((c3 '&' ('not' c1)) '&' ('not' c2)) by E12
.= ((((c1 '&' c2) '&' c3) 'or' ((('not' c3) '&' c1) '&' ('not' c2))) 'or' ((('not' c3) '&' ('not' c1)) '&' c2)) 'or' ((c3 '&' ('not' c1)) '&' ('not' c2)) by MARGREL1:52
.= ((((c1 '&' c2) '&' c3) 'or' ((c1 '&' ('not' c2)) '&' ('not' c3))) 'or' ((('not' c3) '&' ('not' c1)) '&' c2)) 'or' ((c3 '&' ('not' c1)) '&' ('not' c2)) by MARGREL1:52
.= ((((c1 '&' c2) '&' c3) 'or' ((c1 '&' ('not' c2)) '&' ('not' c3))) 'or' ((('not' c1) '&' c2) '&' ('not' c3))) 'or' ((c3 '&' ('not' c1)) '&' ('not' c2)) by MARGREL1:52
.= ((((c1 '&' c2) '&' c3) 'or' ((c1 '&' ('not' c2)) '&' ('not' c3))) 'or' ((('not' c1) '&' c2) '&' ('not' c3))) 'or' ((('not' c1) '&' ('not' c2)) '&' c3) by MARGREL1:52 ;
E26: c1 'xor' (c2 'xor' c3) = c1 'xor' ((('not' c2) '&' c3) 'or' (c2 '&' ('not' c3)))
.= (('not' c1) '&' ((('not' c2) '&' c3) 'or' (c2 '&' ('not' c3)))) 'or' (c1 '&' ('not' ((('not' c2) '&' c3) 'or' (c2 '&' ('not' c3)))))
.= (('not' c1) '&' ((('not' c2) '&' c3) 'or' (c2 '&' ('not' c3)))) 'or' (c1 '&' (('not' (('not' c2) '&' c3)) '&' ('not' (c2 '&' ('not' c3))))) by E6
.= (('not' c1) '&' ((('not' c2) '&' c3) 'or' (c2 '&' ('not' c3)))) 'or' ((c1 '&' ('not' (('not' c2) '&' c3))) '&' ('not' (c2 '&' ('not' c3)))) by MARGREL1:52 ;
E27: ('not' c1) '&' ((('not' c2) '&' c3) 'or' (c2 '&' ('not' c3))) = (('not' c1) '&' (('not' c2) '&' c3)) 'or' (('not' c1) '&' (c2 '&' ('not' c3))) by E14
.= ((('not' c1) '&' ('not' c2)) '&' c3) 'or' (('not' c1) '&' (c2 '&' ('not' c3))) by MARGREL1:52
.= ((('not' c1) '&' ('not' c2)) '&' c3) 'or' ((('not' c1) '&' c2) '&' ('not' c3)) by MARGREL1:52 ;
E28: 'not' (('not' c2) '&' c3) = ('not' ('not' c2)) 'or' ('not' c3) by E5
.= c2 'or' ('not' c3) by MARGREL1:40 ;
'not' (c2 '&' ('not' c3)) = ('not' c2) 'or' ('not' ('not' c3)) by E5
.= ('not' c2) 'or' c3 by MARGREL1:40 ;
then E29: (c1 '&' ('not' (('not' c2) '&' c3))) '&' ('not' (c2 '&' ('not' c3))) = (('not' c2) 'or' c3) '&' ((c1 '&' c2) 'or' (c1 '&' ('not' c3))) by E28, E14
.= ((('not' c2) 'or' c3) '&' (c1 '&' c2)) 'or' ((('not' c2) 'or' c3) '&' (c1 '&' ('not' c3))) by E14 ;
E30: (('not' c2) 'or' c3) '&' (c1 '&' c2) = ((c1 '&' c2) '&' ('not' c2)) 'or' ((c1 '&' c2) '&' c3) by E14
.= (c1 '&' (c2 '&' ('not' c2))) 'or' ((c1 '&' c2) '&' c3) by MARGREL1:52
.= (c1 '&' FALSE ) 'or' ((c1 '&' c2) '&' c3) by MARGREL1:46
.= FALSE 'or' ((c1 '&' c2) '&' c3) by MARGREL1:49
.= (c1 '&' c2) '&' c3 by E4 ;
(('not' c2) 'or' c3) '&' (c1 '&' ('not' c3)) = ((c1 '&' ('not' c3)) '&' ('not' c2)) 'or' ((c1 '&' ('not' c3)) '&' c3) by E14
.= ((c1 '&' ('not' c3)) '&' ('not' c2)) 'or' (c1 '&' (('not' c3) '&' c3)) by MARGREL1:52
.= ((c1 '&' ('not' c3)) '&' ('not' c2)) 'or' (c1 '&' FALSE ) by MARGREL1:46
.= ((c1 '&' ('not' c3)) '&' ('not' c2)) 'or' FALSE by MARGREL1:49
.= (c1 '&' ('not' c3)) '&' ('not' c2) by E4 ;
then c1 'xor' (c2 'xor' c3) = ((((c1 '&' c2) '&' c3) 'or' ((c1 '&' ('not' c3)) '&' ('not' c2))) 'or' ((('not' c1) '&' c2) '&' ('not' c3))) 'or' ((('not' c1) '&' ('not' c2)) '&' c3) by E26, E27, E29, E30, E12
.= ((((c1 '&' c2) '&' c3) 'or' ((c1 '&' ('not' c2)) '&' ('not' c3))) 'or' ((('not' c1) '&' c2) '&' ('not' c3))) 'or' ((('not' c1) '&' ('not' c2)) '&' c3) by MARGREL1:52 ;
hence (c1 'xor' c2) 'xor' c3 = c1 'xor' (c2 'xor' c3) by E25;
end;

theorem :: BINARITH:35
for b1, b2 being boolean set holds b1 'xor' (('not' b1) '&' b2) = b1 'or' b2
proof
let c1, c2 be boolean set ;
thus c1 'xor' (('not' c1) '&' c2) = (('not' c1) '&' (('not' c1) '&' c2)) 'or' (c1 '&' ('not' (('not' c1) '&' c2)))
.= ((('not' c1) '&' ('not' c1)) '&' c2) 'or' (c1 '&' ('not' (('not' c1) '&' c2))) by MARGREL1:52
.