:: TREES_9 semantic presentation

REAL is set

bool REAL is non empty set

bool NAT is non empty non trivial non finite set
bool NAT is non empty non trivial non finite set

{{},1} is non empty finite V37() set
Trees is non empty constituted-Trees set
bool Trees is non empty set

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

is Relation-like non empty non trivial non finite set

^ 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

B is non empty Tree-like set
g is non empty finite Tree-like set

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

succ m is Element of bool B
bool B is non empty set
{ (m ^ <*b1*>) where b1 is epsilon-transitive epsilon-connected ordinal natural ext-real non negative V16() V20() finite cardinal Element of NAT : m ^ <*b1*> in B } is set
fk is set
fm is set
t . fm is set

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

fk is set

fm is set
t . fk is set
t . fm is set

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

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

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

B is set

B . f is set
g . f is set

g . (B + 1) is set

g is set

f is set
B . f is set

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

(B | ()) . g is set

B . ({} ^ g) is set
B . g is set
B is non empty Tree-like set

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

proj1 B is non empty Tree-like set

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

(() | 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

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

proj1 B is non empty Tree-like set
Leaves () is Element of bool ()
bool () is non empty set

B is non empty Tree-like set
Leaves B is Element of bool B
bool B is non empty set

B | g is non empty Tree-like set

proj1 B is non empty Tree-like set
Leaves () is Element of bool ()
bool () is non empty set

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

bool is non empty finite V37() set

bool is non empty finite V37() set

proj1 B is non empty Tree-like set

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

B . {} is set

{(B . {})} is non empty trivial finite 1 -element set
[:,{(B . {})}:] is Relation-like non empty finite set
bool [:,{(B . {})}:] is non empty finite V37() set

B is set

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

bool is non empty finite V37() set

B is non empty Tree-like set

succ f is Element of bool B
bool B is non empty set
{ (f ^ <*b1*>) where b1 is epsilon-transitive epsilon-connected ordinal natural ext-real non negative V16() V20() finite cardinal Element of NAT : f ^ <*b1*> in B } is set
g is non empty Tree-like finite-order set

succ m is finite Element of bool g
bool g is non empty set
{ (m ^ <*b1*>) where b1 is epsilon-transitive epsilon-connected ordinal natural ext-real non negative V16() V20() finite cardinal Element of NAT : m ^ <*b1*> in g } is set

proj1 B is non empty Tree-like set

proj1 B is non empty Tree-like set

proj1 B is non empty Tree-like set

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

succ g is Element of bool B
bool B is non empty set
{ (g ^ <*b1*>) where b1 is epsilon-transitive epsilon-connected ordinal natural ext-real non negative V16() V20() finite cardinal Element of NAT : g ^ <*b1*> in B } is set
F2() is finite set

proj1 B is set

F1(g) is set

F1((g + 1)) is set

proj1 f is set
{ b1 where b1 is epsilon-transitive epsilon-connected ordinal natural ext-real non negative V16() V20() finite cardinal Element of NAT : not g + 1 <= b1 } is set
proj2 f is set
m is set
t is set
f . t is set

F1(fk) is set
m is set

F1(t) is set
f . t is set
m is set
t is set
f . m is set
f . t is set
F1(m) is set
F1(t) is set

{ b1 where b1 is epsilon-transitive epsilon-connected ordinal natural ext-real non negative V16() V20() finite cardinal Element of NAT : not card F2() <= b1 } is set
g is set
f is set
B . g is set
B . f is set
F1(g) is set
F1(f) is set

proj2 B is set

F1(f) is set
F1((card F2())) is set
{F1((card F2()))} is non empty trivial finite 1 -element set
F2() \ {F1((card F2()))} is finite Element of bool F2()
bool F2() is non empty finite V37() set
m is set
t is set
B . t is set

F1(fk) is set
g is finite set

card (F2() \ {F1((card F2()))}) is epsilon-transitive epsilon-connected ordinal natural ext-real non negative V16() V20() finite cardinal Element of NAT

(card F2()) - (card {F1((card F2()))}) is ext-real V16() V20() set
(card g) - 1 is ext-real V16() V20() set

((card g) - 1) + 1 is ext-real V16() V20() set
F1(0) is set
f is non empty set
the Element of f is Element of f

F1(t) is set

F1(f) is set

F1(m) is set
B is non empty Tree-like () set

succ g is finite Element of bool B
bool B is non empty set
{ (g ^ <*b1*>) where b1 is epsilon-transitive epsilon-connected ordinal natural ext-real non negative V16() V20() finite cardinal Element of NAT : g ^ <*b1*> in B } is set

f is set

(g ^ <*m*>) . ((len g) + 1) is set
B is non empty Tree-like () set

succ g is finite Element of bool B
bool B is non empty set
{ (g ^ <*b1*>) where b1 is epsilon-transitive epsilon-connected ordinal natural ext-real non negative V16() V20() finite cardinal Element of NAT : g ^ <*b1*> in B } is set

m is set

t is set
f . m is set
f . t is set

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

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

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

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

f . (m + 1) is set

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

m is set

f . (t + 1) is set

rng m is finite Element of bool B
t is set

m . (fk + 1) is set

m . (t + 1) is set

rng f is finite Element of bool B

rng m is finite Element of bool B

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

f . t is set

m . t is set

proj1 B is non empty Tree-like () set

rng ((),f) is finite Element of bool ()
bool () is non empty set

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

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

B . {} is set
proj1 B is non empty Tree-like () set
() -level 1 is Level of proj1 B
{ } is set

succ g is finite Element of bool ()
bool () is non empty set
{ (g ^ <*b1*>) where b1 is epsilon-transitive epsilon-connected ordinal natural ext-real non negative V16() V20() finite cardinal Element of NAT : g ^ <*b1*> in proj1 B } is set
f is finite set

t is set

t9 is set

proj1 t is set

fm is set
dom fk is finite Element of bool NAT
fk . fm is set

succ m is finite Element of bool ()
{ (m ^ <*b1*>) where b1 is epsilon-transitive epsilon-connected ordinal natural ext-real non negative V16() V20() finite cardinal Element of NAT : m ^ <*b1*> in proj1 B } is set

n is set

dom fm is finite Element of bool NAT
fm . (q + 1) is set
(doms fm) . (q + 1) is set

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

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

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

fm . (t9 + 1) is set

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

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

fm . (n + 1) is set

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

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

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

B is non empty set

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

proj1 B is non empty Tree-like set
{ (B | b1) where b1 is Relation-like NAT -defined NAT -valued Function-like finite FinSequence-like FinSubsequence-like Element of proj1 B : verum } is set

(B) is set
proj1 B is non empty Tree-like set
{ (B | b1) where b1 is Relation-like NAT -defined NAT -valued Function-like finite FinSequence-like FinSubsequence-like Element of proj1 B : verum } is set

m is non empty set
t is set

B is non empty set

(g) is non empty functional constituted-DTrees set
proj1 g is non empty Tree-like set
{ (g | b1) where b1 is Relation-like NAT -defined NAT -valued Function-like finite FinSequence-like FinSubsequence-like Element of proj1 g : verum } is set
Trees B is non empty functional constituted-DTrees DTree-set of B
bool () is non empty set
f is set

B is non empty set

(g) is non empty functional constituted-DTrees set
proj1 g is non empty finite Tree-like finite-order () set
{ (g | b1) where b1 is Relation-like NAT -defined NAT -valued Function-like finite FinSequence-like FinSubsequence-like Element of proj1 g : verum } is set

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

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

(B) is non empty functional constituted-DTrees set
proj1 B is non empty finite Tree-like finite-order () set
{ (B | b1) where b1 is Relation-like NAT -defined NAT -valued Function-like finite FinSequence-like FinSubsequence-like Element of proj1 B : verum } is set

proj1 m is non empty Tree-like set
B is set

(g) is non empty functional constituted-DTrees set
proj1 g is non empty Tree-like set
{ (g | b1) where b1 is Relation-like NAT -defined NAT -valued Function-like finite FinSequence-like FinSubsequence-like Element of proj1 g : verum } is set
f is set

(m) is non empty functional constituted-DTrees set
{ (m | b1) where b1 is Relation-like NAT -defined NAT -valued Function-like finite FinSequence-like FinSubsequence-like Element of proj1 m : verum } is set

(B) is non empty functional constituted-DTrees set
proj1 B is non empty Tree-like set
{ (B | b1) where b1 is Relation-like NAT -defined NAT -valued Function-like finite FinSequence-like FinSubsequence-like Element of proj1 B : verum } is set

(B) is non empty functional constituted-DTrees set
proj1 B is non empty Tree-like set
{ (B | b1) where b1 is Relation-like NAT -defined NAT -valued Function-like finite FinSequence-like FinSubsequence-like Element of proj1 B : verum } is set

(g) is non empty functional constituted-DTrees set
proj1 g is non empty Tree-like set
{ (g | b1) where b1 is Relation-like NAT -defined NAT -valued Function-like finite FinSequence-like FinSubsequence-like Element of proj1 g : verum } is set

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

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

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

proj1 B is non empty Tree-like set
(B) is non empty functional constituted-DTrees set
{ (B | b1) where b1 is Relation-like NAT -defined NAT -valued Function-like finite FinSequence-like FinSubsequence-like Element of proj1 B : verum } is set

((B | g)) is non empty functional constituted-DTrees set
proj1 (B | g) is non empty Tree-like set
{ ((B | g) | b1) where b1 is Relation-like NAT -defined NAT -valued Function-like finite FinSequence-like FinSubsequence-like Element of proj1 (B | g) : verum } is set
f is set

() | g is non empty Tree-like set

proj1 B is non empty Tree-like set
{ [b1,(B | b1)] where b1 is Relation-like NAT -defined NAT -valued Function-like finite FinSequence-like FinSubsequence-like Element of proj1 B : verum } is set
(B) is non empty functional constituted-DTrees set
{ (B | b1) where b1 is Relation-like NAT -defined NAT -valued Function-like finite FinSequence-like FinSubsequence-like Element of proj1 B : verum } is set
[:(),(B):] is Relation-like non empty set
bool [:(),(B):] is non empty set
f is 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 proj1 B -defined (B) -valued Element of bool [:(),(B):]
proj1 B is non empty Tree-like set
(B) is non empty functional constituted-DTrees set
{ (B | b1) where b1 is Relation-like NAT -defined NAT -valued Function-like finite FinSequence-like FinSubsequence-like Element of proj1 B : verum } is set
[:(),(B):] is Relation-like non empty set
bool [:(),(B):] is non empty set
{ [b1,(B | b1)] where b1 is Relation-like NAT -defined NAT -valued Function-like finite FinSequence-like FinSubsequence-like Element of proj1 B : verum } is set

[ the Relation-like NAT -defined NAT -valued Function-like finite FinSequence-like FinSubsequence-like Element of proj1 B,()] is non empty V27() set
{ the Relation-like NAT -defined NAT -valued Function-like finite FinSequence-like FinSubsequence-like Element of proj1 B,()} is non empty functional finite set
{} 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,()},{}} is non empty finite V37() set

