thus or2 . <*0,0*> =
FALSE 'or' FALSE
by FACIRC_1:def 5
.=
0
; ( 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
; ( 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
; ( 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
; ( 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
; ( 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
; ( 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
; ( 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
; ( 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
; ( nand2 . <*0,1*> = 1 & nand2 . <*1,0*> = 1 & nand2 . <*1,1*> = 0 )
thus nand2 . <*0,1*> =
TRUE 'or' ('not' TRUE)
by Lm2
.=
1
; ( nand2 . <*1,0*> = 1 & nand2 . <*1,1*> = 0 )
thus nand2 . <*1,0*> =
('not' TRUE) 'or' TRUE
by Lm2
.=
1
; nand2 . <*1,1*> = 0
thus nand2 . <*1,1*> =
FALSE 'or' ('not' TRUE)
by Lm2
.=
0
; verum