let h, i be Integer; :: thesis: 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:
S1[1]
proof
assume A2:
(
- (2 to_power 1) <= h + i &
h < 0 &
i < 0 &
- (2 to_power (1 -' 1)) <= h &
- (2 to_power (1 -' 1)) <= i )
;
:: thesis: (carry (2sComplement (1 + 1),h),(2sComplement (1 + 1),i)) /. (1 + 1) = TRUE
then
(
- (2 to_power 1) < h &
- (2 to_power 1) < i )
by Th9;
then A3:
(
- 2
< h &
- 2
< i )
by POWER:30;
(- 2) + 1
= - 1
;
then A4:
(
- 1
<= h &
- 1
<= i )
by A3, INT_1:20;
A5:
(
h <= - 1 &
i <= - 1 )
by A2, INT_1:21;
then A6:
(
h = - 1 &
i = - 1 )
by A4, XXREAL_0:1;
then
(
abs h = - (- 1) &
abs i = - (- 1) )
by ABSVALUE:def 1;
then
( 2
to_power 0 = abs h & 2
to_power 2
> 2
to_power 0 )
by POWER:29, POWER:44;
then A7:
MajP 2,
(abs h) = 2
by Th24;
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
;
then A8:
abs ((2 to_power (MajP 2,(abs h))) + h) =
abs (4 + (- 1))
by A4, A5, A7, XXREAL_0:1
.=
3
by ABSVALUE:def 1
;
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 A9:
(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
;
A10:
1
in Seg 2
by FINSEQ_1:3;
A11:
(2sComplement 2,h) /. 1 =
(2 -BinarySequence 3) /. 1
by A2, A8, Def2
.=
IFEQ 1,
0 ,
FALSE ,
TRUE
by A9, A10, BINARI_3:def 1
.=
TRUE
by FUNCOP_1:def 8
;
set H =
2sComplement 2,
h;
set I =
2sComplement 2,
i;
set T =
TRUE ;
(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 A6, A11, 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
;
:: thesis: verum
end;
A12:
for n being non empty Nat st S1[n] holds
S1[n + 1]
proof
let n be non
empty Nat;
:: thesis: ( S1[n] implies S1[n + 1] )
assume
S1[
n]
;
:: thesis: S1[n + 1]
assume A13:
(
- (2 to_power (n + 1)) <= h + i &
h < 0 &
i < 0 &
- (2 to_power ((n + 1) -' 1)) <= h &
- (2 to_power ((n + 1) -' 1)) <= i )
;
:: thesis: (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;
A14:
(n + 1) - 1
= n
;
A15:
(n + 1) -' 1
= (n + 1) - 1
by XREAL_0:def 2;
A16:
(n + 1) -' 1
= n
by A14, XREAL_0:def 2;
A17:
2
to_power ((n + 1) -' 1) < 2
to_power (n + 1)
by A15, 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 A15, POWER:32
;
then A18:
(- (2 to_power ((n + 1) -' 1))) + (2 to_power (n + 1)) = 2
to_power ((n + 1) -' 1)
;
(
abs h = - h &
abs i = - i )
by A13, ABSVALUE:def 1;
then
(
- (- (2 to_power ((n + 1) -' 1))) >= abs h &
- (- (2 to_power ((n + 1) -' 1))) >= abs i )
by A13, XREAL_1:26;
then A19:
(
MajP (n + 1),
(abs h) = n + 1 &
MajP (n + 1),
(abs i) = n + 1 )
by A17, Th24, XXREAL_0:2;
A20:
( 2
to_power ((n + 1) -' 1) <= (2 to_power (n + 1)) + h & 2
to_power ((n + 1) -' 1) <= (2 to_power (n + 1)) + i )
by A13, A18, XREAL_1:8;
(
0 <= (2 to_power (n + 1)) + h &
0 <= (2 to_power (n + 1)) + i )
by A13, A18, 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;
A21:
( 1
<= n + 1 &
len ((n + 1) -BinarySequence NH) = n + 1 &
len ((n + 1) -BinarySequence NI) = n + 1 )
by FINSEQ_1:def 18, NAT_1:11;
A22:
(
(2 to_power (n + 1)) + h < 0 + (2 to_power (n + 1)) &
(2 to_power (n + 1)) + i < 0 + (2 to_power (n + 1)) )
by A13, XREAL_1:10;
A23:
(2sComplement (n + 1),h) /. (n + 1) =
((n + 1) -BinarySequence (abs NH)) /. (n + 1)
by A13, A19, Def2
.=
((n + 1) -BinarySequence NH) /. (n + 1)
by ABSVALUE:def 1
.=
((n + 1) -BinarySequence NH) . (n + 1)
by A21, FINSEQ_4:24
.=
TRUE
by A16, A20, A22, BINARI_3:30
;
A24:
(2sComplement (n + 1),i) /. (n + 1) =
((n + 1) -BinarySequence (abs NI)) /. (n + 1)
by A13, A19, Def2
.=
((n + 1) -BinarySequence NI) /. (n + 1)
by ABSVALUE:def 1
.=
((n + 1) -BinarySequence NI) . (n + 1)
by A21, FINSEQ_4:24
.=
TRUE
by A16, A20, A22, BINARI_3:30
;
A25:
(
(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 A21, Th32;
n + 1
< (n + 1) + 1
by NAT_1:13;
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 A21, A23, A24, A25, 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
;
:: thesis: verum
end;
thus
for n being non empty Nat holds S1[n]
from NAT_1:sch 10(A1, A12); :: thesis: verum