:: MSAFREE1 semantic presentation

K97() is set

K101() is non empty V24() V25() V26() Element of bool K97()

bool K97() is set

K96() is non empty V24() V25() V26() set

bool K96() is set

[:K101(),K97():] is Relation-like set

bool [:K101(),K97():] is set

bool (bool K97()) is set

bool K101() is set

{} is Relation-like non-empty empty-yielding K101() -defined Function-like one-to-one constant functional empty V24() V25() V26() V28() V29() V30() V31() 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 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 functional non empty constituted-DTrees DTree-set of the carrier of PeanoNat

TS PeanoNat is functional non empty constituted-DTrees Element of bool (FinTrees the carrier of PeanoNat)

bool (FinTrees the carrier of PeanoNat) is set

[:(TS PeanoNat),K101():] is Relation-like set

bool [:(TS PeanoNat),K101():] is set

[:K101(),(TS PeanoNat):] is Relation-like set

bool [:K101(),(TS PeanoNat):] is set

2 is non empty set

3 is non empty set

f2 is Relation-like Function-like set

f1 is Relation-like Function-like set

product f1 is set

rng f2 is set

Union f1 is set

G is set

dom f2 is set

R is set

f2 . R is set

dom f1 is set

f1 . R is set

F

F

TS F

the carrier of F

FinTrees the carrier of F

