:: DTCONSTR semantic presentation

REAL is set

NAT is non empty non trivial V33() V34() V35() non finite V46() V47() Element of bool REAL

bool REAL is non empty set

RAT is set

{} is Relation-like non-empty empty-yielding NAT -defined RAT -valued Function-like one-to-one constant functional empty ext-real non positive non negative V32() V33() V34() V35() V37() V38() V39() V40() finite finite-yielding V45() V46() V48( {} ) FinSequence-like FinSubsequence-like FinSequence-membered constituted-Trees constituted-FinTrees constituted-DTrees Tree-yielding FinTree-yielding DTree-yielding V90() V91() V92() V93() set

the Relation-like non-empty empty-yielding NAT -defined RAT -valued Function-like one-to-one constant functional empty ext-real non positive non negative V32() V33() V34() V35() V37() V38() V39() V40() finite finite-yielding V45() V46() V48( {} ) FinSequence-like FinSubsequence-like FinSequence-membered constituted-Trees constituted-FinTrees constituted-DTrees Tree-yielding FinTree-yielding DTree-yielding V90() V91() V92() V93() set is Relation-like non-empty empty-yielding NAT -defined RAT -valued Function-like one-to-one constant functional empty ext-real non positive non negative V32() V33() V34() V35() V37() V38() V39() V40() finite finite-yielding V45() V46() V48( {} ) FinSequence-like FinSubsequence-like FinSequence-membered constituted-Trees constituted-FinTrees constituted-DTrees Tree-yielding FinTree-yielding DTree-yielding V90() V91() V92() V93() set

NAT is non empty non trivial V33() V34() V35() non finite V46() V47() set

bool NAT is non empty non trivial non finite set

bool NAT is non empty non trivial non finite set

K118(NAT) is V27() set

1 is non empty ext-real positive non negative V32() V33() V34() V35() V39() V40() finite V46() Element of NAT

{{},1} is non empty finite V45() 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

COMPLEX is set

INT is set

2 is non empty ext-real positive non negative V32() V33() V34() V35() V39() V40() finite V46() Element of NAT

3 is non empty ext-real positive non negative V32() V33() V34() V35() V39() V40() finite V46() Element of NAT

0 is Relation-like non-empty empty-yielding NAT -defined RAT -valued Function-like one-to-one constant functional empty ext-real non positive non negative V32() V33() V34() V35() V37() V38() V39() V40() finite finite-yielding V45() V46() V48( {} ) FinSequence-like FinSubsequence-like FinSequence-membered constituted-Trees constituted-FinTrees constituted-DTrees Tree-yielding FinTree-yielding DTree-yielding V90() V91() V92() V93() Element of NAT

Seg 1 is non empty trivial finite V48(1) Element of bool NAT

