let n be non zero 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:21
.= l + (Absval (n -BinarySequence m)) by A3, BINARI_3:35
.= l + m by A5, BINARI_3:35 ;
hence contradiction by A2, A4, A1, XREAL_1:146, XXREAL_0:2; :: thesis: verum