:: 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₁ where b₁ is ext-real non negative V32() V33() V34() V35() V39() V40() finite V46() Element of NAT : ( 1 <= b₁ & b₁ <= 1 ) } is set
{1} is non empty trivial finite V45() V48(1) set
Seg 2 is non empty finite V48(2) Element of bool NAT
{ b₁ where b₁ is ext-real non negative V32() V33() V34() V35() V39() V40() finite V46() Element of NAT : ( 1 <= b₁ & b₁ <= 2 ) } is set
{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₁ where b₁ is ext-real non negative V32() V33() V34() V35() V39() V40() finite V46() Element of NAT : ( 1 <= b₁ & b₁ <= len S ) } is set
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<sub>1</sub> where b<sub>1</sub> is ext-real non negative V32() V33() V34() V35() V39() V40() finite V46() Element of NAT : ( 1 <= b<sub>1</sub> & b<sub>1</sub> <= len S ) } is set
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₁() is non empty set
F₁() * is functional non empty FinSequence-membered FinSequenceSet of F₁()
[:F₁(),(F₁() *):] is Relation-like non empty set
bool [:F₁(),(F₁() *):] is non empty set
PN is Relation-like Element of bool [:F₁(),(F₁() *):]
DTConstrStr(# F₁(),PN #) is non empty strict DTConstrStr
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₁() is non empty set
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₁ where b₁ is Element of the carrier of PN : for b₂ being Relation-like NAT -defined Function-like finite FinSequence-like FinSubsequence-like set holds not b₁ ==> b₂ } is set
{ b₁ where b₁ is Element of the carrier of PN : ex b₂ being Relation-like NAT -defined Function-like finite FinSequence-like FinSubsequence-like set st b₁ ==> b₂ } is set
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₃() is non empty set
F₁() is Relation-like Function-like set
dom F₁() is set
F₁() . 0 is set
F₂() is non empty DTConstrStr
the carrier of F₂() is non empty set
[: the carrier of F₂(),F₃():] is Relation-like non empty set
Terminals F₂() is set
{ (root-tree [b₁,b₂]) where b₁ is Element of the carrier of F₂(), b₂ is Element of F₃() : ( ( b₁ in Terminals F₂() & b₂ = F₄(b₁) ) or ( b₁ ==> {} & b₂ = F₅(b₁,{},{}) ) ) } is set
FinTrees [: the carrier of F₂(),F₃():] is functional non empty constituted-DTrees DTree-set of [: the carrier of F₂(),F₃():]
bool (FinTrees [: the carrier of F₂(),F₃():]) is non empty set
Union F₁() is set
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₂(),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₃():] -valued Function-like DecoratedTree-like Element of FinTrees [: the carrier of F₂(),F₃():]
F₄(O) is Element of F₃()
F₅(O,{},{}) is Element of F₃()
PN is ext-real non negative V32() V33() V34() V35() V39() V40() finite V46() Element of NAT
F₁() . PN is set
PN + 1 is non empty ext-real positive non negative V32() V33() V34() V35() V39() V40() finite V46() Element of NAT
F₁() . (PN + 1) is set
O is set
(F₁() . PN) * is functional non empty FinSequence-membered FinSequenceSet of F₁() . PN
{ ([b₁,H₃(b₁,b₂)] -tree b₂) where b₁ is Element of the carrier of F₂(), b₂ is Relation-like NAT -defined F₁() . PN -valued Function-like finite FinSequence-like FinSubsequence-like Element of (F₁() . PN) * : ex b₃ being Relation-like NAT -defined FinTrees [: the carrier of F₂(),F₃():] -valued Function-like finite FinSequence-like FinSubsequence-like DTree-yielding FinSequence of FinTrees [: the carrier of F₂(),F₃():] st
( b₂ = b₃ & b₁ ==> ( the carrier of F₂(),F₃(),([: the carrier of F₂(),F₃():],(FinTrees [: the carrier of F₂(),F₃():]),b₃)) ) } is set
(F₁() . PN) \/ { ([b₁,H₃(b₁,b₂)] -tree b₂) where b₁ is Element of the carrier of F₂(), b₂ is Relation-like NAT -defined F₁() . PN -valued Function-like finite FinSequence-like FinSubsequence-like Element of (F₁() . PN) * : ex b₃ being Relation-like NAT -defined FinTrees [: the carrier of F₂(),F₃():] -valued Function-like finite FinSequence-like FinSubsequence-like DTree-yielding FinSequence of FinTrees [: the carrier of F₂(),F₃():] st
( b₂ = b₃ & b₁ ==> ( the carrier of F₂(),F₃(),([: the carrier of F₂(),F₃():],(FinTrees [: the carrier of F₂(),F₃():]),b₃)) ) } is set
S is Element of the carrier of F₂()
nt is Relation-like NAT -defined F₁() . PN -valued Function-like finite FinSequence-like FinSubsequence-like Element of (F₁() . PN) *
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,(pr1 (roots nt)),(pr2 (roots nt))) is Element of F₃()
[S,H₃(S,nt)] is V15() Element of [: the carrier of F₂(),F₃():]
{S,F₅(S,(pr1 (roots nt)),(pr2 (roots nt)))} is non empty finite set
{S} is non empty trivial finite V48(1) set
{{S,F₅(S,(pr1 (roots nt)),(pr2 (roots nt)))},{S}} is non empty finite V45() set
[S,H₃(S,nt)] -tree nt is Relation-like Function-like DecoratedTree-like set
x is Relation-like NAT -defined FinTrees [: the carrier of F₂(),F₃():] -valued Function-like finite FinSequence-like FinSubsequence-like DTree-yielding FinSequence of FinTrees [: the carrier of F₂(),F₃():]
([: the carrier of F₂(),F₃():],(FinTrees [: the carrier of F₂(),F₃():]),x) is Relation-like NAT -defined [: the carrier of F₂(),F₃():] -valued Function-like finite FinSequence-like FinSubsequence-like FinSequence of [: the carrier of F₂(),F₃():]
( the carrier of F₂(),F₃(),([: the carrier of F₂(),F₃():],(FinTrees [: the carrier of F₂(),F₃():]),x)) is Relation-like NAT -defined the carrier of F₂() -valued Function-like finite FinSequence-like FinSubsequence-like FinSequence of the carrier of F₂()
rtO is Relation-like NAT -defined FinTrees [: the carrier of F₂(),F₃():] -valued Function-like finite FinSequence-like FinSubsequence-like DTree-yielding FinSequence of FinTrees [: the carrier of F₂(),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,(pr1 (roots rtO)),(pr2 (roots rtO))) is Element of F₃()
[S,H₃(S,rtO)] is V15() Element of [: the carrier of F₂(),F₃():]
{S,F₅(S,(pr1 (roots rtO)),(pr2 (roots rtO)))} is non empty finite set
{{S,F₅(S,(pr1 (roots rtO)),(pr2 (roots rtO)))},{S}} is non empty finite V45() set
[S,H₃(S,rtO)] -tree rtO is Relation-like [: the carrier of F₂(),F₃():] -valued Function-like DecoratedTree-like Element of FinTrees [: the carrier of F₂(),F₃():]
PN is set
F₁() . PN is set
TSPN is functional constituted-DTrees Element of bool (FinTrees [: the carrier of F₂(),F₃():])
PN is Element of the carrier of F₂()
F₄(PN) is Element of F₃()
[PN,F₄(PN)] is V15() Element of [: the carrier of F₂(),F₃():]
{PN,F₄(PN)} is non empty finite set
{PN} is non empty trivial finite V48(1) set
{{PN,F₄(PN)},{PN}} is non empty finite V45() set
root-tree [PN,F₄(PN)] is Relation-like [: the carrier of F₂(),F₃():] -valued Function-like DecoratedTree-like Element of FinTrees [: the carrier of F₂(),F₃():]
PN is Element of the carrier of F₂()
O is Relation-like NAT -defined FinTrees [: the carrier of F₂(),F₃():] -valued Function-like finite FinSequence-like FinSubsequence-like DTree-yielding FinSequence of TSPN
([: the carrier of F₂(),F₃():],(FinTrees [: the carrier of F₂(),F₃():]),O) is Relation-like NAT -defined [: the carrier of F₂(),F₃():] -valued Function-like finite FinSequence-like FinSubsequence-like FinSequence of [: the carrier of F₂(),F₃():]
( the carrier of F₂(),F₃(),([: the carrier of F₂(),F₃():],(FinTrees [: the carrier of F₂(),F₃():]),O)) is Relation-like NAT -defined the carrier of F₂() -valued Function-like finite FinSequence-like FinSubsequence-like FinSequence of the carrier of F₂()
( the carrier of F₂(),F₃(),([: the carrier of F₂(),F₃():],(FinTrees [: the carrier of F₂(),F₃():]),O)) is Relation-like NAT -defined F₃() -valued Function-like finite FinSequence-like FinSubsequence-like FinSequence 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₁ where b₁ is ext-real non negative V32() V33() V34() V35() V39() V40() finite V46() Element of NAT : ( 1 <= b₁ & b₁ <= len O ) } is set
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₁() . x is set
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
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₁,F₅(b₁,(pr1 (roots b₂)),(pr2 (roots b₂)))] -tree b₂) where b₁ is Element of the carrier of F₂(), b₂ is Relation-like NAT -defined F₁() . a₁ -valued Function-like finite FinSequence-like FinSubsequence-like Element of (F₁() . a₁) * : ex b₃ being Relation-like NAT -defined FinTrees [: the carrier of F₂(),F₃():] -valued Function-like finite FinSequence-like FinSubsequence-like DTree-yielding FinSequence of FinTrees [: the carrier of F₂(),F₃():] st
( b₂ = b₃ & b₁ ==> ( the carrier of F₂(),F₃(),([: the carrier of F₂(),F₃():],(FinTrees [: the carrier of F₂(),F₃():]),b₃)) ) } is set
ts is ext-real non negative V32() V33() V34() V35() V39() V40() finite V46() Element of NAT
F₁() . ts is set
ts + 1 is non empty ext-real positive non negative V32() V33() V34() V35() V39() V40() finite V46() Element of NAT
F₁() . (ts + 1) is set
(F₁() . ts) * is functional non empty FinSequence-membered FinSequenceSet of F₁() . ts
{ ([b₁,F₅(b₁,(pr1 (roots b₂)),(pr2 (roots b₂)))] -tree b₂) where b₁ is Element of the carrier of F₂(), b₂ is Relation-like NAT -defined F₁() . ts -valued Function-like finite FinSequence-like FinSubsequence-like Element of (F₁() . ts) * : ex b₃ being Relation-like NAT -defined FinTrees [: the carrier of F₂(),F₃():] -valued Function-like finite FinSequence-like FinSubsequence-like DTree-yielding FinSequence of FinTrees [: the carrier of F₂(),F₃():] st
( b₂ = b₃ & b₁ ==> ( the carrier of F₂(),F₃(),([: the carrier of F₂(),F₃():],(FinTrees [: the carrier of F₂(),F₃():]),b₃)) ) } is set
(F₁() . ts) \/ H₄(ts,F₁() . ts) is set
F₁() . f2 is set
F₁() . (rtO . tsg9) is set
x is ext-real non negative V32() V33() V34() V35() V39() V40() finite V46() Element of NAT
F₁() . x is set
x is ext-real non negative V32() V33() V34() V35() V39() V40() finite V46() Element of NAT
F₁() . x is set
rng F₁() is set
union (rng F₁()) is set
n is functional constituted-DTrees Element of bool (FinTrees [: the carrier of F₂(),F₃():])
n * is functional non empty FinSequence-membered FinSequenceSet of n
n is Relation-like NAT -defined FinTrees [: the carrier of F₂(),F₃():] -valued Function-like finite FinSequence-like FinSubsequence-like DTree-yielding FinSequence of n
F₅(PN,( the carrier of F₂(),F₃(),([: the carrier of F₂(),F₃():],(FinTrees [: the carrier of F₂(),F₃():]),O)),( the carrier of F₂(),F₃(),([: the carrier of F₂(),F₃():],(FinTrees [: the carrier of F₂(),F₃():]),O))) is Element of F₃()
[PN,F₅(PN,( the carrier of F₂(),F₃(),([: the carrier of F₂(),F₃():],(FinTrees [: the carrier of F₂(),F₃():]),O)),( the carrier of F₂(),F₃(),([: the carrier of F₂(),F₃():],(FinTrees [: the carrier of F₂(),F₃():]),O)))] is V15() Element of [: the carrier of F₂(),F₃():]
{PN,F₅(PN,( the carrier of F₂(),F₃(),([: the carrier of F₂(),F₃():],(FinTrees [: the carrier of F₂(),F₃():]),O)),( the carrier of F₂(),F₃(),([: the carrier of F₂(),F₃():],(FinTrees [: the carrier of F₂(),F₃():]),O)))} is non empty finite set
{PN} is non empty trivial finite V48(1) set
{{PN,F₅(PN,( the carrier of F₂(),F₃(),([: the carrier of F₂(),F₃():],(FinTrees [: the carrier of F₂(),F₃():]),O)),( the carrier of F₂(),F₃(),([: the carrier of F₂(),F₃():],(FinTrees [: the carrier of F₂(),F₃():]),O)))},{PN}} is non empty finite V45() set
tsg9 is Relation-like NAT -defined n -valued Function-like finite FinSequence-like FinSubsequence-like DTree-yielding Element of n *
[PN,F₅(PN,( the carrier of F₂(),F₃(),([: the carrier of F₂(),F₃():],(FinTrees [: the carrier of F₂(),F₃():]),O)),( the carrier of F₂(),F₃(),([: the carrier of F₂(),F₃():],(FinTrees [: the carrier of F₂(),F₃():]),O)))] -tree tsg9 is Relation-like Function-like DecoratedTree-like set
{ ([b₁,H₃(b₁,b₂)] -tree b₂) where b₁ is Element of the carrier of F₂(), b₂ is Relation-like NAT -defined n -valued Function-like finite FinSequence-like FinSubsequence-like DTree-yielding Element of n * : ex b₃ being Relation-like NAT -defined FinTrees [: the carrier of F₂(),F₃():] -valued Function-like finite FinSequence-like FinSubsequence-like DTree-yielding FinSequence of FinTrees [: the carrier of F₂(),F₃():] st
( b₂ = b₃ & b₁ ==> ( the carrier of F₂(),F₃(),([: the carrier of F₂(),F₃():],(FinTrees [: the carrier of F₂(),F₃():]),b₃)) ) } is set
(F₁() . x) \/ { ([b₁,H₃(b₁,b₂)] -tree b₂) where b₁ is Element of the carrier of F₂(), b₂ is Relation-like NAT -defined n -valued Function-like finite FinSequence-like FinSubsequence-like DTree-yielding Element of n * : ex b₃ being Relation-like NAT -defined FinTrees [: the carrier of F₂(),F₃():] -valued Function-like finite FinSequence-like FinSubsequence-like DTree-yielding FinSequence of FinTrees [: the carrier of F₂(),F₃():] st
( b₂ = b₃ & b₁ ==> ( the carrier of F₂(),F₃(),([: the carrier of F₂(),F₃():],(FinTrees [: the carrier of F₂(),F₃():]),b₃)) ) } is set
x + 1 is non empty ext-real positive non negative V32() V33() V34() V35() V39() V40() finite V46() Element of NAT
F₁() . (x + 1) is set
[PN,F₅(PN,( the carrier of F₂(),F₃(),([: the carrier of F₂(),F₃():],(FinTrees [: the carrier of F₂(),F₃():]),O)),( the carrier of F₂(),F₃(),([: the carrier of F₂(),F₃():],(FinTrees [: the carrier of F₂(),F₃():]),O)))] -tree O is Relation-like [: the carrier of F₂(),F₃():] -valued Function-like DecoratedTree-like Element of FinTrees [: the carrier of F₂(),F₃():]
PN is functional constituted-DTrees Element of bool (FinTrees [: the carrier of F₂(),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₂(),F₃():] -valued Function-like finite FinSequence-like FinSubsequence-like DTree-yielding FinSequence of PN
([: the carrier of F₂(),F₃():],(FinTrees [: the carrier of F₂(),F₃():]),S) is Relation-like NAT -defined [: the carrier of F₂(),F₃():] -valued Function-like finite FinSequence-like FinSubsequence-like FinSequence of [: the carrier of F₂(),F₃():]
( the carrier of F₂(),F₃(),([: the carrier of F₂(),F₃():],(FinTrees [: the carrier of F₂(),F₃():]),S)) is Relation-like NAT -defined the carrier of F₂() -valued Function-like finite FinSequence-like FinSubsequence-like FinSequence of 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₂(),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₃():] -valued Function-like DecoratedTree-like Element of FinTrees [: the carrier of F₂(),F₃():]
F₄(nt) is Element of F₃()
F₅(nt,(pr1 (roots S)),(pr2 (roots S))) is Element of F₃()
[nt,rtO] -tree S is Relation-like [: the carrier of F₂(),F₃():] -valued Function-like DecoratedTree-like Element of FinTrees [: the carrier of F₂(),F₃():]
O is ext-real non negative V32() V33() V34() V35() V39() V40() finite V46() Element of NAT
F₁() . O is set
O + 1 is non empty ext-real positive non negative V32() V33() V34() V35() V39() V40() finite V46() Element of NAT
F₁() . (O + 1) is set
S is set
(F₁() . O) * is functional non empty FinSequence-membered FinSequenceSet of F₁() . O
{ ([b₁,H₃(b₁,b₂)] -tree b₂) where b₁ is Element of the carrier of F₂(), b₂ is Relation-like NAT -defined F₁() . O -valued Function-like finite FinSequence-like FinSubsequence-like Element of (F₁() . O) * : ex b₃ being Relation-like NAT -defined FinTrees [: the carrier of F₂(),F₃():] -valued Function-like finite FinSequence-like FinSubsequence-like DTree-yielding FinSequence of FinTrees [: the carrier of F₂(),F₃():] st
( b₂ = b₃ & b₁ ==> ( the carrier of F₂(),F₃(),([: the carrier of F₂(),F₃():],(FinTrees [: the carrier of F₂(),F₃():]),b₃)) ) } is set
(F₁() . O) \/ { ([b₁,H₃(b₁,b₂)] -tree b₂) where b₁ is Element of the carrier of F₂(), b₂ is Relation-like NAT -defined F₁() . O -valued Function-like finite FinSequence-like FinSubsequence-like Element of (F₁() . O) * : ex b₃ being Relation-like NAT -defined FinTrees [: the carrier of F₂(),F₃():] -valued Function-like finite FinSequence-like FinSubsequence-like DTree-yielding FinSequence of FinTrees [: the carrier of F₂(),F₃():] st
( b₂ = b₃ & b₁ ==> ( the carrier of F₂(),F₃(),([: the carrier of F₂(),F₃():],(FinTrees [: the carrier of F₂(),F₃():]),b₃)) ) } is set
nt is Element of the carrier of F₂()
rtO is Relation-like NAT -defined F₁() . O -valued Function-like finite FinSequence-like FinSubsequence-like Element of (F₁() . O) *
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,(pr1 (roots rtO)),(pr2 (roots rtO))) is Element of F₃()
[nt,H₃(nt,rtO)] is V15() Element of [: the carrier of F₂(),F₃():]
{nt,F₅(nt,(pr1 (roots rtO)),(pr2 (roots rtO)))} is non empty finite set
{nt} is non empty trivial finite V48(1) set
{{nt,F₅(nt,(pr1 (roots rtO)),(pr2 (roots rtO)))},{nt}} is non empty finite V45() set
[nt,H₃(nt,rtO)] -tree rtO is Relation-like Function-like DecoratedTree-like set
rng rtO is finite set
x is Relation-like NAT -defined FinTrees [: the carrier of F₂(),F₃():] -valued Function-like finite FinSequence-like FinSubsequence-like DTree-yielding FinSequence of PN
([: the carrier of F₂(),F₃():],(FinTrees [: the carrier of F₂(),F₃():]),x) is Relation-like NAT -defined [: the carrier of F₂(),F₃():] -valued Function-like finite FinSequence-like FinSubsequence-like FinSequence of [: the carrier of F₂(),F₃():]
( the carrier of F₂(),F₃(),([: the carrier of F₂(),F₃():],(FinTrees [: the carrier of F₂(),F₃():]),x)) is Relation-like NAT -defined the carrier of F₂() -valued Function-like finite FinSequence-like FinSubsequence-like FinSequence of the carrier of F₂()
n is Relation-like NAT -defined FinTrees [: the carrier of F₂(),F₃():] -valued Function-like finite FinSequence-like FinSubsequence-like DTree-yielding FinSequence of FinTrees [: the carrier of F₂(),F₃():]
([: the carrier of F₂(),F₃():],(FinTrees [: the carrier of F₂(),F₃():]),n) is Relation-like NAT -defined [: the carrier of F₂(),F₃():] -valued Function-like finite FinSequence-like FinSubsequence-like FinSequence of [: the carrier of F₂(),F₃():]
( the carrier of F₂(),F₃(),([: the carrier of F₂(),F₃():],(FinTrees [: the carrier of F₂(),F₃():]),n)) is Relation-like NAT -defined the carrier of F₂() -valued Function-like finite FinSequence-like FinSubsequence-like FinSequence of the carrier of F₂()
O is set
S is set
F₁() . S is set
F₃() is non empty set
F₁() is Relation-like Function-like set
dom F₁() is set
F₁() . 0 is set
F₂() is non empty DTConstrStr
the carrier of F₂() is non empty set
[: the carrier of F₂(),F₃():] is Relation-like non empty set
Terminals F₂() is set
{ (root-tree [b₁,b₂]) where b₁ is Element of the carrier of F₂(), b₂ is Element of F₃() : ( ( b₁ in Terminals F₂() & b₂ = F₄(b₁) ) or ( b₁ ==> {} & b₂ = F₅(b₁,{},{}) ) ) } is set
FinTrees [: the carrier of F₂(),F₃():] is functional non empty constituted-DTrees DTree-set of [: the carrier of F₂(),F₃():]
FinTrees the carrier of F₂() is functional non empty constituted-DTrees DTree-set of the carrier of F₂()
bool (FinTrees the carrier of F₂()) is non empty set
Union F₁() is set
{ (b₁ `1) where b<sub>1</sub> is Relation-like [: the carrier of F<sub>2</sub>(),F<sub>3</sub>():] -valued Function-like DecoratedTree-like Element of FinTrees [: the carrier of F<sub>2</sub>(),F<sub>3</sub>():] : b<sub>1</sub> in Union F<sub>1</sub>() } is set
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<sub>1</sub>() . (O + 1) is set
F<sub>1</sub>() . O is set
(F<sub>1</sub>() . O) * is functional non empty FinSequence-membered FinSequenceSet of F<sub>1</sub>() . O
{ ([b<sub>1</sub>,F<sub>5</sub>(b<sub>1</sub>,(pr1 (roots b<sub>2</sub>)),(pr2 (roots b<sub>2</sub>)))] -tree b<sub>2</sub>) where b<sub>1</sub> is Element of the carrier of F<sub>2</sub>(), b<sub>2</sub> is Relation-like NAT -defined F<sub>1</sub>() . O -valued Function-like finite FinSequence-like FinSubsequence-like Element of (F<sub>1</sub>() . O) * : ex b<sub>3</sub> being Relation-like NAT -defined FinTrees [: the carrier of F<sub>2</sub>(),F<sub>3</sub>():] -valued Function-like finite FinSequence-like FinSubsequence-like DTree-yielding FinSequence of FinTrees [: the carrier of F<sub>2</sub>(),F<sub>3</sub>():] st
( b<sub>2</sub> = b<sub>3</sub> & b<sub>1</sub> ==> ( the carrier of F<sub>2</sub>(),F<sub>3</sub>(),([: the carrier of F<sub>2</sub>(),F<sub>3</sub>():],(FinTrees [: the carrier of F<sub>2</sub>(),F<sub>3</sub>():]),b<sub>3</sub>)) ) } is set
(F<sub>1</sub>() . O) \/ { ([b<sub>1</sub>,F<sub>5</sub>(b<sub>1</sub>,(pr1 (roots b<sub>2</sub>)),(pr2 (roots b<sub>2</sub>)))] -tree b<sub>2</sub>) where b<sub>1</sub> is Element of the carrier of F<sub>2</sub>(), b<sub>2</sub> is Relation-like NAT -defined F<sub>1</sub>() . O -valued Function-like finite FinSequence-like FinSubsequence-like Element of (F<sub>1</sub>() . O) * : ex b<sub>3</sub> being Relation-like NAT -defined FinTrees [: the carrier of F<sub>2</sub>(),F<sub>3</sub>():] -valued Function-like finite FinSequence-like FinSubsequence-like DTree-yielding FinSequence of FinTrees [: the carrier of F<sub>2</sub>(),F<sub>3</sub>():] st
( b<sub>2</sub> = b<sub>3</sub> & b<sub>1</sub> ==> ( the carrier of F<sub>2</sub>(),F<sub>3</sub>(),([: the carrier of F<sub>2</sub>(),F<sub>3</sub>():],(FinTrees [: the carrier of F<sub>2</sub>(),F<sub>3</sub>():]),b<sub>3</sub>)) ) } is set
bool (FinTrees [: the carrier of F<sub>2</sub>(),F<sub>3</sub>():]) is non empty set
O is functional constituted-DTrees Element of bool (FinTrees [: the carrier of F<sub>2</sub>(),F<sub>3</sub>():])
nt is set
rtO is Relation-like [: the carrier of F<sub>2</sub>(),F<sub>3</sub>():] -valued Function-like DecoratedTree-like Element of FinTrees [: the carrier of F<sub>2</sub>(),F<sub>3</sub>():]
rtO `1 is Relation-like the carrier of F₂() -valued Function-like DecoratedTree-like set
pr1 ( the carrier of F₂(),F₃()) is Relation-like Function-like V18([: the carrier of F₂(),F₃():], the carrier of F₂()) Element of bool [:[: the carrier of F₂(),F₃():], the carrier of F₂():]
[:[: the carrier of F₂(),F₃():], the carrier of F₂():] is Relation-like non empty set
bool [:[: the carrier of F₂(),F₃():], the carrier of F₂():] is non empty set
rtO * (pr1 ( the carrier of F₂(),F₃())) is Relation-like Function-like DecoratedTree-like set
rng rtO is set
dom (pr1 ( the carrier of F₂(),F₃())) is set
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<sub>2</sub>())
rtO is functional constituted-DTrees Element of bool (FinTrees the carrier of F<sub>2</sub>())
x is Element of the carrier of F<sub>2</sub>()
F<sub>4</sub>(x) is Element of F<sub>3</sub>()
[x,F<sub>4</sub>(x)] is V15() Element of [: the carrier of F<sub>2</sub>(),F<sub>3</sub>():]
{x,F<sub>4</sub>(x)} is non empty finite set
{x} is non empty trivial finite V48(1) set
{{x,F<sub>4</sub>(x)},{x}} is non empty finite V45() set
root-tree [x,F<sub>4</sub>(x)] is Relation-like [: the carrier of F<sub>2</sub>(),F<sub>3</sub>():] -valued Function-like DecoratedTree-like Element of FinTrees [: the carrier of F<sub>2</sub>(),F<sub>3</sub>():]
(root-tree [x,F<sub>4</sub>(x)]) `1 is Relation-like the carrier of F₂() -valued Function-like DecoratedTree-like set
root-tree x is Relation-like the carrier of F₂() -valued Function-like DecoratedTree-like Element of FinTrees the carrier of F₂()
x is Element of the carrier of F₂()
n is Relation-like NAT -defined FinTrees the carrier of F₂() -valued Function-like finite FinSequence-like FinSubsequence-like DTree-yielding FinSequence of rtO
( the carrier of F₂(),(FinTrees the carrier of F₂()),n) is Relation-like NAT -defined the carrier of F₂() -valued Function-like finite FinSequence-like FinSubsequence-like FinSequence of 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₁ where b₁ is ext-real non negative V32() V33() V34() V35() V39() V40() finite V46() Element of NAT : ( 1 <= b₁ & b₁ <= len n ) } is set
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₂(),F₃():] -valued Function-like DecoratedTree-like Element of FinTrees [: the carrier of F₂(),F₃():]
tsg9 `1 is Relation-like the carrier of F<sub>2</sub>() -valued Function-like DecoratedTree-like set
n is Relation-like NAT -defined FinTrees [: the carrier of F<sub>2</sub>(),F<sub>3</sub>():] -valued Function-like finite FinSequence-like FinSubsequence-like DTree-yielding FinSequence of FinTrees [: the carrier of F<sub>2</sub>(),F<sub>3</sub>():]
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<sub>2</sub>(),F<sub>3</sub>():] -valued Function-like DecoratedTree-like set
nt `1 is Relation-like the carrier of F₂() -valued Function-like DecoratedTree-like set
dom ( the carrier of F₂(),(FinTrees the carrier of F₂()),n) is finite Element of bool NAT
tsg9 is Relation-like NAT -defined FinTrees [: the carrier of F₂(),F₃():] -valued Function-like finite FinSequence-like FinSubsequence-like DTree-yielding FinSequence of O
([: the carrier of F₂(),F₃():],(FinTrees [: the carrier of F₂(),F₃():]),tsg9) is Relation-like NAT -defined [: the carrier of F₂(),F₃():] -valued Function-like finite FinSequence-like FinSubsequence-like FinSequence of [: the carrier of F₂(),F₃():]
( the carrier of F₂(),F₃(),([: the carrier of F₂(),F₃():],(FinTrees [: the carrier of F₂(),F₃():]),tsg9)) is Relation-like NAT -defined the carrier of F₂() -valued Function-like finite FinSequence-like FinSubsequence-like FinSequence of the carrier of F₂()
dom ( the carrier of F₂(),F₃(),([: the carrier of F₂(),F₃():],(FinTrees [: the carrier of F₂(),F₃():]),tsg9)) is finite Element of bool NAT
dom ([: the carrier of F₂(),F₃():],(FinTrees [: the carrier of F₂(),F₃():]),tsg9) is finite Element of bool NAT
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₂(),F₃():] -valued Function-like DecoratedTree-like set
f2 `1 is Relation-like the carrier of F<sub>2</sub>() -valued Function-like DecoratedTree-like set
dom f2 is non empty Tree-like set
( the carrier of F<sub>2</sub>(),(FinTrees the carrier of F<sub>2</sub>()),n) . tsg9 is set
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<sub>2</sub>(),F<sub>3</sub>():]
(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₂(),F₃():],(FinTrees [: the carrier of F₂(),F₃():]),tsg9) . tsg9 is set
( the carrier of F₂(),F₃(),([: the carrier of F₂(),F₃():],(FinTrees [: the carrier of F₂(),F₃():]),tsg9)) . tsg9 is set
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,(pr1 (roots tsg9)),(pr2 (roots tsg9))) is Element of F₃()
[x,H₃(x,tsg9)] is V15() Element of [: the carrier of F₂(),F₃():]
{x,F₅(x,(pr1 (roots tsg9)),(pr2 (roots tsg9)))} is non empty finite set
{x} is non empty trivial finite V48(1) set
{{x,F₅(x,(pr1 (roots tsg9)),(pr2 (roots tsg9)))},{x}} is non empty finite V45() set
[x,H₃(x,tsg9)] -tree tsg9 is Relation-like [: the carrier of F₂(),F₃():] -valued Function-like DecoratedTree-like Element of FinTrees [: the carrier of F₂(),F₃():]
rng tsg9 is finite set
Trees [: the carrier of F₂(),F₃():] is functional non empty constituted-DTrees DTree-set of [: the carrier of F₂(),F₃():]
rng n is finite set
Trees the carrier of F₂() is functional non empty constituted-DTrees DTree-set of 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₂(),F₃():] -valued Function-like DecoratedTree-like set
ts `1 is Relation-like the carrier of F<sub>2</sub>() -valued Function-like DecoratedTree-like set
p21 is Relation-like [: the carrier of F<sub>2</sub>(),F<sub>3</sub>():] -valued Function-like DecoratedTree-like set
p21 `1 is Relation-like the carrier of F₂() -valued Function-like DecoratedTree-like set
tsg9 is Relation-like NAT -defined Trees [: the carrier of F₂(),F₃():] -valued Function-like finite FinSequence-like FinSubsequence-like DTree-yielding FinSequence of Trees [: the carrier of F₂(),F₃():]
[x,H₃(x,tsg9)] -tree tsg9 is Relation-like [: the carrier of F₂(),F₃():] -valued Function-like DecoratedTree-like set
([x,H₃(x,tsg9)] -tree tsg9) `1 is Relation-like the carrier of F<sub>2</sub>() -valued Function-like DecoratedTree-like set
f2 is Relation-like NAT -defined Trees the carrier of F<sub>2</sub>() -valued Function-like finite FinSequence-like FinSubsequence-like DTree-yielding FinSequence of Trees the carrier of F<sub>2</sub>()
x -tree f2 is Relation-like the carrier of F<sub>2</sub>() -valued Function-like DecoratedTree-like set
x -tree n is Relation-like the carrier of F<sub>2</sub>() -valued Function-like DecoratedTree-like Element of FinTrees the carrier of F<sub>2</sub>()
x is functional constituted-DTrees Element of bool (FinTrees the carrier of F<sub>2</sub>())
n is set
n is Relation-like [: the carrier of F<sub>2</sub>(),F<sub>3</sub>():] -valued Function-like DecoratedTree-like Element of FinTrees [: the carrier of F<sub>2</sub>(),F<sub>3</sub>():]
n `1 is Relation-like the carrier of F₂() -valued Function-like DecoratedTree-like set
{ b₁ where b₁ is Relation-like [: the carrier of F₂(),F₃():] -valued Function-like DecoratedTree-like Element of FinTrees [: the carrier of F₂(),F₃():] : b₁ `1 in x } is set
tsg9 is set
f2 is Relation-like [: the carrier of F<sub>2</sub>(),F<sub>3</sub>():] -valued Function-like DecoratedTree-like Element of FinTrees [: the carrier of F<sub>2</sub>(),F<sub>3</sub>():]
f2 `1 is Relation-like the carrier of F₂() -valued Function-like DecoratedTree-like set
f2 is Element of the carrier of F₂()
root-tree f2 is Relation-like the carrier of F₂() -valued Function-like DecoratedTree-like Element of FinTrees the carrier of F₂()
F₄(f2) is Element of F₃()
[f2,F₄(f2)] is V15() Element of [: the carrier of F₂(),F₃():]
{f2,F₄(f2)} is non empty finite set
{f2} is non empty trivial finite V48(1) set
{{f2,F₄(f2)},{f2}} is non empty finite V45() set
root-tree [f2,F₄(f2)] is Relation-like [: the carrier of F₂(),F₃():] -valued Function-like DecoratedTree-like Element of FinTrees [: the carrier of F₂(),F₃():]
(root-tree [f2,F₄(f2)]) `1 is Relation-like the carrier of F<sub>2</sub>() -valued Function-like DecoratedTree-like set
tsg9 is functional constituted-DTrees Element of bool (FinTrees [: the carrier of F<sub>2</sub>(),F<sub>3</sub>():])
f2 is Element of the carrier of F<sub>2</sub>()
nt is Relation-like NAT -defined FinTrees [: the carrier of F<sub>2</sub>(),F<sub>3</sub>():] -valued Function-like finite FinSequence-like FinSubsequence-like DTree-yielding FinSequence of tsg9
([: the carrier of F<sub>2</sub>(),F<sub>3</sub>():],(FinTrees [: the carrier of F<sub>2</sub>(),F<sub>3</sub>():]),nt) is Relation-like NAT -defined [: the carrier of F<sub>2</sub>(),F<sub>3</sub>():] -valued Function-like finite FinSequence-like FinSubsequence-like FinSequence of [: the carrier of F<sub>2</sub>(),F<sub>3</sub>():]
( the carrier of F<sub>2</sub>(),F<sub>3</sub>(),([: the carrier of F<sub>2</sub>(),F<sub>3</sub>():],(FinTrees [: the carrier of F<sub>2</sub>(),F<sub>3</sub>():]),nt)) is Relation-like NAT -defined the carrier of F<sub>2</sub>() -valued Function-like finite FinSequence-like FinSubsequence-like FinSequence of the carrier of F<sub>2</sub>()
dom nt is finite Element of bool NAT
( the carrier of F<sub>2</sub>(),F<sub>3</sub>(),([: the carrier of F<sub>2</sub>(),F<sub>3</sub>():],(FinTrees [: the carrier of F<sub>2</sub>(),F<sub>3</sub>():]),nt)) is Relation-like NAT -defined F<sub>3</sub>() -valued Function-like finite FinSequence-like FinSubsequence-like FinSequence of F<sub>3</sub>()
F<sub>5</sub>(f2,( the carrier of F<sub>2</sub>(),F<sub>3</sub>(),([: the carrier of F<sub>2</sub>(),F<sub>3</sub>():],(FinTrees [: the carrier of F<sub>2</sub>(),F<sub>3</sub>():]),nt)),( the carrier of F<sub>2</sub>(),F<sub>3</sub>(),([: the carrier of F<sub>2</sub>(),F<sub>3</sub>():],(FinTrees [: the carrier of F<sub>2</sub>(),F<sub>3</sub>():]),nt))) is Element of F<sub>3</sub>()
[f2,F<sub>5</sub>(f2,( the carrier of F<sub>2</sub>(),F<sub>3</sub>(),([: the carrier of F<sub>2</sub>(),F<sub>3</sub>():],(FinTrees [: the carrier of F<sub>2</sub>(),F<sub>3</sub>():]),nt)),( the carrier of F<sub>2</sub>(),F<sub>3</sub>(),([: the carrier of F<sub>2</sub>(),F<sub>3</sub>():],(FinTrees [: the carrier of F<sub>2</sub>(),F<sub>3</sub>():]),nt)))] is V15() Element of [: the carrier of F<sub>2</sub>(),F<sub>3</sub>():]
{f2,F<sub>5</sub>(f2,( the carrier of F<sub>2</sub>(),F<sub>3</sub>(),([: the carrier of F<sub>2</sub>(),F<sub>3</sub>():],(FinTrees [: the carrier of F<sub>2</sub>(),F<sub>3</sub>():]),nt)),( the carrier of F<sub>2</sub>(),F<sub>3</sub>(),([: the carrier of F<sub>2</sub>(),F<sub>3</sub>():],(FinTrees [: the carrier of F<sub>2</sub>(),F<sub>3</sub>():]),nt)))} is non empty finite set
{f2} is non empty trivial finite V48(1) set
{{f2,F<sub>5</sub>(f2,( the carrier of F<sub>2</sub>(),F<sub>3</sub>(),([: the carrier of F<sub>2</sub>(),F<sub>3</sub>():],(FinTrees [: the carrier of F<sub>2</sub>(),F<sub>3</sub>():]),nt)),( the carrier of F<sub>2</sub>(),F<sub>3</sub>(),([: the carrier of F<sub>2</sub>(),F<sub>3</sub>():],(FinTrees [: the carrier of F<sub>2</sub>(),F<sub>3</sub>():]),nt)))},{f2}} is non empty finite V45() set
[f2,F<sub>5</sub>(f2,( the carrier of F<sub>2</sub>(),F<sub>3</sub>(),([: the carrier of F<sub>2</sub>(),F<sub>3</sub>():],(FinTrees [: the carrier of F<sub>2</sub>(),F<sub>3</sub>():]),nt)),( the carrier of F<sub>2</sub>(),F<sub>3</sub>(),([: the carrier of F<sub>2</sub>(),F<sub>3</sub>():],(FinTrees [: the carrier of F<sub>2</sub>(),F<sub>3</sub>():]),nt)))] -tree nt is Relation-like [: the carrier of F<sub>2</sub>(),F<sub>3</sub>():] -valued Function-like DecoratedTree-like Element of FinTrees [: the carrier of F<sub>2</sub>(),F<sub>3</sub>():]
([f2,F<sub>5</sub>(f2,( the carrier of F<sub>2</sub>(),F<sub>3</sub>(),([: the carrier of F<sub>2</sub>(),F<sub>3</sub>():],(FinTrees [: the carrier of F<sub>2</sub>(),F<sub>3</sub>():]),nt)),( the carrier of F<sub>2</sub>(),F<sub>3</sub>(),([: the carrier of F<sub>2</sub>(),F<sub>3</sub>():],(FinTrees [: the carrier of F<sub>2</sub>(),F<sub>3</sub>():]),nt)))] -tree nt) `1 is Relation-like the carrier of F₂() -valued Function-like DecoratedTree-like set
ts is Relation-like NAT -defined FinTrees the carrier of F₂() -valued Function-like finite FinSequence-like FinSubsequence-like DTree-yielding FinSequence of FinTrees the carrier of F₂()
dom ts is finite Element of bool NAT
f2 -tree ts is Relation-like the carrier of F₂() -valued Function-like DecoratedTree-like Element of FinTrees 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₂(),F₃():] -valued Function-like DecoratedTree-like Element of FinTrees [: the carrier of F₂(),F₃():]
p2k `1 is Relation-like the carrier of F<sub>2</sub>() -valued Function-like DecoratedTree-like set
c<sub>22</sub> is Relation-like [: the carrier of F<sub>2</sub>(),F<sub>3</sub>():] -valued Function-like DecoratedTree-like Element of FinTrees [: the carrier of F<sub>2</sub>(),F<sub>3</sub>():]
c<sub>22</sub> `1 is Relation-like the carrier of F₂() -valued Function-like DecoratedTree-like set
p21 is Relation-like NAT -defined FinTrees the carrier of F₂() -valued Function-like finite FinSequence-like FinSubsequence-like DTree-yielding FinSequence of x
( the carrier of F₂(),(FinTrees the carrier of F₂()),p21) is Relation-like NAT -defined the carrier of F₂() -valued Function-like finite FinSequence-like FinSubsequence-like FinSequence of the carrier of F₂()
dom ( the carrier of F₂(),(FinTrees the carrier of F₂()),p21) is finite Element of bool NAT
dom p21 is finite Element of bool NAT
dom ( the carrier of F₂(),F₃(),([: the carrier of F₂(),F₃():],(FinTrees [: the carrier of F₂(),F₃():]),nt)) is finite Element of bool NAT
dom ([: the carrier of F₂(),F₃():],(FinTrees [: the carrier of F₂(),F₃():]),nt) is finite Element of bool NAT
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₂(),F₃():] -valued Function-like DecoratedTree-like Element of FinTrees [: the carrier of F₂(),F₃():]
p1k `1 is Relation-like the carrier of F<sub>2</sub>() -valued Function-like DecoratedTree-like set
dom p1k is non empty finite Tree-like set
( the carrier of F<sub>2</sub>(),(FinTrees the carrier of F<sub>2</sub>()),p21) . k is set
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<sub>2</sub>(),F<sub>3</sub>():]
(p1k . p2k) `1 is Element of the carrier of F₂()
c₂₂ is Relation-like Function-like DecoratedTree-like set
c₂₂ . {} is set
c₂₃ is Relation-like [: the carrier of F₂(),F₃():] -valued Function-like DecoratedTree-like Element of FinTrees [: the carrier of F₂(),F₃():]
c₂₃ `1 is Relation-like the carrier of F<sub>2</sub>() -valued Function-like DecoratedTree-like set
([: the carrier of F<sub>2</sub>(),F<sub>3</sub>():],(FinTrees [: the carrier of F<sub>2</sub>(),F<sub>3</sub>():]),nt) . k is set
( the carrier of F<sub>2</sub>(),F<sub>3</sub>(),([: the carrier of F<sub>2</sub>(),F<sub>3</sub>():],(FinTrees [: the carrier of F<sub>2</sub>(),F<sub>3</sub>():]),nt)) . k is set
c<sub>22</sub> is Relation-like Function-like DecoratedTree-like set
c<sub>22</sub> . {} is set
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<sub>5</sub>(f2,(pr1 (roots nt)),(pr2 (roots nt))) is Element of F<sub>3</sub>()
[f2,H<sub>3</sub>(f2,nt)] is V15() Element of [: the carrier of F<sub>2</sub>(),F<sub>3</sub>():]
{f2,F<sub>5</sub>(f2,(pr1 (roots nt)),(pr2 (roots nt)))} is non empty finite set
{{f2,F<sub>5</sub>(f2,(pr1 (roots nt)),(pr2 (roots nt)))},{f2}} is non empty finite V45() set
[f2,H<sub>3</sub>(f2,nt)] -tree nt is Relation-like [: the carrier of F<sub>2</sub>(),F<sub>3</sub>():] -valued Function-like DecoratedTree-like Element of FinTrees [: the carrier of F<sub>2</sub>(),F<sub>3</sub>():]
f2 is Relation-like [: the carrier of F<sub>2</sub>(),F<sub>3</sub>():] -valued Function-like DecoratedTree-like Element of FinTrees [: the carrier of F<sub>2</sub>(),F<sub>3</sub>():]
f2 `1 is Relation-like the carrier of F₂() -valued Function-like DecoratedTree-like set
F₃() is non empty set
F₁() is Relation-like Function-like set
dom F₁() is set
F₁() . 0 is set
F₂() is non empty DTConstrStr
the carrier of F₂() is non empty set
[: the carrier of F₂(),F₃():] is Relation-like non empty set
Terminals F₂() is set
{ (root-tree [b₁,b₂]) where b₁ is Element of the carrier of F₂(), b₂ is Element of F₃() : ( ( b₁ in Terminals F₂() & b₂ = F₄(b₁) ) or ( b₁ ==> {} & b₂ = F₅(b₁,{},{}) ) ) } is set
FinTrees [: the carrier of F₂(),F₃():] is functional non empty constituted-DTrees DTree-set of [: the carrier of F₂(),F₃():]
Union F₁() is set
PN is Relation-like [: the carrier of F₂(),F₃():] -valued Function-like DecoratedTree-like Element of FinTrees [: the carrier of F₂(),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₂(),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₃():] -valued Function-like DecoratedTree-like Element of FinTrees [: the carrier of F₂(),F₃():]
F₄(O) is Element of F₃()
F₅(O,{},{}) is Element of F₃()
O is ext-real non negative V32() V33() V34() V35() V39() V40() finite V46() Element of NAT
F₁() . O is set
O + 1 is non empty ext-real positive non negative V32() V33() V34() V35() V39() V40() finite V46() Element of NAT
F₁() . (O + 1) is set
(F₁() . O) * is functional non empty FinSequence-membered FinSequenceSet of F₁() . O
{ ([b₁,H₃(b₁,b₂)] -tree b₂) where b₁ is Element of the carrier of F₂(), b₂ is Relation-like NAT -defined F₁() . O -valued Function-like finite FinSequence-like FinSubsequence-like Element of (F₁() . O) * : ex b₃ being Relation-like NAT -defined FinTrees [: the carrier of F₂(),F₃():] -valued Function-like finite FinSequence-like FinSubsequence-like DTree-yielding FinSequence of FinTrees [: the carrier of F₂(),F₃():] st
( b₂ = b₃ & b₁ ==> ( the carrier of F₂(),F₃(),([: the carrier of F₂(),F₃():],(FinTrees [: the carrier of F₂(),F₃():]),b₃)) ) } is set
(F₁() . O) \/ { ([b₁,H₃(b₁,b₂)] -tree b₂) where b₁ is Element of the carrier of F₂(), b₂ is Relation-like NAT -defined F₁() . O -valued Function-like finite FinSequence-like FinSubsequence-like Element of (F₁() . O) * : ex b₃ being Relation-like NAT -defined FinTrees [: the carrier of F₂(),F₃():] -valued Function-like finite FinSequence-like FinSubsequence-like DTree-yielding FinSequence of FinTrees [: the carrier of F₂(),F₃():] st
( b₂ = b₃ & b₁ ==> ( the carrier of F₂(),F₃(),([: the carrier of F₂(),F₃():],(FinTrees [: the carrier of F₂(),F₃():]),b₃)) ) } is set
S is Element of the carrier of F₂()
nt is Relation-like NAT -defined F₁() . O -valued Function-like finite FinSequence-like FinSubsequence-like Element of (F₁() . O) *
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,(pr1 (roots nt)),(pr2 (roots nt))) is Element of F₃()
[S,H₃(S,nt)] is V15() Element of [: the carrier of F₂(),F₃():]
{S,F₅(S,(pr1 (roots nt)),(pr2 (roots nt)))} is non empty finite set
{S} is non empty trivial finite V48(1) set
{{S,F₅(S,(pr1 (roots nt)),(pr2 (roots nt)))},{S}} is non empty finite V45() set
[S,H₃(S,nt)] -tree nt is Relation-like Function-like DecoratedTree-like set
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₂(),F₃():] -valued Function-like finite FinSequence-like FinSubsequence-like DTree-yielding FinSequence of FinTrees [: the carrier of F₂(),F₃():]
([: the carrier of F₂(),F₃():],(FinTrees [: the carrier of F₂(),F₃():]),rtO) is Relation-like NAT -defined [: the carrier of F₂(),F₃():] -valued Function-like finite FinSequence-like FinSubsequence-like FinSequence of [: the carrier of F₂(),F₃():]
( the carrier of F₂(),F₃(),([: the carrier of F₂(),F₃():],(FinTrees [: the carrier of F₂(),F₃():]),rtO)) is Relation-like NAT -defined the carrier of F₂() -valued Function-like finite FinSequence-like FinSubsequence-like FinSequence of the carrier of F₂()
F₅(S,{},{}) is Element of F₃()
[S,F₅(S,{},{})] is V15() Element of [: the carrier of F₂(),F₃():]
{S,F₅(S,{},{})} is non empty finite set
{{S,F₅(S,{},{})},{S}} is non empty finite V45() set
root-tree [S,F₅(S,{},{})] is Relation-like [: the carrier of F₂(),F₃():] -valued Function-like DecoratedTree-like Element of FinTrees [: the carrier of F₂(),F₃():]
rtO is Relation-like NAT -defined FinTrees [: the carrier of F₂(),F₃():] -valued Function-like finite FinSequence-like FinSubsequence-like DTree-yielding FinSequence of FinTrees [: the carrier of F₂(),F₃():]
([: the carrier of F₂(),F₃():],(FinTrees [: the carrier of F₂(),F₃():]),rtO) is Relation-like NAT -defined [: the carrier of F₂(),F₃():] -valued Function-like finite FinSequence-like FinSubsequence-like FinSequence of [: the carrier of F₂(),F₃():]
( the carrier of F₂(),F₃(),([: the carrier of F₂(),F₃():],(FinTrees [: the carrier of F₂(),F₃():]),rtO)) is Relation-like NAT -defined the carrier of F₂() -valued Function-like finite FinSequence-like FinSubsequence-like FinSequence of the carrier of F₂()
O is set
F₁() . O is set
PN is ext-real non negative V32() V33() V34() V35() V39() V40() finite V46() Element of NAT
F₁() . PN is set
PN + 1 is non empty ext-real positive non negative V32() V33() V34() V35() V39() V40() finite V46() Element of NAT
F₁() . (PN + 1) is set
O is Relation-like [: the carrier of F₂(),F₃():] -valued Function-like DecoratedTree-like Element of FinTrees [: the carrier of F₂(),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₁() . PN) * is functional non empty FinSequence-membered FinSequenceSet of F₁() . PN
{ ([b₁,H₃(b₁,b₂)] -tree b₂) where b₁ is Element of the carrier of F₂(), b₂ is Relation-like NAT -defined F₁() . PN -valued Function-like finite FinSequence-like FinSubsequence-like Element of (F₁() . PN) * : ex b₃ being Relation-like NAT -defined FinTrees [: the carrier of F₂(),F₃():] -valued Function-like finite FinSequence-like FinSubsequence-like DTree-yielding FinSequence of FinTrees [: the carrier of F₂(),F₃():] st
( b₂ = b₃ & b₁ ==> ( the carrier of F₂(),F₃(),([: the carrier of F₂(),F₃():],(FinTrees [: the carrier of F₂(),F₃():]),b₃)) ) } is set
(F₁() . PN) \/ { ([b₁,H₃(b₁,b₂)] -tree b₂) where b₁ is Element of the carrier of F₂(), b₂ is Relation-like NAT -defined F₁() . PN -valued Function-like finite FinSequence-like FinSubsequence-like Element of (F₁() . PN) * : ex b₃ being Relation-like NAT -defined FinTrees [: the carrier of F₂(),F₃():] -valued Function-like finite FinSequence-like FinSubsequence-like DTree-yielding FinSequence of FinTrees [: the carrier of F₂(),F₃():] st
( b₂ = b₃ & b₁ ==> ( the carrier of F₂(),F₃(),([: the carrier of F₂(),F₃():],(FinTrees [: the carrier of F₂(),F₃():]),b₃)) ) } is set
S is Element of the carrier of F₂()
nt is Relation-like NAT -defined F₁() . PN -valued Function-like finite FinSequence-like FinSubsequence-like Element of (F₁() . PN) *
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,(pr1 (roots nt)),(pr2 (roots nt))) is Element of F₃()
[S,H₃(S,nt)] is V15() Element of [: the carrier of F₂(),F₃():]
{S,F₅(S,(pr1 (roots nt)),(pr2 (roots nt)))} is non empty finite set
{S} is non empty trivial finite V48(1) set
{{S,F₅(S,(pr1 (roots nt)),(pr2 (roots nt)))},{S}} is non empty finite V45() set
[S,H₃(S,nt)] -tree nt is Relation-like Function-like DecoratedTree-like set
x is Relation-like NAT -defined FinTrees [: the carrier of F₂(),F₃():] -valued Function-like finite FinSequence-like FinSubsequence-like DTree-yielding FinSequence of FinTrees [: the carrier of F₂(),F₃():]
([: the carrier of F₂(),F₃():],(FinTrees [: the carrier of F₂(),F₃():]),x) is Relation-like NAT -defined [: the carrier of F₂(),F₃():] -valued Function-like finite FinSequence-like FinSubsequence-like FinSequence of [: the carrier of F₂(),F₃():]
( the carrier of F₂(),F₃(),([: the carrier of F₂(),F₃():],(FinTrees [: the carrier of F₂(),F₃():]),x)) is Relation-like NAT -defined the carrier of F₂() -valued Function-like finite FinSequence-like FinSubsequence-like FinSequence of the carrier of F₂()
rtO is Relation-like NAT -defined FinTrees [: the carrier of F₂(),F₃():] -valued Function-like finite FinSequence-like FinSubsequence-like DTree-yielding FinSequence of FinTrees [: the carrier of F₂(),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₂(),F₃():] -valued Function-like DecoratedTree-like Element of FinTrees [: the carrier of F₂(),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 set
S is ext-real non negative V32() V33() V34() V35() V39() V40() finite V46() set
F₁() . S is set
{ ([b₁,F₅(b₁,(pr1 (roots b₂)),(pr2 (roots b₂)))] -tree b₂) where b₁ is Element of the carrier of F₂(), b₂ is Relation-like NAT -defined F₁() . a₁ -valued Function-like finite FinSequence-like FinSubsequence-like Element of (F₁() . a₁) * : ex b₃ being Relation-like NAT -defined FinTrees [: the carrier of F₂(),F₃():] -valued Function-like finite FinSequence-like FinSubsequence-like DTree-yielding FinSequence of FinTrees [: the carrier of F₂(),F₃():] st
( b₂ = b₃ & b₁ ==> ( the carrier of F₂(),F₃(),([: the carrier of F₂(),F₃():],(FinTrees [: the carrier of F₂(),F₃():]),b₃)) ) } is set
nt is ext-real non negative V32() V33() V34() V35() V39() V40() finite V46() Element of NAT
F₁() . nt is set
nt + 1 is non empty ext-real positive non negative V32() V33() V34() V35() V39() V40() finite V46() Element of NAT
F₁() . (nt + 1) is set
(F₁() . nt) * is functional non empty FinSequence-membered FinSequenceSet of F₁() . nt
{ ([b₁,F₅(b₁,(pr1 (roots b₂)),(pr2 (roots b₂)))] -tree b₂) where b₁ is Element of the carrier of F₂(), b₂ is Relation-like NAT -defined F₁() . nt -valued Function-like finite FinSequence-like FinSubsequence-like Element of (F₁() . nt) * : ex b₃ being Relation-like NAT -defined FinTrees [: the carrier of F₂(),F₃():] -valued Function-like finite FinSequence-like FinSubsequence-like DTree-yielding FinSequence of FinTrees [: the carrier of F₂(),F₃():] st
( b₂ = b₃ & b₁ ==> ( the carrier of F₂(),F₃(),([: the carrier of F₂(),F₃():],(FinTrees [: the carrier of F₂(),F₃():]),b₃)) ) } is set
(F₁() . nt) \/ H₄(nt,F₁() . nt) is set
0 + (PN + 1) is non empty ext-real positive non negative V32() V33() V34() V35() V39() V40() finite V46() Element of NAT
F₁() . (0 + (PN + 1)) is set
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
rtO is ext-real non negative V32() V33() V34() V35() V39() V40() finite V46() Element of NAT
rtO + 1 is non empty ext-real positive non negative V32() V33() V34() V35() V39() V40() finite V46() Element of NAT
F₁() . rtO is set
(F₁() . rtO) * is functional non empty FinSequence-membered FinSequenceSet of F₁() . rtO
{ ([b₁,H₃(b₁,b₂)] -tree b₂) where b₁ is Element of the carrier of F₂(), b₂ is Relation-like NAT -defined F₁() . rtO -valued Function-like finite FinSequence-like FinSubsequence-like Element of (F₁() . rtO) * : ex b₃ being Relation-like NAT -defined FinTrees [: the carrier of F₂(),F₃():] -valued Function-like finite FinSequence-like FinSubsequence-like DTree-yielding FinSequence of FinTrees [: the carrier of F₂(),F₃():] st
( b₂ = b₃ & b₁ ==> ( the carrier of F₂(),F₃(),([: the carrier of F₂(),F₃():],(FinTrees [: the carrier of F₂(),F₃():]),b₃)) ) } is set
(F₁() . rtO) \/ { ([b₁,H₃(b₁,b₂)] -tree b₂) where b₁ is Element of the carrier of F₂(), b₂ is Relation-like NAT -defined F₁() . rtO -valued Function-like finite FinSequence-like FinSubsequence-like Element of (F₁() . rtO) * : ex b₃ being Relation-like NAT -defined FinTrees [: the carrier of F₂(),F₃():] -valued Function-like finite FinSequence-like FinSubsequence-like DTree-yielding FinSequence of FinTrees [: the carrier of F₂(),F₃():] st
( b₂ = b₃ & b₁ ==> ( the carrier of F₂(),F₃(),([: the carrier of F₂(),F₃():],(FinTrees [: the carrier of F₂(),F₃():]),b₃)) ) } is set
x is Element of the carrier of F₂()
n is Relation-like NAT -defined F₁() . rtO -valued Function-like finite FinSequence-like FinSubsequence-like Element of (F₁() . rtO) *
roots n is Relation-like NAT -defined Function-like finite FinSequence-like FinSubsequence-like set
pr1 (roots n) is Relation-like Function-like set
pr2 (roots n) is Relation-like Function-like set
F₅(x,(pr1 (roots n)),(pr2 (roots n))) is Element of F₃()
[x,H₃(x,n)] is V15() Element of [: the carrier of F₂(),F₃():]
{x,F₅(x,(pr1 (roots n)),(pr2 (roots n)))} is non empty finite set
{x} is non empty trivial finite V48(1) set
{{x,F₅(x,(pr1 (roots n)),(pr2 (roots n)))},{x}} is non empty finite V45() set
[x,H₃(x,n)] -tree n is Relation-like Function-like DecoratedTree-like set
tsg9 is Relation-like NAT -defined FinTrees [: the carrier of F₂(),F₃():] -valued Function-like finite FinSequence-like FinSubsequence-like DTree-yielding FinSequence of FinTrees [: the carrier of F₂(),F₃():]
([: the carrier of F₂(),F₃():],(FinTrees [: the carrier of F₂(),F₃():]),tsg9) is Relation-like NAT -defined [: the carrier of F₂(),F₃():] -valued Function-like finite FinSequence-like FinSubsequence-like FinSequence of [: the carrier of F₂(),F₃():]
( the carrier of F₂(),F₃(),([: the carrier of F₂(),F₃():],(FinTrees [: the carrier of F₂(),F₃():]),tsg9)) is Relation-like NAT -defined the carrier of F₂() -valued Function-like finite FinSequence-like FinSubsequence-like FinSequence of the carrier of F₂()
n is Relation-like NAT -defined FinTrees [: the carrier of F₂(),F₃():] -valued Function-like finite FinSequence-like FinSubsequence-like DTree-yielding FinSequence of FinTrees [: the carrier of F₂(),F₃():]
doms n is Relation-like NAT -defined FinTrees -valued Function-like finite FinSequence-like FinSubsequence-like Tree-yielding FinTree-yielding FinSequence of FinTrees
tree (doms n) is non empty finite Tree-like set
rng n is finite set
tsg9 is set
dom n is finite Element of bool NAT
tsg9 is set
n . tsg9 is Relation-like Function-like set
dom (doms n) is finite Element of bool NAT
f2 is Relation-like [: the carrier of F₂(),F₃():] -valued Function-like DecoratedTree-like Element of FinTrees [: the carrier of F₂(),F₃():]
dom f2 is non empty finite Tree-like set
(doms n) . tsg9 is set
rng (doms n) is finite set
height (dom f2) is ext-real non negative V32() V33() V34() V35() V39() V40() finite V46() Element of NAT
tsg9 is Relation-like NAT -defined F₁() . PN -valued Function-like finite FinSequence-like FinSubsequence-like Element of (F₁() . PN) *
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,(pr1 (roots tsg9)),(pr2 (roots tsg9))) is Element of F₃()
[x,H₃(x,tsg9)] is V15() Element of [: the carrier of F₂(),F₃():]
{x,F₅(x,(pr1 (roots tsg9)),(pr2 (roots tsg9)))} is non empty finite set
{{x,F₅(x,(pr1 (roots tsg9)),(pr2 (roots tsg9)))},{x}} is non empty finite V45() set
[x,H₃(x,tsg9)] -tree tsg9 is Relation-like Function-like DecoratedTree-like set
tsg9 is Relation-like NAT -defined FinTrees [: the carrier of F₂(),F₃():] -valued Function-like finite FinSequence-like FinSubsequence-like DTree-yielding FinSequence of FinTrees [: the carrier of F₂(),F₃():]
([: the carrier of F₂(),F₃():],(FinTrees [: the carrier of F₂(),F₃():]),tsg9) is Relation-like NAT -defined [: the carrier of F₂(),F₃():] -valued Function-like finite FinSequence-like FinSubsequence-like FinSequence of [: the carrier of F₂(),F₃():]
( the carrier of F₂(),F₃(),([: the carrier of F₂(),F₃():],(FinTrees [: the carrier of F₂(),F₃():]),tsg9)) is Relation-like NAT -defined the carrier of F₂() -valued Function-like finite FinSequence-like FinSubsequence-like FinSequence of the carrier of F₂()
F₃() is non empty set
F₁() is Relation-like Function-like set
dom F₁() is set
F₁() . 0 is set
F₂() is non empty DTConstrStr
the carrier of F₂() is non empty set
[: the carrier of F₂(),F₃():] is Relation-like non empty set
Terminals F₂() is set
{ (root-tree [b₁,b₂]) where b₁ is Element of the carrier of F₂(), b₂ is Element of F₃() : ( ( b₁ in Terminals F₂() & b₂ = F₄(b₁) ) or ( b₁ ==> {} & b₂ = F₅(b₁,{},{}) ) ) } is set
FinTrees [: the carrier of F₂(),F₃():] is functional non empty constituted-DTrees DTree-set of [: the carrier of F₂(),F₃():]
Union F₁() is set
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₁() . (O + 1) is set
F₁() . O is set
(F₁() . O) * is functional non empty FinSequence-membered FinSequenceSet of F₁() . O
{ ([b₁,F₅(b₁,(pr1 (roots b₂)),(pr2 (roots b₂)))] -tree b₂) where b₁ is Element of the carrier of F₂(), b₂ is Relation-like NAT -defined F₁() . O -valued Function-like finite FinSequence-like FinSubsequence-like Element of (F₁() . O) * : ex b₃ being Relation-like NAT -defined FinTrees [: the carrier of F₂(),F₃():] -valued Function-like finite FinSequence-like FinSubsequence-like DTree-yielding FinSequence of FinTrees [: the carrier of F₂(),F₃():] st
( b₂ = b₃ & b₁ ==> ( the carrier of F₂(),F₃(),([: the carrier of F₂(),F₃():],(FinTrees [: the carrier of F₂(),F₃():]),b₃)) ) } is set
(F₁() . O) \/ { ([b₁,F₅(b₁,(pr1 (roots b₂)),(pr2 (roots b₂)))] -tree b₂) where b₁ is Element of the carrier of F₂(), b₂ is Relation-like NAT -defined F₁() . O -valued Function-like finite FinSequence-like FinSubsequence-like Element of (F₁() . O) * : ex b₃ being Relation-like NAT -defined FinTrees [: the carrier of F₂(),F₃():] -valued Function-like finite FinSequence-like FinSubsequence-like DTree-yielding FinSequence of FinTrees [: the carrier of F₂(),F₃():] st
( b₂ = b₃ & b₁ ==> ( the carrier of F₂(),F₃(),([: the carrier of F₂(),F₃():],(FinTrees [: the carrier of F₂(),F₃():]),b₃)) ) } is set
O is Relation-like [: the carrier of F₂(),F₃():] -valued Function-like DecoratedTree-like set
S is Relation-like [: the carrier of F₂(),F₃():] -valued Function-like DecoratedTree-like set
O `1 is Relation-like the carrier of F<sub>2</sub>() -valued Function-like DecoratedTree-like set
S `1 is Relation-like the carrier of F₂() -valued Function-like DecoratedTree-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₂(),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₃():] -valued Function-like DecoratedTree-like Element of FinTrees [: the carrier of F₂(),F₃():]
F₄(nt) is Element of F₃()
F₅(nt,{},{}) is Element of F₃()
x is Element of the carrier of F₂()
n is Element of F₃()
[x,n] is V15() Element of [: the carrier of F₂(),F₃():]
{x,n} is non empty finite set
{x} is non empty trivial finite V48(1) set
{{x,n},{x}} is non empty finite V45() set
root-tree [x,n] is Relation-like [: the carrier of F₂(),F₃():] -valued Function-like DecoratedTree-like Element of FinTrees [: the carrier of F₂(),F₃():]
F₄(x) is Element of F₃()
F₅(x,{},{}) is Element of F₃()
root-tree nt is Relation-like the carrier of F₂() -valued Function-like DecoratedTree-like Element of FinTrees the carrier of F₂()
FinTrees the carrier of F₂() is functional non empty constituted-DTrees DTree-set of the carrier of F₂()
root-tree x is Relation-like the carrier of F₂() -valued Function-like DecoratedTree-like Element of FinTrees the carrier of F₂()
n is Element of the carrier of F₂()
tsg9 is Element of the carrier of F₂()
{ b₁ where b₁ is Element of the carrier of F₂() : for b₂ being Relation-like NAT -defined Function-like finite FinSequence-like FinSubsequence-like set holds not b₁ ==> b₂ } is set
O is ext-real non negative V32() V33() V34() V35() V39() V40() finite V46() Element of NAT
F₁() . O is set
O + 1 is non empty ext-real positive non negative V32() V33() V34() V35() V39() V40() finite V46() Element of NAT
F₁() . (O + 1) is set
S is Relation-like [: the carrier of F₂(),F₃():] -valued Function-like DecoratedTree-like set
nt is Relation-like [: the carrier of F₂(),F₃():] -valued Function-like DecoratedTree-like set
S `1 is Relation-like the carrier of F<sub>2</sub>() -valued Function-like DecoratedTree-like set
nt `1 is Relation-like the carrier of F₂() -valued Function-like DecoratedTree-like set
dom S is non empty Tree-like set
dom (S `1) is non empty Tree-like set
dom nt is non empty Tree-like set
bool (FinTrees [: the carrier of F<sub>2</sub>(),F<sub>3</sub>():]) is non empty set
n is functional constituted-DTrees Element of bool (FinTrees [: the carrier of F<sub>2</sub>(),F<sub>3</sub>():])
rtO is Relation-like [: the carrier of F<sub>2</sub>(),F<sub>3</sub>():] -valued Function-like DecoratedTree-like Element of FinTrees [: the carrier of F<sub>2</sub>(),F<sub>3</sub>():]
dom rtO is non empty finite Tree-like set
height (dom rtO) is ext-real non negative V32() V33() V34() V35() V39() V40() finite V46() Element of NAT
x is Relation-like [: the carrier of F<sub>2</sub>(),F<sub>3</sub>():] -valued Function-like DecoratedTree-like Element of FinTrees [: the carrier of F<sub>2</sub>(),F<sub>3</sub>():]
(F<sub>1</sub>() . O) * is functional non empty FinSequence-membered FinSequenceSet of F<sub>1</sub>() . O
{ ([b<sub>1</sub>,H<sub>3</sub>(b<sub>1</sub>,b<sub>2</sub>)] -tree b<sub>2</sub>) where b<sub>1</sub> is Element of the carrier of F<sub>2</sub>(), b<sub>2</sub> is Relation-like NAT -defined F<sub>1</sub>() . O -valued Function-like finite FinSequence-like FinSubsequence-like Element of (F<sub>1</sub>() . O) * : ex b<sub>3</sub> being Relation-like NAT -defined FinTrees [: the carrier of F<sub>2</sub>(),F<sub>3</sub>():] -valued Function-like finite FinSequence-like FinSubsequence-like DTree-yielding FinSequence of FinTrees [: the carrier of F<sub>2</sub>(),F<sub>3</sub>():] st
( b<sub>2</sub> = b<sub>3</sub> & b<sub>1</sub> ==> ( the carrier of F<sub>2</sub>(),F<sub>3</sub>(),([: the carrier of F<sub>2</sub>(),F<sub>3</sub>():],(FinTrees [: the carrier of F<sub>2</sub>(),F<sub>3</sub>():]),b<sub>3</sub>)) ) } is set
(F<sub>1</sub>() . O) \/ { ([b<sub>1</sub>,H<sub>3</sub>(b<sub>1</sub>,b<sub>2</sub>)] -tree b<sub>2</sub>) where b<sub>1</sub> is Element of the carrier of F<sub>2</sub>(), b<sub>2</sub> is Relation-like NAT -defined F<sub>1</sub>() . O -valued Function-like finite FinSequence-like FinSubsequence-like Element of (F<sub>1</sub>() . O) * : ex b<sub>3</sub> being Relation-like NAT -defined FinTrees [: the carrier of F<sub>2</sub>(),F<sub>3</sub>():] -valued Function-like finite FinSequence-like FinSubsequence-like DTree-yielding FinSequence of FinTrees [: the carrier of F<sub>2</sub>(),F<sub>3</sub>():] st
( b<sub>2</sub> = b<sub>3</sub> & b<sub>1</sub> ==> ( the carrier of F<sub>2</sub>(),F<sub>3</sub>(),([: the carrier of F<sub>2</sub>(),F<sub>3</sub>():],(FinTrees [: the carrier of F<sub>2</sub>(),F<sub>3</sub>():]),b<sub>3</sub>)) ) } is set
n is Element of the carrier of F<sub>2</sub>()
n is Relation-like NAT -defined F<sub>1</sub>() . O -valued Function-like finite FinSequence-like FinSubsequence-like Element of (F<sub>1</sub>() . O) *
roots n is Relation-like NAT -defined Function-like finite FinSequence-like FinSubsequence-like set
pr1 (roots n) is Relation-like Function-like set
pr2 (roots n) is Relation-like Function-like set
F<sub>5</sub>(n,(pr1 (roots n)),(pr2 (roots n))) is Element of F<sub>3</sub>()
[n,H<sub>3</sub>(n,n)] is V15() Element of [: the carrier of F<sub>2</sub>(),F<sub>3</sub>():]
{n,F<sub>5</sub>(n,(pr1 (roots n)),(pr2 (roots n)))} is non empty finite set
{n} is non empty trivial finite V48(1) set
{{n,F<sub>5</sub>(n,(pr1 (roots n)),(pr2 (roots n)))},{n}} is non empty finite V45() set
[n,H<sub>3</sub>(n,n)] -tree n is Relation-like Function-like DecoratedTree-like set
rtO is Relation-like [: the carrier of F<sub>2</sub>(),F<sub>3</sub>():] -valued Function-like DecoratedTree-like Element of FinTrees [: the carrier of F<sub>2</sub>(),F<sub>3</sub>():]
dom rtO is non empty finite Tree-like set
height (dom rtO) is ext-real non negative V32() V33() V34() V35() V39() V40() finite V46() Element of NAT
x is Relation-like [: the carrier of F<sub>2</sub>(),F<sub>3</sub>():] -valued Function-like DecoratedTree-like Element of FinTrees [: the carrier of F<sub>2</sub>(),F<sub>3</sub>():]
tsg9 is Element of the carrier of F<sub>2</sub>()
tsg9 is Relation-like NAT -defined F<sub>1</sub>() . O -valued Function-like finite FinSequence-like FinSubsequence-like Element of (F<sub>1</sub>() . O) *
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<sub>5</sub>(tsg9,(pr1 (roots tsg9)),(pr2 (roots tsg9))) is Element of F<sub>3</sub>()
[tsg9,H<sub>3</sub>(tsg9,tsg9)] is V15() Element of [: the carrier of F<sub>2</sub>(),F<sub>3</sub>():]
{tsg9,F<sub>5</sub>(tsg9,(pr1 (roots tsg9)),(pr2 (roots tsg9)))} is non empty finite set
{tsg9} is non empty trivial finite V48(1) set
{{tsg9,F<sub>5</sub>(tsg9,(pr1 (roots tsg9)),(pr2 (roots tsg9)))},{tsg9}} is non empty finite V45() set
[tsg9,H<sub>3</sub>(tsg9,tsg9)] -tree tsg9 is Relation-like Function-like DecoratedTree-like set
nt is Relation-like NAT -defined FinTrees [: the carrier of F<sub>2</sub>(),F<sub>3</sub>():] -valued Function-like finite FinSequence-like FinSubsequence-like DTree-yielding FinSequence of FinTrees [: the carrier of F<sub>2</sub>(),F<sub>3</sub>():]
([: the carrier of F<sub>2</sub>(),F<sub>3</sub>():],(FinTrees [: the carrier of F<sub>2</sub>(),F<sub>3</sub>():]),nt) is Relation-like NAT -defined [: the carrier of F<sub>2</sub>(),F<sub>3</sub>():] -valued Function-like finite FinSequence-like FinSubsequence-like FinSequence of [: the carrier of F<sub>2</sub>(),F<sub>3</sub>():]
( the carrier of F<sub>2</sub>(),F<sub>3</sub>(),([: the carrier of F<sub>2</sub>(),F<sub>3</sub>():],(FinTrees [: the carrier of F<sub>2</sub>(),F<sub>3</sub>():]),nt)) is Relation-like NAT -defined the carrier of F<sub>2</sub>() -valued Function-like finite FinSequence-like FinSubsequence-like FinSequence of the carrier of F<sub>2</sub>()
FinTrees the carrier of F<sub>2</sub>() is functional non empty constituted-DTrees DTree-set of the carrier of F<sub>2</sub>()
f2 is Relation-like NAT -defined FinTrees [: the carrier of F<sub>2</sub>(),F<sub>3</sub>():] -valued Function-like finite FinSequence-like FinSubsequence-like DTree-yielding FinSequence of FinTrees [: the carrier of F<sub>2</sub>(),F<sub>3</sub>():]
dom f2 is finite Element of bool NAT
roots f2 is Relation-like NAT -defined Function-like finite FinSequence-like FinSubsequence-like set
pr1 (roots f2) is Relation-like Function-like set
pr2 (roots f2) is Relation-like Function-like set
F<sub>5</sub>(n,(pr1 (roots f2)),(pr2 (roots f2))) is Element of F<sub>3</sub>()
[n,H<sub>3</sub>(n,f2)] is V15() Element of [: the carrier of F<sub>2</sub>(),F<sub>3</sub>():]
{n,F<sub>5</sub>(n,(pr1 (roots f2)),(pr2 (roots f2)))} is non empty finite set
{{n,F<sub>5</sub>(n,(pr1 (roots f2)),(pr2 (roots f2)))},{n}} is non empty finite V45() set
[n,H<sub>3</sub>(n,f2)] -tree f2 is Relation-like [: the carrier of F<sub>2</sub>(),F<sub>3</sub>():] -valued Function-like DecoratedTree-like Element of FinTrees [: the carrier of F<sub>2</sub>(),F<sub>3</sub>():]
([n,H<sub>3</sub>(n,f2)] -tree f2) `1 is Relation-like the carrier of F₂() -valued Function-like DecoratedTree-like set
nt is Relation-like NAT -defined FinTrees the carrier of F₂() -valued Function-like finite FinSequence-like FinSubsequence-like DTree-yielding FinSequence of FinTrees the carrier of F₂()
dom nt is finite Element of bool NAT
n -tree nt is Relation-like the carrier of F₂() -valued Function-like DecoratedTree-like Element of FinTrees the carrier of F₂()
p21 is Relation-like NAT -defined FinTrees [: the carrier of F₂(),F₃():] -valued Function-like finite FinSequence-like FinSubsequence-like DTree-yielding FinSequence of FinTrees [: the carrier of F₂(),F₃():]
([: the carrier of F₂(),F₃():],(FinTrees [: the carrier of F₂(),F₃():]),p21) is Relation-like NAT -defined [: the carrier of F₂(),F₃():] -valued Function-like finite FinSequence-like FinSubsequence-like FinSequence of [: the carrier of F₂(),F₃():]
( the carrier of F₂(),F₃(),([: the carrier of F₂(),F₃():],(FinTrees [: the carrier of F₂(),F₃():]),p21)) is Relation-like NAT -defined the carrier of F₂() -valued Function-like finite FinSequence-like FinSubsequence-like FinSequence of the carrier of F₂()
ts is Relation-like NAT -defined FinTrees [: the carrier of F₂(),F₃():] -valued Function-like finite FinSequence-like FinSubsequence-like DTree-yielding FinSequence of FinTrees [: the carrier of F₂(),F₃():]
dom ts is finite Element of bool NAT
roots ts is Relation-like NAT -defined Function-like finite FinSequence-like FinSubsequence-like set
pr1 (roots ts) is Relation-like Function-like set
pr2 (roots ts) is Relation-like Function-like set
F₅(tsg9,(pr1 (roots ts)),(pr2 (roots ts))) is Element of F₃()
[tsg9,H₃(tsg9,ts)] is V15() Element of [: the carrier of F₂(),F₃():]
{tsg9,F₅(tsg9,(pr1 (roots ts)),(pr2 (roots ts)))} is non empty finite set
{{tsg9,F₅(tsg9,(pr1 (roots ts)),(pr2 (roots ts)))},{tsg9}} is non empty finite V45() set
[tsg9,H₃(tsg9,ts)] -tree ts is Relation-like [: the carrier of F₂(),F₃():] -valued Function-like DecoratedTree-like Element of FinTrees [: the carrier of F₂(),F₃():]
([tsg9,H₃(tsg9,ts)] -tree ts) `1 is Relation-like the carrier of F<sub>2</sub>() -valued Function-like DecoratedTree-like set
p21 is Relation-like NAT -defined FinTrees the carrier of F<sub>2</sub>() -valued Function-like finite FinSequence-like FinSubsequence-like DTree-yielding FinSequence of FinTrees the carrier of F<sub>2</sub>()
dom p21 is finite Element of bool NAT
tsg9 -tree p21 is Relation-like the carrier of F<sub>2</sub>() -valued Function-like DecoratedTree-like Element of FinTrees the carrier of F<sub>2</sub>()
k is ext-real non negative V32() V33() V34() V35() V39() V40() finite V46() set
f2 . k is Relation-like Function-like set
nt . k is Relation-like Function-like set
p1k is Relation-like [: the carrier of F<sub>2</sub>(),F<sub>3</sub>():] -valued Function-like DecoratedTree-like Element of FinTrees [: the carrier of F<sub>2</sub>(),F<sub>3</sub>():]
p1k `1 is Relation-like the carrier of F₂() -valued Function-like DecoratedTree-like set
ts . k is Relation-like Function-like set
p21 . k is Relation-like Function-like set
p2k is Relation-like [: the carrier of F₂(),F₃():] -valued Function-like DecoratedTree-like Element of FinTrees [: the carrier of F₂(),F₃():]
p2k `1 is Relation-like the carrier of F<sub>2</sub>() -valued Function-like DecoratedTree-like set
O is Relation-like [: the carrier of F<sub>2</sub>(),F<sub>3</sub>():] -valued Function-like DecoratedTree-like set
S is Relation-like [: the carrier of F<sub>2</sub>(),F<sub>3</sub>():] -valued Function-like DecoratedTree-like set
O `1 is Relation-like the carrier of F₂() -valued Function-like DecoratedTree-like set
S `1 is Relation-like the carrier of F<sub>2</sub>() -valued Function-like DecoratedTree-like set
nt is set
F<sub>1</sub>() . nt is set
rtO is set
F<sub>1</sub>() . rtO is set
{ ([b<sub>1</sub>,F<sub>5</sub>(b<sub>1</sub>,(pr1 (roots b<sub>2</sub>)),(pr2 (roots b<sub>2</sub>)))] -tree b<sub>2</sub>) where b<sub>1</sub> is Element of the carrier of F<sub>2</sub>(), b<sub>2</sub> is Relation-like NAT -defined F<sub>1</sub>() . a<sub>1</sub> -valued Function-like finite FinSequence-like FinSubsequence-like Element of (F<sub>1</sub>() . a<sub>1</sub>) * : ex b<sub>3</sub> being Relation-like NAT -defined FinTrees [: the carrier of F<sub>2</sub>(),F<sub>3</sub>():] -valued Function-like finite FinSequence-like FinSubsequence-like DTree-yielding FinSequence of FinTrees [: the carrier of F<sub>2</sub>(),F<sub>3</sub>():] st
( b<sub>2</sub> = b<sub>3</sub> & b<sub>1</sub> ==> ( the carrier of F<sub>2</sub>(),F<sub>3</sub>(),([: the carrier of F<sub>2</sub>(),F<sub>3</sub>():],(FinTrees [: the carrier of F<sub>2</sub>(),F<sub>3</sub>():]),b<sub>3</sub>)) ) } is set
n is ext-real non negative V32() V33() V34() V35() V39() V40() finite V46() Element of NAT
F<sub>1</sub>() . n is set
n + 1 is non empty ext-real positive non negative V32() V33() V34() V35() V39() V40() finite V46() Element of NAT
F<sub>1</sub>() . (n + 1) is set
(F<sub>1</sub>() . n) * is functional non empty FinSequence-membered FinSequenceSet of F<sub>1</sub>() . n
{ ([b<sub>1</sub>,F<sub>5</sub>(b<sub>1</sub>,(pr1 (roots b<sub>2</sub>)),(pr2 (roots b<sub>2</sub>)))] -tree b<sub>2</sub>) where b<sub>1</sub> is Element of the carrier of F<sub>2</sub>(), b<sub>2</sub> is Relation-like NAT -defined F<sub>1</sub>() . n -valued Function-like finite FinSequence-like FinSubsequence-like Element of (F<sub>1</sub>() . n) * : ex b<sub>3</sub> being Relation-like NAT -defined FinTrees [: the carrier of F<sub>2</sub>(),F<sub>3</sub>():] -valued Function-like finite FinSequence-like FinSubsequence-like DTree-yielding FinSequence of FinTrees [: the carrier of F<sub>2</sub>(),F<sub>3</sub>():] st
( b<sub>2</sub> = b<sub>3</sub> & b<sub>1</sub> ==> ( the carrier of F<sub>2</sub>(),F<sub>3</sub>(),([: the carrier of F<sub>2</sub>(),F<sub>3</sub>():],(FinTrees [: the carrier of F<sub>2</sub>(),F<sub>3</sub>():]),b<sub>3</sub>)) ) } is set
(F<sub>1</sub>() . n) \/ H<sub>4</sub>(n,F<sub>1</sub>() . n) is set
n is ext-real non negative V32() V33() V34() V35() V39() V40() finite V46() set
F<sub>1</sub>() . n is set
tsg9 is ext-real non negative V32() V33() V34() V35() V39() V40() finite V46() set
n + tsg9 is ext-real non negative V32() V33() V34() V35() V39() V40() finite V46() set
F<sub>1</sub>() . (n + tsg9) is set
tsg9 is ext-real non negative V32() V33() V34() V35() V39() V40() finite V46() Element of NAT
f2 is ext-real non negative V32() V33() V34() V35() V39() V40() finite V46() Element of NAT
tsg9 + f2 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
F<sub>1</sub>() . x is set
F<sub>1</sub>() . n is set
n is ext-real non negative V32() V33() V34() V35() V39() V40() finite V46() set
x + n is ext-real non negative V32() V33() V34() V35() V39() V40() finite V46() Element of NAT
tsg9 is ext-real non negative V32() V33() V34() V35() V39() V40() finite V46() set
n + tsg9 is ext-real non negative V32() V33() V34() V35() V39() V40() finite V46() Element of NAT
PN is non empty DTConstrStr
the carrier of PN is non empty set
FinTrees the carrier of PN is functional non empty constituted-DTrees DTree-set of the carrier of PN
bool (FinTrees the carrier of PN) is non empty set
Terminals PN is set
[: the carrier of PN,NAT:] is Relation-like non empty non trivial non finite set
FinTrees [: the carrier of PN,NAT:] is functional non empty constituted-DTrees DTree-set of [: the carrier of PN,NAT:]
{ ([b<sub>1</sub>,H<sub>2</sub>(b<sub>1</sub>, pr1 (roots b<sub>2</sub>), pr2 (roots b<sub>2</sub>))] -tree b<sub>2</sub>) where b<sub>1</sub> is Element of the carrier of PN, b<sub>2</sub> is Relation-like NAT -defined a<sub>2</sub> -valued Function-like finite FinSequence-like FinSubsequence-like Element of a<sub>2</sub> * : ex b<sub>3</sub> being Relation-like NAT -defined FinTrees [: the carrier of PN,NAT:] -valued Function-like finite FinSequence-like FinSubsequence-like DTree-yielding FinSequence of FinTrees [: the carrier of PN,NAT:] st
( b<sub>2</sub> = b<sub>3</sub> & b<sub>1</sub> ==> ( the carrier of PN,NAT,([: the carrier of PN,NAT:],(FinTrees [: the carrier of PN,NAT:]),b<sub>3</sub>)) ) } is set
{ (root-tree [b<sub>1</sub>,b<sub>2</sub>]) where b<sub>1</sub> is Element of the carrier of PN, b<sub>2</sub> is ext-real non negative V32() V33() V34() V35() V39() V40() finite V46() Element of NAT : ( ( b<sub>1</sub> in Terminals PN & b<sub>2</sub> = H<sub>1</sub>(b<sub>1</sub>) ) or ( b<sub>1</sub> ==> {} & b<sub>2</sub> = H<sub>2</sub>(b<sub>1</sub>, {} , {} ) ) ) } is set
O is Relation-like Function-like set
dom O is set
O . 0 is set
S is ext-real non negative V32() V33() V34() V35() V39() V40() finite V46() Element of NAT
S + 1 is non empty ext-real positive non negative V32() V33() V34() V35() V39() V40() finite V46() Element of NAT
O . (S + 1) is set
O . S is set
(O . S) * is functional non empty FinSequence-membered FinSequenceSet of O . S
{ ([b<sub>1</sub>,0] -tree b<sub>2</sub>) where b<sub>1</sub> is Element of the carrier of PN, b<sub>2</sub> is Relation-like NAT -defined O . S -valued Function-like finite FinSequence-like FinSubsequence-like Element of (O . S) * : ex b<sub>3</sub> being Relation-like NAT -defined FinTrees [: the carrier of PN,NAT:] -valued Function-like finite FinSequence-like FinSubsequence-like DTree-yielding FinSequence of FinTrees [: the carrier of PN,NAT:] st
( b<sub>2</sub> = b<sub>3</sub> & b<sub>1</sub> ==> ( the carrier of PN,NAT,([: the carrier of PN,NAT:],(FinTrees [: the carrier of PN,NAT:]),b<sub>3</sub>)) ) } is set
(O . S) \/ { ([b<sub>1</sub>,0] -tree b<sub>2</sub>) where b<sub>1</sub> is Element of the carrier of PN, b<sub>2</sub> is Relation-like NAT -defined O . S -valued Function-like finite FinSequence-like FinSubsequence-like Element of (O . S) * : ex b<sub>3</sub> being Relation-like NAT -defined FinTrees [: the carrier of PN,NAT:] -valued Function-like finite FinSequence-like FinSubsequence-like DTree-yielding FinSequence of FinTrees [: the carrier of PN,NAT:] st
( b<sub>2</sub> = b<sub>3</sub> & b<sub>1</sub> ==> ( the carrier of PN,NAT,([: the carrier of PN,NAT:],(FinTrees [: the carrier of PN,NAT:]),b<sub>3</sub>)) ) } is set
Union O is set
{ (b<sub>1</sub> `1) where b₁ is Relation-like [: the carrier of PN,NAT:] -valued Function-like DecoratedTree-like Element of FinTrees [: the carrier of PN,NAT:] : b₁ in Union O } is set
S is functional constituted-DTrees Element of bool (FinTrees the carrier of PN)
O is functional constituted-DTrees Element of bool (FinTrees the carrier of PN)
S is functional constituted-DTrees Element of bool (FinTrees the carrier of PN)
F₁() is non empty DTConstrStr
the carrier of F₁() is non empty set
Terminals F₁() is set
FinTrees the carrier of F₁() is functional non empty constituted-DTrees DTree-set of the carrier of F₁()
(F₁()) is functional constituted-DTrees Element of bool (FinTrees the carrier of F₁())
bool (FinTrees the carrier of F₁()) is non empty set
[: the carrier of F₁(),NAT:] is Relation-like non empty non trivial non finite set
FinTrees [: the carrier of F₁(),NAT:] is functional non empty constituted-DTrees DTree-set of [: the carrier of F₁(),NAT:]
{ ([b₁,0] -tree b₂) where b₁ is Element of the carrier of F₁(), b₂ is Relation-like NAT -defined a₂ -valued Function-like finite FinSequence-like FinSubsequence-like Element of a₂ * : ex b₃ being Relation-like NAT -defined FinTrees [: the carrier of F₁(),NAT:] -valued Function-like finite FinSequence-like FinSubsequence-like DTree-yielding FinSequence of FinTrees [: the carrier of F₁(),NAT:] st
( b₂ = b₃ & b₁ ==> ( the carrier of F₁(),NAT,([: the carrier of F₁(),NAT:],(FinTrees [: the carrier of F₁(),NAT:]),b₃)) ) } is set
{ (root-tree [b₁,b₂]) where b₁ is Element of the carrier of F₁(), b₂ is ext-real non negative V32() V33() V34() V35() V39() V40() finite V46() Element of NAT : ( ( b₁ in Terminals F₁() & b₂ = H₁(b₁) ) or ( b₁ ==> {} & b₂ = H₂(b₁, {} , {} ) ) ) } is set
PN is Relation-like Function-like set
dom PN is set
PN . 0 is set
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
PN . (O + 1) is set
PN . O is set
(PN . O) * is functional non empty FinSequence-membered FinSequenceSet of PN . O
{ ([b₁,0] -tree b₂) where b₁ is Element of the carrier of F₁(), b₂ is Relation-like NAT -defined PN . O -valued Function-like finite FinSequence-like FinSubsequence-like Element of (PN . O) * : ex b₃ being Relation-like NAT -defined FinTrees [: the carrier of F₁(),NAT:] -valued Function-like finite FinSequence-like FinSubsequence-like DTree-yielding FinSequence of FinTrees [: the carrier of F₁(),NAT:] st
( b₂ = b₃ & b₁ ==> ( the carrier of F₁(),NAT,([: the carrier of F₁(),NAT:],(FinTrees [: the carrier of F₁(),NAT:]),b₃)) ) } is set
(PN . O) \/ { ([b₁,0] -tree b₂) where b₁ is Element of the carrier of F₁(), b₂ is Relation-like NAT -defined PN . O -valued Function-like finite FinSequence-like FinSubsequence-like Element of (PN . O) * : ex b₃ being Relation-like NAT -defined FinTrees [: the carrier of F₁(),NAT:] -valued Function-like finite FinSequence-like FinSubsequence-like DTree-yielding FinSequence of FinTrees [: the carrier of F₁(),NAT:] st
( b₂ = b₃ & b₁ ==> ( the carrier of F₁(),NAT,([: the carrier of F₁(),NAT:],(FinTrees [: the carrier of F₁(),NAT:]),b₃)) ) } is set
bool (FinTrees [: the carrier of F₁(),NAT:]) is non empty set
Union PN is set
{ (b₁ `1) where b<sub>1</sub> is Relation-like [: the carrier of F<sub>1</sub>(),NAT:] -valued Function-like DecoratedTree-like Element of FinTrees [: the carrier of F<sub>1</sub>(),NAT:] : b<sub>1</sub> in Union PN } is set
O is functional constituted-DTrees Element of bool (FinTrees the carrier of F<sub>1</sub>())
S is Relation-like [: the carrier of F<sub>1</sub>(),NAT:] -valued Function-like DecoratedTree-like set
S `1 is Relation-like the carrier of F₁() -valued Function-like DecoratedTree-like set
<*> (F₁()) is Relation-like non-empty empty-yielding NAT -defined (F₁()) -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 (F₁()) *
(F₁()) * is functional non empty FinSequence-membered FinSequenceSet of (F₁())
roots (<*> (F₁())) is Relation-like NAT -defined Function-like finite FinSequence-like FinSubsequence-like set
PN is Element of the carrier of F₁()
O is ext-real non negative V32() V33() V34() V35() V39() V40() finite V46() Element of NAT
[PN,O] is V15() Element of [: the carrier of F₁(),NAT:]
{PN,O} is non empty finite set
{PN} is non empty trivial finite V48(1) set
{{PN,O},{PN}} is non empty finite V45() set
root-tree [PN,O] is Relation-like [: the carrier of F₁(),NAT:] -valued Function-like DecoratedTree-like Element of FinTrees [: the carrier of F₁(),NAT:]
root-tree PN is Relation-like the carrier of F₁() -valued Function-like DecoratedTree-like Element of FinTrees the carrier of F₁()
PN -tree (<*> (F₁())) is Relation-like Function-like DecoratedTree-like set
rng (<*> (F₁())) is Relation-like non-empty empty-yielding NAT -defined RAT -valued Function-like one-to-one constant functional empty trivial 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() V94() V95() V96() V97() V102() V103() V104() V107() set
S is Relation-like the carrier of F₁() -valued Function-like DecoratedTree-like set
S is ext-real non negative V32() V33() V34() V35() V39() V40() finite V46() Element of NAT
PN . S is set
S + 1 is non empty ext-real positive non negative V32() V33() V34() V35() V39() V40() finite V46() Element of NAT
PN . (S + 1) is set
TSPN is Relation-like [: the carrier of F₁(),NAT:] -valued Function-like DecoratedTree-like set
TSPN `1 is Relation-like the carrier of F<sub>1</sub>() -valued Function-like DecoratedTree-like set
(PN . S) * is functional non empty FinSequence-membered FinSequenceSet of PN . S
{ ([b<sub>1</sub>,0] -tree b<sub>2</sub>) where b<sub>1</sub> is Element of the carrier of F<sub>1</sub>(), b<sub>2</sub> is Relation-like NAT -defined PN . S -valued Function-like finite FinSequence-like FinSubsequence-like Element of (PN . S) * : ex b<sub>3</sub> being Relation-like NAT -defined FinTrees [: the carrier of F<sub>1</sub>(),NAT:] -valued Function-like finite FinSequence-like FinSubsequence-like DTree-yielding FinSequence of FinTrees [: the carrier of F<sub>1</sub>(),NAT:] st
( b<sub>2</sub> = b<sub>3</sub> & b<sub>1</sub> ==> ( the carrier of F<sub>1</sub>(),NAT,([: the carrier of F<sub>1</sub>(),NAT:],(FinTrees [: the carrier of F<sub>1</sub>(),NAT:]),b<sub>3</sub>)) ) } is set
(PN . S) \/ { ([b<sub>1</sub>,0] -tree b<sub>2</sub>) where b<sub>1</sub> is Element of the carrier of F<sub>1</sub>(), b<sub>2</sub> is Relation-like NAT -defined PN . S -valued Function-like finite FinSequence-like FinSubsequence-like Element of (PN . S) * : ex b<sub>3</sub> being Relation-like NAT -defined FinTrees [: the carrier of F<sub>1</sub>(),NAT:] -valued Function-like finite FinSequence-like FinSubsequence-like DTree-yielding FinSequence of FinTrees [: the carrier of F<sub>1</sub>(),NAT:] st
( b<sub>2</sub> = b<sub>3</sub> & b<sub>1</sub> ==> ( the carrier of F<sub>1</sub>(),NAT,([: the carrier of F<sub>1</sub>(),NAT:],(FinTrees [: the carrier of F<sub>1</sub>(),NAT:]),b<sub>3</sub>)) ) } is set
PN is Element of the carrier of F<sub>1</sub>()
[PN,0] is V15() Element of [: the carrier of F<sub>1</sub>(),NAT:]
{PN,0} is non empty finite set
{PN} is non empty trivial finite V48(1) set
{{PN,0},{PN}} is non empty finite V45() set
O is Relation-like NAT -defined PN . S -valued Function-like finite FinSequence-like FinSubsequence-like Element of (PN . S) *
[PN,0] -tree O is Relation-like Function-like DecoratedTree-like set
rng PN is set
union (rng PN) is set
rng O is finite set
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<sub>1</sub> where b<sub>1</sub> is ext-real non negative V32() V33() V34() V35() V39() V40() finite V46() Element of NAT : ( 1 <= b<sub>1</sub> & b<sub>1</sub> <= len O ) } is set
S is ext-real non negative V32() V33() V34() V35() V39() V40() finite V46() set
O . S is set
rtO is functional constituted-DTrees Element of bool (FinTrees [: the carrier of F<sub>1</sub>(),NAT:])
nt is Relation-like [: the carrier of F<sub>1</sub>(),NAT:] -valued Function-like DecoratedTree-like Element of FinTrees [: the carrier of F<sub>1</sub>(),NAT:]
nt `1 is Relation-like the carrier of F₁() -valued Function-like DecoratedTree-like set
pr1 ( the carrier of F₁(),NAT) is Relation-like Function-like V18([: the carrier of F₁(),NAT:], the carrier of F₁()) Element of bool [:[: the carrier of F₁(),NAT:], the carrier of F₁():]
[:[: the carrier of F₁(),NAT:], the carrier of F₁():] is Relation-like non empty non trivial non finite set
bool [:[: the carrier of F₁(),NAT:], the carrier of F₁():] is non empty non trivial non finite set
nt * (pr1 ( the carrier of F₁(),NAT)) is Relation-like Function-like DecoratedTree-like set
rng nt is set
dom (pr1 ( the carrier of F₁(),NAT)) is set
dom (nt `1) is non empty Tree-like set
dom nt is non empty finite Tree-like set
rtO is Relation-like the carrier of F<sub>1</sub>() -valued Function-like DecoratedTree-like Element of FinTrees the carrier of F<sub>1</sub>()
S is Relation-like NAT -defined FinTrees the carrier of F<sub>1</sub>() -valued Function-like finite FinSequence-like FinSubsequence-like DTree-yielding FinSequence of FinTrees the carrier of F<sub>1</sub>()
dom S is finite Element of bool NAT
Trees [: the carrier of F<sub>1</sub>(),NAT:] is functional non empty constituted-DTrees DTree-set of [: the carrier of F<sub>1</sub>(),NAT:]
rtO is Relation-like NAT -defined FinTrees [: the carrier of F<sub>1</sub>(),NAT:] -valued Function-like finite FinSequence-like FinSubsequence-like DTree-yielding FinSequence of FinTrees [: the carrier of F<sub>1</sub>(),NAT:]
([: the carrier of F<sub>1</sub>(),NAT:],(FinTrees [: the carrier of F<sub>1</sub>(),NAT:]),rtO) is Relation-like NAT -defined [: the carrier of F<sub>1</sub>(),NAT:] -valued Function-like finite FinSequence-like FinSubsequence-like FinSequence of [: the carrier of F<sub>1</sub>(),NAT:]
( the carrier of F<sub>1</sub>(),NAT,([: the carrier of F<sub>1</sub>(),NAT:],(FinTrees [: the carrier of F<sub>1</sub>(),NAT:]),rtO)) is Relation-like NAT -defined the carrier of F<sub>1</sub>() -valued Function-like finite FinSequence-like FinSubsequence-like FinSequence of the carrier of F<sub>1</sub>()
( the carrier of F<sub>1</sub>(),(FinTrees the carrier of F<sub>1</sub>()),S) is Relation-like NAT -defined the carrier of F<sub>1</sub>() -valued Function-like finite FinSequence-like FinSubsequence-like FinSequence of the carrier of F<sub>1</sub>()
dom ( the carrier of F<sub>1</sub>(),(FinTrees the carrier of F<sub>1</sub>()),S) is finite Element of bool NAT
nt is Relation-like NAT -defined Trees [: the carrier of F<sub>1</sub>(),NAT:] -valued Function-like finite FinSequence-like FinSubsequence-like DTree-yielding FinSequence of Trees [: the carrier of F<sub>1</sub>(),NAT:]
([: the carrier of F<sub>1</sub>(),NAT:],(Trees [: the carrier of F<sub>1</sub>(),NAT:]),nt) is Relation-like NAT -defined [: the carrier of F<sub>1</sub>(),NAT:] -valued Function-like finite FinSequence-like FinSubsequence-like FinSequence of [: the carrier of F<sub>1</sub>(),NAT:]
( the carrier of F<sub>1</sub>(),NAT,([: the carrier of F<sub>1</sub>(),NAT:],(Trees [: the carrier of F<sub>1</sub>(),NAT:]),nt)) is Relation-like NAT -defined the carrier of F<sub>1</sub>() -valued Function-like finite FinSequence-like FinSubsequence-like FinSequence of the carrier of F<sub>1</sub>()
dom ( the carrier of F<sub>1</sub>(),NAT,([: the carrier of F<sub>1</sub>(),NAT:],(Trees [: the carrier of F<sub>1</sub>(),NAT:]),nt)) is finite Element of bool NAT
dom ([: the carrier of F<sub>1</sub>(),NAT:],(Trees [: the carrier of F<sub>1</sub>(),NAT:]),nt) is finite Element of bool NAT
rtO is ext-real non negative V32() V33() V34() V35() V39() V40() finite V46() set
nt . rtO is Relation-like Function-like set
S . rtO is Relation-like Function-like set
x is Relation-like [: the carrier of F<sub>1</sub>(),NAT:] -valued Function-like DecoratedTree-like Element of FinTrees [: the carrier of F<sub>1</sub>(),NAT:]
x `1 is Relation-like the carrier of F₁() -valued Function-like DecoratedTree-like set
dom x is non empty finite Tree-like set
( the carrier of F₁(),(FinTrees the carrier of F₁()),S) . rtO is set
n is Relation-like NAT -defined NAT -valued Function-like finite FinSequence-like FinSubsequence-like V90() V91() V92() V93() Element of dom x
x . n is Element of [: the carrier of F₁(),NAT:]
(x . n) `1 is Element of the carrier of F<sub>1</sub>()
n is Relation-like Function-like DecoratedTree-like set
n . {} is set
([: the carrier of F<sub>1</sub>(),NAT:],(Trees [: the carrier of F<sub>1</sub>(),NAT:]),nt) . rtO is set
( the carrier of F<sub>1</sub>(),NAT,([: the carrier of F<sub>1</sub>(),NAT:],(Trees [: the carrier of F<sub>1</sub>(),NAT:]),nt)) . rtO is set
n is Relation-like Function-like DecoratedTree-like set
n . {} is set
rng S is finite set
rtO is set
x is set
S . x is Relation-like Function-like set
n is ext-real non negative V32() V33() V34() V35() V39() V40() finite V46() Element of NAT
nt . n is Relation-like Function-like set
S . n is Relation-like Function-like set
n is Relation-like [: the carrier of F<sub>1</sub>(),NAT:] -valued Function-like DecoratedTree-like Element of FinTrees [: the carrier of F<sub>1</sub>(),NAT:]
n `1 is Relation-like the carrier of F₁() -valued Function-like DecoratedTree-like set
x is Relation-like the carrier of F₁() -valued Function-like DecoratedTree-like set
rtO is Relation-like NAT -defined FinTrees the carrier of F₁() -valued Function-like finite FinSequence-like FinSubsequence-like DTree-yielding FinSequence of (F₁())
rng rtO is finite set
dom rtO is finite Element of bool NAT
n is set
rtO . n is Relation-like Function-like set
n is ext-real non negative V32() V33() V34() V35() V39() V40() finite V46() Element of NAT
nt . n is Relation-like Function-like set
rtO . n is Relation-like Function-like set
rng nt is finite set
tsg9 is Relation-like [: the carrier of F₁(),NAT:] -valued Function-like DecoratedTree-like Element of FinTrees [: the carrier of F₁(),NAT:]
tsg9 `1 is Relation-like the carrier of F<sub>1</sub>() -valued Function-like DecoratedTree-like set
PN -tree rtO is Relation-like the carrier of F<sub>1</sub>() -valued Function-like DecoratedTree-like Element of FinTrees the carrier of F<sub>1</sub>()
x is Relation-like NAT -defined FinTrees [: the carrier of F<sub>1</sub>(),NAT:] -valued Function-like finite FinSequence-like FinSubsequence-like DTree-yielding FinSequence of FinTrees [: the carrier of F<sub>1</sub>(),NAT:]
([: the carrier of F<sub>1</sub>(),NAT:],(FinTrees [: the carrier of F<sub>1</sub>(),NAT:]),x) is Relation-like NAT -defined [: the carrier of F<sub>1</sub>(),NAT:] -valued Function-like finite FinSequence-like FinSubsequence-like FinSequence of [: the carrier of F<sub>1</sub>(),NAT:]
( the carrier of F<sub>1</sub>(),NAT,([: the carrier of F<sub>1</sub>(),NAT:],(FinTrees [: the carrier of F<sub>1</sub>(),NAT:]),x)) is Relation-like NAT -defined the carrier of F<sub>1</sub>() -valued Function-like finite FinSequence-like FinSubsequence-like FinSequence of the carrier of F<sub>1</sub>()
Trees the carrier of F<sub>1</sub>() is functional non empty constituted-DTrees DTree-set of the carrier of F<sub>1</sub>()
n is ext-real non negative V32() V33() V34() V35() V39() V40() finite V46() Element of NAT
dom nt is finite Element of bool NAT
nt . n is Relation-like Function-like set
x is Relation-like NAT -defined Trees the carrier of F<sub>1</sub>() -valued Function-like finite FinSequence-like FinSubsequence-like DTree-yielding FinSequence of Trees the carrier of F<sub>1</sub>()
x . n is Relation-like Function-like set
n is Relation-like [: the carrier of F<sub>1</sub>(),NAT:] -valued Function-like DecoratedTree-like set
n `1 is Relation-like the carrier of F₁() -valued Function-like DecoratedTree-like set
tsg9 is Relation-like [: the carrier of F₁(),NAT:] -valued Function-like DecoratedTree-like Element of FinTrees [: the carrier of F₁(),NAT:]
tsg9 `1 is Relation-like the carrier of F<sub>1</sub>() -valued Function-like DecoratedTree-like set
S is Relation-like the carrier of F<sub>1</sub>() -valued Function-like DecoratedTree-like set
TSPN is Relation-like [: the carrier of F<sub>1</sub>(),NAT:] -valued Function-like DecoratedTree-like Element of FinTrees [: the carrier of F<sub>1</sub>(),NAT:]
TSPN `1 is Relation-like the carrier of F₁() -valued Function-like DecoratedTree-like set
PN is set
PN . PN is set
F₂() is non empty set
F₁() is non empty DTConstrStr
(F₁()) is functional constituted-DTrees Element of bool (FinTrees the carrier of F₁())
the carrier of F₁() is non empty set
FinTrees the carrier of F₁() is functional non empty constituted-DTrees DTree-set of the carrier of F₁()
bool (FinTrees the carrier of F₁()) is non empty set
[:(F₁()),F₂():] is Relation-like set
bool [:(F₁()),F₂():] is non empty set
Terminals F₁() is set
[: the carrier of F₁(),F₂():] is Relation-like non empty set
FinTrees [: the carrier of F₁(),F₂():] is functional non empty constituted-DTrees DTree-set of [: the carrier of F₁(),F₂():]
{ ([b₁,F₄(b₁,(pr1 (roots b₂)),(pr2 (roots b₂)))] -tree b₂) where b₁ is Element of the carrier of F₁(), b₂ is Relation-like NAT -defined a₂ -valued Function-like finite FinSequence-like FinSubsequence-like Element of a₂ * : ex b₃ being Relation-like NAT -defined FinTrees [: the carrier of F₁(),F₂():] -valued Function-like finite FinSequence-like FinSubsequence-like DTree-yielding FinSequence of FinTrees [: the carrier of F₁(),F₂():] st
( b₂ = b₃ & b₁ ==> ( the carrier of F₁(),F₂(),([: the carrier of F₁(),F₂():],(FinTrees [: the carrier of F₁(),F₂():]),b₃)) ) } is set
{ (root-tree [b₁,b₂]) where b₁ is Element of the carrier of F₁(), b₂ is Element of F₂() : ( ( b₁ in Terminals F₁() & b₂ = F₃(b₁) ) or ( b₁ ==> {} & b₂ = F₄(b₁,{},{}) ) ) } is set
O is Relation-like Function-like set
dom O is set
O . 0 is set
S is ext-real non negative V32() V33() V34() V35() V39() V40() finite V46() Element of NAT
S + 1 is non empty ext-real positive non negative V32() V33() V34() V35() V39() V40() finite V46() Element of NAT
O . (S + 1) is set
O . S is set
(O . S) * is functional non empty FinSequence-membered FinSequenceSet of O . S
{ ([b₁,F₄(b₁,(pr1 (roots b₂)),(pr2 (roots b₂)))] -tree b₂) where b₁ is Element of the carrier of F₁(), b₂ is Relation-like NAT -defined O . S -valued Function-like finite FinSequence-like FinSubsequence-like Element of (O . S) * : ex b₃ being Relation-like NAT -defined FinTrees [: the carrier of F₁(),F₂():] -valued Function-like finite FinSequence-like FinSubsequence-like DTree-yielding FinSequence of FinTrees [: the carrier of F₁(),F₂():] st
( b₂ = b₃ & b₁ ==> ( the carrier of F₁(),F₂(),([: the carrier of F₁(),F₂():],(FinTrees [: the carrier of F₁(),F₂():]),b₃)) ) } is set
(O . S) \/ { ([b₁,F₄(b₁,(pr1 (roots b₂)),(pr2 (roots b₂)))] -tree b₂) where b₁ is Element of the carrier of F₁(), b₂ is Relation-like NAT -defined O . S -valued Function-like finite FinSequence-like FinSubsequence-like Element of (O . S) * : ex b₃ being Relation-like NAT -defined FinTrees [: the carrier of F₁(),F₂():] -valued Function-like finite FinSequence-like FinSubsequence-like DTree-yielding FinSequence of FinTrees [: the carrier of F₁(),F₂():] st
( b₂ = b₃ & b₁ ==> ( the carrier of F₁(),F₂(),([: the carrier of F₁(),F₂():],(FinTrees [: the carrier of F₁(),F₂():]),b₃)) ) } is set
Union O is set
{ (b₁ `1) where b<sub>1</sub> is Relation-like [: the carrier of F<sub>1</sub>(),F<sub>2</sub>():] -valued Function-like DecoratedTree-like Element of FinTrees [: the carrier of F<sub>1</sub>(),F<sub>2</sub>():] : b<sub>1</sub> in Union O } is set
S is functional constituted-DTrees Element of bool (FinTrees the carrier of F<sub>1</sub>())
S is set
TSPN is Relation-like [: the carrier of F<sub>1</sub>(),F<sub>2</sub>():] -valued Function-like DecoratedTree-like Element of FinTrees [: the carrier of F<sub>1</sub>(),F<sub>2</sub>():]
TSPN `1 is Relation-like the carrier of F₁() -valued Function-like DecoratedTree-like set
TSPN `2 is Relation-like F<sub>2</sub>() -valued Function-like DecoratedTree-like set
dom (TSPN `2) is non empty Tree-like set
PN is Relation-like NAT -defined NAT -valued Function-like finite FinSequence-like FinSubsequence-like V90() V91() V92() V93() Element of dom (TSPN `2)
(TSPN `2) . PN is Element of F₂()
O is Element of F₂()
S is Relation-like [: the carrier of F₁(),F₂():] -valued Function-like DecoratedTree-like set
S `1 is Relation-like the carrier of F<sub>1</sub>() -valued Function-like DecoratedTree-like set
S `2 is Relation-like F₂() -valued Function-like DecoratedTree-like set
(S `2) . {} is set
S is Relation-like Function-like set
dom S is set
rng S is set
TSPN is Relation-like Function-like V18((F<sub>1</sub>()),F<sub>2</sub>()) Element of bool [:(F<sub>1</sub>()),F<sub>2</sub>():]
bool (FinTrees [: the carrier of F<sub>1</sub>(),F<sub>2</sub>():]) is non empty set
PN is functional constituted-DTrees Element of bool (FinTrees [: the carrier of F<sub>1</sub>(),F<sub>2</sub>():])
O is Element of the carrier of F<sub>1</sub>()
F<sub>3</sub>(O) is Element of F<sub>2</sub>()
[O,F<sub>3</sub>(O)] is V15() Element of [: the carrier of F<sub>1</sub>(),F<sub>2</sub>():]
{O,F<sub>3</sub>(O)} is non empty finite set
{O} is non empty trivial finite V48(1) set
{{O,F<sub>3</sub>(O)},{O}} is non empty finite V45() set
root-tree [O,F<sub>3</sub>(O)] is Relation-like [: the carrier of F<sub>1</sub>(),F<sub>2</sub>():] -valued Function-like DecoratedTree-like Element of FinTrees [: the carrier of F<sub>1</sub>(),F<sub>2</sub>():]
(root-tree [O,F<sub>3</sub>(O)]) `1 is Relation-like the carrier of F₁() -valued Function-like DecoratedTree-like set
root-tree O is Relation-like the carrier of F₁() -valued Function-like DecoratedTree-like Element of FinTrees the carrier of F₁()
(root-tree [O,F₃(O)]) `2 is Relation-like F<sub>2</sub>() -valued Function-like DecoratedTree-like set
root-tree F<sub>3</sub>(O) is Relation-like F<sub>2</sub>() -valued Function-like DecoratedTree-like Element of FinTrees F<sub>2</sub>()
FinTrees F<sub>2</sub>() is functional non empty constituted-DTrees DTree-set of F<sub>2</sub>()
TSPN . (root-tree O) is set
(root-tree F<sub>3</sub>(O)) . {} is set
O is Element of the carrier of F<sub>1</sub>()
S is Relation-like NAT -defined FinTrees the carrier of F<sub>1</sub>() -valued Function-like finite FinSequence-like FinSubsequence-like DTree-yielding FinSequence of (F<sub>1</sub>())
( the carrier of F<sub>1</sub>(),(FinTrees the carrier of F<sub>1</sub>()),S) is Relation-like NAT -defined the carrier of F<sub>1</sub>() -valued Function-like finite FinSequence-like FinSubsequence-like FinSequence of the carrier of F<sub>1</sub>()
O -tree S is Relation-like the carrier of F<sub>1</sub>() -valued Function-like DecoratedTree-like Element of FinTrees the carrier of F<sub>1</sub>()
TSPN . (O -tree S) is set
TSPN * S is Relation-like NAT -defined F<sub>2</sub>() -valued Function-like finite FinSequence-like FinSubsequence-like FinSequence of F<sub>2</sub>()
F<sub>4</sub>(O,( the carrier of F<sub>1</sub>(),(FinTrees the carrier of F<sub>1</sub>()),S),(TSPN * S)) is Element of F<sub>2</sub>()
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<sub>1</sub> where b<sub>1</sub> is ext-real non negative V32() V33() V34() V35() V39() V40() finite V46() Element of NAT : ( 1 <= b<sub>1</sub> & b<sub>1</sub> <= len S ) } is set
x is ext-real non negative V32() V33() V34() V35() V39() V40() finite V46() set
S . x is Relation-like Function-like set
rng S is finite set
n is Relation-like [: the carrier of F<sub>1</sub>(),F<sub>2</sub>():] -valued Function-like DecoratedTree-like Element of FinTrees [: the carrier of F<sub>1</sub>(),F<sub>2</sub>():]
n `1 is Relation-like the carrier of F₁() -valued Function-like DecoratedTree-like set
x is Relation-like NAT -defined FinTrees [: the carrier of F₁(),F₂():] -valued Function-like finite FinSequence-like FinSubsequence-like DTree-yielding FinSequence of FinTrees [: the carrier of F₁(),F₂():]
dom x is finite Element of bool NAT
rng x is finite set
n is set
n is set
x . n is Relation-like Function-like set
tsg9 is ext-real non negative V32() V33() V34() V35() V39() V40() finite V46() Element of NAT
S . tsg9 is Relation-like Function-like set
tsg9 is Relation-like [: the carrier of F₁(),F₂():] -valued Function-like DecoratedTree-like set
tsg9 `1 is Relation-like the carrier of F<sub>1</sub>() -valued Function-like DecoratedTree-like set
dom ( the carrier of F<sub>1</sub>(),(FinTrees the carrier of F<sub>1</sub>()),S) is finite Element of bool NAT
n is Relation-like NAT -defined FinTrees [: the carrier of F<sub>1</sub>(),F<sub>2</sub>():] -valued Function-like finite FinSequence-like FinSubsequence-like DTree-yielding FinSequence of PN
([: the carrier of F<sub>1</sub>(),F<sub>2</sub>():],(FinTrees [: the carrier of F<sub>1</sub>(),F<sub>2</sub>():]),n) is Relation-like NAT -defined [: the carrier of F<sub>1</sub>(),F<sub>2</sub>():] -valued Function-like finite FinSequence-like FinSubsequence-like FinSequence of [: the carrier of F<sub>1</sub>(),F<sub>2</sub>():]
( the carrier of F<sub>1</sub>(),F<sub>2</sub>(),([: the carrier of F<sub>1</sub>(),F<sub>2</sub>():],(FinTrees [: the carrier of F<sub>1</sub>(),F<sub>2</sub>():]),n)) is Relation-like NAT -defined the carrier of F<sub>1</sub>() -valued Function-like finite FinSequence-like FinSubsequence-like FinSequence of the carrier of F<sub>1</sub>()
dom ( the carrier of F<sub>1</sub>(),F<sub>2</sub>(),([: the carrier of F<sub>1</sub>(),F<sub>2</sub>():],(FinTrees [: the carrier of F<sub>1</sub>(),F<sub>2</sub>():]),n)) is finite Element of bool NAT
dom ([: the carrier of F<sub>1</sub>(),F<sub>2</sub>():],(FinTrees [: the carrier of F<sub>1</sub>(),F<sub>2</sub>():]),n) is finite Element of bool NAT
( the carrier of F<sub>1</sub>(),F<sub>2</sub>(),([: the carrier of F<sub>1</sub>(),F<sub>2</sub>():],(FinTrees [: the carrier of F<sub>1</sub>(),F<sub>2</sub>():]),n)) is Relation-like NAT -defined F<sub>2</sub>() -valued Function-like finite FinSequence-like FinSubsequence-like FinSequence of F<sub>2</sub>()
dom ( the carrier of F<sub>1</sub>(),F<sub>2</sub>(),([: the carrier of F<sub>1</sub>(),F<sub>2</sub>():],(FinTrees [: the carrier of F<sub>1</sub>(),F<sub>2</sub>():]),n)) is finite Element of bool NAT
n is ext-real non negative V32() V33() V34() V35() V39() V40() finite V46() set
n . n is Relation-like Function-like set
S . n is Relation-like Function-like set
tsg9 is Relation-like [: the carrier of F<sub>1</sub>(),F<sub>2</sub>():] -valued Function-like DecoratedTree-like set
tsg9 `1 is Relation-like the carrier of F₁() -valued Function-like DecoratedTree-like set
dom tsg9 is non empty Tree-like set
( the carrier of F₁(),(FinTrees the carrier of F₁()),S) . n is set
tsg9 is Relation-like NAT -defined NAT -valued Function-like finite FinSequence-like FinSubsequence-like V90() V91() V92() V93() Element of dom tsg9
tsg9 . tsg9 is Element of [: the carrier of F₁(),F₂():]
(tsg9 . tsg9) `1 is Element of the carrier of F<sub>1</sub>()
f2 is Relation-like Function-like DecoratedTree-like set
f2 . {} is set
([: the carrier of F<sub>1</sub>(),F<sub>2</sub>():],(FinTrees [: the carrier of F<sub>1</sub>(),F<sub>2</sub>():]),n) . n is set
( the carrier of F<sub>1</sub>(),F<sub>2</sub>(),([: the carrier of F<sub>1</sub>(),F<sub>2</sub>():],(FinTrees [: the carrier of F<sub>1</sub>(),F<sub>2</sub>():]),n)) . n is set
f2 is Relation-like Function-like DecoratedTree-like set
f2 . {} is set
roots n is Relation-like NAT -defined Function-like finite FinSequence-like FinSubsequence-like set
pr1 (roots n) is Relation-like Function-like set
pr2 (roots n) is Relation-like Function-like set
F<sub>4</sub>(O,(pr1 (roots n)),(pr2 (roots n))) is Element of F<sub>2</sub>()
[O,H<sub>3</sub>(O,n)] is V15() Element of [: the carrier of F<sub>1</sub>(),F<sub>2</sub>():]
{O,F<sub>4</sub>(O,(pr1 (roots n)),(pr2 (roots n)))} is non empty finite set
{O} is non empty trivial finite V48(1) set
{{O,F<sub>4</sub>(O,(pr1 (roots n)),(pr2 (roots n)))},{O}} is non empty finite V45() set
[O,H<sub>3</sub>(O,n)] -tree n is Relation-like [: the carrier of F<sub>1</sub>(),F<sub>2</sub>():] -valued Function-like DecoratedTree-like Element of FinTrees [: the carrier of F<sub>1</sub>(),F<sub>2</sub>():]
rng n is finite set
Trees [: the carrier of F<sub>1</sub>(),F<sub>2</sub>():] is functional non empty constituted-DTrees DTree-set of [: the carrier of F<sub>1</sub>(),F<sub>2</sub>():]
rng S is finite set
Trees the carrier of F<sub>1</sub>() is functional non empty constituted-DTrees DTree-set of the carrier of F<sub>1</sub>()
tsg9 is ext-real non negative V32() V33() V34() V35() V39() V40() finite V46() Element of NAT
dom n is finite Element of bool NAT
n . tsg9 is Relation-like Function-like set
S . tsg9 is Relation-like Function-like set
f2 is Relation-like [: the carrier of F<sub>1</sub>(),F<sub>2</sub>():] -valued Function-like DecoratedTree-like set
f2 `1 is Relation-like the carrier of F₁() -valued Function-like DecoratedTree-like set
nt is Relation-like [: the carrier of F₁(),F₂():] -valued Function-like DecoratedTree-like set
nt `1 is Relation-like the carrier of F<sub>1</sub>() -valued Function-like DecoratedTree-like set
n is Relation-like NAT -defined Trees [: the carrier of F<sub>1</sub>(),F<sub>2</sub>():] -valued Function-like finite FinSequence-like FinSubsequence-like DTree-yielding FinSequence of Trees [: the carrier of F<sub>1</sub>(),F<sub>2</sub>():]
[O,H<sub>3</sub>(O,n)] -tree n is Relation-like [: the carrier of F<sub>1</sub>(),F<sub>2</sub>():] -valued Function-like DecoratedTree-like set
([O,H<sub>3</sub>(O,n)] -tree n) `1 is Relation-like the carrier of F₁() -valued Function-like DecoratedTree-like set
tsg9 is Relation-like NAT -defined Trees the carrier of F₁() -valued Function-like finite FinSequence-like FinSubsequence-like DTree-yielding FinSequence of Trees the carrier of F₁()
O -tree tsg9 is Relation-like the carrier of F₁() -valued Function-like DecoratedTree-like set
dom TSPN is set
dom (TSPN * S) is finite Element of bool NAT
tsg9 is ext-real non negative V32() V33() V34() V35() V39() V40() finite V46() set
n . tsg9 is Relation-like Function-like set
S . tsg9 is Relation-like Function-like set
f2 is Relation-like [: the carrier of F₁(),F₂():] -valued Function-like DecoratedTree-like set
f2 `1 is Relation-like the carrier of F<sub>1</sub>() -valued Function-like DecoratedTree-like set
dom f2 is non empty Tree-like set
(TSPN * S) . tsg9 is set
TSPN . (f2 `1) is set
f2 `2 is Relation-like F<sub>2</sub>() -valued Function-like DecoratedTree-like set
(f2 `2) . {} is set
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₁(),F₂():]
(f2 . nt) `2 is Element of F<sub>2</sub>()
([: the carrier of F<sub>1</sub>(),F<sub>2</sub>():],(FinTrees [: the carrier of F<sub>1</sub>(),F<sub>2</sub>():]),n) . tsg9 is set
( the carrier of F<sub>1</sub>(),F<sub>2</sub>(),([: the carrier of F<sub>1</sub>(),F<sub>2</sub>():],(FinTrees [: the carrier of F<sub>1</sub>(),F<sub>2</sub>():]),n)) . tsg9 is set
ts is Relation-like Function-like DecoratedTree-like set
ts . nt is set
[O,F<sub>4</sub>(O,( the carrier of F<sub>1</sub>(),(FinTrees the carrier of F<sub>1</sub>()),S),(TSPN * S))] is V15() Element of [: the carrier of F<sub>1</sub>(),F<sub>2</sub>():]
{O,F<sub>4</sub>(O,( the carrier of F<sub>1</sub>(),(FinTrees the carrier of F<sub>1</sub>()),S),(TSPN * S))} is non empty finite set
{{O,F<sub>4</sub>(O,( the carrier of F<sub>1</sub>(),(FinTrees the carrier of F<sub>1</sub>()),S),(TSPN * S))},{O}} is non empty finite V45() set
[O,F<sub>4</sub>(O,( the carrier of F<sub>1</sub>(),(FinTrees the carrier of F<sub>1</sub>()),S),(TSPN * S))] -tree n is Relation-like [: the carrier of F<sub>1</sub>(),F<sub>2</sub>():] -valued Function-like DecoratedTree-like Element of FinTrees [: the carrier of F<sub>1</sub>(),F<sub>2</sub>():]
dom ([O,F<sub>4</sub>(O,( the carrier of F<sub>1</sub>(),(FinTrees the carrier of F<sub>1</sub>()),S),(TSPN * S))] -tree n) is non empty finite Tree-like set
([O,F<sub>4</sub>(O,( the carrier of F<sub>1</sub>(),(FinTrees the carrier of F<sub>1</sub>()),S),(TSPN * S))] -tree n) `2 is Relation-like F₂() -valued Function-like DecoratedTree-like set
tsg9 is Relation-like NAT -defined NAT -valued Function-like finite FinSequence-like FinSubsequence-like V90() V91() V92() V93() Element of dom ([O,F₄(O,( the carrier of F₁(),(FinTrees the carrier of F₁()),S),(TSPN * S))] -tree n)
(([O,F₄(O,( the carrier of F₁(),(FinTrees the carrier of F₁()),S),(TSPN * S))] -tree n) `2) . tsg9 is set
([O,F<sub>4</sub>(O,( the carrier of F<sub>1</sub>(),(FinTrees the carrier of F<sub>1</sub>()),S),(TSPN * S))] -tree n) . tsg9 is Element of [: the carrier of F<sub>1</sub>(),F<sub>2</sub>():]
(([O,F<sub>4</sub>(O,( the carrier of F<sub>1</sub>(),(FinTrees the carrier of F<sub>1</sub>()),S),(TSPN * S))] -tree n) . tsg9) `2 is Element of F₂()
[O,F₄(O,( the carrier of F₁(),(FinTrees the carrier of F₁()),S),(TSPN * S))] `2 is Element of F₂()
F₂() is non empty set
F₁() is non empty DTConstrStr
(F₁()) is functional constituted-DTrees Element of bool (FinTrees the carrier of F₁())
the carrier of F₁() is non empty set
FinTrees the carrier of F₁() is functional non empty constituted-DTrees DTree-set of the carrier of F₁()
bool (FinTrees the carrier of F₁()) is non empty set
[:(F₁()),F₂():] is Relation-like set
bool [:(F₁()),F₂():] is non empty set
Terminals F₁() is set
F₅() is Relation-like Function-like V18((F₁()),F₂()) Element of bool [:(F₁()),F₂():]
F₆() is Relation-like Function-like V18((F₁()),F₂()) Element of bool [:(F₁()),F₂():]
O is Element of the carrier of F₁()
root-tree O is Relation-like the carrier of F₁() -valued Function-like DecoratedTree-like Element of FinTrees the carrier of F₁()
F₅() . (root-tree O) is set
F₃(O) is Element of F₂()
F₆() . (root-tree O) is set
O is Element of the carrier of F₁()
S is Relation-like NAT -defined FinTrees the carrier of F₁() -valued Function-like finite FinSequence-like FinSubsequence-like DTree-yielding FinSequence of (F₁())
( the carrier of F₁(),(FinTrees the carrier of F₁()),S) is Relation-like NAT -defined the carrier of F₁() -valued Function-like finite FinSequence-like FinSubsequence-like FinSequence of the carrier of F₁()
rng S is finite set
dom F₅() is set
F₅() * S is Relation-like NAT -defined F₂() -valued Function-like finite FinSequence-like FinSubsequence-like FinSequence of F₂()
dom (F₅() * S) is finite Element of bool NAT
dom S is finite Element of bool NAT
TSPN is Relation-like NAT -defined Function-like finite FinSequence-like FinSubsequence-like set
dom F₆() is set
F₆() * S is Relation-like NAT -defined F₂() -valued Function-like finite FinSequence-like FinSubsequence-like FinSequence of F₂()
dom (F₆() * S) is finite Element of bool NAT
O is set
S . O is Relation-like Function-like set
S is Relation-like the carrier of F₁() -valued Function-like DecoratedTree-like Element of FinTrees the carrier of F₁()
F₅() . S is set
F₆() . S is set
(F₅() * S) . O is set
(F₆() * S) . O is set
O -tree S is Relation-like the carrier of F₁() -valued Function-like DecoratedTree-like Element of FinTrees the carrier of F₁()
F₅() . (O -tree S) is set
PN is Relation-like NAT -defined F₂() -valued Function-like finite FinSequence-like FinSubsequence-like FinSequence of F₂()
F₄(O,( the carrier of F₁(),(FinTrees the carrier of F₁()),S),PN) is Element of F₂()
F₆() . (O -tree S) is set
O is set
F₅() . O is set
F₆() . O is set
<*0*> is Relation-like NAT -defined NAT -valued Function-like one-to-one constant non empty trivial finite V48(1) FinSequence-like FinSubsequence-like V90() V91() V92() V93() V94() V95() V96() V97() Element of NAT *
NAT * is functional non empty FinSequence-membered FinSequenceSet of NAT
[1,0] is V15() set
{1,0} is non empty finite V45() set
{{1,0},{1}} is non empty finite V45() set
{[1,0]} is Relation-like Function-like constant non empty trivial finite V48(1) set
<*1*> is Relation-like NAT -defined NAT -valued Function-like one-to-one constant non empty trivial finite V48(1) FinSequence-like FinSubsequence-like V90() V91() V92() V93() V94() V95() V96() V97() Element of NAT *
[1,1] is V15() set
{1,1} is non empty finite V45() set
{{1,1},{1}} is non empty finite V45() set
{[1,1]} is Relation-like Function-like constant non empty trivial finite V48(1) set
{0,1} is non empty finite V45() Element of bool NAT
() is non empty strict DTConstrStr
the carrier of () is non empty set
S is Element of the carrier of ()
O is Element of the carrier of ()
<*O*> is Relation-like NAT -defined the carrier of () -valued Function-like constant non empty trivial finite V48(1) FinSequence-like FinSubsequence-like Element of the carrier of () *
the carrier of () * is functional non empty FinSequence-membered FinSequenceSet of the carrier of ()
[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
<*S*> is Relation-like NAT -defined the carrier of () -valued Function-like constant non empty trivial finite V48(1) FinSequence-like FinSubsequence-like Element of the carrier of () *
[1,S] is V15() set
{1,S} is non empty finite set
{{1,S},{1}} is non empty finite V45() set
{[1,S]} is Relation-like Function-like constant non empty trivial finite V48(1) set
Terminals () is set
{ b₁ where b₁ is Element of the carrier of () : for b₂ being Relation-like NAT -defined Function-like finite FinSequence-like FinSubsequence-like set holds not b₁ ==> b₂ } is set
TSPN is Relation-like NAT -defined Function-like finite FinSequence-like FinSubsequence-like set
[O,TSPN] is V15() set
{O,TSPN} is non empty finite set
{O} is non empty trivial finite V48(1) set
{{O,TSPN},{O}} is non empty finite V45() set
the Rules of () is Relation-like Element of bool [: the carrier of (),( the carrier of () *):]
[: the carrier of (),( the carrier of () *):] is Relation-like non empty set
bool [: the carrier of (),( the carrier of () *):] is non empty set
{O} is non empty trivial finite V48(1) Element of bool the carrier of ()
bool the carrier of () is non empty set
TSPN is set
PN is Element of the carrier of ()
{O,S} is non empty finite Element of bool the carrier of ()
NonTerminals () is set
{ b₁ where b₁ is Element of the carrier of () : ex b₂ being Relation-like NAT -defined Function-like finite FinSequence-like FinSubsequence-like set st b₁ ==> b₂ } is set
{S} is non empty trivial finite V48(1) Element of bool the carrier of ()
TSPN is set
PN is Element of the carrier of ()
O is Relation-like NAT -defined Function-like finite FinSequence-like FinSubsequence-like set
FinTrees the carrier of () is functional non empty constituted-DTrees DTree-set of the carrier of ()
bool (FinTrees the carrier of ()) is non empty set
(()) is functional constituted-DTrees Element of bool (FinTrees the carrier of ())
TSPN is functional non empty constituted-DTrees Element of bool (FinTrees the carrier of ())
root-tree O is Relation-like the carrier of () -valued Function-like DecoratedTree-like Element of FinTrees the carrier of ()
PN is Relation-like the carrier of () -valued Function-like DecoratedTree-like ( the carrier of (), FinTrees the carrier of (),TSPN)
<*PN*> is Relation-like NAT -defined TSPN -valued Function-like constant non empty trivial finite V48(1) FinSequence-like FinSubsequence-like DTree-yielding Element of TSPN *
TSPN * is functional non empty FinSequence-membered FinSequenceSet of TSPN
[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 FinTrees the carrier of () -valued Function-like finite FinSequence-like FinSubsequence-like DTree-yielding FinSequence of TSPN
nt is Element of the carrier of ()
S is Relation-like NAT -defined FinTrees the carrier of () -valued Function-like finite FinSequence-like FinSubsequence-like DTree-yielding FinSequence of (())
( the carrier of (),(FinTrees the carrier of ()),S) is Relation-like NAT -defined the carrier of () -valued Function-like finite FinSequence-like FinSubsequence-like FinSequence of the carrier of ()
dom <*PN*> is non empty trivial finite V48(1) Element of bool NAT
dom <*O*> is non empty trivial finite V48(1) Element of bool NAT
rtO is ext-real non negative V32() V33() V34() V35() V39() V40() finite V46() Element of NAT
dom S is finite Element of bool NAT
x is Relation-like Function-like DecoratedTree-like set
<*O*> . 1 is set
n is Relation-like Function-like DecoratedTree-like set
S . rtO is Relation-like Function-like set
<*O*> . rtO is set
n . {} is set
PN is non empty () DTConstrStr
Terminals PN is set
the carrier of PN is non empty set
bool the carrier of PN is non empty set
{ b₁ where b₁ is Element of the carrier of PN : S₂[b₁] } is set
PN is non empty () DTConstrStr
(PN) is functional constituted-DTrees Element of bool (FinTrees the carrier of PN)
the carrier of PN is non empty set
FinTrees the carrier of PN is functional non empty constituted-DTrees DTree-set of the carrier of PN
bool (FinTrees the carrier of PN) is non empty set
(PN) is non empty Element of bool the carrier of PN
bool the carrier of PN is non empty set
O is set
PN is non empty () DTConstrStr
(PN) is functional constituted-DTrees Element of bool (FinTrees the carrier of PN)
the carrier of PN is non empty set
FinTrees the carrier of PN is functional non empty constituted-DTrees DTree-set of the carrier of PN
bool (FinTrees the carrier of PN) is non empty set
the Element of the carrier of PN is Element of the carrier of PN
{ b₁ where b₁ is Element of the carrier of PN : for b₂ being Relation-like NAT -defined Function-like finite FinSequence-like FinSubsequence-like set holds not b₁ ==> b₂ } is set
Terminals PN is set
{ b₁ where b₁ is Element of the carrier of PN : ex b₂ being Relation-like NAT -defined Function-like finite FinSequence-like FinSubsequence-like set st b₁ ==> b₂ } is set
S is Relation-like NAT -defined Function-like finite FinSequence-like FinSubsequence-like set
NonTerminals PN is set
S is Relation-like NAT -defined FinTrees the carrier of PN -valued Function-like finite FinSequence-like FinSubsequence-like DTree-yielding FinSequence of (PN)
( the carrier of PN,(FinTrees the carrier of PN),S) 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 Relation-like NAT -defined Function-like finite FinSequence-like FinSubsequence-like set
PN is non empty () DTConstrStr
NonTerminals PN is set
the carrier of PN is non empty set
bool the carrier of PN is non empty set
{ b₁ where b₁ is Element of the carrier of PN : S₂[b₁] } is set
PN is non empty () () DTConstrStr
the carrier of PN is non empty set
(PN) is non empty Element of bool the carrier of PN
bool the carrier of PN is non empty set
FinTrees the carrier of PN is functional non empty constituted-DTrees DTree-set of the carrier of PN
(PN) is functional non empty constituted-DTrees Element of bool (FinTrees the carrier of PN)
bool (FinTrees the carrier of PN) is non empty set
O is Element of (PN)
PN is non empty () DTConstrStr
the carrier of PN is non empty set
(PN) is non empty Element of bool the carrier of PN
bool the carrier of PN is non empty set
O is Element of (PN)
root-tree O is Relation-like Function-like DecoratedTree-like set
FinTrees the carrier of PN is functional non empty constituted-DTrees DTree-set of the carrier of PN
(PN) is functional non empty constituted-DTrees Element of bool (FinTrees the carrier of PN)
bool (FinTrees the carrier of PN) is non empty set
PN is non empty () () DTConstrStr
the carrier of PN is non empty set
(PN) is non empty Element of bool the carrier of PN
bool the carrier of PN is non empty set
FinTrees the carrier of PN is functional non empty constituted-DTrees DTree-set of the carrier of PN
O is Element of (PN)
S is Relation-like NAT -defined FinTrees the carrier of PN -valued Function-like finite FinSequence-like FinSubsequence-like DTree-yielding (PN,O)
O -tree S is Relation-like Function-like DecoratedTree-like set
(PN) is functional non empty constituted-DTrees Element of bool (FinTrees the carrier of PN)
bool (FinTrees the carrier of PN) is non empty set
( the carrier of PN,(FinTrees the carrier of PN),S) 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
the carrier of PN is non empty set
FinTrees the carrier of PN is functional non empty constituted-DTrees DTree-set of the carrier of PN
(PN) is functional non empty constituted-DTrees Element of bool (FinTrees the carrier of PN)
bool (FinTrees the carrier of PN) is non empty set
(PN) is non empty Element of bool the carrier of PN
bool the carrier of PN is non empty set
O is Relation-like the carrier of PN -valued Function-like DecoratedTree-like ( the carrier of PN, FinTrees the carrier of PN,(PN))
O . {} is set
S is Element of (PN)
(PN,S) is Relation-like the carrier of PN -valued Function-like DecoratedTree-like ( the carrier of PN, FinTrees the carrier of PN,(PN))
nt is Element of the carrier of PN
root-tree nt is Relation-like the carrier of PN -valued Function-like DecoratedTree-like Element of FinTrees the carrier of PN
(root-tree nt) . {} is set
rtO is Element of (PN)
(PN,rtO) is Relation-like the carrier of PN -valued Function-like DecoratedTree-like ( the carrier of PN, FinTrees the carrier of PN,(PN))
nt is Element of the carrier of PN
rtO is Relation-like NAT -defined FinTrees the carrier of PN -valued Function-like finite FinSequence-like FinSubsequence-like DTree-yielding FinSequence of (PN)
( the carrier of PN,(FinTrees the carrier of PN),rtO) is Relation-like NAT -defined the carrier of PN -valued Function-like finite FinSequence-like FinSubsequence-like FinSequence of the carrier of PN
rng rtO is finite set
nt -tree rtO is Relation-like the carrier of PN -valued Function-like DecoratedTree-like Element of FinTrees the carrier of PN
(nt -tree rtO) . {} is set
x is Element of (PN)
(PN,x) is Relation-like the carrier of PN -valued Function-like DecoratedTree-like ( the carrier of PN, FinTrees the carrier of PN,(PN))
{ b₁ where b₁ is Element of the carrier of PN : for b₂ being Relation-like NAT -defined Function-like finite FinSequence-like FinSubsequence-like set holds not b₁ ==> b₂ } is set
n is Element of the carrier of PN
PN is non empty () () DTConstrStr
the carrier of PN is non empty set
FinTrees the carrier of PN is functional non empty constituted-DTrees DTree-set of the carrier of PN
(PN) is functional non empty constituted-DTrees Element of bool (FinTrees the carrier of PN)
bool (FinTrees the carrier of PN) is non empty set
(PN) is non empty Element of bool the carrier of PN
bool the carrier of PN is non empty set
O is Element of the carrier of PN
(PN) is non empty Element of bool the carrier of PN
root-tree O is Relation-like the carrier of PN -valued Function-like DecoratedTree-like Element of FinTrees the carrier of PN
(root-tree O) . {} is set
S is Element of (PN)
{ b₁ where b₁ is Element of the carrier of PN : for b₂ being Relation-like NAT -defined Function-like finite FinSequence-like FinSubsequence-like set holds not b₁ ==> b₂ } is set
{ b₁ where b₁ is Element of the carrier of PN : ex b₂ being Relation-like NAT -defined Function-like finite FinSequence-like FinSubsequence-like set st b₁ ==> b₂ } is set
nt is Element of the carrier of PN
rtO is Relation-like NAT -defined Function-like finite FinSequence-like FinSubsequence-like set
x is Element of the carrier of PN
O is Element of the carrier of PN
S is Relation-like NAT -defined FinTrees the carrier of PN -valued Function-like finite FinSequence-like FinSubsequence-like DTree-yielding FinSequence of (PN)
( the carrier of PN,(FinTrees the carrier of PN),S) is Relation-like NAT -defined the carrier of PN -valued Function-like finite FinSequence-like FinSubsequence-like FinSequence of the carrier of PN
rng S is finite set
O -tree S is Relation-like the carrier of PN -valued Function-like DecoratedTree-like Element of FinTrees the carrier of PN
(O -tree S) . {} is set
nt is Element of (PN)
rtO is Relation-like NAT -defined FinTrees the carrier of PN -valued Function-like finite FinSequence-like FinSubsequence-like DTree-yielding FinSequence of (PN)
nt -tree rtO is Relation-like the carrier of PN -valued Function-like DecoratedTree-like Element of FinTrees the carrier of PN
( the carrier of PN,(FinTrees the carrier of PN),rtO) is Relation-like NAT -defined the carrier of PN -valued Function-like finite FinSequence-like FinSubsequence-like FinSequence of the carrier of PN
O is Relation-like the carrier of PN -valued Function-like DecoratedTree-like ( the carrier of PN, FinTrees the carrier of PN,(PN))
O . {} is set
S is Element of (PN)
(()) is non empty Element of bool the carrier of ()
(()) is non empty Element of bool the carrier of ()
nt is Element of (())
rtO is Relation-like the carrier of () -valued Function-like DecoratedTree-like ( the carrier of (), FinTrees the carrier of (),(()))
nt -tree rtO is Relation-like the carrier of () -valued Function-like DecoratedTree-like set
dom rtO is non empty finite Tree-like set
x is Relation-like NAT -defined NAT -valued Function-like finite FinSequence-like FinSubsequence-like V90() V91() V92() V93() Element of dom rtO
rtO . x is Element of the carrier of ()
<*rtO*> is Relation-like NAT -defined (()) -valued Function-like constant non empty trivial finite V48(1) FinSequence-like FinSubsequence-like DTree-yielding Element of (()) *
(()) * is functional non empty FinSequence-membered FinSequenceSet of (())
[1,rtO] is V15() set
{1,rtO} is non empty finite set
{{1,rtO},{1}} is non empty finite V45() set
{[1,rtO]} is Relation-like Function-like constant non empty trivial finite V48(1) set
roots <*rtO*> is Relation-like NAT -defined Function-like finite FinSequence-like FinSubsequence-like set
S is Element of (())
nt -tree <*rtO*> is Relation-like Function-like DecoratedTree-like set
nt is Relation-like NAT -defined NAT -valued Function-like finite FinSequence-like FinSubsequence-like V90() V91() V92() V93() FinSequence of NAT
nt . 1 is ext-real non negative V32() V33() V34() V35() V39() V40() finite V46() set
(nt . 1) + 1 is non empty ext-real positive non negative V32() V33() V34() V35() V39() V40() finite V46() Element of NAT
[:(()),NAT:] is Relation-like non empty non trivial non finite set
bool [:(()),NAT:] is non empty non trivial non finite set
nt is Relation-like Function-like V18((()), NAT ) Element of bool [:(()),NAT:]
rtO is Relation-like Function-like V18((()), NAT ) Element of bool [:(()),NAT:]
() is Relation-like Function-like V18((()), NAT ) Element of bool [:(()),NAT:]
nt is Relation-like the carrier of () -valued Function-like DecoratedTree-like ( the carrier of (), FinTrees the carrier of (),(()))
<*nt*> is Relation-like NAT -defined (()) -valued Function-like constant non empty trivial finite V48(1) FinSequence-like FinSubsequence-like DTree-yielding Element of (()) *
(()) * is functional non empty FinSequence-membered FinSequenceSet of (())
[1,nt] is V15() set
{1,nt} is non empty finite set
{{1,nt},{1}} is non empty finite V45() set
{[1,nt]} is Relation-like Function-like constant non empty trivial finite V48(1) set
1 -tree <*nt*> is Relation-like Function-like DecoratedTree-like set
dom nt is non empty finite Tree-like set
roots <*nt*> is Relation-like NAT -defined Function-like finite FinSequence-like FinSubsequence-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 the carrier of ()
<*(nt . rtO)*> is Relation-like NAT -defined the carrier of () -valued Function-like constant non empty trivial finite V48(1) FinSequence-like FinSubsequence-like Element of the carrier of () *
[1,(nt . rtO)] is V15() set
{1,(nt . rtO)} is non empty finite set
{{1,(nt . rtO)},{1}} is non empty finite V45() set
{[1,(nt . rtO)]} is Relation-like Function-like constant non empty trivial finite V48(1) set
O is Element of (())
S is Element of (())
[:NAT,(()):] is Relation-like non empty non trivial non finite set
bool [:NAT,(()):] is non empty non trivial non finite set
root-tree 0 is Relation-like NAT -valued Function-like DecoratedTree-like V90() V91() V92() V93() Element of FinTrees NAT
FinTrees NAT is functional non empty constituted-DTrees DTree-set of NAT
O is Element of (())
((),O) is Relation-like the carrier of () -valued Function-like DecoratedTree-like ( the carrier of (), FinTrees the carrier of (),(()))
nt is Relation-like Function-like V18( NAT ,(())) Element of bool [:NAT,(()):]
nt . 0 is Relation-like Function-like DecoratedTree-like Element of (())
nt is Relation-like Function-like V18( NAT ,(())) Element of bool [:NAT,(()):]
nt . 0 is Relation-like Function-like DecoratedTree-like Element of (())
rtO is Relation-like Function-like V18( NAT ,(())) Element of bool [:NAT,(()):]
rtO . 0 is Relation-like Function-like DecoratedTree-like Element of (())
O is Element of (())
((),O) is Relation-like the carrier of () -valued Function-like DecoratedTree-like ( the carrier of (), FinTrees the carrier of (),(()))
x is ext-real non negative V32() V33() V34() V35() V39() V40() finite V46() set
x + 1 is non empty ext-real positive non negative V32() V33() V34() V35() V39() V40() finite V46() Element of NAT
nt . (x + 1) is Relation-like Function-like DecoratedTree-like Element of (())
nt . x is Relation-like Function-like DecoratedTree-like Element of (())
((nt . x)) is Relation-like the carrier of () -valued Function-like DecoratedTree-like ( the carrier of (), FinTrees the carrier of (),(()))
<*(nt . x)*> is Relation-like NAT -defined (()) -valued Function-like constant non empty trivial finite V48(1) FinSequence-like FinSubsequence-like DTree-yielding Element of (()) *
[1,(nt . x)] is V15() set
{1,(nt . x)} is non empty finite set
{{1,(nt . x)},{1}} is non empty finite V45() set
{[1,(nt . x)]} is Relation-like Function-like constant non empty trivial finite V48(1) set
1 -tree <*(nt . x)*> is Relation-like Function-like DecoratedTree-like set
x is ext-real non negative V32() V33() V34() V35() V39() V40() finite V46() set
x + 1 is non empty ext-real positive non negative V32() V33() V34() V35() V39() V40() finite V46() Element of NAT
rtO . (x + 1) is Relation-like Function-like DecoratedTree-like Element of (())
rtO . x is Relation-like Function-like DecoratedTree-like Element of (())
((rtO . x)) is Relation-like the carrier of () -valued Function-like DecoratedTree-like ( the carrier of (), FinTrees the carrier of (),(()))
<*(rtO . x)*> is Relation-like NAT -defined (()) -valued Function-like constant non empty trivial finite V48(1) FinSequence-like FinSubsequence-like DTree-yielding Element of (()) *
[1,(rtO . x)] is V15() set
{1,(rtO . x)} is non empty finite set
{{1,(rtO . x)},{1}} is non empty finite V45() set
{[1,(rtO . x)]} is Relation-like Function-like constant non empty trivial finite V48(1) set
1 -tree <*(rtO . x)*> is Relation-like Function-like DecoratedTree-like set
() is Relation-like Function-like V18( NAT ,(())) Element of bool [:NAT,(()):]
nt is Element of the carrier of ()
root-tree nt is Relation-like the carrier of () -valued Function-like DecoratedTree-like Element of FinTrees the carrier of ()
() . (root-tree nt) is set
() . (() . (root-tree nt)) is set
() . 0 is Relation-like Function-like DecoratedTree-like Element of (())
O is Element of (())
((),O) is Relation-like the carrier of () -valued Function-like DecoratedTree-like ( the carrier of (), FinTrees the carrier of (),(()))
nt is Element of the carrier of ()
rtO is Relation-like NAT -defined FinTrees the carrier of () -valued Function-like finite FinSequence-like FinSubsequence-like DTree-yielding FinSequence of (())
( the carrier of (),(FinTrees the carrier of ()),rtO) is Relation-like NAT -defined the carrier of () -valued Function-like finite FinSequence-like FinSubsequence-like FinSequence of the carrier of ()
rng rtO is finite set
<*O*> is Relation-like NAT -defined (()) -valued Function-like constant non empty trivial finite V48(1) FinSequence-like FinSubsequence-like Element of (()) *
(()) * is functional non empty FinSequence-membered FinSequenceSet of (())
[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
S is Element of (())
<*S*> is Relation-like NAT -defined (()) -valued Function-like constant non empty trivial finite V48(1) FinSequence-like FinSubsequence-like Element of (()) *
(()) * is functional non empty FinSequence-membered FinSequenceSet of (())
[1,S] is V15() set
{1,S} is non empty finite set
{{1,S},{1}} is non empty finite V45() set
{[1,S]} is Relation-like Function-like constant non empty trivial finite V48(1) set
len ( the carrier of (),(FinTrees the carrier of ()),rtO) is ext-real non negative V32() V33() V34() V35() V39() V40() finite V46() Element of NAT
x is Relation-like the carrier of () -valued Function-like DecoratedTree-like Element of FinTrees the carrier of ()
<*x*> is Relation-like NAT -defined FinTrees the carrier of () -valued Function-like constant non empty trivial finite V48(1) FinSequence-like FinSubsequence-like DTree-yielding Element of (FinTrees the carrier of ()) *
(FinTrees the carrier of ()) * is functional non empty FinSequence-membered FinSequenceSet of FinTrees the carrier of ()
[1,x] is V15() set
{1,x} is non empty finite set
{{1,x},{1}} is non empty finite V45() set
{[1,x]} is Relation-like Function-like constant non empty trivial finite V48(1) set
n is Relation-like the carrier of () -valued Function-like DecoratedTree-like ( the carrier of (), FinTrees the carrier of (),(()))
{n} is functional non empty trivial finite V48(1) constituted-DTrees Element of bool (())
bool (()) is non empty set
() . n is ext-real non negative V32() V33() V34() V35() V39() V40() finite V46() Element of NAT
() . (() . n) is Relation-like Function-like DecoratedTree-like Element of (())
() * rtO is Relation-like NAT -defined NAT -valued Function-like finite FinSequence-like FinSubsequence-like V90() V91() V92() V93() FinSequence of NAT
<*(() . n)*> is Relation-like NAT -defined NAT -valued Function-like one-to-one constant non empty trivial finite V48(1) FinSequence-like FinSubsequence-like V90() V91() V92() V93() V94() V95() V96() V97() Element of NAT *
[1,(() . n)] is V15() set
{1,(() . n)} is non empty finite V45() set
{{1,(() . n)},{1}} is non empty finite V45() set
{[1,(() . n)]} is Relation-like Function-like constant non empty trivial finite V48(1) set
(<*(() . n)*>) is ext-real non negative V32() V33() V34() V35() V39() V40() finite V46() Element of NAT
<*(() . n)*> . 1 is ext-real non negative V32() V33() V34() V35() V39() V40() finite V46() set
(<*(() . n)*> . 1) + 1 is non empty ext-real positive non negative V32() V33() V34() V35() V39() V40() finite V46() Element of NAT
(() . n) + 1 is non empty ext-real positive non negative V32() V33() V34() V35() V39() V40() finite V46() Element of NAT
() . ((() . n) + 1) is Relation-like Function-like DecoratedTree-like Element of (())
(n) is Relation-like the carrier of () -valued Function-like DecoratedTree-like ( the carrier of (), FinTrees the carrier of (),(()))
<*n*> is Relation-like NAT -defined (()) -valued Function-like constant non empty trivial finite V48(1) FinSequence-like FinSubsequence-like DTree-yielding Element of (()) *
[1,n] is V15() set
{1,n} is non empty finite set
{{1,n},{1}} is non empty finite V45() set
{[1,n]} is Relation-like Function-like constant non empty trivial finite V48(1) set
1 -tree <*n*> is Relation-like Function-like DecoratedTree-like set
nt -tree rtO is Relation-like the carrier of () -valued Function-like DecoratedTree-like Element of FinTrees the carrier of ()
() . (nt -tree rtO) is set
() . (() . (nt -tree rtO)) is set
nt is Relation-like the carrier of () -valued Function-like DecoratedTree-like ( the carrier of (), FinTrees the carrier of (),(()))
() . nt is ext-real non negative V32() V33() V34() V35() V39() V40() finite V46() Element of NAT
() . (() . nt) is Relation-like Function-like DecoratedTree-like Element of (())
O is Element of (())
((),O) is Relation-like the carrier of () -valued Function-like DecoratedTree-like ( the carrier of (), FinTrees the carrier of (),(()))
() . ((),O) is ext-real non negative V32() V33() V34() V35() V39() V40() finite V46() Element of NAT
() . 0 is Relation-like Function-like DecoratedTree-like Element of (())
() . (() . 0) 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() Element of NAT
() . nt is Relation-like Function-like DecoratedTree-like Element of (())
() . (() . nt) is ext-real non negative V32() V33() V34() V35() V39() V40() finite V46() Element of NAT
rtO is Relation-like the carrier of () -valued Function-like DecoratedTree-like ( the carrier of (), FinTrees the carrier of (),(()))
dom rtO is non empty finite Tree-like set
x is Relation-like NAT -defined NAT -valued Function-like finite FinSequence-like FinSubsequence-like V90() V91() V92() V93() Element of dom rtO
rtO . x is Element of the carrier of ()
S is Element of (())
nt + 1 is non empty ext-real positive non negative V32() V33() V34() V35() V39() V40() finite V46() Element of NAT
() . (nt + 1) is Relation-like Function-like DecoratedTree-like Element of (())
((() . nt)) is Relation-like the carrier of () -valued Function-like DecoratedTree-like ( the carrier of (), FinTrees the carrier of (),(()))
<*(() . nt)*> is Relation-like NAT -defined (()) -valued Function-like constant non empty trivial finite V48(1) FinSequence-like FinSubsequence-like DTree-yielding Element of (()) *
[1,(() . nt)] is V15() set
{1,(() . nt)} is non empty finite set
{{1,(() . nt)},{1}} is non empty finite V45() set
{[1,(() . nt)]} is Relation-like Function-like constant non empty trivial finite V48(1) set
1 -tree <*(() . nt)*> is Relation-like Function-like DecoratedTree-like set
S -tree <*(() . nt)*> is Relation-like Function-like DecoratedTree-like set
roots <*(() . nt)*> is Relation-like NAT -defined Function-like finite FinSequence-like FinSubsequence-like set
<*(() . (() . nt))*> is Relation-like NAT -defined NAT -valued Function-like one-to-one constant non empty trivial finite V48(1) FinSequence-like FinSubsequence-like V90() V91() V92() V93() V94() V95() V96() V97() Element of NAT *
[1,(() . (() . nt))] is V15() set
{1,(() . (() . nt))} is non empty finite V45() set
{{1,(() . (() . nt))},{1}} is non empty finite V45() set
{[1,(() . (() . nt))]} is Relation-like Function-like constant non empty trivial finite V48(1) set
() * <*(() . nt)*> is Relation-like NAT -defined NAT -valued Function-like finite FinSequence-like FinSubsequence-like V90() V91() V92() V93() FinSequence of NAT
() . (S -tree <*(() . nt)*>) is set
<*nt*> is Relation-like NAT -defined NAT -valued Function-like one-to-one constant non empty trivial finite V48(1) FinSequence-like FinSubsequence-like V90() V91() V92() V93() V94() V95() V96() V97() Element of NAT *
[1,nt] is V15() set
{1,nt} is non empty finite V45() set
{{1,nt},{1}} is non empty finite V45() set
{[1,nt]} is Relation-like Function-like constant non empty trivial finite V48(1) set
(<*nt*>) is ext-real non negative V32() V33() V34() V35() V39() V40() finite V46() Element of NAT
<*nt*> . 1 is ext-real non negative V32() V33() V34() V35() V39() V40() finite V46() set
(<*nt*> . 1) + 1 is non empty ext-real positive non negative V32() V33() V34() V35() V39() V40() finite V46() Element of NAT
() . (() . (nt + 1)) 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() Element of NAT
() . nt is Relation-like Function-like DecoratedTree-like Element of (())
() . (() . nt) is ext-real non negative V32() V33() V34() V35() V39() V40() finite V46() Element of NAT
nt + 1 is non empty ext-real positive non negative V32() V33() V34() V35() V39() V40() finite V46() Element of NAT
() . (nt + 1) is Relation-like Function-like DecoratedTree-like Element of (())
() . (() . (nt + 1)) is ext-real non negative V32() V33() V34() V35() V39() V40() finite V46() Element of NAT
nt is non empty DTConstrStr
the carrier of nt is non empty set
rtO is Relation-like the carrier of nt -valued Function-like DecoratedTree-like set
(nt) is functional constituted-DTrees Element of bool (FinTrees the carrier of nt)
FinTrees the carrier of nt is functional non empty constituted-DTrees DTree-set of the carrier of nt
bool (FinTrees the carrier of nt) is non empty set
Terminals nt is set
x is set
n is non empty set
n is Element of n
<*n*> is Relation-like NAT -defined n -valued Function-like constant non empty trivial finite V48(1) FinSequence-like FinSubsequence-like Element of n *
n * is functional non empty FinSequence-membered FinSequenceSet of n
[1,n] is V15() set
{1,n} is non empty finite set
{{1,n},{1}} is non empty finite V45() set
{[1,n]} is Relation-like Function-like constant non empty trivial finite V48(1) set
<*x*> is Relation-like NAT -defined Function-like constant non empty trivial finite V48(1) FinSequence-like FinSubsequence-like set
[1,x] is V15() set
{1,x} is non empty finite set
{{1,x},{1}} is non empty finite V45() set
{[1,x]} is Relation-like Function-like constant non empty trivial finite V48(1) set
(Terminals nt) * is functional non empty FinSequence-membered FinSequenceSet of Terminals nt
<*> (Terminals nt) is Relation-like non-empty empty-yielding NAT -defined Terminals nt -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 (Terminals nt) *
[: the carrier of nt,((Terminals nt) *):] is Relation-like non empty set
bool [: the carrier of nt,((Terminals nt) *):] is non empty set
x is Relation-like Function-like V18( the carrier of nt,(Terminals nt) * ) Element of bool [: the carrier of nt,((Terminals nt) *):]
[:(nt),((Terminals nt) *):] is Relation-like set
bool [:(nt),((Terminals nt) *):] is non empty set
n is Relation-like Function-like V18((nt),(Terminals nt) * ) Element of bool [:(nt),((Terminals nt) *):]
n . rtO is set
n is Relation-like NAT -defined Terminals nt -valued Function-like finite FinSequence-like FinSubsequence-like FinSequence of Terminals nt
tsg9 is Element of the carrier of nt
root-tree tsg9 is Relation-like the carrier of nt -valued Function-like DecoratedTree-like Element of FinTrees the carrier of nt
n . (root-tree tsg9) is set
x . tsg9 is Relation-like NAT -defined Function-like finite FinSequence-like FinSubsequence-like Element of (Terminals nt) *
<*tsg9*> is Relation-like NAT -defined the carrier of nt -valued Function-like constant non empty trivial finite V48(1) FinSequence-like FinSubsequence-like Element of the carrier of nt *
the carrier of nt * is functional non empty FinSequence-membered FinSequenceSet of the carrier of nt
[1,tsg9] is V15() set
{1,tsg9} is non empty finite set
{{1,tsg9},{1}} is non empty finite V45() set
{[1,tsg9]} is Relation-like Function-like constant non empty trivial finite V48(1) set
tsg9 is Element of the carrier of nt
tsg9 is Relation-like NAT -defined FinTrees the carrier of nt -valued Function-like finite FinSequence-like FinSubsequence-like DTree-yielding FinSequence of (nt)
( the carrier of nt,(FinTrees the carrier of nt),tsg9) is Relation-like NAT -defined the carrier of nt -valued Function-like finite FinSequence-like FinSubsequence-like FinSequence of the carrier of nt
tsg9 -tree tsg9 is Relation-like the carrier of nt -valued Function-like DecoratedTree-like Element of FinTrees the carrier of nt
n . (tsg9 -tree tsg9) is set
n * tsg9 is Relation-like NAT -defined (Terminals nt) * -valued Function-like finite FinSequence-like FinSubsequence-like FinSequence of (Terminals nt) *
FlattenSeq (n * tsg9) is Relation-like NAT -defined Terminals nt -valued Function-like finite FinSequence-like FinSubsequence-like Element of (Terminals nt) *
n is Relation-like NAT -defined Terminals nt -valued Function-like finite FinSequence-like FinSubsequence-like FinSequence of Terminals nt
n is Relation-like NAT -defined Terminals nt -valued Function-like finite FinSequence-like FinSubsequence-like FinSequence of Terminals nt
tsg9 is Relation-like Function-like V18((nt),(Terminals nt) * ) Element of bool [:(nt),((Terminals nt) *):]
tsg9 . rtO is set
tsg9 is Relation-like Function-like V18((nt),(Terminals nt) * ) Element of bool [:(nt),((Terminals nt) *):]
tsg9 . rtO is set
f2 is Element of the carrier of nt
root-tree f2 is Relation-like the carrier of nt -valued Function-like DecoratedTree-like Element of FinTrees the carrier of nt
tsg9 . (root-tree f2) is set
<*f2*> is Relation-like NAT -defined the carrier of nt -valued Function-like constant non empty trivial finite V48(1) FinSequence-like FinSubsequence-like Element of the carrier of nt *
the carrier of nt * is functional non empty FinSequence-membered FinSequenceSet of the carrier of nt
[1,f2] is V15() set
{1,f2} is non empty finite set
{{1,f2},{1}} is non empty finite V45() set
{[1,f2]} is Relation-like Function-like constant non empty trivial finite V48(1) set
x . f2 is Relation-like NAT -defined Function-like finite FinSequence-like FinSubsequence-like Element of (Terminals nt) *
f2 is Element of the carrier of nt
nt is Relation-like NAT -defined FinTrees the carrier of nt -valued Function-like finite FinSequence-like FinSubsequence-like DTree-yielding FinSequence of (nt)
( the carrier of nt,(FinTrees the carrier of nt),nt) is Relation-like NAT -defined the carrier of nt -valued Function-like finite FinSequence-like FinSubsequence-like FinSequence of the carrier of nt
f2 -tree nt is Relation-like the carrier of nt -valued Function-like DecoratedTree-like Element of FinTrees the carrier of nt
tsg9 . (f2 -tree nt) is set
tsg9 * nt is Relation-like NAT -defined (Terminals nt) * -valued Function-like finite FinSequence-like FinSubsequence-like FinSequence of (Terminals nt) *
FlattenSeq (tsg9 * nt) is Relation-like NAT -defined Terminals nt -valued Function-like finite FinSequence-like FinSubsequence-like Element of (Terminals nt) *
f2 is Element of the carrier of nt
root-tree f2 is Relation-like the carrier of nt -valued Function-like DecoratedTree-like Element of FinTrees the carrier of nt
tsg9 . (root-tree f2) is set
<*f2*> is Relation-like NAT -defined the carrier of nt -valued Function-like constant non empty trivial finite V48(1) FinSequence-like FinSubsequence-like Element of the carrier of nt *
[1,f2] is V15() set
{1,f2} is non empty finite set
{{1,f2},{1}} is non empty finite V45() set
{[1,f2]} is Relation-like Function-like constant non empty trivial finite V48(1) set
x . f2 is Relation-like NAT -defined Function-like finite FinSequence-like FinSubsequence-like Element of (Terminals nt) *
f2 is Element of the carrier of nt
nt is Relation-like NAT -defined FinTrees the carrier of nt -valued Function-like finite FinSequence-like FinSubsequence-like DTree-yielding FinSequence of (nt)
( the carrier of nt,(FinTrees the carrier of nt),nt) is Relation-like NAT -defined the carrier of nt -valued Function-like finite FinSequence-like FinSubsequence-like FinSequence of the carrier of nt
f2 -tree nt is Relation-like the carrier of nt -valued Function-like DecoratedTree-like Element of FinTrees the carrier of nt
tsg9 . (f2 -tree nt) is set
tsg9 * nt is Relation-like NAT -defined (Terminals nt) * -valued Function-like finite FinSequence-like FinSubsequence-like FinSequence of (Terminals nt) *
FlattenSeq (tsg9 * nt) is Relation-like NAT -defined Terminals nt -valued Function-like finite FinSequence-like FinSubsequence-like Element of (Terminals nt) *
n is set
n is Element of the carrier of nt
<*n*> is Relation-like NAT -defined the carrier of nt -valued Function-like constant non empty trivial finite V48(1) FinSequence-like FinSubsequence-like Element of the carrier of nt *
the carrier of nt * is functional non empty FinSequence-membered FinSequenceSet of the carrier of nt
[1,n] is V15() set
{1,n} is non empty finite set
{{1,n},{1}} is non empty finite V45() set
{[1,n]} is Relation-like Function-like constant non empty trivial finite V48(1) set
<*n*> is Relation-like NAT -defined Function-like constant non empty trivial finite V48(1) FinSequence-like FinSubsequence-like set
[1,n] is V15() set
{1,n} is non empty finite set
{{1,n},{1}} is non empty finite V45() set
{[1,n]} is Relation-like Function-like constant non empty trivial finite V48(1) set
[: the carrier of nt,( the carrier of nt *):] is Relation-like non empty set
bool [: the carrier of nt,( the carrier of nt *):] is non empty set
n is Relation-like Function-like V18( the carrier of nt, the carrier of nt * ) Element of bool [: the carrier of nt,( the carrier of nt *):]
[:(nt),( the carrier of nt *):] is Relation-like set
bool [:(nt),( the carrier of nt *):] is non empty set
n is Relation-like Function-like V18((nt), the carrier of nt * ) Element of bool [:(nt),( the carrier of nt *):]
n . rtO is set
tsg9 is Relation-like NAT -defined the carrier of nt -valued Function-like finite FinSequence-like FinSubsequence-like FinSequence of the carrier of nt
tsg9 is Element of the carrier of nt
root-tree tsg9 is Relation-like the carrier of nt -valued Function-like DecoratedTree-like Element of FinTrees the carrier of nt
n . (root-tree tsg9) is set
n . tsg9 is Relation-like NAT -defined Function-like finite FinSequence-like FinSubsequence-like Element of the carrier of nt *
<*tsg9*> is Relation-like NAT -defined the carrier of nt -valued Function-like constant non empty trivial finite V48(1) FinSequence-like FinSubsequence-like Element of the carrier of nt *
[1,tsg9] is V15() set
{1,tsg9} is non empty finite set
{{1,tsg9},{1}} is non empty finite V45() set
{[1,tsg9]} is Relation-like Function-like constant non empty trivial finite V48(1) set
tsg9 is Element of the carrier of nt
<*tsg9*> is Relation-like NAT -defined the carrier of nt -valued Function-like constant non empty trivial finite V48(1) FinSequence-like FinSubsequence-like Element of the carrier of nt *
[1,tsg9] is V15() set
{1,tsg9} is non empty finite set
{{1,tsg9},{1}} is non empty finite V45() set
{[1,tsg9]} is Relation-like Function-like constant non empty trivial finite V48(1) set
f2 is Relation-like NAT -defined FinTrees the carrier of nt -valued Function-like finite FinSequence-like FinSubsequence-like DTree-yielding FinSequence of (nt)
( the carrier of nt,(FinTrees the carrier of nt),f2) is Relation-like NAT -defined the carrier of nt -valued Function-like finite FinSequence-like FinSubsequence-like FinSequence of the carrier of nt
n * f2 is Relation-like NAT -defined the carrier of nt * -valued Function-like finite FinSequence-like FinSubsequence-like FinSequence of the carrier of nt *
tsg9 -tree f2 is Relation-like the carrier of nt -valued Function-like DecoratedTree-like Element of FinTrees the carrier of nt
n . (tsg9 -tree f2) is set
nt is Relation-like NAT -defined Function-like finite FinSequence-like FinSubsequence-like set
ts is Relation-like NAT -defined the carrier of nt * -valued Function-like finite FinSequence-like FinSubsequence-like FinSequence of the carrier of nt *
FlattenSeq ts is Relation-like NAT -defined the carrier of nt -valued Function-like finite FinSequence-like FinSubsequence-like Element of the carrier of nt *
<*tsg9*> ^ (FlattenSeq ts) is Relation-like NAT -defined the carrier of nt -valued Function-like non empty finite FinSequence-like FinSubsequence-like Element of the carrier of nt *
n . tsg9 is Relation-like NAT -defined Function-like finite FinSequence-like FinSubsequence-like Element of the carrier of nt *
(n . tsg9) ^ (FlattenSeq ts) is Relation-like NAT -defined the carrier of nt -valued Function-like finite FinSequence-like FinSubsequence-like Element of the carrier of nt *
n is Relation-like NAT -defined the carrier of nt -valued Function-like finite FinSequence-like FinSubsequence-like FinSequence of the carrier of nt
tsg9 is Relation-like NAT -defined the carrier of nt -valued Function-like finite FinSequence-like FinSubsequence-like FinSequence of the carrier of nt
tsg9 is Relation-like Function-like V18((nt), the carrier of nt * ) Element of bool [:(nt),( the carrier of nt *):]
tsg9 . rtO is set
f2 is Relation-like Function-like V18((nt), the carrier of nt * ) Element of bool [:(nt),( the carrier of nt *):]
f2 . rtO is set
nt is Element of the carrier of nt
root-tree nt is Relation-like the carrier of nt -valued Function-like DecoratedTree-like Element of FinTrees the carrier of nt
tsg9 . (root-tree nt) is set
<*nt*> is Relation-like NAT -defined the carrier of nt -valued Function-like constant non empty trivial finite V48(1) FinSequence-like FinSubsequence-like Element of the carrier of nt *
[1,nt] is V15() set
{1,nt} is non empty finite set
{{1,nt},{1}} is non empty finite V45() set
{[1,nt]} is Relation-like Function-like constant non empty trivial finite V48(1) set
n . nt is Relation-like NAT -defined Function-like finite FinSequence-like FinSubsequence-like Element of the carrier of nt *
nt is Element of the carrier of nt
ts is Relation-like NAT -defined FinTrees the carrier of nt -valued Function-like finite FinSequence-like FinSubsequence-like DTree-yielding FinSequence of (nt)
( the carrier of nt,(FinTrees the carrier of nt),ts) is Relation-like NAT -defined the carrier of nt -valued Function-like finite FinSequence-like FinSubsequence-like FinSequence of the carrier of nt
nt -tree ts is Relation-like the carrier of nt -valued Function-like DecoratedTree-like Element of FinTrees the carrier of nt
tsg9 . (nt -tree ts) is set
<*nt*> is Relation-like NAT -defined the carrier of nt -valued Function-like constant non empty trivial finite V48(1) FinSequence-like FinSubsequence-like Element of the carrier of nt *
[1,nt] is V15() set
{1,nt} is non empty finite set
{{1,nt},{1}} is non empty finite V45() set
{[1,nt]} is Relation-like Function-like constant non empty trivial finite V48(1) set
tsg9 * ts is Relation-like NAT -defined the carrier of nt * -valued Function-like finite FinSequence-like FinSubsequence-like FinSequence of the carrier of nt *
FlattenSeq (tsg9 * ts) is Relation-like NAT -defined the carrier of nt -valued Function-like finite FinSequence-like FinSubsequence-like Element of the carrier of nt *
<*nt*> ^ (FlattenSeq (tsg9 * ts)) is Relation-like NAT -defined the carrier of nt -valued Function-like non empty finite FinSequence-like FinSubsequence-like Element of the carrier of nt *
n . nt is Relation-like NAT -defined Function-like finite FinSequence-like FinSubsequence-like Element of the carrier of nt *
(n . nt) ^ (FlattenSeq (tsg9 * ts)) is Relation-like NAT -defined the carrier of nt -valued Function-like finite FinSequence-like FinSubsequence-like Element of the carrier of nt *
nt is Element of the carrier of nt
root-tree nt is Relation-like the carrier of nt -valued Function-like DecoratedTree-like Element of FinTrees the carrier of nt
f2 . (root-tree nt) is set
<*nt*> is Relation-like NAT -defined the carrier of nt -valued Function-like constant non empty trivial finite V48(1) FinSequence-like FinSubsequence-like Element of the carrier of nt *
[1,nt] is V15() set
{1,nt} is non empty finite set
{{1,nt},{1}} is non empty finite V45() set
{[1,nt]} is Relation-like Function-like constant non empty trivial finite V48(1) set
n . nt is Relation-like NAT -defined Function-like finite FinSequence-like FinSubsequence-like Element of the carrier of nt *
nt is Element of the carrier of nt
ts is Relation-like NAT -defined FinTrees the carrier of nt -valued Function-like finite FinSequence-like FinSubsequence-like DTree-yielding FinSequence of (nt)
( the carrier of nt,(FinTrees the carrier of nt),ts) is Relation-like NAT -defined the carrier of nt -valued Function-like finite FinSequence-like FinSubsequence-like FinSequence of the carrier of nt
nt -tree ts is Relation-like the carrier of nt -valued Function-like DecoratedTree-like Element of FinTrees the carrier of nt
f2 . (nt -tree ts) is set
<*nt*> is Relation-like NAT -defined the carrier of nt -valued Function-like constant non empty trivial finite V48(1) FinSequence-like FinSubsequence-like Element of the carrier of nt *
[1,nt] is V15() set
{1,nt} is non empty finite set
{{1,nt},{1}} is non empty finite V45() set
{[1,nt]} is Relation-like Function-like constant non empty trivial finite V48(1) set
f2 * ts is Relation-like NAT -defined the carrier of nt * -valued Function-like finite FinSequence-like FinSubsequence-like FinSequence of the carrier of nt *
FlattenSeq (f2 * ts) is Relation-like NAT -defined the carrier of nt -valued Function-like finite FinSequence-like FinSubsequence-like Element of the carrier of nt *
<*nt*> ^ (FlattenSeq (f2 * ts)) is Relation-like NAT -defined the carrier of nt -valued Function-like non empty finite FinSequence-like FinSubsequence-like Element of the carrier of nt *
n . nt is Relation-like NAT -defined Function-like finite FinSequence-like FinSubsequence-like Element of the carrier of nt *
(n . nt) ^ (FlattenSeq (f2 * ts)) is Relation-like NAT -defined the carrier of nt -valued Function-like finite FinSequence-like FinSubsequence-like Element of the carrier of nt *
n is Relation-like Function-like V18((nt), the carrier of nt * ) Element of bool [:(nt),( the carrier of nt *):]
n . rtO is set
tsg9 is Relation-like NAT -defined the carrier of nt -valued Function-like finite FinSequence-like FinSubsequence-like FinSequence of the carrier of nt
tsg9 is Element of the carrier of nt
root-tree tsg9 is Relation-like the carrier of nt -valued Function-like DecoratedTree-like Element of FinTrees the carrier of nt
n . (root-tree tsg9) is set
n . tsg9 is Relation-like NAT -defined Function-like finite FinSequence-like FinSubsequence-like Element of the carrier of nt *
<*tsg9*> is Relation-like NAT -defined the carrier of nt -valued Function-like constant non empty trivial finite V48(1) FinSequence-like FinSubsequence-like Element of the carrier of nt *
[1,tsg9] is V15() set
{1,tsg9} is non empty finite set
{{1,tsg9},{1}} is non empty finite V45() set
{[1,tsg9]} is Relation-like Function-like constant non empty trivial finite V48(1) set
tsg9 is Element of the carrier of nt
<*tsg9*> is Relation-like NAT -defined the carrier of nt -valued Function-like constant non empty trivial finite V48(1) FinSequence-like FinSubsequence-like Element of the carrier of nt *
[1,tsg9] is V15() set
{1,tsg9} is non empty finite set
{{1,tsg9},{1}} is non empty finite V45() set
{[1,tsg9]} is Relation-like Function-like constant non empty trivial finite V48(1) set
f2 is Relation-like NAT -defined FinTrees the carrier of nt -valued Function-like finite FinSequence-like FinSubsequence-like DTree-yielding FinSequence of (nt)
( the carrier of nt,(FinTrees the carrier of nt),f2) is Relation-like NAT -defined the carrier of nt -valued Function-like finite FinSequence-like FinSubsequence-like FinSequence of the carrier of nt
n * f2 is Relation-like NAT -defined the carrier of nt * -valued Function-like finite FinSequence-like FinSubsequence-like FinSequence of the carrier of nt *
tsg9 -tree f2 is Relation-like the carrier of nt -valued Function-like DecoratedTree-like Element of FinTrees the carrier of nt
n . (tsg9 -tree f2) is set
nt is Relation-like NAT -defined Function-like finite FinSequence-like FinSubsequence-like set
ts is Relation-like NAT -defined the carrier of nt * -valued Function-like finite FinSequence-like FinSubsequence-like FinSequence of the carrier of nt *
FlattenSeq ts is Relation-like NAT -defined the carrier of nt -valued Function-like finite FinSequence-like FinSubsequence-like Element of the carrier of nt *
(FlattenSeq ts) ^ <*tsg9*> is Relation-like NAT -defined the carrier of nt -valued Function-like non empty finite FinSequence-like FinSubsequence-like Element of the carrier of nt *
n . tsg9 is Relation-like NAT -defined Function-like finite FinSequence-like FinSubsequence-like Element of the carrier of nt *
(FlattenSeq ts) ^ (n . tsg9) is Relation-like NAT -defined the carrier of nt -valued Function-like finite FinSequence-like FinSubsequence-like Element of the carrier of nt *
n is Relation-like NAT -defined the carrier of nt -valued Function-like finite FinSequence-like FinSubsequence-like FinSequence of the carrier of nt
tsg9 is Relation-like NAT -defined the carrier of nt -valued Function-like finite FinSequence-like FinSubsequence-like FinSequence of the carrier of nt
tsg9 is Relation-like Function-like V18((nt), the carrier of nt * ) Element of bool [:(nt),( the carrier of nt *):]
tsg9 . rtO is set
f2 is Relation-like Function-like V18((nt), the carrier of nt * ) Element of bool [:(nt),( the carrier of nt *):]
f2 . rtO is set
nt is Element of the carrier of nt
root-tree nt is Relation-like the carrier of nt -valued Function-like DecoratedTree-like Element of FinTrees the carrier of nt
tsg9 . (root-tree nt) is set
<*nt*> is Relation-like NAT -defined the carrier of nt -valued Function-like constant non empty trivial finite V48(1) FinSequence-like FinSubsequence-like Element of the carrier of nt *
[1,nt] is V15() set
{1,nt} is non empty finite set
{{1,nt},{1}} is non empty finite V45() set
{[1,nt]} is Relation-like Function-like constant non empty trivial finite V48(1) set
n . nt is Relation-like NAT -defined Function-like finite FinSequence-like FinSubsequence-like Element of the carrier of nt *
nt is Element of the carrier of nt
ts is Relation-like NAT -defined FinTrees the carrier of nt -valued Function-like finite FinSequence-like FinSubsequence-like DTree-yielding FinSequence of (nt)
( the carrier of nt,(FinTrees the carrier of nt),ts) is Relation-like NAT -defined the carrier of nt -valued Function-like finite FinSequence-like FinSubsequence-like FinSequence of the carrier of nt
nt -tree ts is Relation-like the carrier of nt -valued Function-like DecoratedTree-like Element of FinTrees the carrier of nt
tsg9 . (nt -tree ts) is set
tsg9 * ts is Relation-like NAT -defined the carrier of nt * -valued Function-like finite FinSequence-like FinSubsequence-like FinSequence of the carrier of nt *
FlattenSeq (tsg9 * ts) is Relation-like NAT -defined the carrier of nt -valued Function-like finite FinSequence-like FinSubsequence-like Element of the carrier of nt *
<*nt*> is Relation-like NAT -defined the carrier of nt -valued Function-like constant non empty trivial finite V48(1) FinSequence-like FinSubsequence-like Element of the carrier of nt *
[1,nt] is V15() set
{1,nt} is non empty finite set
{{1,nt},{1}} is non empty finite V45() set
{[1,nt]} is Relation-like Function-like constant non empty trivial finite V48(1) set
(FlattenSeq (tsg9 * ts)) ^ <*nt*> is Relation-like NAT -defined the carrier of nt -valued Function-like non empty finite FinSequence-like FinSubsequence-like Element of the carrier of nt *
n . nt is Relation-like NAT -defined Function-like finite FinSequence-like FinSubsequence-like Element of the carrier of nt *
(FlattenSeq (tsg9 * ts)) ^ (n . nt) is Relation-like NAT -defined the carrier of nt -valued Function-like finite FinSequence-like FinSubsequence-like Element of the carrier of nt *
nt is Element of the carrier of nt
root-tree nt is Relation-like the carrier of nt -valued Function-like DecoratedTree-like Element of FinTrees the carrier of nt
f2 . (root-tree nt) is set
<*nt*> is Relation-like NAT -defined the carrier of nt -valued Function-like constant non empty trivial finite V48(1) FinSequence-like FinSubsequence-like Element of the carrier of nt *
[1,nt] is V15() set
{1,nt} is non empty finite set
{{1,nt},{1}} is non empty finite V45() set
{[1,nt]} is Relation-like Function-like constant non empty trivial finite V48(1) set
n . nt is Relation-like NAT -defined Function-like finite FinSequence-like FinSubsequence-like Element of the carrier of nt *
nt is Element of the carrier of nt
ts is Relation-like NAT -defined FinTrees the carrier of nt -valued Function-like finite FinSequence-like FinSubsequence-like DTree-yielding FinSequence of (nt)
( the carrier of nt,(FinTrees the carrier of nt),ts) is Relation-like NAT -defined the carrier of nt -valued Function-like finite FinSequence-like FinSubsequence-like FinSequence of the carrier of nt
nt -tree ts is Relation-like the carrier of nt -valued Function-like DecoratedTree-like Element of FinTrees the carrier of nt
f2 . (nt -tree ts) is set
f2 * ts is Relation-like NAT -defined the carrier of nt * -valued Function-like finite FinSequence-like FinSubsequence-like FinSequence of the carrier of nt *
FlattenSeq (f2 * ts) is Relation-like NAT -defined the carrier of nt -valued Function-like finite FinSequence-like FinSubsequence-like Element of the carrier of nt *
<*nt*> is Relation-like NAT -defined the carrier of nt -valued Function-like constant non empty trivial finite V48(1) FinSequence-like FinSubsequence-like Element of the carrier of nt *
[1,nt] is V15() set
{1,nt} is non empty finite set
{{1,nt},{1}} is non empty finite V45() set
{[1,nt]} is Relation-like Function-like constant non empty trivial finite V48(1) set
(FlattenSeq (f2 * ts)) ^ <*nt*> is Relation-like NAT -defined the carrier of nt -valued Function-like non empty finite FinSequence-like FinSubsequence-like Element of the carrier of nt *
n . nt is Relation-like NAT -defined Function-like finite FinSequence-like FinSubsequence-like Element of the carrier of nt *
(FlattenSeq (f2 * ts)) ^ (n . nt) is Relation-like NAT -defined the carrier of nt -valued Function-like finite FinSequence-like FinSubsequence-like Element of the carrier of nt *
nt is non empty () DTConstrStr
the carrier of nt is non empty set
FinTrees the carrier of nt is functional non empty constituted-DTrees DTree-set of the carrier of nt
(nt) is functional constituted-DTrees Element of bool (FinTrees the carrier of nt)
bool (FinTrees the carrier of nt) is non empty set
rtO is Element of the carrier of nt
{ (nt,b₁) where b₁ is Relation-like the carrier of nt -valued Function-like DecoratedTree-like Element of FinTrees the carrier of nt : ( b₁ in (nt) & b₁ . {} = rtO ) } is set
Terminals nt is set
(Terminals nt) * is functional non empty FinSequence-membered FinSequenceSet of Terminals nt
bool ((Terminals nt) *) is non empty set
n is set
n is Relation-like the carrier of nt -valued Function-like DecoratedTree-like Element of FinTrees the carrier of nt
(nt,n) is Relation-like NAT -defined Terminals nt -valued Function-like finite FinSequence-like FinSubsequence-like FinSequence of Terminals nt
n . {} is set
{ (nt,b₁) where b₁ is Relation-like the carrier of nt -valued Function-like DecoratedTree-like Element of FinTrees the carrier of nt : ( b₁ in (nt) & b₁ . {} = rtO ) } is set
the carrier of nt * is functional non empty FinSequence-membered FinSequenceSet of the carrier of nt
bool ( the carrier of nt *) is non empty set
n is set
n is Relation-like the carrier of nt -valued Function-like DecoratedTree-like Element of FinTrees the carrier of nt
(nt,n) is Relation-like NAT -defined the carrier of nt -valued Function-like finite FinSequence-like FinSubsequence-like FinSequence of the carrier of nt
n . {} is set
{ (nt,b₁) where b₁ is Relation-like the carrier of nt -valued Function-like DecoratedTree-like Element of FinTrees the carrier of nt : ( b₁ in (nt) & b₁ . {} = rtO ) } is set
n is set
n is Relation-like the carrier of nt -valued Function-like DecoratedTree-like Element of FinTrees the carrier of nt
(nt,n) is Relation-like NAT -defined the carrier of nt -valued Function-like finite FinSequence-like FinSubsequence-like FinSequence of the carrier of nt
n . {} is set
(()) * is functional non empty FinSequence-membered FinSequenceSet of (())
[:(()),((()) *):] is Relation-like non empty set
bool [:(()),((()) *):] is non empty set
root-tree O is Relation-like the carrier of () -valued Function-like DecoratedTree-like Element of FinTrees the carrier of ()
((),(root-tree O)) is Relation-like NAT -defined Terminals () -valued Function-like finite FinSequence-like FinSubsequence-like FinSequence of Terminals ()
nt is Relation-like Function-like V18((()),(()) * ) Element of bool [:(()),((()) *):]
nt . ((),O) is Relation-like NAT -defined Function-like finite FinSequence-like FinSubsequence-like Element of (()) *
rtO is Element of the carrier of ()
root-tree rtO is Relation-like the carrier of () -valued Function-like DecoratedTree-like Element of FinTrees the carrier of ()
((),(root-tree rtO)) is Relation-like NAT -defined Terminals () -valued Function-like finite FinSequence-like FinSubsequence-like FinSequence of Terminals ()
rtO is Element of the carrier of ()
x is Relation-like NAT -defined FinTrees the carrier of () -valued Function-like finite FinSequence-like FinSubsequence-like DTree-yielding FinSequence of (())
( the carrier of (),(FinTrees the carrier of ()),x) is Relation-like NAT -defined the carrier of () -valued Function-like finite FinSequence-like FinSubsequence-like FinSequence of the carrier of ()
rng x is finite set
rtO -tree x is Relation-like the carrier of () -valued Function-like DecoratedTree-like Element of FinTrees the carrier of ()
<*O*> is Relation-like NAT -defined (()) -valued Function-like constant non empty trivial finite V48(1) FinSequence-like FinSubsequence-like Element of (()) *
[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
len ( the carrier of (),(FinTrees the carrier of ()),x) is ext-real non negative V32() V33() V34() V35() V39() V40() finite V46() Element of NAT
n is Relation-like the carrier of () -valued Function-like DecoratedTree-like Element of FinTrees the carrier of ()
<*n*> is Relation-like NAT -defined FinTrees the carrier of () -valued Function-like constant non empty trivial finite V48(1) FinSequence-like FinSubsequence-like DTree-yielding Element of (FinTrees the carrier of ()) *
(FinTrees the carrier of ()) * is functional non empty FinSequence-membered FinSequenceSet of FinTrees the carrier of ()
[1,n] is V15() set
{1,n} is non empty finite set
{{1,n},{1}} is non empty finite V45() set
{[1,n]} is Relation-like Function-like constant non empty trivial finite V48(1) set
{n} is functional non empty trivial finite V48(1) constituted-DTrees Element of bool (FinTrees the carrier of ())
n is Relation-like the carrier of () -valued Function-like DecoratedTree-like ( the carrier of (), FinTrees the carrier of (),(()))
nt . n is Relation-like NAT -defined Function-like finite FinSequence-like FinSubsequence-like Element of (()) *
((),n) is Relation-like NAT -defined Terminals () -valued Function-like finite FinSequence-like FinSubsequence-like FinSequence of Terminals ()
nt * x is Relation-like NAT -defined (()) * -valued Function-like finite FinSequence-like FinSubsequence-like FinSequence of (()) *
nt . n is set
<*(nt . n)*> is Relation-like NAT -defined Function-like constant non empty trivial finite V48(1) FinSequence-like FinSubsequence-like set
[1,(nt . n)] is V15() set
{1,(nt . n)} is non empty finite set
{{1,(nt . n)},{1}} is non empty finite V45() set
{[1,(nt . n)]} is Relation-like Function-like constant non empty trivial finite V48(1) set
nt . (rtO -tree x) is set
<*(nt . n)*> is Relation-like NAT -defined (()) * -valued Function-like constant non empty trivial finite V48(1) FinSequence-like FinSubsequence-like Element of ((()) *) *
((()) *) * is functional non empty FinSequence-membered FinSequenceSet of (()) *
[1,(nt . n)] is V15() set
{1,(nt . n)} is non empty finite V45() set
{{1,(nt . n)},{1}} is non empty finite V45() set
{[1,(nt . n)]} is Relation-like Function-like constant non empty trivial finite V48(1) set
FlattenSeq <*(nt . n)*> is Relation-like NAT -defined (()) -valued Function-like finite FinSequence-like FinSubsequence-like Element of (()) *
((),(rtO -tree x)) is Relation-like NAT -defined Terminals () -valued Function-like finite FinSequence-like FinSubsequence-like FinSequence of Terminals ()
{<*0*>} is functional non empty trivial finite V45() V48(1) FinSequence-membered Element of bool (NAT *)
bool (NAT *) is non empty set
nt is Element of the carrier of ()
((),nt) is functional FinSequence-membered Element of bool ((Terminals ()) *)
(Terminals ()) * is functional non empty FinSequence-membered FinSequenceSet of Terminals ()
bool ((Terminals ()) *) is non empty set
{ ((),b₁) where b₁ is Relation-like the carrier of () -valued Function-like DecoratedTree-like Element of FinTrees the carrier of () : ( b₁ in (()) & b₁ . {} = nt ) } is set
rtO is set
<*O*> is Relation-like NAT -defined (()) -valued Function-like constant non empty trivial finite V48(1) FinSequence-like FinSubsequence-like Element of (()) *
(()) * is functional non empty FinSequence-membered FinSequenceSet of (())
[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
x is Relation-like the carrier of () -valued Function-like DecoratedTree-like Element of FinTrees the carrier of ()
((),x) is Relation-like NAT -defined Terminals () -valued Function-like finite FinSequence-like FinSubsequence-like FinSequence of Terminals ()
x . {} is set
rtO is set
x is Relation-like Function-like DecoratedTree-like Element of (())
<*x*> is Relation-like NAT -defined (()) -valued Function-like constant non empty trivial finite V48(1) FinSequence-like FinSubsequence-like DTree-yielding Element of (()) *
[1,x] is V15() set
{1,x} is non empty finite set
{{1,x},{1}} is non empty finite V45() set
{[1,x]} is Relation-like Function-like constant non empty trivial finite V48(1) set
n is Relation-like the carrier of () -valued Function-like DecoratedTree-like ( the carrier of (), FinTrees the carrier of (),(()))
n . {} is set
<*n*> is Relation-like NAT -defined (()) -valued Function-like constant non empty trivial finite V48(1) FinSequence-like FinSubsequence-like DTree-yielding Element of (()) *
[1,n] is V15() set
{1,n} is non empty finite set
{{1,n},{1}} is non empty finite V45() set
{[1,n]} is Relation-like Function-like constant non empty trivial finite V48(1) set
roots <*n*> is Relation-like NAT -defined Function-like finite FinSequence-like FinSubsequence-like set
S -tree <*x*> is Relation-like Function-like DecoratedTree-like set
n is Relation-like NAT -defined FinTrees the carrier of () -valued Function-like finite FinSequence-like FinSubsequence-like DTree-yielding FinSequence of (())
S -tree n is Relation-like the carrier of () -valued Function-like DecoratedTree-like Element of FinTrees the carrier of ()
((),(S -tree n)) is Relation-like NAT -defined Terminals () -valued Function-like finite FinSequence-like FinSubsequence-like FinSequence of Terminals ()
S -tree <*n*> is Relation-like Function-like DecoratedTree-like set
(S -tree <*n*>) . {} is set
((),n) is Relation-like NAT -defined Terminals () -valued Function-like finite FinSequence-like FinSubsequence-like FinSequence of Terminals ()
[:(()),( the carrier of () *):] is Relation-like non empty set
bool [:(()),( the carrier of () *):] is non empty set
root-tree O is Relation-like the carrier of () -valued Function-like DecoratedTree-like Element of FinTrees the carrier of ()
((),(root-tree O)) is Relation-like NAT -defined the carrier of () -valued Function-like finite FinSequence-like FinSubsequence-like FinSequence of the carrier of ()
nt is Relation-like Function-like V18((()), the carrier of () * ) Element of bool [:(()),( the carrier of () *):]
nt . ((),O) is Relation-like NAT -defined Function-like finite FinSequence-like FinSubsequence-like Element of the carrier of () *
x is Element of the carrier of ()
root-tree x is Relation-like the carrier of () -valued Function-like DecoratedTree-like Element of FinTrees the carrier of ()
rtO is Relation-like the carrier of () -valued Function-like DecoratedTree-like ( the carrier of (), FinTrees the carrier of (),(()))
n is Relation-like the carrier of () -valued Function-like DecoratedTree-like ( the carrier of (), FinTrees the carrier of (),(()))
((),n) is Relation-like NAT -defined the carrier of () -valued Function-like finite FinSequence-like FinSubsequence-like FinSequence of the carrier of ()
dom n is non empty finite Tree-like set
height (dom n) is ext-real non negative V32() V33() V34() V35() V39() V40() finite V46() Element of NAT
(height (dom n)) |-> 1 is Relation-like NAT -defined NAT -valued Function-like finite V48( height (dom n)) FinSequence-like FinSubsequence-like V90() V91() V92() V93() Element of (height (dom n)) -tuples_on NAT
(height (dom n)) -tuples_on NAT is functional non empty FinSequence-membered FinSequenceSet of NAT
((height (dom n)) |-> 1) ^ <*0*> is Relation-like NAT -defined NAT -valued Function-like non empty finite V48((height (dom n)) + 1) FinSequence-like FinSubsequence-like V90() V91() V92() V93() FinSequence of NAT
(height (dom n)) + 1 is non empty ext-real positive non negative V32() V33() V34() V35() V39() V40() finite V46() Element of NAT
<*O*> is Relation-like NAT -defined (()) -valued Function-like constant non empty trivial finite V48(1) FinSequence-like FinSubsequence-like Element of (()) *
(()) * is functional non empty FinSequence-membered FinSequenceSet of (())
[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
{} ^ <*O*> is Relation-like NAT -defined Function-like non empty finite V48({} + 1) FinSequence-like FinSubsequence-like set
{} + 1 is non empty ext-real positive non negative V32() V33() V34() V35() V39() V40() finite V46() Element of NAT
0 |-> 1 is Relation-like non-empty empty-yielding NAT -defined NAT -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( 0 ) FinSequence-like FinSubsequence-like FinSequence-membered constituted-Trees constituted-FinTrees constituted-DTrees Tree-yielding FinTree-yielding DTree-yielding V90() V91() V92() V93() Element of 0 -tuples_on NAT
0 -tuples_on NAT is functional non empty FinSequence-membered FinSequenceSet of NAT
(0 |-> 1) ^ <*0*> is Relation-like NAT -defined NAT -valued Function-like non empty finite V48(0 + 1) FinSequence-like FinSubsequence-like V90() V91() V92() V93() FinSequence of NAT
0 + 1 is non empty ext-real positive non negative V32() V33() V34() V35() V39() V40() finite V46() Element of NAT
x is Element of the carrier of ()
n is Relation-like NAT -defined FinTrees the carrier of () -valued Function-like finite FinSequence-like FinSubsequence-like DTree-yielding FinSequence of (())
( the carrier of (),(FinTrees the carrier of ()),n) is Relation-like NAT -defined the carrier of () -valued Function-like finite FinSequence-like FinSubsequence-like FinSequence of the carrier of ()
rng n is finite set
x -tree n is Relation-like the carrier of () -valued Function-like DecoratedTree-like Element of FinTrees the carrier of ()
<*O*> is Relation-like NAT -defined (()) -valued Function-like constant non empty trivial finite V48(1) FinSequence-like FinSubsequence-like Element of (()) *
(()) * is functional non empty FinSequence-membered FinSequenceSet of (())
[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
len ( the carrier of (),(FinTrees the carrier of ()),n) is ext-real non negative V32() V33() V34() V35() V39() V40() finite V46() Element of NAT
tsg9 is Relation-like the carrier of () -valued Function-like DecoratedTree-like Element of FinTrees the carrier of ()
<*tsg9*> is Relation-like NAT -defined FinTrees the carrier of () -valued Function-like constant non empty trivial finite V48(1) FinSequence-like FinSubsequence-like DTree-yielding Element of (FinTrees the carrier of ()) *
(FinTrees the carrier of ()) * is functional non empty FinSequence-membered FinSequenceSet of FinTrees the carrier of ()
[1,tsg9] is V15() set
{1,tsg9} is non empty finite set
{{1,tsg9},{1}} is non empty finite V45() set
{[1,tsg9]} is Relation-like Function-like constant non empty trivial finite V48(1) set
{tsg9} is functional non empty trivial finite V48(1) constituted-DTrees Element of bool (FinTrees the carrier of ())
tsg9 is Relation-like the carrier of () -valued Function-like DecoratedTree-like ( the carrier of (), FinTrees the carrier of (),(()))
nt . tsg9 is Relation-like NAT -defined Function-like finite FinSequence-like FinSubsequence-like Element of the carrier of () *
dom tsg9 is non empty finite Tree-like set
height (dom tsg9) is ext-real non negative V32() V33() V34() V35() V39() V40() finite V46() Element of NAT
(height (dom tsg9)) |-> 1 is Relation-like NAT -defined NAT -valued Function-like finite V48( height (dom tsg9)) FinSequence-like FinSubsequence-like V90() V91() V92() V93() Element of (height (dom tsg9)) -tuples_on NAT
(height (dom tsg9)) -tuples_on NAT is functional non empty FinSequence-membered FinSequenceSet of NAT
((height (dom tsg9)) |-> 1) ^ <*0*> is Relation-like NAT -defined NAT -valued Function-like non empty finite V48((height (dom tsg9)) + 1) FinSequence-like FinSubsequence-like V90() V91() V92() V93() FinSequence of NAT
(height (dom tsg9)) + 1 is non empty ext-real positive non negative V32() V33() V34() V35() V39() V40() finite V46() Element of NAT
f2 is Relation-like the carrier of () -valued Function-like DecoratedTree-like ( the carrier of (), FinTrees the carrier of (),(()))
((),f2) is Relation-like NAT -defined the carrier of () -valued Function-like finite FinSequence-like FinSubsequence-like FinSequence of the carrier of ()
dom f2 is non empty finite Tree-like set
height (dom f2) is ext-real non negative V32() V33() V34() V35() V39() V40() finite V46() Element of NAT
(height (dom f2)) |-> 1 is Relation-like NAT -defined NAT -valued Function-like finite V48( height (dom f2)) FinSequence-like FinSubsequence-like V90() V91() V92() V93() Element of (height (dom f2)) -tuples_on NAT
(height (dom f2)) -tuples_on NAT is functional non empty FinSequence-membered FinSequenceSet of NAT
((height (dom f2)) |-> 1) ^ <*0*> is Relation-like NAT -defined NAT -valued Function-like non empty finite V48((height (dom f2)) + 1) FinSequence-like FinSubsequence-like V90() V91() V92() V93() FinSequence of NAT
(height (dom f2)) + 1 is non empty ext-real positive non negative V32() V33() V34() V35() V39() V40() finite V46() Element of NAT
nt * n is Relation-like NAT -defined the carrier of () * -valued Function-like finite FinSequence-like FinSubsequence-like FinSequence of the carrier of () *
nt . tsg9 is set
<*(nt . tsg9)*> is Relation-like NAT -defined Function-like constant non empty trivial finite V48(1) FinSequence-like FinSubsequence-like set
[1,(nt . tsg9)] is V15() set
{1,(nt . tsg9)} is non empty finite set
{{1,(nt . tsg9)},{1}} is non empty finite V45() set
{[1,(nt . tsg9)]} is Relation-like Function-like constant non empty trivial finite V48(1) set
nt . (x -tree n) is set
<*x*> is Relation-like NAT -defined the carrier of () -valued Function-like constant non empty trivial finite V48(1) FinSequence-like FinSubsequence-like Element of the carrier of () *
[1,x] is V15() set
{1,x} is non empty finite set
{{1,x},{1}} is non empty finite V45() set
{[1,x]} is Relation-like Function-like constant non empty trivial finite V48(1) set
<*(nt . tsg9)*> is Relation-like NAT -defined the carrier of () * -valued Function-like constant non empty trivial finite V48(1) FinSequence-like FinSubsequence-like Element of ( the carrier of () *) *
( the carrier of () *) * is functional non empty FinSequence-membered FinSequenceSet of the carrier of () *
[1,(nt . tsg9)] is V15() set
{1,(nt . tsg9)} is non empty finite V45() set
{{1,(nt . tsg9)},{1}} is non empty finite V45() set
{[1,(nt . tsg9)]} is Relation-like Function-like constant non empty trivial finite V48(1) set
FlattenSeq <*(nt . tsg9)*> is Relation-like NAT -defined the carrier of () -valued Function-like finite FinSequence-like FinSubsequence-like Element of the carrier of () *
<*x*> ^ (FlattenSeq <*(nt . tsg9)*>) is Relation-like NAT -defined the carrier of () -valued Function-like non empty finite FinSequence-like FinSubsequence-like Element of the carrier of () *
<*x*> ^ (((height (dom tsg9)) |-> 1) ^ <*0*>) is Relation-like NAT -defined Function-like non empty finite V48(1 + ((height (dom tsg9)) + 1)) FinSequence-like FinSubsequence-like set
1 + ((height (dom tsg9)) + 1) is non empty ext-real positive non negative V32() V33() V34() V35() V39() V40() finite V46() Element of NAT
<*x*> ^ ((height (dom tsg9)) |-> 1) is Relation-like NAT -defined Function-like non empty finite V48(1 + (height (dom tsg9))) FinSequence-like FinSubsequence-like set
1 + (height (dom tsg9)) is non empty ext-real positive non negative V32() V33() V34() V35() V39() V40() finite V46() Element of NAT
(<*x*> ^ ((height (dom tsg9)) |-> 1)) ^ <*0*> is Relation-like NAT -defined Function-like non empty finite V48((1 + (height (dom tsg9))) + 1) FinSequence-like FinSubsequence-like set
(1 + (height (dom tsg9))) + 1 is non empty ext-real positive non negative V32() V33() V34() V35() V39() V40() finite V46() Element of NAT
1 |-> 1 is Relation-like NAT -defined NAT -valued Function-like one-to-one constant non empty trivial finite V48(1) FinSequence-like FinSubsequence-like V90() V91() V92() V93() V94() V95() V96() V97() Element of 1 -tuples_on NAT
1 -tuples_on NAT is functional non empty FinSequence-membered FinSequenceSet of NAT
(1 |-> 1) ^ ((height (dom tsg9)) |-> 1) is Relation-like NAT -defined NAT -valued Function-like non empty finite V48(1 + (height (dom tsg9))) FinSequence-like FinSubsequence-like V90() V91() V92() V93() FinSequence of NAT
((1 |-> 1) ^ ((height (dom tsg9)) |-> 1)) ^ <*0*> is Relation-like NAT -defined NAT -valued Function-like non empty finite V48((1 + (height (dom tsg9))) + 1) FinSequence-like FinSubsequence-like V90() V91() V92() V93() FinSequence of NAT
(height (dom tsg9)) + 1 is non empty ext-real positive non negative V32() V33() V34() V35() V39() V40() finite V46() Element of NAT
((height (dom tsg9)) + 1) |-> 1 is Relation-like NAT -defined NAT -valued Function-like finite V48((height (dom tsg9)) + 1) FinSequence-like FinSubsequence-like V90() V91() V92() V93() Element of ((height (dom tsg9)) + 1) -tuples_on NAT
((height (dom tsg9)) + 1) -tuples_on NAT is functional non empty FinSequence-membered FinSequenceSet of NAT
(((height (dom tsg9)) + 1) |-> 1) ^ <*0*> is Relation-like NAT -defined NAT -valued Function-like non empty finite V48(((height (dom tsg9)) + 1) + 1) FinSequence-like FinSubsequence-like V90() V91() V92() V93() FinSequence of NAT
((height (dom tsg9)) + 1) + 1 is non empty ext-real positive non negative V32() V33() V34() V35() V39() V40() finite V46() Element of NAT
^ (dom tsg9) is non empty finite Tree-like set
height (^ (dom tsg9)) is ext-real non negative V32() V33() V34() V35() V39() V40() finite V46() Element of NAT
(height (^ (dom tsg9))) |-> 1 is Relation-like NAT -defined NAT -valued Function-like finite V48( height (^ (dom tsg9))) FinSequence-like FinSubsequence-like V90() V91() V92() V93() Element of (height (^ (dom tsg9))) -tuples_on NAT
(height (^ (dom tsg9))) -tuples_on NAT is functional non empty FinSequence-membered FinSequenceSet of NAT
((height (^ (dom tsg9))) |-> 1) ^ <*0*> is Relation-like NAT -defined NAT -valued Function-like non empty finite V48((height (^ (dom tsg9))) + 1) FinSequence-like FinSubsequence-like V90() V91() V92() V93() FinSequence of NAT
(height (^ (dom tsg9))) + 1 is non empty ext-real positive non negative V32() V33() V34() V35() V39() V40() finite V46() Element of NAT
x -tree tsg9 is Relation-like the carrier of () -valued Function-like DecoratedTree-like set
dom (x -tree tsg9) is non empty Tree-like set
n is Relation-like the carrier of () -valued Function-like DecoratedTree-like ( the carrier of (), FinTrees the carrier of (),(()))
nt . n is Relation-like NAT -defined Function-like finite FinSequence-like FinSubsequence-like Element of the carrier of () *
((),(x -tree n)) is Relation-like NAT -defined the carrier of () -valued Function-like finite FinSequence-like FinSubsequence-like FinSequence of the carrier of ()
x is Relation-like the carrier of () -valued Function-like DecoratedTree-like ( the carrier of (), FinTrees the carrier of (),(()))
((),x) is Relation-like NAT -defined the carrier of () -valued Function-like finite FinSequence-like FinSubsequence-like FinSequence of the carrier of ()
dom x is non empty finite Tree-like set
height (dom x) is ext-real non negative V32() V33() V34() V35() V39() V40() finite V46() Element of NAT
(height (dom x)) |-> 1 is Relation-like NAT -defined NAT -valued Function-like finite V48( height (dom x)) FinSequence-like FinSubsequence-like V90() V91() V92() V93() Element of (height (dom x)) -tuples_on NAT
(height (dom x)) -tuples_on NAT is functional non empty FinSequence-membered FinSequenceSet of NAT
((height (dom x)) |-> 1) ^ <*0*> is Relation-like NAT -defined NAT -valued Function-like non empty finite V48((height (dom x)) + 1) FinSequence-like FinSubsequence-like V90() V91() V92() V93() FinSequence of NAT
(height (dom x)) + 1 is non empty ext-real positive non negative V32() V33() V34() V35() V39() V40() finite V46() Element of NAT
n is Relation-like the carrier of () -valued Function-like DecoratedTree-like ( the carrier of (), FinTrees the carrier of (),(()))
((),n) is Relation-like NAT -defined the carrier of () -valued Function-like finite FinSequence-like FinSubsequence-like FinSequence of the carrier of ()
dom n is non empty finite Tree-like set
height (dom n) is ext-real non negative V32() V33() V34() V35() V39() V40() finite V46() Element of NAT
(height (dom n)) |-> 1 is Relation-like NAT -defined NAT -valued Function-like finite V48( height (dom n)) FinSequence-like FinSubsequence-like V90() V91() V92() V93() Element of (height (dom n)) -tuples_on NAT
(height (dom n)) -tuples_on NAT is functional non empty FinSequence-membered FinSequenceSet of NAT
((height (dom n)) |-> 1) ^ <*0*> is Relation-like NAT -defined NAT -valued Function-like non empty finite V48((height (dom n)) + 1) FinSequence-like FinSubsequence-like V90() V91() V92() V93() FinSequence of NAT
(height (dom n)) + 1 is non empty ext-real positive non negative V32() V33() V34() V35() V39() V40() finite V46() Element of NAT
{ ((b₁ |-> 1) ^ <*0*>) where b₁ is ext-real non negative V32() V33() V34() V35() V39() V40() finite V46() Element of NAT : not b₁ = 0 } is set
nt is Element of the carrier of ()
((),nt) is functional FinSequence-membered Element of bool ( the carrier of () *)
bool ( the carrier of () *) is non empty set
{ ((),b₁) where b₁ is Relation-like the carrier of () -valued Function-like DecoratedTree-like Element of FinTrees the carrier of () : ( b₁ in (()) & b₁ . {} = nt ) } is set
dom (root-tree 0) is non empty finite Tree-like set
height (dom (root-tree 0)) is ext-real non negative V32() V33() V34() V35() V39() V40() finite V46() Element of NAT
rtO is Relation-like the carrier of () -valued Function-like DecoratedTree-like ( the carrier of (), FinTrees the carrier of (),(()))
((),rtO) is Relation-like NAT -defined the carrier of () -valued Function-like finite FinSequence-like FinSubsequence-like FinSequence of the carrier of ()
0 |-> 1 is Relation-like non-empty empty-yielding NAT -defined NAT -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( 0 ) FinSequence-like FinSubsequence-like FinSequence-membered constituted-Trees constituted-FinTrees constituted-DTrees Tree-yielding FinTree-yielding DTree-yielding V90() V91() V92() V93() Element of 0 -tuples_on NAT
0 -tuples_on NAT is functional non empty FinSequence-membered FinSequenceSet of NAT
<*O*> is Relation-like NAT -defined (()) -valued Function-like constant non empty trivial finite V48(1) FinSequence-like FinSubsequence-like Element of (()) *
(()) * is functional non empty FinSequence-membered FinSequenceSet of (())
[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
(0 |-> 1) ^ <*O*> is Relation-like NAT -defined Function-like non empty finite V48(0 + 1) FinSequence-like FinSubsequence-like set
0 + 1 is non empty ext-real positive non negative V32() V33() V34() V35() V39() V40() finite V46() Element of NAT
{} ^ <*O*> is Relation-like NAT -defined Function-like non empty finite V48({} + 1) FinSequence-like FinSubsequence-like set
{} + 1 is non empty ext-real positive non negative V32() V33() V34() V35() V39() V40() finite V46() Element of NAT
x is set
n is Relation-like the carrier of () -valued Function-like DecoratedTree-like Element of FinTrees the carrier of ()
((),n) is Relation-like NAT -defined the carrier of () -valued Function-like finite FinSequence-like FinSubsequence-like FinSequence of the carrier of ()
n . {} is set
x is set
rtO . {} is set
x is set
n is Relation-like the carrier of () -valued Function-like DecoratedTree-like Element of FinTrees the carrier of ()
((),n) is Relation-like NAT -defined the carrier of () -valued Function-like finite FinSequence-like FinSubsequence-like FinSequence of the carrier of ()
n . {} is set
n is Relation-like NAT -defined FinTrees the carrier of () -valued Function-like finite FinSequence-like FinSubsequence-like DTree-yielding FinSequence of (())
S -tree n is Relation-like the carrier of () -valued Function-like DecoratedTree-like Element of FinTrees the carrier of ()
( the carrier of (),(FinTrees the carrier of ()),n) is Relation-like NAT -defined the carrier of () -valued Function-like finite FinSequence-like FinSubsequence-like FinSequence of the carrier of ()
len ( the carrier of (),(FinTrees the carrier of ()),n) is ext-real non negative V32() V33() V34() V35() V39() V40() finite V46() Element of NAT
tsg9 is Relation-like the carrier of () -valued Function-like DecoratedTree-like Element of FinTrees the carrier of ()
<*tsg9*> is Relation-like NAT -defined FinTrees the carrier of () -valued Function-like constant non empty trivial finite V48(1) FinSequence-like FinSubsequence-like DTree-yielding Element of (FinTrees the carrier of ()) *
(FinTrees the carrier of ()) * is functional non empty FinSequence-membered FinSequenceSet of FinTrees the carrier of ()
[1,tsg9] is V15() set
{1,tsg9} is non empty finite set
{{1,tsg9},{1}} is non empty finite V45() set
{[1,tsg9]} is Relation-like Function-like constant non empty trivial finite V48(1) set
S -tree tsg9 is Relation-like the carrier of () -valued Function-like DecoratedTree-like set
dom n is non empty finite Tree-like set
dom tsg9 is non empty finite Tree-like set
^ (dom tsg9) is non empty finite Tree-like set
height (dom n) is ext-real non negative V32() V33() V34() V35() V39() V40() finite V46() Element of NAT
height (dom tsg9) is ext-real non negative V32() V33() V34() V35() V39() V40() finite V46() Element of NAT
(height (dom tsg9)) + 1 is non empty ext-real positive non negative V32() V33() V34() V35() V39() V40() finite V46() Element of NAT
(height (dom n)) |-> 1 is Relation-like NAT -defined NAT -valued Function-like finite V48( height (dom n)) FinSequence-like FinSubsequence-like V90() V91() V92() V93() Element of (height (dom n)) -tuples_on NAT
(height (dom n)) -tuples_on NAT is functional non empty FinSequence-membered FinSequenceSet of NAT
((height (dom n)) |-> 1) ^ <*0*> is Relation-like NAT -defined NAT -valued Function-like non empty finite V48((height (dom n)) + 1) FinSequence-like FinSubsequence-like V90() V91() V92() V93() FinSequence of NAT
(height (dom n)) + 1 is non empty ext-real positive non negative V32() V33() V34() V35() V39() V40() finite V46() Element of NAT
x is set
n is ext-real non negative V32() V33() V34() V35() V39() V40() finite V46() Element of NAT
n |-> 1 is Relation-like NAT -defined NAT -valued Function-like finite V48(n) FinSequence-like FinSubsequence-like V90() V91() V92() V93() Element of n -tuples_on NAT
n -tuples_on NAT is functional non empty FinSequence-membered FinSequenceSet of NAT
(n |-> 1) ^ <*0*> is Relation-like NAT -defined NAT -valued Function-like non empty finite V48(n + 1) FinSequence-like FinSubsequence-like V90() V91() V92() V93() FinSequence of NAT
n + 1 is non empty ext-real positive non negative V32() V33() V34() V35() V39() V40() finite V46() Element of NAT
(0 |-> 1) ^ <*0*> is Relation-like NAT -defined NAT -valued Function-like non empty finite V48(0 + 1) FinSequence-like FinSubsequence-like V90() V91() V92() V93() FinSequence of NAT
n is ext-real non negative V32() V33() V34() V35() V39() V40() finite V46() Element of NAT
n |-> 1 is Relation-like NAT -defined NAT -valued Function-like finite V48(n) FinSequence-like FinSubsequence-like V90() V91() V92() V93() Element of n -tuples_on NAT
n -tuples_on NAT is functional non empty FinSequence-membered FinSequenceSet of NAT
(n |-> 1) ^ <*0*> is Relation-like NAT -defined NAT -valued Function-like non empty finite V48(n + 1) FinSequence-like FinSubsequence-like V90() V91() V92() V93() FinSequence of NAT
n + 1 is non empty ext-real positive non negative V32() V33() V34() V35() V39() V40() finite V46() Element of NAT
n + 1 is non empty ext-real positive non negative V32() V33() V34() V35() V39() V40() finite V46() Element of NAT
(n + 1) |-> 1 is Relation-like NAT -defined NAT -valued Function-like finite V48(n + 1) FinSequence-like FinSubsequence-like V90() V91() V92() V93() Element of (n + 1) -tuples_on NAT
(n + 1) -tuples_on NAT is functional non empty FinSequence-membered FinSequenceSet of NAT
((n + 1) |-> 1) ^ <*0*> is Relation-like NAT -defined NAT -valued Function-like non empty finite V48((n + 1) + 1) FinSequence-like FinSubsequence-like V90() V91() V92() V93() FinSequence of NAT
(n + 1) + 1 is non empty ext-real positive non negative V32() V33() V34() V35() V39() V40() finite V46() Element of NAT
tsg9 is Relation-like the carrier of () -valued Function-like DecoratedTree-like ( the carrier of (), FinTrees the carrier of (),(()))
tsg9 . {} is set
((),tsg9) is Relation-like NAT -defined the carrier of () -valued Function-like finite FinSequence-like FinSubsequence-like FinSequence of the carrier of ()
tsg9 is Relation-like the carrier of () -valued Function-like DecoratedTree-like ( the carrier of (), FinTrees the carrier of (),(()))
tsg9 . {} is set
((),tsg9) is Relation-like NAT -defined the carrier of () -valued Function-like finite FinSequence-like FinSubsequence-like FinSequence of the carrier of ()
dom tsg9 is non empty finite Tree-like set
height (dom tsg9) is ext-real non negative V32() V33() V34() V35() V39() V40() finite V46() Element of NAT
(height (dom tsg9)) |-> 1 is Relation-like NAT -defined NAT -valued Function-like finite V48( height (dom tsg9)) FinSequence-like FinSubsequence-like V90() V91() V92() V93() Element of (height (dom tsg9)) -tuples_on NAT
(height (dom tsg9)) -tuples_on NAT is functional non empty FinSequence-membered FinSequenceSet of NAT
((height (dom tsg9)) |-> 1) ^ <*0*> is Relation-like NAT -defined NAT -valued Function-like non empty finite V48((height (dom tsg9)) + 1) FinSequence-like FinSubsequence-like V90() V91() V92() V93() FinSequence of NAT
(height (dom tsg9)) + 1 is non empty ext-real positive non negative V32() V33() V34() V35() V39() V40() finite V46() Element of NAT
len (n |-> 1) is ext-real non negative V32() V33() V34() V35() V39() V40() finite V46() Element of NAT
(S,tsg9) is Relation-like the carrier of () -valued Function-like DecoratedTree-like ( the carrier of (), FinTrees the carrier of (),(()))
tsg9 is Relation-like the carrier of () -valued Function-like DecoratedTree-like ( the carrier of (), FinTrees the carrier of (),(()))
tsg9 . {} is set
((),tsg9) is Relation-like NAT -defined the carrier of () -valued Function-like finite FinSequence-like FinSubsequence-like FinSequence of the carrier of ()
<*tsg9*> is Relation-like NAT -defined (()) -valued Function-like constant non empty trivial finite V48(1) FinSequence-like FinSubsequence-like DTree-yielding Element of (()) *
[1,tsg9] is V15() set
{1,tsg9} is non empty finite set
{{1,tsg9},{1}} is non empty finite V45() set
{[1,tsg9]} is Relation-like Function-like constant non empty trivial finite V48(1) set
S -tree <*tsg9*> is Relation-like Function-like DecoratedTree-like set
dom tsg9 is non empty finite Tree-like set
height (dom tsg9) is ext-real non negative V32() V33() V34() V35() V39() V40() finite V46() Element of NAT
^ (dom tsg9) is non empty finite Tree-like set
height (^ (dom tsg9)) is ext-real non negative V32() V33() V34() V35() V39() V40() finite V46() Element of NAT
(S,rtO) is Relation-like the carrier of () -valued Function-like DecoratedTree-like ( the carrier of (), FinTrees the carrier of (),(()))
tsg9 is Relation-like the carrier of () -valued Function-like DecoratedTree-like ( the carrier of (), FinTrees the carrier of (),(()))
tsg9 . {} is set
((),tsg9) is Relation-like NAT -defined the carrier of () -valued Function-like finite FinSequence-like FinSubsequence-like FinSequence of the carrier of ()
<*rtO*> is Relation-like NAT -defined (()) -valued Function-like constant non empty trivial finite V48(1) FinSequence-like FinSubsequence-like DTree-yielding Element of (()) *
[1,rtO] is V15() set
{1,rtO} is non empty finite set
{{1,rtO},{1}} is non empty finite V45() set
{[1,rtO]} is Relation-like Function-like constant non empty trivial finite V48(1) set
S -tree <*rtO*> is Relation-like Function-like DecoratedTree-like set
dom tsg9 is non empty finite Tree-like set
height (dom tsg9) is ext-real non negative V32() V33() V34() V35() V39() V40() finite V46() Element of NAT
dom rtO is non empty finite Tree-like set
^ (dom rtO) is non empty finite Tree-like set
height (^ (dom rtO)) is ext-real non negative V32() V33() V34() V35() V39() V40() finite V46() Element of NAT
height (dom rtO) is ext-real non negative V32() V33() V34() V35() V39() V40() finite V46() Element of NAT
(height (dom rtO)) + 1 is non empty ext-real positive non negative V32() V33() V34() V35() V39() V40() finite V46() Element of NAT
n is Relation-like the carrier of () -valued Function-like DecoratedTree-like ( the carrier of (), FinTrees the carrier of (),(()))
n . {} is set
((),n) is Relation-like NAT -defined the carrier of () -valued Function-like finite FinSequence-like FinSubsequence-like FinSequence of the carrier of ()
[:(()),( the carrier of () *):] is Relation-like non empty set
bool [:(()),( the carrier of () *):] is non empty set
root-tree O is Relation-like the carrier of () -valued Function-like DecoratedTree-like Element of FinTrees the carrier of ()
((),(root-tree O)) is Relation-like NAT -defined the carrier of () -valued Function-like finite FinSequence-like FinSubsequence-like FinSequence of the carrier of ()
nt is Relation-like Function-like V18((()), the carrier of () * ) Element of bool [:(()),( the carrier of () *):]
nt . ((),O) is Relation-like NAT -defined Function-like finite FinSequence-like FinSubsequence-like Element of the carrier of () *
x is Element of the carrier of ()
root-tree x is Relation-like the carrier of () -valued Function-like DecoratedTree-like Element of FinTrees the carrier of ()
rtO is Relation-like the carrier of () -valued Function-like DecoratedTree-like ( the carrier of (), FinTrees the carrier of (),(()))
n is Relation-like the carrier of () -valued Function-like DecoratedTree-like ( the carrier of (), FinTrees the carrier of (),(()))
((),n) is Relation-like NAT -defined the carrier of () -valued Function-like finite FinSequence-like FinSubsequence-like FinSequence of the carrier of ()
dom n is non empty finite Tree-like set
height (dom n) is ext-real non negative V32() V33() V34() V35() V39() V40() finite V46() Element of NAT
(height (dom n)) |-> 1 is Relation-like NAT -defined NAT -valued Function-like finite V48( height (dom n)) FinSequence-like FinSubsequence-like V90() V91() V92() V93() Element of (height (dom n)) -tuples_on NAT
(height (dom n)) -tuples_on NAT is functional non empty FinSequence-membered FinSequenceSet of NAT
<*0*> ^ ((height (dom n)) |-> 1) is Relation-like NAT -defined NAT -valued Function-like non empty finite V48(1 + (height (dom n))) FinSequence-like FinSubsequence-like V90() V91() V92() V93() FinSequence of NAT
1 + (height (dom n)) is non empty ext-real positive non negative V32() V33() V34() V35() V39() V40() finite V46() Element of NAT
<*O*> is Relation-like NAT -defined (()) -valued Function-like constant non empty trivial finite V48(1) FinSequence-like FinSubsequence-like Element of (()) *
(()) * is functional non empty FinSequence-membered FinSequenceSet of (())
[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
<*O*> ^ {} is Relation-like NAT -defined Function-like non empty finite FinSequence-like FinSubsequence-like set
0 |-> 1 is Relation-like non-empty empty-yielding NAT -defined NAT -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( 0 ) FinSequence-like FinSubsequence-like FinSequence-membered constituted-Trees constituted-FinTrees constituted-DTrees Tree-yielding FinTree-yielding DTree-yielding V90() V91() V92() V93() Element of 0 -tuples_on NAT
0 -tuples_on NAT is functional non empty FinSequence-membered FinSequenceSet of NAT
<*0*> ^ (0 |-> 1) is Relation-like NAT -defined NAT -valued Function-like non empty finite V48(1 + 0) FinSequence-like FinSubsequence-like V90() V91() V92() V93() FinSequence of NAT
1 + 0 is non empty ext-real positive non negative V32() V33() V34() V35() V39() V40() finite V46() Element of NAT
x is Element of the carrier of ()
n is Relation-like NAT -defined FinTrees the carrier of () -valued Function-like finite FinSequence-like FinSubsequence-like DTree-yielding FinSequence of (())
( the carrier of (),(FinTrees the carrier of ()),n) is Relation-like NAT -defined the carrier of () -valued Function-like finite FinSequence-like FinSubsequence-like FinSequence of the carrier of ()
rng n is finite set
x -tree n is Relation-like the carrier of () -valued Function-like DecoratedTree-like Element of FinTrees the carrier of ()
<*O*> is Relation-like NAT -defined (()) -valued Function-like constant non empty trivial finite V48(1) FinSequence-like FinSubsequence-like Element of (()) *
(()) * is functional non empty FinSequence-membered FinSequenceSet of (())
[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
len ( the carrier of (),(FinTrees the carrier of ()),n) is ext-real non negative V32() V33() V34() V35() V39() V40() finite V46() Element of NAT
tsg9 is Relation-like the carrier of () -valued Function-like DecoratedTree-like Element of FinTrees the carrier of ()
<*tsg9*> is Relation-like NAT -defined FinTrees the carrier of () -valued Function-like constant non empty trivial finite V48(1) FinSequence-like FinSubsequence-like DTree-yielding Element of (FinTrees the carrier of ()) *
(FinTrees the carrier of ()) * is functional non empty FinSequence-membered FinSequenceSet of FinTrees the carrier of ()
[1,tsg9] is V15() set
{1,tsg9} is non empty finite set
{{1,tsg9},{1}} is non empty finite V45() set
{[1,tsg9]} is Relation-like Function-like constant non empty trivial finite V48(1) set
{tsg9} is functional non empty trivial finite V48(1) constituted-DTrees Element of bool (FinTrees the carrier of ())
tsg9 is Relation-like the carrier of () -valued Function-like DecoratedTree-like ( the carrier of (), FinTrees the carrier of (),(()))
nt . tsg9 is Relation-like NAT -defined Function-like finite FinSequence-like FinSubsequence-like Element of the carrier of () *
dom tsg9 is non empty finite Tree-like set
height (dom tsg9) is ext-real non negative V32() V33() V34() V35() V39() V40() finite V46() Element of NAT
(height (dom tsg9)) |-> 1 is Relation-like NAT -defined NAT -valued Function-like finite V48( height (dom tsg9)) FinSequence-like FinSubsequence-like V90() V91() V92() V93() Element of (height (dom tsg9)) -tuples_on NAT
(height (dom tsg9)) -tuples_on NAT is functional non empty FinSequence-membered FinSequenceSet of NAT
<*O*> ^ ((height (dom tsg9)) |-> 1) is Relation-like NAT -defined Function-like non empty finite V48(1 + (height (dom tsg9))) FinSequence-like FinSubsequence-like set
1 + (height (dom tsg9)) is non empty ext-real positive non negative V32() V33() V34() V35() V39() V40() finite V46() Element of NAT
f2 is Relation-like the carrier of () -valued Function-like DecoratedTree-like ( the carrier of (), FinTrees the carrier of (),(()))
((),f2) is Relation-like NAT -defined the carrier of () -valued Function-like finite FinSequence-like FinSubsequence-like FinSequence of the carrier of ()
dom f2 is non empty finite Tree-like set
height (dom f2) is ext-real non negative V32() V33() V34() V35() V39() V40() finite V46() Element of NAT
(height (dom f2)) |-> 1 is Relation-like NAT -defined NAT -valued Function-like finite V48( height (dom f2)) FinSequence-like FinSubsequence-like V90() V91() V92() V93() Element of (height (dom f2)) -tuples_on NAT
(height (dom f2)) -tuples_on NAT is functional non empty FinSequence-membered FinSequenceSet of NAT
<*O*> ^ ((height (dom f2)) |-> 1) is Relation-like NAT -defined Function-like non empty finite V48(1 + (height (dom f2))) FinSequence-like FinSubsequence-like set
1 + (height (dom f2)) is non empty ext-real positive non negative V32() V33() V34() V35() V39() V40() finite V46() Element of NAT
nt * n is Relation-like NAT -defined the carrier of () * -valued Function-like finite FinSequence-like FinSubsequence-like FinSequence of the carrier of () *
nt . tsg9 is set
<*(nt . tsg9)*> is Relation-like NAT -defined Function-like constant non empty trivial finite V48(1) FinSequence-like FinSubsequence-like set
[1,(nt . tsg9)] is V15() set
{1,(nt . tsg9)} is non empty finite set
{{1,(nt . tsg9)},{1}} is non empty finite V45() set
{[1,(nt . tsg9)]} is Relation-like Function-like constant non empty trivial finite V48(1) set
nt . (x -tree n) is set
<*(nt . tsg9)*> is Relation-like NAT -defined the carrier of () * -valued Function-like constant non empty trivial finite V48(1) FinSequence-like FinSubsequence-like Element of ( the carrier of () *) *
( the carrier of () *) * is functional non empty FinSequence-membered FinSequenceSet of the carrier of () *
[1,(nt . tsg9)] is V15() set
{1,(nt . tsg9)} is non empty finite V45() set
{{1,(nt . tsg9)},{1}} is non empty finite V45() set
{[1,(nt . tsg9)]} is Relation-like Function-like constant non empty trivial finite V48(1) set
FlattenSeq <*(nt . tsg9)*> is Relation-like NAT -defined the carrier of () -valued Function-like finite FinSequence-like FinSubsequence-like Element of the carrier of () *
<*x*> is Relation-like NAT -defined the carrier of () -valued Function-like constant non empty trivial finite V48(1) FinSequence-like FinSubsequence-like Element of the carrier of () *
[1,x] is V15() set
{1,x} is non empty finite set
{{1,x},{1}} is non empty finite V45() set
{[1,x]} is Relation-like Function-like constant non empty trivial finite V48(1) set
(FlattenSeq <*(nt . tsg9)*>) ^ <*x*> is Relation-like NAT -defined the carrier of () -valued Function-like non empty finite FinSequence-like FinSubsequence-like Element of the carrier of () *
(<*O*> ^ ((height (dom tsg9)) |-> 1)) ^ <*x*> is Relation-like NAT -defined Function-like non empty finite V48((1 + (height (dom tsg9))) + 1) FinSequence-like FinSubsequence-like set
(1 + (height (dom tsg9))) + 1 is non empty ext-real positive non negative V32() V33() V34() V35() V39() V40() finite V46() Element of NAT
((height (dom tsg9)) |-> 1) ^ <*x*> is Relation-like NAT -defined Function-like non empty finite V48((height (dom tsg9)) + 1) FinSequence-like FinSubsequence-like set
(height (dom tsg9)) + 1 is non empty ext-real positive non negative V32() V33() V34() V35() V39() V40() finite V46() Element of NAT
<*O*> ^ (((height (dom tsg9)) |-> 1) ^ <*x*>) is Relation-like NAT -defined Function-like non empty finite V48(1 + ((height (dom tsg9)) + 1)) FinSequence-like FinSubsequence-like set
1 + ((height (dom tsg9)) + 1) is non empty ext-real positive non negative V32() V33() V34() V35() V39() V40() finite V46() Element of NAT
1 |-> 1 is Relation-like NAT -defined NAT -valued Function-like one-to-one constant non empty trivial finite V48(1) FinSequence-like FinSubsequence-like V90() V91() V92() V93() V94() V95() V96() V97() Element of 1 -tuples_on NAT
1 -tuples_on NAT is functional non empty FinSequence-membered FinSequenceSet of NAT
((height (dom tsg9)) |-> 1) ^ (1 |-> 1) is Relation-like NAT -defined NAT -valued Function-like non empty finite V48((height (dom tsg9)) + 1) FinSequence-like FinSubsequence-like V90() V91() V92() V93() FinSequence of NAT
<*O*> ^ (((height (dom tsg9)) |-> 1) ^ (1 |-> 1)) is Relation-like NAT -defined Function-like non empty finite V48(1 + ((height (dom tsg9)) + 1)) FinSequence-like FinSubsequence-like set
(height (dom tsg9)) + 1 is non empty ext-real positive non negative V32() V33() V34() V35() V39() V40() finite V46() Element of NAT
((height (dom tsg9)) + 1) |-> 1 is Relation-like NAT -defined NAT -valued Function-like finite V48((height (dom tsg9)) + 1) FinSequence-like FinSubsequence-like V90() V91() V92() V93() Element of ((height (dom tsg9)) + 1) -tuples_on NAT
((height (dom tsg9)) + 1) -tuples_on NAT is functional non empty FinSequence-membered FinSequenceSet of NAT
<*O*> ^ (((height (dom tsg9)) + 1) |-> 1) is Relation-like NAT -defined Function-like non empty finite V48(1 + ((height (dom tsg9)) + 1)) FinSequence-like FinSubsequence-like set
1 + ((height (dom tsg9)) + 1) is non empty ext-real positive non negative V32() V33() V34() V35() V39() V40() finite V46() Element of NAT
^ (dom tsg9) is non empty finite Tree-like set
height (^ (dom tsg9)) is ext-real non negative V32() V33() V34() V35() V39() V40() finite V46() Element of NAT
(height (^ (dom tsg9))) |-> 1 is Relation-like NAT -defined NAT -valued Function-like finite V48( height (^ (dom tsg9))) FinSequence-like FinSubsequence-like V90() V91() V92() V93() Element of (height (^ (dom tsg9))) -tuples_on NAT
(height (^ (dom tsg9))) -tuples_on NAT is functional non empty FinSequence-membered FinSequenceSet of NAT
<*O*> ^ ((height (^ (dom tsg9))) |-> 1) is Relation-like NAT -defined Function-like non empty finite V48(1 + (height (^ (dom tsg9)))) FinSequence-like FinSubsequence-like set
1 + (height (^ (dom tsg9))) is non empty ext-real positive non negative V32() V33() V34() V35() V39() V40() finite V46() Element of NAT
x -tree tsg9 is Relation-like the carrier of () -valued Function-like DecoratedTree-like set
dom (x -tree tsg9) is non empty Tree-like set
n is Relation-like the carrier of () -valued Function-like DecoratedTree-like ( the carrier of (), FinTrees the carrier of (),(()))
nt . n is Relation-like NAT -defined Function-like finite FinSequence-like FinSubsequence-like Element of the carrier of () *
((),(x -tree n)) is Relation-like NAT -defined the carrier of () -valued Function-like finite FinSequence-like FinSubsequence-like FinSequence of the carrier of ()
x is Relation-like the carrier of () -valued Function-like DecoratedTree-like ( the carrier of (), FinTrees the carrier of (),(()))
((),x) is Relation-like NAT -defined the carrier of () -valued Function-like finite FinSequence-like FinSubsequence-like FinSequence of the carrier of ()
dom x is non empty finite Tree-like set
height (dom x) is ext-real non negative V32() V33() V34() V35() V39() V40() finite V46() Element of NAT
(height (dom x)) |-> 1 is Relation-like NAT -defined NAT -valued Function-like finite V48( height (dom x)) FinSequence-like FinSubsequence-like V90() V91() V92() V93() Element of (height (dom x)) -tuples_on NAT
(height (dom x)) -tuples_on NAT is functional non empty FinSequence-membered FinSequenceSet of NAT
<*0*> ^ ((height (dom x)) |-> 1) is Relation-like NAT -defined NAT -valued Function-like non empty finite V48(1 + (height (dom x))) FinSequence-like FinSubsequence-like V90() V91() V92() V93() FinSequence of NAT
1 + (height (dom x)) is non empty ext-real positive non negative V32() V33() V34() V35() V39() V40() finite V46() Element of NAT
n is Relation-like the carrier of () -valued Function-like DecoratedTree-like ( the carrier of (), FinTrees the carrier of (),(()))
((),n) is Relation-like NAT -defined the carrier of () -valued Function-like finite FinSequence-like FinSubsequence-like FinSequence of the carrier of ()
dom n is non empty finite Tree-like set
height (dom n) is ext-real non negative V32() V33() V34() V35() V39() V40() finite V46() Element of NAT
(height (dom n)) |-> 1 is Relation-like NAT -defined NAT -valued Function-like finite V48( height (dom n)) FinSequence-like FinSubsequence-like V90() V91() V92() V93() Element of (height (dom n)) -tuples_on NAT
(height (dom n)) -tuples_on NAT is functional non empty FinSequence-membered FinSequenceSet of NAT
<*0*> ^ ((height (dom n)) |-> 1) is Relation-like NAT -defined NAT -valued Function-like non empty finite V48(1 + (height (dom n))) FinSequence-like FinSubsequence-like V90() V91() V92() V93() FinSequence of NAT
1 + (height (dom n)) is non empty ext-real positive non negative V32() V33() V34() V35() V39() V40() finite V46() Element of NAT
{ (<*0*> ^ (b₁ |-> 1)) where b₁ is ext-real non negative V32() V33() V34() V35() V39() V40() finite V46() Element of NAT : not b₁ = 0 } is set
nt is Element of the carrier of ()
((),nt) is functional FinSequence-membered Element of bool ( the carrier of () *)
bool ( the carrier of () *) is non empty set
{ ((),b₁) where b₁ is Relation-like the carrier of () -valued Function-like DecoratedTree-like Element of FinTrees the carrier of () : ( b₁ in (()) & b₁ . {} = nt ) } is set
dom (root-tree 0) is non empty finite Tree-like set
height (dom (root-tree 0)) is ext-real non negative V32() V33() V34() V35() V39() V40() finite V46() Element of NAT
rtO is Relation-like the carrier of () -valued Function-like DecoratedTree-like ( the carrier of (), FinTrees the carrier of (),(()))
((),rtO) is Relation-like NAT -defined the carrier of () -valued Function-like finite FinSequence-like FinSubsequence-like FinSequence of the carrier of ()
0 |-> 1 is Relation-like non-empty empty-yielding NAT -defined NAT -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( 0 ) FinSequence-like FinSubsequence-like FinSequence-membered constituted-Trees constituted-FinTrees constituted-DTrees Tree-yielding FinTree-yielding DTree-yielding V90() V91() V92() V93() Element of 0 -tuples_on NAT
0 -tuples_on NAT is functional non empty FinSequence-membered FinSequenceSet of NAT
<*0*> ^ (0 |-> 1) is Relation-like NAT -defined NAT -valued Function-like non empty finite V48(1 + 0) FinSequence-like FinSubsequence-like V90() V91() V92() V93() FinSequence of NAT
1 + 0 is non empty ext-real positive non negative V32() V33() V34() V35() V39() V40() finite V46() Element of NAT
<*O*> is Relation-like NAT -defined (()) -valued Function-like constant non empty trivial finite V48(1) FinSequence-like FinSubsequence-like Element of (()) *
(()) * is functional non empty FinSequence-membered FinSequenceSet of (())
[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
<*O*> ^ {} is Relation-like NAT -defined Function-like non empty finite FinSequence-like FinSubsequence-like set
x is set
n is Relation-like the carrier of () -valued Function-like DecoratedTree-like Element of FinTrees the carrier of ()
((),n) is Relation-like NAT -defined the carrier of () -valued Function-like finite FinSequence-like FinSubsequence-like FinSequence of the carrier of ()
n . {} is set
x is set
rtO . {} is set
x is set
n is Relation-like the carrier of () -valued Function-like DecoratedTree-like Element of FinTrees the carrier of ()
((),n) is Relation-like NAT -defined the carrier of () -valued Function-like finite FinSequence-like FinSubsequence-like FinSequence of the carrier of ()
n . {} is set
n is Relation-like NAT -defined FinTrees the carrier of () -valued Function-like finite FinSequence-like FinSubsequence-like DTree-yielding FinSequence of (())
S -tree n is Relation-like the carrier of () -valued Function-like DecoratedTree-like Element of FinTrees the carrier of ()
( the carrier of (),(FinTrees the carrier of ()),n) is Relation-like NAT -defined the carrier of () -valued Function-like finite FinSequence-like FinSubsequence-like FinSequence of the carrier of ()
len ( the carrier of (),(FinTrees the carrier of ()),n) is ext-real non negative V32() V33() V34() V35() V39() V40() finite V46() Element of NAT
tsg9 is Relation-like the carrier of () -valued Function-like DecoratedTree-like Element of FinTrees the carrier of ()
<*tsg9*> is Relation-like NAT -defined FinTrees the carrier of () -valued Function-like constant non empty trivial finite V48(1) FinSequence-like FinSubsequence-like DTree-yielding Element of (FinTrees the carrier of ()) *
(FinTrees the carrier of ()) * is functional non empty FinSequence-membered FinSequenceSet of FinTrees the carrier of ()
[1,tsg9] is V15() set
{1,tsg9} is non empty finite set
{{1,tsg9},{1}} is non empty finite V45() set
{[1,tsg9]} is Relation-like Function-like constant non empty trivial finite V48(1) set
S -tree tsg9 is Relation-like the carrier of () -valued Function-like DecoratedTree-like set
dom n is non empty finite Tree-like set
dom tsg9 is non empty finite Tree-like set
^ (dom tsg9) is non empty finite Tree-like set
height (dom n) is ext-real non negative V32() V33() V34() V35() V39() V40() finite V46() Element of NAT
height (dom tsg9) is ext-real non negative V32() V33() V34() V35() V39() V40() finite V46() Element of NAT
(height (dom tsg9)) + 1 is non empty ext-real positive non negative V32() V33() V34() V35() V39() V40() finite V46() Element of NAT
(height (dom n)) |-> 1 is Relation-like NAT -defined NAT -valued Function-like finite V48( height (dom n)) FinSequence-like FinSubsequence-like V90() V91() V92() V93() Element of (height (dom n)) -tuples_on NAT
(height (dom n)) -tuples_on NAT is functional non empty FinSequence-membered FinSequenceSet of NAT
<*0*> ^ ((height (dom n)) |-> 1) is Relation-like NAT -defined NAT -valued Function-like non empty finite V48(1 + (height (dom n))) FinSequence-like FinSubsequence-like V90() V91() V92() V93() FinSequence of NAT
1 + (height (dom n)) is non empty ext-real positive non negative V32() V33() V34() V35() V39() V40() finite V46() Element of NAT
x is set
n is ext-real non negative V32() V33() V34() V35() V39() V40() finite V46() Element of NAT
n |-> 1 is Relation-like NAT -defined NAT -valued Function-like finite V48(n) FinSequence-like FinSubsequence-like V90() V91() V92() V93() Element of n -tuples_on NAT
n -tuples_on NAT is functional non empty FinSequence-membered FinSequenceSet of NAT
<*0*> ^ (n |-> 1) is Relation-like NAT -defined NAT -valued Function-like non empty finite V48(1 + n) FinSequence-like FinSubsequence-like V90() V91() V92() V93() FinSequence of NAT
1 + n is non empty ext-real positive 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
n |-> 1 is Relation-like NAT -defined NAT -valued Function-like finite V48(n) FinSequence-like FinSubsequence-like V90() V91() V92() V93() Element of n -tuples_on NAT
n -tuples_on NAT is functional non empty FinSequence-membered FinSequenceSet of NAT
<*0*> ^ (n |-> 1) is Relation-like NAT -defined NAT -valued Function-like non empty finite V48(1 + n) FinSequence-like FinSubsequence-like V90() V91() V92() V93() FinSequence of NAT
1 + n is non empty ext-real positive non negative V32() V33() V34() V35() V39() V40() finite V46() Element of NAT
n + 1 is non empty ext-real positive non negative V32() V33() V34() V35() V39() V40() finite V46() Element of NAT
(n + 1) |-> 1 is Relation-like NAT -defined NAT -valued Function-like finite V48(n + 1) FinSequence-like FinSubsequence-like V90() V91() V92() V93() Element of (n + 1) -tuples_on NAT
(n + 1) -tuples_on NAT is functional non empty FinSequence-membered FinSequenceSet of NAT
<*0*> ^ ((n + 1) |-> 1) is Relation-like NAT -defined NAT -valued Function-like non empty finite V48(1 + (n + 1)) FinSequence-like FinSubsequence-like V90() V91() V92() V93() FinSequence of NAT
1 + (n + 1) is non empty ext-real positive non negative V32() V33() V34() V35() V39() V40() finite V46() Element of NAT
tsg9 is Relation-like the carrier of () -valued Function-like DecoratedTree-like ( the carrier of (), FinTrees the carrier of (),(()))
tsg9 . {} is set
((),tsg9) is Relation-like NAT -defined the carrier of () -valued Function-like finite FinSequence-like FinSubsequence-like FinSequence of the carrier of ()
tsg9 is Relation-like the carrier of () -valued Function-like DecoratedTree-like ( the carrier of (), FinTrees the carrier of (),(()))
tsg9 . {} is set
((),tsg9) is Relation-like NAT -defined the carrier of () -valued Function-like finite FinSequence-like FinSubsequence-like FinSequence of the carrier of ()
dom tsg9 is non empty finite Tree-like set
height (dom tsg9) is ext-real non negative V32() V33() V34() V35() V39() V40() finite V46() Element of NAT
(height (dom tsg9)) |-> 1 is Relation-like NAT -defined NAT -valued Function-like finite V48( height (dom tsg9)) FinSequence-like FinSubsequence-like V90() V91() V92() V93() Element of (height (dom tsg9)) -tuples_on NAT
(height (dom tsg9)) -tuples_on NAT is functional non empty FinSequence-membered FinSequenceSet of NAT
<*0*> ^ ((height (dom tsg9)) |-> 1) is Relation-like NAT -defined NAT -valued Function-like non empty finite V48(1 + (height (dom tsg9))) FinSequence-like FinSubsequence-like V90() V91() V92() V93() FinSequence of NAT
1 + (height (dom tsg9)) is non empty ext-real positive non negative V32() V33() V34() V35() V39() V40() finite V46() Element of NAT
len (n |-> 1) is ext-real non negative V32() V33() V34() V35() V39() V40() finite V46() Element of NAT
(S,tsg9) is Relation-like the carrier of () -valued Function-like DecoratedTree-like ( the carrier of (), FinTrees the carrier of (),(()))
tsg9 is Relation-like the carrier of () -valued Function-like DecoratedTree-like ( the carrier of (), FinTrees the carrier of (),(()))
tsg9 . {} is set
((),tsg9) is Relation-like NAT -defined the carrier of () -valued Function-like finite FinSequence-like FinSubsequence-like FinSequence of the carrier of ()
<*tsg9*> is Relation-like NAT -defined (()) -valued Function-like constant non empty trivial finite V48(1) FinSequence-like FinSubsequence-like DTree-yielding Element of (()) *
[1,tsg9] is V15() set
{1,tsg9} is non empty finite set
{{1,tsg9},{1}} is non empty finite V45() set
{[1,tsg9]} is Relation-like Function-like constant non empty trivial finite V48(1) set
S -tree <*tsg9*> is Relation-like Function-like DecoratedTree-like set
dom tsg9 is non empty finite Tree-like set
height (dom tsg9) is ext-real non negative V32() V33() V34() V35() V39() V40() finite V46() Element of NAT
^ (dom tsg9) is non empty finite Tree-like set
height (^ (dom tsg9)) is ext-real non negative V32() V33() V34() V35() V39() V40() finite V46() Element of NAT
(S,rtO) is Relation-like the carrier of () -valued Function-like DecoratedTree-like ( the carrier of (), FinTrees the carrier of (),(()))
tsg9 is Relation-like the carrier of () -valued Function-like DecoratedTree-like ( the carrier of (), FinTrees the carrier of (),(()))
tsg9 . {} is set
((),tsg9) is Relation-like NAT -defined the carrier of () -valued Function-like finite FinSequence-like FinSubsequence-like FinSequence of the carrier of ()
<*rtO*> is Relation-like NAT -defined (()) -valued Function-like constant non empty trivial finite V48(1) FinSequence-like FinSubsequence-like DTree-yielding Element of (()) *
[1,rtO] is V15() set
{1,rtO} is non empty finite set
{{1,rtO},{1}} is non empty finite V45() set
{[1,rtO]} is Relation-like Function-like constant non empty trivial finite V48(1) set
S -tree <*rtO*> is Relation-like Function-like DecoratedTree-like set
dom tsg9 is non empty finite Tree-like set
height (dom tsg9) is ext-real non negative V32() V33() V34() V35() V39() V40() finite V46() Element of NAT
dom rtO is non empty finite Tree-like set
^ (dom rtO) is non empty finite Tree-like set
height (^ (dom rtO)) is ext-real non negative V32() V33() V34() V35() V39() V40() finite V46() Element of NAT
height (dom rtO) is ext-real non negative V32() V33() V34() V35() V39() V40() finite V46() Element of NAT
(height (dom rtO)) + 1 is non empty ext-real positive non negative V32() V33() V34() V35() V39() V40() finite V46() Element of NAT
n is Relation-like the carrier of () -valued Function-like DecoratedTree-like ( the carrier of (), FinTrees the carrier of (),(()))
n . {} is set
((),n) is Relation-like NAT -defined the carrier of () -valued Function-like finite FinSequence-like FinSubsequence-like FinSequence of the carrier of ()