:: MSAFREE semantic presentation

K33() is set

K37() is non empty V7() V8() V9() Element of bool K33()

bool K33() is non empty set

K34() is set

K32() is non empty V7() V8() V9() set

bool K32() is non empty set

bool K37() is non empty set

{} is empty V7() V8() V9() V11() V12() V13() Relation-like non-empty empty-yielding K37() -defined Function-like one-to-one constant functional V35() V48() V49() FinSequence-like FinSubsequence-like FinSequence-membered V59() V60() V61() V62() V63() V64() set

the empty V7() V8() V9() V11() V12() V13() Relation-like non-empty empty-yielding K37() -defined Function-like one-to-one constant functional V35() V48() V49() FinSequence-like FinSubsequence-like FinSequence-membered V59() V60() V61() V62() V63() V64() set is empty V7() V8() V9() V11() V12() V13() Relation-like non-empty empty-yielding K37() -defined Function-like one-to-one constant functional V35() V48() V49() FinSequence-like FinSubsequence-like FinSequence-membered V59() V60() V61() V62() V63() V64() set

1 is non empty V7() V8() V9() V13() Element of K37()

{{},1} is non empty set

K257() is non empty V59() set

bool K257() is non empty set

K258() is non empty V59() V60() Element of bool K257()

PeanoNat is non empty strict with_terminals with_nonterminals with_useful_nonterminals DTConstrStr

the carrier of PeanoNat is non empty set

K261( the carrier of PeanoNat) is non empty functional V61() M14( the carrier of PeanoNat)

TS PeanoNat is non empty functional V61() Element of bool K261( the carrier of PeanoNat)

bool K261( the carrier of PeanoNat) is non empty set

[:(TS PeanoNat),K37():] is non empty Relation-like set

bool [:(TS PeanoNat),K37():] is non empty set

[:K37(),(TS PeanoNat):] is non empty Relation-like set

bool [:K37(),(TS PeanoNat):] is non empty set

2 is non empty V7() V8() V9() V13() Element of K37()

3 is non empty V7() V8() V9() V13() Element of K37()

K38() is empty V7() V8() V9() V11() V12() V13() Relation-like non-empty empty-yielding K37() -defined Function-like one-to-one constant functional V35() V48() V49() FinSequence-like FinSubsequence-like FinSequence-membered V59() V60() V61() V62() V63() V64() Element of K37()

K242(K38()) is non empty V54() set

<*> K37() is empty proper V7() V8() V9() V11() V12() V13() Relation-like non-empty empty-yielding K37() -defined K37() -valued Function-like one-to-one constant functional V35() Cardinal-yielding V48() V49() FinSequence-like FinSubsequence-like FinSequence-membered V59() V60() V61() V62() V63() V64() FinSequence of K37()

[:K37(),K37():] is non empty Relation-like set

S is set

U1 is non empty set

U1 * is non empty functional FinSequence-membered M19(U1)

[:S,(U1 *):] is Relation-like set

bool [:S,(U1 *):] is non empty set

U0 is Relation-like S -defined U1 * -valued Function-like total V29(S,U1 * ) V48() V49() Element of bool [:S,(U1 *):]

F is non empty Relation-like U1 -defined Function-like total set

F # is non empty Relation-like U1 * -defined Function-like total set

