:: GLIB_004 semantic presentation

REAL is non empty non trivial non finite set

NAT is non empty non trivial epsilon-transitive epsilon-connected ordinal non finite cardinal limit_cardinal Element of bool REAL

bool REAL is non empty non trivial non finite V101() set

COMPLEX is non empty non trivial non finite set

RAT is non empty non trivial non finite set

INT is non empty non trivial non finite set

[:COMPLEX,COMPLEX:] is non empty non trivial Relation-like non finite set

bool [:COMPLEX,COMPLEX:] is non empty non trivial non finite V101() set

[:[:COMPLEX,COMPLEX:],COMPLEX:] is non empty non trivial Relation-like non finite set

bool [:[:COMPLEX,COMPLEX:],COMPLEX:] is non empty non trivial non finite V101() set

[:REAL,REAL:] is non empty non trivial Relation-like non finite set

bool [:REAL,REAL:] is non empty non trivial non finite V101() set

[:[:REAL,REAL:],REAL:] is non empty non trivial Relation-like non finite set

bool [:[:REAL,REAL:],REAL:] is non empty non trivial non finite V101() set

[:RAT,RAT:] is non empty non trivial Relation-like non finite set

bool [:RAT,RAT:] is non empty non trivial non finite V101() set

[:[:RAT,RAT:],RAT:] is non empty non trivial Relation-like non finite set

bool [:[:RAT,RAT:],RAT:] is non empty non trivial non finite V101() set

[:INT,INT:] is non empty non trivial Relation-like non finite set

bool [:INT,INT:] is non empty non trivial non finite V101() set

[:[:INT,INT:],INT:] is non empty non trivial Relation-like non finite set

bool [:[:INT,INT:],INT:] is non empty non trivial non finite V101() set

[:NAT,NAT:] is non empty non trivial Relation-like non finite set

[:[:NAT,NAT:],NAT:] is non empty non trivial Relation-like non finite set

bool [:[:NAT,NAT:],NAT:] is non empty non trivial non finite V101() set

NAT is non empty non trivial epsilon-transitive epsilon-connected ordinal non finite cardinal limit_cardinal set

bool NAT is non empty non trivial non finite V101() set

bool NAT is non empty non trivial non finite V101() set

K195(NAT) is V35() set

{} is empty Relation-like non-empty empty-yielding RAT -valued Function-like one-to-one constant functional V21() epsilon-transitive epsilon-connected ordinal T-Sequence-like c=-linear natural real V30() finite finite-yielding V40() cardinal {} -element ext-real non positive non negative V50() V51() V52() V53() Function-yielding V99() FinSequence-yielding finite-support set

1 is non empty V21() epsilon-transitive epsilon-connected ordinal natural real V30() finite cardinal ext-real positive non negative Element of NAT

{{},1} is non empty finite V40() set

2 is non empty V21() epsilon-transitive epsilon-connected ordinal natural real V30() finite cardinal ext-real positive non negative Element of NAT

[:NAT,REAL:] is non empty non trivial Relation-like non finite set

bool [:NAT,REAL:] is non empty non trivial non finite V101() set

1 -tuples_on NAT is FinSequenceSet of NAT

_GraphSelectors is non empty Element of bool NAT

VertexSelector is V21() epsilon-transitive epsilon-connected ordinal natural real V30() finite cardinal ext-real non negative Element of NAT

EdgeSelector is V21() epsilon-transitive epsilon-connected ordinal natural real V30() finite cardinal ext-real non negative Element of NAT

SourceSelector is V21() epsilon-transitive epsilon-connected ordinal natural real V30() finite cardinal ext-real non negative Element of NAT

3 is non empty V21() epsilon-transitive epsilon-connected ordinal natural real V30() finite cardinal ext-real positive non negative Element of NAT

TargetSelector is V21() epsilon-transitive epsilon-connected ordinal natural real V30() finite cardinal ext-real non negative Element of NAT

4 is non empty V21() epsilon-transitive epsilon-connected ordinal natural real V30() finite cardinal ext-real positive non negative Element of NAT

{VertexSelector,EdgeSelector,SourceSelector,TargetSelector} is non empty finite Element of bool NAT

card {} is empty Relation-like non-empty empty-yielding RAT -valued Function-like one-to-one constant functional V21() epsilon-transitive epsilon-connected ordinal T-Sequence-like c=-linear natural real V30() finite finite-yielding V40() cardinal {} -element ext-real non positive non negative V50() V51() V52() V53() Function-yielding V99() FinSequence-yielding finite-support set

0 is empty Relation-like non-empty empty-yielding RAT -valued Function-like one-to-one constant functional V21() epsilon-transitive epsilon-connected ordinal T-Sequence-like c=-linear natural real V30() finite finite-yielding V40() cardinal {} -element ext-real non positive non negative V50() V51() V52() V53() Function-yielding V99() FinSequence-yielding finite-support Element of NAT

WeightSelector is V21() epsilon-transitive epsilon-connected ordinal natural real V30() finite cardinal ext-real non negative Element of NAT

5 is non empty V21() epsilon-transitive epsilon-connected ordinal natural real V30() finite cardinal ext-real positive non negative Element of NAT

G1 is Relation-like Function-like set

proj1 G1 is set

PMST is set

G2 is set

PMST .--> G2 is Relation-like {PMST} -defined Function-like one-to-one finite finite-support set

{PMST} is non empty trivial finite 1 -element set

{PMST} --> G2 is non empty Relation-like {PMST} -defined {G2} -valued Function-like constant total quasi_total finite finite-support Element of bool [:{PMST},{G2}:]

{G2} is non empty trivial finite 1 -element set

[:{PMST},{G2}:] is non empty Relation-like finite set

bool [:{PMST},{G2}:] is non empty finite V40() V101() set

G1 +* (PMST .--> G2) is Relation-like Function-like set

proj1 (G1 +* (PMST .--> G2)) is set

(proj1 G1) \/ {PMST} is non empty set

dom (PMST .--> G2) is trivial finite Element of bool {PMST}

bool {PMST} is non empty finite V40() V101() set

(proj1 G1) \/ (dom (PMST .--> G2)) is set

G1 is Relation-like Function-like set

proj1 G1 is set

G29 is set

PMST is set

G2 is set

PMST .--> G2 is Relation-like {PMST} -defined Function-like one-to-one finite finite-support set

{PMST} is non empty trivial finite 1 -element set

{PMST} --> G2 is non empty Relation-like {PMST} -defined {G2} -valued Function-like constant total quasi_total finite finite-support Element of bool [:{PMST},{G2}:]

{G2} is non empty trivial finite 1 -element set

[:{PMST},{G2}:] is non empty Relation-like finite set

bool [:{PMST},{G2}:] is non empty finite V40() V101() set

G1 +* (PMST .--> G2) is Relation-like Function-like set

proj1 (G1 +* (PMST .--> G2)) is set

dom (PMST .--> G2) is trivial finite Element of bool {PMST}

bool {PMST} is non empty finite V40() V101() set

(proj1 G1) \/ {PMST} is non empty set

G1 is Relation-like Function-like set

PMST is Relation-like Function-like set

G1 +* PMST is Relation-like Function-like set

support (G1 +* PMST) is set

support G1 is set

support PMST is set

(support G1) \/ (support PMST) is set

G2 is set

(G1 +* PMST) . G2 is set

G1 . G2 is set

PMST . G2 is set

proj1 PMST is set

G1 is Relation-like Function-like set

support G1 is set

PMST is set

G2 is set

PMST .--> G2 is Relation-like {PMST} -defined Function-like one-to-one finite finite-support set

{PMST} is non empty trivial finite 1 -element set

{PMST} --> G2 is non empty Relation-like {PMST} -defined {G2} -valued Function-like constant total quasi_total finite finite-support Element of bool [:{PMST},{G2}:]

{G2} is non empty trivial finite 1 -element set

[:{PMST},{G2}:] is non empty Relation-like finite set

bool [:{PMST},{G2}:] is non empty finite V40() V101() set

G1 +* (PMST .--> G2) is Relation-like Function-like set

support (G1 +* (PMST .--> G2)) is set

(support G1) \/ {PMST} is non empty set

G29 is set

(G1 +* (PMST .--> G2)) . G29 is set

G1 . G29 is set

G1 is set

PMST is set

G1 \ PMST is Element of bool G1

bool G1 is non empty set

G2 is Relation-like G1 -defined Function-like total V50() V51() V52() finite-support set

Sum G2 is V21() real ext-real set

G29 is Relation-like PMST -defined Function-like total V50() V51() V52() finite-support set

Sum G29 is V21() real ext-real set

VG1 is Relation-like G1 \ PMST -defined Function-like total V50() V51() V52() finite-support set

G29 +* VG1 is Relation-like Function-like V50() V51() V52() set

Sum VG1 is V21() real ext-real set

(Sum G29) + (Sum VG1) is V21() real ext-real set

dom G2 is Element of bool G1

dom G29 is Element of bool PMST

bool PMST is non empty set

dom VG1 is Element of bool (G1 \ PMST)

bool (G1 \ PMST) is non empty set

(dom G29) \/ (dom VG1) is set

EmptyBag G1 is Relation-like G1 -defined RAT -valued Function-like total V50() V51() V52() V53() finite-support Element of Bags G1

Bags G1 is non empty set

