:: 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()