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 ^ <*b1*>) where b1 is epsilon-transitive epsilon-connected ordinal natural ext-real non negative V16() V20() finite cardinal Element of NAT : m ^ <*b1*> in B } is set
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 ^ <*b1*>) where b1 is epsilon-transitive epsilon-connected ordinal natural ext-real non negative V16() V20() finite cardinal Element of NAT : f ^ <*b1*> in B } is set
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 ^ <*b1*>) where b1 is epsilon-transitive epsilon-connected ordinal natural ext-real non negative V16() V20() finite cardinal Element of NAT : m ^ <*b1*> in g } is 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 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 ^ <*b1*>) where b1 is epsilon-transitive epsilon-connected ordinal natural ext-real non negative V16() V20() finite cardinal Element of NAT : g ^ <*b1*> in B } is set
F2() is finite set
card F2() is epsilon-transitive epsilon-connected ordinal natural ext-real non negative V16() V20() finite cardinal Element of NAT
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
F1(g) is set
g + 1 is epsilon-transitive epsilon-connected ordinal natural ext-real positive non negative V16() non empty V20() finite cardinal Element of NAT
F1((g + 1)) is set
f is Relation-like Function-like set
proj1 f is set
{ b1 where b1 is epsilon-transitive epsilon-connected ordinal natural ext-real non negative V16() V20() finite cardinal Element of NAT : not g + 1 <= b1 } is set
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
F1(fk) is set
m is set
t is epsilon-transitive epsilon-connected ordinal natural ext-real non negative V16() V20() finite cardinal Element of NAT
F1(t) is set
f . t is set
m is set
t is set
f . m is set
f . t is set
F1(m) is set
F1(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 Element of NAT
{ b1 where b1 is epsilon-transitive epsilon-connected ordinal natural ext-real non negative V16() V20() finite cardinal Element of NAT : not card F2() <= b1 } is set
g is set
f is set
B . g is set
B . f is set
F1(g) is set
F1(f) is set
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 F2()) 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
F1(f) is set
F1((card F2())) is set
{F1((card F2()))} is non empty trivial finite 1 -element set
F2() \ {F1((card F2()))} is finite Element of bool F2()
bool F2() is non empty finite V37() set
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
F1(fk) is set
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 (F2() \ {F1((card F2()))}) is epsilon-transitive epsilon-connected ordinal natural ext-real non negative V16() V20() finite cardinal Element of NAT
card {F1((card F2()))} is epsilon-transitive epsilon-connected ordinal natural ext-real non negative V16() non empty V20() finite cardinal Element of NAT
(card F2()) - (card {F1((card F2()))}) is ext-real V16() V20() set
(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
F1(0) is set
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
F1(t) is set
f is epsilon-transitive epsilon-connected ordinal natural ext-real non negative V16() V20() finite cardinal Element of NAT
F1(f) is set
m is epsilon-transitive epsilon-connected ordinal natural ext-real non negative V16() V20() finite cardinal Element of NAT
F1(m) 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 ^ <*b1*>) where b1 is epsilon-transitive epsilon-connected ordinal natural ext-real non negative V16() V20() finite cardinal Element of NAT : g ^ <*b1*> in B } is set
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 ^ <*b1*>) where b1 is epsilon-transitive epsilon-connected ordinal natural ext-real non negative V16() V20() finite cardinal Element of NAT : g ^ <*b1*> in B } is set
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
{ b1 where b1 is Relation-like NAT -defined NAT -valued Function-like finite FinSequence-like FinSubsequence-like Element of proj1 B : len b1 = 1 } is set
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 ^ <*b1*>) where b1 is epsilon-transitive epsilon-connected ordinal natural ext-real non negative V16() V20() finite cardinal Element of NAT : g ^ <*b1*> in proj1 B } is set
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 ^ <*b1*>) where b1 is epsilon-transitive epsilon-connected ordinal natural ext-real non negative V16() V20() finite cardinal Element of NAT : m ^ <*b1*> in proj1 B } is set
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
c12 is Relation-like NAT -defined Function-like finite FinSequence-like FinSubsequence-like set
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
c15 is epsilon-transitive epsilon-connected ordinal natural ext-real non negative V16() V20() finite cardinal Element of NAT
c15 + 1 is epsilon-transitive epsilon-connected ordinal natural ext-real positive non negative V16() non empty V20() finite cardinal Element of NAT
<*c15*> is Relation-like NAT -defined NAT -valued non empty trivial Function-like constant finite 1 -element FinSequence-like FinSubsequence-like FinSequence of NAT
B | <*c15*> is Relation-like Function-like DecoratedTree-like set
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 | b1) where b1 is Relation-like NAT -defined NAT -valued Function-like finite FinSequence-like FinSubsequence-like Element of proj1 B : verum } is set
B is Relation-like Function-like DecoratedTree-like set
(B) is set
proj1 B is non empty Tree-like set
{ (B | b1) where b1 is Relation-like NAT -defined NAT -valued Function-like finite FinSequence-like FinSubsequence-like Element of proj1 B : verum } is set
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 | b1) where b1 is Relation-like NAT -defined NAT -valued Function-like finite FinSequence-like FinSubsequence-like Element of proj1 g : verum } is set
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 | b1) where b1 is Relation-like NAT -defined NAT -valued Function-like finite FinSequence-like FinSubsequence-like Element of proj1 g : verum } is set
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 | b1) where b1 is Relation-like NAT -defined NAT -valued Function-like finite FinSequence-like FinSubsequence-like Element of proj1 B : verum } is set
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 | b1) where b1 is Relation-like NAT -defined NAT -valued Function-like finite FinSequence-like FinSubsequence-like Element of proj1 g : verum } is set
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 | b1) where b1 is Relation-like NAT -defined NAT -valued Function-like finite FinSequence-like FinSubsequence-like Element of proj1 m : verum } is 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 | b1) where b1 is Relation-like NAT -defined NAT -valued Function-like finite FinSequence-like FinSubsequence-like Element of proj1 B : verum } is 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
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 | b1) where b1 is Relation-like NAT -defined NAT -valued Function-like finite FinSequence-like FinSubsequence-like Element of proj1 B : verum } 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 | b1) where b1 is Relation-like NAT -defined NAT -valued Function-like finite FinSequence-like FinSubsequence-like Element of proj1 g : verum } 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 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 | b1) where b1 is Relation-like NAT -defined NAT -valued Function-like finite FinSequence-like FinSubsequence-like Element of proj1 B : verum } is 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
((B | g)) is non empty functional constituted-DTrees set
proj1 (B | g) is non empty Tree-like set
{ ((B | g) | b1) where b1 is Relation-like NAT -defined NAT -valued Function-like finite FinSequence-like FinSubsequence-like Element of proj1 (B | g) : verum } is set
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
{ [b1,(B | b1)] where b1 is Relation-like NAT -defined NAT -valued Function-like finite FinSequence-like FinSubsequence-like Element of proj1 B : verum } is set
(B) is non empty functional constituted-DTrees set
{ (B | b1) where b1 is Relation-like NAT -defined NAT -valued Function-like finite FinSequence-like FinSubsequence-like Element of proj1 B : verum } is set
[:(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 | b1) where b1 is Relation-like NAT -defined NAT -valued Function-like finite FinSequence-like FinSubsequence-like Element of proj1 B : verum } is set
[:(proj1 B),(B):] is Relation-like non empty set
bool [:(proj1 B),(B):] is non empty set
{ [b1,(B | b1)] where b1 is Relation-like NAT -defined NAT -valued Function-like finite FinSequence-like FinSubsequence-like Element of proj1 B : verum } is set
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 | b1) where b1 is Relation-like NAT -defined NAT -valued Function-like finite FinSequence-like FinSubsequence-like Element of proj1 g : verum } is set
[:(proj1 g),(g):] is Relation-like non empty set
bool [:(proj1 g),(g):] is non empty set
{ [b1,(g | b1)] where b1 is Relation-like NAT -defined NAT -valued Function-like finite FinSequence-like FinSubsequence-like Element of proj1 g : verum } is set
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 | b1) where b1 is Relation-like NAT -defined NAT -valued Function-like finite FinSequence-like FinSubsequence-like Element of proj1 m : verum } is set
[:(proj1 m),(m):] is Relation-like non empty set
bool [:(proj1 m),(m):] is non empty set
{ [b1,(m | b1)] where b1 is Relation-like NAT -defined NAT -valued Function-like finite FinSequence-like FinSubsequence-like Element of proj1 m : verum } is set
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 | b1) where b1 is Relation-like NAT -defined NAT -valued Function-like finite FinSequence-like FinSubsequence-like Element of proj1 B : verum } is set
[:(proj1 B),(B):] is Relation-like non empty set
bool [:(proj1 B),(B):] is non empty set
{ [b1,(B | b1)] where b1 is Relation-like NAT -defined NAT -valued Function-like finite FinSequence-like FinSubsequence-like Element of proj1 B : verum } is 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
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 | b1) where b1 is Relation-like NAT -defined NAT -valued Function-like finite FinSequence-like FinSubsequence-like Element of proj1 B : verum } is set
[:(proj1 B),(B):] is Relation-like non empty set
bool [:(proj1 B),(B):] is non empty set
{ [b1,(B | b1)] where b1 is Relation-like NAT -defined NAT -valued Function-like finite FinSequence-like FinSubsequence-like Element of proj1 B : verum } 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 | b1) where b1 is Relation-like NAT -defined NAT -valued Function-like finite FinSequence-like FinSubsequence-like Element of proj1 g : verum } is set
[:(proj1 g),(g):] is Relation-like non empty set
bool [:(proj1 g),(g):] is non empty set
{ [b1,(g | b1)] where b1 is Relation-like NAT -defined NAT -valued Function-like finite FinSequence-like FinSubsequence-like Element of proj1 g : verum } is set
[{},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 | b1) where b1 is Relation-like NAT -defined NAT -valued Function-like finite FinSequence-like FinSubsequence-like Element of proj1 B : ( not b1 in Leaves (proj1 B) or B . b1 in g ) } is set
(B) is non empty functional constituted-DTrees set
{ (B | b1) where b1 is Relation-like NAT -defined NAT -valued Function-like finite FinSequence-like FinSubsequence-like Element of proj1 B : verum } is set
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 | b1) where b1 is Relation-like NAT -defined NAT -valued Function-like finite FinSequence-like FinSubsequence-like Element of proj1 g : verum } is set
bool (g) is non empty set
Leaves (proj1 g) is Element of bool (proj1 g)
bool (proj1 g) is non empty set
{ (g | b1) where b1 is Relation-like NAT -defined NAT -valued Function-like finite FinSequence-like FinSubsequence-like Element of proj1 g : ( not b1 in Leaves (proj1 g) or g . b1 in f ) } is set
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 | b1) where b1 is Relation-like NAT -defined NAT -valued Function-like finite FinSequence-like FinSubsequence-like Element of proj1 t : verum } is set
bool (t) is non empty set
{ (t | b1) where b1 is Relation-like NAT -defined NAT -valued Function-like finite FinSequence-like FinSubsequence-like Element of proj1 t : ( not b1 in Leaves (proj1 t) or t . b1 in fk ) } is set
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 | b1) where b1 is Relation-like NAT -defined NAT -valued Function-like finite FinSequence-like FinSubsequence-like Element of proj1 B : verum } is set
bool (B) is non empty set
Leaves (proj1 B) is Element of bool (proj1 B)
bool (proj1 B) is non empty set
{ (B | b1) where b1 is Relation-like NAT -defined NAT -valued Function-like finite FinSequence-like FinSubsequence-like Element of proj1 B : ( not b1 in Leaves (proj1 B) or B . b1 in g ) } is set
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 | b1) where b1 is Relation-like NAT -defined NAT -valued Function-like finite FinSequence-like FinSubsequence-like Element of proj1 B : verum } is set
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 | b1) where b1 is Relation-like NAT -defined NAT -valued Function-like finite FinSequence-like FinSubsequence-like Element of proj1 B : ( not b1 in Leaves (proj1 B) or B . b1 in g ) } is set
(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
c12 is Relation-like NAT -defined NAT -valued Function-like finite FinSequence-like FinSubsequence-like Element of proj1 B
B | c12 is Relation-like Function-like finite DecoratedTree-like () () set
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
{ (b1 | b2) where b1 is Relation-like Function-like DecoratedTree-like Element of B, b2 is