:: BINTREE1 semantic presentation

REAL is V101() V102() V103() V107() set
NAT is V101() V102() V103() V104() V105() V106() V107() Element of bool REAL
bool REAL is non empty set
NAT is V101() V102() V103() V104() V105() V106() V107() set
bool NAT is non empty set
bool NAT is non empty set

1 is non empty V29() V84() V85() ext-real positive V89() V90() V101() V102() V103() V104() V105() V106() Element of NAT
{{},1} is non empty finite set
Trees is non empty constituted-Trees set
bool Trees is non empty set

the carrier of PeanoNat is non empty set
FinTrees the carrier of PeanoNat is non empty functional constituted-DTrees DTree-set of the carrier of PeanoNat
TS PeanoNat is non empty functional constituted-DTrees Element of bool ()
bool () is non empty set

bool is non empty set

bool is non empty set
COMPLEX is V101() V107() set
RAT is V101() V102() V103() V104() V107() set
INT is V101() V102() V103() V104() V105() V107() set
2 is non empty V29() V84() V85() ext-real positive V89() V90() V101() V102() V103() V104() V105() V106() Element of NAT
3 is non empty V29() V84() V85() ext-real positive V89() V90() V101() V102() V103() V104() V105() V106() Element of NAT

elementary_tree 2 is non empty finite Tree-like set

K5({},,<*1*>) is non empty finite set
Seg 1 is non empty finite V37(1) V101() V102() V103() V104() V105() V106() Element of bool NAT
{1} is non empty finite V101() V102() V103() V104() V105() V106() set
Seg 2 is non empty finite V37(2) V101() V102() V103() V104() V105() V106() Element of bool NAT
{1,2} is non empty finite V101() V102() V103() V104() V105() V106() set
K237(NAT) is non empty functional FinSequence-membered M19( NAT )

is non empty functional finite V34() Tree-like set
G is non empty set

s . {} is set
proj1 s is non empty Tree-like set

s . TV is Element of G
G is non empty set

(G,s) is Element of G
s . {} is set

K237(G) is non empty functional FinSequence-membered M19(G)
G is non empty set

(G,s) is Element of G
s . {} is set
(G,TV) is Element of G
TV . {} is set
<*(G,s),(G,TV)*> is non empty Relation-like NAT -defined G -valued Function-like finite V37(2) FinSequence-like FinSubsequence-like M20(G,K237(G))
K237(G) is non empty functional FinSequence-membered M19(G)

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

succ s is Element of bool G

{ (s ^ <*b1*>) where b1 is V29() V84() V85() ext-real V89() V90() V101() V102() V103() V104() V105() V106() Element of NAT : s ^ <*b1*> in G } is set
the Element of succ s is Element of succ s
NTV is V29() V84() V85() ext-real V89() V90() V101() V102() V103() V104() V105() V106() Element of NAT

Leaves is non empty finite Element of bool
bool is non empty finite V34() set

{(),(s ^ <*1*>)} is non empty functional finite V34() set

Leaves () is non empty finite Element of bool ()
bool () is non empty finite V34() set
succ s is finite Element of bool ()

{(),(s ^ <*1*>)} is non empty functional finite V34() set
{ (s ^ <*b1*>) where b1 is V29() V84() V85() ext-real V89() V90() V101() V102() V103() V104() V105() V106() Element of NAT : s ^ <*b1*> in elementary_tree 2 } is set
TV is set
f19 is V29() V84() V85() ext-real V89() V90() V101() V102() V103() V104() V105() V106() Element of NAT

f19 is V29() V84() V85() ext-real V89() V90() V101() V102() V103() V104() V105() V106() Element of NAT

f19 is V29() V84() V85() ext-real V89() V90() V101() V102() V103() V104() V105() V106() Element of NAT

len is V29() V84() V85() ext-real V89() V90() V101() V102() V103() V104() V105() V106() Element of NAT
() + () is V29() V84() V85() ext-real V89() V90() V101() V102() V103() V104() V105() V106() Element of NAT
len is V29() V84() V85() ext-real V89() V90() V101() V102() V103() V104() V105() V106() Element of NAT
() + () is V29() V84() V85() ext-real V89() V90() V101() V102() V103() V104() V105() V106() Element of NAT
len <*1*> is V29() V84() V85() ext-real V89() V90() V101() V102() V103() V104() V105() V106() Element of NAT
1 + () is V29() V84() V85() ext-real V89() V90() V101() V102() V103() V104() V105() V106() Element of NAT
1 + 1 is V29() V84() V85() ext-real V89() V90() V101() V102() V103() V104() V105() V106() Element of NAT
len <*1*> is V29() V84() V85() ext-real V89() V90() V101() V102() V103() V104() V105() V106() Element of NAT
len is V29() V84() V85() ext-real V89() V90() V101() V102() V103() V104() V105() V106() Element of NAT
() + () is V29() V84() V85() ext-real V89() V90() V101() V102() V103() V104() V105() V106() Element of NAT
len <*1*> is V29() V84() V85() ext-real V89() V90() V101() V102() V103() V104() V105() V106() Element of NAT
len is V29() V84() V85() ext-real V89() V90() V101() V102() V103() V104() V105() V106() Element of NAT
() + () is V29() V84() V85() ext-real V89() V90() V101() V102() V103() V104() V105() V106() Element of NAT
G is non empty set
the non empty finite Tree-like () set is non empty finite Tree-like () set
[: the non empty finite Tree-like () set ,G:] is non empty Relation-like set
bool [: the non empty finite Tree-like () set ,G:] is non empty set
the Relation-like the non empty finite Tree-like () set -defined G -valued Function-like quasi_total finite DecoratedTree-like Element of bool [: the non empty finite Tree-like () set ,G:] is Relation-like the non empty finite Tree-like () set -defined G -valued Function-like quasi_total finite DecoratedTree-like Element of bool [: the non empty finite Tree-like () set ,G:]