bool (FinTrees the carrier of F

[:(TS F

bool [:(TS F

Terminals F

F

(TS F

F

F

f1 is Element of the carrier of F

f2 is Relation-like K101() -defined FinTrees the carrier of F

roots f2 is Relation-like K101() -defined the carrier of F

rng f2 is set

f1 -tree f2 is Relation-like the carrier of F

F

F

dom F

F

[:K101(),F

bool [:K101(),F

dom (F

dom f2 is Element of bool K101()

dom F

F

dom (F

G is set

f2 . G is Relation-like Function-like set

R is Relation-like the carrier of F

F

F

(F

(F

len f2 is V24() V25() V26() V30() Element of K101()

Seg (len f2) is V31() V41( len f2) Element of bool K101()

G is Relation-like K101() -defined Function-like V31() FinSequence-like FinSubsequence-like set

rng G is set

H is Relation-like K101() -defined Function-like V31() FinSequence-like FinSubsequence-like Element of (TS F

R is Relation-like K101() -defined Function-like V31() FinSequence-like FinSubsequence-like Element of F

F

f1 is Element of the carrier of F

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

F

F

F

f1 is set

F

F

f1 is non empty non void V68() ManySortedSign

the carrier of f1 is non empty set

the carrier' of f1 is non empty set

{ the carrier of f1} is non empty set

[: the carrier' of f1,{ the carrier of f1}:] is Relation-like set

f2 is Relation-like the carrier of f1 -defined Function-like non empty total set

REL f2 is Relation-like [: the carrier' of f1,{ the carrier of f1}:] \/ (Union (coprod f2)) -defined ([: the carrier' of f1,{ the carrier of f1}:] \/ (Union (coprod f2))) * -valued Element of bool [:([: the carrier' of f1,{ the carrier of f1}:] \/ (Union (coprod f2))),(([: the carrier' of f1,{ the carrier of f1}:] \/ (Union (coprod f2))) *):]

coprod f2 is Relation-like the carrier of f1 -defined Function-like non empty total set

Union (coprod f2) is set

[: the carrier' of f1,{ the carrier of f1}:] \/ (Union (coprod f2)) is set

([: the carrier' of f1,{ the carrier of f1}:] \/ (Union (coprod f2))) * is functional non empty FinSequence-membered M11([: the carrier' of f1,{ the carrier of f1}:] \/ (Union (coprod f2)))

[:([: the carrier' of f1,{ the carrier of f1}:] \/ (Union (coprod f2))),(([: the carrier' of f1,{ the carrier of f1}:] \/ (Union (coprod f2))) *):] is Relation-like set

bool [:([: the carrier' of f1,{ the carrier of f1}:] \/ (Union (coprod f2))),(([: the carrier' of f1,{ the carrier of f1}:] \/ (Union (coprod f2))) *):] is set

([: the carrier' of f1,{ the carrier of f1}:] \/ (Union (coprod f2))) * is functional non empty FinSequence-membered set

G is set

R is set

[G,R] is V15() set

{G,R} is non empty set

{G} is non empty set

{{G,R},{G}} is non empty set

H is Element of [: the carrier' of f1,{ the carrier of f1}:] \/ (Union (coprod f2))

o is Relation-like K101() -defined Function-like V31() FinSequence-like FinSubsequence-like Element of ([: the carrier' of f1,{ the carrier of f1}:] \/ (Union (coprod f2))) *

[H,o] is V15() set

{H,o} is non empty set

{H} is non empty set

{{H,o},{H}} is non empty set

f1 is non empty non void V68() ManySortedSign

the carrier of f1 is non empty set

the carrier' of f1 is non empty set

{ the carrier of f1} is non empty set

[: the carrier' of f1,{ the carrier of f1}:] is Relation-like set

f2 is Relation-like the carrier of f1 -defined Function-like non empty total set

REL f2 is Relation-like [: the carrier' of f1,{ the carrier of f1}:] \/ (Union (coprod f2)) -defined ([: the carrier' of f1,{ the carrier of f1}:] \/ (Union (coprod f2))) * -valued Element of bool [:([: the carrier' of f1,{ the carrier of f1}:] \/ (Union (coprod f2))),(([: the carrier' of f1,{ the carrier of f1}:] \/ (Union (coprod f2))) *):]

coprod f2 is Relation-like the carrier of f1 -defined Function-like non empty total set

Union (coprod f2) is set

[: the carrier' of f1,{ the carrier of f1}:] \/ (Union (coprod f2)) is set

([: the carrier' of f1,{ the carrier of f1}:] \/ (Union (coprod f2))) * is functional non empty FinSequence-membered M11([: the carrier' of f1,{ the carrier of f1}:] \/ (Union (coprod f2)))

[:([: the carrier' of f1,{ the carrier of f1}:] \/ (Union (coprod f2))),(([: the carrier' of f1,{ the carrier of f1}:] \/ (Union (coprod f2))) *):] is Relation-like set

bool [:([: the carrier' of f1,{ the carrier of f1}:] \/ (Union (coprod f2))),(([: the carrier' of f1,{ the carrier of f1}:] \/ (Union (coprod f2))) *):] is set

G is Element of the carrier' of f1

[G, the carrier of f1] is V15() set

{G, the carrier of f1} is non empty set

{G} is non empty set

{{G, the carrier of f1},{G}} is non empty set

the_arity_of G is Relation-like K101() -defined the carrier of f1 -valued Function-like V31() FinSequence-like FinSubsequence-like Element of the carrier of f1 *

the carrier of f1 * is functional non empty FinSequence-membered M11( the carrier of f1)

the Arity of f1 is Relation-like the carrier' of f1 -defined the carrier of f1 * -valued Function-like V18( the carrier' of f1, the carrier of f1 * ) Element of bool [: the carrier' of f1,( the carrier of f1 *):]

[: the carrier' of f1,( the carrier of f1 *):] is Relation-like set

bool [: the carrier' of f1,( the carrier of f1 *):] is set

the Arity of f1 . G is Relation-like K101() -defined Function-like V31() FinSequence-like FinSubsequence-like Element of the carrier of f1 *

len (the_arity_of G) is V24() V25() V26() V30() Element of K101()

R is Relation-like K101() -defined Function-like V31() FinSequence-like FinSubsequence-like set

[[G, the carrier of f1],R] is V15() set

{[G, the carrier of f1],R} is non empty set

{[G, the carrier of f1]} is Relation-like Function-like non empty set

{{[G, the carrier of f1],R},{[G, the carrier of f1]}} is non empty set

len R is V24() V25() V26() V30() Element of K101()

dom R is Element of bool K101()

([: the carrier' of f1,{ the carrier of f1}:] \/ (Union (coprod f2))) * is functional non empty FinSequence-membered set

H is Relation-like K101() -defined Function-like V31() FinSequence-like FinSubsequence-like Element of ([: the carrier' of f1,{ the carrier of f1}:] \/ (Union (coprod f2))) *

len H is V24() V25() V26() V30() Element of K101()

dom H is Element of bool K101()

o is set

H . o is set

ts is Element of the carrier' of f1

[ts, the carrier of f1] is V15() set

{ts, the carrier of f1} is non empty set

{ts} is non empty set

{{ts, the carrier of f1},{ts}} is non empty set

the_result_sort_of ts is Element of the carrier of f1

the ResultSort of f1 is Relation-like the carrier' of f1 -defined the carrier of f1 -valued Function-like V18( the carrier' of f1, the carrier of f1) Element of bool [: the carrier' of f1, the carrier of f1:]

[: the carrier' of f1, the carrier of f1:] is Relation-like set

bool [: the carrier' of f1, the carrier of f1:] is set

the ResultSort of f1 . ts is Element of the carrier of f1

(the_arity_of G) . o is set

coprod (((the_arity_of G) . o),f2) is set

o is set

R . o is set

ts is Element of the carrier' of f1

[ts, the carrier of f1] is V15() set

{ts, the carrier of f1} is non empty set

{ts} is non empty set

{{ts, the carrier of f1},{ts}} is non empty set

the_result_sort_of ts is Element of the carrier of f1

the ResultSort of f1 is Relation-like the carrier' of f1 -defined the carrier of f1 -valued Function-like V18( the carrier' of f1, the carrier of f1) Element of bool [: the carrier' of f1, the carrier of f1:]

[: the carrier' of f1, the carrier of f1:] is Relation-like set

bool [: the carrier' of f1, the carrier of f1:] is set

the ResultSort of f1 . ts is Element of the carrier of f1

(the_arity_of G) . o is set

coprod (((the_arity_of G) . o),f2) is set

f1 is non empty set

f2 is Relation-like f1 -defined Function-like non empty total set

rng f2 is non empty set

f1 is set

f2 is Relation-like f1 -defined Function-like total set

G is set

R is set

f2 . G is set

f2 . R is set

dom f2 is set

dom f2 is set

dom f2 is set

f1 is set

the Relation-like empty-yielding f1 -defined Function-like total disjoint_valued set is Relation-like empty-yielding f1 -defined Function-like total disjoint_valued set

f1 is non empty set

f2 is Relation-like f1 -defined Function-like non empty total disjoint_valued set

G is Relation-like non-empty non empty-yielding f1 -defined Function-like non empty total set

Union f2 is set

Union G is non empty set

[:(Union f2),(Union G):] is Relation-like set

bool [:(Union f2),(Union G):] is set

R is Relation-like f1 -defined Function-like non empty total V53() ManySortedFunction of f2,G

H is set

dom f2 is non empty set

o is set

f2 . o is set

ts is Element of f1

R . ts is Relation-like f2 . ts -defined G . ts -valued Function-like V18(f2 . ts,G . ts) Element of bool [:(f2 . ts),(G . ts):]

f2 . ts is set

G . ts is non empty set

[:(f2 . ts),(G . ts):] is Relation-like set

bool [:(f2 . ts),(G . ts):] is set

(R . ts) . H is set

x is set

dom G is non empty set

a is Element of f1

f2 . a is set

R . a is Relation-like f2 . a -defined G . a -valued Function-like V18(f2 . a,G . a) Element of bool [:(f2 . a),(G . a):]

G . a is non empty set

[:(f2 . a),(G . a):] is Relation-like set

bool [:(f2 . a),(G . a):] is set

(R . a) . H is set

H is Relation-like Union f2 -defined Union G -valued Function-like V18( Union f2, Union G) Element of bool [:(Union f2),(Union G):]

o is Element of f1

f2 . o is set

R . o is Relation-like f2 . o -defined G . o -valued Function-like V18(f2 . o,G . o) Element of bool [:(f2 . o),(G . o):]

G . o is non empty set

[:(f2 . o),(G . o):] is Relation-like set

bool [:(f2 . o),(G . o):] is set

ts is set

H . ts is set

(R . o) . ts is set

dom f2 is non empty set

H is Relation-like Union f2 -defined Union G -valued Function-like V18( Union f2, Union G) Element of bool [:(Union f2),(Union G):]

o is Relation-like Union f2 -defined Union G -valued Function-like V18( Union f2, Union G) Element of bool [:(Union f2),(Union G):]

ts is set

dom f2 is non empty set

x is set

f2 . x is set

H . ts is set

a is Element of f1

R . a is Relation-like f2 . a -defined G . a -valued Function-like V18(f2 . a,G . a) Element of bool [:(f2 . a),(G . a):]

f2 . a is set

G . a is non empty set

[:(f2 . a),(G . a):] is Relation-like set

bool [:(f2 . a),(G . a):] is set

(R . a) . ts is set

o . ts is set

f1 is non empty set

f2 is Relation-like f1 -defined Function-like non empty total disjoint_valued set

Union f2 is set

G is Relation-like non-empty non empty-yielding f1 -defined Function-like non empty total set

Union G is non empty set

R is Relation-like f1 -defined Function-like non empty total V53() ManySortedFunction of f2,G

(f1,f2,G,R) is Relation-like Union f2 -defined Union G -valued Function-like V18( Union f2, Union G) Element of bool [:(Union f2),(Union G):]

[:(Union f2),(Union G):] is Relation-like set

bool [:(Union f2),(Union G):] is set

H is Relation-like f1 -defined Function-like non empty total V53() ManySortedFunction of f2,G

(f1,f2,G,H) is Relation-like Union f2 -defined Union G -valued Function-like V18( Union f2, Union G) Element of bool [:(Union f2),(Union G):]

o is set

G . o is set

f2 . o is set

ts is non empty set

[:(f2 . o),ts:] is Relation-like set

bool [:(f2 . o),ts:] is set

R . o is set

H . o is set

x9 is set

x is Relation-like f2 . o -defined ts -valued Function-like V18(f2 . o,ts) Element of bool [:(f2 . o),ts:]

x . x9 is set

(f1,f2,G,R) . x9 is set

a is Relation-like f2 . o -defined ts -valued Function-like V18(f2 . o,ts) Element of bool [:(f2 . o),ts:]

a . x9 is set

f1 is non empty V68() ManySortedSign

f1 is non empty V68() ManySortedSign

the carrier of f1 is non empty set

f2 is Relation-like the carrier of f1 -defined Function-like non empty total set

the carrier' of f1 is set

the Arity of f1 is Relation-like the carrier' of f1 -defined the carrier of f1 * -valued Function-like V18( the carrier' of f1, the carrier of f1 * ) Element of bool [: the carrier' of f1,( the carrier of f1 *):]

the carrier of f1 * is functional non empty FinSequence-membered M11( the carrier of f1)

[: the carrier' of f1,( the carrier of f1 *):] is Relation-like set

bool [: the carrier' of f1,( the carrier of f1 *):] is set

f2 # is Relation-like the carrier of f1 * -defined Function-like non empty total set

the Arity of f1 * (f2 #) is Relation-like the carrier' of f1 -defined Function-like total set

the ResultSort of f1 is Relation-like the carrier' of f1 -defined the carrier of f1 -valued Function-like V18( the carrier' of f1, the carrier of f1) Element of bool [: the carrier' of f1, the carrier of f1:]

[: the carrier' of f1, the carrier of f1:] is Relation-like set

bool [: the carrier' of f1, the carrier of f1:] is set

the ResultSort of f1 * f2 is Relation-like the carrier' of f1 -defined Function-like total set

the Relation-like the carrier' of f1 -defined Function-like total V53() ManySortedFunction of the Arity of f1 * (f2 #), the ResultSort of f1 * f2 is Relation-like the carrier' of f1 -defined Function-like total V53() ManySortedFunction of the Arity of f1 * (f2 #), the ResultSort of f1 * f2

MSAlgebra(# f2, the Relation-like the carrier' of f1 -defined Function-like total V53() ManySortedFunction of the Arity of f1 * (f2 #), the ResultSort of f1 * f2 #) is strict MSAlgebra over f1

the Sorts of MSAlgebra(# f2, the Relation-like the carrier' of f1 -defined Function-like total V53() ManySortedFunction of the Arity of f1 * (f2 #), the ResultSort of f1 * f2 #) is Relation-like the carrier of f1 -defined Function-like non empty total set

R is set

the Sorts of MSAlgebra(# f2, the Relation-like the carrier' of f1 -defined Function-like total V53() ManySortedFunction of the Arity of f1 * (f2 #), the ResultSort of f1 * f2 #) . R is set

{R} is non empty set

f2 is strict MSAlgebra over f1

the Sorts of f2 is Relation-like the carrier of f1 -defined Function-like non empty total set

G is strict MSAlgebra over f1

the Sorts of G is Relation-like the carrier of f1 -defined Function-like non empty total set

H is set

the Sorts of f2 . H is set

{H} is non empty set

the Sorts of G . H is set

the ResultSort of f1 is Relation-like the carrier' of f1 -defined the carrier of f1 -valued Function-like V18( the carrier' of f1, the carrier of f1) Element of bool [: the carrier' of f1, the carrier of f1:]

the carrier' of f1 is set

[: the carrier' of f1, the carrier of f1:] is Relation-like set

bool [: the carrier' of f1, the carrier of f1:] is set

dom the ResultSort of f1 is set

the ResultSort of f1 * the Sorts of f2 is Relation-like the carrier' of f1 -defined Function-like total set

H is set

( the ResultSort of f1 * the Sorts of f2) . H is set

the ResultSort of f1 . H is set

the Sorts of f2 . ( the ResultSort of f1 . H) is set

{( the ResultSort of f1 . H)} is non empty set

the Arity of f1 is Relation-like the carrier' of f1 -defined the carrier of f1 * -valued Function-like V18( the carrier' of f1, the carrier of f1 * ) Element of bool [: the carrier' of f1,( the carrier of f1 *):]

the carrier of f1 * is functional non empty FinSequence-membered M11( the carrier of f1)

[: the carrier' of f1,( the carrier of f1 *):] is Relation-like set

bool [: the carrier' of f1,( the carrier of f1 *):] is set

the Sorts of f2 # is Relation-like the carrier of f1 * -defined Function-like non empty total set

the Arity of f1 * ( the Sorts of f2 #) is Relation-like the carrier' of f1 -defined Function-like total set

( the Arity of f1 * ( the Sorts of f2 #)) . H is set

ts is non empty set

[:(( the Arity of f1 * ( the Sorts of f2 #)) . H),ts:] is Relation-like set

bool [:(( the Arity of f1 * ( the Sorts of f2 #)) . H),ts:] is set

the Charact of f2 is Relation-like the carrier' of f1 -defined Function-like total V53() ManySortedFunction of the Arity of f1 * ( the Sorts of f2 #), the ResultSort of f1 * the Sorts of f2

the Charact of f2 . H is set

the Charact of G is Relation-like the carrier' of f1 -defined Function-like total V53() ManySortedFunction of the Arity of f1 * ( the Sorts of G #), the ResultSort of f1 * the Sorts of G

the Sorts of G # is Relation-like the carrier of f1 * -defined Function-like non empty total set

the Arity of f1 * ( the Sorts of G #) is Relation-like the carrier' of f1 -defined Function-like total set

the ResultSort of f1 * the Sorts of G is Relation-like the carrier' of f1 -defined Function-like total set

the Charact of G . H is set

x9 is set

x is Relation-like ( the Arity of f1 * ( the Sorts of f2 #)) . H -defined ts -valued Function-like V18(( the Arity of f1 * ( the Sorts of f2 #)) . H,ts) Element of bool [:(( the Arity of f1 * ( the Sorts of f2 #)) . H),ts:]

x . x9 is set

a is Relation-like ( the Arity of f1 * ( the Sorts of f2 #)) . H -defined ts -valued Function-like V18(( the Arity of f1 * ( the Sorts of f2 #)) . H,ts) Element of bool [:(( the Arity of f1 * ( the Sorts of f2 #)) . H),ts:]

a . x9 is set

f1 is non empty V68() ManySortedSign

(f1) is strict MSAlgebra over f1

the Sorts of (f1) is Relation-like the carrier of f1 -defined Function-like non empty total set

the carrier of f1 is non empty set

G is set

the Sorts of (f1) . G is set

{G} is non empty set

G is set

R is set

the Sorts of (f1) . G is set

the Sorts of (f1) . R is set

dom the Sorts of (f1) is non empty set

{G} is non empty set

{R} is non empty set

dom the Sorts of (f1) is non empty set

dom the Sorts of (f1) is non empty set

f1 is non empty V68() ManySortedSign

(f1) is strict MSAlgebra over f1

f1 is non empty V68() ManySortedSign

(f1) is strict MSAlgebra over f1

f1 is non empty V68() ManySortedSign

f2 is (f1) MSAlgebra over f1

the Sorts of f2 is Relation-like the carrier of f1 -defined Function-like non empty total set

the carrier of f1 is non empty set

f1 is non empty non void V68() ManySortedSign

the carrier' of f1 is non empty set

the carrier of f1 is non empty set

f2 is Element of the carrier' of f1

G is non-empty (f1) MSAlgebra over f1

the Sorts of G is Relation-like non-empty non empty-yielding the carrier of f1 -defined Function-like non empty total disjoint_valued set

Args (f2,G) is functional non empty Element of rng ( the Sorts of G #)

the Sorts of G # is Relation-like the carrier of f1 * -defined Function-like non empty total set

the carrier of f1 * is functional non empty FinSequence-membered M11( the carrier of f1)

rng ( the Sorts of G #) is non empty set

the Arity of f1 is Relation-like the carrier' of f1 -defined the carrier of f1 * -valued Function-like V18( the carrier' of f1, the carrier of f1 * ) Element of bool [: the carrier' of f1,( the carrier of f1 *):]

[: the carrier' of f1,( the carrier of f1 *):] is Relation-like set

bool [: the carrier' of f1,( the carrier of f1 *):] is set

the Arity of f1 * ( the Sorts of G #) is Relation-like the carrier' of f1 -defined Function-like non empty total set

( the Arity of f1 * ( the Sorts of G #)) . f2 is set

R is non-empty MSAlgebra over f1

the Sorts of R is Relation-like non-empty non empty-yielding the carrier of f1 -defined Function-like non empty total set

H is Relation-like the carrier of f1 -defined Function-like non empty total V53() ManySortedFunction of the Sorts of G, the Sorts of R

( the carrier of f1, the Sorts of G, the Sorts of R,H) is Relation-like Union the Sorts of G -defined Union the Sorts of R -valued Function-like V18( Union the Sorts of G, Union the Sorts of R) Element of bool [:(Union the Sorts of G),(Union the Sorts of R):]

Union the Sorts of G is non empty set

Union the Sorts of R is non empty set

[:(Union the Sorts of G),(Union the Sorts of R):] is Relation-like set

bool [:(Union the Sorts of G),(Union the Sorts of R):] is set

o is Relation-like Function-like Element of Args (f2,G)

o * ( the carrier of f1, the Sorts of G, the Sorts of R,H) is Relation-like Union the Sorts of R -valued Function-like set

H # o is Relation-like Function-like Element of Args (f2,R)

Args (f2,R) is functional non empty Element of rng ( the Sorts of R #)

the Sorts of R # is Relation-like the carrier of f1 * -defined Function-like non empty total set

rng ( the Sorts of R #) is non empty set

the Arity of f1 * ( the Sorts of R #) is Relation-like the carrier' of f1 -defined Function-like non empty total set

( the Arity of f1 * ( the Sorts of R #)) . f2 is set

dom the Arity of f1 is set

the_arity_of f2 is Relation-like K101() -defined the carrier of f1 -valued Function-like V31() FinSequence-like FinSubsequence-like Element of the carrier of f1 *

the Arity of f1 . f2 is Relation-like K101() -defined Function-like V31() FinSequence-like FinSubsequence-like Element of the carrier of f1 *

( the Sorts of G #) . ( the Arity of f1 . f2) is set

(the_arity_of f2) * the Sorts of G is Relation-like non-empty K101() -defined Function-like set

product ((the_arity_of f2) * the Sorts of G) is set

rng o is set

Union ((the_arity_of f2) * the Sorts of G) is set

rng ((the_arity_of f2) * the Sorts of G) is V36() set

union (rng ((the_arity_of f2) * the Sorts of G)) is set

rng the Sorts of G is non empty V36() set

union (rng the Sorts of G) is set

dom ( the carrier of f1, the Sorts of G, the Sorts of R,H) is set

dom (o * ( the carrier of f1, the Sorts of G, the Sorts of R,H)) is set

dom o is set

rng (the_arity_of f2) is set

dom the Sorts of G is non empty set

dom ((the_arity_of f2) * the Sorts of G) is set

dom (the_arity_of f2) is Element of bool K101()

x is set

(the_arity_of f2) * the Sorts of R is Relation-like non-empty K101() -defined Function-like set

dom ((the_arity_of f2) * the Sorts of R) is set

(the_arity_of f2) . x is set

the Sorts of R . ((the_arity_of f2) . x) is set

((the_arity_of f2) * the Sorts of R) . x is set

the Sorts of G . ((the_arity_of f2) . x) is set

((the_arity_of f2) * the Sorts of G) . x is set

o . x is set

a is Element of the carrier of f1

the Sorts of G . a is non empty set

(o * ( the carrier of f1, the Sorts of G, the Sorts of R,H)) . x is set

( the carrier of f1, the Sorts of G, the Sorts of R,H) . (o . x) is set

H . a is Relation-like the Sorts of G . a -defined the Sorts of R . a -valued Function-like V18( the Sorts of G . a, the Sorts of R . a) Element of bool [:( the Sorts of G . a),( the Sorts of R . a):]

the Sorts of R . a is non empty set

[:( the Sorts of G . a),( the Sorts of R . a):] is Relation-like set

bool [:( the Sorts of G . a),( the Sorts of R . a):] is set

(H . a) . (o . x) is set

dom the Sorts of R is non empty set

product ((the_arity_of f2) * the Sorts of R) is set

( the Sorts of R #) . ( the Arity of f1 . f2) is set

a is V24() V25() V26() V30() set

(the_arity_of f2) /. a is Element of the carrier of f1

(the_arity_of f2) . a is set

o . a is set

((the_arity_of f2) * the Sorts of G) . a is set

the Sorts of G . ((the_arity_of f2) /. a) is non empty set

x is Relation-like Function-like Element of Args (f2,R)

x . a is set

( the carrier of f1, the Sorts of G, the Sorts of R,H) . (o . a) is set

H . ((the_arity_of f2) /. a) is Relation-like the Sorts of G . ((the_arity_of f2) /. a) -defined the Sorts of R . ((the_arity_of f2) /. a) -valued Function-like V18( the Sorts of G . ((the_arity_of f2) /. a), the Sorts of R . ((the_arity_of f2) /. a)) Element of bool [:( the Sorts of G . ((the_arity_of f2) /. a)),( the Sorts of R . ((the_arity_of f2) /. a)):]

the Sorts of R . ((the_arity_of f2) /. a) is non empty set

[:( the Sorts of G . ((the_arity_of f2) /. a)),( the Sorts of R . ((the_arity_of f2) /. a)):] is Relation-like set

bool [:( the Sorts of G . ((the_arity_of f2) /. a)),( the Sorts of R . ((the_arity_of f2) /. a)):] is set

(H . ((the_arity_of f2) /. a)) . (o . a) is set

f1 is non empty non void V68() ManySortedSign

the carrier of f1 is non empty set

f2 is Relation-like non-empty non empty-yielding the carrier of f1 -defined Function-like non empty total set

FreeSort f2 is Relation-like non-empty non empty-yielding the carrier of f1 -defined Function-like non empty total set

G is set

R is set

(FreeSort f2) . G is set

(FreeSort f2) . R is set

dom (FreeSort f2) is non empty set

o is Element of the carrier of f1

(FreeSort f2) . o is non empty set

ts is Element of the carrier of f1

(FreeSort f2) . ts is non empty set

dom (FreeSort f2) is non empty set

dom (FreeSort f2) is non empty set

F

the carrier of F

F

Union F

F

FreeSort F

the carrier' of F

FreeMSA F

(Union F

F

( the carrier of F

Union (FreeSort F

[:(Union (FreeSort F

bool [:(Union (FreeSort F

F

( the carrier of F

DTConMSA F

TS (DTConMSA F

the carrier of (DTConMSA F

FinTrees the carrier of (DTConMSA F

bool (FinTrees the carrier of (DTConMSA F

rng (FreeSort F

union (rng (FreeSort F

f1 is non empty set

[:(TS (DTConMSA F

bool [:(TS (DTConMSA F

(TS (DTConMSA F

[: the carrier of (DTConMSA F

[:[: the carrier of (DTConMSA F

bool [:[: the carrier of (DTConMSA F

R is Relation-like [: the carrier of (DTConMSA F

f1 * is functional non empty FinSequence-membered set

[: the carrier of (DTConMSA F

[:[: the carrier of (DTConMSA F

bool [:[: the carrier of (DTConMSA F

H is Relation-like [: the carrier of (DTConMSA F

{ the carrier of F

[: the carrier' of F

coprod F

Union (coprod F

[: the carrier' of F

REL F

([: the carrier' of F

[:([: the carrier' of F

bool [:([: the carrier' of F

DTConstrStr(# ([: the carrier' of F

o is Relation-like the carrier of F

( the carrier of F

ts is Element of the carrier of (DTConMSA F

x is Relation-like K101() -defined Function-like V31() FinSequence-like FinSubsequence-like Element of (TS (DTConMSA F

roots x is Relation-like K101() -defined Function-like V31() FinSequence-like FinSubsequence-like set

[ts,(roots x)] is V15() set

{ts,(roots x)} is non empty set

{ts} is non empty set

{{ts,(roots x)},{ts}} is non empty set

a is Element of the carrier' of F

x9 is Element of { the carrier of F

[a,x9] is V15() set

{a,x9} is non empty set

{a} is non empty set

{{a,x9},{a}} is non empty set

x is Relation-like K101() -defined Function-like V31() FinSequence-like FinSubsequence-like Element of f1 *

x * ( the carrier of F

FreeOper F

the Arity of F

the carrier of F

[: the carrier' of F

bool [: the carrier' of F

(FreeSort F

the Arity of F

the ResultSort of F

[: the carrier' of F

bool [: the carrier' of F

the ResultSort of F

MSAlgebra(# (FreeSort F

Sym (a,F

tss is Relation-like K101() -defined FinTrees the carrier of (DTConMSA F

( the Arity of F

( the ResultSort of F

the_result_sort_of a is Element of the carrier of F

the ResultSort of F

(FreeSort F

DenOp (a,F

[:(( the Arity of F

bool [:(( the Arity of F

(DenOp (a,F

[a, the carrier of F

{a, the carrier of F

{{a, the carrier of F

[a, the carrier of F

( the carrier of F

(DenOp (a,F

( the carrier of F

o . (the_result_sort_of a) is Relation-like (FreeSort F

F

[:((FreeSort F

bool [:((FreeSort F

(o . (the_result_sort_of a)) . ((DenOp (a,F

Den (a,(FreeMSA F

Args (a,(FreeMSA F

the Sorts of (FreeMSA F

the Sorts of (FreeMSA F

rng ( the Sorts of (FreeMSA F

the Arity of F

( the Arity of F

Result (a,(FreeMSA F

rng the Sorts of (FreeMSA F

the ResultSort of F

( the ResultSort of F

[:(Args (a,(FreeMSA F

bool [:(Args (a,(FreeMSA F

the Charact of (FreeMSA F

the Charact of (FreeMSA F

(Den (a,(FreeMSA F

(o . (the_result_sort_of a)) . ((Den (a,(FreeMSA F

F

ts `1 is set

F

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

( the carrier of F

xx is Relation-like K101() -defined Function-like V31() FinSequence-like FinSubsequence-like Element of (Union F

F

H . (ts,x,x) is Element of f1

f2 is Relation-like TS (DTConMSA F

o is Element of the carrier of (DTConMSA F

ts is Relation-like K101() -defined Function-like V31() FinSequence-like FinSubsequence-like Element of (TS (DTConMSA F

roots ts is Relation-like K101() -defined Function-like V31() FinSequence-like FinSubsequence-like set

x is Relation-like K101() -defined Function-like V31() FinSequence-like FinSubsequence-like Element of f1 *

ts * f2 is Relation-like K101() -defined f1 -valued Function-like set

o -tree ts is Relation-like Function-like DecoratedTree-like set

f2 . (o -tree ts) is set

H . (o,ts,x) is Element of f1

Terminals (DTConMSA F

bool the carrier of (DTConMSA F

[: the carrier of (DTConMSA F

bool [: the carrier of (DTConMSA F

o is Relation-like the carrier of (DTConMSA F

[: the carrier of (DTConMSA F

bool [: the carrier of (DTConMSA F

ts is Relation-like the carrier of (DTConMSA F

dom F

x is Relation-like the carrier of F

a is Element of the carrier of (DTConMSA F

a `2 is set

a `1 is set

F

x9 is Element of the carrier of F

[(a `1),x9] is V15() set

{(a `1),x9} is non empty set

{(a `1)} is non empty set

{{(a `1),x9},{(a `1)}} is non empty set

root-tree [(a `1),x9] is Relation-like Function-like DecoratedTree-like set

FreeGen (x9,F

(FreeSort F

bool ((FreeSort F

[(a `1),(a `2)] is V15() set

{(a `1),(a `2)} is non empty set

{{(a `1),(a `2)},{(a `1)}} is non empty set

( the carrier of F

root-tree a is Relation-like the carrier of (DTConMSA F

( the carrier of F

x . x9 is Relation-like (FreeSort F

F

[:((FreeSort F

bool [:((FreeSort F

(x . x9) . (root-tree [(a `1),x9]) is set

F

ts . a is Element of f1

G is Relation-like TS (DTConMSA F

x is Element of the carrier of (DTConMSA F

root-tree x is Relation-like the carrier of (DTConMSA F

G . (root-tree x) is set

ts . x is Element of f1

x is Element of the carrier of (DTConMSA F

a is Relation-like K101() -defined Function-like V31() FinSequence-like FinSubsequence-like Element of (TS (DTConMSA F

roots a is Relation-like K101() -defined Function-like V31() FinSequence-like FinSubsequence-like set

x9 is Relation-like K101() -defined Function-like V31() FinSequence-like FinSubsequence-like Element of f1 *

a * G is Relation-like K101() -defined f1 -valued Function-like set

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

G . (x -tree a) is set

H . (x,a,x9) is Element of f1

x is Element of the carrier of (DTConMSA F

root-tree x is Relation-like the carrier of (DTConMSA F

f2 . (root-tree x) is set

ts . x is Element of f1

f1 is non empty non void V68() ManySortedSign

the carrier of f1 is non empty set

f2 is Relation-like non-empty non empty-yielding the carrier of f1 -defined Function-like non empty total set

FreeMSA f2 is strict non-empty MSAlgebra over f1

f1 is non empty non void V68() ManySortedSign

the carrier' of f1 is non empty set

f2 is Element of the carrier' of f1

G is non-empty MSAlgebra over f1

Args (f2,G) is functional non empty Element of rng ( the Sorts of G #)

the carrier of f1 is non empty set

the Sorts of G is Relation-like non-empty non empty-yielding the carrier of f1 -defined Function-like non empty total set

the Sorts of G # is Relation-like the carrier of f1 * -defined Function-like non empty total set

the carrier of f1 * is functional non empty FinSequence-membered M11( the carrier of f1)

rng ( the Sorts of G #) is non empty set

the Arity of f1 is Relation-like the carrier' of f1 -defined the carrier of f1 * -valued Function-like V18( the carrier' of f1, the carrier of f1 * ) Element of bool [: the carrier' of f1,( the carrier of f1 *):]

[: the carrier' of f1,( the carrier of f1 *):] is Relation-like set

bool [: the carrier' of f1,( the carrier of f1 *):] is set

the Arity of f1 * ( the Sorts of G #) is Relation-like the carrier' of f1 -defined Function-like non empty total set

( the Arity of f1 * ( the Sorts of G #)) . f2 is set

Result (f2,G) is non empty Element of rng the Sorts of G

rng the Sorts of G is non empty V36() set

the ResultSort of f1 is Relation-like the carrier' of f1 -defined the carrier of f1 -valued Function-like V18( the carrier' of f1, the carrier of f1) Element of bool [: the carrier' of f1, the carrier of f1:]

[: the carrier' of f1, the carrier of f1:] is Relation-like set

bool [: the carrier' of f1, the carrier of f1:] is set

the ResultSort of f1 * the Sorts of G is Relation-like non-empty non empty-yielding the carrier' of f1 -defined Function-like non empty total set

( the ResultSort of f1 * the Sorts of G) . f2 is non empty set

f1 is non empty non void V68() ManySortedSign

the carrier of f1 is non empty set

f2 is Relation-like non-empty non empty-yielding the carrier of f1 -defined Function-like non empty total set

FreeMSA f2 is strict non-empty MSAlgebra over f1

the Sorts of (FreeMSA f2) is Relation-like non-empty non empty-yielding the carrier of f1 -defined Function-like non empty total set

FreeSort f2 is Relation-like non-empty non empty-yielding the carrier of f1 -defined Function-like non empty total disjoint_valued set

FreeOper f2 is Relation-like the carrier' of f1 -defined Function-like non empty total V53() ManySortedFunction of the Arity of f1 * ((FreeSort f2) #), the ResultSort of f1 * (FreeSort f2)

the carrier' of f1 is non empty set

the Arity of f1 is Relation-like the carrier' of f1 -defined the carrier of f1 * -valued Function-like V18( the carrier' of f1, the carrier of f1 * ) Element of bool [: the carrier' of f1,( the carrier of f1 *):]

the carrier of f1 * is functional non empty FinSequence-membered M11( the carrier of f1)

[: the carrier' of f1,( the carrier of f1 *):] is Relation-like set

bool [: the carrier' of f1,( the carrier of f1 *):] is set

(FreeSort f2) # is Relation-like the carrier of f1 * -defined Function-like non empty total set

the Arity of f1 * ((FreeSort f2) #) is Relation-like the carrier' of f1 -defined Function-like non empty total set

the ResultSort of f1 is Relation-like the carrier' of f1 -defined the carrier of f1 -valued Function-like V18( the carrier' of f1, the carrier of f1) Element of bool [: the carrier' of f1, the carrier of f1:]

[: the carrier' of f1, the carrier of f1:] is Relation-like set

bool [: the carrier' of f1, the carrier of f1:] is set

the ResultSort of f1 * (FreeSort f2) is Relation-like non-empty non empty-yielding the carrier' of f1 -defined Function-like non empty total set

MSAlgebra(# (FreeSort f2),(FreeOper f2) #) is strict MSAlgebra over f1

f1 is non empty non void V68() ManySortedSign

the carrier of f1 is non empty set

f2 is Relation-like non-empty non empty-yielding the carrier of f1 -defined Function-like non empty total set

FreeMSA f2 is strict non-empty MSAlgebra over f1

the Sorts of (FreeMSA f2) is Relation-like non-empty non empty-yielding the carrier of f1 -defined Function-like non empty total disjoint_valued set

F

the carrier of F

F

FreeMSA F

the Sorts of (FreeMSA F

F

the Sorts of F

F

F

FreeSort F

FreeOper F

the carrier' of F

the Arity of F

the carrier of F

[: the carrier' of F

bool [: the carrier' of F

(FreeSort F

the Arity of F

the ResultSort of F

[: the carrier' of F

bool [: the carrier' of F

the ResultSort of F

MSAlgebra(# (FreeSort F

FreeGen F

Union (FreeGen F

Union the Sorts of F

G is set

dom the Sorts of F

dom (FreeGen F

R is set

(FreeGen F

H is Element of the carrier of F

FreeGen (H,F

(FreeSort F

bool ((FreeSort F

F

the Sorts of (FreeMSA F

the Sorts of F

[:( the Sorts of (FreeMSA F

bool [:( the Sorts of (FreeMSA F

(F

o is set

f1 is Relation-like the carrier of F

f1 . H is Relation-like (FreeSort F

[:((FreeSort F

bool [:((FreeSort F

ts is Element of the carrier of F

FreeGen (ts,F

(FreeSort F

bool ((FreeSort F

((FreeSort F

[:(Union (FreeGen F

bool [:(Union (FreeGen F

G is Relation-like Union (FreeGen F

{ [b

R is set

f1 is Relation-like the carrier of F

H is Element of the carrier of F

FreeGen (H,F

(FreeSort F

bool ((FreeSort F

f1 . H is Relation-like (FreeSort F

the Sorts of F

[:((FreeSort F

bool [:((FreeSort F

o is set

(f1 . H) . o is set

G /. o is Element of Union the Sorts of F

dom (FreeGen F

(FreeGen F

G . o is set

H is set

o is Element of the carrier' of F

Args (o,F

the Sorts of F

rng ( the Sorts of F

the Arity of F

( the Arity of F

ts is Relation-like Function-like Element of Args (o,F

[o,ts] is V15() set

{o,ts} is non empty set

{o} is non empty set

{{o,ts},{o}} is non empty set

Result (o,F

rng the Sorts of F

the ResultSort of F

( the ResultSort of F

Den (o,F

[:(Args (o,F

bool [:(Args (o,F

the Charact of F

the Charact of F

(Den (o,F

x is set

union (rng the Sorts of F

a is Element of the carrier' of F

Args (a,F

( the Arity of F

Result (a,F

( the ResultSort of F

Den (a,F

[:(Args (a,F

bool [:(Args (a,F

the Charact of F

x9 is Relation-like Function-like Element of Args (a,F

[a,x9] is V15() set

{a,x9} is non empty set

{a} is non empty set

{{a,x9},{a}} is non empty set

(Den (a,F

[:R,(Union the Sorts of F

bool [:R,(Union the Sorts of F

H is Relation-like R -defined Union the Sorts of F

f2 is Relation-like the carrier of F

o is Element of the carrier of F

FreeGen (o,F

(FreeSort F

bool ((FreeSort F

f2 . o is Relation-like (FreeSort F

the Sorts of F

[:((FreeSort F

bool [:((FreeSort F

ts is set

(f2 . o) . ts is set

G /. ts is Element of Union the Sorts of F

dom (FreeGen F

(FreeGen F

G . ts is set

(Union the Sorts of F

( the carrier of F

Union (FreeSort F

[:(Union (FreeSort F

bool [:(Union (FreeSort F

o is Element of the carrier' of F

Args (o,(FreeMSA F

the Sorts of (FreeMSA F

rng ( the Sorts of (FreeMSA F

the Arity of F

( the Arity of F

the_result_sort_of o is Element of the carrier of F

the ResultSort of F

f2 . (the_result_sort_of o) is Relation-like (FreeSort F

(FreeSort F

the Sorts of F

[:((FreeSort F

bool [:((FreeSort F

Result (o,(FreeMSA F

rng the Sorts of (FreeMSA F

the ResultSort of F

( the ResultSort of F

Den (o,(FreeMSA F

[:(Args (o,(FreeMSA F

bool [:(Args (o,(FreeMSA F

the Charact of (FreeMSA F

the Charact of (FreeMSA F

ts is Relation-like Function-like Element of Args (o,(FreeMSA F

ts * ( the carrier of F

(Den (o,(FreeMSA F

(f2 . (the_result_sort_of o)) . ((Den (o,(FreeMSA F

x is Relation-like K101() -defined Function-like V31() FinSequence-like FinSubsequence-like Element of (Union the Sorts of F

[o,x] is V15() set

{o,x} is non empty set

{o} is non empty set

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

H /. [o,x] is Element of Union the Sorts of F

F

Args (o,F

the Sorts of F

rng ( the Sorts of F

the Arity of F

( the Arity of F

a is Relation-like Function-like Element of Args (o,F

[o,a] is V15() set

{o,a} is non empty set

{{o,a},{o}} is non empty set

Result (o,F

rng the Sorts of F

the ResultSort of F

( the ResultSort of F

Den (o,F

[:(Args (o,F

bool [:(Args (o,F

the Charact of F

the Charact of F

(Den (o,F

H . [o,x] is set

( the carrier of F

o is Element of the carrier' of F

Args (o,(FreeMSA F

the Sorts of (FreeMSA F

rng ( the Sorts of (FreeMSA F

the Arity of F

( the Arity of F

the_result_sort_of o is Element of the carrier of F

the ResultSort of F

f1 . (the_result_sort_of o) is Relation-like (FreeSort F

(FreeSort F

the Sorts of F

[:((FreeSort F

bool [:((FreeSort F

Result (o,(FreeMSA F

rng the Sorts of (FreeMSA F

the ResultSort of F

( the ResultSort of F

Den (o,(FreeMSA F

[:(Args (o,(FreeMSA F

bool [:(Args (o,(FreeMSA F

the Charact of (FreeMSA F

the Charact of (FreeMSA F

ts is Relation-like Function-like Element of Args (o,(FreeMSA F

ts * ( the carrier of F

(Den (o,(FreeMSA F

(f1 . (the_result_sort_of o)) . ((Den (o,(FreeMSA F

x is Relation-like K101() -defined Function-like V31() FinSequence-like FinSubsequence-like Element of (Union the Sorts of F

[o,x] is V15() set

{o,x} is non empty set

{o} is non empty set

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

H /. [o,x] is Element of Union the Sorts of F

F

Args (o,F

the Sorts of F

rng ( the Sorts of F

the Arity of F

( the Arity of F

a is Relation-like Function-like Element of Args (o,F

[o,a] is V15() set

{o,a} is non empty set

{{o,a},{o}} is non empty set

Result (o,F

rng the Sorts of F

the ResultSort of F

( the ResultSort of F

Den (o,F

[:(Args (o,F

bool [:(Args (o,F

the Charact of F

the Charact of F

(Den (o,F

H . [o,x] is set