let h, i be Integer; :: thesis: for n being non zero 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 zero 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 zero Nat st S₁[n] holds
S₁[n + 1]

proof

let n be non zero 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 :: thesis: Intval ((2sComplement ((n + 1),h)) + (2sComplement ((n + 1),i))) = h + i

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:27
.= (- (2 to_power n)) + (2 * (2 to_power n)) by POWER:25
.= 2 to_power n ;
then A14: 2 to_power n <= (2 to_power (n + 1)) + i by A11, XREAL_1:6;
then reconsider NI = (2 to_power (n + 1)) + i as Element of NAT by INT_1:3;
n < n + 1 by XREAL_1:29;
then A15: 2 to_power n < 2 to_power (n + 1) by POWER:39;
|.i.| = - i by A13, ABSVALUE:def 1;
then |.i.| <= - (- (2 to_power n)) by A11, XREAL_1:24;
then A16: MajP ((n + 1),|.i.|) = n + 1 by A15, Th24, XXREAL_0:2;
then A17: 2sComplement ((n + 1),i) = (n + 1) -BinarySequence |.((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:8;
reconsider h = h as Element of NAT by A13, INT_1:3;
A19: h < 2 to_power n by A12, XREAL_1:146, XXREAL_0:2;
A20: 2sComplement ((n + 1),h) = (n + 1) -BinarySequence |.h.| by Def2
.= (n + 1) -BinarySequence h by ABSVALUE:def 1 ;
then A21: (2sComplement ((n + 1),h)) . (n + 1) = FALSE by A19, BINARI_3:26;
n + 0 < n + 1 by XREAL_1:8;
then 2 to_power n < 2 to_power (n + 1) by POWER:39;
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 CARD_1:def 7;
then A24: (2sComplement ((n + 1),i)) /. (n + 1) = (2sComplement ((n + 1),i)) . (n + 1) by A23, FINSEQ_4:15;
A25: (2sComplement ((n + 1),i)) . (n + 1) = ((n + 1) -BinarySequence |.((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:29 ;
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:35
.= i ;
len (2sComplement ((n + 1),h)) = n + 1 by CARD_1:def 7;
then A27: (2sComplement ((n + 1),h)) /. (n + 1) = (2sComplement ((n + 1),h)) . (n + 1) by A23, FINSEQ_4:15;
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:35 ;
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:12
.= ((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:27
.= (- (2 to_power n)) + (2 * (2 to_power n)) by POWER:25
.= 2 to_power n ;
then A31: 2 to_power n <= (2 to_power (n + 1)) + h by A8, XREAL_1:6;
then reconsider NH = (2 to_power (n + 1)) + h as Element of NAT by INT_1:3;
n < n + 1 by XREAL_1:29;
then A32: 2 to_power n < 2 to_power (n + 1) by POWER:39;
|.h.| = - h by A30, ABSVALUE:def 1;
then |.h.| <= - (- (2 to_power n)) by A8, XREAL_1:24;
then A33: MajP ((n + 1),|.h.|) = n + 1 by A32, Th24, XXREAL_0:2;
then A34: 2sComplement ((n + 1),h) = (n + 1) -BinarySequence |.((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:8;
reconsider i = i as Element of NAT by A30, INT_1:3;
A36: i < 2 to_power n by A9, XREAL_1:146, XXREAL_0:2;
A37: 2sComplement ((n + 1),i) = (n + 1) -BinarySequence |.i.| by Def2
.= (n + 1) -BinarySequence i by ABSVALUE:def 1 ;
then A38: (2sComplement ((n + 1),i)) . (n + 1) = FALSE by A36, BINARI_3:26;
n + 0 < n + 1 by XREAL_1:8;
then 2 to_power n < 2 to_power (n + 1) by POWER:39;
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 CARD_1:def 7;
then A41: (2sComplement ((n + 1),h)) /. (n + 1) = (2sComplement ((n + 1),h)) . (n + 1) by A40, FINSEQ_4:15;
A42: (2sComplement ((n + 1),h)) . (n + 1) = ((n + 1) -BinarySequence |.((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:29 ;
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:35
.= h ;
len (2sComplement ((n + 1),i)) = n + 1 by CARD_1:def 7;
then A44: (2sComplement ((n + 1),i)) /. (n + 1) = (2sComplement ((n + 1),i)) . (n + 1) by A40, FINSEQ_4:15;
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:35 ;
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:12
.= ((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: |.(- 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:25;
then MajP (1,|.(- 1).|) = 1 by A48, Def1;
then A49: 2sComplement (1,(- 1)) = 1 -BinarySequence |.((2 to_power 1) + (- 1)).| by Def2
.= 1 -BinarySequence |.(2 + (- 1)).| by POWER:25
.= 1 -BinarySequence 1 by ABSVALUE:def 1
.= (0 + 1) -BinarySequence (2 to_power 0) by POWER:24
.= (0* 0) ^ <*1*> by BINARI_3:28
.= <*TRUE*> by FINSEQ_1:34 ;
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:24;
A57: i <= 1 - 1 by A53, A55, POWER:24;
A58: - 1 <= i by A52, A55, POWER:24;
A59: 2sComplement (1,0) = 1 -BinarySequence |.0.| by Def2
.= 1 -BinarySequence 0 by ABSVALUE:def 1
.= 0* 1 by BINARI_3:25
.= <*FALSE*> by FINSEQ_2:59 ;
A60: - 1 <= h by A50, A55, POWER:24;

now :: thesis: Intval ((2sComplement (1,h)) + (2sComplement (1,i))) = h + i

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:8;
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:17; :: 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:8;
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:17; :: thesis: verum

end;

end;

end;

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

end;

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