U0 * (F #) is Relation-like S -defined Function-like total set

FG is Relation-like K37() -defined U1 -valued Function-like V35() FinSequence-like FinSubsequence-like Element of U1 *

FG * F is Relation-like K37() -defined Function-like set

product (FG * F) is set

fa is set

U0 . fa is Relation-like K37() -defined Function-like V35() FinSequence-like FinSubsequence-like set

(U0 * (F #)) . fa is set

dom U0 is Element of bool S

bool S is non empty set

dom (U0 * (F #)) is Element of bool S

(F #) . FG is set

S is set

U1 is Relation-like S -defined Function-like total set

U0 is Relation-like S -defined Function-like total set

F is Relation-like S -defined Function-like total ManySortedSubset of U1

FG is Relation-like S -defined Function-like total V48() V49() ManySortedFunction of U1,U0

fa is set

U1 . fa is set

U0 . fa is set

[:(U1 . fa),(U0 . fa):] is Relation-like set

bool [:(U1 . fa),(U0 . fa):] is non empty set

FG . fa is Relation-like Function-like set

F . fa is set

f is Relation-like U1 . fa -defined U0 . fa -valued Function-like V29(U1 . fa,U0 . fa) Element of bool [:(U1 . fa),(U0 . fa):]

f | (F . fa) is Relation-like U1 . fa -defined F . fa -defined U1 . fa -defined U0 . fa -valued Function-like Element of bool [:(U1 . fa),(U0 . fa):]

F is Relation-like U1 . fa -defined U0 . fa -valued Function-like V29(U1 . fa,U0 . fa) Element of bool [:(U1 . fa),(U0 . fa):]

F | (F . fa) is Relation-like U1 . fa -defined F . fa -defined U1 . fa -defined U0 . fa -valued Function-like Element of bool [:(U1 . fa),(U0 . fa):]

fa is Relation-like Function-like set

proj1 fa is set

f is Relation-like S -defined Function-like total set

F is set

f . F is set

F . F is set

U0 . F is set

[:(F . F),(U0 . F):] is Relation-like set

bool [:(F . F),(U0 . F):] is non empty set

U1 . F is set

[:(U1 . F),(U0 . F):] is Relation-like set

bool [:(U1 . F),(U0 . F):] is non empty set

FG . F is Relation-like Function-like set

a is Relation-like U1 . F -defined U0 . F -valued Function-like V29(U1 . F,U0 . F) Element of bool [:(U1 . F),(U0 . F):]

a | (F . F) is Relation-like F . F -defined U1 . F -defined U0 . F -valued Function-like Element of bool [:(U1 . F),(U0 . F):]

dom a is Element of bool (U1 . F)

bool (U1 . F) is non empty set

proj2 (a | (F . F)) is set

dom (a | (F . F)) is Element of bool (U1 . F)

(dom a) /\ (F . F) is Element of bool (U1 . F)

F is Relation-like S -defined Function-like total V48() V49() ManySortedFunction of F,U0

a is set

U1 . a is set

U0 . a is set

[:(U1 . a),(U0 . a):] is Relation-like set

bool [:(U1 . a),(U0 . a):] is non empty set

s is Relation-like U1 . a -defined U0 . a -valued Function-like V29(U1 . a,U0 . a) Element of bool [:(U1 . a),(U0 . a):]

FG . a is Relation-like Function-like set

F . a is Relation-like Function-like set

F . a is set

s | (F . a) is Relation-like U1 . a -defined F . a -defined U1 . a -defined U0 . a -valued Function-like Element of bool [:(U1 . a),(U0 . a):]

fa is Relation-like S -defined Function-like total V48() V49() ManySortedFunction of F,U0

f is Relation-like S -defined Function-like total V48() V49() ManySortedFunction of F,U0

F is set

fa . F is Relation-like Function-like set

f . F is Relation-like Function-like set

U1 . F is set

U0 . F is set

[:(U1 . F),(U0 . F):] is Relation-like set

bool [:(U1 . F),(U0 . F):] is non empty set

FG . F is Relation-like Function-like set

a is Relation-like U1 . F -defined U0 . F -valued Function-like V29(U1 . F,U0 . F) Element of bool [:(U1 . F),(U0 . F):]

F . F is set

a | (F . F) is Relation-like U1 . F -defined F . F -defined U1 . F -defined U0 . F -valued Function-like Element of bool [:(U1 . F),(U0 . F):]

S is set

U0 is set

U1 is Relation-like S -defined Function-like total set

U1 . U0 is set

[:(U1 . U0),S:] is Relation-like set

F is set

FG is set

fa is set

[fa,U0] is V26() set

{fa,U0} is non empty set

{fa} is non empty set

{{fa,U0},{fa}} is non empty set

F is set

FG is set

fa is set

f is set

[f,U0] is V26() set

{f,U0} is non empty set

{f} is non empty set

{{f,U0},{f}} is non empty set

fa is set

f is set

[f,U0] is V26() set

{f,U0} is non empty set

{f} is non empty set

{{f,U0},{f}} is non empty set

S is set

S is set

U1 is Relation-like S -defined Function-like total set

disjoin U1 is Relation-like Function-like set

proj1 (disjoin U1) is set

dom U1 is Element of bool S

bool S is non empty set

S is set

U1 is Relation-like S -defined Function-like total set

disjoin U1 is Relation-like S -defined Function-like set

dom (disjoin U1) is Element of bool S

bool S is non empty set

dom U1 is Element of bool S

S is set

U1 is Relation-like S -defined Function-like total set

disjoin U1 is Relation-like S -defined Function-like total set

U0 is Relation-like Function-like set

proj1 U0 is set

F is set

dom U1 is Element of bool S

bool S is non empty set

U0 . F is set

U1 . F is set

{F} is non empty set

[:(U1 . F),{F}:] is Relation-like set

FG is set

fa is set

f is set

[fa,f] is V26() set

{fa,f} is non empty set

{fa} is non empty set

{{fa,f},{fa}} is non empty set

F is set

[F,F] is V26() set

{F,F} is non empty set

{F} is non empty set

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

fa is set

[fa,F] is V26() set

{fa,F} is non empty set

{fa} is non empty set

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

(S,U1,F) is set

F is set

FG is set

(S,U1,F) is set

U1 . F is set

{F} is non empty set

[:(U1 . F),{F}:] is Relation-like set

fa is set

[fa,F] is V26() set

{fa,F} is non empty set

{fa} is non empty set

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

fa is set

f is set

[fa,f] is V26() set

{fa,f} is non empty set

{fa} is non empty set

{{fa,f},{fa}} is non empty set

U0 . F is set

S is non empty set

U1 is non empty Relation-like non-empty non empty-yielding S -defined Function-like total set

(S,U1) is non empty Relation-like S -defined Function-like total set

U0 is set

F is Element of S

U1 . F is non empty set

FG is set

(S,U1) . F is set

(S,U1,F) is set

[FG,F] is V26() set

{FG,F} is non empty set

{FG} is non empty set

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

(S,U1) . U0 is set

S is non empty set

U1 is non empty Relation-like non-empty non empty-yielding S -defined Function-like total set

Union U1 is set

the Element of S is Element of S

U1 . the Element of S is non empty set

F is set

dom U1 is non empty Element of bool S

bool S is non empty set

proj2 U1 is non empty set

union (proj2 U1) is set

S is set

U1 is Relation-like S -defined Function-like total set

(S,U1) is Relation-like S -defined Function-like total set

U0 is set

U1 . U0 is set

(S,U1) . U0 is set

(S,U1,U0) is set

F is set

[F,U0] is V26() set

{F,U0} is non empty set

{F} is non empty set

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

F is set

FG is set

[FG,U0] is V26() set

{FG,U0} is non empty set

{FG} is non empty set

{{FG,U0},{FG}} is non empty set

S is non empty non void V78() ManySortedSign

the carrier of S is non empty set

U1 is MSAlgebra over S

the Sorts of U1 is non empty Relation-like the carrier of S -defined Function-like total set

F is non empty Relation-like the carrier of S -defined Function-like total ManySortedSubset of the Sorts of U1

GenMSAlg F is strict MSSubAlgebra of U1

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

S is non empty non void V78() ManySortedSign

the carrier of S is non empty set

U1 is strict non-empty MSAlgebra over S

the Sorts of U1 is non empty Relation-like non-empty non empty-yielding the carrier of S -defined Function-like total set

U0 is non empty Relation-like the carrier of S -defined Function-like total ManySortedSubset of the Sorts of U1

GenMSAlg U0 is strict MSSubAlgebra of U1

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

F is MSSubAlgebra of U1

the Sorts of F is non empty Relation-like the carrier of S -defined Function-like total set

S is non empty non void V78() ManySortedSign

the carrier of S is non empty set

U1 is MSAlgebra over S

S is non empty non void V78() ManySortedSign

S is non empty non void V78() ManySortedSign

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

U1 is non empty Relation-like the carrier of S -defined Function-like total set

( the carrier of S,U1) is non empty Relation-like the carrier of S -defined Function-like total set

Union ( the carrier of S,U1) is set

(Union ( the carrier of S,U1)) /\ [: the carrier' of S,{ the carrier of S}:] is Relation-like set

U0 is set

proj2 ( the carrier of S,U1) is non empty set

union (proj2 ( the carrier of S,U1)) is set

F is set

dom ( the carrier of S,U1) is non empty Element of bool the carrier of S

bool the carrier of S is non empty set

FG is set

( the carrier of S,U1) . FG is set

fa is Element of the carrier of S

( the carrier of S,U1,fa) is set

U1 . fa is set

f is set

[f,fa] is V26() set

{f,fa} is non empty set

{f} is non empty set

{{f,fa},{f}} is non empty set

S is non empty non void V78() ManySortedSign

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

U1 is non empty Relation-like the carrier of S -defined Function-like total set

( the carrier of S,U1) is non empty Relation-like the carrier of S -defined Function-like total set

Union ( the carrier of S,U1) is set

[: the carrier' of S,{ the carrier of S}:] \/ (Union ( the carrier of S,U1)) is non empty set

([: the carrier' of S,{ the carrier of S}:] \/ (Union ( the carrier of S,U1))) * is non empty functional FinSequence-membered M19([: the carrier' of S,{ the carrier of S}:] \/ (Union ( the carrier of S,U1)))

[:([: the carrier' of S,{ the carrier of S}:] \/ (Union ( the carrier of S,U1))),(([: the carrier' of S,{ the carrier of S}:] \/ (Union ( the carrier of S,U1))) *):] is non empty Relation-like set

bool [:([: the carrier' of S,{ the carrier of S}:] \/ (Union ( the carrier of S,U1))),(([: the carrier' of S,{ the carrier of S}:] \/ (Union ( the carrier of S,U1))) *):] is non empty set

F is Relation-like [: the carrier' of S,{ the carrier of S}:] \/ (Union ( the carrier of S,U1)) -defined ([: the carrier' of S,{ the carrier of S}:] \/ (Union ( the carrier of S,U1))) * -valued Element of bool [:([: the carrier' of S,{ the carrier of S}:] \/ (Union ( the carrier of S,U1))),(([: the carrier' of S,{ the carrier of S}:] \/ (Union ( the carrier of S,U1))) *):]

FG is Element of [: the carrier' of S,{ the carrier of S}:] \/ (Union ( the carrier of S,U1))

fa is Relation-like K37() -defined [: the carrier' of S,{ the carrier of S}:] \/ (Union ( the carrier of S,U1)) -valued Function-like V35() FinSequence-like FinSubsequence-like Element of ([: the carrier' of S,{ the carrier of S}:] \/ (Union ( the carrier of S,U1))) *

[FG,fa] is V26() set

{FG,fa} is non empty set

{FG} is non empty set

{{FG,fa},{FG}} is non empty set

len fa is V7() V8() V9() V13() Element of K37()

dom fa is Element of bool K37()

f is Element of the carrier' of S

[f, the carrier of S] is V26() set

{f, the carrier of S} is non empty set

{f} is non empty set

{{f, the carrier of S},{f}} is non empty set

the_arity_of f is Relation-like K37() -defined the carrier of S -valued Function-like V35() FinSequence-like FinSubsequence-like Element of the carrier of S *

the carrier of S * is non empty functional FinSequence-membered M19( the carrier of S)

len (the_arity_of f) is V7() V8() V9() V13() Element of K37()

F is set

fa . F 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 f) . F is set

( the carrier of S,U1,((the_arity_of f) . F)) is set

F is Relation-like [: the carrier' of S,{ the carrier of S}:] \/ (Union ( the carrier of S,U1)) -defined ([: the carrier' of S,{ the carrier of S}:] \/ (Union ( the carrier of S,U1))) * -valued Element of bool [:([: the carrier' of S,{ the carrier of S}:] \/ (Union ( the carrier of S,U1))),(([: the carrier' of S,{ the carrier of S}:] \/ (Union ( the carrier of S,U1))) *):]

FG is Relation-like [: the carrier' of S,{ the carrier of S}:] \/ (Union ( the carrier of S,U1)) -defined ([: the carrier' of S,{ the carrier of S}:] \/ (Union ( the carrier of S,U1))) * -valued Element of bool [:([: the carrier' of S,{ the carrier of S}:] \/ (Union ( the carrier of S,U1))),(([: the carrier' of S,{ the carrier of S}:] \/ (Union ( the carrier of S,U1))) *):]

