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

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)

Real>=0 is non empty Element of K32(REAL)
{ b1 where b1 is V24() V25() ext-real Element of REAL : 0 <= b1 } is set

rng n is finite set
i is set

rng <*i*> is V5() finite set
{i} is non empty V5() finite 1 -element set
n is set

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

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

len i is V17() V18() V19() V23() V24() V25() finite cardinal integer ext-real non negative Element of NAT
i . 1 is 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)

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

Sum (RealSequence (i,f)) is V24() V25() ext-real Element of 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

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

len i is V17() V18() V19() V23() V24() V25() finite cardinal integer ext-real non negative Element of NAT
i . n is 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

len f is V17() V18() V19() V23() V24() V25() finite cardinal integer ext-real non negative Element of NAT
f . n is 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))

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

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

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

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

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
() \ {G} is Element of K32( the carrier of n)
(() \ {G}) \ {G} is Element of K32( the carrier of n)
{G} \/ {G} is non empty finite set
() \ ({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

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

cost (i,f) is V24() V25() ext-real Element of REAL
cost (v2,f) is V24() V25() ext-real Element of REAL

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

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

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

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

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

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

len Ug is V17() V18() V19() V23() V24() V25() finite cardinal integer ext-real non negative Element of NAT

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
() \ {W} is Element of K32( the carrier of n)

i is set
f is non empty finite MultiGraphStruct
the carrier' of f is finite set
the carrier of f is finite set

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

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
() \ {v2} is finite Element of K32( the carrier of f)
M . (len M) is set
the Target of f . (M . (len M)) is set

len cn is V17() V18() V19() V23() V24() V25() finite cardinal integer ext-real non negative Element of NAT

len mi is V17() V18() V19() V23() V24() V25() finite cardinal integer ext-real non negative Element of NAT

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)
(() \ {v2}) \ {v1} is finite Element of K32( the carrier of f)
{v2} \/ {v1} is non empty finite set
() \ ({v2} \/ {v1}) is finite Element of K32( the carrier of f)
() \ {v1} is finite Element of K32( the carrier of f)
(() \ {v1}) \ {v2} is finite Element of K32( the carrier of f)
cost (G,n) is V24() V25() ext-real Element of REAL

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)
() \ {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

len m 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

vertices nj is finite Element of K32( 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)

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

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

{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

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

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

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

len RM is V17() V18() V19() V23() V24() V25() finite cardinal integer ext-real non negative Element of NAT

len cn is V17() V18() V19() V23() V24() V25() finite cardinal integer ext-real non negative Element of NAT

(vertices Vg) \ {W} is finite Element of K32( the carrier of i)
{W} \/ {G} is non empty finite set

p . 1 is set
the Source of i . (p . 1) is set

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)

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
() \ {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

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

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

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

len p 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

m . 1 is set
the Source of f . (m . 1) is set
mi . 1 is set
the Source of f . (mi . 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
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)

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

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

W is Element of the carrier of f
v1 is Element of the carrier of f

cost (g,G) is V24() V25() ext-real Element of REAL
cost (v2,G) is V24() V25() ext-real Element of REAL

cost (v2,G) is V24() V25() ext-real Element 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)

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

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

dom f is finite Element of K32(NAT)
g is V24() V25() ext-real Element 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 . n is V24() V25() ext-real Element of REAL
G is V24() V25() ext-real Element 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

dom f is finite Element of K32(NAT)
g is V24() V25() ext-real Element 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

dom f is finite Element of K32(NAT)
g is V24() V25() ext-real Element 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)

K33(n,n) is set
K32(K33(n,n)) is set

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

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 ((),()) is non empty functional FUNCTION_DOMAIN of REAL * ,REAL *
Funcs ((),()) is non empty functional set

((),n) is non empty Relation-like NAT -defined Funcs ((),()) -valued Function-like total quasi_total Element of K32(K33(NAT,(Funcs ((),()))))
K33(NAT,(Funcs ((),()))) is V5() non finite set
K32(K33(NAT,(Funcs ((),())))) is V5() non finite set
((),n) . 0 is Relation-like Function-like Element of Funcs ((),())

id () is non empty Relation-like Function-like one-to-one Element of Funcs ((),())

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

dom f is set
rng f is set

