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:16;
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 6;
then A2: ( ((<*x*> /. 1) '&' (<*y*> /. 1)) 'or' ((<*x*> /. 1) '&' ((carry (<*x*>,<*y*>)) /. 1)) = TRUE or (<*y*> /. 1) '&' ((carry (<*x*>,<*y*>)) /. 1) = TRUE ) by Th12;

now :: thesis: ( x = TRUE & y = TRUE )

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, Th12;

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

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

end;

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

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

end;

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

then (carry (<*x*>,<*y*>)) /. 1 = TRUE by MARGREL1:12;
hence ( x = TRUE & y = TRUE ) by BINARITH:def 2; :: 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 6
.= TRUE by A1 ; :: thesis: verum