{ b

{1} is non empty trivial finite V45() V48(1) set

Seg 2 is non empty finite V48(2) Element of bool NAT

{ b

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

<*> NAT is Relation-like non-empty empty-yielding NAT -defined NAT -valued Function-like one-to-one constant functional empty proper ext-real non positive non negative V32() V33() V34() V35() V37() V38() V39() V40() finite finite-yielding V45() V46() V48( {} ) FinSequence-like FinSubsequence-like FinSequence-membered constituted-Trees constituted-FinTrees constituted-DTrees Tree-yielding FinTree-yielding DTree-yielding V90() V91() V92() V93() 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

height (elementary_tree 0) is ext-real non negative V32() V33() V34() V35() V39() V40() finite V46() Element of NAT

PN is non empty set

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

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

bool (Trees PN) is non empty set

O is Relation-like NAT -defined FinTrees PN -valued Function-like finite FinSequence-like FinSubsequence-like DTree-yielding FinSequence of FinTrees PN

PN is set

O is set

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

dom S is finite Element of bool NAT

S . O is set

rng S is finite set

PN is non empty set

O is functional non empty constituted-DTrees DTree-set of PN

S is Relation-like NAT -defined O -valued Function-like finite FinSequence-like FinSubsequence-like DTree-yielding FinSequence of O

PN is non empty set

O is functional non empty constituted-DTrees DTree-set of PN

bool O is non empty set

S is functional non empty constituted-DTrees Element of bool O

TSPN is Relation-like Function-like DecoratedTree-like Element of S

PN is non empty set

O is functional non empty constituted-DTrees DTree-set of PN

S is Relation-like NAT -defined O -valued Function-like finite FinSequence-like FinSubsequence-like DTree-yielding FinSequence of O

roots S is Relation-like NAT -defined Function-like finite FinSequence-like FinSubsequence-like set

TSPN is set

rng (roots S) is finite set

dom (roots S) is finite Element of bool NAT

PN is set

(roots S) . PN is set

dom S is finite Element of bool NAT

O is ext-real non negative V32() V33() V34() V35() V39() V40() finite V46() Element of NAT

S . O is Relation-like Function-like set

(roots S) . O is set

S is Relation-like Function-like DecoratedTree-like set

S . {} is set

nt is Relation-like PN -valued Function-like DecoratedTree-like set

dom nt is non empty Tree-like set

rtO is Relation-like NAT -defined NAT -valued Function-like finite FinSequence-like FinSubsequence-like V90() V91() V92() V93() Element of dom nt

nt . rtO is Element of PN

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

dom (roots {}) is finite Element of bool NAT

dom {} is Relation-like non-empty empty-yielding NAT -defined RAT -valued Function-like one-to-one constant functional empty proper ext-real non positive non negative V32() V33() V34() V35() V37() V38() V39() V40() finite finite-yielding V45() V46() V48( {} ) FinSequence-like FinSubsequence-like FinSequence-membered constituted-Trees constituted-FinTrees constituted-DTrees Tree-yielding FinTree-yielding DTree-yielding V90() V91() V92() V93() Element of bool NAT

PN is Relation-like Function-like DecoratedTree-like set

<*PN*> is Relation-like NAT -defined Function-like constant non empty trivial finite V48(1) FinSequence-like FinSubsequence-like DTree-yielding set

[1,PN] is V15() set

{1,PN} is non empty finite set

{{1,PN},{1}} is non empty finite V45() set

{[1,PN]} is Relation-like Function-like constant non empty trivial finite V48(1) set

roots <*PN*> is Relation-like NAT -defined Function-like finite FinSequence-like FinSubsequence-like set

PN . {} is set

<*(PN . {})*> is Relation-like NAT -defined Function-like constant non empty trivial finite V48(1) FinSequence-like FinSubsequence-like set

[1,(PN . {})] is V15() set

{1,(PN . {})} is non empty finite set

{{1,(PN . {})},{1}} is non empty finite V45() set

{[1,(PN . {})]} is Relation-like Function-like constant non empty trivial finite V48(1) set

dom <*PN*> is non empty trivial finite V48(1) Element of bool NAT

dom <*(PN . {})*> is non empty trivial finite V48(1) Element of bool NAT

<*PN*> . 1 is set

<*(PN . {})*> . 1 is set

O is ext-real non negative V32() V33() V34() V35() V39() V40() finite V46() Element of NAT

S is Relation-like Function-like DecoratedTree-like set

<*PN*> . O is set

<*(PN . {})*> . O is set

S . {} is set

PN is non empty set

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

bool (FinTrees PN) is non empty set

O is functional constituted-DTrees Element of bool (FinTrees PN)

S is Relation-like NAT -defined FinTrees PN -valued Function-like finite FinSequence-like FinSubsequence-like DTree-yielding FinSequence of O

(PN,(FinTrees PN),S) is Relation-like NAT -defined PN -valued Function-like finite FinSequence-like FinSubsequence-like FinSequence of PN

len (PN,(FinTrees PN),S) is ext-real non negative V32() V33() V34() V35() V39() V40() finite V46() Element of NAT

dom (PN,(FinTrees PN),S) is finite Element of bool NAT

dom S is finite Element of bool NAT

S . 1 is Relation-like Function-like set

TSPN is Relation-like PN -valued Function-like DecoratedTree-like Element of FinTrees PN

<*TSPN*> is Relation-like NAT -defined FinTrees PN -valued Function-like constant non empty trivial finite V48(1) FinSequence-like FinSubsequence-like DTree-yielding Element of (FinTrees PN) *

(FinTrees PN) * is functional non empty FinSequence-membered FinSequenceSet of FinTrees PN

[1,TSPN] is V15() set

{1,TSPN} is non empty finite set

{{1,TSPN},{1}} is non empty finite V45() set

{[1,TSPN]} is Relation-like Function-like constant non empty trivial finite V48(1) set

PN is Relation-like Function-like DecoratedTree-like set

O is Relation-like Function-like DecoratedTree-like set

<*PN,O*> is Relation-like NAT -defined Function-like non empty finite V48(2) FinSequence-like FinSubsequence-like DTree-yielding set

<*PN*> is Relation-like NAT -defined Function-like constant non empty trivial finite V48(1) FinSequence-like FinSubsequence-like DTree-yielding set

[1,PN] is V15() set

{1,PN} is non empty finite set

{{1,PN},{1}} is non empty finite V45() set

{[1,PN]} is Relation-like Function-like constant non empty trivial finite V48(1) set

<*O*> is Relation-like NAT -defined Function-like constant non empty trivial finite V48(1) FinSequence-like FinSubsequence-like DTree-yielding set

[1,O] is V15() set

{1,O} is non empty finite set

{{1,O},{1}} is non empty finite V45() set

{[1,O]} is Relation-like Function-like constant non empty trivial finite V48(1) set

<*PN*> ^ <*O*> is Relation-like NAT -defined Function-like non empty finite V48(1 + 1) FinSequence-like FinSubsequence-like DTree-yielding set

1 + 1 is non empty ext-real positive non negative V32() V33() V34() V35() V39() V40() finite V46() Element of NAT

roots <*PN,O*> is Relation-like NAT -defined Function-like finite FinSequence-like FinSubsequence-like set

PN . {} is set

O . {} is set

<*(PN . {}),(O . {})*> is Relation-like NAT -defined Function-like non empty finite V48(2) FinSequence-like FinSubsequence-like set

<*(PN . {})*> is Relation-like NAT -defined Function-like constant non empty trivial finite V48(1) FinSequence-like FinSubsequence-like set

[1,(PN . {})] is V15() set

{1,(PN . {})} is non empty finite set

{{1,(PN . {})},{1}} is non empty finite V45() set

{[1,(PN . {})]} is Relation-like Function-like constant non empty trivial finite V48(1) set

<*(O . {})*> is Relation-like NAT -defined Function-like constant non empty trivial finite V48(1) FinSequence-like FinSubsequence-like set

[1,(O . {})] is V15() set

{1,(O . {})} is non empty finite set

{{1,(O . {})},{1}} is non empty finite V45() set

{[1,(O . {})]} is Relation-like Function-like constant non empty trivial finite V48(1) set

<*(PN . {})*> ^ <*(O . {})*> is Relation-like NAT -defined Function-like non empty finite V48(1 + 1) FinSequence-like FinSubsequence-like set

len <*PN,O*> is non empty ext-real positive non negative V32() V33() V34() V35() V39() V40() finite V46() Element of NAT

len <*(PN . {}),(O . {})*> is non empty ext-real positive non negative V32() V33() V34() V35() V39() V40() finite V46() Element of NAT

<*PN,O*> . 1 is set

<*(PN . {}),(O . {})*> . 1 is set

<*PN,O*> . 2 is set

<*(PN . {}),(O . {})*> . 2 is set

dom <*PN,O*> is non empty finite V48(2) Element of bool NAT

dom <*(PN . {}),(O . {})*> is non empty finite V48(2) Element of bool NAT

S is ext-real non negative V32() V33() V34() V35() V39() V40() finite V46() Element of NAT

<*PN,O*> . S is set

<*(PN . {}),(O . {})*> . S is set

PN is set

O is set

[:PN,O:] is Relation-like set

S is Relation-like NAT -defined [:PN,O:] -valued Function-like finite FinSequence-like FinSubsequence-like FinSequence of [:PN,O:]

pr1 S is Relation-like Function-like set

dom (pr1 S) is set

dom S is finite Element of bool NAT

len S is ext-real non negative V32() V33() V34() V35() V39() V40() finite V46() Element of NAT

Seg (len S) is finite V48( len S) Element of bool NAT

{ b

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

rng TSPN is finite set

PN is set

dom TSPN is finite Element of bool NAT

O is set

TSPN . O is set

S . O is set

(S . O) `1 is set

pr2 S is Relation-like Function-like set

dom (pr2 S) is set

dom S is finite Element of bool NAT

len S is ext-real non negative V32() V33() V34() V35() V39() V40() finite V46() Element of NAT

Seg (len S) is finite V48( len S) Element of bool NAT

{ b

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

rng TSPN is finite set

PN is set

dom TSPN is finite Element of bool NAT

O is set

TSPN . O is set

S . O is set

(S . O) `2 is set

pr1 {} is Relation-like Function-like set

pr2 {} is Relation-like Function-like set

[:{},{}:] is Relation-like finite set

<*> [:{},{}:] is Relation-like non-empty empty-yielding NAT -defined [:{},{}:] -valued Function-like one-to-one constant functional empty ext-real non positive non negative V32() V33() V34() V35() V37() V38() V39() V40() finite finite-yielding V45() V46() V48( {} ) FinSequence-like FinSubsequence-like FinSequence-membered constituted-Trees constituted-FinTrees constituted-DTrees Tree-yielding FinTree-yielding DTree-yielding V90() V91() V92() V93() Element of [:{},{}:] *

[:{},{}:] * is functional non empty FinSequence-membered FinSequenceSet of [:{},{}:]

({},{},(<*> [:{},{}:])) is Relation-like non-empty empty-yielding NAT -defined {} -valued Function-like one-to-one constant functional empty ext-real non positive non negative V32() V33() V34() V35() V37() V38() V39() V40() finite finite-yielding V45() V46() V48( {} ) FinSequence-like FinSubsequence-like FinSequence-membered constituted-Trees constituted-FinTrees constituted-DTrees Tree-yielding FinTree-yielding DTree-yielding V90() V91() V92() V93() FinSequence of {}

dom ({},{},(<*> [:{},{}:])) is Relation-like non-empty empty-yielding NAT -defined RAT -valued Function-like one-to-one constant functional empty proper ext-real non positive non negative V32() V33() V34() V35() V37() V38() V39() V40() finite finite-yielding V45() V46() V48( {} ) FinSequence-like FinSubsequence-like FinSequence-membered constituted-Trees constituted-FinTrees constituted-DTrees Tree-yielding FinTree-yielding DTree-yielding V90() V91() V92() V93() Element of bool NAT

({},{},(<*> [:{},{}:])) is Relation-like non-empty empty-yielding NAT -defined {} -valued Function-like one-to-one constant functional empty ext-real non positive non negative V32() V33() V34() V35() V37() V38() V39() V40() finite finite-yielding V45() V46() V48( {} ) FinSequence-like FinSubsequence-like FinSequence-membered constituted-Trees constituted-FinTrees constituted-DTrees Tree-yielding FinTree-yielding DTree-yielding V90() V91() V92() V93() FinSequence of {}

dom ({},{},(<*> [:{},{}:])) is Relation-like non-empty empty-yielding NAT -defined RAT -valued Function-like one-to-one constant functional empty proper ext-real non positive non negative V32() V33() V34() V35() V37() V38() V39() V40() finite finite-yielding V45() V46() V48( {} ) FinSequence-like FinSubsequence-like FinSequence-membered constituted-Trees constituted-FinTrees constituted-DTrees Tree-yielding FinTree-yielding DTree-yielding V90() V91() V92() V93() Element of bool NAT

PN is non empty set

PN * is functional non empty FinSequence-membered FinSequenceSet of PN

[:PN,(PN *):] is Relation-like non empty set

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

O is Relation-like Element of bool [:PN,(PN *):]

DTConstrStr(# PN,O #) is strict DTConstrStr

F

F

[:F

bool [:F

PN is Relation-like Element of bool [:F

DTConstrStr(# F

O is non empty strict DTConstrStr

the carrier of O is non empty set

S is Element of the carrier of O

TSPN is Relation-like NAT -defined the carrier of O -valued Function-like finite FinSequence-like FinSubsequence-like FinSequence of the carrier of O

[:NAT, the carrier of O:] is Relation-like non empty non trivial non finite set

bool [:NAT, the carrier of O:] is non empty non trivial non finite set

[S,TSPN] is V15() Element of [: the carrier of O,(bool [:NAT, the carrier of O:]):]

[: the carrier of O,(bool [:NAT, the carrier of O:]):] is Relation-like non empty non trivial non finite set

{S,TSPN} is non empty finite set

{S} is non empty trivial finite V48(1) set

{{S,TSPN},{S}} is non empty finite V45() set

the Rules of O is Relation-like Element of bool [: the carrier of O,( the carrier of O *):]

the carrier of O * is functional non empty FinSequence-membered FinSequenceSet of the carrier of O

[: the carrier of O,( the carrier of O *):] is Relation-like non empty set

bool [: the carrier of O,( the carrier of O *):] is non empty set

F

PN is non empty strict DTConstrStr

the carrier of PN is non empty set

O is non empty strict DTConstrStr

the carrier of O is non empty set

S is set

TSPN is set

[S,TSPN] is V15() set

{S,TSPN} is non empty finite set

{S} is non empty trivial finite V48(1) set

{{S,TSPN},{S}} is non empty finite V45() set

the Rules of PN is Relation-like Element of bool [: the carrier of PN,( the carrier of PN *):]

the carrier of PN * is functional non empty FinSequence-membered FinSequenceSet of the carrier of PN

[: the carrier of PN,( the carrier of PN *):] is Relation-like non empty set

bool [: the carrier of PN,( the carrier of PN *):] is non empty set

PN is Element of the carrier of PN

O is Relation-like NAT -defined the carrier of PN -valued Function-like finite FinSequence-like FinSubsequence-like FinSequence of the carrier of PN

S is Element of the carrier of O

nt is Relation-like NAT -defined the carrier of O -valued Function-like finite FinSequence-like FinSubsequence-like FinSequence of the carrier of O

the Rules of O is Relation-like Element of bool [: the carrier of O,( the carrier of O *):]

the carrier of O * is functional non empty FinSequence-membered FinSequenceSet of the carrier of O

[: the carrier of O,( the carrier of O *):] is Relation-like non empty set

bool [: the carrier of O,( the carrier of O *):] is non empty set

PN is Element of the carrier of O

O is Relation-like NAT -defined the carrier of O -valued Function-like finite FinSequence-like FinSubsequence-like FinSequence of the carrier of O

S is Element of the carrier of PN

nt is Relation-like NAT -defined the carrier of PN -valued Function-like finite FinSequence-like FinSubsequence-like FinSequence of the carrier of PN

PN is non empty DTConstrStr

Terminals PN is set

NonTerminals PN is set

the carrier of PN is non empty set

{ b

{ b

O is set

S is Element of the carrier of PN

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

PN is Element of the carrier of PN

F

F

dom F

F

F

the carrier of F

[: the carrier of F

Terminals F

{ (root-tree [b

FinTrees [: the carrier of F

bool (FinTrees [: the carrier of F

Union F

TSPN is set

PN is set

O is Element of the carrier of F

S is Element of F

[O,S] is V15() Element of [: the carrier of F

{O,S} is non empty finite set

{O} is non empty trivial finite V48(1) set

{{O,S},{O}} is non empty finite V45() set

root-tree [O,S] is Relation-like [: the carrier of F

F

F

PN is ext-real non negative V32() V33() V34() V35() V39() V40() finite V46() Element of NAT

F

PN + 1 is non empty ext-real positive non negative V32() V33() V34() V35() V39() V40() finite V46() Element of NAT

F

O is set

(F

{ ([b

( b

(F

( b

S is Element of the carrier of F

nt is Relation-like NAT -defined F

roots nt is Relation-like NAT -defined Function-like finite FinSequence-like FinSubsequence-like set

pr1 (roots nt) is Relation-like Function-like set

pr2 (roots nt) is Relation-like Function-like set

F

[S,H

{S,F

{S} is non empty trivial finite V48(1) set

{{S,F

[S,H

x is Relation-like NAT -defined FinTrees [: the carrier of F

([: the carrier of F

( the carrier of F

rtO is Relation-like NAT -defined FinTrees [: the carrier of F

roots rtO is Relation-like NAT -defined Function-like finite FinSequence-like FinSubsequence-like set

pr1 (roots rtO) is Relation-like Function-like set

pr2 (roots rtO) is Relation-like Function-like set

F

[S,H

{S,F

{{S,F

[S,H

PN is set

F

TSPN is functional constituted-DTrees Element of bool (FinTrees [: the carrier of F

PN is Element of the carrier of F

F

[PN,F

{PN,F

{PN} is non empty trivial finite V48(1) set

{{PN,F

root-tree [PN,F

PN is Element of the carrier of F

O is Relation-like NAT -defined FinTrees [: the carrier of F

([: the carrier of F

( the carrier of F

( the carrier of F

dom O is finite Element of bool NAT

len O is ext-real non negative V32() V33() V34() V35() V39() V40() finite V46() Element of NAT

Seg (len O) is finite V48( len O) Element of bool NAT

{ b

rtO is ext-real non negative V32() V33() V34() V35() V39() V40() finite V46() set

O . rtO is Relation-like Function-like set

rng O is finite set

x is set

F

rtO is Relation-like NAT -defined NAT -valued Function-like finite FinSequence-like FinSubsequence-like V90() V91() V92() V93() FinSequence of NAT

dom rtO is finite Element of bool NAT

rng rtO is finite V102() V103() V104() V107() set

n is ext-real non negative V32() V33() V34() V35() V39() V40() finite V46() Element of NAT

x is ext-real non negative V32() V33() V34() V35() V39() V40() finite V46() Element of NAT

n is ext-real non negative V32() V33() V34() V35() V39() V40() finite V46() Element of NAT

x is ext-real non negative V32() V33() V34() V35() V39() V40() finite V46() Element of NAT

n is ext-real non negative V32() V33() V34() V35() V39() V40() finite V46() Element of NAT

x is ext-real non negative V32() V33() V34() V35() V39() V40() finite V46() Element of NAT

rng O is finite set

n is ext-real non negative V32() V33() V34() V35() V39() V40() finite V46() Element of NAT

F

n is set

tsg9 is set

O . tsg9 is Relation-like Function-like set

tsg9 is ext-real non negative V32() V33() V34() V35() V39() V40() finite V46() Element of NAT

rtO . tsg9 is ext-real non negative V32() V33() V34() V35() V39() V40() finite V46() set

f2 is ext-real non negative V32() V33() V34() V35() V39() V40() finite V46() Element of NAT

nt is ext-real non negative V32() V33() V34() V35() V39() V40() finite V46() set

f2 + nt is ext-real non negative V32() V33() V34() V35() V39() V40() finite V46() Element of NAT

{ ([b

( b

ts is ext-real non negative V32() V33() V34() V35() V39() V40() finite V46() Element of NAT

F

ts + 1 is non empty ext-real positive non negative V32() V33() V34() V35() V39() V40() finite V46() Element of NAT

F

(F

{ ([b

( b

(F

F

F

x is ext-real non negative V32() V33() V34() V35() V39() V40() finite V46() Element of NAT

F

x is ext-real non negative V32() V33() V34() V35() V39() V40() finite V46() Element of NAT

F

rng F

union (rng F

n is functional constituted-DTrees Element of bool (FinTrees [: the carrier of F

n * is functional non empty FinSequence-membered FinSequenceSet of n

n is Relation-like NAT -defined FinTrees [: the carrier of F

F

[PN,F

{PN,F

{PN} is non empty trivial finite V48(1) set

{{PN,F

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

[PN,F

{ ([b

( b

(F

( b

x + 1 is non empty ext-real positive non negative V32() V33() V34() V35() V39() V40() finite V46() Element of NAT

F

[PN,F

PN is functional constituted-DTrees Element of bool (FinTrees [: the carrier of F

O is set

<*> PN is Relation-like non-empty empty-yielding NAT -defined PN -valued Function-like one-to-one constant functional empty ext-real non positive non negative V32() V33() V34() V35() V37() V38() V39() V40() finite finite-yielding V45() V46() V48( {} ) FinSequence-like FinSubsequence-like FinSequence-membered constituted-Trees constituted-FinTrees constituted-DTrees Tree-yielding FinTree-yielding DTree-yielding V90() V91() V92() V93() Element of PN *

PN * is functional non empty FinSequence-membered FinSequenceSet of PN

S is Relation-like NAT -defined FinTrees [: the carrier of F

([: the carrier of F

( the carrier of F

roots S is Relation-like NAT -defined Function-like finite FinSequence-like FinSubsequence-like set

pr1 (roots S) is Relation-like Function-like set

pr2 (roots S) is Relation-like Function-like set

nt is Element of the carrier of F

rtO is Element of F

[nt,rtO] is V15() Element of [: the carrier of F

{nt,rtO} is non empty finite set

{nt} is non empty trivial finite V48(1) set

{{nt,rtO},{nt}} is non empty finite V45() set

root-tree [nt,rtO] is Relation-like [: the carrier of F

F

F

[nt,rtO] -tree S is Relation-like [: the carrier of F

O is ext-real non negative V32() V33() V34() V35() V39() V40() finite V46() Element of NAT

F

O + 1 is non empty ext-real positive non negative V32() V33() V34() V35() V39() V40() finite V46() Element of NAT

F

S is set

(F

{ ([b

( b

(F

( b

nt is Element of the carrier of F

rtO is Relation-like NAT -defined F

roots rtO is Relation-like NAT -defined Function-like finite FinSequence-like FinSubsequence-like set

pr1 (roots rtO) is Relation-like Function-like set

pr2 (roots rtO) is Relation-like Function-like set

F

[nt,H

{nt,F

{nt} is non empty trivial finite V48(1) set

{{nt,F

[nt,H

rng rtO is finite set

x is Relation-like NAT -defined FinTrees [: the carrier of F

([: the carrier of F

( the carrier of F

n is Relation-like NAT -defined FinTrees [: the carrier of F

([: the carrier of F

( the carrier of F

O is set

S is set

F

F

F

dom F

F

F

the carrier of F

[: the carrier of F

Terminals F

{ (root-tree [b

FinTrees [: the carrier of F

FinTrees the carrier of F

bool (FinTrees the carrier of F

Union F

{ (b

O is ext-real non negative V32() V33() V34() V35() V39() V40() finite V46() Element of NAT

O + 1 is non empty ext-real positive non negative V32() V33() V34() V35() V39() V40() finite V46() Element of NAT

F

F

(F

{ ([b

( b

(F

( b

bool (FinTrees [: the carrier of F

O is functional constituted-DTrees Element of bool (FinTrees [: the carrier of F

nt is set

rtO is Relation-like [: the carrier of F

rtO `1 is Relation-like the carrier of F

pr1 ( the carrier of F

[:[: the carrier of F

bool [:[: the carrier of F

rtO * (pr1 ( the carrier of F

rng rtO is set

dom (pr1 ( the carrier of F

dom (rtO `1) is non empty Tree-like set

dom rtO is non empty finite Tree-like set

nt is functional constituted-DTrees Element of bool (FinTrees the carrier of F

rtO is functional constituted-DTrees Element of bool (FinTrees the carrier of F

x is Element of the carrier of F

F

[x,F

{x,F

{x} is non empty trivial finite V48(1) set

{{x,F

root-tree [x,F

(root-tree [x,F

root-tree x is Relation-like the carrier of F

x is Element of the carrier of F

n is Relation-like NAT -defined FinTrees the carrier of F

( the carrier of F

dom n is finite Element of bool NAT

len n is ext-real non negative V32() V33() V34() V35() V39() V40() finite V46() Element of NAT

Seg (len n) is finite V48( len n) Element of bool NAT

{ b

n is ext-real non negative V32() V33() V34() V35() V39() V40() finite V46() set

n . n is Relation-like Function-like set

rng n is finite set

tsg9 is Relation-like [: the carrier of F

tsg9 `1 is Relation-like the carrier of F

n is Relation-like NAT -defined FinTrees [: the carrier of F

dom n is finite Element of bool NAT

rng n is finite set

tsg9 is set

tsg9 is set

n . tsg9 is Relation-like Function-like set

f2 is ext-real non negative V32() V33() V34() V35() V39() V40() finite V46() Element of NAT

n . f2 is Relation-like Function-like set

nt is Relation-like [: the carrier of F

nt `1 is Relation-like the carrier of F

dom ( the carrier of F

tsg9 is Relation-like NAT -defined FinTrees [: the carrier of F

([: the carrier of F

( the carrier of F

dom ( the carrier of F

dom ([: the carrier of F

tsg9 is ext-real non negative V32() V33() V34() V35() V39() V40() finite V46() set

tsg9 . tsg9 is Relation-like Function-like set

n . tsg9 is Relation-like Function-like set

f2 is Relation-like [: the carrier of F

f2 `1 is Relation-like the carrier of F

dom f2 is non empty Tree-like set

( the carrier of F

nt is Relation-like NAT -defined NAT -valued Function-like finite FinSequence-like FinSubsequence-like V90() V91() V92() V93() Element of dom f2

f2 . nt is Element of [: the carrier of F

(f2 . nt) `1 is Element of the carrier of F

ts is Relation-like Function-like DecoratedTree-like set

ts . {} is set

([: the carrier of F

( the carrier of F

ts is Relation-like Function-like DecoratedTree-like set

ts . {} is set

roots tsg9 is Relation-like NAT -defined Function-like finite FinSequence-like FinSubsequence-like set

pr1 (roots tsg9) is Relation-like Function-like set

pr2 (roots tsg9) is Relation-like Function-like set

F

[x,H

{x,F

{x} is non empty trivial finite V48(1) set

{{x,F

[x,H

rng tsg9 is finite set

Trees [: the carrier of F

rng n is finite set

Trees the carrier of F

nt is ext-real non negative V32() V33() V34() V35() V39() V40() finite V46() Element of NAT

dom tsg9 is finite Element of bool NAT

tsg9 . nt is Relation-like Function-like set

n . nt is Relation-like Function-like set

ts is Relation-like [: the carrier of F

ts `1 is Relation-like the carrier of F

p21 is Relation-like [: the carrier of F

p21 `1 is Relation-like the carrier of F

tsg9 is Relation-like NAT -defined Trees [: the carrier of F

[x,H

([x,H

f2 is Relation-like NAT -defined Trees the carrier of F

x -tree f2 is Relation-like the carrier of F

x -tree n is Relation-like the carrier of F

x is functional constituted-DTrees Element of bool (FinTrees the carrier of F

n is set

n is Relation-like [: the carrier of F

n `1 is Relation-like the carrier of F

{ b

tsg9 is set

f2 is Relation-like [: the carrier of F

f2 `1 is Relation-like the carrier of F

f2 is Element of the carrier of F

root-tree f2 is Relation-like the carrier of F

F

[f2,F

{f2,F

{f2} is non empty trivial finite V48(1) set

{{f2,F

root-tree [f2,F

(root-tree [f2,F

tsg9 is functional constituted-DTrees Element of bool (FinTrees [: the carrier of F

f2 is Element of the carrier of F

nt is Relation-like NAT -defined FinTrees [: the carrier of F

([: the carrier of F

( the carrier of F

dom nt is finite Element of bool NAT

( the carrier of F

F

[f2,F

{f2,F

{f2} is non empty trivial finite V48(1) set

{{f2,F

[f2,F

([f2,F

ts is Relation-like NAT -defined FinTrees the carrier of F

dom ts is finite Element of bool NAT

f2 -tree ts is Relation-like the carrier of F

rng ts is finite set

p21 is set

k is set

ts . k is Relation-like Function-like set

p1k is ext-real non negative V32() V33() V34() V35() V39() V40() finite V46() Element of NAT

nt . p1k is Relation-like Function-like set

rng nt is finite set

p2k is Relation-like [: the carrier of F

p2k `1 is Relation-like the carrier of F

c

c

p21 is Relation-like NAT -defined FinTrees the carrier of F

( the carrier of F

dom ( the carrier of F

dom p21 is finite Element of bool NAT

dom ( the carrier of F

dom ([: the carrier of F

k is ext-real non negative V32() V33() V34() V35() V39() V40() finite V46() set

nt . k is Relation-like Function-like set

rng nt is finite set

p21 . k is Relation-like Function-like set

p1k is Relation-like [: the carrier of F

p1k `1 is Relation-like the carrier of F

dom p1k is non empty finite Tree-like set

( the carrier of F

p2k is Relation-like NAT -defined NAT -valued Function-like finite FinSequence-like FinSubsequence-like V90() V91() V92() V93() Element of dom p1k

p1k . p2k is Element of [: the carrier of F

(p1k . p2k) `1 is Element of the carrier of F

c

c

c

c

([: the carrier of F

( the carrier of F

c

c

roots nt is Relation-like NAT -defined Function-like finite FinSequence-like FinSubsequence-like set

pr1 (roots nt) is Relation-like Function-like set

pr2 (roots nt) is Relation-like Function-like set

F

[f2,H

{f2,F

{{f2,F

[f2,H

f2 is Relation-like [: the carrier of F

f2 `1 is Relation-like the carrier of F

F

F

dom F

F

F

the carrier of F

[: the carrier of F

Terminals F

{ (root-tree [b

FinTrees [: the carrier of F

Union F

PN is Relation-like [: the carrier of F

dom PN is non empty finite Tree-like set

height (dom PN) is ext-real non negative V32() V33() V34() V35() V39() V40() finite V46() Element of NAT

O is Element of the carrier of F

S is Element of F

[O,S] is V15() Element of [: the carrier of F

{O,S} is non empty finite set

{O} is non empty trivial finite V48(1) set

{{O,S},{O}} is non empty finite V45() set

root-tree [O,S] is Relation-like [: the carrier of F

F

F

O is ext-real non negative V32() V33() V34() V35() V39() V40() finite V46() Element of NAT

F

O + 1 is non empty ext-real positive non negative V32() V33() V34() V35() V39() V40() finite V46() Element of NAT

F

(F

{ ([b

( b

(F

( b

S is Element of the carrier of F

nt is Relation-like NAT -defined F

roots nt is Relation-like NAT -defined Function-like finite FinSequence-like FinSubsequence-like set

pr1 (roots nt) is Relation-like Function-like set

pr2 (roots nt) is Relation-like Function-like set

F

[S,H

{S,F

{S} is non empty trivial finite V48(1) set

{{S,F

[S,H

PN . {} is set

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

rtO is Relation-like NAT -defined FinTrees [: the carrier of F

([: the carrier of F

( the carrier of F

F

[S,F

{S,F

{{S,F

root-tree [S,F

rtO is Relation-like NAT -defined FinTrees [: the carrier of F

([: the carrier of F

( the carrier of F

O is set

F

PN is ext-real non negative V32() V33() V34() V35() V39() V40() finite V46() Element of NAT

F

PN + 1 is non empty ext-real positive non negative V32() V33() V34() V35() V39() V40() finite V46() Element of NAT

F

O is Relation-like [: the carrier of F

dom O is non empty finite Tree-like set

height (dom O) is ext-real non negative V32() V33() V34() V35() V39() V40() finite V46() Element of NAT

(F

{ ([b

( b

(F

( b

S is Element of the carrier of F

nt is Relation-like NAT -defined F

roots nt is Relation-like NAT -defined Function-like finite FinSequence-like FinSubsequence-like set

pr1 (roots nt) is Relation-like Function-like set

pr2 (roots nt) is Relation-like Function-like set

F

[S,H

{S,F

{S} is non empty trivial finite V48(1) set

{{S,F

[S,H

x is Relation-like NAT -defined FinTrees [: the carrier of F

([: the carrier of F

( the carrier of F

rtO is Relation-like NAT -defined FinTrees [: the carrier of F

doms rtO is Relation-like NAT -defined FinTrees -valued Function-like finite FinSequence-like FinSubsequence-like Tree-yielding FinTree-yielding FinSequence of FinTrees

tree (doms rtO) is non empty finite Tree-like set

x is non empty finite Tree-like set

rng (doms rtO) is finite set

dom (doms rtO) is finite Element of bool NAT

n is set

(doms rtO) . n is set

dom rtO is finite Element of bool NAT

rtO . n is Relation-like Function-like set

rng rtO is finite set

n is Relation-like [: the carrier of F

dom n is non empty finite Tree-like set

height x is ext-real non negative V32() V33() V34() V35() V39() V40() finite V46() Element of NAT

S is set

F

S is ext-real non negative V32() V33() V34() V35() V39() V40() finite V46() set

F

{ ([b

( b

nt is ext-real non negative V32() V33() V34() V35() V39() V40() finite V46() Element of NAT

F

nt + 1 is non empty ext-real positive non negative V32() V33() V34() V35() V39() V40() finite V46() Element of NAT

F

(F

{ ([b

( b

(F

0 + (PN + 1) is non empty ext-real positive non negative V32() V33() V34() V35() V39() V40() finite V46() Element of NAT

F

nt is ext-real non negative V32() V33() V34() V35() V39() V40() finite V46() set

nt + 1 is non empty ext-real positive non negative V32() V33() V34() V35() V39() V40() finite V46() Element of NAT

nt is ext-real non negative V32() V33() V34() V35() V39() V40() finite V46() set

nt + 1 is non empty ext-real positive non negative V32() V33() V34() V35() V39() V40() finite V46() Element of NAT