let x, y be Element of BOOLEAN ; ( 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 ) )
( x = TRUE & y = TRUE implies add_ovfl (<*x*>,<*y*>) = TRUE )
assume that
A4:
x = TRUE
and
A5:
y = TRUE
; 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
; verum