:: GRAPHSP semantic presentation

REAL is non empty V5() non finite set
NAT is non empty V5() V17() V18() V19() non finite cardinal limit_cardinal Element of K32(REAL)
K32(REAL) is V5() non finite set
NAT is non empty V5() V17() V18() V19() non finite cardinal limit_cardinal set
K32(NAT) is V5() non finite set
K32(NAT) is V5() non finite set
K184(NAT) is V44() set
COMPLEX is non empty V5() non finite set
K362() is set
K32(K362()) is set
K32(K32(K362())) is set
K370() is Element of K32(K32(K362()))
Real>=0 is non empty set
RAT is non empty V5() non finite set
INT is non empty V5() non finite set
K33(COMPLEX,COMPLEX) is V5() non finite set
K32(K33(COMPLEX,COMPLEX)) is V5() non finite set
K33(K33(COMPLEX,COMPLEX),COMPLEX) is V5() non finite set
K32(K33(K33(COMPLEX,COMPLEX),COMPLEX)) is V5() non finite set
K33(REAL,REAL) is V5() non finite set
K32(K33(REAL,REAL)) is V5() non finite set
K33(K33(REAL,REAL),REAL) is V5() non finite set
K32(K33(K33(REAL,REAL),REAL)) is V5() non finite set
K33(RAT,RAT) is V5() non finite set
K32(K33(RAT,RAT)) is V5() non finite set
K33(K33(RAT,RAT),RAT) is V5() non finite set
K32(K33(K33(RAT,RAT),RAT)) is V5() non finite set
K33(INT,INT) is V5() non finite set
K32(K33(INT,INT)) is V5() non finite set
K33(K33(INT,INT),INT) is V5() non finite set
K32(K33(K33(INT,INT),INT)) is V5() non finite set
K33(NAT,NAT) is V5() non finite set
K33(K33(NAT,NAT),NAT) is V5() non finite set
K32(K33(K33(NAT,NAT),NAT)) is V5() non finite set
{} is empty Function-like functional V17() V18() V19() V21() V22() V23() V24() V25() finite V30() cardinal {} -element FinSequence-membered integer ext-real non positive non negative set
1 is non empty V17() V18() V19() V23() V24() V25() finite cardinal integer ext-real positive non negative Element of NAT
2 is non empty V17() V18() V19() V23() V24() V25() finite cardinal integer ext-real positive non negative Element of NAT
3 is non empty V17() V18() V19() V23() V24() V25() finite cardinal integer ext-real positive non negative Element of NAT
Seg 1 is non empty V5() finite 1 -element Element of K32(NAT)
0 is empty Function-like functional V17() V18() V19() V21() V22() V23() V24() V25() finite V30() cardinal {} -element FinSequence-membered integer ext-real non positive non negative Element of NAT
Real>=0 is non empty Element of K32(REAL)
{ b₁ where b₁ is V24() V25() ext-real Element of REAL : 0 <= b₁ } is set
n is Relation-like NAT -defined Function-like finite FinSequence-like FinSubsequence-like set
rng n is finite set
i is set
<*i*> is non empty V5() Relation-like NAT -defined Function-like constant finite 1 -element FinSequence-like FinSubsequence-like set
n ^ <*i*> is non empty Relation-like NAT -defined Function-like finite FinSequence-like FinSubsequence-like set
rng <*i*> is V5() finite set
{i} is non empty V5() finite 1 -element set
n is set
i is Relation-like NAT -defined n -valued Function-like finite FinSequence-like FinSubsequence-like FinSequence of n
len i is V17() V18() V19() V23() V24() V25() finite cardinal integer ext-real non negative Element of NAT
f is V24() V25() integer ext-real set
i . f is set
g is V17() V18() V19() V23() V24() V25() finite cardinal integer ext-real non negative Element of NAT
dom i is finite Element of K32(NAT)
n is set
i is Relation-like NAT -defined n -valued Function-like finite FinSequence-like FinSubsequence-like FinSequence of n
len i is V17() V18() V19() V23() V24() V25() finite cardinal integer ext-real non negative Element of NAT
f is V24() V25() integer ext-real set
i /. f is Element of n
i . f is set
g is V17() V18() V19() V23() V24() V25() finite cardinal integer ext-real non negative Element of NAT
dom i is finite Element of K32(NAT)
n is non empty MultiGraphStruct
the carrier' of n is set
i is Relation-like NAT -defined the carrier' of n -valued Function-like finite FinSequence-like FinSubsequence-like FinSequence of the carrier' of n
len i is V17() V18() V19() V23() V24() V25() finite cardinal integer ext-real non negative Element of NAT
i . 1 is set
f is Relation-like Function-like set
cost (i,f) is V24() V25() ext-real Element of REAL
f . (i . 1) is set
dom i is finite Element of K32(NAT)
RealSequence (i,f) is Relation-like NAT -defined REAL -valued Function-like finite FinSequence-like FinSubsequence-like V88() V89() V90() FinSequence of REAL
dom (RealSequence (i,f)) is finite Element of K32(NAT)
len (RealSequence (i,f)) is V17() V18() V19() V23() V24() V25() finite cardinal integer ext-real non negative Element of NAT
(RealSequence (i,f)) . 1 is V24() V25() ext-real Element of REAL
<*((RealSequence (i,f)) . 1)*> is non empty V5() Relation-like NAT -defined REAL -valued Function-like one-to-one constant finite 1 -element FinSequence-like FinSubsequence-like V88() V89() V90() V92() V93() V94() V95() FinSequence of REAL
Sum (RealSequence (i,f)) is V24() V25() ext-real Element of REAL
K440() is Relation-like K33(REAL,REAL) -defined REAL -valued Function-like total quasi_total V88() V89() V90() Element of K32(K33(K33(REAL,REAL),REAL))
K185(REAL,(RealSequence (i,f)),K440()) is V24() V25() ext-real Element of REAL
n is non empty MultiGraphStruct
the carrier' of n is set
i is set
<*i*> is non empty V5() Relation-like NAT -defined Function-like constant finite 1 -element FinSequence-like FinSubsequence-like set
len <*i*> is non empty V17() V18() V19() V23() V24() V25() finite cardinal integer ext-real positive non negative Element of NAT
n is V17() V18() V19() V23() V24() V25() finite cardinal integer ext-real non negative set
i is Relation-like NAT -defined Function-like finite FinSequence-like FinSubsequence-like set
len i is V17() V18() V19() V23() V24() V25() finite cardinal integer ext-real non negative Element of NAT
i . n is set
f is Relation-like NAT -defined Function-like finite FinSequence-like FinSubsequence-like set
i ^ f is Relation-like NAT -defined Function-like finite FinSequence-like FinSubsequence-like set
(i ^ f) . n is set
dom i is finite Element of K32(NAT)
n is V17() V18() V19() V23() V24() V25() finite cardinal integer ext-real non negative Element of NAT
f is Relation-like NAT -defined Function-like finite FinSequence-like FinSubsequence-like set
len f is V17() V18() V19() V23() V24() V25() finite cardinal integer ext-real non negative Element of NAT
f . n is set
i is Relation-like NAT -defined Function-like finite FinSequence-like FinSubsequence-like set
i ^ f is Relation-like NAT -defined Function-like finite FinSequence-like FinSubsequence-like set
len i is V17() V18() V19() V23() V24() V25() finite cardinal integer ext-real non negative Element of NAT
(len i) + n is V17() V18() V19() V23() V24() V25() finite cardinal integer ext-real non negative Element of NAT
(i ^ f) . ((len i) + n) is set
dom f is finite Element of K32(NAT)
n is non empty MultiGraphStruct
the carrier' of n is set
the Target of n is Relation-like the carrier' of n -defined the carrier of n -valued Function-like quasi_total Element of K32(K33( the carrier' of n, the carrier of n))
the carrier of n is set
K33( the carrier' of n, the carrier of n) is set
K32(K33( the carrier' of n, the carrier of n)) is set
the Source of n is Relation-like the carrier' of n -defined the carrier of n -valued Function-like quasi_total Element of K32(K33( the carrier' of n, the carrier of n))
i is Relation-like NAT -defined the carrier' of n -valued Function-like finite FinSequence-like FinSubsequence-like FinSequence of the carrier' of n
len i is V17() V18() V19() V23() V24() V25() finite cardinal integer ext-real non negative Element of NAT
i . (len i) is set
the Target of n . (i . (len i)) is set
f is Relation-like NAT -defined the carrier' of n -valued Function-like finite FinSequence-like FinSubsequence-like FinSequence of the carrier' of n
i ^ f is Relation-like NAT -defined the carrier' of n -valued Function-like finite FinSequence-like FinSubsequence-like FinSequence of the carrier' of n
len f is V17() V18() V19() V23() V24() V25() finite cardinal integer ext-real non negative Element of NAT
f . 1 is set
the Source of n . (f . 1) is set
g is Relation-like NAT -defined the carrier' of n -valued Function-like finite FinSequence-like FinSubsequence-like oriented Simple Chain of n
len g is V17() V18() V19() V23() V24() V25() finite cardinal integer ext-real non negative Element of NAT
g . (len g) is set
the Target of n . (g . (len g)) is set
g . 1 is set
the Source of n . (g . 1) is set
v1 is Relation-like NAT -defined the carrier of n -valued Function-like finite FinSequence-like FinSubsequence-like FinSequence of the carrier of n
len v1 is V17() V18() V19() V23() V24() V25() finite cardinal integer ext-real non negative Element of NAT
(len g) + 1 is non empty V17() V18() V19() V23() V24() V25() finite cardinal integer ext-real positive non negative Element of NAT
(len i) + (len f) is V17() V18() V19() V23() V24() V25() finite cardinal integer ext-real non negative Element of NAT
(len i) + 1 is non empty V17() V18() V19() V23() V24() V25() finite cardinal integer ext-real positive non negative Element of NAT
v1 /. 1 is Element of the carrier of n
1 + 1 is non empty V17() V18() V19() V23() V24() V25() finite cardinal integer ext-real positive non negative Element of NAT
v1 /. (1 + 1) is Element of the carrier of n
v1 . 1 is set
v1 /. (len i) is Element of the carrier of n
v1 /. ((len i) + 1) is Element of the carrier of n
g . (len i) is set
v1 /. (len g) is Element of the carrier of n
v1 /. ((len g) + 1) is Element of the carrier of n
v1 . (len v1) is set
((len i) + 1) + 1 is non empty V17() V18() V19() V23() V24() V25() finite cardinal integer ext-real positive non negative Element of NAT
v1 /. (((len i) + 1) + 1) is Element of the carrier of n
g . ((len i) + 1) is set
the Target of n . (g . (len i)) is set
v1 . ((len i) + 1) is set
the Source of n . (g . ((len i) + 1)) is set
n is non empty MultiGraphStruct
the carrier' of n is set
the carrier of n is set
i is Relation-like NAT -defined the carrier' of n -valued Function-like finite FinSequence-like FinSubsequence-like oriented Chain of n
f is set
g is Element of the carrier of n
G is Element of the carrier of n
{G} is non empty V5() finite 1 -element set
f \/ {G} is non empty set
vertices i is Element of K32( the carrier of n)
K32( the carrier of n) is set
(vertices i) \ {G} is Element of K32( the carrier of n)
((vertices i) \ {G}) \ {G} is Element of K32( the carrier of n)
{G} \/ {G} is non empty finite set
(vertices i) \ ({G} \/ {G}) is Element of K32( the carrier of n)
n is non empty MultiGraphStruct
the carrier' of n is set
the carrier of n is set
i is Relation-like NAT -defined the carrier' of n -valued Function-like finite FinSequence-like FinSubsequence-like oriented Chain of n
f is Relation-like Function-like set
g is set
G is Element of the carrier of n
W is Element of the carrier of n
{W} is non empty V5() finite 1 -element set
g \/ {W} is non empty set
v2 is Relation-like NAT -defined the carrier' of n -valued Function-like finite FinSequence-like FinSubsequence-like oriented Chain of n
cost (i,f) is V24() V25() ext-real Element of REAL
cost (v2,f) is V24() V25() ext-real Element of REAL
v2 is Relation-like NAT -defined the carrier' of n -valued Function-like finite FinSequence-like FinSubsequence-like oriented Chain of n
cost (v2,f) is V24() V25() ext-real Element of REAL
n is non empty MultiGraphStruct
the carrier' of n is set
the carrier of n is set
i is Relation-like NAT -defined the carrier' of n -valued Function-like finite FinSequence-like FinSubsequence-like oriented Chain of n
f is Relation-like NAT -defined the carrier' of n -valued Function-like finite FinSequence-like FinSubsequence-like oriented Chain of n
g is Relation-like Function-like set
cost (i,g) is V24() V25() ext-real Element of REAL
cost (f,g) is V24() V25() ext-real Element of REAL
G is set
W is Element of the carrier of n
v1 is Element of the carrier of n
n is non empty oriented MultiGraphStruct
the carrier of n is set
the carrier' of n is set
i is Element of the carrier of n
f is Element of the carrier of n
g is set
G is set
the Source of n is Relation-like the carrier' of n -defined the carrier of n -valued Function-like quasi_total Element of K32(K33( the carrier' of n, the carrier of n))
K33( the carrier' of n, the carrier of n) is set
K32(K33( the carrier' of n, the carrier of n)) is set
the Source of n . G is set
the Target of n is Relation-like the carrier' of n -defined the carrier of n -valued Function-like quasi_total Element of K32(K33( the carrier' of n, the carrier of n))
the Target of n . G is set
the Source of n . g is set
the Target of n . g is set
n is V17() V18() V19() V23() V24() V25() finite cardinal integer ext-real non negative Element of NAT
i is non empty MultiGraphStruct
the carrier' of i is set
the Source of i is Relation-like the carrier' of i -defined the carrier of i -valued Function-like quasi_total Element of K32(K33( the carrier' of i, the carrier of i))
the carrier of i is set
K33( the carrier' of i, the carrier of i) is set
K32(K33( the carrier' of i, the carrier of i)) is set
the Target of i is Relation-like the carrier' of i -defined the carrier of i -valued Function-like quasi_total Element of K32(K33( the carrier' of i, the carrier of i))
f is Relation-like NAT -defined the carrier' of i -valued Function-like finite FinSequence-like FinSubsequence-like FinSequence of the carrier' of i
len f is V17() V18() V19() V23() V24() V25() finite cardinal integer ext-real non negative Element of NAT
f . n is set
the Source of i . (f . n) is set
the Target of i . (f . n) is set
dom f is finite Element of K32(NAT)
n is non empty MultiGraphStruct
the carrier of n is set
the carrier' of n is set
i is set
f is set
i \/ f is set
g is Element of the carrier of n
G is Element of the carrier of n
the Source of n is Relation-like the carrier' of n -defined the carrier of n -valued Function-like quasi_total Element of K32(K33( the carrier' of n, the carrier of n))
K33( the carrier' of n, the carrier of n) is set
K32(K33( the carrier' of n, the carrier of n)) is set
the Target of n is Relation-like the carrier' of n -defined the carrier of n -valued Function-like quasi_total Element of K32(K33( the carrier' of n, the carrier of n))
v2 is Relation-like NAT -defined the carrier' of n -valued Function-like finite FinSequence-like FinSubsequence-like oriented Chain of n
len v2 is V17() V18() V19() V23() V24() V25() finite cardinal integer ext-real non negative Element of NAT
VG is V17() V18() V19() V23() V24() V25() finite cardinal integer ext-real non negative set
v2 . VG is set
the Source of n . (v2 . VG) is set
v2 . 1 is set
the Source of n . (v2 . 1) is set
VG is V17() V18() V19() V23() V24() V25() finite cardinal integer ext-real non negative set
v2 . VG is set
the Source of n . (v2 . VG) is set
Ug is V17() V18() V19() V23() V24() V25() finite cardinal integer ext-real non negative Element of NAT
v2 . Ug is set
the Source of n . (v2 . Ug) is set
v2 . (len v2) is set
the Target of n . (v2 . (len v2)) is set
Vg is Element of the carrier of n
Ug + 1 is non empty V17() V18() V19() V23() V24() V25() finite cardinal integer ext-real positive non negative Element of NAT
v2 . (Ug + 1) is set
the Source of n . (v2 . (Ug + 1)) is set
the Target of n . (v2 . Ug) is set
Vg is Element of the carrier of n
R is Element of the carrier of n
n is V17() V18() V19() V23() V24() V25() finite cardinal integer ext-real non negative Element of NAT
i is non empty MultiGraphStruct
the carrier' of i is set
the carrier of i is set
the Source of i is Relation-like the carrier' of i -defined the carrier of i -valued Function-like quasi_total Element of K32(K33( the carrier' of i, the carrier of i))
K33( the carrier' of i, the carrier of i) is set
K32(K33( the carrier' of i, the carrier of i)) is set
the Target of i is Relation-like the carrier' of i -defined the carrier of i -valued Function-like quasi_total Element of K32(K33( the carrier' of i, the carrier of i))
f is Relation-like NAT -defined the carrier' of i -valued Function-like finite FinSequence-like FinSubsequence-like FinSequence of the carrier' of i
len f is V17() V18() V19() V23() V24() V25() finite cardinal integer ext-real non negative Element of NAT
f . n is set
the Source of i . (f . n) is set
the Target of i . (f . n) is set
vertices f is Element of K32( the carrier of i)
K32( the carrier of i) is set
g is Element of the carrier of i
dom f is finite Element of K32(NAT)
n is non empty MultiGraphStruct
the carrier' of n is set
the carrier of n is set
i is Relation-like NAT -defined the carrier' of n -valued Function-like finite FinSequence-like FinSubsequence-like oriented Chain of n
f is set
g is set
f \/ g is set
G is Element of the carrier of n
W is Element of the carrier of n
the Source of n is Relation-like the carrier' of n -defined the carrier of n -valued Function-like quasi_total Element of K32(K33( the carrier' of n, the carrier of n))
K33( the carrier' of n, the carrier of n) is set
K32(K33( the carrier' of n, the carrier of n)) is set
the Target of n is Relation-like the carrier' of n -defined the carrier of n -valued Function-like quasi_total Element of K32(K33( the carrier' of n, the carrier of n))
vertices i is Element of K32( the carrier of n)
K32( the carrier of n) is set
len i is V17() V18() V19() V23() V24() V25() finite cardinal integer ext-real non negative Element of NAT
VG is V17() V18() V19() V23() V24() V25() finite cardinal integer ext-real non negative Element of NAT
VG + 1 is non empty V17() V18() V19() V23() V24() V25() finite cardinal integer ext-real positive non negative Element of NAT
i /. (VG + 1) is Element of the carrier' of n
vertices (i /. (VG + 1)) is set
Ug is Relation-like NAT -defined the carrier' of n -valued Function-like finite FinSequence-like FinSubsequence-like FinSequence of the carrier' of n
len Ug is V17() V18() V19() V23() V24() V25() finite cardinal integer ext-real non negative Element of NAT
Vg is Relation-like NAT -defined the carrier' of n -valued Function-like finite FinSequence-like FinSubsequence-like FinSequence of the carrier' of n
Ug ^ Vg is Relation-like NAT -defined the carrier' of n -valued Function-like finite FinSequence-like FinSubsequence-like FinSequence of the carrier' of n
vertices Ug is Element of K32( the carrier of n)
i . (VG + 1) is set
the Source of n . (i . (VG + 1)) is set
the Target of n . (i . (VG + 1)) is set
{( the Source of n . (i . (VG + 1))),( the Target of n . (i . (VG + 1)))} is non empty finite set
(vertices (i /. (VG + 1))) \/ f is set
R is Element of the carrier of n
M is Element of the carrier of n
M is Element of the carrier of n
1 + 0 is non empty V17() V18() V19() V23() V24() V25() finite cardinal integer ext-real positive non negative Element of NAT
Ug . VG is set
the Target of n . (Ug . VG) is set
RM is Element of the carrier of n
i . VG is set
the Target of n . (i . VG) is set
M is Element of the carrier of n
{W} is non empty V5() finite 1 -element set
(vertices i) \ {W} is Element of K32( the carrier of n)
n is Relation-like Function-like set
i is set
f is non empty finite MultiGraphStruct
the carrier' of f is finite set
the carrier of f is finite set
g is Relation-like NAT -defined the carrier' of f -valued Function-like finite FinSequence-like FinSubsequence-like oriented Chain of f
G is Relation-like NAT -defined the carrier' of f -valued Function-like finite FinSequence-like FinSubsequence-like oriented Chain of f
W is Element of the carrier of f
v1 is Element of the carrier of f
{v1} is non empty V5() finite 1 -element set
i \/ {v1} is non empty set
v2 is Element of the carrier of f
the Source of f is Relation-like the carrier' of f -defined the carrier of f -valued Function-like finite quasi_total Element of K32(K33( the carrier' of f, the carrier of f))
K33( the carrier' of f, the carrier of f) is finite set
K32(K33( the carrier' of f, the carrier of f)) is finite V30() set
the Target of f is Relation-like the carrier' of f -defined the carrier of f -valued Function-like finite quasi_total Element of K32(K33( the carrier' of f, the carrier of f))
R is Relation-like NAT -defined the carrier' of f -valued Function-like finite FinSequence-like FinSubsequence-like oriented Chain of f
M is Relation-like NAT -defined the carrier' of f -valued Function-like finite FinSequence-like FinSubsequence-like oriented Simple Chain of f
cost (M,n) is V24() V25() ext-real Element of REAL
cost (R,n) is V24() V25() ext-real Element of REAL
M . 1 is set
the Source of f . (M . 1) is set
len M is V17() V18() V19() V23() V24() V25() finite cardinal integer ext-real non negative Element of NAT
RM is V17() V18() V19() V23() V24() V25() finite cardinal integer ext-real non negative set
1 + RM is non empty V17() V18() V19() V23() V24() V25() finite cardinal integer ext-real positive non negative Element of NAT
vertices M is finite Element of K32( the carrier of f)
K32( the carrier of f) is finite V30() set
{v2} is non empty V5() finite 1 -element set
(vertices M) \ {v2} is finite Element of K32( the carrier of f)
M . (len M) is set
the Target of f . (M . (len M)) is set
cn is Relation-like NAT -defined Function-like finite FinSequence-like FinSubsequence-like set
len cn is V17() V18() V19() V23() V24() V25() finite cardinal integer ext-real non negative Element of NAT
mi is Relation-like NAT -defined Function-like finite FinSequence-like FinSubsequence-like set
len mi is V17() V18() V19() V23() V24() V25() finite cardinal integer ext-real non negative Element of NAT
cn ^ mi is Relation-like NAT -defined Function-like finite FinSequence-like FinSubsequence-like set
P is Relation-like NAT -defined the carrier' of f -valued Function-like finite FinSequence-like FinSubsequence-like oriented Simple Chain of f
P . 1 is set
the Source of f . (P . 1) is set
p is Element of the carrier of f
dom P is finite Element of K32(NAT)
((vertices M) \ {v2}) \ {v1} is finite Element of K32( the carrier of f)
{v2} \/ {v1} is non empty finite set
(vertices M) \ ({v2} \/ {v1}) is finite Element of K32( the carrier of f)
(vertices M) \ {v1} is finite Element of K32( the carrier of f)
((vertices M) \ {v1}) \ {v2} is finite Element of K32( the carrier of f)
cost (G,n) is V24() V25() ext-real Element of REAL
p is Relation-like NAT -defined the carrier' of f -valued Function-like finite FinSequence-like FinSubsequence-like oriented Simple Chain of f
len p is V17() V18() V19() V23() V24() V25() finite cardinal integer ext-real non negative Element of NAT
P is V17() V18() V19() V23() V24() V25() finite cardinal integer ext-real non negative Element of NAT
M . P is set
the Target of f . (M . P) is set
0 + 1 is non empty V17() V18() V19() V23() V24() V25() finite cardinal integer ext-real positive non negative Element of NAT
(len p) + 1 is non empty V17() V18() V19() V23() V24() V25() finite cardinal integer ext-real positive non negative Element of NAT
M . ((len p) + 1) is set
the Source of f . (M . ((len p) + 1)) is set
M . (len p) is set
the Target of f . (M . (len p)) is set
p . (len p) is set
the Target of f . (p . (len p)) is set
vertices p is finite Element of K32( the carrier of f)
(vertices p) \ {v1} is finite Element of K32( the carrier of f)
nk is V17() V18() V19() V23() V24() V25() finite cardinal integer ext-real non negative set
P + nk is V17() V18() V19() V23() V24() V25() finite cardinal integer ext-real non negative Element of NAT
m is Relation-like NAT -defined Function-like finite FinSequence-like FinSubsequence-like set
len m is V17() V18() V19() V23() V24() V25() finite cardinal integer ext-real non negative Element of NAT
j is Relation-like NAT -defined Function-like finite FinSequence-like FinSubsequence-like set
len j is V17() V18() V19() V23() V24() V25() finite cardinal integer ext-real non negative Element of NAT
m ^ j is Relation-like NAT -defined Function-like finite FinSequence-like FinSubsequence-like set
nj is Relation-like NAT -defined the carrier' of f -valued Function-like finite FinSequence-like FinSubsequence-like oriented Simple Chain of f
vertices nj is finite Element of K32( the carrier of f)
p ^ P is Relation-like NAT -defined the carrier' of f -valued Function-like finite FinSequence-like FinSubsequence-like FinSequence of the carrier' of f
vertices (p ^ P) is finite Element of K32( the carrier of f)
(vertices (p ^ P)) \ {v2} is finite Element of K32( the carrier of f)
v3 is Relation-like NAT -defined the carrier' of f -valued Function-like finite FinSequence-like FinSubsequence-like oriented Simple Chain of f
nj ^ v3 is Relation-like NAT -defined the carrier' of f -valued Function-like finite FinSequence-like FinSubsequence-like FinSequence of the carrier' of f
vertices (nj ^ v3) is finite Element of K32( the carrier of f)
(vertices (nj ^ v3)) \ {v2} is finite Element of K32( the carrier of f)
(vertices nj) \ {v2} is finite Element of K32( the carrier of f)
len P is V17() V18() V19() V23() V24() V25() finite cardinal integer ext-real non negative Element of NAT
vertices P is finite Element of K32( the carrier of f)
cost (g,n) is V24() V25() ext-real Element of REAL
e is Relation-like NAT -defined the carrier' of f -valued Function-like finite FinSequence-like FinSubsequence-like oriented Chain of f
cost (e,n) is V24() V25() ext-real Element of REAL
cost (v3,n) is V24() V25() ext-real Element of REAL
(vertices nj) \ {v1} is finite Element of K32( the carrier of f)
nj . 1 is set
the Source of f . (nj . 1) is set
p . 1 is set
the Source of f . (p . 1) is set
cost (p,n) is V24() V25() ext-real Element of REAL
cost (nj,n) is V24() V25() ext-real Element of REAL
(cost (nj,n)) + (cost (v3,n)) is V24() V25() ext-real Element of REAL
0 + (cost (nj,n)) is V24() V25() ext-real Element of REAL
len nj is V17() V18() V19() V23() V24() V25() finite cardinal integer ext-real non negative Element of NAT
nj . (len nj) is set
the Target of f . (nj . (len nj)) is set
p . P is set
the Target of f . (p . P) is set
len e is V17() V18() V19() V23() V24() V25() finite cardinal integer ext-real non negative Element of NAT
e ^ P is Relation-like NAT -defined the carrier' of f -valued Function-like finite FinSequence-like FinSubsequence-like FinSequence of the carrier' of f
pe is Relation-like NAT -defined the carrier' of f -valued Function-like finite FinSequence-like FinSubsequence-like oriented Chain of f
{p} is non empty V5() finite 1 -element set
i \/ {p} is non empty set
cost (G,n) is V24() V25() ext-real Element of REAL
cost (pe,n) is V24() V25() ext-real Element of REAL
cost (P,n) is V24() V25() ext-real Element of REAL
(cost (e,n)) + (cost (P,n)) is V24() V25() ext-real Element of REAL
(cost (p,n)) + (cost (P,n)) is V24() V25() ext-real Element of REAL
cost (G,n) is V24() V25() ext-real Element of REAL
cost (G,n) is V24() V25() ext-real Element of REAL
n is set
<*n*> is non empty V5() Relation-like NAT -defined Function-like constant finite 1 -element FinSequence-like FinSubsequence-like set
i is non empty oriented finite MultiGraphStruct
the carrier' of i is finite set
K33( the carrier' of i,Real>=0) is set
K32(K33( the carrier' of i,Real>=0)) is set
the carrier of i is finite set
f is Relation-like NAT -defined the carrier' of i -valued Function-like finite FinSequence-like FinSubsequence-like oriented Chain of i
g is Relation-like the carrier' of i -defined Real>=0 -valued Function-like finite total quasi_total Element of K32(K33( the carrier' of i,Real>=0))
G is Element of the carrier of i
{G} is non empty V5() finite 1 -element set
W is Element of the carrier of i
len f is V17() V18() V19() V23() V24() V25() finite cardinal integer ext-real non negative Element of NAT
vertices f is finite Element of K32( the carrier of i)
K32( the carrier of i) is finite V30() set
f /. 1 is Element of the carrier' of i
vertices (f /. 1) is set
the Source of i is Relation-like the carrier' of i -defined the carrier of i -valued Function-like finite quasi_total Element of K32(K33( the carrier' of i, the carrier of i))
K33( the carrier' of i, the carrier of i) is finite set
K32(K33( the carrier' of i, the carrier of i)) is finite V30() set
the Target of i is Relation-like the carrier' of i -defined the carrier of i -valued Function-like finite quasi_total Element of K32(K33( the carrier' of i, the carrier of i))
the Source of i . n is set
the Target of i . n is set
Ug is Relation-like NAT -defined the carrier' of i -valued Function-like finite FinSequence-like FinSubsequence-like oriented Chain of i
Vg is Relation-like NAT -defined the carrier' of i -valued Function-like finite FinSequence-like FinSubsequence-like oriented Simple Chain of i
vertices Vg is finite Element of K32( the carrier of i)
len Vg is V17() V18() V19() V23() V24() V25() finite cardinal integer ext-real non negative Element of NAT
M is V17() V18() V19() V23() V24() V25() finite cardinal integer ext-real non negative set
1 + M is non empty V17() V18() V19() V23() V24() V25() finite cardinal integer ext-real positive non negative Element of NAT
Vg . (len Vg) is set
the Target of i . (Vg . (len Vg)) is set
{W} is non empty V5() finite 1 -element set
Vg . 1 is set
the Source of i . (Vg . 1) is set
{G} \/ {W} is non empty finite set
{G,W} is non empty finite set
RM is Relation-like NAT -defined Function-like finite FinSequence-like FinSubsequence-like set
len RM is V17() V18() V19() V23() V24() V25() finite cardinal integer ext-real non negative Element of NAT
cn is Relation-like NAT -defined Function-like finite FinSequence-like FinSubsequence-like set
len cn is V17() V18() V19() V23() V24() V25() finite cardinal integer ext-real non negative Element of NAT
RM ^ cn is Relation-like NAT -defined Function-like finite FinSequence-like FinSubsequence-like set
(vertices Vg) \ {W} is finite Element of K32( the carrier of i)
{W} \/ {G} is non empty finite set
p is Relation-like NAT -defined the carrier' of i -valued Function-like finite FinSequence-like FinSubsequence-like oriented Simple Chain of i
p . 1 is set
the Source of i . (p . 1) is set
mi is Relation-like NAT -defined the carrier' of i -valued Function-like finite FinSequence-like FinSubsequence-like oriented Simple Chain of i
len mi is V17() V18() V19() V23() V24() V25() finite cardinal integer ext-real non negative Element of NAT
P is Element of the carrier of i
vertices p is finite Element of K32( the carrier of i)
mi ^ p is Relation-like NAT -defined the carrier' of i -valued Function-like finite FinSequence-like FinSubsequence-like FinSequence of the carrier' of i
vertices (mi ^ p) is finite Element of K32( the carrier of i)
len p is V17() V18() V19() V23() V24() V25() finite cardinal integer ext-real non negative Element of NAT
mi . (len mi) is set
the Target of i . (mi . (len mi)) is set
(len mi) + 1 is non empty V17() V18() V19() V23() V24() V25() finite cardinal integer ext-real positive non negative Element of NAT
Vg . ((len mi) + 1) is set
the Source of i . (Vg . ((len mi) + 1)) is set
Vg . (len mi) is set
the Target of i . (Vg . (len mi)) is set
0 + 1 is non empty V17() V18() V19() V23() V24() V25() finite cardinal integer ext-real positive non negative Element of NAT
Vg /. 1 is Element of the carrier' of i
cost (f,g) is V24() V25() ext-real Element of REAL
cost (Ug,g) is V24() V25() ext-real Element of REAL
f . 1 is set
(vertices f) \ {W} is finite Element of K32( the carrier of i)
({G} \/ {W}) \ {W} is finite Element of K32(({G} \/ {W}))
K32(({G} \/ {W})) is finite V30() set
{G} \ {W} is finite Element of K32({G})
K32({G}) is finite V30() set
n is set
<*n*> is non empty V5() Relation-like NAT -defined Function-like constant finite 1 -element FinSequence-like FinSubsequence-like set
i is set
f is non empty oriented finite MultiGraphStruct
the carrier' of f is finite set
K33( the carrier' of f,Real>=0) is set
K32(K33( the carrier' of f,Real>=0)) is set
the carrier of f is finite set
g is Relation-like NAT -defined the carrier' of f -valued Function-like finite FinSequence-like FinSubsequence-like oriented Chain of f
g ^ <*n*> is non empty Relation-like NAT -defined Function-like finite FinSequence-like FinSubsequence-like set
G is Relation-like NAT -defined the carrier' of f -valued Function-like finite FinSequence-like FinSubsequence-like oriented Chain of f
W is Relation-like the carrier' of f -defined Real>=0 -valued Function-like finite total quasi_total Element of K32(K33( the carrier' of f,Real>=0))
v1 is Element of the carrier of f
v2 is Element of the carrier of f
{v2} is non empty V5() finite 1 -element set
i \/ {v2} is non empty set
VG is Element of the carrier of f
len g is V17() V18() V19() V23() V24() V25() finite cardinal integer ext-real non negative Element of NAT
the Source of f is Relation-like the carrier' of f -defined the carrier of f -valued Function-like finite quasi_total Element of K32(K33( the carrier' of f, the carrier of f))
K33( the carrier' of f, the carrier of f) is finite set
K32(K33( the carrier' of f, the carrier of f)) is finite V30() set
the Target of f is Relation-like the carrier' of f -defined the carrier of f -valued Function-like finite quasi_total Element of K32(K33( the carrier' of f, the carrier of f))
cn is Relation-like NAT -defined the carrier' of f -valued Function-like finite FinSequence-like FinSubsequence-like oriented Chain of f
mi is Relation-like NAT -defined the carrier' of f -valued Function-like finite FinSequence-like FinSubsequence-like oriented Simple Chain of f
vertices mi is finite Element of K32( the carrier of f)
K32( the carrier of f) is finite V30() set
len mi is V17() V18() V19() V23() V24() V25() finite cardinal integer ext-real non negative Element of NAT
mi . (len mi) is set
the Target of f . (mi . (len mi)) is set
{VG} is non empty V5() finite 1 -element set
(vertices mi) \ {VG} is finite Element of K32( the carrier of f)
P is V17() V18() V19() V23() V24() V25() finite cardinal integer ext-real non negative set
1 + P is non empty V17() V18() V19() V23() V24() V25() finite cardinal integer ext-real positive non negative Element of NAT
p is Relation-like NAT -defined Function-like finite FinSequence-like FinSubsequence-like set
len p is V17() V18() V19() V23() V24() V25() finite cardinal integer ext-real non negative Element of NAT
P is Relation-like NAT -defined Function-like finite FinSequence-like FinSubsequence-like set
len P is V17() V18() V19() V23() V24() V25() finite cardinal integer ext-real non negative Element of NAT
p ^ P is Relation-like NAT -defined Function-like finite FinSequence-like FinSubsequence-like set
m is Relation-like NAT -defined the carrier' of f -valued Function-like finite FinSequence-like FinSubsequence-like oriented Simple Chain of f
m . 1 is set
the Source of f . (m . 1) is set
mi . 1 is set
the Source of f . (mi . 1) is set
nk is Relation-like NAT -defined the carrier' of f -valued Function-like finite FinSequence-like FinSubsequence-like oriented Simple Chain of f
1 + 0 is non empty V17() V18() V19() V23() V24() V25() finite cardinal integer ext-real positive non negative Element of NAT
len nk is V17() V18() V19() V23() V24() V25() finite cardinal integer ext-real non negative Element of NAT
the Source of f . (mi . (len mi)) is set
mi . (len nk) is set
the Target of f . (mi . (len nk)) is set
nk . (len nk) is set
the Target of f . (nk . (len nk)) is set
j is Element of the carrier of f
len m is V17() V18() V19() V23() V24() V25() finite cardinal integer ext-real non negative Element of NAT
vertices nk is finite Element of K32( the carrier of f)
(vertices nk) \ {VG} is finite Element of K32( the carrier of f)
nk ^ m is Relation-like NAT -defined the carrier' of f -valued Function-like finite FinSequence-like FinSubsequence-like FinSequence of the carrier' of f
vertices (nk ^ m) is finite Element of K32( the carrier of f)
(vertices nk) \ {v2} is finite Element of K32( the carrier of f)
(i \/ {v2}) \ {v2} is Element of K32((i \/ {v2}))
K32((i \/ {v2})) is set
i \ {v2} is Element of K32(i)
K32(i) is set
m /. 1 is Element of the carrier' of f
the Source of f . n is set
the Target of f . n is set
cost (G,W) is V24() V25() ext-real Element of REAL
cost (g,W) is V24() V25() ext-real Element of REAL
cost (m,W) is V24() V25() ext-real Element of REAL
(cost (g,W)) + (cost (m,W)) is V24() V25() ext-real Element of REAL
nk . 1 is set
the Source of f . (nk . 1) is set
cost (nk,W) is V24() V25() ext-real Element of REAL
cost (mi,W) is V24() V25() ext-real Element of REAL
cost (cn,W) is V24() V25() ext-real Element of REAL
(cost (nk,W)) + (cost (m,W)) is V24() V25() ext-real Element of REAL
Vg is Relation-like NAT -defined the carrier' of f -valued Function-like finite FinSequence-like FinSubsequence-like FinSequence of the carrier' of f
len Vg is V17() V18() V19() V23() V24() V25() finite cardinal integer ext-real non negative Element of NAT
Vg . 1 is set
n is set
i is set
n \/ i is set
f is non empty oriented finite MultiGraphStruct
the carrier' of f is finite set
K33( the carrier' of f,Real>=0) is set
K32(K33( the carrier' of f,Real>=0)) is set
the carrier of f is finite set
g is Relation-like NAT -defined the carrier' of f -valued Function-like finite FinSequence-like FinSubsequence-like oriented Chain of f
G is Relation-like the carrier' of f -defined Real>=0 -valued Function-like finite total quasi_total Element of K32(K33( the carrier' of f,Real>=0))
W is Element of the carrier of f
v1 is Element of the carrier of f
v2 is Relation-like NAT -defined the carrier' of f -valued Function-like finite FinSequence-like FinSubsequence-like oriented Chain of f
cost (g,G) is V24() V25() ext-real Element of REAL
cost (v2,G) is V24() V25() ext-real Element of REAL
v2 is Relation-like NAT -defined the carrier' of f -valued Function-like finite FinSequence-like FinSubsequence-like oriented Chain of f
cost (v2,G) is V24() V25() ext-real Element of REAL
n is Relation-like NAT -defined REAL -valued Function-like finite FinSequence-like FinSubsequence-like V88() V89() V90() FinSequence of REAL
i is set
f is V24() V25() ext-real Element of REAL
n +* (i,f) is Relation-like Function-like set
rng (n +* (i,f)) is set
g is set
rng n is finite V99() V100() V101() Element of K32(REAL)
{f} is non empty V5() finite 1 -element Element of K32(REAL)
(rng n) \/ {f} is non empty finite Element of K32(REAL)
dom (n +* (i,f)) is set
dom n is finite Element of K32(NAT)
len n is V17() V18() V19() V23() V24() V25() finite cardinal integer ext-real non negative Element of NAT
Seg (len n) is finite len n -element Element of K32(NAT)
f is Relation-like NAT -defined REAL -valued Function-like finite FinSequence-like FinSubsequence-like V88() V89() V90() FinSequence of REAL
n is V17() V18() V19() V23() V24() V25() finite cardinal integer ext-real non negative Element of NAT
i is V17() V18() V19() V23() V24() V25() finite cardinal integer ext-real non negative Element of NAT
(f,n,i) is Relation-like NAT -defined REAL -valued Function-like finite FinSequence-like FinSubsequence-like V88() V89() V90() FinSequence of REAL
g is V24() V25() ext-real Element of REAL
((f,n,i),i,g) is Relation-like NAT -defined REAL -valued Function-like finite FinSequence-like FinSubsequence-like V88() V89() V90() FinSequence of REAL
REAL * is non empty functional FinSequence-membered M15( REAL )
n is V17() V18() V19() V23() V24() V25() finite cardinal integer ext-real non negative Element of NAT
i is V17() V18() V19() V23() V24() V25() finite cardinal integer ext-real non negative Element of NAT
f is Relation-like NAT -defined REAL -valued Function-like finite FinSequence-like FinSubsequence-like V88() V89() V90() Element of REAL *
dom f is finite Element of K32(NAT)
g is V24() V25() ext-real Element of REAL
(n,i,f,g) is Relation-like NAT -defined REAL -valued Function-like finite FinSequence-like FinSubsequence-like V88() V89() V90() FinSequence of REAL
(f,n,i) is Relation-like NAT -defined REAL -valued Function-like finite FinSequence-like FinSubsequence-like V88() V89() V90() FinSequence of REAL
((f,n,i),i,g) is Relation-like NAT -defined REAL -valued Function-like finite FinSequence-like FinSubsequence-like V88() V89() V90() FinSequence of REAL
(n,i,f,g) . n is V24() V25() ext-real Element of REAL
(f,n,i) . n is V24() V25() ext-real Element of REAL
n is V17() V18() V19() V23() V24() V25() finite cardinal integer ext-real non negative Element of NAT
i is V17() V18() V19() V23() V24() V25() finite cardinal integer ext-real non negative Element of NAT
f is V17() V18() V19() V23() V24() V25() finite cardinal integer ext-real non negative Element of NAT
g is Relation-like NAT -defined REAL -valued Function-like finite FinSequence-like FinSubsequence-like V88() V89() V90() Element of REAL *
g . n is V24() V25() ext-real Element of REAL
G is V24() V25() ext-real Element of REAL
(i,f,g,G) is Relation-like NAT -defined REAL -valued Function-like finite FinSequence-like FinSubsequence-like V88() V89() V90() FinSequence of REAL
(g,i,f) is Relation-like NAT -defined REAL -valued Function-like finite FinSequence-like FinSubsequence-like V88() V89() V90() FinSequence of REAL
((g,i,f),f,G) is Relation-like NAT -defined REAL -valued Function-like finite FinSequence-like FinSubsequence-like V88() V89() V90() FinSequence of REAL
(i,f,g,G) . n is V24() V25() ext-real Element of REAL
(g,i,f) . n is V24() V25() ext-real Element of REAL
n is V17() V18() V19() V23() V24() V25() finite cardinal integer ext-real non negative Element of NAT
i is V17() V18() V19() V23() V24() V25() finite cardinal integer ext-real non negative Element of NAT
f is Relation-like NAT -defined REAL -valued Function-like finite FinSequence-like FinSubsequence-like V88() V89() V90() Element of REAL *
dom f is finite Element of K32(NAT)
g is V24() V25() ext-real Element of REAL
(i,n,f,g) is Relation-like NAT -defined REAL -valued Function-like finite FinSequence-like FinSubsequence-like V88() V89() V90() FinSequence of REAL
(f,i,n) is Relation-like NAT -defined REAL -valued Function-like finite FinSequence-like FinSubsequence-like V88() V89() V90() FinSequence of REAL
((f,i,n),n,g) is Relation-like NAT -defined REAL -valued Function-like finite FinSequence-like FinSubsequence-like V88() V89() V90() FinSequence of REAL
(i,n,f,g) . n is V24() V25() ext-real Element of REAL
dom (f,i,n) is finite Element of K32(NAT)
n is V17() V18() V19() V23() V24() V25() finite cardinal integer ext-real non negative Element of NAT
i is V17() V18() V19() V23() V24() V25() finite cardinal integer ext-real non negative Element of NAT
f is Relation-like NAT -defined REAL -valued Function-like finite FinSequence-like FinSubsequence-like V88() V89() V90() Element of REAL *
dom f is finite Element of K32(NAT)
g is V24() V25() ext-real Element of REAL
(n,i,f,g) is Relation-like NAT -defined REAL -valued Function-like finite FinSequence-like FinSubsequence-like V88() V89() V90() FinSequence of REAL
(f,n,i) is Relation-like NAT -defined REAL -valued Function-like finite FinSequence-like FinSubsequence-like V88() V89() V90() FinSequence of REAL
((f,n,i),i,g) is Relation-like NAT -defined REAL -valued Function-like finite FinSequence-like FinSubsequence-like V88() V89() V90() FinSequence of REAL
dom (n,i,f,g) is finite Element of K32(NAT)
dom (f,n,i) is finite Element of K32(NAT)
n is set
Funcs (n,n) is non empty functional set
i is Relation-like Function-like Element of Funcs (n,n)
f is Relation-like Function-like Element of Funcs (n,n)
i * f is Relation-like Function-like set
K33(n,n) is set
K32(K33(n,n)) is set
g is Relation-like n -defined n -valued Function-like total quasi_total Element of K32(K33(n,n))
G is Relation-like n -defined n -valued Function-like total quasi_total Element of K32(K33(n,n))
G * g is Relation-like n -defined n -valued Function-like total quasi_total Element of K32(K33(n,n))
n is set
Funcs (n,n) is non empty functional set
i is Relation-like Function-like Element of Funcs (n,n)
f is Element of n
i . f is set
K33(n,n) is set
K32(K33(n,n)) is set
dom i is set
n is set
Funcs (n,n) is non empty functional set
K33(NAT,(Funcs (n,n))) is V5() non finite set
K32(K33(NAT,(Funcs (n,n)))) is V5() non finite set
id n is Relation-like Function-like one-to-one Element of Funcs (n,n)
i is Relation-like Function-like Element of Funcs (n,n)
f is non empty Relation-like NAT -defined Funcs (n,n) -valued Function-like total quasi_total Element of K32(K33(NAT,(Funcs (n,n))))
f . 0 is Relation-like Function-like Element of Funcs (n,n)
f is non empty Relation-like NAT -defined Funcs (n,n) -valued Function-like total quasi_total Element of K32(K33(NAT,(Funcs (n,n))))
f . 0 is Relation-like Function-like Element of Funcs (n,n)
g is non empty Relation-like NAT -defined Funcs (n,n) -valued Function-like total quasi_total Element of K32(K33(NAT,(Funcs (n,n))))
g . 0 is Relation-like Function-like Element of Funcs (n,n)
Funcs ((REAL *),(REAL *)) is non empty functional FUNCTION_DOMAIN of REAL * ,REAL *
Funcs ((REAL *),(REAL *)) is non empty functional set
n is Relation-like REAL * -defined REAL * -valued Function-like total quasi_total Element of Funcs ((REAL *),(REAL *))
((REAL *),n) is non empty Relation-like NAT -defined Funcs ((REAL *),(REAL *)) -valued Function-like total quasi_total Element of K32(K33(NAT,(Funcs ((REAL *),(REAL *)))))
K33(NAT,(Funcs ((REAL *),(REAL *)))) is V5() non finite set
K32(K33(NAT,(Funcs ((REAL *),(REAL *))))) is V5() non finite set
((REAL *),n) . 0 is Relation-like Function-like Element of Funcs ((REAL *),(REAL *))
i is Relation-like NAT -defined REAL -valued Function-like finite FinSequence-like FinSubsequence-like V88() V89() V90() Element of REAL *
((REAL *),(((REAL *),n) . 0),i) is Relation-like NAT -defined Function-like finite FinSequence-like FinSubsequence-like Element of REAL *
id (REAL *) is non empty Relation-like Function-like one-to-one Element of Funcs ((REAL *),(REAL *))
((REAL *),(id (REAL *)),i) is Relation-like NAT -defined Function-like finite FinSequence-like FinSubsequence-like Element of REAL *
n is set
Funcs (n,n) is non empty functional set
i is Relation-like Function-like Element of Funcs (n,n)
dom i is set
f is Relation-like Function-like set
dom f is set
rng f is set
i is Relation-like REAL * -defined REAL * -valued Function-like total quasi_total Element of Funcs ((REAL *),(REAL *))
n is Relation-like REAL * -defined REAL * -valued Function-like total quasi_total Element of Funcs ((REAL *),(REAL *))
((REAL *),i,n) is Relation-like Function-like Element of Funcs ((REAL *),(REAL *))
((REAL *),((REAL *),i,n)) is non empty Relation-like NAT -defined Funcs ((REAL *),(REAL *)) -valued Function-like total quasi_total Element of K32(K33(NAT,(Funcs ((REAL *),(REAL *)))))
K33(NAT,(Funcs ((REAL *),(REAL *)))) is V5() non finite set
K32(K33(NAT,(Funcs ((REAL *),(REAL *))))) is V5() non finite set
f is Relation-like NAT -defined REAL -valued Function-like finite FinSequence-like FinSubsequence-like V88() V89() V90() Element of REAL *
g is V17() V18() V19() V23() V24() V25() finite cardinal integer ext-real non negative Element of NAT
g + 1 is non empty V17() V18() V19() V23() V24() V25() finite cardinal integer ext-real positive non negative Element of NAT
((REAL *),((REAL *),i,n)) . (g + 1) is Relation-like Function-like Element of Funcs ((REAL *),(REAL *))
((REAL *),(((REAL *),((REAL *),i,n)) . (g + 1)),f) is Relation-like NAT -defined Function-like finite FinSequence-like FinSubsequence-like Element of REAL *
((REAL *),((REAL *),i,n)) . g is Relation-like Function-like Element of Funcs ((REAL *),(REAL *))
((REAL *),(((REAL *),((REAL *),i,n)) . g),f) is Relation-like NAT -defined Function-like finite FinSequence-like FinSubsequence-like Element of REAL *
((REAL *),i,((REAL *),(((REAL *),((REAL *),i,n)) . g),f)) is Relation-like NAT -defined Function-like finite FinSequence-like FinSubsequence-like Element of REAL *
((REAL *),n,((REAL *),i,((REAL *),(((REAL *),((REAL *),i,n)) . g),f))) is Relation-like NAT -defined Function-like finite FinSequence-like FinSubsequence-like Element of REAL *
((REAL *),(((REAL *),((REAL *),i,n)) . g),((REAL *),i,n)) is Relation-like Function-like Element of Funcs ((REAL *),(REAL *))
dom ((REAL *),i,n) is set
dom ((REAL *),(((REAL *),((REAL *),i,n)) . g),((REAL *),i,n)) is set
((REAL *),((REAL *),(((REAL *),((REAL *),i,n)) . g),((REAL *),i,n)),f) is Relation-like NAT -defined Function-like finite FinSequence-like FinSubsequence-like Element of REAL *
((REAL *),((REAL *),i,n),((REAL *),(((REAL *),((REAL *),i,n)) . g),f)) is Relation-like NAT -defined Function-like finite FinSequence-like FinSubsequence-like Element of REAL *
n is Relation-like REAL * -defined REAL * -valued Function-like total quasi_total Element of Funcs ((REAL *),(REAL *))
i is Relation-like NAT -defined REAL -valued Function-like finite FinSequence-like FinSubsequence-like V88() V89() V90() Element of REAL *
n . i is Relation-like NAT -defined Function-like finite FinSequence-like FinSubsequence-like set
((REAL *),n,i) is Relation-like NAT -defined Function-like finite FinSequence-like FinSubsequence-like Element of REAL *
n is Relation-like NAT -defined REAL -valued Function-like finite FinSequence-like FinSubsequence-like V88() V89() V90() Element of REAL *
dom n is finite Element of K32(NAT)
i is V17() V18() V19() V23() V24() V25() finite cardinal integer ext-real non negative set
- 1 is V24() V25() integer ext-real non positive Element of REAL
{ b₁ where b₁ is V17() V18() V19() V23() V24() V25() finite cardinal integer ext-real non negative Element of NAT : ( b₁ in dom n & 1 <= b₁ & b₁ <= i & not n . b₁ = - 1 & not n . (i + b₁) = - 1 ) } is set
g is set
G is V17() V18() V19() V23() V24() V25() finite cardinal integer ext-real non negative Element of NAT
n . G is V24() V25() ext-real Element of REAL
i + G is V17() V18() V19() V23() V24() V25() finite cardinal integer ext-real non negative Element of NAT
n . (i + G) is V24() V25() ext-real Element of REAL
n is Relation-like REAL * -defined REAL * -valued Function-like total quasi_total Element of Funcs ((REAL *),(REAL *))
((REAL *),n) is non empty Relation-like NAT -defined Funcs ((REAL *),(REAL *)) -valued Function-like total quasi_total Element of K32(K33(NAT,(Funcs ((REAL *),(REAL *)))))
K33(NAT,(Funcs ((REAL *),(REAL *)))) is V5() non finite set
K32(K33(NAT,(Funcs ((REAL *),(REAL *))))) is V5() non finite set
i is Relation-like NAT -defined REAL -valued Function-like finite FinSequence-like FinSubsequence-like V88() V89() V90() Element of REAL *
f is V17() V18() V19() V23() V24() V25() finite cardinal integer ext-real non negative set
g is V17() V18() V19() V23() V24() V25() finite cardinal integer ext-real non negative Element of NAT
((REAL *),n) . g is Relation-like Function-like Element of Funcs ((REAL *),(REAL *))
((((REAL *),n) . g),i) is Relation-like NAT -defined REAL -valued Function-like finite FinSequence-like FinSubsequence-like V88() V89() V90() Element of REAL *
(((((REAL *),n) . g),i),f) is Element of K32(NAT)
dom ((((REAL *),n) . g),i) is finite Element of K32(NAT)
{ b₁ where b₁ is V17() V18() V19() V23() V24() V25() finite cardinal integer ext-real non negative Element of NAT : ( b₁ in dom ((((REAL *),n) . g),i) & 1 <= b₁ & b₁ <= f & not ((((REAL *),n) . g),i) . b₁ = - 1 & not ((((REAL *),n) . g),i) . (f + b₁) = - 1 ) } is set
g is V17() V18() V19() V23() V24() V25() finite cardinal integer ext-real non negative set
((REAL *),n) . g is Relation-like Function-like Element of Funcs ((REAL *),(REAL *))
((((REAL *),n) . g),i) is Relation-like NAT -defined REAL -valued Function-like finite FinSequence-like FinSubsequence-like V88() V89() V90() Element of REAL *
(((((REAL *),n) . g),i),f) is Element of K32(NAT)
dom ((((REAL *),n) . g),i) is finite Element of K32(NAT)
{ b₁ where b₁ is V17() V18() V19() V23() V24() V25() finite cardinal integer ext-real non negative Element of NAT : ( b₁ in dom ((((REAL *),n) . g),i) & 1 <= b₁ & b₁ <= f & not ((((REAL *),n) . g),i) . b₁ = - 1 & not ((((REAL *),n) . g),i) . (f + b₁) = - 1 ) } is set
g is V17() V18() V19() V23() V24() V25() finite cardinal integer ext-real non negative set
((REAL *),n) . g is Relation-like Function-like Element of Funcs ((REAL *),(REAL *))
((((REAL *),n) . g),i) is Relation-like NAT -defined REAL -valued Function-like finite FinSequence-like FinSubsequence-like V88() V89() V90() Element of REAL *
(((((REAL *),n) . g),i),f) is Element of K32(NAT)
dom ((((REAL *),n) . g),i) is finite Element of K32(NAT)
{ b₁ where b₁ is V17() V18() V19() V23() V24() V25() finite cardinal integer ext-real non negative Element of NAT : ( b₁ in dom ((((REAL *),n) . g),i) & 1 <= b₁ & b₁ <= f & not ((((REAL *),n) . g),i) . b₁ = - 1 & not ((((REAL *),n) . g),i) . (f + b₁) = - 1 ) } is set
g is V17() V18() V19() V23() V24() V25() finite cardinal integer ext-real non negative Element of NAT
((REAL *),n) . g is Relation-like Function-like Element of Funcs ((REAL *),(REAL *))
((((REAL *),n) . g),i) is Relation-like NAT -defined REAL -valued Function-like finite FinSequence-like FinSubsequence-like V88() V89() V90() Element of REAL *
(((((REAL *),n) . g),i),f) is Element of K32(NAT)
dom ((((REAL *),n) . g),i) is finite Element of K32(NAT)
{ b₁ where b₁ is V17() V18() V19() V23() V24() V25() finite cardinal integer ext-real non negative Element of NAT : ( b₁ in dom ((((REAL *),n) . g),i) & 1 <= b₁ & b₁ <= f & not ((((REAL *),n) . g),i) . b₁ = - 1 & not ((((REAL *),n) . g),i) . (f + b₁) = - 1 ) } is set
G is V17() V18() V19() V23() V24() V25() finite cardinal integer ext-real non negative Element of NAT
((REAL *),n) . G is Relation-like Function-like Element of Funcs ((REAL *),(REAL *))
((((REAL *),n) . G),i) is Relation-like NAT -defined REAL -valued Function-like finite FinSequence-like FinSubsequence-like V88() V89() V90() Element of REAL *
(((((REAL *),n) . G),i),f) is Element of K32(NAT)
dom ((((REAL *),n) . G),i) is finite Element of K32(NAT)
{ b₁ where b₁ is V17() V18() V19() V23() V24() V25() finite cardinal integer ext-real non negative Element of NAT : ( b₁ in dom ((((REAL *),n) . G),i) & 1 <= b₁ & b₁ <= f & not ((((REAL *),n) . G),i) . b₁ = - 1 & not ((((REAL *),n) . G),i) . (f + b₁) = - 1 ) } is set
n is Relation-like REAL * -defined REAL * -valued Function-like total quasi_total Element of Funcs ((REAL *),(REAL *))
((REAL *),n) is non empty Relation-like NAT -defined Funcs ((REAL *),(REAL *)) -valued Function-like total quasi_total Element of K32(K33(NAT,(Funcs ((REAL *),(REAL *)))))
i is V17() V18() V19() V23() V24() V25() finite cardinal integer ext-real non negative Element of NAT
g is set
dom n is set
W is Relation-like Function-like set
dom W is set
rng W is set
G is Relation-like NAT -defined REAL -valued Function-like finite FinSequence-like FinSubsequence-like V88() V89() V90() Element of REAL *
(n,G,i) is V17() V18() V19() V23() V24() V25() finite cardinal integer ext-real non negative Element of NAT
((REAL *),n) . (n,G,i) is Relation-like Function-like Element of Funcs ((REAL *),(REAL *))
((((REAL *),n) . (n,G,i)),G) is Relation-like NAT -defined REAL -valued Function-like finite FinSequence-like FinSubsequence-like V88() V89() V90() Element of REAL *
v1 is Relation-like NAT -defined REAL -valued Function-like finite FinSequence-like FinSubsequence-like V88() V89() V90() Element of REAL *
W is Relation-like NAT -defined REAL -valued Function-like finite FinSequence-like FinSubsequence-like V88() V89() V90() Element of REAL *
(n,v1,i) is V17() V18() V19() V23() V24() V25() finite cardinal integer ext-real non negative Element of NAT
((REAL *),n) . (n,v1,i) is Relation-like Function-like Element of Funcs ((REAL *),(REAL *))
((((REAL *),n) . (n,v1,i)),v1) is Relation-like NAT -defined REAL -valued Function-like finite FinSequence-like FinSubsequence-like V88() V89() V90() Element of REAL *
W is Relation-like NAT -defined REAL -valued Function-like finite FinSequence-like FinSubsequence-like V88() V89() V90() Element of REAL *
g is Relation-like Function-like set
dom g is set
rng g is set
G is set
W is set
g . W is set
v2 is Relation-like Function-like set
dom v2 is set
rng v2 is set
v1 is Relation-like NAT -defined REAL -valued Function-like finite FinSequence-like FinSubsequence-like V88() V89() V90() Element of REAL *
(n,v1,i) is V17() V18() V19() V23() V24() V25() finite cardinal integer ext-real non negative Element of NAT
((REAL *),n) . (n,v1,i) is Relation-like Function-like Element of Funcs ((REAL *),(REAL *))
((((REAL *),n) . (n,v1,i)),v1) is Relation-like NAT -defined REAL -valued Function-like finite FinSequence-like FinSubsequence-like V88() V89() V90() Element of REAL *
W is Relation-like Function-like set
dom W is set
rng W is set
G is Relation-like REAL * -defined REAL * -valued Function-like total quasi_total Element of Funcs ((REAL *),(REAL *))
dom G is set
W is Relation-like Function-like set
dom W is set
rng W is set
W is Relation-like NAT -defined REAL -valued Function-like finite FinSequence-like FinSubsequence-like V88() V89() V90() Element of REAL *
(G,W) is Relation-like NAT -defined REAL -valued Function-like finite FinSequence-like FinSubsequence-like V88() V89() V90() Element of REAL *
(n,W,i) is V17() V18() V19() V23() V24() V25() finite cardinal integer ext-real non negative Element of NAT
((REAL *),n) . (n,W,i) is Relation-like Function-like Element of Funcs ((REAL *),(REAL *))
((((REAL *),n) . (n,W,i)),W) is Relation-like NAT -defined REAL -valued Function-like finite FinSequence-like FinSubsequence-like V88() V89() V90() Element of REAL *
v1 is Relation-like Function-like set
dom v1 is set
rng v1 is set
g is Relation-like REAL * -defined REAL * -valued Function-like total quasi_total Element of Funcs ((REAL *),(REAL *))
dom g is set
G is Relation-like REAL * -defined REAL * -valued Function-like total quasi_total Element of Funcs ((REAL *),(REAL *))
dom G is set
W is set
g . W is Relation-like NAT -defined Function-like finite FinSequence-like FinSubsequence-like set
v1 is Relation-like NAT -defined REAL -valued Function-like finite FinSequence-like FinSubsequence-like V88() V89() V90() Element of REAL *
(n,v1,i) is V17() V18() V19() V23() V24() V25() finite cardinal integer ext-real non negative Element of NAT
((REAL *),n) . (n,v1,i) is Relation-like Function-like Element of Funcs ((REAL *),(REAL *))
((((REAL *),n) . (n,v1,i)),v1) is Relation-like NAT -defined REAL -valued Function-like finite FinSequence-like FinSubsequence-like V88() V89() V90() Element of REAL *
G . W is Relation-like NAT -defined Function-like finite FinSequence-like FinSubsequence-like set
n is non empty oriented MultiGraphStruct
the carrier of n is set
the carrier' of n is set
i is Element of the carrier of n
f is Element of the carrier of n
g is set
g is set
W is set
G is set
v1 is set
n is non empty oriented MultiGraphStruct
the carrier of n is set
the carrier' of n is set
i is Element of the carrier of n
f is Element of the carrier of n
g is Relation-like Function-like set
(n,i,f) is set
g . (n,i,f) is set
G is set
n is non empty oriented MultiGraphStruct
the carrier of n is set
the carrier' of n is set
K33( the carrier' of n,Real>=0) is set
K32(K33( the carrier' of n,Real>=0)) is set
i is Element of the carrier of n
f is Element of the carrier of n
g is Relation-like the carrier' of n -defined Real>=0 -valued Function-like total quasi_total Element of K32(K33( the carrier' of n,Real>=0))
(n,i,f,g) is set
(n,i,f) is set
G is set
G is set
dom g is set
g . (n,i,f) is set
W is set
G is set
n is non empty oriented MultiGraphStruct
the carrier of n is set
the carrier' of n is set
K33( the carrier' of n,Real>=0) is set
K32(K33( the carrier' of n,Real>=0)) is set
i is Element of the carrier of n
f is Element of the carrier of n
g is Relation-like the carrier' of n -defined Real>=0 -valued Function-like total quasi_total Element of K32(K33( the carrier' of n,Real>=0))
(n,i,f,g) is V24() V25() ext-real Element of REAL
(n,i,f) is set
W is set
W is set
dom g is set
g . W is set
v1 is V24() V25() ext-real Element of REAL
n is non empty oriented MultiGraphStruct
the carrier of n is set
the carrier' of n is set
K33( the carrier' of n,Real>=0) is set
K32(K33( the carrier' of n,Real>=0)) is set
W is non empty oriented MultiGraphStruct
the carrier of W is set
the carrier' of W is set
K33( the carrier' of W,Real>=0) is set
K32(K33( the carrier' of W,Real>=0)) is set
i is Element of the carrier of n
f is Element of the carrier of n
g is Relation-like the carrier' of n -defined Real>=0 -valued Function-like total quasi_total Element of K32(K33( the carrier' of n,Real>=0))
(n,i,f,g) is V24() V25() ext-real Element of REAL
G is set
v1 is Element of the carrier of W
v2 is Element of the carrier of W
VG is Relation-like the carrier' of W -defined Real>=0 -valued Function-like total quasi_total Element of K32(K33( the carrier' of W,Real>=0))
(W,v1,v2,VG) is V24() V25() ext-real Element of REAL
n is set
i is non empty oriented MultiGraphStruct
the carrier of i is set
the carrier' of i is set
K33( the carrier' of i,Real>=0) is set
K32(K33( the carrier' of i,Real>=0)) is set
f is Element of the carrier of i
g is Element of the carrier of i
G is Relation-like the carrier' of i -defined Real>=0 -valued Function-like total quasi_total Element of K32(K33( the carrier' of i,Real>=0))
(i,f,g,G) is V24() V25() ext-real Element of REAL
G . n is set
(i,f,g) is set
v1 is set
n is Relation-like NAT -defined REAL -valued Function-like finite FinSequence-like FinSubsequence-like V88() V89() V90() Element of REAL *
dom n is finite Element of K32(NAT)
i is V17() V18() V19() V23() V24() V25() finite cardinal integer ext-real non negative Element of NAT
{ b₁ where b₁ is V17() V18() V19() V23() V24() V25() finite cardinal integer ext-real non negative Element of NAT : ( b₁ in dom n & 1 <= b₁ & b₁ <= i & not n . b₁ = - 1 ) } is set
g is set
G is V17() V18() V19() V23() V24() V25() finite cardinal integer ext-real non negative Element of NAT
n . G is V24() V25() ext-real Element of REAL
n is Relation-like NAT -defined REAL -valued Function-like finite FinSequence-like FinSubsequence-like V88() V89() V90() Element of REAL *
dom n is finite Element of K32(NAT)
i is V17() V18() V19() V23() V24() V25() finite cardinal integer ext-real non negative Element of NAT
{ b₁ where b₁ is V17() V18() V19() V23() V24() V25() finite cardinal integer ext-real non negative Element of NAT : ( b₁ in dom n & 1 <= b₁ & b₁ <= i & n . b₁ = - 1 ) } is set
g is set
G is V17() V18() V19() V23() V24() V25() finite cardinal integer ext-real non negative Element of NAT
n . G is V24() V25() ext-real Element of REAL
n is V17() V18() V19() V23() V24() V25() finite cardinal integer ext-real non negative Element of NAT
Seg n is finite n -element Element of K32(NAT)
i is Relation-like NAT -defined REAL -valued Function-like finite FinSequence-like FinSubsequence-like V88() V89() V90() Element of REAL *
(i,n) is Element of K32(NAT)
dom i is finite Element of K32(NAT)
{ b₁ where b₁ is V17() V18() V19() V23() V24() V25() finite cardinal integer ext-real non negative Element of NAT : ( b₁ in dom i & 1 <= b₁ & b₁ <= n & not i . b₁ = - 1 ) } is set
f is set
{ b₁ where b₁ is V17() V18() V19() V23() V24() V25() finite cardinal integer ext-real non negative Element of NAT : ( 1 <= b₁ & b₁ <= n ) } is set
g is V17() V18() V19() V23() V24() V25() finite cardinal integer ext-real non negative Element of NAT
i . g is V24() V25() ext-real Element of REAL
n is Relation-like NAT -defined REAL -valued Function-like finite FinSequence-like FinSubsequence-like V88() V89() V90() Element of REAL *
i is V17() V18() V19() V23() V24() V25() finite cardinal integer ext-real non negative Element of NAT
(n,i) is Element of K32(NAT)
dom n is finite Element of K32(NAT)
{ b₁ where b₁ is V17() V18() V19() V23() V24() V25() finite cardinal integer ext-real non negative Element of NAT : ( b₁ in dom n & 1 <= b₁ & b₁ <= i & not n . b₁ = - 1 ) } is set
Seg i is finite i -element Element of K32(NAT)
n is V17() V18() V19() V23() V24() V25() finite cardinal integer ext-real non negative Element of NAT
i is Relation-like NAT -defined REAL -valued Function-like finite FinSequence-like FinSubsequence-like V88() V89() V90() Element of REAL *
(i,n) is Element of K32(NAT)
dom i is finite Element of K32(NAT)
{ b₁ where b₁ is V17() V18() V19() V23() V24() V25() finite cardinal integer ext-real non negative Element of NAT : ( b₁ in dom i & 1 <= b₁ & b₁ <= n & not i . b₁ = - 1 & not i . (n + b₁) = - 1 ) } is set
(i,n) is finite Element of K32(NAT)
{ b₁ where b₁ is V17() V18() V19() V23() V24() V25() finite cardinal integer ext-real non negative Element of NAT : ( b₁ in dom i & 1 <= b₁ & b₁ <= n & not i . b₁ = - 1 ) } is set
f is set
g is V17() V18() V19() V23() V24() V25() finite cardinal integer ext-real non negative Element of NAT
i . g is V24() V25() ext-real Element of REAL
n + g is V17() V18() V19() V23() V24() V25() finite cardinal integer ext-real non negative Element of NAT
i . (n + g) is V24() V25() ext-real Element of REAL
n is V17() V18() V19() V23() V24() V25() finite cardinal integer ext-real non negative Element of NAT
Seg n is finite n -element Element of K32(NAT)
i is Relation-like NAT -defined REAL -valued Function-like finite FinSequence-like FinSubsequence-like V88() V89() V90() Element of REAL *
(i,n) is Element of K32(NAT)
dom i is finite Element of K32(NAT)
{ b₁ where b₁ is V17() V18() V19() V23() V24() V25() finite cardinal integer ext-real non negative Element of NAT : ( b₁ in dom i & 1 <= b₁ & b₁ <= n & not i . b₁ = - 1 & not i . (n + b₁) = - 1 ) } is set
(i,n) is finite Element of K32(NAT)
{ b₁ where b₁ is V17() V18() V19() V23() V24() V25() finite cardinal integer ext-real non negative Element of NAT : ( b₁ in dom i & 1 <= b₁ & b₁ <= n & not i . b₁ = - 1 ) } is set
n is Relation-like NAT -defined REAL -valued Function-like finite FinSequence-like FinSubsequence-like V88() V89() V90() Element of REAL *
i is V17() V18() V19() V23() V24() V25() finite cardinal integer ext-real non negative Element of NAT
(n,i) is Element of K32(NAT)
dom n is finite Element of K32(NAT)
{ b₁ where b₁ is V17() V18() V19() V23() V24() V25() finite cardinal integer ext-real non negative Element of NAT : ( b₁ in dom n & 1 <= b₁ & b₁ <= i & not n . b₁ = - 1 & not n . (i + b₁) = - 1 ) } is set
Seg i is finite i -element Element of K32(NAT)
n is finite Element of K32(NAT)
i is Relation-like NAT -defined REAL -valued Function-like finite FinSequence-like FinSubsequence-like V88() V89() V90() Element of REAL *
f is V17() V18() V19() V23() V24() V25() finite cardinal integer ext-real non negative Element of NAT
2 * f is V17() V18() V19() V23() V24() V25() finite cardinal integer ext-real non negative Element of NAT
g is non empty finite Element of K32(NAT)
G is Element of g
(2 * f) + G is V17() V18() V19() V23() V24() V25() finite cardinal integer ext-real non negative Element of NAT
i /. ((2 * f) + G) is V24() V25() ext-real Element of REAL
W is V17() V18() V19() V23() V24() V25() finite cardinal integer ext-real non negative Element of NAT
(2 * f) + W is V17() V18() V19() V23() V24() V25() finite cardinal integer ext-real non negative Element of NAT
i /. ((2 * f) + W) is V24() V25() ext-real Element of REAL
v1 is V17() V18() V19() V23() V24() V25() finite cardinal integer ext-real non negative set
(2 * f) + v1 is V17() V18() V19() V23() V24() V25() finite cardinal integer ext-real non negative Element of NAT
i /. ((2 * f) + v1) is V24() V25() ext-real Element of REAL
v2 is V17() V18() V19() V23() V24() V25() finite cardinal integer ext-real non negative Element of NAT
VG is V17() V18() V19() V23() V24() V25() finite cardinal integer ext-real non negative Element of NAT
Ug is V17() V18() V19() V23() V24() V25() finite cardinal integer ext-real non negative Element of NAT
(2 * f) + Ug is V17() V18() V19() V23() V24() V25() finite cardinal integer ext-real non negative Element of NAT
i /. ((2 * f) + Ug) is V24() V25() ext-real Element of REAL
Vg is V17() V18() V19() V23() V24() V25() finite cardinal integer ext-real non negative Element of NAT
(2 * f) + Vg is V17() V18() V19() V23() V24() V25() finite cardinal integer ext-real non negative Element of NAT
i /. ((2 * f) + Vg) is V24() V25() ext-real Element of REAL
Vg is V17() V18() V19() V23() V24() V25() finite cardinal integer ext-real non negative Element of NAT
(2 * f) + Vg is V17() V18() V19() V23() V24() V25() finite cardinal integer ext-real non negative Element of NAT
i /. ((2 * f) + Vg) is V24() V25() ext-real Element of REAL
g is V17() V18() V19() V23() V24() V25() finite cardinal integer ext-real non negative Element of NAT
G is V17() V18() V19() V23() V24() V25() finite cardinal integer ext-real non negative Element of NAT
W is V17() V18() V19() V23() V24() V25() finite cardinal integer ext-real non negative Element of NAT
(2 * f) + W is V17() V18() V19() V23() V24() V25() finite cardinal integer ext-real non negative Element of NAT
i /. ((2 * f) + W) is V24() V25() ext-real Element of REAL
W is V17() V18() V19() V23() V24() V25() finite cardinal integer ext-real non negative Element of NAT
(2 * f) + W is V17() V18() V19() V23() V24() V25() finite cardinal integer ext-real non negative Element of NAT
i /. ((2 * f) + W) is V24() V25() ext-real Element of REAL
v1 is V17() V18() V19() V23() V24() V25() finite cardinal integer ext-real non negative Element of NAT
(2 * f) + v1 is V17() V18() V19() V23() V24() V25() finite cardinal integer ext-real non negative Element of NAT
i /. ((2 * f) + v1) is V24() V25() ext-real Element of REAL
v1 is V17() V18() V19() V23() V24() V25() finite cardinal integer ext-real non negative Element of NAT
(2 * f) + v1 is V17() V18() V19() V23() V24() V25() finite cardinal integer ext-real non negative Element of NAT
i /. ((2 * f) + v1) is V24() V25() ext-real Element of REAL
n is V17() V18() V19() V23() V24() V25() finite cardinal integer ext-real non negative Element of NAT
i is V17() V18() V19() V23() V24() V25() finite cardinal integer ext-real non negative Element of NAT
n + i is V17() V18() V19() V23() V24() V25() finite cardinal integer ext-real non negative Element of NAT
f is Relation-like NAT -defined REAL -valued Function-like finite FinSequence-like FinSubsequence-like V88() V89() V90() Element of REAL *
(f,n) is finite Element of K32(NAT)
dom f is finite Element of K32(NAT)
{ b₁ where b₁ is V17() V18() V19() V23() V24() V25() finite cardinal integer ext-real non negative Element of NAT : ( b₁ in dom f & 1 <= b₁ & b₁ <= n & not f . b₁ = - 1 & not f . (n + b₁) = - 1 ) } is set
((f,n),f,n) is V17() V18() V19() V23() V24() V25() finite cardinal integer ext-real non negative Element of NAT
f . i is V24() V25() ext-real Element of REAL
f . (n + i) is V24() V25() ext-real Element of REAL
2 * n is V17() V18() V19() V23() V24() V25() finite cardinal integer ext-real non negative Element of NAT
G is V17() V18() V19() V23() V24() V25() finite cardinal integer ext-real non negative Element of NAT
(2 * n) + G is V17() V18() V19() V23() V24() V25() finite cardinal integer ext-real non negative Element of NAT
f /. ((2 * n) + G) is V24() V25() ext-real Element of REAL
G is V17() V18() V19() V23() V24() V25() finite cardinal integer ext-real non negative Element of NAT
f . G is V24() V25() ext-real Element of REAL
n + G is V17() V18() V19() V23() V24() V25() finite cardinal integer ext-real non negative Element of NAT
f . (n + G) is V24() V25() ext-real Element of REAL
n is V17() V18() V19() V23() V24() V25() finite cardinal integer ext-real non negative Element of NAT
i is Relation-like NAT -defined REAL -valued Function-like finite FinSequence-like FinSubsequence-like V88() V89() V90() Element of REAL *
(i,n) is finite Element of K32(NAT)
dom i is finite Element of K32(NAT)
{ b₁ where b₁ is V17() V18() V19() V23() V24() V25() finite cardinal integer ext-real non negative Element of NAT : ( b₁ in dom i & 1 <= b₁ & b₁ <= n & not i . b₁ = - 1 & not i . (n + b₁) = - 1 ) } is set
((i,n),i,n) is V17() V18() V19() V23() V24() V25() finite cardinal integer ext-real non negative Element of NAT
n is V17() V18() V19() V23() V24() V25() finite cardinal integer ext-real non negative Element of NAT
n * n is V17() V18() V19() V23() V24() V25() finite cardinal integer ext-real non negative Element of NAT
3 * n is V17() V18() V19() V23() V24() V25() finite cardinal integer ext-real non negative Element of NAT
(n * n) + (3 * n) is V17() V18() V19() V23() V24() V25() finite cardinal integer ext-real non negative Element of NAT
((n * n) + (3 * n)) + 1 is non empty V17() V18() V19() V23() V24() V25() finite cardinal integer ext-real positive non negative Element of NAT
g is set
G is Relation-like NAT -defined REAL -valued Function-like finite FinSequence-like FinSubsequence-like V88() V89() V90() Element of REAL *
(G,n) is finite Element of K32(NAT)
dom G is finite Element of K32(NAT)
{ b₁ where b₁ is V17() V18() V19() V23() V24() V25() finite cardinal integer ext-real non negative Element of NAT : ( b₁ in dom G & 1 <= b₁ & b₁ <= n & not G . b₁ = - 1 & not G . (n + b₁) = - 1 ) } is set
((G,n),G,n) is V17() V18() V19() V23() V24() V25() finite cardinal integer ext-real non negative Element of NAT
((((n * n) + (3 * n)) + 1),((G,n),G,n),G,(- 1)) is Relation-like NAT -defined REAL -valued Function-like finite FinSequence-like FinSubsequence-like V88() V89() V90() FinSequence of REAL
(G,(((n * n) + (3 * n)) + 1),((G,n),G,n)) is Relation-like NAT -defined REAL -valued Function-like finite FinSequence-like FinSubsequence-like V88() V89() V90() FinSequence of REAL
((G,(((n * n) + (3 * n)) + 1),((G,n),G,n)),((G,n),G,n),(- 1)) is Relation-like NAT -defined REAL -valued Function-like finite FinSequence-like FinSubsequence-like V88() V89() V90() FinSequence of REAL
W is set
v1 is set
v2 is Relation-like NAT -defined REAL -valued Function-like finite FinSequence-like FinSubsequence-like V88() V89() V90() Element of REAL *
(v2,n) is finite Element of K32(NAT)
dom v2 is finite Element of K32(NAT)
{ b₁ where b₁ is V17() V18() V19() V23() V24() V25() finite cardinal integer ext-real non negative Element of NAT : ( b₁ in dom v2 & 1 <= b₁ & b₁ <= n & not v2 . b₁ = - 1 & not v2 . (n + b₁) = - 1 ) } is set
((v2,n),v2,n) is V17() V18() V19() V23() V24() V25() finite cardinal integer ext-real non negative Element of NAT
((((n * n) + (3 * n)) + 1),((v2,n),v2,n),v2,(- 1)) is Relation-like NAT -defined REAL -valued Function-like finite FinSequence-like FinSubsequence-like V88() V89() V90() FinSequence of REAL
(v2,(((n * n) + (3 * n)) + 1),((v2,n),v2,n)) is Relation-like NAT -defined REAL -valued Function-like finite FinSequence-like FinSubsequence-like V88() V89() V90() FinSequence of REAL
((v2,(((n * n) + (3 * n)) + 1),((v2,n),v2,n)),((v2,n),v2,n),(- 1)) is Relation-like NAT -defined REAL -valued Function-like finite FinSequence-like FinSubsequence-like V88() V89() V90() FinSequence of REAL
g is Relation-like Function-like set
dom g is set
rng g is set
G is set
W is set
g . W is set
v1 is Relation-like NAT -defined REAL -valued Function-like finite FinSequence-like FinSubsequence-like V88() V89() V90() Element of REAL *
(v1,n) is finite Element of K32(NAT)
dom v1 is finite Element of K32(NAT)
{ b₁ where b₁ is V17() V18() V19() V23() V24() V25() finite cardinal integer ext-real non negative Element of NAT : ( b₁ in dom v1 & 1 <= b₁ & b₁ <= n & not v1 . b₁ = - 1 & not v1 . (n + b₁) = - 1 ) } is set
((v1,n),v1,n) is V17() V18() V19() V23() V24() V25() finite cardinal integer ext-real non negative Element of NAT
((((n * n) + (3 * n)) + 1),((v1,n),v1,n),v1,(- 1)) is Relation-like NAT -defined REAL -valued Function-like finite FinSequence-like FinSubsequence-like V88() V89() V90() FinSequence of REAL
(v1,(((n * n) + (3 * n)) + 1),((v1,n),v1,n)) is Relation-like NAT -defined REAL -valued Function-like finite FinSequence-like FinSubsequence-like V88() V89() V90() FinSequence of REAL
((v1,(((n * n) + (3 * n)) + 1),((v1,n),v1,n)),((v1,n),v1,n),(- 1)) is Relation-like NAT -defined REAL -valued Function-like finite FinSequence-like FinSubsequence-like V88() V89() V90() FinSequence of REAL
G is Relation-like REAL * -defined REAL * -valued Function-like total quasi_total Element of Funcs ((REAL *),(REAL *))
dom G is set
W is Relation-like NAT -defined REAL -valued Function-like finite FinSequence-like FinSubsequence-like V88() V89() V90() Element of REAL *
(G,W) is Relation-like NAT -defined REAL -valued Function-like finite FinSequence-like FinSubsequence-like V88() V89() V90() Element of REAL *
(W,n) is finite Element of K32(NAT)
dom W is finite Element of K32(NAT)
{ b₁ where b₁ is V17() V18() V19() V23() V24() V25() finite cardinal integer ext-real non negative Element of NAT : ( b₁ in dom W & 1 <= b₁ & b₁ <= n & not W . b₁ = - 1 & not W . (n + b₁) = - 1 ) } is set
((W,n),W,n) is V17() V18() V19() V23() V24() V25() finite cardinal integer ext-real non negative Element of NAT
((((n * n) + (3 * n)) + 1),((W,n),W,n),W,(- 1)) is Relation-like NAT -defined REAL -valued Function-like finite FinSequence-like FinSubsequence-like V88() V89() V90() FinSequence of REAL
(W,(((n * n) + (3 * n)) + 1),((W,n),W,n)) is Relation-like NAT -defined REAL -valued Function-like finite FinSequence-like FinSubsequence-like V88() V89() V90() FinSequence of REAL
((W,(((n * n) + (3 * n)) + 1),((W,n),W,n)),((W,n),W,n),(- 1)) is Relation-like NAT -defined REAL -valued Function-like finite FinSequence-like FinSubsequence-like V88() V89() V90() FinSequence of REAL
g is Relation-like REAL * -defined REAL * -valued Function-like total quasi_total Element of Funcs ((REAL *),(REAL *))
dom g is set
G is Relation-like REAL * -defined REAL * -valued Function-like total quasi_total Element of Funcs ((REAL *),(REAL *))
dom G is set
W is set
g . W is Relation-like NAT -defined Function-like finite FinSequence-like FinSubsequence-like set
v1 is Relation-like NAT -defined REAL -valued Function-like finite FinSequence-like FinSubsequence-like V88() V89() V90() Element of REAL *
(v1,n) is finite Element of K32(NAT)
dom v1 is finite Element of K32(NAT)
{ b₁ where b₁ is V17() V18() V19() V23() V24() V25() finite cardinal integer ext-real non negative Element of NAT : ( b₁ in dom v1 & 1 <= b₁ & b₁ <= n & not v1 . b₁ = - 1 & not v1 . (n + b₁) = - 1 ) } is set
((v1,n),v1,n) is V17() V18() V19() V23() V24() V25() finite cardinal integer ext-real non negative Element of NAT
((((n * n) + (3 * n)) + 1),((v1,n),v1,n),v1,(- 1)) is Relation-like NAT -defined REAL -valued Function-like finite FinSequence-like FinSubsequence-like V88() V89() V90() FinSequence of REAL
(v1,(((n * n) + (3 * n)) + 1),((v1,n),v1,n)) is Relation-like NAT -defined REAL -valued Function-like finite FinSequence-like FinSubsequence-like V88() V89() V90() FinSequence of REAL
((v1,(((n * n) + (3 * n)) + 1),((v1,n),v1,n)),((v1,n),v1,n),(- 1)) is Relation-like NAT -defined REAL -valued Function-like finite FinSequence-like FinSubsequence-like V88() V89() V90() FinSequence of REAL
G . W is Relation-like NAT -defined Function-like finite FinSequence-like FinSubsequence-like set
n is V17() V18() V19() V23() V24() V25() finite cardinal integer ext-real non negative Element of NAT
i is V17() V18() V19() V23() V24() V25() finite cardinal integer ext-real non negative Element of NAT
i * i is V17() V18() V19() V23() V24() V25() finite cardinal integer ext-real non negative Element of NAT
3 * i is V17() V18() V19() V23() V24() V25() finite cardinal integer ext-real non negative Element of NAT
(i * i) + (3 * i) is V17() V18() V19() V23() V24() V25() finite cardinal integer ext-real non negative Element of NAT
((i * i) + (3 * i)) + 1 is non empty V17() V18() V19() V23() V24() V25() finite cardinal integer ext-real positive non negative Element of NAT
(i) is Relation-like REAL * -defined REAL * -valued Function-like total quasi_total Element of Funcs ((REAL *),(REAL *))
f is Relation-like NAT -defined REAL -valued Function-like finite FinSequence-like FinSubsequence-like V88() V89() V90() Element of REAL *
((i),f) is Relation-like NAT -defined REAL -valued Function-like finite FinSequence-like FinSubsequence-like V88() V89() V90() Element of REAL *
((i),f) . n is V24() V25() ext-real Element of REAL
f . n is V24() V25() ext-real Element of REAL
(f,i) is finite Element of K32(NAT)
dom f is finite Element of K32(NAT)
{ b₁ where b₁ is V17() V18() V19() V23() V24() V25() finite cardinal integer ext-real non negative Element of NAT : ( b₁ in dom f & 1 <= b₁ & b₁ <= i & not f . b₁ = - 1 & not f . (i + b₁) = - 1 ) } is set
((f,i),f,i) is V17() V18() V19() V23() V24() V25() finite cardinal integer ext-real non negative Element of NAT
((((i * i) + (3 * i)) + 1),((f,i),f,i),f,(- 1)) is Relation-like NAT -defined REAL -valued Function-like finite FinSequence-like FinSubsequence-like V88() V89() V90() FinSequence of REAL
(f,(((i * i) + (3 * i)) + 1),((f,i),f,i)) is Relation-like NAT -defined REAL -valued Function-like finite FinSequence-like FinSubsequence-like V88() V89() V90() FinSequence of REAL
((f,(((i * i) + (3 * i)) + 1),((f,i),f,i)),((f,i),f,i),(- 1)) is Relation-like NAT -defined REAL -valued Function-like finite FinSequence-like FinSubsequence-like V88() V89() V90() FinSequence of REAL
((((i * i) + (3 * i)) + 1),((f,i),f,i),f,(- 1)) . n is V24() V25() ext-real Element of REAL
n is V17() V18() V19() V23() V24() V25() finite cardinal integer ext-real non negative Element of NAT
i is V17() V18() V19() V23() V24() V25() finite cardinal integer ext-real non negative Element of NAT
i * i is V17() V18() V19() V23() V24() V25() finite cardinal integer ext-real non negative Element of NAT
3 * i is V17() V18() V19() V23() V24() V25() finite cardinal integer ext-real non negative Element of NAT
(i * i) + (3 * i) is V17() V18() V19() V23() V24() V25() finite cardinal integer ext-real non negative Element of NAT
((i * i) + (3 * i)) + 1 is non empty V17() V18() V19() V23() V24() V25() finite cardinal integer ext-real positive non negative Element of NAT
(i) is Relation-like REAL * -defined REAL * -valued Function-like total quasi_total Element of Funcs ((REAL *),(REAL *))
f is Relation-like NAT -defined REAL -valued Function-like finite FinSequence-like FinSubsequence-like V88() V89() V90() Element of REAL *
dom f is finite Element of K32(NAT)
f . n is V24() V25() ext-real Element of REAL
((i),f) is Relation-like NAT -defined REAL -valued Function-like finite FinSequence-like FinSubsequence-like V88() V89() V90() Element of REAL *
((i),f) . n is V24() V25() ext-real Element of REAL
(f,i) is finite Element of K32(NAT)
{ b₁ where b₁ is V17() V18() V19() V23() V24() V25() finite cardinal integer ext-real non negative Element of NAT : ( b₁ in dom f & 1 <= b₁ & b₁ <= i & not f . b₁ = - 1 & not f . (i + b₁) = - 1 ) } is set
((f,i),f,i) is V17() V18() V19() V23() V24() V25() finite cardinal integer ext-real non negative Element of NAT
((((i * i) + (3 * i)) + 1),((f,i),f,i),f,(- 1)) is Relation-like NAT -defined REAL -valued Function-like finite FinSequence-like FinSubsequence-like V88() V89() V90() FinSequence of REAL
(f,(((i * i) + (3 * i)) + 1),((f,i),f,i)) is Relation-like NAT -defined REAL -valued Function-like finite FinSequence-like FinSubsequence-like V88() V89() V90() FinSequence of REAL
((f,(((i * i) + (3 * i)) + 1),((f,i),f,i)),((f,i),f,i),(- 1)) is Relation-like NAT -defined REAL -valued Function-like finite FinSequence-like FinSubsequence-like V88() V89() V90() FinSequence of REAL
((((i * i) + (3 * i)) + 1),((f,i),f,i),f,(- 1)) . n is V24() V25() ext-real Element of REAL
n is V17() V18() V19() V23() V24() V25() finite cardinal integer ext-real non negative Element of NAT
(n) is Relation-like REAL * -defined REAL * -valued Function-like total quasi_total Element of Funcs ((REAL *),(REAL *))
i is Relation-like NAT -defined REAL -valued Function-like finite FinSequence-like FinSubsequence-like V88() V89() V90() Element of REAL *
((n),i) is Relation-like NAT -defined REAL -valued Function-like finite FinSequence-like FinSubsequence-like V88() V89() V90() Element of REAL *
dom ((n),i) is finite Element of K32(NAT)
dom i is finite Element of K32(NAT)
n * n is V17() V18() V19() V23() V24() V25() finite cardinal integer ext-real non negative Element of NAT
3 * n is V17() V18() V19() V23() V24() V25() finite cardinal integer ext-real non negative Element of NAT
(n * n) + (3 * n) is V17() V18() V19() V23() V24() V25() finite cardinal integer ext-real non negative Element of NAT
((n * n) + (3 * n)) + 1 is non empty V17() V18() V19() V23() V24() V25() finite cardinal integer ext-real positive non negative Element of NAT
(i,n) is finite Element of K32(NAT)
{ b₁ where b₁ is V17() V18() V19() V23() V24() V25() finite cardinal integer ext-real non negative Element of NAT : ( b₁ in dom i & 1 <= b₁ & b₁ <= n & not i . b₁ = - 1 & not i . (n + b₁) = - 1 ) } is set
((i,n),i,n) is V17() V18() V19() V23() V24() V25() finite cardinal integer ext-real non negative Element of NAT
((((n * n) + (3 * n)) + 1),((i,n),i,n),i,(- 1)) is Relation-like NAT -defined REAL -valued Function-like finite FinSequence-like FinSubsequence-like V88() V89() V90() FinSequence of REAL
(i,(((n * n) + (3 * n)) + 1),((i,n),i,n)) is Relation-like NAT -defined REAL -valued Function-like finite FinSequence-like FinSubsequence-like V88() V89() V90() FinSequence of REAL
((i,(((n * n) + (3 * n)) + 1),((i,n),i,n)),((i,n),i,n),(- 1)) is Relation-like NAT -defined REAL -valued Function-like finite FinSequence-like FinSubsequence-like V88() V89() V90() FinSequence of REAL
n is V17() V18() V19() V23() V24() V25() finite cardinal integer ext-real non negative Element of NAT
i is V17() V18() V19() V23() V24() V25() finite cardinal integer ext-real non negative Element of NAT
n * i is V17() V18() V19() V23() V24() V25() finite cardinal integer ext-real non negative Element of NAT
1 * i is V17() V18() V19() V23() V24() V25() finite cardinal integer ext-real non negative Element of NAT
n is V17() V18() V19() V23() V24() V25() finite cardinal integer ext-real non negative Element of NAT
n * n is V17() V18() V19() V23() V24() V25() finite cardinal integer ext-real non negative Element of NAT
3 * n is V17() V18() V19() V23() V24() V25() finite cardinal integer ext-real non negative Element of NAT
(n * n) + (3 * n) is V17() V18() V19() V23() V24() V25() finite cardinal integer ext-real non negative Element of NAT
((n * n) + (3 * n)) + 1 is non empty V17() V18() V19() V23() V24() V25() finite cardinal integer ext-real positive non negative Element of NAT
2 * n is V17() V18() V19() V23() V24() V25() finite cardinal integer ext-real non negative Element of NAT
n is V17() V18() V19() V23() V24() V25() finite cardinal integer ext-real non negative Element of NAT
2 * n is V17() V18() V19() V23() V24() V25() finite cardinal integer ext-real non negative Element of NAT
3 * n is V17() V18() V19() V23() V24() V25() finite cardinal integer ext-real non negative Element of NAT
i is V17() V18() V19() V23() V24() V25() finite cardinal integer ext-real non negative Element of NAT
n + n is V17() V18() V19() V23() V24() V25() finite cardinal integer ext-real non negative Element of NAT
n is V17() V18() V19() V23() V24() V25() finite cardinal integer ext-real non negative Element of NAT
(n) is Relation-like REAL * -defined REAL * -valued Function-like total quasi_total Element of Funcs ((REAL *),(REAL *))
i is Relation-like NAT -defined REAL -valued Function-like finite FinSequence-like FinSubsequence-like V88() V89() V90() Element of REAL *
(i,n) is finite Element of K32(NAT)
dom i is finite Element of K32(NAT)
{ b₁ where b₁ is V17() V18() V19() V23() V24() V25() finite cardinal integer ext-real non negative Element of NAT : ( b₁ in dom i & 1 <= b₁ & b₁ <= n & not i . b₁ = - 1 & not i . (n + b₁) = - 1 ) } is set
((n),i) is Relation-like NAT -defined REAL -valued Function-like finite FinSequence-like FinSubsequence-like V88() V89() V90() Element of REAL *
((i,n),i,n) is V17() V18() V19() V23() V24() V25() finite cardinal integer ext-real non negative Element of NAT
2 * n is V17() V18() V19() V23() V24() V25() finite cardinal integer ext-real non negative Element of NAT
g is V17() V18() V19() V23() V24() V25() finite cardinal integer ext-real non negative Element of NAT
(2 * n) + g is V17() V18() V19() V23() V24() V25() finite cardinal integer ext-real non negative Element of NAT
i /. ((2 * n) + g) is V24() V25() ext-real Element of REAL
((n),i) . g is V24() V25() ext-real Element of REAL
G is V17() V18() V19() V23() V24() V25() finite cardinal integer ext-real non negative Element of NAT
i . G is V24() V25() ext-real Element of REAL
n + G is V17() V18() V19() V23() V24() V25() finite cardinal integer ext-real non negative Element of NAT
i . (n + G) is V24() V25() ext-real Element of REAL
n * n is V17() V18() V19() V23() V24() V25() finite cardinal integer ext-real non negative Element of NAT
3 * n is V17() V18() V19() V23() V24() V25() finite cardinal integer ext-real non negative Element of NAT
(n * n) + (3 * n) is V17() V18() V19() V23() V24() V25() finite cardinal integer ext-real non negative Element of NAT
((n * n) + (3 * n)) + 1 is non empty V17() V18() V19() V23() V24() V25() finite cardinal integer ext-real positive non negative Element of NAT
((((n * n) + (3 * n)) + 1),g,i,(- 1)) is Relation-like NAT -defined REAL -valued Function-like finite FinSequence-like FinSubsequence-like V88() V89() V90() FinSequence of REAL
(i,(((n * n) + (3 * n)) + 1),g) is Relation-like NAT -defined REAL -valued Function-like finite FinSequence-like FinSubsequence-like V88() V89() V90() FinSequence of REAL
((i,(((n * n) + (3 * n)) + 1),g),g,(- 1)) is Relation-like NAT -defined REAL -valued Function-like finite FinSequence-like FinSubsequence-like V88() V89() V90() FinSequence of REAL
((((n * n) + (3 * n)) + 1),g,i,(- 1)) . g is V24() V25() ext-real Element of REAL
G is V17() V18() V19() V23() V24() V25() finite cardinal integer ext-real non negative Element of NAT
i . G is V24() V25() ext-real Element of REAL
n + G is V17() V18() V19() V23() V24() V25() finite cardinal integer ext-real non negative Element of NAT
i . (n + G) is V24() V25() ext-real Element of REAL
n is Relation-like NAT -defined REAL -valued Function-like finite FinSequence-like FinSubsequence-like V88() V89() V90() Element of REAL *
i is V17() V18() V19() V23() V24() V25() finite cardinal integer ext-real non negative Element of NAT
2 * i is V17() V18() V19() V23() V24() V25() finite cardinal integer ext-real non negative Element of NAT
i * i is V17() V18() V19() V23() V24() V25() finite cardinal integer ext-real non negative Element of NAT
3 * i is V17() V18() V19() V23() V24() V25() finite cardinal integer ext-real non negative Element of NAT
(i * i) + (3 * i) is V17() V18() V19() V23() V24() V25() finite cardinal integer ext-real non negative Element of NAT
((i * i) + (3 * i)) + 1 is non empty V17() V18() V19() V23() V24() V25() finite cardinal integer ext-real positive non negative Element of NAT
n /. (((i * i) + (3 * i)) + 1) is V24() V25() ext-real Element of REAL
(2 * i) + (n /. (((i * i) + (3 * i)) + 1)) is V24() V25() ext-real Element of REAL
n /. ((2 * i) + (n /. (((i * i) + (3 * i)) + 1))) is V24() V25() ext-real Element of REAL
i * (n /. (((i * i) + (3 * i)) + 1)) is V24() V25() ext-real Element of REAL
(2 * i) + (i * (n /. (((i * i) + (3 * i)) + 1))) is V24() V25() ext-real Element of REAL
f is V17() V18() V19() V23() V24() V25() finite cardinal integer ext-real non negative Element of NAT
((2 * i) + (i * (n /. (((i * i) + (3 * i)) + 1)))) + f is V24() V25() ext-real Element of REAL
n /. (((2 * i) + (i * (n /. (((i * i) + (3 * i)) + 1)))) + f) is V24() V25() ext-real Element of REAL
(n /. ((2 * i) + (n /. (((i * i) + (3 * i)) + 1)))) + (n /. (((2 * i) + (i * (n /. (((i * i) + (3 * i)) + 1)))) + f)) is V24() V25() ext-real Element of REAL
n is Relation-like NAT -defined REAL -valued Function-like finite FinSequence-like FinSubsequence-like V88() V89() V90() Element of REAL *
dom n is finite Element of K32(NAT)
i is V17() V18() V19() V23() V24() V25() finite cardinal integer ext-real non negative Element of NAT
2 * i is V17() V18() V19() V23() V24() V25() finite cardinal integer ext-real non negative Element of NAT
i * i is V17() V18() V19() V23() V24() V25() finite cardinal integer ext-real non negative Element of NAT
3 * i is V17() V18() V19() V23() V24() V25() finite cardinal integer ext-real non negative Element of NAT
(i * i) + (3 * i) is V17() V18() V19() V23() V24() V25() finite cardinal integer ext-real non negative Element of NAT
((i * i) + (3 * i)) + 1 is non empty V17() V18() V19() V23() V24() V25() finite cardinal integer ext-real positive non negative Element of NAT
n /. (((i * i) + (3 * i)) + 1) is V24() V25() ext-real Element of REAL
g is set
G is V17() V18() V19() V23() V24() V25() finite cardinal integer ext-real non negative Element of NAT
G -' i is V17() V18() V19() V23() V24() V25() finite cardinal integer ext-real non negative Element of NAT
W is V24() V25() ext-real Element of REAL
v1 is V17() V18() V19() V23() V24() V25() finite cardinal integer ext-real non negative Element of NAT
v1 -' i is V17() V18() V19() V23() V24() V25() finite cardinal integer ext-real non negative Element of NAT
n . v1 is V24() V25() ext-real Element of REAL
v1 -' (2 * i) is V17() V18() V19() V23() V24() V25() finite cardinal integer ext-real non negative Element of NAT
(n,i,(v1 -' (2 * i))) is V24() V25() ext-real Element of REAL
(2 * i) + (n /. (((i * i) + (3 * i)) + 1)) is V24() V25() ext-real Element of REAL
n /. ((2 * i) + (n /. (((i * i) + (3 * i)) + 1))) is V24() V25() ext-real Element of REAL
i * (n /. (((i * i) + (3 * i)) + 1)) is V24() V25() ext-real Element of REAL
(2 * i) + (i * (n /. (((i * i) + (3 * i)) + 1))) is V24() V25() ext-real Element of REAL
((2 * i) + (i * (n /. (((i * i) + (3 * i)) + 1)))) + (v1 -' (2 * i)) is V24() V25() ext-real Element of REAL
n /. (((2 * i) + (i * (n /. (((i * i) + (3 * i)) + 1)))) + (v1 -' (2 * i))) is V24() V25() ext-real Element of REAL
(n /. ((2 * i) + (n /. (((i * i) + (3 * i)) + 1)))) + (n /. (((2 * i) + (i * (n /. (((i * i) + (3 * i)) + 1)))) + (v1 -' (2 * i)))) is V24() V25() ext-real Element of REAL
G -' i is V17() V18() V19() V23() V24() V25() finite cardinal integer ext-real non negative Element of NAT
n . G is V24() V25() ext-real Element of REAL
W is V24() V25() ext-real Element of REAL
v1 is V17() V18() V19() V23() V24() V25() finite cardinal integer ext-real non negative Element of NAT
v1 -' i is V17() V18() V19() V23() V24() V25() finite cardinal integer ext-real non negative Element of NAT
n . v1 is V24() V25() ext-real Element of REAL
v1 -' (2 * i) is V17() V18() V19() V23() V24() V25() finite cardinal integer ext-real non negative Element of NAT
(n,i,(v1 -' (2 * i))) is V24() V25() ext-real Element of REAL
(2 * i) + (n /. (((i * i) + (3 * i)) + 1)) is V24() V25() ext-real Element of REAL
n /. ((2 * i) + (n /. (((i * i) + (3 * i)) + 1))) is V24() V25() ext-real Element of REAL
i * (n /. (((i * i) + (3 * i)) + 1)) is V24() V25() ext-real Element of REAL
(2 * i) + (i * (n /. (((i * i) + (3 * i)) + 1))) is V24() V25() ext-real Element of REAL
((2 * i) + (i * (n /. (((i * i) + (3 * i)) + 1)))) + (v1 -' (2 * i)) is V24() V25() ext-real Element of REAL
n /. (((2 * i) + (i * (n /. (((i * i) + (3 * i)) + 1)))) + (v1 -' (2 * i))) is V24() V25() ext-real Element of REAL
(n /. ((2 * i) + (n /. (((i * i) + (3 * i)) + 1)))) + (n /. (((2 * i) + (i * (n /. (((i * i) + (3 * i)) + 1)))) + (v1 -' (2 * i)))) is V24() V25() ext-real Element of REAL
G -' i is V17() V18() V19() V23() V24() V25() finite cardinal integer ext-real non negative Element of NAT
G is V17() V18() V19() V23() V24() V25() finite cardinal integer ext-real non negative Element of NAT
G -' (2 * i) is V17() V18() V19() V23() V24() V25() finite cardinal integer ext-real non negative Element of NAT
(n,i,(G -' (2 * i))) is V24() V25() ext-real Element of REAL
(2 * i) + (n /. (((i * i) + (3 * i)) + 1)) is V24() V25() ext-real Element of REAL
n /. ((2 * i) + (n /. (((i * i) + (3 * i)) + 1))) is V24() V25() ext-real Element of REAL
i * (n /. (((i * i) + (3 * i)) + 1)) is V24() V25() ext-real Element of REAL
(2 * i) + (i * (n /. (((i * i) + (3 * i)) + 1))) is V24() V25() ext-real Element of REAL
((2 * i) + (i * (n /. (((i * i) + (3 * i)) + 1)))) + (G -' (2 * i)) is V24() V25() ext-real Element of REAL
n /. (((2 * i) + (i * (n /. (((i * i) + (3 * i)) + 1)))) + (G -' (2 * i))) is V24() V25() ext-real Element of REAL
(n /. ((2 * i) + (n /. (((i * i) + (3 * i)) + 1)))) + (n /. (((2 * i) + (i * (n /. (((i * i) + (3 * i)) + 1)))) + (G -' (2 * i)))) is V24() V25() ext-real Element of REAL
W is V24() V25() ext-real Element of REAL
v1 is V17() V18() V19() V23() V24() V25() finite cardinal integer ext-real non negative Element of NAT
v1 -' i is V17() V18() V19() V23() V24() V25() finite cardinal integer ext-real non negative Element of NAT
n . v1 is V24() V25() ext-real Element of REAL
v1 -' (2 * i) is V17() V18() V19() V23() V24() V25() finite cardinal integer ext-real non negative Element of NAT
(n,i,(v1 -' (2 * i))) is V24() V25() ext-real Element of REAL
((2 * i) + (i * (n /. (((i * i) + (3 * i)) + 1)))) + (v1 -' (2 * i)) is V24() V25() ext-real Element of REAL
n /. (((2 * i) + (i * (n /. (((i * i) + (3 * i)) + 1)))) + (v1 -' (2 * i))) is V24() V25() ext-real Element of REAL
(n /. ((2 * i) + (n /. (((i * i) + (3 * i)) + 1)))) + (n /. (((2 * i) + (i * (n /. (((i * i) + (3 * i)) + 1)))) + (v1 -' (2 * i)))) is V24() V25() ext-real Element of REAL
G -' (2 * i) is V17() V18() V19() V23() V24() V25() finite cardinal integer ext-real non negative Element of NAT
n . G is V24() V25() ext-real Element of REAL
W is V24() V25() ext-real Element of REAL
v1 is V17() V18() V19() V23() V24() V25() finite cardinal integer ext-real non negative Element of NAT
v1 -' i is V17() V18() V19() V23() V24() V25() finite cardinal integer ext-real non negative Element of NAT
n . v1 is V24() V25() ext-real Element of REAL
v1 -' (2 * i) is V17() V18() V19() V23() V24() V25() finite cardinal integer ext-real non negative Element of NAT
(n,i,(v1 -' (2 * i))) is V24() V25() ext-real Element of REAL
(2 * i) + (n /. (((i * i) + (3 * i)) + 1)) is V24() V25() ext-real Element of REAL
n /. ((2 * i) + (n /. (((i * i) + (3 * i)) + 1))) is V24() V25() ext-real Element of REAL
i * (n /. (((i * i) + (3 * i)) + 1)) is V24() V25() ext-real Element of REAL
(2 * i) + (i * (n /. (((i * i) + (3 * i)) + 1))) is V24() V25() ext-real Element of REAL
((2 * i) + (i * (n /. (((i * i) + (3 * i)) + 1)))) + (v1 -' (2 * i)) is V24() V25() ext-real Element of REAL
n /. (((2 * i) + (i * (n /. (((i * i) + (3 * i)) + 1)))) + (v1 -' (2 * i))) is V24() V25() ext-real Element of REAL
(n /. ((2 * i) + (n /. (((i * i) + (3 * i)) + 1)))) + (n /. (((2 * i) + (i * (n /. (((i * i) + (3 * i)) + 1)))) + (v1 -' (2 * i)))) is V24() V25() ext-real Element of REAL
G -' (2 * i) is V17() V18() V19() V23() V24() V25() finite cardinal integer ext-real non negative Element of NAT
G is V17() V18() V19() V23() V24() V25() finite cardinal integer ext-real non negative Element of NAT
n . G is V24() V25() ext-real Element of REAL
W is V24() V25() ext-real Element of REAL
v1 is V17() V18() V19() V23() V24() V25() finite cardinal integer ext-real non negative Element of NAT
v1 -' i is V17() V18() V19() V23() V24() V25() finite cardinal integer ext-real non negative Element of NAT
n . v1 is V24() V25() ext-real Element of REAL
v1 -' (2 * i) is V17() V18() V19() V23() V24() V25() finite cardinal integer ext-real non negative Element of NAT
(n,i,(v1 -' (2 * i))) is V24() V25() ext-real Element of REAL
(2 * i) + (n /. (((i * i) + (3 * i)) + 1)) is V24() V25() ext-real Element of REAL
n /. ((2 * i) + (n /. (((i * i) + (3 * i)) + 1))) is V24() V25() ext-real Element of REAL
i * (n /. (((i * i) + (3 * i)) + 1)) is V24() V25() ext-real Element of REAL
(2 * i) + (i * (n /. (((i * i) + (3 * i)) + 1))) is V24() V25() ext-real Element of REAL
((2 * i) + (i * (n /. (((i * i) + (3 * i)) + 1)))) + (v1 -' (2 * i)) is V24() V25() ext-real Element of REAL
n /. (((2 * i) + (i * (n /. (((i * i) + (3 * i)) + 1)))) + (v1 -' (2 * i))) is V24() V25() ext-real Element of REAL
(n /. ((2 * i) + (n /. (((i * i) + (3 * i)) + 1)))) + (n /. (((2 * i) + (i * (n /. (((i * i) + (3 * i)) + 1)))) + (v1 -' (2 * i)))) is V24() V25() ext-real Element of REAL
G is V17() V18() V19() V23() V24() V25() finite cardinal integer ext-real non negative Element of NAT
g is Relation-like Function-like set
dom g is set
rng g is set
G is set
W is set
g . W is set
v1 is V17() V18() V19() V23() V24() V25() finite cardinal integer ext-real non negative Element of NAT
v1 -' i is V17() V18() V19() V23() V24() V25() finite cardinal integer ext-real non negative Element of NAT
v1 -' i is V17() V18() V19() V23() V24() V25() finite cardinal integer ext-real non negative Element of NAT
n . v1 is V24() V25() ext-real Element of REAL
n /. v1 is V24() V25() ext-real Element of REAL
v1 -' i is V17() V18() V19() V23() V24() V25() finite cardinal integer ext-real non negative Element of NAT
v1 is V17() V18() V19() V23() V24() V25() finite cardinal integer ext-real non negative Element of NAT
v1 -' (2 * i) is V17() V18() V19() V23() V24() V25() finite cardinal integer ext-real non negative Element of NAT
(n,i,(v1 -' (2 * i))) is V24() V25() ext-real Element of REAL
(2 * i) + (n /. (((i * i) + (3 * i)) + 1)) is V24() V25() ext-real Element of REAL
n /. ((2 * i) + (n /. (((i * i) + (3 * i)) + 1))) is V24() V25() ext-real Element of REAL
i * (n /. (((i * i) + (3 * i)) + 1)) is V24() V25() ext-real Element of REAL
(2 * i) + (i * (n /. (((i * i) + (3 * i)) + 1))) is V24() V25() ext-real Element of REAL
((2 * i) + (i * (n /. (((i * i) + (3 * i)) + 1)))) + (v1 -' (2 * i)) is V24() V25() ext-real Element of REAL
n /. (((2 * i) + (i * (n /. (((i * i) + (3 * i)) + 1)))) + (v1 -' (2 * i))) is V24() V25() ext-real Element of REAL
(n /. ((2 * i) + (n /. (((i * i) + (3 * i)) + 1)))) + (n /. (((2 * i) + (i * (n /. (((i * i) + (3 * i)) + 1)))) + (v1 -' (2 * i)))) is V24() V25() ext-real Element of REAL
v1 -' (2 * i) is V17() V18() V19() V23() V24() V25() finite cardinal integer ext-real non negative Element of NAT
n . v1 is V24() V25() ext-real Element of REAL
n /. v1 is V24() V25() ext-real Element of REAL
v1 -' (2 * i) is V17() V18() V19() V23() V24() V25() finite cardinal integer ext-real non negative Element of NAT
v1 is V17() V18() V19() V23() V24() V25() finite cardinal integer ext-real non negative Element of NAT
n . v1 is V24() V25() ext-real Element of REAL
n /. v1 is V24() V25() ext-real Element of REAL
v1 is V17() V18() V19() V23() V24() V25() finite cardinal integer ext-real non negative Element of NAT
len n is V17() V18() V19() V23() V24() V25() finite cardinal integer ext-real non negative Element of NAT
Seg (len n) is finite len n -element Element of K32(NAT)
G is Relation-like NAT -defined REAL -valued Function-like finite FinSequence-like FinSubsequence-like V88() V89() V90() Element of REAL *
dom G is finite Element of K32(NAT)
W is V17() V18() V19() V23() V24() V25() finite cardinal integer ext-real non negative Element of NAT
W -' i is V17() V18() V19() V23() V24() V25() finite cardinal integer ext-real non negative Element of NAT
G . W is V24() V25() ext-real Element of REAL
n . W is V24() V25() ext-real Element of REAL
W -' (2 * i) is V17() V18() V19() V23() V24() V25() finite cardinal integer ext-real non negative Element of NAT
(n,i,(W -' (2 * i))) is V24() V25() ext-real Element of REAL
(2 * i) + (n /. (((i * i) + (3 * i)) + 1)) is V24() V25() ext-real Element of REAL
n /. ((2 * i) + (n /. (((i * i) + (3 * i)) + 1))) is V24() V25() ext-real Element of REAL
i * (n /. (((i * i) + (3 * i)) + 1)) is V24() V25() ext-real Element of REAL
(2 * i) + (i * (n /. (((i * i) + (3 * i)) + 1))) is V24() V25() ext-real Element of REAL
((2 * i) + (i * (n /. (((i * i) + (3 * i)) + 1)))) + (W -' (2 * i)) is V24() V25() ext-real Element of REAL
n /. (((2 * i) + (i * (n /. (((i * i) + (3 * i)) + 1)))) + (W -' (2 * i))) is V24() V25() ext-real Element of REAL
(n /. ((2 * i) + (n /. (((i * i) + (3 * i)) + 1)))) + (n /. (((2 * i) + (i * (n /. (((i * i) + (3 * i)) + 1)))) + (W -' (2 * i)))) is V24() V25() ext-real Element of REAL
f is Relation-like NAT -defined REAL -valued Function-like finite FinSequence-like FinSubsequence-like V88() V89() V90() Element of REAL *
dom f is finite Element of K32(NAT)
g is Relation-like NAT -defined REAL -valued Function-like finite FinSequence-like FinSubsequence-like V88() V89() V90() Element of REAL *
dom g is finite Element of K32(NAT)
G is set
W is V17() V18() V19() V23() V24() V25() finite cardinal integer ext-real non negative Element of NAT
W -' (2 * i) is V17() V18() V19() V23() V24() V25() finite cardinal integer ext-real non negative Element of NAT
W -' i is V17() V18() V19() V23() V24() V25() finite cardinal integer ext-real non negative Element of NAT
f . G is V24() V25() ext-real Element of REAL
g . G is V24() V25() ext-real Element of REAL
f . G is V24() V25() ext-real Element of REAL
n . W is V24() V25() ext-real Element of REAL
g . G is V24() V25() ext-real Element of REAL
f . G is V24() V25() ext-real Element of REAL
g . G is V24() V25() ext-real Element of REAL
f . G is V24() V25() ext-real Element of REAL
g . G is V24() V25() ext-real Element of REAL
f . G is V24() V25() ext-real Element of REAL
(n,i,(W -' (2 * i))) is V24() V25() ext-real Element of REAL
(2 * i) + (n /. (((i * i) + (3 * i)) + 1)) is V24() V25() ext-real Element of REAL
n /. ((2 * i) + (n /. (((i * i) + (3 * i)) + 1))) is V24() V25() ext-real Element of REAL
i * (n /. (((i * i) + (3 * i)) + 1)) is V24() V25() ext-real Element of REAL
(2 * i) + (i * (n /. (((i * i) + (3 * i)) + 1))) is V24() V25() ext-real Element of REAL
((2 * i) + (i * (n /. (((i * i) + (3 * i)) + 1)))) + (W -' (2 * i)) is V24() V25() ext-real Element of REAL
n /. (((2 * i) + (i * (n /. (((i * i) + (3 * i)) + 1)))) + (W -' (2 * i))) is V24() V25() ext-real Element of REAL
(n /. ((2 * i) + (n /. (((i * i) + (3 * i)) + 1)))) + (n /. (((2 * i) + (i * (n /. (((i * i) + (3 * i)) + 1)))) + (W -' (2 * i)))) is V24() V25() ext-real Element of REAL
g . G is V24() V25() ext-real Element of REAL
f . G is V24() V25() ext-real Element of REAL
n . W is V24() V25() ext-real Element of REAL
g . G is V24() V25() ext-real Element of REAL
f . G is V24() V25() ext-real Element of REAL
g . G is V24() V25() ext-real Element of REAL
f . G is V24() V25() ext-real Element of REAL
g . G is V24() V25() ext-real Element of REAL
f . G is V24() V25() ext-real Element of REAL
n . W is V24() V25() ext-real Element of REAL
g . G is V24() V25() ext-real Element of REAL
n is V17() V18() V19() V23() V24() V25() finite cardinal integer ext-real non negative Element of NAT
f is set
g is Relation-like NAT -defined REAL -valued Function-like finite FinSequence-like FinSubsequence-like V88() V89() V90() Element of REAL *
(g,n) is Relation-like NAT -defined REAL -valued Function-like finite FinSequence-like FinSubsequence-like V88() V89() V90() Element of REAL *
G is Relation-like NAT -defined REAL -valued Function-like finite FinSequence-like FinSubsequence-like V88() V89() V90() Element of REAL *
W is Relation-like NAT -defined REAL -valued Function-like finite FinSequence-like FinSubsequence-like V88() V89() V90() Element of REAL *
(W,n) is Relation-like NAT -defined REAL -valued Function-like finite FinSequence-like FinSubsequence-like V88() V89() V90() Element of REAL *
f is Relation-like Function-like set
dom f is set
g is set
rng f is set
G is set
f . G is set
W is Relation-like NAT -defined REAL -valued Function-like finite FinSequence-like FinSubsequence-like V88() V89() V90() Element of REAL *
(W,n) is Relation-like NAT -defined REAL -valued Function-like finite FinSequence-like FinSubsequence-like V88() V89() V90() Element of REAL *
g is Relation-like REAL * -defined REAL * -valued Function-like total quasi_total Element of Funcs ((REAL *),(REAL *))
dom g is set
G is Relation-like NAT -defined REAL -valued Function-like finite FinSequence-like FinSubsequence-like V88() V89() V90() Element of REAL *
(g,G) is Relation-like NAT -defined REAL -valued Function-like finite FinSequence-like FinSubsequence-like V88() V89() V90() Element of REAL *
(G,n) is Relation-like NAT -defined REAL -valued Function-like finite FinSequence-like FinSubsequence-like V88() V89() V90() Element of REAL *
f is Relation-like REAL * -defined REAL * -valued Function-like total quasi_total Element of Funcs ((REAL *),(REAL *))
dom f is set
g is Relation-like REAL * -defined REAL * -valued Function-like total quasi_total Element of Funcs ((REAL *),(REAL *))
dom g is set
G is set
f . G is Relation-like NAT -defined Function-like finite FinSequence-like FinSubsequence-like set
W is Relation-like NAT -defined REAL -valued Function-like finite FinSequence-like FinSubsequence-like V88() V89() V90() Element of REAL *
(W,n) is Relation-like NAT -defined REAL -valued Function-like finite FinSequence-like FinSubsequence-like V88() V89() V90() Element of REAL *
g . G is Relation-like NAT -defined Function-like finite FinSequence-like FinSubsequence-like set
n is V17() V18() V19() V23() V24() V25() finite cardinal integer ext-real non negative Element of NAT
(n) is Relation-like REAL * -defined REAL * -valued Function-like total quasi_total Element of Funcs ((REAL *),(REAL *))
i is Relation-like NAT -defined REAL -valued Function-like finite FinSequence-like FinSubsequence-like V88() V89() V90() Element of REAL *
((n),i) is Relation-like NAT -defined REAL -valued Function-like finite FinSequence-like FinSubsequence-like V88() V89() V90() Element of REAL *
dom ((n),i) is finite Element of K32(NAT)
dom i is finite Element of K32(NAT)
(i,n) is Relation-like NAT -defined REAL -valued Function-like finite FinSequence-like FinSubsequence-like V88() V89() V90() Element of REAL *
dom (i,n) is finite Element of K32(NAT)
n is V17() V18() V19() V23() V24() V25() finite cardinal integer ext-real non negative Element of NAT
i is V17() V18() V19() V23() V24() V25() finite cardinal integer ext-real non negative Element of NAT
3 * i is V17() V18() V19() V23() V24() V25() finite cardinal integer ext-real non negative Element of NAT
(i) is Relation-like REAL * -defined REAL * -valued Function-like total quasi_total Element of Funcs ((REAL *),(REAL *))
f is Relation-like NAT -defined REAL -valued Function-like finite FinSequence-like FinSubsequence-like V88() V89() V90() Element of REAL *
dom f is finite Element of K32(NAT)
((i),f) is Relation-like NAT -defined REAL -valued Function-like finite FinSequence-like FinSubsequence-like V88() V89() V90() Element of REAL *
((i),f) . n is V24() V25() ext-real Element of REAL
f . n is V24() V25() ext-real Element of REAL
(f,i) is Relation-like NAT -defined REAL -valued Function-like finite FinSequence-like FinSubsequence-like V88() V89() V90() Element of REAL *
(f,i) . n is V24() V25() ext-real Element of REAL
n is V17() V18() V19() V23() V24() V25() finite cardinal integer ext-real non negative Element of NAT
(n) is Relation-like REAL * -defined REAL * -valued Function-like total quasi_total Element of Funcs ((REAL *),(REAL *))
(n) is Relation-like REAL * -defined REAL * -valued Function-like total quasi_total Element of Funcs ((REAL *),(REAL *))
((REAL *),(n),(n)) is Relation-like Function-like Element of Funcs ((REAL *),(REAL *))
((REAL *),((REAL *),(n),(n))) is non empty Relation-like NAT -defined Funcs ((REAL *),(REAL *)) -valued Function-like total quasi_total Element of K32(K33(NAT,(Funcs ((REAL *),(REAL *)))))
i is V17() V18() V19() V23() V24() V25() finite cardinal integer ext-real non negative Element of NAT
((REAL *),((REAL *),(n),(n))) . i is Relation-like Function-like Element of Funcs ((REAL *),(REAL *))
i + 1 is non empty V17() V18() V19() V23() V24() V25() finite cardinal integer ext-real positive non negative Element of NAT
((REAL *),((REAL *),(n),(n))) . (i + 1) is Relation-like Function-like Element of Funcs ((REAL *),(REAL *))
f is Relation-like NAT -defined REAL -valued Function-like finite FinSequence-like FinSubsequence-like V88() V89() V90() Element of REAL *
((((REAL *),((REAL *),(n),(n))) . i),f) is Relation-like NAT -defined REAL -valued Function-like finite FinSequence-like FinSubsequence-like V88() V89() V90() Element of REAL *
dom ((((REAL *),((REAL *),(n),(n))) . i),f) is finite Element of K32(NAT)
((((REAL *),((REAL *),(n),(n))) . (i + 1)),f) is Relation-like NAT -defined REAL -valued Function-like finite FinSequence-like FinSubsequence-like V88() V89() V90() Element of REAL *
dom ((((REAL *),((REAL *),(n),(n))) . (i + 1)),f) is finite Element of K32(NAT)
((n),((((REAL *),((REAL *),(n),(n))) . i),f)) is Relation-like NAT -defined REAL -valued Function-like finite FinSequence-like FinSubsequence-like V88() V89() V90() Element of REAL *
((n),((n),((((REAL *),((REAL *),(n),(n))) . i),f))) is Relation-like NAT -defined REAL -valued Function-like finite FinSequence-like FinSubsequence-like V88() V89() V90() Element of REAL *
dom ((n),((n),((((REAL *),((REAL *),(n),(n))) . i),f))) is finite Element of K32(NAT)
dom ((n),((((REAL *),((REAL *),(n),(n))) . i),f)) is finite Element of K32(NAT)
n is V17() V18() V19() V23() V24() V25() finite cardinal integer ext-real non negative Element of NAT
(n) is Relation-like REAL * -defined REAL * -valued Function-like total quasi_total Element of Funcs ((REAL *),(REAL *))
(n) is Relation-like REAL * -defined REAL * -valued Function-like total quasi_total Element of Funcs ((REAL *),(REAL *))
((REAL *),(n),(n)) is Relation-like Function-like Element of Funcs ((REAL *),(REAL *))
((REAL *),((REAL *),(n),(n))) is non empty Relation-like NAT -defined Funcs ((REAL *),(REAL *)) -valued Function-like total quasi_total Element of K32(K33(NAT,(Funcs ((REAL *),(REAL *)))))
i is V17() V18() V19() V23() V24() V25() finite cardinal integer ext-real non negative Element of NAT
((REAL *),((REAL *),(n),(n))) . i is Relation-like Function-like Element of Funcs ((REAL *),(REAL *))
i + 1 is non empty V17() V18() V19() V23() V24() V25() finite cardinal integer ext-real positive non negative Element of NAT
((REAL *),((REAL *),(n),(n))) . (i + 1) is Relation-like Function-like Element of Funcs ((REAL *),(REAL *))
f is Relation-like NAT -defined REAL -valued Function-like finite FinSequence-like FinSubsequence-like V88() V89() V90() Element of REAL *
((((REAL *),((REAL *),(n),(n))) . i),f) is Relation-like NAT -defined REAL -valued Function-like finite FinSequence-like FinSubsequence-like V88() V89() V90() Element of REAL *
(((((REAL *),((REAL *),(n),(n))) . i),f),n) is finite Element of K32(NAT)
dom ((((REAL *),((REAL *),(n),(n))) . i),f) is finite Element of K32(NAT)
{ b₁ where b₁ is V17() V18() V19() V23() V24() V25() finite cardinal integer ext-real non negative Element of NAT : ( b₁ in dom ((((REAL *),((REAL *),(n),(n))) . i),f) & 1 <= b₁ & b₁ <= n & not ((((REAL *),((REAL *),(n),(n))) . i),f) . b₁ = - 1 & not ((((REAL *),((REAL *),(n),(n))) . i),f) . (n + b₁) = - 1 ) } is set
((((REAL *),((REAL *),(n),(n))) . (i + 1)),f) is Relation-like NAT -defined REAL -valued Function-like finite FinSequence-like FinSubsequence-like V88() V89() V90() Element of REAL *
(((((REAL *),((REAL *),(n),(n))) . (i + 1)),f),n) is finite Element of K32(NAT)
dom ((((REAL *),((REAL *),(n),(n))) . (i + 1)),f) is finite Element of K32(NAT)
{ b₁ where b₁ is V17() V18() V19() V23() V24() V25() finite cardinal integer ext-real non negative Element of NAT : ( b₁ in dom ((((REAL *),((REAL *),(n),(n))) . (i + 1)),f) & 1 <= b₁ & b₁ <= n & not ((((REAL *),((REAL *),(n),(n))) . (i + 1)),f) . b₁ = - 1 ) } is set
(((((REAL *),((REAL *),(n),(n))) . i),f),n) is finite Element of K32(NAT)
{ b₁ where b₁ is V17() V18() V19() V23() V24() V25() finite cardinal integer ext-real non negative Element of NAT : ( b₁ in dom ((((REAL *),((REAL *),(n),(n))) . i),f) & 1 <= b₁ & b₁ <= n & not ((((REAL *),((REAL *),(n),(n))) . i),f) . b₁ = - 1 ) } is set
((n),((((REAL *),((REAL *),(n),(n))) . i),f)) is Relation-like NAT -defined REAL -valued Function-like finite FinSequence-like FinSubsequence-like V88() V89() V90() Element of REAL *
dom ((n),((((REAL *),((REAL *),(n),(n))) . i),f)) is finite Element of K32(NAT)
v2 is set
VG is V17() V18() V19() V23() V24() V25() finite cardinal integer ext-real non negative Element of NAT
((((REAL *),((REAL *),(n),(n))) . (i + 1)),f) . VG is V24() V25() ext-real Element of REAL
((n),((n),((((REAL *),((REAL *),(n),(n))) . i),f))) is Relation-like NAT -defined REAL -valued Function-like finite FinSequence-like FinSubsequence-like V88() V89() V90() Element of REAL *
((n),((n),((((REAL *),((REAL *),(n),(n))) . i),f))) . VG is V24() V25() ext-real Element of REAL
((n),((((REAL *),((REAL *),(n),(n))) . i),f)) . VG is V24() V25() ext-real Element of REAL
((n),((((REAL *),((REAL *),(n),(n))) . i),f)) . v2 is V24() V25() ext-real Element of REAL
n * n is V17() V18() V19() V23() V24() V25() finite cardinal integer ext-real non negative Element of NAT
3 * n is V17() V18() V19() V23() V24() V25() finite cardinal integer ext-real non negative Element of NAT
(n * n) + (3 * n) is V17() V18() V19() V23() V24() V25() finite cardinal integer ext-real non negative Element of NAT
((n * n) + (3 * n)) + 1 is non empty V17() V18() V19() V23() V24() V25() finite cardinal integer ext-real positive non negative Element of NAT
v2 is set
VG is V17() V18() V19() V23() V24() V25() finite cardinal integer ext-real non negative Element of NAT
((((REAL *),((REAL *),(n),(n))) . (i + 1)),f) . VG is V24() V25() ext-real Element of REAL
((n),((n),((((REAL *),((REAL *),(n),(n))) . i),f))) . VG is V24() V25() ext-real Element of REAL
((n),((((REAL *),((REAL *),(n),(n))) . i),f)) . VG is V24() V25() ext-real Element of REAL
((((REAL *),((REAL *),(n),(n))) . i),f) . VG is V24() V25() ext-real Element of REAL
v2 is V17() V18() V19() V23() V24() V25() finite cardinal integer ext-real non negative Element of NAT
((n),((((REAL *),((REAL *),(n),(n))) . i),f)) . v2 is V24() V25() ext-real Element of REAL
n is V17() V18() V19() V23() V24() V25() finite cardinal integer ext-real non negative Element of NAT
(n) is Relation-like REAL * -defined REAL * -valued Function-like total quasi_total Element of Funcs ((REAL *),(REAL *))
(n) is Relation-like REAL * -defined REAL * -valued Function-like total quasi_total Element of Funcs ((REAL *),(REAL *))
((REAL *),(n),(n)) is Relation-like Function-like Element of Funcs ((REAL *),(REAL *))
((REAL *),((REAL *),(n),(n))) is non empty Relation-like NAT -defined Funcs ((REAL *),(REAL *)) -valued Function-like total quasi_total Element of K32(K33(NAT,(Funcs ((REAL *),(REAL *)))))
i is V17() V18() V19() V23() V24() V25() finite cardinal integer ext-real non negative Element of NAT
((REAL *),((REAL *),(n),(n))) . i is Relation-like Function-like Element of Funcs ((REAL *),(REAL *))
i + 1 is non empty V17() V18() V19() V23() V24() V25() finite cardinal integer ext-real positive non negative Element of NAT
((REAL *),((REAL *),(n),(n))) . (i + 1) is Relation-like Function-like Element of Funcs ((REAL *),(REAL *))
f is V17() V18() V19() V23() V24() V25() finite cardinal integer ext-real non negative Element of NAT
{f} is non empty V5() finite V30() 1 -element Element of K32(NAT)
g is Relation-like NAT -defined REAL -valued Function-like finite FinSequence-like FinSubsequence-like V88() V89() V90() Element of REAL *
(g,n) is finite Element of K32(NAT)
dom g is finite Element of K32(NAT)
{ b₁ where b₁ is V17() V18() V19() V23() V24() V25() finite cardinal integer ext-real non negative Element of NAT : ( b₁ in dom g & 1 <= b₁ & b₁ <= n & not g . b₁ = - 1 & not g . (n + b₁) = - 1 ) } is set
((g,n),g,n) is V17() V18() V19() V23() V24() V25() finite cardinal integer ext-real non negative Element of NAT
(g,n) is Element of K32(NAT)
{ b₁ where b₁ is V17() V18() V19() V23() V24() V25() finite cardinal integer ext-real non negative Element of NAT : ( b₁ in dom g & 1 <= b₁ & b₁ <= n & g . b₁ = - 1 ) } is set
(g,n) \/ {f} is non empty Element of K32(NAT)
G is Relation-like NAT -defined REAL -valued Function-like finite FinSequence-like FinSubsequence-like V88() V89() V90() Element of REAL *
((((REAL *),((REAL *),(n),(n))) . i),G) is Relation-like NAT -defined REAL -valued Function-like finite FinSequence-like FinSubsequence-like V88() V89() V90() Element of REAL *
((((REAL *),((REAL *),(n),(n))) . (i + 1)),G) is Relation-like NAT -defined REAL -valued Function-like finite FinSequence-like FinSubsequence-like V88() V89() V90() Element of REAL *
W is Relation-like NAT -defined REAL -valued Function-like finite FinSequence-like FinSubsequence-like V88() V89() V90() Element of REAL *
(W,n) is Element of K32(NAT)
dom W is finite Element of K32(NAT)
{ b₁ where b₁ is V17() V18() V19() V23() V24() V25() finite cardinal integer ext-real non negative Element of NAT : ( b₁ in dom W & 1 <= b₁ & b₁ <= n & W . b₁ = - 1 ) } is set
n * n is V17() V18() V19() V23() V24() V25() finite cardinal integer ext-real non negative Element of NAT
3 * n is V17() V18() V19() V23() V24() V25() finite cardinal integer ext-real non negative Element of NAT
(n * n) + (3 * n) is V17() V18() V19() V23() V24() V25() finite cardinal integer ext-real non negative Element of NAT
((n * n) + (3 * n)) + 1 is non empty V17() V18() V19() V23() V24() V25() finite cardinal integer ext-real positive non negative Element of NAT
((n),((((REAL *),((REAL *),(n),(n))) . i),G)) is Relation-like NAT -defined REAL -valued Function-like finite FinSequence-like FinSubsequence-like V88() V89() V90() Element of REAL *
((((n * n) + (3 * n)) + 1),f,((((REAL *),((REAL *),(n),(n))) . i),G),(- 1)) is Relation-like NAT -defined REAL -valued Function-like finite FinSequence-like FinSubsequence-like V88() V89() V90() FinSequence of REAL
(((((REAL *),((REAL *),(n),(n))) . i),G),(((n * n) + (3 * n)) + 1),f) is Relation-like NAT -defined REAL -valued Function-like finite FinSequence-like FinSubsequence-like V88() V89() V90() FinSequence of REAL
((((((REAL *),((REAL *),(n),(n))) . i),G),(((n * n) + (3 * n)) + 1),f),f,(- 1)) is Relation-like NAT -defined REAL -valued Function-like finite FinSequence-like FinSubsequence-like V88() V89() V90() FinSequence of REAL
dom ((((REAL *),((REAL *),(n),(n))) . i),G) is finite Element of K32(NAT)
dom ((n),((((REAL *),((REAL *),(n),(n))) . i),G)) is finite Element of K32(NAT)
R is set
M is V17() V18() V19() V23() V24() V25() finite cardinal integer ext-real non negative Element of NAT
g . M is V24() V25() ext-real Element of REAL
W . M is V24() V25() ext-real Element of REAL
((n),((n),((((REAL *),((REAL *),(n),(n))) . i),G))) is Relation-like NAT -defined REAL -valued Function-like finite FinSequence-like FinSubsequence-like V88() V89() V90() Element of REAL *
((n),((n),((((REAL *),((REAL *),(n),(n))) . i),G))) . M is V24() V25() ext-real Element of REAL
((n),((((REAL *),((REAL *),(n),(n))) . i),G)) . M is V24() V25() ext-real Element of REAL
W . f is V24() V25() ext-real Element of REAL
((n),((n),((((REAL *),((REAL *),(n),(n))) . i),G))) is Relation-like NAT -defined REAL -valued Function-like finite FinSequence-like FinSubsequence-like V88() V89() V90() Element of REAL *
((n),((n),((((REAL *),((REAL *),(n),(n))) . i),G))) . f is V24() V25() ext-real Element of REAL
((n),((((REAL *),((REAL *),(n),(n))) . i),G)) . f is V24() V25() ext-real Element of REAL
R is set
M is V17() V18() V19() V23() V24() V25() finite cardinal integer ext-real non negative Element of NAT
W . M is V24() V25() ext-real Element of REAL
((n),((n),((((REAL *),((REAL *),(n),(n))) . i),G))) is Relation-like NAT -defined REAL -valued Function-like finite FinSequence-like FinSubsequence-like V88() V89() V90() Element of REAL *
((n),((n),((((REAL *),((REAL *),(n),(n))) . i),G))) . M is V24() V25() ext-real Element of REAL
((n),((((REAL *),((REAL *),(n),(n))) . i),G)) . M is V24() V25() ext-real Element of REAL
((((REAL *),((REAL *),(n),(n))) . i),G) . M is V24() V25() ext-real Element of REAL
{ b₁ where b₁ is V17() V18() V19() V23() V24() V25() finite cardinal integer ext-real non negative Element of NAT : ( b₁ in dom ((((REAL *),((REAL *),(n),(n))) . i),G) & 1 <= b₁ & b₁ <= n & ((((REAL *),((REAL *),(n),(n))) . i),G) . b₁ = - 1 ) } is set
R is V17() V18() V19() V23() V24() V25() finite cardinal integer ext-real non negative Element of NAT
g . R is V24() V25() ext-real Element of REAL
n is V17() V18() V19() V23() V24() V25() finite cardinal integer ext-real non negative Element of NAT
(n) is Relation-like REAL * -defined REAL * -valued Function-like total quasi_total Element of Funcs ((REAL *),(REAL *))
(n) is Relation-like REAL * -defined REAL * -valued Function-like total quasi_total Element of Funcs ((REAL *),(REAL *))
((REAL *),(n),(n)) is Relation-like Function-like Element of Funcs ((REAL *),(REAL *))
((REAL *),((REAL *),(n),(n))) is non empty Relation-like NAT -defined Funcs ((REAL *),(REAL *)) -valued Function-like total quasi_total Element of K32(K33(NAT,(Funcs ((REAL *),(REAL *)))))
i is Relation-like NAT -defined REAL -valued Function-like finite FinSequence-like FinSubsequence-like V88() V89() V90() Element of REAL *
((REAL *),((REAL *),(n),(n))) . n is Relation-like Function-like Element of Funcs ((REAL *),(REAL *))
((((REAL *),((REAL *),(n),(n))) . n),i) is Relation-like NAT -defined REAL -valued Function-like finite FinSequence-like FinSubsequence-like V88() V89() V90() Element of REAL *
W is V17() V18() V19() V23() V24() V25() finite cardinal integer ext-real non negative Element of NAT
((REAL *),((REAL *),(n),(n))) . W is Relation-like Function-like Element of Funcs ((REAL *),(REAL *))
((((REAL *),((REAL *),(n),(n))) . W),i) is Relation-like NAT -defined REAL -valued Function-like finite FinSequence-like FinSubsequence-like V88() V89() V90() Element of REAL *
(((((REAL *),((REAL *),(n),(n))) . W),i),n) is finite Element of K32(NAT)
dom ((((REAL *),((REAL *),(n),(n))) . W),i) is finite Element of K32(NAT)
{ b₁ where b₁ is V17() V18() V19() V23() V24() V25() finite cardinal integer ext-real non negative Element of NAT : ( b₁ in dom ((((REAL *),((REAL *),(n),(n))) . W),i) & 1 <= b₁ & b₁ <= n & not ((((REAL *),((REAL *),(n),(n))) . W),i) . b₁ = - 1 ) } is set
card (((((REAL *),((REAL *),(n),(n))) . W),i),n) is V17() V18() V19() V23() V24() V25() finite cardinal integer ext-real non negative Element of NAT
n - W is V24() V25() integer ext-real Element of REAL
W + 1 is non empty V17() V18() V19() V23() V24() V25() finite cardinal integer ext-real positive non negative Element of NAT
((REAL *),((REAL *),(n),(n))) . (W + 1) is Relation-like Function-like Element of Funcs ((REAL *),(REAL *))
((((REAL *),((REAL *),(n),(n))) . (W + 1)),i) is Relation-like NAT -defined REAL -valued Function-like finite FinSequence-like FinSubsequence-like V88() V89() V90() Element of REAL *
(((((REAL *),((REAL *),(n),(n))) . (W + 1)),i),n) is finite Element of K32(NAT)
dom ((((REAL *),((REAL *),(n),(n))) . (W + 1)),i) is finite Element of K32(NAT)
{ b₁ where b₁ is V17() V18() V19() V23() V24() V25() finite cardinal integer ext-real non negative Element of NAT : ( b₁ in dom ((((REAL *),((REAL *),(n),(n))) . (W + 1)),i) & 1 <= b₁ & b₁ <= n & not ((((REAL *),((REAL *),(n),(n))) . (W + 1)),i) . b₁ = - 1 ) } is set
card (((((REAL *),((REAL *),(n),(n))) . (W + 1)),i),n) is V17() V18() V19() V23() V24() V25() finite cardinal integer ext-real non negative Element of NAT
n - (W + 1) is V24() V25() integer ext-real Element of REAL
(((((REAL *),((REAL *),(n),(n))) . W),i),n) is finite Element of K32(NAT)
{ b₁ where b₁ is V17() V18() V19() V23() V24() V25() finite cardinal integer ext-real non negative Element of NAT : ( b₁ in dom ((((REAL *),((REAL *),(n),(n))) . W),i) & 1 <= b₁ & b₁ <= n & not ((((REAL *),((REAL *),(n),(n))) . W),i) . b₁ = - 1 & not ((((REAL *),((REAL *),(n),(n))) . W),i) . (n + b₁) = - 1 ) } is set
(card (((((REAL *),((REAL *),(n),(n))) . (W + 1)),i),n)) + 1 is non empty V17() V18() V19() V23() V24() V25() finite cardinal integer ext-real positive non negative Element of NAT
(n - W) - 1 is V24() V25() integer ext-real Element of REAL
((REAL *),((REAL *),(n),(n))) . 0 is Relation-like Function-like Element of Funcs ((REAL *),(REAL *))
((((REAL *),((REAL *),(n),(n))) . 0),i) is Relation-like NAT -defined REAL -valued Function-like finite FinSequence-like FinSubsequence-like V88() V89() V90() Element of REAL *
(((((REAL *),((REAL *),(n),(n))) . 0),i),n) is finite Element of K32(NAT)
dom ((((REAL *),((REAL *),(n),(n))) . 0),i) is finite Element of K32(NAT)
{ b₁ where b₁ is V17() V18() V19() V23() V24() V25() finite cardinal integer ext-real non negative Element of NAT : ( b₁ in dom ((((REAL *),((REAL *),(n),(n))) . 0),i) & 1 <= b₁ & b₁ <= n & not ((((REAL *),((REAL *),(n),(n))) . 0),i) . b₁ = - 1 ) } is set
card (((((REAL *),((REAL *),(n),(n))) . 0),i),n) is V17() V18() V19() V23() V24() V25() finite cardinal integer ext-real non negative Element of NAT
n - 0 is V24() V25() integer ext-real non negative Element of REAL
Seg n is finite n -element Element of K32(NAT)
card (Seg n) is V17() V18() V19() V23() V24() V25() finite cardinal integer ext-real non negative Element of NAT
(((((REAL *),((REAL *),(n),(n))) . n),i),n) is finite Element of K32(NAT)
dom ((((REAL *),((REAL *),(n),(n))) . n),i) is finite Element of K32(NAT)
{ b₁ where b₁ is V17() V18() V19() V23() V24() V25() finite cardinal integer ext-real non negative Element of NAT : ( b₁ in dom ((((REAL *),((REAL *),(n),(n))) . n),i) & 1 <= b₁ & b₁ <= n & not ((((REAL *),((REAL *),(n),(n))) . n),i) . b₁ = - 1 ) } is set
card (((((REAL *),((REAL *),(n),(n))) . n),i),n) is V17() V18() V19() V23() V24() V25() finite cardinal integer ext-real non negative Element of NAT
n - n is V24() V25() integer ext-real Element of REAL
(((((REAL *),((REAL *),(n),(n))) . n),i),n) is finite Element of K32(NAT)
{ b₁ where b₁ is V17() V18() V19() V23() V24() V25() finite cardinal integer ext-real non negative Element of NAT : ( b₁ in dom ((((REAL *),((REAL *),(n),(n))) . n),i) & 1 <= b₁ & b₁ <= n & not ((((REAL *),((REAL *),(n),(n))) . n),i) . b₁ = - 1 & not ((((REAL *),((REAL *),(n),(n))) . n),i) . (n + b₁) = - 1 ) } is set
n is V17() V18() V19() V23() V24() V25() finite cardinal integer ext-real non negative Element of NAT
i is V17() V18() V19() V23() V24() V25() finite cardinal integer ext-real non negative Element of NAT
n - i is V24() V25() integer ext-real Element of REAL
n + i is V17() V18() V19() V23() V24() V25() finite cardinal integer ext-real non negative Element of NAT
n is Relation-like NAT -defined NAT -valued Function-like finite FinSequence-like FinSubsequence-like V88() V89() V90() V91() FinSequence of NAT
len n is V17() V18() V19() V23() V24() V25() finite cardinal integer ext-real non negative Element of NAT
i is Relation-like NAT -defined NAT -valued Function-like finite FinSequence-like FinSubsequence-like V88() V89() V90() V91() FinSequence of NAT
len i is V17() V18() V19() V23() V24() V25() finite cardinal integer ext-real non negative Element of NAT
n . (len n) is V17() V18() V19() V23() V24() V25() finite cardinal integer ext-real non negative Element of REAL
i . (len i) is V17() V18() V19() V23() V24() V25() finite cardinal integer ext-real non negative Element of REAL
f is Relation-like NAT -defined REAL -valued Function-like finite FinSequence-like FinSubsequence-like V88() V89() V90() Element of REAL *
G is V17() V18() V19() V23() V24() V25() finite cardinal integer ext-real non negative Element of NAT
W is V17() V18() V19() V23() V24() V25() finite cardinal integer ext-real non negative Element of NAT
(len n) - W is V24() V25() integer ext-real Element of REAL
n . ((len n) - W) is V17() V18() V19() V23() V24() V25() finite cardinal integer ext-real non negative Element of REAL
(len i) - W is V24() V25() integer ext-real Element of REAL
i . ((len i) - W) is V17() V18() V19() V23() V24() V25() finite cardinal integer ext-real non negative Element of REAL
W + 1 is non empty V17() V18() V19() V23() V24() V25() finite cardinal integer ext-real positive non negative Element of NAT
(len n) - (W + 1) is V24() V25() integer ext-real Element of REAL
n . ((len n) - (W + 1)) is V17() V18() V19() V23() V24() V25() finite cardinal integer ext-real non negative Element of REAL
(len i) - (W + 1) is V24() V25() integer ext-real Element of REAL
i . ((len i) - (W + 1)) is V17() V18() V19() V23() V24() V25() finite cardinal integer ext-real non negative Element of REAL
n /. ((len n) - W) is V17() V18() V19() V23() V24() V25() finite cardinal integer ext-real non negative Element of NAT
i /. ((len i) - W) is V17() V18() V19() V23() V24() V25() finite cardinal integer ext-real non negative Element of NAT
((len n) - (W + 1)) + 1 is V24() V25() integer ext-real Element of REAL
n /. (((len n) - (W + 1)) + 1) is V17() V18() V19() V23() V24() V25() finite cardinal integer ext-real non negative Element of NAT
(n /. (((len n) - (W + 1)) + 1)) + G is V17() V18() V19() V23() V24() V25() finite cardinal integer ext-real non negative Element of NAT
f . ((n /. (((len n) - (W + 1)) + 1)) + G) is V24() V25() ext-real Element of REAL
((len i) - (W + 1)) + 1 is V24() V25() integer ext-real Element of REAL
i /. (((len i) - (W + 1)) + 1) is V17() V18() V19() V23() V24() V25() finite cardinal integer ext-real non negative Element of NAT
(i /. (((len i) - (W + 1)) + 1)) + G is V17() V18() V19() V23() V24() V25() finite cardinal integer ext-real non negative Element of NAT
f . ((i /. (((len i) - (W + 1)) + 1)) + G) is V24() V25() ext-real Element of REAL
(len n) - 0 is V24() V25() integer ext-real non negative Element of REAL
n . ((len n) - 0) is V17() V18() V19() V23() V24() V25() finite cardinal integer ext-real non negative Element of REAL
(len i) - 0 is V24() V25() integer ext-real non negative Element of REAL
i . ((len i) - 0) is V17() V18() V19() V23() V24() V25() finite cardinal integer ext-real non negative Element of REAL
W is V17() V18() V19() V23() V24() V25() finite cardinal integer ext-real non negative Element of NAT
(len n) - W is V24() V25() integer ext-real Element of REAL
n . ((len n) - W) is V17() V18() V19() V23() V24() V25() finite cardinal integer ext-real non negative Element of REAL
(len i) - W is V24() V25() integer ext-real Element of REAL
i . ((len i) - W) is V17() V18() V19() V23() V24() V25() finite cardinal integer ext-real non negative Element of REAL
n is V17() V18() V19() V23() V24() V25() finite cardinal integer ext-real non negative Element of NAT
(n) is Relation-like REAL * -defined REAL * -valued Function-like total quasi_total Element of Funcs ((REAL *),(REAL *))
(n) is Relation-like REAL * -defined REAL * -valued Function-like total quasi_total Element of Funcs ((REAL *),(REAL *))
((REAL *),(n),(n)) is Relation-like Function-like Element of Funcs ((REAL *),(REAL *))
((REAL *),((REAL *),(n),(n))) is non empty Relation-like NAT -defined Funcs ((REAL *),(REAL *)) -valued Function-like total quasi_total Element of K32(K33(NAT,(Funcs ((REAL *),(REAL *)))))
i is V17() V18() V19() V23() V24() V25() finite cardinal integer ext-real non negative Element of NAT
((REAL *),((REAL *),(n),(n))) . i is Relation-like Function-like Element of Funcs ((REAL *),(REAL *))
f is Relation-like NAT -defined REAL -valued Function-like finite FinSequence-like FinSubsequence-like V88() V89() V90() Element of REAL *
dom f is finite Element of K32(NAT)
((((REAL *),((REAL *),(n),(n))) . i),f) is Relation-like NAT -defined REAL -valued Function-like finite FinSequence-like FinSubsequence-like V88() V89() V90() Element of REAL *
dom ((((REAL *),((REAL *),(n),(n))) . i),f) is finite Element of K32(NAT)
((REAL *),((REAL *),(n),(n))) . 0 is Relation-like Function-like Element of Funcs ((REAL *),(REAL *))
((((REAL *),((REAL *),(n),(n))) . 0),f) is Relation-like NAT -defined REAL -valued Function-like finite FinSequence-like FinSubsequence-like V88() V89() V90() Element of REAL *
dom ((((REAL *),((REAL *),(n),(n))) . 0),f) is finite Element of K32(NAT)
id (REAL *) is non empty Relation-like Function-like one-to-one Element of Funcs ((REAL *),(REAL *))
((id (REAL *)),f) is Relation-like NAT -defined REAL -valued Function-like finite FinSequence-like FinSubsequence-like V88() V89() V90() Element of REAL *
dom ((id (REAL *)),f) is finite Element of K32(NAT)
W is V17() V18() V19() V23() V24() V25() finite cardinal integer ext-real non negative Element of NAT
((REAL *),((REAL *),(n),(n))) . W is Relation-like Function-like Element of Funcs ((REAL *),(REAL *))
((((REAL *),((REAL *),(n),(n))) . W),f) is Relation-like NAT -defined REAL -valued Function-like finite FinSequence-like FinSubsequence-like V88() V89() V90() Element of REAL *
dom ((((REAL *),((REAL *),(n),(n))) . W),f) is finite Element of K32(NAT)
W + 1 is non empty V17() V18() V19() V23() V24() V25() finite cardinal integer ext-real positive non negative Element of NAT
((REAL *),((REAL *),(n),(n))) . (W + 1) is Relation-like Function-like Element of Funcs ((REAL *),(REAL *))
((((REAL *),((REAL *),(n),(n))) . (W + 1)),f) is Relation-like NAT -defined REAL -valued Function-like finite FinSequence-like FinSubsequence-like V88() V89() V90() Element of REAL *
dom ((((REAL *),((REAL *),(n),(n))) . (W + 1)),f) is finite Element of K32(NAT)
n is V17() V18() V19() V23() V24() V25() finite cardinal integer ext-real non negative Element of NAT
i is V17() V18() V19() V23() V24() V25() finite cardinal integer ext-real non negative Element of NAT
f is Relation-like NAT -defined REAL -valued Function-like finite FinSequence-like FinSubsequence-like V88() V89() V90() Element of REAL *
dom f is finite Element of K32(NAT)
g is V17() V18() V19() V23() V24() V25() finite cardinal integer ext-real non negative Element of NAT
f . g is V24() V25() ext-real Element of REAL
n is V17() V18() V19() V23() V24() V25() finite cardinal integer ext-real non negative Element of NAT
i is V17() V18() V19() V23() V24() V25() finite cardinal integer ext-real non negative Element of NAT
f is Relation-like NAT -defined REAL -valued Function-like finite FinSequence-like FinSubsequence-like V88() V89() V90() Element of REAL *
g is Relation-like NAT -defined REAL -valued Function-like finite FinSequence-like FinSubsequence-like V88() V89() V90() Element of REAL *
G is Relation-like NAT -defined REAL -valued Function-like finite FinSequence-like FinSubsequence-like V88() V89() V90() Element of REAL *
dom f is finite Element of K32(NAT)
dom g is finite Element of K32(NAT)
W is V17() V18() V19() V23() V24() V25() finite cardinal integer ext-real non negative Element of NAT
f . W is V24() V25() ext-real Element of REAL
g . W is V24() V25() ext-real Element of REAL
G . W is V24() V25() ext-real Element of REAL
dom G is finite Element of K32(NAT)
n is V17() V18() V19() V23() V24() V25() finite cardinal integer ext-real non negative Element of NAT
(n) is Relation-like REAL * -defined REAL * -valued Function-like total quasi_total Element of Funcs ((REAL *),(REAL *))
(n) is Relation-like REAL * -defined REAL * -valued Function-like total quasi_total Element of Funcs ((REAL *),(REAL *))
((REAL *),(n),(n)) is Relation-like Function-like Element of Funcs ((REAL *),(REAL *))
((REAL *),((REAL *),(n),(n))) is non empty Relation-like NAT -defined Funcs ((REAL *),(REAL *)) -valued Function-like total quasi_total Element of K32(K33(NAT,(Funcs ((REAL *),(REAL *)))))
3 * n is V17() V18() V19() V23() V24() V25() finite cardinal integer ext-real non negative Element of NAT
(3 * n) + 1 is non empty V17() V18() V19() V23() V24() V25() finite cardinal integer ext-real positive non negative Element of NAT
n * n is V17() V18() V19() V23() V24() V25() finite cardinal integer ext-real non negative Element of NAT
(n * n) + (3 * n) is V17() V18() V19() V23() V24() V25() finite cardinal integer ext-real non negative Element of NAT
i is V17() V18() V19() V23() V24() V25() finite cardinal integer ext-real non negative Element of NAT
((REAL *),((REAL *),(n),(n))) . i is Relation-like Function-like Element of Funcs ((REAL *),(REAL *))
i + 1 is non empty V17() V18() V19() V23() V24() V25() finite cardinal integer ext-real positive non negative Element of NAT
((REAL *),((REAL *),(n),(n))) . (i + 1) is Relation-like Function-like Element of Funcs ((REAL *),(REAL *))
f is Relation-like NAT -defined REAL -valued Function-like finite FinSequence-like FinSubsequence-like V88() V89() V90() Element of REAL *
((((REAL *),((REAL *),(n),(n))) . i),f) is Relation-like NAT -defined REAL -valued Function-like finite FinSequence-like FinSubsequence-like V88() V89() V90() Element of REAL *
((((REAL *),((REAL *),(n),(n))) . (i + 1)),f) is Relation-like NAT -defined REAL -valued Function-like finite FinSequence-like FinSubsequence-like V88() V89() V90() Element of REAL *
v2 is V17() V18() V19() V23() V24() V25() finite cardinal integer ext-real non negative Element of NAT
dom ((((REAL *),((REAL *),(n),(n))) . i),f) is finite Element of K32(NAT)
((n),((((REAL *),((REAL *),(n),(n))) . i),f)) is Relation-like NAT -defined REAL -valued Function-like finite FinSequence-like FinSubsequence-like V88() V89() V90() Element of REAL *
dom ((n),((((REAL *),((REAL *),(n),(n))) . i),f)) is finite Element of K32(NAT)
((n * n) + (3 * n)) + 1 is non empty V17() V18() V19() V23() V24() V25() finite cardinal integer ext-real positive non negative Element of NAT
((((REAL *),((REAL *),(n),(n))) . (i + 1)),f) . v2 is V24() V25() ext-real Element of REAL
((n),((n),((((REAL *),((REAL *),(n),(n))) . i),f))) is Relation-like NAT -defined REAL -valued Function-like finite FinSequence-like FinSubsequence-like V88() V89() V90() Element of REAL *
((n),((n),((((REAL *),((REAL *),(n),(n))) . i),f))) . v2 is V24() V25() ext-real Element of REAL
((n),((((REAL *),((REAL *),(n),(n))) . i),f)) . v2 is V24() V25() ext-real Element of REAL
((((REAL *),((REAL *),(n),(n))) . i),f) . v2 is V24() V25() ext-real Element of REAL
dom ((((REAL *),((REAL *),(n),(n))) . (i + 1)),f) is finite Element of K32(NAT)
n is Relation-like REAL * -defined REAL * -valued Function-like total quasi_total Element of Funcs ((REAL *),(REAL *))
i is Relation-like NAT -defined REAL -valued Function-like finite FinSequence-like FinSubsequence-like V88() V89() V90() Element of REAL *
f is V17() V18() V19() V23() V24() V25() finite cardinal integer ext-real non negative Element of NAT
(n,i,f) is V17() V18() V19() V23() V24() V25() finite cardinal integer ext-real non negative Element of NAT
g is V17() V18() V19() V23() V24() V25() finite cardinal integer ext-real non negative Element of NAT
((REAL *),n) is non empty Relation-like NAT -defined Funcs ((REAL *),(REAL *)) -valued Function-like total quasi_total Element of K32(K33(NAT,(Funcs ((REAL *),(REAL *)))))
((REAL *),n) . g is Relation-like Function-like Element of Funcs ((REAL *),(REAL *))
((((REAL *),n) . g),i) is Relation-like NAT -defined REAL -valued Function-like finite FinSequence-like FinSubsequence-like V88() V89() V90() Element of REAL *
(((((REAL *),n) . g),i),f) is finite Element of K32(NAT)
dom ((((REAL *),n) . g),i) is finite Element of K32(NAT)
{ b₁ where b₁ is V17() V18() V19() V23() V24() V25() finite cardinal integer ext-real non negative Element of NAT : ( b₁ in dom ((((REAL *),n) . g),i) & 1 <= b₁ & b₁ <= f & not ((((REAL *),n) . g),i) . b₁ = - 1 & not ((((REAL *),n) . g),i) . (f + b₁) = - 1 ) } is set
n is V17() V18() V19() V23() V24() V25() finite cardinal integer ext-real non negative Element of NAT
(n) is Relation-like REAL * -defined REAL * -valued Function-like total quasi_total Element of Funcs ((REAL *),(REAL *))
(n) is Relation-like REAL * -defined REAL * -valued Function-like total quasi_total Element of Funcs ((REAL *),(REAL *))
((REAL *),(n),(n)) is Relation-like Function-like Element of Funcs ((REAL *),(REAL *))
((REAL *),((REAL *),(n),(n))) is non empty Relation-like NAT -defined Funcs ((REAL *),(REAL *)) -valued Function-like total quasi_total Element of K32(K33(NAT,(Funcs ((REAL *),(REAL *)))))
3 * n is V17() V18() V19() V23() V24() V25() finite cardinal integer ext-real non negative Element of NAT
(3 * n) + 1 is non empty V17() V18() V19() V23() V24() V25() finite cardinal integer ext-real positive non negative Element of NAT
n * n is V17() V18() V19() V23() V24() V25() finite cardinal integer ext-real non negative Element of NAT
(n * n) + (3 * n) is V17() V18() V19() V23() V24() V25() finite cardinal integer ext-real non negative Element of NAT
i is V17() V18() V19() V23() V24() V25() finite cardinal integer ext-real non negative Element of NAT
((REAL *),((REAL *),(n),(n))) . i is Relation-like Function-like Element of Funcs ((REAL *),(REAL *))
f is Relation-like NAT -defined REAL -valued Function-like finite FinSequence-like FinSubsequence-like V88() V89() V90() Element of REAL *
((((REAL *),((REAL *),(n),(n))) . i),f) is Relation-like NAT -defined REAL -valued Function-like finite FinSequence-like FinSubsequence-like V88() V89() V90() Element of REAL *
v2 is V17() V18() V19() V23() V24() V25() finite cardinal integer ext-real non negative Element of NAT
((REAL *),((REAL *),(n),(n))) . v2 is Relation-like Function-like Element of Funcs ((REAL *),(REAL *))
((((REAL *),((REAL *),(n),(n))) . v2),f) is Relation-like NAT -defined REAL -valued Function-like finite FinSequence-like FinSubsequence-like V88() V89() V90() Element of REAL *
v2 + 1 is non empty V17() V18() V19() V23() V24() V25() finite cardinal integer ext-real positive non negative Element of NAT
((REAL *),((REAL *),(n),(n))) . (v2 + 1) is Relation-like Function-like Element of Funcs ((REAL *),(REAL *))
((((REAL *),((REAL *),(n),(n))) . (v2 + 1)),f) is Relation-like NAT -defined REAL -valued Function-like finite FinSequence-like FinSubsequence-like V88() V89() V90() Element of REAL *
((REAL *),((REAL *),(n),(n))) . 0 is Relation-like Function-like Element of Funcs ((REAL *),(REAL *))
((((REAL *),((REAL *),(n),(n))) . 0),f) is Relation-like NAT -defined REAL -valued Function-like finite FinSequence-like FinSubsequence-like V88() V89() V90() Element of REAL *
{1} is non empty V5() finite V30() 1 -element Element of K32(NAT)
n is V17() V18() V19() V23() V24() V25() finite cardinal integer ext-real non negative Element of NAT
n + 1 is non empty V17() V18() V19() V23() V24() V25() finite cardinal integer ext-real positive non negative Element of NAT
(n) is Relation-like REAL * -defined REAL * -valued Function-like total quasi_total Element of Funcs ((REAL *),(REAL *))
(n) is Relation-like REAL * -defined REAL * -valued Function-like total quasi_total Element of Funcs ((REAL *),(REAL *))
((REAL *),(n),(n)) is Relation-like Function-like Element of Funcs ((REAL *),(REAL *))
((REAL *),((REAL *),(n),(n))) is non empty Relation-like NAT -defined Funcs ((REAL *),(REAL *)) -valued Function-like total quasi_total Element of K32(K33(NAT,(Funcs ((REAL *),(REAL *)))))
((REAL *),((REAL *),(n),(n))) . 1 is Relation-like Function-like Element of Funcs ((REAL *),(REAL *))
i is Relation-like NAT -defined REAL -valued Function-like finite FinSequence-like FinSubsequence-like V88() V89() V90() Element of REAL *
dom i is finite Element of K32(NAT)
i . (n + 1) is V24() V25() ext-real Element of REAL
(i,n) is finite Element of K32(NAT)
{ b₁ where b₁ is V17() V18() V19() V23() V24() V25() finite cardinal integer ext-real non negative Element of NAT : ( b₁ in dom i & 1 <= b₁ & b₁ <= n & not i . b₁ = - 1 & not i . (n + b₁) = - 1 ) } is set
((i,n),i,n) is V17() V18() V19() V23() V24() V25() finite cardinal integer ext-real non negative Element of NAT
(i,n) is Element of K32(NAT)
{ b₁ where b₁ is V17() V18() V19() V23() V24() V25() finite cardinal integer ext-real non negative Element of NAT : ( b₁ in dom i & 1 <= b₁ & b₁ <= n & i . b₁ = - 1 ) } is set
((((REAL *),((REAL *),(n),(n))) . 1),i) is Relation-like NAT -defined REAL -valued Function-like finite FinSequence-like FinSubsequence-like V88() V89() V90() Element of REAL *
(((((REAL *),((REAL *),(n),(n))) . 1),i),n) is Element of K32(NAT)
dom ((((REAL *),((REAL *),(n),(n))) . 1),i) is finite Element of K32(NAT)
{ b₁ where b₁ is V17() V18() V19() V23() V24() V25() finite cardinal integer ext-real non negative Element of NAT : ( b₁ in dom ((((REAL *),((REAL *),(n),(n))) . 1),i) & 1 <= b₁ & b₁ <= n & ((((REAL *),((REAL *),(n),(n))) . 1),i) . b₁ = - 1 ) } is set
((REAL *),((REAL *),(n),(n))) . 0 is Relation-like Function-like Element of Funcs ((REAL *),(REAL *))
((((REAL *),((REAL *),(n),(n))) . 0),i) is Relation-like NAT -defined REAL -valued Function-like finite FinSequence-like FinSubsequence-like V88() V89() V90() Element of REAL *
i . 1 is V24() V25() ext-real Element of REAL
{ b₁ where b₁ is V17() V18() V19() V23() V24() V25() finite cardinal integer ext-real non negative Element of NAT : ( b₁ in dom i & 1 <= b₁ & b₁ <= n & not i . b₁ = - 1 & not i . (n + b₁) = - 1 ) } is set
1 + 1 is non empty V17() V18() V19() V23() V24() V25() finite cardinal integer ext-real positive non negative Element of NAT
n + ((i,n),i,n) is V17() V18() V19() V23() V24() V25() finite cardinal integer ext-real non negative Element of NAT
i . (n + ((i,n),i,n)) is V24() V25() ext-real Element of REAL
v2 is set
VG is V17() V18() V19() V23() V24() V25() finite cardinal integer ext-real non negative Element of NAT
i . VG is V24() V25() ext-real Element of REAL
(((((REAL *),((REAL *),(n),(n))) . 0),i),n) is finite Element of K32(NAT)
dom ((((REAL *),((REAL *),(n),(n))) . 0),i) is finite Element of K32(NAT)
{ b₁ where b₁ is V17() V18() V19() V23() V24() V25() finite cardinal integer ext-real non negative Element of NAT : ( b₁ in dom ((((REAL *),((REAL *),(n),(n))) . 0),i) & 1 <= b₁ & b₁ <= n & not ((((REAL *),((REAL *),(n),(n))) . 0),i) . b₁ = - 1 & not ((((REAL *),((REAL *),(n),(n))) . 0),i) . (n + b₁) = - 1 ) } is set
((((((REAL *),((REAL *),(n),(n))) . 0),i),n),((((REAL *),((REAL *),(n),(n))) . 0),i),n) is V17() V18() V19() V23() V24() V25() finite cardinal integer ext-real non negative Element of NAT
((i,n),((((REAL *),((REAL *),(n),(n))) . 0),i),n) is V17() V18() V19() V23() V24() V25() finite cardinal integer ext-real non negative Element of NAT
0 + 1 is non empty V17() V18() V19() V23() V24() V25() finite cardinal integer ext-real positive non negative Element of NAT
((REAL *),((REAL *),(n),(n))) . (0 + 1) is Relation-like Function-like Element of Funcs ((REAL *),(REAL *))
((((REAL *),((REAL *),(n),(n))) . (0 + 1)),i) is Relation-like NAT -defined REAL -valued Function-like finite FinSequence-like FinSubsequence-like V88() V89() V90() Element of REAL *
(((((REAL *),((REAL *),(n),(n))) . (0 + 1)),i),n) is Element of K32(NAT)
dom ((((REAL *),((REAL *),(n),(n))) . (0 + 1)),i) is finite Element of K32(NAT)
{ b₁ where b₁ is V17() V18() V19() V23() V24() V25() finite cardinal integer ext-real non negative Element of NAT : ( b₁ in dom ((((REAL *),((REAL *),(n),(n))) . (0 + 1)),i) & 1 <= b₁ & b₁ <= n & ((((REAL *),((REAL *),(n),(n))) . (0 + 1)),i) . b₁ = - 1 ) } is set
(((((REAL *),((REAL *),(n),(n))) . 0),i),n) is Element of K32(NAT)
{ b₁ where b₁ is V17() V18() V19() V23() V24() V25() finite cardinal integer ext-real non negative Element of NAT : ( b₁ in dom ((((REAL *),((REAL *),(n),(n))) . 0),i) & 1 <= b₁ & b₁ <= n & ((((REAL *),((REAL *),(n),(n))) . 0),i) . b₁ = - 1 ) } is set
(((((REAL *),((REAL *),(n),(n))) . 0),i),n) \/ {1} is non empty Element of K32(NAT)
(i,n) \/ {1} is non empty Element of K32(NAT)
n is V17() V18() V19() V23() V24() V25() finite cardinal integer ext-real non negative Element of NAT
(n) is Relation-like REAL * -defined REAL * -valued Function-like total quasi_total Element of Funcs ((REAL *),(REAL *))
(n) is Relation-like REAL * -defined REAL * -valued Function-like total quasi_total Element of Funcs ((REAL *),(REAL *))
((REAL *),(n),(n)) is Relation-like Function-like Element of Funcs ((REAL *),(REAL *))
((REAL *),((REAL *),(n),(n))) is non empty Relation-like NAT -defined Funcs ((REAL *),(REAL *)) -valued Function-like total quasi_total Element of K32(K33(NAT,(Funcs ((REAL *),(REAL *)))))
((REAL *),((REAL *),(n),(n))) . 1 is Relation-like Function-like Element of Funcs ((REAL *),(REAL *))
i is V17() V18() V19() V23() V24() V25() finite cardinal integer ext-real non negative Element of NAT
((REAL *),((REAL *),(n),(n))) . i is Relation-like Function-like Element of Funcs ((REAL *),(REAL *))
f is V17() V18() V19() V23() V24() V25() finite cardinal integer ext-real non negative Element of NAT
g is Relation-like NAT -defined REAL -valued Function-like finite FinSequence-like FinSubsequence-like V88() V89() V90() Element of REAL *
(g,n) is Element of K32(NAT)
dom g is finite Element of K32(NAT)
{ b₁ where b₁ is V17() V18() V19() V23() V24() V25() finite cardinal integer ext-real non negative Element of NAT : ( b₁ in dom g & 1 <= b₁ & b₁ <= n & g . b₁ = - 1 ) } is set
G is Relation-like NAT -defined REAL -valued Function-like finite FinSequence-like FinSubsequence-like V88() V89() V90() Element of REAL *
((((REAL *),((REAL *),(n),(n))) . 1),G) is Relation-like NAT -defined REAL -valued Function-like finite FinSequence-like FinSubsequence-like V88() V89() V90() Element of REAL *
((((REAL *),((REAL *),(n),(n))) . i),G) is Relation-like NAT -defined REAL -valued Function-like finite FinSequence-like FinSubsequence-like V88() V89() V90() Element of REAL *
(((REAL *),(n),(n)),G,n) is V17() V18() V19() V23() V24() V25() finite cardinal integer ext-real non negative Element of NAT
W is Relation-like NAT -defined REAL -valued Function-like finite FinSequence-like FinSubsequence-like V88() V89() V90() Element of REAL *
(W,n) is Element of K32(NAT)
dom W is finite Element of K32(NAT)
{ b₁ where b₁ is V17() V18() V19() V23() V24() V25() finite cardinal integer ext-real non negative Element of NAT : ( b₁ in dom W & 1 <= b₁ & b₁ <= n & W . b₁ = - 1 ) } is set
Ug is V17() V18() V19() V23() V24() V25() finite cardinal integer ext-real non negative Element of NAT
((REAL *),((REAL *),(n),(n))) . Ug is Relation-like Function-like Element of Funcs ((REAL *),(REAL *))
((((REAL *),((REAL *),(n),(n))) . Ug),G) is Relation-like NAT -defined REAL -valued Function-like finite FinSequence-like FinSubsequence-like V88() V89() V90() Element of REAL *
(((((REAL *),((REAL *),(n),(n))) . Ug),G),n) is Element of K32(NAT)
dom ((((REAL *),((REAL *),(n),(n))) . Ug),G) is finite Element of K32(NAT)
{ b₁ where b₁ is V17() V18() V19() V23() V24() V25() finite cardinal integer ext-real non negative Element of NAT : ( b₁ in dom ((((REAL *),((REAL *),(n),(n))) . Ug),G) & 1 <= b₁ & b₁ <= n & ((((REAL *),((REAL *),(n),(n))) . Ug),G) . b₁ = - 1 ) } is set
Ug + 1 is non empty V17() V18() V19() V23() V24() V25() finite cardinal integer ext-real positive non negative Element of NAT
((REAL *),((REAL *),(n),(n))) . (Ug + 1) is Relation-like Function-like Element of Funcs ((REAL *),(REAL *))
((((REAL *),((REAL *),(n),(n))) . (Ug + 1)),G) is Relation-like NAT -defined REAL -valued Function-like finite FinSequence-like FinSubsequence-like V88() V89() V90() Element of REAL *
(((((REAL *),((REAL *),(n),(n))) . (Ug + 1)),G),n) is Element of K32(NAT)
dom ((((REAL *),((REAL *),(n),(n))) . (Ug + 1)),G) is finite Element of K32(NAT)
{ b₁ where b₁ is V17() V18() V19() V23() V24() V25() finite cardinal integer ext-real non negative Element of NAT : ( b₁ in dom ((((REAL *),((REAL *),(n),(n))) . (Ug + 1)),G) & 1 <= b₁ & b₁ <= n & ((((REAL *),((REAL *),(n),(n))) . (Ug + 1)),G) . b₁ = - 1 ) } is set
(((((REAL *),((REAL *),(n),(n))) . Ug),G),n) is finite Element of K32(NAT)
{ b₁ where b₁ is V17() V18() V19() V23() V24() V25() finite cardinal integer ext-real non negative Element of NAT : ( b₁ in dom ((((REAL *),((REAL *),(n),(n))) . Ug),G) & 1 <= b₁ & b₁ <= n & not ((((REAL *),((REAL *),(n),(n))) . Ug),G) . b₁ = - 1 & not ((((REAL *),((REAL *),(n),(n))) . Ug),G) . (n + b₁) = - 1 ) } is set
((((((REAL *),((REAL *),(n),(n))) . Ug),G),n),((((REAL *),((REAL *),(n),(n))) . Ug),G),n) is V17() V18() V19() V23() V24() V25() finite cardinal integer ext-real non negative Element of NAT
{((((((REAL *),((REAL *),(n),(n))) . Ug),G),n),((((REAL *),((REAL *),(n),(n))) . Ug),G),n)} is non empty V5() finite V30() 1 -element Element of K32(NAT)
(((((REAL *),((REAL *),(n),(n))) . Ug),G),n) \/ {((((((REAL *),((REAL *),(n),(n))) . Ug),G),n),((((REAL *),((REAL *),(n),(n))) . Ug),G),n)} is non empty Element of K32(NAT)
1 + 0 is non empty V17() V18() V19() V23() V24() V25() finite cardinal integer ext-real positive non negative Element of NAT
((REAL *),((REAL *),(n),(n))) . 0 is Relation-like Function-like Element of Funcs ((REAL *),(REAL *))
((((REAL *),((REAL *),(n),(n))) . 0),G) is Relation-like NAT -defined REAL -valued Function-like finite FinSequence-like FinSubsequence-like V88() V89() V90() Element of REAL *
(((((REAL *),((REAL *),(n),(n))) . 0),G),n) is Element of K32(NAT)
dom ((((REAL *),((REAL *),(n),(n))) . 0),G) is finite Element of K32(NAT)
{ b₁ where b₁ is V17() V18() V19() V23() V24() V25() finite cardinal integer ext-real non negative Element of NAT : ( b₁ in dom ((((REAL *),((REAL *),(n),(n))) . 0),G) & 1 <= b₁ & b₁ <= n & ((((REAL *),((REAL *),(n),(n))) . 0),G) . b₁ = - 1 ) } is set
n is Relation-like NAT -defined NAT -valued Function-like finite FinSequence-like FinSubsequence-like V88() V89() V90() V91() FinSequence of NAT
i is Relation-like NAT -defined NAT -valued Function-like finite FinSequence-like FinSubsequence-like V88() V89() V90() V91() FinSequence of NAT
f is Relation-like NAT -defined REAL -valued Function-like finite FinSequence-like FinSubsequence-like V88() V89() V90() Element of REAL *
g is V17() V18() V19() V23() V24() V25() finite cardinal integer ext-real non negative Element of NAT
G is V17() V18() V19() V23() V24() V25() finite cardinal integer ext-real non negative Element of NAT
n . 1 is V17() V18() V19() V23() V24() V25() finite cardinal integer ext-real non negative Element of REAL
i . 1 is V17() V18() V19() V23() V24() V25() finite cardinal integer ext-real non negative Element of REAL
len n is V17() V18() V19() V23() V24() V25() finite cardinal integer ext-real non negative Element of NAT
n . (len n) is V17() V18() V19() V23() V24() V25() finite cardinal integer ext-real non negative Element of REAL
W is V17() V18() V19() V23() V24() V25() finite cardinal integer ext-real non negative Element of NAT
(len n) - W is V24() V25() integer ext-real Element of REAL
n . ((len n) - W) is V17() V18() V19() V23() V24() V25() finite cardinal integer ext-real non negative Element of REAL
((len n) - W) + 1 is V24() V25() integer ext-real Element of REAL
n /. (((len n) - W) + 1) is V17() V18() V19() V23() V24() V25() finite cardinal integer ext-real non negative Element of NAT
(n /. (((len n) - W) + 1)) + G is V17() V18() V19() V23() V24() V25() finite cardinal integer ext-real non negative Element of NAT
f . ((n /. (((len n) - W) + 1)) + G) is V24() V25() ext-real Element of REAL
len i is V17() V18() V19() V23() V24() V25() finite cardinal integer ext-real non negative Element of NAT
i . (len i) is V17() V18() V19() V23() V24() V25() finite cardinal integer ext-real non negative Element of REAL
W is V17() V18() V19() V23() V24() V25() finite cardinal integer ext-real non negative Element of NAT
(len i) - W is V24() V25() integer ext-real Element of REAL
i . ((len i) - W) is V17() V18() V19() V23() V24() V25() finite cardinal integer ext-real non negative Element of REAL
((len i) - W) + 1 is V24() V25() integer ext-real Element of REAL
i /. (((len i) - W) + 1) is V17() V18() V19() V23() V24() V25() finite cardinal integer ext-real non negative Element of NAT
(i /. (((len i) - W) + 1)) + G is V17() V18() V19() V23() V24() V25() finite cardinal integer ext-real non negative Element of NAT
f . ((i /. (((len i) - W) + 1)) + G) is V24() V25() ext-real Element of REAL
(len n) - 1 is V24() V25() integer ext-real Element of REAL
1 - 1 is V24() V25() integer ext-real Element of REAL
W is V17() V18() V19() V23() V24() V25() finite cardinal integer ext-real non negative Element of NAT
(len n) - W is V24() V25() integer ext-real Element of REAL
0 + 1 is non empty V17() V18() V19() V23() V24() V25() finite cardinal integer ext-real positive non negative Element of NAT
(len i) - W is V24() V25() integer ext-real Element of REAL
i . ((len i) - W) is V17() V18() V19() V23() V24() V25() finite cardinal integer ext-real non negative Element of REAL
v1 is V17() V18() V19() V23() V24() V25() finite cardinal integer ext-real non negative Element of NAT
(len i) - 1 is V24() V25() integer ext-real Element of REAL
1 - 1 is V24() V25() integer ext-real Element of REAL
W is V17() V18() V19() V23() V24() V25() finite cardinal integer ext-real non negative Element of NAT
(len i) - W is V24() V25() integer ext-real Element of REAL
0 + 1 is non empty V17() V18() V19() V23() V24() V25() finite cardinal integer ext-real positive non negative Element of NAT
(len n) - W is V24() V25() integer ext-real Element of REAL
n . ((len n) - W) is V17() V18() V19() V23() V24() V25() finite cardinal integer ext-real non negative Element of REAL
v1 is V17() V18() V19() V23() V24() V25() finite cardinal integer ext-real non negative Element of NAT
W is V17() V18() V19() V23() V24() V25() finite cardinal integer ext-real non negative set
n . W is V17() V18() V19() V23() V24() V25() finite cardinal integer ext-real non negative Element of REAL
i . W is V17() V18() V19() V23() V24() V25() finite cardinal integer ext-real non negative Element of REAL
(len n) - W is V24() V25() integer ext-real Element of REAL
W - W is V24() V25() integer ext-real set
v1 is V17() V18() V19() V23() V24() V25() finite cardinal integer ext-real non negative Element of NAT
(len i) - v1 is V24() V25() integer ext-real Element of REAL
0 + W is V17() V18() V19() V23() V24() V25() finite cardinal integer ext-real non negative Element of NAT
(len n) - 1 is V24() V25() integer ext-real Element of REAL
0 + 1 is non empty V17() V18() V19() V23() V24() V25() finite cardinal integer ext-real positive non negative Element of NAT
n . W is V17() V18() V19() V23() V24() V25() finite cardinal integer ext-real non negative Element of REAL
i . W is V17() V18() V19() V23() V24() V25() finite cardinal integer ext-real non negative Element of REAL
n is non empty MultiGraphStruct
the carrier' of n is set
n is non empty oriented MultiGraphStruct
the carrier' of n is set
i is Relation-like NAT -defined Function-like finite FinSequence-like FinSubsequence-like set
f is Relation-like NAT -defined the carrier' of n -valued Function-like finite FinSequence-like FinSubsequence-like oriented Chain of n
g is Relation-like NAT -defined the carrier' of n -valued Function-like finite FinSequence-like FinSubsequence-like oriented Chain of n
len f is V17() V18() V19() V23() V24() V25() finite cardinal integer ext-real non negative Element of NAT
(len f) + 1 is non empty V17() V18() V19() V23() V24() V25() finite cardinal integer ext-real positive non negative Element of NAT
len i is V17() V18() V19() V23() V24() V25() finite cardinal integer ext-real non negative Element of NAT
len g is V17() V18() V19() V23() V24() V25() finite cardinal integer ext-real non negative Element of NAT
(len g) + 1 is non empty V17() V18() V19() V23() V24() V25() finite cardinal integer ext-real positive non negative Element of NAT
G is V17() V18() V19() V23() V24() V25() finite cardinal integer ext-real non negative set
the Target of n is Relation-like the carrier' of n -defined the carrier of n -valued Function-like quasi_total Element of K32(K33( the carrier' of n, the carrier of n))
the carrier of n is set
K33( the carrier' of n, the carrier of n) is set
K32(K33( the carrier' of n, the carrier of n)) is set
f . G is set
the Target of n . (f . G) is set
G + 1 is non empty V17() V18() V19() V23() V24() V25() finite cardinal integer ext-real positive non negative Element of NAT
i . (G + 1) is set
g . G is set
the Target of n . (g . G) is set
the Source of n is Relation-like the carrier' of n -defined the carrier of n -valued Function-like quasi_total Element of K32(K33( the carrier' of n, the carrier of n))
the Source of n . (f . G) is set
i . G is set
the Source of n . (g . G) is set
n is non empty MultiGraphStruct
the carrier' of n is set
i is Relation-like NAT -defined Function-like finite FinSequence-like FinSubsequence-like set
f is Relation-like NAT -defined Function-like finite FinSequence-like FinSubsequence-like set
g is Relation-like NAT -defined the carrier' of n -valued Function-like finite FinSequence-like FinSubsequence-like oriented Chain of n
len g is V17() V18() V19() V23() V24() V25() finite cardinal integer ext-real non negative Element of NAT
G is V17() V18() V19() V23() V24() V25() finite cardinal integer ext-real non negative set
len i is V17() V18() V19() V23() V24() V25() finite cardinal integer ext-real non negative Element of NAT
(len g) + 1 is non empty V17() V18() V19() V23() V24() V25() finite cardinal integer ext-real positive non negative Element of NAT
i . G is set
the Target of n is Relation-like the carrier' of n -defined the carrier of n -valued Function-like quasi_total Element of K32(K33( the carrier' of n, the carrier of n))
the carrier of n is set
K33( the carrier' of n, the carrier of n) is set
K32(K33( the carrier' of n, the carrier of n)) is set
g . (len g) is set
the Target of n . (g . (len g)) is set
f . G is set
G + 1 is non empty V17() V18() V19() V23() V24() V25() finite cardinal integer ext-real positive non negative Element of NAT
(len g) + 1 is non empty V17() V18() V19() V23() V24() V25() finite cardinal integer ext-real positive non negative Element of NAT
i . G is set
the Source of n is Relation-like the carrier' of n -defined the carrier of n -valued Function-like quasi_total Element of K32(K33( the carrier' of n, the carrier of n))
the carrier of n is set
K33( the carrier' of n, the carrier of n) is set
K32(K33( the carrier' of n, the carrier of n)) is set
g . G is set
the Source of n . (g . G) is set
f . G is set
(len g) + 1 is non empty V17() V18() V19() V23() V24() V25() finite cardinal integer ext-real positive non negative Element of NAT
len f is V17() V18() V19() V23() V24() V25() finite cardinal integer ext-real non negative Element of NAT
n is V17() V18() V19() V23() V24() V25() finite cardinal integer ext-real non negative Element of NAT
i is V17() V18() V19() V23() V24() V25() finite cardinal integer ext-real non negative Element of NAT
2 * i is V17() V18() V19() V23() V24() V25() finite cardinal integer ext-real non negative Element of NAT
(2 * i) + n is V17() V18() V19() V23() V24() V25() finite cardinal integer ext-real non negative Element of NAT
i * i is V17() V18() V19() V23() V24() V25() finite cardinal integer ext-real non negative Element of NAT
3 * i is V17() V18() V19() V23() V24() V25() finite cardinal integer ext-real non negative Element of NAT
(i * i) + (3 * i) is V17() V18() V19() V23() V24() V25() finite cardinal integer ext-real non negative Element of NAT
((i * i) + (3 * i)) + 1 is non empty V17() V18() V19() V23() V24() V25() finite cardinal integer ext-real positive non negative Element of NAT
(2 * i) + 1 is non empty V17() V18() V19() V23() V24() V25() finite cardinal integer ext-real positive non negative Element of NAT
2 * 1 is V17() V18() V19() V23() V24() V25() finite cardinal integer ext-real non negative Element of NAT
(2 * i) + i is V17() V18() V19() V23() V24() V25() finite cardinal integer ext-real non negative Element of NAT
2 + 1 is non empty V17() V18() V19() V23() V24() V25() finite cardinal integer ext-real positive non negative Element of NAT
(2 + 1) * i is V17() V18() V19() V23() V24() V25() finite cardinal integer ext-real non negative Element of NAT
n is V17() V18() V19() V23() V24() V25() finite cardinal integer ext-real non negative Element of NAT
i is V17() V18() V19() V23() V24() V25() finite cardinal integer ext-real non negative Element of NAT
i + n is V17() V18() V19() V23() V24() V25() finite cardinal integer ext-real non negative Element of NAT
2 * i is V17() V18() V19() V23() V24() V25() finite cardinal integer ext-real non negative Element of NAT
i * i is V17() V18() V19() V23() V24() V25() finite cardinal integer ext-real non negative Element of NAT
3 * i is V17() V18() V19() V23() V24() V25() finite cardinal integer ext-real non negative Element of NAT
(i * i) + (3 * i) is V17() V18() V19() V23() V24() V25() finite cardinal integer ext-real non negative Element of NAT
((i * i) + (3 * i)) + 1 is non empty V17() V18() V19() V23() V24() V25() finite cardinal integer ext-real positive non negative Element of NAT
1 + 1 is non empty V17() V18() V19() V23() V24() V25() finite cardinal integer ext-real positive non negative Element of NAT
i + i is V17() V18() V19() V23() V24() V25() finite cardinal integer ext-real non negative Element of NAT
n is V17() V18() V19() V23() V24() V25() finite cardinal integer ext-real non negative Element of NAT
i is V17() V18() V19() V23() V24() V25() finite cardinal integer ext-real non negative Element of NAT
2 * i is V17() V18() V19() V23() V24() V25() finite cardinal integer ext-real non negative Element of NAT
i * n is V17() V18() V19() V23() V24() V25() finite cardinal integer ext-real non negative Element of NAT
(2 * i) + (i * n) is V17() V18() V19() V23() V24() V25() finite cardinal integer ext-real non negative Element of NAT
i * i is V17() V18() V19() V23() V24() V25() finite cardinal integer ext-real non negative Element of NAT
3 * i is V17() V18() V19() V23() V24() V25() finite cardinal integer ext-real non negative Element of NAT
(i * i) + (3 * i) is V17() V18() V19() V23() V24() V25() finite cardinal integer ext-real non negative Element of NAT
((i * i) + (3 * i)) + 1 is non empty V17() V18() V19() V23() V24() V25() finite cardinal integer ext-real positive non negative Element of NAT
f is V17() V18() V19() V23() V24() V25() finite cardinal integer ext-real non negative Element of NAT
((2 * i) + (i * n)) + f is V17() V18() V19() V23() V24() V25() finite cardinal integer ext-real non negative Element of NAT
2 * 1 is V17() V18() V19() V23() V24() V25() finite cardinal integer ext-real non negative Element of NAT
(2 * i) + f is V17() V18() V19() V23() V24() V25() finite cardinal integer ext-real non negative Element of NAT
((2 * i) + f) + (i * n) is V17() V18() V19() V23() V24() V25() finite cardinal integer ext-real non negative Element of NAT
(i * n) + f is V17() V18() V19() V23() V24() V25() finite cardinal integer ext-real non negative Element of NAT
(2 * i) + ((i * n) + f) is V17() V18() V19() V23() V24() V25() finite cardinal integer ext-real non negative Element of NAT
1 * n is V17() V18() V19() V23() V24() V25() finite cardinal integer ext-real non negative Element of NAT
1 + n is non empty V17() V18() V19() V23() V24() V25() finite cardinal integer ext-real positive non negative Element of NAT
(2 * i) + i is V17() V18() V19() V23() V24() V25() finite cardinal integer ext-real non negative Element of NAT
2 + 1 is non empty V17() V18() V19() V23() V24() V25() finite cardinal integer ext-real positive non negative Element of NAT
(2 + 1) * i is V17() V18() V19() V23() V24() V25() finite cardinal integer ext-real non negative Element of NAT
n is V17() V18() V19() V23() V24() V25() finite cardinal integer ext-real non negative Element of NAT
i is V17() V18() V19() V23() V24() V25() finite cardinal integer ext-real non negative Element of NAT
3 * i is V17() V18() V19() V23() V24() V25() finite cardinal integer ext-real non negative Element of NAT
(3 * i) + 1 is non empty V17() V18() V19() V23() V24() V25() finite cardinal integer ext-real positive non negative Element of NAT
2 * i is V17() V18() V19() V23() V24() V25() finite cardinal integer ext-real non negative Element of NAT
i * n is V17() V18() V19() V23() V24() V25() finite cardinal integer ext-real non negative Element of NAT
(2 * i) + (i * n) is V17() V18() V19() V23() V24() V25() finite cardinal integer ext-real non negative Element of NAT
i * i is V17() V18() V19() V23() V24() V25() finite cardinal integer ext-real non negative Element of NAT
(i * i) + (3 * i) is V17() V18() V19() V23() V24() V25() finite cardinal integer ext-real non negative Element of NAT
f is V17() V18() V19() V23() V24() V25() finite cardinal integer ext-real non negative Element of NAT
((2 * i) + (i * n)) + f is V17() V18() V19() V23() V24() V25() finite cardinal integer ext-real non negative Element of NAT
(2 * i) + f is V17() V18() V19() V23() V24() V25() finite cardinal integer ext-real non negative Element of NAT
((2 * i) + f) + (i * n) is V17() V18() V19() V23() V24() V25() finite cardinal integer ext-real non negative Element of NAT
i * 1 is V17() V18() V19() V23() V24() V25() finite cardinal integer ext-real non negative Element of NAT
(2 * i) + i is V17() V18() V19() V23() V24() V25() finite cardinal integer ext-real non negative Element of NAT
2 + 1 is non empty V17() V18() V19() V23() V24() V25() finite cardinal integer ext-real positive non negative Element of NAT
(2 + 1) * i is V17() V18() V19() V23() V24() V25() finite cardinal integer ext-real non negative Element of NAT
i is non empty oriented MultiGraphStruct
the carrier' of i is set
K33( the carrier' of i,Real>=0) is set
K32(K33( the carrier' of i,Real>=0)) is set
n is V17() V18() V19() V23() V24() V25() finite cardinal integer ext-real non negative Element of NAT
(n) is Relation-like REAL * -defined REAL * -valued Function-like total quasi_total Element of Funcs ((REAL *),(REAL *))
(n) is Relation-like REAL * -defined REAL * -valued Function-like total quasi_total Element of Funcs ((REAL *),(REAL *))
((REAL *),(n),(n)) is Relation-like Function-like Element of Funcs ((REAL *),(REAL *))
(((REAL *),(n),(n)),n) is Relation-like REAL * -defined REAL * -valued Function-like total quasi_total Element of Funcs ((REAL *),(REAL *))
n is V17() V18() V19() V23() V24() V25() finite cardinal integer ext-real non negative Element of NAT
(n) is Relation-like REAL * -defined REAL * -valued Function-like total quasi_total Element of Funcs ((REAL *),(REAL *))
(n) is Relation-like REAL * -defined REAL * -valued Function-like total quasi_total Element of Funcs ((REAL *),(REAL *))
((REAL *),(n),(n)) is Relation-like Function-like Element of Funcs ((REAL *),(REAL *))
((REAL *),((REAL *),(n),(n))) is non empty Relation-like NAT -defined Funcs ((REAL *),(REAL *)) -valued Function-like total quasi_total Element of K32(K33(NAT,(Funcs ((REAL *),(REAL *)))))
((REAL *),((REAL *),(n),(n))) . 1 is Relation-like Function-like Element of Funcs ((REAL *),(REAL *))
2 * n is V17() V18() V19() V23() V24() V25() finite cardinal integer ext-real non negative Element of NAT
i is Relation-like NAT -defined REAL -valued Function-like finite FinSequence-like FinSubsequence-like V88() V89() V90() Element of REAL *
((((REAL *),((REAL *),(n),(n))) . 1),i) is Relation-like NAT -defined REAL -valued Function-like finite FinSequence-like FinSubsequence-like V88() V89() V90() Element of REAL *
f is Relation-like NAT -defined REAL -valued Function-like finite FinSequence-like FinSubsequence-like V88() V89() V90() Element of REAL *
(f,n) is Element of K32(NAT)
dom f is finite Element of K32(NAT)
{ b₁ where b₁ is V17() V18() V19() V23() V24() V25() finite cardinal integer ext-real non negative Element of NAT : ( b₁ in dom f & 1 <= b₁ & b₁ <= n & f . b₁ = - 1 ) } is set
g is non empty oriented finite MultiGraphStruct
the carrier' of g is finite set
K33( the carrier' of g,Real>=0) is set
K32(K33( the carrier' of g,Real>=0)) is set
the carrier of g is finite set
G is Relation-like the carrier' of g -defined Real>=0 -valued Function-like finite total quasi_total Element of K32(K33( the carrier' of g,Real>=0))
W is Element of the carrier of g
((REAL *),((REAL *),(n),(n))) . 0 is Relation-like Function-like Element of Funcs ((REAL *),(REAL *))
((((REAL *),((REAL *),(n),(n))) . 0),i) is Relation-like NAT -defined REAL -valued Function-like finite FinSequence-like FinSubsequence-like V88() V89() V90() Element of REAL *
n * n is V17() V18() V19() V23() V24() V25() finite cardinal integer ext-real non negative Element of NAT
3 * n is V17() V18() V19() V23() V24() V25() finite cardinal integer ext-real non negative Element of NAT
(n * n) + (3 * n) is V17() V18() V19() V23() V24() V25() finite cardinal integer ext-real non negative Element of NAT
((n * n) + (3 * n)) + 1 is non empty V17() V18() V19() V23() V24() V25() finite cardinal integer ext-real positive non negative Element of NAT
len i is V17() V18() V19() V23() V24() V25() finite cardinal integer ext-real non negative Element of NAT
n + 1 is non empty V17() V18() V19() V23() V24() V25() finite cardinal integer ext-real positive non negative Element of NAT
(2 * n) + n is V17() V18() V19() V23() V24() V25() finite cardinal integer ext-real non negative Element of NAT
2 + 1 is non empty V17() V18() V19() V23() V24() V25() finite cardinal integer ext-real positive non negative Element of NAT
(2 + 1) * n is V17() V18() V19() V23() V24() V25() finite cardinal integer ext-real non negative Element of NAT
i . (n + 1) is V24() V25() ext-real Element of REAL
dom i is finite Element of K32(NAT)
R is V17() V18() V19() V23() V24() V25() finite cardinal integer ext-real non negative Element of NAT
i . R is V24() V25() ext-real Element of REAL
M is V17() V18() V19() V23() V24() V25() finite cardinal integer ext-real non negative Element of NAT
n + M is V17() V18() V19() V23() V24() V25() finite cardinal integer ext-real non negative Element of NAT
i . (n + M) is V24() V25() ext-real Element of REAL
0 + 1 is non empty V17() V18() V19() V23() V24() V25() finite cardinal integer ext-real positive non negative Element of NAT
((REAL *),((REAL *),(n),(n))) . (0 + 1) is Relation-like Function-like Element of Funcs ((REAL *),(REAL *))
((((REAL *),((REAL *),(n),(n))) . (0 + 1)),i) is Relation-like NAT -defined REAL -valued Function-like finite FinSequence-like FinSubsequence-like V88() V89() V90() Element of REAL *
((n),((((REAL *),((REAL *),(n),(n))) . 0),i)) is Relation-like NAT -defined REAL -valued Function-like finite FinSequence-like FinSubsequence-like V88() V89() V90() Element of REAL *
((n),((n),((((REAL *),((REAL *),(n),(n))) . 0),i))) is Relation-like NAT -defined REAL -valued Function-like finite FinSequence-like FinSubsequence-like V88() V89() V90() Element of REAL *
(((n),((((REAL *),((REAL *),(n),(n))) . 0),i)),n) is Relation-like NAT -defined REAL -valued Function-like finite FinSequence-like FinSubsequence-like V88() V89() V90() Element of REAL *
Seg n is finite n -element Element of K32(NAT)
(i,n) is finite Element of K32(NAT)
{ b₁ where b₁ is V17() V18() V19() V23() V24() V25() finite cardinal integer ext-real non negative Element of NAT : ( b₁ in dom i & 1 <= b₁ & b₁ <= n & not i . b₁ = - 1 & not i . (n + b₁) = - 1 ) } is set
((i,n),i,n) is V17() V18() V19() V23() V24() V25() finite cardinal integer ext-real non negative Element of NAT
dom ((n),((((REAL *),((REAL *),(n),(n))) . 0),i)) is finite Element of K32(NAT)
dom ((((REAL *),((REAL *),(n),(n))) . 0),i) is finite Element of K32(NAT)
((n),i) is Relation-like NAT -defined REAL -valued Function-like finite FinSequence-like FinSubsequence-like V88() V89() V90() Element of REAL *
((((n * n) + (3 * n)) + 1),1,i,(- 1)) is Relation-like NAT -defined REAL -valued Function-like finite FinSequence-like FinSubsequence-like V88() V89() V90() FinSequence of REAL
(i,(((n * n) + (3 * n)) + 1),1) is Relation-like NAT -defined REAL -valued Function-like finite FinSequence-like FinSubsequence-like V88() V89() V90() FinSequence of REAL
((i,(((n * n) + (3 * n)) + 1),1),1,(- 1)) is Relation-like NAT -defined REAL -valued Function-like finite FinSequence-like FinSubsequence-like V88() V89() V90() FinSequence of REAL
((n),((((REAL *),((REAL *),(n),(n))) . 0),i)) . 1 is V24() V25() ext-real Element of REAL
(n + 1) -' n is V17() V18() V19() V23() V24() V25() finite cardinal integer ext-real non negative Element of NAT
(2 * n) + 1 is non empty V17() V18() V19() V23() V24() V25() finite cardinal integer ext-real positive non negative Element of NAT
mi is V17() V18() V19() V23() V24() V25() finite cardinal integer ext-real non negative Element of NAT
n + mi is V17() V18() V19() V23() V24() V25() finite cardinal integer ext-real non negative Element of NAT
cn is Element of the carrier of g
f . (n + mi) is V24() V25() ext-real Element of REAL
(2 * n) + mi is V17() V18() V19() V23() V24() V25() finite cardinal integer ext-real non negative Element of NAT
R is non empty Element of K32(NAT)
1 + 1 is non empty V17() V18() V19() V23() V24() V25() finite cardinal integer ext-real positive non negative Element of NAT
i . (n + mi) is V24() V25() ext-real Element of REAL
((n),((((REAL *),((REAL *),(n),(n))) . 0),i)) /. (((n * n) + (3 * n)) + 1) is V24() V25() ext-real Element of REAL
((n),((((REAL *),((REAL *),(n),(n))) . 0),i)) . (((n * n) + (3 * n)) + 1) is V24() V25() ext-real Element of REAL
(2 * n) + (((n),((((REAL *),((REAL *),(n),(n))) . 0),i)) /. (((n * n) + (3 * n)) + 1)) is V24() V25() ext-real Element of REAL
((n),((((REAL *),((REAL *),(n),(n))) . 0),i)) /. ((2 * n) + (((n),((((REAL *),((REAL *),(n),(n))) . 0),i)) /. (((n * n) + (3 * n)) + 1))) is V24() V25() ext-real Element of REAL
((n),((((REAL *),((REAL *),(n),(n))) . 0),i)) . ((2 * n) + 1) is V24() V25() ext-real Element of REAL
i . ((2 * n) + 1) is V24() V25() ext-real Element of REAL
((n),((((REAL *),((REAL *),(n),(n))) . 0),i)) . (n + mi) is V24() V25() ext-real Element of REAL
(n + mi) -' n is V17() V18() V19() V23() V24() V25() finite cardinal integer ext-real non negative Element of NAT
n * 1 is V17() V18() V19() V23() V24() V25() finite cardinal integer ext-real non negative Element of NAT
(2 * n) + (n * 1) is V17() V18() V19() V23() V24() V25() finite cardinal integer ext-real non negative Element of NAT
((2 * n) + (n * 1)) + mi is V17() V18() V19() V23() V24() V25() finite cardinal integer ext-real non negative Element of NAT
<*1,mi*> is non empty Relation-like NAT -defined NAT -valued Function-like finite 2 -element FinSequence-like FinSubsequence-like V88() V89() V90() V91() FinSequence of NAT
P is Relation-like NAT -defined NAT -valued Function-like finite FinSequence-like FinSubsequence-like V88() V89() V90() V91() FinSequence of NAT
P . 1 is V17() V18() V19() V23() V24() V25() finite cardinal integer ext-real non negative Element of REAL
n * (((n),((((REAL *),((REAL *),(n),(n))) . 0),i)) /. (((n * n) + (3 * n)) + 1)) is V24() V25() ext-real Element of REAL
(2 * n) + (n * (((n),((((REAL *),((REAL *),(n),(n))) . 0),i)) /. (((n * n) + (3 * n)) + 1))) is V24() V25() ext-real Element of REAL
((2 * n) + (n * (((n),((((REAL *),((REAL *),(n),(n))) . 0),i)) /. (((n * n) + (3 * n)) + 1)))) + mi is V24() V25() ext-real Element of REAL
((n),((((REAL *),((REAL *),(n),(n))) . 0),i)) /. (((2 * n) + (n * (((n),((((REAL *),((REAL *),(n),(n))) . 0),i)) /. (((n * n) + (3 * n)) + 1)))) + mi) is V24() V25() ext-real Element of REAL
((n),((((REAL *),((REAL *),(n),(n))) . 0),i)) . (((2 * n) + (n * 1)) + mi) is V24() V25() ext-real Element of REAL
i . (((2 * n) + (n * 1)) + mi) is V24() V25() ext-real Element of REAL
(g,W,cn,G) is V24() V25() ext-real Element of REAL
nk is set
<*nk*> is non empty V5() Relation-like NAT -defined Function-like constant finite 1 -element FinSequence-like FinSubsequence-like set
m is Relation-like NAT -defined the carrier' of g -valued Function-like finite FinSequence-like FinSubsequence-like oriented Chain of g
len m is V17() V18() V19() V23() V24() V25() finite cardinal integer ext-real non negative Element of NAT
len P is V17() V18() V19() V23() V24() V25() finite cardinal integer ext-real non negative Element of NAT
P . (len P) is V17() V18() V19() V23() V24() V25() finite cardinal integer ext-real non negative Element of REAL
j is V17() V18() V19() V23() V24() V25() finite cardinal integer ext-real non negative set
the Source of g is Relation-like the carrier' of g -defined the carrier of g -valued Function-like finite quasi_total Element of K32(K33( the carrier' of g, the carrier of g))
K33( the carrier' of g, the carrier of g) is finite set
K32(K33( the carrier' of g, the carrier of g)) is finite V30() set
m . j is set
the Source of g . (m . j) is set
the Source of g . nk is set
P . j is V17() V18() V19() V23() V24() V25() finite cardinal integer ext-real non negative Element of REAL
the Target of g is Relation-like the carrier' of g -defined the carrier of g -valued Function-like finite quasi_total Element of K32(K33( the carrier' of g, the carrier of g))
the Target of g . (m . j) is set
the Target of g . nk is set
j + 1 is non empty V17() V18() V19() V23() V24() V25() finite cardinal integer ext-real positive non negative Element of NAT
P . (j + 1) is V17() V18() V19() V23() V24() V25() finite cardinal integer ext-real non negative Element of REAL
j is V17() V18() V19() V23() V24() V25() finite cardinal integer ext-real non negative Element of NAT
(len P) - j is V24() V25() integer ext-real Element of REAL
P . ((len P) - j) is V17() V18() V19() V23() V24() V25() finite cardinal integer ext-real non negative Element of REAL
((len P) - j) + 1 is V24() V25() integer ext-real Element of REAL
P /. (((len P) - j) + 1) is V17() V18() V19() V23() V24() V25() finite cardinal integer ext-real non negative Element of NAT
n + (P /. (((len P) - j) + 1)) is V17() V18() V19() V23() V24() V25() finite cardinal integer ext-real non negative Element of NAT
f . (n + (P /. (((len P) - j) + 1))) is V24() V25() ext-real Element of REAL
((2 * n) + mi) -' (2 * n) is V17() V18() V19() V23() V24() V25() finite cardinal integer ext-real non negative Element of NAT
(((n),((((REAL *),((REAL *),(n),(n))) . 0),i)),n) . ((2 * n) + mi) is V24() V25() ext-real Element of REAL
(((n),((((REAL *),((REAL *),(n),(n))) . 0),i)),n,(((2 * n) + mi) -' (2 * n))) is V24() V25() ext-real Element of REAL
((2 * n) + (n * (((n),((((REAL *),((REAL *),(n),(n))) . 0),i)) /. (((n * n) + (3 * n)) + 1)))) + (((2 * n) + mi) -' (2 * n)) is V24() V25() ext-real Element of REAL
((n),((((REAL *),((REAL *),(n),(n))) . 0),i)) /. (((2 * n) + (n * (((n),((((REAL *),((REAL *),(n),(n))) . 0),i)) /. (((n * n) + (3 * n)) + 1)))) + (((2 * n) + mi) -' (2 * n))) is V24() V25() ext-real Element of REAL
(((n),((((REAL *),((REAL *),(n),(n))) . 0),i)) /. ((2 * n) + (((n),((((REAL *),((REAL *),(n),(n))) . 0),i)) /. (((n * n) + (3 * n)) + 1)))) + (((n),((((REAL *),((REAL *),(n),(n))) . 0),i)) /. (((2 * n) + (n * (((n),((((REAL *),((REAL *),(n),(n))) . 0),i)) /. (((n * n) + (3 * n)) + 1)))) + (((2 * n) + mi) -' (2 * n)))) is V24() V25() ext-real Element of REAL
0 + (((n),((((REAL *),((REAL *),(n),(n))) . 0),i)) /. (((2 * n) + (n * (((n),((((REAL *),((REAL *),(n),(n))) . 0),i)) /. (((n * n) + (3 * n)) + 1)))) + mi)) is V24() V25() ext-real Element of REAL
j is Relation-like NAT -defined NAT -valued Function-like finite FinSequence-like FinSubsequence-like V88() V89() V90() V91() FinSequence of NAT
v3 is V17() V18() V19() V23() V24() V25() finite cardinal integer ext-real non negative Element of NAT
len j is V17() V18() V19() V23() V24() V25() finite cardinal integer ext-real non negative Element of NAT
v3 + 1 is non empty V17() V18() V19() V23() V24() V25() finite cardinal integer ext-real positive non negative Element of NAT
j . v3 is V17() V18() V19() V23() V24() V25() finite cardinal integer ext-real non negative Element of REAL
nj is Relation-like NAT -defined the carrier' of g -valued Function-like finite FinSequence-like FinSubsequence-like oriented Chain of g
len nj is V17() V18() V19() V23() V24() V25() finite cardinal integer ext-real non negative Element of NAT
(len nj) + 1 is non empty V17() V18() V19() V23() V24() V25() finite cardinal integer ext-real positive non negative Element of NAT
cost (nj,G) is V24() V25() ext-real Element of REAL
nj . 1 is set
G . (nj . 1) is set
G . nk is set
f . ((2 * n) + mi) is V24() V25() ext-real Element of REAL
v3 is Element of the carrier of g
2 * 1 is V17() V18() V19() V23() V24() V25() finite cardinal integer ext-real non negative Element of NAT
f . (n + 1) is V24() V25() ext-real Element of REAL
((n),((((REAL *),((REAL *),(n),(n))) . 0),i)) . (n + 1) is V24() V25() ext-real Element of REAL
((((REAL *),((REAL *),(n),(n))) . 0),i) . (n + 1) is V24() V25() ext-real Element of REAL
cn is V17() V18() V19() V23() V24() V25() finite cardinal integer ext-real non negative Element of NAT
n + cn is V17() V18() V19() V23() V24() V25() finite cardinal integer ext-real non negative Element of NAT
f . (n + cn) is V24() V25() ext-real Element of REAL
RM is V17() V18() V19() V23() V24() V25() finite cardinal integer ext-real non negative Element of NAT
(2 * n) + cn is V17() V18() V19() V23() V24() V25() finite cardinal integer ext-real non negative Element of NAT
((n),((((REAL *),((REAL *),(n),(n))) . 0),i)) . cn is V24() V25() ext-real Element of REAL
i . cn is V24() V25() ext-real Element of REAL
n + n is V17() V18() V19() V23() V24() V25() finite cardinal integer ext-real non negative Element of NAT
(n + cn) -' n is V17() V18() V19() V23() V24() V25() finite cardinal integer ext-real non negative Element of NAT
((n),((((REAL *),((REAL *),(n),(n))) . 0),i)) . (n + cn) is V24() V25() ext-real Element of REAL
((2 * n) + (n * (((n),((((REAL *),((REAL *),(n),(n))) . 0),i)) /. (((n * n) + (3 * n)) + 1)))) + cn is V24() V25() ext-real Element of REAL
((n),((((REAL *),((REAL *),(n),(n))) . 0),i)) /. (((2 * n) + (n * (((n),((((REAL *),((REAL *),(n),(n))) . 0),i)) /. (((n * n) + (3 * n)) + 1)))) + cn) is V24() V25() ext-real Element of REAL
((2 * n) + (n * 1)) + cn is V17() V18() V19() V23() V24() V25() finite cardinal integer ext-real non negative Element of NAT
(n * 1) + cn is V17() V18() V19() V23() V24() V25() finite cardinal integer ext-real non negative Element of NAT
(2 * n) + ((n * 1) + cn) is V17() V18() V19() V23() V24() V25() finite cardinal integer ext-real non negative Element of NAT
(3 * n) + (n * n) is V17() V18() V19() V23() V24() V25() finite cardinal integer ext-real non negative Element of NAT
((n),((((REAL *),((REAL *),(n),(n))) . 0),i)) . (((2 * n) + (n * 1)) + cn) is V24() V25() ext-real Element of REAL
i . (((2 * n) + (n * 1)) + cn) is V24() V25() ext-real Element of REAL
mi is Element of the carrier of g
(g,W,mi,G) is V24() V25() ext-real Element of REAL
P is set
n * RM is V17() V18() V19() V23() V24() V25() finite cardinal integer ext-real non negative Element of NAT
(2 * n) + (n * RM) is V17() V18() V19() V23() V24() V25() finite cardinal integer ext-real non negative Element of NAT
((2 * n) + (n * RM)) + cn is V17() V18() V19() V23() V24() V25() finite cardinal integer ext-real non negative Element of NAT
i . (((2 * n) + (n * RM)) + cn) is V24() V25() ext-real Element of REAL
RM is V17() V18() V19() V23() V24() V25() finite cardinal integer ext-real non negative Element of NAT
n + RM is V17() V18() V19() V23() V24() V25() finite cardinal integer ext-real non negative Element of NAT
f . (n + RM) is V24() V25() ext-real Element of REAL
n is V17() V18() V19() V23() V24() V25() finite cardinal integer ext-real non negative Element of NAT
(n) is Relation-like REAL * -defined REAL * -valued Function-like total quasi_total Element of Funcs ((REAL *),(REAL *))
(n) is Relation-like REAL * -defined REAL * -valued Function-like total quasi_total Element of Funcs ((REAL *),(REAL *))
((REAL *),(n),(n)) is Relation-like Function-like Element of Funcs ((REAL *),(REAL *))
((REAL *),((REAL *),(n),(n))) is non empty Relation-like NAT -defined Funcs ((REAL *),(REAL *)) -valued Function-like total quasi_total Element of K32(K33(NAT,(Funcs ((REAL *),(REAL *)))))
n * n is V17() V18() V19() V23() V24() V25() finite cardinal integer ext-real non negative Element of NAT
3 * n is V17() V18() V19() V23() V24() V25() finite cardinal integer ext-real non negative Element of NAT
(n * n) + (3 * n) is V17() V18() V19() V23() V24() V25() finite cardinal integer ext-real non negative Element of NAT
((n * n) + (3 * n)) + 1 is non empty V17() V18() V19() V23() V24() V25() finite cardinal integer ext-real positive non negative Element of NAT
i is V17() V18() V19() V23() V24() V25() finite cardinal integer ext-real non negative Element of NAT
((REAL *),((REAL *),(n),(n))) . i is Relation-like Function-like Element of Funcs ((REAL *),(REAL *))
i + 1 is non empty V17() V18() V19() V23() V24() V25() finite cardinal integer ext-real positive non negative Element of NAT
((REAL *),((REAL *),(n),(n))) . (i + 1) is Relation-like Function-like Element of Funcs ((REAL *),(REAL *))
f is V17() V18() V19() V23() V24() V25() finite cardinal integer ext-real non negative Element of NAT
n + f is V17() V18() V19() V23() V24() V25() finite cardinal integer ext-real non negative Element of NAT
g is Relation-like NAT -defined REAL -valued Function-like finite FinSequence-like FinSubsequence-like V88() V89() V90() Element of REAL *
(g,n) is finite Element of K32(NAT)
dom g is finite Element of K32(NAT)
{ b₁ where b₁ is V17() V18() V19() V23() V24() V25() finite cardinal integer ext-real non negative Element of NAT : ( b₁ in dom g & 1 <= b₁ & b₁ <= n & not g . b₁ = - 1 & not g . (n + b₁) = - 1 ) } is set
(g,n) is Element of K32(NAT)
{ b₁ where b₁ is V17() V18() V19() V23() V24() V25() finite cardinal integer ext-real non negative Element of NAT : ( b₁ in dom g & 1 <= b₁ & b₁ <= n & g . b₁ = - 1 ) } is set
g . (n + f) is V24() V25() ext-real Element of REAL
G is Relation-like NAT -defined REAL -valued Function-like finite FinSequence-like FinSubsequence-like V88() V89() V90() Element of REAL *
((((REAL *),((REAL *),(n),(n))) . i),G) is Relation-like NAT -defined REAL -valued Function-like finite FinSequence-like FinSubsequence-like V88() V89() V90() Element of REAL *
((((REAL *),((REAL *),(n),(n))) . (i + 1)),G) is Relation-like NAT -defined REAL -valued Function-like finite FinSequence-like FinSubsequence-like V88() V89() V90() Element of REAL *
len G is V17() V18() V19() V23() V24() V25() finite cardinal integer ext-real non negative Element of NAT
W is Relation-like NAT -defined REAL -valued Function-like finite FinSequence-like FinSubsequence-like V88() V89() V90() Element of REAL *
W . (n + f) is V24() V25() ext-real Element of REAL
((g,n),g,n) is V17() V18() V19() V23() V24() V25() finite cardinal integer ext-real non negative Element of NAT
((n),g) is Relation-like NAT -defined REAL -valued Function-like finite FinSequence-like FinSubsequence-like V88() V89() V90() Element of REAL *
((n),((n),g)) is Relation-like NAT -defined REAL -valued Function-like finite FinSequence-like FinSubsequence-like V88() V89() V90() Element of REAL *
(((n),g),n) is Relation-like NAT -defined REAL -valued Function-like finite FinSequence-like FinSubsequence-like V88() V89() V90() Element of REAL *
n + n is V17() V18() V19() V23() V24() V25() finite cardinal integer ext-real non negative Element of NAT
M is V17() V18() V19() V23() V24() V25() finite cardinal integer ext-real non negative Element of NAT
g . M is V24() V25() ext-real Element of REAL
M is V17() V18() V19() V23() V24() V25() finite cardinal integer ext-real non negative Element of NAT
g . M is V24() V25() ext-real Element of REAL
2 * n is V17() V18() V19() V23() V24() V25() finite cardinal integer ext-real non negative Element of NAT
dom G is finite Element of K32(NAT)
(n + f) -' n is V17() V18() V19() V23() V24() V25() finite cardinal integer ext-real non negative Element of NAT
dom ((n),g) is finite Element of K32(NAT)
((((n * n) + (3 * n)) + 1),((g,n),g,n),g,(- 1)) is Relation-like NAT -defined REAL -valued Function-like finite FinSequence-like FinSubsequence-like V88() V89() V90() FinSequence of REAL
(g,(((n * n) + (3 * n)) + 1),((g,n),g,n)) is Relation-like NAT -defined REAL -valued Function-like finite FinSequence-like FinSubsequence-like V88() V89() V90() FinSequence of REAL
((g,(((n * n) + (3 * n)) + 1),((g,n),g,n)),((g,n),g,n),(- 1)) is Relation-like NAT -defined REAL -valued Function-like finite FinSequence-like FinSubsequence-like V88() V89() V90() FinSequence of REAL
g . ((g,n),g,n) is V24() V25() ext-real Element of REAL
((n),g) . f is V24() V25() ext-real Element of REAL
M is V17() V18() V19() V23() V24() V25() finite cardinal integer ext-real non negative Element of NAT
g . M is V24() V25() ext-real Element of REAL
n + 1 is non empty V17() V18() V19() V23() V24() V25() finite cardinal integer ext-real positive non negative Element of NAT
M is V17() V18() V19() V23() V24() V25() finite cardinal integer ext-real non negative Element of NAT
g . M is V24() V25() ext-real Element of REAL
((n),g) . (n + f) is V24() V25() ext-real Element of REAL
n is V17() V18() V19() V23() V24() V25() finite cardinal integer ext-real non negative Element of NAT
(n) is Relation-like REAL * -defined REAL * -valued Function-like total quasi_total Element of Funcs ((REAL *),(REAL *))
(n) is Relation-like REAL * -defined REAL * -valued Function-like total quasi_total Element of Funcs ((REAL *),(REAL *))
((REAL *),(n),(n)) is Relation-like Function-like Element of Funcs ((REAL *),(REAL *))
((REAL *),((REAL *),(n),(n))) is non empty Relation-like NAT -defined Funcs ((REAL *),(REAL *)) -valued Function-like total quasi_total Element of K32(K33(NAT,(Funcs ((REAL *),(REAL *)))))
n * n is V17() V18() V19() V23() V24() V25() finite cardinal integer ext-real non negative Element of NAT
3 * n is V17() V18() V19() V23() V24() V25() finite cardinal integer ext-real non negative Element of NAT
(n * n) + (3 * n) is V17() V18() V19() V23() V24() V25() finite cardinal integer ext-real non negative Element of NAT
((n * n) + (3 * n)) + 1 is non empty V17() V18() V19() V23() V24() V25() finite cardinal integer ext-real positive non negative Element of NAT
i is V17() V18() V19() V23() V24() V25() finite cardinal integer ext-real non negative Element of NAT
((REAL *),((REAL *),(n),(n))) . i is Relation-like Function-like Element of Funcs ((REAL *),(REAL *))
i + 1 is non empty V17() V18() V19() V23() V24() V25() finite cardinal integer ext-real positive non negative Element of NAT
((REAL *),((REAL *),(n),(n))) . (i + 1) is Relation-like Function-like Element of Funcs ((REAL *),(REAL *))
f is V17() V18() V19() V23() V24() V25() finite cardinal integer ext-real non negative Element of NAT
n + f is V17() V18() V19() V23() V24() V25() finite cardinal integer ext-real non negative Element of NAT
g is Relation-like NAT -defined REAL -valued Function-like finite FinSequence-like FinSubsequence-like V88() V89() V90() Element of REAL *
(g,n) is finite Element of K32(NAT)
dom g is finite Element of K32(NAT)
{ b₁ where b₁ is V17() V18() V19() V23() V24() V25() finite cardinal integer ext-real non negative Element of NAT : ( b₁ in dom g & 1 <= b₁ & b₁ <= n & not g . b₁ = - 1 & not g . (n + b₁) = - 1 ) } is set
g . (n + f) is V24() V25() ext-real Element of REAL
(g,n) is Element of K32(NAT)
{ b₁ where b₁ is V17() V18() V19() V23() V24() V25() finite cardinal integer ext-real non negative Element of NAT : ( b₁ in dom g & 1 <= b₁ & b₁ <= n & g . b₁ = - 1 ) } is set
G is Relation-like NAT -defined REAL -valued Function-like finite FinSequence-like FinSubsequence-like V88() V89() V90() Element of REAL *
((((REAL *),((REAL *),(n),(n))) . i),G) is Relation-like NAT -defined REAL -valued Function-like finite FinSequence-like FinSubsequence-like V88() V89() V90() Element of REAL *
((((REAL *),((REAL *),(n),(n))) . (i + 1)),G) is Relation-like NAT -defined REAL -valued Function-like finite FinSequence-like FinSubsequence-like V88() V89() V90() Element of REAL *
len G is V17() V18() V19() V23() V24() V25() finite cardinal integer ext-real non negative Element of NAT
W is Relation-like NAT -defined REAL -valued Function-like finite FinSequence-like FinSubsequence-like V88() V89() V90() Element of REAL *
W . (n + f) is V24() V25() ext-real Element of REAL
v1 is Relation-like NAT -defined NAT -valued Function-like finite FinSequence-like FinSubsequence-like V88() V89() V90() V91() FinSequence of NAT
len v1 is V17() V18() V19() V23() V24() V25() finite cardinal integer ext-real non negative Element of NAT
v1 . (len v1) is V17() V18() V19() V23() V24() V25() finite cardinal integer ext-real non negative Element of REAL
VG is V17() V18() V19() V23() V24() V25() finite cardinal integer ext-real non negative Element of NAT
(len v1) - VG is V24() V25() integer ext-real Element of REAL
VG - VG is V24() V25() integer ext-real Element of REAL
Ug is V17() V18() V19() V23() V24() V25() finite cardinal integer ext-real non negative Element of NAT
(len v1) - 1 is V24() V25() integer ext-real Element of REAL
Ug + 1 is non empty V17() V18() V19() V23() V24() V25() finite cardinal integer ext-real positive non negative Element of NAT
((len v1) - 1) + 1 is V24() V25() integer ext-real Element of REAL
1 + 0 is non empty V17() V18() V19() V23() V24() V25() finite cardinal integer ext-real positive non negative Element of NAT
v1 /. (Ug + 1) is V17() V18() V19() V23() V24() V25() finite cardinal integer ext-real non negative Element of NAT
v1 . (Ug + 1) is V17() V18() V19() V23() V24() V25() finite cardinal integer ext-real non negative Element of REAL
v1 . ((len v1) - VG) is V17() V18() V19() V23() V24() V25() finite cardinal integer ext-real non negative Element of REAL
((len v1) - VG) + 1 is V24() V25() integer ext-real Element of REAL
v1 /. (((len v1) - VG) + 1) is V17() V18() V19() V23() V24() V25() finite cardinal integer ext-real non negative Element of NAT
n + (v1 /. (((len v1) - VG) + 1)) is V17() V18() V19() V23() V24() V25() finite cardinal integer ext-real non negative Element of NAT
W . (n + (v1 /. (((len v1) - VG) + 1))) is V24() V25() ext-real Element of REAL
v1 . ((len v1) - VG) is V17() V18() V19() V23() V24() V25() finite cardinal integer ext-real non negative Element of REAL
((len v1) - VG) + 1 is V24() V25() integer ext-real Element of REAL
v1 /. (((len v1) - VG) + 1) is V17() V18() V19() V23() V24() V25() finite cardinal integer ext-real non negative Element of NAT
n + (v1 /. (((len v1) - VG) + 1)) is V17() V18() V19() V23() V24() V25() finite cardinal integer ext-real non negative Element of NAT
g . (n + (v1 /. (((len v1) - VG) + 1))) is V24() V25() ext-real Element of REAL
W . (n + (v1 /. (((len v1) - VG) + 1))) is V24() V25() ext-real Element of REAL
v1 . 1 is V17() V18() V19() V23() V24() V25() finite cardinal integer ext-real non negative Element of REAL
n is V17() V18() V19() V23() V24() V25() finite cardinal integer ext-real non negative Element of NAT
(n) is Relation-like REAL * -defined REAL * -valued Function-like total quasi_total Element of Funcs ((REAL *),(REAL *))
(n) is Relation-like REAL * -defined REAL * -valued Function-like total quasi_total Element of Funcs ((REAL *),(REAL *))
((REAL *),(n),(n)) is Relation-like Function-like Element of Funcs ((REAL *),(REAL *))
((REAL *),((REAL *),(n),(n))) is non empty Relation-like NAT -defined Funcs ((REAL *),(REAL *)) -valued Function-like total quasi_total Element of K32(K33(NAT,(Funcs ((REAL *),(REAL *)))))
n * n is V17() V18() V19() V23() V24() V25() finite cardinal integer ext-real non negative Element of NAT
3 * n is V17() V18() V19() V23() V24() V25() finite cardinal integer ext-real non negative Element of NAT
(n * n) + (3 * n) is V17() V18() V19() V23() V24() V25() finite cardinal integer ext-real non negative Element of NAT
((n * n) + (3 * n)) + 1 is non empty V17() V18() V19() V23() V24() V25() finite cardinal integer ext-real positive non negative Element of NAT
i is V17() V18() V19() V23() V24() V25() finite cardinal integer ext-real non negative Element of NAT
((REAL *),((REAL *),(n),(n))) . i is Relation-like Function-like Element of Funcs ((REAL *),(REAL *))
i + 1 is non empty V17() V18() V19() V23() V24() V25() finite cardinal integer ext-real positive non negative Element of NAT
((REAL *),((REAL *),(n),(n))) . (i + 1) is Relation-like Function-like Element of Funcs ((REAL *),(REAL *))
f is V17() V18() V19() V23() V24() V25() finite cardinal integer ext-real non negative Element of NAT
n + f is V17() V18() V19() V23() V24() V25() finite cardinal integer ext-real non negative Element of NAT
g is V17() V18() V19() V23() V24() V25() finite cardinal integer ext-real non negative Element of NAT
n + g is V17() V18() V19() V23() V24() V25() finite cardinal integer ext-real non negative Element of NAT
<*g*> is non empty V5() Relation-like NAT -defined NAT -valued Function-like one-to-one constant finite 1 -element FinSequence-like FinSubsequence-like V88() V89() V90() V91() V92() V93() V94() V95() FinSequence of NAT
G is Relation-like NAT -defined REAL -valued Function-like finite FinSequence-like FinSubsequence-like V88() V89() V90() Element of REAL *
(G,n) is finite Element of K32(NAT)
dom G is finite Element of K32(NAT)
{ b₁ where b₁ is V17() V18() V19() V23() V24() V25() finite cardinal integer ext-real non negative Element of NAT : ( b₁ in dom G & 1 <= b₁ & b₁ <= n & not G . b₁ = - 1 & not G . (n + b₁) = - 1 ) } is set
G . (n + f) is V24() V25() ext-real Element of REAL
(G,n) is Element of K32(NAT)
{ b₁ where b₁ is V17() V18() V19() V23() V24() V25() finite cardinal integer ext-real non negative Element of NAT : ( b₁ in dom G & 1 <= b₁ & b₁ <= n & G . b₁ = - 1 ) } is set
W is Relation-like NAT -defined REAL -valued Function-like finite FinSequence-like FinSubsequence-like V88() V89() V90() Element of REAL *
((((REAL *),((REAL *),(n),(n))) . i),W) is Relation-like NAT -defined REAL -valued Function-like finite FinSequence-like FinSubsequence-like V88() V89() V90() Element of REAL *
((((REAL *),((REAL *),(n),(n))) . (i + 1)),W) is Relation-like NAT -defined REAL -valued Function-like finite FinSequence-like FinSubsequence-like V88() V89() V90() Element of REAL *
len W is V17() V18() V19() V23() V24() V25() finite cardinal integer ext-real non negative Element of NAT
v1 is Relation-like NAT -defined REAL -valued Function-like finite FinSequence-like FinSubsequence-like V88() V89() V90() Element of REAL *
v1 . (n + g) is V24() V25() ext-real Element of REAL
v1 . (n + f) is V24() V25() ext-real Element of REAL
v2 is Relation-like NAT -defined NAT -valued Function-like finite FinSequence-like FinSubsequence-like V88() V89() V90() V91() FinSequence of NAT
len v2 is V17() V18() V19() V23() V24() V25() finite cardinal integer ext-real non negative Element of NAT
v2 ^ <*g*> is non empty Relation-like NAT -defined NAT -valued Function-like finite FinSequence-like FinSubsequence-like V88() V89() V90() V91() FinSequence of NAT
v2 . (len v2) is V17() V18() V19() V23() V24() V25() finite cardinal integer ext-real non negative Element of REAL
len (v2 ^ <*g*>) is non empty V17() V18() V19() V23() V24() V25() finite cardinal integer ext-real positive non negative Element of NAT
(len v2) + 1 is non empty V17() V18() V19() V23() V24() V25() finite cardinal integer ext-real positive non negative Element of NAT
(v2 ^ <*g*>) . (len (v2 ^ <*g*>)) is V17() V18() V19() V23() V24() V25() finite cardinal integer ext-real non negative Element of REAL
Vg is V17() V18() V19() V23() V24() V25() finite cardinal integer ext-real non negative Element of NAT
(len (v2 ^ <*g*>)) - Vg is V24() V25() integer ext-real Element of REAL
Vg - Vg is V24() V25() integer ext-real Element of REAL
R is V17() V18() V19() V23() V24() V25() finite cardinal integer ext-real non negative Element of NAT
R + 1 is non empty V17() V18() V19() V23() V24() V25() finite cardinal integer ext-real positive non negative Element of NAT
1 + 0 is non empty V17() V18() V19() V23() V24() V25() finite cardinal integer ext-real positive non negative Element of NAT
(len (v2 ^ <*g*>)) - 1 is V24() V25() integer ext-real Element of REAL
((len (v2 ^ <*g*>)) - 1) + 1 is V24() V25() integer ext-real Element of REAL
(v2 ^ <*g*>) /. (R + 1) is V17() V18() V19() V23() V24() V25() finite cardinal integer ext-real non negative Element of NAT
(v2 ^ <*g*>) . (R + 1) is V17() V18() V19() V23() V24() V25() finite cardinal integer ext-real non negative Element of REAL
(v2 ^ <*g*>) . ((len (v2 ^ <*g*>)) - Vg) is V17() V18() V19() V23() V24() V25() finite cardinal integer ext-real non negative Element of REAL
((len (v2 ^ <*g*>)) - Vg) + 1 is V24() V25() integer ext-real Element of REAL
(v2 ^ <*g*>) /. (((len (v2 ^ <*g*>)) - Vg) + 1) is V17() V18() V19() V23() V24() V25() finite cardinal integer ext-real non negative Element of NAT
n + ((v2 ^ <*g*>) /. (((len (v2 ^ <*g*>)) - Vg) + 1)) is V17() V18() V19() V23() V24() V25() finite cardinal integer ext-real non negative Element of NAT
v1 . (n + ((v2 ^ <*g*>) /. (((len (v2 ^ <*g*>)) - Vg) + 1))) is V24() V25() ext-real Element of REAL
(v2 ^ <*g*>) . ((len (v2 ^ <*g*>)) - Vg) is V17() V18() V19() V23() V24() V25() finite cardinal integer ext-real non negative Element of REAL
v2 . R is V17() V18() V19() V23() V24() V25() finite cardinal integer ext-real non negative Element of REAL
(len v2) - 1 is V24() V25() integer ext-real Element of REAL
((len v2) - 1) + 1 is V24() V25() integer ext-real Element of REAL
v2 /. (((len v2) - 1) + 1) is V17() V18() V19() V23() V24() V25() finite cardinal integer ext-real non negative Element of NAT
((len (v2 ^ <*g*>)) - Vg) + 1 is V24() V25() integer ext-real Element of REAL
(v2 ^ <*g*>) /. (((len (v2 ^ <*g*>)) - Vg) + 1) is V17() V18() V19() V23() V24() V25() finite cardinal integer ext-real non negative Element of NAT
n + ((v2 ^ <*g*>) /. (((len (v2 ^ <*g*>)) - Vg) + 1)) is V17() V18() V19() V23() V24() V25() finite cardinal integer ext-real non negative Element of NAT
v1 . (n + ((v2 ^ <*g*>) /. (((len (v2 ^ <*g*>)) - Vg) + 1))) is V24() V25() ext-real Element of REAL
Vg - 1 is V24() V25() integer ext-real Element of REAL
(len v2) - 1 is V24() V25() integer ext-real Element of REAL
(len v2) - (Vg - 1) is V24() V25() integer ext-real Element of REAL
v2 /. (R + 1) is V17() V18() V19() V23() V24() V25() finite cardinal integer ext-real non negative Element of NAT
v2 . (R + 1) is V17() V18() V19() V23() V24() V25() finite cardinal integer ext-real non negative Element of REAL
((len (v2 ^ <*g*>)) - Vg) + 1 is V24() V25() integer ext-real Element of REAL
(v2 ^ <*g*>) /. (((len (v2 ^ <*g*>)) - Vg) + 1) is V17() V18() V19() V23() V24() V25() finite cardinal integer ext-real non negative Element of NAT
RM is V17() V18() V19() V23() V24() V25() finite cardinal integer ext-real non negative Element of NAT
(len v2) - RM is V24() V25() integer ext-real Element of REAL
((len v2) - RM) + 1 is V24() V25() integer ext-real Element of REAL
v2 /. (((len v2) - RM) + 1) is V17() V18() V19() V23() V24() V25() finite cardinal integer ext-real non negative Element of NAT
n + (v2 /. (((len v2) - RM) + 1)) is V17() V18() V19() V23() V24() V25() finite cardinal integer ext-real non negative Element of NAT
G . (n + (v2 /. (((len v2) - RM) + 1))) is V24() V25() ext-real Element of REAL
n + ((v2 ^ <*g*>) /. (((len (v2 ^ <*g*>)) - Vg) + 1)) is V17() V18() V19() V23() V24() V25() finite cardinal integer ext-real non negative Element of NAT
v1 . (n + ((v2 ^ <*g*>) /. (((len (v2 ^ <*g*>)) - Vg) + 1))) is V24() V25() ext-real Element of REAL
((len (v2 ^ <*g*>)) - Vg) + 1 is V24() V25() integer ext-real Element of REAL
(v2 ^ <*g*>) /. (((len (v2 ^ <*g*>)) - Vg) + 1) is V17() V18() V19() V23() V24() V25() finite cardinal integer ext-real non negative Element of NAT
n + ((v2 ^ <*g*>) /. (((len (v2 ^ <*g*>)) - Vg) + 1)) is V17() V18() V19() V23() V24() V25() finite cardinal integer ext-real non negative Element of NAT
v1 . (n + ((v2 ^ <*g*>) /. (((len (v2 ^ <*g*>)) - Vg) + 1))) is V24() V25() ext-real Element of REAL
((len (v2 ^ <*g*>)) - Vg) + 1 is V24() V25() integer ext-real Element of REAL
(v2 ^ <*g*>) /. (((len (v2 ^ <*g*>)) - Vg) + 1) is V17() V18() V19() V23() V24() V25() finite cardinal integer ext-real non negative Element of NAT
n + ((v2 ^ <*g*>) /. (((len (v2 ^ <*g*>)) - Vg) + 1)) is V17() V18() V19() V23() V24() V25() finite cardinal integer ext-real non negative Element of NAT
v1 . (n + ((v2 ^ <*g*>) /. (((len (v2 ^ <*g*>)) - Vg) + 1))) is V24() V25() ext-real Element of REAL
rng v2 is finite V99() V100() V101() V104() Element of K32(REAL)
dom v2 is finite Element of K32(NAT)
Vg is V17() V18() V19() V23() V24() V25() finite cardinal integer ext-real non negative set
v2 . Vg is V17() V18() V19() V23() V24() V25() finite cardinal integer ext-real non negative Element of REAL
v2 . 1 is V17() V18() V19() V23() V24() V25() finite cardinal integer ext-real non negative Element of REAL
(v2 ^ <*g*>) . 1 is V17() V18() V19() V23() V24() V25() finite cardinal integer ext-real non negative Element of REAL
n is V17() V18() V19() V23() V24() V25() finite cardinal integer ext-real non negative Element of NAT
2 * n is V17() V18() V19() V23() V24() V25() finite cardinal integer ext-real non negative Element of NAT
i is V17() V18() V19() V23() V24() V25() finite cardinal integer ext-real non negative Element of NAT
n + i is V17() V18() V19() V23() V24() V25() finite cardinal integer ext-real non negative Element of NAT
f is set
g is Relation-like NAT -defined REAL -valued Function-like finite FinSequence-like FinSubsequence-like V88() V89() V90() Element of REAL *
G is Relation-like NAT -defined REAL -valued Function-like finite FinSequence-like FinSubsequence-like V88() V89() V90() Element of REAL *
G . (n + i) is V24() V25() ext-real Element of REAL
W is non empty oriented finite MultiGraphStruct
the carrier' of W is finite set
K33( the carrier' of W,Real>=0) is set
K32(K33( the carrier' of W,Real>=0)) is set
the carrier of W is finite set
v1 is Relation-like NAT -defined the carrier' of W -valued Function-like finite FinSequence-like FinSubsequence-like oriented Chain of W
v2 is Relation-like the carrier' of W -defined Real>=0 -valued Function-like finite total quasi_total Element of K32(K33( the carrier' of W,Real>=0))
VG is Element of the carrier of W
Ug is Element of the carrier of W
Vg is Relation-like NAT -defined the carrier' of W -valued Function-like finite FinSequence-like FinSubsequence-like oriented Simple Chain of W
the Target of W is Relation-like the carrier' of W -defined the carrier of W -valued Function-like finite quasi_total Element of K32(K33( the carrier' of W, the carrier of W))
K33( the carrier' of W, the carrier of W) is finite set
K32(K33( the carrier' of W, the carrier of W)) is finite V30() set
len Vg is V17() V18() V19() V23() V24() V25() finite cardinal integer ext-real non negative Element of NAT
Vg . (len Vg) is set
RM is Relation-like NAT -defined the carrier of W -valued Function-like finite FinSequence-like FinSubsequence-like FinSequence of the carrier of W
len RM is V17() V18() V19() V23() V24() V25() finite cardinal integer ext-real non negative Element of NAT
RM /. (len Vg) is Element of the carrier of W
(len Vg) + 1 is non empty V17() V18() V19() V23() V24() V25() finite cardinal integer ext-real positive non negative Element of NAT
RM /. ((len Vg) + 1) is Element of the carrier of W
dom Vg is finite Element of K32(NAT)
dom RM is finite Element of K32(NAT)
RM . (len Vg) is set
the Target of W . (Vg . (len Vg)) is set
RM . (len RM) is set
RM /. 1 is Element of the carrier of W
1 + 1 is non empty V17() V18() V19() V23() V24() V25() finite cardinal integer ext-real positive non negative Element of NAT
RM /. (1 + 1) is Element of the carrier of W
Vg . 1 is set
cn is Element of the carrier of W
the Source of W is Relation-like the carrier' of W -defined the carrier of W -valued Function-like finite quasi_total Element of K32(K33( the carrier' of W, the carrier of W))
the Source of W . (Vg . 1) is set
RM . 1 is set
{VG} is non empty V5() finite 1 -element set
Seg n is finite n -element Element of K32(NAT)
mi is V17() V18() V19() V23() V24() V25() finite cardinal integer ext-real non negative Element of NAT
n * mi is V17() V18() V19() V23() V24() V25() finite cardinal integer ext-real non negative Element of NAT
(2 * n) + (n * mi) is V17() V18() V19() V23() V24() V25() finite cardinal integer ext-real non negative Element of NAT
((2 * n) + (n * mi)) + i is V17() V18() V19() V23() V24() V25() finite cardinal integer ext-real non negative Element of NAT
g . (((2 * n) + (n * mi)) + i) is V24() V25() ext-real Element of REAL
(W,cn,VG,v2) is V24() V25() ext-real Element of REAL
the Source of W . (Vg . (len Vg)) is set
vertices Vg is finite Element of K32( the carrier of W)
K32( the carrier of W) is finite V30() set
(vertices Vg) \ {VG} is finite Element of K32( the carrier of W)
n is V17() V18() V19() V23() V24() V25() finite cardinal integer ext-real non negative Element of NAT
(n) is Relation-like REAL * -defined REAL * -valued Function-like total quasi_total Element of Funcs ((REAL *),(REAL *))
(n) is Relation-like REAL * -defined REAL * -valued Function-like total quasi_total Element of Funcs ((REAL *),(REAL *))
((REAL *),(n),(n)) is Relation-like Function-like Element of Funcs ((REAL *),(REAL *))
((REAL *),((REAL *),(n),(n))) is non empty Relation-like NAT -defined Funcs ((REAL *),(REAL *)) -valued Function-like total quasi_total Element of K32(K33(NAT,(Funcs ((REAL *),(REAL *)))))
2 * n is V17() V18() V19() V23() V24() V25() finite cardinal integer ext-real non negative Element of NAT
i is V17() V18() V19() V23() V24() V25() finite cardinal integer ext-real non negative Element of NAT
((REAL *),((REAL *),(n),(n))) . i is Relation-like Function-like Element of Funcs ((REAL *),(REAL *))
i + 1 is non empty V17() V18() V19() V23() V24() V25() finite cardinal integer ext-real positive non negative Element of NAT
((REAL *),((REAL *),(n),(n))) . (i + 1) is Relation-like Function-like Element of Funcs ((REAL *),(REAL *))
f is Relation-like NAT -defined REAL -valued Function-like finite FinSequence-like FinSubsequence-like V88() V89() V90() Element of REAL *
((((REAL *),((REAL *),(n),(n))) . i),f) is Relation-like NAT -defined REAL -valued Function-like finite FinSequence-like FinSubsequence-like V88() V89() V90() Element of REAL *
((((REAL *),((REAL *),(n),(n))) . (i + 1)),f) is Relation-like NAT -defined REAL -valued Function-like finite FinSequence-like FinSubsequence-like V88() V89() V90() Element of REAL *
g is Relation-like NAT -defined REAL -valued Function-like finite FinSequence-like FinSubsequence-like V88() V89() V90() Element of REAL *
(g,n) is finite Element of K32(NAT)
dom g is finite Element of K32(NAT)
{ b₁ where b₁ is V17() V18() V19() V23() V24() V25() finite cardinal integer ext-real non negative Element of NAT : ( b₁ in dom g & 1 <= b₁ & b₁ <= n & not g . b₁ = - 1 & not g . (n + b₁) = - 1 ) } is set
(g,n) is Element of K32(NAT)
{ b₁ where b₁ is V17() V18() V19() V23() V24() V25() finite cardinal integer ext-real non negative Element of NAT : ( b₁ in dom g & 1 <= b₁ & b₁ <= n & g . b₁ = - 1 ) } is set
G is Relation-like NAT -defined REAL -valued Function-like finite FinSequence-like FinSubsequence-like V88() V89() V90() Element of REAL *
(G,n) is Element of K32(NAT)
dom G is finite Element of K32(NAT)
{ b₁ where b₁ is V17() V18() V19() V23() V24() V25() finite cardinal integer ext-real non negative Element of NAT : ( b₁ in dom G & 1 <= b₁ & b₁ <= n & G . b₁ = - 1 ) } is set
W is non empty oriented finite MultiGraphStruct
the carrier' of W is finite set
K33( the carrier' of W,Real>=0) is set
K32(K33( the carrier' of W,Real>=0)) is set
the carrier of W is finite set
v1 is Relation-like the carrier' of W -defined Real>=0 -valued Function-like finite total quasi_total Element of K32(K33( the carrier' of W,Real>=0))
v2 is Element of the carrier of W
n * n is V17() V18() V19() V23() V24() V25() finite cardinal integer ext-real non negative Element of NAT
3 * n is V17() V18() V19() V23() V24() V25() finite cardinal integer ext-real non negative Element of NAT
(n * n) + (3 * n) is V17() V18() V19() V23() V24() V25() finite cardinal integer ext-real non negative Element of NAT
((n * n) + (3 * n)) + 1 is non empty V17() V18() V19() V23() V24() V25() finite cardinal integer ext-real positive non negative Element of NAT
((g,n),g,n) is V17() V18() V19() V23() V24() V25() finite cardinal integer ext-real non negative Element of NAT
len f is V17() V18() V19() V23() V24() V25() finite cardinal integer ext-real non negative Element of NAT
((n),g) is Relation-like NAT -defined REAL -valued Function-like finite FinSequence-like FinSubsequence-like V88() V89() V90() Element of REAL *
((((n * n) + (3 * n)) + 1),((g,n),g,n),g,(- 1)) is Relation-like NAT -defined REAL -valued Function-like finite FinSequence-like FinSubsequence-like V88() V89() V90() FinSequence of REAL
(g,(((n * n) + (3 * n)) + 1),((g,n),g,n)) is Relation-like NAT -defined REAL -valued Function-like finite FinSequence-like FinSubsequence-like V88() V89() V90() FinSequence of REAL
((g,(((n * n) + (3 * n)) + 1),((g,n),g,n)),((g,n),g,n),(- 1)) is Relation-like NAT -defined REAL -valued Function-like finite FinSequence-like FinSubsequence-like V88() V89() V90() FinSequence of REAL
dom ((n),g) is finite Element of K32(NAT)
((n),((n),g)) is Relation-like NAT -defined REAL -valued Function-like finite FinSequence-like FinSubsequence-like V88() V89() V90() Element of REAL *
(((n),g),n) is Relation-like NAT -defined REAL -valued Function-like finite FinSequence-like FinSubsequence-like V88() V89() V90() Element of REAL *
Seg n is finite n -element Element of K32(NAT)
(2 * n) + n is V17() V18() V19() V23() V24() V25() finite cardinal integer ext-real non negative Element of NAT
2 + 1 is non empty V17() V18() V19() V23() V24() V25() finite cardinal integer ext-real positive non negative Element of NAT
(2 + 1) * n is V17() V18() V19() V23() V24() V25() finite cardinal integer ext-real non negative Element of NAT
dom f is finite Element of K32(NAT)
n + ((g,n),g,n) is V17() V18() V19() V23() V24() V25() finite cardinal integer ext-real non negative Element of NAT
g . (n + ((g,n),g,n)) is V24() V25() ext-real Element of REAL
{((g,n),g,n)} is non empty V5() finite V30() 1 -element Element of K32(NAT)
(g,n) \/ {((g,n),g,n)} is non empty Element of K32(NAT)
p is Element of the carrier of W
(2 * n) + ((g,n),g,n) is V17() V18() V19() V23() V24() V25() finite cardinal integer ext-real non negative Element of NAT
g . ((2 * n) + ((g,n),g,n)) is V24() V25() ext-real Element of REAL
P is Relation-like NAT -defined NAT -valued Function-like finite FinSequence-like FinSubsequence-like V88() V89() V90() V91() FinSequence of NAT
len P is V17() V18() V19() V23() V24() V25() finite cardinal integer ext-real non negative Element of NAT
p is Relation-like NAT -defined the carrier' of W -valued Function-like finite FinSequence-like FinSubsequence-like oriented Chain of W
cost (p,v1) is V24() V25() ext-real Element of REAL
(3 * n) + 1 is non empty V17() V18() V19() V23() V24() V25() finite cardinal integer ext-real positive non negative Element of NAT
len p is V17() V18() V19() V23() V24() V25() finite cardinal integer ext-real non negative Element of NAT
((n),g) /. (((n * n) + (3 * n)) + 1) is V24() V25() ext-real Element of REAL
((n),g) . (((n * n) + (3 * n)) + 1) is V24() V25() ext-real Element of REAL
((n),g) /. ((2 * n) + ((g,n),g,n)) is V24() V25() ext-real Element of REAL
((n),g) . ((2 * n) + ((g,n),g,n)) is V24() V25() ext-real Element of REAL
n + 1 is non empty V17() V18() V19() V23() V24() V25() finite cardinal integer ext-real positive non negative Element of NAT
((n),g) . (n + ((g,n),g,n)) is V24() V25() ext-real Element of REAL
n * (((n),g) /. (((n * n) + (3 * n)) + 1)) is V24() V25() ext-real Element of REAL
(2 * n) + (n * (((n),g) /. (((n * n) + (3 * n)) + 1))) is V24() V25() ext-real Element of REAL
((2 * n) + (n * (((n),g) /. (((n * n) + (3 * n)) + 1)))) + ((g,n),g,n) is V24() V25() ext-real Element of REAL
((n),g) /. (((2 * n) + (n * (((n),g) /. (((n * n) + (3 * n)) + 1)))) + ((g,n),g,n)) is V24() V25() ext-real Element of REAL
(((n),g),n,((g,n),g,n)) is V24() V25() ext-real Element of REAL
(2 * n) + (((n),g) /. (((n * n) + (3 * n)) + 1)) is V24() V25() ext-real Element of REAL
((n),g) /. ((2 * n) + (((n),g) /. (((n * n) + (3 * n)) + 1))) is V24() V25() ext-real Element of REAL
(((n),g) /. ((2 * n) + (((n),g) /. (((n * n) + (3 * n)) + 1)))) + (((n),g) /. (((2 * n) + (n * (((n),g) /. (((n * n) + (3 * n)) + 1)))) + ((g,n),g,n))) is V24() V25() ext-real Element of REAL
(((n),g) /. ((2 * n) + ((g,n),g,n))) + 0 is V24() V25() ext-real Element of REAL
(((n),g) /. ((2 * n) + ((g,n),g,n))) + (((n),g) /. (((2 * n) + (n * (((n),g) /. (((n * n) + (3 * n)) + 1)))) + ((g,n),g,n))) is V24() V25() ext-real Element of REAL
(n + ((g,n),g,n)) -' n is V17() V18() V19() V23() V24() V25() finite cardinal integer ext-real non negative Element of NAT
G . (n + ((g,n),g,n)) is V24() V25() ext-real Element of REAL
m is Element of the carrier of W
j is V17() V18() V19() V23() V24() V25() finite cardinal integer ext-real non negative Element of NAT
n + j is V17() V18() V19() V23() V24() V25() finite cardinal integer ext-real non negative Element of NAT
G . (n + j) is V24() V25() ext-real Element of REAL
cn is non empty Element of K32(NAT)
(n + j) -' n is V17() V18() V19() V23() V24() V25() finite cardinal integer ext-real non negative Element of NAT
(2 * n) + j is V17() V18() V19() V23() V24() V25() finite cardinal integer ext-real non negative Element of NAT
(2 * n) + 1 is non empty V17() V18() V19() V23() V24() V25() finite cardinal integer ext-real positive non negative Element of NAT
((2 * n) + j) -' (2 * n) is V17() V18() V19() V23() V24() V25() finite cardinal integer ext-real non negative Element of NAT
((n),g) . (n + j) is V24() V25() ext-real Element of REAL
g . (n + j) is V24() V25() ext-real Element of REAL
((n),g) . ((2 * n) + j) is V24() V25() ext-real Element of REAL
g . ((2 * n) + j) is V24() V25() ext-real Element of REAL
n * ((g,n),g,n) is V17() V18() V19() V23() V24() V25() finite cardinal integer ext-real non negative Element of NAT
(2 * n) + (n * ((g,n),g,n)) is V17() V18() V19() V23() V24() V25() finite cardinal integer ext-real non negative Element of NAT
((2 * n) + (n * ((g,n),g,n))) + j is V17() V18() V19() V23() V24() V25() finite cardinal integer ext-real non negative Element of NAT
((2 * n) + (n * (((n),g) /. (((n * n) + (3 * n)) + 1)))) + j is V24() V25() ext-real Element of REAL
((n),g) /. (((2 * n) + (n * (((n),g) /. (((n * n) + (3 * n)) + 1)))) + j) is V24() V25() ext-real Element of REAL
((n),g) . (((2 * n) + (n * ((g,n),g,n))) + j) is V24() V25() ext-real Element of REAL
g . (((2 * n) + (n * ((g,n),g,n))) + j) is V24() V25() ext-real Element of REAL
f . (((2 * n) + (n * ((g,n),g,n))) + j) is V24() V25() ext-real Element of REAL
(W,p,m,v1) is V24() V25() ext-real Element of REAL
((n),g) /. ((2 * n) + j) is V24() V25() ext-real Element of REAL
e is Relation-like NAT -defined NAT -valued Function-like finite FinSequence-like FinSubsequence-like V88() V89() V90() V91() FinSequence of NAT
len e is V17() V18() V19() V23() V24() V25() finite cardinal integer ext-real non negative Element of NAT
pe is Relation-like NAT -defined the carrier' of W -valued Function-like finite FinSequence-like FinSubsequence-like oriented Chain of W
cost (pe,v1) is V24() V25() ext-real Element of REAL
Q is Relation-like NAT -defined NAT -valued Function-like finite FinSequence-like FinSubsequence-like V88() V89() V90() V91() FinSequence of NAT
Q is V17() V18() V19() V23() V24() V25() finite cardinal integer ext-real non negative Element of NAT
len Q is V17() V18() V19() V23() V24() V25() finite cardinal integer ext-real non negative Element of NAT
Q . Q is V17() V18() V19() V23() V24() V25() finite cardinal integer ext-real non negative Element of REAL
q is Relation-like NAT -defined the carrier' of W -valued Function-like finite FinSequence-like FinSubsequence-like oriented Chain of W
((n),g) . j is V24() V25() ext-real Element of REAL
(((n),g),n) . j is V24() V25() ext-real Element of REAL
FS is Element of the carrier of W
Q is Relation-like NAT -defined the carrier' of W -valued Function-like finite FinSequence-like FinSubsequence-like oriented Chain of W
FT is V17() V18() V19() V23() V24() V25() finite cardinal integer ext-real non negative Element of NAT
n + FT is V17() V18() V19() V23() V24() V25() finite cardinal integer ext-real non negative Element of NAT
g . (n + FT) is V24() V25() ext-real Element of REAL
(2 * n) + FT is V17() V18() V19() V23() V24() V25() finite cardinal integer ext-real non negative Element of NAT
g . ((2 * n) + FT) is V24() V25() ext-real Element of REAL
v2 is Relation-like NAT -defined NAT -valued Function-like finite FinSequence-like FinSubsequence-like V88() V89() V90() V91() FinSequence of NAT
len v2 is V17() V18() V19() V23() V24() V25() finite cardinal integer ext-real non negative Element of NAT
P is Relation-like NAT -defined the carrier' of W -valued Function-like finite FinSequence-like FinSubsequence-like oriented Chain of W
cost (P,v1) is V24() V25() ext-real Element of REAL
cost (Q,v1) is V24() V25() ext-real Element of REAL
cost (q,v1) is V24() V25() ext-real Element of REAL
P is Relation-like NAT -defined the carrier' of W -valued Function-like finite FinSequence-like FinSubsequence-like oriented Chain of W
cost (P,v1) is V24() V25() ext-real Element of REAL
g . FT is V24() V25() ext-real Element of REAL
{ b₁ where b₁ is V17() V18() V19() V23() V24() V25() finite cardinal integer ext-real non negative Element of NAT : ( b₁ in dom g & 1 <= b₁ & b₁ <= n & not g . b₁ = - 1 & not g . (n + b₁) = - 1 ) } is set
g /. ((2 * n) + ((g,n),g,n)) is V24() V25() ext-real Element of REAL
g /. ((2 * n) + FT) is V24() V25() ext-real Element of REAL
P is V17() V18() V19() V23() V24() V25() finite cardinal integer ext-real non negative Element of NAT
(2 * n) + P is V17() V18() V19() V23() V24() V25() finite cardinal integer ext-real non negative Element of NAT
g /. ((2 * n) + P) is V24() V25() ext-real Element of REAL
cost (q,v1) is V24() V25() ext-real Element of REAL
cost (q,v1) is V24() V25() ext-real Element of REAL
cost (q,v1) is V24() V25() ext-real Element of REAL
((n),g) . j is V24() V25() ext-real Element of REAL
(((n),g),n,j) is V24() V25() ext-real Element of REAL
(((n),g) /. ((2 * n) + (((n),g) /. (((n * n) + (3 * n)) + 1)))) + (((n),g) /. (((2 * n) + (n * (((n),g) /. (((n * n) + (3 * n)) + 1)))) + j)) is V24() V25() ext-real Element of REAL
cost (q,v1) is V24() V25() ext-real Element of REAL
Q is set
<*Q*> is non empty V5() Relation-like NAT -defined Function-like constant finite 1 -element FinSequence-like FinSubsequence-like set
FS is Relation-like NAT -defined the carrier' of W -valued Function-like finite FinSequence-like FinSubsequence-like oriented Chain of W
len FS is V17() V18() V19() V23() V24() V25() finite cardinal integer ext-real non negative Element of NAT
FS . 1 is set
p ^ FS is Relation-like NAT -defined the carrier' of W -valued Function-like finite FinSequence-like FinSubsequence-like FinSequence of the carrier' of W
FT is Relation-like NAT -defined the carrier' of W -valued Function-like finite FinSequence-like FinSubsequence-like oriented Chain of W
cost (FS,v1) is V24() V25() ext-real Element of REAL
v1 . (FS . 1) is set
cost (FT,v1) is V24() V25() ext-real Element of REAL
Q is set
((n),g) . j is V24() V25() ext-real Element of REAL
cost (q,v1) is V24() V25() ext-real Element of REAL
G . ((2 * n) + j) is V24() V25() ext-real Element of REAL
Q is Element of the carrier of W
FS is Relation-like NAT -defined the carrier' of W -valued Function-like finite FinSequence-like FinSubsequence-like oriented Chain of W
g . j is V24() V25() ext-real Element of REAL
{ b₁ where b₁ is V17() V18() V19() V23() V24() V25() finite cardinal integer ext-real non negative Element of NAT : ( b₁ in dom g & 1 <= b₁ & b₁ <= n & not g . b₁ = - 1 & not g . (n + b₁) = - 1 ) } is set
g /. ((2 * n) + ((g,n),g,n)) is V24() V25() ext-real Element of REAL
g /. ((2 * n) + j) is V24() V25() ext-real Element of REAL
FT is V17() V18() V19() V23() V24() V25() finite cardinal integer ext-real non negative Element of NAT
(2 * n) + FT is V17() V18() V19() V23() V24() V25() finite cardinal integer ext-real non negative Element of NAT
g /. ((2 * n) + FT) is V24() V25() ext-real Element of REAL
cost (FS,v1) is V24() V25() ext-real Element of REAL
FS is Relation-like NAT -defined the carrier' of W -valued Function-like finite FinSequence-like FinSubsequence-like oriented Chain of W
cost (FS,v1) is V24() V25() ext-real Element of REAL
v2 is Element of the carrier of W
FT is Relation-like NAT -defined the carrier' of W -valued Function-like finite FinSequence-like FinSubsequence-like oriented Chain of W
P is V17() V18() V19() V23() V24() V25() finite cardinal integer ext-real non negative Element of NAT
n + P is V17() V18() V19() V23() V24() V25() finite cardinal integer ext-real non negative Element of NAT
g . (n + P) is V24() V25() ext-real Element of REAL
(2 * n) + P is V17() V18() V19() V23() V24() V25() finite cardinal integer ext-real non negative Element of NAT
g . ((2 * n) + P) is V24() V25() ext-real Element of REAL
P is Relation-like NAT -defined NAT -valued Function-like finite FinSequence-like FinSubsequence-like V88() V89() V90() V91() FinSequence of NAT
len P is V17() V18() V19() V23() V24() V25() finite cardinal integer ext-real non negative Element of NAT
v4 is Relation-like NAT -defined the carrier' of W -valued Function-like finite FinSequence-like FinSubsequence-like oriented Chain of W
cost (v4,v1) is V24() V25() ext-real Element of REAL
j4 is Relation-like NAT -defined the carrier' of W -valued Function-like finite FinSequence-like FinSubsequence-like oriented Chain of W
cost (j4,v1) is V24() V25() ext-real Element of REAL
cost (FT,v1) is V24() V25() ext-real Element of REAL
FT is Relation-like NAT -defined the carrier' of W -valued Function-like finite FinSequence-like FinSubsequence-like oriented Chain of W
cost (FT,v1) is V24() V25() ext-real Element of REAL
(((n),g),n) . (n + j) is V24() V25() ext-real Element of REAL
(((n),g),n,j) is V24() V25() ext-real Element of REAL
(((n),g) /. ((2 * n) + (((n),g) /. (((n * n) + (3 * n)) + 1)))) + (((n),g) /. (((2 * n) + (n * (((n),g) /. (((n * n) + (3 * n)) + 1)))) + j)) is V24() V25() ext-real Element of REAL
((n),g) . j is V24() V25() ext-real Element of REAL
(((n),g) /. ((2 * n) + ((g,n),g,n))) + (W,p,m,v1) is V24() V25() ext-real Element of REAL
(((n),g) /. ((2 * n) + j)) + 0 is V24() V25() ext-real Element of REAL
(((n),g) /. ((2 * n) + j)) + (W,p,m,v1) is V24() V25() ext-real Element of REAL
e is V17() V18() V19() V23() V24() V25() finite cardinal integer ext-real non negative Element of NAT
g . e is V24() V25() ext-real Element of REAL
e is set
<*e*> is non empty V5() Relation-like NAT -defined Function-like constant finite 1 -element FinSequence-like FinSubsequence-like set
pe is Relation-like NAT -defined the carrier' of W -valued Function-like finite FinSequence-like FinSubsequence-like oriented Chain of W
len pe is V17() V18() V19() V23() V24() V25() finite cardinal integer ext-real non negative Element of NAT
pe . 1 is set
p ^ pe is Relation-like NAT -defined the carrier' of W -valued Function-like finite FinSequence-like FinSubsequence-like FinSequence of the carrier' of W
Q is Relation-like NAT -defined the carrier' of W -valued Function-like finite FinSequence-like FinSubsequence-like oriented Chain of W
<*j*> is non empty V5() Relation-like NAT -defined NAT -valued Function-like one-to-one constant finite 1 -element FinSequence-like FinSubsequence-like V88() V89() V90() V91() V92() V93() V94() V95() FinSequence of NAT
P ^ <*j*> is non empty Relation-like NAT -defined NAT -valued Function-like finite FinSequence-like FinSubsequence-like V88() V89() V90() V91() FinSequence of NAT
q is non empty Relation-like NAT -defined NAT -valued Function-like finite FinSequence-like FinSubsequence-like V88() V89() V90() V91() FinSequence of NAT
q . (len P) is V17() V18() V19() V23() V24() V25() finite cardinal integer ext-real non negative Element of REAL
P . (len P) is V17() V18() V19() V23() V24() V25() finite cardinal integer ext-real non negative Element of REAL
FS is V17() V18() V19() V23() V24() V25() finite cardinal integer ext-real non negative Element of NAT
len q is non empty V17() V18() V19() V23() V24() V25() finite cardinal integer ext-real positive non negative Element of NAT
(len P) + 1 is non empty V17() V18() V19() V23() V24() V25() finite cardinal integer ext-real positive non negative Element of NAT
q . FS is V17() V18() V19() V23() V24() V25() finite cardinal integer ext-real non negative Element of REAL
q . FS is V17() V18() V19() V23() V24() V25() finite cardinal integer ext-real non negative Element of REAL
P . FS is V17() V18() V19() V23() V24() V25() finite cardinal integer ext-real non negative Element of REAL
q . FS is V17() V18() V19() V23() V24() V25() finite cardinal integer ext-real non negative Element of REAL
q . FS is V17() V18() V19() V23() V24() V25() finite cardinal integer ext-real non negative Element of REAL
Q is Relation-like NAT -defined the carrier' of W -valued Function-like finite FinSequence-like FinSubsequence-like oriented Chain of W
len Q is V17() V18() V19() V23() V24() V25() finite cardinal integer ext-real non negative Element of NAT
(len p) + 1 is non empty V17() V18() V19() V23() V24() V25() finite cardinal integer ext-real positive non negative Element of NAT
(len Q) + 1 is non empty V17() V18() V19() V23() V24() V25() finite cardinal integer ext-real positive non negative Element of NAT
the Source of W is Relation-like the carrier' of W -defined the carrier of W -valued Function-like finite quasi_total Element of K32(K33( the carrier' of W, the carrier of W))
K33( the carrier' of W, the carrier of W) is finite set
K32(K33( the carrier' of W, the carrier of W)) is finite V30() set
the Target of W is Relation-like the carrier' of W -defined the carrier of W -valued Function-like finite quasi_total Element of K32(K33( the carrier' of W, the carrier of W))
v2 is V17() V18() V19() V23() V24() V25() finite cardinal integer ext-real non negative set
Q . v2 is set
the Target of W . (Q . v2) is set
the Source of W . (Q . v2) is set
q . v2 is V17() V18() V19() V23() V24() V25() finite cardinal integer ext-real non negative Element of REAL
v2 + 1 is non empty V17() V18() V19() V23() V24() V25() finite cardinal integer ext-real positive non negative Element of NAT
q . (v2 + 1) is V17() V18() V19() V23() V24() V25() finite cardinal integer ext-real non negative Element of REAL
p . v2 is set
the Source of W . (p . v2) is set
P . v2 is V17() V18() V19() V23() V24() V25() finite cardinal integer ext-real non negative Element of REAL
the Target of W . (p . v2) is set
v2 + 1 is non empty V17() V18() V19() V23() V24() V25() finite cardinal integer ext-real positive non negative Element of NAT
P . (v2 + 1) is V17() V18() V19() V23() V24() V25() finite cardinal integer ext-real non negative Element of REAL
Q . v2 is set
the Source of W . (Q . v2) is set
q . v2 is V17() V18() V19() V23() V24() V25() finite cardinal integer ext-real non negative Element of REAL
the Target of W . (Q . v2) is set
q . (v2 + 1) is V17() V18() V19() V23() V24() V25() finite cardinal integer ext-real non negative Element of REAL
cost (pe,v1) is V24() V25() ext-real Element of REAL
(cost (p,v1)) + (cost (pe,v1)) is V24() V25() ext-real Element of REAL
cost (Q,v1) is V24() V25() ext-real Element of REAL
v1 . (pe . 1) is set
v2 is Element of the carrier of W
P is V17() V18() V19() V23() V24() V25() finite cardinal integer ext-real non negative Element of NAT
n * P is V17() V18() V19() V23() V24() V25() finite cardinal integer ext-real non negative Element of NAT
(2 * n) + (n * P) is V17() V18() V19() V23() V24() V25() finite cardinal integer ext-real non negative Element of NAT
((2 * n) + (n * P)) + j is V17() V18() V19() V23() V24() V25() finite cardinal integer ext-real non negative Element of NAT
f . (((2 * n) + (n * P)) + j) is V24() V25() ext-real Element of REAL
(W,v2,m,v1) is V24() V25() ext-real Element of REAL
P is set
v2 is Relation-like NAT -defined NAT -valued Function-like finite FinSequence-like FinSubsequence-like V88() V89() V90() V91() FinSequence of NAT
len v2 is V17() V18() V19() V23() V24() V25() finite cardinal integer ext-real non negative Element of NAT
P is Relation-like NAT -defined the carrier' of W -valued Function-like finite FinSequence-like FinSubsequence-like oriented Chain of W
cost (P,v1) is V24() V25() ext-real Element of REAL
G . ((2 * n) + j) is V24() V25() ext-real Element of REAL
(cost (p,v1)) + 0 is V24() V25() ext-real Element of REAL
v2 is Element of the carrier of W
P is Relation-like NAT -defined the carrier' of W -valued Function-like finite FinSequence-like FinSubsequence-like oriented Chain of W
cost (P,v1) is V24() V25() ext-real Element of REAL
P is Relation-like NAT -defined the carrier' of W -valued Function-like finite FinSequence-like FinSubsequence-like oriented Chain of W
cost (P,v1) is V24() V25() ext-real Element of REAL
v4 is Element of the carrier of W
P is Relation-like NAT -defined the carrier' of W -valued Function-like finite FinSequence-like FinSubsequence-like oriented Chain of W
j4 is V17() V18() V19() V23() V24() V25() finite cardinal integer ext-real non negative Element of NAT
n + j4 is V17() V18() V19() V23() V24() V25() finite cardinal integer ext-real non negative Element of NAT
g . (n + j4) is V24() V25() ext-real Element of REAL
(2 * n) + j4 is V17() V18() V19() V23() V24() V25() finite cardinal integer ext-real non negative Element of NAT
g . ((2 * n) + j4) is V24() V25() ext-real Element of REAL
rn is Relation-like NAT -defined NAT -valued Function-like finite FinSequence-like FinSubsequence-like V88() V89() V90() V91() FinSequence of NAT
len rn is V17() V18() V19() V23() V24() V25() finite cardinal integer ext-real non negative Element of NAT
RR is Relation-like NAT -defined the carrier' of W -valued Function-like finite FinSequence-like FinSubsequence-like oriented Chain of W
cost (RR,v1) is V24() V25() ext-real Element of REAL
PP is Relation-like NAT -defined the carrier' of W -valued Function-like finite FinSequence-like FinSubsequence-like oriented Chain of W
cost (PP,v1) is V24() V25() ext-real Element of REAL
cost (P,v1) is V24() V25() ext-real Element of REAL
P is Relation-like NAT -defined the carrier' of W -valued Function-like finite FinSequence-like FinSubsequence-like oriented Chain of W
cost (P,v1) is V24() V25() ext-real Element of REAL
j is V17() V18() V19() V23() V24() V25() finite cardinal integer ext-real non negative Element of NAT
n + j is V17() V18() V19() V23() V24() V25() finite cardinal integer ext-real non negative Element of NAT
G . (n + j) is V24() V25() ext-real Element of REAL
m is V17() V18() V19() V23() V24() V25() finite cardinal integer ext-real non negative Element of NAT
(n + j) -' n is V17() V18() V19() V23() V24() V25() finite cardinal integer ext-real non negative Element of NAT
((n),g) . (n + j) is V24() V25() ext-real Element of REAL
g . (n + j) is V24() V25() ext-real Element of REAL
g . j is V24() V25() ext-real Element of REAL
((n),g) . j is V24() V25() ext-real Element of REAL
((2 * n) + (n * (((n),g) /. (((n * n) + (3 * n)) + 1)))) + j is V24() V25() ext-real Element of REAL
((n),g) /. (((2 * n) + (n * (((n),g) /. (((n * n) + (3 * n)) + 1)))) + j) is V24() V25() ext-real Element of REAL
((2 * n) + (n * ((g,n),g,n))) + j is V17() V18() V19() V23() V24() V25() finite cardinal integer ext-real non negative Element of NAT
f . (((2 * n) + (n * ((g,n),g,n))) + j) is V24() V25() ext-real Element of REAL
v3 is Element of the carrier of W
(W,p,v3,v1) is V24() V25() ext-real Element of REAL
((n),g) . (((2 * n) + (n * ((g,n),g,n))) + j) is V24() V25() ext-real Element of REAL
g . (((2 * n) + (n * ((g,n),g,n))) + j) is V24() V25() ext-real Element of REAL
e is set
n * m is V17() V18() V19() V23() V24() V25() finite cardinal integer ext-real non negative Element of NAT
(2 * n) + (n * m) is V17() V18() V19() V23() V24() V25() finite cardinal integer ext-real non negative Element of NAT
((2 * n) + (n * m)) + j is V17() V18() V19() V23() V24() V25() finite cardinal integer ext-real non negative Element of NAT
f . (((2 * n) + (n * m)) + j) is V24() V25() ext-real Element of REAL
n * m is V17() V18() V19() V23() V24() V25() finite cardinal integer ext-real non negative Element of NAT
(2 * n) + (n * m) is V17() V18() V19() V23() V24() V25() finite cardinal integer ext-real non negative Element of NAT
((2 * n) + (n * m)) + j is V17() V18() V19() V23() V24() V25() finite cardinal integer ext-real non negative Element of NAT
f . (((2 * n) + (n * m)) + j) is V24() V25() ext-real Element of REAL
m is V17() V18() V19() V23() V24() V25() finite cardinal integer ext-real non negative Element of NAT
n + m is V17() V18() V19() V23() V24() V25() finite cardinal integer ext-real non negative Element of NAT
G . (n + m) is V24() V25() ext-real Element of REAL
g . (n + m) is V24() V25() ext-real Element of REAL
n is V17() V18() V19() V23() V24() V25() finite cardinal integer ext-real non negative Element of NAT
(n) is Relation-like REAL * -defined REAL * -valued Function-like total quasi_total Element of Funcs ((REAL *),(REAL *))
(n) is Relation-like REAL * -defined REAL * -valued Function-like total quasi_total Element of Funcs ((REAL *),(REAL *))
(n) is Relation-like REAL * -defined REAL * -valued Function-like total quasi_total Element of Funcs ((REAL *),(REAL *))
((REAL *),(n),(n)) is Relation-like Function-like Element of Funcs ((REAL *),(REAL *))
(((REAL *),(n),(n)),n) is Relation-like REAL * -defined REAL * -valued Function-like total quasi_total Element of Funcs ((REAL *),(REAL *))
2 * n is V17() V18() V19() V23() V24() V25() finite cardinal integer ext-real non negative Element of NAT
i is V17() V18() V19() V23() V24() V25() finite cardinal integer ext-real non negative Element of NAT
(2 * n) + i is V17() V18() V19() V23() V24() V25() finite cardinal integer ext-real non negative Element of NAT
f is Relation-like NAT -defined REAL -valued Function-like finite FinSequence-like FinSubsequence-like V88() V89() V90() Element of REAL *
((n),f) is Relation-like NAT -defined REAL -valued Function-like finite FinSequence-like FinSubsequence-like V88() V89() V90() Element of REAL *
g is Relation-like NAT -defined REAL -valued Function-like finite FinSequence-like FinSubsequence-like V88() V89() V90() Element of REAL *
(g,n) is Element of K32(NAT)
dom g is finite Element of K32(NAT)
{ b₁ where b₁ is V17() V18() V19() V23() V24() V25() finite cardinal integer ext-real non negative Element of NAT : ( b₁ in dom g & 1 <= b₁ & b₁ <= n & g . b₁ = - 1 ) } is set
(g,n) is finite Element of K32(NAT)
{ b₁ where b₁ is V17() V18() V19() V23() V24() V25() finite cardinal integer ext-real non negative Element of NAT : ( b₁ in dom g & 1 <= b₁ & b₁ <= n & not g . b₁ = - 1 ) } is set
(g,n) \/ (g,n) is Element of K32(NAT)
g . ((2 * n) + i) is V24() V25() ext-real Element of REAL
G is non empty oriented finite MultiGraphStruct
the carrier' of G is finite set
K33( the carrier' of G,Real>=0) is set
K32(K33( the carrier' of G,Real>=0)) is set
the carrier of G is finite set
W is Relation-like the carrier' of G -defined Real>=0 -valued Function-like finite total quasi_total Element of K32(K33( the carrier' of G,Real>=0))
v1 is Element of the carrier of G
v2 is Element of the carrier of G
Seg n is finite n -element Element of K32(NAT)
n + 1 is non empty V17() V18() V19() V23() V24() V25() finite cardinal integer ext-real positive non negative Element of NAT
f . (n + 1) is V24() V25() ext-real Element of REAL
((REAL *),((REAL *),(n),(n))) is non empty Relation-like NAT -defined Funcs ((REAL *),(REAL *)) -valued Function-like total quasi_total Element of K32(K33(NAT,(Funcs ((REAL *),(REAL *)))))
(((REAL *),(n),(n)),f,n) is V17() V18() V19() V23() V24() V25() finite cardinal integer ext-real non negative Element of NAT
n * n is V17() V18() V19() V23() V24() V25() finite cardinal integer ext-real non negative Element of NAT
3 * n is V17() V18() V19() V23() V24() V25() finite cardinal integer ext-real non negative Element of NAT
(n * n) + (3 * n) is V17() V18() V19() V23() V24() V25() finite cardinal integer ext-real non negative Element of NAT
((n * n) + (3 * n)) + 1 is non empty V17() V18() V19() V23() V24() V25() finite cardinal integer ext-real positive non negative Element of NAT
((REAL *),((REAL *),(n),(n))) . (((REAL *),(n),(n)),f,n) is Relation-like Function-like Element of Funcs ((REAL *),(REAL *))
((((REAL *),((REAL *),(n),(n))) . (((REAL *),(n),(n)),f,n)),f) is Relation-like NAT -defined REAL -valued Function-like finite FinSequence-like FinSubsequence-like V88() V89() V90() Element of REAL *
VG is non empty Element of K32(NAT)
p is set
P is V17() V18() V19() V23() V24() V25() finite cardinal integer ext-real non negative Element of NAT
g . P is V24() V25() ext-real Element of REAL
P is V17() V18() V19() V23() V24() V25() finite cardinal integer ext-real non negative Element of NAT
g . P is V24() V25() ext-real Element of REAL
len f is V17() V18() V19() V23() V24() V25() finite cardinal integer ext-real non negative Element of NAT
p is set
P is V17() V18() V19() V23() V24() V25() finite cardinal integer ext-real non negative Element of NAT
dom f is finite Element of K32(NAT)
g . P is V24() V25() ext-real Element of REAL
g . P is V24() V25() ext-real Element of REAL
g . P is V24() V25() ext-real Element of REAL
dom f is finite Element of K32(NAT)
p is V17() V18() V19() V23() V24() V25() finite cardinal integer ext-real non negative Element of NAT
f . p is V24() V25() ext-real Element of REAL
P is V17() V18() V19() V23() V24() V25() finite cardinal integer ext-real non negative Element of NAT
n + P is V17() V18() V19() V23() V24() V25() finite cardinal integer ext-real non negative Element of NAT
f . (n + P) is V24() V25() ext-real Element of REAL
((REAL *),((REAL *),(n),(n))) . 1 is Relation-like Function-like Element of Funcs ((REAL *),(REAL *))
((((REAL *),((REAL *),(n),(n))) . 1),f) is Relation-like NAT -defined REAL -valued Function-like finite FinSequence-like FinSubsequence-like V88() V89() V90() Element of REAL *
(((((REAL *),((REAL *),(n),(n))) . 1),f),n) is Element of K32(NAT)
dom ((((REAL *),((REAL *),(n),(n))) . 1),f) is finite Element of K32(NAT)
{ b₁ where b₁ is V17() V18() V19() V23() V24() V25() finite cardinal integer ext-real non negative Element of NAT : ( b₁ in dom ((((REAL *),((REAL *),(n),(n))) . 1),f) & 1 <= b₁ & b₁ <= n & ((((REAL *),((REAL *),(n),(n))) . 1),f) . b₁ = - 1 ) } is set
p is V17() V18() V19() V23() V24() V25() finite cardinal integer ext-real non negative Element of NAT
((REAL *),((REAL *),(n),(n))) . p is Relation-like Function-like Element of Funcs ((REAL *),(REAL *))
((((REAL *),((REAL *),(n),(n))) . p),f) is Relation-like NAT -defined REAL -valued Function-like finite FinSequence-like FinSubsequence-like V88() V89() V90() Element of REAL *
(((((REAL *),((REAL *),(n),(n))) . p),f),n) is Element of K32(NAT)
dom ((((REAL *),((REAL *),(n),(n))) . p),f) is finite Element of K32(NAT)
{ b₁ where b₁ is V17() V18() V19() V23() V24() V25() finite cardinal integer ext-real non negative Element of NAT : ( b₁ in dom ((((REAL *),((REAL *),(n),(n))) . p),f) & 1 <= b₁ & b₁ <= n & ((((REAL *),((REAL *),(n),(n))) . p),f) . b₁ = - 1 ) } is set
p + 1 is non empty V17() V18() V19() V23() V24() V25() finite cardinal integer ext-real positive non negative Element of NAT
((REAL *),((REAL *),(n),(n))) . (p + 1) is Relation-like Function-like Element of Funcs ((REAL *),(REAL *))
((((REAL *),((REAL *),(n),(n))) . (p + 1)),f) is Relation-like NAT -defined REAL -valued Function-like finite FinSequence-like FinSubsequence-like V88() V89() V90() Element of REAL *
(((((REAL *),((REAL *),(n),(n))) . (p + 1)),f),n) is Element of K32(NAT)
dom ((((REAL *),((REAL *),(n),(n))) . (p + 1)),f) is finite Element of K32(NAT)
{ b₁ where b₁ is V17() V18() V19() V23() V24() V25() finite cardinal integer ext-real non negative Element of NAT : ( b₁ in dom ((((REAL *),((REAL *),(n),(n))) . (p + 1)),f) & 1 <= b₁ & b₁ <= n & ((((REAL *),((REAL *),(n),(n))) . (p + 1)),f) . b₁ = - 1 ) } is set
(((((REAL *),((REAL *),(n),(n))) . p),f),n) is finite Element of K32(NAT)
{ b₁ where b₁ is V17() V18() V19() V23() V24() V25() finite cardinal integer ext-real non negative Element of NAT : ( b₁ in dom ((((REAL *),((REAL *),(n),(n))) . p),f) & 1 <= b₁ & b₁ <= n & not ((((REAL *),((REAL *),(n),(n))) . p),f) . b₁ = - 1 & not ((((REAL *),((REAL *),(n),(n))) . p),f) . (n + b₁) = - 1 ) } is set
nk is Element of the carrier of G
m is V17() V18() V19() V23() V24() V25() finite cardinal integer ext-real non negative Element of NAT
n + m is V17() V18() V19() V23() V24() V25() finite cardinal integer ext-real non negative Element of NAT
((((REAL *),((REAL *),(n),(n))) . (p + 1)),f) . (n + m) is V24() V25() ext-real Element of REAL
(2 * n) + m is V17() V18() V19() V23() V24() V25() finite cardinal integer ext-real non negative Element of NAT
((((REAL *),((REAL *),(n),(n))) . (p + 1)),f) . ((2 * n) + m) is V24() V25() ext-real Element of REAL
nj is V17() V18() V19() V23() V24() V25() finite cardinal integer ext-real non negative Element of NAT
n + nj is V17() V18() V19() V23() V24() V25() finite cardinal integer ext-real non negative Element of NAT
((((REAL *),((REAL *),(n),(n))) . (p + 1)),f) . (n + nj) is V24() V25() ext-real Element of REAL
j is V17() V18() V19() V23() V24() V25() finite cardinal integer ext-real non negative Element of NAT
n * j is V17() V18() V19() V23() V24() V25() finite cardinal integer ext-real non negative Element of NAT
(2 * n) + (n * j) is V17() V18() V19() V23() V24() V25() finite cardinal integer ext-real non negative Element of NAT
((2 * n) + (n * j)) + nj is V17() V18() V19() V23() V24() V25() finite cardinal integer ext-real non negative Element of NAT
f . (((2 * n) + (n * j)) + nj) is V24() V25() ext-real Element of REAL
v3 is V17() V18() V19() V23() V24() V25() finite cardinal integer ext-real non negative Element of NAT
n + v3 is V17() V18() V19() V23() V24() V25() finite cardinal integer ext-real non negative Element of NAT
((((REAL *),((REAL *),(n),(n))) . (p + 1)),f) . (n + v3) is V24() V25() ext-real Element of REAL
1 + 0 is non empty V17() V18() V19() V23() V24() V25() finite cardinal integer ext-real positive non negative Element of NAT
nk is Element of the carrier of G
m is V17() V18() V19() V23() V24() V25() finite cardinal integer ext-real non negative Element of NAT
n + m is V17() V18() V19() V23() V24() V25() finite cardinal integer ext-real non negative Element of NAT
((((REAL *),((REAL *),(n),(n))) . (p + 1)),f) . (n + m) is V24() V25() ext-real Element of REAL
(2 * n) + m is V17() V18() V19() V23() V24() V25() finite cardinal integer ext-real non negative Element of NAT
((((REAL *),((REAL *),(n),(n))) . (p + 1)),f) . ((2 * n) + m) is V24() V25() ext-real Element of REAL
nj is V17() V18() V19() V23() V24() V25() finite cardinal integer ext-real non negative Element of NAT
n + nj is V17() V18() V19() V23() V24() V25() finite cardinal integer ext-real non negative Element of NAT
((((REAL *),((REAL *),(n),(n))) . (p + 1)),f) . (n + nj) is V24() V25() ext-real Element of REAL
j is V17() V18() V19() V23() V24() V25() finite cardinal integer ext-real non negative Element of NAT
n * j is V17() V18() V19() V23() V24() V25() finite cardinal integer ext-real non negative Element of NAT
(2 * n) + (n * j) is V17() V18() V19() V23() V24() V25() finite cardinal integer ext-real non negative Element of NAT
((2 * n) + (n * j)) + nj is V17() V18() V19() V23() V24() V25() finite cardinal integer ext-real non negative Element of NAT
f . (((2 * n) + (n * j)) + nj) is V24() V25() ext-real Element of REAL
v3 is V17() V18() V19() V23() V24() V25() finite cardinal integer ext-real non negative Element of NAT
n + v3 is V17() V18() V19() V23() V24() V25() finite cardinal integer ext-real non negative Element of NAT
((((REAL *),((REAL *),(n),(n))) . (p + 1)),f) . (n + v3) is V24() V25() ext-real Element of REAL
P is Element of the carrier of G
p is V17() V18() V19() V23() V24() V25() finite cardinal integer ext-real non negative Element of NAT
n + p is V17() V18() V19() V23() V24() V25() finite cardinal integer ext-real non negative Element of NAT
((((REAL *),((REAL *),(n),(n))) . (p + 1)),f) . (n + p) is V24() V25() ext-real Element of REAL
(2 * n) + p is V17() V18() V19() V23() V24() V25() finite cardinal integer ext-real non negative Element of NAT
((((REAL *),((REAL *),(n),(n))) . (p + 1)),f) . ((2 * n) + p) is V24() V25() ext-real Element of REAL
nk is V17() V18() V19() V23() V24() V25() finite cardinal integer ext-real non negative Element of NAT
n + nk is V17() V18() V19() V23() V24() V25() finite cardinal integer ext-real non negative Element of NAT
((((REAL *),((REAL *),(n),(n))) . (p + 1)),f) . (n + nk) is V24() V25() ext-real Element of REAL
P is V17() V18() V19() V23() V24() V25() finite cardinal integer ext-real non negative Element of NAT
n * P is V17() V18() V19() V23() V24() V25() finite cardinal integer ext-real non negative Element of NAT
(2 * n) + (n * P) is V17() V18() V19() V23() V24() V25() finite cardinal integer ext-real non negative Element of NAT
((2 * n) + (n * P)) + nk is V17() V18() V19() V23() V24() V25() finite cardinal integer ext-real non negative Element of NAT
f . (((2 * n) + (n * P)) + nk) is V24() V25() ext-real Element of REAL
m is V17() V18() V19() V23() V24() V25() finite cardinal integer ext-real non negative Element of NAT
n + m is V17() V18() V19() V23() V24() V25() finite cardinal integer ext-real non negative Element of NAT
((((REAL *),((REAL *),(n),(n))) . (p + 1)),f) . (n + m) is V24() V25() ext-real Element of REAL
((REAL *),((REAL *),(n),(n))) . 0 is Relation-like Function-like Element of Funcs ((REAL *),(REAL *))
((((REAL *),((REAL *),(n),(n))) . 0),f) is Relation-like NAT -defined REAL -valued Function-like finite FinSequence-like FinSubsequence-like V88() V89() V90() Element of REAL *
(((((REAL *),((REAL *),(n),(n))) . 0),f),n) is Element of K32(NAT)
dom ((((REAL *),((REAL *),(n),(n))) . 0),f) is finite Element of K32(NAT)
{ b₁ where b₁ is V17() V18() V19() V23() V24() V25() finite cardinal integer ext-real non negative Element of NAT : ( b₁ in dom ((((REAL *),((REAL *),(n),(n))) . 0),f) & 1 <= b₁ & b₁ <= n & ((((REAL *),((REAL *),(n),(n))) . 0),f) . b₁ = - 1 ) } is set
p is Element of the carrier of G
P is V17() V18() V19() V23() V24() V25() finite cardinal integer ext-real non negative Element of NAT
n + P is V17() V18() V19() V23() V24() V25() finite cardinal integer ext-real non negative Element of NAT
((((REAL *),((REAL *),(n),(n))) . 0),f) . (n + P) is V24() V25() ext-real Element of REAL
1 + 1 is non empty V17() V18() V19() V23() V24() V25() finite cardinal integer ext-real positive non negative Element of NAT
(2 * n) + P is V17() V18() V19() V23() V24() V25() finite cardinal integer ext-real non negative Element of NAT
((((REAL *),((REAL *),(n),(n))) . 0),f) . ((2 * n) + P) is V24() V25() ext-real Element of REAL
P is V17() V18() V19() V23() V24() V25() finite cardinal integer ext-real non negative Element of NAT
n + P is V17() V18() V19() V23() V24() V25() finite cardinal integer ext-real non negative Element of NAT
((((REAL *),((REAL *),(n),(n))) . 0),f) . (n + P) is V24() V25() ext-real Element of REAL
p is V17() V18() V19() V23() V24() V25() finite cardinal integer ext-real non negative Element of NAT
n * p is V17() V18() V19() V23() V24() V25() finite cardinal integer ext-real non negative Element of NAT
(2 * n) + (n * p) is V17() V18() V19() V23() V24() V25() finite cardinal integer ext-real non negative Element of NAT
((2 * n) + (n * p)) + P is V17() V18() V19() V23() V24() V25() finite cardinal integer ext-real non negative Element of NAT
f . (((2 * n) + (n * p)) + P) is V24() V25() ext-real Element of REAL
p is V17() V18() V19() V23() V24() V25() finite cardinal integer ext-real non negative Element of NAT
n + p is V17() V18() V19() V23() V24() V25() finite cardinal integer ext-real non negative Element of NAT
((((REAL *),((REAL *),(n),(n))) . 0),f) . (n + p) is V24() V25() ext-real Element of REAL
(g,n) is finite Element of K32(NAT)
{ b₁ where b₁ is V17() V18() V19() V23() V24() V25() finite cardinal integer ext-real non negative Element of NAT : ( b₁ in dom g & 1 <= b₁ & b₁ <= n & not g . b₁ = - 1 & not g . (n + b₁) = - 1 ) } is set
p is V17() V18() V19() V23() V24() V25() finite cardinal integer ext-real non negative Element of NAT
((REAL *),((REAL *),(n),(n))) . p is Relation-like Function-like Element of Funcs ((REAL *),(REAL *))
((((REAL *),((REAL *),(n),(n))) . p),f) is Relation-like NAT -defined REAL -valued Function-like finite FinSequence-like FinSubsequence-like V88() V89() V90() Element of REAL *
(((((REAL *),((REAL *),(n),(n))) . p),f),n) is finite Element of K32(NAT)
dom ((((REAL *),((REAL *),(n),(n))) . p),f) is finite Element of K32(NAT)
{ b₁ where b₁ is V17() V18() V19() V23() V24() V25() finite cardinal integer ext-real non negative Element of NAT : ( b₁ in dom ((((REAL *),((REAL *),(n),(n))) . p),f) & 1 <= b₁ & b₁ <= n & not ((((REAL *),((REAL *),(n),(n))) . p),f) . b₁ = - 1 & not ((((REAL *),((REAL *),(n),(n))) . p),f) . (n + b₁) = - 1 ) } is set
p is Element of the carrier of G
P is Element of the carrier of G
P is V17() V18() V19() V23() V24() V25() finite cardinal integer ext-real non negative Element of NAT
g . P is V24() V25() ext-real Element of REAL
n + P is V17() V18() V19() V23() V24() V25() finite cardinal integer ext-real non negative Element of NAT
g . (n + P) is V24() V25() ext-real Element of REAL
{ b₁ where b₁ is V17() V18() V19() V23() V24() V25() finite cardinal integer ext-real non negative Element of NAT : ( b₁ in dom g & 1 <= b₁ & b₁ <= n & not g . b₁ = - 1 & not g . (n + b₁) = - 1 ) } is set
p is V17() V18() V19() V23() V24() V25() finite cardinal integer ext-real non negative Element of NAT
n * p is V17() V18() V19() V23() V24() V25() finite cardinal integer ext-real non negative Element of NAT
(2 * n) + (n * p) is V17() V18() V19() V23() V24() V25() finite cardinal integer ext-real non negative Element of NAT
((2 * n) + (n * p)) + P is V17() V18() V19() V23() V24() V25() finite cardinal integer ext-real non negative Element of NAT
f . (((2 * n) + (n * p)) + P) is V24() V25() ext-real Element of REAL
(G,p,P,W) is V24() V25() ext-real Element of REAL
nk is set
f . 1 is V24() V25() ext-real Element of REAL
{ b₁ where b₁ is V17() V18() V19() V23() V24() V25() finite cardinal integer ext-real non negative Element of NAT : ( b₁ in dom f & 1 <= b₁ & b₁ <= n & not f . b₁ = - 1 & not f . (n + b₁) = - 1 ) } is set
1 + 0 is non empty V17() V18() V19() V23() V24() V25() finite cardinal integer ext-real positive non negative Element of NAT
n + i is V17() V18() V19() V23() V24() V25() finite cardinal integer ext-real non negative Element of NAT
g . (n + i) is V24() V25() ext-real Element of REAL
p is Relation-like NAT -defined NAT -valued Function-like finite FinSequence-like FinSubsequence-like V88() V89() V90() V91() FinSequence of NAT
len p is V17() V18() V19() V23() V24() V25() finite cardinal integer ext-real non negative Element of NAT
P is Relation-like NAT -defined the carrier' of G -valued Function-like finite FinSequence-like FinSubsequence-like oriented Chain of G
cost (P,W) is V24() V25() ext-real Element of REAL
p is Relation-like NAT -defined NAT -valued Function-like finite FinSequence-like FinSubsequence-like V88() V89() V90() V91() FinSequence of NAT
P is Relation-like NAT -defined the carrier' of G -valued Function-like finite FinSequence-like FinSubsequence-like oriented Chain of G
cost (P,W) is V24() V25() ext-real Element of REAL
p is Relation-like NAT -defined the carrier' of G -valued Function-like finite FinSequence-like FinSubsequence-like oriented Chain of G