thus and2 . <*0,0*> = FALSE '&' FALSE by FACIRC_1:def 6
.= 0 ; :: thesis: ( and2 . <*0,1*> = 0 & and2 . <*1,0*> = 0 & and2 . <*1,1*> = 1 & and2a . <*0,0*> = 0 & and2a . <*0,1*> = 1 & and2a . <*1,0*> = 0 & and2a . <*1,1*> = 0 & nor2 . <*0,0*> = 1 & nor2 . <*0,1*> = 0 & nor2 . <*1,0*> = 0 & nor2 . <*1,1*> = 0 )
thus and2 . <*0,1*> = FALSE '&' TRUE by FACIRC_1:def 6
.= 0 ; :: thesis: ( and2 . <*1,0*> = 0 & and2 . <*1,1*> = 1 & and2a . <*0,0*> = 0 & and2a . <*0,1*> = 1 & and2a . <*1,0*> = 0 & and2a . <*1,1*> = 0 & nor2 . <*0,0*> = 1 & nor2 . <*0,1*> = 0 & nor2 . <*1,0*> = 0 & nor2 . <*1,1*> = 0 )
thus and2 . <*1,0*> = TRUE '&' FALSE by FACIRC_1:def 6
.= 0 ; :: thesis: ( and2 . <*1,1*> = 1 & and2a . <*0,0*> = 0 & and2a . <*0,1*> = 1 & and2a . <*1,0*> = 0 & and2a . <*1,1*> = 0 & nor2 . <*0,0*> = 1 & nor2 . <*0,1*> = 0 & nor2 . <*1,0*> = 0 & nor2 . <*1,1*> = 0 )
thus and2 . <*1,1*> = TRUE '&' TRUE by FACIRC_1:def 6
.= 1 ; :: thesis: ( and2a . <*0,0*> = 0 & and2a . <*0,1*> = 1 & and2a . <*1,0*> = 0 & and2a . <*1,1*> = 0 & nor2 . <*0,0*> = 1 & nor2 . <*0,1*> = 0 & nor2 . <*1,0*> = 0 & nor2 . <*1,1*> = 0 )
thus and2a . <*0,0*> = ('not' FALSE) '&' FALSE by Def1
.= 0 ; :: thesis: ( and2a . <*0,1*> = 1 & and2a . <*1,0*> = 0 & and2a . <*1,1*> = 0 & nor2 . <*0,0*> = 1 & nor2 . <*0,1*> = 0 & nor2 . <*1,0*> = 0 & nor2 . <*1,1*> = 0 )
thus and2a . <*0,1*> = ('not' FALSE) '&' TRUE by Def1
.= 1 ; :: thesis: ( and2a . <*1,0*> = 0 & and2a . <*1,1*> = 0 & nor2 . <*0,0*> = 1 & nor2 . <*0,1*> = 0 & nor2 . <*1,0*> = 0 & nor2 . <*1,1*> = 0 )
thus and2a . <*1,0*> = ('not' TRUE) '&' FALSE by Def1
.= 0 ; :: thesis: ( and2a . <*1,1*> = 0 & nor2 . <*0,0*> = 1 & nor2 . <*0,1*> = 0 & nor2 . <*1,0*> = 0 & nor2 . <*1,1*> = 0 )
thus and2a . <*1,1*> = ('not' TRUE) '&' TRUE by Def1
.= 0 ; :: thesis: ( nor2 . <*0,0*> = 1 & nor2 . <*0,1*> = 0 & nor2 . <*1,0*> = 0 & nor2 . <*1,1*> = 0 )
thus nor2 . <*0,0*> = TRUE '&' ('not' FALSE) by Lm3
.= 1 ; :: thesis: ( nor2 . <*0,1*> = 0 & nor2 . <*1,0*> = 0 & nor2 . <*1,1*> = 0 )
thus nor2 . <*0,1*> = ('not' FALSE) '&' ('not' TRUE) by Lm3
.= 0 ; :: thesis: ( nor2 . <*1,0*> = 0 & nor2 . <*1,1*> = 0 )
thus nor2 . <*1,0*> = ('not' TRUE) '&' ('not' FALSE) by Lm3
.= 0 ; :: thesis: nor2 . <*1,1*> = 0
thus nor2 . <*1,1*> = FALSE '&' ('not' TRUE) by Lm3
.= 0 ; :: thesis: verum