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
{ b1 where b1 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 : b1 is_Walk_from PMST,G2 } is set
VG1 is set
{ b1 where b1 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 : verum } is set
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