let n be non zero 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 7;
then A3: Absval ((n -BinarySequence l) + (n -BinarySequence m)) = (Absval (n -BinarySequence l)) + (Absval (n -BinarySequence m)) by BINARITH:22
.= l + (Absval (n -BinarySequence m)) by A2, BINARI_3:35 ;
m < 2 to_power n by A1, Th8;
hence Absval ((n -BinarySequence l) + (n -BinarySequence m)) = l + m by A3, BINARI_3:35; :: thesis: verum