begin
Lm1:
for k being Nat st 1 <= k holds
Radix k = (Radix (k -' 1)) + (Radix (k -' 1))
Lm2:
for k being Nat st 1 <= k holds
(Radix k) - (Radix (k -' 1)) = Radix (k -' 1)
Lm3:
for k being Nat st 1 <= k holds
(- (Radix k)) + (Radix (k -' 1)) = - (Radix (k -' 1))
Lm4:
for k being Nat st 1 <= k holds
2 <= Radix k
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)
:: 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
canceled;
theorem Th2:
theorem Th3:
theorem Th4:
theorem
theorem Th6:
theorem Th7:
theorem Th8:
theorem Th9:
theorem Th10:
theorem Th11:
theorem Th12:
begin
:: 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 ) );
:: 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 Th13:
theorem Th14:
theorem Th15:
theorem Th16:
theorem Th17:
begin
:: 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:
(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) )
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 Th18:
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:
SD2SDSubDigit (
x,
i,
k);
coherence
SD2SDSubDigit (x,i,k) is Element of k -SD_Sub
by A1, Th18;
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:
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)
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
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
theorem
begin
:: 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);
:: 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:
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)
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
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) );
:: 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 Th21:
theorem