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

theorem Th1: :: RADIX_4:1  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
2 < Radix k
proof end;

Lm1: for k being Nat
for i1 being Integer st i1 in k -SD_Sub_S holds
( i1 >= - (Radix (k -' 1)) & i1 <= (Radix (k -' 1)) - 1 )
proof end;

Lm2: for n, m, k, i being Nat st i in Seg n holds
DigA (DecSD m,(n + 1),k),i = DigA (DecSD m,n,k),i
proof end;

Lm3: for k, x, n being Nat st n >= 1 & x is_represented_by n + 1,k holds
DigA (DecSD (x mod ((Radix k) |^ n)),n,k),n = DigA (DecSD x,n,k),n
proof end;

theorem Th2: :: RADIX_4:2  Show TPTP formulae Show IDV graph:: Showing IDV graph ... (Click the Palm Tree again to close it) Show TPTP problem
for x, y being Integer
for k being Nat st 3 <= k holds
SDSub_Add_Carry ((SDSub_Add_Carry x,k) + (SDSub_Add_Carry y,k)),k = 0
proof end;

theorem Th3: :: RADIX_4:3  Show TPTP formulae Show IDV graph:: Showing IDV graph ... (Click the Palm Tree again to close it) Show TPTP problem
for k, m, n being Nat st 2 <= k holds
DigA_SDSub (SD2SDSub (DecSD m,n,k)),(n + 1) = SDSub_Add_Carry (DigA (DecSD m,n,k),n),k
proof end;

theorem Th4: :: RADIX_4:4  Show TPTP formulae Show IDV graph:: Showing IDV graph ... (Click the Palm Tree again to close it) Show TPTP problem
for k, m being Nat st 2 <= k & m is_represented_by 1,k holds
DigA_SDSub (SD2SDSub (DecSD m,1,k)),(1 + 1) = SDSub_Add_Carry m,k
proof end;

theorem Th5: :: RADIX_4:5  Show TPTP formulae Show IDV graph:: Showing IDV graph ... (Click the Palm Tree again to close it) Show TPTP problem
for k, x, n being Nat st n >= 1 & k >= 3 & x is_represented_by n + 1,k holds
DigA_SDSub (SD2SDSub (DecSD (x mod ((Radix k) |^ n)),n,k)),(n + 1) = SDSub_Add_Carry (DigA (DecSD x,n,k),n),k
proof end;

theorem Th6: :: RADIX_4:6  Show TPTP formulae Show IDV graph:: Showing IDV graph ... (Click the Palm Tree again to close it) Show TPTP problem
for k, m being Nat st 2 <= k & m is_represented_by 1,k holds
DigA_SDSub (SD2SDSub (DecSD m,1,k)),1 = m - ((SDSub_Add_Carry m,k) * (Radix k))
proof end;

theorem Th7: :: RADIX_4:7  Show TPTP formulae Show IDV graph:: Showing IDV graph ... (Click the Palm Tree again to close it) Show TPTP problem
for k, x, n being Nat st n >= 1 & k >= 2 & x is_represented_by n + 1,k holds
((Radix k) |^ n) * (DigA_SDSub (SD2SDSub (DecSD x,(n + 1),k)),(n + 1)) = ((((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))
proof end;

definition
let i, n, k be Nat;
let x, y be Tuple of n,(k -SD_Sub );
assume A1: ( i in Seg n & k >= 2 ) ;
func SDSubAddDigit x,y,i,k -> Element of k -SD_Sub equals :Def1: :: RADIX_4:def 1
(SDSub_Add_Data ((DigA_SDSub x,i) + (DigA_SDSub y,i)),k) + (SDSub_Add_Carry ((DigA_SDSub x,(i -' 1)) + (DigA_SDSub y,(i -' 1))),k);
coherence
(SDSub_Add_Data ((DigA_SDSub x,i) + (DigA_SDSub y,i)),k) + (SDSub_Add_Carry ((DigA_SDSub x,(i -' 1)) + (DigA_SDSub y,(i -' 1))),k) is Element of k -SD_Sub
proof end;
end;

:: deftheorem Def1 defines SDSubAddDigit RADIX_4:def 1 :
for i, n, k being Nat
for x, y being Tuple of n,(k -SD_Sub ) st i in Seg n & k >= 2 holds
SDSubAddDigit x,y,i,k = (SDSub_Add_Data ((DigA_SDSub x,i) + (DigA_SDSub y,i)),k) + (SDSub_Add_Carry ((DigA_SDSub x,(i -' 1)) + (DigA_SDSub y,(i -' 1))),k);

definition
let n, k be Nat;
let x, y be Tuple of n,(k -SD_Sub );
func x '+' y -> Tuple of n,(k -SD_Sub ) means :Def2: :: RADIX_4:def 2
for i being Nat st i in Seg n holds
DigA_SDSub it,i = SDSubAddDigit x,y,i,k;
existence
ex b1 being Tuple of n,(k -SD_Sub ) st
for i being Nat st i in Seg n holds
DigA_SDSub b1,i = SDSubAddDigit x,y,i,k
proof end;
uniqueness
for b1, b2 being Tuple of n,(k -SD_Sub ) st ( for i being Nat st i in Seg n holds
DigA_SDSub b1,i = SDSubAddDigit x,y,i,k ) & ( for i being Nat st i in Seg n holds
DigA_SDSub b2,i = SDSubAddDigit x,y,i,k ) holds
b1 = b2
proof end;
end;

:: deftheorem Def2 defines '+' RADIX_4:def 2 :
for n, k being Nat
for x, y, b5 being Tuple of n,(k -SD_Sub ) holds
( b5 = x '+' y iff for i being Nat st i in Seg n holds
DigA_SDSub b5,i = SDSubAddDigit x,y,i,k );

theorem Th8: :: RADIX_4:8  Show TPTP formulae Show IDV graph:: Showing IDV graph ... (Click the Palm Tree again to close it) Show TPTP problem
for n, k, x, y, i being Nat st i in Seg n & 2 <= k holds
SDSubAddDigit (SD2SDSub (DecSD x,(n + 1),k)),(SD2SDSub (DecSD y,(n + 1),k)),i,k = SDSubAddDigit (SD2SDSub (DecSD (x mod ((Radix k) |^ n)),n,k)),(SD2SDSub (DecSD (y mod ((Radix k) |^ n)),n,k)),i,k
proof end;

theorem :: RADIX_4:9  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, y being Nat st k >= 3 & x is_represented_by n,k & y is_represented_by n,k holds
x + y = SDSub2IntOut ((SD2SDSub (DecSD x,n,k)) '+' (SD2SDSub (DecSD y,n,k)))
proof end;