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