:: 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₃ is V23() V24() V25() V29() V30() V35() V129() V130() V131() Element of NAT
<*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₃ is Element of K32( the carrier of D)
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₁ where b₁ is Element of the carrier of D : ex b₂ being non empty Relation-like the carrier of D * -defined the carrier of D -valued Function-like homogeneous quasi_total Element of Operations D st
( arity b₂ = 0 & b₁ in rng b₂ ) } is set
f is Element of K32( the carrier of D)
c₃ is set
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₁ where b₁ is Relation-like NAT -defined the carrier of D -valued Function-like V30() FinSequence-like FinSubsequence-like Element of the carrier of D * : len b₁ = 0 } is set
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₁ where b₁ is Element of the carrier of D : ex b₂ being non empty Relation-like the carrier of D * -defined the carrier of D -valued Function-like homogeneous quasi_total Element of Operations D st
( arity b₂ = 0 & b₁ in rng b₂ ) } is set
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₃ is non empty Element of K32( the carrier of D)
c₃ is Element of K32( the carrier of D)
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₁ where b₁ is Element of the carrier of c1 : ex b₂ being non empty Relation-like the carrier of c1 * -defined the carrier of c1 -valued Function-like homogeneous quasi_total Element of Operations c1 st
( arity b₂ = 0 & b₁ in rng b₂ ) } is set
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₁ where b₁ is Relation-like NAT -defined the carrier of ff -valued Function-like V30() FinSequence-like FinSubsequence-like Element of the carrier of ff * : len b₁ = 0 } is set
{(<*> 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₁ where b₁ is Element of the carrier of D : ex b₂ being non empty Relation-like the carrier of D * -defined the carrier of D -valued Function-like homogeneous quasi_total Element of Operations D st
( arity b₂ = 0 & b₁ in rng b₂ ) } is set
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₁ where b₁ is Relation-like NAT -defined (dom D) \/ f -valued Function-like V30() FinSequence-like FinSubsequence-like Element of ((dom D) \/ f) * : len b₁ = cf } is set
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₁ where b₁ is Element of the carrier of (D,f) : ex b₂ being Relation-like NAT -defined Function-like V30() FinSequence-like FinSubsequence-like set st b₁ ==> b₂ } is set
U1 is set
{ b₁ where b₁ is Element of the carrier of (D,f) : ex b₂ being Relation-like NAT -defined Function-like V30() FinSequence-like FinSubsequence-like set st b₁ ==> b₂ } is set
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₁ where b₁ is Relation-like NAT -defined (dom D) \/ f -valued Function-like V30() FinSequence-like FinSubsequence-like Element of ((dom D) \/ f) * : len b₁ = c1 } is set
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₁ where b₁ is Element of the carrier of (D,f) : ex b₂ being Relation-like NAT -defined Function-like V30() FinSequence-like FinSubsequence-like set st b₁ ==> b₂ } 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
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₁ where b₁ is Relation-like NAT -defined FinTrees the carrier of (D,f) -valued Function-like V30() FinSequence-like FinSubsequence-like Element of (FinTrees the carrier of (D,f)) * : len b₁ = c1 } is set
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₃ is V23() V24() V25() V29() V30() V35() V129() V130() V131() 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
(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₃ is V23() V24() V25() V29() V30() V35() V129() V130() V131() 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 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₃ is V23() V24() V25() V29() V30() V35() V129() V130() V131() Element of NAT
(D /. c₃) -tuples_on (TS (D,f)) is non empty functional FinSequence-membered FinSequenceSet of TS (D,f)
{ b₁ where b₁ is Relation-like NAT -defined TS (D,f) -valued Function-like V30() FinSequence-like FinSubsequence-like Element of (TS (D,f)) * : len b₁ = D /. c₃ } is set
(D,f,c₃) is Element of the carrier of (D,f)
D . c₃ 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₃) -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)
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₃) -tree x is Relation-like Function-like DecoratedTree-like set
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₃) -tree s is Relation-like the carrier of (D,f) -valued Function-like DecoratedTree-like Element of FinTrees 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 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₃) FinSequence-like FinSubsequence-like DTree-yielding Element of (D /. c₃) -tuples_on (TS (D,f)) is Relation-like NAT -defined TS (D,f) -valued Function-like V30() V37(D /. c₃) FinSequence-like FinSubsequence-like DTree-yielding Element of (D /. c₃) -tuples_on (TS (D,f))
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₃) -tree ff is Relation-like the carrier of (D,f) -valued Function-like DecoratedTree-like Element of FinTrees the carrier of (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))))
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₃) -tree cf is Relation-like Function-like DecoratedTree-like set
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₃ 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 c₃ is V23() V24() V25() V29() V30() V35() V129() V130() V131() Element of NAT
dom c₃ is Element of K32(NAT)
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₃ . U1 is Relation-like Function-like set
fua . U1 is Relation-like Function-like set
Seg (len c₃) is V30() V37( len c₃) Element of K32(NAT)
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₁ where b₁ is Relation-like NAT -defined the carrier of (D,f) -valued Function-like V30() FinSequence-like FinSubsequence-like Element of the carrier of (D,f) * : len b₁ = arity A } is set
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₁ where b₁ is Relation-like NAT -defined TS (D,f) -valued Function-like V30() FinSequence-like FinSubsequence-like Element of (TS (D,f)) * : len b₁ = D /. U1 } is set
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₁) where b₁ is Element of the carrier of (D,f) : b₁ in Terminals (D,f) } is set
(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₁) where b₁ is Element of the carrier of (D,f) : b₁ in Terminals (D,f) } is set
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 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₁) where b₁ is Element of the carrier of (D,f) : b₁ in Terminals (D,f) } is set
GenUnivAlg (D,f) is non empty strict V109() quasi_total non-empty SubAlgebra of (D,f)
the carrier of (GenUnivAlg (D,f)) is non empty set
c1 is Element of the carrier of (D,f)
cf 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 cf 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)
rng cf is set
c1 -tree cf is Relation-like the carrier of (D,f) -valued Function-like DecoratedTree-like Element of FinTrees the carrier of (D,f)
F is set
ff is Relation-like the carrier of (D,f) -valued Function-like DecoratedTree-like Element of FinTrees the carrier of (D,f)
[c1,(roots cf)] is set
{c1,(roots cf)} is non empty set
{c1} is non empty V5() V37(1) set
{{c1,(roots cf)},{c1}} 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
x is Element 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) *
[x,ff] is set
{x,ff} is non empty set
{x} is non empty V5() V37(1) set
{{x,ff},{x}} is non empty set
D . x is set
len ff is V23() V24() V25() V29() V30() V35() V129() V130() V131() Element of NAT
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
dom (D,f) is Element of K32(NAT)
Seg (len D) is non empty V30() V37( len D) Element of K32(NAT)
s is V23() V24() V25() V29() V30() V35() V129() V130() V131() Element of NAT
(D,f) . s is Relation-like Function-like set
rng (D,f) is set
the carrier of (D,f) * is non empty functional FinSequence-membered FinSequenceSet of the carrier of (D,f)
Operations (D,f) is non empty PFuncsDomHQN of the carrier of (D,f)
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))
PFuncs (( the carrier of (D,f) *), the carrier of (D,f)) is non empty functional set
rng the charact of (D,f) is set
(D,f,s) 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 Element of K32( the carrier of (D,f))
o2 is non empty Relation-like the carrier of (D,f) * -defined the carrier of (D,f) -valued Function-like homogeneous quasi_total Element of Operations (D,f)
dom (D,f,s) is non empty functional FinSequence-membered with_common_domain Element of K32(((TS (D,f)) *))
K32(((TS (D,f)) *)) is non empty set
D /. s is V23() V24() V25() V29() V30() V35() V129() V130() V131() Element of NAT
(D /. s) -tuples_on (TS (D,f)) is non empty functional FinSequence-membered FinSequenceSet of TS (D,f)
{ b₁ where b₁ is Relation-like NAT -defined TS (D,f) -valued Function-like V30() FinSequence-like FinSubsequence-like Element of (TS (D,f)) * : len b₁ = D /. s } is set
dom o2 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 o2 is V23() V24() V25() V29() V30() V35() V129() V130() V131() Element of NAT
(arity o2) -tuples_on the carrier of (D,f) is non empty functional FinSequence-membered FinSequenceSet of the carrier of (D,f)
{ b₁ where b₁ is Relation-like NAT -defined the carrier of (D,f) -valued Function-like V30() FinSequence-like FinSubsequence-like Element of the carrier of (D,f) * : len b₁ = arity o2 } is set
dom (roots cf) is Element of K32(NAT)
dom cf is Element of K32(NAT)
len cf is V23() V24() V25() V29() V30() V35() V129() V130() V131() Element of NAT
Seg (len cf) is V30() V37( len cf) Element of K32(NAT)
ff is Relation-like NAT -defined TS (D,f) -valued Function-like V30() FinSequence-like FinSubsequence-like DTree-yielding Element of (TS (D,f)) *
F is Relation-like NAT -defined the carrier of (GenUnivAlg (D,f)) -valued Function-like V30() FinSequence-like FinSubsequence-like FinSequence of the carrier of (GenUnivAlg (D,f))
o2 . F is set
(D,f,s) is Element of the carrier of (D,f)
(D,f,s) -tree cf is Relation-like the carrier of (D,f) -valued Function-like DecoratedTree-like Element of FinTrees the carrier of (D,f)
A is set
c1 is Relation-like the carrier of (D,f) -valued Function-like DecoratedTree-like Element of FinTrees the carrier of (D,f)
cf is Element of the carrier of (D,f)
root-tree cf 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 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
(D,f) is ((D,f))
(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
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₁) where b₁ is Element of the carrier of (D,f) : b₁ in Terminals (D,f) } is set
c₃ is non empty set
K33((D,f),c₃) is Relation-like set
K32(K33((D,f),c₃)) is non empty set
fua is Element of the carrier of (D,f)
U1 is Relation-like (D,f) -defined c₃ -valued Function-like quasi_total Element of K32(K33((D,f),c₃))
root-tree fua is Relation-like the carrier of (D,f) -valued Function-like DecoratedTree-like Element of FinTrees the carrier of (D,f)
U1 . (root-tree fua) is set
dom U1 is Element of K32((D,f))
K32((D,f)) is non empty set
rng 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 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
the carrier of (D,f) is non empty set
c₃ is Element of the carrier of (D,f)
fua is Relation-like NAT -defined Function-like V30() FinSequence-like FinSubsequence-like set
[c₃,fua] is set
{c₃,fua} is non empty set
{c₃} is non empty V5() V37(1) set
{{c₃,fua},{c₃}} 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
U1 is Element of (dom D) \/ f
c1 is Relation-like NAT -defined (dom D) \/ f -valued Function-like V30() FinSequence-like FinSubsequence-like Element of ((dom D) \/ f) *
[U1,c1] is set
{U1,c1} is non empty set
{U1} is non empty V5() V37(1) set
{{U1,c1},{U1}} 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 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
(D,f) is ((D,f))
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₁) where b₁ is Element of the carrier of (D,f) : b₁ in Terminals (D,f) } is set
U1 is non empty V109() quasi_total non-empty UAStr
the carrier of U1 is non empty set
K33((D,f), the carrier of U1) is Relation-like set
K32(K33((D,f), the carrier of U1)) is non empty set
the carrier of (D,f) is non empty set
K33( the carrier of (D,f), the carrier of U1) is non empty Relation-like set
K32(K33( the carrier of (D,f), the carrier of U1)) is non empty set
F is Relation-like (D,f) -defined the carrier of U1 -valued Function-like quasi_total Element of K32(K33((D,f), the carrier of U1))
K33((TS (D,f)), the carrier of U1) is non empty Relation-like set
K32(K33((TS (D,f)), the carrier of U1)) is non empty set
ff is Relation-like TS (D,f) -defined the carrier of U1 -valued Function-like quasi_total Element of K32(K33((TS (D,f)), the carrier of U1))
ff is Relation-like the carrier of (D,f) -defined the carrier of U1 -valued Function-like quasi_total Element of K32(K33( the carrier of (D,f), the carrier of U1))
ff | (D,f) is Relation-like (D,f) -defined the carrier of (D,f) -defined the carrier of U1 -valued Function-like Element of K32(K33( the carrier of (D,f), the carrier of U1))
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 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
dom the charact of (D,f) is Element of K32(NAT)
Operations (D,f) is non empty PFuncsDomHQN of the carrier of (D,f)
rng the charact of (D,f) is set
the carrier of U1 * is non empty functional FinSequence-membered FinSequenceSet of the carrier of U1
Operations U1 is non empty PFuncsDomHQN of the carrier of U1
the charact of U1 is Relation-like NAT -defined PFuncs (( the carrier of U1 *), the carrier of U1) -valued Function-like V30() FinSequence-like FinSubsequence-like FinSequence of PFuncs (( the carrier of U1 *), the carrier of U1)
PFuncs (( the carrier of U1 *), the carrier of U1) is non empty functional set
rng the charact of U1 is set
len the charact of U1 is V23() V24() V25() V29() V30() V35() V129() V130() V131() Element of NAT
Seg (len the charact of U1) is V30() V37( len the charact of U1) Element of K32(NAT)
dom the charact of U1 is Element of K32(NAT)
x is V23() V24() V25() V29() V30() V35() V129() V130() V131() Element of NAT
the charact of (D,f) . x is Relation-like Function-like set
the charact of U1 . x is Relation-like Function-like set
s is non empty Relation-like the carrier of (D,f) * -defined the carrier of (D,f) -valued Function-like homogeneous quasi_total Element of Operations (D,f)
dom s 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
o2 is non empty Relation-like the carrier of U1 * -defined the carrier of U1 -valued Function-like homogeneous quasi_total Element of Operations U1
x 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)
s . x is set
ff . (s . x) is set
ff * x is Relation-like NAT -defined the carrier of U1 -valued Function-like V30() FinSequence-like FinSubsequence-like Element of the carrier of U1 *
o2 . (ff * x) is set
xa 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 xa 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 xa) is Element of K32(NAT)
dom xa is Element of K32(NAT)
len xa is V23() V24() V25() V29() V30() V35() V129() V130() V131() Element of NAT
Seg (len xa) is V30() V37( len xa) Element of K32(NAT)
len (roots xa) is V23() V24() V25() V29() V30() V35() V129() V130() V131() Element of NAT
xa 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 xa 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)
rxa is Relation-like NAT -defined (dom D) \/ f -valued Function-like V30() FinSequence-like FinSubsequence-like FinSequence of (dom D) \/ f
arity s is V23() V24() V25() V29() V30() V35() V129() V130() V131() Element of NAT
(arity s) -tuples_on the carrier of (D,f) is non empty functional FinSequence-membered FinSequenceSet of the carrier of (D,f)
{ b₁ where b₁ is Relation-like NAT -defined the carrier of (D,f) -valued Function-like V30() FinSequence-like FinSubsequence-like Element of the carrier of (D,f) * : len b₁ = arity s } is set
(D,f,x) 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
dom o2 is non empty functional FinSequence-membered with_common_domain Element of K32(( the carrier of U1 *))
K32(( the carrier of U1 *)) is non empty set
arity o2 is V23() V24() V25() V29() V30() V35() V129() V130() V131() Element of NAT
(arity o2) -tuples_on the carrier of U1 is non empty functional FinSequence-membered FinSequenceSet of the carrier of U1
{ b₁ where b₁ is Relation-like NAT -defined the carrier of U1 -valued Function-like V30() FinSequence-like FinSubsequence-like Element of the carrier of U1 * : len b₁ = arity o2 } is set
len the charact of (D,f) is V23() V24() V25() V29() V30() V35() V129() V130() V131() Element of NAT
Seg (len the charact of (D,f)) is V30() V37( len the charact of (D,f)) Element of K32(NAT)
dom (D,f) is Element of K32(NAT)
len (D,f) is V23() V24() V25() V29() V30() V35() V129() V130() V131() Element of NAT
Seg (len (D,f)) is V30() V37( len (D,f)) Element of K32(NAT)
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)
signature (D,f) is Relation-like NAT -defined NAT -valued Function-like V30() FinSequence-like FinSubsequence-like FinSequence of NAT
(signature (D,f)) . x is set
nd is Element of (dom D) \/ f
rxa is Relation-like NAT -defined (dom D) \/ f -valued Function-like V30() FinSequence-like FinSubsequence-like Element of ((dom D) \/ f) *
[nd,rxa] is set
{nd,rxa} is non empty set
{nd} is non empty V5() V37(1) set
{{nd,rxa},{nd}} is non empty set
xa is Relation-like NAT -defined the carrier of (D,f) -valued Function-like V30() FinSequence-like FinSubsequence-like Element of the carrier of (D,f) *
len xa is V23() V24() V25() V29() V30() V35() V129() V130() V131() Element of NAT
nt is Element of the carrier of (D,f)
nt -tree xa is Relation-like the carrier of (D,f) -valued Function-like DecoratedTree-like Element of FinTrees the carrier of (D,f)
ff . (nt -tree xa) is set
(D,f,nt) is V23() V24() V25() V29() V30() V35() V129() V130() V131() Element of NAT
(U1,(D,f,nt)) is non empty Relation-like the carrier of U1 * -defined the carrier of U1 -valued Function-like homogeneous quasi_total Element of Operations U1
(U1,(D,f,nt)) /. (ff * x) is Element of the carrier of U1
signature U1 is Relation-like NAT -defined NAT -valued Function-like V30() FinSequence-like FinSubsequence-like FinSequence of NAT
len (ff * x) is V23() V24() V25() V29() V30() V35() V129() V130() V131() Element of NAT
len x is V23() V24() V25() V29() V30() V35() V129() V130() V131() Element of NAT
xa is Relation-like NAT -defined the carrier of (D,f) -valued Function-like V30() FinSequence-like FinSubsequence-like Element of the carrier of (D,f) *
len xa is V23() V24() V25() V29() V30() V35() V129() V130() V131() Element of NAT
fx is Relation-like NAT -defined the carrier of U1 -valued Function-like V30() FinSequence-like FinSubsequence-like Element of the carrier of U1 *
(D,f,x) is Element of the carrier of (D,f)
xa is Relation-like NAT -defined TS (D,f) -valued Function-like V30() FinSequence-like FinSubsequence-like DTree-yielding Element of (TS (D,f)) *
nt -tree xa is Relation-like Function-like DecoratedTree-like set
the carrier of (D,f) /\ (D,f) is Element of K32( the carrier of (D,f))
K32( the carrier of (D,f)) is non empty set
dom (ff | (D,f)) is Element of K32((D,f))
K32((D,f)) is non empty set
dom ff is Element of K32( the carrier of (D,f))
(dom ff) /\ (D,f) is Element of K32( the carrier of (D,f))
x is set
dom F is Element of K32((D,f))
s is Element of the carrier of (D,f)
root-tree s is Relation-like the carrier of (D,f) -valued Function-like DecoratedTree-like Element of FinTrees the carrier of (D,f)
(ff | (D,f)) . x is set
ff . x is set
(D,f, the carrier of U1,s,F) is Element of the carrier of U1
F . x 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 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
(D,f) is ((D,f))
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₁) where b₁ is Element of the carrier of (D,f) : b₁ in Terminals (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 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₁) where b₁ is Element of the carrier of (D,f) : b₁ in Terminals (D,f) } is set
c₃ is V23() V24() V25() V29() V30() V35() V129() V130() V131() set
D is non empty Relation-like non non-empty 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 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₃ is V23() V24() V25() V29() V30() V35() V129() V130() V131() Element of NAT
(D /. c₃) -tuples_on (TS (D,f)) is non empty functional FinSequence-membered FinSequenceSet of TS (D,f)
{ b₁ where b₁ is Relation-like NAT -defined TS (D,f) -valued Function-like V30() FinSequence-like FinSubsequence-like Element of (TS (D,f)) * : len b₁ = D /. c₃ } is set
(D,f,c₃) is Element of the carrier of (D,f)
D . c₃ 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₃) -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)
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₃) -tree x is Relation-like Function-like DecoratedTree-like set
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₃) -tree s is Relation-like the carrier of (D,f) -valued Function-like DecoratedTree-like Element of FinTrees 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 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₃) FinSequence-like FinSubsequence-like DTree-yielding Element of (D /. c₃) -tuples_on (TS (D,f)) is Relation-like NAT -defined TS (D,f) -valued Function-like V30() V37(D /. c₃) FinSequence-like FinSubsequence-like DTree-yielding Element of (D /. c₃) -tuples_on (TS (D,f))
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₃) -tree ff is Relation-like the carrier of (D,f) -valued Function-like DecoratedTree-like Element of FinTrees the carrier of (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))))
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₃) -tree cf is Relation-like Function-like DecoratedTree-like set
U1 . c1 is Relation-like Function-like set
A . c1 is Relation-like Function-like 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 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₃ 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 c₃ is V23() V24() V25() V29() V30() V35() V129() V130() V131() Element of NAT
dom c₃ is Element of K32(NAT)
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)
Seg (len c₃) is V30() V37( len c₃) Element of K32(NAT)
Seg (len D) is non empty V30() V37( len D) Element of K32(NAT)
Seg (len fua) is V30() V37( len fua) Element of K32(NAT)
U1 is V23() V24() V25() V29() V30() V35() V129() V130() V131() set
c₃ . U1 is Relation-like Function-like set
fua . U1 is Relation-like Function-like 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
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 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 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 V109() quasi_total non-empty UAStr
(D,f) is non empty strict 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₁ where b₁ is Relation-like NAT -defined the carrier of (D,f) -valued Function-like V30() FinSequence-like FinSubsequence-like Element of the carrier of (D,f) * : len b₁ = arity A } is set
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₁ where b₁ is Relation-like NAT -defined TS (D,f) -valued Function-like V30() FinSequence-like FinSubsequence-like Element of (TS (D,f)) * : len b₁ = D /. U1 } is set
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 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 V109() quasi_total non-empty UAStr
(D,f) is non empty strict 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
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)
rng D is non empty set
U1 is V23() V24() V25() V29() V30() V35() V129() V130() V131() set
D . U1 is set
len (D,f) is V23() V24() V25() V29() V30() V35() V129() V130() V131() Element of NAT
dom (D,f) is Element of K32(NAT)
Seg (len (D,f)) is V30() V37( len (D,f)) Element of K32(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
the charact of (D,f) . U1 is Relation-like Function-like 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
Operations (D,f) is non empty PFuncsDomHQN of the carrier of (D,f)
rng the charact of (D,f) is 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 Operations (D,f)
arity A is V23() V24() V25() V29() V30() V35() V129() V130() V131() Element of NAT
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) -tuples_on the carrier of (D,f) is non empty functional FinSequence-membered FinSequenceSet of the carrier of (D,f)
{ b₁ where b₁ is Relation-like NAT -defined the carrier of (D,f) -valued Function-like V30() FinSequence-like FinSubsequence-like Element of the carrier of (D,f) * : len b₁ = arity A } is set
D /. U1 is V23() V24() V25() V29() V30() V35() V129() V130() V131() Element of NAT
dom (D,f,U1) is non empty functional FinSequence-membered with_common_domain Element of K32(((TS (D,f)) *))
K32(((TS (D,f)) *)) is non empty set
(D /. U1) -tuples_on (TS (D,f)) is non empty functional FinSequence-membered FinSequenceSet of TS (D,f)
{ b₁ where b₁ is Relation-like NAT -defined TS (D,f) -valued Function-like V30() FinSequence-like FinSubsequence-like Element of (TS (D,f)) * : len b₁ = D /. U1 } 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 V109() quasi_total non-empty UAStr
(D,f) is non empty strict 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
Constants (D,f) is 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
the carrier of (D,f) * is non empty functional FinSequence-membered FinSequenceSet of the carrier of (D,f)
Operations (D,f) is non empty PFuncsDomHQN of the carrier of (D,f)
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))
PFuncs (( the carrier of (D,f) *), the carrier of (D,f)) is non empty functional set
rng the charact of (D,f) is set
{ b₁ where b₁ is Element of the carrier of (D,f) : ex b₂ being non empty Relation-like the carrier of (D,f) * -defined the carrier of (D,f) -valued Function-like homogeneous quasi_total Element of Operations (D,f) st
( arity b₂ = 0 & b₁ in rng b₂ ) } is 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)
rng D is non empty set
A is V23() V24() V25() V29() V30() V35() V129() V130() V131() set
D . A is set
len (D,f) is V23() V24() V25() V29() V30() V35() V129() V130() V131() Element of NAT
dom (D,f) is Element of K32(NAT)
Seg (len (D,f)) is V30() V37( len (D,f)) Element of K32(NAT)
the charact of (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))))
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 /. A is V23() V24() V25() V29() V30() V35() V129() V130() V131() Element of NAT
dom (D,f,A) is non empty functional FinSequence-membered with_common_domain Element of K32(((TS (D,f)) *))
K32(((TS (D,f)) *)) is non empty set
(D /. A) -tuples_on (TS (D,f)) is non empty functional FinSequence-membered FinSequenceSet of TS (D,f)
{ b₁ where b₁ is Relation-like NAT -defined TS (D,f) -valued Function-like V30() FinSequence-like FinSubsequence-like Element of (TS (D,f)) * : len b₁ = D /. A } is set
c1 is non empty Relation-like the carrier of (D,f) * -defined the carrier of (D,f) -valued Function-like homogeneous quasi_total Element of Operations (D,f)
dom c1 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
<*> (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 V5() functional V37(1) set
c1 . (<*> (TS (D,f))) is set
rng c1 is non empty set
arity c1 is V23() V24() V25() V29() V30() V35() V129() V130() V131() Element of NAT
(arity c1) -tuples_on the carrier of (D,f) is non empty functional FinSequence-membered FinSequenceSet of the carrier of (D,f)
{ b₁ where b₁ is Relation-like NAT -defined the carrier of (D,f) -valued Function-like V30() FinSequence-like FinSubsequence-like Element of the carrier of (D,f) * : len b₁ = arity c1 } is set
cf is Element of the carrier of (D,f)
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 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 set
{ (root-tree b₁) where b₁ is Element of the carrier of (D,f) : b₁ in Terminals (D,f) } is set
(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 non non-empty NAT -defined NAT -valued Function-like V30() FinSequence-like FinSubsequence-like FinSequence of NAT
f is () 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_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 set
{ (root-tree b₁) where b₁ is Element of the carrier of (D,f) : b₁ in Terminals (D,f) } is set
GenUnivAlg (D,f) is non empty strict V109() quasi_total non-empty SubAlgebra of (D,f)
the carrier of (GenUnivAlg (D,f)) is non empty set
c1 is Element of the carrier of (D,f)
cf 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 cf 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)
rng cf is set
c1 -tree cf is Relation-like the carrier of (D,f) -valued Function-like DecoratedTree-like Element of FinTrees the carrier of (D,f)
F is set
ff is Relation-like the carrier of (D,f) -valued Function-like DecoratedTree-like Element of FinTrees the carrier of (D,f)
[c1,(roots cf)] is set
{c1,(roots cf)} is non empty set
{c1} is non empty V5() V37(1) set
{{c1,(roots cf)},{c1}} 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
x is Element 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) *
[x,ff] is set
{x,ff} is non empty set
{x} is non empty V5() V37(1) set
{{x,ff},{x}} is non empty set
D . x is set
len ff is V23() V24() V25() V29() V30() V35() V129() V130() V131() Element of NAT
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
dom (D,f) is Element of K32(NAT)
Seg (len D) is non empty V30() V37( len D) Element of K32(NAT)
s is V23() V24() V25() V29() V30() V35() V129() V130() V131() Element of NAT
(D,f) . s is Relation-like Function-like set
rng (D,f) is set
the carrier of (D,f) * is non empty functional FinSequence-membered FinSequenceSet of the carrier of (D,f)
Operations (D,f) is non empty PFuncsDomHQN of the carrier of (D,f)
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))
PFuncs (( the carrier of (D,f) *), the carrier of (D,f)) is non empty functional set
rng the charact of (D,f) is set
(D,f,s) 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 Element of K32( the carrier of (D,f))
o2 is non empty Relation-like the carrier of (D,f) * -defined the carrier of (D,f) -valued Function-like homogeneous quasi_total Element of Operations (D,f)
dom (D,f,s) is non empty functional FinSequence-membered with_common_domain Element of K32(((TS (D,f)) *))
K32(((TS (D,f)) *)) is non empty set
D /. s is V23() V24() V25() V29() V30() V35() V129() V130() V131() Element of NAT
(D /. s) -tuples_on (TS (D,f)) is non empty functional FinSequence-membered FinSequenceSet of TS (D,f)
{ b₁ where b₁ is Relation-like NAT -defined TS (D,f) -valued Function-like V30() FinSequence-like FinSubsequence-like Element of (TS (D,f)) * : len b₁ = D /. s } is set
dom o2 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 o2 is V23() V24() V25() V29() V30() V35() V129() V130() V131() Element of NAT
(arity o2) -tuples_on the carrier of (D,f) is non empty functional FinSequence-membered FinSequenceSet of the carrier of (D,f)
{ b₁ where b₁ is Relation-like NAT -defined the carrier of (D,f) -valued Function-like V30() FinSequence-like FinSubsequence-like Element of the carrier of (D,f) * : len b₁ = arity o2 } is set
dom (roots cf) is Element of K32(NAT)
dom cf is Element of K32(NAT)
len cf is V23() V24() V25() V29() V30() V35() V129() V130() V131() Element of NAT
Seg (len cf) is V30() V37( len cf) Element of K32(NAT)
ff is Relation-like NAT -defined TS (D,f) -valued Function-like V30() FinSequence-like FinSubsequence-like DTree-yielding Element of (TS (D,f)) *
F is Relation-like NAT -defined the carrier of (GenUnivAlg (D,f)) -valued Function-like V30() FinSequence-like FinSubsequence-like FinSequence of the carrier of (GenUnivAlg (D,f))
o2 . F is set
(D,f,s) is Element of the carrier of (D,f)
(D,f,s) -tree cf is Relation-like the carrier of (D,f) -valued Function-like DecoratedTree-like Element of FinTrees the carrier of (D,f)
A is set
c1 is Relation-like the carrier of (D,f) -valued Function-like DecoratedTree-like Element of FinTrees the carrier of (D,f)
cf is Element of the carrier of (D,f)
root-tree cf is Relation-like the carrier of (D,f) -valued Function-like DecoratedTree-like Element of FinTrees the carrier of (D,f)
Constants (D,f) is Element of K32( the carrier of (D,f))
the carrier of (D,f) * is non empty functional FinSequence-membered FinSequenceSet of the carrier of (D,f)
Operations (D,f) is non empty PFuncsDomHQN of the carrier of (D,f)
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))
PFuncs (( the carrier of (D,f) *), the carrier of (D,f)) is non empty functional set
rng the charact of (D,f) is set
{ b₁ where b₁ is Element of the carrier of (D,f) : ex b₂ being non empty Relation-like the carrier of (D,f) * -defined the carrier of (D,f) -valued Function-like homogeneous quasi_total Element of Operations (D,f) st
( arity b₂ = 0 & b₁ in rng b₂ ) } is set
Constants (D,f) is Element of K32( the carrier of (D,f))
the carrier of (D,f) * is non empty functional FinSequence-membered FinSequenceSet of the carrier of (D,f)
Operations (D,f) is non empty PFuncsDomHQN of the carrier of (D,f)
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))
PFuncs (( the carrier of (D,f) *), the carrier of (D,f)) is non empty functional set
rng the charact of (D,f) is set
{ b₁ where b₁ is Element of the carrier of (D,f) : ex b₂ being non empty Relation-like the carrier of (D,f) * -defined the carrier of (D,f) -valued Function-like homogeneous quasi_total Element of Operations (D,f) st
( arity b₂ = 0 & b₁ in rng b₂ ) } 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 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
(D,f) is ((D,f))
(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
Terminals (D,f) is set
{ (root-tree b₁) where b₁ is Element of the carrier of (D,f) : b₁ in Terminals (D,f) } is set
c₃ is non empty set
K33((D,f),c₃) is Relation-like set
K32(K33((D,f),c₃)) is non empty set
fua is Element of the carrier of (D,f)
U1 is Relation-like (D,f) -defined c₃ -valued Function-like quasi_total Element of K32(K33((D,f),c₃))
root-tree fua is Relation-like the carrier of (D,f) -valued Function-like DecoratedTree-like Element of FinTrees the carrier of (D,f)
U1 . (root-tree fua) is set
dom U1 is Element of K32((D,f))
K32((D,f)) is non empty set
rng U1 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 V109() quasi_total non-empty UAStr
(D,f) is non empty strict 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
(D,f) is ((D,f))
Terminals (D,f) is set
{ (root-tree b₁) where b₁ is Element of the carrier of (D,f) : b₁ in Terminals (D,f) } is set
U1 is non empty V109() quasi_total non-empty UAStr
the carrier of U1 is non empty set
K33((D,f), the carrier of U1) is Relation-like set
K32(K33((D,f), the carrier of U1)) is non empty set
the carrier of (D,f) is non empty set
K33( the carrier of (D,f), the carrier of U1) is non empty Relation-like set
K32(K33( the carrier of (D,f), the carrier of U1)) is non empty set
F is Relation-like (D,f) -defined the carrier of U1 -valued Function-like quasi_total Element of K32(K33((D,f), the carrier of U1))
K33((TS (D,f)), the carrier of U1) is non empty Relation-like set
K32(K33((TS (D,f)), the carrier of U1)) is non empty set
ff is Relation-like TS (D,f) -defined the carrier of U1 -valued Function-like quasi_total Element of K32(K33((TS (D,f)), the carrier of U1))
ff is Relation-like the carrier of (D,f) -defined the carrier of U1 -valued Function-like quasi_total Element of K32(K33( the carrier of (D,f), the carrier of U1))
ff | (D,f) is Relation-like (D,f) -defined the carrier of (D,f) -defined the carrier of U1 -valued Function-like Element of K32(K33( the carrier of (D,f), the carrier of U1))
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 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
dom the charact of (D,f) is Element of K32(NAT)
Operations (D,f) is non empty PFuncsDomHQN of the carrier of (D,f)
rng the charact of (D,f) is set
the carrier of U1 * is non empty functional FinSequence-membered FinSequenceSet of the carrier of U1
Operations U1 is non empty PFuncsDomHQN of the carrier of U1
the charact of U1 is Relation-like NAT -defined PFuncs (( the carrier of U1 *), the carrier of U1) -valued Function-like V30() FinSequence-like FinSubsequence-like FinSequence of PFuncs (( the carrier of U1 *), the carrier of U1)
PFuncs (( the carrier of U1 *), the carrier of U1) is non empty functional set
rng the charact of U1 is set
dom the charact of U1 is Element of K32(NAT)
len the charact of U1 is V23() V24() V25() V29() V30() V35() V129() V130() V131() Element of NAT
Seg (len the charact of U1) is V30() V37( len the charact of U1) Element of K32(NAT)
x is V23() V24() V25() V29() V30() V35() V129() V130() V131() Element of NAT
the charact of (D,f) . x is Relation-like Function-like set
the charact of U1 . x is Relation-like Function-like set
s is non empty Relation-like the carrier of (D,f) * -defined the carrier of (D,f) -valued Function-like homogeneous quasi_total Element of Operations (D,f)
dom s 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
o2 is non empty Relation-like the carrier of U1 * -defined the carrier of U1 -valued Function-like homogeneous quasi_total Element of Operations U1
x 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)
s . x is set
ff . (s . x) is set
ff * x is Relation-like NAT -defined the carrier of U1 -valued Function-like V30() FinSequence-like FinSubsequence-like Element of the carrier of U1 *
o2 . (ff * x) is set
xa 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 xa 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 xa) is Element of K32(NAT)
dom xa is Element of K32(NAT)
len xa is V23() V24() V25() V29() V30() V35() V129() V130() V131() Element of NAT
Seg (len xa) is V30() V37( len xa) Element of K32(NAT)
len (roots xa) is V23() V24() V25() V29() V30() V35() V129() V130() V131() Element of NAT
xa 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 xa 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)
rxa is Relation-like NAT -defined (dom D) \/ f -valued Function-like V30() FinSequence-like FinSubsequence-like FinSequence of (dom D) \/ f
arity s is V23() V24() V25() V29() V30() V35() V129() V130() V131() Element of NAT
(arity s) -tuples_on the carrier of (D,f) is non empty functional FinSequence-membered FinSequenceSet of the carrier of (D,f)
{ b₁ where b₁ is Relation-like NAT -defined the carrier of (D,f) -valued Function-like V30() FinSequence-like FinSubsequence-like Element of the carrier of (D,f) * : len b₁ = arity s } is set
(D,f,x) 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
dom o2 is non empty functional FinSequence-membered with_common_domain Element of K32(( the carrier of U1 *))
K32(( the carrier of U1 *)) is non empty set
arity o2 is V23() V24() V25() V29() V30() V35() V129() V130() V131() Element of NAT
(arity o2) -tuples_on the carrier of U1 is non empty functional FinSequence-membered FinSequenceSet of the carrier of U1
{ b₁ where b₁ is Relation-like NAT -defined the carrier of U1 -valued Function-like V30() FinSequence-like FinSubsequence-like Element of the carrier of U1 * : len b₁ = arity o2 } is set
len the charact of (D,f) is V23() V24() V25() V29() V30() V35() V129() V130() V131() Element of NAT
Seg (len the charact of (D,f)) is V30() V37( len the charact of (D,f)) Element of K32(NAT)
len (D,f) is V23() V24() V25() V29() V30() V35() V129() V130() V131() Element of NAT
Seg (len (D,f)) is V30() V37( len (D,f)) Element of K32(NAT)
dom (D,f) is Element of K32(NAT)
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)
signature (D,f) is Relation-like NAT -defined NAT -valued Function-like V30() FinSequence-like FinSubsequence-like FinSequence of NAT
(signature (D,f)) . x is set
nd is Element of (dom D) \/ f
rxa is Relation-like NAT -defined (dom D) \/ f -valued Function-like V30() FinSequence-like FinSubsequence-like Element of ((dom D) \/ f) *
[nd,rxa] is set
{nd,rxa} is non empty set
{nd} is non empty V5() V37(1) set
{{nd,rxa},{nd}} is non empty set
xa is Relation-like NAT -defined the carrier of (D,f) -valued Function-like V30() FinSequence-like FinSubsequence-like Element of the carrier of (D,f) *
len xa is V23() V24() V25() V29() V30() V35() V129() V130() V131() Element of NAT
nt is Element of the carrier of (D,f)
nt -tree xa is Relation-like the carrier of (D,f) -valued Function-like DecoratedTree-like Element of FinTrees the carrier of (D,f)
ff . (nt -tree xa) is set
(D,f,nt) is V23() V24() V25() V29() V30() V35() V129() V130() V131() Element of NAT
(U1,(D,f,nt)) is non empty Relation-like the carrier of U1 * -defined the carrier of U1 -valued Function-like homogeneous quasi_total Element of Operations U1
(U1,(D,f,nt)) /. (ff * x) is Element of the carrier of U1
signature U1 is Relation-like NAT -defined NAT -valued Function-like V30() FinSequence-like FinSubsequence-like FinSequence of NAT
len (ff * x) is V23() V24() V25() V29() V30() V35() V129() V130() V131() Element of NAT
len x is V23() V24() V25() V29() V30() V35() V129() V130() V131() Element of NAT
xa is Relation-like NAT -defined the carrier of (D,f) -valued Function-like V30() FinSequence-like FinSubsequence-like Element of the carrier of (D,f) *
len xa is V23() V24() V25() V29() V30() V35() V129() V130() V131() Element of NAT
fx is Relation-like NAT -defined the carrier of U1 -valued Function-like V30() FinSequence-like FinSubsequence-like Element of the carrier of U1 *
(D,f,x) is Element of the carrier of (D,f)
xa is Relation-like NAT -defined TS (D,f) -valued Function-like V30() FinSequence-like FinSubsequence-like DTree-yielding Element of (TS (D,f)) *
nt -tree xa is Relation-like Function-like DecoratedTree-like set
the carrier of (D,f) /\ (D,f) is Element of K32( the carrier of (D,f))
K32( the carrier of (D,f)) is non empty set
dom (ff | (D,f)) is Element of K32((D,f))
K32((D,f)) is non empty set
dom ff is Element of K32( the carrier of (D,f))
(dom ff) /\ (D,f) is Element of K32( the carrier of (D,f))
x is set
dom F is Element of K32((D,f))
s is Element of the carrier of (D,f)
root-tree s is Relation-like the carrier of (D,f) -valued Function-like DecoratedTree-like Element of FinTrees the carrier of (D,f)
(ff | (D,f)) . x is set
ff . x is set
(D,f, the carrier of U1,s,F) is Element of the carrier of U1
F . x 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 V109() quasi_total non-empty UAStr
(D,f) is non empty strict 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
(D,f) is ((D,f))
Terminals (D,f) is set
{ (root-tree b₁) where b₁ is Element of the carrier of (D,f) : b₁ in Terminals (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 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_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 set
{ (root-tree b₁) where b₁ is Element of the carrier of (D,f) : b₁ in Terminals (D,f) } is set
the () set is () set
the non empty Relation-like non non-empty NAT -defined NAT -valued Function-like V30() FinSequence-like FinSubsequence-like FinSequence of NAT is non empty Relation-like non non-empty NAT -defined NAT -valued Function-like V30() FinSequence-like FinSubsequence-like FinSequence of NAT
( the non empty Relation-like non non-empty NAT -defined NAT -valued Function-like V30() FinSequence-like FinSubsequence-like FinSequence of NAT , the () set ) is non empty strict V109() quasi_total non-empty () UAStr
( the non empty Relation-like non non-empty NAT -defined NAT -valued Function-like V30() FinSequence-like FinSubsequence-like FinSequence of NAT , the () set ) is non empty strict with_nonterminals with_useful_nonterminals DTConstrStr
dom the non empty Relation-like non non-empty NAT -defined NAT -valued Function-like V30() FinSequence-like FinSubsequence-like FinSequence of NAT is non empty Element of K32(NAT)
(dom the non empty Relation-like non non-empty NAT -defined NAT -valued Function-like V30() FinSequence-like FinSubsequence-like FinSequence of NAT ) \/ the () set is non empty set
( the non empty Relation-like non non-empty NAT -defined NAT -valued Function-like V30() FinSequence-like FinSubsequence-like FinSequence of NAT , the () set ) is Relation-like (dom the non empty Relation-like non non-empty NAT -defined NAT -valued Function-like V30() FinSequence-like FinSubsequence-like FinSequence of NAT ) \/ the () set -defined ((dom the non empty Relation-like non non-empty NAT -defined NAT -valued Function-like V30() FinSequence-like FinSubsequence-like FinSequence of NAT ) \/ the () set ) * -valued Element of K32(K33(((dom the non empty Relation-like non non-empty NAT -defined NAT -valued Function-like V30() FinSequence-like FinSubsequence-like FinSequence of NAT ) \/ the () set ),(((dom the non empty Relation-like non non-empty NAT -defined NAT -valued Function-like V30() FinSequence-like FinSubsequence-like FinSequence of NAT ) \/ the () set ) *)))
((dom the non empty Relation-like non non-empty NAT -defined NAT -valued Function-like V30() FinSequence-like FinSubsequence-like FinSequence of NAT ) \/ the () set ) * is non empty functional FinSequence-membered FinSequenceSet of (dom the non empty Relation-like non non-empty NAT -defined NAT -valued Function-like V30() FinSequence-like FinSubsequence-like FinSequence of NAT ) \/ the () set
K33(((dom the non empty Relation-like non non-empty NAT -defined NAT -valued Function-like V30() FinSequence-like FinSubsequence-like FinSequence of NAT ) \/ the () set ),(((dom the non empty Relation-like non non-empty NAT -defined NAT -valued Function-like V30() FinSequence-like FinSubsequence-like FinSequence of NAT ) \/ the () set ) *)) is non empty Relation-like set
K32(K33(((dom the non empty Relation-like non non-empty NAT -defined NAT -valued Function-like V30() FinSequence-like FinSubsequence-like FinSequence of NAT ) \/ the () set ),(((dom the non empty Relation-like non non-empty NAT -defined NAT -valued Function-like V30() FinSequence-like FinSubsequence-like FinSequence of NAT ) \/ the () set ) *))) is non empty set
DTConstrStr(# ((dom the non empty Relation-like non non-empty NAT -defined NAT -valued Function-like V30() FinSequence-like FinSubsequence-like FinSequence of NAT ) \/ the () set ),( the non empty Relation-like non non-empty NAT -defined NAT -valued Function-like V30() FinSequence-like FinSubsequence-like FinSequence of NAT , the () set ) #) is non empty strict DTConstrStr
TS ( the non empty Relation-like non non-empty NAT -defined NAT -valued Function-like V30() FinSequence-like FinSubsequence-like FinSequence of NAT , the () set ) is non empty functional constituted-DTrees Element of K32((FinTrees the carrier of ( the non empty Relation-like non non-empty NAT -defined NAT -valued Function-like V30() FinSequence-like FinSubsequence-like FinSequence of NAT , the () set )))
the carrier of ( the non empty Relation-like non non-empty NAT -defined NAT -valued Function-like V30() FinSequence-like FinSubsequence-like FinSequence of NAT , the () set ) is non empty set
FinTrees the carrier of ( the non empty Relation-like non non-empty NAT -defined NAT -valued Function-like V30() FinSequence-like FinSubsequence-like FinSequence of NAT , the () set ) is non empty functional constituted-DTrees DTree-set of the carrier of ( the non empty Relation-like non non-empty NAT -defined NAT -valued Function-like V30() FinSequence-like FinSubsequence-like FinSequence of NAT , the () set )
K32((FinTrees the carrier of ( the non empty Relation-like non non-empty NAT -defined NAT -valued Function-like V30() FinSequence-like FinSubsequence-like FinSequence of NAT , the () set ))) is non empty set
( the non empty Relation-like non non-empty NAT -defined NAT -valued Function-like V30() FinSequence-like FinSubsequence-like FinSequence of NAT , the () set ) is Relation-like NAT -defined PFuncs (((TS ( the non empty Relation-like non non-empty NAT -defined NAT -valued Function-like V30() FinSequence-like FinSubsequence-like FinSequence of NAT , the () set )) *),(TS ( the non empty Relation-like non non-empty NAT -defined NAT -valued Function-like V30() FinSequence-like FinSubsequence-like FinSequence of NAT , the () set ))) -valued Function-like V30() FinSequence-like FinSubsequence-like FinSequence of PFuncs (((TS ( the non empty Relation-like non non-empty NAT -defined NAT -valued Function-like V30() FinSequence-like FinSubsequence-like FinSequence of NAT , the () set )) *),(TS ( the non empty Relation-like non non-empty NAT -defined NAT -valued Function-like V30() FinSequence-like FinSubsequence-like FinSequence of NAT , the () set )))
(TS ( the non empty Relation-like non non-empty NAT -defined NAT -valued Function-like V30() FinSequence-like FinSubsequence-like FinSequence of NAT , the () set )) * is non empty functional FinSequence-membered FinSequenceSet of TS ( the non empty Relation-like non non-empty NAT -defined NAT -valued Function-like V30() FinSequence-like FinSubsequence-like FinSequence of NAT , the () set )
PFuncs (((TS ( the non empty Relation-like non non-empty NAT -defined NAT -valued Function-like V30() FinSequence-like FinSubsequence-like FinSequence of NAT , the () set )) *),(TS ( the non empty Relation-like non non-empty NAT -defined NAT -valued Function-like V30() FinSequence-like FinSubsequence-like FinSequence of NAT , the () set ))) is non empty functional set
UAStr(# (TS ( the non empty Relation-like non non-empty NAT -defined NAT -valued Function-like V30() FinSequence-like FinSubsequence-like FinSequence of NAT , the () set )),( the non empty Relation-like non non-empty NAT -defined NAT -valued Function-like V30() FinSequence-like FinSubsequence-like FinSequence of NAT , the () set ) #) is strict UAStr