:: RADIX_5 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_5: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 k >= 2 holds
(Radix k) - 1 in k -SD
proof end;

theorem Th2: :: RADIX_5:2  Show TPTP formulae Show IDV graph:: Showing IDV graph ... (Click the Palm Tree again to close it) Show TPTP problem
for i, n being Nat st i > 1 & i in Seg n holds
i -' 1 in Seg n
proof end;

theorem Th3: :: RADIX_5: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 st 2 <= k holds
4 <= Radix k
proof end;

theorem Th4: :: RADIX_5: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
for tx being Tuple of 1,(k -SD ) holds SDDec tx = DigA tx,1
proof end;

theorem Th5: :: RADIX_5:5  Show TPTP formulae Show IDV graph:: Showing IDV graph ... (Click the Palm Tree again to close it) Show TPTP problem
for i, k, n being Nat st i in Seg n holds
DigA (DecSD 0,n,k),i = 0
proof end;

theorem :: RADIX_5:6  Show TPTP formulae Show IDV graph:: Showing IDV graph ... (Click the Palm Tree again to close it) Show TPTP problem
for n, k being Nat st n >= 1 holds
SDDec (DecSD 0,n,k) = 0
proof end;

theorem Th7: :: RADIX_5:7  Show TPTP formulae Show IDV graph:: Showing IDV graph ... (Click the Palm Tree again to close it) Show TPTP problem
for k, n being Nat st 1 in Seg n & k >= 2 holds
DigA (DecSD 1,n,k),1 = 1
proof end;

theorem Th8: :: RADIX_5:8  Show TPTP formulae Show IDV graph:: Showing IDV graph ... (Click the Palm Tree again to close it) Show TPTP problem
for i, k, n being Nat st i in Seg n & i > 1 & k >= 2 holds
DigA (DecSD 1,n,k),i = 0
proof end;

theorem :: RADIX_5:9  Show TPTP formulae Show IDV graph:: Showing IDV graph ... (Click the Palm Tree again to close it) Show TPTP problem
for n, k being Nat st n >= 1 & k >= 2 holds
SDDec (DecSD 1,n,k) = 1
proof end;

theorem Th10: :: RADIX_5: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 st k >= 2 holds
SD_Add_Carry (Radix k) = 1
proof end;

theorem Th11: :: RADIX_5: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 st k >= 2 holds
SD_Add_Data (Radix k),k = 0
proof end;

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

Lm2: for n, k, i being Nat st k >= 2 & i in Seg n holds
SD_Add_Carry (DigA (DecSD 1,n,k),i) = 0
proof end;

theorem Th12: :: RADIX_5:12  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 being Nat
for tx, ty being Tuple of n,(k -SD ) st ( for i being Nat st i in Seg n holds
DigA tx,i = DigA ty,i ) holds
SDDec tx = SDDec ty
proof end;

theorem :: RADIX_5:13  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 being Nat
for tx, ty being Tuple of n,(k -SD ) st ( for i being Nat st i in Seg n holds
DigA tx,i >= DigA ty,i ) holds
SDDec tx >= SDDec ty
proof end;

theorem Th14: :: RADIX_5:14  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 being Nat st k >= 2 holds
for tx, ty, tz, tw being Tuple of n,(k -SD ) st ( for i being Nat holds
( not i in Seg n or ( DigA tx,i = DigA tz,i & DigA ty,i = DigA tw,i ) or ( DigA ty,i = DigA tz,i & DigA tx,i = DigA tw,i ) ) ) holds
(SDDec tz) + (SDDec tw) = (SDDec tx) + (SDDec ty)
proof end;

theorem :: RADIX_5:15  Show TPTP formulae Show IDV graph:: Showing IDV graph ... (Click the Palm Tree again to close it) Show TPTP problem
for n, k being Nat st n >= 1 & k >= 2 holds
for tx, ty, tz being Tuple of n,(k -SD ) st ( for i being Nat holds
( not i in Seg n or ( DigA tx,i = DigA tz,i & DigA ty,i = 0 ) or ( DigA ty,i = DigA tz,i & DigA tx,i = 0 ) ) ) holds
(SDDec tz) + (SDDec (DecSD 0,n,k)) = (SDDec tx) + (SDDec ty)
proof end;

