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

{} 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 ^ <*b

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 ^ <*b

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 ^ <*b

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 ^ <*b

<*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 ^ <*b

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 ^ <*b

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 ^ <*b

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 ^ <*b

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 ^ <*b

nt is set

succ NTV is Element of bool G

{ (NTV ^ <*b

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 ^ <*b

nt is set

succ NTV is Element of bool s

{ (NTV ^ <*b

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

{ b

Terminals nt is set

tl is Element of the carrier of nt

[tl,NTV] is V1() set

{ b

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

F

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)

{ b

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)

F

the carrier of F

Terminals F

bool the carrier of F

NonTerminals F

FinTrees the carrier of F

TS F

bool (FinTrees the carrier of F

G is Element of the carrier of F

s is Relation-like NAT -defined FinTrees the carrier of F

roots s is Relation-like NAT -defined the carrier of F

rng s is functional finite constituted-DTrees Element of bool (FinTrees the carrier of F

G -tree s is Relation-like the carrier of F

s . 1 is Relation-like Function-like set

s . 2 is Relation-like Function-like set

TV is Relation-like the carrier of F

( the carrier of F

TV . {} is set

NTV is Relation-like the carrier of F

( the carrier of F

NTV . {} is set

<*( the carrier of F

K237( the carrier of F

G -tree (TV,NTV) is Relation-like the carrier of F

G is Element of the carrier of F

root-tree G is Relation-like the carrier of F

G is Relation-like the carrier of F

F

F

TS F

the carrier of F

FinTrees the carrier of F

bool (FinTrees the carrier of F

[:(TS F

bool [:(TS F

Terminals F

bool the carrier of F

NonTerminals F

G is Relation-like TS F

s is Element of Terminals F

root-tree s is Relation-like the carrier of F

G . (root-tree s) is Element of F

F

s is Element of NonTerminals F

TV is Relation-like the carrier of F

( the carrier of F

TV . {} is set

NTV is Relation-like the carrier of F

( the carrier of F

NTV . {} is set

G . TV is Element of F

G . NTV is Element of F

s -tree (TV,NTV) is Relation-like the carrier of F

G . (s -tree (TV,NTV)) is set

f19 is Element of the carrier of F

nt is Element of the carrier of F

<*f19,nt*> is non empty Relation-like NAT -defined the carrier of F

K237( the carrier of F

<*TV,NTV*> is non empty Relation-like NAT -defined TS F

K237((TS F

tr is Relation-like NAT -defined FinTrees the carrier of F

tr . 1 is Relation-like Function-like set

rtl is Element of F

rtr is Element of F

F

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

<*rtl,rtr*> is non empty Relation-like NAT -defined F

K237(F

g is Relation-like NAT -defined F

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 F

bool (TS F

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 F

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 F

s -tree tr is Relation-like the carrier of F

G . (s -tree tr) is set

g . 1 is set

g . 2 is set

F

F

TS F

the carrier of F

FinTrees the carrier of F

bool (FinTrees the carrier of F

F

[:(TS F

bool [:(TS F

Terminals F

bool the carrier of F

F

NonTerminals F

F

G is Element of the carrier of F

root-tree G is Relation-like the carrier of F

F

F

s is Relation-like NAT -defined FinTrees the carrier of F

roots s is Relation-like NAT -defined the carrier of F

F

K237(F

G is Element of the carrier of F

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 F

rng s is functional finite constituted-DTrees Element of bool (FinTrees the carrier of F

f19 is Relation-like the carrier of F

( the carrier of F

f19 . {} is set

nt is Relation-like the carrier of F

( the carrier of F

nt . {} is set

<*( the carrier of F

K237( the carrier of F

G -tree (f19,nt) is Relation-like the carrier of F

F

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

(F

tl is Element of F

F

(F

tr is Element of F

(roots s) . 1 is set

(roots s) . 2 is set

F

F

G is Element of the carrier of F

root-tree G is Relation-like the carrier of F

F

F

s is Relation-like NAT -defined FinTrees the carrier of F

roots s is Relation-like NAT -defined the carrier of F

F

G is Element of the carrier of F

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 F

rng s is functional finite constituted-DTrees Element of bool (FinTrees the carrier of F

f19 is Relation-like the carrier of F

( the carrier of F

f19 . {} is set

nt is Relation-like the carrier of F

( the carrier of F

nt . {} is set

<*( the carrier of F

G -tree (f19,nt) is Relation-like the carrier of F

F

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

(F

tl is Element of F

F

(F

tr is Element of F

(roots s) . 1 is set

(roots s) . 2 is set

F

F

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

F

F

TS F

the carrier of F

FinTrees the carrier of F

bool (FinTrees the carrier of F

F

Funcs (F

[:(TS F

bool [:(TS F

Terminals F

bool the carrier of F

[:F

bool [:F

NonTerminals F

s is Element of Terminals F

TV is Relation-like F

dom TV is Element of bool F

bool F

rng TV is Element of bool F

bool F

G is non empty set

NTV is Element of G

f19 is Element of G

nt is Relation-like F

tl is Element of F

nt . tl is Element of F

F

[:(Terminals F

bool [:(Terminals F

s is Relation-like Terminals F

TV is Element of NonTerminals F

NTV is Element of G

f19 is Element of G

nt is Relation-like F

dom nt is Element of bool F

rng nt is Element of bool F

tl is Element of G

tr is Element of G

rtr is Relation-like F

rtl is Element of F

rtr . rtl is Element of F

F

[:(NonTerminals F

[:[:(NonTerminals F

bool [:[:(NonTerminals F

TV is Relation-like [:(NonTerminals F

[:(TS F

bool [:(TS F

NTV is Relation-like TS F

f19 is Relation-like TS F

nt is Element of Terminals F

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 F

rtl is Relation-like F

root-tree nt is Relation-like the carrier of F

f19 . (root-tree nt) is Element of Funcs (F

rtr is Element of F

rtl . rtr is Element of F

F

nt is Element of NonTerminals F

tl is Relation-like the carrier of F

( the carrier of F

tl . {} is set

tr is Relation-like the carrier of F

( the carrier of F

tr . {} is set

nt -tree (tl,tr) is Relation-like the carrier of F

f19 . (nt -tree (tl,tr)) is set

f19 . tl is Element of Funcs (F

f19 . tr is Element of Funcs (F

rtl is Element of the carrier of F

rtr is Element of the carrier of F

<*rtl,rtr*> is non empty Relation-like NAT -defined the carrier of F

K237( the carrier of F

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 F

[nt,(NTV . tl)] is V1() set

[[nt,(NTV . tl)],(NTV . tr)] is V1() set

TV . ((NonTerminals F

ff1 is Relation-like F

g is Relation-like F

((NonTerminals F

[:(NonTerminals F

[nt,ff1] is V1() set

[[nt,ff1],g] is V1() set

TV . ((NonTerminals F

ff2 is Relation-like Function-like set

proj1 ff2 is set

proj2 ff2 is set

xl is Relation-like F

xr is Element of F

xl . xr is Element of F

F

F

TS F

the carrier of F

FinTrees the carrier of F

bool (FinTrees the carrier of F

F

F

Funcs (F

[:(TS F

bool [:(TS F

Terminals F

bool the carrier of F

[:F

bool [:F

F

NonTerminals F

F

G is non empty set

[:(TS F

bool [:(TS F

TV is Element of Terminals F

NTV is Relation-like F

dom NTV is Element of bool F

bool F

rng NTV is Element of bool F

bool F

f19 is Element of G

nt is Element of G

tl is Relation-like F

tr is Element of F

tl . tr is Element of F

F

[:(Terminals F

bool [:(Terminals F

TV is Relation-like Terminals F

NTV is Element of NonTerminals F

f19 is Element of G

nt is Element of G

tl is Relation-like F

dom tl is Element of bool F

rng tl is Element of bool F

tr is Element of G

rtl is Element of G

g is Relation-like F

rtr is Element of F

g . rtr is Element of F

F

[:(NonTerminals F

[:[:(NonTerminals F

bool [:[:(NonTerminals F

NTV is Relation-like [:(NonTerminals F

f19 is Element of Terminals F

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 F

F

tr is Relation-like F

dom tr is Element of bool F

tl is Relation-like F

dom tl is Element of bool F

rtl is set

rtr is Element of F

tr . rtr is Element of F

F

tl . rtr is Element of F

tr . rtl is set

tl . rtl is set

s is Relation-like TS F

s . (root-tree f19) is Element of G

tr is Element of the carrier of F

nt is Relation-like the carrier of F

( the carrier of F

nt . {} is set

rtl is Element of the carrier of F

tl is Relation-like the carrier of F

( the carrier of F

tl . {} is set

f19 is Element of NonTerminals F

<*tr,rtl*> is non empty Relation-like NAT -defined the carrier of F

K237( the carrier of F

f19 -tree (nt,tl) is Relation-like the carrier of F

F

F

F

rtr is Relation-like F

g is Relation-like F

ff1 is Relation-like F

ff2 is Element of G

xl is Element of G

((NonTerminals F

[f19,ff2