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