let x, y be Element of BOOLEAN ; :: thesis: ( add_ovfl <*x*>,<*y*> = TRUE iff ( x = TRUE & y = TRUE ) )
A1: (<*TRUE *> /. 1) '&' (<*TRUE *> /. 1) = TRUE by FINSEQ_4:25;
thus ( add_ovfl <*x*>,<*y*> = TRUE implies ( x = TRUE & y = TRUE ) ) :: thesis: ( x = TRUE & y = TRUE implies add_ovfl <*x*>,<*y*> = TRUE )

proof

assume add_ovfl <*x*>,<*y*> = TRUE ; :: thesis: ( x = TRUE & y = TRUE )
then (((<*x*> /. 1) '&' (<*y*> /. 1)) 'or' ((<*x*> /. 1) '&' ((carry <*x*>,<*y*>) /. 1))) 'or' ((<*y*> /. 1) '&' ((carry <*x*>,<*y*>) /. 1)) = TRUE by BINARITH:def 9;
then A2: ( ((<*x*> /. 1) '&' (<*y*> /. 1)) 'or' ((<*x*> /. 1) '&' ((carry <*x*>,<*y*>) /. 1)) = TRUE or (<*y*> /. 1) '&' ((carry <*x*>,<*y*>) /. 1) = TRUE ) by Th13;

now

per cases ( (<*x*> /. 1) '&' (<*y*> /. 1) = TRUE or (<*x*> /. 1) '&' ((carry <*x*>,<*y*>) /. 1) = TRUE or (<*y*> /. 1) '&' ((carry <*x*>,<*y*>) /. 1) = TRUE ) by A2, Th13;

suppose A3: (<*x*> /. 1) '&' (<*y*> /. 1) = TRUE ; :: thesis: ( x = TRUE & y = TRUE )

then <*x*> /. 1 = TRUE by MARGREL1:45;
hence ( x = TRUE & y = TRUE ) by A3, FINSEQ_4:25; :: thesis: verum

end;

suppose (<*x*> /. 1) '&' ((carry <*x*>,<*y*>) /. 1) = TRUE ; :: thesis: ( x = TRUE & y = TRUE )

then (carry <*x*>,<*y*>) /. 1 = TRUE by MARGREL1:45;
hence ( x = TRUE & y = TRUE ) by BINARITH:def 5; :: thesis: verum

end;

suppose (<*y*> /. 1) '&' ((carry <*x*>,<*y*>) /. 1) = TRUE ; :: thesis: ( x = TRUE & y = TRUE )

then (carry <*x*>,<*y*>) /. 1 = TRUE by MARGREL1:45;
hence ( x = TRUE & y = TRUE ) by BINARITH:def 5; :: thesis: verum

end;

end;

end;

hence ( x = TRUE & y = TRUE ) ; :: thesis: verum

end;

assume that
A4: x = TRUE and
A5: y = TRUE ; :: thesis: add_ovfl <*x*>,<*y*> = TRUE
thus add_ovfl <*x*>,<*y*> = (((<*TRUE *> /. 1) '&' (<*TRUE *> /. 1)) 'or' ((<*TRUE *> /. 1) '&' ((carry <*TRUE *>,<*TRUE *>) /. 1))) 'or' ((<*TRUE *> /. 1) '&' ((carry <*TRUE *>,<*TRUE *>) /. 1)) by A4, A5, BINARITH:def 9
.= TRUE by A1 ; :: thesis: verum