thus and2 . <*0,0*> = FALSE '&' FALSE by Def1
.= 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 & and2b . <*0,0*> = 1 & and2b . <*0,1*> = 0 & and2b . <*1,0*> = 0 & and2b . <*1,1*> = 0 )
thus and2 . <*0,1*> = FALSE '&' TRUE by Def1
.= 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 & and2b . <*0,0*> = 1 & and2b . <*0,1*> = 0 & and2b . <*1,0*> = 0 & and2b . <*1,1*> = 0 )
thus and2 . <*1,0*> = TRUE '&' FALSE by Def1
.= 0 ; :: thesis: ( and2 . <*1,1*> = 1 & and2a . <*0,0*> = 0 & and2a . <*0,1*> = 1 & and2a . <*1,0*> = 0 & and2a . <*1,1*> = 0 & and2b . <*0,0*> = 1 & and2b . <*0,1*> = 0 & and2b . <*1,0*> = 0 & and2b . <*1,1*> = 0 )
thus and2 . <*1,1*> = TRUE '&' TRUE by Def1
.= 1 ; :: thesis: ( and2a . <*0,0*> = 0 & and2a . <*0,1*> = 1 & and2a . <*1,0*> = 0 & and2a . <*1,1*> = 0 & and2b . <*0,0*> = 1 & and2b . <*0,1*> = 0 & and2b . <*1,0*> = 0 & and2b . <*1,1*> = 0 )
thus and2a . <*0,0*> = ('not' FALSE) '&' FALSE by Def2
.= 0 ; :: thesis: ( and2a . <*0,1*> = 1 & and2a . <*1,0*> = 0 & and2a . <*1,1*> = 0 & and2b . <*0,0*> = 1 & and2b . <*0,1*> = 0 & and2b . <*1,0*> = 0 & and2b . <*1,1*> = 0 )
thus and2a . <*0,1*> = ('not' FALSE) '&' TRUE by Def2
.= 1 ; :: thesis: ( and2a . <*1,0*> = 0 & and2a . <*1,1*> = 0 & and2b . <*0,0*> = 1 & and2b . <*0,1*> = 0 & and2b . <*1,0*> = 0 & and2b . <*1,1*> = 0 )
thus and2a . <*1,0*> = ('not' TRUE) '&' FALSE by Def2
.= 0 ; :: thesis: ( and2a . <*1,1*> = 0 & and2b . <*0,0*> = 1 & and2b . <*0,1*> = 0 & and2b . <*1,0*> = 0 & and2b . <*1,1*> = 0 )
thus and2a . <*1,1*> = ('not' TRUE) '&' TRUE by Def2
.= 0 ; :: thesis: ( and2b . <*0,0*> = 1 & and2b . <*0,1*> = 0 & and2b . <*1,0*> = 0 & and2b . <*1,1*> = 0 )
thus and2b . <*0,0*> = TRUE '&' ('not' FALSE) by Def3
.= 1 ; :: thesis: ( and2b . <*0,1*> = 0 & and2b . <*1,0*> = 0 & and2b . <*1,1*> = 0 )
thus and2b . <*0,1*> = ('not' FALSE) '&' ('not' TRUE) by Def3
.= 0 ; :: thesis: ( and2b . <*1,0*> = 0 & and2b . <*1,1*> = 0 )
thus and2b . <*1,0*> = ('not' TRUE) '&' ('not' FALSE) by Def3
.= 0 ; :: thesis: and2b . <*1,1*> = 0
thus and2b . <*1,1*> = FALSE '&' ('not' TRUE) by Def3
.= 0 ; :: thesis: verum