Bags G1 is non empty functional Element of bool (Bags G1)

bool (Bags G1) is non empty V101() set

(EmptyBag G1) +* G29 is Relation-like Function-like V50() V51() V52() set

proj1 ((EmptyBag G1) +* G29) is set

dom (EmptyBag G1) is Element of bool G1

(dom (EmptyBag G1)) \/ (dom G29) is set

G1 \/ (dom G29) is set

G1 \/ PMST is set

support ((EmptyBag G1) +* G29) is set

support (EmptyBag G1) is finite set

support G29 is finite set

(support (EmptyBag G1)) \/ (support G29) is finite set

(EmptyBag G1) +* VG1 is Relation-like Function-like V50() V51() V52() set

proj1 ((EmptyBag G1) +* VG1) is set

(dom (EmptyBag G1)) \/ (dom VG1) is set

G1 \/ (dom VG1) is set

G1 \/ (G1 \ PMST) is set

support ((EmptyBag G1) +* VG1) is set

support VG1 is finite set

(support (EmptyBag G1)) \/ (support VG1) is finite set

X is set

WG1 is Relation-like G1 -defined Function-like total V50() V51() V52() finite-support set

WG1 . X is V21() real ext-real Element of REAL

G29 . X is V21() real ext-real Element of REAL

X is Relation-like G1 -defined Function-like total V50() V51() V52() finite-support set

X . X is V21() real ext-real Element of REAL

(EmptyBag G1) . X is V21() epsilon-transitive epsilon-connected ordinal natural real V30() V31() finite cardinal ext-real non negative Element of REAL

G2 . X is V21() real ext-real Element of REAL

(WG1 . X) + (X . X) is V21() real ext-real set

WG1 + X is Relation-like G1 -defined Function-like total set

(WG1 + X) . X is set

WG1 is Relation-like G1 -defined Function-like total V50() V51() V52() finite-support set

WG1 . X is V21() real ext-real Element of REAL

(EmptyBag G1) . X is V21() epsilon-transitive epsilon-connected ordinal natural real V30() V31() finite cardinal ext-real non negative Element of REAL

X is Relation-like G1 -defined Function-like total V50() V51() V52() finite-support set

X . X is V21() real ext-real Element of REAL

VG1 . X is V21() real ext-real Element of REAL

G2 . X is V21() real ext-real Element of REAL

(WG1 . X) + (X . X) is V21() real ext-real set

WG1 + X is Relation-like G1 -defined Function-like total set

(WG1 + X) . X is set

WG1 is Relation-like G1 -defined Function-like total V50() V51() V52() finite-support set

X is Relation-like G1 -defined Function-like total V50() V51() V52() finite-support set

WG1 + X is Relation-like G1 -defined Function-like total set

WG1 is Relation-like G1 -defined Function-like total V50() V51() V52() finite-support set

X is Relation-like G1 -defined Function-like total V50() V51() V52() finite-support set

WG1 + X is Relation-like G1 -defined Function-like total set

Sum X is V21() real ext-real set

support X is finite set

canFS (support X) is Relation-like NAT -defined support X -valued Function-like one-to-one onto FinSequence-like FinSequence of support X

(canFS (support X)) * X is Relation-like NAT -defined Function-like V50() V51() V52() set

X is Relation-like NAT -defined REAL -valued Function-like FinSequence-like V50() V51() V52() FinSequence of REAL

Sum X is V21() real ext-real Element of REAL

K168() is Relation-like [:REAL,REAL:] -defined REAL -valued Function-like quasi_total V50() V51() V52() Element of bool [:[:REAL,REAL:],REAL:]

K221(REAL,X,K168()) is V21() real ext-real Element of REAL

proj2 (canFS (support X)) is set

dom X is Element of bool G1

dom X is Element of bool NAT

dom (canFS (support X)) is Element of bool NAT

Sum WG1 is V21() real ext-real set

support WG1 is finite set

canFS (support WG1) is Relation-like NAT -defined support WG1 -valued Function-like one-to-one onto FinSequence-like FinSequence of support WG1

(canFS (support WG1)) * WG1 is Relation-like NAT -defined Function-like V50() V51() V52() set

X is Relation-like NAT -defined REAL -valued Function-like FinSequence-like V50() V51() V52() FinSequence of REAL

Sum X is V21() real ext-real Element of REAL

K221(REAL,X,K168()) is V21() real ext-real Element of REAL

canFS (support G29) is Relation-like NAT -defined support G29 -valued Function-like one-to-one onto FinSequence-like FinSequence of support G29

(canFS (support G29)) * G29 is Relation-like NAT -defined Function-like V50() V51() V52() set

M is Relation-like NAT -defined REAL -valued Function-like FinSequence-like V50() V51() V52() FinSequence of REAL

Sum M is V21() real ext-real Element of REAL

K221(REAL,M,K168()) is V21() real ext-real Element of REAL

proj2 (canFS (support G29)) is set

dom M is Element of bool NAT

dom (canFS (support G29)) is Element of bool NAT

M is set

G29 . M is V21() real ext-real Element of REAL

WG1 . M is V21() real ext-real Element of REAL

(EmptyBag G1) . M is V21() epsilon-transitive epsilon-connected ordinal natural real V30() V31() finite cardinal ext-real non negative Element of REAL

M is V21() epsilon-transitive epsilon-connected ordinal natural real V30() finite cardinal ext-real non negative set

(canFS (support G29)) . M is set

M . M is V21() real ext-real Element of REAL

G29 . ((canFS (support G29)) . M) is V21() real ext-real Element of REAL

WG1 . ((canFS (support G29)) . M) is V21() real ext-real Element of REAL

X . M is V21() real ext-real Element of REAL

proj2 (canFS (support WG1)) is set

dom WG1 is Element of bool G1

dom X is Element of bool NAT

dom (canFS (support WG1)) is Element of bool NAT

canFS (support VG1) is Relation-like NAT -defined support VG1 -valued Function-like one-to-one onto FinSequence-like FinSequence of support VG1

(canFS (support VG1)) * VG1 is Relation-like NAT -defined Function-like V50() V51() V52() set

M is Relation-like NAT -defined REAL -valued Function-like FinSequence-like V50() V51() V52() FinSequence of REAL

Sum M is V21() real ext-real Element of REAL

K221(REAL,M,K168()) is V21() real ext-real Element of REAL

proj2 (canFS (support VG1)) is set

dom M is Element of bool NAT

dom (canFS (support VG1)) is Element of bool NAT

k is set

VG1 . k is V21() real ext-real Element of REAL

X . k is V21() real ext-real Element of REAL

(EmptyBag G1) . k is V21() epsilon-transitive epsilon-connected ordinal natural real V30() V31() finite cardinal ext-real non negative Element of REAL

k is V21() epsilon-transitive epsilon-connected ordinal natural real V30() finite cardinal ext-real non negative set

(canFS (support VG1)) . k is set

M . k is V21() real ext-real Element of REAL

VG1 . ((canFS (support VG1)) . k) is V21() real ext-real Element of REAL

X . ((canFS (support VG1)) . k) is V21() real ext-real Element of REAL

X . k is V21() real ext-real Element of REAL

G1 is set

PMST is set

{PMST} is non empty trivial finite 1 -element set

G2 is Relation-like G1 -defined Function-like total V50() V51() V52() finite-support set

dom G2 is Element of bool G1

bool G1 is non empty set

Sum G2 is V21() real ext-real set

G2 . PMST is V21() real ext-real Element of REAL

support G2 is finite set

canFS {PMST} is non empty Relation-like NAT -defined {PMST} -valued Function-like one-to-one onto FinSequence-like FinSequence of {PMST}

(canFS {PMST}) * G2 is Relation-like NAT -defined Function-like V50() V51() V52() set

G29 is Relation-like NAT -defined REAL -valued Function-like FinSequence-like V50() V51() V52() FinSequence of REAL

Sum G29 is V21() real ext-real Element of REAL

K168() is Relation-like [:REAL,REAL:] -defined REAL -valued Function-like quasi_total V50() V51() V52() Element of bool [:[:REAL,REAL:],REAL:]

K221(REAL,G29,K168()) is V21() real ext-real Element of REAL

<*PMST*> is Relation-like Function-like set

<*PMST*> * G2 is Relation-like Function-like V50() V51() V52() set

<*(G2 . PMST)*> is Relation-like NAT -defined REAL -valued Function-like FinSequence-like V50() V51() V52() Element of REAL *

REAL * is FinSequenceSet of REAL

G1 is set

PMST is Relation-like G1 -defined Function-like total V50() V51() V52() finite-support set

G2 is Relation-like G1 -defined Function-like total V50() V51() V52() finite-support set

Sum PMST is V21() real ext-real set

Sum G2 is V21() real ext-real set

support PMST is finite set

support G2 is finite set

(support PMST) \/ (support G2) is finite set

dom G2 is Element of bool G1

bool G1 is non empty set

dom PMST is Element of bool G1

VG1 is finite Element of bool G1

canFS VG1 is Relation-like NAT -defined VG1 -valued Function-like one-to-one onto FinSequence-like FinSequence of VG1

(canFS VG1) * PMST is Relation-like NAT -defined Function-like V50() V51() V52() set

EG1 is Relation-like NAT -defined REAL -valued Function-like FinSequence-like V50() V51() V52() FinSequence of REAL