fa is set

f is set

[fa,f] is V26() set

{fa,f} is non empty set

{fa} is non empty set

{{fa,f},{fa}} is non empty set

F is Element of [: the carrier' of S,{ the carrier of S}:] \/ (Union ( the carrier of S,U1))

a is Relation-like K37() -defined [: the carrier' of S,{ the carrier of S}:] \/ (Union ( the carrier of S,U1)) -valued Function-like V35() FinSequence-like FinSubsequence-like Element of ([: the carrier' of S,{ the carrier of S}:] \/ (Union ( the carrier of S,U1))) *

[F,a] is V26() set

{F,a} is non empty set

{F} is non empty set

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

len a is V7() V8() V9() V13() Element of K37()

dom a is Element of bool K37()

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_arity_of s is Relation-like K37() -defined the carrier of S -valued Function-like V35() FinSequence-like FinSubsequence-like Element of the carrier of S *

the carrier of S * is non empty functional FinSequence-membered M19( the carrier of S)

len (the_arity_of s) is V7() V8() V9() V13() Element of K37()

s0 is set

a . s0 is set

g is Element of the carrier' of S

[g, the carrier of S] is V26() set

{g, the carrier of S} is non empty set

{g} is non empty set

{{g, the carrier of S},{g}} is non empty set

the_result_sort_of g is Element of the carrier of S

(the_arity_of s) . s0 is set

( the carrier of S,U1,((the_arity_of s) . s0)) is set

F is Element of [: the carrier' of S,{ the carrier of S}:] \/ (Union ( the carrier of S,U1))

a is Relation-like K37() -defined [: the carrier' of S,{ the carrier of S}:] \/ (Union ( the carrier of S,U1)) -valued Function-like V35() FinSequence-like FinSubsequence-like Element of ([: the carrier' of S,{ the carrier of S}:] \/ (Union ( the carrier of S,U1))) *

[F,a] is V26() set

{F,a} is non empty set

{F} is non empty set

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

len a is V7() V8() V9() V13() Element of K37()

dom a is Element of bool K37()

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_arity_of s is Relation-like K37() -defined the carrier of S -valued Function-like V35() FinSequence-like FinSubsequence-like Element of the carrier of S *

the carrier of S * is non empty functional FinSequence-membered M19( the carrier of S)

len (the_arity_of s) is V7() V8() V9() V13() Element of K37()

s0 is set

a . s0 is set

g is Element of the carrier' of S

[g, the carrier of S] is V26() set

{g, the carrier of S} is non empty set

{g} is non empty set

{{g, the carrier of S},{g}} is non empty set

the_result_sort_of g is Element of the carrier of S

(the_arity_of s) . s0 is set

( the carrier of S,U1,((the_arity_of s) . s0)) is set

S is non empty non void V78() ManySortedSign

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

U1 is non empty Relation-like the carrier of S -defined Function-like total set

( the carrier of S,U1) is non empty Relation-like the carrier of S -defined Function-like total set

Union ( the carrier of S,U1) is set

[: the carrier' of S,{ the carrier of S}:] \/ (Union ( the carrier of S,U1)) is non empty set

([: the carrier' of S,{ the carrier of S}:] \/ (Union ( the carrier of S,U1))) * is non empty functional FinSequence-membered M19([: the carrier' of S,{ the carrier of S}:] \/ (Union ( the carrier of S,U1)))

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

[:([: the carrier' of S,{ the carrier of S}:] \/ (Union ( the carrier of S,U1))),(([: the carrier' of S,{ the carrier of S}:] \/ (Union ( the carrier of S,U1))) *):] is non empty Relation-like set

bool [:([: the carrier' of S,{ the carrier of S}:] \/ (Union ( the carrier of S,U1))),(([: the carrier' of S,{ the carrier of S}:] \/ (Union ( the carrier of S,U1))) *):] is non empty set

U0 is Element of the carrier' of S

[U0, the carrier of S] is V26() set

{U0, the carrier of S} is non empty set

{U0} is non empty set

{{U0, the carrier of S},{U0}} is non empty set

the_arity_of U0 is Relation-like K37() -defined the carrier of S -valued Function-like V35() FinSequence-like FinSubsequence-like Element of the carrier of S *

the carrier of S * is non empty functional FinSequence-membered M19( the carrier of S)

len (the_arity_of U0) is V7() V8() V9() V13() Element of K37()

