thus nand3 . <*0,0,0*> =
(('not' FALSE) 'or' ('not' FALSE)) 'or' TRUE
by Lm6
.=
1
; ( nand3 . <*0,0,1*> = 1 & nand3 . <*0,1,0*> = 1 & nand3 . <*0,1,1*> = 1 & nand3 . <*1,0,0*> = 1 & nand3 . <*1,0,1*> = 1 & nand3 . <*1,1,0*> = 1 & nand3 . <*1,1,1*> = 0 )
thus nand3 . <*0,0,1*> =
(('not' FALSE) 'or' ('not' FALSE)) 'or' FALSE
by Lm6
.=
1
; ( nand3 . <*0,1,0*> = 1 & nand3 . <*0,1,1*> = 1 & nand3 . <*1,0,0*> = 1 & nand3 . <*1,0,1*> = 1 & nand3 . <*1,1,0*> = 1 & nand3 . <*1,1,1*> = 0 )
thus nand3 . <*0,1,0*> =
(('not' FALSE) 'or' ('not' TRUE)) 'or' TRUE
by Lm6
.=
1
; ( nand3 . <*0,1,1*> = 1 & nand3 . <*1,0,0*> = 1 & nand3 . <*1,0,1*> = 1 & nand3 . <*1,1,0*> = 1 & nand3 . <*1,1,1*> = 0 )
thus nand3 . <*0,1,1*> =
(TRUE 'or' ('not' TRUE)) 'or' ('not' TRUE)
by Lm6
.=
1
; ( nand3 . <*1,0,0*> = 1 & nand3 . <*1,0,1*> = 1 & nand3 . <*1,1,0*> = 1 & nand3 . <*1,1,1*> = 0 )
thus nand3 . <*1,0,0*> =
(('not' TRUE) 'or' ('not' FALSE)) 'or' TRUE
by Lm6
.=
1
; ( nand3 . <*1,0,1*> = 1 & nand3 . <*1,1,0*> = 1 & nand3 . <*1,1,1*> = 0 )
thus nand3 . <*1,0,1*> =
(('not' TRUE) 'or' TRUE) 'or' ('not' TRUE)
by Lm6
.=
1
; ( nand3 . <*1,1,0*> = 1 & nand3 . <*1,1,1*> = 0 )
thus nand3 . <*1,1,0*> =
(('not' TRUE) 'or' ('not' TRUE)) 'or' TRUE
by Lm6
.=
1
; nand3 . <*1,1,1*> = 0
thus nand3 . <*1,1,1*> =
(FALSE 'or' ('not' TRUE)) 'or' ('not' TRUE)
by Lm6
.=
0
; verum