Sum EG1 is V21() real ext-real Element of REAL

K168() is Relation-like [:REAL,REAL:] -defined REAL -valued Function-like quasi_total V50() V51() V52() Element of bool [:[:REAL,REAL:],REAL:]

K221(REAL,EG1,K168()) is V21() real ext-real Element of REAL

(canFS VG1) * G2 is Relation-like NAT -defined Function-like V50() V51() V52() set

WG1 is Relation-like NAT -defined REAL -valued Function-like FinSequence-like V50() V51() V52() FinSequence of REAL

Sum WG1 is V21() real ext-real Element of REAL

K221(REAL,WG1,K168()) is V21() real ext-real Element of REAL

proj2 (canFS VG1) is set

dom EG1 is Element of bool NAT

dom (canFS VG1) is Element of bool NAT

PCS is V21() epsilon-transitive epsilon-connected ordinal natural real V30() finite cardinal ext-real non negative set

len EG1 is V21() epsilon-transitive epsilon-connected ordinal natural real V30() finite cardinal ext-real non negative Element of NAT

Seg (len EG1) is Element of bool NAT

(canFS VG1) . PCS is set

EG1 . PCS is V21() real ext-real Element of REAL

PMST . ((canFS VG1) . PCS) is V21() real ext-real Element of REAL

WG1 . PCS is V21() real ext-real Element of REAL

G2 . ((canFS VG1) . PCS) is V21() real ext-real Element of REAL

dom WG1 is Element of bool NAT

len WG1 is V21() epsilon-transitive epsilon-connected ordinal natural real V30() finite cardinal ext-real non negative Element of NAT

(len EG1) -tuples_on REAL is FinSequenceSet of REAL

(len WG1) -tuples_on REAL is FinSequenceSet of REAL

G1 is set

PMST is Relation-like G1 -defined Function-like total V50() V51() V52() finite-support set

G2 is Relation-like G1 -defined Function-like total V50() V51() V52() finite-support set

Sum PMST is V21() real ext-real set

Sum G2 is V21() real ext-real set

G29 is set

G2 . G29 is V21() real ext-real Element of REAL

PMST . G29 is V21() real ext-real Element of REAL

G29 is set

PMST . G29 is V21() real ext-real Element of REAL

G2 . G29 is V21() real ext-real Element of REAL

G1 is set

PMST is set

G2 is Relation-like G1 -defined Function-like total V50() V51() V52() finite-support set

Sum G2 is V21() real ext-real set

G29 is Relation-like PMST -defined Function-like total V50() V51() V52() finite-support set

Sum G29 is V21() real ext-real set

support G29 is finite set

canFS (support G29) is Relation-like NAT -defined support G29 -valued Function-like one-to-one onto FinSequence-like FinSequence of support G29

(canFS (support G29)) * G29 is Relation-like NAT -defined Function-like V50() V51() V52() set

VG1 is Relation-like NAT -defined REAL -valued Function-like FinSequence-like V50() V51() V52() FinSequence of REAL

Sum VG1 is V21() real ext-real Element of REAL

K168() is Relation-like [:REAL,REAL:] -defined REAL -valued Function-like quasi_total V50() V51() V52() Element of bool [:[:REAL,REAL:],REAL:]

K221(REAL,VG1,K168()) is V21() real ext-real Element of REAL

G1 is set

EmptyBag G1 is Relation-like G1 -defined RAT -valued Function-like total V50() V51() V52() V53() finite-support Element of Bags G1

Bags G1 is non empty set

Bags G1 is non empty functional Element of bool (Bags G1)

bool (Bags G1) is non empty V101() set

PMST is set

G2 is Relation-like G1 -defined Function-like total V50() V51() V52() finite-support set

Sum G2 is V21() real ext-real set

G29 is V21() real ext-real set

PMST .--> G29 is Relation-like {PMST} -defined Function-like one-to-one finite V50() V51() V52() finite-support set

{PMST} is non empty trivial finite 1 -element set

{PMST} --> G29 is non empty Relation-like {PMST} -defined {G29} -valued Function-like constant total quasi_total finite V50() V51() V52() finite-support Element of bool [:{PMST},{G29}:]

{G29} is non empty trivial finite 1 -element set

[:{PMST},{G29}:] is non empty Relation-like finite set

bool [:{PMST},{G29}:] is non empty finite V40() V101() set

(EmptyBag G1) +* (PMST .--> G29) is Relation-like Function-like V50() V51() V52() set

dom (PMST .--> G29) is trivial finite Element of bool {PMST}

bool {PMST} is non empty finite V40() V101() set

dom G2 is Element of bool G1

bool G1 is non empty set

dom (EmptyBag G1) is Element of bool G1

(dom (EmptyBag G1)) \/ (dom (PMST .--> G29)) is set

support G2 is finite set

VG1 is finite Element of bool G1

EG1 is set

G2 . EG1 is V21() real ext-real Element of REAL

(EmptyBag G1) . EG1 is V21() epsilon-transitive epsilon-connected ordinal natural real V30() V31() finite cardinal ext-real non negative Element of REAL

canFS VG1 is Relation-like NAT -defined VG1 -valued Function-like one-to-one onto FinSequence-like FinSequence of VG1

(canFS VG1) * G2 is Relation-like NAT -defined Function-like V50() V51() V52() set

EG1 is Relation-like NAT -defined REAL -valued Function-like FinSequence-like V50() V51() V52() FinSequence of REAL

Sum EG1 is V21() real ext-real Element of REAL

K168() is Relation-like [:REAL,REAL:] -defined REAL -valued Function-like quasi_total V50() V51() V52() Element of bool [:[:REAL,REAL:],REAL:]

K221(REAL,EG1,K168()) is V21() real ext-real Element of REAL

<*PMST*> is Relation-like Function-like set

G2 . PMST is V21() real ext-real Element of REAL

<*(G2 . PMST)*> is Relation-like NAT -defined REAL -valued Function-like FinSequence-like V50() V51() V52() Element of REAL *

REAL * is FinSequenceSet of REAL

G1 is set

PMST is set

G29 is Relation-like G1 -defined Function-like total V50() V51() V52() finite-support set

G2 is Relation-like G1 -defined Function-like total V50() V51() V52() finite-support set

Sum G29 is V21() real ext-real set

Sum G2 is V21() real ext-real set

G2 . PMST is V21() real ext-real Element of REAL

VG1 is V21() real ext-real set

PMST .--> VG1 is Relation-like {PMST} -defined Function-like one-to-one finite V50() V51() V52() finite-support set

{PMST} is non empty trivial finite 1 -element set

{PMST} --> VG1 is non empty Relation-like {PMST} -defined {VG1} -valued Function-like constant total quasi_total finite V50() V51() V52() finite-support Element of bool [:{PMST},{VG1}:]

{VG1} is non empty trivial finite 1 -element set

[:{PMST},{VG1}:] is non empty Relation-like finite set

bool [:{PMST},{VG1}:] is non empty finite V40() V101() set

G2 +* (PMST .--> VG1) is Relation-like Function-like V50() V51() V52() set

(Sum G2) + VG1 is V21() real ext-real set

((Sum G2) + VG1) - (G2 . PMST) is V21() real ext-real set

dom (PMST .--> VG1) is trivial finite Element of bool {PMST}

bool {PMST} is non empty finite V40() V101() set

dom G29 is Element of bool G1

bool G1 is non empty set

dom G2 is Element of bool G1

(dom G2) \/ (dom (PMST .--> VG1)) is set

EmptyBag G1 is Relation-like G1 -defined RAT -valued Function-like total V50() V51() V52() V53() finite-support Element of Bags G1

Bags G1 is non empty set

Bags G1 is non empty functional Element of bool (Bags G1)

bool (Bags G1) is non empty V101() set

(EmptyBag G1) +* (PMST .--> VG1) is Relation-like Function-like V50() V51() V52() set

proj1 ((EmptyBag G1) +* (PMST .--> VG1)) is set

dom (EmptyBag G1) is Element of bool G1

(dom (EmptyBag G1)) \/ (dom (PMST .--> VG1)) is set

G1 \/ (dom (PMST .--> VG1)) is set

G1 \/ {PMST} is non empty set

PMST .--> 0 is Relation-like {PMST} -defined NAT -valued RAT -valued INT -valued Function-like one-to-one finite V50() V51() V52() V53() Function-yielding V99() finite-support set

{PMST} --> 0 is non empty Relation-like {PMST} -defined NAT -valued RAT -valued INT -valued {0} -valued Function-like constant total quasi_total finite V50() V51() V52() V53() Function-yielding V99() finite-support Element of bool [:{PMST},{0}:]

{0} is non empty trivial functional finite V40() 1 -element set

[:{PMST},{0}:] is non empty Relation-like finite set

bool [:{PMST},{0}:] is non empty finite V40() V101() set

G2 +* (PMST .--> 0) is Relation-like Function-like V50() V51() V52() set

proj1 (G2 +* (PMST .--> 0)) is set

dom (PMST .--> 0) is trivial finite Element of bool {PMST}

(dom G2) \/ (dom (PMST .--> 0)) is set

G1 \/ (dom (PMST .--> 0)) is set

PMST .--> (G2 . PMST) is Relation-like {PMST} -defined REAL -valued Function-like one-to-one finite V50() V51() V52() finite-support set