F is Relation-like K37() -defined [: the carrier' of S,{ the carrier of S}:] \/ (Union ( the carrier of S,U1)) -valued Function-like V35() FinSequence-like FinSubsequence-like Element of ([: the carrier' of S,{ the carrier of S}:] \/ (Union ( the carrier of S,U1))) *

[[U0, the carrier of S],F] is V26() set

{[U0, the carrier of S],F} is non empty set

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

{{[U0, the carrier of S],F},{[U0, the carrier of S]}} is non empty set

len F is V7() V8() V9() V13() Element of K37()

dom F is Element of bool K37()

fa is Element of [: the carrier' of S,{ the carrier of S}:] \/ (Union ( the carrier of S,U1))

f is Element of the carrier' of S

[f, the carrier of S] is V26() set

{f, the carrier of S} is non empty set

{f} is non empty set

{{f, the carrier of S},{f}} is non empty set

the_arity_of f is Relation-like K37() -defined the carrier of S -valued Function-like V35() FinSequence-like FinSubsequence-like Element of the carrier of S *

len (the_arity_of f) is V7() V8() V9() V13() Element of K37()

F is set

F . F 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 f) . F is set

( the carrier of S,U1,((the_arity_of f) . F)) is set

f is set

F . f is set

F is Element of the carrier' of S

[F, the carrier of S] is V26() set

{F, the carrier of S} is non empty set

{F} is non empty set

{{F, the carrier of S},{F}} is non empty set

the_result_sort_of F is Element of the carrier of S

(the_arity_of U0) . f is set

( the carrier of S,U1,((the_arity_of U0) . f)) is set

f is Element of the carrier' of S

[f, the carrier of S] is V26() set

{f, the carrier of S} is non empty set

{f} is non empty set

{{f, the carrier of S},{f}} is non empty set

fa is Element of [: the carrier' of S,{ the carrier of S}:] \/ (Union ( the carrier of S,U1))

the_arity_of f is Relation-like K37() -defined the carrier of S -valued Function-like V35() FinSequence-like FinSubsequence-like Element of the carrier of S *

len (the_arity_of f) is V7() V8() V9() V13() Element of K37()

F is set

F . F 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 f) . F is set

( the carrier of S,U1,((the_arity_of f) . F)) is set

S is non empty non void V78() ManySortedSign

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

U1 is non empty Relation-like the carrier of S -defined Function-like total set

( the carrier of S,U1) is non empty Relation-like the carrier of S -defined Function-like total set

Union ( the carrier of S,U1) is set

[: the carrier' of S,{ the carrier of S}:] \/ (Union ( the carrier of S,U1)) is non empty set

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

([: the carrier' of S,{ the carrier of S}:] \/ (Union ( the carrier of S,U1))) * is non empty functional FinSequence-membered M19([: the carrier' of S,{ the carrier of S}:] \/ (Union ( the carrier of S,U1)))

[:([: the carrier' of S,{ the carrier of S}:] \/ (Union ( the carrier of S,U1))),(([: the carrier' of S,{ the carrier of S}:] \/ (Union ( the carrier of S,U1))) *):] is non empty Relation-like set

bool [:([: the carrier' of S,{ the carrier of S}:] \/ (Union ( the carrier of S,U1))),(([: the carrier' of S,{ the carrier of S}:] \/ (Union ( the carrier of S,U1))) *):] is non empty set

DTConstrStr(# ([: the carrier' of S,{ the carrier of S}:] \/ (Union ( the carrier of S,U1))),(S,U1) #) is non empty strict DTConstrStr

S is non empty non void V78() ManySortedSign

the carrier of S is non empty set

U1 is non empty Relation-like the carrier of S -defined Function-like total set

(S,U1) 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

( the carrier of S,U1) is non empty Relation-like the carrier of S -defined Function-like total set

Union ( the carrier of S,U1) is set

[: the carrier' of S,{ the carrier of S}:] \/ (Union ( the carrier of S,U1)) is non empty set

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

([: the carrier' of S,{ the carrier of S}:] \/ (Union ( the carrier of S,U1))) * is non empty functional FinSequence-membered M19([: the carrier' of S,{ the carrier of S}:] \/ (Union ( the carrier of S,U1)))

[:([: the carrier' of S,{ the carrier of S}:] \/ (Union ( the carrier of S,U1))),(([: the carrier' of S,{ the carrier of S}:] \/ (Union ( the carrier of S,U1))) *):] is non empty Relation-like set

bool [:([: the carrier' of S,{ the carrier of S}:] \/ (Union ( the carrier of S,U1))),(([: the carrier' of S,{ the carrier of S}:] \/ (Union ( the carrier of S,U1))) *):] is non empty set

DTConstrStr(# ([: the carrier' of S,{ the carrier of S}:] \/ (Union ( the carrier of S,U1))),(S,U1) #) is non empty strict DTConstrStr

S is non empty non void V78() ManySortedSign

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

U1 is non empty Relation-like the carrier of S -defined Function-like total set

(S,U1) is non empty strict DTConstrStr

( the carrier of S,U1) is non empty Relation-like the carrier of S -defined Function-like total set

Union ( the carrier of S,U1) is set

[: the carrier' of S,{ the carrier of S}:] \/ (Union ( the carrier of S,U1)) is non empty set

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

([: the carrier' of S,{ the carrier of S}:] \/ (Union ( the carrier of S,U1))) * is non empty functional FinSequence-membered M19([: the carrier' of S,{ the carrier of S}:] \/ (Union ( the carrier of S,U1)))

[:([: the carrier' of S,{ the carrier of S}:] \/ (Union ( the carrier of S,U1))),(([: the carrier' of S,{ the carrier of S}:] \/ (Union ( the carrier of S,U1))) *):] is non empty Relation-like set

bool [:([: the carrier' of S,{ the carrier of S}:] \/ (Union ( the carrier of S,U1))),(([: the carrier' of S,{ the carrier of S}:] \/ (Union ( the carrier of S,U1))) *):] is non empty set

