let h, i be Integer; :: thesis: for n being non empty Nat st - (2 to_power ((n + 1) -' 1)) <= h + i & h + i <= (2 to_power ((n + 1) -' 1)) - 1 & h < 0 & i < 0 & - (2 to_power (n -' 1)) <= h & - (2 to_power (n -' 1)) <= i holds
Intval ((2sComplement (n + 1),h) + (2sComplement (n + 1),i)) = h + i
let n be non empty Nat; :: thesis: ( - (2 to_power ((n + 1) -' 1)) <= h + i & h + i <= (2 to_power ((n + 1) -' 1)) - 1 & h < 0 & i < 0 & - (2 to_power (n -' 1)) <= h & - (2 to_power (n -' 1)) <= i implies Intval ((2sComplement (n + 1),h) + (2sComplement (n + 1),i)) = h + i )
assume A1: ( - (2 to_power ((n + 1) -' 1)) <= h + i & h + i <= (2 to_power ((n + 1) -' 1)) - 1 & h < 0 & i < 0 & - (2 to_power (n -' 1)) <= h & - (2 to_power (n -' 1)) <= i ) ; :: thesis: Intval ((2sComplement (n + 1),h) + (2sComplement (n + 1),i)) = h + i
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 + 1) - 1 = n & n >= 0 ) ;
then A2: ( - (2 to_power n) <= h + i & h + i <= (2 to_power n) - 1 ) by A1, XREAL_0:def 2;
then A3: ( - (2 to_power n) < h & - (2 to_power n) < i ) by A1, Th9;
then ( - h < - (- (2 to_power n)) & - i < - (- (2 to_power n)) ) by XREAL_1:26;
then A4: ( abs h < 2 to_power n & abs i < 2 to_power n ) by A1, ABSVALUE:def 1;
n < n + 1 by XREAL_1:31;
then 2 to_power n < 2 to_power (n + 1) by POWER:44;
then A5: ( MajP (n + 1),(abs h) = n + 1 & MajP (n + 1),(abs i) = n + 1 ) by A4, Th24, XXREAL_0:2;
A6: ( (2 to_power (n + 1)) + h < (2 to_power (n + 1)) + 0 & (2 to_power (n + 1)) + i < (2 to_power (n + 1)) + 0 ) by A1, XREAL_1:10;
A7: (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 ;
then A8: ( 2 to_power n <= (2 to_power (n + 1)) + h & 2 to_power n <= (2 to_power (n + 1)) + i ) by A3, XREAL_1:8;
( 0 <= (2 to_power (n + 1)) + h & 0 <= (2 to_power (n + 1)) + i ) by A3, A7, XREAL_1:8;
then reconsider NH = (2 to_power (n + 1)) + h, NI = (2 to_power (n + 1)) + i as Element of NAT by INT_1:16;
consider a being Element of BOOLEAN such that
A9: 2sComplement (n + 1),h = (2sComplement n,h) ^ <*a*> by Th33;
consider a being Element of BOOLEAN such that
A10: 2sComplement (n + 1),i = (2sComplement n,i) ^ <*a*> by Th33;
A11: ( len (2sComplement (n + 1),h) = n + 1 & len (2sComplement (n + 1),i) = n + 1 ) by FINSEQ_1:def 18;
A12: 1 <= n + 1 by NAT_1:11;
then A13: (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 A1, A5, Def2
.= ((n + 1) -BinarySequence NH) . (n + 1) by ABSVALUE:def 1
.= TRUE by A6, A8, BINARI_3:30 ;
A14: (2sComplement (n + 1),i) /. (n + 1) = (2sComplement (n + 1),i) . (n + 1) by A11, A12, FINSEQ_4:24
.= ((n + 1) -BinarySequence (abs ((2 to_power (n + 1)) + i))) . (n + 1) by A1, A5, Def2
.= ((n + 1) -BinarySequence NI) . (n + 1) by ABSVALUE:def 1
.= TRUE by A6, A8, BINARI_3:30 ;
A15: 2sComplement (n + 1),h = (n + 1) -BinarySequence (abs ((2 to_power (n + 1)) + h)) by A1, A5, Def2
.= (n + 1) -BinarySequence NH by ABSVALUE:def 1 ;
A16: 2sComplement (n + 1),i = (n + 1) -BinarySequence (abs ((2 to_power (n + 1)) + i)) by A1, A5, Def2
.= (n + 1) -BinarySequence NI by ABSVALUE:def 1 ;
A17: Intval (2sComplement (n + 1),h) = (Absval (2sComplement (n + 1),h)) - (2 to_power (n + 1)) by A13, BINARI_2:def 3
.= NH - (2 to_power (n + 1)) by A6, A15, BINARI_3:36
.= h ;
A18: Intval (2sComplement (n + 1),i) = (Absval (2sComplement (n + 1),i)) - (2 to_power (n + 1)) by A14, BINARI_2:def 3
.= NI - (2 to_power (n + 1)) by A6, A16, BINARI_3:36
.= i ;
A19: (carry (2sComplement (n + 1),h),(2sComplement (n + 1),i)) /. (n + 1) = TRUE by A1, A2, Th35;
then A20: Int_add_ovfl (2sComplement (n + 1),h),(2sComplement (n + 1),i) = (FALSE '&' ('not' TRUE )) '&' TRUE by A13, A14, BINARI_2:def 4
.= FALSE ;
Int_add_udfl (2sComplement (n + 1),h),(2sComplement (n + 1),i) = (TRUE '&' TRUE ) '&' ('not' TRUE ) by A13, A14, A19, BINARI_2:def 5
.= FALSE ;
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 A9, A10, A17, A18, A20, BINARI_2:14
.= ((h + i) - 0 ) + 0 ;
hence Intval ((2sComplement (n + 1),h) + (2sComplement (n + 1),i)) = h + i ; :: thesis: verum