:: 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₁*>) where b₁ is epsilon-transitive epsilon-connected ordinal natural ext-real non negative V16() V20() finite cardinal Element of NAT : m ^ <*b₁*> 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 ^ <*b₁*>) where b₁ is epsilon-transitive epsilon-connected ordinal natural ext-real non negative V16() V20() finite cardinal Element of NAT : f ^ <*b₁*> 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 ^ <*b₁*>) where b₁ is epsilon-transitive epsilon-connected ordinal natural ext-real non negative V16() V20() finite cardinal Element of NAT : m ^ <*b₁*> 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 ^ <*b₁*>) where b₁ is epsilon-transitive epsilon-connected ordinal natural ext-real non negative V16() V20() finite cardinal Element of NAT : g ^ <*b₁*> in 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
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) 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
F₁((g + 1)) is set
f is Relation-like Function-like set
proj1 f is set
{ b₁ where b₁ is epsilon-transitive epsilon-connected ordinal natural ext-real non negative V16() V20() finite cardinal Element of NAT : not g + 1 <= b₁ } 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
F₁(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
F₁(t) is set
f . t is set
m is set
t is set
f . m is set
f . 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
fm is epsilon-transitive epsilon-connected ordinal natural ext-real non negative V16() V20() finite cardinal Element of NAT
{ b₁ where b₁ is epsilon-transitive epsilon-connected ordinal natural ext-real non negative V16() V20() finite cardinal Element of NAT : not card F₂() <= b₁ } is set
g is set
f is set
B . g is set
B . f is set
F₁(g) is set
F₁(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 F₂()) 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
F₁(f) is set
F₁((card F₂())) is set
{F₁((card F₂()))} is non empty trivial finite 1 -element set
F₂() \ {F₁((card F₂()))} is finite Element of bool F₂()
bool F₂() 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
F₁(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 (F₂() \ {F₁((card F₂()))}) is epsilon-transitive epsilon-connected ordinal natural ext-real non negative V16() V20() finite cardinal Element of NAT
card {F₁((card F₂()))} is epsilon-transitive epsilon-connected ordinal natural ext-real non negative V16() non empty V20() finite cardinal Element of NAT
(card F₂()) - (card {F₁((card F₂()))}) 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
F₁(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
F₁(t) is set
f is epsilon-transitive epsilon-connected ordinal natural ext-real non negative V16() V20() finite cardinal Element of NAT
F₁(f) is set
m is epsilon-transitive epsilon-connected ordinal natural ext-real non negative V16() V20() finite cardinal Element of NAT
F₁(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 ^ <*b₁*>) where b₁ is epsilon-transitive epsilon-connected ordinal natural ext-real non negative V16() V20() finite cardinal Element of NAT : g ^ <*b₁*> 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 ^ <*b₁*>) where b₁ is epsilon-transitive epsilon-connected ordinal natural ext-real non negative V16() V20() finite cardinal Element of NAT : g ^ <*b₁*> 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
{ b₁ where b₁ is Relation-like NAT -defined NAT -valued Function-like finite FinSequence-like FinSubsequence-like Element of proj1 B : len b₁ = 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 ^ <*b₁*>) where b₁ is epsilon-transitive epsilon-connected ordinal natural ext-real non negative V16() V20() finite cardinal Element of NAT : g ^ <*b₁*> 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 ^ <*b₁*>) where b₁ is epsilon-transitive epsilon-connected ordinal natural ext-real non negative V16() V20() finite cardinal Element of NAT : m ^ <*b₁*> 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
c₁₂ 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
c₁₅ is epsilon-transitive epsilon-connected ordinal natural ext-real non negative V16() V20() finite cardinal Element of NAT
c₁₅ + 1 is epsilon-transitive epsilon-connected ordinal natural ext-real positive non negative V16() non empty V20() finite cardinal Element of NAT
<*c₁₅*> is Relation-like NAT -defined NAT -valued non empty trivial Function-like constant finite 1 -element FinSequence-like FinSubsequence-like FinSequence of NAT
B | <*c₁₅*> 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 | b₁) where b₁ 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 | b₁) where b₁ 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 | b₁) where b₁ 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 | b₁) where b₁ 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 | b₁) where b₁ 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 | b₁) where b₁ 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 | b₁) where b₁ 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 | b₁) where b₁ 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 | b₁) where b₁ 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 | b₁) where b₁ 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 | b₁) where b₁ 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) | b₁) where b₁ 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
{ [b₁,(B | b₁)] where b₁ 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 | b₁) where b₁ 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 | b₁) where b₁ 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
{ [b₁,(B | b₁)] where b₁ 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 | b₁) where b₁ 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
{ [b₁,(g | b₁)] where b₁ 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 | b₁) where b₁ 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
{ [b₁,(m | b₁)] where b₁ 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 | b₁) where b₁ 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
{ [b₁,(B | b₁)] where b₁ 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 | b₁) where b₁ 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
{ [b₁,(B | b₁)] where b₁ 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 | b₁) where b₁ 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
{ [b₁,(g | b₁)] where b₁ 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 | b₁) where b₁ is Relation-like NAT -defined NAT -valued Function-like finite FinSequence-like FinSubsequence-like Element of proj1 B : ( not b₁ in Leaves (proj1 B) or B . b₁ in g ) } is set
(B) is non empty functional constituted-DTrees set
{ (B | b₁) where b₁ 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 | b₁) where b₁ 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 | b₁) where b₁ is Relation-like NAT -defined NAT -valued Function-like finite FinSequence-like FinSubsequence-like Element of proj1 g : ( not b₁ in Leaves (proj1 g) or g . b₁ 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 | b₁) where b₁ 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 | b₁) where b₁ is Relation-like NAT -defined NAT -valued Function-like finite FinSequence-like FinSubsequence-like Element of proj1 t : ( not b₁ in Leaves (proj1 t) or t . b₁ 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 | b₁) where b₁ 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 | b₁) where b₁ is Relation-like NAT -defined NAT -valued Function-like finite FinSequence-like FinSubsequence-like Element of proj1 B : ( not b₁ in Leaves (proj1 B) or B . b₁ 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 | b₁) where b₁ 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 | b₁) where b₁ is Relation-like NAT -defined NAT -valued Function-like finite FinSequence-like FinSubsequence-like Element of proj1 B : ( not b₁ in Leaves (proj1 B) or B . b₁ 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
c₁₂ is Relation-like NAT -defined NAT -valued Function-like finite FinSequence-like FinSubsequence-like Element of proj1 B
B | c₁₂ 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
{ (b₁ | b₂) where b₁ is Relation-like Function-like DecoratedTree-like Element of B, b₂ 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) is set
{ (b₁ | b₂) where b₁ is Relation-like Function-like DecoratedTree-like Element of B, b₂ is Relation-like NAT -defined NAT -valued Function-like finite FinSequence-like FinSubsequence-like Element of proj1 b₁ : verum } is set
the Relation-like Function-like DecoratedTree-like Element of B is Relation-like Function-like DecoratedTree-like Element of B
proj1 the Relation-like Function-like DecoratedTree-like Element of B is non empty Tree-like set
the Relation-like NAT -defined NAT -valued Function-like finite FinSequence-like FinSubsequence-like Element of proj1 the Relation-like Function-like DecoratedTree-like Element of B is Relation-like NAT -defined NAT -valued Function-like finite FinSequence-like FinSubsequence-like Element of proj1 the Relation-like Function-like DecoratedTree-like Element of B
the Relation-like Function-like DecoratedTree-like Element of B | the Relation-like NAT -defined NAT -valued Function-like finite FinSequence-like FinSubsequence-like Element of proj1 the Relation-like Function-like DecoratedTree-like Element of B is Relation-like Function-like DecoratedTree-like set
t is non empty set
fk is set
fm is Relation-like Function-like DecoratedTree-like Element of B
proj1 fm is non empty Tree-like set
n is Relation-like NAT -defined NAT -valued Function-like finite FinSequence-like FinSubsequence-like Element of proj1 fm
fm | n is Relation-like Function-like DecoratedTree-like set
B is non empty set
Trees B is non empty functional constituted-DTrees DTree-set of B
bool (Trees B) is non empty set
g is non empty functional constituted-DTrees Element of bool (Trees B)
(g) is non empty functional constituted-DTrees set
{ (b₁ | b₂) where b₁ is Relation-like Function-like DecoratedTree-like Element of g, b₂ is Relation-like NAT -defined NAT -valued Function-like finite FinSequence-like FinSubsequence-like Element of proj1 b₁ : verum } is set
f is set
m is Relation-like B -valued Function-like DecoratedTree-like (B, Trees B,g)
proj1 m is non empty Tree-like 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 B -valued Function-like DecoratedTree-like set
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)
(g) is non empty functional constituted-DTrees set
{ (b₁ | b₂) where b₁ is Relation-like Function-like DecoratedTree-like Element of g, b₂ is Relation-like NAT -defined NAT -valued Function-like finite FinSequence-like FinSubsequence-like Element of proj1 b₁ : verum } is set
f is set
t is Relation-like B -valued Function-like finite DecoratedTree-like () () (B, FinTrees B,g)
proj1 t is non empty finite Tree-like finite-order () set
fk is Relation-like NAT -defined NAT -valued Function-like finite FinSequence-like FinSubsequence-like Element of proj1 t
t | fk 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
m is non empty functional constituted-DTrees set
t is Relation-like Function-like DecoratedTree-like Element of m
proj1 t is non empty Tree-like set
B is set
g is non empty functional constituted-DTrees set
(g) is non empty functional constituted-DTrees set
{ (b₁ | b₂) where b₁ is Relation-like Function-like DecoratedTree-like Element of g, b₂ is Relation-like NAT -defined NAT -valued Function-like finite FinSequence-like FinSubsequence-like Element of proj1 b₁ : verum } is set
f is set
fk is Relation-like NAT -defined NAT -valued Function-like finite FinSequence-like FinSubsequence-like Element of proj1 t
t | fk is Relation-like Function-like DecoratedTree-like set
(m) is non empty functional constituted-DTrees set
{ (b₁ | b₂) where b₁ is Relation-like Function-like DecoratedTree-like Element of m, b₂ 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
g is non empty functional constituted-DTrees set
(g) is non empty functional constituted-DTrees set
{ (b₁ | b₂) where b₁ is Relation-like Function-like DecoratedTree-like Element of g, b₂ is Relation-like NAT -defined NAT -valued Function-like finite FinSequence-like FinSubsequence-like Element of proj1 b₁ : verum } is set
f is Relation-like Function-like DecoratedTree-like Element of g
proj1 f is non empty Tree-like set
m is Relation-like NAT -defined NAT -valued Function-like finite FinSequence-like FinSubsequence-like Element of proj1 f
f | m is Relation-like Function-like DecoratedTree-like set
B is non empty functional constituted-DTrees set
(B) is non empty functional constituted-DTrees set
{ (b₁ | b₂) where b₁ is Relation-like Function-like DecoratedTree-like Element of B, b₂ is Relation-like NAT -defined NAT -valued Function-like finite FinSequence-like FinSubsequence-like Element of proj1 b₁ : verum } is set
g is non empty functional constituted-DTrees set
(g) is non empty functional constituted-DTrees set
{ (b₁ | b₂) where b₁ is Relation-like Function-like DecoratedTree-like Element of g, b₂ is Relation-like NAT -defined NAT -valued Function-like finite FinSequence-like FinSubsequence-like Element of proj1 b₁ : verum } is set
f is set
m is Relation-like Function-like DecoratedTree-like Element of B
proj1 m is non empty Tree-like 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
fk is Relation-like Function-like DecoratedTree-like Element of g
proj1 fk is non empty Tree-like set
fm is Relation-like NAT -defined NAT -valued Function-like finite FinSequence-like FinSubsequence-like Element of proj1 fk
fk | fm is Relation-like Function-like DecoratedTree-like set
B is Relation-like Function-like DecoratedTree-like set
{B} is non empty trivial functional finite 1 -element set
B is Relation-like Function-like DecoratedTree-like set
{B} is non empty trivial functional finite 1 -element constituted-DTrees set
({B}) is non empty functional constituted-DTrees set
{ (b₁ | b₂) where b₁ is Relation-like Function-like DecoratedTree-like Element of {B}, b₂ 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
proj1 B is non empty Tree-like set
{ (B | b₁) where b₁ is Relation-like NAT -defined NAT -valued Function-like finite FinSequence-like FinSubsequence-like Element of proj1 B : verum } is set
g is set
f is Relation-like Function-like DecoratedTree-like Element of {B}
proj1 f is non empty Tree-like set
m is Relation-like NAT -defined NAT -valued Function-like finite FinSequence-like FinSubsequence-like Element of proj1 f
f | m is Relation-like Function-like DecoratedTree-like set
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
B is non empty functional constituted-DTrees set
(B) is non empty functional constituted-DTrees set
{ (b₁ | b₂) where b₁ is Relation-like Function-like DecoratedTree-like Element of B, b₂ is Relation-like NAT -defined NAT -valued Function-like finite FinSequence-like FinSubsequence-like Element of proj1 b₁ : verum } is set
{ (b₁) where b₁ is Relation-like Function-like DecoratedTree-like Element of B : verum } is set
union { (b₁) where b₁ is Relation-like Function-like DecoratedTree-like Element of B : verum } is set
g is set
f is Relation-like Function-like DecoratedTree-like Element of B
proj1 f is non empty Tree-like set
(f) is non empty functional constituted-DTrees set
{ (f | b₁) where b₁ is Relation-like NAT -defined NAT -valued Function-like finite FinSequence-like FinSubsequence-like Element of proj1 f : verum } is set
m is Relation-like NAT -defined NAT -valued Function-like finite FinSequence-like FinSubsequence-like Element of proj1 f
f | m is Relation-like Function-like DecoratedTree-like set
g is set
f is set
m is Relation-like Function-like DecoratedTree-like Element of B
(m) is non empty functional constituted-DTrees set
proj1 m is non empty Tree-like set
{ (m | b₁) where b₁ is Relation-like NAT -defined NAT -valued Function-like finite FinSequence-like FinSubsequence-like Element of proj1 m : verum } 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
B is non empty functional constituted-DTrees set
g is set
{ (b₁ | b₂) where b₁ is Relation-like Function-like DecoratedTree-like Element of B, b₂ is Relation-like NAT -defined NAT -valued Function-like finite FinSequence-like FinSubsequence-like Element of proj1 b₁ : ( not b₂ in Leaves (proj1 b₁) or b₁ . b₂ in g ) } is set
(B) is non empty functional constituted-DTrees set
{ (b₁ | b₂) where b₁ is Relation-like Function-like DecoratedTree-like Element of B, b₂ 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 Function-like DecoratedTree-like Element of B
proj1 t is non empty Tree-like set
fk is Relation-like NAT -defined NAT -valued Function-like finite FinSequence-like FinSubsequence-like Element of proj1 t
t | fk 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 . fk is set
fk is non empty functional constituted-DTrees set
fm is Relation-like Function-like DecoratedTree-like Element of fk
proj1 fm is non empty Tree-like set
B is set
f is non empty functional constituted-DTrees set
g is set
(f,g) is functional constituted-DTrees Element of bool (f)
(f) is non empty functional constituted-DTrees set
{ (b₁ | b₂) where b₁ is Relation-like Function-like DecoratedTree-like Element of f, b₂ is Relation-like NAT -defined NAT -valued Function-like finite FinSequence-like FinSubsequence-like Element of proj1 b₁ : verum } is set
bool (f) is non empty set
{ (b₁ | b₂) where b₁ is Relation-like Function-like DecoratedTree-like Element of f, b₂ is Relation-like NAT -defined NAT -valued Function-like finite FinSequence-like FinSubsequence-like Element of proj1 b₁ : ( not b₂ in Leaves (proj1 b₁) or b₁ . b₂ in g ) } is set
m is set
n is Relation-like NAT -defined NAT -valued Function-like finite FinSequence-like FinSubsequence-like Element of proj1 fm
fm | n is Relation-like Function-like DecoratedTree-like set
Leaves (proj1 fm) is Element of bool (proj1 fm)
bool (proj1 fm) is non empty set
fm . n is set
t is set
(fk,t) is functional constituted-DTrees Element of bool (fk)
(fk) is non empty functional constituted-DTrees set
{ (b₁ | b₂) where b₁ is Relation-like Function-like DecoratedTree-like Element of fk, b₂ is Relation-like NAT -defined NAT -valued Function-like finite FinSequence-like FinSubsequence-like Element of proj1 b₁ : verum } is set
bool (fk) is non empty set
{ (b₁ | b₂) where b₁ is Relation-like Function-like DecoratedTree-like Element of fk, b₂ is Relation-like NAT -defined NAT -valued Function-like finite FinSequence-like FinSubsequence-like Element of proj1 b₁ : ( not b₂ in Leaves (proj1 b₁) or b₁ . b₂ in t ) } is set
B is set
g is non empty functional constituted-DTrees set
(g,B) is functional constituted-DTrees Element of bool (g)
(g) is non empty functional constituted-DTrees set
{ (b₁ | b₂) where b₁ is Relation-like Function-like DecoratedTree-like Element of g, b₂ is Relation-like NAT -defined NAT -valued Function-like finite FinSequence-like FinSubsequence-like Element of proj1 b₁ : verum } is set
bool (g) is non empty set
{ (b₁ | b₂) where b₁ is Relation-like Function-like DecoratedTree-like Element of g, b₂ is Relation-like NAT -defined NAT -valued Function-like finite FinSequence-like FinSubsequence-like Element of proj1 b₁ : ( not b₂ in Leaves (proj1 b₁) or b₁ . b₂ in B ) } is set
f is Relation-like Function-like DecoratedTree-like Element of g
proj1 f is non empty Tree-like set
m is Relation-like NAT -defined NAT -valued Function-like finite FinSequence-like FinSubsequence-like Element of proj1 f
f | m is Relation-like Function-like DecoratedTree-like set
Leaves (proj1 f) is Element of bool (proj1 f)
bool (proj1 f) is non empty set
f . {} is set
f is non empty functional constituted-DTrees Element of bool (g)
the Relation-like Function-like DecoratedTree-like Element of f is Relation-like Function-like DecoratedTree-like Element of f
t is Relation-like Function-like DecoratedTree-like Element of g
proj1 t is non empty Tree-like set
fk is Relation-like NAT -defined NAT -valued Function-like finite FinSequence-like FinSubsequence-like Element of proj1 t
t | fk 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 . fk is set
fm is Relation-like NAT -defined NAT -valued Function-like finite FinSequence-like FinSubsequence-like Element of proj1 t
fm ^ <*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 DecoratedTree-like set
{B} is non empty trivial functional finite 1 -element constituted-DTrees set
g is set
({B},g) is functional constituted-DTrees Element of bool ({B})
({B}) is non empty functional constituted-DTrees set
{ (b₁ | b₂) where b₁ is Relation-like Function-like DecoratedTree-like Element of {B}, b₂ 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
{ (b₁ | b₂) where b₁ is Relation-like Function-like DecoratedTree-like Element of {B}, b₂ is Relation-like NAT -defined NAT -valued Function-like finite FinSequence-like FinSubsequence-like Element of proj1 b₁ : ( not b₂ in Leaves (proj1 b₁) or b₁ . b₂ in 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₁) where b₁ 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 | b₁) where b₁ is Relation-like NAT -defined NAT -valued Function-like finite FinSequence-like FinSubsequence-like Element of proj1 B : ( not b₁ in Leaves (proj1 B) or B . b₁ in g ) } is set
f is set
m is Relation-like Function-like DecoratedTree-like Element of {B}
proj1 m is non empty Tree-like 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
Leaves (proj1 m) is Element of bool (proj1 m)
bool (proj1 m) is non empty set
m . t is 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
B . m is set
B is set
g is non empty functional constituted-DTrees set
(g,B) is functional constituted-DTrees Element of bool (g)
(g) is non empty functional constituted-DTrees set
{ (b₁ | b₂) where b₁ is Relation-like Function-like DecoratedTree-like Element of g, b₂ is Relation-like NAT -defined NAT -valued Function-like finite FinSequence-like FinSubsequence-like Element of proj1 b₁ : verum } is set
bool (g) is non empty set
{ (b₁ | b₂) where b₁ is Relation-like Function-like DecoratedTree-like Element of g, b₂ is Relation-like NAT -defined NAT -valued Function-like finite FinSequence-like FinSubsequence-like Element of proj1 b₁ : ( not b₂ in Leaves (proj1 b₁) or b₁ . b₂ in B ) } is set
{ (b₁,B) where b₁ is Relation-like Function-like DecoratedTree-like Element of g : verum } is set
union { (b₁,B) where b₁ is Relation-like Function-like DecoratedTree-like Element of g : verum } is set
f is set
m is Relation-like Function-like DecoratedTree-like Element of g
proj1 m is non empty Tree-like set
Leaves (proj1 m) is Element of bool (proj1 m)
bool (proj1 m) is non empty set
(m,B) is functional constituted-DTrees Element of bool (m)
(m) is non empty functional constituted-DTrees set
{ (m | b₁) where b₁ is Relation-like NAT -defined NAT -valued Function-like finite FinSequence-like FinSubsequence-like Element of proj1 m : verum } is set
bool (m) is non empty set
{ (m | b₁) where b₁ is Relation-like NAT -defined NAT -valued Function-like finite FinSequence-like FinSubsequence-like Element of proj1 m : ( not b₁ in Leaves (proj1 m) or m . b₁ in B ) } 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 . t is set
f is set
m is set
t is Relation-like Function-like DecoratedTree-like Element of g
(t,B) is functional constituted-DTrees Element of bool (t)
(t) is non empty functional constituted-DTrees set
proj1 t is non empty Tree-like set
{ (t | b₁) where b₁ 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
Leaves (proj1 t) is Element of bool (proj1 t)
bool (proj1 t) is non empty set
{ (t | b₁) where b₁ is Relation-like NAT -defined NAT -valued Function-like finite FinSequence-like FinSubsequence-like Element of proj1 t : ( not b₁ in Leaves (proj1 t) or t . b₁ in B ) } is set
fk is Relation-like NAT -defined NAT -valued Function-like finite FinSequence-like FinSubsequence-like Element of proj1 t
t | fk is Relation-like Function-like DecoratedTree-like set
t . fk is set
B is non empty functional constituted-DTrees set
g is set
(B,g) is functional constituted-DTrees Element of bool (B)
(B) is non empty functional constituted-DTrees set
{ (b₁ | b₂) where b₁ is Relation-like Function-like DecoratedTree-like Element of B, b₂ 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
{ (b₁ | b₂) where b₁ is Relation-like Function-like DecoratedTree-like Element of B, b₂ is Relation-like NAT -defined NAT -valued Function-like finite FinSequence-like FinSubsequence-like Element of proj1 b₁ : ( not b₂ in Leaves (proj1 b₁) or b₁ . b₂ 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 DecoratedTree-like Element of (B)
fk is Relation-like Function-like DecoratedTree-like Element of B
proj1 fk is non empty Tree-like set
fm is Relation-like NAT -defined NAT -valued Function-like finite FinSequence-like FinSubsequence-like Element of proj1 fk
fk | fm is Relation-like Function-like DecoratedTree-like set
n is set
t9 is Relation-like NAT -defined Function-like finite FinSequence-like FinSubsequence-like DTree-yielding set
n -tree t9 is Relation-like Function-like DecoratedTree-like set
proj2 t9 is finite set
n is set
proj1 (fk | fm) is non empty Tree-like set
(proj1 fk) | fm is non empty Tree-like set
len t9 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
t9 . (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
c₁₂ is Relation-like NAT -defined NAT -valued Function-like finite FinSequence-like FinSubsequence-like Element of proj1 (m | <*n*>)
<*n*> ^ c₁₂ is Relation-like NAT -defined NAT -valued non empty Function-like finite FinSequence-like FinSubsequence-like FinSequence of NAT
proj1 m is non empty Tree-like set
fm ^ <*n*> is Relation-like NAT -defined NAT -valued non empty Function-like finite FinSequence-like FinSubsequence-like FinSequence of NAT
q is Relation-like NAT -defined NAT -valued Function-like finite FinSequence-like FinSubsequence-like Element of proj1 fk
fk | q 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)
n is set
t is Relation-like Function-like DecoratedTree-like set
t . {} is set
(t . {}) -tree n 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 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 Tree-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 NAT -defined Function-like finite FinSequence-like FinSubsequence-like set
len (B,g) is epsilon-transitive epsilon-connected ordinal natural ext-real non negative V16() V20() finite cardinal Element of NAT
((proj1 B),g) is Relation-like NAT -defined proj1 B -valued Function-like one-to-one finite FinSequence-like FinSubsequence-like FinSequence of proj1 B
len ((proj1 B),g) is epsilon-transitive epsilon-connected ordinal natural ext-real non negative V16() V20() finite cardinal Element of NAT
dom (B,g) is finite Element of bool NAT
dom ((proj1 B),g) is finite Element of bool NAT
rng ((proj1 B),g) is finite Element of bool (proj1 B)
bool (proj1 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 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
((proj1 B),f) * B is Relation-like NAT -defined Function-like finite set
B is Relation-like NAT -defined Function-like finite FinSequence-like FinSubsequence-like Tree-yielding FinTree-yielding set
tree B is non empty finite Tree-like finite-order () 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 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 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 tree B
succ g is finite Element of bool (tree B)
bool (tree B) is non empty finite V37() set
{ (g ^ <*b₁*>) where b₁ is epsilon-transitive epsilon-connected ordinal natural ext-real non negative V16() V20() finite cardinal Element of NAT : g ^ <*b₁*> in tree B } is set
card (succ g) is epsilon-transitive epsilon-connected ordinal natural ext-real non negative V16() V20() finite cardinal Element of NAT
(card (succ g)) + 1 is epsilon-transitive epsilon-connected ordinal natural ext-real positive non negative V16() non empty V20() finite cardinal Element of NAT
dom B is finite Element of bool NAT
B . ((card (succ g)) + 1) is set
<*(card (succ g))*> is Relation-like NAT -defined NAT -valued non empty trivial Function-like constant finite 1 -element FinSequence-like FinSubsequence-like FinSequence of NAT
g ^ <*(card (succ g))*> is Relation-like NAT -defined NAT -valued non empty Function-like finite {} + 1 -element FinSequence-like FinSubsequence-like FinSequence of NAT
{} + 1 is epsilon-transitive epsilon-connected ordinal natural ext-real positive non negative V16() non empty V20() finite cardinal Element of NAT
f is non empty finite Tree-like finite-order () set
<*(card (succ g))*> ^ g is Relation-like NAT -defined NAT -valued non empty Function-like finite FinSequence-like FinSubsequence-like FinSequence of NAT
<*(len B)*> is Relation-like NAT -defined NAT -valued non empty trivial Function-like constant finite 1 -element FinSequence-like FinSubsequence-like FinSequence of NAT
g ^ <*(len B)*> is Relation-like NAT -defined NAT -valued non empty Function-like finite {} + 1 -element FinSequence-like FinSubsequence-like FinSequence of NAT
{} + 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 non negative V16() V20() finite cardinal Element of NAT
m is Relation-like NAT -defined Function-like finite FinSequence-like FinSubsequence-like set
f + 1 is epsilon-transitive epsilon-connected ordinal natural ext-real positive non negative V16() non empty V20() finite cardinal Element of NAT
B . (f + 1) is set
<*f*> is Relation-like NAT -defined NAT -valued non empty trivial Function-like constant finite 1 -element FinSequence-like FinSubsequence-like FinSequence of NAT
<*f*> ^ m is Relation-like NAT -defined non empty Function-like finite FinSequence-like FinSubsequence-like set
<*(len B)*> . 1 is set
B is Relation-like Function-like finite DecoratedTree-like () () set
proj1 B is non empty finite Tree-like finite-order () set
g is set
f is Relation-like NAT -defined Function-like finite FinSequence-like FinSubsequence-like DTree-yielding set
g -tree f is Relation-like Function-like DecoratedTree-like set
roots f is Relation-like NAT -defined Function-like finite FinSequence-like FinSubsequence-like set
m 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 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 proj1 B
(B,m) is Relation-like NAT -defined Function-like finite FinSequence-like FinSubsequence-like set
doms f is Relation-like NAT -defined Function-like finite FinSequence-like FinSubsequence-like Tree-yielding set
len (doms f) is epsilon-transitive epsilon-connected ordinal natural ext-real non negative V16() V20() finite cardinal Element of NAT
len f is epsilon-transitive epsilon-connected ordinal natural ext-real non negative V16() V20() finite cardinal Element of NAT
t is set
dom (doms f) is finite Element of bool NAT
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
B | <*fk*> is Relation-like Function-like DecoratedTree-like set
proj1 (B | <*fk*>) is non empty Tree-like set
<*fk*> ^ m is Relation-like NAT -defined NAT -valued non empty Function-like finite FinSequence-like FinSubsequence-like FinSequence of NAT
dom f is finite Element of bool NAT
(doms f) . t is set
fm is Relation-like NAT -defined NAT -valued Function-like finite FinSequence-like FinSubsequence-like Element of proj1 B
B | fm is Relation-like Function-like finite DecoratedTree-like () () set
proj1 (B | fm) is non empty finite Tree-like finite-order () set
t is Relation-like NAT -defined Function-like finite FinSequence-like FinSubsequence-like Tree-yielding FinTree-yielding set
tree t is non empty finite Tree-like finite-order () set
((proj1 B),m) 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),m) is finite Element of bool (proj1 B)
bool (proj1 B) is non empty finite V37() set
dom (B,m) is finite Element of bool NAT
dom ((proj1 B),m) is finite Element of bool NAT
fk is Relation-like NAT -defined NAT -valued Function-like finite FinSequence-like FinSubsequence-like Element of proj1 B
((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
len (B,m) is epsilon-transitive epsilon-connected ordinal natural ext-real non negative V16() V20() finite cardinal Element of NAT
len ((proj1 B),m) is epsilon-transitive epsilon-connected ordinal natural ext-real non negative V16() V20() finite cardinal Element of NAT
succ m is finite Element of bool (proj1 B)
{ (m ^ <*b₁*>) where b₁ is epsilon-transitive epsilon-connected ordinal natural ext-real non negative V16() V20() finite cardinal Element of NAT : m ^ <*b₁*> in proj1 B } is set
card (succ m) is epsilon-transitive epsilon-connected ordinal natural ext-real non negative V16() V20() finite cardinal Element of NAT
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
<*fk*> is Relation-like NAT -defined NAT -valued non empty trivial Function-like constant finite 1 -element FinSequence-like FinSubsequence-like FinSequence of NAT
(proj1 B) | <*fk*> is non empty Tree-like set
f . (fk + 1) is set
(roots f) . (fk + 1) is set
B | <*fk*> is Relation-like Function-like DecoratedTree-like set
<*fk*> ^ {} is Relation-like NAT -defined non empty Function-like finite FinSequence-like FinSubsequence-like set
B . (<*fk*> ^ {}) is set
fm is Relation-like Function-like DecoratedTree-like set
fm . {} is set
(B,m) . (fk + 1) is set
((proj1 B),m) . (fk + 1) is set
B . (((proj1 B),m) . (fk + 1)) is set
m ^ <*fk*> is Relation-like NAT -defined NAT -valued non empty Function-like finite {} + 1 -element FinSequence-like FinSubsequence-like FinSequence of NAT
{} + 1 is epsilon-transitive epsilon-connected ordinal natural ext-real positive non negative V16() non empty V20() finite cardinal Element of NAT
B . (m ^ <*fk*>) is set
B . <*fk*> is set
fm is Relation-like NAT -defined NAT -valued Function-like finite FinSequence-like FinSubsequence-like Element of proj1 B
((proj1 B),fm) is Relation-like NAT -defined proj1 B -valued Function-like one-to-one finite FinSequence-like FinSubsequence-like FinSequence of proj1 B
((proj1 B),fm) * B is Relation-like NAT -defined Function-like finite set
dom (roots f) is finite Element of bool NAT
len (roots f) is epsilon-transitive epsilon-connected ordinal natural ext-real non negative V16() V20() finite cardinal Element 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 Element of proj1 B
B | g is Relation-like Function-like DecoratedTree-like set
proj1 (B | g) 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 | g)
succ f is Element of bool (proj1 (B | g))
bool (proj1 (B | g)) is non empty set
{ (f ^ <*b₁*>) where b₁ is epsilon-transitive epsilon-connected ordinal natural ext-real non negative V16() V20() finite cardinal Element of NAT : f ^ <*b₁*> in proj1 (B | g) } is set
(proj1 B) | g is non empty Tree-like set
g ^ f is Relation-like NAT -defined NAT -valued Function-like finite FinSequence-like FinSubsequence-like FinSequence of NAT
(proj1 B) with-replacement (g,((proj1 B) | g)) is non empty Tree-like set
m is Relation-like NAT -defined NAT -valued Function-like finite FinSequence-like FinSubsequence-like Element of proj1 B
succ m is finite Element of bool (proj1 B)
bool (proj1 B) is non empty set
{ (m ^ <*b₁*>) where b₁ is epsilon-transitive epsilon-connected ordinal natural ext-real non negative V16() V20() finite cardinal Element of NAT : m ^ <*b₁*> in proj1 B } is set
card (succ f) is epsilon-transitive epsilon-connected ordinal cardinal set
card (succ m) is epsilon-transitive epsilon-connected ordinal natural ext-real non negative V16() V20() finite cardinal Element 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 Element of proj1 B
B | g is Relation-like Function-like DecoratedTree-like () set
proj1 (B | g) 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 | g)
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 NAT -defined Function-like finite FinSequence-like FinSubsequence-like set
((B | g),f) is Relation-like NAT -defined Function-like finite FinSequence-like FinSubsequence-like set
(proj1 B) | g is non empty Tree-like set
(proj1 B) with-replacement (g,((proj1 B) | g)) is non empty Tree-like set
m is Relation-like NAT -defined NAT -valued Function-like finite FinSequence-like FinSubsequence-like Element of proj1 B
succ m is finite Element of bool (proj1 B)
bool (proj1 B) is non empty set
{ (m ^ <*b₁*>) where b₁ is epsilon-transitive epsilon-connected ordinal natural ext-real non negative V16() V20() finite cardinal Element of NAT : m ^ <*b₁*> in proj1 B } is set
t is Relation-like NAT -defined NAT -valued Function-like finite FinSequence-like FinSubsequence-like Element of proj1 (B | g)
succ t is finite Element of bool (proj1 (B | g))
bool (proj1 (B | g)) is non empty set
{ (t ^ <*b₁*>) where b₁ is epsilon-transitive epsilon-connected ordinal natural ext-real non negative V16() V20() finite cardinal Element of NAT : t ^ <*b₁*> in proj1 (B | g) } is set
card (succ t) is epsilon-transitive epsilon-connected ordinal natural ext-real non negative V16() V20() finite cardinal Element of NAT
card (succ m) is epsilon-transitive epsilon-connected ordinal natural ext-real non negative V16() V20() finite cardinal Element of NAT
((B | g),t) is Relation-like NAT -defined Function-like finite FinSequence-like FinSubsequence-like set
((proj1 (B | g)),t) is Relation-like NAT -defined proj1 (B | g) -valued Function-like one-to-one finite FinSequence-like FinSubsequence-like FinSequence of proj1 (B | g)
rng ((proj1 (B | g)),t) is finite Element of bool (proj1 (B | g))
dom ((B | g),t) is finite Element of bool NAT
dom ((proj1 (B | g)),t) is finite Element of bool NAT
fk is Relation-like NAT -defined NAT -valued Function-like finite FinSequence-like FinSubsequence-like Element of proj1 (B | g)
((proj1 (B | g)),fk) is Relation-like NAT -defined proj1 (B | g) -valued Function-like one-to-one finite FinSequence-like FinSubsequence-like FinSequence of proj1 (B | g)
((proj1 (B | g)),fk) * (B | g) is Relation-like NAT -defined Function-like finite set
(B,m) is Relation-like NAT -defined Function-like finite FinSequence-like FinSubsequence-like set
((proj1 B),m) 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),m) is finite Element of bool (proj1 B)
dom (B,m) is finite Element of bool NAT
dom ((proj1 B),m) is finite Element of bool NAT
fk is Relation-like NAT -defined NAT -valued Function-like finite FinSequence-like FinSubsequence-like Element of proj1 B
((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
len ((proj1 (B | g)),t) is epsilon-transitive epsilon-connected ordinal natural ext-real non negative V16() V20() finite cardinal Element of NAT
len ((proj1 B),m) is epsilon-transitive epsilon-connected ordinal natural ext-real non negative V16() V20() finite cardinal Element of NAT
fk is epsilon-transitive epsilon-connected ordinal natural ext-real non negative V16() V20() finite cardinal set
fm is epsilon-transitive epsilon-connected ordinal natural ext-real non negative V16() V20() finite cardinal Element of NAT
fm + 1 is epsilon-transitive epsilon-connected ordinal natural ext-real positive non negative V16() non empty 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
t ^ <*fm*> is Relation-like NAT -defined NAT -valued non empty Function-like finite FinSequence-like FinSubsequence-like FinSequence of NAT
(B,m) . fk is set
((proj1 B),m) . fk is set
B . (((proj1 B),m) . fk) is set
m ^ <*fm*> is Relation-like NAT -defined NAT -valued non empty Function-like finite FinSequence-like FinSubsequence-like FinSequence of NAT
B . (m ^ <*fm*>) is set
g ^ (t ^ <*fm*>) is Relation-like NAT -defined NAT -valued non empty Function-like finite FinSequence-like FinSubsequence-like FinSequence of NAT
B . (g ^ (t ^ <*fm*>)) is set
(B | g) . (t ^ <*fm*>) is set
((proj1 (B | g)),t) . fk is set
(B | g) . (((proj1 (B | g)),t) . fk) is set
((B | g),t) . fk is set
n is Relation-like NAT -defined NAT -valued Function-like finite FinSequence-like FinSubsequence-like Element of proj1 B
((proj1 B),n) is Relation-like NAT -defined proj1 B -valued Function-like one-to-one finite FinSequence-like FinSubsequence-like FinSequence of proj1 B
((proj1 B),n) * B is Relation-like NAT -defined Function-like finite set
n is Relation-like NAT -defined NAT -valued Function-like finite FinSequence-like FinSubsequence-like Element of proj1 (B | g)
((proj1 (B | g)),n) is Relation-like NAT -defined proj1 (B | g) -valued Function-like one-to-one finite FinSequence-like FinSubsequence-like FinSequence of proj1 (B | g)
((proj1 (B | g)),n) * (B | g) is Relation-like NAT -defined Function-like finite set
B is epsilon-transitive epsilon-connected ordinal natural ext-real non negative V16() V20() finite cardinal Element of NAT
Seg B is finite B -element Element of bool NAT
g is Relation-like NAT -defined Function-like finite FinSequence-like FinSubsequence-like set
g | (Seg B) is Relation-like NAT -defined Seg B -defined NAT -defined Function-like finite FinSubsequence-like set
f is Relation-like NAT -defined Function-like finite FinSequence-like FinSubsequence-like set
B is non empty set
g is Relation-like NAT -defined B -valued Function-like finite FinSequence-like FinSubsequence-like FinSequence of B
len 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
m is Relation-like NAT -defined Function-like finite FinSequence-like FinSubsequence-like 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
Seg (t + 1) is non empty finite t + 1 -element Element of bool NAT
g | (Seg (t + 1)) is Relation-like NAT -defined Seg (t + 1) -defined NAT -defined B -valued Function-like finite FinSubsequence-like Element of bool [:NAT,B:]
[:NAT,B:] is Relation-like non empty non trivial non finite set
bool [:NAT,B:] is non empty non trivial non finite set
Seg t is finite t -element Element of bool NAT
g | (Seg t) is Relation-like NAT -defined Seg t -defined NAT -defined B -valued Function-like finite FinSubsequence-like Element of bool [:NAT,B:]
len m is epsilon-transitive epsilon-connected ordinal natural ext-real non negative V16() V20() finite cardinal Element of NAT
fm is Relation-like NAT -defined Function-like finite FinSequence-like FinSubsequence-like set
m ^ fm is Relation-like NAT -defined Function-like finite FinSequence-like FinSubsequence-like set
n is Relation-like NAT -defined Function-like finite FinSequence-like FinSubsequence-like set
f ^ n 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
fm is Relation-like NAT -defined B -valued Function-like finite FinSequence-like FinSubsequence-like FinSequence of B
fk is Relation-like NAT -defined B -valued Function-like finite FinSequence-like FinSubsequence-like FinSequence of B
t + 0 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
f ^ n is Relation-like NAT -defined Function-like finite FinSequence-like FinSubsequence-like set
t9 is Relation-like NAT -defined Function-like finite FinSequence-like FinSubsequence-like set
m ^ t9 is Relation-like NAT -defined Function-like finite FinSequence-like FinSubsequence-like set
n is Relation-like NAT -defined Function-like finite FinSequence-like FinSubsequence-like set
fk ^ n is Relation-like NAT -defined Function-like finite FinSequence-like FinSubsequence-like set
t9 is Relation-like NAT -defined B -valued Function-like finite FinSequence-like FinSubsequence-like FinSequence of B
len t9 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
t + n is epsilon-transitive epsilon-connected ordinal natural ext-real non negative V16() V20() finite cardinal Element of NAT
t9 . 1 is set
n is set
dom t9 is finite Element of bool NAT
rng t9 is finite Element of bool B
bool B is non empty set
<*n*> is Relation-like NAT -defined non empty trivial Function-like constant finite 1 -element FinSequence-like FinSubsequence-like set
B is non empty set
g is Relation-like NAT -defined B -valued Function-like finite FinSequence-like FinSubsequence-like FinSequence of B
len g is epsilon-transitive epsilon-connected ordinal natural ext-real non negative V16() V20() finite cardinal Element of NAT
g | (Seg 1) is Relation-like NAT -defined Seg 1 -defined NAT -defined B -valued Function-like finite FinSubsequence-like Element of bool [:NAT,B:]
[:NAT,B:] is Relation-like non empty non trivial non finite set
bool [:NAT,B:] is non empty non trivial non finite set
f is Relation-like NAT -defined Function-like finite FinSequence-like FinSubsequence-like set
f . 1 is set
m is set
dom f is finite Element of bool NAT
proj2 f is finite set
len 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 non empty trivial Function-like constant finite 1 -element FinSequence-like FinSubsequence-like set
fk is Relation-like NAT -defined Function-like finite FinSequence-like FinSubsequence-like set
f ^ fk is Relation-like NAT -defined Function-like finite FinSequence-like FinSubsequence-like set
t is Relation-like NAT -defined B -valued Function-like finite FinSequence-like FinSubsequence-like FinSequence of B
rng t is finite Element of bool B
bool B is non empty set
B is Relation-like Function-like DecoratedTree-like set
g is Relation-like NAT -defined NAT -valued Function-like finite FinSequence-like FinSubsequence-like FinSequence of NAT
B . g is set
B | g is Relation-like Function-like DecoratedTree-like set
(B | g) . {} is set
proj1 B is non empty Tree-like set
(proj1 B) | g is non empty Tree-like set
(B | g) . (<*> NAT) is set
g ^ (<*> NAT) is Relation-like NAT -defined NAT -valued Function-like finite FinSequence-like FinSubsequence-like FinSequence of NAT
B . (g ^ (<*> NAT)) is set
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 Element of proj1 B
(B,g) is Relation-like NAT -defined Function-like finite FinSequence-like FinSubsequence-like set
((proj1 B),g) is Relation-like NAT -defined proj1 B -valued Function-like one-to-one finite FinSequence-like FinSubsequence-like FinSequence of proj1 B
((proj1 B),g) * B is Relation-like NAT -defined Function-like finite 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
((proj1 B),f) * B is Relation-like NAT -defined Function-like finite set
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 Element of proj1 B
((proj1 B),g) is Relation-like NAT -defined proj1 B -valued Function-like one-to-one finite FinSequence-like FinSubsequence-like FinSequence of proj1 B
((proj1 B),g) * B is Relation-like NAT -defined Function-like finite set
dom (((proj1 B),g) * B) is finite Element of bool NAT
dom ((proj1 B),g) is finite Element of bool NAT
rng ((proj1 B),g) is finite Element of bool (proj1 B)
bool (proj1 B) is non empty set
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 Element of proj1 B
(B,g) is Relation-like NAT -defined Function-like finite FinSequence-like FinSubsequence-like set
dom (B,g) is finite Element of bool NAT
((proj1 B),g) is Relation-like NAT -defined proj1 B -valued Function-like one-to-one finite FinSequence-like FinSubsequence-like FinSequence of proj1 B
dom ((proj1 B),g) is finite Element of bool NAT
((proj1 B),g) * B is Relation-like NAT -defined Function-like finite set
dom (((proj1 B),g) * B) is finite Element of bool 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 Element of proj1 B
((proj1 B),g) is Relation-like NAT -defined proj1 B -valued Function-like one-to-one finite FinSequence-like FinSubsequence-like FinSequence of proj1 B
dom ((proj1 B),g) is finite Element of bool 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
f + 1 is epsilon-transitive epsilon-connected ordinal natural ext-real positive non negative V16() non empty V20() finite cardinal Element of NAT
succ g is finite Element of bool (proj1 B)
bool (proj1 B) is non empty set
{ (g ^ <*b₁*>) where b₁ is epsilon-transitive epsilon-connected ordinal natural ext-real non negative V16() V20() finite cardinal Element of NAT : g ^ <*b₁*> in proj1 B } is set
card (succ g) is epsilon-transitive epsilon-connected ordinal natural ext-real non negative V16() V20() finite cardinal Element of NAT
len ((proj1 B),g) is epsilon-transitive epsilon-connected ordinal natural ext-real non negative V16() V20() finite cardinal Element of NAT
0 + 1 is epsilon-transitive epsilon-connected ordinal natural ext-real positive non negative V16() non empty V20() finite cardinal Element of NAT
Seg (len ((proj1 B),g)) is finite len ((proj1 B),g) -element Element of bool NAT
B is Relation-like Function-like DecoratedTree-like () set
proj1 B is non empty Tree-like () set
g is Relation-like NAT -defined Function-like finite FinSequence-like FinSubsequence-like set
(B,g) is Relation-like NAT -defined Function-like finite FinSequence-like FinSubsequence-like set
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 non empty Function-like finite FinSequence-like FinSubsequence-like set
B . (g ^ <*f*>) is set
f + 1 is epsilon-transitive epsilon-connected ordinal natural ext-real positive non negative V16() non empty V20() finite cardinal Element of NAT
(B,g) . (f + 1) is set
m is Relation-like NAT -defined NAT -valued Function-like finite FinSequence-like FinSubsequence-like Element of proj1 B
((proj1 B),m) is Relation-like NAT -defined proj1 B -valued Function-like one-to-one finite FinSequence-like FinSubsequence-like FinSequence of proj1 B
((proj1 B),m) * B is Relation-like NAT -defined Function-like finite set
dom ((proj1 B),m) is finite Element of bool NAT
len ((proj1 B),m) is epsilon-transitive epsilon-connected ordinal natural ext-real non negative V16() V20() finite cardinal Element of NAT
Seg (len ((proj1 B),m)) is finite len ((proj1 B),m) -element Element of bool NAT
dom (((proj1 B),m) * B) is finite Element of bool NAT
((proj1 B),m) . (f + 1) is set
B . (((proj1 B),m) . (f + 1)) is set
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 Element of proj1 B
B . g is set
f is Relation-like NAT -defined NAT -valued Function-like finite FinSequence-like FinSubsequence-like Element of proj1 B
succ f is finite Element of bool (proj1 B)
bool (proj1 B) is non empty set
{ (f ^ <*b₁*>) where b₁ is epsilon-transitive epsilon-connected ordinal natural ext-real non negative V16() V20() finite cardinal Element of NAT : f ^ <*b₁*> in proj1 B } is set
(B,f) is Relation-like NAT -defined Function-like finite FinSequence-like FinSubsequence-like set
proj2 (B,f) is finite 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
f ^ <*m*> is Relation-like NAT -defined NAT -valued non empty Function-like finite FinSequence-like FinSubsequence-like FinSequence 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,f) . (m + 1) is set
dom (B,f) is finite Element of bool NAT
((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
((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
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 Element of proj1 B
(B,g) is Relation-like NAT -defined Function-like finite FinSequence-like FinSubsequence-like set
proj2 (B,g) is finite set
succ g is finite Element of bool (proj1 B)
bool (proj1 B) is non empty set
{ (g ^ <*b₁*>) where b₁ is epsilon-transitive epsilon-connected ordinal natural ext-real non negative V16() V20() finite cardinal Element of NAT : g ^ <*b₁*> in proj1 B } is set
f is set
dom (B,g) is finite Element of bool NAT
m is epsilon-transitive epsilon-connected ordinal natural ext-real non negative V16() V20() finite cardinal set
Seg m is finite m -element Element of bool NAT
t is set
(B,g) . t is set
{ b₁ where b₁ is epsilon-transitive epsilon-connected ordinal natural ext-real non negative V16() V20() finite cardinal Element of NAT : ( 1 <= b₁ & b₁ <= m ) } 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
fm + 1 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 + 1 is epsilon-transitive epsilon-connected ordinal natural ext-real positive non negative V16() non empty V20() finite cardinal Element of NAT
((proj1 B),g) is Relation-like NAT -defined proj1 B -valued Function-like one-to-one finite FinSequence-like FinSubsequence-like FinSequence of proj1 B
dom ((proj1 B),g) is finite Element of bool 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
g ^ <*n*> is Relation-like NAT -defined NAT -valued non empty Function-like finite FinSequence-like FinSubsequence-like FinSequence of NAT
t9 is Relation-like NAT -defined NAT -valued Function-like finite FinSequence-like FinSubsequence-like Element of proj1 B
B . t9 is set
F₁() is non empty set
F₂() is Element of F₁()
{0} is non empty trivial functional finite V37() 1 -element Tree-like finite-order () set
B is set
F₃(B) is Relation-like NAT -defined F₁() -valued Function-like finite FinSequence-like FinSubsequence-like FinSequence of F₁()
len F₃(B) is epsilon-transitive epsilon-connected ordinal natural ext-real non negative V16() V20() finite cardinal Element of NAT
g is epsilon-transitive epsilon-connected ordinal natural ext-real non negative V16() V20() finite cardinal set
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 non negative V16() V20() finite cardinal Element of NAT
Seg f is finite f -element Element of bool NAT
{0} \/ (Seg f) is non empty finite set
m is set
B is Relation-like Function-like set
proj1 B is set
B is Relation-like Function-like set
g is epsilon-transitive epsilon-connected ordinal natural ext-real non negative V16() V20() finite cardinal Element of NAT
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 set
B . f is set
F₃(f) is Relation-like NAT -defined F₁() -valued Function-like finite FinSequence-like FinSubsequence-like FinSequence of F₁()
len F₃(f) is epsilon-transitive epsilon-connected ordinal natural ext-real non negative V16() V20() finite cardinal Element of NAT
Seg (len F₃(f)) is finite len F₃(f) -element Element of bool 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
Seg m is finite m -element Element of bool NAT
{0} \/ (Seg m) is non empty 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
0 + 1 is epsilon-transitive epsilon-connected ordinal natural ext-real positive non negative V16() non empty 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
Seg m is finite m -element Element of bool NAT
{0} \/ (Seg m) is non empty finite set
g is Relation-like Function-like DecoratedTree-like () set
proj1 g is non empty Tree-like () set
f is set
B . f is set
F₃(f) is Relation-like NAT -defined F₁() -valued Function-like finite FinSequence-like FinSubsequence-like FinSequence of F₁()
len F₃(f) is epsilon-transitive epsilon-connected ordinal natural ext-real non negative V16() V20() finite cardinal Element of NAT
Seg (len F₃(f)) is finite len F₃(f) -element Element of bool NAT
m is Relation-like NAT -defined NAT -valued Function-like finite FinSequence-like FinSubsequence-like Element of proj1 g
{ (m ^ <*b₁*>) where b₁ is epsilon-transitive epsilon-connected ordinal natural ext-real non negative V16() V20() finite cardinal Element of NAT : b₁ in H₁(f) } is set
{ (m ^ <*b₁*>) where b₁ is epsilon-transitive epsilon-connected ordinal natural ext-real non negative V16() V20() finite cardinal Element of NAT : b₁ + 1 in Seg (len F₃(f)) } is set
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
m ^ <*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
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
m ^ <*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
[:F₁(),NAT:] is Relation-like non empty non trivial non finite set
g is Element of [:F₁(),NAT:]
g `1 is set
g `2 is set
f is Element of F₁()
m is epsilon-transitive epsilon-connected ordinal natural ext-real non negative V16() V20() finite cardinal Element of NAT
[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 . f is set
m + 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 NAT -defined F₁() -valued Function-like finite FinSequence-like FinSubsequence-like FinSequence of F₁()
len F₃(f) is epsilon-transitive epsilon-connected ordinal natural ext-real non negative V16() V20() finite cardinal Element of NAT
Seg (len F₃(f)) is finite len F₃(f) -element Element of bool NAT
dom F₃(f) is finite Element of bool NAT
F₃(f) . (m + 1) is set
rng F₃(f) is finite Element of bool F₁()
bool F₁() is non empty set
B . f is set
B . f is set
[:[:F₁(),NAT:],F₁():] is Relation-like non empty non trivial non finite set
bool [:[:F₁(),NAT:],F₁():] is non empty non trivial non finite set
g is Relation-like [:F₁(),NAT:] -defined F₁() -valued Function-like V30([:F₁(),NAT:],F₁()) Element of bool [:[:F₁(),NAT:],F₁():]
g is Relation-like [:F₁(),NAT:] -defined F₁() -valued Function-like V30([:F₁(),NAT:],F₁()) Element of bool [:[:F₁(),NAT:],F₁():]
f is epsilon-transitive epsilon-connected ordinal natural ext-real non negative V16() V20() finite cardinal Element of NAT
m is set
F₃(m) is Relation-like NAT -defined F₁() -valued Function-like finite FinSequence-like FinSubsequence-like FinSequence of F₁()
len F₃(m) is epsilon-transitive epsilon-connected ordinal natural ext-real non negative V16() V20() finite cardinal Element of NAT
B . 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
Seg t is finite t -element Element of bool NAT
Seg t is finite t -element Element of bool NAT
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
Seg fk is finite fk -element Element of bool NAT
{0} \/ (Seg fk) is non empty finite 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
Seg fk is finite fk -element Element of bool NAT
{0} \/ (Seg fk) is non empty 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
Seg t is finite t -element Element of bool NAT
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
Seg fk is finite fk -element Element of bool NAT
{0} \/ (Seg fk) is non empty finite set
f is Element of F₁()
B . 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
F₃(f) is Relation-like NAT -defined F₁() -valued Function-like finite FinSequence-like FinSubsequence-like FinSequence of F₁()
len F₃(f) is epsilon-transitive epsilon-connected ordinal natural ext-real non negative V16() V20() finite cardinal Element of NAT
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
Seg fk is finite fk -element Element of bool NAT
{0} \/ (Seg fk) is non empty finite 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 is Relation-like F₁() -valued Function-like DecoratedTree-like set
f . {} is set
proj1 f is non empty Tree-like set
m is Relation-like NAT -defined NAT -valued Function-like finite FinSequence-like FinSubsequence-like Element of proj1 f
succ m is Element of bool (proj1 f)
bool (proj1 f) is non empty set
{ (m ^ <*b₁*>) where b₁ is epsilon-transitive epsilon-connected ordinal natural ext-real non negative V16() V20() finite cardinal Element of NAT : m ^ <*b₁*> in proj1 f } is set
f . m is Element of F₁()
F₃((f . m)) is Relation-like NAT -defined F₁() -valued Function-like finite FinSequence-like FinSubsequence-like FinSequence of F₁()
len F₃((f . m)) is epsilon-transitive epsilon-connected ordinal natural ext-real non negative V16() V20() finite cardinal Element of NAT
Seg (len F₃((f . m))) is finite len F₃((f . m)) -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 set
fk + 1 is epsilon-transitive epsilon-connected ordinal natural ext-real positive non negative V16() non empty 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
<*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
n is set
t is Relation-like NAT -defined Function-like finite FinSequence-like FinSubsequence-like set
dom t is finite Element of bool NAT
t is Relation-like NAT -defined Function-like finite FinSequence-like FinSubsequence-like set
dom t is finite Element of bool NAT
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
t . (fk + 1) 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
m ^ <*fk*> is Relation-like NAT -defined NAT -valued non empty Function-like finite FinSequence-like FinSubsequence-like FinSequence of NAT
fm is epsilon-transitive epsilon-connected ordinal natural ext-real non negative V16() V20() finite cardinal Element of NAT
fm + 1 is epsilon-transitive epsilon-connected ordinal natural ext-real positive non negative V16() non empty 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
B . (f . m) is set
{ (m ^ <*b₁*>) where b₁ is epsilon-transitive epsilon-connected ordinal natural ext-real non negative V16() V20() finite cardinal Element of NAT : b₁ in H₁(f . m) } is set
proj2 t is finite set
fk is set
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
fm + 1 is epsilon-transitive epsilon-connected ordinal natural ext-real positive non negative V16() non empty V20() finite cardinal Element of NAT
t . (fm + 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
fk is set
B . fk is set
g . (fk,t) is set
[fk,t] is non empty V27() set
{fk,t} is non empty finite set
{fk} is non empty trivial finite 1 -element set
{{fk,t},{fk}} is non empty finite V37() set
g . [fk,t] is set
F₃(fk) is Relation-like NAT -defined F₁() -valued Function-like finite FinSequence-like FinSubsequence-like FinSequence of F₁()
F₃(fk) . (t + 1) is set
[fk,t] `1 is set
[fk,t] `2 is set
fm is Element of [:F₁(),NAT:]
g . fm is Element of F₁()
n is set
t9 is epsilon-transitive epsilon-connected ordinal natural ext-real non negative V16() V20() finite cardinal Element of NAT
[n,t9] is non empty V27() set
{n,t9} is non empty finite set
{n} is non empty trivial finite 1 -element set
{{n,t9},{n}} is non empty finite V37() set
B . n is set
F₃(n) is Relation-like NAT -defined F₁() -valued Function-like finite FinSequence-like FinSubsequence-like FinSequence of F₁()
t9 + 1 is epsilon-transitive epsilon-connected ordinal natural ext-real positive non negative V16() non empty V20() finite cardinal Element of NAT
F₃(n) . (t9 + 1) is set
m is Relation-like F₁() -valued Function-like DecoratedTree-like () set
proj1 m is non empty Tree-like () set
fk is Element of F₁()
t is Relation-like NAT -defined NAT -valued Function-like finite FinSequence-like FinSubsequence-like Element of proj1 m
m . t is Element of F₁()
succ t is finite Element of bool (proj1 m)
bool (proj1 m) is non empty set
{ (t ^ <*b₁*>) where b₁ is epsilon-transitive epsilon-connected ordinal natural ext-real non negative V16() V20() finite cardinal Element of NAT : t ^ <*b₁*> in proj1 m } is set
B . fk is set
{ (t ^ <*b₁*>) where b₁ is epsilon-transitive epsilon-connected ordinal natural ext-real non negative V16() V20() finite cardinal Element of NAT : b₁ in H₁(fk) } is set
F₃(fk) is Relation-like NAT -defined F₁() -valued Function-like finite FinSequence-like FinSubsequence-like FinSequence of F₁()
len F₃(fk) is epsilon-transitive epsilon-connected ordinal natural ext-real non negative V16() V20() finite cardinal Element of NAT
Seg (len F₃(fk)) is finite len F₃(fk) -element Element of bool NAT
{ (t ^ <*b₁*>) where b₁ is epsilon-transitive epsilon-connected ordinal natural ext-real non negative V16() V20() finite cardinal Element of NAT : b₁ + 1 in Seg (len F₃(fk)) } is set
dom F₃(fk) is finite Element of bool NAT
((proj1 m),t) is Relation-like NAT -defined proj1 m -valued Function-like one-to-one finite FinSequence-like FinSubsequence-like FinSequence of proj1 m
dom ((proj1 m),t) is finite Element of bool NAT
len ((proj1 m),t) is epsilon-transitive epsilon-connected ordinal natural ext-real non negative V16() V20() finite cardinal Element of NAT
Seg (len ((proj1 m),t)) is finite len ((proj1 m),t) -element Element of bool NAT
fm is set
{ b₁ where b₁ is epsilon-transitive epsilon-connected ordinal natural ext-real non negative V16() V20() finite cardinal Element of NAT : ( 1 <= b₁ & b₁ <= len ((proj1 m),t) ) } 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
t9 + 1 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 + 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
t ^ <*n*> is Relation-like NAT -defined NAT -valued non empty Function-like finite FinSequence-like FinSubsequence-like FinSequence 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
t ^ <*n*> is Relation-like NAT -defined NAT -valued non empty Function-like finite FinSequence-like FinSubsequence-like FinSequence 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 is set
{ b₁ where b₁ is epsilon-transitive epsilon-connected ordinal natural ext-real non negative V16() V20() finite cardinal Element of NAT : ( 1 <= b₁ & b₁ <= len F₃(fk) ) } 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
t9 + 1 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 + 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
t ^ <*n*> is Relation-like NAT -defined NAT -valued non empty Function-like finite FinSequence-like FinSubsequence-like FinSequence of NAT
(m,t) is Relation-like NAT -defined Function-like finite FinSequence-like FinSubsequence-like set
dom (m,t) is finite Element of bool NAT
fm is epsilon-transitive epsilon-connected ordinal natural ext-real non negative V16() V20() finite cardinal set
(m,t) . fm is set
F₃(fk) . fm is set
{ b₁ where b₁ is epsilon-transitive epsilon-connected ordinal natural ext-real non negative V16() V20() finite cardinal Element of NAT : ( 1 <= b₁ & b₁ <= len F₃(fk) ) } is set
F₃((m . t)) is Relation-like NAT -defined F₁() -valued Function-like finite FinSequence-like FinSubsequence-like FinSequence of F₁()
len F₃((m . t)) is epsilon-transitive epsilon-connected ordinal natural ext-real non negative V16() V20() finite cardinal Element of NAT
B . (m . t) 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
Seg n is finite n -element Element of bool NAT
{0} \/ (Seg n) is non empty finite set
t9 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 set
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 epsilon-transitive epsilon-connected ordinal natural ext-real non negative V16() V20() finite cardinal Element of NAT
0 + 1 is epsilon-transitive epsilon-connected ordinal natural ext-real positive non negative V16() non empty 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
t ^ <*n*> is Relation-like NAT -defined NAT -valued non empty Function-like finite FinSequence-like FinSubsequence-like FinSequence of NAT
(m,t) . (n + 1) is set
m . (t ^ <*n*>) is set
g . ((m . t),n) is Element of F₁()
[(m . t),n] is non empty V27() set
{(m . t),n} is non empty finite set
{(m . t)} is non empty trivial finite 1 -element set
{{(m . t),n},{(m . t)}} is non empty finite V37() set
g . [(m . t),n] is set
F₃(fk) . (n + 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
ProperPrefixes g is finite set
f is Relation-like NAT -defined NAT -valued Function-like finite 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
B is non empty Tree-like set
B -level 0 is Level of B
{ b₁ where b₁ is Relation-like NAT -defined NAT -valued Function-like finite FinSequence-like FinSubsequence-like Element of B : len b₁ = 0 } is set
g is set
f is Relation-like NAT -defined NAT -valued Function-like finite FinSequence-like FinSubsequence-like Element of B
len f is epsilon-transitive epsilon-connected ordinal natural ext-real non negative V16() V20() finite cardinal Element of NAT
g is set
f is Relation-like NAT -defined NAT -valued Function-like finite FinSequence-like FinSubsequence-like Element of B
len f is epsilon-transitive epsilon-connected ordinal natural ext-real non negative V16() V20() finite cardinal Element of 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 non empty Tree-like set
g -level (B + 1) is Level of g
{ b₁ where b₁ is Relation-like NAT -defined NAT -valued Function-like finite FinSequence-like FinSubsequence-like Element of g : len b₁ = B + 1 } is set
{ (succ b₁) where b₁ is Relation-like NAT -defined NAT -valued Function-like finite FinSequence-like FinSubsequence-like Element of g : len b₁ = B } is set
union { (succ b₁) where b₁ is Relation-like NAT -defined NAT -valued Function-like finite FinSequence-like FinSubsequence-like Element of g : len b₁ = B } is set
f is set
m is Relation-like NAT -defined NAT -valued Function-like finite FinSequence-like FinSubsequence-like Element of g
Seg B is finite B -element Element of bool NAT
m | (Seg B) is Relation-like NAT -defined Seg B -defined NAT -defined NAT -valued Function-like finite FinSubsequence-like Element of bool [:NAT,NAT:]
bool [:NAT,NAT:] is non empty non trivial non finite set
t is Relation-like NAT -defined NAT -valued Function-like finite FinSequence-like FinSubsequence-like FinSequence of NAT
B + 0 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 Function-like finite FinSequence-like FinSubsequence-like Element of g
len fk 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 Function-like finite FinSequence-like FinSubsequence-like Element of g
len fm is epsilon-transitive epsilon-connected ordinal natural ext-real non negative V16() V20() finite cardinal Element of NAT
succ fk is Element of bool g
bool g is non empty set
{ (fk ^ <*b₁*>) where b₁ is epsilon-transitive epsilon-connected ordinal natural ext-real non negative V16() V20() finite cardinal Element of NAT : fk ^ <*b₁*> in g } is set
Seg (B + 1) is non empty finite B + 1 -element Element of bool NAT
dom m is finite Element of bool NAT
fm is Relation-like NAT -defined NAT -valued Function-like finite FinSequence-like FinSubsequence-like Element of g
len fm is epsilon-transitive epsilon-connected ordinal natural ext-real non negative V16() V20() finite cardinal Element of NAT
m | (Seg (B + 1)) is Relation-like NAT -defined Seg (B + 1) -defined NAT -defined NAT -valued Function-like finite FinSubsequence-like Element of bool [:NAT,NAT:]
fm is Relation-like NAT -defined NAT -valued Function-like finite FinSequence-like FinSubsequence-like Element of g
len fm 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
<*fm*> is Relation-like NAT -defined NAT -valued non empty trivial Function-like constant finite 1 -element FinSequence-like FinSubsequence-like FinSequence of NAT
fk ^ <*fm*> is Relation-like NAT -defined NAT -valued non empty Function-like finite FinSequence-like FinSubsequence-like FinSequence of NAT
m is set
t is set
fk is Relation-like NAT -defined NAT -valued Function-like finite FinSequence-like FinSubsequence-like Element of g
succ fk is Element of bool g
bool g is non empty set
{ (fk ^ <*b₁*>) where b₁ is epsilon-transitive epsilon-connected ordinal natural ext-real non negative V16() V20() finite cardinal Element of NAT : fk ^ <*b₁*> in g } is set
len fk 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 Function-like finite FinSequence-like FinSubsequence-like Element of g
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
fk ^ <*n*> is Relation-like NAT -defined NAT -valued non empty Function-like finite FinSequence-like FinSubsequence-like FinSequence of NAT
len <*n*> is epsilon-transitive epsilon-connected ordinal natural ext-real non negative V16() non empty 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
B is non empty Tree-like () set
g is epsilon-transitive epsilon-connected ordinal natural ext-real non negative V16() V20() finite cardinal Element of NAT
B -level g is Level of B
{ b₁ where b₁ is Relation-like NAT -defined NAT -valued Function-like finite FinSequence-like FinSubsequence-like Element of B : len b₁ = 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
B -level (g + 1) is Level of B
{ b₁ where b₁ is Relation-like NAT -defined NAT -valued Function-like finite FinSequence-like FinSubsequence-like Element of B : len b₁ = g + 1 } is set
{ (succ b₁) where b₁ is Relation-like NAT -defined NAT -valued Function-like finite FinSequence-like FinSubsequence-like Element of B : len b₁ = g } is set
m is set
t is Relation-like NAT -defined NAT -valued Function-like finite FinSequence-like FinSubsequence-like Element of B
succ t is finite Element of bool B
bool B is non empty set
{ (t ^ <*b₁*>) where b₁ is epsilon-transitive epsilon-connected ordinal natural ext-real non negative V16() V20() finite cardinal Element of NAT : t ^ <*b₁*> in B } is set
fk is set
m is Relation-like Function-like set
proj1 m is set
proj2 m is set
t is set
fk is Relation-like NAT -defined NAT -valued Function-like finite FinSequence-like FinSubsequence-like Element of B
succ fk is finite Element of bool B
bool B is non empty set
{ (fk ^ <*b₁*>) where b₁ is epsilon-transitive epsilon-connected ordinal natural ext-real non negative V16() V20() finite cardinal Element of NAT : fk ^ <*b₁*> in B } is set
len fk is epsilon-transitive epsilon-connected ordinal natural ext-real non negative V16() V20() finite cardinal Element of NAT
m . fk is set
fm is Relation-like NAT -defined NAT -valued Function-like finite FinSequence-like FinSubsequence-like Element of B
succ fm is finite Element of bool B
{ (fm ^ <*b₁*>) where b₁ is epsilon-transitive epsilon-connected ordinal natural ext-real non negative V16() V20() finite cardinal Element of NAT : fm ^ <*b₁*> in B } is set
card (proj2 m) is epsilon-transitive epsilon-connected ordinal cardinal set
card (proj1 m) is epsilon-transitive epsilon-connected ordinal cardinal set
m is set
t is Relation-like NAT -defined NAT -valued Function-like finite FinSequence-like FinSubsequence-like Element of B
succ t is finite Element of bool B
bool B is non empty set
{ (t ^ <*b₁*>) where b₁ is epsilon-transitive epsilon-connected ordinal natural ext-real non negative V16() V20() finite cardinal Element of NAT : t ^ <*b₁*> in B } is set
len t is epsilon-transitive epsilon-connected ordinal natural ext-real non negative V16() V20() finite cardinal Element of NAT
union { (succ b₁) where b₁ is Relation-like NAT -defined NAT -valued Function-like finite FinSequence-like FinSubsequence-like Element of B : len b₁ = g } is set
B -level 0 is Level of B
{ b₁ where b₁ is Relation-like NAT -defined NAT -valued Function-like finite FinSequence-like FinSubsequence-like Element of B : len b₁ = 0 } is set
B is non empty Tree-like () set
g is epsilon-transitive epsilon-connected ordinal natural ext-real non negative V16() V20() finite cardinal Element of NAT
B -level g is Level of B
{ b₁ where b₁ is Relation-like NAT -defined NAT -valued Function-like finite FinSequence-like FinSubsequence-like Element of B : len b₁ = g } is set
f is set
m is Relation-like NAT -defined NAT -valued Function-like finite FinSequence-like FinSubsequence-like Element of B
len m is epsilon-transitive epsilon-connected ordinal natural ext-real non negative V16() V20() finite cardinal Element of NAT
ProperPrefixes m is finite set
t is finite Chain of B
card t is epsilon-transitive epsilon-connected ordinal natural ext-real non negative V16() V20() finite cardinal Element of NAT
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₁*>) where b₁ is epsilon-transitive epsilon-connected ordinal natural ext-real non negative V16() V20() finite cardinal Element of NAT : g ^ <*b₁*> in B } is set
g is Chain of B
g is epsilon-transitive epsilon-connected ordinal natural ext-real non negative V16() V20() finite cardinal Element of NAT
B -level g is Level of B
{ b₁ where b₁ is Relation-like NAT -defined NAT -valued Function-like finite FinSequence-like FinSubsequence-like Element of B : len b₁ = g } is set
g is epsilon-transitive epsilon-connected ordinal natural ext-real non negative V16() V20() finite cardinal Element of NAT
B -level g is Level of B
{ b₁ where b₁ is Relation-like NAT -defined NAT -valued Function-like finite FinSequence-like FinSubsequence-like Element of B : len b₁ = g } is set
g is epsilon-transitive epsilon-connected ordinal natural ext-real non negative V16() V20() finite cardinal Element of NAT
B -level g is Level of B
{ b₁ where b₁ is Relation-like NAT -defined NAT -valued Function-like finite FinSequence-like FinSubsequence-like Element of B : len b₁ = g } is set
{ H₁(b₁) where b₁ is epsilon-transitive epsilon-connected ordinal natural ext-real non negative V16() V20() finite cardinal Element of NAT : b₁ <= g } is set
union { H₁(b₁) where b₁ is epsilon-transitive epsilon-connected ordinal natural ext-real non negative V16() V20() finite cardinal Element of NAT : b₁ <= g } is set
m is set
t is Relation-like NAT -defined NAT -valued Function-like finite FinSequence-like FinSubsequence-like Element of B
len t is epsilon-transitive epsilon-connected ordinal natural ext-real non negative V16() V20() finite cardinal Element of NAT
fk is epsilon-transitive epsilon-connected ordinal natural ext-real non negative V16() V20() finite cardinal Element of NAT
B -level fk is Level of B
{ b₁ where b₁ is Relation-like NAT -defined NAT -valued Function-like finite FinSequence-like FinSubsequence-like Element of B : len b₁ = fk } is set
Seg g is finite g -element Element of bool NAT
t | (Seg g) is Relation-like NAT -defined Seg g -defined NAT -defined NAT -valued Function-like finite FinSubsequence-like Element of bool [:NAT,NAT:]
bool [:NAT,NAT:] is non empty non trivial non finite set
fm is Relation-like NAT -defined Function-like finite FinSequence-like FinSubsequence-like set
len fm 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 Function-like finite FinSequence-like FinSubsequence-like Element of B
g + 1 is epsilon-transitive epsilon-connected ordinal natural ext-real positive non negative V16() non empty V20() finite cardinal Element of NAT
Seg (g + 1) is non empty finite g + 1 -element Element of bool NAT
m is epsilon-transitive epsilon-connected ordinal natural ext-real non negative V16() V20() finite cardinal set
t is epsilon-transitive epsilon-connected ordinal natural ext-real non negative V16() V20() finite cardinal set
t + 1 is epsilon-transitive epsilon-connected ordinal natural ext-real positive non negative V16() non empty V20() finite cardinal Element of NAT
fk is epsilon-transitive epsilon-connected ordinal natural ext-real non negative V16() V20() finite cardinal Element of NAT
B -level fk is Level of B
{ b₁ where b₁ is Relation-like NAT -defined NAT -valued Function-like finite FinSequence-like FinSubsequence-like Element of B : len b₁ = fk } is set
fm is set
fk + 1 is epsilon-transitive epsilon-connected ordinal natural ext-real positive non negative V16() non empty V20() finite cardinal Element of NAT
m is Relation-like NAT -defined Function-like finite FinSequence-like FinSubsequence-like set
dom m is finite Element of bool 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
m . (t + 1) is set
B -level t is Level of B
{ b₁ where b₁ is Relation-like NAT -defined NAT -valued Function-like finite FinSequence-like FinSubsequence-like Element of B : len b₁ = t } is set
fm is epsilon-transitive epsilon-connected ordinal natural ext-real non negative V16() V20() finite cardinal Element of NAT
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
B -level fk is Level of B
{ b₁ where b₁ is Relation-like NAT -defined NAT -valued Function-like finite FinSequence-like FinSubsequence-like Element of B : len b₁ = fk } is set
proj2 m is finite set
t is set
fk is epsilon-transitive epsilon-connected ordinal natural ext-real non negative V16() V20() finite cardinal Element of NAT
B -level fk is Level of B
{ b₁ where b₁ is Relation-like NAT -defined NAT -valued Function-like finite FinSequence-like FinSubsequence-like Element of B : len b₁ = fk } is set
0 + 1 is epsilon-transitive epsilon-connected ordinal natural ext-real positive non negative V16() non empty 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
m . (fk + 1) is set
m is set
t is epsilon-transitive epsilon-connected ordinal natural ext-real non negative V16() V20() finite cardinal Element of NAT
B -level t is Level of B
{ b₁ where b₁ is Relation-like NAT -defined NAT -valued Function-like finite FinSequence-like FinSubsequence-like Element of B : len b₁ = t } is set
B is non empty Tree-like () set
g is epsilon-transitive epsilon-connected ordinal natural ext-real non negative V16() V20() finite cardinal Element of NAT
B -level g is Level of B
{ b₁ where b₁ is Relation-like NAT -defined NAT -valued Function-like finite FinSequence-like FinSubsequence-like Element of B : len b₁ = g } is set
f is set
m is Relation-like NAT -defined NAT -valued Function-like finite FinSequence-like FinSubsequence-like Element of B
ProperPrefixes m is finite set
t is finite Chain of B
card t 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 Function-like finite FinSequence-like FinSubsequence-like Element of B
len fk is epsilon-transitive epsilon-connected ordinal natural ext-real non negative V16() V20() finite cardinal Element of NAT
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₁*>) where b₁ is epsilon-transitive epsilon-connected ordinal natural ext-real non negative V16() V20() finite cardinal Element of NAT : g ^ <*b₁*> in B } is set
B is non empty Tree-like () set
g is Chain of B
f is non empty Branch-like Chain of B
B is non empty Tree-like set
g is Chain of B
f is Relation-like NAT -defined NAT -valued Function-like finite FinSequence-like FinSubsequence-like Element of B
m is Relation-like NAT -defined NAT -valued Function-like finite FinSequence-like FinSubsequence-like Element of B
ProperPrefixes f is finite set
{f} is non empty trivial functional finite V37() 1 -element set
(ProperPrefixes f) \/ {f} is non empty finite set
m is set
t is Relation-like NAT -defined NAT -valued Function-like finite FinSequence-like FinSubsequence-like Element of B
m is Relation-like NAT -defined NAT -valued Function-like finite FinSequence-like FinSubsequence-like Element of B
B is non empty Tree-like set
g is non empty Branch-like Chain of B
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₁*>) where b₁ is epsilon-transitive epsilon-connected ordinal natural ext-real non negative V16() V20() finite cardinal Element of NAT : f ^ <*b₁*> in B } is set
m is Relation-like NAT -defined NAT -valued Function-like finite FinSequence-like FinSubsequence-like Element of B
t is Relation-like NAT -defined Function-like finite FinSequence-like FinSubsequence-like set
f ^ t is Relation-like NAT -defined Function-like finite FinSequence-like FinSubsequence-like set
fk is Relation-like NAT -defined NAT -valued Function-like finite FinSequence-like FinSubsequence-like FinSequence of NAT
fk | (Seg 1) is Relation-like NAT -defined Seg 1 -defined NAT -defined NAT -valued Function-like finite FinSubsequence-like Element of bool [:NAT,NAT:]
bool [:NAT,NAT:] is non empty non trivial non finite set
fm is Relation-like NAT -defined NAT -valued Function-like finite FinSequence-like FinSubsequence-like FinSequence of NAT
len fk is epsilon-transitive epsilon-connected ordinal natural ext-real non negative V16() V20() finite cardinal Element of NAT
len m is epsilon-transitive epsilon-connected ordinal natural ext-real non negative V16() V20() finite cardinal Element of NAT
len f 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 set
(len f) + n is epsilon-transitive epsilon-connected ordinal natural ext-real non negative V16() V20() finite cardinal Element of NAT
0 + 1 is epsilon-transitive epsilon-connected ordinal natural ext-real positive non negative V16() non empty V20() finite cardinal Element of NAT
(len f) + (len fk) 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*> is Relation-like NAT -defined NAT -valued non empty trivial Function-like constant finite 1 -element FinSequence-like FinSubsequence-like FinSequence of NAT
f ^ fm is Relation-like NAT -defined NAT -valued Function-like finite FinSequence-like FinSubsequence-like FinSequence of NAT
f ^ <*n*> is Relation-like NAT -defined NAT -valued non empty Function-like finite FinSequence-like FinSubsequence-like FinSequence of NAT
t9 is Relation-like NAT -defined NAT -valued Function-like finite FinSequence-like FinSubsequence-like Element of B
bool [:NAT,NAT:] is non empty non trivial non finite set
B is Relation-like NAT -defined NAT -valued Function-like V30( NAT , NAT ) Element of bool [:NAT,NAT:]
g is epsilon-transitive epsilon-connected ordinal natural ext-real non negative V16() V20() finite cardinal Element of NAT
B . g is epsilon-transitive epsilon-connected ordinal natural ext-real non negative V16() V20() finite cardinal Element of NAT
g + 1 is epsilon-transitive epsilon-connected ordinal natural ext-real positive non negative V16() non empty V20() finite cardinal Element of NAT
B . (g + 1) 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
B . f is epsilon-transitive epsilon-connected ordinal natural ext-real non negative V16() V20() finite cardinal Element of NAT
fk 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
t is epsilon-transitive epsilon-connected ordinal natural ext-real non negative V16() V20() finite cardinal Element of NAT
B . f 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
B . f is epsilon-transitive epsilon-connected ordinal natural ext-real non negative V16() V20() finite cardinal Element of NAT
B . 0 is epsilon-transitive epsilon-connected ordinal natural ext-real non negative V16() V20() finite cardinal Element of NAT
g is epsilon-transitive epsilon-connected ordinal natural ext-real non negative V16() V20() finite cardinal Element of NAT
B . g is epsilon-transitive epsilon-connected ordinal natural ext-real non negative V16() V20() finite cardinal Element of NAT
g is epsilon-transitive epsilon-connected ordinal natural ext-real non negative V16() V20() finite cardinal Element of NAT
B . 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
B . f is epsilon-transitive epsilon-connected ordinal natural ext-real non negative V16() V20() finite cardinal Element of NAT
rng B is Element of bool NAT
B . 0 is epsilon-transitive epsilon-connected ordinal natural ext-real non negative V16() V20() finite cardinal Element of NAT
g is set
f is epsilon-transitive epsilon-connected ordinal natural ext-real non negative V16() V20() finite cardinal Element of NAT
dom B is Element of bool NAT
g is epsilon-transitive epsilon-connected ordinal natural ext-real non negative V16() V20() finite cardinal set
g is epsilon-transitive epsilon-connected ordinal natural ext-real non negative V16() V20() finite cardinal set
dom B is Element of bool NAT
f is set
B . f is set
m is epsilon-transitive epsilon-connected ordinal natural ext-real non negative V16() V20() finite cardinal Element of NAT
B . 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
B . t is epsilon-transitive epsilon-connected ordinal natural ext-real non negative V16() V20() finite cardinal Element of NAT
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
F₁() is non empty set
F₂() is Relation-like F₁() -valued Function-like DecoratedTree-like () set
proj1 F₂() is non empty Tree-like () set
B is non empty Branch-like Chain of proj1 F₂()
g is set
f is Relation-like NAT -defined NAT -valued Function-like finite FinSequence-like FinSubsequence-like Element of proj1 F₂()
F₂() . f is Element of F₁()
f is Relation-like NAT -defined NAT -valued Function-like finite FinSequence-like FinSubsequence-like Element of proj1 F₂()
F₂() . f is Element of F₁()
succ f is finite Element of bool (proj1 F₂())
bool (proj1 F₂()) is non empty set
{ (f ^ <*b₁*>) where b₁ is epsilon-transitive epsilon-connected ordinal natural ext-real non negative V16() V20() finite cardinal Element of NAT : f ^ <*b₁*> in proj1 F₂() } is set
m is Relation-like NAT -defined NAT -valued Function-like finite FinSequence-like FinSubsequence-like Element of proj1 F₂()
F₂() . m is Element of F₁()
t is set
F₂() . {} is set
g is Relation-like NAT -defined NAT -valued Function-like finite FinSequence-like FinSubsequence-like Element of proj1 F₂()
F₂() . g is Element of F₁()
g is Relation-like Function-like set
proj1 g is set
proj2 g is set
g . 0 is set
g is Relation-like Function-like set
proj1 g is set
proj2 g is set
g . 0 is set
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
g . m is set
t is Relation-like NAT -defined NAT -valued Function-like finite FinSequence-like FinSubsequence-like Element of proj1 F₂()
F₂() . t is Element of F₁()
F₃((F₂() . t)) is epsilon-transitive epsilon-connected ordinal natural ext-real non negative V16() V20() finite cardinal Element of NAT
fk is set
f is Relation-like NAT -defined NAT -valued Function-like V30( NAT , NAT ) Element of bool [:NAT,NAT:]
f is Relation-like NAT -defined NAT -valued Function-like V30( NAT , NAT ) Element of bool [:NAT,NAT:]
m 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
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 epsilon-transitive epsilon-connected ordinal natural ext-real non negative V16() V20() finite cardinal Element of NAT
g . m is set
g . (m + 1) is set
t is Element of F₁()
F₃(t) is epsilon-transitive epsilon-connected ordinal natural ext-real non negative V16() V20() finite cardinal Element of NAT
fk is Element of F₁()
F₃(fk) 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 Function-like finite FinSequence-like FinSubsequence-like Element of proj1 F₂()
fm is Relation-like NAT -defined NAT -valued Function-like finite FinSequence-like FinSubsequence-like Element of proj1 F₂()
succ fm is finite Element of bool (proj1 F₂())
bool (proj1 F₂()) is non empty set
{ (fm ^ <*b₁*>) where b₁ is epsilon-transitive epsilon-connected ordinal natural ext-real non negative V16() V20() finite cardinal Element of NAT : fm ^ <*b₁*> in proj1 F₂() } is set
F₂() . fm is Element of F₁()
F₂() . n is Element of F₁()
m 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
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 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 Function-like finite FinSequence-like FinSubsequence-like Element of proj1 F₂()
t is Relation-like NAT -defined NAT -valued Function-like finite FinSequence-like FinSubsequence-like Element of proj1 F₂()
succ t is finite Element of bool (proj1 F₂())
bool (proj1 F₂()) is non empty set
{ (t ^ <*b₁*>) where b₁ is epsilon-transitive epsilon-connected ordinal natural ext-real non negative V16() V20() finite cardinal Element of NAT : t ^ <*b₁*> in proj1 F₂() } is set
F₂() . t is Element of F₁()
F₃((F₂() . t)) is epsilon-transitive epsilon-connected ordinal natural ext-real non negative V16() V20() finite cardinal Element of NAT
F₂() . fk is Element of F₁()
F₃((F₂() . fk)) 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
f . (m + 1) 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
fk is Relation-like NAT -defined NAT -valued Function-like finite FinSequence-like FinSubsequence-like Element of proj1 F₂()
t is Relation-like NAT -defined NAT -valued Function-like finite FinSequence-like FinSubsequence-like Element of proj1 F₂()
succ t is finite Element of bool (proj1 F₂())
bool (proj1 F₂()) is non empty set
{ (t ^ <*b₁*>) where b₁ is epsilon-transitive epsilon-connected ordinal natural ext-real non negative V16() V20() finite cardinal Element of NAT : t ^ <*b₁*> in proj1 F₂() } is set
F₂() . t is Element of F₁()
F₃((F₂() . t)) is epsilon-transitive epsilon-connected ordinal natural ext-real non negative V16() V20() finite cardinal Element of NAT
F₂() . fk is Element of F₁()
F₃((F₂() . fk)) 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
f . m is epsilon-transitive epsilon-connected ordinal natural ext-real non negative V16() V20() finite cardinal Element of NAT
m + 0 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 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 Function-like finite FinSequence-like FinSubsequence-like Element of proj1 F₂()
t is Relation-like NAT -defined NAT -valued Function-like finite FinSequence-like FinSubsequence-like Element of proj1 F₂()
succ t is finite Element of bool (proj1 F₂())
bool (proj1 F₂()) is non empty set
{ (t ^ <*b₁*>) where b₁ is epsilon-transitive epsilon-connected ordinal natural ext-real non negative V16() V20() finite cardinal Element of NAT : t ^ <*b₁*> in proj1 F₂() } is set
F₂() . t is Element of F₁()
F₃((F₂() . t)) is epsilon-transitive epsilon-connected ordinal natural ext-real non negative V16() V20() finite cardinal Element of NAT
F₂() . fk is Element of F₁()
F₃((F₂() . fk)) is epsilon-transitive epsilon-connected ordinal natural ext-real non negative V16() V20() finite cardinal Element of NAT