proj1 NTV is non empty Tree-like set

G is non empty Tree-like set

Leaves G is Element of bool G
bool G is non empty set
Leaves G is Element of bool G
bool G is non empty set
<*2*> . 1 is set
{ (s ^ <*b1*>) where b1 is V29() V84() V85() ext-real V89() V90() V101() V102() V103() V104() V105() V106() Element of NAT : s ^ <*b1*> in G } is set
succ s is Element of bool G

{(),(s ^ <*1*>)} is non empty functional finite V34() set
Leaves G is Element of bool G
bool G is non empty set
G is non empty Tree-like set
s is non empty Tree-like set
tree (G,s) is non empty Tree-like set
Leaves (tree (G,s)) is Element of bool (tree (G,s))
bool (tree (G,s)) is non empty set
Leaves G is Element of bool G
bool G is non empty set
Leaves s is Element of bool s
bool s is non empty set

nt is V29() V84() V85() ext-real V89() V90() V101() V102() V103() V104() V105() V106() Element of NAT

nt is V29() V84() V85() ext-real V89() V90() V101() V102() V103() V104() V105() V106() Element of NAT

nt is V29() V84() V85() ext-real V89() V90() V101() V102() V103() V104() V105() V106() Element of NAT

nt is V29() V84() V85() ext-real V89() V90() V101() V102() V103() V104() V105() V106() Element of NAT

G is non empty Tree-like set
s is non empty Tree-like set
tree (G,s) is non empty Tree-like set

succ TV is Element of bool (tree (G,s))
bool (tree (G,s)) is non empty set

{(TV ^ ),(TV ^ <*1*>)} is non empty functional finite V34() set

{ (TV ^ <*b1*>) where b1 is V29() V84() V85() ext-real V89() V90() V101() V102() V103() V104() V105() V106() Element of NAT : TV ^ <*b1*> in tree (G,s) } is set

f19 is set
nt is V29() V84() V85() ext-real V89() V90() V101() V102() V103() V104() V105() V106() Element of NAT

tl . 1 is set

succ f19 is Element of bool G
bool G is non empty set
{ (f19 ^ <*b1*>) where b1 is V29() V84() V85() ext-real V89() V90() V101() V102() V103() V104() V105() V106() Element of NAT : f19 ^ <*b1*> in G } is set
tl is V29() V84() V85() ext-real V89() V90() V101() V102() V103() V104() V105() V106() Element of NAT

tr is V29() V84() V85() ext-real V89() V90() V101() V102() V103() V104() V105() V106() Element of NAT

succ f19 is Element of bool s
bool s is non empty set

{ (f19 ^ <*b1*>) where b1 is V29() V84() V85() ext-real V89() V90() V101() V102() V103() V104() V105() V106() Element of NAT : f19 ^ <*b1*> in s } is set
tl is V29() V84() V85() ext-real V89() V90() V101() V102() V103() V104() V105() V106() Element of NAT

tr is V29() V84() V85() ext-real V89() V90() V101() V102() V103() V104() V105() V106() Element of NAT

G is non empty Tree-like set
s is non empty Tree-like set
tree (G,s) is non empty Tree-like set

Leaves (tree (G,s)) is Element of bool (tree (G,s))
bool (tree (G,s)) is non empty set
succ NTV is Element of bool (tree (G,s))

{(NTV ^ ),(NTV ^ <*1*>)} is non empty functional finite V34() set

Leaves s is Element of bool s
bool s is non empty set
succ NTV is Element of bool (tree (G,s))

{(NTV ^ ),(NTV ^ <*1*>)} is non empty functional finite V34() set

Leaves s is Element of bool s
bool s is non empty set
succ nt is Element of bool s

{(nt ^ ),(nt ^ <*1*>)} is non empty functional finite V34() set
tl is set
succ NTV is Element of bool (tree (G,s))
{ (NTV ^ <*b1*>) where b1 is V29() V84() V85() ext-real V89() V90() V101() V102() V103() V104() V105() V106() Element of NAT : NTV ^ <*b1*> in tree (G,s) } is set
tr is V29() V84() V85() ext-real V89() V90() V101() V102() V103() V104() V105() V106() Element of NAT

{(NTV ^ ),(NTV ^ <*1*>)} is non empty functional finite V34() set

Leaves s is Element of bool s
bool s is non empty set
succ NTV is Element of bool (tree (G,s))

{(NTV ^ ),(NTV ^ <*1*>)} is non empty functional finite V34() set
succ NTV is Element of bool (tree (G,s))

{(NTV ^ ),(NTV ^ <*1*>)} is non empty functional finite V34() set

Leaves G is Element of bool G
bool G is non empty set

Leaves G is Element of bool G
bool G is non empty set
succ nt is Element of bool G

{(nt ^ ),(nt ^ <*1*>)} is non empty functional finite V34() set
tl is set
{ (NTV ^ <*b1*>) where b1 is V29() V84() V85() ext-real V89() V90() V101() V102() V103() V104() V105() V106() Element of NAT : NTV ^ <*b1*> in tree (G,s) } is set
tr is V29() V84() V85() ext-real V89() V90() V101() V102() V103() V104() V105() V106() Element of NAT

