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