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 :
:: deftheorem defines -SD_Sub RADIX_3:def 2 :
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 :
:: deftheorem defines SDSub_Add_Data RADIX_3:def 4 :
theorem Th13:
theorem Th14:
theorem Th15:
theorem Th16:
theorem Th17:
begin
:: deftheorem Def5 defines DigA_SDSub RADIX_3:def 5 :
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 :
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 :
theorem
theorem
begin
:: deftheorem defines DigB_SDSub RADIX_3:def 9 :
:: deftheorem defines SDSub2INTDigit RADIX_3:def 10 :
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 :
:: deftheorem defines SDSub2IntOut RADIX_3:def 12 :
theorem Th21:
theorem