let h, i be Integer; :: thesis: for n being non empty Nat st - (2 to_power (n -' 1)) <= h & h <= (2 to_power (n -' 1)) - 1 & - (2 to_power (n -' 1)) <= i & i <= (2 to_power (n -' 1)) - 1 & - (2 to_power (n -' 1)) <= h + i & h + i <= (2 to_power (n -' 1)) - 1 & ( ( h >= 0 & i < 0 ) or ( h < 0 & i >= 0 ) ) holds
Intval ((2sComplement n,h) + (2sComplement n,i)) = h + i
defpred S₁[ non empty Nat] means ( - (2 to_power ($1 -' 1)) <= h & h <= (2 to_power ($1 -' 1)) - 1 & - (2 to_power ($1 -' 1)) <= i & i <= (2 to_power ($1 -' 1)) - 1 & - (2 to_power ($1 -' 1)) <= h + i & h + i <= (2 to_power ($1 -' 1)) - 1 & ( ( h >= 0 & i < 0 ) or ( h < 0 & i >= 0 ) ) implies Intval ((2sComplement $1,h) + (2sComplement $1,i)) = h + i );
A1: S₁[1]

proof

assume A2: ( - (2 to_power (1 -' 1)) <= h & h <= (2 to_power (1 -' 1)) - 1 & - (2 to_power (1 -' 1)) <= i & i <= (2 to_power (1 -' 1)) - 1 & - (2 to_power (1 -' 1)) <= h + i & h + i <= (2 to_power (1 -' 1)) - 1 & ( ( h >= 0 & i < 0 ) or ( h < 0 & i >= 0 ) ) ) ; :: thesis: Intval ((2sComplement 1,h) + (2sComplement 1,i)) = h + i
1 -' 1 = 1 - 1 by XREAL_0:def 2
.= 0 ;
then A3: ( - 1 <= h & h <= 1 - 1 & - 1 <= i & i <= 1 - 1 & - 1 <= h + i & h + i <= 1 - 1 ) by A2, POWER:29;
A4: 2sComplement 1,0 = 1 -BinarySequence (abs 0 ) by Def2
.= 1 -BinarySequence 0 by ABSVALUE:def 1
.= 0* 1 by BINARI_3:26
.= <*FALSE *> by FINSEQ_2:73 ;
A5: ( 2 to_power 1 = 2 & ( for k being Nat st 2 to_power k >= 1 & k >= 1 holds
k >= 1 ) ) by POWER:30;
abs (- 1) = - (- 1) by ABSVALUE:def 1
.= 1 ;
then A6: MajP 1,(abs (- 1)) = 1 by A5, Def1;
A8: 2sComplement 1,(- 1) = 1 -BinarySequence (abs ((2 to_power 1) + (- 1))) by A6, Def2
.= 1 -BinarySequence (abs (2 + (- 1))) by POWER:30
.= 1 -BinarySequence 1 by ABSVALUE:def 1
.= (0 + 1) -BinarySequence (2 to_power 0 ) by POWER:29
.= (0* 0 ) ^ <*1*> by BINARI_3:29
.= <*TRUE *> by FINSEQ_1:47 ;

now

per cases ( ( h >= 0 & i < 0 ) or ( h < 0 & i >= 0 ) ) by A2;

suppose ( h >= 0 & i < 0 ) ; :: thesis: Intval ((2sComplement 1,h) + (2sComplement 1,i)) = h + i

then A9: ( h = 0 & i <= - 1 ) by A3, INT_1:21;
then i = - 1 by A3, XXREAL_0:1;
hence Intval ((2sComplement 1,h) + (2sComplement 1,i)) = h + i by A4, A8, A9, Th15, BINARI_3:18; :: thesis: verum

end;

suppose A10: ( h < 0 & i >= 0 ) ; :: thesis: Intval ((2sComplement 1,h) + (2sComplement 1,i)) = h + i

then h <= - 1 by INT_1:21;
then A11: h = - 1 by A3, XXREAL_0:1;
i = 0 by A3, A10;
hence Intval ((2sComplement 1,h) + (2sComplement 1,i)) = h + i by A4, A8, A11, Th15, BINARI_3:18; :: thesis: verum

end;

end;

end;

hence Intval ((2sComplement 1,h) + (2sComplement 1,i)) = h + i ; :: thesis: verum

end;

A12: for n being non empty Nat st S₁[n] holds
S₁[n + 1]

proof

