:: TREES_9 semantic presentation

REAL is set

NAT is epsilon-transitive epsilon-connected ordinal non empty non trivial non finite cardinal limit_cardinal Element of bool REAL

bool REAL is non empty set

NAT is epsilon-transitive epsilon-connected ordinal non empty non trivial non finite cardinal limit_cardinal set

bool NAT is non empty non trivial non finite set

bool NAT is non empty non trivial non finite set

{} is Relation-like non-empty empty-yielding NAT -defined epsilon-transitive epsilon-connected ordinal T-Sequence-like c=-linear natural ext-real non negative V16() empty trivial V20() Function-like one-to-one constant functional finite finite-yielding V37() cardinal {} -element FinSequence-like FinSubsequence-like FinSequence-membered constituted-Trees constituted-FinTrees constituted-DTrees Tree-yielding FinTree-yielding DTree-yielding set

the Relation-like non-empty empty-yielding NAT -defined epsilon-transitive epsilon-connected ordinal T-Sequence-like c=-linear natural ext-real non negative V16() empty trivial V20() Function-like one-to-one constant functional finite finite-yielding V37() cardinal {} -element FinSequence-like FinSubsequence-like FinSequence-membered constituted-Trees constituted-FinTrees constituted-DTrees Tree-yielding FinTree-yielding DTree-yielding set is Relation-like non-empty empty-yielding NAT -defined epsilon-transitive epsilon-connected ordinal T-Sequence-like c=-linear natural ext-real non negative V16() empty trivial V20() Function-like one-to-one constant functional finite finite-yielding V37() cardinal {} -element FinSequence-like FinSubsequence-like FinSequence-membered constituted-Trees constituted-FinTrees constituted-DTrees Tree-yielding FinTree-yielding DTree-yielding set

1 is epsilon-transitive epsilon-connected ordinal natural ext-real positive non negative V16() non empty V20() finite cardinal Element of NAT

{{},1} is non empty finite V37() set

Trees is non empty constituted-Trees set

bool Trees is non empty set

FinTrees is non empty constituted-Trees constituted-FinTrees Element of bool Trees

[:{},{}:] is Relation-like non-empty empty-yielding NAT -defined epsilon-transitive epsilon-connected ordinal T-Sequence-like c=-linear natural ext-real non negative V16() empty trivial V20() Function-like one-to-one constant functional finite finite-yielding V37() cardinal {} -element FinSequence-like FinSubsequence-like FinSequence-membered constituted-Trees constituted-FinTrees constituted-DTrees Tree-yielding FinTree-yielding DTree-yielding set

2 is epsilon-transitive epsilon-connected ordinal natural ext-real positive non negative V16() non empty V20() finite cardinal Element of NAT

3 is epsilon-transitive epsilon-connected ordinal natural ext-real positive non negative V16() non empty V20() finite cardinal Element of NAT

0 is Relation-like non-empty empty-yielding NAT -defined epsilon-transitive epsilon-connected ordinal T-Sequence-like c=-linear natural ext-real non negative V16() empty trivial V20() Function-like one-to-one constant functional finite finite-yielding V37() cardinal {} -element FinSequence-like FinSubsequence-like FinSequence-membered constituted-Trees constituted-FinTrees constituted-DTrees Tree-yielding FinTree-yielding DTree-yielding Element of NAT

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

{1} is non empty trivial finite V37() 1 -element set

Seg 2 is non empty finite 2 -element Element of bool NAT

{1,2} is non empty finite V37() set

NAT * is non empty functional FinSequence-membered M8( NAT )

<*> NAT is Relation-like non-empty empty-yielding NAT -defined NAT -valued epsilon-transitive epsilon-connected ordinal T-Sequence-like c=-linear natural ext-real non negative V16() empty trivial proper V20() Function-like one-to-one constant functional finite finite-yielding V37() cardinal {} -element FinSequence-like FinSubsequence-like FinSequence-membered constituted-Trees constituted-FinTrees constituted-DTrees Tree-yielding FinTree-yielding DTree-yielding FinSequence of NAT

[:NAT,NAT:] is Relation-like non empty non trivial non finite set

elementary_tree 0 is non empty finite Tree-like set

{{}} is non empty trivial functional finite V37() 1 -element Tree-like set

<*0*> is Relation-like NAT -defined NAT -valued non empty trivial Function-like constant finite 1 -element FinSequence-like FinSubsequence-like FinSequence of NAT

^ (elementary_tree 0) is non empty finite Tree-like set

<*(elementary_tree 0)*> is Relation-like NAT -defined non empty trivial Function-like constant finite 1 -element FinSequence-like FinSubsequence-like Tree-yielding FinTree-yielding set

tree <*(elementary_tree 0)*> is non empty finite Tree-like set

elementary_tree 1 is non empty finite Tree-like set

B is non empty set

g is non empty functional constituted-DTrees DTree-set of B

bool g is non empty set

f is non empty functional constituted-DTrees Element of bool g

m is Relation-like Function-like DecoratedTree-like Element of f

B is non empty Tree-like set

g is non empty finite Tree-like set

card g is epsilon-transitive epsilon-connected ordinal natural ext-real non negative V16() non empty V20() finite cardinal Element of NAT

(card g) + 1 is epsilon-transitive epsilon-connected ordinal natural ext-real positive non negative V16() non empty V20() finite cardinal Element of NAT

f is epsilon-transitive epsilon-connected ordinal natural ext-real positive non negative V16() non empty V20() finite cardinal Element of NAT

<*f*> is Relation-like NAT -defined NAT -valued non empty trivial Function-like constant finite 1 -element FinSequence-like FinSubsequence-like FinSequence of NAT

m is Relation-like NAT -defined NAT -valued Function-like finite FinSequence-like FinSubsequence-like Element of B

m ^ <*f*> is Relation-like NAT -defined NAT -valued non empty Function-like finite FinSequence-like FinSubsequence-like FinSequence of NAT

t is Relation-like NAT -defined Function-like finite FinSequence-like FinSubsequence-like set

len t is epsilon-transitive epsilon-connected ordinal natural ext-real non negative V16() V20() finite cardinal Element of NAT

dom t is finite Element of bool NAT

Seg f is non empty finite f -element Element of bool NAT

proj2 t is finite set

succ m is Element of bool B

bool B is non empty set

