let h, i be Integer; for n being non zero Nat st - (2 to_power n) <= h + i & h < 0 & i < 0 & - (2 to_power (n -' 1)) <= h & - (2 to_power (n -' 1)) <= i holds
(carry ((2sComplement ((n + 1),h)),(2sComplement ((n + 1),i)))) /. (n + 1) = TRUE
defpred S1[ Nat] means ( - (2 to_power $1) <= h + i & h < 0 & i < 0 & - (2 to_power ($1 -' 1)) <= h & - (2 to_power ($1 -' 1)) <= i implies (carry ((2sComplement (($1 + 1),h)),(2sComplement (($1 + 1),i)))) /. ($1 + 1) = TRUE );
A1:
for n being non zero Nat st S1[n] holds
S1[n + 1]
proof
let n be non
zero Nat;
( S1[n] implies S1[n + 1] )
assume
S1[
n]
;
S1[n + 1]
assume that
- (2 to_power (n + 1)) <= h + i
and A2:
h < 0
and A3:
i < 0
and A4:
- (2 to_power ((n + 1) -' 1)) <= h
and A5:
- (2 to_power ((n + 1) -' 1)) <= i
;
(carry ((2sComplement (((n + 1) + 1),h)),(2sComplement (((n + 1) + 1),i)))) /. ((n + 1) + 1) = TRUE
set H1 =
2sComplement (
((n + 1) + 1),
h);
set I1 =
2sComplement (
((n + 1) + 1),
i);
set H =
2sComplement (
(n + 1),
h);
set I =
2sComplement (
(n + 1),
i);
set T =
TRUE ;
set N =
n + 1;
A6:
(n + 1) -' 1
= (n + 1) - 1
by XREAL_0:def 2;
then A7:
2
to_power ((n + 1) -' 1) < 2
to_power (n + 1)
by POWER:39, XREAL_1:146;
(2 to_power ((n + 1) -' 1)) + (2 to_power ((n + 1) -' 1)) =
2
* (2 to_power ((n + 1) -' 1))
.=
(2 to_power 1) * (2 to_power ((n + 1) -' 1))
by POWER:25
.=
2
to_power (0 + (n + 1))
by A6, POWER:27
;
then A8:
(- (2 to_power ((n + 1) -' 1))) + (2 to_power (n + 1)) = 2
to_power ((n + 1) -' 1)
;
then A9:
2
to_power ((n + 1) -' 1) <= (2 to_power (n + 1)) + h
by A4, XREAL_1:6;
A10:
2
to_power ((n + 1) -' 1) <= (2 to_power (n + 1)) + i
by A5, A8, XREAL_1:6;
A11:
(2 to_power (n + 1)) + i < 0 + (2 to_power (n + 1))
by A3, XREAL_1:8;
(n + 1) - 1
= n
;
then A12:
(n + 1) -' 1
= n
by XREAL_0:def 2;
(
0 <= (2 to_power (n + 1)) + h &
0 <= (2 to_power (n + 1)) + i )
by A4, A5, A8, XREAL_1:6;
then reconsider NH =
(2 to_power (n + 1)) + h,
NI =
(2 to_power (n + 1)) + i as
Element of
NAT by INT_1:3;
A13:
len ((n + 1) -BinarySequence NI) = n + 1
by CARD_1:def 7;
A14:
1
<= n + 1
by NAT_1:11;
then A15:
(
(2sComplement (((n + 1) + 1),h)) /. (n + 1) = (2sComplement ((n + 1),h)) /. (n + 1) &
(2sComplement (((n + 1) + 1),i)) /. (n + 1) = (2sComplement ((n + 1),i)) /. (n + 1) )
by Th32;
A16:
(2 to_power (n + 1)) + h < 0 + (2 to_power (n + 1))
by A2, XREAL_1:8;
A17:
n + 1
< (n + 1) + 1
by NAT_1:13;
|.i.| = - i
by A3, ABSVALUE:def 1;
then
- (- (2 to_power ((n + 1) -' 1))) >= |.i.|
by A5, XREAL_1:24;
then
MajP (
(n + 1),
|.i.|)
= n + 1
by A7, Th24, XXREAL_0:2;
then A18:
(2sComplement ((n + 1),i)) /. (n + 1) =
((n + 1) -BinarySequence |.NI.|) /. (n + 1)
by A3, Def2
.=
((n + 1) -BinarySequence NI) /. (n + 1)
by ABSVALUE:def 1
.=
((n + 1) -BinarySequence NI) . (n + 1)
by A14, A13, FINSEQ_4:15
.=
TRUE
by A12, A10, A11, BINARI_3:29
;
A19:
len ((n + 1) -BinarySequence NH) = n + 1
by CARD_1:def 7;
|.h.| = - h
by A2, ABSVALUE:def 1;
then
- (- (2 to_power ((n + 1) -' 1))) >= |.h.|
by A4, XREAL_1:24;
then
MajP (
(n + 1),
|.h.|)
= n + 1
by A7, Th24, XXREAL_0:2;
then (2sComplement ((n + 1),h)) /. (n + 1) =
((n + 1) -BinarySequence |.NH.|) /. (n + 1)
by A2, Def2
.=
((n + 1) -BinarySequence NH) /. (n + 1)
by ABSVALUE:def 1
.=
((n + 1) -BinarySequence NH) . (n + 1)
by A14, A19, FINSEQ_4:15
.=
TRUE
by A12, A9, A16, BINARI_3:29
;
then (carry ((2sComplement (((n + 1) + 1),h)),(2sComplement (((n + 1) + 1),i)))) /. ((n + 1) + 1) =
((TRUE '&' TRUE) 'or' (TRUE '&' ((carry ((2sComplement (((n + 1) + 1),h)),(2sComplement (((n + 1) + 1),i)))) /. (n + 1)))) 'or' (TRUE '&' ((carry ((2sComplement (((n + 1) + 1),h)),(2sComplement (((n + 1) + 1),i)))) /. (n + 1)))
by A14, A18, A15, A17, BINARITH:def 2
.=
TRUE 'or' ((carry ((2sComplement (((n + 1) + 1),h)),(2sComplement (((n + 1) + 1),i)))) /. (n + 1))
;
hence
(carry ((2sComplement (((n + 1) + 1),h)),(2sComplement (((n + 1) + 1),i)))) /. ((n + 1) + 1) = TRUE
;
verum
end;
A20:
S1[1]
proof
1
-' 1
= 1
- 1
by XREAL_0:def 2;
then 3
div (2 to_power (1 -' 1)) =
(1 + 2) div 1
by POWER:24
.=
3
by NAT_2:4
;
then A21:
(3 div (2 to_power (1 -' 1))) mod 2 =
(2 + 1) mod 2
.=
((2 mod 2) + 1) mod 2
by NAT_D:22
.=
(0 + 1) mod 2
by NAT_D:25
.=
1
by PEPIN:5
;
A22:
(- 2) + 1
= - 1
;
set H =
2sComplement (2,
h);
set I =
2sComplement (2,
i);
set T =
TRUE ;
assume that A23:
- (2 to_power 1) <= h + i
and A24:
h < 0
and A25:
i < 0
and
- (2 to_power (1 -' 1)) <= h
and
- (2 to_power (1 -' 1)) <= i
;
(carry ((2sComplement ((1 + 1),h)),(2sComplement ((1 + 1),i)))) /. (1 + 1) = TRUE
A26:
i <= - 1
by A25, INT_1:8;
- (2 to_power 1) < h
by A23, A24, A25, Th9;
then
- 2
< h
by POWER:25;
then A27:
- 1
<= h
by A22, INT_1:7;
- (2 to_power 1) < i
by A23, A24, A25, Th9;
then
- 2
< i
by POWER:25;
then
- 1
<= i
by A22, INT_1:7;
then A28:
i = - 1
by A26, XXREAL_0:1;
A29:
1
in Seg 2
by FINSEQ_1:1;
A30: 2
to_power 2 =
2
|^ (1 + 1)
by POWER:41
.=
(2 |^ 1) + (2 |^ 1)
by PEPIN:29
.=
(2 to_power 1) + (2 |^ 1)
by POWER:41
.=
(2 to_power 1) + (2 to_power 1)
by POWER:41
.=
2
+ (2 to_power 1)
by POWER:25
.=
2
+ 2
by POWER:25
;
A31:
2
to_power 2
> 2
to_power 0
by POWER:39;
A32:
h <= - 1
by A24, INT_1:8;
then A33:
h = - 1
by A27, XXREAL_0:1;
then
|.h.| = - (- 1)
by ABSVALUE:def 1;
then
2
to_power 0 = |.h.|
by POWER:24;
then
MajP (2,
|.h.|)
= 2
by A31, Th24;
then |.((2 to_power (MajP (2,|.h.|))) + h).| =
|.(4 + (- 1)).|
by A27, A32, A30, XXREAL_0:1
.=
3
by ABSVALUE:def 1
;
then (2sComplement (2,h)) /. 1 =
(2 -BinarySequence 3) /. 1
by A24, Def2
.=
IFEQ (1,
0,
FALSE,
TRUE)
by A21, A29, BINARI_3:def 1
.=
TRUE
by FUNCOP_1:def 8
;
then (carry ((2sComplement (2,h)),(2sComplement (2,i)))) /. (1 + 1) =
((TRUE '&' TRUE) 'or' (TRUE '&' ((carry ((2sComplement (2,h)),(2sComplement (2,i)))) /. 1))) 'or' (TRUE '&' ((carry ((2sComplement (2,h)),(2sComplement (2,i)))) /. 1))
by A33, A28, BINARITH:def 2
.=
TRUE 'or' ((carry ((2sComplement (2,h)),(2sComplement (2,i)))) /. 1)
;
hence
(carry ((2sComplement ((1 + 1),h)),(2sComplement ((1 + 1),i)))) /. (1 + 1) = TRUE
;
verum
end;
thus
for n being non zero Nat holds S1[n]
from NAT_1:sch 10(A20, A1); verum