Copyright (c) 2003 Association of Mizar Users
environ
vocabulary ARYTM_1, NAT_1, INT_1, RADIX_1, FINSEQ_1, POWER, MIDSP_3, FINSEQ_4,
GROUP_1, RELAT_1, RLVECT_1, FUNCT_1, RADIX_5;
notation TARSKI, SUBSET_1, XCMPLX_0, XREAL_0, NAT_1, BINARITH, RADIX_1, POWER,
MIDSP_3, FINSEQ_4, FINSEQ_1, FUNCT_1, WSIERP_1;
constructors RADIX_1, BINARITH, POWER, FINSEQ_4, EULER_2;
clusters REAL_1, NUMBERS, XREAL_0, INT_1, RELSET_1;
requirements REAL, NUMERALS, SUBSET, BOOLE, ARITHM;
definitions TARSKI;
theorems RADIX_1, RADIX_4, AXIOMS, REAL_1, REAL_2, INT_1, NAT_1, XCMPLX_1,
SCMFSA_7, FINSEQ_1, JORDAN3, POWER, GOBOARD9, FINSEQ_2, NEWTON, RADIX_2,
NAT_2, PREPOWER, GR_CY_1, GROUP_4, BINARITH, PEPIN, JORDAN4, JORDAN5B,
FUNCT_1, FINSEQ_4, RVSUM_1, XCMPLX_0;
schemes BINOM, FINSEQ_2, INT_2;
begin :: Some Useful Theorems
theorem Lm1:
for k be Nat st k >= 2 holds Radix(k) - 1 in k-SD
proof
let k be Nat;
assume
A1: k >= 2;
A2: k-SD = {w where w is Element of INT:w <= Radix(k)-1 & w >= -Radix(k)+1}
by RADIX_1:def 2;
Radix(k) > 2 by A1,RADIX_4:1; then
Radix(k) > 1 by AXIOMS:22; then
Radix(k) + Radix(k) > 1 + 1 by REAL_1:67; then
Radix(k) - 1 > 0 + 1 - Radix(k) by REAL_2:169; then
A4: Radix(k) - 1 > -Radix(k) + 1 + 0 by XCMPLX_1:155;
Radix(k) - 1 is Element of INT by INT_1:def 2;
hence thesis by A2,A4;
end;
Lm2:
for k be Nat holds Radix(k) > 0 by RADIX_2:6;
theorem Th1:
for i,n be Nat st i > 1 & i in Seg n holds
i -' 1 in Seg n
proof
let i,n be Nat;
assume
A1: i > 1 & i in Seg n; then
i - 1 > 1 - 1 by REAL_1:54; then
i -' 1 > 0 by A1,SCMFSA_7:3; then
A2: i -' 1 >= 0 + 1 by NAT_1:38;
i >= 1 & i <= n by A1,FINSEQ_1:3; then
i -' 1 <= n by JORDAN3:7;
hence thesis by A2,FINSEQ_1:3;
end;
reserve k for Nat;
theorem Th2:
for k be Nat st 2 <= k holds 4 <= Radix(k)
proof
defpred P[Nat] means 4 <= Radix($1);
Radix(2) = 2 to_power (1+1) by RADIX_1:def 1
.= 2 to_power 1 * 2 to_power 1 by POWER:32
.= 2 * (2 to_power 1) by POWER:30
.= 2 * 2 by POWER:30;
then
A1: P[2];
A2: for kk be Nat st kk >= 2 & P[kk] holds P[kk + 1]
proof
let kk be Nat;
assume
A6: 2 <= kk & 4 <= Radix(kk);
A7: Radix(kk + 1) = 2 to_power (kk + 1) by RADIX_1:def 1
.= 2 to_power (1) * 2 to_power (kk) by POWER:32
.= 2 * 2 to_power (kk) by POWER:30
.= 2 * Radix(kk) by RADIX_1:def 1;
Radix(kk) >= 0 by A6,AXIOMS:22; then
Radix(kk + 1) >= Radix(kk) by A7,REAL_2:146;
hence thesis by A6, AXIOMS:22;
end;
for i being Nat st 2 <= i holds P[i] from Ind2(A1,A2);
hence thesis;
end;
theorem Th3:
for k be Nat, tx be Tuple of 1,k-SD holds
SDDec(tx) = DigA(tx,1)
proof
let k be Nat, tx be Tuple of 1,k-SD;
A3: 1 in Seg 1 by FINSEQ_1:3; then
A4: (DigitSD(tx))/.1 = SubDigit(tx,1,k) by RADIX_1:def 6
.= ( Radix(k) |^ (1-'1) )*DigB(tx,1) by RADIX_1:def 5
.= (Radix(k) |^ (1-'1))*DigA(tx,1) by RADIX_1:def 4
.= (Radix(k) |^ 0)*DigA(tx,1) by GOBOARD9:1
.= 1 * DigA(tx,1) by NEWTON:9;
A5: len DigitSD(tx) = 1 by FINSEQ_2:109; then
1 in dom DigitSD(tx) by A3,FINSEQ_1:def 3; then
A6: DigitSD(tx).1 = DigA(tx,1) by FINSEQ_4:def 4,A4;
reconsider w = DigA(tx,1) as Element of INT by INT_1:def 2;
SDDec(tx) = Sum DigitSD(tx) by RADIX_1:def 7
.= Sum <*w*> by A5,A6,FINSEQ_1:57
.= DigA(tx,1) by RVSUM_1:103;
hence thesis;
end;
begin :: Properties of Primary Radix-$2^k$ SD Number
theorem Th4:
for i,k,n be Nat st i in Seg n holds
DigA(DecSD(0,n,k),i) = 0
proof
let i,k,n be Nat;
assume
A1: i in Seg n;
A2: Radix(k) > 0 by Lm2;
A3: i >= 1 by A1,FINSEQ_1:3;
DigA(DecSD(0,n,k),i)
= DigitDC(0,i,k) by A1,RADIX_1:def 9
.= (0 mod (Radix(k) |^ i)) div (Radix(k) |^ (i-'1)) by RADIX_1:def 8
.= (0 div (Radix(k) |^ (i-'1))) mod Radix(k) by A2,A3,RADIX_2:4
.= 0 mod Radix(k) by NAT_2:4;
hence thesis by GR_CY_1:6;
end;
theorem
for n,k be Nat st n >= 1 holds
SDDec(DecSD(0,n,k)) = 0
proof
let n,k be Nat;
assume
A1: n >= 1;
Radix(k) > 0 by Lm2; then
Radix(k) >= 0 + 1 by INT_1:20; then
Radix(k) |^ n >= 1 by PREPOWER:19; then
Radix(k) |^ n > 0 by AXIOMS:22; then
0 is_represented_by n,k by RADIX_1:def 12;
hence thesis by A1,RADIX_1:25;
end;
theorem Th6:
for k,n be Nat st 1 in Seg n & k >= 2 holds
DigA(DecSD(1,n,k),1) = 1
proof
let k,n be Nat;
assume
A1: 1 in Seg n & k >= 2; then
Radix(k) > 2 by RADIX_4:1; then
A2: Radix(k) > 1 by AXIOMS:22; then
A3: Radix(k) > 0 by AXIOMS:22;
DigA(DecSD(1,n,k),1)
= DigitDC(1,1,k) by A1,RADIX_1:def 9
.= (1 mod (Radix(k) |^ 1)) div (Radix(k) |^ (1-'1)) by RADIX_1:def 8
.= (1 div (Radix(k) |^ (1-'1))) mod Radix(k) by A3,RADIX_2:4
.= (1 div (Radix(k) |^ 0)) mod Radix(k) by NAT_2:10
.= (1 div 1) mod Radix(k) by NEWTON:9
.= 1 mod Radix(k) by NAT_2:6;
hence thesis by A2,GROUP_4:102;
end;
theorem Th7:
for i,k,n be Nat st i in Seg n & i > 1 & k >= 2 holds
DigA(DecSD(1,n,k),i) = 0
proof
let i,k,n be Nat;
assume
A1: i in Seg n & i > 1 & k >= 2; then
Radix(k) > 2 by RADIX_4:1; then
A2: Radix(k) > 1 by AXIOMS:22; then
A3: Radix(k) > 0 by AXIOMS:22;
A4: DigA(DecSD(1,n,k),i)
= DigitDC(1,i,k) by A1,RADIX_1:def 9
.=(1 mod (Radix(k) |^ i)) div (Radix(k) |^ (i-'1)) by RADIX_1:def 8
.=(1 div (Radix(k) |^ (i-'1))) mod Radix(k) by A1,A3,RADIX_2:4;
i-1 > 1 - 1 by A1,REAL_1:92; then
i-'1 > 0 by BINARITH:def 3; then
(Radix(k) |^ (i-'1)) > 1 by A2,PEPIN:26; then
1 div (Radix(k) |^ (i-'1)) = 0 by JORDAN4:5;
hence thesis by A4,GR_CY_1:6;
end;
theorem
for n,k be Nat st n >= 1 & k >= 2 holds
SDDec(DecSD(1,n,k)) = 1
proof
let n,k be Nat;
assume
A1: n >= 1 & k >= 2; then
A2: Radix(k) > 2 by RADIX_4:1;
Radix(k) > 0 by Lm2; then
Radix(k) >= 0 + 1 by INT_1:20; then
Radix(k) |^ n >= Radix(k) by A1,PREPOWER:20; then
Radix(k) |^ n >= 2 by A2,AXIOMS:22; then
Radix(k) |^ n > 1 by AXIOMS:22; then
1 is_represented_by n,k by RADIX_1:def 12;
hence thesis by A1,RADIX_1:25;
end;
theorem Th9:
for k be Nat st k >= 2 holds SD_Add_Carry(Radix(k)) = 1
proof
let k be Nat;
assume k >= 2; then
Radix(k) > 2 by RADIX_4:1;
hence thesis by RADIX_1:def 10;
end;
theorem Th10:
for k be Nat st k >= 2 holds SD_Add_Data(Radix(k),k) = 0
proof
let k be Nat;
assume k >= 2; then
A1: SD_Add_Carry(Radix(k)) = 1 by Th9;
SD_Add_Data(Radix(k),k)
= Radix(k) - SD_Add_Carry(Radix(k)) * Radix(k) by RADIX_1:def 11
.= Radix(k) - Radix(k) by A1;
hence thesis by XCMPLX_1:14;
end;
begin :: Primary Magnitude Relation of Radix-2^k SD Number
Lm5:
for k be Nat st 2 <= k holds SD_Add_Carry(Radix(k) - 1) = 1
proof
let k be Nat;
assume k >= 2; then
Radix(k) >= 4 by Th2; then
Radix(k) - 1 >= 4 - 1 by REAL_1:49; then
Radix(k) - 1 > 2 by AXIOMS:22;
hence thesis by RADIX_1:def 10;
end;
Lm6:
for n,k,i be Nat st k >= 2 & i in Seg n holds
SD_Add_Carry(DigA(DecSD(1,n,k),i)) = 0
proof
let n,k,i be Nat;
assume
A1: k >= 2 & i in Seg n; then
A2: i >= 1 by FINSEQ_1:3;
now per cases by A2,REAL_1:def 5;
suppose
i = 1; then
SD_Add_Carry(DigA(DecSD(1,n,k),i))
= SD_Add_Carry(1) by A1,Th6;
hence thesis by RADIX_1:def 10;
suppose
i > 1; then
SD_Add_Carry(DigA(DecSD(1,n,k),i))
= SD_Add_Carry(0) by A1,Th7;
hence thesis by RADIX_1:def 10;
end;
hence thesis;
end;
theorem Th11:
for n be Nat st n >= 1 holds
for k be Nat, tx,ty be Tuple of n,k-SD st
(for i be Nat st i in Seg n holds DigA(tx,i) = DigA(ty,i)) holds
SDDec(tx) = SDDec(ty)
proof
defpred P[Nat] means
for k be Nat, tx,ty be Tuple of $1,k-SD st
(for i be Nat st i in Seg $1 holds DigA(tx,i) = DigA(ty,i)) holds
SDDec(tx) = SDDec(ty);
A1: P[1]
proof
let k be Nat, tx,ty be Tuple of 1,k-SD;
assume
A2: for i be Nat st i in Seg 1 holds DigA(tx,i) = DigA(ty,i);
A3: 1 in Seg 1 by FINSEQ_1:3;
A4: SDDec(tx) = DigA(tx,1) by Th3;
SDDec(ty) = DigA(ty,1) by Th3;
hence thesis by A2,A3,A4;
end;
A10: for n be Nat st n >= 1 & P[n] holds P[n+1]
proof
let n be Nat;
assume
A11: n >= 1 & P[n];
let k be Nat, tx,ty be Tuple of (n+1),k-SD;
assume
A12: for i be Nat st i in Seg (n+1) holds DigA(tx,i) = DigA(ty,i);
deffunc F(Nat) = DigB(tx,$1);
consider txn being FinSequence of INT such that
A13: len txn = n and
A14: for i be Nat st i in Seg n holds txn.i = F(i) from SeqLambdaD;
rng txn c= k-SD
proof
let z be set;
assume z in rng txn; then
consider xx be set such that
A16: xx in dom txn and
A17: z = txn.xx by FUNCT_1:def 5;
reconsider xx as Nat by A16;
A18: dom txn = Seg n by FINSEQ_1:def 3,A13; then
A19: z = DigB(tx,xx) by A14,A16,A17
.= DigA(tx,xx) by RADIX_1:def 4;
xx in Seg (n+1) by A16,A18,FINSEQ_2:9; then
DigA(tx,xx) is Element of k-SD by RADIX_1:19;
hence thesis by A19;
end;
then reconsider txn as FinSequence of k-SD by FINSEQ_1:def 4;
A20: for i be Nat st i in Seg n holds txn.i = tx.i
proof
let i be Nat;
assume
A21: i in Seg n; then
A22: i in Seg (n+1) by FINSEQ_2:9;
txn.i = DigB(tx,i) by A14,A21
.= DigA(tx,i) by RADIX_1:def 4;
hence thesis by A22,RADIX_1:def 3;
end;
deffunc F(Nat) = DigB(ty,$1);
consider tyn being FinSequence of INT such that
A23: len tyn = n and
A24: for i be Nat st i in Seg n holds tyn.i = F(i) from SeqLambdaD;
rng tyn c= k-SD
proof
let z be set;
assume z in rng tyn; then
consider yy be set such that
A26: yy in dom tyn and
A27: z = tyn.yy by FUNCT_1:def 5;
reconsider yy as Nat by A26;
A28: dom tyn = Seg n by FINSEQ_1:def 3,A23; then
A29: z = DigB(ty,yy) by A24,A26,A27
.= DigA(ty,yy) by RADIX_1:def 4;
yy in Seg (n+1) by A26,A28,FINSEQ_2:9; then
DigA(ty,yy) is Element of k-SD by RADIX_1:19;
hence thesis by A29;
end;
then reconsider tyn as FinSequence of k-SD by FINSEQ_1:def 4;
A30: for i be Nat st i in Seg n holds tyn.i = ty.i
proof
let i be Nat;
assume
A31: i in Seg n; then
A32: i in Seg (n+1) by FINSEQ_2:9;
tyn.i = DigB(ty,i) by A24,A31
.= DigA(ty,i) by RADIX_1:def 4;
hence thesis by A32,RADIX_1:def 3;
end;
reconsider txn as Tuple of n,k-SD by A13,FINSEQ_2:110;
reconsider tyn as Tuple of n,k-SD by A23,FINSEQ_2:110;
A33: SDDec(txn) + (Radix(k) |^ n)*DigA(tx,n+1) = SDDec(tx) by A20,RADIX_2:10;
A34: SDDec(tyn) + (Radix(k) |^ n)*DigA(ty,n+1) = SDDec(ty) by A30,RADIX_2:10;
for i be Nat st i in Seg n holds DigA(txn,i) = DigA(tyn,i)
proof
let i be Nat;
assume
A35: i in Seg n; then
A36: DigA(txn,i) = txn.i by RADIX_1:def 3
.= DigB(tx,i) by A14,A35
.= DigA(tx,i) by RADIX_1:def 4;
A37: DigA(tyn,i) = tyn.i by A35,RADIX_1:def 3
.= DigB(ty,i) by A24,A35
.= DigA(ty,i) by RADIX_1:def 4;
i in Seg (n+1) by A35,FINSEQ_2:9;
hence thesis by A12,A36,A37;
end;
then
A38: SDDec(txn) = SDDec(tyn) by A11;
(n+1) in Seg (n+1) by FINSEQ_1:6; then
SDDec(tx) = SDDec(tyn) + (Radix(k) |^ n)*DigA(ty,n+1) by A12,A33,A38;
hence thesis by A34;
end;
for n be Nat st n >= 1 holds P[n] from Ind1(A1,A10);
hence thesis;
end;
theorem
for n be Nat st n >= 1 holds
for k be Nat, tx,ty be Tuple of n,k-SD st
(for i be Nat st i in Seg n holds DigA(tx,i) >= DigA(ty,i)) holds
SDDec(tx) >= SDDec(ty)
proof
defpred P[Nat] means
for k be Nat, tx,ty be Tuple of $1,k-SD st
(for i be Nat st i in Seg $1 holds DigA(tx,i) >= DigA(ty,i)) holds
SDDec(tx) >= SDDec(ty);
A1: P[1]
proof
let k be Nat, tx,ty be Tuple of 1,k-SD;
assume
A2: for i be Nat st i in Seg 1 holds DigA(tx,i) >= DigA(ty,i);
A3: 1 in Seg 1 by FINSEQ_1:3;
A4: SDDec(tx) = DigA(tx,1) by Th3;
SDDec(ty) = DigA(ty,1) by Th3;
hence thesis by A2,A3,A4;
end;
A10: for n be Nat st n >= 1 & P[n] holds P[n+1]
proof
let n be Nat;
assume
A11: n >= 1 & P[n];
let k be Nat, tx,ty be Tuple of (n+1),k-SD;
assume
A12: for i be Nat st i in Seg (n+1) holds DigA(tx,i) >= DigA(ty,i);
deffunc F(Nat) = DigB(tx,$1);
consider txn being FinSequence of INT such that
A13: len txn = n and
A14: for i be Nat st i in Seg n holds txn.i = F(i) from SeqLambdaD;
rng txn c= k-SD
proof
let z be set;
assume z in rng txn; then
consider xx be set such that
A16: xx in dom txn and
A17: z = txn.xx by FUNCT_1:def 5;
reconsider xx as Nat by A16;
A18: dom txn = Seg n by FINSEQ_1:def 3,A13; then
A19: z = DigB(tx,xx) by A14,A16,A17
.= DigA(tx,xx) by RADIX_1:def 4;
xx in Seg (n+1) by A16,A18,FINSEQ_2:9; then
DigA(tx,xx) is Element of k-SD by RADIX_1:19;
hence thesis by A19;
end;
then reconsider txn as FinSequence of k-SD by FINSEQ_1:def 4;
A20: for i be Nat st i in Seg n holds txn.i = tx.i
proof
let i be Nat;
assume
A21: i in Seg n; then
A22: i in Seg (n+1) by FINSEQ_2:9;
txn.i = DigB(tx,i) by A14,A21
.= DigA(tx,i) by RADIX_1:def 4;
hence thesis by A22,RADIX_1:def 3;
end;
deffunc F(Nat) = DigB(ty,$1);
consider tyn being FinSequence of INT such that
A23: len tyn = n and
A24: for i be Nat st i in Seg n holds tyn.i = F(i) from SeqLambdaD;
rng tyn c= k-SD
proof
let z be set;
assume z in rng tyn; then
consider yy be set such that
A26: yy in dom tyn and
A27: z = tyn.yy by FUNCT_1:def 5;
reconsider yy as Nat by A26;
A28: dom tyn = Seg n by FINSEQ_1:def 3,A23; then
A29: z = DigB(ty,yy) by A24,A26,A27
.= DigA(ty,yy) by RADIX_1:def 4;
yy in Seg (n+1) by A26,A28,FINSEQ_2:9; then
DigA(ty,yy) is Element of k-SD by RADIX_1:19;
hence thesis by A29;
end;
then reconsider tyn as FinSequence of k-SD by FINSEQ_1:def 4;
A30: for i be Nat st i in Seg n holds tyn.i = ty.i
proof
let i be Nat;
assume
A31: i in Seg n; then
A32: i in Seg (n+1) by FINSEQ_2:9;
tyn.i = DigB(ty,i) by A24,A31
.= DigA(ty,i) by RADIX_1:def 4;
hence thesis by A32,RADIX_1:def 3;
end;
reconsider txn as Tuple of n,k-SD by A13,FINSEQ_2:110;
reconsider tyn as Tuple of n,k-SD by A23,FINSEQ_2:110;
A33: SDDec(txn) + (Radix(k) |^ n)*DigA(tx,n+1) = SDDec(tx) by A20,RADIX_2:10;
A34: SDDec(tyn) + (Radix(k) |^ n)*DigA(ty,n+1) = SDDec(ty) by A30,RADIX_2:10;
for i be Nat st i in Seg n holds DigA(txn,i) >= DigA(tyn,i)
proof
let i be Nat;
assume
A35: i in Seg n; then
A36: DigA(txn,i) = txn.i by RADIX_1:def 3
.= DigB(tx,i) by A14,A35
.= DigA(tx,i) by RADIX_1:def 4;
A37: DigA(tyn,i) = tyn.i by A35,RADIX_1:def 3
.= DigB(ty,i) by A24,A35
.= DigA(ty,i) by RADIX_1:def 4;
i in Seg (n+1) by A35,FINSEQ_2:9;
hence thesis by A12,A36,A37;
end;
then
A38: SDDec(txn) >= SDDec(tyn) by A11;
(n+1) in Seg (n+1) by FINSEQ_1:6; then
A39: DigA(tx,n+1) >= DigA(ty,n+1) by A12;
Radix(k) > 0 by Lm2; then
(Radix(k) |^ n) > 0 by PREPOWER:13; then
(Radix(k) |^ n)*DigA(tx,n+1) >= (Radix(k) |^ n)*DigA(ty,n+1)
by A39,AXIOMS:25;
hence thesis by A33,A34,A38,REAL_1:55;
end;
for n be Nat st n >= 1 holds P[n] from Ind1(A1,A10);
hence thesis;
end;
theorem Th13:
for n be Nat st n >= 1 holds
for k be Nat st k >= 2 holds
for tx,ty,tz,tw be Tuple of n,k-SD st
(for i be Nat st i in Seg n holds
(DigA(tx,i) = DigA(tz,i) & DigA(ty,i) = DigA(tw,i))
or (DigA(ty,i) = DigA(tz,i) & DigA(tx,i) = DigA(tw,i))) holds
SDDec(tz) + SDDec(tw) = SDDec(tx) + SDDec(ty)
proof
defpred P[Nat] means
for k be Nat st k >= 2 holds
for tx,ty,tz,tw be Tuple of $1,k-SD st
(for i be Nat st i in Seg $1 holds
(DigA(tx,i) = DigA(tz,i) & DigA(ty,i) = DigA(tw,i))
or (DigA(ty,i) = DigA(tz,i) & DigA(tx,i) = DigA(tw,i))) holds
SDDec(tz) + SDDec(tw) = SDDec(tx) + SDDec(ty);
A1: P[1]
proof
let k be Nat;
assume
A2: k >= 2;
let tx,ty,tz,tw be Tuple of 1,k-SD;
assume
A3: for j be Nat st j in Seg 1 holds
(DigA(tx,j) = DigA(tz,j) & DigA(ty,j) = DigA(tw,j))
or (DigA(ty,j) = DigA(tz,j) & DigA(tx,j) = DigA(tw,j));
A4: 1 in Seg 1 by FINSEQ_1:3;
A5: SDDec(tz '+' tw) = DigA(tz '+' tw,1) by Th3
.= Add(tz,tw,1,k) by A4,RADIX_1:def 14
.= SD_Add_Data(DigA(tz,1)+DigA(tw,1),k)
+ SD_Add_Carry(DigA(tz,1-'1)+DigA(tw,1-'1)) by A2,A4,RADIX_1:def 13
.= SD_Add_Data(DigA(tz,1)+DigA(tw,1),k)
+ SD_Add_Carry(DigA(tz,0)+DigA(tw,1-'1)) by GOBOARD9:1
.= SD_Add_Data(DigA(tz,1)+DigA(tw,1),k)
+ SD_Add_Carry(DigA(tz,0)+DigA(tw,0)) by GOBOARD9:1
.= SD_Add_Data(DigA(tz,1)+DigA(tw,1),k)
+ SD_Add_Carry(DigA(tz,0)+0) by RADIX_1:def 3
.= SD_Add_Data(DigA(tz,1)+DigA(tw,1),k)
+ SD_Add_Carry(0+0) by RADIX_1:def 3
.= SD_Add_Data(DigA(tz,1)+DigA(tw,1),k) + 0 by RADIX_1:def 10;
A6: SDDec(tx '+' ty) = DigA(tx '+' ty,1) by Th3
.= Add(tx,ty,1,k) by A4,RADIX_1:def 14
.= SD_Add_Data(DigA(tx,1)+DigA(ty,1),k)
+ SD_Add_Carry(DigA(tx,1-'1)+DigA(ty,1-'1)) by A2,A4,RADIX_1:def 13
.= SD_Add_Data(DigA(tx,1)+DigA(ty,1),k)
+ SD_Add_Carry(DigA(tx,0)+DigA(ty,1-'1)) by GOBOARD9:1
.= SD_Add_Data(DigA(tx,1)+DigA(ty,1),k)
+ SD_Add_Carry(DigA(tx,0)+DigA(ty,0)) by GOBOARD9:1
.= SD_Add_Data(DigA(tx,1)+DigA(ty,1),k)
+ SD_Add_Carry(DigA(tx,0)+0) by RADIX_1:def 3
.= SD_Add_Data(DigA(tx,1)+DigA(ty,1),k)
+ SD_Add_Carry(0+0) by RADIX_1:def 3
.= SD_Add_Data(DigA(tx,1)+DigA(ty,1),k) + 0 by RADIX_1:def 10;
A7: DigA(tx,1) = DigA(tz,1) & DigA(ty,1) = DigA(tw,1)
or DigA(ty,1) = DigA(tz,1) & DigA(tx,1) = DigA(tw,1) by A3,A4;
A8: DigA(tx,1) = DigA(tz,1) & DigA(ty,1) = DigA(tw,1) implies
SDDec(tz) + SDDec(tw) = SDDec(tx) + SDDec(ty)
proof
assume
A9: DigA(tx,1) = DigA(tz,1) & DigA(ty,1) = DigA(tw,1);
SDDec(tz) + SDDec(tw)
= (SDDec(tx '+' ty))
+ (SD_Add_Carry(DigA(tx,1)+DigA(ty,1))*(Radix(k) |^ 1))
by A2,A5,A6,A9,RADIX_2:11;
hence thesis by A2,RADIX_2:11;
end;
DigA(ty,1) = DigA(tz,1) & DigA(tx,1) = DigA(tw,1) implies
SDDec(tz) + SDDec(tw) = SDDec(tx) + SDDec(ty)
proof
assume
DigA(ty,1) = DigA(tz,1) & DigA(tx,1) = DigA(tw,1);
SDDec(tz) + SDDec(tw)
= (SDDec(tx '+' ty))
+ SD_Add_Carry(DigA(tx,1)+DigA(ty,1))*(Radix(k) |^ 1)
by A2,A5,A6,A7,RADIX_2:11;
hence thesis by A2,RADIX_2:11;
end;
hence thesis by A7,A8;
end;
A20: for n be Nat st n >= 1 & P[n] holds P[n+1]
proof
let n be Nat;
assume
A21: n >= 1 & P[n];
let k be Nat;
assume
A22: k >= 2;
let tx,ty,tz,tw be Tuple of (n+1),k-SD;
assume
A23: for i be Nat st i in Seg (n+1) holds
(DigA(tx,i) = DigA(tz,i) & DigA(ty,i) = DigA(tw,i))
or (DigA(ty,i) = DigA(tz,i) & DigA(tx,i) = DigA(tw,i));
deffunc F(Nat) = DigB(tx,$1);
consider txn being FinSequence of INT such that
A24: len txn = n and
A25: for i be Nat st i in Seg n holds txn.i = F(i) from SeqLambdaD;
rng txn c= k-SD
proof
let z be set;
assume z in rng txn; then
consider xx be set such that
A26: xx in dom txn and
A27: z = txn.xx by FUNCT_1:def 5;
reconsider xx as Nat by A26;
A28: dom txn = Seg n by FINSEQ_1:def 3,A24; then
A29: z = DigB(tx,xx) by A25,A26,A27
.= DigA(tx,xx) by RADIX_1:def 4;
xx in Seg (n+1) by A26,A28,FINSEQ_2:9; then
DigA(tx,xx) is Element of k-SD by RADIX_1:19;
hence thesis by A29;
end;
then reconsider txn as FinSequence of k-SD by FINSEQ_1:def 4;
A30: for i be Nat st i in Seg n holds txn.i = tx.i
proof
let i be Nat;
assume
A31: i in Seg n; then
A32: i in Seg (n+1) by FINSEQ_2:9;
txn.i = DigB(tx,i) by A25,A31
.= DigA(tx,i) by RADIX_1:def 4;
hence thesis by A32,RADIX_1:def 3;
end;
deffunc F(Nat) = DigB(ty,$1);
consider tyn being FinSequence of INT such that
A33: len tyn = n and
A34: for i be Nat st i in Seg n holds tyn.i = F(i) from SeqLambdaD;
rng tyn c= k-SD
proof
let z be set;
assume z in rng tyn; then
consider yy be set such that
A36: yy in dom tyn and
A37: z = tyn.yy by FUNCT_1:def 5;
reconsider yy as Nat by A36;
A38: dom tyn = Seg n by FINSEQ_1:def 3,A33; then
A39: z = DigB(ty,yy) by A34,A36,A37
.= DigA(ty,yy) by RADIX_1:def 4;
yy in Seg (n+1) by A36,A38,FINSEQ_2:9; then
DigA(ty,yy) is Element of k-SD by RADIX_1:19;
hence thesis by A39;
end;
then reconsider tyn as FinSequence of k-SD by FINSEQ_1:def 4;
A40: for i be Nat st i in Seg n holds tyn.i = ty.i
proof
let i be Nat;
assume
A41: i in Seg n; then
A42: i in Seg (n+1) by FINSEQ_2:9;
tyn.i = DigB(ty,i) by A34,A41
.= DigA(ty,i) by RADIX_1:def 4;
hence thesis by A42,RADIX_1:def 3;
end;
deffunc F(Nat) = DigB(tz,$1);
consider tzn being FinSequence of INT such that
A43: len tzn = n and
A44: for i be Nat st i in Seg n holds tzn.i = F(i) from SeqLambdaD;
rng tzn c= k-SD
proof
let z be set;
assume z in rng tzn; then
consider zz be set such that
A46: zz in dom tzn and
A47: z = tzn.zz by FUNCT_1:def 5;
reconsider zz as Nat by A46;
A48: dom tzn = Seg n by FINSEQ_1:def 3,A43; then
A49: z = DigB(tz,zz) by A44,A46,A47
.= DigA(tz,zz) by RADIX_1:def 4;
zz in Seg (n+1) by A46,A48,FINSEQ_2:9; then
DigA(tz,zz) is Element of k-SD by RADIX_1:19;
hence thesis by A49;
end;
then reconsider tzn as FinSequence of k-SD by FINSEQ_1:def 4;
A50: for i be Nat st i in Seg n holds tzn.i = tz.i
proof
let i be Nat;
assume
A51: i in Seg n; then
A52: i in Seg (n+1) by FINSEQ_2:9;
tzn.i = DigB(tz,i) by A44,A51
.= DigA(tz,i) by RADIX_1:def 4;
hence thesis by A52,RADIX_1:def 3;
end;
deffunc F(Nat) = DigB(tw,$1);
consider twn being FinSequence of INT such that
A53: len twn = n and
A54: for i be Nat st i in Seg n holds twn.i = F(i) from SeqLambdaD;
rng twn c= k-SD
proof
let w be set;
assume w in rng twn; then
consider ww be set such that
A56: ww in dom twn and
A57: w = twn.ww by FUNCT_1:def 5;
reconsider ww as Nat by A56;
A58: dom twn = Seg n by FINSEQ_1:def 3,A53; then
A59: w = DigB(tw,ww) by A54,A56,A57
.= DigA(tw,ww) by RADIX_1:def 4;
ww in Seg (n+1) by A56,A58,FINSEQ_2:9; then
DigA(tw,ww) is Element of k-SD by RADIX_1:19;
hence thesis by A59;
end;
then reconsider twn as FinSequence of k-SD by FINSEQ_1:def 4;
A60: for i be Nat st i in Seg n holds twn.i = tw.i
proof
let i be Nat;
assume
A61: i in Seg n; then
A62: i in Seg (n+1) by FINSEQ_2:9;
twn.i = DigB(tw,i) by A54,A61
.= DigA(tw,i) by RADIX_1:def 4;
hence thesis by A62,RADIX_1:def 3;
end;
reconsider txn as Tuple of n,k-SD by A24,FINSEQ_2:110;
reconsider tyn as Tuple of n,k-SD by A33,FINSEQ_2:110;
reconsider tzn as Tuple of n,k-SD by A43,FINSEQ_2:110;
reconsider twn as Tuple of n,k-SD by A53,FINSEQ_2:110;
A65: SDDec(txn) + (Radix(k) |^ n)*DigA(tx,n+1) = SDDec(tx) by A30,RADIX_2:10;
A66: SDDec(tyn) + (Radix(k) |^ n)*DigA(ty,n+1) = SDDec(ty) by A40,RADIX_2:10;
A67: SDDec(tzn) + (Radix(k) |^ n)*DigA(tz,n+1) = SDDec(tz) by A50,RADIX_2:10;
A68: SDDec(twn) + (Radix(k) |^ n)*DigA(tw,n+1) = SDDec(tw) by A60,RADIX_2:10;
for i be Nat st i in Seg n holds
(DigA(txn,i) = DigA(tzn,i) & DigA(tyn,i) = DigA(twn,i))
or (DigA(tyn,i) = DigA(tzn,i) & DigA(txn,i) = DigA(twn,i))
proof
let i be Nat;
assume
A70: i in Seg n; then
A71: 1 <= i & i <= n by FINSEQ_1:3; then
i <= n + 1 by NAT_1:37; then
A72: i in Seg (n+1) by A71,FINSEQ_1:3; then
A73: (DigA(tx,i) = DigA(tz,i) & DigA(ty,i) = DigA(tw,i))
or (DigA(ty,i) = DigA(tz,i) & DigA(tx,i) = DigA(tw,i)) by A23;
A74: DigA(tx,i) = tx.i by A72,RADIX_1:def 3
.= txn.i by A70,A30
.= DigA(txn,i) by A70,RADIX_1:def 3;
A75: DigA(ty,i) = ty.i by A72,RADIX_1:def 3
.= tyn.i by A70,A40
.= DigA(tyn,i) by A70,RADIX_1:def 3;
A76: DigA(tz,i) = tz.i by A72,RADIX_1:def 3
.= tzn.i by A70,A50
.= DigA(tzn,i) by A70,RADIX_1:def 3;
A77: DigA(tw,i) = tw.i by A72,RADIX_1:def 3
.= twn.i by A70,A60
.= DigA(twn,i) by A70,RADIX_1:def 3;
thus thesis by A73,A74,A75,A76,A77;
end; then
A83: SDDec(tzn) + SDDec(twn) = SDDec(txn) + SDDec(tyn) by A21,A22;
A84: n+1 >= 1 by NAT_1:29;
A85: SDDec(tz) + SDDec(tw)
= SDDec(tzn) + (Radix(k) |^ n)*DigA(tz,n+1)
+ SDDec(twn) + (Radix(k) |^ n)*DigA(tw,n+1) by A67,A68,XCMPLX_1:1
.= SDDec(tzn) + SDDec(twn) + (Radix(k) |^ n)*DigA(tz,n+1)
+ (Radix(k) |^ n)*DigA(tw,n+1) by XCMPLX_1:1
.= SDDec(tzn) + SDDec(twn) + ((Radix(k) |^ n)*DigA(tz,n+1)
+ (Radix(k) |^ n)*DigA(tw,n+1)) by XCMPLX_1:1;
A86: SDDec(tx) + SDDec(ty)
= SDDec(txn) + (Radix(k) |^ n)*DigA(tx,n+1)
+ SDDec(tyn) + (Radix(k) |^ n)*DigA(ty,n+1) by A65,A66,XCMPLX_1:1
.= SDDec(txn) + SDDec(tyn) + (Radix(k) |^ n)*DigA(tx,n+1)
+ (Radix(k) |^ n)*DigA(ty,n+1) by XCMPLX_1:1
.= SDDec(tzn) + SDDec(twn) + ((Radix(k) |^ n)*DigA(tx,n+1)
+ (Radix(k) |^ n)*DigA(ty,n+1)) by A83,XCMPLX_1:1;
n+1 > 0 by A84,AXIOMS:22; then
n+1 in Seg (n+1) by FINSEQ_1:5; then
A87: (DigA(tx,n+1) = DigA(tz,n+1) & DigA(ty,n+1) = DigA(tw,n+1))
or (DigA(ty,n+1) = DigA(tz,n+1) & DigA(tx,n+1) = DigA(tw,n+1)) by A23;
thus thesis by A87,A85,A86;
end;
for n be Nat st n >= 1 holds P[n] from Ind1(A1,A20);
hence thesis;
end;
theorem
for n,k be Nat st n >= 1 & k >= 2 holds
for tx,ty,tz be Tuple of n,k-SD st
(for i be Nat st i in Seg n holds
(DigA(tx,i) = DigA(tz,i) & DigA(ty,i) = 0)
or (DigA(ty,i) = DigA(tz,i) & DigA(tx,i) = 0)) holds
SDDec(tz) + SDDec(DecSD(0,n,k)) = SDDec(tx) + SDDec(ty)
proof
let n,k be Nat;
assume
A1: n >= 1 & k >= 2;
let tx,ty,tz be Tuple of n,k-SD;
assume
A2: for i be Nat st i in Seg n holds
(DigA(tx,i) = DigA(tz,i) & DigA(ty,i) = 0)
or (DigA(ty,i) = DigA(tz,i) & DigA(tx,i) = 0);
for i be Nat st i in Seg n holds
(DigA(tx,i) = DigA(tz,i) & DigA(ty,i) = DigA(DecSD(0,n,k),i))
or (DigA(ty,i) = DigA(tz,i) & DigA(tx,i) = DigA(DecSD(0,n,k),i))
proof
let i be Nat;
assume
A3: i in Seg n; then
DigA(DecSD(0,n,k),i) = 0 by Th4;
hence thesis by A2,A3;
end;
hence thesis by A1,Th13;
end;
begin :: Definiton of Max/Min Radix-2^k SD Number in Some Digits
definition let i,m,k be Nat;
assume
A1: k >= 2;
func SDMinDigit(m,k,i) -> Element of k-SD equals
:Def1:
-Radix(k)+1 if 1 <= i & i < m
otherwise 0;
coherence
proof
A3: k-SD = {w where w is Element of INT:w <= Radix(k)-1 & w >= -Radix(k)+1}
by RADIX_1:def 2;
Radix(k) > 2 by A1,RADIX_4:1; then
Radix(k) > 1 by AXIOMS:22; then
Radix(k) + Radix(k) > 1 + 1 by REAL_1:67; then
Radix(k) - 1 > 1 - Radix(k) by REAL_2:169; then
A4: Radix(k) - 1 > -Radix(k) + 1 by XCMPLX_0:def 8;
-Radix(k) + 1 is Element of INT by INT_1:def 2; then
-Radix(k) + 1 in k-SD by A3,A4;
hence thesis by RADIX_1:16;
end;
consistency;
end;
definition let n,m,k be Nat;
func SDMin(n,m,k) -> Tuple of n,k-SD means
:Def2:
for i be Nat st i in Seg n holds DigA(it,i) = SDMinDigit(m,k,i);
existence
proof
deffunc F(Nat) = SDMinDigit(m,k,$1);
consider z being FinSequence of k-SD such that
A2: len z = n and
A3: for j be Nat st j in Seg n holds
z.j = F(j) from SeqLambdaD;
reconsider z as Tuple of n,(k-SD) by A2,FINSEQ_2:110;
take z;
let i be Nat;
assume
A4: i in Seg n; then
DigA(z,i) = z.i by RADIX_1:def 3;
hence thesis by A3,A4;
end;
uniqueness
proof
let k1,k2 be Tuple of n,k-SD such that
A10: for i be Nat st i in Seg n holds DigA(k1,i) = SDMinDigit(m,k,i) and
A11: for i be Nat st i in Seg n holds DigA(k2,i) = SDMinDigit(m,k,i);
A12: len k1 = n & len k2 = n by FINSEQ_2:109;
now let j be Nat;
assume
A13: j in Seg n; then
k1.j = DigA(k1,j) by RADIX_1:def 3
.= SDMinDigit(m,k,j) by A10,A13
.= DigA(k2,j) by A11,A13
.= k2.j by A13,RADIX_1:def 3;
hence k1.j = k2.j;
end;
hence k1 = k2 by A12,FINSEQ_2:10;
end;
end;
definition let i,m,k be Nat;
assume
A1: k >= 2;
func SDMaxDigit(m,k,i) -> Element of k-SD equals
:Def3:
Radix(k)-1 if 1 <= i & i < m
otherwise 0;
coherence by RADIX_1:16,A1,Lm1;
consistency;
end;
definition let n,m,k be Nat;
func SDMax(n,m,k) -> Tuple of n,k-SD means
:Def4:
for i be Nat st i in Seg n holds DigA(it,i) = SDMaxDigit(m,k,i);
existence
proof
deffunc F(Nat) = SDMaxDigit(m,k,$1);
consider z being FinSequence of k-SD such that
A2: len z = n and
A3: for j be Nat st j in Seg n holds
z.j = F(j) from SeqLambdaD;
reconsider z as Tuple of n,(k-SD) by A2,FINSEQ_2:110;
take z;
let i be Nat;
assume
A4: i in Seg n; then
DigA(z,i) = z.i by RADIX_1:def 3;
hence thesis by A3,A4;
end;
uniqueness
proof
let k1,k2 be Tuple of n,k-SD such that
A10: for i be Nat st i in Seg n holds DigA(k1,i) = SDMaxDigit(m,k,i) and
A11: for i be Nat st i in Seg n holds DigA(k2,i) = SDMaxDigit(m,k,i);
A12: len k1 = n & len k2 = n by FINSEQ_2:109;
now let j be Nat;
assume
A13: j in Seg n; then
k1.j = DigA(k1,j) by RADIX_1:def 3
.= SDMaxDigit(m,k,j) by A10,A13
.= DigA(k2,j) by A11,A13
.= k2.j by A13,RADIX_1:def 3;
hence k1.j = k2.j;
end;
hence k1 = k2 by A12,FINSEQ_2:10;
end;
end;
definition let i,m,k be Nat;
assume
A1: k >= 2;
func FminDigit(m,k,i) -> Element of k-SD equals
:Def5:
1 if i = m
otherwise 0;
coherence
proof
1 in k-SD
proof
A3: k-SD = {w where w is Element of INT:w <= Radix(k)-1 & w >= -Radix(k)+1}
by RADIX_1:def 2;
A4: Radix(k) > 2 by A1, RADIX_4:1; then
Radix(k)+ -1 > 2 + -1 by REAL_1:53; then
A5: Radix(k) - 1 >= 1 by XCMPLX_0:def 8;
-Radix(k) < -2 by A4,REAL_1:50; then
-Radix(k) + 1 < -2 + 1 by REAL_1:53; then
A6: -Radix(k) + 1 <= 1 by AXIOMS:22;
1 is Element of INT by INT_1:def 2;
hence thesis by A3,A5,A6;
end;
hence thesis by RADIX_1:16;
end;
consistency;
end;
definition let n,m,k be Nat;
func Fmin(n,m,k) -> Tuple of n,k-SD means
:Def6:
for i be Nat st i in Seg n holds DigA(it,i) = FminDigit(m,k,i);
existence
proof
deffunc F(Nat) = FminDigit(m,k,$1);
consider z being FinSequence of k-SD such that
A2: len z = n and
A3: for j be Nat st j in Seg n holds
z.j = F(j) from SeqLambdaD;
reconsider z as Tuple of n,(k-SD) by A2,FINSEQ_2:110;
take z;
let i be Nat;
assume
A4: i in Seg n;
hence DigA(z,i) = z.i by RADIX_1:def 3
.= FminDigit(m,k,i) by A3,A4;
end;
uniqueness
proof
let k1,k2 be Tuple of n,k-SD such that
A10: for i be Nat st i in Seg n holds DigA(k1,i) = FminDigit(m,k,i) and
A11: for i be Nat st i in Seg n holds DigA(k2,i) = FminDigit(m,k,i);
A12: len k1 = n & len k2 = n by FINSEQ_2:109;
now let j be Nat;
assume
A13: j in Seg n; then
k1.j = DigA(k1,j) by RADIX_1:def 3
.= FminDigit(m,k,j) by A10,A13
.= DigA(k2,j) by A11,A13
.= k2.j by A13,RADIX_1:def 3;
hence k1.j = k2.j;
end;
hence k1 = k2 by A12,FINSEQ_2:10;
end;
end;
definition let i,m,k be Nat;
assume
A1: k >= 2;
func FmaxDigit(m,k,i) -> Element of k-SD equals
:Def7:
Radix(k) - 1 if i = m
otherwise 0;
coherence by A1,Lm1,RADIX_1:16;
consistency;
end;
definition let n,m,k be Nat;
func Fmax(n,m,k) -> Tuple of n,k-SD means
:Def8:
for i be Nat st i in Seg n holds DigA(it,i) = FmaxDigit(m,k,i);
existence
proof
deffunc F(Nat) = FmaxDigit(m,k,$1);
consider z being FinSequence of k-SD such that
A2: len z = n and
A3: for j be Nat st j in Seg n holds
z.j = F(j) from SeqLambdaD;
reconsider z as Tuple of n,(k-SD) by A2,FINSEQ_2:110;
take z;
let i be Nat;
assume
A4: i in Seg n;
hence DigA(z,i) = z.i by RADIX_1:def 3
.= FmaxDigit(m,k,i) by A3,A4;
end;
uniqueness
proof
let k1,k2 be Tuple of n,k-SD such that
A10: for i be Nat st i in Seg n holds DigA(k1,i) = FmaxDigit(m,k,i) and
A11: for i be Nat st i in Seg n holds DigA(k2,i) = FmaxDigit(m,k,i);
A12: len k1 = n & len k2 = n by FINSEQ_2:109;
now let j be Nat;
assume
A13: j in Seg n; then
k1.j = DigA(k1,j) by RADIX_1:def 3
.= FmaxDigit(m,k,j) by A10,A13
.= DigA(k2,j) by A11,A13
.= k2.j by A13,RADIX_1:def 3;
hence k1.j = k2.j;
end;
hence k1 = k2 by A12,FINSEQ_2:10;
end;
end;
begin :: Properties of Max/Min Radix-$2^k$ SD Numbers
theorem Th15:
for n,m,k be Nat st n >= 1 & k >= 2 & m in Seg n holds
for i be Nat st i in Seg n holds
DigA(SDMax(n,m,k),i)+DigA(SDMin(n,m,k),i) = 0
proof
let n,m,k be Nat;
assume
A1: n >= 1 & k >= 2 & m in Seg n;
let i be Nat;
assume
A2: i in Seg n; then
A3: i >= 1 & i <= n by FINSEQ_1:3;
reconsider a = SDMinDigit(m,k,i) as Element of INT;
reconsider b = SDMaxDigit(m,k,i) as Element of INT;
DigA(SDMin(n,m,k),i) = SDMinDigit(m,k,i) by A2,Def2; then
A9: DigA(SDMax(n,m,k),i) + DigA(SDMin(n,m,k),i)
= b + a by A2,Def4;
now per cases;
suppose
A10: i < m; then
a + b
= -Radix(k) + 1 + b by A1,A3,Def1
.= -Radix(k) + 1 + (Radix(k) - 1) by A1,A3,A10,Def3
.= -Radix(k) + ( 1 + (Radix(k) - 1)) by XCMPLX_1:1
.= -Radix(k) + ( Radix(k) ) by XCMPLX_1:27
.= 0 by XCMPLX_0:def 6;
hence thesis by A9;
suppose
A11: i >= m; then
a + b
= 0 + b by A1,Def1
.= 0 + 0 by A1,A11,Def3;
hence thesis by A9;
end;
hence thesis;
end;
theorem
for n be Nat st n >= 1 holds
for m,k be Nat st m in Seg n & k >= 2 holds
SDDec(SDMax(n,m,k)) + SDDec(SDMin(n,m,k)) = SDDec(DecSD(0,n,k))
proof
let n be Nat;
assume
A1: n >= 1;
let m,k be Nat;
assume
A2: m in Seg n & k >= 2;
A4: n in Seg n by A1,FINSEQ_1:3;
for i be Nat st i in Seg n holds
DigA(DecSD(0,n,k),i) = DigA(SDMax(n,m,k) '+' SDMin(n,m,k),i)
proof
let i be Nat;
assume
A10: i in Seg n; then
A11: i >= 1 & i <= n by FINSEQ_1:3;
A12: DigA(SDMax(n,m,k) '+' SDMin(n,m,k),i)
= Add(SDMax(n,m,k),SDMin(n,m,k),i,k) by A10,RADIX_1:def 14
.= SD_Add_Data(DigA(SDMax(n,m,k),i)+DigA(SDMin(n,m,k),i),k)
+ SD_Add_Carry(DigA(SDMax(n,m,k),i-'1)+DigA(SDMin(n,m,k),i-'1))
by A2,A10,RADIX_1:def 13
.= SD_Add_Data(0,k)
+ SD_Add_Carry(DigA(SDMax(n,m,k),i-'1)+DigA(SDMin(n,m,k),i-'1))
by A1,A2,A10,Th15
.= 0+SD_Add_Carry(DigA(SDMax(n,m,k),i-'1)+DigA(SDMin(n,m,k),i-'1))
by RADIX_1:22;
A13: DigA(DecSD(0,n,k),i) = 0 by A10,Th4;
now per cases by A11,REAL_1:def 5;
suppose
i = 1; then
A15: i -' 1 = 0 by NAT_2:10; then
DigA(SDMin(n,m,k),i-'1) = 0 by RADIX_1:def 3; then
DigA(SDMax(n,m,k) '+' SDMin(n,m,k),i)
= SD_Add_Carry(0+0) by A12,A15,RADIX_1:def 3;
hence thesis by RADIX_1:def 10,A13;
suppose
i > 1; then
i -' 1 in Seg n by A10,Th1; then
DigA(SDMax(n,m,k) '+' SDMin(n,m,k),i)
= SD_Add_Carry(0) by A12,A1,A2,Th15;
hence thesis by RADIX_1:def 10,A13;
end;
hence thesis;
end; then
A90: SDDec(DecSD(0,n,k)) = SDDec(SDMax(n,m,k) '+' SDMin(n,m,k)) by A1,Th11;
SDDec(SDMax(n,m,k)) + SDDec(SDMin(n,m,k))
= SDDec(SDMax(n,m,k) '+' SDMin(n,m,k))
+ SD_Add_Carry(DigA(SDMax(n,m,k),n)+DigA(SDMin(n,m,k),n))
* (Radix(k) |^ n) by A1,A2,RADIX_2:11
.= SDDec(SDMax(n,m,k) '+' SDMin(n,m,k))
+ SD_Add_Carry(0) * (Radix(k) |^ n) by A1,A2,A4,Th15
.= SDDec(SDMax(n,m,k) '+' SDMin(n,m,k)) + 0 * (Radix(k) |^ n)
by RADIX_1:def 10;
hence thesis by A90;
end;
theorem
for n be Nat st n >= 1 holds
for m,k be Nat st m in Seg n & k >= 2 holds
SDDec(Fmin(n,m,k)) = SDDec(SDMax(n,m,k)) + SDDec(DecSD(1,n,k))
proof
let n be Nat;
assume
A1: n >= 1;
let m,k be Nat;
assume
A2: m in Seg n & k >= 2; then
A3: n >= m & m >= 1 by FINSEQ_1:3;
A4: 1 in Seg 1 by FINSEQ_1:3;
A5: 1 in Seg n by A1,FINSEQ_1:3;
now per cases by A1,REAL_1:def 5;
suppose
A10: n = 1;
A12: SDDec(SDMax(1,m,k) '+' DecSD(1,1,k))
= DigA(SDMax(1,m,k) '+' DecSD(1,1,k),1) by Th3
.= Add(SDMax(1,m,k),DecSD(1,1,k),1,k) by A4,RADIX_1:def 14
.= SD_Add_Data(DigA(SDMax(1,m,k),1)+DigA(DecSD(1,1,k),1),k)
+ SD_Add_Carry(DigA(SDMax(1,m,k),1-'1)+DigA(DecSD(1,1,k),1-'1))
by A2,A4,RADIX_1:def 13
.= SD_Add_Data(DigA(SDMax(1,m,k),1)+DigA(DecSD(1,1,k),1),k)
+ SD_Add_Carry(DigA(SDMax(1,m,k),0)+DigA(DecSD(1,1,k),1-'1))
by GOBOARD9:1
.= SD_Add_Data(DigA(SDMax(1,m,k),1)+DigA(DecSD(1,1,k),1),k)
+ SD_Add_Carry(DigA(SDMax(1,m,k),0)+DigA(DecSD(1,1,k),0))
by GOBOARD9:1
.= SD_Add_Data(DigA(SDMax(1,m,k),1)+DigA(DecSD(1,1,k),1),k)
+ SD_Add_Carry(DigA(SDMax(1,m,k),0)+0) by RADIX_1:def 3
.= SD_Add_Data(DigA(SDMax(1,m,k),1)+DigA(DecSD(1,1,k),1),k)
+ SD_Add_Carry(0+0) by RADIX_1:def 3
.= SD_Add_Data(DigA(SDMax(1,m,k),1)+DigA(DecSD(1,1,k),1),k) + 0
by RADIX_1:def 10
.= SD_Add_Data(DigA(SDMax(1,m,k),1)+1,k) by A2,A4,Th6;
A13: m = 1 by A3,A10,AXIOMS:21;
A14: DigA(SDMax(1,m,k),1) = SDMaxDigit(m,k,1) by A4,Def4
.= 0 by A13,A2,Def3; then
A15: SDDec(SDMax(1,m,k) '+' DecSD(1,1,k)) = SD_Add_Data(0+1,k) by A12
.= 1 - SD_Add_Carry(1) * Radix(k) by RADIX_1:def 11
.= 1 - 0 * Radix(k) by RADIX_1:def 10
.= 1;
A16: SDDec(SDMax(1,m,k)) + SDDec(DecSD(1,1,k))
= SDDec(SDMax(1,m,k) '+' DecSD(1,1,k))
+ SD_Add_Carry(DigA(SDMax(1,m,k),1)+DigA(DecSD(1,1,k),1))
*(Radix(k) |^ 1) by A2,RADIX_2:11
.= 1 + SD_Add_Carry(DigA(SDMax(1,m,k),1)+DigA(DecSD(1,1,k),1))
*(Radix(k) |^ 1) by A15
.= 1 + SD_Add_Carry(0+1) *(Radix(k) |^ 1) by A2,A4,Th6,A14
.= 1 + 0 * (Radix(k) |^ 1) by RADIX_1:def 10;
SDDec(Fmin(1,m,k))
= DigA(Fmin(1,m,k),1) by Th3
.= FminDigit(m,k,1) by A4,Def6
.= 1 by A2,A13,Def5;
hence thesis by A10,A16;
suppose
A30: n > 1;
A31: n in Seg n by A1,FINSEQ_1:3; then
A32: DigA(SDMax(n,m,k),n) = SDMaxDigit(m,k,n) by Def4
.= 0 by A2,A3,Def3;
A33: DigA(DecSD(1,n,k),n) = 0 by A31,A30,A2,Th7;
A35: SDDec(SDMax(n,m,k)) + SDDec(DecSD(1,n,k))
= SDDec(SDMax(n,m,k) '+' DecSD(1,n,k))
+ SD_Add_Carry(DigA(SDMax(n,m,k),n)+DigA(DecSD(1,n,k),n))
* (Radix(k) |^ n) by A1,A2,RADIX_2:11
.= SDDec(SDMax(n,m,k) '+' DecSD(1,n,k))
+ 0 * (Radix(k) |^ n) by RADIX_1:21,A32,A33;
for i be Nat st i in Seg n holds
DigA(Fmin(n,m,k),i) = DigA(SDMax(n,m,k) '+' DecSD(1,n,k),i)
proof
let i be Nat;
assume
A40: i in Seg n; then
A41: DigA(SDMax(n,m,k) '+' DecSD(1,n,k),i)
= Add(SDMax(n,m,k),DecSD(1,n,k),i,k) by RADIX_1:def 14
.= SD_Add_Data(DigA(SDMax(n,m,k),i)+DigA(DecSD(1,n,k),i),k)
+ SD_Add_Carry(DigA(SDMax(n,m,k),i-'1)+DigA(DecSD(1,n,k),i-'1))
by A2,A40,RADIX_1:def 13;
A42: DigA(Fmin(n,m,k),i) = FminDigit(m,k,i) by A40,Def6;
A43: DigA(SDMax(n,m,k),i) = SDMaxDigit(m,k,i) by A40,Def4;
A44: i >= 1 & i <= n by A40,FINSEQ_1:3;
now per cases;
suppose
A50: i >= m+1; then
A52: i > m by NAT_1:38; then
A53: i > 1 by A3,AXIOMS:22; then
A54: i -' 1 in Seg n by A40,Th1;
A55: DigA(Fmin(n,m,k),i) = 0 by A42,A2,A52,Def5;
A56: DigA(SDMax(n,m,k),i) = 0 by A43,A2,A52,Def3;
A57: DigA(DecSD(1,n,k),i) = 0 by A2,A40,A53,Th7;
now per cases by A50,REAL_1:def 5;
suppose
A60: i = m+1;
DigA(SDMax(n,m,k),i-'1) = DigA(SDMax(n,m,k),m) by A60,BINARITH:39
.= SDMaxDigit(m,k,m) by A2,Def4
.= 0 by A2,Def3; then
DigA(SDMax(n,m,k) '+' DecSD(1,n,k),i)
= SD_Add_Data(0+0,k) + SD_Add_Carry(0+DigA(DecSD(1,n,k),i-'1))
by A41,A56,A57
.= SD_Add_Data(0+0,k) + 0 by A2,A54,Lm6
.= 0 by RADIX_1:22;
hence thesis by A55;
suppose i > m+1; then
i - 1 > m + 1 - 1 by REAL_1:92; then
A63: i - 1 > m by XCMPLX_1:26; then
i - 1 > 0 by A3,AXIOMS:22; then
A64: i -' 1 > m by A63,BINARITH:def 3;
i -' 1 in Seg n by A53,A40,Th1; then
DigA(SDMax(n,m,k),i-'1) = SDMaxDigit(m,k,i-'1) by Def4
.= 0 by A2,A64,Def3; then
DigA(SDMax(n,m,k) '+' DecSD(1,n,k),i)
= SD_Add_Data(0+0,k) + SD_Add_Carry(0+DigA(DecSD(1,n,k),i-'1))
by A41,A56,A57
.= SD_Add_Data(0+0,k) + 0 by A2,A54,Lm6
.= 0 by RADIX_1:22;
hence thesis by A55;
end;
hence thesis;
suppose i < m+1; then
A67: i <= m by NAT_1:38;
A68: i >= 1 by A40,FINSEQ_1:3;
now per cases by A68,REAL_1:def 5;
suppose
A69: i > 1; then
A70: m > 1 by A67,AXIOMS:22; then
A71: m -' 1 in Seg n by A2,Th1; then
A72: m -' 1 >= 1 by FINSEQ_1:3;
A73: m -' 1 < m by A70,JORDAN5B:1;
now per cases by A67,REAL_1:def 5;
suppose
A74: i = m; then
A75: DigA(Fmin(n,m,k),i) = FminDigit(m,k,m) by A2,Def6
.= 1 by A2,Def5;
A76: DigA(SDMax(n,m,k),i) = 0 by A43,A2,A74,Def3;
A77: DigA(DecSD(1,n,k),i) = 0 by A2,A70,A74,Th7;
A78: DigA(SDMax(n,m,k),i-'1) = DigA(SDMax(n,m,k),m-'1) by A74
.= SDMaxDigit(m,k,m-'1) by A71,Def4
.= Radix(k) - 1 by A2,A72,A73,Def3;
A79: i >= 1 + 1 by A69,INT_1:20;
now per cases by A79,REAL_1:def 5;
suppose
i = 2; then
i -' 1 = 2 - 1 by SCMFSA_7:3; then
DigA(DecSD(1,n,k),i-'1) = 1 by A5,A2,Th6; then
DigA(SDMax(n,m,k) '+' DecSD(1,n,k),i)
= SD_Add_Data(0+0,k)
+SD_Add_Carry(Radix(k) - 1 + 1) by A41,A76,A77,A78
.= 0 + SD_Add_Carry(Radix(k) - 1 + 1) by RADIX_1:22
.= SD_Add_Carry(Radix(k) + 1 - 1) by XCMPLX_1:29
.= SD_Add_Carry(Radix(k)) by XCMPLX_1:26
.= 1 by A2,Th9;
hence thesis by A75;
suppose
A83: i > 2; then
A84: i - 1 > 2 - 1 by REAL_1:92; then
i - 1 > 0 by AXIOMS:22; then
A85: i -' 1 > 1 by A84,BINARITH:def 3;
i > 1 by A83,AXIOMS:22; then
i -' 1 in Seg n by A40,Th1; then
DigA(DecSD(1,n,k),i-'1) = 0 by A2,A85,Th7; then
DigA(SDMax(n,m,k) '+' DecSD(1,n,k),i)
= SD_Add_Data(0+0,k)
+ SD_Add_Carry(Radix(k) - 1 + 0) by A41,A76,A77,A78
.= 0 + SD_Add_Carry(Radix(k) - 1) by RADIX_1:22
.= 1 by A2,Lm5;
hence thesis by A75;
end;
hence thesis;
suppose
A87: i < m;
A89: DigA(Fmin(n,m,k),i) = 0 by A42,A2,A87,Def5;
A90: DigA(SDMax(n,m,k),i) = Radix(k)-1 by A43,A2,A44,A87,Def3;
A91: DigA(DecSD(1,n,k),i) = 0 by A2,A40,A69,Th7;
A92: i >= 1 + 1 by A69,INT_1:20;
i -' 1 < i by A69,JORDAN5B:1; then
A94: i -' 1 < m by A87,AXIOMS:22;
A95: i -' 1 in Seg n by A40,A69,Th1;
now per cases by A92,REAL_1:def 5;
suppose i = 2; then
A97: i -' 1 = 2 - 1 by SCMFSA_7:3; then
A98: i -' 1 >= 1;
A99: DigA(DecSD(1,n,k),i-'1) = 1 by A97,A5,A2,Th6;
DigA(SDMax(n,m,k),i-'1)
= SDMaxDigit(m,k,i-'1) by A95,Def4
.= Radix(k) - 1 by A98,A94,A2,Def3; then
DigA(SDMax(n,m,k) '+' DecSD(1,n,k),i)
= SD_Add_Data(Radix(k)-1+0,k)
+SD_Add_Carry(Radix(k) - 1 + 1) by A41,A90,A91,A99
.= SD_Add_Data(Radix(k)-1,k)
+SD_Add_Carry(Radix(k) + 1 - 1) by XCMPLX_1:29
.= SD_Add_Data(Radix(k)-1,k)
+SD_Add_Carry(Radix(k)) by XCMPLX_1:26
.= SD_Add_Data(Radix(k)-1,k) + 1 by A2,Th9
.= (Radix(k)-1) - SD_Add_Carry(Radix(k)-1)*Radix(k) + 1
by RADIX_1:def 11
.= (Radix(k)-1) - 1*Radix(k) + 1 by A2,Lm5
.= (Radix(k) - 1 ) + 1 - Radix(k) by XCMPLX_1:29
.= (Radix(k) + 1 - 1) - Radix(k) by XCMPLX_1:29
.= Radix(k) - Radix(k) by XCMPLX_1:26
.= 0 by XCMPLX_1:14;
hence thesis by A89;
suppose
A100: i > 2; then
A101: i - 1 > 2 - 1 by REAL_1:92; then
i - 1 > 0 by AXIOMS:22; then
A102: i -' 1 > 1 by A101,BINARITH:def 3;
i > 1 by A100,AXIOMS:22; then
i -' 1 in Seg n by A40,Th1; then
A104: DigA(DecSD(1,n,k),i-'1) = 0 by A2,A102,Th7;
DigA(SDMax(n,m,k),i-'1)
= SDMaxDigit(m,k,i-'1) by A95,Def4
.= Radix(k) - 1 by A102,A94,A2,Def3; then
DigA(SDMax(n,m,k) '+' DecSD(1,n,k),i)
= SD_Add_Data(Radix(k)-1+0,k)
+SD_Add_Carry(Radix(k) - 1 + 0) by A41,A90,A91,A104
.= SD_Add_Data(Radix(k)-1,k) + 1 by A2,Lm5
.= (Radix(k)-1) - SD_Add_Carry(Radix(k)-1)*Radix(k) + 1
by RADIX_1:def 11
.= (Radix(k)-1) - 1*Radix(k) + 1 by A2,Lm5
.= (Radix(k) - 1 ) + 1 - Radix(k) by XCMPLX_1:29
.= (Radix(k) + 1 - 1) - Radix(k) by XCMPLX_1:29
.= Radix(k) - Radix(k) by XCMPLX_1:26
.= 0 by XCMPLX_1:14;
hence thesis by A89;
end;
hence thesis;
end;
hence thesis;
suppose
A106: i = 1;
A107: i -' 1 = 0 by A106,NAT_2:10; then
A108: DigA(SDMax(n,m,k),i-'1) = 0 by RADIX_1:def 3;
A109: DigA(DecSD(1,n,k),i-'1) = 0 by A107,RADIX_1:def 3;
now per cases by A67,REAL_1:def 5;
suppose
A110: i < m;
A111: i >= 1 by A106;
A112: DigA(Fmin(n,m,k),i) = 0 by A110,A42,A2,Def5;
A113: DigA(SDMax(n,m,k),i)=Radix(k)-1 by A43,A2,A110,A111,Def3;
DigA(DecSD(1,n,k),i) = 1 by A2,A5,A106,Th6; then
DigA(SDMax(n,m,k) '+' DecSD(1,n,k),i)
= SD_Add_Data(Radix(k)-1+1,k)
+ SD_Add_Carry(0+0) by A41,A108,A109,A113
.= SD_Add_Data(Radix(k)-1+1,k) + 0 by RADIX_1:21
.= SD_Add_Data(Radix(k)+1-1,k) + 0 by XCMPLX_1:29
.= SD_Add_Data(Radix(k),k) + 0 by XCMPLX_1:26
.= Radix(k) - SD_Add_Carry(Radix(k)) * Radix(k)
by RADIX_1:def 11
.= Radix(k) - 1 * Radix(k) by A2,Th9
.= 0 by XCMPLX_1:14;
hence thesis by A112;
suppose
A115: i = m;
A116: DigA(Fmin(n,m,k),i) = 1 by A115,A42,A2,Def5;
A117: DigA(SDMax(n,m,k),i) = 0 by A43,A2,A115,Def3;
DigA(DecSD(1,n,k),i) = 1 by A2,A5,A106,Th6; then
DigA(SDMax(n,m,k) '+' DecSD(1,n,k),i)
= SD_Add_Data(1+0,k)+SD_Add_Carry(0+0) by A41,A108,A109,A117
.= SD_Add_Data(1,k) + 0 by RADIX_1:21
.= 1 - SD_Add_Carry(1) * Radix(k) by RADIX_1:def 11
.= 1 - 0 * Radix(k) by RADIX_1:def 10
.= 1;
hence thesis by A116;
end;
hence thesis;
end;
hence thesis;
end;
hence thesis;
end;
hence thesis by A1,A35,Th11;
end;
hence thesis;
end;
theorem
for n,m,k be Nat st m in Seg n & k >= 2 holds
SDDec(Fmin(n+1,m+1,k)) = SDDec(Fmin(n+1,m,k)) + SDDec(Fmax(n+1,m,k))
proof
let n,m,k be Nat;
assume
A2: m in Seg n & k >= 2; then
A3: n >= m & m >= 1 by FINSEQ_1:3; then
A4: n + 1 > m by NAT_1:38;
A5: n+1 >= 1 by NAT_1:29; then
n+1 > 0 by AXIOMS:22; then
A6: n+1 in Seg(n+1) by FINSEQ_1:5; then
A7: DigA(Fmin(n+1,m,k),n+1) = FminDigit(m,k,n+1) by Def6
.= 0 by A2,A4,Def5;
A8: DigA(Fmax(n+1,m,k),n+1) = FmaxDigit(m,k,n+1) by A6,Def8
.= 0 by A2,A4,Def7;
A9: SDDec(Fmin(n+1,m,k)) + SDDec(Fmax(n+1,m,k))
= SDDec(Fmin(n+1,m,k) '+' Fmax(n+1,m,k))
+ SD_Add_Carry(DigA(Fmin(n+1,m,k),n+1)+DigA(Fmax(n+1,m,k),n+1))
* (Radix(k) |^ (n+1)) by A2,A5,RADIX_2:11
.= SDDec(Fmin(n+1,m,k) '+' Fmax(n+1,m,k))
+ 0 * (Radix(k) |^ (n+1)) by RADIX_1:21,A7,A8;
A10: m in Seg (n+1) by A2,FINSEQ_2:9;
for i be Nat st i in Seg (n+1) holds
DigA(Fmin(n+1,m+1,k),i)
= DigA(Fmin(n+1,m,k) '+' Fmax(n+1,m,k),i)
proof
let i be Nat;
assume
A12: i in Seg (n+1); then
A13: DigA(Fmin(n+1,m,k) '+' Fmax(n+1,m,k),i)
= Add(Fmin(n+1,m,k),Fmax(n+1,m,k),i,k) by RADIX_1:def 14
.= SD_Add_Data(DigA(Fmin(n+1,m,k),i)+DigA(Fmax(n+1,m,k),i),k)
+ SD_Add_Carry(DigA(Fmin(n+1,m,k),i-'1)+DigA(Fmax(n+1,m,k),i-'1))
by A2,A12,RADIX_1:def 13;
A14: m + 1 > m by NAT_1:38;
A16: DigA(Fmin(n+1,m,k),i) = FminDigit(m,k,i) by A12,Def6;
A17: DigA(Fmax(n+1,m,k),i) = FmaxDigit(m,k,i) by A12,Def8;
A18: DigA(Fmin(n+1,m+1,k),i) = FminDigit(m+1,k,i) by A12,Def6;
A19: i >= 1 by A12,FINSEQ_1:3;
now per cases;
suppose
A21: i >= m+1;
now per cases;
suppose
A22: i = m+1;
A24: DigA(Fmin(n+1,m,k),i) = FminDigit(m,k,m+1) by A12,A22,Def6
.= 0 by A2,A14,Def5;
A25: DigA(Fmax(n+1,m,k),i) = FmaxDigit(m,k,m+1) by A12,A22,Def8
.= 0 by A2,A14,Def7;
A26: DigA(Fmin(n+1,m,k),i-'1) = DigA(Fmin(n+1,m,k),m) by A22,BINARITH:39
.= FminDigit(m,k,m) by A10,Def6
.= 1 by A2,Def5;
A27: DigA(Fmax(n+1,m,k),i-'1) = DigA(Fmax(n+1,m,k),m) by A22,BINARITH:39
.= FmaxDigit(m,k,m) by A10,Def8
.= Radix(k) - 1 by A2,Def7;
A29: DigA(Fmin(n+1,m+1,k),i) = FminDigit(m+1,k,m+1) by A18,A22
.= 1 by A2,Def5;
DigA(Fmin(n+1,m,k) '+' Fmax(n+1,m,k),i)
= SD_Add_Data(0+0,k) + SD_Add_Carry(1+(Radix(k)-1))
by A13,A24,A25,A26,A27
.= 0 + SD_Add_Carry(1+(Radix(k)-1)) by RADIX_1:22
.= SD_Add_Carry(Radix(k)) by XCMPLX_1:27
.= 1 by A2,Th9;
hence thesis by A29;
suppose i <> m + 1; then
A31: i > m + 1 by A21,REAL_1:def 5; then
A32: i > m by A14,AXIOMS:22; then
i > 1 by A3,AXIOMS:22; then
A34: i -' 1 in Seg (n+1) by A12,Th1;
i - 1 > m + 1 - 1 by A31,REAL_1:92; then
A35: i - 1 > m by XCMPLX_1:26; then
i - 1 > 0 by A3,AXIOMS:22; then
A36: i -' 1 > m by A35,BINARITH:def 3;
A37: DigA(Fmin(n+1,m,k),i) = 0 by A16,A2,A32,Def5;
A38: DigA(Fmax(n+1,m,k),i) = 0 by A17,A2,A32,Def7;
A39: DigA(Fmin(n+1,m,k),i-'1) = FminDigit(m,k,i-'1) by A34,Def6
.= 0 by A2,A36,Def5;
A40: DigA(Fmax(n+1,m,k),i-'1) = FmaxDigit(m,k,i-'1) by A34,Def8
.= 0 by A2,A36,Def7;
A41: DigA(Fmin(n+1,m+1,k),i) = 0 by A18,A2,A31,Def5;
DigA(Fmin(n+1,m,k) '+' Fmax(n+1,m,k),i)
= SD_Add_Data(0+0,k) + SD_Add_Carry(0+0) by A13,A37,A38,A39,A40;
hence thesis by RADIX_1:22,RADIX_1:21,A41;
end;
hence thesis;
suppose i < m+1; then
A50: i <= m by NAT_1:38;
now per cases by A19,REAL_1:def 5;
suppose
A51: i > 1; then
A60: m > 1 by A50,AXIOMS:22; then
A61: m -' 1 in Seg (n+1) by A10,Th1;
A62: m -' 1 < m by A60,JORDAN5B:1;
now per cases by A50,REAL_1:def 5;
suppose
A63: i = m; then
A64: DigA(Fmin(n+1,m,k),i) = 1 by A16,A2,Def5;
A65: DigA(Fmax(n+1,m,k),i) = Radix(k) - 1 by A17,A2,A63,Def7;
A66: DigA(Fmin(n+1,m,k),i-'1) = DigA(Fmin(n+1,m,k),m-'1) by A63
.= FminDigit(m,k,m-'1) by A61,Def6
.= 0 by A2,A62,Def5;
A67: DigA(Fmax(n+1,m,k),i-'1) = DigA(Fmax(n+1,m,k),m-'1) by A63
.= FmaxDigit(m,k,m-'1) by A61,Def8
.= 0 by A2,A62,Def7;
A68: DigA(Fmin(n+1,m+1,k),i) = FminDigit(m+1,k,m) by A18,A63
.= 0 by A2,A14,Def5;
DigA(Fmin(n+1,m,k) '+' Fmax(n+1,m,k),i)
= SD_Add_Data(1 + (Radix(k) - 1),k)
+ SD_Add_Carry(0+0) by A13,A64,A65,A66,A67
.= SD_Add_Data(1 + (Radix(k) - 1),k) + 0 by RADIX_1:21
.= SD_Add_Data(Radix(k),k) by XCMPLX_1:27
.= 0 by A2,Th10;
hence thesis by A68;
suppose
A70: i < m;
i -' 1 < i by A19,JORDAN5B:1; then
A71: i -' 1 < m by A70,AXIOMS:22; then
A72: i -' 1 <= n+1 by A4,AXIOMS:22;
i -' 1 >= 1 by A51,JORDAN3:12; then
A73: i -' 1 in Seg (n+1) by A72,FINSEQ_1:3;
A74: DigA(Fmin(n+1,m,k),i) = 0 by A16,A2,A70,Def5;
A75: DigA(Fmax(n+1,m,k),i) = 0 by A17,A2,A70,Def7;
A76: DigA(Fmin(n+1,m,k),i-'1)
= FminDigit(m,k,i-'1) by A73,Def6
.= 0 by A2,A71,Def5;
A77: DigA(Fmax(n+1,m,k),i-'1)
= FmaxDigit(m,k,i-'1) by A73,Def8
.= 0 by A2,A71,Def7;
i < m + 1 by A70,NAT_1:38; then
A78: DigA(Fmin(n+1,m+1,k),i) = 0 by A18,A2,Def5;
DigA(Fmin(n+1,m,k) '+' Fmax(n+1,m,k),i)
= SD_Add_Data(0+0,k) + SD_Add_Carry(0+0) by A13,A74,A75,A76,A77
.= 0 + 0 by RADIX_1:22,RADIX_1:21;
hence thesis by A78;
end;
hence thesis;
suppose
A80: i = 1;
A81: i -' 1 = 0 by A80,NAT_2:10;
A82: DigA(Fmin(n+1,m,k),i-'1) = 0 by A81,RADIX_1:def 3;
A83: DigA(Fmax(n+1,m,k),i-'1) = 0 by A81,RADIX_1:def 3;
now per cases by A50,REAL_1:def 5;
suppose
A86: i < m; then
A87: DigA(Fmin(n+1,m,k),i) = 0 by A16,A2,Def5;
A88: DigA(Fmax(n+1,m,k),i) = 0 by A17,A2,A86,Def7;
i < m + 1 by A86,NAT_1:38; then
A89: DigA(Fmin(n+1,m+1,k),i) = 0 by A18,A2,Def5;
DigA(Fmin(n+1,m,k) '+' Fmax(n+1,m,k),i)
= SD_Add_Data(0+0,k) + SD_Add_Carry(0+0) by A13,A82,A83,A87,A88
.= 0 + 0 by RADIX_1:22,RADIX_1:21;
hence thesis by A89;
suppose
A90: i = m; then
A91: DigA(Fmin(n+1,m,k),i) = 1 by A16,A2,Def5;
A92: DigA(Fmax(n+1,m,k),i) = Radix(k) - 1 by A17,A2,A90,Def7;
i < m + 1 by A90,NAT_1:38; then
A93: DigA(Fmin(n+1,m+1,k),i) = 0 by A18,A2,Def5;
DigA(Fmin(n+1,m,k) '+' Fmax(n+1,m,k),i)
= SD_Add_Data(1+(Radix(k)-1),k)
+ SD_Add_Carry(0+0) by A13,A82,A83,A91,A92
.= SD_Add_Data(1 + (Radix(k) - 1),k) + 0 by RADIX_1:21
.= SD_Add_Data(Radix(k),k) by XCMPLX_1:27
.= 0 by A2,Th10;
hence thesis by A93;
end;
hence thesis;
end;
hence thesis;
end;
hence thesis;
end;
hence thesis by A9,A5,Th11;
end;