{PMST} --> (G2 . PMST) is non empty Relation-like {PMST} -defined REAL -valued {(G2 . PMST)} -valued Function-like constant total quasi_total finite V50() V51() V52() finite-support Element of bool [:{PMST},{(G2 . PMST)}:]

{(G2 . PMST)} is non empty trivial finite 1 -element set

[:{PMST},{(G2 . PMST)}:] is non empty Relation-like finite set

bool [:{PMST},{(G2 . PMST)}:] is non empty finite V40() V101() set

(EmptyBag G1) +* (PMST .--> (G2 . PMST)) is Relation-like Function-like V50() V51() V52() set

proj1 ((EmptyBag G1) +* (PMST .--> (G2 . PMST))) is set

dom (PMST .--> (G2 . PMST)) is trivial finite Element of bool {PMST}

(dom (EmptyBag G1)) \/ (dom (PMST .--> (G2 . PMST))) is set

G1 \/ (dom (PMST .--> (G2 . PMST))) is set

support ((EmptyBag G1) +* (PMST .--> (G2 . PMST))) is set

support (EmptyBag G1) is finite set

(support (EmptyBag G1)) \/ {PMST} is non empty finite set

support (G2 +* (PMST .--> 0)) is set

support G2 is finite set

(support G2) \/ {PMST} is non empty finite set

support ((EmptyBag G1) +* (PMST .--> VG1)) is set

M is set

(EmptyBag G1) . M is V21() epsilon-transitive epsilon-connected ordinal natural real V30() V31() finite cardinal ext-real non negative Element of REAL

X is Relation-like G1 -defined Function-like total V50() V51() V52() finite-support set

X is Relation-like G1 -defined Function-like total V50() V51() V52() finite-support set

X + X is Relation-like G1 -defined Function-like total set

(X + X) . M is set

X . M is V21() real ext-real Element of REAL

X . M is V21() real ext-real Element of REAL

(X . M) + (X . M) is V21() real ext-real set

0 + (X . M) is V21() real ext-real set

G2 . M is V21() real ext-real Element of REAL

X is Relation-like G1 -defined Function-like total V50() V51() V52() finite-support set

X is Relation-like G1 -defined Function-like total V50() V51() V52() finite-support set

X + X is Relation-like G1 -defined Function-like total set

(X + X) . M is set

X . M is V21() real ext-real Element of REAL

X . M is V21() real ext-real Element of REAL

(X . M) + (X . M) is V21() real ext-real set

G2 . M is V21() real ext-real Element of REAL

(G2 . M) + (X . M) is V21() real ext-real set

(G2 . M) + 0 is V21() real ext-real set

X is Relation-like G1 -defined Function-like total V50() V51() V52() finite-support set

X is Relation-like G1 -defined Function-like total V50() V51() V52() finite-support set

X + X is Relation-like G1 -defined Function-like total set

X is Relation-like G1 -defined Function-like total V50() V51() V52() finite-support set

X is Relation-like G1 -defined Function-like total V50() V51() V52() finite-support set

X + X is Relation-like G1 -defined Function-like total set

Sum X is V21() real ext-real set

(Sum G2) - (Sum X) is V21() real ext-real set

Sum X is V21() real ext-real set

(Sum X) + (Sum X) is V21() real ext-real set

((Sum X) + (Sum X)) - (Sum X) is V21() real ext-real set

X is Relation-like G1 -defined Function-like total V50() V51() V52() finite-support set

Sum X is V21() real ext-real set

M is set

(EmptyBag G1) . M is V21() epsilon-transitive epsilon-connected ordinal natural real V30() V31() finite cardinal ext-real non negative Element of REAL

G29 . M is V21() real ext-real Element of REAL

X . M is V21() real ext-real Element of REAL

0 + (X . M) is V21() real ext-real set

X . M is V21() real ext-real Element of REAL

(X . M) + (X . M) is V21() real ext-real set

X + X is Relation-like G1 -defined Function-like total set

(X + X) . M is set

X . M is V21() real ext-real Element of REAL

G29 . M is V21() real ext-real Element of REAL

G2 . M is V21() real ext-real Element of REAL

X . M is V21() real ext-real Element of REAL

(X . M) + (X . M) is V21() real ext-real set

X + X is Relation-like G1 -defined Function-like total set

(X + X) . M is set

X + X is Relation-like G1 -defined Function-like total set

X + X is Relation-like G1 -defined Function-like total set

((Sum G2) - (Sum X)) + (Sum X) is V21() real ext-real set

G1 is Relation-like NAT -defined Function-like finite finite-support [Graph-like] [Weighted] real-weighted set

G1 is Relation-like NAT -defined Function-like finite finite-support [Graph-like] [Weighted] real-weighted set

the_Vertices_of G1 is non empty set

G1 . VertexSelector is set

the_Edges_of G1 is set

G1 . EdgeSelector is set

(the_Vertices_of G1) \/ (the_Edges_of G1) is non empty set

G1 is Relation-like NAT -defined Function-like finite finite-support [Graph-like] finite [Weighted] real-weighted set

the_Vertices_of G1 is non empty finite set

G1 . VertexSelector is set

the_Edges_of G1 is finite set

G1 . EdgeSelector is set

(the_Vertices_of G1) \/ (the_Edges_of G1) is non empty finite set

PMST is set

G2 is set

