thus nand3 . <*0,0,0*> = (('not' FALSE) 'or' ('not' FALSE)) 'or' TRUE by Lm6
.= 1 ; :: thesis: ( 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 ; :: thesis: ( 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 ; :: thesis: ( 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 ; :: thesis: ( 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 ; :: thesis: ( 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 ; :: thesis: ( 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 ; :: thesis: nand3 . <*1,1,1*> = 0
thus nand3 . <*1,1,1*> = (FALSE 'or' ('not' TRUE)) 'or' ('not' TRUE) by Lm6
.= 0 ; :: thesis: verum