definition
let i, m, k be Nat;
assume A1: k >= 2 ;
func SDMinDigit m,k,i -> Element of k -SD equals :Def1: :: RADIX_5:def 1
(- (Radix k)) + 1 if ( 1 <= i & i < m )
otherwise 0;
coherence
( ( 1 <= i & i < m implies (- (Radix k)) + 1 is Element of k -SD ) & ( ( not 1 <= i or not i < m ) implies 0 is Element of k -SD ) )
proof end;
consistency
for b1 being Element of k -SD holds verum ;
end;

:: deftheorem Def1 defines SDMinDigit RADIX_5:def 1 :
for i, m, k being Nat st k >= 2 holds
( ( 1 <= i & i < m implies SDMinDigit m,k,i = (- (Radix k)) + 1 ) & ( ( not 1 <= i or not i < m ) implies SDMinDigit m,k,i = 0 ) );

definition
let n, m, k be Nat;
func SDMin n,m,k -> Tuple of n,(k -SD ) means :Def2: :: RADIX_5:def 2
for i being Nat st i in Seg n holds
DigA it,i = SDMinDigit m,k,i;
existence
ex b1 being Tuple of n,(k -SD ) st
for i being Nat st i in Seg n holds
DigA b1,i = SDMinDigit m,k,i
proof end;
uniqueness
for b1, b2 being Tuple of n,(k -SD ) st ( for i being Nat st i in Seg n holds
DigA b1,i = SDMinDigit m,k,i ) & ( for i being Nat st i in Seg n holds
DigA b2,i = SDMinDigit m,k,i ) holds
b1 = b2
proof end;
end;

:: deftheorem Def2 defines SDMin RADIX_5:def 2 :
for n, m, k being Nat
for b4 being Tuple of n,(k -SD ) holds
( b4 = SDMin n,m,k iff for i being Nat st i in Seg n holds
DigA b4,i = SDMinDigit m,k,i );

definition
let i, m, k be Nat;
assume A1: k >= 2 ;
func SDMaxDigit m,k,i -> Element of k -SD equals :Def3: :: RADIX_5:def 3
(Radix k) - 1 if ( 1 <= i & i < m )
otherwise 0;
coherence
( ( 1 <= i & i < m implies (Radix k) - 1 is Element of k -SD ) & ( ( not 1 <= i or not i < m ) implies 0 is Element of k -SD ) ) by A1, Th1, RADIX_1:16;
consistency
for b1 being Element of k -SD holds verum ;
end;

:: deftheorem Def3 defines SDMaxDigit RADIX_5:def 3 :
for i, m, k being Nat st k >= 2 holds
( ( 1 <= i & i < m implies SDMaxDigit m,k,i = (Radix k) - 1 ) & ( ( not 1 <= i or not i < m ) implies SDMaxDigit m,k,i = 0 ) );

definition
let n, m, k be Nat;
func SDMax n,m,k -> Tuple of n,(k -SD ) means :Def4: :: RADIX_5:def 4
for i being Nat st i in Seg n holds
DigA it,i = SDMaxDigit m,k,i;
existence
ex b1 being Tuple of n,(k -SD ) st
for i being Nat st i in Seg n holds
DigA b1,i = SDMaxDigit m,k,i
proof end;
uniqueness
for b1, b2 being Tuple of n,(k -SD ) st ( for i being Nat st i in Seg n holds
DigA b1,i = SDMaxDigit m,k,i ) & ( for i being Nat st i in Seg n holds
DigA b2,i = SDMaxDigit m,k,i ) holds
b1 = b2
proof end;
end;

:: deftheorem Def4 defines SDMax RADIX_5:def 4 :
for n, m, k being Nat
for b4 being Tuple of n,(k -SD ) holds
( b4 = SDMax n,m,k iff for i being Nat st i in Seg n holds
DigA b4,i = SDMaxDigit m,k,i );

definition
let i, m, k be Nat;
assume A1: k >= 2 ;
func FminDigit m,k,i -> Element of k -SD equals :Def5: :: RADIX_5:def 5
1 if i = m
otherwise 0;
coherence
( ( i = m implies 1 is Element of k -SD ) & ( not i = m implies 0 is Element of k -SD ) )
proof end;
consistency
for b1 being Element of k -SD holds verum ;
end;

