thus or2 . <*0,0*> = FALSE 'or' FALSE by FACIRC_1:def 5
.= 0 ; :: thesis: ( or2 . <*0,1*> = 1 & or2 . <*1,0*> = 1 & or2 . <*1,1*> = 1 & or2a . <*0,0*> = 1 & or2a . <*0,1*> = 1 & or2a . <*1,0*> = 0 & or2a . <*1,1*> = 1 & nand2 . <*0,0*> = 1 & nand2 . <*0,1*> = 1 & nand2 . <*1,0*> = 1 & nand2 . <*1,1*> = 0 )
thus or2 . <*0,1*> = FALSE 'or' TRUE by FACIRC_1:def 5
.= 1 ; :: thesis: ( or2 . <*1,0*> = 1 & or2 . <*1,1*> = 1 & or2a . <*0,0*> = 1 & or2a . <*0,1*> = 1 & or2a . <*1,0*> = 0 & or2a . <*1,1*> = 1 & nand2 . <*0,0*> = 1 & nand2 . <*0,1*> = 1 & nand2 . <*1,0*> = 1 & nand2 . <*1,1*> = 0 )
thus or2 . <*1,0*> = TRUE 'or' FALSE by FACIRC_1:def 5
.= 1 ; :: thesis: ( or2 . <*1,1*> = 1 & or2a . <*0,0*> = 1 & or2a . <*0,1*> = 1 & or2a . <*1,0*> = 0 & or2a . <*1,1*> = 1 & nand2 . <*0,0*> = 1 & nand2 . <*0,1*> = 1 & nand2 . <*1,0*> = 1 & nand2 . <*1,1*> = 0 )
thus or2 . <*1,1*> = TRUE 'or' TRUE by FACIRC_1:def 5
.= 1 ; :: thesis: ( or2a . <*0,0*> = 1 & or2a . <*0,1*> = 1 & or2a . <*1,0*> = 0 & or2a . <*1,1*> = 1 & nand2 . <*0,0*> = 1 & nand2 . <*0,1*> = 1 & nand2 . <*1,0*> = 1 & nand2 . <*1,1*> = 0 )
thus or2a . <*0,0*> = TRUE 'or' FALSE by Def4
.= 1 ; :: thesis: ( or2a . <*0,1*> = 1 & or2a . <*1,0*> = 0 & or2a . <*1,1*> = 1 & nand2 . <*0,0*> = 1 & nand2 . <*0,1*> = 1 & nand2 . <*1,0*> = 1 & nand2 . <*1,1*> = 0 )
thus or2a . <*0,1*> = ('not' FALSE) 'or' TRUE by Def4
.= 1 ; :: thesis: ( or2a . <*1,0*> = 0 & or2a . <*1,1*> = 1 & nand2 . <*0,0*> = 1 & nand2 . <*0,1*> = 1 & nand2 . <*1,0*> = 1 & nand2 . <*1,1*> = 0 )
thus or2a . <*1,0*> = ('not' TRUE) 'or' FALSE by Def4
.= 0 ; :: thesis: ( or2a . <*1,1*> = 1 & nand2 . <*0,0*> = 1 & nand2 . <*0,1*> = 1 & nand2 . <*1,0*> = 1 & nand2 . <*1,1*> = 0 )
thus or2a . <*1,1*> = ('not' TRUE) 'or' TRUE by Def4
.= 1 ; :: thesis: ( nand2 . <*0,0*> = 1 & nand2 . <*0,1*> = 1 & nand2 . <*1,0*> = 1 & nand2 . <*1,1*> = 0 )
thus nand2 . <*0,0*> = TRUE 'or' ('not' FALSE) by Lm2
.= 1 ; :: thesis: ( nand2 . <*0,1*> = 1 & nand2 . <*1,0*> = 1 & nand2 . <*1,1*> = 0 )
thus nand2 . <*0,1*> = TRUE 'or' ('not' TRUE) by Lm2
.= 1 ; :: thesis: ( nand2 . <*1,0*> = 1 & nand2 . <*1,1*> = 0 )
thus nand2 . <*1,0*> = ('not' TRUE) 'or' TRUE by Lm2
.= 1 ; :: thesis: nand2 . <*1,1*> = 0
thus nand2 . <*1,1*> = FALSE 'or' ('not' TRUE) by Lm2
.= 0 ; :: thesis: verum