thus xor2 . <*0,0*> = FALSE 'xor' FALSE by FACIRC_1:def 4
.= 0 ; :: thesis: ( 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 ; :: thesis: ( 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 ; :: thesis: ( 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 ; :: thesis: ( 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 ; :: thesis: ( xor2a . <*0,1*> = 0 & xor2a . <*1,0*> = 0 & xor2a . <*1,1*> = 1 )
thus xor2a . <*0,1*> = ('not' FALSE) 'xor' TRUE by Def7
.= 0 ; :: thesis: ( xor2a . <*1,0*> = 0 & xor2a . <*1,1*> = 1 )
thus xor2a . <*1,0*> = ('not' TRUE) 'xor' FALSE by Def7
.= 0 ; :: thesis: xor2a . <*1,1*> = 1
thus xor2a . <*1,1*> = ('not' TRUE) 'xor' TRUE by Def7
.= 1 ; :: thesis: verum