:: FREEALG semantic presentation

REAL is set

NAT is non empty V23() V24() V25() V30() V35() V36() Element of K32(REAL)

K32(REAL) is non empty set

NAT is non empty V23() V24() V25() V30() V35() V36() set

K32(NAT) is non empty V30() set

K32(NAT) is non empty V30() set

{} is empty Relation-like non-empty empty-yielding NAT -defined Function-like one-to-one constant functional V23() V24() V25() V27() V28() V29() V30() V35() V37( {} ) FinSequence-like FinSubsequence-like FinSequence-membered constituted-Trees constituted-FinTrees constituted-DTrees Tree-yielding FinTree-yielding DTree-yielding with_common_domain V129() V130() V131() set

the empty Relation-like non-empty empty-yielding NAT -defined Function-like one-to-one constant functional V23() V24() V25() V27() V28() V29() V30() V35() V37( {} ) FinSequence-like FinSubsequence-like FinSequence-membered constituted-Trees constituted-FinTrees constituted-DTrees Tree-yielding FinTree-yielding DTree-yielding with_common_domain V129() V130() V131() set is empty Relation-like non-empty empty-yielding NAT -defined Function-like one-to-one constant functional V23() V24() V25() V27() V28() V29() V30() V35() V37( {} ) FinSequence-like FinSubsequence-like FinSequence-membered constituted-Trees constituted-FinTrees constituted-DTrees Tree-yielding FinTree-yielding DTree-yielding with_common_domain V129() V130() V131() set

1 is non empty V23() V24() V25() V29() V30() V35() V129() V130() V131() V132() Element of NAT

{{},1} is non empty set

Trees is non empty constituted-Trees set

K32(Trees) is non empty set

