thus xor3 . <*0 ,0 ,0 *> = FALSE 'xor' FALSE by Def32
.= 0 ; :: thesis: ( xor3 . <*0 ,0 ,1*> = 1 & xor3 . <*0 ,1,0 *> = 1 & xor3 . <*0 ,1,1*> = 0 & xor3 . <*1,0 ,0 *> = 1 & xor3 . <*1,0 ,1*> = 0 & xor3 . <*1,1,0 *> = 0 & xor3 . <*1,1,1*> = 1 )
thus xor3 . <*0 ,0 ,1*> = (FALSE 'xor' FALSE ) 'xor' TRUE by Def32
.= 1 ; :: thesis: ( xor3 . <*0 ,1,0 *> = 1 & xor3 . <*0 ,1,1*> = 0 & xor3 . <*1,0 ,0 *> = 1 & xor3 . <*1,0 ,1*> = 0 & xor3 . <*1,1,0 *> = 0 & xor3 . <*1,1,1*> = 1 )
thus xor3 . <*0 ,1,0 *> = 1 by Def32, BINARITH:33; :: thesis: ( xor3 . <*0 ,1,1*> = 0 & xor3 . <*1,0 ,0 *> = 1 & xor3 . <*1,0 ,1*> = 0 & xor3 . <*1,1,0 *> = 0 & xor3 . <*1,1,1*> = 1 )
thus xor3 . <*0 ,1,1*> = TRUE 'xor' TRUE by Def32, BINARITH:33
.= 0 ; :: thesis: ( xor3 . <*1,0 ,0 *> = 1 & xor3 . <*1,0 ,1*> = 0 & xor3 . <*1,1,0 *> = 0 & xor3 . <*1,1,1*> = 1 )
thus xor3 . <*1,0 ,0 *> = 1 by Def32, BINARITH:33; :: thesis: ( xor3 . <*1,0 ,1*> = 0 & xor3 . <*1,1,0 *> = 0 & xor3 . <*1,1,1*> = 1 )
thus xor3 . <*1,0 ,1*> = TRUE 'xor' TRUE by Def32, BINARITH:33
.= 0 ; :: thesis: ( xor3 . <*1,1,0 *> = 0 & xor3 . <*1,1,1*> = 1 )
thus xor3 . <*1,1,0 *> = (TRUE 'xor' TRUE ) 'xor' FALSE by Def32
.= 0 ; :: thesis: xor3 . <*1,1,1*> = 1
thus xor3 . <*1,1,1*> = (TRUE 'xor' TRUE ) 'xor' TRUE by Def32
.= 1 ; :: thesis: verum