:: RADIX_1 semantic presentation

begin


theorem Th1: :: RADIX_1:1
for n, k being Nat st n mod k = k - 1 holds
(n + 1) mod k = 0 by NAT_D:69;

theorem Th2: :: RADIX_1:2
for n, k being Nat st n mod k < k - 1 holds
(n + 1) mod k = (n mod k) + 1 by NAT_D:70;

theorem Th3: :: RADIX_1:3
for m, k, n being Nat st m <> 0 holds
(k mod (m * n)) mod n = k mod n
proof
let m, k, n be Nat; ::_thesis: ( m <> 0 implies (k mod (m * n)) mod n = k mod n )
assume A1: m <> 0 ; ::_thesis: (k mod (m * n)) mod n = k mod n
percases ( n <> 0 or n = 0 ) ;
supposeA2: n <> 0 ; ::_thesis: (k mod (m * n)) mod n = k mod n
reconsider k9 = k, m9 = m, n9 = n as Integer ;
 m9 * n9 <> 0 by A1, A2, XCMPLX_1:6;
hence (k mod (m * n)) mod n = (k9 - ((k9 div (m9 * n9)) * (m9 * n9))) mod n9 by INT_1:def_10
.= (k9 + ((- (m9 * (k9 div (m9 * n9)))) * n9)) mod n9
.= k mod n by EULER_1:12 ;
::_thesis: verum
end;
supposeA3: n = 0 ; ::_thesis: (k mod (m * n)) mod n = k mod n
hence (k mod (m * n)) mod n = 0 by NAT_D:def_2
.= k mod n by A3, NAT_D:def_2 ;
::_thesis: verum
end;
end;
end;

theorem :: RADIX_1:4
for k, n being Nat holds
( not k <> 0 or (n + 1) mod k = 0 or (n + 1) mod k = (n mod k) + 1 )
proof
let k, n be Nat; ::_thesis: ( not k <> 0 or (n + 1) mod k = 0 or (n + 1) mod k = (n mod k) + 1 )
assume A1: k <> 0 ; ::_thesis: ( (n + 1) mod k = 0 or (n + 1) mod k = (n mod k) + 1 )
then  k >= 1 by NAT_1:14;
then reconsider K = k - 1 as Element of NAT by INT_1:3, XREAL_1:48;
 n mod k < (k - 1) + 1 by A1, NAT_D:1;
then A2: n mod k <= K by NAT_1:13;
percases ( n mod k < k - 1 or n mod k = k - 1 ) by A2, XXREAL_0:1;
suppose n mod k < k - 1 ; ::_thesis: ( (n + 1) mod k = 0 or (n + 1) mod k = (n mod k) + 1 )
hence  ( (n + 1) mod k = 0 or (n + 1) mod k = (n mod k) + 1 ) by Th2; ::_thesis: verum
end;
suppose n mod k = k - 1 ; ::_thesis: ( (n + 1) mod k = 0 or (n + 1) mod k = (n mod k) + 1 )
hence  ( (n + 1) mod k = 0 or (n + 1) mod k = (n mod k) + 1 ) by Th1; ::_thesis: verum
end;
end;
end;


