:: RADIX_3 semantic presentation

REAL is non empty V28() V70() V71() V72() V76() set
NAT is V6() V28() V33() V34() V70() V71() V72() V73() V74() V75() V76() Element of K6(REAL)
K6(REAL) is V28() set
COMPLEX is non empty V28() V70() V76() set
NAT is V6() V28() V33() V34() V70() V71() V72() V73() V74() V75() V76() set
K6(NAT) is V28() set
K6(NAT) is V28() set
RAT is non empty V28() V70() V71() V72() V73() V76() set
INT is non empty V28() V70() V71() V72() V73() V74() V76() set
K7(COMPLEX,COMPLEX) is V28() V60() set
K6(K7(COMPLEX,COMPLEX)) is V28() set
K7(K7(COMPLEX,COMPLEX),COMPLEX) is V28() V60() set
K6(K7(K7(COMPLEX,COMPLEX),COMPLEX)) is V28() set
K7(REAL,REAL) is V28() V60() V61() V62() set
K6(K7(REAL,REAL)) is V28() set
K7(K7(REAL,REAL),REAL) is V28() V60() V61() V62() set
K6(K7(K7(REAL,REAL),REAL)) is V28() set
K7(RAT,RAT) is V19( RAT ) V28() V60() V61() V62() set
K6(K7(RAT,RAT)) is V28() set
K7(K7(RAT,RAT),RAT) is V19( RAT ) V28() V60() V61() V62() set
K6(K7(K7(RAT,RAT),RAT)) is V28() set
K7(INT,INT) is V19( RAT ) V19( INT ) V28() V60() V61() V62() set
K6(K7(INT,INT)) is V28() set
K7(K7(INT,INT),INT) is V19( RAT ) V19( INT ) V28() V60() V61() V62() set
K6(K7(K7(INT,INT),INT)) is V28() set
K7(NAT,NAT) is V19( RAT ) V19( INT ) V60() V61() V62() V63() set
K7(K7(NAT,NAT),NAT) is V19( RAT ) V19( INT ) V60() V61() V62() V63() set
K6(K7(K7(NAT,NAT),NAT)) is set
K297() is set
1 is non empty V6() V10() V11() V12() integer V28() V33() V43() ext-real positive non negative V70() V71() V72() V73() V74() V75() Element of NAT
K454() is V82() V110() L8()
the U1 of K454() is set
K6(INT) is V28() set
{} is empty V6() V33() V35( {} ) V70() V71() V72() V73() V74() V75() V76() set
0 is empty V6() V10() V11() V12() integer V28() V33() V35( {} ) V43() ext-real non positive non negative V70() V71() V72() V73() V74() V75() V76() Element of NAT
2 is non empty V6() V10() V11() V12() integer V28() V33() V43() ext-real positive non negative V70() V71() V72() V73() V74() V75() Element of NAT
n is V6() V10() V11() V12() integer V28() V33() ext-real non negative set
Radix n is V6() V10() V11() V12() integer V28() V33() V43() ext-real non negative V70() V71() V72() V73() V74() V75() Element of NAT
2 to_power n is V11() V12() ext-real set
n -' 1 is V6() V10() V11() V12() integer V28() V33() V43() ext-real non negative V70() V71() V72() V73() V74() V75() Element of NAT
Radix (n -' 1) is V6() V10() V11() V12() integer V28() V33() V43() ext-real non negative V70() V71() V72() V73() V74() V75() Element of NAT
2 to_power (n -' 1) is V11() V12() ext-real set
(Radix (n -' 1)) + (Radix (n -' 1)) is V6() V10() V11() V12() integer V28() V33() ext-real non negative set
(n -' 1) + 1 is non empty V6() V10() V11() V12() integer V28() V33() ext-real positive non negative set
2 to_power ((n -' 1) + 1) is V11() V12() ext-real set
2 to_power 1 is V11() V12() ext-real Element of REAL
(2 to_power 1) * (2 to_power (n -' 1)) is V11() V12() ext-real set
2 * (Radix (n -' 1)) is V6() V10() V11() V12() integer V28() V33() ext-real non negative set
n is V6() V10() V11() V12() integer V28() V33() ext-real non negative set
Radix n is V6() V10() V11() V12() integer V28() V33() V43() ext-real non negative V70() V71() V72() V73() V74() V75() Element of NAT
2 to_power n is V11() V12() ext-real set
n -' 1 is V6() V10() V11() V12() integer V28() V33() V43() ext-real non negative V70() V71() V72() V73() V74() V75() Element of NAT
Radix (n -' 1) is V6() V10() V11() V12() integer V28() V33() V43() ext-real non negative V70() V71() V72() V73() V74() V75() Element of NAT
2 to_power (n -' 1) is V11() V12() ext-real set
(Radix n) - (Radix (n -' 1)) is V11() V12() integer ext-real set
(Radix n) + 0 is V6() V10() V11() V12() integer V28() V33() ext-real non negative set
(Radix (n -' 1)) + (Radix (n -' 1)) is V6() V10() V11() V12() integer V28() V33() ext-real non negative set
n is V6() V10() V11() V12() integer V28() V33() ext-real non negative set
Radix n is V6() V10() V11() V12() integer V28() V33() V43() ext-real non negative V70() V71() V72() V73() V74() V75() Element of NAT
2 to_power n is V11() V12() ext-real set
- (Radix n) is V11() V12() integer ext-real non positive set
n -' 1 is V6() V10() V11() V12() integer V28() V33() V43() ext-real non negative V70() V71() V72() V73() V74() V75() Element of NAT
Radix (n -' 1) is V6() V10() V11() V12() integer V28() V33() V43() ext-real non negative V70() V71() V72() V73() V74() V75() Element of NAT
2 to_power (n -' 1) is V11() V12() ext-real set
(- (Radix n)) + (Radix (n -' 1)) is V11() V12() integer ext-real set
- (Radix (n -' 1)) is V11() V12() integer ext-real non positive set
(Radix n) - (Radix (n -' 1)) is V11() V12() integer ext-real set
- ((Radix n) - (Radix (n -' 1))) is V11() V12() integer ext-real set
n is V6() V10() V11() V12() integer V28() V33() ext-real non negative set
Radix n is V6() V10() V11() V12() integer V28() V33() V43() ext-real non negative V70() V71() V72() V73() V74() V75() Element of NAT
2 to_power n is V11() V12() ext-real set
k is V6() V10() V11() V12() integer V28() V33() ext-real non negative set
Radix k is V6() V10() V11() V12() integer V28() V33() V43() ext-real non negative V70() V71() V72() V73() V74() V75() Element of NAT
2 to_power k is V11() V12() ext-real set
k + 1 is non empty V6() V10() V11() V12() integer V28() V33() ext-real positive non negative set
Radix (k + 1) is V6() V10() V11() V12() integer V28() V33() V43() ext-real non negative V70() V71() V72() V73() V74() V75() Element of NAT
2 to_power (k + 1) is V11() V12() ext-real set
2 to_power 1 is V11() V12() ext-real Element of REAL
(2 to_power 1) * (2 to_power k) is V11() V12() ext-real set
2 * (Radix k) is V6() V10() V11() V12() integer V28() V33() ext-real non negative set
Radix 1 is V6() V10() V11() V12() integer V28() V33() V43() ext-real non negative V70() V71() V72() V73() V74() V75() Element of NAT
2 to_power 1 is V11() V12() ext-real set
n is V6() V10() V11() V12() integer V28() V33() ext-real non negative set
Seg n is V70() V71() V72() V73() V74() V75() Element of K6(NAT)
n + 1 is non empty V6() V10() V11() V12() integer V28() V33() ext-real positive non negative set
k is V6() V10() V11() V12() integer V28() V33() ext-real non negative set
x is V6() V10() V11() V12() integer V28() V33() ext-real non negative set
DecSD (k,(n + 1),x) is V15() V18( NAT ) V19(x -SD ) Function-like V35(n + 1) FinSequence-like V60() V61() V62() FinSequence of x -SD
x -SD is non empty V70() V71() V72() V73() V74() Element of K6(INT)
Radix x is V6() V10() V11() V12() integer V28() V33() V43() ext-real non negative V70() V71() V72() V73() V74() V75() Element of NAT
2 to_power x is V11() V12() ext-real set
(Radix x) - 1 is V11() V12() integer ext-real set
- (Radix x) is V11() V12() integer ext-real non positive set
(- (Radix x)) + 1 is V11() V12() integer ext-real set
{ b₁ where b₁ is V11() V12() integer V43() ext-real Element of INT : ( b₁ <= (Radix x) - 1 & (- (Radix x)) + 1 <= b₁ ) } is set
(Radix x) |^ n is V6() V10() V11() V12() integer V28() V33() ext-real non negative set
k mod ((Radix x) |^ n) is V6() V10() V11() V12() integer V28() V33() V43() ext-real non negative V70() V71() V72() V73() V74() V75() Element of NAT
DecSD ((k mod ((Radix x) |^ n)),n,x) is V15() V18( NAT ) V19(x -SD ) Function-like V35(n) FinSequence-like V60() V61() V62() FinSequence of x -SD
X is V6() V10() V11() V12() integer V28() V33() ext-real non negative set
DigA ((DecSD (k,(n + 1),x)),X) is V11() V12() integer ext-real set
DigA ((DecSD ((k mod ((Radix x) |^ n)),n,x)),X) is V11() V12() integer ext-real set
Seg (n + 1) is V70() V71() V72() V73() V74() V75() Element of K6(NAT)
(Radix x) |^ X is V6() V10() V11() V12() integer V28() V33() ext-real non negative set
CRY is V6() V10() V11() V12() integer V28() V33() ext-real non negative set
((Radix x) |^ X) * CRY is V6() V10() V11() V12() integer V28() V33() ext-real non negative set
DigitDC ((k mod ((Radix x) |^ n)),X,x) is V11() V12() integer V43() ext-real Element of x -SD
(k mod ((Radix x) |^ n)) mod ((Radix x) |^ X) is V6() V10() V11() V12() integer V28() V33() V43() ext-real non negative V70() V71() V72() V73() V74() V75() Element of NAT
X -' 1 is V6() V10() V11() V12() integer V28() V33() V43() ext-real non negative V70() V71() V72() V73() V74() V75() Element of NAT
(Radix x) |^ (X -' 1) is V6() V10() V11() V12() integer V28() V33() V43() ext-real non negative V70() V71() V72() V73() V74() V75() Element of NAT
((k mod ((Radix x) |^ n)) mod ((Radix x) |^ X)) div ((Radix x) |^ (X -' 1)) is V6() V10() V11() V12() integer V28() V33() V43() ext-real non negative V70() V71() V72() V73() V74() V75() Element of NAT
DigitDC (k,X,x) is V11() V12() integer V43() ext-real Element of x -SD
k mod ((Radix x) |^ X) is V6() V10() V11() V12() integer V28() V33() V43() ext-real non negative V70() V71() V72() V73() V74() V75() Element of NAT
(k mod ((Radix x) |^ X)) div ((Radix x) |^ (X -' 1)) is V6() V10() V11() V12() integer V28() V33() V43() ext-real non negative V70() V71() V72() V73() V74() V75() Element of NAT
n is V6() V10() V11() V12() integer V28() V33() ext-real non negative set
n -' 1 is V6() V10() V11() V12() integer V28() V33() V43() ext-real non negative V70() V71() V72() V73() V74() V75() Element of NAT
Radix (n -' 1) is V6() V10() V11() V12() integer V28() V33() V43() ext-real non negative V70() V71() V72() V73() V74() V75() Element of NAT
2 to_power (n -' 1) is V11() V12() ext-real set
- (Radix (n -' 1)) is V11() V12() integer ext-real non positive set
(Radix (n -' 1)) - 1 is V11() V12() integer ext-real set
{ b₁ where b₁ is V11() V12() integer V43() ext-real Element of INT : ( - (Radix (n -' 1)) <= b₁ & b₁ <= (Radix (n -' 1)) - 1 ) } is set
(- (Radix (n -' 1))) - 1 is non empty V11() V12() integer ext-real non positive negative set
{ b₁ where b₁ is V11() V12() integer V43() ext-real Element of INT : ( (- (Radix (n -' 1))) - 1 <= b₁ & b₁ <= Radix (n -' 1) ) } is set
n is V6() V10() V11() V12() integer V28() V33() ext-real non negative set
(n) is set
n -' 1 is V6() V10() V11() V12() integer V28() V33() V43() ext-real non negative V70() V71() V72() V73() V74() V75() Element of NAT
Radix (n -' 1) is V6() V10() V11() V12() integer V28() V33() V43() ext-real non negative V70() V71() V72() V73() V74() V75() Element of NAT
2 to_power (n -' 1) is V11() V12() ext-real set
- (Radix (n -' 1)) is V11() V12() integer ext-real non positive set
(- (Radix (n -' 1))) - 1 is non empty V11() V12() integer ext-real non positive negative set
{ b₁ where b₁ is V11() V12() integer V43() ext-real Element of INT : ( (- (Radix (n -' 1))) - 1 <= b₁ & b₁ <= Radix (n -' 1) ) } is set
k is V11() V12() integer ext-real set
x is V11() V12() integer V43() ext-real Element of INT
n is V6() V10() V11() V12() integer V28() V33() ext-real non negative set
(n) is set
n -' 1 is V6() V10() V11() V12() integer V28() V33() V43() ext-real non negative V70() V71() V72() V73() V74() V75() Element of NAT
Radix (n -' 1) is V6() V10() V11() V12() integer V28() V33() V43() ext-real non negative V70() V71() V72() V73() V74() V75() Element of NAT
2 to_power (n -' 1) is V11() V12() ext-real set
- (Radix (n -' 1)) is V11() V12() integer ext-real non positive set
(Radix (n -' 1)) - 1 is V11() V12() integer ext-real set
{ b₁ where b₁ is V11() V12() integer V43() ext-real Element of INT : ( - (Radix (n -' 1)) <= b₁ & b₁ <= (Radix (n -' 1)) - 1 ) } is set
(n) is set
(- (Radix (n -' 1))) - 1 is non empty V11() V12() integer ext-real non positive negative set
{ b₁ where b₁ is V11() V12() integer V43() ext-real Element of INT : ( (- (Radix (n -' 1))) - 1 <= b₁ & b₁ <= Radix (n -' 1) ) } is set
k is set
x is V11() V12() integer V43() ext-real Element of INT
(Radix (n -' 1)) + 0 is V6() V10() V11() V12() integer V28() V33() ext-real non negative set
(Radix (n -' 1)) + 1 is non empty V6() V10() V11() V12() integer V28() V33() ext-real positive non negative set
- ((Radix (n -' 1)) + 1) is V11() V12() integer ext-real non positive set
- 1 is V11() V12() integer ext-real non positive set
(Radix (n -' 1)) + (- 1) is V11() V12() integer ext-real set
n is V6() V10() V11() V12() integer V28() V33() ext-real non negative set
(n) is set
n -' 1 is V6() V10() V11() V12() integer V28() V33() V43() ext-real non negative V70() V71() V72() V73() V74() V75() Element of NAT
Radix (n -' 1) is V6() V10() V11() V12() integer V28() V33() V43() ext-real non negative V70() V71() V72() V73() V74() V75() Element of NAT
2 to_power (n -' 1) is V11() V12() ext-real set
- (Radix (n -' 1)) is V11() V12() integer ext-real non positive set
(Radix (n -' 1)) - 1 is V11() V12() integer ext-real set
{ b₁ where b₁ is V11() V12() integer V43() ext-real Element of INT : ( - (Radix (n -' 1)) <= b₁ & b₁ <= (Radix (n -' 1)) - 1 ) } is set
n + 1 is non empty V6() V10() V11() V12() integer V28() V33() ext-real positive non negative set
((n + 1)) is set
(n + 1) -' 1 is V6() V10() V11() V12() integer V28() V33() V43() ext-real non negative V70() V71() V72() V73() V74() V75() Element of NAT
Radix ((n + 1) -' 1) is V6() V10() V11() V12() integer V28() V33() V43() ext-real non negative V70() V71() V72() V73() V74() V75() Element of NAT
2 to_power ((n + 1) -' 1) is V11() V12() ext-real set
- (Radix ((n + 1) -' 1)) is V11() V12() integer ext-real non positive set
(Radix ((n + 1) -' 1)) - 1 is V11() V12() integer ext-real set
{ b₁ where b₁ is V11() V12() integer V43() ext-real Element of INT : ( - (Radix ((n + 1) -' 1)) <= b₁ & b₁ <= (Radix ((n + 1) -' 1)) - 1 ) } is set
k is set
x is V11() V12() integer V43() ext-real Element of INT
2 to_power n is V11() V12() ext-real set
Radix n is V6() V10() V11() V12() integer V28() V33() V43() ext-real non negative V70() V71() V72() V73() V74() V75() Element of NAT
(Radix n) - 1 is V11() V12() integer ext-real set
- (Radix n) is V11() V12() integer ext-real non positive set
n is V6() V10() V11() V12() integer V28() V33() ext-real non negative set
(n) is set
n -' 1 is V6() V10() V11() V12() integer V28() V33() V43() ext-real non negative V70() V71() V72() V73() V74() V75() Element of NAT
Radix (n -' 1) is V6() V10() V11() V12() integer V28() V33() V43() ext-real non negative V70() V71() V72() V73() V74() V75() Element of NAT
2 to_power (n -' 1) is V11() V12() ext-real set
- (Radix (n -' 1)) is V11() V12() integer ext-real non positive set
(- (Radix (n -' 1))) - 1 is non empty V11() V12() integer ext-real non positive negative set
{ b₁ where b₁ is V11() V12() integer V43() ext-real Element of INT : ( (- (Radix (n -' 1))) - 1 <= b₁ & b₁ <= Radix (n -' 1) ) } is set
n -SD is non empty V70() V71() V72() V73() V74() Element of K6(INT)
Radix n is V6() V10() V11() V12() integer V28() V33() V43() ext-real non negative V70() V71() V72() V73() V74() V75() Element of NAT
2 to_power n is V11() V12() ext-real set
(Radix n) - 1 is V11() V12() integer ext-real set
- (Radix n) is V11() V12() integer ext-real non positive set
(- (Radix n)) + 1 is V11() V12() integer ext-real set
{ b₁ where b₁ is V11() V12() integer V43() ext-real Element of INT : ( b₁ <= (Radix n) - 1 & (- (Radix n)) + 1 <= b₁ ) } is set
1 + 1 is non empty V6() V10() V11() V12() integer V28() V33() ext-real positive non negative set
- 1 is V11() V12() integer ext-real non positive set
(Radix n) + (- (Radix (n -' 1))) is V11() V12() integer ext-real set
(Radix n) + (- 1) is V11() V12() integer ext-real set
k is set
x is V11() V12() integer V43() ext-real Element of INT
(Radix (n -' 1)) + 2 is non empty V6() V10() V11() V12() integer V28() V33() ext-real positive non negative set
(Radix (n -' 1)) + (Radix (n -' 1)) is V6() V10() V11() V12() integer V28() V33() ext-real non negative set
(Radix (n -' 1)) + 1 is non empty V6() V10() V11() V12() integer V28() V33() ext-real positive non negative set
((Radix (n -' 1)) + 1) + 1 is non empty V6() V10() V11() V12() integer V28() V33() ext-real positive non negative set
(Radix n) + 0 is V6() V10() V11() V12() integer V28() V33() ext-real non negative set
((Radix (n -' 1)) + 1) - 0 is non empty V11() V12() integer ext-real positive non negative set
- ((Radix n) - 1) is V11() V12() integer ext-real set
- ((Radix (n -' 1)) + 1) is V11() V12() integer ext-real non positive set
(0) is set
0 -' 1 is V6() V10() V11() V12() integer V28() V33() V43() ext-real non negative V70() V71() V72() V73() V74() V75() Element of NAT
Radix (0 -' 1) is V6() V10() V11() V12() integer V28() V33() V43() ext-real non negative V70() V71() V72() V73() V74() V75() Element of NAT
2 to_power (0 -' 1) is V11() V12() ext-real set
- (Radix (0 -' 1)) is V11() V12() integer ext-real non positive set
(Radix (0 -' 1)) - 1 is V11() V12() integer ext-real set
{ b₁ where b₁ is V11() V12() integer V43() ext-real Element of INT : ( - (Radix (0 -' 1)) <= b₁ & b₁ <= (Radix (0 -' 1)) - 1 ) } is set
0 - 1 is non empty V11() V12() integer ext-real non positive negative set
n is V11() V12() integer ext-real set
n is V6() V10() V11() V12() integer V28() V33() ext-real non negative set
(n) is set
n -' 1 is V6() V10() V11() V12() integer V28() V33() V43() ext-real non negative V70() V71() V72() V73() V74() V75() Element of NAT
Radix (n -' 1) is V6() V10() V11() V12() integer V28() V33() V43() ext-real non negative V70() V71() V72() V73() V74() V75() Element of NAT
2 to_power (n -' 1) is V11() V12() ext-real set
- (Radix (n -' 1)) is V11() V12() integer ext-real non positive set
(Radix (n -' 1)) - 1 is V11() V12() integer ext-real set
{ b₁ where b₁ is V11() V12() integer V43() ext-real Element of INT : ( - (Radix (n -' 1)) <= b₁ & b₁ <= (Radix (n -' 1)) - 1 ) } is set
k is V6() V10() V11() V12() integer V28() V33() ext-real non negative set
(k) is set
k -' 1 is V6() V10() V11() V12() integer V28() V33() V43() ext-real non negative V70() V71() V72() V73() V74() V75() Element of NAT
Radix (k -' 1) is V6() V10() V11() V12() integer V28() V33() V43() ext-real non negative V70() V71() V72() V73() V74() V75() Element of NAT
2 to_power (k -' 1) is V11() V12() ext-real set
- (Radix (k -' 1)) is V11() V12() integer ext-real non positive set
(Radix (k -' 1)) - 1 is V11() V12() integer ext-real set
{ b₁ where b₁ is V11() V12() integer V43() ext-real Element of INT : ( - (Radix (k -' 1)) <= b₁ & b₁ <= (Radix (k -' 1)) - 1 ) } is set
k + 1 is non empty V6() V10() V11() V12() integer V28() V33() ext-real positive non negative set
((k + 1)) is set
(k + 1) -' 1 is V6() V10() V11() V12() integer V28() V33() V43() ext-real non negative V70() V71() V72() V73() V74() V75() Element of NAT
Radix ((k + 1) -' 1) is V6() V10() V11() V12() integer V28() V33() V43() ext-real non negative V70() V71() V72() V73() V74() V75() Element of NAT
2 to_power ((k + 1) -' 1) is V11() V12() ext-real set
- (Radix ((k + 1) -' 1)) is V11() V12() integer ext-real non positive set
(Radix ((k + 1) -' 1)) - 1 is V11() V12() integer ext-real set
{ b₁ where b₁ is V11() V12() integer V43() ext-real Element of INT : ( - (Radix ((k + 1) -' 1)) <= b₁ & b₁ <= (Radix ((k + 1) -' 1)) - 1 ) } is set
n is V6() V10() V11() V12() integer V28() V33() ext-real non negative set
(n) is set
n -' 1 is V6() V10() V11() V12() integer V28() V33() V43() ext-real non negative V70() V71() V72() V73() V74() V75() Element of NAT
Radix (n -' 1) is V6() V10() V11() V12() integer V28() V33() V43() ext-real non negative V70() V71() V72() V73() V74() V75() Element of NAT
2 to_power (n -' 1) is V11() V12() ext-real set
- (Radix (n -' 1)) is V11() V12() integer ext-real non positive set
(- (Radix (n -' 1))) - 1 is non empty V11() V12() integer ext-real non positive negative set
{ b₁ where b₁ is V11() V12() integer V43() ext-real Element of INT : ( (- (Radix (n -' 1))) - 1 <= b₁ & b₁ <= Radix (n -' 1) ) } is set
(n) is set
(Radix (n -' 1)) - 1 is V11() V12() integer ext-real set
{ b₁ where b₁ is V11() V12() integer V43() ext-real Element of INT : ( - (Radix (n -' 1)) <= b₁ & b₁ <= (Radix (n -' 1)) - 1 ) } is set
n is V6() V10() V11() V12() integer V28() V33() ext-real non negative set
(n) is set
n -' 1 is V6() V10() V11() V12() integer V28() V33() V43() ext-real non negative V70() V71() V72() V73() V74() V75() Element of NAT
Radix (n -' 1) is V6() V10() V11() V12() integer V28() V33() V43() ext-real non negative V70() V71() V72() V73() V74() V75() Element of NAT
2 to_power (n -' 1) is V11() V12() ext-real set
- (Radix (n -' 1)) is V11() V12() integer ext-real non positive set
(- (Radix (n -' 1))) - 1 is non empty V11() V12() integer ext-real non positive negative set
{ b₁ where b₁ is V11() V12() integer V43() ext-real Element of INT : ( (- (Radix (n -' 1))) - 1 <= b₁ & b₁ <= Radix (n -' 1) ) } is set
k is set
x is V11() V12() integer V43() ext-real Element of INT
n is V6() V10() V11() V12() integer V28() V33() ext-real non negative set
(n) is set
n -' 1 is V6() V10() V11() V12() integer V28() V33() V43() ext-real non negative V70() V71() V72() V73() V74() V75() Element of NAT
Radix (n -' 1) is V6() V10() V11() V12() integer V28() V33() V43() ext-real non negative V70() V71() V72() V73() V74() V75() Element of NAT
2 to_power (n -' 1) is V11() V12() ext-real set
- (Radix (n -' 1)) is V11() V12() integer ext-real non positive set
(- (Radix (n -' 1))) - 1 is non empty V11() V12() integer ext-real non positive negative set
{ b₁ where b₁ is V11() V12() integer V43() ext-real Element of INT : ( (- (Radix (n -' 1))) - 1 <= b₁ & b₁ <= Radix (n -' 1) ) } is set
k is set
n is V6() V10() V11() V12() integer V28() V33() ext-real non negative set
(n) is set
n -' 1 is V6() V10() V11() V12() integer V28() V33() V43() ext-real non negative V70() V71() V72() V73() V74() V75() Element of NAT
Radix (n -' 1) is V6() V10() V11() V12() integer V28() V33() V43() ext-real non negative V70() V71() V72() V73() V74() V75() Element of NAT
2 to_power (n -' 1) is V11() V12() ext-real set
- (Radix (n -' 1)) is V11() V12() integer ext-real non positive set
(Radix (n -' 1)) - 1 is V11() V12() integer ext-real set
{ b₁ where b₁ is V11() V12() integer V43() ext-real Element of INT : ( - (Radix (n -' 1)) <= b₁ & b₁ <= (Radix (n -' 1)) - 1 ) } is set
k is set
(n) is set
(- (Radix (n -' 1))) - 1 is non empty V11() V12() integer ext-real non positive negative set
{ b₁ where b₁ is V11() V12() integer V43() ext-real Element of INT : ( (- (Radix (n -' 1))) - 1 <= b₁ & b₁ <= Radix (n -' 1) ) } is set
n is V6() V10() V11() V12() integer V28() V33() ext-real non negative set
(n) is set
n -' 1 is V6() V10() V11() V12() integer V28() V33() V43() ext-real non negative V70() V71() V72() V73() V74() V75() Element of NAT
Radix (n -' 1) is V6() V10() V11() V12() integer V28() V33() V43() ext-real non negative V70() V71() V72() V73() V74() V75() Element of NAT
2 to_power (n -' 1) is V11() V12() ext-real set
- (Radix (n -' 1)) is V11() V12() integer ext-real non positive set
(Radix (n -' 1)) - 1 is V11() V12() integer ext-real set
{ b₁ where b₁ is V11() V12() integer V43() ext-real Element of INT : ( - (Radix (n -' 1)) <= b₁ & b₁ <= (Radix (n -' 1)) - 1 ) } is set
(n) is set
(- (Radix (n -' 1))) - 1 is non empty V11() V12() integer ext-real non positive negative set
{ b₁ where b₁ is V11() V12() integer V43() ext-real Element of INT : ( (- (Radix (n -' 1))) - 1 <= b₁ & b₁ <= Radix (n -' 1) ) } is set
n is V6() V10() V11() V12() integer V28() V33() ext-real non negative set
(n) is non empty set
n -' 1 is V6() V10() V11() V12() integer V28() V33() V43() ext-real non negative V70() V71() V72() V73() V74() V75() Element of NAT
Radix (n -' 1) is V6() V10() V11() V12() integer V28() V33() V43() ext-real non negative V70() V71() V72() V73() V74() V75() Element of NAT
2 to_power (n -' 1) is V11() V12() ext-real set
- (Radix (n -' 1)) is V11() V12() integer ext-real non positive set
(Radix (n -' 1)) - 1 is V11() V12() integer ext-real set
{ b₁ where b₁ is V11() V12() integer V43() ext-real Element of INT : ( - (Radix (n -' 1)) <= b₁ & b₁ <= (Radix (n -' 1)) - 1 ) } is set
n is V6() V10() V11() V12() integer V28() V33() ext-real non negative set
(n) is non empty set
n -' 1 is V6() V10() V11() V12() integer V28() V33() V43() ext-real non negative V70() V71() V72() V73() V74() V75() Element of NAT
Radix (n -' 1) is V6() V10() V11() V12() integer V28() V33() V43() ext-real non negative V70() V71() V72() V73() V74() V75() Element of NAT
2 to_power (n -' 1) is V11() V12() ext-real set
- (Radix (n -' 1)) is V11() V12() integer ext-real non positive set
(- (Radix (n -' 1))) - 1 is non empty V11() V12() integer ext-real non positive negative set
{ b₁ where b₁ is V11() V12() integer V43() ext-real Element of INT : ( (- (Radix (n -' 1))) - 1 <= b₁ & b₁ <= Radix (n -' 1) ) } is set
n is V6() V10() V11() V12() integer V28() V33() ext-real non negative set
k is V6() V10() V11() V12() integer V28() V33() ext-real non negative set
Seg k is V70() V71() V72() V73() V74() V75() Element of K6(NAT)
x is V6() V10() V11() V12() integer V28() V33() ext-real non negative set
(x) is non empty V70() V71() V72() V73() V74() Element of K6(INT)
x -' 1 is V6() V10() V11() V12() integer V28() V33() V43() ext-real non negative V70() V71() V72() V73() V74() V75() Element of NAT
Radix (x -' 1) is V6() V10() V11() V12() integer V28() V33() V43() ext-real non negative V70() V71() V72() V73() V74() V75() Element of NAT
2 to_power (x -' 1) is V11() V12() ext-real set
- (Radix (x -' 1)) is V11() V12() integer ext-real non positive set
(- (Radix (x -' 1))) - 1 is non empty V11() V12() integer ext-real non positive negative set
{ b₁ where b₁ is V11() V12() integer V43() ext-real Element of INT : ( (- (Radix (x -' 1))) - 1 <= b₁ & b₁ <= Radix (x -' 1) ) } is set
X is V15() V18( NAT ) V19((x)) Function-like V35(k) FinSequence-like V60() V61() V62() FinSequence of (x)
X . n is V11() V12() ext-real set
len X is V6() V10() V11() V12() integer V28() V33() V43() ext-real non negative V70() V71() V72() V73() V74() V75() Element of NAT
dom X is V35(k) V70() V71() V72() V73() V74() V75() Element of K6(NAT)
rng X is V70() V71() V72() set
k is V6() V10() V11() V12() integer V28() V33() ext-real non negative set
k -' 1 is V6() V10() V11() V12() integer V28() V33() V43() ext-real non negative V70() V71() V72() V73() V74() V75() Element of NAT
Radix (k -' 1) is V6() V10() V11() V12() integer V28() V33() V43() ext-real non negative V70() V71() V72() V73() V74() V75() Element of NAT
2 to_power (k -' 1) is V11() V12() ext-real set
n is V11() V12() integer ext-real set
- (Radix (k -' 1)) is V11() V12() integer ext-real non positive set
- 1 is V11() V12() integer ext-real non positive set
x is V11() V12() integer ext-real set
n is V11() V12() integer ext-real set
k is V6() V10() V11() V12() integer V28() V33() ext-real non negative set
Radix k is V6() V10() V11() V12() integer V28() V33() V43() ext-real non negative V70() V71() V72() V73() V74() V75() Element of NAT
2 to_power k is V11() V12() ext-real set
(n,k) is V11() V12() integer ext-real set
(Radix k) * (n,k) is V11() V12() integer ext-real set
n - ((Radix k) * (n,k)) is V11() V12() integer ext-real set
n is V11() V12() integer ext-real set
k is V6() V10() V11() V12() integer V28() V33() ext-real non negative set
(n,k) is V11() V12() integer ext-real set
k -' 1 is V6() V10() V11() V12() integer V28() V33() V43() ext-real non negative V70() V71() V72() V73() V74() V75() Element of NAT
Radix (k -' 1) is V6() V10() V11() V12() integer V28() V33() V43() ext-real non negative V70() V71() V72() V73() V74() V75() Element of NAT
2 to_power (k -' 1) is V11() V12() ext-real set
- (Radix (k -' 1)) is V11() V12() integer ext-real non positive set
k -' 1 is V6() V10() V11() V12() integer V28() V33() V43() ext-real non negative V70() V71() V72() V73() V74() V75() Element of NAT
Radix (k -' 1) is V6() V10() V11() V12() integer V28() V33() V43() ext-real non negative V70() V71() V72() V73() V74() V75() Element of NAT
2 to_power (k -' 1) is V11() V12() ext-real set
- (Radix (k -' 1)) is V11() V12() integer ext-real non positive set
k -' 1 is V6() V10() V11() V12() integer V28() V33() V43() ext-real non negative V70() V71() V72() V73() V74() V75() Element of NAT
Radix (k -' 1) is V6() V10() V11() V12() integer V28() V33() V43() ext-real non negative V70() V71() V72() V73() V74() V75() Element of NAT
2 to_power (k -' 1) is V11() V12() ext-real set
k -' 1 is V6() V10() V11() V12() integer V28() V33() V43() ext-real non negative V70() V71() V72() V73() V74() V75() Element of NAT
Radix (k -' 1) is V6() V10() V11() V12() integer V28() V33() V43() ext-real non negative V70() V71() V72() V73() V74() V75() Element of NAT
2 to_power (k -' 1) is V11() V12() ext-real set
- (Radix (k -' 1)) is V11() V12() integer ext-real non positive set
n is V6() V10() V11() V12() integer V28() V33() ext-real non negative set
n -SD is non empty V70() V71() V72() V73() V74() Element of K6(INT)
Radix n is V6() V10() V11() V12() integer V28() V33() V43() ext-real non negative V70() V71() V72() V73() V74() V75() Element of NAT
2 to_power n is V11() V12() ext-real set
(Radix n) - 1 is V11() V12() integer ext-real set
- (Radix n) is V11() V12() integer ext-real non positive set
(- (Radix n)) + 1 is V11() V12() integer ext-real set
{ b₁ where b₁ is V11() V12() integer V43() ext-real Element of INT : ( b₁ <= (Radix n) - 1 & (- (Radix n)) + 1 <= b₁ ) } is set
n -' 1 is V6() V10() V11() V12() integer V28() V33() V43() ext-real non negative V70() V71() V72() V73() V74() V75() Element of NAT
Radix (n -' 1) is V6() V10() V11() V12() integer V28() V33() V43() ext-real non negative V70() V71() V72() V73() V74() V75() Element of NAT
2 to_power (n -' 1) is V11() V12() ext-real set
- (Radix (n -' 1)) is V11() V12() integer ext-real non positive set
(Radix (n -' 1)) - 1 is V11() V12() integer ext-real set
k is V11() V12() integer ext-real set
(k,n) is V11() V12() integer ext-real set
(k,n) is V11() V12() integer ext-real set
(Radix n) * (k,n) is V11() V12() integer ext-real set
k - ((Radix n) * (k,n)) is V11() V12() integer ext-real set
k + 1 is V11() V12() integer ext-real set
(- (Radix (n -' 1))) - 1 is non empty V11() V12() integer ext-real non positive negative set
k + (Radix n) is V11() V12() integer ext-real set
(Radix n) + ((- (Radix (n -' 1))) - 1) is V11() V12() integer ext-real set
(Radix n) - (Radix (n -' 1)) is V11() V12() integer ext-real set
((Radix n) - (Radix (n -' 1))) - 1 is V11() V12() integer ext-real set
k + 1 is V11() V12() integer ext-real set
(Radix n) + (- 1) is V11() V12() integer ext-real set
0 - 1 is non empty V11() V12() integer ext-real non positive negative set
k - (Radix n) is V11() V12() integer ext-real set
(Radix (n -' 1)) + (- (Radix n)) is V11() V12() integer ext-real set
k + (- (Radix n)) is V11() V12() integer ext-real set
n is V11() V12() integer ext-real set
k is V6() V10() V11() V12() integer V28() V33() ext-real non negative set
(n,k) is V11() V12() integer ext-real set
(k) is non empty V70() V71() V72() V73() V74() Element of K6(INT)
k -' 1 is V6() V10() V11() V12() integer V28() V33() V43() ext-real non negative V70() V71() V72() V73() V74() V75() Element of NAT
Radix (k -' 1) is V6() V10() V11() V12() integer V28() V33() V43() ext-real non negative V70() V71() V72() V73() V74() V75() Element of NAT
2 to_power (k -' 1) is V11() V12() ext-real set
- (Radix (k -' 1)) is V11() V12() integer ext-real non positive set
(Radix (k -' 1)) - 1 is V11() V12() integer ext-real set
{ b₁ where b₁ is V11() V12() integer V43() ext-real Element of INT : ( - (Radix (k -' 1)) <= b₁ & b₁ <= (Radix (k -' 1)) - 1 ) } is set
k - 1 is V11() V12() integer ext-real set
1 - 1 is V11() V12() integer ext-real set
n is V6() V10() V11() V12() integer V28() V33() ext-real non negative set
n -SD is non empty V70() V71() V72() V73() V74() Element of K6(INT)
Radix n is V6() V10() V11() V12() integer V28() V33() V43() ext-real non negative V70() V71() V72() V73() V74() V75() Element of NAT
2 to_power n is V11() V12() ext-real set
(Radix n) - 1 is V11() V12() integer ext-real set
- (Radix n) is V11() V12() integer ext-real non positive set
(- (Radix n)) + 1 is V11() V12() integer ext-real set
{ b₁ where b₁ is V11() V12() integer V43() ext-real Element of INT : ( b₁ <= (Radix n) - 1 & (- (Radix n)) + 1 <= b₁ ) } is set
(n) is non empty V70() V71() V72() V73() V74() Element of K6(INT)
n -' 1 is V6() V10() V11() V12() integer V28() V33() V43() ext-real non negative V70() V71() V72() V73() V74() V75() Element of NAT
Radix (n -' 1) is V6() V10() V11() V12() integer V28() V33() V43() ext-real non negative V70() V71() V72() V73() V74() V75() Element of NAT
2 to_power (n -' 1) is V11() V12() ext-real set
- (Radix (n -' 1)) is V11() V12() integer ext-real non positive set
(- (Radix (n -' 1))) - 1 is non empty V11() V12() integer ext-real non positive negative set
{ b₁ where b₁ is V11() V12() integer V43() ext-real Element of INT : ( (- (Radix (n -' 1))) - 1 <= b₁ & b₁ <= Radix (n -' 1) ) } is set
k is V11() V12() integer ext-real set
(k,n) is V11() V12() integer ext-real set
(k,n) is V11() V12() integer ext-real set
(Radix n) * (k,n) is V11() V12() integer ext-real set
k - ((Radix n) * (k,n)) is V11() V12() integer ext-real set
x is V11() V12() integer ext-real set
(x,n) is V11() V12() integer ext-real set
(k,n) + (x,n) is V11() V12() integer ext-real set
(- (Radix (n -' 1))) + (- 1) is V11() V12() integer ext-real non positive set
(Radix (n -' 1)) - 1 is V11() V12() integer ext-real set
((Radix (n -' 1)) - 1) + 1 is V11() V12() integer ext-real set
n is V6() V10() V11() V12() integer V28() V33() ext-real non negative set
(0,n) is V11() V12() integer ext-real set
n -' 1 is V6() V10() V11() V12() integer V28() V33() V43() ext-real non negative V70() V71() V72() V73() V74() V75() Element of NAT
Radix (n -' 1) is V6() V10() V11() V12() integer V28() V33() V43() ext-real non negative V70() V71() V72() V73() V74() V75() Element of NAT
2 to_power (n -' 1) is V11() V12() ext-real set
- (Radix (n -' 1)) is V11() V12() integer ext-real non positive set
0 - 0 is empty V6() V11() V12() integer V33() V35( {} ) ext-real non positive non negative V70() V71() V72() V73() V74() V75() V76() set
x is V6() V10() V11() V12() integer V28() V33() ext-real non negative set
k is V6() V10() V11() V12() integer V28() V33() ext-real non negative set
(k) is non empty V70() V71() V72() V73() V74() Element of K6(INT)
k -' 1 is V6() V10() V11() V12() integer V28() V33() V43() ext-real non negative V70() V71() V72() V73() V74() V75() Element of NAT
Radix (k -' 1) is V6() V10() V11() V12() integer V28() V33() V43() ext-real non negative V70() V71() V72() V73() V74() V75() Element of NAT
2 to_power (k -' 1) is V11() V12() ext-real set
- (Radix (k -' 1)) is V11() V12() integer ext-real non positive set
(- (Radix (k -' 1))) - 1 is non empty V11() V12() integer ext-real non positive negative set
{ b₁ where b₁ is V11() V12() integer V43() ext-real Element of INT : ( (- (Radix (k -' 1))) - 1 <= b₁ & b₁ <= Radix (k -' 1) ) } is set
n is V6() V10() V11() V12() integer V28() V33() ext-real non negative set
Seg x is V70() V71() V72() V73() V74() V75() Element of K6(NAT)
X is V15() V18( NAT ) V19((k)) Function-like V35(x) FinSequence-like V60() V61() V62() FinSequence of (k)
X . n is V11() V12() ext-real set
CRY is V11() V12() integer ext-real set
x is V6() V10() V11() V12() integer V28() V33() ext-real non negative set
k is V6() V10() V11() V12() integer V28() V33() ext-real non negative set
k -SD is non empty V70() V71() V72() V73() V74() Element of K6(INT)
Radix k is V6() V10() V11() V12() integer V28() V33() V43() ext-real non negative V70() V71() V72() V73() V74() V75() Element of NAT
2 to_power k is V11() V12() ext-real set
(Radix k) - 1 is V11() V12() integer ext-real set
- (Radix k) is V11() V12() integer ext-real non positive set
(- (Radix k)) + 1 is V11() V12() integer ext-real set
{ b₁ where b₁ is V11() V12() integer V43() ext-real Element of INT : ( b₁ <= (Radix k) - 1 & (- (Radix k)) + 1 <= b₁ ) } is set
n is V6() V10() V11() V12() integer V28() V33() ext-real non negative set
Seg x is V70() V71() V72() V73() V74() V75() Element of K6(NAT)
X is V15() V18( NAT ) V19(k -SD ) Function-like V35(x) FinSequence-like V60() V61() V62() FinSequence of k -SD
DigA (X,n) is V11() V12() integer ext-real set
((DigA (X,n)),k) is V11() V12() integer ext-real set
((DigA (X,n)),k) is V11() V12() integer ext-real set
(Radix k) * ((DigA (X,n)),k) is V11() V12() integer ext-real set
(DigA (X,n)) - ((Radix k) * ((DigA (X,n)),k)) is V11() V12() integer ext-real set
n -' 1 is V6() V10() V11() V12() integer V28() V33() V43() ext-real non negative V70() V71() V72() V73() V74() V75() Element of NAT
DigA (X,(n -' 1)) is V11() V12() integer ext-real set
((DigA (X,(n -' 1))),k) is V11() V12() integer ext-real set
((DigA (X,n)),k) + ((DigA (X,(n -' 1))),k) is V11() V12() integer ext-real set
x + 1 is non empty V6() V10() V11() V12() integer V28() V33() ext-real positive non negative set
CRY is V11() V12() integer ext-real set
n is V6() V10() V11() V12() integer V28() V33() ext-real non negative set
n -SD is non empty V70() V71() V72() V73() V74() Element of K6(INT)
Radix n is V6() V10() V11() V12() integer V28() V33() V43() ext-real non negative V70() V71() V72() V73() V74() V75() Element of NAT
2 to_power n is V11() V12() ext-real set
(Radix n) - 1 is V11() V12() integer ext-real set
- (Radix n) is V11() V12() integer ext-real non positive set
(- (Radix n)) + 1 is V11() V12() integer ext-real set
{ b₁ where b₁ is V11() V12() integer V43() ext-real Element of INT : ( b₁ <= (Radix n) - 1 & (- (Radix n)) + 1 <= b₁ ) } is set
(n) is non empty V70() V71() V72() V73() V74() Element of K6(INT)
n -' 1 is V6() V10() V11() V12() integer V28() V33() V43() ext-real non negative V70() V71() V72() V73() V74() V75() Element of NAT
Radix (n -' 1) is V6() V10() V11() V12() integer V28() V33() V43() ext-real non negative V70() V71() V72() V73() V74() V75() Element of NAT
2 to_power (n -' 1) is V11() V12() ext-real set
- (Radix (n -' 1)) is V11() V12() integer ext-real non positive set
(- (Radix (n -' 1))) - 1 is non empty V11() V12() integer ext-real non positive negative set
{ b₁ where b₁ is V11() V12() integer V43() ext-real Element of INT : ( (- (Radix (n -' 1))) - 1 <= b₁ & b₁ <= Radix (n -' 1) ) } is set
k is V6() V10() V11() V12() integer V28() V33() ext-real non negative set
x is V6() V10() V11() V12() integer V28() V33() ext-real non negative set
x + 1 is non empty V6() V10() V11() V12() integer V28() V33() ext-real positive non negative set
Seg (x + 1) is V70() V71() V72() V73() V74() V75() Element of K6(NAT)
X is V15() V18( NAT ) V19(n -SD ) Function-like V35(x) FinSequence-like V60() V61() V62() FinSequence of n -SD
(k,n,x,X) is V11() V12() integer ext-real set
DigA (X,k) is V11() V12() integer ext-real set
((DigA (X,k)),n) is V11() V12() integer ext-real set
((DigA (X,k)),n) is V11() V12() integer ext-real set
(Radix n) * ((DigA (X,k)),n) is V11() V12() integer ext-real set
(DigA (X,k)) - ((Radix n) * ((DigA (X,k)),n)) is V11() V12() integer ext-real set
k -' 1 is V6() V10() V11() V12() integer V28() V33() V43() ext-real non negative V70() V71() V72() V73() V74() V75() Element of NAT
DigA (X,(k -' 1)) is V11() V12() integer ext-real set
((DigA (X,(k -' 1))),n) is V11() V12() integer ext-real set
((DigA (X,k)),n) + ((DigA (X,(k -' 1))),n) is V11() V12() integer ext-real set
Seg x is V70() V71() V72() V73() V74() V75() Element of K6(NAT)
(n) is non empty V70() V71() V72() V73() V74() Element of K6(INT)
(Radix (n -' 1)) - 1 is V11() V12() integer ext-real set
{ b₁ where b₁ is V11() V12() integer V43() ext-real Element of INT : ( - (Radix (n -' 1)) <= b₁ & b₁ <= (Radix (n -' 1)) - 1 ) } is set
Seg x is V70() V71() V72() V73() V74() V75() Element of K6(NAT)
x is V6() V10() V11() V12() integer V28() V33() ext-real non negative set
k is V6() V10() V11() V12() integer V28() V33() ext-real non negative set
k -SD is non empty V70() V71() V72() V73() V74() Element of K6(INT)
Radix k is V6() V10() V11() V12() integer V28() V33() V43() ext-real non negative V70() V71() V72() V73() V74() V75() Element of NAT
2 to_power k is V11() V12() ext-real set
(Radix k) - 1 is V11() V12() integer ext-real set
- (Radix k) is V11() V12() integer ext-real non positive set
(- (Radix k)) + 1 is V11() V12() integer ext-real set
{ b₁ where b₁ is V11() V12() integer V43() ext-real Element of INT : ( b₁ <= (Radix k) - 1 & (- (Radix k)) + 1 <= b₁ ) } is set
n is V6() V10() V11() V12() integer V28() V33() ext-real non negative set
x + 1 is non empty V6() V10() V11() V12() integer V28() V33() ext-real positive non negative set
Seg (x + 1) is V70() V71() V72() V73() V74() V75() Element of K6(NAT)
X is V15() V18( NAT ) V19(k -SD ) Function-like V35(x) FinSequence-like V60() V61() V62() FinSequence of k -SD
(n,k,x,X) is V11() V12() integer ext-real set
(k) is non empty V70() V71() V72() V73() V74() Element of K6(INT)
k -' 1 is V6() V10() V11() V12() integer V28() V33() V43() ext-real non negative V70() V71() V72() V73() V74() V75() Element of NAT
Radix (k -' 1) is V6() V10() V11() V12() integer V28() V33() V43() ext-real non negative V70() V71() V72() V73() V74() V75() Element of NAT
2 to_power (k -' 1) is V11() V12() ext-real set
- (Radix (k -' 1)) is V11() V12() integer ext-real non positive set
(- (Radix (k -' 1))) - 1 is non empty V11() V12() integer ext-real non positive negative set
{ b₁ where b₁ is V11() V12() integer V43() ext-real Element of INT : ( (- (Radix (k -' 1))) - 1 <= b₁ & b₁ <= Radix (k -' 1) ) } is set
n is V6() V10() V11() V12() integer V28() V33() ext-real non negative set
k is V6() V10() V11() V12() integer V28() V33() ext-real non negative set
k -SD is non empty V70() V71() V72() V73() V74() Element of K6(INT)
Radix k is V6() V10() V11() V12() integer V28() V33() V43() ext-real non negative V70() V71() V72() V73() V74() V75() Element of NAT
2 to_power k is V11() V12() ext-real set
(Radix k) - 1 is V11() V12() integer ext-real set
- (Radix k) is V11() V12() integer ext-real non positive set
(- (Radix k)) + 1 is V11() V12() integer ext-real set
{ b₁ where b₁ is V11() V12() integer V43() ext-real Element of INT : ( b₁ <= (Radix k) - 1 & (- (Radix k)) + 1 <= b₁ ) } is set
n + 1 is non empty V6() V10() V11() V12() integer V28() V33() ext-real positive non negative set
(k) is non empty V70() V71() V72() V73() V74() Element of K6(INT)
k -' 1 is V6() V10() V11() V12() integer V28() V33() V43() ext-real non negative V70() V71() V72() V73() V74() V75() Element of NAT
Radix (k -' 1) is V6() V10() V11() V12() integer V28() V33() V43() ext-real non negative V70() V71() V72() V73() V74() V75() Element of NAT
2 to_power (k -' 1) is V11() V12() ext-real set
- (Radix (k -' 1)) is V11() V12() integer ext-real non positive set
(- (Radix (k -' 1))) - 1 is non empty V11() V12() integer ext-real non positive negative set
{ b₁ where b₁ is V11() V12() integer V43() ext-real Element of INT : ( (- (Radix (k -' 1))) - 1 <= b₁ & b₁ <= Radix (k -' 1) ) } is set
Seg (n + 1) is V70() V71() V72() V73() V74() V75() Element of K6(NAT)
x is V15() V18( NAT ) V19(k -SD ) Function-like V35(n) FinSequence-like V60() V61() V62() FinSequence of k -SD
X is V15() V18( NAT ) V19((k)) Function-like FinSequence-like V60() V61() V62() FinSequence of (k)
len X is V6() V10() V11() V12() integer V28() V33() V43() ext-real non negative V70() V71() V72() V73() V74() V75() Element of NAT
dom X is V70() V71() V72() V73() V74() V75() Element of K6(NAT)
(n + 1) -tuples_on (k) is non empty functional FinSequence-membered FinSequenceSet of (k)
CRY is V15() V18( NAT ) V19((k)) Function-like V35(n + 1) FinSequence-like V60() V61() V62() FinSequence of (k)
DIG2 is V6() V10() V11() V12() integer V28() V33() ext-real non negative set
(DIG2,k,(n + 1),CRY) is V11() V12() integer ext-real set
(DIG2,k,n,x) is V11() V12() integer V43() ext-real Element of (k)
CRY . DIG2 is V11() V12() ext-real set
X is V15() V18( NAT ) V19((k)) Function-like V35(n + 1) FinSequence-like V60() V61() V62() FinSequence of (k)
CRY is V15() V18( NAT ) V19((k)) Function-like V35(n + 1) FinSequence-like V60() V61() V62() FinSequence of (k)
len X is V6() V10() V11() V12() integer V28() V33() V43() ext-real non negative V70() V71() V72() V73() V74() V75() Element of NAT
dom X is V35(n + 1) V70() V71() V72() V73() V74() V75() Element of K6(NAT)
DIG2 is V6() V10() V11() V12() integer V28() V33() ext-real non negative set
X . DIG2 is V11() V12() ext-real set
(DIG2,k,(n + 1),X) is V11() V12() integer ext-real set
(DIG2,k,n,x) is V11() V12() integer V43() ext-real Element of (k)
(DIG2,k,(n + 1),CRY) is V11() V12() integer ext-real set
CRY . DIG2 is V11() V12() ext-real set
len CRY is V6() V10() V11() V12() integer V28() V33() V43() ext-real non negative V70() V71() V72() V73() V74() V75() Element of NAT
n is V6() V10() V11() V12() integer V28() V33() ext-real non negative set
k is V6() V10() V11() V12() integer V28() V33() ext-real non negative set
Seg k is V70() V71() V72() V73() V74() V75() Element of K6(NAT)
x is V6() V10() V11() V12() integer V28() V33() ext-real non negative set
(x) is non empty V70() V71() V72() V73() V74() Element of K6(INT)
x -' 1 is V6() V10() V11() V12() integer V28() V33() V43() ext-real non negative V70() V71() V72() V73() V74() V75() Element of NAT
Radix (x -' 1) is V6() V10() V11() V12() integer V28() V33() V43() ext-real non negative V70() V71() V72() V73() V74() V75() Element of NAT
2 to_power (x -' 1) is V11() V12() ext-real set
- (Radix (x -' 1)) is V11() V12() integer ext-real non positive set
(- (Radix (x -' 1))) - 1 is non empty V11() V12() integer ext-real non positive negative set
{ b₁ where b₁ is V11() V12() integer V43() ext-real Element of INT : ( (- (Radix (x -' 1))) - 1 <= b₁ & b₁ <= Radix (x -' 1) ) } is set
X is V15() V18( NAT ) V19((x)) Function-like V35(k) FinSequence-like V60() V61() V62() FinSequence of (x)
(n,x,k,X) is V11() V12() integer ext-real set
X . n is V11() V12() ext-real set
n is V6() V10() V11() V12() integer V28() V33() ext-real non negative set
n -SD is non empty V70() V71() V72() V73() V74() Element of K6(INT)
Radix n is V6() V10() V11() V12() integer V28() V33() V43() ext-real non negative V70() V71() V72() V73() V74() V75() Element of NAT
2 to_power n is V11() V12() ext-real set
(Radix n) - 1 is V11() V12() integer ext-real set
- (Radix n) is V11() V12() integer ext-real non positive set
(- (Radix n)) + 1 is V11() V12() integer ext-real set
{ b₁ where b₁ is V11() V12() integer V43() ext-real Element of INT : ( b₁ <= (Radix n) - 1 & (- (Radix n)) + 1 <= b₁ ) } is set
(n) is non empty V70() V71() V72() V73() V74() Element of K6(INT)
n -' 1 is V6() V10() V11() V12() integer V28() V33() V43() ext-real non negative V70() V71() V72() V73() V74() V75() Element of NAT
Radix (n -' 1) is V6() V10() V11() V12() integer V28() V33() V43() ext-real non negative V70() V71() V72() V73() V74() V75() Element of NAT
2 to_power (n -' 1) is V11() V12() ext-real set
- (Radix (n -' 1)) is V11() V12() integer ext-real non positive set
(- (Radix (n -' 1))) - 1 is non empty V11() V12() integer ext-real non positive negative set
{ b₁ where b₁ is V11() V12() integer V43() ext-real Element of INT : ( (- (Radix (n -' 1))) - 1 <= b₁ & b₁ <= Radix (n -' 1) ) } is set
(n) is non empty V70() V71() V72() V73() V74() Element of K6(INT)
(Radix (n -' 1)) - 1 is V11() V12() integer ext-real set
{ b₁ where b₁ is V11() V12() integer V43() ext-real Element of INT : ( - (Radix (n -' 1)) <= b₁ & b₁ <= (Radix (n -' 1)) - 1 ) } is set
k is V11() V12() integer ext-real set
x is V11() V12() integer ext-real set
k + x is V11() V12() integer ext-real set
((k + x),n) is V11() V12() integer ext-real set
((k + x),n) is V11() V12() integer ext-real set
(Radix n) * ((k + x),n) is V11() V12() integer ext-real set
(k + x) - ((Radix n) * ((k + x),n)) is V11() V12() integer ext-real set
((Radix n) - 1) + (Radix (n -' 1)) is V11() V12() integer ext-real set
((- (Radix n)) + 1) + ((- (Radix (n -' 1))) - 1) is V11() V12() integer ext-real set
(k + x) + 1 is V11() V12() integer ext-real set
(- (Radix (n -' 1))) + (- 1) is V11() V12() integer ext-real non positive set
(- (Radix n)) + (Radix (n -' 1)) is V11() V12() integer ext-real set
((- (Radix n)) + (Radix (n -' 1))) + (- 1) is V11() V12() integer ext-real set
(Radix (n -' 1)) + (- 1) is V11() V12() integer ext-real set
(- (Radix n)) + ((Radix (n -' 1)) + (- 1)) is V11() V12() integer ext-real set
(- (Radix (n -' 1))) + (- (Radix n)) is V11() V12() integer ext-real non positive set
(k + x) + 0 is V11() V12() integer ext-real set
(- (Radix (n -' 1))) - 0 is V11() V12() integer ext-real non positive set
(k + x) - (- (Radix n)) is V11() V12() integer ext-real set
(k + x) + 1 is V11() V12() integer ext-real set
(Radix n) - (Radix (n -' 1)) is V11() V12() integer ext-real set
(Radix n) + (- (Radix (n -' 1))) is V11() V12() integer ext-real set
(Radix n) + ((Radix (n -' 1)) - 1) is V11() V12() integer ext-real set
x is V6() V10() V11() V12() integer V28() V33() ext-real non negative set
k is V6() V10() V11() V12() integer V28() V33() ext-real non negative set
(k) is non empty V70() V71() V72() V73() V74() Element of K6(INT)
k -' 1 is V6() V10() V11() V12() integer V28() V33() V43() ext-real non negative V70() V71() V72() V73() V74() V75() Element of NAT
Radix (k -' 1) is V6() V10() V11() V12() integer V28() V33() V43() ext-real non negative V70() V71() V72() V73() V74() V75() Element of NAT
2 to_power (k -' 1) is V11() V12() ext-real set
- (Radix (k -' 1)) is V11() V12() integer ext-real non positive set
(- (Radix (k -' 1))) - 1 is non empty V11() V12() integer ext-real non positive negative set
{ b₁ where b₁ is V11() V12() integer V43() ext-real Element of INT : ( (- (Radix (k -' 1))) - 1 <= b₁ & b₁ <= Radix (k -' 1) ) } is set
n is V6() V10() V11() V12() integer V28() V33() ext-real non negative set
X is V15() V18( NAT ) V19((k)) Function-like V35(x) FinSequence-like V60() V61() V62() FinSequence of (k)
(n,k,x,X) is V11() V12() integer ext-real set
x is V6() V10() V11() V12() integer V28() V33() ext-real non negative set
k is V6() V10() V11() V12() integer V28() V33() ext-real non negative set
(k) is non empty V70() V71() V72() V73() V74() Element of K6(INT)
k -' 1 is V6() V10() V11() V12() integer V28() V33() V43() ext-real non negative V70() V71() V72() V73() V74() V75() Element of NAT
Radix (k -' 1) is V6() V10() V11() V12() integer V28() V33() V43() ext-real non negative V70() V71() V72() V73() V74() V75() Element of NAT
2 to_power (k -' 1) is V11() V12() ext-real set
- (Radix (k -' 1)) is V11() V12() integer ext-real non positive set
(- (Radix (k -' 1))) - 1 is non empty V11() V12() integer ext-real non positive negative set
{ b₁ where b₁ is V11() V12() integer V43() ext-real Element of INT : ( (- (Radix (k -' 1))) - 1 <= b₁ & b₁ <= Radix (k -' 1) ) } is set
Radix k is V6() V10() V11() V12() integer V28() V33() V43() ext-real non negative V70() V71() V72() V73() V74() V75() Element of NAT
2 to_power k is V11() V12() ext-real set
n is V6() V10() V11() V12() integer V28() V33() ext-real non negative set
n -' 1 is V6() V10() V11() V12() integer V28() V33() V43() ext-real non negative V70() V71() V72() V73() V74() V75() Element of NAT
(Radix k) |^ (n -' 1) is V6() V10() V11() V12() integer V28() V33() V43() ext-real non negative V70() V71() V72() V73() V74() V75() Element of NAT
X is V15() V18( NAT ) V19((k)) Function-like V35(x) FinSequence-like V60() V61() V62() FinSequence of (k)
(n,k,x,X) is V11() V12() integer V43() ext-real Element of INT
(n,k,x,X) is V11() V12() integer ext-real set
((Radix k) |^ (n -' 1)) * (n,k,x,X) is V11() V12() integer ext-real set
n is V6() V10() V11() V12() integer V28() V33() ext-real non negative set
k is V6() V10() V11() V12() integer V28() V33() ext-real non negative set
(k) is non empty V70() V71() V72() V73() V74() Element of K6(INT)
k -' 1 is V6() V10() V11() V12() integer V28() V33() V43() ext-real non negative V70() V71() V72() V73() V74() V75() Element of NAT
Radix (k -' 1) is V6() V10() V11() V12() integer V28() V33() V43() ext-real non negative V70() V71() V72() V73() V74() V75() Element of NAT
2 to_power (k -' 1) is V11() V12() ext-real set
- (Radix (k -' 1)) is V11() V12() integer ext-real non positive set
(- (Radix (k -' 1))) - 1 is non empty V11() V12() integer ext-real non positive negative set
{ b₁ where b₁ is V11() V12() integer V43() ext-real Element of INT : ( (- (Radix (k -' 1))) - 1 <= b₁ & b₁ <= Radix (k -' 1) ) } is set
Seg n is V70() V71() V72() V73() V74() V75() Element of K6(NAT)
x is V15() V18( NAT ) V19((k)) Function-like V35(n) FinSequence-like V60() V61() V62() FinSequence of (k)
X is V15() V18( NAT ) V19( INT ) Function-like FinSequence-like V60() V61() V62() FinSequence of INT
len X is V6() V10() V11() V12() integer V28() V33() V43() ext-real non negative V70() V71() V72() V73() V74() V75() Element of NAT
dom X is V70() V71() V72() V73() V74() V75() Element of K6(NAT)
n -tuples_on INT is non empty functional FinSequence-membered FinSequenceSet of INT
CRY is V15() V18( NAT ) V19( INT ) Function-like V35(n) FinSequence-like V60() V61() V62() FinSequence of INT
DIG2 is V6() V10() V11() V12() integer V28() V33() ext-real non negative set
CRY /. DIG2 is V11() V12() integer V43() ext-real Element of INT
(DIG2,k,n,x) is V11() V12() integer V43() ext-real Element of INT
Radix k is V6() V10() V11() V12() integer V28() V33() V43() ext-real non negative V70() V71() V72() V73() V74() V75() Element of NAT
2 to_power k is V11() V12() ext-real set
DIG2 -' 1 is V6() V10() V11() V12() integer V28() V33() V43() ext-real non negative V70() V71() V72() V73() V74() V75() Element of NAT
(Radix k) |^ (DIG2 -' 1) is V6() V10() V11() V12() integer V28() V33() V43() ext-real non negative V70() V71() V72() V73() V74() V75() Element of NAT
(DIG2,k,n,x) is V11() V12() integer V43() ext-real Element of INT
(DIG2,k,n,x) is V11() V12() integer ext-real set
((Radix k) |^ (DIG2 -' 1)) * (DIG2,k,n,x) is V11() V12() integer ext-real set
dom CRY is V35(n) V70() V71() V72() V73() V74() V75() Element of K6(NAT)
CRY . DIG2 is V11() V12() integer ext-real set
X is V15() V18( NAT ) V19( INT ) Function-like V35(n) FinSequence-like V60() V61() V62() FinSequence of INT
CRY is V15() V18( NAT ) V19( INT ) Function-like V35(n) FinSequence-like V60() V61() V62() FinSequence of INT
len X is V6() V10() V11() V12() integer V28() V33() V43() ext-real non negative V70() V71() V72() V73() V74() V75() Element of NAT
dom X is V35(n) V70() V71() V72() V73() V74() V75() Element of K6(NAT)
len CRY is V6() V10() V11() V12() integer V28() V33() V43() ext-real non negative V70() V71() V72() V73() V74() V75() Element of NAT
DIG2 is V6() V10() V11() V12() integer V28() V33() ext-real non negative set
dom CRY is V35(n) V70() V71() V72() V73() V74() V75() Element of K6(NAT)
X . DIG2 is V11() V12() integer ext-real set
X /. DIG2 is V11() V12() integer V43() ext-real Element of INT
(DIG2,k,n,x) is V11() V12() integer V43() ext-real Element of INT
Radix k is V6() V10() V11() V12() integer V28() V33() V43() ext-real non negative V70() V71() V72() V73() V74() V75() Element of NAT
2 to_power k is V11() V12() ext-real set
DIG2 -' 1 is V6() V10() V11() V12() integer V28() V33() V43() ext-real non negative V70() V71() V72() V73() V74() V75() Element of NAT
(Radix k) |^ (DIG2 -' 1) is V6() V10() V11() V12() integer V28() V33() V43() ext-real non negative V70() V71() V72() V73() V74() V75() Element of NAT
(DIG2,k,n,x) is V11() V12() integer V43() ext-real Element of INT
(DIG2,k,n,x) is V11() V12() integer ext-real set
((Radix k) |^ (DIG2 -' 1)) * (DIG2,k,n,x) is V11() V12() integer ext-real set
CRY /. DIG2 is V11() V12() integer V43() ext-real Element of INT
CRY . DIG2 is V11() V12() integer ext-real set
n is V6() V10() V11() V12() integer V28() V33() ext-real non negative set
k is V6() V10() V11() V12() integer V28() V33() ext-real non negative set
(k) is non empty V70() V71() V72() V73() V74() Element of K6(INT)
k -' 1 is V6() V10() V11() V12() integer V28() V33() V43() ext-real non negative V70() V71() V72() V73() V74() V75() Element of NAT
Radix (k -' 1) is V6() V10() V11() V12() integer V28() V33() V43() ext-real non negative V70() V71() V72() V73() V74() V75() Element of NAT
2 to_power (k -' 1) is V11() V12() ext-real set
- (Radix (k -' 1)) is V11() V12() integer ext-real non positive set
(- (Radix (k -' 1))) - 1 is non empty V11() V12() integer ext-real non positive negative set
{ b₁ where b₁ is V11() V12() integer V43() ext-real Element of INT : ( (- (Radix (k -' 1))) - 1 <= b₁ & b₁ <= Radix (k -' 1) ) } is set
x is V15() V18( NAT ) V19((k)) Function-like V35(n) FinSequence-like V60() V61() V62() FinSequence of (k)
(n,k,x) is V15() V18( NAT ) V19( INT ) Function-like V35(n) FinSequence-like V60() V61() V62() FinSequence of INT
Sum (n,k,x) is V11() V12() integer V43() ext-real Element of INT
n is V6() V10() V11() V12() integer V28() V33() ext-real non negative set
Seg n is V70() V71() V72() V73() V74() V75() Element of K6(NAT)
n + 1 is non empty V6() V10() V11() V12() integer V28() V33() ext-real positive non negative set
(n + 1) + 1 is non empty V6() V10() V11() V12() integer V28() V33() ext-real positive non negative set
k is V6() V10() V11() V12() integer V28() V33() ext-real non negative set
Radix k is V6() V10() V11() V12() integer V28() V33() V43() ext-real non negative V70() V71() V72() V73() V74() V75() Element of NAT
2 to_power k is V11() V12() ext-real set
(Radix k) |^ n is V6() V10() V11() V12() integer V28() V33() ext-real non negative set
x is V6() V10() V11() V12() integer V28() V33() ext-real non negative set
DecSD (x,(n + 1),k) is V15() V18( NAT ) V19(k -SD ) Function-like V35(n + 1) FinSequence-like V60() V61() V62() FinSequence of k -SD
k -SD is non empty V70() V71() V72() V73() V74() Element of K6(INT)
(Radix k) - 1 is V11() V12() integer ext-real set
- (Radix k) is V11() V12() integer ext-real non positive set
(- (Radix k)) + 1 is V11() V12() integer ext-real set
{ b₁ where b₁ is V11() V12() integer V43() ext-real Element of INT : ( b₁ <= (Radix k) - 1 & (- (Radix k)) + 1 <= b₁ ) } is set
((n + 1),k,(DecSD (x,(n + 1),k))) is V15() V18( NAT ) V19((k)) Function-like V35((n + 1) + 1) FinSequence-like V60() V61() V62() FinSequence of (k)
(k) is non empty V70() V71() V72() V73() V74() Element of K6(INT)
k -' 1 is V6() V10() V11() V12() integer V28() V33() V43() ext-real non negative V70() V71() V72() V73() V74() V75() Element of NAT
Radix (k -' 1) is V6() V10() V11() V12() integer V28() V33() V43() ext-real non negative V70() V71() V72() V73() V74() V75() Element of NAT
2 to_power (k -' 1) is V11() V12() ext-real set
- (Radix (k -' 1)) is V11() V12() integer ext-real non positive set
(- (Radix (k -' 1))) - 1 is non empty V11() V12() integer ext-real non positive negative set
{ b₁ where b₁ is V11() V12() integer V43() ext-real Element of INT : ( (- (Radix (k -' 1))) - 1 <= b₁ & b₁ <= Radix (k -' 1) ) } is set
x mod ((Radix k) |^ n) is V6() V10() V11() V12() integer V28() V33() V43() ext-real non negative V70() V71() V72() V73() V74() V75() Element of NAT
DecSD ((x mod ((Radix k) |^ n)),n,k) is V15() V18( NAT ) V19(k -SD ) Function-like V35(n) FinSequence-like V60() V61() V62() FinSequence of k -SD
(n,k,(DecSD ((x mod ((Radix k) |^ n)),n,k))) is V15() V18( NAT ) V19((k)) Function-like V35(n + 1) FinSequence-like V60() V61() V62() FinSequence of (k)
X is V6() V10() V11() V12() integer V28() V33() ext-real non negative set
(X,k,((n + 1) + 1),((n + 1),k,(DecSD (x,(n + 1),k)))) is V11() V12() integer ext-real set
(X,k,(n + 1),(n,k,(DecSD ((x mod ((Radix k) |^ n)),n,k)))) is V11() V12() integer ext-real set
CRY is V6() V10() V11() V12() integer V28() V33() V43() ext-real non negative V70() V71() V72() V73() V74() V75() Element of NAT
Seg (n + 1) is V70() V71() V72() V73() V74() V75() Element of K6(NAT)
Seg ((n + 1) + 1) is V70() V71() V72() V73() V74() V75() Element of K6(NAT)
(CRY,k,(n + 1),(n,k,(DecSD ((x mod ((Radix k) |^ n)),n,k)))) is V11() V12() integer ext-real set
(CRY,k,n,(DecSD ((x mod ((Radix k) |^ n)),n,k))) is V11() V12() integer V43() ext-real Element of (k)
(CRY,k,n,(DecSD ((x mod ((Radix k) |^ n)),n,k))) is V11() V12() integer ext-real set
DigA ((DecSD ((x mod ((Radix k) |^ n)),n,k)),CRY) is V11() V12() integer ext-real set
((DigA ((DecSD ((x mod ((Radix k) |^ n)),n,k)),CRY)),k) is V11() V12() integer ext-real set
((DigA ((DecSD ((x mod ((Radix k) |^ n)),n,k)),CRY)),k) is V11() V12() integer ext-real set
(Radix k) * ((DigA ((DecSD ((x mod ((Radix k) |^ n)),n,k)),CRY)),k) is V11() V12() integer ext-real set
(DigA ((DecSD ((x mod ((Radix k) |^ n)),n,k)),CRY)) - ((Radix k) * ((DigA ((DecSD ((x mod ((Radix k) |^ n)),n,k)),CRY)),k)) is V11() V12() integer ext-real set
CRY -' 1 is V6() V10() V11() V12() integer V28() V33() V43() ext-real non negative V70() V71() V72() V73() V74() V75() Element of NAT
DigA ((DecSD ((x mod ((Radix k) |^ n)),n,k)),(CRY -' 1)) is V11() V12() integer ext-real set
((DigA ((DecSD ((x mod ((Radix k) |^ n)),n,k)),(CRY -' 1))),k) is V11() V12() integer ext-real set
((DigA ((DecSD ((x mod ((Radix k) |^ n)),n,k)),CRY)),k) + ((DigA ((DecSD ((x mod ((Radix k) |^ n)),n,k)),(CRY -' 1))),k) is V11() V12() integer ext-real set
DigA ((DecSD (x,(n + 1),k)),CRY) is V11() V12() integer ext-real set
((DigA ((DecSD (x,(n + 1),k)),CRY)),k) is V11() V12() integer ext-real set
((DigA ((DecSD (x,(n + 1),k)),CRY)),k) is V11() V12() integer ext-real set
(Radix k) * ((DigA ((DecSD (x,(n + 1),k)),CRY)),k) is V11() V12() integer ext-real set
(DigA ((DecSD (x,(n + 1),k)),CRY)) - ((Radix k) * ((DigA ((DecSD (x,(n + 1),k)),CRY)),k)) is V11() V12() integer ext-real set
((DigA ((DecSD (x,(n + 1),k)),CRY)),k) + ((DigA ((DecSD ((x mod ((Radix k) |^ n)),n,k)),(CRY -' 1))),k) is V11() V12() integer ext-real set
DigA ((DecSD ((x mod ((Radix k) |^ n)),n,k)),0) is V11() V12() integer ext-real set
((DigA ((DecSD ((x mod ((Radix k) |^ n)),n,k)),0)),k) is V11() V12() integer ext-real set
((DigA ((DecSD (x,(n + 1),k)),CRY)),k) + ((DigA ((DecSD ((x mod ((Radix k) |^ n)),n,k)),0)),k) is V11() V12() integer ext-real set
(0,k) is V11() V12() integer ext-real set
((DigA ((DecSD (x,(n + 1),k)),CRY)),k) + (0,k) is V11() V12() integer ext-real set
((DigA ((DecSD (x,(n + 1),k)),CRY)),k) + 0 is V11() V12() integer ext-real set
(CRY,k,((n + 1) + 1),((n + 1),k,(DecSD (x,(n + 1),k)))) is V11() V12() integer ext-real set
(CRY,k,(n + 1),(DecSD (x,(n + 1),k))) is V11() V12() integer V43() ext-real Element of (k)
(CRY,k,(n + 1),(DecSD (x,(n + 1),k))) is V11() V12() integer ext-real set
DigA ((DecSD (x,(n + 1),k)),(CRY -' 1)) is V11() V12() integer ext-real set
((DigA ((DecSD (x,(n + 1),k)),(CRY -' 1))),k) is V11() V12() integer ext-real set
((DigA ((DecSD (x,(n + 1),k)),CRY)),k) + ((DigA ((DecSD (x,(n + 1),k)),(CRY -' 1))),k) is V11() V12() integer ext-real set
DigA ((DecSD (x,(n + 1),k)),0) is V11() V12() integer ext-real set
((DigA ((DecSD (x,(n + 1),k)),0)),k) is V11() V12() integer ext-real set
((DigA ((DecSD (x,(n + 1),k)),CRY)),k) + ((DigA ((DecSD (x,(n + 1),k)),0)),k) is V11() V12() integer ext-real set
0 + 1 is non empty V6() V10() V11() V12() integer V28() V33() ext-real positive non negative set
DigA ((DecSD (x,(n + 1),k)),(CRY -' 1)) is V11() V12() integer ext-real set
((DigA ((DecSD (x,(n + 1),k)),(CRY -' 1))),k) is V11() V12() integer ext-real set
((DigA ((DecSD (x,(n + 1),k)),CRY)),k) + ((DigA ((DecSD (x,(n + 1),k)),(CRY -' 1))),k) is V11() V12() integer ext-real set
(CRY,k,(n + 1),(DecSD (x,(n + 1),k))) is V11() V12() integer ext-real set
(CRY,k,(n + 1),(DecSD (x,(n + 1),k))) is V11() V12() integer V43() ext-real Element of (k)
(CRY,k,((n + 1) + 1),((n + 1),k,(DecSD (x,(n + 1),k)))) is V11() V12() integer ext-real set
n is V6() V10() V11() V12() integer V28() V33() ext-real non negative set
n + 1 is non empty V6() V10() V11() V12() integer V28() V33() ext-real positive non negative set
k is V6() V10() V11() V12() integer V28() V33() ext-real non negative set
k + 1 is non empty V6() V10() V11() V12() integer V28() V33() ext-real positive non negative set
(k + 1) + 1 is non empty V6() V10() V11() V12() integer V28() V33() ext-real positive non negative set
Seg k is V70() V71() V72() V73() V74() V75() Element of K6(NAT)
x is V6() V10() V11() V12() integer V28() V33() ext-real non negative set
X is V6() V10() V11() V12() integer V28() V33() ext-real non negative set
DecSD (X,(k + 1),x) is V15() V18( NAT ) V19(x -SD ) Function-like V35(k + 1) FinSequence-like V60() V61() V62() FinSequence of x -SD
x -SD is non empty V70() V71() V72() V73() V74() Element of K6(INT)
Radix x is V6() V10() V11() V12() integer V28() V33() V43() ext-real non negative V70() V71() V72() V73() V74() V75() Element of NAT
2 to_power x is V11() V12() ext-real set
(Radix x) - 1 is V11() V12() integer ext-real set
- (Radix x) is V11() V12() integer ext-real non positive set
(- (Radix x)) + 1 is V11() V12() integer ext-real set
{ b₁ where b₁ is V11() V12() integer V43() ext-real Element of INT : ( b₁ <= (Radix x) - 1 & (- (Radix x)) + 1 <= b₁ ) } is set
((k + 1),x,(DecSD (X,(k + 1),x))) is V15() V18( NAT ) V19((x)) Function-like V35((k + 1) + 1) FinSequence-like V60() V61() V62() FinSequence of (x)
(x) is non empty V70() V71() V72() V73() V74() Element of K6(INT)
x -' 1 is V6() V10() V11() V12() integer V28() V33() V43() ext-real non negative V70() V71() V72() V73() V74() V75() Element of NAT
Radix (x -' 1) is V6() V10() V11() V12() integer V28() V33() V43() ext-real non negative V70() V71() V72() V73() V74() V75() Element of NAT
2 to_power (x -' 1) is V11() V12() ext-real set
- (Radix (x -' 1)) is V11() V12() integer ext-real non positive set
(- (Radix (x -' 1))) - 1 is non empty V11() V12() integer ext-real non positive negative set
{ b₁ where b₁ is V11() V12() integer V43() ext-real Element of INT : ( (- (Radix (x -' 1))) - 1 <= b₁ & b₁ <= Radix (x -' 1) ) } is set
(((k + 1) + 1),x,((k + 1),x,(DecSD (X,(k + 1),x)))) is V11() V12() integer ext-real set
(((k + 1) + 1),x,((k + 1),x,(DecSD (X,(k + 1),x)))) is V15() V18( NAT ) V19( INT ) Function-like V35((k + 1) + 1) FinSequence-like V60() V61() V62() FinSequence of INT
Sum (((k + 1) + 1),x,((k + 1),x,(DecSD (X,(k + 1),x)))) is V11() V12() integer V43() ext-real Element of INT
CRY is V6() V10() V11() V12() integer V28() V33() V43() ext-real non negative V70() V71() V72() V73() V74() V75() Element of NAT
Radix CRY is V6() V10() V11() V12() integer V28() V33() V43() ext-real non negative V70() V71() V72() V73() V74() V75() Element of NAT
2 to_power CRY is V11() V12() ext-real set
(Radix CRY) |^ k is V6() V10() V11() V12() integer V28() V33() ext-real non negative set
X mod ((Radix CRY) |^ k) is V6() V10() V11() V12() integer V28() V33() V43() ext-real non negative V70() V71() V72() V73() V74() V75() Element of NAT
(Radix CRY) |^ (k + 1) is V6() V10() V11() V12() integer V28() V33() ext-real non negative set
Seg ((k + 1) + 1) is V70() V71() V72() V73() V74() V75() Element of K6(NAT)
DecSD (X,(k + 1),CRY) is V15() V18( NAT ) V19(CRY -SD ) Function-like V35(k + 1) FinSequence-like V60() V61() V62() FinSequence of CRY -SD
CRY -SD is non empty V70() V71() V72() V73() V74() Element of K6(INT)
(Radix CRY) - 1 is V11() V12() integer ext-real set
- (Radix CRY) is V11() V12() integer ext-real non positive set
(- (Radix CRY)) + 1 is V11() V12() integer ext-real set
{ b₁ where b₁ is V11() V12() integer V43() ext-real Element of INT : ( b₁ <= (Radix CRY) - 1 & (- (Radix CRY)) + 1 <= b₁ ) } is set
((k + 1),CRY,(DecSD (X,(k + 1),CRY))) is V15() V18( NAT ) V19((CRY)) Function-like V35((k + 1) + 1) FinSequence-like V60() V61() V62() FinSequence of (CRY)
(CRY) is non empty V70() V71() V72() V73() V74() Element of K6(INT)
CRY -' 1 is V6() V10() V11() V12() integer V28() V33() V43() ext-real non negative V70() V71() V72() V73() V74() V75() Element of NAT
Radix (CRY -' 1) is V6() V10() V11() V12() integer V28() V33() V43() ext-real non negative V70() V71() V72() V73() V74() V75() Element of NAT
2 to_power (CRY -' 1) is V11() V12() ext-real set
- (Radix (CRY -' 1)) is V11() V12() integer ext-real non positive set
(- (Radix (CRY -' 1))) - 1 is non empty V11() V12() integer ext-real non positive negative set
{ b₁ where b₁ is V11() V12() integer V43() ext-real Element of INT : ( (- (Radix (CRY -' 1))) - 1 <= b₁ & b₁ <= Radix (CRY -' 1) ) } is set
(((k + 1) + 1),CRY,((k + 1) + 1),((k + 1),CRY,(DecSD (X,(k + 1),CRY)))) is V11() V12() integer V43() ext-real Element of INT
((k + 1) + 1) -' 1 is V6() V10() V11() V12() integer V28() V33() V43() ext-real non negative V70() V71() V72() V73() V74() V75() Element of NAT
(Radix CRY) |^ (((k + 1) + 1) -' 1) is V6() V10() V11() V12() integer V28() V33() V43() ext-real non negative V70() V71() V72() V73() V74() V75() Element of NAT
(((k + 1) + 1),CRY,((k + 1) + 1),((k + 1),CRY,(DecSD (X,(k + 1),CRY)))) is V11() V12() integer V43() ext-real Element of INT
(((k + 1) + 1),CRY,((k + 1) + 1),((k + 1),CRY,(DecSD (X,(k + 1),CRY)))) is V11() V12() integer ext-real set
((Radix CRY) |^ (((k + 1) + 1) -' 1)) * (((k + 1) + 1),CRY,((k + 1) + 1),((k + 1),CRY,(DecSD (X,(k + 1),CRY)))) is V11() V12() integer ext-real set
((Radix CRY) |^ (k + 1)) * (((k + 1) + 1),CRY,((k + 1) + 1),((k + 1),CRY,(DecSD (X,(k + 1),CRY)))) is V11() V12() integer ext-real set
(((k + 1) + 1),CRY,(k + 1),(DecSD (X,(k + 1),CRY))) is V11() V12() integer V43() ext-real Element of (CRY)
((Radix CRY) |^ (k + 1)) * (((k + 1) + 1),CRY,(k + 1),(DecSD (X,(k + 1),CRY))) is V11() V12() integer ext-real set
(((k + 1) + 1),CRY,(k + 1),(DecSD (X,(k + 1),CRY))) is V11() V12() integer ext-real set
((Radix CRY) |^ (k + 1)) * (((k + 1) + 1),CRY,(k + 1),(DecSD (X,(k + 1),CRY))) is V11() V12() integer ext-real set
DigA ((DecSD (X,(k + 1),CRY)),(((k + 1) + 1) -' 1)) is V11() V12() integer ext-real set
((DigA ((DecSD (X,(k + 1),CRY)),(((k + 1) + 1) -' 1))),CRY) is V11() V12() integer ext-real set
((Radix CRY) |^ (k + 1)) * ((DigA ((DecSD (X,(k + 1),CRY)),(((k + 1) + 1) -' 1))),CRY) is V11() V12() integer ext-real set
DigA ((DecSD (X,(k + 1),CRY)),(k + 1)) is V11() V12() integer ext-real set
((DigA ((DecSD (X,(k + 1),CRY)),(k + 1))),CRY) is V11() V12() integer ext-real set
((Radix CRY) |^ (k + 1)) * ((DigA ((DecSD (X,(k + 1),CRY)),(k + 1))),CRY) is V11() V12() integer ext-real set
DecSD ((X mod ((Radix CRY) |^ k)),k,CRY) is V15() V18( NAT ) V19(CRY -SD ) Function-like V35(k) FinSequence-like V60() V61() V62() FinSequence of CRY -SD
(k,CRY,(DecSD ((X mod ((Radix CRY) |^ k)),k,CRY))) is V15() V18( NAT ) V19((CRY)) Function-like V35(k + 1) FinSequence-like V60() V61() V62() FinSequence of (CRY)
xp is V15() V18( NAT ) V19( INT ) Function-like FinSequence-like V60() V61() V62() FinSequence of INT
len xp is V6() V10() V11() V12() integer V28() V33() V43() ext-real non negative V70() V71() V72() V73() V74() V75() Element of NAT
dom xp is V70() V71() V72() V73() V74() V75() Element of K6(NAT)
Seg (k + 1) is V70() V71() V72() V73() V74() V75() Element of K6(NAT)
(((k + 1) + 1),CRY,((k + 1),CRY,(DecSD (X,(k + 1),CRY)))) is V15() V18( NAT ) V19( INT ) Function-like V35((k + 1) + 1) FinSequence-like V60() V61() V62() FinSequence of INT
len (((k + 1) + 1),CRY,((k + 1),CRY,(DecSD (X,(k + 1),CRY)))) is V6() V10() V11() V12() integer V28() V33() V43() ext-real non negative V70() V71() V72() V73() V74() V75() Element of NAT
<*(((k + 1) + 1),CRY,((k + 1) + 1),((k + 1),CRY,(DecSD (X,(k + 1),CRY))))*> is V15() V18( NAT ) V19( INT ) Function-like FinSequence-like V60() V61() V62() FinSequence of INT
xp ^ <*(((k + 1) + 1),CRY,((k + 1) + 1),((k + 1),CRY,(DecSD (X,(k + 1),CRY))))*> is V15() V18( NAT ) V19( INT ) Function-like FinSequence-like V60() V61() V62() FinSequence of INT
xpp is V6() V10() V11() V12() integer V28() V33() ext-real non negative set
(((k + 1) + 1),CRY,((k + 1),CRY,(DecSD (X,(k + 1),CRY)))) . xpp is V11() V12() integer ext-real set
(xp ^ <*(((k + 1) + 1),CRY,((k + 1) + 1),((k + 1),CRY,(DecSD (X,(k + 1),CRY))))*>) . xpp is V11() V12() integer ext-real set
dom (((k + 1) + 1),CRY,((k + 1),CRY,(DecSD (X,(k + 1),CRY)))) is V35((k + 1) + 1) V70() V71() V72() V73() V74() V75() Element of K6(NAT)
xp . xpp is V11() V12() integer ext-real set
(xpp,CRY,((k + 1) + 1),((k + 1),CRY,(DecSD (X,(k + 1),CRY)))) is V11() V12() integer V43() ext-real Element of INT
xpp -' 1 is V6() V10() V11() V12() integer V28() V33() V43() ext-real non negative V70() V71() V72() V73() V74() V75() Element of NAT
(Radix CRY) |^ (xpp -' 1) is V6() V10() V11() V12() integer V28() V33() V43() ext-real non negative V70() V71() V72() V73() V74() V75() Element of NAT
(xpp,CRY,((k + 1) + 1),((k + 1),CRY,(DecSD (X,(k + 1),CRY)))) is V11() V12() integer V43() ext-real Element of INT
(xpp,CRY,((k + 1) + 1),((k + 1),CRY,(DecSD (X,(k + 1),CRY)))) is V11() V12() integer ext-real set
((Radix CRY) |^ (xpp -' 1)) * (xpp,CRY,((k + 1) + 1),((k + 1),CRY,(DecSD (X,(k + 1),CRY)))) is V11() V12() integer ext-real set
(((k + 1) + 1),CRY,((k + 1),CRY,(DecSD (X,(k + 1),CRY)))) /. xpp is V11() V12() integer V43() ext-real Element of INT
(((k + 1) + 1),CRY,((k + 1),CRY,(DecSD (X,(k + 1),CRY)))) /. ((k + 1) + 1) is V11() V12() integer V43() ext-real Element of INT
((k + 1),CRY,(k,CRY,(DecSD ((X mod ((Radix CRY) |^ k)),k,CRY)))) is V11() V12() integer ext-real set
((k + 1),CRY,(k,CRY,(DecSD ((X mod ((Radix CRY) |^ k)),k,CRY)))) is V15() V18( NAT ) V19( INT ) Function-like V35(k + 1) FinSequence-like V60() V61() V62() FinSequence of INT
Sum ((k + 1),CRY,(k,CRY,(DecSD ((X mod ((Radix CRY) |^ k)),k,CRY)))) is V11() V12() integer V43() ext-real Element of INT
xpp is V15() V18( NAT ) V19( INT ) Function-like FinSequence-like V60() V61() V62() FinSequence of INT
len xpp is V6() V10() V11() V12() integer V28() V33() V43() ext-real non negative V70() V71() V72() V73() V74() V75() Element of NAT
dom xpp is V70() V71() V72() V73() V74() V75() Element of K6(NAT)
((k + 1),CRY,((k + 1) + 1),((k + 1),CRY,(DecSD (X,(k + 1),CRY)))) is V11() V12() integer V43() ext-real Element of INT
(k + 1) -' 1 is V6() V10() V11() V12() integer V28() V33() V43() ext-real non negative V70() V71() V72() V73() V74() V75() Element of NAT
(Radix CRY) |^ ((k + 1) -' 1) is V6() V10() V11() V12() integer V28() V33() V43() ext-real non negative V70() V71() V72() V73() V74() V75() Element of NAT
((k + 1),CRY,((k + 1) + 1),((k + 1),CRY,(DecSD (X,(k + 1),CRY)))) is V11() V12() integer V43() ext-real Element of INT
((k + 1),CRY,((k + 1) + 1),((k + 1),CRY,(DecSD (X,(k + 1),CRY)))) is V11() V12() integer ext-real set
((Radix CRY) |^ ((k + 1) -' 1)) * ((k + 1),CRY,((k + 1) + 1),((k + 1),CRY,(DecSD (X,(k + 1),CRY)))) is V11() V12() integer ext-real set
<*((k + 1),CRY,((k + 1) + 1),((k + 1),CRY,(DecSD (X,(k + 1),CRY))))*> is V15() V18( NAT ) V19( INT ) Function-like FinSequence-like V60() V61() V62() FinSequence of INT
xpp ^ <*((k + 1),CRY,((k + 1) + 1),((k + 1),CRY,(DecSD (X,(k + 1),CRY))))*> is V15() V18( NAT ) V19( INT ) Function-like FinSequence-like V60() V61() V62() FinSequence of INT
xnpp is V6() V10() V11() V12() integer V28() V33() ext-real non negative set
xp . xnpp is V11() V12() integer ext-real set
(xpp ^ <*((k + 1),CRY,((k + 1) + 1),((k + 1),CRY,(DecSD (X,(k + 1),CRY))))*>) . xnpp is V11() V12() integer ext-real set
xpp . xnpp is V11() V12() integer ext-real set
(xnpp,CRY,((k + 1) + 1),((k + 1),CRY,(DecSD (X,(k + 1),CRY)))) is V11() V12() integer V43() ext-real Element of INT
xnpp -' 1 is V6() V10() V11() V12() integer V28() V33() V43() ext-real non negative V70() V71() V72() V73() V74() V75() Element of NAT
(Radix CRY) |^ (xnpp -' 1) is V6() V10() V11() V12() integer V28() V33() V43() ext-real non negative V70() V71() V72() V73() V74() V75() Element of NAT
(xnpp,CRY,((k + 1) + 1),((k + 1),CRY,(DecSD (X,(k + 1),CRY)))) is V11() V12() integer V43() ext-real Element of INT
(xnpp,CRY,((k + 1) + 1),((k + 1),CRY,(DecSD (X,(k + 1),CRY)))) is V11() V12() integer ext-real set
((Radix CRY) |^ (xnpp -' 1)) * (xnpp,CRY,((k + 1) + 1),((k + 1),CRY,(DecSD (X,(k + 1),CRY)))) is V11() V12() integer ext-real set
xnpp is V15() V18( NAT ) V19( INT ) Function-like FinSequence-like V60() V61() V62() FinSequence of INT
len xnpp is V6() V10() V11() V12() integer V28() V33() V43() ext-real non negative V70() V71() V72() V73() V74() V75() Element of NAT
dom xnpp is V70() V71() V72() V73() V74() V75() Element of K6(NAT)
RNDIG is V6() V10() V11() V12() integer V28() V33() ext-real non negative set
xnpp . RNDIG is V11() V12() integer ext-real set
xpp . RNDIG is V11() V12() integer ext-real set
(RNDIG,CRY,((k + 1) + 1),((k + 1),CRY,(DecSD (X,(k + 1),CRY)))) is V11() V12() integer V43() ext-real Element of INT
RNDIG -' 1 is V6() V10() V11() V12() integer V28() V33() V43() ext-real non negative V70() V71() V72() V73() V74() V75() Element of NAT
(Radix CRY) |^ (RNDIG -' 1) is V6() V10() V11() V12() integer V28() V33() V43() ext-real non negative V70() V71() V72() V73() V74() V75() Element of NAT
(RNDIG,CRY,((k + 1) + 1),((k + 1),CRY,(DecSD (X,(k + 1),CRY)))) is V11() V12() integer V43() ext-real Element of INT
(RNDIG,CRY,((k + 1) + 1),((k + 1),CRY,(DecSD (X,(k + 1),CRY)))) is V11() V12() integer ext-real set
((Radix CRY) |^ (RNDIG -' 1)) * (RNDIG,CRY,((k + 1) + 1),((k + 1),CRY,(DecSD (X,(k + 1),CRY)))) is V11() V12() integer ext-real set
(RNDIG,CRY,(k + 1),(k,CRY,(DecSD ((X mod ((Radix CRY) |^ k)),k,CRY)))) is V11() V12() integer V43() ext-real Element of INT
(RNDIG,CRY,(k + 1),(k,CRY,(DecSD ((X mod ((Radix CRY) |^ k)),k,CRY)))) is V11() V12() integer V43() ext-real Element of INT
(RNDIG,CRY,(k + 1),(k,CRY,(DecSD ((X mod ((Radix CRY) |^ k)),k,CRY)))) is V11() V12() integer ext-real set
((Radix CRY) |^ (RNDIG -' 1)) * (RNDIG,CRY,(k + 1),(k,CRY,(DecSD ((X mod ((Radix CRY) |^ k)),k,CRY)))) is V11() V12() integer ext-real set
len ((k + 1),CRY,(k,CRY,(DecSD ((X mod ((Radix CRY) |^ k)),k,CRY)))) is V6() V10() V11() V12() integer V28() V33() V43() ext-real non negative V70() V71() V72() V73() V74() V75() Element of NAT
((k + 1),CRY,(k + 1),(k,CRY,(DecSD ((X mod ((Radix CRY) |^ k)),k,CRY)))) is V11() V12() integer V43() ext-real Element of INT
((k + 1),CRY,(k + 1),(k,CRY,(DecSD ((X mod ((Radix CRY) |^ k)),k,CRY)))) is V11() V12() integer V43() ext-real Element of INT
((k + 1),CRY,(k + 1),(k,CRY,(DecSD ((X mod ((Radix CRY) |^ k)),k,CRY)))) is V11() V12() integer ext-real set
((Radix CRY) |^ ((k + 1) -' 1)) * ((k + 1),CRY,(k + 1),(k,CRY,(DecSD ((X mod ((Radix CRY) |^ k)),k,CRY)))) is V11() V12() integer ext-real set
<*((k + 1),CRY,(k + 1),(k,CRY,(DecSD ((X mod ((Radix CRY) |^ k)),k,CRY))))*> is V15() V18( NAT ) V19( INT ) Function-like FinSequence-like V60() V61() V62() FinSequence of INT
xnpp ^ <*((k + 1),CRY,(k + 1),(k,CRY,(DecSD ((X mod ((Radix CRY) |^ k)),k,CRY))))*> is V15() V18( NAT ) V19( INT ) Function-like FinSequence-like V60() V61() V62() FinSequence of INT
RNDIG is V6() V10() V11() V12() integer V28() V33() ext-real non negative set
((k + 1),CRY,(k,CRY,(DecSD ((X mod ((Radix CRY) |^ k)),k,CRY)))) . RNDIG is V11() V12() integer ext-real set
(xnpp ^ <*((k + 1),CRY,(k + 1),(k,CRY,(DecSD ((X mod ((Radix CRY) |^ k)),k,CRY))))*>) . RNDIG is V11() V12() integer ext-real set
dom ((k + 1),CRY,(k,CRY,(DecSD ((X mod ((Radix CRY) |^ k)),k,CRY)))) is V35(k + 1) V70() V71() V72() V73() V74() V75() Element of K6(NAT)
xnpp . RNDIG is V11() V12() integer ext-real set
(RNDIG,CRY,(k + 1),(k,CRY,(DecSD ((X mod ((Radix CRY) |^ k)),k,CRY)))) is V11() V12() integer V43() ext-real Element of INT
RNDIG -' 1 is V6() V10() V11() V12() integer V28() V33() V43() ext-real non negative V70() V71() V72() V73() V74() V75() Element of NAT
(Radix CRY) |^ (RNDIG -' 1) is V6() V10() V11() V12() integer V28() V33() V43() ext-real non negative V70() V71() V72() V73() V74() V75() Element of NAT
(RNDIG,CRY,(k + 1),(k,CRY,(DecSD ((X mod ((Radix CRY) |^ k)),k,CRY)))) is V11() V12() integer V43() ext-real Element of INT
(RNDIG,CRY,(k + 1),(k,CRY,(DecSD ((X mod ((Radix CRY) |^ k)),k,CRY)))) is V11() V12() integer ext-real set
((Radix CRY) |^ (RNDIG -' 1)) * (RNDIG,CRY,(k + 1),(k,CRY,(DecSD ((X mod ((Radix CRY) |^ k)),k,CRY)))) is V11() V12() integer ext-real set
((k + 1),CRY,(k,CRY,(DecSD ((X mod ((Radix CRY) |^ k)),k,CRY)))) /. RNDIG is V11() V12() integer V43() ext-real Element of INT
((k + 1),CRY,(k,CRY,(DecSD ((X mod ((Radix CRY) |^ k)),k,CRY)))) /. (k + 1) is V11() V12() integer V43() ext-real Element of INT
len (xpp ^ <*((k + 1),CRY,((k + 1) + 1),((k + 1),CRY,(DecSD (X,(k + 1),CRY))))*>) is V6() V10() V11() V12() integer V28() V33() V43() ext-real non negative V70() V71() V72() V73() V74() V75() Element of NAT
len (xp ^ <*(((k + 1) + 1),CRY,((k + 1) + 1),((k + 1),CRY,(DecSD (X,(k + 1),CRY))))*>) is V6() V10() V11() V12() integer V28() V33() V43() ext-real non negative V70() V71() V72() V73() V74() V75() Element of NAT
Sum (((k + 1) + 1),CRY,((k + 1),CRY,(DecSD (X,(k + 1),CRY)))) is V11() V12() integer V43() ext-real Element of INT
Sum xp is V11() V12() integer V43() ext-real Element of INT
(Sum xp) + (((k + 1) + 1),CRY,((k + 1) + 1),((k + 1),CRY,(DecSD (X,(k + 1),CRY)))) is V11() V12() integer ext-real set
Sum xnpp is V11() V12() integer V43() ext-real Element of INT
(Sum xnpp) + ((k + 1),CRY,((k + 1) + 1),((k + 1),CRY,(DecSD (X,(k + 1),CRY)))) is V11() V12() integer ext-real set
((Sum xnpp) + ((k + 1),CRY,((k + 1) + 1),((k + 1),CRY,(DecSD (X,(k + 1),CRY))))) + (((k + 1) + 1),CRY,((k + 1) + 1),((k + 1),CRY,(DecSD (X,(k + 1),CRY)))) is V11() V12() integer ext-real set
((Radix CRY) |^ k) * (DigA ((DecSD (X,(k + 1),CRY)),(k + 1))) is V11() V12() integer ext-real set
DigA ((DecSD (X,(k + 1),CRY)),k) is V11() V12() integer ext-real set
((DigA ((DecSD (X,(k + 1),CRY)),k)),CRY) is V11() V12() integer ext-real set
((Radix CRY) |^ k) * ((DigA ((DecSD (X,(k + 1),CRY)),k)),CRY) is V11() V12() integer ext-real set
len (xnpp ^ <*((k + 1),CRY,(k + 1),(k,CRY,(DecSD ((X mod ((Radix CRY) |^ k)),k,CRY))))*>) is V6() V10() V11() V12() integer V28() V33() V43() ext-real non negative V70() V71() V72() V73() V74() V75() Element of NAT
(X mod ((Radix CRY) |^ k)) + 0 is V6() V10() V11() V12() integer V28() V33() ext-real non negative set
(Sum xnpp) + ((k + 1),CRY,(k + 1),(k,CRY,(DecSD ((X mod ((Radix CRY) |^ k)),k,CRY)))) is V11() V12() integer ext-real set
((Radix CRY) |^ k) * ((k + 1),CRY,((k + 1) + 1),((k + 1),CRY,(DecSD (X,(k + 1),CRY)))) is V11() V12() integer ext-real set
((k + 1),CRY,(k + 1),(DecSD (X,(k + 1),CRY))) is V11() V12() integer V43() ext-real Element of (CRY)
((Radix CRY) |^ k) * ((k + 1),CRY,(k + 1),(DecSD (X,(k + 1),CRY))) is V11() V12() integer ext-real set
((k + 1),CRY,(k + 1),(DecSD (X,(k + 1),CRY))) is V11() V12() integer ext-real set
((Radix CRY) |^ k) * ((k + 1),CRY,(k + 1),(DecSD (X,(k + 1),CRY))) is V11() V12() integer ext-real set
((DigA ((DecSD (X,(k + 1),CRY)),(k + 1))),CRY) is V11() V12() integer ext-real set
(Radix CRY) * ((DigA ((DecSD (X,(k + 1),CRY)),(k + 1))),CRY) is V11() V12() integer ext-real set
(DigA ((DecSD (X,(k + 1),CRY)),(k + 1))) - ((Radix CRY) * ((DigA ((DecSD (X,(k + 1),CRY)),(k + 1))),CRY)) is V11() V12() integer ext-real set
DigA ((DecSD (X,(k + 1),CRY)),((k + 1) -' 1)) is V11() V12() integer ext-real set
((DigA ((DecSD (X,(k + 1),CRY)),((k + 1) -' 1))),CRY) is V11() V12() integer ext-real set
((DigA ((DecSD (X,(k + 1),CRY)),(k + 1))),CRY) + ((DigA ((DecSD (X,(k + 1),CRY)),((k + 1) -' 1))),CRY) is V11() V12() integer ext-real set
((Radix CRY) |^ k) * (((DigA ((DecSD (X,(k + 1),CRY)),(k + 1))),CRY) + ((DigA ((DecSD (X,(k + 1),CRY)),((k + 1) -' 1))),CRY)) is V11() V12() integer ext-real set
((DigA ((DecSD (X,(k + 1),CRY)),(k + 1))),CRY) + ((DigA ((DecSD (X,(k + 1),CRY)),k)),CRY) is V11() V12() integer ext-real set
((Radix CRY) |^ k) * (((DigA ((DecSD (X,(k + 1),CRY)),(k + 1))),CRY) + ((DigA ((DecSD (X,(k + 1),CRY)),k)),CRY)) is V11() V12() integer ext-real set
((Radix CRY) |^ k) * (Radix CRY) is V6() V10() V11() V12() integer V28() V33() ext-real non negative set
(((Radix CRY) |^ k) * (Radix CRY)) * ((DigA ((DecSD (X,(k + 1),CRY)),(k + 1))),CRY) is V11() V12() integer ext-real set
(((Radix CRY) |^ k) * (DigA ((DecSD (X,(k + 1),CRY)),(k + 1)))) - ((((Radix CRY) |^ k) * (Radix CRY)) * ((DigA ((DecSD (X,(k + 1),CRY)),(k + 1))),CRY)) is V11() V12() integer ext-real set
((((Radix CRY) |^ k) * (DigA ((DecSD (X,(k + 1),CRY)),(k + 1)))) - ((((Radix CRY) |^ k) * (Radix CRY)) * ((DigA ((DecSD (X,(k + 1),CRY)),(k + 1))),CRY))) + (((Radix CRY) |^ k) * ((DigA ((DecSD (X,(k + 1),CRY)),k)),CRY)) is V11() V12() integer ext-real set
(((Radix CRY) |^ k) * (DigA ((DecSD (X,(k + 1),CRY)),(k + 1)))) - (((Radix CRY) |^ (k + 1)) * ((DigA ((DecSD (X,(k + 1),CRY)),(k + 1))),CRY)) is V11() V12() integer ext-real set
((((Radix CRY) |^ k) * (DigA ((DecSD (X,(k + 1),CRY)),(k + 1)))) - (((Radix CRY) |^ (k + 1)) * ((DigA ((DecSD (X,(k + 1),CRY)),(k + 1))),CRY))) + (((Radix CRY) |^ k) * ((DigA ((DecSD (X,(k + 1),CRY)),k)),CRY)) is V11() V12() integer ext-real set
((Radix CRY) |^ k) * ((k + 1),CRY,(k + 1),(k,CRY,(DecSD ((X mod ((Radix CRY) |^ k)),k,CRY)))) is V11() V12() integer ext-real set
((k + 1),CRY,k,(DecSD ((X mod ((Radix CRY) |^ k)),k,CRY))) is V11() V12() integer V43() ext-real Element of (CRY)
((Radix CRY) |^ k) * ((k + 1),CRY,k,(DecSD ((X mod ((Radix CRY) |^ k)),k,CRY))) is V11() V12() integer ext-real set
((k + 1),CRY,k,(DecSD ((X mod ((Radix CRY) |^ k)),k,CRY))) is V11() V12() integer ext-real set
((Radix CRY) |^ k) * ((k + 1),CRY,k,(DecSD ((X mod ((Radix CRY) |^ k)),k,CRY))) is V11() V12() integer ext-real set
DigA ((DecSD ((X mod ((Radix CRY) |^ k)),k,CRY)),((k + 1) -' 1)) is V11() V12() integer ext-real set
((DigA ((DecSD ((X mod ((Radix CRY) |^ k)),k,CRY)),((k + 1) -' 1))),CRY) is V11() V12() integer ext-real set
((Radix CRY) |^ k) * ((DigA ((DecSD ((X mod ((Radix CRY) |^ k)),k,CRY)),((k + 1) -' 1))),CRY) is V11() V12() integer ext-real set
DigA ((DecSD ((X mod ((Radix CRY) |^ k)),k,CRY)),k) is V11() V12() integer ext-real set
((DigA ((DecSD ((X mod ((Radix CRY) |^ k)),k,CRY)),k)),CRY) is V11() V12() integer ext-real set
((Radix CRY) |^ k) * ((DigA ((DecSD ((X mod ((Radix CRY) |^ k)),k,CRY)),k)),CRY) is V11() V12() integer ext-real set
(X mod ((Radix CRY) |^ k)) + (((Radix CRY) |^ k) * (DigA ((DecSD (X,(k + 1),CRY)),(k + 1)))) is V11() V12() integer ext-real set
((X mod ((Radix CRY) |^ k)) + (((Radix CRY) |^ k) * (DigA ((DecSD (X,(k + 1),CRY)),(k + 1))))) - (((Radix CRY) |^ k) * ((DigA ((DecSD (X,(k + 1),CRY)),k)),CRY)) is V11() V12() integer ext-real set
(((X mod ((Radix CRY) |^ k)) + (((Radix CRY) |^ k) * (DigA ((DecSD (X,(k + 1),CRY)),(k + 1))))) - (((Radix CRY) |^ k) * ((DigA ((DecSD (X,(k + 1),CRY)),k)),CRY))) + (((Radix CRY) |^ k) * ((DigA ((DecSD (X,(k + 1),CRY)),k)),CRY)) is V11() V12() integer ext-real set
X div ((Radix CRY) |^ k) is V6() V10() V11() V12() integer V28() V33() V43() ext-real non negative V70() V71() V72() V73() V74() V75() Element of NAT
((Radix CRY) |^ k) * (X div ((Radix CRY) |^ k)) is V6() V10() V11() V12() integer V28() V33() ext-real non negative set
(X mod ((Radix CRY) |^ k)) + (((Radix CRY) |^ k) * (X div ((Radix CRY) |^ k))) is V6() V10() V11() V12() integer V28() V33() ext-real non negative set
1 + 1 is non empty V6() V10() V11() V12() integer V28() V33() ext-real positive non negative set
Seg 1 is V70() V71() V72() V73() V74() V75() Element of K6(NAT)
2 - 1 is V11() V12() integer ext-real set
2 -' 1 is V6() V10() V11() V12() integer V28() V33() V43() ext-real non negative V70() V71() V72() V73() V74() V75() Element of NAT
k is V6() V10() V11() V12() integer V28() V33() ext-real non negative set
x is V6() V10() V11() V12() integer V28() V33() ext-real non negative set
DecSD (x,1,k) is non empty V2() V15() V18( NAT ) V19(k -SD ) Function-like V35(1) FinSequence-like V60() V61() V62() V64() V65() V66() V67() FinSequence of k -SD
k -SD is non empty V70() V71() V72() V73() V74() Element of K6(INT)
Radix k is V6() V10() V11() V12() integer V28() V33() V43() ext-real non negative V70() V71() V72() V73() V74() V75() Element of NAT
2 to_power k is V11() V12() ext-real set
(Radix k) - 1 is V11() V12() integer ext-real set
- (Radix k) is V11() V12() integer ext-real non positive set
(- (Radix k)) + 1 is V11() V12() integer ext-real set
{ b₁ where b₁ is V11() V12() integer V43() ext-real Element of INT : ( b₁ <= (Radix k) - 1 & (- (Radix k)) + 1 <= b₁ ) } is set
(1,k,(DecSD (x,1,k))) is V15() V18( NAT ) V19((k)) Function-like V35(1 + 1) FinSequence-like V60() V61() V62() FinSequence of (k)
(k) is non empty V70() V71() V72() V73() V74() Element of K6(INT)
k -' 1 is V6() V10() V11() V12() integer V28() V33() V43() ext-real non negative V70() V71() V72() V73() V74() V75() Element of NAT
Radix (k -' 1) is V6() V10() V11() V12() integer V28() V33() V43() ext-real non negative V70() V71() V72() V73() V74() V75() Element of NAT
2 to_power (k -' 1) is V11() V12() ext-real set
- (Radix (k -' 1)) is V11() V12() integer ext-real non positive set
(- (Radix (k -' 1))) - 1 is non empty V11() V12() integer ext-real non positive negative set
{ b₁ where b₁ is V11() V12() integer V43() ext-real Element of INT : ( (- (Radix (k -' 1))) - 1 <= b₁ & b₁ <= Radix (k -' 1) ) } is set
((1 + 1),k,(1,k,(DecSD (x,1,k)))) is V11() V12() integer ext-real set
((1 + 1),k,(1,k,(DecSD (x,1,k)))) is V15() V18( NAT ) V19( INT ) Function-like V35(1 + 1) FinSequence-like V60() V61() V62() FinSequence of INT
Sum ((1 + 1),k,(1,k,(DecSD (x,1,k)))) is V11() V12() integer V43() ext-real Element of INT
DigA ((DecSD (x,1,k)),1) is V11() V12() integer ext-real set
((DigA ((DecSD (x,1,k)),1)),k) is V11() V12() integer ext-real set
(Radix k) * ((DigA ((DecSD (x,1,k)),1)),k) is V11() V12() integer ext-real set
CRY is V11() V12() integer ext-real set
(DigA ((DecSD (x,1,k)),1)) - CRY is V11() V12() integer ext-real set
Seg (1 + 1) is V70() V71() V72() V73() V74() V75() Element of K6(NAT)
len ((1 + 1),k,(1,k,(DecSD (x,1,k)))) is V6() V10() V11() V12() integer V28() V33() V43() ext-real non negative V70() V71() V72() V73() V74() V75() Element of NAT
dom ((1 + 1),k,(1,k,(DecSD (x,1,k)))) is V35(1 + 1) V70() V71() V72() V73() V74() V75() Element of K6(NAT)
((1 + 1),k,(1,k,(DecSD (x,1,k)))) /. 2 is V11() V12() integer V43() ext-real Element of INT
(2,k,(1 + 1),(1,k,(DecSD (x,1,k)))) is V11() V12() integer V43() ext-real Element of INT
(Radix k) |^ (2 -' 1) is V6() V10() V11() V12() integer V28() V33() V43() ext-real non negative V70() V71() V72() V73() V74() V75() Element of NAT
(2,k,(1 + 1),(1,k,(DecSD (x,1,k)))) is V11() V12() integer V43() ext-real Element of INT
(2,k,(1 + 1),(1,k,(DecSD (x,1,k)))) is V11() V12() integer ext-real set
((Radix k) |^ (2 -' 1)) * (2,k,(1 + 1),(1,k,(DecSD (x,1,k)))) is V11() V12() integer ext-real set
(Radix k) * (2,k,(1 + 1),(1,k,(DecSD (x,1,k)))) is V11() V12() integer ext-real set
(2,k,1,(DecSD (x,1,k))) is V11() V12() integer V43() ext-real Element of (k)
(Radix k) * (2,k,1,(DecSD (x,1,k))) is V11() V12() integer ext-real set
(2,k,1,(DecSD (x,1,k))) is V11() V12() integer ext-real set
(Radix k) * (2,k,1,(DecSD (x,1,k))) is V11() V12() integer ext-real set
((1 + 1),k,(1,k,(DecSD (x,1,k)))) . 2 is V11() V12() integer ext-real set
((1 + 1),k,(1,k,(DecSD (x,1,k)))) /. 1 is V11() V12() integer V43() ext-real Element of INT
(1,k,(1 + 1),(1,k,(DecSD (x,1,k)))) is V11() V12() integer V43() ext-real Element of INT
1 -' 1 is V6() V10() V11() V12() integer V28() V33() V43() ext-real non negative V70() V71() V72() V73() V74() V75() Element of NAT
(Radix k) |^ (1 -' 1) is V6() V10() V11() V12() integer V28() V33() V43() ext-real non negative V70() V71() V72() V73() V74() V75() Element of NAT
(1,k,(1 + 1),(1,k,(DecSD (x,1,k)))) is V11() V12() integer V43() ext-real Element of INT
(1,k,(1 + 1),(1,k,(DecSD (x,1,k)))) is V11() V12() integer ext-real set
((Radix k) |^ (1 -' 1)) * (1,k,(1 + 1),(1,k,(DecSD (x,1,k)))) is V11() V12() integer ext-real set
(Radix k) |^ 0 is V6() V10() V11() V12() integer V28() V33() V43() ext-real non negative V70() V71() V72() V73() V74() V75() Element of NAT
((Radix k) |^ 0) * (1,k,(1 + 1),(1,k,(DecSD (x,1,k)))) is V11() V12() integer ext-real set
1 * (1,k,(1 + 1),(1,k,(DecSD (x,1,k)))) is V11() V12() integer ext-real set
(1,k,1,(DecSD (x,1,k))) is V11() V12() integer V43() ext-real Element of (k)
(1,k,1,(DecSD (x,1,k))) is V11() V12() integer ext-real set
((DigA ((DecSD (x,1,k)),1)),k) is V11() V12() integer ext-real set
(DigA ((DecSD (x,1,k)),1)) - ((Radix k) * ((DigA ((DecSD (x,1,k)),1)),k)) is V11() V12() integer ext-real set
DigA ((DecSD (x,1,k)),(1 -' 1)) is V11() V12() integer ext-real set
((DigA ((DecSD (x,1,k)),(1 -' 1))),k) is V11() V12() integer ext-real set
((DigA ((DecSD (x,1,k)),1)),k) + ((DigA ((DecSD (x,1,k)),(1 -' 1))),k) is V11() V12() integer ext-real set
DigA ((DecSD (x,1,k)),0) is V11() V12() integer ext-real set
((DigA ((DecSD (x,1,k)),0)),k) is V11() V12() integer ext-real set
((DigA ((DecSD (x,1,k)),1)),k) + ((DigA ((DecSD (x,1,k)),0)),k) is V11() V12() integer ext-real set
(0,k) is V11() V12() integer ext-real set
((DigA ((DecSD (x,1,k)),1)),k) + (0,k) is V11() V12() integer ext-real set
((DigA ((DecSD (x,1,k)),1)),k) + 0 is V11() V12() integer ext-real set
((1 + 1),k,(1,k,(DecSD (x,1,k)))) . 1 is V11() V12() integer ext-real set
DIG1 is V11() V12() integer V43() ext-real Element of INT
DIG2 is V11() V12() integer V43() ext-real Element of INT
<*DIG1,DIG2*> is set
DIG1 + DIG2 is V11() V12() integer ext-real set
k is V6() V10() V11() V12() integer V28() V33() ext-real non negative set
x is V6() V10() V11() V12() integer V28() V33() ext-real non negative set
DecSD (x,n,k) is V15() V18( NAT ) V19(k -SD ) Function-like V35(n) FinSequence-like V60() V61() V62() FinSequence of k -SD
k -SD is non empty V70() V71() V72() V73() V74() Element of K6(INT)
Radix k is V6() V10() V11() V12() integer V28() V33() V43() ext-real non negative V70() V71() V72() V73() V74() V75() Element of NAT
2 to_power k is V11() V12() ext-real set
(Radix k) - 1 is V11() V12() integer ext-real set
- (Radix k) is V11() V12() integer ext-real non positive set
(- (Radix k)) + 1 is V11() V12() integer ext-real set
{ b₁ where b₁ is V11() V12() integer V43() ext-real Element of INT : ( b₁ <= (Radix k) - 1 & (- (Radix k)) + 1 <= b₁ ) } is set
(n,k,(DecSD (x,n,k))) is V15() V18( NAT ) V19((k)) Function-like V35(n + 1) FinSequence-like V60() V61() V62() FinSequence of (k)
(k) is non empty V70() V71() V72() V73() V74() Element of K6(INT)
k -' 1 is V6() V10() V11() V12() integer V28() V33() V43() ext-real non negative V70() V71() V72() V73() V74() V75() Element of NAT
Radix (k -' 1) is V6() V10() V11() V12() integer V28() V33() V43() ext-real non negative V70() V71() V72() V73() V74() V75() Element of NAT
2 to_power (k -' 1) is V11() V12() ext-real set
- (Radix (k -' 1)) is V11() V12() integer ext-real non positive set
(- (Radix (k -' 1))) - 1 is non empty V11() V12() integer ext-real non positive negative set
{ b₁ where b₁ is V11() V12() integer V43() ext-real Element of INT : ( (- (Radix (k -' 1))) - 1 <= b₁ & b₁ <= Radix (k -' 1) ) } is set
((n + 1),k,(n,k,(DecSD (x,n,k)))) is V11() V12() integer ext-real set
((n + 1),k,(n,k,(DecSD (x,n,k)))) is V15() V18( NAT ) V19( INT ) Function-like V35(n + 1) FinSequence-like V60() V61() V62() FinSequence of INT
Sum ((n + 1),k,(n,k,(DecSD (x,n,k)))) is V11() V12() integer V43() ext-real Element of INT