:: HELLY semantic presentation

K32(REAL) is set

K32(omega) is non trivial non finite set
K32(NAT) is non trivial non finite set

T . 1 is set

(<*(T . 1)*> ^' T) . H is set
<*(T . 1)*> . 1 is set
T . H is set

(<*(T . 1)*> ^' T) . H is set
T . H is set

{ 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

cA is set
mA . cA is set
T . cA is set
A . cA is set

T . 1 is set

X is set
<*(T . 1)*> . X is set
T . X is set

T . 1 is set

X . 1 is set

(T,X) . H is set
T . H is set

T . H is set
X . H is set
(T,X) . H is set

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)

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

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

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

the_Vertices_of T is non empty set

() \/ () is non empty set

X .cut (H,H9) is V7() V10( NAT ) V11(() \/ ()) Function-like finite FinSequence-like FinSubsequence-like Walk of T

X .cut (cH,A) is V7() V10( NAT ) V11(() \/ ()) Function-like finite FinSequence-like FinSubsequence-like Walk of T

the_Vertices_of T is non empty set

() \/ () is non empty set

X .cut (H,H9) is V7() V10( NAT ) V11(() \/ ()) Function-like finite FinSequence-like FinSubsequence-like Walk of T

the_Vertices_of T is non empty set

() \/ () is non empty set

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(() \/ ()) Function-like finite FinSequence-like FinSubsequence-like Walk of T

(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) - 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) - 1 is non empty V27() ext-real V73() V74() non even set

X .cut (mA,cA) is V7() V10( NAT ) V11(() \/ ()) Function-like finite FinSequence-like FinSubsequence-like Walk of T

(X .cut (mA,cA)) . (B + 1) is set

X . (H + B) is set

(H9 + 1) - 1 is non empty V27() ext-real V73() V74() non even set

the_Vertices_of T is non empty set

() \/ () is non empty set

the_Vertices_of T is non empty set

() \/ () is non empty set
X is non empty V7() V10( NAT ) V11(() \/ ()) Function-like finite FinSequence-like FinSubsequence-like Walk of T
H is non empty V7() V10( NAT ) V11(() \/ ()) Function-like finite FinSequence-like FinSubsequence-like Walk of T
X .vertices() is finite Element of K32(())
K32(()) is non empty-membered set

K319((),()) is finite Element of K32(())
H .vertices() is finite Element of K32(())

K319((),()) is finite Element of K32(())
H9 is set

X . cH is set

H . cH is set

the_Vertices_of T is non empty set

() \/ () is non empty set
X is non empty V7() V10( NAT ) V11(() \/ ()) Function-like finite FinSequence-like FinSubsequence-like Walk of T
H is non empty V7() V10( NAT ) V11(() \/ ()) Function-like finite FinSequence-like FinSubsequence-like Walk of T
X .edges() is finite Element of K32(())
K32(()) is set

K319((),()) is finite Element of K32(())
H .edges() is finite Element of K32(())

K319((),()) is finite Element of K32(())
H9 is set

X . cH is set

H . cH is set

the_Vertices_of T is non empty set

() \/ () is non empty set
X is non empty V7() V10( NAT ) V11(() \/ ()) Function-like finite FinSequence-like FinSubsequence-like Walk of T
H is non empty V7() V10( NAT ) V11(() \/ ()) Function-like finite FinSequence-like FinSubsequence-like Walk of T

X . (len X) is set

H . 1 is set

cH is set
X . cH is set
(X .append H) . cH is set

X . (len X) is set

H . 1 is set

X . (len X) is set

H . 1 is set

the_Vertices_of T is non empty set

() \/ () is non empty set
X is non empty V7() V10( NAT ) V11(() \/ ()) Function-like finite FinSequence-like FinSubsequence-like Walk of T

X . (len X) is set
H is non empty V7() V10( NAT ) V11(() \/ ()) Function-like finite FinSequence-like FinSubsequence-like Walk of T

H . 1 is set

1 - 1 is V27() ext-real V73() V74() set
H9 - 1 is V27() ext-real V73() V74() set

(X .append H) . (1 + cH) is set

H . (cH + 1) is set
(X .append H) . H9 is set
H . H9 is set

the_Vertices_of T is non empty set

() \/ () is non empty set

X . (len X) is set

H . 1 is set
X .edges() is finite Element of K32(())
K32(()) is set

K319((),()) is finite Element of K32(())
H .edges() is finite Element of K32(())

K319((),()) is finite Element of K32(())

X . cH is set
(X .append H) . cH is set
X . A is set
(X .append H) . A is set

(X .append H) . A is set

H . (mA + 1) is set

X . cH is set
(X .append H) . cH is set

(X .append H) . cH is set
H . (B + 1) is set

the_Vertices_of T is non empty set

() \/ () is non empty set

X . (len X) is set

H . 1 is set
X .edges() is finite Element of K32(())
K32(()) is set

K319((),()) is finite Element of K32(())
H .edges() is finite Element of K32(())

K319((),()) is finite Element of K32(())

X . 1 is set
H .vertices() is finite Element of K32(())
K32(()) is non empty-membered set

K319((),()) is finite Element of K32(())

H . (len H) is set
X .vertices() is finite Element of K32(())

K319((),()) is finite Element of K32(())
() /\ () is finite Element of K32(())
{(),()} is non empty finite set

(X .append H) . cH is set
(X .append H) . A is set

H . (A + 1) is set

H . (mA + 1) is set

H . (cA + 1) is set

H . (B + 1) is set

X . cH is set

X . ((2 * 0) + 1) is set

X . cH is set
X . A is set

the_Vertices_of T is non empty set

() \/ () is non empty set

X . (len X) is set

H . 1 is set
X .vertices() is finite Element of K32(())
K32(()) is non empty-membered set

K319((),()) is finite Element of K32(())
H .vertices() is finite Element of K32(())

K319((),()) is finite Element of K32(())
() /\ () is finite Element of K32(())
{()} is non empty trivial finite 1 -element set

(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

(X .append H) . (len (X .append H)) is set

X . 1 is set

H . (len H) is set

X . 1 is set
X .edges() is finite Element of K32(())
K32(()) is set

K319((),()) is finite Element of K32(())
H .edges() is finite Element of K32(())

K319((),()) is finite Element of K32(())
() /\ () is finite Element of K32(())
cH is set

A is Element of the_Vertices_of T
H . mA is set

H . (mA + 1) is set
A is Element of the_Vertices_of T
H . (mA + 2) is set

cA is Element of the_Vertices_of T
X . C is set

X . (C + 1) is set
B is Element of the_Vertices_of T
X . (C + 2) is set

{cA,B} is non empty finite set

{A,A} is non empty finite set
{(),()} is non empty finite set

the_Vertices_of T is non empty set

() \/ () is non empty set

X . (len X) is set

H . 1 is set

H . (len H) is set

X . 1 is set
X .edges() is finite Element of K32(())
K32(()) is set

K319((),()) is finite Element of K32(())
H .edges() is finite Element of K32(())

K319((),()) is finite Element of K32(())
X .vertices() is finite Element of K32(())
K32(()) is non empty-membered set

K319((),()) is finite Element of K32(())
H .vertices() is finite Element of K32(())

K319((),()) is finite Element of K32(())
() /\ () is finite Element of K32(())
{(),()} is non empty finite set

(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

(X .append H) . (len (X .append H)) is set

the_Vertices_of T is non empty set

() \/ () is non empty set
X is non empty V7() V10( NAT ) V11(() \/ ()) Function-like finite FinSequence-like FinSubsequence-like Walk of T

H is non empty V7() V10( NAT ) V11(() \/ ()) Function-like finite FinSequence-like FinSubsequence-like Walk of T

H9 is non empty ordinal natural V27() ext-real positive non negative finite cardinal V73() V74() non even 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 - 1 is non empty V27() ext-real V73() V74() non even set

X . A is set

X . (A + 2) is set

X . (A + 1) is set

H . (A + 2) is set
H . A is set
H . (A + 1) is set

the_Vertices_of T is non empty set

() \/ () is non empty set
X is non empty V7() V10( NAT ) V11(() \/ ()) Function-like finite FinSequence-like FinSubsequence-like Walk of T

X . 1 is set
H is non empty V7() V10( NAT ) V11(() \/ ()) Function-like finite FinSequence-like FinSubsequence-like Walk of T

H . 1 is set

(len (X,H)) - 1 is V27() ext-real V73() V74() set

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)

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

H . cH is set

H . (cH + 2) is set
H . (len (X,H)) is set

X . cH is set
X . (cH + 2) is set
X . (len (X,H)) is set
mA is set

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

the_Vertices_of T is non empty set

() \/ () is non empty set
X is non empty V7() V10( NAT ) V11(() \/ ()) Function-like finite FinSequence-like FinSubsequence-like Walk of T

X . 1 is set
H is non empty V7() V10( NAT ) V11(() \/ ()) Function-like finite FinSequence-like FinSubsequence-like Walk of T

H . 1 is set

the_Vertices_of T is non empty set

() \/ () is non empty set
X is non empty V7() V10( NAT ) V11(() \/ ()) Function-like finite FinSequence-like FinSubsequence-like Walk of T

X . 1 is set
H is non empty V7() V10( NAT ) V11(() \/ ()) Function-like finite FinSequence-like FinSubsequence-like Walk of T

H . 1 is set

X . ((len (X,H)) + 2) is set
H . ((len (X,H)) + 2) is set

X . (len (X,H)) is set

X . ((len (X,H)) + 1) is set
H . (len (X,H)) is set

H . ((len (X,H)) + 1) is set

the_Vertices_of T is non empty set

() \/ () is non empty set
X is non empty