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