((),i,n) is Relation-like Function-like Element of Funcs ((),())
((),((),i,n)) is non empty Relation-like NAT -defined Funcs ((),()) -valued Function-like total quasi_total Element of K32(K33(NAT,(Funcs ((),()))))
K33(NAT,(Funcs ((),()))) is V5() non finite set
K32(K33(NAT,(Funcs ((),())))) is V5() non finite set

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
((),((),i,n)) . (g + 1) is Relation-like Function-like Element of Funcs ((),())
((),(((),((),i,n)) . (g + 1)),f) is Relation-like NAT -defined Function-like finite FinSequence-like FinSubsequence-like Element of REAL *
((),((),i,n)) . g is Relation-like Function-like Element of Funcs ((),())
((),(((),((),i,n)) . g),f) is Relation-like NAT -defined Function-like finite FinSequence-like FinSubsequence-like Element of REAL *
((),i,((),(((),((),i,n)) . g),f)) is Relation-like NAT -defined Function-like finite FinSequence-like FinSubsequence-like Element of REAL *
((),n,((),i,((),(((),((),i,n)) . g),f))) is Relation-like NAT -defined Function-like finite FinSequence-like FinSubsequence-like Element of REAL *
((),(((),((),i,n)) . g),((),i,n)) is Relation-like Function-like Element of Funcs ((),())
dom ((),i,n) is set
dom ((),(((),((),i,n)) . g),((),i,n)) is set
((),((),(((),((),i,n)) . g),((),i,n)),f) is Relation-like NAT -defined Function-like finite FinSequence-like FinSubsequence-like Element of REAL *
((),((),i,n),((),(((),((),i,n)) . g),f)) is Relation-like NAT -defined Function-like finite FinSequence-like FinSubsequence-like 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
{ b1 where b1 is V17() V18() V19() V23() V24() V25() finite cardinal integer ext-real non negative Element of NAT : ( b1 in dom n & 1 <= b1 & b1 <= i & not n . b1 = - 1 & not n . (i + b1) = - 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 non empty Relation-like NAT -defined Funcs ((),()) -valued Function-like total quasi_total Element of K32(K33(NAT,(Funcs ((),()))))
K33(NAT,(Funcs ((),()))) is V5() non finite set
K32(K33(NAT,(Funcs ((),())))) is V5() non finite set

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
((),n) . g is Relation-like Function-like Element of Funcs ((),())

(((((),n) . g),i),f) is Element of K32(NAT)
dom ((((),n) . g),i) is finite Element of K32(NAT)
{ b1 where b1 is V17() V18() V19() V23() V24() V25() finite cardinal integer ext-real non negative Element of NAT : ( b1 in dom ((((),n) . g),i) & 1 <= b1 & b1 <= f & not ((((),n) . g),i) . b1 = - 1 & not ((((),n) . g),i) . (f + b1) = - 1 ) } is set
g is V17() V18() V19() V23() V24() V25() finite cardinal integer ext-real non negative set
((),n) . g is Relation-like Function-like Element of Funcs ((),())

(((((),n) . g),i),f) is Element of K32(NAT)
dom ((((),n) . g),i) is finite Element of K32(NAT)
{ b1 where b1 is V17() V18() V19() V23() V24() V25() finite cardinal integer ext-real non negative Element of NAT : ( b1 in dom ((((),n) . g),i) & 1 <= b1 & b1 <= f & not ((((),n) . g),i) . b1 = - 1 & not ((((),n) . g),i) . (f + b1) = - 1 ) } is set
g is V17() V18() V19() V23() V24() V25() finite cardinal integer ext-real non negative set
((),n) . g is Relation-like Function-like Element of Funcs ((),())

(((((),n) . g),i),f) is Element of K32(NAT)
dom ((((),n) . g),i) is finite Element of K32(NAT)
{ b1 where b1 is V17() V18() V19() V23() V24() V25() finite cardinal integer ext-real non negative Element of NAT : ( b1 in dom ((((),n) . g),i) & 1 <= b1 & b1 <= f & not ((((),n) . g),i) . b1 = - 1 & not ((((),n) . g),i) . (f + b1) = - 1 ) } is set
g is V17() V18() V19() V23() V24() V25() finite cardinal integer ext-real non negative Element of NAT
((),n) . g is Relation-like Function-like Element of Funcs ((),())

(((((),n) . g),i),f) is Element of K32(NAT)
dom ((((),n) . g),i) is finite Element of K32(NAT)
{ b1 where b1 is V17() V18() V19() V23() V24() V25() finite cardinal integer ext-real non negative Element of NAT : ( b1 in dom ((((),n) . g),i) & 1 <= b1 & b1 <= f & not ((((),n) . g),i) . b1 = - 1 & not ((((),n) . g),i) . (f + b1) = - 1 ) } is set
G is V17() V18() V19() V23() V24() V25() finite cardinal integer ext-real non negative Element of NAT
((),n) . G is Relation-like Function-like Element of Funcs ((),())

(((((),n) . G),i),f) is Element of K32(NAT)
dom ((((),n) . G),i) is finite Element of K32(NAT)
{ b1 where b1 is V17() V18() V19() V23() V24() V25() finite cardinal integer ext-real non negative Element of NAT : ( b1 in dom ((((),n) . G),i) & 1 <= b1 & b1 <= f & not ((((),n) . G),i) . b1 = - 1 & not ((((),n) . G),i) . (f + b1) = - 1 ) } is set

((),n) is non empty Relation-like NAT -defined Funcs ((),()) -valued Function-like total quasi_total Element of K32(K33(NAT,(Funcs ((),()))))
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

dom W is set
rng W is set

(n,G,i) is V17() V18() V19() V23() V24() V25() finite cardinal integer ext-real non negative Element of NAT
((),n) . (n,G,i) is Relation-like Function-like Element of Funcs ((),())
((((),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 *

(n,v1,i) is V17() V18() V19() V23() V24() V25() finite cardinal integer ext-real non negative Element of NAT
((),n) . (n,v1,i) is Relation-like Function-like Element of Funcs ((),())
((((),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 *

dom g is set
rng g is set
G is set
W is set
g . W is set

dom v2 is set
rng v2 is set

(n,v1,i) is V17() V18() V19() V23() V24() V25() finite cardinal integer ext-real non negative Element of NAT
((),n) . (n,v1,i) is Relation-like Function-like Element of Funcs ((),())
((((),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 *

dom W is set
rng W is set

dom G is set

dom W is set
rng W is set

(n,W,i) is V17() V18() V19() V23() V24() V25() finite cardinal integer ext-real non negative Element of NAT
((),n) . (n,W,i) is Relation-like Function-like Element of Funcs ((),())
((((),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 *

dom v1 is set
rng v1 is set

dom g is set

dom G is set
W is set

(n,v1,i) is V17() V18() V19() V23() V24() V25() finite cardinal integer ext-real non negative Element of NAT
((),n) . (n,v1,i) is Relation-like Function-like Element of Funcs ((),())
((((),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 *

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

(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

(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

(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

(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

(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

(i,f,g,G) is V24() V25() ext-real Element of REAL
G . n is set
(i,f,g) is set
v1 is set

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
{ b1 where b1 is V17() V18() V19() V23() V24() V25() finite cardinal integer ext-real non negative Element of NAT : ( b1 in dom n & 1 <= b1 & b1 <= i & not n . b1 = - 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

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
{ b1 where b1 is V17() V18() V19() V23() V24() V25() finite cardinal integer ext-real non negative Element of NAT : ( b1 in dom n & 1 <= b1 & b1 <= i & n . b1 = - 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,n) is Element of K32(NAT)
dom i is finite Element of K32(NAT)
{ b1 where b1 is V17() V18() V19() V23() V24() V25() finite cardinal integer ext-real non negative Element of NAT : ( b1 in dom i & 1 <= b1 & b1 <= n & not i . b1 = - 1 ) } is set
f is set
{ b1 where b1 is V17() V18() V19() V23() V24() V25() finite cardinal integer ext-real non negative Element of NAT : ( 1 <= b1 & b1 <= 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

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)
{ b1 where b1 is V17() V18() V19() V23() V24() V25() finite cardinal integer ext-real non negative Element of NAT : ( b1 in dom n & 1 <= b1 & b1 <= i & not n . b1 = - 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,n) is Element of K32(NAT)
dom i is finite Element of K32(NAT)
{ b1 where b1 is V17() V18() V19() V23() V24() V25() finite cardinal integer ext-real non negative Element of NAT : ( b1 in dom i & 1 <= b1 & b1 <= n & not i . b1 = - 1 & not i . (n + b1) = - 1 ) } is set
(i,n) is finite Element of K32(NAT)
{ b1 where b1 is V17() V18() V19() V23() V24() V25() finite cardinal integer ext-real non negative Element of NAT : ( b1 in dom i & 1 <= b1 & b1 <= n & not i . b1 = - 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,n) is Element of K32(NAT)
dom i is finite Element of K32(NAT)
{ b1 where b1 is V17() V18() V19() V23() V24() V25() finite cardinal integer ext-real non negative Element of NAT : ( b1 in dom i & 1 <= b1 & b1 <= n & not i . b1 = - 1 & not i . (n + b1) = - 1 ) } is set
(i,n) is finite Element of K32(NAT)
{ b1 where b1 is V17() V18() V19() V23() V24() V25() finite cardinal integer ext-real non negative Element of NAT : ( b1 in dom i & 1 <= b1 & b1 <= n & not i . b1 = - 1 ) } is set