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: 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 that
A2: - (2 to_power ((n + 1) -' 1)) <= h and
A3: h <= (2 to_power ((n + 1) -' 1)) - 1 and
A4: - (2 to_power ((n + 1) -' 1)) <= i and
A5: i <= (2 to_power ((n + 1) -' 1)) - 1 and
- (2 to_power ((n + 1) -' 1)) <= h + i and
h + i <= (2 to_power ((n + 1) -' 1)) - 1 and
A6: ( ( 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 ;
A7: (n + 1) - 1 = n ;
then A8: - (2 to_power n) <= h by A2, XREAL_0:def 2;
A9: i <= (2 to_power n) - 1 by A5, A7, XREAL_0:def 2;
A10: ( ex a being Element of BOOLEAN st 2sComplement (n + 1),h = (2sComplement n,h) ^ <*a*> & ex b being Element of BOOLEAN st 2sComplement (n + 1),i = (2sComplement n,i) ^ <*b*> ) by Th33;
A11: - (2 to_power n) <= i by A4, A7, XREAL_0:def 2;
A12: h <= (2 to_power n) - 1 by A3, A7, XREAL_0:def 2;

now

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

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

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

end;

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

(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 A31: 2 to_power n <= (2 to_power (n + 1)) + h by A8, XREAL_1:8;
then reconsider NH = (2 to_power (n + 1)) + h as Element of NAT by INT_1:16;
n < n + 1 by XREAL_1:31;
then A32: 2 to_power n < 2 to_power (n + 1) by POWER:44;
abs h = - h by A30, ABSVALUE:def 1;
then abs h <= - (- (2 to_power n)) by A8, XREAL_1:26;
then A33: MajP (n + 1),(abs h) = n + 1 by A32, Th24, XXREAL_0:2;
then A34: 2sComplement (n + 1),h = (n + 1) -BinarySequence (abs ((2 to_power (n + 1)) + h)) by A30, Def2
.= (n + 1) -BinarySequence NH by ABSVALUE:def 1 ;
A35: (2 to_power (n + 1)) + h < (2 to_power (n + 1)) + 0 by A30, XREAL_1:10;
reconsider i = i as Element of NAT by A30, INT_1:16;
A36: i < 2 to_power n by A9, XREAL_1:148, XXREAL_0:2;
A37: 2sComplement (n + 1),i = (n + 1) -BinarySequence (abs i) by Def2
.= (n + 1) -BinarySequence i by ABSVALUE:def 1 ;
then A38: (2sComplement (n + 1),i) . (n + 1) = FALSE by A36, BINARI_3:27;
n + 0 < n + 1 by XREAL_1:10;
then 2 to_power n < 2 to_power (n + 1) by POWER:44;
then A39: i < 2 to_power (n + 1) by A36, XXREAL_0:2;
A40: 1 <= n + 1 by NAT_1:11;
len (2sComplement (n + 1),h) = n + 1 by FINSEQ_1:def 18;
then A41: (2sComplement (n + 1),h) /. (n + 1) = (2sComplement (n + 1),h) . (n + 1) by A40, FINSEQ_4:24;
A42: (2sComplement (n + 1),h) . (n + 1) = ((n + 1) -BinarySequence (abs ((2 to_power (n + 1)) + h))) . (n + 1) by A30, A33, Def2
.= ((n + 1) -BinarySequence NH) . (n + 1) by ABSVALUE:def 1
.= TRUE by A35, A31, BINARI_3:30 ;
then A43: Intval (2sComplement (n + 1),h) = (Absval (2sComplement (n + 1),h)) - (2 to_power (n + 1)) by A41, BINARI_2:def 3
.= NH - (2 to_power (n + 1)) by A35, A34, BINARI_3:36
.= h ;
len (2sComplement (n + 1),i) = n + 1 by FINSEQ_1:def 18;
then A44: (2sComplement (n + 1),i) /. (n + 1) = (2sComplement (n + 1),i) . (n + 1) by A40, FINSEQ_4:24;
then A45: 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, A42, A41, BINARI_2:def 4
.= FALSE ;
A46: 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, A42, A44, A41, BINARI_2:def 5
.= FALSE ;
Intval (2sComplement (n + 1),i) = Absval (2sComplement (n + 1),i) by A38, A44, BINARI_2:def 3
.= i by A37, A39, BINARI_3:36 ;
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 A10, A43, A45, A46, 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;

A47: S₁[1]

proof

A48: abs (- 1) = - (- 1) by ABSVALUE:def 1
.= 1 ;
( 2 to_power 1 = 2 & ( for k being Nat st 2 to_power k >= 1 & k >= 1 holds
k >= 1 ) ) by POWER:30;
then MajP 1,(abs (- 1)) = 1 by A48, Def1;
then A49: 2sComplement 1,(- 1) = 1 -BinarySequence (abs ((2 to_power 1) + (- 1))) by 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 ;
assume that
A50: - (2 to_power (1 -' 1)) <= h and
A51: h <= (2 to_power (1 -' 1)) - 1 and
A52: - (2 to_power (1 -' 1)) <= i and
A53: i <= (2 to_power (1 -' 1)) - 1 and
- (2 to_power (1 -' 1)) <= h + i and
h + i <= (2 to_power (1 -' 1)) - 1 and
A54: ( ( h >= 0 & i < 0 ) or ( h < 0 & i >= 0 ) ) ; :: thesis: Intval ((2sComplement 1,h) + (2sComplement 1,i)) = h + i
A55: 1 -' 1 = 1 - 1 by XREAL_0:def 2
.= 0 ;
then A56: h <= 1 - 1 by A51, POWER:29;
A57: i <= 1 - 1 by A53, A55, POWER:29;
A58: - 1 <= i by A52, A55, POWER:29;
A59: 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 ;
A60: - 1 <= h by A50, A55, POWER:29;

now

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

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

then i <= - 1 by INT_1:21;
then A62: i = - 1 by A58, XXREAL_0:1;
h = 0 by A56, A61;
hence Intval ((2sComplement 1,h) + (2sComplement 1,i)) = h + i by A59, A49, A62, Th15, BINARI_3:18; :: thesis: verum

end;

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

then h <= - 1 by INT_1:21;
then A64: h = - 1 by A60, XXREAL_0:1;
i = 0 by A57, A63;
hence Intval ((2sComplement 1,h) + (2sComplement 1,i)) = h + i by A59, A49, A64, Th15, BINARI_3:18; :: thesis: verum

end;

end;

end;

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

end;

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