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
{} is empty Relation-like non-empty empty-yielding NAT -defined Function-like one-to-one constant functional finite finite-yielding V34() FinSequence-like FinSubsequence-like FinSequence-membered constituted-Trees constituted-FinTrees constituted-DTrees Tree-yielding FinTree-yielding DTree-yielding V101() V102() V103() V104() V105() V106() V107() 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
FinTrees is non empty constituted-Trees constituted-FinTrees Element of bool Trees
PeanoNat is non empty strict with_terminals with_nonterminals with_useful_nonterminals DTConstrStr
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 (FinTrees the carrier of PeanoNat)
bool (FinTrees the carrier of PeanoNat) is non empty set
[:(TS PeanoNat),NAT:] is Relation-like set
bool [:(TS PeanoNat),NAT:] is non empty set
[:NAT,(TS PeanoNat):] is Relation-like set
bool [:NAT,(TS PeanoNat):] 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
0 is empty Relation-like non-empty empty-yielding NAT -defined Function-like one-to-one constant functional V29() finite finite-yielding V34() FinSequence-like FinSubsequence-like FinSequence-membered constituted-Trees constituted-FinTrees constituted-DTrees Tree-yielding FinTree-yielding DTree-yielding V84() V85() ext-real V89() V90() V101() V102() V103() V104() V105() V106() V107() Element of NAT
elementary_tree 2 is non empty finite Tree-like set
<*0*> is non empty Relation-like NAT -defined NAT -valued Function-like finite V37(1) FinSequence-like FinSubsequence-like FinSequence of NAT
<*1*> is non empty Relation-like NAT -defined NAT -valued Function-like finite V37(1) FinSequence-like FinSubsequence-like FinSequence of NAT
K5({},<*0*>,<*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 )
<*> NAT is empty Relation-like non-empty empty-yielding NAT -defined NAT -valued Function-like one-to-one constant functional finite finite-yielding V34() FinSequence-like FinSubsequence-like FinSequence-membered constituted-Trees constituted-FinTrees constituted-DTrees Tree-yielding FinTree-yielding DTree-yielding V101() V102() V103() V104() V105() V106() V107() FinSequence of NAT
elementary_tree 0 is non empty finite Tree-like set
{{}} is non empty functional finite V34() Tree-like set
G is non empty set
s is Relation-like G -valued Function-like DecoratedTree-like set
s . {} is set
proj1 s is non empty Tree-like set
TV is Relation-like NAT -defined NAT -valued Function-like finite FinSequence-like FinSubsequence-like Element of proj1 s
s . TV is Element of G
G is non empty set
s is Relation-like G -valued Function-like DecoratedTree-like set
<*s*> is non empty Relation-like NAT -defined Function-like finite V37(1) FinSequence-like FinSubsequence-like DTree-yielding set
roots <*s*> is Relation-like NAT -defined Function-like finite FinSequence-like FinSubsequence-like set
(G,s) is Element of G
s . {} is set
<*(G,s)*> is non empty Relation-like NAT -defined G -valued Function-like finite V37(1) FinSequence-like FinSubsequence-like M20(G,K237(G))
K237(G) is non empty functional FinSequence-membered M19(G)
G is non empty set
s is Relation-like G -valued Function-like DecoratedTree-like set
TV is Relation-like G -valued Function-like DecoratedTree-like set
<*s,TV*> is non empty Relation-like NAT -defined Function-like finite V37(2) FinSequence-like FinSubsequence-like DTree-yielding set
roots <*s,TV*> is Relation-like NAT -defined Function-like finite FinSequence-like FinSubsequence-like 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)
<*0*> is non empty Relation-like NAT -defined Function-like finite V37(1) FinSequence-like FinSubsequence-like set
<*1*> is non empty Relation-like NAT -defined Function-like finite V37(1) FinSequence-like FinSubsequence-like set
G is non empty Tree-like set
Leaves G is Element of bool G
bool G is non empty set
s is Relation-like NAT -defined NAT -valued Function-like finite FinSequence-like FinSubsequence-like Element of G
succ s is Element of bool G
s ^ <*0*> is non empty Relation-like NAT -defined Function-like finite FinSequence-like FinSubsequence-like 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
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
<*NTV*> is non empty Relation-like NAT -defined Function-like finite V37(1) FinSequence-like FinSubsequence-like set
s ^ <*NTV*> is non empty Relation-like NAT -defined Function-like finite FinSequence-like FinSubsequence-like set
s is Relation-like NAT -defined NAT -valued Function-like finite FinSequence-like FinSubsequence-like Element of elementary_tree 0
Leaves (elementary_tree 0) is non empty finite Element of bool (elementary_tree 0)
bool (elementary_tree 0) is non empty finite V34() set
succ s is finite Element of bool (elementary_tree 0)
s ^ <*0*> is non empty Relation-like NAT -defined Function-like finite FinSequence-like FinSubsequence-like set
s ^ <*1*> is non empty Relation-like NAT -defined Function-like finite FinSequence-like FinSubsequence-like set
{(s ^ <*0*>),(s ^ <*1*>)} is non empty functional finite V34() set
TV is Relation-like NAT -defined NAT -valued Function-like finite FinSequence-like FinSubsequence-like FinSequence of NAT
s is Relation-like NAT -defined NAT -valued Function-like finite FinSequence-like FinSubsequence-like Element of elementary_tree 2
Leaves (elementary_tree 2) is non empty finite Element of bool (elementary_tree 2)
bool (elementary_tree 2) is non empty finite V34() set
succ s is finite Element of bool (elementary_tree 2)
s ^ <*0*> is non empty Relation-like NAT -defined Function-like finite FinSequence-like FinSubsequence-like set
s ^ <*1*> is non empty Relation-like NAT -defined Function-like finite FinSequence-like FinSubsequence-like set
{(s ^ <*0*>),(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 non empty Relation-like NAT -defined Function-like finite V37(1) FinSequence-like FinSubsequence-like set
s ^ <*f19*> is non empty Relation-like NAT -defined Function-like finite FinSequence-like FinSubsequence-like set
f19 is V29() V84() V85() ext-real V89() V90() V101() V102() V103() V104() V105() V106() Element of NAT
<*f19*> is non empty Relation-like NAT -defined Function-like finite V37(1) FinSequence-like FinSubsequence-like set
s ^ <*f19*> is non empty Relation-like NAT -defined Function-like finite FinSequence-like FinSubsequence-like set
NTV is Relation-like NAT -defined Function-like finite FinSequence-like FinSubsequence-like set
NTV is Relation-like NAT -defined Function-like finite FinSequence-like FinSubsequence-like set
f19 is V29() V84() V85() ext-real V89() V90() V101() V102() V103() V104() V105() V106() Element of NAT
<*f19*> is non empty Relation-like NAT -defined Function-like finite V37(1) FinSequence-like FinSubsequence-like set
s ^ <*f19*> is non empty Relation-like NAT -defined Function-like finite FinSequence-like FinSubsequence-like set
NTV is Relation-like NAT -defined Function-like finite FinSequence-like FinSubsequence-like set
len <*0*> is V29() V84() V85() ext-real V89() V90() V101() V102() V103() V104() V105() V106() Element of NAT
(len <*0*>) + (len <*0*>) is V29() V84() V85() ext-real V89() V90() V101() V102() V103() V104() V105() V106() Element of NAT
len <*0*> is V29() V84() V85() ext-real V89() V90() V101() V102() V103() V104() V105() V106() Element of NAT
(len <*0*>) + (len <*0*>) 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 + (len <*0*>) 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 <*0*> is V29() V84() V85() ext-real V89() V90() V101() V102() V103() V104() V105() V106() Element of NAT
(len <*1*>) + (len <*0*>) 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 <*0*> is V29() V84() V85() ext-real V89() V90() V101() V102() V103() V104() V105() V106() Element of NAT
(len <*1*>) + (len <*0*>) 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:]
NTV is Relation-like G -valued Function-like DecoratedTree-like set
proj1 NTV is non empty Tree-like set
the Relation-like {{}} -valued Function-like finite DecoratedTree-like () set is Relation-like {{}} -valued Function-like finite DecoratedTree-like () set
G is non empty Tree-like set
s is Relation-like NAT -defined NAT -valued Function-like finite FinSequence-like FinSubsequence-like Element of G
<*2*> is non empty Relation-like NAT -defined Function-like finite V37(1) FinSequence-like FinSubsequence-like set
s ^ <*2*> is non empty Relation-like NAT -defined Function-like finite FinSequence-like FinSubsequence-like set
s ^ <*0*> is non empty Relation-like NAT -defined Function-like finite FinSequence-like FinSubsequence-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 Relation-like NAT -defined Function-like finite FinSequence-like FinSubsequence-like set
{(s ^ <*0*>),(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
TV is Relation-like NAT -defined NAT -valued Function-like finite FinSequence-like FinSubsequence-like Element of tree (G,s)
f19 is Relation-like NAT -defined NAT -valued Function-like finite FinSequence-like FinSubsequence-like Element of G
<*0*> ^ f19 is non empty Relation-like NAT -defined Function-like finite FinSequence-like FinSubsequence-like set
nt is V29() V84() V85() ext-real V89() V90() V101() V102() V103() V104() V105() V106() Element of NAT
<*nt*> is non empty Relation-like NAT -defined Function-like finite V37(1) FinSequence-like FinSubsequence-like set
f19 ^ <*nt*> is non empty Relation-like NAT -defined Function-like finite FinSequence-like FinSubsequence-like set
<*0*> ^ (f19 ^ <*nt*>) is non empty Relation-like NAT -defined Function-like finite FinSequence-like FinSubsequence-like set
(<*0*> ^ f19) ^ <*nt*> is non empty Relation-like NAT -defined Function-like finite FinSequence-like FinSubsequence-like set
nt is V29() V84() V85() ext-real V89() V90() V101() V102() V103() V104() V105() V106() Element of NAT
<*nt*> is non empty Relation-like NAT -defined Function-like finite V37(1) FinSequence-like FinSubsequence-like set
TV ^ <*nt*> is non empty Relation-like NAT -defined Function-like finite FinSequence-like FinSubsequence-like set
f19 ^ <*nt*> is non empty Relation-like NAT -defined Function-like finite FinSequence-like FinSubsequence-like set
<*0*> ^ (f19 ^ <*nt*>) is non empty Relation-like NAT -defined Function-like finite FinSequence-like FinSubsequence-like set
f19 is Relation-like NAT -defined NAT -valued Function-like finite FinSequence-like FinSubsequence-like Element of s
<*1*> ^ f19 is non empty Relation-like NAT -defined Function-like finite FinSequence-like FinSubsequence-like set
nt is V29() V84() V85() ext-real V89() V90() V101() V102() V103() V104() V105() V106() Element of NAT
<*nt*> is non empty Relation-like NAT -defined Function-like finite V37(1) FinSequence-like FinSubsequence-like set
f19 ^ <*nt*> is non empty Relation-like NAT -defined Function-like finite FinSequence-like FinSubsequence-like set
<*1*> ^ (f19 ^ <*nt*>) is non empty Relation-like NAT -defined Function-like finite FinSequence-like FinSubsequence-like set
(<*1*> ^ f19) ^ <*nt*> is non empty Relation-like NAT -defined Function-like finite FinSequence-like FinSubsequence-like set
nt is V29() V84() V85() ext-real V89() V90() V101() V102() V103() V104() V105() V106() Element of NAT
<*nt*> is non empty Relation-like NAT -defined Function-like finite V37(1) FinSequence-like FinSubsequence-like set
TV ^ <*nt*> is non empty Relation-like NAT -defined Function-like finite FinSequence-like FinSubsequence-like set
f19 ^ <*nt*> is non empty Relation-like NAT -defined Function-like finite FinSequence-like FinSubsequence-like set
<*1*> ^ (f19 ^ <*nt*>) is non empty Relation-like NAT -defined Function-like finite FinSequence-like FinSubsequence-like set
G is non empty Tree-like set
s is non empty Tree-like set
tree (G,s) is non empty Tree-like set
TV is Relation-like NAT -defined NAT -valued Function-like finite FinSequence-like FinSubsequence-like Element of tree (G,s)
succ TV is Element of bool (tree (G,s))
bool (tree (G,s)) is non empty set
TV ^ <*0*> is non empty Relation-like NAT -defined Function-like finite FinSequence-like FinSubsequence-like set
TV ^ <*1*> is non empty Relation-like NAT -defined Function-like finite FinSequence-like FinSubsequence-like set
{(TV ^ <*0*>),(TV ^ <*1*>)} is non empty functional finite V34() set
<*1*> ^ {} is non empty Relation-like NAT -defined Function-like finite FinSequence-like FinSubsequence-like 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
<*0*> ^ {} is non empty Relation-like NAT -defined Function-like finite FinSequence-like FinSubsequence-like set
f19 is set
nt is V29() V84() V85() ext-real V89() V90() V101() V102() V103() V104() V105() V106() Element of NAT
<*nt*> is non empty Relation-like NAT -defined Function-like finite V37(1) FinSequence-like FinSubsequence-like set
TV ^ <*nt*> is non empty Relation-like NAT -defined Function-like finite FinSequence-like FinSubsequence-like set
tl is Relation-like NAT -defined Function-like finite FinSequence-like FinSubsequence-like set
tl . 1 is set
tr is Relation-like NAT -defined Function-like finite FinSequence-like FinSubsequence-like set
<*0*> ^ tr is non empty Relation-like NAT -defined Function-like finite FinSequence-like FinSubsequence-like set
rtl is Relation-like NAT -defined Function-like finite FinSequence-like FinSubsequence-like set
<*1*> ^ rtl is non empty Relation-like NAT -defined Function-like finite FinSequence-like FinSubsequence-like set
f19 is Relation-like NAT -defined NAT -valued Function-like finite FinSequence-like FinSubsequence-like Element of G
<*0*> ^ f19 is non empty Relation-like NAT -defined Function-like finite FinSequence-like FinSubsequence-like set
nt is Relation-like NAT -defined Function-like finite FinSequence-like FinSubsequence-like 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
<*tl*> is non empty Relation-like NAT -defined Function-like finite V37(1) FinSequence-like FinSubsequence-like set
f19 ^ <*tl*> is non empty Relation-like NAT -defined Function-like finite FinSequence-like FinSubsequence-like set
<*0*> ^ (f19 ^ <*tl*>) is non empty Relation-like NAT -defined Function-like finite FinSequence-like FinSubsequence-like set
(<*0*> ^ f19) ^ <*tl*> is non empty Relation-like NAT -defined Function-like finite FinSequence-like FinSubsequence-like set
TV ^ <*tl*> is non empty Relation-like NAT -defined Function-like finite FinSequence-like FinSubsequence-like set
<*0*> ^ nt is non empty Relation-like NAT -defined Function-like finite FinSequence-like FinSubsequence-like set
tr is V29() V84() V85() ext-real V89() V90() V101() V102() V103() V104() V105() V106() Element of NAT
<*tr*> is non empty Relation-like NAT -defined Function-like finite V37(1) FinSequence-like FinSubsequence-like set
TV ^ <*tr*> is non empty Relation-like NAT -defined Function-like finite FinSequence-like FinSubsequence-like set
f19 ^ <*tr*> is non empty Relation-like NAT -defined Function-like finite FinSequence-like FinSubsequence-like set
<*0*> ^ (f19 ^ <*tr*>) is non empty Relation-like NAT -defined Function-like finite FinSequence-like FinSubsequence-like set
f19 is Relation-like NAT -defined NAT -valued Function-like finite FinSequence-like FinSubsequence-like Element of s
<*1*> ^ f19 is non empty Relation-like NAT -defined Function-like finite FinSequence-like FinSubsequence-like set
succ f19 is Element of bool s
bool s is non empty set
nt is Relation-like NAT -defined Function-like finite FinSequence-like FinSubsequence-like set
<*1*> ^ nt is non empty Relation-like NAT -defined Function-like finite FinSequence-like FinSubsequence-like 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
<*tl*> is non empty Relation-like NAT -defined Function-like finite V37(1) FinSequence-like FinSubsequence-like set
f19 ^ <*tl*> is non empty Relation-like NAT -defined Function-like finite FinSequence-like FinSubsequence-like set
<*1*> ^ (f19 ^ <*tl*>) is non empty Relation-like NAT -defined Function-like finite FinSequence-like FinSubsequence-like set
(<*1*> ^ f19) ^ <*tl*> is non empty Relation-like NAT -defined Function-like finite FinSequence-like FinSubsequence-like set
TV ^ <*tl*> is non empty Relation-like NAT -defined Function-like finite FinSequence-like FinSubsequence-like set
tr is V29() V84() V85() ext-real V89() V90() V101() V102() V103() V104() V105() V106() Element of NAT
<*tr*> is non empty Relation-like NAT -defined Function-like finite V37(1) FinSequence-like FinSubsequence-like set
TV ^ <*tr*> is non empty Relation-like NAT -defined Function-like finite FinSequence-like FinSubsequence-like set
f19 ^ <*tr*> is non empty Relation-like NAT -defined Function-like finite FinSequence-like FinSubsequence-like set
<*1*> ^ (f19 ^ <*tr*>) is non empty Relation-like NAT -defined Function-like finite FinSequence-like FinSubsequence-like set
G is non empty Tree-like set
s is non empty Tree-like set
tree (G,s) is non empty Tree-like set
NTV is Relation-like NAT -defined NAT -valued Function-like finite FinSequence-like FinSubsequence-like Element of tree (G,s)
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 ^ <*0*> is non empty Relation-like NAT -defined Function-like finite FinSequence-like FinSubsequence-like set
NTV ^ <*1*> is non empty Relation-like NAT -defined Function-like finite FinSequence-like FinSubsequence-like set
{(NTV ^ <*0*>),(NTV ^ <*1*>)} is non empty functional finite V34() set
f19 is Relation-like NAT -defined Function-like finite FinSequence-like FinSubsequence-like set
<*0*> ^ f19 is non empty Relation-like NAT -defined Function-like finite FinSequence-like FinSubsequence-like set
nt is Relation-like NAT -defined Function-like finite FinSequence-like FinSubsequence-like set
<*1*> ^ nt is non empty Relation-like NAT -defined Function-like finite FinSequence-like FinSubsequence-like set
f19 is Relation-like NAT -defined Function-like finite FinSequence-like FinSubsequence-like set
<*0*> ^ f19 is non empty Relation-like NAT -defined Function-like finite FinSequence-like FinSubsequence-like set
<*1*> ^ f19 is non empty Relation-like NAT -defined Function-like finite FinSequence-like FinSubsequence-like set
nt is Relation-like NAT -defined NAT -valued Function-like finite FinSequence-like FinSubsequence-like Element of s
Leaves s is Element of bool s
bool s is non empty set
succ NTV is Element of bool (tree (G,s))
NTV ^ <*0*> is non empty Relation-like NAT -defined Function-like finite FinSequence-like FinSubsequence-like set
NTV ^ <*1*> is non empty Relation-like NAT -defined Function-like finite FinSequence-like FinSubsequence-like set
{(NTV ^ <*0*>),(NTV ^ <*1*>)} is non empty functional finite V34() set
nt is Relation-like NAT -defined NAT -valued Function-like finite FinSequence-like FinSubsequence-like Element of s
Leaves s is Element of bool s
bool s is non empty set
succ nt is Element of bool s
nt ^ <*0*> is non empty Relation-like NAT -defined Function-like finite FinSequence-like FinSubsequence-like set
nt ^ <*1*> is non empty Relation-like NAT -defined Function-like finite FinSequence-like FinSubsequence-like set
{(nt ^ <*0*>),(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
<*tr*> is non empty Relation-like NAT -defined Function-like finite V37(1) FinSequence-like FinSubsequence-like set
NTV ^ <*tr*> is non empty Relation-like NAT -defined Function-like finite FinSequence-like FinSubsequence-like set
nt ^ <*tr*> is non empty Relation-like NAT -defined Function-like finite FinSequence-like FinSubsequence-like set
<*1*> ^ (nt ^ <*tr*>) is non empty Relation-like NAT -defined Function-like finite FinSequence-like FinSubsequence-like set
rtl is Relation-like NAT -defined NAT -valued Function-like finite FinSequence-like FinSubsequence-like Element of s
NTV ^ <*0*> is non empty Relation-like NAT -defined Function-like finite FinSequence-like FinSubsequence-like set
NTV ^ <*1*> is non empty Relation-like NAT -defined Function-like finite FinSequence-like FinSubsequence-like set
{(NTV ^ <*0*>),(NTV ^ <*1*>)} is non empty functional finite V34() set
<*1*> ^ nt is non empty Relation-like NAT -defined Function-like finite FinSequence-like FinSubsequence-like set
(<*1*> ^ nt) ^ <*0*> is non empty Relation-like NAT -defined Function-like finite FinSequence-like FinSubsequence-like set
(<*1*> ^ nt) ^ <*1*> is non empty Relation-like NAT -defined Function-like finite FinSequence-like FinSubsequence-like set
<*1*> ^ (nt ^ <*0*>) is non empty Relation-like NAT -defined Function-like finite FinSequence-like FinSubsequence-like set
<*1*> ^ (nt ^ <*1*>) is non empty Relation-like NAT -defined Function-like finite FinSequence-like FinSubsequence-like set
nt is Relation-like NAT -defined NAT -valued Function-like finite FinSequence-like FinSubsequence-like Element of s
Leaves s is Element of bool s
bool s is non empty set
succ NTV is Element of bool (tree (G,s))
NTV ^ <*0*> is non empty Relation-like NAT -defined Function-like finite FinSequence-like FinSubsequence-like set
NTV ^ <*1*> is non empty Relation-like NAT -defined Function-like finite FinSequence-like FinSubsequence-like set
{(NTV ^ <*0*>),(NTV ^ <*1*>)} is non empty functional finite V34() set
succ NTV is Element of bool (tree (G,s))
NTV ^ <*0*> is non empty Relation-like NAT -defined Function-like finite FinSequence-like FinSubsequence-like set
NTV ^ <*1*> is non empty Relation-like NAT -defined Function-like finite FinSequence-like FinSubsequence-like set
{(NTV ^ <*0*>),(NTV ^ <*1*>)} is non empty functional finite V34() set
nt is Relation-like NAT -defined NAT -valued Function-like finite FinSequence-like FinSubsequence-like Element of G
Leaves G is Element of bool G
bool G is non empty set
nt is Relation-like NAT -defined NAT -valued Function-like finite FinSequence-like FinSubsequence-like Element of G
Leaves G is Element of bool G
bool G is non empty set
succ nt is Element of bool G
nt ^ <*0*> is non empty Relation-like NAT -defined Function-like finite FinSequence-like FinSubsequence-like set
nt ^ <*1*> is non empty Relation-like NAT -defined Function-like finite FinSequence-like FinSubsequence-like set
{(nt ^ <*0*>),(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
<*tr*> is non empty Relation-like NAT -defined Function-like finite V37(1) FinSequence-like FinSubsequence-like set
NTV ^ <*tr*> is non empty Relation-like NAT -defined Function-like finite FinSequence-like FinSubsequence-like set
nt ^ <*tr*> is non empty Relation-like NAT -defined Function-like finite FinSequence-like FinSubsequence-like set
<*0*> ^ (nt ^ <*tr*>) is non empty Relation-like NAT -defined Function-like finite FinSequence-like FinSubsequence-like set
rtl is Relation-like NAT -defined NAT -valued Function-like finite FinSequence-like FinSubsequence-like Element of G
<*0*> ^ nt is non empty Relation-like NAT -defined Function-like finite FinSequence-like FinSubsequence-like set
(<*0*> ^ nt) ^ <*0*> is non empty Relation-like NAT -defined Function-like finite FinSequence-like FinSubsequence-like set
(<*0*> ^ nt) ^ <*1*> is non empty Relation-like NAT -defined Function-like finite FinSequence-like FinSubsequence-like set
<*0*> ^ (nt ^ <*0*>) is non empty Relation-like NAT -defined Function-like finite FinSequence-like FinSubsequence-like set
<*0*> ^ (nt ^ <*1*>) is non empty Relation-like NAT -defined Function-like finite FinSequence-like FinSubsequence-like set
nt is Relation-like NAT -defined NAT -valued Function-like finite FinSequence-like FinSubsequence-like Element of G
Leaves G is Element of bool G
bool G is non empty set
NTV is Relation-like NAT -defined NAT -valued Function-like finite FinSequence-like FinSubsequence-like Element of G
<*0*> ^ NTV is non empty Relation-like NAT -defined Function-like finite FinSequence-like FinSubsequence-like set
Leaves G is Element of bool G
bool G is non empty set
f19 is Relation-like NAT -defined NAT -valued Function-like finite FinSequence-like FinSubsequence-like Element of tree (G,s)
succ f19 is Element of bool (tree (G,s))
(<*0*> ^ NTV) ^ <*0*> is non empty Relation-like NAT -defined Function-like finite FinSequence-like FinSubsequence-like set
(<*0*> ^ NTV) ^ <*1*> is non empty Relation-like NAT -defined Function-like finite FinSequence-like FinSubsequence-like set
{((<*0*> ^ NTV) ^ <*0*>),((<*0*> ^ 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
<*tl*> is non empty Relation-like NAT -defined Function-like finite V37(1) FinSequence-like FinSubsequence-like set
NTV ^ <*tl*> is non empty Relation-like NAT -defined Function-like finite FinSequence-like FinSubsequence-like set
<*0*> ^ (NTV ^ <*tl*>) is non empty Relation-like NAT -defined Function-like finite FinSequence-like FinSubsequence-like set
f19 ^ <*tl*> is non empty Relation-like NAT -defined Function-like finite FinSequence-like FinSubsequence-like set
f19 ^ <*0*> is non empty Relation-like NAT -defined Function-like finite FinSequence-like FinSubsequence-like set
f19 ^ <*1*> is non empty Relation-like NAT -defined Function-like finite FinSequence-like FinSubsequence-like set
NTV ^ <*0*> is non empty Relation-like NAT -defined Function-like finite FinSequence-like FinSubsequence-like set
NTV ^ <*1*> is non empty Relation-like NAT -defined Function-like finite FinSequence-like FinSubsequence-like set
{(NTV ^ <*0*>),(NTV ^ <*1*>)} is non empty functional finite V34() set
<*0*> ^ (NTV ^ <*1*>) is non empty Relation-like NAT -defined Function-like finite FinSequence-like FinSubsequence-like set
<*0*> ^ (NTV ^ <*0*>) is non empty Relation-like NAT -defined Function-like finite FinSequence-like FinSubsequence-like set
NTV is Relation-like NAT -defined NAT -valued Function-like finite FinSequence-like FinSubsequence-like Element of s
<*1*> ^ NTV is non empty Relation-like NAT -defined Function-like finite FinSequence-like FinSubsequence-like set
Leaves s is Element of bool s
bool s is non empty set
f19 is Relation-like NAT -defined NAT -valued Function-like finite FinSequence-like FinSubsequence-like Element of tree (G,s)
succ f19 is Element of bool (tree (G,s))
(<*1*> ^ NTV) ^ <*0*> is non empty Relation-like NAT -defined Function-like finite FinSequence-like FinSubsequence-like set
(<*1*> ^ NTV) ^ <*1*> is non empty Relation-like NAT -defined Function-like finite FinSequence-like FinSubsequence-like set
{((<*1*> ^ NTV) ^ <*0*>),((<*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
<*tl*> is non empty Relation-like NAT -defined Function-like finite V37(1) FinSequence-like FinSubsequence-like set
NTV ^ <*tl*> is non empty Relation-like NAT -defined Function-like finite FinSequence-like FinSubsequence-like set
<*1*> ^ (NTV ^ <*tl*>) is non empty Relation-like NAT -defined Function-like finite FinSequence-like FinSubsequence-like set
f19 ^ <*tl*> is non empty Relation-like NAT -defined Function-like finite FinSequence-like FinSubsequence-like set
f19 ^ <*0*> is non empty Relation-like NAT -defined Function-like finite FinSequence-like FinSubsequence-like set
f19 ^ <*1*> is non empty Relation-like NAT -defined Function-like finite FinSequence-like FinSubsequence-like set
NTV ^ <*0*> is non empty Relation-like NAT -defined Function-like finite FinSequence-like FinSubsequence-like set
NTV ^ <*1*> is non empty Relation-like NAT -defined Function-like finite FinSequence-like FinSubsequence-like set
{(NTV ^ <*0*>),(NTV ^ <*1*>)} is non empty functional finite V34() set
<*1*> ^ (NTV ^ <*1*>) is non empty Relation-like NAT -defined Function-like finite FinSequence-like FinSubsequence-like set
<*1*> ^ (NTV ^ <*0*>) is non empty Relation-like NAT -defined Function-like finite FinSequence-like FinSubsequence-like set
G is Relation-like Function-like DecoratedTree-like set
s is Relation-like Function-like DecoratedTree-like set
TV is set
TV -tree (G,s) is Relation-like Function-like DecoratedTree-like set
proj1 G is non empty Tree-like set
proj1 s is non empty Tree-like set
tree ((proj1 G),(proj1 s)) 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
TV is Relation-like G -valued Function-like finite DecoratedTree-like () set
NTV is Relation-like G -valued Function-like finite DecoratedTree-like () set
s -tree (TV,NTV) is Relation-like G -valued Function-like DecoratedTree-like set
<*TV,NTV*> is non empty Relation-like NAT -defined Function-like finite V37(2) FinSequence-like FinSubsequence-like DTree-yielding set
proj1 TV is non empty finite Tree-like set
FinTrees G is non empty functional constituted-DTrees DTree-set of G
proj1 NTV is non empty finite Tree-like set
proj2 <*TV,NTV*> is non empty finite set
<*TV*> is non empty Relation-like NAT -defined Function-like finite V37(1) FinSequence-like FinSubsequence-like DTree-yielding set
<*NTV*> is non empty Relation-like NAT -defined Function-like finite V37(1) FinSequence-like FinSubsequence-like DTree-yielding set
<*TV*> ^ <*NTV*> is non empty Relation-like NAT -defined Function-like finite V37(1 + 1) FinSequence-like FinSubsequence-like DTree-yielding 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 <*TV*>) \/ (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
nt is Relation-like NAT -defined FinTrees G -valued Function-like finite FinSequence-like FinSubsequence-like DTree-yielding FinSequence of FinTrees G
s -tree nt is Relation-like G -valued Function-like DecoratedTree-like Element of FinTrees G
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
G * is non empty functional FinSequence-membered set
TV is Element of G
<*TV*> is non empty Relation-like NAT -defined G -valued Function-like finite V37(1) FinSequence-like FinSubsequence-like M20(G,K237(G))
K237(G) is non empty functional FinSequence-membered M19(G)
<*TV*> ^ <*TV*> is non empty Relation-like NAT -defined G -valued Function-like finite V37(1 + 1) FinSequence-like FinSubsequence-like M20(G,K237(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
NTV is Relation-like NAT -defined Function-like finite FinSequence-like FinSubsequence-like 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
rtr is Relation-like NAT -defined Function-like finite FinSequence-like FinSubsequence-like set
tr is Element of the carrier of nt
[rtl,rtr] is V1() set
[0,NTV] is V1() set
<*1,1*> is non empty Relation-like NAT -defined Function-like finite V37(2) FinSequence-like FinSubsequence-like 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)
rtl is Relation-like NAT -defined Function-like finite FinSequence-like FinSubsequence-like set
[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
root-tree tr is Relation-like the carrier of nt -valued Function-like DecoratedTree-like Element of FinTrees the carrier of nt
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))
ff1 is Relation-like NAT -defined FinTrees the carrier of nt -valued Function-like finite FinSequence-like FinSubsequence-like DTree-yielding FinSequence of TS nt
root-tree 1 is Relation-like Function-like DecoratedTree-like set
<*(root-tree 1),(root-tree 1)*> is non empty Relation-like NAT -defined Function-like finite V37(2) FinSequence-like FinSubsequence-like DTree-yielding set
roots ff1 is Relation-like NAT -defined the carrier of nt -valued Function-like finite FinSequence-like FinSubsequence-like FinSequence of the carrier of nt
(root-tree tr) . {} is set
<*((root-tree tr) . {}),((root-tree tr) . {})*> 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
xl is Relation-like NAT -defined Function-like finite FinSequence-like FinSubsequence-like set
ff2 is Relation-like NAT -defined Function-like finite FinSequence-like FinSubsequence-like set
[rtr,ff2] is V1() set
(root-tree 1) . {} is set
xl is Relation-like NAT -defined FinTrees the carrier of nt -valued Function-like finite FinSequence-like FinSubsequence-like DTree-yielding FinSequence of TS nt
roots xl is Relation-like NAT -defined the carrier of nt -valued Function-like finite FinSequence-like FinSubsequence-like FinSequence of the carrier of nt
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
TV is Relation-like NAT -defined Function-like finite FinSequence-like FinSubsequence-like set
[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 is Relation-like NAT -defined the carrier of G -valued Function-like finite FinSequence-like FinSubsequence-like FinSequence of the carrier of G
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)*> is non empty Relation-like NAT -defined Function-like finite V37(1) FinSequence-like FinSubsequence-like set
<*(NTV . 2)*> is non empty Relation-like NAT -defined Function-like finite V37(1) FinSequence-like FinSubsequence-like 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 is Relation-like NAT -defined the carrier of G -valued Function-like finite FinSequence-like FinSubsequence-like FinSequence of the carrier of G
f19 . 1 is set
f19 . 2 is set
s is Element of the carrier of G
G is non empty with_terminals with_nonterminals () DTConstrStr
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
s is Relation-like NAT -defined FinTrees the carrier of G -valued Function-like finite FinSequence-like FinSubsequence-like DTree-yielding FinSequence of TS G
roots s is Relation-like NAT -defined the carrier of G -valued Function-like finite FinSequence-like FinSubsequence-like FinSequence of the carrier of G
dom s is finite V101() V102() V103() V104() V105() V106() Element of bool NAT
s . 1 is Relation-like Function-like set
s . 2 is Relation-like Function-like set
rng s is functional finite constituted-DTrees Element of bool (FinTrees the carrier of G)
TV is Element of the carrier of G
TV -tree s is Relation-like the carrier of G -valued Function-like DecoratedTree-like Element of FinTrees 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 Relation-like Function-like DecoratedTree-like set
nt . {} is set
<*NTV,f19*> . 2 is set
tl is Relation-like Function-like DecoratedTree-like set
tl . {} is set
tr is Relation-like the carrier of G -valued Function-like DecoratedTree-like Element of TS G
( the carrier of G,tr) is Element of the carrier of G
tr . {} is set
rtl is Relation-like the carrier of G -valued Function-like DecoratedTree-like Element of TS G
( 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
<*tr,rtl*> is non empty Relation-like NAT -defined TS G -valued Function-like finite V37(2) FinSequence-like FinSubsequence-like DTree-yielding M20( TS G,K237((TS G)))
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()
s is Relation-like NAT -defined FinTrees the carrier of F1() -valued Function-like finite FinSequence-like FinSubsequence-like DTree-yielding FinSequence of TS F1()
roots s is Relation-like NAT -defined the carrier of F1() -valued Function-like finite FinSequence-like FinSubsequence-like FinSequence 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()
s . 1 is Relation-like Function-like set
s . 2 is Relation-like Function-like set
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
F1() is non empty with_terminals with_nonterminals with_useful_nonterminals () DTConstrStr
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()
root-tree s is Relation-like the carrier of F1() -valued Function-like DecoratedTree-like Element of TS F1()
G . (root-tree s) 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())
tr is Relation-like NAT -defined FinTrees the carrier of F1() -valued Function-like finite FinSequence-like FinSubsequence-like DTree-yielding FinSequence of TS F1()
tr . 1 is Relation-like Function-like set
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())
g is Relation-like NAT -defined F2() -valued Function-like finite FinSequence-like FinSubsequence-like FinSequence of F2()
dom g is finite V101() V102() V103() V104() V105() V106() Element of bool NAT
tr . 2 is Relation-like Function-like set
dom G is functional constituted-DTrees Element of bool (TS F1())
bool (TS F1()) is non empty set
ff1 is set
tr . ff1 is Relation-like Function-like set
ff1 is set
g . ff1 is set
tr . ff1 is Relation-like Function-like set
G . (tr . ff1) is set
G * tr is Relation-like NAT -defined F2() -valued Function-like finite FinSequence-like FinSubsequence-like M20(F2(),K237(F2()))
tl is Relation-like NAT -defined Function-like finite FinSequence-like FinSubsequence-like 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
tr . ff1 is Relation-like Function-like set
tl . ff1 is set
tr . ff1 is Relation-like Function-like set
tl . ff1 is set
dom tl is finite V101() V102() V103() V104() V105() V106() Element of bool NAT
roots tr is Relation-like NAT -defined the carrier of F1() -valued Function-like finite FinSequence-like FinSubsequence-like FinSequence of the carrier of F1()
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()
F1() is non empty with_terminals with_nonterminals with_useful_nonterminals () DTConstrStr
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() . (root-tree G) is set
F5(G) is Element of F2()
s is Relation-like NAT -defined FinTrees the carrier of F1() -valued Function-like finite FinSequence-like FinSubsequence-like DTree-yielding FinSequence of TS F1()
roots s is Relation-like NAT -defined the carrier of F1() -valued Function-like finite FinSequence-like FinSubsequence-like FinSequence of the carrier of F1()
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()
s . 1 is Relation-like Function-like set
s . 2 is Relation-like Function-like set
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()
(roots s) . 1 is set
(roots s) . 2 is set
F4() . (G -tree s) is set
F6(G,((roots s) . 1),((roots s) . 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() . (root-tree G) is set
F5(G) is Element of F2()
s is Relation-like NAT -defined FinTrees the carrier of F1() -valued Function-like finite FinSequence-like FinSubsequence-like DTree-yielding FinSequence of TS F1()
roots s is Relation-like NAT -defined the carrier of F1() -valued Function-like finite FinSequence-like FinSubsequence-like FinSequence of the carrier of F1()
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()
s . 1 is Relation-like Function-like set
s . 2 is Relation-like Function-like set
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()
(roots s) . 1 is set
(roots s) . 2 is set
F3() . (G -tree s) is set
F6(G,((roots s) . 1),((roots s) . 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
F1() is non empty with_terminals with_nonterminals with_useful_nonterminals () DTConstrStr
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
s is Relation-like Terminals F1() -defined G -valued Function-like quasi_total Element of bool [:(Terminals F1()),G:]
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
tl is Relation-like Function-like set
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 . (root-tree nt) 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
ff1 is Relation-like Function-like set
proj1 ff1 is set
proj2 ff1 is set
NTV . tl is Element of G
ff2 is Relation-like Function-like set
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
ff2 is Relation-like Function-like 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()
F1() is non empty with_terminals with_nonterminals with_useful_nonterminals () DTConstrStr
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
TV is Relation-like Terminals F1() -defined G -valued Function-like quasi_total Element of bool [:(Terminals F1()),G:]
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
nt is Relation-like Function-like set
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] is V1() set
[[f19,ff2],xl] is V1() set
NTV . ((NonTerminals F1()),G,G,f19,ff2,xl) is Element of G
xr is Relation-like Function-like set
proj1 xr is set
proj2 xr is set
s . nt is Element of G
s . tl is Element of G
dom rtr is Element of bool F2()
ntvnt is Relation-like F2() -defined F3() -valued Function-like quasi_total Element of bool [:F2(),F3():]
dom ntvnt is Element of bool F2()
ntvnt is set
x is Element of F2()
rtr . x is Element of F3()
F7(f19,ff2,xl,x) is Element of F3()
ntvnt . x is Element of F3()
rtr . ntvnt is set
ntvnt . ntvnt is set
s . (f19 -tree (nt,tl)) is set
nt is Element of Terminals F1()
TV . nt is Element of G
tl is Relation-like Function-like set
proj1 tl is set
proj2 tl is set
root-tree nt is Relation-like the carrier of F1() -valued Function-like DecoratedTree-like Element of TS F1()
F4() . (root-tree nt) is Element of Funcs (F2(),F3())
rtl is Relation-like F2() -defined F3() -valued Function-like quasi_total Element of bool [:F2(),F3():]
dom rtl is Element of bool F2()
tr is Relation-like F2() -defined F3() -valued Function-like quasi_total Element of bool [:F2(),F3():]
dom tr is Element of bool F2()
rtr is set
g is Element of F2()
rtl . g is Element of F3()
F6(nt,g) is Element of F3()
tr . g is Element of F3()
rtl . rtr is set
tr . rtr is set
f19 is Relation-like TS F1() -defined G -valued Function-like quasi_total Element of bool [:(TS F1()),G:]
f19 . (root-tree nt) is Element of G
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
rtr is Element of the carrier of F1()
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 is Element of NonTerminals 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()))
nt -tree (tl,tr) is Relation-like the carrier of F1() -valued Function-like DecoratedTree-like set
F4() . (nt -tree (tl,tr)) is set
F4() . tl is Element of Funcs (F2(),F3())
F4() . tr is Element of Funcs (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 Relation-like F2() -defined F3() -valued Function-like quasi_total Element of bool [:F2(),F3():]
xl is Element of G
xr is Element of G
((NonTerminals F1()),G,G,nt,xl,xr) is V1() V2() Element of [:(NonTerminals F1()),G,G:]
[nt,xl] is V1() set
[[nt,xl],xr] is V1() set
NTV . ((NonTerminals F1()),G,G,nt,xl,xr) is Element of G
ntvnt is Relation-like Function-like set
proj1 ntvnt is set
proj2 ntvnt is set
f19 . tl is Element of G
f19 . tr is Element of G
dom g is Element of bool F2()
ntvnt is Relation-like F2() -defined F3() -valued Function-like quasi_total Element of bool [:F2(),F3():]
dom ntvnt is Element of bool F2()
x is set
xx is Element of F2()
g . xx is Element of F3()
F7(nt,xl,xr,xx) is Element of F3()
ntvnt . xx is Element of F3()
g . x is set
ntvnt . x is set
f19 . (nt -tree (tl,tr)) is set
G is non empty with_terminals with_nonterminals () DTConstrStr
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
Terminals G is non empty Element of bool the carrier of G
bool the carrier of G is non empty set
s is Element of Terminals G
root-tree s is Relation-like the carrier of G -valued Function-like DecoratedTree-like Element of TS G
proj1 (root-tree s) is non empty finite Tree-like set
NonTerminals G is non empty Element of bool the carrier of G
s is Element of NonTerminals G
TV is Relation-like the carrier of G -valued Function-like DecoratedTree-like Element of TS G
( the carrier of G,TV) is Element of the carrier of G
TV . {} is set
NTV is Relation-like the carrier of G -valued Function-like DecoratedTree-like Element of TS G
( the carrier of G,NTV) is Element of the carrier of G
NTV . {} is set
<*( the carrier of G,TV),( the carrier of G,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))
K237( the carrier of G) is non empty functional FinSequence-membered M19( the carrier of G)
s -tree (TV,NTV) is Relation-like the carrier of G -valued Function-like DecoratedTree-like set