:: RADIX_3 semantic presentation  Show TPTP formulae Show IDV graph for whole article:: Showing IDV graph ... (Click the Palm Trees again to close it)

Lm1: for k being Nat st 1 <= k holds
Radix k = (Radix (k -' 1)) + (Radix (k -' 1))
proof end;

Lm2: for k being Nat st 1 <= k holds
(Radix k) - (Radix (k -' 1)) = Radix (k -' 1)
proof end;

Lm3: for k being Nat st 1 <= k holds
(- (Radix k)) + (Radix (k -' 1)) = - (Radix (k -' 1))
proof end;

Lm4: for k being Nat st 1 <= k holds
2 <= Radix k
proof 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 end;

definition
let k be Nat;
func k -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
;
;
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 ) } ;

definition
let k be Nat;
func k -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 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 :: RADIX_3:1  Show TPTP formulae Show IDV graph:: Showing IDV graph ... (Click the Palm Tree again to close it) Show TPTP problem
canceled;

theorem Th2: :: RADIX_3:2  Show TPTP formulae Show IDV graph:: Showing IDV graph ... (Click the Palm Tree again to close it) Show TPTP problem
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 end;

theorem Th3: :: RADIX_3:3  Show TPTP formulae Show IDV graph:: Showing IDV graph ... (Click the Palm Tree again to close it) Show TPTP problem
for k being Nat holds k -SD_Sub_S c= k -SD_Sub
proof end;

theorem Th4: :: RADIX_3:4  Show TPTP formulae Show IDV graph:: Showing IDV graph ... (Click the Palm Tree again to close it) Show TPTP problem
for k being Nat holds k -SD_Sub_S c= (k + 1) -SD_Sub_S
proof end;

theorem :: RADIX_3:5  Show TPTP formulae Show IDV graph:: Showing IDV graph ... (Click the Palm Tree again to close it) Show TPTP problem
for k being Nat st 2 <= k holds
k -SD_Sub c= k -SD
proof end;

theorem Th6: :: RADIX_3:6  Show TPTP formulae Show IDV graph:: Showing IDV graph ... (Click the Palm Tree again to close it) Show TPTP problem
0 in 0 -SD_Sub_S
proof end;

theorem Th7: :: RADIX_3:7  Show TPTP formulae Show IDV graph:: Showing IDV graph ... (Click the Palm Tree again to close it) Show TPTP problem
for k being Nat holds 0 in k -SD_Sub_S
proof end;

theorem Th8: :: RADIX_3:8  Show TPTP formulae Show IDV graph:: Showing IDV graph ... (Click the Palm Tree again to close it) Show TPTP problem
for k being Nat holds 0 in k -SD_Sub
proof end;

theorem Th9: :: RADIX_3:9  Show TPTP formulae Show IDV graph:: Showing IDV graph ... (Click the Palm Tree again to close it) Show TPTP problem
for k being Nat
for e being set st e in k -SD_Sub holds
e is Integer
proof end;

theorem Th10: :: RADIX_3:10  Show TPTP formulae Show IDV graph:: Showing IDV graph ... (Click the Palm Tree again to close it) Show TPTP problem
for k being Nat holds k -SD_Sub c= INT
proof end;

theorem Th11: :: RADIX_3:11  Show TPTP formulae Show IDV graph:: Showing IDV graph ... (Click the Palm Tree again to close it) Show TPTP problem
for k being Nat holds k -SD_Sub_S c= INT
proof end;

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

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

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

theorem Th12: :: RADIX_3:12  Show TPTP formulae Show IDV graph:: Showing IDV graph ... (Click the Palm Tree again to close it) Show TPTP problem
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 end;

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 Th13: :: RADIX_3:13  Show TPTP formulae Show IDV graph:: Showing IDV graph ... (Click the Palm Tree again to close it) Show TPTP problem
for x being Integer
for k being Nat st 2 <= k holds
( - 1 <= SDSub_Add_Carry x,k & SDSub_Add_Carry x,k <= 1 )
proof end;

theorem Th14: :: RADIX_3:14  Show TPTP formulae Show IDV graph:: Showing IDV graph ... (Click the Palm Tree again to close it) Show TPTP problem
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 end;

theorem Th15: :: RADIX_3:15  Show TPTP formulae Show IDV graph:: Showing IDV graph ... (Click the Palm Tree again to close it) Show TPTP problem
for x being Integer
for k being Nat st 2 <= k holds
SDSub_Add_Carry x,k in k -SD_Sub_S
proof end;

theorem Th16: :: RADIX_3:16  Show TPTP formulae Show IDV graph:: Showing IDV graph ... (Click the Palm Tree again to close it) Show TPTP problem
for k being Nat
for i1, i2 being Integer st 2 <= k & i1 in k -SD & i2 in k -SD holds
(SDSub_Add_Data i1,k) + (SDSub_Add_Carry i2,k) in k -SD_Sub
proof end;

theorem Th17: :: RADIX_3:17  Show TPTP formulae Show IDV graph:: Showing IDV graph ... (Click the Palm Tree again to close it) Show TPTP problem
for k being Nat st 2 <= k holds
SDSub_Add_Carry 0,k = 0
proof end;

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 ) )
proof end;
consistency
for b1 being Integer st i in Seg n & i = 0 holds
( b1 = x . i iff b1 = 0 )
by FINSEQ_1:3;
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 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 Th18: :: RADIX_3:18  Show TPTP formulae Show IDV graph:: Showing IDV graph ... (Click the Palm Tree again to close it) Show TPTP problem
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 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, 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: :: 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 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 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:19  Show TPTP formulae Show IDV graph:: Showing IDV graph ... (Click the Palm Tree again to close it) Show TPTP problem
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 end;

theorem :: RADIX_3:20  Show TPTP formulae Show IDV graph:: Showing IDV graph ... (Click the Palm Tree again to close it) Show TPTP problem
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 end;

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 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 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 Th21: :: RADIX_3:21  Show TPTP formulae Show IDV graph:: Showing IDV graph ... (Click the Palm Tree again to close it) Show TPTP problem
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 end;

theorem :: RADIX_3:22  Show TPTP formulae Show IDV graph:: Showing IDV graph ... (Click the Palm Tree again to close it) Show TPTP problem
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 end;