:: CHORD semantic presentation

REAL is non empty non trivial non finite complex-membered ext-real-membered real-membered V141() V148() V149() V151() set

bool REAL is non empty non trivial non finite set
COMPLEX is non empty non trivial non finite complex-membered V141() set

bool omega is non empty non trivial non finite set
bool NAT is non empty non trivial non finite set

(0 + 1) - 1 is complex V25() integer ext-real set

(P - G) + 1 is complex V25() integer ext-real set

(P - S) + 1 is complex V25() integer ext-real set
((P - S) + 1) + 2 is complex V25() integer ext-real set
((P - G) + 1) - 3 is complex V25() integer ext-real set
(P - S) + 3 is complex V25() integer ext-real set
((P - S) + 3) - 3 is complex V25() integer ext-real set
P - (G + 2) is complex V25() integer ext-real set
S is non empty complex V25() integer non even ext-real set
G is non empty complex V25() integer non even ext-real set

(G + 1) + (- 1) is complex V25() integer ext-real set
S + (- 1) is complex V25() integer ext-real set

(S - 1) + (- 1) is complex V25() integer ext-real set
G is non empty complex V25() integer non even ext-real set
S is non empty complex V25() integer non even ext-real set
S + 2 is non empty complex V25() integer non even ext-real set

(S + 1) + 1 is non empty complex V25() integer non even ext-real set

(1 + 2) - 2 is complex V25() integer ext-real set

G - (2 * 1) is non empty complex V25() integer non even ext-real set

G . S is set

rng G is finite set
G . ((G . S) .. G) is set

rng G is non empty finite set
bool (rng G) is non empty finite V32() set
S is non empty finite Element of bool (rng G)
P is Element of S

x is set

rng ((S,(len G)) -cut G) is finite set

rng G is finite set

S is set

(G,P) is finite set

rng ((P,(len G)) -cut G) is finite set
G . (S .. G) is set

((P,(len G)) -cut G) . x is set

G . x is set

(x + P) + (- P) is complex V25() integer ext-real set
(len G) + (- P) is complex V25() integer ext-real set

(len G) - P is complex V25() integer ext-real set
((len G) - P) + 1 is complex V25() integer ext-real set
((P,(len G)) -cut G) . (x + 1) is set

P is set

(G,(x + 1)) is finite set

rng (((x + 1),(len G)) -cut G) is finite set
(S,x) is finite set

rng ((x,(len S)) -cut S) is finite set

G . (() + x) is set
S . x is set

G . (x + 1) is set

(len G) - x is complex V25() integer ext-real set
0 + ((len G) - x) is complex V25() integer ext-real set

(- 1) + x is complex V25() integer ext-real set
1 + (- 1) is complex V25() integer ext-real set
x + (- 1) is complex V25() integer ext-real set

x + ((len G) - x) is complex V25() integer ext-real set

((n + x) + 1) + (- 1) is complex V25() integer ext-real set
((len S) + 1) + (- 1) is complex V25() integer ext-real set

(((x + 1),(len G)) -cut G) . x is set

(((x + 1),(len G)) -cut G) . (n + 1) is set

G . ((x + 1) + n) is set

G . ((x + n) + 1) is set
S . (x + n) is set
((x,(len S)) -cut S) . (n + 1) is set
((x,(len S)) -cut S) . x is set
x is set

(((x + 1),(len G)) -cut G) . n is set
((x,(len S)) -cut S) . n is set

((x,(len S)) -cut S) . n is set
(((x + 1),(len G)) -cut G) . n is set
G is set

bool S is non empty finite V32() set

the_Vertices_of G is non empty set

bool () is non empty set
S is Element of bool ()
G .edgesBetween S is Element of bool ()

bool () is non empty set
G .edgesInto S is Element of bool ()
G .edgesOutOf S is Element of bool ()
() /\ () is Element of bool ()

x is set
x is set
H is set
n is non empty Element of bool ()
G .edgesBetween n is Element of bool ()
G .edgesInto n is Element of bool ()
G .edgesOutOf n is Element of bool ()
() /\ () is Element of bool ()
the_Edges_of P is Element of bool ()

the_Vertices_of P is non empty set

bool [:(),():] is non empty set

bool [:(),():] is non empty set

() . H is set
() . H is set

() . H is set

() . H is set

the_Vertices_of G is non empty set

() \/ () is non empty set

bool () is non empty set

K426((),()) is finite Element of bool ()

the_Vertices_of G is non empty set

bool () is non empty set

() \/ () is non empty set
S is Element of bool ()
() \ S is Element of bool ()
G .edgesBetween (() \ S) is Element of bool ()
bool () is non empty set
G .edgesInto (() \ S) is Element of bool ()
G .edgesOutOf (() \ S) is Element of bool ()
(G .edgesInto (() \ S)) /\ (G .edgesOutOf (() \ S)) is Element of bool ()

the_Vertices_of P is non empty set

() \/ () is non empty set

x . (len x) is set
the_Edges_of P is Element of bool ()

K426((),()) is finite Element of bool ()

