:: NTALGO_1 semantic presentation

REAL is non empty V38() set
NAT is non empty V7() V8() V9() V38() V43() V44() Element of bool REAL
bool REAL is non empty V38() set
COMPLEX is non empty V38() set
RAT is non empty V38() set
INT is non empty V38() set
[:COMPLEX,COMPLEX:] is non empty V38() set
bool [:COMPLEX,COMPLEX:] is non empty V38() set
[:[:COMPLEX,COMPLEX:],COMPLEX:] is non empty V38() set
bool [:[:COMPLEX,COMPLEX:],COMPLEX:] is non empty V38() set
[:REAL,REAL:] is non empty V38() set
bool [:REAL,REAL:] is non empty V38() set
[:[:REAL,REAL:],REAL:] is non empty V38() set
bool [:[:REAL,REAL:],REAL:] is non empty V38() set
[:RAT,RAT:] is non empty V38() set
bool [:RAT,RAT:] is non empty V38() set
[:[:RAT,RAT:],RAT:] is non empty V38() set
bool [:[:RAT,RAT:],RAT:] is non empty V38() set
[:INT,INT:] is non empty V38() set
bool [:INT,INT:] is non empty V38() set
[:[:INT,INT:],INT:] is non empty V38() set
bool [:[:INT,INT:],INT:] is non empty V38() set
[:NAT,NAT:] is non empty V38() set
[:[:NAT,NAT:],NAT:] is non empty V38() set
bool [:[:NAT,NAT:],NAT:] is non empty V38() set
NAT is non empty V7() V8() V9() V38() V43() V44() set
bool NAT is non empty V38() set
bool NAT is non empty V38() set
K281() is set
1 is ext-real positive non negative non empty V7() V8() V9() V13() V14() V15() integer V38() V43() Element of NAT
{} is ext-real non positive non negative empty V7() V8() V9() V11() V12() V13() V14() V15() integer functional V38() V43() V45( {} ) FinSequence-membered set
2 is ext-real positive non negative non empty V7() V8() V9() V13() V14() V15() integer V38() V43() Element of NAT
3 is ext-real positive non negative non empty V7() V8() V9() V13() V14() V15() integer V38() V43() Element of NAT
0 is ext-real non positive non negative empty V7() V8() V9() V11() V12() V13() V14() V15() integer functional V38() V43() V45( {} ) FinSequence-membered Element of NAT
Seg 1 is non empty trivial V38() V45(1) Element of bool NAT
{ b₁ where b₁ is ext-real non negative V7() V8() V9() V13() V14() V15() integer V38() V43() Element of NAT : ( 1 <= b₁ & b₁ <= 1 ) } is set
{1} is non empty trivial V45(1) set
Seg 2 is non empty V38() V45(2) Element of bool NAT
{ b₁ where b₁ is ext-real non negative V7() V8() V9() V13() V14() V15() integer V38() V43() Element of NAT : ( 1 <= b₁ & b₁ <= 2 ) } is set
{1,2} is non empty set
<*> REAL is ext-real non positive non negative empty proper V7() V8() V9() V11() V12() V13() V14() V15() integer V18() V21( NAT ) V22( REAL ) Function-like functional V38() V43() V45( {} ) FinSequence-like FinSubsequence-like FinSequence-membered V60() V61() V62() V63() FinSequence of REAL
[:NAT,REAL:] is non empty V38() set
Product (<*> REAL) is ext-real V14() V15() Element of REAL
nlist is ext-real V14() V15() integer set
a is ext-real V14() V15() integer set
nlist mod a is ext-real V14() V15() integer set
(nlist mod a) mod a is ext-real V14() V15() integer set
nlist + 0 is ext-real V14() V15() integer set
(nlist + 0) mod a is ext-real V14() V15() integer set
0 mod a is ext-real V14() V15() integer set
(nlist mod a) + (0 mod a) is ext-real V14() V15() integer set
((nlist mod a) + (0 mod a)) mod a is ext-real V14() V15() integer set
(nlist mod a) + 0 is ext-real V14() V15() integer set
((nlist mod a) + 0) mod a is ext-real V14() V15() integer set
nlist is ext-real non negative V7() V8() V9() V13() V14() V15() integer V38() V43() Element of NAT
nlist gcd 0 is ext-real non negative V7() V8() V9() V13() V14() V15() integer V38() V43() Element of NAT
0 * nlist is ext-real non positive non negative empty V7() V8() V9() V11() V12() V13() V14() V15() integer functional V38() V43() V45( {} ) FinSequence-membered Element of NAT
a is ext-real V14() V15() integer set
bool [:NAT,NAT:] is non empty V38() set
nlist is ext-real V14() V15() integer Element of INT
abs nlist is ext-real non negative V7() V8() V9() V13() V14() V15() integer V38() V43() Element of NAT
a is ext-real V14() V15() integer Element of INT
abs a is ext-real non negative V7() V8() V9() V13() V14() V15() integer V38() V43() Element of NAT
y is ext-real non negative V7() V8() V9() V13() V14() V15() integer V38() V43() Element of NAT
x is ext-real non negative V7() V8() V9() V13() V14() V15() integer V38() V43() Element of NAT
x mod y is ext-real non negative V7() V8() V9() V13() V14() V15() integer V38() V43() Element of NAT
b is V18() V21( NAT ) V22( NAT ) Function-like V32( NAT , NAT ) V60() V61() V62() V63() Element of bool [:NAT,NAT:]
b . 0 is ext-real non negative V7() V8() V9() V13() V14() V15() integer V38() V43() Element of NAT
x is V18() V21( NAT ) V22( NAT ) Function-like V32( NAT , NAT ) V60() V61() V62() V63() Element of bool [:NAT,NAT:]
x . 0 is ext-real non negative V7() V8() V9() V13() V14() V15() integer V38() V43() Element of NAT
y is ext-real non negative V7() V8() V9() V13() V14() V15() integer V38() V43() Element of NAT
y + 1 is ext-real positive non negative non empty V7() V8() V9() V13() V14() V15() integer V38() V43() Element of NAT
b . (y + 1) is ext-real non negative V7() V8() V9() V13() V14() V15() integer V38() V43() Element of NAT
x . y is ext-real non negative V7() V8() V9() V13() V14() V15() integer V38() V43() Element of NAT
m is ext-real non negative V7() V8() V9() V13() V14() V15() integer V38() V43() Element of NAT
m + 1 is ext-real positive non negative non empty V7() V8() V9() V13() V14() V15() integer V38() V43() Element of NAT
x . (m + 1) is ext-real non negative V7() V8() V9() V13() V14() V15() integer V38() V43() Element of NAT
b . m is ext-real non negative V7() V8() V9() V13() V14() V15() integer V38() V43() Element of NAT
x . m is ext-real non negative V7() V8() V9() V13() V14() V15() integer V38() V43() Element of NAT
(b . m) mod (x . m) is ext-real non negative V7() V8() V9() V13() V14() V15() integer V38() V43() Element of NAT
nlist is ext-real V14() V15() integer Element of INT
abs nlist is ext-real non negative V7() V8() V9() V13() V14() V15() integer V38() V43() Element of NAT
a is ext-real V14() V15() integer Element of INT
abs a is ext-real non negative V7() V8() V9() V13() V14() V15() integer V38() V43() Element of NAT
b is V18() V21( NAT ) V22( NAT ) Function-like V32( NAT , NAT ) V60() V61() V62() V63() Element of bool [:NAT,NAT:]
b . 0 is ext-real non negative V7() V8() V9() V13() V14() V15() integer V38() V43() Element of NAT
x is V18() V21( NAT ) V22( NAT ) Function-like V32( NAT , NAT ) V60() V61() V62() V63() Element of bool [:NAT,NAT:]
x . 0 is ext-real non negative V7() V8() V9() V13() V14() V15() integer V38() V43() Element of NAT
y is V18() V21( NAT ) V22( NAT ) Function-like V32( NAT , NAT ) V60() V61() V62() V63() Element of bool [:NAT,NAT:]
y . 0 is ext-real non negative V7() V8() V9() V13() V14() V15() integer V38() V43() Element of NAT
m is V18() V21( NAT ) V22( NAT ) Function-like V32( NAT , NAT ) V60() V61() V62() V63() Element of bool [:NAT,NAT:]
m . 0 is ext-real non negative V7() V8() V9() V13() V14() V15() integer V38() V43() Element of NAT
i is ext-real non negative V7() V8() V9() V13() V14() V15() integer V38() V43() Element of NAT
b . i is ext-real non negative V7() V8() V9() V13() V14() V15() integer V38() V43() Element of NAT
y . i is ext-real non negative V7() V8() V9() V13() V14() V15() integer V38() V43() Element of NAT
x . i is ext-real non negative V7() V8() V9() V13() V14() V15() integer V38() V43() Element of NAT
m . i is ext-real non negative V7() V8() V9() V13() V14() V15() integer V38() V43() Element of NAT
i + 1 is ext-real positive non negative non empty V7() V8() V9() V13() V14() V15() integer V38() V43() Element of NAT
b . (i + 1) is ext-real non negative V7() V8() V9() V13() V14() V15() integer V38() V43() Element of NAT
y . (i + 1) is ext-real non negative V7() V8() V9() V13() V14() V15() integer V38() V43() Element of NAT
x . (i + 1) is ext-real non negative V7() V8() V9() V13() V14() V15() integer V38() V43() Element of NAT
m . (i + 1) is ext-real non negative V7() V8() V9() V13() V14() V15() integer V38() V43() Element of NAT
(b . i) mod (x . i) is ext-real non negative V7() V8() V9() V13() V14() V15() integer V38() V43() Element of NAT
nlist is ext-real V14() V15() integer Element of INT
abs nlist is ext-real non negative V7() V8() V9() V13() V14() V15() integer V38() V43() Element of NAT
a is ext-real V14() V15() integer Element of INT
abs a is ext-real non negative V7() V8() V9() V13() V14() V15() integer V38() V43() Element of NAT
b is V18() V21( NAT ) V22( NAT ) Function-like V32( NAT , NAT ) V60() V61() V62() V63() Element of bool [:NAT,NAT:]
b . 0 is ext-real non negative V7() V8() V9() V13() V14() V15() integer V38() V43() Element of NAT
x is V18() V21( NAT ) V22( NAT ) Function-like V32( NAT , NAT ) V60() V61() V62() V63() Element of bool [:NAT,NAT:]
x . 0 is ext-real non negative V7() V8() V9() V13() V14() V15() integer V38() V43() Element of NAT
{ b₁ where b₁ is ext-real non negative V7() V8() V9() V13() V14() V15() integer V38() V43() Element of NAT : x . b₁ = 0 } is set
min* { b₁ where b₁ is ext-real non negative V7() V8() V9() V13() V14() V15() integer V38() V43() Element of NAT : x . b₁ = 0 } is ext-real non negative V7() V8() V9() V13() V14() V15() integer V38() V43() Element of NAT
b . (min* { b₁ where b₁ is ext-real non negative V7() V8() V9() V13() V14() V15() integer V38() V43() Element of NAT : x . b₁ = 0 } ) is ext-real non negative V7() V8() V9() V13() V14() V15() integer V38() V43() Element of NAT
b is ext-real non negative V7() V8() V9() V13() V14() V15() integer V38() V43() Element of NAT
x is ext-real non negative V7() V8() V9() V13() V14() V15() integer V38() V43() Element of NAT
y is V18() V21( NAT ) V22( NAT ) Function-like V32( NAT , NAT ) V60() V61() V62() V63() Element of bool [:NAT,NAT:]
y . 0 is ext-real non negative V7() V8() V9() V13() V14() V15() integer V38() V43() Element of NAT
m is V18() V21( NAT ) V22( NAT ) Function-like V32( NAT , NAT ) V60() V61() V62() V63() Element of bool [:NAT,NAT:]
m . 0 is ext-real non negative V7() V8() V9() V13() V14() V15() integer V38() V43() Element of NAT
{ b₁ where b₁ is ext-real non negative V7() V8() V9() V13() V14() V15() integer V38() V43() Element of NAT : m . b₁ = 0 } is set
min* { b₁ where b₁ is ext-real non negative V7() V8() V9() V13() V14() V15() integer V38() V43() Element of NAT : m . b₁ = 0 } is ext-real non negative V7() V8() V9() V13() V14() V15() integer V38() V43() Element of NAT
y . (min* { b₁ where b₁ is ext-real non negative V7() V8() V9() V13() V14() V15() integer V38() V43() Element of NAT : m . b₁ = 0 } ) is ext-real non negative V7() V8() V9() V13() V14() V15() integer V38() V43() Element of NAT
y is V18() V21( NAT ) V22( NAT ) Function-like V32( NAT , NAT ) V60() V61() V62() V63() Element of bool [:NAT,NAT:]
y . 0 is ext-real non negative V7() V8() V9() V13() V14() V15() integer V38() V43() Element of NAT
m is V18() V21( NAT ) V22( NAT ) Function-like V32( NAT , NAT ) V60() V61() V62() V63() Element of bool [:NAT,NAT:]
m . 0 is ext-real non negative V7() V8() V9() V13() V14() V15() integer V38() V43() Element of NAT
{ b₁ where b₁ is ext-real non negative V7() V8() V9() V13() V14() V15() integer V38() V43() Element of NAT : m . b₁ = 0 } is set
min* { b₁ where b₁ is ext-real non negative V7() V8() V9() V13() V14() V15() integer V38() V43() Element of NAT : m . b₁ = 0 } is ext-real non negative V7() V8() V9() V13() V14() V15() integer V38() V43() Element of NAT
y . (min* { b₁ where b₁ is ext-real non negative V7() V8() V9() V13() V14() V15() integer V38() V43() Element of NAT : m . b₁ = 0 } ) is ext-real non negative V7() V8() V9() V13() V14() V15() integer V38() V43() Element of NAT
i is V18() V21( NAT ) V22( NAT ) Function-like V32( NAT , NAT ) V60() V61() V62() V63() Element of bool [:NAT,NAT:]
i . 0 is ext-real non negative V7() V8() V9() V13() V14() V15() integer V38() V43() Element of NAT
I0 is V18() V21( NAT ) V22( NAT ) Function-like V32( NAT , NAT ) V60() V61() V62() V63() Element of bool [:NAT,NAT:]
I0 . 0 is ext-real non negative V7() V8() V9() V13() V14() V15() integer V38() V43() Element of NAT
{ b₁ where b₁ is ext-real non negative V7() V8() V9() V13() V14() V15() integer V38() V43() Element of NAT : I0 . b₁ = 0 } is set
min* { b₁ where b₁ is ext-real non negative V7() V8() V9() V13() V14() V15() integer V38() V43() Element of NAT : I0 . b₁ = 0 } is ext-real non negative V7() V8() V9() V13() V14() V15() integer V38() V43() Element of NAT
i . (min* { b₁ where b₁ is ext-real non negative V7() V8() V9() V13() V14() V15() integer V38() V43() Element of NAT : I0 . b₁ = 0 } ) is ext-real non negative V7() V8() V9() V13() V14() V15() integer V38() V43() Element of NAT
i is V18() V21( NAT ) V22( NAT ) Function-like V32( NAT , NAT ) V60() V61() V62() V63() Element of bool [:NAT,NAT:]
i . 0 is ext-real non negative V7() V8() V9() V13() V14() V15() integer V38() V43() Element of NAT
I0 is V18() V21( NAT ) V22( NAT ) Function-like V32( NAT , NAT ) V60() V61() V62() V63() Element of bool [:NAT,NAT:]
I0 . 0 is ext-real non negative V7() V8() V9() V13() V14() V15() integer V38() V43() Element of NAT
{ b₁ where b₁ is ext-real non negative V7() V8() V9() V13() V14() V15() integer V38() V43() Element of NAT : I0 . b₁ = 0 } is set
min* { b₁ where b₁ is ext-real non negative V7() V8() V9() V13() V14() V15() integer V38() V43() Element of NAT : I0 . b₁ = 0 } is ext-real non negative V7() V8() V9() V13() V14() V15() integer V38() V43() Element of NAT
i . (min* { b₁ where b₁ is ext-real non negative V7() V8() V9() V13() V14() V15() integer V38() V43() Element of NAT : I0 . b₁ = 0 } ) is ext-real non negative V7() V8() V9() V13() V14() V15() integer V38() V43() Element of NAT
nlist is ext-real V14() V15() integer Element of INT
abs nlist is ext-real non negative V7() V8() V9() V13() V14() V15() integer V38() V43() Element of NAT
a is ext-real V14() V15() integer Element of INT
abs a is ext-real non negative V7() V8() V9() V13() V14() V15() integer V38() V43() Element of NAT
b is V18() V21( NAT ) V22( NAT ) Function-like V32( NAT , NAT ) V60() V61() V62() V63() Element of bool [:NAT,NAT:]
b . 0 is ext-real non negative V7() V8() V9() V13() V14() V15() integer V38() V43() Element of NAT
x is V18() V21( NAT ) V22( NAT ) Function-like V32( NAT , NAT ) V60() V61() V62() V63() Element of bool [:NAT,NAT:]
x . 0 is ext-real non negative V7() V8() V9() V13() V14() V15() integer V38() V43() Element of NAT
y is ext-real non negative V7() V8() V9() V13() V14() V15() integer V38() V43() Element of NAT
x . y is ext-real non negative V7() V8() V9() V13() V14() V15() integer V38() V43() Element of NAT
b . y is ext-real non negative V7() V8() V9() V13() V14() V15() integer V38() V43() Element of NAT
(b . y) gcd (x . y) is ext-real non negative V7() V8() V9() V13() V14() V15() integer V38() V43() Element of NAT
y + 1 is ext-real positive non negative non empty V7() V8() V9() V13() V14() V15() integer V38() V43() Element of NAT
b . (y + 1) is ext-real non negative V7() V8() V9() V13() V14() V15() integer V38() V43() Element of NAT
x . (y + 1) is ext-real non negative V7() V8() V9() V13() V14() V15() integer V38() V43() Element of NAT
(b . (y + 1)) gcd (x . (y + 1)) is ext-real non negative V7() V8() V9() V13() V14() V15() integer V38() V43() Element of NAT
(b . y) mod (x . y) is ext-real non negative V7() V8() V9() V13() V14() V15() integer V38() V43() Element of NAT
(b . y) div (x . y) is ext-real non negative V7() V8() V9() V13() V14() V15() integer V38() V43() Element of NAT
(b . y) / (x . y) is ext-real non negative V14() V15() set
[\((b . y) / (x . y))/] is ext-real V14() V15() integer set
((b . y) div (x . y)) * (x . y) is ext-real non negative V7() V8() V9() V13() V14() V15() integer V38() V43() Element of NAT
(b . y) - (((b . y) div (x . y)) * (x . y)) is ext-real V14() V15() integer set
i is ext-real V14() V15() integer set
((b . y) gcd (x . y)) * i is ext-real V14() V15() integer set
I0 is ext-real V14() V15() integer set
((b . y) gcd (x . y)) * I0 is ext-real V14() V15() integer set
i is ext-real V14() V15() integer set
((b . y) gcd (x . y)) * i is ext-real V14() V15() integer set
I0 is ext-real V14() V15() integer set
((b . y) gcd (x . y)) * I0 is ext-real V14() V15() integer set
((b . y) div (x . y)) * (((b . y) gcd (x . y)) * I0) is ext-real V14() V15() integer set
(((b . y) gcd (x . y)) * i) - (((b . y) div (x . y)) * (((b . y) gcd (x . y)) * I0)) is ext-real V14() V15() integer set
((b . y) div (x . y)) * I0 is ext-real V14() V15() integer set
i - (((b . y) div (x . y)) * I0) is ext-real V14() V15() integer set
(i - (((b . y) div (x . y)) * I0)) * ((b . y) gcd (x . y)) is ext-real V14() V15() integer set
i is ext-real V14() V15() integer set
(b . y) div (x . y) is ext-real non negative V7() V8() V9() V13() V14() V15() integer V38() V43() Element of NAT
(b . y) / (x . y) is ext-real non negative V14() V15() set
[\((b . y) / (x . y))/] is ext-real V14() V15() integer set
((b . y) div (x . y)) * (x . y) is ext-real non negative V7() V8() V9() V13() V14() V15() integer V38() V43() Element of NAT
(b . y) - (((b . y) div (x . y)) * (x . y)) is ext-real V14() V15() integer set
(x . (y + 1)) + (((b . y) div (x . y)) * (x . y)) is ext-real non negative V7() V8() V9() V13() V14() V15() integer V38() V43() Element of NAT
I0 is ext-real V14() V15() integer set
i * I0 is ext-real V14() V15() integer set
m is ext-real V14() V15() integer set
i * m is ext-real V14() V15() integer set
I0 is ext-real V14() V15() integer set
i * I0 is ext-real V14() V15() integer set
m is ext-real V14() V15() integer set
i * m is ext-real V14() V15() integer set
((b . y) div (x . y)) * (i * m) is ext-real V14() V15() integer set
(i * I0) + (((b . y) div (x . y)) * (i * m)) is ext-real V14() V15() integer set
((b . y) div (x . y)) * m is ext-real V14() V15() integer set
I0 + (((b . y) div (x . y)) * m) is ext-real V14() V15() integer set
i * (I0 + (((b . y) div (x . y)) * m)) is ext-real V14() V15() integer set
nlist is ext-real V14() V15() integer Element of INT
abs nlist is ext-real non negative V7() V8() V9() V13() V14() V15() integer V38() V43() Element of NAT
a is ext-real V14() V15() integer Element of INT
abs a is ext-real non negative V7() V8() V9() V13() V14() V15() integer V38() V43() Element of NAT
b is V18() V21( NAT ) V22( NAT ) Function-like V32( NAT , NAT ) V60() V61() V62() V63() Element of bool [:NAT,NAT:]
b . 0 is ext-real non negative V7() V8() V9() V13() V14() V15() integer V38() V43() Element of NAT
x is V18() V21( NAT ) V22( NAT ) Function-like V32( NAT , NAT ) V60() V61() V62() V63() Element of bool [:NAT,NAT:]
x . 0 is ext-real non negative V7() V8() V9() V13() V14() V15() integer V38() V43() Element of NAT
(b . 0) gcd (x . 0) is ext-real non negative V7() V8() V9() V13() V14() V15() integer V38() V43() Element of NAT
y is ext-real non negative V7() V8() V9() V13() V14() V15() integer V38() V43() Element of NAT
x . y is ext-real non negative V7() V8() V9() V13() V14() V15() integer V38() V43() Element of NAT
b . y is ext-real non negative V7() V8() V9() V13() V14() V15() integer V38() V43() Element of NAT
(b . y) gcd (x . y) is ext-real non negative V7() V8() V9() V13() V14() V15() integer V38() V43() Element of NAT
y + 1 is ext-real positive non negative non empty V7() V8() V9() V13() V14() V15() integer V38() V43() Element of NAT
x . (y + 1) is ext-real non negative V7() V8() V9() V13() V14() V15() integer V38() V43() Element of NAT
b . (y + 1) is ext-real non negative V7() V8() V9() V13() V14() V15() integer V38() V43() Element of NAT
(b . (y + 1)) gcd (x . (y + 1)) is ext-real non negative V7() V8() V9() V13() V14() V15() integer V38() V43() Element of NAT
(b . y) mod (x . y) is ext-real non negative V7() V8() V9() V13() V14() V15() integer V38() V43() Element of NAT
y is ext-real non negative V7() V8() V9() V13() V14() V15() integer V38() V43() Element of NAT
x . y is ext-real non negative V7() V8() V9() V13() V14() V15() integer V38() V43() Element of NAT
b . y is ext-real non negative V7() V8() V9() V13() V14() V15() integer V38() V43() Element of NAT
(b . y) gcd (x . y) is ext-real non negative V7() V8() V9() V13() V14() V15() integer V38() V43() Element of NAT
nlist is ext-real V14() V15() integer Element of INT
abs nlist is ext-real non negative V7() V8() V9() V13() V14() V15() integer V38() V43() Element of NAT
a is ext-real V14() V15() integer Element of INT
abs a is ext-real non negative V7() V8() V9() V13() V14() V15() integer V38() V43() Element of NAT
b is V18() V21( NAT ) V22( NAT ) Function-like V32( NAT , NAT ) V60() V61() V62() V63() Element of bool [:NAT,NAT:]
b . 0 is ext-real non negative V7() V8() V9() V13() V14() V15() integer V38() V43() Element of NAT
x is V18() V21( NAT ) V22( NAT ) Function-like V32( NAT , NAT ) V60() V61() V62() V63() Element of bool [:NAT,NAT:]
x . 0 is ext-real non negative V7() V8() V9() V13() V14() V15() integer V38() V43() Element of NAT
{ b₁ where b₁ is ext-real non negative V7() V8() V9() V13() V14() V15() integer V38() V43() Element of NAT : x . b₁ = 0 } is set
y is set
m is ext-real non negative V7() V8() V9() V13() V14() V15() integer V38() V43() Element of NAT
x . m is ext-real non negative V7() V8() V9() V13() V14() V15() integer V38() V43() Element of NAT
y is ext-real non negative V7() V8() V9() V13() V14() V15() integer V38() V43() Element of NAT
y + 1 is ext-real positive non negative non empty V7() V8() V9() V13() V14() V15() integer V38() V43() Element of NAT
x . (y + 1) is ext-real non negative V7() V8() V9() V13() V14() V15() integer V38() V43() Element of NAT
x . y is ext-real non negative V7() V8() V9() V13() V14() V15() integer V38() V43() Element of NAT
(x . y) - 1 is ext-real V14() V15() integer set
b . y is ext-real non negative V7() V8() V9() V13() V14() V15() integer V38() V43() Element of NAT
(b . y) mod (x . y) is ext-real non negative V7() V8() V9() V13() V14() V15() integer V38() V43() Element of NAT
(x . (y + 1)) + 1 is ext-real positive non negative non empty V7() V8() V9() V13() V14() V15() integer V38() V43() Element of NAT
((x . (y + 1)) + 1) - 1 is ext-real V14() V15() integer set
(x . 0) - 0 is ext-real non negative V14() V15() integer set
y is ext-real non negative V7() V8() V9() V13() V14() V15() integer V38() V43() Element of NAT
x . y is ext-real non negative V7() V8() V9() V13() V14() V15() integer V38() V43() Element of NAT
(x . 0) - y is ext-real V14() V15() integer set
y + 1 is ext-real positive non negative non empty V7() V8() V9() V13() V14() V15() integer V38() V43() Element of NAT
x . (y + 1) is ext-real non negative V7() V8() V9() V13() V14() V15() integer V38() V43() Element of NAT
(x . 0) - (y + 1) is ext-real V14() V15() integer set
(x . y) - 1 is ext-real V14() V15() integer set
((x . 0) - y) - 1 is ext-real V14() V15() integer set
x . (x . 0) is ext-real non negative V7() V8() V9() V13() V14() V15() integer V38() V43() Element of NAT
(x . 0) - (x . 0) is ext-real V14() V15() integer set
y is ext-real non negative V7() V8() V9() V13() V14() V15() integer V38() V43() Element of NAT
x . y is ext-real non negative V7() V8() V9() V13() V14() V15() integer V38() V43() Element of NAT
y is ext-real non negative V7() V8() V9() V13() V14() V15() integer V38() V43() Element of NAT
x . y is ext-real non negative V7() V8() V9() V13() V14() V15() integer V38() V43() Element of NAT
nlist is ext-real V14() V15() integer Element of INT
a is ext-real V14() V15() integer Element of INT
(nlist,a) is ext-real non negative V7() V8() V9() V13() V14() V15() integer V38() V43() Element of NAT
nlist gcd a is ext-real non negative V7() V8() V9() V13() V14() V15() integer V38() V43() set
abs nlist is ext-real non negative V7() V8() V9() V13() V14() V15() integer V38() V43() Element of NAT
abs a is ext-real non negative V7() V8() V9() V13() V14() V15() integer V38() V43() Element of NAT
b is V18() V21( NAT ) V22( NAT ) Function-like V32( NAT , NAT ) V60() V61() V62() V63() Element of bool [:NAT,NAT:]
b . 0 is ext-real non negative V7() V8() V9() V13() V14() V15() integer V38() V43() Element of NAT
x is V18() V21( NAT ) V22( NAT ) Function-like V32( NAT , NAT ) V60() V61() V62() V63() Element of bool [:NAT,NAT:]
x . 0 is ext-real non negative V7() V8() V9() V13() V14() V15() integer V38() V43() Element of NAT
{ b₁ where b₁ is ext-real non negative V7() V8() V9() V13() V14() V15() integer V38() V43() Element of NAT : x . b₁ = 0 } is set
min* { b₁ where b₁ is ext-real non negative V7() V8() V9() V13() V14() V15() integer V38() V43() Element of NAT : x . b₁ = 0 } is ext-real non negative V7() V8() V9() V13() V14() V15() integer V38() V43() Element of NAT
b . (min* { b₁ where b₁ is ext-real non negative V7() V8() V9() V13() V14() V15() integer V38() V43() Element of NAT : x . b₁ = 0 } ) is ext-real non negative V7() V8() V9() V13() V14() V15() integer V38() V43() Element of NAT
(b . 0) gcd (x . 0) is ext-real non negative V7() V8() V9() V13() V14() V15() integer V38() V43() Element of NAT
m is ext-real non negative V7() V8() V9() V13() V14() V15() integer V38() V43() Element of NAT
x . m is ext-real non negative V7() V8() V9() V13() V14() V15() integer V38() V43() Element of NAT
1 - 1 is ext-real V14() V15() integer set
(min* { b₁ where b₁ is ext-real non negative V7() V8() V9() V13() V14() V15() integer V38() V43() Element of NAT : x . b₁ = 0 } ) - 1 is ext-real V14() V15() integer set
m is ext-real non negative V7() V8() V9() V13() V14() V15() integer V38() V43() Element of NAT
x . m is ext-real non negative V7() V8() V9() V13() V14() V15() integer V38() V43() Element of NAT
(min* { b₁ where b₁ is ext-real non negative V7() V8() V9() V13() V14() V15() integer V38() V43() Element of NAT : x . b₁ = 0 } ) - 0 is ext-real non negative V14() V15() integer set
(b . 0) gcd (x . 0) is ext-real non negative V7() V8() V9() V13() V14() V15() integer V38() V43() Element of NAT
b . m is ext-real non negative V7() V8() V9() V13() V14() V15() integer V38() V43() Element of NAT
(b . m) gcd (x . m) is ext-real non negative V7() V8() V9() V13() V14() V15() integer V38() V43() Element of NAT
m + 1 is ext-real positive non negative non empty V7() V8() V9() V13() V14() V15() integer V38() V43() Element of NAT
b . (m + 1) is ext-real non negative V7() V8() V9() V13() V14() V15() integer V38() V43() Element of NAT
x . (m + 1) is ext-real non negative V7() V8() V9() V13() V14() V15() integer V38() V43() Element of NAT
(b . (m + 1)) gcd (x . (m + 1)) is ext-real non negative V7() V8() V9() V13() V14() V15() integer V38() V43() Element of NAT
x . (min* { b₁ where b₁ is ext-real non negative V7() V8() V9() V13() V14() V15() integer V38() V43() Element of NAT : x . b₁ = 0 } ) is ext-real non negative V7() V8() V9() V13() V14() V15() integer V38() V43() Element of NAT
(b . (min* { b₁ where b₁ is ext-real non negative V7() V8() V9() V13() V14() V15() integer V38() V43() Element of NAT : x . b₁ = 0 } )) gcd (x . (min* { b₁ where b₁ is ext-real non negative V7() V8() V9() V13() V14() V15() integer V38() V43() Element of NAT : x . b₁ = 0 } )) is ext-real non negative V7() V8() V9() V13() V14() V15() integer V38() V43() Element of NAT
i is ext-real non negative V7() V8() V9() V13() V14() V15() integer V38() V43() Element of NAT
x . i is ext-real non negative V7() V8() V9() V13() V14() V15() integer V38() V43() Element of NAT
F₁() is non empty set
F₂() is non empty set
F₃() is non empty set
F₄() is non empty set
[:NAT,F₁():] is non empty V38() set
bool [:NAT,F₁():] is non empty V38() set
[:NAT,F₂():] is non empty V38() set
bool [:NAT,F₂():] is non empty V38() set
[:NAT,F₃():] is non empty V38() set
bool [:NAT,F₃():] is non empty V38() set
[:NAT,F₄():] is non empty V38() set
bool [:NAT,F₄():] is non empty V38() set
F₅() is Element of F₁()
F₆() is Element of F₂()
F₇() is Element of F₃()
F₈() is Element of F₄()
[:F₁(),F₂():] is non empty set
[:F₃(),F₄():] is non empty set
nlist is ext-real non negative V7() V8() V9() V13() V14() V15() integer V38() V43() Element of NAT
a is Element of [:F₁(),F₂():]
a `1 is set
a `2 is set
b is Element of [:F₃(),F₄():]
b `1 is set
b `2 is set
x is Element of F₁()
y is Element of F₂()
m is Element of F₃()
i is Element of F₄()
[x,y] is V29() set
[m,i] is V29() set
I0 is Element of [:F₁(),F₂():]
I0 `1 is set
I0 `2 is set
m is Element of [:F₃(),F₄():]
m `1 is set
m `2 is set
[x,y] `1 is set
[x,y] `2 is set
[m,i] `1 is set
[m,i] `2 is set
[F₅(),F₆()] is V29() set
[F₇(),F₈()] is V29() set
[:NAT,[:F₁(),F₂():]:] is non empty V38() set
bool [:NAT,[:F₁(),F₂():]:] is non empty V38() set
[:NAT,[:F₃(),F₄():]:] is non empty V38() set
bool [:NAT,[:F₃(),F₄():]:] is non empty V38() set
nlist is Element of [:F₁(),F₂():]
a is Element of [:F₃(),F₄():]
b is V18() V21( NAT ) V22([:F₁(),F₂():]) Function-like V32( NAT ,[:F₁(),F₂():]) Element of bool [:NAT,[:F₁(),F₂():]:]
b . 0 is Element of [:F₁(),F₂():]
x is V18() V21( NAT ) V22([:F₃(),F₄():]) Function-like V32( NAT ,[:F₃(),F₄():]) Element of bool [:NAT,[:F₃(),F₄():]:]
x . 0 is Element of [:F₃(),F₄():]
pr1 b is V18() V21( NAT ) V22(F₁()) Function-like V32( NAT ,F₁()) Element of bool [:NAT,F₁():]
(pr1 b) . 0 is Element of F₁()
pr2 b is V18() V21( NAT ) V22(F₂()) Function-like V32( NAT ,F₂()) Element of bool [:NAT,F₂():]
(pr2 b) . 0 is Element of F₂()
pr1 x is V18() V21( NAT ) V22(F₃()) Function-like V32( NAT ,F₃()) Element of bool [:NAT,F₃():]
(pr1 x) . 0 is Element of F₃()
pr2 x is V18() V21( NAT ) V22(F₄()) Function-like V32( NAT ,F₄()) Element of bool [:NAT,F₄():]
(pr2 x) . 0 is Element of F₄()
(b . 0) `1 is set
(b . 0) `2 is set
(x . 0) `1 is set
(x . 0) `2 is set
y is ext-real non negative V7() V8() V9() V13() V14() V15() integer V38() V43() Element of NAT
(pr1 b) . y is Element of F₁()
(pr2 b) . y is Element of F₂()
(pr1 x) . y is Element of F₃()
(pr2 x) . y is Element of F₄()
y + 1 is ext-real positive non negative non empty V7() V8() V9() V13() V14() V15() integer V38() V43() Element of NAT
(pr1 b) . (y + 1) is Element of F₁()
(pr2 b) . (y + 1) is Element of F₂()
(pr1 x) . (y + 1) is Element of F₃()
(pr2 x) . (y + 1) is Element of F₄()
b . (y + 1) is Element of [:F₁(),F₂():]
(b . (y + 1)) `1 is set
(b . (y + 1)) `2 is set
x . (y + 1) is Element of [:F₃(),F₄():]
(x . (y + 1)) `1 is set
(x . (y + 1)) `2 is set
b . y is Element of [:F₁(),F₂():]
(b . y) `1 is set
(b . y) `2 is set
x . y is Element of [:F₃(),F₄():]
(x . y) `1 is set
(x . y) `2 is set
[:NAT,INT:] is non empty V38() set
bool [:NAT,INT:] is non empty V38() set
nlist is ext-real V14() V15() integer Element of INT
a is ext-real V14() V15() integer Element of INT
b is ext-real non negative V7() V8() V9() V13() V14() V15() integer V38() V43() Element of NAT
x is ext-real V14() V15() integer Element of INT
y is ext-real V14() V15() integer Element of INT
m is ext-real V14() V15() integer Element of INT
i is ext-real V14() V15() integer Element of INT
m div i is ext-real V14() V15() integer set
m / i is ext-real V14() V15() set
[\(m / i)/] is ext-real V14() V15() integer set
m mod i is ext-real V14() V15() integer set
m is ext-real V14() V15() integer Element of INT
I0 is ext-real V14() V15() integer Element of INT
x is ext-real V14() V15() integer Element of INT
y is V18() V21( NAT ) V22( INT ) Function-like V32( NAT , INT ) V60() V61() V62() Element of bool [:NAT,INT:]
y . 0 is ext-real V14() V15() integer Element of INT
m is V18() V21( NAT ) V22( INT ) Function-like V32( NAT , INT ) V60() V61() V62() Element of bool [:NAT,INT:]
m . 0 is ext-real V14() V15() integer Element of INT
i is V18() V21( NAT ) V22( INT ) Function-like V32( NAT , INT ) V60() V61() V62() Element of bool [:NAT,INT:]
i . 0 is ext-real V14() V15() integer Element of INT
I0 is V18() V21( NAT ) V22( INT ) Function-like V32( NAT , INT ) V60() V61() V62() Element of bool [:NAT,INT:]
I0 . 0 is ext-real V14() V15() integer Element of INT
m is ext-real non negative V7() V8() V9() V13() V14() V15() integer V38() V43() Element of NAT
m + 1 is ext-real positive non negative non empty V7() V8() V9() V13() V14() V15() integer V38() V43() Element of NAT
y . (m + 1) is ext-real V14() V15() integer Element of INT
l is ext-real V14() V15() integer Element of INT
prodc is ext-real V14() V15() integer Element of INT
prodi is ext-real V14() V15() integer Element of INT
M0 is ext-real V14() V15() integer Element of INT
(y . (m + 1)) * prodi is ext-real V14() V15() integer set
l - ((y . (m + 1)) * prodi) is ext-real V14() V15() integer set
(y . (m + 1)) * M0 is ext-real V14() V15() integer set
prodc - ((y . (m + 1)) * M0) is ext-real V14() V15() integer set
m + 1 is ext-real positive non negative non empty V7() V8() V9() V13() V14() V15() integer V38() V43() Element of NAT
y . (m + 1) is ext-real V14() V15() integer Element of INT
(y . (m + 1)) * prodi is ext-real V14() V15() integer set
l - ((y . (m + 1)) * prodi) is ext-real V14() V15() integer set
(y . (m + 1)) * M0 is ext-real V14() V15() integer set
prodc - ((y . (m + 1)) * M0) is ext-real V14() V15() integer set
m1 is ext-real V14() V15() integer Element of INT
nn1 is ext-real V14() V15() integer Element of INT
b is ext-real V14() V15() integer Element of INT
m is V18() V21( NAT ) V22( INT ) Function-like V32( NAT , INT ) V60() V61() V62() Element of bool [:NAT,INT:]
m . 0 is ext-real V14() V15() integer Element of INT
l is V18() V21( NAT ) V22( INT ) Function-like V32( NAT , INT ) V60() V61() V62() Element of bool [:NAT,INT:]
l . 0 is ext-real V14() V15() integer Element of INT
prodc is V18() V21( NAT ) V22( INT ) Function-like V32( NAT , INT ) V60() V61() V62() Element of bool [:NAT,INT:]
prodc . 0 is ext-real V14() V15() integer Element of INT
prodi is V18() V21( NAT ) V22( INT ) Function-like V32( NAT , INT ) V60() V61() V62() Element of bool [:NAT,INT:]
prodi . 0 is ext-real V14() V15() integer Element of INT
M0 is ext-real non negative V7() V8() V9() V13() V14() V15() integer V38() V43() Element of NAT
M0 + 1 is ext-real positive non negative non empty V7() V8() V9() V13() V14() V15() integer V38() V43() Element of NAT
y . (M0 + 1) is ext-real V14() V15() integer Element of INT
i . M0 is ext-real V14() V15() integer Element of INT
I0 . M0 is ext-real V14() V15() integer Element of INT
(i . M0) div (I0 . M0) is ext-real V14() V15() integer set
(i . M0) / (I0 . M0) is ext-real V14() V15() set
[\((i . M0) / (I0 . M0))/] is ext-real V14() V15() integer set
M is ext-real non negative V7() V8() V9() V13() V14() V15() integer V38() V43() Element of NAT
M + 1 is ext-real positive non negative non empty V7() V8() V9() V13() V14() V15() integer V38() V43() Element of NAT
m . (M + 1) is ext-real V14() V15() integer Element of INT
i . M is ext-real V14() V15() integer Element of INT
I0 . M is ext-real V14() V15() integer Element of INT
(i . M) mod (I0 . M) is ext-real V14() V15() integer set
lb1 is ext-real non negative V7() V8() V9() V13() V14() V15() integer V38() V43() Element of NAT
lb1 + 1 is ext-real positive non negative non empty V7() V8() V9() V13() V14() V15() integer V38() V43() Element of NAT
m . (lb1 + 1) is ext-real V14() V15() integer Element of INT
prodc . lb1 is ext-real V14() V15() integer Element of INT
l1 is ext-real non negative V7() V8() V9() V13() V14() V15() integer V38() V43() Element of NAT
l1 + 1 is ext-real positive non negative non empty V7() V8() V9() V13() V14() V15() integer V38() V43() Element of NAT
l . (l1 + 1) is ext-real V14() V15() integer Element of INT
prodi . l1 is ext-real V14() V15() integer Element of INT
m1 is ext-real non negative V7() V8() V9() V13() V14() V15() integer V38() V43() Element of NAT
m1 + 1 is ext-real positive non negative non empty V7() V8() V9() V13() V14() V15() integer V38() V43() Element of NAT
i . (m1 + 1) is ext-real V14() V15() integer Element of INT
I0 . m1 is ext-real V14() V15() integer Element of INT
nn1 is ext-real non negative V7() V8() V9() V13() V14() V15() integer V38() V43() Element of NAT
nn1 + 1 is ext-real positive non negative non empty V7() V8() V9() V13() V14() V15() integer V38() V43() Element of NAT
prodc . (nn1 + 1) is ext-real V14() V15() integer Element of INT
m . nn1 is ext-real V14() V15() integer Element of INT
y . (nn1 + 1) is ext-real V14() V15() integer Element of INT
prodc . nn1 is ext-real V14() V15() integer Element of INT
(y . (nn1 + 1)) * (prodc . nn1) is ext-real V14() V15() integer set
(m . nn1) - ((y . (nn1 + 1)) * (prodc . nn1)) is ext-real V14() V15() integer set
prodi1 is ext-real non negative V7() V8() V9() V13() V14() V15() integer V38() V43() Element of NAT
prodi1 + 1 is ext-real positive non negative non empty V7() V8() V9() V13() V14() V15() integer V38() V43() Element of NAT
prodi . (prodi1 + 1) is ext-real V14() V15() integer Element of INT
l . prodi1 is ext-real V14() V15() integer Element of INT
y . (prodi1 + 1) is ext-real V14() V15() integer Element of INT
prodi . prodi1 is ext-real V14() V15() integer Element of INT
(y . (prodi1 + 1)) * (prodi . prodi1) is ext-real V14() V15() integer set
(l . prodi1) - ((y . (prodi1 + 1)) * (prodi . prodi1)) is ext-real V14() V15() integer set
prodc1 is ext-real non negative V7() V8() V9() V13() V14() V15() integer V38() V43() Element of NAT
prodc1 + 1 is ext-real positive non negative non empty V7() V8() V9() V13() V14() V15() integer V38() V43() Element of NAT
I0 . (prodc1 + 1) is ext-real V14() V15() integer Element of INT
m . (prodc1 + 1) is ext-real V14() V15() integer Element of INT
nlist is ext-real V14() V15() integer Element of INT
a is ext-real V14() V15() integer Element of INT
i is V18() V21( NAT ) V22( INT ) Function-like V32( NAT , INT ) V60() V61() V62() Element of bool [:NAT,INT:]
i . 0 is ext-real V14() V15() integer Element of INT
I0 is V18() V21( NAT ) V22( INT ) Function-like V32( NAT , INT ) V60() V61() V62() Element of bool [:NAT,INT:]
I0 . 0 is ext-real V14() V15() integer Element of INT
b is V18() V21( NAT ) V22( INT ) Function-like V32( NAT , INT ) V60() V61() V62() Element of bool [:NAT,INT:]
b . 0 is ext-real V14() V15() integer Element of INT
y is V18() V21( NAT ) V22( INT ) Function-like V32( NAT , INT ) V60() V61() V62() Element of bool [:NAT,INT:]
y . 0 is ext-real V14() V15() integer Element of INT
l is V18() V21( NAT ) V22( INT ) Function-like V32( NAT , INT ) V60() V61() V62() Element of bool [:NAT,INT:]
l . 0 is ext-real V14() V15() integer Element of INT
m is V18() V21( NAT ) V22( INT ) Function-like V32( NAT , INT ) V60() V61() V62() Element of bool [:NAT,INT:]
m . 0 is ext-real V14() V15() integer Element of INT
x is V18() V21( NAT ) V22( INT ) Function-like V32( NAT , INT ) V60() V61() V62() Element of bool [:NAT,INT:]
x . 0 is ext-real V14() V15() integer Element of INT
m is V18() V21( NAT ) V22( INT ) Function-like V32( NAT , INT ) V60() V61() V62() Element of bool [:NAT,INT:]
m . 0 is ext-real V14() V15() integer Element of INT
lb1 is V18() V21( NAT ) V22( INT ) Function-like V32( NAT , INT ) V60() V61() V62() Element of bool [:NAT,INT:]
lb1 . 0 is ext-real V14() V15() integer Element of INT
l1 is V18() V21( NAT ) V22( INT ) Function-like V32( NAT , INT ) V60() V61() V62() Element of bool [:NAT,INT:]
l1 . 0 is ext-real V14() V15() integer Element of INT
prodc is V18() V21( NAT ) V22( INT ) Function-like V32( NAT , INT ) V60() V61() V62() Element of bool [:NAT,INT:]
prodc . 0 is ext-real V14() V15() integer Element of INT
M0 is V18() V21( NAT ) V22( INT ) Function-like V32( NAT , INT ) V60() V61() V62() Element of bool [:NAT,INT:]
M0 . 0 is ext-real V14() V15() integer Element of INT
nn1 is V18() V21( NAT ) V22( INT ) Function-like V32( NAT , INT ) V60() V61() V62() Element of bool [:NAT,INT:]
nn1 . 0 is ext-real V14() V15() integer Element of INT
m1 is V18() V21( NAT ) V22( INT ) Function-like V32( NAT , INT ) V60() V61() V62() Element of bool [:NAT,INT:]
m1 . 0 is ext-real V14() V15() integer Element of INT
prodi is V18() V21( NAT ) V22( INT ) Function-like V32( NAT , INT ) V60() V61() V62() Element of bool [:NAT,INT:]
prodi . 0 is ext-real V14() V15() integer Element of INT
M is V18() V21( NAT ) V22( INT ) Function-like V32( NAT , INT ) V60() V61() V62() Element of bool [:NAT,INT:]
M . 0 is ext-real V14() V15() integer Element of INT
prodi1 is ext-real non negative V7() V8() V9() V13() V14() V15() integer V38() V43() Element of NAT
b . prodi1 is ext-real V14() V15() integer Element of INT
prodc . prodi1 is ext-real V14() V15() integer Element of INT
x . prodi1 is ext-real V14() V15() integer Element of INT
prodi . prodi1 is ext-real V14() V15() integer Element of INT
y . prodi1 is ext-real V14() V15() integer Element of INT
M0 . prodi1 is ext-real V14() V15() integer Element of INT
m . prodi1 is ext-real V14() V15() integer Element of INT
M . prodi1 is ext-real V14() V15() integer Element of INT
i . prodi1 is ext-real V14() V15() integer Element of INT
lb1 . prodi1 is ext-real V14() V15() integer Element of INT
I0 . prodi1 is ext-real V14() V15() integer Element of INT
l1 . prodi1 is ext-real V14() V15() integer Element of INT
m . prodi1 is ext-real V14() V15() integer Element of INT
m1 . prodi1 is ext-real V14() V15() integer Element of INT
l . prodi1 is ext-real V14() V15() integer Element of INT
nn1 . prodi1 is ext-real V14() V15() integer Element of INT
prodi1 + 1 is ext-real positive non negative non empty V7() V8() V9() V13() V14() V15() integer V38() V43() Element of NAT
b . (prodi1 + 1) is ext-real V14() V15() integer Element of INT
prodc . (prodi1 + 1) is ext-real V14() V15() integer Element of INT
x . (prodi1 + 1) is ext-real V14() V15() integer Element of INT
prodi . (prodi1 + 1) is ext-real V14() V15() integer Element of INT
y . (prodi1 + 1) is ext-real V14() V15() integer Element of INT
M0 . (prodi1 + 1) is ext-real V14() V15() integer Element of INT
m . (prodi1 + 1) is ext-real V14() V15() integer Element of INT
M . (prodi1 + 1) is ext-real V14() V15() integer Element of INT
i . (prodi1 + 1) is ext-real V14() V15() integer Element of INT
lb1 . (prodi1 + 1) is ext-real V14() V15() integer Element of INT
I0 . (prodi1 + 1) is ext-real V14() V15() integer Element of INT
l1 . (prodi1 + 1) is ext-real V14() V15() integer Element of INT
m . (prodi1 + 1) is ext-real V14() V15() integer Element of INT
m1 . (prodi1 + 1) is ext-real V14() V15() integer Element of INT
l . (prodi1 + 1) is ext-real V14() V15() integer Element of INT
nn1 . (prodi1 + 1) is ext-real V14() V15() integer Element of INT
(prodc . prodi1) div (prodi . prodi1) is ext-real V14() V15() integer set
(prodc . prodi1) / (prodi . prodi1) is ext-real V14() V15() set
[\((prodc . prodi1) / (prodi . prodi1))/] is ext-real V14() V15() integer set
(prodc . prodi1) mod (prodi . prodi1) is ext-real V14() V15() integer set
(y . (prodi1 + 1)) * (nn1 . prodi1) is ext-real V14() V15() integer set
(lb1 . prodi1) - ((y . (prodi1 + 1)) * (nn1 . prodi1)) is ext-real V14() V15() integer set
(y . (prodi1 + 1)) * (m1 . prodi1) is ext-real V14() V15() integer set
(l1 . prodi1) - ((y . (prodi1 + 1)) * (m1 . prodi1)) is ext-real V14() V15() integer set
[:INT,INT,INT:] is non empty set
nlist is ext-real V14() V15() integer Element of INT
a is ext-real V14() V15() integer Element of INT
i is V18() V21( NAT ) V22( INT ) Function-like V32( NAT , INT ) V60() V61() V62() Element of bool [:NAT,INT:]
i . 0 is ext-real V14() V15() integer Element of INT
I0 is V18() V21( NAT ) V22( INT ) Function-like V32( NAT , INT ) V60() V61() V62() Element of bool [:NAT,INT:]
I0 . 0 is ext-real V14() V15() integer Element of INT
b is V18() V21( NAT ) V22( INT ) Function-like V32( NAT , INT ) V60() V61() V62() Element of bool [:NAT,INT:]
b . 0 is ext-real V14() V15() integer Element of INT
y is V18() V21( NAT ) V22( INT ) Function-like V32( NAT , INT ) V60() V61() V62() Element of bool [:NAT,INT:]
y . 0 is ext-real V14() V15() integer Element of INT
l is V18() V21( NAT ) V22( INT ) Function-like V32( NAT , INT ) V60() V61() V62() Element of bool [:NAT,INT:]
l . 0 is ext-real V14() V15() integer Element of INT
m is V18() V21( NAT ) V22( INT ) Function-like V32( NAT , INT ) V60() V61() V62() Element of bool [:NAT,INT:]
m . 0 is ext-real V14() V15() integer Element of INT
x is V18() V21( NAT ) V22( INT ) Function-like V32( NAT , INT ) V60() V61() V62() Element of bool [:NAT,INT:]
x . 0 is ext-real V14() V15() integer Element of INT
m is V18() V21( NAT ) V22( INT ) Function-like V32( NAT , INT ) V60() V61() V62() Element of bool [:NAT,INT:]
m . 0 is ext-real V14() V15() integer Element of INT
{ b₁ where b₁ is ext-real non negative V7() V8() V9() V13() V14() V15() integer V38() V43() Element of NAT : x . b₁ = 0 } is set
min* { b₁ where b₁ is ext-real non negative V7() V8() V9() V13() V14() V15() integer V38() V43() Element of NAT : x . b₁ = 0 } is ext-real non negative V7() V8() V9() V13() V14() V15() integer V38() V43() Element of NAT
b . (min* { b₁ where b₁ is ext-real non negative V7() V8() V9() V13() V14() V15() integer V38() V43() Element of NAT : x . b₁ = 0 } ) is ext-real V14() V15() integer Element of INT
i . (min* { b₁ where b₁ is ext-real non negative V7() V8() V9() V13() V14() V15() integer V38() V43() Element of NAT : x . b₁ = 0 } ) is ext-real V14() V15() integer Element of INT
I0 . (min* { b₁ where b₁ is ext-real non negative V7() V8() V9() V13() V14() V15() integer V38() V43() Element of NAT : x . b₁ = 0 } ) is ext-real V14() V15() integer Element of INT
[(i . (min* { b₁ where b₁ is ext-real non negative V7() V8() V9() V13() V14() V15() integer V38() V43() Element of NAT : x . b₁ = 0 } )),(I0 . (min* { b₁ where b₁ is ext-real non negative V7() V8() V9() V13() V14() V15() integer V38() V43() Element of NAT : x . b₁ = 0 } )),(b . (min* { b₁ where b₁ is ext-real non negative V7() V8() V9() V13() V14() V15() integer V38() V43() Element of NAT : x . b₁ = 0 } ))] is V29() V30() set
[(i . (min* { b₁ where b₁ is ext-real non negative V7() V8() V9() V13() V14() V15() integer V38() V43() Element of NAT : x . b₁ = 0 } )),(I0 . (min* { b₁ where b₁ is ext-real non negative V7() V8() V9() V13() V14() V15() integer V38() V43() Element of NAT : x . b₁ = 0 } ))] is V29() set
[[(i . (min* { b₁ where b₁ is ext-real non negative V7() V8() V9() V13() V14() V15() integer V38() V43() Element of NAT : x . b₁ = 0 } )),(I0 . (min* { b₁ where b₁ is ext-real non negative V7() V8() V9() V13() V14() V15() integer V38() V43() Element of NAT : x . b₁ = 0 } ))],(b . (min* { b₁ where b₁ is ext-real non negative V7() V8() V9() V13() V14() V15() integer V38() V43() Element of NAT : x . b₁ = 0 } ))] is V29() set
- (i . (min* { b₁ where b₁ is ext-real non negative V7() V8() V9() V13() V14() V15() integer V38() V43() Element of NAT : x . b₁ = 0 } )) is ext-real V14() V15() integer set
- (I0 . (min* { b₁ where b₁ is ext-real non negative V7() V8() V9() V13() V14() V15() integer V38() V43() Element of NAT : x . b₁ = 0 } )) is ext-real V14() V15() integer set
- (b . (min* { b₁ where b₁ is ext-real non negative V7() V8() V9() V13() V14() V15() integer V38() V43() Element of NAT : x . b₁ = 0 } )) is ext-real V14() V15() integer set
[(- (i . (min* { b₁ where b₁ is ext-real non negative V7() V8() V9() V13() V14() V15() integer V38() V43() Element of NAT : x . b₁ = 0 } ))),(- (I0 . (min* { b₁ where b₁ is ext-real non negative V7() V8() V9() V13() V14() V15() integer V38() V43() Element of NAT : x . b₁ = 0 } ))),(- (b . (min* { b₁ where b₁ is ext-real non negative V7() V8() V9() V13() V14() V15() integer V38() V43() Element of NAT : x . b₁ = 0 } )))] is V29() V30() set
[(- (i . (min* { b₁ where b₁ is ext-real non negative V7() V8() V9() V13() V14() V15() integer V38() V43() Element of NAT : x . b₁ = 0 } ))),(- (I0 . (min* { b₁ where b₁ is ext-real non negative V7() V8() V9() V13() V14() V15() integer V38() V43() Element of NAT : x . b₁ = 0 } )))] is V29() set
[[(- (i . (min* { b₁ where b₁ is ext-real non negative V7() V8() V9() V13() V14() V15() integer V38() V43() Element of NAT : x . b₁ = 0 } ))),(- (I0 . (min* { b₁ where b₁ is ext-real non negative V7() V8() V9() V13() V14() V15() integer V38() V43() Element of NAT : x . b₁ = 0 } )))],(- (b . (min* { b₁ where b₁ is ext-real non negative V7() V8() V9() V13() V14() V15() integer V38() V43() Element of NAT : x . b₁ = 0 } )))] is V29() set
b . (min* { b₁ where b₁ is ext-real non negative V7() V8() V9() V13() V14() V15() integer V38() V43() Element of NAT : x . b₁ = 0 } ) is ext-real V14() V15() integer Element of INT
- (b . (min* { b₁ where b₁ is ext-real non negative V7() V8() V9() V13() V14() V15() integer V38() V43() Element of NAT : x . b₁ = 0 } )) is ext-real V14() V15() integer set
i . (min* { b₁ where b₁ is ext-real non negative V7() V8() V9() V13() V14() V15() integer V38() V43() Element of NAT : x . b₁ = 0 } ) is ext-real V14() V15() integer Element of INT
- (i . (min* { b₁ where b₁ is ext-real non negative V7() V8() V9() V13() V14() V15() integer V38() V43() Element of NAT : x . b₁ = 0 } )) is ext-real V14() V15() integer set
I0 . (min* { b₁ where b₁ is ext-real non negative V7() V8() V9() V13() V14() V15() integer V38() V43() Element of NAT : x . b₁ = 0 } ) is ext-real V14() V15() integer Element of INT
- (I0 . (min* { b₁ where b₁ is ext-real non negative V7() V8() V9() V13() V14() V15() integer V38() V43() Element of NAT : x . b₁ = 0 } )) is ext-real V14() V15() integer set
[(- (i . (min* { b₁ where b₁ is ext-real non negative V7() V8() V9() V13() V14() V15() integer V38() V43() Element of NAT : x . b₁ = 0 } ))),(- (I0 . (min* { b₁ where b₁ is ext-real non negative V7() V8() V9() V13() V14() V15() integer V38() V43() Element of NAT : x . b₁ = 0 } ))),(- (b . (min* { b₁ where b₁ is ext-real non negative V7() V8() V9() V13() V14() V15() integer V38() V43() Element of NAT : x . b₁ = 0 } )))] is V29() V30() set
[(- (i . (min* { b₁ where b₁ is ext-real non negative V7() V8() V9() V13() V14() V15() integer V38() V43() Element of NAT : x . b₁ = 0 } ))),(- (I0 . (min* { b₁ where b₁ is ext-real non negative V7() V8() V9() V13() V14() V15() integer V38() V43() Element of NAT : x . b₁ = 0 } )))] is V29() set
[[(- (i . (min* { b₁ where b₁ is ext-real non negative V7() V8() V9() V13() V14() V15() integer V38() V43() Element of NAT : x . b₁ = 0 } ))),(- (I0 . (min* { b₁ where b₁ is ext-real non negative V7() V8() V9() V13() V14() V15() integer V38() V43() Element of NAT : x . b₁ = 0 } )))],(- (b . (min* { b₁ where b₁ is ext-real non negative V7() V8() V9() V13() V14() V15() integer V38() V43() Element of NAT : x . b₁ = 0 } )))] is V29() set
[(i . (min* { b₁ where b₁ is ext-real non negative V7() V8() V9() V13() V14() V15() integer V38() V43() Element of NAT : x . b₁ = 0 } )),(I0 . (min* { b₁ where b₁ is ext-real non negative V7() V8() V9() V13() V14() V15() integer V38() V43() Element of NAT : x . b₁ = 0 } )),(b . (min* { b₁ where b₁ is ext-real non negative V7() V8() V9() V13() V14() V15() integer V38() V43() Element of NAT : x . b₁ = 0 } ))] is V29() V30() set
[(i . (min* { b₁ where b₁ is ext-real non negative V7() V8() V9() V13() V14() V15() integer V38() V43() Element of NAT : x . b₁ = 0 } )),(I0 . (min* { b₁ where b₁ is ext-real non negative V7() V8() V9() V13() V14() V15() integer V38() V43() Element of NAT : x . b₁ = 0 } ))] is V29() set
[[(i . (min* { b₁ where b₁ is ext-real non negative V7() V8() V9() V13() V14() V15() integer V38() V43() Element of NAT : x . b₁ = 0 } )),(I0 . (min* { b₁ where b₁ is ext-real non negative V7() V8() V9() V13() V14() V15() integer V38() V43() Element of NAT : x . b₁ = 0 } ))],(b . (min* { b₁ where b₁ is ext-real non negative V7() V8() V9() V13() V14() V15() integer V38() V43() Element of NAT : x . b₁ = 0 } ))] is V29() set
b . (min* { b₁ where b₁ is ext-real non negative V7() V8() V9() V13() V14() V15() integer V38() V43() Element of NAT : x . b₁ = 0 } ) is ext-real V14() V15() integer Element of INT
i . (min* { b₁ where b₁ is ext-real non negative V7() V8() V9() V13() V14() V15() integer V38() V43() Element of NAT : x . b₁ = 0 } ) is ext-real V14() V15() integer Element of INT
I0 . (min* { b₁ where b₁ is ext-real non negative V7() V8() V9() V13() V14() V15() integer V38() V43() Element of NAT : x . b₁ = 0 } ) is ext-real V14() V15() integer Element of INT
[(i . (min* { b₁ where b₁ is ext-real non negative V7() V8() V9() V13() V14() V15() integer V38() V43() Element of NAT : x . b₁ = 0 } )),(I0 . (min* { b₁ where b₁ is ext-real non negative V7() V8() V9() V13() V14() V15() integer V38() V43() Element of NAT : x . b₁ = 0 } )),(b . (min* { b₁ where b₁ is ext-real non negative V7() V8() V9() V13() V14() V15() integer V38() V43() Element of NAT : x . b₁ = 0 } ))] is V29() V30() set
[(i . (min* { b₁ where b₁ is ext-real non negative V7() V8() V9() V13() V14() V15() integer V38() V43() Element of NAT : x . b₁ = 0 } )),(I0 . (min* { b₁ where b₁ is ext-real non negative V7() V8() V9() V13() V14() V15() integer V38() V43() Element of NAT : x . b₁ = 0 } ))] is V29() set
[[(i . (min* { b₁ where b₁ is ext-real non negative V7() V8() V9() V13() V14() V15() integer V38() V43() Element of NAT : x . b₁ = 0 } )),(I0 . (min* { b₁ where b₁ is ext-real non negative V7() V8() V9() V13() V14() V15() integer V38() V43() Element of NAT : x . b₁ = 0 } ))],(b . (min* { b₁ where b₁ is ext-real non negative V7() V8() V9() V13() V14() V15() integer V38() V43() Element of NAT : x . b₁ = 0 } ))] is V29() set
- (i . (min* { b₁ where b₁ is ext-real non negative V7() V8() V9() V13() V14() V15() integer V38() V43() Element of NAT : x . b₁ = 0 } )) is ext-real V14() V15() integer set
- (I0 . (min* { b₁ where b₁ is ext-real non negative V7() V8() V9() V13() V14() V15() integer V38() V43() Element of NAT : x . b₁ = 0 } )) is ext-real V14() V15() integer set
- (b . (min* { b₁ where b₁ is ext-real non negative V7() V8() V9() V13() V14() V15() integer V38() V43() Element of NAT : x . b₁ = 0 } )) is ext-real V14() V15() integer set
[(- (i . (min* { b₁ where b₁ is ext-real non negative V7() V8() V9() V13() V14() V15() integer V38() V43() Element of NAT : x . b₁ = 0 } ))),(- (I0 . (min* { b₁ where b₁ is ext-real non negative V7() V8() V9() V13() V14() V15() integer V38() V43() Element of NAT : x . b₁ = 0 } ))),(- (b . (min* { b₁ where b₁ is ext-real non negative V7() V8() V9() V13() V14() V15() integer V38() V43() Element of NAT : x . b₁ = 0 } )))] is V29() V30() set
[(- (i . (min* { b₁ where b₁ is ext-real non negative V7() V8() V9() V13() V14() V15() integer V38() V43() Element of NAT : x . b₁ = 0 } ))),(- (I0 . (min* { b₁ where b₁ is ext-real non negative V7() V8() V9() V13() V14() V15() integer