:: MSSCYC_1 semantic presentation

REAL is set
NAT is V6() V7() V8() non empty non trivial non finite cardinal limit_cardinal Element of bool REAL

NAT is V6() V7() V8() non empty non trivial non finite cardinal limit_cardinal set
bool NAT is non trivial non finite set
bool NAT is non trivial non finite set

1 is V6() V7() V8() V12() non empty finite cardinal V139() V140() ext-real positive non negative V144() Element of NAT
{{},1} is non empty finite V28() set
Trees is non empty constituted-Trees set

PeanoNat is non empty strict L13()
the carrier of PeanoNat is non empty set

bool () is set

bool is set

bool is set

RAT is set
INT is set
2 is V6() V7() V8() V12() non empty finite cardinal V139() V140() ext-real positive non negative V144() Element of NAT
3 is V6() V7() V8() V12() non empty finite cardinal V139() V140() ext-real positive non negative V144() Element of NAT

Seg 1 is non empty trivial finite 1 -element Element of bool NAT

height is V6() V7() V8() V12() finite cardinal V139() V140() ext-real non negative V144() Element of NAT
S is non empty V54() MultiGraphStruct
the carrier' of S is set
the carrier of S is non empty set

len X is V6() V7() V8() V12() finite cardinal V139() V140() ext-real non negative V144() Element of NAT
(len X) + 1 is V6() V7() V8() V12() non empty finite cardinal V139() V140() ext-real positive non negative V144() Element of NAT

len v is V6() V7() V8() V12() finite cardinal V139() V140() ext-real non negative V144() Element of NAT
vk is V6() V7() V8() V12() finite cardinal V139() V140() ext-real non negative V144() set

v . vk is set

len o is V6() V7() V8() V12() finite cardinal V139() V140() ext-real non negative V144() Element of NAT
t is V6() V7() V8() V12() finite cardinal V139() V140() ext-real non negative V144() Element of NAT
o /. t is Element of the carrier of S
t + 1 is V6() V7() V8() V12() non empty finite cardinal V139() V140() ext-real positive non negative V144() Element of NAT
o /. (t + 1) is Element of the carrier of S
X . t is set
o . (t + 1) is set
o . t is set
a is Element of the carrier of S
k is Element of the carrier of S

vk is V6() V7() V8() V12() finite cardinal V139() V140() ext-real non negative V144() Element of NAT

X . vk is set

len v is V6() V7() V8() V12() finite cardinal V139() V140() ext-real non negative V144() Element of NAT
vk is V6() V7() V8() V12() finite cardinal V139() V140() ext-real non negative V144() Element of NAT

v . vk is set

vk is V6() V7() V8() V12() finite cardinal V139() V140() ext-real non negative V144() Element of NAT
v . vk is set
vk + 1 is V6() V7() V8() V12() non empty finite cardinal V139() V140() ext-real positive non negative V144() Element of NAT
v . (vk + 1) is set
X . vk is set
v /. vk is Element of the carrier of S
o is Element of the carrier of S
v /. (vk + 1) is Element of the carrier of S
t is Element of the carrier of S
S is V6() V7() V8() V12() finite cardinal V139() V140() ext-real non negative V144() Element of NAT

len X is V6() V7() V8() V12() finite cardinal V139() V140() ext-real non negative V144() Element of NAT

len ((1,S) -cut X) is V6() V7() V8() V12() finite cardinal V139() V140() ext-real non negative V144() Element of NAT
(len ((1,S) -cut X)) + 1 is V6() V7() V8() V12() non empty finite cardinal V139() V140() ext-real positive non negative V144() Element of NAT
S + 1 is V6() V7() V8() V12() non empty finite cardinal V139() V140() ext-real positive non negative V144() Element of NAT
len (X ^ v) is V6() V7() V8() V12() finite cardinal V139() V140() ext-real non negative V144() Element of NAT
len v is V6() V7() V8() V12() finite cardinal V139() V140() ext-real non negative V144() Element of NAT
(len X) + (len v) is V6() V7() V8() V12() finite cardinal V139() V140() ext-real non negative V144() Element of NAT
len ((1,S) -cut (X ^ v)) is V6() V7() V8() V12() finite cardinal V139() V140() ext-real non negative V144() Element of NAT
(len ((1,S) -cut (X ^ v))) + 1 is V6() V7() V8() V12() non empty finite cardinal V139() V140() ext-real positive non negative V144() Element of NAT
t is V6() V7() V8() V12() finite cardinal V139() V140() ext-real non negative V144() set

0 + 1 is V6() V7() V8() V12() non empty finite cardinal V139() V140() ext-real positive non negative V144() Element of NAT
((1,S) -cut X) . t is set
X . t is set
(X ^ v) . t is set
((1,S) -cut (X ^ v)) . t is set
a is V6() V7() V8() V12() finite cardinal V139() V140() ext-real non negative V144() Element of NAT
a + 1 is V6() V7() V8() V12() non empty finite cardinal V139() V140() ext-real positive non negative V144() Element of NAT
a is V6() V7() V8() V12() finite cardinal V139() V140() ext-real non negative V144() Element of NAT
a + 1 is V6() V7() V8() V12() non empty finite cardinal V139() V140() ext-real positive non negative V144() Element of NAT
S is non empty V54() MultiGraphStruct
S is non empty V54() MultiGraphStruct
{1} is non empty trivial finite V28() 1 -element set

bool [:{},{1}:] is finite V28() set

