REAL is set
NAT is V1() V4() V5() V6() Element of K6(REAL)
K6(REAL) is set
COMPLEX is set
NAT is V1() V4() V5() V6() set
K6(NAT) is set
K6(NAT) is set
RAT is set
INT is set
K7(REAL,REAL) is set
K6(K7(REAL,REAL)) is set
K327() is V69() V97() L8()
the U1 of K327() is set
K6(INT) is set
0 is V1() V4() V5() V6() V8() V9() V10() V11() V12() integer ext-real non positive non negative Element of NAT
1 is V1() V4() V5() V6() V10() V11() V12() integer ext-real positive non negative Element of NAT
2 is V1() V4() V5() V6() V10() V11() V12() integer ext-real positive non negative Element of NAT
m is V4() V5() V6() V10() V11() V12() integer ext-real non negative set
m + 2 is V1() V4() V5() V6() V10() V11() V12() integer ext-real positive non negative set
m is V4() V5() V6() V10() V11() V12() integer ext-real non negative set
m + 1 is V1() V4() V5() V6() V10() V11() V12() integer ext-real positive non negative set
n is V4() V5() V6() V10() V11() V12() integer ext-real non negative set
k is V4() V5() V6() V10() V11() V12() integer ext-real non negative set
n + (m + 1) is V1() V4() V5() V6() V10() V11() V12() integer ext-real positive non negative set
Fmin ((n + (m + 1)),n,k) is V15() V18( NAT ) V19(k -SD ) Function-like V35(n + (m + 1)) FinSequence-like FinSequence of k -SD
k -SD is V1() Element of K6(INT)
SDDec (Fmin ((n + (m + 1)),n,k)) is V11() V12() integer ext-real set
Fmin (n,n,k) is V15() V18( NAT ) V19(k -SD ) Function-like V35(n) FinSequence-like FinSequence of k -SD
SDDec (Fmin (n,n,k)) is V11() V12() integer ext-real set
n + m is V4() V5() V6() V10() V11() V12() integer ext-real non negative set
(n + m) + 1 is V1() V4() V5() V6() V10() V11() V12() integer ext-real positive non negative set
Seg ((n + m) + 1) is Element of K6(NAT)
Fmin (((n + m) + 1),n,k) is V15() V18( NAT ) V19(k -SD ) Function-like V35((n + m) + 1) FinSequence-like FinSequence of k -SD
DigA ((Fmin (((n + m) + 1),n,k)),((n + m) + 1)) is V11() V12() integer ext-real set
FminDigit (n,k,((n + m) + 1)) is Element of k -SD
Seg (n + m) is Element of K6(NAT)
Fmin ((n + m),n,k) is V15() V18( NAT ) V19(k -SD ) Function-like V35(n + m) FinSequence-like FinSequence of k -SD
r is V4() V5() V6() V10() V11() V12() integer ext-real non negative set
(Fmin (((n + m) + 1),n,k)) . r is set
(Fmin ((n + m),n,k)) . r is set
DigA ((Fmin (((n + m) + 1),n,k)),r) is V11() V12() integer ext-real set
FminDigit (n,k,r) is Element of k -SD
DigA ((Fmin ((n + m),n,k)),r) is V11() V12() integer ext-real set
SDDec (Fmin ((n + m),n,k)) is V11() V12() integer ext-real set
Radix k is V4() V5() V6() V10() V11() V12() integer ext-real non negative Element of NAT
(Radix k) |^ (n + m) is V4() V5() V6() V10() V11() V12() integer ext-real non negative set
((Radix k) |^ (n + m)) * (DigA ((Fmin (((n + m) + 1),n,k)),((n + m) + 1))) is V11() V12() integer ext-real set
(SDDec (Fmin ((n + m),n,k))) + (((Radix k) |^ (n + m)) * (DigA ((Fmin (((n + m) + 1),n,k)),((n + m) + 1)))) is V11() V12() integer ext-real set
m is V4() V5() V6() V10() V11() V12() integer ext-real non negative set
n is V4() V5() V6() V10() V11() V12() integer ext-real non negative set
m + 1 is V1() V4() V5() V6() V10() V11() V12() integer ext-real positive non negative set
Fmin ((m + 1),m,n) is V15() V18( NAT ) V19(n -SD ) Function-like V35(m + 1) FinSequence-like FinSequence of n -SD
n -SD is V1() Element of K6(INT)
SDDec (Fmin ((m + 1),m,n)) is V11() V12() integer ext-real set
Fmin (m,m,n) is V15() V18( NAT ) V19(n -SD ) Function-like V35(m) FinSequence-like FinSequence of n -SD
SDDec (Fmin (m,m,n)) is V11() V12() integer ext-real set
Seg m is Element of K6(NAT)
k is V4() V5() V6() V10() V11() V12() integer ext-real non negative set
(Fmin ((m + 1),m,n)) . k is set
(Fmin (m,m,n)) . k is set
Seg (m + 1) is Element of K6(NAT)
DigA ((Fmin ((m + 1),m,n)),k) is V11() V12() integer ext-real set
FminDigit (m,n,k) is Element of n -SD
DigA ((Fmin (m,m,n)),k) is V11() V12() integer ext-real set
Radix n is V4() V5() V6() V10() V11() V12() integer ext-real non negative Element of NAT
(Radix n) |^ m is V4() V5() V6() V10() V11() V12() integer ext-real non negative set
DigA ((Fmin ((m + 1),m,n)),(m + 1)) is V11() V12() integer ext-real set
((Radix n) |^ m) * (DigA ((Fmin ((m + 1),m,n)),(m + 1))) is V11() V12() integer ext-real set
(SDDec (Fmin (m,m,n))) + (((Radix n) |^ m) * (DigA ((Fmin ((m + 1),m,n)),(m + 1)))) is V11() V12() integer ext-real set
Seg (m + 1) is Element of K6(NAT)
FminDigit (m,n,(m + 1)) is Element of n -SD
m is V4() V5() V6() V10() V11() V12() integer ext-real non negative set
n is V4() V5() V6() V10() V11() V12() integer ext-real non negative set
k is V4() V5() V6() V10() V11() V12() integer ext-real non negative set
n + m is V4() V5() V6() V10() V11() V12() integer ext-real non negative set
Fmin ((n + m),n,k) is V15() V18( NAT ) V19(k -SD ) Function-like V35(n + m) FinSequence-like FinSequence of k -SD
k -SD is V1() Element of K6(INT)
SDDec (Fmin ((n + m),n,k)) is V11() V12() integer ext-real set
Fmin (n,n,k) is V15() V18( NAT ) V19(k -SD ) Function-like V35(n) FinSequence-like FinSequence of k -SD
SDDec (Fmin (n,n,k)) is V11() V12() integer ext-real set
m is V4() V5() V6() V10() V11() V12() integer ext-real non negative set
m + 1 is V1() V4() V5() V6() V10() V11() V12() integer ext-real positive non negative set
n is V4() V5() V6() V10() V11() V12() integer ext-real non negative set
Fmin ((m + 1),(m + 1),n) is V15() V18( NAT ) V19(n -SD ) Function-like V35(m + 1) FinSequence-like FinSequence of n -SD
n -SD is V1() Element of K6(INT)
SDDec (Fmin ((m + 1),(m + 1),n)) is V11() V12() integer ext-real set
Radix n is V4() V5() V6() V10() V11() V12() integer ext-real non negative Element of NAT
Seg (m + 1) is Element of K6(NAT)
DigA ((Fmin ((m + 1),(m + 1),n)),(m + 1)) is V11() V12() integer ext-real set
FminDigit ((m + 1),n,(m + 1)) is Element of n -SD
Seg m is Element of K6(NAT)
DecSD (0,m,n) is V15() V18( NAT ) V19(n -SD ) Function-like V35(m) FinSequence-like FinSequence of n -SD
k is V4() V5() V6() V10() V11() V12() integer ext-real non negative set
(Fmin ((m + 1),(m + 1),n)) . k is set
(DecSD (0,m,n)) . k is set
DigA ((Fmin ((m + 1),(m + 1),n)),k) is V11() V12() integer ext-real set
FminDigit ((m + 1),n,k) is Element of n -SD
DigA ((DecSD (0,m,n)),k) is V11() V12() integer ext-real set
SDDec (DecSD (0,m,n)) is V11() V12() integer ext-real set
(Radix n) |^ m is V4() V5() V6() V10() V11() V12() integer ext-real non negative set
((Radix n) |^ m) * (DigA ((Fmin ((m + 1),(m + 1),n)),(m + 1))) is V11() V12() integer ext-real set
(SDDec (DecSD (0,m,n))) + (((Radix n) |^ m) * (DigA ((Fmin ((m + 1),(m + 1),n)),(m + 1)))) is V11() V12() integer ext-real set
0 + ((Radix n) |^ m) is V4() V5() V6() V10() V11() V12() integer ext-real non negative set
m is V4() V5() V6() V10() V11() V12() integer ext-real non negative set
Fmin (1,1,m) is V15() V18( NAT ) V19(m -SD ) Function-like V35(1) FinSequence-like FinSequence of m -SD
m -SD is V1() Element of K6(INT)
SDDec (Fmin (1,1,m)) is V11() V12() integer ext-real set
Seg 1 is Element of K6(NAT)
DigitSD (Fmin (1,1,m)) is V15() V18( NAT ) V19( INT ) Function-like V35(1) FinSequence-like FinSequence of INT
(DigitSD (Fmin (1,1,m))) /. 1 is V11() V12() integer ext-real Element of INT
SubDigit ((Fmin (1,1,m)),1,m) is V11() V12() integer ext-real Element of INT
Radix m is V4() V5() V6() V10() V11() V12() integer ext-real non negative Element of NAT
1 -' 1 is V4() V5() V6() V10() V11() V12() integer ext-real non negative Element of NAT
(Radix m) |^ (1 -' 1) is V4() V5() V6() V10() V11() V12() integer ext-real non negative Element of NAT
DigB ((Fmin (1,1,m)),1) is V11() V12() integer ext-real Element of INT
((Radix m) |^ (1 -' 1)) * (DigB ((Fmin (1,1,m)),1)) is V11() V12() integer ext-real set
DigA ((Fmin (1,1,m)),1) is V11() V12() integer ext-real set
((Radix m) |^ (1 -' 1)) * (DigA ((Fmin (1,1,m)),1)) is V11() V12() integer ext-real set
(Radix m) |^ 0 is V4() V5() V6() V10() V11() V12() integer ext-real non negative Element of NAT
((Radix m) |^ 0) * (DigA ((Fmin (1,1,m)),1)) is V11() V12() integer ext-real set
1 * (DigA ((Fmin (1,1,m)),1)) is V11() V12() integer ext-real set
FminDigit (1,m,1) is Element of m -SD
<*1*> is V15() V18( NAT ) V19( NAT ) Function-like FinSequence-like FinSequence of NAT
Sum (DigitSD (Fmin (1,1,m))) is V11() V12() integer ext-real Element of INT
m is V4() V5() V6() V10() V11() V12() integer ext-real non negative set
n is V4() V5() V6() V10() V11() V12() integer ext-real non negative set
Fmin (m,m,n) is V15() V18( NAT ) V19(n -SD ) Function-like V35(m) FinSequence-like FinSequence of n -SD
n -SD is V1() Element of K6(INT)
SDDec (Fmin (m,m,n)) is V11() V12() integer ext-real set
n is V4() V5() V6() V10() V11() V12() integer ext-real non negative set
n + 2 is V1() V4() V5() V6() V10() V11() V12() integer ext-real positive non negative set
k is V4() V5() V6() V10() V11() V12() integer ext-real non negative set
k -SD is V1() Element of K6(INT)
m is V4() V5() V6() V10() V11() V12() integer ext-real non negative set
Seg (n + 2) is Element of K6(NAT)
r is V15() V18( NAT ) V19(k -SD ) Function-like V35(n + 2) FinSequence-like FinSequence of k -SD
r . m is set
len r is V4() V5() V6() V10() V11() V12() integer ext-real non negative Element of NAT
dom r is Element of K6(NAT)
rng r is Element of K6((k -SD))
K6((k -SD)) is set
m is V4() V5() V6() V10() V11() V12() integer ext-real non negative set
m + 2 is V1() V4() V5() V6() V10() V11() V12() integer ext-real positive non negative set
n is V4() V5() V6() V10() V11() V12() integer ext-real non negative set
n -SD is V1() Element of K6(INT)
Seg (m + 2) is Element of K6(NAT)
k is V15() V18( NAT ) V19(n -SD ) Function-like V35(m + 2) FinSequence-like FinSequence of n -SD
r is V15() V18( NAT ) V19(n -SD ) Function-like FinSequence-like FinSequence of n -SD
len r is V4() V5() V6() V10() V11() V12() integer ext-real non negative Element of NAT
dom r is Element of K6(NAT)
(m + 2) -tuples_on (n -SD) is V1() functional FinSequence-membered FinSequenceSet of n -SD
i is V15() V18( NAT ) V19(n -SD ) Function-like V35(m + 2) FinSequence-like FinSequence of n -SD
j is V4() V5() V6() V10() V11() V12() integer ext-real non negative set
DigA (i,j) is V11() V12() integer ext-real set
(j,m,n,k) is Element of n -SD
i . j is set
r is V15() V18( NAT ) V19(n -SD ) Function-like V35(m + 2) FinSequence-like FinSequence of n -SD
i is V15() V18( NAT ) V19(n -SD ) Function-like V35(m + 2) FinSequence-like FinSequence of n -SD
len r is V4() V5() V6() V10() V11() V12() integer ext-real non negative Element of NAT
dom r is Element of K6(NAT)
j is V4() V5() V6() V10() V11() V12() integer ext-real non negative set
r . j is set
DigA (r,j) is V11() V12() integer ext-real set
(j,m,n,k) is Element of n -SD
DigA (i,j) is V11() V12() integer ext-real set
i . j is set
len i is V4() V5() V6() V10() V11() V12() integer ext-real non negative Element of NAT
n is V4() V5() V6() V10() V11() V12() integer ext-real non negative set
n + 2 is V1() V4() V5() V6() V10() V11() V12() integer ext-real positive non negative set
k is V4() V5() V6() V10() V11() V12() integer ext-real non negative set
k -SD is V1() Element of K6(INT)
m is V4() V5() V6() V10() V11() V12() integer ext-real non negative set
Seg (n + 2) is Element of K6(NAT)
r is V15() V18( NAT ) V19(k -SD ) Function-like V35(n + 2) FinSequence-like FinSequence of k -SD
r . m is set
Radix k is V4() V5() V6() V10() V11() V12() integer ext-real non negative Element of NAT
(Radix k) - 1 is V11() V12() integer ext-real set
len r is V4() V5() V6() V10() V11() V12() integer ext-real non negative Element of NAT
dom r is Element of K6(NAT)
rng r is Element of K6((k -SD))
K6((k -SD)) is set
m is V4() V5() V6() V10() V11() V12() integer ext-real non negative set
m + 2 is V1() V4() V5() V6() V10() V11() V12() integer ext-real positive non negative set
n is V4() V5() V6() V10() V11() V12() integer ext-real non negative set
n -SD is V1() Element of K6(INT)
Seg (m + 2) is Element of K6(NAT)
k is V15() V18( NAT ) V19(n -SD ) Function-like V35(m + 2) FinSequence-like FinSequence of n -SD
r is V15() V18( NAT ) V19(n -SD ) Function-like FinSequence-like FinSequence of n -SD
len r is V4() V5() V6() V10() V11() V12() integer ext-real non negative Element of NAT
dom r is Element of K6(NAT)
(m + 2) -tuples_on (n -SD) is V1() functional FinSequence-membered FinSequenceSet of n -SD
i is V15() V18( NAT ) V19(n -SD ) Function-like V35(m + 2) FinSequence-like FinSequence of n -SD
j is V4() V5() V6() V10() V11() V12() integer ext-real non negative set
DigA (i,j) is V11() V12() integer ext-real set
(j,m,n,k) is Element of n -SD
i . j is set
r is V15() V18( NAT ) V19(n -SD ) Function-like V35(m + 2) FinSequence-like FinSequence of n -SD
i is V15() V18( NAT ) V19(n -SD ) Function-like V35(m + 2) FinSequence-like FinSequence of n -SD
len r is V4() V5() V6() V10() V11() V12() integer ext-real non negative Element of NAT
dom r is Element of K6(NAT)
j is V4() V5() V6() V10() V11() V12() integer ext-real non negative set
r . j is set
DigA (r,j) is V11() V12() integer ext-real set
(j,m,n,k) is Element of n -SD
DigA (i,j) is V11() V12() integer ext-real set
i . j is set
len i is V4() V5() V6() V10() V11() V12() integer ext-real non negative Element of NAT
n is V4() V5() V6() V10() V11() V12() integer ext-real non negative set
n + 2 is V1() V4() V5() V6() V10() V11() V12() integer ext-real positive non negative set
k is V4() V5() V6() V10() V11() V12() integer ext-real non negative set
k -SD is V1() Element of K6(INT)
m is V4() V5() V6() V10() V11() V12() integer ext-real non negative set
Seg (n + 2) is Element of K6(NAT)
r is V15() V18( NAT ) V19(k -SD ) Function-like V35(n + 2) FinSequence-like FinSequence of k -SD
r . m is set
Radix k is V4() V5() V6() V10() V11() V12() integer ext-real non negative Element of NAT
- (Radix k) is V11() V12() integer ext-real non positive set
(- (Radix k)) + 1 is V11() V12() integer ext-real set
len r is V4() V5() V6() V10() V11() V12() integer ext-real non negative Element of NAT
dom r is Element of K6(NAT)
rng r is Element of K6((k -SD))
K6((k -SD)) is set
(Radix k) + (Radix k) is V4() V5() V6() V10() V11() V12() integer ext-real non negative set
1 + 1 is V1() V4() V5() V6() V10() V11() V12() integer ext-real positive non negative set
(Radix k) - 1 is V11() V12() integer ext-real set
1 - (Radix k) is V11() V12() integer ext-real set
{ b1 where b1 is V11() V12() integer ext-real Element of INT : ( b1 <= (Radix k) - 1 & (- (Radix k)) + 1 <= b1 ) } is set
m is V4() V5() V6() V10() V11() V12() integer ext-real non negative set
m + 2 is V1() V4() V5() V6() V10() V11() V12() integer ext-real positive non negative set
n is V4() V5() V6() V10() V11() V12() integer ext-real non negative set
n -SD is V1() Element of K6(INT)
Seg (m + 2) is Element of K6(NAT)
k is V15() V18( NAT ) V19(n -SD ) Function-like V35(m + 2) FinSequence-like FinSequence of n -SD
r is V15() V18( NAT ) V19(n -SD ) Function-like FinSequence-like FinSequence of n -SD
len r is V4() V5() V6() V10() V11() V12() integer ext-real non negative Element of NAT
dom r is Element of K6(NAT)
(m + 2) -tuples_on (n -SD) is V1() functional FinSequence-membered FinSequenceSet of n -SD
i is V15() V18( NAT ) V19(n -SD ) Function-like V35(m + 2) FinSequence-like FinSequence of n -SD
j is V4() V5() V6() V10() V11() V12() integer ext-real non negative set
DigA (i,j) is V11() V12() integer ext-real set
(j,m,n,k) is Element of n -SD
i . j is set
r is V15() V18( NAT ) V19(n -SD ) Function-like V35(m + 2) FinSequence-like FinSequence of n -SD
i is V15() V18( NAT ) V19(n -SD ) Function-like V35(m + 2) FinSequence-like FinSequence of n -SD
len r is V4() V5() V6() V10() V11() V12() integer ext-real non negative Element of NAT
dom r is Element of K6(NAT)
j is V4() V5() V6() V10() V11() V12() integer ext-real non negative set
r . j is set
DigA (r,j) is V11() V12() integer ext-real set
(j,m,n,k) is Element of n -SD
DigA (i,j) is V11() V12() integer ext-real set
i . j is set
len i is V4() V5() V6() V10() V11() V12() integer ext-real non negative Element of NAT
n is V4() V5() V6() V10() V11() V12() integer ext-real non negative set
m is V4() V5() V6() V10() V11() V12() integer ext-real non negative set
m + 2 is V1() V4() V5() V6() V10() V11() V12() integer ext-real positive non negative set
n -SD is V1() Element of K6(INT)
k is V15() V18( NAT ) V19(n -SD ) Function-like V35(m + 2) FinSequence-like FinSequence of n -SD
SDDec k is V11() V12() integer ext-real set
(m,n,k) is V15() V18( NAT ) V19(n -SD ) Function-like V35(m + 2) FinSequence-like FinSequence of n -SD
SDDec (m,n,k) is V11() V12() integer ext-real set
Seg (m + 2) is Element of K6(NAT)
r is V4() V5() V6() V10() V11() V12() integer ext-real non negative set
DigA (k,r) is V11() V12() integer ext-real set
DigA ((m,n,k),r) is V11() V12() integer ext-real set
(r,m,n,k) is Element of n -SD
k . r is set
k . r is set
Radix n is V4() V5() V6() V10() V11() V12() integer ext-real non negative Element of NAT
(Radix n) - 1 is V11() V12() integer ext-real set
n is V4() V5() V6() V10() V11() V12() integer ext-real non negative set
m is V4() V5() V6() V10() V11() V12() integer ext-real non negative set
m + 2 is V1() V4() V5() V6() V10() V11() V12() integer ext-real positive non negative set
n -SD is V1() Element of K6(INT)
k is V15() V18( NAT ) V19(n -SD ) Function-like V35(m + 2) FinSequence-like FinSequence of n -SD
(m,n,k) is V15() V18( NAT ) V19(n -SD ) Function-like V35(m + 2) FinSequence-like FinSequence of n -SD
SDDec (m,n,k) is V11() V12() integer ext-real set
SDDec k is V11() V12() integer ext-real set
Seg (m + 2) is Element of K6(NAT)
r is V4() V5() V6() V10() V11() V12() integer ext-real non negative set
DigA ((m,n,k),r) is V11() V12() integer ext-real set
DigA (k,r) is V11() V12() integer ext-real set
(r,m,n,k) is Element of n -SD
k . r is set
k . r is set
Radix n is V4() V5() V6() V10() V11() V12() integer ext-real non negative Element of NAT
- (Radix n) is V11() V12() integer ext-real non positive set
(- (Radix n)) + 1 is V11() V12() integer ext-real set
r is V4() V5() V6() V10() V11() V12() integer ext-real non negative set
n is V4() V5() V6() V10() V11() V12() integer ext-real non negative set
Seg n is Element of K6(NAT)
k is V4() V5() V6() V10() V11() V12() integer ext-real non negative set
m is V4() V5() V6() V10() V11() V12() integer ext-real non negative set
DecSD (m,n,k) is V15() V18( NAT ) V19(k -SD ) Function-like V35(n) FinSequence-like FinSequence of k -SD
k -SD is V1() Element of K6(INT)
DigA ((DecSD (m,n,k)),r) is V11() V12() integer ext-real set
DigitDC (m,r,k) is Element of k -SD
Radix k is V4() V5() V6() V10() V11() V12() integer ext-real non negative Element of NAT
(Radix k) |^ r is V4() V5() V6() V10() V11() V12() integer ext-real non negative set
m mod ((Radix k) |^ r) is V4() V5() V6() V10() V11() V12() integer ext-real non negative Element of NAT
r -' 1 is V4() V5() V6() V10() V11() V12() integer ext-real non negative Element of NAT
(Radix k) |^ (r -' 1) is V4() V5() V6() V10() V11() V12() integer ext-real non negative Element of NAT
(m mod ((Radix k) |^ r)) div ((Radix k) |^ (r -' 1)) is V4() V5() V6() V10() V11() V12() integer ext-real non negative Element of NAT
m div ((Radix k) |^ (r -' 1)) is V4() V5() V6() V10() V11() V12() integer ext-real non negative Element of NAT
(m div ((Radix k) |^ (r -' 1))) mod (Radix k) is V4() V5() V6() V10() V11() V12() integer ext-real non negative Element of NAT
m is V4() V5() V6() V10() V11() V12() integer ext-real non negative set
n is V4() V5() V6() V10() V11() V12() integer ext-real non negative set
k is V4() V5() V6() V10() V11() V12() integer ext-real non negative set
DecSD (k,m,n) is V15() V18( NAT ) V19(n -SD ) Function-like V35(m) FinSequence-like FinSequence of n -SD
n -SD is V1() Element of K6(INT)
DigA ((DecSD (k,m,n)),m) is V11() V12() integer ext-real set
Radix n is V4() V5() V6() V10() V11() V12() integer ext-real non negative Element of NAT
(Radix n) |^ m is V4() V5() V6() V10() V11() V12() integer ext-real non negative set
k mod ((Radix n) |^ m) is V4() V5() V6() V10() V11() V12() integer ext-real non negative Element of NAT
Seg m is Element of K6(NAT)
DigitDC (k,m,n) is Element of n -SD
m -' 1 is V4() V5() V6() V10() V11() V12() integer ext-real non negative Element of NAT
(Radix n) |^ (m -' 1) is V4() V5() V6() V10() V11() V12() integer ext-real non negative Element of NAT
k div ((Radix n) |^ (m -' 1)) is V4() V5() V6() V10() V11() V12() integer ext-real non negative Element of NAT
n is V4() V5() V6() V10() V11() V12() integer ext-real non negative set
k is V4() V5() V6() V10() V11() V12() integer ext-real non negative set
m is V4() V5() V6() V10() V11() V12() integer ext-real non negative set
n + 2 is V1() V4() V5() V6() V10() V11() V12() integer ext-real positive non negative set
Fmin ((n + 2),n,k) is V15() V18( NAT ) V19(k -SD ) Function-like V35(n + 2) FinSequence-like FinSequence of k -SD
k -SD is V1() Element of K6(INT)
SDDec (Fmin ((n + 2),n,k)) is V11() V12() integer ext-real set
Seg n is Element of K6(NAT)
Fmin (n,n,k) is V15() V18( NAT ) V19(k -SD ) Function-like V35(n) FinSequence-like FinSequence of k -SD
DecSD (m,n,k) is V15() V18( NAT ) V19(k -SD ) Function-like V35(n) FinSequence-like FinSequence of k -SD
r is V4() V5() V6() V10() V11() V12() integer ext-real non negative set
DigA ((Fmin (n,n,k)),r) is V11() V12() integer ext-real set
DigA ((DecSD (m,n,k)),r) is V11() V12() integer ext-real set
0 + 1 is V1() V4() V5() V6() V10() V11() V12() integer ext-real positive non negative set
FminDigit (n,k,r) is Element of k -SD
FminDigit (n,k,r) is Element of k -SD
SDDec (Fmin (n,n,k)) is V11() V12() integer ext-real set
SDDec (DecSD (m,n,k)) is V11() V12() integer ext-real set
Radix k is V4() V5() V6() V10() V11() V12() integer ext-real non negative Element of NAT
(Radix k) |^ n is V4() V5() V6() V10() V11() V12() integer ext-real non negative set
m is V11() V12() integer ext-real set
k is V11() V12() integer ext-real set
m + k is V11() V12() integer ext-real set
n is V11() V12() integer ext-real set
- k is V11() V12() integer ext-real set
r is V4() V5() V6() V10() V11() V12() integer ext-real non negative Element of NAT
m + r is V11() V12() integer ext-real set
n div r is V11() V12() integer ext-real set
(n div r) * r is V11() V12() integer ext-real set
- ((n div r) * r) is V11() V12() integer ext-real set
(m + r) + (- ((n div r) * r)) is V11() V12() integer ext-real set
n + (- ((n div r) * r)) is V11() V12() integer ext-real set
n mod r is V11() V12() integer ext-real set
n - ((n div r) * r) is V11() V12() integer ext-real set
m + (- ((n div r) * r)) is V11() V12() integer ext-real set
(m + (- ((n div r) * r))) + r is V11() V12() integer ext-real set
- r is V11() V12() integer ext-real non positive set
((m + (- ((n div r) * r))) + r) + (- r) is V11() V12() integer ext-real set
0 + (- r) is V11() V12() integer ext-real non positive set
m - ((n div r) * r) is V11() V12() integer ext-real set
n is V4() V5() V6() V10() V11() V12() integer ext-real non negative set
m is V4() V5() V6() V10() V11() V12() integer ext-real non negative set
m + 2 is V1() V4() V5() V6() V10() V11() V12() integer ext-real positive non negative set
n -SD is V1() Element of K6(INT)
DecSD (0,(m + 2),n) is V15() V18( NAT ) V19(n -SD ) Function-like V35(m + 2) FinSequence-like FinSequence of n -SD
SDDec (DecSD (0,(m + 2),n)) is V11() V12() integer ext-real set
SDMax ((m + 2),m,n) is V15() V18( NAT ) V19(n -SD ) Function-like V35(m + 2) FinSequence-like FinSequence of n -SD
SDDec (SDMax ((m + 2),m,n)) is V11() V12() integer ext-real set
k is V15() V18( NAT ) V19(n -SD ) Function-like V35(m + 2) FinSequence-like FinSequence of n -SD
(m,n,k) is V15() V18( NAT ) V19(n -SD ) Function-like V35(m + 2) FinSequence-like FinSequence of n -SD
SDDec (m,n,k) is V11() V12() integer ext-real set
(SDDec (m,n,k)) + (SDDec (DecSD (0,(m + 2),n))) is V11() V12() integer ext-real set
(m,n,k) is V15() V18( NAT ) V19(n -SD ) Function-like V35(m + 2) FinSequence-like FinSequence of n -SD
SDDec (m,n,k) is V11() V12() integer ext-real set
(SDDec (m,n,k)) + (SDDec (SDMax ((m + 2),m,n))) is V11() V12() integer ext-real set
Seg (m + 2) is Element of K6(NAT)
r is V4() V5() V6() V10() V11() V12() integer ext-real non negative set
DigA ((m,n,k),r) is V11() V12() integer ext-real set
DigA ((m,n,k),r) is V11() V12() integer ext-real set
DigA ((SDMax ((m + 2),m,n)),r) is V11() V12() integer ext-real set
(r,m,n,k) is Element of n -SD
(r,m,n,k) is Element of n -SD
Radix n is V4() V5() V6() V10() V11() V12() integer ext-real non negative Element of NAT
(Radix n) - 1 is V11() V12() integer ext-real set
SDMaxDigit (m,n,r) is Element of n -SD
SDMaxDigit (m,n,r) is Element of n -SD
k . r is set
(r,m,n,k) is Element of n -SD
m is V4() V5() V6() V10() V11() V12() integer ext-real non negative set
n is V4() V5() V6() V10() V11() V12() integer ext-real non negative set
m + 2 is V1() V4() V5() V6() V10() V11() V12() integer ext-real positive non negative set
n -SD is V1() Element of K6(INT)
Fmin ((m + 2),m,n) is V15() V18( NAT ) V19(n -SD ) Function-like V35(m + 2) FinSequence-like FinSequence of n -SD
SDDec (Fmin ((m + 2),m,n)) is V11() V12() integer ext-real set
k is V15() V18( NAT ) V19(n -SD ) Function-like V35(m + 2) FinSequence-like FinSequence of n -SD
(m,n,k) is V15() V18( NAT ) V19(n -SD ) Function-like V35(m + 2) FinSequence-like FinSequence of n -SD
SDDec (m,n,k) is V11() V12() integer ext-real set
(SDDec (m,n,k)) + (SDDec (Fmin ((m + 2),m,n))) is V11() V12() integer ext-real set
(m,n,k) is V15() V18( NAT ) V19(n -SD ) Function-like V35(m + 2) FinSequence-like FinSequence of n -SD
SDDec (m,n,k) is V11() V12() integer ext-real set
(SDDec (m,n,k)) + 1 is V11() V12() integer ext-real set
(SDDec (m,n,k)) + 0 is V11() V12() integer ext-real set
SDMax ((m + 2),m,n) is V15() V18( NAT ) V19(n -SD ) Function-like V35(m + 2) FinSequence-like FinSequence of n -SD
SDDec (SDMax ((m + 2),m,n)) is V11() V12() integer ext-real set
(SDDec (m,n,k)) + (SDDec (SDMax ((m + 2),m,n))) is V11() V12() integer ext-real set
DecSD (0,(m + 2),n) is V15() V18( NAT ) V19(n -SD ) Function-like V35(m + 2) FinSequence-like FinSequence of n -SD
SDDec (DecSD (0,(m + 2),n)) is V11() V12() integer ext-real set
(SDDec (m,n,k)) + (SDDec (DecSD (0,(m + 2),n))) is V11() V12() integer ext-real set
Seg (m + 2) is Element of K6(NAT)
DecSD (1,(m + 2),n) is V15() V18( NAT ) V19(n -SD ) Function-like V35(m + 2) FinSequence-like FinSequence of n -SD
SDDec (DecSD (1,(m + 2),n)) is V11() V12() integer ext-real set
(SDDec (SDMax ((m + 2),m,n))) + (SDDec (DecSD (1,(m + 2),n))) is V11() V12() integer ext-real set
(SDDec (SDMax ((m + 2),m,n))) + 1 is V11() V12() integer ext-real set
n is V4() V5() V6() V10() V11() V12() integer ext-real non negative set
m is V4() V5() V6() V10() V11() V12() integer ext-real non negative set
m + 2 is V1() V4() V5() V6() V10() V11() V12() integer ext-real positive non negative set
n -SD is V1() Element of K6(INT)
DecSD (0,(m + 2),n) is V15() V18( NAT ) V19(n -SD ) Function-like V35(m + 2) FinSequence-like FinSequence of n -SD
SDDec (DecSD (0,(m + 2),n)) is V11() V12() integer ext-real set
SDMin ((m + 2),m,n) is V15() V18( NAT ) V19(n -SD ) Function-like V35(m + 2) FinSequence-like FinSequence of n -SD
SDDec (SDMin ((m + 2),m,n)) is V11() V12() integer ext-real set
k is V15() V18( NAT ) V19(n -SD ) Function-like V35(m + 2) FinSequence-like FinSequence of n -SD
(m,n,k) is V15() V18( NAT ) V19(n -SD ) Function-like V35(m + 2) FinSequence-like FinSequence of n -SD
SDDec (m,n,k) is V11() V12() integer ext-real set
(SDDec (m,n,k)) + (SDDec (DecSD (0,(m + 2),n))) is V11() V12() integer ext-real set
(m,n,k) is V15() V18( NAT ) V19(n -SD ) Function-like V35(m + 2) FinSequence-like FinSequence of n -SD
SDDec (m,n,k) is V11() V12() integer ext-real set
(SDDec (m,n,k)) + (SDDec (SDMin ((m + 2),m,n))) is V11() V12() integer ext-real set
Seg (m + 2) is Element of K6(NAT)
r is V4() V5() V6() V10() V11() V12() integer ext-real non negative set
DigA ((m,n,k),r) is V11() V12() integer ext-real set
DigA ((m,n,k),r) is V11() V12() integer ext-real set
DigA ((SDMin ((m + 2),m,n)),r) is V11() V12() integer ext-real set
(r,m,n,k) is Element of n -SD
(r,m,n,k) is Element of n -SD
Radix n is V4() V5() V6() V10() V11() V12() integer ext-real non negative Element of NAT
- (Radix n) is V11() V12() integer ext-real non positive set
(- (Radix n)) + 1 is V11() V12() integer ext-real set
SDMinDigit (m,n,r) is Element of n -SD
SDMinDigit (m,n,r) is Element of n -SD
k . r is set
(r,m,n,k) is Element of n -SD
m is V4() V5() V6() V10() V11() V12() integer ext-real non negative set
m + 2 is V1() V4() V5() V6() V10() V11() V12() integer ext-real positive non negative set
n is V4() V5() V6() V10() V11() V12() integer ext-real non negative set
n -SD is V1() Element of K6(INT)
DecSD (0,(m + 2),n) is V15() V18( NAT ) V19(n -SD ) Function-like V35(m + 2) FinSequence-like FinSequence of n -SD
SDDec (DecSD (0,(m + 2),n)) is V11() V12() integer ext-real set
SDMax ((m + 2),m,n) is V15() V18( NAT ) V19(n -SD ) Function-like V35(m + 2) FinSequence-like FinSequence of n -SD
SDDec (SDMax ((m + 2),m,n)) is V11() V12() integer ext-real set
k is V15() V18( NAT ) V19(n -SD ) Function-like V35(m + 2) FinSequence-like FinSequence of n -SD
(m,n,k) is V15() V18( NAT ) V19(n -SD ) Function-like V35(m + 2) FinSequence-like FinSequence of n -SD
SDDec (m,n,k) is V11() V12() integer ext-real set
(SDDec (m,n,k)) + (SDDec (DecSD (0,(m + 2),n))) is V11() V12() integer ext-real set
(m,n,k) is V15() V18( NAT ) V19(n -SD ) Function-like V35(m + 2) FinSequence-like FinSequence of n -SD
SDDec (m,n,k) is V11() V12() integer ext-real set
(SDDec (m,n,k)) + (SDDec (SDMax ((m + 2),m,n))) is V11() V12() integer ext-real set
SDMin ((m + 2),m,n) is V15() V18( NAT ) V19(n -SD ) Function-like V35(m + 2) FinSequence-like FinSequence of n -SD
SDDec (SDMin ((m + 2),m,n)) is V11() V12() integer ext-real set
(SDDec (m,n,k)) + (SDDec (SDMin ((m + 2),m,n))) is V11() V12() integer ext-real set
(SDDec (m,n,k)) + (SDDec (DecSD (0,(m + 2),n))) is V11() V12() integer ext-real set
(SDDec (m,n,k)) + 0 is V11() V12() integer ext-real set
(SDDec (SDMax ((m + 2),m,n))) + (SDDec (SDMin ((m + 2),m,n))) is V11() V12() integer ext-real set
(SDDec (m,n,k)) + ((SDDec (SDMax ((m + 2),m,n))) + (SDDec (SDMin ((m + 2),m,n)))) is V11() V12() integer ext-real set
m is V4() V5() V6() V10() V11() V12() integer ext-real non negative set
n is V4() V5() V6() V10() V11() V12() integer ext-real non negative set
m + 2 is V1() V4() V5() V6() V10() V11() V12() integer ext-real positive non negative set
n -SD is V1() Element of K6(INT)
Fmin ((m + 2),m,n) is V15() V18( NAT ) V19(n -SD ) Function-like V35(m + 2) FinSequence-like FinSequence of n -SD
SDDec (Fmin ((m + 2),m,n)) is V11() V12() integer ext-real set
k is V15() V18( NAT ) V19(n -SD ) Function-like V35(m + 2) FinSequence-like FinSequence of n -SD
(m,n,k) is V15() V18( NAT ) V19(n -SD ) Function-like V35(m + 2) FinSequence-like FinSequence of n -SD
SDDec (m,n,k) is V11() V12() integer ext-real set
(SDDec (m,n,k)) + (SDDec (Fmin ((m + 2),m,n))) is V11() V12() integer ext-real set
(m,n,k) is V15() V18( NAT ) V19(n -SD ) Function-like V35(m + 2) FinSequence-like FinSequence of n -SD
SDDec (m,n,k) is V11() V12() integer ext-real set
SDMax ((m + 2),m,n) is V15() V18( NAT ) V19(n -SD ) Function-like V35(m + 2) FinSequence-like FinSequence of n -SD
SDDec (SDMax ((m + 2),m,n)) is V11() V12() integer ext-real set
(SDDec (m,n,k)) + (SDDec (SDMax ((m + 2),m,n))) is V11() V12() integer ext-real set
DecSD (0,(m + 2),n) is V15() V18( NAT ) V19(n -SD ) Function-like V35(m + 2) FinSequence-like FinSequence of n -SD
SDDec (DecSD (0,(m + 2),n)) is V11() V12() integer ext-real set
(SDDec (m,n,k)) + (SDDec (DecSD (0,(m + 2),n))) is V11() V12() integer ext-real set
(SDDec (m,n,k)) + 0 is V11() V12() integer ext-real set
(SDDec (m,n,k)) + 1 is V11() V12() integer ext-real set
Seg (m + 2) is Element of K6(NAT)
DecSD (1,(m + 2),n) is V15() V18( NAT ) V19(n -SD ) Function-like V35(m + 2) FinSequence-like FinSequence of n -SD
SDDec (DecSD (1,(m + 2),n)) is V11() V12() integer ext-real set
(SDDec (SDMax ((m + 2),m,n))) + (SDDec (DecSD (1,(m + 2),n))) is V11() V12() integer ext-real set
(SDDec (SDMax ((m + 2),m,n))) + 1 is V11() V12() integer ext-real set
m is V4() V5() V6() V10() V11() V12() integer ext-real non negative set
m + 2 is V1() V4() V5() V6() V10() V11() V12() integer ext-real positive non negative set
n is V4() V5() V6() V10() V11() V12() integer ext-real non negative set
n -SD is V1() Element of K6(INT)
k is V4() V5() V6() V10() V11() V12() integer ext-real non negative set
- k is V11() V12() integer ext-real non positive set
r is V15() V18( NAT ) V19(n -SD ) Function-like V35(m + 2) FinSequence-like FinSequence of n -SD
(m,n,r) is V15() V18( NAT ) V19(n -SD ) Function-like V35(m + 2) FinSequence-like FinSequence of n -SD
SDDec (m,n,r) is V11() V12() integer ext-real set
(m,n,r) is V15() V18( NAT ) V19(n -SD ) Function-like V35(m + 2) FinSequence-like FinSequence of n -SD
SDDec (m,n,r) is V11() V12() integer ext-real set
Fmin ((m + 2),m,n) is V15() V18( NAT ) V19(n -SD ) Function-like V35(m + 2) FinSequence-like FinSequence of n -SD
SDDec (Fmin ((m + 2),m,n)) is V11() V12() integer ext-real set
(SDDec (m,n,r)) + (SDDec (Fmin ((m + 2),m,n))) is V11() V12() integer ext-real set
(SDDec (m,n,r)) + k is V11() V12() integer ext-real set
Radix n is V4() V5() V6() V10() V11() V12() integer ext-real non negative Element of NAT
m -' 1 is V4() V5() V6() V10() V11() V12() integer ext-real non negative Element of NAT
(Radix n) |^ (m -' 1) is V4() V5() V6() V10() V11() V12() integer ext-real non negative Element of NAT
m is V4() V5() V6() V10() V11() V12() integer ext-real non negative set
m + 2 is V1() V4() V5() V6() V10() V11() V12() integer ext-real positive non negative set
n is V4() V5() V6() V10() V11() V12() integer ext-real non negative set
n -SD is V1() Element of K6(INT)
k is V4() V5() V6() V10() V11() V12() integer ext-real non negative set
- k is V11() V12() integer ext-real non positive set
r is V15() V18( NAT ) V19(n -SD ) Function-like V35(m + 2) FinSequence-like FinSequence of n -SD
(m,n,r) is V15() V18( NAT ) V19(n -SD ) Function-like V35(m + 2) FinSequence-like FinSequence of n -SD
SDDec (m,n,r) is V11() V12() integer ext-real set
(m,n,r) is V15() V18( NAT ) V19(n -SD ) Function-like V35(m + 2) FinSequence-like FinSequence of n -SD
SDDec (m,n,r) is V11() V12() integer ext-real set
Fmin ((m + 2),m,n) is V15() V18( NAT ) V19(n -SD ) Function-like V35(m + 2) FinSequence-like FinSequence of n -SD
SDDec (Fmin ((m + 2),m,n)) is V11() V12() integer ext-real set
(SDDec (m,n,r)) + (SDDec (Fmin ((m + 2),m,n))) is V11() V12() integer ext-real set
(SDDec (m,n,r)) + k is V11() V12() integer ext-real set
Radix n is V4() V5() V6() V10() V11() V12() integer ext-real non negative Element of NAT
m -' 1 is V4() V5() V6() V10() V11() V12() integer ext-real non negative Element of NAT
(Radix n) |^ (m -' 1) is V4() V5() V6() V10() V11() V12() integer ext-real non negative Element of NAT
m is V4() V5() V6() V10() V11() V12() integer ext-real non negative set
m + 2 is V1() V4() V5() V6() V10() V11() V12() integer ext-real positive non negative set
n is V4() V5() V6() V10() V11() V12() integer ext-real non negative set
n -SD is V1() Element of K6(INT)
k is V15() V18( NAT ) V19(n -SD ) Function-like V35(m + 2) FinSequence-like FinSequence of n -SD
(m,n,k) is V15() V18( NAT ) V19(n -SD ) Function-like V35(m + 2) FinSequence-like FinSequence of n -SD
SDDec (m,n,k) is V11() V12() integer ext-real set
SDDec k is V11() V12() integer ext-real set
(m,n,k) is V15() V18( NAT ) V19(n -SD ) Function-like V35(m + 2) FinSequence-like FinSequence of n -SD
SDDec (m,n,k) is V11() V12() integer ext-real set
(m,n,k) is V15() V18( NAT ) V19(n -SD ) Function-like V35(m + 2) FinSequence-like FinSequence of n -SD
SDDec (m,n,k) is V11() V12() integer ext-real set
n is V4() V5() V6() V10() V11() V12() integer ext-real non negative set
n + 2 is V1() V4() V5() V6() V10() V11() V12() integer ext-real positive non negative set
k is V4() V5() V6() V10() V11() V12() integer ext-real non negative set
k -SD is V1() Element of K6(INT)
m is V4() V5() V6() V10() V11() V12() integer ext-real non negative set
Seg (n + 2) is Element of K6(NAT)
r is V15() V18( NAT ) V19(k -SD ) Function-like V35(n + 2) FinSequence-like FinSequence of k -SD
r . m is set
len r is V4() V5() V6() V10() V11() V12() integer ext-real non negative Element of NAT
dom r is Element of K6(NAT)
rng r is Element of K6((k -SD))
K6((k -SD)) is set
m is V4() V5() V6() V10() V11() V12() integer ext-real non negative set
m + 2 is V1() V4() V5() V6() V10() V11() V12() integer ext-real positive non negative set
n is V4() V5() V6() V10() V11() V12() integer ext-real non negative set
n -SD is V1() Element of K6(INT)
Seg (m + 2) is Element of K6(NAT)
k is V15() V18( NAT ) V19(n -SD ) Function-like V35(m + 2) FinSequence-like FinSequence of n -SD
r is V15() V18( NAT ) V19(n -SD ) Function-like FinSequence-like FinSequence of n -SD
len r is V4() V5() V6() V10() V11() V12() integer ext-real non negative Element of NAT
dom r is Element of K6(NAT)
(m + 2) -tuples_on (n -SD) is V1() functional FinSequence-membered FinSequenceSet of n -SD
i is V15() V18( NAT ) V19(n -SD ) Function-like V35(m + 2) FinSequence-like FinSequence of n -SD
j is V4() V5() V6() V10() V11() V12() integer ext-real non negative set
DigA (i,j) is V11() V12() integer ext-real set
(j,m,n,k) is Element of n -SD
i . j is set
r is V15() V18( NAT ) V19(n -SD ) Function-like V35(m + 2) FinSequence-like FinSequence of n -SD
i is V15() V18( NAT ) V19(n -SD ) Function-like V35(m + 2) FinSequence-like FinSequence of n -SD
len r is V4() V5() V6() V10() V11() V12() integer ext-real non negative Element of NAT
dom r is Element of K6(NAT)
j is V4() V5() V6() V10() V11() V12() integer ext-real non negative set
r . j is set
DigA (r,j) is V11() V12() integer ext-real set
(j,m,n,k) is Element of n -SD
DigA (i,j) is V11() V12() integer ext-real set
i . j is set
len i is V4() V5() V6() V10() V11() V12() integer ext-real non negative Element of NAT
m is V4() V5() V6() V10() V11() V12() integer ext-real non negative set
m + 2 is V1() V4() V5() V6() V10() V11() V12() integer ext-real positive non negative set
n is V4() V5() V6() V10() V11() V12() integer ext-real non negative set
n -SD is V1() Element of K6(INT)
DecSD (0,(m + 2),n) is V15() V18( NAT ) V19(n -SD ) Function-like V35(m + 2) FinSequence-like FinSequence of n -SD
SDDec (DecSD (0,(m + 2),n)) is V11() V12() integer ext-real set
k is V15() V18( NAT ) V19(n -SD ) Function-like V35(m + 2) FinSequence-like FinSequence of n -SD
(m,n,k) is V15() V18( NAT ) V19(n -SD ) Function-like V35(m + 2) FinSequence-like FinSequence of n -SD
SDDec (m,n,k) is V11() V12() integer ext-real set
(m,n,k) is V15() V18( NAT ) V19(n -SD ) Function-like V35(m + 2) FinSequence-like FinSequence of n -SD
SDDec (m,n,k) is V11() V12() integer ext-real set
(SDDec (m,n,k)) + (SDDec (m,n,k)) is V11() V12() integer ext-real set
SDDec k is V11() V12() integer ext-real set
(SDDec k) + (SDDec (DecSD (0,(m + 2),n))) is V11() V12() integer ext-real set
Seg (m + 2) is Element of K6(NAT)
r is V4() V5() V6() V10() V11() V12() integer ext-real non negative set
DigA ((m,n,k),r) is V11() V12() integer ext-real set
DigA (k,r) is V11() V12() integer ext-real set
DigA ((m,n,k),r) is V11() V12() integer ext-real set
(r,m,n,k) is Element of n -SD
(r,m,n,k) is Element of n -SD
k . r is set
(r,m,n,k) is Element of n -SD
(r,m,n,k) is Element of n -SD
k . r is set
m is V4() V5() V6() V10() V11() V12() integer ext-real non negative set
m + 2 is V1() V4() V5() V6() V10() V11() V12() integer ext-real positive non negative set
n is V4() V5() V6() V10() V11() V12() integer ext-real non negative set
n -SD is V1() Element of K6(INT)
k is V15() V18( NAT ) V19(n -SD ) Function-like V35(m + 2) FinSequence-like FinSequence of n -SD
(m,n,k) is V15() V18( NAT ) V19(n -SD ) Function-like V35(m + 2) FinSequence-like FinSequence of n -SD
SDDec (m,n,k) is V11() V12() integer ext-real set
SDDec k is V11() V12() integer ext-real set
(m,n,k) is V15() V18( NAT ) V19(n -SD ) Function-like V35(m + 2) FinSequence-like FinSequence of n -SD
SDDec (m,n,k) is V11() V12() integer ext-real set
(SDDec (m,n,k)) + (SDDec (m,n,k)) is V11() V12() integer ext-real set
DecSD (0,(m + 2),n) is V15() V18( NAT ) V19(n -SD ) Function-like V35(m + 2) FinSequence-like FinSequence of n -SD
SDDec (DecSD (0,(m + 2),n)) is V11() V12() integer ext-real set
(SDDec k) + (SDDec (DecSD (0,(m + 2),n))) is V11() V12() integer ext-real set
(SDDec k) + 0 is V11() V12() integer ext-real set
(SDDec k) - (SDDec (m,n,k)) is V11() V12() integer ext-real set
(SDDec (m,n,k)) - 0 is V11() V12() integer ext-real set
k is V4() V5() V6() V10() V11() V12() integer ext-real non negative set
m is V4() V5() V6() V10() V11() V12() integer ext-real non negative set
n is V4() V5() V6() V10() V11() V12() integer ext-real non negative set
k -SD is V1() Element of K6(INT)
Radix k is V4() V5() V6() V10() V11() V12() integer ext-real non negative Element of NAT
- (Radix k) is V11() V12() integer ext-real non positive set
(- (Radix k)) + 1 is V11() V12() integer ext-real set
(Radix k) + (Radix k) is V4() V5() V6() V10() V11() V12() integer ext-real non negative set
1 + 1 is V1() V4() V5() V6() V10() V11() V12() integer ext-real positive non negative set
(Radix k) - 1 is V11() V12() integer ext-real set
1 - (Radix k) is V11() V12() integer ext-real set
{ b1 where b1 is V11() V12() integer ext-real Element of INT : ( b1 <= (Radix k) - 1 & (- (Radix k)) + 1 <= b1 ) } is set
- 2 is V11() V12() integer ext-real non positive set
(- 2) + 1 is V11() V12() integer ext-real set
- 1 is V11() V12() integer ext-real non positive set
(Radix k) + (- 1) is V11() V12() integer ext-real set
2 + (- 1) is V11() V12() integer ext-real set
r is Element of k -SD
m is V4() V5() V6() V10() V11() V12() integer ext-real non negative set
k is V4() V5() V6() V10() V11() V12() integer ext-real non negative set
k -SD is V1() Element of K6(INT)
Seg m is Element of K6(NAT)
n is V4() V5() V6() V10() V11() V12() integer ext-real non negative set
r is V15() V18( NAT ) V19(k -SD ) Function-like FinSequence-like FinSequence of k -SD
len r is V4() V5() V6() V10() V11() V12() integer ext-real non negative Element of NAT
dom r is Element of K6(NAT)
m -tuples_on (k -SD) is V1() functional FinSequence-membered FinSequenceSet of k -SD
i is V15() V18( NAT ) V19(k -SD ) Function-like V35(m) FinSequence-like FinSequence of k -SD
j is V4() V5() V6() V10() V11() V12() integer ext-real non negative set
DigA (i,j) is V11() V12() integer ext-real set
(j,n,k) is Element of k -SD
i . j is set
r is V15() V18( NAT ) V19(k -SD ) Function-like V35(m) FinSequence-like FinSequence of k -SD
i is V15() V18( NAT ) V19(k -SD ) Function-like V35(m) FinSequence-like FinSequence of k -SD
len r is V4() V5() V6() V10() V11() V12() integer ext-real non negative Element of NAT
dom r is Element of K6(NAT)
j is V4() V5() V6() V10() V11() V12() integer ext-real non negative set
r . j is set
DigA (r,j) is V11() V12() integer ext-real set
(j,n,k) is Element of k -SD
DigA (i,j) is V11() V12() integer ext-real set
i . j is set
len i is V4() V5() V6() V10() V11() V12() integer ext-real non negative Element of NAT
m is V4() V5() V6() V10() V11() V12() integer ext-real non negative set
Seg m is Element of K6(NAT)
n is V4() V5() V6() V10() V11() V12() integer ext-real non negative set
k is V4() V5() V6() V10() V11() V12() integer ext-real non negative set
(m,n,k) is V15() V18( NAT ) V19(k -SD ) Function-like V35(m) FinSequence-like FinSequence of k -SD
k -SD is V1() Element of K6(INT)
SDDec (m,n,k) is V11() V12() integer ext-real set
Fmin (m,n,k) is V15() V18( NAT ) V19(k -SD ) Function-like V35(m) FinSequence-like FinSequence of k -SD
SDMin (m,n,k) is V15() V18( NAT ) V19(k -SD ) Function-like V35(m) FinSequence-like FinSequence of k -SD
r is V4() V5() V6() V10() V11() V12() integer ext-real non negative set
DigA ((m,n,k),r) is V11() V12() integer ext-real set
DigA ((Fmin (m,n,k)),r) is V11() V12() integer ext-real set
DigA ((SDMin (m,n,k)),r) is V11() V12() integer ext-real set
FminDigit (n,k,r) is Element of k -SD
SDMinDigit (n,k,r) is Element of k -SD
(r,n,k) is Element of k -SD
FminDigit (n,k,r) is Element of k -SD
SDMinDigit (n,k,r) is Element of k -SD
(r,n,k) is Element of k -SD
FminDigit (n,k,r) is Element of k -SD
SDMinDigit (n,k,r) is Element of k -SD
Radix k is V4() V5() V6() V10() V11() V12() integer ext-real non negative Element of NAT
- (Radix k) is V11() V12() integer ext-real non positive set
(- (Radix k)) + 1 is V11() V12() integer ext-real set
(r,n,k) is Element of k -SD
DecSD (0,m,k) is V15() V18( NAT ) V19(k -SD ) Function-like V35(m) FinSequence-like FinSequence of k -SD
SDDec (DecSD (0,m,k)) is V11() V12() integer ext-real set
(SDDec (m,n,k)) + (SDDec (DecSD (0,m,k))) is V11() V12() integer ext-real set
SDDec (Fmin (m,n,k)) is V11() V12() integer ext-real set
SDDec (SDMin (m,n,k)) is V11() V12() integer ext-real set
(SDDec (Fmin (m,n,k))) + (SDDec (SDMin (m,n,k))) is V11() V12() integer ext-real set
(SDDec (m,n,k)) + 0 is V11() V12() integer ext-real set
SDMax (m,n,k) is V15() V18( NAT ) V19(k -SD ) Function-like V35(m) FinSequence-like FinSequence of k -SD
SDDec (SDMax (m,n,k)) is V11() V12() integer ext-real set
DecSD (1,m,k) is V15() V18( NAT ) V19(k -SD ) Function-like V35(m) FinSequence-like FinSequence of k -SD
SDDec (DecSD (1,m,k)) is V11() V12() integer ext-real set
(SDDec (SDMax (m,n,k))) + (SDDec (DecSD (1,m,k))) is V11() V12() integer ext-real set
((SDDec (SDMax (m,n,k))) + (SDDec (DecSD (1,m,k)))) + (SDDec (SDMin (m,n,k))) is V11() V12() integer ext-real set
(SDDec (SDMax (m,n,k))) + (SDDec (SDMin (m,n,k))) is V11() V12() integer ext-real set
((SDDec (SDMax (m,n,k))) + (SDDec (SDMin (m,n,k)))) + (SDDec (DecSD (1,m,k))) is V11() V12() integer ext-real set
(SDDec (DecSD (0,m,k))) + (SDDec (DecSD (1,m,k))) is V11() V12() integer ext-real set
0 + (SDDec (DecSD (1,m,k))) is V11() V12() integer ext-real set
n is V4() V5() V6() V10() V11() V12() integer ext-real non negative set
n + 2 is V1() V4() V5() V6() V10() V11() V12() integer ext-real positive non negative set
k is V4() V5() V6() V10() V11() V12() integer ext-real non negative set
k -SD is V1() Element of K6(INT)
m is V4() V5() V6() V10() V11() V12() integer ext-real non negative set
m + 2 is V1() V4() V5() V6() V10() V11() V12() integer ext-real positive non negative set
Seg (m + 2) is Element of K6(NAT)
k is V4() V5() V6() V10() V11() V12() integer ext-real non negative set
k -SD is V1() Element of K6(INT)
n is V4() V5() V6() V10() V11() V12() integer ext-real non negative set
r is V15() V18( NAT ) V19(k -SD ) Function-like V35(m + 2) FinSequence-like FinSequence of k -SD
(m,k,r) is V15() V18( NAT ) V19(k -SD ) Function-like V35(m + 2) FinSequence-like FinSequence of k -SD
DigA ((m,k,r),n) is V11() V12() integer ext-real set
SDDec (m,k,r) is V11() V12() integer ext-real set
((m + 2),n,k) is V15() V18( NAT ) V19(k -SD ) Function-like V35(m + 2) FinSequence-like FinSequence of k -SD
i is V4() V5() V6() V10() V11() V12() integer ext-real non negative set
DigA (((m + 2),n,k),i) is V11() V12() integer ext-real set
DigA ((m,k,r),i) is V11() V12() integer ext-real set
(i,n,k) is Element of k -SD
0 + 1 is V1() V4() V5() V6() V10() V11() V12() integer ext-real positive non negative set
(i,n,k) is Element of k -SD
(m,k,r) . i is set
(i,n,k) is Element of k -SD
Radix k is V4() V5() V6() V10() V11() V12() integer ext-real non negative Element of NAT
- (Radix k) is V11() V12() integer ext-real non positive set
(- (Radix k)) + 1 is V11() V12() integer ext-real set
SDDec ((m + 2),n,k) is V11() V12() integer ext-real set