:: 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 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 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
prodi is Element of [:INT,INT,INT:]
prodi is Element of [:INT,INT,INT:]
b is Element of [:INT,INT,INT:]
x is Element of [:INT,INT,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
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
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
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
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
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
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
M0 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 . M0 is ext-real V14() V15() integer Element of INT
m . M0 is ext-real V14() V15() integer Element of INT
l . M0 is ext-real V14() V15() integer Element of INT
[(m . M0),(l . M0),(y . M0)] is V29() V30() set
[(m . M0),(l . M0)] is V29() set
[[(m . M0),(l . M0)],(y . M0)] is V29() set
- (m . M0) is ext-real V14() V15() integer set
- (l . M0) is ext-real V14() V15() integer set
- (y . M0) is ext-real V14() V15() integer set
[(- (m . M0)),(- (l . M0)),(- (y . M0))] is V29() V30() set
[(- (m . M0)),(- (l . M0))] is V29() set
[[(- (m . M0)),(- (l . M0))],(- (y . M0))] is V29() set
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
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
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
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
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
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
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
M0 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 . M0 is ext-real V14() V15() integer Element of INT
m . M0 is ext-real V14() V15() integer Element of INT
l . M0 is ext-real V14() V15() integer Element of INT
[(m . M0),(l . M0),(y . M0)] is V29() V30() set
[(m . M0),(l . M0)] is V29() set
[[(m . M0),(l . M0)],(y . M0)] is V29() set
- (m . M0) is ext-real V14() V15() integer set
- (l . M0) is ext-real V14() V15() integer set
- (y . M0) is ext-real V14() V15() integer set
[(- (m . M0)),(- (l . M0)),(- (y . M0))] is V29() V30() set
[(- (m . M0)),(- (l . M0))] is V29() set
[[(- (m . M0)),(- (l . M0))],(- (y . M0))] is V29() set
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
prodi1 is V18() V21( NAT ) V22( INT ) Function-like V32( NAT , INT ) V60() V61() V62() Element of bool [:NAT,INT:]
prodi1 . 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
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
M01 is V18() V21( NAT ) V22( INT ) Function-like V32( NAT , INT ) V60() V61() V62() Element of bool [:NAT,INT:]
M01 . 0 is ext-real V14() V15() integer Element of INT
prodc1 is V18() V21( NAT ) V22( INT ) Function-like V32( NAT , INT ) V60() V61() V62() Element of bool [:NAT,INT:]
prodc1 . 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
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
M1 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 : lb1 . 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 : lb1 . b₁ = 0 } is ext-real non negative V7() V8() V9() V13() V14() V15() integer V38() V43() Element of NAT
M . M1 is ext-real V14() V15() integer Element of INT
nn1 . M1 is ext-real V14() V15() integer Element of INT
prodi1 . M1 is ext-real V14() V15() integer Element of INT
[(nn1 . M1),(prodi1 . M1),(M . M1)] is V29() V30() set
[(nn1 . M1),(prodi1 . M1)] is V29() set
[[(nn1 . M1),(prodi1 . M1)],(M . M1)] is V29() set
- (nn1 . M1) is ext-real V14() V15() integer set
- (prodi1 . M1) is ext-real V14() V15() integer set
- (M . M1) is ext-real V14() V15() integer set
[(- (nn1 . M1)),(- (prodi1 . M1)),(- (M . M1))] is V29() V30() set
[(- (nn1 . M1)),(- (prodi1 . M1))] is V29() set
[[(- (nn1 . M1)),(- (prodi1 . M1))],(- (M . M1))] is V29() set
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
prodi1 is V18() V21( NAT ) V22( INT ) Function-like V32( NAT , INT ) V60() V61() V62() Element of bool [:NAT,INT:]
prodi1 . 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
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
M01 is V18() V21( NAT ) V22( INT ) Function-like V32( NAT , INT ) V60() V61() V62() Element of bool [:NAT,INT:]
M01 . 0 is ext-real V14() V15() integer Element of INT
prodc1 is V18() V21( NAT ) V22( INT ) Function-like V32( NAT , INT ) V60() V61() V62() Element of bool [:NAT,INT:]
prodc1 . 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
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
M1 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 : lb1 . 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 : lb1 . b₁ = 0 } is ext-real non negative V7() V8() V9() V13() V14() V15() integer V38() V43() Element of NAT
M . M1 is ext-real V14() V15() integer Element of INT
nn1 . M1 is ext-real V14() V15() integer Element of INT
prodi1 . M1 is ext-real V14() V15() integer Element of INT
[(nn1 . M1),(prodi1 . M1),(M . M1)] is V29() V30() set
[(nn1 . M1),(prodi1 . M1)] is V29() set
[[(nn1 . M1),(prodi1 . M1)],(M . M1)] is V29() set
- (nn1 . M1) is ext-real V14() V15() integer set
- (prodi1 . M1) is ext-real V14() V15() integer set
- (M . M1) is ext-real V14() V15() integer set
[(- (nn1 . M1)),(- (prodi1 . M1)),(- (M . M1))] is V29() V30() set
[(- (nn1 . M1)),(- (prodi1 . M1))] is V29() set
[[(- (nn1 . M1)),(- (prodi1 . M1))],(- (M . M1))] is V29() set
nlist is ext-real V14() V15() integer Element of INT
a 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
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
y is ext-real non negative V7() V8() V9() V13() V14() V15() integer V38() V43() Element of NAT
x . y is ext-real V14() V15() integer Element of INT
b . y is ext-real V14() V15() integer Element of INT
(b . y) gcd (x . y) is ext-real non negative V7() V8() V9() V13() V14() V15() integer V38() V43() set
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 V14() V15() integer Element of INT
x . (y + 1) is ext-real V14() V15() integer Element of INT
(b . (y + 1)) gcd (x . (y + 1)) is ext-real non negative V7() V8() V9() V13() V14() V15() integer V38() V43() set
(b . y) mod (x . y) is ext-real V14() V15() integer set
(b . y) div (x . y) is ext-real V14() V15() integer set
(b . y) / (x . y) is ext-real V14() V15() set
[\((b . y) / (x . y))/] is ext-real V14() V15() integer set
((b . y) div (x . y)) * (x . y) is ext-real V14() V15() integer set
(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 V14() V15() integer set
(b . y) / (x . y) is ext-real V14() V15() set
[\((b . y) / (x . y))/] is ext-real V14() V15() integer set
((b . y) div (x . y)) * (x . y) is ext-real V14() V15() integer set
(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 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
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
a 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
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
(b . 0) gcd (x . 0) is ext-real non negative V7() V8() V9() V13() V14() V15() integer V38() V43() set
y is ext-real non negative V7() V8() V9() V13() V14() V15() integer V38() V43() Element of NAT
x . y is ext-real V14() V15() integer Element of INT
b . y is ext-real V14() V15() integer Element of INT
(b . y) gcd (x . y) is ext-real non negative V7() V8() V9() V13() V14() V15() integer V38() V43() 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 V14() V15() integer Element of INT
b . (y + 1) is ext-real V14() V15() integer Element of INT
(b . (y + 1)) gcd (x . (y + 1)) is ext-real non negative V7() V8() V9() V13() V14() V15() integer V38() V43() set
(b . y) mod (x . y) 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 V14() V15() integer Element of INT
b . y is ext-real V14() V15() integer Element of INT
(b . y) gcd (x . y) is ext-real non negative V7() V8() V9() V13() V14() V15() integer V38() V43() set
nlist is ext-real V14() V15() integer set
a is ext-real V14() V15() integer set
a mod nlist is ext-real V14() V15() integer set
a / nlist is ext-real V14() V15() set
[\(a / nlist)/] is ext-real V14() V15() integer set
(a / nlist) * nlist is ext-real V14() V15() set
a div nlist is ext-real V14() V15() integer set
(a div nlist) * nlist is ext-real V14() V15() integer set
a - ((a div nlist) * nlist) is ext-real V14() V15() integer set
nlist is ext-real V14() V15() integer set
- nlist is ext-real V14() V15() integer set
a is ext-real V14() V15() integer set
a mod nlist is ext-real V14() V15() integer set
- (a mod nlist) is ext-real V14() V15() integer set
a / nlist is ext-real V14() V15() set
[\(a / nlist)/] is ext-real V14() V15() integer set
(a / nlist) - 1 is ext-real V14() V15() set
((a / nlist) - 1) * nlist is ext-real V14() V15() set
a div nlist is ext-real V14() V15() integer set
(a div nlist) * nlist is ext-real V14() V15() integer set
(a / nlist) * nlist is ext-real V14() V15() set
1 * nlist is ext-real V14() V15() integer set
((a / nlist) * nlist) - (1 * nlist) is ext-real V14() V15() set
a - nlist is ext-real V14() V15() integer set
(a - nlist) - a is ext-real V14() V15() integer set
((a div nlist) * nlist) - a is ext-real V14() V15() integer set
a - ((a div nlist) * nlist) is ext-real V14() V15() integer set
- (a - ((a div nlist) * nlist)) is ext-real V14() V15() integer set
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
nlist is ext-real V14() V15() integer Element of INT
nlist mod a is ext-real V14() V15() integer set
abs (nlist mod a) is ext-real non negative V7() V8() V9() V13() V14() V15() integer V38() V43() Element of NAT
- a is ext-real V14() V15() integer set
- (nlist mod a) is ext-real V14() V15() integer set
nlist is ext-real V14() V15() integer Element of INT
a 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
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
{ 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 V14() V15() integer Element of INT
y is ext-real non negative V7() V8() V9() V13() V14() V15() integer V38() V43() Element of NAT
x . y is ext-real V14() V15() integer Element of INT
abs (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
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 V14() V15() integer Element of INT
abs (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 V14() V15() integer Element of INT
abs (x . y) is ext-real non negative V7() V8() V9() V13() V14() V15() integer V38() V43() Element of NAT
(abs (x . y)) - 1 is ext-real V14() V15() integer set
b . y is ext-real V14() V15() integer Element of INT
(b . y) mod (x . y) is ext-real V14() V15() integer set
abs ((b . y) mod (x . y)) is ext-real non negative V7() V8() V9() V13() V14() V15() integer V38() V43() Element of NAT
(abs (x . (y + 1))) + 1 is ext-real positive non negative non empty V7() V8() V9() V13() V14() V15() integer V38() V43() Element of NAT
((abs (x . (y + 1))) + 1) - 1 is ext-real V14() V15() integer set
abs (x . 0) is ext-real non negative V7() V8() V9() V13() V14() V15() integer V38() V43() Element of NAT
(abs (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 V14() V15() integer Element of INT
abs (x . y) is ext-real non negative V7() V8() V9() V13() V14() V15() integer V38() V43() Element of NAT
(abs (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 V14() V15() integer Element of INT
abs (x . (y + 1)) is ext-real non negative V7() V8() V9() V13() V14() V15() integer V38() V43() Element of NAT
(abs (x . 0)) - (y + 1) is ext-real V14() V15() integer set
(abs (x . y)) - 1 is ext-real V14() V15() integer set
((abs (x . 0)) - y) - 1 is ext-real V14() V15() integer set
x . (abs (x . 0)) is ext-real V14() V15() integer Element of INT
abs (x . (abs (x . 0))) is ext-real non negative V7() V8() V9() V13() V14() V15() integer V38() V43() Element of NAT
(abs (x . 0)) - (abs (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 V14() V15() integer Element of INT
y is ext-real non negative V7() V8() V9() V13() V14() V15() integer V38() V43() Element of NAT
x . y is ext-real V14() V15() integer Element of INT
nlist is ext-real V14() V15() integer Element of INT
nlist gcd 0 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
nlist is ext-real V14() V15() integer Element of INT
a 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
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
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
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
(i . 0) * nlist is ext-real V14() V15() integer set
(I0 . 0) * a is ext-real V14() V15() integer set
((i . 0) * nlist) + ((I0 . 0) * a) is ext-real V14() V15() integer set
0 + 1 is ext-real positive non negative non empty V7() V8() V9() V13() V14() V15() integer V38() V43() Element of NAT
i . (0 + 1) is ext-real V14() V15() integer Element of INT
(i . (0 + 1)) * nlist is ext-real V14() V15() integer set
I0 . (0 + 1) is ext-real V14() V15() integer Element of INT
(I0 . (0 + 1)) * a is ext-real V14() V15() integer set
((i . (0 + 1)) * nlist) + ((I0 . (0 + 1)) * a) is ext-real V14() V15() integer set
b . (0 + 1) is ext-real V14() V15() integer Element of INT
prodc is ext-real non negative V7() V8() V9() V13() V14() V15() integer V38() V43() Element of NAT
prodc + 1 is ext-real positive non negative non empty V7() V8() V9() V13() V14() V15() integer V38() V43() Element of NAT
i . (prodc + 1) is ext-real V14() V15() integer Element of INT
(i . (prodc + 1)) * nlist is ext-real V14() V15() integer set
I0 . (prodc + 1) is ext-real V14() V15() integer Element of INT
(I0 . (prodc + 1)) * a is ext-real V14() V15() integer set
((i . (prodc + 1)) * nlist) + ((I0 . (prodc + 1)) * a) is ext-real V14() V15() integer set
(l . 0) * nlist is ext-real V14() V15() integer set
((l . 0) * nlist) + ((I0 . (prodc + 1)) * a) is ext-real V14() V15() integer set
0 * nlist is ext-real V14() V15() integer set
1 * a is ext-real V14() V15() integer set
(0 * nlist) + (1 * a) is ext-real V14() V15() integer set
b . (prodc + 1) is ext-real V14() V15() integer Element of INT
prodc is ext-real non negative V7() V8() V9() V13() V14() V15() integer V38() V43() Element of NAT
x . prodc is ext-real V14() V15() integer Element of INT
i . prodc is ext-real V14() V15() integer Element of INT
(i . prodc) * nlist is ext-real V14() V15() integer set
I0 . prodc is ext-real V14() V15() integer Element of INT
(I0 . prodc) * a is ext-real V14() V15() integer set
((i . prodc) * nlist) + ((I0 . prodc) * a) is ext-real V14() V15() integer set
b . prodc is ext-real V14() V15() integer Element of INT
prodc + 1 is ext-real positive non negative non empty V7() V8() V9() V13() V14() V15() integer V38() V43() Element of NAT
i . (prodc + 1) is ext-real V14() V15() integer Element of INT
(i . (prodc + 1)) * nlist is ext-real V14() V15() integer set
I0 . (prodc + 1) is ext-real V14() V15() integer Element of INT
(I0 . (prodc + 1)) * a is ext-real V14() V15() integer set
((i . (prodc + 1)) * nlist) + ((I0 . (prodc + 1)) * a) is ext-real V14() V15() integer set
b . (prodc + 1) is ext-real V14() V15() integer Element of INT
prodc + 1 is ext-real positive non negative non empty V7() V8() V9() V13() V14() V15() integer V38() V43() Element of NAT
x . (prodc + 1) is ext-real V14() V15() integer Element of INT
i . (prodc + 1) is ext-real V14() V15() integer Element of INT
(i . (prodc + 1)) * nlist is ext-real V14() V15() integer set
I0 . (prodc + 1) is ext-real V14() V15() integer Element of INT
(I0 . (prodc + 1)) * a is ext-real V14() V15() integer set
((i . (prodc + 1)) * nlist) + ((I0 . (prodc + 1)) * a) is ext-real V14() V15() integer set
b . (prodc + 1) is ext-real V14() V15() integer Element of INT
(prodc + 1) + 1 is ext-real positive non negative non empty V7() V8() V9() V13() V14() V15() integer V38() V43() Element of NAT
i . ((prodc + 1) + 1) is ext-real V14() V15() integer Element of INT
(i . ((prodc + 1) + 1)) * nlist is ext-real V14() V15() integer set
I0 . ((prodc + 1) + 1) is ext-real V14() V15() integer Element of INT
(I0 . ((prodc + 1) + 1)) * a is ext-real V14() V15() integer set
((i . ((prodc + 1) + 1)) * nlist) + ((I0 . ((prodc + 1) + 1)) * a) is ext-real V14() V15() integer set
b . ((prodc + 1) + 1) is ext-real V14() V15() integer Element of INT
m . (prodc + 1) is ext-real V14() V15() integer Element of INT
(b . prodc) mod (x . prodc) is ext-real V14() V15() integer set
(prodc + 1) + 1 is ext-real positive non negative non empty V7() V8() V9() V13() V14() V15() integer V38() V43() Element of NAT
i . ((prodc + 1) + 1) is ext-real V14() V15() integer Element of INT
(i . ((prodc + 1) + 1)) * nlist is ext-real V14() V15() integer set
I0 . ((prodc + 1) + 1) is ext-real V14() V15() integer Element of INT
(I0 . ((prodc + 1) + 1)) * a is ext-real V14() V15() integer set
((i . ((prodc + 1) + 1)) * nlist) + ((I0 . ((prodc + 1) + 1)) * a) is ext-real V14() V15() integer set
l . (prodc + 1) is ext-real V14() V15() integer Element of INT
(l . (prodc + 1)) * nlist is ext-real V14() V15() integer set
((l . (prodc + 1)) * nlist) + ((I0 . ((prodc + 1) + 1)) * a) is ext-real V14() V15() integer set
m . (prodc + 1) is ext-real V14() V15() integer Element of INT
(m . (prodc + 1)) * a is ext-real V14() V15() integer set
((l . (prodc + 1)) * nlist) + ((m . (prodc + 1)) * a) is ext-real V14() V15() integer set
y . (prodc + 1) is ext-real V14() V15() integer Element of INT
l . prodc is ext-real V14() V15() integer Element of INT
(y . (prodc + 1)) * (l . prodc) is ext-real V14() V15() integer set
(i . prodc) - ((y . (prodc + 1)) * (l . prodc)) is ext-real V14() V15() integer set
((i . prodc) - ((y . (prodc + 1)) * (l . prodc))) * nlist is ext-real V14() V15() integer set
(((i . prodc) - ((y . (prodc + 1)) * (l . prodc))) * nlist) + ((m . (prodc + 1)) * a) is ext-real V14() V15() integer set
m . prodc is ext-real V14() V15() integer Element of INT
(y . (prodc + 1)) * (m . prodc) is ext-real V14() V15() integer set
(I0 . prodc) - ((y . (prodc + 1)) * (m . prodc)) is ext-real V14() V15() integer set
((I0 . prodc) - ((y . (prodc + 1)) * (m . prodc))) * a is ext-real V14() V15() integer set
(((i . prodc) - ((y . (prodc + 1)) * (l . prodc))) * nlist) + (((I0 . prodc) - ((y . (prodc + 1)) * (m . prodc))) * a) is ext-real V14() V15() integer set
(l . prodc) * nlist is ext-real V14() V15() integer set
(m . prodc) * a is ext-real V14() V15() integer set
((l . prodc) * nlist) + ((m . prodc) * a) is ext-real V14() V15() integer set
(y . (prodc + 1)) * (((l . prodc) * nlist) + ((m . prodc) * a)) is ext-real V14() V15() integer set
(b . prodc) - ((y . (prodc + 1)) * (((l . prodc) * nlist) + ((m . prodc) * a))) is ext-real V14() V15() integer set
((i . (prodc + 1)) * nlist) + ((m . prodc) * a) is ext-real V14() V15() integer set
(y . (prodc + 1)) * (((i . (prodc + 1)) * nlist) + ((m . prodc) * a)) is ext-real V14() V15() integer set
(b . prodc) - ((y . (prodc + 1)) * (((i . (prodc + 1)) * nlist) + ((m . prodc) * a))) is ext-real V14() V15() integer set
(y . (prodc + 1)) * (b . (prodc + 1)) is ext-real V14() V15() integer set
(b . prodc) - ((y . (prodc + 1)) * (b . (prodc + 1))) is ext-real V14() V15() integer set
(b . prodc) div (x . prodc) is ext-real V14() V15() integer set
(b . prodc) / (x . prodc) is ext-real V14() V15() set
[\((b . prodc) / (x . prodc))/] is ext-real V14() V15() integer set
((b . prodc) div (x . prodc)) * (b . (prodc + 1)) is ext-real V14() V15() integer set
(b . prodc) - (((b . prodc) div (x . prodc)) * (b . (prodc + 1))) is ext-real V14() V15() integer set
((b . prodc) div (x . prodc)) * (x . prodc) is ext-real V14() V15() integer set
(b . prodc) - (((b . prodc) div (x . prodc)) * (x . prodc)) is ext-real V14() V15() integer set
(b . prodc) mod (x . prodc) is ext-real V14() V15() integer set
m . (prodc + 1) is ext-real V14() V15() integer Element of INT
b . ((prodc + 1) + 1) is ext-real V14() V15() integer Element of INT
prodc is ext-real non negative V7() V8() V9() V13() V14() V15() integer V38() V43() Element of NAT
x . prodc is ext-real V14() V15() integer Element of INT
prodc + 1 is ext-real positive non negative non empty V7() V8() V9() V13() V14() V15() integer V38() V43() Element of NAT
i . (prodc + 1) is ext-real V14() V15() integer Element of INT
(i . (prodc + 1)) * nlist is ext-real V14() V15() integer set
I0 . (prodc + 1) is ext-real V14() V15() integer Element of INT
(I0 . (prodc + 1)) * a is ext-real V14() V15() integer set
((i . (prodc + 1)) * nlist) + ((I0 . (prodc + 1)) * a) is ext-real V14() V15() integer set
b . (prodc + 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
(nlist,a) is Element of [:INT,INT,INT:]
(nlist,a) `3_3 is ext-real V14() V15() integer Element of INT
nlist gcd a is ext-real non negative V7() V8() V9() V13() V14() V15() integer V38() V43() set
(nlist,a) `1_3 is ext-real V14() V15() integer Element of INT
(nlist,a) `1 is set
((nlist,a) `1) `1 is set
((nlist,a) `1_3) * nlist is ext-real V14() V15() integer set
(nlist,a) `2_3 is ext-real V14() V15() integer Element of INT
((nlist,a) `1) `2 is set
((nlist,a) `2_3) * a is ext-real V14() V15() integer set
(((nlist,a) `1_3) * nlist) + (((nlist,a) `2_3) * a) is ext-real V14() V15() integer set
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
prodc 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 . prodc is ext-real V14() V15() integer Element of INT
i . prodc is ext-real V14() V15() integer Element of INT
I0 . prodc is ext-real V14() V15() integer Element of INT
[(i . prodc),(I0 . prodc),(b . prodc)] is V29() V30() set
[(i . prodc),(I0 . prodc)] is V29() set
[[(i . prodc),(I0 . prodc)],(b . prodc)] is V29() set
- (i . prodc) is ext-real V14() V15() integer set
- (I0 . prodc) is ext-real V14() V15() integer set
- (b . prodc) is ext-real V14() V15() integer set
[(- (i . prodc)),(- (I0 . prodc)),(- (b . prodc))] is V29() V30() set
[(- (i . prodc)),(- (I0 . prodc))] is V29() set
[[(- (i . prodc)),(- (I0 . prodc))],(- (b . prodc))] is V29() set
prodi is ext-real non negative V7() V8() V9() V13() V14() V15() integer V38() V43() Element of NAT
prodi + 1 is ext-real positive non negative non empty V7() V8() V9() V13() V14() V15() integer V38() V43() Element of NAT
b . (prodi + 1) is ext-real V14() V15() integer Element of INT
x . prodi is ext-real V14() V15() integer Element of INT
x . (prodi + 1) is ext-real V14() V15() integer Element of INT
m . (prodi + 1) is ext-real V14() V15() integer Element of INT
b . prodi is ext-real V14() V15() integer Element of INT
(b . prodi) mod (x . prodi) is ext-real V14() V15() integer set
abs (b . prodc) is ext-real non negative V7() V8() V9() V13() V14() V15() integer V38() V43() Element of NAT
prodi is ext-real non negative V7() V8() V9() V13() V14() V15() integer V38() V43() Element of NAT
x . prodi is ext-real V14() V15() integer Element of INT
- 1 is ext-real non positive V14() V15() integer set
1 - 1 is ext-real V14() V15() integer set
prodc - 1 is ext-real V14() V15() integer set
prodi is ext-real non negative V7() V8() V9() V13() V14() V15() integer V38() V43() Element of NAT
x . prodi is ext-real V14() V15() integer Element of INT
prodc - 0 is ext-real non negative V14() V15() integer set
b . prodi is ext-real V14() V15() integer Element of INT
(b . prodi) gcd (x . prodi) is ext-real non negative V7() V8() V9() V13() V14() V15() integer V38() V43() set
prodi + 1 is ext-real positive non negative non empty V7() V8() V9() V13() V14() V15() integer V38() V43() Element of NAT
b . (prodi + 1) is ext-real V14() V15() integer Element of INT
x . (prodi + 1) is ext-real V14() V15() integer Element of INT
(b . (prodi + 1)) gcd (x . (prodi + 1)) is ext-real non negative V7() V8() V9() V13() V14() V15() integer V38() V43() set
x . prodc is ext-real V14() V15() integer Element of INT
(b . prodc) gcd (x . prodc) is ext-real non negative V7() V8() V9() V13() V14() V15() integer V38() V43() set
M0 is ext-real non negative V7() V8() V9() V13() V14() V15() integer V38() V43() Element of NAT
x . M0 is ext-real V14() V15() integer Element of INT
i . (prodi + 1) is ext-real V14() V15() integer Element of INT
(i . (prodi + 1)) * nlist is ext-real V14() V15() integer set
I0 . (prodi + 1) is ext-real V14() V15() integer Element of INT
(I0 . (prodi + 1)) * a is ext-real V14() V15() integer set
((i . (prodi + 1)) * nlist) + ((I0 . (prodi + 1)) * a) is ext-real V14() V15() integer set
nlist is ext-real V14() V15() integer Element of INT
a is ext-real V14() V15() integer Element of INT
nlist mod a is ext-real V14() V15() integer set
b is ext-real V14() V15() integer Element of INT
(a,b) is Element of [:INT,INT,INT:]
(a,b) `3_3 is ext-real V14() V15() integer Element of INT
(a,b) `2_3 is ext-real V14() V15() integer Element of INT
(a,b) `1 is set
((a,b) `1) `2 is set
x is ext-real V14() V15() integer Element of INT
a + x is ext-real V14() V15() integer set
y is ext-real V14() V15() integer Element of INT
m is ext-real V14() V15() integer Element of INT
a + m is ext-real V14() V15() integer set
(a,b) `2_3 is ext-real V14() V15() integer Element of INT
(a,b) `1 is set
((a,b) `1) `2 is set
(a,b) `2_3 is ext-real V14() V15() integer Element of INT
(a,b) `1 is set
((a,b) `1) `2 is set
(a,b) `2_3 is ext-real V14() V15() integer Element of INT
(a,b) `1 is set
((a,b) `1) `2 is set
y is ext-real V14() V15() integer Element of INT
x is ext-real V14() V15() integer Element of INT
a + y is ext-real V14() V15() integer set
b is ext-real V14() V15() integer Element of INT
(a,b) is Element of [:INT,INT,INT:]
(a,b) `3_3 is ext-real V14() V15() integer Element of INT
x is ext-real V14() V15() integer Element of INT
(a,b) `2_3 is ext-real V14() V15() integer Element of INT
(a,b) `1 is set
((a,b) `1) `2 is set
b is ext-real V14() V15() integer Element of INT
(a,b) is Element of [:INT,INT,INT:]
(a,b) `3_3 is ext-real V14() V15() integer Element of INT
(a,b) `2_3 is ext-real V14() V15() integer Element of INT
(a,b) `1 is set
((a,b) `1) `2 is set
b is ext-real V14() V15() integer Element of INT
(a,b) is Element of [:INT,INT,INT:]
(a,b) `3_3 is ext-real V14() V15() integer Element of INT
(a,b) `2_3 is ext-real V14() V15() integer Element of INT
(a,b) `1 is set
((a,b) `1) `2 is set
y is ext-real V14() V15() integer Element of INT
x is ext-real V14() V15() integer Element of INT
a + y is ext-real V14() V15() integer set
x is ext-real V14() V15() integer Element of INT
y is ext-real V14() V15() integer Element of INT
(a,y) is Element of [:INT,INT,INT:]
(a,y) `3_3 is ext-real V14() V15() integer Element of INT
(a,y) `2_3 is ext-real V14() V15() integer Element of INT
(a,y) `1 is set
((a,y) `1) `2 is set
m is ext-real V14() V15() integer Element of INT
a + m is ext-real V14() V15() integer set
b is ext-real V14() V15() integer Element of INT
x is ext-real V14() V15() integer Element of INT
y is ext-real V14() V15() integer Element of INT
(a,y) is Element of [:INT,INT,INT:]
(a,y) `3_3 is ext-real V14() V15() integer Element of INT
(a,y) `2_3 is ext-real V14() V15() integer Element of INT
(a,y) `1 is set
((a,y) `1) `2 is set
m is ext-real V14() V15() integer Element of INT
a + m is ext-real V14() V15() integer set
i is ext-real V14() V15() integer Element of INT
a + i is ext-real V14() V15() integer set
(a,y) `2_3 is ext-real V14() V15() integer Element of INT
(a,y) `1 is set
((a,y) `1) `2 is set
(a,y) `2_3 is ext-real V14() V15() integer Element of INT
(a,y) `1 is set
((a,y) `1) `2 is set
y is ext-real V14() V15() integer Element of INT
(a,y) is Element of [:INT,INT,INT:]
(a,y) `3_3 is ext-real V14() V15() integer Element of INT
y is ext-real V14() V15() integer Element of INT
(a,y) is Element of [:INT,INT,INT:]
(a,y) `3_3 is ext-real V14() V15() integer Element of INT
a is ext-real V14() V15() integer Element of INT
nlist is ext-real V14() V15() integer Element of INT
b is ext-real V14() V15() integer Element of INT
nlist mod b is ext-real V14() V15() integer set
(b,a) is Element of [:INT,INT,INT:]
(b,a) `3_3 is ext-real V14() V15() integer Element of INT
(nlist,b) is ext-real V14() V15() integer Element of INT
(nlist,b) * nlist is ext-real V14() V15() integer set
((nlist,b) * nlist) mod b is ext-real V14() V15() integer set
1 mod b is ext-real V14() V15() integer set
b gcd a is ext-real non negative V7() V8() V9() V13() V14() V15() integer V38() V43() set
(b,a) `1_3 is ext-real V14() V15() integer Element of INT
(b,a) `1 is set
((b,a) `1) `1 is set
((b,a) `1_3) * b is ext-real V14() V15() integer set
(b,a) `2_3 is ext-real V14() V15() integer Element of INT
((b,a) `1) `2 is set
((b,a) `2_3) * a is ext-real V14() V15() integer set
(((b,a) `1_3) * b) + (((b,a) `2_3) * a) is ext-real V14() V15() integer set
b mod b is ext-real V14() V15() integer set
(((b,a) `1_3) * b) mod b is ext-real V14() V15() integer set
((b,a) `1_3) mod b is ext-real V14() V15() integer set
(((b,a) `1_3) mod b) * (b mod b) is ext-real V14() V15() integer set
((((b,a) `1_3) mod b) * (b mod b)) mod b is ext-real V14() V15() integer set
((((b,a) `1_3) * b) + (((b,a) `2_3) * a)) mod b is ext-real V14() V15() integer set
x is ext-real V14() V15() integer set
x mod b is ext-real V14() V15() integer set
y is ext-real V14() V15() integer set
y mod b is ext-real V14() V15() integer set
(x mod b) + (y mod b) is ext-real V14() V15() integer set
((x mod b) + (y mod b)) mod b is ext-real V14() V15() integer set
(((b,a) `2_3) * a) mod b is ext-real V14() V15() integer set
I0 is ext-real V14() V15() integer Element of INT
b + I0 is ext-real V14() V15() integer set
b * nlist is ext-real V14() V15() integer set
I0 * nlist is ext-real V14() V15() integer set
(b * nlist) + (I0 * nlist) is ext-real V14() V15() integer set
((b * nlist) + (I0 * nlist)) mod b is ext-real V14() V15() integer set
(I0 * nlist) mod b is ext-real V14() V15() integer set
I0 mod b is ext-real V14() V15() integer set
(I0 mod b) * (nlist mod b) is ext-real V14() V15() integer set
((I0 mod b) * (nlist mod b)) mod b is ext-real V14() V15() integer set
(nlist mod b) mod b is ext-real V14() V15() integer set
(I0 mod b) * ((nlist mod b) mod b) is ext-real V14() V15() integer set
((I0 mod b) * ((nlist mod b) mod b)) mod b is ext-real V14() V15() integer set
((b,a) `2_3) * nlist is ext-real V14() V15() integer set
(((b,a) `2_3) * nlist) mod b is ext-real V14() V15() integer set
m is ext-real V14() V15() integer set
m mod b is ext-real V14() V15() integer set
(m mod b) * (nlist mod b) is ext-real V14() V15() integer set
((m mod b) * (nlist mod b)) mod b is ext-real V14() V15() integer set
(nlist mod b) mod b is ext-real V14() V15() integer set
(m mod b) * ((nlist mod b) mod b) is ext-real V14() V15() integer set
((m mod b) * ((nlist mod b) mod b)) mod b is ext-real V14() V15() integer set
b 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
nlist mod a is ext-real V14() V15() integer set
(a,b) is Element of [:INT,INT,INT:]
(a,b) `3_3 is ext-real V14() V15() integer Element of INT
(nlist,a) is ext-real V14() V15() integer Element of INT
(nlist,a) * nlist is ext-real V14() V15() integer set
((nlist,a) * nlist) mod a is ext-real V14() V15() integer set
1 mod a is ext-real V14() V15() integer set
nlist is non empty V18() V21( NAT ) V22([:INT,INT:]) Function-like V38() FinSequence-like FinSubsequence-like FinSequence of [:INT,INT:]
len nlist is ext-real positive non negative non empty V7() V8() V9() V13() V14() V15() integer V38() V43() Element of NAT
nlist . 1 is set
(nlist . 1) `1 is set
(len nlist) - 1 is ext-real V14() V15() integer set
Seg (len nlist) is non empty V38() V45( len nlist) Element of bool NAT
{ b<sub>1</sub> where b<sub>1</sub> is ext-real non negative V7() V8() V9() V13() V14() V15() integer V38() V43() Element of NAT : ( 1 <= b<sub>1</sub> & b<sub>1</sub> <= len nlist ) } is set
dom nlist is Element of bool NAT
b is ext-real non negative V7() V8() V9() V13() V14() V15() integer V38() V43() Element of NAT
nlist . b is set
(nlist . b) `2 is set
x is ext-real V14() V15() integer Element of INT
Seg (len nlist) is non empty V38() V45( len nlist) 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₁ <= len nlist ) } is set
dom nlist is Element of bool NAT
y is ext-real V14() V15() integer Element of INT
x * y is ext-real V14() V15() integer set
m is ext-real V14() V15() integer Element of INT
a is ext-real V14() V15() integer Element of INT
b is V18() V21( NAT ) V22( INT ) Function-like V38() FinSequence-like FinSubsequence-like V60() V61() V62() FinSequence of INT
len b is ext-real non negative V7() V8() V9() V13() V14() V15() integer V38() V43() Element of NAT
b . 1 is ext-real V14() V15() integer set
(len b) - 0 is ext-real non negative V14() V15() integer set
(len b) - 1 is ext-real V14() V15() integer set
x is ext-real non negative V7() V8() V9() V13() V14() V15() integer V38() V43() set
nlist . x is set
(nlist . x) `2 is set
x + 1 is ext-real positive non negative non empty V7() V8() V9() V13() V14() V15() integer V38() V43() Element of NAT
b . (x + 1) is ext-real V14() V15() integer set
b . x is ext-real V14() V15() integer set
1 - 1 is ext-real V14() V15() integer set
x is ext-real non negative V7() V8() V9() V13() V14() V15() integer V38() V43() Element of NAT
Seg x is V38() V45(x) Element of bool NAT
{ b<sub>1</sub> where b<sub>1</sub> is ext-real non negative V7() V8() V9() V13() V14() V15() integer V38() V43() Element of NAT : ( 1 <= b<sub>1</sub> & b<sub>1</sub> <= x ) } is set
y is ext-real non negative V7() V8() V9() V13() V14() V15() integer V38() V43() set
nlist . y is set
(nlist . y) `2 is set
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 V14() V15() integer set
b . y is ext-real V14() V15() integer set
nlist . (y + 1) is set
(nlist . (y + 1)) `2 is set
m is ext-real V14() V15() integer Element of INT
(b . y) * m is ext-real V14() V15() integer set
((len b) - 1) + 1 is ext-real V14() V15() integer set
Seg (len nlist) is non empty V38() V45( len nlist) Element of bool NAT
{ b<sub>1</sub> where b<sub>1</sub> is ext-real non negative V7() V8() V9() V13() V14() V15() integer V38() V43() Element of NAT : ( 1 <= b<sub>1</sub> & b<sub>1</sub> <= len nlist ) } is set
dom nlist is Element of bool NAT
i is ext-real V14() V15() integer Element of INT
I0 is ext-real V14() V15() integer Element of INT
(i,I0) is ext-real V14() V15() integer Element of INT
m is ext-real V14() V15() integer Element of INT
y is V18() V21( NAT ) V22( INT ) Function-like V38() FinSequence-like FinSubsequence-like V60() V61() V62() FinSequence of INT
dom y is Element of bool NAT
len 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() set
nlist . m is set
(nlist . m) `2 is set
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 V14() V15() integer set
b . m is ext-real V14() V15() integer set
nlist . (m + 1) is set
(nlist . (m + 1)) `2 is set
y . m is ext-real V14() V15() integer set
m is ext-real non negative V7() V8() V9() V13() V14() V15() integer V38() V43() set
nlist . m is set
(nlist . m) `2 is set
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 V14() V15() integer set
b . m is ext-real V14() V15() integer set
nlist . (m + 1) is set
(nlist . (m + 1)) `2 is set
y . m is ext-real V14() V15() integer set
I0 is ext-real V14() V15() integer Element of INT
(b . m) * I0 is ext-real V14() V15() integer set
m is ext-real V14() V15() integer Element of INT
i is ext-real V14() V15() integer Element of INT
(m,i) is ext-real V14() V15() integer Element of INT
l is ext-real V14() V15() integer Element of INT
m is V18() V21( NAT ) V22( INT ) Function-like V38() FinSequence-like FinSubsequence-like V60() V61() V62() FinSequence of INT
dom m is Element of bool NAT
len m 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() set
nlist . i is set
(nlist . i) `2 is set
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 V14() V15() integer set
b . i is ext-real V14() V15() integer set
nlist . (i + 1) is set
(nlist . (i + 1)) `2 is set
y . i is ext-real V14() V15() integer set
m . i is ext-real V14() V15() integer set
Seg (len nlist) is non empty V38() V45( len nlist) Element of bool NAT
{ b<sub>1</sub> where b<sub>1</sub> is ext-real non negative V7() V8() V9() V13() V14() V15() integer V38() V43() Element of NAT : ( 1 <= b<sub>1</sub> & b<sub>1</sub> <= len nlist ) } is set
dom nlist is Element of bool NAT
nlist . (len b) is set
(nlist . (len b)) `2 is set
1 + 1 is ext-real positive non negative non empty V7() V8() V9() V13() V14() V15() integer V38() V43() Element of NAT
2 - 1 is ext-real V14() V15() integer set
INT * is non empty functional FinSequence-membered set
m . ((len b) - 1) is ext-real V14() V15() integer set
I0 is ext-real V14() V15() integer Element of INT
i is ext-real V14() V15() integer Element of INT
I0 * i is ext-real V14() V15() integer set
prodc is ext-real non negative V7() V8() V9() V13() V14() V15() integer V38() V43() Element of NAT
prodc + 1 is ext-real positive non negative non empty V7() V8() V9() V13() V14() V15() integer V38() V43() Element of NAT
nlist . (prodc + 1) is set
(nlist . (prodc + 1)) `1 is set
(nlist . (prodc + 1)) `2 is set
y . prodc is ext-real V14() V15() integer set
m . prodc is ext-real V14() V15() integer set
prodi is ext-real V14() V15() integer Element of INT
prodc + 1 is ext-real positive non negative non empty V7() V8() V9() V13() V14() V15() integer V38() V43() Element of NAT
nlist . (prodc + 1) is set
(nlist . (prodc + 1)) `1 is set
(nlist . (prodc + 1)) `2 is set
M0 is ext-real V14() V15() integer Element of INT
M0 - prodi is ext-real V14() V15() integer set
(M0 - prodi) * (y . prodc) is ext-real V14() V15() integer set
M is ext-real V14() V15() integer Element of INT
((M0 - prodi) * (y . prodc)) mod M is ext-real V14() V15() integer set
lb1 is ext-real V14() V15() integer Element of INT
lb1 * (m . prodc) is ext-real V14() V15() integer set
prodi + (lb1 * (m . prodc)) is ext-real V14() V15() integer set
l1 is ext-real V14() V15() integer Element of INT
prodc is ext-real V14() V15() integer Element of INT
prodi is V18() V21( NAT ) V22( INT ) Function-like V38() FinSequence-like FinSubsequence-like V60() V61() V62() FinSequence of INT
len prodi is ext-real non negative V7() V8() V9() V13() V14() V15() integer V38() V43() Element of NAT
prodi . 1 is ext-real V14() V15() integer set
M0 is ext-real non negative V7() V8() V9() V13() V14() V15() integer V38() V43() set
M0 + 1 is ext-real positive non negative non empty V7() V8() V9() V13() V14() V15() integer V38() V43() Element of NAT
nlist . (M0 + 1) is set
(nlist . (M0 + 1)) `1 is set
(nlist . (M0 + 1)) `2 is set
prodi . M0 is ext-real V14() V15() integer set
y . M0 is ext-real V14() V15() integer set
prodi . (M0 + 1) is ext-real V14() V15() integer set
m . M0 is ext-real V14() V15() integer set
prodi . (len b) is ext-real V14() V15() integer set
m is ext-real V14() V15() integer Element of INT
(prodi . (len b)) mod m is ext-real V14() V15() integer set
(m . ((len b) - 1)) * i is ext-real V14() V15() integer set
M0 is ext-real V14() V15() integer Element of INT
a is ext-real V14() V15() integer Element of INT
b is ext-real V14() V15() integer Element of INT
x is V18() V21( NAT ) V22( INT ) Function-like V38() FinSequence-like FinSubsequence-like V60() V61() V62() FinSequence of INT
len x is ext-real non negative V7() V8() V9() V13() V14() V15() integer V38() V43() Element of NAT
y is V18() V21( NAT ) V22( INT ) Function-like V38() FinSequence-like FinSubsequence-like V60() V61() V62() FinSequence of INT
len y is ext-real non negative V7() V8() V9() V13() V14() V15() integer V38() V43() Element of NAT
m is V18() V21( NAT ) V22( INT ) Function-like V38() FinSequence-like FinSubsequence-like V60() V61() V62() FinSequence of INT
len m is ext-real non negative V7() V8() V9() V13() V14() V15() integer V38() V43() Element of NAT
i is V18() V21( NAT ) V22( INT ) Function-like V38() FinSequence-like FinSubsequence-like V60() V61() V62() FinSequence of INT
len i is ext-real non negative V7() V8() V9() V13() V14() V15() integer V38() V43() Element of NAT
x . 1 is ext-real V14() V15() integer set
(len x) - 1 is ext-real V14() V15() integer set
I0 is ext-real V14() V15() integer Element of INT
nlist . (len x) is set
(nlist . (len x)) `2 is set
m is ext-real V14() V15() integer Element of INT
m . ((len x) - 1) is ext-real V14() V15() integer set
(m . ((len x) - 1)) * I0 is ext-real V14() V15() integer set
y . 1 is ext-real V14() V15() integer set
y . (len x) is ext-real V14() V15() integer set
(y . (len x)) mod m is ext-real V14() V15() integer set
l is V18() V21( NAT ) V22( INT ) Function-like V38() FinSequence-like FinSubsequence-like V60() V61() V62() FinSequence of INT
len l is ext-real non negative V7() V8() V9() V13() V14() V15() integer V38() V43() Element of NAT
prodc is V18() V21( NAT ) V22( INT ) Function-like V38() FinSequence-like FinSubsequence-like V60() V61() V62() FinSequence of INT
len prodc is ext-real non negative V7() V8() V9() V13() V14() V15() integer V38() V43() Element of NAT
prodi is V18() V21( NAT ) V22( INT ) Function-like V38() FinSequence-like FinSubsequence-like V60() V61() V62() FinSequence of INT
len prodi is ext-real non negative V7() V8() V9() V13() V14() V15() integer V38() V43() Element of NAT
M0 is V18() V21( NAT ) V22( INT ) Function-like V38() FinSequence-like FinSubsequence-like V60() V61() V62() FinSequence of INT
len M0 is ext-real non negative V7() V8() V9() V13() V14() V15() integer V38() V43() Element of NAT
l . 1 is ext-real V14() V15() integer set
(len l) - 1 is ext-real V14() V15() integer set
M is ext-real V14() V15() integer Element of INT
nlist . (len l) is set
(nlist . (len l)) `2 is set
lb1 is ext-real V14() V15() integer Element of INT
prodi . ((len l) - 1) is ext-real V14() V15() integer set
(prodi . ((len l) - 1)) * M is ext-real V14() V15() integer set
prodc . 1 is ext-real V14() V15() integer set
prodc . (len l) is ext-real V14() V15() integer set
(prodc . (len l)) mod lb1 is ext-real V14() V15() integer set
x is V18() V21( NAT ) V22( INT ) Function-like V38() FinSequence-like FinSubsequence-like V60() V61() V62() FinSequence of INT
len x is ext-real non negative V7() V8() V9() V13() V14() V15() integer V38() V43() Element of NAT
y is V18() V21( NAT ) V22( INT ) Function-like V38() FinSequence-like FinSubsequence-like V60() V61() V62() FinSequence of INT
len y is ext-real non negative V7() V8() V9() V13() V14() V15() integer V38() V43() Element of NAT
m is V18() V21( NAT ) V22( INT ) Function-like V38() FinSequence-like FinSubsequence-like V60() V61() V62() FinSequence of INT
len m is ext-real non negative V7() V8() V9() V13() V14() V15() integer V38() V43() Element of NAT
i is V18() V21( NAT ) V22( INT ) Function-like V38() FinSequence-like FinSubsequence-like V60() V61() V62() FinSequence of INT
len i is ext-real non negative V7() V8() V9() V13() V14() V15() integer V38() V43() Element of NAT
x . 1 is ext-real V14() V15() integer set
(len x) - 1 is ext-real V14() V15() integer set
I0 is ext-real V14() V15() integer Element of INT
nlist . (len x) is set
(nlist . (len x)) `2 is set
m is ext-real V14() V15() integer Element of INT
m . ((len x) - 1) is ext-real V14() V15() integer set
(m . ((len x) - 1)) * I0 is ext-real V14() V15() integer set
y . 1 is ext-real V14() V15() integer set
y . (len x) is ext-real V14() V15() integer set
(y . (len x)) mod m is ext-real V14() V15() integer set
x is V18() V21( NAT ) V22( INT ) Function-like V38() FinSequence-like FinSubsequence-like V60() V61() V62() FinSequence of INT
len x is ext-real non negative V7() V8() V9() V13() V14() V15() integer V38() V43() Element of NAT
y is V18() V21( NAT ) V22( INT ) Function-like V38() FinSequence-like FinSubsequence-like V60() V61() V62() FinSequence of INT
len y is ext-real non negative V7() V8() V9() V13() V14() V15() integer V38() V43() Element of NAT
m is V18() V21( NAT ) V22( INT ) Function-like V38() FinSequence-like FinSubsequence-like V60() V61() V62() FinSequence of INT
len m is ext-real non negative V7() V8() V9() V13() V14() V15() integer V38() V43() Element of NAT
i is V18() V21( NAT ) V22( INT ) Function-like V38() FinSequence-like FinSubsequence-like V60() V61() V62() FinSequence of INT
len i is ext-real non negative V7() V8() V9() V13() V14() V15() integer V38() V43() Element of NAT
x . 1 is ext-real V14() V15() integer set
(len x) - 1 is ext-real V14() V15() integer set
I0 is ext-real V14() V15() integer Element of INT
nlist . (len x) is set
(nlist . (len x)) `2 is set
m is ext-real V14() V15() integer Element of INT
m . ((len x) - 1) is ext-real V14() V15() integer set
(m . ((len x) - 1)) * I0 is ext-real V14() V15() integer set
y . 1 is ext-real V14() V15() integer set
y . (len x) is ext-real V14() V15() integer set
(y . (len x)) mod m is ext-real V14() V15() integer set
l is V18() V21( NAT ) V22( INT ) Function-like V38() FinSequence-like FinSubsequence-like V60() V61() V62() FinSequence of INT
len l is ext-real non negative V7() V8() V9() V13() V14() V15() integer V38() V43() Element of NAT
prodc is V18() V21( NAT ) V22( INT ) Function-like V38() FinSequence-like FinSubsequence-like V60() V61() V62() FinSequence of INT
len prodc is ext-real non negative V7() V8() V9() V13() V14() V15() integer V38() V43() Element of NAT
prodi is V18() V21( NAT ) V22( INT ) Function-like V38() FinSequence-like FinSubsequence-like V60() V61() V62() FinSequence of INT
len prodi is ext-real non negative V7() V8() V9() V13() V14() V15() integer V38() V43() Element of NAT
M0 is V18() V21( NAT ) V22( INT ) Function-like V38() FinSequence-like FinSubsequence-like V60() V61() V62() FinSequence of INT
len M0 is ext-real non negative V7() V8() V9() V13() V14() V15() integer V38() V43() Element of NAT
l . 1 is ext-real V14() V15() integer set
(len l) - 1 is ext-real V14() V15() integer set
M is ext-real V14() V15() integer Element of INT
nlist . (len l) is set
(nlist . (len l)) `2 is set
lb1 is ext-real V14() V15() integer Element of INT
prodi . ((len l) - 1) is ext-real V14() V15() integer set
(prodi . ((len l) - 1)) * M is ext-real V14() V15() integer set
prodc . 1 is ext-real V14() V15() integer set
prodc . (len l) is ext-real V14() V15() integer set
(prodc . (len l)) mod lb1 is ext-real V14() V15() integer set
l is V18() V21( NAT ) V22( INT ) Function-like V38() FinSequence-like FinSubsequence-like V60() V61() V62() FinSequence of INT
len l is ext-real non negative V7() V8() V9() V13() V14() V15() integer V38() V43() Element of NAT
prodc is V18() V21( NAT ) V22( INT ) Function-like V38() FinSequence-like FinSubsequence-like V60() V61() V62() FinSequence of INT
len prodc is ext-real non negative V7() V8() V9() V13() V14() V15() integer V38() V43() Element of NAT
prodi is V18() V21( NAT ) V22( INT ) Function-like V38() FinSequence-like FinSubsequence-like V60() V61() V62() FinSequence of INT
len prodi is ext-real non negative V7() V8() V9() V13() V14() V15() integer V38() V43() Element of NAT
M0 is V18() V21( NAT ) V22( INT ) Function-like V38() FinSequence-like FinSubsequence-like V60() V61() V62() FinSequence of INT
len M0 is ext-real non negative V7() V8() V9() V13() V14() V15() integer V38() V43() Element of NAT
l . 1 is ext-real V14() V15() integer set
(len l) - 1 is ext-real V14() V15() integer set
M is ext-real V14() V15() integer Element of INT
nlist . (len l) is set
(nlist . (len l)) `2 is set
lb1 is ext-real V14() V15() integer Element of INT
prodi . ((len l) - 1) is ext-real V14() V15() integer set
(prodi . ((len l) - 1)) * M is ext-real V14() V15() integer set
prodc . 1 is ext-real V14() V15() integer set
prodc . (len l) is ext-real V14() V15() integer set
(prodc . (len l)) mod lb1 is ext-real V14() V15() integer set
x . 0 is ext-real V14() V15() integer set
l . 0 is ext-real V14() V15() integer set
l1 is ext-real non negative V7() V8() V9() V13() V14() V15() integer V38() V43() set
x . l1 is ext-real V14() V15() integer set
l . l1 is ext-real V14() V15() integer set
l1 + 1 is ext-real positive non negative non empty V7() V8() V9() V13() V14() V15() integer V38() V43() Element of NAT
x . (l1 + 1) is ext-real V14() V15() integer set
l . (l1 + 1) is ext-real V14() V15() integer set
1 - 1 is ext-real V14() V15() integer set
(l1 + 1) - 1 is ext-real V14() V15() integer set
(len x) - 0 is ext-real non negative V14() V15() integer set
nlist . l1 is set
(nlist . l1) `2 is set
nlist . (l1 + 1) is set
(nlist . (l1 + 1)) `2 is set
i . l1 is ext-real V14() V15() integer set
m . l1 is ext-real V14() V15() integer set
M0 . l1 is ext-real V14() V15() integer set
prodi . l1 is ext-real V14() V15() integer set
nn1 is ext-real V14() V15() integer Element of INT
(l . l1) * nn1 is ext-real V14() V15() integer set
prodi1 is ext-real V14() V15() integer Element of INT
m1 is ext-real V14() V15() integer Element of INT
(prodi1,m1) is ext-real V14() V15() integer Element of INT
M01 is ext-real V14() V15() integer Element of INT
(x . l1) * M01 is ext-real V14() V15() integer set
M1 is ext-real V14() V15() integer Element of INT
prodc1 is ext-real V14() V15() integer Element of INT
(M1,prodc1) is ext-real V14() V15() integer Element of INT
l1 is ext-real non negative V7() V8() V9() V13() V14() V15() integer V38() V43() set
nlist . l1 is set
(nlist . l1) `2 is set
l1 + 1 is ext-real positive non negative non empty V7() V8() V9() V13() V14() V15() integer V38() V43() Element of NAT
x . (l1 + 1) is ext-real V14() V15() integer set
x . l1 is ext-real V14() V15() integer set
nlist . (l1 + 1) is set
(nlist . (l1 + 1)) `2 is set
i . l1 is ext-real V14() V15() integer set
m . l1 is ext-real V14() V15() integer set
l . (l1 + 1) is ext-real V14() V15() integer set
l . l1 is ext-real V14() V15() integer set
M0 . l1 is ext-real V14() V15() integer set
prodi . l1 is ext-real V14() V15() integer set
nn1 is ext-real V14() V15() integer Element of INT
(l . l1) * nn1 is ext-real V14() V15() integer set
prodi1 is ext-real V14() V15() integer Element of INT
m1 is ext-real V14() V15() integer Element of INT
(prodi1,m1) is ext-real V14() V15() integer Element of INT
M01 is ext-real V14() V15() integer Element of INT
(x . l1) * M01 is ext-real V14() V15() integer set
M1 is ext-real V14() V15() integer Element of INT
prodc1 is ext-real V14() V15() integer Element of INT
(M1,prodc1) is ext-real V14() V15() integer Element of INT
l1 is ext-real non negative V7() V8() V9() V13() V14() V15() integer V38() V43() set
nlist . l1 is set
(nlist . l1) `2 is set
l1 + 1 is ext-real positive non negative non empty V7() V8() V9() V13() V14() V15() integer V38() V43() Element of NAT
x . (l1 + 1) is ext-real V14() V15() integer set
x . l1 is ext-real V14() V15() integer set
nlist . (l1 + 1) is set
(nlist . (l1 + 1)) `2 is set
i . l1 is ext-real V14() V15() integer set
m . l1 is ext-real V14() V15() integer set
l . (l1 + 1) is ext-real V14() V15() integer set
l . l1 is ext-real V14() V15() integer set
M0 . l1 is ext-real V14() V15() integer set
prodi . l1 is ext-real V14() V15() integer set
nn1 is ext-real V14() V15() integer Element of INT
(l . l1) * nn1 is ext-real V14() V15() integer set
prodi1 is ext-real V14() V15() integer Element of INT
m1 is ext-real V14() V15() integer Element of INT
(prodi1,m1) is ext-real V14() V15() integer Element of INT
M01 is ext-real V14() V15() integer Element of INT
(x . l1) * M01 is ext-real V14() V15() integer set
M1 is ext-real V14() V15() integer Element of INT
prodc1 is ext-real V14() V15() integer Element of INT
(M1,prodc1) is ext-real V14() V15() integer Element of INT
y . 0 is ext-real V14() V15() integer set
prodc . 0 is ext-real V14() V15() integer set
l1 is ext-real non negative V7() V8() V9() V13() V14() V15() integer V38() V43() set
y . l1 is ext-real V14() V15() integer set
prodc . l1 is ext-real V14() V15() integer set
l1 + 1 is ext-real positive non negative non empty V7() V8() V9() V13() V14() V15() integer V38() V43() Element of NAT
y . (l1 + 1) is ext-real V14() V15() integer set
prodc . (l1 + 1) is ext-real V14() V15() integer set
1 - 1 is ext-real V14() V15() integer set
(l1 + 1) - 1 is ext-real V14() V15() integer set
(len y) - 1 is ext-real V14() V15() integer set
(len y) - 0 is ext-real non negative V14() V15() integer set
nlist . (l1 + 1) is set
(nlist . (l1 + 1)) `1 is set
(nlist . (l1 + 1)) `2 is set
i . l1 is ext-real V14() V15() integer set
m . l1 is ext-real V14() V15() integer set
M0 . l1 is ext-real V14() V15() integer set
prodi . l1 is ext-real V14() V15() integer set
nn1 is ext-real V14() V15() integer Element of INT
prodi1 is ext-real V14() V15() integer Element of INT
m1 is ext-real V14() V15() integer Element of INT
nn1 - (prodc . l1) is ext-real V14() V15() integer set
(nn1 - (prodc . l1)) * (M0 . l1) is ext-real V14() V15() integer set
((nn1 - (prodc . l1)) * (M0 . l1)) mod prodi1 is ext-real V14() V15() integer set
m1 * (prodi . l1) is ext-real V14() V15() integer set
(prodc . l1) + (m1 * (prodi . l1)) is ext-real V14() V15() integer set
M01 is ext-real V14() V15() integer Element of INT
M1 is ext-real V14() V15() integer Element of INT
prodc1 is ext-real V14() V15() integer Element of INT
M01 - (y . l1) is ext-real V14() V15() integer set
(M01 - (y . l1)) * (i . l1) is ext-real V14() V15() integer set
((M01 - (y . l1)) * (i . l1)) mod M1 is ext-real V14() V15() integer set
prodc1 * (m . l1) is ext-real V14() V15() integer set
(y . l1) + (prodc1 * (m . l1)) is ext-real V14() V15() integer set
a is ext-real V14() V15() integer Element of INT
nlist is ext-real V14() V15() integer Element of INT
nlist mod a is ext-real V14() V15() integer set
nlist div a is ext-real V14() V15() integer set
nlist / a is ext-real V14() V15() set
[\(nlist / a)/] is ext-real V14() V15() integer set
(nlist div a) * a is ext-real V14() V15() integer set
nlist - ((nlist div a) * a) is ext-real V14() V15() integer set
- (nlist div a) is ext-real V14() V15() integer set
b is ext-real V14() V15() integer Element of INT
a * b is ext-real V14() V15() integer set
(nlist mod a) - nlist is ext-real V14() V15() integer set
a is ext-real V14() V15() integer Element of INT
nlist is ext-real V14() V15() integer Element of INT
nlist mod a is ext-real V14() V15() integer set
(nlist mod a) gcd a is ext-real non negative V7() V8() V9() V13() V14() V15() integer V38() V43() set
nlist gcd a is ext-real non negative V7() V8() V9() V13() V14() V15() integer V38() V43() set
b 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
a mod b is ext-real V14() V15() integer set
a gcd b is ext-real non negative V7() V8() V9() V13() V14() V15() integer V38() V43() set
nlist gcd b is ext-real non negative V7() V8() V9() V13() V14() V15() integer V38() V43() 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 V14() V15() integer Element of INT
a mod b is ext-real V14() V15() integer set
a div b is ext-real V14() V15() integer set
a / b is ext-real V14() V15() set
[\(a / b)/] is ext-real V14() V15() integer set
(a div b) * b is ext-real V14() V15() integer set
((a div b) * b) + nlist is ext-real V14() V15() integer set
- (a div b) is ext-real V14() V15() integer set
x is ext-real V14() V15() integer Element of INT
x * b is ext-real V14() V15() integer set
a + (x * b) is ext-real V14() V15() integer set
nlist is V18() V21( NAT ) V22( INT ) Function-like V38() FinSequence-like FinSubsequence-like V60() V61() V62() FinSequence of INT
len nlist is ext-real non negative V7() V8() V9() V13() V14() V15() integer V38() V43() Element of NAT
a is V18() V21( NAT ) V22( INT ) Function-like V38() FinSequence-like FinSubsequence-like V60() V61() V62() FinSequence of INT
len a is ext-real non negative V7() V8() V9() V13() V14() V15() integer V38() V43() Element of NAT
Seg (len nlist) is V38() V45( len nlist) 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₁ <= len nlist ) } is set
a . 1 is ext-real V14() V15() integer set
(len nlist) - 1 is ext-real V14() V15() integer set
0 + 1 is ext-real positive non negative non empty V7() V8() V9() V13() V14() V15() integer V38() V43() Element of NAT
a . (0 + 1) is ext-real V14() V15() integer set
x is ext-real non negative V7() V8() V9() V13() V14() V15() integer V38() V43() Element of NAT
x + 1 is ext-real positive non negative non empty V7() V8() V9() V13() V14() V15() integer V38() V43() Element of NAT
a . (x + 1) is ext-real V14() V15() integer set
x + 1 is ext-real positive non negative non empty V7() V8() V9() V13() V14() V15() integer V38() V43() Element of NAT
(x + 1) + 1 is ext-real positive non negative non empty V7() V8() V9() V13() V14() V15() integer V38() V43() Element of NAT
a . ((x + 1) + 1) is ext-real V14() V15() integer set
(x + 1) + 1 is ext-real positive non negative non empty V7() V8() V9() V13() V14() V15() integer V38() V43() Element of NAT
a . ((x + 1) + 1) is ext-real V14() V15() integer set
nlist . 1 is ext-real V14() V15() integer set
(a . 1) * (nlist . 1) is ext-real V14() V15() integer set
((len nlist) - 1) + 0 is ext-real V14() V15() integer set
((len nlist) - 1) + 1 is ext-real V14() V15() integer set
y is ext-real non negative V7() V8() V9() V13() V14() V15() integer V38() V43() set
y + 1 is ext-real positive non negative non empty V7() V8() V9() V13() V14() V15() integer V38() V43() Element of NAT
a . (y + 1) is ext-real V14() V15() integer set
a . y is ext-real V14() V15() integer set
nlist . y is ext-real V14() V15() integer set
(a . y) * (nlist . y) is ext-real V14() V15() integer set
(x + 1) + 1 is ext-real positive non negative non empty V7() V8() V9() V13() V14() V15() integer V38() V43() Element of NAT
a . ((x + 1) + 1) is ext-real V14() V15() integer set
((len nlist) - 1) + 1 is ext-real V14() V15() integer set
nlist . (x + 1) is ext-real V14() V15() integer set
a . (x + 1) is ext-real V14() V15() integer set
(a . (x + 1)) * (nlist . (x + 1)) is ext-real V14() V15() integer set
y is ext-real non negative V7() V8() V9() V13() V14() V15() integer V38() V43() set
y + 1 is ext-real positive non negative non empty V7() V8() V9() V13() V14() V15() integer V38() V43() Element of NAT
a . (y + 1) is ext-real V14() V15() integer set
a . y is ext-real V14() V15() integer set
nlist . y is ext-real V14() V15() integer set
(a . y) * (nlist . y) is ext-real V14() V15() integer set
x is ext-real non negative V7() V8() V9() V13() V14() V15() integer V38() V43() Element of NAT
x + 1 is ext-real positive non negative non empty V7() V8() V9() V13() V14() V15() integer V38() V43() Element of NAT
a . (x + 1) is ext-real V14() V15() integer set
nlist is V18() V21( NAT ) V22( INT ) Function-like V38() FinSequence-like FinSubsequence-like V60() V61() V62() FinSequence of INT
len nlist is ext-real non negative V7() V8() V9() V13() V14() V15() integer V38() V43() Element of NAT
Seg (len nlist) is V38() V45( len nlist) 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₁ <= len nlist ) } is set
a is V18() V21( NAT ) V22( INT ) Function-like V38() FinSequence-like FinSubsequence-like V60() V61() V62() FinSequence of INT
a . 1 is ext-real V14() V15() integer set
(len nlist) - 1 is ext-real V14() V15() integer set
0 + 1 is ext-real positive non negative non empty V7() V8() V9() V13() V14() V15() integer V38() V43() Element of NAT
a . (0 + 1) is ext-real V14() V15() integer set
x is ext-real non negative V7() V8() V9() V13() V14() V15() integer V38() V43() set
nlist . x is ext-real V14() V15() integer set
x is ext-real non negative V7() V8() V9() V13() V14() V15() integer V38() V43() Element of NAT
x + 1 is ext-real positive non negative non empty V7() V8() V9() V13() V14() V15() integer V38() V43() Element of NAT
a . (x + 1) is ext-real V14() V15() integer set
x + 1 is ext-real positive non negative non empty V7() V8() V9() V13() V14() V15() integer V38() V43() Element of NAT
(x + 1) + 1 is ext-real positive non negative non empty V7() V8() V9() V13() V14() V15() integer V38() V43() Element of NAT
a . ((x + 1) + 1) is ext-real V14() V15() integer set
(x + 1) + 1 is ext-real positive non negative non empty V7() V8() V9() V13() V14() V15() integer V38() V43() Element of NAT
a . ((x + 1) + 1) is ext-real V14() V15() integer set
nlist . 1 is ext-real V14() V15() integer set
(a . 1) * (nlist . 1) is ext-real V14() V15() integer set
y is ext-real non negative V7() V8() V9() V13() V14() V15() integer V38() V43() set
nlist . y is ext-real V14() V15() integer set
y is ext-real non negative V7() V8() V9() V13() V14() V15() integer V38() V43() set
nlist . y is ext-real V14() V15() integer set
y is ext-real non negative V7() V8() V9() V13() V14() V15() integer V38() V43() set
y + 1 is ext-real positive non negative non empty V7() V8() V9() V13() V14() V15() integer V38() V43() Element of NAT
a . (y + 1) is ext-real V14() V15() integer set
a . y is ext-real V14() V15() integer set
nlist . y is ext-real V14() V15() integer set
(a . y) * (nlist . y) is ext-real V14() V15() integer set
(x + 1) + 1 is ext-real positive non negative non empty V7() V8() V9() V13() V14() V15() integer V38() V43() Element of NAT
a . ((x + 1) + 1) is ext-real V14() V15() integer set
y is ext-real non negative V7() V8() V9() V13() V14() V15() integer V38() V43() set
nlist . y is ext-real V14() V15() integer set
a . (x + 1) is ext-real V14() V15() integer set
m is ext-real non negative V7() V8() V9() V13() V14() V15() integer V38() V43() set
m + 1 is ext-real positive non negative non empty V7() V8() V9() V13() V14() V15() integer V38() V43() Element of NAT
a . (m + 1) is ext-real V14() V15() integer set
a . m is ext-real V14() V15() integer set
nlist . m is ext-real V14() V15() integer set
(a . m) * (nlist . m) is ext-real V14() V15() integer set
nlist . (x + 1) is ext-real V14() V15() integer set
(a . (x + 1)) * (nlist . (x + 1)) is ext-real V14() V15() integer set
x is ext-real non negative V7() V8() V9() V13() V14() V15() integer V38() V43() Element of NAT
x + 1 is ext-real positive non negative non empty 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() set
a . (x + 1) is ext-real V14() V15() integer set
nlist . y is ext-real V14() V15() integer set
nlist is V18() V21( NAT ) V22( INT ) Function-like V38() FinSequence-like FinSubsequence-like V60() V61() V62() FinSequence of INT
len nlist is ext-real non negative V7() V8() V9() V13() V14() V15() integer V38() V43() Element of NAT
a is V18() V21( NAT ) V22( INT ) Function-like V38() FinSequence-like FinSubsequence-like V60() V61() V62() FinSequence of INT
len a is ext-real non negative V7() V8() V9() V13() V14() V15() integer V38() V43() Element of NAT
a . 1 is ext-real V14() V15() integer set
(len nlist) - 1 is ext-real V14() V15() integer set
0 + 1 is ext-real positive non negative non empty V7() V8() V9() V13() V14() V15() integer V38() V43() Element of NAT
a . (0 + 1) is ext-real V14() V15() integer set
x is ext-real non negative V7() V8() V9() V13() V14() V15() integer V38() V43() set
nlist . x is ext-real V14() V15() integer set
(a . (0 + 1)) mod (nlist . x) is ext-real V14() V15() integer set
x is ext-real non negative V7() V8() V9() V13() V14() V15() integer V38() V43() Element of NAT
x + 1 is ext-real positive non negative non empty V7() V8() V9() V13() V14() V15() integer V38() V43() Element of NAT
a . (x + 1) is ext-real V14() V15() integer set
x + 1 is ext-real positive non negative non empty V7() V8() V9() V13() V14() V15() integer V38() V43() Element of NAT
(x + 1) + 1 is ext-real positive non negative non empty V7() V8() V9() V13() V14() V15() integer V38() V43() Element of NAT
a . ((x + 1) + 1) is ext-real V14() V15() integer set
(x + 1) + 1 is ext-real positive non negative non empty V7() V8() V9() V13() V14() V15() integer V38() V43() Element of NAT
a . ((x + 1) + 1) is ext-real V14() V15() integer set
nlist . 1 is ext-real V14() V15() integer set
(a . 1) * (nlist . 1) is ext-real V14() V15() integer set
y is ext-real non negative V7() V8() V9() V13() V14() V15() integer V38() V43() set
nlist . y is ext-real V14() V15() integer set
(a . ((x + 1) + 1)) mod (nlist . y) is ext-real V14() V15() integer set
y is ext-real non negative V7() V8() V9() V13() V14() V15() integer V38() V43() set
nlist . y is ext-real V14() V15() integer set
(a . ((x + 1) + 1)) mod (nlist . y) is ext-real V14() V15() integer set
y is ext-real non negative V7() V8() V9() V13() V14() V15() integer V38() V43() set
y + 1 is ext-real positive non negative non empty V7() V8() V9() V13() V14() V15() integer V38() V43() Element of NAT
a . (y + 1) is ext-real V14() V15() integer set
a . y is ext-real V14() V15() integer set
nlist . y is ext-real V14() V15() integer set
(a . y) * (nlist . y) is ext-real V14() V15() integer set
(x + 1) + 1 is ext-real positive non negative non empty V7() V8() V9() V13() V14() V15() integer V38() V43() Element of NAT
a . ((x + 1) + 1) is ext-real V14() V15() integer set
y is ext-real non negative V7() V8() V9() V13() V14() V15() integer V38() V43() set
nlist . y is ext-real V14() V15() integer set
(a . ((x + 1) + 1)) mod (nlist . y) is ext-real V14() V15() integer set
a . (x + 1) is ext-real V14() V15() integer set
nlist . (x + 1) is ext-real V14() V15() integer set
(a . (x + 1)) * (nlist . (x + 1)) is ext-real V14() V15() integer set
((a . (x + 1)) * (nlist . (x + 1))) mod (nlist . y) is ext-real V14() V15() integer set
(a . (x + 1)) mod (nlist . y) is ext-real V14() V15() integer set
(nlist . (x + 1)) mod (nlist . y) is ext-real V14() V15() integer set
((a . (x + 1)) mod (nlist . y)) * ((nlist . (x + 1)) mod (nlist . y)) is ext-real V14() V15() integer set
(((a . (x + 1)) mod (nlist . y)) * ((nlist . (x + 1)) mod (nlist . y))) mod (nlist . y) is ext-real V14() V15() integer set
((a . (x + 1)) mod (nlist . y)) * 0 is ext-real V14() V15() integer set
(((a . (x + 1)) mod (nlist . y)) * 0) mod (nlist . y) is ext-real V14() V15() integer set
a . (x + 1) is ext-real V14() V15() integer set
nlist . (x + 1) is ext-real V14() V15() integer set
(a . (x + 1)) * (nlist . (x + 1)) is ext-real V14() V15() integer set
((a . (x + 1)) * (nlist . (x + 1))) mod (nlist . y) is ext-real V14() V15() integer set
(a . (x + 1)) mod (nlist . y) is ext-real V14() V15() integer set
(nlist . (x + 1)) mod (nlist . y) is ext-real V14() V15() integer set
((a . (x + 1)) mod (nlist . y)) * ((nlist . (x + 1)) mod (nlist . y)) is ext-real V14() V15() integer set
(((a . (x + 1)) mod (nlist . y)) * ((nlist . (x + 1)) mod (nlist . y))) mod (nlist . y) is ext-real V14() V15() integer set
0 * ((nlist . (x + 1)) mod (nlist . y)) is ext-real V14() V15() integer set
(0 * ((nlist . (x + 1)) mod (nlist . y))) mod (nlist . y) is ext-real V14() V15() integer set
i is ext-real non negative V7() V8() V9() V13() V14() V15() integer V38() V43() set
i + 1 is ext-real positive non negative non empty V7() V8() V9() V13() V14() V15() integer V38() V43() Element of NAT
a . (i + 1) is ext-real V14() V15() integer set
a . i is ext-real V14() V15() integer set
nlist . i is ext-real V14() V15() integer set
(a . i) * (nlist . i) is ext-real V14() V15() integer set
x 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() set
x + 1 is ext-real positive non negative non empty V7() V8() V9() V13() V14() V15() integer V38() V43() Element of NAT
a . (x + 1) is ext-real V14() V15() integer set
nlist . y is ext-real V14() V15() integer set
(a . (x + 1)) mod (nlist . y) is ext-real V14() V15() integer set
nlist is non empty V18() V21( NAT ) V22([:INT,INT:]) Function-like V38() FinSequence-like FinSubsequence-like FinSequence of [:INT,INT:]
len nlist is ext-real positive non negative non empty V7() V8() V9() V13() V14() V15() integer V38() V43() Element of NAT
a is V18() V21( NAT ) V22( INT ) Function-like V38() FinSequence-like FinSubsequence-like V60() V61() V62() FinSequence of INT
len a is ext-real non negative V7() V8() V9() V13() V14() V15() integer V38() V43() Element of NAT
b is V18() V21( NAT ) V22( INT ) Function-like V38() FinSequence-like FinSubsequence-like V60() V61() V62() FinSequence of INT
len b is ext-real non negative V7() V8() V9() V13() V14() V15() integer V38() V43() Element of NAT
Seg (len nlist) is non empty V38() V45( len nlist) 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₁ <= len nlist ) } is set
x is ext-real non negative V7() V8() V9() V13() V14() V15() integer V38() V43() set
(nlist) is ext-real V14() V15() integer Element of INT
b . x is ext-real V14() V15() integer set
(nlist) mod (b . x) is ext-real V14() V15() integer set
a . x is ext-real V14() V15() integer set
(a . x) mod (b . x) 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 + 1 is ext-real positive non negative non empty V7() V8() V9() V13() V14() V15() integer V38() V43() Element of NAT
a is non empty V18() V21( NAT ) V22([:INT,INT:]) Function-like V38() FinSequence-like FinSubsequence-like FinSequence of [:INT,INT:]
len a is ext-real positive non negative non empty V7() V8() V9() V13() V14() V15() integer V38() V43() Element of NAT
Seg (len a) is non empty V38() V45( len a) 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₁ <= len a ) } is set
(a) is ext-real V14() V15() integer Element of INT
b is V18() V21( NAT ) V22( INT ) Function-like V38() FinSequence-like FinSubsequence-like V60() V61() V62() FinSequence of INT
len b is ext-real non negative V7() V8() V9() V13() V14() V15() integer V38() V43() Element of NAT
x is V18() V21( NAT ) V22( INT ) Function-like V38() FinSequence-like FinSubsequence-like V60() V61() V62() FinSequence of INT
len x is ext-real non negative V7() V8() V9() V13() V14() V15() integer V38() V43() Element of NAT
a . 1 is set
(a . 1) `1 is set
b . 1 is ext-real V14() V15() integer set
y is ext-real non negative V7() V8() V9() V13() V14() V15() integer V38() V43() set
x . y is ext-real V14() V15() integer set
(a) mod (x . y) is ext-real V14() V15() integer set
b . y is ext-real V14() V15() integer set
(b . y) mod (x . y) is ext-real V14() V15() integer set
a | nlist is V18() V21( NAT ) V22([:INT,INT:]) Function-like V38() FinSequence-like FinSubsequence-like FinSequence of [:INT,INT:]
Seg nlist is V38() V45(nlist) Element of bool NAT
{ b<sub>1</sub> where b<sub>1</sub> is ext-real non negative V7() V8() V9() V13() V14() V15() integer V38() V43() Element of NAT : ( 1 <= b<sub>1</sub> & b<sub>1</sub> <= nlist ) } is set
K96(a,(Seg nlist)) is V18() FinSubsequence-like set
b | nlist is V18() V21( NAT ) V22( INT ) Function-like V38() FinSequence-like FinSubsequence-like V60() V61() V62() FinSequence of INT
K96(b,(Seg nlist)) is V18() V22( INT ) FinSubsequence-like V60() V61() V62() set
x | nlist is V18() V21( NAT ) V22( INT ) Function-like V38() FinSequence-like FinSubsequence-like V60() V61() V62() FinSequence of INT
K96(x,(Seg nlist)) is V18() V22( INT ) FinSubsequence-like V60() V61() V62() set
m is V18() V21( NAT ) V22( INT ) Function-like V38() FinSequence-like FinSubsequence-like V60() V61() V62() FinSequence of INT
len m is ext-real non negative V7() V8() V9() V13() V14() V15() integer V38() V43() Element of NAT
y is V18() V21( NAT ) V22([:INT,INT:]) Function-like V38() FinSequence-like FinSubsequence-like FinSequence of [:INT,INT:]
len y is ext-real non negative V7() V8() V9() V13() V14() V15() integer V38() V43() Element of NAT
I0 is non empty V18() V21( NAT ) V22([:INT,INT:]) Function-like V38() FinSequence-like FinSubsequence-like FinSequence of [:INT,INT:]
dom I0 is Element of bool NAT
len I0 is ext-real positive non negative non empty V7() V8() V9() V13() V14() V15() integer V38() V43() Element of NAT
Seg (len I0) is non empty V38() V45( len I0) Element of bool NAT
{ b<sub>1</sub> where b<sub>1</sub> is ext-real non negative V7() V8() V9() V13() V14() V15() integer V38() V43() Element of NAT : ( 1 <= b<sub>1</sub> & b<sub>1</sub> <= len I0 ) } is set
i is V18() V21( NAT ) V22( INT ) Function-like V38() FinSequence-like FinSubsequence-like V60() V61() V62() FinSequence of INT
len i 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() set
i . m is ext-real V14() V15() integer set
x . m is ext-real V14() V15() integer set
m is ext-real non negative V7() V8() V9() V13() V14() V15() integer V38() V43() set
I0 . m is set
(I0 . m) `1 is set
m . m is ext-real V14() V15() integer set
(I0 . m) `2 is set
i . m is ext-real V14() V15() integer set
a . m is set
(a . m) `1 is set
b . m is ext-real V14() V15() integer set
(a . m) `2 is set
x . m is ext-real V14() V15() integer set
m is ext-real non negative V7() V8() V9() V13() V14() V15() integer V38() V43() set
l is ext-real non negative V7() V8() V9() V13() V14() V15() integer V38() V43() set
i . m is ext-real V14() V15() integer set
i . l is ext-real V14() V15() integer set
x . m is ext-real V14() V15() integer set
x . l is ext-real V14() V15() integer set
(I0) is ext-real V14() V15() integer Element of INT
m is ext-real non negative V7() V8() V9() V13() V14() V15() integer V38() V43() set
x . m is ext-real V14() V15() integer set
(I0) mod (x . m) is ext-real V14() V15() integer set
b . m is ext-real V14() V15() integer set
(b . m) mod (x . m) is ext-real V14() V15() integer set
m . m is ext-real V14() V15() integer set
i . m is ext-real V14() V15() integer set
(len a) - 1 is ext-real V14() V15() integer set
a . 1 is set
(a . 1) `1 is set
m is V18() V21( NAT ) V22( INT ) Function-like V38() FinSequence-like FinSubsequence-like V60() V61() V62() FinSequence of INT
len m is ext-real non negative V7() V8() V9() V13() V14() V15() integer V38() V43() Element of NAT
l is V18() V21( NAT ) V22( INT ) Function-like V38() FinSequence-like FinSubsequence-like V60() V61() V62() FinSequence of INT
len l is ext-real non negative V7() V8() V9() V13() V14() V15() integer V38() V43() Element of NAT
prodc is V18() V21( NAT ) V22( INT ) Function-like V38() FinSequence-like FinSubsequence-like V60() V61() V62() FinSequence of INT
len prodc is ext-real non negative V7() V8() V9() V13() V14() V15() integer V38() V43() Element of NAT
prodi is V18() V21( NAT ) V22( INT ) Function-like V38() FinSequence-like FinSubsequence-like V60() V61() V62() FinSequence of INT
len prodi is ext-real non negative V7() V8() V9() V13() V14() V15() integer V38() V43() Element of NAT
m . 1 is ext-real V14() V15() integer set
(len m) - 1 is ext-real V14() V15() integer set
M0 is ext-real V14() V15() integer Element of INT
a . (len m) is set
(a . (len m)) `2 is set
M is ext-real V14() V15() integer Element of INT
prodc . ((len m) - 1) is ext-real V14() V15() integer set
(prodc . ((len m) - 1)) * M0 is ext-real V14() V15() integer set
l . 1 is ext-real V14() V15() integer set
l . (len m) is ext-real V14() V15() integer set
(l . (len m)) mod M is ext-real V14() V15() integer set
1 + 1 is ext-real positive non negative non empty V7() V8() V9() V13() V14() V15() integer V38() V43() Element of NAT
(len x) - 1 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
l1 is ext-real non negative V7() V8() V9() V13() V14() V15() integer V38() V43() set
l1 + 1 is ext-real positive non negative non empty V7() V8() V9() V13() V14() V15() integer V38() V43() Element of NAT
m . (l1 + 1) is ext-real V14() V15() integer set
m . l1 is ext-real V14() V15() integer set
x . l1 is ext-real V14() V15() integer set
(m . l1) * (x . l1) is ext-real V14() V15() integer set
a . l1 is set
(a . l1) `2 is set
a . (l1 + 1) is set
(a . (l1 + 1)) `2 is set
prodi . l1 is ext-real V14() V15() integer set
prodc . l1 is ext-real V14() V15() integer set
nn1 is ext-real V14() V15() integer Element of INT
(m . l1) * nn1 is ext-real V14() V15() integer set
prodi1 is ext-real V14() V15() integer Element of INT
m1 is ext-real V14() V15() integer Element of INT
(prodi1,m1) is ext-real V14() V15() integer Element of INT
m . (len a) is ext-real V14() V15() integer set
x . (len a) is ext-real V14() V15() integer set
l | nlist is V18() V21( NAT ) V22( INT ) Function-like V38() FinSequence-like FinSubsequence-like V60() V61() V62() FinSequence of INT
K96(l,(Seg nlist)) is V18() V22( INT ) FinSubsequence-like V60() V61() V62() set
m | nlist is V18() V21( NAT ) V22( INT ) Function-like V38() FinSequence-like FinSubsequence-like V60() V61() V62() FinSequence of INT
K96(m,(Seg nlist)) is V18() V22( INT ) FinSubsequence-like V60() V61() V62() set
len (l | nlist) is ext-real non negative V7() V8() V9() V13() V14() V15() integer V38() V43() Element of NAT
dom (m | nlist) is Element of bool NAT
len (m | nlist) is ext-real non negative V7() V8() V9() V13() V14() V15() integer V38() V43() Element of NAT
Seg (len (m | nlist)) is V38() V45( len (m | nlist)) Element of bool NAT
{ b<sub>1</sub> where b<sub>1</sub> is ext-real non negative V7() V8() V9() V13() V14() V15() integer V38() V43() Element of NAT : ( 1 <= b<sub>1</sub> & b<sub>1</sub> <= len (m | nlist) ) } is set
1 - 1 is ext-real V14() V15() integer set
nlist - 1 is ext-real V14() V15() integer set
nn1 is ext-real non negative V7() V8() V9() V13() V14() V15() integer V38() V43() set
prodi | nn1 is V18() V21( NAT ) V22( INT ) Function-like V38() FinSequence-like FinSubsequence-like V60() V61() V62() FinSequence of INT
Seg nn1 is V38() V45(nn1) Element of bool NAT
{ b<sub>1</sub> where b<sub>1</sub> is ext-real non negative V7() V8() V9() V13() V14() V15() integer V38() V43() Element of NAT : ( 1 <= b<sub>1</sub> & b<sub>1</sub> <= nn1 ) } is set
K96(prodi,(Seg nn1)) is V18() V22( INT ) FinSubsequence-like V60() V61() V62() set
prodc | nn1 is V18() V21( NAT ) V22( INT ) Function-like V38() FinSequence-like FinSubsequence-like V60() V61() V62() FinSequence of INT
K96(prodc,(Seg nn1)) is V18() V22( INT ) FinSubsequence-like V60() V61() V62() set
nlist - 0 is ext-real non negative V14() V15() integer set
prodi1 is V18() V21( NAT ) V22( INT ) Function-like V38() FinSequence-like FinSubsequence-like V60() V61() V62() FinSequence of INT
len prodi1 is ext-real non negative V7() V8() V9() V13() V14() V15() integer V38() V43() Element of NAT
prodc1 is V18() V21( NAT ) V22( INT ) Function-like V38() FinSequence-like FinSubsequence-like V60() V61() V62() FinSequence of INT
len prodc1 is ext-real non negative V7() V8() V9() V13() V14() V15() integer V38() V43() Element of NAT
(l | nlist) . 1 is ext-real V14() V15() integer set
I0 . 1 is set
(I0 . 1) `1 is set
M01 is ext-real non negative V7() V8() V9() V13() V14() V15() integer V38() V43() set
(len (m | nlist)) - 1 is ext-real V14() V15() integer set
(m | nlist) . M01 is ext-real V14() V15() integer set
m . M01 is ext-real V14() V15() integer set
Seg (len (l | nlist)) is V38() V45( len (l | nlist)) 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₁ <= len (l | nlist) ) } is set
(l | nlist) . M01 is ext-real V14() V15() integer set
l . M01 is ext-real V14() V15() integer set
Seg (len prodi1) is V38() V45( len prodi1) 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₁ <= len prodi1 ) } is set
prodi1 . M01 is ext-real V14() V15() integer set
prodi . M01 is ext-real V14() V15() integer set
Seg (len prodc1) is V38() V45( len prodc1) 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₁ <= len prodc1 ) } is set
prodc1 . M01 is ext-real V14() V15() integer set
prodc . M01 is ext-real V14() V15() integer set
I0 . (len (m | nlist)) is set
a . (len (m | nlist)) is set
dom a is Element of bool NAT
(I0 . (len (m | nlist))) `2 is set
prodc1 . ((len (m | nlist)) - 1) is ext-real V14() V15() integer set
M01 is ext-real V14() V15() integer Element of INT
(prodc1 . ((len (m | nlist)) - 1)) * M01 is ext-real V14() V15() integer set
(len I0) - 1 is ext-real V14() V15() integer set
(m | nlist) . 1 is ext-real V14() V15() integer set
s is ext-real non negative V7() V8() V9() V13() V14() V15() integer V38() V43() set
I0 . s is set
(I0 . s) `2 is set
s + 1 is ext-real positive non negative non empty V7() V8() V9() V13() V14() V15() integer V38() V43() Element of NAT
(m | nlist) . (s + 1) is ext-real V14() V15() integer set
(m | nlist) . s is ext-real V14() V15() integer set
I0 . (s + 1) is set
(I0 . (s + 1)) `2 is set
prodi1 . s is ext-real V14() V15() integer set
prodc1 . s is ext-real V14() V15() integer set
m . s is ext-real V14() V15() integer set
prodi . s is ext-real V14() V15() integer set
prodc . s is ext-real V14() V15() integer set
((len (m | nlist)) - 1) + 1 is ext-real V14() V15() integer set
m . (s + 1) is ext-real V14() V15() integer set
a . s is set
a . (s + 1) is set
s is ext-real non negative V7() V8() V9() V13() V14() V15() integer V38() V43() set
s + 1 is ext-real positive non negative non empty V7() V8() V9() V13() V14() V15() integer V38() V43() Element of NAT
I0 . (s + 1) is set
(I0 . (s + 1)) `1 is set
(I0 . (s + 1)) `2 is set
(l | nlist) . s is ext-real V14() V15() integer set
prodi1 . s is ext-real V14() V15() integer set
(l | nlist) . (s + 1) is ext-real V14() V15() integer set
prodc1 . s is ext-real V14() V15() integer set
l . s is ext-real V14() V15() integer set
prodi . s is ext-real V14() V15() integer set
prodc . s is ext-real V14() V15() integer set
((len (m | nlist)) - 1) + 1 is ext-real V14() V15() integer set
l . (s + 1) is ext-real V14() V15() integer set
a . (s + 1) is set
(l | nlist) . (len (m | nlist)) is ext-real V14() V15() integer set
M1 is ext-real V14() V15() integer Element of INT
((l | nlist) . (len (m | nlist))) mod M1 is ext-real V14() V15() integer set
lm1 is ext-real non negative V7() V8() V9() V13() V14() V15() integer V38() V43() Element of NAT
a . lm1 is set
(a . lm1) `2 is set
lm1 + 1 is ext-real positive non negative non empty V7() V8() V9() V13() V14() V15() integer V38() V43() Element of NAT
m . (lm1 + 1) is ext-real V14() V15() integer set
m . lm1 is ext-real V14() V15() integer set
a . (lm1 + 1) is set
(a . (lm1 + 1)) `2 is set
prodi . lm1 is ext-real V14() V15() integer set
prodc . lm1 is ext-real V14() V15() integer set
x is ext-real V14() V15() integer Element of INT
(m . lm1) * x is ext-real V14() V15() integer set
y is ext-real V14() V15() integer Element of INT
d is ext-real V14() V15() integer Element of INT
(y,d) is ext-real V14() V15() integer Element of INT
(a . (lm1 + 1)) `1 is set
l . lm1 is ext-real V14() V15() integer set
l . (lm1 + 1) is ext-real V14() V15() integer set
u0 is ext-real V14() V15() integer Element of INT
u1 is ext-real V14() V15() integer Element of INT
u is ext-real V14() V15() integer Element of INT
u0 - (l . lm1) is ext-real V14() V15() integer set
(u0 - (l . lm1)) * (prodi . lm1) is ext-real V14() V15() integer set
((u0 - (l . lm1)) * (prodi . lm1)) mod u1 is ext-real V14() V15() integer set
u * (prodc . lm1) is ext-real V14() V15() integer set
(l . lm1) + (u * (prodc . lm1)) is ext-real V14() V15() integer set
l . ((len m) - 1) is ext-real V14() V15() integer set
u0 - (l . ((len m) - 1)) is ext-real V14() V15() integer set
(y,M0) is ext-real V14() V15() integer Element of INT
(u0 - (l . ((len m) - 1))) * (y,M0) is ext-real V14() V15() integer set
r is ext-real V14() V15() integer Element of INT
r * M0 is ext-real V14() V15() integer set
((u0 - (l . ((len m) - 1))) * (y,M0)) + (r * M0) is ext-real V14() V15() integer set
u * y is ext-real V14() V15() integer set
(l . ((len m) - 1)) + (u * y) is ext-real V14() V15() integer set
((l . ((len m) - 1)) + (u * y)) mod M is ext-real V14() V15() integer set
p is ext-real V14() V15() integer Element of INT
p * y is ext-real V14() V15() integer set
(l . ((len m) - 1)) + (p * y) is ext-real V14() V15() integer set
y0 is ext-real V14() V15() integer Element of INT
qr is ext-real V14() V15() integer Element of INT
y0 + qr is ext-real V14() V15() integer set
y * M0 is ext-real V14() V15() integer set
i is ext-real V14() V15() integer Element of INT
K1 is ext-real V14() V15() integer Element of INT
K1 * M is ext-real V14() V15() integer set
i + (K1 * M) is ext-real V14() V15() integer set
r + K1 is ext-real V14() V15() integer set
y0 * (y,M0) is ext-real V14() V15() integer set
(y0 * (y,M0)) * y is ext-real V14() V15() integer set
((y0 * (y,M0)) * y) + (p * y) is ext-real V14() V15() integer set
(I0) - (((y0 * (y,M0)) * y) + (p * y)) is ext-real V14() V15() integer set
K2 is ext-real V14() V15() integer Element of INT
K2 * M0 is ext-real V14() V15() integer set
(K2 * M0) * y is ext-real V14() V15() integer set
((I0) - (((y0 * (y,M0)) * y) + (p * y))) + ((K2 * M0) * y) is ext-real V14() V15() integer set
u0 * (y,M0) is ext-real V14() V15() integer set
(u0 * (y,M0)) * y is ext-real V14() V15() integer set
(((I0) - (((y0 * (y,M0)) * y) + (p * y))) + ((K2 * M0) * y)) + ((u0 * (y,M0)) * y) is ext-real V14() V15() integer set
(l . ((len m) - 1)) * (y,M0) is ext-real V14() V15() integer set
((l . ((len m) - 1)) * (y,M0)) * y is ext-real V14() V15() integer set
s is ext-real V14() V15() integer Element of INT
((l | nlist) . (len (m | nlist))) mod ((prodc1 . ((len (m | nlist)) - 1)) * M01) is ext-real V14() V15() integer set
(l | nlist) . (len (l | nlist)) is ext-real V14() V15() integer set
l . (len (l | nlist)) is ext-real V14() V15() integer set
2 - 1 is ext-real V14() V15() integer set
(a . (len (m | nlist))) `2 is set
a . ((len m) - 1) is set
(a . ((len m) - 1)) `2 is set
I0 . nn1 is set
(I0 . nn1) `2 is set
nn1 + 1 is ext-real positive non negative non empty V7() V8() V9() V13() V14() V15() integer V38() V43() Element of NAT
(m | nlist) . (nn1 + 1) is ext-real V14() V15() integer set
(m | nlist) . nn1 is ext-real V14() V15() integer set
I0 . (nn1 + 1) is set
(I0 . (nn1 + 1)) `2 is set
prodi1 . nn1 is ext-real V14() V15() integer set
prodc1 . nn1 is ext-real V14() V15() integer set
qr is ext-real V14() V15() integer Element of INT
((m | nlist) . nn1) * qr is ext-real V14() V15() integer set
y0 is ext-real V14() V15() integer Element of INT
p is ext-real V14() V15() integer Element of INT
(y0,p) is ext-real V14() V15() integer Element of INT
y0 * M01 is ext-real V14() V15() integer set
(l . ((len m) - 1)) mod (y0 * M01) is ext-real V14() V15() integer set
y0 * x is ext-real V14() V15() integer set
i is ext-real V14() V15() integer Element of INT
i * (y0 * M01) is ext-real V14() V15() integer set
(l . ((len m) - 1)) + (i * (y0 * M01)) is ext-real V14() V15() integer set
u * (y0 * x) is ext-real V14() V15() integer set
(l . ((len m) - 1)) + (u * (y0 * x)) is ext-real V14() V15() integer set
((l . ((len m) - 1)) + (u * (y0 * x))) mod ((prodc . ((len m) - 1)) * M0) is ext-real V14() V15() integer set
(y0 * x) * M0 is ext-real V14() V15() integer set
((l . ((len m) - 1)) + (u * (y0 * x))) mod ((y0 * x) * M0) is ext-real V14() V15() integer set
K1 is ext-real V14() V15() integer Element of INT
K1 * ((y0 * x) * M0) is ext-real V14() V15() integer set
((l . ((len m) - 1)) + (u * (y0 * x))) + (K1 * ((y0 * x) * M0)) is ext-real V14() V15() integer set
r + K1 is ext-real V14() V15() integer set
(I0) - (i * (y0 * M01)) is ext-real V14() V15() integer set
((I0) - (i * (y0 * M01))) + (u * (y0 * x)) is ext-real V14() V15() integer set
i * (y0 * x) is ext-real V14() V15() integer set
(I0) - (i * (y0 * x)) is ext-real V14() V15() integer set
((I0) - (i * (y0 * x))) + (u * (y0 * x)) is ext-real V14() V15() integer set
(l . ((len m) - 1)) * (y,M0) is ext-real V14() V15() integer set
((l . ((len m) - 1)) * (y,M0)) * y is ext-real V14() V15() integer set
i * y is ext-real V14() V15() integer set
(((l . ((len m) - 1)) * (y,M0)) * y) + (i * y) is ext-real V14() V15() integer set
(I0) - ((((l . ((len m) - 1)) * (y,M0)) * y) + (i * y)) is ext-real V14() V15() integer set
(r * M0) * y is ext-real V14() V15() integer set
((I0) - ((((l . ((len m) - 1)) * (y,M0)) * y) + (i * y))) + ((r * M0) * y) is ext-real V14() V15() integer set
u0 * (y,M0) is ext-real V14() V15() integer set
(u0 * (y,M0)) * y is ext-real V14() V15() integer set
(((I0) - ((((l . ((len m) - 1)) * (y,M0)) * y) + (i * y))) + ((r * M0) * y)) + ((u0 * (y,M0)) * y) is ext-real V14() V15() integer set
y * M0 is ext-real V14() V15() integer set
K1 * (y * M0) is ext-real V14() V15() integer set
((((I0) - ((((l . ((len m) - 1)) * (y,M0)) * y) + (i * y))) + ((r * M0) * y)) + ((u0 * (y,M0)) * y)) + (K1 * (y * M0)) is ext-real V14() V15() integer set
K2 is ext-real V14() V15() integer Element of INT
K2 * M0 is ext-real V14() V15() integer set
(K2 * M0) * y is ext-real V14() V15() integer set
((I0) - ((((l . ((len m) - 1)) * (y,M0)) * y) + (i * y))) + ((K2 * M0) * y) is ext-real V14() V15() integer set
(((I0) - ((((l . ((len m) - 1)) * (y,M0)) * y) + (i * y))) + ((K2 * M0) * y)) + ((u0 * (y,M0)) * y) is ext-real V14() V15() integer set
(l . ((len m) - 1)) * (y,M0) is ext-real V14() V15() integer set
((l . ((len m) - 1)) * (y,M0)) * y is ext-real V14() V15() integer set
u0 * (y,M0) is ext-real V14() V15() integer set
(u0 * (y,M0)) * y is ext-real V14() V15() integer set
(l . ((len m) - 1)) * (y,M0) is ext-real V14() V15() integer set
((l . ((len m) - 1)) * (y,M0)) * y is ext-real V14() V15() integer set
u0 * (y,M0) is ext-real V14() V15() integer set
(u0 * (y,M0)) * y is ext-real V14() V15() integer set
p is ext-real V14() V15() integer Element of INT
p * y is ext-real V14() V15() integer set
(((l . ((len m) - 1)) * (y,M0)) * y) + (p * y) is ext-real V14() V15() integer set
(I0) - ((((l . ((len m) - 1)) * (y,M0)) * y) + (p * y)) is ext-real V14() V15() integer set
qr is ext-real V14() V15() integer Element of INT
qr * M0 is ext-real V14() V15() integer set
(qr * M0) * y is ext-real V14() V15() integer set
((I0) - ((((l . ((len m) - 1)) * (y,M0)) * y) + (p * y))) + ((qr * M0) * y) is ext-real V14() V15() integer set
(((I0) - ((((l . ((len m) - 1)) * (y,M0)) * y) + (p * y))) + ((qr * M0) * y)) + ((u0 * (y,M0)) * y) is ext-real V14() V15() integer set
(l . ((len m) - 1)) + (p * y) is ext-real V14() V15() integer set
p is ext-real V14() V15() integer Element of INT
p * y is ext-real V14() V15() integer set
(((l . ((len m) - 1)) * (y,M0)) * y) + (p * y) is ext-real V14() V15() integer set
(I0) - ((((l . ((len m) - 1)) * (y,M0)) * y) + (p * y)) is ext-real V14() V15() integer set
qr is ext-real V14() V15() integer Element of INT
qr * M0 is ext-real V14() V15() integer set
(qr * M0) * y is ext-real V14() V15() integer set
((I0) - ((((l . ((len m) - 1)) * (y,M0)) * y) + (p * y))) + ((qr * M0) * y) is ext-real V14() V15() integer set
(((I0) - ((((l . ((len m) - 1)) * (y,M0)) * y) + (p * y))) + ((qr * M0) * y)) + ((u0 * (y,M0)) * y) is ext-real V14() V15() integer set
(l . ((len m) - 1)) + (p * y) is ext-real V14() V15() integer set
y mod M0 is ext-real V14() V15() integer set
y0 is ext-real V14() V15() integer Element of INT
y0 gcd M0 is ext-real non negative V7() V8() V9() V13() V14() V15() integer V38() V43() set
(M0,y0) is Element of [:INT,INT,INT:]
(M0,y0) `3_3 is ext-real V14() V15() integer Element of INT
((((l . ((len m) - 1)) * (y,M0)) * y) + (p * y)) mod M0 is ext-real V14() V15() integer set
(y,M0) * y is ext-real V14() V15() integer set
(l . ((len m) - 1)) * ((y,M0) * y) is ext-real V14() V15() integer set
((l . ((len m) - 1)) * ((y,M0) * y)) mod M0 is ext-real V14() V15() integer set
(p * y) mod M0 is ext-real V14() V15() integer set
(((l . ((len m) - 1)) * ((y,M0) * y)) mod M0) + ((p * y) mod M0) is ext-real V14() V15() integer set
((((l . ((len m) - 1)) * ((y,M0) * y)) mod M0) + ((p * y) mod M0)) mod M0 is ext-real V14() V15() integer set
(l . ((len m) - 1)) mod M0 is ext-real V14() V15() integer set
((y,M0) * y) mod M0 is ext-real V14() V15() integer set
((l . ((len m) - 1)) mod M0) * (((y,M0) * y) mod M0) is ext-real V14() V15() integer set
(((l . ((len m) - 1)) mod M0) * (((y,M0) * y) mod M0)) mod M0 is ext-real V14() V15() integer set
((((l . ((len m) - 1)) mod M0) * (((y,M0) * y) mod M0)) mod M0) + ((p * y) mod M0) is ext-real V14() V15() integer set
(((((l . ((len m) - 1)) mod M0) * (((y,M0) * y) mod M0)) mod M0) + ((p * y) mod M0)) mod M0 is ext-real V14() V15() integer set
1 mod M0 is ext-real V14() V15() integer set
((l . ((len m) - 1)) mod M0) * (1 mod M0) is ext-real V14() V15() integer set
(((l . ((len m) - 1)) mod M0) * (1 mod M0)) mod M0 is ext-real V14() V15() integer set
((((l . ((len m) - 1)) mod M0) * (1 mod M0)) mod M0) + ((p * y) mod M0) is ext-real V14() V15() integer set
(((((l . ((len m) - 1)) mod M0) * (1 mod M0)) mod M0) + ((p * y) mod M0)) mod M0 is ext-real V14() V15() integer set
(l . ((len m) - 1)) * 1 is ext-real V14() V15() integer set
((l . ((len m) - 1)) * 1) mod M0 is ext-real V14() V15() integer set
(((l . ((len m) - 1)) * 1) mod M0) + ((p * y) mod M0) is ext-real V14() V15() integer set
((((l . ((len m) - 1)) * 1) mod M0) + ((p * y) mod M0)) mod M0 is ext-real V14() V15() integer set
(I0) mod M0 is ext-real V14() V15() integer set
i is ext-real non negative V7() V8() V9() V13() V14() V15() integer V38() V43() set
x . i is ext-real V14() V15() integer set
(a) mod (x . i) is ext-real V14() V15() integer set
b . i is ext-real V14() V15() integer set
(b . i) mod (x . i) is ext-real V14() V15() integer set
qr * y is ext-real V14() V15() integer set
(qr * y) * M0 is ext-real V14() V15() integer set
u0 * ((y,M0) * y) is ext-real V14() V15() integer set
I0 is ext-real V14() V15() integer Element of INT
K1y is ext-real V14() V15() integer Element of INT
I0 + K1y is ext-real V14() V15() integer set
I0 mod (x . i) is ext-real V14() V15() integer set
(qr * y) mod M0 is ext-real V14() V15() integer set
M0 mod M0 is ext-real V14() V15() integer set
((qr * y) mod M0) * (M0 mod M0) is ext-real V14() V15() integer set
(((qr * y) mod M0) * (M0 mod M0)) mod M0 is ext-real V14() V15() integer set
K1 is ext-real V14() V15() integer Element of INT
((qr * y) mod M0) * K1 is ext-real V14() V15() integer set
(((qr * y) mod M0) * K1) mod M0 is ext-real V14() V15() integer set
K1 mod (x . i) is ext-real V14() V15() integer set
K2y is ext-real V14() V15() integer Element of INT
K2y mod (x . i) is ext-real V14() V15() integer set
K1y mod (x . i) is ext-real V14() V15() integer set
(K1 mod (x . i)) + (K1y mod (x . i)) is ext-real V14() V15() integer set
((K1 mod (x . i)) + (K1y mod (x . i))) mod (x . i) is ext-real V14() V15() integer set
K1 + K1y is ext-real V14() V15() integer set
(K1 + K1y) mod (x . i) is ext-real V14() V15() integer set
u0 mod (x . i) is ext-real V14() V15() integer set
((y,M0) * y) mod (x . i) is ext-real V14() V15() integer set
(u0 mod (x . i)) * (((y,M0) * y) mod (x . i)) is ext-real V14() V15() integer set
((u0 mod (x . i)) * (((y,M0) * y) mod (x . i))) mod (x . i) is ext-real V14() V15() integer set
1 mod (x . i) is ext-real V14() V15() integer set
(u0 mod (x . i)) * (1 mod (x . i)) is ext-real V14() V15() integer set
((u0 mod (x . i)) * (1 mod (x . i))) mod (x . i) is ext-real V14() V15() integer set
u0 * 1 is ext-real V14() V15() integer set
(u0 * 1) mod (x . i) is ext-real V14() V15() integer set
K2 is ext-real V14() V15() integer Element of INT
(a) + K2 is ext-real V14() V15() integer set
((a) + K2) mod (x . i) is ext-real V14() V15() integer set
(I0) mod (x . i) is ext-real V14() V15() integer set
((a) mod (x . i)) + ((I0) mod (x . i)) is ext-real V14() V15() integer set
(((a) mod (x . i)) + ((I0) mod (x . i))) mod (x . i) is ext-real V14() V15() integer set
(a) + (I0) is ext-real V14() V15() integer set
((a) + (I0)) mod (x . i) is ext-real V14() V15() integer set
(I0) + K2y is ext-real V14() V15() integer set
((I0) + K2y) mod (x . i) is ext-real V14() V15() integer set
((I0) mod (x . i)) + (K2y mod (x . i)) is ext-real V14() V15() integer set
(((I0) mod (x . i)) + (K2y mod (x . i))) mod (x . i) is ext-real V14() V15() integer set
(I0) + (b . i) is ext-real V14() V15() integer set
((I0) + (b . i)) mod (x . i) is ext-real V14() V15() integer set
LL is ext-real V14() V15() integer Element of INT
LL1 is ext-real V14() V15() integer Element of INT
bi is ext-real V14() V15() integer Element of INT
r is ext-real V14() V15() integer Element of INT
r * bi is ext-real V14() V15() integer set
LL1 + (r * bi) is ext-real V14() V15() integer set
LL2 is ext-real V14() V15() integer Element of INT
s is ext-real V14() V15() integer Element of INT
s * bi is ext-real V14() V15() integer set
LL2 + (s * bi) is ext-real V14() V15() integer set
s - r is ext-real V14() V15() integer set
LL3 is ext-real V14() V15() integer Element of INT
LL3 * (x . i) is ext-real V14() V15() integer set
(LL3 * (x . i)) mod (x . i) is ext-real V14() V15() integer set
LL3 mod (x . i) is ext-real V14() V15() integer set
(x . i) mod (x . i) is ext-real V14() V15() integer set
(LL3 mod (x . i)) * ((x . i) mod (x . i)) is ext-real V14() V15() integer set
((LL3 mod (x . i)) * ((x . i) mod (x . i))) mod (x . i) is ext-real V14() V15() integer set
(LL3 mod (x . i)) * K1 is ext-real V14() V15() integer set
((LL3 mod (x . i)) * K1) mod (x . i) is ext-real V14() V15() integer set
(s - r) * (x . i) is ext-real V14() V15() integer set
(b . i) + ((s - r) * (x . i)) is ext-real V14() V15() integer set
((b . i) + ((s - r) * (x . i))) mod (x . i) is ext-real V14() V15() integer set
((b . i) mod (x . i)) + (K1 mod (x . i)) is ext-real V14() V15() integer set
(((b . i) mod (x . i)) + (K1 mod (x . i))) mod (x . i) is ext-real V14() V15() integer set
(b . i) + K1 is ext-real V14() V15() integer set
((b . i) + K1) mod (x . i) is ext-real V14() V15() integer set
i + 1 is ext-real positive non negative non empty V7() V8() V9() V13() V14() V15() integer V38() V43() Element of NAT
(i + 1) - 1 is ext-real V14() V15() integer set
((l . ((len m) - 1)) * (y,M0)) + p is ext-real V14() V15() integer set
(qr * M0) + (u0 * (y,M0)) is ext-real V14() V15() integer set
y mod (x . i) is ext-real V14() V15() integer set
K1 is ext-real V14() V15() integer Element of INT
K1 * y is ext-real V14() V15() integer set
K2 is ext-real V14() V15() integer Element of INT
K2 * y is ext-real V14() V15() integer set
(K1 * y) mod (x . i) is ext-real V14() V15() integer set
K1 mod (x . i) is ext-real V14() V15() integer set
(K1 mod (x . i)) * (y mod (x . i)) is ext-real V14() V15() integer set
((K1 mod (x . i)) * (y mod (x . i))) mod (x . i) is ext-real V14() V15() integer set
0 mod (x . i) is ext-real V14() V15() integer set
(K2 * y) mod (x . i) is ext-real V14() V15() integer set
K2 mod (x . i) is ext-real V14() V15() integer set
(K2 mod (x . i)) * (y mod (x . i)) is ext-real V14() V15() integer set
((K2 mod (x . i)) * (y mod (x . i))) mod (x . i) is ext-real V14() V15() integer set
K1y is ext-real V14() V15() integer Element of INT
(a) + K1y is ext-real V14() V15() integer set
((a) + K1y) mod (x . i) is ext-real V14() V15() integer set
K1y mod (x . i) is ext-real V14() V15() integer set
((a) mod (x . i)) + (K1y mod (x . i)) is ext-real V14() V15() integer set
(((a) mod (x . i)) + (K1y mod (x . i))) mod (x . i) is ext-real V14() V15() integer set
I0 is ext-real V14() V15() integer Element of INT
(a) + I0 is ext-real V14() V15() integer set
((a) + I0) mod (x . i) is ext-real V14() V15() integer set
K2y is ext-real V14() V15() integer Element of INT
(I0) + K2y is ext-real V14() V15() integer set
((I0) + K2y) mod (x . i) is ext-real V14() V15() integer set
(I0) mod (x . i) is ext-real V14() V15() integer set
K2y mod (x . i) is ext-real V14() V15() integer set
((I0) mod (x . i)) + (K2y mod (x . i)) is ext-real V14() V15() integer set
(((I0) mod (x . i)) + (K2y mod (x . i))) mod (x . i) is ext-real V14() V15() integer set
(I0) + I0 is ext-real V14() V15() integer set
((I0) + I0) mod (x . i) is ext-real V14() V15() integer set
a is V18() V21( NAT ) V22( INT ) Function-like V38() FinSequence-like FinSubsequence-like V60() V61() V62() FinSequence of INT
len a is ext-real non negative V7() V8() V9() V13() V14() V15() integer V38() V43() Element of NAT
b is V18() V21( NAT ) V22( INT ) Function-like V38() FinSequence-like FinSubsequence-like V60() V61() V62() FinSequence of INT
len b is ext-real non negative V7() V8() V9() V13() V14() V15() integer V38() V43() Element of NAT
nlist is non empty V18() V21( NAT ) V22([:INT,INT:]) Function-like V38() FinSequence-like FinSubsequence-like FinSequence of [:INT,INT:]
len nlist is ext-real positive non negative non empty V7() V8() V9() V13() V14() V15() integer V38() V43() Element of NAT
Seg (len nlist) is non empty V38() V45( len nlist) 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₁ <= len nlist ) } is set
x is ext-real non negative V7() V8() V9() V13() V14() V15() integer V38() V43() set
(nlist) is ext-real V14() V15() integer Element of INT
b . x is ext-real V14() V15() integer set
(nlist) mod (b . x) is ext-real V14() V15() integer set
a . x is ext-real V14() V15() integer set
(a . x) mod (b . x) is ext-real V14() V15() integer set
nlist is ext-real V14() V15() integer Element of INT
b is ext-real V14() V15() integer Element of INT
nlist mod b is ext-real V14() V15() integer set
a is ext-real V14() V15() integer Element of INT
a mod b is ext-real V14() V15() integer set
x is ext-real V14() V15() integer Element of INT
nlist mod x is ext-real V14() V15() integer set
a mod x is ext-real V14() V15() integer set
b * x is ext-real V14() V15() integer set
nlist mod (b * x) is ext-real V14() V15() integer set
a mod (b * x) is ext-real V14() V15() integer set
a div b is ext-real V14() V15() integer set
a / b is ext-real V14() V15() set
[\(a / b)/] is ext-real V14() V15() integer set
(a div b) * b is ext-real V14() V15() integer set
((a div b) * b) + (a mod b) is ext-real V14() V15() integer set
nlist div x is ext-real V14() V15() integer set
nlist / x is ext-real V14() V15() set
[\(nlist / x)/] is ext-real V14() V15() integer set
(nlist div x) * x is ext-real V14() V15() integer set
((nlist div x) * x) + (nlist mod x) is ext-real V14() V15() integer set
nlist - a is ext-real V14() V15() integer set
nlist div b is ext-real V14() V15() integer set
nlist / b is ext-real V14() V15() set
[\(nlist / b)/] is ext-real V14() V15() integer set
(nlist div b) * b is ext-real V14() V15() integer set
((nlist div b) * b) + (nlist mod b) is ext-real V14() V15() integer set
(((nlist div b) * b) + (nlist mod b)) - (((a div b) * b) + (a mod b)) is ext-real V14() V15() integer set
(nlist div b) - (a div b) is ext-real V14() V15() integer set
((nlist div b) - (a div b)) * b is ext-real V14() V15() integer set
a div x is ext-real V14() V15() integer set
a / x is ext-real V14() V15() set
[\(a / x)/] is ext-real V14() V15() integer set
(a div x) * x is ext-real V14() V15() integer set
((a div x) * x) + (a mod x) is ext-real V14() V15() integer set
(((nlist div x) * x) + (nlist mod x)) - (((a div x) * x) + (a mod x)) is ext-real V14() V15() integer set
(nlist div x) - (a div x) is ext-real V14() V15() integer set
((nlist div x) - (a div x)) * x is ext-real V14() V15() integer set
i is ext-real V14() V15() integer set
(b * x) * i is ext-real V14() V15() integer set
a + ((b * x) * i) is ext-real V14() V15() integer set
(a + ((b * x) * i)) mod (b * x) is ext-real V14() V15() integer set
((b * x) * i) mod (b * x) is ext-real V14() V15() integer set
(a mod (b * x)) + (((b * x) * i) mod (b * x)) is ext-real V14() V15() integer set
((a mod (b * x)) + (((b * x) * i) mod (b * x))) mod (b * x) is ext-real V14() V15() integer set
(b * x) mod (b * x) is ext-real V14() V15() integer set
i mod (b * x) is ext-real V14() V15() integer set
((b * x) mod (b * x)) * (i mod (b * x)) is ext-real V14() V15() integer set
(((b * x) mod (b * x)) * (i mod (b * x))) mod (b * x) is ext-real V14() V15() integer set
(a mod (b * x)) + ((((b * x) mod (b * x)) * (i mod (b * x))) mod (b * x)) is ext-real V14() V15() integer set
((a mod (b * x)) + ((((b * x) mod (b * x)) * (i mod (b * x))) mod (b * x))) mod (b * x) is ext-real V14() V15() integer set
I0 is ext-real V14() V15() integer Element of INT
I0 * (i mod (b * x)) is ext-real V14() V15() integer set
(I0 * (i mod (b * x))) mod (b * x) is ext-real V14() V15() integer set
(a mod (b * x)) + ((I0 * (i mod (b * x))) mod (b * x)) is ext-real V14() V15() integer set
((a mod (b * x)) + ((I0 * (i mod (b * x))) mod (b * x))) mod (b * x) is ext-real V14() V15() integer set
a + I0 is ext-real V14() V15() integer set
(a + I0) mod (b * x) is ext-real V14() V15() integer set
nlist is ext-real V14() V15() integer Element of INT
a is ext-real V14() V15() integer Element of INT
b is non empty V18() V21( NAT ) V22( INT ) Function-like V38() FinSequence-like FinSubsequence-like V60() V61() V62() FinSequence of INT
len b is ext-real positive non negative non empty V7() V8() V9() V13() V14() V15() integer V38() V43() Element of NAT
Seg (len b) is non empty V38() V45( len b) 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₁ <= len b ) } is set
x is non empty V18() V21( NAT ) V22( INT ) Function-like V38() FinSequence-like FinSubsequence-like V60() V61() V62() FinSequence of INT
x . 1 is ext-real V14() V15() integer set
0 + 1 is ext-real positive non negative non empty V7() V8() V9() V13() V14() V15() integer V38() V43() Element of NAT
x . (0 + 1) is ext-real V14() V15() integer set
nlist mod (x . (0 + 1)) is ext-real V14() V15() integer set
a mod (x . (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
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 V14() V15() integer set
nlist mod (x . (m + 1)) is ext-real V14() V15() integer set
a mod (x . (m + 1)) 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
(m + 1) + 1 is ext-real positive non negative non empty V7() V8() V9() V13() V14() V15() integer V38() V43() Element of NAT
x . ((m + 1) + 1) is ext-real V14() V15() integer set
nlist mod (x . ((m + 1) + 1)) is ext-real V14() V15() integer set
a mod (x . ((m + 1) + 1)) is ext-real V14() V15() integer set
(m + 1) + 1 is ext-real positive non negative non empty V7() V8() V9() V13() V14() V15() integer V38() V43() Element of NAT
x . ((m + 1) + 1) is ext-real V14() V15() integer set
b . 1 is ext-real V14() V15() integer set
(x . 1) * (b . 1) is ext-real V14() V15() integer set
nlist mod (x . ((m + 1) + 1)) is ext-real V14() V15() integer set
a mod (x . ((m + 1) + 1)) is ext-real V14() V15() integer set
(m + 1) - 1 is ext-real V14() V15() integer set
(len b) - 1 is ext-real V14() V15() integer set
i is ext-real non negative V7() V8() V9() V13() V14() V15() integer V38() V43() set
i + 1 is ext-real positive non negative non empty V7() V8() V9() V13() V14() V15() integer V38() V43() Element of NAT
x . (i + 1) is ext-real V14() V15() integer set
x . i is ext-real V14() V15() integer set
b . i is ext-real V14() V15() integer set
(x . i) * (b . i) is ext-real V14() V15() integer set
(m + 1) + 1 is ext-real positive non negative non empty V7() V8() V9() V13() V14() V15() integer V38() V43() Element of NAT
x . ((m + 1) + 1) is ext-real V14() V15() integer set
x . (m + 1) is ext-real V14() V15() integer set
b . (m + 1) is ext-real V14() V15() integer set
(x . (m + 1)) * (b . (m + 1)) is ext-real V14() V15() integer set
nlist mod (b . (m + 1)) is ext-real V14() V15() integer set
a mod (b . (m + 1)) is ext-real V14() V15() integer set
nlist mod (x . ((m + 1) + 1)) is ext-real V14() V15() integer set
a mod (x . ((m + 1) + 1)) is ext-real V14() V15() integer set
i is ext-real non negative V7() V8() V9() V13() V14() V15() integer V38() V43() set
i + 1 is ext-real positive non negative non empty V7() V8() V9() V13() V14() V15() integer V38() V43() Element of NAT
x . (i + 1) is ext-real V14() V15() integer set
x . i is ext-real V14() V15() integer set
b . i is ext-real V14() V15() integer set
(x . i) * (b . i) 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
x . (m + 1) is ext-real V14() V15() integer set
nlist mod (x . (m + 1)) is ext-real V14() V15() integer set
a mod (x . (m + 1)) is ext-real V14() V15() integer set
nlist is V18() V21( NAT ) V22( INT ) Function-like V38() FinSequence-like FinSubsequence-like V60() V61() V62() FinSequence of INT
len nlist is ext-real non negative V7() V8() V9() V13() V14() V15() integer V38() V43() Element of NAT
Product nlist is V14() set
nlist . 1 is ext-real V14() V15() integer set
<*(nlist . 1)*> is non empty trivial V18() V21( NAT ) Function-like V38() V45(1) FinSequence-like FinSubsequence-like set
[1,(nlist . 1)] is V29() set
{[1,(nlist . 1)]} is non empty trivial V45(1) set
nlist is V18() V21( NAT ) V22( INT ) Function-like V38() FinSequence-like FinSubsequence-like V60() V61() V62() FinSequence of INT
len nlist is ext-real non negative V7() V8() V9() V13() V14() V15() integer V38() V43() Element of NAT
(len nlist) + 1 is ext-real positive non negative non empty V7() V8() V9() V13() V14() V15() integer V38() V43() Element of NAT
Product nlist is V14() set
<*1*> is non empty trivial V18() V21( NAT ) Function-like V38() V45(1) FinSequence-like FinSubsequence-like set
[1,1] is V29() set
{[1,1]} is non empty trivial V45(1) set
rng <*1*> is set
a is non empty V18() V21( NAT ) V22( INT ) Function-like V38() FinSequence-like FinSubsequence-like V60() V61() V62() FinSequence of INT
len a is ext-real positive non negative non empty V7() V8() V9() V13() V14() V15() integer V38() V43() Element of NAT
a . 1 is ext-real V14() V15() integer set
b is ext-real non negative V7() V8() V9() V13() V14() V15() integer V38() V43() set
b + 1 is ext-real positive non negative non empty V7() V8() V9() V13() V14() V15() integer V38() V43() Element of NAT
a . (b + 1) is ext-real V14() V15() integer set
a . b is ext-real V14() V15() integer set
nlist . b is ext-real V14() V15() integer set
(a . b) * (nlist . b) 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 + 1 is ext-real positive non negative non empty V7() V8() V9() V13() V14() V15() integer V38() V43() Element of NAT
a is V18() V21( NAT ) V22( INT ) Function-like V38() FinSequence-like FinSubsequence-like V60() V61() V62() FinSequence of INT
len a is ext-real non negative V7() V8() V9() V13() V14() V15() integer V38() V43() Element of NAT
(len a) + 1 is ext-real positive non negative non empty V7() V8() V9() V13() V14() V15() integer V38() V43() Element of NAT
Product a is V14() set
a | nlist is V18() V21( NAT ) V22( INT ) Function-like V38() FinSequence-like FinSubsequence-like V60() V61() V62() FinSequence of INT
Seg nlist is V38() V45(nlist) 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₁ <= nlist ) } is set
K96(a,(Seg nlist)) is V18() V22( INT ) FinSubsequence-like V60() V61() V62() set
len (a | nlist) is ext-real non negative V7() V8() V9() V13() V14() V15() integer V38() V43() Element of NAT
(len (a | nlist)) + 1 is ext-real positive non negative non empty V7() V8() V9() V13() V14() V15() integer V38() V43() Element of NAT
Product (a | nlist) is V14() set
x is non empty V18() V21( NAT ) V22( INT ) Function-like V38() FinSequence-like FinSubsequence-like V60() V61() V62() FinSequence of INT
len x is ext-real positive non negative non empty V7() V8() V9() V13() V14() V15() integer V38() V43() Element of NAT
x . 1 is ext-real V14() V15() integer set
x . ((len (a | nlist)) + 1) is ext-real V14() V15() integer set
a . (len a) is ext-real V14() V15() integer set
(Product (a | nlist)) * (a . (len a)) is set
<*((Product (a | nlist)) * (a . (len a)))*> is non empty trivial V18() V21( NAT ) Function-like V38() V45(1) FinSequence-like FinSubsequence-like set
[1,((Product (a | nlist)) * (a . (len a)))] is V29() set
{[1,((Product (a | nlist)) * (a . (len a)))]} is non empty trivial V45(1) set
x ^ <*((Product (a | nlist)) * (a . (len a)))*> is non empty V18() V21( NAT ) Function-like V38() FinSequence-like FinSubsequence-like set
rng <*((Product (a | nlist)) * (a . (len a)))*> is set
{((Product (a | nlist)) * (a . (len a)))} is non empty trivial V45(1) set
len (x ^ <*((Product (a | nlist)) * (a . (len a)))*>) is ext-real positive non negative non empty V7() V8() V9() V13() V14() V15() integer V38() V43() Element of NAT
len <*((Product (a | nlist)) * (a . (len a)))*> is ext-real positive non negative non empty V7() V8() V9() V13() V14() V15() integer V38() V43() Element of NAT
(len x) + (len <*((Product (a | nlist)) * (a . (len a)))*>) is ext-real positive non negative non empty V7() V8() V9() V13() V14() V15() integer V38() V43() Element of NAT
((len (a | nlist)) + 1) + 1 is ext-real positive non negative non empty V7() V8() V9() V13() V14() V15() integer V38() V43() Element of NAT
rng (x ^ <*((Product (a | nlist)) * (a . (len a)))*>) is set
rng x is V70() V71() V72() V74() Element of bool REAL
(rng x) \/ {((Product (a | nlist)) * (a . (len a)))} is non empty set
Seg (len x) is non empty V38() V45( len x) 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₁ <= len x ) } is set
dom x is Element of bool NAT
m is non empty V18() V21( NAT ) V22( INT ) Function-like V38() FinSequence-like FinSubsequence-like V60() V61() V62() FinSequence of INT
m . 1 is ext-real V14() V15() integer set
i is ext-real non negative V7() V8() V9() V13() V14() V15() integer V38() V43() set
i + 1 is ext-real positive non negative non empty V7() V8() V9() V13() V14() V15() integer V38() V43() Element of NAT
m . (i + 1) is ext-real V14() V15() integer set
m . i is ext-real V14() V15() integer set
a . i is ext-real V14() V15() integer set
(m . i) * (a . i) is ext-real V14() V15() integer set
m . ((len (a | nlist)) + 1) is ext-real V14() V15() integer set
dom <*((Product (a | nlist)) * (a . (len a)))*> is non empty trivial V45(1) Element of bool NAT
<*((Product (a | nlist)) * (a . (len a)))*> . 1 is set
x . (i + 1) is ext-real V14() V15() integer set
x . i is ext-real V14() V15() integer set
(a | nlist) . i is ext-real V14() V15() integer set
(x . i) * ((a | nlist) . i) is ext-real V14() V15() integer set
a | (nlist + 1) is V18() V21( NAT ) V22( INT ) Function-like V38() FinSequence-like FinSubsequence-like V60() V61() V62() FinSequence of INT
Seg (nlist + 1) is non empty V38() V45(nlist + 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₁ <= nlist + 1 ) } is set
K96(a,(Seg (nlist + 1))) is V18() V22( INT ) FinSubsequence-like V60() V61() V62() set
<*(a . (len a))*> is non empty trivial V18() V21( NAT ) Function-like V38() V45(1) FinSequence-like FinSubsequence-like set
[1,(a . (len a))] is V29() set
{[1,(a . (len a))]} is non empty trivial V45(1) set
(a | nlist) ^ <*(a . (len a))*> is non empty V18() V21( NAT ) Function-like V38() FinSequence-like FinSubsequence-like set
(x . ((len (a | nlist)) + 1)) * (a . (len a)) is ext-real V14() V15() integer set
x . (len a) is ext-real V14() V15() integer set
(x . (len a)) * (a . (len a)) is ext-real V14() V15() integer set
m . (len a) is ext-real V14() V15() integer set
(m . (len a)) * (a . (len a)) is ext-real V14() V15() integer set
m . ((len a) + 1) is ext-real V14() V15() integer set
nlist is V18() V21( NAT ) V22( INT ) Function-like V38() FinSequence-like FinSubsequence-like V60() V61() V62() FinSequence of INT
len nlist is ext-real non negative V7() V8() V9() V13() V14() V15() integer V38() V43() Element of NAT
(len nlist) + 1 is ext-real positive non negative non empty V7() V8() V9() V13() V14() V15() integer V38() V43() Element of NAT
Product nlist is V14() set
nlist is non empty V18() V21( NAT ) V22([:INT,INT:]) Function-like V38() FinSequence-like FinSubsequence-like FinSequence of [:INT,INT:]
len nlist is ext-real positive non negative non empty V7() V8() V9() V13() V14() V15() integer V38() V43() Element of NAT
Seg (len nlist) is non empty V38() V45( len nlist) 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₁ <= len nlist ) } is set
(nlist) is ext-real V14() V15() integer Element of INT
a is non empty V18() V21( NAT ) V22( INT ) Function-like V38() FinSequence-like FinSubsequence-like V60() V61() V62() FinSequence of INT
len a is ext-real positive non negative non empty V7() V8() V9() V13() V14() V15() integer V38() V43() Element of NAT
b is non empty V18() V21( NAT ) V22( INT ) Function-like V38() FinSequence-like FinSubsequence-like V60() V61() V62() FinSequence of INT
len b is ext-real positive non negative non empty V7() V8() V9() V13() V14() V15() integer V38() V43() Element of NAT
Product b is V14() set
x is ext-real V14() V15() integer Element of INT
y is ext-real V14() V15() integer Element of INT
(nlist) mod y is ext-real V14() V15() integer set
x mod y is ext-real V14() V15() integer set
m is ext-real non negative V7() V8() V9() V13() V14() V15() integer V38() V43() set
b . m is ext-real V14() V15() integer set
(nlist) mod (b . m) is ext-real V14() V15() integer set
x mod (b . m) is ext-real V14() V15() integer set
a . m is ext-real V14() V15() integer set
(a . m) mod (b . m) is ext-real V14() V15() integer set
b . 1 is ext-real V14() V15() integer set
(nlist) mod (b . 1) is ext-real V14() V15() integer set
x mod (b . 1) is ext-real V14() V15() integer set
(len b) + 1 is ext-real positive non negative non empty V7() V8() V9() V13() V14() V15() integer V38() V43() Element of NAT
m is non empty V18() V21( NAT ) V22( INT ) Function-like V38() FinSequence-like FinSubsequence-like V60() V61() V62() FinSequence of INT
len m is ext-real positive non negative non empty V7() V8() V9() V13() V14() V15() integer V38() V43() Element of NAT
m . 1 is ext-real V14() V15() integer set
m . ((len b) + 1) is ext-real V14() V15() integer set