thus nor3 . <*0,0,0*> = (TRUE '&' ('not' FALSE)) '&' ('not' FALSE) by Lm7
.= 1 ; :: thesis: ( nor3 . <*0,0,1*> = 0 & nor3 . <*0,1,0*> = 0 & nor3 . <*0,1,1*> = 0 & nor3 . <*1,0,0*> = 0 & nor3 . <*1,0,1*> = 0 & nor3 . <*1,1,0*> = 0 & nor3 . <*1,1,1*> = 0 )
thus nor3 . <*0,0,1*> = (('not' FALSE) '&' ('not' FALSE)) '&' ('not' TRUE) by Lm7
.= 0 ; :: thesis: ( nor3 . <*0,1,0*> = 0 & nor3 . <*0,1,1*> = 0 & nor3 . <*1,0,0*> = 0 & nor3 . <*1,0,1*> = 0 & nor3 . <*1,1,0*> = 0 & nor3 . <*1,1,1*> = 0 )
thus nor3 . <*0,1,0*> = (('not' FALSE) '&' ('not' TRUE)) '&' ('not' FALSE) by Lm7
.= 0 ; :: thesis: ( nor3 . <*0,1,1*> = 0 & nor3 . <*1,0,0*> = 0 & nor3 . <*1,0,1*> = 0 & nor3 . <*1,1,0*> = 0 & nor3 . <*1,1,1*> = 0 )
thus nor3 . <*0,1,1*> = (('not' FALSE) '&' ('not' TRUE)) '&' FALSE by Lm7
.= 0 ; :: thesis: ( nor3 . <*1,0,0*> = 0 & nor3 . <*1,0,1*> = 0 & nor3 . <*1,1,0*> = 0 & nor3 . <*1,1,1*> = 0 )
thus nor3 . <*1,0,0*> = (('not' TRUE) '&' ('not' FALSE)) '&' ('not' FALSE) by Lm7
.= 0 ; :: thesis: ( nor3 . <*1,0,1*> = 0 & nor3 . <*1,1,0*> = 0 & nor3 . <*1,1,1*> = 0 )
thus nor3 . <*1,0,1*> = (('not' TRUE) '&' ('not' FALSE)) '&' FALSE by Lm7
.= 0 ; :: thesis: ( nor3 . <*1,1,0*> = 0 & nor3 . <*1,1,1*> = 0 )
thus nor3 . <*1,1,0*> = (FALSE '&' ('not' TRUE)) '&' ('not' FALSE) by Lm7
.= 0 ; :: thesis: nor3 . <*1,1,1*> = 0
thus nor3 . <*1,1,1*> = (('not' TRUE) '&' ('not' TRUE)) '&' FALSE by Lm7
.= 0 ; :: thesis: verum