let h, i be Integer; for n being non empty 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 empty Nat st S1[n] holds
S1[n + 1]
proof
let n be non
empty 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:44, XREAL_1:148;
(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:30
.=
2
to_power (0 + (n + 1))
by A6, POWER:32
;
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:8;
A10:
2
to_power ((n + 1) -' 1) <= (2 to_power (n + 1)) + i
by A5, A8, XREAL_1:8;
A11:
(2 to_power (n + 1)) + i < 0 + (2 to_power (n + 1))
by A3, XREAL_1:10;
(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:8;
then reconsider NH =
(2 to_power (n + 1)) + h,
NI =
(2 to_power (n + 1)) + i as
Element of
NAT by INT_1:16;
A13:
len ((n + 1) -BinarySequence NI) = n + 1
by FINSEQ_1:def 18;
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:10;
A17:
n + 1
< (n + 1) + 1
by NAT_1:13;
abs i = - i
by A3, ABSVALUE:def 1;
then
- (- (2 to_power ((n + 1) -' 1))) >= abs i
by A5, XREAL_1:26;
then
MajP (n + 1),
(abs i) = n + 1
by A7, Th24, XXREAL_0:2;
then A18:
(2sComplement (n + 1),i) /. (n + 1) =
((n + 1) -BinarySequence (abs 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:24
.=
TRUE
by A12, A10, A11, BINARI_3:30
;
A19:
len ((n + 1) -BinarySequence NH) = n + 1
by FINSEQ_1:def 18;
abs h = - h
by A2, ABSVALUE:def 1;
then
- (- (2 to_power ((n + 1) -' 1))) >= abs h
by A4, XREAL_1:26;
then
MajP (n + 1),
(abs h) = n + 1
by A7, Th24, XXREAL_0:2;
then (2sComplement (n + 1),h) /. (n + 1) =
((n + 1) -BinarySequence (abs 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:24
.=
TRUE
by A12, A9, A16, BINARI_3:30
;
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 5
.=
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:29
.=
3
by NAT_2:6
;
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:21;
- (2 to_power 1) < h
by A23, A24, A25, Th9;
then
- 2
< h
by POWER:30;
then A27:
- 1
<= h
by A22, INT_1:20;
- (2 to_power 1) < i
by A23, A24, A25, Th9;
then
- 2
< i
by POWER:30;
then
- 1
<= i
by A22, INT_1:20;
then A28:
i = - 1
by A26, XXREAL_0:1;
A29:
1
in Seg 2
by FINSEQ_1:3;
A30: 2
to_power 2 =
2
|^ (1 + 1)
by POWER:46
.=
(2 |^ 1) + (2 |^ 1)
by PEPIN:30
.=
(2 to_power 1) + (2 |^ 1)
by POWER:46
.=
(2 to_power 1) + (2 to_power 1)
by POWER:46
.=
2
+ (2 to_power 1)
by POWER:30
.=
2
+ 2
by POWER:30
;
A31:
2
to_power 2
> 2
to_power 0
by POWER:44;
A32:
h <= - 1
by A24, INT_1:21;
then A33:
h = - 1
by A27, XXREAL_0:1;
then
abs h = - (- 1)
by ABSVALUE:def 1;
then
2
to_power 0 = abs h
by POWER:29;
then
MajP 2,
(abs h) = 2
by A31, Th24;
then abs ((2 to_power (MajP 2,(abs h))) + h) =
abs (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 5
.=
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 empty Nat holds S1[n]
from NAT_1:sch 10(A20, A1); verum