:: 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