let n be non empty Nat; :: thesis: for l, m being Nat st l + m <= (2 to_power n) - 1 holds
add_ovfl (n -BinarySequence l),(n -BinarySequence m) = FALSE
let l, m be Nat; :: thesis: ( l + m <= (2 to_power n) - 1 implies add_ovfl (n -BinarySequence l),(n -BinarySequence m) = FALSE )
set L = n -BinarySequence l;
set M = n -BinarySequence m;
A1: (Absval ((n -BinarySequence l) + (n -BinarySequence m))) + (2 to_power n) >= 2 to_power n by NAT_1:11;
assume A2: l + m <= (2 to_power n) - 1 ; :: thesis: add_ovfl (n -BinarySequence l),(n -BinarySequence m) = FALSE
then A3: l < 2 to_power n by Th8;
assume add_ovfl (n -BinarySequence l),(n -BinarySequence m) <> FALSE ; :: thesis: contradiction
then A4: IFEQ (add_ovfl (n -BinarySequence l),(n -BinarySequence m)),FALSE ,0 ,(2 to_power n) = 2 to_power n by FUNCOP_1:def 8;
A5: m < 2 to_power n by A2, Th8;
(Absval ((n -BinarySequence l) + (n -BinarySequence m))) + (IFEQ (add_ovfl (n -BinarySequence l),(n -BinarySequence m)),FALSE ,0 ,(2 to_power n)) = (Absval (n -BinarySequence l)) + (Absval (n -BinarySequence m)) by BINARITH:47
.= l + (Absval (n -BinarySequence m)) by A3, BINARI_3:36
.= l + m by A5, BINARI_3:36 ;
hence contradiction by A2, A4, A1, XREAL_1:148, XXREAL_0:2; :: thesis: verum