{ b

VG1 is set

{ b

EG1 is Relation-like NAT -defined (the_Vertices_of G1) \/ (the_Edges_of G1) -valued Function-like FinSequence-like directed Trail-like Path-like Walk of G1

G1 .allDPaths() is non empty finite Element of bool (G1 .allDTrails())

G1 .allDTrails() is non empty finite Element of bool (G1 .allTrails())

G1 .allTrails() is non empty finite Element of bool (G1 .allWalks())

G1 .allWalks() is non empty Element of bool (((the_Vertices_of G1) \/ (the_Edges_of G1)) *)

((the_Vertices_of G1) \/ (the_Edges_of G1)) * is set

bool (((the_Vertices_of G1) \/ (the_Edges_of G1)) *) is non empty set

bool (G1 .allWalks()) is non empty V101() set

bool (G1 .allTrails()) is non empty finite V40() V101() set

bool (G1 .allDTrails()) is non empty finite V40() V101() set

bool (G1 .allDPaths()) is non empty finite V40() V101() set

EG1 is Relation-like NAT -defined (the_Vertices_of G1) \/ (the_Edges_of G1) -valued Function-like FinSequence-like directed Walk of G1

EG1 is Relation-like NAT -defined (the_Vertices_of G1) \/ (the_Edges_of G1) -valued Function-like FinSequence-like directed Walk of G1

the Relation-like NAT -defined (the_Vertices_of G1) \/ (the_Edges_of G1) -valued Function-like FinSequence-like directed Trail-like Path-like Subwalk of EG1 is Relation-like NAT -defined (the_Vertices_of G1) \/ (the_Edges_of G1) -valued Function-like FinSequence-like directed Trail-like Path-like Subwalk of EG1

VG1 is finite Element of bool (G1 .allDPaths())

PCS is non empty finite Element of bool (G1 .allDPaths())

X is Relation-like NAT -defined (the_Vertices_of G1) \/ (the_Edges_of G1) -valued Function-like FinSequence-like directed Trail-like Path-like Element of PCS

X .cost() is V21() real ext-real Element of REAL

X .weightSeq() is Relation-like NAT -defined REAL -valued Function-like FinSequence-like V50() V51() V52() FinSequence of REAL

Sum (X .weightSeq()) is V21() real ext-real Element of REAL

K168() is Relation-like [:REAL,REAL:] -defined REAL -valued Function-like quasi_total V50() V51() V52() Element of bool [:[:REAL,REAL:],REAL:]

K221(REAL,(X .weightSeq()),K168()) is V21() real ext-real Element of REAL

X is Relation-like NAT -defined (the_Vertices_of G1) \/ (the_Edges_of G1) -valued Function-like FinSequence-like directed Trail-like Path-like Walk of G1

X is Relation-like NAT -defined (the_Vertices_of G1) \/ (the_Edges_of G1) -valued Function-like FinSequence-like directed Trail-like Path-like Walk of G1

M is Relation-like NAT -defined (the_Vertices_of G1) \/ (the_Edges_of G1) -valued Function-like FinSequence-like directed Trail-like Path-like Element of PCS

M .cost() is V21() real ext-real Element of REAL

M .weightSeq() is Relation-like NAT -defined REAL -valued Function-like FinSequence-like V50() V51() V52() FinSequence of REAL

Sum (M .weightSeq()) is V21() real ext-real Element of REAL

K221(REAL,(M .weightSeq()),K168()) is V21() real ext-real Element of REAL

X .cost() is V21() real ext-real Element of REAL

X .weightSeq() is Relation-like NAT -defined REAL -valued Function-like FinSequence-like V50() V51() V52() FinSequence of REAL

Sum (X .weightSeq()) is V21() real ext-real Element of REAL

K221(REAL,(X .weightSeq()),K168()) is V21() real ext-real Element of REAL

X .cost() is V21() real ext-real Element of REAL

X .weightSeq() is Relation-like NAT -defined REAL -valued Function-like FinSequence-like V50() V51() V52() FinSequence of REAL

Sum (X .weightSeq()) is V21() real ext-real Element of REAL

K221(REAL,(X .weightSeq()),K168()) is V21() real ext-real Element of REAL

X is Relation-like NAT -defined (the_Vertices_of G1) \/ (the_Edges_of G1) -valued Function-like FinSequence-like directed Trail-like Path-like Walk of G1

X .cost() is V21() real ext-real Element of REAL

X .weightSeq() is Relation-like NAT -defined REAL -valued Function-like FinSequence-like V50() V51() V52() FinSequence of REAL

Sum (X .weightSeq()) is V21() real ext-real Element of REAL

K221(REAL,(X .weightSeq()),K168()) is V21() real ext-real Element of REAL

k is Relation-like NAT -defined (the_Vertices_of G1) \/ (the_Edges_of G1) -valued Function-like FinSequence-like directed Trail-like Path-like Walk of G1

M is V21() real ext-real Element of REAL

k .cost() is V21() real ext-real Element of REAL

k .weightSeq() is Relation-like NAT -defined REAL -valued Function-like FinSequence-like V50() V51() V52() FinSequence of REAL

Sum (k .weightSeq()) is V21() real ext-real Element of REAL

K221(REAL,(k .weightSeq()),K168()) is V21() real ext-real Element of REAL

G29 is V21() real ext-real Element of REAL

VG1 is V21() real ext-real Element of REAL

EG1 is Relation-like NAT -defined (the_Vertices_of G1) \/ (the_Edges_of G1) -valued Function-like FinSequence-like directed Trail-like Path-like Walk of G1

EG1 .cost() is V21() real ext-real Element of REAL

EG1 .weightSeq() is Relation-like NAT -defined REAL -valued Function-like FinSequence-like V50() V51() V52() FinSequence of REAL

Sum (EG1 .weightSeq()) is V21() real ext-real Element of REAL

K168() is Relation-like [:REAL,REAL:] -defined REAL -valued Function-like quasi_total V50() V51() V52() Element of bool [:[:REAL,REAL:],REAL:]

K221(REAL,(EG1 .weightSeq()),K168()) is V21() real ext-real Element of REAL

WG1 is Relation-like NAT -defined (the_Vertices_of G1) \/ (the_Edges_of G1) -valued Function-like FinSequence-like directed Trail-like Path-like Walk of G1

WG1 .cost() is V21() real ext-real Element of REAL

WG1 .weightSeq() is Relation-like NAT -defined REAL -valued Function-like FinSequence-like V50() V51() V52() FinSequence of REAL

Sum (WG1 .weightSeq()) is V21() real ext-real Element of REAL

K221(REAL,(WG1 .weightSeq()),K168()) is V21() real ext-real Element of REAL

{VertexSelector,EdgeSelector,SourceSelector,TargetSelector,WeightSelector} is non empty finite Element of bool NAT

() is non empty finite Element of bool NAT

G1 is Relation-like NAT -defined Function-like finite finite-support [Graph-like] [Weighted] set

dom G1 is finite Element of bool NAT

PMST is set

G1 is Relation-like NAT -defined Function-like finite finite-support [Graph-like] [Weighted] set

G1 | () is Relation-like () -defined NAT -defined Function-like finite finite-support set

the_Target_of (G1 | ()) is set

(G1 | ()) . TargetSelector is set

the_Target_of G1 is Relation-like the_Edges_of G1 -defined the_Vertices_of G1 -valued Function-like quasi_total Element of bool [:(the_Edges_of G1),(the_Vertices_of G1):]

the_Edges_of G1 is set

G1 . EdgeSelector is set

the_Vertices_of G1 is non empty set

G1 . VertexSelector is set

[:(the_Edges_of G1),(the_Vertices_of G1):] is Relation-like set

bool [:(the_Edges_of G1),(the_Vertices_of G1):] is non empty set

G1 . TargetSelector is set

the_Source_of (G1 | ()) is set

(G1 | ()) . SourceSelector is set

the_Source_of G1 is Relation-like the_Edges_of G1 -defined the_Vertices_of G1 -valued Function-like quasi_total Element of bool [:(the_Edges_of G1),(the_Vertices_of G1):]

G1 . SourceSelector is set

the_Edges_of (G1 | ()) is set

(G1 | ()) . EdgeSelector is set

dom (G1 | ()) is finite Element of bool ()

bool () is non empty finite V40() V101() set

dom G1 is finite Element of bool NAT

(dom G1) /\ () is finite Element of bool NAT

G2 is set

the_Vertices_of (G1 | ()) is set

(G1 | ()) . VertexSelector is set

(G1 | ()) . WeightSelector is set

G1 . WeightSelector is set

G1 is Relation-like NAT -defined Function-like finite finite-support [Graph-like] [Weighted] set

G1 | () is Relation-like NAT -defined () -defined NAT -defined Function-like finite finite-support [Graph-like] [Weighted] set

the_Weight_of G1 is Relation-like the_Edges_of G1 -defined Function-like total set

the_Edges_of G1 is set

G1 . EdgeSelector is set

G1 . WeightSelector is set

the_Weight_of (G1 | ()) is Relation-like the_Edges_of (G1 | ()) -defined Function-like total set

the_Edges_of (G1 | ()) is set

(G1 | ()) . EdgeSelector is set

(G1 | ()) . WeightSelector is set

the_Vertices_of (G1 | ()) is non empty set

(G1 | ()) . VertexSelector is set

the_Vertices_of G1 is non empty set

G1 . VertexSelector is set

the_Source_of (G1 | ()) is Relation-like the_Edges_of (G1 | ()) -defined the_Vertices_of (G1 | ()) -valued Function-like quasi_total Element of bool [:(the_Edges_of (G1 | ())),(the_Vertices_of (G1 | ())):]

[:(the_Edges_of (G1 | ())),(the_Vertices_of (G1 | ())):] is Relation-like set

bool [:(the_Edges_of (G1 | ())),(the_Vertices_of (G1 | ())):] is non empty set

(G1 | ()) . SourceSelector is set

the_Source_of G1 is Relation-like the_Edges_of G1 -defined the_Vertices_of G1 -valued Function-like quasi_total Element of bool [:(the_Edges_of G1),(the_Vertices_of G1):]

[:(the_Edges_of G1),(the_Vertices_of G1):] is Relation-like set

bool [:(the_Edges_of G1),(the_Vertices_of G1):] is non empty set

G1 . SourceSelector is set

the_Target_of (G1 | ()) is Relation-like the_Edges_of (G1 | ()) -defined the_Vertices_of (G1 | ()) -valued Function-like quasi_total Element of bool [:(the_Edges_of (G1 | ())),(the_Vertices_of (G1 | ())):]

(G1 | ()) . TargetSelector is set

the_Target_of G1 is Relation-like the_Edges_of G1 -defined the_Vertices_of G1 -valued Function-like quasi_total Element of bool [:(the_Edges_of G1),(the_Vertices_of G1):]

G1 . TargetSelector is set

G1 is Relation-like NAT -defined Function-like finite finite-support [Graph-like] [Weighted] set

G1 | () is Relation-like NAT -defined () -defined NAT -defined Function-like finite finite-support [Graph-like] [Weighted] set

dom (G1 | ()) is finite Element of bool ()

bool () is non empty finite V40() V101() set

dom G1 is finite Element of bool NAT

G1 is Relation-like NAT -defined Function-like finite finite-support [Graph-like] [Weighted] set

G1 | () is Relation-like NAT -defined () -defined NAT -defined Function-like finite finite-support [Graph-like] [Weighted] set

the_Weight_of G1 is Relation-like the_Edges_of G1 -defined Function-like total set

the_Edges_of G1 is set

G1 . EdgeSelector is set

G1 . WeightSelector is set

the_Weight_of (G1 | ()) is Relation-like the_Edges_of (G1 | ()) -defined Function-like total set

the_Edges_of (G1 | ()) is set

(G1 | ()) . EdgeSelector is set

(G1 | ()) . WeightSelector is set

dom (the_Weight_of G1) is Element of bool (the_Edges_of G1)

bool (the_Edges_of G1) is non empty set

G2 is Relation-like NAT -defined Function-like finite finite-support [Graph-like] [Weighted] Subgraph of G1

the_Edges_of G2 is Element of bool (the_Edges_of G1)

G2 . EdgeSelector is set

the_Weight_of G2 is Relation-like the_Edges_of G2 -defined Function-like total set

the_Edges_of G2 is set

G2 . WeightSelector is set

(the_Weight_of G1) | (the_Edges_of G2) is Relation-like the_Edges_of G2 -defined the_Edges_of G1 -defined Function-like set

the_Vertices_of G1 is non empty set

G1 . VertexSelector is set

bool (the_Vertices_of G1) is non empty V101() set

the_Source_of G1 is Relation-like the_Edges_of G1 -defined the_Vertices_of G1 -valued Function-like quasi_total Element of bool [:(the_Edges_of G1),(the_Vertices_of G1):]

[:(the_Edges_of G1),(the_Vertices_of G1):] is Relation-like set

bool [:(the_Edges_of G1),(the_Vertices_of G1):] is non empty set

G1 . SourceSelector is set

bool (the_Source_of G1) is non empty set

the_Target_of G1 is Relation-like the_Edges_of G1 -defined the_Vertices_of G1 -valued Function-like quasi_total Element of bool [:(the_Edges_of G1),(the_Vertices_of G1):]

G1 . TargetSelector is set

bool (the_Target_of G1) is non empty set

bool (the_Weight_of G1) is non empty set

{(bool (the_Vertices_of G1)),(bool (the_Edges_of G1)),(bool (the_Source_of G1)),(bool (the_Target_of G1)),(bool (the_Weight_of G1))} is non empty finite set

union {(bool (the_Vertices_of G1)),(bool (the_Edges_of G1)),(bool (the_Source_of G1)),(bool (the_Target_of G1)),(bool (the_Weight_of G1))} is set

Funcs ((),(union {(bool (the_Vertices_of G1)),(bool (the_Edges_of G1)),(bool (the_Source_of G1)),(bool (the_Target_of G1)),(bool (the_Weight_of G1))})) is set

bool (Funcs ((),(union {(bool (the_Vertices_of G1)),(bool (the_Edges_of G1)),(bool (the_Source_of G1)),(bool (the_Target_of G1)),(bool (the_Weight_of G1))}))) is non empty set

PCS is Element of bool (Funcs ((),(union {(bool (the_Vertices_of G1)),(bool (the_Edges_of G1)),(bool (the_Source_of G1)),(bool (the_Target_of G1)),(bool (the_Weight_of G1))})))

X is Relation-like NAT -defined Function-like finite finite-support [Graph-like] [Weighted] weight-inheriting Subgraph of G1

dom X is finite Element of bool NAT

X is set

proj2 X is finite set

X is set

X . X is set

the_Vertices_of X is non empty Element of bool (the_Vertices_of G1)

X . VertexSelector is set

the_Edges_of X is Element of bool (the_Edges_of G1)

X . EdgeSelector is set

the_Source_of X is Relation-like the_Edges_of X -defined the_Vertices_of X -valued Function-like quasi_total Element of bool [:(the_Edges_of X),(the_Vertices_of X):]

the_Edges_of X is set

X . EdgeSelector is set

the_Vertices_of X is non empty set

X . VertexSelector is set

[:(the_Edges_of X),(the_Vertices_of X):] is Relation-like set

bool [:(the_Edges_of X),(the_Vertices_of X):] is non empty set

X . SourceSelector is set

the_Edges_of X is Element of bool (the_Edges_of G1)

(the_Source_of G1) | (the_Edges_of X) is Relation-like the_Edges_of G1 -defined the_Edges_of X -defined the_Edges_of G1 -defined the_Vertices_of G1 -valued Function-like Element of bool [:(the_Edges_of G1),(the_Vertices_of G1):]

the_Target_of X is Relation-like the_Edges_of X -defined the_Vertices_of X -valued Function-like quasi_total Element of bool [:(the_Edges_of X),(the_Vertices_of X):]

the_Edges_of X is set

X . EdgeSelector is set

the_Vertices_of X is non empty set

X . VertexSelector is set

[:(the_Edges_of X),(the_Vertices_of X):] is Relation-like set

bool [:(the_Edges_of X),(the_Vertices_of X):] is non empty set

X . TargetSelector is set

the_Edges_of X is Element of bool (the_Edges_of G1)

(the_Target_of G1) | (the_Edges_of X) is Relation-like the_Edges_of G1 -defined the_Edges_of X -defined the_Edges_of G1 -defined the_Vertices_of G1 -valued Function-like Element of bool [:(the_Edges_of G1),(the_Vertices_of G1):]

the_Weight_of X is Relation-like the_Edges_of X -defined Function-like total set

the_Edges_of X is set

X . EdgeSelector is set

X . WeightSelector is set

the_Edges_of X is Element of bool (the_Edges_of G1)

(the_Weight_of G1) | (the_Edges_of X) is Relation-like the_Edges_of X -defined the_Edges_of G1 -defined Function-like set

G29 is Relation-like NAT -defined Function-like finite finite-support [Graph-like] [Weighted] weight-inheriting Subgraph of G1

dom G29 is finite Element of bool NAT

proj2 G29 is finite set

X is non empty set

X is set

X is Relation-like NAT -defined Function-like finite finite-support [Graph-like] [Weighted] weight-inheriting Subgraph of G1

M is Relation-like NAT -defined Function-like finite finite-support [Graph-like] [Weighted] weight-inheriting Subgraph of G1

dom M is finite Element of bool NAT

M is Relation-like Function-like set

proj1 M is set

proj2 M is set

X is Relation-like NAT -defined Function-like finite finite-support [Graph-like] [Weighted] weight-inheriting Subgraph of G1

dom X is finite Element of bool NAT

proj2 X is finite set

PMST is non empty set

G2 is non empty set

G29 is set

VG1 is Relation-like NAT -defined Function-like finite finite-support [Graph-like] [Weighted] weight-inheriting Subgraph of G1

dom VG1 is finite Element of bool NAT

VG1 is Relation-like NAT -defined Function-like finite finite-support [Graph-like] [Weighted] weight-inheriting Subgraph of G1

dom VG1 is finite Element of bool NAT

G1 is Relation-like NAT -defined Function-like finite finite-support [Graph-like] finite [Weighted] set

(G1) is non empty set

the_Vertices_of G1 is non empty finite set

G1 . VertexSelector is set

bool (the_Vertices_of G1) is non empty finite V40() V101() set

the_Edges_of G1 is finite set

G1 . EdgeSelector is set

bool (the_Edges_of G1) is non empty finite V40() set

the_Source_of G1 is Relation-like the_Edges_of G1 -defined the_Vertices_of G1 -valued Function-like quasi_total finite finite-support Element of bool [:(the_Edges_of G1),(the_Vertices_of G1):]

[:(the_Edges_of G1),(the_Vertices_of G1):] is Relation-like finite set

bool [:(the_Edges_of G1),(the_Vertices_of G1):] is non empty finite V40() set

G1 . SourceSelector is set

bool (the_Source_of G1) is non empty finite V40() set

the_Target_of G1 is Relation-like the_Edges_of G1 -defined the_Vertices_of G1 -valued Function-like quasi_total finite finite-support Element of bool [:(the_Edges_of G1),(the_Vertices_of G1):]

G1 . TargetSelector is set

bool (the_Target_of G1) is non empty finite V40() set

the_Weight_of G1 is Relation-like the_Edges_of G1 -defined Function-like total finite finite-support set

G1 . WeightSelector is set

bool (the_Weight_of G1) is non empty finite V40() set

{(bool (the_Vertices_of G1)),(bool (the_Edges_of G1)),(bool (the_Source_of G1)),(bool (the_Target_of G1)),(bool (the_Weight_of G1))} is non empty finite set

union {(bool (the_Vertices_of G1)),(bool (the_Edges_of G1)),(bool (the_Source_of G1)),(bool (the_Target_of G1)),(bool (the_Weight_of G1))} is set

G29 is set

G29 is finite set

Funcs ((),G29) is finite set

EG1 is set

WG1 is Relation-like NAT -defined Function-like finite finite-support [Graph-like] finite [Weighted] weight-inheriting Subgraph of G1

dom WG1 is finite Element of bool NAT

PCS is set

proj2 WG1 is finite set

X is set

WG1 . X is set

the_Vertices_of WG1 is non empty finite Element of bool (the_Vertices_of G1)

WG1 . VertexSelector is set

the_Edges_of WG1 is finite Element of bool (the_Edges_of G1)

WG1 . EdgeSelector is set

the_Source_of WG1 is Relation-like the_Edges_of WG1 -defined the_Vertices_of WG1 -valued Function-like quasi_total finite finite-support Element of bool [:(the_Edges_of WG1),(the_Vertices_of WG1):]

the_Edges_of WG1 is finite set

WG1 . EdgeSelector is set

the_Vertices_of WG1 is non empty finite set

WG1 . VertexSelector is set

[:(the_Edges_of WG1),(the_Vertices_of WG1):] is Relation-like finite set

bool [:(the_Edges_of WG1),(the_Vertices_of WG1):] is non empty finite V40() set

WG1 . SourceSelector is set

the_Edges_of WG1 is finite Element of bool (the_Edges_of G1)

(the_Source_of G1) | (the_Edges_of WG1) is Relation-like the_Edges_of G1 -defined the_Edges_of WG1 -defined the_Edges_of G1 -defined the_Vertices_of G1 -valued Function-like finite finite-support Element of bool [:(the_Edges_of G1),(the_Vertices_of G1):]

the_Target_of WG1 is Relation-like the_Edges_of WG1 -defined the_Vertices_of WG1 -valued Function-like quasi_total finite finite-support Element of bool [:(the_Edges_of WG1),(the_Vertices_of WG1):]

the_Edges_of WG1 is finite set

WG1 . EdgeSelector is set

the_Vertices_of WG1 is non empty finite set

WG1 . VertexSelector is set

[:(the_Edges_of WG1),(the_Vertices_of WG1):] is Relation-like finite set

bool [:(the_Edges_of WG1),(the_Vertices_of WG1):] is non empty finite V40() set

WG1 . TargetSelector is set

the_Edges_of WG1 is finite Element of bool (the_Edges_of G1)

(the_Target_of G1) | (the_Edges_of WG1) is Relation-like the_Edges_of G1 -defined the_Edges_of WG1 -defined the_Edges_of G1 -defined the_Vertices_of G1 -valued Function-like finite finite-support Element of bool [:(the_Edges_of G1),(the_Vertices_of G1):]

the_Weight_of WG1 is Relation-like the_Edges_of WG1 -defined Function-like total finite finite-support set

the_Edges_of WG1 is finite set

WG1 . EdgeSelector is set

WG1 . WeightSelector is set

the_Edges_of WG1 is finite Element of bool (the_Edges_of G1)

(the_Weight_of G1) | (the_Edges_of WG1) is Relation-like the_Edges_of WG1 -defined the_Edges_of G1 -defined Function-like finite finite-support set

G1 is Relation-like NAT -defined Function-like finite finite-support [Graph-like] [Weighted] set

(G1) is non empty set

bool (G1) is non empty V101() set

PMST is non empty Element of bool (G1)

G2 is Element of PMST

G29 is Relation-like NAT -defined Function-like finite finite-support [Graph-like] [Weighted] weight-inheriting Subgraph of G1

dom G29 is finite Element of bool NAT

G1 is Relation-like NAT -defined Function-like finite finite-support [Graph-like] finite [Weighted] real-weighted set

the_Edges_of G1 is finite set

G1 . EdgeSelector is set

the_Weight_of G1 is Relation-like the_Edges_of G1 -defined Function-like total finite V50() V51() V52() finite-support set

G1 . WeightSelector is set

Sum (the_Weight_of G1) is V21() real ext-real set

G1 is Relation-like NAT -defined Function-like finite finite-support [Graph-like] finite [Weighted] real-weighted set

the_Vertices_of G1 is non empty finite set

G1 . VertexSelector is set

the_Edges_of G1 is finite set

G1 . EdgeSelector is set

(G1) is V21() real ext-real Element of REAL

the_Weight_of G1 is Relation-like the_Edges_of G1 -defined Function-like total finite V50() V51() V52() finite-support set

G1 . WeightSelector is set

Sum (the_Weight_of G1) is V21() real ext-real set

PMST is set

{PMST} is non empty trivial finite 1 -element set

(the_Edges_of G1) \ {PMST} is finite Element of bool (the_Edges_of G1)

bool (the_Edges_of G1) is non empty finite V40() set

(the_Weight_of G1) . PMST is V21() real ext-real Element of REAL

G2 is Relation-like NAT -defined Function-like finite finite-support [Graph-like] finite spanning [Weighted] weight-inheriting real-weighted inducedSubgraph of G1, the_Vertices_of G1,(the_Edges_of G1) \ {PMST}

(G2) is V21() real ext-real Element of REAL

the_Edges_of G2 is finite set

G2 . EdgeSelector is set

the_Weight_of G2 is Relation-like the_Edges_of G2 -defined Function-like total finite V50() V51() V52() finite-support set

G2 . WeightSelector is set

Sum (the_Weight_of G2) is V21() real ext-real set

(G2) + ((the_Weight_of G1) . PMST) is V21() real ext-real set

the_Edges_of G2 is finite Element of bool (the_Edges_of G1)

dom (the_Weight_of G1) is finite Element of bool (the_Edges_of G1)

PMST .--> ((the_Weight_of G1) . PMST) is Relation-like {PMST} -defined REAL -valued Function-like one-to-one finite V50() V51() V52() finite-support set

{PMST} --> ((the_Weight_of G1) . PMST) is non empty Relation-like {PMST} -defined REAL -valued {((the_Weight_of G1) . PMST)} -valued Function-like constant total quasi_total finite V50() V51() V52() finite-support Element of bool [:{PMST},{((the_Weight_of G1) . PMST)}:]

{((the_Weight_of G1) . PMST)} is non empty trivial finite 1 -element set

[:{PMST},{((the_Weight_of G1) . PMST)}:] is non empty Relation-like finite set

bool [:{PMST},{((the_Weight_of G1) . PMST)}:] is non empty finite V40() V101() set

dom (PMST .--> ((the_Weight_of G1) . PMST)) is trivial finite Element of bool {PMST}

bool {PMST} is non empty finite V40() V101() set

(the_Edges_of G1) \ (the_Edges_of G2) is finite Element of bool (the_Edges_of G1)

(the_Edges_of G1) /\ {PMST} is finite set

WG1 is Relation-like (the_Edges_of G1) \ (the_Edges_of G2) -defined Function-like total finite-support set

(the_Weight_of G1) | (the_Edges_of G2) is Relation-like the_Edges_of G2 -defined the_Edges_of G1 -defined Function-like finite V50() V51() V52() finite-support set

X is set

PCS is Relation-like (the_Edges_of G1) \ (the_Edges_of G2) -defined Function-like total V50() V51() V52() finite-support set

(the_Weight_of G2) +* PCS is Relation-like Function-like V50() V51() V52() set

((the_Weight_of G2) +* PCS) . X is V21() real ext-real Element of REAL

PCS . PMST is V21() real ext-real Element of REAL

(the_Weight_of G1) . X is V21() real ext-real Element of REAL

PCS is Relation-like (the_Edges_of G1) \ (the_Edges_of G2) -defined Function-like total V50() V51() V52() finite-support set

(the_Weight_of G2) +* PCS is Relation-like Function-like V50() V51() V52() set

((the_Weight_of G2) +* PCS) . X is V21() real ext-real Element of REAL

(the_Weight_of G2) . X is V21() real ext-real Element of REAL

(the_Weight_of G1) . X is V21() real ext-real Element of REAL

PCS is Relation-like (the_Edges_of G1) \ (the_Edges_of G2) -defined Function-like total V50() V51() V52() finite-support set

(the_Weight_of G2) +* PCS is Relation-like Function-like V50() V51() V52() set

((the_Weight_of G2) +* PCS) . X is V21() real ext-real Element of REAL

(the_Weight_of G1) . X is V21() real ext-real Element of REAL

PCS is Relation-like (the_Edges_of G1) \ (the_Edges_of G2) -defined Function-like total V50() V51() V52() finite-support set

(the_Weight_of G2) +* PCS is Relation-like Function-like V50() V51() V52() set

((the_Weight_of G2) +* PCS) . X is V21() real ext-real Element of REAL

(the_Weight_of G1) . X is V21() real ext-real Element of REAL

proj1 ((the_Weight_of G2) +* PCS) is set

dom (the_Weight_of G2) is finite Element of bool (the_Edges_of G2)

bool (the_Edges_of G2) is non empty finite V40() set

(dom (the_Weight_of G2)) \/ {PMST} is non empty finite set

((the_Edges_of G1) \ {PMST}) \/ {PMST} is non empty finite set

(the_Edges_of G1) \/ {PMST} is non empty finite set

Sum PCS is V21() real ext-real set

(G2) + (Sum PCS) is V21() real ext-real set

PCS . PMST is V21() real ext-real Element of REAL

(G2) + (PCS . PMST) is V21() real ext-real set

G1 is Relation-like NAT -defined Function-like finite finite-support [Graph-like] finite [Weighted] real-weighted set

the_Vertices_of G1 is non empty finite set

G1 . VertexSelector is set

bool (the_Vertices_of G1) is non empty finite V40() V101() set

the_Weight_of G1 is Relation-like the_Edges_of G1 -defined Function-like total finite V50() V51() V52() finite-support set

the_Edges_of G1 is finite set

G1 . EdgeSelector is set

G1 . WeightSelector is set

PMST is non empty finite Element of bool (the_Vertices_of G1)

G1 .edgesBetween PMST is finite Element of bool (the_Edges_of G1)

bool (the_Edges_of G1) is non empty finite V40() set

G1 .edgesInto PMST is finite Element of bool (the_Edges_of G1)

G1 .edgesOutOf PMST is finite Element of bool (the_Edges_of G1)

(G1 .edgesInto PMST) /\ (G1 .edgesOutOf PMST) is finite Element of bool (the_Edges_of G1)

bool (G1 .edgesBetween PMST) is non empty finite V40() set

G2 is finite Element of bool (G1 .edgesBetween PMST)

G29 is Relation-like NAT -defined Function-like finite finite-support [Graph-like] finite [Weighted] weight-inheriting real-weighted inducedSubgraph of G1,PMST,G2

(G29) is V21() real ext-real Element of REAL

the_Edges_of G29 is finite set

G29 . EdgeSelector is set

the_Weight_of G29 is Relation-like the_Edges_of G29 -defined Function-like total finite V50() V51() V52() finite-support set

G29 . WeightSelector is set

Sum (the_Weight_of G29) is V21() real ext-real set

VG1 is set

{VG1} is non empty trivial finite 1 -element set

G2 \/ {VG1} is non empty finite set

(the_Weight_of G1) . VG1 is V21() real ext-real Element of REAL

(G29) + ((the_Weight_of G1) . VG1) is V21() real ext-real set

EG1 is Relation-like NAT -defined Function-like finite finite-support [Graph-like] finite [Weighted] weight-inheriting real-weighted inducedSubgraph of G1,PMST,G2 \/ {VG1}

(EG1) is V21() real ext-real Element of REAL

the_Edges_of EG1 is finite set

EG1 . EdgeSelector is set

the_Weight_of EG1 is Relation-like the_Edges_of EG1 -defined Function-like total finite V50() V51() V52() finite-support set

EG1 . WeightSelector is set

Sum (the_Weight_of EG1) is V21() real ext-real set

the_Edges_of EG1 is finite Element of bool (the_Edges_of G1)

dom (the_Weight_of EG1) is finite Element of bool (the_Edges_of EG1)

bool (the_Edges_of EG1) is non empty finite V40() set

VG1 .--> ((the_Weight_of G1) . VG1) is Relation-like {VG1} -defined REAL -valued Function-like one-to-one finite V50() V51() V52() finite-support set

{VG1} --> ((the_Weight_of G1) . VG1) is non empty Relation-like {VG1} -defined REAL -valued {((the_Weight_of G1) . VG1)} -valued Function-like constant total quasi_total finite V50() V51() V52() finite-support Element of bool [:{VG1},{((the_Weight_of G1) . VG1)}:]

{((the_Weight_of G1) . VG1)} is non empty trivial finite 1 -element set

[:{VG1},{((the_Weight_of G1) . VG1)}:] is non empty Relation-like finite set

bool [:{VG1},{((the_Weight_of G1) . VG1)}:] is non empty finite V40() V101() set

dom (VG1 .--> ((the_Weight_of G1) . VG1)) is trivial finite Element of bool {VG1}

bool {VG1} is non empty finite V40() V101() set

the_Edges_of G29 is finite Element of bool (the_Edges_of G1)

(the_Edges_of EG1) \ (the_Edges_of G29) is finite Element of bool (the_Edges_of G1)

{VG1} \ G2 is trivial finite Element of bool {VG1}

PCS is Relation-like (the_Edges_of EG1) \ (the_Edges_of G29) -defined Function-like total finite-support set

(the_Weight_of G1) | G2 is Relation-like G2 -defined the_Edges_of G1 -defined Function-like finite V50() V51() V52() finite-support set

X is set

(the_Weight_of G1) | (G2 \/ {VG1}) is Relation-like G2 \/ {VG1} -defined the_Edges_of G1 -defined Function-like finite V50() V51() V52() finite-support set

(the_Weight_of EG1) . X is V21() real ext-real Element of REAL

(the_Weight_of G1) . X is V21() real ext-real Element of REAL

X is Relation-like (the_Edges_of EG1) \ (the_Edges_of G29) -defined Function-like total V50() V51() V52() finite-support set

dom X is finite Element of bool ((the_Edges_of EG1) \ (the_Edges_of G29))

bool ((the_Edges_of EG1) \ (the_Edges_of G29)) is non empty finite V40() set

(the_Weight_of G29) +* X is Relation-like Function-like V50() V51() V52() set

((the_Weight_of G29) +* X) . X is V21() real ext-real Element of REAL

(the_Weight_of G29) . X is V21() real ext-real Element of REAL

X is Relation-like (the_Edges_of EG1) \ (the_Edges_of G29) -defined Function-like total V50() V51() V52() finite-support set

dom X is finite Element of bool ((the_Edges_of EG1) \ (the_Edges_of G29))

bool ((the_Edges_of EG1) \ (the_Edges_of G29)) is non empty finite V40() set

(the_Weight_of G29) +* X is Relation-like Function-like V50() V51() V52() set

((the_Weight_of G29) +* X) . X is V21() real ext-real Element of REAL

X . X is V21() real ext-real Element of REAL

X is Relation-like (the_Edges_of EG1) \ (the_Edges_of G29) -defined Function-like total V50() V51() V52() finite-support set

dom X is finite Element of bool ((the_Edges_of EG1) \ (the_Edges_of G29))

bool ((the_Edges_of EG1) \ (the_Edges_of G29)) is non empty finite V40() set

(the_Weight_of G29) +* X is Relation-like Function-like V50() V51() V52() set

((the_Weight_of G29) +* X) . X is V21() real ext-real Element of REAL

X is Relation-like (the_Edges_of EG1) \ (the_Edges_of G29) -defined Function-like total V50() V51() V52() finite-support set

(the_Weight_of G29) +* X is Relation-like Function-like V50() V51() V52() set

((the_Weight_of G29) +* X) . X is V21() real ext-real Element of REAL

dom X is finite Element of bool ((the_Edges_of EG1) \ (the_Edges_of G29))

bool ((the_Edges_of EG1) \ (the_Edges_of G29)) is non empty finite V40() set

Sum X is V21() real ext-real set

X . VG1 is V21() real ext-real Element of REAL

proj1 ((the_Weight_of G29) +* X) is set

dom (the_Weight_of G29) is finite Element of bool (the_Edges_of G29)

bool (the_Edges_of G29) is non empty finite V40() set

(dom (the_Weight_of G29)) \/ (dom X) is finite set

G1 is Relation-like NAT -defined Function-like finite finite-support [Graph-like] finite [Weighted] real-weighted nonnegative-weighted set

the_Vertices_of G1 is non empty finite set

G1 . VertexSelector is set

the_Edges_of G1 is finite set

G1 . EdgeSelector is set

(the_Vertices_of G1) \/ (the_Edges_of G1) is non empty finite set

PMST is Relation-like NAT -defined (the_Vertices_of G1) \/ (the_Edges_of G1) -valued Function-like FinSequence-like directed Trail-like Path-like Walk of G1

G2 is set

G29 is set

VG1 is V21() epsilon-transitive epsilon-connected ordinal natural real V30() finite cardinal ext-real non negative Element of NAT

EG1 is V21() epsilon-transitive epsilon-connected ordinal natural real V30() finite cardinal ext-real non negative Element of NAT

PMST .cut (VG1,EG1) is Relation-like NAT -defined (the_Vertices_of G1) \/ (the_Edges_of G1) -valued Function-like FinSequence-like directed Trail-like Path-like Walk of G1

(PMST .cut (VG1,EG1)) .first() is Element of the_Vertices_of G1

(PMST .cut (VG1,EG1)) .last() is Element of the_Vertices_of G1

PMST . 1 is set

len PMST is non empty V21() epsilon-transitive epsilon-connected ordinal natural real V30() finite cardinal ext-real positive non negative non even Element of NAT

PMST . (len PMST) is set

PMST .cut (1,VG1) is Relation-like NAT -defined (the_Vertices_of G1) \/ (the_Edges_of G1) -valued Function-like FinSequence-like directed Trail-like Path-like Walk of G1

PMST .cut (EG1,(len PMST)) is Relation-like NAT -defined (the_Vertices_of G1) \/ (the_Edges_of G1) -valued Function-like FinSequence-like directed Trail-like Path-like Walk of G1

PMST .cut (1,EG1) is Relation-like NAT -defined (the_Vertices_of G1) \/ (the_Edges_of G1) -valued Function-like FinSequence-like directed Trail-like Path-like Walk of G1

(PMST .cut (1,EG1)) .append (PMST .cut (EG1,(len PMST))) is Relation-like NAT -defined (the_Vertices_of G1) \/ (the_Edges_of G1) -valued Function-like FinSequence-like directed Walk of G1

PMST .cut (1,(len PMST)) is Relation-like NAT -defined (the_Vertices_of G1) \/ (the_Edges_of G1) -valued Function-like FinSequence-like directed Trail-like Path-like Walk of G1

(PMST .cut (1,EG1)) .last() is Element of the_Vertices_of G1

PMST . EG1 is set

(PMST .cut (EG1,(len PMST))) .first() is Element of the_Vertices_of G1

PMST .cost() is V21() real ext-real Element of REAL

PMST .weightSeq() is Relation-like NAT -defined REAL -valued Function-like FinSequence-like V50() V51() V52() FinSequence of REAL

Sum (PMST .weightSeq()) is V21() real ext-real Element of REAL

K168() is Relation-like [:REAL,REAL:] -defined REAL -valued Function-like quasi_total V50() V51() V52() Element of bool [:[:REAL,REAL:],REAL:]

K221(REAL,(PMST .weightSeq()),K168()) is V21() real ext-real Element of REAL

(PMST .cut (1,EG1)) .cost() is V21() real ext-real Element of REAL

(PMST .cut (1,EG1)) .weightSeq() is Relation-like NAT -defined REAL -valued Function-like FinSequence-like V50() V51() V52() FinSequence of REAL

Sum ((PMST .cut (1,EG1)) .weightSeq()) is V21() real ext-real Element of REAL

K221(REAL,((PMST .cut (1,EG1)) .weightSeq()),K168()) is V21() real ext-real Element of REAL

(PMST .cut (EG1,(len PMST))) .cost() is V21() real ext-real Element of REAL

(PMST .cut (EG1,(len PMST))) .weightSeq() is Relation-like NAT -defined REAL -valued Function-like FinSequence-like V50() V51() V52() FinSequence of REAL

Sum ((PMST .cut (EG1,(len PMST))) .weightSeq()) is V21() real ext-real Element of REAL

K221(REAL,((PMST .cut (EG1,(len PMST))) .weightSeq()),K168()) is V21() real ext-real Element of REAL

((PMST .cut (1,EG1)) .cost()) + ((PMST .cut (EG1,(len PMST))) .cost()) is V21() real ext-real set

(PMST .cut (1,VG1)) .append (PMST .cut (VG1,EG1)) is Relation-like NAT -defined (the_Vertices_of G1) \/ (the_Edges_of G1) -valued Function-like FinSequence-like directed Walk of G1

(PMST .cut (1,VG1)) .last() is Element of the_Vertices_of G1

PMST . VG1 is set

(PMST .cut (1,VG1)) .cost() is V21() real ext-real Element of