K32() is non empty V4() V5() V6() Element of bool K28()
K28() is set
bool K28() is non empty set
K27() is non empty V4() V5() V6() set
bool K27() is non empty set
bool K32() is non empty set
{} is empty V4() V5() V6() V8() V9() V10() Relation-like non-empty empty-yielding K32() -defined Function-like one-to-one constant functional V32() V33() V34() FinSequence-like FinSubsequence-like FinSequence-membered constituted-Trees constituted-FinTrees constituted-DTrees Tree-yielding FinTree-yielding DTree-yielding set
the empty V4() V5() V6() V8() V9() V10() Relation-like non-empty empty-yielding K32() -defined Function-like one-to-one constant functional V32() V33() V34() FinSequence-like FinSubsequence-like FinSequence-membered constituted-Trees constituted-FinTrees constituted-DTrees Tree-yielding FinTree-yielding DTree-yielding set is empty V4() V5() V6() V8() V9() V10() Relation-like non-empty empty-yielding K32() -defined Function-like one-to-one constant functional V32() V33() V34() FinSequence-like FinSubsequence-like FinSequence-membered constituted-Trees constituted-FinTrees constituted-DTrees Tree-yielding FinTree-yielding DTree-yielding set
1 is non empty set
{{},1} is non empty set
Trees is non empty constituted-Trees set
bool Trees is non empty set
FinTrees is non empty constituted-Trees constituted-FinTrees Element of bool Trees
PeanoNat is non empty strict with_terminals with_nonterminals with_useful_nonterminals DTConstrStr
the carrier of PeanoNat is non empty set
FinTrees the carrier of PeanoNat is non empty functional constituted-DTrees DTree-set of the carrier of PeanoNat
TS PeanoNat is non empty functional constituted-DTrees Element of bool (FinTrees the carrier of PeanoNat)
bool (FinTrees the carrier of PeanoNat) is non empty set
[:(TS PeanoNat),K32():] is non empty Relation-like set
bool [:(TS PeanoNat),K32():] is non empty set
[:K32(),(TS PeanoNat):] is non empty Relation-like set
bool [:K32(),(TS PeanoNat):] is non empty set
2 is non empty set
3 is non empty set
K33() is empty V4() V5() V6() V8() V9() V10() Relation-like non-empty empty-yielding K32() -defined Function-like one-to-one constant functional V32() V33() V34() FinSequence-like FinSubsequence-like FinSequence-membered constituted-Trees constituted-FinTrees constituted-DTrees Tree-yielding FinTree-yielding DTree-yielding Element of K32()
K289(K33()) is non empty V104() set
<*> K32() is empty proper V4() V5() V6() V8() V9() V10() Relation-like non-empty empty-yielding K32() -defined K32() -valued Function-like one-to-one constant functional V32() V33() V34() FinSequence-like FinSubsequence-like FinSequence-membered constituted-Trees constituted-FinTrees constituted-DTrees Tree-yielding FinTree-yielding DTree-yielding FinSequence of K32()
[:K32(),K32():] is non empty Relation-like set
S is non empty non void V60() reflexive transitive antisymmetric order-sorted discernable OverloadedRSSign
the carrier of S is non empty set
X is order-sorted MSAlgebra over S
the Sorts of X is non empty Relation-like the carrier of S -defined Function-like total set
y is non empty Relation-like the carrier of S -defined Function-like total ManySortedSubset of the Sorts of X
t is non empty Relation-like the carrier of S -defined Function-like total OSSubset of X
OSCl t is non empty Relation-like the carrier of S -defined Function-like total order-sorted set
GenOSAlg t is strict order-sorted MSSubAlgebra of X
the Sorts of (GenOSAlg t) is non empty Relation-like the carrier of S -defined Function-like total set
P is non empty Relation-like the carrier of S -defined Function-like total OSSubset of X
GenOSAlg P is strict order-sorted MSSubAlgebra of X
the Sorts of (GenOSAlg P) is non empty Relation-like the carrier of S -defined Function-like total set
S is non empty non void V60() reflexive transitive antisymmetric order-sorted discernable OverloadedRSSign
the carrier of S is non empty set
X is strict non-empty order-sorted MSAlgebra over S
the Sorts of X is non empty Relation-like non-empty non empty-yielding the carrier of S -defined Function-like total set
x is non empty Relation-like the carrier of S -defined Function-like total ManySortedSubset of the Sorts of X
OSCl x is non empty Relation-like the carrier of S -defined Function-like total order-sorted set
t is non empty Relation-like the carrier of S -defined Function-like total OSSubset of X
GenOSAlg t is strict order-sorted MSSubAlgebra of X
the Sorts of (GenOSAlg t) is non empty Relation-like the carrier of S -defined Function-like total set
y is MSSubAlgebra of X
the Sorts of y is non empty Relation-like the carrier of S -defined Function-like total set
y is non empty Relation-like the carrier of S -defined Function-like total OSSubset of X
GenOSAlg y is strict order-sorted MSSubAlgebra of X
the Sorts of (GenOSAlg y) is non empty Relation-like the carrier of S -defined Function-like total set
S is non empty non void V60() reflexive transitive antisymmetric order-sorted discernable OverloadedRSSign
the carrier of S is non empty set
X is order-sorted monotone MSAlgebra over S
S is non empty non void V60() reflexive transitive antisymmetric order-sorted discernable OverloadedRSSign
S is non empty non void V60() reflexive transitive antisymmetric order-sorted discernable OverloadedRSSign
the carrier of S is non empty set
the carrier' of S is non empty set
{ the carrier of S} is non empty set
[: the carrier' of S,{ the carrier of S}:] is non empty Relation-like set
X is non empty Relation-like the carrier of S -defined Function-like total set
coprod X is non empty Relation-like the carrier of S -defined Function-like total set
Union (coprod X) is set
[: the carrier' of S,{ the carrier of S}:] \/ (Union (coprod X)) is non empty set
([: the carrier' of S,{ the carrier of S}:] \/ (Union (coprod X))) * is non empty functional FinSequence-membered M10([: the carrier' of S,{ the carrier of S}:] \/ (Union (coprod X)))
[:([: the carrier' of S,{ the carrier of S}:] \/ (Union (coprod X))),(([: the carrier' of S,{ the carrier of S}:] \/ (Union (coprod X))) *):] is non empty Relation-like set
bool [:([: the carrier' of S,{ the carrier of S}:] \/ (Union (coprod X))),(([: the carrier' of S,{ the carrier of S}:] \/ (Union (coprod X))) *):] is non empty set
y is Relation-like [: the carrier' of S,{ the carrier of S}:] \/ (Union (coprod X)) -defined ([: the carrier' of S,{ the carrier of S}:] \/ (Union (coprod X))) * -valued Element of bool [:([: the carrier' of S,{ the carrier of S}:] \/ (Union (coprod X))),(([: the carrier' of S,{ the carrier of S}:] \/ (Union (coprod X))) *):]
t is Element of [: the carrier' of S,{ the carrier of S}:] \/ (Union (coprod X))
tx is Relation-like K32() -defined [: the carrier' of S,{ the carrier of S}:] \/ (Union (coprod X)) -valued Function-like V34() FinSequence-like FinSubsequence-like Element of ([: the carrier' of S,{ the carrier of S}:] \/ (Union (coprod X))) *
[t,tx] is V26() set
{t,tx} is non empty set
{t} is non empty set
{{t,tx},{t}} is non empty set
len tx is V4() V5() V6() V10() Element of K32()
dom tx is Element of bool K32()
P is Element of the carrier' of S
[P, the carrier of S] is V26() set
{P, the carrier of S} is non empty set
{P} is non empty set
{{P, the carrier of S},{P}} is non empty set
the_arity_of P is Relation-like K32() -defined the carrier of S -valued Function-like V34() FinSequence-like FinSubsequence-like Element of the carrier of S *
the carrier of S * is non empty functional FinSequence-membered M10( the carrier of S)
len (the_arity_of P) is V4() V5() V6() V10() Element of K32()
O1 is set
tx . O1 is set
R is Element of the carrier' of S
[R, the carrier of S] is V26() set
{R, the carrier of S} is non empty set
{R} is non empty set
{{R, the carrier of S},{R}} is non empty set
the_result_sort_of R is Element of the carrier of S
(the_arity_of P) /. O1 is Element of the carrier of S
y is Relation-like [: the carrier' of S,{ the carrier of S}:] \/ (Union (coprod X)) -defined ([: the carrier' of S,{ the carrier of S}:] \/ (Union (coprod X))) * -valued Element of bool [:([: the carrier' of S,{ the carrier of S}:] \/ (Union (coprod X))),(([: the carrier' of S,{ the carrier of S}:] \/ (Union (coprod X))) *):]
t is Relation-like [: the carrier' of S,{ the carrier of S}:] \/ (Union (coprod X)) -defined ([: the carrier' of S,{ the carrier of S}:] \/ (Union (coprod X))) * -valued Element of bool [:([: the carrier' of S,{ the carrier of S}:] \/ (Union (coprod X))),(([: the carrier' of S,{ the carrier of S}:] \/ (Union (coprod X))) *):]
tx is set
P is set
[tx,P] is V26() set
{tx,P} is non empty set
{tx} is non empty set
{{tx,P},{tx}} is non empty set
O1 is Element of [: the carrier' of S,{ the carrier of S}:] \/ (Union (coprod X))
R is Relation-like K32() -defined [: the carrier' of S,{ the carrier of S}:] \/ (Union (coprod X)) -valued Function-like V34() FinSequence-like FinSubsequence-like Element of ([: the carrier' of S,{ the carrier of S}:] \/ (Union (coprod X))) *
[O1,R] is V26() set
{O1,R} is non empty set
{O1} is non empty set
{{O1,R},{O1}} is non empty set
len R is V4() V5() V6() V10() Element of K32()
dom R is Element of bool K32()
i is Element of the carrier' of S
[i, the carrier of S] is V26() set
{i, the carrier of S} is non empty set
{i} is non empty set
{{i, the carrier of S},{i}} is non empty set
the_arity_of i is Relation-like K32() -defined the carrier of S -valued Function-like V34() FinSequence-like FinSubsequence-like Element of the carrier of S *
the carrier of S * is non empty functional FinSequence-membered M10( the carrier of S)
len (the_arity_of i) is V4() V5() V6() V10() Element of K32()
s is set
R . s is set
a is Element of the carrier' of S
[a, the carrier of S] is V26() set
{a, the carrier of S} is non empty set
{a} is non empty set
{{a, the carrier of S},{a}} is non empty set
the_result_sort_of a is Element of the carrier of S
(the_arity_of i) /. s is Element of the carrier of S
O1 is Element of [: the carrier' of S,{ the carrier of S}:] \/ (Union (coprod X))
R is Relation-like K32() -defined [: the carrier' of S,{ the carrier of S}:] \/ (Union (coprod X)) -valued Function-like V34() FinSequence-like FinSubsequence-like Element of ([: the carrier' of S,{ the carrier of S}:] \/ (Union (coprod X))) *
[O1,R] is V26() set
{O1,R} is non empty set
{O1} is non empty set
{{O1,R},{O1}} is non empty set
len R is V4() V5() V6() V10() Element of K32()
dom R is Element of bool K32()
i is Element of the carrier' of S
[i, the carrier of S] is V26() set
{i, the carrier of S} is non empty set
{i} is non empty set
{{i, the carrier of S},{i}} is non empty set
the_arity_of i is Relation-like K32() -defined the carrier of S -valued Function-like V34() FinSequence-like FinSubsequence-like Element of the carrier of S *
the carrier of S * is non empty functional FinSequence-membered M10( the carrier of S)
len (the_arity_of i) is V4() V5() V6() V10() Element of K32()
s is set
R . s is set
a is Element of the carrier' of S
[a, the carrier of S] is V26() set
{a, the carrier of S} is non empty set
{a} is non empty set
{{a, the carrier of S},{a}} is non empty set
the_result_sort_of a is Element of the carrier of S
(the_arity_of i) /. s is Element of the carrier of S
S is non empty non void V60() reflexive transitive antisymmetric order-sorted discernable OverloadedRSSign
the carrier of S is non empty set
the carrier' of S is non empty set
{ the carrier of S} is non empty set
[: the carrier' of S,{ the carrier of S}:] is non empty Relation-like set
X is non empty Relation-like the carrier of S -defined Function-like total set
coprod X is non empty Relation-like the carrier of S -defined Function-like total set
Union (coprod X) is set
[: the carrier' of S,{ the carrier of S}:] \/ (Union (coprod X)) is non empty set
([: the carrier' of S,{ the carrier of S}:] \/ (Union (coprod X))) * is non empty functional FinSequence-membered M10([: the carrier' of S,{ the carrier of S}:] \/ (Union (coprod X)))
(S,X) is Relation-like [: the carrier' of S,{ the carrier of S}:] \/ (Union (coprod X)) -defined ([: the carrier' of S,{ the carrier of S}:] \/ (Union (coprod X))) * -valued Element of bool [:([: the carrier' of S,{ the carrier of S}:] \/ (Union (coprod X))),(([: the carrier' of S,{ the carrier of S}:] \/ (Union (coprod X))) *):]
[:([: the carrier' of S,{ the carrier of S}:] \/ (Union (coprod X))),(([: the carrier' of S,{ the carrier of S}:] \/ (Union (coprod X))) *):] is non empty Relation-like set
bool [:([: the carrier' of S,{ the carrier of S}:] \/ (Union (coprod X))),(([: the carrier' of S,{ the carrier of S}:] \/ (Union (coprod X))) *):] is non empty set
x is Element of the carrier' of S
[x, the carrier of S] is V26() set
{x, the carrier of S} is non empty set
{x} is non empty set
{{x, the carrier of S},{x}} is non empty set
the_arity_of x is Relation-like K32() -defined the carrier of S -valued Function-like V34() FinSequence-like FinSubsequence-like Element of the carrier of S *
the carrier of S * is non empty functional FinSequence-membered M10( the carrier of S)
len (the_arity_of x) is V4() V5() V6() V10() Element of K32()
y is Relation-like K32() -defined [: the carrier' of S,{ the carrier of S}:] \/ (Union (coprod X)) -valued Function-like V34() FinSequence-like FinSubsequence-like Element of ([: the carrier' of S,{ the carrier of S}:] \/ (Union (coprod X))) *
[[x, the carrier of S],y] is V26() set
{[x, the carrier of S],y} is non empty set
{[x, the carrier of S]} is non empty Relation-like Function-like set
{{[x, the carrier of S],y},{[x, the carrier of S]}} is non empty set
len y is V4() V5() V6() V10() Element of K32()
dom y is Element of bool K32()
tx is Element of [: the carrier' of S,{ the carrier of S}:] \/ (Union (coprod X))
P is Element of the carrier' of S
[P, the carrier of S] is V26() set
{P, the carrier of S} is non empty set
{P} is non empty set
{{P, the carrier of S},{P}} is non empty set
the_arity_of P is Relation-like K32() -defined the carrier of S -valued Function-like V34() FinSequence-like FinSubsequence-like Element of the carrier of S *
len (the_arity_of P) is V4() V5() V6() V10() Element of K32()
O1 is set
y . O1 is set
R is Element of the carrier' of S
[R, the carrier of S] is V26() set
{R, the carrier of S} is non empty set
{R} is non empty set
{{R, the carrier of S},{R}} is non empty set
the_result_sort_of R is Element of the carrier of S
(the_arity_of P) /. O1 is Element of the carrier of S
P is set
y . P is set
O1 is Element of the carrier' of S
[O1, the carrier of S] is V26() set
{O1, the carrier of S} is non empty set
{O1} is non empty set
{{O1, the carrier of S},{O1}} is non empty set
the_result_sort_of O1 is Element of the carrier of S
(the_arity_of x) /. P is Element of the carrier of S
P is Element of the carrier' of S
[P, the carrier of S] is V26() set
{P, the carrier of S} is non empty set
{P} is non empty set
{{P, the carrier of S},{P}} is non empty set
tx is Element of [: the carrier' of S,{ the carrier of S}:] \/ (Union (coprod X))
the_arity_of P is Relation-like K32() -defined the carrier of S -valued Function-like V34() FinSequence-like FinSubsequence-like Element of the carrier of S *
len (the_arity_of P) is V4() V5() V6() V10() Element of K32()
O1 is set
y . O1 is set
R is Element of the carrier' of S
[R, the carrier of S] is V26() set
{R, the carrier of S} is non empty set
{R} is non empty set
{{R, the carrier of S},{R}} is non empty set
the_result_sort_of R is Element of the carrier of S
(the_arity_of P) /. O1 is Element of the carrier of S
S is non empty non void V60() reflexive transitive antisymmetric order-sorted discernable OverloadedRSSign
the carrier of S is non empty set
the carrier' of S is non empty set
{ the carrier of S} is non empty set
[: the carrier' of S,{ the carrier of S}:] is non empty Relation-like set
X is non empty Relation-like the carrier of S -defined Function-like total set
coprod X is non empty Relation-like the carrier of S -defined Function-like total set
Union (coprod X) is set
[: the carrier' of S,{ the carrier of S}:] \/ (Union (coprod X)) is non empty set
(S,X) is Relation-like [: the carrier' of S,{ the carrier of S}:] \/ (Union (coprod X)) -defined ([: the carrier' of S,{ the carrier of S}:] \/ (Union (coprod X))) * -valued Element of bool [:([: the carrier' of S,{ the carrier of S}:] \/ (Union (coprod X))),(([: the carrier' of S,{ the carrier of S}:] \/ (Union (coprod X))) *):]
([: the carrier' of S,{ the carrier of S}:] \/ (Union (coprod X))) * is non empty functional FinSequence-membered M10([: the carrier' of S,{ the carrier of S}:] \/ (Union (coprod X)))
[:([: the carrier' of S,{ the carrier of S}:] \/ (Union (coprod X))),(([: the carrier' of S,{ the carrier of S}:] \/ (Union (coprod X))) *):] is non empty Relation-like set
bool [:([: the carrier' of S,{ the carrier of S}:] \/ (Union (coprod X))),(([: the carrier' of S,{ the carrier of S}:] \/ (Union (coprod X))) *):] is non empty set
DTConstrStr(# ([: the carrier' of S,{ the carrier of S}:] \/ (Union (coprod X))),(S,X) #) is non empty strict DTConstrStr
S is non empty non void V60() reflexive transitive antisymmetric order-sorted discernable OverloadedRSSign
the carrier of S is non empty set
X is non empty Relation-like the carrier of S -defined Function-like total set
(S,X) is DTConstrStr
the carrier' of S is non empty set
{ the carrier of S} is non empty set
[: the carrier' of S,{ the carrier of S}:] is non empty Relation-like set
coprod X is non empty Relation-like the carrier of S -defined Function-like total set
Union (coprod X) is set
[: the carrier' of S,{ the carrier of S}:] \/ (Union (coprod X)) is non empty set
(S,X) is Relation-like [: the carrier' of S,{ the carrier of S}:] \/ (Union (coprod X)) -defined ([: the carrier' of S,{ the carrier of S}:] \/ (Union (coprod X))) * -valued Element of bool [:([: the carrier' of S,{ the carrier of S}:] \/ (Union (coprod X))),(([: the carrier' of S,{ the carrier of S}:] \/ (Union (coprod X))) *):]
([: the carrier' of S,{ the carrier of S}:] \/ (Union (coprod X))) * is non empty functional FinSequence-membered M10([: the carrier' of S,{ the carrier of S}:] \/ (Union (coprod X)))
[:([: the carrier' of S,{ the carrier of S}:] \/ (Union (coprod X))),(([: the carrier' of S,{ the carrier of S}:] \/ (Union (coprod X))) *):] is non empty Relation-like set
bool [:([: the carrier' of S,{ the carrier of S}:] \/ (Union (coprod X))),(([: the carrier' of S,{ the carrier of S}:] \/ (Union (coprod X))) *):] is non empty set
DTConstrStr(# ([: the carrier' of S,{ the carrier of S}:] \/ (Union (coprod X))),(S,X) #) is non empty strict DTConstrStr
S is non empty non void V60() reflexive transitive antisymmetric order-sorted discernable OverloadedRSSign
the carrier of S is non empty set
the carrier' of S is non empty set
{ the carrier of S} is non empty set
[: the carrier' of S,{ the carrier of S}:] is non empty Relation-like set
X is non empty Relation-like non-empty non empty-yielding the carrier of S -defined Function-like total set
(S,X) is non empty strict DTConstrStr
coprod X is non empty Relation-like non-empty non empty-yielding the carrier of S -defined Function-like total set
Union (coprod X) is non empty set
[: the carrier' of S,{ the carrier of S}:] \/ (Union (coprod X)) is non empty set
(S,X) is Relation-like [: the carrier' of S,{ the carrier of S}:] \/ (Union (coprod X)) -defined ([: the carrier' of S,{ the carrier of S}:] \/ (Union (coprod X))) * -valued Element of bool [:([: the carrier' of S,{ the carrier of S}:] \/ (Union (coprod X))),(([: the carrier' of S,{ the carrier of S}:] \/ (Union (coprod X))) *):]
([: the carrier' of S,{ the carrier of S}:] \/ (Union (coprod X))) * is non empty functional FinSequence-membered M10([: the carrier' of S,{ the carrier of S}:] \/ (Union (coprod X)))
[:([: the carrier' of S,{ the carrier of S}:] \/ (Union (coprod X))),(([: the carrier' of S,{ the carrier of S}:] \/ (Union (coprod X))) *):] is non empty Relation-like set
bool [:([: the carrier' of S,{ the carrier of S}:] \/ (Union (coprod X))),(([: the carrier' of S,{ the carrier of S}:] \/ (Union (coprod X))) *):] is non empty set
DTConstrStr(# ([: the carrier' of S,{ the carrier of S}:] \/ (Union (coprod X))),(S,X) #) is non empty strict DTConstrStr
NonTerminals (S,X) is set
Terminals (S,X) is set
the carrier of (S,X) is non empty set
(Terminals (S,X)) \/ (NonTerminals (S,X)) is set
t is set
{ b1 where b1 is Element of the carrier of (S,X) : ex b2 being Relation-like K32() -defined Function-like V34() FinSequence-like FinSubsequence-like set st b1 ==> b2 } is set
tx is Element of the carrier of (S,X)
P is Relation-like K32() -defined Function-like V34() FinSequence-like FinSubsequence-like set
P is Relation-like K32() -defined Function-like V34() FinSequence-like FinSubsequence-like set
[tx,P] is V26() set
{tx,P} is non empty set
{tx} is non empty set
{{tx,P},{tx}} is non empty set
the Rules of (S,X) is Relation-like the carrier of (S,X) -defined the carrier of (S,X) * -valued Element of bool [: the carrier of (S,X),( the carrier of (S,X) *):]
the carrier of (S,X) * is non empty functional FinSequence-membered M10( the carrier of (S,X))
[: the carrier of (S,X),( the carrier of (S,X) *):] is non empty Relation-like set
bool [: the carrier of (S,X),( the carrier of (S,X) *):] is non empty set
R is Element of [: the carrier' of S,{ the carrier of S}:] \/ (Union (coprod X))
O1 is Relation-like K32() -defined [: the carrier' of S,{ the carrier of S}:] \/ (Union (coprod X)) -valued Function-like V34() FinSequence-like FinSubsequence-like Element of ([: the carrier' of S,{ the carrier of S}:] \/ (Union (coprod X))) *
[R,O1] is V26() set
{R,O1} is non empty set
{R} is non empty set
{{R,O1},{R}} is non empty set
t is set
tx is Element of the carrier' of S
P is Element of { the carrier of S}
[tx,P] is V26() set
{tx,P} is non empty set
{tx} is non empty set
{{tx,P},{tx}} is non empty set
the_arity_of tx is Relation-like K32() -defined the carrier of S -valued Function-like V34() FinSequence-like FinSubsequence-like Element of the carrier of S *
the carrier of S * is non empty functional FinSequence-membered M10( the carrier of S)
len (the_arity_of tx) is V4() V5() V6() V10() Element of K32()
Seg (len (the_arity_of tx)) is V34() V41( len (the_arity_of tx)) Element of bool K32()
R is set
(the_arity_of tx) /. R is Element of the carrier of S
dom (the_arity_of tx) is Element of bool K32()
(the_arity_of tx) . R is set
proj2 (the_arity_of tx) is set
X . ((the_arity_of tx) . R) is set
i is set
[i,((the_arity_of tx) . R)] is V26() set
{i,((the_arity_of tx) . R)} is non empty set
{i} is non empty set
{{i,((the_arity_of tx) . R)},{i}} is non empty set
s is V26() set
coprod (((the_arity_of tx) /. R),X) is set
coprod (((the_arity_of tx) . R),X) is set
R is Relation-like Function-like set
proj1 R is set
i is Relation-like K32() -defined Function-like V34() FinSequence-like FinSubsequence-like set
proj2 i is set
s is set
dom i is Element of bool K32()
a is set
i . a is set
(the_arity_of tx) /. a is Element of the carrier of S
b is Element of the carrier of S
coprod (b,X) is set
dom (coprod X) is non empty Element of bool the carrier of S
bool the carrier of S is non empty set
(coprod X) . b is non empty set
proj2 (coprod X) is non empty V205() set
union (proj2 (coprod X)) is set
s is Relation-like K32() -defined [: the carrier' of S,{ the carrier of S}:] \/ (Union (coprod X)) -valued Function-like V34() FinSequence-like FinSubsequence-like FinSequence of [: the carrier' of S,{ the carrier of S}:] \/ (Union (coprod X))
b is set
a is Relation-like K32() -defined [: the carrier' of S,{ the carrier of S}:] \/ (Union (coprod X)) -valued Function-like V34() FinSequence-like FinSubsequence-like Element of ([: the carrier' of S,{ the carrier of S}:] \/ (Union (coprod X))) *
dom a is Element of bool K32()
(the_arity_of tx) /. b is Element of the carrier of S
a . b is set
ta is Element of the carrier of S
coprod (ta,X) is set
dom (coprod X) is non empty Element of bool the carrier of S
bool the carrier of S is non empty set
(coprod X) . ta is non empty set
proj2 (coprod X) is non empty V205() set
union (proj2 (coprod X)) is set
tb is Element of the carrier' of S
[tb, the carrier of S] is V26() set
{tb, the carrier of S} is non empty set
{tb} is non empty set
{{tb, the carrier of S},{tb}} is non empty set
the_result_sort_of tb is Element of the carrier of S
[tx, the carrier of S] is V26() set
{tx, the carrier of S} is non empty set
{{tx, the carrier of S},{tx}} is non empty set
len a is V4() V5() V6() V10() Element of K32()
b is Element of the carrier of (S,X)
[b,a] is V26() set
{b,a} is non empty set
{b} is non empty set
{{b,a},{b}} is non empty set
{ b1 where b1 is Element of the carrier of (S,X) : ex b2 being Relation-like K32() -defined Function-like V34() FinSequence-like FinSubsequence-like set st b1 ==> b2 } is set
t is set
t is set
S is non empty non void V60() reflexive transitive antisymmetric order-sorted discernable OverloadedRSSign
the carrier of S is non empty set
X is non empty Relation-like non-empty non empty-yielding the carrier of S -defined Function-like total set
(S,X) is non empty strict DTConstrStr
the carrier' of S is non empty set
{ the carrier of S} is non empty set
[: the carrier' of S,{ the carrier of S}:] is non empty Relation-like set
coprod X is non empty Relation-like non-empty non empty-yielding the carrier of S -defined Function-like total set
Union (coprod X) is non empty set
[: the carrier' of S,{ the carrier of S}:] \/ (Union (coprod X)) is non empty set
(S,X) is Relation-like [: the carrier' of S,{ the carrier of S}:] \/ (Union (coprod X)) -defined ([: the carrier' of S,{ the carrier of S}:] \/ (Union (coprod X))) * -valued Element of bool [:([: the carrier' of S,{ the carrier of S}:] \/ (Union (coprod X))),(([: the carrier' of S,{ the carrier of S}:] \/ (Union (coprod X))) *):]
([: the carrier' of S,{ the carrier of S}:] \/ (Union (coprod X))) * is non empty functional FinSequence-membered M10([: the carrier' of S,{ the carrier of S}:] \/ (Union (coprod X)))
[:([: the carrier' of S,{ the carrier of S}:] \/ (Union (coprod X))),(([: the carrier' of S,{ the carrier of S}:] \/ (Union (coprod X))) *):] is non empty Relation-like set
bool [:([: the carrier' of S,{ the carrier of S}:] \/ (Union (coprod X))),(([: the carrier' of S,{ the carrier of S}:] \/ (Union (coprod X))) *):] is non empty set
DTConstrStr(# ([: the carrier' of S,{ the carrier of S}:] \/ (Union (coprod X))),(S,X) #) is non empty strict DTConstrStr
Terminals (S,X) is set
NonTerminals (S,X) is set
the carrier of (S,X) is non empty set
FinTrees the carrier of (S,X) is non empty functional constituted-DTrees DTree-set of the carrier of (S,X)
TS (S,X) is functional constituted-DTrees Element of bool (FinTrees the carrier of (S,X))
bool (FinTrees the carrier of (S,X)) is non empty set
t is Element of the carrier of (S,X)
tx is Element of the carrier' of S
P is Element of { the carrier of S}
[tx,P] is V26() set
{tx,P} is non empty set
{tx} is non empty set
{{tx,P},{tx}} is non empty set
the_arity_of tx is Relation-like K32() -defined the carrier of S -valued Function-like V34() FinSequence-like FinSubsequence-like Element of the carrier of S *
the carrier of S * is non empty functional FinSequence-membered M10( the carrier of S)
len (the_arity_of tx) is V4() V5() V6() V10() Element of K32()
Seg (len (the_arity_of tx)) is V34() V41( len (the_arity_of tx)) Element of bool K32()
R is set
(the_arity_of tx) /. R is Element of the carrier of S
dom (the_arity_of tx) is Element of bool K32()
(the_arity_of tx) . R is set
proj2 (the_arity_of tx) is set
X . ((the_arity_of tx) . R) is set
i is set
[i,((the_arity_of tx) . R)] is V26() set
{i,((the_arity_of tx) . R)} is non empty set
{i} is non empty set
{{i,((the_arity_of tx) . R)},{i}} is non empty set
s is V26() set
coprod (((the_arity_of tx) /. R),X) is set
coprod (((the_arity_of tx) . R),X) is set
R is Relation-like Function-like set
proj1 R is set
i is Relation-like K32() -defined Function-like V34() FinSequence-like FinSubsequence-like set
proj2 i is set
s is set
dom i is Element of bool K32()
a is set
i . a is set
(the_arity_of tx) /. a is Element of the carrier of S
b is Element of the carrier of S
coprod (b,X) is set
dom (coprod X) is non empty Element of bool the carrier of S
bool the carrier of S is non empty set
(coprod X) . b is non empty set
proj2 (coprod X) is non empty V205() set
union (proj2 (coprod X)) is set
s is Relation-like K32() -defined [: the carrier' of S,{ the carrier of S}:] \/ (Union (coprod X)) -valued Function-like V34() FinSequence-like FinSubsequence-like FinSequence of [: the carrier' of S,{ the carrier of S}:] \/ (Union (coprod X))
a is Relation-like K32() -defined [: the carrier' of S,{ the carrier of S}:] \/ (Union (coprod X)) -valued Function-like V34() FinSequence-like FinSubsequence-like Element of ([: the carrier' of S,{ the carrier of S}:] \/ (Union (coprod X))) *
dom a is Element of bool K32()
b is Relation-like Function-like set
proj1 b is set
ta is Relation-like K32() -defined Function-like V34() FinSequence-like FinSubsequence-like set
proj2 ta is set
tb is set
dom ta is Element of bool K32()
t1 is set
ta . t1 is set
a . t1 is set
proj2 a is set
(the_arity_of tx) /. t1 is Element of the carrier of S
t1 is Element of the carrier of S
coprod (t1,X) is set
dom (coprod X) is non empty Element of bool the carrier of S
bool the carrier of S is non empty set
(coprod X) . t1 is non empty set
proj2 (coprod X) is non empty V205() set
union (proj2 (coprod X)) is set
t2 is Element of the carrier of (S,X)
root-tree (a . t1) is Relation-like Function-like DecoratedTree-like set
tb is Relation-like K32() -defined FinTrees the carrier of (S,X) -valued Function-like V32() V33() V34() FinSequence-like FinSubsequence-like FinSequence of TS (S,X)
roots tb is Relation-like K32() -defined the carrier of (S,X) -valued Function-like V34() FinSequence-like FinSubsequence-like FinSequence of the carrier of (S,X)
t1 is set
(roots tb) . t1 is set
a . t1 is set
t2 is V4() V5() V6() V10() set
tb . t2 is Relation-like Function-like set
(roots tb) . t2 is set
tb . t1 is Relation-like Function-like set
root-tree (a . t1) is Relation-like Function-like DecoratedTree-like set
t1 is Relation-like Function-like DecoratedTree-like set
t1 . {} is set
t1 is set
(the_arity_of tx) /. t1 is Element of the carrier of S
a . t1 is set
t2 is Element of the carrier of S
coprod (t2,X) is set
dom (coprod X) is non empty Element of bool the carrier of S
bool the carrier of S is non empty set
(coprod X) . t2 is non empty set
proj2 (coprod X) is non empty V205() set
union (proj2 (coprod X)) is set
t1 is Element of the carrier' of S
[t1, the carrier of S] is V26() set
{t1, the carrier of S} is non empty set
{t1} is non empty set
{{t1, the carrier of S},{t1}} is non empty set
the_result_sort_of t1 is Element of the carrier of S
len a is V4() V5() V6() V10() Element of K32()
[t,a] is V26() set
{t,a} is non empty set
{t} is non empty set
{{t,a},{t}} is non empty set
dom (roots tb) is Element of bool K32()
dom tb is Element of bool K32()
S is non empty non void V60() reflexive transitive antisymmetric order-sorted discernable OverloadedRSSign
the carrier of S is non empty set
X is non empty Relation-like non-empty non empty-yielding the carrier of S -defined Function-like total set
(S,X) is non empty strict with_terminals with_nonterminals with_useful_nonterminals DTConstrStr
the carrier' of S is non empty set
{ the carrier of S} is non empty set
[: the carrier' of S,{ the carrier of S}:] is non empty Relation-like set
coprod X is non empty Relation-like non-empty non empty-yielding the carrier of S -defined Function-like total set
Union (coprod X) is non empty set
[: the carrier' of S,{ the carrier of S}:] \/ (Union (coprod X)) is non empty set
(S,X) is Relation-like [: the carrier' of S,{ the carrier of S}:] \/ (Union (coprod X)) -defined ([: the carrier' of S,{ the carrier of S}:] \/ (Union (coprod X))) * -valued Element of bool [:([: the carrier' of S,{ the carrier of S}:] \/ (Union (coprod X))),(([: the carrier' of S,{ the carrier of S}:] \/ (Union (coprod X))) *):]
([: the carrier' of S,{ the carrier of S}:] \/ (Union (coprod X))) * is non empty functional FinSequence-membered M10([: the carrier' of S,{ the carrier of S}:] \/ (Union (coprod X)))
[:([: the carrier' of S,{ the carrier of S}:] \/ (Union (coprod X))),(([: the carrier' of S,{ the carrier of S}:] \/ (Union (coprod X))) *):] is non empty Relation-like set
bool [:([: the carrier' of S,{ the carrier of S}:] \/ (Union (coprod X))),(([: the carrier' of S,{ the carrier of S}:] \/ (Union (coprod X))) *):] is non empty set
DTConstrStr(# ([: the carrier' of S,{ the carrier of S}:] \/ (Union (coprod X))),(S,X) #) is non empty strict DTConstrStr
Terminals (S,X) is non empty Element of bool the carrier of (S,X)
the carrier of (S,X) is non empty set
bool the carrier of (S,X) is non empty set
x is set
proj2 (coprod X) is non empty V205() set
union (proj2 (coprod X)) is set
t is set
dom (coprod X) is non empty Element of bool the carrier of S
bool the carrier of S is non empty set
tx is set
(coprod X) . tx is set
P is Element of the carrier of S
(coprod X) . P is non empty set
coprod (P,X) is set
X . P is non empty set
O1 is set
[O1,P] is V26() set
{O1,P} is non empty set
{O1} is non empty set
{{O1,P},{O1}} is non empty set
tx is set
t is Element of the carrier of S
X . t is non empty set
[tx,t] is V26() set
{tx,t} is non empty set
{tx} is non empty set
{{tx,t},{tx}} is non empty set
coprod (t,X) is set
(coprod X) . t is non empty set
dom (coprod X) is non empty Element of bool the carrier of S
bool the carrier of S is non empty set
S is non empty non void V60() reflexive transitive antisymmetric order-sorted discernable OverloadedRSSign
the carrier of S is non empty set
the carrier' of S is non empty set
x is Element of the carrier' of S
[x, the carrier of S] is V26() set
{x, the carrier of S} is non empty set
{x} is non empty set
{{x, the carrier of S},{x}} is non empty set
X is non empty Relation-like non-empty non empty-yielding the carrier of S -defined Function-like total set
(S,X) is non empty strict with_terminals with_nonterminals with_useful_nonterminals DTConstrStr
{ the carrier of S} is non empty set
[: the carrier' of S,{ the carrier of S}:] is non empty Relation-like set
coprod X is non empty Relation-like non-empty non empty-yielding the carrier of S -defined Function-like total set
Union (coprod X) is non empty set
[: the carrier' of S,{ the carrier of S}:] \/ (Union (coprod X)) is non empty set
(S,X) is Relation-like [: the carrier' of S,{ the carrier of S}:] \/ (Union (coprod X)) -defined ([: the carrier' of S,{ the carrier of S}:] \/ (Union (coprod X))) * -valued Element of bool [:([: the carrier' of S,{ the carrier of S}:] \/ (Union (coprod X))),(([: the carrier' of S,{ the carrier of S}:] \/ (Union (coprod X))) *):]
([: the carrier' of S,{ the carrier of S}:] \/ (Union (coprod X))) * is non empty functional FinSequence-membered M10([: the carrier' of S,{ the carrier of S}:] \/ (Union (coprod X)))
[:([: the carrier' of S,{ the carrier of S}:] \/ (Union (coprod X))),(([: the carrier' of S,{ the carrier of S}:] \/ (Union (coprod X))) *):] is non empty Relation-like set
bool [:([: the carrier' of S,{ the carrier of S}:] \/ (Union (coprod X))),(([: the carrier' of S,{ the carrier of S}:] \/ (Union (coprod X))) *):] is non empty set
DTConstrStr(# ([: the carrier' of S,{ the carrier of S}:] \/ (Union (coprod X))),(S,X) #) is non empty strict DTConstrStr
the carrier of (S,X) is non empty set
NonTerminals (S,X) is non empty Element of bool the carrier of (S,X)
bool the carrier of (S,X) is non empty set
S is non empty non void V60() reflexive transitive antisymmetric order-sorted discernable OverloadedRSSign
the carrier of S is non empty set
X is non empty Relation-like non-empty non empty-yielding the carrier of S -defined Function-like total set
(S,X) is non empty strict with_terminals with_nonterminals with_useful_nonterminals DTConstrStr
the carrier' of S is non empty set
{ the carrier of S} is non empty set
[: the carrier' of S,{ the carrier of S}:] is non empty Relation-like set
coprod X is non empty Relation-like non-empty non empty-yielding the carrier of S -defined Function-like total set
Union (coprod X) is non empty set
[: the carrier' of S,{ the carrier of S}:] \/ (Union (coprod X)) is non empty set
(S,X) is Relation-like [: the carrier' of S,{ the carrier of S}:] \/ (Union (coprod X)) -defined ([: the carrier' of S,{ the carrier of S}:] \/ (Union (coprod X))) * -valued Element of bool [:([: the carrier' of S,{ the carrier of S}:] \/ (Union (coprod X))),(([: the carrier' of S,{ the carrier of S}:] \/ (Union (coprod X))) *):]
([: the carrier' of S,{ the carrier of S}:] \/ (Union (coprod X))) * is non empty functional FinSequence-membered M10([: the carrier' of S,{ the carrier of S}:] \/ (Union (coprod X)))
[:([: the carrier' of S,{ the carrier of S}:] \/ (Union (coprod X))),(([: the carrier' of S,{ the carrier of S}:] \/ (Union (coprod X))) *):] is non empty Relation-like set
bool [:([: the carrier' of S,{ the carrier of S}:] \/ (Union (coprod X))),(([: the carrier' of S,{ the carrier of S}:] \/ (Union (coprod X))) *):] is non empty set
DTConstrStr(# ([: the carrier' of S,{ the carrier of S}:] \/ (Union (coprod X))),(S,X) #) is non empty strict DTConstrStr
the carrier of (S,X) is non empty set
FinTrees the carrier of (S,X) is non empty functional constituted-DTrees DTree-set of the carrier of (S,X)
TS (S,X) is non empty functional constituted-DTrees Element of bool (FinTrees the carrier of (S,X))
bool (FinTrees the carrier of (S,X)) is non empty set
x is Element of the carrier of S
{ b1 where b1 is Relation-like the carrier of (S,X) -valued Function-like DecoratedTree-like Element of TS (S,X) : ( ex b2 being Element of the carrier of S ex b3 being set st
( b2 <= x & b3 in X . b2 & b1 = root-tree [b3,b2] ) or ex b2 being Element of the carrier' of S st
( [b2, the carrier of S] = b1 . {} & the_result_sort_of b2 <= x ) ) } is set
bool (TS (S,X)) is non empty set
t is set
tx is Relation-like the carrier of (S,X) -valued Function-like DecoratedTree-like Element of TS (S,X)
P is Element of the carrier of S
O1 is set
X . P is non empty set
[O1,P] is V26() set
{O1,P} is non empty set
{O1} is non empty set
{{O1,P},{O1}} is non empty set
root-tree [O1,P] is Relation-like Function-like DecoratedTree-like set
R is Element of the carrier' of S
[R, the carrier of S] is V26() set
{R, the carrier of S} is non empty set
{R} is non empty set
{{R, the carrier of S},{R}} is non empty set
tx . {} is set
the_result_sort_of R is Element of the carrier of S
S is non empty non void V60() reflexive transitive antisymmetric order-sorted discernable OverloadedRSSign
the carrier of S is non empty set
X is non empty Relation-like non-empty non empty-yielding the carrier of S -defined Function-like total set
x is Element of the carrier of S
(S,X,x) is functional constituted-DTrees Element of bool (TS (S,X))
(S,X) is non empty strict with_terminals with_nonterminals with_useful_nonterminals DTConstrStr
the carrier' of S is non empty set
{ the carrier of S} is non empty set
[: the carrier' of S,{ the carrier of S}:] is non empty Relation-like set
coprod X is non empty Relation-like non-empty non empty-yielding the carrier of S -defined Function-like total set
Union (coprod X) is non empty set
[: the carrier' of S,{ the carrier of S}:] \/ (Union (coprod X)) is non empty set
(S,X) is Relation-like [: the carrier' of S,{ the carrier of S}:] \/ (Union (coprod X)) -defined ([: the carrier' of S,{ the carrier of S}:] \/ (Union (coprod X))) * -valued Element of bool [:([: the carrier' of S,{ the carrier of S}:] \/ (Union (coprod X))),(([: the carrier' of S,{ the carrier of S}:] \/ (Union (coprod X))) *):]
([: the carrier' of S,{ the carrier of S}:] \/ (Union (coprod X))) * is non empty functional FinSequence-membered M10([: the carrier' of S,{ the carrier of S}:] \/ (Union (coprod X)))
[:([: the carrier' of S,{ the carrier of S}:] \/ (Union (coprod X))),(([: the carrier' of S,{ the carrier of S}:] \/ (Union (coprod X))) *):] is non empty Relation-like set
bool [:([: the carrier' of S,{ the carrier of S}:] \/ (Union (coprod X))),(([: the carrier' of S,{ the carrier of S}:] \/ (Union (coprod X))) *):] is non empty set
DTConstrStr(# ([: the carrier' of S,{ the carrier of S}:] \/ (Union (coprod X))),(S,X) #) is non empty strict DTConstrStr
TS (S,X) is non empty functional constituted-DTrees Element of bool (FinTrees the carrier of (S,X))
the carrier of (S,X) is non empty set
FinTrees the carrier of (S,X) is non empty functional constituted-DTrees DTree-set of the carrier of (S,X)
bool (FinTrees the carrier of (S,X)) is non empty set
bool (TS (S,X)) is non empty set
{ b1 where b1 is Relation-like the carrier of (S,X) -valued Function-like DecoratedTree-like Element of TS (S,X) : ( ex b2 being Element of the carrier of S ex b3 being set st
( b2 <= x & b3 in X . b2 & b1 = root-tree [b3,b2] ) or ex b2 being Element of the carrier' of S st
( [b2, the carrier of S] = b1 . {} & the_result_sort_of b2 <= x ) ) } is set
dom (coprod X) is non empty Element of bool the carrier of S
bool the carrier of S is non empty set
(coprod X) . x is non empty set
proj2 (coprod X) is non empty V205() set
coprod (x,X) is set
X . x is non empty set
t is set
[t,x] is V26() set
{t,x} is non empty set
{t} is non empty set
{{t,x},{t}} is non empty set
Terminals (S,X) is non empty Element of bool the carrier of (S,X)
bool the carrier of (S,X) is non empty set
union (proj2 (coprod X)) is set
P is Element of the carrier of (S,X)
root-tree P is Relation-like the carrier of (S,X) -valued Function-like DecoratedTree-like Element of FinTrees the carrier of (S,X)
O1 is Relation-like the carrier of (S,X) -valued Function-like DecoratedTree-like Element of TS (S,X)
S is non empty non void V60() reflexive transitive antisymmetric order-sorted discernable OverloadedRSSign
the carrier of S is non empty set
X is non empty Relation-like non-empty non empty-yielding the carrier of S -defined Function-like total set
(S,X) is non empty strict with_terminals with_nonterminals with_useful_nonterminals DTConstrStr
the carrier' of S is non empty set
{ the carrier of S} is non empty set
[: the carrier' of S,{ the carrier of S}:] is non empty Relation-like set
coprod X is non empty Relation-like non-empty non empty-yielding the carrier of S -defined Function-like total set
Union (coprod X) is non empty set
[: the carrier' of S,{ the carrier of S}:] \/ (Union (coprod X)) is non empty set
(S,X) is Relation-like [: the carrier' of S,{ the carrier of S}:] \/ (Union (coprod X)) -defined ([: the carrier' of S,{ the carrier of S}:] \/ (Union (coprod X))) * -valued Element of bool [:([: the carrier' of S,{ the carrier of S}:] \/ (Union (coprod X))),(([: the carrier' of S,{ the carrier of S}:] \/ (Union (coprod X))) *):]
([: the carrier' of S,{ the carrier of S}:] \/ (Union (coprod X))) * is non empty functional FinSequence-membered M10([: the carrier' of S,{ the carrier of S}:] \/ (Union (coprod X)))
[:([: the carrier' of S,{ the carrier of S}:] \/ (Union (coprod X))),(([: the carrier' of S,{ the carrier of S}:] \/ (Union (coprod X))) *):] is non empty Relation-like set
bool [:([: the carrier' of S,{ the carrier of S}:] \/ (Union (coprod X))),(([: the carrier' of S,{ the carrier of S}:] \/ (Union (coprod X))) *):] is non empty set
DTConstrStr(# ([: the carrier' of S,{ the carrier of S}:] \/ (Union (coprod X))),(S,X) #) is non empty strict DTConstrStr
TS (S,X) is non empty functional constituted-DTrees Element of bool (FinTrees the carrier of (S,X))
the carrier of (S,X) is non empty set
FinTrees the carrier of (S,X) is non empty functional constituted-DTrees DTree-set of the carrier of (S,X)
bool (FinTrees the carrier of (S,X)) is non empty set
bool (TS (S,X)) is non empty set
x is Relation-like Function-like set
proj1 x is set
y is non empty Relation-like the carrier of S -defined Function-like total set
t is Element of the carrier of S
tx is Element of the carrier of S
y . t is set
y . tx is set
P is set
(S,X,t) is non empty functional constituted-DTrees Element of bool (TS (S,X))
{ b1 where b1 is Relation-like the carrier of (S,X) -valued Function-like DecoratedTree-like Element of TS (S,X) : ( ex b2 being Element of the carrier of S ex b3 being set st
( b2 <= t & b3 in X . b2 & b1 = root-tree [b3,b2] ) or ex b2 being Element of the carrier' of S st
( [b2, the carrier of S] = b1 . {} & the_result_sort_of b2 <= t ) ) } is set
O1 is Relation-like the carrier of (S,X) -valued Function-like DecoratedTree-like Element of TS (S,X)
O1 . {} is set
R is Element of the carrier of S
i is set
X . R is non empty set
[i,R] is V26() set
{i,R} is non empty set
{i} is non empty set
{{i,R},{i}} is non empty set
root-tree [i,R] is Relation-like Function-like DecoratedTree-like set
R is Element of the carrier of S
i is set
X . R is non empty set
[i,R] is V26() set
{i,R} is non empty set
{i} is non empty set
{{i,R},{i}} is non empty set
root-tree [i,R] is Relation-like Function-like DecoratedTree-like set
i is Element of the carrier' of S
[i, the carrier of S] is V26() set
{i, the carrier of S} is non empty set
{i} is non empty set
{{i, the carrier of S},{i}} is non empty set
the_result_sort_of i is Element of the carrier of S
i is Element of the carrier' of S
[i, the carrier of S] is V26() set
{i, the carrier of S} is non empty set
{i} is non empty set
{{i, the carrier of S},{i}} is non empty set
the_result_sort_of i is Element of the carrier of S
R is Element of the carrier of S
R is Element of the carrier of S
i is set
X . R is non empty set
[i,R] is V26() set
{i,R} is non empty set
{i} is non empty set
{{i,R},{i}} is non empty set
root-tree [i,R] is Relation-like Function-like DecoratedTree-like set
s is Element of the carrier' of S
[s, the carrier of S] is V26() set
{s, the carrier of S} is non empty set
{s} is non empty set
{{s, the carrier of S},{s}} is non empty set
the_result_sort_of s is Element of the carrier of S
(S,X,tx) is non empty functional constituted-DTrees Element of bool (TS (S,X))
{ b1 where b1 is Relation-like the carrier of (S,X) -valued Function-like DecoratedTree-like Element of TS (S,X) : ( ex b2 being Element of the carrier of S ex b3 being set st
( b2 <= tx & b3 in X . b2 & b1 = root-tree [b3,b2] ) or ex b2 being Element of the carrier' of S st
( [b2, the carrier of S] = b1 . {} & the_result_sort_of b2 <= tx ) ) } is set
R is Element of the carrier of S
i is set
X . R is non empty set
[i,R] is V26() set
{i,R} is non empty set
{i} is non empty set
{{i,R},{i}} is non empty set
root-tree [i,R] is Relation-like Function-like DecoratedTree-like set
s is Element of the carrier' of S
[s, the carrier of S] is V26() set
{s, the carrier of S} is non empty set
{s} is non empty set
{{s, the carrier of S},{s}} is non empty set
the_result_sort_of s is Element of the carrier of S
t is non empty Relation-like the carrier of S -defined Function-like total order-sorted set
tx is Element of the carrier of S
t . tx is set
(S,X,tx) is non empty functional constituted-DTrees Element of bool (TS (S,X))
{ b1 where b1 is Relation-like the carrier of (S,X) -valued Function-like DecoratedTree-like Element of TS (S,X) : ( ex b2 being Element of the carrier of S ex b3 being set st
( b2 <= tx & b3 in X . b2 & b1 = root-tree [b3,b2] ) or ex b2 being Element of the carrier' of S st
( [b2, the carrier of S] = b1 . {} & the_result_sort_of b2 <= tx ) ) } is set
x is non empty Relation-like the carrier of S -defined Function-like total order-sorted set
y is non empty Relation-like the carrier of S -defined Function-like total order-sorted set
t is set
x . t is set
y . t is set
tx is Element of the carrier of S
x . tx is set
(S,X,tx) is non empty functional constituted-DTrees Element of bool (TS (S,X))
(S,X) is non empty strict with_terminals with_nonterminals with_useful_nonterminals DTConstrStr
the carrier' of S is non empty set
{ the carrier of S} is non empty set
[: the carrier' of S,{ the carrier of S}:] is non empty Relation-like set
coprod X is non empty Relation-like non-empty non empty-yielding the carrier of S -defined Function-like total set
Union (coprod X) is non empty set
[: the carrier' of S,{ the carrier of S}:] \/ (Union (coprod X)) is non empty set
(S,X) is Relation-like [: the carrier' of S,{ the carrier of S}:] \/ (Union (coprod X)) -defined ([: the carrier' of S,{ the carrier of S}:] \/ (Union (coprod X))) * -valued Element of bool [:([: the carrier' of S,{ the carrier of S}:] \/ (Union (coprod X))),(([: the carrier' of S,{ the carrier of S}:] \/ (Union (coprod X))) *):]
([: the carrier' of S,{ the carrier of S}:] \/ (Union (coprod X))) * is non empty functional FinSequence-membered M10([: the carrier' of S,{ the carrier of S}:] \/ (Union (coprod X)))
[:([: the carrier' of S,{ the carrier of S}:] \/ (Union (coprod X))),(([: the carrier' of S,{ the carrier of S}:] \/ (Union (coprod X))) *):] is non empty Relation-like set
bool [:([: the carrier' of S,{ the carrier of S}:] \/ (Union (coprod X))),(([: the carrier' of S,{ the carrier of S}:] \/ (Union (coprod X))) *):] is non empty set
DTConstrStr(# ([: the carrier' of S,{ the carrier of S}:] \/ (Union (coprod X))),(S,X) #) is non empty strict DTConstrStr
TS (S,X) is non empty functional constituted-DTrees Element of bool (FinTrees the carrier of (S,X))
the carrier of (S,X) is non empty set
FinTrees the carrier of (S,X) is non empty functional constituted-DTrees DTree-set of the carrier of (S,X)
bool (FinTrees the carrier of (S,X)) is non empty set
bool (TS (S,X)) is non empty set
{ b1 where b1 is Relation-like the carrier of (S,X) -valued Function-like DecoratedTree-like Element of TS (S,X) : ( ex b2 being Element of the carrier of S ex b3 being set st
( b2 <= tx & b3 in X . b2 & b1 = root-tree [b3,b2] ) or ex b2 being Element of the carrier' of S st
( [b2, the carrier of S] = b1 . {} & the_result_sort_of b2 <= tx ) ) } is set
S is non empty non void V60() reflexive transitive antisymmetric order-sorted discernable OverloadedRSSign
the carrier of S is non empty set
X is non empty Relation-like non-empty non empty-yielding the carrier of S -defined Function-like total set
(S,X) is non empty Relation-like the carrier of S -defined Function-like total order-sorted set
x is set
(S,X) . x is set
y is Element of the carrier of S
(S,X) . y is set
(S,X,y) is non empty functional constituted-DTrees Element of bool (TS (S,X))
(S,X) is non empty strict with_terminals with_nonterminals with_useful_nonterminals DTConstrStr
the carrier' of S is non empty set
{ the carrier of S} is non empty set
[: the carrier' of S,{ the carrier of S}:] is non empty Relation-like set
coprod X is non empty Relation-like non-empty non empty-yielding the carrier of S -defined Function-like total set
Union (coprod X) is non empty set
[: the carrier' of S,{ the carrier of S}:] \/ (Union (coprod X)) is non empty set
(S,X) is Relation-like [: the carrier' of S,{ the carrier of S}:] \/ (Union (coprod X)) -defined ([: the carrier' of S,{ the carrier of S}:] \/ (Union (coprod X))) * -valued Element of bool [:([: the carrier' of S,{ the carrier of S}:] \/ (Union (coprod X))),(([: the carrier' of S,{ the carrier of S}:] \/ (Union (coprod X))) *):]
([: the carrier' of S,{ the carrier of S}:] \/ (Union (coprod X))) * is non empty functional FinSequence-membered M10([: the carrier' of S,{ the carrier of S}:] \/ (Union (coprod X)))
[:([: the carrier' of S,{ the carrier of S}:] \/ (Union (coprod X))),(([: the carrier' of S,{ the carrier of S}:] \/ (Union (coprod X))) *):] is non empty Relation-like set
bool [:([: the carrier' of S,{ the carrier of S}:] \/ (Union (coprod X))),(([: the carrier' of S,{ the carrier of S}:] \/ (Union (coprod X))) *):] is non empty set
DTConstrStr(# ([: the carrier' of S,{ the carrier of S}:] \/ (Union (coprod X))),(S,X) #) is non empty strict DTConstrStr
TS (S,X) is non empty functional constituted-DTrees Element of bool (FinTrees the carrier of (S,X))
the carrier of (S,X) is non empty set
FinTrees the carrier of (S,X) is non empty functional constituted-DTrees DTree-set of the carrier of (S,X)
bool (FinTrees the carrier of (S,X)) is non empty set
bool (TS (S,X)) is non empty set
{ b1 where b1 is Relation-like the carrier of (S,X) -valued Function-like DecoratedTree-like Element of TS (S,X) : ( ex b2 being Element of the carrier of S ex b3 being set st
( b2 <= y & b3 in X . b2 & b1 = root-tree [b3,b2] ) or ex b2 being Element of the carrier' of S st
( [b2, the carrier of S] = b1 . {} & the_result_sort_of b2 <= y ) ) } is set
S is non empty non void V60() reflexive transitive antisymmetric order-sorted discernable OverloadedRSSign
the carrier of S is non empty set
the carrier' of S is non empty set
the Arity of S is Relation-like the carrier' of S -defined the carrier of S * -valued Function-like V29( the carrier' of S, the carrier of S * ) V32() V33() Element of bool [: the carrier' of S,( the carrier of S *):]
the carrier of S * is non empty functional FinSequence-membered M10( the carrier of S)
[: the carrier' of S,( the carrier of S *):] is non empty Relation-like set
bool [: the carrier' of S,( the carrier of S *):] is non empty set
X is non empty Relation-like non-empty non empty-yielding the carrier of S -defined Function-like total set
(S,X) is non empty Relation-like non-empty non empty-yielding the carrier of S -defined Function-like total order-sorted set
(S,X) # is non empty Relation-like the carrier of S * -defined Function-like total set
the Arity of S * ((S,X) #) is non empty Relation-like the carrier' of S -defined Function-like total set
(S,X) is non empty strict with_terminals with_nonterminals with_useful_nonterminals DTConstrStr
{ the carrier of S} is non empty set
[: the carrier' of S,{ the carrier of S}:] is non empty Relation-like set
coprod X is non empty Relation-like non-empty non empty-yielding the carrier of S -defined Function-like total set
Union (coprod X) is non empty set
[: the carrier' of S,{ the carrier of S}:] \/ (Union (coprod X)) is non empty set
(S,X) is Relation-like [: the carrier' of S,{ the carrier of S}:] \/ (Union (coprod X)) -defined ([: the carrier' of S,{ the carrier of S}:] \/ (Union (coprod X))) * -valued Element of bool [:([: the carrier' of S,{ the carrier of S}:] \/ (Union (coprod X))),(([: the carrier' of S,{ the carrier of S}:] \/ (Union (coprod X))) *):]
([: the carrier' of S,{ the carrier of S}:] \/ (Union (coprod X))) * is non empty functional FinSequence-membered M10([: the carrier' of S,{ the carrier of S}:] \/ (Union (coprod X)))
[:([: the carrier' of S,{ the carrier of S}:] \/ (Union (coprod X))),(([: the carrier' of S,{ the carrier of S}:] \/ (Union (coprod X))) *):] is non empty Relation-like set
bool [:([: the carrier' of S,{ the carrier of S}:] \/ (Union (coprod X))),(([: the carrier' of S,{ the carrier of S}:] \/ (Union (coprod X))) *):] is non empty set
DTConstrStr(# ([: the carrier' of S,{ the carrier of S}:] \/ (Union (coprod X))),(S,X) #) is non empty strict DTConstrStr
the carrier of (S,X) is non empty set
FinTrees the carrier of (S,X) is non empty functional constituted-DTrees DTree-set of the carrier of (S,X)
TS (S,X) is non empty functional constituted-DTrees Element of bool (FinTrees the carrier of (S,X))
bool (FinTrees the carrier of (S,X)) is non empty set
x is Element of the carrier' of S
( the Arity of S * ((S,X) #)) . x is set
y is set
the_arity_of x is Relation-like K32() -defined the carrier of S -valued Function-like V34() FinSequence-like FinSubsequence-like Element of the carrier of S *
the Arity of S . x is Relation-like K32() -defined Function-like V34() FinSequence-like FinSubsequence-like Element of the carrier of S *
(the_arity_of x) * (S,X) is Relation-like non-empty K32() -defined dom (the_arity_of x) -defined Function-like total V34() FinSequence-like FinSubsequence-like set
dom (the_arity_of x) is Element of bool K32()
product ((the_arity_of x) * (S,X)) is set
dom ((the_arity_of x) * (S,X)) is Element of bool K32()
P is Relation-like Function-like set
proj1 P is set
len (the_arity_of x) is V4() V5() V6() V10() Element of K32()
Seg (len (the_arity_of x)) is V34() V41( len (the_arity_of x)) Element of bool K32()
O1 is Relation-like K32() -defined Function-like V34() FinSequence-like FinSubsequence-like set
proj2 O1 is set
R is set
dom O1 is Element of bool K32()
i is set
O1 . i is set
((the_arity_of x) * (S,X)) . i is set
s is V4() V5() V6() V10() set
((the_arity_of x) * (S,X)) . s is set
(the_arity_of x) . s is set
(S,X) . ((the_arity_of x) . s) is set
(the_arity_of x) /. s is Element of the carrier of S
(S,X) . ((the_arity_of x) /. s) is non empty set
(S,X,((the_arity_of x) /. s)) is non empty functional constituted-DTrees Element of bool (TS (S,X))
bool (TS (S,X)) is non empty set
{ b1 where b1 is Relation-like the carrier of (S,X) -valued Function-like DecoratedTree-like Element of TS (S,X) : ( ex b2 being Element of the carrier of S ex b3 being set st
( b2 <= (the_arity_of x) /. s & b3 in X . b2 & b1 = root-tree [b3,b2] ) or ex b2 being Element of the carrier' of S st
( [b2, the carrier of S] = b1 . {} & the_result_sort_of b2 <= (the_arity_of x) /. s ) ) } is set
a is Relation-like the carrier of (S,X) -valued Function-like DecoratedTree-like Element of TS (S,X)
b is Element of the carrier of S
ta is set
X . b is non empty set
[ta,b] is V26() set
{ta,b} is non empty set
{ta} is non empty set
{{ta,b},{ta}} is non empty set
root-tree [ta,b] is Relation-like Function-like DecoratedTree-like set
tb is Element of the carrier' of S
[tb, the carrier of S] is V26() set
{tb, the carrier of S} is non empty set
{tb} is non empty set
{{tb, the carrier of S},{tb}} is non empty set
a . {} is set
the_result_sort_of tb is Element of the carrier of S
R is Relation-like K32() -defined FinTrees the carrier of (S,X) -valued Function-like V32() V33() V34() FinSequence-like FinSubsequence-like DTree-yielding FinSequence of TS (S,X)
S is non empty non void V60() reflexive transitive antisymmetric order-sorted discernable OverloadedRSSign
the carrier of S is non empty set
the carrier' of S is non empty set
the Arity of S is Relation-like the carrier' of S -defined the carrier of S * -valued Function-like V29( the carrier' of S, the carrier of S * ) V32() V33() Element of bool [: the carrier' of S,( the carrier of S *):]
the carrier of S * is non empty functional FinSequence-membered M10( the carrier of S)
[: the carrier' of S,( the carrier of S *):] is non empty Relation-like set
bool [: the carrier' of S,( the carrier of S *):] is non empty set
X is non empty Relation-like non-empty non empty-yielding the carrier of S -defined Function-like total set
(S,X) is non empty strict with_terminals with_nonterminals with_useful_nonterminals DTConstrStr
{ the carrier of S} is non empty set
[: the carrier' of S,{ the carrier of S}:] is non empty Relation-like set
coprod X is non empty Relation-like non-empty non empty-yielding the carrier of S -defined Function-like total set
Union (coprod X) is non empty set
[: the carrier' of S,{ the carrier of S}:] \/ (Union (coprod X)) is non empty set
(S,X) is Relation-like [: the carrier' of S,{ the carrier of S}:] \/ (Union (coprod X)) -defined ([: the carrier' of S,{ the carrier of S}:] \/ (Union (coprod X))) * -valued Element of bool [:([: the carrier' of S,{ the carrier of S}:] \/ (Union (coprod X))),(([: the carrier' of S,{ the carrier of S}:] \/ (Union (coprod X))) *):]
([: the carrier' of S,{ the carrier of S}:] \/ (Union (coprod X))) * is non empty functional FinSequence-membered M10([: the carrier' of S,{ the carrier of S}:] \/ (Union (coprod X)))
[:([: the carrier' of S,{ the carrier of S}:] \/ (Union (coprod X))),(([: the carrier' of S,{ the carrier of S}:] \/ (Union (coprod X))) *):] is non empty Relation-like set
bool [:([: the carrier' of S,{ the carrier of S}:] \/ (Union (coprod X))),(([: the carrier' of S,{ the carrier of S}:] \/ (Union (coprod X))) *):] is non empty set
DTConstrStr(# ([: the carrier' of S,{ the carrier of S}:] \/ (Union (coprod X))),(S,X) #) is non empty strict DTConstrStr
the carrier of (S,X) is non empty set
FinTrees the carrier of (S,X) is non empty functional constituted-DTrees DTree-set of the carrier of (S,X)
TS (S,X) is non empty functional constituted-DTrees Element of bool (FinTrees the carrier of (S,X))
bool (FinTrees the carrier of (S,X)) is non empty set
(S,X) is non empty Relation-like non-empty non empty-yielding the carrier of S -defined Function-like total order-sorted set
(S,X) # is non empty Relation-like the carrier of S * -defined Function-like total set
the Arity of S * ((S,X) #) is non empty Relation-like the carrier' of S -defined Functio