:: OSAFREE semantic presentation

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

{ b

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

{ b

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

{ b

( b

( [b

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

{ b

( b

( [b

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

{ b

( b

( [b

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

{ b

( b

( [b

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

{ b

( b

( [b

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

{ b

( b

( [b

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

{ b

( b

( [b

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

{ b

( b

( [b

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