DTConstrStr(# ([: the carrier' of S,{ the carrier of S}:] \/ (Union ( the carrier of S,U1))),(S,U1) #) is non empty strict DTConstrStr

NonTerminals (S,U1) is set

Terminals (S,U1) is set

the carrier of (S,U1) is non empty set

(Terminals (S,U1)) \/ (NonTerminals (S,U1)) is set

FG is set

{ b

fa is Element of the carrier of (S,U1)

f is Relation-like K37() -defined Function-like V35() FinSequence-like FinSubsequence-like set

f is Relation-like K37() -defined Function-like V35() FinSequence-like FinSubsequence-like set

[fa,f] is V26() set

{fa,f} is non empty set

{fa} is non empty set

{{fa,f},{fa}} is non empty set

the Rules of (S,U1) is Relation-like the carrier of (S,U1) -defined the carrier of (S,U1) * -valued Element of bool [: the carrier of (S,U1),( the carrier of (S,U1) *):]

the carrier of (S,U1) * is non empty functional FinSequence-membered M19( the carrier of (S,U1))

[: the carrier of (S,U1),( the carrier of (S,U1) *):] is non empty Relation-like set

bool [: the carrier of (S,U1),( the carrier of (S,U1) *):] is non empty set

a is Element of [: the carrier' of S,{ the carrier of S}:] \/ (Union ( the carrier of S,U1))

F is Relation-like K37() -defined [: the carrier' of S,{ the carrier of S}:] \/ (Union ( the carrier of S,U1)) -valued Function-like V35() FinSequence-like FinSubsequence-like Element of ([: the carrier' of S,{ the carrier of S}:] \/ (Union ( the carrier of S,U1))) *

[a,F] is V26() set

{a,F} is non empty set

{a} is non empty set

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

FG is set

FG is set

fa is Element of the carrier' of S

f is Element of { the carrier of S}

[fa,f] is V26() set

{fa,f} is non empty set

{fa} is non empty set

{{fa,f},{fa}} is non empty set

the_arity_of fa is Relation-like K37() -defined the carrier of S -valued Function-like V35() FinSequence-like FinSubsequence-like Element of the carrier of S *

the carrier of S * is non empty functional FinSequence-membered M19( the carrier of S)

len (the_arity_of fa) is V7() V8() V9() V13() Element of K37()

Seg (len (the_arity_of fa)) is V35() V42( len (the_arity_of fa)) Element of bool K37()

a is set

(the_arity_of fa) . a is set

( the carrier of S,U1,((the_arity_of fa) . a)) is set

dom (the_arity_of fa) is Element of bool K37()

proj2 (the_arity_of fa) is set

U1 . ((the_arity_of fa) . a) is set

s is set

[s,((the_arity_of fa) . a)] is V26() set

{s,((the_arity_of fa) . a)} is non empty set

{s} is non empty set

{{s,((the_arity_of fa) . a)},{s}} is non empty set

a is Relation-like Function-like set

proj1 a is set

s is Relation-like K37() -defined Function-like V35() FinSequence-like FinSubsequence-like set

proj2 s is set

s0 is set

proj2 (the_arity_of fa) is set

dom s is Element of bool K37()

g is set

s . g is set

dom (the_arity_of fa) is Element of bool K37()

(the_arity_of fa) . g is set

dom ( the carrier of S,U1) is non empty Element of bool the carrier of S

bool the carrier of S is non empty set

( the carrier of S,U1) . ((the_arity_of fa) . g) is set

proj2 ( the carrier of S,U1) is non empty set

( the carrier of S,U1,((the_arity_of fa) . g)) is set

union (proj2 ( the carrier of S,U1)) is set

s0 is Relation-like K37() -defined [: the carrier' of S,{ the carrier of S}:] \/ (Union ( the carrier of S,U1)) -valued Function-like V35() FinSequence-like FinSubsequence-like FinSequence of [: the carrier' of S,{ the carrier of S}:] \/ (Union ( the carrier of S,U1))

x is set

g is Relation-like K37() -defined [: the carrier' of S,{ the carrier of S}:] \/ (Union ( the carrier of S,U1)) -valued Function-like V35() FinSequence-like FinSubsequence-like Element of ([: the carrier' of S,{ the carrier of S}:] \/ (Union ( the carrier of S,U1))) *

dom g is Element of bool K37()

dom (the_arity_of fa) is Element of bool K37()

(the_arity_of fa) . x is set

proj2 (the_arity_of fa) is set

dom ( the carrier of S,U1) is non empty Element of bool the carrier of S

bool the carrier of S is non empty set

( the carrier of S,U1) . ((the_arity_of fa) . x) is set

proj2 ( the carrier of S,U1) is non empty set

( the carrier of S,U1,((the_arity_of fa) . x)) is set

g . x is set

union (proj2 ( the carrier of S,U1)) is set

D is Element of the carrier' of S

[D, the carrier of S] is V26() set

{D, the carrier of S} is non empty set

{D} is non empty set

{{D, the carrier of S},{D}} is non empty set

the_result_sort_of D is Element of the carrier of S

[fa, the carrier of S] is V26() set

{fa, the carrier of S} is non empty set

{{fa, the carrier of S},{fa}} is non empty set

len g is V7() V8() V9() V13() Element of K37()

x is Element of the carrier of (S,U1)

[x,g] is V26() set

{x,g} is non empty set

{x} is non empty set

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

{ b

FG is set

S is non empty non void V78() ManySortedSign

the carrier of S is non empty set

U1 is non empty Relation-like non-empty non empty-yielding the carrier of S -defined Function-like total set

(S,U1) 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

( the carrier of S,U1) is non empty Relation-like non-empty non empty-yielding the carrier of S -defined Function-like total set

Union ( the carrier of S,U1) is non empty set

[: the carrier' of S,{ the carrier of S}:] \/ (Union ( the carrier of S,U1)) is non empty set

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

([: the carrier' of S,{ the carrier of S}:] \/ (Union ( the carrier of S,U1))) * is non empty functional FinSequence-membered M19([: the carrier' of S,{ the carrier of S}:] \/ (Union ( the carrier of S,U1)))

[:([: the carrier' of S,{ the carrier of S}:] \/ (Union ( the carrier of S,U1))),(([: the carrier' of S,{ the carrier of S}:] \/ (Union ( the carrier of S,U1))) *):] is non empty Relation-like set

bool [:([: the carrier' of S,{ the carrier of S}:] \/ (Union ( the carrier of S,U1))),(([: the carrier' of S,{ the carrier of S}:] \/ (Union ( the carrier of S,U1))) *):] is non empty set

DTConstrStr(# ([: the carrier' of S,{ the carrier of S}:] \/ (Union ( the carrier of S,U1))),(S,U1) #) is non empty strict DTConstrStr

Terminals (S,U1) is set

NonTerminals (S,U1) is set

the carrier of (S,U1) is non empty set

K261( the carrier of (S,U1)) is non empty functional V61() M14( the carrier of (S,U1))

TS (S,U1) is functional V61() Element of bool K261( the carrier of (S,U1))

bool K261( the carrier of (S,U1)) is non empty set

FG is Element of the carrier of (S,U1)

fa is Element of the carrier' of S

f is Element of { the carrier of S}

[fa,f] is V26() set

{fa,f} is non empty set

{fa} is non empty set

{{fa,f},{fa}} is non empty set

the_arity_of fa is Relation-like K37() -defined the carrier of S -valued Function-like V35() FinSequence-like FinSubsequence-like Element of the carrier of S *

the carrier of S * is non empty functional FinSequence-membered M19( the carrier of S)

len (the_arity_of fa) is V7() V8() V9() V13() Element of K37()

Seg (len (the_arity_of fa)) is V35() V42( len (the_arity_of fa)) Element of bool K37()

a is set

(the_arity_of fa) . a is set

( the carrier of S,U1,((the_arity_of fa) . a)) is set

dom (the_arity_of fa) is Element of bool K37()

proj2 (the_arity_of fa) is set

U1 . ((the_arity_of fa) . a) is set

s is set

[s,((the_arity_of fa) . a)] is V26() set

{s,((the_arity_of fa) . a)} is non empty set

{s} is non empty set

{{s,((the_arity_of fa) . a)},{s}} is non empty set

a is Relation-like Function-like set

proj1 a is set

s is Relation-like K37() -defined Function-like V35() FinSequence-like FinSubsequence-like set

proj2 s is set

s0 is set

proj2 (the_arity_of fa) is set

dom s is Element of bool K37()

g is set

s . g is set

dom (the_arity_of fa) is Element of bool K37()

(the_arity_of fa) . g is set

dom ( the carrier of S,U1) is non empty Element of bool the carrier of S

bool the carrier of S is non empty set

( the carrier of S,U1) . ((the_arity_of fa) . g) is set

proj2 ( the carrier of S,U1) is non empty set

( the carrier of S,U1,((the_arity_of fa) . g)) is set

union (proj2 ( the carrier of S,U1)) is set

s0 is Relation-like K37() -defined [: the carrier' of S,{ the carrier of S}:] \/ (Union ( the carrier of S,U1)) -valued Function-like V35() FinSequence-like FinSubsequence-like FinSequence of [: the carrier' of S,{ the carrier of S}:] \/ (Union ( the carrier of S,U1))

g is Relation-like K37() -defined [: the carrier' of S,{ the carrier of S}:] \/ (Union ( the carrier of S,U1)) -valued Function-like V35() FinSequence-like FinSubsequence-like Element of ([: the carrier' of S,{ the carrier of S}:] \/ (Union ( the carrier of S,U1))) *

dom g is Element of bool K37()

x is Relation-like Function-like set

proj1 x is set

D is Relation-like K37() -defined Function-like V35() FinSequence-like FinSubsequence-like set

proj2 D is set

t is set

proj2 (the_arity_of fa) is set

dom D is Element of bool K37()

t is set

D . t is set

dom (the_arity_of fa) is Element of bool K37()

(the_arity_of fa) . t is set

dom ( the carrier of S,U1) is non empty Element of bool the carrier of S

bool the carrier of S is non empty set

( the carrier of S,U1) . ((the_arity_of fa) . t) is set

proj2 ( the carrier of S,U1) is non empty set

( the carrier of S,U1,((the_arity_of fa) . t)) is set

g . t is set

proj2 g is set

union (proj2 ( the carrier of S,U1)) is set

h is Element of the carrier of (S,U1)

root-tree (g . t) is Relation-like Function-like DecoratedTree-like set

t is Relation-like K37() -defined K261( the carrier of (S,U1)) -valued Function-like V35() V48() V49() FinSequence-like FinSubsequence-like FinSequence of TS (S,U1)

roots t is Relation-like K37() -defined the carrier of (S,U1) -valued Function-like V35() FinSequence-like FinSubsequence-like FinSequence of the carrier of (S,U1)

t is set

(roots t) . t is set

g . t is set

t . t is Relation-like Function-like set

root-tree (g . t) is Relation-like Function-like DecoratedTree-like set

h is V7() V8() V9() V13() set

t . h is Relation-like Function-like set

(roots t) . h is set

h is Relation-like Function-like DecoratedTree-like set

h . {} is set

t is set

dom (the_arity_of fa) is Element of bool K37()

(the_arity_of fa) . t is set

proj2 (the_arity_of fa) is set

dom ( the carrier of S,U1) is non empty Element of bool the carrier of S

bool the carrier of S is non empty set

( the carrier of S,U1) . ((the_arity_of fa) . t) is set

proj2 ( the carrier of S,U1) is non empty set

( the carrier of S,U1,((the_arity_of fa) . t)) is set

g . t is set

union (proj2 ( the carrier of S,U1)) is set

h is Element of the carrier' of S

[h, the carrier of S] is V26() set

{h, the carrier of S} is non empty set

{h} is non empty set

{{h, the carrier of S},{h}} is non empty set

the_result_sort_of h is Element of the carrier of S

len g is V7() V8() V9() V13() Element of K37()

[FG,g] is V26() set

{FG,g} is non empty set

{FG} is non empty set

{{FG,g},{FG}} is non empty set

dom (roots t) is Element of bool K37()

dom t is Element of bool K37()

S is non empty non void V78() ManySortedSign

the carrier of S is non empty set

U1 is non empty Relation-like the carrier of S -defined Function-like total set

(S,U1) 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

( the carrier of S,U1) is non empty Relation-like the carrier of S -defined Function-like total set

Union ( the carrier of S,U1) is set

[: the carrier' of S,{ the carrier of S}:] \/ (Union ( the carrier of S,U1)) is non empty set

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

([: the carrier' of S,{ the carrier of S}:] \/ (Union ( the carrier of S,U1))) * is non empty functional FinSequence-membered M19([: the carrier' of S,{ the carrier of S}:] \/ (Union ( the carrier of S,U1)))

[:([: the carrier' of S,{ the carrier of S}:] \/ (Union ( the carrier of S,U1))),(([: the carrier' of S,{ the carrier of S}:] \/ (Union ( the carrier of S,U1))) *):] is non empty Relation-like set

bool [:([: the carrier' of S,{ the carrier of S}:] \/ (Union ( the carrier of S,U1))),(([: the carrier' of S,{ the carrier of S}:] \/ (Union ( the carrier of S,U1))) *):] is non empty set