proj1 m is non empty Tree-like set
B is set

(g) is Relation-like proj1 g -defined (g) -valued non empty Element of bool [:(),(g):]
proj1 g is non empty Tree-like set
(g) is non empty functional constituted-DTrees set
{ (g | b1) where b1 is Relation-like NAT -defined NAT -valued Function-like finite FinSequence-like FinSubsequence-like Element of proj1 g : verum } is set
[:(),(g):] is Relation-like non empty set
bool [:(),(g):] is non empty set
{ [b1,(g | b1)] where b1 is Relation-like NAT -defined NAT -valued Function-like finite FinSequence-like FinSubsequence-like Element of proj1 g : verum } is set
f is set

[t,(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 [:(),(m):]
(m) is non empty functional constituted-DTrees set
{ (m | b1) where b1 is Relation-like NAT -defined NAT -valued Function-like finite FinSequence-like FinSubsequence-like Element of proj1 m : verum } is set
[:(),(m):] is Relation-like non empty set
bool [:(),(m):] is non empty set
{ [b1,(m | b1)] where b1 is Relation-like NAT -defined NAT -valued Function-like finite FinSequence-like FinSubsequence-like Element of proj1 m : verum } is set

[{},B] is 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 [:(),(B):]
proj1 B is non empty Tree-like set
(B) is non empty functional constituted-DTrees set
{ (B | b1) where b1 is Relation-like NAT -defined NAT -valued Function-like finite FinSequence-like FinSubsequence-like Element of proj1 B : verum } is set
[:(),(B):] is Relation-like non empty set
bool [:(),(B):] is non empty set
{ [b1,(B | b1)] where b1 is Relation-like NAT -defined NAT -valued Function-like finite FinSequence-like FinSubsequence-like Element of proj1 B : verum } is set

(B) is Relation-like proj1 B -defined (B) -valued non empty Element of bool [:(),(B):]
proj1 B is non empty Tree-like set
(B) is non empty functional constituted-DTrees set
{ (B | b1) where b1 is Relation-like NAT -defined NAT -valued Function-like finite FinSequence-like FinSubsequence-like Element of proj1 B : verum } is set
[:(),(B):] is Relation-like non empty set
bool [:(),(B):] is non empty set
{ [b1,(B | b1)] where b1 is Relation-like NAT -defined NAT -valued Function-like finite FinSequence-like FinSubsequence-like Element of proj1 B : verum } is set

(g) is Relation-like proj1 g -defined (g) -valued non empty Element of bool [:(),(g):]
proj1 g is non empty Tree-like set
(g) is non empty functional constituted-DTrees set
{ (g | b1) where b1 is Relation-like NAT -defined NAT -valued Function-like finite FinSequence-like FinSubsequence-like Element of proj1 g : verum } is set
[:(),(g):] is Relation-like non empty set
bool [:(),(g):] is non empty set
{ [b1,(g | b1)] where b1 is Relation-like NAT -defined NAT -valued Function-like finite FinSequence-like FinSubsequence-like Element of proj1 g : verum } is set
[{},B] is non empty V27() set
{{},B} is non empty functional finite set
{{{},B},} is non empty finite V37() set

[f,(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

proj1 B is non empty Tree-like set
Leaves () is Element of bool ()
bool () is non empty set
g is set
{ (B | b1) where b1 is Relation-like NAT -defined NAT -valued Function-like finite FinSequence-like FinSubsequence-like Element of proj1 B : ( not b1 in Leaves () or B . b1 in g ) } is set
(B) is non empty functional constituted-DTrees set
{ (B | b1) where b1 is Relation-like NAT -defined NAT -valued Function-like finite FinSequence-like FinSubsequence-like Element of proj1 B : verum } is set
bool (B) is non empty set
m is set

B . t is set

proj1 t is non empty Tree-like set
B is set

f is set
(g,f) is functional constituted-DTrees Element of bool (g)
(g) is non empty functional constituted-DTrees set
proj1 g is non empty Tree-like set
{ (g | b1) where b1 is Relation-like NAT -defined NAT -valued Function-like finite FinSequence-like FinSubsequence-like Element of proj1 g : verum } is set
bool (g) is non empty set
Leaves () is Element of bool ()
bool () is non empty set
{ (g | b1) where b1 is Relation-like NAT -defined NAT -valued Function-like finite FinSequence-like FinSubsequence-like Element of proj1 g : ( not b1 in Leaves () or g . b1 in f ) } is set
m is set

Leaves () is Element of bool ()
bool () is non empty set
t . fm is set
fk is set
(t,fk) is functional constituted-DTrees Element of bool (t)
(t) is non empty functional constituted-DTrees set
{ (t | b1) where b1 is Relation-like NAT -defined NAT -valued Function-like finite FinSequence-like FinSubsequence-like Element of proj1 t : verum } is set
bool (t) is non empty set
{ (t | b1) where b1 is Relation-like NAT -defined NAT -valued Function-like finite FinSequence-like FinSubsequence-like Element of proj1 t : ( not b1 in Leaves () or t . b1 in fk ) } is set

B . {} is set
g is set
(B,g) is functional constituted-DTrees Element of bool (B)
(B) is non empty functional constituted-DTrees set
proj1 B is non empty Tree-like set
{ (B | b1) where b1 is Relation-like NAT -defined NAT -valued Function-like finite FinSequence-like FinSubsequence-like Element of proj1 B : verum } is set
bool (B) is non empty set
Leaves () is Element of bool ()
bool () is non empty set
{ (B | b1) where b1 is Relation-like NAT -defined NAT -valued Function-like finite FinSequence-like FinSubsequence-like Element of proj1 B : ( not b1 in Leaves () or B . b1 in g ) } is set

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

B . fk 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 finite Tree-like finite-order () set
{ (B | b1) where b1 is Relation-like NAT -defined NAT -valued Function-like finite FinSequence-like FinSubsequence-like Element of proj1 B : verum } is set
bool (B) is non empty set
Leaves () is non empty finite Element of bool ()
bool () is non empty finite V37() set
{ (B | b1) where b1 is Relation-like NAT -defined NAT -valued Function-like finite FinSequence-like FinSubsequence-like Element of proj1 B : ( not b1 in Leaves () or B . b1 in g ) } is set
(B) * is non empty functional FinSequence-membered M8((B))
[:(B,g),((B) *):] is Relation-like set
bool [:(B,g),((B) *):] is non empty set
f is set

fm is set

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

n . (n + 1) is set

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

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

n is set

t . {} is 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 set

fm . {} is 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)

fk . {} is set

B is non empty functional constituted-DTrees set
{ (b1 | b2) where b1 is Relation-like Function-like DecoratedTree-like Element of B, b2 is