let h, i be Integer; :: thesis: for n being non zero 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 zero 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:3;
A3: 2sComplement (n,i) = n -BinarySequence |.i.| by Def2
.= n -BinarySequence i by ABSVALUE:def 1 ;
2sComplement (n,h) = n -BinarySequence |.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