DTConstrStr(# ([: the carrier' of S,{ the carrier of S}:] \/ (Union ( the carrier of S,U1))),(S,U1) #) is non empty strict DTConstrStr

Terminals (S,U1) is set

U0 is set

proj2 ( the carrier of S,U1) is non empty set

union (proj2 ( the carrier of S,U1)) is set

FG is set

dom ( the carrier of S,U1) is non empty Element of bool the carrier of S

bool the carrier of S is non empty set

fa is set

( the carrier of S,U1) . fa is set

f is Element of the carrier of S

( the carrier of S,U1) . f is set

( the carrier of S,U1,f) is set

U1 . f is set

F is set

[F,f] is V26() set

{F,f} is non empty set

{F} is non empty set

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

FG is Element of the carrier of S

U1 . FG is set

fa is set

[fa,FG] is V26() set

{fa,FG} is non empty set

{fa} is non empty set

{{fa,FG},{fa}} is non empty set

dom ( the carrier of S,U1) is non empty Element of bool the carrier of S

bool the carrier of S is non empty set

( the carrier of S,U1) . FG is set

( the carrier of S,U1,FG) is set

S is non empty non void V78() ManySortedSign

the carrier of S is non empty set

the carrier' of S is non empty set

U0 is Element of the carrier' of S

[U0, the carrier of S] is V26() set

{U0, the carrier of S} is non empty set

{U0} is non empty set

{{U0, the carrier of S},{U0}} is non empty set

U1 is non empty Relation-like non-empty non empty-yielding the carrier of S -defined Function-like total set

(S,U1) 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

( the carrier of S,U1) is non empty Relation-like non-empty non empty-yielding the carrier of S -defined Function-like total set

Union ( the carrier of S,U1) is non empty set

[: the carrier' of S,{ the carrier of S}:] \/ (Union ( the carrier of S,U1)) is non empty set

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

([: the carrier' of S,{ the carrier of S}:] \/ (Union ( the carrier of S,U1))) * is non empty functional FinSequence-membered M19([: the carrier' of S,{ the carrier of S}:] \/ (Union ( the carrier of S,U1)))

[:([: the carrier' of S,{ the carrier of S}:] \/ (Union ( the carrier of S,U1))),(([: the carrier' of S,{ the carrier of S}:] \/ (Union ( the carrier of S,U1))) *):] is non empty Relation-like set

bool [:([: the carrier' of S,{ the carrier of S}:] \/ (Union ( the carrier of S,U1))),(([: the carrier' of S,{ the carrier of S}:] \/ (Union ( the carrier of S,U1))) *):] is non empty set

