thus xor2 . <*0,0*> =
FALSE 'xor' FALSE
by FACIRC_1:def 4
.=
0
; ( xor2 . <*0,1*> = 1 & xor2 . <*1,0*> = 1 & xor2 . <*1,1*> = 0 & xor2a . <*0,0*> = 1 & xor2a . <*0,1*> = 0 & xor2a . <*1,0*> = 0 & xor2a . <*1,1*> = 1 )
thus xor2 . <*0,1*> =
FALSE 'xor' TRUE
by FACIRC_1:def 4
.=
1
; ( xor2 . <*1,0*> = 1 & xor2 . <*1,1*> = 0 & xor2a . <*0,0*> = 1 & xor2a . <*0,1*> = 0 & xor2a . <*1,0*> = 0 & xor2a . <*1,1*> = 1 )
thus xor2 . <*1,0*> =
TRUE 'xor' FALSE
by FACIRC_1:def 4
.=
1
; ( xor2 . <*1,1*> = 0 & xor2a . <*0,0*> = 1 & xor2a . <*0,1*> = 0 & xor2a . <*1,0*> = 0 & xor2a . <*1,1*> = 1 )
thus xor2 . <*1,1*> =
TRUE 'xor' TRUE
by FACIRC_1:def 4
.=
0
; ( xor2a . <*0,0*> = 1 & xor2a . <*0,1*> = 0 & xor2a . <*1,0*> = 0 & xor2a . <*1,1*> = 1 )
thus xor2a . <*0,0*> =
('not' FALSE) 'xor' FALSE
by Def7
.=
1
; ( xor2a . <*0,1*> = 0 & xor2a . <*1,0*> = 0 & xor2a . <*1,1*> = 1 )
thus xor2a . <*0,1*> =
('not' FALSE) 'xor' TRUE
by Def7
.=
0
; ( xor2a . <*1,0*> = 0 & xor2a . <*1,1*> = 1 )
thus xor2a . <*1,0*> =
('not' TRUE) 'xor' FALSE
by Def7
.=
0
; xor2a . <*1,1*> = 1
thus xor2a . <*1,1*> =
('not' TRUE) 'xor' TRUE
by Def7
.=
1
; verum