FinTrees is non empty constituted-Trees constituted-FinTrees Element of K32(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 K32((FinTrees the carrier of PeanoNat))

K32((FinTrees the carrier of PeanoNat)) is non empty set

K33((TS PeanoNat),NAT) is non empty Relation-like V30() set

K32(K33((TS PeanoNat),NAT)) is non empty V30() set

K33(NAT,(TS PeanoNat)) is non empty Relation-like V30() set

K32(K33(NAT,(TS PeanoNat))) is non empty V30() set

K343() is non empty set

0 is empty Relation-like non-empty empty-yielding NAT -defined Function-like one-to-one constant functional V23() V24() V25() V27() V28() V29() V30() V35() V37( {} ) FinSequence-like FinSubsequence-like FinSequence-membered constituted-Trees constituted-FinTrees constituted-DTrees Tree-yielding FinTree-yielding DTree-yielding with_common_domain V129() V130() V131() Element of NAT

{0,1} is non empty set

COMPLEX is set

RAT is set

INT is set

2 is non empty V23() V24() V25() V29() V30() V35() V129() V130() V131() V132() Element of NAT

3 is non empty V23() V24() V25() V29() V30() V35() V129() V130() V131() V132() Element of NAT

Seg 1 is non empty V5() V30() V37(1) Element of K32(NAT)

{1} is non empty V5() V37(1) set

Seg 2 is non empty V30() V37(2) Element of K32(NAT)

{1,2} is non empty set

roots {} is Relation-like NAT -defined Function-like V30() FinSequence-like FinSubsequence-like set

dom {} is empty Relation-like non-empty empty-yielding NAT -defined Function-like one-to-one constant functional V23() V24() V25() V27() V28() V29() V30() V35() V37( {} ) FinSequence-like FinSubsequence-like FinSequence-membered constituted-Trees constituted-FinTrees constituted-DTrees Tree-yielding FinTree-yielding DTree-yielding with_common_domain V129() V130() V131() set

rng {} is empty V5() Relation-like non-empty empty-yielding NAT -defined Function-like one-to-one constant functional V23() V24() V25() V27() V28() V29() V30() V35() V37( {} ) FinSequence-like FinSubsequence-like FinSequence-membered constituted-Trees constituted-FinTrees constituted-DTrees Tree-yielding FinTree-yielding DTree-yielding V75() with_common_domain V129() V130() V131() set

- 1 is V129() V130() V131() set

{(- 1)} is non empty V5() V37(1) set

D is non empty V5() V37(1) set

f is set

c

<*1*> is non empty V5() Relation-like NAT -defined NAT -valued Function-like constant V30() V37(1) FinSequence-like FinSubsequence-like Element of NAT *

NAT * is non empty functional FinSequence-membered FinSequenceSet of NAT

rng <*1*> is non empty V5() V37(1) set

<*0*> is non empty V5() Relation-like NAT -defined NAT -valued Function-like constant V30() V37(1) FinSequence-like FinSubsequence-like Element of NAT *

rng <*0*> is non empty V5() V37(1) set

{0} is non empty V5() functional V37(1) set

D is Relation-like set

rng D is set

D is Relation-like NAT -defined NAT -valued Function-like V30() FinSequence-like FinSubsequence-like FinSequence of NAT

rng D is set

D is Relation-like NAT -defined NAT -valued Function-like V30() FinSequence-like FinSubsequence-like FinSequence of NAT

rng D is set

f is V23() V24() V25() V29() V30() V35() V129() V130() V131() Element of NAT

D is non empty V109() quasi_total non-empty UAStr

the charact of D is Relation-like NAT -defined PFuncs (( the carrier of D *), the carrier of D) -valued Function-like V30() FinSequence-like FinSubsequence-like FinSequence of PFuncs (( the carrier of D *), the carrier of D)

the carrier of D is non empty set

the carrier of D * is non empty functional FinSequence-membered FinSequenceSet of the carrier of D

PFuncs (( the carrier of D *), the carrier of D) is non empty functional set

dom the charact of D is Element of K32(NAT)

the charact of D . f is Relation-like Function-like set

Operations D is non empty PFuncsDomHQN of the carrier of D

rng the charact of D is set

D is non empty V109() quasi_total non-empty UAStr

the carrier of D is non empty set

K32( the carrier of D) is non empty set

f is non empty Element of K32( the carrier of D)

c

D is non empty V109() quasi_total non-empty UAStr

the carrier of D is non empty set

K32( the carrier of D) is non empty set

Constants D is Element of K32( the carrier of D)

the carrier of D * is non empty functional FinSequence-membered FinSequenceSet of the carrier of D

Operations D is non empty PFuncsDomHQN of the carrier of D

the charact of D is Relation-like NAT -defined PFuncs (( the carrier of D *), the carrier of D) -valued Function-like V30() FinSequence-like FinSubsequence-like FinSequence of PFuncs (( the carrier of D *), the carrier of D)

PFuncs (( the carrier of D *), the carrier of D) is non empty functional set

rng the charact of D is set

{ b

( arity b

f is Element of K32( the carrier of D)

c

fua is Element of the carrier of D

U1 is non empty Relation-like the carrier of D * -defined the carrier of D -valued Function-like homogeneous quasi_total Element of Operations D

arity U1 is V23() V24() V25() V29() V30() V35() V129() V130() V131() Element of NAT

rng U1 is non empty set

U1 is non empty Relation-like the carrier of D * -defined the carrier of D -valued Function-like homogeneous quasi_total Element of Operations D

arity U1 is V23() V24() V25() V29() V30() V35() V129() V130() V131() Element of NAT

rng U1 is non empty set

dom U1 is non empty functional FinSequence-membered with_common_domain Element of K32(( the carrier of D *))

K32(( the carrier of D *)) is non empty set

A is set

U1 . A is set

0 -tuples_on the carrier of D is non empty functional FinSequence-membered FinSequenceSet of the carrier of D

{ b

c1 is Relation-like NAT -defined the carrier of D -valued Function-like V30() FinSequence-like FinSubsequence-like Element of the carrier of D *

rng c1 is set

len c1 is V23() V24() V25() V29() V30() V35() V129() V130() V131() Element of NAT

D is non empty V109() quasi_total non-empty UAStr

the carrier of D is non empty set

K32( the carrier of D) is non empty set

Constants D is Element of K32( the carrier of D)

the carrier of D * is non empty functional FinSequence-membered FinSequenceSet of the carrier of D

Operations D is non empty PFuncsDomHQN of the carrier of D

the charact of D is Relation-like NAT -defined PFuncs (( the carrier of D *), the carrier of D) -valued Function-like V30() FinSequence-like FinSubsequence-like FinSequence of PFuncs (( the carrier of D *), the carrier of D)

PFuncs (( the carrier of D *), the carrier of D) is non empty functional set

rng the charact of D is set

{ b

( arity b

f is Element of K32( the carrier of D)

GenUnivAlg f is non empty strict V109() quasi_total non-empty SubAlgebra of D

the carrier of (GenUnivAlg f) is non empty set

c

c

fua is non empty Element of K32( the carrier of D)

UniAlgSetClosed fua is non empty strict V109() quasi_total non-empty SubAlgebra of D

Opers (D,fua) is Relation-like NAT -defined PFuncs ((fua *),fua) -valued Function-like V30() FinSequence-like FinSubsequence-like FinSequence of PFuncs ((fua *),fua)

fua * is non empty functional FinSequence-membered FinSequenceSet of fua

PFuncs ((fua *),fua) is non empty functional set

UAStr(# fua,(Opers (D,fua)) #) is strict UAStr

K32(fua) is non empty set

D is non empty V109() quasi_total non-empty UAStr

the set is set

{ the set } is non empty V5() V37(1) set

f is non empty set

the Element of f is Element of f

f * is non empty functional FinSequence-membered FinSequenceSet of f

PFuncs ((f *),f) is non empty functional set

<*> f is empty Relation-like non-empty empty-yielding NAT -defined f -valued Function-like one-to-one constant functional V23() V24() V25() V27() V28() V29() V30() V35() V37( {} ) FinSequence-like FinSubsequence-like FinSequence-membered constituted-Trees constituted-FinTrees constituted-DTrees Tree-yielding FinTree-yielding DTree-yielding with_common_domain V129() V130() V131() Element of f *

(<*> f) .--> the Element of f is set

{(<*> f)} is non empty V5() functional V37(1) set

{(<*> f)} --> the Element of f is Relation-like {(<*> f)} -defined { the Element of f} -valued Function-like quasi_total Element of K32(K33({(<*> f)},{ the Element of f}))

{ the Element of f} is non empty V5() V37(1) set

K33({(<*> f)},{ the Element of f}) is non empty Relation-like set

K32(K33({(<*> f)},{ the Element of f})) is non empty set

fua is Relation-like Function-like Element of PFuncs ((f *),f)

<*fua*> is non empty V5() Relation-like NAT -defined PFuncs ((f *),f) -valued Function-like constant V30() V37(1) FinSequence-like FinSubsequence-like Element of (PFuncs ((f *),f)) *

(PFuncs ((f *),f)) * is non empty functional FinSequence-membered FinSequenceSet of PFuncs ((f *),f)

U1 is Relation-like NAT -defined PFuncs ((f *),f) -valued Function-like V30() FinSequence-like FinSubsequence-like FinSequence of PFuncs ((f *),f)

UAStr(# f,U1 #) is strict UAStr

the carrier of UAStr(# f,U1 #) is set

the charact of UAStr(# f,U1 #) is Relation-like NAT -defined PFuncs (( the carrier of UAStr(# f,U1 #) *), the carrier of UAStr(# f,U1 #)) -valued Function-like V30() FinSequence-like FinSubsequence-like FinSequence of PFuncs (( the carrier of UAStr(# f,U1 #) *), the carrier of UAStr(# f,U1 #))

the carrier of UAStr(# f,U1 #) * is non empty functional FinSequence-membered FinSequenceSet of the carrier of UAStr(# f,U1 #)

PFuncs (( the carrier of UAStr(# f,U1 #) *), the carrier of UAStr(# f,U1 #)) is non empty functional set

len the charact of UAStr(# f,U1 #) is V23() V24() V25() V29() V30() V35() V129() V130() V131() Element of NAT

c1 is non empty V109() quasi_total non-empty UAStr

the charact of c1 is Relation-like NAT -defined PFuncs (( the carrier of c1 *), the carrier of c1) -valued Function-like V30() FinSequence-like FinSubsequence-like FinSequence of PFuncs (( the carrier of c1 *), the carrier of c1)

the carrier of c1 is non empty set

the carrier of c1 * is non empty functional FinSequence-membered FinSequenceSet of the carrier of c1

PFuncs (( the carrier of c1 *), the carrier of c1) is non empty functional set

dom the charact of c1 is Element of K32(NAT)

Operations c1 is non empty PFuncsDomHQN of the carrier of c1

rng the charact of c1 is set

the charact of c1 . 1 is Relation-like Function-like set

{} the carrier of c1 is empty proper Relation-like non-empty empty-yielding NAT -defined Function-like one-to-one constant functional V23() V24() V25() V27() V28() V29() V30() V35() V37( {} ) FinSequence-like FinSubsequence-like FinSequence-membered constituted-Trees constituted-FinTrees constituted-DTrees Tree-yielding FinTree-yielding DTree-yielding with_common_domain V129() V130() V131() Element of K32( the carrier of c1)

K32( the carrier of c1) is non empty set

GenUnivAlg ({} the carrier of c1) is non empty strict V109() quasi_total non-empty SubAlgebra of c1

the carrier of (GenUnivAlg ({} the carrier of c1)) is non empty set

ff is non empty Element of K32( the carrier of c1)

Opers (c1,ff) is Relation-like NAT -defined PFuncs ((ff *),ff) -valued Function-like V30() FinSequence-like FinSubsequence-like FinSequence of PFuncs ((ff *),ff)

ff * is non empty functional FinSequence-membered FinSequenceSet of ff

PFuncs ((ff *),ff) is non empty functional set

dom (Opers (c1,ff)) is Element of K32(NAT)

ff is V23() V24() V25() V29() V30() V35() V129() V130() V131() set

the charact of c1 . ff is Relation-like Function-like set

(Opers (c1,ff)) . ff is Relation-like Function-like set

x is non empty Relation-like the carrier of c1 * -defined the carrier of c1 -valued Function-like homogeneous quasi_total Element of Operations c1

x /. ff is non empty Relation-like ff * -defined ff -valued Function-like homogeneous quasi_total Element of K32(K33((ff *),ff))

K33((ff *),ff) is non empty Relation-like set

K32(K33((ff *),ff)) is non empty set

the charact of (GenUnivAlg ({} the carrier of c1)) is Relation-like NAT -defined PFuncs (( the carrier of (GenUnivAlg ({} the carrier of c1)) *), the carrier of (GenUnivAlg ({} the carrier of c1))) -valued Function-like V30() FinSequence-like FinSubsequence-like FinSequence of PFuncs (( the carrier of (GenUnivAlg ({} the carrier of c1)) *), the carrier of (GenUnivAlg ({} the carrier of c1)))

the carrier of (GenUnivAlg ({} the carrier of c1)) * is non empty functional FinSequence-membered FinSequenceSet of the carrier of (GenUnivAlg ({} the carrier of c1))

PFuncs (( the carrier of (GenUnivAlg ({} the carrier of c1)) *), the carrier of (GenUnivAlg ({} the carrier of c1))) is non empty functional set

cf is non empty Relation-like the carrier of c1 * -defined the carrier of c1 -valued Function-like homogeneous quasi_total Element of Operations c1

dom cf is non empty functional FinSequence-membered with_common_domain Element of K32(( the carrier of c1 *))

K32(( the carrier of c1 *)) is non empty set

F is Relation-like NAT -defined Function-like V30() FinSequence-like FinSubsequence-like set

len F is V23() V24() V25() V29() V30() V35() V129() V130() V131() Element of NAT

arity cf is V23() V24() V25() V29() V30() V35() V129() V130() V131() Element of NAT

F is Relation-like NAT -defined Function-like V30() FinSequence-like FinSubsequence-like set

cf . (<*> f) is set

rng cf is non empty set

Constants c1 is Element of K32( the carrier of c1)

{ b

( arity b

F is (c1)

ff is non empty V109() quasi_total non-empty UAStr

signature c1 is Relation-like NAT -defined NAT -valued Function-like V30() FinSequence-like FinSubsequence-like FinSequence of NAT

signature ff is Relation-like NAT -defined NAT -valued Function-like V30() FinSequence-like FinSubsequence-like FinSequence of NAT

the charact of ff is Relation-like NAT -defined PFuncs (( the carrier of ff *), the carrier of ff) -valued Function-like V30() FinSequence-like FinSubsequence-like FinSequence of PFuncs (( the carrier of ff *), the carrier of ff)

the carrier of ff is non empty set

the carrier of ff * is non empty functional FinSequence-membered FinSequenceSet of the carrier of ff

PFuncs (( the carrier of ff *), the carrier of ff) is non empty functional set

len the charact of ff is V23() V24() V25() V29() V30() V35() V129() V130() V131() Element of NAT

dom the charact of ff is Element of K32(NAT)

Operations ff is non empty PFuncsDomHQN of the carrier of ff

rng the charact of ff is set

the charact of ff . 1 is Relation-like Function-like set

x is non empty Relation-like the carrier of ff * -defined the carrier of ff -valued Function-like homogeneous quasi_total Element of Operations ff

rng x is non empty set

ff is (c1)

K33(ff, the carrier of ff) is Relation-like set

K32(K33(ff, the carrier of ff)) is non empty set

dom x is non empty functional FinSequence-membered with_common_domain Element of K32(( the carrier of ff *))

K32(( the carrier of ff *)) is non empty set

o2 is set

x . o2 is set

K33( the carrier of c1, the carrier of ff) is non empty Relation-like set

K32(K33( the carrier of c1, the carrier of ff)) is non empty set

x is Element of the carrier of ff

the carrier of c1 --> x is Relation-like the carrier of c1 -defined the carrier of ff -valued Function-like quasi_total Element of K32(K33( the carrier of c1, the carrier of ff))

{x} is non empty V5() V37(1) set

K33( the carrier of c1,{x}) is non empty Relation-like set

xa is Relation-like the carrier of c1 -defined the carrier of ff -valued Function-like quasi_total Element of K32(K33( the carrier of c1, the carrier of ff))

len (signature c1) is V23() V24() V25() V29() V30() V35() V129() V130() V131() Element of NAT

len the charact of c1 is V23() V24() V25() V29() V30() V35() V129() V130() V131() Element of NAT

dom (signature c1) is Element of K32(NAT)

Seg (len (signature c1)) is V30() V37( len (signature c1)) Element of K32(NAT)

(signature c1) . 1 is set

arity x is V23() V24() V25() V29() V30() V35() V129() V130() V131() Element of NAT

rxa is V23() V24() V25() V29() V30() V35() V129() V130() V131() Element of NAT

rxa is non empty Relation-like the carrier of c1 * -defined the carrier of c1 -valued Function-like homogeneous quasi_total Element of Operations c1

the charact of c1 . rxa is Relation-like Function-like set

fx is non empty Relation-like the carrier of ff * -defined the carrier of ff -valued Function-like homogeneous quasi_total Element of Operations ff

the charact of ff . rxa is Relation-like Function-like set

nt is Relation-like NAT -defined the carrier of c1 -valued Function-like V30() FinSequence-like FinSubsequence-like FinSequence of the carrier of c1

dom rxa is non empty functional FinSequence-membered with_common_domain Element of K32(( the carrier of c1 *))

<*> the carrier of c1 is empty Relation-like non-empty empty-yielding NAT -defined the carrier of c1 -valued Function-like one-to-one constant functional V23() V24() V25() V27() V28() V29() V30() V35() V37( {} ) FinSequence-like FinSubsequence-like FinSequence-membered constituted-Trees constituted-FinTrees constituted-DTrees Tree-yielding FinTree-yielding DTree-yielding with_common_domain V129() V130() V131() Element of the carrier of c1 *

xa is Relation-like the carrier of c1 -defined the carrier of ff -valued Function-like quasi_total Element of K32(K33( the carrier of c1, the carrier of ff))

xa * nt is Relation-like NAT -defined the carrier of ff -valued Function-like V30() FinSequence-like FinSubsequence-like Element of the carrier of ff *

<*> the carrier of ff is empty Relation-like non-empty empty-yielding NAT -defined the carrier of ff -valued Function-like one-to-one constant functional V23() V24() V25() V27() V28() V29() V30() V35() V37( {} ) FinSequence-like FinSubsequence-like FinSequence-membered constituted-Trees constituted-FinTrees constituted-DTrees Tree-yielding FinTree-yielding DTree-yielding with_common_domain V129() V130() V131() Element of the carrier of ff *

dom fx is non empty functional FinSequence-membered with_common_domain Element of K32(( the carrier of ff *))

0 -tuples_on the carrier of ff is non empty functional FinSequence-membered FinSequenceSet of the carrier of ff

{ b

{(<*> the carrier of ff)} is non empty V5() functional V37(1) set

fx . (xa * nt) is set

rng rxa is non empty set

rxa . nt is set

xa . (rxa . nt) is set

s is Relation-like ff -defined the carrier of ff -valued Function-like quasi_total Element of K32(K33(ff, the carrier of ff))

xa | ff is Relation-like the carrier of c1 -defined ff -defined the carrier of c1 -defined the carrier of ff -valued Function-like Element of K32(K33( the carrier of c1, the carrier of ff))

ff is (c1)

D is non empty V109() quasi_total non-empty () UAStr

D is non empty strict V109() quasi_total non-empty UAStr

the carrier of D is non empty set

K32( the carrier of D) is non empty set

Constants D is Element of K32( the carrier of D)

the carrier of D * is non empty functional FinSequence-membered FinSequenceSet of the carrier of D

Operations D is non empty PFuncsDomHQN of the carrier of D

the charact of D is Relation-like NAT -defined PFuncs (( the carrier of D *), the carrier of D) -valued Function-like V30() FinSequence-like FinSubsequence-like FinSequence of PFuncs (( the carrier of D *), the carrier of D)

PFuncs (( the carrier of D *), the carrier of D) is non empty functional set

rng the charact of D is set

{ b

( arity b

f is Element of K32( the carrier of D)

GenUnivAlg f is non empty strict V109() quasi_total non-empty SubAlgebra of D

the carrier of (GenUnivAlg f) is non empty set

D is non empty Relation-like NAT -defined NAT -valued Function-like V30() FinSequence-like FinSubsequence-like FinSequence of NAT

dom D is non empty Element of K32(NAT)

f is set

(dom D) \/ f is non empty set

((dom D) \/ f) * is non empty functional FinSequence-membered FinSequenceSet of (dom D) \/ f

K33(((dom D) \/ f),(((dom D) \/ f) *)) is non empty Relation-like set

K32(K33(((dom D) \/ f),(((dom D) \/ f) *))) is non empty set

fua is Relation-like (dom D) \/ f -defined ((dom D) \/ f) * -valued Element of K32(K33(((dom D) \/ f),(((dom D) \/ f) *)))

U1 is Element of (dom D) \/ f

D . U1 is set

A is Relation-like NAT -defined (dom D) \/ f -valued Function-like V30() FinSequence-like FinSubsequence-like Element of ((dom D) \/ f) *

[U1,A] is set

{U1,A} is non empty set

{U1} is non empty V5() V37(1) set

{{U1,A},{U1}} is non empty set

len A is V23() V24() V25() V29() V30() V35() V129() V130() V131() Element of NAT

fua is Relation-like (dom D) \/ f -defined ((dom D) \/ f) * -valued Element of K32(K33(((dom D) \/ f),(((dom D) \/ f) *)))

U1 is Relation-like (dom D) \/ f -defined ((dom D) \/ f) * -valued Element of K32(K33(((dom D) \/ f),(((dom D) \/ f) *)))

A is set

c1 is set

[A,c1] is set

{A,c1} is non empty set

{A} is non empty V5() V37(1) set

{{A,c1},{A}} is non empty set

cf is Element of (dom D) \/ f

F is Relation-like NAT -defined (dom D) \/ f -valued Function-like V30() FinSequence-like FinSubsequence-like Element of ((dom D) \/ f) *

[cf,F] is set

{cf,F} is non empty set

{cf} is non empty V5() V37(1) set

{{cf,F},{cf}} is non empty set

D . cf is set

len F is V23() V24() V25() V29() V30() V35() V129() V130() V131() Element of NAT

cf is Element of (dom D) \/ f

F is Relation-like NAT -defined (dom D) \/ f -valued Function-like V30() FinSequence-like FinSubsequence-like Element of ((dom D) \/ f) *

[cf,F] is set

{cf,F} is non empty set

{cf} is non empty V5() V37(1) set

{{cf,F},{cf}} is non empty set

D . cf is set

len F is V23() V24() V25() V29() V30() V35() V129() V130() V131() Element of NAT

D is non empty Relation-like NAT -defined NAT -valued Function-like V30() FinSequence-like FinSubsequence-like FinSequence of NAT

dom D is non empty Element of K32(NAT)

f is set

(dom D) \/ f is non empty set

(D,f) is Relation-like (dom D) \/ f -defined ((dom D) \/ f) * -valued Element of K32(K33(((dom D) \/ f),(((dom D) \/ f) *)))

((dom D) \/ f) * is non empty functional FinSequence-membered FinSequenceSet of (dom D) \/ f

K33(((dom D) \/ f),(((dom D) \/ f) *)) is non empty Relation-like set

K32(K33(((dom D) \/ f),(((dom D) \/ f) *))) is non empty set

DTConstrStr(# ((dom D) \/ f),(D,f) #) is non empty strict DTConstrStr

D is non empty Relation-like NAT -defined NAT -valued Function-like V30() FinSequence-like FinSubsequence-like FinSequence of NAT

f is set

(D,f) is strict DTConstrStr

dom D is non empty Element of K32(NAT)

(dom D) \/ f is non empty set

(D,f) is Relation-like (dom D) \/ f -defined ((dom D) \/ f) * -valued Element of K32(K33(((dom D) \/ f),(((dom D) \/ f) *)))

((dom D) \/ f) * is non empty functional FinSequence-membered FinSequenceSet of (dom D) \/ f

K33(((dom D) \/ f),(((dom D) \/ f) *)) is non empty Relation-like set

K32(K33(((dom D) \/ f),(((dom D) \/ f) *))) is non empty set

DTConstrStr(# ((dom D) \/ f),(D,f) #) is non empty strict DTConstrStr

D is non empty Relation-like NAT -defined NAT -valued Function-like V30() FinSequence-like FinSubsequence-like FinSequence of NAT

dom D is non empty Element of K32(NAT)

f is set

(D,f) is non empty strict DTConstrStr

(dom D) \/ f is non empty set

(D,f) is Relation-like (dom D) \/ f -defined ((dom D) \/ f) * -valued Element of K32(K33(((dom D) \/ f),(((dom D) \/ f) *)))

((dom D) \/ f) * is non empty functional FinSequence-membered FinSequenceSet of (dom D) \/ f

K33(((dom D) \/ f),(((dom D) \/ f) *)) is non empty Relation-like set

K32(K33(((dom D) \/ f),(((dom D) \/ f) *))) is non empty set

DTConstrStr(# ((dom D) \/ f),(D,f) #) is non empty strict DTConstrStr

Terminals (D,f) is set

NonTerminals (D,f) is set

the carrier of (D,f) is non empty set

(Terminals (D,f)) \/ (NonTerminals (D,f)) is set

(Terminals (D,f)) /\ (NonTerminals (D,f)) is set

U1 is set

rng D is non empty set

D . U1 is set

cf is V23() V24() V25() V29() V30() V35() V129() V130() V131() Element of NAT

A is Element of (dom D) \/ f

cf |-> A is Relation-like NAT -defined (dom D) \/ f -valued Function-like V30() V37(cf) FinSequence-like FinSubsequence-like Element of cf -tuples_on ((dom D) \/ f)

cf -tuples_on ((dom D) \/ f) is non empty functional FinSequence-membered FinSequenceSet of (dom D) \/ f

{ b

Seg cf is V30() V37(cf) Element of K32(NAT)

(Seg cf) --> A is Relation-like Seg cf -defined {A} -valued Function-like quasi_total V30() FinSequence-like FinSubsequence-like Element of K32(K33((Seg cf),{A}))

{A} is non empty V5() V37(1) set

K33((Seg cf),{A}) is Relation-like set

K32(K33((Seg cf),{A})) is non empty set

F is Relation-like NAT -defined (dom D) \/ f -valued Function-like V30() FinSequence-like FinSubsequence-like FinSequence of (dom D) \/ f

ff is Relation-like NAT -defined (dom D) \/ f -valued Function-like V30() FinSequence-like FinSubsequence-like Element of ((dom D) \/ f) *

len ff is V23() V24() V25() V29() V30() V35() V129() V130() V131() Element of NAT

D . A is set

[A,ff] is set

{A,ff} is non empty set

{{A,ff},{A}} is non empty set

c1 is Element of the carrier of (D,f)

{ b

U1 is set

{ b

A is Element of the carrier of (D,f)

c1 is Relation-like NAT -defined Function-like V30() FinSequence-like FinSubsequence-like set

c1 is Relation-like NAT -defined Function-like V30() FinSequence-like FinSubsequence-like set

[A,c1] is set

{A,c1} is non empty set

{A} is non empty V5() V37(1) set

{{A,c1},{A}} is non empty set

the Rules of (D,f) is Relation-like the carrier of (D,f) -defined the carrier of (D,f) * -valued Element of K32(K33( the carrier of (D,f),( the carrier of (D,f) *)))

the carrier of (D,f) * is non empty functional FinSequence-membered FinSequenceSet of the carrier of (D,f)

K33( the carrier of (D,f),( the carrier of (D,f) *)) is non empty Relation-like set

K32(K33( the carrier of (D,f),( the carrier of (D,f) *))) is non empty set

F is Element of (dom D) \/ f

cf is Relation-like NAT -defined (dom D) \/ f -valued Function-like V30() FinSequence-like FinSubsequence-like Element of ((dom D) \/ f) *

[F,cf] is set

{F,cf} is non empty set

{F} is non empty V5() V37(1) set

{{F,cf},{F}} is non empty set

U1 is set

rng D is non empty set

D . U1 is set

c1 is V23() V24() V25() V29() V30() V35() V129() V130() V131() Element of NAT

cf is Element of (dom D) \/ f

c1 |-> cf is Relation-like NAT -defined (dom D) \/ f -valued Function-like V30() V37(c1) FinSequence-like FinSubsequence-like Element of c1 -tuples_on ((dom D) \/ f)

c1 -tuples_on ((dom D) \/ f) is non empty functional FinSequence-membered FinSequenceSet of (dom D) \/ f

{ b

Seg c1 is V30() V37(c1) Element of K32(NAT)

(Seg c1) --> cf is Relation-like Seg c1 -defined {cf} -valued Function-like quasi_total V30() FinSequence-like FinSubsequence-like Element of K32(K33((Seg c1),{cf}))

{cf} is non empty V5() V37(1) set

K33((Seg c1),{cf}) is Relation-like set

K32(K33((Seg c1),{cf})) is non empty set

F is Relation-like NAT -defined (dom D) \/ f -valued Function-like V30() FinSequence-like FinSubsequence-like FinSequence of (dom D) \/ f

ff is Relation-like NAT -defined (dom D) \/ f -valued Function-like V30() FinSequence-like FinSubsequence-like Element of ((dom D) \/ f) *

len ff is V23() V24() V25() V29() V30() V35() V129() V130() V131() Element of NAT

D . cf is set

[cf,ff] is set

{cf,ff} is non empty set

{{cf,ff},{cf}} is non empty set

A is Element of the carrier of (D,f)

{ b

D is non empty Relation-like NAT -defined NAT -valued Function-like V30() FinSequence-like FinSubsequence-like FinSequence of NAT

f is () set

(D,f) is non empty strict DTConstrStr

dom D is non empty Element of K32(NAT)

(dom D) \/ f is non empty set

(D,f) is Relation-like (dom D) \/ f -defined ((dom D) \/ f) * -valued Element of K32(K33(((dom D) \/ f),(((dom D) \/ f) *)))

((dom D) \/ f) * is non empty functional FinSequence-membered FinSequenceSet of (dom D) \/ f

K33(((dom D) \/ f),(((dom D) \/ f) *)) is non empty Relation-like set

K32(K33(((dom D) \/ f),(((dom D) \/ f) *))) is non empty set

DTConstrStr(# ((dom D) \/ f),(D,f) #) is non empty strict DTConstrStr

Terminals (D,f) is set

fua is set

NonTerminals (D,f) is set

the carrier of (D,f) is non empty set

(Terminals (D,f)) \/ (NonTerminals (D,f)) is set

D is non empty Relation-like NAT -defined NAT -valued Function-like V30() FinSequence-like FinSubsequence-like FinSequence of NAT

f is set

(D,f) is non empty strict DTConstrStr

dom D is non empty Element of K32(NAT)

(dom D) \/ f is non empty set

(D,f) is Relation-like (dom D) \/ f -defined ((dom D) \/ f) * -valued Element of K32(K33(((dom D) \/ f),(((dom D) \/ f) *)))

((dom D) \/ f) * is non empty functional FinSequence-membered FinSequenceSet of (dom D) \/ f

K33(((dom D) \/ f),(((dom D) \/ f) *)) is non empty Relation-like set

K32(K33(((dom D) \/ f),(((dom D) \/ f) *))) is non empty set

DTConstrStr(# ((dom D) \/ f),(D,f) #) is non empty strict DTConstrStr

NonTerminals (D,f) is set

D is non empty Relation-like non non-empty NAT -defined NAT -valued Function-like V30() FinSequence-like FinSubsequence-like FinSequence of NAT

f is set

(D,f) is non empty strict with_nonterminals DTConstrStr

dom D is non empty Element of K32(NAT)

(dom D) \/ f is non empty set

(D,f) is Relation-like (dom D) \/ f -defined ((dom D) \/ f) * -valued Element of K32(K33(((dom D) \/ f),(((dom D) \/ f) *)))

((dom D) \/ f) * is non empty functional FinSequence-membered FinSequenceSet of (dom D) \/ f

K33(((dom D) \/ f),(((dom D) \/ f) *)) is non empty Relation-like set

K32(K33(((dom D) \/ f),(((dom D) \/ f) *))) is non empty set

DTConstrStr(# ((dom D) \/ f),(D,f) #) is non empty strict DTConstrStr

TS (D,f) is functional constituted-DTrees Element of K32((FinTrees the carrier of (D,f)))

the carrier of (D,f) is non empty set

FinTrees the carrier of (D,f) is non empty functional constituted-DTrees DTree-set of the carrier of (D,f)

K32((FinTrees the carrier of (D,f))) is non empty set

<*> (TS (D,f)) is empty Relation-like non-empty empty-yielding NAT -defined TS (D,f) -valued Function-like one-to-one constant functional V23() V24() V25() V27() V28() V29() V30() V35() V37( {} ) FinSequence-like FinSubsequence-like FinSequence-membered constituted-Trees constituted-FinTrees constituted-DTrees Tree-yielding FinTree-yielding DTree-yielding with_common_domain V129() V130() V131() Element of (TS (D,f)) *

(TS (D,f)) * is non empty functional FinSequence-membered FinSequenceSet of TS (D,f)

A is Element of the carrier of (D,f)

NonTerminals (D,f) is set

NonTerminals (D,f) is non empty Element of K32( the carrier of (D,f))

K32( the carrier of (D,f)) is non empty set

rng D is non empty set

D . A is set

roots (<*> (TS (D,f))) is Relation-like NAT -defined Function-like V30() FinSequence-like FinSubsequence-like set

<*> ((dom D) \/ f) is empty Relation-like non-empty empty-yielding NAT -defined (dom D) \/ f -valued Function-like one-to-one constant functional V23() V24() V25() V27() V28() V29() V30() V35() V37( {} ) FinSequence-like FinSubsequence-like FinSequence-membered constituted-Trees constituted-FinTrees constituted-DTrees Tree-yielding FinTree-yielding DTree-yielding with_common_domain V129() V130() V131() Element of ((dom D) \/ f) *

ff is set

D . ff is set

c1 is V23() V24() V25() V29() V30() V35() V129() V130() V131() Element of NAT

ff is Element of the carrier of (D,f)

ff -tree (<*> (TS (D,f))) is Relation-like Function-like DecoratedTree-like set

c1 |-> (ff -tree (<*> (TS (D,f)))) is Relation-like NAT -defined Function-like V30() V37(c1) FinSequence-like FinSubsequence-like DTree-yielding set

Seg c1 is V30() V37(c1) Element of K32(NAT)

(Seg c1) --> (ff -tree (<*> (TS (D,f)))) is Relation-like Seg c1 -defined {(ff -tree (<*> (TS (D,f))))} -valued Function-like quasi_total V30() FinSequence-like FinSubsequence-like Element of K32(K33((Seg c1),{(ff -tree (<*> (TS (D,f))))}))

{(ff -tree (<*> (TS (D,f))))} is non empty V5() functional V37(1) set

K33((Seg c1),{(ff -tree (<*> (TS (D,f))))}) is Relation-like set

K32(K33((Seg c1),{(ff -tree (<*> (TS (D,f))))})) is non empty set

len (c1 |-> (ff -tree (<*> (TS (D,f))))) is V23() V24() V25() V29() V30() V35() V129() V130() V131() Element of NAT

F is Relation-like NAT -defined (dom D) \/ f -valued Function-like V30() FinSequence-like FinSubsequence-like Element of ((dom D) \/ f) *

len F is V23() V24() V25() V29() V30() V35() V129() V130() V131() Element of NAT

[ff,(roots (<*> (TS (D,f))))] is set

{ff,(roots (<*> (TS (D,f))))} is non empty set

{ff} is non empty V5() V37(1) set

{{ff,(roots (<*> (TS (D,f))))},{ff}} is non empty set

the Rules of (D,f) is Relation-like the carrier of (D,f) -defined the carrier of (D,f) * -valued Element of K32(K33( the carrier of (D,f),( the carrier of (D,f) *)))

the carrier of (D,f) * is non empty functional FinSequence-membered FinSequenceSet of the carrier of (D,f)

K33( the carrier of (D,f),( the carrier of (D,f) *)) is non empty Relation-like set

K32(K33( the carrier of (D,f),( the carrier of (D,f) *))) is non empty set

rng (c1 |-> (ff -tree (<*> (TS (D,f))))) is set

s is set

dom (c1 |-> (ff -tree (<*> (TS (D,f))))) is V37(c1) Element of K32(NAT)

Seg (len (c1 |-> (ff -tree (<*> (TS (D,f)))))) is V30() V37( len (c1 |-> (ff -tree (<*> (TS (D,f)))))) Element of K32(NAT)

o2 is V23() V24() V25() V29() V30() V35() V129() V130() V131() set

(c1 |-> (ff -tree (<*> (TS (D,f))))) . o2 is set

roots (c1 |-> (ff -tree (<*> (TS (D,f))))) is Relation-like NAT -defined Function-like V30() FinSequence-like FinSubsequence-like set

dom (roots (c1 |-> (ff -tree (<*> (TS (D,f)))))) is Element of K32(NAT)

dom (c1 |-> (ff -tree (<*> (TS (D,f))))) is V37(c1) Element of K32(NAT)

Seg (len (c1 |-> (ff -tree (<*> (TS (D,f)))))) is V30() V37( len (c1 |-> (ff -tree (<*> (TS (D,f)))))) Element of K32(NAT)

len (roots (c1 |-> (ff -tree (<*> (TS (D,f)))))) is V23() V24() V25() V29() V30() V35() V129() V130() V131() Element of NAT

s is Relation-like NAT -defined FinTrees the carrier of (D,f) -valued Function-like V30() FinSequence-like FinSubsequence-like FinSequence of TS (D,f)

roots s is Relation-like NAT -defined the carrier of (D,f) -valued Function-like V30() FinSequence-like FinSubsequence-like FinSequence of the carrier of (D,f)

o2 is Relation-like NAT -defined FinTrees the carrier of (D,f) -valued Function-like V30() FinSequence-like FinSubsequence-like DTree-yielding FinSequence of FinTrees the carrier of (D,f)

roots o2 is Relation-like NAT -defined the carrier of (D,f) -valued Function-like V30() FinSequence-like FinSubsequence-like FinSequence of the carrier of (D,f)

cf is Element of (dom D) \/ f

x is Relation-like NAT -defined (dom D) \/ f -valued Function-like V30() FinSequence-like FinSubsequence-like Element of ((dom D) \/ f) *

[cf,x] is set

{cf,x} is non empty set

{cf} is non empty V5() V37(1) set

{{cf,x},{cf}} is non empty set

D is non empty Relation-like NAT -defined NAT -valued Function-like V30() FinSequence-like FinSubsequence-like FinSequence of NAT

f is non empty () set

(D,f) is non empty strict with_nonterminals DTConstrStr

dom D is non empty Element of K32(NAT)

(dom D) \/ f is non empty set

(D,f) is Relation-like (dom D) \/ f -defined ((dom D) \/ f) * -valued Element of K32(K33(((dom D) \/ f),(((dom D) \/ f) *)))

((dom D) \/ f) * is non empty functional FinSequence-membered FinSequenceSet of (dom D) \/ f

K33(((dom D) \/ f),(((dom D) \/ f) *)) is non empty Relation-like set

K32(K33(((dom D) \/ f),(((dom D) \/ f) *))) is non empty set

DTConstrStr(# ((dom D) \/ f),(D,f) #) is non empty strict DTConstrStr

NonTerminals (D,f) is non empty Element of K32( the carrier of (D,f))

the carrier of (D,f) is non empty set

K32( the carrier of (D,f)) is non empty set

Terminals (D,f) is set

the Element of f is Element of f

U1 is Element of the carrier of (D,f)

NonTerminals (D,f) is set

FinTrees the carrier of (D,f) is non empty functional constituted-DTrees DTree-set of the carrier of (D,f)

TS (D,f) is functional constituted-DTrees Element of K32((FinTrees the carrier of (D,f)))

K32((FinTrees the carrier of (D,f))) is non empty set

rng D is non empty set

D . U1 is set

c1 is V23() V24() V25() V29() V30() V35() V129() V130() V131() Element of NAT

A is Element of the carrier of (D,f)

root-tree A is Relation-like the carrier of (D,f) -valued Function-like DecoratedTree-like Element of FinTrees the carrier of (D,f)

c1 |-> (root-tree A) is Relation-like NAT -defined FinTrees the carrier of (D,f) -valued Function-like V30() V37(c1) FinSequence-like FinSubsequence-like DTree-yielding Element of c1 -tuples_on (FinTrees the carrier of (D,f))

c1 -tuples_on (FinTrees the carrier of (D,f)) is non empty functional FinSequence-membered FinSequenceSet of FinTrees the carrier of (D,f)

(FinTrees the carrier of (D,f)) * is non empty functional FinSequence-membered FinSequenceSet of FinTrees the carrier of (D,f)

{ b

Seg c1 is V30() V37(c1) Element of K32(NAT)

(Seg c1) --> (root-tree A) is Relation-like Seg c1 -defined {(root-tree A)} -valued Function-like quasi_total V30() FinSequence-like FinSubsequence-like Element of K32(K33((Seg c1),{(root-tree A)}))

{(root-tree A)} is non empty V5() functional V37(1) set

K33((Seg c1),{(root-tree A)}) is Relation-like set

K32(K33((Seg c1),{(root-tree A)})) is non empty set

len (c1 |-> (root-tree A)) is V23() V24() V25() V29() V30() V35() V129() V130() V131() Element of NAT

rng (c1 |-> (root-tree A)) is set

ff is set

dom (c1 |-> (root-tree A)) is V37(c1) Element of K32(NAT)

ff is V23() V24() V25() V29() V30() V35() V129() V130() V131() set

(c1 |-> (root-tree A)) . ff is Relation-like Function-like set

Seg (len (c1 |-> (root-tree A))) is V30() V37( len (c1 |-> (root-tree A))) Element of K32(NAT)

roots (c1 |-> (root-tree A)) is Relation-like NAT -defined the carrier of (D,f) -valued Function-like V30() FinSequence-like FinSubsequence-like FinSequence of the carrier of (D,f)

dom (roots (c1 |-> (root-tree A))) is Element of K32(NAT)

dom (c1 |-> (root-tree A)) is V37(c1) Element of K32(NAT)

Seg (len (c1 |-> (root-tree A))) is V30() V37( len (c1 |-> (root-tree A))) Element of K32(NAT)

len (roots (c1 |-> (root-tree A))) is V23() V24() V25() V29() V30() V35() V129() V130() V131() Element of NAT

ff is Relation-like NAT -defined FinTrees the carrier of (D,f) -valued Function-like V30() FinSequence-like FinSubsequence-like FinSequence of TS (D,f)

roots ff is Relation-like NAT -defined the carrier of (D,f) -valued Function-like V30() FinSequence-like FinSubsequence-like FinSequence of the carrier of (D,f)

ff is Relation-like NAT -defined FinTrees the carrier of (D,f) -valued Function-like V30() FinSequence-like FinSubsequence-like DTree-yielding FinSequence of FinTrees the carrier of (D,f)

roots ff is Relation-like NAT -defined the carrier of (D,f) -valued Function-like V30() FinSequence-like FinSubsequence-like FinSequence of the carrier of (D,f)

cf is Element of (dom D) \/ f

x is Relation-like NAT -defined (dom D) \/ f -valued Function-like V30() FinSequence-like FinSubsequence-like Element of ((dom D) \/ f) *

[cf,x] is set

{cf,x} is non empty set

{cf} is non empty V5() V37(1) set

{{cf,x},{cf}} is non empty set

c

D is non empty Relation-like NAT -defined NAT -valued Function-like V30() FinSequence-like FinSubsequence-like FinSequence of NAT

dom D is non empty Element of K32(NAT)

f is set

(D,f) is non empty strict with_nonterminals DTConstrStr

(dom D) \/ f is non empty set

(D,f) is Relation-like (dom D) \/ f -defined ((dom D) \/ f) * -valued Element of K32(K33(((dom D) \/ f),(((dom D) \/ f) *)))

((dom D) \/ f) * is non empty functional FinSequence-membered FinSequenceSet of (dom D) \/ f

K33(((dom D) \/ f),(((dom D) \/ f) *)) is non empty Relation-like set

K32(K33(((dom D) \/ f),(((dom D) \/ f) *))) is non empty set

DTConstrStr(# ((dom D) \/ f),(D,f) #) is non empty strict DTConstrStr

the carrier of (D,f) is non empty set

c

D is non empty Relation-like NAT -defined NAT -valued Function-like V30() FinSequence-like FinSubsequence-like FinSequence of NAT

dom D is non empty Element of K32(NAT)

f is non empty () set

(D,f) is non empty strict with_terminals with_nonterminals with_useful_nonterminals DTConstrStr

(dom D) \/ f is non empty set

(D,f) is Relation-like (dom D) \/ f -defined ((dom D) \/ f) * -valued Element of K32(K33(((dom D) \/ f),(((dom D) \/ f) *)))

((dom D) \/ f) * is non empty functional FinSequence-membered FinSequenceSet of (dom D) \/ f

K33(((dom D) \/ f),(((dom D) \/ f) *)) is non empty Relation-like set

K32(K33(((dom D) \/ f),(((dom D) \/ f) *))) is non empty set

DTConstrStr(# ((dom D) \/ f),(D,f) #) is non empty strict DTConstrStr

TS (D,f) is non empty functional constituted-DTrees Element of K32((FinTrees the carrier of (D,f)))

the carrier of (D,f) is non empty set

FinTrees the carrier of (D,f) is non empty functional constituted-DTrees DTree-set of the carrier of (D,f)

K32((FinTrees the carrier of (D,f))) is non empty set

(TS (D,f)) * is non empty functional FinSequence-membered FinSequenceSet of TS (D,f)

K33(((TS (D,f)) *),(TS (D,f))) is non empty Relation-like set

K32(K33(((TS (D,f)) *),(TS (D,f)))) is non empty set

D /. c

(D /. c

{ b

(D,f,c

D . c

ff is set

ff is set

x is Relation-like NAT -defined TS (D,f) -valued Function-like V30() FinSequence-like FinSubsequence-like DTree-yielding Element of (TS (D,f)) *

len x is V23() V24() V25() V29() V30() V35() V129() V130() V131() Element of NAT

(D,f,c

s is Relation-like NAT -defined FinTrees the carrier of (D,f) -valued Function-like V30() FinSequence-like FinSubsequence-like DTree-yielding FinSequence of TS (D,f)

roots s is Relation-like NAT -defined the carrier of (D,f) -valued Function-like V30() FinSequence-like FinSubsequence-like FinSequence of the carrier of (D,f)

dom (roots s) is Element of K32(NAT)

dom s is Element of K32(NAT)

len (roots s) is V23() V24() V25() V29() V30() V35() V129() V130() V131() Element of NAT

Seg (len (roots s)) is V30() V37( len (roots s)) Element of K32(NAT)

o2 is Relation-like NAT -defined FinTrees the carrier of (D,f) -valued Function-like V30() FinSequence-like FinSubsequence-like DTree-yielding FinSequence of FinTrees the carrier of (D,f)

roots o2 is Relation-like NAT -defined the carrier of (D,f) -valued Function-like V30() FinSequence-like FinSubsequence-like FinSequence of the carrier of (D,f)

F is Element of (dom D) \/ f

x is Relation-like NAT -defined (dom D) \/ f -valued Function-like V30() FinSequence-like FinSubsequence-like Element of ((dom D) \/ f) *

[F,x] is set

{F,x} is non empty set

{F} is non empty V5() V37(1) set

{{F,x},{F}} is non empty set

F is set

ff is set

ff is set

x is Relation-like NAT -defined TS (D,f) -valued Function-like V30() FinSequence-like FinSubsequence-like DTree-yielding Element of (TS (D,f)) *

len x is V23() V24() V25() V29() V30() V35() V129() V130() V131() Element of NAT

(D,f,c

F is Relation-like (TS (D,f)) * -defined TS (D,f) -valued Function-like Element of K32(K33(((TS (D,f)) *),(TS (D,f))))

dom F is functional FinSequence-membered Element of K32(((TS (D,f)) *))

K32(((TS (D,f)) *)) is non empty set

ff is set

ff is set

ff is set

x is Relation-like NAT -defined TS (D,f) -valued Function-like V30() FinSequence-like FinSubsequence-like DTree-yielding Element of (TS (D,f)) *

len x is V23() V24() V25() V29() V30() V35() V129() V130() V131() Element of NAT

ff is Element of the carrier of (D,f)

ff -tree x is Relation-like Function-like DecoratedTree-like set

s is Relation-like NAT -defined FinTrees the carrier of (D,f) -valued Function-like V30() FinSequence-like FinSubsequence-like DTree-yielding FinSequence of TS (D,f)

(D,f,c

ff is Relation-like NAT -defined FinTrees the carrier of (D,f) -valued Function-like V30() FinSequence-like FinSubsequence-like DTree-yielding FinSequence of TS (D,f)

len ff is V23() V24() V25() V29() V30() V35() V129() V130() V131() Element of NAT

ff is Relation-like NAT -defined FinTrees the carrier of (D,f) -valued Function-like V30() FinSequence-like FinSubsequence-like DTree-yielding FinSequence of TS (D,f)

len ff is V23() V24() V25() V29() V30() V35() V129() V130() V131() Element of NAT

x is Relation-like NAT -defined TS (D,f) -valued Function-like V30() FinSequence-like FinSubsequence-like DTree-yielding Element of (TS (D,f)) *

s is Relation-like NAT -defined TS (D,f) -valued Function-like V30() FinSequence-like FinSubsequence-like DTree-yielding Element of (TS (D,f)) *

len s is V23() V24() V25() V29() V30() V35() V129() V130() V131() Element of NAT

the Relation-like NAT -defined TS (D,f) -valued Function-like V30() V37(D /. c

ff is Relation-like NAT -defined Function-like V30() FinSequence-like FinSubsequence-like set

ff is Relation-like NAT -defined Function-like V30() FinSequence-like FinSubsequence-like set

len ff is V23() V24() V25() V29() V30() V35() V129() V130() V131() Element of NAT

len ff is V23() V24() V25() V29() V30() V35() V129() V130() V131() Element of NAT

x is Relation-like NAT -defined TS (D,f) -valued Function-like V30() FinSequence-like FinSubsequence-like DTree-yielding Element of (TS (D,f)) *

len x is V23() V24() V25() V29() V30() V35() V129() V130() V131() Element of NAT

s is Relation-like NAT -defined TS (D,f) -valued Function-like V30() FinSequence-like FinSubsequence-like DTree-yielding Element of (TS (D,f)) *

len s is V23() V24() V25() V29() V30() V35() V129() V130() V131() Element of NAT

ff is Relation-like NAT -defined Function-like V30() FinSequence-like FinSubsequence-like set

ff is non empty Relation-like (TS (D,f)) * -defined TS (D,f) -valued Function-like homogeneous quasi_total Element of K32(K33(((TS (D,f)) *),(TS (D,f))))

dom ff is non empty functional FinSequence-membered with_common_domain Element of K32(((TS (D,f)) *))

ff is Relation-like NAT -defined FinTrees the carrier of (D,f) -valued Function-like V30() FinSequence-like FinSubsequence-like DTree-yielding FinSequence of TS (D,f)

ff . ff is Relation-like Function-like set

(D,f,c

U1 is non empty Relation-like (TS (D,f)) * -defined TS (D,f) -valued Function-like homogeneous quasi_total Element of K32(K33(((TS (D,f)) *),(TS (D,f))))

dom U1 is non empty functional FinSequence-membered with_common_domain Element of K32(((TS (D,f)) *))

K32(((TS (D,f)) *)) is non empty set

A is non empty Relation-like (TS (D,f)) * -defined TS (D,f) -valued Function-like homogeneous quasi_total Element of K32(K33(((TS (D,f)) *),(TS (D,f))))

dom A is non empty functional FinSequence-membered with_common_domain Element of K32(((TS (D,f)) *))

c1 is set

cf is Relation-like NAT -defined TS (D,f) -valued Function-like V30() FinSequence-like FinSubsequence-like DTree-yielding Element of (TS (D,f)) *

len cf is V23() V24() V25() V29() V30() V35() V129() V130() V131() Element of NAT

U1 . cf is Relation-like Function-like set

(D,f,c

U1 . c1 is Relation-like Function-like set

A . c1 is Relation-like Function-like set

D is non empty Relation-like NAT -defined NAT -valued Function-like V30() FinSequence-like FinSubsequence-like FinSequence of NAT

f is non empty () set

(D,f) is non empty strict with_terminals with_nonterminals with_useful_nonterminals DTConstrStr

dom D is non empty Element of K32(NAT)

(dom D) \/ f is non empty set

(D,f) is Relation-like (dom D) \/ f -defined ((dom D) \/ f) * -valued Element of K32(K33(((dom D) \/ f),(((dom D) \/ f) *)))

((dom D) \/ f) * is non empty functional FinSequence-membered FinSequenceSet of (dom D) \/ f

K33(((dom D) \/ f),(((dom D) \/ f) *)) is non empty Relation-like set

K32(K33(((dom D) \/ f),(((dom D) \/ f) *))) is non empty set

DTConstrStr(# ((dom D) \/ f),(D,f) #) is non empty strict DTConstrStr

TS (D,f) is non empty functional constituted-DTrees Element of K32((FinTrees the carrier of (D,f)))

the carrier of (D,f) is non empty set

FinTrees the carrier of (D,f) is non empty functional constituted-DTrees DTree-set of the carrier of (D,f)

K32((FinTrees the carrier of (D,f))) is non empty set

(TS (D,f)) * is non empty functional FinSequence-membered FinSequenceSet of TS (D,f)

PFuncs (((TS (D,f)) *),(TS (D,f))) is non empty functional set

len D is non empty V23() V24() V25() V29() V30() V35() V129() V130() V131() Element of NAT

Seg (len D) is non empty V30() V37( len D) Element of K32(NAT)

fua is V23() V24() V25() V29() V30() V35() V129() V130() V131() set

(D,f,fua) is non empty Relation-like (TS (D,f)) * -defined TS (D,f) -valued Function-like homogeneous quasi_total Element of K32(K33(((TS (D,f)) *),(TS (D,f))))

K33(((TS (D,f)) *),(TS (D,f))) is non empty Relation-like set

K32(K33(((TS (D,f)) *),(TS (D,f)))) is non empty set

U1 is Relation-like Function-like Element of PFuncs (((TS (D,f)) *),(TS (D,f)))

fua is Relation-like NAT -defined PFuncs (((TS (D,f)) *),(TS (D,f))) -valued Function-like V30() FinSequence-like FinSubsequence-like FinSequence of PFuncs (((TS (D,f)) *),(TS (D,f)))

dom fua is Element of K32(NAT)

U1 is Relation-like NAT -defined PFuncs (((TS (D,f)) *),(TS (D,f))) -valued Function-like V30() FinSequence-like FinSubsequence-like FinSequence of PFuncs (((TS (D,f)) *),(TS (D,f)))

len U1 is V23() V24() V25() V29() V30() V35() V129() V130() V131() Element of NAT

dom U1 is Element of K32(NAT)

A is V23() V24() V25() V29() V30() V35() V129() V130() V131() Element of NAT

U1 . A is Relation-like Function-like set

(D,f,A) is non empty Relation-like (TS (D,f)) * -defined TS (D,f) -valued Function-like homogeneous quasi_total Element of K32(K33(((TS (D,f)) *),(TS (D,f))))

K33(((TS (D,f)) *),(TS (D,f))) is non empty Relation-like set

K32(K33(((TS (D,f)) *),(TS (D,f)))) is non empty set

c

len c

dom c

fua is Relation-like NAT -defined PFuncs (((TS (D,f)) *),(TS (D,f))) -valued Function-like V30() FinSequence-like FinSubsequence-like FinSequence of PFuncs (((TS (D,f)) *),(TS (D,f)))

len fua is V23() V24() V25() V29() V30() V35() V129() V130() V131() Element of NAT

dom fua is Element of K32(NAT)

U1 is V23() V24() V25() V29() V30() V35() V129() V130() V131() set

c

fua . U1 is Relation-like Function-like set

Seg (len c

Seg (len fua) is V30() V37( len fua) Element of K32(NAT)

(D,f,U1) is non empty Relation-like (TS (D,f)) * -defined TS (D,f) -valued Function-like homogeneous quasi_total Element of K32(K33(((TS (D,f)) *),(TS (D,f))))

K33(((TS (D,f)) *),(TS (D,f))) is non empty Relation-like set

K32(K33(((TS (D,f)) *),(TS (D,f)))) is non empty set

D is non empty Relation-like NAT -defined NAT -valued Function-like V30() FinSequence-like FinSubsequence-like FinSequence of NAT

f is non empty () set

(D,f) is non empty strict with_terminals with_nonterminals with_useful_nonterminals DTConstrStr

dom D is non empty Element of K32(NAT)

(dom D) \/ f is non empty set

(D,f) is Relation-like (dom D) \/ f -defined ((dom D) \/ f) * -valued Element of K32(K33(((dom D) \/ f),(((dom D) \/ f) *)))

((dom D) \/ f) * is non empty functional FinSequence-membered FinSequenceSet of (dom D) \/ f

K33(((dom D) \/ f),(((dom D) \/ f) *)) is non empty Relation-like set

K32(K33(((dom D) \/ f),(((dom D) \/ f) *))) is non empty set

DTConstrStr(# ((dom D) \/ f),(D,f) #) is non empty strict DTConstrStr

TS (D,f) is non empty functional constituted-DTrees Element of K32((FinTrees the carrier of (D,f)))

the carrier of (D,f) is non empty set

FinTrees the carrier of (D,f) is non empty functional constituted-DTrees DTree-set of the carrier of (D,f)

K32((FinTrees the carrier of (D,f))) is non empty set

(D,f) is Relation-like NAT -defined PFuncs (((TS (D,f)) *),(TS (D,f))) -valued Function-like V30() FinSequence-like FinSubsequence-like FinSequence of PFuncs (((TS (D,f)) *),(TS (D,f)))

(TS (D,f)) * is non empty functional FinSequence-membered FinSequenceSet of TS (D,f)

PFuncs (((TS (D,f)) *),(TS (D,f))) is non empty functional set

UAStr(# (TS (D,f)),(D,f) #) is strict UAStr

K33(((TS (D,f)) *),(TS (D,f))) is non empty Relation-like set

K32(K33(((TS (D,f)) *),(TS (D,f)))) is non empty set

the charact of UAStr(# (TS (D,f)),(D,f) #) is Relation-like NAT -defined PFuncs (( the carrier of UAStr(# (TS (D,f)),(D,f) #) *), the carrier of UAStr(# (TS (D,f)),(D,f) #)) -valued Function-like V30() FinSequence-like FinSubsequence-like FinSequence of PFuncs (( the carrier of UAStr(# (TS (D,f)),(D,f) #) *), the carrier of UAStr(# (TS (D,f)),(D,f) #))

the carrier of UAStr(# (TS (D,f)),(D,f) #) is set

the carrier of UAStr(# (TS (D,f)),(D,f) #) * is non empty functional FinSequence-membered FinSequenceSet of the carrier of UAStr(# (TS (D,f)),(D,f) #)

PFuncs (( the carrier of UAStr(# (TS (D,f)),(D,f) #) *), the carrier of UAStr(# (TS (D,f)),(D,f) #)) is non empty functional set

dom the charact of UAStr(# (TS (D,f)),(D,f) #) is Element of K32(NAT)

U1 is V23() V24() V25() V29() V30() V35() V129() V130() V131() set

the charact of UAStr(# (TS (D,f)),(D,f) #) . U1 is Relation-like Function-like set

A is Relation-like (TS (D,f)) * -defined TS (D,f) -valued Function-like Element of K32(K33(((TS (D,f)) *),(TS (D,f))))

(D,f,U1) is non empty Relation-like (TS (D,f)) * -defined TS (D,f) -valued Function-like homogeneous quasi_total Element of K32(K33(((TS (D,f)) *),(TS (D,f))))

U1 is V23() V24() V25() V29() V30() V35() V129() V130() V131() set

the charact of UAStr(# (TS (D,f)),(D,f) #) . U1 is Relation-like Function-like set

A is Relation-like (TS (D,f)) * -defined TS (D,f) -valued Function-like Element of K32(K33(((TS (D,f)) *),(TS (D,f))))

(D,f,U1) is non empty Relation-like (TS (D,f)) * -defined TS (D,f) -valued Function-like homogeneous quasi_total Element of K32(K33(((TS (D,f)) *),(TS (D,f))))

U1 is set

the charact of UAStr(# (TS (D,f)),(D,f) #) . U1 is Relation-like Function-like set

A is V23() V24() V25() V29() V30() V35() V129() V130() V131() Element of NAT

the charact of UAStr(# (TS (D,f)),(D,f) #) . A is Relation-like Function-like set

(D,f,A) is non empty Relation-like (TS (D,f)) * -defined TS (D,f) -valued Function-like homogeneous quasi_total Element of K32(K33(((TS (D,f)) *),(TS (D,f))))

len (D,f) is V23() V24() V25() V29() V30() V35() V129() V130() V131() Element of NAT

len D is non empty V23() V24() V25() V29() V30() V35() V129() V130() V131() Element of NAT

D is non empty Relation-like NAT -defined NAT -valued Function-like V30() FinSequence-like FinSubsequence-like FinSequence of NAT

f is non empty () set

(D,f) is non empty strict V109() quasi_total non-empty UAStr

(D,f) is non empty strict with_terminals with_nonterminals with_useful_nonterminals DTConstrStr

dom D is non empty Element of K32(NAT)

(dom D) \/ f is non empty set

(D,f) is Relation-like (dom D) \/ f -defined ((dom D) \/ f) * -valued Element of K32(K33(((dom D) \/ f),(((dom D) \/ f) *)))

((dom D) \/ f) * is non empty functional FinSequence-membered FinSequenceSet of (dom D) \/ f

K33(((dom D) \/ f),(((dom D) \/ f) *)) is non empty Relation-like set

K32(K33(((dom D) \/ f),(((dom D) \/ f) *))) is non empty set

DTConstrStr(# ((dom D) \/ f),(D,f) #) is non empty strict DTConstrStr

TS (D,f) is non empty functional constituted-DTrees Element of K32((FinTrees the carrier of (D,f)))

the carrier of (D,f) is non empty set

FinTrees the carrier of (D,f) is non empty functional constituted-DTrees DTree-set of the carrier of (D,f)

K32((FinTrees the carrier of (D,f))) is non empty set

(D,f) is Relation-like NAT -defined PFuncs (((TS (D,f)) *),(TS (D,f))) -valued Function-like V30() FinSequence-like FinSubsequence-like FinSequence of PFuncs (((TS (D,f)) *),(TS (D,f)))

(TS (D,f)) * is non empty functional FinSequence-membered FinSequenceSet of TS (D,f)

PFuncs (((TS (D,f)) *),(TS (D,f))) is non empty functional set

UAStr(# (TS (D,f)),(D,f) #) is strict UAStr

signature (D,f) is Relation-like NAT -defined NAT -valued Function-like V30() FinSequence-like FinSubsequence-like FinSequence of NAT

the charact of (D,f) is Relation-like NAT -defined PFuncs (( the carrier of (D,f) *), the carrier of (D,f)) -valued Function-like V30() FinSequence-like FinSubsequence-like FinSequence of PFuncs (( the carrier of (D,f) *), the carrier of (D,f))

the carrier of (D,f) is non empty set

the carrier of (D,f) * is non empty functional FinSequence-membered FinSequenceSet of the carrier of (D,f)

PFuncs (( the carrier of (D,f) *), the carrier of (D,f)) is non empty functional set

len the charact of (D,f) is V23() V24() V25() V29() V30() V35() V129() V130() V131() Element of NAT

len D is non empty V23() V24() V25() V29() V30() V35() V129() V130() V131() Element of NAT

len (signature (D,f)) is V23() V24() V25() V29() V30() V35() V129() V130() V131() Element of NAT

dom (signature (D,f)) is Element of K32(NAT)

Seg (len D) is non empty V30() V37( len D) Element of K32(NAT)

K33(( the carrier of (D,f) *), the carrier of (D,f)) is non empty Relation-like set

K32(K33(( the carrier of (D,f) *), the carrier of (D,f))) is non empty set

U1 is V23() V24() V25() V29() V30() V35() V129() V130() V131() set

(D,f,U1) is non empty Relation-like (TS (D,f)) * -defined TS (D,f) -valued Function-like homogeneous quasi_total Element of K32(K33(((TS (D,f)) *),(TS (D,f))))

K33(((TS (D,f)) *),(TS (D,f))) is non empty Relation-like set

K32(K33(((TS (D,f)) *),(TS (D,f)))) is non empty set

A is non empty Relation-like the carrier of (D,f) * -defined the carrier of (D,f) -valued Function-like homogeneous quasi_total Element of K32(K33(( the carrier of (D,f) *), the carrier of (D,f)))

dom A is non empty functional FinSequence-membered with_common_domain Element of K32(( the carrier of (D,f) *))

K32(( the carrier of (D,f) *)) is non empty set

arity A is V23() V24() V25() V29() V30() V35() V129() V130() V131() Element of NAT

(arity A) -tuples_on the carrier of (D,f) is non empty functional FinSequence-membered FinSequenceSet of the carrier of (D,f)

{ b

D /. U1 is V23() V24() V25() V29() V30() V35() V129() V130() V131() Element of NAT

(D /. U1) -tuples_on (TS (D,f)) is non empty functional FinSequence-membered FinSequenceSet of TS (D,f)

{ b

dom (D,f) is Element of K32(NAT)

the charact of (D,f) . U1 is Relation-like Function-like set

(signature (D,f)) . U1 is set

D . U1 is set

D is non empty Relation-like NAT -defined NAT -valued Function-like V30() FinSequence-like FinSubsequence-like FinSequence of NAT

f is non empty () set

(D,f) is non empty strict with_terminals with_nonterminals with_useful_nonterminals DTConstrStr

dom D is non empty Element of K32(NAT)

(dom D) \/ f is non empty set

(D,f) is Relation-like (dom D) \/ f -defined ((dom D) \/ f) * -valued Element of K32(K33(((dom D) \/ f),(((dom D) \/ f) *)))

((dom D) \/ f) * is non empty functional FinSequence-membered FinSequenceSet of (dom D) \/ f

K33(((dom D) \/ f),(((dom D) \/ f) *)) is non empty Relation-like set

K32(K33(((dom D) \/ f),(((dom D) \/ f) *))) is non empty set

DTConstrStr(# ((dom D) \/ f),(D,f) #) is non empty strict DTConstrStr

the carrier of (D,f) is non empty set

Terminals (D,f) is non empty Element of K32( the carrier of (D,f))

K32( the carrier of (D,f)) is non empty set

{ (root-tree b

(D,f) is non empty strict V109() quasi_total non-empty UAStr

TS (D,f) is non empty functional constituted-DTrees Element of K32((FinTrees the carrier of (D,f)))

FinTrees the carrier of (D,f) is non empty functional constituted-DTrees DTree-set of the carrier of (D,f)

K32((FinTrees the carrier of (D,f))) is non empty set

(D,f) is Relation-like NAT -defined PFuncs (((TS (D,f)) *),(TS (D,f))) -valued Function-like V30() FinSequence-like FinSubsequence-like FinSequence of PFuncs (((TS (D,f)) *),(TS (D,f)))

(TS (D,f)) * is non empty functional FinSequence-membered FinSequenceSet of TS (D,f)

PFuncs (((TS (D,f)) *),(TS (D,f))) is non empty functional set

UAStr(# (TS (D,f)),(D,f) #) is strict UAStr

the carrier of (D,f) is non empty set

K32( the carrier of (D,f)) is non empty set

U1 is set

A is Element of the carrier of (D,f)

root-tree A is Relation-like the carrier of (D,f) -valued Function-like DecoratedTree-like Element of FinTrees the carrier of (D,f)

D is non empty Relation-like NAT -defined NAT -valued Function-like V30() FinSequence-like FinSubsequence-like FinSequence of NAT

f is non empty () set

(D,f) is Element of K32( the carrier of (D,f))

(D,f) is non empty strict V109() quasi_total non-empty UAStr

(D,f) is non empty strict with_terminals with_nonterminals with_useful_nonterminals DTConstrStr

dom D is non empty Element of K32(NAT)

(dom D) \/ f is non empty set

(D,f) is Relation-like (dom D) \/ f -defined ((dom D) \/ f) * -valued Element of K32(K33(((dom D) \/ f),(((dom D) \/ f) *)))

((dom D) \/ f) * is non empty functional FinSequence-membered FinSequenceSet of (dom D) \/ f

K33(((dom D) \/ f),(((dom D) \/ f) *)) is non empty Relation-like set

K32(K33(((dom D) \/ f),(((dom D) \/ f) *))) is non empty set

DTConstrStr(# ((dom D) \/ f),(D,f) #) is non empty strict DTConstrStr

TS (D,f) is non empty functional constituted-DTrees Element of K32((FinTrees the carrier of (D,f)))

the carrier of (D,f) is non empty set

FinTrees the carrier of (D,f) is non empty functional constituted-DTrees DTree-set of the carrier of (D,f)

K32((FinTrees the carrier of (D,f))) is non empty set

(D,f) is Relation-like NAT -defined PFuncs (((TS (D,f)) *),(TS (D,f))) -valued Function-like V30() FinSequence-like FinSubsequence-like FinSequence of PFuncs (((TS (D,f)) *),(TS (D,f)))

(TS (D,f)) * is non empty functional FinSequence-membered FinSequenceSet of TS (D,f)

PFuncs (((TS (D,f)) *),(TS (D,f))) is non empty functional set

UAStr(# (TS (D,f)),(D,f) #) is strict UAStr

the carrier of (D,f) is non empty set

K32( the carrier of (D,f)) is non empty set

Terminals (D,f) is non empty Element of K32( the carrier of (D,f))

K32( the carrier of (D,f)) is non empty set

{ (root-tree b

the Element of f is Element of f

U1 is Element of the carrier of (D,f)

root-tree U1 is Relation-like the carrier of (D,f) -valued Function-like DecoratedTree-like Element of FinTrees the carrier of (D,f)

D is non empty Relation-like NAT -defined NAT -valued Function-like V30() FinSequence-like FinSubsequence-like FinSequence of NAT

f is non empty () set

(D,f) is Element of K32( the carrier of (D,f))

(D,f) is non empty strict V109() quasi_total non-empty UAStr

(D,f) is non empty strict with_terminals with_nonterminals with_useful_nonterminals DTConstrStr

dom D is non empty Element of K32(NAT)

(dom D) \/ f is non