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

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

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

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

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

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

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

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

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

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

f is set

{ b

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

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

(i,n) is finite Element of K32(NAT)

{ b

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

(i,n) is finite Element of K32(NAT)

{ b