:: deftheorem Def5 defines FminDigit RADIX_5:def 5 :
for i, m, k being Nat st k >= 2 holds
( ( i = m implies FminDigit m,k,i = 1 ) & ( not i = m implies FminDigit m,k,i = 0 ) );

definition
let n, m, k be Nat;
func Fmin n,m,k -> Tuple of n,(k -SD ) means :Def6: :: RADIX_5:def 6
for i being Nat st i in Seg n holds
DigA it,i = FminDigit m,k,i;
existence
ex b1 being Tuple of n,(k -SD ) st
for i being Nat st i in Seg n holds
DigA b1,i = FminDigit m,k,i
proof end;
uniqueness
for b1, b2 being Tuple of n,(k -SD ) st ( for i being Nat st i in Seg n holds
DigA b1,i = FminDigit m,k,i ) & ( for i being Nat st i in Seg n holds
DigA b2,i = FminDigit m,k,i ) holds
b1 = b2
proof end;
end;

:: deftheorem Def6 defines Fmin RADIX_5:def 6 :
for n, m, k being Nat
for b4 being Tuple of n,(k -SD ) holds
( b4 = Fmin n,m,k iff for i being Nat st i in Seg n holds
DigA b4,i = FminDigit m,k,i );

definition
let i, m, k be Nat;
assume A1: k >= 2 ;
func FmaxDigit m,k,i -> Element of k -SD equals :Def7: :: RADIX_5:def 7
(Radix k) - 1 if i = m
otherwise 0;
coherence
( ( i = m implies (Radix k) - 1 is Element of k -SD ) & ( not i = m implies 0 is Element of k -SD ) ) by A1, Th1, RADIX_1:16;
consistency
for b1 being Element of k -SD holds verum ;
end;

:: deftheorem Def7 defines FmaxDigit RADIX_5:def 7 :
for i, m, k being Nat st k >= 2 holds
( ( i = m implies FmaxDigit m,k,i = (Radix k) - 1 ) & ( not i = m implies FmaxDigit m,k,i = 0 ) );

definition
let n, m, k be Nat;
func Fmax n,m,k -> Tuple of n,(k -SD ) means :Def8: :: RADIX_5:def 8
for i being Nat st i in Seg n holds
DigA it,i = FmaxDigit m,k,i;
existence
ex b1 being Tuple of n,(k -SD ) st
for i being Nat st i in Seg n holds
DigA b1,i = FmaxDigit m,k,i
proof end;
uniqueness
for b1, b2 being Tuple of n,(k -SD ) st ( for i being Nat st i in Seg n holds
DigA b1,i = FmaxDigit m,k,i ) & ( for i being Nat st i in Seg n holds
DigA b2,i = FmaxDigit m,k,i ) holds
b1 = b2
proof end;
end;

:: deftheorem Def8 defines Fmax RADIX_5:def 8 :
for n, m, k being Nat
for b4 being Tuple of n,(k -SD ) holds
( b4 = Fmax n,m,k iff for i being Nat st i in Seg n holds
DigA b4,i = FmaxDigit m,k,i );

theorem Th16: :: RADIX_5:16  Show TPTP formulae Show IDV graph:: Showing IDV graph ... (Click the Palm Tree again to close it) Show TPTP problem
for n, m, k being Nat st n >= 1 & k >= 2 & m in Seg n holds
for i being Nat st i in Seg n holds
(DigA (SDMax n,m,k),i) + (DigA (SDMin n,m,k),i) = 0
proof end;

theorem :: RADIX_5:17  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 m, k being Nat st m in Seg n & k >= 2 holds
(SDDec (SDMax n,m,k)) + (SDDec (SDMin n,m,k)) = SDDec (DecSD 0,n,k)
proof end;

theorem :: RADIX_5:18  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 m, k being Nat st m in Seg n & k >= 2 holds
SDDec (Fmin n,m,k) = (SDDec (SDMax n,m,k)) + (SDDec (DecSD 1,n,k))
proof end;

theorem :: RADIX_5:19  Show TPTP formulae Show IDV graph:: Showing IDV graph ... (Click the Palm Tree again to close it) Show TPTP problem
for n, m, k being Nat st m in Seg n & k >= 2 holds
SDDec (Fmin (n + 1),(m + 1),k) = (SDDec (Fmin (n + 1),m,k)) + (SDDec (Fmax (n + 1),m,k))
proof end;