:: MSAFREE1 semantic presentation

K97() is set
K101() is non empty V24() V25() V26() Element of bool K97()
bool K97() is set
K96() is non empty V24() V25() V26() set
bool K96() is set
[:K101(),K97():] is Relation-like set
bool [:K101(),K97():] is set
bool (bool K97()) is set
bool K101() is set
{} is Relation-like non-empty empty-yielding K101() -defined Function-like one-to-one constant functional empty V24() V25() V26() V28() V29() V30() V31() FinSequence-like FinSubsequence-like FinSequence-membered constituted-Trees constituted-FinTrees constituted-DTrees Tree-yielding FinTree-yielding DTree-yielding set
1 is non empty set
{{},1} is non empty set
Trees is non empty constituted-Trees set
bool Trees is set
FinTrees is non empty constituted-Trees constituted-FinTrees Element of bool Trees
PeanoNat is non empty strict with_terminals with_nonterminals with_useful_nonterminals DTConstrStr
the carrier of PeanoNat is non empty set
FinTrees the carrier of PeanoNat is functional non empty constituted-DTrees DTree-set of the carrier of PeanoNat
TS PeanoNat is functional non empty constituted-DTrees Element of bool (FinTrees the carrier of PeanoNat)
bool (FinTrees the carrier of PeanoNat) is set
[:(TS PeanoNat),K101():] is Relation-like set
bool [:(TS PeanoNat),K101():] is set
[:K101(),(TS PeanoNat):] is Relation-like set
bool [:K101(),(TS PeanoNat):] is set
2 is non empty set
3 is non empty set
f2 is Relation-like Function-like set
f1 is Relation-like Function-like set
product f1 is set
rng f2 is set
Union f1 is set
G is set
dom f2 is set
R is set
f2 . R is set
dom f1 is set
f1 . R is set
F₂() is non empty set
F₁() is non empty DTConstrStr
TS F₁() is functional constituted-DTrees Element of bool (FinTrees the carrier of F₁())
the carrier of F₁() is non empty set
FinTrees the carrier of F₁() is functional non empty constituted-DTrees DTree-set of the carrier of F₁()
bool (FinTrees the carrier of F₁()) is set
[:(TS F₁()),F₂():] is Relation-like set
bool [:(TS F₁()),F₂():] is set
Terminals F₁() is set
F₅() is Relation-like TS F₁() -defined F₂() -valued Function-like V18( TS F₁(),F₂()) Element of bool [:(TS F₁()),F₂():]
(TS F₁()) * is functional non empty FinSequence-membered set
F₂() * is functional non empty FinSequence-membered set
F₆() is Relation-like TS F₁() -defined F₂() -valued Function-like V18( TS F₁(),F₂()) Element of bool [:(TS F₁()),F₂():]
f1 is Element of the carrier of F₁()
f2 is Relation-like K101() -defined FinTrees the carrier of F₁() -valued Function-like V31() FinSequence-like FinSubsequence-like FinSequence of TS F₁()
roots f2 is Relation-like K101() -defined the carrier of F₁() -valued Function-like V31() FinSequence-like FinSubsequence-like FinSequence of the carrier of F₁()
rng f2 is set
f1 -tree f2 is Relation-like the carrier of F₁() -valued Function-like DecoratedTree-like Element of FinTrees the carrier of F₁()
F₅() . (f1 -tree f2) is set
F₆() . (f1 -tree f2) is set
dom F₅() is set
F₅() * f2 is Relation-like K101() -defined F₂() -valued Function-like Element of bool [:K101(),F₂():]
[:K101(),F₂():] is Relation-like set
bool [:K101(),F₂():] is set
dom (F₅() * f2) is set
dom f2 is Element of bool K101()
dom F₆() is set
F₆() * f2 is Relation-like K101() -defined F₂() -valued Function-like Element of bool [:K101(),F₂():]
dom (F₆() * f2) is set
G is set
f2 . G is Relation-like Function-like set
R is Relation-like the carrier of F₁() -valued Function-like DecoratedTree-like Element of FinTrees the carrier of F₁()
F₅() . R is set
F₆() . R is set
(F₅() * f2) . G is set
(F₆() * f2) . G is set
len f2 is V24() V25() V26() V30() Element of K101()
Seg (len f2) is V31() V41( len f2) Element of bool K101()
G is Relation-like K101() -defined Function-like V31() FinSequence-like FinSubsequence-like set
rng G is set
H is Relation-like K101() -defined Function-like V31() FinSequence-like FinSubsequence-like Element of (TS F₁()) *
R is Relation-like K101() -defined Function-like V31() FinSequence-like FinSubsequence-like Element of F₂() *
F₄(f1,H,R) is Element of F₂()
f1 is Element of the carrier of F₁()
root-tree f1 is Relation-like the carrier of F₁() -valued Function-like DecoratedTree-like Element of FinTrees the carrier of F₁()
F₅() . (root-tree f1) is set
F₆() . (root-tree f1) is set
F₃(f1) is Element of F₂()
f1 is set
F₅() . f1 is set
F₆() . f1 is set
f1 is non empty non void V68() ManySortedSign
the carrier of f1 is non empty set
the carrier' of f1 is non empty set
{ the carrier of f1} is non empty set
[: the carrier' of f1,{ the carrier of f1}:] is Relation-like set
f2 is Relation-like the carrier of f1 -defined Function-like non empty total set
REL f2 is Relation-like [: the carrier' of f1,{ the carrier of f1}:] \/ (Union (coprod f2)) -defined ([: the carrier' of f1,{ the carrier of f1}:] \/ (Union (coprod f2))) * -valued Element of bool [:([: the carrier' of f1,{ the carrier of f1}:] \/ (Union (coprod f2))),(([: the carrier' of f1,{ the carrier of f1}:] \/ (Union (coprod f2))) *):]
coprod f2 is Relation-like the carrier of f1 -defined Function-like non empty total set
Union (coprod f2) is set
[: the carrier' of f1,{ the carrier of f1}:] \/ (Union (coprod f2)) is set
([: the carrier' of f1,{ the carrier of f1}:] \/ (Union (coprod f2))) * is functional non empty FinSequence-membered M11([: the carrier' of f1,{ the carrier of f1}:] \/ (Union (coprod f2)))
[:([: the carrier' of f1,{ the carrier of f1}:] \/ (Union (coprod f2))),(([: the carrier' of f1,{ the carrier of f1}:] \/ (Union (coprod f2))) *):] is Relation-like set
bool [:([: the carrier' of f1,{ the carrier of f1}:] \/ (Union (coprod f2))),(([: the carrier' of f1,{ the carrier of f1}:] \/ (Union (coprod f2))) *):] is set
([: the carrier' of f1,{ the carrier of f1}:] \/ (Union (coprod f2))) * is functional non empty FinSequence-membered set
G is set
R is set
[G,R] is V15() set
{G,R} is non empty set
{G} is non empty set
{{G,R},{G}} is non empty set
H is Element of [: the carrier' of f1,{ the carrier of f1}:] \/ (Union (coprod f2))
o is Relation-like K101() -defined Function-like V31() FinSequence-like FinSubsequence-like Element of ([: the carrier' of f1,{ the carrier of f1}:] \/ (Union (coprod f2))) *
[H,o] is V15() set
{H,o} is non empty set
{H} is non empty set
{{H,o},{H}} is non empty set
f1 is non empty non void V68() ManySortedSign
the carrier of f1 is non empty set
the carrier' of f1 is non empty set
{ the carrier of f1} is non empty set
[: the carrier' of f1,{ the carrier of f1}:] is Relation-like set
f2 is Relation-like the carrier of f1 -defined Function-like non empty total set
REL f2 is Relation-like [: the carrier' of f1,{ the carrier of f1}:] \/ (Union (coprod f2)) -defined ([: the carrier' of f1,{ the carrier of f1}:] \/ (Union (coprod f2))) * -valued Element of bool [:([: the carrier' of f1,{ the carrier of f1}:] \/ (Union (coprod f2))),(([: the carrier' of f1,{ the carrier of f1}:] \/ (Union (coprod f2))) *):]
coprod f2 is Relation-like the carrier of f1 -defined Function-like non empty total set
Union (coprod f2) is set
[: the carrier' of f1,{ the carrier of f1}:] \/ (Union (coprod f2)) is set
([: the carrier' of f1,{ the carrier of f1}:] \/ (Union (coprod f2))) * is functional non empty FinSequence-membered M11([: the carrier' of f1,{ the carrier of f1}:] \/ (Union (coprod f2)))
[:([: the carrier' of f1,{ the carrier of f1}:] \/ (Union (coprod f2))),(([: the carrier' of f1,{ the carrier of f1}:] \/ (Union (coprod f2))) *):] is Relation-like set
bool [:([: the carrier' of f1,{ the carrier of f1}:] \/ (Union (coprod f2))),(([: the carrier' of f1,{ the carrier of f1}:] \/ (Union (coprod f2))) *):] is set
G is Element of the carrier' of f1
[G, the carrier of f1] is V15() set
{G, the carrier of f1} is non empty set
{G} is non empty set
{{G, the carrier of f1},{G}} is non empty set
the_arity_of G is Relation-like K101() -defined the carrier of f1 -valued Function-like V31() FinSequence-like FinSubsequence-like Element of the carrier of f1 *
the carrier of f1 * is functional non empty FinSequence-membered M11( the carrier of f1)
the Arity of f1 is Relation-like the carrier' of f1 -defined the carrier of f1 * -valued Function-like V18( the carrier' of f1, the carrier of f1 * ) Element of bool [: the carrier' of f1,( the carrier of f1 *):]
[: the carrier' of f1,( the carrier of f1 *):] is Relation-like set
bool [: the carrier' of f1,( the carrier of f1 *):] is set
the Arity of f1 . G is Relation-like K101() -defined Function-like V31() FinSequence-like FinSubsequence-like Element of the carrier of f1 *
len (the_arity_of G) is V24() V25() V26() V30() Element of K101()
R is Relation-like K101() -defined Function-like V31() FinSequence-like FinSubsequence-like set
[[G, the carrier of f1],R] is V15() set
{[G, the carrier of f1],R} is non empty set
{[G, the carrier of f1]} is Relation-like Function-like non empty set
{{[G, the carrier of f1],R},{[G, the carrier of f1]}} is non empty set
len R is V24() V25() V26() V30() Element of K101()
dom R is Element of bool K101()
([: the carrier' of f1,{ the carrier of f1}:] \/ (Union (coprod f2))) * is functional non empty FinSequence-membered set
H is Relation-like K101() -defined Function-like V31() FinSequence-like FinSubsequence-like Element of ([: the carrier' of f1,{ the carrier of f1}:] \/ (Union (coprod f2))) *
len H is V24() V25() V26() V30() Element of K101()
dom H is Element of bool K101()
o is set
H . o is set
ts is Element of the carrier' of f1
[ts, the carrier of f1] is V15() set
{ts, the carrier of f1} is non empty set
{ts} is non empty set
{{ts, the carrier of f1},{ts}} is non empty set
the_result_sort_of ts is Element of the carrier of f1
the ResultSort of f1 is Relation-like the carrier' of f1 -defined the carrier of f1 -valued Function-like V18( the carrier' of f1, the carrier of f1) Element of bool [: the carrier' of f1, the carrier of f1:]
[: the carrier' of f1, the carrier of f1:] is Relation-like set
bool [: the carrier' of f1, the carrier of f1:] is set
the ResultSort of f1 . ts is Element of the carrier of f1
(the_arity_of G) . o is set
coprod (((the_arity_of G) . o),f2) is set
o is set
R . o is set
ts is Element of the carrier' of f1
[ts, the carrier of f1] is V15() set
{ts, the carrier of f1} is non empty set
{ts} is non empty set
{{ts, the carrier of f1},{ts}} is non empty set
the_result_sort_of ts is Element of the carrier of f1
the ResultSort of f1 is Relation-like the carrier' of f1 -defined the carrier of f1 -valued Function-like V18( the carrier' of f1, the carrier of f1) Element of bool [: the carrier' of f1, the carrier of f1:]
[: the carrier' of f1, the carrier of f1:] is Relation-like set
bool [: the carrier' of f1, the carrier of f1:] is set
the ResultSort of f1 . ts is Element of the carrier of f1
(the_arity_of G) . o is set
coprod (((the_arity_of G) . o),f2) is set
f1 is non empty set
f2 is Relation-like f1 -defined Function-like non empty total set
rng f2 is non empty set
f1 is set
f2 is Relation-like f1 -defined Function-like total set
G is set
R is set
f2 . G is set
f2 . R is set
dom f2 is set
dom f2 is set
dom f2 is set
f1 is set
the Relation-like empty-yielding f1 -defined Function-like total disjoint_valued set is Relation-like empty-yielding f1 -defined Function-like total disjoint_valued set
f1 is non empty set
f2 is Relation-like f1 -defined Function-like non empty total disjoint_valued set
G is Relation-like non-empty non empty-yielding f1 -defined Function-like non empty total set
Union f2 is set
Union G is non empty set
[:(Union f2),(Union G):] is Relation-like set
bool [:(Union f2),(Union G):] is set
R is Relation-like f1 -defined Function-like non empty total V53() ManySortedFunction of f2,G
H is set
dom f2 is non empty set
o is set
f2 . o is set
ts is Element of f1
R . ts is Relation-like f2 . ts -defined G . ts -valued Function-like V18(f2 . ts,G . ts) Element of bool [:(f2 . ts),(G . ts):]
f2 . ts is set
G . ts is non empty set
[:(f2 . ts),(G . ts):] is Relation-like set
bool [:(f2 . ts),(G . ts):] is set
(R . ts) . H is set
x is set
dom G is non empty set
a is Element of f1
f2 . a is set
R . a is Relation-like f2 . a -defined G . a -valued Function-like V18(f2 . a,G . a) Element of bool [:(f2 . a),(G . a):]
G . a is non empty set
[:(f2 . a),(G . a):] is Relation-like set
bool [:(f2 . a),(G . a):] is set
(R . a) . H is set
H is Relation-like Union f2 -defined Union G -valued Function-like V18( Union f2, Union G) Element of bool [:(Union f2),(Union G):]
o is Element of f1
f2 . o is set
R . o is Relation-like f2 . o -defined G . o -valued Function-like V18(f2 . o,G . o) Element of bool [:(f2 . o),(G . o):]
G . o is non empty set
[:(f2 . o),(G . o):] is Relation-like set
bool [:(f2 . o),(G . o):] is set
ts is set
H . ts is set
(R . o) . ts is set
dom f2 is non empty set
H is Relation-like Union f2 -defined Union G -valued Function-like V18( Union f2, Union G) Element of bool [:(Union f2),(Union G):]
o is Relation-like Union f2 -defined Union G -valued Function-like V18( Union f2, Union G) Element of bool [:(Union f2),(Union G):]
ts is set
dom f2 is non empty set
x is set
f2 . x is set
H . ts is set
a is Element of f1
R . a is Relation-like f2 . a -defined G . a -valued Function-like V18(f2 . a,G . a) Element of bool [:(f2 . a),(G . a):]
f2 . a is set
G . a is non empty set
[:(f2 . a),(G . a):] is Relation-like set
bool [:(f2 . a),(G . a):] is set
(R . a) . ts is set
o . ts is set
f1 is non empty set
f2 is Relation-like f1 -defined Function-like non empty total disjoint_valued set
Union f2 is set
G is Relation-like non-empty non empty-yielding f1 -defined Function-like non empty total set
Union G is non empty set
R is Relation-like f1 -defined Function-like non empty total V53() ManySortedFunction of f2,G
(f1,f2,G,R) is Relation-like Union f2 -defined Union G -valued Function-like V18( Union f2, Union G) Element of bool [:(Union f2),(Union G):]
[:(Union f2),(Union G):] is Relation-like set
bool [:(Union f2),(Union G):] is set
H is Relation-like f1 -defined Function-like non empty total V53() ManySortedFunction of f2,G
(f1,f2,G,H) is Relation-like Union f2 -defined Union G -valued Function-like V18( Union f2, Union G) Element of bool [:(Union f2),(Union G):]
o is set
G . o is set
f2 . o is set
ts is non empty set
[:(f2 . o),ts:] is Relation-like set
bool [:(f2 . o),ts:] is set
R . o is set
H . o is set
x9 is set
x is Relation-like f2 . o -defined ts -valued Function-like V18(f2 . o,ts) Element of bool [:(f2 . o),ts:]
x . x9 is set
(f1,f2,G,R) . x9 is set
a is Relation-like f2 . o -defined ts -valued Function-like V18(f2 . o,ts) Element of bool [:(f2 . o),ts:]
a . x9 is set
f1 is non empty V68() ManySortedSign
f1 is non empty V68() ManySortedSign
the carrier of f1 is non empty set
f2 is Relation-like the carrier of f1 -defined Function-like non empty total set
the carrier' of f1 is set
the Arity of f1 is Relation-like the carrier' of f1 -defined the carrier of f1 * -valued Function-like V18( the carrier' of f1, the carrier of f1 * ) Element of bool [: the carrier' of f1,( the carrier of f1 *):]
the carrier of f1 * is functional non empty FinSequence-membered M11( the carrier of f1)
[: the carrier' of f1,( the carrier of f1 *):] is Relation-like set
bool [: the carrier' of f1,( the carrier of f1 *):] is set
f2 # is Relation-like the carrier of f1 * -defined Function-like non empty total set
the Arity of f1 * (f2 #) is Relation-like the carrier' of f1 -defined Function-like total set
the ResultSort of f1 is Relation-like the carrier' of f1 -defined the carrier of f1 -valued Function-like V18( the carrier' of f1, the carrier of f1) Element of bool [: the carrier' of f1, the carrier of f1:]
[: the carrier' of f1, the carrier of f1:] is Relation-like set
bool [: the carrier' of f1, the carrier of f1:] is set
the ResultSort of f1 * f2 is Relation-like the carrier' of f1 -defined Function-like total set
the Relation-like the carrier' of f1 -defined Function-like total V53() ManySortedFunction of the Arity of f1 * (f2 #), the ResultSort of f1 * f2 is Relation-like the carrier' of f1 -defined Function-like total V53() ManySortedFunction of the Arity of f1 * (f2 #), the ResultSort of f1 * f2
MSAlgebra(# f2, the Relation-like the carrier' of f1 -defined Function-like total V53() ManySortedFunction of the Arity of f1 * (f2 #), the ResultSort of f1 * f2 #) is strict MSAlgebra over f1
the Sorts of MSAlgebra(# f2, the Relation-like the carrier' of f1 -defined Function-like total V53() ManySortedFunction of the Arity of f1 * (f2 #), the ResultSort of f1 * f2 #) is Relation-like the carrier of f1 -defined Function-like non empty total set
R is set
the Sorts of MSAlgebra(# f2, the Relation-like the carrier' of f1 -defined Function-like total V53() ManySortedFunction of the Arity of f1 * (f2 #), the ResultSort of f1 * f2 #) . R is set
{R} is non empty set
f2 is strict MSAlgebra over f1
the Sorts of f2 is Relation-like the carrier of f1 -defined Function-like non empty total set
G is strict MSAlgebra over f1
the Sorts of G is Relation-like the carrier of f1 -defined Function-like non empty total set
H is set
the Sorts of f2 . H is set
{H} is non empty set
the Sorts of G . H is set
the ResultSort of f1 is Relation-like the carrier' of f1 -defined the carrier of f1 -valued Function-like V18( the carrier' of f1, the carrier of f1) Element of bool [: the carrier' of f1, the carrier of f1:]
the carrier' of f1 is set
[: the carrier' of f1, the carrier of f1:] is Relation-like set
bool [: the carrier' of f1, the carrier of f1:] is set
dom the ResultSort of f1 is set
the ResultSort of f1 * the Sorts of f2 is Relation-like the carrier' of f1 -defined Function-like total set
H is set
( the ResultSort of f1 * the Sorts of f2) . H is set
the ResultSort of f1 . H is set
the Sorts of f2 . ( the ResultSort of f1 . H) is set
{( the ResultSort of f1 . H)} is non empty set
the Arity of f1 is Relation-like the carrier' of f1 -defined the carrier of f1 * -valued Function-like V18( the carrier' of f1, the carrier of f1 * ) Element of bool [: the carrier' of f1,( the carrier of f1 *):]
the carrier of f1 * is functional non empty FinSequence-membered M11( the carrier of f1)
[: the carrier' of f1,( the carrier of f1 *):] is Relation-like set
bool [: the carrier' of f1,( the carrier of f1 *):] is set
the Sorts of f2 # is Relation-like the carrier of f1 * -defined Function-like non empty total set
the Arity of f1 * ( the Sorts of f2 #) is Relation-like the carrier' of f1 -defined Function-like total set
( the Arity of f1 * ( the Sorts of f2 #)) . H is set
ts is non empty set
[:(( the Arity of f1 * ( the Sorts of f2 #)) . H),ts:] is Relation-like set
bool [:(( the Arity of f1 * ( the Sorts of f2 #)) . H),ts:] is set
the Charact of f2 is Relation-like the carrier' of f1 -defined Function-like total V53() ManySortedFunction of the Arity of f1 * ( the Sorts of f2 #), the ResultSort of f1 * the Sorts of f2
the Charact of f2 . H is set
the Charact of G is Relation-like the carrier' of f1 -defined Function-like total V53() ManySortedFunction of the Arity of f1 * ( the Sorts of G #), the ResultSort of f1 * the Sorts of G
the Sorts of G # is Relation-like the carrier of f1 * -defined Function-like non empty total set
the Arity of f1 * ( the Sorts of G #) is Relation-like the carrier' of f1 -defined Function-like total set
the ResultSort of f1 * the Sorts of G is Relation-like the carrier' of f1 -defined Function-like total set
the Charact of G . H is set
x9 is set
x is Relation-like ( the Arity of f1 * ( the Sorts of f2 #)) . H -defined ts -valued Function-like V18(( the Arity of f1 * ( the Sorts of f2 #)) . H,ts) Element of bool [:(( the Arity of f1 * ( the Sorts of f2 #)) . H),ts:]
x . x9 is set
a is Relation-like ( the Arity of f1 * ( the Sorts of f2 #)) . H -defined ts -valued Function-like V18(( the Arity of f1 * ( the Sorts of f2 #)) . H,ts) Element of bool [:(( the Arity of f1 * ( the Sorts of f2 #)) . H),ts:]
a . x9 is set
f1 is non empty V68() ManySortedSign
(f1) is strict MSAlgebra over f1
the Sorts of (f1) is Relation-like the carrier of f1 -defined Function-like non empty total set
the carrier of f1 is non empty set
G is set
the Sorts of (f1) . G is set
{G} is non empty set
G is set
R is set
the Sorts of (f1) . G is set
the Sorts of (f1) . R is set
dom the Sorts of (f1) is non empty set
{G} is non empty set
{R} is non empty set
dom the Sorts of (f1) is non empty set
dom the Sorts of (f1) is non empty set
f1 is non empty V68() ManySortedSign
(f1) is strict MSAlgebra over f1
f1 is non empty V68() ManySortedSign
(f1) is strict MSAlgebra over f1
f1 is non empty V68() ManySortedSign
f2 is (f1) MSAlgebra over f1
the Sorts of f2 is Relation-like the carrier of f1 -defined Function-like non empty total set
the carrier of f1 is non empty set
f1 is non empty non void V68() ManySortedSign
the carrier' of f1 is non empty set
the carrier of f1 is non empty set
f2 is Element of the carrier' of f1
G is non-empty (f1) MSAlgebra over f1
the Sorts of G is Relation-like non-empty non empty-yielding the carrier of f1 -defined Function-like non empty total disjoint_valued set
Args (f2,G) is functional non empty Element of rng ( the Sorts of G #)
the Sorts of G # is Relation-like the carrier of f1 * -defined Function-like non empty total set
the carrier of f1 * is functional non empty FinSequence-membered M11( the carrier of f1)
rng ( the Sorts of G #) is non empty set
the Arity of f1 is Relation-like the carrier' of f1 -defined the carrier of f1 * -valued Function-like V18( the carrier' of f1, the carrier of f1 * ) Element of bool [: the carrier' of f1,( the carrier of f1 *):]
[: the carrier' of f1,( the carrier of f1 *):] is Relation-like set
bool [: the carrier' of f1,( the carrier of f1 *):] is set
the Arity of f1 * ( the Sorts of G #) is Relation-like the carrier' of f1 -defined Function-like non empty total set
( the Arity of f1 * ( the Sorts of G #)) . f2 is set
R is non-empty MSAlgebra over f1
the Sorts of R is Relation-like non-empty non empty-yielding the carrier of f1 -defined Function-like non empty total set
H is Relation-like the carrier of f1 -defined Function-like non empty total V53() ManySortedFunction of the Sorts of G, the Sorts of R
( the carrier of f1, the Sorts of G, the Sorts of R,H) is Relation-like Union the Sorts of G -defined Union the Sorts of R -valued Function-like V18( Union the Sorts of G, Union the Sorts of R) Element of bool [:(Union the Sorts of G),(Union the Sorts of R):]
Union the Sorts of G is non empty set
Union the Sorts of R is non empty set
[:(Union the Sorts of G),(Union the Sorts of R):] is Relation-like set
bool [:(Union the Sorts of G),(Union the Sorts of R):] is set
o is Relation-like Function-like Element of Args (f2,G)
o * ( the carrier of f1, the Sorts of G, the Sorts of R,H) is Relation-like Union the Sorts of R -valued Function-like set
H # o is Relation-like Function-like Element of Args (f2,R)
Args (f2,R) is functional non empty Element of rng ( the Sorts of R #)
the Sorts of R # is Relation-like the carrier of f1 * -defined Function-like non empty total set
rng ( the Sorts of R #) is non empty set
the Arity of f1 * ( the Sorts of R #) is Relation-like the carrier' of f1 -defined Function-like non empty total set
( the Arity of f1 * ( the Sorts of R #)) . f2 is set
dom the Arity of f1 is set
the_arity_of f2 is Relation-like K101() -defined the carrier of f1 -valued Function-like V31() FinSequence-like FinSubsequence-like Element of the carrier of f1 *
the Arity of f1 . f2 is Relation-like K101() -defined Function-like V31() FinSequence-like FinSubsequence-like Element of the carrier of f1 *
( the Sorts of G #) . ( the Arity of f1 . f2) is set
(the_arity_of f2) * the Sorts of G is Relation-like non-empty K101() -defined Function-like set
product ((the_arity_of f2) * the Sorts of G) is set
rng o is set
Union ((the_arity_of f2) * the Sorts of G) is set
rng ((the_arity_of f2) * the Sorts of G) is V36() set
union (rng ((the_arity_of f2) * the Sorts of G)) is set
rng the Sorts of G is non empty V36() set
union (rng the Sorts of G) is set
dom ( the carrier of f1, the Sorts of G, the Sorts of R,H) is set
dom (o * ( the carrier of f1, the Sorts of G, the Sorts of R,H)) is set
dom o is set
rng (the_arity_of f2) is set
dom the Sorts of G is non empty set
dom ((the_arity_of f2) * the Sorts of G) is set
dom (the_arity_of f2) is Element of bool K101()
x is set
(the_arity_of f2) * the Sorts of R is Relation-like non-empty K101() -defined Function-like set
dom ((the_arity_of f2) * the Sorts of R) is set
(the_arity_of f2) . x is set
the Sorts of R . ((the_arity_of f2) . x) is set
((the_arity_of f2) * the Sorts of R) . x is set
the Sorts of G . ((the_arity_of f2) . x) is set
((the_arity_of f2) * the Sorts of G) . x is set
o . x is set
a is Element of the carrier of f1
the Sorts of G . a is non empty set
(o * ( the carrier of f1, the Sorts of G, the Sorts of R,H)) . x is set
( the carrier of f1, the Sorts of G, the Sorts of R,H) . (o . x) is set
H . a is Relation-like the Sorts of G . a -defined the Sorts of R . a -valued Function-like V18( the Sorts of G . a, the Sorts of R . a) Element of bool [:( the Sorts of G . a),( the Sorts of R . a):]
the Sorts of R . a is non empty set
[:( the Sorts of G . a),( the Sorts of R . a):] is Relation-like set
bool [:( the Sorts of G . a),( the Sorts of R . a):] is set
(H . a) . (o . x) is set
dom the Sorts of R is non empty set
product ((the_arity_of f2) * the Sorts of R) is set
( the Sorts of R #) . ( the Arity of f1 . f2) is set
a is V24() V25() V26() V30() set
(the_arity_of f2) /. a is Element of the carrier of f1
(the_arity_of f2) . a is set
o . a is set
((the_arity_of f2) * the Sorts of G) . a is set
the Sorts of G . ((the_arity_of f2) /. a) is non empty set
x is Relation-like Function-like Element of Args (f2,R)
x . a is set
( the carrier of f1, the Sorts of G, the Sorts of R,H) . (o . a) is set
H . ((the_arity_of f2) /. a) is Relation-like the Sorts of G . ((the_arity_of f2) /. a) -defined the Sorts of R . ((the_arity_of f2) /. a) -valued Function-like V18( the Sorts of G . ((the_arity_of f2) /. a), the Sorts of R . ((the_arity_of f2) /. a)) Element of bool [:( the Sorts of G . ((the_arity_of f2) /. a)),( the Sorts of R . ((the_arity_of f2) /. a)):]
the Sorts of R . ((the_arity_of f2) /. a) is non empty set
[:( the Sorts of G . ((the_arity_of f2) /. a)),( the Sorts of R . ((the_arity_of f2) /. a)):] is Relation-like set
bool [:( the Sorts of G . ((the_arity_of f2) /. a)),( the Sorts of R . ((the_arity_of f2) /. a)):] is set
(H . ((the_arity_of f2) /. a)) . (o . a) is set
f1 is non empty non void V68() ManySortedSign
the carrier of f1 is non empty set
f2 is Relation-like non-empty non empty-yielding the carrier of f1 -defined Function-like non empty total set
FreeSort f2 is Relation-like non-empty non empty-yielding the carrier of f1 -defined Function-like non empty total set
G is set
R is set
(FreeSort f2) . G is set
(FreeSort f2) . R is set
dom (FreeSort f2) is non empty set
o is Element of the carrier of f1
(FreeSort f2) . o is non empty set
ts is Element of the carrier of f1
(FreeSort f2) . ts is non empty set
dom (FreeSort f2) is non empty set
dom (FreeSort f2) is non empty set
F₁() is non empty non void V68() ManySortedSign
the carrier of F₁() is non empty set
F₃() is Relation-like non-empty non empty-yielding the carrier of F₁() -defined Function-like non empty total set
Union F₃() is non empty set
F₂() is Relation-like non-empty non empty-yielding the carrier of F₁() -defined Function-like non empty total set
FreeSort F₂() is Relation-like non-empty non empty-yielding the carrier of F₁() -defined Function-like non empty total disjoint_valued set
the carrier' of F₁() is non empty set
FreeMSA F₂() is strict non-empty MSAlgebra over F₁()
(Union F₃()) * is functional non empty FinSequence-membered set
F₆() is Relation-like the carrier of F₁() -defined Function-like non empty total V53() ManySortedFunction of FreeSort F₂(),F₃()
( the carrier of F₁(),(FreeSort F₂()),F₃(),F₆()) is Relation-like Union (FreeSort F₂()) -defined Union F₃() -valued Function-like V18( Union (FreeSort F₂()), Union F₃()) Element of bool [:(Union (FreeSort F₂())),(Union F₃()):]
Union (FreeSort F₂()) is non empty set
[:(Union (FreeSort F₂())),(Union F₃()):] is Relation-like set
bool [:(Union (FreeSort F₂())),(Union F₃()):] is set
F₇() is Relation-like the carrier of F₁() -defined Function-like non empty total V53() ManySortedFunction of FreeSort F₂(),F₃()
( the carrier of F₁(),(FreeSort F₂()),F₃(),F₇()) is Relation-like Union (FreeSort F₂()) -defined Union F₃() -valued Function-like V18( Union (FreeSort F₂()), Union F₃()) Element of bool [:(Union (FreeSort F₂())),(Union F₃()):]
DTConMSA F₂() is non empty strict with_terminals with_nonterminals with_useful_nonterminals DTConstrStr
TS (DTConMSA F₂()) is functional non empty constituted-DTrees Element of bool (FinTrees the carrier of (DTConMSA F₂()))
the carrier of (DTConMSA F₂()) is non empty set
FinTrees the carrier of (DTConMSA F₂()) is functional non empty constituted-DTrees DTree-set of the carrier of (DTConMSA F₂())
bool (FinTrees the carrier of (DTConMSA F₂())) is set
rng (FreeSort F₂()) is non empty V36() set
union (rng (FreeSort F₂())) is set
f1 is non empty set
[:(TS (DTConMSA F₂())),f1:] is Relation-like set
bool [:(TS (DTConMSA F₂())),f1:] is set
(TS (DTConMSA F₂())) * is functional non empty FinSequence-membered set
[: the carrier of (DTConMSA F₂()),((TS (DTConMSA F₂())) *),((Union F₃()) *):] is set
[:[: the carrier of (DTConMSA F₂()),((TS (DTConMSA F₂())) *),((Union F₃()) *):],(Union F₃()):] is Relation-like set
bool [:[: the carrier of (DTConMSA F₂()),((TS (DTConMSA F₂())) *),((Union F₃()) *):],(Union F₃()):] is set
R is Relation-like [: the carrier of (DTConMSA F₂()),((TS (DTConMSA F₂())) *),((Union F₃()) *):] -defined Union F₃() -valued Function-like V18([: the carrier of (DTConMSA F₂()),((TS (DTConMSA F₂())) *),((Union F₃()) *):], Union F₃()) Element of bool [:[: the carrier of (DTConMSA F₂()),((TS (DTConMSA F₂())) *),((Union F₃()) *):],(Union F₃()):]
f1 * is functional non empty FinSequence-membered set
[: the carrier of (DTConMSA F₂()),((TS (DTConMSA F₂())) *),(f1 *):] is set
[:[: the carrier of (DTConMSA F₂()),((TS (DTConMSA F₂())) *),(f1 *):],f1:] is Relation-like set
bool [:[: the carrier of (DTConMSA F₂()),((TS (DTConMSA F₂())) *),(f1 *):],f1:] is set
H is Relation-like [: the carrier of (DTConMSA F₂()),((TS (DTConMSA F₂())) *),(f1 *):] -defined f1 -valued Function-like V18([: the carrier of (DTConMSA F₂()),((TS (DTConMSA F₂())) *),(f1 *):],f1) Element of bool [:[: the carrier of (DTConMSA F₂()),((TS (DTConMSA F₂())) *),(f1 *):],f1:]
{ the carrier of F₁()} is non empty set
[: the carrier' of F₁(),{ the carrier of F₁()}:] is Relation-like set
coprod F₂() is Relation-like non-empty non empty-yielding the carrier of F₁() -defined Function-like non empty total set
Union (coprod F₂()) is non empty set
[: the carrier' of F₁(),{ the carrier of F₁()}:] \/ (Union (coprod F₂())) is non empty set
REL F₂() is Relation-like [: the carrier' of F₁(),{ the carrier of F₁()}:] \/ (Union (coprod F₂())) -defined ([: the carrier' of F₁(),{ the carrier of F₁()}:] \/ (Union (coprod F₂()))) * -valued Element of bool [:([: the carrier' of F₁(),{ the carrier of F₁()}:] \/ (Union (coprod F₂()))),(([: the carrier' of F₁(),{ the carrier of F₁()}:] \/ (Union (coprod F₂()))) *):]
([: the carrier' of F₁(),{ the carrier of F₁()}:] \/ (Union (coprod F₂()))) * is functional non empty FinSequence-membered M11([: the carrier' of F₁(),{ the carrier of F₁()}:] \/ (Union (coprod F₂())))
[:([: the carrier' of F₁(),{ the carrier of F₁()}:] \/ (Union (coprod F₂()))),(([: the carrier' of F₁(),{ the carrier of F₁()}:] \/ (Union (coprod F₂()))) *):] is Relation-like set
bool [:([: the carrier' of F₁(),{ the carrier of F₁()}:] \/ (Union (coprod F₂()))),(([: the carrier' of F₁(),{ the carrier of F₁()}:] \/ (Union (coprod F₂()))) *):] is set
DTConstrStr(# ([: the carrier' of F₁(),{ the carrier of F₁()}:] \/ (Union (coprod F₂()))),(REL F₂()) #) is non empty strict DTConstrStr
o is Relation-like the carrier of F₁() -defined Function-like non empty total V53() ManySortedFunction of FreeSort F₂(),F₃()
( the carrier of F₁(),(FreeSort F₂()),F₃(),o) is Relation-like Union (FreeSort F₂()) -defined Union F₃() -valued Function-like V18( Union (FreeSort F₂()), Union F₃()) Element of bool [:(Union (FreeSort F₂())),(Union F₃()):]
ts is Element of the carrier of (DTConMSA F₂())
x is Relation-like K101() -defined Function-like V31() FinSequence-like FinSubsequence-like Element of (TS (DTConMSA F₂())) *
roots x is Relation-like K101() -defined Function-like V31() FinSequence-like FinSubsequence-like set
[ts,(roots x)] is V15() set
{ts,(roots x)} is non empty set
{ts} is non empty set
{{ts,(roots x)},{ts}} is non empty set
a is Element of the carrier' of F₁()
x9 is Element of { the carrier of F₁()}
[a,x9] is V15() set
{a,x9} is non empty set
{a} is non empty set
{{a,x9},{a}} is non empty set
x is Relation-like K101() -defined Function-like V31() FinSequence-like FinSubsequence-like Element of f1 *
x * ( the carrier of F₁(),(FreeSort F₂()),F₃(),o) is Relation-like K101() -defined Union F₃() -valued Function-like set
FreeOper F₂() is Relation-like the carrier' of F₁() -defined Function-like non empty total V53() ManySortedFunction of the Arity of F₁() * ((FreeSort F₂()) #), the ResultSort of F₁() * (FreeSort F₂())
the Arity of F₁() is Relation-like the carrier' of F₁() -defined the carrier of F₁() * -valued Function-like V18( the carrier' of F₁(), the carrier of F₁() * ) Element of bool [: the carrier' of F₁(),( the carrier of F₁() *):]
the carrier of F₁() * is functional non empty FinSequence-membered M11( the carrier of F₁())
[: the carrier' of F₁(),( the carrier of F₁() *):] is Relation-like set
bool [: the carrier' of F₁(),( the carrier of F₁() *):] is set
(FreeSort F₂()) # is Relation-like the carrier of F₁() * -defined Function-like non empty total set
the Arity of F₁() * ((FreeSort F₂()) #) is Relation-like the carrier' of F₁() -defined Function-like non empty total set
the ResultSort of F₁() is Relation-like the carrier' of F₁() -defined the carrier of F₁() -valued Function-like V18( the carrier' of F₁(), the carrier of F₁()) Element of bool [: the carrier' of F₁(), the carrier of F₁():]
[: the carrier' of F₁(), the carrier of F₁():] is Relation-like set
bool [: the carrier' of F₁(), the carrier of F₁():] is set
the ResultSort of F₁() * (FreeSort F₂()) is Relation-like non-empty non empty-yielding the carrier' of F₁() -defined Function-like non empty total set
MSAlgebra(# (FreeSort F₂()),(FreeOper F₂()) #) is strict MSAlgebra over F₁()
Sym (a,F₂()) is Element of the carrier of (DTConMSA F₂())
tss is Relation-like K101() -defined FinTrees the carrier of (DTConMSA F₂()) -valued Function-like V31() FinSequence-like FinSubsequence-like DTree-yielding FinSequence of TS (DTConMSA F₂())
( the Arity of F₁() * ((FreeSort F₂()) #)) . a is set
( the ResultSort of F₁() * (FreeSort F₂())) . a is non empty set
the_result_sort_of a is Element of the carrier of F₁()
the ResultSort of F₁() . a is Element of the carrier of F₁()
(FreeSort F₂()) . (the_result_sort_of a) is non empty set
DenOp (a,F₂()) is Relation-like ( the Arity of F₁() * ((FreeSort F₂()) #)) . a -defined ( the ResultSort of F₁() * (FreeSort F₂())) . a -valued Function-like V18(( the Arity of F₁() * ((FreeSort F₂()) #)) . a,( the ResultSort of F₁() * (FreeSort F₂())) . a) Element of bool [:(( the Arity of F₁() * ((FreeSort F₂()) #)) . a),(( the ResultSort of F₁() * (FreeSort F₂())) . a):]
[:(( the Arity of F₁() * ((FreeSort F₂()) #)) . a),(( the ResultSort of F₁() * (FreeSort F₂())) . a):] is Relation-like set
bool [:(( the Arity of F₁() * ((FreeSort F₂()) #)) . a),(( the ResultSort of F₁() * (FreeSort F₂())) . a):] is set
(DenOp (a,F₂())) . x is set
[a, the carrier of F₁()] is V15() set
{a, the carrier of F₁()} is non empty set
{{a, the carrier of F₁()},{a}} is non empty set
[a, the carrier of F₁()] -tree x is Relation-like Function-like DecoratedTree-like set
( the carrier of F₁(),(FreeSort F₂()),F₃(),o) . ([a, the carrier of F₁()] -tree x) is set
(DenOp (a,F₂())) . tss is set
( the carrier of F₁(),(FreeSort F₂()),F₃(),o) . ((DenOp (a,F₂())) . tss) is set
o . (the_result_sort_of a) is Relation-like (FreeSort F₂()) . (the_result_sort_of a) -defined F₃() . (the_result_sort_of a) -valued Function-like V18((FreeSort F₂()) . (the_result_sort_of a),F₃() . (the_result_sort_of a)) Element of bool [:((FreeSort F₂()) . (the_result_sort_of a)),(F₃() . (the_result_sort_of a)):]
F₃() . (the_result_sort_of a) is non empty set
[:((FreeSort F₂()) . (the_result_sort_of a)),(F₃() . (the_result_sort_of a)):] is Relation-like set
bool [:((FreeSort F₂()) . (the_result_sort_of a)),(F₃() . (the_result_sort_of a)):] is set
(o . (the_result_sort_of a)) . ((DenOp (a,F₂())) . x) is set
Den (a,(FreeMSA F₂())) is Relation-like Args (a,(FreeMSA F₂())) -defined Result (a,(FreeMSA F₂())) -valued Function-like V18( Args (a,(FreeMSA F₂())), Result (a,(FreeMSA F₂()))) Element of bool [:(Args (a,(FreeMSA F₂()))),(Result (a,(FreeMSA F₂()))):]
Args (a,(FreeMSA F₂())) is functional non empty Element of rng ( the Sorts of (FreeMSA F₂()) #)
the Sorts of (FreeMSA F₂()) is Relation-like non-empty non empty-yielding the carrier of F₁() -defined Function-like non empty total set
the Sorts of (FreeMSA F₂()) # is Relation-like the carrier of F₁() * -defined Function-like non empty total set
rng ( the Sorts of (FreeMSA F₂()) #) is non empty set
the Arity of F₁() * ( the Sorts of (FreeMSA F₂()) #) is Relation-like the carrier' of F₁() -defined Function-like non empty total set
( the Arity of F₁() * ( the Sorts of (FreeMSA F₂()) #)) . a is set
Result (a,(FreeMSA F₂())) is non empty Element of rng the Sorts of (FreeMSA F₂())
rng the Sorts of (FreeMSA F₂()) is non empty V36() set
the ResultSort of F₁() * the Sorts of (FreeMSA F₂()) is Relation-like non-empty non empty-yielding the carrier' of F₁() -defined Function-like non empty total set
( the ResultSort of F₁() * the Sorts of (FreeMSA F₂())) . a is non empty set
[:(Args (a,(FreeMSA F₂()))),(Result (a,(FreeMSA F₂()))):] is Relation-like set
bool [:(Args (a,(FreeMSA F₂()))),(Result (a,(FreeMSA F₂()))):] is set
the Charact of (FreeMSA F₂()) is Relation-like the carrier' of F₁() -defined Function-like non empty total V53() ManySortedFunction of the Arity of F₁() * ( the Sorts of (FreeMSA F₂()) #), the ResultSort of F₁() * the Sorts of (FreeMSA F₂())
the Charact of (FreeMSA F₂()) . a is set
(Den (a,(FreeMSA F₂()))) . x is set
(o . (the_result_sort_of a)) . ((Den (a,(FreeMSA F₂()))) . x) is set
F₅(a,x,x) is Element of Union F₃()
ts `1 is set
F<sub>5</sub>((ts `1),x,x) is Element of Union F₃()
ts -tree x is Relation-like Function-like DecoratedTree-like set
( the carrier of F₁(),(FreeSort F₂()),F₃(),o) . (ts -tree x) is set
xx is Relation-like K101() -defined Function-like V31() FinSequence-like FinSubsequence-like Element of (Union F₃()) *
F₅((ts `1),x,xx) is Element of Union F<sub>3</sub>()
H . (ts,x,x) is Element of f1
f2 is Relation-like TS (DTConMSA F<sub>2</sub>()) -defined f1 -valued Function-like V18( TS (DTConMSA F<sub>2</sub>()),f1) Element of bool [:(TS (DTConMSA F<sub>2</sub>())),f1:]
o is Element of the carrier of (DTConMSA F<sub>2</sub>())
ts is Relation-like K101() -defined Function-like V31() FinSequence-like FinSubsequence-like Element of (TS (DTConMSA F<sub>2</sub>())) *
roots ts is Relation-like K101() -defined Function-like V31() FinSequence-like FinSubsequence-like set
x is Relation-like K101() -defined Function-like V31() FinSequence-like FinSubsequence-like Element of f1 *
ts * f2 is Relation-like K101() -defined f1 -valued Function-like set
o -tree ts is Relation-like Function-like DecoratedTree-like set
f2 . (o -tree ts) is set
H . (o,ts,x) is Element of f1
Terminals (DTConMSA F<sub>2</sub>()) is non empty Element of bool the carrier of (DTConMSA F<sub>2</sub>())
bool the carrier of (DTConMSA F<sub>2</sub>()) is set
[: the carrier of (DTConMSA F<sub>2</sub>()),(Union F<sub>3</sub>()):] is Relation-like set
bool [: the carrier of (DTConMSA F<sub>2</sub>()),(Union F<sub>3</sub>()):] is set
o is Relation-like the carrier of (DTConMSA F<sub>2</sub>()) -defined Union F<sub>3</sub>() -valued Function-like V18( the carrier of (DTConMSA F<sub>2</sub>()), Union F<sub>3</sub>()) Element of bool [: the carrier of (DTConMSA F<sub>2</sub>()),(Union F<sub>3</sub>()):]
[: the carrier of (DTConMSA F<sub>2</sub>()),f1:] is Relation-like set
bool [: the carrier of (DTConMSA F<sub>2</sub>()),f1:] is set
ts is Relation-like the carrier of (DTConMSA F<sub>2</sub>()) -defined f1 -valued Function-like V18( the carrier of (DTConMSA F<sub>2</sub>()),f1) Element of bool [: the carrier of (DTConMSA F<sub>2</sub>()),f1:]
dom F<sub>2</sub>() is non empty set
x is Relation-like the carrier of F<sub>1</sub>() -defined Function-like non empty total V53() ManySortedFunction of FreeSort F<sub>2</sub>(),F<sub>3</sub>()
a is Element of the carrier of (DTConMSA F<sub>2</sub>())
a `2 is set
a `1 is set
F<sub>2</sub>() . (a `2) is set
x9 is Element of the carrier of F₁()
[(a `1),x9] is V15() set
{(a `1),x9} is non empty set
{(a `1)} is non empty set
{{(a `1),x9},{(a `1)}} is non empty set
root-tree [(a `1),x9] is Relation-like Function-like DecoratedTree-like set
FreeGen (x9,F₂()) is non empty Element of bool ((FreeSort F₂()) . x9)
(FreeSort F₂()) . x9 is non empty set
bool ((FreeSort F₂()) . x9) is set
[(a `1),(a `2)] is V15() set
{(a `1),(a `2)} is non empty set
{{(a `1),(a `2)},{(a `1)}} is non empty set
( the carrier of F<sub>1</sub>(),(FreeSort F<sub>2</sub>()),F<sub>3</sub>(),x) is Relation-like Union (FreeSort F<sub>2</sub>()) -defined Union F<sub>3</sub>() -valued Function-like V18( Union (FreeSort F<sub>2</sub>()), Union F<sub>3</sub>()) Element of bool [:(Union (FreeSort F<sub>2</sub>())),(Union F<sub>3</sub>()):]
root-tree a is Relation-like the carrier of (DTConMSA F<sub>2</sub>()) -valued Function-like DecoratedTree-like Element of FinTrees the carrier of (DTConMSA F<sub>2</sub>())
( the carrier of F<sub>1</sub>(),(FreeSort F<sub>2</sub>()),F<sub>3</sub>(),x) . (root-tree a) is set
x . x9 is Relation-like (FreeSort F<sub>2</sub>()) . x9 -defined F<sub>3</sub>() . x9 -valued Function-like V18((FreeSort F<sub>2</sub>()) . x9,F<sub>3</sub>() . x9) Element of bool [:((FreeSort F<sub>2</sub>()) . x9),(F<sub>3</sub>() . x9):]
F<sub>3</sub>() . x9 is non empty set
[:((FreeSort F<sub>2</sub>()) . x9),(F<sub>3</sub>() . x9):] is Relation-like set
bool [:((FreeSort F<sub>2</sub>()) . x9),(F<sub>3</sub>() . x9):] is set
(x . x9) . (root-tree [(a `1),x9]) is set
F₄((root-tree a)) is Element of Union F₃()
ts . a is Element of f1
G is Relation-like TS (DTConMSA F₂()) -defined f1 -valued Function-like V18( TS (DTConMSA F₂()),f1) Element of bool [:(TS (DTConMSA F₂())),f1:]
x is Element of the carrier of (DTConMSA F₂())
root-tree x is Relation-like the carrier of (DTConMSA F₂()) -valued Function-like DecoratedTree-like Element of FinTrees the carrier of (DTConMSA F₂())
G . (root-tree x) is set
ts . x is Element of f1
x is Element of the carrier of (DTConMSA F₂())
a is Relation-like K101() -defined Function-like V31() FinSequence-like FinSubsequence-like Element of (TS (DTConMSA F₂())) *
roots a is Relation-like K101() -defined Function-like V31() FinSequence-like FinSubsequence-like set
x9 is Relation-like K101() -defined Function-like V31() FinSequence-like FinSubsequence-like Element of f1 *
a * G is Relation-like K101() -defined f1 -valued Function-like set
x -tree a is Relation-like Function-like DecoratedTree-like set
G . (x -tree a) is set
H . (x,a,x9) is Element of f1
x is Element of the carrier of (DTConMSA F₂())
root-tree x is Relation-like the carrier of (DTConMSA F₂()) -valued Function-like DecoratedTree-like Element of FinTrees the carrier of (DTConMSA F₂())
f2 . (root-tree x) is set
ts . x is Element of f1
f1 is non empty non void V68() ManySortedSign
the carrier of f1 is non empty set
f2 is Relation-like non-empty non empty-yielding the carrier of f1 -defined Function-like non empty total set
FreeMSA f2 is strict non-empty MSAlgebra over f1
f1 is non empty non void V68() ManySortedSign
the carrier' of f1 is non empty set
f2 is Element of the carrier' of f1
G is non-empty MSAlgebra over f1
Args (f2,G) is functional non empty Element of rng ( the Sorts of G #)
the carrier of f1 is non empty set
the Sorts of G is Relation-like non-empty non empty-yielding the carrier of f1 -defined Function-like non empty total set
the Sorts of G # is Relation-like the carrier of f1 * -defined Function-like non empty total set
the carrier of f1 * is functional non empty FinSequence-membered M11( the carrier of f1)
rng ( the Sorts of G #) is non empty set
the Arity of f1 is Relation-like the carrier' of f1 -defined the carrier of f1 * -valued Function-like V18( the carrier' of f1, the carrier of f1 * ) Element of bool [: the carrier' of f1,( the carrier of f1 *):]
[: the carrier' of f1,( the carrier of f1 *):] is Relation-like set
bool [: the carrier' of f1,( the carrier of f1 *):] is set
the Arity of f1 * ( the Sorts of G #) is Relation-like the carrier' of f1 -defined Function-like non empty total set
( the Arity of f1 * ( the Sorts of G #)) . f2 is set
Result (f2,G) is non empty Element of rng the Sorts of G
rng the Sorts of G is non empty V36() set
the ResultSort of f1 is Relation-like the carrier' of f1 -defined the carrier of f1 -valued Function-like V18( the carrier' of f1, the carrier of f1) Element of bool [: the carrier' of f1, the carrier of f1:]
[: the carrier' of f1, the carrier of f1:] is Relation-like set
bool [: the carrier' of f1, the carrier of f1:] is set
the ResultSort of f1 * the Sorts of G is Relation-like non-empty non empty-yielding the carrier' of f1 -defined Function-like non empty total set
( the ResultSort of f1 * the Sorts of G) . f2 is non empty set
f1 is non empty non void V68() ManySortedSign
the carrier of f1 is non empty set
f2 is Relation-like non-empty non empty-yielding the carrier of f1 -defined Function-like non empty total set
FreeMSA f2 is strict non-empty MSAlgebra over f1
the Sorts of (FreeMSA f2) is Relation-like non-empty non empty-yielding the carrier of f1 -defined Function-like non empty total set
FreeSort f2 is Relation-like non-empty non empty-yielding the carrier of f1 -defined Function-like non empty total disjoint_valued set
FreeOper f2 is Relation-like the carrier' of f1 -defined Function-like non empty total V53() ManySortedFunction of the Arity of f1 * ((FreeSort f2) #), the ResultSort of f1 * (FreeSort f2)
the carrier' of f1 is non empty set
the Arity of f1 is Relation-like the carrier' of f1 -defined the carrier of f1 * -valued Function-like V18( the carrier' of f1, the carrier of f1 * ) Element of bool [: the carrier' of f1,( the carrier of f1 *):]
the carrier of f1 * is functional non empty FinSequence-membered M11( the carrier of f1)
[: the carrier' of f1,( the carrier of f1 *):] is Relation-like set
bool [: the carrier' of f1,( the carrier of f1 *):] is set
(FreeSort f2) # is Relation-like the carrier of f1 * -defined Function-like non empty total set
the Arity of f1 * ((FreeSort f2) #) is Relation-like the carrier' of f1 -defined Function-like non empty total set
the ResultSort of f1 is Relation-like the carrier' of f1 -defined the carrier of f1 -valued Function-like V18( the carrier' of f1, the carrier of f1) Element of bool [: the carrier' of f1, the carrier of f1:]
[: the carrier' of f1, the carrier of f1:] is Relation-like set
bool [: the carrier' of f1, the carrier of f1:] is set
the ResultSort of f1 * (FreeSort f2) is Relation-like non-empty non empty-yielding the carrier' of f1 -defined Function-like non empty total set
MSAlgebra(# (FreeSort f2),(FreeOper f2) #) is strict MSAlgebra over f1
f1 is non empty non void V68() ManySortedSign
the carrier of f1 is non empty set
f2 is Relation-like non-empty non empty-yielding the carrier of f1 -defined Function-like non empty total set
FreeMSA f2 is strict non-empty MSAlgebra over f1
the Sorts of (FreeMSA f2) is Relation-like non-empty non empty-yielding the carrier of f1 -defined Function-like non empty total disjoint_valued set
F₁() is non empty non void V68() ManySortedSign
the carrier of F₁() is non empty set
F₂() is Relation-like non-empty non empty-yielding the carrier of F₁() -defined Function-like non empty total set
FreeMSA F₂() is strict non-empty (F₁()) MSAlgebra over F₁()
the Sorts of (FreeMSA F₂()) is Relation-like non-empty non empty-yielding the carrier of F₁() -defined Function-like non empty total disjoint_valued set
F₃() is non-empty MSAlgebra over F₁()
the Sorts of F₃() is Relation-like non-empty non empty-yielding the carrier of F₁() -defined Function-like non empty total set
F₄() is Relation-like the carrier of F₁() -defined Function-like non empty total V53() ManySortedFunction of the Sorts of (FreeMSA F₂()), the Sorts of F₃()
F₅() is Relation-like the carrier of F₁() -defined Function-like non empty total V53() ManySortedFunction of the Sorts of (FreeMSA F₂()), the Sorts of F₃()
FreeSort F₂() is Relation-like non-empty non empty-yielding the carrier of F₁() -defined Function-like non empty total disjoint_valued set
FreeOper F₂() is Relation-like the carrier' of F₁() -defined Function-like non empty total V53() ManySortedFunction of the Arity of F₁() * ((FreeSort F₂()) #), the ResultSort of F₁() * (FreeSort F₂())
the carrier' of F₁() is non empty set
the Arity of F₁() is Relation-like the carrier' of F₁() -defined the carrier of F₁() * -valued Function-like V18( the carrier' of F₁(), the carrier of F₁() * ) Element of bool [: the carrier' of F₁(),( the carrier of F₁() *):]
the carrier of F₁() * is functional non empty FinSequence-membered M11( the carrier of F₁())
[: the carrier' of F₁(),( the carrier of F₁() *):] is Relation-like set
bool [: the carrier' of F₁(),( the carrier of F₁() *):] is set
(FreeSort F₂()) # is Relation-like the carrier of F₁() * -defined Function-like non empty total set
the Arity of F₁() * ((FreeSort F₂()) #) is Relation-like the carrier' of F₁() -defined Function-like non empty total set
the ResultSort of F₁() is Relation-like the carrier' of F₁() -defined the carrier of F₁() -valued Function-like V18( the carrier' of F₁(), the carrier of F₁()) Element of bool [: the carrier' of F₁(), the carrier of F₁():]
[: the carrier' of F₁(), the carrier of F₁():] is Relation-like set
bool [: the carrier' of F₁(), the carrier of F₁():] is set
the ResultSort of F₁() * (FreeSort F₂()) is Relation-like non-empty non empty-yielding the carrier' of F₁() -defined Function-like non empty total set
MSAlgebra(# (FreeSort F₂()),(FreeOper F₂()) #) is strict MSAlgebra over F₁()
FreeGen F₂() is Relation-like the carrier of F₁() -defined Function-like non empty total GeneratorSet of FreeMSA F₂()
Union (FreeGen F₂()) is set
Union the Sorts of F₃() is non empty set
G is set
dom the Sorts of F₃() is non empty set
dom (FreeGen F₂()) is non empty set
R is set
(FreeGen F₂()) . R is set
H is Element of the carrier of F₁()
FreeGen (H,F₂()) is non empty Element of bool ((FreeSort F₂()) . H)
(FreeSort F₂()) . H is non empty set
bool ((FreeSort F₂()) . H) is set
F₄() . H is Relation-like the Sorts of (FreeMSA F₂()) . H -defined the Sorts of F₃() . H -valued Function-like V18( the Sorts of (FreeMSA F₂()) . H, the Sorts of F₃() . H) Element of bool [:( the Sorts of (FreeMSA F₂()) . H),( the Sorts of F₃() . H):]
the Sorts of (FreeMSA F₂()) . H is non empty set
the Sorts of F₃() . H is non empty set
[:( the Sorts of (FreeMSA F₂()) . H),( the Sorts of F₃() . H):] is Relation-like set
bool [:( the Sorts of (FreeMSA F₂()) . H),( the Sorts of F₃() . H):] is set
(F₄() . H) . G is set
o is set
f1 is Relation-like the carrier of F₁() -defined Function-like non empty total V53() ManySortedFunction of FreeSort F₂(), the Sorts of F₃()
f1 . H is Relation-like (FreeSort F₂()) . H -defined the Sorts of F₃() . H -valued Function-like V18((FreeSort F₂()) . H, the Sorts of F₃() . H) Element of bool [:((FreeSort F₂()) . H),( the Sorts of F₃() . H):]
[:((FreeSort F₂()) . H),( the Sorts of F₃() . H):] is Relation-like set
bool [:((FreeSort F₂()) . H),( the Sorts of F₃() . H):] is set
ts is Element of the carrier of F₁()
FreeGen (ts,F₂()) is non empty Element of bool ((FreeSort F₂()) . ts)
(FreeSort F₂()) . ts is non empty set
bool ((FreeSort F₂()) . ts) is set
((FreeSort F₂()) . ts) /\ ((FreeSort F₂()) . H) is set
[:(Union (FreeGen F₂())),(Union the Sorts of F₃()):] is Relation-like set
bool [:(Union (FreeGen F₂())),(Union the Sorts of F₃()):] is set
G is Relation-like Union (FreeGen F₂()) -defined Union the Sorts of F₃() -valued Function-like V18( Union (FreeGen F₂()), Union the Sorts of F₃()) Element of bool [:(Union (FreeGen F₂())),(Union the Sorts of F₃()):]
{ [b₁,b₂] where b₁ is Element of the carrier' of F₁(), b₂ is Relation-like Function-like Element of Args (b₁,F₃()) : verum } is set
R is set
f1 is Relation-like the carrier of F₁() -defined Function-like non empty total V53() ManySortedFunction of FreeSort F₂(), the Sorts of F₃()
H is Element of the carrier of F₁()
FreeGen (H,F₂()) is non empty Element of bool ((FreeSort F₂()) . H)
(FreeSort F₂()) . H is non empty set
bool ((FreeSort F₂()) . H) is set
f1 . H is Relation-like (FreeSort F₂()) . H -defined the Sorts of F₃() . H -valued Function-like V18((FreeSort F₂()) . H, the Sorts of F₃() . H) Element of bool [:((FreeSort F₂()) . H),( the Sorts of F₃() . H):]
the Sorts of F₃() . H is non empty set
[:((FreeSort F₂()) . H),( the Sorts of F₃() . H):] is Relation-like set
bool [:((FreeSort F₂()) . H),( the Sorts of F₃() . H):] is set
o is set
(f1 . H) . o is set
G /. o is Element of Union the Sorts of F₃()
dom (FreeGen F₂()) is non empty set
(FreeGen F₂()) . H is set
G . o is set
H is set
o is Element of the carrier' of F₁()
Args (o,F₃()) is functional non empty Element of rng ( the Sorts of F₃() #)
the Sorts of F₃() # is Relation-like the carrier of F₁() * -defined Function-like non empty total set
rng ( the Sorts of F₃() #) is non empty set
the Arity of F₁() * ( the Sorts of F₃() #) is Relation-like the carrier' of F₁() -defined Function-like non empty total set
( the Arity of F₁() * ( the Sorts of F₃() #)) . o is set
ts is Relation-like Function-like Element of Args (o,F₃())
[o,ts] is V15() set
{o,ts} is non empty set
{o} is non empty set
{{o,ts},{o}} is non empty set
Result (o,F₃()) is non empty Element of rng the Sorts of F₃()
rng the Sorts of F₃() is non empty V36() set
the ResultSort of F₁() * the Sorts of F₃() is Relation-like non-empty non empty-yielding the carrier' of F₁() -defined Function-like non empty total set
( the ResultSort of F₁() * the Sorts of F₃()) . o is non empty set
Den (o,F₃()) is Relation-like Args (o,F₃()) -defined Result (o,F₃()) -valued Function-like V18( Args (o,F₃()), Result (o,F₃())) Element of bool [:(Args (o,F₃())),(Result (o,F₃())):]
[:(Args (o,F₃())),(Result (o,F₃())):] is Relation-like set
bool [:(Args (o,F₃())),(Result (o,F₃())):] is set
the Charact of F₃() is Relation-like the carrier' of F₁() -defined Function-like non empty total V53() ManySortedFunction of the Arity of F₁() * ( the Sorts of F₃() #), the ResultSort of F₁() * the Sorts of F₃()
the Charact of F₃() . o is set
(Den (o,F₃())) . ts is Element of Result (o,F₃())
x is set
union (rng the Sorts of F₃()) is set
a is Element of the carrier' of F₁()
Args (a,F₃()) is functional non empty Element of rng ( the Sorts of F₃() #)
( the Arity of F₁() * ( the Sorts of F₃() #)) . a is set
Result (a,F₃()) is non empty Element of rng the Sorts of F₃()
( the ResultSort of F₁() * the Sorts of F₃()) . a is non empty set
Den (a,F₃()) is Relation-like Args (a,F₃()) -defined Result (a,F₃()) -valued Function-like V18( Args (a,F₃()), Result (a,F₃())) Element of bool [:(Args (a,F₃())),(Result (a,F₃())):]
[:(Args (a,F₃())),(Result (a,F₃())):] is Relation-like set
bool [:(Args (a,F₃())),(Result (a,F₃())):] is set
the Charact of F₃() . a is set
x9 is Relation-like Function-like Element of Args (a,F₃())
[a,x9] is V15() set
{a,x9} is non empty set
{a} is non empty set
{{a,x9},{a}} is non empty set
(Den (a,F₃())) . x9 is Element of Result (a,F₃())
[:R,(Union the Sorts of F₃()):] is Relation-like set
bool [:R,(Union the Sorts of F₃()):] is set
H is Relation-like R -defined Union the Sorts of F₃() -valued Function-like V18(R, Union the Sorts of F₃()) Element of bool [:R,(Union the Sorts of F₃()):]
f2 is Relation-like the carrier of F₁() -defined Function-like non empty total V53() ManySortedFunction of FreeSort F₂(), the Sorts of F₃()
o is Element of the carrier of F₁()
FreeGen (o,F₂()) is non empty Element of bool ((FreeSort F₂()) . o)
(FreeSort F₂()) . o is non empty set
bool ((FreeSort F₂()) . o) is set
f2 . o is Relation-like (FreeSort F₂()) . o -defined the Sorts of F₃() . o -valued Function-like V18((FreeSort F₂()) . o, the Sorts of F₃() . o) Element of bool [:((FreeSort F₂()) . o),( the Sorts of F₃() . o):]
the Sorts of F₃() . o is non empty set
[:((FreeSort F₂()) . o),( the Sorts of F₃() . o):] is Relation-like set
bool [:((FreeSort F₂()) . o),( the Sorts of F₃() . o):] is set
ts is set
(f2 . o) . ts is set
G /. ts is Element of Union the Sorts of F₃()
dom (FreeGen F₂()) is non empty set
(FreeGen F₂()) . o is set
G . ts is set
(Union the Sorts of F₃()) * is functional non empty FinSequence-membered set
( the carrier of F₁(),(FreeSort F₂()), the Sorts of F₃(),f2) is Relation-like Union (FreeSort F₂()) -defined Union the Sorts of F₃() -valued Function-like V18( Union (FreeSort F₂()), Union the Sorts of F₃()) Element of bool [:(Union (FreeSort F₂())),(Union the Sorts of F₃()):]
Union (FreeSort F₂()) is non empty set
[:(Union (FreeSort F₂())),(Union the Sorts of F₃()):] is Relation-like set
bool [:(Union (FreeSort F₂())),(Union the Sorts of F₃()):] is set
o is Element of the carrier' of F₁()
Args (o,(FreeMSA F₂())) is functional non empty Element of rng ( the Sorts of (FreeMSA F₂()) #)
the Sorts of (FreeMSA F₂()) # is Relation-like the carrier of F₁() * -defined Function-like non empty total set
rng ( the Sorts of (FreeMSA F₂()) #) is non empty set
the Arity of F₁() * ( the Sorts of (FreeMSA F₂()) #) is Relation-like the carrier' of F₁() -defined Function-like non empty total set
( the Arity of F₁() * ( the Sorts of (FreeMSA F₂()) #)) . o is set
the_result_sort_of o is Element of the carrier of F₁()
the ResultSort of F₁() . o is Element of the carrier of F₁()
f2 . (the_result_sort_of o) is Relation-like (FreeSort F₂()) . (the_result_sort_of o) -defined the Sorts of F₃() . (the_result_sort_of o) -valued Function-like V18((FreeSort F₂()) . (the_result_sort_of o), the Sorts of F₃() . (the_result_sort_of o)) Element of bool [:((FreeSort F₂()) . (the_result_sort_of o)),( the Sorts of F₃() . (the_result_sort_of o)):]
(FreeSort F₂()) . (the_result_sort_of o) is non empty set
the Sorts of F₃() . (the_result_sort_of o) is non empty set
[:((FreeSort F₂()) . (the_result_sort_of o)),( the Sorts of F₃() . (the_result_sort_of o)):] is Relation-like set
bool [:((FreeSort F₂()) . (the_result_sort_of o)),( the Sorts of F₃() . (the_result_sort_of o)):] is set
Result (o,(FreeMSA F₂())) is non empty Element of rng the Sorts of (FreeMSA F₂())
rng the Sorts of (FreeMSA F₂()) is non empty V36() set
the ResultSort of F₁() * the Sorts of (FreeMSA F₂()) is Relation-like non-empty non empty-yielding the carrier' of F₁() -defined Function-like non empty total set
( the ResultSort of F₁() * the Sorts of (FreeMSA F₂())) . o is non empty set
Den (o,(FreeMSA F₂())) is Relation-like Args (o,(FreeMSA F₂())) -defined Result (o,(FreeMSA F₂())) -valued Function-like V18( Args (o,(FreeMSA F₂())), Result (o,(FreeMSA F₂()))) Element of bool [:(Args (o,(FreeMSA F₂()))),(Result (o,(FreeMSA F₂()))):]
[:(Args (o,(FreeMSA F₂()))),(Result (o,(FreeMSA F₂()))):] is Relation-like set
bool [:(Args (o,(FreeMSA F₂()))),(Result (o,(FreeMSA F₂()))):] is set
the Charact of (FreeMSA F₂()) is Relation-like the carrier' of F₁() -defined Function-like non empty total V53() ManySortedFunction of the Arity of F₁() * ( the Sorts of (FreeMSA F₂()) #), the ResultSort of F₁() * the Sorts of (FreeMSA F₂())
the Charact of (FreeMSA F₂()) . o is set
ts is Relation-like Function-like Element of Args (o,(FreeMSA F₂()))
ts * ( the carrier of F₁(),(FreeSort F₂()), the Sorts of F₃(),f2) is Relation-like Union the Sorts of F₃() -valued Function-like set
(Den (o,(FreeMSA F₂()))) . ts is Element of Result (o,(FreeMSA F₂()))
(f2 . (the_result_sort_of o)) . ((Den (o,(FreeMSA F₂()))) . ts) is set
x is Relation-like K101() -defined Function-like V31() FinSequence-like FinSubsequence-like Element of (Union the Sorts of F₃()) *
[o,x] is V15() set
{o,x} is non empty set
{o} is non empty set
{{o,x},{o}} is non empty set
H /. [o,x] is Element of Union the Sorts of F₃()
F₅() # ts is Relation-like Function-like Element of Args (o,F₃())
Args (o,F₃()) is functional non empty Element of rng ( the Sorts of F₃() #)
the Sorts of F₃() # is Relation-like the carrier of F₁() * -defined Function-like non empty total set
rng ( the Sorts of F₃() #) is non empty set
the Arity of F₁() * ( the Sorts of F₃() #) is Relation-like the carrier' of F₁() -defined Function-like non empty total set
( the Arity of F₁() * ( the Sorts of F₃() #)) . o is set
a is Relation-like Function-like Element of Args (o,F₃())
[o,a] is V15() set
{o,a} is non empty set
{{o,a},{o}} is non empty set
Result (o,F₃()) is non empty Element of rng the Sorts of F₃()
rng the Sorts of F₃() is non empty V36() set
the ResultSort of F₁() * the Sorts of F₃() is Relation-like non-empty non empty-yielding the carrier' of F₁() -defined Function-like non empty total set
( the ResultSort of F₁() * the Sorts of F₃()) . o is non empty set
Den (o,F₃()) is Relation-like Args (o,F₃()) -defined Result (o,F₃()) -valued Function-like V18( Args (o,F₃()), Result (o,F₃())) Element of bool [:(Args (o,F₃())),(Result (o,F₃())):]
[:(Args (o,F₃())),(Result (o,F₃())):] is Relation-like set
bool [:(Args (o,F₃())),(Result (o,F₃())):] is set
the Charact of F₃() is Relation-like the carrier' of F₁() -defined Function-like non empty total V53() ManySortedFunction of the Arity of F₁() * ( the Sorts of F₃() #), the ResultSort of F₁() * the Sorts of F₃()
the Charact of F₃() . o is set
(Den (o,F₃())) . a is Element of Result (o,F₃())
H . [o,x] is set
( the carrier of F₁(),(FreeSort F₂()), the Sorts of F₃(),f1) is Relation-like Union (FreeSort F₂()) -defined Union the Sorts of F₃() -valued Function-like V18( Union (FreeSort F₂()), Union the Sorts of F₃()) Element of bool [:(Union (FreeSort F₂())),(Union the Sorts of F₃()):]
o is Element of the carrier' of F₁()
Args (o,(FreeMSA F₂())) is functional non empty Element of rng ( the Sorts of (FreeMSA F₂()) #)
the Sorts of (FreeMSA F₂()) # is Relation-like the carrier of F₁() * -defined Function-like non empty total set
rng ( the Sorts of (FreeMSA F₂()) #) is non empty set
the Arity of F₁() * ( the Sorts of (FreeMSA F₂()) #) is Relation-like the carrier' of F₁() -defined Function-like non empty total set
( the Arity of F₁() * ( the Sorts of (FreeMSA F₂()) #)) . o is set
the_result_sort_of o is Element of the carrier of F₁()
the ResultSort of F₁() . o is Element of the carrier of F₁()
f1 . (the_result_sort_of o) is Relation-like (FreeSort F₂()) . (the_result_sort_of o) -defined the Sorts of F₃() . (the_result_sort_of o) -valued Function-like V18((FreeSort F₂()) . (the_result_sort_of o), the Sorts of F₃() . (the_result_sort_of o)) Element of bool [:((FreeSort F₂()) . (the_result_sort_of o)),( the Sorts of F₃() . (the_result_sort_of o)):]
(FreeSort F₂()) . (the_result_sort_of o) is non empty set
the Sorts of F₃() . (the_result_sort_of o) is non empty set
[:((FreeSort F₂()) . (the_result_sort_of o)),( the Sorts of F₃() . (the_result_sort_of o)):] is Relation-like set
bool [:((FreeSort F₂()) . (the_result_sort_of o)),( the Sorts of F₃() . (the_result_sort_of o)):] is set
Result (o,(FreeMSA F₂())) is non empty Element of rng the Sorts of (FreeMSA F₂())
rng the Sorts of (FreeMSA F₂()) is non empty V36() set
the ResultSort of F₁() * the Sorts of (FreeMSA F₂()) is Relation-like non-empty non empty-yielding the carrier' of F₁() -defined Function-like non empty total set
( the ResultSort of F₁() * the Sorts of (FreeMSA F₂())) . o is non empty set
Den (o,(FreeMSA F₂())) is Relation-like Args (o,(FreeMSA F₂())) -defined Result (o,(FreeMSA F₂())) -valued Function-like V18( Args (o,(FreeMSA F₂())), Result (o,(FreeMSA F₂()))) Element of bool [:(Args (o,(FreeMSA F₂()))),(Result (o,(FreeMSA F₂()))):]
[:(Args (o,(FreeMSA F₂()))),(Result (o,(FreeMSA F₂()))):] is Relation-like set
bool [:(Args (o,(FreeMSA F₂()))),(Result (o,(FreeMSA F₂()))):] is set
the Charact of (FreeMSA F₂()) is Relation-like the carrier' of F₁() -defined Function-like non empty total V53() ManySortedFunction of the Arity of F₁() * ( the Sorts of (FreeMSA F₂()) #), the ResultSort of F₁() * the Sorts of (FreeMSA F₂())
the Charact of (FreeMSA F₂()) . o is set
ts is Relation-like Function-like Element of Args (o,(FreeMSA F₂()))
ts * ( the carrier of F₁(),(FreeSort F₂()), the Sorts of F₃(),f1) is Relation-like Union the Sorts of F₃() -valued Function-like set
(Den (o,(FreeMSA F₂()))) . ts is Element of Result (o,(FreeMSA F₂()))
(f1 . (the_result_sort_of o)) . ((Den (o,(FreeMSA F₂()))) . ts) is set
x is Relation-like K101() -defined Function-like V31() FinSequence-like FinSubsequence-like Element of (Union the Sorts of F₃()) *
[o,x] is V15() set
{o,x} is non empty set
{o} is non empty set
{{o,x},{o}} is non empty set
H /. [o,x] is Element of Union the Sorts of F₃()
F₄() # ts is Relation-like Function-like Element of Args (o,F₃())
Args (o,F₃()) is functional non empty Element of rng ( the Sorts of F₃() #)
the Sorts of F₃() # is Relation-like the carrier of F₁() * -defined Function-like non empty total set
rng ( the Sorts of F₃() #) is non empty set
the Arity of F₁() * ( the Sorts of F₃() #) is Relation-like the carrier' of F₁() -defined Function-like non empty total set
( the Arity of F₁() * ( the Sorts of F₃() #)) . o is set
a is Relation-like Function-like Element of Args (o,F₃())
[o,a] is V15() set
{o,a} is non empty set
{{o,a},{o}} is non empty set
Result (o,F₃()) is non empty Element of rng the Sorts of F₃()
rng the Sorts of F₃() is non empty V36() set
the ResultSort of F₁() * the Sorts of F₃() is Relation-like non-empty non empty-yielding the carrier' of F₁() -defined Function-like non empty total set
( the ResultSort of F₁() * the Sorts of F₃()) . o is non empty set
Den (o,F₃()) is Relation-like Args (o,F₃()) -defined Result (o,F₃()) -valued Function-like V18( Args (o,F₃()), Result (o,F₃())) Element of bool [:(Args (o,F₃())),(Result (o,F₃())):]
[:(Args (o,F₃())),(Result (o,F₃())):] is Relation-like set
bool [:(Args (o,F₃())),(Result (o,F₃())):] is set
the Charact of F₃() is Relation-like the carrier' of F₁() -defined Function-like non empty total V53() ManySortedFunction of the Arity of F₁() * ( the Sorts of F₃() #), the ResultSort of F₁() * the Sorts of F₃()
the Charact of F₃() . o is set
(Den (o,F₃())) . a is Element of Result (o,F₃())
H . [o,x] is set