thus and3b . <*0 ,0 ,0 *> = (('not' FALSE ) '&' ('not' FALSE )) '&' FALSE by Def18
.= 0 ; :: thesis: ( and3b . <*0 ,0 ,1*> = 1 & and3b . <*0 ,1,0 *> = 0 & and3b . <*0 ,1,1*> = 0 & and3b . <*1,0 ,0 *> = 0 & and3b . <*1,0 ,1*> = 0 & and3b . <*1,1,0 *> = 0 & and3b . <*1,1,1*> = 0 )
thus and3b . <*0 ,0 ,1*> = (TRUE '&' ('not' FALSE )) '&' TRUE by Def18
.= 1 ; :: thesis: ( and3b . <*0 ,1,0 *> = 0 & and3b . <*0 ,1,1*> = 0 & and3b . <*1,0 ,0 *> = 0 & and3b . <*1,0 ,1*> = 0 & and3b . <*1,1,0 *> = 0 & and3b . <*1,1,1*> = 0 )
thus and3b . <*0 ,1,0 *> = (('not' FALSE ) '&' ('not' TRUE )) '&' FALSE by Def18
.= 0 ; :: thesis: ( and3b . <*0 ,1,1*> = 0 & and3b . <*1,0 ,0 *> = 0 & and3b . <*1,0 ,1*> = 0 & and3b . <*1,1,0 *> = 0 & and3b . <*1,1,1*> = 0 )
thus and3b . <*0 ,1,1*> = (('not' FALSE ) '&' ('not' TRUE )) '&' TRUE by Def18
.= 0 ; :: thesis: ( and3b . <*1,0 ,0 *> = 0 & and3b . <*1,0 ,1*> = 0 & and3b . <*1,1,0 *> = 0 & and3b . <*1,1,1*> = 0 )
thus and3b . <*1,0 ,0 *> = (('not' TRUE ) '&' ('not' FALSE )) '&' FALSE by Def18
.= 0 ; :: thesis: ( and3b . <*1,0 ,1*> = 0 & and3b . <*1,1,0 *> = 0 & and3b . <*1,1,1*> = 0 )
thus and3b . <*1,0 ,1*> = (('not' TRUE ) '&' ('not' FALSE )) '&' TRUE by Def18
.= 0 ; :: thesis: ( and3b . <*1,1,0 *> = 0 & and3b . <*1,1,1*> = 0 )
thus and3b . <*1,1,0 *> = (('not' TRUE ) '&' ('not' TRUE )) '&' FALSE by Def18
.= 0 ; :: thesis: and3b . <*1,1,1*> = 0
thus and3b . <*1,1,1*> = (FALSE '&' ('not' TRUE )) '&' TRUE by Def18
.= 0 ; :: thesis: verum