theorem Th5: :: RADIX_1:5
for i, k, n being Nat st i <> 0 & k <> 0 holds
(n mod (i |^ k)) div (i |^ (k -' 1)) < i
proof
let i, k, n be Nat; ::_thesis: ( i <> 0 & k <> 0 implies (n mod (i |^ k)) div (i |^ (k -' 1)) < i )
assume that
A1: i <> 0 and
A2: k <> 0 ; ::_thesis: (n mod (i |^ k)) div (i |^ (k -' 1)) < i
A3: n mod (i |^ k) < i |^ k by A1, NAT_D:1, PREPOWER:6;
reconsider n = n, i = i, k = k as Element of NAT by ORDINAL1:def_12;
set I1 = i |^ (k -' 1);
set T = n mod (i |^ k);
 i |^ k = i * (i |^ (k -' 1)) by A1, A2, PEPIN:26;
then (n mod (i |^ k)) mod (i |^ (k -' 1)) = n mod (i |^ (k -' 1)) by A1, Th3
.= n - ((i |^ (k -' 1)) * (n div (i |^ (k -' 1)))) by A1, NEWTON:63, PREPOWER:6 ;
then  n mod (i |^ k) = ((i |^ (k -' 1)) * ((n mod (i |^ k)) div (i |^ (k -' 1)))) + (n - ((i |^ (k -' 1)) * (n div (i |^ (k -' 1))))) by A1, NAT_D:2, PREPOWER:6;
then A4: ((i |^ (k -' 1)) * ((n mod (i |^ k)) div (i |^ (k -' 1)))) + (n - ((i |^ (k -' 1)) * (n div (i |^ (k -' 1))))) < i * (i |^ (k -' 1)) by A1, A2, A3, PEPIN:26;
A5: i |^ (k -' 1) <> 0 by A1, PREPOWER:6;
 [\(n / (i |^ (k -' 1)))/] <= n / (i |^ (k -' 1)) by INT_1:def_6;
then  ( n div (i |^ (k -' 1)) = [\(n / (i |^ (k -' 1)))/] & ((n mod (i |^ k)) div (i |^ (k -' 1))) + [\(n / (i |^ (k -' 1)))/] <= ((n mod (i |^ k)) div (i |^ (k -' 1))) + (n / (i |^ (k -' 1))) ) by INT_1:def_9, XREAL_1:6;
then A6: (((n mod (i |^ k)) div (i |^ (k -' 1))) + [\(n / (i |^ (k -' 1)))/]) - [\(n / (i |^ (k -' 1)))/] <= (((n mod (i |^ k)) div (i |^ (k -' 1))) + (n / (i |^ (k -' 1)))) - (n div (i |^ (k -' 1))) by XREAL_1:9;
 i |^ (k -' 1) > 0 by A1, PREPOWER:6;
then  ((((i |^ (k -' 1)) * ((n mod (i |^ k)) div (i |^ (k -' 1)))) + n) - ((i |^ (k -' 1)) * (n div (i |^ (k -' 1))))) / (i |^ (k -' 1)) < (i * (i |^ (k -' 1))) / (i |^ (k -' 1)) by A4, XREAL_1:74;
then  ((((i |^ (k -' 1)) * ((n mod (i |^ k)) div (i |^ (k -' 1)))) / (i |^ (k -' 1))) + (n / (i |^ (k -' 1)))) - (((i |^ (k -' 1)) * (n div (i |^ (k -' 1)))) / (i |^ (k -' 1))) < (i * (i |^ (k -' 1))) / (i |^ (k -' 1)) by XCMPLX_1:124;
then  (((n mod (i |^ k)) div (i |^ (k -' 1))) + (n / (i |^ (k -' 1)))) - (((i |^ (k -' 1)) * (n div (i |^ (k -' 1)))) / (i |^ (k -' 1))) < (i * (i |^ (k -' 1))) / (i |^ (k -' 1)) by A5, XCMPLX_1:89;
then  (((n mod (i |^ k)) div (i |^ (k -' 1))) + (n / (i |^ (k -' 1)))) - (n div (i |^ (k -' 1))) < (i * (i |^ (k -' 1))) / (i |^ (k -' 1)) by A5, XCMPLX_1:89;
then  (((n mod (i |^ k)) div (i |^ (k -' 1))) + (n / (i |^ (k -' 1)))) - (n div (i |^ (k -' 1))) < i by A5, XCMPLX_1:89;
hence  (n mod (i |^ k)) div (i |^ (k -' 1)) < i by A6, XXREAL_0:2; ::_thesis: verum
end;

theorem :: RADIX_1:6
canceled;

theorem :: RADIX_1:7
for i2, i3, i1 being Integer st i2 > 0 & i3 >= 0 holds
(i1 mod (i2 * i3)) mod i3 = i1 mod i3
proof
let i2, i3, i1 be Integer; ::_thesis: ( i2 > 0 & i3 >= 0 implies (i1 mod (i2 * i3)) mod i3 = i1 mod i3 )
assume that
A1: i2 > 0 and
A2: i3 >= 0 ; ::_thesis: (i1 mod (i2 * i3)) mod i3 = i1 mod i3
percases ( i3 > 0 or i3 = 0 ) by A2;
suppose i3 > 0 ; ::_thesis: (i1 mod (i2 * i3)) mod i3 = i1 mod i3
then  i2 * i3 <> 0 by A1, XCMPLX_1:6;
then (i1 mod (i2 * i3)) mod i3 = (i1 - ((i1 div (i2 * i3)) * (i2 * i3))) mod i3 by INT_1:def_10
.= (i1 + ((- (i2 * (i1 div (i2 * i3)))) * i3)) mod i3 ;
hence  (i1 mod (i2 * i3)) mod i3 = i1 mod i3 by EULER_1:12; ::_thesis: verum
end;
supposeA3: i3 = 0 ; ::_thesis: (i1 mod (i2 * i3)) mod i3 = i1 mod i3
then  (i1 mod (i2 * i3)) mod i3 = 0 by INT_1:def_10;
hence  (i1 mod (i2 * i3)) mod i3 = i1 mod i3 by A3, INT_1:def_10; ::_thesis: verum
end;
end;
end;

begin

definition
let n be Nat;
func Radix n ->  Element of NAT  equals :: RADIX_1:def 1
2 to_power n;
correctness
coherence
2 to_power n is Element of NAT ;
by ORDINAL1:def_12;
end;

:: deftheorem  defines Radix RADIX_1:def_1_:_
 for n being Nat holds Radix n = 2 to_power n;

definition
let k be Nat;
funck -SD  ->  set  equals :: RADIX_1:def 2
 {  e where e is Element of INT : ( e <= (Radix k) - 1 & e >= (- (Radix k)) + 1 )  }  ;
correctness
coherence
{  e where e is Element of INT : ( e <= (Radix k) - 1 & e >= (- (Radix k)) + 1 )  }  is set ;
;
end;

:: deftheorem  defines -SD RADIX_1:def_2_:_
 for k being Nat holds k -SD =  {  e where e is Element of INT : ( e <= (Radix k) - 1 & e >= (- (Radix k)) + 1 )  }  ;

Lm1:  for k being Nat st k >= 2 holds
Radix k >= 2 + 2
proof
defpred S1[ Nat] means  Radix $1 >= 2 + 2;
let k be Nat; ::_thesis: ( k >= 2 implies Radix k >= 2 + 2 )
A1: for kk being Nat st kk >= 2 & S1[kk] holds
S1[kk + 1]
proof
let kk be Nat; ::_thesis: ( kk >= 2 & S1[kk] implies S1[kk + 1] )
assume  kk >= 2 ; ::_thesis: ( not S1[kk] or S1[kk + 1] )
Radix (kk + 1) = (2 to_power kk) * (2 to_power 1) by POWER:27
.= (Radix kk) * 2 by POWER:25 ;
then A2: Radix (kk + 1) >= Radix kk by XREAL_1:155;
assume  Radix kk >= 2 + 2 ; ::_thesis: S1[kk + 1]
hence  S1[kk + 1] by A2, XXREAL_0:2; ::_thesis: verum
end;
Radix 2 = 2 to_power (1 + 1)
.= (2 to_power 1) * (2 to_power 1) by POWER:27
.= 2 * (2 to_power 1) by POWER:25
.= 2 * 2 by POWER:25 ;
then A3: S1[2] ;
 for k being Nat st k >= 2 holds
S1[k] from NAT_1:sch_8(A3, A1);
hence  ( k >= 2 implies Radix k >= 2 + 2 ) ; ::_thesis: verum
end;

theorem Th8: :: RADIX_1:8
for e being set holds
( e in 0 -SD iff e = 0 )
proof
let e be set ; ::_thesis: ( e in 0 -SD iff e = 0 )
A1: Radix 0 = 1 by POWER:24;
hereby  ::_thesis: ( e = 0 implies e in 0 -SD )
assume  e in 0 -SD ; ::_thesis: e = 0
then  ex b being Element of INT st
( e = b & b <= 0 & b >= 0 ) by A1;
hence  e = 0 ; ::_thesis: verum
end;
assume A2: e = 0 ; ::_thesis: e in 0 -SD
then  e is Element of INT by INT_1:def_2;
hence  e in 0 -SD by A1, A2; ::_thesis: verum
end;

theorem :: RADIX_1:9
0 -SD = {0} by Th8, TARSKI:def_1;

theorem Th10: :: RADIX_1:10
for k being Nat holds k -SD c= (k + 1) -SD
proof
let k be Nat; ::_thesis: k -SD c= (k + 1) -SD
let e be set ; :: according to TARSKI:def_3 ::_thesis: ( not e in k -SD or e in (k + 1) -SD )
assume  e in k -SD ; ::_thesis: e in (k + 1) -SD
then consider g being Element of INT  such that
A1: e = g and
A2: g <= (Radix k) - 1 and
A3: g >= (- (Radix k)) + 1 ;
 k < k + 1 by NAT_1:13;
then A4: 2 to_power k < 2 to_power (k + 1) by POWER:39;
then  - (Radix k) > - (Radix (k + 1)) by XREAL_1:24;
then  (- (Radix k)) + 1 > (- (Radix (k + 1))) + 1 by XREAL_1:6;
then A5: g >= (- (Radix (k + 1))) + 1 by A3, XXREAL_0:2;
 (Radix k) - 1 < (Radix (k + 1)) - 1 by A4, XREAL_1:9;
then  g <= (Radix (k + 1)) - 1 by A2, XXREAL_0:2;
hence  e in (k + 1) -SD by A1, A5; ::_thesis: verum
end;

theorem Th11: :: RADIX_1:11
for e being set
for k being Nat st e in k -SD holds
e is Integer
proof
let e be set ; ::_thesis: for k being Nat st e in k -SD holds
e is Integer
let k be Nat; ::_thesis: ( e in k -SD implies e is Integer )
assume  e in k -SD ; ::_thesis: e is Integer
then  ex t being Element of INT st
( e = t & t <= (Radix k) - 1 & t >= (- (Radix k)) + 1 ) ;
hence  e is Integer ; ::_thesis: verum
end;

theorem Th12: :: RADIX_1:12
for k being Nat holds k -SD c= INT
proof
let k be Nat; ::_thesis: k -SD c= INT
let e be set ; :: according to TARSKI:def_3 ::_thesis: ( not e in k -SD or e in INT )
assume  e in k -SD ; ::_thesis: e in INT
then  e is Integer by Th11;
hence  e in INT by INT_1:def_2; ::_thesis: verum
end;

theorem Th13: :: RADIX_1:13
for i1 being Integer
for k being Nat st i1 in k -SD holds
( i1 <= (Radix k) - 1 & i1 >= (- (Radix k)) + 1 )
proof
let i1 be Integer; ::_thesis: for k being Nat st i1 in k -SD holds
( i1 <= (Radix k) - 1 & i1 >= (- (Radix k)) + 1 )
let k be Nat; ::_thesis: ( i1 in k -SD implies ( i1 <= (Radix k) - 1 & i1 >= (- (Radix k)) + 1 ) )
assume  i1 in k -SD ; ::_thesis: ( i1 <= (Radix k) - 1 & i1 >= (- (Radix k)) + 1 )
then  ex i being Element of INT st
( i = i1 & i <= (Radix k) - 1 & i >= (- (Radix k)) + 1 ) ;
hence  ( i1 <= (Radix k) - 1 & i1 >= (- (Radix k)) + 1 ) ; ::_thesis: verum
end;

theorem Th14: :: RADIX_1:14
for k being Nat holds 0 in k -SD
proof
let k be Nat; ::_thesis: 0 in k -SD
defpred S1[ Nat] means  0 in $1 -SD ;
A1: for k being Nat st S1[k] holds
S1[k + 1]
proof
let kk be Nat; ::_thesis: ( S1[kk] implies S1[kk + 1] )
assume A2: 0 in kk -SD ; ::_thesis: S1[kk + 1]
 kk -SD c= (kk + 1) -SD by Th10;
hence  S1[kk + 1] by A2; ::_thesis: verum
end;
A3: S1[ 0 ] by Th8;
 for k being Nat holds S1[k] from NAT_1:sch_2(A3, A1);
hence  0 in k -SD ; ::_thesis: verum
end;

registration
let k be Nat;
clusterk -SD  ->  non empty ;
coherence
 not k -SD is empty by Th14;
end;

definition
let k be Nat;
:: original: -SD
redefine funck -SD  ->  non empty Subset of INT;
coherence
 k -SD is non empty Subset of INT by Th12;
end;

begin

theorem Th15: :: RADIX_1:15
for i, n, k being Nat
for a being Tuple of n,k -SD st i in Seg n holds
a . i is Element of k -SD
proof
let i, n, k be Nat; ::_thesis: for a being Tuple of n,k -SD st i in Seg n holds
a . i is Element of k -SD
let a be Tuple of n,k -SD ; ::_thesis: ( i in Seg n implies a . i is Element of k -SD )
A1: len a = n by CARD_1:def_7;
assume  i in Seg n ; ::_thesis: a . i is Element of k -SD
then  i in dom a by A1, FINSEQ_1:def_3;
then A2: a . i in rng a by FUNCT_1:def_3;
 rng a c= k -SD by FINSEQ_1:def_4;
hence  a . i is Element of k -SD by A2; ::_thesis: verum
end;

definition
let i, k, n be Nat;
let x be Tuple of n,k -SD ;
func DigA (x,i) ->  Integer equals :Def3: :: RADIX_1:def 3
x . i if i in Seg n
0  if i = 0
;
coherence
 ( ( i in Seg n implies x . i is Integer ) & ( i = 0 implies 0 is Integer ) ) by INT_1:def_2;
consistency
 for b1 being Integer st i in Seg n & i = 0 holds
( b1 = x . i iff b1 = 0 ) by FINSEQ_1:1;
end;

:: deftheorem Def3 defines DigA RADIX_1:def_3_:_
 for i, k, n being Nat
for x being Tuple of n,k -SD holds
( ( i in Seg n implies DigA (x,i) = x . i ) & ( i = 0 implies DigA (x,i) = 0 ) );

definition
let i, k, n be Nat;
let x be Tuple of n,k -SD ;
func DigB (x,i) ->  Element of INT  equals :: RADIX_1:def 4
 DigA (x,i);
coherence
 DigA (x,i) is Element of INT by INT_1:def_2;
end;

:: deftheorem  defines DigB RADIX_1:def_4_:_
 for i, k, n being Nat
for x being Tuple of n,k -SD holds DigB (x,i) = DigA (x,i);

theorem Th16: :: RADIX_1:16
for i, n, k being Nat
for a being Tuple of n,k -SD st i in Seg n holds
DigA (a,i) is Element of k -SD
proof
let i, n, k be Nat; ::_thesis: for a being Tuple of n,k -SD st i in Seg n holds
DigA (a,i) is Element of k -SD
let a be Tuple of n,k -SD ; ::_thesis: ( i in Seg n implies DigA (a,i) is Element of k -SD )
assume A1: i in Seg n ; ::_thesis: DigA (a,i) is Element of k -SD
then  a . i = DigA (a,i) by Def3;
hence  DigA (a,i) is Element of k -SD by A1, Th15; ::_thesis: verum
end;

theorem Th17: :: RADIX_1:17
for m being Nat
for x being Tuple of 1, INT st x /. 1 = m holds
x = <*m*>
proof
let m be Nat; ::_thesis: for x being Tuple of 1, INT st x /. 1 = m holds
x = <*m*>
let x be Tuple of 1, INT ; ::_thesis: ( x /. 1 = m implies x = <*m*> )
assume A1: x /. 1 = m ; ::_thesis: x = <*m*>
A2: len x = 1 by CARD_1:def_7;
then  x /. 1 = x . 1 by FINSEQ_4:15;
hence  x = <*m*> by A1, A2, FINSEQ_1:40; ::_thesis: verum
end;

definition
let i, k, n be Nat;
let x be Tuple of n,k -SD ;
func SubDigit (x,i,k) ->  Element of INT  equals :: RADIX_1:def 5
((Radix k) |^ (i -' 1)) * (DigB (x,i));
coherence
 ((Radix k) |^ (i -' 1)) * (DigB (x,i)) is Element of INT by INT_1:def_2;
end;

:: deftheorem  defines SubDigit RADIX_1:def_5_:_
 for i, k, n being Nat
for x being Tuple of n,k -SD holds SubDigit (x,i,k) = ((Radix k) |^ (i -' 1)) * (DigB (x,i));

definition
let n, k be Nat;
let x be Tuple of n,k -SD ;
func DigitSD x ->  Tuple of n, INT  means :Def6: :: RADIX_1:def 6
 for i being Nat st i in Seg n holds
it /. i = SubDigit (x,i,k);
existence
 ex b1 being Tuple of n, INT st
for i being Nat st i in Seg n holds
b1 /. i = SubDigit (x,i,k)
proof
deffunc H1( Nat) ->  Element of INT = SubDigit (x,$1,k);
consider z being FinSequence of INT  such that
A1: len z = n and
A2: for j being Nat st j in dom z holds
z . j = H1(j) from FINSEQ_2:sch_1();
A3: dom z = Seg n by A1, FINSEQ_1:def_3;
reconsider z = z as Tuple of n, INT by A1, CARD_1:def_7;
take  z ; ::_thesis: for i being Nat st i in Seg n holds
z /. i = SubDigit (x,i,k)
let i be Nat; ::_thesis: ( i in Seg n implies z /. i = SubDigit (x,i,k) )
assume A4: i in Seg n ; ::_thesis: z /. i = SubDigit (x,i,k)
then  i in dom z by A1, FINSEQ_1:def_3;
hence z /. i = z . i by PARTFUN1:def_6
.= SubDigit (x,i,k) by A2, A3, A4 ;
::_thesis: verum
end;
uniqueness
 for b1, b2 being Tuple of n, INT st ( for i being Nat st i in Seg n holds
b1 /. i = SubDigit (x,i,k) ) & ( for i being Nat st i in Seg n holds
b2 /. i = SubDigit (x,i,k) ) holds
b1 = b2
proof
let k1, k2 be Tuple of n, INT ; ::_thesis: ( ( for i being Nat st i in Seg n holds
k1 /. i = SubDigit (x,i,k) ) & ( for i being Nat st i in Seg n holds
k2 /. i = SubDigit (x,i,k) ) implies k1 = k2 )
assume that
A5: for i being Nat st i in Seg n holds
k1 /. i = SubDigit (x,i,k) and
A6: for i being Nat st i in Seg n holds
k2 /. i = SubDigit (x,i,k) ; ::_thesis: k1 = k2
A7: len k1 = n by CARD_1:def_7;
then A8: dom k1 = Seg n by FINSEQ_1:def_3;
A9: len k2 = n by CARD_1:def_7;
now__::_thesis:_for_j_being_Nat_st_j_in_dom_k1_holds_
k1_._j_=_k2_._j
let j be Nat; ::_thesis: ( j in dom k1 implies k1 . j = k2 . j )
assume A10: j in dom k1 ; ::_thesis: k1 . j = k2 . j
then A11: j in dom k2 by A9, A8, FINSEQ_1:def_3;
k1 . j = k1 /. j by A10, PARTFUN1:def_6
.= SubDigit (x,j,k) by A5, A8, A10
.= k2 /. j by A6, A8, A10
.= k2 . j by A11, PARTFUN1:def_6 ;
hence  k1 . j = k2 . j ; ::_thesis: verum
end;
hence  k1 = k2 by A7, A9, FINSEQ_2:9; ::_thesis: verum
end;
end;

:: deftheorem Def6 defines DigitSD RADIX_1:def_6_:_
 for n, k being Nat
for x being Tuple of n,k -SD
for b4 being Tuple of n, INT holds
( b4 = DigitSD x iff for i being Nat st i in Seg n holds
b4 /. i = SubDigit (x,i,k) );

definition
let n, k be Nat;
let x be Tuple of n,k -SD ;
func SDDec x ->  Integer equals :: RADIX_1:def 7
 Sum (DigitSD x);
coherence
 Sum (DigitSD x) is Integer ;
end;

:: deftheorem  defines SDDec RADIX_1:def_7_:_
 for n, k being Nat
for x being Tuple of n,k -SD holds SDDec x = Sum (DigitSD x);

definition
let i, k, x be Nat;
func DigitDC (x,i,k) ->  Element of k -SD  equals :: RADIX_1:def 8
(x mod ((Radix k) |^ i)) div ((Radix k) |^ (i -' 1));
coherence
 (x mod ((Radix k) |^ i)) div ((Radix k) |^ (i -' 1)) is Element of k -SD
proof
reconsider i = i, k = k as Element of NAT by ORDINAL1:def_12;
set T = (Radix k) |^ i;
set S = (Radix k) |^ (i -' 1);
defpred S1[ Nat] means ($1 mod ((Radix k) |^ i)) div ((Radix k) |^ (i -' 1)) is Element of k -SD ;
A1: 0 in k -SD by Th14;
A2: Radix k <> 0 by POWER:34;
then A3: (Radix k) |^ (i -' 1) > 0 by NAT_1:14, PREPOWER:11;
then A4: 0 div ((Radix k) |^ (i -' 1)) = 0 by NAT_D:27;
A5: Radix k >= 1 by A2, NAT_1:14;
A6: for x being Nat st S1[x] holds
S1[x + 1]
proof
reconsider R = (Radix k) - 1 as Element of NAT by A5, INT_1:3, XREAL_1:48;
let xx be Nat; ::_thesis: ( S1[xx] implies S1[xx + 1] )
assume  (xx mod ((Radix k) |^ i)) div ((Radix k) |^ (i -' 1)) is Element of k -SD ; ::_thesis: S1[xx + 1]
set X = ((xx + 1) mod ((Radix k) |^ i)) div ((Radix k) |^ (i -' 1));
percases ( i = 0 or i > 0 ) ;
supposeA7: i = 0 ; ::_thesis: S1[xx + 1]
(Radix k) |^ i = (Radix k) to_power i
.= 1 by A7, POWER:24 ;
then (xx + 1) mod ((Radix k) |^ i) = ((xx + 1) * 1) mod 1
.= 0 by NAT_D:13 ;
then  ((xx + 1) mod ((Radix k) |^ i)) div ((Radix k) |^ (i -' 1)) = 0 by A3, NAT_D:27;
hence  S1[xx + 1] by Th14; ::_thesis: verum
end;
supposeA8: i > 0 ; ::_thesis: S1[xx + 1]
 - 1 >= - (Radix k) by A5, XREAL_1:24;
then A9: ( ((xx + 1) mod ((Radix k) |^ i)) div ((Radix k) |^ (i -' 1)) is Element of INT & 0 >= (- (Radix k)) + 1 ) by INT_1:def_2, XREAL_1:59;
 ((xx + 1) mod ((Radix k) |^ i)) div ((Radix k) |^ (i -' 1)) < ((Radix k) - 1) + 1 by A2, A8, Th5;
then  ((xx + 1) mod ((Radix k) |^ i)) div ((Radix k) |^ (i -' 1)) <= R by NAT_1:13;
then  ((xx + 1) mod ((Radix k) |^ i)) div ((Radix k) |^ (i -' 1)) in k -SD by A9;
hence  S1[xx + 1] ; ::_thesis: verum
end;
end;
end;
 (Radix k) |^ i > 0 by A2, NAT_1:14, PREPOWER:11;
then A10: S1[ 0 ] by A4, A1, NAT_D:24;
 for x being Nat holds S1[x] from NAT_1:sch_2(A10, A6);
hence  (x mod ((Radix k) |^ i)) div ((Radix k) |^ (i -' 1)) is Element of k -SD ; ::_thesis: verum
end;
end;

:: deftheorem  defines DigitDC RADIX_1:def_8_:_
 for i, k, x being Nat holds DigitDC (x,i,k) = (x mod ((Radix k) |^ i)) div ((Radix k) |^ (i -' 1));

definition
let k, n, x be Nat;
func DecSD (x,n,k) ->  Tuple of n,k -SD  means :Def9: :: RADIX_1:def 9
 for i being Nat st i in Seg n holds
DigA (it,i) = DigitDC (x,i,k);
existence
 ex b1 being Tuple of n,k -SD st
for i being Nat st i in Seg n holds
DigA (b1,i) = DigitDC (x,i,k)
proof
deffunc H1( Nat) ->  Element of k -SD = DigitDC (x,$1,k);
consider z being FinSequence of k -SD  such that
A1: len z = n and
A2: for j being Nat st j in dom z holds
z . j = H1(j) from FINSEQ_2:sch_1();
A3: dom z = Seg n by A1, FINSEQ_1:def_3;
reconsider z = z as Tuple of n,k -SD by A1, CARD_1:def_7;
take  z ; ::_thesis: for i being Nat st i in Seg n holds
DigA (z,i) = DigitDC (x,i,k)
let i be Nat; ::_thesis: ( i in Seg n implies DigA (z,i) = DigitDC (x,i,k) )
assume A4: i in Seg n ; ::_thesis: DigA (z,i) = DigitDC (x,i,k)
hence  DigA (z,i) = z . i by Def3
.= DigitDC (x,i,k) by A2, A3, A4 ;
::_thesis: verum
end;
uniqueness
 for b1, b2 being Tuple of n,k -SD st ( for i being Nat st i in Seg n holds
DigA (b1,i) = DigitDC (x,i,k) ) & ( for i being Nat st i in Seg n holds
DigA (b2,i) = DigitDC (x,i,k) ) holds
b1 = b2
proof
let k1, k2 be Tuple of n,k -SD ; ::_thesis: ( ( for i being Nat st i in Seg n holds
DigA (k1,i) = DigitDC (x,i,k) ) & ( for i being Nat st i in Seg n holds
DigA (k2,i) = DigitDC (x,i,k) ) implies k1 = k2 )
assume that
A5: for i being Nat st i in Seg n holds
DigA (k1,i) = DigitDC (x,i,k) and
A6: for i being Nat st i in Seg n holds
DigA (k2,i) = DigitDC (x,i,k) ; ::_thesis: k1 = k2
A7: len k1 = n by CARD_1:def_7;
then A8: dom k1 = Seg n by FINSEQ_1:def_3;
A9: now__::_thesis:_for_j_being_Nat_st_j_in_dom_k1_holds_
k1_._j_=_k2_._j
let j be Nat; ::_thesis: ( j in dom k1 implies k1 . j = k2 . j )
assume A10: j in dom k1 ; ::_thesis: k1 . j = k2 . j
then k1 . j = DigA (k1,j) by A8, Def3
.= DigitDC (x,j,k) by A5, A8, A10
.= DigA (k2,j) by A6, A8, A10
.= k2 . j by A8, A10, Def3 ;
hence  k1 . j = k2 . j ; ::_thesis: verum
end;
 len k2 = n by CARD_1:def_7;
hence  k1 = k2 by A7, A9, FINSEQ_2:9; ::_thesis: verum
end;
end;

:: deftheorem Def9 defines DecSD RADIX_1:def_9_:_
 for k, n, x being Nat
for b4 being Tuple of n,k -SD holds
( b4 = DecSD (x,n,k) iff for i being Nat st i in Seg n holds
DigA (b4,i) = DigitDC (x,i,k) );

begin

definition
let x be Integer;
func SD_Add_Carry x ->  Integer equals :Def10: :: RADIX_1:def 10
1 if x > 2
- 1 if x < - 2
otherwise  0 ;
coherence
 ( ( x > 2 implies 1 is Integer ) & ( x < - 2 implies - 1 is Integer ) & ( not x > 2 & not x < - 2 implies 0 is Integer ) ) ;
consistency
 for b1 being Integer st x > 2 & x < - 2 holds
( b1 = 1 iff b1 = - 1 ) ;
end;

:: deftheorem Def10 defines SD_Add_Carry RADIX_1:def_10_:_
 for x being Integer holds
( ( x > 2 implies SD_Add_Carry x = 1 ) & ( x < - 2 implies SD_Add_Carry x = - 1 ) & ( not x > 2 & not x < - 2 implies SD_Add_Carry x = 0 ) );

theorem Th18: :: RADIX_1:18
SD_Add_Carry 0 = 0 by Def10;

Lm2:  for x being Integer holds
( - 1 <= SD_Add_Carry x & SD_Add_Carry x <= 1 )
proof
let x be Integer; ::_thesis: ( - 1 <= SD_Add_Carry x & SD_Add_Carry x <= 1 )
percases ( x < - 2 or ( - 2 <= x & x <= 2 ) or x > 2 ) ;
suppose x < - 2 ; ::_thesis: ( - 1 <= SD_Add_Carry x & SD_Add_Carry x <= 1 )
hence  ( - 1 <= SD_Add_Carry x & SD_Add_Carry x <= 1 ) by Def10; ::_thesis: verum
end;
suppose ( - 2 <= x & x <= 2 ) ; ::_thesis: ( - 1 <= SD_Add_Carry x & SD_Add_Carry x <= 1 )
hence  ( - 1 <= SD_Add_Carry x & SD_Add_Carry x <= 1 ) by Def10; ::_thesis: verum
end;
suppose x > 2 ; ::_thesis: ( - 1 <= SD_Add_Carry x & SD_Add_Carry x <= 1 )
hence  ( - 1 <= SD_Add_Carry x & SD_Add_Carry x <= 1 ) by Def10; ::_thesis: verum
end;
end;
end;

definition
let x be Integer;
let k be Nat;
func SD_Add_Data (x,k) ->  Integer equals :: RADIX_1:def 11
x - ((SD_Add_Carry x) * (Radix k));
coherence
 x - ((SD_Add_Carry x) * (Radix k)) is Integer ;
end;

:: deftheorem  defines SD_Add_Data RADIX_1:def_11_:_
 for x being Integer
for k being Nat holds SD_Add_Data (x,k) = x - ((SD_Add_Carry x) * (Radix k));

theorem :: RADIX_1:19
for k being Nat holds SD_Add_Data (0,k) = 0 by Th18;

theorem Th20: :: RADIX_1:20
for i1, i2 being Integer
for k being Nat st k >= 2 & i1 in k -SD & i2 in k -SD holds
( (- (Radix k)) + 2 <= SD_Add_Data ((i1 + i2),k) & SD_Add_Data ((i1 + i2),k) <= (Radix k) - 2 )
proof
let i1, i2 be Integer; ::_thesis: for k being Nat st k >= 2 & i1 in k -SD & i2 in k -SD holds
( (- (Radix k)) + 2 <= SD_Add_Data ((i1 + i2),k) & SD_Add_Data ((i1 + i2),k) <= (Radix k) - 2 )
let k be Nat; ::_thesis: ( k >= 2 & i1 in k -SD & i2 in k -SD implies ( (- (Radix k)) + 2 <= SD_Add_Data ((i1 + i2),k) & SD_Add_Data ((i1 + i2),k) <= (Radix k) - 2 ) )
assume that
A1: k >= 2 and
A2: ( i1 in k -SD & i2 in k -SD ) ; ::_thesis: ( (- (Radix k)) + 2 <= SD_Add_Data ((i1 + i2),k) & SD_Add_Data ((i1 + i2),k) <= (Radix k) - 2 )
A3: ( (- (Radix k)) + 1 <= i1 & (- (Radix k)) + 1 <= i2 ) by A2, Th13;
set z = i1 + i2;
 ( i1 <= (Radix k) - 1 & i2 <= (Radix k) - 1 ) by A2, Th13;
then A4: i1 + i2 <= ((Radix k) - 1) + ((Radix k) - 1) by XREAL_1:7;
percases ( i1 + i2 < - 2 or ( - 2 <= i1 + i2 & i1 + i2 <= 2 ) or i1 + i2 > 2 ) ;
supposeA5: i1 + i2 < - 2 ; ::_thesis: ( (- (Radix k)) + 2 <= SD_Add_Data ((i1 + i2),k) & SD_Add_Data ((i1 + i2),k) <= (Radix k) - 2 )
 ((- (Radix k)) + 1) + (1 + (- (Radix k))) <= i1 + i2 by A3, XREAL_1:7;
then A6: ((- (Radix k)) + (1 + 1)) - (Radix k) <= i1 + i2 ;
 ( SD_Add_Carry (i1 + i2) = - 1 & (i1 + i2) + (Radix k) < (- 2) + (Radix k) ) by A5, Def10, XREAL_1:6;
hence  ( (- (Radix k)) + 2 <= SD_Add_Data ((i1 + i2),k) & SD_Add_Data ((i1 + i2),k) <= (Radix k) - 2 ) by A6, XREAL_1:20; ::_thesis: verum
end;
supposeA7: ( - 2 <= i1 + i2 & i1 + i2 <= 2 ) ; ::_thesis: ( (- (Radix k)) + 2 <= SD_Add_Data ((i1 + i2),k) & SD_Add_Data ((i1 + i2),k) <= (Radix k) - 2 )
A8: Radix k >= 2 + 2 by A1, Lm1;
then A9: (Radix k) - 2 >= 2 by XREAL_1:19;
 - (Radix k) <= - (2 + 2) by A8, XREAL_1:24;
then  - (Radix k) <= (- 2) + (- 2) ;
then A10: (- (Radix k)) - (- 2) <= - 2 by XREAL_1:20;
 SD_Add_Carry (i1 + i2) = 0 by A7, Def10;
hence  ( (- (Radix k)) + 2 <= SD_Add_Data ((i1 + i2),k) & SD_Add_Data ((i1 + i2),k) <= (Radix k) - 2 ) by A7, A9, A10, XXREAL_0:2; ::_thesis: verum
end;
supposeA11: i1 + i2 > 2 ; ::_thesis: ( (- (Radix k)) + 2 <= SD_Add_Data ((i1 + i2),k) & SD_Add_Data ((i1 + i2),k) <= (Radix k) - 2 )
A12: i1 + i2 <= (((Radix k) - 1) - 1) + (Radix k) by A4;
 ( SD_Add_Carry (i1 + i2) = 1 & (i1 + i2) - (Radix k) > 2 - (Radix k) ) by A11, Def10, XREAL_1:9;
hence  ( (- (Radix k)) + 2 <= SD_Add_Data ((i1 + i2),k) & SD_Add_Data ((i1 + i2),k) <= (Radix k) - 2 ) by A12, XREAL_1:20; ::_thesis: verum
end;
end;
end;

begin

definition
let n, x, k be Nat;
predx is_represented_by n,k means :Def12: :: RADIX_1:def 12
x < (Radix k) |^ n;
end;

:: deftheorem Def12 defines is_represented_by RADIX_1:def_12_:_
 for n, x, k being Nat holds
( x is_represented_by n,k iff x < (Radix k) |^ n );

theorem Th21: :: RADIX_1:21
for m, k being Nat st m is_represented_by 1,k holds
DigA ((DecSD (m,1,k)),1) = m
proof
let m, k be Nat; ::_thesis: ( m is_represented_by 1,k implies DigA ((DecSD (m,1,k)),1) = m )
assume  m is_represented_by 1,k ; ::_thesis: DigA ((DecSD (m,1,k)),1) = m
then A1: m < (Radix k) |^ 1 by Def12;
 1 in Seg 1 by FINSEQ_1:1;
hence  DigA ((DecSD (m,1,k)),1) = DigitDC (m,1,k) by Def9
.= (m mod ((Radix k) |^ 1)) div ((Radix k) |^ 0) by XREAL_1:232
.= (m mod ((Radix k) |^ 1)) div 1 by NEWTON:4
.= m mod ((Radix k) |^ 1) by NAT_2:4
.= m by A1, NAT_D:24 ;
::_thesis: verum
end;

theorem :: RADIX_1:22
for k, n being Nat st n >= 1 holds
for m being Nat st m is_represented_by n,k holds
m = SDDec (DecSD (m,n,k))
proof
let k, n be Nat; ::_thesis: ( n >= 1 implies for m being Nat st m is_represented_by n,k holds
m = SDDec (DecSD (m,n,k)) )
defpred S1[ Nat] means  for m being Nat st m is_represented_by $1,k holds
m = SDDec (DecSD (m,$1,k));
A1: for u being Nat st u >= 1 & S1[u] holds
S1[u + 1]
proof
let u be Nat; ::_thesis: ( u >= 1 & S1[u] implies S1[u + 1] )
assume that
 u >= 1 and
A2: S1[u] ; ::_thesis: S1[u + 1]
 for p being Nat st p is_represented_by u + 1,k holds
p = SDDec (DecSD (p,(u + 1),k))
proof
let p be Nat; ::_thesis: ( p is_represented_by u + 1,k implies p = SDDec (DecSD (p,(u + 1),k)) )
set I = u + 1;
set R = (Radix k) |^ u;
set M = p mod ((Radix k) |^ u);
set N = ((Radix k) |^ u) * (p div ((Radix k) |^ u));
A3: (u + 1) -' 1 = u by NAT_D:34;
A4: u + 1 <= len (DigitSD (DecSD (p,(u + 1),k))) by CARD_1:def_7;
A5: 1 <= u + 1 by NAT_1:12;
then A6: u + 1 in Seg (u + 1) by FINSEQ_1:1;
assume  p is_represented_by u + 1,k ; ::_thesis: p = SDDec (DecSD (p,(u + 1),k))
then  p < (Radix k) |^ (u + 1) by Def12;
then  p div ((Radix k) |^ u) = DigitDC (p,(u + 1),k) by A3, NAT_D:24;
then A7: ((Radix k) |^ u) * (p div ((Radix k) |^ u)) = SubDigit ((DecSD (p,(u + 1),k)),(u + 1),k) by A3, A6, Def9
.= (DigitSD (DecSD (p,(u + 1),k))) /. (u + 1) by A6, Def6
.= (DigitSD (DecSD (p,(u + 1),k))) . (u + 1) by A4, FINSEQ_4:15, NAT_1:12 ;
A8: (DigitSD (DecSD ((p mod ((Radix k) |^ u)),u,k))) ^ <*(((Radix k) |^ u) * (p div ((Radix k) |^ u)))*> = DigitSD (DecSD (p,(u + 1),k))
proof
 ((Radix k) |^ u) * (p div ((Radix k) |^ u)) is Element of INT by INT_1:def_2;
then reconsider z1 = <*(((Radix k) |^ u) * (p div ((Radix k) |^ u)))*> as FinSequence of INT by FINSEQ_1:74;
reconsider DD = DigitSD (DecSD (p,(u + 1),k)) as FinSequence of INT ;
set z0 = DigitSD (DecSD ((p mod ((Radix k) |^ u)),u,k));
reconsider z = (DigitSD (DecSD ((p mod ((Radix k) |^ u)),u,k))) ^ z1 as FinSequence of INT ;
A9: len z = (len (DigitSD (DecSD ((p mod ((Radix k) |^ u)),u,k)))) + (len <*(((Radix k) |^ u) * (p div ((Radix k) |^ u)))*>) by FINSEQ_1:22
.= u + (len <*(((Radix k) |^ u) * (p div ((Radix k) |^ u)))*>) by CARD_1:def_7
.= u + 1 by FINSEQ_1:39 ;
A10: for i being Nat st 1 <= i & i <= len z holds
z /. i = DD /. i
proof
let i be Nat; ::_thesis: ( 1 <= i & i <= len z implies z /. i = DD /. i )
assume  ( 1 <= i & i <= len z ) ; ::_thesis: z /. i = DD /. i
then A11: i in Seg (u + 1) by A9, FINSEQ_1:1;
percases ( i in Seg u or i = u + 1 ) by A11, FINSEQ_2:7;
supposeA12: i in Seg u ; ::_thesis: z /. i = DD /. i
A13: (p mod ((Radix k) |^ u)) mod ((Radix k) |^ i) = p mod ((Radix k) |^ i)
proof
 i <= u by A12, FINSEQ_1:1;
then  (Radix k) |^ i divides (Radix k) |^ u by NEWTON:89;
then consider t being Nat such that
A14: (Radix k) |^ u = ((Radix k) |^ i) * t by NAT_D:def_3;
 Radix k <> 0 by POWER:34;
then  t <> 0 by A14, PREPOWER:5;
hence  (p mod ((Radix k) |^ u)) mod ((Radix k) |^ i) = p mod ((Radix k) |^ i) by A14, Th3; ::_thesis: verum
end;
A15: i in dom ((DigitSD (DecSD ((p mod ((Radix k) |^ u)),u,k))) ^ z1) by A9, A11, FINSEQ_1:def_3;
 len DD = u + 1 by CARD_1:def_7;
then A16: i in dom DD by A11, FINSEQ_1:def_3;
then A17: DD . i = DD /. i by PARTFUN1:def_6;
A18: DD . i = (DigitSD (DecSD (p,(u + 1),k))) /. i by A16, PARTFUN1:def_6
.= SubDigit ((DecSD (p,(u + 1),k)),i,k) by A11, Def6
.= ((Radix k) |^ (i -' 1)) * (DigitDC (p,i,k)) by A11, Def9
.= ((Radix k) |^ (i -' 1)) * ((p mod ((Radix k) |^ i)) div ((Radix k) |^ (i -' 1))) ;
 len (DigitSD (DecSD ((p mod ((Radix k) |^ u)),u,k))) = u by CARD_1:def_7;
then A19: i in dom (DigitSD (DecSD ((p mod ((Radix k) |^ u)),u,k))) by A12, FINSEQ_1:def_3;
then ((DigitSD (DecSD ((p mod ((Radix k) |^ u)),u,k))) ^ z1) . i = (DigitSD (DecSD ((p mod ((Radix k) |^ u)),u,k))) . i by FINSEQ_1:def_7
.= (DigitSD (DecSD ((p mod ((Radix k) |^ u)),u,k))) /. i by A19, PARTFUN1:def_6
.= SubDigit ((DecSD ((p mod ((Radix k) |^ u)),u,k)),i,k) by A12, Def6
.= ((Radix k) |^ (i -' 1)) * (DigitDC ((p mod ((Radix k) |^ u)),i,k)) by A12, Def9
.= ((Radix k) |^ (i -' 1)) * ((p mod ((Radix k) |^ i)) div ((Radix k) |^ (i -' 1))) by A13 ;
hence  z /. i = DD /. i by A18, A17, A15, PARTFUN1:def_6; ::_thesis: verum
end;
supposeA20: i = u + 1 ; ::_thesis: z /. i = DD /. i
hence z /. i = z . (u + 1) by A5, A9, FINSEQ_4:15
.= ((DigitSD (DecSD ((p mod ((Radix k) |^ u)),u,k))) ^ z1) . ((len (DigitSD (DecSD ((p mod ((Radix k) |^ u)),u,k)))) + 1) by CARD_1:def_7
.= (DigitSD (DecSD (p,(u + 1),k))) . (u + 1) by A7, FINSEQ_1:42
.= DD /. i by A4, A20, FINSEQ_4:15, NAT_1:12 ;
::_thesis: verum
end;
end;
end;
 len DD = u + 1 by CARD_1:def_7;
hence  (DigitSD (DecSD ((p mod ((Radix k) |^ u)),u,k))) ^ <*(((Radix k) |^ u) * (p div ((Radix k) |^ u)))*> = DigitSD (DecSD (p,(u + 1),k)) by A9, A10, FINSEQ_5:13; ::_thesis: verum
end;
 Radix k <> 0 by POWER:34;
then A21: (Radix k) |^ u <> 0 by PREPOWER:5;
then  p mod ((Radix k) |^ u) < (Radix k) |^ u by NAT_D:1;
then A22: p mod ((Radix k) |^ u) is_represented_by u,k by Def12;
 p = (((Radix k) |^ u) * (p div ((Radix k) |^ u))) + (p mod ((Radix k) |^ u)) by A21, NAT_D:2;
then  p = (SDDec (DecSD ((p mod ((Radix k) |^ u)),u,k))) + (((Radix k) |^ u) * (p div ((Radix k) |^ u))) by A2, A22;
hence  p = SDDec (DecSD (p,(u + 1),k)) by A8, RVSUM_1:74; ::_thesis: verum
end;
hence  S1[u + 1] ; ::_thesis: verum
end;
A23: S1[1]
proof
let m be Nat; ::_thesis: ( m is_represented_by 1,k implies m = SDDec (DecSD (m,1,k)) )
assume A24: m is_represented_by 1,k ; ::_thesis: m = SDDec (DecSD (m,1,k))
reconsider i = m as Element of REAL by XREAL_0:def_1;
reconsider M = <*i*> as FinSequence of REAL ;
A25: 1 in Seg 1 by FINSEQ_1:1;
SubDigit ((DecSD (m,1,k)),1,k) = ((Radix k) |^ 0) * (DigB ((DecSD (m,1,k)),1)) by XREAL_1:232
.= 1 * (DigB ((DecSD (m,1,k)),1)) by NEWTON:4
.= m by A24, Th21 ;
then  (DigitSD (DecSD (m,1,k))) /. 1 = m by A25, Def6;
hence  SDDec (DecSD (m,1,k)) = Sum M by Th17
.= m by FINSOP_1:11 ;
::_thesis: verum
end;
 for u being Nat st u >= 1 holds
S1[u] from NAT_1:sch_8(A23, A1);
hence  ( n >= 1 implies for m being Nat st m is_represented_by n,k holds
m = SDDec (DecSD (m,n,k)) ) ; ::_thesis: verum
end;

theorem Th23: :: RADIX_1:23
for m, k, n being Nat st m is_represented_by 1,k & n is_represented_by 1,k holds
SD_Add_Carry ((DigA ((DecSD (m,1,k)),1)) + (DigA ((DecSD (n,1,k)),1))) = SD_Add_Carry (m + n)
proof
let m, k, n be Nat; ::_thesis: ( m is_represented_by 1,k & n is_represented_by 1,k implies SD_Add_Carry ((DigA ((DecSD (m,1,k)),1)) + (DigA ((DecSD (n,1,k)),1))) = SD_Add_Carry (m + n) )
assume that
A1: m is_represented_by 1,k and
A2: n is_represented_by 1,k ; ::_thesis: SD_Add_Carry ((DigA ((DecSD (m,1,k)),1)) + (DigA ((DecSD (n,1,k)),1))) = SD_Add_Carry (m + n)
SD_Add_Carry ((DigA ((DecSD (m,1,k)),1)) + (DigA ((DecSD (n,1,k)),1))) = SD_Add_Carry (m + (DigA ((DecSD (n,1,k)),1))) by A1, Th21
.= SD_Add_Carry (m + n) by A2, Th21 ;
hence  SD_Add_Carry ((DigA ((DecSD (m,1,k)),1)) + (DigA ((DecSD (n,1,k)),1))) = SD_Add_Carry (m + n) ; ::_thesis: verum
end;

Lm3:  for n, m, k, i being Nat st i in Seg n holds
DigA ((DecSD (m,(n + 1),k)),i) = DigA ((DecSD ((m mod ((Radix k) |^ n)),n,k)),i)
proof
let n, m, k, i be Nat; ::_thesis: ( i in Seg n implies DigA ((DecSD (m,(n + 1),k)),i) = DigA ((DecSD ((m mod ((Radix k) |^ n)),n,k)),i) )
assume A1: i in Seg n ; ::_thesis: DigA ((DecSD (m,(n + 1),k)),i) = DigA ((DecSD ((m mod ((Radix k) |^ n)),n,k)),i)
then A2: i <= n by FINSEQ_1:1;
then A3: i <= n + 1 by NAT_1:12;
 1 <= i by A1, FINSEQ_1:1;
then A4: i in Seg (n + 1) by A3, FINSEQ_1:1;
 (Radix k) |^ i divides (Radix k) |^ n by A2, NEWTON:89;
then consider t being Nat such that
A5: (Radix k) |^ n = ((Radix k) |^ i) * t by NAT_D:def_3;
 Radix k <> 0 by POWER:34;
then A6: t <> 0 by A5, PREPOWER:5;
DigA ((DecSD ((m mod ((Radix k) |^ n)),n,k)),i) = DigitDC ((m mod ((Radix k) |^ n)),i,k) by A1, Def9
.= DigitDC (m,i,k) by A5, A6, Th3
.= DigA ((DecSD (m,(n + 1),k)),i) by A4, Def9 ;
hence  DigA ((DecSD (m,(n + 1),k)),i) = DigA ((DecSD ((m mod ((Radix k) |^ n)),n,k)),i) ; ::_thesis: verum
end;

theorem Th24: :: RADIX_1:24
for m, n, k being Nat st m is_represented_by n + 1,k holds
DigA ((DecSD (m,(n + 1),k)),(n + 1)) = m div ((Radix k) |^ n)
proof
let m, n, k be Nat; ::_thesis: ( m is_represented_by n + 1,k implies DigA ((DecSD (m,(n + 1),k)),(n + 1)) = m div ((Radix k) |^ n) )
assume  m is_represented_by n + 1,k ; ::_thesis: DigA ((DecSD (m,(n + 1),k)),(n + 1)) = m div ((Radix k) |^ n)
then A1: m < (Radix k) |^ (n + 1) by Def12;
 n + 1 in Seg (n + 1) by FINSEQ_1:3;
then  DigA ((DecSD (m,(n + 1),k)),(n + 1)) = DigitDC (m,(n + 1),k) by Def9
.= m div ((Radix k) |^ ((n + 1) -' 1)) by A1, NAT_D:24
.= m div ((Radix k) |^ n) by NAT_D:34 ;
hence  DigA ((DecSD (m,(n + 1),k)),(n + 1)) = m div ((Radix k) |^ n) ; ::_thesis: verum
end;

begin

definition
let k, i, n be Nat;
let x, y be Tuple of n,k -SD ;
assume that
A1: i in Seg n and
A2: k >= 2 ;
func Add (x,y,i,k) ->  Element of k -SD  equals :Def13: :: RADIX_1:def 13
(SD_Add_Data (((DigA (x,i)) + (DigA (y,i))),k)) + (SD_Add_Carry ((DigA (x,(i -' 1))) + (DigA (y,(i -' 1)))));
coherence
 (SD_Add_Data (((DigA (x,i)) + (DigA (y,i))),k)) + (SD_Add_Carry ((DigA (x,(i -' 1))) + (DigA (y,(i -' 1))))) is Element of k -SD
proof
set SDC = SD_Add_Carry ((DigA (x,(i -' 1))) + (DigA (y,(i -' 1))));
set SDD = SD_Add_Data (((DigA (x,i)) + (DigA (y,i))),k);
A3: - 1 <= SD_Add_Carry ((DigA (x,(i -' 1))) + (DigA (y,(i -' 1)))) by Lm2;
A4: SD_Add_Carry ((DigA (x,(i -' 1))) + (DigA (y,(i -' 1)))) <= 1 by Lm2;
A5: ( DigA (x,i) is Element of k -SD & DigA (y,i) is Element of k -SD ) by A1, Th16;
then  SD_Add_Data (((DigA (x,i)) + (DigA (y,i))),k) <= (Radix k) - 2 by A2, Th20;
then A6: (SD_Add_Data (((DigA (x,i)) + (DigA (y,i))),k)) + (SD_Add_Carry ((DigA (x,(i -' 1))) + (DigA (y,(i -' 1))))) <= ((Radix k) - 2) + 1 by A4, XREAL_1:7;
 (- (Radix k)) + 2 <= SD_Add_Data (((DigA (x,i)) + (DigA (y,i))),k) by A2, A5, Th20;
then  ( (SD_Add_Data (((DigA (x,i)) + (DigA (y,i))),k)) + (SD_Add_Carry ((DigA (x,(i -' 1))) + (DigA (y,(i -' 1))))) is Element of INT & ((- (Radix k)) + 2) + (- 1) <= (SD_Add_Data (((DigA (x,i)) + (DigA (y,i))),k)) + (SD_Add_Carry ((DigA (x,(i -' 1))) + (DigA (y,(i -' 1))))) ) by A3, INT_1:def_2, XREAL_1:7;
then  (SD_Add_Data (((DigA (x,i)) + (DigA (y,i))),k)) + (SD_Add_Carry ((DigA (x,(i -' 1))) + (DigA (y,(i -' 1))))) in k -SD by A6;
hence  (SD_Add_Data (((DigA (x,i)) + (DigA (y,i))),k)) + (SD_Add_Carry ((DigA (x,(i -' 1))) + (DigA (y,(i -' 1))))) is Element of k -SD ; ::_thesis: verum
end;
end;

:: deftheorem Def13 defines Add RADIX_1:def_13_:_
 for k, i, n being Nat
for x, y being Tuple of n,k -SD st i in Seg n & k >= 2 holds
Add (x,y,i,k) = (SD_Add_Data (((DigA (x,i)) + (DigA (y,i))),k)) + (SD_Add_Carry ((DigA (x,(i -' 1))) + (DigA (y,(i -' 1)))));

definition
let n, k be Nat;
let x, y be Tuple of n,k -SD ;
funcx '+' y ->  Tuple of n,k -SD  means :Def14: :: RADIX_1:def 14
 for i being Nat st i in Seg n holds
DigA (it,i) = Add (x,y,i,k);
existence
 ex b1 being Tuple of n,k -SD st
for i being Nat st i in Seg n holds
DigA (b1,i) = Add (x,y,i,k)
proof
deffunc H1( Nat) ->  Element of k -SD = Add (x,y,$1,k);
consider z being FinSequence of k -SD  such that
A1: len z = n and
A2: for j being Nat st j in dom z holds
z . j = H1(j) from FINSEQ_2:sch_1();
A3: dom z = Seg n by A1, FINSEQ_1:def_3;
reconsider z = z as Tuple of n,k -SD by A1, CARD_1:def_7;
take  z ; ::_thesis: for i being Nat st i in Seg n holds
DigA (z,i) = Add (x,y,i,k)
let i be Nat; ::_thesis: ( i in Seg n implies DigA (z,i) = Add (x,y,i,k) )
assume A4: i in Seg n ; ::_thesis: DigA (z,i) = Add (x,y,i,k)
hence  DigA (z,i) = z . i by Def3
.= Add (x,y,i,k) by A2, A3, A4 ;
::_thesis: verum
end;
uniqueness
 for b1, b2 being Tuple of n,k -SD st ( for i being Nat st i in Seg n holds
DigA (b1,i) = Add (x,y,i,k) ) & ( for i being Nat st i in Seg n holds
DigA (b2,i) = Add (x,y,i,k) ) holds
b1 = b2
proof
let k1, k2 be Tuple of n,k -SD ; ::_thesis: ( ( for i being Nat st i in Seg n holds
DigA (k1,i) = Add (x,y,i,k) ) & ( for i being Nat st i in Seg n holds
DigA (k2,i) = Add (x,y,i,k) ) implies k1 = k2 )
assume that
A5: for i being Nat st i in Seg n holds
DigA (k1,i) = Add (x,y,i,k) and
A6: for i being Nat st i in Seg n holds
DigA (k2,i) = Add (x,y,i,k) ; ::_thesis: k1 = k2
A7: len k1 = n by CARD_1:def_7;
then A8: dom k1 = Seg n by FINSEQ_1:def_3;
A9: now__::_thesis:_for_j_being_Nat_st_j_in_dom_k1_holds_
k1_._j_=_k2_._j
let j be Nat; ::_thesis: ( j in dom k1 implies k1 . j = k2 . j )
assume A10: j in dom k1 ; ::_thesis: k1 . j = k2 . j
then k1 . j = DigA (k1,j) by A8, Def3
.= Add (x,y,j,k) by A5, A8, A10
.= DigA (k2,j) by A6, A8, A10
.= k2 . j by A8, A10, Def3 ;
hence  k1 . j = k2 . j ; ::_thesis: verum
end;
 len k2 = n by CARD_1:def_7;
hence  k1 = k2 by A7, A9, FINSEQ_2:9; ::_thesis: verum
end;
end;

:: deftheorem Def14 defines '+' RADIX_1:def_14_:_
 for n, k being Nat
for x, y, b5 being Tuple of n,k -SD holds
( b5 = x '+' y iff for i being Nat st i in Seg n holds
DigA (b5,i) = Add (x,y,i,k) );

theorem Th25: :: RADIX_1:25
for k, m, n being Nat st k >= 2 & m is_represented_by 1,k & n is_represented_by 1,k holds
SDDec ((DecSD (m,1,k)) '+' (DecSD (n,1,k))) = SD_Add_Data ((m + n),k)
proof
let k, m, n be Nat; ::_thesis: ( k >= 2 & m is_represented_by 1,k & n is_represented_by 1,k implies SDDec ((DecSD (m,1,k)) '+' (DecSD (n,1,k))) = SD_Add_Data ((m + n),k) )
assume that
A1: k >= 2 and
A2: m is_represented_by 1,k and
A3: n is_represented_by 1,k ; ::_thesis: SDDec ((DecSD (m,1,k)) '+' (DecSD (n,1,k))) = SD_Add_Data ((m + n),k)
set N = DecSD (n,1,k);
set M = DecSD (m,1,k);
A4: 1 in Seg 1 by FINSEQ_1:1;
then A5: DigA (((DecSD (m,1,k)) '+' (DecSD (n,1,k))),1) = Add ((DecSD (m,1,k)),(DecSD (n,1,k)),1,k) by Def14
.= (SD_Add_Data (((DigA ((DecSD (m,1,k)),1)) + (DigA ((DecSD (n,1,k)),1))),k)) + (SD_Add_Carry ((DigA ((DecSD (m,1,k)),(1 -' 1))) + (DigA ((DecSD (n,1,k)),(1 -' 1))))) by A1, A4, Def13
.= (SD_Add_Data (((DigA ((DecSD (m,1,k)),1)) + (DigA ((DecSD (n,1,k)),1))),k)) + (SD_Add_Carry ((DigA ((DecSD (m,1,k)),0)) + (DigA ((DecSD (n,1,k)),(1 -' 1))))) by XREAL_1:232
.= (SD_Add_Data (((DigA ((DecSD (m,1,k)),1)) + (DigA ((DecSD (n,1,k)),1))),k)) + (SD_Add_Carry ((DigA ((DecSD (m,1,k)),0)) + (DigA ((DecSD (n,1,k)),0)))) by XREAL_1:232
.= (SD_Add_Data (((DigA ((DecSD (m,1,k)),1)) + (DigA ((DecSD (n,1,k)),1))),k)) + (SD_Add_Carry (0 + (DigA ((DecSD (n,1,k)),0)))) by Def3
.= (SD_Add_Data (((DigA ((DecSD (m,1,k)),1)) + (DigA ((DecSD (n,1,k)),1))),k)) + 0 by Def3, Th18
.= SD_Add_Data ((m + (DigA ((DecSD (n,1,k)),1))),k) by A2, Th21
.= SD_Add_Data ((m + n),k) by A3, Th21 ;
A6: (DigitSD ((DecSD (m,1,k)) '+' (DecSD (n,1,k)))) /. 1 = SubDigit (((DecSD (m,1,k)) '+' (DecSD (n,1,k))),1,k) by A4, Def6
.= ((Radix k) |^ 0) * (DigA (((DecSD (m,1,k)) '+' (DecSD (n,1,k))),1)) by XREAL_1:232
.= 1 * (DigA (((DecSD (m,1,k)) '+' (DecSD (n,1,k))),1)) by NEWTON:4
.= SD_Add_Data ((m + n),k) by A5 ;
reconsider w = SD_Add_Data ((m + n),k) as Element of INT by INT_1:def_2;
A7: len (DigitSD ((DecSD (m,1,k)) '+' (DecSD (n,1,k)))) = 1 by CARD_1:def_7;
 1 in Seg 1 by FINSEQ_1:1;
then  1 in dom (DigitSD ((DecSD (m,1,k)) '+' (DecSD (n,1,k)))) by A7, FINSEQ_1:def_3;
then  (DigitSD ((DecSD (m,1,k)) '+' (DecSD (n,1,k)))) . 1 = SD_Add_Data ((m + n),k) by A6, PARTFUN1:def_6;
then  SDDec ((DecSD (m,1,k)) '+' (DecSD (n,1,k))) = Sum <*w*> by A7, FINSEQ_1:40
.= SD_Add_Data ((m + n),k) by RVSUM_1:73 ;
hence  SDDec ((DecSD (m,1,k)) '+' (DecSD (n,1,k))) = SD_Add_Data ((m + n),k) ; ::_thesis: verum
end;

theorem :: RADIX_1:26
for n being Nat st n >= 1 holds
for k, x, y being Nat st k >= 2 & x is_represented_by n,k & y is_represented_by n,k holds
x + y = (SDDec ((DecSD (x,n,k)) '+' (DecSD (y,n,k)))) + (((Radix k) |^ n) * (SD_Add_Carry ((DigA ((DecSD (x,n,k)),n)) + (DigA ((DecSD (y,n,k)),n)))))
proof
defpred S1[ Nat] means  for k, x, y being Nat st k >= 2 & x is_represented_by $1,k & y is_represented_by $1,k holds
x + y = (SDDec ((DecSD (x,$1,k)) '+' (DecSD (y,$1,k)))) + (((Radix k) |^ $1) * (SD_Add_Carry ((DigA ((DecSD (x,$1,k)),$1)) + (DigA ((DecSD (y,$1,k)),$1)))));
let n be Nat; ::_thesis: ( n >= 1 implies for k, x, y being Nat st k >= 2 & x is_represented_by n,k & y is_represented_by n,k holds
x + y = (SDDec ((DecSD (x,n,k)) '+' (DecSD (y,n,k)))) + (((Radix k) |^ n) * (SD_Add_Carry ((DigA ((DecSD (x,n,k)),n)) + (DigA ((DecSD (y,n,k)),n))))) )
assume A1: n >= 1 ; ::_thesis: for k, x, y being Nat st k >= 2 & x is_represented_by n,k & y is_represented_by n,k holds
x + y = (SDDec ((DecSD (x,n,k)) '+' (DecSD (y,n,k)))) + (((Radix k) |^ n) * (SD_Add_Carry ((DigA ((DecSD (x,n,k)),n)) + (DigA ((DecSD (y,n,k)),n)))))
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 A3, FINSEQ_1:3;
let k, x, y be Nat; ::_thesis: ( k >= 2 & x is_represented_by n + 1,k & y is_represented_by n + 1,k implies x + y = (SDDec ((DecSD (x,(n + 1),k)) '+' (DecSD (y,(n + 1),k)))) + (((Radix k) |^ (n + 1)) * (SD_Add_Carry ((DigA ((DecSD (x,(n + 1),k)),(n + 1))) + (DigA ((DecSD (y,(n + 1),k)),(n + 1)))))) )
A6: n + 1 in Seg (n + 1) by FINSEQ_1:3;
set z = (DecSD (x,(n + 1),k)) '+' (DecSD (y,(n + 1),k));
set yn = y mod ((Radix k) |^ n);
set xn = x mod ((Radix k) |^ n);
assume that
A7: k >= 2 and
A8: x is_represented_by n + 1,k and
A9: y is_represented_by n + 1,k ; ::_thesis: x + y = (SDDec ((DecSD (x,(n + 1),k)) '+' (DecSD (y,(n + 1),k)))) + (((Radix k) |^ (n + 1)) * (SD_Add_Carry ((DigA ((DecSD (x,(n + 1),k)),(n + 1))) + (DigA ((DecSD (y,(n + 1),k)),(n + 1))))))
set zn = (DecSD ((x mod ((Radix k) |^ n)),n,k)) '+' (DecSD ((y mod ((Radix k) |^ n)),n,k));
A10: len (DigitSD ((DecSD ((x mod ((Radix k) |^ n)),n,k)) '+' (DecSD ((y mod ((Radix k) |^ n)),n,k)))) = n by CARD_1:def_7;
A11: len (DigitSD ((DecSD (x,(n + 1),k)) '+' (DecSD (y,(n + 1),k)))) = n + 1 by CARD_1:def_7;
A12: for i being Nat st 1 <= i & i <= len (DigitSD ((DecSD (x,(n + 1),k)) '+' (DecSD (y,(n + 1),k)))) holds
(DigitSD ((DecSD (x,(n + 1),k)) '+' (DecSD (y,(n + 1),k)))) . i = ((DigitSD ((DecSD ((x mod ((Radix k) |^ n)),n,k)) '+' (DecSD ((y mod ((Radix k) |^ n)),n,k)))) ^ <*(SubDigit (((DecSD (x,(n + 1),k)) '+' (DecSD (y,(n + 1),k))),(n + 1),k))*>) . i
proof
let i be Nat; ::_thesis: ( 1 <= i & i <= len (DigitSD ((DecSD (x,(n + 1),k)) '+' (DecSD (y,(n + 1),k)))) implies (DigitSD ((DecSD (x,(n + 1),k)) '+' (DecSD (y,(n + 1),k)))) . i = ((DigitSD ((DecSD ((x mod ((Radix k) |^ n)),n,k)) '+' (DecSD ((y mod ((Radix k) |^ n)),n,k)))) ^ <*(SubDigit (((DecSD (x,(n + 1),k)) '+' (DecSD (y,(n + 1),k))),(n + 1),k))*>) . i )
assume that
A13: 1 <= i and
A14: i <= len (DigitSD ((DecSD (x,(n + 1),k)) '+' (DecSD (y,(n + 1),k)))) ; ::_thesis: (DigitSD ((DecSD (x,(n + 1),k)) '+' (DecSD (y,(n + 1),k)))) . i = ((DigitSD ((DecSD ((x mod ((Radix k) |^ n)),n,k)) '+' (DecSD ((y mod ((Radix k) |^ n)),n,k)))) ^ <*(SubDigit (((DecSD (x,(n + 1),k)) '+' (DecSD (y,(n + 1),k))),(n + 1),k))*>) . i
A15: i -' 1 = i - 1 by A13, XREAL_1:233;
A16: i <= n + 1 by A14, CARD_1:def_7;
then A17: i in Seg (n + 1) by A13, FINSEQ_1:1;
then A18: i in dom (DigitSD ((DecSD (x,(n + 1),k)) '+' (DecSD (y,(n + 1),k)))) by A11, FINSEQ_1:def_3;
percases ( i in Seg n or i = n + 1 ) by A17, FINSEQ_2:7;
supposeA19: i in Seg n ; ::_thesis: (DigitSD ((DecSD (x,(n + 1),k)) '+' (DecSD (y,(n + 1),k)))) . i = ((DigitSD ((DecSD ((x mod ((Radix k) |^ n)),n,k)) '+' (DecSD ((y mod ((Radix k) |^ n)),n,k)))) ^ <*(SubDigit (((DecSD (x,(n + 1),k)) '+' (DecSD (y,(n + 1),k))),(n + 1),k))*>) . i
then A20: i in dom (DigitSD ((DecSD ((x mod ((Radix k) |^ n)),n,k)) '+' (DecSD ((y mod ((Radix k) |^ n)),n,k)))) by A10, FINSEQ_1:def_3;
then A21: ((DigitSD ((DecSD ((x mod ((Radix k) |^ n)),n,k)) '+' (DecSD ((y mod ((Radix k) |^ n)),n,k)))) ^ <*(SubDigit (((DecSD (x,(n + 1),k)) '+' (DecSD (y,(n + 1),k))),(n + 1),k))*>) . i = (DigitSD ((DecSD ((x mod ((Radix k) |^ n)),n,k)) '+' (DecSD ((y mod ((Radix k) |^ n)),n,k)))) . i by FINSEQ_1:def_7
.= (DigitSD ((DecSD ((x mod ((Radix k) |^ n)),n,k)) '+' (DecSD ((y mod ((Radix k) |^ n)),n,k)))) /. i by A20, PARTFUN1:def_6
.= SubDigit (((DecSD ((x mod ((Radix k) |^ n)),n,k)) '+' (DecSD ((y mod ((Radix k) |^ n)),n,k))),i,k) by A19, Def6
.= ((Radix k) |^ (i -' 1)) * (Add ((DecSD ((x mod ((Radix k) |^ n)),n,k)),(DecSD ((y mod ((Radix k) |^ n)),n,k)),i,k)) by A19, Def14
.= ((Radix k) |^ (i -' 1)) * ((SD_Add_Data (((DigA ((DecSD ((x mod ((Radix k) |^ n)),n,k)),i)) + (DigA ((DecSD ((y mod ((Radix k) |^ n)),n,k)),i))),k)) + (SD_Add_Carry ((DigA ((DecSD ((x mod ((Radix k) |^ n)),n,k)),(i -' 1))) + (DigA ((DecSD ((y mod ((Radix k) |^ n)),n,k)),(i -' 1)))))) by A7, A19, Def13 ;
A22: (DigitSD ((DecSD (x,(n + 1),k)) '+' (DecSD (y,(n + 1),k)))) . i = (DigitSD ((DecSD (x,(n + 1),k)) '+' (DecSD (y,(n + 1),k)))) /. i by A18, PARTFUN1:def_6
.= SubDigit (((DecSD (x,(n + 1),k)) '+' (DecSD (y,(n + 1),k))),i,k) by A17, Def6
.= ((Radix k) |^ (i -' 1)) * (Add ((DecSD (x,(n + 1),k)),(DecSD (y,(n + 1),k)),i,k)) by A17, Def14
.= ((Radix k) |^ (i -' 1)) * ((SD_Add_Data (((DigA ((DecSD (x,(n + 1),k)),i)) + (DigA ((DecSD (y,(n + 1),k)),i))),k)) + (SD_Add_Carry ((DigA ((DecSD (x,(n + 1),k)),(i -' 1))) + (DigA ((DecSD (y,(n + 1),k)),(i -' 1)))))) by A7, A17, Def13 ;
now__::_thesis:_(DigitSD_((DecSD_(x,(n_+_1),k))_'+'_(DecSD_(y,(n_+_1),k))))_._i_=_((DigitSD_((DecSD_((x_mod_((Radix_k)_|^_n)),n,k))_'+'_(DecSD_((y_mod_((Radix_k)_|^_n)),n,k))))_^_<*(SubDigit_(((DecSD_(x,(n_+_1),k))_'+'_(DecSD_(y,(n_+_1),k))),(n_+_1),k))*>)_._i
percases ( i = 1 or i > 1 ) by A13, XXREAL_0:1;
supposeA23: i = 1 ; ::_thesis: (DigitSD ((DecSD (x,(n + 1),k)) '+' (DecSD (y,(n + 1),k)))) . i = ((DigitSD ((DecSD ((x mod ((Radix k) |^ n)),n,k)) '+' (DecSD ((y mod ((Radix k) |^ n)),n,k)))) ^ <*(SubDigit (((DecSD (x,(n + 1),k)) '+' (DecSD (y,(n + 1),k))),(n + 1),k))*>) . i
then A24: ((DigitSD ((DecSD ((x mod ((Radix k) |^ n)),n,k)) '+' (DecSD ((y mod ((Radix k) |^ n)),n,k)))) ^ <*(SubDigit (((DecSD (x,(n + 1),k)) '+' (DecSD (y,(n + 1),k))),(n + 1),k))*>) . i = ((Radix k) |^ (i -' 1)) * ((SD_Add_Data (((DigA ((DecSD ((x mod ((Radix k) |^ n)),n,k)),i)) + (DigA ((DecSD ((y mod ((Radix k) |^ n)),n,k)),i))),k)) + (SD_Add_Carry ((DigA ((DecSD ((x mod ((Radix k) |^ n)),n,k)),(i -' 1))) + (DigA ((DecSD ((y mod ((Radix k) |^ n)),n,k)),0))))) by A21, XREAL_1:232
.= ((Radix k) |^ (i -' 1)) * ((SD_Add_Data (((DigA ((DecSD ((x mod ((Radix k) |^ n)),n,k)),i)) + (DigA ((DecSD ((y mod ((Radix k) |^ n)),n,k)),i))),k)) + (SD_Add_Carry ((DigA ((DecSD ((x mod ((Radix k) |^ n)),n,k)),0)) + (DigA ((DecSD ((y mod ((Radix k) |^ n)),n,k)),0))))) by A23, XREAL_1:232
.= ((Radix k) |^ (i -' 1)) * ((SD_Add_Data (((DigA ((DecSD ((x mod ((Radix k) |^ n)),n,k)),i)) + (DigA ((DecSD ((y mod ((Radix k) |^ n)),n,k)),i))),k)) + (SD_Add_Carry ((DigA ((DecSD ((x mod ((Radix k) |^ n)),n,k)),0)) + 0))) by Def3
.= ((Radix k) |^ (i -' 1)) * ((SD_Add_Data (((DigA ((DecSD ((x mod ((Radix k) |^ n)),n,k)),i)) + (DigA ((DecSD ((y mod ((Radix k) |^ n)),n,k)),i))),k)) + 0) by Def3, Th18 ;
(DigitSD ((DecSD (x,(n + 1),k)) '+' (DecSD (y,(n + 1),k)))) . i = ((Radix k) |^ (i -' 1)) * ((SD_Add_Data (((DigA ((DecSD (x,(n + 1),k)),i)) + (DigA ((DecSD (y,(n + 1),k)),i))),k)) + (SD_Add_Carry ((DigA ((DecSD (x,(n + 1),k)),(i -' 1))) + (DigA ((DecSD (y,(n + 1),k)),0))))) by A22, A23, XREAL_1:232
.= ((Radix k) |^ (i -' 1)) * ((SD_Add_Data (((DigA ((DecSD (x,(n + 1),k)),i)) + (DigA ((DecSD (y,(n + 1),k)),i))),k)) + (SD_Add_Carry ((DigA ((DecSD (x,(n + 1),k)),0)) + (DigA ((DecSD (y,(n + 1),k)),0))))) by A23, XREAL_1:232
.= ((Radix k) |^ (i -' 1)) * ((SD_Add_Data (((DigA ((DecSD (x,(n + 1),k)),i)) + (DigA ((DecSD (y,(n + 1),k)),i))),k)) + (SD_Add_Carry ((DigA ((DecSD (x,(n + 1),k)),0)) + 0))) by Def3
.= ((Radix k) |^ (i -' 1)) * ((SD_Add_Data (((DigA ((DecSD (x,(n + 1),k)),i)) + (DigA ((DecSD (y,(n + 1),k)),i))),k)) + 0) by Def3, Th18
.= ((Radix k) |^ (i -' 1)) * (SD_Add_Data (((DigA ((DecSD ((x mod ((Radix k) |^ n)),n,k)),i)) + (DigA ((DecSD (y,(n + 1),k)),i))),k)) by A19, Lm3
.= ((Radix k) |^ (i -' 1)) * (SD_Add_Data (((DigA ((DecSD ((x mod ((Radix k) |^ n)),n,k)),i)) + (DigA ((DecSD ((y mod ((Radix k) |^ n)),n,k)),i))),k)) by A19, Lm3 ;
hence  (DigitSD ((DecSD (x,(n + 1),k)) '+' (DecSD (y,(n + 1),k)))) . i = ((DigitSD ((DecSD ((x mod ((Radix k) |^ n)),n,k)) '+' (DecSD ((y mod ((Radix k) |^ n)),n,k)))) ^ <*(SubDigit (((DecSD (x,(n + 1),k)) '+' (DecSD (y,(n + 1),k))),(n + 1),k))*>) . i by A24; ::_thesis: verum
end;
supposeA25: i > 1 ; ::_thesis: (DigitSD ((DecSD (x,(n + 1),k)) '+' (DecSD (y,(n + 1),k)))) . i = ((DigitSD ((DecSD ((x mod ((Radix k) |^ n)),n,k)) '+' (DecSD ((y mod ((Radix k) |^ n)),n,k)))) ^ <*(SubDigit (((DecSD (x,(n + 1),k)) '+' (DecSD (y,(n + 1),k))),(n + 1),k))*>) . i
A26: i - 1 <= n by A16, XREAL_1:20;
 i -' 1 >= 1 by A25, NAT_D:49;
then A27: i -' 1 in Seg n by A15, A26, FINSEQ_1:1;
(DigitSD ((DecSD (x,(n + 1),k)) '+' (DecSD (y,(n + 1),k)))) . i = ((Radix k) |^ (i -' 1)) * ((SD_Add_Data (((DigA ((DecSD ((x mod ((Radix k) |^ n)),n,k)),i)) + (DigA ((DecSD (y,(n + 1),k)),i))),k)) + (SD_Add_Carry ((DigA ((DecSD (x,(n + 1),k)),(i -' 1))) + (DigA ((DecSD (y,(n + 1),k)),(i -' 1)))))) by A19, A22, Lm3
.= ((Radix k) |^ (i -' 1)) * ((SD_Add_Data (((DigA ((DecSD ((x mod ((Radix k) |^ n)),n,k)),i)) + (DigA ((DecSD ((y mod ((Radix k) |^ n)),n,k)),i))),k)) + (SD_Add_Carry ((DigA ((DecSD (x,(n + 1),k)),(i -' 1))) + (DigA ((DecSD (y,(n + 1),k)),(i -' 1)))))) by A19, Lm3
.= ((Radix k) |^ (i -' 1)) * ((SD_Add_Data (((DigA ((DecSD ((x mod ((Radix k) |^ n)),n,k)),i)) + (DigA ((DecSD ((y mod ((Radix k) |^ n)),n,k)),i))),k)) + (SD_Add_Carry ((DigA ((DecSD ((x mod ((Radix k) |^ n)),n,k)),(i -' 1))) + (DigA ((DecSD (y,(n + 1),k)),(i -' 1)))))) by A27, Lm3
.= ((Radix k) |^ (i -' 1)) * ((SD_Add_Data (((DigA ((DecSD ((x mod ((Radix k) |^ n)),n,k)),i)) + (DigA ((DecSD ((y mod ((Radix k) |^ n)),n,k)),i))),k)) + (SD_Add_Carry ((DigA ((DecSD ((x mod ((Radix k) |^ n)),n,k)),(i -' 1))) + (DigA ((DecSD ((y mod ((Radix k) |^ n)),n,k)),(i -' 1)))))) by A27, Lm3 ;
hence  (DigitSD ((DecSD (x,(n + 1),k)) '+' (DecSD (y,(n + 1),k)))) . i = ((DigitSD ((DecSD ((x mod ((Radix k) |^ n)),n,k)) '+' (DecSD ((y mod ((Radix k) |^ n)),n,k)))) ^ <*(SubDigit (((DecSD (x,(n + 1),k)) '+' (DecSD (y,(n + 1),k))),(n + 1),k))*>) . i by A21; ::_thesis: verum
end;
end;
end;
hence  (DigitSD ((DecSD (x,(n + 1),k)) '+' (DecSD (y,(n + 1),k)))) . i = ((DigitSD ((DecSD ((x mod ((Radix k) |^ n)),n,k)) '+' (DecSD ((y mod ((Radix k) |^ n)),n,k)))) ^ <*(SubDigit (((DecSD (x,(n + 1),k)) '+' (DecSD (y,(n + 1),k))),(n + 1),k))*>) . i ; ::_thesis: verum
end;
supposeA28: i = n + 1 ; ::_thesis: (DigitSD ((DecSD (x,(n + 1),k)) '+' (DecSD (y,(n + 1),k)))) . i = ((DigitSD ((DecSD ((x mod ((Radix k) |^ n)),n,k)) '+' (DecSD ((y mod ((Radix k) |^ n)),n,k)))) ^ <*(SubDigit (((DecSD (x,(n + 1),k)) '+' (DecSD (y,(n + 1),k))),(n + 1),k))*>) . i
then ((DigitSD ((DecSD ((x mod ((Radix k) |^ n)),n,k)) '+' (DecSD ((y mod ((Radix k) |^ n)),n,k)))) ^ <*(SubDigit (((DecSD (x,(n + 1),k)) '+' (DecSD (y,(n + 1),k))),(n + 1),k))*>) . i = ((DigitSD ((DecSD ((x mod ((Radix k) |^ n)),n,k)) '+' (DecSD ((y mod ((Radix k) |^ n)),n,k)))) ^ <*(SubDigit (((DecSD (x,(n + 1),k)) '+' (DecSD (y,(n + 1),k))),(n + 1),k))*>) . ((len (DigitSD ((DecSD ((x mod ((Radix k) |^ n)),n,k)) '+' (DecSD ((y mod ((Radix k) |^ n)),n,k))))) + 1) by CARD_1:def_7
.= SubDigit (((DecSD (x,(n + 1),k)) '+' (DecSD (y,(n + 1),k))),(n + 1),k) by FINSEQ_1:42
.= (DigitSD ((DecSD (x,(n + 1),k)) '+' (DecSD (y,(n + 1),k)))) /. (n + 1) by A6, Def6
.= (DigitSD ((DecSD (x,(n + 1),k)) '+' (DecSD (y,(n + 1),k)))) . (n + 1) by A18, A28, PARTFUN1:def_6 ;
hence  (DigitSD ((DecSD (x,(n + 1),k)) '+' (DecSD (y,(n + 1),k)))) . i = ((DigitSD ((DecSD ((x mod ((Radix k) |^ n)),n,k)) '+' (DecSD ((y mod ((Radix k) |^ n)),n,k)))) ^ <*(SubDigit (((DecSD (x,(n + 1),k)) '+' (DecSD (y,(n + 1),k))),(n + 1),k))*>) . i by A28; ::_thesis: verum
end;
end;
end;
A29: SubDigit (((DecSD (x,(n + 1),k)) '+' (DecSD (y,(n + 1),k))),(n + 1),k) = ((Radix k) |^ n) * (DigB (((DecSD (x,(n + 1),k)) '+' (DecSD (y,(n + 1),k))),(n + 1))) by NAT_D:34;
A30: Radix k > 0 by POWER:34;
then A31: x = ((x div ((Radix k) |^ n)) * ((Radix k) |^ n)) + (x mod ((Radix k) |^ n)) by NAT_D:2, PREPOWER:6;
set y1 = y div ((Radix k) |^ n);
set x1 = x div ((Radix k) |^ n);
A32: len <*(SubDigit (((DecSD (x,(n + 1),k)) '+' (DecSD (y,(n + 1),k))),(n + 1),k))*> = 1 by FINSEQ_1:39;
A33: DigA ((DecSD (y,(n + 1),k)),(n + 1)) = y div ((Radix k) |^ n) by A9, Th24;
 y mod ((Radix k) |^ n) < (Radix k) |^ n by A30, NAT_D:1, PREPOWER:6;
then A34: y mod ((Radix k) |^ n) is_represented_by n,k by Def12;
 x mod ((Radix k) |^ n) < (Radix k) |^ n by A30, NAT_D:1, PREPOWER:6;
then A35: x mod ((Radix k) |^ n) is_represented_by n,k by Def12;
len ((DigitSD ((DecSD ((x mod ((Radix k) |^ n)),n,k)) '+' (DecSD ((y mod ((Radix k) |^ n)),n,k)))) ^ <*(SubDigit (((DecSD (x,(n + 1),k)) '+' (DecSD (y,(n + 1),k))),(n + 1),k))*>) = (len (DigitSD ((DecSD ((x mod ((Radix k) |^ n)),n,k)) '+' (DecSD ((y mod ((Radix k) |^ n)),n,k))))) + (len <*(SubDigit (((DecSD (x,(n + 1),k)) '+' (DecSD (y,(n + 1),k))),(n + 1),k))*>) by FINSEQ_1:22
.= n + 1 by A32, CARD_1:def_7 ;
then  len (DigitSD ((DecSD (x,(n + 1),k)) '+' (DecSD (y,(n + 1),k)))) = len ((DigitSD ((DecSD ((x mod ((Radix k) |^ n)),n,k)) '+' (DecSD ((y mod ((Radix k) |^ n)),n,k)))) ^ <*(SubDigit (((DecSD (x,(n + 1),k)) '+' (DecSD (y,(n + 1),k))),(n + 1),k))*>) by CARD_1:def_7;
then  DigitSD ((DecSD (x,(n + 1),k)) '+' (DecSD (y,(n + 1),k))) = (DigitSD ((DecSD ((x mod ((Radix k) |^ n)),n,k)) '+' (DecSD ((y mod ((Radix k) |^ n)),n,k)))) ^ <*(SubDigit (((DecSD (x,(n + 1),k)) '+' (DecSD (y,(n + 1),k))),(n + 1),k))*> by A12, FINSEQ_1:14;
then  SDDec ((DecSD (x,(n + 1),k)) '+' (DecSD (y,(n + 1),k))) = (((Radix k) |^ n) * (DigB (((DecSD (x,(n + 1),k)) '+' (DecSD (y,(n + 1),k))),(n + 1)))) + (Sum (DigitSD ((DecSD ((x mod ((Radix k) |^ n)),n,k)) '+' (DecSD ((y mod ((Radix k) |^ n)),n,k))))) by A29, RVSUM_1:74
.= ((Add ((DecSD (x,(n + 1),k)),(DecSD (y,(n + 1),k)),(n + 1),k)) * ((Radix k) |^ n)) + (Sum (DigitSD ((DecSD ((x mod ((Radix k) |^ n)),n,k)) '+' (DecSD ((y mod ((Radix k) |^ n)),n,k))))) by A6, Def14
.= (((SD_Add_Data (((DigA ((DecSD (x,(n + 1),k)),(n + 1))) + (DigA ((DecSD (y,(n + 1),k)),(n + 1)))),k)) + (SD_Add_Carry ((DigA ((DecSD (x,(n + 1),k)),((n + 1) -' 1))) + (DigA ((DecSD (y,(n + 1),k)),((n + 1) -' 1)))))) * ((Radix k) |^ n)) + (Sum (DigitSD ((DecSD ((x mod ((Radix k) |^ n)),n,k)) '+' (DecSD ((y mod ((Radix k) |^ n)),n,k))))) by A6, A7, Def13
.= (((SD_Add_Data (((DigA ((DecSD (x,(n + 1),k)),(n + 1))) + (DigA ((DecSD (y,(n + 1),k)),(n + 1)))),k)) + (SD_Add_Carry ((DigA ((DecSD (x,(n + 1),k)),((n + 1) -' 1))) + (DigA ((DecSD (y,(n + 1),k)),n))))) * ((Radix k) |^ n)) + (Sum (DigitSD ((DecSD ((x mod ((Radix k) |^ n)),n,k)) '+' (DecSD ((y mod ((Radix k) |^ n)),n,k))))) by NAT_D:34
.= (((SD_Add_Data (((DigA ((DecSD (x,(n + 1),k)),(n + 1))) + (DigA ((DecSD (y,(n + 1),k)),(n + 1)))),k)) + (SD_Add_Carry ((DigA ((DecSD (x,(n + 1),k)),n)) + (DigA ((DecSD (y,(n + 1),k)),n))))) * ((Radix k) |^ n)) + (Sum (DigitSD ((DecSD ((x mod ((Radix k) |^ n)),n,k)) '+' (DecSD ((y mod ((Radix k) |^ n)),n,k))))) by NAT_D:34
.= (((SD_Add_Data (((DigA ((DecSD (x,(n + 1),k)),(n + 1))) + (DigA ((DecSD (y,(n + 1),k)),(n + 1)))),k)) + (SD_Add_Carry ((DigA ((DecSD ((x mod ((Radix k) |^ n)),n,k)),n)) + (DigA ((DecSD (y,(n + 1),k)),n))))) * ((Radix k) |^ n)) + (Sum (DigitSD ((DecSD ((x mod ((Radix k) |^ n)),n,k)) '+' (DecSD ((y mod ((Radix k) |^ n)),n,k))))) by A5, Lm3
.= (((SD_Add_Data (((DigA ((DecSD (x,(n + 1),k)),(n + 1))) + (DigA ((DecSD (y,(n + 1),k)),(n + 1)))),k)) + (SD_Add_Carry ((DigA ((DecSD ((x mod ((Radix k) |^ n)),n,k)),n)) + (DigA ((DecSD ((y mod ((Radix k) |^ n)),n,k)),n))))) * ((Radix k) |^ n)) + (Sum (DigitSD ((DecSD ((x mod ((Radix k) |^ n)),n,k)) '+' (DecSD ((y mod ((Radix k) |^ n)),n,k))))) by A5, Lm3
.= (((SD_Add_Data (((x div ((Radix k) |^ n)) + (y div ((Radix k) |^ n))),k)) + (SD_Add_Carry ((DigA ((DecSD ((x mod ((Radix k) |^ n)),n,k)),n)) + (DigA ((DecSD ((y mod ((Radix k) |^ n)),n,k)),n))))) * ((Radix k) |^ n)) + (Sum (DigitSD ((DecSD ((x mod ((Radix k) |^ n)),n,k)) '+' (DecSD ((y mod ((Radix k) |^ n)),n,k))))) by A8, A33, Th24
.= ((SD_Add_Data (((x div ((Radix k) |^ n)) + (y div ((Radix k) |^ n))),k)) * ((Radix k) |^ n)) + (((SD_Add_Carry ((DigA ((DecSD ((x mod ((Radix k) |^ n)),n,k)),n)) + (DigA ((DecSD ((y mod ((Radix k) |^ n)),n,k)),n)))) * ((Radix k) |^ n)) + (SDDec ((DecSD ((x mod ((Radix k) |^ n)),n,k)) '+' (DecSD ((y mod ((Radix k) |^ n)),n,k)))))
.= ((SD_Add_Data (((x div ((Radix k) |^ n)) + (y div ((Radix k) |^ n))),k)) * ((Radix k) |^ n)) + ((x mod ((Radix k) |^ n)) + (y mod ((Radix k) |^ n))) by A4, A7, A35, A34
.= (((SD_Add_Data (((x div ((Radix k) |^ n)) + (y div ((Radix k) |^ n))),k)) * ((Radix k) |^ n)) + (x mod ((Radix k) |^ n))) + (y mod ((Radix k) |^ n)) ;
then (SDDec ((DecSD (x,(n + 1),k)) '+' (DecSD (y,(n + 1),k)))) + ((SD_Add_Carry ((x div ((Radix k) |^ n)) + (y div ((Radix k) |^ n)))) * ((Radix k) |^ (n + 1))) = ((((SD_Add_Data (((x div ((Radix k) |^ n)) + (y div ((Radix k) |^ n))),k)) * ((Radix k) |^ n)) + ((SD_Add_Carry ((x div ((Radix k) |^ n)) + (y div ((Radix k) |^ n)))) * ((Radix k) |^ (n + 1)))) + (x mod ((Radix k) |^ n))) + (y mod ((Radix k) |^ n))
.= ((((SD_Add_Data (((x div ((Radix k) |^ n)) + (y div ((Radix k) |^ n))),k)) * ((Radix k) |^ n)) + ((SD_Add_Carry ((x div ((Radix k) |^ n)) + (y div ((Radix k) |^ n)))) * (((Radix k) |^ n) * (Radix k)))) + (x mod ((Radix k) |^ n))) + (y mod ((Radix k) |^ n)) by NEWTON:6
.= (((x div ((Radix k) |^ n)) * ((Radix k) |^ n)) + (x mod ((Radix k) |^ n))) + (((y div ((Radix k) |^ n)) * ((Radix k) |^ n)) + (y mod ((Radix k) |^ n)))
.= x + y by A30, A31, NAT_D:2, PREPOWER:6 ;
hence  x + y = (SDDec ((DecSD (x,(n + 1),k)) '+' (DecSD (y,(n + 1),k)))) + (((Radix k) |^ (n + 1)) * (SD_Add_Carry ((DigA ((DecSD (x,(n + 1),k)),(n + 1))) + (DigA ((DecSD (y,(n + 1),k)),(n + 1)))))) by A8, A33, Th24; ::_thesis: verum
end;
A36: S1[1]
proof
let k, x, y be Nat; ::_thesis: ( k >= 2 & x is_represented_by 1,k & y is_represented_by 1,k implies x + y = (SDDec ((DecSD (x,1,k)) '+' (DecSD (y,1,k)))) + (((Radix k) |^ 1) * (SD_Add_Carry ((DigA ((DecSD (x,1,k)),1)) + (DigA ((DecSD (y,1,k)),1))))) )
assume  ( k >= 2 & x is_represented_by 1,k & y is_represented_by 1,k ) ; ::_thesis: x + y = (SDDec ((DecSD (x,1,k)) '+' (DecSD (y,1,k)))) + (((Radix k) |^ 1) * (SD_Add_Carry ((DigA ((DecSD (x,1,k)),1)) + (DigA ((DecSD (y,1,k)),1)))))
then A37: ( SDDec ((DecSD (x,1,k)) '+' (DecSD (y,1,k))) = SD_Add_Data ((x + y),k) & SD_Add_Carry ((DigA ((DecSD (x,1,k)),1)) + (DigA ((DecSD (y,1,k)),1))) = SD_Add_Carry (x + y) ) by Th23, Th25;
 (SD_Add_Data ((x + y),k)) + ((SD_Add_Carry (x + y)) * (Radix k)) = (x + y) - 0 ;
hence  x + y = (SDDec ((DecSD (x,1,k)) '+' (DecSD (y,1,k)))) + (((Radix k) |^ 1) * (SD_Add_Carry ((DigA ((DecSD (x,1,k)),1)) + (DigA ((DecSD (y,1,k)),1))))) by A37, NEWTON:5; ::_thesis: verum
end;
 for n being Nat st n >= 1 holds
S1[n] from NAT_1:sch_8(A36, A2);
hence  for k, x, y being Nat st k >= 2 & x is_represented_by n,k & y is_represented_by n,k holds
x + y = (SDDec ((DecSD (x,n,k)) '+' (DecSD (y,n,k)))) + (((Radix k) |^ n) * (SD_Add_Carry ((DigA ((DecSD (x,n,k)),n)) + (DigA ((DecSD (y,n,k)),n))))) by A1; ::_thesis: verum
end;