thus xor3 . <*0,0,0*> = FALSE 'xor' FALSE by Def20
.= 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 Def20
.= 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 Def20, BINARITH:13; :: 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 Def20, BINARITH:13
.= 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 Def20, BINARITH:13; :: 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 Def20, BINARITH:13
.= 0 ; :: thesis: ( xor3 . <*1,1,0*> = 0 & xor3 . <*1,1,1*> = 1 )
thus xor3 . <*1,1,0*> = (TRUE 'xor' TRUE) 'xor' FALSE by Def20
.= 0 ; :: thesis: xor3 . <*1,1,1*> = 1
thus xor3 . <*1,1,1*> = (TRUE 'xor' TRUE) 'xor' TRUE by Def20
.= 1 ; :: thesis: verum