let n be non empty Nat; :: thesis: ( S₁[n] implies S₁[n + 1] )
assume ( - (2 to_power (n -' 1)) <= h & h <= (2 to_power (n -' 1)) - 1 & - (2 to_power (n -' 1)) <= i & i <= (2 to_power (n -' 1)) - 1 & - (2 to_power (n -' 1)) <= h + i & h + i <= (2 to_power (n -' 1)) - 1 & ( ( h >= 0 & i < 0 ) or ( h < 0 & i >= 0 ) ) implies Intval ((2sComplement n,h) + (2sComplement n,i)) = h + i ) ; :: thesis: S₁[n + 1]
assume A13: ( - (2 to_power ((n + 1) -' 1)) <= h & h <= (2 to_power ((n + 1) -' 1)) - 1 & - (2 to_power ((n + 1) -' 1)) <= i & i <= (2 to_power ((n + 1) -' 1)) - 1 & - (2 to_power ((n + 1) -' 1)) <= h + i & h + i <= (2 to_power ((n + 1) -' 1)) - 1 & ( ( h >= 0 & i < 0 ) or ( h < 0 & i >= 0 ) ) ) ; :: 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 n2 = 2 to_power n;
set F = FALSE ;
set T = TRUE ;
( (n + 1) - 1 = n & n >= 0 ) ;
then A14: ( - (2 to_power n) <= h & h <= (2 to_power n) - 1 & - (2 to_power n) <= i & i <= (2 to_power n) - 1 & - (2 to_power n) <= h + i & h + i <= (2 to_power n) - 1 ) by A13, XREAL_0:def 2;
consider a being Element of BOOLEAN such that
A15: 2sComplement (n + 1),h = (2sComplement n,h) ^ <*a*> by Th33;
consider b being Element of BOOLEAN such that
A16: 2sComplement (n + 1),i = (2sComplement n,i) ^ <*b*> by Th33;

now

per cases ( ( h >= 0 & i < 0 ) or ( h < 0 & i >= 0 ) ) by A13;

suppose A17: ( h >= 0 & i < 0 ) ; :: thesis: Intval ((2sComplement (n + 1),h) + (2sComplement (n + 1),i)) = h + i

