defpred S1[ Nat] means for k, x being Nat st k >= 2 & x is_represented_by \$1,k holds
x = SDSub2IntOut (SD2SDSub (DecSD (x,\$1,k)));
let n be Nat; :: thesis: ( n >= 1 implies for k, x being Nat st k >= 2 & x is_represented_by n,k holds
x = SDSub2IntOut (SD2SDSub (DecSD (x,n,k))) )

assume A1: n >= 1 ; :: thesis: for k, x being Nat st k >= 2 & x is_represented_by n,k holds
x = SDSub2IntOut (SD2SDSub (DecSD (x,n,k)))

A2: for n being Nat st n >= 1 & S1[n] holds
S1[n + 1]
proof
let n be Nat; :: thesis: ( n >= 1 & S1[n] implies S1[n + 1] )
assume that
A3: n >= 1 and
A4: S1[n] ; :: thesis: S1[n + 1]
A5: n in Seg n by ;
let k, x be Nat; :: thesis: ( k >= 2 & x is_represented_by n + 1,k implies x = SDSub2IntOut (SD2SDSub (DecSD (x,(n + 1),k))) )
assume that
A6: k >= 2 and
A7: x is_represented_by n + 1,k ; :: thesis: x = SDSub2IntOut (SD2SDSub (DecSD (x,(n + 1),k)))
reconsider k = k as Element of NAT by ORDINAL1:def 12;
set xn = x mod (() |^ n);
set RN1 = () |^ (n + 1);
set RN = () |^ n;
A8: (n + 1) + 1 in Seg ((n + 1) + 1) by FINSEQ_1:3;
A9: SDSub2INTDigit ((SD2SDSub (DecSD (x,(n + 1),k))),((n + 1) + 1),k) = (() |^ (n + 1)) * (DigB_SDSub ((SD2SDSub (DecSD (x,(n + 1),k))),((n + 1) + 1))) by NAT_D:34
.= (() |^ (n + 1)) * (SD2SDSubDigitS ((DecSD (x,(n + 1),k)),((n + 1) + 1),k)) by
.= (() |^ (n + 1)) * (SD2SDSubDigit ((DecSD (x,(n + 1),k)),((n + 1) + 1),k)) by A6, A8, Def7
.= (() |^ (n + 1)) * (SDSub_Add_Carry ((DigA ((DecSD (x,(n + 1),k)),(((n + 1) + 1) -' 1))),k)) by Def6
.= (() |^ (n + 1)) * (SDSub_Add_Carry ((DigA ((DecSD (x,(n + 1),k)),(n + 1))),k)) by NAT_D:34 ;
set XN = SD2SDSub (DecSD ((x mod (() |^ n)),n,k));
set X = SD2SDSub (DecSD (x,(n + 1),k));
deffunc H1( Nat) -> Element of INT = SDSub2INTDigit ((SD2SDSub (DecSD (x,(n + 1),k))),\$1,k);
consider xp being FinSequence of INT such that
A10: len xp = n + 1 and
A11: for i being Nat st i in dom xp holds
xp . i = H1(i) from A12: dom xp = Seg (n + 1) by ;
A13: len (SDSub2INT (SD2SDSub (DecSD (x,(n + 1),k)))) = (n + 1) + 1 by CARD_1:def 7;
A14: for j being Nat st 1 <= j & j <= len (SDSub2INT (SD2SDSub (DecSD (x,(n + 1),k)))) holds
(SDSub2INT (SD2SDSub (DecSD (x,(n + 1),k)))) . j = (xp ^ <*(SDSub2INTDigit ((SD2SDSub (DecSD (x,(n + 1),k))),((n + 1) + 1),k))*>) . j
proof
let j be Nat; :: thesis: ( 1 <= j & j <= len (SDSub2INT (SD2SDSub (DecSD (x,(n + 1),k)))) implies (SDSub2INT (SD2SDSub (DecSD (x,(n + 1),k)))) . j = (xp ^ <*(SDSub2INTDigit ((SD2SDSub (DecSD (x,(n + 1),k))),((n + 1) + 1),k))*>) . j )
assume that
A15: 1 <= j and
A16: j <= len (SDSub2INT (SD2SDSub (DecSD (x,(n + 1),k)))) ; :: thesis: (SDSub2INT (SD2SDSub (DecSD (x,(n + 1),k)))) . j = (xp ^ <*(SDSub2INTDigit ((SD2SDSub (DecSD (x,(n + 1),k))),((n + 1) + 1),k))*>) . j
j <= (n + 1) + 1 by ;
then A17: j in Seg ((n + 1) + 1) by ;
A18: j in dom (SDSub2INT (SD2SDSub (DecSD (x,(n + 1),k)))) by ;
now :: thesis: (SDSub2INT (SD2SDSub (DecSD (x,(n + 1),k)))) . j = (xp ^ <*(SDSub2INTDigit ((SD2SDSub (DecSD (x,(n + 1),k))),((n + 1) + 1),k))*>) . j
per cases ( j in Seg (n + 1) or j = (n + 1) + 1 ) by ;
suppose A19: j in Seg (n + 1) ; :: thesis: (SDSub2INT (SD2SDSub (DecSD (x,(n + 1),k)))) . j = (xp ^ <*(SDSub2INTDigit ((SD2SDSub (DecSD (x,(n + 1),k))),((n + 1) + 1),k))*>) . j
then j in dom xp by ;
then (xp ^ <*(SDSub2INTDigit ((SD2SDSub (DecSD (x,(n + 1),k))),((n + 1) + 1),k))*>) . j = xp . j by FINSEQ_1:def 7
.= SDSub2INTDigit ((SD2SDSub (DecSD (x,(n + 1),k))),j,k) by
.= (SDSub2INT (SD2SDSub (DecSD (x,(n + 1),k)))) /. j by
.= (SDSub2INT (SD2SDSub (DecSD (x,(n + 1),k)))) . j by ;
hence (SDSub2INT (SD2SDSub (DecSD (x,(n + 1),k)))) . j = (xp ^ <*(SDSub2INTDigit ((SD2SDSub (DecSD (x,(n + 1),k))),((n + 1) + 1),k))*>) . j ; :: thesis: verum
end;
suppose A20: j = (n + 1) + 1 ; :: thesis: (SDSub2INT (SD2SDSub (DecSD (x,(n + 1),k)))) . j = (xp ^ <*(SDSub2INTDigit ((SD2SDSub (DecSD (x,(n + 1),k))),((n + 1) + 1),k))*>) . j
A21: j in dom (SDSub2INT (SD2SDSub (DecSD (x,(n + 1),k)))) by ;
(xp ^ <*(SDSub2INTDigit ((SD2SDSub (DecSD (x,(n + 1),k))),((n + 1) + 1),k))*>) . j = SDSub2INTDigit ((SD2SDSub (DecSD (x,(n + 1),k))),((n + 1) + 1),k) by
.= (SDSub2INT (SD2SDSub (DecSD (x,(n + 1),k)))) /. ((n + 1) + 1) by
.= (SDSub2INT (SD2SDSub (DecSD (x,(n + 1),k)))) . j by ;
hence (SDSub2INT (SD2SDSub (DecSD (x,(n + 1),k)))) . j = (xp ^ <*(SDSub2INTDigit ((SD2SDSub (DecSD (x,(n + 1),k))),((n + 1) + 1),k))*>) . j ; :: thesis: verum
end;
end;
end;
hence (SDSub2INT (SD2SDSub (DecSD (x,(n + 1),k)))) . j = (xp ^ <*(SDSub2INTDigit ((SD2SDSub (DecSD (x,(n + 1),k))),((n + 1) + 1),k))*>) . j ; :: thesis: verum
end;
then x mod (() |^ n) < () |^ n by ;
then x mod (() |^ n) is_represented_by n,k ;
then A22: x mod (() |^ n) = SDSub2IntOut (SD2SDSub (DecSD ((x mod (() |^ n)),n,k))) by A4, A6
.= Sum (SDSub2INT (SD2SDSub (DecSD ((x mod (() |^ n)),n,k)))) ;
A23: n + 1 in Seg (n + 1) by FINSEQ_1:3;
then A24: n + 1 in Seg ((n + 1) + 1) by FINSEQ_2:8;
consider xpp being FinSequence of INT such that
A25: len xpp = n and
A26: for i being Nat st i in dom xpp holds
xpp . i = H1(i) from A27: dom xpp = Seg n by ;
A28: for j being Nat st 1 <= j & j <= len xp holds
xp . j = (xpp ^ <*(SDSub2INTDigit ((SD2SDSub (DecSD (x,(n + 1),k))),(n + 1),k))*>) . j
proof
let j be Nat; :: thesis: ( 1 <= j & j <= len xp implies xp . j = (xpp ^ <*(SDSub2INTDigit ((SD2SDSub (DecSD (x,(n + 1),k))),(n + 1),k))*>) . j )
assume ( 1 <= j & j <= len xp ) ; :: thesis: xp . j = (xpp ^ <*(SDSub2INTDigit ((SD2SDSub (DecSD (x,(n + 1),k))),(n + 1),k))*>) . j
then A29: j in Seg (n + 1) by ;
now :: thesis: xp . j = (xpp ^ <*(SDSub2INTDigit ((SD2SDSub (DecSD (x,(n + 1),k))),(n + 1),k))*>) . j
per cases ( j in Seg n or j = n + 1 ) by ;
suppose A30: j in Seg n ; :: thesis: xp . j = (xpp ^ <*(SDSub2INTDigit ((SD2SDSub (DecSD (x,(n + 1),k))),(n + 1),k))*>) . j
then j in dom xpp by ;
then (xpp ^ <*(SDSub2INTDigit ((SD2SDSub (DecSD (x,(n + 1),k))),(n + 1),k))*>) . j = xpp . j by FINSEQ_1:def 7
.= SDSub2INTDigit ((SD2SDSub (DecSD (x,(n + 1),k))),j,k) by
.= xp . j by ;
hence xp . j = (xpp ^ <*(SDSub2INTDigit ((SD2SDSub (DecSD (x,(n + 1),k))),(n + 1),k))*>) . j ; :: thesis: verum
end;
suppose A31: j = n + 1 ; :: thesis: xp . j = (xpp ^ <*(SDSub2INTDigit ((SD2SDSub (DecSD (x,(n + 1),k))),(n + 1),k))*>) . j
then (xpp ^ <*(SDSub2INTDigit ((SD2SDSub (DecSD (x,(n + 1),k))),(n + 1),k))*>) . j = SDSub2INTDigit ((SD2SDSub (DecSD (x,(n + 1),k))),(n + 1),k) by
.= xp . j by A11, A12, A29, A31 ;
hence xp . j = (xpp ^ <*(SDSub2INTDigit ((SD2SDSub (DecSD (x,(n + 1),k))),(n + 1),k))*>) . j ; :: thesis: verum
end;
end;
end;
hence xp . j = (xpp ^ <*(SDSub2INTDigit ((SD2SDSub (DecSD (x,(n + 1),k))),(n + 1),k))*>) . j ; :: thesis: verum
end;
deffunc H2( Nat) -> Element of INT = SDSub2INTDigit ((SD2SDSub (DecSD ((x mod (() |^ n)),n,k))),\$1,k);
consider xnpp being FinSequence of INT such that
A32: len xnpp = n and
A33: for i being Nat st i in dom xnpp holds
xnpp . i = H2(i) from A34: dom xnpp = Seg n by ;
for j being Nat st 1 <= j & j <= len xnpp holds
xnpp . j = xpp . j
proof
let j be Nat; :: thesis: ( 1 <= j & j <= len xnpp implies xnpp . j = xpp . j )
assume ( 1 <= j & j <= len xnpp ) ; :: thesis: xnpp . j = xpp . j
then A35: j in Seg n by ;
then xpp . j = SDSub2INTDigit ((SD2SDSub (DecSD (x,(n + 1),k))),j,k) by
.= SDSub2INTDigit ((SD2SDSub (DecSD ((x mod (() |^ n)),n,k))),j,k) by
.= xnpp . j by ;
hence xnpp . j = xpp . j ; :: thesis: verum
end;
then A36: xpp = xnpp by ;
A37: len (SDSub2INT (SD2SDSub (DecSD ((x mod (() |^ n)),n,k)))) = n + 1 by CARD_1:def 7;
A38: for j being Nat st 1 <= j & j <= len (SDSub2INT (SD2SDSub (DecSD ((x mod (() |^ n)),n,k)))) holds
(SDSub2INT (SD2SDSub (DecSD ((x mod (() |^ n)),n,k)))) . j = (xnpp ^ <*(SDSub2INTDigit ((SD2SDSub (DecSD ((x mod (() |^ n)),n,k))),(n + 1),k))*>) . j
proof
let j be Nat; :: thesis: ( 1 <= j & j <= len (SDSub2INT (SD2SDSub (DecSD ((x mod (() |^ n)),n,k)))) implies (SDSub2INT (SD2SDSub (DecSD ((x mod (() |^ n)),n,k)))) . j = (xnpp ^ <*(SDSub2INTDigit ((SD2SDSub (DecSD ((x mod (() |^ n)),n,k))),(n + 1),k))*>) . j )
assume A39: ( 1 <= j & j <= len (SDSub2INT (SD2SDSub (DecSD ((x mod (() |^ n)),n,k)))) ) ; :: thesis: (SDSub2INT (SD2SDSub (DecSD ((x mod (() |^ n)),n,k)))) . j = (xnpp ^ <*(SDSub2INTDigit ((SD2SDSub (DecSD ((x mod (() |^ n)),n,k))),(n + 1),k))*>) . j
then A40: j in Seg (n + 1) by ;
A41: j in dom (SDSub2INT (SD2SDSub (DecSD ((x mod (() |^ n)),n,k)))) by ;
now :: thesis: (SDSub2INT (SD2SDSub (DecSD ((x mod (() |^ n)),n,k)))) . j = (xnpp ^ <*(SDSub2INTDigit ((SD2SDSub (DecSD ((x mod (() |^ n)),n,k))),(n + 1),k))*>) . j
per cases ( j in Seg n or j = n + 1 ) by ;
suppose A42: j in Seg n ; :: thesis: (SDSub2INT (SD2SDSub (DecSD ((x mod (() |^ n)),n,k)))) . j = (xnpp ^ <*(SDSub2INTDigit ((SD2SDSub (DecSD ((x mod (() |^ n)),n,k))),(n + 1),k))*>) . j
then j in dom xnpp by ;
then (xnpp ^ <*(SDSub2INTDigit ((SD2SDSub (DecSD ((x mod (() |^ n)),n,k))),(n + 1),k))*>) . j = xnpp . j by FINSEQ_1:def 7
.= SDSub2INTDigit ((SD2SDSub (DecSD ((x mod (() |^ n)),n,k))),j,k) by
.= (SDSub2INT (SD2SDSub (DecSD ((x mod (() |^ n)),n,k)))) /. j by
.= (SDSub2INT (SD2SDSub (DecSD ((x mod (() |^ n)),n,k)))) . j by ;
hence (SDSub2INT (SD2SDSub (DecSD ((x mod (() |^ n)),n,k)))) . j = (xnpp ^ <*(SDSub2INTDigit ((SD2SDSub (DecSD ((x mod (() |^ n)),n,k))),(n + 1),k))*>) . j ; :: thesis: verum
end;
suppose A43: j = n + 1 ; :: thesis: (SDSub2INT (SD2SDSub (DecSD ((x mod (() |^ n)),n,k)))) . j = (xnpp ^ <*(SDSub2INTDigit ((SD2SDSub (DecSD ((x mod (() |^ n)),n,k))),(n + 1),k))*>) . j
A44: j in dom (SDSub2INT (SD2SDSub (DecSD ((x mod (() |^ n)),n,k)))) by ;
(xnpp ^ <*(SDSub2INTDigit ((SD2SDSub (DecSD ((x mod (() |^ n)),n,k))),(n + 1),k))*>) . j = SDSub2INTDigit ((SD2SDSub (DecSD ((x mod (() |^ n)),n,k))),(n + 1),k) by
.= (SDSub2INT (SD2SDSub (DecSD ((x mod (() |^ n)),n,k)))) /. (n + 1) by
.= (SDSub2INT (SD2SDSub (DecSD ((x mod (() |^ n)),n,k)))) . j by ;
hence (SDSub2INT (SD2SDSub (DecSD ((x mod (() |^ n)),n,k)))) . j = (xnpp ^ <*(SDSub2INTDigit ((SD2SDSub (DecSD ((x mod (() |^ n)),n,k))),(n + 1),k))*>) . j ; :: thesis: verum
end;
end;
end;
hence (SDSub2INT (SD2SDSub (DecSD ((x mod (() |^ n)),n,k)))) . j = (xnpp ^ <*(SDSub2INTDigit ((SD2SDSub (DecSD ((x mod (() |^ n)),n,k))),(n + 1),k))*>) . j ; :: thesis: verum
end;
len xp = len (xpp ^ <*(SDSub2INTDigit ((SD2SDSub (DecSD (x,(n + 1),k))),(n + 1),k))*>) by ;
then A45: xp = xpp ^ <*(SDSub2INTDigit ((SD2SDSub (DecSD (x,(n + 1),k))),(n + 1),k))*> by ;
len (xp ^ <*(SDSub2INTDigit ((SD2SDSub (DecSD (x,(n + 1),k))),((n + 1) + 1),k))*>) = (n + 1) + 1 by ;
then len (SDSub2INT (SD2SDSub (DecSD (x,(n + 1),k)))) = len (xp ^ <*(SDSub2INTDigit ((SD2SDSub (DecSD (x,(n + 1),k))),((n + 1) + 1),k))*>) by CARD_1:def 7;
then SDSub2INT (SD2SDSub (DecSD (x,(n + 1),k))) = xp ^ <*(SDSub2INTDigit ((SD2SDSub (DecSD (x,(n + 1),k))),((n + 1) + 1),k))*> by ;
then A46: Sum (SDSub2INT (SD2SDSub (DecSD (x,(n + 1),k)))) = (Sum xp) + (SDSub2INTDigit ((SD2SDSub (DecSD (x,(n + 1),k))),((n + 1) + 1),k)) by RVSUM_1:74
.= ((Sum xnpp) + (SDSub2INTDigit ((SD2SDSub (DecSD (x,(n + 1),k))),(n + 1),k))) + (SDSub2INTDigit ((SD2SDSub (DecSD (x,(n + 1),k))),((n + 1) + 1),k)) by ;
set RNDIG = (() |^ n) * (DigA ((DecSD (x,(n + 1),k)),(n + 1)));
set RNSDC = (() |^ n) * (SDSub_Add_Carry ((DigA ((DecSD (x,(n + 1),k)),n)),k));
len (xnpp ^ <*(SDSub2INTDigit ((SD2SDSub (DecSD ((x mod (() |^ n)),n,k))),(n + 1),k))*>) = n + 1 by ;
then SDSub2INT (SD2SDSub (DecSD ((x mod (() |^ n)),n,k))) = xnpp ^ <*(SDSub2INTDigit ((SD2SDSub (DecSD ((x mod (() |^ n)),n,k))),(n + 1),k))*> by ;
then A48: (x mod (() |^ n)) + 0 = (Sum xnpp) + (SDSub2INTDigit ((SD2SDSub (DecSD ((x mod (() |^ n)),n,k))),(n + 1),k)) by ;
A49: SDSub2INTDigit ((SD2SDSub (DecSD (x,(n + 1),k))),(n + 1),k) = (() |^ n) * (DigB_SDSub ((SD2SDSub (DecSD (x,(n + 1),k))),(n + 1))) by NAT_D:34
.= (() |^ n) * (SD2SDSubDigitS ((DecSD (x,(n + 1),k)),(n + 1),k)) by
.= (() |^ n) * (SD2SDSubDigit ((DecSD (x,(n + 1),k)),(n + 1),k)) by
.= (() |^ n) * ((SDSub_Add_Data ((DigA ((DecSD (x,(n + 1),k)),(n + 1))),k)) + (SDSub_Add_Carry ((DigA ((DecSD (x,(n + 1),k)),((n + 1) -' 1))),k))) by
.= (() |^ n) * ((SDSub_Add_Data ((DigA ((DecSD (x,(n + 1),k)),(n + 1))),k)) + (SDSub_Add_Carry ((DigA ((DecSD (x,(n + 1),k)),n)),k))) by NAT_D:34
.= (((() |^ n) * (DigA ((DecSD (x,(n + 1),k)),(n + 1)))) - (((() |^ n) * ()) * (SDSub_Add_Carry ((DigA ((DecSD (x,(n + 1),k)),(n + 1))),k)))) + ((() |^ n) * (SDSub_Add_Carry ((DigA ((DecSD (x,(n + 1),k)),n)),k)))
.= (((() |^ n) * (DigA ((DecSD (x,(n + 1),k)),(n + 1)))) - ((() |^ (n + 1)) * (SDSub_Add_Carry ((DigA ((DecSD (x,(n + 1),k)),(n + 1))),k)))) + ((() |^ n) * (SDSub_Add_Carry ((DigA ((DecSD (x,(n + 1),k)),n)),k))) by NEWTON:6 ;
SDSub2INTDigit ((SD2SDSub (DecSD ((x mod (() |^ n)),n,k))),(n + 1),k) = (() |^ n) * (DigB_SDSub ((SD2SDSub (DecSD ((x mod (() |^ n)),n,k))),(n + 1))) by NAT_D:34
.= (() |^ n) * (SD2SDSubDigitS ((DecSD ((x mod (() |^ n)),n,k)),(n + 1),k)) by
.= (() |^ n) * (SD2SDSubDigit ((DecSD ((x mod (() |^ n)),n,k)),(n + 1),k)) by
.= (() |^ n) * (SDSub_Add_Carry ((DigA ((DecSD ((x mod (() |^ n)),n,k)),((n + 1) -' 1))),k)) by Def6
.= (() |^ n) * (SDSub_Add_Carry ((DigA ((DecSD ((x mod (() |^ n)),n,k)),n)),k)) by NAT_D:34
.= (() |^ n) * (SDSub_Add_Carry ((DigA ((DecSD (x,(n + 1),k)),n)),k)) by ;
then Sum (SDSub2INT (SD2SDSub (DecSD (x,(n + 1),k)))) = (((x mod (() |^ n)) + ((() |^ n) * (DigA ((DecSD (x,(n + 1),k)),(n + 1))))) - ((() |^ n) * (SDSub_Add_Carry ((DigA ((DecSD (x,(n + 1),k)),n)),k)))) + ((() |^ n) * (SDSub_Add_Carry ((DigA ((DecSD (x,(n + 1),k)),n)),k))) by A46, A48, A49, A9
.= (x mod (() |^ n)) + ((() |^ n) * (x div (() |^ n))) by ;
hence x = SDSub2IntOut (SD2SDSub (DecSD (x,(n + 1),k))) by ; :: thesis: verum
end;
A50: S1[1]
proof
A51: 1 in Seg 1 by FINSEQ_1:1;
2 - 1 = 1 ;
then A52: 2 -' 1 = 1 by XREAL_0:def 2;
let k, x be Nat; :: thesis: ( k >= 2 & x is_represented_by 1,k implies x = SDSub2IntOut (SD2SDSub (DecSD (x,1,k))) )
assume that
A53: k >= 2 and
A54: x is_represented_by 1,k ; :: thesis: x = SDSub2IntOut (SD2SDSub (DecSD (x,1,k)))
set X = DecSD (x,1,k);
reconsider CRY = () * (SDSub_Add_Carry ((DigA ((DecSD (x,1,k)),1)),k)) as Integer ;
reconsider DIG2 = CRY as Element of INT by INT_1:def 2;
reconsider DIG1 = (DigA ((DecSD (x,1,k)),1)) - CRY as Element of INT by INT_1:def 2;
A55: 1 in Seg (1 + 1) by FINSEQ_1:1;
A56: len (SDSub2INT (SD2SDSub (DecSD (x,1,k)))) = 1 + 1 by CARD_1:def 7;
then A57: 1 in dom (SDSub2INT (SD2SDSub (DecSD (x,1,k)))) by ;
A58: 2 in Seg (1 + 1) by FINSEQ_1:1;
then A59: 2 in dom (SDSub2INT (SD2SDSub (DecSD (x,1,k)))) by ;
(SDSub2INT (SD2SDSub (DecSD (x,1,k)))) /. 2 = SDSub2INTDigit ((SD2SDSub (DecSD (x,1,k))),2,k) by
.= () * (DigB_SDSub ((SD2SDSub (DecSD (x,1,k))),2)) by A52
.= () * (SD2SDSubDigitS ((DecSD (x,1,k)),2,k)) by
.= () * (SD2SDSubDigit ((DecSD (x,1,k)),2,k)) by
.= () * (SDSub_Add_Carry ((DigA ((DecSD (x,1,k)),1)),k)) by ;
then A60: (SDSub2INT (SD2SDSub (DecSD (x,1,k)))) . 2 = CRY by ;
(SDSub2INT (SD2SDSub (DecSD (x,1,k)))) /. 1 = SDSub2INTDigit ((SD2SDSub (DecSD (x,1,k))),1,k) by
.= (() |^ 0) * (DigB_SDSub ((SD2SDSub (DecSD (x,1,k))),1)) by XREAL_1:232
.= 1 * (DigB_SDSub ((SD2SDSub (DecSD (x,1,k))),1)) by NEWTON:4
.= SD2SDSubDigitS ((DecSD (x,1,k)),1,k) by
.= SD2SDSubDigit ((DecSD (x,1,k)),1,k) by
.= (SDSub_Add_Data ((DigA ((DecSD (x,1,k)),1)),k)) + (SDSub_Add_Carry ((DigA ((DecSD (x,1,k)),(1 -' 1))),k)) by
.= (SDSub_Add_Data ((DigA ((DecSD (x,1,k)),1)),k)) + (SDSub_Add_Carry ((DigA ((DecSD (x,1,k)),0)),k)) by XREAL_1:232