let h, i be Integer; :: thesis:
let n be non empty Nat; :: thesis:
assume that
A1: - (2 to_power ((n + 1) -' 1)) <= h + i and
A2: h < 0 and
A3: i < 0 and
A4: ( - (2 to_power (n -' 1)) <= h & - (2 to_power (n -' 1)) <= i ) ; :: thesis:
A5: (2 to_power (n + 1)) + (- (2 to_power n)) = (- (2 to_power n)) + ((2 to_power 1) * (2 to_power n)) by POWER:32
.= (- (2 to_power n)) + (2 * (2 to_power n)) by POWER:30
.= 2 to_power n ;
(n + 1) - 1 = n ;
then A6: - (2 to_power n) <= h + i by A1, XREAL_0:def 2;
then A7: - (2 to_power n) < h by A2, A3, Th9;
then A8: 2 to_power n <= (2 to_power (n + 1)) + h by A5, XREAL_1:8;
A9: - (2 to_power n) < i by A2, A3, A6, Th9;
then A10: 0 <= (2 to_power (n + 1)) + i by A5, XREAL_1:8;
0 <= (2 to_power (n + 1)) + h by A7, A5, XREAL_1:8;
then reconsider NH = (2 to_power (n + 1)) + h, NI = (2 to_power (n + 1)) + i as Element of NAT by A10, INT_1:16;
A11: 1 <= n + 1 by NAT_1:11;
set H = 2sComplement n,h;
set I = 2sComplement n,i;
set H1 = 2sComplement (n + 1),h;
set I1 = 2sComplement (n + 1),i;
set F = FALSE ;
set T = TRUE ;
n < n + 1 by XREAL_1:31;
then A12: 2 to_power n < 2 to_power (n + 1) by POWER:44;
A13: ( ex a being Element of BOOLEAN st 2sComplement (n + 1),h = (2sComplement n,h) ^ <*a*> & ex a being Element of BOOLEAN st 2sComplement (n + 1),i = (2sComplement n,i) ^ <*a*> ) by Th33;
A14: (2 to_power (n + 1)) + h < (2 to_power (n + 1)) + 0 by A2, XREAL_1:10;
- h < - (- (2 to_power n)) by A7, XREAL_1:26;
then abs h < 2 to_power n by A2, ABSVALUE:def 1;
then A15: MajP (n + 1),(abs h) = n + 1 by A12, Th24, XXREAL_0:2;
then A16: 2sComplement (n + 1),h = (n + 1) -BinarySequence (abs ((2 to_power (n + 1)) + h)) by A2, Def2
.= (n + 1) -BinarySequence NH by ABSVALUE:def 1 ;
len (2sComplement (n + 1),h) = n + 1 by FINSEQ_1:def 18;
then A17: (2sComplement (n + 1),h) /. (n + 1) = (2sComplement (n + 1),h) . (n + 1) by A11, FINSEQ_4:24
.= ((n + 1) -BinarySequence (abs ((2 to_power (n + 1)) + h))) . (n + 1) by A2, A15, Def2
.= ((n + 1) -BinarySequence NH) . (n + 1) by ABSVALUE:def 1
.= TRUE by A14, A8, BINARI_3:30 ;
A18: 2 to_power n <= (2 to_power (n + 1)) + i by A9, A5, XREAL_1:8;
A19: (2 to_power (n + 1)) + i < (2 to_power (n + 1)) + 0 by A3, XREAL_1:10;
- i < - (- (2 to_power n)) by A9, XREAL_1:26;
then abs i < 2 to_power n by A3, ABSVALUE:def 1;
then A20: MajP (n + 1),(abs i) = n + 1 by A12, Th24, XXREAL_0:2;
then A21: 2sComplement (n + 1),i = (n + 1) -BinarySequence (abs ((2 to_power (n + 1)) + i)) by A3, Def2
.= (n + 1) -BinarySequence NI by ABSVALUE:def 1 ;
len (2sComplement (n + 1),i) = n + 1 by FINSEQ_1:def 18;
then A22: (2sComplement (n + 1),i) /. (n + 1) = (2sComplement (n + 1),i) . (n + 1) by A11, FINSEQ_4:24
.= ((n + 1) -BinarySequence (abs ((2 to_power (n + 1)) + i))) . (n + 1) by A3, A20, Def2
.= ((n + 1) -BinarySequence NI) . (n + 1) by ABSVALUE:def 1
.= TRUE by A19, A18, BINARI_3:30 ;
then A23: Intval (2sComplement (n + 1),i) = (Absval (2sComplement (n + 1),i)) - (2 to_power (n + 1)) by BINARI_2:def 3
.= NI - (2 to_power (n + 1)) by A19, A21, BINARI_3:36
.= i ;
A24: (carry (2sComplement (n + 1),h),(2sComplement (n + 1),i)) /. (n + 1) = TRUE by A2, A3, A4, A6, Th35;
then A25: Int_add_ovfl (2sComplement (n + 1),h),(2sComplement (n + 1),i) = (FALSE '&' ('not' TRUE )) '&' TRUE by A17, A22, BINARI_2:def 4
.= FALSE ;
A26: Int_add_udfl (2sComplement (n + 1),h),(2sComplement (n + 1),i) = (TRUE '&' TRUE ) '&' ('not' TRUE ) by A17, A22, A24, BINARI_2:def 5
.= FALSE ;
Intval (2sComplement (n + 1),h) = (Absval (2sComplement (n + 1),h)) - (2 to_power (n + 1)) by A17, BINARI_2:def 3
.= NH - (2 to_power (n + 1)) by A14, A16, BINARI_3:36
.= h ;
then Intval ((2sComplement (n + 1),h) + (2sComplement (n + 1),i)) = ((h + i) - (IFEQ FALSE ,FALSE ,0 ,(2 to_power (n + 1)))) + (IFEQ FALSE ,FALSE ,0 ,(2 to_power (n + 1))) by A13, A23, A25, A26, BINARI_2:14
.= ((h + i) - 0 ) + 0 ;
hence Intval ((2sComplement (n + 1),h) + (2sComplement (n + 1),i)) = h + i ; :: thesis: