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

Lm1: for m being Nat st m >= 1 holds
m + 2 > 1
proof end;

theorem Th1: :: RADIX_6:1  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 >= 1 & k >= 2 holds
SDDec (Fmin (m + n),m,k) = SDDec (Fmin m,m,k)
proof end;

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

definition
let i, m, k be Nat;
let r be Tuple of (m + 2),(k -SD );
assume A1: i in Seg (m + 2) ;
func M0Digit r,i -> Element of k -SD equals :Def1: :: RADIX_6:def 1
r . i if i >= m
0 if i < m
;
coherence
( ( i >= m implies r . i is Element of k -SD ) & ( i < m implies 0 is Element of k -SD ) )
proof end;
consistency
for b1 being Element of k -SD st i >= m & i < m holds
( b1 = r . i iff b1 = 0 ) ;
end;

:: deftheorem Def1 defines M0Digit RADIX_6:def 1 :
for i, m, k being Nat
for r being Tuple of (m + 2),(k -SD ) st i in Seg (m + 2) holds
( ( i >= m implies M0Digit r,i = r . i ) & ( i < m implies M0Digit r,i = 0 ) );

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

:: deftheorem Def2 defines M0 RADIX_6:def 2 :
for m, k being Nat
for r, b4 being Tuple of (m + 2),(k -SD ) holds
( b4 = M0 r iff for i being Nat st i in Seg (m + 2) holds
DigA b4,i = M0Digit r,i );

definition
let i, m, k be Nat;
let r be Tuple of (m + 2),(k -SD );
assume that
A1: k >= 2 and
A2: i in Seg (m + 2) ;
func MmaxDigit r,i -> Element of k -SD equals :Def3: :: RADIX_6:def 3
r . i if i >= m
(Radix k) - 1 if i < m
;
coherence
( ( i >= m implies r . i is Element of k -SD ) & ( i < m implies (Radix k) - 1 is Element of k -SD ) )
proof end;
consistency
for b1 being Element of k -SD st i >= m & i < m holds
( b1 = r . i iff b1 = (Radix k) - 1 ) ;
end;

:: deftheorem Def3 defines MmaxDigit RADIX_6:def 3 :
for i, m, k being Nat
for r being Tuple of (m + 2),(k -SD ) st k >= 2 & i in Seg (m + 2) holds
( ( i >= m implies MmaxDigit r,i = r . i ) & ( i < m implies MmaxDigit r,i = (Radix k) - 1 ) );

definition
let m, k be Nat;
let r be Tuple of (m + 2),(k -SD );
func Mmax r -> Tuple of (m + 2),(k -SD ) means :Def4: :: RADIX_6:def 4
for i being Nat st i in Seg (m + 2) holds
DigA it,i = MmaxDigit r,i;
existence
ex b1 being Tuple of (m + 2),(k -SD ) st
for i being Nat st i in Seg (m + 2) holds
DigA b1,i = MmaxDigit r,i
proof end;
uniqueness
for b1, b2 being Tuple of (m + 2),(k -SD ) st ( for i being Nat st i in Seg (m + 2) holds
DigA b1,i = MmaxDigit r,i ) & ( for i being Nat st i in Seg (m + 2) holds
DigA b2,i = MmaxDigit r,i ) holds
b1 = b2
proof end;
end;

:: deftheorem Def4 defines Mmax RADIX_6:def 4 :
for m, k being Nat
for r, b4 being Tuple of (m + 2),(k -SD ) holds
( b4 = Mmax r iff for i being Nat st i in Seg (m + 2) holds
DigA b4,i = MmaxDigit r,i );

definition
let i, m, k be Nat;
let r be Tuple of (m + 2),(k -SD );
assume that
A1: k >= 2 and
A2: i in Seg (m + 2) ;
func MminDigit r,i -> Element of k -SD equals :Def5: :: RADIX_6:def 5
r . i if i >= m
(- (Radix k)) + 1 if i < m
;
coherence
( ( i >= m implies r . i is Element of k -SD ) & ( i < m implies (- (Radix k)) + 1 is Element of k -SD ) )
proof end;
consistency
for b1 being Element of k -SD st i >= m & i < m holds
( b1 = r . i iff b1 = (- (Radix k)) + 1 ) ;
end;

:: deftheorem Def5 defines MminDigit RADIX_6:def 5 :
for i, m, k being Nat
for r being Tuple of (m + 2),(k -SD ) st k >= 2 & i in Seg (m + 2) holds
( ( i >= m implies MminDigit r,i = r . i ) & ( i < m implies MminDigit r,i = (- (Radix k)) + 1 ) );

definition
let m, k be Nat;
let r be Tuple of (m + 2),(k -SD );
func Mmin r -> Tuple of (m + 2),(k -SD ) means :Def6: :: RADIX_6:def 6
for i being Nat st i in Seg (m + 2) holds
DigA it,i = MminDigit r,i;
existence
ex b1 being Tuple of (m + 2),(k -SD ) st
for i being Nat st i in Seg (m + 2) holds
DigA b1,i = MminDigit r,i
proof end;
uniqueness
for b1, b2 being Tuple of (m + 2),(k -SD ) st ( for i being Nat st i in Seg (m + 2) holds
DigA b1,i = MminDigit r,i ) & ( for i being Nat st i in Seg (m + 2) holds
DigA b2,i = MminDigit r,i ) holds
b1 = b2
proof end;
end;

:: deftheorem Def6 defines Mmin RADIX_6:def 6 :
for m, k being Nat
for r, b4 being Tuple of (m + 2),(k -SD ) holds
( b4 = Mmin r iff for i being Nat st i in Seg (m + 2) holds
DigA b4,i = MminDigit r,i );

theorem Th3: :: RADIX_6:3  Show TPTP formulae Show IDV graph:: Showing IDV graph ... (Click the Palm Tree again to close it) Show TPTP problem
for m, k being Nat st m >= 1 & k >= 2 holds
for r being Tuple of (m + 2),(k -SD ) holds SDDec (Mmax r) >= SDDec r
proof end;

theorem Th4: :: RADIX_6:4  Show TPTP formulae Show IDV graph:: Showing IDV graph ... (Click the Palm Tree again to close it) Show TPTP problem
for m, k being Nat st m >= 1 & k >= 2 holds
for r being Tuple of (m + 2),(k -SD ) holds SDDec r >= SDDec (Mmin r)
proof end;

definition
let n, k be Nat;
let x be Integer;
pred x needs_digits_of n,k means :Def7: :: RADIX_6:def 7
( x < (Radix k) |^ n & x >= (Radix k) |^ (n -' 1) );
end;

:: deftheorem Def7 defines needs_digits_of RADIX_6:def 7 :
for n, k being Nat
for x being Integer holds
( x needs_digits_of n,k iff ( x < (Radix k) |^ n & x >= (Radix k) |^ (n -' 1) ) );

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

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

theorem Th7: :: RADIX_6:7  Show TPTP formulae Show IDV graph:: Showing IDV graph ... (Click the Palm Tree again to close it) Show TPTP problem
for f, m, k being Nat st m >= 1 & k >= 2 & f needs_digits_of m,k holds
f >= SDDec (Fmin (m + 2),m,k)
proof end;

theorem Th8: :: RADIX_6:8  Show TPTP formulae Show IDV graph:: Showing IDV graph ... (Click the Palm Tree again to close it) Show TPTP problem
for mlow, mhigh, f being Integer st mhigh < mlow + f & f > 0 holds
ex s being Integer st
( - f < mlow - (s * f) & mhigh - (s * f) < f )
proof end;

theorem Th9: :: RADIX_6:9  Show TPTP formulae Show IDV graph:: Showing IDV graph ... (Click the Palm Tree again to close it) Show TPTP problem
for m, k being Nat st m >= 1 & k >= 2 holds
for r being Tuple of (m + 2),(k -SD ) holds (SDDec (Mmax r)) + (SDDec (DecSD 0,(m + 2),k)) = (SDDec (M0 r)) + (SDDec (SDMax (m + 2),m,k))
proof end;

theorem Th10: :: RADIX_6:10  Show TPTP formulae Show IDV graph:: Showing IDV graph ... (Click the Palm Tree again to close it) Show TPTP problem
for m, k being Nat st m >= 1 & k >= 2 holds
for r being Tuple of (m + 2),(k -SD ) holds SDDec (Mmax r) < (SDDec (M0 r)) + (SDDec (Fmin (m + 2),m,k))
proof end;

theorem Th11: :: RADIX_6:11  Show TPTP formulae Show IDV graph:: Showing IDV graph ... (Click the Palm Tree again to close it) Show TPTP problem
for m, k being Nat st m >= 1 & k >= 2 holds
for r being Tuple of (m + 2),(k -SD ) holds (SDDec (Mmin r)) + (SDDec (DecSD 0,(m + 2),k)) = (SDDec (M0 r)) + (SDDec (SDMin (m + 2),m,k))
proof end;

theorem Th12: :: RADIX_6:12  Show TPTP formulae Show IDV graph:: Showing IDV graph ... (Click the Palm Tree again to close it) Show TPTP problem
for m, k being Nat
for r being Tuple of (m + 2),(k -SD ) st m >= 1 & k >= 2 holds
(SDDec (M0 r)) + (SDDec (DecSD 0,(m + 2),k)) = (SDDec (Mmin r)) + (SDDec (SDMax (m + 2),m,k))
proof end;

theorem Th13: :: RADIX_6:13  Show TPTP formulae Show IDV graph:: Showing IDV graph ... (Click the Palm Tree again to close it) Show TPTP problem
for m, k being Nat st m >= 1 & k >= 2 holds
for r being Tuple of (m + 2),(k -SD ) holds SDDec (M0 r) < (SDDec (Mmin r)) + (SDDec (Fmin (m + 2),m,k))
proof end;

theorem :: RADIX_6:14  Show TPTP formulae Show IDV graph:: Showing IDV graph ... (Click the Palm Tree again to close it) Show TPTP problem
for m, k, f being Nat
for r being Tuple of (m + 2),(k -SD ) st m >= 1 & k >= 2 & f needs_digits_of m,k holds
ex s being Integer st
( - f < (SDDec (M0 r)) - (s * f) & (SDDec (Mmax r)) - (s * f) < f )
proof end;

theorem :: RADIX_6:15  Show TPTP formulae Show IDV graph:: Showing IDV graph ... (Click the Palm Tree again to close it) Show TPTP problem
for m, k, f being Nat
for r being Tuple of (m + 2),(k -SD ) st m >= 1 & k >= 2 & f needs_digits_of m,k holds
ex s being Integer st
( - f < (SDDec (Mmin r)) - (s * f) & (SDDec (M0 r)) - (s * f) < f )
proof end;

theorem :: RADIX_6:16  Show TPTP formulae Show IDV graph:: Showing IDV graph ... (Click the Palm Tree again to close it) Show TPTP problem
for m, k being Nat
for r being Tuple of (m + 2),(k -SD ) st m >= 1 & k >= 2 & not ( SDDec (M0 r) <= SDDec r & SDDec r <= SDDec (Mmax r) ) holds
( SDDec (Mmin r) <= SDDec r & SDDec r < SDDec (M0 r) )
proof end;

definition
let i, m, k be Nat;
let r be Tuple of (m + 2),(k -SD );
assume A1: i in Seg (m + 2) ;
func MmaskDigit r,i -> Element of k -SD equals :Def8: :: RADIX_6:def 8
r . i if i < m
0 if i >= m
;
coherence
( ( i < m implies r . i is Element of k -SD ) & ( i >= m implies 0 is Element of k -SD ) )
proof end;
consistency
for b1 being Element of k -SD st i < m & i >= m holds
( b1 = r . i iff b1 = 0 ) ;
end;

:: deftheorem Def8 defines MmaskDigit RADIX_6:def 8 :
for i, m, k being Nat
for r being Tuple of (m + 2),(k -SD ) st i in Seg (m + 2) holds
( ( i < m implies MmaskDigit r,i = r . i ) & ( i >= m implies MmaskDigit r,i = 0 ) );

definition
let m, k be Nat;
let r be Tuple of (m + 2),(k -SD );
func Mmask r -> Tuple of (m + 2),(k -SD ) means :Def9: :: RADIX_6:def 9
for i being Nat st i in Seg (m + 2) holds
DigA it,i = MmaskDigit r,i;
existence
ex b1 being Tuple of (m + 2),(k -SD ) st
for i being Nat st i in Seg (m + 2) holds
DigA b1,i = MmaskDigit r,i
proof end;
uniqueness
for b1, b2 being Tuple of (m + 2),(k -SD ) st ( for i being Nat st i in Seg (m + 2) holds
DigA b1,i = MmaskDigit r,i ) & ( for i being Nat st i in Seg (m + 2) holds
DigA b2,i = MmaskDigit r,i ) holds
b1 = b2
proof end;
end;

:: deftheorem Def9 defines Mmask RADIX_6:def 9 :
for m, k being Nat
for r, b4 being Tuple of (m + 2),(k -SD ) holds
( b4 = Mmask r iff for i being Nat st i in Seg (m + 2) holds
DigA b4,i = MmaskDigit r,i );

theorem Th17: :: RADIX_6:17  Show TPTP formulae Show IDV graph:: Showing IDV graph ... (Click the Palm Tree again to close it) Show TPTP problem
for m, k being Nat
for r being Tuple of (m + 2),(k -SD ) st m >= 1 & k >= 2 holds
(SDDec (M0 r)) + (SDDec (Mmask r)) = (SDDec r) + (SDDec (DecSD 0,(m + 2),k))
proof end;

theorem :: RADIX_6:18  Show TPTP formulae Show IDV graph:: Showing IDV graph ... (Click the Palm Tree again to close it) Show TPTP problem
for m, k being Nat
for r being Tuple of (m + 2),(k -SD ) st m >= 1 & k >= 2 & SDDec (Mmask r) > 0 holds
SDDec r > SDDec (M0 r)
proof end;

definition
let i, m, k be Nat;
assume A1: k >= 2 ;
func FSDMinDigit m,k,i -> Element of k -SD equals :Def10: :: RADIX_6:def 10
0 if i > m
1 if i = m
otherwise (- (Radix k)) + 1;
coherence
( ( i > m implies 0 is Element of k -SD ) & ( i = m implies 1 is Element of k -SD ) & ( not i > m & not i = m implies (- (Radix k)) + 1 is Element of k -SD ) )
proof end;
consistency
for b1 being Element of k -SD st i > m & i = m holds
( b1 = 0 iff b1 = 1 ) ;
end;

:: deftheorem Def10 defines FSDMinDigit RADIX_6:def 10 :
for i, m, k being Nat st k >= 2 holds
( ( i > m implies FSDMinDigit m,k,i = 0 ) & ( i = m implies FSDMinDigit m,k,i = 1 ) & ( not i > m & not i = m implies FSDMinDigit m,k,i = (- (Radix k)) + 1 ) );

definition
let n, m, k be Nat;
func FSDMin n,m,k -> Tuple of n,(k -SD ) means :Def11: :: RADIX_6:def 11
for i being Nat st i in Seg n holds
DigA it,i = FSDMinDigit 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 = FSDMinDigit 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 = FSDMinDigit m,k,i ) & ( for i being Nat st i in Seg n holds
DigA b2,i = FSDMinDigit m,k,i ) holds
b1 = b2
proof end;
end;

:: deftheorem Def11 defines FSDMin RADIX_6:def 11 :
for n, m, k being Nat
for b4 being Tuple of n,(k -SD ) holds
( b4 = FSDMin n,m,k iff for i being Nat st i in Seg n holds
DigA b4,i = FSDMinDigit m,k,i );

theorem Th19: :: RADIX_6:19  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 (FSDMin n,m,k) = 1
proof end;

definition
let n, m, k be Nat;
let r be Tuple of (m + 2),(k -SD );
pred r is_Zero_over n means :Def12: :: RADIX_6:def 12
for i being Nat st i > n holds
DigA r,i = 0;
end;

:: deftheorem Def12 defines is_Zero_over RADIX_6:def 12 :
for n, m, k being Nat
for r being Tuple of (m + 2),(k -SD ) holds
( r is_Zero_over n iff for i being Nat st i > n holds
DigA r,i = 0 );

theorem :: RADIX_6:20  Show TPTP formulae Show IDV graph:: Showing IDV graph ... (Click the Palm Tree again to close it) Show TPTP problem
for m being Nat st m >= 1 holds
for n, k being Nat
for r being Tuple of (m + 2),(k -SD ) st k >= 2 & n in Seg (m + 2) & Mmask r is_Zero_over n & DigA (Mmask r),n > 0 holds
SDDec (Mmask r) > 0
proof end;