vk is non empty V54() MultiGraphStruct
the carrier' of vk is set
S is non empty V54() MultiGraphStruct
the Source of S is Relation-like the carrier' of S -defined the carrier of S -valued Function-like V36( the carrier' of S, the carrier of S) Element of bool [: the carrier' of S, the carrier of S:]
the carrier' of S is set
the carrier of S is non empty set
[: the carrier' of S, the carrier of S:] is Relation-like set
bool [: the carrier' of S, the carrier of S:] is set
proj2 the Source of S is set
the Target of S is Relation-like the carrier' of S -defined the carrier of S -valued Function-like V36( the carrier' of S, the carrier of S) Element of bool [: the carrier' of S, the carrier of S:]
proj2 the Target of S is set
(proj2 the Source of S) \/ (proj2 the Target of S) is set
{1,2} is non empty finite V28() set
{1} is non empty trivial finite V28() 1 -element set

bool [:{1},{1,2}:] is finite V28() set

is Relation-like non trivial non finite set
bool is non trivial non finite set

v is Relation-like {1} -defined {1,2} -valued Function-like finite V36({1},{1,2}) Element of bool [:{1},{1,2}:]
vk is Relation-like {1} -defined {1,2} -valued Function-like finite V36({1},{1,2}) Element of bool [:{1},{1,2}:]
MultiGraphStruct(# {1,2},{1},v,vk #) is strict MultiGraphStruct
o is non empty V54() MultiGraphStruct
v . 1 is set
the carrier' of o is set
the Source of o is Relation-like the carrier' of o -defined the carrier of o -valued Function-like V36( the carrier' of o, the carrier of o) Element of bool [: the carrier' of o, the carrier of o:]
the carrier of o is non empty set
[: the carrier' of o, the carrier of o:] is Relation-like set
bool [: the carrier' of o, the carrier of o:] is set
the Target of o is Relation-like the carrier' of o -defined the carrier of o -valued Function-like V36( the carrier' of o, the carrier of o) Element of bool [: the carrier' of o, the carrier of o:]
t is set
the Source of o . t is set
the Target of o . t is set
vk . 1 is set
the carrier of o is non empty set
the carrier' of o is set
the Source of o is Relation-like the carrier' of o -defined the carrier of o -valued Function-like V36( the carrier' of o, the carrier of o) Element of bool [: the carrier' of o, the carrier of o:]
[: the carrier' of o, the carrier of o:] is Relation-like set
bool [: the carrier' of o, the carrier of o:] is set
the Target of o is Relation-like the carrier' of o -defined the carrier of o -valued Function-like V36( the carrier' of o, the carrier of o) Element of bool [: the carrier' of o, the carrier of o:]
MultiGraphStruct(# the carrier of o, the carrier' of o, the Source of o, the Target of o #) is strict MultiGraphStruct
a is non empty V54() MultiGraphStruct
the carrier of a is non empty set
k is non empty V54() MultiGraphStruct
the carrier of k is non empty set
a \/ k is non empty V54() strict MultiGraphStruct
the Target of a is Relation-like the carrier' of a -defined the carrier of a -valued Function-like V36( the carrier' of a, the carrier of a) Element of bool [: the carrier' of a, the carrier of a:]
the carrier' of a is set
[: the carrier' of a, the carrier of a:] is Relation-like set
bool [: the carrier' of a, the carrier of a:] is set
the Target of k is Relation-like the carrier' of k -defined the carrier of k -valued Function-like V36( the carrier' of k, the carrier of k) Element of bool [: the carrier' of k, the carrier of k:]
the carrier' of k is set
[: the carrier' of k, the carrier of k:] is Relation-like set
bool [: the carrier' of k, the carrier of k:] is set
the Source of a is Relation-like the carrier' of a -defined the carrier of a -valued Function-like V36( the carrier' of a, the carrier of a) Element of bool [: the carrier' of a, the carrier of a:]
the Source of k is Relation-like the carrier' of k -defined the carrier of k -valued Function-like V36( the carrier' of k, the carrier of k) Element of bool [: the carrier' of k, the carrier of k:]
proj2 the Source of a is set
proj2 the Target of a is set
(proj2 the Source of a) \/ (proj2 the Target of a) is set
proj2 the Source of k is set
proj2 the Target of k is set
(proj2 the Source of k) \/ (proj2 the Target of k) is set
the carrier of MultiGraphStruct(# the carrier of o, the carrier' of o, the Source of o, the Target of o #) is set
the carrier of a \/ the carrier of k is non empty set
the carrier' of MultiGraphStruct(# the carrier of o, the carrier' of o, the Source of o, the Target of o #) is set
the carrier' of a \/ the carrier' of k is set
the Source of k . 1 is set
the Source of a . 1 is set
the Target of a . 1 is set
the Source of a . 1 is set
the Target of k . 1 is set
the Source of k . 1 is set
S is non empty V54() MultiGraphStruct
the carrier of S is non empty set
the Source of S is Relation-like the carrier' of S -defined the carrier of S -valued Function-like V36( the carrier' of S, the carrier of S) Element of bool [: the carrier' of S, the carrier of S:]
the carrier' of S is set
[: the carrier' of S, the carrier of S:] is Relation-like set
bool [: the carrier' of S, the carrier of S:] is set
the Target of S is Relation-like the carrier' of S -defined the carrier of S -valued Function-like V36( the carrier' of S, the carrier of S) Element of bool [: the carrier' of S, the carrier of S:]
X is set
the Source of S . X is set
the Target of S . X is set

v is Element of the carrier of S
vk is Element of the carrier of S

the carrier of S * is functional non empty FinSequence-membered M8( the carrier of S)
1 + 1 is V6() V7() V8() V12() non empty finite cardinal V139() V140() ext-real positive non negative V144() Element of NAT
<*v,vk*> /. (1 + 1) is Element of the carrier of S
len <*X*> is V6() V7() V8() V12() non empty finite cardinal V139() V140() ext-real positive non negative V144() Element of NAT
len <*v,vk*> is V6() V7() V8() V12() non empty finite cardinal V139() V140() ext-real positive non negative V144() Element of NAT
() + 1 is V6() V7() V8() V12() non empty finite cardinal V139() V140() ext-real positive non negative V144() Element of NAT
a is V6() V7() V8() V12() finite cardinal V139() V140() ext-real non negative V144() Element of NAT
<*v,vk*> /. a is Element of the carrier of S
a + 1 is V6() V7() V8() V12() non empty finite cardinal V139() V140() ext-real positive non negative V144() Element of NAT
<*v,vk*> /. (a + 1) is Element of the carrier of S
<*X*> . a is set
<*X*> . 1 is set
<*v,vk*> /. 1 is Element of the carrier of S
S is non empty V54() MultiGraphStruct
the carrier' of S is set
X is set

the carrier of S is non empty set
the Source of S is Relation-like the carrier' of S -defined the carrier of S -valued Function-like V36( the carrier' of S, the carrier of S) Element of bool [: the carrier' of S, the carrier of S:]
[: the carrier' of S, the carrier of S:] is Relation-like set
bool [: the carrier' of S, the carrier of S:] is set
the Source of S . X is set
the Target of S is Relation-like the carrier' of S -defined the carrier of S -valued Function-like V36( the carrier' of S, the carrier of S) Element of bool [: the carrier' of S, the carrier of S:]
the Target of S . X is set
o is non empty set
v is Element of the carrier of S
vk is Element of the carrier of S

the carrier of S * is functional non empty FinSequence-membered M8( the carrier of S)
t is Element of o

k is V6() V7() V8() V12() finite cardinal V139() V140() ext-real non negative V144() Element of NAT
len a is V6() V7() V8() V12() finite cardinal V139() V140() ext-real non negative V144() Element of NAT
k + 1 is V6() V7() V8() V12() non empty finite cardinal V139() V140() ext-real positive non negative V144() Element of NAT
a . (k + 1) is set
the Source of S . (a . (k + 1)) is set
a . k is set
the Target of S . (a . k) is set
S is non empty non void V54() MultiGraphStruct
the carrier' of S is non empty set
the Element of the carrier' of S is Element of the carrier' of S
<* the Element of the carrier' of S*> is Relation-like NAT -defined the carrier' of S -valued Function-like constant non empty trivial finite 1 -element FinSequence-like FinSubsequence-like Element of the carrier' of S *
the carrier' of S * is functional non empty FinSequence-membered M8( the carrier' of S)

vk is V6() V7() V8() V12() finite cardinal V139() V140() ext-real non negative V144() Element of NAT
o is V6() V7() V8() V12() finite cardinal V139() V140() ext-real non negative V144() Element of NAT
len v is V6() V7() V8() V12() finite cardinal V139() V140() ext-real non negative V144() Element of NAT
v . vk is set
v . o is set
S is non empty V54() MultiGraphStruct
the carrier of S is non empty set

v . 1 is set
len v is V6() V7() V8() V12() finite cardinal V139() V140() ext-real non negative V144() Element of NAT
v . (len v) is set

vk . 1 is set
len vk is V6() V7() V8() V12() finite cardinal V139() V140() ext-real non negative V144() Element of NAT
vk . (len vk) is set
card the carrier of S is V6() V7() V8() non empty cardinal set

card the carrier of S is V6() V7() V8() non empty cardinal set
len X is V6() V7() V8() V12() finite cardinal V139() V140() ext-real non negative V144() Element of NAT
(len X) + 1 is V6() V7() V8() V12() non empty finite cardinal V139() V140() ext-real positive non negative V144() Element of NAT
the Source of S is Relation-like the carrier' of S -defined the carrier of S -valued Function-like V36( the carrier' of S, the carrier of S) Element of bool [: the carrier' of S, the carrier of S:]
the carrier' of S is set
[: the carrier' of S, the carrier of S:] is Relation-like set
bool [: the carrier' of S, the carrier of S:] is set
the Target of S is Relation-like the carrier' of S -defined the carrier of S -valued Function-like V36( the carrier' of S, the carrier of S) Element of bool [: the carrier' of S, the carrier of S:]

X . 1 is set
the Source of S . (X . 1) is set
the Target of S . (X . 1) is set
{( the Source of S . (X . 1)),( the Target of S . (X . 1))} is non empty finite set

proj2 vk is finite set
dom vk is finite Element of bool NAT
card the carrier of S is V6() V7() V8() non empty cardinal set
S is non empty V54() MultiGraphStruct
the carrier of S is non empty set

v . 1 is set
len v is V6() V7() V8() V12() finite cardinal V139() V140() ext-real non negative V144() Element of NAT
v . (len v) is set
S is non empty V54() MultiGraphStruct
the carrier' of S is set
the Source of S is Relation-like the carrier' of S -defined the carrier of S -valued Function-like V36( the carrier' of S, the carrier of S) Element of bool [: the carrier' of S, the carrier of S:]
the carrier of S is non empty set
[: the carrier' of S, the carrier of S:] is Relation-like set
bool [: the carrier' of S, the carrier of S:] is set
the Target of S is Relation-like the carrier' of S -defined the carrier of S -valued Function-like V36( the carrier' of S, the carrier of S) Element of bool [: the carrier' of S, the carrier of S:]
X is set

the Source of S . X is set
the Target of S . X is set
<*( the Source of S . X),( the Target of S . X)*> is Relation-like NAT -defined Function-like non empty finite 2 -element FinSequence-like FinSubsequence-like set
v is Element of the carrier of S
vk is Element of the carrier of S

the carrier of S * is functional non empty FinSequence-membered M8( the carrier of S)

len t is V6() V7() V8() V12() finite cardinal V139() V140() ext-real non negative V144() Element of NAT

len o is V6() V7() V8() V12() finite cardinal V139() V140() ext-real non negative V144() Element of NAT
(len t) + 1 is V6() V7() V8() V12() non empty finite cardinal V139() V140() ext-real positive non negative V144() Element of NAT
a is V6() V7() V8() V12() finite cardinal V139() V140() ext-real non negative V144() Element of NAT
o /. a is Element of the carrier of S
a + 1 is V6() V7() V8() V12() non empty finite cardinal V139() V140() ext-real positive non negative V144() Element of NAT
o /. (a + 1) is Element of the carrier of S
t . a is set
o /. 2 is Element of the carrier of S
o /. 1 is Element of the carrier of S
t . 1 is set
o . 1 is set
the Source of S . (t . 1) is set
S is V6() V7() V8() V12() finite cardinal V139() V140() ext-real non negative V144() Element of NAT
X is V6() V7() V8() V12() finite cardinal V139() V140() ext-real non negative V144() Element of NAT

len ((S,X) -cut v) is V6() V7() V8() V12() finite cardinal V139() V140() ext-real non negative V144() Element of NAT
len v is V6() V7() V8() V12() finite cardinal V139() V140() ext-real non negative V144() Element of NAT
(len ((S,X) -cut v)) + S is V6() V7() V8() V12() finite cardinal V139() V140() ext-real non negative V144() Element of NAT
X + 1 is V6() V7() V8() V12() non empty finite cardinal V139() V140() ext-real positive non negative V144() Element of NAT
X + ((len ((S,X) -cut v)) + S) is V6() V7() V8() V12() finite cardinal V139() V140() ext-real non negative V144() Element of NAT
(X + 1) + (len v) is V6() V7() V8() V12() non empty finite cardinal V139() V140() ext-real positive non negative V144() Element of NAT
1 + (len v) is V6() V7() V8() V12() non empty finite cardinal V139() V140() ext-real positive non negative V144() Element of NAT
X + (1 + (len v)) is V6() V7() V8() V12() non empty finite cardinal V139() V140() ext-real positive non negative V144() Element of NAT
((len ((S,X) -cut v)) + S) + 1 is V6() V7() V8() V12() non empty finite cardinal V139() V140() ext-real positive non negative V144() Element of NAT
S + (1 + (len v)) is V6() V7() V8() V12() non empty finite cardinal V139() V140() ext-real positive non negative V144() Element of NAT
S + 1 is V6() V7() V8() V12() non empty finite cardinal V139() V140() ext-real positive non negative V144() Element of NAT
(len ((S,X) -cut v)) + (S + 1) is V6() V7() V8() V12() non empty finite cardinal V139() V140() ext-real positive non negative V144() Element of NAT
(S + 1) + (len v) is V6() V7() V8() V12() non empty finite cardinal V139() V140() ext-real positive non negative V144() Element of NAT
S is V6() V7() V8() V12() finite cardinal V139() V140() ext-real non negative V144() Element of NAT
X is V6() V7() V8() V12() finite cardinal V139() V140() ext-real non negative V144() Element of NAT
v is non empty non void V54() MultiGraphStruct

len vk is V6() V7() V8() V12() finite cardinal V139() V140() ext-real non negative V144() Element of NAT

len o is V6() V7() V8() V12() finite cardinal V139() V140() ext-real non negative V144() Element of NAT
(len o) + S is V6() V7() V8() V12() finite cardinal V139() V140() ext-real non negative V144() Element of NAT
X + 1 is V6() V7() V8() V12() non empty finite cardinal V139() V140() ext-real positive non negative V144() Element of NAT
(len vk) + 1 is V6() V7() V8() V12() non empty finite cardinal V139() V140() ext-real positive non negative V144() Element of NAT
t is V6() V7() V8() V12() finite cardinal V139() V140() ext-real non negative V144() Element of NAT
0 + 1 is V6() V7() V8() V12() non empty finite cardinal V139() V140() ext-real positive non negative V144() Element of NAT
a is V6() V7() V8() V12() finite cardinal V139() V140() ext-real non negative V144() Element of NAT
a + 1 is V6() V7() V8() V12() non empty finite cardinal V139() V140() ext-real positive non negative V144() Element of NAT
S + a is V6() V7() V8() V12() finite cardinal V139() V140() ext-real non negative V144() Element of NAT
S + (a + 1) is V6() V7() V8() V12() non empty finite cardinal V139() V140() ext-real positive non negative V144() Element of NAT
(S + a) + 1 is V6() V7() V8() V12() non empty finite cardinal V139() V140() ext-real positive non negative V144() Element of NAT
t + 1 is V6() V7() V8() V12() non empty finite cardinal V139() V140() ext-real positive non negative V144() Element of NAT
o . (t + 1) is set
S + t is V6() V7() V8() V12() finite cardinal V139() V140() ext-real non negative V144() Element of NAT
vk . (S + t) is set
o . (a + 1) is set
vk . (S + a) is set
the Source of v is Relation-like the carrier' of v -defined the carrier of v -valued Function-like V36( the carrier' of v, the carrier of v) Element of bool [: the carrier' of v, the carrier of v:]
the carrier' of v is non empty set
the carrier of v is non empty set
[: the carrier' of v, the carrier of v:] is Relation-like set
bool [: the carrier' of v, the carrier of v:] is set
the Source of v . (o . (t + 1)) is set
the Target of v is Relation-like the carrier' of v -defined the carrier of v -valued Function-like V36( the carrier' of v, the carrier of v) Element of bool [: the carrier' of v, the carrier of v:]
o . t is set
the Target of v . (o . t) is set
S is non empty non void V54() MultiGraphStruct

the carrier of S is non empty set
len () is V6() V7() V8() V12() finite cardinal V139() V140() ext-real non negative V144() Element of NAT
len X is V6() V7() V8() V12() non empty finite cardinal V139() V140() ext-real positive non negative V144() Element of NAT
(len X) + 1 is V6() V7() V8() V12() non empty finite cardinal V139() V140() ext-real positive non negative V144() Element of NAT
S is non empty non void V54() MultiGraphStruct

the carrier of S is non empty set
len () is V6() V7() V8() V12() finite cardinal V139() V140() ext-real non negative V144() Element of NAT
len X is V6() V7() V8() V12() non empty finite cardinal V139() V140() ext-real positive non negative V144() Element of NAT
(len X) + 1 is V6() V7() V8() V12() non empty finite cardinal V139() V140() ext-real positive non negative V144() Element of NAT
S is non empty non void V54() MultiGraphStruct
the Source of S is Relation-like the carrier' of S -defined the carrier of S -valued Function-like V36( the carrier' of S, the carrier of S) Element of bool [: the carrier' of S, the carrier of S:]
the carrier' of S is non empty set
the carrier of S is non empty set
[: the carrier' of S, the carrier of S:] is Relation-like set
bool [: the carrier' of S, the carrier of S:] is set
the Target of S is Relation-like the carrier' of S -defined the carrier of S -valued Function-like V36( the carrier' of S, the carrier of S) Element of bool [: the carrier' of S, the carrier of S:]

len X is V6() V7() V8() V12() non empty finite cardinal V139() V140() ext-real positive non negative V144() Element of NAT

t is V6() V7() V8() V12() finite cardinal V139() V140() ext-real non negative V144() Element of NAT
() . t is set
X . t is set
the Source of S . (X . t) is set
t + 1 is V6() V7() V8() V12() non empty finite cardinal V139() V140() ext-real positive non negative V144() Element of NAT
() . (t + 1) is set
the Target of S . (X . t) is set
X . (t + 1) is set
the Source of S . (X . (t + 1)) is set
(t + 1) + 1 is V6() V7() V8() V12() non empty finite cardinal V139() V140() ext-real positive non negative V144() Element of NAT
() . ((t + 1) + 1) is set
the Target of S . (X . (t + 1)) is set
() /. 1 is Element of the carrier of S
1 + 1 is V6() V7() V8() V12() non empty finite cardinal V139() V140() ext-real positive non negative V144() Element of NAT
() /. (1 + 1) is Element of the carrier of S
dom () is non empty finite Element of bool NAT
() . 1 is set
len () is V6() V7() V8() V12() non empty finite cardinal V139() V140() ext-real positive non negative V144() Element of NAT
(len X) + 1 is V6() V7() V8() V12() non empty finite cardinal V139() V140() ext-real positive non negative V144() Element of NAT
() . (1 + 1) is set
X . 1 is set
() /. (t + 1) is Element of the carrier of S
() /. ((t + 1) + 1) is Element of the carrier of S
len () is V6() V7() V8() V12() non empty finite cardinal V139() V140() ext-real positive non negative V144() Element of NAT
(len X) + 1 is V6() V7() V8() V12() non empty finite cardinal V139() V140() ext-real positive non negative V144() Element of NAT
dom () is non empty finite Element of bool NAT
() . 0 is set
X . 0 is set
the Source of S . (X . 0) is set
0 + 1 is V6() V7() V8() V12() non empty finite cardinal V139() V140() ext-real positive non negative V144() Element of NAT
() . (0 + 1) is set
the Target of S . (X . 0) is set
S is V6() V7() V8() V12() finite cardinal V139() V140() ext-real non negative V144() Element of NAT
X is V6() V7() V8() V12() finite cardinal V139() V140() ext-real non negative V144() Element of NAT

len v is V6() V7() V8() V12() non empty finite cardinal V139() V140() ext-real positive non negative V144() Element of NAT

len ((S,X) -cut v) is V6() V7() V8() V12() finite cardinal V139() V140() ext-real non negative V144() Element of NAT
X + 1 is V6() V7() V8() V12() non empty finite cardinal V139() V140() ext-real positive non negative V144() Element of NAT
(len ((S,X) -cut v)) + S is V6() V7() V8() V12() finite cardinal V139() V140() ext-real non negative V144() Element of NAT
(X + 1) - (X + 1) is V139() V140() ext-real V144() set
S - ((len ((S,X) -cut v)) + S) is V139() V140() ext-real V144() set
- (len ((S,X) -cut v)) is V139() V140() ext-real non positive V144() set
- (- (len ((S,X) -cut v))) is V139() V140() ext-real non negative V144() set
S is V6() V7() V8() V12() finite cardinal V139() V140() ext-real non negative V144() Element of NAT
X is V6() V7() V8() V12() finite cardinal V139() V140() ext-real non negative V144() Element of NAT
X + 1 is V6() V7() V8() V12() non empty finite cardinal V139() V140() ext-real positive non negative V144() Element of NAT
v is non empty non void V54() MultiGraphStruct
the carrier of v is non empty set

len vk is V6() V7() V8() V12() finite cardinal V139() V140() ext-real non negative V144() Element of NAT

(S,(X + 1)) -cut () is Relation-like NAT -defined the carrier of v -valued Function-like finite FinSequence-like FinSubsequence-like FinSequence of the carrier of v
len () is V6() V7() V8() V12() finite cardinal V139() V140() ext-real non negative V144() Element of NAT
(len vk) + 1 is V6() V7() V8() V12() non empty finite cardinal V139() V140() ext-real positive non negative V144() Element of NAT
len o is V6() V7() V8() V12() finite cardinal V139() V140() ext-real non negative V144() Element of NAT
0 + 1 is V6() V7() V8() V12() non empty finite cardinal V139() V140() ext-real positive non negative V144() Element of NAT
o . (0 + 1) is set
S + 0 is V6() V7() V8() V12() finite cardinal V139() V140() ext-real non negative V144() Element of NAT
vk . (S + 0) is set
len ((S,(X + 1)) -cut ()) is V6() V7() V8() V12() finite cardinal V139() V140() ext-real non negative V144() Element of NAT
() . (S + 0) is set
((S,(X + 1)) -cut ()) . (0 + 1) is set
((S,(X + 1)) -cut ()) . 1 is set
the Source of v is Relation-like the carrier' of v -defined the carrier of v -valued Function-like V36( the carrier' of v, the carrier of v) Element of bool [: the carrier' of v, the carrier of v:]
the carrier' of v is non empty set
[: the carrier' of v, the carrier of v:] is Relation-like set
bool [: the carrier' of v, the carrier of v:] is set
o . 1 is set
the Source of v . (o . 1) is set
S is non empty non void V54() MultiGraphStruct
the Target of S is Relation-like the carrier' of S -defined the carrier of S -valued Function-like V36( the carrier' of S, the carrier of S) Element of bool [: the carrier' of S, the carrier of S:]
the carrier' of S is non empty set
the carrier of S is non empty set
[: the carrier' of S, the carrier of S:] is Relation-like set
bool [: the carrier' of S, the carrier of S:] is set

len X is V6() V7() V8() V12() non empty finite cardinal V139() V140() ext-real positive non negative V144() Element of NAT
(len X) + 1 is V6() V7() V8() V12() non empty finite cardinal V139() V140() ext-real positive non negative V144() Element of NAT
() . ((len X) + 1) is set
X . (len X) is set
the Target of S . (X . (len X)) is set
dom X is non empty finite Element of bool NAT
S is non empty non void V54() MultiGraphStruct

the carrier of S is non empty set
len X is V6() V7() V8() V12() non empty finite cardinal V139() V140() ext-real positive non negative V144() Element of NAT
(len X) + 1 is V6() V7() V8() V12() non empty finite cardinal V139() V140() ext-real positive non negative V144() Element of NAT
() . ((len X) + 1) is set

() . 1 is set

len (X ^ v) is V6() V7() V8() V12() non empty finite cardinal V139() V140() ext-real positive non negative V144() Element of NAT
len v is V6() V7() V8() V12() non empty finite cardinal V139() V140() ext-real positive non negative V144() Element of NAT
(len X) + (len v) is V6() V7() V8() V12() non empty finite cardinal V139() V140() ext-real positive non negative V144() Element of NAT
len () is V6() V7() V8() V12() non empty finite cardinal V139() V140() ext-real positive non negative V144() Element of NAT

a is V6() V7() V8() V12() finite cardinal V139() V140() ext-real non negative V144() Element of NAT
len t is V6() V7() V8() V12() finite cardinal V139() V140() ext-real non negative V144() Element of NAT
the Source of S is Relation-like the carrier' of S -defined the carrier of S -valued Function-like V36( the carrier' of S, the carrier of S) Element of bool [: the carrier' of S, the carrier of S:]
the carrier' of S is non empty set
[: the carrier' of S, the carrier of S:] is Relation-like set
bool [: the carrier' of S, the carrier of S:] is set
a + 1 is V6() V7() V8() V12() non empty finite cardinal V139() V140() ext-real positive non negative V144() Element of NAT
t . (a + 1) is set
the Source of S . (t . (a + 1)) is set
the Target of S is Relation-like the carrier' of S -defined the carrier of S -valued Function-like V36( the carrier' of S, the carrier of S) Element of bool [: the carrier' of S, the carrier of S:]
t . a is set
the Target of S . (t . a) is set
dom X is non empty finite Element of bool NAT
X . (a + 1) is set
X . a is set
dom X is non empty finite Element of bool NAT
X . a is set
dom v is non empty finite Element of bool NAT
v . 1 is set
X . (len X) is set
the Target of S . (X . (len X)) is set
a - (len X) is V139() V140() ext-real V144() set
k is V6() V7() V8() V12() finite cardinal V139() V140() ext-real non negative V144() Element of NAT
(len X) + k is V6() V7() V8() V12() non empty finite cardinal V139() V140() ext-real positive non negative V144() Element of NAT
k + 1 is V6() V7() V8() V12() non empty finite cardinal V139() V140() ext-real positive non negative V144() Element of NAT
(len X) + (k + 1) is V6() V7() V8() V12() non empty finite cardinal V139() V140() ext-real positive non negative V144() Element of NAT
dom v is non empty finite Element of bool NAT
v . (k + 1) is set
v . k is set

len a is V6() V7() V8() V12() non empty finite cardinal V139() V140() ext-real positive non negative V144() Element of NAT
dom X is non empty finite Element of bool NAT
a . (len X) is set
X . (len X) is set
the Source of S is Relation-like the carrier' of S -defined the carrier of S -valued Function-like V36( the carrier' of S, the carrier of S) Element of bool [: the carrier' of S, the carrier of S:]
the carrier' of S is non empty set
[: the carrier' of S, the carrier of S:] is Relation-like set
bool [: the carrier' of S, the carrier of S:] is set
a . ((len X) + 1) is set
the Source of S . (a . ((len X) + 1)) is set
the Target of S is Relation-like the carrier' of S -defined the carrier of S -valued Function-like V36( the carrier' of S, the carrier of S) Element of bool [: the carrier' of S, the carrier of S:]
the Target of S . (a . (len X)) is set
dom v is non empty finite Element of bool NAT
v . 1 is set
the Target of S . (X . (len X)) is set
S is non empty non void V54() MultiGraphStruct

the carrier of S is non empty set
() . 1 is set

() . 1 is set
len X is V6() V7() V8() V12() non empty finite cardinal V139() V140() ext-real positive non negative V144() Element of NAT
(len X) + 1 is V6() V7() V8() V12() non empty finite cardinal V139() V140() ext-real positive non negative V144() Element of NAT
() . ((len X) + 1) is set

len vk is V6() V7() V8() V12() non empty finite cardinal V139() V140() ext-real positive non negative V144() Element of NAT
(len vk) + 1 is V6() V7() V8() V12() non empty finite cardinal V139() V140() ext-real positive non negative V144() Element of NAT
() . ((len vk) + 1) is set
dom X is non empty finite Element of bool NAT
the Source of S is Relation-like the carrier' of S -defined the carrier of S -valued Function-like V36( the carrier' of S, the carrier of S) Element of bool [: the carrier' of S, the carrier of S:]
the carrier' of S is non empty set
[: the carrier' of S, the carrier of S:] is Relation-like set
bool [: the carrier' of S, the carrier of S:] is set
X . 1 is set
the Source of S . (X . 1) is set
the Target of S is Relation-like the carrier' of S -defined the carrier of S -valued Function-like V36( the carrier' of S, the carrier of S) Element of bool [: the carrier' of S, the carrier of S:]
X . (len X) is set
the Target of S . (X . (len X)) is set
dom v is non empty finite Element of bool NAT
len v is V6() V7() V8() V12() non empty finite cardinal V139() V140() ext-real positive non negative V144() Element of NAT
v . 1 is set
the Source of S . (v . 1) is set
dom vk is non empty finite Element of bool NAT
vk . (len vk) is set
the Target of S . (vk . (len vk)) is set
(len v) + (len vk) is V6() V7() V8() V12() non empty finite cardinal V139() V140() ext-real positive non negative V144() Element of NAT
S is non empty non void V54() MultiGraphStruct

the carrier of S is non empty set
() . 1 is set
len X is V6() V7() V8() V12() non empty finite cardinal V139() V140() ext-real positive non negative V144() Element of NAT
(len X) + 1 is V6() V7() V8() V12() non empty finite cardinal V139() V140() ext-real positive non negative V144() Element of NAT
() . ((len X) + 1) is set
len () is V6() V7() V8() V12() non empty finite cardinal V139() V140() ext-real positive non negative V144() Element of NAT
S is non empty non void V54() MultiGraphStruct

proj2 X is non empty finite set
the carrier' of S is non empty set
len X is V6() V7() V8() V12() non empty finite cardinal V139() V140() ext-real positive non negative V144() Element of NAT
dom X is non empty finite Element of bool NAT
X . (len X) is set
v is Element of the carrier' of S

the carrier' of S * is functional non empty FinSequence-membered M8( the carrier' of S)

proj2 vk is finite set
{(X . (len X))} is non empty trivial finite 1 -element set
len vk is V6() V7() V8() V12() finite cardinal V139() V140() ext-real non negative V144() Element of NAT
o is V6() V7() V8() V12() finite cardinal V139() V140() ext-real non negative V144() Element of NAT
o + 1 is V6() V7() V8() V12() non empty finite cardinal V139() V140() ext-real positive non negative V144() Element of NAT

len t is V6() V7() V8() V12() finite cardinal V139() V140() ext-real non negative V144() Element of NAT

the carrier of S is non empty set
the Source of S is Relation-like the carrier' of S -defined the carrier of S -valued Function-like V36( the carrier' of S, the carrier of S) Element of bool [: the carrier' of S, the carrier of S:]
[: the carrier' of S, the carrier of S:] is Relation-like set
bool [: the carrier' of S, the carrier of S:] is set
the Source of S . v is Element of the carrier of S
the Target of S is Relation-like the carrier' of S -defined the carrier of S -valued Function-like V36( the carrier' of S, the carrier of S) Element of bool [: the carrier' of S, the carrier of S:]
the Target of S . v is Element of the carrier of S
<*( the Source of S . v),( the Target of S . v)*> is Relation-like NAT -defined the carrier of S -valued Function-like non empty finite 2 -element FinSequence-like FinSubsequence-like Element of the carrier of S *
the carrier of S * is functional non empty FinSequence-membered M8( the carrier of S)
(len vk) + 1 is V6() V7() V8() V12() non empty finite cardinal V139() V140() ext-real positive non negative V144() Element of NAT
() . ((len vk) + 1) is set

(len X) + 1 is V6() V7() V8() V12() non empty finite cardinal V139() V140() ext-real positive non negative V144() Element of NAT
() . ((len X) + 1) is set
() . 1 is set

t . 1 is set
a is V6() V7() V8() V12() finite cardinal V139() V140() ext-real non negative V144() set
X . a is set

the carrier of S is non empty set
the Source of S is Relation-like the carrier' of S -defined the carrier of S -valued Function-like V36( the carrier' of S, the carrier of S) Element of bool [: the carrier' of S, the carrier of S:]
[: the carrier' of S, the carrier of S:] is Relation-like set
bool [: the carrier' of S, the carrier of S:] is set
the Source of S . v is Element of the carrier of S
the Target of S is Relation-like the carrier' of S -defined the carrier of S -valued Function-like V36( the carrier' of S, the carrier of S) Element of bool [: the carrier' of S, the carrier of S:]
the Target of S . v is Element of the carrier of S
<*( the Source of S . v),( the Target of S . v)*> is Relation-like NAT -defined the carrier of S -valued Function-like non empty finite 2 -element FinSequence-like FinSubsequence-like Element of the carrier of S *
the carrier of S * is functional non empty FinSequence-membered M8( the carrier of S)
(len vk) + 1 is V6() V7() V8() V12() non empty finite cardinal V139() V140() ext-real positive non negative V144() Element of NAT
() . ((len vk) + 1) is set

(len X) + 1 is V6() V7() V8() V12() non empty finite cardinal V139() V140() ext-real positive non negative V144() Element of NAT
() . ((len X) + 1) is set
() . 1 is set
the Source of S . (t . 1) is set

() . 1 is set

proj2 a9 is finite set
(proj2 vk) \/ () is finite set
len a9 is V6() V7() V8() V12() finite cardinal V139() V140() ext-real non negative V144() Element of NAT

(len a9) + 1 is V6() V7() V8() V12() non empty finite cardinal V139() V140() ext-real positive non negative V144() Element of NAT
() . ((len a9) + 1) is set
(len t) + 1 is V6() V7() V8() V12() non empty finite cardinal V139() V140() ext-real positive non negative V144() Element of NAT
() . ((len t) + 1) is set

1 + 1 is V6() V7() V8() V12() non empty finite cardinal V139() V140() ext-real positive non negative V144() Element of NAT
k is V6() V7() V8() V12() finite cardinal V139() V140() ext-real non negative V144() Element of NAT
k + 1 is V6() V7() V8() V12() non empty finite cardinal V139() V140() ext-real positive non negative V144() Element of NAT
X . k is set
ak is Element of the carrier' of S

the carrier of S is non empty set
len a9 is V6() V7() V8() V12() finite cardinal V139() V140() ext-real non negative V144() Element of NAT
the Source of S is Relation-like the carrier' of S -defined the carrier of S -valued Function-like V36( the carrier' of S, the carrier of S) Element of bool [: the carrier' of S, the carrier of S:]
[: the carrier' of S, the carrier of S:] is Relation-like set
bool [: the carrier' of S, the carrier of S:] is set
the Source of S . ak is Element of the carrier of S
the Target of S is Relation-like the carrier' of S -defined the carrier of S -valued Function-like V36( the carrier' of S, the carrier of S) Element of bool [: the carrier' of S, the carrier of S:]
the Target of S . ak is Element of the carrier of S
<*( the Source of S . ak),( the Target of S . ak)*> is Relation-like NAT -defined the carrier of S -valued Function-like non empty finite 2 -element FinSequence-like FinSubsequence-like Element of the carrier of S *
the carrier of S * is functional non empty FinSequence-membered M8( the carrier of S)
(len a9) + 1 is V6() V7() V8() V12() non empty finite cardinal V139() V140() ext-real positive non negative V144() Element of NAT
() . ((len a9) + 1) is set
the Source of S . (t . 1) is set

() . 1 is set

proj2 a9 is finite set
{(X . k)} is non empty trivial finite 1 -element set

proj2 ttk is finite set
(proj2 a9) \/ () is finite set
len ttk is V6() V7() V8() V12() finite cardinal V139() V140() ext-real non negative V144() Element of NAT

(len ttk) + 1 is V6() V7() V8() V12() non empty finite cardinal V139() V140() ext-real positive non negative V144() Element of NAT
(vertex-seq ttk) . ((len ttk) + 1) is set
(len t) + 1 is V6() V7() V8() V12() non empty finite cardinal V139() V140() ext-real positive non negative V144() Element of NAT
() . ((len t) + 1) is set

() . 1 is set

len k is V6() V7() V8() V12() finite cardinal V139() V140() ext-real non negative V144() Element of NAT

v is V6() V7() V8() V12() finite cardinal V139() V140() ext-real non negative V144() Element of NAT

len o is V6() V7() V8() V12() finite cardinal V139() V140() ext-real non negative V144() Element of NAT

proj2 vk is finite set
len vk is V6() V7() V8() V12() finite cardinal V139() V140() ext-real non negative V144() Element of NAT

S is non empty V54() MultiGraphStruct

the carrier' of S is set
S is non empty void V54() trivial' () MultiGraphStruct

S is non empty V54() MultiGraphStruct
the carrier of S is non empty set
v is Element of the carrier of S

len vk is V6() V7() V8() V12() finite cardinal V139() V140() ext-real non negative V144() Element of NAT
(len vk) + 1 is V6() V7() V8() V12() non empty finite cardinal V139() V140() ext-real positive non negative V144() Element of NAT
() . ((len vk) + 1) is set
X is non empty void V54() trivial' () MultiGraphStruct

S is non empty V54() MultiGraphStruct
the non empty void V54() trivial' () () MultiGraphStruct is non empty void V54() trivial' () () MultiGraphStruct
S is non empty V54() MultiGraphStruct
X is non empty void V54() trivial' () () MultiGraphStruct
X is non empty non void V54() MultiGraphStruct

the carrier of X is non empty set
len () is V6() V7() V8() V12() finite cardinal V139() V140() ext-real non negative V144() Element of NAT
len v is V6() V7() V8() V12() finite cardinal V139() V140() ext-real non negative V144() Element of NAT
(len v) + 1 is V6() V7() V8() V12() non empty finite cardinal V139() V140() ext-real positive non negative V144() Element of NAT

the carrier of S is non empty set
() . 1 is set
o is Element of the carrier of S
t is V6() V7() V8() V12() finite cardinal V139() V140() ext-real non negative V144() Element of NAT
t + 1 is V6() V7() V8() V12() non empty finite cardinal V139() V140() ext-real positive non negative V144() Element of NAT

len a is V6() V7() V8() V12() finite cardinal V139() V140() ext-real non negative V144() Element of NAT

() . ((len v) + 1) is set

len ak is V6() V7() V8() V12() non empty finite cardinal V139() V140() ext-real positive non negative V144() Element of NAT
(len ak) + 1 is V6() V7() V8() V12() non empty finite cardinal V139() V140() ext-real positive non negative V144() Element of NAT
() . ((len ak) + 1) is set
(t + 1) + (len v) is V6() V7() V8() V12() non empty finite cardinal V139() V140() ext-real positive non negative V144() Element of NAT
{1} is non empty trivial finite V28() 1 -element set

bool [:{1},{1}:] is finite V28() set
v is finite Element of {1}

MultiGraphStruct(# {1},{1},vk,o #) is strict MultiGraphStruct
t is non empty V54() MultiGraphStruct
the carrier of t is non empty set
vk . 1 is set

a is Element of the carrier of t

the carrier of t * is functional non empty FinSequence-membered M8( the carrier of t)
<*a,a*> . 2 is set
len <*a,a*> is V6() V7() V8() V12() non empty finite cardinal V139() V140() ext-real positive non negative V144() Element of NAT
<*a,a*> . 1 is set
k is non empty V54() () () MultiGraphStruct
the non empty V54() () () MultiGraphStruct is non empty V54() () () MultiGraphStruct

proj1 S is non empty Tree-like set

v is V6() V7() V8() V12() finite cardinal V139() V140() ext-real non negative V144() Element of NAT

bool is non trivial non finite set
S is non empty non void V54() ManySortedSign
the carrier of S is non empty set
the carrier' of S is non empty set

{ the carrier of S} is non empty trivial finite 1 -element set
[: the carrier' of S,{ the carrier of S}:] is Relation-like set

Union () is non empty set
[: the carrier' of S,{ the carrier of S}:] \/ (Union ()) is non empty set
REL X is Relation-like [: the carrier' of S,{ the carrier of S}:] \/ (Union ()) -defined ([: the carrier' of S,{ the carrier of S}:] \/ (Union ())) * -valued Element of bool [:([: the carrier' of S,{ the carrier of S}:] \/ (Union ())),(([: the carrier' of S,{ the carrier of S}:] \/ (Union ())) *):]
([: the carrier' of S,{ the carrier of S}:] \/ (Union ())) * is functional non empty FinSequence-membered M8([: the carrier' of S,{ the carrier of S}:] \/ (Union ()))
[:([: the carrier' of S,{ the carrier of S}:] \/ (Union ())),(([: the carrier' of S,{ the carrier of S}:] \/ (Union ())) *):] is Relation-like set
bool [:([: the carrier' of S,{ the carrier of S}:] \/ (Union ())),(([: the carrier' of S,{ the carrier of S}:] \/ (Union ())) *):] is set
G13(([: the carrier' of S,{ the carrier of S}:] \/ (Union ())),(REL X)) is strict L13()
the carrier of () is non empty set
FinTrees the carrier of () is functional non empty constituted-DTrees DTree-set of the carrier of ()
S -Terms X is functional non empty constituted-DTrees Element of bool (FinTrees the carrier of ())
bool (FinTrees the carrier of ()) is set

v . {} is set
vk is Element of the carrier of S
X . vk is non empty set
o is Element of X . vk
[o,vk] is V21() set
{o,vk} is non empty finite set
{o} is non empty trivial finite 1 -element set
{{o,vk},{o}} is non empty finite V28() set
vk is Element of the carrier of S
X . vk is non empty set
o is Element of X . vk
[o,vk] is V21() set
{o,vk} is non empty finite set
{o} is non empty trivial finite 1 -element set
{{o,vk},{o}} is non empty finite V28() set

vk is set
o is set
[vk,o] is V21() set
{vk,o} is non empty