let h, i be Integer; :: thesis: for n being non empty Nat st - (2 to_power (n -' 1)) <= h + i & h + i <= (2 to_power (n -' 1)) - 1 & h >= 0 & i >= 0 holds
Intval ((2sComplement n,h) + (2sComplement n,i)) = h + i
let n be non empty Nat; :: thesis: ( - (2 to_power (n -' 1)) <= h + i & h + i <= (2 to_power (n -' 1)) - 1 & h >= 0 & i >= 0 implies Intval ((2sComplement n,h) + (2sComplement n,i)) = h + i )
assume A1: ( - (2 to_power (n -' 1)) <= h + i & h + i <= (2 to_power (n -' 1)) - 1 & h >= 0 & i >= 0 ) ; :: thesis: Intval ((2sComplement n,h) + (2sComplement n,i)) = h + i
reconsider h = h, i = i as Element of NAT by A1, INT_1:16;
A2: 2sComplement n,h = n -BinarySequence (abs h) by Def2
.= n -BinarySequence h by ABSVALUE:def 1 ;
2sComplement n,i = n -BinarySequence (abs i) by Def2
.= n -BinarySequence i by ABSVALUE:def 1 ;
hence Intval ((2sComplement n,h) + (2sComplement n,i)) = h + i by A1, A2, Th14; :: thesis: verum