{ (m ^ <*b

fk is set

fm is set

t . fm is set

n is epsilon-transitive epsilon-connected ordinal natural ext-real non negative V16() V20() finite cardinal Element of NAT

t9 is epsilon-transitive epsilon-connected ordinal natural ext-real non negative V16() V20() finite cardinal set

1 + t9 is epsilon-transitive epsilon-connected ordinal natural ext-real positive non negative V16() non empty V20() finite cardinal Element of NAT

n is epsilon-transitive epsilon-connected ordinal natural ext-real non negative V16() V20() finite cardinal Element of NAT

<*n*> is Relation-like NAT -defined NAT -valued non empty trivial Function-like constant finite 1 -element FinSequence-like FinSubsequence-like FinSequence of NAT

m ^ <*n*> is Relation-like NAT -defined NAT -valued non empty Function-like finite FinSequence-like FinSubsequence-like FinSequence of NAT

n - 1 is ext-real V16() V20() set

card (succ m) is epsilon-transitive epsilon-connected ordinal cardinal set

card B is epsilon-transitive epsilon-connected ordinal non empty cardinal set

fk is set

proj1 t is finite set

fm is set

t . fk is set

t . fm is set

n is epsilon-transitive epsilon-connected ordinal natural ext-real non negative V16() V20() finite cardinal Element of NAT

n - 1 is ext-real V16() V20() set

<*(n - 1)*> is Relation-like NAT -defined non empty trivial Function-like constant finite 1 -element FinSequence-like FinSubsequence-like set

m ^ <*(n - 1)*> is Relation-like NAT -defined non empty Function-like finite FinSequence-like FinSubsequence-like set

t9 is epsilon-transitive epsilon-connected ordinal natural ext-real non negative V16() V20() finite cardinal Element of NAT

t9 - 1 is ext-real V16() V20() set

<*(t9 - 1)*> is Relation-like NAT -defined non empty trivial Function-like constant finite 1 -element FinSequence-like FinSubsequence-like set

m ^ <*(t9 - 1)*> is Relation-like NAT -defined non empty Function-like finite FinSequence-like FinSubsequence-like set

<*(t9 - 1)*> . 1 is set

card (dom t) is epsilon-transitive epsilon-connected ordinal natural ext-real non negative V16() V20() finite cardinal Element of NAT

card (Seg f) is epsilon-transitive epsilon-connected ordinal natural ext-real non negative V16() non empty V20() finite cardinal Element of NAT

(card g) + 0 is epsilon-transitive epsilon-connected ordinal natural ext-real non negative V16() non empty V20() finite cardinal Element of NAT

B is set

g is Relation-like NAT -defined Function-like finite FinSequence-like FinSubsequence-like set

dom g is finite Element of bool NAT

len g is epsilon-transitive epsilon-connected ordinal natural ext-real non negative V16() V20() finite cardinal Element of NAT

f is epsilon-transitive epsilon-connected ordinal natural ext-real non negative V16() V20() finite cardinal Element of NAT

m is epsilon-transitive epsilon-connected ordinal natural ext-real non negative V16() V20() finite cardinal set

1 + m is epsilon-transitive epsilon-connected ordinal natural ext-real positive non negative V16() non empty V20() finite cardinal Element of NAT

t is epsilon-transitive epsilon-connected ordinal natural ext-real non negative V16() V20() finite cardinal Element of NAT

t + 1 is epsilon-transitive epsilon-connected ordinal natural ext-real positive non negative V16() non empty V20() finite cardinal Element of NAT

B is Relation-like NAT -defined Function-like finite FinSequence-like FinSubsequence-like set

len B is epsilon-transitive epsilon-connected ordinal natural ext-real non negative V16() V20() finite cardinal Element of NAT

g is Relation-like NAT -defined Function-like finite FinSequence-like FinSubsequence-like set

len g is epsilon-transitive epsilon-connected ordinal natural ext-real non negative V16() V20() finite cardinal Element of NAT

f is epsilon-transitive epsilon-connected ordinal natural ext-real non negative V16() V20() finite cardinal set

dom B is finite Element of bool NAT

B . f is set

g . f is set

m is epsilon-transitive epsilon-connected ordinal natural ext-real non negative V16() V20() finite cardinal Element of NAT

m + 1 is epsilon-transitive epsilon-connected ordinal natural ext-real positive non negative V16() non empty V20() finite cardinal Element of NAT

dom g is finite Element of bool NAT

B is epsilon-transitive epsilon-connected ordinal natural ext-real non negative V16() V20() finite cardinal Element of NAT

B + 1 is epsilon-transitive epsilon-connected ordinal natural ext-real positive non negative V16() non empty V20() finite cardinal Element of NAT

g is Relation-like NAT -defined Function-like finite FinSequence-like FinSubsequence-like set

len g is epsilon-transitive epsilon-connected ordinal natural ext-real non negative V16() V20() finite cardinal Element of NAT

dom g is finite Element of bool NAT

g . (B + 1) is set

proj2 g is finite set

0 + 1 is epsilon-transitive epsilon-connected ordinal natural ext-real positive non negative V16() non empty V20() finite cardinal Element of NAT

g is set

B is Relation-like NAT -defined Function-like finite FinSequence-like FinSubsequence-like set

proj2 B is finite set

dom B is finite Element of bool NAT

f is set

B . f is set

len B is epsilon-transitive epsilon-connected ordinal natural ext-real non negative V16() V20() finite cardinal Element of NAT

m is epsilon-transitive epsilon-connected ordinal natural ext-real non negative V16() V20() finite cardinal Element of NAT

m + 1 is epsilon-transitive epsilon-connected ordinal natural ext-real positive non negative V16() non empty V20() finite cardinal Element of NAT

B is Relation-like Function-like DecoratedTree-like set

B | (<*> NAT) is Relation-like Function-like DecoratedTree-like set

proj1 (B | (<*> NAT)) is non empty Tree-like set

proj1 B is non empty Tree-like set

(proj1 B) | (<*> NAT) is non empty Tree-like set

g is Relation-like NAT -defined NAT -valued Function-like finite FinSequence-like FinSubsequence-like FinSequence of NAT

(B | (<*> NAT)) . g is set

{} ^ g is Relation-like NAT -defined Function-like finite FinSequence-like FinSubsequence-like set

B . ({} ^ g) is set

B . g is set

B is non empty Tree-like set

g is Relation-like NAT -defined NAT -valued Function-like finite FinSequence-like FinSubsequence-like FinSequence of NAT

f is Relation-like NAT -defined NAT -valued Function-like finite FinSequence-like FinSubsequence-like FinSequence of NAT

g ^ f is Relation-like NAT -defined NAT -valued Function-like finite FinSequence-like FinSubsequence-like FinSequence of NAT

B | (g ^ f) is non empty Tree-like set

B | g is non empty Tree-like set

(B | g) | f is non empty Tree-like set

m is Relation-like NAT -defined NAT -valued Function-like finite FinSequence-like FinSubsequence-like FinSequence of NAT

f ^ m is Relation-like NAT -defined NAT -valued Function-like finite FinSequence-like FinSubsequence-like FinSequence of NAT

(g ^ f) ^ m is Relation-like NAT -defined NAT -valued Function-like finite FinSequence-like FinSubsequence-like FinSequence of NAT

g ^ (f ^ m) is Relation-like NAT -defined NAT -valued Function-like finite FinSequence-like FinSubsequence-like FinSequence of NAT

B is Relation-like Function-like DecoratedTree-like set

proj1 B is non empty Tree-like set

g is Relation-like NAT -defined NAT -valued Function-like finite FinSequence-like FinSubsequence-like FinSequence of NAT

f is Relation-like NAT -defined NAT -valued Function-like finite FinSequence-like FinSubsequence-like FinSequence of NAT

g ^ f is Relation-like NAT -defined NAT -valued Function-like finite FinSequence-like FinSubsequence-like FinSequence of NAT

B | (g ^ f) is Relation-like Function-like DecoratedTree-like set

B | g is Relation-like Function-like DecoratedTree-like set

(B | g) | f is Relation-like Function-like DecoratedTree-like set

proj1 (B | g) is non empty Tree-like set

(proj1 B) | g is non empty Tree-like set

proj1 (B | (g ^ f)) is non empty Tree-like set

(proj1 B) | (g ^ f) is non empty Tree-like set

m is Relation-like NAT -defined NAT -valued Function-like finite FinSequence-like FinSubsequence-like FinSequence of NAT

(g ^ f) ^ m is Relation-like NAT -defined NAT -valued Function-like finite FinSequence-like FinSubsequence-like FinSequence of NAT

f ^ m is Relation-like NAT -defined NAT -valued Function-like finite FinSequence-like FinSubsequence-like FinSequence of NAT

g ^ (f ^ m) is Relation-like NAT -defined NAT -valued Function-like finite FinSequence-like FinSubsequence-like FinSequence of NAT

((proj1 B) | g) | f is non empty Tree-like set

(B | (g ^ f)) . m is set

B . ((g ^ f) ^ m) is set

(B | g) . (f ^ m) is set

((B | g) | f) . m is set

proj1 ((B | g) | f) is non empty Tree-like set

(proj1 (B | g)) | f is non empty Tree-like set

B is Relation-like Function-like DecoratedTree-like set

proj1 B is non empty Tree-like set

g is set

{g} is non empty trivial finite 1 -element set

f is set

m is set

[f,m] is non empty V27() set

{f,m} is non empty finite set

{f} is non empty trivial finite 1 -element set

{{f,m},{f}} is non empty finite V37() set

B is Relation-like Function-like DecoratedTree-like set

proj1 B is non empty Tree-like set

Leaves (proj1 B) is Element of bool (proj1 B)

bool (proj1 B) is non empty set

g is Relation-like NAT -defined NAT -valued Function-like finite FinSequence-like FinSubsequence-like Element of proj1 B

g ^ <*0*> is Relation-like NAT -defined NAT -valued non empty Function-like finite FinSequence-like FinSubsequence-like FinSequence of NAT

f is Relation-like NAT -defined NAT -valued Function-like finite FinSequence-like FinSubsequence-like FinSequence of NAT

t is epsilon-transitive epsilon-connected ordinal natural ext-real non negative V16() V20() finite cardinal Element of NAT

<*t*> is Relation-like NAT -defined NAT -valued non empty trivial Function-like constant finite 1 -element FinSequence-like FinSubsequence-like FinSequence of NAT

m is Relation-like NAT -defined NAT -valued Function-like finite FinSequence-like FinSubsequence-like FinSequence of NAT

<*t*> ^ m is Relation-like NAT -defined NAT -valued non empty Function-like finite FinSequence-like FinSubsequence-like FinSequence of NAT

g ^ <*t*> is Relation-like NAT -defined NAT -valued non empty Function-like finite FinSequence-like FinSubsequence-like FinSequence of NAT

B is non empty Tree-like set

Leaves B is Element of bool B

bool B is non empty set

g is Relation-like NAT -defined NAT -valued Function-like finite FinSequence-like FinSubsequence-like Element of B

B | g is non empty Tree-like set

g ^ <*0*> is Relation-like NAT -defined NAT -valued non empty Function-like finite FinSequence-like FinSubsequence-like FinSequence of NAT

f is Relation-like NAT -defined NAT -valued Function-like finite FinSequence-like FinSubsequence-like FinSequence of NAT

g ^ f is Relation-like NAT -defined NAT -valued Function-like finite FinSequence-like FinSubsequence-like FinSequence of NAT

g ^ {} is Relation-like NAT -defined Function-like finite FinSequence-like FinSubsequence-like set

B is Relation-like Function-like DecoratedTree-like set

proj1 B is non empty Tree-like set

Leaves (proj1 B) is Element of bool (proj1 B)

bool (proj1 B) is non empty set

g is Relation-like NAT -defined NAT -valued Function-like finite FinSequence-like FinSubsequence-like Element of proj1 B

B | g is Relation-like Function-like DecoratedTree-like set

proj1 (B | g) is non empty Tree-like set

(proj1 B) | g is non empty Tree-like set

FinTrees NAT is non empty functional constituted-DTrees DTree-set of NAT

root-tree 0 is Relation-like NAT -valued Function-like finite DecoratedTree-like Element of FinTrees NAT

K158((elementary_tree 0),0) is Relation-like elementary_tree 0 -defined {0} -valued Function-like V30( elementary_tree 0,{0}) finite DecoratedTree-like Element of bool [:(elementary_tree 0),{0}:]

{0} is non empty trivial functional finite V37() 1 -element Tree-like finite-order set

[:(elementary_tree 0),{0}:] is Relation-like non empty finite set

bool [:(elementary_tree 0),{0}:] is non empty finite V37() set

B is Relation-like NAT -valued Function-like finite DecoratedTree-like Element of FinTrees NAT

proj1 B is non empty finite Tree-like finite-order set

root-tree 0 is Relation-like NAT -valued Function-like finite DecoratedTree-like Element of FinTrees NAT

FinTrees NAT is non empty functional constituted-DTrees DTree-set of NAT

K158((elementary_tree 0),0) is Relation-like elementary_tree 0 -defined {0} -valued Function-like V30( elementary_tree 0,{0}) finite DecoratedTree-like Element of bool [:(elementary_tree 0),{0}:]

{0} is non empty trivial functional finite V37() 1 -element Tree-like finite-order set

[:(elementary_tree 0),{0}:] is Relation-like non empty finite set

bool [:(elementary_tree 0),{0}:] is non empty finite V37() set

0 -tree (root-tree 0) is Relation-like Function-like DecoratedTree-like set

<*(root-tree 0)*> is Relation-like NAT -defined non empty trivial Function-like constant finite 1 -element FinSequence-like FinSubsequence-like DTree-yielding set

0 -tree <*(root-tree 0)*> is Relation-like Function-like DecoratedTree-like set

B is Relation-like Function-like DecoratedTree-like set

proj1 B is non empty Tree-like set

proj1 (root-tree 0) is non empty finite Tree-like finite-order set

^ (proj1 (root-tree 0)) is non empty finite Tree-like finite-order set

<*(proj1 (root-tree 0))*> is Relation-like NAT -defined non empty trivial Function-like constant finite 1 -element FinSequence-like FinSubsequence-like Tree-yielding FinTree-yielding set

tree <*(proj1 (root-tree 0))*> is non empty finite Tree-like finite-order set

B . {} is set

root-tree (B . {}) is Relation-like Function-like finite DecoratedTree-like set

K158((elementary_tree 0),(B . {})) is Relation-like elementary_tree 0 -defined {(B . {})} -valued Function-like V30( elementary_tree 0,{(B . {})}) finite DecoratedTree-like Element of bool [:(elementary_tree 0),{(B . {})}:]

{(B . {})} is non empty trivial finite 1 -element set

[:(elementary_tree 0),{(B . {})}:] is Relation-like non empty finite set

bool [:(elementary_tree 0),{(B . {})}:] is non empty finite V37() set

<*(root-tree 0)*> is Relation-like NAT -defined FinTrees NAT -valued non empty trivial Function-like constant finite 1 -element FinSequence-like FinSubsequence-like DTree-yielding FinSequence of FinTrees NAT

0 -tree <*(root-tree 0)*> is Relation-like NAT -valued Function-like finite DecoratedTree-like Element of FinTrees NAT

B is set

root-tree B is Relation-like Function-like finite DecoratedTree-like set

K158((elementary_tree 0),B) is Relation-like elementary_tree 0 -defined {B} -valued Function-like V30( elementary_tree 0,{B}) finite DecoratedTree-like Element of bool [:(elementary_tree 0),{B}:]

{B} is non empty trivial finite 1 -element set

[:(elementary_tree 0),{B}:] is Relation-like non empty finite set

bool [:(elementary_tree 0),{B}:] is non empty finite V37() set

proj1 (root-tree B) is non empty finite Tree-like finite-order set

B is non empty Tree-like set

f is Relation-like NAT -defined NAT -valued Function-like finite FinSequence-like FinSubsequence-like Element of B

succ f is Element of bool B

bool B is non empty set

{ (f ^ <*b

g is non empty Tree-like finite-order set

m is Relation-like NAT -defined NAT -valued Function-like finite FinSequence-like FinSubsequence-like Element of g

succ m is finite Element of bool g

bool g is non empty set

{ (m ^ <*b

B is Relation-like Function-like DecoratedTree-like set

proj1 B is non empty Tree-like set

B is Relation-like Function-like DecoratedTree-like set

proj1 B is non empty Tree-like set

B is Relation-like Function-like DecoratedTree-like () () set

proj1 B is non empty Tree-like set

B is Relation-like Function-like DecoratedTree-like () set

proj1 B is non empty Tree-like set

B is non empty Tree-like () set

g is Relation-like NAT -defined NAT -valued Function-like finite FinSequence-like FinSubsequence-like Element of B

succ g is Element of bool B

bool B is non empty set

{ (g ^ <*b

F

card F

B is Relation-like Function-like set

proj1 B is set

g is epsilon-transitive epsilon-connected ordinal natural ext-real non negative V16() V20() finite cardinal Element of NAT

F

g + 1 is epsilon-transitive epsilon-connected ordinal natural ext-real positive non negative V16() non empty V20() finite cardinal Element of NAT

F

f is Relation-like Function-like set

proj1 f is set

{ b

proj2 f is set

m is set

t is set

f . t is set

fk is epsilon-transitive epsilon-connected ordinal natural ext-real non negative V16() V20() finite cardinal Element of NAT

F

m is set

t is epsilon-transitive epsilon-connected ordinal natural ext-real non negative V16() V20() finite cardinal Element of NAT

F

f . t is set

m is set

t is set

f . m is set

f . t is set

F

F

fk is epsilon-transitive epsilon-connected ordinal natural ext-real non negative V16() V20() finite cardinal Element of NAT

fm is epsilon-transitive epsilon-connected ordinal natural ext-real non negative V16() V20() finite cardinal Element of NAT

{ b

g is set

f is set

B . g is set

B . f is set

F

F

m is epsilon-transitive epsilon-connected ordinal natural ext-real non negative V16() V20() finite cardinal Element of NAT

t is epsilon-transitive epsilon-connected ordinal natural ext-real non negative V16() V20() finite cardinal Element of NAT

proj2 B is set

card (proj2 B) is epsilon-transitive epsilon-connected ordinal cardinal set

card (card F

f is epsilon-transitive epsilon-connected ordinal natural ext-real non negative V16() V20() finite cardinal Element of NAT

F

F

{F

F

bool F

m is set

t is set

B . t is set

fk is epsilon-transitive epsilon-connected ordinal natural ext-real non negative V16() V20() finite cardinal Element of NAT

F

g is finite set

card g is epsilon-transitive epsilon-connected ordinal natural ext-real non negative V16() V20() finite cardinal Element of NAT

card (F

card {F

(card F

(card g) - 1 is ext-real V16() V20() set

(card g) + 1 is epsilon-transitive epsilon-connected ordinal natural ext-real positive non negative V16() non empty V20() finite cardinal Element of NAT

((card g) - 1) + 1 is ext-real V16() V20() set

F

f is non empty set

the Element of f is Element of f

t is epsilon-transitive epsilon-connected ordinal natural ext-real non negative V16() V20() finite cardinal Element of NAT

F

f is epsilon-transitive epsilon-connected ordinal natural ext-real non negative V16() V20() finite cardinal Element of NAT

F

m is epsilon-transitive epsilon-connected ordinal natural ext-real non negative V16() V20() finite cardinal Element of NAT

F

B is non empty Tree-like () set

g is Relation-like NAT -defined NAT -valued Function-like finite FinSequence-like FinSubsequence-like Element of B

succ g is finite Element of bool B

bool B is non empty set

{ (g ^ <*b

card (succ g) is epsilon-transitive epsilon-connected ordinal natural ext-real non negative V16() V20() finite cardinal Element of NAT

f is set

m is epsilon-transitive epsilon-connected ordinal natural ext-real non negative V16() V20() finite cardinal Element of NAT

<*m*> is Relation-like NAT -defined NAT -valued non empty trivial Function-like constant finite 1 -element FinSequence-like FinSubsequence-like FinSequence of NAT

g ^ <*m*> is Relation-like NAT -defined NAT -valued non empty Function-like finite FinSequence-like FinSubsequence-like FinSequence of NAT

m is epsilon-transitive epsilon-connected ordinal natural ext-real non negative V16() V20() finite cardinal Element of NAT

f is epsilon-transitive epsilon-connected ordinal natural ext-real non negative V16() V20() finite cardinal Element of NAT

<*m*> is Relation-like NAT -defined NAT -valued non empty trivial Function-like constant finite 1 -element FinSequence-like FinSubsequence-like FinSequence of NAT

g ^ <*m*> is Relation-like NAT -defined NAT -valued non empty Function-like finite FinSequence-like FinSubsequence-like FinSequence of NAT

<*f*> is Relation-like NAT -defined NAT -valued non empty trivial Function-like constant finite 1 -element FinSequence-like FinSubsequence-like FinSequence of NAT

g ^ <*f*> is Relation-like NAT -defined NAT -valued non empty Function-like finite FinSequence-like FinSubsequence-like FinSequence of NAT

f is epsilon-transitive epsilon-connected ordinal natural ext-real non negative V16() V20() finite cardinal Element of NAT

<*f*> is Relation-like NAT -defined NAT -valued non empty trivial Function-like constant finite 1 -element FinSequence-like FinSubsequence-like FinSequence of NAT

g ^ <*f*> is Relation-like NAT -defined NAT -valued non empty Function-like finite FinSequence-like FinSubsequence-like FinSequence of NAT

m is epsilon-transitive epsilon-connected ordinal natural ext-real non negative V16() V20() finite cardinal Element of NAT

<*m*> is Relation-like NAT -defined NAT -valued non empty trivial Function-like constant finite 1 -element FinSequence-like FinSubsequence-like FinSequence of NAT

g ^ <*m*> is Relation-like NAT -defined NAT -valued non empty Function-like finite FinSequence-like FinSubsequence-like FinSequence of NAT

len g is epsilon-transitive epsilon-connected ordinal natural ext-real non negative V16() V20() finite cardinal Element of NAT

(len g) + 1 is epsilon-transitive epsilon-connected ordinal natural ext-real positive non negative V16() non empty V20() finite cardinal Element of NAT

(g ^ <*m*>) . ((len g) + 1) is set

B is non empty Tree-like () set

g is Relation-like NAT -defined NAT -valued Function-like finite FinSequence-like FinSubsequence-like Element of B

succ g is finite Element of bool B

bool B is non empty set

{ (g ^ <*b

card (succ g) is epsilon-transitive epsilon-connected ordinal natural ext-real non negative V16() V20() finite cardinal Element of NAT

f is Relation-like NAT -defined Function-like finite FinSequence-like FinSubsequence-like set

len f is epsilon-transitive epsilon-connected ordinal natural ext-real non negative V16() V20() finite cardinal Element of NAT

dom f is finite Element of bool NAT

m is set

proj1 f is finite set

t is set

f . m is set

f . t is set

fk is epsilon-transitive epsilon-connected ordinal natural ext-real non negative V16() V20() finite cardinal Element of NAT

fk - 1 is ext-real V16() V20() set

<*(fk - 1)*> is Relation-like NAT -defined non empty trivial Function-like constant finite 1 -element FinSequence-like FinSubsequence-like set

g ^ <*(fk - 1)*> is Relation-like NAT -defined non empty Function-like finite FinSequence-like FinSubsequence-like set

len g is epsilon-transitive epsilon-connected ordinal natural ext-real non negative V16() V20() finite cardinal Element of NAT

(len g) + 1 is epsilon-transitive epsilon-connected ordinal natural ext-real positive non negative V16() non empty V20() finite cardinal Element of NAT

(g ^ <*(fk - 1)*>) . ((len g) + 1) is set

fm is epsilon-transitive epsilon-connected ordinal natural ext-real non negative V16() V20() finite cardinal Element of NAT

fm - 1 is ext-real V16() V20() set

<*(fm - 1)*> is Relation-like NAT -defined non empty trivial Function-like constant finite 1 -element FinSequence-like FinSubsequence-like set

g ^ <*(fm - 1)*> is Relation-like NAT -defined non empty Function-like finite FinSequence-like FinSubsequence-like set

(g ^ <*(fm - 1)*>) . ((len g) + 1) is set

m is epsilon-transitive epsilon-connected ordinal natural ext-real non negative V16() V20() finite cardinal Element of NAT

m + 1 is epsilon-transitive epsilon-connected ordinal natural ext-real positive non negative V16() non empty V20() finite cardinal Element of NAT

f . (m + 1) is set

<*m*> is Relation-like NAT -defined NAT -valued non empty trivial Function-like constant finite 1 -element FinSequence-like FinSubsequence-like FinSequence of NAT

g ^ <*m*> is Relation-like NAT -defined NAT -valued non empty Function-like finite FinSequence-like FinSubsequence-like FinSequence of NAT

(m + 1) - 1 is ext-real V16() V20() set

<*((m + 1) - 1)*> is Relation-like NAT -defined non empty trivial Function-like constant finite 1 -element FinSequence-like FinSubsequence-like set

g ^ <*((m + 1) - 1)*> is Relation-like NAT -defined non empty Function-like finite FinSequence-like FinSubsequence-like set

proj2 f is finite set

m is set

t is epsilon-transitive epsilon-connected ordinal natural ext-real non negative V16() V20() finite cardinal Element of NAT

t + 1 is epsilon-transitive epsilon-connected ordinal natural ext-real positive non negative V16() non empty V20() finite cardinal Element of NAT

f . (t + 1) is set

<*t*> is Relation-like NAT -defined NAT -valued non empty trivial Function-like constant finite 1 -element FinSequence-like FinSubsequence-like FinSequence of NAT

g ^ <*t*> is Relation-like NAT -defined NAT -valued non empty Function-like finite FinSequence-like FinSubsequence-like FinSequence of NAT

m is Relation-like NAT -defined B -valued Function-like one-to-one finite FinSequence-like FinSubsequence-like FinSequence of succ g

len m is epsilon-transitive epsilon-connected ordinal natural ext-real non negative V16() V20() finite cardinal Element of NAT

rng m is finite Element of bool B

t is set

fk is epsilon-transitive epsilon-connected ordinal natural ext-real non negative V16() V20() finite cardinal Element of NAT

<*fk*> is Relation-like NAT -defined NAT -valued non empty trivial Function-like constant finite 1 -element FinSequence-like FinSubsequence-like FinSequence of NAT

g ^ <*fk*> is Relation-like NAT -defined NAT -valued non empty Function-like finite FinSequence-like FinSubsequence-like FinSequence of NAT

fk + 1 is epsilon-transitive epsilon-connected ordinal natural ext-real positive non negative V16() non empty V20() finite cardinal Element of NAT

m . (fk + 1) is set

t is epsilon-transitive epsilon-connected ordinal natural ext-real non negative V16() V20() finite cardinal Element of NAT

t + 1 is epsilon-transitive epsilon-connected ordinal natural ext-real positive non negative V16() non empty V20() finite cardinal Element of NAT

m . (t + 1) is set

<*t*> is Relation-like NAT -defined NAT -valued non empty trivial Function-like constant finite 1 -element FinSequence-like FinSubsequence-like FinSequence of NAT

g ^ <*t*> is Relation-like NAT -defined NAT -valued non empty Function-like finite FinSequence-like FinSubsequence-like FinSequence of NAT

f is Relation-like NAT -defined B -valued Function-like one-to-one finite FinSequence-like FinSubsequence-like FinSequence of B

len f is epsilon-transitive epsilon-connected ordinal natural ext-real non negative V16() V20() finite cardinal Element of NAT

rng f is finite Element of bool B

m is Relation-like NAT -defined B -valued Function-like one-to-one finite FinSequence-like FinSubsequence-like FinSequence of B

len m is epsilon-transitive epsilon-connected ordinal natural ext-real non negative V16() V20() finite cardinal Element of NAT

rng m is finite Element of bool B

dom f is finite Element of bool NAT

Seg (card (succ g)) is finite card (succ g) -element Element of bool NAT

t is epsilon-transitive epsilon-connected ordinal natural ext-real non negative V16() V20() finite cardinal set

fk is epsilon-transitive epsilon-connected ordinal natural ext-real non negative V16() V20() finite cardinal Element of NAT

fk + 1 is epsilon-transitive epsilon-connected ordinal natural ext-real positive non negative V16() non empty V20() finite cardinal Element of NAT

f . t is set

<*fk*> is Relation-like NAT -defined NAT -valued non empty trivial Function-like constant finite 1 -element FinSequence-like FinSubsequence-like FinSequence of NAT

g ^ <*fk*> is Relation-like NAT -defined NAT -valued non empty Function-like finite FinSequence-like FinSubsequence-like FinSequence of NAT

m . t is set

dom m is finite Element of bool NAT

g is Relation-like NAT -defined Function-like finite FinSequence-like FinSubsequence-like set

B is Relation-like Function-like DecoratedTree-like () set

proj1 B is non empty Tree-like () set

f is Relation-like NAT -defined NAT -valued Function-like finite FinSequence-like FinSubsequence-like Element of proj1 B

((proj1 B),f) is Relation-like NAT -defined proj1 B -valued Function-like one-to-one finite FinSequence-like FinSubsequence-like FinSequence of proj1 B

rng ((proj1 B),f) is finite Element of bool (proj1 B)

bool (proj1 B) is non empty set

((proj1 B),f) * B is Relation-like NAT -defined Function-like finite set

dom (((proj1 B),f) * B) is finite Element of bool NAT

dom ((proj1 B),f) is finite Element of bool NAT

len ((proj1 B),f) is epsilon-transitive epsilon-connected ordinal natural ext-real non negative V16() V20() finite cardinal Element of NAT

Seg (len ((proj1 B),f)) is finite len ((proj1 B),f) -element Element of bool NAT

t is Relation-like NAT -defined NAT -valued Function-like finite FinSequence-like FinSubsequence-like Element of proj1 B

f is Relation-like NAT -defined Function-like finite FinSequence-like FinSubsequence-like set

((proj1 B),t) is Relation-like NAT -defined proj1 B -valued Function-like one-to-one finite FinSequence-like FinSubsequence-like FinSequence of proj1 B

((proj1 B),t) * B is Relation-like NAT -defined Function-like finite set

fk is Relation-like NAT -defined NAT -valued Function-like finite FinSequence-like FinSubsequence-like Element of proj1 B

m is Relation-like NAT -defined Function-like finite FinSequence-like FinSubsequence-like set

((proj1 B),fk) is Relation-like NAT -defined proj1 B -valued Function-like one-to-one finite FinSequence-like FinSubsequence-like FinSequence of proj1 B

((proj1 B),fk) * B is Relation-like NAT -defined Function-like finite set

B is Relation-like Function-like DecoratedTree-like () set

B . {} is set

proj1 B is non empty Tree-like () set

(proj1 B) -level 1 is Level of proj1 B

{ b

g is Relation-like NAT -defined NAT -valued Function-like finite FinSequence-like FinSubsequence-like Element of proj1 B

succ g is finite Element of bool (proj1 B)

bool (proj1 B) is non empty set

{ (g ^ <*b

f is finite set

card f is epsilon-transitive epsilon-connected ordinal natural ext-real non negative V16() V20() finite cardinal Element of NAT

Seg (card f) is finite card f -element Element of bool NAT

t is set

fk is epsilon-transitive epsilon-connected ordinal natural ext-real non negative V16() V20() finite cardinal Element of NAT

fm is epsilon-transitive epsilon-connected ordinal natural ext-real non negative V16() V20() finite cardinal set

1 + fm is epsilon-transitive epsilon-connected ordinal natural ext-real positive non negative V16() non empty V20() finite cardinal Element of NAT

n is epsilon-transitive epsilon-connected ordinal natural ext-real non negative V16() V20() finite cardinal Element of NAT

<*n*> is Relation-like NAT -defined NAT -valued non empty trivial Function-like constant finite 1 -element FinSequence-like FinSubsequence-like FinSequence of NAT

B | <*n*> is Relation-like Function-like DecoratedTree-like set

t9 is set

n + 1 is epsilon-transitive epsilon-connected ordinal natural ext-real positive non negative V16() non empty V20() finite cardinal Element of NAT

t is Relation-like Function-like set

proj1 t is set

fk is Relation-like NAT -defined Function-like finite FinSequence-like FinSubsequence-like set

len fk is epsilon-transitive epsilon-connected ordinal natural ext-real non negative V16() V20() finite cardinal Element of NAT

fm is set

dom fk is finite Element of bool NAT

fk . fm is set

n is epsilon-transitive epsilon-connected ordinal natural ext-real non negative V16() V20() finite cardinal Element of NAT

n + 1 is epsilon-transitive epsilon-connected ordinal natural ext-real positive non negative V16() non empty V20() finite cardinal Element of NAT

<*n*> is Relation-like NAT -defined NAT -valued non empty trivial Function-like constant finite 1 -element FinSequence-like FinSubsequence-like FinSequence of NAT

B | <*n*> is Relation-like Function-like DecoratedTree-like set

m is Relation-like NAT -defined NAT -valued Function-like finite FinSequence-like FinSubsequence-like Element of proj1 B

fm is epsilon-transitive epsilon-connected ordinal natural ext-real non negative V16() V20() finite cardinal Element of NAT

<*fm*> is Relation-like NAT -defined NAT -valued non empty trivial Function-like constant finite 1 -element FinSequence-like FinSubsequence-like FinSequence of NAT

m ^ <*fm*> is Relation-like NAT -defined NAT -valued non empty Function-like finite FinSequence-like FinSubsequence-like FinSequence of NAT

succ m is finite Element of bool (proj1 B)

{ (m ^ <*b

fm is Relation-like NAT -defined Function-like finite FinSequence-like FinSubsequence-like DTree-yielding set

doms fm is Relation-like NAT -defined Function-like finite FinSequence-like FinSubsequence-like Tree-yielding set

len (doms fm) is epsilon-transitive epsilon-connected ordinal natural ext-real non negative V16() V20() finite cardinal Element of NAT

len fm is epsilon-transitive epsilon-connected ordinal natural ext-real non negative V16() V20() finite cardinal Element of NAT

n is set

t9 is Relation-like NAT -defined NAT -valued Function-like finite FinSequence-like FinSubsequence-like Element of proj1 B

n is epsilon-transitive epsilon-connected ordinal natural ext-real non negative V16() V20() finite cardinal Element of NAT

<*n*> is Relation-like NAT -defined NAT -valued non empty trivial Function-like constant finite 1 -element FinSequence-like FinSubsequence-like FinSequence of NAT

n is Relation-like NAT -defined NAT -valued Function-like finite FinSequence-like FinSubsequence-like FinSequence of NAT

<*n*> ^ n is Relation-like NAT -defined NAT -valued non empty Function-like finite FinSequence-like FinSubsequence-like FinSequence of NAT

c

q is epsilon-transitive epsilon-connected ordinal natural ext-real non negative V16() V20() finite cardinal Element of NAT

<*q*> is Relation-like NAT -defined NAT -valued non empty trivial Function-like constant finite 1 -element FinSequence-like FinSubsequence-like FinSequence of NAT

m ^ <*q*> is Relation-like NAT -defined NAT -valued non empty Function-like finite FinSequence-like FinSubsequence-like FinSequence of NAT

q + 1 is epsilon-transitive epsilon-connected ordinal natural ext-real positive non negative V16() non empty V20() finite cardinal Element of NAT

dom fm is finite Element of bool NAT

fm . (q + 1) is set

(doms fm) . (q + 1) is set

B | <*q*> is Relation-like Function-like DecoratedTree-like set

proj1 (B | <*q*>) is non empty Tree-like set

(proj1 B) | <*q*> is non empty Tree-like set

c

c

<*c

B | <*c

q is Relation-like NAT -defined Function-like finite FinSequence-like FinSubsequence-like set

<*q*> ^ q is Relation-like NAT -defined non empty Function-like finite FinSequence-like FinSubsequence-like set

t9 is epsilon-transitive epsilon-connected ordinal natural ext-real non negative V16() V20() finite cardinal Element of NAT

n is Relation-like NAT -defined Function-like finite FinSequence-like FinSubsequence-like set

t9 + 1 is epsilon-transitive epsilon-connected ordinal natural ext-real positive non negative V16() non empty V20() finite cardinal Element of NAT

(doms fm) . (t9 + 1) is set

<*t9*> is Relation-like NAT -defined NAT -valued non empty trivial Function-like constant finite 1 -element FinSequence-like FinSubsequence-like FinSequence of NAT

<*t9*> ^ n is Relation-like NAT -defined non empty Function-like finite FinSequence-like FinSubsequence-like set

t9 is epsilon-transitive epsilon-connected ordinal natural ext-real non negative V16() V20() finite cardinal Element of NAT

n is Relation-like NAT -defined Function-like finite FinSequence-like FinSubsequence-like set

t9 + 1 is epsilon-transitive epsilon-connected ordinal natural ext-real positive non negative V16() non empty V20() finite cardinal Element of NAT

(doms fm) . (t9 + 1) is set

<*t9*> is Relation-like NAT -defined NAT -valued non empty trivial Function-like constant finite 1 -element FinSequence-like FinSubsequence-like FinSequence of NAT

<*t9*> ^ n is Relation-like NAT -defined non empty Function-like finite FinSequence-like FinSubsequence-like set

fm . (t9 + 1) is set

B | <*t9*> is Relation-like Function-like DecoratedTree-like set

proj1 (B | <*t9*>) is non empty Tree-like set

(proj1 B) | <*t9*> is non empty Tree-like set

n is epsilon-transitive epsilon-connected ordinal natural ext-real non negative V16() V20() finite cardinal Element of NAT

n + 1 is epsilon-transitive epsilon-connected ordinal natural ext-real positive non negative V16() non empty V20() finite cardinal Element of NAT

<*n*> is Relation-like NAT -defined NAT -valued non empty trivial Function-like constant finite 1 -element FinSequence-like FinSubsequence-like FinSequence of NAT

B | <*n*> is Relation-like Function-like DecoratedTree-like set

n is Relation-like NAT -defined NAT -valued Function-like finite FinSequence-like FinSubsequence-like Element of (proj1 B) | <*t9*>

<*t9*> ^ n is Relation-like NAT -defined NAT -valued non empty Function-like finite FinSequence-like FinSubsequence-like FinSequence of NAT

tree (doms fm) is non empty Tree-like set

(B . {}) -tree fm is Relation-like Function-like DecoratedTree-like set

n is epsilon-transitive epsilon-connected ordinal natural ext-real non negative V16() V20() finite cardinal Element of NAT

n + 1 is epsilon-transitive epsilon-connected ordinal natural ext-real positive non negative V16() non empty V20() finite cardinal Element of NAT

fm . (n + 1) is set

<*n*> is Relation-like NAT -defined NAT -valued non empty trivial Function-like constant finite 1 -element FinSequence-like FinSubsequence-like FinSequence of NAT

B | <*n*> is Relation-like Function-like DecoratedTree-like set

t9 is epsilon-transitive epsilon-connected ordinal natural ext-real non negative V16() V20() finite cardinal Element of NAT

t9 + 1 is epsilon-transitive epsilon-connected ordinal natural ext-real positive non negative V16() non empty V20() finite cardinal Element of NAT

<*t9*> is Relation-like NAT -defined NAT -valued non empty trivial Function-like constant finite 1 -element FinSequence-like FinSubsequence-like FinSequence of NAT

B | <*t9*> is Relation-like Function-like DecoratedTree-like set

B is Relation-like Function-like finite DecoratedTree-like () () set

proj1 B is non empty finite Tree-like finite-order () set

g is Relation-like NAT -defined NAT -valued Function-like finite FinSequence-like FinSubsequence-like Element of proj1 B

B | g is Relation-like Function-like finite DecoratedTree-like () () set

B is non empty finite Tree-like finite-order () set

g is Relation-like NAT -defined NAT -valued Function-like finite FinSequence-like FinSubsequence-like Element of B

B | g is non empty finite Tree-like finite-order () set

height B is epsilon-transitive epsilon-connected ordinal natural ext-real non negative V16() V20() finite cardinal Element of NAT

height (B | g) is epsilon-transitive epsilon-connected ordinal natural ext-real non negative V16() V20() finite cardinal Element of NAT

B is non empty set

FinTrees B is non empty functional constituted-DTrees DTree-set of B

bool (FinTrees B) is non empty set

g is non empty functional constituted-DTrees Element of bool (FinTrees B)

f is Relation-like B -valued Function-like DecoratedTree-like (B, FinTrees B,g)

B is Relation-like Function-like DecoratedTree-like set

proj1 B is non empty Tree-like set

{ (B | b

B is Relation-like Function-like DecoratedTree-like set

(B) is set

proj1 B is non empty Tree-like set

{ (B | b

the Relation-like NAT -defined NAT -valued Function-like finite FinSequence-like FinSubsequence-like Element of proj1 B is Relation-like NAT -defined NAT -valued Function-like finite FinSequence-like FinSubsequence-like Element of proj1 B

B | the Relation-like NAT -defined NAT -valued Function-like finite FinSequence-like FinSubsequence-like Element of proj1 B is Relation-like Function-like DecoratedTree-like set

m is non empty set

t is set

fk is Relation-like NAT -defined NAT -valued Function-like finite FinSequence-like FinSubsequence-like Element of proj1 B

B | fk is Relation-like Function-like DecoratedTree-like set

B is non empty set

g is Relation-like B -valued Function-like DecoratedTree-like set

(g) is non empty functional constituted-DTrees set

proj1 g is non empty Tree-like set

{ (g | b

Trees B is non empty functional constituted-DTrees DTree-set of B

bool (Trees B) is non empty set

f is set

m is Relation-like NAT -defined NAT -valued Function-like finite FinSequence-like FinSubsequence-like Element of proj1 g

g | m is Relation-like B -valued Function-like DecoratedTree-like set

B is non empty set

g is Relation-like B -valued Function-like finite DecoratedTree-like () () set

(g) is non empty functional constituted-DTrees set

proj1 g is non empty finite Tree-like finite-order () set

{ (g | b

FinTrees B is non empty functional constituted-DTrees DTree-set of B

bool (FinTrees B) is non empty set

(B,g) is non empty functional constituted-DTrees Element of bool (Trees B)

Trees B is non empty functional constituted-DTrees DTree-set of B

bool (Trees B) is non empty set

f is set

t is Relation-like NAT -defined NAT -valued Function-like finite FinSequence-like FinSubsequence-like Element of proj1 g

g | t is Relation-like B -valued Function-like finite DecoratedTree-like () () set

m is Relation-like B -valued Function-like finite DecoratedTree-like () () set

proj1 m is non empty finite Tree-like finite-order () set

B is Relation-like Function-like finite DecoratedTree-like () () set

(B) is non empty functional constituted-DTrees set

proj1 B is non empty finite Tree-like finite-order () set

{ (B | b

g is Relation-like Function-like DecoratedTree-like Element of (B)

f is Relation-like NAT -defined NAT -valued Function-like finite FinSequence-like FinSubsequence-like Element of proj1 B

B | f is Relation-like Function-like finite DecoratedTree-like () () set

m is Relation-like Function-like DecoratedTree-like set

proj1 m is non empty Tree-like set

B is set

g is Relation-like Function-like DecoratedTree-like set

(g) is non empty functional constituted-DTrees set

proj1 g is non empty Tree-like set

{ (g | b

f is set

t is Relation-like NAT -defined NAT -valued Function-like finite FinSequence-like FinSubsequence-like Element of proj1 m

m | t is Relation-like Function-like DecoratedTree-like set

(m) is non empty functional constituted-DTrees set

{ (m | b

B is Relation-like Function-like DecoratedTree-like set

(B) is non empty functional constituted-DTrees set

proj1 B is non empty Tree-like set

{ (B | b

g is Relation-like NAT -defined NAT -valued Function-like finite FinSequence-like FinSubsequence-like Element of proj1 B

B | g is Relation-like Function-like DecoratedTree-like set

B is Relation-like Function-like DecoratedTree-like set

(B) is non empty functional constituted-DTrees set

proj1 B is non empty Tree-like set

{ (B | b

g is Relation-like Function-like DecoratedTree-like set

(g) is non empty functional constituted-DTrees set

proj1 g is non empty Tree-like set

{ (g | b

m is Relation-like NAT -defined NAT -valued Function-like finite FinSequence-like FinSubsequence-like Element of proj1 g

g | m is Relation-like Function-like DecoratedTree-like set

t is Relation-like NAT -defined NAT -valued Function-like finite FinSequence-like FinSubsequence-like Element of proj1 B

B | t is Relation-like Function-like DecoratedTree-like set

proj1 (B | t) is non empty Tree-like set

(proj1 B) | t is non empty Tree-like set

f is Relation-like Function-like finite DecoratedTree-like () () set

proj1 f is non empty finite Tree-like finite-order () set

t ^ m is Relation-like NAT -defined NAT -valued Function-like finite FinSequence-like FinSubsequence-like FinSequence of NAT

fk is Relation-like NAT -defined NAT -valued Function-like finite FinSequence-like FinSubsequence-like Element of proj1 f

f | fk is Relation-like Function-like finite DecoratedTree-like () () set

(proj1 f) | fk is non empty finite Tree-like finite-order () set

B is Relation-like Function-like DecoratedTree-like set

proj1 B is non empty Tree-like set

(B) is non empty functional constituted-DTrees set

{ (B | b

g is Relation-like NAT -defined NAT -valued Function-like finite FinSequence-like FinSubsequence-like Element of proj1 B

B | g is Relation-like Function-like DecoratedTree-like set

((B | g)) is non empty functional constituted-DTrees set

proj1 (B | g) is non empty Tree-like set

{ ((B | g) | b

f is set

m is Relation-like NAT -defined NAT -valued Function-like finite FinSequence-like FinSubsequence-like Element of proj1 (B | g)

(B | g) | m is Relation-like Function-like DecoratedTree-like set

(proj1 B) | g is non empty Tree-like set

g ^ m is Relation-like NAT -defined NAT -valued Function-like finite FinSequence-like FinSubsequence-like FinSequence of NAT

t is Relation-like NAT -defined NAT -valued Function-like finite FinSequence-like FinSubsequence-like Element of proj1 B

B | t is Relation-like Function-like DecoratedTree-like set

B is Relation-like Function-like DecoratedTree-like set

proj1 B is non empty Tree-like set

{ [b

(B) is non empty functional constituted-DTrees set

{ (B | b

[:(proj1 B),(B):] is Relation-like non empty set

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

f is set

m is Relation-like NAT -defined NAT -valued Function-like finite FinSequence-like FinSubsequence-like Element of proj1 B

B | m is Relation-like Function-like DecoratedTree-like set

[m,(B | m)] is non empty V27() set

{m,(B | m)} is non empty functional finite set

{m} is non empty trivial functional finite V37() 1 -element set

{{m,(B | m)},{m}} is non empty finite V37() set

B is Relation-like Function-like DecoratedTree-like set

(B) is Relation-like proj1 B -defined (B) -valued Element of bool [:(proj1 B),(B):]

proj1 B is non empty Tree-like set

(B) is non empty functional constituted-DTrees set

{ (B | b

[:(proj1 B),(B):] is Relation-like non empty set

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

{ [b

the Relation-like NAT -defined NAT -valued Function-like finite FinSequence-like FinSubsequence-like Element of proj1 B is Relation-like NAT -defined NAT -valued Function-like finite FinSequence-like FinSubsequence-like Element of proj1 B

B | the Relation-like NAT -defined NAT -valued Function-like finite FinSequence-like FinSubsequence-like Element of proj1 B is Relation-like Function-like DecoratedTree-like set

[ the Relation-like NAT -defined NAT -valued Function-like finite FinSequence-like FinSubsequence-like Element of proj1 B,(B | the Relation-like NAT -defined NAT -valued Function-like finite FinSequence-like FinSubsequence-like Element of proj1 B)] is non empty V27() set

{ the Relation-like NAT -defined NAT -valued Function-like finite FinSequence-like FinSubsequence-like Element of proj1 B,(B | the Relation-like NAT -defined NAT -valued Function-like finite FinSequence-like FinSubsequence-like Element of proj1 B)} is non empty functional finite set

{ the Relation-like NAT -defined NAT -valued Function-like finite FinSequence-like FinSubsequence-like Element of proj1 B} is non empty trivial functional finite V37() 1 -element set

{{ the Relation-like NAT -defined NAT -valued Function-like finite FinSequence-like FinSubsequence-like Element of proj1 B,(B | the Relation-like NAT -defined NAT -valued Function-like finite FinSequence-like FinSubsequence-like Element of proj1 B)},{ the Relation-like NAT -defined NAT -valued Function-like finite FinSequence-like FinSubsequence-like Element of proj1 B}} is non empty finite V37() set

m is Relation-like Function-like DecoratedTree-like set

proj1 m is non empty Tree-like set

B is set

g is Relation-like Function-like DecoratedTree-like set

(g) is Relation-like proj1 g -defined (g) -valued non empty Element of bool [:(proj1 g),(g):]

proj1 g is non empty Tree-like set

(g) is non empty functional constituted-DTrees set

{ (g | b

[:(proj1 g),(g):] is Relation-like non empty set

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

{ [b

f is set

t is Relation-like NAT -defined NAT -valued Function-like finite FinSequence-like FinSubsequence-like Element of proj1 m

m | t is Relation-like Function-like DecoratedTree-like set

[t,(m | t)] is non empty V27() set

{t,(m | t)} is non empty functional finite set

{t} is non empty trivial functional finite V37() 1 -element set

{{t,(m | t)},{t}} is non empty finite V37() set

(m) is Relation-like proj1 m -defined (m) -valued non empty Element of bool [:(proj1 m),(m):]

(m) is non empty functional constituted-DTrees set

{ (m | b

[:(proj1 m),(m):] is Relation-like non empty set

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

{ [b

B is Relation-like Function-like DecoratedTree-like set

[{},B] is non empty V27() set

{{},B} is non empty functional finite set

{{{},B},{{}}} is non empty finite V37() set

(B) is Relation-like proj1 B -defined (B) -valued non empty Element of bool [:(proj1 B),(B):]

proj1 B is non empty Tree-like set

(B) is non empty functional constituted-DTrees set

{ (B | b

[:(proj1 B),(B):] is Relation-like non empty set

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

{ [b

g is Relation-like NAT -defined NAT -valued Function-like finite FinSequence-like FinSubsequence-like Element of proj1 B

B | g is Relation-like Function-like DecoratedTree-like set

B is Relation-like Function-like DecoratedTree-like set

(B) is Relation-like proj1 B -defined (B) -valued non empty Element of bool [:(proj1 B),(B):]

proj1 B is non empty Tree-like set

(B) is non empty functional constituted-DTrees set

{ (B | b

[:(proj1 B),(B):] is Relation-like non empty set

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

{ [b

g is Relation-like Function-like DecoratedTree-like set

(g) is Relation-like proj1 g -defined (g) -valued non empty Element of bool [:(proj1 g),(g):]

proj1 g is non empty Tree-like set

(g) is non empty functional constituted-DTrees set

{ (g | b

[:(proj1 g),(g):] is Relation-like non empty set

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

{ [b

[{},B] is non empty V27() set

{{},B} is non empty functional finite set

{{{},B},{{}}} is non empty finite V37() set

f is Relation-like NAT -defined NAT -valued Function-like finite FinSequence-like FinSubsequence-like Element of proj1 g

g | f is Relation-like Function-like DecoratedTree-like set

[f,(g | f)] is non empty V27() set

{f,(g | f)} is non empty functional finite set

{f} is non empty trivial functional finite V37() 1 -element set

{{f,(g | f)},{f}} is non empty finite V37() set

B is Relation-like Function-like DecoratedTree-like set

proj1 B is non empty Tree-like set

Leaves (proj1 B) is Element of bool (proj1 B)

bool (proj1 B) is non empty set

g is set

{ (B | b

(B) is non empty functional constituted-DTrees set

{ (B | b

bool (B) is non empty set

m is set

t is Relation-like NAT -defined NAT -valued Function-like finite FinSequence-like FinSubsequence-like Element of proj1 B

B | t is Relation-like Function-like DecoratedTree-like set

B . t is set

t is Relation-like Function-like DecoratedTree-like set

proj1 t is non empty Tree-like set

B is set

g is Relation-like Function-like DecoratedTree-like set

f is set

(g,f) is functional constituted-DTrees Element of bool (g)

(g) is non empty functional constituted-DTrees set

proj1 g is non empty Tree-like set

{ (g | b

bool (g) is non empty set

Leaves (proj1 g) is Element of bool (proj1 g)

bool (proj1 g) is non empty set

{ (g | b

m is set

fm is Relation-like NAT -defined NAT -valued Function-like finite FinSequence-like FinSubsequence-like Element of proj1 t

t | fm is Relation-like Function-like DecoratedTree-like set

Leaves (proj1 t) is Element of bool (proj1 t)

bool (proj1 t) is non empty set

t . fm is set

fk is set

(t,fk) is functional constituted-DTrees Element of bool (t)

(t) is non empty functional constituted-DTrees set

{ (t | b

bool (t) is non empty set

{ (t | b

B is Relation-like Function-like DecoratedTree-like set

B . {} is set

g is set

(B,g) is functional constituted-DTrees Element of bool (B)

(B) is non empty functional constituted-DTrees set

proj1 B is non empty Tree-like set

{ (B | b

bool (B) is non empty set

Leaves (proj1 B) is Element of bool (proj1 B)

bool (proj1 B) is non empty set

{ (B | b

f is Relation-like NAT -defined NAT -valued Function-like finite FinSequence-like FinSubsequence-like Element of proj1 B

B | f is Relation-like Function-like DecoratedTree-like set

m is non empty functional constituted-DTrees Element of bool (B)

the Relation-like Function-like DecoratedTree-like Element of m is Relation-like Function-like DecoratedTree-like Element of m

fk is Relation-like NAT -defined NAT -valued Function-like finite FinSequence-like FinSubsequence-like Element of proj1 B

B | fk is Relation-like Function-like DecoratedTree-like set

B . fk is set

f ^ <*0*> is Relation-like NAT -defined NAT -valued non empty Function-like finite FinSequence-like FinSubsequence-like FinSequence of NAT

B is Relation-like Function-like finite DecoratedTree-like () () set

g is set

(B,g) is functional constituted-DTrees Element of bool (B)

(B) is non empty functional constituted-DTrees set

proj1 B is non empty finite Tree-like finite-order () set

{ (B | b

bool (B) is non empty set

Leaves (proj1 B) is non empty finite Element of bool (proj1 B)

bool (proj1 B) is non empty finite V37() set

{ (B | b

(B) * is non empty functional FinSequence-membered M8((B))

[:(B,g),((B) *):] is Relation-like set

bool [:(B,g),((B) *):] is non empty set

f is set

m is Relation-like Function-like finite DecoratedTree-like () () Element of (B)

fk is Relation-like NAT -defined NAT -valued Function-like finite FinSequence-like FinSubsequence-like Element of proj1 B

B | fk is Relation-like Function-like finite DecoratedTree-like () () set

fm is set

n is Relation-like NAT -defined Function-like finite FinSequence-like FinSubsequence-like DTree-yielding set

fm -tree n is Relation-like Function-like DecoratedTree-like set

proj2 n is finite set

t9 is set

proj1 (B | fk) is non empty finite Tree-like finite-order () set

(proj1 B) | fk is non empty finite Tree-like finite-order () set

len n is epsilon-transitive epsilon-connected ordinal natural ext-real non negative V16() V20() finite cardinal Element of NAT

n is epsilon-transitive epsilon-connected ordinal natural ext-real non negative V16() V20() finite cardinal Element of NAT

n + 1 is epsilon-transitive epsilon-connected ordinal natural ext-real positive non negative V16() non empty V20() finite cardinal Element of NAT

n . (n + 1) is set

<*n*> is Relation-like NAT -defined NAT -valued non empty trivial Function-like constant finite 1 -element FinSequence-like FinSubsequence-like FinSequence of NAT

m | <*n*> is Relation-like Function-like DecoratedTree-like set

proj1 (m | <*n*>) is non empty Tree-like set

n is Relation-like NAT -defined NAT -valued Function-like finite FinSequence-like FinSubsequence-like Element of proj1 (m | <*n*>)

<*n*> ^ n is Relation-like NAT -defined NAT -valued non empty Function-like finite FinSequence-like FinSubsequence-like FinSequence of NAT

proj1 m is non empty finite Tree-like finite-order () set

fk ^ <*n*> is Relation-like NAT -defined NAT -valued non empty Function-like finite FinSequence-like FinSubsequence-like FinSequence of NAT

c

B | c

t9 is Relation-like NAT -defined (B) -valued Function-like finite FinSequence-like FinSubsequence-like DTree-yielding FinSequence of (B)

n is set

t is Relation-like Function-like DecoratedTree-like set

t . {} is set

(t . {}) -tree t9 is Relation-like Function-like DecoratedTree-like set

f is Relation-like Function-like set

proj1 f is set

proj2 f is set

m is Relation-like (B,g) -defined (B) * -valued Function-like V30((B,g),(B) * ) Element of bool [:(B,g),((B) *):]

t is Relation-like Function-like DecoratedTree-like set

m . t is Relation-like NAT -defined Function-like finite FinSequence-like FinSubsequence-like set

t . {} is set

fk is Relation-like NAT -defined (B) -valued Function-like finite FinSequence-like FinSubsequence-like DTree-yielding FinSequence of (B)

(t . {}) -tree fk is Relation-like Function-like DecoratedTree-like set

n is Relation-like NAT -defined (B) -valued Function-like finite FinSequence-like FinSubsequence-like DTree-yielding FinSequence of (B)

fm is Relation-like Function-like DecoratedTree-like set

fm . {} is set

(fm . {}) -tree n is Relation-like Function-like DecoratedTree-like set

f is Relation-like (B,g) -defined (B) * -valued Function-like V30((B,g),(B) * ) Element of bool [:(B,g),((B) *):]

m is Relation-like (B,g) -defined (B) * -valued Function-like V30((B,g),(B) * ) Element of bool [:(B,g),((B) *):]

t is set

fk is Relation-like Function-like finite DecoratedTree-like () () Element of (B)

f . fk is Relation-like NAT -defined Function-like finite FinSequence-like FinSubsequence-like set

m . fk is Relation-like NAT -defined Function-like finite FinSequence-like FinSubsequence-like set

fk . {} is set

fm is Relation-like NAT -defined (B) -valued Function-like finite FinSequence-like FinSubsequence-like DTree-yielding Element of (B) *

(fk . {}) -tree fm is Relation-like Function-like DecoratedTree-like set

n is Relation-like NAT -defined (B) -valued Function-like finite FinSequence-like FinSubsequence-like DTree-yielding Element of (B) *

(fk . {}) -tree n is Relation-like Function-like DecoratedTree-like set

f . t is Relation-like NAT -defined Function-like finite FinSequence-like FinSubsequence-like set

m . t is Relation-like NAT -defined Function-like finite FinSequence-like FinSubsequence-like set

B is non empty functional constituted-DTrees set

{ (b