let n be non empty Nat; :: thesis: for l, m being Nat st l + m <= (2 to_power n) - 1 holds
Absval ((n -BinarySequence l) + (n -BinarySequence m)) = l + m
let l, m be Nat; :: thesis: ( l + m <= (2 to_power n) - 1 implies Absval ((n -BinarySequence l) + (n -BinarySequence m)) = l + m )
assume A1: l + m <= (2 to_power n) - 1 ; :: thesis: Absval ((n -BinarySequence l) + (n -BinarySequence m)) = l + m
A2: l < 2 to_power n by A1, Th8;
set L = n -BinarySequence l;
set M = n -BinarySequence m;
add_ovfl (n -BinarySequence l),(n -BinarySequence m) = FALSE by A1, Th10;
then n -BinarySequence l,n -BinarySequence m are_summable by BINARITH:def 10;
then A3: Absval ((n -BinarySequence l) + (n -BinarySequence m)) = (Absval (n -BinarySequence l)) + (Absval (n -BinarySequence m)) by BINARITH:48
.= l + (Absval (n -BinarySequence m)) by A2, BINARI_3:36 ;
m < 2 to_power n by A1, Th8;
hence Absval ((n -BinarySequence l) + (n -BinarySequence m)) = l + m by A3, BINARI_3:36; :: thesis: verum