then reconsider h = h as Element of NAT by INT_1:16;
A18: 2sComplement (n + 1),h = (n + 1) -BinarySequence (abs h) by Def2
.= (n + 1) -BinarySequence h by ABSVALUE:def 1 ;
A19: ( len (2sComplement (n + 1),h) = n + 1 & len (2sComplement (n + 1),i) = n + 1 & 1 <= n + 1 ) by FINSEQ_1:def 18, NAT_1:11;
A20: h < 2 to_power n by A14, XREAL_1:148, XXREAL_0:2;
then A21: (2sComplement (n + 1),h) . (n + 1) = FALSE by A18, BINARI_3:27;
abs i = - i by A17, ABSVALUE:def 1;
then A22: abs i <= - (- (2 to_power n)) by A14, XREAL_1:26;
n < n + 1 by XREAL_1:31;
then 2 to_power n < 2 to_power (n + 1) by POWER:44;
then A23: MajP (n + 1),(abs i) = n + 1 by A22, Th24, XXREAL_0:2;
A24: (2 to_power (n + 1)) + i < (2 to_power (n + 1)) + 0 by A17, XREAL_1:10;
(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 A25: 2 to_power n <= (2 to_power (n + 1)) + i by A14, XREAL_1:8;
then reconsider NI = (2 to_power (n + 1)) + i as Element of NAT by INT_1:16;
A26: (2sComplement (n + 1),i) . (n + 1) = ((n + 1) -BinarySequence (abs ((2 to_power (n + 1)) + i))) . (n + 1) by A17, A23, Def2
.= ((n + 1) -BinarySequence NI) . (n + 1) by ABSVALUE:def 1
.= TRUE by A24, A25, BINARI_3:30 ;
n + 0 < n + 1 by XREAL_1:10;
then 2 to_power n < 2 to_power (n + 1) by POWER:44;
then A27: h < 2 to_power (n + 1) by A20, XXREAL_0:2;
A28: (2sComplement (n + 1),h) /. (n + 1) = (2sComplement (n + 1),h) . (n + 1) by A19, FINSEQ_4:24;
then A29: Intval (2sComplement (n + 1),h) = Absval (2sComplement (n + 1),h) by A21, BINARI_2:def 3
.= h by A18, A27, BINARI_3:36 ;
A30: 2sComplement (n + 1),i = (n + 1) -BinarySequence (abs ((2 to_power (n + 1)) + i)) by A17, A23, Def2
.= (n + 1) -BinarySequence NI by ABSVALUE:def 1 ;
A31: (2sComplement (n + 1),i) /. (n + 1) = (2sComplement (n + 1),i) . (n + 1) by A19, FINSEQ_4:24;
then A32: Intval (2sComplement (n + 1),i) = (Absval (2sComplement (n + 1),i)) - (2 to_power (n + 1)) by A26, BINARI_2:def 3
.= NI - (2 to_power (n + 1)) by A24, A30, BINARI_3:36
.= i ;
A33: Int_add_ovfl (2sComplement (n + 1),h),(2sComplement (n + 1),i) = (('not' FALSE ) '&' ('not' TRUE )) '&' ((carry (2sComplement (n + 1),h),(2sComplement (n + 1),i)) /. (n + 1)) by A21, A26, A28, A31, BINARI_2:def 4
.= FALSE ;
Int_add_udfl (2sComplement (n + 1),h),(2sComplement (n + 1),i) = (FALSE '&' TRUE ) '&' ('not' ((carry (2sComplement (n + 1),h),(2sComplement (n + 1),i)) /. (n + 1))) by A21, A26, A28, A31, 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 A15, A16, A29, A32, A33, BINARI_2:14
.= ((h + i) - 0 ) + 0 ;
hence Intval ((2sComplement (n + 1),h) + (2sComplement (n + 1),i)) = h + i ; :: thesis: verum

end;

suppose A34: ( h < 0 & i >= 0 ) ; :: thesis: Intval ((2sComplement (n + 1),h) + (2sComplement (n + 1),i)) = h + i

then reconsider i = i as Element of NAT by INT_1:16;
A35: 2sComplement (n + 1),i = (n + 1) -BinarySequence (abs i) by Def2
.= (n + 1) -BinarySequence i by ABSVALUE:def 1 ;
A36: ( len (2sComplement (n + 1),i) = n + 1 & len (2sComplement (n + 1),h) = n + 1 & 1 <= n + 1 ) by FINSEQ_1:def 18, NAT_1:11;
A37: i < 2 to_power n by A14, XREAL_1:148, XXREAL_0:2;
then A38: (2sComplement (n + 1),i) . (n + 1) = FALSE by A35, BINARI_3:27;
abs h = - h by A34, ABSVALUE:def 1;
then A39: abs h <= - (- (2 to_power n)) by A14, XREAL_1:26;
n < n + 1 by XREAL_1:31;
then 2 to_power n < 2 to_power (n + 1) by POWER:44;
then A40: MajP (n + 1),(abs h) = n + 1 by A39, Th24, XXREAL_0:2;
A41: (2 to_power (n + 1)) + h < (2 to_power (n + 1)) + 0 by A34, XREAL_1:10;
(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 A42: 2 to_power n <= (2 to_power (n + 1)) + h by A14, XREAL_1:8;
then reconsider NH = (2 to_power (n + 1)) + h as Element of NAT by INT_1:16;
A43: (2sComplement (n + 1),h) . (n + 1) = ((n + 1) -BinarySequence (abs ((2 to_power (n + 1)) + h))) . (n + 1) by A34, A40, Def2
.= ((n + 1) -BinarySequence NH) . (n + 1) by ABSVALUE:def 1
.= TRUE by A41, A42, BINARI_3:30 ;
n + 0 < n + 1 by XREAL_1:10;
then 2 to_power n < 2 to_power (n + 1) by POWER:44;
then A44: i < 2 to_power (n + 1) by A37, XXREAL_0:2;
A45: (2sComplement (n + 1),i) /. (n + 1) = (2sComplement (n + 1),i) . (n + 1) by A36, FINSEQ_4:24;
then A46: Intval (2sComplement (n + 1),i) = Absval (2sComplement (n + 1),i) by A38, BINARI_2:def 3
.= i by A35, A44, BINARI_3:36 ;
A47: 2sComplement (n + 1),h = (n + 1) -BinarySequence (abs ((2 to_power (n + 1)) + h)) by A34, A40, Def2
.= (n + 1) -BinarySequence NH by ABSVALUE:def 1 ;
A48: (2sComplement (n + 1),h) /. (n + 1) = (2sComplement (n + 1),h) . (n + 1) by A36, FINSEQ_4:24;
then A49: Intval (2sComplement (n + 1),h) = (Absval (2sComplement (n + 1),h)) - (2 to_power (n + 1)) by A43, BINARI_2:def 3
.= NH - (2 to_power (n + 1)) by A41, A47, BINARI_3:36
.= h ;
A50: Int_add_ovfl (2sComplement (n + 1),h),(2sComplement (n + 1),i) = (('not' TRUE ) '&' ('not' FALSE )) '&' ((carry (2sComplement (n + 1),h),(2sComplement (n + 1),i)) /. (n + 1)) by A38, A43, A45, A48, BINARI_2:def 4
.= FALSE ;
Int_add_udfl (2sComplement (n + 1),h),(2sComplement (n + 1),i) = (TRUE '&' FALSE ) '&' ('not' ((carry (2sComplement (n + 1),h),(2sComplement (n + 1),i)) /. (n + 1))) by A38, A43, A45, A48, 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 A15, A16, A46, A49, A50, BINARI_2:14
.= ((h + i) - 0 ) + 0 ;
hence Intval ((2sComplement (n + 1),h) + (2sComplement (n + 1),i)) = h + i ; :: thesis: verum

end;

end;

end;

hence Intval ((2sComplement (n + 1),h) + (2sComplement (n + 1),i)) = h + i ; :: thesis: verum

end;

thus for n being non empty Nat holds S₁[n] from NAT_1:sch 10(A1, A12); :: thesis: verum