:: CIRCUIT1 semantic presentation

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
{ b₁ where b₁ is Element of the carrier of IIG : b₁ 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
{ b₁ where b₁ is Element of t : ex b₂ being Element of the carrier' of IIG st
( the Arity of IIG . b₂ = {} & the ResultSort of IIG . b₂ = Y1 & b₁ in rng (Den (b₂,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
{ b₁ where b₁ is Element of t1 : ex b₂ being Element of the carrier' of IIG st
( the Arity of IIG . b₂ = {} & the ResultSort of IIG . b₂ = Y1 & b₁ in rng (Den (b₂,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
{ b₁ where b₁ is Element of s : ex b₂ being Element of the carrier' of IIG st
( the Arity of IIG . b₂ = {} & the ResultSort of IIG . b₂ = Y1 & b₁ in rng (Den (b₂,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
{ b₁ where b₁ is Element of s1 : ex b₂ being Element of the carrier' of IIG st
( the Arity of IIG . b₂ = {} & the ResultSort of IIG . b₂ = v & b₁ in rng (Den (b₂,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
{ b₁ where b₁ is Element of Y1 : ex b₂ being Element of the carrier' of IIG st
( the Arity of IIG . b₂ = {} & the ResultSort of IIG . b₂ = v & b₁ in rng (Den (b₂,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
{ b₁ where b₁ 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 b₂ being set st
( b₂ in the Sorts of v . s1 & b₁ = root-tree [b₂,s1] ) or ex b₂ being Element of the carrier' of A st
( [b₂, the carrier of A] = b₁ . {} & the_result_sort_of b₂ = 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)
c₃₆ is Relation-like Function-like DecoratedTree-like set
c₃₆ . {} is set
{ b₁ where b₁ 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 b₂ being set st
( b₂ in the Sorts of v . s1 & b₁ = root-tree [b₂,s1] ) or ex b₂ being Element of the carrier' of A st
( [b₂, the carrier of A] = b₁ . {} & the_result_sort_of b₂ = 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
c₃₆ is Relation-like Function-like DecoratedTree-like set
c₃₆ . {} 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
{ b₁ where b₁ 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 b₂ being set st
( b₂ in the Sorts of v . v1 & b₁ = root-tree [b₂,v1] ) or ex b₂ being Element of the carrier' of A st
( [b₂, the carrier of A] = b₁ . {} & the_result_sort_of b₂ = 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
{ b₁ where b₁ 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 b₂ being set st
( b₂ in the Sorts of A . v & b₁ = root-tree [b₂,v] ) or ex b₂ being Element of the carrier' of IIG st
( [b₂, the carrier of IIG] = b₁ . {} & the_result_sort_of b₂ = 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 b₁) where b₁ is Relation-like Function-like non empty finite countable DecoratedTree-like Element of the Sorts of (FreeEnv A) . v : verum } is set
{ H₁(b₁) where b₁ is Relation-like Function-like non empty finite countable DecoratedTree-like Element of the Sorts of (FreeEnv A) . v : S₁[b₁] } 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 finite-yielding MSAlgebra over IIG
v is Element of the carrier of IIG
(IIG,A,v) is epsilon-transitive epsilon-connected ordinal natural V28() real finite cardinal countable ext-real non negative set
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
the Sorts of (FreeEnv A) . v is non empty finite countable set
{ (card b₁) where b₁ is Relation-like Function-like non empty finite countable DecoratedTree-like Element of the Sorts of (FreeEnv A) . v : verum } is set
v1 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 v1 is epsilon-transitive epsilon-connected ordinal natural V28() real finite cardinal countable ext-real non negative V136() V137() set
s1 is non empty finite countable complex-membered ext-real-membered real-membered V149() V150() V151() V152() V153() set
max s1 is V28() real ext-real set
Y1 is Relation-like Function-like non empty finite countable DecoratedTree-like Element of the Sorts of (FreeEnv A) . v
card Y1 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
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 * (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))
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
{ b₁ where b₁ 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 b₂ being set st
( b₂ in the Sorts of A . v & b₁ = root-tree [b₂,v] ) or ex b₂ being Element of the carrier' of IIG st
( [b₂, the carrier of IIG] = b₁ . {} & the_result_sort_of b₂ = v ) ) } is set
{ b₁ where b₁ is Element of the carrier of IIG : b₁ is with_const_op } is set
InnerVertices IIG is non empty Element of bool the carrier of IIG
(InputVertices IIG) \/ (InnerVertices IIG) is non empty Element of bool the carrier of IIG
dom the ResultSort of IIG is non empty Element of bool the carrier' of IIG
bool the carrier' of IIG is set
t1 is set
the ResultSort of IIG . t1 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_arity_of av 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 non empty trivial finite 1 -element countable set
[: the carrier' of IIG,{ the carrier of IIG}:] is Relation-like set
coprod the Sorts of A is Relation-like non-empty non empty-yielding the carrier of IIG -defined Function-like non empty total set
Union (coprod the Sorts of A) is non empty set
[: the carrier' of IIG,{ the carrier of IIG}:] \/ (Union (coprod the Sorts of A)) is non empty set
s is non empty set
s * is functional non empty FinSequence-membered M11(s)
[:s,(s *):] is Relation-like set
bool [:s,(s *):] is set
REL the Sorts of A is Relation-like [: the carrier' of IIG,{ the carrier of IIG}:] \/ (Union (coprod the Sorts of A)) -defined ([: the carrier' of IIG,{ the carrier of IIG}:] \/ (Union (coprod the Sorts of A))) * -valued Element of bool [:([: the carrier' of IIG,{ the carrier of IIG}:] \/ (Union (coprod the Sorts of A))),(([: the carrier' of IIG,{ the carrier of IIG}:] \/ (Union (coprod the Sorts of A))) *):]
([: the carrier' of IIG,{ the carrier of IIG}:] \/ (Union (coprod the Sorts of A))) * is functional non empty FinSequence-membered M11([: the carrier' of IIG,{ the carrier of IIG}:] \/ (Union (coprod the Sorts of A)))
[:([: the carrier' of IIG,{ the carrier of IIG}:] \/ (Union (coprod the Sorts of A))),(([: the carrier' of IIG,{ the carrier of IIG}:] \/ (Union (coprod the Sorts of A))) *):] is Relation-like set
bool [:([: the carrier' of IIG,{ the carrier of IIG}:] \/ (Union (coprod the Sorts of A))),(([: the carrier' of IIG,{ the carrier of IIG}:] \/ (Union (coprod the Sorts of A))) *):] is set
[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
x is Relation-like s -defined s * -valued Element of bool [:s,(s *):]
DTConstrStr(# s,x #) is non empty strict DTConstrStr
Y is Element of the carrier of (DTConMSA the Sorts of A)
NonTerminals (DTConMSA the Sorts of A) is non empty Element of bool the carrier of (DTConMSA the Sorts of A)
bool the carrier of (DTConMSA the Sorts of A) is set
t 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)
roots t 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)
Y -tree t 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)
k is Relation-like the carrier of (DTConMSA the Sorts of A) -valued Function-like DecoratedTree-like Element of TS (DTConMSA the Sorts of A)
k1 is Relation-like Function-like finite countable DecoratedTree-like set
card k1 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 omega
k . {} is set
tft is Element of the carrier' of IIG
the_result_sort_of tft is Element of the carrier of IIG
e9 is Element of the carrier' of IIG
[e9, the carrier of IIG] is set
{e9, the carrier of IIG} is non empty finite countable set
{e9} is non empty trivial finite 1 -element countable set
{{e9, the carrier of IIG},{e9}} is non empty finite V34() countable set
the_result_sort_of e9 is Element of the carrier of IIG
the_result_sort_of av is Element of the carrier of IIG
the Sorts of (FreeEnv A) . (the_result_sort_of av) is non empty finite countable set
(FreeSort the Sorts of A) . v is non empty set
len t 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
len (the_arity_of 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
rng t is functional finite countable constituted-DTrees Element of bool (FinTrees the carrier of (DTConMSA the Sorts of A))
dom t is finite countable complex-membered ext-real-membered real-membered rational-membered integer-membered natural-membered V151() V152() V153() Element of bool NAT
dom k is non empty finite countable Tree-like set
0 + 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
<*0*> is Relation-like NAT -defined NAT -valued Function-like constant non empty trivial finite 1 -element FinSequence-like FinSubsequence-like countable FinSequence of NAT
e9 is Relation-like NAT -defined Function-like finite FinSequence-like FinSubsequence-like countable DTree-yielding set
doms e9 is Relation-like NAT -defined Function-like finite FinSequence-like FinSubsequence-like countable Tree-yielding set
tree (doms e9) is non empty Tree-like set
dt19 is Relation-like Function-like DecoratedTree-like set
dom dt19 is non empty Tree-like set
e9 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
e9 + 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
t . (e9 + 1) is Relation-like Function-like set
<*e9*> is Relation-like NAT -defined NAT -valued Function-like constant non empty trivial finite 1 -element FinSequence-like FinSubsequence-like countable FinSequence of NAT
t19 is Relation-like NAT -defined NAT -valued Function-like finite FinSequence-like FinSubsequence-like countable Element of dom dt19
<*e9*> ^ t19 is Relation-like NAT -defined NAT -valued Function-like non empty finite FinSequence-like FinSubsequence-like countable FinSequence of NAT
k . <*0*> is set
dt19 . t19 is set
[<*0*>,(dt19 . t19)] is set
{<*0*>,(dt19 . t19)} is non empty finite countable set
{<*0*>} is functional non empty trivial finite V34() 1 -element with_common_domain countable set
{{<*0*>,(dt19 . t19)},{<*0*>}} is non empty finite V34() countable set
[{},Y] is set
{{},Y} is non empty finite countable set
{{{},Y},{{}}} is non empty finite V34() countable set
{[{},Y],[<*0*>,(dt19 . t19)]} is Relation-like non empty finite countable set
tft is Relation-like Function-like non empty finite countable DecoratedTree-like Element of the Sorts of (FreeEnv A) . v
f is V28() real ext-real set
card {[{},Y],[<*0*>,(dt19 . t19)]} 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
av is Element of the carrier' of IIG
the ResultSort of IIG . av 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
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)
t1 . {} is set
av is set
[av,v] is set
{av,v} is non empty finite countable set
{av} is non empty trivial finite 1 -element countable set
{{av,v},{av}} is non empty finite V34() countable set
root-tree [av,v] is Relation-like Function-like finite countable DecoratedTree-like set
s is Element of the carrier' of IIG
[s, the carrier of IIG] is set
{s, the carrier of IIG} is non empty finite countable set
{s} is non empty trivial finite 1 -element countable set
{{s, the carrier of IIG},{s}} is non empty finite V34() countable set
the_result_sort_of s is Element of the carrier of IIG
av is set
[av,v] is set
{av,v} is non empty finite countable set
{av} is non empty trivial finite 1 -element countable set
{{av,v},{av}} is non empty finite V34() countable set
root-tree [av,v] is Relation-like Function-like finite countable DecoratedTree-like set
{{}} --> [av,v] is Relation-like {{}} -defined {[av,v]} -valued Function-like non empty total V18({{}},{[av,v]}) finite countable DecoratedTree-like Element of bool [:{{}},{[av,v]}:]
{[av,v]} is Relation-like Function-like constant non empty trivial finite 1 -element countable set
[:{{}},{[av,v]}:] is Relation-like finite countable set
bool [:{{}},{[av,v]}:] is finite V34() countable set
[{},[av,v]] is set
{{},[av,v]} is non empty finite countable set
{{{},[av,v]},{{}}} is non empty finite V34() countable set
{[{},[av,v]]} is Relation-like Function-like constant non empty trivial finite 1 -element countable set
{ b₁ where b₁ is Element of the carrier of IIG : b₁ is with_const_op } is set
av is Element of the carrier of IIG
s is Element of the carrier' of IIG
the Arity of IIG . s is Relation-like NAT -defined Function-like finite FinSequence-like FinSubsequence-like countable set
the ResultSort of IIG . s is set
x is set
[x,v] is set
{x,v} is non empty finite countable set
{x} is non empty trivial finite 1 -element countable set
{{x,v},{x}} is non empty finite V34() countable set
root-tree [x,v] is Relation-like Function-like finite countable DecoratedTree-like set
x is set
[x,v] is set
{x,v} is non empty finite countable set
{x} is non empty trivial finite 1 -element countable set
{{x,v},{x}} is non empty finite V34() countable set
root-tree [x,v] is Relation-like Function-like finite countable DecoratedTree-like set
[{},[x,v]] is set
{{},[x,v]} is non empty finite countable set
{{{},[x,v]},{{}}} is non empty finite V34() countable set
{[{},[x,v]]} is Relation-like Function-like constant non empty trivial finite 1 -element countable set
x is Element of the carrier' of IIG
[x, the carrier of IIG] is set
{x, the carrier of IIG} is non empty finite countable set
{x} is non empty trivial finite 1 -element countable set
{{x, the carrier of IIG},{x}} is non empty finite V34() countable set
the_result_sort_of x is Element of the carrier of IIG
x is Element of the carrier' of IIG
[x, the carrier of IIG] is set
{x, the carrier of IIG} is non empty finite countable set
{x} is non empty trivial finite 1 -element countable set
{{x, the carrier of IIG},{x}} is non empty finite V34() countable set
the_result_sort_of x is Element of the carrier of IIG
the_result_sort_of s is Element of the carrier of IIG
NonTerminals (DTConMSA the Sorts of A) is non empty Element of bool the carrier of (DTConMSA the Sorts of A)
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
Y is Element of NonTerminals (DTConMSA the Sorts of A)
t 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)
Y -tree t 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 t 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)
k is Relation-like NAT -defined Function-like finite FinSequence-like FinSubsequence-like countable DTree-yielding set
len k 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 x 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 x) 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
len {} 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
root-tree Y is Relation-like NonTerminals (DTConMSA the Sorts of A) -valued Function-like finite countable DecoratedTree-like Element of FinTrees (NonTerminals (DTConMSA the Sorts of A))
FinTrees (NonTerminals (DTConMSA the Sorts of A)) is functional non empty constituted-DTrees DTree-set of NonTerminals (DTConMSA the Sorts of A)
[{},Y] is set
{{},Y} is non empty finite countable set
{{{},Y},{{}}} is non empty finite V34() countable set
{[{},Y]} is Relation-like Function-like constant non empty trivial finite 1 -element countable set
x is set
[x,v] is set
{x,v} is non empty finite countable set
{x} is non empty trivial finite 1 -element countable set
{{x,v},{x}} is non empty finite V34() countable set
root-tree [x,v] is Relation-like Function-like finite countable DecoratedTree-like set
Y is Element of the carrier' of IIG
[Y, the carrier of IIG] is set
{Y, the carrier of IIG} is non empty finite countable set
{Y} is non empty trivial finite 1 -element countable set
{{Y, the carrier of IIG},{Y}} is non empty finite V34() countable set
the_result_sort_of Y is Element of the carrier of IIG
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
SortsWithConstants IIG is Element of bool the carrier of IIG
(InnerVertices IIG) \ (SortsWithConstants IIG) is 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 finite countable set
v1 is Element of the carrier of IIG
the Sorts of (FreeEnv A) . v1 is non empty finite countable set
(IIG,A,v) is epsilon-transitive epsilon-connected ordinal natural V28() real finite cardinal countable ext-real non negative 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
(IIG,A,v1) is epsilon-transitive epsilon-connected ordinal natural V28() real finite cardinal countable ext-real non negative set
s1 is Relation-like Function-like non empty finite countable DecoratedTree-like Element of the Sorts of (FreeEnv A) . v
card s1 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 Relation-like Function-like non empty finite countable DecoratedTree-like Element of the Sorts of (FreeEnv A) . v1
card Y1 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
t1 is Relation-like NAT -defined Function-like finite FinSequence-like FinSubsequence-like countable DTree-yielding set
[(action_at v), the carrier of IIG] -tree t1 is Relation-like Function-like DecoratedTree-like set
rng t1 is finite countable set
{ (card b₁) where b₁ is Relation-like Function-like non empty finite countable DecoratedTree-like Element of the Sorts of (FreeEnv A) . v1 : verum } is set
av 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 av is epsilon-transitive epsilon-connected ordinal natural V28() real finite cardinal countable ext-real non negative V136() V137() set
s is non empty finite countable complex-membered ext-real-membered real-membered V149() V150() V151() V152() V153() set
max s is V28() real ext-real set
x is V28() real ext-real set
Y is Relation-like Function-like non empty finite countable DecoratedTree-like Element of the Sorts of (FreeEnv A) . v1
card Y 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
k1 is Relation-like Function-like set
dom k1 is set
f is set
k1 . f is set
dom t1 is finite countable complex-membered ext-real-membered real-membered rational-membered integer-membered natural-membered V151() V152() V153() Element of bool 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
tft - 1 is V28() real ext-real Element of REAL
e9 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
e9 + 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
k is Relation-like Function-like DecoratedTree-like set
dom k is non empty Tree-like set
dom s1 is non empty finite countable Tree-like set
<*e9*> is Relation-like NAT -defined NAT -valued Function-like constant non empty trivial finite 1 -element FinSequence-like FinSubsequence-like countable FinSequence of NAT
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
len 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
dt19 is Relation-like NAT -defined NAT -valued Function-like finite FinSequence-like FinSubsequence-like countable Element of dom s1
s1 | dt19 is Relation-like Function-like finite countable DecoratedTree-like set
s1 with-replacement (dt19,Y) is Relation-like Function-like finite countable DecoratedTree-like set
card (s1 with-replacement (dt19,Y)) 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 omega
card (s1 | dt19) 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 omega
(card (s1 with-replacement (dt19,Y))) + (card (s1 | dt19)) 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
(card s1) + (card Y) 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
(card s1) + (card (s1 | dt19)) 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
t19 is Relation-like NAT -defined REAL -valued Function-like finite FinSequence-like FinSubsequence-like countable FinSequence of NAT
t is Relation-like Function-like DecoratedTree-like set
k with-replacement (t19,t) is Relation-like Function-like DecoratedTree-like set
a is Relation-like Function-like DecoratedTree-like set
{ (card b₁) where b₁ is Relation-like Function-like non empty finite countable DecoratedTree-like Element of the Sorts of (FreeEnv A) . v : verum } is set
o9 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 o9 is epsilon-transitive epsilon-connected ordinal natural V28() real finite cardinal countable ext-real non negative V136() V137() set
o is Relation-like Function-like non empty finite countable DecoratedTree-like Element of the Sorts of (FreeEnv A) . v
card o 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
q is non empty finite countable complex-membered ext-real-membered real-membered V149() V150() V151() V152() V153() 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
SortsWithConstants IIG is Element of bool the carrier of IIG
(InnerVertices IIG) \ (SortsWithConstants IIG) is 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 finite countable set
(IIG,A,v) is epsilon-transitive epsilon-connected ordinal natural V28() real finite cardinal countable ext-real non negative 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 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
InputVertices IIG is 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) /\ (InnerVertices IIG) is Element of bool the carrier of IIG
(InputVertices IIG) \/ (SortsWithConstants IIG) is Element of bool 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 * 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 * (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))
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
{ b₁ where b₁ 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 b₂ being set st
( b₂ in the Sorts of A . v & b₁ = root-tree [b₂,v] ) or ex b₂ being Element of the carrier' of IIG st
( [b₂, the carrier of IIG] = b₁ . {} & the_result_sort_of b₂ = v ) ) } is set
s1 is non empty finite countable set
card s1 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
Y1 is Element of the carrier' of IIG
[Y1, the carrier of IIG] is set
{Y1, the carrier of IIG} is non empty finite countable set
{Y1} is non empty trivial finite 1 -element countable set
{{Y1, the carrier of IIG},{Y1}} is non empty finite V34() countable set
NonTerminals (DTConMSA the Sorts of A) is non empty Element of bool the carrier of (DTConMSA the Sorts of A)
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
av is Relation-like the carrier of (DTConMSA the Sorts of A) -valued Function-like DecoratedTree-like Element of TS (DTConMSA the Sorts of A)
av . {} is set
s is set
[s,v] is set
{s,v} is non empty finite countable set
{s} is non empty trivial finite 1 -element countable set
{{s,v},{s}} is non empty finite V34() countable set
root-tree [s,v] is Relation-like Function-like finite countable DecoratedTree-like set
x is Element of the carrier' of IIG
[x, the carrier of IIG] is set
{x, the carrier of IIG} is non empty finite countable set
{x} is non empty trivial finite 1 -element countable set
{{x, the carrier of IIG},{x}} is non empty finite V34() countable set
the_result_sort_of x is Element of the carrier of IIG
s is set
[s,v] is set
{s,v} is non empty finite countable set
{s} is non empty trivial finite 1 -element countable set
{{s,v},{s}} is non empty finite V34() countable set
root-tree [s,v] is Relation-like Function-like finite countable DecoratedTree-like set
t1 is Element of NonTerminals (DTConMSA the Sorts of A)
x 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)
t1 -tree x 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 x 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)
Y is Relation-like NAT -defined Function-like finite FinSequence-like FinSubsequence-like countable DTree-yielding set
[(action_at v), the carrier of IIG] -tree Y is Relation-like Function-like DecoratedTree-like set
t is set
t is Element of the carrier' of IIG
[t, the carrier of IIG] is set
{t, the carrier of IIG} is non empty finite countable set
{t} is non empty trivial finite 1 -element countable set
{{t, the carrier of IIG},{t}} is non empty finite V34() countable set
the_result_sort_of t is Element of the carrier of IIG
t is Element of the carrier' of IIG
[t, the carrier of IIG] is set
{t, the carrier of IIG} is non empty finite countable set
{t} is non empty trivial finite 1 -element countable set
{{t, the carrier of IIG},{t}} is non empty finite V34() countable set
the_result_sort_of t is Element of the carrier of IIG
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
SortsWithConstants IIG is Element of bool the carrier of IIG
(InnerVertices IIG) \ (SortsWithConstants IIG) is 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 finite countable set
(IIG,A,v) is epsilon-transitive epsilon-connected ordinal natural V28() real finite cardinal countable ext-real non negative 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
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
s1 is Relation-like NAT -defined Function-like finite FinSequence-like FinSubsequence-like countable DTree-yielding set
[(action_at v), the carrier of IIG] -tree s1 is Relation-like Function-like DecoratedTree-like set
IIG is non empty non void V51() 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
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
v1 is Element of the Sorts of (FreeEnv A) . v
s1 is Relation-like Function-like non empty finite countable DecoratedTree-like Element of the Sorts of (FreeMSA the Sorts of A) . v
depth s1 is epsilon-transitive epsilon-connected ordinal natural V28() real finite cardinal countable ext-real non negative set
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
t1 is Relation-like Function-like non empty finite countable DecoratedTree-like Element of the Sorts of (FreeMSA the Sorts of A) . 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
depth t1 is epsilon-transitive epsilon-connected ordinal natural V28() real finite cardinal countable ext-real non negative set
av is Relation-like Function-like non empty finite countable DecoratedTree-like Element of the Sorts of (FreeMSA the Sorts of A) . v
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
depth av is epsilon-transitive epsilon-connected ordinal natural V28() real finite cardinal countable ext-real non negative 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
v is Element of the carrier of IIG
v1 is Element of the carrier of IIG
action_at v is Element of the carrier' of IIG
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)
rng (the_arity_of (action_at v)) is finite countable Element of bool the carrier of IIG
(IIG,A,v) is epsilon-transitive epsilon-connected ordinal natural V28() real finite cardinal countable ext-real non negative set
(IIG,A,v1) is epsilon-transitive epsilon-connected ordinal natural V28() real finite cardinal countable ext-real non negative set
s1 is Element of the carrier' of IIG
the_arity_of s1 is Relation-like NAT -defined the carrier of IIG -valued Function-like finite FinSequence-like FinSubsequence-like countable Element of the carrier of IIG *
dom (the_arity_of s1) is finite countable complex-membered ext-real-membered real-membered rational-membered integer-membered natural-membered V151() V152() V153() Element of bool NAT
Y1 is set
(the_arity_of s1) . Y1 is set
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
t1 - 1 is V28() real ext-real Element of REAL
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
av + 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*> is Relation-like NAT -defined NAT -valued Function-like constant non empty trivial finite 1 -element FinSequence-like FinSubsequence-like countable FinSequence of NAT
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
the Sorts of (FreeEnv A) . v is non empty finite countable set
{ (card b₁) where b₁ is Relation-like Function-like non empty finite countable DecoratedTree-like Element of the Sorts of (FreeEnv A) . v : verum } is set
x 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 x is epsilon-transitive epsilon-connected ordinal natural V28() real finite cardinal countable ext-real non negative V136() V137() set
Y is non empty finite countable complex-membered ext-real-membered real-membered V149() V150() V151() V152() V153() set
max Y is V28() real ext-real set
t is Relation-like Function-like non empty finite countable DecoratedTree-like Element of the Sorts of (FreeEnv A) . v
card t 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
SortsWithConstants IIG is Element of bool the carrier of IIG
{ b₁ where b₁ is Element of the carrier of IIG : b₁ is with_const_op } is set
k is Element of the carrier of IIG
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
k1 is Element of the carrier' of IIG
the Arity of IIG . k1 is Relation-like NAT -defined Function-like finite FinSequence-like FinSubsequence-like countable set
the ResultSort of IIG . k1 is set
the_result_sort_of k1 is Element of the carrier of IIG
the_result_sort_of s1 is Element of the carrier of IIG
f is Relation-like NAT -defined Function-like finite FinSequence-like FinSubsequence-like countable set
dom f is finite countable complex-membered ext-real-membered real-membered rational-membered integer-membered natural-membered V151() V152() V153() Element of bool NAT
(InnerVertices IIG) \ (SortsWithConstants IIG) is Element of bool the carrier of IIG
[s1, the carrier of IIG] is set
{s1, the carrier of IIG} is non empty finite countable set
{s1} is non empty trivial finite 1 -element countable set
{{s1, the carrier of IIG},{s1}} is non empty finite V34() countable set
k is Relation-like NAT -defined Function-like finite FinSequence-like FinSubsequence-like countable DTree-yielding set
[s1, the carrier of IIG] -tree k is Relation-like Function-like DecoratedTree-like set
the Sorts of (FreeEnv A) . (the_result_sort_of s1) is non empty finite countable set
len k 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
len (the_arity_of 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
dom k is finite countable complex-membered ext-real-membered real-membered rational-membered integer-membered natural-membered V151() V152() V153() Element of bool NAT
k1 is Relation-like Function-like finite countable DecoratedTree-like set
dom k1 is non empty finite countable Tree-like set
the Sorts of (FreeEnv A) . v1 is non empty finite countable set
{ (card b₁) where b₁ is Relation-like Function-like non empty finite countable DecoratedTree-like Element of the Sorts of (FreeEnv A) . v1 : verum } is set
tft 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 tft is epsilon-transitive epsilon-connected ordinal natural V28() real finite cardinal countable ext-real non negative V136() V137() set
e9 is non empty finite countable complex-membered ext-real-membered real-membered V149() V150() V151() V152() V153() set
max e9 is V28() real ext-real set
dt19 is Relation-like Function-like non empty finite countable DecoratedTree-like Element of the Sorts of (FreeEnv A) . v1
card dt19 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
t19 is Relation-like Function-like finite countable DecoratedTree-like set
dom t19 is non empty finite countable Tree-like set
s is Relation-like NAT -defined REAL -valued Function-like finite FinSequence-like FinSubsequence-like countable FinSequence of NAT
o9 is Relation-like NAT -defined Function-like finite FinSequence-like FinSubsequence-like countable DTree-yielding set
doms o9 is Relation-like NAT -defined Function-like finite FinSequence-like FinSubsequence-like countable Tree-yielding set
tree (doms o9) is non empty Tree-like set
o is Relation-like NAT -defined NAT -valued Function-like finite FinSequence-like FinSubsequence-like countable Element of dom k1
k1 with-replacement (o,t19) is Relation-like Function-like finite countable DecoratedTree-like set
f is non empty finite countable Tree-like set
o9 is Relation-like Function-like finite countable set
dom o9 is finite countable set
card f 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
q is Relation-like NAT -defined NAT -valued Function-like finite FinSequence-like FinSubsequence-like countable Element of f
f | q is non empty finite countable Tree-like set
card (f | q) 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
a is non empty finite countable Tree-like set
f with-replacement (q,a) is non empty finite countable Tree-like set
q9 is non empty finite countable Tree-like set
card q9 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
(card q9) + (card (f | q)) 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
card a 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
(card f) + (card a) 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
(card (f | q)) + (card a) 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
card t19 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 omega
k . t1 is set
(the_arity_of s1) . t1 is set
the Sorts of (FreeEnv A) . ((the_arity_of s1) . t1) is set
qq is Relation-like Function-like non empty finite countable DecoratedTree-like Element of the Sorts of (FreeEnv A) . v
card qq 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
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
v is Element of the carrier of IIG
(IIG,A,v) is epsilon-transitive epsilon-connected ordinal natural V28() real finite cardinal countable ext-real non negative set
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
the Sorts of (FreeEnv A) . v is non empty finite countable set
{ (card b₁) where b₁ is Relation-like Function-like non empty finite countable DecoratedTree-like Element of the Sorts of (FreeEnv A) . v : verum } is set
v1 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 v1 is epsilon-transitive epsilon-connected ordinal natural V28() real finite cardinal countable ext-real non negative V136() V137() set
s1 is non empty finite countable complex-membered ext-real-membered real-membered V149() V150() V151() V152() V153() set
max s1 is V28() real ext-real set
Y1 is Relation-like Function-like non empty finite countable DecoratedTree-like Element of the Sorts of (FreeEnv A) . v
card Y1 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
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 finite countable 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
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)
(IIG,A,v) is epsilon-transitive epsilon-connected ordinal natural V28() real finite cardinal countable ext-real non negative 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
s1 is Relation-like NAT -defined Function-like finite FinSequence-like FinSubsequence-like countable DTree-yielding set
[(action_at v), the carrier of IIG] -tree s1 is Relation-like Function-like DecoratedTree-like set
dom s1 is finite countable complex-membered ext-real-membered real-membered rational-membered integer-membered natural-membered V151() V152() V153() Element of bool NAT
{ (card b₁) where b₁ is Relation-like Function-like non empty finite countable DecoratedTree-like Element of the Sorts of (FreeEnv A) . v : verum } is 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
max Y1 is epsilon-transitive epsilon-connected ordinal natural V28() real finite cardinal countable ext-real non negative V136() V137() set
av is finite countable set
card 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 omega
s is ext-real set
t1 is non empty finite countable complex-membered ext-real-membered real-membered V149() V150() V151() V152() V153() set
x is Relation-like Function-like non empty finite countable DecoratedTree-like Element of the Sorts of (FreeEnv A) . v
card x 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
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
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
{ b₁ where b₁ 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 b₂ being set st
( b₂ in the Sorts of A . v & b₁ = root-tree [b₂,v] ) or ex b₂ being Element of the carrier' of IIG st
( [b₂, the carrier of IIG] = b₁ . {} & the_result_sort_of b₂ = v ) ) } is set
Y is Relation-like the carrier of (DTConMSA the Sorts of A) -valued Function-like DecoratedTree-like Element of TS (DTConMSA the Sorts of A)
Y . {} is set
t is set
[t,v] is set
{t,v} is non empty finite countable set
{t} is non empty trivial finite 1 -element countable set
{{t,v},{t}} is non empty finite V34() countable set
root-tree [t,v] is Relation-like Function-like finite countable DecoratedTree-like set
t is set
[t,v] is set
{t,v} is non empty finite countable set
{t} is non empty trivial finite 1 -element countable set
{{t,v},{t}} is non empty finite V34() countable set
root-tree [t,v] is Relation-like Function-like finite countable DecoratedTree-like set
[{},[t,v]] is set
{{},[t,v]} is non empty finite countable set
{{{},[t,v]},{{}}} is non empty finite V34() countable set
{[{},[t,v]]} is Relation-like Function-like constant non empty trivial finite 1 -element countable set
t is Element of the carrier' of IIG
[t, the carrier of IIG] is set
{t, the carrier of IIG} is non empty finite countable set
{t} is non empty trivial finite 1 -element countable set
{{t, the carrier of IIG},{t}} is non empty finite V34() countable set
the_result_sort_of t is Element of the carrier of IIG
t is Relation-like NAT -defined Function-like finite FinSequence-like FinSubsequence-like countable DTree-yielding set
[(action_at v), the carrier of IIG] -tree t is Relation-like Function-like DecoratedTree-like set
len 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
k is Relation-like NAT -defined Function-like finite FinSequence-like FinSubsequence-like countable set
len k 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 k 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 (action_at v) is Element of the carrier of IIG
Seg (len s1) is finite len s1 -element countable complex-membered ext-real-membered real-membered rational-membered integer-membered natural-membered V151() V152() V153() Element of bool NAT
len t 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
root-tree [(action_at v), the carrier of IIG] is Relation-like Function-like finite countable DecoratedTree-like set
len t 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
len (the_arity_of (action_at v)) 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
1 + 0 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
dom t is finite countable complex-membered ext-real-membered real-membered rational-membered integer-membered natural-membered V151() V152() V153() Element of bool NAT
dom (the_arity_of (action_at v)) is finite countable complex-membered ext-real-membered real-membered rational-membered integer-membered natural-membered V151() V152() V153() Element of bool NAT
k1 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
k . k1 is set
k1 + 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
k . (k1 + 1) is set
tft is Relation-like NAT -defined Function-like finite FinSequence-like FinSubsequence-like countable DTree-yielding set
[(action_at v), the carrier of IIG] -tree tft is Relation-like Function-like DecoratedTree-like set
e9 is finite countable set
card e9 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 omega
(the_arity_of (action_at v)) /. 1 is Element of the carrier of IIG
the Sorts of (FreeEnv A) . ((the_arity_of (action_at v)) /. 1) is non empty finite countable set
s1 . 1 is set
(IIG,A,((the_arity_of (action_at v)) /. 1)) is epsilon-transitive epsilon-connected ordinal natural V28() real finite cardinal countable ext-real non negative set
a is Relation-like Function-like non empty finite countable DecoratedTree-like Element of the Sorts of (FreeEnv A) . ((the_arity_of (action_at v)) /. 1)
card a 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
t | (Seg 1) is Relation-like NAT -defined Seg 1 -defined NAT -defined Function-like finite FinSubsequence-like countable set
dom (t | (Seg 1)) is finite countable complex-membered ext-real-membered real-membered rational-membered integer-membered natural-membered V151() V152() V153() Element of bool NAT
t . 1 is set
(the_arity_of (action_at v)) . 1 is set
the Sorts of (FreeEnv A) . ((the_arity_of (action_at v)) . 1) is set
o9 is Relation-like Function-like finite countable DecoratedTree-like set
dom o9 is non empty finite countable Tree-like set
<*0*> is Relation-like NAT -defined NAT -valued Function-like constant non empty trivial finite 1 -element FinSequence-like FinSubsequence-like countable FinSequence of NAT
<*0*> ^ {} is Relation-like NAT -defined Function-like non empty finite FinSequence-like FinSubsequence-like countable set
f is Relation-like Function-like finite countable DecoratedTree-like set
dom f is non empty finite countable Tree-like set
q is Relation-like NAT -defined NAT -valued Function-like finite FinSequence-like FinSubsequence-like countable Element of dom f
o is Relation-like Function-like non empty finite countable DecoratedTree-like Element of the Sorts of (FreeEnv A) . ((the_arity_of (action_at v)) /. 1)
v1 with-replacement (q,o) is Relation-like Function-like DecoratedTree-like set
0 + 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
q9 is Relation-like NAT -defined Function-like finite FinSequence-like FinSubsequence-like countable DTree-yielding set
[(action_at v), the carrier of IIG] -tree q9 is Relation-like Function-like DecoratedTree-like set
len q9 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
q9 . (0 + 1) is set
tft . 1 is set
s1 +* (t | (Seg 1)) is Relation-like Function-like finite countable set
(s1 +* (t | (Seg 1))) . 1 is set
(t | (Seg 1)) . 1 is set
qq is epsilon-transitive epsilon-connected ordinal natural V28() real finite cardinal countable ext-real non negative set
q9 . qq is set
tft . qq is set
(dom t) /\ (Seg 1) is finite countable complex-membered ext-real-membered real-membered rational-membered integer-membered natural-membered V151() V152() V153() Element of bool NAT
tft . qq is set
(s1 +* (t | (Seg 1))) . qq is set
s1 . qq is set
q9 . qq is set
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
dom (s1 +* (t | (Seg 1))) is finite countable set
(dom s1) \/ (dom (t | (Seg 1))) is finite countable complex-membered ext-real-membered real-membered rational-membered integer-membered natural-membered V151() V152() V153() Element of bool NAT
(dom t) /\ (Seg 1) is finite countable complex-membered ext-real-membered real-membered rational-membered integer-membered natural-membered V151() V152() V153() Element of bool NAT
(dom s1) \/ ((dom t) /\ (Seg 1)) is finite countable complex-membered ext-real-membered real-membered rational-membered integer-membered natural-membered V151() V152() V153() Element of bool NAT
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
dt19 is Relation-like Function-like finite countable DecoratedTree-like set
f with-replacement (q,o) is Relation-like Function-like finite countable DecoratedTree-like set
card dt19 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 omega
f | q is Relation-like Function-like finite countable DecoratedTree-like set
card (f | q) 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 omega
(card dt19) + (card (f | q)) 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
card f 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 omega
card o 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
(card f) + (card o) 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
{ (card b₁) where b₁ is Relation-like Function-like non empty finite countable DecoratedTree-like Element of the Sorts of (FreeEnv A) . ((the_arity_of (action_at v)) /. 1) : verum } is set
qq 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 qq is epsilon-transitive epsilon-connected ordinal natural V28() real finite cardinal countable ext-real non negative V136() V137() set
tft is non empty finite countable complex-membered ext-real-membered real-membered V149() V150() V151() V152() V153() set
(the_arity_of (action_at v)) /. (k1 + 1) is Element of the carrier of IIG
Seg k1 is finite k1 -element countable complex-membered ext-real-membered real-membered rational-membered integer-membered natural-membered V151() V152() V153() Element of bool NAT
t | (Seg k1) is Relation-like NAT -defined Seg k1 -defined NAT -defined Function-like finite FinSubsequence-like countable set
dom (t | (Seg k1)) is finite countable complex-membered ext-real-membered real-membered rational-membered integer-membered natural-membered V151() V152() V153() Element of bool NAT
(dom t) /\ (Seg k1) is finite countable complex-membered ext-real-membered real-membered rational-membered integer-membered natural-membered V151() V152() V153() Element of bool NAT
s1 . (k1 + 1) is set
(the_arity_of (action_at v)) . (k1 + 1) is set
the Sorts of (FreeEnv A) . ((the_arity_of (action_at v)) . (k1 + 1)) is set
the Sorts of (FreeEnv A) . ((the_arity_of (action_at v)) /. (k1 + 1)) is non empty finite countable set
Seg (k1 + 1) is non empty finite k1 + 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
t | (Seg (k1 + 1)) is Relation-like NAT -defined Seg (k1 + 1) -defined NAT -defined Function-like finite FinSubsequence-like countable set
dom (t | (Seg (k1 + 1))) is finite countable complex-membered ext-real-membered real-membered rational-membered integer-membered natural-membered V151() V152() V153() Element of bool NAT
s1 +* (t | (Seg k1)) is Relation-like Function-like finite countable set
o is Relation-like Function-like set
dom o is set
dom (s1 +* (t | (Seg k1))) is finite countable set
(dom s1) \/ (dom (t | (Seg k1))) is finite countable complex-membered ext-real-membered real-membered rational-membered integer-membered natural-membered V151() V152() V153() Element of bool NAT
(dom s1) \/ ((dom t) /\ (Seg k1)) 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 Function-like finite FinSequence-like FinSubsequence-like countable set
dom o9 is finite countable complex-membered ext-real-membered real-membered rational-membered integer-membered natural-membered V151() V152() V153() Element of bool NAT
q is set
o9 . q is set
q9 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 (action_at v)) /. q9 is Element of the carrier of IIG
o9 . q9 is set
t . q9 is set
s1 . q9 is set
(s1 +* (t | (Seg k1))) . q9 is set
(t | (Seg k1)) . q9 is set
(s1 +* (t | (Seg k1))) . q9 is set
(the_arity_of (action_at v)) . q9 is set
the Sorts of (FreeEnv A) . ((the_arity_of (action_at v)) . q9) is set
the Sorts of (FreeEnv A) . ((the_arity_of (action_at v)) /. q9) is non empty finite countable set
tft is Relation-like Function-like non empty finite countable DecoratedTree-like Element of the Sorts of (FreeEnv A) . ((the_arity_of (action_at v)) /. q9)
q is set
o9 . q is set
q is Relation-like NAT -defined Function-like finite FinSequence-like FinSubsequence-like countable DTree-yielding set
len q 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
q . (k1 + 1) is set
(s1 +* (t | (Seg k1))) . (k1 + 1) is set
q9 is set
doms q is Relation-like NAT -defined Function-like finite FinSequence-like FinSubsequence-like countable Tree-yielding set
dom (doms q) is finite countable complex-membered ext-real-membered real-membered rational-membered integer-membered natural-membered V151() V152() V153() Element of bool NAT
dom q is finite countable complex-membered ext-real-membered real-membered rational-membered integer-membered natural-membered V151() V152() V153() Element of bool NAT
q . q9 is set
qq is Relation-like Function-like finite countable DecoratedTree-like set
dom qq is non empty finite countable Tree-like set
(doms q) . q9 is set
q9 is Relation-like NAT -defined Function-like finite FinSequence-like FinSubsequence-like countable Tree-yielding FinTree-yielding set
tree q9 is non empty finite countable Tree-like set
[(action_at v), the carrier of IIG] -tree q is Relation-like Function-like DecoratedTree-like set
dom ([(action_at v), the carrier of IIG] -tree q) is non empty Tree-like set
tft is Relation-like NAT -defined Function-like finite FinSequence-like FinSubsequence-like countable DTree-yielding set
doms tft is Relation-like NAT -defined Function-like finite FinSequence-like FinSubsequence-like countable Tree-yielding set
tree (doms tft) is non empty Tree-like set
(IIG,A,((the_arity_of (action_at v)) /. (k1 + 1))) is epsilon-transitive epsilon-connected ordinal natural V28() real finite cardinal countable ext-real non negative set
tft is Relation-like Function-like non empty finite countable DecoratedTree-like Element of the Sorts of (FreeEnv A) . ((the_arity_of (action_at v)) /. (k1 + 1))
card tft 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
a is Relation-like Function-like non empty finite countable DecoratedTree-like Element of the Sorts of (FreeEnv A) . ((the_arity_of (action_at v)) /. (k1 + 1))
t . (k1 + 1) is set
dtft is Relation-like Function-like finite countable DecoratedTree-like set
dom dtft is non empty finite countable Tree-like set
<*k1*> is Relation-like NAT -defined NAT -valued Function-like constant non empty trivial finite 1 -element FinSequence-like FinSubsequence-like countable FinSequence of NAT
<*k1*> ^ {} is Relation-like NAT -defined Function-like non empty finite FinSequence-like FinSubsequence-like countable set
qq is Relation-like Function-like finite countable DecoratedTree-like set
dom qq is non empty finite countable Tree-like set
e9 is Relation-like Function-like non empty finite countable DecoratedTree-like Element of the Sorts of (FreeEnv A) . ((the_arity_of (action_at v)) /. (k1 + 1))
qq with-replacement (<*k1*>,e9) is Relation-like Function-like DecoratedTree-like set
dttft is Relation-like NAT -defined Function-like finite FinSequence-like FinSubsequence-like countable DTree-yielding set
[(action_at v), the carrier of IIG] -tree dttft is Relation-like Function-like DecoratedTree-like set
len dttft 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
dttft . (k1 + 1) is set
tft . (k1 + 1) is set
s1 +* (t | (Seg (k1 + 1))) is Relation-like Function-like finite countable set
(s1 +* (t | (Seg (k1 + 1)))) . (k1 + 1) is set
(t | (Seg (k1 + 1))) . (k1 + 1) is set
ttft is epsilon-transitive epsilon-connected ordinal natural V28() real finite cardinal countable ext-real non negative set
dttft . ttft is set
tft . ttft is set
(dom t) /\ (Seg (k1 + 1)) is finite countable complex-membered ext-real-membered real-membered rational-membered integer-membered natural-membered V151() V152() V153() Element of bool NAT
tft . ttft is set
(s1 +* (t | (Seg (k1 + 1)))) . ttft is set
s1 . ttft is set
(s1 +* (t | (Seg k1))) . ttft is set
q . ttft is set
dttft . ttft is set
(dom t) /\ (Seg (k1 + 1)) is finite countable complex-membered ext-real-membered real-membered rational-membered integer-membered natural-membered V151() V152() V153() Element of bool NAT
tft . ttft is set
(s1 +* (t | (Seg (k1 + 1)))) . ttft is set
(t | (Seg (k1 + 1))) . ttft is set
t . ttft is set
(t | (Seg k1)) . ttft is set
(s1 +* (t | (Seg k1))) . ttft is set
q . ttft is set
dttft . ttft is set
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
dom (s1 +* (t | (Seg (k1 + 1)))) is finite countable set
(dom s1) \/ (dom (t | (Seg (k1 + 1)))) is finite countable complex-membered ext-real-membered real-membered rational-membered integer-membered natural-membered V151() V152() V153() Element of bool NAT
(dom t) /\ (Seg (k1 + 1)) is finite countable complex-membered ext-real-membered real-membered rational-membered integer-membered natural-membered V151() V152() V153() Element of bool NAT
(dom s1) \/ ((dom t) /\ (Seg (k1 + 1))) is finite countable complex-membered ext-real-membered real-membered rational-membered integer-membered natural-membered V151() V152() V153() Element of bool NAT
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
dt19 is Relation-like Function-like finite countable DecoratedTree-like set
ttft is Relation-like NAT -defined NAT -valued Function-like finite FinSequence-like FinSubsequence-like countable Element of dom qq
qq with-replacement (ttft,e9) is Relation-like Function-like finite countable DecoratedTree-like set
card dt19 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 omega
qq | ttft is Relation-like Function-like finite countable DecoratedTree-like set
card (qq | ttft) 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 omega
(card dt19) + (card (qq | ttft)) 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
card qq 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 omega
card e9 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
(card qq) + (card e9) 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
{ (card b₁) where b₁ is Relation-like Function-like non empty finite countable DecoratedTree-like Element of the Sorts of (FreeEnv A) . ((the_arity_of (action_at v)) /. (k1 + 1)) : verum } is set
f9 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 f9 is epsilon-transitive epsilon-connected ordinal natural V28() real finite cardinal countable ext-real non negative V136() V137() set
S1 is non empty finite countable complex-membered ext-real-membered real-membered V149() V150() V151() V152() V153() set
k . 0 is set
k1 is Relation-like NAT -defined Function-like finite FinSequence-like FinSubsequence-like countable DTree-yielding set
f is finite countable set
[(action_at v), the carrier of IIG] -tree k1 is Relation-like Function-like DecoratedTree-like set
card f 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 omega
k . (len s1) is set
t | (dom s1) is Relation-like NAT -defined dom s1 -defined NAT -defined Function-like finite FinSubsequence-like countable set
s1 +* (t | (dom s1)) is Relation-like Function-like finite countable set
s1 +* t is Relation-like Function-like finite countable set
len t 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
t is set
[t,v] is set
{t,v} is non empty finite countable set
{t} is non empty trivial finite 1 -element countable set
{{t,v},{t}} is non empty finite V34() countable set
root-tree [t,v] is Relation-like Function-like finite countable DecoratedTree-like set
k is Element of the carrier' of IIG
[k, the carrier of IIG] is set
{k, the carrier of IIG} is non empty finite countable set
{k} is non empty trivial finite 1 -element countable set
{{k, the carrier of IIG},{k}} is non empty finite V34() countable set
the_result_sort_of k is Element of the carrier of IIG
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 finite countable set
{ (IIG,A,v,b₁) where b₁ is Element of the Sorts of (FreeEnv A) . v : verum } is set
{ H₁(b₁) where b₁ is Element of the Sorts of (FreeEnv A) . v : S₁[b₁] } is set
the Element of the Sorts of (FreeEnv A) . v is Element of the Sorts of (FreeEnv A) . v
(IIG,A,v, the Element of the Sorts of (FreeEnv A) . v) 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 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 finite non void V51() Circuit-like monotonic ManySortedSign
the carrier of IIG is non empty finite countable set
A is non-empty finitely-generated finite-yielding MSAlgebra over IIG
{ (IIG,A,b₁) where b₁ is Element of the carrier of IIG : b₁ in the carrier of IIG } is set
{ H₁(b₁) where b₁ is Element of the carrier of IIG : b₁ in the carrier of IIG } is set
v1 is set
s1 is Element of the carrier of IIG
(IIG,A,s1) is epsilon-transitive epsilon-connected ordinal natural V28() real finite cardinal countable ext-real non negative set
the Element of the carrier of IIG is Element of the carrier of IIG
(IIG,A, the Element of the carrier of IIG) is epsilon-transitive epsilon-connected ordinal natural V28() real finite cardinal countable ext-real non negative set
s1 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 s1 is epsilon-transitive epsilon-connected ordinal natural V28() real finite cardinal countable ext-real non negative V136() V137() set
s1 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
v is epsilon-transitive epsilon-connected ordinal natural V28() real finite cardinal countable ext-real non negative set
max s1 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
IIG is non empty finite non void V51() Circuit-like monotonic ManySortedSign
the carrier of IIG is non empty finite countable set
A is non-empty finitely-generated finite-yielding MSAlgebra over IIG
(IIG,A) is epsilon-transitive epsilon-connected ordinal natural V28() real finite cardinal countable ext-real non negative set
v is Element of the carrier of IIG
(IIG,A,v) is epsilon-transitive epsilon-connected ordinal natural V28() real finite cardinal countable ext-real non negative set
{ (IIG,A,b₁) where b₁ is Element of the carrier of IIG : b₁ in the carrier of IIG } is set
v1 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 v1 is epsilon-transitive epsilon-connected ordinal natural V28() real finite cardinal countable ext-real non negative V136() V137() set
s1 is non empty finite countable complex-membered ext-real-membered real-membered V149() V150() V151() V152() V153() 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
A is non-empty finitely-generated finite-yielding MSAlgebra over IIG
v is Element of the carrier of IIG
(IIG,A,v) is epsilon-transitive epsilon-connected ordinal natural V28() real finite cardinal countable ext-real non negative set
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
the Sorts of (FreeEnv A) . v is non empty finite countable set
{ (IIG,A,v,b₁) where b₁ is Relation-like Function-like non empty finite countable DecoratedTree-like Element of the Sorts of (FreeEnv A) . v : verum } is set
v1 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 v1 is epsilon-transitive epsilon-connected ordinal natural V28() real finite cardinal countable ext-real non negative V136() V137() set
s1 is non empty finite countable complex-membered ext-real-membered real-membered V149() V150() V151() V152() V153() set
max s1 is V28() real ext-real set
{ (card b₁) where b₁ is Relation-like Function-like non empty finite countable DecoratedTree-like Element of the Sorts of (FreeEnv A) . v : verum } is set
(IIG,A,v) is epsilon-transitive epsilon-connected ordinal natural V28() real finite cardinal countable ext-real non negative 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
max Y1 is epsilon-transitive epsilon-connected ordinal natural V28() real finite cardinal countable ext-real non negative V136() V137() set
av is Relation-like Function-like non empty finite countable DecoratedTree-like Element of the Sorts of (FreeEnv A) . v
(IIG,A,v,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
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
x is Relation-like Function-like non empty finite countable DecoratedTree-like Element of the Sorts of (FreeMSA the Sorts of A) . v
depth x is epsilon-transitive epsilon-connected ordinal natural V28() real finite cardinal countable ext-real non negative set
Y is Relation-like Function-like finite countable DecoratedTree-like set
t is non empty finite countable Tree-like set
dom Y is non empty finite countable Tree-like set
height t 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
k is Relation-like NAT -defined REAL -valued Function-like finite FinSequence-like FinSubsequence-like countable FinSequence of NAT
len k 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 is Relation-like Function-like set
k1 is set
[k,k1] is set
{k,k1} is non empty finite countable set
{k} is functional non empty trivial finite V34() 1 -element with_common_domain countable set
{{k,k1},{k}} is non empty finite V34() countable set
t1 is non empty finite countable complex-membered ext-real-membered real-membered V149() V150() V151() V152() V153() set
f is ext-real set
tft is Relation-like Function-like non empty finite countable DecoratedTree-like Element of the Sorts of (FreeEnv A) . v
card tft 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
(IIG,A,v,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
e9 is Relation-like Function-like non empty finite countable DecoratedTree-like Element of the Sorts of (FreeMSA the Sorts of A) . v
depth e9 is epsilon-transitive epsilon-connected ordinal natural V28() real finite cardinal countable ext-real non negative set
rng tft is non empty finite countable set
tft . {} is set
{(tft . {})} is non empty trivial finite 1 -element countable set
dt19 is Relation-like Function-like finite countable DecoratedTree-like set
t19 is non empty finite countable Tree-like set
dom dt19 is non empty finite countable Tree-like set
height t19 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 set
{{},(tft . {})} is non empty finite countable set
{{{},(tft . {})},{{}}} is non empty finite V34() countable set
{[{},(tft . {})]} is Relation-like Function-like constant non empty trivial finite 1 -element countable set
dt19 is Relation-like Function-like finite countable DecoratedTree-like set
t19 is non empty finite countable Tree-like set
dom dt19 is non empty finite countable Tree-like set
height t19 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
rng s is set
av . {} is set
{(av . {})} is non empty trivial finite 1 -element countable set
[{},(av . {})] is set
{{},(av . {})} is non empty finite countable set
{{{},(av . {})},{{}}} is non empty finite V34() countable set
{[{},(av . {})]} is Relation-like Function-like constant non empty trivial finite 1 -element countable set
card av 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
(InputVertices IIG) \/ (SortsWithConstants IIG) is Element of bool the carrier of IIG
card av 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
dom av is non empty finite countable Tree-like set
tft is set
[{},tft] is set
{{},tft} is non empty finite countable set
{{{},tft},{{}}} is non empty finite V34() countable set
(InputVertices IIG) \/ (SortsWithConstants IIG) is Element of bool the carrier of IIG
f is V28() real ext-real Element of REAL
0 + 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
e9 is set
{e9} is non empty trivial finite 1 -element countable 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
v is Element of the carrier of IIG
v1 is Element of the carrier of IIG
action_at v is Element of the carrier' of IIG
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)
rng (the_arity_of (action_at v)) is finite countable Element of bool the carrier of IIG
(IIG,A,v) is epsilon-transitive epsilon-connected ordinal natural V28() real finite cardinal countable ext-real non negative set
(IIG,A,v1) is epsilon-transitive epsilon-connected ordinal natural V28() real finite cardinal countable ext-real non negative set
(IIG,A,v1) is epsilon-transitive epsilon-connected ordinal natural V28() real finite cardinal countable ext-real non negative set
0 + 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
(IIG,A,v) is epsilon-transitive epsilon-connected ordinal natural V28() real finite cardinal countable ext-real non negative set
InputVertices IIG is 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
(InnerVertices IIG) \ (SortsWithConstants IIG) is Element of bool the carrier of 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
the Sorts of (FreeEnv A) . v1 is non empty finite countable set
{ (IIG,A,v1,b₁) where b₁ is Relation-like Function-like non empty finite countable DecoratedTree-like Element of the Sorts of (FreeEnv A) . v1 : verum } is set
s1 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 s1 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 V149() V150() V151() V152() V153() set
max Y1 is V28() real ext-real set
t1 is Relation-like Function-like non empty finite countable DecoratedTree-like Element of the Sorts of (FreeEnv A) . v1
(IIG,A,v1,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
the Sorts of (FreeEnv A) . v is non empty finite countable set
{ (IIG,A,v,b₁) where b₁ is Relation-like Function-like non empty finite countable DecoratedTree-like Element of the Sorts of (FreeEnv A) . v : verum } is set
s 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 s is epsilon-transitive epsilon-connected ordinal natural V28() real finite cardinal countable ext-real non negative V136() V137() set
av is Element of the carrier' of IIG
the_arity_of av is Relation-like NAT -defined the carrier of IIG -valued Function-like finite FinSequence-like FinSubsequence-like countable Element of the carrier of IIG *
dom (the_arity_of av) is finite countable complex-membered ext-real-membered real-membered rational-membered integer-membered natural-membered V151() V152() V153() Element of bool NAT
x is set
(the_arity_of av) . x is set
Y is non empty finite countable complex-membered ext-real-membered real-membered V149() V150() V151() V152() V153() set
max Y is V28() real ext-real set
t is Relation-like Function-like non empty finite countable DecoratedTree-like Element of the Sorts of (FreeEnv A) . v
(IIG,A,v,t) 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
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
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
{ b₁ where b₁ 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 b₂ being set st
( b₂ in the Sorts of A . v & b₁ = root-tree [b₂,v] ) or ex b₂ being Element of the carrier' of IIG st
( [b₂, the carrier of IIG] = b₁ . {} & the_result_sort_of b₂ = v ) ) } is set
k 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
k - 1 is V28() real ext-real Element of REAL
k1 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
<*k1*> is Relation-like NAT -defined NAT -valued Function-like constant non empty trivial finite 1 -element FinSequence-like FinSubsequence-like countable FinSequence of NAT
k1 + 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
f is Relation-like NAT -defined REAL -valued Function-like finite FinSequence-like FinSubsequence-like countable FinSequence of NAT
t with-replacement (f,t1) is Relation-like Function-like DecoratedTree-like 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) . v1 is non empty set
e9 is Relation-like Function-like non empty finite countable DecoratedTree-like Element of the Sorts of (FreeMSA the Sorts of A) . v1
depth e9 is epsilon-transitive epsilon-connected ordinal natural V28() real finite cardinal countable ext-real non negative set
dt19 is Relation-like Function-like finite countable DecoratedTree-like set
t19 is non empty finite countable Tree-like set
dom dt19 is non empty finite countable Tree-like set
height t19 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 the carrier of (DTConMSA the Sorts of A) -valued Function-like DecoratedTree-like Element of TS (DTConMSA the Sorts of A)
a . {} is set
o is set
[o,v] is set
{o,v} is non empty finite countable set
{o} is non empty trivial finite 1 -element countable set
{{o,v},{o}} is non empty finite V34() countable set
root-tree [o,v] is Relation-like Function-like finite countable DecoratedTree-like set
the Sorts of (FreeMSA the Sorts of A) . v is non empty set
o9 is Relation-like Function-like non empty finite countable DecoratedTree-like Element of the Sorts of (FreeMSA the Sorts of A) . v
depth o9 is epsilon-transitive epsilon-connected ordinal natural V28() real finite cardinal countable ext-real non negative set
q is Relation-like Function-like finite countable DecoratedTree-like set
q9 is non empty finite countable Tree-like set
dom q is non empty finite countable Tree-like set
height q9 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
o is set
[o,v] is set
{o,v} is non empty finite countable set
{o} is non empty trivial finite 1 -element countable set
{{o,v},{o}} is non empty finite V34() countable set
root-tree [o,v] is Relation-like Function-like finite countable DecoratedTree-like set
o9 is Element of the carrier' of IIG
[o9, the carrier of IIG] is set
{o9, the carrier of IIG} is non empty finite countable set
{o9} is non empty trivial finite 1 -element countable set
{{o9, the carrier of IIG},{o9}} is non empty finite V34() countable set
the_result_sort_of o9 is Element of the carrier of IIG
o is Element of the carrier' of IIG
[o, the carrier of IIG] is set
{o, the carrier of IIG} is non empty finite countable set
{o} is non empty trivial finite 1 -element countable set
{{o, the carrier of IIG},{o}} is non empty finite V34() countable set
the_result_sort_of o is Element of the carrier of IIG
NonTerminals (DTConMSA the Sorts of A) is non empty Element of bool the carrier of (DTConMSA the Sorts of A)
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
o9 is Element of NonTerminals (DTConMSA the Sorts of A)
q 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)
o9 -tree q 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 q 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)
dom a is non empty finite countable Tree-like set
q9 is Relation-like NAT -defined Function-like finite FinSequence-like FinSubsequence-like countable DTree-yielding set
doms q9 is Relation-like NAT -defined Function-like finite FinSequence-like FinSubsequence-like countable Tree-yielding set
tree (doms q9) is non empty Tree-like set
[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
[av, the carrier of IIG] -tree q9 is Relation-like Function-like DecoratedTree-like set
len q9 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
len (the_arity_of 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
dom q9 is finite countable complex-membered ext-real-membered real-membered rational-membered integer-membered natural-membered V151() V152() V153() Element of bool NAT
qq is Relation-like NAT -defined Function-like finite FinSequence-like FinSubsequence-like countable DTree-yielding set
o9 -tree qq is Relation-like Function-like DecoratedTree-like set
len qq 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
qq . (k1 + 1) is set
dom qq is finite countable complex-membered ext-real-membered real-membered rational-membered integer-membered natural-membered V151() V152() V153() Element of bool NAT
q9 . k is set
tft is Relation-like Function-like DecoratedTree-like set
tft is Relation-like Function-like non empty finite countable DecoratedTree-like Element of the Sorts of (FreeEnv A) . v
(IIG,A,v,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
dtft is V28() real ext-real Element of REAL
e9 is Relation-like Function-like non empty finite countable DecoratedTree-like Element of the Sorts of (FreeMSA the Sorts of A) . v
depth e9 is epsilon-transitive epsilon-connected ordinal natural V28() real finite cardinal countable ext-real non negative set
dttft is Relation-like Function-like finite countable DecoratedTree-like set
ttft is non empty finite countable Tree-like set
dom dttft is non empty finite countable Tree-like set
height ttft 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 tft is non empty finite countable Tree-like set
S1 is Relation-like NAT -defined Function-like finite FinSequence-like FinSubsequence-like countable DTree-yielding set
doms S1 is Relation-like NAT -defined Function-like finite FinSequence-like FinSubsequence-like countable Tree-yielding set
tree (doms S1) is non empty Tree-like set
dom t is non empty finite countable Tree-like set
dom t1 is non empty finite countable Tree-like set
(dom t) with-replacement (f,(dom t1)) is non empty Tree-like set
f9 is Relation-like NAT -defined NAT -valued Function-like finite FinSequence-like FinSubsequence-like countable Element of ttft
ttft | f is non empty Tree-like set