Leaves G is Element of bool G
bool G is non empty set

Leaves G is Element of bool G
bool G is non empty set

succ f19 is Element of bool (tree (G,s))

{(( ^ NTV) ^ ),(( ^ NTV) ^ <*1*>)} is non empty functional finite V34() set
{ (f19 ^ <*b1*>) where b1 is V29() V84() V85() ext-real V89() V90() V101() V102() V103() V104() V105() V106() Element of NAT : f19 ^ <*b1*> in tree (G,s) } is set
nt is set
succ NTV is Element of bool G
{ (NTV ^ <*b1*>) where b1 is V29() V84() V85() ext-real V89() V90() V101() V102() V103() V104() V105() V106() Element of NAT : NTV ^ <*b1*> in G } is set
tl is V29() V84() V85() ext-real V89() V90() V101() V102() V103() V104() V105() V106() Element of NAT

{(NTV ^ ),(NTV ^ <*1*>)} is non empty functional finite V34() set

Leaves s is Element of bool s
bool s is non empty set

succ f19 is Element of bool (tree (G,s))

{((<*1*> ^ NTV) ^ ),((<*1*> ^ NTV) ^ <*1*>)} is non empty functional finite V34() set
{ (f19 ^ <*b1*>) where b1 is V29() V84() V85() ext-real V89() V90() V101() V102() V103() V104() V105() V106() Element of NAT : f19 ^ <*b1*> in tree (G,s) } is set
nt is set
succ NTV is Element of bool s
{ (NTV ^ <*b1*>) where b1 is V29() V84() V85() ext-real V89() V90() V101() V102() V103() V104() V105() V106() Element of NAT : NTV ^ <*b1*> in s } is set
tl is V29() V84() V85() ext-real V89() V90() V101() V102() V103() V104() V105() V106() Element of NAT

{(NTV ^ ),(NTV ^ <*1*>)} is non empty functional finite V34() set

TV is set

proj1 G is non empty Tree-like set
proj1 s is non empty Tree-like set
tree ((),()) is non empty Tree-like set
proj1 (TV -tree (G,s)) is non empty Tree-like set
G is non empty set
s is Element of G

proj1 TV is non empty finite Tree-like set

proj1 NTV is non empty finite Tree-like set
proj2 <*TV,NTV*> is non empty finite set

1 + 1 is V29() V84() V85() ext-real V89() V90() V101() V102() V103() V104() V105() V106() Element of NAT
proj2 (<*TV*> ^ <*NTV*>) is non empty finite set
proj2 <*TV*> is non empty finite set
proj2 <*NTV*> is non empty finite set
() \/ (proj2 <*NTV*>) is non empty finite set
{TV} is non empty functional finite V34() set
{TV} \/ (proj2 <*NTV*>) is non empty finite set
{NTV} is non empty functional finite V34() set
{TV} \/ {NTV} is non empty finite V34() set
{TV,NTV} is non empty functional finite V34() set
nt is set

proj1 (s -tree (TV,NTV)) is non empty Tree-like set
{0,1} is non empty finite V101() V102() V103() V104() V105() V106() set
G is non empty set

TV is Element of G

K237(G) is non empty functional FinSequence-membered M19(G)

1 + 1 is V29() V84() V85() ext-real V89() V90() V101() V102() V103() V104() V105() V106() Element of NAT
[:G,(G *):] is non empty Relation-like set
bool [:G,(G *):] is non empty set
s is Element of G

