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
{ b1 where b1 is Element of the carrier of (S,U1) : ex b2 being Relation-like K37() -defined Function-like V35() FinSequence-like FinSubsequence-like set st b1 ==> b2 } is set
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
{ b1 where b1 is Element of the carrier of (S,U1) : ex b2 being Relation-like K37() -defined Function-like V35() FinSequence-like FinSubsequence-like set st b1 ==> b2 } is set
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
{ b1 where b1 is Relation-like the carrier of (S,U1) -valued Function-like DecoratedTree-like Element of TS (S,U1) : ( ex b2 being set st
( b2 in U1 . U0 & b1 = root-tree [b2,U0] ) or ex b2 being Element of the carrier' of S st
( [b2, the carrier of S] = b1 . {} & the_result_sort_of b2 = U0 ) ) } is set
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
{ b1 where b1 is Relation-like the carrier of (S,U1) -valued Function-like DecoratedTree-like Element of TS (S,U1) : ( ex b2 being set st
( b2 in U1 . U0 & b1 = root-tree [b2,U0] ) or ex b2 being Element of the carrier' of S st
( [b2, the carrier of S] = b1 . {} & the_result_sort_of b2 = U0 ) ) } 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) . 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
{ b1 where b1 is Relation-like the carrier of (S,U1) -valued Function-like DecoratedTree-like Element of TS (S,U1) : ( ex b2 being set st
( b2 in U1 . FG & b1 = root-tree [b2,FG] ) or ex b2 being Element of the carrier' of S st
( [b2, the carrier of S] = b1 . {} & the_result_sort_of b2 = FG ) ) } is set
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
{ b1 where b1 is Relation-like the carrier of (S,U1) -valued Function-like DecoratedTree-like Element of TS (S,U1) : ( ex b2 being set st
( b2 in U1 . fa & b1 = root-tree [b2,fa] ) or ex b2 being Element of the carrier' of S st
( [b2, the carrier of S] = b1 . {} & the_result_sort_of b2 = fa ) ) } 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 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
{ b1 where b1 is Relation-like the carrier of (S,U1) -valued Function-like DecoratedTree-like Element of TS (S,U1) : ( ex b2 being set st
( b2 in U1 . F & b1 = root-tree [b2,F] ) or ex b2 being Element of the carrier' of S st
( [b2, the carrier of S] = b1 . {} & the_result_sort_of b2 = 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 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 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
( the Arity of S * ((S,U1) #)) . U0 is set
F is 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 Arity of S . U0 is Relation-like K37() -defined Function-like V35() FinSequence-like FinSubsequence-like Element of the carrier of S *
proj2 (the_arity_of U0) is set
dom (S,U1) is non empty Element of bool the carrier of S
bool the carrier of S is non empty set
(the_arity_of U0) * (S,U1) is Relation-like non-empty K37() -defined Function-like set
dom ((the_arity_of U0) * (S,U1)) is Element of bool K37()
dom (the_arity_of U0) is Element of bool K37()
product ((the_arity_of U0) * (S,U1)) is set
F is Relation-like Function-like set
proj1 F is set
len (the_arity_of U0) is V7() V8() V9() V13() Element of K37()
Seg (len (the_arity_of U0)) is V35() V42( len (the_arity_of U0)) Element of bool K37()
a is Relation-like K37() -defined Function-like V35() FinSequence-like FinSubsequence-like set
proj2 a is set
s is set
dom a is Element of bool K37()
s0 is set
a . s0 is set
((the_arity_of U0) * (S,U1)) . s0 is set
g is V7() V8() V9() V13() set
((the_arity_of U0) * (S,U1)) . g is set
(the_arity_of U0) . g is set
(S,U1) . ((the_arity_of U0) . g) is set
(the_arity_of U0) /. g is Element of the carrier of S
(S,U1) . ((the_arity_of U0) /. g) is non empty set
(S,U1,((the_arity_of U0) /. g)) is non empty functional V61() Element of bool (TS (S,U1))
bool (TS (S,U1)) is non empty set
U1 . ((the_arity_of U0) /. g) is non empty set
{ b1 where b1 is Relation-like the carrier of (S,U1) -valued Function-like DecoratedTree-like Element of TS (S,U1) : ( ex b2 being set st
( b2 in U1 . ((the_arity_of U0) /. g) & b1 = root-tree [b2,((the_arity_of U0) /. g)] ) or ex b2 being Element of the carrier' of S st
( [b2, the carrier of S] = b1 . {} & the_result_sort_of b2 = (the_arity_of U0) /. g ) ) } is set
x is Relation-like the carrier of (S,U1) -valued Function-like DecoratedTree-like Element of TS (S,U1)
D is set
[D,((the_arity_of U0) /. g)] is V26() set
{D,((the_arity_of U0) /. g)} is non empty set
{D} is non empty set
{{D,((the_arity_of U0) /. g)},{D}} is non empty set
root-tree [D,((the_arity_of U0) /. g)] is Relation-like Function-like DecoratedTree-like set
t is Element of the carrier' of S
[t, the carrier of S] is V26() set
{t, the carrier of S} is non empty set
{t} is non empty set
{{t, the carrier of S},{t}} is non empty set
x . {} is set
the_result_sort_of t is Element of the carrier of S
s is Relation-like K37() -defined K261( the carrier of (S,U1)) -valued Function-like V35() V48() V49() FinSequence-like FinSubsequence-like V64() FinSequence of TS (S,U1)
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 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 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
(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
U0 is Element of the carrier' of S
( the Arity of S * ((S,U1) #)) . U0 is 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 *
dom (the_arity_of U0) is Element of bool K37()
F is Relation-like K37() -defined K261( the carrier of (S,U1)) -valued Function-like V35() V48() V49() FinSequence-like FinSubsequence-like V64() FinSequence of TS (S,U1)
dom F is Element of bool K37()
the Arity of S . U0 is Relation-like K37() -defined Function-like V35() FinSequence-like FinSubsequence-like Element of the carrier of S *
proj2 (the_arity_of U0) is set
dom (S,U1) is non empty Element of bool the carrier of S
bool the carrier of S is non empty set
(the_arity_of U0) * (S,U1) is Relation-like non-empty K37() -defined Function-like set
dom ((the_arity_of U0) * (S,U1)) is Element of bool K37()
product ((the_arity_of U0) * (S,U1)) is set
F is V7() V8() V9() V13() set
F . F is Relation-like Function-like set
(the_arity_of U0) /. F is Element of the carrier of S
(S,U1,((the_arity_of U0) /. F)) is non empty functional V61() Element of bool (TS (S,U1))
bool (TS (S,U1)) is non empty set
U1 . ((the_arity_of U0) /. F) is non empty set
{ b1 where b1 is Relation-like the carrier of (S,U1) -valued Function-like DecoratedTree-like Element of TS (S,U1) : ( ex b2 being set st
( b2 in U1 . ((the_arity_of U0) /. F) & b1 = root-tree [b2,((the_arity_of U0) /. F)] ) or ex b2 being Element of the carrier' of S st
( [b2, the carrier of S] = b1 . {} & the_result_sort_of b2 = (the_arity_of U0) /. F ) ) } is set
((the_arity_of U0) * (S,U1)) . F is set
(the_arity_of U0) . F is set
(S,U1) . ((the_arity_of U0) . F) is set
(S,U1) . ((the_arity_of U0) /. F) is non empty set
proj2 (the_arity_of U0) is set
dom (S,U1) is non empty Element of bool the carrier of S
bool the carrier of S is non empty set
(the_arity_of U0) * (S,U1) is Relation-like non-empty K37() -defined Function-like set
dom ((the_arity_of U0) * (S,U1)) is Element of bool K37()
F is set
F . F is Relation-like Function-like set
((the_arity_of U0) * (S,U1)) . F is set
a is V7() V8() V9() V13() set
(the_arity_of U0) /. a is Element of the carrier of S
(S,U1,((the_arity_of U0) /. a)) is non empty functional V61() Element of bool (TS (S,U1))
bool (TS (S,U1)) is non empty set
U1 . ((the_arity_of U0) /. a) is non empty set
{ b1 where b1 is Relation-like the carrier of (S,U1) -valued Function-like DecoratedTree-like Element of TS (S,U1) : ( ex b2 being set st
( b2 in U1 . ((the_arity_of U0) /. a) & b1 = root-tree [b2,((the_arity_of U0) /. a)] ) or ex b2 being Element of the carrier' of S st
( [b2, the carrier of S] = b1 . {} & the_result_sort_of b2 = (the_arity_of U0) /. a ) ) } is set
(S,U1) . ((the_arity_of U0) /. a) is non empty set
(the_arity_of U0) . a is set
(S,U1) . ((the_arity_of U0) . a) is set
the Arity of S . U0 is Relation-like K37() -defined Function-like V35() FinSequence-like FinSubsequence-like Element of the carrier of S *
product ((the_arity_of U0) * (S,U1)) 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 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 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 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
(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
U0 is Element of the carrier' of S
(S,U1,U0) is Element of the carrier of (S,U1)
[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 S * ((S,U1) #)) . U0 is set
F is Relation-like K37() -defined K261( the carrier of (S,U1)) -valued Function-like V35() V48() V49() FinSequence-like FinSubsequence-like V64() FinSequence of TS (S,U1)
roots F 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)
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 *
dom F is Element of bool K37()
dom (roots F) is Element of bool K37()
[[U0, the carrier of S],(roots F)] is V26() set
{[U0, the carrier of S],(roots F)} is non empty set
{[U0, the carrier of S]} is non empty Relation-like Function-like set
{{[U0, the carrier of S],(roots F)},{[U0, the carrier of S]}} is non empty set
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))) *
dom a is Element of bool K37()
len a is V7() V8() V9() V13() Element of K37()
Seg (len a) is V35() V42( len a) Element of bool K37()
len (the_arity_of U0) is V7() V8() V9() V13() Element of K37()
Seg (len (the_arity_of U0)) is V35() V42( len (the_arity_of U0)) Element of bool K37()
dom (the_arity_of U0) is Element of bool K37()
s is V7() V8() V9() V13() set
F . s is Relation-like Function-like set
(the_arity_of U0) /. s is Element of the carrier of S
(S,U1,((the_arity_of U0) /. s)) is non empty functional V61() Element of bool (TS (S,U1))
bool (TS (S,U1)) is non empty set
U1 . ((the_arity_of U0) /. s) is non empty set
{ b1 where b1 is Relation-like the carrier of (S,U1) -valued Function-like DecoratedTree-like Element of TS (S,U1) : ( ex b2 being set st
( b2 in U1 . ((the_arity_of U0) /. s) & b1 = root-tree [b2,((the_arity_of U0) /. s)] ) or ex b2 being Element of the carrier' of S st
( [b2, the carrier of S] = b1 . {} & the_result_sort_of b2 = (the_arity_of U0) /. s ) ) } is set
a . s is set
g is Relation-like Function-like DecoratedTree-like set
g . {} is set
proj2 F is set
proj2 a is set
D is Element of the carrier' of S
t is Element of { the carrier of S}
[D,t] is V26() set
{D,t} is non empty set
{D} is non empty set
{{D,t},{D}} is non empty set
the_result_sort_of D is Element of the carrier of S
(the_arity_of U0) . s is set
x is Relation-like the carrier of (S,U1) -valued Function-like DecoratedTree-like Element of TS (S,U1)
x . {} is set
t is set
[t,((the_arity_of U0) /. s)] is V26() set
{t,((the_arity_of U0) /. s)} is non empty set
{t} is non empty set
{{t,((the_arity_of U0) /. s)},{t}} is non empty set
root-tree [t,((the_arity_of U0) /. s)] is Relation-like Function-like DecoratedTree-like 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
(the_arity_of U0) . s is set
( the carrier of S,U1,((the_arity_of U0) . s)) is set
( the carrier of S,U1,((the_arity_of U0) /. s)) is 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
x is Relation-like the carrier of (S,U1) -valued Function-like DecoratedTree-like Element of TS (S,U1)
D is Element of Terminals (S,U1)
root-tree D is Relation-like the carrier of (S,U1) -valued Function-like DecoratedTree-like Element of TS (S,U1)
t is set
[t,((the_arity_of U0) /. s)] is V26() set
{t,((the_arity_of U0) /. s)} is non empty set
{t} is non empty set
{{t,((the_arity_of U0) /. s)},{t}} is non empty set
len (roots F) is V7() V8() V9() V13() Element of K37()
Seg (len (roots F)) is V35() V42( len (roots F)) Element of bool K37()
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 FinSequence of [: the carrier' of S,{ the carrier of S}:] \/ (Union ( the carrier of S,U1))
dom (the_arity_of U0) is Element of bool K37()
s 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 s is Element of bool K37()
s0 is set
s . s0 is set
(the_arity_of U0) . s0 is set
( the carrier of S,U1,((the_arity_of U0) . s0)) is set
g is V7() V8() V9() V13() set
F . g is Relation-like Function-like set
s . g is set
(the_arity_of U0) /. g is Element of the carrier of S
(S,U1,((the_arity_of U0) /. g)) is non empty functional V61() Element of bool (TS (S,U1))
bool (TS (S,U1)) is non empty set
U1 . ((the_arity_of U0) /. g) is non empty set
{ b1 where b1 is Relation-like the carrier of (S,U1) -valued Function-like DecoratedTree-like Element of TS (S,U1) : ( ex b2 being set st
( b2 in U1 . ((the_arity_of U0) /. g) & b1 = root-tree [b2,((the_arity_of U0) /. g)] ) or ex b2 being Element of the carrier' of S st
( [b2, the carrier of S] = b1 . {} & the_result_sort_of b2 = (the_arity_of U0) /. g ) ) } is set
D is Relation-like the carrier of (S,U1) -valued Function-like DecoratedTree-like Element of TS (S,U1)
D . {} is set
(the_arity_of U0) . 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 U0) /. g) is non empty set
proj2 ( the carrier of S,U1) is non empty set
( the carrier of S,U1,((the_arity_of U0) /. g)) is set
t is set
[t,((the_arity_of U0) /. g)] is V26() set
{t,((the_arity_of U0) /. g)} is non empty set
{t} is non empty set
{{t,((the_arity_of U0) /. g)},{t}} is non empty set
root-tree [t,((the_arity_of U0) /. g)] is Relation-like Function-like DecoratedTree-like set
t is Relation-like Function-like DecoratedTree-like set
t . {} is set
union (proj2 ( the carrier of S,U1)) is set
t is Element of the carrier' of S
[t, the carrier of S] is V26() set
{t, the carrier of S} is non empty set
{t} is non empty set
{{t, the carrier of S},{t}} is non empty set
the_result_sort_of t is Element of the carrier of S
t is set
[t,((the_arity_of U0) /. g)] is V26() set
{t,((the_arity_of U0) /. g)} is non empty set
{t} is non empty set
{{t,((the_arity_of U0) /. g)},{t}} is non empty set
root-tree [t,((the_arity_of U0) /. g)] is Relation-like Function-like DecoratedTree-like 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
h is Relation-like Function-like DecoratedTree-like set
h . {} is set
t is Element of the carrier' of S
[t, the carrier of S] is V26() set
{t, the carrier of S} is non empty set
{t} is non empty set
{{t, the carrier of S},{t}} is non empty set
the_result_sort_of t is Element of the carrier of S
t is Relation-like Function-like DecoratedTree-like set
t . {} is set
t is set
[t,((the_arity_of U0) /. g)] is V26() set
{t,((the_arity_of U0) /. g)} is non empty set
{t} is non empty set
{{t,((the_arity_of U0) /. g)},{t}} is non empty set
root-tree [t,((the_arity_of U0) /. g)] is Relation-like Function-like DecoratedTree-like set
t is Element of the carrier' of S
[t, the carrier of S] is V26() set
{t, the carrier of S} is non empty set
{t} is non empty set
{{t, the carrier of S},{t}} is non empty set
the_result_sort_of t is Element of the carrier of S
t is set
[t,((the_arity_of U0) /. g)] is V26() set
{t,((the_arity_of U0) /. g)} is non empty set
{t} is non empty set
{{t,((the_arity_of U0) /. g)},{t}} is non empty set
root-tree [t,((the_arity_of U0) /. g)] is Relation-like Function-like DecoratedTree-like set
t is Relation-like Function-like DecoratedTree-like set
t . {} is set
len s is V7() V8() V9() V13() Element of K37()
len (the_arity_of U0) is V7() V8() V9() V13() Element of K37()
[[U0, the carrier of S],s] is V26() set
{[U0, the carrier of S],s} is non empty set
{[U0, the carrier of S]} is non empty Relation-like Function-like set
{{[U0, the carrier of S],s},{[U0, the carrier of S]}} 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 Relation-like non-empty non empty-yielding the carrier of S -defined Function-like total set
proj2 (S,U1) is non empty set
union (proj2 (S,U1)) is 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
dom (S,U1) is non empty Element of bool the carrier of S
bool the carrier of S is non empty set
F is set
FG is set
fa is set
(S,U1) . fa is set
f is Element of the carrier of S
(S,U1,f) is non empty functional V61() Element of bool (TS (S,U1))
bool (TS (S,U1)) is non empty set
U1 . f is non empty set
{ b1 where b1 is Relation-like the carrier of (S,U1) -valued Function-like DecoratedTree-like Element of TS (S,U1) : ( ex b2 being set st
( b2 in U1 . f & b1 = root-tree [b2,f] ) or ex b2 being Element of the carrier' of S st
( [b2, the carrier of S] = b1 . {} & the_result_sort_of b2 = f ) ) } is set
F is Relation-like the carrier of (S,U1) -valued Function-like DecoratedTree-like Element of TS (S,U1)
a is set
[a,f] is V26() set
{a,f} is non empty set
{a} is non empty set
{{a,f},{a}} is non empty set
root-tree [a,f] is Relation-like Function-like DecoratedTree-like set
s is Element of the carrier' of S
[s, the carrier of S] is V26() set
{s, the carrier of S} is non empty set
{s} is non empty set
{{s, the carrier of S},{s}} is non empty set
F . {} is set
the_result_sort_of s is Element of the carrier of S
F is set
FG is Relation-like the carrier of (S,U1) -valued Function-like DecoratedTree-like Element of TS (S,U1)
proj2 FG is 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
NonTerminals (S,U1) is non empty Element of bool the carrier of (S,U1)
(Terminals (S,U1)) \/ (NonTerminals (S,U1)) is non empty Element of bool the carrier of (S,U1)
proj1 FG is non empty V35() V54() set
FG . {} is set
fa is Element of Terminals (S,U1)
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
F is set
( the carrier of S,U1) . F is set
a is Element of the carrier of S
( the carrier of S,U1,a) is set
root-tree fa is Relation-like the carrier of (S,U1) -valued Function-like DecoratedTree-like Element of TS (S,U1)
U1 . a is non empty set
(S,U1,a) is non empty functional V61() Element of bool (TS (S,U1))
bool (TS (S,U1)) is non empty set
{ b1 where b1 is Relation-like the carrier of (S,U1) -valued Function-like DecoratedTree-like Element of TS (S,U1) : ( ex b2 being set st
( b2 in U1 . a & b1 = root-tree [b2,a] ) or ex b2 being Element of the carrier' of S st
( [b2, the carrier of S] = b1 . {} & the_result_sort_of b2 = a ) ) } is set
s is set
[s,a] is V26() set
{s,a} is non empty set
{s} is non empty set
{{s,a},{s}} is non empty set
(S,U1) . a is non empty set
fa is Element of NonTerminals (S,U1)
f is Element of the carrier' of S
F is Element of { the carrier of S}
[f,F] is V26() set
{f,F} is non empty set
{f} is non empty set
{{f,F},{f}} is non empty set
the_result_sort_of f is Element of the carrier of S
(S,U1,(the_result_sort_of f)) is non empty functional V61() Element of bool (TS (S,U1))
bool (TS (S,U1)) is non empty set
U1 . (the_result_sort_of f) is non empty set
{ b1 where b1 is Relation-like the carrier of (S,U1) -valued Function-like DecoratedTree-like Element of TS (S,U1) : ( ex b2 being set st
( b2 in U1 . (the_result_sort_of f) & b1 = root-tree [b2,(the_result_sort_of f)] ) or ex b2 being Element of the carrier' of S st
( [b2, the carrier of S] = b1 . {} & the_result_sort_of b2 = the_result_sort_of f ) ) } is set
(S,U1) . (the_result_sort_of f) 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 Relation-like non-empty non empty-yielding the carrier of S -defined Function-like total set
U0 is Element of the carrier of S
F is Element of the carrier of S
(S,U1) . U0 is non empty set
(S,U1) . F is non empty set
((S,U1) . U0) /\ ((S,U1) . F) is set
FG is 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
(S,U1,U0) is non empty functional V61() Element of bool (TS (S,U1))
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
{ b1 where b1 is Relation-like the carrier of (S,U1) -valued Function-like DecoratedTree-like Element of TS (S,U1) : ( ex b2 being set st
( b2 in U1 . U0 & b1 = root-tree [b2,U0] ) or ex b2 being Element of the carrier' of S st
( [b2, the carrier of S] = b1 . {} & the_result_sort_of b2 = U0 ) ) } is set
(S,U1,F) is non empty functional V61() Element of bool (TS (S,U1))
U1 . F is non empty set
{ b1 where b1 is Relation-like the carrier of (S,U1) -valued Function-like DecoratedTree-like Element of TS (S,U1) : ( ex b2 being set st
( b2 in U1 . F & b1 = root-tree [b2,F] ) or ex b2 being Element of the carrier' of S st
( [b2, the carrier of S] = b1 . {} & the_result_sort_of b2 = F ) ) } is set
f is Relation-like the carrier of (S,U1) -valued Function-like DecoratedTree-like Element of TS (S,U1)
f . {} is set
F is Relation-like the carrier of (S,U1) -valued Function-like DecoratedTree-like Element of TS (S,U1)
F . {} is set
a is set
[a,U0] is V26() set
{a,U0} is non empty set
{a} is non empty set
{{a,U0},{a}} is non empty set
root-tree [a,U0] is Relation-like Function-like DecoratedTree-like set
a is set
[a,U0] is V26() set
{a,U0} is non empty set
{a} is non empty set
{{a,U0},{a}} is non empty set
root-tree [a,U0] is Relation-like Function-like DecoratedTree-like set
s is set
[s,F] is V26() set
{s,F} is non empty set
{s} is non empty set
{{s,F},{s}} is non empty set
root-tree [s,F] is Relation-like Function-like DecoratedTree-like set
s is set
[s,F] is V26() set
{s,F} is non empty set
{s} is non empty set
{{s,F},{s}} is non empty set
root-tree [s,F] is Relation-like Function-like DecoratedTree-like set
s is Element of the carrier' of S
[s, the carrier of S] is V26() set
{s, the carrier of S} is non empty set
{s} is non empty set
{{s, the carrier of S},{s}} is non empty set
the_result_sort_of s is Element of the carrier of S
s is Element of the carrier' of S
[s, the carrier of S] is V26() set
{s, the carrier of S} is non empty set
{s} is non empty set
{{s, the carrier of S},{s}} is non empty set
the_result_sort_of s is Element of the carrier of S
s0 is set
s is set
[s,F] is V26() set
{s,F} is non empty set
{s} is non empty set
{{s,F},{s}} is non empty set
root-tree [s,F] is Relation-like Function-like DecoratedTree-like set
s0 is Element of the carrier' of S
[s0, the carrier of S] is V26() set
{s0, the carrier of S} is non empty set
{s0} is non empty set
{{s0, the carrier of S},{s0}} is non empty set
the_result_sort_of s0 is Element of the carrier of S
s is set
[s,F] is V26() set
{s,F} is non empty set
{s} is non empty set
{{s,F},{s}} is non empty set
root-tree [s,F] is Relation-like Function-like DecoratedTree-like set
s0 is Element of the carrier' of S
[s0, the carrier of S] is V26() set
{s0, the carrier of S} is non empty set
{s0} is non empty set
{{s0, the carrier of S},{s0}} is non empty set
the_result_sort_of s0 is Element of the carrier of S
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
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
s is set
[s,F] is V26() set
{s,F} is non empty set
{s} is non empty set
{{s,F},{s}} is non empty set
root-tree [s,F] is Relation-like Function-like DecoratedTree-like set
s is set
[s,F] is V26() set
{s,F} is non empty set
{s} is non empty set
{{s,F},{s}} is non empty set
root-tree [s,F] is Relation-like Function-like DecoratedTree-like set
s0 is set
s is Element of the carrier' of S
[s, the carrier of S] is V26() set
{s, the carrier of S} is non empty set
{s} is non empty set
{{s, the carrier of S},{s}} is non empty set
the_result_sort_of s is Element of the carrier of S
s is set
[s,F] is V26() set
{s,F} is non empty set
{s} is non empty set
{{s,F},{s}} is non empty set
root-tree [s,F] is Relation-like Function-like DecoratedTree-like set
s0 is Element of the carrier' of S
[s0, the carrier of S] is V26() set
{s0, the carrier of S} is non empty set
{s0} is non empty set
{{s0, the carrier of S},{s0}} is non empty set
the_result_sort_of s0 is Element of the carrier of S
s is set
[s,F] is V26() set
{s,F} is non empty set
{s} is non empty set
{{s,F},{s}} is non empty set
root-tree [s,F] is Relation-like Function-like DecoratedTree-like set
s0 is Element of the carrier' of S
[s0, the carrier of S] is V26() set
{s0, the carrier of S} is non empty set
{s0} is non empty set
{{s0, the carrier of S},{s0}} is non empty set
the_result_sort_of s0 is Element of the carrier of S
a is set
[a,U0] is V26() set
{a,U0} is non empty set
{a} is non empty set
{{a,U0},{a}} is non empty set
root-tree [a,U0] is Relation-like Function-like DecoratedTree-like set
s is Element of the carrier' of S
[s, the carrier of S] is V26() set
{s, the carrier of S} is non empty set
{s} is non empty set
{{s, the carrier of S},{s}} is non empty set
the_result_sort_of s is Element of the carrier of S
S 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
U0 is Element of the carrier' of S
( the Arity of S * ((S,U1) #)) . U0 is set
the ResultSort 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) Element of bool [: the carrier' of S, 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
the ResultSort of S * (S,U1) is non empty Relation-like non-empty non empty-yielding the carrier' of S -defined Function-like total set
( the ResultSort of S * (S,U1)) . U0 is non empty set
[:(( the Arity of S * ((S,U1) #)) . U0),(( the ResultSort of S * (S,U1)) . U0):] is Relation-like set
bool [:(( the Arity of S * ((S,U1) #)) . U0),(( the ResultSort of S * (S,U1)) . U0):] is non empty 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 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
(S,U1,U0) is Element of the carrier of (S,U1)
[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_result_sort_of U0 is Element of the carrier of S
s is set
s0 is Relation-like K37() -defined K261( the carrier of (S,U1)) -valued Function-like V35() V48() V49() FinSequence-like FinSubsequence-like V64() FinSequence of TS (S,U1)
roots s0 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)
(S,U1,U0) -tree s0 is Relation-like the carrier of (S,U1) -valued Function-like DecoratedTree-like Element of K261( the carrier of (S,U1))
x is Relation-like the carrier of (S,U1) -valued Function-like DecoratedTree-like Element of K261( the carrier of (S,U1))
dom ( the ResultSort of S * (S,U1)) is non empty Element of bool the carrier' of S
bool the carrier' of S is non empty set
the ResultSort of S . U0 is Element of the carrier of S
(S,U1) . ( the ResultSort of S . U0) is non empty set
(S,U1) . (the_result_sort_of U0) is non empty set
(S,U1,(the_result_sort_of U0)) is non empty functional V61() Element of bool (TS (S,U1))
bool (TS (S,U1)) is non empty set
U1 . (the_result_sort_of U0) is non empty set
{ b1 where b1 is Relation-like the carrier of (S,U1) -valued Function-like DecoratedTree-like Element of TS (S,U1) : ( ex b2 being set st
( b2 in U1 . (the_result_sort_of U0) & b1 = root-tree [b2,(the_result_sort_of U0)] ) or ex b2 being Element of the carrier' of S st
( [b2, the carrier of S] = b1 . {} & the_result_sort_of b2 = the_result_sort_of U0 ) ) } is set
g is Relation-like the carrier of (S,U1) -valued Function-like DecoratedTree-like Element of TS (S,U1)
g . {} is set
D is Relation-like K37() -defined K261( the carrier of (S,U1)) -valued Function-like V35() V48() V49() FinSequence-like FinSubsequence-like V64() FinSequence of TS (S,U1)
(S,U1,U0) -tree D is Relation-like the carrier of (S,U1) -valued Function-like DecoratedTree-like Element of K261( the carrier of (S,U1))
s is Relation-like Function-like set
proj1 s is set
proj2 s is set
[:(( the Arity of S * ((S,U1) #)) . U0),(proj2 s):] is Relation-like set
bool [:(( the Arity of S * ((S,U1) #)) . U0),(proj2 s):] is non empty set
s0 is Relation-like ( the Arity of S * ((S,U1) #)) . U0 -defined proj2 s -valued Function-like V29(( the Arity of S * ((S,U1) #)) . U0, proj2 s) Element of bool [:(( the Arity of S * ((S,U1) #)) . U0),(proj2 s):]
g is Relation-like ( the Arity of S * ((S,U1) #)) . U0 -defined ( the ResultSort of S * (S,U1)) . U0 -valued Function-like total V29(( the Arity of S * ((S,U1) #)) . U0,( the ResultSort of S * (S,U1)) . U0) Element of bool [:(( the Arity of S * ((S,U1) #)) . U0),(( the ResultSort of S * (S,U1)) . U0):]
x is Relation-like K37() -defined K261( the carrier of (S,U1)) -valued Function-like V35() V48() V49() FinSequence-like FinSubsequence-like V64() FinSequence of TS (S,U1)
roots x 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)
g . x is set
(S,U1,U0) -tree x 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 Arity of S * ((S,U1) #)) . U0 -defined ( the ResultSort of S * (S,U1)) . U0 -valued Function-like total V29(( the Arity of S * ((S,U1) #)) . U0,( the ResultSort of S * (S,U1)) . U0) Element of bool [:(( the Arity of S * ((S,U1) #)) . U0),(( the ResultSort of S * (S,U1)) . U0):]
F is Relation-like ( the Arity of S * ((S,U1) #)) . U0 -defined ( the ResultSort of S * (S,U1)) . U0 -valued Function-like total V29(( the Arity of S * ((S,U1) #)) . U0,( the ResultSort of S * (S,U1)) . U0) Element of bool [:(( the Arity of S * ((S,U1) #)) . U0),(( the ResultSort of S * (S,U1)) . U0):]
a is set
f . a is set
F . a is set
s is Relation-like K37() -defined K261( the carrier of (S,U1)) -valued Function-like V35() V48() V49() FinSequence-like FinSubsequence-like V64() FinSequence of TS (S,U1)
roots s 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)
f . s is set
(S,U1,U0) -tree s is Relation-like the carrier of (S,U1) -valued Function-like DecoratedTree-like Element of K261( the carrier of (S,U1))
dom f is Element of bool (( the Arity of S * ((S,U1) #)) . U0)
bool (( the Arity of S * ((S,U1) #)) . U0) is non empty set
dom F is Element of bool (( the Arity of S * ((S,U1) #)) . U0)
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
the ResultSort 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) Element of bool [: the carrier' of S, 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
the ResultSort of S * (S,U1) is non empty Relation-like non-empty non empty-yielding the carrier' of S -defined Function-like total set
F is set
FG is Element of the carrier' of S
(S,U1,FG) is Relation-like ( the Arity of S * ((S,U1) #)) . FG -defined ( the ResultSort of S * (S,U1)) . FG -valued Function-like total V29(( the Arity of S * ((S,U1) #)) . FG,( the ResultSort of S * (S,U1)) . FG) Element of bool [:(( the Arity of S * ((S,U1) #)) . FG),(( the ResultSort of S * (S,U1)) . FG):]
( the Arity of S * ((S,U1) #)) . FG is set
( the ResultSort of S * (S,U1)) . FG is non empty set
[:(( the Arity of S * ((S,U1) #)) . FG),(( the ResultSort of S * (S,U1)) . FG):] is Relation-like set
bool [:(( the Arity of S * ((S,U1) #)) . FG),(( the ResultSort of S * (S,U1)) . FG):] is non empty set
fa is Element of the carrier' of S
(S,U1,fa) is Relation-like ( the Arity of S * ((S,U1) #)) . fa -defined ( the ResultSort of S * (S,U1)) . fa -valued Function-like total V29(( the Arity of S * ((S,U1) #)) . fa,( the ResultSort of S * (S,U1)) . fa) Element of bool [:(( the Arity of S * ((S,U1) #)) . fa),(( the ResultSort of S * (S,U1)) . fa):]
( the Arity of S * ((S,U1) #)) . fa is set
( the ResultSort of S * (S,U1)) . fa is non empty set
[:(( the Arity of S * ((S,U1) #)) . fa),(( the ResultSort of S * (S,U1)) . fa):] is Relation-like set
bool [:(( the Arity of S * ((S,U1) #)) . fa),(( the ResultSort of S * (S,U1)) . fa):] is non empty set
F is Relation-like Function-like set
proj1 F is set
FG is non empty Relation-like the carrier' of S -defined Function-like total set
dom FG is non empty Element of bool the carrier' of S
bool the carrier' of S is non empty set
fa is set
FG . fa is set
f is Element of the carrier' of S
FG . f is set
(S,U1,f) is Relation-like ( the Arity of S * ((S,U1) #)) . f -defined ( the ResultSort of S * (S,U1)) . f -valued Function-like total V29(( the Arity of S * ((S,U1) #)) . f,( the ResultSort of S * (S,U1)) . f) Element of bool [:(( the Arity of S * ((S,U1) #)) . f),(( the ResultSort of S * (S,U1)) . f):]
( the Arity of S * ((S,U1) #)) . f is set
( the ResultSort of S * (S,U1)) . f is non empty set
[:(( the Arity of S * ((S,U1) #)) . f),(( the ResultSort of S * (S,U1)) . f):] is Relation-like set
bool [:(( the Arity of S * ((S,U1) #)) . f),(( the ResultSort of S * (S,U1)) . f):] is non empty set
fa is non empty Relation-like the carrier' of S -defined Function-like total V48() V49() set
f is set
fa . f is Relation-like Function-like set
( the Arity of S * ((S,U1) #)) . f is set
( the ResultSort of S * (S,U1)) . f is set
[:(( the Arity of S * ((S,U1) #)) . f),(( the ResultSort of S * (S,U1)) . f):] is Relation-like set
bool [:(( the Arity of S * ((S,U1) #)) . f),(( the ResultSort of S * (S,U1)) . f):] is non empty set
F is Element of the carrier' of S
fa . F is Relation-like Function-like set
(S,U1,F) is Relation-like ( the Arity of S * ((S,U1) #)) . F -defined ( the ResultSort of S * (S,U1)) . F -valued Function-like total V29(( the Arity of S * ((S,U1) #)) . F,( the ResultSort of S * (S,U1)) . F) Element of bool [:(( the Arity of S * ((S,U1) #)) . F),(( the ResultSort of S * (S,U1)) . F):]
( the Arity of S * ((S,U1) #)) . F is set
( the ResultSort of S * (S,U1)) . F is non empty set
[:(( the Arity of S * ((S,U1) #)) . F),(( the ResultSort of S * (S,U1)) . F):] is Relation-like set
bool [:(( the Arity of S * ((S,U1) #)) . F),(( the ResultSort of S * (S,U1)) . F):] is non empty set
f is non empty Relation-like the carrier' of S -defined Function-like total V48() V49() ManySortedFunction of the Arity of S * ((S,U1) #), the ResultSort of S * (S,U1)
F is Element of the carrier' of S
( the Arity of S * ((S,U1) #)) . F is set
f . F is Relation-like ( the Arity of S * ((S,U1) #)) . F -defined ( the ResultSort of S * (S,U1)) . F -valued Function-like total V29(( the Arity of S * ((S,U1) #)) . F,( the ResultSort of S * (S,U1)) . F) Element of bool [:(( the Arity of S * ((S,U1) #)) . F),(( the ResultSort of S * (S,U1)) . F):]
( the ResultSort of S * (S,U1)) . F is non empty set
[:(( the Arity of S * ((S,U1) #)) . F),(( the ResultSort of S * (S,U1)) . F):] is Relation-like set
bool [:(( the Arity of S * ((S,U1) #)) . F),(( the ResultSort of S * (S,U1)) . F):] is non empty set
(S,U1,F) is Relation-like ( the Arity of S * ((S,U1) #)) . F -defined ( the ResultSort of S * (S,U1)) . F -valued Function-like total V29(( the Arity of S * ((S,U1) #)) . F,( the ResultSort of S * (S,U1)) . F) Element of bool [:(( the Arity of S * ((S,U1) #)) . F),(( the ResultSort of S * (S,U1)) . F):]
U0 is non empty Relation-like the carrier' of S -defined Function-like total V48() V49() ManySortedFunction of the Arity of S * ((S,U1) #), the ResultSort of S * (S,U1)
F is non empty Relation-like the carrier' of S -defined Function-like total V48() V49() ManySortedFunction of the Arity of S * ((S,U1) #), the ResultSort of S * (S,U1)
FG is set
U0 . FG is Relation-like Function-like set
F . FG is Relation-like Function-like set
fa is Element of the carrier' of S
( the Arity of S * ((S,U1) #)) . fa is set
U0 . fa is Relation-like ( the Arity of S * ((S,U1) #)) . fa -defined ( the ResultSort of S * (S,U1)) . fa -valued Function-like total V29(( the Arity of S * ((S,U1) #)) . fa,( the ResultSort of S * (S,U1)) . fa) Element of bool [:(( the Arity of S * ((S,U1) #)) . fa),(( the ResultSort of S * (S,U1)) . fa):]
( the ResultSort of S * (S,U1)) . fa is non empty set
[:(( the Arity of S * ((S,U1) #)) . fa),(( the ResultSort of S * (S,U1)) . fa):] is Relation-like set
bool [:(( the Arity of S * ((S,U1) #)) . fa),(( the ResultSort of S * (S,U1)) . fa):] is non empty set
(S,U1,fa) is Relation-like ( the Arity of S * ((S,U1) #)) . fa -defined ( the ResultSort of S * (S,U1)) . fa -valued Function-like total V29(( the Arity of S * ((S,U1) #)) . fa,( the ResultSort of S * (S,U1)) . fa) Element of bool [:(( the Arity of S * ((S,U1) #)) . fa),(( the ResultSort of S * (S,U1)) . fa):]
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 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 V48() V49() ManySortedFunction of the Arity of S * ((S,U1) #), the ResultSort of S * (S,U1)
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
(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
the ResultSort 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) Element of bool [: the carrier' of S, 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
the ResultSort of S * (S,U1) is non empty Relation-like non-empty non empty-yielding the carrier' of S -defined Function-like total set
MSAlgebra(# (S,U1),(S,U1) #) is strict MSAlgebra over 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
(S,U1) is MSAlgebra over S
(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 V48() V49() ManySortedFunction of the Arity of S * ((S,U1) #), the ResultSort of S * (S,U1)
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
(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
the ResultSort 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) Element of bool [: the carrier' of S, 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
the ResultSort of S * (S,U1) is non empty Relation-like non-empty non empty-yielding the carrier' of S -defined Function-like total set
MSAlgebra(# (S,U1),(S,U1) #) is strict MSAlgebra over 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
(S,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 non empty set
bool ((S,U1) . U0) is non empty set
U1 . U0 is non empty 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
FG is set
fa is set
fa is Element of bool ((S,U1) . U0)
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
Terminals (S,U1) is non empty Element of bool the carrier of (S,U1)
the carrier of (S,U1) is non empty set
bool the carrier of (S,U1) is non empty set
f is 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
{ b1 where b1 is Relation-like the carrier of (S,U1) -valued Function-like DecoratedTree-like Element of TS (S,U1) : ( ex b2 being set st
( b2 in U1 . U0 & b1 = root-tree [b2,U0] ) or ex b2 being Element of the carrier' of S st
( [b2, the carrier of S] = b1 . {} & the_result_sort_of b2 = U0 ) ) } is set
a is set
[a,U0] is V26() set
{a,U0} is non empty set
{a} is non empty set
{{a,U0},{a}} is non empty set
root-tree [a,U0] is Relation-like Function-like DecoratedTree-like set
a is set
[a,U0] is V26() set
{a,U0} is non empty set
{a} is non empty set
{{a,U0},{a}} is non empty set
root-tree [a,U0] is Relation-like Function-like DecoratedTree-like set
(S,U1,U0) is non empty functional V61() Element of bool (TS (S,U1))
bool (TS (S,U1)) is non empty set
union (proj2 ( the carrier of S,U1)) is set
s0 is Element of the carrier of (S,U1)
root-tree s0 is Relation-like the carrier of (S,U1) -valued Function-like DecoratedTree-like Element of K261( the carrier of (S,U1))
g is Relation-like the carrier of (S,U1) -valued Function-like DecoratedTree-like Element of TS (S,U1)
x is set
[x,U0] is V26() set
{x,U0} is non empty set
{x} is non empty set
{{x,U0},{x}} is non empty set
root-tree [x,U0] is Relation-like Function-like DecoratedTree-like set
F is Element of bool ((S,U1) . U0)
FG is Element of bool ((S,U1) . U0)
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
root-tree [f,U0] is Relation-like Function-like DecoratedTree-like 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
root-tree [f,U0] is Relation-like Function-like DecoratedTree-like 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
U0 is Element of the carrier of S
(S,U1,U0) is Element of bool ((S,U1) . U0)
(S,U1) is non empty Relation-like non-empty non empty-yielding the carrier of S -defined Function-like total set
(S,U1) . U0 is non empty set
bool ((S,U1) . U0) is non empty set
U1 . U0 is non empty 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
root-tree [F,U0] is Relation-like Function-like DecoratedTree-like 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
root-tree [FG,U0] is Relation-like Function-like DecoratedTree-like 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
Terminals (S,U1) is non empty Element of bool the carrier of (S,U1)
bool the carrier of (S,U1) is non empty set
U0 is Element of the carrier of S
(S,U1,U0) is non empty Element of bool ((S,U1) . U0)
(S,U1) is non empty Relation-like non-empty non empty-yielding the carrier of S -defined Function-like total set
(S,U1) . U0 is non empty set
bool ((S,U1) . U0) is non empty set
{ (root-tree b1) where b1 is Element of the carrier of (S,U1) : ( b1 in Terminals (S,U1) & b1 `2 = U0 ) } is set
fa is set
U1 . U0 is non empty 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
root-tree [f,U0] is Relation-like Function-like DecoratedTree-like set
F is Element of the carrier of (S,U1)
F `2 is set
fa 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))
K261( the carrier of (S,U1)) is non empty functional V61() M14( the carrier of (S,U1))
f `2 is set
a is set
F is Element of the carrier of S
U1 . F is non empty set
[a,F] is V26() set
{a,F} is non empty set
{a} is non empty set
{{a,F},{a}} 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 strict non-empty MSAlgebra over S
(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 V48() V49() ManySortedFunction of the Arity of S * ((S,U1) #), the ResultSort of S * (S,U1)
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
(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
the ResultSort 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) Element of bool [: the carrier' of S, 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
the ResultSort of S * (S,U1) is non empty Relation-like non-empty non empty-yielding the carrier' of S -defined Function-like total set
MSAlgebra(# (S,U1),(S,U1) #) is strict MSAlgebra over S
(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
FG is Relation-like Function-like set
proj1 FG is set
fa is non empty Relation-like the carrier of S -defined Function-like total set
the Sorts of (S,U1) is non empty Relation-like non-empty non empty-yielding the carrier of S -defined Function-like total set
f is set
fa . f is set
the Sorts of (S,U1) . f is set
F is Element of the carrier of S
fa . F is set
(S,U1,F) is non empty Element of bool ((S,U1) . F)
(S,U1) . F is non empty set
bool ((S,U1) . F) is non empty set
f is non empty Relation-like the carrier of S -defined Function-like total ManySortedSubset of the Sorts of (S,U1)
GenMSAlg f is strict MSSubAlgebra of (S,U1)
the Sorts of (GenMSAlg f) is non empty Relation-like the carrier of S -defined Function-like total set
proj2 the Sorts of (GenMSAlg f) is non empty set
union (proj2 the Sorts of (GenMSAlg f)) 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 non empty functional V61() Element of bool K261( the carrier of (S,U1))
bool K261( the carrier of (S,U1)) is non empty set
s is Element of the carrier of (S,U1)
s0 is Relation-like K37() -defined K261( the carrier of (S,U1)) -valued Function-like V35() V48() V49() FinSequence-like FinSubsequence-like V64() FinSequence of TS (S,U1)
roots s0 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)
proj2 s0 is set
s -tree s0 is Relation-like the carrier of (S,U1) -valued Function-like DecoratedTree-like Element of K261( the carrier of (S,U1))
[s,(roots s0)] is V26() set
{s,(roots s0)} is non empty set
{s} is non empty set
{{s,(roots s0)},{s}} 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
g is Element of [: the carrier' of S,{ the carrier of S}:] \/ (Union ( the carrier of S,U1))
x 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))) *
[g,x] is V26() set
{g,x} is non empty set
{g} is non empty set
{{g,x},{g}} is non empty set
D is Element of the carrier' of S
t is Element of { the carrier of S}
[D,t] is V26() set
{D,t} is non empty set
{D} is non empty set
{{D,t},{D}} is non empty set
the_arity_of D is Relation-like K37() -defined the carrier of S -valued Function-like V35() FinSequence-like FinSubsequence-like Element of the carrier of S *
the_result_sort_of D is Element of the carrier of S
len x is V7() V8() V9() V13() Element of K37()
len (the_arity_of D) is V7() V8() V9() V13() Element of K37()
h is non empty Relation-like the carrier of S -defined Function-like total ManySortedSubset of the Sorts of (S,U1)
dom h is non empty Element of bool the carrier of S
bool the carrier of S is non empty set
dom (roots s0) is Element of bool K37()
dom s0 is Element of bool K37()
proj2 (the_arity_of D) is set
(the_arity_of D) * h is Relation-like K37() -defined Function-like set
dom ((the_arity_of D) * h) is Element of bool K37()
dom (the_arity_of D) is Element of bool K37()
Seg (len x) is V35() V42( len x) Element of bool K37()
dom x is Element of bool K37()
Seg (len (the_arity_of D)) is V35() V42( len (the_arity_of D)) Element of bool K37()
hf is set
s0 . hf is Relation-like Function-like set
((the_arity_of D) * h) . hf is set
x is V7() V8() V9() V13() set
s0 . x is Relation-like Function-like set
s is Relation-like the carrier of (S,U1) -valued Function-like DecoratedTree-like Element of TS (S,U1)
a is set
(the_arity_of D) /. x is Element of the carrier of S
U1 . ((the_arity_of D) /. x) is non empty set
{ b1 where b1 is Relation-like the carrier of (S,U1) -valued Function-like DecoratedTree-like Element of TS (S,U1) : ( ex b2 being set st
( b2 in U1 . ((the_arity_of D) /. x) & b1 = root-tree [b2,((the_arity_of D) /. x)] ) or ex b2 being Element of the carrier' of S st
( [b2, the carrier of S] = b1 . {} & the_result_sort_of b2 = (the_arity_of D) /. x ) ) } is set
(S,U1,((the_arity_of D) /. x)) is non empty functional V61() Element of bool (TS (S,U1))
bool (TS (S,U1)) is non empty set
(S,U1) . ((the_arity_of D) /. x) is non empty set
x . x is set
dom the Sorts of (GenMSAlg f) is non empty Element of bool the carrier of S
ar is set
the Sorts of (GenMSAlg f) . ar is set
proj2 x is set
rt is Element of the carrier' of S
a is Element of { the carrier of S}
[rt,a] is V26() set
{rt,a} is non empty set
{rt} is non empty set
{{rt,a},{rt}} is non empty set
the_result_sort_of rt is Element of the carrier of S
(the_arity_of D) . x is set
n is Relation-like Function-like DecoratedTree-like set
n . {} is set
(the_arity_of D) . x is set
( the carrier of S,U1,((the_arity_of D) . x)) is set
( the carrier of S,U1,((the_arity_of D) /. x)) is 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
rt is Element of Terminals (S,U1)
root-tree rt is Relation-like the carrier of (S,U1) -valued Function-like DecoratedTree-like Element of TS (S,U1)
a is Relation-like Function-like DecoratedTree-like set
a . {} is set
a is set
[a,((the_arity_of D) /. x)] is V26() set
{a,((the_arity_of D) /. x)} is non empty set
{a} is non empty set
{{a,((the_arity_of D) /. x)},{a}} is non empty set
p is Element of the carrier of S
(S,U1) . p is non empty set
the Sorts of (GenMSAlg f) . p is set
the Sorts of (S,U1) . p is non empty set
(the_arity_of D) . x is set
h . ((the_arity_of D) . x) is set
h . ((the_arity_of D) /. x) is set
h # is non empty Relation-like the carrier of S * -defined Function-like total set
the Arity of S * (h #) is non empty Relation-like the carrier' of S -defined Function-like total set
Den (D,(S,U1)) is non empty Relation-like Args (D,(S,U1)) -defined Result (D,(S,U1)) -valued Function-like total V29( Args (D,(S,U1)), Result (D,(S,U1))) Element of bool [:(Args (D,(S,U1))),(Result (D,(S,U1))):]
Args (D,(S,U1)) is non empty functional Element of proj2 ( the Sorts of (S,U1) #)
the Sorts of (S,U1) # is non empty Relation-like the carrier of S * -defined Function-like total set
proj2 ( the Sorts of (S,U1) #) is non empty set
Result (D,(S,U1)) is non empty Element of proj2 the Sorts of (S,U1)
proj2 the Sorts of (S,U1) is non empty set
[:(Args (D,(S,U1))),(Result (D,(S,U1))):] is non empty Relation-like set
bool [:(Args (D,(S,U1))),(Result (D,(S,U1))):] is non empty set
(S,U1) . D is Relation-like ( the Arity of S * ((S,U1) #)) . D -defined ( the ResultSort of S * (S,U1)) . D -valued Function-like total V29(( the Arity of S * ((S,U1) #)) . D,( the ResultSort of S * (S,U1)) . D) Element of bool [:(( the Arity of S * ((S,U1) #)) . D),(( the ResultSort of S * (S,U1)) . D):]
( the Arity of S * ((S,U1) #)) . D is set
( the ResultSort of S * (S,U1)) . D is non empty set
[:(( the Arity of S * ((S,U1) #)) . D),(( the ResultSort of S * (S,U1)) . D):] is Relation-like set
bool [:(( the Arity of S * ((S,U1) #)) . D),(( the ResultSort of S * (S,U1)) . D):] is non empty set
(S,U1,D) is Relation-like ( the Arity of S * ((S,U1) #)) . D -defined ( the ResultSort of S * (S,U1)) . D -valued Function-like total V29(( the Arity of S * ((S,U1) #)) . D,( the ResultSort of S * (S,U1)) . D) Element of bool [:(( the Arity of S * ((S,U1) #)) . D),(( the ResultSort of S * (S,U1)) . D):]
(S,U1,D) is Element of the carrier of (S,U1)
[D, the carrier of S] is V26() set
{D, the carrier of S} is non empty set
{{D, the carrier of S},{D}} is non empty set
the Arity of S . D is Relation-like K37() -defined Function-like V35() FinSequence-like FinSubsequence-like Element of the carrier of S *
( the Arity of S * (h #)) . D is set
product ((the_arity_of D) * h) is set
dom (S,U1,D) is Element of bool (( the Arity of S * ((S,U1) #)) . D)
bool (( the Arity of S * ((S,U1) #)) . D) is non empty set
(dom (S,U1,D)) /\ (( the Arity of S * (h #)) . D) is Element of bool (( the Arity of S * ((S,U1) #)) . D)
(S,U1,D) | (( the Arity of S * (h #)) . D) is Relation-like ( the Arity of S * ((S,U1) #)) . D -defined ( the Arity of S * (h #)) . D -defined ( the Arity of S * ((S,U1) #)) . D -defined ( the ResultSort of S * (S,U1)) . D -valued Function-like Element of bool [:(( the Arity of S * ((S,U1) #)) . D),(( the ResultSort of S * (S,U1)) . D):]
dom ((S,U1,D) | (( the Arity of S * (h #)) . D)) is Element of bool (( the Arity of S * (h #)) . D)
bool (( the Arity of S * (h #)) . D) is non empty set
((S,U1,D) | (( the Arity of S * (h #)) . D)) . s0 is set
(S,U1,D) . s0 is set
(Den (D,(S,U1))) | (( the Arity of S * (h #)) . D) is Relation-like Args (D,(S,U1)) -defined ( the Arity of S * (h #)) . D -defined Args (D,(S,U1)) -defined Result (D,(S,U1)) -valued Function-like Element of bool [:(Args (D,(S,U1))),(Result (D,(S,U1))):]
proj2 ((Den (D,(S,U1))) | (( the Arity of S * (h #)) . D)) is set
the ResultSort of S . D is Element of the carrier of S
the ResultSort of S * h is non empty Relation-like the carrier' of S -defined Function-like total set
dom ( the ResultSort of S * h) is non empty Element of bool the carrier' of S
bool the carrier' of S is non empty set
( the ResultSort of S * h) . D is set
h . (the_result_sort_of D) is set
proj2 h 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
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))
proj2 ( the carrier of S,U1) is non empty set
union (proj2 ( the carrier of S,U1)) is set
a 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
s is set
( the carrier of S,U1) . s is set
s0 is Element of the carrier of S
( the carrier of S,U1,s0) is set
U1 . s0 is non empty set
(S,U1,s0) is non empty Element of bool ((S,U1) . s0)
(S,U1) . s0 is non empty set
bool ((S,U1) . s0) is non empty set
g is set
[g,s0] is V26() set
{g,s0} is non empty set
{g} is non empty set
{{g,s0},{g}} is non empty set
f . s0 is set
the Sorts of (GenMSAlg f) . s0 is set
dom the Sorts of (GenMSAlg f) is non empty Element of bool the carrier of S
proj2 the Sorts of (S,U1) is non empty set
union (proj2 the Sorts of (S,U1)) is set
a is set
s is set
dom (S,U1) is non empty Element of bool the carrier of S
bool the carrier of S is non empty set
s0 is set
(S,U1) . s0 is set
g is Element of the carrier of S
(S,U1,g) is non empty functional V61() Element of bool (TS (S,U1))
bool (TS (S,U1)) is non empty set
U1 . g is non empty set
{ b1 where b1 is Relation-like the carrier of (S,U1) -valued Function-like DecoratedTree-like Element of TS (S,U1) : ( ex b2 being set st
( b2 in U1 . g & b1 = root-tree [b2,g] ) or ex b2 being Element of the carrier' of S st
( [b2, the carrier of S] = b1 . {} & the_result_sort_of b2 = g ) ) } is set
x is Relation-like the carrier of (S,U1) -valued Function-like DecoratedTree-like Element of TS (S,U1)
D is set
[D,g] is V26() set
{D,g} is non empty set
{D} is non empty set
{{D,g},{D}} is non empty set
root-tree [D,g] is Relation-like Function-like DecoratedTree-like set
t is Element of the carrier' of S
[t, the carrier of S] is V26() set
{t, the carrier of S} is non empty set
{t} is non empty set
{{t, the carrier of S},{t}} is non empty set
x . {} is set
the_result_sort_of t is Element of the carrier of S
F is Element of the carrier of S
the Sorts of (GenMSAlg f) . F is set
the Sorts of (S,U1) . F is non empty set
s is set
dom the Sorts of (S,U1) is non empty Element of bool the carrier of S
bool the carrier of S is non empty set
a is Element of the carrier of S
the Sorts of (S,U1) . a is non empty set
s0 is set
dom the Sorts of (GenMSAlg f) is non empty Element of bool the carrier of S
g is set
the Sorts of (GenMSAlg f) . g is set
x is Element of the carrier of S
(S,U1) . a is non empty set
(S,U1) . x is non empty set
((S,U1) . a) /\ ((S,U1) . x) is set
the Sorts of (GenMSAlg f) . x is set
the Sorts of (S,U1) . x is non empty set
F is non empty Relation-like the carrier of S -defined Function-like total (S,(S,U1))
a is Element of the carrier of S
F . a is set
(S,U1,a) is non empty Element of bool ((S,U1) . a)
(S,U1) . a is non empty set
bool ((S,U1) . a) is non empty set
U0 is non empty Relation-like the carrier of S -defined Function-like total (S,(S,U1))
F is non empty Relation-like the carrier of S -defined Function-like total (S,(S,U1))
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 Element of bool ((S,U1) . fa)
(S,U1) . fa is non empty set
bool ((S,U1) . fa) 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 Relation-like the carrier of S -defined Function-like total (S,(S,U1))
(S,U1) is strict non-empty MSAlgebra over S
(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 V48() V49() ManySortedFunction of the Arity of S * ((S,U1) #), the ResultSort of S * (S,U1)
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
(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
the ResultSort 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) Element of bool [: the carrier' of S, 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
the ResultSort of S * (S,U1) is non empty Relation-like non-empty non empty-yielding the carrier' of S -defined Function-like total set
MSAlgebra(# (S,U1),(S,U1) #) is strict MSAlgebra over S
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 Element of bool ((S,U1) . F)
(S,U1) . F is non empty set
bool ((S,U1) . F) 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 Relation-like the carrier of S -defined Function-like total (S,(S,U1))
(S,U1) is strict non-empty MSAlgebra over S
(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 V48() V49() ManySortedFunction of the Arity of S * ((S,U1) #), the ResultSort of S * (S,U1)
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
(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
the ResultSort 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) Element of bool [: the carrier' of S, 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
the ResultSort of S * (S,U1) is non empty Relation-like non-empty non empty-yielding the carrier' of S -defined Function-like total set
MSAlgebra(# (S,U1),(S,U1) #) is strict MSAlgebra over S
proj2 (S,U1) is non empty set
union (proj2 (S,U1)) is 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
Terminals (S,U1) is non empty Element of bool the carrier of (S,U1)
bool the carrier of (S,U1) is non empty set
{ (root-tree b1) where b1 is Element of the carrier of (S,U1) : b1 in Terminals (S,U1) } is set
fa is set
f is set
dom (S,U1) is non empty Element of bool the carrier of S
bool the carrier of S is non empty set
F is set
(S,U1) . F is set
a is Element of the carrier of S
(S,U1,a) is non empty Element of bool ((S,U1) . a)
(S,U1) . a is non empty set
bool ((S,U1) . a) is non empty set
{ (root-tree b1) where b1 is Element of the carrier of (S,U1) : ( b1 in Terminals (S,U1) & b1 `2 = a ) } is set
s is Element of the carrier of (S,U1)
root-tree s is Relation-like the carrier of (S,U1) -valued Function-like DecoratedTree-like Element of K261( the carrier of (S,U1))
K261( the carrier of (S,U1)) is non empty functional V61() M14( the carrier of (S,U1))
s `2 is set
fa 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))
K261( the carrier of (S,U1)) is non empty functional V61() M14( the carrier of (S,U1))
a is set
F is Element of the carrier of S
U1 . F is non empty set
[a,F] is V26() set
{a,F} is non empty set
{a} is non empty set
{{a,F},{a}} is non empty set
f `2 is set
{ (root-tree b1) where b1 is Element of the carrier of (S,U1) : ( b1 in Terminals (S,U1) & b1 `2 = F ) } is set
(S,U1,F) is non empty Element of bool ((S,U1) . F)
(S,U1) . F is non empty set
bool ((S,U1) . F) is non empty set
(S,U1) . F is set
dom (S,U1) is non empty Element of bool the carrier of S
bool the carrier of S is non empty set
S is non empty non void 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 non empty Element of bool ((S,U1) . U0)
(S,U1) is non empty Relation-like non-empty non empty-yielding the carrier of S -defined Function-like total set
(S,U1) . U0 is non empty set
bool ((S,U1) . U0) is non empty set
U1 . U0 is non empty set
[:(S,U1,U0),(U1 . U0):] is non empty Relation-like set
bool [:(S,U1,U0),(U1 . U0):] is non empty 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
fa is 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
{ (root-tree b1) where b1 is Element of the carrier of (S,U1) : ( b1 in Terminals (S,U1) & b1 `2 = U0 ) } 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))
K261( the carrier of (S,U1)) is non empty functional V61() M14( the carrier of (S,U1))
f `2 is set
a is set
F is Element of the carrier of S
U1 . F is non empty set
[a,F] is V26() set
{a,F} is non empty set
{a} is non empty set
{{a,F},{a}} is non empty set
s is Element of the carrier of (S,U1)
root-tree s is Relation-like the carrier of (S,U1) -valued Function-like DecoratedTree-like Element of K261( the carrier of (S,U1))
s `1 is set
fa is Relation-like Function-like set
proj1 fa is set
proj2 fa is set
f is non empty Relation-like (S,U1,U0) -defined U1 . U0 -valued Function-like total V29((S,U1,U0),U1 . U0) Element of bool [:(S,U1,U0),(U1 . U0):]
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))
K261( the carrier of (S,U1)) is non empty functional V61() M14( the carrier of (S,U1))
f . (root-tree F) is set
F `1 is 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
{ (root-tree b1) where b1 is Element of the carrier of (S,U1) : ( b1 in Terminals (S,U1) & b1 `2 = U0 ) } is set
fa is non empty Relation-like (S,U1,U0) -defined U1 . U0 -valued Function-like total V29((S,U1,U0),U1 . U0) Element of bool [:(S,U1,U0),(U1 . U0):]
f is non empty Relation-like (S,U1,U0) -defined U1 . U0 -valued Function-like total V29((S,U1,U0),U1 . U0) Element of bool [:(S,U1,U0),(U1 . U0):]
F is set
fa . F is set
f . F is set
a is Element of the carrier of (S,U1)
root-tree a is Relation-like the carrier of (S,U1) -valued Function-like DecoratedTree-like Element of K261( the carrier of (S,U1))
K261( the carrier of (S,U1)) is non empty functional V61() M14( the carrier of (S,U1))
a `2 is set
fa . (root-tree a) is set
a `1 is set
dom fa is non empty Element of bool (S,U1,U0)
bool (S,U1,U0) is non empty set
dom f is non empty Element of bool (S,U1,U0)
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 (S,(S,U1))
(S,U1) is strict non-empty MSAlgebra over S
(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 V48() V49() ManySortedFunction of the Arity of S * ((S,U1) #), the ResultSort of S * (S,U1)
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
(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
the ResultSort 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) Element of bool [: the carrier' of S, 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
the ResultSort of S * (S,U1) is non empty Relation-like non-empty non empty-yielding the carrier' of S -defined Function-like total set
MSAlgebra(# (S,U1),(S,U1) #) is strict MSAlgebra over S
FG is set
fa is Element of the carrier of S
(S,U1,fa) is non empty Relation-like (S,U1,fa) -defined U1 . fa -valued Function-like total V29((S,U1,fa),U1 . fa) Element of bool [:(S,U1,fa),(U1 . fa):]
(S,U1,fa) is non empty Element of bool ((S,U1) . fa)
(S,U1) . fa is non empty set
bool ((S,U1) . fa) is non empty set
U1 . fa is non empty set
[:(S,U1,fa),(U1 . fa):] is non empty Relation-like set
bool [:(S,U1,fa),(U1 . fa):] is non empty set
f is Element of the carrier of S
(S,U1,f) is non empty Relation-like (S,U1,f) -defined U1 . f -valued Function-like total V29((S,U1,f),U1 . f) Element of bool [:(S,U1,f),(U1 . f):]
(S,U1,f) is non empty Element of bool ((S,U1) . f)
(S,U1) . f is non empty set
bool ((S,U1) . f) is non empty set
U1 . f is non empty set
[:(S,U1,f),(U1 . f):] is non empty Relation-like set
bool [:(S,U1,f),(U1 . f):] is non empty set
FG is Relation-like Function-like set
proj1 FG is set
fa is non empty Relation-like the carrier of S -defined Function-like total set
dom fa is non empty Element of bool the carrier of S
bool the carrier of S is non empty set
f is set
fa . f is set
F is Element of the carrier of S
fa . F is set
(S,U1,F) is non empty Relation-like (S,U1,F) -defined U1 . F -valued Function-like total V29((S,U1,F),U1 . F) Element of bool [:(S,U1,F),(U1 . F):]
(S,U1,F) is non empty Element of bool ((S,U1) . F)
(S,U1) . F is non empty set
bool ((S,U1) . F) is non empty set
U1 . F is non empty set
[:(S,U1,F),(U1 . F):] is non empty Relation-like set
bool [:(S,U1,F),(U1 . F):] is non empty set
f is non empty Relation-like the carrier of S -defined Function-like total V48() V49() set
F is set
f . F is Relation-like Function-like set
(S,U1) . F is set
U1 . F is set
[:((S,U1) . F),(U1 . F):] is Relation-like set
bool [:((S,U1) . F),(U1 . F):] is non empty set
a is Element of the carrier of S
(S,U1) . a is set
(S,U1,a) is non empty Element of bool ((S,U1) . a)
(S,U1) . a is non empty set
bool ((S,U1) . a) is non empty set
(S,U1,a) is non empty Relation-like (S,U1,a) -defined U1 . a -valued Function-like total V29((S,U1,a),U1 . a) Element of bool [:(S,U1,a),(U1 . a):]
U1 . a is non empty set
[:(S,U1,a),(U1 . a):] is non empty Relation-like set
bool [:(S,U1,a),(U1 . a):] is non empty set
F is non empty Relation-like the carrier of S -defined Function-like total V48() V49() ManySortedFunction of (S,U1),U1
a is Element of the carrier of S
(S,U1) . a is set
U1 . a is non empty set
(S,U1,a) is non empty Element of bool ((S,U1) . a)
(S,U1) . a is non empty set
bool ((S,U1) . a) is non empty set
F . a is Relation-like (S,U1) . a -defined U1 . a -valued Function-like total V29((S,U1) . a,U1 . a) Element of bool [:((S,U1) . a),(U1 . a):]
[:((S,U1) . a),(U1 . a):] is Relation-like set
bool [:((S,U1) . a),(U1 . a):] is non empty set
(S,U1,a) is non empty Relation-like (S,U1,a) -defined U1 . a -valued Function-like total V29((S,U1,a),U1 . a) Element of bool [:(S,U1,a),(U1 . a):]
[:(S,U1,a),(U1 . a):] is non empty Relation-like set
bool [:(S,U1,a),(U1 . a):] is non empty set
U0 is non empty Relation-like the carrier of S -defined Function-like total V48() V49() ManySortedFunction of (S,U1),U1
F is non empty Relation-like the carrier of S -defined Function-like total V48() V49() ManySortedFunction of (S,U1),U1
FG is set
U0 . FG is Relation-like Function-like set
F . FG is Relation-like Function-like set
fa is Element of the carrier of S
(S,U1) . fa is set
U1 . fa is non empty set
(S,U1,fa) is non empty Element of bool ((S,U1) . fa)
(S,U1) . fa is non empty set
bool ((S,U1) . fa) is non empty set
U0 . fa is Relation-like (S,U1) . fa -defined U1 . fa -valued Function-like total V29((S,U1) . fa,U1 . fa) Element of bool [:((S,U1) . fa),(U1 . fa):]
[:((S,U1) . fa),(U1 . fa):] is Relation-like set
bool [:((S,U1) . fa),(U1 . fa):] is non empty set
(S,U1,fa) is non empty Relation-like (S,U1,fa) -defined U1 . fa -valued Function-like total V29((S,U1,fa),U1 . fa) Element of bool [:(S,U1,fa),(U1 . fa):]
[:(S,U1,fa),(U1 . fa):] is non empty Relation-like set
bool [:(S,U1,fa),(U1 . fa):] 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 Relation-like the carrier of S -defined Function-like total (S,(S,U1))
(S,U1) is strict non-empty MSAlgebra over S
(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 V48() V49() ManySortedFunction of the Arity of S * ((S,U1) #), the ResultSort of S * (S,U1)
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
(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
the ResultSort 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) Element of bool [: the carrier' of S, 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
the ResultSort of S * (S,U1) is non empty Relation-like non-empty non empty-yielding the carrier' of S -defined Function-like total set
MSAlgebra(# (S,U1),(S,U1) #) is strict MSAlgebra over S
U0 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
FG is Element of the carrier of (S,U1)
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 U0 is non empty set
F is non empty Relation-like the carrier of S -defined Function-like total V48() V49() ManySortedFunction of (S,U1),U0
FG `2 is set
F . (FG `2) is Relation-like Function-like set
root-tree FG is Relation-like the carrier of (S,U1) -valued Function-like DecoratedTree-like Element of K261( the carrier of (S,U1))
K261( the carrier of (S,U1)) is non empty functional V61() M14( the carrier of (S,U1))
a is set
F is Element of the carrier of S
U1 . F is non empty set
[a,F] is V26() set
{a,F} is non empty set
{a} is non empty set
{{a,F},{a}} is non empty set
(S,U1) . F is set
(S,U1,F) is non empty Element of bool ((S,U1) . F)
(S,U1) . F is non empty set
bool ((S,U1) . F) is non empty set
F . F is Relation-like (S,U1) . F -defined U0 . F -valued Function-like total V29((S,U1) . F,U0 . F) Element of bool [:((S,U1) . F),(U0 . F):]
U0 . F is non empty set
[:((S,U1) . F),(U0 . F):] is Relation-like set
bool [:((S,U1) . F),(U0 . F):] is non empty set
dom (F . F) is Element of bool ((S,U1) . F)
bool ((S,U1) . F) is non empty set
{ (root-tree b1) where b1 is Element of the carrier of (S,U1) : ( b1 in Terminals (S,U1) & b1 `2 = F ) } is set
(F . F) . (root-tree FG) is set
proj2 (F . F) is set
dom U0 is non empty Element of bool the carrier of S
bool the carrier of S is non empty set
proj2 U0 is non empty set
union (proj2 U0) is set
s is Element of Union U0
s0 is Relation-like Function-like set
s0 . (root-tree FG) is set
f is set
fa is Element of the carrier of S
U1 . fa is non empty set
[f,fa] is V26() set
{f,fa} is non empty set
{f} is non empty set
{{f,fa},{f}} is non empty set
F . fa is Relation-like (S,U1) . fa -defined U0 . fa -valued Function-like total V29((S,U1) . fa,U0 . fa) Element of bool [:((S,U1) . fa),(U0 . fa):]
(S,U1) . fa is set
U0 . fa is non empty set
[:((S,U1) . fa),(U0 . fa):] is Relation-like set
bool [:((S,U1) . fa),(U0 . fa):] is non empty set
a is Element of Union U0
s is Element of Union U0
F is Relation-like Function-like set
F . (root-tree 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 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
U0 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
[U0,f] is V26() set
{U0,f} is non empty set
{U0} is non empty set
{{U0,f},{U0}} 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
fa 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))) *
[fa,F] is V26() set
{fa,F} is non empty set
{fa} is non empty set
{{fa,F},{fa}} is non empty set
a is Element of the carrier' of S
s is Element of { the carrier of S}
[a,s] is V26() set
{a,s} is non empty set
{a} is non empty set
{{a,s},{a}} is non empty set
[a, the carrier of S] is V26() set
{a, the carrier of S} is non empty set
{{a, the carrier of S},{a}} is non empty 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
FG is Element of the carrier' of S
[FG, the carrier of S] is V26() set
{FG, the carrier of S} is non empty set
{FG} is non empty set
{{FG, the carrier of S},{FG}} is non empty set
S is non empty non void V78() ManySortedSign
the carrier' of S is non empty set
F is Relation-like K37() -defined Function-like V35() FinSequence-like FinSubsequence-like set
U0 is Element of the carrier' of S
U1 is non-empty MSAlgebra over S
Args (U0,U1) is non empty functional Element of proj2 ( the Sorts of U1 #)
the carrier of S is non empty set
the Sorts of U1 is non empty Relation-like non-empty non empty-yielding the carrier of S -defined Function-like total set
the Sorts of U1 # is non empty Relation-like the carrier of S * -defined Function-like total set
the carrier of S * is non empty functional FinSequence-membered M19( the carrier of S)
proj2 ( the Sorts of U1 #) is non empty set
Den (U0,U1) is non empty Relation-like Args (U0,U1) -defined Result (U0,U1) -valued Function-like total V29( Args (U0,U1), Result (U0,U1)) Element of bool [:(Args (U0,U1)),(Result (U0,U1)):]
Result (U0,U1) is non empty Element of proj2 the Sorts of U1
proj2 the Sorts of U1 is non empty set
[:(Args (U0,U1)),(Result (U0,U1)):] is non empty Relation-like set
bool [:(Args (U0,U1)),(Result (U0,U1)):] is non empty set
(Den (U0,U1)) . F is set
Union the Sorts of U1 is non empty set
dom (Den (U0,U1)) is non empty functional Element of bool (Args (U0,U1))
bool (Args (U0,U1)) is non empty set
proj2 (Den (U0,U1)) is non empty set
union (proj2 the Sorts of U1) 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 strict non-empty MSAlgebra over S
(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 V48() V49() ManySortedFunction of the Arity of S * ((S,U1) #), the ResultSort of S * (S,U1)
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
(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
the ResultSort 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) Element of bool [: the carrier' of S, 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
the ResultSort of S * (S,U1) is non empty Relation-like non-empty non empty-yielding the carrier' of S -defined Function-like total set
MSAlgebra(# (S,U1),(S,U1) #) is strict MSAlgebra over S
(S,U1) is non empty Relation-like the carrier of S -defined Function-like total (S,(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,{ 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
fa is non-empty MSAlgebra over S
the Sorts of fa is non empty Relation-like non-empty non empty-yielding the carrier of S -defined Function-like total set
the Sorts of (S,U1) is non empty Relation-like non-empty non empty-yielding the carrier of S -defined Function-like total set
f is non empty Relation-like the carrier of S -defined Function-like total V48() V49() ManySortedFunction of (S,U1), the Sorts of fa
Union the Sorts of fa is non empty set
the carrier of (S,U1) is non empty set
TS (S,U1) is non empty functional V61() Element of bool K261( the carrier of (S,U1))
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
[:(TS (S,U1)),(Union the Sorts of fa):] is non empty Relation-like set
bool [:(TS (S,U1)),(Union the Sorts of fa):] 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
D is non empty Relation-like TS (S,U1) -defined Union the Sorts of fa -valued Function-like total V29( TS (S,U1), Union the Sorts of fa) Element of bool [:(TS (S,U1)),(Union the Sorts of fa):]
t is Relation-like Function-like set
proj1 t is set
t is non empty Relation-like the carrier of S -defined Function-like total set
dom t is non empty Element of bool the carrier of S
bool the carrier of S is non empty set
h is set
t . h is set
the Sorts of (S,U1) . h is set
D | ( the Sorts of (S,U1) . h) is Relation-like TS (S,U1) -defined the Sorts of (S,U1) . h -defined TS (S,U1) -defined Union the Sorts of fa -valued Function-like Element of bool [:(TS (S,U1)),(Union the Sorts of fa):]
h is non empty Relation-like the carrier of S -defined Function-like total V48() V49() set
h is Element of the carrier of (S,U1)
hf is Relation-like K37() -defined K261( the carrier of (S,U1)) -valued Function-like V35() V48() V49() FinSequence-like FinSubsequence-like V64() FinSequence of TS (S,U1)
roots hf 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)
proj2 hf is set
h -tree hf is Relation-like the carrier of (S,U1) -valued Function-like DecoratedTree-like Element of K261( the carrier of (S,U1))
D * hf is Relation-like K37() -defined Union the Sorts of fa -valued Function-like V35() FinSequence-like FinSubsequence-like Element of (Union the Sorts of fa) *
(Union the Sorts of fa) * is non empty functional FinSequence-membered M19( Union the Sorts of fa)
(S,U1,h) is Element of the carrier' of S
the_arity_of (S,U1,h) is Relation-like K37() -defined the carrier of S -valued Function-like V35() FinSequence-like FinSubsequence-like Element of the carrier of S *
the_result_sort_of (S,U1,h) is Element of the carrier of S
[(S,U1,h), the carrier of S] is V26() set
{(S,U1,h), the carrier of S} is non empty set
{(S,U1,h)} is non empty set
{{(S,U1,h), the carrier of S},{(S,U1,h)}} is non empty set
[[(S,U1,h), the carrier of S],(roots hf)] is V26() set
{[(S,U1,h), the carrier of S],(roots hf)} is non empty set
{[(S,U1,h), the carrier of S]} is non empty Relation-like Function-like set
{{[(S,U1,h), the carrier of S],(roots hf)},{[(S,U1,h), the carrier of S]}} 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
(S,U1,(S,U1,h)) is Element of the carrier of (S,U1)
(S,U1,(S,U1,h)) is Relation-like ( the Arity of S * ((S,U1) #)) . (S,U1,h) -defined ( the ResultSort of S * (S,U1)) . (S,U1,h) -valued Function-like total V29(( the Arity of S * ((S,U1) #)) . (S,U1,h),( the ResultSort of S * (S,U1)) . (S,U1,h)) Element of bool [:(( the Arity of S * ((S,U1) #)) . (S,U1,h)),(( the ResultSort of S * (S,U1)) . (S,U1,h)):]
( the Arity of S * ((S,U1) #)) . (S,U1,h) is set
( the ResultSort of S * (S,U1)) . (S,U1,h) is non empty set
[:(( the Arity of S * ((S,U1) #)) . (S,U1,h)),(( the ResultSort of S * (S,U1)) . (S,U1,h)):] is Relation-like set
bool [:(( the Arity of S * ((S,U1) #)) . (S,U1,h)),(( the ResultSort of S * (S,U1)) . (S,U1,h)):] is non empty set
(S,U1,(S,U1,h)) . hf is set
dom (S,U1,(S,U1,h)) is Element of bool (( the Arity of S * ((S,U1) #)) . (S,U1,h))
bool (( the Arity of S * ((S,U1) #)) . (S,U1,h)) is non empty set
proj2 (S,U1,(S,U1,h)) is set
the ResultSort of S * the Sorts of (S,U1) is non empty Relation-like non-empty non empty-yielding the carrier' of S -defined Function-like total set
( the ResultSort of S * the Sorts of (S,U1)) . (S,U1,h) is non empty set
(S,fa,(S,U1,h),(D * hf)) is Element of Union the Sorts of fa
proj2 the ResultSort of S is non empty set
proj2 (the_arity_of (S,U1,h)) is set
rt 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))) *
len rt is V7() V8() V9() V13() Element of K37()
len (the_arity_of (S,U1,h)) is V7() V8() V9() V13() Element of K37()
dom rt is Element of bool K37()
Seg (len rt) is V35() V42( len rt) Element of bool K37()
dom the Sorts of (S,U1) is non empty Element of bool the carrier of S
(the_arity_of (S,U1,h)) * the Sorts of (S,U1) is Relation-like non-empty K37() -defined Function-like set
dom ((the_arity_of (S,U1,h)) * the Sorts of (S,U1)) is Element of bool K37()
dom (the_arity_of (S,U1,h)) is Element of bool K37()
the Arity of S . (S,U1,h) is Relation-like K37() -defined Function-like V35() FinSequence-like FinSubsequence-like Element of the carrier of S *
dom the Sorts of fa is non empty Element of bool the carrier of S
(the_arity_of (S,U1,h)) * the Sorts of fa is Relation-like non-empty K37() -defined Function-like set
dom ((the_arity_of (S,U1,h)) * the Sorts of fa) is Element of bool K37()
dom hf is Element of bool K37()
Seg (len (the_arity_of (S,U1,h))) is V35() V42( len (the_arity_of (S,U1,h))) Element of bool K37()
dom (D * hf) is Element of bool K37()
a is set
(D * hf) . a is set
((the_arity_of (S,U1,h)) * the Sorts of fa) . a is set
n is V7() V8() V9() V13() set
hf . n is Relation-like Function-like set
(D * hf) . n is set
D . (hf . n) is set
(the_arity_of (S,U1,h)) . a is set
s is Element of the carrier of S
h . s is Relation-like Function-like set
the Sorts of (S,U1) . s is non empty set
D | ( the Sorts of (S,U1) . s) is Relation-like TS (S,U1) -defined the Sorts of (S,U1) . s -defined TS (S,U1) -defined Union the Sorts of fa -valued Function-like Element of bool [:(TS (S,U1)),(Union the Sorts of fa):]
proj2 the Sorts of (S,U1) is non empty set
dom D is non empty functional V61() Element of bool (TS (S,U1))
bool (TS (S,U1)) is non empty set
union (proj2 the Sorts of (S,U1)) is set
proj1 (h . s) is set
(the_arity_of (S,U1,h)) * (S,U1) is Relation-like non-empty K37() -defined Function-like set
product ((the_arity_of (S,U1,h)) * (S,U1)) is set
hf . a is Relation-like Function-like set
((the_arity_of (S,U1,h)) * (S,U1)) . a is set
(S,U1) . ((the_arity_of (S,U1,h)) . a) is set
rt is Relation-like the carrier of (S,U1) -valued Function-like DecoratedTree-like Element of TS (S,U1)
(h . s) . rt is set
the Sorts of fa . s is non empty set
D . rt is Element of Union the Sorts of fa
the ResultSort of S * the Sorts of fa is non empty Relation-like non-empty non empty-yielding the carrier' of S -defined Function-like total set
dom ( the ResultSort of S * the Sorts of fa) is non empty Element of bool the carrier' of S
bool the carrier' of S is non empty set
dom the ResultSort of S is non empty Element of bool the carrier' of S
a is Element of the carrier of S
the Sorts of (S,U1) . a is non empty set
h . a is Relation-like Function-like set
(h . a) . (h -tree hf) is set
the Sorts of fa . a is non empty set
Args ((S,U1,h),fa) is non empty functional Element of proj2 ( the Sorts of fa #)
the Sorts of fa # is non empty Relation-like the carrier of S * -defined Function-like total set
proj2 ( the Sorts of fa #) is non empty set
Den ((S,U1,h),fa) is non empty Relation-like Args ((S,U1,h),fa) -defined Result ((S,U1,h),fa) -valued Function-like total V29( Args ((S,U1,h),fa), Result ((S,U1,h),fa)) Element of bool [:(Args ((S,U1,h),fa)),(Result ((S,U1,h),fa)):]
Result ((S,U1,h),fa) is non empty Element of proj2 the Sorts of fa
proj2 the Sorts of fa is non empty set
[:(Args ((S,U1,h),fa)),(Result ((S,U1,h),fa)):] is non empty Relation-like set
bool [:(Args ((S,U1,h),fa)),(Result ((S,U1,h),fa)):] is non empty set
dom (Den ((S,U1,h),fa)) is non empty functional Element of bool (Args ((S,U1,h),fa))
bool (Args ((S,U1,h),fa)) is non empty set
dom ( the ResultSort of S * the Sorts of (S,U1)) is non empty Element of bool the carrier' of S
the ResultSort of S . (S,U1,h) is Element of the carrier of S
the Sorts of (S,U1) . ( the ResultSort of S . (S,U1,h)) is non empty set
the Sorts of (S,U1) . (the_result_sort_of (S,U1,h)) is non empty set
the Arity of S * ( the Sorts of fa #) is non empty Relation-like the carrier' of S -defined Function-like total set
( the Arity of S * ( the Sorts of fa #)) . (S,U1,h) is set
product ((the_arity_of (S,U1,h)) * the Sorts of fa) is set
(Den ((S,U1,h),fa)) . (D * hf) is set
proj2 (Den ((S,U1,h),fa)) is non empty set
(S,U1) . (the_result_sort_of (S,U1,h)) is non empty set
(S,U1) . a is non empty set
D . (h -tree hf) is set
D | ( the Sorts of (S,U1) . (the_result_sort_of (S,U1,h))) is Relation-like TS (S,U1) -defined the Sorts of (S,U1) . (the_result_sort_of (S,U1,h)) -defined TS (S,U1) -defined Union the Sorts of fa -valued Function-like Element of bool [:(TS (S,U1)),(Union the Sorts of fa):]
(D | ( the Sorts of (S,U1) . (the_result_sort_of (S,U1,h)))) . (h -tree hf) is set
( the ResultSort of S * the Sorts of fa) . (S,U1,h) is non empty set
the Sorts of fa . ( the ResultSort of S . (S,U1,h)) is non empty set
the Sorts of fa . (the_result_sort_of (S,U1,h)) is non empty set
h is Element of the carrier of (S,U1)
root-tree h is Relation-like the carrier of (S,U1) -valued Function-like DecoratedTree-like Element of K261( the carrier of (S,U1))
x is set
hf is Element of the carrier of S
U1 . hf is non empty set
[x,hf] is V26() set
{x,hf} is non empty set
{x} is non empty set
{{x,hf},{x}} is non empty set
{ (root-tree b1) where b1 is Element of the carrier of (S,U1) : ( b1 in Terminals (S,U1) & b1 `2 = hf ) } is set
h `2 is set
t is Element of the carrier of S
the Sorts of (S,U1) . t is non empty set
h . t is Relation-like Function-like set
(h . t) . (root-tree h) is set
the Sorts of fa . t is non empty set
(S,U1) . hf is set
the Sorts of fa . hf is non empty set
[:((S,U1) . hf),( the Sorts of fa . hf):] is Relation-like set
bool [:((S,U1) . hf),( the Sorts of fa . hf):] is non empty set
f . hf is Relation-like (S,U1) . hf -defined the Sorts of fa . hf -valued Function-like total V29((S,U1) . hf, the Sorts of fa . hf) Element of bool [:((S,U1) . hf),( the Sorts of fa . hf):]
OU is Relation-like (S,U1) . hf -defined the Sorts of fa . hf -valued Function-like total V29((S,U1) . hf, the Sorts of fa . hf) Element of bool [:((S,U1) . hf),( the Sorts of fa . hf):]
dom OU is Element of bool ((S,U1) . hf)
bool ((S,U1) . hf) is non empty set
(S,U1,hf) is non empty Element of bool ((S,U1) . hf)
(S,U1) . hf is non empty set
bool ((S,U1) . hf) is non empty set
proj2 OU is set
OU . (root-tree h) is set
(S,U1) . t is non empty set
((S,U1) . hf) /\ ((S,U1) . t) is set
h . hf is Relation-like Function-like set
the Sorts of (S,U1) . hf is non empty set
D | ( the Sorts of (S,U1) . hf) is Relation-like TS (S,U1) -defined the Sorts of (S,U1) . hf -defined TS (S,U1) -defined Union the Sorts of fa -valued Function-like Element of bool [:(TS (S,U1)),(Union the Sorts of fa):]
(h . hf) . (root-tree h) is set
D . (root-tree h) is set
(S,U1, the Sorts of fa,f,h) is Element of Union the Sorts of fa
h is set
h . h is Relation-like Function-like set
the Sorts of (S,U1) . h is set
the Sorts of fa . h is set
[:( the Sorts of (S,U1) . h),( the Sorts of fa . h):] is Relation-like set
bool [:( the Sorts of (S,U1) . h),( the Sorts of fa . h):] is non empty set
dom D is non empty functional V61() Element of bool (TS (S,U1))
bool (TS (S,U1)) is non empty set
proj2 the Sorts of (S,U1) is non empty set
union (proj2 the Sorts of (S,U1)) is set
dom the Sorts of (S,U1) is non empty Element of bool the carrier of S
hf is Element of the carrier of S
the Sorts of (S,U1) . hf is non empty set
h . hf is Relation-like Function-like set
D | ( the Sorts of (S,U1) . hf) is Relation-like TS (S,U1) -defined the Sorts of (S,U1) . hf -defined TS (S,U1) -defined Union the Sorts of fa -valued Function-like Element of bool [:(TS (S,U1)),(Union the Sorts of fa):]
proj1 (h . hf) is set
proj2 (h . hf) is set
the Sorts of fa . hf is non empty set
x is set
s is set
(h . hf) . s is set
a is Relation-like the carrier of (S,U1) -valued Function-like DecoratedTree-like Element of TS (S,U1)
h is non empty Relation-like the carrier of S -defined Function-like total V48() V49() ManySortedFunction of the Sorts of (S,U1), the Sorts of fa
( the carrier of S, the Sorts of (S,U1), the Sorts of fa,(S,U1),h) is non empty Relation-like the carrier of S -defined Function-like total V48() V49() ManySortedFunction of (S,U1), the Sorts of fa
proj2 the ResultSort of S is non empty set
dom the Sorts of (S,U1) is non empty Element of bool the carrier of S
dom the ResultSort of S is non empty Element of bool the carrier' of S
bool the carrier' of S is non empty set
the ResultSort of S * the Sorts of (S,U1) is non empty Relation-like non-empty non empty-yielding the carrier' of S -defined Function-like total set
dom ( the ResultSort of S * the Sorts of (S,U1)) is non empty Element of bool the carrier' of S
hf is Element of the carrier' of S
Args (hf,(S,U1)) is non empty functional Element of proj2 ( the Sorts of (S,U1) #)
the Sorts of (S,U1) # is non empty Relation-like the carrier of S * -defined Function-like total set
proj2 ( the Sorts of (S,U1) #) is non empty set
the_result_sort_of hf is Element of the carrier of S
h . (the_result_sort_of hf) is non empty Relation-like the Sorts of (S,U1) . (the_result_sort_of hf) -defined the Sorts of fa . (the_result_sort_of hf) -valued Function-like total V29( the Sorts of (S,U1) . (the_result_sort_of hf), the Sorts of fa . (the_result_sort_of hf)) Element of bool [:( the Sorts of (S,U1) . (the_result_sort_of hf)),( the Sorts of fa . (the_result_sort_of hf)):]
the Sorts of (S,U1) . (the_result_sort_of hf) is non empty set
the Sorts of fa . (the_result_sort_of hf) is non empty set
[:( the Sorts of (S,U1) . (the_result_sort_of hf)),( the Sorts of fa . (the_result_sort_of hf)):] is non empty Relation-like set
bool [:( the Sorts of (S,U1) . (the_result_sort_of hf)),( the Sorts of fa . (the_result_sort_of hf)):] is non empty set
Den (hf,(S,U1)) is non empty Relation-like Args (hf,(S,U1)) -defined Result (hf,(S,U1)) -valued Function-like total V29( Args (hf,(S,U1)), Result (hf,(S,U1))) Element of bool [:(Args (hf,(S,U1))),(Result (hf,(S,U1))):]
Result (hf,(S,U1)) is non empty Element of proj2 the Sorts of (S,U1)
proj2 the Sorts of (S,U1) is non empty set
[:(Args (hf,(S,U1))),(Result (hf,(S,U1))):] is non empty Relation-like set
bool [:(Args (hf,(S,U1))),(Result (hf,(S,U1))):] is non empty set
Den (hf,fa) is non empty Relation-like Args (hf,fa) -defined Result (hf,fa) -valued Function-like total V29( Args (hf,fa), Result (hf,fa)) Element of bool [:(Args (hf,fa)),(Result (hf,fa)):]
Args (hf,fa) is non empty functional Element of proj2 ( the Sorts of fa #)
the Sorts of fa # is non empty Relation-like the carrier of S * -defined Function-like total set
proj2 ( the Sorts of fa #) is non empty set
Result (hf,fa) is non empty Element of proj2 the Sorts of fa
proj2 the Sorts of fa is non empty set
[:(Args (hf,fa)),(Result (hf,fa)):] is non empty Relation-like set
bool [:(Args (hf,fa)),(Result (hf,fa)):] is non empty set
x is Relation-like Function-like Element of Args (hf,(S,U1))
(Den (hf,(S,U1))) . x is set
(h . (the_result_sort_of hf)) . ((Den (hf,(S,U1))) . x) is set
h # x is Relation-like Function-like Element of Args (hf,fa)
(Den (hf,fa)) . (h # x) is set
the_arity_of hf is Relation-like K37() -defined the carrier of S -valued Function-like V35() FinSequence-like FinSubsequence-like Element of the carrier of S *
the Arity of S . hf is Relation-like K37() -defined Function-like V35() FinSequence-like FinSubsequence-like Element of the carrier of S *
( the Arity of S * ((S,U1) #)) . hf is set
(S,U1,hf) is Element of the carrier of (S,U1)
[hf, the carrier of S] is V26() set
{hf, the carrier of S} is non empty set
{hf} is non empty set
{{hf, the carrier of S},{hf}} is non empty set
p is Relation-like K37() -defined K261( the carrier of (S,U1)) -valued Function-like V35() V48() V49() FinSequence-like FinSubsequence-like V64() FinSequence of TS (S,U1)
roots p 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)
(S,U1,(S,U1,hf)) is Element of the carrier' of S
D * p is Relation-like K37() -defined Union the Sorts of fa -valued Function-like V35() FinSequence-like FinSubsequence-like Element of (Union the Sorts of fa) *
(Union the Sorts of fa) * is non empty functional FinSequence-membered M19( Union the Sorts of fa)
dom (D * p) is Element of bool K37()
dom p is Element of bool K37()
proj2 (the_arity_of hf) is set
(the_arity_of hf) * the Sorts of (S,U1) is Relation-like non-empty K37() -defined Function-like set
dom ((the_arity_of hf) * the Sorts of (S,U1)) is Element of bool K37()
dom (the_arity_of hf) is Element of bool K37()
a is set
(D * p) . a is set
(h # x) . a is set
[[hf, the carrier of S],(roots p)] is V26() set
{[hf, the carrier of S],(roots p)} is non empty set
{[hf, the carrier of S]} is non empty Relation-like Function-like set
{{[hf, the carrier of S],(roots p)},{[hf, the carrier of S]}} 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
rt 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))) *
len rt is V7() V8() V9() V13() Element of K37()
len (the_arity_of hf) is V7() V8() V9() V13() Element of K37()
n is V7() V8() V9() V13() set
(D * p) . n is set
x . n is set
D . (x . n) is set
(h # x) . n is set
(the_arity_of hf) /. n is Element of the carrier of S
h . ((the_arity_of hf) /. n) is non empty Relation-like the Sorts of (S,U1) . ((the_arity_of hf) /. n) -defined the Sorts of fa . ((the_arity_of hf) /. n) -valued Function-like total V29( the Sorts of (S,U1) . ((the_arity_of hf) /. n), the Sorts of fa . ((the_arity_of hf) /. n)) Element of bool [:( the Sorts of (S,U1) . ((the_arity_of hf) /. n)),( the Sorts of fa . ((the_arity_of hf) /. n)):]
the Sorts of (S,U1) . ((the_arity_of hf) /. n) is non empty set
the Sorts of fa . ((the_arity_of hf) /. n) is non empty set
[:( the Sorts of (S,U1) . ((the_arity_of hf) /. n)),( the Sorts of fa . ((the_arity_of hf) /. n)):] is non empty Relation-like set
bool [:( the Sorts of (S,U1) . ((the_arity_of hf) /. n)),( the Sorts of fa . ((the_arity_of hf) /. n)):] is non empty set
(h . ((the_arity_of hf) /. n)) . (x . n) is set
D | ( the Sorts of (S,U1) . ((the_arity_of hf) /. n)) is Relation-like TS (S,U1) -defined the Sorts of (S,U1) . ((the_arity_of hf) /. n) -defined TS (S,U1) -defined Union the Sorts of fa -valued Function-like Element of bool [:(TS (S,U1)),(Union the Sorts of fa):]
Seg (len rt) is V35() V42( len rt) Element of bool K37()
dom rt is Element of bool K37()
Seg (len (the_arity_of hf)) is V35() V42( len (the_arity_of hf)) Element of bool K37()
(the_arity_of hf) * (S,U1) is Relation-like non-empty K37() -defined Function-like set
product ((the_arity_of hf) * (S,U1)) is set
p . n is Relation-like Function-like set
((the_arity_of hf) * (S,U1)) . n is set
(the_arity_of hf) . n is set
the Sorts of (S,U1) . ((the_arity_of hf) . n) is set
proj1 (h # x) is set
dom (the_arity_of hf) is Element of bool K37()
D | ( the Sorts of (S,U1) . (the_result_sort_of hf)) is Relation-like TS (S,U1) -defined the Sorts of (S,U1) . (the_result_sort_of hf) -defined TS (S,U1) -defined Union the Sorts of fa -valued Function-like Element of bool [:(TS (S,U1)),(Union the Sorts of fa):]
(S,U1,hf) is Relation-like ( the Arity of S * ((S,U1) #)) . hf -defined ( the ResultSort of S * (S,U1)) . hf -valued Function-like total V29(( the Arity of S * ((S,U1) #)) . hf,( the ResultSort of S * (S,U1)) . hf) Element of bool [:(( the Arity of S * ((S,U1) #)) . hf),(( the ResultSort of S * (S,U1)) . hf):]
( the ResultSort of S * (S,U1)) . hf is non empty set
[:(( the Arity of S * ((S,U1) #)) . hf),(( the ResultSort of S * (S,U1)) . hf):] is Relation-like set
bool [:(( the Arity of S * ((S,U1) #)) . hf),(( the ResultSort of S * (S,U1)) . hf):] is non empty set
dom (S,U1,hf) is Element of bool (( the Arity of S * ((S,U1) #)) . hf)
bool (( the Arity of S * ((S,U1) #)) . hf) is non empty set
(S,U1,hf) . p is set
(S,U1,hf) -tree p is Relation-like the carrier of (S,U1) -valued Function-like DecoratedTree-like Element of K261( the carrier of (S,U1))
proj2 (S,U1,hf) is set
( the ResultSort of S * the Sorts of (S,U1)) . hf is non empty set
the ResultSort of S . hf is Element of the carrier of S
the Sorts of (S,U1) . ( the ResultSort of S . hf) is non empty set
dom D is non empty functional V61() Element of bool (TS (S,U1))
bool (TS (S,U1)) is non empty set
union (proj2 the Sorts of (S,U1)) is set
dom (h . (the_result_sort_of hf)) is non empty Element of bool ( the Sorts of (S,U1) . (the_result_sort_of hf))
bool ( the Sorts of (S,U1) . (the_result_sort_of hf)) is non empty set
(S,U1) . hf is Relation-like ( the Arity of S * ((S,U1) #)) . hf -defined ( the ResultSort of S * (S,U1)) . hf -valued Function-like total V29(( the Arity of S * ((S,U1) #)) . hf,( the ResultSort of S * (S,U1)) . hf) Element of bool [:(( the Arity of S * ((S,U1) #)) . hf),(( the ResultSort of S * (S,U1)) . hf):]
(Den (hf,(S,U1))) . x is Element of Result (hf,(S,U1))
(h . (the_result_sort_of hf)) . ((Den (hf,(S,U1))) . x) is set
D . ((S,U1,hf) -tree p) is set
(S,fa,(S,U1,(S,U1,hf)),(D * p)) is Element of Union the Sorts of fa
(Den (hf,fa)) . (h # x) is Element of Result (hf,fa)
x is set
( the carrier of S, the Sorts of (S,U1), the Sorts of fa,(S,U1),h) . x is Relation-like Function-like set
f . x is Relation-like Function-like set
s is Element of the carrier of S
the Sorts of (S,U1) . s is non empty set
h . s is non empty Relation-like the Sorts of (S,U1) . s -defined the Sorts of fa . s -valued Function-like total V29( the Sorts of (S,U1) . s, the Sorts of fa . s) Element of bool [:( the Sorts of (S,U1) . s),( the Sorts of fa . s):]
the Sorts of fa . s is non empty set
[:( the Sorts of (S,U1) . s),( the Sorts of fa . s):] is non empty Relation-like set
bool [:( the Sorts of (S,U1) . s),( the Sorts of fa . s):] is non empty set
dom (h . s) is non empty Element of bool ( the Sorts of (S,U1) . s)
bool ( the Sorts of (S,U1) . s) is non empty set
(S,U1) . s is set
( the carrier of S, the Sorts of (S,U1), the Sorts of fa,(S,U1),h) . s is Relation-like (S,U1) . s -defined the Sorts of fa . s -valued Function-like total V29((S,U1) . s, the Sorts of fa . s) Element of bool [:((S,U1) . s),( the Sorts of fa . s):]
[:((S,U1) . s),( the Sorts of fa . s):] is Relation-like set
bool [:((S,U1) . s),( the Sorts of fa . s):] is non empty set
dom (( the carrier of S, the Sorts of (S,U1), the Sorts of fa,(S,U1),h) . s) is Element of bool ((S,U1) . s)
bool ((S,U1) . s) is non empty set
(S,U1,s) is non empty Element of bool ((S,U1) . s)
(S,U1) . s is non empty set
bool ((S,U1) . s) is non empty set
(h . s) | ((S,U1) . s) is Relation-like the Sorts of (S,U1) . s -defined (S,U1) . s -defined the Sorts of (S,U1) . s -defined the Sorts of fa . s -valued Function-like Element of bool [:( the Sorts of (S,U1) . s),( the Sorts of fa . s):]
f . s is Relation-like (S,U1) . s -defined the Sorts of fa . s -valued Function-like total V29((S,U1) . s, the Sorts of fa . s) Element of bool [:((S,U1) . s),( the Sorts of fa . s):]
a is set
(( the carrier of S, the Sorts of (S,U1), the Sorts of fa,(S,U1),h) . s) . a is set
(f . s) . a is set
D | ( the Sorts of (S,U1) . s) is Relation-like TS (S,U1) -defined the Sorts of (S,U1) . s -defined TS (S,U1) -defined Union the Sorts of fa -valued Function-like Element of bool [:(TS (S,U1)),(Union the Sorts of fa):]
{ (root-tree b1) where b1 is Element of the carrier of (S,U1) : ( b1 in Terminals (S,U1) & b1 `2 = s ) } is set
t is Element of the carrier of (S,U1)
root-tree t is Relation-like the carrier of (S,U1) -valued Function-like DecoratedTree-like Element of K261( the carrier of (S,U1))
t `2 is set
(h . s) . a is set
D . a is set
(S,U1, the Sorts of fa,f,t) is Element of Union the Sorts of fa
dom (f . s) is Element of bool ((S,U1) . 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
(S,U1) is strict non-empty MSAlgebra over S
(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 V48() V49() ManySortedFunction of the Arity of S * ((S,U1) #), the ResultSort of S * (S,U1)
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
(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
the ResultSort 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) Element of bool [: the carrier' of S, 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
the ResultSort of S * (S,U1) is non empty Relation-like non-empty non empty-yielding the carrier' of S -defined Function-like total set
MSAlgebra(# (S,U1),(S,U1) #) is strict MSAlgebra over S
(S,U1) is non empty Relation-like the carrier of S -defined Function-like total (S,(S,U1))
S is non empty non void V78() ManySortedSign
the non-empty MSAlgebra over S is non-empty MSAlgebra over S
the Sorts of the non-empty MSAlgebra over S is non empty Relation-like non-empty non empty-yielding the carrier of S -defined Function-like total set
the carrier of S is non empty set
(S, the Sorts of the non-empty MSAlgebra over S) is strict non-empty MSAlgebra over S
(S, the Sorts of the non-empty MSAlgebra over S) is non empty Relation-like non-empty non empty-yielding the carrier of S -defined Function-like total set
(S, the Sorts of the non-empty MSAlgebra over S) is non empty Relation-like the carrier' of S -defined Function-like total V48() V49() ManySortedFunction of the Arity of S * ((S, the Sorts of the non-empty MSAlgebra over S) #), the ResultSort of S * (S, the Sorts of the non-empty MSAlgebra over S)
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
(S, the Sorts of the non-empty MSAlgebra over S) # is non empty Relation-like the carrier of S * -defined Function-like total set
the Arity of S * ((S, the Sorts of the non-empty MSAlgebra over S) #) is non empty Relation-like the carrier' of S -defined Function-like total set
the ResultSort 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) Element of bool [: the carrier' of S, 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
the ResultSort of S * (S, the Sorts of the non-empty MSAlgebra over S) is non empty Relation-like non-empty non empty-yielding the carrier' of S -defined Function-like total set
MSAlgebra(# (S, the Sorts of the non-empty MSAlgebra over S),(S, the Sorts of the non-empty MSAlgebra over S) #) is strict MSAlgebra over S
S is non empty non void V78() ManySortedSign
the carrier of S is non empty set
U1 is (S) MSAlgebra over S
S is non empty non void V78() ManySortedSign
the carrier of S is non empty set
U1 is 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
(S, the Sorts of U1) is strict non-empty MSAlgebra over S
(S, the Sorts of U1) is non empty Relation-like non-empty non empty-yielding the carrier of S -defined Function-like total set
(S, the Sorts of U1) is non empty Relation-like the carrier' of S -defined Function-like total V48() V49() ManySortedFunction of the Arity of S * ((S, the Sorts of U1) #), the ResultSort of S * (S, the Sorts of U1)
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
(S, the Sorts of U1) # is non empty Relation-like the carrier of S * -defined Function-like total set
the Arity of S * ((S, the Sorts of U1) #) is non empty Relation-like the carrier' of S -defined Function-like total set
the ResultSort 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) Element of bool [: the carrier' of S, 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
the ResultSort of S * (S, the Sorts of U1) is non empty Relation-like non-empty non empty-yielding the carrier' of S -defined Function-like total set
MSAlgebra(# (S, the Sorts of U1),(S, the Sorts of U1) #) is strict MSAlgebra over S
(S, the Sorts of U1) is non empty Relation-like the carrier of S -defined Function-like total (S,(S, the Sorts of U1))
(S, the Sorts of U1) is non empty Relation-like the carrier of S -defined Function-like total V48() V49() ManySortedFunction of (S, the Sorts of U1), the Sorts of U1
fa is strict non-empty (S) MSAlgebra over S
the Sorts of fa is non empty Relation-like non-empty non empty-yielding the carrier of S -defined Function-like total set
the Sorts of (S, the Sorts of U1) is non empty Relation-like non-empty non empty-yielding the carrier of S -defined Function-like total set
F is non empty Relation-like the carrier of S -defined Function-like total V48() V49() ManySortedFunction of the Sorts of (S, the Sorts of U1), the Sorts of U1
( the carrier of S, the Sorts of (S, the Sorts of U1), the Sorts of U1,(S, the Sorts of U1),F) is non empty Relation-like the carrier of S -defined Function-like total V48() V49() ManySortedFunction of (S, the Sorts of U1), the Sorts of U1
a is non empty Relation-like the carrier of S -defined Function-like total V48() V49() ManySortedFunction of the Sorts of fa, the Sorts of U1
s is set
a . s is Relation-like Function-like set
proj2 (a . s) is set
the Sorts of U1 . s is set
s0 is Element of the carrier of S
the Sorts of fa . s0 is non empty set
the Sorts of U1 . s0 is non empty set
[:( the Sorts of fa . s0),( the Sorts of U1 . s0):] is non empty Relation-like set
bool [:( the Sorts of fa . s0),( the Sorts of U1 . s0):] is non empty set
(S, the Sorts of U1) . s0 is Relation-like (S, the Sorts of U1) . s0 -defined the Sorts of U1 . s0 -valued Function-like total V29((S, the Sorts of U1) . s0, the Sorts of U1 . s0) Element of bool [:((S, the Sorts of U1) . s0),( the Sorts of U1 . s0):]
(S, the Sorts of U1) . s0 is set
[:((S, the Sorts of U1) . s0),( the Sorts of U1 . s0):] is Relation-like set
bool [:((S, the Sorts of U1) . s0),( the Sorts of U1 . s0):] is non empty set
g is non empty Relation-like the Sorts of fa . s0 -defined the Sorts of U1 . s0 -valued Function-like total V29( the Sorts of fa . s0, the Sorts of U1 . s0) Element of bool [:( the Sorts of fa . s0),( the Sorts of U1 . s0):]
g | ((S, the Sorts of U1) . s0) is Relation-like the Sorts of fa . s0 -defined (S, the Sorts of U1) . s0 -defined the Sorts of fa . s0 -defined the Sorts of U1 . s0 -valued Function-like Element of bool [:( the Sorts of fa . s0),( the Sorts of U1 . s0):]
proj2 ((S, the Sorts of U1) . s0) is set
proj2 g is non empty set
x is set
(S, the Sorts of 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, the Sorts of 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, the Sorts of U1) is non empty set
[: the carrier' of S,{ the carrier of S}:] \/ (Union ( the carrier of S, the Sorts of U1)) is non empty set
(S, the Sorts of U1) is Relation-like [: the carrier' of S,{ the carrier of S}:] \/ (Union ( the carrier of S, the Sorts of U1)) -defined ([: the carrier' of S,{ the carrier of S}:] \/ (Union ( the carrier of S, the Sorts of U1))) * -valued Element of bool [:([: the carrier' of S,{ the carrier of S}:] \/ (Union ( the carrier of S, the Sorts of U1))),(([: the carrier' of S,{ the carrier of S}:] \/ (Union ( the carrier of S, the Sorts of U1))) *):]
([: the carrier' of S,{ the carrier of S}:] \/ (Union ( the carrier of S, the Sorts of U1))) * is non empty functional FinSequence-membered M19([: the carrier' of S,{ the carrier of S}:] \/ (Union ( the carrier of S, the Sorts of U1)))
[:([: the carrier' of S,{ the carrier of S}:] \/ (Union ( the carrier of S, the Sorts of U1))),(([: the carrier' of S,{ the carrier of S}:] \/ (Union ( the carrier of S, the Sorts of U1))) *):] is non empty Relation-like set
bool [:([: the carrier' of S,{ the carrier of S}:] \/ (Union ( the carrier of S, the Sorts of U1))),(([: the carrier' of S,{ the carrier of S}:] \/ (Union ( the carrier of S, the Sorts of U1))) *):] is non empty set
DTConstrStr(# ([: the carrier' of S,{ the carrier of S}:] \/ (Union ( the carrier of S, the Sorts of U1))),(S, the Sorts of U1) #) is non empty strict DTConstrStr
[x,s0] is V26() set
{x,s0} is non empty set
{x} is non empty set
{{x,s0},{x}} is non empty set
Terminals (S, the Sorts of U1) is non empty Element of bool the carrier of (S, the Sorts of U1)
the carrier of (S, the Sorts of U1) is non empty set
bool the carrier of (S, the Sorts of U1) is non empty set
t is Element of the carrier of (S, the Sorts of U1)
t `2 is set
root-tree t is Relation-like the carrier of (S, the Sorts of U1) -valued Function-like DecoratedTree-like Element of K261( the carrier of (S, the Sorts of U1))
K261( the carrier of (S, the Sorts of U1)) is non empty functional V61() M14( the carrier of (S, the Sorts of U1))
{ (root-tree b1) where b1 is Element of the carrier of (S, the Sorts of U1) : ( b1 in Terminals (S, the Sorts of U1) & b1 `2 = s0 ) } is set
(S, the Sorts of U1,s0) is non empty Element of bool ((S, the Sorts of U1) . s0)
(S, the Sorts of U1) . s0 is non empty set
bool ((S, the Sorts of U1) . s0) is non empty set
(S, the Sorts of U1,s0) is non empty Relation-like (S, the Sorts of U1,s0) -defined the Sorts of U1 . s0 -valued Function-like total V29((S, the Sorts of U1,s0), the Sorts of U1 . s0) Element of bool [:(S, the Sorts of U1,s0),( the Sorts of U1 . s0):]
[:(S, the Sorts of U1,s0),( the Sorts of U1 . s0):] is non empty Relation-like set
bool [:(S, the Sorts of U1,s0),( the Sorts of U1 . s0):] is non empty set
dom ((S, the Sorts of U1) . s0) is Element of bool ((S, the Sorts of U1) . s0)
bool ((S, the Sorts of U1) . s0) is non empty set
((S, the Sorts of U1) . s0) . (root-tree t) is set
t `1 is 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 strict non-empty (S) MSAlgebra over S
the Sorts of U0 is non empty Relation-like non-empty non empty-yielding the carrier of S -defined Function-like total set
F is non empty Relation-like the carrier of S -defined Function-like total V48() V49() ManySortedFunction of the Sorts of U0, the Sorts of U1
Image F is strict non-empty MSSubAlgebra of U1