:: RADIX_1 semantic presentation

REAL is non empty V36() V61() V62() V63() V67() set
NAT is V6() V36() V41() V42() V61() V62() V63() V64() V65() V66() V67() Element of K6(REAL)
K6(REAL) is V36() set
COMPLEX is non empty V36() V61() V67() set
NAT is V6() V36() V41() V42() V61() V62() V63() V64() V65() V66() V67() set
K6(NAT) is V36() set
K6(NAT) is V36() set
K158(NAT) is V35() set
RAT is non empty V36() V61() V62() V63() V64() V67() set
INT is non empty V36() V61() V62() V63() V64() V65() V67() set
K7(REAL,REAL) is V36() V51() V52() V53() set
K6(K7(REAL,REAL)) is V36() set
K350() is V73() V101() L8()
the U1 of K350() is set
K7(COMPLEX,COMPLEX) is V36() V51() set
K6(K7(COMPLEX,COMPLEX)) is V36() set
K7(K7(COMPLEX,COMPLEX),COMPLEX) is V36() V51() set
K6(K7(K7(COMPLEX,COMPLEX),COMPLEX)) is V36() set
K7(K7(REAL,REAL),REAL) is V36() V51() V52() V53() set
K6(K7(K7(REAL,REAL),REAL)) is V36() set
K7(RAT,RAT) is V19( RAT ) V36() V51() V52() V53() set
K6(K7(RAT,RAT)) is V36() set
K7(K7(RAT,RAT),RAT) is V19( RAT ) V36() V51() V52() V53() set
K6(K7(K7(RAT,RAT),RAT)) is V36() set
K7(INT,INT) is V19( RAT ) V19( INT ) V36() V51() V52() V53() set
K6(K7(INT,INT)) is V36() set
K7(K7(INT,INT),INT) is V19( RAT ) V19( INT ) V36() V51() V52() V53() set
K6(K7(K7(INT,INT),INT)) is V36() set
K7(NAT,NAT) is V19( RAT ) V19( INT ) V51() V52() V53() V54() set
K7(K7(NAT,NAT),NAT) is V19( RAT ) V19( INT ) V51() V52() V53() V54() set
K6(K7(K7(NAT,NAT),NAT)) is set
{} is empty V6() functional V41() V43( {} ) FinSequence-membered V61() V62() V63() V64() V65() V66() V67() set
1 is non empty V6() V10() V11() V12() integer V36() V41() ext-real positive non negative V50() V61() V62() V63() V64() V65() V66() Element of NAT
2 is non empty V6() V10() V11() V12() integer V36() V41() ext-real positive non negative V50() V61() V62() V63() V64() V65() V66() Element of NAT
3 is non empty V6() V10() V11() V12() integer V36() V41() ext-real positive non negative V50() V61() V62() V63() V64() V65() V66() Element of NAT
0 is empty V6() V10() V11() V12() integer functional V36() V41() V43( {} ) FinSequence-membered ext-real non positive non negative V50() V61() V62() V63() V64() V65() V66() V67() Element of NAT
n is V6() V10() V11() V12() integer V36() V41() ext-real non negative set
k is V6() V10() V11() V12() integer V36() V41() ext-real non negative set
n mod k is V6() V10() V11() V12() integer V36() V41() ext-real non negative V50() V61() V62() V63() V64() V65() V66() Element of NAT
k - 1 is V11() V12() integer ext-real set
n + 1 is non empty V6() V10() V11() V12() integer V36() V41() ext-real positive non negative set
(n + 1) mod k is V6() V10() V11() V12() integer V36() V41() ext-real non negative V50() V61() V62() V63() V64() V65() V66() Element of NAT
k is V6() V10() V11() V12() integer V36() V41() ext-real non negative set
k - 1 is V11() V12() integer ext-real set
n is V6() V10() V11() V12() integer V36() V41() ext-real non negative set
n mod k is V6() V10() V11() V12() integer V36() V41() ext-real non negative V50() V61() V62() V63() V64() V65() V66() Element of NAT
n + 1 is non empty V6() V10() V11() V12() integer V36() V41() ext-real positive non negative set
(n + 1) mod k is V6() V10() V11() V12() integer V36() V41() ext-real non negative V50() V61() V62() V63() V64() V65() V66() Element of NAT
(n mod k) + 1 is non empty V6() V10() V11() V12() integer V36() V41() ext-real positive non negative set
n is V6() V10() V11() V12() integer V36() V41() ext-real non negative set
k is V6() V10() V11() V12() integer V36() V41() ext-real non negative set
x is V6() V10() V11() V12() integer V36() V41() ext-real non negative set
n * x is V6() V10() V11() V12() integer V36() V41() ext-real non negative set
k mod (n * x) is V6() V10() V11() V12() integer V36() V41() ext-real non negative V50() V61() V62() V63() V64() V65() V66() Element of NAT
(k mod (n * x)) mod x is V6() V10() V11() V12() integer V36() V41() ext-real non negative V50() V61() V62() V63() V64() V65() V66() Element of NAT
k mod x is V6() V10() V11() V12() integer V36() V41() ext-real non negative V50() V61() V62() V63() V64() V65() V66() Element of NAT
y is V11() V12() integer ext-real set
z is V11() V12() integer ext-real set
y * z is V11() V12() integer ext-real set
y is V11() V12() integer ext-real set
y div (y * z) is V11() V12() integer ext-real set
(y div (y * z)) * (y * z) is V11() V12() integer ext-real set
y - ((y div (y * z)) * (y * z)) is V11() V12() integer ext-real set
(y - ((y div (y * z)) * (y * z))) mod z is V11() V12() integer ext-real set
y * (y div (y * z)) is V11() V12() integer ext-real set
- (y * (y div (y * z))) is V11() V12() integer ext-real set
(- (y * (y div (y * z)))) * z is V11() V12() integer ext-real set
y + ((- (y * (y div (y * z)))) * z) is V11() V12() integer ext-real set
(y + ((- (y * (y div (y * z)))) * z)) mod z is V11() V12() integer ext-real set
n is V6() V10() V11() V12() integer V36() V41() ext-real non negative set
k is V6() V10() V11() V12() integer V36() V41() ext-real non negative set
k + 1 is non empty V6() V10() V11() V12() integer V36() V41() ext-real positive non negative set
(k + 1) mod n is V6() V10() V11() V12() integer V36() V41() ext-real non negative V50() V61() V62() V63() V64() V65() V66() Element of NAT
k mod n is V6() V10() V11() V12() integer V36() V41() ext-real non negative V50() V61() V62() V63() V64() V65() V66() Element of NAT
(k mod n) + 1 is non empty V6() V10() V11() V12() integer V36() V41() ext-real positive non negative set
n - 1 is V11() V12() integer ext-real set
(n - 1) + 1 is V11() V12() integer ext-real set
x is V6() V10() V11() V12() integer V36() V41() ext-real non negative V50() V61() V62() V63() V64() V65() V66() Element of NAT
n is V6() V10() V11() V12() integer V36() V41() ext-real non negative set
k is V6() V10() V11() V12() integer V36() V41() ext-real non negative set
n |^ k is V6() V10() V11() V12() integer V36() V41() ext-real non negative set
k -' 1 is V6() V10() V11() V12() integer V36() V41() ext-real non negative V50() V61() V62() V63() V64() V65() V66() Element of NAT
n |^ (k -' 1) is V6() V10() V11() V12() integer V36() V41() ext-real non negative set
x is V6() V10() V11() V12() integer V36() V41() ext-real non negative set
x mod (n |^ k) is V6() V10() V11() V12() integer V36() V41() ext-real non negative V50() V61() V62() V63() V64() V65() V66() Element of NAT
(x mod (n |^ k)) div (n |^ (k -' 1)) is V6() V10() V11() V12() integer V36() V41() ext-real non negative V50() V61() V62() V63() V64() V65() V66() Element of NAT
y is V6() V10() V11() V12() integer V36() V41() ext-real non negative V50() V61() V62() V63() V64() V65() V66() Element of NAT
z is V6() V10() V11() V12() integer V36() V41() ext-real non negative V50() V61() V62() V63() V64() V65() V66() Element of NAT
z -' 1 is V6() V10() V11() V12() integer V36() V41() ext-real non negative V50() V61() V62() V63() V64() V65() V66() Element of NAT
y |^ (z -' 1) is V6() V10() V11() V12() integer V36() V41() ext-real non negative V50() V61() V62() V63() V64() V65() V66() Element of NAT
y is V6() V10() V11() V12() integer V36() V41() ext-real non negative V50() V61() V62() V63() V64() V65() V66() Element of NAT
y |^ z is V6() V10() V11() V12() integer V36() V41() ext-real non negative V50() V61() V62() V63() V64() V65() V66() Element of NAT
y mod (y |^ z) is V6() V10() V11() V12() integer V36() V41() ext-real non negative V50() V61() V62() V63() V64() V65() V66() Element of NAT
y * (y |^ (z -' 1)) is V6() V10() V11() V12() integer V36() V41() ext-real non negative set
(y mod (y |^ z)) mod (y |^ (z -' 1)) is V6() V10() V11() V12() integer V36() V41() ext-real non negative V50() V61() V62() V63() V64() V65() V66() Element of NAT
y mod (y |^ (z -' 1)) is V6() V10() V11() V12() integer V36() V41() ext-real non negative V50() V61() V62() V63() V64() V65() V66() Element of NAT
y div (y |^ (z -' 1)) is V6() V10() V11() V12() integer V36() V41() ext-real non negative V50() V61() V62() V63() V64() V65() V66() Element of NAT
(y |^ (z -' 1)) * (y div (y |^ (z -' 1))) is V6() V10() V11() V12() integer V36() V41() ext-real non negative set
y - ((y |^ (z -' 1)) * (y div (y |^ (z -' 1)))) is V11() V12() integer ext-real set
(y mod (y |^ z)) div (y |^ (z -' 1)) is V6() V10() V11() V12() integer V36() V41() ext-real non negative V50() V61() V62() V63() V64() V65() V66() Element of NAT
(y |^ (z -' 1)) * ((y mod (y |^ z)) div (y |^ (z -' 1))) is V6() V10() V11() V12() integer V36() V41() ext-real non negative set
((y |^ (z -' 1)) * ((y mod (y |^ z)) div (y |^ (z -' 1)))) + (y - ((y |^ (z -' 1)) * (y div (y |^ (z -' 1))))) is V11() V12() integer ext-real set
y / (y |^ (z -' 1)) is V11() V12() ext-real non negative set
[\(y / (y |^ (z -' 1)))/] is V11() V12() integer ext-real set
((y mod (y |^ z)) div (y |^ (z -' 1))) + [\(y / (y |^ (z -' 1)))/] is V11() V12() integer ext-real set
((y mod (y |^ z)) div (y |^ (z -' 1))) + (y / (y |^ (z -' 1))) is V11() V12() ext-real non negative set
(((y mod (y |^ z)) div (y |^ (z -' 1))) + [\(y / (y |^ (z -' 1)))/]) - [\(y / (y |^ (z -' 1)))/] is V11() V12() integer ext-real set
(((y mod (y |^ z)) div (y |^ (z -' 1))) + (y / (y |^ (z -' 1)))) - (y div (y |^ (z -' 1))) is V11() V12() ext-real set
(y * (y |^ (z -' 1))) / (y |^ (z -' 1)) is V11() V12() ext-real non negative set
((y |^ (z -' 1)) * ((y mod (y |^ z)) div (y |^ (z -' 1)))) + y is V6() V10() V11() V12() integer V36() V41() ext-real non negative set
(((y |^ (z -' 1)) * ((y mod (y |^ z)) div (y |^ (z -' 1)))) + y) - ((y |^ (z -' 1)) * (y div (y |^ (z -' 1)))) is V11() V12() integer ext-real set
((((y |^ (z -' 1)) * ((y mod (y |^ z)) div (y |^ (z -' 1)))) + y) - ((y |^ (z -' 1)) * (y div (y |^ (z -' 1))))) / (y |^ (z -' 1)) is V11() V12() ext-real set
((y |^ (z -' 1)) * ((y mod (y |^ z)) div (y |^ (z -' 1)))) / (y |^ (z -' 1)) is V11() V12() ext-real non negative set
(((y |^ (z -' 1)) * ((y mod (y |^ z)) div (y |^ (z -' 1)))) / (y |^ (z -' 1))) + (y / (y |^ (z -' 1))) is V11() V12() ext-real non negative set
((y |^ (z -' 1)) * (y div (y |^ (z -' 1)))) / (y |^ (z -' 1)) is V11() V12() ext-real non negative set
((((y |^ (z -' 1)) * ((y mod (y |^ z)) div (y |^ (z -' 1)))) / (y |^ (z -' 1))) + (y / (y |^ (z -' 1)))) - (((y |^ (z -' 1)) * (y div (y |^ (z -' 1)))) / (y |^ (z -' 1))) is V11() V12() ext-real set
(((y mod (y |^ z)) div (y |^ (z -' 1))) + (y / (y |^ (z -' 1)))) - (((y |^ (z -' 1)) * (y div (y |^ (z -' 1)))) / (y |^ (z -' 1))) is V11() V12() ext-real set
n is V11() V12() integer ext-real set
k is V11() V12() integer ext-real set
n * k is V11() V12() integer ext-real set
x is V11() V12() integer ext-real set
x mod (n * k) is V11() V12() integer ext-real set
(x mod (n * k)) mod k is V11() V12() integer ext-real set
x mod k is V11() V12() integer ext-real set
x div (n * k) is V11() V12() integer ext-real set
(x div (n * k)) * (n * k) is V11() V12() integer ext-real set
x - ((x div (n * k)) * (n * k)) is V11() V12() integer ext-real set
(x - ((x div (n * k)) * (n * k))) mod k is V11() V12() integer ext-real set
n * (x div (n * k)) is V11() V12() integer ext-real set
- (n * (x div (n * k))) is V11() V12() integer ext-real set
(- (n * (x div (n * k)))) * k is V11() V12() integer ext-real set
x + ((- (n * (x div (n * k)))) * k) is V11() V12() integer ext-real set
(x + ((- (n * (x div (n * k)))) * k)) mod k is V11() V12() integer ext-real set
n is V6() V10() V11() V12() integer V36() V41() ext-real non negative set
2 to_power n is V11() V12() ext-real set
2 |^ n is V6() V10() V11() V12() integer V36() V41() ext-real non negative set
n is V6() V10() V11() V12() integer V36() V41() ext-real non negative set
(n) is V6() V10() V11() V12() integer V36() V41() ext-real non negative V50() V61() V62() V63() V64() V65() V66() Element of NAT
2 to_power n is V11() V12() ext-real set
2 |^ n is V6() V10() V11() V12() integer V36() V41() ext-real non negative set
(n) - 1 is V11() V12() integer ext-real set
- (n) is V11() V12() integer ext-real non positive set
(- (n)) + 1 is V11() V12() integer ext-real set
{ b₁ where b₁ is V11() V12() integer ext-real V50() Element of INT : ( b₁ <= (n) - 1 & (- (n)) + 1 <= b₁ ) } is set
2 + 2 is non empty V6() V10() V11() V12() integer V36() V41() ext-real positive non negative set
n is V6() V10() V11() V12() integer V36() V41() ext-real non negative set
(n) is V6() V10() V11() V12() integer V36() V41() ext-real non negative V50() V61() V62() V63() V64() V65() V66() Element of NAT
2 to_power n is V11() V12() ext-real set
2 |^ n is V6() V10() V11() V12() integer V36() V41() ext-real non negative set
k is V6() V10() V11() V12() integer V36() V41() ext-real non negative set
(k) is V6() V10() V11() V12() integer V36() V41() ext-real non negative V50() V61() V62() V63() V64() V65() V66() Element of NAT
2 to_power k is V11() V12() ext-real set
2 |^ k is V6() V10() V11() V12() integer V36() V41() ext-real non negative set
k + 1 is non empty V6() V10() V11() V12() integer V36() V41() ext-real positive non negative set
((k + 1)) is V6() V10() V11() V12() integer V36() V41() ext-real non negative V50() V61() V62() V63() V64() V65() V66() Element of NAT
2 to_power (k + 1) is V11() V12() ext-real set
2 |^ (k + 1) is V6() V10() V11() V12() integer V36() V41() ext-real non negative set
2 to_power 1 is V11() V12() ext-real Element of REAL
2 |^ 1 is V6() V10() V11() V12() integer V36() V41() ext-real non negative set
(2 to_power k) * (2 to_power 1) is V11() V12() ext-real set
(k) * 2 is V6() V10() V11() V12() integer V36() V41() ext-real non negative set
(2) is V6() V10() V11() V12() integer V36() V41() ext-real non negative V50() V61() V62() V63() V64() V65() V66() Element of NAT
2 to_power 2 is V11() V12() ext-real set
2 |^ 2 is V6() V10() V11() V12() integer V36() V41() ext-real non negative set
1 + 1 is non empty V6() V10() V11() V12() integer V36() V41() ext-real positive non negative set
2 to_power (1 + 1) is V11() V12() ext-real set
2 |^ (1 + 1) is V6() V10() V11() V12() integer V36() V41() ext-real non negative set
2 to_power 1 is V11() V12() ext-real Element of REAL
2 |^ 1 is V6() V10() V11() V12() integer V36() V41() ext-real non negative set
(2 to_power 1) * (2 to_power 1) is V11() V12() ext-real set
2 * (2 to_power 1) is V11() V12() ext-real set
2 * 2 is V6() V10() V11() V12() integer V36() V41() ext-real non negative set
(0) is set
(0) is V6() V10() V11() V12() integer V36() V41() ext-real non negative V50() V61() V62() V63() V64() V65() V66() Element of NAT
2 to_power 0 is V11() V12() ext-real set
2 |^ 0 is V6() V10() V11() V12() integer V36() V41() ext-real non negative set
(0) - 1 is V11() V12() integer ext-real set
- (0) is V11() V12() integer ext-real non positive set
(- (0)) + 1 is V11() V12() integer ext-real set
{ b₁ where b₁ is V11() V12() integer ext-real V50() Element of INT : ( b₁ <= (0) - 1 & (- (0)) + 1 <= b₁ ) } is set
n is set
k is V11() V12() integer ext-real V50() Element of INT
{0} is non empty V2() V43(1) V61() V62() V63() V64() V65() V66() set
n is V6() V10() V11() V12() integer V36() V41() ext-real non negative set
(n) is set
(n) is V6() V10() V11() V12() integer V36() V41() ext-real non negative V50() V61() V62() V63() V64() V65() V66() Element of NAT
2 to_power n is V11() V12() ext-real set
2 |^ n is V6() V10() V11() V12() integer V36() V41() ext-real non negative set
(n) - 1 is V11() V12() integer ext-real set
- (n) is V11() V12() integer ext-real non positive set
(- (n)) + 1 is V11() V12() integer ext-real set
{ b₁ where b₁ is V11() V12() integer ext-real V50() Element of INT : ( b₁ <= (n) - 1 & (- (n)) + 1 <= b₁ ) } is set
n + 1 is non empty V6() V10() V11() V12() integer V36() V41() ext-real positive non negative set
((n + 1)) is set
((n + 1)) is V6() V10() V11() V12() integer V36() V41() ext-real non negative V50() V61() V62() V63() V64() V65() V66() Element of NAT
2 to_power (n + 1) is V11() V12() ext-real set
2 |^ (n + 1) is V6() V10() V11() V12() integer V36() V41() ext-real non negative set
((n + 1)) - 1 is V11() V12() integer ext-real set
- ((n + 1)) is V11() V12() integer ext-real non positive set
(- ((n + 1))) + 1 is V11() V12() integer ext-real set
{ b₁ where b₁ is V11() V12() integer ext-real V50() Element of INT : ( b₁ <= ((n + 1)) - 1 & (- ((n + 1))) + 1 <= b₁ ) } is set
k is set
x is V11() V12() integer ext-real V50() Element of INT
n is set
k is V6() V10() V11() V12() integer V36() V41() ext-real non negative set
(k) is set
(k) is V6() V10() V11() V12() integer V36() V41() ext-real non negative V50() V61() V62() V63() V64() V65() V66() Element of NAT
2 to_power k is V11() V12() ext-real set
2 |^ k is V6() V10() V11() V12() integer V36() V41() ext-real non negative set
(k) - 1 is V11() V12() integer ext-real set
- (k) is V11() V12() integer ext-real non positive set
(- (k)) + 1 is V11() V12() integer ext-real set
{ b₁ where b₁ is V11() V12() integer ext-real V50() Element of INT : ( b₁ <= (k) - 1 & (- (k)) + 1 <= b₁ ) } is set
x is V11() V12() integer ext-real V50() Element of INT
n is V6() V10() V11() V12() integer V36() V41() ext-real non negative set
(n) is set
(n) is V6() V10() V11() V12() integer V36() V41() ext-real non negative V50() V61() V62() V63() V64() V65() V66() Element of NAT
2 to_power n is V11() V12() ext-real set
2 |^ n is V6() V10() V11() V12() integer V36() V41() ext-real non negative set
(n) - 1 is V11() V12() integer ext-real set
- (n) is V11() V12() integer ext-real non positive set
(- (n)) + 1 is V11() V12() integer ext-real set
{ b₁ where b₁ is V11() V12() integer ext-real V50() Element of INT : ( b₁ <= (n) - 1 & (- (n)) + 1 <= b₁ ) } is set
k is set
n is V11() V12() integer ext-real set
k is V6() V10() V11() V12() integer V36() V41() ext-real non negative set
(k) is set
(k) is V6() V10() V11() V12() integer V36() V41() ext-real non negative V50() V61() V62() V63() V64() V65() V66() Element of NAT
2 to_power k is V11() V12() ext-real set
2 |^ k is V6() V10() V11() V12() integer V36() V41() ext-real non negative set
(k) - 1 is V11() V12() integer ext-real set
- (k) is V11() V12() integer ext-real non positive set
(- (k)) + 1 is V11() V12() integer ext-real set
{ b₁ where b₁ is V11() V12() integer ext-real V50() Element of INT : ( b₁ <= (k) - 1 & (- (k)) + 1 <= b₁ ) } is set
x is V11() V12() integer ext-real V50() Element of INT
n is V6() V10() V11() V12() integer V36() V41() ext-real non negative set
(n) is set
(n) is V6() V10() V11() V12() integer V36() V41() ext-real non negative V50() V61() V62() V63() V64() V65() V66() Element of NAT
2 to_power n is V11() V12() ext-real set
2 |^ n is V6() V10() V11() V12() integer V36() V41() ext-real non negative set
(n) - 1 is V11() V12() integer ext-real set
- (n) is V11() V12() integer ext-real non positive set
(- (n)) + 1 is V11() V12() integer ext-real set
{ b₁ where b₁ is V11() V12() integer ext-real V50() Element of INT : ( b₁ <= (n) - 1 & (- (n)) + 1 <= b₁ ) } is set
k is V6() V10() V11() V12() integer V36() V41() ext-real non negative set
(k) is set
(k) is V6() V10() V11() V12() integer V36() V41() ext-real non negative V50() V61() V62() V63() V64() V65() V66() Element of NAT
2 to_power k is V11() V12() ext-real set
2 |^ k is V6() V10() V11() V12() integer V36() V41() ext-real non negative set
(k) - 1 is V11() V12() integer ext-real set
- (k) is V11() V12() integer ext-real non positive set
(- (k)) + 1 is V11() V12() integer ext-real set
{ b₁ where b₁ is V11() V12() integer ext-real V50() Element of INT : ( b₁ <= (k) - 1 & (- (k)) + 1 <= b₁ ) } is set
k + 1 is non empty V6() V10() V11() V12() integer V36() V41() ext-real positive non negative set
((k + 1)) is set
((k + 1)) is V6() V10() V11() V12() integer V36() V41() ext-real non negative V50() V61() V62() V63() V64() V65() V66() Element of NAT
2 to_power (k + 1) is V11() V12() ext-real set
2 |^ (k + 1) is V6() V10() V11() V12() integer V36() V41() ext-real non negative set
((k + 1)) - 1 is V11() V12() integer ext-real set
- ((k + 1)) is V11() V12() integer ext-real non positive set
(- ((k + 1))) + 1 is V11() V12() integer ext-real set
{ b₁ where b₁ is V11() V12() integer ext-real V50() Element of INT : ( b₁ <= ((k + 1)) - 1 & (- ((k + 1))) + 1 <= b₁ ) } is set
n is V6() V10() V11() V12() integer V36() V41() ext-real non negative set
(n) is set
(n) is V6() V10() V11() V12() integer V36() V41() ext-real non negative V50() V61() V62() V63() V64() V65() V66() Element of NAT
2 to_power n is V11() V12() ext-real set
2 |^ n is V6() V10() V11() V12() integer V36() V41() ext-real non negative set
(n) - 1 is V11() V12() integer ext-real set
- (n) is V11() V12() integer ext-real non positive set
(- (n)) + 1 is V11() V12() integer ext-real set
{ b₁ where b₁ is V11() V12() integer ext-real V50() Element of INT : ( b₁ <= (n) - 1 & (- (n)) + 1 <= b₁ ) } is set
n is V6() V10() V11() V12() integer V36() V41() ext-real non negative set
(n) is non empty set
(n) is V6() V10() V11() V12() integer V36() V41() ext-real non negative V50() V61() V62() V63() V64() V65() V66() Element of NAT
2 to_power n is V11() V12() ext-real set
2 |^ n is V6() V10() V11() V12() integer V36() V41() ext-real non negative set
(n) - 1 is V11() V12() integer ext-real set
- (n) is V11() V12() integer ext-real non positive set
(- (n)) + 1 is V11() V12() integer ext-real set
{ b₁ where b₁ is V11() V12() integer ext-real V50() Element of INT : ( b₁ <= (n) - 1 & (- (n)) + 1 <= b₁ ) } is set
K6(INT) is V36() set
n is V6() V10() V11() V12() integer V36() V41() ext-real non negative set
k is V6() V10() V11() V12() integer V36() V41() ext-real non negative set
Seg k is V36() V43(k) V61() V62() V63() V64() V65() V66() Element of K6(NAT)
x is V6() V10() V11() V12() integer V36() V41() ext-real non negative set
(x) is non empty V61() V62() V63() V64() V65() Element of K6(INT)
(x) is V6() V10() V11() V12() integer V36() V41() ext-real non negative V50() V61() V62() V63() V64() V65() V66() Element of NAT
2 to_power x is V11() V12() ext-real set
2 |^ x is V6() V10() V11() V12() integer V36() V41() ext-real non negative set
(x) - 1 is V11() V12() integer ext-real set
- (x) is V11() V12() integer ext-real non positive set
(- (x)) + 1 is V11() V12() integer ext-real set
{ b₁ where b₁ is V11() V12() integer ext-real V50() Element of INT : ( b₁ <= (x) - 1 & (- (x)) + 1 <= b₁ ) } is set
y is V15() V18( NAT ) V19((x)) Function-like V36() V43(k) FinSequence-like FinSubsequence-like V51() V52() V53() FinSequence of (x)
y . n is V11() V12() ext-real set
len y is V6() V10() V11() V12() integer V36() V41() ext-real non negative V50() V61() V62() V63() V64() V65() V66() Element of NAT
dom y is V43(k) V61() V62() V63() V64() V65() V66() Element of K6(NAT)
rng y is V61() V62() V63() Element of K6(REAL)
x is V6() V10() V11() V12() integer V36() V41() ext-real non negative set
k is V6() V10() V11() V12() integer V36() V41() ext-real non negative set
(k) is non empty V61() V62() V63() V64() V65() Element of K6(INT)
(k) is V6() V10() V11() V12() integer V36() V41() ext-real non negative V50() V61() V62() V63() V64() V65() V66() Element of NAT
2 to_power k is V11() V12() ext-real set
2 |^ k is V6() V10() V11() V12() integer V36() V41() ext-real non negative set
(k) - 1 is V11() V12() integer ext-real set
- (k) is V11() V12() integer ext-real non positive set
(- (k)) + 1 is V11() V12() integer ext-real set
{ b₁ where b₁ is V11() V12() integer ext-real V50() Element of INT : ( b₁ <= (k) - 1 & (- (k)) + 1 <= b₁ ) } is set
n is V6() V10() V11() V12() integer V36() V41() ext-real non negative set
Seg x is V36() V43(x) V61() V62() V63() V64() V65() V66() Element of K6(NAT)
y is V15() V18( NAT ) V19((k)) Function-like V36() V43(x) FinSequence-like FinSubsequence-like V51() V52() V53() FinSequence of (k)
y . n is V11() V12() ext-real set
y is V11() V12() integer ext-real set
x is V6() V10() V11() V12() integer V36() V41() ext-real non negative set
k is V6() V10() V11() V12() integer V36() V41() ext-real non negative set
(k) is non empty V61() V62() V63() V64() V65() Element of K6(INT)
(k) is V6() V10() V11() V12() integer V36() V41() ext-real non negative V50() V61() V62() V63() V64() V65() V66() Element of NAT
2 to_power k is V11() V12() ext-real set
2 |^ k is V6() V10() V11() V12() integer V36() V41() ext-real non negative set
(k) - 1 is V11() V12() integer ext-real set
- (k) is V11() V12() integer ext-real non positive set
(- (k)) + 1 is V11() V12() integer ext-real set
{ b₁ where b₁ is V11() V12() integer ext-real V50() Element of INT : ( b₁ <= (k) - 1 & (- (k)) + 1 <= b₁ ) } is set
n is V6() V10() V11() V12() integer V36() V41() ext-real non negative set
y is V15() V18( NAT ) V19((k)) Function-like V36() V43(x) FinSequence-like FinSubsequence-like V51() V52() V53() FinSequence of (k)
(n,k,x,y) is V11() V12() integer ext-real set
n is V6() V10() V11() V12() integer V36() V41() ext-real non negative set
k is V6() V10() V11() V12() integer V36() V41() ext-real non negative set
Seg k is V36() V43(k) V61() V62() V63() V64() V65() V66() Element of K6(NAT)
x is V6() V10() V11() V12() integer V36() V41() ext-real non negative set
(x) is non empty V61() V62() V63() V64() V65() Element of K6(INT)
(x) is V6() V10() V11() V12() integer V36() V41() ext-real non negative V50() V61() V62() V63() V64() V65() V66() Element of NAT
2 to_power x is V11() V12() ext-real set
2 |^ x is V6() V10() V11() V12() integer V36() V41() ext-real non negative set
(x) - 1 is V11() V12() integer ext-real set
- (x) is V11() V12() integer ext-real non positive set
(- (x)) + 1 is V11() V12() integer ext-real set
{ b₁ where b₁ is V11() V12() integer ext-real V50() Element of INT : ( b₁ <= (x) - 1 & (- (x)) + 1 <= b₁ ) } is set
y is V15() V18( NAT ) V19((x)) Function-like V36() V43(k) FinSequence-like FinSubsequence-like V51() V52() V53() FinSequence of (x)
(n,x,k,y) is V11() V12() integer ext-real set
y . n is V11() V12() ext-real set
n is V6() V10() V11() V12() integer V36() V41() ext-real non negative set
<*n*> is non empty V2() V15() V18( NAT ) Function-like V36() V43(1) FinSequence-like FinSubsequence-like set
k is non empty V2() V15() V18( NAT ) V19( INT ) Function-like one-to-one V36() V43(1) FinSequence-like FinSubsequence-like V51() V52() V53() V55() V56() V57() V58() FinSequence of INT
k /. 1 is V11() V12() integer ext-real V50() Element of INT
len k is non empty V6() V10() V11() V12() integer V36() V41() ext-real positive non negative V50() V61() V62() V63() V64() V65() V66() Element of NAT
k . 1 is V11() V12() integer ext-real set
x is V6() V10() V11() V12() integer V36() V41() ext-real non negative set
k is V6() V10() V11() V12() integer V36() V41() ext-real non negative set
(k) is non empty V61() V62() V63() V64() V65() Element of K6(INT)
(k) is V6() V10() V11() V12() integer V36() V41() ext-real non negative V50() V61() V62() V63() V64() V65() V66() Element of NAT
2 to_power k is V11() V12() ext-real set
2 |^ k is V6() V10() V11() V12() integer V36() V41() ext-real non negative set
(k) - 1 is V11() V12() integer ext-real set
- (k) is V11() V12() integer ext-real non positive set
(- (k)) + 1 is V11() V12() integer ext-real set
{ b₁ where b₁ is V11() V12() integer ext-real V50() Element of INT : ( b₁ <= (k) - 1 & (- (k)) + 1 <= b₁ ) } is set
n is V6() V10() V11() V12() integer V36() V41() ext-real non negative set
n -' 1 is V6() V10() V11() V12() integer V36() V41() ext-real non negative V50() V61() V62() V63() V64() V65() V66() Element of NAT
(k) |^ (n -' 1) is V6() V10() V11() V12() integer V36() V41() ext-real non negative V50() V61() V62() V63() V64() V65() V66() Element of NAT
y is V15() V18( NAT ) V19((k)) Function-like V36() V43(x) FinSequence-like FinSubsequence-like V51() V52() V53() FinSequence of (k)
(n,k,x,y) is V11() V12() integer ext-real V50() Element of INT
(n,k,x,y) is V11() V12() integer ext-real set
((k) |^ (n -' 1)) * (n,k,x,y) is V11() V12() integer ext-real set
n is V6() V10() V11() V12() integer V36() V41() ext-real non negative set
k is V6() V10() V11() V12() integer V36() V41() ext-real non negative set
(k) is non empty V61() V62() V63() V64() V65() Element of K6(INT)
(k) is V6() V10() V11() V12() integer V36() V41() ext-real non negative V50() V61() V62() V63() V64() V65() V66() Element of NAT
2 to_power k is V11() V12() ext-real set
2 |^ k is V6() V10() V11() V12() integer V36() V41() ext-real non negative set
(k) - 1 is V11() V12() integer ext-real set
- (k) is V11() V12() integer ext-real non positive set
(- (k)) + 1 is V11() V12() integer ext-real set
{ b₁ where b₁ is V11() V12() integer ext-real V50() Element of INT : ( b₁ <= (k) - 1 & (- (k)) + 1 <= b₁ ) } is set
Seg n is V36() V43(n) V61() V62() V63() V64() V65() V66() Element of K6(NAT)
x is V15() V18( NAT ) V19((k)) Function-like V36() V43(n) FinSequence-like FinSubsequence-like V51() V52() V53() FinSequence of (k)
y is V15() V18( NAT ) V19( INT ) Function-like V36() FinSequence-like FinSubsequence-like V51() V52() V53() FinSequence of INT
len y is V6() V10() V11() V12() integer V36() V41() ext-real non negative V50() V61() V62() V63() V64() V65() V66() Element of NAT
dom y is V61() V62() V63() V64() V65() V66() Element of K6(NAT)
y is V15() V18( NAT ) V19( INT ) Function-like V36() V43(n) FinSequence-like FinSubsequence-like V51() V52() V53() FinSequence of INT
z is V6() V10() V11() V12() integer V36() V41() ext-real non negative set
y /. z is V11() V12() integer ext-real V50() Element of INT
(z,k,n,x) is V11() V12() integer ext-real V50() Element of INT
z -' 1 is V6() V10() V11() V12() integer V36() V41() ext-real non negative V50() V61() V62() V63() V64() V65() V66() Element of NAT
(k) |^ (z -' 1) is V6() V10() V11() V12() integer V36() V41() ext-real non negative V50() V61() V62() V63() V64() V65() V66() Element of NAT
(z,k,n,x) is V11() V12() integer ext-real V50() Element of INT
(z,k,n,x) is V11() V12() integer ext-real set
((k) |^ (z -' 1)) * (z,k,n,x) is V11() V12() integer ext-real set
dom y is V43(n) V61() V62() V63() V64() V65() V66() Element of K6(NAT)
y . z is V11() V12() integer ext-real set
y is V15() V18( NAT ) V19( INT ) Function-like V36() V43(n) FinSequence-like FinSubsequence-like V51() V52() V53() FinSequence of INT
y is V15() V18( NAT ) V19( INT ) Function-like V36() V43(n) FinSequence-like FinSubsequence-like V51() V52() V53() FinSequence of INT
len y is V6() V10() V11() V12() integer V36() V41() ext-real non negative V50() V61() V62() V63() V64() V65() V66() Element of NAT
dom y is V43(n) V61() V62() V63() V64() V65() V66() Element of K6(NAT)
len y is V6() V10() V11() V12() integer V36() V41() ext-real non negative V50() V61() V62() V63() V64() V65() V66() Element of NAT
z is V6() V10() V11() V12() integer V36() V41() ext-real non negative set
dom y is V43(n) V61() V62() V63() V64() V65() V66() Element of K6(NAT)
y . z is V11() V12() integer ext-real set
y /. z is V11() V12() integer ext-real V50() Element of INT
(z,k,n,x) is V11() V12() integer ext-real V50() Element of INT
z -' 1 is V6() V10() V11() V12() integer V36() V41() ext-real non negative V50() V61() V62() V63() V64() V65() V66() Element of NAT
(k) |^ (z -' 1) is V6() V10() V11() V12() integer V36() V41() ext-real non negative V50() V61() V62() V63() V64() V65() V66() Element of NAT
(z,k,n,x) is V11() V12() integer ext-real V50() Element of INT
(z,k,n,x) is V11() V12() integer ext-real set
((k) |^ (z -' 1)) * (z,k,n,x) is V11() V12() integer ext-real set
y /. z is V11() V12() integer ext-real V50() Element of INT
y . z is V11() V12() integer ext-real set
n is V6() V10() V11() V12() integer V36() V41() ext-real non negative set
k is V6() V10() V11() V12() integer V36() V41() ext-real non negative set
(k) is non empty V61() V62() V63() V64() V65() Element of K6(INT)
(k) is V6() V10() V11() V12() integer V36() V41() ext-real non negative V50() V61() V62() V63() V64() V65() V66() Element of NAT
2 to_power k is V11() V12() ext-real set
2 |^ k is V6() V10() V11() V12() integer V36() V41() ext-real non negative set
(k) - 1 is V11() V12() integer ext-real set
- (k) is V11() V12() integer ext-real non positive set
(- (k)) + 1 is V11() V12() integer ext-real set
{ b₁ where b₁ is V11() V12() integer ext-real V50() Element of INT : ( b₁ <= (k) - 1 & (- (k)) + 1 <= b₁ ) } is set
x is V15() V18( NAT ) V19((k)) Function-like V36() V43(n) FinSequence-like FinSubsequence-like V51() V52() V53() FinSequence of (k)
(n,k,x) is V15() V18( NAT ) V19( INT ) Function-like V36() V43(n) FinSequence-like FinSubsequence-like V51() V52() V53() FinSequence of INT
Sum (n,k,x) is V11() V12() integer ext-real V50() Element of INT
x is V6() V10() V11() V12() integer V36() V41() ext-real non negative set
k is V6() V10() V11() V12() integer V36() V41() ext-real non negative set
(k) is V6() V10() V11() V12() integer V36() V41() ext-real non negative V50() V61() V62() V63() V64() V65() V66() Element of NAT
2 to_power k is V11() V12() ext-real set
2 |^ k is V6() V10() V11() V12() integer V36() V41() ext-real non negative set
n is V6() V10() V11() V12() integer V36() V41() ext-real non negative set
(k) |^ n is V6() V10() V11() V12() integer V36() V41() ext-real non negative set
x mod ((k) |^ n) is V6() V10() V11() V12() integer V36() V41() ext-real non negative V50() V61() V62() V63() V64() V65() V66() Element of NAT
n -' 1 is V6() V10() V11() V12() integer V36() V41() ext-real non negative V50() V61() V62() V63() V64() V65() V66() Element of NAT
(k) |^ (n -' 1) is V6() V10() V11() V12() integer V36() V41() ext-real non negative V50() V61() V62() V63() V64() V65() V66() Element of NAT
(x mod ((k) |^ n)) div ((k) |^ (n -' 1)) is V6() V10() V11() V12() integer V36() V41() ext-real non negative V50() V61() V62() V63() V64() V65() V66() Element of NAT
(k) is non empty V61() V62() V63() V64() V65() Element of K6(INT)
(k) - 1 is V11() V12() integer ext-real set
- (k) is V11() V12() integer ext-real non positive set
(- (k)) + 1 is V11() V12() integer ext-real set
{ b₁ where b₁ is V11() V12() integer ext-real V50() Element of INT : ( b₁ <= (k) - 1 & (- (k)) + 1 <= b₁ ) } is set
y is V6() V10() V11() V12() integer V36() V41() ext-real non negative V50() V61() V62() V63() V64() V65() V66() Element of NAT
(y) is V6() V10() V11() V12() integer V36() V41() ext-real non negative V50() V61() V62() V63() V64() V65() V66() Element of NAT
2 to_power y is V11() V12() ext-real set
2 |^ y is V6() V10() V11() V12() integer V36() V41() ext-real non negative set
y is V6() V10() V11() V12() integer V36() V41() ext-real non negative V50() V61() V62() V63() V64() V65() V66() Element of NAT
(y) |^ y is V6() V10() V11() V12() integer V36() V41() ext-real non negative V50() V61() V62() V63() V64() V65() V66() Element of NAT
y -' 1 is V6() V10() V11() V12() integer V36() V41() ext-real non negative V50() V61() V62() V63() V64() V65() V66() Element of NAT
(y) |^ (y -' 1) is V6() V10() V11() V12() integer V36() V41() ext-real non negative V50() V61() V62() V63() V64() V65() V66() Element of NAT
(y) is non empty V61() V62() V63() V64() V65() Element of K6(INT)
(y) - 1 is V11() V12() integer ext-real set
- (y) is V11() V12() integer ext-real non positive set
(- (y)) + 1 is V11() V12() integer ext-real set
{ b₁ where b₁ is V11() V12() integer ext-real V50() Element of INT : ( b₁ <= (y) - 1 & (- (y)) + 1 <= b₁ ) } is set
0 div ((y) |^ (y -' 1)) is V6() V10() V11() V12() integer V36() V41() ext-real non negative V50() V61() V62() V63() V64() V65() V66() Element of NAT
zn is V6() V10() V11() V12() integer V36() V41() ext-real non negative set
zn mod ((y) |^ y) is V6() V10() V11() V12() integer V36() V41() ext-real non negative V50() V61() V62() V63() V64() V65() V66() Element of NAT
(zn mod ((y) |^ y)) div ((y) |^ (y -' 1)) is V6() V10() V11() V12() integer V36() V41() ext-real non negative V50() V61() V62() V63() V64() V65() V66() Element of NAT
zn + 1 is non empty V6() V10() V11() V12() integer V36() V41() ext-real positive non negative set
(zn + 1) mod ((y) |^ y) is V6() V10() V11() V12() integer V36() V41() ext-real non negative V50() V61() V62() V63() V64() V65() V66() Element of NAT
((zn + 1) mod ((y) |^ y)) div ((y) |^ (y -' 1)) is V6() V10() V11() V12() integer V36() V41() ext-real non negative V50() V61() V62() V63() V64() V65() V66() Element of NAT
(y) to_power y is V11() V12() ext-real set
(y) |^ y is V6() V10() V11() V12() integer V36() V41() ext-real non negative set
(zn + 1) * 1 is V6() V10() V11() V12() integer V36() V41() ext-real non negative set
((zn + 1) * 1) mod 1 is V6() V10() V11() V12() integer V36() V41() ext-real non negative V50() V61() V62() V63() V64() V65() V66() Element of NAT
- 1 is V11() V12() integer ext-real non positive set
((y) - 1) + 1 is V11() V12() integer ext-real set
xn is V6() V10() V11() V12() integer V36() V41() ext-real non negative V50() V61() V62() V63() V64() V65() V66() Element of NAT
0 mod ((y) |^ y) is V6() V10() V11() V12() integer V36() V41() ext-real non negative V50() V61() V62() V63() V64() V65() V66() Element of NAT
(0 mod ((y) |^ y)) div ((y) |^ (y -' 1)) is V6() V10() V11() V12() integer V36() V41() ext-real non negative V50() V61() V62() V63() V64() V65() V66() Element of NAT
k is V6() V10() V11() V12() integer V36() V41() ext-real non negative set
n is V6() V10() V11() V12() integer V36() V41() ext-real non negative set
(n) is non empty V61() V62() V63() V64() V65() Element of K6(INT)
(n) is V6() V10() V11() V12() integer V36() V41() ext-real non negative V50() V61() V62() V63() V64() V65() V66() Element of NAT
2 to_power n is V11() V12() ext-real set
2 |^ n is V6() V10() V11() V12() integer V36() V41() ext-real non negative set
(n) - 1 is V11() V12() integer ext-real set
- (n) is V11() V12() integer ext-real non positive set
(- (n)) + 1 is V11() V12() integer ext-real set
{ b₁ where b₁ is V11() V12() integer ext-real V50() Element of INT : ( b₁ <= (n) - 1 & (- (n)) + 1 <= b₁ ) } is set
Seg k is V36() V43(k) V61() V62() V63() V64() V65() V66() Element of K6(NAT)
x is V6() V10() V11() V12() integer V36() V41() ext-real non negative set
y is V15() V18( NAT ) V19((n)) Function-like V36() FinSequence-like FinSubsequence-like V51() V52() V53() FinSequence of (n)
len y is V6() V10() V11() V12() integer V36() V41() ext-real non negative V50() V61() V62() V63() V64() V65() V66() Element of NAT
dom y is V61() V62() V63() V64() V65() V66() Element of K6(NAT)
y is V15() V18( NAT ) V19((n)) Function-like V36() V43(k) FinSequence-like FinSubsequence-like V51() V52() V53() FinSequence of (n)
z is V6() V10() V11() V12() integer V36() V41() ext-real non negative set
(z,n,k,y) is V11() V12() integer ext-real set
(z,n,x) is V11() V12() integer ext-real V50() Element of (n)
(n) |^ z is V6() V10() V11() V12() integer V36() V41() ext-real non negative set
x mod ((n) |^ z) is V6() V10() V11() V12() integer V36() V41() ext-real non negative V50() V61() V62() V63() V64() V65() V66() Element of NAT
z -' 1 is V6() V10() V11() V12() integer V36() V41() ext-real non negative V50() V61() V62() V63() V64() V65() V66() Element of NAT
(n) |^ (z -' 1) is V6() V10() V11() V12() integer V36() V41() ext-real non negative V50() V61() V62() V63() V64() V65() V66() Element of NAT
(x mod ((n) |^ z)) div ((n) |^ (z -' 1)) is V6() V10() V11() V12() integer V36() V41() ext-real non negative V50() V61() V62() V63() V64() V65() V66() Element of NAT
y . z is V11() V12() ext-real set
y is V15() V18( NAT ) V19((n)) Function-like V36() V43(k) FinSequence-like FinSubsequence-like V51() V52() V53() FinSequence of (n)
y is V15() V18( NAT ) V19((n)) Function-like V36() V43(k) FinSequence-like FinSubsequence-like V51() V52() V53() FinSequence of (n)
len y is V6() V10() V11() V12() integer V36() V41() ext-real non negative V50() V61() V62() V63() V64() V65() V66() Element of NAT
dom y is V43(k) V61() V62() V63() V64() V65() V66() Element of K6(NAT)
z is V6() V10() V11() V12() integer V36() V41() ext-real non negative set
y . z is V11() V12() ext-real set
(z,n,k,y) is V11() V12() integer ext-real set
(z,n,x) is V11() V12() integer ext-real V50() Element of (n)
(n) |^ z is V6() V10() V11() V12() integer V36() V41() ext-real non negative set
x mod ((n) |^ z) is V6() V10() V11() V12() integer V36() V41() ext-real non negative V50() V61() V62() V63() V64() V65() V66() Element of NAT
z -' 1 is V6() V10() V11() V12() integer V36() V41() ext-real non negative V50() V61() V62() V63() V64() V65() V66() Element of NAT
(n) |^ (z -' 1) is V6() V10() V11() V12() integer V36() V41() ext-real non negative V50() V61() V62() V63() V64() V65() V66() Element of NAT
(x mod ((n) |^ z)) div ((n) |^ (z -' 1)) is V6() V10() V11() V12() integer V36() V41() ext-real non negative V50() V61() V62() V63() V64() V65() V66() Element of NAT
(z,n,k,y) is V11() V12() integer ext-real set
y . z is V11() V12() ext-real set
len y is V6() V10() V11() V12() integer V36() V41() ext-real non negative V50() V61() V62() V63() V64() V65() V66() Element of NAT
n is V11() V12() integer ext-real set
- 2 is V11() V12() integer ext-real non positive set
- 1 is V11() V12() integer ext-real non positive set
k is V11() V12() integer ext-real set
(0) is V11() V12() integer ext-real set
n is V11() V12() integer ext-real set
(n) is V11() V12() integer ext-real set
n is V11() V12() integer ext-real set
(n) is V11() V12() integer ext-real set
k is V6() V10() V11() V12() integer V36() V41() ext-real non negative set
(k) is V6() V10() V11() V12() integer V36() V41() ext-real non negative V50() V61() V62() V63() V64() V65() V66() Element of NAT
2 to_power k is V11() V12() ext-real set
2 |^ k is V6() V10() V11() V12() integer V36() V41() ext-real non negative set
(n) * (k) is V11() V12() integer ext-real set
n - ((n) * (k)) is V11() V12() integer ext-real set
n is V6() V10() V11() V12() integer V36() V41() ext-real non negative set
(0,n) is V11() V12() integer ext-real set
(n) is V6() V10() V11() V12() integer V36() V41() ext-real non negative V50() V61() V62() V63() V64() V65() V66() Element of NAT
2 to_power n is V11() V12() ext-real set
2 |^ n is V6() V10() V11() V12() integer V36() V41() ext-real non negative set
(0) * (n) is V11() V12() integer ext-real set
0 - ((0) * (n)) is V11() V12() integer ext-real set
n is V11() V12() integer ext-real set
k is V11() V12() integer ext-real set
n + k is V11() V12() integer ext-real set
x is V6() V10() V11() V12() integer V36() V41() ext-real non negative set
(x) is non empty V61() V62() V63() V64() V65() Element of K6(INT)
(x) is V6() V10() V11() V12() integer V36() V41() ext-real non negative V50() V61() V62() V63() V64() V65() V66() Element of NAT
2 to_power x is V11() V12() ext-real set
2 |^ x is V6() V10() V11() V12() integer V36() V41() ext-real non negative set
(x) - 1 is V11() V12() integer ext-real set
- (x) is V11() V12() integer ext-real non positive set
(- (x)) + 1 is V11() V12() integer ext-real set
{ b₁ where b₁ is V11() V12() integer ext-real V50() Element of INT : ( b₁ <= (x) - 1 & (- (x)) + 1 <= b₁ ) } is set
(- (x)) + 2 is V11() V12() integer ext-real set
((n + k),x) is V11() V12() integer ext-real set
((n + k)) is V11() V12() integer ext-real set
((n + k)) * (x) is V11() V12() integer ext-real set
(n + k) - (((n + k)) * (x)) is V11() V12() integer ext-real set
(x) - 2 is V11() V12() integer ext-real set
((x) - 1) + ((x) - 1) is V11() V12() integer ext-real set
1 + (- (x)) is V11() V12() integer ext-real set
((- (x)) + 1) + (1 + (- (x))) is V11() V12() integer ext-real set
1 + 1 is non empty V6() V10() V11() V12() integer V36() V41() ext-real positive non negative set
(- (x)) + (1 + 1) is V11() V12() integer ext-real set
((- (x)) + (1 + 1)) - (x) is V11() V12() integer ext-real set
(- 2) + (x) is V11() V12() integer ext-real set
(n + k) + (x) is V11() V12() integer ext-real set
- (2 + 2) is V11() V12() integer ext-real non positive set
(- 2) + (- 2) is V11() V12() integer ext-real non positive set
(- (x)) - (- 2) is V11() V12() integer ext-real set
((x) - 1) - 1 is V11() V12() integer ext-real set
(((x) - 1) - 1) + (x) is V11() V12() integer ext-real set
(n + k) - (x) is V11() V12() integer ext-real set
2 - (x) is V11() V12() integer ext-real set
n is V6() V10() V11() V12() integer V36() V41() ext-real non negative set
k is V6() V10() V11() V12() integer V36() V41() ext-real non negative set
(k,1,n) is non empty V2() V15() V18( NAT ) V19((k)) Function-like one-to-one V36() V43(1) FinSequence-like FinSubsequence-like V51() V52() V53() V55() V56() V57() V58() FinSequence of (k)
(k) is non empty V61() V62() V63() V64() V65() Element of K6(INT)
(k) is V6() V10() V11() V12() integer V36() V41() ext-real non negative V50() V61() V62() V63() V64() V65() V66() Element of NAT
2 to_power k is V11() V12() ext-real set
2 |^ k is V6() V10() V11() V12() integer V36() V41() ext-real non negative set
(k) - 1 is V11() V12() integer ext-real set
- (k) is V11() V12() integer ext-real non positive set
(- (k)) + 1 is V11() V12() integer ext-real set
{ b₁ where b₁ is V11() V12() integer ext-real V50() Element of INT : ( b₁ <= (k) - 1 & (- (k)) + 1 <= b₁ ) } is set
(1,k,1,(k,1,n)) is V11() V12() integer ext-real set
(k) |^ 1 is V6() V10() V11() V12() integer V36() V41() ext-real non negative V50() V61() V62() V63() V64() V65() V66() Element of NAT
Seg 1 is non empty V2() V36() V43(1) V61() V62() V63() V64() V65() V66() Element of K6(NAT)
(1,k,n) is V11() V12() integer ext-real V50() Element of (k)
(k) |^ 1 is V6() V10() V11() V12() integer V36() V41() ext-real non negative set
n mod ((k) |^ 1) is V6() V10() V11() V12() integer V36() V41() ext-real non negative V50() V61() V62() V63() V64() V65() V66() Element of NAT
1 -' 1 is V6() V10() V11() V12() integer V36() V41() ext-real non negative V50() V61() V62() V63() V64() V65() V66() Element of NAT
(k) |^ (1 -' 1) is V6() V10() V11() V12() integer V36() V41() ext-real non negative V50() V61() V62() V63() V64() V65() V66() Element of NAT
(n mod ((k) |^ 1)) div ((k) |^ (1 -' 1)) is V6() V10() V11() V12() integer V36() V41() ext-real non negative V50() V61() V62() V63() V64() V65() V66() Element of NAT
n mod ((k) |^ 1) is V6() V10() V11() V12() integer V36() V41() ext-real non negative V50() V61() V62() V63() V64() V65() V66() Element of NAT
(k) |^ 0 is V6() V10() V11() V12() integer V36() V41() ext-real non negative V50() V61() V62() V63() V64() V65() V66() Element of NAT
(n mod ((k) |^ 1)) div ((k) |^ 0) is V6() V10() V11() V12() integer V36() V41() ext-real non negative V50() V61() V62() V63() V64() V65() V66() Element of NAT
(n mod ((k) |^ 1)) div 1 is V6() V10() V11() V12() integer V36() V41() ext-real non negative V50() V61() V62() V63() V64() V65() V66() Element of NAT
n is V6() V10() V11() V12() integer V36() V41() ext-real non negative set
k is V6() V10() V11() V12() integer V36() V41() ext-real non negative set
x is V6() V10() V11() V12() integer V36() V41() ext-real non negative set
x + 1 is non empty V6() V10() V11() V12() integer V36() V41() ext-real positive non negative set
y is V6() V10() V11() V12() integer V36() V41() ext-real non negative set
(n,(x + 1),y) is V15() V18( NAT ) V19((n)) Function-like V36() V43(x + 1) FinSequence-like FinSubsequence-like V51() V52() V53() FinSequence of (n)
(n) is non empty V61() V62() V63() V64() V65() Element of K6(INT)
(n) is V6() V10() V11() V12() integer V36() V41() ext-real non negative V50() V61() V62() V63() V64() V65() V66() Element of NAT
2 to_power n is V11() V12() ext-real set
2 |^ n is V6() V10() V11() V12() integer V36() V41() ext-real non negative set
(n) - 1 is V11() V12() integer ext-real set
- (n) is V11() V12() integer ext-real non positive set
(- (n)) + 1 is V11() V12() integer ext-real set
{ b₁ where b₁ is V11() V12() integer ext-real V50() Element of INT : ( b₁ <= (n) - 1 & (- (n)) + 1 <= b₁ ) } is set
((x + 1),n,(n,(x + 1),y)) is V11() V12() integer ext-real set
((x + 1),n,(n,(x + 1),y)) is V15() V18( NAT ) V19( INT ) Function-like V36() V43(x + 1) FinSequence-like FinSubsequence-like V51() V52() V53() FinSequence of INT
Sum ((x + 1),n,(n,(x + 1),y)) is V11() V12() integer ext-real V50() Element of INT
(n) |^ x is V6() V10() V11() V12() integer V36() V41() ext-real non negative set
y mod ((n) |^ x) is V6() V10() V11() V12() integer V36() V41() ext-real non negative V50() V61() V62() V63() V64() V65() V66() Element of NAT
y div ((n) |^ x) is V6() V10() V11() V12() integer V36() V41() ext-real non negative V50() V61() V62() V63() V64() V65() V66() Element of NAT
((n) |^ x) * (y div ((n) |^ x)) is V6() V10() V11() V12() integer V36() V41() ext-real non negative set
(x + 1) -' 1 is V6() V10() V11() V12() integer V36() V41() ext-real non negative V50() V61() V62() V63() V64() V65() V66() Element of NAT
len ((x + 1),n,(n,(x + 1),y)) is V6() V10() V11() V12() integer V36() V41() ext-real non negative V50() V61() V62() V63() V64() V65() V66() Element of NAT
Seg (x + 1) is non empty V36() V43(x + 1) V61() V62() V63() V64() V65() V66() Element of K6(NAT)
(n) |^ (x + 1) is V6() V10() V11() V12() integer V36() V41() ext-real non negative set
((x + 1),n,y) is V11() V12() integer ext-real V50() Element of (n)
y mod ((n) |^ (x + 1)) is V6() V10() V11() V12() integer V36() V41() ext-real non negative V50() V61() V62() V63() V64() V65() V66() Element of NAT
(n) |^ ((x + 1) -' 1) is V6() V10() V11() V12() integer V36() V41() ext-real non negative V50() V61() V62() V63() V64() V65() V66() Element of NAT
(y mod ((n) |^ (x + 1))) div ((n) |^ ((x + 1) -' 1)) is V6() V10() V11() V12() integer V36() V41() ext-real non negative V50() V61() V62() V63() V64() V65() V66() Element of NAT
((x + 1),n,(x + 1),(n,(x + 1),y)) is V11() V12() integer ext-real V50() Element of INT
((x + 1),n,(x + 1),(n,(x + 1),y)) is V11() V12() integer ext-real V50() Element of INT
((x + 1),n,(x + 1),(n,(x + 1),y)) is V11() V12() integer ext-real set
((n) |^ ((x + 1) -' 1)) * ((x + 1),n,(x + 1),(n,(x + 1),y)) is V11() V12() integer ext-real set
((x + 1),n,(n,(x + 1),y)) /. (x + 1) is V11() V12() integer ext-real V50() Element of INT
((x + 1),n,(n,(x + 1),y)) . (x + 1) is V11() V12() integer ext-real set
(n,x,(y mod ((n) |^ x))) is V15() V18( NAT ) V19((n)) Function-like V36() V43(x) FinSequence-like FinSubsequence-like V51() V52() V53() FinSequence of (n)
(x,n,(n,x,(y mod ((n) |^ x)))) is V15() V18( NAT ) V19( INT ) Function-like V36() V43(x) FinSequence-like FinSubsequence-like V51() V52() V53() FinSequence of INT
<*(((n) |^ x) * (y div ((n) |^ x)))*> is non empty V2() V15() V18( NAT ) Function-like V36() V43(1) FinSequence-like FinSubsequence-like set
(x,n,(n,x,(y mod ((n) |^ x)))) ^ <*(((n) |^ x) * (y div ((n) |^ x)))*> is non empty V15() V18( NAT ) Function-like V36() V43(K213(x,1)) FinSequence-like FinSubsequence-like set
K213(x,1) is non empty V6() V10() V11() V12() integer V36() V41() ext-real positive non negative V50() V61() V62() V63() V64() V65() V66() Element of NAT
zn is V15() V18( NAT ) V19( INT ) Function-like V36() FinSequence-like FinSubsequence-like V51() V52() V53() FinSequence of INT
(x,n,(n,x,(y mod ((n) |^ x)))) ^ zn is V15() V18( NAT ) V19( INT ) Function-like V36() FinSequence-like FinSubsequence-like V51() V52() V53() FinSequence of INT
z is V15() V18( NAT ) V19( INT ) Function-like V36() FinSequence-like FinSubsequence-like V51() V52() V53() FinSequence of INT
len z is V6() V10() V11() V12() integer V36() V41() ext-real non negative V50() V61() V62() V63() V64() V65() V66() Element of NAT
len (x,n,(n,x,(y mod ((n) |^ x)))) is V6() V10() V11() V12() integer V36() V41() ext-real non negative V50() V61() V62() V63() V64() V65() V66() Element of NAT
len <*(((n) |^ x) * (y div ((n) |^ x)))*> is non empty V6() V10() V11() V12() integer V36() V41() ext-real positive non negative V50() V61() V62() V63() V64() V65() V66() Element of NAT
(len (x,n,(n,x,(y mod ((n) |^ x))))) + (len <*(((n) |^ x) * (y div ((n) |^ x)))*>) is non empty V6() V10() V11() V12() integer V36() V41() ext-real positive non negative set
x + (len <*(((n) |^ x) * (y div ((n) |^ x)))*>) is non empty V6() V10() V11() V12() integer V36() V41() ext-real positive non negative set
y1 is V15() V18( NAT ) V19( INT ) Function-like V36() FinSequence-like FinSubsequence-like V51() V52() V53() FinSequence of INT
i is V6() V10() V11() V12() integer V36() V41() ext-real non negative set
z /. i is V11() V12() integer ext-real V50() Element of INT
y1 /. i is V11() V12() integer ext-real V50() Element of INT
Seg x is V36() V43(x) V61() V62() V63() V64() V65() V66() Element of K6(NAT)
(n) |^ i is V6() V10() V11() V12() integer V36() V41() ext-real non negative set
(y mod ((n) |^ x)) mod ((n) |^ i) is V6() V10() V11() V12() integer V36() V41() ext-real non negative V50() V61() V62() V63() V64() V65() V66() Element of NAT
y mod ((n) |^ i) is V6() V10() V11() V12() integer V36() V41() ext-real non negative V50() V61() V62() V63() V64() V65() V66() Element of NAT
t is V6() V10() V11() V12() integer V36() V41() ext-real non negative set
((n) |^ i) * t is V6() V10() V11() V12() integer V36() V41() ext-real non negative set
dom ((x,n,(n,x,(y mod ((n) |^ x)))) ^ zn) is V61() V62() V63() V64() V65() V66() Element of K6(NAT)
len y1 is V6() V10() V11() V12() integer V36() V41() ext-real non negative V50() V61() V62() V63() V64() V65() V66() Element of NAT
dom y1 is V61() V62() V63() V64() V65() V66() Element of K6(NAT)
y1 . i is V11() V12() integer ext-real set
((x + 1),n,(n,(x + 1),y)) /. i is V11() V12() integer ext-real V50() Element of INT
(i,n,(x + 1),(n,(x + 1),y)) is V11() V12() integer ext-real V50() Element of INT
i -' 1 is V6() V10() V11() V12() integer V36() V41() ext-real non negative V50() V61() V62() V63() V64() V65() V66() Element of NAT
(n) |^ (i -' 1) is V6() V10() V11() V12() integer V36() V41() ext-real non negative V50() V61() V62() V63() V64() V65() V66() Element of NAT
(i,n,(x + 1),(n,(x + 1),y)) is V11() V12() integer ext-real V50() Element of INT
(i,n,(x + 1),(n,(x + 1),y)) is V11() V12() integer ext-real set
((n) |^ (i -' 1)) * (i,n,(x + 1),(n,(x + 1),y)) is V11() V12() integer ext-real set
(i,n,y) is V11() V12() integer ext-real V50() Element of (n)
(y mod ((n) |^ i)) div ((n) |^ (i -' 1)) is V6() V10() V11() V12() integer V36() V41() ext-real non negative V50() V61() V62() V63() V64() V65() V66() Element of NAT
((n) |^ (i -' 1)) * (i,n,y) is V11() V12() integer ext-real set
((n) |^ (i -' 1)) * ((y mod ((n) |^ i)) div ((n) |^ (i -' 1))) is V6() V10() V11() V12() integer V36() V41() ext-real non negative set
dom (x,n,(n,x,(y mod ((n) |^ x)))) is V43(x) V61() V62() V63() V64() V65() V66() Element of K6(NAT)
((x,n,(n,x,(y mod ((n) |^ x)))) ^ zn) . i is V11() V12() integer ext-real set
(x,n,(n,x,(y mod ((n) |^ x)))) . i is V11() V12() integer ext-real set
(x,n,(n,x,(y mod ((n) |^ x)))) /. i is V11() V12() integer ext-real V50() Element of INT
(i,n,x,(n,x,(y mod ((n) |^ x)))) is V11() V12() integer ext-real V50() Element of INT
(i,n,x,(n,x,(y mod ((n) |^ x)))) is V11() V12() integer ext-real V50() Element of INT
(i,n,x,(n,x,(y mod ((n) |^ x)))) is V11() V12() integer ext-real set
((n) |^ (i -' 1)) * (i,n,x,(n,x,(y mod ((n) |^ x)))) is V11() V12() integer ext-real set
(i,n,(y mod ((n) |^ x))) is V11() V12() integer ext-real V50() Element of (n)
((y mod ((n) |^ x)) mod ((n) |^ i)) div ((n) |^ (i -' 1)) is V6() V10() V11() V12() integer V36() V41() ext-real non negative V50() V61() V62() V63() V64() V65() V66() Element of NAT
((n) |^ (i -' 1)) * (i,n,(y mod ((n) |^ x))) is V11() V12() integer ext-real set
z . (x + 1) is V11() V12() integer ext-real set
(len (x,n,(n,x,(y mod ((n) |^ x))))) + 1 is non empty V6() V10() V11() V12() integer V36() V41() ext-real positive non negative set
((x,n,(n,x,(y mod ((n) |^ x)))) ^ zn) . ((len (x,n,(n,x,(y mod ((n) |^ x))))) + 1) is V11() V12() integer ext-real set
Seg x is V36() V43(x) V61() V62() V63() V64() V65() V66() Element of K6(NAT)
len y1 is V6() V10() V11() V12() integer V36() V41() ext-real non negative V50() V61() V62() V63() V64() V65() V66() Element of NAT
(((n) |^ x) * (y div ((n) |^ x))) + (y mod ((n) |^ x)) is V6() V10() V11() V12() integer V36() V41() ext-real non negative set
(x,n,(n,x,(y mod ((n) |^ x)))) is V11() V12() integer ext-real set
Sum (x,n,(n,x,(y mod ((n) |^ x)))) is V11() V12() integer ext-real V50() Element of INT
(x,n,(n,x,(y mod ((n) |^ x)))) + (((n) |^ x) * (y div ((n) |^ x))) is V11() V12() integer ext-real set
y is V6() V10() V11() V12() integer V36() V41() ext-real non negative set
(n,(x + 1),y) is V15() V18( NAT ) V19((n)) Function-like V36() V43(x + 1) FinSequence-like FinSubsequence-like V51() V52() V53() FinSequence of (n)
(n) is non empty V61() V62() V63() V64() V65() Element of K6(INT)
(n) is V6() V10() V11() V12() integer V36() V41() ext-real non negative V50() V61() V62() V63() V64() V65() V66() Element of NAT
2 to_power n is V11() V12() ext-real set
2 |^ n is V6() V10() V11() V12() integer V36() V41() ext-real non negative set
(n) - 1 is V11() V12() integer ext-real set
- (n) is V11() V12() integer ext-real non positive set
(- (n)) + 1 is V11() V12() integer ext-real set
{ b₁ where b₁ is V11() V12() integer ext-real V50() Element of INT : ( b₁ <= (n) - 1 & (- (n)) + 1 <= b₁ ) } is set
((x + 1),n,(n,(x + 1),y)) is V11() V12() integer ext-real set
((x + 1),n,(n,(x + 1),y)) is V15() V18( NAT ) V19( INT ) Function-like V36() V43(x + 1) FinSequence-like FinSubsequence-like V51() V52() V53() FinSequence of INT
Sum ((x + 1),n,(n,(x + 1),y)) is V11() V12() integer ext-real V50() Element of INT
x is V6() V10() V11() V12() integer V36() V41() ext-real non negative set
(n,1,x) is non empty V2() V15() V18( NAT ) V19((n)) Function-like one-to-one V36() V43(1) FinSequence-like FinSubsequence-like V51() V52() V53() V55() V56() V57() V58() FinSequence of (n)
(n) is non empty V61() V62() V63() V64() V65() Element of K6(INT)
(n) is V6() V10() V11() V12() integer V36() V41() ext-real non negative V50() V61() V62() V63() V64() V65() V66() Element of NAT
2 to_power n is V11() V12() ext-real set
2 |^ n is V6() V10() V11() V12() integer V36() V41() ext-real non negative set
(n) - 1 is V11() V12() integer ext-real set
- (n) is V11() V12() integer ext-real non positive set
(- (n)) + 1 is V11() V12() integer ext-real set
{ b₁ where b₁ is V11() V12() integer ext-real V50() Element of INT : ( b₁ <= (n) - 1 & (- (n)) + 1 <= b₁ ) } is set
(1,n,(n,1,x)) is V11() V12() integer ext-real set
(1,n,(n,1,x)) is non empty V2() V15() V18( NAT ) V19( INT ) Function-like one-to-one V36() V43(1) FinSequence-like FinSubsequence-like V51() V52() V53() V55() V56() V57() V58() FinSequence of INT
Sum (1,n,(n,1,x)) is V11() V12() integer ext-real V50() Element of INT
y is V11() V12() ext-real Element of REAL
<*y*> is non empty V2() V15() V18( NAT ) V19( REAL ) Function-like one-to-one V36() V43(1) FinSequence-like FinSubsequence-like V51() V52() V53() V55() V56() V57() V58() FinSequence of REAL
Seg 1 is non empty V2() V36() V43(1) V61() V62() V63() V64() V65() V66() Element of K6(NAT)
(1,n,1,(n,1,x)) is V11() V12() integer ext-real V50() Element of INT
1 -' 1 is V6() V10() V11() V12() integer V36() V41() ext-real non negative V50() V61() V62() V63() V64() V65() V66() Element of NAT
(n) |^ (1 -' 1) is V6() V10() V11() V12() integer V36() V41() ext-real non negative V50() V61() V62() V63() V64() V65() V66() Element of NAT
(1,n,1,(n,1,x)) is V11() V12() integer ext-real V50() Element of INT
(1,n,1,(n,1,x)) is V11() V12() integer ext-real set
((n) |^ (1 -' 1)) * (1,n,1,(n,1,x)) is V11() V12() integer ext-real set
(n) |^ 0 is V6() V10() V11() V12() integer V36() V41() ext-real non negative V50() V61() V62() V63() V64() V65() V66() Element of NAT
((n) |^ 0) * (1,n,1,(n,1,x)) is V11() V12() integer ext-real set
1 * (1,n,1,(n,1,x)) is V11() V12() integer ext-real set
(1,n,(n,1,x)) /. 1 is V11() V12() integer ext-real V50() Element of INT
y is V15() V18( NAT ) V19( REAL ) Function-like V36() FinSequence-like FinSubsequence-like V51() V52() V53() FinSequence of REAL
Sum y is V11() V12() ext-real Element of REAL
K386() is V15() V18(K7(REAL,REAL)) V19( REAL ) Function-like V29(K7(REAL,REAL), REAL ) V51() V52() V53() Element of K6(K7(K7(REAL,REAL),REAL))
K184(REAL,y,K386()) is V11() V12() ext-real Element of REAL
x is V6() V10() V11() V12() integer V36() V41() ext-real non negative set
(n,k,x) is V15() V18( NAT ) V19((n)) Function-like V36() V43(k) FinSequence-like FinSubsequence-like V51() V52() V53() FinSequence of (n)
(n) is non empty V61() V62() V63() V64() V65() Element of K6(INT)
(n) is V6() V10() V11() V12() integer V36() V41() ext-real non negative V50() V61() V62() V63() V64() V65() V66() Element of NAT
2 to_power n is V11() V12() ext-real set
2 |^ n is V6() V10() V11() V12() integer V36() V41() ext-real non negative set
(n) - 1 is V11() V12() integer ext-real set
- (n) is V11() V12() integer ext-real non positive set
(- (n)) + 1 is V11() V12() integer ext-real set
{ b₁ where b₁ is V11() V12() integer ext-real V50() Element of INT : ( b₁ <= (n) - 1 & (- (n)) + 1 <= b₁ ) } is set
(k,n,(n,k,x)) is V11() V12() integer ext-real set
(k,n,(n,k,x)) is V15() V18( NAT ) V19( INT ) Function-like V36() V43(k) FinSequence-like FinSubsequence-like V51() V52() V53() FinSequence of INT
Sum (k,n,(n,k,x)) is V11() V12() integer ext-real V50() Element of INT
n is V6() V10() V11() V12() integer V36() V41() ext-real non negative set
k is V6() V10() V11() V12() integer V36() V41() ext-real non negative set
(k,1,n) is non empty V2() V15() V18( NAT ) V19((k)) Function-like one-to-one V36() V43(1) FinSequence-like FinSubsequence-like V51() V52() V53() V55() V56() V57() V58() FinSequence of (k)
(k) is non empty V61() V62() V63() V64() V65() Element of K6(INT)
(k) is V6() V10() V11() V12() integer V36() V41() ext-real non negative V50() V61() V62() V63() V64() V65() V66() Element of NAT
2 to_power k is V11() V12() ext-real set
2 |^ k is V6() V10() V11() V12() integer V36() V41() ext-real non negative set
(k) - 1 is V11() V12() integer ext-real set
- (k) is V11() V12() integer ext-real non positive set
(- (k)) + 1 is V11() V12() integer ext-real set
{ b₁ where b₁ is V11() V12() integer ext-real V50() Element of INT : ( b₁ <= (k) - 1 & (- (k)) + 1 <= b₁ ) } is set
(1,k,1,(k,1,n)) is V11() V12() integer ext-real set
x is V6() V10() V11() V12() integer V36() V41() ext-real non negative set
(k,1,x) is non empty V2() V15() V18( NAT ) V19((k)) Function-like one-to-one V36() V43(1) FinSequence-like FinSubsequence-like V51() V52() V53() V55() V56() V57() V58() FinSequence of (k)
(1,k,1,(k,1,x)) is V11() V12() integer ext-real set
(1,k,1,(k,1,n)) + (1,k,1,(k,1,x)) is V11() V12() integer ext-real set
(((1,k,1,(k,1,n)) + (1,k,1,(k,1,x)))) is V11() V12() integer ext-real set
n + x is V6() V10() V11() V12() integer V36() V41() ext-real non negative set
((n + x)) is V11() V12() integer ext-real set
n + (1,k,1,(k,1,x)) is V11() V12() integer ext-real set
((n + (1,k,1,(k,1,x)))) is V11() V12() integer ext-real set
n is V6() V10() V11() V12() integer V36() V41() ext-real non negative set
Seg n is V36() V43(n) V61() V62() V63() V64() V65() V66() Element of K6(NAT)
n + 1 is non empty V6() V10() V11() V12() integer V36() V41() ext-real positive non negative set
k is V6() V10() V11() V12() integer V36() V41() ext-real non negative set
x is V6() V10() V11() V12() integer V36() V41() ext-real non negative set
(x,(n + 1),k) is V15() V18( NAT ) V19((x)) Function-like V36() V43(n + 1) FinSequence-like FinSubsequence-like V51() V52() V53() FinSequence of (x)
(x) is non empty V61() V62() V63() V64() V65() Element of K6(INT)
(x) is V6() V10() V11() V12() integer V36() V41() ext-real non negative V50() V61() V62() V63() V64() V65() V66() Element of NAT
2 to_power x is V11() V12() ext-real set
2 |^ x is V6() V10() V11() V12() integer V36() V41() ext-real non negative set
(x) - 1 is V11() V12() integer ext-real set
- (x) is V11() V12() integer ext-real non positive set
(- (x)) + 1 is V11() V12() integer ext-real set
{ b₁ where b₁ is V11() V12() integer ext-real V50() Element of INT : ( b₁ <= (x) - 1 & (- (x)) + 1 <= b₁ ) } is set
(x) |^ n is V6() V10() V11() V12() integer V36() V41() ext-real non negative set
k mod ((x) |^ n) is V6() V10() V11() V12() integer V36() V41() ext-real non negative V50() V61() V62() V63() V64() V65() V66() Element of NAT
(x,n,(k mod ((x) |^ n))) is V15() V18( NAT ) V19((x)) Function-like V36() V43(n) FinSequence-like FinSubsequence-like V51() V52() V53() FinSequence of (x)
y is V6() V10() V11() V12() integer V36() V41() ext-real non negative set
(y,x,(n + 1),(x,(n + 1),k)) is V11() V12() integer ext-real set
(y,x,n,(x,n,(k mod ((x) |^ n)))) is V11() V12() integer ext-real set
Seg (n + 1) is non empty V36() V43(n + 1) V61() V62() V63() V64() V65() V66() Element of K6(NAT)
(x) |^ y is V6() V10() V11() V12() integer V36() V41() ext-real non negative set
y is V6() V10() V11() V12() integer V36() V41() ext-real non negative set
((x) |^ y) * y is V6() V10() V11() V12() integer V36() V41() ext-real non negative set
(y,x,(k mod ((x) |^ n))) is V11() V12() integer ext-real V50() Element of (x)
(k mod ((x) |^ n)) mod ((x) |^ y) is V6() V10() V11() V12() integer V36() V41() ext-real non negative V50() V61() V62() V63() V64() V65() V66() Element of NAT
y -' 1 is V6() V10() V11() V12() integer V36() V41() ext-real non negative V50() V61() V62() V63() V64() V65() V66() Element of NAT
(x) |^ (y -' 1) is V6() V10() V11() V12() integer V36() V41() ext-real non negative V50() V61() V62() V63() V64() V65() V66() Element of NAT
((k mod ((x) |^ n)) mod ((x) |^ y)) div ((x) |^ (y -' 1)) is V6() V10() V11() V12() integer V36() V41() ext-real non negative V50() V61() V62() V63() V64() V65() V66() Element of NAT
(y,x,k) is V11() V12() integer ext-real V50() Element of (x)
k mod ((x) |^ y) is V6() V10() V11() V12() integer V36() V41() ext-real non negative V50() V61() V62() V63() V64() V65() V66() Element of NAT
(k mod ((x) |^ y)) div ((x) |^ (y -' 1)) is V6() V10() V11() V12() integer V36() V41() ext-real non negative V50() V61() V62() V63() V64() V65() V66() Element of NAT
n is V6() V10() V11() V12() integer V36() V41() ext-real non negative set
k is V6() V10() V11() V12() integer V36() V41() ext-real non negative set
k + 1 is non empty V6() V10() V11() V12() integer V36() V41() ext-real positive non negative set
x is V6() V10() V11() V12() integer V36() V41() ext-real non negative set
(x,(k + 1),n) is V15() V18( NAT ) V19((x)) Function-like V36() V43(k + 1) FinSequence-like FinSubsequence-like V51() V52() V53() FinSequence of (x)
(x) is non empty V61() V62() V63() V64() V65() Element of K6(INT)
(x) is V6() V10() V11() V12() integer V36() V41() ext-real non negative V50() V61() V62() V63() V64() V65() V66() Element of NAT
2 to_power x is V11() V12() ext-real set
2 |^ x is V6() V10() V11() V12() integer V36() V41() ext-real non negative set
(x) - 1 is V11() V12() integer ext-real set
- (x) is V11() V12() integer ext-real non positive set
(- (x)) + 1 is V11() V12() integer ext-real set
{ b₁ where b₁ is V11() V12() integer ext-real V50() Element of INT : ( b₁ <= (x) - 1 & (- (x)) + 1 <= b₁ ) } is set
((k + 1),x,(k + 1),(x,(k + 1),n)) is V11() V12() integer ext-real set
(x) |^ k is V6() V10() V11() V12() integer V36() V41() ext-real non negative set
n div ((x) |^ k) is V6() V10() V11() V12() integer V36() V41() ext-real non negative V50() V61() V62() V63() V64() V65() V66() Element of NAT
(x) |^ (k + 1) is V6() V10() V11() V12() integer V36() V41() ext-real non negative set
Seg (k + 1) is non empty V36() V43(k + 1) V61() V62() V63() V64() V65() V66() Element of K6(NAT)
((k + 1),x,n) is V11() V12() integer ext-real V50() Element of (x)
n mod ((x) |^ (k + 1)) is V6() V10() V11() V12() integer V36() V41() ext-real non negative V50() V61() V62() V63() V64() V65() V66() Element of NAT
(k + 1) -' 1 is V6() V10() V11() V12() integer V36() V41() ext-real non negative V50() V61() V62() V63() V64() V65() V66() Element of NAT
(x) |^ ((k + 1) -' 1) is V6() V10() V11() V12() integer V36() V41() ext-real non negative V50() V61() V62() V63() V64() V65() V66() Element of NAT
(n mod ((x) |^ (k + 1))) div ((x) |^ ((k + 1) -' 1)) is V6() V10() V11() V12() integer V36() V41() ext-real non negative V50() V61() V62() V63() V64() V65() V66() Element of NAT
n div ((x) |^ ((k + 1) -' 1)) is V6() V10() V11() V12() integer V36() V41() ext-real non negative V50() V61() V62() V63() V64() V65() V66() Element of NAT
x is V6() V10() V11() V12() integer V36() V41() ext-real non negative set
n is V6() V10() V11() V12() integer V36() V41() ext-real non negative set
(n) is non empty V61() V62() V63() V64() V65() Element of K6(INT)
(n) is V6() V10() V11() V12() integer V36() V41() ext-real non negative V50() V61() V62() V63() V64() V65() V66() Element of NAT
2 to_power n is V11() V12() ext-real set
2 |^ n is V6() V10() V11() V12() integer V36() V41() ext-real non negative set
(n) - 1 is V11() V12() integer ext-real set
- (n) is V11() V12() integer ext-real non positive set
(- (n)) + 1 is V11() V12() integer ext-real set
{ b₁ where b₁ is V11() V12() integer ext-real V50() Element of INT : ( b₁ <= (n) - 1 & (- (n)) + 1 <= b₁ ) } is set
k is V6() V10() V11() V12() integer V36() V41() ext-real non negative set
Seg x is V36() V43(x) V61() V62() V63() V64() V65() V66() Element of K6(NAT)
y is V15() V18( NAT ) V19((n)) Function-like V36() V43(x) FinSequence-like FinSubsequence-like V51() V52() V53() FinSequence of (n)
(k,n,x,y) is V11() V12() integer ext-real set
y is V15() V18( NAT ) V19((n)) Function-like V36() V43(x) FinSequence-like FinSubsequence-like V51() V52() V53() FinSequence of (n)
(k,n,x,y) is V11() V12() integer ext-real set
(k,n,x,y) + (k,n,x,y) is V11() V12() integer ext-real set
(((k,n,x,y) + (k,n,x,y)),n) is V11() V12() integer ext-real set
(((k,n,x,y) + (k,n,x,y))) is V11() V12() integer ext-real set
(((k,n,x,y) + (k,n,x,y))) * (n) is V11() V12() integer ext-real set
((k,n,x,y) + (k,n,x,y)) - ((((k,n,x,y) + (k,n,x,y))) * (n)) is V11() V12() integer ext-real set
k -' 1 is V6() V10() V11() V12() integer V36() V41() ext-real non negative V50() V61() V62() V63() V64() V65() V66() Element of NAT
((k -' 1),n,x,y) is V11() V12() integer ext-real set
((k -' 1),n,x,y) is V11() V12() integer ext-real set
((k -' 1),n,x,y) + ((k -' 1),n,x,y) is V11() V12() integer ext-real set
((((k -' 1),n,x,y) + ((k -' 1),n,x,y))) is V11() V12() integer ext-real set
(((k,n,x,y) + (k,n,x,y)),n) + ((((k -' 1),n,x,y) + ((k -' 1),n,x,y))) is V11() V12() integer ext-real set
(n) - 2 is V11() V12() integer ext-real set
((n) - 2) + 1 is V11() V12() integer ext-real set
(- (n)) + 2 is V11() V12() integer ext-real set
((- (n)) + 2) + (- 1) is V11() V12() integer ext-real set
n is V6() V10() V11() V12() integer V36() V41() ext-real non negative set
k is V6() V10() V11() V12() integer V36() V41() ext-real non negative set
(k) is non empty V61() V62() V63() V64() V65() Element of K6(INT)
(k) is V6() V10() V11() V12() integer V36() V41() ext-real non negative V50() V61() V62() V63() V64() V65() V66() Element of NAT
2 to_power k is V11() V12() ext-real set
2 |^ k is V6() V10() V11() V12() integer V36() V41() ext-real non negative set
(k) - 1 is V11() V12() integer ext-real set
- (k) is V11() V12() integer ext-real non positive set
(- (k)) + 1 is V11() V12() integer ext-real set
{ b₁ where b₁ is V11() V12() integer ext-real V50() Element of INT : ( b₁ <= (k) - 1 & (- (k)) + 1 <= b₁ ) } is set
Seg n is V36() V43(n) V61() V62() V63() V64() V65() V66() Element of K6(NAT)
x is V15() V18( NAT ) V19((k)) Function-like V36() V43(n) FinSequence-like FinSubsequence-like V51() V52() V53() FinSequence of (k)
y is V15() V18( NAT ) V19((k)) Function-like V36() V43(n) FinSequence-like FinSubsequence-like V51() V52() V53() FinSequence of (k)
y is V15() V18( NAT ) V19((k)) Function-like V36() FinSequence-like FinSubsequence-like V51() V52() V53() FinSequence of (k)
len y is V6() V10() V11() V12() integer V36() V41() ext-real non negative V50() V61() V62() V63() V64() V65() V66() Element of NAT
dom y is V61() V62() V63() V64() V65() V66() Element of K6(NAT)
z is V15() V18( NAT ) V19((k)) Function-like V36() V43(n) FinSequence-like FinSubsequence-like V51() V52() V53() FinSequence of (k)
yn is V6() V10() V11() V12() integer V36() V41() ext-real non negative set
(yn,k,n,z) is V11() V12() integer ext-real set
(k,yn,n,x,y) is V11() V12() integer ext-real V50() Element of (k)
z . yn is V11() V12() ext-real set
y is V15() V18( NAT ) V19((k)) Function-like V36() V43(n) FinSequence-like FinSubsequence-like V51() V52() V53() FinSequence of (k)
z is V15() V18( NAT ) V19((k)) Function-like V36() V43(n) FinSequence-like FinSubsequence-like V51() V52() V53() FinSequence of (k)
len y is V6() V10() V11() V12() integer V36() V41() ext-real non negative V50() V61() V62() V63() V64() V65() V66() Element of NAT
dom y is V43(n) V61() V62() V63() V64() V65() V66() Element of K6(NAT)
yn is V6() V10() V11() V12() integer V36() V41() ext-real non negative set
y . yn is V11() V12() ext-real set
(yn,k,n,y) is V11() V12() integer ext-real set
(k,yn,n,x,y) is V11() V12() integer ext-real V50() Element of (k)
(yn,k,n,z) is V11() V12() integer ext-real set
z . yn is V11() V12() ext-real set
len z is V6() V10() V11() V12() integer V36() V41() ext-real non negative V50() V61() V62() V63() V64() V65() V66() Element of NAT
n is V6() V10() V11() V12() integer V36() V41() ext-real non negative set
k is V6() V10() V11() V12() integer V36() V41() ext-real non negative set
(n,1,k) is non empty V2() V15() V18( NAT ) V19((n)) Function-like one-to-one V36() V43(1) FinSequence-like FinSubsequence-like V51() V52() V53() V55() V56() V57() V58() FinSequence of (n)
(n) is non empty V61() V62() V63() V64() V65() Element of K6(INT)
(n) is V6() V10() V11() V12() integer V36() V41() ext-real non negative V50() V61() V62() V63() V64() V65() V66() Element of NAT
2 to_power n is V11() V12() ext-real set
2 |^ n is V6() V10() V11() V12() integer V36() V41() ext-real non negative set
(n) - 1 is V11() V12() integer ext-real set
- (n) is V11() V12() integer ext-real non positive set
(- (n)) + 1 is V11() V12() integer ext-real set
{ b₁ where b₁ is V11() V12() integer ext-real V50() Element of INT : ( b₁ <= (n) - 1 & (- (n)) + 1 <= b₁ ) } is set
x is V6() V10() V11() V12() integer V36() V41() ext-real non negative set
(n,1,x) is non empty V2() V15() V18( NAT ) V19((n)) Function-like one-to-one V36() V43(1) FinSequence-like FinSubsequence-like V51() V52() V53() V55() V56() V57() V58() FinSequence of (n)
(1,n,(n,1,k),(n,1,x)) is non empty V2() V15() V18( NAT ) V19((n)) Function-like one-to-one V36() V43(1) FinSequence-like FinSubsequence-like V51() V52() V53() V55() V56() V57() V58() FinSequence of (n)
(1,n,(1,n,(n,1,k),(n,1,x))) is V11() V12() integer ext-real set
(1,n,(1,n,(n,1,k),(n,1,x))) is non empty V2() V15() V18( NAT ) V19( INT ) Function-like one-to-one V36() V43(1) FinSequence-like FinSubsequence-like V51() V52() V53() V55() V56() V57() V58() FinSequence of INT
Sum (1,n,(1,n,(n,1,k),(n,1,x))) is V11() V12() integer ext-real V50() Element of INT
k + x is V6() V10() V11() V12() integer V36() V41() ext-real non negative set
((k + x),n) 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) - (((k + x)) * (n)) is V11() V12() integer ext-real set
Seg 1 is non empty V2() V36() V43(1) V61() V62() V63() V64() V65() V66() Element of K6(NAT)
(1,n,1,(1,n,(n,1,k),(n,1,x))) is V11() V12() integer ext-real set
(n,1,1,(n,1,k),(n,1,x)) is V11() V12() integer ext-real V50() Element of (n)
(1,n,1,(n,1,k)) is V11() V12() integer ext-real set
(1,n,1,(n,1,x)) is V11() V12() integer ext-real set
(1,n,1,(n,1,k)) + (1,n,1,(n,1,x)) is V11() V12() integer ext-real set
(((1,n,1,(n,1,k)) + (1,n,1,(n,1,x))),n) is V11() V12() integer ext-real set
(((1,n,1,(n,1,k)) + (1,n,1,(n,1,x)))) is V11() V12() integer ext-real set
(((1,n,1,(n,1,k)) + (1,n,1,(n,1,x)))) * (n) is V11() V12() integer ext-real set
((1,n,1,(n,1,k)) + (1,n,1,(n,1,x))) - ((((1,n,1,(n,1,k)) + (1,n,1,(n,1,x)))) * (n)) is V11() V12() integer ext-real set
1 -' 1 is V6() V10() V11() V12() integer V36() V41() ext-real non negative V50() V61() V62() V63() V64() V65() V66() Element of NAT
((1 -' 1),n,1,(n,1,k)) is V11() V12() integer ext-real set
((1 -' 1),n,1,(n,1,x)) is V11() V12() integer ext-real set
((1 -' 1),n,1,(n,1,k)) + ((1 -' 1),n,1,(n,1,x)) is V11() V12() integer ext-real set
((((1 -' 1),n,1,(n,1,k)) + ((1 -' 1),n,1,(n,1,x)))) is V11() V12() integer ext-real set
(((1,n,1,(n,1,k)) + (1,n,1,(n,1,x))),n) + ((((1 -' 1),n,1,(n,1,k)) + ((1 -' 1),n,1,(n,1,x)))) is V11() V12() integer ext-real set
(0,n,1,(n,1,k)) is V11() V12() integer ext-real set
(0,n,1,(n,1,k)) + ((1 -' 1),n,1,(n,1,x)) is V11() V12() integer ext-real set
(((0,n,1,(n,1,k)) + ((1 -' 1),n,1,(n,1,x)))) is V11() V12() integer ext-real set
(((1,n,1,(n,1,k)) + (1,n,1,(n,1,x))),n) + (((0,n,1,(n,1,k)) + ((1 -' 1),n,1,(n,1,x)))) is V11() V12() integer ext-real set
(0,n,1,(n,1,x)) is V11() V12() integer ext-real set
(0,n,1,(n,1,k)) + (0,n,1,(n,1,x)) is V11() V12() integer ext-real set
(((0,n,1,(n,1,k)) + (0,n,1,(n,1,x)))) is V11() V12() integer ext-real set
(((1,n,1,(n,1,k)) + (1,n,1,(n,1,x))),n) + (((0,n,1,(n,1,k)) + (0,n,1,(n,1,x)))) is V11() V12() integer ext-real set
0 + (0,n,1,(n,1,x)) is V11() V12() integer ext-real set
((0 + (0,n,1,(n,1,x)))) is V11() V12() integer ext-real set
(((1,n,1,(n,1,k)) + (1,n,1,(n,1,x))),n) + ((0 + (0,n,1,(n,1,x)))) is V11() V12() integer ext-real set
(((1,n,1,(n,1,k)) + (1,n,1,(n,1,x))),n) + 0 is V11() V12() integer ext-real set
k + (1,n,1,(n,1,x)) is V11() V12() integer ext-real set
((k + (1,n,1,(n,1,x))),n) is V11() V12() integer ext-real set
((k + (1,n,1,(n,1,x)))) is V11() V12() integer ext-real set
((k + (1,n,1,(n,1,x)))) * (n) is V11() V12() integer ext-real set
(k + (1,n,1,(n,1,x))) - (((k + (1,n,1,(n,1,x)))) * (n)) is V11() V12() integer ext-real set
(1,n,(1,n,(n,1,k),(n,1,x))) /. 1 is V11() V12() integer ext-real V50() Element of INT
(1,n,1,(1,n,(n,1,k),(n,1,x))) is V11() V12() integer ext-real V50() Element of INT
(n) |^ (1 -' 1) is V6() V10() V11() V12() integer V36() V41() ext-real non negative V50() V61() V62() V63() V64() V65() V66() Element of NAT
(1,n,1,(1,n,(n,1,k),(n,1,x))) is V11() V12() integer ext-real V50() Element of INT
((n) |^ (1 -' 1)) * (1,n,1,(1,n,(n,1,k),(n,1,x))) is V11() V12() integer ext-real set
(n) |^ 0 is V6() V10() V11() V12() integer V36() V41() ext-real non negative V50() V61() V62() V63() V64() V65() V66() Element of NAT
((n) |^ 0) * (1,n,1,(1,n,(n,1,k),(n,1,x))) is V11() V12() integer ext-real set
1 * (1,n,1,(1,n,(n,1,k),(n,1,x))) is V11() V12() integer ext-real set
len (1,n,(1,n,(n,1,k),(n,1,x))) is non empty V6() V10() V11() V12() integer V36() V41() ext-real positive non negative V50() V61() V62() V63() V64() V65() V66() Element of NAT
dom (1,n,(1,n,(n,1,k),(n,1,x))) is non empty V2() V43(1) V61() V62() V63() V64() V65() V66() Element of K6(NAT)
(1,n,(1,n,(n,1,k),(n,1,x))) . 1 is V11() V12() integer ext-real set
z is V11() V12() integer ext-real V50() Element of INT
<*z*> is non empty V2() V15() V18( NAT ) V19( INT ) Function-like one-to-one V36() V43(1) FinSequence-like FinSubsequence-like V51() V52() V53() V55() V56() V57() V58() FinSequence of INT
Sum <*z*> is V11() V12() integer ext-real V50() Element of INT
n is V6() V10() V11() V12() integer V36() V41() ext-real non negative set
k is V6() V10() V11() V12() integer V36() V41() ext-real non negative set
k + 1 is non empty V6() V10() V11() V12() integer V36() V41() ext-real positive non negative set
Seg k is V36() V43(k) V61() V62() V63() V64() V65() V66() Element of K6(NAT)
x is V6() V10() V11() V12() integer V36() V41() ext-real non negative set
y is V6() V10() V11() V12() integer V36() V41() ext-real non negative set
y is V6() V10() V11() V12() integer V36() V41() ext-real non negative set
y + y is V6() V10() V11() V12() integer V36() V41() ext-real non negative set
(x,(k + 1),y) is V15() V18( NAT ) V19((x)) Function-like V36() V43(k + 1) FinSequence-like FinSubsequence-like V51() V52() V53() FinSequence of (x)
(x) is non empty V61() V62() V63() V64() V65() Element of K6(INT)
(x) is V6() V10() V11() V12() integer V36() V41() ext-real non negative V50() V61() V62() V63() V64() V65() V66() Element of NAT
2 to_power x is V11() V12() ext-real set
2 |^ x is V6() V10() V11() V12() integer V36() V41() ext-real non negative set
(x) - 1 is V11() V12() integer ext-real set
- (x) is V11() V12() integer ext-real non positive set
(- (x)) + 1 is V11() V12() integer ext-real set
{ b₁ where b₁ is V11() V12() integer ext-real V50() Element of INT : ( b₁ <= (x) - 1 & (- (x)) + 1 <= b₁ ) } is set
(x,(k + 1),y) is V15() V18( NAT ) V19((x)) Function-like V36() V43(k + 1) FinSequence-like FinSubsequence-like V51() V52() V53() FinSequence of (x)
((k + 1),x,(x,(k + 1),y),(x,(k + 1),y)) is V15() V18( NAT ) V19((x)) Function-like V36() V43(k + 1) FinSequence-like FinSubsequence-like V51() V52() V53() FinSequence of (x)
((k + 1),x,((k + 1),x,(x,(k + 1),y),(x,(k + 1),y))) is V11() V12() integer ext-real set
((k + 1),x,((k + 1),x,(x,(k + 1),y),(x,(k + 1),y))) is V15() V18( NAT ) V19( INT ) Function-like V36() V43(k + 1) FinSequence-like FinSubsequence-like V51() V52() V53() FinSequence of INT
Sum ((k + 1),x,((k + 1),x,(x,(k + 1),y),(x,(k + 1),y))) is V11() V12() integer ext-real V50() Element of INT
(x) |^ (k + 1) is V6() V10() V11() V12() integer V36() V41() ext-real non negative set
((k + 1),x,(k + 1),(x,(k + 1),y)) is V11() V12() integer ext-real set
((k + 1),x,(k + 1),(x,(k + 1),y)) is V11() V12() integer ext-real set
((k + 1),x,(k + 1),(x,(k + 1),y)) + ((k + 1),x,(k + 1),(x,(k + 1),y)) is V11() V12() integer ext-real set
((((k + 1),x,(k + 1),(x,(k + 1),y)) + ((k + 1),x,(k + 1),(x,(k + 1),y)))) is V11() V12() integer ext-real set
((x) |^ (k + 1)) * ((((k + 1),x,(k + 1),(x,(k + 1),y)) + ((k + 1),x,(k + 1),(x,(k + 1),y)))) is V11() V12() integer ext-real set
((k + 1),x,((k + 1),x,(x,(k + 1),y),(x,(k + 1),y))) + (((x) |^ (k + 1)) * ((((k + 1),x,(k + 1),(x,(k + 1),y)) + ((k + 1),x,(k + 1),(x,(k + 1),y))))) is V11() V12() integer ext-real set
Seg (k + 1) is non empty V36() V43(k + 1) V61() V62() V63() V64() V65() V66() Element of K6(NAT)
(x) |^ k is V6() V10() V11() V12() integer V36() V41() ext-real non negative set
y mod ((x) |^ k) is V6() V10() V11() V12() integer V36() V41() ext-real non negative V50() V61() V62() V63() V64() V65() V66() Element of NAT
y mod ((x) |^ k) is V6() V10() V11() V12() integer V36() V41() ext-real non negative V50() V61() V62() V63() V64() V65() V66() Element of NAT
(x,k,(y mod ((x) |^ k))) is V15() V18( NAT ) V19((x)) Function-like V36() V43(k) FinSequence-like FinSubsequence-like V51() V52() V53() FinSequence of (x)
(x,k,(y mod ((x) |^ k))) is V15() V18( NAT ) V19((x)) Function-like V36() V43(k) FinSequence-like FinSubsequence-like V51() V52() V53() FinSequence of (x)
(k,x,(x,k,(y mod ((x) |^ k))),(x,k,(y mod ((x) |^ k)))) is V15() V18( NAT ) V19((x)) Function-like V36() V43(k) FinSequence-like FinSubsequence-like V51() V52() V53() FinSequence of (x)
(k,x,(k,x,(x,k,(y mod ((x) |^ k))),(x,k,(y mod ((x) |^ k))))) is V15() V18( NAT ) V19( INT ) Function-like V36() V43(k) FinSequence-like FinSubsequence-like V51() V52() V53() FinSequence of INT
len (k,x,(k,x,(x,k,(y mod ((x) |^ k))),(x,k,(y mod ((x) |^ k))))) is V6() V10() V11() V12() integer V36() V41() ext-real non negative V50() V61() V62() V63() V64() V65() V66() Element of NAT
len ((k + 1),x,((k + 1),x,(x,(k + 1),y),(x,(k + 1),y))) is V6() V10() V11() V12() integer V36() V41() ext-real non negative V50() V61() V62() V63() V64() V65() V66() Element of NAT
((k + 1),x,(k + 1),((k + 1),x,(x,(k + 1),y),(x,(k + 1),y))) is V11() V12() integer ext-real V50() Element of INT
(k + 1) -' 1 is V6() V10() V11() V12() integer V36() V41() ext-real non negative V50() V61() V62() V63() V64() V65() V66() Element of NAT
(x) |^ ((k + 1) -' 1) is V6() V10() V11() V12() integer V36() V41() ext-real non negative V50() V61() V62() V63() V64() V65() V66() Element of NAT
((k + 1),x,(k + 1),((k + 1),x,(x,(k + 1),y),(x,(k + 1),y))) is V11() V12() integer ext-real V50() Element of INT
((k + 1),x,(k + 1),((k + 1),x,(x,(k + 1),y),(x,(k + 1),y))) is V11() V12() integer ext-real set
((x) |^ ((k + 1) -' 1)) * ((k + 1),x,(k + 1),((k + 1),x,(x,(k + 1),y),(x,(k + 1),y))) is V11() V12() integer ext-real set
<*((k + 1),x,(k + 1),((k + 1),x,(x,(k + 1),y),(x,(k + 1),y)))*> is non empty V2() V15() V18( NAT ) V19( INT ) Function-like one-to-one V36() V43(1) FinSequence-like FinSubsequence-like V51() V52() V53() V55() V56() V57() V58() FinSequence of INT
(k,x,(k,x,(x,k,(y mod ((x) |^ k))),(x,k,(y mod ((x) |^ k))))) ^ <*((k + 1),x,(k + 1),((k + 1),x,(x,(k + 1),y),(x,(k + 1),y)))*> is non empty V15() V18( NAT ) V19( INT ) Function-like V36() V43(K213(k,1)) FinSequence-like FinSubsequence-like V51() V52() V53() FinSequence of INT
K213(k,1) is non empty V6() V10() V11() V12() integer V36() V41() ext-real positive non negative V50() V61() V62() V63() V64() V65() V66() Element of NAT
y1 is V6() V10() V11() V12() integer V36() V41() ext-real non negative set
((k + 1),x,((k + 1),x,(x,(k + 1),y),(x,(k + 1),y))) . y1 is V11() V12() integer ext-real set
((k,x,(k,x,(x,k,(y mod ((x) |^ k))),(x,k,(y mod ((x) |^ k))))) ^ <*((k + 1),x,(k + 1),((k + 1),x,(x,(k + 1),y),(x,(k + 1),y)))*>) . y1 is V11() V12() integer ext-real set
y1 -' 1 is V6() V10() V11() V12() integer V36() V41() ext-real non negative V50() V61() V62() V63() V64() V65() V66() Element of NAT
y1 - 1 is V11() V12() integer ext-real set
dom ((k + 1),x,((k + 1),x,(x,(k + 1),y),(x,(k + 1),y))) is V43(k + 1) V61() V62() V63() V64() V65() V66() Element of K6(NAT)
dom (k,x,(k,x,(x,k,(y mod ((x) |^ k))),(x,k,(y mod ((x) |^ k))))) is V43(k) V61() V62() V63() V64() V65() V66() Element of K6(NAT)
(k,x,(k,x,(x,k,(y mod ((x) |^ k))),(x,k,(y mod ((x) |^ k))))) . y1 is V11() V12() integer ext-real set
(k,x,(k,x,(x,k,(y mod ((x) |^ k))),(x,k,(y mod ((x) |^ k))))) /. y1 is V11() V12() integer ext-real V50() Element of INT
(y1,x,k,(k,x,(x,k,(y mod ((x) |^ k))),(x,k,(y mod ((x) |^ k))))) is V11() V12() integer ext-real V50() Element of INT
(x) |^ (y1 -' 1) is V6() V10() V11() V12() integer V36() V41() ext-real non negative V50() V61() V62() V63() V64() V65() V66() Element of NAT
(y1,x,k,(k,x,(x,k,(y mod ((x) |^ k))),(x,k,(y mod ((x) |^ k))))) is V11() V12() integer ext-real V50() Element of INT
(y1,x,k,(k,x,(x,k,(y mod ((x) |^ k))),(x,k,(y mod ((x) |^ k))))) is V11() V12() integer ext-real set
((x) |^ (y1 -' 1)) * (y1,x,k,(k,x,(x,k,(y mod ((x) |^ k))),(x,k,(y mod ((x) |^ k))))) is V11() V12() integer ext-real set
(x,y1,k,(x,k,(y mod ((x) |^ k))),(x,k,(y mod ((x) |^ k)))) is V11() V12() integer ext-real V50() Element of (x)
((x) |^ (y1 -' 1)) * (x,y1,k,(x,k,(y mod ((x) |^ k))),(x,k,(y mod ((x) |^ k)))) is V11() V12() integer ext-real set
(y1,x,k,(x,k,(y mod ((x) |^ k)))) is V11() V12() integer ext-real set
(y1,x,k,(x,k,(y mod ((x) |^ k)))) is V11() V12() integer ext-real set
(y1,x,k,(x,k,(y mod ((x) |^ k)))) + (y1,x,k,(x,k,(y mod ((x) |^ k)))) is V11() V12() integer ext-real set
(((y1,x,k,(x,k,(y mod ((x) |^ k)))) + (y1,x,k,(x,k,(y mod ((x) |^ k))))),x) is V11() V12() integer ext-real set
(((y1,x,k,(x,k,(y mod ((x) |^ k)))) + (y1,x,k,(x,k,(y mod ((x) |^ k)))))) is V11() V12() integer ext-real set
(((y1,x,k,(x,k,(y mod ((x) |^ k)))) + (y1,x,k,(x,k,(y mod ((x) |^ k)))))) * (x) is V11() V12() integer ext-real set
((y1,x,k,(x,k,(y mod ((x) |^ k)))) + (y1,x,k,(x,k,(y mod ((x) |^ k))))) - ((((y1,x,k,(x,k,(y mod ((x) |^ k)))) + (y1,x,k,(x,k,(y mod ((x) |^ k)))))) * (x)) is V11() V12() integer ext-real set
((y1 -' 1),x,k,(x,k,(y mod ((x) |^ k)))) is V11() V12() integer ext-real set
((y1 -' 1),x,k,(x,k,(y mod ((x) |^ k)))) is V11() V12() integer ext-real set
((y1 -' 1),x,k,(x,k,(y mod ((x) |^ k)))) + ((y1 -' 1),x,k,(x,k,(y mod ((x) |^ k)))) is V11() V12() integer ext-real set
((((y1 -' 1),x,k,(x,k,(y mod ((x) |^ k)))) + ((y1 -' 1),x,k,(x,k,(y mod ((x) |^ k)))))) is V11() V12() integer ext-real set
(((y1,x,k,(x,k,(y mod ((x) |^ k)))) + (y1,x,k,(x,k,(y mod ((x) |^ k))))),x) + ((((y1 -' 1),x,k,(x,k,(y mod ((x) |^ k)))) + ((y1 -' 1),x,k,(x,k,(y mod ((x) |^ k)))))) is V11() V12() integer ext-real set
((x) |^ (y1 -' 1)) * ((((y1,x,k,(x,k,(y mod ((x) |^ k)))) + (y1,x,k,(x,k,(y mod ((x) |^ k))))),x) + ((((y1 -' 1),x,k,(x,k,(y mod ((x) |^ k)))) + ((y1 -' 1),x,k,(x,k,(y mod ((x) |^ k))))))) is V11() V12() integer ext-real set
((k + 1),x,((k + 1),x,(x,(k + 1),y),(x,(k + 1),y))) /. y1 is V11() V12() integer ext-real V50() Element of INT
(y1,x,(k + 1),((k + 1),x,(x,(k + 1),y),(x,(k + 1),y))) is V11() V12() integer ext-real V50() Element of INT
(y1,x,(k + 1),((k + 1),x,(x,(k + 1),y),(x,(k + 1),y))) is V11() V12() integer ext-real V50() Element of INT
(y1,x,(k + 1),((k + 1),x,(x,(k + 1),y),(x,(k + 1),y))) is V11() V12() integer ext-real set
((x) |^ (y1 -' 1)) * (y1,x,(k + 1),((k + 1),x,(x,(k + 1),y),(x,(k + 1),y))) is V11() V12() integer ext-real set
(x,y1,(k + 1),(x,(k + 1),y),(x,(k + 1),y)) is V11() V12() integer ext-real V50() Element of (x)
((x) |^ (y1 -' 1)) * (x,y1,(k + 1),(x,(k + 1),y),(x,(k + 1),y)) is V11() V12() integer ext-real set
(y1,x,(k + 1),(x,(k + 1),y)) is V11() V12() integer ext-real set
(y1,x,(k + 1),(x,(k + 1),y)) is V11() V12() integer ext-real set
(y1,x,(k + 1),(x,(k + 1),y)) + (y1,x,(k + 1),(x,(k + 1),y)) is V11() V12() integer ext-real set
(((y1,x,(k + 1),(x,(k + 1),y)) + (y1,x,(k + 1),(x,(k + 1),y))),x) is V11() V12() integer ext-real set
(((y1,x,(k + 1),(x,(k + 1),y)) + (y1,x,(k + 1),(x,(k + 1),y)))) is V11() V12() integer ext-real set
(((y1,x,(k + 1),(x,(k + 1),y)) + (y1,x,(k + 1),(x,(k + 1),y)))) * (x) is V11() V12() integer ext-real set
((y1,x,(k + 1),(x,(k + 1),y)) + (y1,x,(k + 1),(x,(k + 1),y))) - ((((y1,x,(k + 1),(x,(k + 1),y)) + (y1,x,(k + 1),(x,(k + 1),y)))) * (x)) is V11() V12() integer ext-real set
((y1 -' 1),x,(k + 1),(x,(k + 1),y)) is V11() V12() integer ext-real set
((y1 -' 1),x,(k + 1),(x,(k + 1),y)) is V11() V12() integer ext-real set
((y1 -' 1),x,(k + 1),(x,(k + 1),y)) + ((y1 -' 1),x,(k + 1),(x,(k + 1),y)) is V11() V12() integer ext-real set
((((y1 -' 1),x,(k + 1),(x,(k + 1),y)) + ((y1 -' 1),x,(k + 1),(x,(k + 1),y)))) is V11() V12() integer ext-real set
(((y1,x,(k + 1),(x,(k + 1),y)) + (y1,x,(k + 1),(x,(k + 1),y))),x) + ((((y1 -' 1),x,(k + 1),(x,(k + 1),y)) + ((y1 -' 1),x,(k + 1),(x,(k + 1),y)))) is V11() V12() integer ext-real set
((x) |^ (y1 -' 1)) * ((((y1,x,(k + 1),(x,(k + 1),y)) + (y1,x,(k + 1),(x,(k + 1),y))),x) + ((((y1 -' 1),x,(k + 1),(x,(k + 1),y)) + ((y1 -' 1),x,(k + 1),(x,(k + 1),y))))) is V11() V12() integer ext-real set
(0,x,k,(x,k,(y mod ((x) |^ k)))) is V11() V12() integer ext-real set
((y1 -' 1),x,k,(x,k,(y mod ((x) |^ k)))) + (0,x,k,(x,k,(y mod ((x) |^ k)))) is V11() V12() integer ext-real set
((((y1 -' 1),x,k,(x,k,(y mod ((x) |^ k)))) + (0,x,k,(x,k,(y mod ((x) |^ k)))))) is V11() V12() integer ext-real set
(((y1,x,k,(x,k,(y mod ((x) |^ k)))) + (y1,x,k,(x,k,(y mod ((x) |^ k))))),x) + ((((y1 -' 1),x,k,(x,k,(y mod ((x) |^ k)))) + (0,x,k,(x,k,(y mod ((x) |^ k)))))) is V11() V12() integer ext-real set
((x) |^ (y1 -' 1)) * ((((y1,x,k,(x,k,(y mod ((x) |^ k)))) + (y1,x,k,(x,k,(y mod ((x) |^ k))))),x) + ((((y1 -' 1),x,k,(x,k,(y mod ((x) |^ k)))) + (0,x,k,(x,k,(y mod ((x) |^ k))))))) is V11() V12() integer ext-real set
(0,x,k,(x,k,(y mod ((x) |^ k)))) is V11() V12() integer ext-real set
(0,x,k,(x,k,(y mod ((x) |^ k)))) + (0,x,k,(x,k,(y mod ((x) |^ k)))) is V11() V12() integer ext-real set
(((0,x,k,(x,k,(y mod ((x) |^ k)))) + (0,x,k,(x,k,(y mod ((x) |^ k)))))) is V11() V12() integer ext-real set
(((y1,x,k,(x,k,(y mod ((x) |^ k)))) + (y1,x,k,(x,k,(y mod ((x) |^ k))))),x) + (((0,x,k,(x,k,(y mod ((x) |^ k)))) + (0,x,k,(x,k,(y mod ((x) |^ k)))))) is V11() V12() integer ext-real set
((x) |^ (y1 -' 1)) * ((((y1,x,k,(x,k,(y mod ((x) |^ k)))) + (y1,x,k,(x,k,(y mod ((x) |^ k))))),x) + (((0,x,k,(x,k,(y mod ((x) |^ k)))) + (0,x,k,(x,k,(y mod ((x) |^ k))))))) is V11() V12() integer ext-real set
(0,x,k,(x,k,(y mod ((x) |^ k)))) + 0 is V11() V12() integer ext-real set
(((0,x,k,(x,k,(y mod ((x) |^ k)))) + 0)) is V11() V12() integer ext-real set
(((y1,x,k,(x,k,(y mod ((x) |^ k)))) + (y1,x,k,(x,k,(y mod ((x) |^ k))))),x) + (((0,x,k,(x,k,(y mod ((x) |^ k)))) + 0)) is V11() V12() integer ext-real set
((x) |^ (y1 -' 1)) * ((((y1,x,k,(x,k,(y mod ((x) |^ k)))) + (y1,x,k,(x,k,(y mod ((x) |^ k))))),x) + (((0,x,k,(x,k,(y mod ((x) |^ k)))) + 0))) is V11() V12() integer ext-real set
(((y1,x,k,(x,k,(y mod ((x) |^ k)))) + (y1,x,k,(x,k,(y mod ((x) |^ k))))),x) + 0 is V11() V12() integer ext-real set
((x) |^ (y1 -' 1)) * ((((y1,x,k,(x,k,(y mod ((x) |^ k)))) + (y1,x,k,(x,k,(y mod ((x) |^ k))))),x) + 0) is V11() V12() integer ext-real set
(0,x,(k + 1),(x,(k + 1),y)) is V11() V12() integer ext-real set
((y1 -' 1),x,(k + 1),(x,(k + 1),y)) + (0,x,(k + 1),(x,(k + 1),y)) is V11() V12() integer ext-real set
((((y1 -' 1),x,(k + 1),(x,(k + 1),y)) + (0,x,(k + 1),(x,(k + 1),y)))) is V11() V12() integer ext-real set
(((y1,x,(k + 1),(x,(k + 1),y)) + (y1,x,(k + 1),(x,(k + 1),y))),x) + ((((y1 -' 1),x,(k + 1),(x,(k + 1),y)) + (0,x,(k + 1),(x,(k + 1),y)))) is V11() V12() integer ext-real set
((x) |^ (y1 -' 1)) * ((((y1,x,(k + 1),(x,(k + 1),y)) + (y1,x,(k + 1),(x,(k + 1),y))),x) + ((((y1 -' 1),x,(k + 1),(x,(k + 1),y)) + (0,x,(k + 1),(x,(k + 1),y))))) is V11() V12() integer ext-real set
(0,x,(k + 1),(x,(k + 1),y)) is V11() V12() integer ext-real set
(0,x,(k + 1),(x,(k + 1),y)) + (0,x,(k + 1),(x,(k + 1),y)) is V11() V12() integer ext-real set
(((0,x,(k + 1),(x,(k + 1),y)) + (0,x,(k + 1),(x,(k + 1),y)))) is V11() V12() integer ext-real set
(((y1,x,(k + 1),(x,(k + 1),y)) + (y1,x,(k + 1),(x,(k + 1),y))),x) + (((0,x,(k + 1),(x,(k + 1),y)) + (0,x,(k + 1),(x,(k + 1),y)))) is V11() V12() integer ext-real set
((x) |^ (y1 -' 1)) * ((((y1,x,(k + 1),(x,(k + 1),y)) + (y1,x,(k + 1),(x,(k + 1),y))),x) + (((0,x,(k + 1),(x,(k + 1),y)) + (0,x,(k + 1),(x,(k + 1),y))))) is V11() V12() integer ext-real set
(0,x,(k + 1),(x,(k + 1),y)) + 0 is V11() V12() integer ext-real set
(((0,x,(k + 1),(x,(k + 1),y)) + 0)) is V11() V12() integer ext-real set
(((y1,x,(k + 1),(x,(k + 1),y)) + (y1,x,(k + 1),(x,(k + 1),y))),x) + (((0,x,(k + 1),(x,(k + 1),y)) + 0)) is V11() V12() integer ext-real set
((x) |^ (y1 -' 1)) * ((((y1,x,(k + 1),(x,(k + 1),y)) + (y1,x,(k + 1),(x,(k + 1),y))),x) + (((0,x,(k + 1),(x,(k + 1),y)) + 0))) is V11() V12() integer ext-real set
(((y1,x,(k + 1),(x,(k + 1),y)) + (y1,x,(k + 1),(x,(k + 1),y))),x) + 0 is V11() V12() integer ext-real set
((x) |^ (y1 -' 1)) * ((((y1,x,(k + 1),(x,(k + 1),y)) + (y1,x,(k + 1),(x,(k + 1),y))),x) + 0) is V11() V12() integer ext-real set
(y1,x,k,(x,k,(y mod ((x) |^ k)))) + (y1,x,(k + 1),(x,(k + 1),y)) is V11() V12() integer ext-real set
(((y1,x,k,(x,k,(y mod ((x) |^ k)))) + (y1,x,(k + 1),(x,(k + 1),y))),x) is V11() V12() integer ext-real set
(((y1,x,k,(x,k,(y mod ((x) |^ k)))) + (y1,x,(k + 1),(x,(k + 1),y)))) is V11() V12() integer ext-real set
(((y1,x,k,(x,k,(y mod ((x) |^ k)))) + (y1,x,(k + 1),(x,(k + 1),y)))) * (x) is V11() V12() integer ext-real set
((y1,x,k,(x,k,(y mod ((x) |^ k)))) + (y1,x,(k + 1),(x,(k + 1),y))) - ((((y1,x,k,(x,k,(y mod ((x) |^ k)))) + (y1,x,(k + 1),(x,(k + 1),y)))) * (x)) is V11() V12() integer ext-real set
((x) |^ (y1 -' 1)) * (((y1,x,k,(x,k,(y mod ((x) |^ k)))) + (y1,x,(k + 1),(x,(k + 1),y))),x) is V11() V12() integer ext-real set
((x) |^ (y1 -' 1)) * (((y1,x,k,(x,k,(y mod ((x) |^ k)))) + (y1,x,k,(x,k,(y mod ((x) |^ k))))),x) is V11() V12() integer ext-real set
(y1,x,k,(x,k,(y mod ((x) |^ k)))) + (y1,x,(k + 1),(x,(k + 1),y)) is V11() V12() integer ext-real set
(((y1,x,k,(x,k,(y mod ((x) |^ k)))) + (y1,x,(k + 1),(x,(k + 1),y))),x) is V11() V12() integer ext-real set
(((y1,x,k,(x,k,(y mod ((x) |^ k)))) + (y1,x,(k + 1),(x,(k + 1),y)))) is V11() V12() integer ext-real set
(((y1,x,k,(x,k,(y mod ((x) |^ k)))) + (y1,x,(k + 1),(x,(k + 1),y)))) * (x) is V11() V12() integer ext-real set
((y1,x,k,(x,k,(y mod ((x) |^ k)))) + (y1,x,(k + 1),(x,(k + 1),y))) - ((((y1,x,k,(x,k,(y mod ((x) |^ k)))) + (y1,x,(k + 1),(x,(k + 1),y)))) * (x)) is V11() V12() integer ext-real set
(((y1,x,k,(x,k,(y mod ((x) |^ k)))) + (y1,x,(k + 1),(x,(k + 1),y))),x) + ((((y1 -' 1),x,(k + 1),(x,(k + 1),y)) + ((y1 -' 1),x,(k + 1),(x,(k + 1),y)))) is V11() V12() integer ext-real set
((x) |^ (y1 -' 1)) * ((((y1,x,k,(x,k,(y mod ((x) |^ k)))) + (y1,x,(k + 1),(x,(k + 1),y))),x) + ((((y1 -' 1),x,(k + 1),(x,(k + 1),y)) + ((y1 -' 1),x,(k + 1),(x,(k + 1),y))))) is V11() V12() integer ext-real set
(((y1,x,k,(x,k,(y mod ((x) |^ k)))) + (y1,x,k,(x,k,(y mod ((x) |^ k))))),x) + ((((y1 -' 1),x,(k + 1),(x,(k + 1),y)) + ((y1 -' 1),x,(k + 1),(x,(k + 1),y)))) is V11() V12() integer ext-real set
((x) |^ (y1 -' 1)) * ((((y1,x,k,(x,k,(y mod ((x) |^ k)))) + (y1,x,k,(x,k,(y mod ((x) |^ k))))),x) + ((((y1 -' 1),x,(k + 1),(x,(k + 1),y)) + ((y1 -' 1),x,(k + 1),(x,(k + 1),y))))) is V11() V12() integer ext-real set
((y1 -' 1),x,k,(x,k,(y mod ((x) |^ k)))) + ((y1 -' 1),x,(k + 1),(x,(k + 1),y)) is V11() V12() integer ext-real set
((((y1 -' 1),x,k,(x,k,(y mod ((x) |^ k)))) + ((y1 -' 1),x,(k + 1),(x,(k + 1),y)))) is V11() V12() integer ext-real set
(((y1,x,k,(x,k,(y mod ((x) |^ k)))) + (y1,x,k,(x,k,(y mod ((x) |^ k))))),x) + ((((y1 -' 1),x,k,(x,k,(y mod ((x) |^ k)))) + ((y1 -' 1),x,(k + 1),(x,(k + 1),y)))) is V11() V12() integer ext-real set
((x) |^ (y1 -' 1)) * ((((y1,x,k,(x,k,(y mod ((x) |^ k)))) + (y1,x,k,(x,k,(y mod ((x) |^ k))))),x) + ((((y1 -' 1),x,k,(x,k,(y mod ((x) |^ k)))) + ((y1 -' 1),x,(k + 1),(x,(k + 1),y))))) is V11() V12() integer ext-real set
(len (k,x,(k,x,(x,k,(y mod ((x) |^ k))),(x,k,(y mod ((x) |^ k)))))) + 1 is non empty V6() V10() V11() V12() integer V36() V41() ext-real positive non negative set
((k,x,(k,x,(x,k,(y mod ((x) |^ k))),(x,k,(y mod ((x) |^ k))))) ^ <*((k + 1),x,(k + 1),((k + 1),x,(x,(k + 1),y),(x,(k + 1),y)))*>) . ((len (k,x,(k,x,(x,k,(y mod ((x) |^ k))),(x,k,(y mod ((x) |^ k)))))) + 1) is V11() V12() integer ext-real set
((k + 1),x,((k + 1),x,(x,(k + 1),y),(x,(k + 1),y))) /. (k + 1) is V11() V12() integer ext-real V50() Element of INT
((k + 1),x,((k + 1),x,(x,(k + 1),y),(x,(k + 1),y))) . (k + 1) is V11() V12() integer ext-real set
((x) |^ k) * ((k + 1),x,(k + 1),((k + 1),x,(x,(k + 1),y),(x,(k + 1),y))) is V11() V12() integer ext-real set
y div ((x) |^ k) is V6() V10() V11() V12() integer V36() V41() ext-real non negative V50() V61() V62() V63() V64() V65() V66() Element of NAT
(y div ((x) |^ k)) * ((x) |^ k) is V6() V10() V11() V12() integer V36() V41() ext-real non negative set
((y div ((x) |^ k)) * ((x) |^ k)) + (y mod ((x) |^ k)) is V6() V10() V11() V12() integer V36() V41() ext-real non negative set
y div ((x) |^ k) is V6() V10() V11() V12() integer V36() V41() ext-real non negative V50() V61() V62() V63() V64() V65() V66() Element of NAT
len <*((k + 1),x,(k + 1),((k + 1),x,(x,(k + 1),y),(x,(k + 1),y)))*> is non empty V6() V10() V11() V12() integer V36() V41() ext-real positive non negative V50() V61() V62() V63() V64() V65() V66() Element of NAT
len ((k,x,(k,x,(x,k,(y mod ((x) |^ k))),(x,k,(y mod ((x) |^ k))))) ^ <*((k + 1),x,(k + 1),((k + 1),x,(x,(k + 1),y),(x,(k + 1),y)))*>) is non empty V6() V10() V11() V12() integer V36() V41() ext-real positive non negative V50() V61() V62() V63() V64() V65() V66() Element of NAT
(len (k,x,(k,x,(x,k,(y mod ((x) |^ k))),(x,k,(y mod ((x) |^ k)))))) + (len <*((k + 1),x,(k + 1),((k + 1),x,(x,(k + 1),y),(x,(k + 1),y)))*>) is non empty V6() V10() V11() V12() integer V36() V41() ext-real positive non negative set
Sum (k,x,(k,x,(x,k,(y mod ((x) |^ k))),(x,k,(y mod ((x) |^ k))))) is V11() V12() integer ext-real V50() Element of INT
(((x) |^ k) * ((k + 1),x,(k + 1),((k + 1),x,(x,(k + 1),y),(x,(k + 1),y)))) + (Sum (k,x,(k,x,(x,k,(y mod ((x) |^ k))),(x,k,(y mod ((x) |^ k)))))) is V11() V12() integer ext-real set
(x,(k + 1),(k + 1),(x,(k + 1),y),(x,(k + 1),y)) is V11() V12() integer ext-real V50() Element of (x)
(x,(k + 1),(k + 1),(x,(k + 1),y),(x,(k + 1),y)) * ((x) |^ k) is V11() V12() integer ext-real set
((x,(k + 1),(k + 1),(x,(k + 1),y),(x,(k + 1),y)) * ((x) |^ k)) + (Sum (k,x,(k,x,(x,k,(y mod ((x) |^ k))),(x,k,(y mod ((x) |^ k)))))) is V11() V12() integer ext-real set
((((k + 1),x,(k + 1),(x,(k + 1),y)) + ((k + 1),x,(k + 1),(x,(k + 1),y))),x) is V11() V12() integer ext-real set
((((k + 1),x,(k + 1),(x,(k + 1),y)) + ((k + 1),x,(k + 1),(x,(k + 1),y)))) * (x) is V11() V12() integer ext-real set
(((k + 1),x,(k + 1),(x,(k + 1),y)) + ((k + 1),x,(k + 1),(x,(k + 1),y))) - (((((k + 1),x,(k + 1),(x,(k + 1),y)) + ((k + 1),x,(k + 1),(x,(k + 1),y)))) * (x)) is V11() V12() integer ext-real set
(((k + 1) -' 1),x,(k + 1),(x,(k + 1),y)) is V11() V12() integer ext-real set
(((k + 1) -' 1),x,(k + 1),(x,(k + 1),y)) is V11() V12() integer ext-real set
(((k + 1) -' 1),x,(k + 1),(x,(k + 1),y)) + (((k + 1) -' 1),x,(k + 1),(x,(k + 1),y)) is V11() V12() integer ext-real set
(((((k + 1) -' 1),x,(k + 1),(x,(k + 1),y)) + (((k + 1) -' 1),x,(k + 1),(x,(k + 1),y)))) is V11() V12() integer ext-real set
((((k + 1),x,(k + 1),(x,(k + 1),y)) + ((k + 1),x,(k + 1),(x,(k + 1),y))),x) + (((((k + 1) -' 1),x,(k + 1),(x,(k + 1),y)) + (((k + 1) -' 1),x,(k + 1),(x,(k + 1),y)))) is V11() V12() integer ext-real set
(((((k + 1),x,(k + 1),(x,(k + 1),y)) + ((k + 1),x,(k + 1),(x,(k + 1),y))),x) + (((((k + 1) -' 1),x,(k + 1),(x,(k + 1),y)) + (((k + 1) -' 1),x,(k + 1),(x,(k + 1),y))))) * ((x) |^ k) is V11() V12() integer ext-real set
((((((k + 1),x,(k + 1),(x,(k + 1),y)) + ((k + 1),x,(k + 1),(x,(k + 1),y))),x) + (((((k + 1) -' 1),x,(k + 1),(x,(k + 1),y)) + (((k + 1) -' 1),x,(k + 1),(x,(k + 1),y))))) * ((x) |^ k)) + (Sum (k,x,(k,x,(x,k,(y mod ((x) |^ k))),(x,k,(y mod ((x) |^ k)))))) is V11() V12() integer ext-real set
(k,x,(k + 1),(x,(k + 1),y)) is V11() V12() integer ext-real set
(((k + 1) -' 1),x,(k + 1),(x,(k + 1),y)) + (k,x,(k + 1),(x,(k + 1),y)) is V11() V12() integer ext-real set
(((((k + 1) -' 1),x,(k + 1),(x,(k + 1),y)) + (k,x,(k + 1),(x,(k + 1),y)))) is V11() V12() integer ext-real set
((((k + 1),x,(k + 1),(x,(k + 1),y)) + ((k + 1),x,(k + 1),(x,(k + 1),y))),x) + (((((k + 1) -' 1),x,(k + 1),(x,(k + 1),y)) + (k,x,(k + 1),(x,(k + 1),y)))) is V11() V12() integer ext-real set
(((((k + 1),x,(k + 1),(x,(k + 1),y)) + ((k + 1),x,(k + 1),(x,(k + 1),y))),x) + (((((k + 1) -' 1),x,(k + 1),(x,(k + 1),y)) + (k,x,(k + 1),(x,(k + 1),y))))) * ((x) |^ k) is V11() V12() integer ext-real set
((((((k + 1),x,(k + 1),(x,(k + 1),y)) + ((k + 1),x,(k + 1),(x,(k + 1),y))),x) + (((((k + 1) -' 1),x,(k + 1),(x,(k + 1),y)) + (k,x,(k + 1),(x,(k + 1),y))))) * ((x) |^ k)) + (Sum (k,x,(k,x,(x,k,(y mod ((x) |^ k))),(x,k,(y mod ((x) |^ k)))))) is V11() V12() integer ext-real set
(k,x,(k + 1),(x,(k + 1),y)) is V11() V12() integer ext-real set
(k,x,(k + 1),(x,(k + 1),y)) + (k,x,(k + 1),(x,(k + 1),y)) is V11() V12() integer ext-real set
(((k,x,(k + 1),(x,(k + 1),y)) + (k,x,(k + 1),(x,(k + 1),y)))) is V11() V12() integer ext-real set
((((k + 1),x,(k + 1),(x,(k + 1),y)) + ((k + 1),x,(k + 1),(x,(k + 1),y))),x) + (((k,x,(k + 1),(x,(k + 1),y)) + (k,x,(k + 1),(x,(k + 1),y)))) is V11() V12() integer ext-real set
(((((k + 1),x,(k + 1),(x,(k + 1),y)) + ((k + 1),x,(k + 1),(x,(k + 1),y))),x) + (((k,x,(k + 1),(x,(k + 1),y)) + (k,x,(k + 1),(x,(k + 1),y))))) * ((x) |^ k) is V11() V12() integer ext-real set
((((((k + 1),x,(k + 1),(x,(k + 1),y)) + ((k + 1),x,(k + 1),(x,(k + 1),y))),x) + (((k,x,(k + 1),(x,(k + 1),y)) + (k,x,(k + 1),(x,(k + 1),y))))) * ((x) |^ k)) + (Sum (k,x,(k,x,(x,k,(y mod ((x) |^ k))),(x,k,(y mod ((x) |^ k)))))) is V11() V12() integer ext-real set
(k,x,k,(x,k,(y mod ((x) |^ k)))) is V11() V12() integer ext-real set
(k,x,k,(x,k,(y mod ((x) |^ k)))) + (k,x,(k + 1),(x,(k + 1),y)) is V11() V12() integer ext-real set
(((k,x,k,(x,k,(y mod ((x) |^ k)))) + (k,x,(k + 1),(x,(k + 1),y)))) is V11() V12() integer ext-real set
((((k + 1),x,(k + 1),(x,(k + 1),y)) + ((k + 1),x,(k + 1),(x,(k + 1),y))),x) + (((k,x,k,(x,k,(y mod ((x) |^ k)))) + (k,x,(k + 1),(x,(k + 1),y)))) is V11() V12() integer ext-real set
(((((k + 1),x,(k + 1),(x,(k + 1),y)) + ((k + 1),x,(k + 1),(x,(k + 1),y))),x) + (((k,x,k,(x,k,(y mod ((x) |^ k)))) + (k,x,(k + 1),(x,(k + 1),y))))) * ((x) |^ k) is V11() V12() integer ext-real set
((((((k + 1),x,(k + 1),(x,(k + 1),y)) + ((k + 1),x,(k + 1),(x,(k + 1),y))),x) + (((k,x,k,(x,k,(y mod ((x) |^ k)))) + (k,x,(k + 1),(x,(k + 1),y))))) * ((x) |^ k)) + (Sum (k,x,(k,x,(x,k,(y mod ((x) |^ k))),(x,k,(y mod ((x) |^ k)))))) is V11() V12() integer ext-real set
(k,x,k,(x,k,(y mod ((x) |^ k)))) is V11() V12() integer ext-real set
(k,x,k,(x,k,(y mod ((x) |^ k)))) + (k,x,k,(x,k,(y mod ((x) |^ k)))) is V11() V12() integer ext-real set
(((k,x,k,(x,k,(y mod ((x) |^ k)))) + (k,x,k,(x,k,(y mod ((x) |^ k)))))) is V11() V12() integer ext-real set
((((k + 1),x,(k + 1),(x,(k + 1),y)) + ((k + 1),x,(k + 1),(x,(k + 1),y))),x) + (((k,x,k,(x,k,(y mod ((x) |^ k)))) + (k,x,k,(x,k,(y mod ((x) |^ k)))))) is V11() V12() integer ext-real set
(((((k + 1),x,(k + 1),(x,(k + 1),y)) + ((k + 1),x,(k + 1),(x,(k + 1),y))),x) + (((k,x,k,(x,k,(y mod ((x) |^ k)))) + (k,x,k,(x,k,(y mod ((x) |^ k))))))) * ((x) |^ k) is V11() V12() integer ext-real set
((((((k + 1),x,(k + 1),(x,(k + 1),y)) + ((k + 1),x,(k + 1),(x,(k + 1),y))),x) + (((k,x,k,(x,k,(y mod ((x) |^ k)))) + (k,x,k,(x,k,(y mod ((x) |^ k))))))) * ((x) |^ k)) + (Sum (k,x,(k,x,(x,k,(y mod ((x) |^ k))),(x,k,(y mod ((x) |^ k)))))) is V11() V12() integer ext-real set
(y div ((x) |^ k)) + (y div ((x) |^ k)) is V6() V10() V11() V12() integer V36() V41() ext-real non negative set
(((y div ((x) |^ k)) + (y div ((x) |^ k))),x) is V11() V12() integer ext-real set
(((y div ((x) |^ k)) + (y div ((x) |^ k)))) is V11() V12() integer ext-real set
(((y div ((x) |^ k)) + (y div ((x) |^ k)))) * (x) is V11() V12() integer ext-real set
((y div ((x) |^ k)) + (y div ((x) |^ k))) - ((((y div ((x) |^ k)) + (y div ((x) |^ k)))) * (x)) is V11() V12() integer ext-real set
(((y div ((x) |^ k)) + (y div ((x) |^ k))),x) + (((k,x,k,(x,k,(y mod ((x) |^ k)))) + (k,x,k,(x,k,(y mod ((x) |^ k)))))) is V11() V12() integer ext-real set
((((y div ((x) |^ k)) + (y div ((x) |^ k))),x) + (((k,x,k,(x,k,(y mod ((x) |^ k)))) + (k,x,k,(x,k,(y mod ((x) |^ k))))))) * ((x) |^ k) is V11() V12() integer ext-real set
(((((y div ((x) |^ k)) + (y div ((x) |^ k))),x) + (((k,x,k,(x,k,(y mod ((x) |^ k)))) + (k,x,k,(x,k,(y mod ((x) |^ k))))))) * ((x) |^ k)) + (Sum (k,x,(k,x,(x,k,(y mod ((x) |^ k))),(x,k,(y mod ((x) |^ k)))))) is V11() V12() integer ext-real set
(((y div ((x) |^ k)) + (y div ((x) |^ k))),x) * ((x) |^ k) is V11() V12() integer ext-real set
(((k,x,k,(x,k,(y mod ((x) |^ k)))) + (k,x,k,(x,k,(y mod ((x) |^ k)))))) * ((x) |^ k) is V11() V12() integer ext-real set
(k,x,(k,x,(x,k,(y mod ((x) |^ k))),(x,k,(y mod ((x) |^ k))))) is V11() V12() integer ext-real set
((((k,x,k,(x,k,(y mod ((x) |^ k)))) + (k,x,k,(x,k,(y mod ((x) |^ k)))))) * ((x) |^ k)) + (k,x,(k,x,(x,k,(y mod ((x) |^ k))),(x,k,(y mod ((x) |^ k))))) is V11() V12() integer ext-real set
((((y div ((x) |^ k)) + (y div ((x) |^ k))),x) * ((x) |^ k)) + (((((k,x,k,(x,k,(y mod ((x) |^ k)))) + (k,x,k,(x,k,(y mod ((x) |^ k)))))) * ((x) |^ k)) + (k,x,(k,x,(x,k,(y mod ((x) |^ k))),(x,k,(y mod ((x) |^ k)))))) is V11() V12() integer ext-real set
(y mod ((x) |^ k)) + (y mod ((x) |^ k)) is V6() V10() V11() V12() integer V36() V41() ext-real non negative set
((((y div ((x) |^ k)) + (y div ((x) |^ k))),x) * ((x) |^ k)) + ((y mod ((x) |^ k)) + (y mod ((x) |^ k))) is V11() V12() integer ext-real set
((((y div ((x) |^ k)) + (y div ((x) |^ k))),x) * ((x) |^ k)) + (y mod ((x) |^ k)) is V11() V12() integer ext-real set
(((((y div ((x) |^ k)) + (y div ((x) |^ k))),x) * ((x) |^ k)) + (y mod ((x) |^ k))) + (y mod ((x) |^ k)) is V11() V12() integer ext-real set
(((y div ((x) |^ k)) + (y div ((x) |^ k)))) * ((x) |^ (k + 1)) is V11() V12() integer ext-real set
((k + 1),x,((k + 1),x,(x,(k + 1),y),(x,(k + 1),y))) + ((((y div ((x) |^ k)) + (y div ((x) |^ k)))) * ((x) |^ (k + 1))) is V11() V12() integer ext-real set
((((y div ((x) |^ k)) + (y div ((x) |^ k))),x) * ((x) |^ k)) + ((((y div ((x) |^ k)) + (y div ((x) |^ k)))) * ((x) |^ (k + 1))) is V11() V12() integer ext-real set
(((((y div ((x) |^ k)) + (y div ((x) |^ k))),x) * ((x) |^ k)) + ((((y div ((x) |^ k)) + (y div ((x) |^ k)))) * ((x) |^ (k + 1)))) + (y mod ((x) |^ k)) is V11() V12() integer ext-real set
((((((y div ((x) |^ k)) + (y div ((x) |^ k))),x) * ((x) |^ k)) + ((((y div ((x) |^ k)) + (y div ((x) |^ k)))) * ((x) |^ (k + 1)))) + (y mod ((x) |^ k))) + (y mod ((x) |^ k)) is V11() V12() integer ext-real set
((x) |^ k) * (x) is V6() V10() V11() V12() integer V36() V41() ext-real non negative set
(((y div ((x) |^ k)) + (y div ((x) |^ k)))) * (((x) |^ k) * (x)) is V11() V12() integer ext-real set
((((y div ((x) |^ k)) + (y div ((x) |^ k))),x) * ((x) |^ k)) + ((((y div ((x) |^ k)) + (y div ((x) |^ k)))) * (((x) |^ k) * (x))) is V11() V12() integer ext-real set
(((((y div ((x) |^ k)) + (y div ((x) |^ k))),x) * ((x) |^ k)) + ((((y div ((x) |^ k)) + (y div ((x) |^ k)))) * (((x) |^ k) * (x)))) + (y mod ((x) |^ k)) is V11() V12() integer ext-real set
((((((y div ((x) |^ k)) + (y div ((x) |^ k))),x) * ((x) |^ k)) + ((((y div ((x) |^ k)) + (y div ((x) |^ k)))) * (((x) |^ k) * (x)))) + (y mod ((x) |^ k))) + (y mod ((x) |^ k)) is V11() V12() integer ext-real set
(y div ((x) |^ k)) * ((x) |^ k) is V6() V10() V11() V12() integer V36() V41() ext-real non negative set
((y div ((x) |^ k)) * ((x) |^ k)) + (y mod ((x) |^ k)) is V6() V10() V11() V12() integer V36() V41() ext-real non negative set
(((y div ((x) |^ k)) * ((x) |^ k)) + (y mod ((x) |^ k))) + (((y div ((x) |^ k)) * ((x) |^ k)) + (y mod ((x) |^ k))) is V6() V10() V11() V12() integer V36() V41() ext-real non negative set
k is V6() V10() V11() V12() integer V36() V41() ext-real non negative set
x is V6() V10() V11() V12() integer V36() V41() ext-real non negative set
y is V6() V10() V11() V12() integer V36() V41() ext-real non negative set
x + y is V6() V10() V11() V12() integer V36() V41() ext-real non negative set
(k,1,x) is non empty V2() V15() V18( NAT ) V19((k)) Function-like one-to-one V36() V43(1) FinSequence-like FinSubsequence-like V51() V52() V53() V55() V56() V57() V58() FinSequence of (k)
(k) is non empty V61() V62() V63() V64() V65() Element of K6(INT)
(k) is V6() V10() V11() V12() integer V36() V41() ext-real non negative V50() V61() V62() V63() V64() V65() V66() Element of NAT
2 to_power k is V11() V12() ext-real set
2 |^ k is V6() V10() V11() V12() integer V36() V41() ext-real non negative set
(k) - 1 is V11() V12() integer ext-real set
- (k) is V11() V12() integer ext-real non positive set
(- (k)) + 1 is V11() V12() integer ext-real set
{ b₁ where b₁ is V11() V12() integer ext-real V50() Element of INT : ( b₁ <= (k) - 1 & (- (k)) + 1 <= b₁ ) } is set
(k,1,y) is non empty V2() V15() V18( NAT ) V19((k)) Function-like one-to-one V36() V43(1) FinSequence-like FinSubsequence-like V51() V52() V53() V55() V56() V57() V58() FinSequence of (k)
(1,k,(k,1,x),(k,1,y)) is non empty V2() V15() V18( NAT ) V19((k)) Function-like one-to-one V36() V43(1) FinSequence-like FinSubsequence-like V51() V52() V53() V55() V56() V57() V58() FinSequence of (k)
(1,k,(1,k,(k,1,x),(k,1,y))) is V11() V12() integer ext-real set
(1,k,(1,k,(k,1,x),(k,1,y))) is non empty V2() V15() V18( NAT ) V19( INT ) Function-like one-to-one V36() V43(1) FinSequence-like FinSubsequence-like V51() V52() V53() V55() V56() V57() V58() FinSequence of INT
Sum (1,k,(1,k,(k,1,x),(k,1,y))) is V11() V12() integer ext-real V50() Element of INT
(k) |^ 1 is V6() V10() V11() V12() integer V36() V41() ext-real non negative set
(1,k,1,(k,1,x)) is V11() V12() integer ext-real set
(1,k,1,(k,1,y)) is V11() V12() integer ext-real set
(1,k,1,(k,1,x)) + (1,k,1,(k,1,y)) is V11() V12() integer ext-real set
(((1,k,1,(k,1,x)) + (1,k,1,(k,1,y)))) is V11() V12() integer ext-real set
((k) |^ 1) * (((1,k,1,(k,1,x)) + (1,k,1,(k,1,y)))) is V11() V12() integer ext-real set
(1,k,(1,k,(k,1,x),(k,1,y))) + (((k) |^ 1) * (((1,k,1,(k,1,x)) + (1,k,1,(k,1,y))))) is V11() V12() integer ext-real set
((x + y),k) is V11() V12() integer ext-real set
((x + y)) is V11() V12() integer ext-real set
((x + y)) * (k) is V11() V12() integer ext-real set
(x + y) - (((x + y)) * (k)) is V11() V12() integer ext-real set
((x + y),k) + (((x + y)) * (k)) is V11() V12() integer ext-real set
(x + y) - 0 is V11() V12() integer ext-real non negative set
k is V6() V10() V11() V12() integer V36() V41() ext-real non negative set
x is V6() V10() V11() V12() integer V36() V41() ext-real non negative set
y is V6() V10() V11() V12() integer V36() V41() ext-real non negative set
x + y is V6() V10() V11() V12() integer V36() V41() ext-real non negative set
(k,n,x) is V15() V18( NAT ) V19((k)) Function-like V36() V43(n) FinSequence-like FinSubsequence-like V51() V52() V53() FinSequence of (k)
(k) is non empty V61() V62() V63() V64() V65() Element of K6(INT)
(k) is V6() V10() V11() V12() integer V36() V41() ext-real non negative V50() V61() V62() V63() V64() V65() V66() Element of NAT
2 to_power k is V11() V12() ext-real set
2 |^ k is V6() V10() V11() V12() integer V36() V41() ext-real non negative set
(k) - 1 is V11() V12() integer ext-real set
- (k) is V11() V12() integer ext-real non positive set
(- (k)) + 1 is V11() V12() integer ext-real set
{ b₁ where b₁ is V11() V12() integer ext-real V50() Element of INT : ( b₁ <= (k) - 1 & (- (k)) + 1 <= b₁ ) } is set
(k,n,y) is V15() V18( NAT ) V19((k)) Function-like V36() V43(n) FinSequence-like FinSubsequence-like V51() V52() V53() FinSequence of (k)
(n,k,(k,n,x),(k,n,y)) is V15() V18( NAT ) V19((k)) Function-like V36() V43(n) FinSequence-like FinSubsequence-like V51() V52() V53() FinSequence of (k)
(n,k,(n,k,(k,n,x),(k,n,y))) is V11() V12() integer ext-real set
(n,k,(n,k,(k,n,x),(k,n,y))) is V15() V18( NAT ) V19( INT ) Function-like V36() V43(n) FinSequence-like FinSubsequence-like V51() V52() V53() FinSequence of INT
Sum (n,k,(n,k,(k,n,x),(k,n,y))) is V11() V12() integer ext-real V50() Element of INT
(k) |^ n is V6() V10() V11() V12() integer V36() V41() ext-real non negative set
(n,k,n,(k,n,x)) is V11() V12() integer ext-real set
(n,k,n,(k,n,y)) is V11() V12() integer ext-real set
(n,k,n,(k,n,x)) + (n,k,n,(k,n,y)) is V11() V12() integer ext-real set
(((n,k,n,(k,n,x)) + (n,k,n,(k,n,y)))) is V11() V12() integer ext-real set
((k) |^ n) * (((n,k,n,(k,n,x)) + (n,k,n,(k,n,y)))) is V11() V12() integer ext-real set
(n,k,(n,k,(k,n,x),(k,n,y))) + (((k) |^ n) * (((n,k,n,(k,n,x)) + (n,k,n,(k,n,y))))) is V11() V12() integer ext-real set