DTConstrStr(# ([: the carrier' of S,{ the carrier of S}:] \/ (Union ( the carrier of S,U1))),(S,U1) #) is non empty strict DTConstrStr

the carrier of (S,U1) is non empty set

NonTerminals (S,U1) is non empty Element of bool the carrier of (S,U1)

bool the carrier of (S,U1) is non empty set

S is non empty non void V78() ManySortedSign

the carrier of S is non empty set

U1 is non empty Relation-like non-empty non empty-yielding the carrier of S -defined Function-like total set

(S,U1) 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

( the carrier of S,U1) is non empty Relation-like non-empty non empty-yielding the carrier of S -defined Function-like total set

Union ( the carrier of S,U1) is non empty set

[: the carrier' of S,{ the carrier of S}:] \/ (Union ( the carrier of S,U1)) is non empty set

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

([: the carrier' of S,{ the carrier of S}:] \/ (Union ( the carrier of S,U1))) * is non empty functional FinSequence-membered M19([: the carrier' of S,{ the carrier of S}:] \/ (Union ( the carrier of S,U1)))

[:([: the carrier' of S,{ the carrier of S}:] \/ (Union ( the carrier of S,U1))),(([: the carrier' of S,{ the carrier of S}:] \/ (Union ( the carrier of S,U1))) *):] is non empty Relation-like set

bool [:([: the carrier' of S,{ the carrier of S}:] \/ (Union ( the carrier of S,U1))),(([: the carrier' of S,{ the carrier of S}:] \/ (Union ( the carrier of S,U1))) *):] is non empty set

