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