let h, i be Integer; for n being non zero Nat st - (2 to_power ((n + 1) -' 1)) <= h + i & 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 zero Nat; ( - (2 to_power ((n + 1) -' 1)) <= h + i & 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 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 )
; Intval ((2sComplement ((n + 1),h)) + (2sComplement ((n + 1),i))) = h + i
A5: (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
;
(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:6;
A9:
- (2 to_power n) < i
by A2, A3, A6, Th9;
then A10:
0 <= (2 to_power (n + 1)) + i
by A5, XREAL_1:6;
0 <= (2 to_power (n + 1)) + h
by A7, A5, XREAL_1:6;
then reconsider NH = (2 to_power (n + 1)) + h, NI = (2 to_power (n + 1)) + i as Element of NAT by A10, INT_1:3;
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:29;
then A12:
2 to_power n < 2 to_power (n + 1)
by POWER:39;
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:8;
- h < - (- (2 to_power n))
by A7, XREAL_1:24;
then
|.h.| < 2 to_power n
by A2, ABSVALUE:def 1;
then A15:
MajP ((n + 1),|.h.|) = n + 1
by A12, Th24, XXREAL_0:2;
then A16: 2sComplement ((n + 1),h) =
(n + 1) -BinarySequence |.((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 CARD_1:def 7;
then A17: (2sComplement ((n + 1),h)) /. (n + 1) =
(2sComplement ((n + 1),h)) . (n + 1)
by A11, FINSEQ_4:15
.=
((n + 1) -BinarySequence |.((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:29
;
A18:
2 to_power n <= (2 to_power (n + 1)) + i
by A9, A5, XREAL_1:6;
A19:
(2 to_power (n + 1)) + i < (2 to_power (n + 1)) + 0
by A3, XREAL_1:8;
- i < - (- (2 to_power n))
by A9, XREAL_1:24;
then
|.i.| < 2 to_power n
by A3, ABSVALUE:def 1;
then A20:
MajP ((n + 1),|.i.|) = n + 1
by A12, Th24, XXREAL_0:2;
then A21: 2sComplement ((n + 1),i) =
(n + 1) -BinarySequence |.((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 CARD_1:def 7;
then A22: (2sComplement ((n + 1),i)) /. (n + 1) =
(2sComplement ((n + 1),i)) . (n + 1)
by A11, FINSEQ_4:15
.=
((n + 1) -BinarySequence |.((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:29
;
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:35
.=
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:35
.=
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:12
.=
((h + i) - 0) + 0
;
hence
Intval ((2sComplement ((n + 1),h)) + (2sComplement ((n + 1),i))) = h + i
; verum