DTConstrStr(# ([: the carrier' of S,{ the carrier of S}:] \/ (Union ( the carrier of S,U1))),(S,U1) #) is non empty strict DTConstrStr

the carrier of (S,U1) is non empty set

K261( the carrier of (S,U1)) is non empty functional V61() M14( the carrier of (S,U1))

TS (S,U1) is non empty functional V61() Element of bool K261( the carrier of (S,U1))

bool K261( the carrier of (S,U1)) is non empty set

U0 is Element of the carrier of S

U1 . U0 is non empty set

{ b

( b

( [b

bool (TS (S,U1)) is non empty set

FG is set

fa is Relation-like the carrier of (S,U1) -valued Function-like DecoratedTree-like Element of TS (S,U1)

f is set

[f,U0] is V26() set

{f,U0} is non empty set

{f} is non empty set

{{f,U0},{f}} is non empty set

root-tree [f,U0] is Relation-like Function-like DecoratedTree-like set

F is Element of the carrier' of S

[F, the carrier of S] is V26() set

{F, the carrier of S} is non empty set

{F} is non empty set

{{F, the carrier of S},{F}} is non empty set

fa . {} is set

the_result_sort_of F is Element of the carrier of S

S is non empty non void V78() ManySortedSign

the carrier of S is non empty set

U1 is non empty Relation-like non-empty non empty-yielding the carrier of S -defined Function-like total set

U0 is Element of the carrier of S

(S,U1,U0) is functional V61() Element of bool (TS (S,U1))

(S,U1) 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

( the carrier of S,U1) is non empty Relation-like non-empty non empty-yielding the carrier of S -defined Function-like total set

Union ( the carrier of S,U1) is non empty set

[: the carrier' of S,{ the carrier of S}:] \/ (Union ( the carrier of S,U1)) is non empty set

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

([: the carrier' of S,{ the carrier of S}:] \/ (Union ( the carrier of S,U1))) * is non empty functional FinSequence-membered M19([: the carrier' of S,{ the carrier of S}:] \/ (Union ( the carrier of S,U1)))

[:([: the carrier' of S,{ the carrier of S}:] \/ (Union ( the carrier of S,U1))),(([: the carrier' of S,{ the carrier of S}:] \/ (Union ( the carrier of S,U1))) *):] is non empty Relation-like set

bool [:([: the carrier' of S,{ the carrier of S}:] \/ (Union ( the carrier of S,U1))),(([: the carrier' of S,{ the carrier of S}:] \/ (Union ( the carrier of S,U1))) *):] is non empty set

DTConstrStr(# ([: the carrier' of S,{ the carrier of S}:] \/ (Union ( the carrier of S,U1))),(S,U1) #) is non empty strict DTConstrStr

TS (S,U1) is non empty functional V61() Element of bool K261( the carrier of (S,U1))

the carrier of (S,U1) is non empty set

K261( the carrier of (S,U1)) is non empty functional V61() M14( the carrier of (S,U1))

bool K261( the carrier of (S,U1)) is non empty set

bool (TS (S,U1)) is non empty set

U1 . U0 is non empty set

{ b

( b

( [b

dom ( the carrier of S,U1) is non empty Element of bool the carrier of S

bool the carrier of S is non empty set

( the carrier of S,U1) . U0 is non empty set

proj2 ( the carrier of S,U1) is non empty set

( the carrier of S,U1,U0) is set

FG is set

[FG,U0] is V26() set

{FG,U0} is non empty set

{FG} is non empty set

{{FG,U0},{FG}} is non empty set

Terminals (S,U1) is non empty Element of bool the carrier of (S,U1)

bool the carrier of (S,U1) is non empty set

union (proj2 ( the carrier of S,U1)) is set

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

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

F is Relation-like the carrier of (S,U1) -valued Function-like DecoratedTree-like Element of TS (S,U1)

S is non empty non void V78() ManySortedSign

the carrier of S is non empty set

U1 is non empty Relation-like non-empty non empty-yielding the carrier of S -defined Function-like total set

(S,U1) 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

( the carrier of S,U1) is non empty Relation-like non-empty non empty-yielding the carrier of S -defined Function-like total set

Union ( the carrier of S,U1) is non empty set

[: the carrier' of S,{ the carrier of S}:] \/ (Union ( the carrier of S,U1)) is non empty set

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

([: the carrier' of S,{ the carrier of S}:] \/ (Union ( the carrier of S,U1))) * is non empty functional FinSequence-membered M19([: the carrier' of S,{ the carrier of S}:] \/ (Union ( the carrier of S,U1)))

[:([: the carrier' of S,{ the carrier of S}:] \/ (Union ( the carrier of S,U1))),(([: the carrier' of S,{ the carrier of S}:] \/ (Union ( the carrier of S,U1))) *):] is non empty Relation-like set

bool [:([: the carrier' of S,{ the carrier of S}:] \/ (Union ( the carrier of S,U1))),(([: the carrier' of S,{ the carrier of S}:] \/ (Union ( the carrier of S,U1))) *):] is non empty set

DTConstrStr(# ([: the carrier' of S,{ the carrier of S}:] \/ (Union ( the carrier of S,U1))),(S,U1) #) is non empty strict DTConstrStr

TS (S,U1) is non empty functional V61() Element of bool K261( the carrier of (S,U1))

the carrier of (S,U1) is non empty set

K261( the carrier of (S,U1)) is non empty functional V61() M14( the carrier of (S,U1))

bool K261( the carrier of (S,U1)) is non empty set

bool (TS (S,U1)) is non empty set

U0 is Relation-like Function-like set

proj1 U0 is set

F is non empty Relation-like the carrier of S -defined Function-like total set

FG is Element of the carrier of S

F . FG is set

(S,U1,FG) is non empty functional V61() Element of bool (TS (S,U1))

U1 . FG is non empty set

{ b

( b

( [b

U0 is non empty Relation-like the carrier of S -defined Function-like total set

F is non empty Relation-like the carrier of S -defined Function-like total set

FG is set

U0 . FG is set

F . FG is set

fa is Element of the carrier of S

U0 . fa is set

(S,U1,fa) is non empty functional V61() Element of bool (TS (S,U1))

(S,U1) 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

( the carrier of S,U1) is non empty Relation-like non-empty non empty-yielding the carrier of S -defined Function-like total set

Union ( the carrier of S,U1) is non empty set

[: the carrier' of S,{ the carrier of S}:] \/ (Union ( the carrier of S,U1)) is non empty set

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

([: the carrier' of S,{ the carrier of S}:] \/ (Union ( the carrier of S,U1))) * is non empty functional FinSequence-membered M19([: the carrier' of S,{ the carrier of S}:] \/ (Union ( the carrier of S,U1)))

[:([: the carrier' of S,{ the carrier of S}:] \/ (Union ( the carrier of S,U1))),(([: the carrier' of S,{ the carrier of S}:] \/ (Union ( the carrier of S,U1))) *):] is non empty Relation-like set

bool [:([: the carrier' of S,{ the carrier of S}:] \/ (Union ( the carrier of S,U1))),(([: the carrier' of S,{ the carrier of S}:] \/ (Union ( the carrier of S,U1))) *):] is non empty set

DTConstrStr(# ([: the carrier' of S,{ the carrier of S}:] \/ (Union ( the carrier of S,U1))),(S,U1) #) is non empty strict DTConstrStr

TS (S,U1) is non empty functional V61() Element of bool K261( the carrier of (S,U1))

the carrier of (S,U1) is non empty set

K261( the carrier of (S,U1)) is non empty functional V61() M14( the carrier of (S,U1))

bool K261( the carrier of (S,U1)) is non empty set

bool (TS (S,U1)) is non empty set

U1 . fa is non empty set

{ b

( b

( [b

S is non empty non void V78() ManySortedSign

the carrier of S is non empty set

U1 is non empty Relation-like non-empty non empty-yielding the carrier of S -defined Function-like total set

(S,U1) is non empty Relation-like the carrier of S -defined Function-like total set

U0 is set

(S,U1) . U0 is set

F is Element of the carrier of S

(S,U1) . F is set

(S,U1,F) is non empty functional V61() Element of bool (TS (S,U1))

(S,U1) 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

( the carrier of S,U1) is non empty Relation-like non-empty non empty-yielding the carrier of S -defined Function-like total set

Union ( the carrier of S,U1) is non empty set

[: the carrier' of S,{ the carrier of S}:] \/ (Union ( the carrier of S,U1)) is non empty set

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

([: the carrier' of S,{ the carrier of S}:] \/ (Union ( the carrier of S,U1))) * is non empty functional FinSequence-membered M19([: the carrier' of S,{ the carrier of S}:] \/ (Union ( the carrier of S,U1)))

[:([: the carrier' of S,{ the carrier of S}:] \/ (Union ( the carrier of S,U1))),(([: the carrier' of S,{ the carrier of S}:] \/ (Union ( the carrier of S,U1))) *):] is non empty Relation-like set

bool [:([: the carrier' of S,{ the carrier of S}:] \/ (Union ( the carrier of S,U1))),(([: the carrier' of S,{ the carrier of S}:] \/ (Union ( the carrier of S,U1))) *):] is non empty set

DTConstrStr(# ([: the carrier' of S,{ the carrier of S}:] \/ (Union ( the carrier of S,U1))),(S,U1) #) is non empty strict DTConstrStr

TS (S,U1) is non empty functional V61() Element of bool K261( the carrier of (S,U1))

the carrier of (S,U1) is non empty set

K261( the carrier of (S,U1)) is non empty functional V61() M14( the carrier of (S,U1))

bool K261( the carrier of (S,U1)) is non empty set

bool (TS (S,U1)) is non empty set

U1 . F is non empty set

{ b

( b

( [b

S is non empty non void V78() ManySortedSign

the carrier of S is non empty set

the carrier' of S is non empty set

the Arity of S is non empty Relation-like the carrier' of S -defined the carrier of S * -valued Function-like total V29( the carrier' of S, the carrier of S * ) V48() V49() Element of bool [: the carrier' of S,( the carrier of S *):]

the carrier of S * is non empty functional FinSequence-membered M19( 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

U1 is non empty Relation-like non-empty non empty-yielding the carrier of S -defined Function-like total set

(S,U1) is non empty Relation-like non-empty non empty-yielding the carrier of S -defined Function-like total set

(S,U1) # is non empty Relation-like the carrier of S * -defined Function-like total set

the Arity of S * ((S,U1) #) is non empty Relation-like the carrier' of S -defined Function-like total set

(S,U1) 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

( the carrier of S,U1) is non empty Relation-like non-empty non empty-yielding the carrier of S -defined Function-like total set

Union ( the carrier of S,U1) is non empty set

[: the carrier' of S,{ the carrier of S}:] \/ (Union ( the carrier of S,U1)) is non empty set

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

([: the carrier' of S,{ the carrier of S}:] \/ (Union ( the carrier of S,U1))) * is non empty functional FinSequence-membered M19([: the carrier' of S,{ the carrier of S}:] \/ (Union ( the carrier of S,U1)))

[:([: the carrier' of S,{ the carrier of S}:] \/ (Union ( the carrier of S,U1))),(([: the carrier' of S,{ the carrier of S}:] \/ (Union ( the carrier of S,U1))) *):] is non empty Relation-like set

bool [:([: the carrier' of S,{ the carrier of S}:] \/ (Union ( the carrier of S,U1))),(([: the carrier' of S,{ the carrier of S}:] \/ (Union ( the carrier of S,U1))) *):] is non empty set

DTConstrStr(# ([: the carrier' of S,{ the carrier of S}:] \/ (Union ( the carrier of S,U1))),(S,U1) #) is non empty strict DTConstrStr

the carrier of (S,U1) is non empty set

K261( the carrier of (S,U1)) is non empty