thus or3b . <*0,0,0*> =
(TRUE 'or' ('not' FALSE)) 'or' FALSE
by Def16
.=
1
; ( or3b . <*0,0,1*> = 1 & or3b . <*0,1,0*> = 1 & or3b . <*0,1,1*> = 1 & or3b . <*1,0,0*> = 1 & or3b . <*1,0,1*> = 1 & or3b . <*1,1,0*> = 0 & or3b . <*1,1,1*> = 1 )
thus or3b . <*0,0,1*> =
(('not' FALSE) 'or' ('not' FALSE)) 'or' TRUE
by Def16
.=
1
; ( or3b . <*0,1,0*> = 1 & or3b . <*0,1,1*> = 1 & or3b . <*1,0,0*> = 1 & or3b . <*1,0,1*> = 1 & or3b . <*1,1,0*> = 0 & or3b . <*1,1,1*> = 1 )
thus or3b . <*0,1,0*> =
('not' FALSE) 'or' ('not' TRUE)
by Def16
.=
1
; ( or3b . <*0,1,1*> = 1 & or3b . <*1,0,0*> = 1 & or3b . <*1,0,1*> = 1 & or3b . <*1,1,0*> = 0 & or3b . <*1,1,1*> = 1 )
thus or3b . <*0,1,1*> =
(('not' FALSE) 'or' ('not' TRUE)) 'or' TRUE
by Def16
.=
1
; ( or3b . <*1,0,0*> = 1 & or3b . <*1,0,1*> = 1 & or3b . <*1,1,0*> = 0 & or3b . <*1,1,1*> = 1 )
thus or3b . <*1,0,0*> =
('not' TRUE) 'or' ('not' FALSE)
by Def16
.=
1
; ( or3b . <*1,0,1*> = 1 & or3b . <*1,1,0*> = 0 & or3b . <*1,1,1*> = 1 )
thus or3b . <*1,0,1*> =
(('not' TRUE) 'or' ('not' FALSE)) 'or' TRUE
by Def16
.=
1
; ( or3b . <*1,1,0*> = 0 & or3b . <*1,1,1*> = 1 )
thus or3b . <*1,1,0*> =
('not' TRUE) 'or' ('not' TRUE)
by Def16
.=
0
; or3b . <*1,1,1*> = 1
thus or3b . <*1,1,1*> =
(('not' TRUE) 'or' ('not' TRUE)) 'or' TRUE
by Def16
.=
1
; verum