:: GLIB_001 semantic presentation

REAL is set
NAT is non empty non trivial V21() V22() V23() non finite cardinal limit_cardinal Element of K32(REAL)
K32(REAL) is non empty set
COMPLEX is set
NAT is non empty non trivial V21() V22() V23() non finite cardinal limit_cardinal set
K32(NAT) is non empty non trivial non finite set
K32(NAT) is non empty non trivial non finite set
{} is empty Relation-like non-empty empty-yielding NAT -defined Function-like one-to-one constant functional V21() V22() V23() V25() V26() V27() V28() V29() V30() ext-real non positive non negative finite finite-yielding V49() cardinal {} -element FinSequence-like FinSubsequence-like FinSequence-membered Function-yielding V86() set
1 is non empty V21() V22() V23() V27() V28() V29() V30() ext-real positive non negative finite cardinal Element of NAT
2 is non empty V21() V22() V23() V27() V28() V29() V30() ext-real positive non negative finite cardinal Element of NAT
3 is non empty V21() V22() V23() V27() V28() V29() V30() ext-real positive non negative finite cardinal Element of NAT
_GraphSelectors is non empty Element of K32(NAT)
card {} is empty Relation-like non-empty empty-yielding NAT -defined Function-like one-to-one constant functional V21() V22() V23() V25() V26() V27() V28() V29() V30() ext-real non positive non negative finite finite-yielding V49() cardinal {} -element FinSequence-like FinSubsequence-like FinSequence-membered Function-yielding V86() set
Seg 1 is non empty trivial finite 1 -element Element of K32(NAT)
{1} is non empty trivial finite V49() 1 -element set
Seg 2 is non empty finite 2 -element Element of K32(NAT)
{1,2} is non empty finite V49() set
Seg 3 is non empty finite 3 -element Element of K32(NAT)
K5(1,2,3) is non empty finite set
0 is empty Relation-like non-empty empty-yielding NAT -defined Function-like one-to-one constant functional V21() V22() V23() V25() V26() V27() V28() V29() V30() ext-real non positive non negative finite finite-yielding V49() cardinal {} -element FinSequence-like FinSubsequence-like FinSequence-membered Function-yielding V86() Element of NAT
G2 is non empty V21() V22() V23() V27() V28() V29() V30() ext-real positive non negative finite cardinal non even Element of NAT
G1 is non empty V21() V22() V23() V27() V28() V29() V30() ext-real positive non negative finite cardinal non even Element of NAT
G1 + 2 is non empty V21() V22() V23() V27() V28() V29() V30() ext-real positive non negative finite cardinal non even Element of NAT
G1 + 1 is non empty V21() V22() V23() V27() V28() V29() V30() ext-real positive non negative finite cardinal even Element of NAT
G2 + 1 is non empty V21() V22() V23() V27() V28() V29() V30() ext-real positive non negative finite cardinal even Element of NAT
(G1 + 1) + 1 is non empty V21() V22() V23() V27() V28() V29() V30() ext-real positive non negative finite cardinal non even Element of NAT
G2 - 0 is non empty V28() V29() V30() ext-real positive non negative set
(G1 + 2) - 2 is V28() V29() V30() ext-real set
G1 is set
G2 is Relation-like NAT -defined G1 -valued Function-like finite FinSequence-like FinSubsequence-like FinSequence of G1
K32(G2) is non empty finite V49() set
len G2 is V21() V22() V23() V27() V28() V29() V30() ext-real non negative finite cardinal Element of NAT
W1 is Relation-like NAT -defined G1 -valued Function-like finite FinSubsequence-like Element of K32(G2)
Seq W1 is Relation-like NAT -defined Function-like finite FinSequence-like FinSubsequence-like set
len (Seq W1) is V21() V22() V23() V27() V28() V29() V30() ext-real non negative finite cardinal Element of NAT
dom W1 is finite Element of K32(NAT)
Sgm (dom W1) is Relation-like NAT -defined NAT -valued Function-like finite FinSequence-like FinSubsequence-like FinSequence of NAT
(Sgm (dom W1)) * W1 is Relation-like NAT -defined G1 -valued Function-like finite set
dom G2 is finite Element of K32(NAT)
Seg (len G2) is finite len G2 -element Element of K32(NAT)
rng (Sgm (dom W1)) is finite Element of K32(NAT)
len (Sgm (dom W1)) is V21() V22() V23() V27() V28() V29() V30() ext-real non negative finite cardinal Element of NAT
card (dom W1) is V21() V22() V23() V27() V28() V29() V30() ext-real non negative finite cardinal Element of NAT
card W1 is V21() V22() V23() V27() V28() V29() V30() ext-real non negative finite cardinal Element of NAT
G1 is set
G2 is Relation-like NAT -defined G1 -valued Function-like finite FinSequence-like FinSubsequence-like FinSequence of G1
K32(G2) is non empty finite V49() set
dom G2 is finite Element of K32(NAT)
W1 is Relation-like NAT -defined G1 -valued Function-like finite FinSubsequence-like Element of K32(G2)
Seq W1 is Relation-like NAT -defined Function-like finite FinSequence-like FinSubsequence-like set
dom (Seq W1) is finite Element of K32(NAT)
W2 is V21() V22() V23() V27() V28() V29() V30() ext-real non negative finite cardinal Element of NAT
(Seq W1) . W2 is set
dom W1 is finite Element of K32(NAT)
Sgm (dom W1) is Relation-like NAT -defined NAT -valued Function-like finite FinSequence-like FinSubsequence-like FinSequence of NAT
(Sgm (dom W1)) . W2 is set
vs is V21() V22() V23() V27() V28() V29() V30() ext-real non negative finite cardinal set
Seg vs is finite vs -element Element of K32(NAT)
(Sgm (dom W1)) * W1 is Relation-like NAT -defined G1 -valued Function-like finite set
dom ((Sgm (dom W1)) * W1) is finite Element of K32(NAT)
W1 . ((Sgm (dom W1)) . W2) is set
[((Sgm (dom W1)) . W2),((Seq W1) . W2)] is V1() set
dom (Sgm (dom W1)) is finite Element of K32(NAT)
G2 . ((Sgm (dom W1)) . W2) is set
G1 is set
G2 is Relation-like NAT -defined G1 -valued Function-like finite FinSequence-like FinSubsequence-like FinSequence of G1
K32(G2) is non empty finite V49() set
W1 is Relation-like NAT -defined G1 -valued Function-like finite FinSubsequence-like Element of K32(G2)
Seq W1 is Relation-like NAT -defined Function-like finite FinSequence-like FinSubsequence-like set
len (Seq W1) is V21() V22() V23() V27() V28() V29() V30() ext-real non negative finite cardinal Element of NAT
card W1 is V21() V22() V23() V27() V28() V29() V30() ext-real non negative finite cardinal Element of NAT
dom W1 is finite Element of K32(NAT)
Sgm (dom W1) is Relation-like NAT -defined NAT -valued Function-like finite FinSequence-like FinSubsequence-like FinSequence of NAT
(Sgm (dom W1)) * W1 is Relation-like NAT -defined G1 -valued Function-like finite set
rng (Sgm (dom W1)) is finite Element of K32(NAT)
W2 is V21() V22() V23() V27() V28() V29() V30() ext-real non negative finite cardinal set
Seg W2 is finite W2 -element Element of K32(NAT)
dom (Seq W1) is finite Element of K32(NAT)
dom (Sgm (dom W1)) is finite Element of K32(NAT)
card (dom W1) is V21() V22() V23() V27() V28() V29() V30() ext-real non negative finite cardinal Element of NAT
Seg (card (dom W1)) is finite card (dom W1) -element Element of K32(NAT)
W2 is V21() V22() V23() V27() V28() V29() V30() ext-real non negative finite cardinal set
Seg W2 is finite W2 -element Element of K32(NAT)
G1 is set
G2 is Relation-like NAT -defined G1 -valued Function-like finite FinSequence-like FinSubsequence-like FinSequence of G1
K32(G2) is non empty finite V49() set
W1 is Relation-like NAT -defined G1 -valued Function-like finite FinSubsequence-like Element of K32(G2)
Seq W1 is Relation-like NAT -defined Function-like finite FinSequence-like FinSubsequence-like set
dom (Seq W1) is finite Element of K32(NAT)
dom W1 is finite Element of K32(NAT)
Sgm (dom W1) is Relation-like NAT -defined NAT -valued Function-like finite FinSequence-like FinSubsequence-like FinSequence of NAT
dom (Sgm (dom W1)) is finite Element of K32(NAT)
rng (Sgm (dom W1)) is finite Element of K32(NAT)
W2 is V21() V22() V23() V27() V28() V29() V30() ext-real non negative finite cardinal set
Seg W2 is finite W2 -element Element of K32(NAT)
(Sgm (dom W1)) * W1 is Relation-like NAT -defined G1 -valued Function-like finite set
G1 is Relation-like NAT -defined Function-like finite [Graph-like] set
the_Vertices_of G1 is non empty set
choose (the_Vertices_of G1) is Element of the_Vertices_of G1
<*(choose (the_Vertices_of G1))*> is non empty trivial Relation-like NAT -defined the_Vertices_of G1 -valued Function-like constant finite 1 -element FinSequence-like FinSubsequence-like FinSequence of the_Vertices_of G1
W2 is Relation-like NAT -defined the_Vertices_of G1 -valued Function-like finite FinSequence-like FinSubsequence-like FinSequence of the_Vertices_of G1
len W2 is V21() V22() V23() V27() V28() V29() V30() ext-real non negative finite cardinal Element of NAT
y is V21() V22() V23() V27() V28() V29() V30() ext-real non negative finite cardinal Element of NAT
W2 . y is set
y + 1 is non empty V21() V22() V23() V27() V28() V29() V30() ext-real positive non negative finite cardinal Element of NAT
W2 . (y + 1) is set
G1 is Relation-like NAT -defined Function-like finite [Graph-like] set
the_Edges_of G1 is set
the_Vertices_of G1 is non empty set
<*> (the_Edges_of G1) is empty Relation-like non-empty empty-yielding NAT -defined the_Edges_of G1 -valued Function-like one-to-one constant functional V21() V22() V23() V25() V26() V27() V28() V29() V30() ext-real non positive non negative finite finite-yielding V49() cardinal {} -element FinSequence-like FinSubsequence-like FinSequence-membered Function-yielding V86() FinSequence of the_Edges_of G1
choose (the_Vertices_of G1) is Element of the_Vertices_of G1
<*(choose (the_Vertices_of G1))*> is non empty trivial Relation-like NAT -defined the_Vertices_of G1 -valued Function-like constant finite 1 -element FinSequence-like FinSubsequence-like FinSequence of the_Vertices_of G1
len (<*> (the_Edges_of G1)) is empty Relation-like non-empty empty-yielding NAT -defined Function-like one-to-one constant functional V21() V22() V23() V25() V26() V27() V28() V29() V30() ext-real non positive non negative finite finite-yielding V49() cardinal {} -element FinSequence-like FinSubsequence-like FinSequence-membered Function-yielding V86() Element of NAT
(len (<*> (the_Edges_of G1))) + 1 is non empty V21() V22() V23() V27() V28() V29() V30() ext-real positive non negative finite cardinal Element of NAT
W2 is Relation-like NAT -defined the_Vertices_of G1 -valued Function-like finite FinSequence-like FinSubsequence-like FinSequence of the_Vertices_of G1
len W2 is V21() V22() V23() V27() V28() V29() V30() ext-real non negative finite cardinal Element of NAT
y is V21() V22() V23() V27() V28() V29() V30() ext-real non negative finite cardinal Element of NAT
W2 . y is set
y + 1 is non empty V21() V22() V23() V27() V28() V29() V30() ext-real positive non negative finite cardinal Element of NAT
W2 . (y + 1) is set
(<*> (the_Edges_of G1)) . y is empty Relation-like non-empty empty-yielding NAT -defined Function-like one-to-one constant functional V21() V22() V23() V25() V26() V27() V28() V29() V30() ext-real non positive non negative finite finite-yielding V49() cardinal {} -element FinSequence-like FinSubsequence-like FinSequence-membered Function-yielding V86() set
G1 is Relation-like NAT -defined Function-like finite [Graph-like] set
the_Vertices_of G1 is non empty set
the_Edges_of G1 is set
(the_Vertices_of G1) \/ (the_Edges_of G1) is non empty set
W1 is set
W2 is Element of (the_Vertices_of G1) \/ (the_Edges_of G1)
<*W2*> is non empty trivial Relation-like NAT -defined (the_Vertices_of G1) \/ (the_Edges_of G1) -valued Function-like constant finite 1 -element FinSequence-like FinSubsequence-like FinSequence of (the_Vertices_of G1) \/ (the_Edges_of G1)
len <*W2*> is non empty V21() V22() V23() V27() V28() V29() V30() ext-real positive non negative finite cardinal Element of NAT
<*W2*> . 1 is set
y is non empty V21() V22() V23() V27() V28() V29() V30() ext-real positive non negative finite cardinal non even Element of NAT
<*W2*> . y is set
y + 2 is non empty V21() V22() V23() V27() V28() V29() V30() ext-real positive non negative finite cardinal non even Element of NAT
<*W2*> . (y + 2) is set
y + 1 is non empty V21() V22() V23() V27() V28() V29() V30() ext-real positive non negative finite cardinal even Element of NAT
<*W2*> . (y + 1) is set
G1 is Relation-like NAT -defined Function-like finite [Graph-like] set
the_Vertices_of G1 is non empty set
the_Edges_of G1 is set
(the_Vertices_of G1) \/ (the_Edges_of G1) is non empty set
G2 is Relation-like NAT -defined (the_Vertices_of G1) \/ (the_Edges_of G1) -valued Function-like finite FinSequence-like FinSubsequence-like (G1)
len G2 is V21() V22() V23() V27() V28() V29() V30() ext-real non negative finite cardinal Element of NAT
G1 is Relation-like NAT -defined Function-like finite [Graph-like] set
the_Vertices_of G1 is non empty set
G2 is Element of the_Vertices_of G1
<*G2*> is non empty trivial Relation-like NAT -defined the_Vertices_of G1 -valued Function-like constant finite 1 -element FinSequence-like FinSubsequence-like FinSequence of the_Vertices_of G1
the_Edges_of G1 is set
(the_Vertices_of G1) \/ (the_Edges_of G1) is non empty set
vs is Element of (the_Vertices_of G1) \/ (the_Edges_of G1)
<*vs*> is non empty trivial Relation-like NAT -defined (the_Vertices_of G1) \/ (the_Edges_of G1) -valued Function-like constant finite 1 -element FinSequence-like FinSubsequence-like FinSequence of (the_Vertices_of G1) \/ (the_Edges_of G1)
vs is Relation-like NAT -defined (the_Vertices_of G1) \/ (the_Edges_of G1) -valued Function-like finite FinSequence-like FinSubsequence-like FinSequence of (the_Vertices_of G1) \/ (the_Edges_of G1)
len vs is V21() V22() V23() V27() V28() V29() V30() ext-real non negative finite cardinal Element of NAT
vs . 1 is set
vs is non empty V21() V22() V23() V27() V28() V29() V30() ext-real positive non negative finite cardinal non even Element of NAT
len <*G2*> is non empty V21() V22() V23() V27() V28() V29() V30() ext-real positive non negative finite cardinal Element of NAT
vs . vs is set
vs + 2 is non empty V21() V22() V23() V27() V28() V29() V30() ext-real positive non negative finite cardinal non even Element of NAT
vs . (vs + 2) is set
vs + 1 is non empty V21() V22() V23() V27() V28() V29() V30() ext-real positive non negative finite cardinal even Element of NAT
vs . (vs + 1) is set
G1 is Relation-like NAT -defined Function-like finite [Graph-like] set
G2 is set
W1 is set
W2 is set
<*G2,W2,W1*> is non empty Relation-like NAT -defined Function-like finite 3 -element FinSequence-like FinSubsequence-like set
the_Vertices_of G1 is non empty set
the_Edges_of G1 is set
(the_Vertices_of G1) \/ (the_Edges_of G1) is non empty set
choose (the_Vertices_of G1) is Element of the_Vertices_of G1
(G1,(choose (the_Vertices_of G1))) is Relation-like NAT -defined (the_Vertices_of G1) \/ (the_Edges_of G1) -valued Function-like finite FinSequence-like FinSubsequence-like (G1)
<*(choose (the_Vertices_of G1))*> is non empty trivial Relation-like NAT -defined the_Vertices_of G1 -valued Function-like constant finite 1 -element FinSequence-like FinSubsequence-like FinSequence of the_Vertices_of G1
vs is Relation-like NAT -defined (the_Vertices_of G1) \/ (the_Edges_of G1) -valued Function-like finite FinSequence-like FinSubsequence-like FinSequence of (the_Vertices_of G1) \/ (the_Edges_of G1)
vs . 1 is set
vs . 2 is set
vs is non empty V21() V22() V23() V27() V28() V29() V30() ext-real positive non negative finite cardinal non even Element of NAT
vs + 2 is non empty V21() V22() V23() V27() V28() V29() V30() ext-real positive non negative finite cardinal non even Element of NAT
len vs is V21() V22() V23() V27() V28() V29() V30() ext-real non negative finite cardinal Element of NAT
n is non empty V21() V22() V23() V27() V28() V29() V30() ext-real positive non negative finite cardinal non even Element of NAT
2 + 1 is non empty V21() V22() V23() V27() V28() V29() V30() ext-real positive non negative finite cardinal Element of NAT
2 * 1 is V21() V22() V23() V27() V28() V29() V30() ext-real non negative finite cardinal even Element of NAT
2 * 0 is empty Relation-like non-empty empty-yielding NAT -defined Function-like one-to-one constant functional V21() V22() V23() V25() V26() V27() V28() V29() V30() ext-real non positive non negative finite finite-yielding V49() cardinal {} -element FinSequence-like FinSubsequence-like FinSequence-membered Function-yielding V86() even Element of NAT
vs . n is set
n + 2 is non empty V21() V22() V23() V27() V28() V29() V30() ext-real positive non negative finite cardinal non even Element of NAT
vs . (n + 2) is set
n + 1 is non empty V21() V22() V23() V27() V28() V29() V30() ext-real positive non negative finite cardinal even Element of NAT
vs . (n + 1) is set
G1 is Relation-like NAT -defined Function-like finite [Graph-like] set
the_Vertices_of G1 is non empty set
the_Edges_of G1 is set
(the_Vertices_of G1) \/ (the_Edges_of G1) is non empty set
G2 is Relation-like NAT -defined (the_Vertices_of G1) \/ (the_Edges_of G1) -valued Function-like finite FinSequence-like FinSubsequence-like (G1)
G2 . 1 is set
len G2 is non empty V21() V22() V23() V27() V28() V29() V30() ext-real positive non negative finite cardinal non even Element of NAT
G2 . (len G2) is set
(len G2) + 1 is non empty V21() V22() V23() V27() V28() V29() V30() ext-real positive non negative finite cardinal even Element of NAT
1 + 1 is non empty V21() V22() V23() V27() V28() V29() V30() ext-real positive non negative finite cardinal Element of NAT
2 * 1 is V21() V22() V23() V27() V28() V29() V30() ext-real non negative finite cardinal even Element of NAT
(len G2) - (2 * 1) is non empty V28() V29() V30() ext-real non even set
W1 is non empty V21() V22() V23() V27() V28() V29() V30() ext-real positive non negative finite cardinal non even Element of NAT
W1 + 2 is non empty V21() V22() V23() V27() V28() V29() V30() ext-real positive non negative finite cardinal non even Element of NAT
G2 . W1 is set
W1 + 1 is non empty V21() V22() V23() V27() V28() V29() V30() ext-real positive non negative finite cardinal even Element of NAT
G2 . (W1 + 1) is set
G1 is Relation-like NAT -defined Function-like finite [Graph-like] set
the_Vertices_of G1 is non empty set
the_Edges_of G1 is set
(the_Vertices_of G1) \/ (the_Edges_of G1) is non empty set
W1 is V21() V22() V23() V27() V28() V29() V30() ext-real non negative finite cardinal set
G2 is Relation-like NAT -defined (the_Vertices_of G1) \/ (the_Edges_of G1) -valued Function-like finite FinSequence-like FinSubsequence-like (G1)
len G2 is non empty V21() V22() V23() V27() V28() V29() V30() ext-real positive non negative finite cardinal non even Element of NAT
G2 . W1 is set
(G1,G2) is Element of the_Vertices_of G1
G2 . 1 is set
(G1,G2) is Element of the_Vertices_of G1
G2 . (len G2) is set
W1 + 2 is non empty V21() V22() V23() V27() V28() V29() V30() ext-real positive non negative finite cardinal Element of NAT
G2 . (W1 + 2) is set
W2 is V21() V22() V23() V27() V28() V29() V30() ext-real non negative finite cardinal Element of NAT
W2 + 1 is non empty V21() V22() V23() V27() V28() V29() V30() ext-real positive non negative finite cardinal Element of NAT
G2 . (W2 + 1) is set
G1 is Relation-like NAT -defined Function-like finite [Graph-like] set
the_Vertices_of G1 is non empty set
the_Edges_of G1 is set
(the_Vertices_of G1) \/ (the_Edges_of G1) is non empty set
G2 is Relation-like NAT -defined (the_Vertices_of G1) \/ (the_Edges_of G1) -valued Function-like finite FinSequence-like FinSubsequence-like (G1)
Rev G2 is Relation-like NAT -defined (the_Vertices_of G1) \/ (the_Edges_of G1) -valued Function-like finite FinSequence-like FinSubsequence-like FinSequence of (the_Vertices_of G1) \/ (the_Edges_of G1)
W2 is Relation-like NAT -defined (the_Vertices_of G1) \/ (the_Edges_of G1) -valued Function-like finite FinSequence-like FinSubsequence-like FinSequence of (the_Vertices_of G1) \/ (the_Edges_of G1)
len W2 is V21() V22() V23() V27() V28() V29() V30() ext-real non negative finite cardinal Element of NAT
len G2 is non empty V21() V22() V23() V27() V28() V29() V30() ext-real positive non negative finite cardinal non even Element of NAT
W2 . 1 is set
(G1,G2) is Element of the_Vertices_of G1
G2 . (len G2) is set
y is non empty V21() V22() V23() V27() V28() V29() V30() ext-real positive non negative finite cardinal non even Element of NAT
(len G2) - y is V28() V29() V30() ext-real even set
((len G2) - y) + 1 is non empty V28() V29() V30() ext-real non even set
y + 1 is non empty V21() V22() V23() V27() V28() V29() V30() ext-real positive non negative finite cardinal even Element of NAT
(len G2) - (y + 1) is non empty V28() V29() V30() ext-real non even set
((len G2) - (y + 1)) + 1 is V28() V29() V30() ext-real even set
y + 2 is non empty V21() V22() V23() V27() V28() V29() V30() ext-real positive non negative finite cardinal non even Element of NAT
(len G2) - (y + 2) is V28() V29() V30() ext-real even set
((len G2) - (y + 2)) + 1 is non empty V28() V29() V30() ext-real non even set
(y + 1) + 1 is non empty V21() V22() V23() V27() V28() V29() V30() ext-real positive non negative finite cardinal non even Element of NAT
dom G2 is finite Element of K32(NAT)
W2 . (y + 1) is set
n is V21() V22() V23() V27() V28() V29() V30() ext-real non negative finite cardinal even Element of NAT
G2 . n is set
n is non empty V21() V22() V23() V27() V28() V29() V30() ext-real positive non negative finite cardinal non even Element of NAT
n + 1 is non empty V21() V22() V23() V27() V28() V29() V30() ext-real positive non negative finite cardinal even Element of NAT
G2 . (n + 1) is set
W2 . y is set
x is non empty V21() V22() V23() V27() V28() V29() V30() ext-real positive non negative finite cardinal non even Element of NAT
G2 . x is set
n + 2 is non empty V21() V22() V23() V27() V28() V29() V30() ext-real positive non negative finite cardinal non even Element of NAT
G2 . (n + 2) is set
1 + 0 is non empty V21() V22() V23() V27() V28() V29() V30() ext-real positive non negative finite cardinal Element of NAT
(len G2) - 1 is V28() V29() V30() ext-real even set
((len G2) - 1) + 1 is non empty V28() V29() V30() ext-real non even set
G2 . n is set
W2 . (y + 2) is set
W1 is Relation-like NAT -defined (the_Vertices_of G1) \/ (the_Edges_of G1) -valued Function-like finite FinSequence-like FinSubsequence-like (G1)
W2 is Relation-like NAT -defined (the_Vertices_of G1) \/ (the_Edges_of G1) -valued Function-like finite FinSequence-like FinSubsequence-like (G1)
Rev W2 is Relation-like NAT -defined (the_Vertices_of G1) \/ (the_Edges_of G1) -valued Function-like finite FinSequence-like FinSubsequence-like FinSequence of (the_Vertices_of G1) \/ (the_Edges_of G1)
Rev W1 is Relation-like NAT -defined (the_Vertices_of G1) \/ (the_Edges_of G1) -valued Function-like finite FinSequence-like FinSubsequence-like FinSequence of (the_Vertices_of G1) \/ (the_Edges_of G1)
G1 is Relation-like NAT -defined Function-like finite [Graph-like] set
the_Vertices_of G1 is non empty set
the_Edges_of G1 is set
(the_Vertices_of G1) \/ (the_Edges_of G1) is non empty set
G2 is Relation-like NAT -defined (the_Vertices_of G1) \/ (the_Edges_of G1) -valued Function-like finite FinSequence-like FinSubsequence-like (G1)
(G1,G2) is Element of the_Vertices_of G1
len G2 is non empty V21() V22() V23() V27() V28() V29() V30() ext-real positive non negative finite cardinal non even Element of NAT
G2 . (len G2) is set
W1 is Relation-like NAT -defined (the_Vertices_of G1) \/ (the_Edges_of G1) -valued Function-like finite FinSequence-like FinSubsequence-like (G1)
(G1,W1) is Element of the_Vertices_of G1
W1 . 1 is set
G2 ^' W1 is Relation-like NAT -defined (the_Vertices_of G1) \/ (the_Edges_of G1) -valued Function-like finite FinSequence-like FinSubsequence-like FinSequence of (the_Vertices_of G1) \/ (the_Edges_of G1)
len (G2 ^' W1) is V21() V22() V23() V27() V28() V29() V30() ext-real non negative finite cardinal Element of NAT
vs is non empty V21() V22() V23() V27() V28() V29() V30() ext-real positive non negative finite cardinal non even Element of NAT
(G2 ^' W1) . vs is set
vs + 2 is non empty V21() V22() V23() V27() V28() V29() V30() ext-real positive non negative finite cardinal non even Element of NAT
(G2 ^' W1) . (vs + 2) is set
vs + 1 is non empty V21() V22() V23() V27() V28() V29() V30() ext-real positive non negative finite cardinal even Element of NAT
(G2 ^' W1) . (vs + 1) is set
(vs + 2) - 2 is V28() V29() V30() ext-real set
(len G2) - 0 is non empty V28() V29() V30() ext-real positive non negative set
G2 . vs is set
(vs + 2) - 1 is V28() V29() V30() ext-real even set
G2 . (vs + 1) is set
G2 . (vs + 2) is set
(len G2) + 1 is non empty V21() V22() V23() V27() V28() V29() V30() ext-real positive non negative finite cardinal even Element of NAT
(vs + 1) + 1 is non empty V21() V22() V23() V27() V28() V29() V30() ext-real positive non negative finite cardinal non even Element of NAT
n is V21() V22() V23() V27() V28() V29() V30() ext-real non negative finite cardinal set
(len G2) + n is non empty V21() V22() V23() V27() V28() V29() V30() ext-real positive non negative finite cardinal Element of NAT
x is V21() V22() V23() V27() V28() V29() V30() ext-real non negative finite cardinal even Element of NAT
x + 1 is non empty V21() V22() V23() V27() V28() V29() V30() ext-real positive non negative finite cardinal non even Element of NAT
0 + 1 is non empty V21() V22() V23() V27() V28() V29() V30() ext-real positive non negative finite cardinal Element of NAT
(len (G2 ^' W1)) + 1 is non empty V21() V22() V23() V27() V28() V29() V30() ext-real positive non negative finite cardinal Element of NAT
len W1 is non empty V21() V22() V23() V27() V28() V29() V30() ext-real positive non negative finite cardinal non even Element of NAT
(len G2) + (len W1) is non empty V21() V22() V23() V27() V28() V29() V30() ext-real positive non negative finite cardinal even Element of NAT
((len G2) + (len W1)) + 1 is non empty V21() V22() V23() V27() V28() V29() V30() ext-real positive non negative finite cardinal non even Element of NAT
(len W1) + 1 is non empty V21() V22() V23() V27() V28() V29() V30() ext-real positive non negative finite cardinal even Element of NAT
(len G2) + ((len W1) + 1) is non empty V21() V22() V23() V27() V28() V29() V30() ext-real positive non negative finite cardinal non even Element of NAT
x + (len G2) is non empty V21() V22() V23() V27() V28() V29() V30() ext-real positive non negative finite cardinal non even Element of NAT
W1 . (x + 1) is set
1 + 1 is non empty V21() V22() V23() V27() V28() V29() V30() ext-real positive non negative finite cardinal Element of NAT
(1 + 1) + 0 is non empty V21() V22() V23() V27() V28() V29() V30() ext-real positive non negative finite cardinal Element of NAT
W1 . (1 + 1) is set
2 * 1 is V21() V22() V23() V27() V28() V29() V30() ext-real non negative finite cardinal even Element of NAT
xaa1 is V21() V22() V23() V27() V28() V29() V30() ext-real non negative finite cardinal even Element of NAT
x - xaa1 is V28() V29() V30() ext-real even set
(x + (len G2)) - (len G2) is V28() V29() V30() ext-real even set
2 + (len G2) is non empty V21() V22() V23() V27() V28() V29() V30() ext-real positive non negative finite cardinal non even Element of NAT
(2 + (len G2)) - (len G2) is V28() V29() V30() ext-real even set
W2 is V21() V22() V23() V27() V28() V29() V30() ext-real non negative finite cardinal even Element of NAT
W2 + 1 is non empty V21() V22() V23() V27() V28() V29() V30() ext-real positive non negative finite cardinal non even Element of NAT
(W2 + 1) + 1 is non empty V21() V22() V23() V27() V28() V29() V30() ext-real positive non negative finite cardinal even Element of NAT
((W2 + 1) + 1) - 1 is non empty V28() V29() V30() ext-real non even set
1 + 1 is non empty V21() V22() V23() V27() V28() V29() V30() ext-real positive non negative finite cardinal Element of NAT
(1 + 1) - 1 is V28() V29() V30() ext-real set
(len W1) - 0 is non empty V28() V29() V30() ext-real positive non negative set
es is non empty V21() V22() V23() V27() V28() V29() V30() ext-real positive non negative finite cardinal non even Element of NAT
es + 1 is non empty V21() V22() V23() V27() V28() V29() V30() ext-real positive non negative finite cardinal even Element of NAT
(es + 1) - 1 is non empty V28() V29() V30() ext-real non even set
W1 . (es + 1) is set
(len G2) + es is non empty V21() V22() V23() V27() V28() V29() V30() ext-real positive non negative finite cardinal even Element of NAT
(G2 ^' W1) . ((len G2) + es) is set
es + 2 is non empty V21() V22() V23() V27() V28() V29() V30() ext-real positive non negative finite cardinal non even Element of NAT
W1 . (es + 2) is set
W2 + (1 + 1) is non empty V21() V22() V23() V27() V28() V29() V30() ext-real positive non negative finite cardinal Element of NAT
(len G2) + W2 is non empty V21() V22() V23() V27() V28() V29() V30() ext-real positive non negative finite cardinal non even Element of NAT
((len G2) + W2) + 2 is non empty V21() V22() V23() V27() V28() V29() V30() ext-real positive non negative finite cardinal non even Element of NAT
W1 . (W2 + 1) is set
vs is V21() V22() V23() V27() V28() V29() V30() ext-real non negative finite cardinal even Element of NAT
vs + 1 is non empty V21() V22() V23() V27() V28() V29() V30() ext-real positive non negative finite cardinal non even Element of NAT
len W1 is non empty V21() V22() V23() V27() V28() V29() V30() ext-real positive non negative finite cardinal non even Element of NAT
(len G2) + (len W1) is non empty V21() V22() V23() V27() V28() V29() V30() ext-real positive non negative finite cardinal even Element of NAT
(G2 ^' W1) . 1 is set
(G1,G2) is Element of the_Vertices_of G1
G2 . 1 is set
G1 is Relation-like NAT -defined Function-like finite [Graph-like] set
the_Vertices_of G1 is non empty set
the_Edges_of G1 is set
(the_Vertices_of G1) \/ (the_Edges_of G1) is non empty set
W1 is V21() V22() V23() V27() V28() V29() V30() ext-real non negative finite cardinal set
W2 is V21() V22() V23() V27() V28() V29() V30() ext-real non negative finite cardinal set
G2 is Relation-like NAT -defined (the_Vertices_of G1) \/ (the_Edges_of G1) -valued Function-like finite FinSequence-like FinSubsequence-like (G1)
len G2 is non empty V21() V22() V23() V27() V28() V29() V30() ext-real positive non negative finite cardinal non even Element of NAT
(W1,W2) -cut G2 is Relation-like NAT -defined (the_Vertices_of G1) \/ (the_Edges_of G1) -valued Function-like finite FinSequence-like FinSubsequence-like FinSequence of (the_Vertices_of G1) \/ (the_Edges_of G1)
len ((W1,W2) -cut G2) is V21() V22() V23() V27() V28() V29() V30() ext-real non negative finite cardinal Element of NAT
vs is non empty V21() V22() V23() V27() V28() V29() V30() ext-real positive non negative finite cardinal non even set
(len ((W1,W2) -cut G2)) + vs is non empty V21() V22() V23() V27() V28() V29() V30() ext-real positive non negative finite cardinal Element of NAT
((len ((W1,W2) -cut G2)) + vs) - vs is V28() V29() V30() ext-real set
vs is non empty V21() V22() V23() V27() V28() V29() V30() ext-real positive non negative finite cardinal non even set
vs + 1 is non empty V21() V22() V23() V27() V28() V29() V30() ext-real positive non negative finite cardinal even Element of NAT
(vs + 1) - vs is non empty V28() V29() V30() ext-real non even set
n is non empty V21() V22() V23() V27() V28() V29() V30() ext-real positive non negative finite cardinal non even Element of NAT
n - 1 is V28() V29() V30() ext-real even set
n is V21() V22() V23() V27() V28() V29() V30() ext-real non negative finite cardinal Element of NAT
n + 1 is non empty V21() V22() V23() V27() V28() V29() V30() ext-real positive non negative finite cardinal Element of NAT
0 + 1 is non empty V21() V22() V23() V27() V28() V29() V30() ext-real positive non negative finite cardinal Element of NAT
((W1,W2) -cut G2) . (0 + 1) is set
W1 + 0 is V21() V22() V23() V27() V28() V29() V30() ext-real non negative finite cardinal Element of NAT
G2 . (W1 + 0) is set
G2 . W1 is set
(G1,G2,W1) is Element of the_Vertices_of G1
((W1,W2) -cut G2) . 1 is set
x is non empty V21() V22() V23() V27() V28() V29() V30() ext-real positive non negative finite cardinal non even Element of NAT
vs + x is non empty V21() V22() V23() V27() V28() V29() V30() ext-real positive non negative finite cardinal even Element of NAT
(vs + x) - 1 is non empty V28() V29() V30() ext-real non even set
x - 1 is V28() V29() V30() ext-real even set
x + 1 is non empty V21() V22() V23() V27() V28() V29() V30() ext-real positive non negative finite cardinal even Element of NAT
(x + 1) + 1 is non empty V21() V22() V23() V27() V28() V29() V30() ext-real positive non negative finite cardinal non even Element of NAT
((W1,W2) -cut G2) . ((x + 1) + 1) is set
W1 + (x + 1) is non empty V21() V22() V23() V27() V28() V29() V30() ext-real positive non negative finite cardinal Element of NAT
G2 . (W1 + (x + 1)) is set
(len ((W1,W2) -cut G2)) + W1 is V21() V22() V23() V27() V28() V29() V30() ext-real non negative finite cardinal Element of NAT
x + W1 is non empty V21() V22() V23() V27() V28() V29() V30() ext-real positive non negative finite cardinal Element of NAT
W2 + 1 is non empty V21() V22() V23() V27() V28() V29() V30() ext-real positive non negative finite cardinal Element of NAT
x + vs is non empty V21() V22() V23() V27() V28() V29() V30() ext-real positive non negative finite cardinal even Element of NAT
W1 + x is non empty V21() V22() V23() V27() V28() V29() V30() ext-real positive non negative finite cardinal Element of NAT
(len G2) - 0 is non empty V28() V29() V30() ext-real positive non negative set
(W1 + x) - 1 is V28() V29() V30() ext-real set
xaa1 is non empty V21() V22() V23() V27() V28() V29() V30() ext-real positive non negative finite cardinal non even Element of NAT
G2 . xaa1 is set
xaa1 + 2 is non empty V21() V22() V23() V27() V28() V29() V30() ext-real positive non negative finite cardinal non even Element of NAT
G2 . (xaa1 + 2) is set
xaa1 + 1 is non empty V21() V22() V23() V27() V28() V29() V30() ext-real positive non negative finite cardinal even Element of NAT
G2 . (xaa1 + 1) is set
(len ((W1,W2) -cut G2)) - 0 is V28() V29() V30() ext-real non negative set
W2 is V21() V22() V23() V27() V28() V29() V30() ext-real non negative finite cardinal even Element of NAT
W2 + 1 is non empty V21() V22() V23() V27() V28() V29() V30() ext-real positive non negative finite cardinal non even Element of NAT
((W1,W2) -cut G2) . (W2 + 1) is set
W1 + W2 is V21() V22() V23() V27() V28() V29() V30() ext-real non negative finite cardinal Element of NAT
G2 . (W1 + W2) is set
((W1,W2) -cut G2) . x is set
x + 2 is non empty V21() V22() V23() V27() V28() V29() V30() ext-real positive non negative finite cardinal non even Element of NAT
((W1,W2) -cut G2) . (x + 2) is set
((W1,W2) -cut G2) . (x + 1) is set
G1 is Relation-like NAT -defined Function-like finite [Graph-like] set
the_Vertices_of G1 is non empty set
the_Edges_of G1 is set
(the_Vertices_of G1) \/ (the_Edges_of G1) is non empty set
W1 is V21() V22() V23() V27() V28() V29() V30() ext-real non negative finite cardinal Element of NAT
W2 is V21() V22() V23() V27() V28() V29() V30() ext-real non negative finite cardinal Element of NAT
G2 is Relation-like NAT -defined (the_Vertices_of G1) \/ (the_Edges_of G1) -valued Function-like finite FinSequence-like FinSubsequence-like (G1)
len G2 is non empty V21() V22() V23() V27() V28() V29() V30() ext-real positive non negative finite cardinal non even Element of NAT
G2 . W1 is set
G2 . W2 is set
(G1,G2,1,W1) is Relation-like NAT -defined (the_Vertices_of G1) \/ (the_Edges_of G1) -valued Function-like finite FinSequence-like FinSubsequence-like (G1)
(G1,G2,W2,(len G2)) is Relation-like NAT -defined (the_Vertices_of G1) \/ (the_Edges_of G1) -valued Function-like finite FinSequence-like FinSubsequence-like (G1)
(G1,(G1,G2,1,W1),(G1,G2,W2,(len G2))) is Relation-like NAT -defined (the_Vertices_of G1) \/ (the_Edges_of G1) -valued Function-like finite FinSequence-like FinSubsequence-like (G1)
G1 is Relation-like NAT -defined Function-like finite [Graph-like] set
the_Vertices_of G1 is non empty set
the_Edges_of G1 is set
(the_Vertices_of G1) \/ (the_Edges_of G1) is non empty set
G2 is Relation-like NAT -defined (the_Vertices_of G1) \/ (the_Edges_of G1) -valued Function-like finite FinSequence-like FinSubsequence-like (G1)
(G1,G2) is Element of the_Vertices_of G1
len G2 is non empty V21() V22() V23() V27() V28() V29() V30() ext-real positive non negative finite cardinal non even Element of NAT
G2 . (len G2) is set
W1 is set
(G1,G2) .adj W1 is Element of the_Vertices_of G1
(G1,(G1,G2),((G1,G2) .adj W1),W1) is Relation-like NAT -defined (the_Vertices_of G1) \/ (the_Edges_of G1) -valued Function-like finite FinSequence-like FinSubsequence-like (G1)
(G1,G2,(G1,(G1,G2),((G1,G2) .adj W1),W1)) is Relation-like NAT -defined (the_Vertices_of G1) \/ (the_Edges_of G1) -valued Function-like finite FinSequence-like FinSubsequence-like (G1)
G1 is Relation-like NAT -defined Function-like finite [Graph-like] set
the_Vertices_of G1 is non empty set
the_Edges_of G1 is set
(the_Vertices_of G1) \/ (the_Edges_of G1) is non empty set
G2 is Relation-like NAT -defined (the_Vertices_of G1) \/ (the_Edges_of G1) -valued Function-like finite FinSequence-like FinSubsequence-like (G1)
len G2 is non empty V21() V22() V23() V27() V28() V29() V30() ext-real positive non negative finite cardinal non even Element of NAT
(len G2) + 1 is non empty V21() V22() V23() V27() V28() V29() V30() ext-real positive non negative finite cardinal even Element of NAT
W1 is V21() V22() V23() V27() V28() V29() V30() ext-real non negative finite cardinal even Element of NAT
W1 div 2 is V21() V22() V23() V27() V28() V29() V30() ext-real non negative finite cardinal Element of NAT
y is Relation-like NAT -defined Function-like finite FinSequence-like FinSubsequence-like set
len y is V21() V22() V23() V27() V28() V29() V30() ext-real non negative finite cardinal Element of NAT
dom y is finite Element of K32(NAT)
2 * (W1 div 2) is V21() V22() V23() V27() V28() V29() V30() ext-real non negative finite cardinal even Element of NAT
vs is set
rng y is finite set
vs is set
y . vs is set
Seg (W1 div 2) is finite W1 div 2 -element Element of K32(NAT)
vs is V21() V22() V23() V27() V28() V29() V30() ext-real non negative finite cardinal Element of NAT
vs * 2 is V21() V22() V23() V27() V28() V29() V30() ext-real non negative finite cardinal even Element of NAT
n is V21() V22() V23() V27() V28() V29() V30() ext-real non negative finite cardinal even Element of NAT
n - 1 is non empty V28() V29() V30() ext-real non even set
1 * 2 is V21() V22() V23() V27() V28() V29() V30() ext-real non negative finite cardinal even Element of NAT
(W1 div 2) * 2 is V21() V22() V23() V27() V28() V29() V30() ext-real non negative finite cardinal even Element of NAT
xaa1 is non empty V21() V22() V23() V27() V28() V29() V30() ext-real positive non negative finite cardinal non even Element of NAT
W1 - 1 is non empty V28() V29() V30() ext-real non even set
G2 . xaa1 is set
(G1,G2,xaa1) is Element of the_Vertices_of G1
vs is Relation-like NAT -defined the_Vertices_of G1 -valued Function-like finite FinSequence-like FinSubsequence-like FinSequence of the_Vertices_of G1
vs is V21() V22() V23() V27() V28() V29() V30() ext-real non negative finite cardinal Element of NAT
vs + 1 is non empty V21() V22() V23() V27() V28() V29() V30() ext-real positive non negative finite cardinal Element of NAT
vs . (vs + 1) is set
len vs is V21() V22() V23() V27() V28() V29() V30() ext-real non negative finite cardinal Element of NAT
2 * vs is V21() V22() V23() V27() V28() V29() V30() ext-real non negative finite cardinal even Element of NAT
n is V21() V22() V23() V27() V28() V29() V30() ext-real non negative finite cardinal even Element of NAT
n - 1 is non empty V28() V29() V30() ext-real non even set
vs * 2 is V21() V22() V23() V27() V28() V29() V30() ext-real non negative finite cardinal even Element of NAT
((len G2) + 1) - 1 is non empty V28() V29() V30() ext-real non even set
xaa1 is non empty V21() V22() V23() V27() V28() V29() V30() ext-real positive non negative finite cardinal non even Element of NAT
G2 . xaa1 is set
xaa1 + 2 is non empty V21() V22() V23() V27() V28() V29() V30() ext-real positive non negative finite cardinal non even Element of NAT
G2 . (xaa1 + 2) is set
xaa1 + 1 is non empty V21() V22() V23() V27() V28() V29() V30() ext-real positive non negative finite cardinal even Element of NAT
G2 . (xaa1 + 1) is set
dom vs is finite Element of K32(NAT)
2 * (vs + 1) is V21() V22() V23() V27() V28() V29() V30() ext-real non negative finite cardinal even Element of NAT
(2 * (vs + 1)) - 1 is non empty V28() V29() V30() ext-real non even set
G2 . ((2 * (vs + 1)) - 1) is set
n + 1 is non empty V21() V22() V23() V27() V28() V29() V30() ext-real positive non negative finite cardinal non even Element of NAT
G2 . (n + 1) is set
vs . vs is set
vs is Relation-like NAT -defined the_Vertices_of G1 -valued Function-like finite FinSequence-like FinSubsequence-like (G1)
len vs is V21() V22() V23() V27() V28() V29() V30() ext-real non negative finite cardinal Element of NAT
2 * (len vs) is V21() V22() V23() V27() V28() V29() V30() ext-real non negative finite cardinal even Element of NAT
vs is V21() V22() V23() V27() V28() V29() V30() ext-real non negative finite cardinal set
vs . vs is set
2 * vs is V21() V22() V23() V27() V28() V29() V30() ext-real non negative finite cardinal even Element of NAT
(2 * vs) - 1 is non empty V28() V29() V30() ext-real non even set
G2 . ((2 * vs) - 1) is set
dom vs is finite Element of K32(NAT)
W1 is Relation-like NAT -defined the_Vertices_of G1 -valued Function-like finite FinSequence-like FinSubsequence-like (G1)
len W1 is V21() V22() V23() V27() V28() V29() V30() ext-real non negative finite cardinal Element of NAT
2 * (len W1) is V21() V22() V23() V27() V28() V29() V30() ext-real non negative finite cardinal even Element of NAT
W2 is Relation-like NAT -defined the_Vertices_of G1 -valued Function-like finite FinSequence-like FinSubsequence-like (G1)
len W2 is V21() V22() V23() V27() V28() V29() V30() ext-real non negative finite cardinal Element of NAT
2 * (len W2) is V21() V22() V23() V27() V28() V29() V30() ext-real non negative finite cardinal even Element of NAT
y is V21() V22() V23() V27() V28() V29() V30() ext-real non negative finite cardinal set
dom W1 is finite Element of K32(NAT)
W1 . y is set
2 * y is V21() V22() V23() V27() V28() V29() V30() ext-real non negative finite cardinal even Element of NAT
(2 * y) - 1 is non empty V28() V29() V30() ext-real non even set
G2 . ((2 * y) - 1) is set
W2 . y is set
Seg (len W2) is finite len W2 -element Element of K32(NAT)
dom W2 is finite Element of K32(NAT)
G1 is Relation-like NAT -defined Function-like finite [Graph-like] set
the_Vertices_of G1 is non empty set
the_Edges_of G1 is set
(the_Vertices_of G1) \/ (the_Edges_of G1) is non empty set
G2 is Relation-like NAT -defined (the_Vertices_of G1) \/ (the_Edges_of G1) -valued Function-like finite FinSequence-like FinSubsequence-like (G1)
len G2 is non empty V21() V22() V23() V27() V28() V29() V30() ext-real positive non negative finite cardinal non even Element of NAT
(len G2) - 1 is V28() V29() V30() ext-real even set
W1 is V21() V22() V23() V27() V28() V29() V30() ext-real non negative finite cardinal even Element of NAT
W1 div 2 is V21() V22() V23() V27() V28() V29() V30() ext-real non negative finite cardinal Element of NAT
y is V21() V22() V23() V27() V28() V29() V30() ext-real non negative finite cardinal Element of NAT
vs is Relation-like NAT -defined Function-like finite FinSequence-like FinSubsequence-like set
len vs is V21() V22() V23() V27() V28() V29() V30() ext-real non negative finite cardinal Element of NAT
dom vs is finite Element of K32(NAT)
vs is set
rng vs is finite set
vs is set
vs . vs is set
Seg y is finite y -element Element of K32(NAT)
n is V21() V22() V23() V27() V28() V29() V30() ext-real non negative finite cardinal Element of NAT
2 * n is V21() V22() V23() V27() V28() V29() V30() ext-real non negative finite cardinal even Element of NAT
n * 2 is V21() V22() V23() V27() V28() V29() V30() ext-real non negative finite cardinal even Element of NAT
y * 2 is V21() V22() V23() V27() V28() V29() V30() ext-real non negative finite cardinal even Element of NAT
n is V21() V22() V23() V27() V28() V29() V30() ext-real non negative finite cardinal even Element of NAT
n + 1 is non empty V21() V22() V23() V27() V28() V29() V30() ext-real positive non negative finite cardinal non even Element of NAT
W1 + 1 is non empty V21() V22() V23() V27() V28() V29() V30() ext-real positive non negative finite cardinal non even Element of NAT
1 * 2 is V21() V22() V23() V27() V28() V29() V30() ext-real non negative finite cardinal even Element of NAT
n - 1 is non empty V28() V29() V30() ext-real non even set
x is non empty V21() V22() V23() V27() V28() V29() V30() ext-real positive non negative finite cardinal non even Element of NAT
G2 . x is set
x + 2 is non empty V21() V22() V23() V27() V28() V29() V30() ext-real positive non negative finite cardinal non even Element of NAT
G2 . (x + 2) is set
x + 1 is non empty V21() V22() V23() V27() V28() V29() V30() ext-real positive non negative finite cardinal even Element of NAT
G2 . (x + 1) is set
G2 . (2 * n) is set
2 * y is V21() V22() V23() V27() V28() V29() V30() ext-real non negative finite cardinal even Element of NAT
(2 * y) + 1 is non empty V21() V22() V23() V27() V28() V29() V30() ext-real positive non negative finite cardinal non even Element of NAT
(G1,G2) is Relation-like NAT -defined the_Vertices_of G1 -valued Function-like finite FinSequence-like FinSubsequence-like (G1)
vs is Relation-like NAT -defined the_Edges_of G1 -valued Function-like finite FinSequence-like FinSubsequence-like FinSequence of the_Edges_of G1
len vs is V21() V22() V23() V27() V28() V29() V30() ext-real non negative finite cardinal Element of NAT
2 * (len vs) is V21() V22() V23() V27() V28() V29() V30() ext-real non negative finite cardinal even Element of NAT
(2 * (len vs)) + 1 is non empty V21() V22() V23() V27() V28() V29() V30() ext-real positive non negative finite cardinal non even Element of NAT
((2 * (len vs)) + 1) + 1 is non empty V21() V22() V23() V27() V28() V29() V30() ext-real positive non negative finite cardinal even Element of NAT
n is Relation-like NAT -defined the_Vertices_of G1 -valued Function-like finite FinSequence-like FinSubsequence-like (G1)
len n is V21() V22() V23() V27() V28() V29() V30() ext-real non negative finite cardinal Element of NAT
2 * (len n) is V21() V22() V23() V27() V28() V29() V30() ext-real non negative finite cardinal even Element of NAT
(len vs) + 1 is non empty V21() V22() V23() V27() V28() V29() V30() ext-real positive non negative finite cardinal Element of NAT
2 * ((len vs) + 1) is V21() V22() V23() V27() V28() V29() V30() ext-real non negative finite cardinal even Element of NAT
n is V21() V22() V23() V27() V28() V29() V30() ext-real non negative finite cardinal Element of NAT
n . n is set
n + 1 is non empty V21() V22() V23() V27() V28() V29() V30() ext-real positive non negative finite cardinal Element of NAT
n . (n + 1) is set
2 * n is V21() V22() V23() V27() V28() V29() V30() ext-real non negative finite cardinal even Element of NAT
g is V21() V22() V23() V27() V28() V29() V30() ext-real non negative finite cardinal even Element of NAT
g - 1 is non empty V28() V29() V30() ext-real non even set
n + n is V21() V22() V23() V27() V28() V29() V30() ext-real non negative finite cardinal Element of NAT
n * 2 is V21() V22() V23() V27() V28() V29() V30() ext-real non negative finite cardinal even Element of NAT
(len vs) * 2 is V21() V22() V23() V27() V28() V29() V30() ext-real non negative finite cardinal even Element of NAT
(len G2) - 0 is non empty V28() V29() V30() ext-real positive non negative set
es is non empty V21() V22() V23() V27() V28() V29() V30() ext-real positive non negative finite cardinal non even Element of NAT
2 * (n + 1) is V21() V22() V23() V27() V28() V29() V30() ext-real non negative finite cardinal even Element of NAT
(2 * (n + 1)) - 1 is non empty V28() V29() V30() ext-real non even set
G2 . ((2 * (n + 1)) - 1) is set
es + 2 is non empty V21() V22() V23() V27() V28() V29() V30() ext-real positive non negative finite cardinal non even Element of NAT
G2 . (es + 2) is set
dom vs is finite Element of K32(NAT)
vs . n is set
es + 1 is non empty V21() V22() V23() V27() V28() V29() V30() ext-real positive non negative finite cardinal even Element of NAT
G2 . (es + 1) is set
(2 * n) - 1 is non empty V28() V29() V30() ext-real non even set
G2 . ((2 * n) - 1) is set
n is Relation-like NAT -defined the_Vertices_of G1 -valued Function-like finite FinSequence-like FinSubsequence-like (G1)
len n is V21() V22() V23() V27() V28() V29() V30() ext-real non negative finite cardinal Element of NAT
vs is Relation-like NAT -defined the_Edges_of G1 -valued Function-like finite FinSequence-like FinSubsequence-like (G1)
len vs is V21() V22() V23() V27() V28() V29() V30() ext-real non negative finite cardinal Element of NAT
2 * (len vs) is V21() V22() V23() V27() V28() V29() V30() ext-real non negative finite cardinal even Element of NAT
(2 * (len vs)) + 1 is non empty V21() V22() V23() V27() V28() V29() V30() ext-real positive non negative finite cardinal non even Element of NAT
n is V21() V22() V23() V27() V28() V29() V30() ext-real non negative finite cardinal set
vs . n is set
2 * n is V21() V22() V23() V27() V28() V29() V30() ext-real non negative finite cardinal even Element of NAT
G2 . (2 * n) is set
dom vs is finite Element of K32(NAT)
W1 is Relation-like NAT -defined the_Edges_of G1 -valued Function-like finite FinSequence-like FinSubsequence-like (G1)
len W1 is V21() V22() V23() V27() V28() V29() V30() ext-real non negative finite cardinal Element of NAT
2 * (len W1) is V21() V22() V23() V27() V28() V29() V30() ext-real non negative finite cardinal even Element of NAT
(2 * (len W1)) + 1 is non empty V21() V22() V23() V27() V28() V29() V30() ext-real positive non negative finite cardinal non even Element of NAT
W2 is Relation-like NAT -defined the_Edges_of G1 -valued Function-like finite FinSequence-like FinSubsequence-like (G1)
len W2 is V21() V22() V23() V27() V28() V29() V30() ext-real non negative finite cardinal Element of NAT
2 * (len W2) is V21() V22() V23() V27() V28() V29() V30() ext-real non negative finite cardinal even Element of NAT
(2 * (len W2)) + 1 is non empty V21() V22() V23() V27() V28() V29() V30() ext-real positive non negative finite cardinal non even Element of NAT
y is V21() V22() V23() V27() V28() V29() V30() ext-real non negative finite cardinal set
dom W1 is finite Element of K32(NAT)
W1 . y is set
2 * y is V21() V22() V23() V27() V28() V29() V30() ext-real non negative finite cardinal even Element of NAT
G2 . (2 * y) is set
W2 . y is set
Seg (len W2) is finite len W2 -element Element of K32(NAT)
dom W2 is finite Element of K32(NAT)
G1 is Relation-like NAT -defined Function-like finite [Graph-like] set
the_Vertices_of G1 is non empty set
the_Edges_of G1 is set
(the_Vertices_of G1) \/ (the_Edges_of G1) is non empty set
G2 is Relation-like NAT -defined (the_Vertices_of G1) \/ (the_Edges_of G1) -valued Function-like finite FinSequence-like FinSubsequence-like (G1)
(G1,G2) is Relation-like NAT -defined the_Vertices_of G1 -valued Function-like finite FinSequence-like FinSubsequence-like (G1)
rng (G1,G2) is finite Element of K32((the_Vertices_of G1))
K32((the_Vertices_of G1)) is non empty set
G1 is Relation-like NAT -defined Function-like finite [Graph-like] set
the_Vertices_of G1 is non empty set
the_Edges_of G1 is set
(the_Vertices_of G1) \/ (the_Edges_of G1) is non empty set
G2 is Relation-like NAT -defined (the_Vertices_of G1) \/ (the_Edges_of G1) -valued Function-like finite FinSequence-like FinSubsequence-like (G1)
(G1,G2) is Relation-like NAT -defined the_Edges_of G1 -valued Function-like finite FinSequence-like FinSubsequence-like (G1)
rng (G1,G2) is finite Element of K32((the_Edges_of G1))
K32((the_Edges_of G1)) is non empty set
G1 is Relation-like NAT -defined Function-like finite [Graph-like] set
the_Vertices_of G1 is non empty set
the_Edges_of G1 is set
(the_Vertices_of G1) \/ (the_Edges_of G1) is non empty set
G2 is Relation-like NAT -defined (the_Vertices_of G1) \/ (the_Edges_of G1) -valued Function-like finite FinSequence-like FinSubsequence-like (G1)
(G1,G2) is Relation-like NAT -defined the_Edges_of G1 -valued Function-like finite FinSequence-like FinSubsequence-like (G1)
len (G1,G2) is V21() V22() V23() V27() V28() V29() V30() ext-real non negative finite cardinal Element of NAT
G1 is Relation-like NAT -defined Function-like finite [Graph-like] set
the_Vertices_of G1 is non empty set
the_Edges_of G1 is set
(the_Vertices_of G1) \/ (the_Edges_of G1) is non empty set
W1 is set
G2 is Relation-like NAT -defined (the_Vertices_of G1) \/ (the_Edges_of G1) -valued Function-like finite FinSequence-like FinSubsequence-like (G1)
(G1,G2) is finite Element of K32((the_Vertices_of G1))
K32((the_Vertices_of G1)) is non empty set
(G1,G2) is Relation-like NAT -defined the_Vertices_of G1 -valued Function-like finite FinSequence-like FinSubsequence-like (G1)
rng (G1,G2) is finite Element of K32((the_Vertices_of G1))
len G2 is non empty V21() V22() V23() V27() V28() V29() V30() ext-real positive non negative finite cardinal non even Element of NAT
dom (G1,G2) is finite Element of K32(NAT)
y is V21() V22() V23() V27() V28() V29() V30() ext-real non negative finite cardinal set
(G1,G2) . y is set
2 * y is V21() V22() V23() V27() V28() V29() V30() ext-real non negative finite cardinal even Element of NAT
vs is V21() V22() V23() V27() V28() V29() V30() ext-real non negative finite cardinal even set
vs - 1 is non empty V28() V29() V30() ext-real non even set
y + y is V21() V22() V23() V27() V28() V29() V30() ext-real non negative finite cardinal set
n is non empty V21() V22() V23() V27() V28() V29() V30() ext-real positive non negative finite cardinal non even Element of NAT
len (G1,G2) is V21() V22() V23() V27() V28() V29() V30() ext-real non negative finite cardinal Element of NAT
y * 2 is V21() V22() V23() V27() V28() V29() V30() ext-real non negative finite cardinal even Element of NAT
(len (G1,G2)) * 2 is V21() V22() V23() V27() V28() V29() V30() ext-real non negative finite cardinal even Element of NAT
(len G2) + 1 is non empty V21() V22() V23() V27() V28() V29() V30() ext-real positive non negative finite cardinal even Element of NAT
((len G2) + 1) - 1 is non empty V28() V29() V30() ext-real non even set
n is non empty V21() V22() V23() V27() V28() V29() V30() ext-real positive non negative finite cardinal non even Element of NAT
G2 . n is set
y is non empty V21() V22() V23() V27() V28() V29() V30() ext-real positive non negative finite cardinal non even Element of NAT
G2 . y is set
y is V21() V22() V23() V27() V28() V29() V30() ext-real non negative finite cardinal set
G2 . y is set
vs is non empty V21() V22() V23() V27() V28() V29() V30() ext-real positive non negative finite cardinal non even Element of NAT
vs is non empty V21() V22() V23() V27() V28() V29() V30() ext-real positive non negative finite cardinal non even Element of NAT
G2 . vs is set
vs is non empty V21() V22() V23() V27() V28() V29() V30() ext-real positive non negative finite cardinal non even set
G2 . vs is set
W2 is non empty V21() V22() V23() V27() V28() V29() V30() ext-real positive non negative finite cardinal non even Element of NAT
G2 . W2 is set
y is non empty V21() V22() V23() V27() V28() V29() V30() ext-real positive non negative finite cardinal non even Element of NAT
G2 . y is set
G1 is Relation-like NAT -defined Function-like finite [Graph-like] set
the_Vertices_of G1 is non empty set
the_Edges_of G1 is set
(the_Vertices_of G1) \/ (the_Edges_of G1) is non empty set
W1 is V21() V22() V23() V27() V28() V29() V30() ext-real non negative finite cardinal Element of NAT
G2 is Relation-like NAT -defined (the_Vertices_of G1) \/ (the_Edges_of G1) -valued Function-like finite FinSequence-like FinSubsequence-like (G1)
len G2 is non empty V21() V22() V23() V27() V28() V29() V30() ext-real positive non negative finite cardinal non even Element of NAT
G2 . W1 is set
W2 is V21() V22() V23() V27() V28() V29() V30() ext-real non negative finite cardinal set
G2 . W2 is set
y is non empty V21() V22() V23() V27() V28() V29() V30() ext-real positive non negative finite cardinal non even Element of NAT
vs is non empty V21() V22() V23() V27() V28() V29() V30() ext-real positive non negative finite cardinal non even Element of NAT
G2 . vs is set
vs is non empty V21() V22() V23() V27() V28() V29() V30() ext-real positive non negative finite cardinal non even set
G2 . vs is set
W2 is non empty V21() V22() V23() V27() V28() V29() V30() ext-real positive non negative finite cardinal non even Element of NAT
G2 . W2 is set
y is non empty V21() V22() V23() V27() V28() V29() V30() ext-real positive non negative finite cardinal non even Element of NAT
G2 . y is set
G1 is Relation-like NAT -defined Function-like finite [Graph-like] set
the_Vertices_of G1 is non empty set
the_Edges_of G1 is set
(the_Vertices_of G1) \/ (the_Edges_of G1) is non empty set
W1 is set
G2 is Relation-like NAT -defined (the_Vertices_of G1) \/ (the_Edges_of G1) -valued Function-like finite FinSequence-like FinSubsequence-like (G1)
(G1,G2) is finite Element of K32((the_Vertices_of G1))
K32((the_Vertices_of G1)) is non empty set
(G1,G2) is Relation-like NAT -defined the_Vertices_of G1 -valued Function-like finite FinSequence-like FinSubsequence-like (G1)
rng (G1,G2) is finite Element of K32((the_Vertices_of G1))
len G2 is non empty V21() V22() V23() V27() V28() V29() V30() ext-real positive non negative finite cardinal non even Element of NAT
(G1,G2,W1) is non empty V21() V22() V23() V27() V28() V29() V30() ext-real positive non negative finite cardinal non even Element of NAT
G2 . (G1,G2,W1) is set
W2 is V21() V22() V23() V27() V28() V29() V30() ext-real non negative finite cardinal set
G2 . W2 is set
W2 is V21() V22() V23() V27() V28() V29() V30() ext-real non negative finite cardinal set
G2 . W2 is set
y is non empty V21() V22() V23() V27() V28() V29() V30() ext-real positive non negative finite cardinal non even Element of NAT
vs is non empty V21() V22() V23() V27() V28() V29() V30() ext-real positive non negative finite cardinal non even Element of NAT
G2 . vs is set
vs is non empty V21() V22() V23() V27() V28() V29() V30() ext-real positive non negative finite cardinal non even Element of NAT
G2 . vs is set
W2 is non empty V21() V22() V23() V27() V28() V29() V30() ext-real positive non negative finite cardinal non even Element of NAT
G2 . W2 is set
y is non empty V21() V22() V23() V27() V28() V29() V30() ext-real positive non negative finite cardinal non even Element of NAT
G2 . y is set
G1 is Relation-like NAT -defined Function-like finite [Graph-like] set
the_Vertices_of G1 is non empty set
the_Edges_of G1 is set
(the_Vertices_of G1) \/ (the_Edges_of G1) is non empty set
W1 is V21() V22() V23() V27() V28() V29() V30() ext-real non negative finite cardinal Element of NAT
G2 is Relation-like NAT -defined (the_Vertices_of G1) \/ (the_Edges_of G1) -valued Function-like finite FinSequence-like FinSubsequence-like (G1)
len G2 is non empty V21() V22() V23() V27() V28() V29() V30() ext-real positive non negative finite cardinal non even Element of NAT
G2 . W1 is set
W2 is V21() V22() V23() V27() V28() V29() V30() ext-real non negative finite cardinal set
G2 . W2 is set
W2 is V21() V22() V23() V27() V28() V29() V30() ext-real non negative finite cardinal set
G2 . W2 is set
y is non empty V21() V22() V23() V27() V28() V29() V30() ext-real positive non negative finite cardinal non even Element of NAT
vs is non empty V21() V22() V23() V27() V28() V29() V30() ext-real positive non negative finite cardinal non even Element of NAT
G2 . vs is set
vs is non empty V21() V22() V23() V27() V28() V29() V30() ext-real positive non negative finite cardinal non even Element of NAT
G2 . vs is set
W2 is non empty V21() V22() V23() V27() V28() V29() V30() ext-real positive non negative finite cardinal non even Element of NAT
G2 . W2 is set
y is non empty V21() V22() V23() V27() V28() V29() V30() ext-real positive non negative finite cardinal non even Element of NAT
G2 . y is set
G1 is Relation-like NAT -defined Function-like finite [Graph-like] set
the_Vertices_of G1 is non empty set
the_Edges_of G1 is set
(the_Vertices_of G1) \/ (the_Edges_of G1) is non empty set
G1 is Relation-like NAT -defined Function-like finite [Graph-like] set
the_Vertices_of G1 is non empty set
the_Edges_of G1 is set
(the_Vertices_of G1) \/ (the_Edges_of G1) is non empty set
G1 is Relation-like NAT -defined Function-like finite [Graph-like] set
the_Vertices_of G1 is non empty set
the_Edges_of G1 is set
(the_Vertices_of G1) \/ (the_Edges_of G1) is non empty set
G1 is Relation-like NAT -defined Function-like finite [Graph-like] set
the_Vertices_of G1 is non empty set
the_Edges_of G1 is set
(the_Vertices_of G1) \/ (the_Edges_of G1) is non empty set
G1 is Relation-like NAT -defined Function-like finite [Graph-like] set
the_Vertices_of G1 is non empty set
the_Edges_of G1 is set
(the_Vertices_of G1) \/ (the_Edges_of G1) is non empty set
G1 is Relation-like NAT -defined Function-like finite [Graph-like] set
the_Vertices_of G1 is non empty set
the_Edges_of G1 is set
(the_Vertices_of G1) \/ (the_Edges_of G1) is non empty set
G1 is Relation-like NAT -defined Function-like finite [Graph-like] set
the_Vertices_of G1 is non empty set
the_Edges_of G1 is set
(the_Vertices_of G1) \/ (the_Edges_of G1) is non empty set
G2 is Relation-like NAT -defined (the_Vertices_of G1) \/ (the_Edges_of G1) -valued Function-like finite FinSequence-like FinSubsequence-like (G1)
len G2 is non empty V21() V22() V23() V27() V28() V29() V30() ext-real positive non negative finite cardinal non even Element of NAT
W1 is non empty V21() V22() V23() V27() V28() V29() V30() ext-real positive non negative finite cardinal non even Element of NAT
G2 . W1 is set
(G1,G2,W1) is Element of the_Vertices_of G1
G1 is Relation-like NAT -defined Function-like finite [Graph-like] set
the_Vertices_of G1 is non empty set
the_Edges_of G1 is set
(the_Vertices_of G1) \/ (the_Edges_of G1) is non empty set
G2 is Relation-like NAT -defined (the_Vertices_of G1) \/ (the_Edges_of G1) -valued Function-like finite FinSequence-like FinSubsequence-like (G1)
dom G2 is finite Element of K32(NAT)
W1 is V21() V22() V23() V27() V28() V29() V30() ext-real non negative finite cardinal even Element of NAT
W1 - 1 is non empty V28() V29() V30() ext-real non even set
W1 + 1 is non empty V21() V22() V23() V27() V28() V29() V30() ext-real positive non negative finite cardinal non even Element of NAT
G2 . (W1 + 1) is set
G2 . W1 is set
1 + W1 is non empty V21() V22() V23() V27() V28() V29() V30() ext-real positive non negative finite cardinal non even Element of NAT
len G2 is non empty V21() V22() V23() V27() V28() V29() V30() ext-real positive non negative finite cardinal non even Element of NAT
W2 is non empty V21() V22() V23() V27() V28() V29() V30() ext-real positive non negative finite cardinal non even Element of NAT
G2 . W2 is set
1 + 1 is non empty V21() V22() V23() V27() V28() V29() V30() ext-real positive non negative finite cardinal Element of NAT
(1 + 1) - 1 is V28() V29() V30() ext-real set
(len G2) - 0 is non empty V28() V29() V30() ext-real positive non negative set
W2 + 2 is non empty V21() V22() V23() V27() V28() V29() V30() ext-real positive non negative finite cardinal non even Element of NAT
G2 . (W2 + 2) is set
W2 + 1 is non empty V21() V22() V23() V27() V28() V29() V30() ext-real positive non negative finite cardinal even Element of NAT
G2 . (W2 + 1) is set
G1 is Relation-like NAT -defined Function-like finite [Graph-like] set
the_Vertices_of G1 is non empty set
the_Edges_of G1 is set
(the_Vertices_of G1) \/ (the_Edges_of G1) is non empty set
G2 is Relation-like NAT -defined (the_Vertices_of G1) \/ (the_Edges_of G1) -valued Function-like finite FinSequence-like FinSubsequence-like (G1)
len G2 is non empty V21() V22() V23() V27() V28() V29() V30() ext-real positive non negative finite cardinal non even Element of NAT
dom G2 is finite Element of K32(NAT)
W1 is non empty V21() V22() V23() V27() V28() V29() V30() ext-real positive non negative finite cardinal non even Element of NAT
W1 + 1 is non empty V21() V22() V23() V27() V28() V29() V30() ext-real positive non negative finite cardinal even Element of NAT
W1 + 2 is non empty V21() V22() V23() V27() V28() V29() V30() ext-real positive non negative finite cardinal non even Element of NAT
G1 is Relation-like NAT -defined Function-like finite [Graph-like] set
the_Vertices_of G1 is non empty set
G2 is Element of the_Vertices_of G1
(G1,G2) is Relation-like NAT -defined (the_Vertices_of G1) \/ (the_Edges_of G1) -valued Function-like finite FinSequence-like FinSubsequence-like (G1)
the_Edges_of G1 is set
(the_Vertices_of G1) \/ (the_Edges_of G1) is non empty set
<*G2*> is non empty trivial Relation-like NAT -defined the_Vertices_of G1 -valued Function-like constant finite 1 -element FinSequence-like FinSubsequence-like FinSequence of the_Vertices_of G1
(G1,(G1,G2)) is Element of the_Vertices_of G1
(G1,G2) . 1 is set
(G1,(G1,G2)) is Element of the_Vertices_of G1
len (G1,G2) is non empty V21() V22() V23() V27() V28() V29() V30() ext-real positive non negative finite cardinal non even Element of NAT
(G1,G2) . (len (G1,G2)) is set
W2 is non empty V21() V22() V23() V27() V28() V29() V30() ext-real positive non negative finite cardinal non even Element of NAT
(G1,G2) . W2 is set
the_Source_of G1 is Relation-like Function-like V18( the_Edges_of G1, the_Vertices_of G1) Element of