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

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

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

Seg 1 is non empty trivial finite V48(1) Element of bool NAT
{ b1 where b1 is ext-real non negative V32() V33() V34() V35() V39() V40() finite V46() Element of NAT : ( 1 <= b1 & b1 <= 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
{ b1 where b1 is ext-real non negative V32() V33() V34() V35() V39() V40() finite V46() Element of NAT : ( 1 <= b1 & b1 <= 2 ) } is set
{1,2} is non empty finite V45() set

is Relation-like non empty non trivial non finite set

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

bool (Trees PN) is non empty set

PN is set
O is set

S . O is set
rng S is finite set
PN is non empty set

PN is non empty set

bool O is non empty set

PN is non empty set

TSPN is set
rng () is finite set
dom () is finite Element of bool NAT
PN is set
() . PN is set

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

() . O is set

S . {} is set

dom nt is non empty Tree-like set

nt . rtO is Element of PN

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

PN . {} is set

[1,(PN . {})] is V15() set
{1,(PN . {})} is non empty finite set
{{1,(PN . {})},{1}} is non empty finite V45() 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

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

bool (FinTrees PN) is non empty set

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

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

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

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

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

PN . {} is set
O . {} is set

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

[1,(O . {})] is V15() set
{1,(O . {})} is non empty finite set
{{1,(O . {})},{1}} is non empty finite V45() 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

dom (pr1 S) is set

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
{ b1 where b1 is ext-real non negative V32() V33() V34() V35() V39() V40() finite V46() Element of NAT : ( 1 <= b1 & b1 <= len S ) } is 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

dom (pr2 S) is set

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
{ b1 where b1 is ext-real non negative V32() V33() V34() V35() V39() V40() finite V46() Element of NAT : ( 1 <= b1 & b1 <= len S ) } is 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

PN is non empty set

[: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
F1() is non empty set
F1() * is functional non empty FinSequence-membered FinSequenceSet of F1()
[:F1(),(F1() *):] is Relation-like non empty set
bool [:F1(),(F1() *):] is non empty set
PN is Relation-like Element of bool [:F1(),(F1() *):]
DTConstrStr(# F1(),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

[: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
F1() 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

S is Element 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

S is Element 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
{ b1 where b1 is Element of the carrier of PN : for b2 being Relation-like NAT -defined Function-like finite FinSequence-like FinSubsequence-like set holds not b1 ==> b2 } is set
{ b1 where b1 is Element of the carrier of PN : ex b2 being Relation-like NAT -defined Function-like finite FinSequence-like FinSubsequence-like set st b1 ==> b2 } is set
O is set
S is Element of the carrier of PN

PN is Element of the carrier of PN
F3() is non empty set

dom F1() is set
F1() . 0 is set
F2() is non empty DTConstrStr
the carrier of F2() is non empty set
[: the carrier of F2(),F3():] is Relation-like non empty set
Terminals F2() is set
{ (root-tree [b1,b2]) where b1 is Element of the carrier of F2(), b2 is Element of F3() : ( ( b1 in Terminals F2() & b2 = F4(b1) ) or ( b1 ==> {} & b2 = F5(b1,{},{}) ) ) } is set
FinTrees [: the carrier of F2(),F3():] is functional non empty constituted-DTrees DTree-set of [: the carrier of F2(),F3():]
bool (FinTrees [: the carrier of F2(),F3():]) is non empty set
Union F1() is set
TSPN is set
PN is set
O is Element of the carrier of F2()
S is Element of F3()
[O,S] is V15() Element of [: the carrier of F2(),F3():]
{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 F2(),F3():] -valued Function-like DecoratedTree-like Element of FinTrees [: the carrier of F2(),F3():]
F4(O) is Element of F3()
F5(O,{},{}) is Element of F3()
PN is ext-real non negative V32() V33() V34() V35() V39() V40() finite V46() Element of NAT
F1() . PN is set
PN + 1 is non empty ext-real positive non negative V32() V33() V34() V35() V39() V40() finite V46() Element of NAT
F1() . (PN + 1) is set
O is set
(F1() . PN) * is functional non empty FinSequence-membered FinSequenceSet of F1() . PN
{ ([b1,H3(b1,b2)] -tree b2) where b1 is Element of the carrier of F2(), b2 is Relation-like NAT -defined F1() . PN -valued Function-like finite FinSequence-like FinSubsequence-like Element of (F1() . PN) * : ex b3 being Relation-like NAT -defined FinTrees [: the carrier of F2(),F3():] -valued Function-like finite FinSequence-like FinSubsequence-like DTree-yielding FinSequence of FinTrees [: the carrier of F2(),F3():] st
( b2 = b3 & b1 ==> ( the carrier of F2(),F3(),([: the carrier of F2(),F3():],(FinTrees [: the carrier of F2(),F3():]),b3)) )
}
is set

(F1() . PN) \/ { ([b1,H3(b1,b2)] -tree b2) where b1 is Element of the carrier of F2(), b2 is Relation-like NAT -defined F1() . PN -valued Function-like finite FinSequence-like FinSubsequence-like Element of (F1() . PN) * : ex b3 being Relation-like NAT -defined FinTrees [: the carrier of F2(),F3():] -valued Function-like finite FinSequence-like FinSubsequence-like DTree-yielding FinSequence of FinTrees [: the carrier of F2(),F3():] st
( b2 = b3 & b1 ==> ( the carrier of F2(),F3(),([: the carrier of F2(),F3():],(FinTrees [: the carrier of F2(),F3():]),b3)) )
}
is set

S is Element of the carrier of F2()

F5(S,(pr1 (roots nt)),(pr2 (roots nt))) is Element of F3()
[S,H3(S,nt)] is V15() Element of [: the carrier of F2(),F3():]
{S,F5(S,(pr1 (roots nt)),(pr2 (roots nt)))} is non empty finite set
{S} is non empty trivial finite V48(1) set
{{S,F5(S,(pr1 (roots nt)),(pr2 (roots nt)))},{S}} is non empty finite V45() set
[S,H3(S,nt)] -tree nt is Relation-like Function-like DecoratedTree-like set
x is Relation-like NAT -defined FinTrees [: the carrier of F2(),F3():] -valued Function-like finite FinSequence-like FinSubsequence-like DTree-yielding FinSequence of FinTrees [: the carrier of F2(),F3():]
([: the carrier of F2(),F3():],(FinTrees [: the carrier of F2(),F3():]),x) is Relation-like NAT -defined [: the carrier of F2(),F3():] -valued Function-like finite FinSequence-like FinSubsequence-like FinSequence of [: the carrier of F2(),F3():]
( the carrier of F2(),F3(),([: the carrier of F2(),F3():],(FinTrees [: the carrier of F2(),F3():]),x)) is Relation-like NAT -defined the carrier of F2() -valued Function-like finite FinSequence-like FinSubsequence-like FinSequence of the carrier of F2()
rtO is Relation-like NAT -defined FinTrees [: the carrier of F2(),F3():] -valued Function-like finite FinSequence-like FinSubsequence-like DTree-yielding FinSequence of FinTrees [: the carrier of F2(),F3():]

F5(S,(pr1 (roots rtO)),(pr2 (roots rtO))) is Element of F3()
[S,H3(S,rtO)] is V15() Element of [: the carrier of F2(),F3():]
{S,F5(S,(pr1 (roots rtO)),(pr2 (roots rtO)))} is non empty finite set
{{S,F5(S,(pr1 (roots rtO)),(pr2 (roots rtO)))},{S}} is non empty finite V45() set
[S,H3(S,rtO)] -tree rtO is Relation-like [: the carrier of F2(),F3():] -valued Function-like DecoratedTree-like Element of FinTrees [: the carrier of F2(),F3():]
PN is set
F1() . PN is set
TSPN is functional constituted-DTrees Element of bool (FinTrees [: the carrier of F2(),F3():])
PN is Element of the carrier of F2()
F4(PN) is Element of F3()
[PN,F4(PN)] is V15() Element of [: the carrier of F2(),F3():]
{PN,F4(PN)} is non empty finite set
{PN} is non empty trivial finite V48(1) set
{{PN,F4(PN)},{PN}} is non empty finite V45() set
root-tree [PN,F4(PN)] is Relation-like [: the carrier of F2(),F3():] -valued Function-like DecoratedTree-like Element of FinTrees [: the carrier of F2(),F3():]
PN is Element of the carrier of F2()

([: the carrier of F2(),F3():],(FinTrees [: the carrier of F2(),F3():]),O) is Relation-like NAT -defined [: the carrier of F2(),F3():] -valued Function-like finite FinSequence-like FinSubsequence-like FinSequence of [: the carrier of F2(),F3():]
( the carrier of F2(),F3(),([: the carrier of F2(),F3():],(FinTrees [: the carrier of F2(),F3():]),O)) is Relation-like NAT -defined the carrier of F2() -valued Function-like finite FinSequence-like FinSubsequence-like FinSequence of the carrier of F2()
( the carrier of F2(),F3(),([: the carrier of F2(),F3():],(FinTrees [: the carrier of F2(),F3():]),O)) is Relation-like NAT -defined F3() -valued Function-like finite FinSequence-like FinSubsequence-like FinSequence of F3()

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
{ b1 where b1 is ext-real non negative V32() V33() V34() V35() V39() V40() finite V46() Element of NAT : ( 1 <= b1 & b1 <= len O ) } is set
rtO is ext-real non negative V32() V33() V34() V35() V39() V40() finite V46() set

rng O is finite set
x is set
F1() . x is set

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
F1() . n is set
n is set
tsg9 is 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
{ ([b1,F5(b1,(pr1 (roots b2)),(pr2 (roots b2)))] -tree b2) where b1 is Element of the carrier of F2(), b2 is Relation-like NAT -defined F1() . a1 -valued Function-like finite FinSequence-like FinSubsequence-like Element of (F1() . a1) * : ex b3 being Relation-like NAT -defined FinTrees [: the carrier of F2(),F3():] -valued Function-like finite FinSequence-like FinSubsequence-like DTree-yielding FinSequence of FinTrees [: the carrier of F2(),F3():] st
( b2 = b3 & b1 ==> ( the carrier of F2(),F3(),([: the carrier of F2(),F3():],(FinTrees [: the carrier of F2(),F3():]),b3)) )
}
is set

ts is ext-real non negative V32() V33() V34() V35() V39() V40() finite V46() Element of NAT
F1() . ts is set
ts + 1 is non empty ext-real positive non negative V32() V33() V34() V35() V39() V40() finite V46() Element of NAT
F1() . (ts + 1) is set
(F1() . ts) * is functional non empty FinSequence-membered FinSequenceSet of F1() . ts
{ ([b1,F5(b1,(pr1 (roots b2)),(pr2 (roots b2)))] -tree b2) where b1 is Element of the carrier of F2(), b2 is Relation-like NAT -defined F1() . ts -valued Function-like finite FinSequence-like FinSubsequence-like Element of (F1() . ts) * : ex b3 being Relation-like NAT -defined FinTrees [: the carrier of F2(),F3():] -valued Function-like finite FinSequence-like FinSubsequence-like DTree-yielding FinSequence of FinTrees [: the carrier of F2(),F3():] st
( b2 = b3 & b1 ==> ( the carrier of F2(),F3(),([: the carrier of F2(),F3():],(FinTrees [: the carrier of F2(),F3():]),b3)) )
}
is set

(F1() . ts) \/ H4(ts,F1() . ts) is set
F1() . f2 is set
F1() . (rtO . tsg9) is set
x is ext-real non negative V32() V33() V34() V35() V39() V40() finite V46() Element of NAT
F1() . x is set
x is ext-real non negative V32() V33() V34() V35() V39() V40() finite V46() Element of NAT
F1() . x is set
rng F1() is set
union (rng F1()) is set
n is functional constituted-DTrees Element of bool (FinTrees [: the carrier of F2(),F3():])

F5(PN,( the carrier of F2(),F3(),([: the carrier of F2(),F3():],(FinTrees [: the carrier of F2(),F3():]),O)),( the carrier of F2(),F3(),([: the carrier of F2(),F3():],(FinTrees [: the carrier of F2(),F3():]),O))) is Element of F3()
[PN,F5(PN,( the carrier of F2(),F3(),([: the carrier of F2(),F3():],(FinTrees [: the carrier of F2(),F3():]),O)),( the carrier of F2(),F3(),([: the carrier of F2(),F3():],(FinTrees [: the carrier of F2(),F3():]),O)))] is V15() Element of [: the carrier of F2(),F3():]
{PN,F5(PN,( the carrier of F2(),F3(),([: the carrier of F2(),F3():],(FinTrees [: the carrier of F2(),F3():]),O)),( the carrier of F2(),F3(),([: the carrier of F2(),F3():],(FinTrees [: the carrier of F2(),F3():]),O)))} is non empty finite set
{PN} is non empty trivial finite V48(1) set
{{PN,F5(PN,( the carrier of F2(),F3(),([: the carrier of F2(),F3():],(FinTrees [: the carrier of F2(),F3():]),O)),( the carrier of F2(),F3(),([: the carrier of F2(),F3():],(FinTrees [: the carrier of F2(),F3():]),O)))},{PN}} is non empty finite V45() set

[PN,F5(PN,( the carrier of F2(),F3(),([: the carrier of F2(),F3():],(FinTrees [: the carrier of F2(),F3():]),O)),( the carrier of F2(),F3(),([: the carrier of F2(),F3():],(FinTrees [: the carrier of F2(),F3():]),O)))] -tree tsg9 is Relation-like Function-like DecoratedTree-like set
{ ([b1,H3(b1,b2)] -tree b2) where b1 is Element of the carrier of F2(), b2 is Relation-like NAT -defined n -valued Function-like finite FinSequence-like FinSubsequence-like DTree-yielding Element of n * : ex b3 being Relation-like NAT -defined FinTrees [: the carrier of F2(),F3():] -valued Function-like finite FinSequence-like FinSubsequence-like DTree-yielding FinSequence of FinTrees [: the carrier of F2(),F3():] st
( b2 = b3 & b1 ==> ( the carrier of F2(),F3(),([: the carrier of F2(),F3():],(FinTrees [: the carrier of F2(),F3():]),b3)) )
}
is set

(F1() . x) \/ { ([b1,H3(b1,b2)] -tree b2) where b1 is Element of the carrier of F2(), b2 is Relation-like NAT -defined n -valued Function-like finite FinSequence-like FinSubsequence-like DTree-yielding Element of n * : ex b3 being Relation-like NAT -defined FinTrees [: the carrier of F2(),F3():] -valued Function-like finite FinSequence-like FinSubsequence-like DTree-yielding FinSequence of FinTrees [: the carrier of F2(),F3():] st
( b2 = b3 & b1 ==> ( the carrier of F2(),F3(),([: the carrier of F2(),F3():],(FinTrees [: the carrier of F2(),F3():]),b3)) )
}
is set

x + 1 is non empty ext-real positive non negative V32() V33() V34() V35() V39() V40() finite V46() Element of NAT
F1() . (x + 1) is set
[PN,F5(PN,( the carrier of F2(),F3(),([: the carrier of F2(),F3():],(FinTrees [: the carrier of F2(),F3():]),O)),( the carrier of F2(),F3(),([: the carrier of F2(),F3():],(FinTrees [: the carrier of F2(),F3():]),O)))] -tree O is Relation-like [: the carrier of F2(),F3():] -valued Function-like DecoratedTree-like Element of FinTrees [: the carrier of F2(),F3():]
PN is functional constituted-DTrees Element of bool (FinTrees [: the carrier of F2(),F3():])
O is set

([: the carrier of F2(),F3():],(FinTrees [: the carrier of F2(),F3():]),S) is Relation-like NAT -defined [: the carrier of F2(),F3():] -valued Function-like finite FinSequence-like FinSubsequence-like FinSequence of [: the carrier of F2(),F3():]
( the carrier of F2(),F3(),([: the carrier of F2(),F3():],(FinTrees [: the carrier of F2(),F3():]),S)) is Relation-like NAT -defined the carrier of F2() -valued Function-like finite FinSequence-like FinSubsequence-like FinSequence of the carrier of F2()

nt is Element of the carrier of F2()
rtO is Element of F3()
[nt,rtO] is V15() Element of [: the carrier of F2(),F3():]
{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 F2(),F3():] -valued Function-like DecoratedTree-like Element of FinTrees [: the carrier of F2(),F3():]
F4(nt) is Element of F3()
F5(nt,(pr1 ()),(pr2 ())) is Element of F3()
[nt,rtO] -tree S is Relation-like [: the carrier of F2(),F3():] -valued Function-like DecoratedTree-like Element of FinTrees [: the carrier of F2(),F3():]
O is ext-real non negative V32() V33() V34() V35() V39() V40() finite V46() Element of NAT
F1() . O is set
O + 1 is non empty ext-real positive non negative V32() V33() V34() V35() V39() V40() finite V46() Element of NAT
F1() . (O + 1) is set
S is set
(F1() . O) * is functional non empty FinSequence-membered FinSequenceSet of F1() . O
{ ([b1,H3(b1,b2)] -tree b2) where b1 is Element of the carrier of F2(), b2 is Relation-like NAT -defined F1() . O -valued Function-like finite FinSequence-like FinSubsequence-like Element of (F1() . O) * : ex b3 being Relation-like NAT -defined FinTrees [: the carrier of F2(),F3():] -valued Function-like finite FinSequence-like FinSubsequence-like DTree-yielding FinSequence of FinTrees [: the carrier of F2(),F3():] st
( b2 = b3 & b1 ==> ( the carrier of F2(),F3(),([: the carrier of F2(),F3():],(FinTrees [: the carrier of F2(),F3():]),b3)) )
}
is set

(F1() . O) \/ { ([b1,H3(b1,b2)] -tree b2) where b1 is Element of the carrier of F2(), b2 is Relation-like NAT -defined F1() . O -valued Function-like finite FinSequence-like FinSubsequence-like Element of (F1() . O) * : ex b3 being Relation-like NAT -defined FinTrees [: the carrier of F2(),F3():] -valued Function-like finite FinSequence-like FinSubsequence-like DTree-yielding FinSequence of FinTrees [: the carrier of F2(),F3():] st
( b2 = b3 & b1 ==> ( the carrier of F2(),F3(),([: the carrier of F2(),F3():],(FinTrees [: the carrier of F2(),F3():]),b3)) )
}
is set

nt is Element of the carrier of F2()

F5(nt,(pr1 (roots rtO)),(pr2 (roots rtO))) is Element of F3()
[nt,H3(nt,rtO)] is V15() Element of [: the carrier of F2(),F3():]
{nt,F5(nt,(pr1 (roots rtO)),(pr2 (roots rtO)))} is non empty finite set
{nt} is non empty trivial finite V48(1) set
{{nt,F5(nt,(pr1 (roots rtO)),(pr2 (roots rtO)))},{nt}} is non empty finite V45() set
[nt,H3(nt,rtO)] -tree rtO is Relation-like Function-like DecoratedTree-like set
rng rtO is finite set

([: the carrier of F2(),F3():],(FinTrees [: the carrier of F2(),F3():]),x) is Relation-like NAT -defined [: the carrier of F2(),F3():] -valued Function-like finite FinSequence-like FinSubsequence-like FinSequence of [: the carrier of F2(),F3():]
( the carrier of F2(),F3(),([: the carrier of F2(),F3():],(FinTrees [: the carrier of F2(),F3():]),x)) is Relation-like NAT -defined the carrier of F2() -valued Function-like finite FinSequence-like FinSubsequence-like FinSequence of the carrier of F2()
n is Relation-like NAT -defined FinTrees [: the carrier of F2(),F3():] -valued Function-like finite FinSequence-like FinSubsequence-like DTree-yielding FinSequence of FinTrees [: the carrier of F2(),F3():]
([: the carrier of F2(),F3():],(FinTrees [: the carrier of F2(),F3():]),n) is Relation-like NAT -defined [: the carrier of F2(),F3():] -valued Function-like finite FinSequence-like FinSubsequence-like FinSequence of [: the carrier of F2(),F3():]
( the carrier of F2(),F3(),([: the carrier of F2(),F3():],(FinTrees [: the carrier of F2(),F3():]),n)) is Relation-like NAT -defined the carrier of F2() -valued Function-like finite FinSequence-like FinSubsequence-like FinSequence of the carrier of F2()
O is set
S is set
F1() . S is set
F3() is non empty set

dom F1() is set
F1() . 0 is set
F2() is non empty DTConstrStr
the carrier of F2() is non empty set
[: the carrier of F2(),F3():] is Relation-like non empty set
Terminals F2() is set
{ (root-tree [b1,b2]) where b1 is Element of the carrier of F2(), b2 is Element of F3() : ( ( b1 in Terminals F2() & b2 = F4(b1) ) or ( b1 ==> {} & b2 = F5(b1,{},{}) ) ) } is set
FinTrees [: the carrier of F2(),F3():] is functional non empty constituted-DTrees DTree-set of [: the carrier of F2(),F3():]
FinTrees the carrier of F2() is functional non empty constituted-DTrees DTree-set of the carrier of F2()
bool (FinTrees the carrier of F2()) is non empty set
Union F1() is set
{ (b1 `1) where b1 is Relation-like [: the carrier of F2(),F3():] -valued Function-like DecoratedTree-like Element of FinTrees [: the carrier of F2(),F3():] : b1 in Union F1() } 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
F1() . (O + 1) is set
F1() . O is set
(F1() . O) * is functional non empty FinSequence-membered FinSequenceSet of F1() . O
{ ([b1,F5(b1,(pr1 (roots b2)),(pr2 (roots b2)))] -tree b2) where b1 is Element of the carrier of F2(), b2 is Relation-like NAT -defined F1() . O -valued Function-like finite FinSequence-like FinSubsequence-like Element of (F1() . O) * : ex b3 being Relation-like NAT -defined FinTrees [: the carrier of F2(),F3():] -valued Function-like finite FinSequence-like FinSubsequence-like DTree-yielding FinSequence of FinTrees [: the carrier of F2(),F3():] st
( b2 = b3 & b1 ==> ( the carrier of F2(),F3(),([: the carrier of F2(),F3():],(FinTrees [: the carrier of F2(),F3():]),b3)) )
}
is set

(F1() . O) \/ { ([b1,F5(b1,(pr1 (roots b2)),(pr2 (roots b2)))] -tree b2) where b1 is Element of the carrier of F2(), b2 is Relation-like NAT -defined F1() . O -valued Function-like finite FinSequence-like FinSubsequence-like Element of (F1() . O) * : ex b3 being Relation-like NAT -defined FinTrees [: the carrier of F2(),F3():] -valued Function-like finite FinSequence-like FinSubsequence-like DTree-yielding FinSequence of FinTrees [: the carrier of F2(),F3():] st
( b2 = b3 & b1 ==> ( the carrier of F2(),F3(),([: the carrier of F2(),F3():],(FinTrees [: the carrier of F2(),F3():]),b3)) )
}
is set

bool (FinTrees [: the carrier of F2(),F3():]) is non empty set
O is functional constituted-DTrees Element of bool (FinTrees [: the carrier of F2(),F3():])
nt is set
rtO is Relation-like [: the carrier of F2(),F3():] -valued Function-like DecoratedTree-like Element of FinTrees [: the carrier of F2(),F3():]

pr1 ( the carrier of F2(),F3()) is Relation-like Function-like V18([: the carrier of F2(),F3():], the carrier of F2()) Element of bool [:[: the carrier of F2(),F3():], the carrier of F2():]
[:[: the carrier of F2(),F3():], the carrier of F2():] is Relation-like non empty set
bool [:[: the carrier of F2(),F3():], the carrier of F2():] is non empty set
rtO * (pr1 ( the carrier of F2(),F3())) is Relation-like Function-like DecoratedTree-like set
rng rtO is set
dom (pr1 ( the carrier of F2(),F3())) 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 F2())
rtO is functional constituted-DTrees Element of bool (FinTrees the carrier of F2())
x is Element of the carrier of F2()
F4(x) is Element of F3()
[x,F4(x)] is V15() Element of [: the carrier of F2(),F3():]
{x,F4(x)} is non empty finite set
{x} is non empty trivial finite V48(1) set
{{x,F4(x)},{x}} is non empty finite V45() set
root-tree [x,F4(x)] is Relation-like [: the carrier of F2(),F3():] -valued Function-like DecoratedTree-like Element of FinTrees [: the carrier of F2(),F3():]
(root-tree [x,F4(x)]) `1 is Relation-like the carrier of F2() -valued Function-like DecoratedTree-like set
root-tree x is Relation-like the carrier of F2() -valued Function-like DecoratedTree-like Element of FinTrees the carrier of F2()
x is Element of the carrier of F2()

( the carrier of F2(),(FinTrees the carrier of F2()),n) is Relation-like NAT -defined the carrier of F2() -valued Function-like finite FinSequence-like FinSubsequence-like FinSequence of the carrier of F2()

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
{ b1 where b1 is ext-real non negative V32() V33() V34() V35() V39() V40() finite V46() Element of NAT : ( 1 <= b1 & b1 <= len n ) } is set
n is ext-real non negative V32() V33() V34() V35() V39() V40() finite V46() set

rng n is finite set
tsg9 is Relation-like [: the carrier of F2(),F3():] -valued Function-like DecoratedTree-like Element of FinTrees [: the carrier of F2(),F3():]

n is Relation-like NAT -defined FinTrees [: the carrier of F2(),F3():] -valued Function-like finite FinSequence-like FinSubsequence-like DTree-yielding FinSequence of FinTrees [: the carrier of F2(),F3():]

rng n is finite set
tsg9 is set
tsg9 is set

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

nt is Relation-like [: the carrier of F2(),F3():] -valued Function-like DecoratedTree-like set

dom ( the carrier of F2(),(FinTrees the carrier of F2()),n) is finite Element of bool NAT

([: the carrier of F2(),F3():],(FinTrees [: the carrier of F2(),F3():]),tsg9) is Relation-like NAT -defined [: the carrier of F2(),F3():] -valued Function-like finite FinSequence-like FinSubsequence-like FinSequence of [: the carrier of F2(),F3():]
( the carrier of F2(),F3(),([: the carrier of F2(),F3():],(FinTrees [: the carrier of F2(),F3():]),tsg9)) is Relation-like NAT -defined the carrier of F2() -valued Function-like finite FinSequence-like FinSubsequence-like FinSequence of the carrier of F2()
dom ( the carrier of F2(),F3(),([: the carrier of F2(),F3():],(FinTrees [: the carrier of F2(),F3():]),tsg9)) is finite Element of bool NAT
dom ([: the carrier of F2(),F3():],(FinTrees [: the carrier of F2(),F3():]),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

f2 is Relation-like [: the carrier of F2(),F3():] -valued Function-like DecoratedTree-like set

dom f2 is non empty Tree-like set
( the carrier of F2(),(FinTrees the carrier of F2()),n) . tsg9 is set

f2 . nt is Element of [: the carrier of F2(),F3():]
(f2 . nt) `1 is Element of the carrier of F2()

ts . {} is set
([: the carrier of F2(),F3():],(FinTrees [: the carrier of F2(),F3():]),tsg9) . tsg9 is set
( the carrier of F2(),F3(),([: the carrier of F2(),F3():],(FinTrees [: the carrier of F2(),F3():]),tsg9)) . tsg9 is set

ts . {} is set

F5(x,(pr1 (roots tsg9)),(pr2 (roots tsg9))) is Element of F3()
[x,H3(x,tsg9)] is V15() Element of [: the carrier of F2(),F3():]
{x,F5(x,(pr1 (roots tsg9)),(pr2 (roots tsg9)))} is non empty finite set
{x} is non empty trivial finite V48(1) set
{{x,F5(x,(pr1 (roots tsg9)),(pr2 (roots tsg9)))},{x}} is non empty finite V45() set
[x,H3(x,tsg9)] -tree tsg9 is Relation-like [: the carrier of F2(),F3():] -valued Function-like DecoratedTree-like Element of FinTrees [: the carrier of F2(),F3():]
rng tsg9 is finite set
Trees [: the carrier of F2(),F3():] is functional non empty constituted-DTrees DTree-set of [: the carrier of F2(),F3():]
rng n is finite set
Trees the carrier of F2() is functional non empty constituted-DTrees DTree-set of the carrier of F2()
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

ts is Relation-like [: the carrier of F2(),F3():] -valued Function-like DecoratedTree-like set

p21 is Relation-like [: the carrier of F2(),F3():] -valued Function-like DecoratedTree-like set

tsg9 is Relation-like NAT -defined Trees [: the carrier of F2(),F3():] -valued Function-like finite FinSequence-like FinSubsequence-like DTree-yielding FinSequence of Trees [: the carrier of F2(),F3():]
[x,H3(x,tsg9)] -tree tsg9 is Relation-like [: the carrier of F2(),F3():] -valued Function-like DecoratedTree-like set
([x,H3(x,tsg9)] -tree tsg9) `1 is Relation-like the carrier of F2() -valued Function-like DecoratedTree-like set

x -tree n is Relation-like the carrier of F2() -valued Function-like DecoratedTree-like Element of FinTrees the carrier of F2()
x is functional constituted-DTrees Element of bool (FinTrees the carrier of F2())
n is set
n is Relation-like [: the carrier of F2(),F3():] -valued Function-like DecoratedTree-like Element of FinTrees [: the carrier of F2(),F3():]

{ b1 where b1 is Relation-like [: the carrier of F2(),F3():] -valued Function-like DecoratedTree-like Element of FinTrees [: the carrier of F2(),F3():] : b1 `1 in x } is set
tsg9 is set
f2 is Relation-like [: the carrier of F2(),F3():] -valued Function-like DecoratedTree-like Element of FinTrees [: the carrier of F2(),F3():]

f2 is Element of the carrier of F2()
root-tree f2 is Relation-like the carrier of F2() -valued Function-like DecoratedTree-like Element of FinTrees the carrier of F2()
F4(f2) is Element of F3()
[f2,F4(f2)] is V15() Element of [: the carrier of F2(),F3():]
{f2,F4(f2)} is non empty finite set
{f2} is non empty trivial finite V48(1) set
{{f2,F4(f2)},{f2}} is non empty finite V45() set
root-tree [f2,F4(f2)] is Relation-like [: the carrier of F2(),F3():] -valued Function-like DecoratedTree-like Element of FinTrees [: the carrier of F2(),F3():]
(root-tree [f2,F4(f2)]) `1 is Relation-like the carrier of F2() -valued Function-like DecoratedTree-like set
tsg9 is functional constituted-DTrees Element of bool (FinTrees [: the carrier of F2(),F3():])
f2 is Element of the carrier of F2()

([: the carrier of F2(),F3():],(FinTrees [: the carrier of F2(),F3():]),nt) is Relation-like NAT -defined [: the carrier of F2(),F3():] -valued Function-like finite FinSequence-like FinSubsequence-like FinSequence of [: the carrier of F2(),F3():]
( the carrier of F2(),F3(),([: the carrier of F2(),F3():],(FinTrees [: the carrier of F2(),F3():]),nt)) is Relation-like NAT -defined the carrier of F2() -valued Function-like finite FinSequence-like FinSubsequence-like FinSequence of the carrier of F2()
dom nt is finite Element of bool NAT
( the carrier of F2(),F3(),([: the carrier of F2(),F3():],(FinTrees [: the carrier of F2(),F3():]),nt)) is Relation-like NAT -defined F3() -valued Function-like finite FinSequence-like FinSubsequence-like FinSequence of F3()
F5(f2,( the carrier of F2(),F3(),([: the carrier of F2(),F3():],(FinTrees [: the carrier of F2(),F3():]),nt)),( the carrier of F2(),F3(),([: the carrier of F2(),F3():],(FinTrees [: the carrier of F2(),F3():]),nt))) is Element of F3()
[f2,F5(f2,( the carrier of F2(),F3(),([: the carrier of F2(),F3():],(FinTrees [: the carrier of F2(),F3():]),nt)),( the carrier of F2(),F3(),([: the carrier of F2(),F3():],(FinTrees [: the carrier of F2(),F3():]),nt)))] is V15() Element of [: the carrier of F2(),F3():]
{f2,F5(f2,( the carrier of F2(),F3(),([: the carrier of F2(),F3():],(FinTrees [: the carrier of F2(),F3():]),nt)),( the carrier of F2(),F3(),([: the carrier of F2(),F3():],(FinTrees [: the carrier of F2(),F3():]),nt)))} is non empty finite set
{f2} is non empty trivial finite V48(1) set
{{f2,F5(f2,( the carrier of F2(),F3(),([: the carrier of F2(),F3():],(FinTrees [: the carrier of F2(),F3():]),nt)),( the carrier of F2(),F3(),([: the carrier of F2(),F3():],(FinTrees [: the carrier of F2(),F3():]),nt)))},{f2}} is non empty finite V45() set
[f2,F5(f2,( the carrier of F2(),F3(),([: the carrier of F2(),F3():],(FinTrees [: the carrier of F2(),F3():]),nt)),( the carrier of F2(),F3(),([: the carrier of F2(),F3():],(FinTrees [: the carrier of F2(),F3():]),nt)))] -tree nt is Relation-like [: the carrier of F2(),F3():] -valued Function-like DecoratedTree-like Element of FinTrees [: the carrier of F2(),F3():]
([f2,F5(f2,( the carrier of F2(),F3(),([: the carrier of F2(),F3():],(FinTrees [: the carrier of F2(),F3():]),nt)),( the carrier of F2(),F3(),([: the carrier of F2(),F3():],(FinTrees [: the carrier of F2(),F3():]),nt)))] -tree nt) `1 is Relation-like the carrier of F2() -valued Function-like DecoratedTree-like set

dom ts is finite Element of bool NAT
f2 -tree ts is Relation-like the carrier of F2() -valued Function-like DecoratedTree-like Element of FinTrees the carrier of F2()
rng ts is finite set
p21 is set
k is set

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

rng nt is finite set
p2k is Relation-like [: the carrier of F2(),F3():] -valued Function-like DecoratedTree-like Element of FinTrees [: the carrier of F2(),F3():]

c22 is Relation-like [: the carrier of F2(),F3():] -valued Function-like DecoratedTree-like Element of FinTrees [: the carrier of F2(),F3():]

( the carrier of F2(),(FinTrees the carrier of F2()),p21) is Relation-like NAT -defined the carrier of F2() -valued Function-like finite FinSequence-like FinSubsequence-like FinSequence of the carrier of F2()
dom ( the carrier of F2(),(FinTrees the carrier of F2()),p21) is finite Element of bool NAT
dom p21 is finite Element of bool NAT
dom ( the carrier of F2(),F3(),([: the carrier of F2(),F3():],(FinTrees [: the carrier of F2(),F3():]),nt)) is finite Element of bool NAT
dom ([: the carrier of F2(),F3():],(FinTrees [: the carrier of F2(),F3():]),nt) is finite Element of bool NAT
k is ext-real non negative V32() V33() V34() V35() V39() V40() finite V46() set

rng nt is finite set

p1k is Relation-like [: the carrier of F2(),F3():] -valued Function-like DecoratedTree-like Element of FinTrees [: the carrier of F2(),F3():]

dom p1k is non empty finite Tree-like set
( the carrier of F2(),(FinTrees the carrier of F2()),p21) . k is set

p1k . p2k is Element of [: the carrier of F2(),F3():]
(p1k . p2k) `1 is Element of the carrier of F2()

c22 . {} is set
c23 is Relation-like [: the carrier of F2(),F3():] -valued Function-like DecoratedTree-like Element of FinTrees [: the carrier of F2(),F3():]

([: the carrier of F2(),F3():],(FinTrees [: the carrier of F2(),F3():]),nt) . k is set
( the carrier of F2(),F3(),([: the carrier of F2(),F3():],(FinTrees [: the carrier of F2(),F3():]),nt)) . k is set

c22 . {} is set

F5(f2,(pr1 (roots nt)),(pr2 (roots nt))) is Element of F3()
[f2,H3(f2,nt)] is V15() Element of [: the carrier of F2(),F3():]
{f2,F5(f2,(pr1 (roots nt)),(pr2 (roots nt)))} is non empty finite set
{{f2,F5(f2,(pr1 (roots nt)),(pr2 (roots nt)))},{f2}} is non empty finite V45() set
[f2,H3(f2,nt)] -tree nt is Relation-like [: the carrier of F2(),F3():] -valued Function-like DecoratedTree-like Element of FinTrees [: the carrier of F2(),F3():]
f2 is Relation-like [: the carrier of F2(),F3():] -valued Function-like DecoratedTree-like Element of FinTrees [: the carrier of F2(),F3():]

F3() is non empty set

dom F1() is set
F1() . 0 is set
F2() is non empty DTConstrStr
the carrier of F2() is non empty set
[: the carrier of F2(),F3():] is Relation-like non empty set
Terminals F2() is set
{ (root-tree [b1,b2]) where b1 is Element of the carrier of F2(), b2 is Element of F3() : ( ( b1 in Terminals F2() & b2 = F4(b1) ) or ( b1 ==> {} & b2 = F5(b1,{},{}) ) ) } is set
FinTrees [: the carrier of F2(),F3():] is functional non empty constituted-DTrees DTree-set of [: the carrier of F2(),F3():]
Union F1() is set
PN is Relation-like [: the carrier of F2(),F3():] -valued Function-like DecoratedTree-like Element of FinTrees [: the carrier of F2(),F3():]
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 F2()
S is Element of F3()
[O,S] is V15() Element of [: the carrier of F2(),F3():]
{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 F2(),F3():] -valued Function-like DecoratedTree-like Element of FinTrees [: the carrier of F2(),F3():]
F4(O) is Element of F3()
F5(O,{},{}) is Element of F3()
O is ext-real non negative V32() V33() V34() V35() V39() V40() finite V46() Element of NAT
F1() . O is set
O + 1 is non empty ext-real positive non negative V32() V33() V34() V35() V39() V40() finite V46() Element of NAT
F1() . (O + 1) is set
(F1() . O) * is functional non empty FinSequence-membered FinSequenceSet of F1() . O
{ ([b1,H3(b1,b2)] -tree b2) where b1 is Element of the carrier of F2(), b2 is Relation-like NAT -defined F1() . O -valued Function-like finite FinSequence-like FinSubsequence-like Element of (F1() . O) * : ex b3 being Relation-like NAT -defined FinTrees [: the carrier of F2(),F3():] -valued Function-like finite FinSequence-like FinSubsequence-like DTree-yielding FinSequence of FinTrees [: the carrier of F2(),F3():] st
( b2 = b3 & b1 ==> ( the carrier of F2(),F3(),([: the carrier of F2(),F3():],(FinTrees [: the carrier of F2(),F3():]),b3)) )
}
is set

(F1() . O) \/ { ([b1,H3(b1,b2)] -tree b2) where b1 is Element of the carrier of F2(), b2 is Relation-like NAT -defined F1() . O -valued Function-like finite FinSequence-like FinSubsequence-like Element of (F1() . O) * : ex b3 being Relation-like NAT -defined FinTrees [: the carrier of F2(),F3():] -valued Function-like finite FinSequence-like FinSubsequence-like DTree-yielding FinSequence of FinTrees [: the carrier of F2(),F3():] st
( b2 = b3 & b1 ==> ( the carrier of F2(),F3(),([: the carrier of F2(),F3():],(FinTrees [: the carrier of F2(),F3():]),b3)) )
}
is set

S is Element of the carrier of F2()

F5(S,(pr1 (roots nt)),(pr2 (roots nt))) is Element of F3()
[S,H3(S,nt)] is V15() Element of [: the carrier of F2(),F3():]
{S,F5(S,(pr1 (roots nt)),(pr2 (roots nt)))} is non empty finite set
{S} is non empty trivial finite V48(1) set
{{S,F5(S,(pr1 (roots nt)),(pr2 (roots nt)))},{S}} is non empty finite V45() set
[S,H3(S,nt)] -tree nt is Relation-like Function-like DecoratedTree-like set
PN . {} is set

rtO is Relation-like NAT -defined FinTrees [: the carrier of F2(),F3():] -valued Function-like finite FinSequence-like FinSubsequence-like DTree-yielding FinSequence of FinTrees [: the carrier of F2(),F3():]
([: the carrier of F2(),F3():],(FinTrees [: the carrier of F2(),F3():]),rtO) is Relation-like NAT -defined [: the carrier of F2(),F3():] -valued Function-like finite FinSequence-like FinSubsequence-like FinSequence of [: the carrier of F2(),F3():]
( the carrier of F2(),F3(),([: the carrier of F2(),F3():],(FinTrees [: the carrier of F2(),F3():]),rtO)) is Relation-like NAT -defined the carrier of F2() -valued Function-like finite FinSequence-like FinSubsequence-like FinSequence of the carrier of F2()
F5(S,{},{}) is Element of F3()
[S,F5(S,{},{})] is V15() Element of [: the carrier of F2(),F3():]
{S,F5(S,{},{})} is non empty finite set
{{S,F5(S,{},{})},{S}} is non empty finite V45() set
root-tree [S,F5(S,{},{})] is Relation-like [: the carrier of F2(),F3():] -valued Function-like DecoratedTree-like Element of FinTrees [: the carrier of F2(),F3():]
rtO is Relation-like NAT -defined FinTrees [: the carrier of F2(),F3():] -valued Function-like finite FinSequence-like FinSubsequence-like DTree-yielding FinSequence of FinTrees [: the carrier of F2(),F3():]
([: the carrier of F2(),F3():],(FinTrees [: the carrier of F2(),F3():]),rtO) is Relation-like NAT -defined [: the carrier of F2(),F3():] -valued Function-like finite FinSequence-like FinSubsequence-like FinSequence of [: the carrier of F2(),F3():]
( the carrier of F2(),F3(),([: the carrier of F2(),F3():],(FinTrees [: the carrier of F2(),F3():]),rtO)) is Relation-like NAT -defined the carrier of F2() -valued Function-like finite FinSequence-like FinSubsequence-like FinSequence of the carrier of F2()
O is set
F1() . O is set
PN is ext-real non negative V32() V33() V34() V35() V39() V40() finite V46() Element of NAT
F1() . PN is set
PN + 1 is non empty ext-real positive non negative V32() V33() V34() V35() V39() V40() finite V46() Element of NAT
F1() . (PN + 1) is set
O is Relation-like [: the carrier of F2(),F3():] -valued Function-like DecoratedTree-like Element of FinTrees [: the carrier of F2(),F3():]
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
(F1() . PN) * is functional non empty FinSequence-membered FinSequenceSet of F1() . PN
{ ([b1,H3(b1,b2)] -tree b2) where b1 is Element of the carrier of F2(), b2 is Relation-like NAT -defined F1() . PN -valued Function-like finite FinSequence-like FinSubsequence-like Element of (F1() . PN) * : ex b3 being Relation-like NAT -defined FinTrees [: the carrier of F2(),F3():] -valued Function-like finite FinSequence-like FinSubsequence-like DTree-yielding FinSequence of FinTrees [: the carrier of F2(),F3():] st
( b2 = b3 & b1 ==> ( the carrier of F2(),F3(),([: the carrier of F2(),F3():],(FinTrees [: the carrier of F2(),F3():]),b3)) )
}
is set

(F1() . PN) \/ { ([b1,H3(b1,b2)] -tree b2) where b1 is Element of the carrier of F2(), b2 is Relation-like NAT -defined F1() . PN -valued Function-like finite FinSequence-like FinSubsequence-like Element of (F1() . PN) * : ex b3 being Relation-like NAT -defined FinTrees [: the carrier of F2(),F3():] -valued Function-like finite FinSequence-like FinSubsequence-like DTree-yielding FinSequence of FinTrees [: the carrier of F2(),F3():] st
( b2 = b3 & b1 ==> ( the carrier of F2(),F3(),([: the carrier of F2(),F3():],(FinTrees [: the carrier of F2(),F3():]),b3)) )
}
is set

S is Element of the carrier of F2()

F5(S,(pr1 (roots nt)),(pr2 (roots nt))) is Element of F3()
[S,H3(S,nt)] is V15() Element of [: the carrier of F2(),F3():]
{S,F5(S,(pr1 (roots nt)),(pr2 (roots nt)))} is non empty finite set
{S} is non empty trivial finite V48(1) set
{{S,F5(S,(pr1 (roots nt)),(pr2 (roots nt)))},{S}} is non empty finite V45() set
[S,H3(S,nt)] -tree nt is Relation-like Function-like DecoratedTree-like set
x is Relation-like NAT -defined FinTrees [: the carrier of F2(),F3():] -valued Function-like finite FinSequence-like FinSubsequence-like DTree-yielding FinSequence of FinTrees [: the carrier of F2(),F3():]
([: the carrier of F2(),F3():],(FinTrees [: the carrier of F2(),F3():]),x) is Relation-like NAT -defined [: the carrier of F2(),F3():] -valued Function-like finite FinSequence-like FinSubsequence-like FinSequence of [: the carrier of F2(),F3():]
( the carrier of F2(),F3(),([: the carrier of F2(),F3():],(FinTrees [: the carrier of F2(),F3():]),x)) is Relation-like NAT -defined the carrier of F2() -valued Function-like finite FinSequence-like FinSubsequence-like FinSequence of the carrier of F2()
rtO is Relation-like NAT -defined FinTrees [: the carrier of F2(),F3():] -valued Function-like finite FinSequence-like FinSubsequence-like DTree-yielding FinSequence of FinTrees [: the carrier of F2(),F3():]

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

rng rtO is finite set
n is Relation-like [: the carrier of F2(),F3():] -valued Function-like DecoratedTree-like Element of FinTrees [: the carrier of F2(),F3():]
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
F1() . S is set
S is ext-real non negative V32() V33() V34() V35() V39() V40() finite V46() set
F1() . S is set
{ ([b1,F5(b1,(pr1 (roots b2)),(pr2 (roots b2)))] -tree b2) where b1 is Element of the carrier of F2(), b2 is Relation-like NAT -defined F1() . a1 -valued Function-like finite FinSequence-like FinSubsequence-like Element of (F1() . a1) * : ex b3 being Relation-like NAT -defined FinTrees [: the carrier of F2(),F3():] -valued Function-like finite FinSequence-like FinSubsequence-like DTree-yielding FinSequence of FinTrees [: the carrier of F2(),F3():] st
( b2 = b3 & b1 ==> ( the carrier of F2(),F3(),([: the carrier of F2(),F3():],(FinTrees [: the carrier of F2(),F3():]),b3)) )
}
is set

nt is ext-real non negative V32() V33() V34() V35() V39() V40() finite V46() Element of NAT
F1() . nt is set
nt + 1 is non empty ext-real positive non negative V32() V33() V34() V35() V39() V40() finite V46() Element of NAT
F1() . (nt + 1) is set
(F1() . nt) * is functional non empty FinSequence-membered FinSequenceSet of F1() . nt
{ ([b1,F5(b1,(pr1 (roots b2)),(pr2 (roots b2)))] -tree b2) where b1 is Element of the carrier of F2(), b2 is Relation-like NAT -defined F1() . nt -valued Function-like finite FinSequence-like FinSubsequence-like Element of (F1() . nt) * : ex b3 being Relation-like NAT -defined FinTrees [: the carrier of F2(),F3():] -valued Function-like finite FinSequence-like FinSubsequence-like DTree-yielding FinSequence of FinTrees [: the carrier of F2(),F3():] st
( b2 = b3 & b1 ==> ( the carrier of F2(),F3(),([: the carrier of F2(),F3():],(FinTrees [: the carrier of F2(),F3():]),b3)) )
}
is set

(F1() . nt) \/ H4(nt,F1() . 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
F1() . (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