:: RADIX_3 semantic presentation

begin

       Lm1:  for k being Nat st 1 <= k holds
Radix k = (Radix (k -' 1)) + (Radix (k -' 1))
proof
let k be Nat; ::_thesis: ( 1 <= k implies Radix k = (Radix (k -' 1)) + (Radix (k -' 1)) )
assume  1 <= k ; ::_thesis: Radix k = (Radix (k -' 1)) + (Radix (k -' 1))
then  Radix k = 2 to_power ((k -' 1) + 1) by XREAL_1:235
.= (2 to_power 1) * (2 to_power (k -' 1)) by POWER:27
.= 2 * (Radix (k -' 1)) by POWER:25
.= (Radix (k -' 1)) + (Radix (k -' 1)) ;
hence  Radix k = (Radix (k -' 1)) + (Radix (k -' 1)) ; ::_thesis: verum
end;

Lm2:  for k being Nat st 1 <= k holds
(Radix k) - (Radix (k -' 1)) = Radix (k -' 1)
proof
let k be Nat; ::_thesis: ( 1 <= k implies (Radix k) - (Radix (k -' 1)) = Radix (k -' 1) )
assume  1 <= k ; ::_thesis: (Radix k) - (Radix (k -' 1)) = Radix (k -' 1)
then  (Radix k) + 0 = (Radix (k -' 1)) + (Radix (k -' 1)) by Lm1;
hence  (Radix k) - (Radix (k -' 1)) = Radix (k -' 1) ; ::_thesis: verum
end;

Lm3:  for k being Nat st 1 <= k holds
(- (Radix k)) + (Radix (k -' 1)) = - (Radix (k -' 1))
proof
let k be Nat; ::_thesis: ( 1 <= k implies (- (Radix k)) + (Radix (k -' 1)) = - (Radix (k -' 1)) )
assume  1 <= k ; ::_thesis: (- (Radix k)) + (Radix (k -' 1)) = - (Radix (k -' 1))
then  - ((Radix k) - (Radix (k -' 1))) = - (Radix (k -' 1)) by Lm2;
hence  (- (Radix k)) + (Radix (k -' 1)) = - (Radix (k -' 1)) ; ::_thesis: verum
end;

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

Lm5:  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, RADIX_1:def_9
.= DigitDC (m,i,k) by A5, A6, RADIX_1:3
.= DigA ((DecSD (m,(n + 1),k)),i) by A4, RADIX_1:def_9 ;
hence  DigA ((DecSD (m,(n + 1),k)),i) = DigA ((DecSD ((m mod ((Radix k) |^ n)),n,k)),i) ; ::_thesis: verum
end;

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

:: deftheorem  defines -SD_Sub_S RADIX_3:def_1_:_
 for k being Nat holds k -SD_Sub_S =  {  e where e is Element of INT : ( e >= - (Radix (k -' 1)) & e <= (Radix (k -' 1)) - 1 )  }  ;

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

theorem Th1: :: RADIX_3:1
for k being Nat
for i1 being Integer st i1 in k -SD_Sub holds
( (- (Radix (k -' 1))) - 1 <= i1 & i1 <= Radix (k -' 1) )
proof
let k be Nat; ::_thesis: for i1 being Integer st i1 in k -SD_Sub holds
( (- (Radix (k -' 1))) - 1 <= i1 & i1 <= Radix (k -' 1) )
let i1 be Integer; ::_thesis: ( i1 in k -SD_Sub implies ( (- (Radix (k -' 1))) - 1 <= i1 & i1 <= Radix (k -' 1) ) )
assume  i1 in k -SD_Sub ; ::_thesis: ( (- (Radix (k -' 1))) - 1 <= i1 & i1 <= Radix (k -' 1) )
then  ex i being Element of INT st
( i = i1 & (- (Radix (k -' 1))) - 1 <= i & i <= Radix (k -' 1) ) ;
hence  ( (- (Radix (k -' 1))) - 1 <= i1 & i1 <= Radix (k -' 1) ) ; ::_thesis: verum
end;

theorem Th2: :: RADIX_3:2
for k being Nat holds k -SD_Sub_S c= k -SD_Sub
proof
let k be Nat; ::_thesis: k -SD_Sub_S c= k -SD_Sub
let e be set ; :: according to TARSKI:def_3 ::_thesis: ( not e in k -SD_Sub_S or e in k -SD_Sub )
assume  e in k -SD_Sub_S ; ::_thesis: e in k -SD_Sub
then consider g being Element of INT  such that
A1: e = g and
A2: g >= - (Radix (k -' 1)) and
A3: g <= (Radix (k -' 1)) - 1 ;
 (Radix (k -' 1)) + 1 >= (Radix (k -' 1)) + 0 by XREAL_1:7;
then  - (Radix (k -' 1)) >= - ((Radix (k -' 1)) + 1) by XREAL_1:24;
then A4: g >= (- (Radix (k -' 1))) - 1 by A2, XXREAL_0:2;
 (Radix (k -' 1)) + 0 >= (Radix (k -' 1)) + (- 1) by XREAL_1:7;
then  Radix (k -' 1) >= g by A3, XXREAL_0:2;
hence  e in k -SD_Sub by A1, A4; ::_thesis: verum
end;

theorem Th3: :: RADIX_3:3
for k being Nat holds k -SD_Sub_S c= (k + 1) -SD_Sub_S
proof
let k be Nat; ::_thesis: k -SD_Sub_S c= (k + 1) -SD_Sub_S
let e be set ; :: according to TARSKI:def_3 ::_thesis: ( not e in k -SD_Sub_S or e in (k + 1) -SD_Sub_S )
assume  e in k -SD_Sub_S ; ::_thesis: e in (k + 1) -SD_Sub_S
then consider g being Element of INT  such that
A1: e = g and
A2: g >= - (Radix (k -' 1)) and
A3: g <= (Radix (k -' 1)) - 1 ;
 k -' 1 <= k by NAT_D:44;
then A4: 2 to_power (k -' 1) <= 2 to_power k by PRE_FF:8;
then  (Radix (k -' 1)) - 1 <= (Radix k) - 1 by XREAL_1:9;
then  (Radix (k -' 1)) - 1 <= (Radix ((k + 1) -' 1)) - 1 by NAT_D:34;
then A5: g <= (Radix ((k + 1) -' 1)) - 1 by A3, XXREAL_0:2;
 - (Radix (k -' 1)) >= - (Radix k) by A4, XREAL_1:24;
then  - (Radix (k -' 1)) >= - (Radix ((k + 1) -' 1)) by NAT_D:34;
then  g >= - (Radix ((k + 1) -' 1)) by A2, XXREAL_0:2;
hence  e in (k + 1) -SD_Sub_S by A1, A5; ::_thesis: verum
end;

theorem :: RADIX_3:4
for k being Nat st 2 <= k holds
k -SD_Sub c= k -SD
proof
let k be Nat; ::_thesis: ( 2 <= k implies k -SD_Sub c= k -SD )
assume A1: 2 <= k ; ::_thesis: k -SD_Sub c= k -SD
then  1 + 1 <= k ;
then  1 <= k -' 1 by NAT_D:55;
then A2: Radix (k -' 1) >= 2 by Lm4;
then  Radix (k -' 1) >= 1 by XXREAL_0:2;
then  - (Radix (k -' 1)) <= - 1 by XREAL_1:24;
then A3: (Radix k) + (- (Radix (k -' 1))) <= (Radix k) + (- 1) by XREAL_1:7;
let e be set ; :: according to TARSKI:def_3 ::_thesis: ( not e in k -SD_Sub or e in k -SD )
assume  e in k -SD_Sub ; ::_thesis: e in k -SD
then consider g being Element of INT  such that
A4: e = g and
A5: g >= (- (Radix (k -' 1))) - 1 and
A6: g <= Radix (k -' 1) ;
 (Radix (k -' 1)) + (Radix (k -' 1)) >= (Radix (k -' 1)) + 2 by A2, XREAL_1:6;
then  (Radix k) + 0 >= ((Radix (k -' 1)) + 1) + 1 by A1, Lm1, XXREAL_0:2;
then  (Radix k) - 1 >= ((Radix (k -' 1)) + 1) - 0 by XREAL_1:21;
then  - ((Radix (k -' 1)) + 1) >= - ((Radix k) - 1) by XREAL_1:24;
then A7: g >= (- (Radix k)) + 1 by A5, XXREAL_0:2;
 (Radix k) + 0 = (Radix (k -' 1)) + (Radix (k -' 1)) by A1, Lm1, XXREAL_0:2;
then  g <= (Radix k) - 1 by A6, A3, XXREAL_0:2;
hence  e in k -SD by A4, A7; ::_thesis: verum
end;

theorem Th5: :: RADIX_3:5
0 in 0 -SD_Sub_S
proof
reconsider ZERO = 0 as Integer ;
 0 > 0 - 1 ;
then  0 -' 1 = 0 by XREAL_0:def_2;
then A1: Radix (0 -' 1) = 1 by POWER:24;
 ZERO is Element of INT by INT_1:def_2;
hence  0 in 0 -SD_Sub_S by A1; ::_thesis: verum
end;

theorem Th6: :: RADIX_3:6
for k being Nat holds 0 in k -SD_Sub_S
proof
let k be Nat; ::_thesis: 0 in k -SD_Sub_S
defpred S1[ Nat] means  0 in $1 -SD_Sub_S ;
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_Sub_S ; ::_thesis: S1[kk + 1]
 kk -SD_Sub_S c= (kk + 1) -SD_Sub_S by Th3;
hence  S1[kk + 1] by A2; ::_thesis: verum
end;
A3: S1[ 0 ] by Th5;
 for k being Nat holds S1[k] from NAT_1:sch_2(A3, A1);
hence  0 in k -SD_Sub_S ; ::_thesis: verum
end;

theorem Th7: :: RADIX_3:7
for k being Nat holds 0 in k -SD_Sub
proof
let k be Nat; ::_thesis: 0 in k -SD_Sub
 ( 0 in k -SD_Sub_S & k -SD_Sub_S c= k -SD_Sub ) by Th2, Th6;
hence  0 in k -SD_Sub ; ::_thesis: verum
end;

theorem Th8: :: RADIX_3:8
for k being Nat
for e being set st e in k -SD_Sub holds
e is Integer
proof
let k be Nat; ::_thesis: for e being set st e in k -SD_Sub holds
e is Integer
let e be set ; ::_thesis: ( e in k -SD_Sub implies e is Integer )
assume  e in k -SD_Sub ; ::_thesis: e is Integer
then  ex t being Element of INT st
( e = t & t >= (- (Radix (k -' 1))) - 1 & t <= Radix (k -' 1) ) ;
hence  e is Integer ; ::_thesis: verum
end;

theorem Th9: :: RADIX_3:9
for k being Nat holds k -SD_Sub c= INT
proof
let k be Nat; ::_thesis: k -SD_Sub c= INT
let e be set ; :: according to TARSKI:def_3 ::_thesis: ( not e in k -SD_Sub or e in INT )
assume  e in k -SD_Sub ; ::_thesis: e in INT
then  e is Integer by Th8;
hence  e in INT by INT_1:def_2; ::_thesis: verum
end;

theorem Th10: :: RADIX_3:10
for k being Nat holds k -SD_Sub_S c= INT
proof
let k be Nat; ::_thesis: k -SD_Sub_S c= INT
let e be set ; :: according to TARSKI:def_3 ::_thesis: ( not e in k -SD_Sub_S or e in INT )
assume A1: e in k -SD_Sub_S ; ::_thesis: e in INT
 k -SD_Sub_S c= k -SD_Sub by Th2;
then  e is Integer by A1, Th8;
hence  e in INT by INT_1:def_2; ::_thesis: verum
end;

registration
let k be Nat;
clusterk -SD_Sub_S  ->  non empty ;
coherence
 not k -SD_Sub_S is empty by Th6;
clusterk -SD_Sub  ->  non empty ;
coherence
 not k -SD_Sub is empty by Th7;
end;

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

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


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

begin

definition
let x be Integer;
let k be Nat;
func SDSub_Add_Carry (x,k) ->  Integer equals :Def3: :: RADIX_3:def 3
1 if  Radix (k -' 1) <= x
- 1 if x < - (Radix (k -' 1))
otherwise  0 ;
coherence
 ( ( Radix (k -' 1) <= x implies 1 is Integer ) & ( x < - (Radix (k -' 1)) implies - 1 is Integer ) & ( not Radix (k -' 1) <= x & not x < - (Radix (k -' 1)) implies 0 is Integer ) ) ;
consistency
 for b1 being Integer st Radix (k -' 1) <= x & x < - (Radix (k -' 1)) holds
( b1 = 1 iff b1 = - 1 ) ;
end;

:: deftheorem Def3 defines SDSub_Add_Carry RADIX_3:def_3_:_
 for x being Integer
for k being Nat holds
( ( Radix (k -' 1) <= x implies SDSub_Add_Carry (x,k) = 1 ) & ( x < - (Radix (k -' 1)) implies SDSub_Add_Carry (x,k) = - 1 ) & ( not Radix (k -' 1) <= x & not x < - (Radix (k -' 1)) implies SDSub_Add_Carry (x,k) = 0 ) );

definition
let x be Integer;
let k be Nat;
func SDSub_Add_Data (x,k) ->  Integer equals :: RADIX_3:def 4
x - ((Radix k) * (SDSub_Add_Carry (x,k)));
coherence
 x - ((Radix k) * (SDSub_Add_Carry (x,k))) is Integer ;
end;

:: deftheorem  defines SDSub_Add_Data RADIX_3:def_4_:_
 for x being Integer
for k being Nat holds SDSub_Add_Data (x,k) = x - ((Radix k) * (SDSub_Add_Carry (x,k)));

theorem Th12: :: RADIX_3:12
for x being Integer
for k being Nat holds
( - 1 <= SDSub_Add_Carry (x,k) & SDSub_Add_Carry (x,k) <= 1 )
proof
let x be Integer; ::_thesis: for k being Nat holds
( - 1 <= SDSub_Add_Carry (x,k) & SDSub_Add_Carry (x,k) <= 1 )
let k be Nat; ::_thesis: ( - 1 <= SDSub_Add_Carry (x,k) & SDSub_Add_Carry (x,k) <= 1 )
percases ( x < - (Radix (k -' 1)) or ( - (Radix (k -' 1)) <= x & x < Radix (k -' 1) ) or x >= Radix (k -' 1) ) ;
suppose x < - (Radix (k -' 1)) ; ::_thesis: ( - 1 <= SDSub_Add_Carry (x,k) & SDSub_Add_Carry (x,k) <= 1 )
hence  ( - 1 <= SDSub_Add_Carry (x,k) & SDSub_Add_Carry (x,k) <= 1 ) by Def3; ::_thesis: verum
end;
suppose ( - (Radix (k -' 1)) <= x & x < Radix (k -' 1) ) ; ::_thesis: ( - 1 <= SDSub_Add_Carry (x,k) & SDSub_Add_Carry (x,k) <= 1 )
hence  ( - 1 <= SDSub_Add_Carry (x,k) & SDSub_Add_Carry (x,k) <= 1 ) by Def3; ::_thesis: verum
end;
suppose x >= Radix (k -' 1) ; ::_thesis: ( - 1 <= SDSub_Add_Carry (x,k) & SDSub_Add_Carry (x,k) <= 1 )
hence  ( - 1 <= SDSub_Add_Carry (x,k) & SDSub_Add_Carry (x,k) <= 1 ) by Def3; ::_thesis: verum
end;
end;
end;

theorem Th13: :: RADIX_3:13
for k being Nat
for i1 being Integer st 2 <= k & i1 in k -SD holds
( SDSub_Add_Data (i1,k) >= - (Radix (k -' 1)) & SDSub_Add_Data (i1,k) <= (Radix (k -' 1)) - 1 )
proof
let k be Nat; ::_thesis: for i1 being Integer st 2 <= k & i1 in k -SD holds
( SDSub_Add_Data (i1,k) >= - (Radix (k -' 1)) & SDSub_Add_Data (i1,k) <= (Radix (k -' 1)) - 1 )
let i1 be Integer; ::_thesis: ( 2 <= k & i1 in k -SD implies ( SDSub_Add_Data (i1,k) >= - (Radix (k -' 1)) & SDSub_Add_Data (i1,k) <= (Radix (k -' 1)) - 1 ) )
assume that
A1: 2 <= k and
A2: i1 in k -SD ; ::_thesis: ( SDSub_Add_Data (i1,k) >= - (Radix (k -' 1)) & SDSub_Add_Data (i1,k) <= (Radix (k -' 1)) - 1 )
A3: ( (- (Radix k)) + 1 <= i1 & 1 <= k ) by A1, A2, RADIX_1:13, XXREAL_0:2;
now__::_thesis:_(_(_i1_<_-_(Radix_(k_-'_1))_&_SDSub_Add_Data_(i1,k)_>=_-_(Radix_(k_-'_1))_&_SDSub_Add_Data_(i1,k)_<=_(Radix_(k_-'_1))_-_1_)_or_(_-_(Radix_(k_-'_1))_<=_i1_&_i1_<_Radix_(k_-'_1)_&_SDSub_Add_Data_(i1,k)_>=_-_(Radix_(k_-'_1))_&_SDSub_Add_Data_(i1,k)_<=_(Radix_(k_-'_1))_-_1_)_or_(_Radix_(k_-'_1)_<=_i1_&_SDSub_Add_Data_(i1,k)_>=_-_(Radix_(k_-'_1))_&_SDSub_Add_Data_(i1,k)_<=_(Radix_(k_-'_1))_-_1_)_)
percases ( i1 < - (Radix (k -' 1)) or ( - (Radix (k -' 1)) <= i1 & i1 < Radix (k -' 1) ) or Radix (k -' 1) <= i1 ) ;
caseA4: i1 < - (Radix (k -' 1)) ; ::_thesis: ( SDSub_Add_Data (i1,k) >= - (Radix (k -' 1)) & SDSub_Add_Data (i1,k) <= (Radix (k -' 1)) - 1 )
then  i1 + 1 <= - (Radix (k -' 1)) by INT_1:7;
then  i1 <= (- (Radix (k -' 1))) - 1 by XREAL_1:19;
then  i1 + (Radix k) <= (Radix k) + ((- (Radix (k -' 1))) - 1) by XREAL_1:7;
then A5: i1 + (Radix k) <= ((Radix k) - (Radix (k -' 1))) - 1 ;
 SDSub_Add_Carry (i1,k) = - 1 by A4, Def3;
hence  ( SDSub_Add_Data (i1,k) >= - (Radix (k -' 1)) & SDSub_Add_Data (i1,k) <= (Radix (k -' 1)) - 1 ) by A3, A5, Lm2, XREAL_1:19; ::_thesis: verum
end;
caseA6: ( - (Radix (k -' 1)) <= i1 & i1 < Radix (k -' 1) ) ; ::_thesis: ( SDSub_Add_Data (i1,k) >= - (Radix (k -' 1)) & SDSub_Add_Data (i1,k) <= (Radix (k -' 1)) - 1 )
then  ( SDSub_Add_Carry (i1,k) = 0 & i1 + 1 <= Radix (k -' 1) ) by Def3, INT_1:7;
hence  ( SDSub_Add_Data (i1,k) >= - (Radix (k -' 1)) & SDSub_Add_Data (i1,k) <= (Radix (k -' 1)) - 1 ) by A6, XREAL_1:19; ::_thesis: verum
end;
caseA7: Radix (k -' 1) <= i1 ; ::_thesis: ( SDSub_Add_Data (i1,k) >= - (Radix (k -' 1)) & SDSub_Add_Data (i1,k) <= (Radix (k -' 1)) - 1 )
 i1 <= (Radix k) + (- 1) by A2, RADIX_1:13;
then A8: ( 0 - 1 <= (Radix (k -' 1)) - 1 & i1 - (Radix k) <= - 1 ) by XREAL_1:9, XREAL_1:20;
 ( SDSub_Add_Carry (i1,k) = 1 & (Radix (k -' 1)) + (- (Radix k)) <= i1 + (- (Radix k)) ) by A7, Def3, XREAL_1:6;
hence  ( SDSub_Add_Data (i1,k) >= - (Radix (k -' 1)) & SDSub_Add_Data (i1,k) <= (Radix (k -' 1)) - 1 ) by A1, A8, Lm3, XXREAL_0:2; ::_thesis: verum
end;
end;
end;
hence  ( SDSub_Add_Data (i1,k) >= - (Radix (k -' 1)) & SDSub_Add_Data (i1,k) <= (Radix (k -' 1)) - 1 ) ; ::_thesis: verum
end;

theorem Th14: :: RADIX_3:14
for x being Integer
for k being Nat st 2 <= k holds
SDSub_Add_Carry (x,k) in k -SD_Sub_S
proof
let x be Integer; ::_thesis: for k being Nat st 2 <= k holds
SDSub_Add_Carry (x,k) in k -SD_Sub_S
let k be Nat; ::_thesis: ( 2 <= k implies SDSub_Add_Carry (x,k) in k -SD_Sub_S )
A1: SDSub_Add_Carry (x,k) <= 1 by Th12;
assume  k >= 2 ; ::_thesis: SDSub_Add_Carry (x,k) in k -SD_Sub_S
then  k > 1 by XXREAL_0:2;
then  k - 1 > 1 - 1 by XREAL_1:14;
then A2: k -' 1 > 0 by XREAL_0:def_2;
then  2 to_power (k -' 1) > 1 by POWER:35;
then A3: - (Radix (k -' 1)) <= - 1 by XREAL_1:24;
 - 1 <= SDSub_Add_Carry (x,k) by Th12;
then A4: SDSub_Add_Carry (x,k) >= - (Radix (k -' 1)) by A3, XXREAL_0:2;
 (Radix (k -' 1)) - 1 >= 1 by A2, INT_1:52, POWER:35;
then A5: SDSub_Add_Carry (x,k) <= (Radix (k -' 1)) - 1 by A1, XXREAL_0:2;
 SDSub_Add_Carry (x,k) is Element of INT by INT_1:def_2;
hence  SDSub_Add_Carry (x,k) in k -SD_Sub_S by A5, A4; ::_thesis: verum
end;

theorem Th15: :: RADIX_3:15
for k being Nat
for i1, i2 being Integer st 2 <= k & i1 in k -SD holds
(SDSub_Add_Data (i1,k)) + (SDSub_Add_Carry (i2,k)) in k -SD_Sub
proof
let k be Nat; ::_thesis: for i1, i2 being Integer st 2 <= k & i1 in k -SD holds
(SDSub_Add_Data (i1,k)) + (SDSub_Add_Carry (i2,k)) in k -SD_Sub
let i1, i2 be Integer; ::_thesis: ( 2 <= k & i1 in k -SD implies (SDSub_Add_Data (i1,k)) + (SDSub_Add_Carry (i2,k)) in k -SD_Sub )
A1: SDSub_Add_Carry (i2,k) >= - 1 by Th12;
assume A2: ( 2 <= k & i1 in k -SD ) ; ::_thesis: (SDSub_Add_Data (i1,k)) + (SDSub_Add_Carry (i2,k)) in k -SD_Sub
then  SDSub_Add_Data (i1,k) >= - (Radix (k -' 1)) by Th13;
then A3: (SDSub_Add_Data (i1,k)) + (SDSub_Add_Carry (i2,k)) >= (- (Radix (k -' 1))) + (- 1) by A1, XREAL_1:7;
A4: SDSub_Add_Carry (i2,k) <= 1 by Th12;
 SDSub_Add_Data (i1,k) <= (Radix (k -' 1)) - 1 by A2, Th13;
then A5: (SDSub_Add_Data (i1,k)) + (SDSub_Add_Carry (i2,k)) <= ((Radix (k -' 1)) - 1) + 1 by A4, XREAL_1:7;
 (SDSub_Add_Data (i1,k)) + (SDSub_Add_Carry (i2,k)) is Element of INT by INT_1:def_2;
hence  (SDSub_Add_Data (i1,k)) + (SDSub_Add_Carry (i2,k)) in k -SD_Sub by A3, A5; ::_thesis: verum
end;

theorem Th16: :: RADIX_3:16
for k being Nat holds SDSub_Add_Carry (0,k) = 0
proof
let k be Nat; ::_thesis: SDSub_Add_Carry (0,k) = 0
set x = 0 ;
 ( Radix (k -' 1) <> 0 & - (Radix (k -' 1)) <= 0 - 0 ) by POWER:34;
hence  SDSub_Add_Carry (0,k) = 0 by Def3; ::_thesis: verum
end;

begin

definition
let i, k, n be Nat;
let x be Tuple of n,k -SD_Sub ;
func DigA_SDSub (x,i) ->  Integer equals :Def5: :: RADIX_3:def 5
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 Def5 defines DigA_SDSub RADIX_3:def_5_:_
 for i, k, n being Nat
for x being Tuple of n,k -SD_Sub holds
( ( i in Seg n implies DigA_SDSub (x,i) = x . i ) & ( i = 0 implies DigA_SDSub (x,i) = 0 ) );

definition
let i, k, n be Nat;
let x be Tuple of n,k -SD ;
func SD2SDSubDigit (x,i,k) ->  Integer equals :Def6: :: RADIX_3:def 6
(SDSub_Add_Data ((DigA (x,i)),k)) + (SDSub_Add_Carry ((DigA (x,(i -' 1))),k)) if i in Seg n
SDSub_Add_Carry ((DigA (x,(i -' 1))),k) if i = n + 1
otherwise  0 ;
coherence
 ( ( i in Seg n implies (SDSub_Add_Data ((DigA (x,i)),k)) + (SDSub_Add_Carry ((DigA (x,(i -' 1))),k)) is Integer ) & ( i = n + 1 implies SDSub_Add_Carry ((DigA (x,(i -' 1))),k) is Integer ) & ( not i in Seg n & not i = n + 1 implies 0 is Integer ) ) ;
consistency
 for b1 being Integer st i in Seg n & i = n + 1 holds
( b1 = (SDSub_Add_Data ((DigA (x,i)),k)) + (SDSub_Add_Carry ((DigA (x,(i -' 1))),k)) iff b1 = SDSub_Add_Carry ((DigA (x,(i -' 1))),k) )
proof
 ( i in Seg n implies not i = n + 1 )
proof
assume  i in Seg n ; ::_thesis: not i = n + 1
then A1: i <= n by FINSEQ_1:1;
assume  i = n + 1 ; ::_thesis: contradiction
hence  contradiction by A1, NAT_1:13; ::_thesis: verum
end;
hence  for b1 being Integer st i in Seg n & i = n + 1 holds
( b1 = (SDSub_Add_Data ((DigA (x,i)),k)) + (SDSub_Add_Carry ((DigA (x,(i -' 1))),k)) iff b1 = SDSub_Add_Carry ((DigA (x,(i -' 1))),k) ) ; ::_thesis: verum
end;
end;

:: deftheorem Def6 defines SD2SDSubDigit RADIX_3:def_6_:_
 for i, k, n being Nat
for x being Tuple of n,k -SD holds
( ( i in Seg n implies SD2SDSubDigit (x,i,k) = (SDSub_Add_Data ((DigA (x,i)),k)) + (SDSub_Add_Carry ((DigA (x,(i -' 1))),k)) ) & ( i = n + 1 implies SD2SDSubDigit (x,i,k) = SDSub_Add_Carry ((DigA (x,(i -' 1))),k) ) & ( not i in Seg n & not i = n + 1 implies SD2SDSubDigit (x,i,k) = 0 ) );

theorem Th17: :: RADIX_3:17
for k, i, n being Nat
for a being Tuple of n,k -SD st 2 <= k & i in Seg (n + 1) holds
SD2SDSubDigit (a,i,k) is Element of k -SD_Sub
proof
let k, i, n be Nat; ::_thesis: for a being Tuple of n,k -SD st 2 <= k & i in Seg (n + 1) holds
SD2SDSubDigit (a,i,k) is Element of k -SD_Sub
let a be Tuple of n,k -SD ; ::_thesis: ( 2 <= k & i in Seg (n + 1) implies SD2SDSubDigit (a,i,k) is Element of k -SD_Sub )
assume that
A1: 2 <= k and
A2: i in Seg (n + 1) ; ::_thesis: SD2SDSubDigit (a,i,k) is Element of k -SD_Sub
set SDD = (SDSub_Add_Data ((DigA (a,i)),k)) + (SDSub_Add_Carry ((DigA (a,(i -' 1))),k));
set SDC = SDSub_Add_Carry ((DigA (a,(i -' 1))),k);
now__::_thesis:_SD2SDSubDigit_(a,i,k)_in_k_-SD_Sub
percases ( i in Seg n or i = n + 1 ) by A2, FINSEQ_2:7;
supposeA3: i in Seg n ; ::_thesis: SD2SDSubDigit (a,i,k) in k -SD_Sub
 (SDSub_Add_Data ((DigA (a,i)),k)) + (SDSub_Add_Carry ((DigA (a,(i -' 1))),k)) in k -SD_Sub
proof
 DigA (a,i) is Element of k -SD by A3, RADIX_1:16;
hence  (SDSub_Add_Data ((DigA (a,i)),k)) + (SDSub_Add_Carry ((DigA (a,(i -' 1))),k)) in k -SD_Sub by A1, Th15; ::_thesis: verum
end;
hence  SD2SDSubDigit (a,i,k) in k -SD_Sub by A3, Def6; ::_thesis: verum
end;
supposeA4: i = n + 1 ; ::_thesis: SD2SDSubDigit (a,i,k) in k -SD_Sub
 ( SDSub_Add_Carry ((DigA (a,(i -' 1))),k) in k -SD_Sub_S & k -SD_Sub_S c= k -SD_Sub ) by A1, Th2, Th14;
then  SDSub_Add_Carry ((DigA (a,(i -' 1))),k) in k -SD_Sub ;
hence  SD2SDSubDigit (a,i,k) in k -SD_Sub by A4, Def6; ::_thesis: verum
end;
end;
end;
hence  SD2SDSubDigit (a,i,k) is Element of k -SD_Sub ; ::_thesis: verum
end;

definition
let i, k, n be Nat;
let x be Tuple of n,k -SD ;
assume A1: ( 2 <= k & i in Seg (n + 1) ) ;
func SD2SDSubDigitS (x,i,k) ->  Element of k -SD_Sub  equals :Def7: :: RADIX_3:def 7
 SD2SDSubDigit (x,i,k);
coherence
 SD2SDSubDigit (x,i,k) is Element of k -SD_Sub by A1, Th17;
end;

:: deftheorem Def7 defines SD2SDSubDigitS RADIX_3:def_7_:_
 for i, k, n being Nat
for x being Tuple of n,k -SD st 2 <= k & i in Seg (n + 1) holds
SD2SDSubDigitS (x,i,k) = SD2SDSubDigit (x,i,k);

definition
let n, k be Nat;
let x be Tuple of n,k -SD ;
func SD2SDSub x ->  Tuple of n + 1,k -SD_Sub  means :Def8: :: RADIX_3:def 8
 for i being Nat st i in Seg (n + 1) holds
DigA_SDSub (it,i) = SD2SDSubDigitS (x,i,k);
existence
 ex b1 being Tuple of n + 1,k -SD_Sub st
for i being Nat st i in Seg (n + 1) holds
DigA_SDSub (b1,i) = SD2SDSubDigitS (x,i,k)
proof
deffunc H1( Nat) ->  Element of k -SD_Sub = SD2SDSubDigitS (x,$1,k);
consider z being FinSequence of k -SD_Sub  such that
A1: len z = n + 1 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 + 1) by A1, FINSEQ_1:def_3;
 z is Element of (n + 1) -tuples_on (k -SD_Sub) by A1, FINSEQ_2:92;
then reconsider z = z as Tuple of n + 1,k -SD_Sub ;
take  z ; ::_thesis: for i being Nat st i in Seg (n + 1) holds
DigA_SDSub (z,i) = SD2SDSubDigitS (x,i,k)
let i be Nat; ::_thesis: ( i in Seg (n + 1) implies DigA_SDSub (z,i) = SD2SDSubDigitS (x,i,k) )
assume A4: i in Seg (n + 1) ; ::_thesis: DigA_SDSub (z,i) = SD2SDSubDigitS (x,i,k)
hence  DigA_SDSub (z,i) = z . i by Def5
.= SD2SDSubDigitS (x,i,k) by A2, A3, A4 ;
::_thesis: verum
end;
uniqueness
 for b1, b2 being Tuple of n + 1,k -SD_Sub st ( for i being Nat st i in Seg (n + 1) holds
DigA_SDSub (b1,i) = SD2SDSubDigitS (x,i,k) ) & ( for i being Nat st i in Seg (n + 1) holds
DigA_SDSub (b2,i) = SD2SDSubDigitS (x,i,k) ) holds
b1 = b2
proof
let k1, k2 be Tuple of n + 1,k -SD_Sub ; ::_thesis: ( ( for i being Nat st i in Seg (n + 1) holds
DigA_SDSub (k1,i) = SD2SDSubDigitS (x,i,k) ) & ( for i being Nat st i in Seg (n + 1) holds
DigA_SDSub (k2,i) = SD2SDSubDigitS (x,i,k) ) implies k1 = k2 )
assume that
A5: for i being Nat st i in Seg (n + 1) holds
DigA_SDSub (k1,i) = SD2SDSubDigitS (x,i,k) and
A6: for i being Nat st i in Seg (n + 1) holds
DigA_SDSub (k2,i) = SD2SDSubDigitS (x,i,k) ; ::_thesis: k1 = k2
A7: len k1 = n + 1 by CARD_1:def_7;
then A8: dom k1 = Seg (n + 1) 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_SDSub (k1,j) by A8, Def5
.= SD2SDSubDigitS (x,j,k) by A5, A8, A10
.= DigA_SDSub (k2,j) by A6, A8, A10
.= k2 . j by A8, A10, Def5 ;
hence  k1 . j = k2 . j ; ::_thesis: verum
end;
 len k2 = n + 1 by CARD_1:def_7;
hence  k1 = k2 by A7, A9, FINSEQ_2:9; ::_thesis: verum
end;
end;

:: deftheorem Def8 defines SD2SDSub RADIX_3:def_8_:_
 for n, k being Nat
for x being Tuple of n,k -SD
for b4 being Tuple of n + 1,k -SD_Sub holds
( b4 = SD2SDSub x iff for i being Nat st i in Seg (n + 1) holds
DigA_SDSub (b4,i) = SD2SDSubDigitS (x,i,k) );

theorem :: RADIX_3:18
for i, n, k being Nat
for aSub being Tuple of n,k -SD_Sub st i in Seg n holds
DigA_SDSub (aSub,i) is Element of k -SD_Sub
proof
let i, n, k be Nat; ::_thesis: for aSub being Tuple of n,k -SD_Sub st i in Seg n holds
DigA_SDSub (aSub,i) is Element of k -SD_Sub
let aSub be Tuple of n,k -SD_Sub ; ::_thesis: ( i in Seg n implies DigA_SDSub (aSub,i) is Element of k -SD_Sub )
assume A1: i in Seg n ; ::_thesis: DigA_SDSub (aSub,i) is Element of k -SD_Sub
then  aSub . i = DigA_SDSub (aSub,i) by Def5;
hence  DigA_SDSub (aSub,i) is Element of k -SD_Sub by A1, Th11; ::_thesis: verum
end;

theorem :: RADIX_3:19
for k being Nat
for i1, i2 being Integer st 2 <= k & i1 in k -SD & i2 in k -SD_Sub holds
SDSub_Add_Data ((i1 + i2),k) in k -SD_Sub_S
proof
let k be Nat; ::_thesis: for i1, i2 being Integer st 2 <= k & i1 in k -SD & i2 in k -SD_Sub holds
SDSub_Add_Data ((i1 + i2),k) in k -SD_Sub_S
let i1, i2 be Integer; ::_thesis: ( 2 <= k & i1 in k -SD & i2 in k -SD_Sub implies SDSub_Add_Data ((i1 + i2),k) in k -SD_Sub_S )
assume that
A1: 2 <= k and
A2: ( i1 in k -SD & i2 in k -SD_Sub ) ; ::_thesis: SDSub_Add_Data ((i1 + i2),k) in k -SD_Sub_S
set z = i1 + i2;
 ( i1 <= (Radix k) - 1 & i2 <= Radix (k -' 1) ) by A2, Th1, RADIX_1:13;
then A3: i1 + i2 <= ((Radix k) - 1) + (Radix (k -' 1)) by XREAL_1:7;
 ( (- (Radix k)) + 1 <= i1 & (- (Radix (k -' 1))) - 1 <= i2 ) by A2, Th1, RADIX_1:13;
then A4: ((- (Radix k)) + 1) + ((- (Radix (k -' 1))) - 1) <= i1 + i2 by XREAL_1:7;
A5: ( SDSub_Add_Data ((i1 + i2),k) >= - (Radix (k -' 1)) & SDSub_Add_Data ((i1 + i2),k) <= (Radix (k -' 1)) - 1 )
proof
now__::_thesis:_(_(_i1_+_i2_<_-_(Radix_(k_-'_1))_&_SDSub_Add_Data_((i1_+_i2),k)_>=_-_(Radix_(k_-'_1))_&_SDSub_Add_Data_((i1_+_i2),k)_<=_(Radix_(k_-'_1))_-_1_)_or_(_-_(Radix_(k_-'_1))_<=_i1_+_i2_&_i1_+_i2_<_Radix_(k_-'_1)_&_SDSub_Add_Data_((i1_+_i2),k)_>=_-_(Radix_(k_-'_1))_&_SDSub_Add_Data_((i1_+_i2),k)_<=_(Radix_(k_-'_1))_-_1_)_or_(_Radix_(k_-'_1)_<=_i1_+_i2_&_SDSub_Add_Data_((i1_+_i2),k)_>=_-_(Radix_(k_-'_1))_&_SDSub_Add_Data_((i1_+_i2),k)_<=_(Radix_(k_-'_1))_-_1_)_)
percases ( i1 + i2 < - (Radix (k -' 1)) or ( - (Radix (k -' 1)) <= i1 + i2 & i1 + i2 < Radix (k -' 1) ) or Radix (k -' 1) <= i1 + i2 ) ;
caseA6: i1 + i2 < - (Radix (k -' 1)) ; ::_thesis: ( SDSub_Add_Data ((i1 + i2),k) >= - (Radix (k -' 1)) & SDSub_Add_Data ((i1 + i2),k) <= (Radix (k -' 1)) - 1 )
then  (i1 + i2) + 1 <= - (Radix (k -' 1)) by INT_1:7;
then  i1 + i2 <= (- (Radix (k -' 1))) - 1 by XREAL_1:19;
then  i1 + i2 <= (- (Radix (k -' 1))) + (- 1) ;
then  i1 + i2 <= ((- (Radix k)) + (Radix (k -' 1))) + (- 1) by A1, Lm3, XXREAL_0:2;
then A7: i1 + i2 <= (- (Radix k)) + ((Radix (k -' 1)) + (- 1)) ;
 (- (Radix (k -' 1))) + (- (Radix k)) <= (i1 + i2) + 0 by A4;
then A8: (- (Radix (k -' 1))) - 0 <= (i1 + i2) - (- (Radix k)) by XREAL_1:21;
 SDSub_Add_Carry ((i1 + i2),k) = - 1 by A6, Def3;
hence  ( SDSub_Add_Data ((i1 + i2),k) >= - (Radix (k -' 1)) & SDSub_Add_Data ((i1 + i2),k) <= (Radix (k -' 1)) - 1 ) by A8, A7, XREAL_1:20; ::_thesis: verum
end;
caseA9: ( - (Radix (k -' 1)) <= i1 + i2 & i1 + i2 < Radix (k -' 1) ) ; ::_thesis: ( SDSub_Add_Data ((i1 + i2),k) >= - (Radix (k -' 1)) & SDSub_Add_Data ((i1 + i2),k) <= (Radix (k -' 1)) - 1 )
then  ( SDSub_Add_Carry ((i1 + i2),k) = 0 & (i1 + i2) + 1 <= Radix (k -' 1) ) by Def3, INT_1:7;
hence  ( SDSub_Add_Data ((i1 + i2),k) >= - (Radix (k -' 1)) & SDSub_Add_Data ((i1 + i2),k) <= (Radix (k -' 1)) - 1 ) by A9, XREAL_1:19; ::_thesis: verum
end;
caseA10: Radix (k -' 1) <= i1 + i2 ; ::_thesis: ( SDSub_Add_Data ((i1 + i2),k) >= - (Radix (k -' 1)) & SDSub_Add_Data ((i1 + i2),k) <= (Radix (k -' 1)) - 1 )
then  (Radix k) - (Radix (k -' 1)) <= i1 + i2 by A1, Lm2, XXREAL_0:2;
then A11: (Radix k) + (- (Radix (k -' 1))) <= i1 + i2 ;
A12: i1 + i2 <= (Radix k) + ((Radix (k -' 1)) - 1) by A3;
 SDSub_Add_Carry ((i1 + i2),k) = 1 by A10, Def3;
hence  ( SDSub_Add_Data ((i1 + i2),k) >= - (Radix (k -' 1)) & SDSub_Add_Data ((i1 + i2),k) <= (Radix (k -' 1)) - 1 ) by A11, A12, XREAL_1:19, XREAL_1:20; ::_thesis: verum
end;
end;
end;
hence  ( SDSub_Add_Data ((i1 + i2),k) >= - (Radix (k -' 1)) & SDSub_Add_Data ((i1 + i2),k) <= (Radix (k -' 1)) - 1 ) ; ::_thesis: verum
end;
 SDSub_Add_Data ((i1 + i2),k) is Element of INT by INT_1:def_2;
hence  SDSub_Add_Data ((i1 + i2),k) in k -SD_Sub_S by A5; ::_thesis: verum
end;

begin

definition
let i, k, n be Nat;
let x be Tuple of n,k -SD_Sub ;
func DigB_SDSub (x,i) ->  Element of INT  equals :: RADIX_3:def 9
 DigA_SDSub (x,i);
coherence
 DigA_SDSub (x,i) is Element of INT by INT_1:def_2;
end;

:: deftheorem  defines DigB_SDSub RADIX_3:def_9_:_
 for i, k, n being Nat
for x being Tuple of n,k -SD_Sub holds DigB_SDSub (x,i) = DigA_SDSub (x,i);

definition
let i, k, n be Nat;
let x be Tuple of n,k -SD_Sub ;
func SDSub2INTDigit (x,i,k) ->  Element of INT  equals :: RADIX_3:def 10
((Radix k) |^ (i -' 1)) * (DigB_SDSub (x,i));
coherence
 ((Radix k) |^ (i -' 1)) * (DigB_SDSub (x,i)) is Element of INT by INT_1:def_2;
end;

:: deftheorem  defines SDSub2INTDigit RADIX_3:def_10_:_
 for i, k, n being Nat
for x being Tuple of n,k -SD_Sub holds SDSub2INTDigit (x,i,k) = ((Radix k) |^ (i -' 1)) * (DigB_SDSub (x,i));

definition
let n, k be Nat;
let x be Tuple of n,k -SD_Sub ;
func SDSub2INT x ->  Tuple of n, INT  means :Def11: :: RADIX_3:def 11
 for i being Nat st i in Seg n holds
it /. i = SDSub2INTDigit (x,i,k);
existence
 ex b1 being Tuple of n, INT st
for i being Nat st i in Seg n holds
b1 /. i = SDSub2INTDigit (x,i,k)
proof
deffunc H1( Nat) ->  Element of INT = SDSub2INTDigit (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;
 z is Element of n -tuples_on INT by A1, FINSEQ_2:92;
then reconsider z = z as Tuple of n, INT ;
take  z ; ::_thesis: for i being Nat st i in Seg n holds
z /. i = SDSub2INTDigit (x,i,k)
let i be Nat; ::_thesis: ( i in Seg n implies z /. i = SDSub2INTDigit (x,i,k) )
assume A4: i in Seg n ; ::_thesis: z /. i = SDSub2INTDigit (x,i,k)
then  i in dom z by A1, FINSEQ_1:def_3;
hence z /. i = z . i by PARTFUN1:def_6
.= SDSub2INTDigit (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 = SDSub2INTDigit (x,i,k) ) & ( for i being Nat st i in Seg n holds
b2 /. i = SDSub2INTDigit (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 = SDSub2INTDigit (x,i,k) ) & ( for i being Nat st i in Seg n holds
k2 /. i = SDSub2INTDigit (x,i,k) ) implies k1 = k2 )
assume that
A5: for i being Nat st i in Seg n holds
k1 /. i = SDSub2INTDigit (x,i,k) and
A6: for i being Nat st i in Seg n holds
k2 /. i = SDSub2INTDigit (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
.= SDSub2INTDigit (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 Def11 defines SDSub2INT RADIX_3:def_11_:_
 for n, k being Nat
for x being Tuple of n,k -SD_Sub
for b4 being Tuple of n, INT holds
( b4 = SDSub2INT x iff for i being Nat st i in Seg n holds
b4 /. i = SDSub2INTDigit (x,i,k) );

definition
let n, k be Nat;
let x be Tuple of n,k -SD_Sub ;
func SDSub2IntOut x ->  Integer equals :: RADIX_3:def 12
 Sum (SDSub2INT x);
coherence
 Sum (SDSub2INT x) is Integer ;
end;

:: deftheorem  defines SDSub2IntOut RADIX_3:def_12_:_
 for n, k being Nat
for x being Tuple of n,k -SD_Sub holds SDSub2IntOut x = Sum (SDSub2INT x);

theorem Th20: :: RADIX_3:20
for n, k, m, i being Nat st i in Seg n & 2 <= k holds
DigA_SDSub ((SD2SDSub (DecSD (m,(n + 1),k))),i) = DigA_SDSub ((SD2SDSub (DecSD ((m mod ((Radix k) |^ n)),n,k))),i)
proof
let n, k, m, i be Nat; ::_thesis: ( i in Seg n & 2 <= k implies DigA_SDSub ((SD2SDSub (DecSD (m,(n + 1),k))),i) = DigA_SDSub ((SD2SDSub (DecSD ((m mod ((Radix k) |^ n)),n,k))),i) )
assume A1: i in Seg n ; ::_thesis: ( not 2 <= k or DigA_SDSub ((SD2SDSub (DecSD (m,(n + 1),k))),i) = DigA_SDSub ((SD2SDSub (DecSD ((m mod ((Radix k) |^ n)),n,k))),i) )
reconsider i = i as Element of NAT by ORDINAL1:def_12;
A2: 1 <= i by A1, FINSEQ_1:1;
 i <= n by A1, FINSEQ_1:1;
then A3: i <= n + 1 by NAT_1:12;
then A4: i in Seg (n + 1) by A2, FINSEQ_1:1;
 i <= (n + 1) + 1 by A3, NAT_1:12;
then A5: i in Seg ((n + 1) + 1) by A2, FINSEQ_1:1;
set M = m mod ((Radix k) |^ n);
assume A6: 2 <= k ; ::_thesis: DigA_SDSub ((SD2SDSub (DecSD (m,(n + 1),k))),i) = DigA_SDSub ((SD2SDSub (DecSD ((m mod ((Radix k) |^ n)),n,k))),i)
A7: DigA_SDSub ((SD2SDSub (DecSD ((m mod ((Radix k) |^ n)),n,k))),i) = SD2SDSubDigitS ((DecSD ((m mod ((Radix k) |^ n)),n,k)),i,k) by A4, Def8
.= SD2SDSubDigit ((DecSD ((m mod ((Radix k) |^ n)),n,k)),i,k) by A6, A4, Def7
.= (SDSub_Add_Data ((DigA ((DecSD ((m mod ((Radix k) |^ n)),n,k)),i)),k)) + (SDSub_Add_Carry ((DigA ((DecSD ((m mod ((Radix k) |^ n)),n,k)),(i -' 1))),k)) by A1, Def6
.= (SDSub_Add_Data ((DigA ((DecSD (m,(n + 1),k)),i)),k)) + (SDSub_Add_Carry ((DigA ((DecSD ((m mod ((Radix k) |^ n)),n,k)),(i -' 1))),k)) by A1, Lm5 ;
now__::_thesis:_DigA_SDSub_((SD2SDSub_(DecSD_(m,(n_+_1),k))),i)_=_DigA_SDSub_((SD2SDSub_(DecSD_((m_mod_((Radix_k)_|^_n)),n,k))),i)
percases ( i = 1 or i <> 1 ) ;
supposeA8: i = 1 ; ::_thesis: DigA_SDSub ((SD2SDSub (DecSD (m,(n + 1),k))),i) = DigA_SDSub ((SD2SDSub (DecSD ((m mod ((Radix k) |^ n)),n,k))),i)
then A9: DigA_SDSub ((SD2SDSub (DecSD ((m mod ((Radix k) |^ n)),n,k))),i) = (SDSub_Add_Data ((DigA ((DecSD (m,(n + 1),k)),i)),k)) + (SDSub_Add_Carry ((DigA ((DecSD ((m mod ((Radix k) |^ n)),n,k)),0)),k)) by A7, XREAL_1:232
.= (SDSub_Add_Data ((DigA ((DecSD (m,(n + 1),k)),i)),k)) + (SDSub_Add_Carry (0,k)) by RADIX_1:def_3
.= (SDSub_Add_Data ((DigA ((DecSD (m,(n + 1),k)),i)),k)) + 0 by Th16 ;
DigA_SDSub ((SD2SDSub (DecSD (m,(n + 1),k))),i) = SD2SDSubDigitS ((DecSD (m,(n + 1),k)),i,k) by A5, Def8
.= SD2SDSubDigit ((DecSD (m,(n + 1),k)),i,k) by A6, A5, Def7
.= (SDSub_Add_Data ((DigA ((DecSD (m,(n + 1),k)),i)),k)) + (SDSub_Add_Carry ((DigA ((DecSD (m,(n + 1),k)),(i -' 1))),k)) by A4, Def6
.= (SDSub_Add_Data ((DigA ((DecSD (m,(n + 1),k)),i)),k)) + (SDSub_Add_Carry ((DigA ((DecSD (m,(n + 1),k)),0)),k)) by A8, XREAL_1:232
.= (SDSub_Add_Data ((DigA ((DecSD (m,(n + 1),k)),i)),k)) + (SDSub_Add_Carry (0,k)) by RADIX_1:def_3
.= (SDSub_Add_Data ((DigA ((DecSD (m,(n + 1),k)),i)),k)) + 0 by Th16 ;
hence  DigA_SDSub ((SD2SDSub (DecSD (m,(n + 1),k))),i) = DigA_SDSub ((SD2SDSub (DecSD ((m mod ((Radix k) |^ n)),n,k))),i) by A9; ::_thesis: verum
end;
supposeA10: i <> 1 ; ::_thesis: DigA_SDSub ((SD2SDSub (DecSD (m,(n + 1),k))),i) = DigA_SDSub ((SD2SDSub (DecSD ((m mod ((Radix k) |^ n)),n,k))),i)
 i <= n by A1, FINSEQ_1:1;
then A11: i -' 1 <= n by NAT_D:44;
 1 < i by A2, A10, XXREAL_0:1;
then  0 + 1 <= i -' 1 by INT_1:7, JORDAN12:1;
then  i -' 1 in Seg n by A11, FINSEQ_1:1;
then  DigA_SDSub ((SD2SDSub (DecSD ((m mod ((Radix k) |^ n)),n,k))),i) = (SDSub_Add_Data ((DigA ((DecSD (m,(n + 1),k)),i)),k)) + (SDSub_Add_Carry ((DigA ((DecSD (m,(n + 1),k)),(i -' 1))),k)) by A7, Lm5
.= SD2SDSubDigit ((DecSD (m,(n + 1),k)),i,k) by A4, Def6
.= SD2SDSubDigitS ((DecSD (m,(n + 1),k)),i,k) by A6, A5, Def7
.= DigA_SDSub ((SD2SDSub (DecSD (m,(n + 1),k))),i) by A5, Def8 ;
hence  DigA_SDSub ((SD2SDSub (DecSD (m,(n + 1),k))),i) = DigA_SDSub ((SD2SDSub (DecSD ((m mod ((Radix k) |^ n)),n,k))),i) ; ::_thesis: verum
end;
end;
end;
hence  DigA_SDSub ((SD2SDSub (DecSD (m,(n + 1),k))),i) = DigA_SDSub ((SD2SDSub (DecSD ((m mod ((Radix k) |^ n)),n,k))),i) ; ::_thesis: verum
end;

theorem :: RADIX_3:21
for n being Nat st n >= 1 holds
for k, x being Nat st k >= 2 & x is_represented_by n,k holds
x = SDSub2IntOut (SD2SDSub (DecSD (x,n,k)))
proof
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 A3, FINSEQ_1:3;
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 ((Radix k) |^ n);
set RN1 = (Radix k) |^ (n + 1);
set RN = (Radix k) |^ 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) = ((Radix k) |^ (n + 1)) * (DigB_SDSub ((SD2SDSub (DecSD (x,(n + 1),k))),((n + 1) + 1))) by NAT_D:34
.= ((Radix k) |^ (n + 1)) * (SD2SDSubDigitS ((DecSD (x,(n + 1),k)),((n + 1) + 1),k)) by A8, Def8
.= ((Radix k) |^ (n + 1)) * (SD2SDSubDigit ((DecSD (x,(n + 1),k)),((n + 1) + 1),k)) by A6, A8, Def7
.= ((Radix k) |^ (n + 1)) * (SDSub_Add_Carry ((DigA ((DecSD (x,(n + 1),k)),(((n + 1) + 1) -' 1))),k)) by Def6
.= ((Radix k) |^ (n + 1)) * (SDSub_Add_Carry ((DigA ((DecSD (x,(n + 1),k)),(n + 1))),k)) by NAT_D:34 ;
set XN = SD2SDSub (DecSD ((x mod ((Radix k) |^ 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 FINSEQ_2:sch_1();
A12: dom xp = Seg (n + 1) by A10, FINSEQ_1:def_3;
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 A16, CARD_1:def_7;
then A17: j in Seg ((n + 1) + 1) by A15, FINSEQ_1:1;
A18: j in dom (SDSub2INT (SD2SDSub (DecSD (x,(n + 1),k)))) by A15, A16, FINSEQ_3:25;
now__::_thesis:_(SDSub2INT_(SD2SDSub_(DecSD_(x,(n_+_1),k))))_._j_=_(xp_^_<*(SDSub2INTDigit_((SD2SDSub_(DecSD_(x,(n_+_1),k))),((n_+_1)_+_1),k))*>)_._j
percases ( j in Seg (n + 1) or j = (n + 1) + 1 ) by A17, FINSEQ_2:7;
supposeA19: 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 A10, FINSEQ_1:def_3;
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 A11, A12, A19
.= (SDSub2INT (SD2SDSub (DecSD (x,(n + 1),k)))) /. j by A17, Def11
.= (SDSub2INT (SD2SDSub (DecSD (x,(n + 1),k)))) . j by A18, PARTFUN1:def_6 ;
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;
supposeA20: 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 A13, A17, FINSEQ_1:def_3;
(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 A10, A20, FINSEQ_1:42
.= (SDSub2INT (SD2SDSub (DecSD (x,(n + 1),k)))) /. ((n + 1) + 1) by A17, A20, Def11
.= (SDSub2INT (SD2SDSub (DecSD (x,(n + 1),k)))) . j by A20, A21, PARTFUN1:def_6 ;
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;
 Radix k > 0 by RADIX_2:6;
then  x mod ((Radix k) |^ n) < (Radix k) |^ n by NAT_D:1, PREPOWER:6;
then  x mod ((Radix k) |^ n) is_represented_by n,k by RADIX_1:def_12;
then A22: x mod ((Radix k) |^ n) = SDSub2IntOut (SD2SDSub (DecSD ((x mod ((Radix k) |^ n)),n,k))) by A4, A6
.= Sum (SDSub2INT (SD2SDSub (DecSD ((x mod ((Radix k) |^ 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 FINSEQ_2:sch_1();
A27: dom xpp = Seg n by A25, FINSEQ_1:def_3;
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 A10, FINSEQ_1:1;
now__::_thesis:_xp_._j_=_(xpp_^_<*(SDSub2INTDigit_((SD2SDSub_(DecSD_(x,(n_+_1),k))),(n_+_1),k))*>)_._j
percases ( j in Seg n or j = n + 1 ) by A29, FINSEQ_2:7;
supposeA30: 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 A25, FINSEQ_1:def_3;
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 A26, A27, A30
.= xp . j by A11, A12, A29 ;
hence  xp . j = (xpp ^ <*(SDSub2INTDigit ((SD2SDSub (DecSD (x,(n + 1),k))),(n + 1),k))*>) . j ; ::_thesis: verum
end;
supposeA31: 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 A25, FINSEQ_1:42
.= 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 ((Radix k) |^ 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 FINSEQ_2:sch_1();
A34: dom xnpp = Seg n by A32, FINSEQ_1:def_3;
 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 A32, FINSEQ_1:1;
then xpp . j = SDSub2INTDigit ((SD2SDSub (DecSD (x,(n + 1),k))),j,k) by A26, A27
.= SDSub2INTDigit ((SD2SDSub (DecSD ((x mod ((Radix k) |^ n)),n,k))),j,k) by A6, A35, Th20
.= xnpp . j by A33, A34, A35 ;
hence  xnpp . j = xpp . j ; ::_thesis: verum
end;
then A36: xpp = xnpp by A25, A32, FINSEQ_1:14;
A37: len (SDSub2INT (SD2SDSub (DecSD ((x mod ((Radix k) |^ 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 ((Radix k) |^ n)),n,k)))) holds
(SDSub2INT (SD2SDSub (DecSD ((x mod ((Radix k) |^ n)),n,k)))) . j = (xnpp ^ <*(SDSub2INTDigit ((SD2SDSub (DecSD ((x mod ((Radix k) |^ n)),n,k))),(n + 1),k))*>) . j
proof
let j be Nat; ::_thesis: ( 1 <= j & j <= len (SDSub2INT (SD2SDSub (DecSD ((x mod ((Radix k) |^ n)),n,k)))) implies (SDSub2INT (SD2SDSub (DecSD ((x mod ((Radix k) |^ n)),n,k)))) . j = (xnpp ^ <*(SDSub2INTDigit ((SD2SDSub (DecSD ((x mod ((Radix k) |^ n)),n,k))),(n + 1),k))*>) . j )
assume A39: ( 1 <= j & j <= len (SDSub2INT (SD2SDSub (DecSD ((x mod ((Radix k) |^ n)),n,k)))) ) ; ::_thesis: (SDSub2INT (SD2SDSub (DecSD ((x mod ((Radix k) |^ n)),n,k)))) . j = (xnpp ^ <*(SDSub2INTDigit ((SD2SDSub (DecSD ((x mod ((Radix k) |^ n)),n,k))),(n + 1),k))*>) . j
then A40: j in Seg (n + 1) by A37, FINSEQ_1:1;
A41: j in dom (SDSub2INT (SD2SDSub (DecSD ((x mod ((Radix k) |^ n)),n,k)))) by A39, FINSEQ_3:25;
now__::_thesis:_(SDSub2INT_(SD2SDSub_(DecSD_((x_mod_((Radix_k)_|^_n)),n,k))))_._j_=_(xnpp_^_<*(SDSub2INTDigit_((SD2SDSub_(DecSD_((x_mod_((Radix_k)_|^_n)),n,k))),(n_+_1),k))*>)_._j
percases ( j in Seg n or j = n + 1 ) by A40, FINSEQ_2:7;
supposeA42: j in Seg n ; ::_thesis: (SDSub2INT (SD2SDSub (DecSD ((x mod ((Radix k) |^ n)),n,k)))) . j = (xnpp ^ <*(SDSub2INTDigit ((SD2SDSub (DecSD ((x mod ((Radix k) |^ n)),n,k))),(n + 1),k))*>) . j
then  j in dom xnpp by A32, FINSEQ_1:def_3;
then (xnpp ^ <*(SDSub2INTDigit ((SD2SDSub (DecSD ((x mod ((Radix k) |^ n)),n,k))),(n + 1),k))*>) . j = xnpp . j by FINSEQ_1:def_7
.= SDSub2INTDigit ((SD2SDSub (DecSD ((x mod ((Radix k) |^ n)),n,k))),j,k) by A33, A34, A42
.= (SDSub2INT (SD2SDSub (DecSD ((x mod ((Radix k) |^ n)),n,k)))) /. j by A40, Def11
.= (SDSub2INT (SD2SDSub (DecSD ((x mod ((Radix k) |^ n)),n,k)))) . j by A41, PARTFUN1:def_6 ;
hence  (SDSub2INT (SD2SDSub (DecSD ((x mod ((Radix k) |^ n)),n,k)))) . j = (xnpp ^ <*(SDSub2INTDigit ((SD2SDSub (DecSD ((x mod ((Radix k) |^ n)),n,k))),(n + 1),k))*>) . j ; ::_thesis: verum
end;
supposeA43: j = n + 1 ; ::_thesis: (SDSub2INT (SD2SDSub (DecSD ((x mod ((Radix k) |^ n)),n,k)))) . j = (xnpp ^ <*(SDSub2INTDigit ((SD2SDSub (DecSD ((x mod ((Radix k) |^ n)),n,k))),(n + 1),k))*>) . j
A44: j in dom (SDSub2INT (SD2SDSub (DecSD ((x mod ((Radix k) |^ n)),n,k)))) by A37, A40, FINSEQ_1:def_3;
(xnpp ^ <*(SDSub2INTDigit ((SD2SDSub (DecSD ((x mod ((Radix k) |^ n)),n,k))),(n + 1),k))*>) . j = SDSub2INTDigit ((SD2SDSub (DecSD ((x mod ((Radix k) |^ n)),n,k))),(n + 1),k) by A32, A43, FINSEQ_1:42
.= (SDSub2INT (SD2SDSub (DecSD ((x mod ((Radix k) |^ n)),n,k)))) /. (n + 1) by A40, A43, Def11
.= (SDSub2INT (SD2SDSub (DecSD ((x mod ((Radix k) |^ n)),n,k)))) . j by A43, A44, PARTFUN1:def_6 ;
hence  (SDSub2INT (SD2SDSub (DecSD ((x mod ((Radix k) |^ n)),n,k)))) . j = (xnpp ^ <*(SDSub2INTDigit ((SD2SDSub (DecSD ((x mod ((Radix k) |^ n)),n,k))),(n + 1),k))*>) . j ; ::_thesis: verum
end;
end;
end;
hence  (SDSub2INT (SD2SDSub (DecSD ((x mod ((Radix k) |^ n)),n,k)))) . j = (xnpp ^ <*(SDSub2INTDigit ((SD2SDSub (DecSD ((x mod ((Radix k) |^ 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 A10, A25, FINSEQ_2:16;
then A45: xp = xpp ^ <*(SDSub2INTDigit ((SD2SDSub (DecSD (x,(n + 1),k))),(n + 1),k))*> by A28, FINSEQ_1:14;
 len (xp ^ <*(SDSub2INTDigit ((SD2SDSub (DecSD (x,(n + 1),k))),((n + 1) + 1),k))*>) = (n + 1) + 1 by A10, FINSEQ_2:16;
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 A14, FINSEQ_1:14;
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 A45, A36, RVSUM_1:74 ;
set RNDIG = ((Radix k) |^ n) * (DigA ((DecSD (x,(n + 1),k)),(n + 1)));
set RNSDC = ((Radix k) |^ n) * (SDSub_Add_Carry ((DigA ((DecSD (x,(n + 1),k)),n)),k));
A47: Radix k > 0 by RADIX_2:6;
 len (xnpp ^ <*(SDSub2INTDigit ((SD2SDSub (DecSD ((x mod ((Radix k) |^ n)),n,k))),(n + 1),k))*>) = n + 1 by A32, FINSEQ_2:16;
then  SDSub2INT (SD2SDSub (DecSD ((x mod ((Radix k) |^ n)),n,k))) = xnpp ^ <*(SDSub2INTDigit ((SD2SDSub (DecSD ((x mod ((Radix k) |^ n)),n,k))),(n + 1),k))*> by A37, A38, FINSEQ_1:14;
then A48: (x mod ((Radix k) |^ n)) + 0 = (Sum xnpp) + (SDSub2INTDigit ((SD2SDSub (DecSD ((x mod ((Radix k) |^ n)),n,k))),(n + 1),k)) by A22, RVSUM_1:74;
A49: SDSub2INTDigit ((SD2SDSub (DecSD (x,(n + 1),k))),(n + 1),k) = ((Radix k) |^ n) * (DigB_SDSub ((SD2SDSub (DecSD (x,(n + 1),k))),(n + 1))) by NAT_D:34
.= ((Radix k) |^ n) * (SD2SDSubDigitS ((DecSD (x,(n + 1),k)),(n + 1),k)) by A24, Def8
.= ((Radix k) |^ n) * (SD2SDSubDigit ((DecSD (x,(n + 1),k)),(n + 1),k)) by A6, A24, Def7
.= ((Radix k) |^ 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 A23, Def6
.= ((Radix k) |^ 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
.= ((((Radix k) |^ n) * (DigA ((DecSD (x,(n + 1),k)),(n + 1)))) - ((((Radix k) |^ n) * (Radix k)) * (SDSub_Add_Carry ((DigA ((DecSD (x,(n + 1),k)),(n + 1))),k)))) + (((Radix k) |^ n) * (SDSub_Add_Carry ((DigA ((DecSD (x,(n + 1),k)),n)),k)))
.= ((((Radix k) |^ n) * (DigA ((DecSD (x,(n + 1),k)),(n + 1)))) - (((Radix k) |^ (n + 1)) * (SDSub_Add_Carry ((DigA ((DecSD (x,(n + 1),k)),(n + 1))),k)))) + (((Radix k) |^ n) * (SDSub_Add_Carry ((DigA ((DecSD (x,(n + 1),k)),n)),k))) by NEWTON:6 ;
SDSub2INTDigit ((SD2SDSub (DecSD ((x mod ((Radix k) |^ n)),n,k))),(n + 1),k) = ((Radix k) |^ n) * (DigB_SDSub ((SD2SDSub (DecSD ((x mod ((Radix k) |^ n)),n,k))),(n + 1))) by NAT_D:34
.= ((Radix k) |^ n) * (SD2SDSubDigitS ((DecSD ((x mod ((Radix k) |^ n)),n,k)),(n + 1),k)) by A23, Def8
.= ((Radix k) |^ n) * (SD2SDSubDigit ((DecSD ((x mod ((Radix k) |^ n)),n,k)),(n + 1),k)) by A23, A6, Def7
.= ((Radix k) |^ n) * (SDSub_Add_Carry ((DigA ((DecSD ((x mod ((Radix k) |^ n)),n,k)),((n + 1) -' 1))),k)) by Def6
.= ((Radix k) |^ n) * (SDSub_Add_Carry ((DigA ((DecSD ((x mod ((Radix k) |^ n)),n,k)),n)),k)) by NAT_D:34
.= ((Radix k) |^ n) * (SDSub_Add_Carry ((DigA ((DecSD (x,(n + 1),k)),n)),k)) by A5, Lm5 ;
then  Sum (SDSub2INT (SD2SDSub (DecSD (x,(n + 1),k)))) = (((x mod ((Radix k) |^ n)) + (((Radix k) |^ n) * (DigA ((DecSD (x,(n + 1),k)),(n + 1))))) - (((Radix k) |^ n) * (SDSub_Add_Carry ((DigA ((DecSD (x,(n + 1),k)),n)),k)))) + (((Radix k) |^ n) * (SDSub_Add_Carry ((DigA ((DecSD (x,(n + 1),k)),n)),k))) by A46, A48, A49, A9
.= (x mod ((Radix k) |^ n)) + (((Radix k) |^ n) * (x div ((Radix k) |^ n))) by A7, RADIX_1:24 ;
hence  x = SDSub2IntOut (SD2SDSub (DecSD (x,(n + 1),k))) by A47, NAT_D:2, PREPOWER:6; ::_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 = (Radix k) * (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 A55, FINSEQ_1:def_3;
A58: 2 in Seg (1 + 1) by FINSEQ_1:1;
then A59: 2 in dom (SDSub2INT (SD2SDSub (DecSD (x,1,k)))) by A56, FINSEQ_1:def_3;
(SDSub2INT (SD2SDSub (DecSD (x,1,k)))) /. 2 = SDSub2INTDigit ((SD2SDSub (DecSD (x,1,k))),2,k) by A58, Def11
.= (Radix k) * (DigB_SDSub ((SD2SDSub (DecSD (x,1,k))),2)) by A52, NEWTON:5
.= (Radix k) * (SD2SDSubDigitS ((DecSD (x,1,k)),2,k)) by A58, Def8
.= (Radix k) * (SD2SDSubDigit ((DecSD (x,1,k)),2,k)) by A53, A58, Def7
.= (Radix k) * (SDSub_Add_Carry ((DigA ((DecSD (x,1,k)),1)),k)) by A52, A58, Def6 ;
then A60: (SDSub2INT (SD2SDSub (DecSD (x,1,k)))) . 2 = CRY by A59, PARTFUN1:def_6;
(SDSub2INT (SD2SDSub (DecSD (x,1,k)))) /. 1 = SDSub2INTDigit ((SD2SDSub (DecSD (x,1,k))),1,k) by A55, Def11
.= ((Radix k) |^ 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 A55, Def8
.= SD2SDSubDigit ((DecSD (x,1,k)),1,k) by A53, A55, Def7
.= (SDSub_Add_Data ((DigA ((DecSD (x,1,k)),1)),k)) + (SDSub_Add_Carry ((DigA ((DecSD (x,1,k)),(1 -' 1))),k)) by A51, Def6
.= (SDSub_Add_Data ((DigA ((DecSD (x,1,k)),1)),k)) + (SDSub_Add_Carry ((DigA ((DecSD (x,1,k)),0)),k)) by XREAL_1:232
.= (SDSub_Add_Data ((DigA ((DecSD (x,1,k)),1)),k)) + (SDSub_Add_Carry (0,k)) by RADIX_1:def_3
.= (SDSub_Add_Data ((DigA ((DecSD (x,1,k)),1)),k)) + 0 by Th16
.= (DigA ((DecSD (x,1,k)),1)) - ((Radix k) * (SDSub_Add_Carry ((DigA ((DecSD (x,1,k)),1)),k))) ;
then  (SDSub2INT (SD2SDSub (DecSD (x,1,k)))) . 1 = (DigA ((DecSD (x,1,k)),1)) - CRY by A57, PARTFUN1:def_6;
then  SDSub2INT (SD2SDSub (DecSD (x,1,k))) = <*DIG1,DIG2*> by A56, A60, FINSEQ_1:44;
then  Sum (SDSub2INT (SD2SDSub (DecSD (x,1,k)))) = DIG1 + DIG2 by RVSUM_1:77
.= x by A54, RADIX_1:21 ;
hence  x = SDSub2IntOut (SD2SDSub (DecSD (x,1,k))) ; ::_thesis: verum
end;
 for n being Nat st n >= 1 holds
S1[n] from NAT_1:sch_8(A50, A2);
hence  for k, x being Nat st k >= 2 & x is_represented_by n,k holds
x = SDSub2IntOut (SD2SDSub (DecSD (x,n,k))) by A1; ::_thesis: verum
end;