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
{ H1(b1) where b1 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 <= b1 & b1 <= len T & S1[b1] ) } 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