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 )
assume A1: l + m <= (2 to_power n) - 1 ; :: thesis: add_ovfl (n -BinarySequence l),(n -BinarySequence m) = FALSE
set L = n -BinarySequence l;
set M = n -BinarySequence m;
assume A2: add_ovfl (n -BinarySequence l),(n -BinarySequence m) <> FALSE ; :: thesis: contradiction
A3: ( l < 2 to_power n & m < 2 to_power n ) by A1, Th8;
A4: IFEQ (add_ovfl (n -BinarySequence l),(n -BinarySequence m)),FALSE ,0 ,(2 to_power n) = 2 to_power n by A2, FUNCOP_1:def 8;
A5: (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 A3, BINARI_3:36 ;
(Absval ((n -BinarySequence l) + (n -BinarySequence m))) + (2 to_power n) >= 2 to_power n by NAT_1:11;
hence contradiction by A1, A4, A5, XREAL_1:148, XXREAL_0:2; :: thesis: verum