[s,NTV] is V1() set
{[s,NTV]} is non empty Relation-like Function-like finite set
f19 is Relation-like G -defined G * -valued Element of bool [:G,(G *):]
DTConstrStr(# G,f19 #) is non empty strict DTConstrStr
nt is non empty strict DTConstrStr
the carrier of nt is non empty set
rtl is Element of the carrier of nt

tr is Element of the carrier of nt
[rtl,rtr] is V1() set
[0,NTV] is V1() set

g is Element of the carrier of nt
ff1 is Element of the carrier of nt
<*g,ff1*> is non empty Relation-like NAT -defined the carrier of nt -valued Function-like finite V37(2) FinSequence-like FinSubsequence-like M20( the carrier of nt,K237( the carrier of nt))
K237( the carrier of nt) is non empty functional FinSequence-membered M19( the carrier of nt)

[1,rtl] is V1() set
{ b1 where b1 is Element of the carrier of nt : for b2 being Relation-like NAT -defined Function-like finite FinSequence-like FinSubsequence-like set holds not b1 ==> b2 } is set
Terminals nt is set
tl is Element of the carrier of nt
[tl,NTV] is V1() set
{ b1 where b1 is Element of the carrier of nt : ex b2 being Relation-like NAT -defined Function-like finite FinSequence-like FinSubsequence-like set st b1 ==> b2 } is set
NonTerminals nt is set
TS nt is functional constituted-DTrees Element of bool (FinTrees the carrier of nt)
FinTrees the carrier of nt is non empty functional constituted-DTrees DTree-set of the carrier of nt
bool (FinTrees the carrier of nt) is non empty set
rtl is non empty set

g is Element of rtl
<*g*> is non empty Relation-like NAT -defined rtl -valued Function-like finite V37(1) FinSequence-like FinSubsequence-like M20(rtl,K237(rtl))
K237(rtl) is non empty functional FinSequence-membered M19(rtl)
<*g*> ^ <*g*> is non empty Relation-like NAT -defined rtl -valued Function-like finite V37(1 + 1) FinSequence-like FinSubsequence-like M20(rtl,K237(rtl))

() . {} is set
<*(() . {}),(() . {})*> is non empty Relation-like NAT -defined Function-like finite V37(2) FinSequence-like FinSubsequence-like set
rtr is Element of the carrier of nt
ff2 is Element of the carrier of nt

[rtr,ff2] is V1() set
() . {} is set

F1() is non empty set
G is non empty strict DTConstrStr
the carrier of G is non empty set
s is Element of the carrier of G

[s,TV] is V1() set
the Rules of G is Relation-like the carrier of G -defined K237( the carrier of G) -valued Element of bool [: the carrier of G,K237( the carrier of G):]
K237( the carrier of G) is non empty functional FinSequence-membered M19( the carrier of G)
[: the carrier of G,K237( the carrier of G):] is non empty Relation-like set
bool [: the carrier of G,K237( the carrier of G):] is non empty set
the carrier of G * is non empty functional FinSequence-membered set

NTV . 1 is set
NTV . 2 is set
<*(NTV . 1),(NTV . 2)*> is non empty Relation-like NAT -defined Function-like finite V37(2) FinSequence-like FinSubsequence-like set
rng NTV is finite Element of bool the carrier of G
bool the carrier of G is non empty set

<*(NTV . 1)*> ^ <*(NTV . 2)*> is non empty Relation-like NAT -defined Function-like finite V37(1 + 1) FinSequence-like FinSubsequence-like set
1 + 1 is V29() V84() V85() ext-real V89() V90() V101() V102() V103() V104() V105() V106() Element of NAT
proj2 (<*(NTV . 1)*> ^ <*(NTV . 2)*>) is non empty finite set
proj2 <*(NTV . 1)*> is non empty finite set
proj2 <*(NTV . 2)*> is non empty finite set
(proj2 <*(NTV . 1)*>) \/ (proj2 <*(NTV . 2)*>) is non empty finite set
{(NTV . 1)} is non empty finite set
{(NTV . 1)} \/ (proj2 <*(NTV . 2)*>) is non empty finite set
{(NTV . 2)} is non empty finite set
{(NTV . 1)} \/ {(NTV . 2)} is non empty finite set
{(NTV . 1),(NTV . 2)} is non empty finite set
f19 is Element of the carrier of G
nt is Element of the carrier of G
tl is Element of the carrier of G
tr is Element of the carrier of G
<*tl,tr*> is non empty Relation-like NAT -defined the carrier of G -valued Function-like finite V37(2) FinSequence-like FinSubsequence-like M20( the carrier of G,K237( the carrier of G))
TV is Element of the carrier of G
NTV is Element of the carrier of G
<*TV,NTV*> is non empty Relation-like NAT -defined the carrier of G -valued Function-like finite V37(2) FinSequence-like FinSubsequence-like M20( the carrier of G,K237( the carrier of G))

f19 . 1 is set
f19 . 2 is set
s is Element of the carrier of G

the carrier of G is non empty set
FinTrees the carrier of G is non empty functional constituted-DTrees DTree-set of the carrier of G
TS G is non empty functional constituted-DTrees Element of bool (FinTrees the carrier of G)
bool (FinTrees the carrier of G) is non empty set
NonTerminals G is non empty Element of bool the carrier of G
bool the carrier of G is non empty set

dom s is finite V101() V102() V103() V104() V105() V106() Element of bool NAT

rng s is functional finite constituted-DTrees Element of bool (FinTrees the carrier of G)
TV is Element of the carrier of G

NTV is Element of the carrier of G
f19 is Element of the carrier of G
<*NTV,f19*> is non empty Relation-like NAT -defined the carrier of G -valued Function-like finite V37(2) FinSequence-like FinSubsequence-like M20( the carrier of G,K237( the carrier of G))
K237( the carrier of G) is non empty functional FinSequence-membered M19( the carrier of G)
{ b1 where b1 is Element of the carrier of G : ex b2 being Relation-like NAT -defined Function-like finite FinSequence-like FinSubsequence-like set st b1 ==> b2 } is set
len <*NTV,f19*> is V29() V84() V85() ext-real V89() V90() V101() V102() V103() V104() V105() V106() Element of NAT
dom <*NTV,f19*> is non empty finite V101() V102() V103() V104() V105() V106() Element of bool NAT
<*NTV,f19*> . 1 is set

nt . {} is set
<*NTV,f19*> . 2 is set

tl . {} is set

( the carrier of G,tr) is Element of the carrier of G
tr . {} is set

( the carrier of G,rtl) is Element of the carrier of G
rtl . {} is set
<*( the carrier of G,tr),( the carrier of G,rtl)*> is non empty Relation-like NAT -defined the carrier of G -valued Function-like finite V37(2) FinSequence-like FinSubsequence-like M20( the carrier of G,K237( the carrier of G))
TV -tree (tr,rtl) is Relation-like the carrier of G -valued Function-like DecoratedTree-like set
Seg (len <*NTV,f19*>) is finite V37( len <*NTV,f19*>) V101() V102() V103() V104() V105() V106() Element of bool NAT
len s is V29() V84() V85() ext-real V89() V90() V101() V102() V103() V104() V105() V106() Element of NAT
Seg (len s) is finite V37( len s) V101() V102() V103() V104() V105() V106() Element of bool NAT

K237((TS G)) is non empty functional FinSequence-membered M19( TS G)
F1() is non empty with_terminals with_nonterminals () DTConstrStr
the carrier of F1() is non empty set
Terminals F1() is non empty Element of bool the carrier of F1()
bool the carrier of F1() is non empty set
NonTerminals F1() is non empty Element of bool the carrier of F1()
FinTrees the carrier of F1() is non empty functional constituted-DTrees DTree-set of the carrier of F1()
TS F1() is non empty functional constituted-DTrees Element of bool (FinTrees the carrier of F1())
bool (FinTrees the carrier of F1()) is non empty set
G is Element of the carrier of F1()

rng s is functional finite constituted-DTrees Element of bool (FinTrees the carrier of F1())
G -tree s is Relation-like the carrier of F1() -valued Function-like DecoratedTree-like Element of FinTrees the carrier of F1()

TV is Relation-like the carrier of F1() -valued Function-like DecoratedTree-like Element of TS F1()
( the carrier of F1(),TV) is Element of the carrier of F1()
TV . {} is set
NTV is Relation-like the carrier of F1() -valued Function-like DecoratedTree-like Element of TS F1()
( the carrier of F1(),NTV) is Element of the carrier of F1()
NTV . {} is set
<*( the carrier of F1(),TV),( the carrier of F1(),NTV)*> is non empty Relation-like NAT -defined the carrier of F1() -valued Function-like finite V37(2) FinSequence-like FinSubsequence-like M20( the carrier of F1(),K237( the carrier of F1()))
K237( the carrier of F1()) is non empty functional FinSequence-membered M19( the carrier of F1())
G -tree (TV,NTV) is Relation-like the carrier of F1() -valued Function-like DecoratedTree-like set
G is Element of the carrier of F1()
root-tree G is Relation-like the carrier of F1() -valued Function-like DecoratedTree-like Element of FinTrees the carrier of F1()
G is Relation-like the carrier of F1() -valued Function-like DecoratedTree-like Element of TS F1()
F2() is non empty set

TS F1() is non empty functional constituted-DTrees Element of bool (FinTrees the carrier of F1())
the carrier of F1() is non empty set
FinTrees the carrier of F1() is non empty functional constituted-DTrees DTree-set of the carrier of F1()
bool (FinTrees the carrier of F1()) is non empty set
[:(TS F1()),F2():] is non empty Relation-like set
bool [:(TS F1()),F2():] is non empty set
Terminals F1() is non empty Element of bool the carrier of F1()
bool the carrier of F1() is non empty set
NonTerminals F1() is non empty Element of bool the carrier of F1()
G is Relation-like TS F1() -defined F2() -valued Function-like quasi_total Element of bool [:(TS F1()),F2():]
s is Element of Terminals F1()

G . () is Element of F2()
F3(s) is Element of F2()
s is Element of NonTerminals F1()
TV is Relation-like the carrier of F1() -valued Function-like DecoratedTree-like Element of TS F1()
( the carrier of F1(),TV) is Element of the carrier of F1()
TV . {} is set
NTV is Relation-like the carrier of F1() -valued Function-like DecoratedTree-like Element of TS F1()
( the carrier of F1(),NTV) is Element of the carrier of F1()
NTV . {} is set
G . TV is Element of F2()
G . NTV is Element of F2()
s -tree (TV,NTV) is Relation-like the carrier of F1() -valued Function-like DecoratedTree-like set
G . (s -tree (TV,NTV)) is set
f19 is Element of the carrier of F1()
nt is Element of the carrier of F1()
<*f19,nt*> is non empty Relation-like NAT -defined the carrier of F1() -valued Function-like finite V37(2) FinSequence-like FinSubsequence-like M20( the carrier of F1(),K237( the carrier of F1()))
K237( the carrier of F1()) is non empty functional FinSequence-membered M19( the carrier of F1())
<*TV,NTV*> is non empty Relation-like NAT -defined TS F1() -valued Function-like finite V37(2) FinSequence-like FinSubsequence-like DTree-yielding M20( TS F1(),K237((TS F1())))
K237((TS F1())) is non empty functional FinSequence-membered M19( TS F1())

rtl is Element of F2()
rtr is Element of F2()
F4(s,f19,nt,rtl,rtr) is Element of F2()
dom tr is finite V101() V102() V103() V104() V105() V106() Element of bool NAT
<*rtl,rtr*> is non empty Relation-like NAT -defined F2() -valued Function-like finite V37(2) FinSequence-like FinSubsequence-like M20(F2(),K237(F2()))
K237(F2()) is non empty functional FinSequence-membered M19(F2())

dom g is finite V101() V102() V103() V104() V105() V106() Element of bool NAT

dom G is functional constituted-DTrees Element of bool (TS F1())
bool (TS F1()) is non empty set
ff1 is set

ff1 is set
g . ff1 is set

G . (tr . ff1) is set

tl . 2 is set
tl . 1 is set
ff1 is V29() V84() V85() ext-real V89() V90() V101() V102() V103() V104() V105() V106() Element of NAT
len tr is V29() V84() V85() ext-real V89() V90() V101() V102() V103() V104() V105() V106() Element of NAT
Seg (len tr) is finite V37( len tr) V101() V102() V103() V104() V105() V106() Element of bool NAT

tl . ff1 is set

tl . ff1 is set
dom tl is finite V101() V102() V103() V104() V105() V106() Element of bool NAT

s -tree tr is Relation-like the carrier of F1() -valued Function-like DecoratedTree-like Element of FinTrees the carrier of F1()
G . (s -tree tr) is set
g . 1 is set
g . 2 is set
F4(s,(tl . 1),(tl . 2),(g . 1),(g . 2)) is Element of F2()

TS F1() is non empty functional constituted-DTrees Element of bool (FinTrees the carrier of F1())
the carrier of F1() is non empty set
FinTrees the carrier of F1() is non empty functional constituted-DTrees DTree-set of the carrier of F1()
bool (FinTrees the carrier of F1()) is non empty set
F2() is non empty set
[:(TS F1()),F2():] is non empty Relation-like set
bool [:(TS F1()),F2():] is non empty set
Terminals F1() is non empty Element of bool the carrier of F1()
bool the carrier of F1() is non empty set
F3() is Relation-like TS F1() -defined F2() -valued Function-like quasi_total Element of bool [:(TS F1()),F2():]
NonTerminals F1() is non empty Element of bool the carrier of F1()
F4() is Relation-like TS F1() -defined F2() -valued Function-like quasi_total Element of bool [:(TS F1()),F2():]
G is Element of the carrier of F1()
root-tree G is Relation-like the carrier of F1() -valued Function-like DecoratedTree-like Element of FinTrees the carrier of F1()
F4() . () is set
F5(G) is Element of F2()

F4() * s is Relation-like NAT -defined F2() -valued Function-like finite FinSequence-like FinSubsequence-like M20(F2(),K237(F2()))
K237(F2()) is non empty functional FinSequence-membered M19(F2())
G is Element of the carrier of F1()

G -tree s is Relation-like the carrier of F1() -valued Function-like DecoratedTree-like Element of FinTrees the carrier of F1()
rng s is functional finite constituted-DTrees Element of bool (FinTrees the carrier of F1())
f19 is Relation-like the carrier of F1() -valued Function-like DecoratedTree-like Element of TS F1()
( the carrier of F1(),f19) is Element of the carrier of F1()
f19 . {} is set
nt is Relation-like the carrier of F1() -valued Function-like DecoratedTree-like Element of TS F1()
( the carrier of F1(),nt) is Element of the carrier of F1()
nt . {} is set
<*( the carrier of F1(),f19),( the carrier of F1(),nt)*> is non empty Relation-like NAT -defined the carrier of F1() -valued Function-like finite V37(2) FinSequence-like FinSubsequence-like M20( the carrier of F1(),K237( the carrier of F1()))
K237( the carrier of F1()) is non empty functional FinSequence-membered M19( the carrier of F1())
G -tree (f19,nt) is Relation-like the carrier of F1() -valued Function-like DecoratedTree-like set
F4() . nt is Element of F2()
dom s is finite V101() V102() V103() V104() V105() V106() Element of bool NAT
(F4() * s) . 2 is set
tl is Element of F2()
F4() . f19 is Element of F2()
(F4() * s) . 1 is set
tr is Element of F2()
() . 1 is set
() . 2 is set
F4() . (G -tree s) is set
F6(G,(() . 1),(() . 2),((F4() * s) . 1),((F4() * s) . 2)) is Element of F2()
G is Element of the carrier of F1()
root-tree G is Relation-like the carrier of F1() -valued Function-like DecoratedTree-like Element of FinTrees the carrier of F1()
F3() . () is set
F5(G) is Element of F2()

F3() * s is Relation-like NAT -defined F2() -valued Function-like finite FinSequence-like FinSubsequence-like M20(F2(),K237(F2()))
G is Element of the carrier of F1()

G -tree s is Relation-like the carrier of F1() -valued Function-like DecoratedTree-like Element of FinTrees the carrier of F1()
rng s is functional finite constituted-DTrees Element of bool (FinTrees the carrier of F1())
f19 is Relation-like the carrier of F1() -valued Function-like DecoratedTree-like Element of TS F1()
( the carrier of F1(),f19) is Element of the carrier of F1()
f19 . {} is set
nt is Relation-like the carrier of F1() -valued Function-like DecoratedTree-like Element of TS F1()
( the carrier of F1(),nt) is Element of the carrier of F1()
nt . {} is set
<*( the carrier of F1(),f19),( the carrier of F1(),nt)*> is non empty Relation-like NAT -defined the carrier of F1() -valued Function-like finite V37(2) FinSequence-like FinSubsequence-like M20( the carrier of F1(),K237( the carrier of F1()))
G -tree (f19,nt) is Relation-like the carrier of F1() -valued Function-like DecoratedTree-like set
F3() . nt is Element of F2()
dom s is finite V101() V102() V103() V104() V105() V106() Element of bool NAT
(F3() * s) . 2 is set
tl is Element of F2()
F3() . f19 is Element of F2()
(F3() * s) . 1 is set
tr is Element of F2()
() . 1 is set
() . 2 is set
F3() . (G -tree s) is set
F6(G,(() . 1),(() . 2),((F3() * s) . 1),((F3() * s) . 2)) is Element of F2()
G is non empty set
s is non empty set
TV is non empty set
NTV is Element of G
f19 is Element of s
nt is Element of TV
[NTV,f19,nt] is V1() V2() set
[NTV,f19] is V1() set
[[NTV,f19],nt] is V1() set
[:G,s,TV:] is non empty set
F3() is non empty set

TS F1() is non empty functional constituted-DTrees Element of bool (FinTrees the carrier of F1())
the carrier of F1() is non empty set
FinTrees the carrier of F1() is non empty functional constituted-DTrees DTree-set of the carrier of F1()
bool (FinTrees the carrier of F1()) is non empty set
F2() is non empty set
Funcs (F2(),F3()) is non empty FUNCTION_DOMAIN of F2(),F3()
[:(TS F1()),(Funcs (F2(),F3())):] is non empty Relation-like set
bool [:(TS F1()),(Funcs (F2(),F3())):] is non empty set
Terminals F1() is non empty Element of bool the carrier of F1()
bool the carrier of F1() is non empty set
[:F2(),F3():] is non empty Relation-like set
bool [:F2(),F3():] is non empty set
NonTerminals F1() is non empty Element of bool the carrier of F1()
s is Element of Terminals F1()
TV is Relation-like F2() -defined F3() -valued Function-like quasi_total Element of bool [:F2(),F3():]
dom TV is Element of bool F2()
bool F2() is non empty set
rng TV is Element of bool F3()
bool F3() is non empty set
G is non empty set
NTV is Element of G
f19 is Element of G
nt is Relation-like F2() -defined F3() -valued Function-like quasi_total Element of bool [:F2(),F3():]
tl is Element of F2()
nt . tl is Element of F3()
F4(s,tl) is Element of F3()
[:(Terminals F1()),G:] is non empty Relation-like set
bool [:(Terminals F1()),G:] is non empty set

TV is Element of NonTerminals F1()
NTV is Element of G
f19 is Element of G
nt is Relation-like F2() -defined F3() -valued Function-like quasi_total Element of bool [:F2(),F3():]
dom nt is Element of bool F2()
rng nt is Element of bool F3()
tl is Element of G
tr is Element of G
rtr is Relation-like F2() -defined F3() -valued Function-like quasi_total Element of bool [:F2(),F3():]
rtl is Element of F2()
rtr . rtl is Element of F3()
F5(TV,NTV,f19,rtl) is Element of F3()
[:(NonTerminals F1()),G,G:] is non empty set
[:[:(NonTerminals F1()),G,G:],G:] is non empty Relation-like set
bool [:[:(NonTerminals F1()),G,G:],G:] is non empty set
TV is Relation-like [:(NonTerminals F1()),G,G:] -defined G -valued Function-like quasi_total Element of bool [:[:(NonTerminals F1()),G,G:],G:]
[:(TS F1()),G:] is non empty Relation-like set
bool [:(TS F1()),G:] is non empty set
NTV is Relation-like TS F1() -defined G -valued Function-like quasi_total Element of bool [:(TS F1()),G:]
f19 is Relation-like TS F1() -defined Funcs (F2(),F3()) -valued Function-like quasi_total Element of bool [:(TS F1()),(Funcs (F2(),F3())):]
nt is Element of Terminals F1()
s . nt is Element of G

proj1 tl is set
proj2 tl is set
tr is Relation-like F2() -defined F3() -valued Function-like quasi_total Element of bool [:F2(),F3():]
rtl is Relation-like F2() -defined F3() -valued Function-like quasi_total Element of bool [:F2(),F3():]
root-tree nt is Relation-like the carrier of F1() -valued Function-like DecoratedTree-like Element of TS F1()
f19 . () is Element of Funcs (F2(),F3())
rtr is Element of F2()
rtl . rtr is Element of F3()
F4(nt,rtr) is Element of F3()
nt is Element of NonTerminals F1()
tl is Relation-like the carrier of F1() -valued Function-like DecoratedTree-like Element of TS F1()
( the carrier of F1(),tl) is Element of the carrier of F1()
tl . {} is set
tr is Relation-like the carrier of F1() -valued Function-like DecoratedTree-like Element of TS F1()
( the carrier of F1(),tr) is Element of the carrier of F1()
tr . {} is set
nt -tree (tl,tr) is Relation-like the carrier of F1() -valued Function-like DecoratedTree-like set
f19 . (nt -tree (tl,tr)) is set
f19 . tl is Element of Funcs (F2(),F3())
f19 . tr is Element of Funcs (F2(),F3())
rtl is Element of the carrier of F1()
rtr is Element of the carrier of F1()
<*rtl,rtr*> is non empty Relation-like NAT -defined the carrier of F1() -valued Function-like finite V37(2) FinSequence-like FinSubsequence-like M20( the carrier of F1(),K237( the carrier of F1()))
K237( the carrier of F1()) is non empty functional FinSequence-membered M19( the carrier of F1())
NTV . tr is Element of G

proj1 ff1 is set
proj2 ff1 is set
NTV . tl is Element of G

proj1 ff2 is set
proj2 ff2 is set
((NonTerminals F1()),G,G,nt,(NTV . tl),(NTV . tr)) is V1() V2() Element of [:(NonTerminals F1()),G,G:]
[nt,(NTV . tl)] is V1() set
[[nt,(NTV . tl)],(NTV . tr)] is V1() set
TV . ((NonTerminals F1()),G,G,nt,(NTV . tl),(NTV . tr)) is Element of G
ff1 is Relation-like F2() -defined F3() -valued Function-like quasi_total Element of bool [:F2(),F3():]
g is Relation-like F2() -defined F3() -valued Function-like quasi_total Element of bool [:F2(),F3():]
((NonTerminals F1()),(bool [:F2(),F3():]),(bool [:F2(),F3():]),nt,ff1,g) is V1() V2() Element of [:(NonTerminals F1()),(bool [:F2(),F3():]),(bool [:F2(),F3():]):]
[:(NonTerminals F1()),(bool [:F2(),F3():]),(bool [:F2(),F3():]):] is non empty set
[nt,ff1] is V1() set
[[nt,ff1],g] is V1() set
TV . ((NonTerminals F1()),(bool [:F2(),F3():]),(bool [:F2(),F3():]),nt,ff1,g) is set

proj1 ff2 is set
proj2 ff2 is set
xl is Relation-like F2() -defined F3() -valued Function-like quasi_total Element of bool [:F2(),F3():]
xr is Element of F2()
xl . xr is Element of F3()
F5(nt,ff1,g,xr) is Element of F3()

TS F1() is non empty functional constituted-DTrees Element of bool (FinTrees the carrier of F1())
the carrier of F1() is non empty set
FinTrees the carrier of F1() is non empty functional constituted-DTrees DTree-set of the carrier of F1()
bool (FinTrees the carrier of F1()) is non empty set
F2() is non empty set
F3() is non empty set
Funcs (F2(),F3()) is non empty FUNCTION_DOMAIN of F2(),F3()
[:(TS F1()),(Funcs (F2(),F3())):] is non empty Relation-like set
bool [:(TS F1()),(Funcs (F2(),F3())):] is non empty set
Terminals F1() is non empty Element of bool the carrier of F1()
bool the carrier of F1() is non empty set
[:F2(),F3():] is non empty Relation-like set
bool [:F2(),F3():] is non empty set
F4() is Relation-like TS F1() -defined Funcs (F2(),F3()) -valued Function-like quasi_total Element of bool [:(TS F1()),(Funcs (F2(),F3())):]
NonTerminals F1() is non empty Element of bool the carrier of F1()
F5() is Relation-like TS F1() -defined Funcs (F2(),F3()) -valued Function-like quasi_total Element of bool [:(TS F1()),(Funcs (F2(),F3())):]
G is non empty set
[:(TS F1()),G:] is non empty Relation-like set
bool [:(TS F1()),G:] is non empty set
TV is Element of Terminals F1()
NTV is Relation-like F2() -defined F3() -valued Function-like quasi_total Element of bool [:F2(),F3():]
dom NTV is Element of bool F2()
bool F2() is non empty set
rng NTV is Element of bool F3()
bool F3() is non empty set
f19 is Element of G
nt is Element of G
tl is Relation-like F2() -defined F3() -valued Function-like quasi_total Element of bool [:F2(),F3():]
tr is Element of F2()
tl . tr is Element of F3()
F6(TV,tr) is Element of F3()
[:(Terminals F1()),G:] is non empty Relation-like set
bool [:(Terminals F1()),G:] is non empty set

NTV is Element of NonTerminals F1()
f19 is Element of G
nt is Element of G
tl is Relation-like F2() -defined F3() -valued Function-like quasi_total Element of bool [:F2(),F3():]
dom tl is Element of bool F2()
rng tl is Element of bool F3()
tr is Element of G
rtl is Element of G
g is Relation-like F2() -defined F3() -valued Function-like quasi_total Element of bool [:F2(),F3():]
rtr is Element of F2()
g . rtr is Element of F3()
F7(NTV,f19,nt,rtr) is Element of F3()
[:(NonTerminals F1()),G,G:] is non empty set
[:[:(NonTerminals F1()),G,G:],G:] is non empty Relation-like set
bool [:[:(NonTerminals F1()),G,G:],G:] is non empty set
NTV is Relation-like [:(NonTerminals F1()),G,G:] -defined G -valued Function-like quasi_total Element of bool [:[:(NonTerminals F1()),G,G:],G:]
f19 is Element of Terminals F1()
TV . f19 is Element of G

proj1 nt is set
proj2 nt is set
root-tree f19 is Relation-like the carrier of F1() -valued Function-like DecoratedTree-like Element of TS F1()
F5() . (root-tree f19) is Element of Funcs (F2(),F3())
tr is Relation-like F2() -defined F3() -valued Function-like quasi_total Element of bool [:F2(),F3():]
dom tr is Element of bool F2()
tl is Relation-like F2() -defined F3() -valued Function-like quasi_total Element of bool [:F2(),F3():]
dom tl is Element of bool F2()
rtl is set
rtr is Element of F2()
tr . rtr is Element of F3()
F6(f19,rtr) is Element of F3()
tl . rtr is Element of F3()
tr . rtl is set
tl . rtl is set
s is Relation-like TS F1() -defined G -valued Function-like quasi_total Element of bool [:(TS F1()),G:]
s . (root-tree f19) is Element of G
tr is Element of the carrier of F1()
nt is Relation-like the carrier of F1() -valued Function-like DecoratedTree-like Element of TS F1()
( the carrier of F1(),nt) is Element of the carrier of F1()
nt . {} is set
rtl is Element of the carrier of F1()
tl is Relation-like the carrier of F1() -valued Function-like DecoratedTree-like Element of TS F1()
( the carrier of F1(),tl) is Element of the carrier of F1()
tl . {} is set
f19 is Element of NonTerminals F1()
<*tr,rtl*> is non empty Relation-like NAT -defined the carrier of F1() -valued Function-like finite V37(2) FinSequence-like FinSubsequence-like M20( the carrier of F1(),K237( the carrier of F1()))
K237( the carrier of F1()) is non empty functional FinSequence-membered M19( the carrier of F1())
f19 -tree (nt,tl) is Relation-like the carrier of F1() -valued Function-like DecoratedTree-like set
F5() . (f19 -tree (nt,tl)) is set
F5() . nt is Element of Funcs (F2(),F3())
F5() . tl is Element of Funcs (F2(),F3())
rtr is Relation-like F2() -defined F3() -valued Function-like quasi_total Element of bool [:F2(),F3():]
g is Relation-like F2() -defined F3() -valued Function-like quasi_total Element of bool [:F2(),F3():]
ff1 is Relation-like F2() -defined F3() -valued Function-like quasi_total Element of bool [:F2(),F3():]
ff2 is Element of G
xl is Element of G
((NonTerminals F1()),G,G,f19,ff2,xl) is V1() V2() Element of [:(NonTerminals F1()),G,G:]
[f19,ff2