let x, y be Element of BOOLEAN ; :: thesis: ( add_ovfl <*x*>,<*y*> = TRUE iff ( x = TRUE & y = TRUE ) )
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 A1: ( ((<*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 A1, Th13;

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

then ( <*x*> /. 1 = TRUE & <*y*> /. 1 = TRUE ) by MARGREL1:45;
hence ( x = TRUE & y = TRUE ) by 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
A2: x = TRUE and
A3: y = TRUE ; :: thesis: add_ovfl <*x*>,<*y*> = TRUE
A4: (<*TRUE *> /. 1) '&' (<*TRUE *> /. 1) = TRUE by FINSEQ_4:25;
thus add_ovfl <*x*>,<*y*> = (((<*TRUE *> /. 1) '&' (<*TRUE *> /. 1)) 'or' ((<*TRUE *> /. 1) '&' ((carry <*TRUE *>,<*TRUE *>) /. 1))) 'or' ((<*TRUE *> /. 1) '&' ((carry <*TRUE *>,<*TRUE *>) /. 1)) by A2, A3, BINARITH:def 9
.= TRUE by A4 ; :: thesis: verum