K426((),()) is finite Element of bool ()
G .edgesBetween () is Element of bool ()
G .edgesInto () is Element of bool ()
G .edgesOutOf () is Element of bool ()
() /\ () is Element of bool ()
the_Vertices_of P is non empty Element of bool ()
x is set

x . n is set
G .edgesBetween () is Element of bool ()
G .edgesInto () is Element of bool ()
G .edgesOutOf () is Element of bool ()
() /\ () is Element of bool ()

the_Vertices_of G is non empty set

() \/ () is non empty set
S is set
P is set
{S,P} is non empty finite set

bool () is non empty set

K426((),()) is finite Element of bool ()

x . 1 is set
x is set
{x} is non empty trivial finite 1 -element set
n is set
{S,P} \ {x} is finite Element of bool {S,P}
bool {S,P} is non empty finite V32() set

x . (x .find n) is set

x . y is set

x . (y + 1) is set
{P} is non empty trivial finite 1 -element set
{S} is non empty trivial finite 1 -element set
{S,P} \ {S} is finite Element of bool {S,P}
{S} is non empty trivial finite 1 -element set
{P} is non empty trivial finite 1 -element set
{S,P} \ {P} is finite Element of bool {S,P}
x is set

the_Vertices_of G is non empty set

bool () is non empty set

() \/ () is non empty set
S is non empty Element of bool ()
G .edgesBetween S is Element of bool ()
bool () is non empty set
G .edgesInto S is Element of bool ()
G .edgesOutOf S is Element of bool ()
() /\ () is Element of bool ()

the_Vertices_of P is non empty set

() \/ () is non empty set
the_Vertices_of P is non empty Element of bool ()
the_Edges_of P is Element of bool ()

K426((),()) is finite Element of bool ()

K426((),()) is finite Element of bool ()
G .edgesBetween () is Element of bool ()
G .edgesInto () is Element of bool ()
G .edgesOutOf () is Element of bool ()
() /\ () is Element of bool ()
G .edgesBetween () is Element of bool ()
G .edgesInto () is Element of bool ()
G .edgesOutOf () is Element of bool ()
() /\ () is Element of bool ()

the_Vertices_of G is non empty set

() \/ () is non empty set
the_Vertices_of S is non empty set

() \/ () is non empty set

P . 1 is set

P . (len P) is set

x . 1 is set

x . (len x) is set

the_Vertices_of G is non empty set

() \/ () is non empty set

S . P is set
S . x is set

the_Vertices_of G is non empty set

() \/ () is non empty set

bool () is non empty set

K426((),()) is finite Element of bool ()

S . 1 is set
P is set
x is set
x is set

(G .walkOf (P,x,x)) .last() is Element of the_Vertices_of G

(G .walkOf (P,x,x)) . (len (G .walkOf (P,x,x))) is set

Seg (len (G .walkOf (P,x,x))) is non empty finite len (G .walkOf (P,x,x)) -element complex-membered ext-real-membered real-membered rational-membered integer-membered natural-membered V146() V147() V148() V149() V150() Element of bool NAT

((G .walkOf (P,x,x)) .append S) . 3 is set
(G .walkOf (P,x,x)) . 3 is set

((G .walkOf (P,x,x)) .append S) . y is set
((G .walkOf (P,x,x)) .append S) . C is set

((G .walkOf (P,x,x)) .append S) .first() is Element of the_Vertices_of G
((G .walkOf (P,x,x)) .append S) . 1 is set
(G .walkOf (P,x,x)) .first() is Element of the_Vertices_of G
(G .walkOf (P,x,x)) . 1 is set

S . b is set
Seg (len ((G .walkOf (P,x,x)) .append S)) is non empty finite len ((G .walkOf (P,x,x)) .append S) -element complex-membered ext-real-membered real-membered rational-membered integer-membered natural-membered V146() V147() V148() V149() V150() Element of bool NAT

S . (C + 1) is set

S . (v + 1) is set

((G .walkOf (P,x,x)) .append S) . y is set
((G .walkOf (P,x,x)) .append S) . C is set

the_Vertices_of G is non empty set

() \/ () is non empty set

bool () is non empty set

K426((),()) is finite Element of bool ()

K426((),()) is finite Element of bool ()

bool () is non empty set

K426((),()) is finite Element of bool ()

K426((),()) is finite Element of bool ()
() /\ () is finite Element of bool ()

S . 1 is set

S . (len S) is set
{(),()} is non empty finite Element of bool ()

P . 1 is set

P . (len P) is set

(S .append P) .first() is Element of the_Vertices_of G
(S .append P) . 1 is set

(S .append P) . x is set
S . x is set

((len (S .append P)) + 1) + (- 1) is complex V25() integer ext-real set

((len S) + (len P)) + (- 1) is complex V25() integer ext-real set

S . x is set
(S .append P) . x is set
S . n is set
(S .append P) . n is set
(S .append P) . x is set
S . x is set

(S .append P) . n is set

P . (H + 1) is set

P . ((2 * 0) + 1) is set
P . C is set
S . ((2 * 0) + 1) is set
(S .append P) . x is set
(S .append P) . n is set