REAL is non empty non trivial non finite complex-membered ext-real-membered real-membered V144() V151() V152() V154() set
NAT is non empty non trivial epsilon-transitive epsilon-connected ordinal non finite cardinal limit_cardinal countable denumerable complex-membered ext-real-membered real-membered rational-membered integer-membered natural-membered V144() V149() V151() Element of bool REAL
bool REAL is non trivial non finite set
omega is non empty non trivial epsilon-transitive epsilon-connected ordinal non finite cardinal limit_cardinal countable denumerable complex-membered ext-real-membered real-membered rational-membered integer-membered natural-membered V144() V149() V151() set
bool omega is non trivial non finite set
bool NAT is non trivial non finite set
{} is Relation-like non-empty empty-yielding NAT -defined Function-like one-to-one constant functional empty epsilon-transitive epsilon-connected ordinal T-Sequence-like c=-linear natural V28() real finite finite-yielding V34() cardinal {} -element FinSequence-like FinSubsequence-like FinSequence-membered Cardinal-yielding countable constituted-Trees constituted-FinTrees constituted-DTrees Tree-yielding FinTree-yielding DTree-yielding ext-real non positive non negative complex-membered ext-real-membered real-membered rational-membered integer-membered natural-membered V144() V151() V152() V153() V154() set
1 is non empty epsilon-transitive epsilon-connected ordinal natural V28() real finite cardinal countable ext-real positive non negative V136() V137() complex-membered ext-real-membered real-membered rational-membered integer-membered natural-membered V149() V150() V151() V152() V153() Element of NAT
{{},1} is non empty finite V34() countable complex-membered ext-real-membered real-membered rational-membered integer-membered natural-membered V149() V150() V151() V152() V153() 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),NAT:] is Relation-like non trivial non finite set
bool [:(TS PeanoNat),NAT:] is non trivial non finite set
[:NAT,(TS PeanoNat):] is Relation-like non trivial non finite set
bool [:NAT,(TS PeanoNat):] is non trivial non finite set
COMPLEX is non empty non trivial non finite complex-membered V144() set
RAT is non empty non trivial non finite complex-membered ext-real-membered real-membered rational-membered V144() set
INT is non empty non trivial non finite complex-membered ext-real-membered real-membered rational-membered integer-membered V144() set
[:COMPLEX,COMPLEX:] is Relation-like non trivial non finite set
bool [:COMPLEX,COMPLEX:] is non trivial non finite set
[:COMPLEX,REAL:] is Relation-like non trivial non finite set
bool [:COMPLEX,REAL:] is non trivial non finite set
2 is non empty epsilon-transitive epsilon-connected ordinal natural V28() real finite cardinal countable ext-real positive non negative V136() V137() complex-membered ext-real-membered real-membered rational-membered integer-membered natural-membered V149() V150() V151() V152() V153() Element of NAT
3 is non empty epsilon-transitive epsilon-connected ordinal natural V28() real finite cardinal countable ext-real positive non negative V136() V137() complex-membered ext-real-membered real-membered rational-membered integer-membered natural-membered V149() V150() V151() V152() V153() Element of NAT
0 is Relation-like non-empty empty-yielding NAT -defined Function-like one-to-one constant functional empty epsilon-transitive epsilon-connected ordinal T-Sequence-like c=-linear natural V28() real finite finite-yielding V34() cardinal {} -element FinSequence-like FinSubsequence-like FinSequence-membered Cardinal-yielding countable constituted-Trees constituted-FinTrees constituted-DTrees Tree-yielding FinTree-yielding DTree-yielding ext-real non positive non negative V136() V137() complex-membered ext-real-membered real-membered rational-membered integer-membered natural-membered V144() V151() V152() V153() V154() Element of NAT
Seg 1 is non empty trivial finite 1 -element countable complex-membered ext-real-membered real-membered rational-membered integer-membered natural-membered V149() V150() V151() V152() V153() Element of bool NAT
{1} is non empty trivial finite V34() 1 -element countable complex-membered ext-real-membered real-membered rational-membered integer-membered natural-membered V149() V150() V151() V152() V153() set
Seg 2 is non empty finite 2 -element countable complex-membered ext-real-membered real-membered rational-membered integer-membered natural-membered V149() V150() V151() V152() V153() Element of bool NAT
{1,2} is non empty finite V34() countable complex-membered ext-real-membered real-membered rational-membered integer-membered natural-membered V149() V150() V151() V152() V153() set
<*> NAT is Relation-like non-empty empty-yielding NAT -defined NAT -valued Function-like one-to-one constant functional empty epsilon-transitive epsilon-connected ordinal T-Sequence-like c=-linear natural V28() real finite finite-yielding V34() cardinal {} -element FinSequence-like FinSubsequence-like FinSequence-membered Cardinal-yielding countable constituted-Trees constituted-FinTrees constituted-DTrees Tree-yielding FinTree-yielding DTree-yielding ext-real non positive non negative complex-membered ext-real-membered real-membered rational-membered integer-membered natural-membered V144() V151() V152() V153() V154() FinSequence of NAT
elementary_tree 0 is non empty finite countable Tree-like set
{{}} is functional non empty trivial finite V34() 1 -element with_common_domain countable Tree-like complex-membered ext-real-membered real-membered rational-membered integer-membered natural-membered V149() V150() V151() V152() V153() set
height (elementary_tree 0) is epsilon-transitive epsilon-connected ordinal natural V28() real finite cardinal countable ext-real non negative V136() V137() complex-membered ext-real-membered real-membered rational-membered integer-membered natural-membered V151() V152() V153() Element of NAT
IIG is non empty non void V51() Circuit-like ManySortedSign
SortsWithConstants IIG is Element of bool the carrier of IIG
the carrier of IIG is non empty set
bool the carrier of IIG is set
A is non-empty finitely-generated finite-yielding MSAlgebra over IIG
{ b1 where b1 is Element of the carrier of IIG : b1 is with_const_op } is set
v1 is set
s1 is Element of the carrier of IIG
Y1 is Element of the carrier of IIG
the carrier' of IIG is non empty set
the Arity of IIG is Relation-like the carrier' of IIG -defined the carrier of IIG * -valued Function-like non empty total V18( the carrier' of IIG, the carrier of IIG * ) Element of bool [: the carrier' of IIG,( the carrier of IIG *):]
the carrier of IIG * is functional non empty FinSequence-membered M11( the carrier of IIG)
[: the carrier' of IIG,( the carrier of IIG *):] is Relation-like set
bool [: the carrier' of IIG,( the carrier of IIG *):] is set
the ResultSort of IIG is Relation-like the carrier' of IIG -defined the carrier of IIG -valued Function-like non empty total V18( the carrier' of IIG, the carrier of IIG) Element of bool [: the carrier' of IIG, the carrier of IIG:]
[: the carrier' of IIG, the carrier of IIG:] is Relation-like set
bool [: the carrier' of IIG, the carrier of IIG:] is set
t1 is Element of the carrier' of IIG
the Arity of IIG . t1 is Relation-like NAT -defined Function-like finite FinSequence-like FinSubsequence-like countable set
the ResultSort of IIG . t1 is set
dom the ResultSort of IIG is non empty Element of bool the carrier' of IIG
bool the carrier' of IIG is set
Result (t1,A) is non empty Element of rng the Sorts of A
the Sorts of A is Relation-like non-empty non empty-yielding the carrier of IIG -defined Function-like non empty total set
rng the Sorts of A is non empty set
Den (t1,A) is Relation-like Args (t1,A) -defined Result (t1,A) -valued Function-like non empty total V18( Args (t1,A), Result (t1,A)) Element of bool [:(Args (t1,A)),(Result (t1,A)):]
Args (t1,A) is non empty Element of rng ( the Sorts of A #)
the Sorts of A # is Relation-like the carrier of IIG * -defined Function-like non empty total set
rng ( the Sorts of A #) is non empty set
[:(Args (t1,A)),(Result (t1,A)):] is Relation-like set
bool [:(Args (t1,A)),(Result (t1,A)):] is set
rng (Den (t1,A)) is non empty Element of bool (Result (t1,A))
bool (Result (t1,A)) is set
the Element of rng (Den (t1,A)) is Element of rng (Den (t1,A))
the ResultSort of IIG * the Sorts of A is Relation-like non-empty non empty-yielding the carrier' of IIG -defined Function-like non empty total set
( the ResultSort of IIG * the Sorts of A) . t1 is non empty set
the Sorts of A . ( the ResultSort of IIG . t1) is set
the Sorts of A . Y1 is non empty set
x is set
Constants (A,Y1) is Element of bool ( the Sorts of A . Y1)
bool ( the Sorts of A . Y1) is set
s is Element of the Sorts of A . Y1
Constants (A,s1) is Element of bool ( the Sorts of A . s1)
the Sorts of A . s1 is non empty set
bool ( the Sorts of A . s1) is set
t is non empty set
{ b1 where b1 is Element of t : ex b2 being Element of the carrier' of IIG st
( the Arity of IIG . b2 = {} & the ResultSort of IIG . b2 = Y1 & b1 in rng (Den (b2,A)) ) } is set
Y is set
v1 is Relation-like SortsWithConstants IIG -defined Function-like total set
dom v1 is Element of bool (SortsWithConstants IIG)
bool (SortsWithConstants IIG) is set
s1 is Element of the carrier of IIG
v1 . s1 is set
Constants (A,s1) is Element of bool ( the Sorts of A . s1)
the Sorts of A . s1 is non empty set
bool ( the Sorts of A . s1) is set
Y1 is Element of the carrier of IIG
Constants (A,Y1) is Element of bool ( the Sorts of A . Y1)
the Sorts of A . Y1 is non empty set
bool ( the Sorts of A . Y1) is set
v is Relation-like SortsWithConstants IIG -defined Function-like total set
dom v is Element of bool (SortsWithConstants IIG)
bool (SortsWithConstants IIG) is set
v1 is Relation-like SortsWithConstants IIG -defined Function-like total set
dom v1 is Element of bool (SortsWithConstants IIG)
the carrier' of IIG is non empty set
the Arity of IIG is Relation-like the carrier' of IIG -defined the carrier of IIG * -valued Function-like non empty total V18( the carrier' of IIG, the carrier of IIG * ) Element of bool [: the carrier' of IIG,( the carrier of IIG *):]
the carrier of IIG * is functional non empty FinSequence-membered M11( the carrier of IIG)
[: the carrier' of IIG,( the carrier of IIG *):] is Relation-like set
bool [: the carrier' of IIG,( the carrier of IIG *):] is set
dom the Arity of IIG is non empty Element of bool the carrier' of IIG
bool the carrier' of IIG is set
s1 is set
the Sorts of A is Relation-like non-empty non empty-yielding the carrier of IIG -defined Function-like non empty total set
Y1 is Element of the carrier of IIG
the Sorts of A . Y1 is non empty set
Constants (A,Y1) is Element of bool ( the Sorts of A . Y1)
bool ( the Sorts of A . Y1) is set
the ResultSort of IIG is Relation-like the carrier' of IIG -defined the carrier of IIG -valued Function-like non empty total V18( the carrier' of IIG, the carrier of IIG) Element of bool [: the carrier' of IIG, the carrier of IIG:]
[: the carrier' of IIG, the carrier of IIG:] is Relation-like set
bool [: the carrier' of IIG, the carrier of IIG:] is set
v1 . Y1 is set
t1 is non empty set
{ b1 where b1 is Element of t1 : ex b2 being Element of the carrier' of IIG st
( the Arity of IIG . b2 = {} & the ResultSort of IIG . b2 = Y1 & b1 in rng (Den (b2,A)) ) } is set
t1 is Element of the Sorts of A . Y1
av is Element of the carrier' of IIG
the Arity of IIG . av is Relation-like NAT -defined Function-like finite FinSequence-like FinSubsequence-like countable set
the ResultSort of IIG . av is set
Result (av,A) is non empty Element of rng the Sorts of A
rng the Sorts of A is non empty set
Den (av,A) is Relation-like Args (av,A) -defined Result (av,A) -valued Function-like non empty total V18( Args (av,A), Result (av,A)) Element of bool [:(Args (av,A)),(Result (av,A)):]
Args (av,A) is non empty Element of rng ( the Sorts of A #)
the Sorts of A # is Relation-like the carrier of IIG * -defined Function-like non empty total set
rng ( the Sorts of A #) is non empty set
[:(Args (av,A)),(Result (av,A)):] is Relation-like set
bool [:(Args (av,A)),(Result (av,A)):] is set
rng (Den (av,A)) is non empty Element of bool (Result (av,A))
bool (Result (av,A)) is set
av is Element of the carrier' of IIG
the Arity of IIG . av is Relation-like NAT -defined Function-like finite FinSequence-like FinSubsequence-like countable set
the ResultSort of IIG . av is set
Result (av,A) is non empty Element of rng the Sorts of A
rng the Sorts of A is non empty set
Den (av,A) is Relation-like Args (av,A) -defined Result (av,A) -valued Function-like non empty total V18( Args (av,A), Result (av,A)) Element of bool [:(Args (av,A)),(Result (av,A)):]
Args (av,A) is non empty Element of rng ( the Sorts of A #)
the Sorts of A # is Relation-like the carrier of IIG * -defined Function-like non empty total set
rng ( the Sorts of A #) is non empty set
[:(Args (av,A)),(Result (av,A)):] is Relation-like set
bool [:(Args (av,A)),(Result (av,A)):] is set
rng (Den (av,A)) is non empty Element of bool (Result (av,A))
bool (Result (av,A)) is set
the_result_sort_of av is Element of the carrier of IIG
v . Y1 is set
s is non empty set
{ b1 where b1 is Element of s : ex b2 being Element of the carrier' of IIG st
( the Arity of IIG . b2 = {} & the ResultSort of IIG . b2 = Y1 & b1 in rng (Den (b2,A)) ) } is set
s is Element of the Sorts of A . Y1
x is Element of the carrier' of IIG
the Arity of IIG . x is Relation-like NAT -defined Function-like finite FinSequence-like FinSubsequence-like countable set
the ResultSort of IIG . x is set
Result (x,A) is non empty Element of rng the Sorts of A
Den (x,A) is Relation-like Args (x,A) -defined Result (x,A) -valued Function-like non empty total V18( Args (x,A), Result (x,A)) Element of bool [:(Args (x,A)),(Result (x,A)):]
Args (x,A) is non empty Element of rng ( the Sorts of A #)
[:(Args (x,A)),(Result (x,A)):] is Relation-like set
bool [:(Args (x,A)),(Result (x,A)):] is set
rng (Den (x,A)) is non empty Element of bool (Result (x,A))
bool (Result (x,A)) is set
x is Element of the carrier' of IIG
the Arity of IIG . x is Relation-like NAT -defined Function-like finite FinSequence-like FinSubsequence-like countable set
the ResultSort of IIG . x is set
Result (x,A) is non empty Element of rng the Sorts of A
Den (x,A) is Relation-like Args (x,A) -defined Result (x,A) -valued Function-like non empty total V18( Args (x,A), Result (x,A)) Element of bool [:(Args (x,A)),(Result (x,A)):]
Args (x,A) is non empty Element of rng ( the Sorts of A #)
[:(Args (x,A)),(Result (x,A)):] is Relation-like set
bool [:(Args (x,A)),(Result (x,A)):] is set
rng (Den (x,A)) is non empty Element of bool (Result (x,A))
bool (Result (x,A)) is set
<*> the carrier of IIG is Relation-like non-empty empty-yielding NAT -defined the carrier of IIG -valued Function-like one-to-one constant functional empty epsilon-transitive epsilon-connected ordinal T-Sequence-like c=-linear natural V28() real finite finite-yielding V34() cardinal {} -element FinSequence-like FinSubsequence-like FinSequence-membered Cardinal-yielding countable constituted-Trees constituted-FinTrees constituted-DTrees Tree-yielding FinTree-yielding DTree-yielding ext-real non positive non negative complex-membered ext-real-membered real-membered rational-membered integer-membered natural-membered V144() V151() V152() V153() V154() FinSequence of the carrier of IIG
dom (Den (av,A)) is non empty Element of bool (Args (av,A))
bool (Args (av,A)) is set
the_result_sort_of x is Element of the carrier of IIG
dom (Den (x,A)) is non empty Element of bool (Args (x,A))
bool (Args (x,A)) is set
Y is set
(Den (x,A)) . Y is set
the Arity of IIG * ( the Sorts of A #) is Relation-like the carrier' of IIG -defined Function-like non empty total set
( the Arity of IIG * ( the Sorts of A #)) . x is set
( the Sorts of A #) . ( the Arity of IIG . x) is set
v . s1 is set
v1 . s1 is set
t is set
(Den (av,A)) . t is set
IIG is non empty non void V51() Circuit-like ManySortedSign
the carrier of IIG is non empty set
SortsWithConstants IIG is Element of bool the carrier of IIG
bool the carrier of IIG is set
A is non-empty finitely-generated finite-yielding MSAlgebra over IIG
the Sorts of A is Relation-like non-empty non empty-yielding the carrier of IIG -defined Function-like non empty total set
(IIG,A) is Relation-like SortsWithConstants IIG -defined Function-like total set
v is Element of the carrier of IIG
the Sorts of A . v is non empty set
Constants (A,v) is Element of bool ( the Sorts of A . v)
bool ( the Sorts of A . v) is set
(IIG,A) . v is set
v1 is Element of the Sorts of A . v
the carrier' of IIG is non empty set
the Arity of IIG is Relation-like the carrier' of IIG -defined the carrier of IIG * -valued Function-like non empty total V18( the carrier' of IIG, the carrier of IIG * ) Element of bool [: the carrier' of IIG,( the carrier of IIG *):]
the carrier of IIG * is functional non empty FinSequence-membered M11( the carrier of IIG)
[: the carrier' of IIG,( the carrier of IIG *):] is Relation-like set
bool [: the carrier' of IIG,( the carrier of IIG *):] is set
the ResultSort of IIG is Relation-like the carrier' of IIG -defined the carrier of IIG -valued Function-like non empty total V18( the carrier' of IIG, the carrier of IIG) Element of bool [: the carrier' of IIG, the carrier of IIG:]
[: the carrier' of IIG, the carrier of IIG:] is Relation-like set
bool [: the carrier' of IIG, the carrier of IIG:] is set
s1 is non empty set
{ b1 where b1 is Element of s1 : ex b2 being Element of the carrier' of IIG st
( the Arity of IIG . b2 = {} & the ResultSort of IIG . b2 = v & b1 in rng (Den (b2,A)) ) } is set
s1 is Element of the Sorts of A . v
Y1 is Element of the carrier' of IIG
the Arity of IIG . Y1 is Relation-like NAT -defined Function-like finite FinSequence-like FinSubsequence-like countable set
the ResultSort of IIG . Y1 is set
Result (Y1,A) is non empty Element of rng the Sorts of A
rng the Sorts of A is non empty set
Den (Y1,A) is Relation-like Args (Y1,A) -defined Result (Y1,A) -valued Function-like non empty total V18( Args (Y1,A), Result (Y1,A)) Element of bool [:(Args (Y1,A)),(Result (Y1,A)):]
Args (Y1,A) is non empty Element of rng ( the Sorts of A #)
the Sorts of A # is Relation-like the carrier of IIG * -defined Function-like non empty total set
rng ( the Sorts of A #) is non empty set
[:(Args (Y1,A)),(Result (Y1,A)):] is Relation-like set
bool [:(Args (Y1,A)),(Result (Y1,A)):] is set
rng (Den (Y1,A)) is non empty Element of bool (Result (Y1,A))
bool (Result (Y1,A)) is set
s1 is Element of the carrier' of IIG
the Arity of IIG . s1 is Relation-like NAT -defined Function-like finite FinSequence-like FinSubsequence-like countable set
the ResultSort of IIG . s1 is set
Result (s1,A) is non empty Element of rng the Sorts of A
rng the Sorts of A is non empty set
Den (s1,A) is Relation-like Args (s1,A) -defined Result (s1,A) -valued Function-like non empty total V18( Args (s1,A), Result (s1,A)) Element of bool [:(Args (s1,A)),(Result (s1,A)):]
Args (s1,A) is non empty Element of rng ( the Sorts of A #)
the Sorts of A # is Relation-like the carrier of IIG * -defined Function-like non empty total set
rng ( the Sorts of A #) is non empty set
[:(Args (s1,A)),(Result (s1,A)):] is Relation-like set
bool [:(Args (s1,A)),(Result (s1,A)):] is set
rng (Den (s1,A)) is non empty Element of bool (Result (s1,A))
bool (Result (s1,A)) is set
<*> the carrier of IIG is Relation-like non-empty empty-yielding NAT -defined the carrier of IIG -valued Function-like one-to-one constant functional empty epsilon-transitive epsilon-connected ordinal T-Sequence-like c=-linear natural V28() real finite finite-yielding V34() cardinal {} -element FinSequence-like FinSubsequence-like FinSequence-membered Cardinal-yielding countable constituted-Trees constituted-FinTrees constituted-DTrees Tree-yielding FinTree-yielding DTree-yielding ext-real non positive non negative complex-membered ext-real-membered real-membered rational-membered integer-membered natural-membered V144() V151() V152() V153() V154() FinSequence of the carrier of IIG
dom (IIG,A) is Element of bool (SortsWithConstants IIG)
bool (SortsWithConstants IIG) is set
Y1 is non empty set
{ b1 where b1 is Element of Y1 : ex b2 being Element of the carrier' of IIG st
( the Arity of IIG . b2 = {} & the ResultSort of IIG . b2 = v & b1 in rng (Den (b2,A)) ) } is set
Y1 is Element of the Sorts of A . v
t1 is Element of the carrier' of IIG
the Arity of IIG . t1 is Relation-like NAT -defined Function-like finite FinSequence-like FinSubsequence-like countable set
the ResultSort of IIG . t1 is set
Result (t1,A) is non empty Element of rng the Sorts of A
Den (t1,A) is Relation-like Args (t1,A) -defined Result (t1,A) -valued Function-like non empty total V18( Args (t1,A), Result (t1,A)) Element of bool [:(Args (t1,A)),(Result (t1,A)):]
Args (t1,A) is non empty Element of rng ( the Sorts of A #)
[:(Args (t1,A)),(Result (t1,A)):] is Relation-like set
bool [:(Args (t1,A)),(Result (t1,A)):] is set
rng (Den (t1,A)) is non empty Element of bool (Result (t1,A))
bool (Result (t1,A)) is set
Y1 is Element of the carrier' of IIG
the Arity of IIG . Y1 is Relation-like NAT -defined Function-like finite FinSequence-like FinSubsequence-like countable set
the ResultSort of IIG . Y1 is set
Result (Y1,A) is non empty Element of rng the Sorts of A
Den (Y1,A) is Relation-like Args (Y1,A) -defined Result (Y1,A) -valued Function-like non empty total V18( Args (Y1,A), Result (Y1,A)) Element of bool [:(Args (Y1,A)),(Result (Y1,A)):]
Args (Y1,A) is non empty Element of rng ( the Sorts of A #)
[:(Args (Y1,A)),(Result (Y1,A)):] is Relation-like set
bool [:(Args (Y1,A)),(Result (Y1,A)):] is set
rng (Den (Y1,A)) is non empty Element of bool (Result (Y1,A))
bool (Result (Y1,A)) is set
dom (Den (Y1,A)) is non empty Element of bool (Args (Y1,A))
bool (Args (Y1,A)) is set
the_result_sort_of s1 is Element of the carrier of IIG
the_result_sort_of Y1 is Element of the carrier of IIG
dom (Den (s1,A)) is non empty Element of bool (Args (s1,A))
bool (Args (s1,A)) is set
t1 is set
(Den (s1,A)) . t1 is set
dom the Arity of IIG is non empty Element of bool the carrier' of IIG
bool the carrier' of IIG is set
the Arity of IIG * ( the Sorts of A #) is Relation-like the carrier' of IIG -defined Function-like non empty total set
( the Arity of IIG * ( the Sorts of A #)) . s1 is set
( the Sorts of A #) . ( the Arity of IIG . s1) is set
av is set
(Den (Y1,A)) . av is set
IIG is non empty non void V51() Circuit-like ManySortedSign
IIG is non empty non void V51() Circuit-like ManySortedSign
InputVertices IIG is Element of bool the carrier of IIG
the carrier of IIG is non empty set
bool the carrier of IIG is set
the ResultSort of IIG is Relation-like the carrier' of IIG -defined the carrier of IIG -valued Function-like non empty total V18( the carrier' of IIG, the carrier of IIG) Element of bool [: the carrier' of IIG, the carrier of IIG:]
the carrier' of IIG is non empty set
[: the carrier' of IIG, the carrier of IIG:] is Relation-like set
bool [: the carrier' of IIG, the carrier of IIG:] is set
rng the ResultSort of IIG is non empty Element of bool the carrier of IIG
the carrier of IIG \ (rng the ResultSort of IIG) is Element of bool the carrier of IIG
(InputVertices IIG) --> NAT is Relation-like InputVertices IIG -defined {NAT} -valued Function-like total V18( InputVertices IIG,{NAT}) Cardinal-yielding Element of bool [:(InputVertices IIG),{NAT}:]
{NAT} is non empty trivial finite 1 -element countable set
[:(InputVertices IIG),{NAT}:] is Relation-like set
bool [:(InputVertices IIG),{NAT}:] is set
A is non-empty finitely-generated finite-yielding MSAlgebra over IIG
the Sorts of A is Relation-like non-empty non empty-yielding the carrier of IIG -defined Function-like non empty total set
the Sorts of A | (InputVertices IIG) is Relation-like non-empty InputVertices IIG -defined the carrier of IIG -defined InputVertices IIG -defined Function-like total set
v is Relation-like InputVertices IIG -defined Function-like total Function-yielding ManySortedFunction of (InputVertices IIG) --> NAT, the Sorts of A | (InputVertices IIG)
commute v is Relation-like Function-like Function-yielding set
v1 is epsilon-transitive epsilon-connected ordinal natural V28() real finite cardinal countable ext-real non negative V136() V137() complex-membered ext-real-membered real-membered rational-membered integer-membered natural-membered V151() V152() V153() Element of NAT
(commute v) . v1 is set
s1 is Element of bool the carrier of IIG
t1 is non empty Element of bool the carrier of IIG
Y1 is Relation-like non-empty non empty-yielding the carrier of IIG -defined Function-like non empty total set
Y1 | t1 is Relation-like non-empty the carrier of IIG -defined t1 -defined the carrier of IIG -defined Function-like non empty total set
av is Relation-like t1 -defined Function-like non empty total set
s is Relation-like non-empty non empty-yielding t1 -defined Function-like non empty total set
x is Relation-like t1 -defined Function-like non empty total set
Y is Element of the carrier of IIG
s . Y is set
the Sorts of A . Y is non empty set
x . Y is set
IIG is non empty non void V51() Circuit-like ManySortedSign
InputVertices IIG is Element of bool the carrier of IIG
the carrier of IIG is non empty set
bool the carrier of IIG is set
the ResultSort of IIG is Relation-like the carrier' of IIG -defined the carrier of IIG -valued Function-like non empty total V18( the carrier' of IIG, the carrier of IIG) Element of bool [: the carrier' of IIG, the carrier of IIG:]
the carrier' of IIG is non empty set
[: the carrier' of IIG, the carrier of IIG:] is Relation-like set
bool [: the carrier' of IIG, the carrier of IIG:] is set
rng the ResultSort of IIG is non empty Element of bool the carrier of IIG
the carrier of IIG \ (rng the ResultSort of IIG) is Element of bool the carrier of IIG
(InputVertices IIG) --> NAT is Relation-like InputVertices IIG -defined {NAT} -valued Function-like total V18( InputVertices IIG,{NAT}) Cardinal-yielding Element of bool [:(InputVertices IIG),{NAT}:]
{NAT} is non empty trivial finite 1 -element countable set
[:(InputVertices IIG),{NAT}:] is Relation-like set
bool [:(InputVertices IIG),{NAT}:] is set
A is non-empty finitely-generated finite-yielding MSAlgebra over IIG
the Sorts of A is Relation-like non-empty non empty-yielding the carrier of IIG -defined Function-like non empty total set
the Sorts of A | (InputVertices IIG) is Relation-like non-empty InputVertices IIG -defined the carrier of IIG -defined InputVertices IIG -defined Function-like total set
v is Relation-like InputVertices IIG -defined Function-like total Function-yielding ManySortedFunction of (InputVertices IIG) --> NAT, the Sorts of A | (InputVertices IIG)
commute v is Relation-like Function-like Function-yielding set
v1 is epsilon-transitive epsilon-connected ordinal natural V28() real finite cardinal countable ext-real non negative V136() V137() complex-membered ext-real-membered real-membered rational-membered integer-membered natural-membered V151() V152() V153() Element of NAT
(commute v) . v1 is set
IIG is non empty non void V51() Circuit-like ManySortedSign
IIG is non empty non void V51() Circuit-like ManySortedSign
the carrier of IIG is non empty set
A is non-empty finitely-generated finite-yielding MSAlgebra over IIG
the Sorts of A is Relation-like non-empty non empty-yielding the carrier of IIG -defined Function-like non empty total set
product the Sorts of A is functional non empty with_common_domain product-like set
v is Relation-like the carrier of IIG -defined Function-like the Sorts of A -compatible non empty total Element of product the Sorts of A
dom v is non empty Element of bool the carrier of IIG
bool the carrier of IIG is set
IIG is non empty non void V51() Circuit-like ManySortedSign
the carrier of IIG is non empty set
A is non-empty finitely-generated finite-yielding MSAlgebra over IIG
the Sorts of A is Relation-like non-empty non empty-yielding the carrier of IIG -defined Function-like non empty total set
product the Sorts of A is functional non empty with_common_domain product-like set
v is Relation-like the carrier of IIG -defined Function-like the Sorts of A -compatible non empty total Element of product the Sorts of A
v1 is Element of the carrier of IIG
v . v1 is set
the Sorts of A . v1 is non empty set
dom the Sorts of A is non empty Element of bool the carrier of IIG
bool the carrier of IIG is set
s1 is Relation-like Function-like set
dom s1 is set
IIG is non empty non void V51() Circuit-like ManySortedSign
the carrier of IIG is non empty set
A is non-empty finitely-generated finite-yielding MSAlgebra over IIG
the Sorts of A is Relation-like non-empty non empty-yielding the carrier of IIG -defined Function-like non empty total set
product the Sorts of A is functional non empty with_common_domain product-like set
the carrier' of IIG is non empty set
v1 is Element of the carrier' of IIG
the_arity_of v1 is Relation-like NAT -defined the carrier of IIG -valued Function-like finite FinSequence-like FinSubsequence-like countable Element of the carrier of IIG *
the carrier of IIG * is functional non empty FinSequence-membered M11( the carrier of IIG)
v is Relation-like the carrier of IIG -defined Function-like the Sorts of A -compatible non empty total Element of product the Sorts of A
(the_arity_of v1) * v is Relation-like NAT -defined Function-like finite countable set
Args (v1,A) is non empty Element of rng ( the Sorts of A #)
the Sorts of A # is Relation-like the carrier of IIG * -defined Function-like non empty total set
rng ( the Sorts of A #) is non empty set
(the_arity_of v1) * the Sorts of A is Relation-like non-empty NAT -defined Function-like finite countable set
product ((the_arity_of v1) * the Sorts of A) is functional non empty with_common_domain product-like set
IIG is non empty non void V51() Circuit-like monotonic ManySortedSign
the carrier of IIG is non empty set
InnerVertices IIG is non empty Element of bool the carrier of IIG
bool the carrier of IIG is set
the ResultSort of IIG is Relation-like the carrier' of IIG -defined the carrier of IIG -valued Function-like non empty total V18( the carrier' of IIG, the carrier of IIG) Element of bool [: the carrier' of IIG, the carrier of IIG:]
the carrier' of IIG is non empty set
[: the carrier' of IIG, the carrier of IIG:] is Relation-like set
bool [: the carrier' of IIG, the carrier of IIG:] is set
rng the ResultSort of IIG is non empty Element of bool the carrier of IIG
A is non-empty finitely-generated finite-yielding MSAlgebra over IIG
FreeEnv A is strict non-empty V117(IIG) MSAlgebra over IIG
the Sorts of A is Relation-like non-empty non empty-yielding the carrier of IIG -defined Function-like non empty total set
FreeMSA the Sorts of A is strict non-empty MSAlgebra over IIG
the Sorts of (FreeEnv A) is Relation-like non-empty non empty-yielding the carrier of IIG -defined Function-like non empty total set
v is Element of the carrier of IIG
the Sorts of (FreeEnv A) . v is non empty set
action_at v is Element of the carrier' of IIG
[(action_at v), the carrier of IIG] is set
{(action_at v), the carrier of IIG} is non empty finite countable set
{(action_at v)} is non empty trivial finite 1 -element countable set
{{(action_at v), the carrier of IIG},{(action_at v)}} is non empty finite V34() countable set
v1 is Element of the carrier of IIG
the Sorts of (FreeEnv A) . v1 is non empty set
the_arity_of (action_at v) is Relation-like NAT -defined the carrier of IIG -valued Function-like finite FinSequence-like FinSubsequence-like countable Element of the carrier of IIG *
the carrier of IIG * is functional non empty FinSequence-membered M11( the carrier of IIG)
s1 is Element of the Sorts of (FreeEnv A) . v
Y1 is Relation-like NAT -defined Function-like finite FinSequence-like FinSubsequence-like countable DTree-yielding set
[(action_at v), the carrier of IIG] -tree Y1 is Relation-like Function-like DecoratedTree-like set
dom Y1 is finite countable complex-membered ext-real-membered real-membered rational-membered integer-membered natural-membered V151() V152() V153() Element of bool NAT
av is epsilon-transitive epsilon-connected ordinal natural V28() real finite cardinal countable ext-real non negative V136() V137() complex-membered ext-real-membered real-membered rational-membered integer-membered natural-membered V151() V152() V153() Element of NAT
Y1 . av is set
(the_arity_of (action_at v)) /. av is Element of the carrier of IIG
FreeSort the Sorts of A is Relation-like non-empty non empty-yielding the carrier of IIG -defined Function-like non empty total set
FreeOper the Sorts of A is Relation-like the carrier' of IIG -defined Function-like non empty total Function-yielding ManySortedFunction of the Arity of IIG * ((FreeSort the Sorts of A) #), the ResultSort of IIG * (FreeSort the Sorts of A)
the Arity of IIG is Relation-like the carrier' of IIG -defined the carrier of IIG * -valued Function-like non empty total V18( the carrier' of IIG, the carrier of IIG * ) Element of bool [: the carrier' of IIG,( the carrier of IIG *):]
[: the carrier' of IIG,( the carrier of IIG *):] is Relation-like set
bool [: the carrier' of IIG,( the carrier of IIG *):] is set
(FreeSort the Sorts of A) # is Relation-like the carrier of IIG * -defined Function-like non empty total set
the Arity of IIG * ((FreeSort the Sorts of A) #) is Relation-like the carrier' of IIG -defined Function-like non empty total set
the ResultSort of IIG * (FreeSort the Sorts of A) is Relation-like non-empty non empty-yielding the carrier' of IIG -defined Function-like non empty total set
MSAlgebra(# (FreeSort the Sorts of A),(FreeOper the Sorts of A) #) is strict MSAlgebra over IIG
t1 is Element of the carrier' of IIG
the_result_sort_of t1 is Element of the carrier of IIG
the Sorts of (FreeEnv A) . (the_result_sort_of t1) is non empty set
len Y1 is epsilon-transitive epsilon-connected ordinal natural V28() real finite cardinal countable ext-real non negative V136() V137() complex-membered ext-real-membered real-membered rational-membered integer-membered natural-membered V151() V152() V153() Element of NAT
the_arity_of t1 is Relation-like NAT -defined the carrier of IIG -valued Function-like finite FinSequence-like FinSubsequence-like countable Element of the carrier of IIG *
len (the_arity_of t1) is epsilon-transitive epsilon-connected ordinal natural V28() real finite cardinal countable ext-real non negative V136() V137() complex-membered ext-real-membered real-membered rational-membered integer-membered natural-membered V151() V152() V153() Element of NAT
dom (the_arity_of t1) is finite countable complex-membered ext-real-membered real-membered rational-membered integer-membered natural-membered V151() V152() V153() Element of bool NAT
(the_arity_of t1) . av is set
the Sorts of (FreeEnv A) . ((the_arity_of t1) . av) is set
(the_arity_of t1) /. av is Element of the carrier of IIG
(FreeSort the Sorts of A) . ((the_arity_of t1) /. av) is non empty set
(FreeSort the Sorts of A) . v1 is non empty set
((FreeSort the Sorts of A) . ((the_arity_of t1) /. av)) /\ ((FreeSort the Sorts of A) . v1) is set
IIG is non empty non void V51() Circuit-like monotonic ManySortedSign
the carrier of IIG is non empty set
A is non-empty finitely-generated finite-yielding MSAlgebra over IIG
FreeEnv A is strict non-empty V117(IIG) MSAlgebra over IIG
the Sorts of A is Relation-like non-empty non empty-yielding the carrier of IIG -defined Function-like non empty total set
FreeMSA the Sorts of A is strict non-empty MSAlgebra over IIG
the Sorts of (FreeEnv A) is Relation-like non-empty non empty-yielding the carrier of IIG -defined Function-like non empty total set
v is Element of the carrier of IIG
the Sorts of (FreeEnv A) . v is non empty set
v1 is Element of the Sorts of (FreeEnv A) . v
s1 is Element of the Sorts of (FreeEnv A) . v
Y1 is Element of the Sorts of (FreeEnv A) . v
t1 is Element of the Sorts of (FreeEnv A) . v
IIG is non empty non void V51() Circuit-like monotonic ManySortedSign
the carrier of IIG is non empty set
A is non-empty finitely-generated finite-yielding MSAlgebra over IIG
FreeEnv A is strict non-empty V117(IIG) MSAlgebra over IIG
the Sorts of A is Relation-like non-empty non empty-yielding the carrier of IIG -defined Function-like non empty total set
FreeMSA the Sorts of A is strict non-empty MSAlgebra over IIG
the Sorts of (FreeEnv A) is Relation-like non-empty non empty-yielding the carrier of IIG -defined Function-like non empty total set
v is Element of the carrier of IIG
the Sorts of (FreeEnv A) . v is non empty set
v1 is Relation-like Function-like non empty finite countable Element of the Sorts of (FreeEnv A) . v
A is non empty non void V51() Circuit-like monotonic ManySortedSign
the carrier of A is non empty set
InnerVertices A is non empty Element of bool the carrier of A
bool the carrier of A is set
the ResultSort of A is Relation-like the carrier' of A -defined the carrier of A -valued Function-like non empty total V18( the carrier' of A, the carrier of A) Element of bool [: the carrier' of A, the carrier of A:]
the carrier' of A is non empty set
[: the carrier' of A, the carrier of A:] is Relation-like set
bool [: the carrier' of A, the carrier of A:] is set
rng the ResultSort of A is non empty Element of bool the carrier of A
SortsWithConstants A is Element of bool the carrier of A
(InnerVertices A) \ (SortsWithConstants A) is Element of bool the carrier of A
v is non-empty finitely-generated finite-yielding MSAlgebra over A
FreeEnv v is strict non-empty V117(A) MSAlgebra over A
the Sorts of v is Relation-like non-empty non empty-yielding the carrier of A -defined Function-like non empty total set
FreeMSA the Sorts of v is strict non-empty MSAlgebra over A
the Sorts of (FreeEnv v) is Relation-like non-empty non empty-yielding the carrier of A -defined Function-like non empty total set
v1 is Element of the carrier of A
the Sorts of (FreeEnv v) . v1 is non empty set
s1 is Element of the carrier of A
the Sorts of (FreeEnv v) . s1 is non empty set
action_at v1 is Element of the carrier' of A
[(action_at v1), the carrier of A] is set
{(action_at v1), the carrier of A} is non empty finite countable set
{(action_at v1)} is non empty trivial finite 1 -element countable set
{{(action_at v1), the carrier of A},{(action_at v1)}} is non empty finite V34() countable set
Y1 is Relation-like Function-like non empty finite countable DecoratedTree-like Element of the Sorts of (FreeEnv v) . v1
t1 is Relation-like Function-like non empty finite countable DecoratedTree-like Element of the Sorts of (FreeEnv v) . s1
av is Relation-like NAT -defined Function-like finite FinSequence-like FinSubsequence-like countable DTree-yielding set
[(action_at v1), the carrier of A] -tree av is Relation-like Function-like DecoratedTree-like set
dom av is finite countable complex-membered ext-real-membered real-membered rational-membered integer-membered natural-membered V151() V152() V153() Element of bool NAT
s is epsilon-transitive epsilon-connected ordinal natural V28() real finite cardinal countable ext-real non negative V136() V137() complex-membered ext-real-membered real-membered rational-membered integer-membered natural-membered V151() V152() V153() Element of NAT
s + 1 is non empty epsilon-transitive epsilon-connected ordinal natural V28() real finite cardinal countable ext-real positive non negative V136() V137() complex-membered ext-real-membered real-membered rational-membered integer-membered natural-membered V149() V150() V151() V152() V153() Element of NAT
av . (s + 1) is set
<*s*> is Relation-like NAT -defined NAT -valued Function-like constant non empty trivial finite 1 -element FinSequence-like FinSubsequence-like countable FinSequence of NAT
Y1 with-replacement (<*s*>,t1) is Relation-like Function-like DecoratedTree-like set
{ the carrier of A} is non empty trivial finite 1 -element countable set
[: the carrier' of A,{ the carrier of A}:] is Relation-like set
coprod the Sorts of v is Relation-like non-empty non empty-yielding the carrier of A -defined Function-like non empty total set
Union (coprod the Sorts of v) is non empty set
[: the carrier' of A,{ the carrier of A}:] \/ (Union (coprod the Sorts of v)) is non empty set
t is non empty set
t * is functional non empty FinSequence-membered M11(t)
[:t,(t *):] is Relation-like set
bool [:t,(t *):] is set
REL the Sorts of v is Relation-like [: the carrier' of A,{ the carrier of A}:] \/ (Union (coprod the Sorts of v)) -defined ([: the carrier' of A,{ the carrier of A}:] \/ (Union (coprod the Sorts of v))) * -valued Element of bool [:([: the carrier' of A,{ the carrier of A}:] \/ (Union (coprod the Sorts of v))),(([: the carrier' of A,{ the carrier of A}:] \/ (Union (coprod the Sorts of v))) *):]
([: the carrier' of A,{ the carrier of A}:] \/ (Union (coprod the Sorts of v))) * is functional non empty FinSequence-membered M11([: the carrier' of A,{ the carrier of A}:] \/ (Union (coprod the Sorts of v)))
[:([: the carrier' of A,{ the carrier of A}:] \/ (Union (coprod the Sorts of v))),(([: the carrier' of A,{ the carrier of A}:] \/ (Union (coprod the Sorts of v))) *):] is Relation-like set
bool [:([: the carrier' of A,{ the carrier of A}:] \/ (Union (coprod the Sorts of v))),(([: the carrier' of A,{ the carrier of A}:] \/ (Union (coprod the Sorts of v))) *):] is set
DTConMSA the Sorts of v is non empty strict with_terminals with_nonterminals with_useful_nonterminals DTConstrStr
k is Relation-like t -defined t * -valued Element of bool [:t,(t *):]
DTConstrStr(# t,k #) is non empty strict DTConstrStr
FinTrees t is functional non empty constituted-DTrees DTree-set of t
bool (FinTrees t) is set
TS (DTConMSA the Sorts of v) is functional non empty constituted-DTrees Element of bool (FinTrees the carrier of (DTConMSA the Sorts of v))
the carrier of (DTConMSA the Sorts of v) is non empty set
FinTrees the carrier of (DTConMSA the Sorts of v) is functional non empty constituted-DTrees DTree-set of the carrier of (DTConMSA the Sorts of v)
bool (FinTrees the carrier of (DTConMSA the Sorts of v)) is set
k1 is functional constituted-DTrees Element of bool (FinTrees t)
f is set
e9 is Relation-like Function-like DecoratedTree-like set
dom e9 is non empty Tree-like set
dom Y1 is non empty finite countable Tree-like set
t19 is Relation-like NAT -defined Function-like finite FinSequence-like FinSubsequence-like countable DTree-yielding set
doms t19 is Relation-like NAT -defined Function-like finite FinSequence-like FinSubsequence-like countable Tree-yielding set
tree (doms t19) is non empty Tree-like set
dt19 is Relation-like NAT -defined NAT -valued Function-like finite FinSequence-like FinSubsequence-like countable Element of dom Y1
t19 is Relation-like NAT -defined REAL -valued Function-like finite FinSequence-like FinSubsequence-like countable FinSequence of NAT
Y1 with-replacement (t19,t1) is Relation-like Function-like DecoratedTree-like set
tft is Element of the carrier' of A
[tft, the carrier of A] is set
{tft, the carrier of A} is non empty finite countable set
{tft} is non empty trivial finite 1 -element countable set
{{tft, the carrier of A},{tft}} is non empty finite V34() countable set
len av is epsilon-transitive epsilon-connected ordinal natural V28() real finite cardinal countable ext-real non negative V136() V137() complex-membered ext-real-membered real-membered rational-membered integer-membered natural-membered V151() V152() V153() Element of NAT
a is Relation-like NAT -defined Function-like finite FinSequence-like FinSubsequence-like countable DTree-yielding set
[tft, the carrier of A] -tree a is Relation-like Function-like DecoratedTree-like set
len a is epsilon-transitive epsilon-connected ordinal natural V28() real finite cardinal countable ext-real non negative V136() V137() complex-membered ext-real-membered real-membered rational-membered integer-membered natural-membered V151() V152() V153() Element of NAT
a . (s + 1) is set
NonTerminals (DTConMSA the Sorts of v) is non empty Element of bool the carrier of (DTConMSA the Sorts of v)
bool the carrier of (DTConMSA the Sorts of v) is set
FreeSort the Sorts of v is Relation-like non-empty non empty-yielding the carrier of A -defined Function-like non empty total set
FreeOper the Sorts of v is Relation-like the carrier' of A -defined Function-like non empty total Function-yielding ManySortedFunction of the Arity of A * ((FreeSort the Sorts of v) #), the ResultSort of A * (FreeSort the Sorts of v)
the Arity of A is Relation-like the carrier' of A -defined the carrier of A * -valued Function-like non empty total V18( the carrier' of A, the carrier of A * ) Element of bool [: the carrier' of A,( the carrier of A *):]
the carrier of A * is functional non empty FinSequence-membered M11( the carrier of A)
[: the carrier' of A,( the carrier of A *):] is Relation-like set
bool [: the carrier' of A,( the carrier of A *):] is set
(FreeSort the Sorts of v) # is Relation-like the carrier of A * -defined Function-like non empty total set
the Arity of A * ((FreeSort the Sorts of v) #) is Relation-like the carrier' of A -defined Function-like non empty total set
the ResultSort of A * (FreeSort the Sorts of v) is Relation-like non-empty non empty-yielding the carrier' of A -defined Function-like non empty total set
MSAlgebra(# (FreeSort the Sorts of v),(FreeOper the Sorts of v) #) is strict MSAlgebra over A
FreeSort ( the Sorts of v,v1) is functional non empty constituted-DTrees Element of bool (TS (DTConMSA the Sorts of v))
bool (TS (DTConMSA the Sorts of v)) is set
Y1 . {} is set
o is Element of NonTerminals (DTConMSA the Sorts of v)
q is Relation-like NAT -defined FinTrees the carrier of (DTConMSA the Sorts of v) -valued Function-like finite FinSequence-like FinSubsequence-like countable DTree-yielding FinSequence of TS (DTConMSA the Sorts of v)
o -tree q is Relation-like the carrier of (DTConMSA the Sorts of v) -valued Function-like finite countable DecoratedTree-like Element of FinTrees the carrier of (DTConMSA the Sorts of v)
roots q is Relation-like NAT -defined the carrier of (DTConMSA the Sorts of v) -valued Function-like finite FinSequence-like FinSubsequence-like countable FinSequence of the carrier of (DTConMSA the Sorts of v)
FreeSort ( the Sorts of v,s1) is functional non empty constituted-DTrees Element of bool (TS (DTConMSA the Sorts of v))
the Sorts of v . s1 is non empty set
{ b1 where b1 is Relation-like the carrier of (DTConMSA the Sorts of v) -valued Function-like DecoratedTree-like Element of TS (DTConMSA the Sorts of v) : ( ex b2 being set st
( b2 in the Sorts of v . s1 & b1 = root-tree [b2,s1] ) or ex b2 being Element of the carrier' of A st
( [b2, the carrier of A] = b1 . {} & the_result_sort_of b2 = s1 ) ) } is set
q is Relation-like the carrier of (DTConMSA the Sorts of v) -valued Function-like DecoratedTree-like Element of TS (DTConMSA the Sorts of v)
q . {} is set
dom a is finite countable complex-membered ext-real-membered real-membered rational-membered integer-membered natural-membered V151() V152() V153() Element of bool NAT
rng a is finite countable set
q9 is set
qq is set
a . qq is set
tft is epsilon-transitive epsilon-connected ordinal natural V28() real finite cardinal countable ext-real non negative V136() V137() complex-membered ext-real-membered real-membered rational-membered integer-membered natural-membered V151() V152() V153() Element of NAT
tft is epsilon-transitive epsilon-connected ordinal natural V28() real finite cardinal countable ext-real non negative V136() V137() complex-membered ext-real-membered real-membered rational-membered integer-membered natural-membered V151() V152() V153() Element of NAT
a . tft is set
o9 is Relation-like NAT -defined FinTrees the carrier of (DTConMSA the Sorts of v) -valued Function-like finite FinSequence-like FinSubsequence-like countable DTree-yielding FinSequence of TS (DTConMSA the Sorts of v)
o9 . tft is Relation-like Function-like set
tft is epsilon-transitive epsilon-connected ordinal natural V28() real finite cardinal countable ext-real non negative V136() V137() complex-membered ext-real-membered real-membered rational-membered integer-membered natural-membered V151() V152() V153() Element of NAT
f is functional non empty constituted-DTrees DTree-set of t
q9 is Relation-like NAT -defined f -valued Function-like finite FinSequence-like FinSubsequence-like countable DTree-yielding FinSequence of f
roots q9 is Relation-like NAT -defined t -valued Function-like finite FinSequence-like FinSubsequence-like countable FinSequence of t
qq is Relation-like NAT -defined t -valued Function-like finite FinSequence-like FinSubsequence-like countable FinSequence of t
tft is Relation-like NAT -defined t -valued Function-like finite FinSequence-like FinSubsequence-like countable Element of t *
dom tft is finite countable complex-membered ext-real-membered real-membered rational-membered integer-membered natural-membered V151() V152() V153() Element of bool NAT
the_result_sort_of tft is Element of the carrier of A
the Sorts of (FreeEnv v) . (the_result_sort_of tft) is non empty set
the_arity_of tft is Relation-like NAT -defined the carrier of A -valued Function-like finite FinSequence-like FinSubsequence-like countable Element of the carrier of A *
len (the_arity_of tft) is epsilon-transitive epsilon-connected ordinal natural V28() real finite cardinal countable ext-real non negative V136() V137() complex-membered ext-real-membered real-membered rational-membered integer-membered natural-membered V151() V152() V153() Element of NAT
dom (the_arity_of tft) is finite countable complex-membered ext-real-membered real-membered rational-membered integer-membered natural-membered V151() V152() V153() Element of bool NAT
o9 is Relation-like NAT -defined FinTrees the carrier of (DTConMSA the Sorts of v) -valued Function-like finite FinSequence-like FinSubsequence-like countable DTree-yielding FinSequence of TS (DTConMSA the Sorts of v)
dttft is set
tft . dttft is set
(the_arity_of tft) . dttft is set
coprod (((the_arity_of tft) . dttft), the Sorts of v) is set
e9 is Relation-like NAT -defined f -valued Function-like finite FinSequence-like FinSubsequence-like countable DTree-yielding FinSequence of f
roots e9 is Relation-like NAT -defined t -valued Function-like finite FinSequence-like FinSubsequence-like countable FinSequence of t
ttft is Relation-like NAT -defined [: the carrier' of A,{ the carrier of A}:] \/ (Union (coprod the Sorts of v)) -valued Function-like finite FinSequence-like FinSubsequence-like countable Element of ([: the carrier' of A,{ the carrier of A}:] \/ (Union (coprod the Sorts of v))) *
S1 is epsilon-transitive epsilon-connected ordinal natural V28() real finite cardinal countable ext-real non negative V136() V137() complex-membered ext-real-membered real-membered rational-membered integer-membered natural-membered V151() V152() V153() Element of NAT
(the_arity_of tft) /. S1 is Element of the carrier of A
(the_arity_of tft) . S1 is set
s1 is epsilon-transitive epsilon-connected ordinal natural V28() real finite cardinal countable ext-real non negative set
av . s1 is set
(the_arity_of tft) /. s1 is Element of the carrier of A
FreeSort ( the Sorts of v,((the_arity_of tft) /. s1)) is functional non empty constituted-DTrees Element of bool (TS (DTConMSA the Sorts of v))
(the_arity_of tft) . s1 is set
the Sorts of (FreeEnv v) . ((the_arity_of tft) . s1) is set
( the Arity of A * ((FreeSort the Sorts of v) #)) . tft is set
Sym (tft, the Sorts of v) is Element of the carrier of (DTConMSA the Sorts of v)
dtft is Element of the carrier of (DTConMSA the Sorts of v)
f9 is Relation-like NAT -defined Function-like finite FinSequence-like FinSubsequence-like countable set
roots av is Relation-like NAT -defined Function-like finite FinSequence-like FinSubsequence-like countable set
dom (roots av) is finite countable complex-membered ext-real-membered real-membered rational-membered integer-membered natural-membered V151() V152() V153() Element of bool NAT
[dtft,f9] is set
{dtft,f9} is non empty finite countable set
{dtft} is non empty trivial finite 1 -element countable set
{{dtft,f9},{dtft}} is non empty finite V34() countable set
(the_arity_of tft) /. (s + 1) is Element of the carrier of A
a . S1 is set
tft . S1 is set
av . S1 is set
(roots av) . S1 is set
s1 is Element of the carrier' of A
[s1, the carrier of A] is set
{s1, the carrier of A} is non empty finite countable set
{s1} is non empty trivial finite 1 -element countable set
{{s1, the carrier of A},{s1}} is non empty finite V34() countable set
the_result_sort_of s1 is Element of the carrier of A
x99 is set
[x99,s1] is set
{x99,s1} is non empty finite countable set
{x99} is non empty trivial finite 1 -element countable set
{{x99,s1},{x99}} is non empty finite V34() countable set
root-tree [x99,s1] is Relation-like Function-like finite countable DecoratedTree-like set
x99 is set
[x99,s1] is set
{x99,s1} is non empty finite countable set
{x99} is non empty trivial finite 1 -element countable set
{{x99,s1},{x99}} is non empty finite V34() countable set
root-tree [x99,s1] is Relation-like Function-like finite countable DecoratedTree-like set
rqx is Relation-like Function-like DecoratedTree-like set
rqx . {} is set
rqx is set
x99 is Element of the carrier' of A
[x99, the carrier of A] is set
{x99, the carrier of A} is non empty finite countable set
{x99} is non empty trivial finite 1 -element countable set
{{x99, the carrier of A},{x99}} is non empty finite V34() countable set
the_result_sort_of x99 is Element of the carrier of A
rqx is Relation-like Function-like DecoratedTree-like set
rqx . {} is set
x99 is set
[x99,s1] is set
{x99,s1} is non empty finite countable set
{x99} is non empty trivial finite 1 -element countable set
{{x99,s1},{x99}} is non empty finite V34() countable set
root-tree [x99,s1] is Relation-like Function-like finite countable DecoratedTree-like set
rqx is Element of the carrier' of A
[rqx, the carrier of A] is set
{rqx, the carrier of A} is non empty finite countable set
{rqx} is non empty trivial finite 1 -element countable set
{{rqx, the carrier of A},{rqx}} is non empty finite V34() countable set
the_result_sort_of rqx is Element of the carrier of A
x99 is set
[x99,s1] is set
{x99,s1} is non empty finite countable set
{x99} is non empty trivial finite 1 -element countable set
{{x99,s1},{x99}} is non empty finite V34() countable set
root-tree [x99,s1] is Relation-like Function-like finite countable DecoratedTree-like set
rqx is Element of the carrier' of A
[rqx, the carrier of A] is set
{rqx, the carrier of A} is non empty finite countable set
{rqx} is non empty trivial finite 1 -element countable set
{{rqx, the carrier of A},{rqx}} is non empty finite V34() countable set
the_result_sort_of rqx is Element of the carrier of A
x99 is Relation-like Function-like DecoratedTree-like set
x99 . {} is set
rqx is Relation-like Function-like DecoratedTree-like set
rqx . {} is set
Terminals (DTConMSA the Sorts of v) is non empty Element of bool the carrier of (DTConMSA the Sorts of v)
x99 is set
s1 is Element of the carrier of A
the Sorts of v . s1 is non empty set
[x99,s1] is set
{x99,s1} is non empty finite countable set
{x99} is non empty trivial finite 1 -element countable set
{{x99,s1},{x99}} is non empty finite V34() countable set
rqx is Element of Terminals (DTConMSA the Sorts of v)
root-tree rqx is Relation-like the carrier of (DTConMSA the Sorts of v) -valued Function-like finite countable DecoratedTree-like Element of TS (DTConMSA the Sorts of v)
c36 is Relation-like Function-like DecoratedTree-like set
c36 . {} is set
{ b1 where b1 is Relation-like the carrier of (DTConMSA the Sorts of v) -valued Function-like DecoratedTree-like Element of TS (DTConMSA the Sorts of v) : ( ex b2 being set st
( b2 in the Sorts of v . s1 & b1 = root-tree [b2,s1] ) or ex b2 being Element of the carrier' of A st
( [b2, the carrier of A] = b1 . {} & the_result_sort_of b2 = s1 ) ) } is set
FreeSort ( the Sorts of v,s1) is functional non empty constituted-DTrees Element of bool (TS (DTConMSA the Sorts of v))
(FreeSort the Sorts of v) . s1 is non empty set
(FreeSort the Sorts of v) . s1 is non empty set
((FreeSort the Sorts of v) . s1) /\ ((FreeSort the Sorts of v) . s1) is set
rqx is Relation-like Function-like DecoratedTree-like set
rqx . {} is set
c36 is Relation-like Function-like DecoratedTree-like set
c36 . {} is set
len tft is epsilon-transitive epsilon-connected ordinal natural V28() real finite cardinal countable ext-real non negative V136() V137() complex-membered ext-real-membered real-membered rational-membered integer-membered natural-membered V151() V152() V153() Element of NAT
roots a is Relation-like NAT -defined Function-like finite FinSequence-like FinSubsequence-like countable set
[o,(roots a)] is set
{o,(roots a)} is non empty finite countable set
{o} is non empty trivial finite 1 -element countable set
{{o,(roots a)},{o}} is non empty finite V34() countable set
dtft is Relation-like NAT -defined FinTrees the carrier of (DTConMSA the Sorts of v) -valued Function-like finite FinSequence-like FinSubsequence-like countable DTree-yielding SubtreeSeq of o
o -tree dtft is Relation-like the carrier of (DTConMSA the Sorts of v) -valued Function-like DecoratedTree-like Element of TS (DTConMSA the Sorts of v)
dom t1 is non empty finite countable Tree-like set
(dom Y1) with-replacement (t19,(dom t1)) is non empty Tree-like set
(Y1 with-replacement (<*s*>,t1)) . (<*> NAT) is set
Y1 . (<*> NAT) is set
(Y1 with-replacement (<*s*>,t1)) . {} is set
dttft is Relation-like NAT -defined REAL -valued Function-like finite FinSequence-like FinSubsequence-like countable FinSequence of NAT
t19 ^ dttft is Relation-like NAT -defined NAT -valued Function-like finite FinSequence-like FinSubsequence-like countable FinSequence of NAT
t1 . dttft is set
dttft is Element of the carrier' of A
the_result_sort_of dttft is Element of the carrier of A
e9 is Relation-like the carrier of (DTConMSA the Sorts of v) -valued Function-like DecoratedTree-like Element of TS (DTConMSA the Sorts of v)
the Sorts of v . v1 is non empty set
{ b1 where b1 is Relation-like the carrier of (DTConMSA the Sorts of v) -valued Function-like DecoratedTree-like Element of TS (DTConMSA the Sorts of v) : ( ex b2 being set st
( b2 in the Sorts of v . v1 & b1 = root-tree [b2,v1] ) or ex b2 being Element of the carrier' of A st
( [b2, the carrier of A] = b1 . {} & the_result_sort_of b2 = v1 ) ) } is set
ttft is Element of the carrier' of A
[ttft, the carrier of A] is set
{ttft, the carrier of A} is non empty finite countable set
{ttft} is non empty trivial finite 1 -element countable set
{{ttft, the carrier of A},{ttft}} is non empty finite V34() countable set
the_result_sort_of ttft is Element of the carrier of A
dttft is Relation-like Function-like non empty finite countable DecoratedTree-like Element of the Sorts of (FreeEnv v) . v1
IIG is non empty non void V51() Circuit-like monotonic ManySortedSign
the carrier of IIG is non empty set
the carrier' of IIG is non empty set
A is non-empty finitely-generated finite-yielding MSAlgebra over IIG
FreeEnv A is strict non-empty V117(IIG) MSAlgebra over IIG
the Sorts of A is Relation-like non-empty non empty-yielding the carrier of IIG -defined Function-like non empty total set
FreeMSA the Sorts of A is strict non-empty MSAlgebra over IIG
the Sorts of (FreeEnv A) is Relation-like non-empty non empty-yielding the carrier of IIG -defined Function-like non empty total set
v is Element of the carrier of IIG
the Sorts of (FreeEnv A) . v is non empty set
v1 is Relation-like Function-like non empty finite countable DecoratedTree-like Element of the Sorts of (FreeEnv A) . v
card v1 is non empty epsilon-transitive epsilon-connected ordinal natural V28() real finite cardinal countable ext-real positive non negative V136() V137() complex-membered ext-real-membered real-membered rational-membered integer-membered natural-membered V149() V150() V151() V152() V153() Element of omega
v1 . {} is set
FreeSort the Sorts of A is Relation-like non-empty non empty-yielding the carrier of IIG -defined Function-like non empty total set
(FreeSort the Sorts of A) . v is non empty set
FreeSort ( the Sorts of A,v) is functional non empty constituted-DTrees Element of bool (TS (DTConMSA the Sorts of A))
DTConMSA the Sorts of A is non empty strict with_terminals with_nonterminals with_useful_nonterminals DTConstrStr
TS (DTConMSA the Sorts of A) is functional non empty constituted-DTrees Element of bool (FinTrees the carrier of (DTConMSA the Sorts of A))
the carrier of (DTConMSA the Sorts of A) is non empty set
FinTrees the carrier of (DTConMSA the Sorts of A) is functional non empty constituted-DTrees DTree-set of the carrier of (DTConMSA the Sorts of A)
bool (FinTrees the carrier of (DTConMSA the Sorts of A)) is set
bool (TS (DTConMSA the Sorts of A)) is set
the Sorts of A . v is non empty set
{ b1 where b1 is Relation-like the carrier of (DTConMSA the Sorts of A) -valued Function-like DecoratedTree-like Element of TS (DTConMSA the Sorts of A) : ( ex b2 being set st
( b2 in the Sorts of A . v & b1 = root-tree [b2,v] ) or ex b2 being Element of the carrier' of IIG st
( [b2, the carrier of IIG] = b1 . {} & the_result_sort_of b2 = v ) ) } is set
the Sorts of (FreeMSA the Sorts of A) is Relation-like non-empty non empty-yielding the carrier of IIG -defined Function-like non empty total set
the Sorts of (FreeMSA the Sorts of A) . v is non empty set
FreeOper the Sorts of A is Relation-like the carrier' of IIG -defined Function-like non empty total Function-yielding ManySortedFunction of the Arity of IIG * ((FreeSort the Sorts of A) #), the ResultSort of IIG * (FreeSort the Sorts of A)
the Arity of IIG is Relation-like the carrier' of IIG -defined the carrier of IIG * -valued Function-like non empty total V18( the carrier' of IIG, the carrier of IIG * ) Element of bool [: the carrier' of IIG,( the carrier of IIG *):]
the carrier of IIG * is functional non empty FinSequence-membered M11( the carrier of IIG)
[: the carrier' of IIG,( the carrier of IIG *):] is Relation-like set
bool [: the carrier' of IIG,( the carrier of IIG *):] is set
(FreeSort the Sorts of A) # is Relation-like the carrier of IIG * -defined Function-like non empty total set
the Arity of IIG * ((FreeSort the Sorts of A) #) is Relation-like the carrier' of IIG -defined Function-like non empty total set
the ResultSort of IIG is Relation-like the carrier' of IIG -defined the carrier of IIG -valued Function-like non empty total V18( the carrier' of IIG, the carrier of IIG) Element of bool [: the carrier' of IIG, the carrier of IIG:]
[: the carrier' of IIG, the carrier of IIG:] is Relation-like set
bool [: the carrier' of IIG, the carrier of IIG:] is set
the ResultSort of IIG * (FreeSort the Sorts of A) is Relation-like non-empty non empty-yielding the carrier' of IIG -defined Function-like non empty total set
MSAlgebra(# (FreeSort the Sorts of A),(FreeOper the Sorts of A) #) is strict MSAlgebra over IIG
Y1 is Relation-like the carrier of (DTConMSA the Sorts of A) -valued Function-like DecoratedTree-like Element of TS (DTConMSA the Sorts of A)
t1 is set
[t1,v] is set
{t1,v} is non empty finite countable set
{t1} is non empty trivial finite 1 -element countable set
{{t1,v},{t1}} is non empty finite V34() countable set
root-tree [t1,v] is Relation-like Function-like finite countable DecoratedTree-like set
av is Element of the carrier' of IIG
[av, the carrier of IIG] is set
{av, the carrier of IIG} is non empty finite countable set
{av} is non empty trivial finite 1 -element countable set
{{av, the carrier of IIG},{av}} is non empty finite V34() countable set
Y1 . {} is set
the_result_sort_of av is Element of the carrier of IIG
IIG is non empty non void V51() Circuit-like ManySortedSign
the carrier of IIG is non empty set
the carrier' of IIG is non empty set
A is non-empty finitely-generated finite-yielding MSAlgebra over IIG
the Sorts of A is Relation-like non-empty non empty-yielding the carrier of IIG -defined Function-like non empty total set
product the Sorts of A is functional non empty with_common_domain product-like set
v is Relation-like the carrier of IIG -defined Function-like the Sorts of A -compatible non empty total Element of product the Sorts of A
v1 is Element of the carrier' of IIG
Den (v1,A) is Relation-like Args (v1,A) -defined Result (v1,A) -valued Function-like non empty total V18( Args (v1,A), Result (v1,A)) Element of bool [:(Args (v1,A)),(Result (v1,A)):]
Args (v1,A) is non empty Element of rng ( the Sorts of A #)
the Sorts of A # is Relation-like the carrier of IIG * -defined Function-like non empty total set
the carrier of IIG * is functional non empty FinSequence-membered M11( the carrier of IIG)
rng ( the Sorts of A #) is non empty set
Result (v1,A) is non empty Element of rng the Sorts of A
rng the Sorts of A is non empty set
[:(Args (v1,A)),(Result (v1,A)):] is Relation-like set
bool [:(Args (v1,A)),(Result (v1,A)):] is set
(IIG,A,v,v1) is Element of Args (v1,A)
the_arity_of v1 is Relation-like NAT -defined the carrier of IIG -valued Function-like finite FinSequence-like FinSubsequence-like countable Element of the carrier of IIG *
(the_arity_of v1) * v is Relation-like NAT -defined Function-like finite countable set
(Den (v1,A)) . (IIG,A,v,v1) is set
the_result_sort_of v1 is Element of the carrier of IIG
the Sorts of A . (the_result_sort_of v1) is non empty set
the ResultSort of IIG is Relation-like the carrier' of IIG -defined the carrier of IIG -valued Function-like non empty total V18( the carrier' of IIG, the carrier of IIG) Element of bool [: the carrier' of IIG, the carrier of IIG:]
[: the carrier' of IIG, the carrier of IIG:] is Relation-like set
bool [: the carrier' of IIG, the carrier of IIG:] is set
dom the ResultSort of IIG is non empty Element of bool the carrier' of IIG
bool the carrier' of IIG is set
the ResultSort of IIG * the Sorts of A is Relation-like non-empty non empty-yielding the carrier' of IIG -defined Function-like non empty total set
( the ResultSort of IIG * the Sorts of A) . v1 is non empty set
the ResultSort of IIG . v1 is set
the Sorts of A . ( the ResultSort of IIG . v1) is set
IIG is non empty non void V51() Circuit-like monotonic ManySortedSign
the carrier of IIG is non empty set
A is non-empty finitely-generated finite-yielding MSAlgebra over IIG
FreeEnv A is strict non-empty V117(IIG) MSAlgebra over IIG
the Sorts of A is Relation-like non-empty non empty-yielding the carrier of IIG -defined Function-like non empty total set
FreeMSA the Sorts of A is strict non-empty MSAlgebra over IIG
the Sorts of (FreeEnv A) is Relation-like non-empty non empty-yielding the carrier of IIG -defined Function-like non empty total set
v is Element of the carrier of IIG
the Sorts of (FreeEnv A) . v is non empty set
action_at v is Element of the carrier' of IIG
the carrier' of IIG is non empty set
[(action_at v), the carrier of IIG] is set
{(action_at v), the carrier of IIG} is non empty finite countable set
{(action_at v)} is non empty trivial finite 1 -element countable set
{{(action_at v), the carrier of IIG},{(action_at v)}} is non empty finite V34() countable set
v1 is Relation-like Function-like non empty finite countable DecoratedTree-like Element of the Sorts of (FreeEnv A) . v
v1 . {} is set
DTConMSA the Sorts of A is non empty strict with_terminals with_nonterminals with_useful_nonterminals DTConstrStr
NonTerminals (DTConMSA the Sorts of A) is non empty Element of bool the carrier of (DTConMSA the Sorts of A)
the carrier of (DTConMSA the Sorts of A) is non empty set
bool the carrier of (DTConMSA the Sorts of A) is set
{ the carrier of IIG} is non empty trivial finite 1 -element countable set
[: the carrier' of IIG,{ the carrier of IIG}:] is Relation-like set
FreeSort the Sorts of A is Relation-like non-empty non empty-yielding the carrier of IIG -defined Function-like non empty total set
FreeOper the Sorts of A is Relation-like the carrier' of IIG -defined Function-like non empty total Function-yielding ManySortedFunction of the Arity of IIG * ((FreeSort the Sorts of A) #), the ResultSort of IIG * (FreeSort the Sorts of A)
the Arity of IIG is Relation-like the carrier' of IIG -defined the carrier of IIG * -valued Function-like non empty total V18( the carrier' of IIG, the carrier of IIG * ) Element of bool [: the carrier' of IIG,( the carrier of IIG *):]
the carrier of IIG * is functional non empty FinSequence-membered M11( the carrier of IIG)
[: the carrier' of IIG,( the carrier of IIG *):] is Relation-like set
bool [: the carrier' of IIG,( the carrier of IIG *):] is set
(FreeSort the Sorts of A) # is Relation-like the carrier of IIG * -defined Function-like non empty total set
the Arity of IIG * ((FreeSort the Sorts of A) #) is Relation-like the carrier' of IIG -defined Function-like non empty total set
the ResultSort of IIG is Relation-like the carrier' of IIG -defined the carrier of IIG -valued Function-like non empty total V18( the carrier' of IIG, the carrier of IIG) Element of bool [: the carrier' of IIG, the carrier of IIG:]
[: the carrier' of IIG, the carrier of IIG:] is Relation-like set
bool [: the carrier' of IIG, the carrier of IIG:] is set
the ResultSort of IIG * (FreeSort the Sorts of A) is Relation-like non-empty non empty-yielding the carrier' of IIG -defined Function-like non empty total set
MSAlgebra(# (FreeSort the Sorts of A),(FreeOper the Sorts of A) #) is strict MSAlgebra over IIG
FreeSort ( the Sorts of A,v) is functional non empty constituted-DTrees Element of bool (TS (DTConMSA the Sorts of A))
TS (DTConMSA the Sorts of A) is functional non empty constituted-DTrees Element of bool (FinTrees the carrier of (DTConMSA the Sorts of A))
FinTrees the carrier of (DTConMSA the Sorts of A) is functional non empty constituted-DTrees DTree-set of the carrier of (DTConMSA the Sorts of A)
bool (FinTrees the carrier of (DTConMSA the Sorts of A)) is set
bool (TS (DTConMSA the Sorts of A)) is set
t1 is Relation-like the carrier of (DTConMSA the Sorts of A) -valued Function-like DecoratedTree-like Element of TS (DTConMSA the Sorts of A)
Y1 is Element of NonTerminals (DTConMSA the Sorts of A)
av is Relation-like NAT -defined FinTrees the carrier of (DTConMSA the Sorts of A) -valued Function-like finite FinSequence-like FinSubsequence-like countable DTree-yielding FinSequence of TS (DTConMSA the Sorts of A)
Y1 -tree av is Relation-like the carrier of (DTConMSA the Sorts of A) -valued Function-like finite countable DecoratedTree-like Element of FinTrees the carrier of (DTConMSA the Sorts of A)
roots av is Relation-like NAT -defined the carrier of (DTConMSA the Sorts of A) -valued Function-like finite FinSequence-like FinSubsequence-like countable FinSequence of the carrier of (DTConMSA the Sorts of A)
[(action_at v), the carrier of IIG] -tree av is Relation-like Function-like DecoratedTree-like set
IIG is non empty non void V51() monotonic ManySortedSign
the carrier of IIG is non empty set
A is non-empty finitely-generated finite-yielding MSAlgebra over IIG
FreeEnv A is strict non-empty V117(IIG) MSAlgebra over IIG
the Sorts of A is Relation-like non-empty non empty-yielding the carrier of IIG -defined Function-like non empty total set
FreeMSA the Sorts of A is strict non-empty MSAlgebra over IIG
the Sorts of (FreeEnv A) is Relation-like non-empty non empty-yielding the carrier of IIG -defined Function-like non empty total set
v is Element of the carrier of IIG
the Sorts of (FreeEnv A) . v is non empty set
IIG is non empty non void V51() Circuit-like monotonic ManySortedSign
the carrier of IIG is non empty set
A is non-empty finitely-generated finite-yielding MSAlgebra over IIG
FreeEnv A is strict non-empty V117(IIG) MSAlgebra over IIG
the Sorts of A is Relation-like non-empty non empty-yielding the carrier of IIG -defined Function-like non empty total set
FreeMSA the Sorts of A is strict non-empty MSAlgebra over IIG
the Sorts of (FreeEnv A) is Relation-like non-empty non empty-yielding the carrier of IIG -defined Function-like non empty total set
v is Element of the carrier of IIG
the Sorts of (FreeEnv A) . v is non empty finite countable set
{ (card b1) where b1 is Relation-like Function-like non empty finite countable DecoratedTree-like Element of the Sorts of (FreeEnv A) . v : verum } is set
{ H1(b1) where b1 is Relation-like Function-like non empty finite countable DecoratedTree-like Element of the Sorts of (FreeEnv A) . v : S1[b1] } is set
the Relation-like Function-like non empty finite countable DecoratedTree-like Element of the Sorts of (FreeEnv A) . v is Relation-like Function-like non empty finite countable DecoratedTree-like Element of the Sorts of (FreeEnv A) . v
card the Relation-like Function-like non empty finite countable DecoratedTree-like Element of the Sorts of (FreeEnv A) . v is non empty epsilon-transitive epsilon-connected ordinal natural V28() real finite cardinal countable ext-real positive non negative V136() V137() complex-membered ext-real-membered real-membered rational-membered integer-membered natural-membered V149() V150() V151() V152() V153() Element of omega
Y1 is non empty finite countable complex-membered ext-real-membered real-membered rational-membered integer-membered natural-membered V149() V150() V151() V152() V153() Element of bool NAT
max Y1 is epsilon-transitive epsilon-connected ordinal natural V28() real finite cardinal countable ext-real non negative V136() V137() set
Y1 is non empty finite countable complex-membered ext-real-membered real-membered rational-membered integer-membered natural-membered V149() V150() V151() V152() V153() Element of bool NAT
v1 is epsilon-transitive epsilon-connected ordinal natural V28() real finite cardinal countable ext-real non negative set
max Y1 is epsilon-transitive epsilon-connected ordinal natural V28() real finite cardinal countable ext-real non negative V136() V137() set
t1 is non empty finite countable complex-membered ext-real-membered real-membered rational-membered integer-membered natural-membered V149() V150() V151() V152() V153() Element of bool NAT
s1 is epsilon-transitive epsilon-connected ordinal natural V28() real finite cardinal countable ext-real non negative set
max t1 is epsilon-transitive epsilon-connected ordinal natural V28() real finite cardinal countable ext-real non negative V136() V137() set
IIG is non empty non void V51() Circuit-like monotonic ManySortedSign
the carrier of IIG is non empty set
InputVertices IIG is Element of bool the carrier of IIG
bool the carrier of IIG is set
the ResultSort of IIG is Relation-like the carrier' of IIG -defined the carrier of IIG -valued Function-like non empty total V18( the carrier' of IIG, the carrier of IIG) Element of bool [: the carrier' of IIG, the carrier of IIG:]
the carrier' of IIG is non empty set
[: the carrier' of IIG, the carrier of IIG:] is Relation-like set
bool [: the carrier' of IIG, the carrier of IIG:] is set
rng the ResultSort of IIG is non empty Element of bool the carrier of IIG
the carrier of IIG \ (rng the ResultSort of IIG) is Element of bool the carrier of IIG
SortsWithConstants IIG is Element of bool the carrier of IIG
(InputVertices IIG) \/ (SortsWithConstants IIG) is Element of bool the carrier of IIG
A is non-empty finitely-generated