:: HELLY semantic presentation

REAL is complex-membered ext-real-membered real-membered V132() V135() V136() V138() set
NAT is non trivial ordinal non finite cardinal limit_cardinal complex-membered ext-real-membered real-membered rational-membered integer-membered natural-membered V132() V135() Element of K32(REAL)
K32(REAL) is set
omega is non trivial ordinal non finite cardinal limit_cardinal complex-membered ext-real-membered real-membered rational-membered integer-membered natural-membered V132() V135() set
K32(omega) is non trivial non finite set
K32(NAT) is non trivial non finite set
{} is empty V7() non-empty empty-yielding V10( NAT ) Function-like one-to-one constant functional ordinal natural V27() ext-real non positive non negative finite finite-yielding V39() cardinal {} -element FinSequence-like FinSubsequence-like FinSequence-membered V73() V74() complex-membered ext-real-membered real-membered rational-membered integer-membered natural-membered V132() V135() V136() V137() V138() set
the empty V7() non-empty empty-yielding V10( NAT ) Function-like one-to-one constant functional ordinal natural V27() ext-real non positive non negative finite finite-yielding V39() cardinal {} -element FinSequence-like FinSubsequence-like FinSequence-membered V73() V74() complex-membered ext-real-membered real-membered rational-membered integer-membered natural-membered V132() V135() V136() V137() V138() set is empty V7() non-empty empty-yielding V10( NAT ) Function-like one-to-one constant functional ordinal natural V27() ext-real non positive non negative finite finite-yielding V39() cardinal {} -element FinSequence-like FinSubsequence-like FinSequence-membered V73() V74() complex-membered ext-real-membered real-membered rational-membered integer-membered natural-membered V132() V135() V136() V137() V138() set
1 is non empty ordinal natural V27() ext-real positive non negative finite cardinal V73() V74() complex-membered ext-real-membered real-membered rational-membered integer-membered natural-membered V133() V134() V135() V136() V137() V139() Element of NAT
2 is non empty ordinal natural V27() ext-real positive non negative finite cardinal V73() V74() complex-membered ext-real-membered real-membered rational-membered integer-membered natural-membered V133() V134() V135() V136() V137() V139() Element of NAT
3 is non empty ordinal natural V27() ext-real positive non negative finite cardinal V73() V74() complex-membered ext-real-membered real-membered rational-membered integer-membered natural-membered V133() V134() V135() V136() V137() V139() Element of NAT
_GraphSelectors is non empty complex-membered ext-real-membered real-membered rational-membered integer-membered natural-membered V133() V135() Element of K32(NAT)
0 is empty V7() non-empty empty-yielding V10( NAT ) Function-like one-to-one constant functional ordinal natural V27() ext-real non positive non negative finite finite-yielding V39() cardinal {} -element FinSequence-like FinSubsequence-like FinSequence-membered V73() V74() complex-membered ext-real-membered real-membered rational-membered integer-membered natural-membered V132() V135() V136() V137() V138() V139() Element of NAT
Seg 1 is non empty trivial finite 1 -element complex-membered ext-real-membered real-membered rational-membered integer-membered natural-membered V133() V134() V135() V136() V137() Element of K32(NAT)
{1} is non empty trivial finite V39() 1 -element complex-membered ext-real-membered real-membered rational-membered integer-membered natural-membered V133() V134() V135() V136() V137() set
Seg 2 is non empty finite 2 -element complex-membered ext-real-membered real-membered rational-membered integer-membered natural-membered V133() V134() V135() V136() V137() Element of K32(NAT)
{1,2} is non empty finite V39() complex-membered ext-real-membered real-membered rational-membered integer-membered natural-membered V133() V134() V135() V136() V137() set
card {} is empty V7() non-empty empty-yielding V10( NAT ) Function-like one-to-one constant functional ordinal natural V27() ext-real non positive non negative finite finite-yielding V39() cardinal {} -element FinSequence-like FinSubsequence-like FinSequence-membered V73() V74() complex-membered ext-real-membered real-membered rational-membered integer-membered natural-membered V132() V135() V136() V137() V138() set
T is non empty V7() V10( NAT ) Function-like finite FinSequence-like FinSubsequence-like set
T . 1 is set
<*(T . 1)*> is non empty trivial V7() V10( NAT ) Function-like constant finite 1 -element FinSequence-like FinSubsequence-like set
<*(T . 1)*> ^' T is V7() V10( NAT ) Function-like finite FinSequence-like FinSubsequence-like set
len (<*(T . 1)*> ^' T) is ordinal natural V27() ext-real non negative finite cardinal V73() V74() complex-membered ext-real-membered real-membered rational-membered integer-membered natural-membered V135() V136() V137() V139() Element of NAT
(len (<*(T . 1)*> ^' T)) + 1 is non empty ordinal natural V27() ext-real positive non negative finite cardinal V73() V74() complex-membered ext-real-membered real-membered rational-membered integer-membered natural-membered V133() V134() V135() V136() V137() V139() Element of NAT
len <*(T . 1)*> is non empty ordinal natural V27() ext-real positive non negative finite cardinal V73() V74() complex-membered ext-real-membered real-membered rational-membered integer-membered natural-membered V133() V134() V135() V136() V137() V139() Element of NAT
len T is non empty ordinal natural V27() ext-real positive non negative finite cardinal V73() V74() complex-membered ext-real-membered real-membered rational-membered integer-membered natural-membered V133() V134() V135() V136() V137() V139() Element of NAT
(len <*(T . 1)*>) + (len T) is non empty ordinal natural V27() ext-real positive non negative finite cardinal V73() V74() complex-membered ext-real-membered real-membered rational-membered integer-membered natural-membered V133() V134() V135() V136() V137() V139() Element of NAT
H is ordinal natural V27() ext-real non negative finite cardinal V73() V74() set
(<*(T . 1)*> ^' T) . H is set
<*(T . 1)*> . 1 is set
T . H is set
H9 is ordinal natural V27() ext-real non negative finite cardinal V73() V74() complex-membered ext-real-membered real-membered rational-membered integer-membered natural-membered V135() V136() V137() V139() Element of NAT
(len <*(T . 1)*>) + H9 is non empty ordinal natural V27() ext-real positive non negative finite cardinal V73() V74() complex-membered ext-real-membered real-membered rational-membered integer-membered natural-membered V133() V134() V135() V136() V137() V139() Element of NAT
(<*(T . 1)*> ^' T) . H is set
T . H is set
1 + (len T) is non empty ordinal natural V27() ext-real positive non negative finite cardinal V73() V74() complex-membered ext-real-membered real-membered rational-membered integer-membered natural-membered V133() V134() V135() V136() V137() V139() Element of NAT
T is V7() V10( NAT ) Function-like finite FinSequence-like FinSubsequence-like set
X is V7() V10( NAT ) Function-like finite FinSequence-like FinSubsequence-like set
len T is ordinal natural V27() ext-real non negative finite cardinal V73() V74() complex-membered ext-real-membered real-membered rational-membered integer-membered natural-membered V135() V136() V137() V139() Element of NAT
{ H₁(b₁) where b₁ is ordinal natural V27() ext-real non negative finite cardinal V73() V74() complex-membered ext-real-membered real-membered rational-membered integer-membered natural-membered V135() V136() V137() V139() Element of NAT : ( 0 <= b₁ & b₁ <= len T & S₁[b₁] ) } is set
H9 is set
cH is ordinal natural V27() ext-real non negative finite cardinal V73() V74() complex-membered ext-real-membered real-membered rational-membered integer-membered natural-membered V135() V136() V137() V139() Element of NAT
A is V7() V10( NAT ) Function-like finite FinSequence-like FinSubsequence-like set
len A is ordinal natural V27() ext-real non negative finite cardinal V73() V74() complex-membered ext-real-membered real-membered rational-membered integer-membered natural-membered V135() V136() V137() V139() Element of NAT
len {} is empty V7() non-empty empty-yielding V10( NAT ) Function-like one-to-one constant functional ordinal natural V27() ext-real non positive non negative finite finite-yielding V39() cardinal {} -element FinSequence-like FinSubsequence-like FinSequence-membered V73() V74() complex-membered ext-real-membered real-membered rational-membered integer-membered natural-membered V132() V135() V136() V137() V138() V139() Element of NAT
H9 is non empty finite complex-membered ext-real-membered real-membered rational-membered integer-membered natural-membered V133() V134() V135() V136() V137() set
max H9 is ordinal natural V27() ext-real non negative finite cardinal V73() V74() V139() set
A is ordinal natural V27() ext-real non negative finite cardinal V73() V74() complex-membered ext-real-membered real-membered rational-membered integer-membered natural-membered V135() V136() V137() V139() Element of NAT
A is V7() V10( NAT ) Function-like finite FinSequence-like FinSubsequence-like set
len A is ordinal natural V27() ext-real non negative finite cardinal V73() V74() complex-membered ext-real-membered real-membered rational-membered integer-membered natural-membered V135() V136() V137() V139() Element of NAT
A is V7() V10( NAT ) Function-like finite FinSequence-like FinSubsequence-like set
len A is ordinal natural V27() ext-real non negative finite cardinal V73() V74() complex-membered ext-real-membered real-membered rational-membered integer-membered natural-membered V135() V136() V137() V139() Element of NAT
mA is V7() V10( NAT ) Function-like finite FinSequence-like FinSubsequence-like set
dom mA is finite complex-membered ext-real-membered real-membered rational-membered integer-membered natural-membered V135() V136() V137() Element of K32(NAT)
dom T is finite complex-membered ext-real-membered real-membered rational-membered integer-membered natural-membered V135() V136() V137() Element of K32(NAT)
len mA is ordinal natural V27() ext-real non negative finite cardinal V73() V74() complex-membered ext-real-membered real-membered rational-membered integer-membered natural-membered V135() V136() V137() V139() Element of NAT
dom A is finite complex-membered ext-real-membered real-membered rational-membered integer-membered natural-membered V135() V136() V137() Element of K32(NAT)
cA is set
mA . cA is set
T . cA is set
A . cA is set
H is V7() V10( NAT ) Function-like finite FinSequence-like FinSubsequence-like set
H9 is V7() V10( NAT ) Function-like finite FinSequence-like FinSubsequence-like set
H is V7() V10( NAT ) Function-like finite FinSequence-like FinSubsequence-like set
H9 is V7() V10( NAT ) Function-like finite FinSequence-like FinSubsequence-like set
cH is V7() V10( NAT ) Function-like finite FinSequence-like FinSubsequence-like set
A is V7() V10( NAT ) Function-like finite FinSequence-like FinSubsequence-like set
T is V7() V10( NAT ) Function-like finite FinSequence-like FinSubsequence-like set
X is V7() V10( NAT ) Function-like finite FinSequence-like FinSubsequence-like set
(T,X) is V7() V10( NAT ) Function-like finite FinSequence-like FinSubsequence-like set
T is V7() V10( NAT ) Function-like finite FinSequence-like FinSubsequence-like set
X is V7() V10( NAT ) Function-like finite FinSequence-like FinSubsequence-like set
(T,X) is V7() V10( NAT ) Function-like finite FinSequence-like FinSubsequence-like set
len (T,X) is ordinal natural V27() ext-real non negative finite cardinal V73() V74() complex-membered ext-real-membered real-membered rational-membered integer-membered natural-membered V135() V136() V137() V139() Element of NAT
len T is ordinal natural V27() ext-real non negative finite cardinal V73() V74() complex-membered ext-real-membered real-membered rational-membered integer-membered natural-membered V135() V136() V137() V139() Element of NAT
T is non empty V7() V10( NAT ) Function-like finite FinSequence-like FinSubsequence-like set
T . 1 is set
<*(T . 1)*> is non empty trivial V7() V10( NAT ) Function-like constant finite 1 -element FinSequence-like FinSubsequence-like set
dom <*(T . 1)*> is non empty trivial finite 1 -element complex-membered ext-real-membered real-membered rational-membered integer-membered natural-membered V133() V134() V135() V136() V137() Element of K32(NAT)
X is set
<*(T . 1)*> . X is set
T . X is set
len T is non empty ordinal natural V27() ext-real positive non negative finite cardinal V73() V74() complex-membered ext-real-membered real-membered rational-membered integer-membered natural-membered V133() V134() V135() V136() V137() V139() Element of NAT
len <*(T . 1)*> is non empty ordinal natural V27() ext-real positive non negative finite cardinal V73() V74() complex-membered ext-real-membered real-membered rational-membered integer-membered natural-membered V133() V134() V135() V136() V137() V139() Element of NAT
dom T is non empty finite complex-membered ext-real-membered real-membered rational-membered integer-membered natural-membered V133() V134() V135() V136() V137() Element of K32(NAT)
T is non empty V7() V10( NAT ) Function-like finite FinSequence-like FinSubsequence-like set
T . 1 is set
X is non empty V7() V10( NAT ) Function-like finite FinSequence-like FinSubsequence-like set
X . 1 is set
(T,X) is V7() V10( NAT ) Function-like finite FinSequence-like FinSubsequence-like set
len (T,X) is ordinal natural V27() ext-real non negative finite cardinal V73() V74() complex-membered ext-real-membered real-membered rational-membered integer-membered natural-membered V135() V136() V137() V139() Element of NAT
<*(T . 1)*> is non empty trivial V7() V10( NAT ) Function-like constant finite 1 -element FinSequence-like FinSubsequence-like set
len <*(T . 1)*> is non empty ordinal natural V27() ext-real positive non negative finite cardinal V73() V74() complex-membered ext-real-membered real-membered rational-membered integer-membered natural-membered V133() V134() V135() V136() V137() V139() Element of NAT
T is V7() V10( NAT ) Function-like finite FinSequence-like FinSubsequence-like set
X is V7() V10( NAT ) Function-like finite FinSequence-like FinSubsequence-like set
(T,X) is V7() V10( NAT ) Function-like finite FinSequence-like FinSubsequence-like set
len (T,X) is ordinal natural V27() ext-real non negative finite cardinal V73() V74() complex-membered ext-real-membered real-membered rational-membered integer-membered natural-membered V135() V136() V137() V139() Element of NAT
H is ordinal natural V27() ext-real non negative finite cardinal V73() V74() set
(T,X) . H is set
T . H is set
dom T is finite complex-membered ext-real-membered real-membered rational-membered integer-membered natural-membered V135() V136() V137() Element of K32(NAT)
dom (T,X) is finite complex-membered ext-real-membered real-membered rational-membered integer-membered natural-membered V135() V136() V137() Element of K32(NAT)
0 + 1 is non empty ordinal natural V27() ext-real positive non negative finite cardinal V73() V74() complex-membered ext-real-membered real-membered rational-membered integer-membered natural-membered V133() V134() V135() V136() V137() V139() Element of NAT
dom (T,X) is finite complex-membered ext-real-membered real-membered rational-membered integer-membered natural-membered V135() V136() V137() Element of K32(NAT)
T is V7() V10( NAT ) Function-like finite FinSequence-like FinSubsequence-like set
X is V7() V10( NAT ) Function-like finite FinSequence-like FinSubsequence-like set
(T,X) is V7() V10( NAT ) Function-like finite FinSequence-like FinSubsequence-like set
len (T,X) is ordinal natural V27() ext-real non negative finite cardinal V73() V74() complex-membered ext-real-membered real-membered rational-membered integer-membered natural-membered V135() V136() V137() V139() Element of NAT
H is ordinal natural V27() ext-real non negative finite cardinal V73() V74() set
T . H is set
X . H is set
(T,X) . H is set
T is V7() V10( NAT ) Function-like finite FinSequence-like FinSubsequence-like set
X is V7() V10( NAT ) Function-like finite FinSequence-like FinSubsequence-like set
len T is ordinal natural V27() ext-real non negative finite cardinal V73() V74() complex-membered ext-real-membered real-membered rational-membered integer-membered natural-membered V135() V136() V137() V139() Element of NAT
(T,X) is V7() V10( NAT ) Function-like finite FinSequence-like FinSubsequence-like set
len (T,X) is ordinal natural V27() ext-real non negative finite cardinal V73() V74() complex-membered ext-real-membered real-membered rational-membered integer-membered natural-membered V135() V136() V137() V139() Element of NAT
dom (T,X) is finite complex-membered ext-real-membered real-membered rational-membered integer-membered natural-membered V135() V136() V137() Element of K32(NAT)
dom T is finite complex-membered ext-real-membered real-membered rational-membered integer-membered natural-membered V135() V136() V137() Element of K32(NAT)
T is V7() V10( NAT ) Function-like finite FinSequence-like FinSubsequence-like set
X is V7() V10( NAT ) Function-like finite FinSequence-like FinSubsequence-like set
(T,X) is V7() V10( NAT ) Function-like finite FinSequence-like FinSubsequence-like set
len (T,X) is ordinal natural V27() ext-real non negative finite cardinal V73() V74() complex-membered ext-real-membered real-membered rational-membered integer-membered natural-membered V135() V136() V137() V139() Element of NAT
(len (T,X)) + 1 is non empty ordinal natural V27() ext-real positive non negative finite cardinal V73() V74() complex-membered ext-real-membered real-membered rational-membered integer-membered natural-membered V133() V134() V135() V136() V137() V139() Element of NAT
T . ((len (T,X)) + 1) is set
X . ((len (T,X)) + 1) is set
<*(T . ((len (T,X)) + 1))*> is non empty trivial V7() V10( NAT ) Function-like constant finite 1 -element FinSequence-like FinSubsequence-like set
(T,X) ^ <*(T . ((len (T,X)) + 1))*> is non empty V7() V10( NAT ) Function-like finite FinSequence-like FinSubsequence-like set
A is set
dom ((T,X) ^ <*(T . ((len (T,X)) + 1))*>) is non empty finite complex-membered ext-real-membered real-membered rational-membered integer-membered natural-membered V133() V134() V135() V136() V137() Element of K32(NAT)
A is ordinal natural V27() ext-real non negative finite cardinal V73() V74() set
len ((T,X) ^ <*(T . ((len (T,X)) + 1))*>) is non empty ordinal natural V27() ext-real positive non negative finite cardinal V73() V74() complex-membered ext-real-membered real-membered rational-membered integer-membered natural-membered V133() V134() V135() V136() V137() V139() Element of NAT
dom (T,X) is finite complex-membered ext-real-membered real-membered rational-membered integer-membered natural-membered V135() V136() V137() Element of K32(NAT)
((T,X) ^ <*(T . ((len (T,X)) + 1))*>) . A is set
(T,X) . A is set
X . A is set
((T,X) ^ <*(T . ((len (T,X)) + 1))*>) . A is set
X . A is set
A is set
A is ordinal natural V27() ext-real non negative finite cardinal V73() V74() set
dom (T,X) is finite complex-membered ext-real-membered real-membered rational-membered integer-membered natural-membered V135() V136() V137() Element of K32(NAT)
((T,X) ^ <*(T . ((len (T,X)) + 1))*>) . A is set
(T,X) . A is set
T . A is set
((T,X) ^ <*(T . ((len (T,X)) + 1))*>) . A is set
T . A is set
len X is ordinal natural V27() ext-real non negative finite cardinal V73() V74() complex-membered ext-real-membered real-membered rational-membered integer-membered natural-membered V135() V136() V137() V139() Element of NAT
dom X is finite complex-membered ext-real-membered real-membered rational-membered integer-membered natural-membered V135() V136() V137() Element of K32(NAT)
len T is ordinal natural V27() ext-real non negative finite cardinal V73() V74() complex-membered ext-real-membered real-membered rational-membered integer-membered natural-membered V135() V136() V137() V139() Element of NAT
dom T is finite complex-membered ext-real-membered real-membered rational-membered integer-membered natural-membered V135() V136() V137() Element of K32(NAT)
T is V7() V10( NAT ) Function-like finite [Graph-like] set
the_Vertices_of T is non empty set
the_Edges_of T is set
(the_Vertices_of T) \/ (the_Edges_of T) is non empty set
X is V7() V10( NAT ) V11((the_Vertices_of T) \/ (the_Edges_of T)) Function-like finite FinSequence-like FinSubsequence-like Walk of T
len X is non empty ordinal natural V27() ext-real positive non negative finite cardinal V73() V74() non even complex-membered ext-real-membered real-membered rational-membered integer-membered natural-membered V133() V134() V135() V136() V137() V139() Element of NAT
H is ordinal natural V27() ext-real non negative finite cardinal V73() V74() set
H9 is ordinal natural V27() ext-real non negative finite cardinal V73() V74() set
X .cut (H,H9) is V7() V10( NAT ) V11((the_Vertices_of T) \/ (the_Edges_of T)) Function-like finite FinSequence-like FinSubsequence-like Walk of T
len (X .cut (H,H9)) is non empty ordinal natural V27() ext-real positive non negative finite cardinal V73() V74() non even complex-membered ext-real-membered real-membered rational-membered integer-membered natural-membered V133() V134() V135() V136() V137() V139() Element of NAT
(H,H9) -cut X is V7() V10( NAT ) V11((the_Vertices_of T) \/ (the_Edges_of T)) Function-like finite FinSequence-like FinSubsequence-like FinSequence of (the_Vertices_of T) \/ (the_Edges_of T)
cH is ordinal natural V27() ext-real non negative finite cardinal V73() V74() complex-membered ext-real-membered real-membered rational-membered integer-membered natural-membered V135() V136() V137() V139() Element of NAT
A is ordinal natural V27() ext-real non negative finite cardinal V73() V74() complex-membered ext-real-membered real-membered rational-membered integer-membered natural-membered V135() V136() V137() V139() Element of NAT
X .cut (cH,A) is V7() V10( NAT ) V11((the_Vertices_of T) \/ (the_Edges_of T)) Function-like finite FinSequence-like FinSubsequence-like Walk of T
len (X .cut (cH,A)) is non empty ordinal natural V27() ext-real positive non negative finite cardinal V73() V74() non even complex-membered ext-real-membered real-membered rational-membered integer-membered natural-membered V133() V134() V135() V136() V137() V139() Element of NAT
T is V7() V10( NAT ) Function-like finite [Graph-like] set
the_Vertices_of T is non empty set
the_Edges_of T is set
(the_Vertices_of T) \/ (the_Edges_of T) is non empty set
X is V7() V10( NAT ) V11((the_Vertices_of T) \/ (the_Edges_of T)) Function-like finite FinSequence-like FinSubsequence-like Walk of T
H is ordinal natural V27() ext-real non negative finite cardinal V73() V74() set
H9 is ordinal natural V27() ext-real non negative finite cardinal V73() V74() set
X .cut (H,H9) is V7() V10( NAT ) V11((the_Vertices_of T) \/ (the_Edges_of T)) Function-like finite FinSequence-like FinSubsequence-like Walk of T
cH is V7() V10( NAT ) V11((the_Vertices_of T) \/ (the_Edges_of T)) Function-like finite FinSequence-like FinSubsequence-like trivial Trail-like Path-like vertex-distinct Walk of T
A is ordinal natural V27() ext-real non negative finite cardinal V73() V74() complex-membered ext-real-membered real-membered rational-membered integer-membered natural-membered V135() V136() V137() V139() Element of NAT
A is ordinal natural V27() ext-real non negative finite cardinal V73() V74() complex-membered ext-real-membered real-membered rational-membered integer-membered natural-membered V135() V136() V137() V139() Element of NAT
cH .cut (A,A) is V7() V10( NAT ) V11((the_Vertices_of T) \/ (the_Edges_of T)) Function-like finite FinSequence-like FinSubsequence-like trivial Trail-like Path-like vertex-distinct Walk of T
T is V7() V10( NAT ) Function-like finite [Graph-like] set
the_Vertices_of T is non empty set
the_Edges_of T is set
(the_Vertices_of T) \/ (the_Edges_of T) is non empty set
X is V7() V10( NAT ) V11((the_Vertices_of T) \/ (the_Edges_of T)) Function-like finite FinSequence-like FinSubsequence-like Walk of T
len X is non empty ordinal natural V27() ext-real positive non negative finite cardinal V73() V74() non even complex-membered ext-real-membered real-membered rational-membered integer-membered natural-membered V133() V134() V135() V136() V137() V139() Element of NAT
H is non empty ordinal natural V27() ext-real positive non negative finite cardinal V73() V74() non even set
H9 is non empty ordinal natural V27() ext-real positive non negative finite cardinal V73() V74() non even set
cH is non empty ordinal natural V27() ext-real positive non negative finite cardinal V73() V74() non even set
X .cut (H,H9) is V7() V10( NAT ) V11((the_Vertices_of T) \/ (the_Edges_of T)) Function-like finite FinSequence-like FinSubsequence-like Walk of T
len (X .cut (H,H9)) is non empty ordinal natural V27() ext-real positive non negative finite cardinal V73() V74() non even complex-membered ext-real-membered real-membered rational-membered integer-membered natural-membered V133() V134() V135() V136() V137() V139() Element of NAT
(X .cut (H,H9)) . cH is set
H + cH is non empty ordinal natural V27() ext-real positive non negative finite cardinal V73() V74() even set
(H + cH) - 1 is non empty V27() ext-real V73() V74() non even set
1 + 1 is non empty ordinal natural V27() ext-real positive non negative finite cardinal V73() V74() complex-membered ext-real-membered real-membered rational-membered integer-membered natural-membered V133() V134() V135() V136() V137() V139() Element of NAT
(1 + 1) - 1 is V27() ext-real V73() V74() set
A is non empty ordinal natural V27() ext-real positive non negative finite cardinal V73() V74() non even set
X . A is set
1 - 1 is V27() ext-real V73() V74() set
cH - 1 is V27() ext-real V73() V74() even set
(len (X .cut (H,H9))) + 1 is non empty ordinal natural V27() ext-real positive non negative finite cardinal V73() V74() even complex-membered ext-real-membered real-membered rational-membered integer-membered natural-membered V133() V134() V135() V136() V137() V139() Element of NAT
((len (X .cut (H,H9))) + 1) - 1 is non empty V27() ext-real V73() V74() non even set
B is ordinal natural V27() ext-real non negative finite cardinal V73() V74() complex-membered ext-real-membered real-membered rational-membered integer-membered natural-membered V135() V136() V137() V139() Element of NAT
mA is non empty ordinal natural V27() ext-real positive non negative finite cardinal V73() V74() non even complex-membered ext-real-membered real-membered rational-membered integer-membered natural-membered V133() V134() V135() V136() V137() V139() Element of NAT
cA is non empty ordinal natural V27() ext-real positive non negative finite cardinal V73() V74() non even complex-membered ext-real-membered real-membered rational-membered integer-membered natural-membered V133() V134() V135() V136() V137() V139() Element of NAT
X .cut (mA,cA) is V7() V10( NAT ) V11((the_Vertices_of T) \/ (the_Edges_of T)) Function-like finite FinSequence-like FinSubsequence-like Walk of T
B + 1 is non empty ordinal natural V27() ext-real positive non negative finite cardinal V73() V74() complex-membered ext-real-membered real-membered rational-membered integer-membered natural-membered V133() V134() V135() V136() V137() V139() Element of NAT
(X .cut (mA,cA)) . (B + 1) is set
H + B is non empty ordinal natural V27() ext-real positive non negative finite cardinal V73() V74() complex-membered ext-real-membered real-membered rational-membered integer-membered natural-membered V133() V134() V135() V136() V137() V139() Element of NAT
X . (H + B) is set
(len (X .cut (H,H9))) + H is non empty ordinal natural V27() ext-real positive non negative finite cardinal V73() V74() even complex-membered ext-real-membered real-membered rational-membered integer-membered natural-membered V133() V134() V135() V136() V137() V139() Element of NAT
mA + cH is non empty ordinal natural V27() ext-real positive non negative finite cardinal V73() V74() even complex-membered ext-real-membered real-membered rational-membered integer-membered natural-membered V133() V134() V135() V136() V137() V139() Element of NAT
cA + 1 is non empty ordinal natural V27() ext-real positive non negative finite cardinal V73() V74() even complex-membered ext-real-membered real-membered rational-membered integer-membered natural-membered V133() V134() V135() V136() V137() V139() Element of NAT
H9 + 1 is non empty ordinal natural V27() ext-real positive non negative finite cardinal V73() V74() even complex-membered ext-real-membered real-membered rational-membered integer-membered natural-membered V133() V134() V135() V136() V137() V139() Element of NAT
(H9 + 1) - 1 is non empty V27() ext-real V73() V74() non even set
T is V7() V10( NAT ) Function-like finite [Graph-like] set
the_Vertices_of T is non empty set
the_Edges_of T is set
(the_Vertices_of T) \/ (the_Edges_of T) is non empty set
X is V7() V10( NAT ) V11((the_Vertices_of T) \/ (the_Edges_of T)) Function-like finite FinSequence-like FinSubsequence-like Walk of T
T is V7() V10( NAT ) Function-like finite [Graph-like] set
the_Vertices_of T is non empty set
the_Edges_of T is set
(the_Vertices_of T) \/ (the_Edges_of T) is non empty set
X is non empty V7() V10( NAT ) V11((the_Vertices_of T) \/ (the_Edges_of T)) Function-like finite FinSequence-like FinSubsequence-like Walk of T
H is non empty V7() V10( NAT ) V11((the_Vertices_of T) \/ (the_Edges_of T)) Function-like finite FinSequence-like FinSubsequence-like Walk of T
X .vertices() is finite Element of K32((the_Vertices_of T))
K32((the_Vertices_of T)) is non empty-membered set
X .vertexSeq() is V7() V10( NAT ) V11( the_Vertices_of T) Function-like finite FinSequence-like FinSubsequence-like VertexSeq of T
K319((the_Vertices_of T),(X .vertexSeq())) is finite Element of K32((the_Vertices_of T))
H .vertices() is finite Element of K32((the_Vertices_of T))
H .vertexSeq() is V7() V10( NAT ) V11( the_Vertices_of T) Function-like finite FinSequence-like FinSubsequence-like VertexSeq of T
K319((the_Vertices_of T),(H .vertexSeq())) is finite Element of K32((the_Vertices_of T))
H9 is set
len X is non empty ordinal natural V27() ext-real positive non negative finite cardinal V73() V74() non even complex-membered ext-real-membered real-membered rational-membered integer-membered natural-membered V133() V134() V135() V136() V137() V139() Element of NAT
cH is non empty ordinal natural V27() ext-real positive non negative finite cardinal V73() V74() non even complex-membered ext-real-membered real-membered rational-membered integer-membered natural-membered V133() V134() V135() V136() V137() V139() Element of NAT
X . cH is set
dom X is non empty finite complex-membered ext-real-membered real-membered rational-membered integer-membered natural-membered V133() V134() V135() V136() V137() Element of K32(NAT)
H . cH is set
len H is non empty ordinal natural V27() ext-real positive non negative finite cardinal V73() V74() non even complex-membered ext-real-membered real-membered rational-membered integer-membered natural-membered V133() V134() V135() V136() V137() V139() Element of NAT
T is V7() V10( NAT ) Function-like finite [Graph-like] set
the_Vertices_of T is non empty set
the_Edges_of T is set
(the_Vertices_of T) \/ (the_Edges_of T) is non empty set
X is non empty V7() V10( NAT ) V11((the_Vertices_of T) \/ (the_Edges_of T)) Function-like finite FinSequence-like FinSubsequence-like Walk of T
H is non empty V7() V10( NAT ) V11((the_Vertices_of T) \/ (the_Edges_of T)) Function-like finite FinSequence-like FinSubsequence-like Walk of T
X .edges() is finite Element of K32((the_Edges_of T))
K32((the_Edges_of T)) is set
X .edgeSeq() is V7() V10( NAT ) V11( the_Edges_of T) Function-like finite FinSequence-like FinSubsequence-like EdgeSeq of T
K319((the_Edges_of T),(X .edgeSeq())) is finite Element of K32((the_Edges_of T))
H .edges() is finite Element of K32((the_Edges_of T))
H .edgeSeq() is V7() V10( NAT ) V11( the_Edges_of T) Function-like finite FinSequence-like FinSubsequence-like EdgeSeq of T
K319((the_Edges_of T),(H .edgeSeq())) is finite Element of K32((the_Edges_of T))
H9 is set
len X is non empty ordinal natural V27() ext-real positive non negative finite cardinal V73() V74() non even complex-membered ext-real-membered real-membered rational-membered integer-membered natural-membered V133() V134() V135() V136() V137() V139() Element of NAT
cH is ordinal natural V27() ext-real non negative finite cardinal V73() V74() even complex-membered ext-real-membered real-membered rational-membered integer-membered natural-membered V135() V136() V137() V139() Element of NAT
X . cH is set
dom X is non empty finite complex-membered ext-real-membered real-membered rational-membered integer-membered natural-membered V133() V134() V135() V136() V137() Element of K32(NAT)
H . cH is set
len H is non empty ordinal natural V27() ext-real positive non negative finite cardinal V73() V74() non even complex-membered ext-real-membered real-membered rational-membered integer-membered natural-membered V133() V134() V135() V136() V137() V139() Element of NAT
T is V7() V10( NAT ) Function-like finite [Graph-like] set
the_Vertices_of T is non empty set
the_Edges_of T is set
(the_Vertices_of T) \/ (the_Edges_of T) is non empty set
X is non empty V7() V10( NAT ) V11((the_Vertices_of T) \/ (the_Edges_of T)) Function-like finite FinSequence-like FinSubsequence-like Walk of T
H is non empty V7() V10( NAT ) V11((the_Vertices_of T) \/ (the_Edges_of T)) Function-like finite FinSequence-like FinSubsequence-like Walk of T
X .append H is non empty V7() V10( NAT ) V11((the_Vertices_of T) \/ (the_Edges_of T)) Function-like finite FinSequence-like FinSubsequence-like Walk of T
X .last() is Element of the_Vertices_of T
len X is non empty ordinal natural V27() ext-real positive non negative finite cardinal V73() V74() non even complex-membered ext-real-membered real-membered rational-membered integer-membered natural-membered V133() V134() V135() V136() V137() V139() Element of NAT
X . (len X) is set
H .first() is Element of the_Vertices_of T
H . 1 is set
len (X .append H) is non empty ordinal natural V27() ext-real positive non negative finite cardinal V73() V74() non even complex-membered ext-real-membered real-membered rational-membered integer-membered natural-membered V133() V134() V135() V136() V137() V139() Element of NAT
dom X is non empty finite complex-membered ext-real-membered real-membered rational-membered integer-membered natural-membered V133() V134() V135() V136() V137() Element of K32(NAT)
dom (X .append H) is non empty finite complex-membered ext-real-membered real-membered rational-membered integer-membered natural-membered V133() V134() V135() V136() V137() Element of K32(NAT)
cH is set
X . cH is set
(X .append H) . cH is set
X .last() is Element of the_Vertices_of T
len X is non empty ordinal natural V27() ext-real positive non negative finite cardinal V73() V74() non even complex-membered ext-real-membered real-membered rational-membered integer-membered natural-membered V133() V134() V135() V136() V137() V139() Element of NAT
X . (len X) is set
H .first() is Element of the_Vertices_of T
H . 1 is set
X .last() is Element of the_Vertices_of T
len X is non empty ordinal natural V27() ext-real positive non negative finite cardinal V73() V74() non even complex-membered ext-real-membered real-membered rational-membered integer-membered natural-membered V133() V134() V135() V136() V137() V139() Element of NAT
X . (len X) is set
H .first() is Element of the_Vertices_of T
H . 1 is set
T is V7() V10( NAT ) Function-like finite [Graph-like] set
the_Vertices_of T is non empty set
the_Edges_of T is set
(the_Vertices_of T) \/ (the_Edges_of T) is non empty set
X is non empty V7() V10( NAT ) V11((the_Vertices_of T) \/ (the_Edges_of T)) Function-like finite FinSequence-like FinSubsequence-like Walk of T
X .last() is Element of the_Vertices_of T
len X is non empty ordinal natural V27() ext-real positive non negative finite cardinal V73() V74() non even complex-membered ext-real-membered real-membered rational-membered integer-membered natural-membered V133() V134() V135() V136() V137() V139() Element of NAT
X . (len X) is set
H is non empty V7() V10( NAT ) V11((the_Vertices_of T) \/ (the_Edges_of T)) Function-like finite FinSequence-like FinSubsequence-like Walk of T
H .first() is Element of the_Vertices_of T
H . 1 is set
X .append H is non empty V7() V10( NAT ) V11((the_Vertices_of T) \/ (the_Edges_of T)) Function-like finite FinSequence-like FinSubsequence-like Walk of T
len (X .append H) is non empty ordinal natural V27() ext-real positive non negative finite cardinal V73() V74() non even complex-membered ext-real-membered real-membered rational-membered integer-membered natural-membered V133() V134() V135() V136() V137() V139() Element of NAT
(len (X .append H)) + 1 is non empty ordinal natural V27() ext-real positive non negative finite cardinal V73() V74() even complex-membered ext-real-membered real-membered rational-membered integer-membered natural-membered V133() V134() V135() V136() V137() V139() Element of NAT
len H is non empty ordinal natural V27() ext-real positive non negative finite cardinal V73() V74() non even complex-membered ext-real-membered real-membered rational-membered integer-membered natural-membered V133() V134() V135() V136() V137() V139() Element of NAT
1 + (len H) is non empty ordinal natural V27() ext-real positive non negative finite cardinal V73() V74() even complex-membered ext-real-membered real-membered rational-membered integer-membered natural-membered V133() V134() V135() V136() V137() V139() Element of NAT
H9 is ordinal natural V27() ext-real non negative finite cardinal V73() V74() set
1 - 1 is V27() ext-real V73() V74() set
H9 - 1 is V27() ext-real V73() V74() set
cH is ordinal natural V27() ext-real non negative finite cardinal V73() V74() complex-membered ext-real-membered real-membered rational-membered integer-membered natural-membered V135() V136() V137() V139() Element of NAT
1 + cH is non empty ordinal natural V27() ext-real positive non negative finite cardinal V73() V74() complex-membered ext-real-membered real-membered rational-membered integer-membered natural-membered V133() V134() V135() V136() V137() V139() Element of NAT
(X .append H) . (1 + cH) is set
cH + 1 is non empty ordinal natural V27() ext-real positive non negative finite cardinal V73() V74() complex-membered ext-real-membered real-membered rational-membered integer-membered natural-membered V133() V134() V135() V136() V137() V139() Element of NAT
H . (cH + 1) is set
(X .append H) . H9 is set
H . H9 is set
T is V7() V10( NAT ) Function-like finite [Graph-like] set
the_Vertices_of T is non empty set
the_Edges_of T is set
(the_Vertices_of T) \/ (the_Edges_of T) is non empty set
X is non empty V7() V10( NAT ) V11((the_Vertices_of T) \/ (the_Edges_of T)) Function-like finite FinSequence-like FinSubsequence-like Trail-like Walk of T
X .last() is Element of the_Vertices_of T
len X is non empty ordinal natural V27() ext-real positive non negative finite cardinal V73() V74() non even complex-membered ext-real-membered real-membered rational-membered integer-membered natural-membered V133() V134() V135() V136() V137() V139() Element of NAT
X . (len X) is set
H is non empty V7() V10( NAT ) V11((the_Vertices_of T) \/ (the_Edges_of T)) Function-like finite FinSequence-like FinSubsequence-like Trail-like Walk of T
H .first() is Element of the_Vertices_of T
H . 1 is set
X .edges() is finite Element of K32((the_Edges_of T))
K32((the_Edges_of T)) is set
X .edgeSeq() is V7() V10( NAT ) V11( the_Edges_of T) Function-like finite FinSequence-like FinSubsequence-like EdgeSeq of T
K319((the_Edges_of T),(X .edgeSeq())) is finite Element of K32((the_Edges_of T))
H .edges() is finite Element of K32((the_Edges_of T))
H .edgeSeq() is V7() V10( NAT ) V11( the_Edges_of T) Function-like finite FinSequence-like FinSubsequence-like EdgeSeq of T
K319((the_Edges_of T),(H .edgeSeq())) is finite Element of K32((the_Edges_of T))
X .append H is non empty V7() V10( NAT ) V11((the_Vertices_of T) \/ (the_Edges_of T)) Function-like finite FinSequence-like FinSubsequence-like Walk of T
cH is ordinal natural V27() ext-real non negative finite cardinal V73() V74() even complex-membered ext-real-membered real-membered rational-membered integer-membered natural-membered V135() V136() V137() V139() Element of NAT
A is ordinal natural V27() ext-real non negative finite cardinal V73() V74() even complex-membered ext-real-membered real-membered rational-membered integer-membered natural-membered V135() V136() V137() V139() Element of NAT
len (X .append H) is non empty ordinal natural V27() ext-real positive non negative finite cardinal V73() V74() non even complex-membered ext-real-membered real-membered rational-membered integer-membered natural-membered V133() V134() V135() V136() V137() V139() Element of NAT
dom (X .append H) is non empty finite complex-membered ext-real-membered real-membered rational-membered integer-membered natural-membered V133() V134() V135() V136() V137() Element of K32(NAT)
dom X is non empty finite complex-membered ext-real-membered real-membered rational-membered integer-membered natural-membered V133() V134() V135() V136() V137() Element of K32(NAT)
X . cH is set
(X .append H) . cH is set
X . A is set
(X .append H) . A is set
len H is non empty ordinal natural V27() ext-real positive non negative finite cardinal V73() V74() non even complex-membered ext-real-membered real-membered rational-membered integer-membered natural-membered V133() V134() V135() V136() V137() V139() Element of NAT
A is ordinal natural V27() ext-real non negative finite cardinal V73() V74() complex-membered ext-real-membered real-membered rational-membered integer-membered natural-membered V135() V136() V137() V139() Element of NAT
(len X) + A is non empty ordinal natural V27() ext-real positive non negative finite cardinal V73() V74() complex-membered ext-real-membered real-membered rational-membered integer-membered natural-membered V133() V134() V135() V136() V137() V139() Element of NAT
A is ordinal natural V27() ext-real non negative finite cardinal V73() V74() complex-membered ext-real-membered real-membered rational-membered integer-membered natural-membered V135() V136() V137() V139() Element of NAT
(len X) + A is non empty ordinal natural V27() ext-real positive non negative finite cardinal V73() V74() complex-membered ext-real-membered real-membered rational-membered integer-membered natural-membered V133() V134() V135() V136() V137() V139() Element of NAT
(X .append H) . A is set
mA is non empty ordinal natural V27() ext-real positive non negative finite cardinal V73() V74() non even complex-membered ext-real-membered real-membered rational-membered integer-membered natural-membered V133() V134() V135() V136() V137() V139() Element of NAT
mA + 1 is non empty ordinal natural V27() ext-real positive non negative finite cardinal V73() V74() even complex-membered ext-real-membered real-membered rational-membered integer-membered natural-membered V133() V134() V135() V136() V137() V139() Element of NAT
H . (mA + 1) is set
dom X is non empty finite complex-membered ext-real-membered real-membered rational-membered integer-membered natural-membered V133() V134() V135() V136() V137() Element of K32(NAT)
X . cH is set
(X .append H) . cH is set
cA is ordinal natural V27() ext-real non negative finite cardinal V73() V74() complex-membered ext-real-membered real-membered rational-membered integer-membered natural-membered V135() V136() V137() V139() Element of NAT
(len X) + cA is non empty ordinal natural V27() ext-real positive non negative finite cardinal V73() V74() complex-membered ext-real-membered real-membered rational-membered integer-membered natural-membered V133() V134() V135() V136() V137() V139() Element of NAT
cA is ordinal natural V27() ext-real non negative finite cardinal V73() V74() complex-membered ext-real-membered real-membered rational-membered integer-membered natural-membered V135() V136() V137() V139() Element of NAT
(len X) + cA is non empty ordinal natural V27() ext-real positive non negative finite cardinal V73() V74() complex-membered ext-real-membered real-membered rational-membered integer-membered natural-membered V133() V134() V135() V136() V137() V139() Element of NAT
B is non empty ordinal natural V27() ext-real positive non negative finite cardinal V73() V74() non even complex-membered ext-real-membered real-membered rational-membered integer-membered natural-membered V133() V134() V135() V136() V137() V139() Element of NAT
B + 1 is non empty ordinal natural V27() ext-real positive non negative finite cardinal V73() V74() even complex-membered ext-real-membered real-membered rational-membered integer-membered natural-membered V133() V134() V135() V136() V137() V139() Element of NAT
(X .append H) . cH is set
H . (B + 1) is set
dom X is non empty finite complex-membered ext-real-membered real-membered rational-membered integer-membered natural-membered V133() V134() V135() V136() V137() Element of K32(NAT)
dom X is non empty finite complex-membered ext-real-membered real-membered rational-membered integer-membered natural-membered V133() V134() V135() V136() V137() Element of K32(NAT)
len H is non empty ordinal natural V27() ext-real positive non negative finite cardinal V73() V74() non even complex-membered ext-real-membered real-membered rational-membered integer-membered natural-membered V133() V134() V135() V136() V137() V139() Element of NAT
T is V7() V10( NAT ) Function-like finite [Graph-like] set
the_Vertices_of T is non empty set
the_Edges_of T is set
(the_Vertices_of T) \/ (the_Edges_of T) is non empty set
X is non empty V7() V10( NAT ) V11((the_Vertices_of T) \/ (the_Edges_of T)) Function-like finite FinSequence-like FinSubsequence-like Trail-like Path-like Walk of T
X .last() is Element of the_Vertices_of T
len X is non empty ordinal natural V27() ext-real positive non negative finite cardinal V73() V74() non even complex-membered ext-real-membered real-membered rational-membered integer-membered natural-membered V133() V134() V135() V136() V137() V139() Element of NAT
X . (len X) is set
H is non empty V7() V10( NAT ) V11((the_Vertices_of T) \/ (the_Edges_of T)) Function-like finite FinSequence-like FinSubsequence-like Trail-like Path-like Walk of T
H .first() is Element of the_Vertices_of T
H . 1 is set
X .edges() is finite Element of K32((the_Edges_of T))
K32((the_Edges_of T)) is set
X .edgeSeq() is V7() V10( NAT ) V11( the_Edges_of T) Function-like finite FinSequence-like FinSubsequence-like EdgeSeq of T
K319((the_Edges_of T),(X .edgeSeq())) is finite Element of K32((the_Edges_of T))
H .edges() is finite Element of K32((the_Edges_of T))
H .edgeSeq() is V7() V10( NAT ) V11( the_Edges_of T) Function-like finite FinSequence-like FinSubsequence-like EdgeSeq of T
K319((the_Edges_of T),(H .edgeSeq())) is finite Element of K32((the_Edges_of T))
X .first() is Element of the_Vertices_of T
X . 1 is set
H .vertices() is finite Element of K32((the_Vertices_of T))
K32((the_Vertices_of T)) is non empty-membered set
H .vertexSeq() is V7() V10( NAT ) V11( the_Vertices_of T) Function-like finite FinSequence-like FinSubsequence-like VertexSeq of T
K319((the_Vertices_of T),(H .vertexSeq())) is finite Element of K32((the_Vertices_of T))
H .last() is Element of the_Vertices_of T
len H is non empty ordinal natural V27() ext-real positive non negative finite cardinal V73() V74() non even complex-membered ext-real-membered real-membered rational-membered integer-membered natural-membered V133() V134() V135() V136() V137() V139() Element of NAT
H . (len H) is set
X .vertices() is finite Element of K32((the_Vertices_of T))
X .vertexSeq() is V7() V10( NAT ) V11( the_Vertices_of T) Function-like finite FinSequence-like FinSubsequence-like VertexSeq of T
K319((the_Vertices_of T),(X .vertexSeq())) is finite Element of K32((the_Vertices_of T))
(X .vertices()) /\ (H .vertices()) is finite Element of K32((the_Vertices_of T))
{(X .first()),(X .last())} is non empty finite set
X .append H is non empty V7() V10( NAT ) V11((the_Vertices_of T) \/ (the_Edges_of T)) Function-like finite FinSequence-like FinSubsequence-like Walk of T
len (X .append H) is non empty ordinal natural V27() ext-real positive non negative finite cardinal V73() V74() non even complex-membered ext-real-membered real-membered rational-membered integer-membered natural-membered V133() V134() V135() V136() V137() V139() Element of NAT
A is non empty ordinal natural V27() ext-real positive non negative finite cardinal V73() V74() non even complex-membered ext-real-membered real-membered rational-membered integer-membered natural-membered V133() V134() V135() V136() V137() V139() Element of NAT
cH is non empty ordinal natural V27() ext-real positive non negative finite cardinal V73() V74() non even complex-membered ext-real-membered real-membered rational-membered integer-membered natural-membered V133() V134() V135() V136() V137() V139() Element of NAT
(X .append H) . cH is set
(X .append H) . A is set
dom (X .append H) is non empty finite complex-membered ext-real-membered real-membered rational-membered integer-membered natural-membered V133() V134() V135() V136() V137() Element of K32(NAT)
A is ordinal natural V27() ext-real non negative finite cardinal V73() V74() complex-membered ext-real-membered real-membered rational-membered integer-membered natural-membered V135() V136() V137() V139() Element of NAT
(len X) + A is non empty ordinal natural V27() ext-real positive non negative finite cardinal V73() V74() complex-membered ext-real-membered real-membered rational-membered integer-membered natural-membered V133() V134() V135() V136() V137() V139() Element of NAT
A is ordinal natural V27() ext-real non negative finite cardinal V73() V74() complex-membered ext-real-membered real-membered rational-membered integer-membered natural-membered V135() V136() V137() V139() Element of NAT
(len X) + A is non empty ordinal natural V27() ext-real positive non negative finite cardinal V73() V74() complex-membered ext-real-membered real-membered rational-membered integer-membered natural-membered V133() V134() V135() V136() V137() V139() Element of NAT
A + 1 is non empty ordinal natural V27() ext-real positive non negative finite cardinal V73() V74() complex-membered ext-real-membered real-membered rational-membered integer-membered natural-membered V133() V134() V135() V136() V137() V139() Element of NAT
H . (A + 1) is set
mA is ordinal natural V27() ext-real non negative finite cardinal V73() V74() even complex-membered ext-real-membered real-membered rational-membered integer-membered natural-membered V135() V136() V137() V139() Element of NAT
mA + 1 is non empty ordinal natural V27() ext-real positive non negative finite cardinal V73() V74() non even complex-membered ext-real-membered real-membered rational-membered integer-membered natural-membered V133() V134() V135() V136() V137() V139() Element of NAT
H . (mA + 1) is set
cA is ordinal natural V27() ext-real non negative finite cardinal V73() V74() complex-membered ext-real-membered real-membered rational-membered integer-membered natural-membered V135() V136() V137() V139() Element of NAT
(len X) + cA is non empty ordinal natural V27() ext-real positive non negative finite cardinal V73() V74() complex-membered ext-real-membered real-membered rational-membered integer-membered natural-membered V133() V134() V135() V136() V137() V139() Element of NAT
cA is ordinal natural V27() ext-real non negative finite cardinal V73() V74() complex-membered ext-real-membered real-membered rational-membered integer-membered natural-membered V135() V136() V137() V139() Element of NAT
(len X) + cA is non empty ordinal natural V27() ext-real positive non negative finite cardinal V73() V74() complex-membered ext-real-membered real-membered rational-membered integer-membered natural-membered V133() V134() V135() V136() V137() V139() Element of NAT
cA + 1 is non empty ordinal natural V27() ext-real positive non negative finite cardinal V73() V74() complex-membered ext-real-membered real-membered rational-membered integer-membered natural-membered V133() V134() V135() V136() V137() V139() Element of NAT
H . (cA + 1) is set
B is ordinal natural V27() ext-real non negative finite cardinal V73() V74() even complex-membered ext-real-membered real-membered rational-membered integer-membered natural-membered V135() V136() V137() V139() Element of NAT
B + 1 is non empty ordinal natural V27() ext-real positive non negative finite cardinal V73() V74() non even complex-membered ext-real-membered real-membered rational-membered integer-membered natural-membered V133() V134() V135() V136() V137() V139() Element of NAT
H . (B + 1) is set
dom X is non empty finite complex-membered ext-real-membered real-membered rational-membered integer-membered natural-membered V133() V134() V135() V136() V137() Element of K32(NAT)
X . cH is set
2 * 0 is empty V7() non-empty empty-yielding V10( NAT ) Function-like one-to-one constant functional ordinal natural V27() ext-real non positive non negative finite finite-yielding V39() cardinal {} -element FinSequence-like FinSubsequence-like FinSequence-membered V73() V74() even complex-membered ext-real-membered real-membered rational-membered integer-membered natural-membered V132() V135() V136() V137() V138() V139() Element of NAT
(2 * 0) + 1 is non empty ordinal natural V27() ext-real positive non negative finite cardinal V73() V74() non even complex-membered ext-real-membered real-membered rational-membered integer-membered natural-membered V133() V134() V135() V136() V137() V139() Element of NAT
2 * 0 is empty V7() non-empty empty-yielding V10( NAT ) Function-like one-to-one constant functional ordinal natural V27() ext-real non positive non negative finite finite-yielding V39() cardinal {} -element FinSequence-like FinSubsequence-like FinSequence-membered V73() V74() even complex-membered ext-real-membered real-membered rational-membered integer-membered natural-membered V132() V135() V136() V137() V138() V139() Element of NAT
(2 * 0) + 1 is non empty ordinal natural V27() ext-real positive non negative finite cardinal V73() V74() non even complex-membered ext-real-membered real-membered rational-membered integer-membered natural-membered V133() V134() V135() V136() V137() V139() Element of NAT
X . ((2 * 0) + 1) is set
(len (X .append H)) + 1 is non empty ordinal natural V27() ext-real positive non negative finite cardinal V73() V74() even complex-membered ext-real-membered real-membered rational-membered integer-membered natural-membered V133() V134() V135() V136() V137() V139() Element of NAT
(len X) + (mA + 1) is non empty ordinal natural V27() ext-real positive non negative finite cardinal V73() V74() even complex-membered ext-real-membered real-membered rational-membered integer-membered natural-membered V133() V134() V135() V136() V137() V139() Element of NAT
dom X is non empty finite complex-membered ext-real-membered real-membered rational-membered integer-membered natural-membered V133() V134() V135() V136() V137() Element of K32(NAT)
dom X is non empty finite complex-membered ext-real-membered real-membered rational-membered integer-membered natural-membered V133() V134() V135() V136() V137() Element of K32(NAT)
X . cH is set
X . A is set
dom X is non empty finite complex-membered ext-real-membered real-membered rational-membered integer-membered natural-membered V133() V134() V135() V136() V137() Element of K32(NAT)
T is V7() V10( NAT ) Function-like finite [Graph-like] set
the_Vertices_of T is non empty set
the_Edges_of T is set
(the_Vertices_of T) \/ (the_Edges_of T) is non empty set
X is non empty V7() V10( NAT ) V11((the_Vertices_of T) \/ (the_Edges_of T)) Function-like finite FinSequence-like FinSubsequence-like Trail-like Path-like Walk of T
X .last() is Element of the_Vertices_of T
len X is non empty ordinal natural V27() ext-real positive non negative finite cardinal V73() V74() non even complex-membered ext-real-membered real-membered rational-membered integer-membered natural-membered V133() V134() V135() V136() V137() V139() Element of NAT
X . (len X) is set
H is non empty V7() V10( NAT ) V11((the_Vertices_of T) \/ (the_Edges_of T)) Function-like finite FinSequence-like FinSubsequence-like Trail-like Path-like Walk of T
H .first() is Element of the_Vertices_of T
H . 1 is set
X .vertices() is finite Element of K32((the_Vertices_of T))
K32((the_Vertices_of T)) is non empty-membered set
X .vertexSeq() is V7() V10( NAT ) V11( the_Vertices_of T) Function-like finite FinSequence-like FinSubsequence-like VertexSeq of T
K319((the_Vertices_of T),(X .vertexSeq())) is finite Element of K32((the_Vertices_of T))
H .vertices() is finite Element of K32((the_Vertices_of T))
H .vertexSeq() is V7() V10( NAT ) V11( the_Vertices_of T) Function-like finite FinSequence-like FinSubsequence-like VertexSeq of T
K319((the_Vertices_of T),(H .vertexSeq())) is finite Element of K32((the_Vertices_of T))
(X .vertices()) /\ (H .vertices()) is finite Element of K32((the_Vertices_of T))
{(X .last())} is non empty trivial finite 1 -element set
X .append H is non empty V7() V10( NAT ) V11((the_Vertices_of T) \/ (the_Edges_of T)) Function-like finite FinSequence-like FinSubsequence-like Walk of T
(X .append H) .first() is Element of the_Vertices_of T
(X .append H) . 1 is set
(X .append H) .last() is Element of the_Vertices_of T
len (X .append H) is non empty ordinal natural V27() ext-real positive non negative finite cardinal V73() V74() non even complex-membered ext-real-membered real-membered rational-membered integer-membered natural-membered V133() V134() V135() V136() V137() V139() Element of NAT
(X .append H) . (len (X .append H)) is set
X .first() is Element of the_Vertices_of T
X . 1 is set
H .last() is Element of the_Vertices_of T
len H is non empty ordinal natural V27() ext-real positive non negative finite cardinal V73() V74() non even complex-membered ext-real-membered real-membered rational-membered integer-membered natural-membered V133() V134() V135() V136() V137() V139() Element of NAT
H . (len H) is set
X .first() is Element of the_Vertices_of T
X . 1 is set
X .edges() is finite Element of K32((the_Edges_of T))
K32((the_Edges_of T)) is set
X .edgeSeq() is V7() V10( NAT ) V11( the_Edges_of T) Function-like finite FinSequence-like FinSubsequence-like EdgeSeq of T
K319((the_Edges_of T),(X .edgeSeq())) is finite Element of K32((the_Edges_of T))
H .edges() is finite Element of K32((the_Edges_of T))
H .edgeSeq() is V7() V10( NAT ) V11( the_Edges_of T) Function-like finite FinSequence-like FinSubsequence-like EdgeSeq of T
K319((the_Edges_of T),(H .edgeSeq())) is finite Element of K32((the_Edges_of T))
(X .edges()) /\ (H .edges()) is finite Element of K32((the_Edges_of T))
cH is set
len H is non empty ordinal natural V27() ext-real positive non negative finite cardinal V73() V74() non even complex-membered ext-real-membered real-membered rational-membered integer-membered natural-membered V133() V134() V135() V136() V137() V139() Element of NAT
mA is non empty ordinal natural V27() ext-real positive non negative finite cardinal V73() V74() non even complex-membered ext-real-membered real-membered rational-membered integer-membered natural-membered V133() V134() V135() V136() V137() V139() Element of NAT
mA + 2 is non empty ordinal natural V27() ext-real positive non negative finite cardinal V73() V74() non even complex-membered ext-real-membered real-membered rational-membered integer-membered natural-membered V133() V134() V135() V136() V137() V139() Element of NAT
A is Element of the_Vertices_of T
H . mA is set
mA + 1 is non empty ordinal natural V27() ext-real positive non negative finite cardinal V73() V74() even complex-membered ext-real-membered real-membered rational-membered integer-membered natural-membered V133() V134() V135() V136() V137() V139() Element of NAT
H . (mA + 1) is set
A is Element of the_Vertices_of T
H . (mA + 2) is set
C is non empty ordinal natural V27() ext-real positive non negative finite cardinal V73() V74() non even complex-membered ext-real-membered real-membered rational-membered integer-membered natural-membered V133() V134() V135() V136() V137() V139() Element of NAT
C + 2 is non empty ordinal natural V27() ext-real positive non negative finite cardinal V73() V74() non even complex-membered ext-real-membered real-membered rational-membered integer-membered natural-membered V133() V134() V135() V136() V137() V139() Element of NAT
cA is Element of the_Vertices_of T
X . C is set
C + 1 is non empty ordinal natural V27() ext-real positive non negative finite cardinal V73() V74() even complex-membered ext-real-membered real-membered rational-membered integer-membered natural-membered V133() V134() V135() V136() V137() V139() Element of NAT
X . (C + 1) is set
B is Element of the_Vertices_of T
X . (C + 2) is set
C + 0 is non empty ordinal natural V27() ext-real positive non negative finite cardinal V73() V74() complex-membered ext-real-membered real-membered rational-membered integer-membered natural-membered V133() V134() V135() V136() V137() V139() Element of NAT
{cA,B} is non empty finite set
mA + 0 is non empty ordinal natural V27() ext-real positive non negative finite cardinal V73() V74() complex-membered ext-real-membered real-membered rational-membered integer-membered natural-membered V133() V134() V135() V136() V137() V139() Element of NAT
{A,A} is non empty finite set
{(X .first()),(X .last())} is non empty finite set
T is V7() V10( NAT ) Function-like finite [Graph-like] set
the_Vertices_of T is non empty set
the_Edges_of T is set
(the_Vertices_of T) \/ (the_Edges_of T) is non empty set
X is non empty V7() V10( NAT ) V11((the_Vertices_of T) \/ (the_Edges_of T)) Function-like finite FinSequence-like FinSubsequence-like Trail-like Path-like Walk of T
X .last() is Element of the_Vertices_of T
len X is non empty ordinal natural V27() ext-real positive non negative finite cardinal V73() V74() non even complex-membered ext-real-membered real-membered rational-membered integer-membered natural-membered V133() V134() V135() V136() V137() V139() Element of NAT
X . (len X) is set
H is non empty V7() V10( NAT ) V11((the_Vertices_of T) \/ (the_Edges_of T)) Function-like finite FinSequence-like FinSubsequence-like Trail-like Path-like Walk of T
H .first() is Element of the_Vertices_of T
H . 1 is set
H .last() is Element of the_Vertices_of T
len H is non empty ordinal natural V27() ext-real positive non negative finite cardinal V73() V74() non even complex-membered ext-real-membered real-membered rational-membered integer-membered natural-membered V133() V134() V135() V136() V137() V139() Element of NAT
H . (len H) is set
X .first() is Element of the_Vertices_of T
X . 1 is set
X .edges() is finite Element of K32((the_Edges_of T))
K32((the_Edges_of T)) is set
X .edgeSeq() is V7() V10( NAT ) V11( the_Edges_of T) Function-like finite FinSequence-like FinSubsequence-like EdgeSeq of T
K319((the_Edges_of T),(X .edgeSeq())) is finite Element of K32((the_Edges_of T))
H .edges() is finite Element of K32((the_Edges_of T))
H .edgeSeq() is V7() V10( NAT ) V11( the_Edges_of T) Function-like finite FinSequence-like FinSubsequence-like EdgeSeq of T
K319((the_Edges_of T),(H .edgeSeq())) is finite Element of K32((the_Edges_of T))
X .vertices() is finite Element of K32((the_Vertices_of T))
K32((the_Vertices_of T)) is non empty-membered set
X .vertexSeq() is V7() V10( NAT ) V11( the_Vertices_of T) Function-like finite FinSequence-like FinSubsequence-like VertexSeq of T
K319((the_Vertices_of T),(X .vertexSeq())) is finite Element of K32((the_Vertices_of T))
H .vertices() is finite Element of K32((the_Vertices_of T))
H .vertexSeq() is V7() V10( NAT ) V11( the_Vertices_of T) Function-like finite FinSequence-like FinSubsequence-like VertexSeq of T
K319((the_Vertices_of T),(H .vertexSeq())) is finite Element of K32((the_Vertices_of T))
(X .vertices()) /\ (H .vertices()) is finite Element of K32((the_Vertices_of T))
{(X .last()),(X .first())} is non empty finite set
X .append H is non empty V7() V10( NAT ) V11((the_Vertices_of T) \/ (the_Edges_of T)) Function-like finite FinSequence-like FinSubsequence-like Walk of T
(X .append H) .first() is Element of the_Vertices_of T
(X .append H) . 1 is set
(X .append H) .last() is Element of the_Vertices_of T
len (X .append H) is non empty ordinal natural V27() ext-real positive non negative finite cardinal V73() V74() non even complex-membered ext-real-membered real-membered rational-membered integer-membered natural-membered V133() V134() V135() V136() V137() V139() Element of NAT
(X .append H) . (len (X .append H)) is set
T is V7() V10( NAT ) Function-like finite [Graph-like] loopless non-multi non-Dmulti simple Dsimple set
the_Vertices_of T is non empty set
the_Edges_of T is set
(the_Vertices_of T) \/ (the_Edges_of T) is non empty set
X is non empty V7() V10( NAT ) V11((the_Vertices_of T) \/ (the_Edges_of T)) Function-like finite FinSequence-like FinSubsequence-like Walk of T
len X is non empty ordinal natural V27() ext-real positive non negative finite cardinal V73() V74() non even complex-membered ext-real-membered real-membered rational-membered integer-membered natural-membered V133() V134() V135() V136() V137() V139() Element of NAT
H is non empty V7() V10( NAT ) V11((the_Vertices_of T) \/ (the_Edges_of T)) Function-like finite FinSequence-like FinSubsequence-like Walk of T
len H is non empty ordinal natural V27() ext-real positive non negative finite cardinal V73() V74() non even complex-membered ext-real-membered real-membered rational-membered integer-membered natural-membered V133() V134() V135() V136() V137() V139() Element of NAT
H9 is non empty ordinal natural V27() ext-real positive non negative finite cardinal V73() V74() non even set
cH is ordinal natural V27() ext-real non negative finite cardinal V73() V74() set
X . cH is set
H . cH is set
1 - 1 is V27() ext-real V73() V74() set
cH - 1 is V27() ext-real V73() V74() set
A is ordinal natural V27() ext-real non negative finite cardinal V73() V74() even set
A - 1 is non empty V27() ext-real V73() V74() non even set
A is non empty ordinal natural V27() ext-real positive non negative finite cardinal V73() V74() non even complex-membered ext-real-membered real-membered rational-membered integer-membered natural-membered V133() V134() V135() V136() V137() V139() Element of NAT
X . A is set
A + 2 is non empty ordinal natural V27() ext-real positive non negative finite cardinal V73() V74() non even complex-membered ext-real-membered real-membered rational-membered integer-membered natural-membered V133() V134() V135() V136() V137() V139() Element of NAT
X . (A + 2) is set
A + 1 is non empty ordinal natural V27() ext-real positive non negative finite cardinal V73() V74() even complex-membered ext-real-membered real-membered rational-membered integer-membered natural-membered V133() V134() V135() V136() V137() V139() Element of NAT
X . (A + 1) is set
(A + 1) + 1 is non empty ordinal natural V27() ext-real positive non negative finite cardinal V73() V74() non even complex-membered ext-real-membered real-membered rational-membered integer-membered natural-membered V133() V134() V135() V136() V137() V139() Element of NAT
H . (A + 2) is set
H . A is set
H . (A + 1) is set
T is V7() V10( NAT ) Function-like finite [Graph-like] set
the_Vertices_of T is non empty set
the_Edges_of T is set
(the_Vertices_of T) \/ (the_Edges_of T) is non empty set
X is non empty V7() V10( NAT ) V11((the_Vertices_of T) \/ (the_Edges_of T)) Function-like finite FinSequence-like FinSubsequence-like Walk of T
X .first() is Element of the_Vertices_of T
X . 1 is set
H is non empty V7() V10( NAT ) V11((the_Vertices_of T) \/ (the_Edges_of T)) Function-like finite FinSequence-like FinSubsequence-like Walk of T
H .first() is Element of the_Vertices_of T
H . 1 is set
(X,H) is V7() V10( NAT ) Function-like finite FinSequence-like FinSubsequence-like set
len (X,H) is ordinal natural V27() ext-real non negative finite cardinal V73() V74() complex-membered ext-real-membered real-membered rational-membered integer-membered natural-membered V135() V136() V137() V139() Element of NAT
(len (X,H)) - 1 is V27() ext-real V73() V74() set
cH is non empty ordinal natural V27() ext-real positive non negative finite cardinal V73() V74() non even complex-membered ext-real-membered real-membered rational-membered integer-membered natural-membered V133() V134() V135() V136() V137() V139() Element of NAT
(len (X,H)) + 1 is non empty ordinal natural V27() ext-real positive non negative finite cardinal V73() V74() complex-membered ext-real-membered real-membered rational-membered integer-membered natural-membered V133() V134() V135() V136() V137() V139() Element of NAT
X . ((len (X,H)) + 1) is set
<*(X . ((len (X,H)) + 1))*> is non empty trivial V7() V10( NAT ) Function-like constant finite 1 -element FinSequence-like FinSubsequence-like set
(X,H) ^ <*(X . ((len (X,H)) + 1))*> is non empty V7() V10( NAT ) Function-like finite FinSequence-like FinSubsequence-like set
len ((X,H) ^ <*(X . ((len (X,H)) + 1))*>) is non empty ordinal natural V27() ext-real positive non negative finite cardinal V73() V74() complex-membered ext-real-membered real-membered rational-membered integer-membered natural-membered V133() V134() V135() V136() V137() V139() Element of NAT
mA is set
dom ((X,H) ^ <*(X . ((len (X,H)) + 1))*>) is non empty finite complex-membered ext-real-membered real-membered rational-membered integer-membered natural-membered V133() V134() V135() V136() V137() Element of K32(NAT)
cA is ordinal natural V27() ext-real non negative finite cardinal V73() V74() set
dom (X,H) is finite complex-membered ext-real-membered real-membered rational-membered integer-membered natural-membered V135() V136() V137() Element of K32(NAT)
((X,H) ^ <*(X . ((len (X,H)) + 1))*>) . mA is set
(X,H) . mA is set
X . mA is set
((X,H) ^ <*(X . ((len (X,H)) + 1))*>) . mA is set
X . mA is set
cH + 1 is non empty ordinal natural V27() ext-real positive non negative finite cardinal V73() V74() even complex-membered ext-real-membered real-membered rational-membered integer-membered natural-membered V133() V134() V135() V136() V137() V139() Element of NAT
len H is non empty ordinal natural V27() ext-real positive non negative finite cardinal V73() V74() non even complex-membered ext-real-membered real-membered rational-membered integer-membered natural-membered V133() V134() V135() V136() V137() V139() Element of NAT
H . cH is set
cH + 2 is non empty ordinal natural V27() ext-real positive non negative finite cardinal V73() V74() non even complex-membered ext-real-membered real-membered rational-membered integer-membered natural-membered V133() V134() V135() V136() V137() V139() Element of NAT
H . (cH + 2) is set
H . (len (X,H)) is set
len X is non empty ordinal natural V27() ext-real positive non negative finite cardinal V73() V74() non even complex-membered ext-real-membered real-membered rational-membered integer-membered natural-membered V133() V134() V135() V136() V137() V139() Element of NAT
X . cH is set
X . (cH + 2) is set
X . (len (X,H)) is set
mA is set
cA is ordinal natural V27() ext-real non negative finite cardinal V73() V74() set
dom (X,H) is finite complex-membered ext-real-membered real-membered rational-membered integer-membered natural-membered V135() V136() V137() Element of K32(NAT)
((X,H) ^ <*(X . ((len (X,H)) + 1))*>) . mA is set
(X,H) . mA is set
H . mA is set
((X,H) ^ <*(X . ((len (X,H)) + 1))*>) . mA is set
H . mA is set
dom H is non empty finite complex-membered ext-real-membered real-membered rational-membered integer-membered natural-membered V133() V134() V135() V136() V137() Element of K32(NAT)
dom X is non empty finite complex-membered ext-real-membered real-membered rational-membered integer-membered natural-membered V133() V134() V135() V136() V137() Element of K32(NAT)
T is V7() V10( NAT ) Function-like finite [Graph-like] set
the_Vertices_of T is non empty set
the_Edges_of T is set
(the_Vertices_of T) \/ (the_Edges_of T) is non empty set
X is non empty V7() V10( NAT ) V11((the_Vertices_of T) \/ (the_Edges_of T)) Function-like finite FinSequence-like FinSubsequence-like Walk of T
X .first() is Element of the_Vertices_of T
X . 1 is set
H is non empty V7() V10( NAT ) V11((the_Vertices_of T) \/ (the_Edges_of T)) Function-like finite FinSequence-like FinSubsequence-like Walk of T
H .first() is Element of the_Vertices_of T
H . 1 is set
(X,H) is V7() V10( NAT ) Function-like finite FinSequence-like FinSubsequence-like set
len (X,H) is ordinal natural V27() ext-real non negative finite cardinal V73() V74() complex-membered ext-real-membered real-membered rational-membered integer-membered natural-membered V135() V136() V137() V139() Element of NAT
(len (X,H)) + 2 is non empty ordinal natural V27() ext-real positive non negative finite cardinal V73() V74() complex-membered ext-real-membered real-membered rational-membered integer-membered natural-membered V133() V134() V135() V136() V137() V139() Element of NAT
len X is non empty ordinal natural V27() ext-real positive non negative finite cardinal V73() V74() non even complex-membered ext-real-membered real-membered rational-membered integer-membered natural-membered V133() V134() V135() V136() V137() V139() Element of NAT
T is V7() V10( NAT ) Function-like finite [Graph-like] non-multi non-Dmulti set
the_Vertices_of T is non empty set
the_Edges_of T is set
(the_Vertices_of T) \/ (the_Edges_of T) is non empty set
X is non empty V7() V10( NAT ) V11((the_Vertices_of T) \/ (the_Edges_of T)) Function-like finite FinSequence-like FinSubsequence-like Walk of T
X .first() is Element of the_Vertices_of T
X . 1 is set
H is non empty V7() V10( NAT ) V11((the_Vertices_of T) \/ (the_Edges_of T)) Function-like finite FinSequence-like FinSubsequence-like Walk of T
H .first() is Element of the_Vertices_of T
H . 1 is set
(X,H) is V7() V10( NAT ) Function-like finite FinSequence-like FinSubsequence-like set
len (X,H) is ordinal natural V27() ext-real non negative finite cardinal V73() V74() complex-membered ext-real-membered real-membered rational-membered integer-membered natural-membered V135() V136() V137() V139() Element of NAT
(len (X,H)) + 2 is non empty ordinal natural V27() ext-real positive non negative finite cardinal V73() V74() complex-membered ext-real-membered real-membered rational-membered integer-membered natural-membered V133() V134() V135() V136() V137() V139() Element of NAT
X . ((len (X,H)) + 2) is set
H . ((len (X,H)) + 2) is set
len X is non empty ordinal natural V27() ext-real positive non negative finite cardinal V73() V74() non even complex-membered ext-real-membered real-membered rational-membered integer-membered natural-membered V133() V134() V135() V136() V137() V139() Element of NAT
X . (len (X,H)) is set
(len (X,H)) + 1 is non empty ordinal natural V27() ext-real positive non negative finite cardinal V73() V74() complex-membered ext-real-membered real-membered rational-membered integer-membered natural-membered V133() V134() V135() V136() V137() V139() Element of NAT
X . ((len (X,H)) + 1) is set
H . (len (X,H)) is set
len H is non empty ordinal natural V27() ext-real positive non negative finite cardinal V73() V74() non even complex-membered ext-real-membered real-membered rational-membered integer-membered natural-membered V133() V134() V135() V136() V137() V139() Element of NAT
H . ((len (X,H)) + 1) is set
T is V7() V10( NAT ) Function-like finite [Graph-like] loopless non-multi non-Dmulti simple Dsimple V118() V119() Tree-like set
the_Vertices_of T is non empty set
the_Edges_of T is set
(the_Vertices_of T) \/ (the_Edges_of T) is non empty set
X is non empty V7() V10( NAT ) V11((the_Vertices_of T) \/ (the_Edges_of T)) Function-like finite FinSequence-like FinSubsequence-like Walk of T
len X is non empty ordinal natural V27() ext-real positive non negative finite cardinal V73() V74() non even complex-membered ext-real-membered real-membered rational-membered integer-membered natural-membered V133() V134() V135() V136() V137() V139() Element of NAT
H9 is non empty ordinal natural V27() ext-real positive non negative finite cardinal V73() V74() non even complex-membered ext-real-membered real-membered rational-membered integer-membered natural-membered V133() V134() V135() V136() V137() V139() Element of NAT
H is non empty ordinal natural V27() ext-real positive non negative finite cardinal V73() V74() non even complex-membered ext-real-membered real-membered rational-membered integer-membered natural-membered V133() V134() V135() V136() V137() V139() Element of NAT
X . H is set
X . H9 is set
H is ordinal natural V27() ext-real non negative finite cardinal V73() V74() set
X . H is set
cH is non empty ordinal natural V27() ext-real positive non negative finite cardinal V73() V74() non even complex-membered ext-real-membered real-membered rational-membered integer-membered natural-membered V133() V134() V135() V136() V137() V139() Element of NAT
X . cH is set
cH is non empty ordinal natural V27() ext-real positive non negative finite cardinal V73() V74() non even complex-membered ext-real-membered real-membered rational-membered integer-membered natural-membered V133() V134() V135() V136() V137() V139() Element of NAT
X . cH is set
H9 is ordinal natural V27() ext-real non negative finite cardinal V73() V74() complex-membered ext-real-membered real-membered rational-membered integer-membered natural-membered V135() V136() V137() V139() Element of NAT
X .cut (cH,H9) is non empty V7() V10( NAT ) V11((the_Vertices_of T) \/ (the_Edges_of T)) Function-like finite FinSequence-like FinSubsequence-like Walk of T
len (X .cut (cH,H9)) is non empty ordinal natural V27() ext-real positive non negative finite cardinal V73() V74() non even complex-membered ext-real-membered real-membered rational-membered integer-membered natural-membered V133() V134() V135() V136() V137() V139() Element of NAT
(len (X .cut (cH,H9))) + cH is non empty ordinal natural V27() ext-real positive non negative finite cardinal V73() V74() even complex-membered ext-real-membered real-membered rational-membered integer-membered natural-membered V133() V134() V135() V136() V137() V139() Element of NAT
H9 + 1 is non empty ordinal natural V27() ext-real positive non negative finite cardinal V73() V74() complex-membered ext-real-membered real-membered rational-membered integer-membered natural-membered V133() V134() V135() V136() V137() V139() Element of NAT
A is non empty ordinal natural V27() ext-real positive non negative finite cardinal V73() V74() non even complex-membered ext-real-membered real-membered rational-membered integer-membered natural-membered V133() V134() V135() V136() V137() V139() Element of NAT
X . A is set
(X .cut (cH,H9)) .last() is Element of the_Vertices_of T
(X .cut (cH,H9)) . (len (X .cut (cH,H9))) is set
A is non empty ordinal natural V27() ext-real positive non negative finite cardinal V73() V74() non even complex-membered ext-real-membered real-membered rational-membered integer-membered natural-membered V133() V134() V135() V136() V137() V139() Element of NAT
X . A is set
mA is non empty ordinal natural V27() ext-real positive non negative finite cardinal V73() V74() non even complex-membered ext-real-membered real-membered rational-membered integer-membered natural-membered V133() V134() V135() V136() V137() V139() Element of NAT
A is non empty ordinal natural V27() ext-real positive non negative finite cardinal V73() V74() non even complex-membered ext-real-membered real-membered rational-membered integer-membered natural-membered V133() V134() V135() V136() V137() V139() Element of NAT
(X .cut (cH,H9)) . A is set
(X .cut (cH,H9)) . mA is set
cH + mA is non empty ordinal natural V27() ext-real positive non negative finite cardinal V73() V74() even complex-membered ext-real-membered real-membered rational-membered integer-membered natural-membered V133() V134() V135() V136() V137() V139() Element of NAT
(cH + mA) - 1 is non empty V27() ext-real V73() V74() non even set
cA is non empty ordinal natural V27() ext-real positive non negative finite cardinal V73() V74() non even complex-membered ext-real-membered real-membered rational-membered integer-membered natural-membered V133() V134() V135() V136() V137() V139() Element of NAT
X . cA is set
cA is non empty ordinal natural V27() ext-real positive non negative finite cardinal V73() V74() non even set
X . cA is set
cH + A is non empty ordinal natural V27() ext-real positive non negative finite cardinal V73() V74() even complex-membered ext-real-membered real-membered rational-membered integer-membered natural-membered V133() V134() V135() V136() V137() V139() Element of NAT
(cH + A) - 1 is non empty V27() ext-real V73() V74() non even set
C is non empty ordinal natural V27() ext-real positive non negative finite cardinal V73() V74() non even complex-membered ext-real-membered real-membered rational-membered integer-membered natural-membered V133() V134() V135() V136() V137() V139() Element of NAT
X . C is set
C is non empty ordinal natural V27() ext-real positive non negative finite cardinal V73() V74() non even set
X . C is set
cH + (len (X .cut (cH,H9))) is non empty ordinal natural V27() ext-real positive non negative finite cardinal V73() V74() even complex-membered ext-real-membered real-membered rational-membered integer-membered natural-membered V133() V134() V135() V136() V137() V139() Element of NAT
H + 1 is non empty ordinal natural V27() ext-real positive non negative finite cardinal V73() V74() complex-membered ext-real-membered real-membered rational-membered integer-membered natural-membered V133() V134() V135() V136() V137() V139() Element of NAT
B is non empty ordinal natural V27() ext-real positive non negative finite cardinal V73() V74() non even complex-membered ext-real-membered real-membered rational-membered integer-membered natural-membered V133() V134() V135() V136() V137() V139() Element of NAT
X . B is set
B is non empty ordinal natural V27() ext-real positive non negative finite cardinal V73() V74() non even complex-membered ext-real-membered real-membered rational-membered integer-membered natural-membered V133() V134() V135() V136() V137() V139() Element of NAT
mC is non empty ordinal natural V27() ext-real positive non negative finite cardinal V73() V74() non even complex-membered ext-real-membered real-membered rational-membered integer-membered natural-membered V133() V134() V135() V136() V137() V139() Element of NAT
H + 1 is non empty ordinal natural V27() ext-real positive non negative finite cardinal V73() V74() complex-membered ext-real-membered real-membered rational-membered integer-membered natural-membered V133() V134() V135() V136() V137() V139() Element of NAT
B is non empty ordinal natural V27() ext-real positive non negative finite cardinal V73() V74() non even complex-membered ext-real-membered real-membered rational-membered integer-membered natural-membered V133() V134() V135() V136() V137() V139() Element of NAT
X . B is set
mC is non empty ordinal natural V27() ext-real positive non negative finite cardinal V73() V74() non even complex-membered ext-real-membered real-membered rational-membered integer-membered natural-membered V133() V134() V135() V136() V137() V139() Element of NAT
cH + 1 is non empty ordinal natural V27() ext-real positive non negative finite cardinal V73() V74() even complex-membered ext-real-membered real-membered rational-membered integer-membered natural-membered V133() V134() V135() V136() V137() V139() Element of NAT
(X .cut (cH,H9)) .first() is Element of the_Vertices_of T
(X .cut (cH,H9)) . 1 is set
A is non empty ordinal natural V27() ext-real positive non negative finite cardinal V73() V74() non even complex-membered ext-real-membered real-membered rational-membered integer-membered natural-membered V133() V134() V135() V136() V137() V139() Element of NAT
X . A is set
T is V7() V10( NAT ) Function-like finite [Graph-like] loopless non-multi non-Dmulti simple Dsimple V118() V119() Tree-like set
the_Vertices_of T is non empty set
the_Edges_of T is set
(the_Vertices_of T) \/ (the_Edges_of T) is non empty set
X is non empty V7() V10( NAT ) V11((the_Vertices_of T) \/ (the_Edges_of T)) Function-like finite FinSequence-like FinSubsequence-like Trail-like Path-like Walk of T
T is V7() V10( NAT ) Function-like finite [Graph-like] loopless non-multi non-Dmulti simple Dsimple V118() V119() Tree-like set
the_Vertices_of T is non empty set
the_Edges_of T is set
(the_Vertices_of T) \/ (the_Edges_of T) is non empty set
X is non empty V7() V10( NAT ) V11((the_Vertices_of T) \/ (the_Edges_of T)) Function-like finite FinSequence-like FinSubsequence-like Trail-like Path-like Walk of T
T is V7() V10( NAT ) Function-like finite [Graph-like] loopless non-multi non-Dmulti simple Dsimple V118() V119() Tree-like set
the_Vertices_of T is non empty set
the_Edges_of T is set
(the_Vertices_of T) \/ (the_Edges_of T) is non empty set
X is non empty V7() V10( NAT ) V11((the_Vertices_of T) \/ (the_Edges_of T)) Function-like finite FinSequence-like FinSubsequence-like Trail-like Path-like Walk of T
len X is non empty ordinal natural V27() ext-real positive non negative finite cardinal V73() V74() non even complex-membered ext-real-membered real-membered rational-membered integer-membered natural-membered V133() V134() V135() V136() V137() V139() Element of NAT
H9 is non empty ordinal natural V27() ext-real positive non negative finite cardinal V73() V74() non even set
H is non empty ordinal natural V27() ext-real positive non negative finite cardinal V73() V74() non even set
X . H is set
X . H9 is set
A is non empty ordinal natural V27() ext-real positive non negative finite cardinal V73() V74() non even complex-membered ext-real-membered real-membered rational-membered integer-membered natural-membered V133() V134() V135() V136() V137() V139() Element of NAT
cH is non empty ordinal natural V27() ext-real positive non negative finite cardinal V73() V74() non even complex-membered ext-real-membered real-membered rational-membered integer-membered natural-membered V133() V134() V135() V136() V137() V139() Element of NAT
X .first() is Element of the_Vertices_of T
X . 1 is set
X .last() is Element of the_Vertices_of T
X . (len X) is set
T is V7() V10( NAT ) Function-like finite [Graph-like] loopless non-multi non-Dmulti simple Dsimple V118() V119() Tree-like set
the_Vertices_of T is non empty set
the_Edges_of T is set
(the_Vertices_of T) \/ (the_Edges_of T) is non empty set
X is Element of the_Vertices_of T
H is Element of the_Vertices_of T
H9 is non empty V7() V10( NAT ) V11((the_Vertices_of T) \/ (the_Edges_of T)) Function-like finite FinSequence-like FinSubsequence-like Trail-like Path-like Walk of T
cH is non empty V7() V10( NAT ) V11((the_Vertices_of T) \/ (the_Edges_of T)) Function-like finite FinSequence-like FinSubsequence-like Trail-like Path-like Walk of T
(H9,cH) is V7() V10( NAT ) Function-like finite FinSequence-like FinSubsequence-like set
len (H9,cH) is ordinal natural V27() ext-real non negative finite cardinal V73() V74() complex-membered ext-real-membered real-membered rational-membered integer-membered natural-membered V135() V136() V137() V139() Element of NAT
H9 .first() is Element of the_Vertices_of T
H9 . 1 is set
cH .first() is Element of the_Vertices_of T
cH . 1 is set
A is non empty ordinal natural V27() ext-real positive non negative finite cardinal V73() V74() non even complex-membered ext-real-membered real-membered rational-membered integer-membered natural-membered V133() V134() V135() V136() V137() V139() Element of NAT
len cH is non empty ordinal natural V27() ext-real positive non negative finite cardinal V73() V74() non even complex-membered ext-real-membered real-membered rational-membered integer-membered natural-membered V133() V134() V135() V136() V137() V139() Element of NAT
H9 .vertices() is finite Element of K32((the_Vertices_of T))
K32((the_Vertices_of T)) is non empty-membered set
H9 .vertexSeq() is V7() V10( NAT ) V11( the_Vertices_of T) Function-like finite FinSequence-like FinSubsequence-like VertexSeq of T
K319((the_Vertices_of T),(H9 .vertexSeq())) is finite Element of K32((the_Vertices_of T))
len H9 is non empty ordinal natural V27() ext-real positive non negative finite cardinal V73() V74() non even complex-membered ext-real-membered real-membered rational-membered integer-membered natural-membered V133() V134() V135() V136() V137() V139() Element of NAT
dom cH is non empty finite complex-membered ext-real-membered real-membered rational-membered integer-membered natural-membered V133() V134() V135() V136() V137() Element of K32(NAT)
cH . (len cH) is set
H9 . (len cH) is set
H9 . (len H9) is set
H9 .last() is Element of the_Vertices_of T
cH .last() is Element of the_Vertices_of T
mA is non empty ordinal natural V27() ext-real positive non negative finite cardinal V73() V74() non even complex-membered ext-real-membered real-membered rational-membered integer-membered natural-membered V133() V134() V135() V136() V137() V139() Element of NAT
cH . mA is set
A + 2 is non empty ordinal natural V27() ext-real positive non negative finite cardinal V73() V74() non even complex-membered ext-real-membered real-membered rational-membered integer-membered natural-membered V133() V134() V135() V136() V137() V139() Element of NAT
cH .last() is Element of the_Vertices_of T
cH . (len cH) is set
H9 .last() is Element of the_Vertices_of T
len H9 is non empty ordinal natural V27() ext-real positive non negative finite cardinal V73() V74() non even complex-membered ext-real-membered real-membered rational-membered integer-membered natural-membered V133() V134() V135() V136() V137() V139() Element of NAT
H9 . (len H9) is set
mA is ordinal natural V27() ext-real non negative finite cardinal V73() V74() set
cH . mA is set
cA is non empty ordinal natural V27() ext-real positive non negative finite cardinal V73() V74() non even complex-membered ext-real-membered real-membered rational-membered integer-membered natural-membered V133() V134() V135() V136() V137() V139() Element of NAT
cH . cA is set
H9 .find (cH . cA) is non empty ordinal natural V27() ext-real positive non negative finite cardinal V73() V74() non even complex-membered ext-real-membered real-membered rational-membered integer-membered natural-membered V133() V134() V135() V136() V137() V139() Element of NAT
cH .cut (A,cA) is non empty V7() V10( NAT ) V11((the_Vertices_of T) \/ (the_Edges_of T)) Function-like finite FinSequence-like FinSubsequence-like Trail-like Path-like Walk of T
H9 .cut (A,(H9 .find (cH . cA))) is non empty V7() V10( NAT ) V11((the_Vertices_of T) \/ (the_Edges_of T)) Function-like finite FinSequence-like FinSubsequence-like Trail-like Path-like Walk of T
len H9 is non empty ordinal natural V27() ext-real positive non negative finite cardinal V73() V74() non even complex-membered ext-real-membered real-membered rational-membered integer-membered natural-membered V133() V134() V135() V136() V137() V139() Element of NAT
(H9 .cut (A,(H9 .find (cH . cA)))) .reverse() is non empty V7() V10( NAT ) V11((the_Vertices_of T) \/ (the_Edges_of T)) Function-like finite FinSequence-like FinSubsequence-like Trail-like Path-like Walk of T
((H9 .cut (A,(H9 .find (cH . cA)))) .reverse()) .vertices() is finite Element of K32((the_Vertices_of T))
((H9 .cut (A,(H9 .find (cH . cA)))) .reverse()) .vertexSeq() is V7() V10( NAT ) V11( the_Vertices_of T) Function-like finite FinSequence-like FinSubsequence-like VertexSeq of T
K319((the_Vertices_of T),(((H9 .cut (A,(H9 .find (cH . cA)))) .reverse()) .vertexSeq())) is finite Element of K32((the_Vertices_of T))
(H9 .cut (A,(H9 .find (cH . cA)))) .vertices() is finite Element of K32((the_Vertices_of T))
(H9 .cut (A,(H9 .find (cH . cA)))) .vertexSeq() is V7() V10( NAT ) V11( the_Vertices_of T) Function-like finite FinSequence-like FinSubsequence-like VertexSeq of T
K319((the_Vertices_of T),((H9 .cut (A,(H9 .find (cH . cA)))) .vertexSeq())) is finite Element of K32((the_Vertices_of T))
(cH .cut (A,cA)) .append ((H9 .cut (A,(H9 .find (cH . cA)))) .reverse()) is non empty V7() V10( NAT ) V11((the_Vertices_of T) \/ (the_Edges_of T)) Function-like finite FinSequence-like FinSubsequence-like Walk of T
H9 . A is set
cH . A is set
(cH .cut (A,cA)) .first() is Element of the_Vertices_of T
(cH .cut (A,cA)) . 1 is set
H9 . (H9 .find (cH . cA)) is set
cH . (H9 .find (cH . cA)) is set
cH .last() is Element of the_Vertices_of T
cH . (len cH) is set
(cH .cut (A,cA)) .vertices() is finite Element of K32((the_Vertices_of T))
(cH .cut (A,cA)) .vertexSeq() is V7() V10( NAT ) V11( the_Vertices_of T) Function-like finite FinSequence-like FinSubsequence-like VertexSeq of T
K319((the_Vertices_of T),((cH .cut (A,cA)) .vertexSeq())) is finite Element of K32((the_Vertices_of T))
((cH .cut (A,cA)) .vertices()) /\ (((H9 .cut (A,(H9 .find (cH . cA)))) .reverse()) .vertices()) is finite Element of K32((the_Vertices_of T))
{(cH . cA),(H9 . A)} is non empty finite set
c is set
len (cH .cut (A,cA)) is non empty ordinal natural V27() ext-real positive non negative finite cardinal V73() V74() non even complex-membered ext-real-membered real-membered rational-membered integer-membered natural-membered V133() V134() V135() V136() V137() V139() Element of NAT
cc is non empty ordinal natural V27() ext-real positive non negative finite cardinal V73() V74() non even complex-membered ext-real-membered real-membered rational-membered integer-membered natural-membered V133() V134() V135() V136() V137() V139() Element of NAT
(cH .cut (A,cA)) . cc is set
A + cc is non empty ordinal natural V27() ext-real positive non negative finite cardinal V73() V74() even complex-membered ext-real-membered real-membered rational-membered integer-membered natural-membered V133() V134() V135() V136() V137() V139() Element of NAT
(A + cc) - 1 is non empty V27() ext-real V73() V74() non even set
aa is non empty ordinal natural V27() ext-real positive non negative finite cardinal V73() V74() non even set
cH . aa is set
bb is non empty ordinal natural V27() ext-real positive non negative finite cardinal V73() V74() non even complex-membered ext-real-membered real-membered rational-membered integer-membered natural-membered V133() V134() V135() V136() V137() V139() Element of NAT
(len (cH .cut (A,cA))) + A is non empty ordinal natural V27() ext-real positive non negative finite cardinal V73() V74() even complex-membered ext-real-membered real-membered rational-membered integer-membered natural-membered V133() V134() V135() V136() V137() V139() Element of NAT
cA + 1 is non empty ordinal natural V27() ext-real positive non negative finite cardinal V73() V74() even complex-membered ext-real-membered real-membered rational-membered integer-membered natural-membered V133() V134() V135() V136() V137() V139() Element of NAT
(cH .cut (A,cA)) .last() is Element of the_Vertices_of T
(cH .cut (A,cA)) . (len (cH .cut (A,cA))) is set
bb + 1 is non empty ordinal natural V27() ext-real positive non negative finite cardinal V73() V74() even complex-membered ext-real-membered real-membered rational-membered integer-membered natural-membered V133() V134() V135() V136() V137() V139() Element of NAT
bb + 1 is non empty ordinal natural V27() ext-real positive non negative finite cardinal V73() V74() even complex-membered ext-real-membered real-membered rational-membered integer-membered natural-membered V133() V134() V135() V136() V137() V139() Element of NAT
(cH .cut (A,cA)) .last() is Element of the_Vertices_of T
len (cH .cut (A,cA)) is non empty ordinal natural V27() ext-real positive non negative finite cardinal V73() V74() non even complex-membered ext-real-membered real-membered rational-membered integer-membered natural-membered V133() V134() V135() V136() V137() V139() Element of NAT
(cH .cut (A,cA)) . (len (cH .cut (A,cA))) is set
(H9 .cut (A,(H9 .find (cH . cA)))) .first() is Element of the_Vertices_of T
(H9 .cut (A,(H9 .find (cH . cA)))) . 1 is set
((H9 .cut (A,(H9 .find (cH . cA)))) .reverse()) .last() is Element of the_Vertices_of T
len ((H9 .cut (A,(H9 .find (cH . cA)))) .reverse()) is non empty ordinal natural V27() ext-real positive non negative finite cardinal V73() V74() non even complex-membered ext-real-membered real-membered rational-membered integer-membered natural-membered V133() V134() V135() V136() V137() V139() Element of NAT
((H9 .cut (A,(H9 .find (cH . cA)))) .reverse()) . (len ((H9 .cut (A,(H9 .find (cH . cA)))) .reverse())) is set
(H9 .cut (A,(H9 .find (cH . cA)))) .last() is Element of the_Vertices_of T
len (H9 .cut (A,(H9 .find (cH . cA)))) is non empty ordinal natural V27() ext-real positive non negative finite cardinal V73() V74() non even complex-membered ext-real-membered real-membered rational-membered integer-membered natural-membered V133() V134() V135() V136() V137() V139() Element of NAT
(H9 .cut (A,(H9 .find (cH . cA)))) . (len (H9 .cut (A,(H9 .find (cH . cA))))) is set
((H9 .cut (A,(H9 .find (cH . cA)))) .reverse()) .first() is Element of the_Vertices_of T
((H9 .cut (A,(H9 .find (cH . cA)))) .reverse()) . 1 is set
c is set
dom H9 is non empty finite complex-membered ext-real-membered real-membered rational-membered integer-membered natural-membered V133() V134() V135() V136() V137() Element of K32(NAT)
H9 . (len H9) is set
cH . (len H9) is set
cH . (len cH) is set
cH .last() is Element of the_Vertices_of T
H9 .last() is Element of the_Vertices_of T
(cH .cut (A,cA)) .edges() is finite Element of K32((the_Edges_of T))
K32((the_Edges_of T)) is set
(cH .cut (A,cA)) .edgeSeq() is V7() V10( NAT ) V11( the_Edges_of T) Function-like finite FinSequence-like FinSubsequence-like EdgeSeq of T
K319((the_Edges_of T),((cH .cut (A,cA)) .edgeSeq())) is finite Element of K32((the_Edges_of T))
((H9 .cut (A,(H9 .find (cH . cA)))) .reverse()) .edges() is finite Element of K32((the_Edges_of T))
((H9 .cut (A,(H9 .find (cH . cA)))) .reverse()) .edgeSeq() is V7() V10( NAT ) V11( the_Edges_of T) Function-like finite FinSequence-like FinSubsequence-like EdgeSeq of T
K319((the_Edges_of T),(((H9 .cut (A,(H9 .find (cH . cA)))) .reverse()) .edgeSeq())) is finite Element of K32((the_Edges_of T))
(H9 .cut (A,(H9 .find (cH . cA)))) .edges() is finite Element of K32((the_Edges_of T))
(H9 .cut (A,(H9 .find (cH . cA)))) .edgeSeq() is V7() V10( NAT ) V11( the_Edges_of T) Function-like finite FinSequence-like FinSubsequence-like EdgeSeq of T
K319((the_Edges_of T),((H9 .cut (A,(H9 .find (cH . cA)))) .edgeSeq())) is finite Element of K32((the_Edges_of T))
((cH .cut (A,cA)) .edges()) /\ (((H9 .cut (A,(H9 .find (cH . cA)))) .reverse()) .edges()) is finite Element of K32((the_Edges_of T))
c is set
bb is non empty ordinal natural V27() ext-real positive non negative finite cardinal V73() V74() non even complex-membered ext-real-membered real-membered rational-membered integer-membered natural-membered V133() V134() V135() V136() V137() V139() Element of NAT
bb + 2 is non empty ordinal natural V27() ext-real positive non negative finite cardinal V73() V74() non even complex-membered ext-real-membered real-membered rational-membered integer-membered natural-membered V133() V134() V135() V136() V137() V139() Element of NAT
cc is Element of the_Vertices_of T
(H9 .cut (A,(H9 .find (cH . cA)))) . bb is set
bb + 1 is non empty ordinal natural V27() ext-real positive non negative finite cardinal V73() V74() even complex-membered ext-real-membered real-membered rational-membered integer-membered natural-membered V133() V134() V135() V136() V137() V139() Element of NAT
(H9 .cut (A,(H9 .find (cH . cA)))) . (bb + 1) is set
aa is Element of the_Vertices_of T
(H9 .cut (A,(H9 .find (cH . cA)))) . (bb + 2) is set
c is non empty ordinal natural V27() ext-real positive non negative finite cardinal V73() V74() non even complex-membered ext-real-membered real-membered rational-membered integer-membered natural-membered V133() V134() V135() V136() V137() V139() Element of NAT
c + 2 is non empty ordinal natural V27() ext-real positive non negative finite cardinal V73() V74() non even complex-membered ext-real-membered real-membered rational-membered integer-membered natural-membered V133() V134() V135() V136() V137() V139() Element of NAT
a is Element of the_Vertices_of T
(cH .cut (A,cA)) . c is set
c + 1 is non empty ordinal natural V27() ext-real positive non negative finite cardinal V73() V74() even complex-membered ext-real-membered real-membered rational-membered integer-membered natural-membered V133() V134() V135() V136() V137() V139() Element of NAT
(cH .cut (A,cA)) . (c + 1) is set
b is Element of the_Vertices_of T
(cH .cut (A,cA)) . (c + 2) is set
c + 0 is non empty ordinal natural V27() ext-real positive non negative finite cardinal V73() V74() complex-membered ext-real-membered real-membered rational-membered integer-membered natural-membered V133() V134() V135() V136() V137() V139() Element of NAT
(c + 1) + 1 is non empty ordinal natural V27() ext-real positive non negative finite cardinal V73() V74() non even complex-membered ext-real-membered real-membered rational-membered integer-membered natural-membered V133() V134() V135() V136() V137() V139() Element of NAT
A + (c + 1) is non empty ordinal natural V27() ext-real positive non negative finite cardinal V73() V74() non even complex-membered ext-real-membered real-membered rational-membered integer-membered natural-membered V133() V134() V135() V136() V137() V139() Element of NAT
cH . (A + (c + 1)) is set
s is ordinal natural V27() ext-real non negative finite cardinal V73() V74() set
s + 1 is non empty ordinal natural V27() ext-real positive non negative finite cardinal V73() V74() complex-membered ext-real-membered real-membered rational-membered integer-membered natural-membered V133() V134() V135() V136() V137() V139() Element of NAT
bb + 0 is non empty ordinal natural V27() ext-real positive non negative finite cardinal V73() V74() complex-membered ext-real-membered real-membered rational-membered integer-membered natural-membered V133() V134() V135() V136() V137() V139() Element of NAT
{cc,aa} is non empty finite set
(bb + 1) + 1 is non empty ordinal natural V27() ext-real positive non negative finite cardinal V73() V74() non even complex-membered ext-real-membered real-membered rational-membered integer-membered natural-membered V133() V134() V135() V136() V137() V139() Element of NAT
A + (bb + 1) is non empty ordinal natural V27() ext-real positive non negative finite cardinal V73() V74() non even complex-membered ext-real-membered real-membered rational-membered integer-membered natural-membered V133() V134() V135() V136() V137() V139() Element of NAT
H9 . (A + (bb + 1)) is set
{a,b} is non empty finite set
ni is ordinal natural V27() ext-real non negative finite cardinal V73() V74() complex-membered ext-real-membered real-membered rational-membered integer-membered natural-membered V135() V136() V137() V139() Element of NAT
A + ni is non empty ordinal natural V27() ext-real positive non negative finite cardinal V73() V74() complex-membered ext-real-membered real-membered rational-membered integer-membered natural-membered V133() V134() V135() V136() V137() V139() Element of NAT
cH . (A + ni) is set
A + 2 is non empty ordinal natural V27() ext-real positive non negative finite cardinal V73() V74() non even complex-membered ext-real-membered real-membered rational-membered integer-membered natural-membered V133() V134() V135() V136() V137() V139() Element of NAT
cH . (A + 2) is set
A + (c + 2) is non empty ordinal natural V27() ext-real positive non negative finite cardinal V73() V74() even complex-membered ext-real-membered real-membered rational-membered integer-membered natural-membered V133() V134() V135() V136() V137() V139() Element of NAT
(len (cH .cut (A,cA))) + A is non empty ordinal natural V27() ext-real positive non negative finite cardinal V73() V74() even complex-membered ext-real-membered real-membered rational-membered integer-membered natural-membered V133() V134() V135() V136() V137() V139() Element of NAT
A + c is non empty ordinal natural V27() ext-real positive non negative finite cardinal V73() V74() even complex-membered ext-real-membered real-membered rational-membered integer-membered natural-membered V133() V134() V135() V136() V137() V139() Element of NAT
(A + c) + 1 is non empty ordinal natural V27() ext-real positive non negative finite cardinal V73() V74() non even complex-membered ext-real-membered real-membered rational-membered integer-membered natural-membered V133() V134() V135() V136() V137() V139() Element of NAT
((A + c) + 1) + 1 is non empty ordinal natural V27() ext-real positive non negative finite cardinal V73() V74() even complex-membered ext-real-membered real-membered rational-membered integer-membered natural-membered V133() V134() V135() V136() V137() V139() Element of NAT
cA + 1 is non empty ordinal natural V27() ext-real positive non negative finite cardinal V73() V74() even complex-membered ext-real-membered real-membered rational-membered integer-membered natural-membered V133() V134() V135() V136() V137() V139() Element of NAT
cH .last() is Element of the_Vertices_of T
cH . (len cH) is set
(len (cH .cut (A,cA))) + A is non empty ordinal natural V27() ext-real positive non negative finite cardinal V73() V74() even complex-membered ext-real-membered real-membered rational-membered integer-membered natural-membered V133() V134() V135() V136() V137() V139() Element of NAT
cA + 1 is non empty ordinal natural V27() ext-real positive non negative finite cardinal V73() V74() even complex-membered ext-real-membered real-membered rational-membered integer-membered natural-membered V133() V134() V135() V136() V137() V139() Element of NAT
im is ordinal natural V27() ext-real non negative finite cardinal V73() V74() even complex-membered ext-real-membered real-membered rational-membered integer-membered natural-membered V135() V136() V137() V139() Element of NAT
A + im is non empty ordinal natural V27() ext-real positive non negative finite cardinal V73() V74() non even complex-membered ext-real-membered real-membered rational-membered integer-membered natural-membered V133() V134() V135() V136() V137() V139() Element of NAT
A + 0 is non empty ordinal natural V27() ext-real positive non negative finite cardinal V73() V74() complex-membered ext-real-membered real-membered rational-membered integer-membered natural-membered V133() V134() V135() V136() V137() V139() Element of NAT
cH .last() is Element of the_Vertices_of T
cH . (len cH) is set
im is ordinal natural V27() ext-real non negative finite cardinal V73() V74() set
im + 1 is non empty ordinal natural V27() ext-real positive non negative finite cardinal V73() V74() complex-membered ext-real-membered real-membered rational-membered integer-membered natural-membered V133() V134() V135() V136() V137() V139() Element of NAT
im is ordinal natural V27() ext-real non negative finite cardinal V73() V74() complex-membered ext-real-membered real-membered rational-membered integer-membered natural-membered V135() V136() V137() V139() Element of NAT
A + im is non empty ordinal natural V27() ext-real positive non negative finite cardinal V73() V74() complex-membered ext-real-membered real-membered rational-membered integer-membered natural-membered V133() V134() V135() V136() V137() V139() Element of NAT
H9 . (A + im) is set
H9 . (A + 2) is set
A + (bb + 2) is non empty ordinal natural V27() ext-real positive non negative finite cardinal V73() V74() even complex-membered ext-real-membered real-membered rational-membered integer-membered natural-membered V133() V134() V135() V136() V137() V139() Element of NAT
(len (H9 .cut (A,(H9 .find (cH . cA))))) + A is non empty ordinal natural V27() ext-real positive non negative finite cardinal V73() V74() even complex-membered ext-real-membered real-membered rational-membered integer-membered natural-membered V133() V134() V135() V136() V137() V139() Element of NAT
A + bb is non empty ordinal natural V27() ext-real positive non negative finite cardinal V73() V74() even complex-membered ext-real-membered real-membered rational-membered integer-membered natural-membered V133() V134() V135() V136() V137() V139() Element of NAT
(A + bb) + 1 is non empty ordinal natural V27() ext-real positive non negative finite cardinal V73() V74() non even complex-membered ext-real-membered real-membered rational-membered integer-membered natural-membered V133() V134() V135() V136() V137() V139() Element of NAT
((A + bb) + 1) + 1 is non empty ordinal natural V27() ext-real positive non negative finite cardinal V73() V74() even complex-membered ext-real-membered real-membered rational-membered integer-membered natural-membered V133() V134() V135() V136() V137() V139() Element of NAT
(H9 .find (cH . cA)) + 1 is non empty ordinal natural V27() ext-real positive non negative finite cardinal V73() V74() even complex-membered ext-real-membered real-membered rational-membered integer-membered natural-membered V133() V134() V135() V136() V137() V139() Element of NAT
H9 .last() is Element of the_Vertices_of T
H9 . (len H9) is set
(len (H9 .cut (A,(H9 .find (cH . cA))))) + A is non empty ordinal natural V27() ext-real positive non negative finite cardinal V73() V74() even complex-membered ext-real-membered real-membered rational-membered integer-membered natural-membered V133() V134() V135() V136() V137() V139() Element of NAT
(H9 .find (cH . cA)) + 1 is non empty ordinal natural V27() ext-real positive non negative finite cardinal V73() V74() even complex-membered ext-real-membered real-membered rational-membered integer-membered natural-membered V133() V134() V135() V136() V137() V139() Element of NAT
im is ordinal natural V27() ext-real non negative finite cardinal V73() V74() even complex-membered ext-real-membered real-membered rational-membered integer-membered natural-membered V135() V136() V137() V139() Element of NAT
A + im is non empty ordinal natural V27() ext-real positive non negative finite cardinal V73() V74() non even complex-membered ext-real-membered real-membered rational-membered integer-membered natural-membered V133() V134() V135() V136() V137() V139() Element of NAT
A + 0 is non empty ordinal natural V27() ext-real positive non negative finite cardinal V73() V74() complex-membered ext-real-membered real-membered rational-membered integer-membered natural-membered V133() V134() V135() V136() V137() V139() Element of NAT
H9 .last() is Element of the_Vertices_of T
H9 . (len H9) is set
T is V7() V10( NAT ) Function-like finite [Graph-like] loopless non-multi non-Dmulti simple Dsimple V118() V119() Tree-like set
the_Vertices_of T is non empty set
the_Edges_of T is set
(the_Vertices_of T) \/ (the_Edges_of T) is non empty set
X is Element of the_Vertices_of T
H is Element of the_Vertices_of T
H9 is non empty V7() V10( NAT ) V11((the_Vertices_of T) \/ (the_Edges_of T)) Function-like finite FinSequence-like FinSubsequence-like Walk of T
the non empty V7() V10( NAT ) V11((the_Vertices_of T) \/ (the_Edges_of T)) Function-like finite FinSequence-like FinSubsequence-like Trail-like Path-like Subwalk of H9 is non empty V7() V10( NAT ) V11((the_Vertices_of T) \/ (the_Edges_of T)) Function-like finite FinSequence-like FinSubsequence-like Trail-like Path-like Subwalk of H9
H9 .first() is Element of the_Vertices_of T
H9 . 1 is set
H9 .last() is Element of the_Vertices_of T
len H9 is non empty ordinal natural V27() ext-real positive non negative finite cardinal V73() V74() non even complex-membered ext-real-membered real-membered rational-membered integer-membered natural-membered V133() V134() V135() V136() V137() V139() Element of NAT
H9 . (len H9) is set
H9 is non empty V7() V10( NAT ) V11((the_Vertices_of T) \/ (the_Edges_of T)) Function-like finite FinSequence-like FinSubsequence-like Trail-like Path-like Walk of T
cH is non empty V7() V10( NAT ) V11((the_Vertices_of T) \/ (the_Edges_of T)) Function-like finite FinSequence-like FinSubsequence-like Trail-like Path-like Walk of T
T is V7() V10( NAT ) Function-like finite [Graph-like] loopless non-multi non-Dmulti simple Dsimple V118() V119() Tree-like set
the_Vertices_of T is non empty set
X is Element of the_Vertices_of T
H is Element of the_Vertices_of T
(T,X,H) is non empty V7() V10( NAT ) V11((the_Vertices_of T) \/ (the_Edges_of T)) Function-like finite FinSequence-like FinSubsequence-like Trail-like Path-like Walk of T
the_Edges_of T is set
(the_Vertices_of T) \/ (the_Edges_of T) is non empty set
(T,X,H) .first() is Element of the_Vertices_of T
(T,X,H) . 1 is set
(T,X,H) .last() is Element of the_Vertices_of T
len (T,X,H) is non empty ordinal natural V27() ext-real positive non negative finite cardinal V73() V74() non even complex-membered ext-real-membered real-membered rational-membered integer-membered natural-membered V133() V134() V135() V136() V137() V139() Element of NAT
(T,X,H) . (len (T,X,H)) is set
T is V7() V10( NAT ) Function-like finite [Graph-like] loopless non-multi non-Dmulti simple Dsimple V118() V119() Tree-like set
the_Vertices_of T is non empty set
X is Element of the_Vertices_of T
H is Element of the_Vertices_of T
(T,X,H) is non empty V7() V10( NAT ) V11((the_Vertices_of T) \/ (the_Edges_of T)) Function-like finite FinSequence-like FinSubsequence-like Trail-like Path-like Walk of T
the_Edges_of T is set
(the_Vertices_of T) \/ (the_Edges_of T) is non empty set
(T,X,H) .vertices() is finite Element of K32((the_Vertices_of T))
K32((the_Vertices_of T)) is non empty-membered set
(T,X,H) .vertexSeq() is V7() V10( NAT ) V11( the_Vertices_of T) Function-like finite FinSequence-like FinSubsequence-like VertexSeq of T
K319((the_Vertices_of T),((T,X,H) .vertexSeq())) is finite Element of K32((the_Vertices_of T))
(T,X,H) .first() is Element of the_Vertices_of T
(T,X,H) . 1 is set
(T,X,H) .last() is Element of the_Vertices_of T
len (T,X,H) is non empty ordinal natural V27() ext-real positive non negative finite cardinal V73() V74() non even complex-membered ext-real-membered real-membered rational-membered integer-membered natural-membered V133() V134() V135() V136() V137() V139() Element of NAT
(T,X,H) . (len (T,X,H)) is set
T is V7() V10( NAT ) Function-like finite [Graph-like] loopless non-multi non-Dmulti simple Dsimple V118() V119() Tree-like set
the_Vertices_of T is non empty set
X is Element of the_Vertices_of T
(T,X,X) is non empty V7() V10( NAT ) V11((the_Vertices_of T) \/ (the_Edges_of T)) Function-like finite FinSequence-like FinSubsequence-like Trail-like Path-like Walk of T
the_Edges_of T is set
(the_Vertices_of T) \/ (the_Edges_of T) is non empty set
T is V7() V10( NAT ) Function-like finite [Graph-like] loopless non-multi non-Dmulti simple Dsimple V118() V119() Tree-like set
the_Vertices_of T is non empty set
X is Element of the_Vertices_of T
(T,X,X) is non empty V7() V10( NAT ) V11((the_Vertices_of T) \/ (the_Edges_of T)) Function-like finite FinSequence-like FinSubsequence-like closed Trail-like Path-like Walk of T
the_Edges_of T is set
(the_Vertices_of T) \/ (the_Edges_of T) is non empty set
T is V7() V10( NAT ) Function-like finite [Graph-like] loopless non-multi non-Dmulti simple Dsimple V118() V119() Tree-like set
the_Vertices_of T is non empty set
X is Element of the_Vertices_of T
(T,X,X) is non empty V7() V10( NAT ) V11((the_Vertices_of T) \/ (the_Edges_of T)) Function-like finite FinSequence-like FinSubsequence-like closed trivial Trail-like Path-like vertex-distinct Walk of T
the_Edges_of T is set
(the_Vertices_of T) \/ (the_Edges_of T) is non empty set
(T,X,X) .vertices() is finite Element of K32((the_Vertices_of T))
K32((the_Vertices_of T)) is non empty-membered set
(T,X,X) .vertexSeq() is V7() V10( NAT ) V11( the_Vertices_of T) Function-like finite FinSequence-like FinSubsequence-like VertexSeq of T
K319((the_Vertices_of T),((T,X,X) .vertexSeq())) is finite Element of K32((the_Vertices_of T))
{X} is non empty trivial finite 1 -element set
H9 is Element of the_Vertices_of T
T .walkOf H9 is non empty V7() V10( NAT ) V11((the_Vertices_of T) \/ (the_Edges_of T)) Function-like finite FinSequence-like FinSubsequence-like closed V111(T) trivial Trail-like Path-like vertex-distinct Walk of T
<*H9*> is non empty trivial V7() V10( NAT ) V11( the_Vertices_of T) Function-like constant finite 1 -element FinSequence-like FinSubsequence-like FinSequence of the_Vertices_of T
(T,X,X) .first() is Element of the_Vertices_of T
(T,X,X) . 1 is set
(T .walkOf H9) .first() is Element of the_Vertices_of T
(T .walkOf H9) . 1 is set
T is V7() V10( NAT ) Function-like finite [Graph-like] loopless non-multi non-Dmulti simple Dsimple V118() V119() Tree-like set
the_Vertices_of T is non empty set
X is Element of the_Vertices_of T
H is Element of the_Vertices_of T
(T,X,H) is non empty V7() V10( NAT ) V11((the_Vertices_of T) \/ (the_Edges_of T)) Function-like finite FinSequence-like FinSubsequence-like Trail-like Path-like Walk of T
the_Edges_of T is set
(the_Vertices_of T) \/ (the_Edges_of T) is non empty set
(T,X,H) .reverse() is non empty V7() V10( NAT ) V11((the_Vertices_of T) \/ (the_Edges_of T)) Function-like finite FinSequence-like FinSubsequence-like Trail-like Path-like Walk of T
(T,H,X) is non empty V7() V10( NAT ) V11((the_Vertices_of T) \/ (the_Edges_of T)) Function-like finite FinSequence-like FinSubsequence-like Trail-like Path-like Walk of T
T is V7() V10( NAT ) Function-like finite [Graph-like] loopless non-multi non-Dmulti simple Dsimple V118() V119() Tree-like set
the_Vertices_of T is non empty set
X is Element of the_Vertices_of T
H is Element of the_Vertices_of T
(T,X,H) is non empty V7() V10( NAT ) V11((the_Vertices_of T) \/ (the_Edges_of T)) Function-like finite FinSequence-like FinSubsequence-like Trail-like Path-like Walk of T
the_Edges_of T is set
(the_Vertices_of T) \/ (the_Edges_of T) is non empty set
(T,X,H) .vertices() is finite Element of K32((the_Vertices_of T))
K32((the_Vertices_of T)) is non empty-membered set
(T,X,H) .vertexSeq() is V7() V10( NAT ) V11( the_Vertices_of T) Function-like finite FinSequence-like FinSubsequence-like VertexSeq of T
K319((the_Vertices_of T),((T,X,H) .vertexSeq())) is finite Element of K32((the_Vertices_of T))
(T,H,X) is non empty V7() V10( NAT ) V11((the_Vertices_of T) \/ (the_Edges_of T)) Function-like finite FinSequence-like FinSubsequence-like Trail-like Path-like Walk of T
(T,H,X) .vertices() is finite Element of K32((the_Vertices_of T))
(T,H,X) .vertexSeq() is V7() V10( NAT ) V11( the_Vertices_of T) Function-like finite FinSequence-like FinSubsequence-like VertexSeq of T
K319((the_Vertices_of T),((T,H,X) .vertexSeq())) is finite Element of K32((the_Vertices_of T))
(T,X,H) .reverse() is non empty V7() V10( NAT ) V11((the_Vertices_of T) \/ (the_Edges_of T)) Function-like finite FinSequence-like FinSubsequence-like Trail-like Path-like Walk of T
T is V7() V10( NAT ) Function-like finite [Graph-like] loopless non-multi non-Dmulti simple Dsimple V118() V119() Tree-like set
the_Vertices_of T is non empty set
X is Element of the_Vertices_of T
H is Element of the_Vertices_of T
(T,X,H) is non empty V7() V10( NAT ) V11((the_Vertices_of T) \/ (the_Edges_of T)) Function-like finite FinSequence-like FinSubsequence-like Trail-like Path-like Walk of T
the_Edges_of T is set
(the_Vertices_of T) \/ (the_Edges_of T) is non empty set
H9 is V7() V10( NAT ) Function-like finite [Graph-like] loopless non-multi non-Dmulti simple Dsimple V118() V119() Tree-like Subgraph of T
the_Vertices_of H9 is non empty set
cH is Element of the_Vertices_of H9
A is Element of the_Vertices_of H9
(H9,cH,A) is non empty V7() V10( NAT ) V11((the_Vertices_of H9) \/ (the_Edges_of H9)) Function-like finite FinSequence-like FinSubsequence-like Trail-like Path-like Walk of H9
the_Edges_of H9 is set
(the_Vertices_of H9) \/ (the_Edges_of H9) is non empty set
mA is non empty V7() V10( NAT ) V11((the_Vertices_of T) \/ (the_Edges_of T)) Function-like finite FinSequence-like FinSubsequence-like Walk of T
mA .last() is Element of the_Vertices_of T
len mA is non empty ordinal natural V27() ext-real positive non negative finite cardinal V73() V74() non even complex-membered ext-real-membered real-membered rational-membered integer-membered natural-membered V133() V134() V135() V136() V137() V139() Element of NAT
mA . (len mA) is set
(H9,cH,A) .last() is Element of the_Vertices_of H9
len (H9,cH,A) is non empty ordinal natural V27() ext-real positive non negative finite cardinal V73() V74() non even complex-membered ext-real-membered real-membered rational-membered integer-membered natural-membered V133() V134() V135() V136() V137() V139() Element of NAT
(H9,cH,A) . (len (H9,cH,A)) is set
mA .first() is Element of the_Vertices_of T
mA . 1 is set
(H9,cH,A) .first() is Element of the_Vertices_of H9
(H9,cH,A) . 1 is set
T is V7() V10( NAT ) Function-like finite [Graph-like] loopless non-multi non-Dmulti simple Dsimple V118() V119() Tree-like set
the_Vertices_of T is non empty set
X is Element of the_Vertices_of T
H is Element of the_Vertices_of T
(T,X,H) is non empty V7() V10( NAT ) V11((the_Vertices_of T) \/ (the_Edges_of T)) Function-like finite FinSequence-like FinSubsequence-like Trail-like Path-like Walk of T
the_Edges_of T is set
(the_Vertices_of T) \/ (the_Edges_of T) is non empty set
(T,X,H) .vertices() is finite Element of K32((the_Vertices_of T))
K32((the_Vertices_of T)) is non empty-membered set
(T,X,H) .vertexSeq() is V7() V10( NAT ) V11( the_Vertices_of T) Function-like finite FinSequence-like FinSubsequence-like VertexSeq of T
K319((the_Vertices_of T),((T,X,H) .vertexSeq())) is finite Element of K32((the_Vertices_of T))
H9 is V7() V10( NAT ) Function-like finite [Graph-like] loopless non-multi non-Dmulti simple Dsimple V118() V119() Tree-like Subgraph of T
the_Vertices_of H9 is non empty Element of K32((the_Vertices_of T))
the_Vertices_of H9 is non empty set
cH is Element of the_Vertices_of H9
A is Element of the_Vertices_of H9
(H9,cH,A) is non empty V7() V10( NAT ) V11((the_Vertices_of H9) \/ (the_Edges_of H9)) Function-like finite FinSequence-like FinSubsequence-like Trail-like Path-like Walk of H9
the_Edges_of H9 is set
(the_Vertices_of H9) \/ (the_Edges_of H9) is non empty set
(H9,cH,A) .vertices() is finite Element of K32((the_Vertices_of H9))
K32((the_Vertices_of H9)) is non empty-membered set
(H9,cH,A) .vertexSeq() is V7() V10( NAT ) V11( the_Vertices_of H9) Function-like finite FinSequence-like FinSubsequence-like VertexSeq of H9
K319((the_Vertices_of H9),((H9,cH,A) .vertexSeq())) is finite Element of K32((the_Vertices_of H9))
T is V7() V10( NAT ) Function-like finite [Graph-like] loopless non-multi non-Dmulti simple Dsimple V118() V119() Tree-like set
the_Vertices_of T is non empty set
the_Edges_of T is set
(the_Vertices_of T) \/ (the_Edges_of T) is non empty set
X is non empty V7() V10( NAT ) V11((the_Vertices_of T) \/ (the_Edges_of T)) Function-like finite FinSequence-like FinSubsequence-like Trail-like Path-like Walk of T
len X is non empty ordinal natural V27() ext-real positive non negative finite cardinal V73() V74() non even complex-membered ext-real-membered real-membered rational-membered integer-membered natural-membered V133() V134() V135() V136() V137() V139() Element of NAT
H is Element of the_Vertices_of T
H9 is Element of the_Vertices_of T
(T,H,H9) is non empty V7() V10( NAT ) V11((the_Vertices_of T) \/ (the_Edges_of T)) Function-like finite FinSequence-like FinSubsequence-like Trail-like Path-like Walk of T
cH is non empty ordinal natural V27() ext-real positive non negative finite cardinal V73() V74() non even set
A is non empty ordinal natural V27() ext-real positive non negative finite cardinal V73() V74() non even set
X . cH is set
X . A is set
X .cut (cH,A) is non empty V7() V10( NAT ) V11((the_Vertices_of T) \/ (the_Edges_of T)) Function-like finite FinSequence-like FinSubsequence-like Walk of T
A is non empty ordinal natural V27() ext-real positive non negative finite cardinal V73() V74() non even complex-membered ext-real-membered real-membered rational-membered integer-membered natural-membered V133() V134() V135() V136() V137() V139() Element of NAT
mA is non empty ordinal natural V27() ext-real positive non negative finite cardinal V73() V74() non even complex-membered ext-real-membered real-membered rational-membered integer-membered natural-membered V133() V134() V135() V136() V137() V139() Element of NAT
X .cut (A,mA) is non empty V7() V10( NAT ) V11((the_Vertices_of T) \/ (the_Edges_of T)) Function-like finite FinSequence-like FinSubsequence-like Trail-like Path-like Walk of T
T is V7() V10( NAT ) Function-like finite [Graph-like] loopless non-multi non-Dmulti simple Dsimple V118() V119() Tree-like set
the_Vertices_of T is non empty set
H9 is Element of the_Vertices_of T
X is Element of the_Vertices_of T
H is Element of the_Vertices_of T
(T,X,H) is non empty V7() V10( NAT ) V11((the_Vertices_of T) \/ (the_Edges_of T)) Function-like finite FinSequence-like FinSubsequence-like Trail-like Path-like Walk of T
the_Edges_of T is set
(the_Vertices_of T) \/ (the_Edges_of T) is non empty set
(T,X,H) .vertices() is finite Element of K32((the_Vertices_of T))
K32((the_Vertices_of T)) is non empty-membered set
(T,X,H) .vertexSeq() is V7() V10( NAT ) V11( the_Vertices_of T) Function-like finite FinSequence-like FinSubsequence-like VertexSeq of T
K319((the_Vertices_of T),((T,X,H) .vertexSeq())) is finite Element of K32((the_Vertices_of T))
(T,X,H9) is non empty V7() V10( NAT ) V11((the_Vertices_of T) \/ (the_Edges_of T)) Function-like finite FinSequence-like FinSubsequence-like Trail-like Path-like Walk of T
(T,H9,H) is non empty V7() V10( NAT ) V11((the_Vertices_of T) \/ (the_Edges_of T)) Function-like finite FinSequence-like FinSubsequence-like Trail-like Path-like Walk of T
(T,X,H9) .append (T,H9,H) is non empty V7() V10( NAT ) V11((the_Vertices_of T) \/ (the_Edges_of T)) Function-like finite FinSequence-like FinSubsequence-like Walk of T
(T,X,H) .find H9 is non empty ordinal natural V27() ext-real positive non negative finite cardinal V73() V74() non even complex-membered ext-real-membered real-membered rational-membered integer-membered natural-membered V133() V134() V135() V136() V137() V139() Element of NAT
len (T,X,H) is non empty ordinal natural V27() ext-real positive non negative finite cardinal V73() V74() non even complex-membered ext-real-membered real-membered rational-membered integer-membered natural-membered V133() V134() V135() V136() V137() V139() Element of NAT
(T,X,H) .cut (1,(len (T,X,H))) is non empty V7() V10( NAT ) V11((the_Vertices_of T) \/ (the_Edges_of T)) Function-like finite FinSequence-like FinSubsequence-like Trail-like Path-like Walk of T
2 * 0 is empty V7() non-empty empty-yielding V10( NAT ) Function-like one-to-one constant functional ordinal natural V27() ext-real non positive non negative finite finite-yielding V39() cardinal {} -element FinSequence-like FinSubsequence-like FinSequence-membered V73() V74() even complex-membered ext-real-membered real-membered rational-membered integer-membered natural-membered V132() V135() V136() V137() V138() V139() Element of NAT
(2 * 0) + 1 is non empty ordinal natural V27() ext-real positive non negative finite cardinal V73() V74() non even complex-membered ext-real-membered real-membered rational-membered integer-membered natural-membered V133() V134() V135() V136() V137() V139() Element of NAT
(T,X,H) . ((T,X,H) .find H9) is set
(T,X,H) . (len (T,X,H)) is set
(T,X,H) .last() is Element of the_Vertices_of T
(T,X,H) .cut (((T,X,H) .find H9),(len (T,X,H))) is non empty V7() V10( NAT ) V11((the_Vertices_of T) \/ (the_Edges_of T)) Function-like finite FinSequence-like FinSubsequence-like Trail-like Path-like Walk of T
(T,X,H) . 1 is set
(T,X,H) .first() is Element of the_Vertices_of T
(T,X,H) .cut (1,((T,X,H) .find H9)) is non empty V7() V10( NAT ) V11((the_Vertices_of T) \/ (the_Edges_of T)) Function-like finite FinSequence-like FinSubsequence-like Trail-like Path-like Walk of T
(T,X,H9) .vertices() is finite Element of K32((the_Vertices_of T))
(T,X,H9) .vertexSeq() is V7() V10( NAT ) V11( the_Vertices_of T) Function-like finite FinSequence-like FinSubsequence-like VertexSeq of T
K319((the_Vertices_of T),((T,X,H9) .vertexSeq())) is finite Element of K32((the_Vertices_of T))
T is V7() V10( NAT ) Function-like finite [Graph-like] loopless non-multi non-Dmulti simple Dsimple V118() V119() Tree-like set
the_Vertices_of T is non empty set
H9 is Element of the_Vertices_of T
X is Element of the_Vertices_of T
H is Element of the_Vertices_of T
(T,X,H) is non empty V7() V10( NAT ) V11((the_Vertices_of T) \/ (the_Edges_of T)) Function-like finite FinSequence-like FinSubsequence-like Trail-like Path-like Walk of T
the_Edges_of T is set
(the_Vertices_of T) \/ (the_Edges_of T) is non empty set
(T,X,H) .vertices() is finite Element of K32((the_Vertices_of T))
K32((the_Vertices_of T)) is non empty-membered set
(T,X,H) .vertexSeq() is V7() V10( NAT ) V11( the_Vertices_of T) Function-like finite FinSequence-like FinSubsequence-like VertexSeq of T
K319((the_Vertices_of T),((T,X,H) .vertexSeq())) is finite Element of K32((the_Vertices_of T))
(T,X,H9) is non empty V7() V10( NAT ) V11((the_Vertices_of T) \/ (the_Edges_of T)) Function-like finite FinSequence-like FinSubsequence-like Trail-like Path-like Walk of T
(T,H9,H) is non empty V7() V10( NAT ) V11((the_Vertices_of T) \/ (the_Edges_of T)) Function-like finite FinSequence-like FinSubsequence-like Trail-like Path-like Walk of T
(T,X,H9) .append (T,H9,H) is non empty V7() V10( NAT ) V11((the_Vertices_of T) \/ (the_Edges_of T)) Function-like finite FinSequence-like FinSubsequence-like Walk of T
(T,X,H9) .vertices() is finite Element of K32((the_Vertices_of T))
(T,X,H9) .vertexSeq() is V7() V10( NAT ) V11( the_Vertices_of T) Function-like finite FinSequence-like FinSubsequence-like VertexSeq of T
K319((the_Vertices_of T),((T,X,H9) .vertexSeq())) is finite Element of K32((the_Vertices_of T))
T is V7() V10( NAT ) Function-like finite [Graph-like] loopless non-multi non-Dmulti simple Dsimple V118() V119() Tree-like set
the_Vertices_of T is non empty set
the_Edges_of T is set
(the_Vertices_of T) \/ (the_Edges_of T) is non empty set
X is non empty V7() V10( NAT ) V11((the_Vertices_of T) \/ (the_Edges_of T)) Function-like finite FinSequence-like FinSubsequence-like Trail-like Path-like Walk of T
X .last() is Element of the_Vertices_of T
len X is non empty ordinal natural V27() ext-real positive non negative finite cardinal V73() V74() non even complex-membered ext-real-membered real-membered rational-membered integer-membered natural-membered V133() V134() V135() V136() V137() V139() Element of NAT
X . (len X) is set
H is non empty V7() V10( NAT ) V11((the_Vertices_of T) \/ (the_Edges_of T)) Function-like finite FinSequence-like FinSubsequence-like Trail-like Path-like Walk of T
H .first() is Element of the_Vertices_of T
H . 1 is set
X .vertices() is finite Element of K32((the_Vertices_of T))
K32((the_Vertices_of T)) is non empty-membered set
X .vertexSeq() is V7() V10( NAT ) V11( the_Vertices_of T) Function-like finite FinSequence-like FinSubsequence-like VertexSeq of T
K319((the_Vertices_of T),(X .vertexSeq())) is finite Element of K32((the_Vertices_of T))
H .vertices() is finite Element of K32((the_Vertices_of T))
H .vertexSeq() is V7() V10( NAT ) V11( the_Vertices_of T) Function-like finite FinSequence-like FinSubsequence-like VertexSeq of T
K319((the_Vertices_of T),(H .vertexSeq())) is finite Element of K32((the_Vertices_of T))
(X .vertices()) /\ (H .vertices()) is finite Element of K32((the_Vertices_of T))
{(X .last())} is non empty trivial finite 1 -element set
X .append H is non empty V7() V10( NAT ) V11((the_Vertices_of T) \/ (the_Edges_of T)) Function-like finite FinSequence-like FinSubsequence-like Walk of T
T is V7() V10( NAT ) Function-like finite [Graph-like] loopless non-multi non-Dmulti simple Dsimple V118() V119() Tree-like set
the_Vertices_of T is non empty set
H9 is Element of the_Vertices_of T
X is Element of the_Vertices_of T
H is Element of the_Vertices_of T
(T,X,H) is non empty V7() V10( NAT ) V11((the_Vertices_of T) \/ (the_Edges_of T)) Function-like finite FinSequence-like FinSubsequence-like Trail-like Path-like Walk of T
the_Edges_of T is set
(the_Vertices_of T) \/ (the_Edges_of T) is non empty set
(T,X,H) .vertices() is finite Element of K32((the_Vertices_of T))
K32((the_Vertices_of T)) is non empty-membered set
(T,X,H) .vertexSeq() is V7() V10( NAT ) V11( the_Vertices_of T) Function-like finite FinSequence-like FinSubsequence-like VertexSeq of T
K319((the_Vertices_of T),((T,X,H) .vertexSeq())) is finite Element of K32((the_Vertices_of T))
(T,X,H9) is non empty V7() V10( NAT ) V11((the_Vertices_of T) \/ (the_Edges_of T)) Function-like finite FinSequence-like FinSubsequence-like Trail-like Path-like Walk of T
(T,X,H9) .vertices() is finite Element of K32((the_Vertices_of T))
(T,X,H9) .vertexSeq() is V7() V10( NAT ) V11( the_Vertices_of T) Function-like finite FinSequence-like FinSubsequence-like VertexSeq of T
K319((the_Vertices_of T),((T,X,H9) .vertexSeq())) is finite Element of K32((the_Vertices_of T))
(T,H9,H) is non empty V7() V10( NAT ) V11((the_Vertices_of T) \/ (the_Edges_of T)) Function-like finite FinSequence-like FinSubsequence-like Trail-like Path-like Walk of T
(T,H9,H) .vertices() is finite Element of K32((the_Vertices_of T))
(T,H9,H) .vertexSeq() is V7() V10( NAT ) V11( the_Vertices_of T) Function-like finite FinSequence-like FinSubsequence-like VertexSeq of T
K319((the_Vertices_of T),((T,H9,H) .vertexSeq())) is finite Element of K32((the_Vertices_of T))
((T,X,H9) .vertices()) /\ ((T,H9,H) .vertices()) is finite Element of K32((the_Vertices_of T))
{H9} is non empty trivial finite 1 -element set
(T,X,H9) .last() is Element of the_Vertices_of T
len (T,X,H9) is non empty ordinal natural V27() ext-real positive non negative finite cardinal V73() V74() non even complex-membered ext-real-membered real-membered rational-membered integer-membered natural-membered V133() V134() V135() V136() V137() V139() Element of NAT
(T,X,H9) . (len (T,X,H9)) is set
(T,H9,H) .first() is Element of the_Vertices_of T
(T,H9,H) . 1 is set
mA is set
(T,X,H9) .append (T,H9,H) is non empty V7() V10( NAT ) V11((the_Vertices_of T) \/ (the_Edges_of T)) Function-like finite FinSequence-like FinSubsequence-like Walk of T
(T,X,H) .first() is Element of the_Vertices_of T
(T,X,H) . 1 is set
(T,X,H) .last() is Element of the_Vertices_of T
len (T,X,H) is non empty ordinal natural V27() ext-real positive non negative finite cardinal V73() V74() non even complex-membered ext-real-membered real-membered rational-membered integer-membered natural-membered V133() V134() V135() V136() V137() V139() Element of NAT
(T,X,H) . (len (T,X,H)) is set
{X} is non empty trivial finite 1 -element set
((T,X,H9) .vertices()) \/ ((T,H9,H) .vertices()) is finite Element of K32((the_Vertices_of T))
len (T,H9,H) is non empty ordinal natural V27() ext-real positive non negative finite cardinal V73() V74() non even complex-membered ext-real-membered real-membered rational-membered integer-membered natural-membered V133() V134() V135() V136() V137() V139() Element of NAT
cA is non empty ordinal natural V27() ext-real positive non negative finite cardinal V73() V74() non even complex-membered ext-real-membered real-membered rational-membered integer-membered natural-membered V133() V134() V135() V136() V137() V139() Element of NAT
(T,H9,H) . cA is set
1 - 1 is V27() ext-real V73() V74() set
cA - 1 is V27() ext-real V73() V74() even set
C is non empty ordinal natural V27() ext-real positive non negative finite cardinal V73() V74() non even complex-membered ext-real-membered real-membered rational-membered integer-membered natural-membered V133() V134() V135() V136() V137() V139() Element of NAT
(T,X,H9) . C is set
B is ordinal natural V27() ext-real non negative finite cardinal V73() V74() even complex-membered ext-real-membered real-membered rational-membered integer-membered natural-membered V135() V136() V137() V139() Element of NAT
(len (T,X,H9)) + B is non empty ordinal natural V27() ext-real positive non negative finite cardinal V73() V74() non even complex-membered ext-real-membered real-membered rational-membered integer-membered natural-membered V133() V134() V135() V136() V137() V139() Element of NAT
dom (T,X,H9) is non empty finite complex-membered ext-real-membered real-membered rational-membered integer-membered natural-membered V133() V134() V135() V136() V137() Element of K32(NAT)
(T,X,H) . C is set
B + 1 is non empty ordinal natural V27() ext-real positive non negative finite cardinal V73() V74() non even complex-membered ext-real-membered real-membered rational-membered integer-membered natural-membered V133() V134() V135() V136() V137() V139() Element of NAT
(len (T,X,H9)) + (B + 1) is non empty ordinal natural V27() ext-real positive non negative finite cardinal V73() V74() even complex-membered ext-real-membered real-membered rational-membered integer-membered natural-membered V133() V134() V135() V136() V137() V139() Element of NAT
(len (T,X,H9)) + (len (T,H9,H)) is non empty ordinal natural V27() ext-real positive non negative finite cardinal V73() V74() even complex-membered ext-real-membered real-membered rational-membered integer-membered natural-membered V133() V134() V135() V136() V137() V139() Element of NAT
((len (T,X,H9)) + B) + 1 is non empty ordinal natural V27() ext-real positive non negative finite cardinal V73() V74() even complex-membered ext-real-membered real-membered rational-membered integer-membered natural-membered V133() V134() V135() V136() V137() V139() Element of NAT
(((len (T,X,H9)) + B) + 1) - 1 is non empty V27() ext-real V73() V74() non even set
((len (T,X,H9)) + (len (T,H9,H))) - 1 is non empty V27() ext-real V73() V74() non even set
(len (T,X,H)) + 1 is non empty ordinal natural V27() ext-real positive non negative finite cardinal V73() V74() even complex-membered ext-real-membered real-membered rational-membered integer-membered natural-membered V133() V134() V135() V136() V137() V139() Element of NAT
((len (T,X,H)) + 1) - 1 is non empty V27() ext-real V73() V74() non even set
(T,X,H) . ((len (T,X,H9)) + B) is set
mA is set
(T,X,H9) .first() is Element of the_Vertices_of T
(T,X,H9) . 1 is set
(T,H9,H) .last() is Element of the_Vertices_of T
len (T,H9,H) is non empty ordinal natural V27() ext-real positive non negative finite cardinal V73() V74() non even complex-membered ext-real-membered real-membered rational-membered integer-membered natural-membered V133() V134() V135() V136() V137() V139() Element of NAT
(T,H9,H) . (len (T,H9,H)) is set
(T,X,H9) .append (T,H9,H) is non empty V7() V10( NAT ) V11((the_Vertices_of T) \/ (the_Edges_of T)) Function-like finite FinSequence-like FinSubsequence-like Walk of T
{((T,X,H9) .last())} is non empty trivial finite 1 -element set
T is V7() V10( NAT ) Function-like finite [Graph-like] loopless non-multi non-Dmulti simple Dsimple V118() V119() Tree-like set
the_Vertices_of T is non empty set
the_Edges_of T is set
(the_Vertices_of T) \/ (the_Edges_of T) is non empty set
X is Element of the_Vertices_of T
H is Element of the_Vertices_of T
(T,X,H) is non empty V7() V10( NAT ) V11((the_Vertices_of T) \/ (the_Edges_of T)) Function-like finite FinSequence-like FinSubsequence-like Trail-like Path-like Walk of T
H9 is Element of the_Vertices_of T
(T,X,H9) is non empty V7() V10( NAT ) V11((the_Vertices_of T) \/ (the_Edges_of T)) Function-like finite FinSequence-like FinSubsequence-like Trail-like Path-like Walk of T
cH is Element of the_Vertices_of T
(T,cH,H) is non empty V7() V10( NAT ) V11((the_Vertices_of T) \/ (the_Edges_of T)) Function-like finite FinSequence-like FinSubsequence-like Trail-like Path-like Walk of T
(T,cH,H) .vertices() is finite Element of K32((the_Vertices_of T))
K32((the_Vertices_of T)) is non empty-membered set
(T,cH,H) .vertexSeq() is V7() V10( NAT ) V11( the_Vertices_of T) Function-like finite FinSequence-like FinSubsequence-like VertexSeq of T
K319((the_Vertices_of T),((T,cH,H) .vertexSeq())) is finite Element of K32((the_Vertices_of T))
(T,cH,H9) is non empty V7() V10( NAT ) V11((the_Vertices_of T) \/ (the_Edges_of T)) Function-like finite FinSequence-like FinSubsequence-like Trail-like Path-like Walk of T
(T,cH,H9) .vertices() is finite Element of K32((the_Vertices_of T))
(T,cH,H9) .vertexSeq() is V7() V10( NAT ) V11( the_Vertices_of T) Function-like finite FinSequence-like FinSubsequence-like VertexSeq of T
K319((the_Vertices_of T),((T,cH,H9) .vertexSeq())) is finite Element of K32((the_Vertices_of T))
((T,cH,H) .vertices()) /\ ((T,cH,H9) .vertices()) is finite Element of K32((the_Vertices_of T))
{cH} is non empty trivial finite 1 -element set
A is non empty V7() V10( NAT ) V11((the_Vertices_of T) \/ (the_Edges_of T)) Function-like finite FinSequence-like FinSubsequence-like Trail-like Path-like Walk of T
A is non empty V7() V10( NAT ) V11((the_Vertices_of T) \/ (the_Edges_of T)) Function-like finite FinSequence-like FinSubsequence-like Trail-like Path-like Walk of T
(A,A) is V7() V10( NAT ) Function-like finite FinSequence-like FinSubsequence-like set
len (A,A) is ordinal natural V27() ext-real non negative finite cardinal V73() V74() complex-membered ext-real-membered real-membered rational-membered integer-membered natural-membered V135() V136() V137() V139() Element of NAT
A . (len (A,A)) is set
(T,X,cH) is non empty V7() V10( NAT ) V11((the_Vertices_of T) \/ (the_Edges_of T)) Function-like finite FinSequence-like FinSubsequence-like Trail-like Path-like Walk of T
A .first() is Element of the_Vertices_of T
A . 1 is set
A .first() is Element of the_Vertices_of T
A . 1 is set
B is non empty ordinal natural V27() ext-real positive non negative finite cardinal V73() V74() non even complex-membered ext-real-membered real-membered rational-membered integer-membered natural-membered V133() V134() V135() V136() V137() V139() Element of NAT
B + 2 is non empty ordinal natural V27() ext-real positive non negative finite cardinal V73() V74() non even complex-membered ext-real-membered real-membered rational-membered integer-membered natural-membered V133() V134() V135() V136() V137() V139() Element of NAT
(T,cH,H) .first() is Element of the_Vertices_of T
(T,cH,H) . 1 is set
A . (len (A,A)) is set
len A is non empty ordinal natural V27() ext-real positive non negative finite cardinal V73() V74() non even complex-membered ext-real-membered real-membered rational-membered integer-membered natural-membered V133() V134() V135() V136() V137() V139() Element of NAT
A .vertices() is finite Element of K32((the_Vertices_of T))
A .vertexSeq() is V7() V10( NAT ) V11( the_Vertices_of T) Function-like finite FinSequence-like FinSubsequence-like VertexSeq of T
K319((the_Vertices_of T),(A .vertexSeq())) is finite Element of K32((the_Vertices_of T))
(T,X,cH) .append (T,cH,H9) is non empty V7() V10( NAT ) V11((the_Vertices_of T) \/ (the_Edges_of T)) Function-like finite FinSequence-like FinSubsequence-like Walk of T
(T,X,cH) .last() is Element of the_Vertices_of T
len (T,X,cH) is non empty ordinal natural V27() ext-real positive non negative finite cardinal V73() V74() non even complex-membered ext-real-membered real-membered rational-membered integer-membered natural-membered V133() V134() V135() V136() V137() V139() Element of NAT
(T,X,cH) . (len (T,X,cH)) is set
(T,cH,H9) . 1 is set
(T,cH,H9) .first() is Element of the_Vertices_of T
len A is non empty ordinal natural V27() ext-real positive non negative finite cardinal V73() V74() non even complex-membered ext-real-membered real-membered rational-membered integer-membered natural-membered V133() V134() V135() V136() V137() V139() Element of NAT
A .vertices() is finite Element of K32((the_Vertices_of T))
A .vertexSeq() is V7() V10( NAT ) V11( the_Vertices_of T) Function-like finite FinSequence-like FinSubsequence-like VertexSeq of T
K319((the_Vertices_of T),(A .vertexSeq())) is finite Element of K32((the_Vertices_of T))
(T,X,cH) .append (T,cH,H) is non empty V7() V10( NAT ) V11((the_Vertices_of T) \/ (the_Edges_of T)) Function-like finite FinSequence-like FinSubsequence-like Walk of T
2 * 0 is empty V7() non-empty empty-yielding V10( NAT ) Function-like one-to-one constant functional ordinal natural V27() ext-real non positive non negative finite finite-yielding V39() cardinal {} -element FinSequence-like FinSubsequence-like FinSequence-membered V73() V74() even complex-membered ext-real-membered real-membered rational-membered integer-membered natural-membered V132() V135() V136() V137() V138() V139() Element of NAT
(2 * 0) + 1 is non empty ordinal natural V27() ext-real positive non negative finite cardinal V73() V74() non even complex-membered ext-real-membered real-membered rational-membered integer-membered natural-membered V133() V134() V135() V136() V137() V139() Element of NAT
A .cut (((2 * 0) + 1),B) is non empty V7() V10( NAT ) V11((the_Vertices_of T) \/ (the_Edges_of T)) Function-like finite FinSequence-like FinSubsequence-like Trail-like Path-like Walk of T
(len (T,X,cH)) + ((2 * 0) + 1) is non empty ordinal natural V27() ext-real positive non negative finite cardinal V73() V74() even complex-membered ext-real-membered real-membered rational-membered integer-membered natural-membered V133() V134() V135() V136() V137() V139() Element of NAT
B + 1 is non empty ordinal natural V27() ext-real positive non negative finite cardinal V73() V74() even complex-membered ext-real-membered real-membered rational-membered integer-membered natural-membered V133() V134() V135() V136() V137() V139() Element of NAT
B is set
len (T,cH,H) is non empty ordinal natural V27() ext-real positive non negative finite cardinal V73() V74() non even complex-membered ext-real-membered real-membered rational-membered integer-membered natural-membered V133() V134() V135() V136() V137() V139() Element of NAT
mB is Element of the_Vertices_of T
a is non empty ordinal natural V27() ext-real positive non negative finite cardinal V73() V74() non even complex-membered ext-real-membered real-membered rational-membered integer-membered natural-membered V133() V134() V135() V136() V137() V139() Element of NAT
(T,cH,H) . a is set
(T,cH,H) .cut (1,a) is non empty V7() V10( NAT ) V11((the_Vertices_of T) \/ (the_Edges_of T)) Function-like finite FinSequence-like FinSubsequence-like Trail-like Path-like Walk of T
len ((T,cH,H) .cut (1,a)) is non empty ordinal natural V27() ext-real positive non negative finite cardinal V73() V74() non even complex-membered ext-real-membered real-membered rational-membered integer-membered natural-membered V133() V134() V135() V136() V137() V139() Element of NAT
((T,cH,H) .cut (1,a)) . 1 is set
((2 * 0) + 1) + 2 is non empty ordinal natural V27() ext-real positive non negative finite cardinal V73() V74() non even complex-membered ext-real-membered real-membered rational-membered integer-membered natural-membered V133() V134() V135() V136() V137() V139() Element of NAT
len (T,cH,H9) is non empty ordinal natural V27() ext-real positive non negative finite cardinal V73() V74() non even complex-membered ext-real-membered real-membered rational-membered integer-membered natural-membered V133() V134() V135() V136() V137() V139() Element of NAT
c is non empty ordinal natural V27() ext-real positive non negative finite cardinal V73() V74() non even complex-membered ext-real-membered real-membered rational-membered integer-membered natural-membered V133() V134() V135() V136() V137() V139() Element of NAT
(T,cH,H9) . c is set
(T,cH,H9) .cut (1,c) is non empty V7() V10( NAT ) V11((the_Vertices_of T) \/ (the_Edges_of T)) Function-like finite FinSequence-like FinSubsequence-like Trail-like Path-like Walk of T
len ((T,cH,H9) .cut (1,c)) is non empty ordinal natural V27() ext-real positive non negative finite cardinal V73() V74() non even complex-membered ext-real-membered real-membered rational-membered integer-membered natural-membered V133() V134() V135() V136() V137() V139() Element of NAT
((T,cH,H9) .cut (1,c)) . 1 is set
1 + 2 is non empty ordinal natural V27() ext-real positive non negative finite cardinal V73() V74() complex-membered ext-real-membered real-membered rational-membered integer-membered natural-membered V133() V134() V135() V136() V137() V139() Element of NAT
dom ((T,cH,H) .cut (1,a)) is non empty finite complex-membered ext-real-membered real-membered rational-membered integer-membered natural-membered V133() V134() V135() V136() V137() Element of K32(NAT)
((T,cH,H) .cut (1,a)) . (1 + 2) is set
(T,cH,H) . (1 + 2) is set
A . (B + 2) is set
A . (B + 2) is set
(T,cH,H9) . (1 + 2) is set
dom ((T,cH,H9) .cut (1,c)) is non empty finite complex-membered ext-real-membered real-membered rational-membered integer-membered natural-membered V133() V134() V135() V136() V137() Element of K32(NAT)
((T,cH,H9) .cut (1,c)) . (1 + 2) is set
T is V7() V10( NAT ) Function-like finite [Graph-like] loopless non-multi non-Dmulti simple Dsimple V118() V119() Tree-like set
the_Vertices_of T is non empty set
H9 is Element of the_Vertices_of T
X is Element of the_Vertices_of T
H is Element of the_Vertices_of T
(T,X,H) is non empty V7() V10( NAT ) V11((the_Vertices_of T) \/ (the_Edges_of T)) Function-like finite FinSequence-like FinSubsequence-like Trail-like Path-like Walk of T
the_Edges_of T is set
(the_Vertices_of T) \/ (the_Edges_of T) is non empty set
(T,X,H) .vertices() is finite Element of K32((the_Vertices_of T))
K32((the_Vertices_of T)) is non empty-membered set
(T,X,H) .vertexSeq() is V7() V10( NAT ) V11( the_Vertices_of T) Function-like finite FinSequence-like FinSubsequence-like VertexSeq of T
K319((the_Vertices_of T),((T,X,H) .vertexSeq())) is finite Element of K32((the_Vertices_of T))
(T,H,H9) is non empty V7() V10( NAT ) V11((the_Vertices_of T) \/ (the_Edges_of T)) Function-like finite FinSequence-like FinSubsequence-like Trail-like Path-like Walk of T
(T,H,H9) .vertices() is finite Element of K32((the_Vertices_of T))
(T,H,H9) .vertexSeq() is V7() V10( NAT ) V11( the_Vertices_of T) Function-like finite FinSequence-like FinSubsequence-like VertexSeq of T
K319((the_Vertices_of T),((T,H,H9) .vertexSeq())) is finite Element of K32((the_Vertices_of T))
((T,X,H) .vertices()) /\ ((T,H,H9) .vertices()) is finite Element of K32((the_Vertices_of T))
(T,H9,X) is non empty V7() V10( NAT ) V11((the_Vertices_of T) \/ (the_Edges_of T)) Function-like finite FinSequence-like FinSubsequence-like Trail-like Path-like Walk of T
(T,H9,X) .vertices() is finite Element of K32((the_Vertices_of T))
(T,H9,X) .vertexSeq() is V7() V10( NAT ) V11( the_Vertices_of T) Function-like finite FinSequence-like FinSubsequence-like VertexSeq of T
K319((the_Vertices_of T),((T,H9,X) .vertexSeq())) is finite Element of K32((the_Vertices_of T))
(((T,X,H) .vertices()) /\ ((T,H,H9) .vertices())) /\ ((T,H9,X) .vertices()) is finite Element of K32((the_Vertices_of T))
{H9} is non empty trivial finite 1 -element set
(T,H,X) is non empty V7() V10( NAT ) V11((the_Vertices_of T) \/ (the_Edges_of T)) Function-like finite FinSequence-like FinSubsequence-like Trail-like Path-like Walk of T
(T,H,X) .vertices() is finite Element of K32((the_Vertices_of T))
(T,H,X) .vertexSeq() is V7() V10( NAT ) V11( the_Vertices_of T) Function-like finite FinSequence-like FinSubsequence-like VertexSeq of T
K319((the_Vertices_of T),((T,H,X) .vertexSeq())) is finite Element of K32((the_Vertices_of T))
((T,H,H9) .vertices()) /\ ((T,H9,X) .vertices()) is finite Element of K32((the_Vertices_of T))
((T,X,H) .vertices()) /\ (((T,H,H9) .vertices()) /\ ((T,H9,X) .vertices())) is finite Element of K32((the_Vertices_of T))
T is V7() V10( NAT ) Function-like finite [Graph-like] loopless non-multi non-Dmulti simple Dsimple V118() V119() Tree-like set
the_Vertices_of T is non empty set
the_Edges_of T is set
(the_Vertices_of T) \/ (the_Edges_of T) is non empty set
X is Element of the_Vertices_of T
H is Element of the_Vertices_of T
(T,X,H) is non empty V7() V10( NAT ) V11((the_Vertices_of T) \/ (the_Edges_of T)) Function-like finite FinSequence-like FinSubsequence-like Trail-like Path-like Walk of T
H9 is Element of the_Vertices_of T
(T,X,H9) is non empty V7() V10( NAT ) V11((the_Vertices_of T) \/ (the_Edges_of T)) Function-like finite FinSequence-like FinSubsequence-like Trail-like Path-like Walk of T
(T,H,H9) is non empty V7() V10( NAT ) V11((the_Vertices_of T) \/ (the_Edges_of T)) Function-like finite FinSequence-like FinSubsequence-like Trail-like Path-like Walk of T
(T,H,H9) .vertices() is finite Element of K32((the_Vertices_of T))
K32((the_Vertices_of T)) is non empty-membered set
(T,H,H9) .vertexSeq() is V7() V10( NAT ) V11( the_Vertices_of T) Function-like finite FinSequence-like FinSubsequence-like VertexSeq of T
K319((the_Vertices_of T),((T,H,H9) .vertexSeq())) is finite Element of K32((the_Vertices_of T))
(T,H9,X) is non empty V7() V10( NAT ) V11((the_Vertices_of T) \/ (the_Edges_of T)) Function-like finite FinSequence-like FinSubsequence-like Trail-like Path-like Walk of T
(T,H9,X) .vertices() is finite Element of K32((the_Vertices_of T))
(T,H9,X) .vertexSeq() is V7() V10( NAT ) V11( the_Vertices_of T) Function-like finite FinSequence-like FinSubsequence-like VertexSeq of T
K319((the_Vertices_of T),((T,H9,X) .vertexSeq())) is finite Element of K32((the_Vertices_of T))
cH is non empty V7() V10( NAT ) V11((the_Vertices_of T) \/ (the_Edges_of T)) Function-like finite FinSequence-like FinSubsequence-like Trail-like Path-like Walk of T
A is non empty V7() V10( NAT ) V11((the_Vertices_of T) \/ (the_Edges_of T)) Function-like finite FinSequence-like FinSubsequence-like Trail-like Path-like Walk of T
cH .vertices() is finite Element of K32((the_Vertices_of T))
cH .vertexSeq() is V7() V10( NAT ) V11( the_Vertices_of T) Function-like finite FinSequence-like FinSubsequence-like VertexSeq of T
K319((the_Vertices_of T),(cH .vertexSeq())) is finite Element of K32((the_Vertices_of T))
(cH .vertices()) /\ ((T,H,H9) .vertices()) is finite Element of K32((the_Vertices_of T))
((cH .vertices()) /\ ((T,H,H9) .vertices())) /\ ((T,H9,X) .vertices()) is finite Element of K32((the_Vertices_of T))
(cH,A) is V7() V10( NAT ) Function-like finite FinSequence-like FinSubsequence-like set
len (cH,A) is ordinal natural V27() ext-real non negative finite cardinal V73() V74() complex-membered ext-real-membered real-membered rational-membered integer-membered natural-membered V135() V136() V137() V139() Element of NAT
cH . (len (cH,A)) is set
{(cH . (len (cH,A)))} is non empty trivial finite 1 -element set
A .vertices() is finite Element of K32((the_Vertices_of T))
A .vertexSeq() is V7() V10( NAT ) V11( the_Vertices_of T) Function-like finite FinSequence-like FinSubsequence-like VertexSeq of T
K319((the_Vertices_of T),(A .vertexSeq())) is finite Element of K32((the_Vertices_of T))
cH .first() is Element of the_Vertices_of T
cH . 1 is set
A .first() is Element of the_Vertices_of T
A . 1 is set
cA is non empty ordinal natural V27() ext-real positive non negative finite cardinal V73() V74() non even complex-membered ext-real-membered real-membered rational-membered integer-membered natural-membered V133() V134() V135() V136() V137() V139() Element of NAT
cH . cA is set
(len (cH,A)) + 2 is non empty ordinal natural V27() ext-real positive non negative finite cardinal V73() V74() complex-membered ext-real-membered real-membered rational-membered integer-membered natural-membered V133() V134() V135() V136() V137() V139() Element of NAT
(T,X,H) .append (T,H,H9) is non empty V7() V10( NAT ) V11((the_Vertices_of T) \/ (the_Edges_of T)) Function-like finite FinSequence-like FinSubsequence-like Walk of T
len A is non empty ordinal natural V27() ext-real positive non negative finite cardinal V73() V74() non even complex-membered ext-real-membered real-membered rational-membered integer-membered natural-membered V133() V134() V135() V136() V137() V139() Element of NAT
len cH is non empty ordinal natural V27() ext-real positive non negative finite cardinal V73() V74() non even complex-membered ext-real-membered real-membered rational-membered integer-membered natural-membered V133() V134() V135() V136() V137() V139() Element of NAT
cH .cut (cA,(len cH)) is non empty V7() V10( NAT ) V11((the_Vertices_of T) \/ (the_Edges_of T)) Function-like finite FinSequence-like FinSubsequence-like Trail-like Path-like Walk of T
(cH .cut (cA,(len cH))) .reverse() is non empty V7() V10( NAT ) V11((the_Vertices_of T) \/ (the_Edges_of T)) Function-like finite FinSequence-like FinSubsequence-like Trail-like Path-like Walk of T
len ((cH .cut (cA,(len cH))) .reverse()) is non empty ordinal natural V27() ext-real positive non negative finite cardinal V73() V74() non even complex-membered ext-real-membered real-membered rational-membered integer-membered natural-membered V133() V134() V135() V136() V137() V139() Element of NAT
A .cut (cA,(len A)) is non empty V7() V10( NAT ) V11((the_Vertices_of T) \/ (the_Edges_of T)) Function-like finite FinSequence-like FinSubsequence-like Trail-like Path-like Walk of T
((cH .cut (cA,(len cH))) .reverse()) .append (A .cut (cA,(len A))) is non empty V7() V10( NAT ) V11((the_Vertices_of T) \/ (the_Edges_of T)) Function-like finite FinSequence-like FinSubsequence-like Walk of T
(cH .cut (cA,(len cH))) .first() is Element of the_Vertices_of T
(cH .cut (cA,(len cH))) . 1 is set
((cH .cut (cA,(len cH))) .reverse()) .last() is Element of the_Vertices_of T
((cH .cut (cA,(len cH))) .reverse()) . (len ((cH .cut (cA,(len cH))) .reverse())) is set
C is Element of the_Vertices_of T
dom ((cH .cut (cA,(len cH))) .reverse()) is non empty finite complex-membered ext-real-membered real-membered rational-membered integer-membered natural-membered V133() V134() V135() V136() V137() Element of K32(NAT)
(((cH .cut (cA,(len cH))) .reverse()) .append (A .cut (cA,(len A)))) . (len ((cH .cut (cA,(len cH))) .reverse())) is set
cH . (len cH) is set
cH .last() is Element of the_Vertices_of T
(cH .cut (cA,(len cH))) .last() is Element of the_Vertices_of T
len (cH .cut (cA,(len cH))) is non empty ordinal natural V27() ext-real positive non negative finite cardinal V73() V74() non even complex-membered ext-real-membered real-membered rational-membered integer-membered natural-membered V133() V134() V135() V136() V137() V139() Element of NAT
(cH .cut (cA,(len cH))) . (len (cH .cut (cA,(len cH)))) is set
((cH .cut (cA,(len cH))) .reverse()) .first() is Element of the_Vertices_of T
((cH .cut (cA,(len cH))) .reverse()) . 1 is set
A . cA is set
A . (len A) is set
A .last() is Element of the_Vertices_of T
(T,C,H9) is non empty V7() V10( NAT ) V11((the_Vertices_of T) \/ (the_Edges_of T)) Function-like finite FinSequence-like FinSubsequence-like Trail-like Path-like Walk of T
(A .cut (cA,(len A))) .first() is Element of the_Vertices_of T
(A .cut (cA,(len A))) . 1 is set
len (((cH .cut (cA,(len cH))) .reverse()) .append (A .cut (cA,(len A)))) is non empty ordinal natural V27() ext-real positive non negative finite cardinal V73() V74() non even complex-membered ext-real-membered real-membered rational-membered integer-membered natural-membered V133() V134() V135() V136() V137() V139() Element of NAT
(T,C,H) is non empty V7() V10( NAT ) V11((the_Vertices_of T) \/ (the_Edges_of T)) Function-like finite FinSequence-like FinSubsequence-like Trail-like Path-like Walk of T
((cH .cut (cA,(len cH))) .reverse()) .vertices() is finite Element of K32((the_Vertices_of T))
((cH .cut (cA,(len cH))) .reverse()) .vertexSeq() is V7() V10( NAT ) V11( the_Vertices_of T) Function-like finite FinSequence-like FinSubsequence-like VertexSeq of T
K319((the_Vertices_of T),(((cH .cut (cA,(len cH))) .reverse()) .vertexSeq())) is finite Element of K32((the_Vertices_of T))
(cH .cut (cA,(len cH))) .vertices() is finite Element of K32((the_Vertices_of T))
(cH .cut (cA,(len cH))) .vertexSeq() is V7() V10( NAT ) V11( the_Vertices_of T) Function-like finite FinSequence-like FinSubsequence-like VertexSeq of T
K319((the_Vertices_of T),((cH .cut (cA,(len cH))) .vertexSeq())) is finite Element of K32((the_Vertices_of T))
(A .cut (cA,(len A))) .vertices() is finite Element of K32((the_Vertices_of T))
(A .cut (cA,(len A))) .vertexSeq() is V7() V10( NAT ) V11( the_Vertices_of T) Function-like finite FinSequence-like FinSubsequence-like VertexSeq of T
K319((the_Vertices_of T),((A .cut (cA,(len A))) .vertexSeq())) is finite Element of K32((the_Vertices_of T))
((cH .cut (cA,(len cH))) .vertices()) /\ ((A .cut (cA,(len A))) .vertices()) is finite Element of K32((the_Vertices_of T))
{C} is non empty trivial finite 1 -element set
(((cH .cut (cA,(len cH))) .reverse()) .vertices()) /\ ((A .cut (cA,(len A))) .vertices()) is finite Element of K32((the_Vertices_of T))
{(((cH .cut (cA,(len cH))) .reverse()) .first()),(((cH .cut (cA,(len cH))) .reverse()) .last())} is non empty finite set
((cH .cut (cA,(len cH))) .reverse()) .edges() is finite Element of K32((the_Edges_of T))
K32((the_Edges_of T)) is set
((cH .cut (cA,(len cH))) .reverse()) .edgeSeq() is V7() V10( NAT ) V11( the_Edges_of T) Function-like finite FinSequence-like FinSubsequence-like EdgeSeq of T
K319((the_Edges_of T),(((cH .cut (cA,(len cH))) .reverse()) .edgeSeq())) is finite Element of K32((the_Edges_of T))
(A .cut (cA,(len A))) .edges() is finite Element of K32((the_Edges_of T))
(A .cut (cA,(len A))) .edgeSeq() is V7() V10( NAT ) V11( the_Edges_of T) Function-like finite FinSequence-like FinSubsequence-like EdgeSeq of T
K319((the_Edges_of T),((A .cut (cA,(len A))) .edgeSeq())) is finite Element of K32((the_Edges_of T))
(((cH .cut (cA,(len cH))) .reverse()) .edges()) /\ ((A .cut (cA,(len A))) .edges()) is finite Element of K32((the_Edges_of T))
cc is set
a is non empty ordinal natural V27() ext-real positive non negative finite cardinal V73() V74() non even complex-membered ext-real-membered real-membered rational-membered integer-membered natural-membered V133() V134() V135() V136() V137() V139() Element of NAT
a + 2 is non empty ordinal natural V27() ext-real positive non negative finite cardinal V73() V74() non even complex-membered ext-real-membered real-membered rational-membered integer-membered natural-membered V133() V134() V135() V136() V137() V139() Element of NAT
aa is Element of the_Vertices_of T
((cH .cut (cA,(len cH))) .reverse()) . a is set
a + 1 is non empty ordinal natural V27() ext-real positive non negative finite cardinal V73() V74() even complex-membered ext-real-membered real-membered rational-membered integer-membered natural-membered V133() V134() V135() V136() V137() V139() Element of NAT
((cH .cut (cA,(len cH))) .reverse()) . (a + 1) is set
bb is Element of the_Vertices_of T
((cH .cut (cA,(len cH))) .reverse()) . (a + 2) is set
{aa,bb} is non empty finite set
len (A .cut (cA,(len A))) is non empty ordinal natural V27() ext-real positive non negative finite cardinal V73() V74() non even complex-membered ext-real-membered real-membered rational-membered integer-membered natural-membered V133() V134() V135() V136() V137() V139() Element of NAT
s is non empty ordinal natural V27() ext-real positive non negative finite cardinal V73() V74() non even complex-membered ext-real-membered real-membered rational-membered integer-membered natural-membered V133() V134() V135() V136() V137() V139() Element of NAT
s + 2 is non empty ordinal natural V27() ext-real positive non negative finite cardinal V73() V74() non even complex-membered ext-real-membered real-membered rational-membered integer-membered natural-membered V133() V134() V135() V136() V137() V139() Element of NAT
b is Element of the_Vertices_of T
(A .cut (cA,(len A))) . s is set
s + 1 is non empty ordinal natural V27() ext-real positive non negative finite cardinal V73() V74() even complex-membered ext-real-membered real-membered rational-membered integer-membered natural-membered V133() V134() V135() V136() V137() V139() Element of NAT
(A .cut (cA,(len A))) . (s + 1) is set
c is Element of the_Vertices_of T
(A .cut (cA,(len A))) . (s + 2) is set
{b,c} is non empty finite set
(A .cut (cA,(len A))) .last() is Element of the_Vertices_of T
len (A .cut (cA,(len A))) is non empty ordinal natural V27() ext-real positive non negative finite cardinal V73() V74() non even complex-membered ext-real-membered real-membered rational-membered integer-membered natural-membered V133() V134() V135() V136() V137() V139() Element of NAT
(A .cut (cA,(len A))) . (len (A .cut (cA,(len A)))) is set
(T,H9,H) is non empty V7() V10( NAT ) V11((the_Vertices_of T) \/ (the_Edges_of T)) Function-like finite FinSequence-like FinSubsequence-like Trail-like Path-like Walk of T
(T,X,H9) .append (T,H9,H) is non empty V7() V10( NAT ) V11((the_Vertices_of T) \/ (the_Edges_of T)) Function-like finite FinSequence-like FinSubsequence-like Walk of T
(T,H9,C) is non empty V7() V10( NAT ) V11((the_Vertices_of T) \/ (the_Edges_of T)) Function-like finite FinSequence-like FinSubsequence-like Trail-like Path-like Walk of T
(T,C,X) is non empty V7() V10( NAT ) V11((the_Vertices_of T) \/ (the_Edges_of T)) Function-like finite FinSequence-like FinSubsequence-like Trail-like Path-like Walk of T
(T,H,C) is non empty V7() V10( NAT ) V11((the_Vertices_of T) \/ (the_Edges_of T)) Function-like finite FinSequence-like FinSubsequence-like Trail-like Path-like Walk of T
(T,X,C) is non empty V7() V10( NAT ) V11((the_Vertices_of T) \/ (the_Edges_of T)) Function-like finite FinSequence-like FinSubsequence-like Trail-like Path-like Walk of T
s is set
(T,H,C) .vertices() is finite Element of K32((the_Vertices_of T))
(T,H,C) .vertexSeq() is V7() V10( NAT ) V11( the_Vertices_of T) Function-like finite FinSequence-like FinSubsequence-like VertexSeq of T
K319((the_Vertices_of T),((T,H,C) .vertexSeq())) is finite Element of K32((the_Vertices_of T))
(T,C,H) .vertices() is finite Element of K32((the_Vertices_of T))
(T,C,H) .vertexSeq() is V7() V10( NAT ) V11( the_Vertices_of T) Function-like finite FinSequence-like FinSubsequence-like VertexSeq of T
K319((the_Vertices_of T),((T,C,H) .vertexSeq())) is finite Element of K32((the_Vertices_of T))
(T,H9,C) .vertices() is finite Element of K32((the_Vertices_of T))
(T,H9,C) .vertexSeq() is V7() V10( NAT ) V11( the_Vertices_of T) Function-like finite FinSequence-like FinSubsequence-like VertexSeq of T
K319((the_Vertices_of T),((T,H9,C) .vertexSeq())) is finite Element of K32((the_Vertices_of T))
(T,C,H9) .vertices() is finite Element of K32((the_Vertices_of T))
(T,C,H9) .vertexSeq() is V7() V10( NAT ) V11( the_Vertices_of T) Function-like finite FinSequence-like FinSubsequence-like VertexSeq of T
K319((the_Vertices_of T),((T,C,H9) .vertexSeq())) is finite Element of K32((the_Vertices_of T))
(T,H9,C) .last() is Element of the_Vertices_of T
len (T,H9,C) is non empty ordinal natural V27() ext-real positive non negative finite cardinal V73() V74() non even complex-membered ext-real-membered real-membered rational-membered integer-membered natural-membered V133() V134() V135() V136() V137() V139() Element of NAT
(T,H9,C) . (len (T,H9,C)) is set
(T,C,X) .first() is Element of the_Vertices_of T
(T,C,X) . 1 is set
(T,H9,C) .append (T,C,X) is non empty V7() V10( NAT ) V11((the_Vertices_of T) \/ (the_Edges_of T)) Function-like finite FinSequence-like FinSubsequence-like Walk of T
(T,C,X) .vertices() is finite Element of K32((the_Vertices_of T))
(T,C,X) .vertexSeq() is V7() V10( NAT ) V11( the_Vertices_of T) Function-like finite FinSequence-like FinSubsequence-like VertexSeq of T
K319((the_Vertices_of T),((T,C,X) .vertexSeq())) is finite Element of K32((the_Vertices_of T))
((T,H9,C) .vertices()) \/ ((T,C,X) .vertices()) is finite Element of K32((the_Vertices_of T))
(T,H,C) .last() is Element of the_Vertices_of T
len (T,H,C) is non empty ordinal natural V27() ext-real positive non negative finite cardinal V73() V74() non even complex-membered ext-real-membered real-membered rational-membered integer-membered natural-membered V133() V134() V135() V136() V137() V139() Element of NAT
(T,H,C) . (len (T,H,C)) is set
(T,C,H9) .first() is Element of the_Vertices_of T
(T,C,H9) . 1 is set
(T,H,C) .append (T,C,H9) is non empty V7() V10( NAT ) V11((the_Vertices_of T) \/ (the_Edges_of T)) Function-like finite FinSequence-like FinSubsequence-like Walk of T
((T,H,C) .vertices()) \/ ((T,C,H9) .vertices()) is finite Element of K32((the_Vertices_of T))
(T,X,C) .last() is Element of the_Vertices_of T
len (T,X,C) is non empty ordinal natural V27() ext-real positive non negative finite cardinal V73() V74() non even complex-membered ext-real-membered real-membered rational-membered integer-membered natural-membered V133() V134() V135() V136() V137() V139() Element of NAT
(T,X,C) . (len (T,X,C)) is set
(T,C,H) .first() is Element of the_Vertices_of T
(T,C,H) . 1 is set
(T,X,C) .append (T,C,H) is non empty V7() V10( NAT ) V11((the_Vertices_of T) \/ (the_Edges_of T)) Function-like finite FinSequence-like FinSubsequence-like Walk of T
(T,X,C) .vertices() is finite Element of K32((the_Vertices_of T))
(T,X,C) .vertexSeq() is V7() V10( NAT ) V11( the_Vertices_of T) Function-like finite FinSequence-like FinSubsequence-like VertexSeq of T
K319((the_Vertices_of T),((T,X,C) .vertexSeq())) is finite Element of K32((the_Vertices_of T))
((T,X,C) .vertices()) \/ ((T,C,H) .vertices()) is finite Element of K32((the_Vertices_of T))
((T,X,C) .vertices()) /\ ((T,C,H) .vertices()) is finite Element of K32((the_Vertices_of T))
((T,X,C) .vertices()) /\ ((T,C,H9) .vertices()) is finite Element of K32((the_Vertices_of T))
((T,H,C) .vertices()) /\ ((T,C,H9) .vertices()) is finite Element of K32((the_Vertices_of T))
T is V7() V10( NAT ) Function-like finite [Graph-like] loopless non-multi non-Dmulti simple Dsimple V118() V119() Tree-like set
the_Vertices_of T is non empty set
X is Element of the_Vertices_of T
H is Element of the_Vertices_of T
(T,X,H) is non empty V7() V10( NAT ) V11((the_Vertices_of T) \/ (the_Edges_of T)) Function-like finite FinSequence-like FinSubsequence-like Trail-like Path-like Walk of T
the_Edges_of T is set
(the_Vertices_of T) \/ (the_Edges_of T) is non empty set
(T,X,H) .vertices() is finite Element of K32((the_Vertices_of T))
K32((the_Vertices_of T)) is non empty-membered set
(T,X,H) .vertexSeq() is V7() V10( NAT ) V11( the_Vertices_of T) Function-like finite FinSequence-like FinSubsequence-like VertexSeq of T
K319((the_Vertices_of T),((T,X,H) .vertexSeq())) is finite Element of K32((the_Vertices_of T))
H9 is Element of the_Vertices_of T
(T,H,H9) is non empty V7() V10( NAT ) V11((the_Vertices_of T) \/ (the_Edges_of T)) Function-like finite FinSequence-like FinSubsequence-like Trail-like Path-like Walk of T
(T,H,H9) .vertices() is finite Element of K32((the_Vertices_of T))
(T,H,H9) .vertexSeq() is V7() V10( NAT ) V11( the_Vertices_of T) Function-like finite FinSequence-like FinSubsequence-like VertexSeq of T
K319((the_Vertices_of T),((T,H,H9) .vertexSeq())) is finite Element of K32((the_Vertices_of T))
((T,X,H) .vertices()) /\ ((T,H,H9) .vertices()) is finite Element of K32((the_Vertices_of T))
(T,H9,X) is non empty V7() V10( NAT ) V11((the_Vertices_of T) \/ (the_Edges_of T)) Function-like finite FinSequence-like FinSubsequence-like Trail-like Path-like Walk of T
(T,H9,X) .vertices() is finite Element of K32((the_Vertices_of T))
(T,H9,X) .vertexSeq() is V7() V10( NAT ) V11( the_Vertices_of T) Function-like finite FinSequence-like FinSubsequence-like VertexSeq of T
K319((the_Vertices_of T),((T,H9,X) .vertexSeq())) is finite Element of K32((the_Vertices_of T))
(((T,X,H) .vertices()) /\ ((T,H,H9) .vertices())) /\ ((T,H9,X) .vertices()) is finite Element of K32((the_Vertices_of T))
{H9} is non empty trivial finite 1 -element set
((T,H,H9) .vertices()) /\ ((T,H9,X) .vertices()) is finite Element of K32((the_Vertices_of T))
(((T,H,H9) .vertices()) /\ ((T,H9,X) .vertices())) /\ ((T,X,H) .vertices()) is finite Element of K32((the_Vertices_of T))
{X} is non empty trivial finite 1 -element set
((T,H9,X) .vertices()) /\ ((T,X,H) .vertices()) is finite Element of K32((the_Vertices_of T))
(((T,H9,X) .vertices()) /\ ((T,X,H) .vertices())) /\ ((T,H,H9) .vertices()) is finite Element of K32((the_Vertices_of T))
{H} is non empty trivial finite 1 -element set
(T,X,H9) is non empty V7() V10( NAT ) V11((the_Vertices_of T) \/ (the_Edges_of T)) Function-like finite FinSequence-like FinSubsequence-like Trail-like Path-like Walk of T
((T,X,H),(T,X,H9)) is V7() V10( NAT ) Function-like finite FinSequence-like FinSubsequence-like set
len ((T,X,H),(T,X,H9)) is ordinal natural V27() ext-real non negative finite cardinal V73() V74() complex-membered ext-real-membered real-membered rational-membered integer-membered natural-membered V135() V136() V137() V139() Element of NAT
(T,X,H) .last() is Element of the_Vertices_of T
len (T,X,H) is non empty ordinal natural V27() ext-real positive non negative finite cardinal V73() V74() non even complex-membered ext-real-membered real-membered rational-membered integer-membered natural-membered V133() V134() V135() V136() V137() V139() Element of NAT
(T,X,H) . (len (T,X,H)) is set
(T,X,H9) .last() is Element of the_Vertices_of T
len (T,X,H9) is non empty ordinal natural V27() ext-real positive non negative finite cardinal V73() V74() non even complex-membered ext-real-membered real-membered rational-membered integer-membered natural-membered V133() V134() V135() V136() V137() V139() Element of NAT
(T,X,H9) . (len (T,X,H9)) is set
(T,X,H9) .vertices() is finite Element of K32((the_Vertices_of T))
(T,X,H9) .vertexSeq() is V7() V10( NAT ) V11( the_Vertices_of T) Function-like finite FinSequence-like FinSubsequence-like VertexSeq of T
K319((the_Vertices_of T),((T,X,H9) .vertexSeq())) is finite Element of K32((the_Vertices_of T))
(T,X,H) .first() is Element of the_Vertices_of T
(T,X,H) . 1 is set
(T,X,H9) .first() is Element of the_Vertices_of T
(T,X,H9) . 1 is set
B is non empty ordinal natural V27() ext-real positive non negative finite cardinal V73() V74() non even complex-membered ext-real-membered real-membered rational-membered integer-membered natural-membered V133() V134() V135() V136() V137() V139() Element of NAT
(T,X,H) . B is set
(len ((T,X,H),(T,X,H9))) + 2 is non empty ordinal natural V27() ext-real positive non negative finite cardinal V73() V74() complex-membered ext-real-membered real-membered rational-membered integer-membered natural-membered V133() V134() V135() V136() V137() V139() Element of NAT
mC is Element of the_Vertices_of T
{mC} is non empty trivial finite 1 -element set
cH is Element of the_Vertices_of T
{cH} is non empty trivial finite 1 -element set
A is Element of the_Vertices_of T
{A} is non empty trivial finite 1 -element set
T is V7() V10( NAT ) Function-like finite [Graph-like] loopless non-multi non-Dmulti simple Dsimple V118() V119() Tree-like set
the_Vertices_of T is non empty set
X is Element of the_Vertices_of T
H is Element of the_Vertices_of T
H9 is Element of the_Vertices_of T
(T,X,H,H9) is Element of the_Vertices_of T
(T,X,H9,H) is Element of the_Vertices_of T
(T,X,H) is non empty V7() V10( NAT ) V11((the_Vertices_of T) \/ (the_Edges_of T)) Function-like finite FinSequence-like FinSubsequence-like Trail-like Path-like Walk of T
the_Edges_of T is set
(the_Vertices_of T) \/ (the_Edges_of T) is non empty set
(T,X,H) .vertices() is finite Element of K32((the_Vertices_of T))
K32((the_Vertices_of T)) is non empty-membered set
(T,X,H) .vertexSeq() is V7() V10( NAT ) V11( the_Vertices_of T) Function-like finite FinSequence-like FinSubsequence-like VertexSeq of T
K319((the_Vertices_of T),((T,X,H) .vertexSeq())) is finite Element of K32((the_Vertices_of T))
(T,H,X) is non empty V7() V10( NAT ) V11((the_Vertices_of T) \/ (the_Edges_of T)) Function-like finite FinSequence-like FinSubsequence-like Trail-like Path-like Walk of T
(T,H,X) .vertices() is finite Element of K32((the_Vertices_of T))
(T,H,X) .vertexSeq() is V7() V10( NAT ) V11( the_Vertices_of T) Function-like finite FinSequence-like FinSubsequence-like VertexSeq of T
K319((the_Vertices_of T),((T,H,X) .vertexSeq())) is finite Element of K32((the_Vertices_of T))
(T,H,H9) is non empty V7() V10( NAT ) V11((the_Vertices_of T) \/ (the_Edges_of T)) Function-like finite FinSequence-like FinSubsequence-like Trail-like Path-like Walk of T
(T,H,H9) .vertices() is finite Element of K32((the_Vertices_of T))
(T,H,H9) .vertexSeq() is V7() V10( NAT ) V11( the_Vertices_of T) Function-like finite FinSequence-like FinSubsequence-like VertexSeq of T
K319((the_Vertices_of T),((T,H,H9) .vertexSeq())) is finite Element of K32((the_Vertices_of T))
(T,H9,H) is non empty V7() V10( NAT ) V11((the_Vertices_of T) \/ (the_Edges_of T)) Function-like finite FinSequence-like FinSubsequence-like Trail-like Path-like Walk of T
(T,H9,H) .vertices() is finite Element of K32((the_Vertices_of T))
(T,H9,H) .vertexSeq() is V7() V10( NAT ) V11( the_Vertices_of T) Function-like finite FinSequence-like FinSubsequence-like VertexSeq of T
K319((the_Vertices_of T),((T,H9,H) .vertexSeq())) is finite Element of K32((the_Vertices_of T))
(T,H9,X) is non empty V7() V10( NAT ) V11((the_Vertices_of T) \/ (the_Edges_of T)) Function-like finite FinSequence-like FinSubsequence-like Trail-like Path-like Walk of T
(T,H9,X) .vertices() is finite Element of K32((the_Vertices_of T))
(T,H9,X) .vertexSeq() is V7() V10( NAT ) V11( the_Vertices_of T) Function-like finite FinSequence-like FinSubsequence-like VertexSeq of T
K319((the_Vertices_of T),((T,H9,X) .vertexSeq())) is finite Element of K32((the_Vertices_of T))
(T,X,H9) is non empty V7() V10( NAT ) V11((the_Vertices_of T) \/ (the_Edges_of T)) Function-like finite FinSequence-like FinSubsequence-like Trail-like Path-like Walk of T
(T,X,H9) .vertices() is finite Element of K32((the_Vertices_of T))
(T,X,H9) .vertexSeq() is V7() V10( NAT ) V11( the_Vertices_of T) Function-like finite FinSequence-like FinSubsequence-like VertexSeq of T
K319((the_Vertices_of T),((T,X,H9) .vertexSeq())) is finite Element of K32((the_Vertices_of T))
((T,X,H) .vertices()) /\ ((T,H,H9) .vertices()) is finite Element of K32((the_Vertices_of T))
(((T,X,H) .vertices()) /\ ((T,H,H9) .vertices())) /\ ((T,H9,X) .vertices()) is finite Element of K32((the_Vertices_of T))
{(T,X,H,H9)} is non empty trivial finite 1 -element set
((T,X,H9) .vertices()) /\ ((T,H9,H) .vertices()) is finite Element of K32((the_Vertices_of T))
(((T,X,H9) .vertices()) /\ ((T,H9,H) .vertices())) /\ ((T,H,X) .vertices()) is finite Element of K32((the_Vertices_of T))
{(T,X,H9,H)} is non empty trivial finite 1 -element set
T is V7() V10( NAT ) Function-like finite [Graph-like] loopless non-multi non-Dmulti simple Dsimple V118() V119() Tree-like set
the_Vertices_of T is non empty set
X is Element of the_Vertices_of T
H is Element of the_Vertices_of T
H9 is Element of the_Vertices_of T
(T,X,H,H9) is Element of the_Vertices_of T
(T,H,X,H9) is Element of the_Vertices_of T
(T,X,H) is non empty V7() V10( NAT ) V11((the_Vertices_of T) \/ (the_Edges_of T)) Function-like finite FinSequence-like FinSubsequence-like Trail-like Path-like Walk of T
the_Edges_of T is set
(the_Vertices_of T) \/ (the_Edges_of T) is non empty set
(T,X,H) .vertices() is finite Element of K32((the_Vertices_of T))
K32((the_Vertices_of T)) is non empty-membered set
(T,X,H) .vertexSeq() is V7() V10( NAT ) V11( the_Vertices_of T) Function-like finite FinSequence-like FinSubsequence-like VertexSeq of T
K319((the_Vertices_of T),((T,X,H) .vertexSeq())) is finite Element of K32((the_Vertices_of T))
(T,H,X) is non empty V7() V10( NAT ) V11((the_Vertices_of T) \/ (the_Edges_of T)) Function-like finite FinSequence-like FinSubsequence-like Trail-like Path-like Walk of T
(T,H,X) .vertices() is finite Element of K32((the_Vertices_of T))
(T,H,X) .vertexSeq() is V7() V10( NAT ) V11( the_Vertices_of T) Function-like finite FinSequence-like FinSubsequence-like VertexSeq of T
K319((the_Vertices_of T),((T,H,X) .vertexSeq())) is finite Element of K32((the_Vertices_of T))
(T,H,H9) is non empty V7() V10( NAT ) V11((the_Vertices_of T) \/ (the_Edges_of T)) Function-like finite FinSequence-like FinSubsequence-like Trail-like Path-like Walk of T
(T,H,H9) .vertices() is finite Element of K32((the_Vertices_of T))
(T,H,H9) .vertexSeq() is V7() V10( NAT ) V11( the_Vertices_of T) Function-like finite FinSequence-like FinSubsequence-like VertexSeq of T
K319((the_Vertices_of T),((T,H,H9) .vertexSeq())) is finite Element of K32((the_Vertices_of T))
(T,H9,H) is non empty V7() V10( NAT ) V11((the_Vertices_of T) \/ (the_Edges_of T)) Function-like finite FinSequence-like FinSubsequence-like Trail-like Path-like Walk of T
(T,H9,H) .vertices() is finite Element of K32((the_Vertices_of T))
(T,H9,H) .vertexSeq() is V7() V10( NAT ) V11( the_Vertices_of T) Function-like finite FinSequence-like FinSubsequence-like VertexSeq of T
K319((the_Vertices_of T),((T,H9,H) .vertexSeq())) is finite Element of K32((the_Vertices_of T))
(T,H9,X) is non empty V7() V10( NAT ) V11((the_Vertices_of T) \/ (the_Edges_of T)) Function-like finite FinSequence-like FinSubsequence-like Trail-like Path-like Walk of T
(T,H9,X) .vertices() is finite Element of K32((the_Vertices_of T))
(T,H9,X) .vertexSeq() is V7() V10( NAT ) V11( the_Vertices_of T) Function-like finite FinSequence-like FinSubsequence-like VertexSeq of T
K319((the_Vertices_of T),((T,H9,X) .vertexSeq())) is finite Element of K32((the_Vertices_of T))
(T,X,H9) is non empty V7() V10( NAT ) V11((the_Vertices_of T) \/ (the_Edges_of T)) Function-like finite FinSequence-like FinSubsequence-like Trail-like Path-like Walk of T
(T,X,H9) .vertices() is finite Element of K32((the_Vertices_of T))
(T,X,H9) .vertexSeq() is V7() V10( NAT ) V11( the_Vertices_of T) Function-like finite FinSequence-like FinSubsequence-like VertexSeq of T
K319((the_Vertices_of T),((T,X,H9) .vertexSeq())) is finite Element of K32((the_Vertices_of T))
((T,X,H) .vertices()) /\ ((T,H,H9) .vertices()) is finite Element of K32((the_Vertices_of T))
(((T,X,H) .vertices()) /\ ((T,H,H9) .vertices())) /\ ((T,H9,X) .vertices()) is finite Element of K32((the_Vertices_of T))
{(T,X,H,H9)} is non empty trivial finite 1 -element set
((T,H,X) .vertices()) /\ ((T,X,H9) .vertices()) is finite Element of K32((the_Vertices_of T))
(((T,H,X) .vertices()) /\ ((T,X,H9) .vertices())) /\ ((T,H9,H) .vertices()) is finite Element of K32((the_Vertices_of T))
{(T,H,X,H9)} is non empty trivial finite 1 -element set
T is V7() V10( NAT ) Function-like finite [Graph-like] loopless non-multi non-Dmulti simple Dsimple V118() V119() Tree-like set
the_Vertices_of T is non empty set
X is Element of the_Vertices_of T
H is Element of the_Vertices_of T
H9 is Element of the_Vertices_of T
(T,X,H,H9) is Element of the_Vertices_of T
(T,H,H9,X) is Element of the_Vertices_of T
(T,H,X,H9) is Element of the_Vertices_of T
T is V7() V10( NAT ) Function-like finite [Graph-like] loopless non-multi non-Dmulti simple Dsimple V118() V119() Tree-like set
the_Vertices_of T is non empty set
X is Element of the_Vertices_of T
H is Element of the_Vertices_of T
H9 is Element of the_Vertices_of T
(T,X,H,H9) is Element of the_Vertices_of T
(T,H9,X,H) is Element of the_Vertices_of T
(T,X,H9,H) is Element of the_Vertices_of T
T is V7() V10( NAT ) Function-like finite [Graph-like] loopless non-multi non-Dmulti simple Dsimple V118() V119() Tree-like set
the_Vertices_of T is non empty set
X is Element of the_Vertices_of T
H is Element of the_Vertices_of T
H9 is Element of the_Vertices_of T
(T,X,H,H9) is Element of the_Vertices_of T
(T,H9,H,X) is Element of the_Vertices_of T
(T,H9,X,H) is Element of the_Vertices_of T
T is V7() V10( NAT ) Function-like finite [Graph-like] loopless non-multi non-Dmulti simple Dsimple V118() V119() Tree-like set
the_Vertices_of T is non empty set
H9 is Element of the_Vertices_of T
X is Element of the_Vertices_of T
H is Element of the_Vertices_of T
(T,X,H) is non empty V7() V10( NAT ) V11((the_Vertices_of T) \/ (the_Edges_of T)) Function-like finite FinSequence-like FinSubsequence-like Trail-like Path-like Walk of T
the_Edges_of T is set
(the_Vertices_of T) \/ (the_Edges_of T) is non empty set
(T,X,H) .vertices() is finite Element of K32((the_Vertices_of T))
K32((the_Vertices_of T)) is non empty-membered set
(T,X,H) .vertexSeq() is V7() V10( NAT ) V11( the_Vertices_of T) Function-like finite FinSequence-like FinSubsequence-like VertexSeq of T
K319((the_Vertices_of T),((T,X,H) .vertexSeq())) is finite Element of K32((the_Vertices_of T))
(T,X,H,H9) is Element of the_Vertices_of T
(T,H,H9) is non empty V7() V10( NAT ) V11((the_Vertices_of T) \/ (the_Edges_of T)) Function-like finite FinSequence-like FinSubsequence-like Trail-like Path-like Walk of T
(T,H,H9) .vertices() is finite Element of K32((the_Vertices_of T))
(T,H,H9) .vertexSeq() is V7() V10( NAT ) V11( the_Vertices_of T) Function-like finite FinSequence-like FinSubsequence-like VertexSeq of T
K319((the_Vertices_of T),((T,H,H9) .vertexSeq())) is finite Element of K32((the_Vertices_of T))
((T,X,H) .vertices()) /\ ((T,H,H9) .vertices()) is finite Element of K32((the_Vertices_of T))
(T,H9,X) is non empty V7() V10( NAT ) V11((the_Vertices_of T) \/ (the_Edges_of T)) Function-like finite FinSequence-like FinSubsequence-like Trail-like Path-like Walk of T
(T,H9,X) .vertices() is finite Element of K32((the_Vertices_of T))
(T,H9,X) .vertexSeq() is V7() V10( NAT ) V11( the_Vertices_of T) Function-like finite FinSequence-like FinSubsequence-like VertexSeq of T
K319((the_Vertices_of T),((T,H9,X) .vertexSeq())) is finite Element of K32((the_Vertices_of T))
(((T,X,H) .vertices()) /\ ((T,H,H9) .vertices())) /\ ((T,H9,X) .vertices()) is finite Element of K32((the_Vertices_of T))
{H9} is non empty trivial finite 1 -element set
T is V7() V10( NAT ) Function-like finite [Graph-like] loopless non-multi non-Dmulti simple Dsimple V118() V119() Tree-like set
the_Vertices_of T is non empty set
X is Element of the_Vertices_of T
(T,X,X,X) is Element of the_Vertices_of T
{X} is non empty trivial finite 1 -element set
(T,X,X) is non empty V7() V10( NAT ) V11((the_Vertices_of T) \/ (the_Edges_of T)) Function-like finite FinSequence-like FinSubsequence-like closed trivial Trail-like Path-like vertex-distinct Walk of T
the_Edges_of T is set
(the_Vertices_of T) \/ (the_Edges_of T) is non empty set
(T,X,X) .vertices() is finite Element of K32((the_Vertices_of T))
K32((the_Vertices_of T)) is non empty-membered set
(T,X,X) .vertexSeq() is V7() V10( NAT ) V11( the_Vertices_of T) Function-like finite FinSequence-like FinSubsequence-like VertexSeq of T
K319((the_Vertices_of T),((T,X,X) .vertexSeq())) is finite Element of K32((the_Vertices_of T))
T is V7() V10( NAT ) Function-like finite [Graph-like] loopless non-multi non-Dmulti simple Dsimple V118() V119() Tree-like set
the_Vertices_of T is non empty set
X is Element of the_Vertices_of T
H is Element of the_Vertices_of T
(T,X,X,H) is Element of the_Vertices_of T
(T,X,H) is non empty V7() V10( NAT ) V11((the_Vertices_of T) \/ (the_Edges_of T)) Function-like finite FinSequence-like FinSubsequence-like Trail-like Path-like Walk of T
the_Edges_of T is set
(the_Vertices_of T) \/ (the_Edges_of T) is non empty set
(T,X,H) .first() is Element of the_Vertices_of T
(T,X,H) . 1 is set
(T,X,H) .vertices() is finite Element of K32((the_Vertices_of T))
K32((the_Vertices_of T)) is non empty-membered set
(T,X,H) .vertexSeq() is V7() V10( NAT ) V11( the_Vertices_of T) Function-like finite FinSequence-like FinSubsequence-like VertexSeq of T
K319((the_Vertices_of T),((T,X,H) .vertexSeq())) is finite Element of K32((the_Vertices_of T))
(T,X,H,X) is Element of the_Vertices_of T
T is V7() V10( NAT ) Function-like finite [Graph-like] loopless non-multi non-Dmulti simple Dsimple V118() V119() Tree-like set
the_Vertices_of T is non empty set
X is Element of the_Vertices_of T
H is Element of the_Vertices_of T
(T,X,H,X) is Element of the_Vertices_of T
(T,X,X,H) is Element of the_Vertices_of T
T is V7() V10( NAT ) Function-like finite [Graph-like] loopless non-multi non-Dmulti simple Dsimple V118() V119() Tree-like set
the_Vertices_of T is non empty set
X is Element of the_Vertices_of T
H is Element of the_Vertices_of T
(T,X,H,H) is Element of the_Vertices_of T
(T,H,X,H) is Element of the_Vertices_of T
T is V7() V10( NAT ) Function-like finite [Graph-like] loopless non-multi non-Dmulti simple Dsimple V118() V119() Tree-like set
the_Vertices_of T is non empty set
the_Edges_of T is set
(the_Vertices_of T) \/ (the_Edges_of T) is non empty set
X is non empty V7() V10( NAT ) V11((the_Vertices_of T) \/ (the_Edges_of T)) Function-like finite FinSequence-like FinSubsequence-like Trail-like Path-like Walk of T
H is non empty V7() V10( NAT ) V11((the_Vertices_of T) \/ (the_Edges_of T)) Function-like finite FinSequence-like FinSubsequence-like Trail-like Path-like Walk of T
H .vertices() is finite Element of K32((the_Vertices_of T))
K32((the_Vertices_of T)) is non empty-membered set
H .vertexSeq() is V7() V10( NAT ) V11( the_Vertices_of T) Function-like finite FinSequence-like FinSubsequence-like VertexSeq of T
K319((the_Vertices_of T),(H .vertexSeq())) is finite Element of K32((the_Vertices_of T))
X .vertices() is finite Element of K32((the_Vertices_of T))
X .vertexSeq() is V7() V10( NAT ) V11( the_Vertices_of T) Function-like finite FinSequence-like FinSubsequence-like VertexSeq of T
K319((the_Vertices_of T),(X .vertexSeq())) is finite Element of K32((the_Vertices_of T))
(X,H) is V7() V10( NAT ) Function-like finite FinSequence-like FinSubsequence-like set
len (X,H) is ordinal natural V27() ext-real non negative finite cardinal V73() V74() complex-membered ext-real-membered real-membered rational-membered integer-membered natural-membered V135() V136() V137() V139() Element of NAT
X . (len (X,H)) is set
H9 is Element of the_Vertices_of T
cH is Element of the_Vertices_of T
(T,H9,cH) is non empty V7() V10( NAT ) V11((the_Vertices_of T) \/ (the_Edges_of T)) Function-like finite FinSequence-like FinSubsequence-like Trail-like Path-like Walk of T
A is Element of the_Vertices_of T
(T,H9,A) is non empty V7() V10( NAT ) V11((the_Vertices_of T) \/ (the_Edges_of T)) Function-like finite FinSequence-like FinSubsequence-like Trail-like Path-like Walk of T
(T,H9,cH,A) is Element of the_Vertices_of T
(T,H9,cH) .vertices() is finite Element of K32((the_Vertices_of T))
(T,H9,cH) .vertexSeq() is V7() V10( NAT ) V11( the_Vertices_of T) Function-like finite FinSequence-like FinSubsequence-like VertexSeq of T
K319((the_Vertices_of T),((T,H9,cH) .vertexSeq())) is finite Element of K32((the_Vertices_of T))
(T,cH,A) is non empty V7() V10( NAT ) V11((the_Vertices_of T) \/ (the_Edges_of T)) Function-like finite FinSequence-like FinSubsequence-like Trail-like Path-like Walk of T
(T,cH,A) .vertices() is finite Element of K32((the_Vertices_of T))
(T,cH,A) .vertexSeq() is V7() V10( NAT ) V11( the_Vertices_of T) Function-like finite FinSequence-like FinSubsequence-like VertexSeq of T
K319((the_Vertices_of T),((T,cH,A) .vertexSeq())) is finite Element of K32((the_Vertices_of T))
((T,H9,cH) .vertices()) /\ ((T,cH,A) .vertices()) is finite Element of K32((the_Vertices_of T))
(T,A,H9) is non empty V7() V10( NAT ) V11((the_Vertices_of T) \/ (the_Edges_of T)) Function-like finite FinSequence-like FinSubsequence-like Trail-like Path-like Walk of T
(T,A,H9) .vertices() is finite Element of K32((the_Vertices_of T))
(T,A,H9) .vertexSeq() is V7() V10( NAT ) V11( the_Vertices_of T) Function-like finite FinSequence-like FinSubsequence-like VertexSeq of T
K319((the_Vertices_of T),((T,A,H9) .vertexSeq())) is finite Element of K32((the_Vertices_of T))
(((T,H9,cH) .vertices()) /\ ((T,cH,A) .vertices())) /\ ((T,A,H9) .vertices()) is finite Element of K32((the_Vertices_of T))
{(X . (len (X,H)))} is non empty trivial finite 1 -element set
{(T,H9,cH,A)} is non empty trivial finite 1 -element set
T is V7() V10( NAT ) Function-like finite [Graph-like] loopless non-multi non-Dmulti simple Dsimple V118() V119() Tree-like set
the_Vertices_of T is non empty set
the_Edges_of T is set
(the_Vertices_of T) \/ (the_Edges_of T) is non empty set
X is non empty V7() V10( NAT ) V11((the_Vertices_of T) \/ (the_Edges_of T)) Function-like finite FinSequence-like FinSubsequence-like Trail-like Path-like Walk of T
H is non empty V7() V10( NAT ) V11((the_Vertices_of T) \/ (the_Edges_of T)) Function-like finite FinSequence-like FinSubsequence-like Trail-like Path-like Walk of T
H9 is non empty V7() V10( NAT ) V11((the_Vertices_of T) \/ (the_Edges_of T)) Function-like finite FinSequence-like FinSubsequence-like Trail-like Path-like Walk of T
cH is non empty V7() V10( NAT ) V11((the_Vertices_of T) \/ (the_Edges_of T)) Function-like finite FinSequence-like FinSubsequence-like Trail-like Path-like Walk of T
H .vertices() is finite Element of K32((the_Vertices_of T))
K32((the_Vertices_of T)) is non empty-membered set
H .vertexSeq() is V7() V10( NAT ) V11( the_Vertices_of T) Function-like finite FinSequence-like FinSubsequence-like VertexSeq of T
K319((the_Vertices_of T),(H .vertexSeq())) is finite Element of K32((the_Vertices_of T))
X .vertices() is finite Element of K32((the_Vertices_of T))
X .vertexSeq() is V7() V10( NAT ) V11( the_Vertices_of T) Function-like finite FinSequence-like FinSubsequence-like VertexSeq of T
K319((the_Vertices_of T),(X .vertexSeq())) is finite Element of K32((the_Vertices_of T))
cH .vertices() is finite Element of K32((the_Vertices_of T))
cH .vertexSeq() is V7() V10( NAT ) V11( the_Vertices_of T) Function-like finite FinSequence-like FinSubsequence-like VertexSeq of T
K319((the_Vertices_of T),(cH .vertexSeq())) is finite Element of K32((the_Vertices_of T))
(X,H) is V7() V10( NAT ) Function-like finite FinSequence-like FinSubsequence-like set
len (X,H) is ordinal natural V27() ext-real non negative finite cardinal V73() V74() complex-membered ext-real-membered real-membered rational-membered integer-membered natural-membered V135() V136() V137() V139() Element of NAT
X . (len (X,H)) is set
(H9,cH) is V7() V10( NAT ) Function-like finite FinSequence-like FinSubsequence-like set
len (H9,cH) is ordinal natural V27() ext-real non negative finite cardinal V73() V74() complex-membered ext-real-membered real-membered rational-membered integer-membered natural-membered V135() V136() V137() V139() Element of NAT
H9 . (len (H9,cH)) is set
A is Element of the_Vertices_of T
A is Element of the_Vertices_of T
(T,A,A) is non empty V7() V10( NAT ) V11((the_Vertices_of T) \/ (the_Edges_of T)) Function-like finite FinSequence-like FinSubsequence-like Trail-like Path-like Walk of T
mA is Element of the_Vertices_of T
(T,A,mA) is non empty V7() V10( NAT ) V11((the_Vertices_of T) \/ (the_Edges_of T)) Function-like finite FinSequence-like FinSubsequence-like Trail-like Path-like Walk of T
(T,A,A) is non empty V7() V10( NAT ) V11((the_Vertices_of T) \/ (the_Edges_of T)) Function-like finite FinSequence-like FinSubsequence-like Trail-like Path-like Walk of T
(T,A,mA) is non empty V7() V10( NAT ) V11((the_Vertices_of T) \/ (the_Edges_of T)) Function-like finite FinSequence-like FinSubsequence-like Trail-like Path-like Walk of T
H9 .vertices() is finite Element of K32((the_Vertices_of T))
H9 .vertexSeq() is V7() V10( NAT ) V11( the_Vertices_of T) Function-like finite FinSequence-like FinSubsequence-like VertexSeq of T
K319((the_Vertices_of T),(H9 .vertexSeq())) is finite Element of K32((the_Vertices_of T))
(T,A,A,mA) is Element of the_Vertices_of T
(T,A,A,mA) is Element of the_Vertices_of T
T is V7() V10( NAT ) Function-like finite [Graph-like] loopless non-multi non-Dmulti simple Dsimple V118() V119() Tree-like set
the_Vertices_of T is non empty set
X is Element of the_Vertices_of T
H is Element of the_Vertices_of T
H9 is Element of the_Vertices_of T
cH is non empty set
meet cH is set
(T,X,H,H9) is Element of the_Vertices_of T
(T,H9,X) is non empty V7() V10( NAT ) V11((the_Vertices_of T) \/ (the_Edges_of T)) Function-like finite FinSequence-like FinSubsequence-like Trail-like Path-like Walk of T
the_Edges_of T is set
(the_Vertices_of T) \/ (the_Edges_of T) is non empty set
(T,H,H9) is non empty V7() V10( NAT ) V11((the_Vertices_of T) \/ (the_Edges_of T)) Function-like finite FinSequence-like FinSubsequence-like Trail-like Path-like Walk of T
(T,X,H9) is non empty V7() V10( NAT ) V11((the_Vertices_of T) \/ (the_Edges_of T)) Function-like finite FinSequence-like FinSubsequence-like Trail-like Path-like Walk of T
(T,X,H) is non empty V7() V10( NAT ) V11((the_Vertices_of T) \/ (the_Edges_of T)) Function-like finite FinSequence-like FinSubsequence-like Trail-like Path-like Walk of T
(T,X,H) .vertices() is finite Element of K32((the_Vertices_of T))
K32((the_Vertices_of T)) is non empty-membered set
(T,X,H) .vertexSeq() is V7() V10( NAT ) V11( the_Vertices_of T) Function-like finite FinSequence-like FinSubsequence-like VertexSeq of T
K319((the_Vertices_of T),((T,X,H) .vertexSeq())) is finite Element of K32((the_Vertices_of T))
(T,X,H9) .vertices() is finite Element of K32((the_Vertices_of T))
(T,X,H9) .vertexSeq() is V7() V10( NAT ) V11( the_Vertices_of T) Function-like finite FinSequence-like FinSubsequence-like VertexSeq of T
K319((the_Vertices_of T),((T,X,H9) .vertexSeq())) is finite Element of K32((the_Vertices_of T))
(T,H,H9) .vertices() is finite Element of K32((the_Vertices_of T))
(T,H,H9) .vertexSeq() is V7() V10( NAT ) V11( the_Vertices_of T) Function-like finite FinSequence-like FinSubsequence-like VertexSeq of T
K319((the_Vertices_of T),((T,H,H9) .vertexSeq())) is finite Element of K32((the_Vertices_of T))
(T,H9,X) .vertices() is finite Element of K32((the_Vertices_of T))
(T,H9,X) .vertexSeq() is V7() V10( NAT ) V11( the_Vertices_of T) Function-like finite FinSequence-like FinSubsequence-like VertexSeq of T
K319((the_Vertices_of T),((T,H9,X) .vertexSeq())) is finite Element of K32((the_Vertices_of T))
((T,X,H) .vertices()) /\ ((T,H,H9) .vertices()) is finite Element of K32((the_Vertices_of T))
(((T,X,H) .vertices()) /\ ((T,H,H9) .vertices())) /\ ((T,H9,X) .vertices()) is finite Element of K32((the_Vertices_of T))
{(T,X,H,H9)} is non empty trivial finite 1 -element set
a is set
b is V7() V10( NAT ) Function-like finite [Graph-like] loopless non-multi non-Dmulti simple Dsimple V118() V119() Tree-like Subgraph of T
the_Vertices_of b is non empty Element of K32((the_Vertices_of T))
b is V7() V10( NAT ) Function-like finite [Graph-like] loopless non-multi non-Dmulti simple Dsimple V118() V119() Tree-like Subgraph of T
the_Vertices_of b is non empty Element of K32((the_Vertices_of T))
b is V7() V10( NAT ) Function-like finite [Graph-like] loopless non-multi non-Dmulti simple Dsimple V118() V119() Tree-like Subgraph of T
the_Vertices_of b is non empty Element of K32((the_Vertices_of T))
T is V7() V10( NAT ) Function-like finite [Graph-like] loopless non-multi non-Dmulti simple Dsimple V118() V119() Tree-like set
X is finite set
H is ordinal natural V27() ext-real non negative finite cardinal V73() V74() set
H9 is non empty finite set
card H9 is non empty ordinal natural V27() ext-real positive non negative finite cardinal V73() V74() complex-membered ext-real-membered real-membered rational-membered integer-membered natural-membered V133() V134() V135() V136() V137() V139() Element of omega
meet H9 is set
cH is Element of H9
{cH} is non empty trivial finite 1 -element set
A is V7() V10( NAT ) Function-like finite [Graph-like] loopless non-multi non-Dmulti simple Dsimple V118() V119() Tree-like Subgraph of T
the_Vertices_of A is non empty Element of K32((the_Vertices_of T))
the_Vertices_of T is non empty set
K32((the_Vertices_of T)) is non empty-membered set
choose H9 is Element of H9
{(choose H9)} is non empty trivial finite 1 -element set
H9 \ {(choose H9)} is finite Element of K32(H9)
K32(H9) is non empty-membered finite V39() set
card (H9 \ {(choose H9)}) is ordinal natural V27() ext-real non negative finite cardinal V73() V74() complex-membered ext-real-membered real-membered rational-membered integer-membered natural-membered V135() V136() V137() V139() Element of omega
card {(choose H9)} is non empty ordinal natural V27() ext-real positive non negative finite cardinal V73() V74() complex-membered ext-real-membered real-membered rational-membered integer-membered natural-membered V133() V134() V135() V136() V137() V139() Element of omega
(card H9) - (card {(choose H9)}) is V27() ext-real V73() V74() set
H - 1 is V27() ext-real V73() V74() set
1 - 1 is V27() ext-real V73() V74() set
A is non empty finite set
mA is set
cA is set
meet A is set
choose A is Element of A
{(choose A)} is non empty trivial finite 1 -element set
H9 \ {(choose A)} is finite Element of K32(H9)
card (H9 \ {(choose A)}) is ordinal natural V27() ext-real non negative finite cardinal V73() V74() complex-membered ext-real-membered real-membered rational-membered integer-membered natural-membered V135() V136() V137() V139() Element of omega
card {(choose A)} is non empty ordinal natural V27() ext-real positive non negative finite cardinal V73() V74() complex-membered ext-real-membered real-membered rational-membered integer-membered natural-membered V133() V134() V135() V136() V137() V139() Element of omega
(card H9) - (card {(choose A)}) is V27() ext-real V73() V74() set
{(choose H9),(choose A)} is non empty finite set
meet {(choose H9),(choose A)} is set
(choose H9) /\ (choose A) is set
B is non empty finite set
mB is set
a is set
meet B is set
mA is non empty set
choose mA is Element of mA
mB is non empty set
choose mB is Element of mB
mC is non empty set
choose mC is Element of mC
union {(choose H9),(choose A)} is set
cc is set
union A is set
aa is set
union B is set
bb is set
the_Vertices_of T is non empty set
s is V7() V10( NAT ) Function-like finite [Graph-like] loopless non-multi non-Dmulti simple Dsimple V118() V119() Tree-like Subgraph of T
the_Vertices_of s is non empty Element of K32((the_Vertices_of T))
K32((the_Vertices_of T)) is non empty-membered set
ni is V7() V10( NAT ) Function-like finite [Graph-like] loopless non-multi non-Dmulti simple Dsimple V118() V119() Tree-like Subgraph of T
the_Vertices_of ni is non empty Element of K32((the_Vertices_of T))
im is V7() V10( NAT ) Function-like finite [Graph-like] loopless non-multi non-Dmulti simple Dsimple V118() V119() Tree-like Subgraph of T
the_Vertices_of im is non empty Element of K32((the_Vertices_of T))
s is set
a is Element of the_Vertices_of T
b is Element of the_Vertices_of T
c is Element of the_Vertices_of T
H is non empty set
meet H is set
H9 is finite set
card H9 is ordinal natural V27() ext-real non negative finite cardinal V73() V74() complex-membered ext-real-membered real-membered rational-membered integer-membered natural-membered V135() V136() V137() V139() Element of omega