:: CIRCUIT2 semantic presentation

REAL is V150() V151() V152() V156() V163() V164() V166() set
NAT is non empty non trivial V21() V22() V23() non finite cardinal limit_cardinal countable denumerable V150() V151() V152() V153() V154() V155() V156() V161() V163() Element of bool REAL
bool REAL is set
NAT is non empty non trivial V21() V22() V23() non finite cardinal limit_cardinal countable denumerable V150() V151() V152() V153() V154() V155() V156() V161() V163() set
bool NAT is non trivial non finite set
bool NAT is non trivial non finite set
K183() is set
{} is Relation-like non-empty empty-yielding NAT -defined Function-like one-to-one constant functional empty V21() V22() V23() V25() V26() V27() finite finite-yielding V32() cardinal {} -element Cardinal-yielding countable Function-yielding V42() FinSequence-like FinSubsequence-like FinSequence-membered constituted-Trees constituted-FinTrees constituted-DTrees Tree-yielding FinTree-yielding DTree-yielding V133() V134() ext-real V150() V151() V152() V153() V154() V155() V156() V163() V164() V165() V166() set
{{}} is functional non empty trivial finite V32() 1 -element with_common_domain countable V150() V151() V152() V153() V154() V155() V161() V162() V163() V164() V165() set
1 is non empty V21() V22() V23() V27() finite cardinal countable V133() V134() ext-real V148() V149() V150() V151() V152() V153() V154() V155() V161() V162() V163() V164() V165() Element of NAT
{{}} * is functional non empty FinSequence-membered M8({{}})
[:({{}} *),{{}}:] is Relation-like set
bool [:({{}} *),{{}}:] is set
PFuncs (({{}} *),{{}}) is set
{{},1} is non empty finite V32() countable V150() V151() V152() V153() V154() V155() V161() V162() V163() V164() V165() 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 L13()
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 constituted-DTrees Element of bool (FinTrees the carrier of PeanoNat)
bool (FinTrees the carrier of PeanoNat) is set
[:(TS PeanoNat),NAT:] is Relation-like set
bool [:(TS PeanoNat),NAT:] is set
[:NAT,(TS PeanoNat):] is Relation-like set
bool [:NAT,(TS PeanoNat):] is set
COMPLEX is V150() V156() set
RAT is V150() V151() V152() V153() V156() set
INT is V150() V151() V152() V153() V154() V156() set
[:COMPLEX,COMPLEX:] is Relation-like set
bool [:COMPLEX,COMPLEX:] is set
[:COMPLEX,REAL:] is Relation-like set
bool [:COMPLEX,REAL:] is set
2 is non empty V21() V22() V23() V27() finite cardinal countable V133() V134() ext-real V148() V149() V150() V151() V152() V153() V154() V155() V161() V162() V163() V164() V165() Element of NAT
3 is non empty V21() V22() V23() V27() finite cardinal countable V133() V134() ext-real V148() V149() V150() V151() V152() V153() V154() V155() V161() V162() V163() V164() V165() Element of NAT
0 is Relation-like non-empty empty-yielding NAT -defined Function-like one-to-one constant functional empty V21() V22() V23() V25() V26() V27() finite finite-yielding V32() cardinal {} -element Cardinal-yielding countable Function-yielding V42() FinSequence-like FinSubsequence-like FinSequence-membered constituted-Trees constituted-FinTrees constituted-DTrees Tree-yielding FinTree-yielding DTree-yielding V133() V134() ext-real V148() V149() V150() V151() V152() V153() V154() V155() V156() V163() V164() V165() V166() Element of NAT
K287(0) is non empty V108() set
IIG is set
IIG is non empty non void V56() 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 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
K539( the carrier of IIG, the ResultSort of IIG) is Element of bool the carrier of IIG
SCS is Relation-like non-empty non empty-yielding the carrier of IIG -defined Function-like non empty total set
FreeMSA SCS is strict non-empty MSAlgebra over IIG
the Sorts of (FreeMSA SCS) is Relation-like non-empty non empty-yielding the carrier of IIG -defined Function-like non empty total set
InpFs is Relation-like the carrier of IIG -defined Function-like non empty total Function-yielding V42() ManySortedFunction of the Sorts of (FreeMSA SCS), the Sorts of (FreeMSA SCS)
iv is Relation-like Function-like Function-yielding V42() set
dSCS is Element of the carrier of IIG
the Sorts of (FreeMSA SCS) . dSCS is non empty set
action_at dSCS is Element of the carrier' of IIG
[(action_at dSCS), the carrier of IIG] is set
the_arity_of (action_at dSCS) is Relation-like NAT -defined the carrier of IIG -valued Function-like finite countable FinSequence-like FinSubsequence-like Element of the carrier of IIG *
the carrier of IIG * is functional non empty FinSequence-membered M8( the carrier of IIG)
(the_arity_of (action_at dSCS)) * InpFs is Relation-like NAT -defined Function-like finite countable Function-yielding V42() set
InpFs . dSCS is Relation-like the Sorts of (FreeMSA SCS) . dSCS -defined the Sorts of (FreeMSA SCS) . dSCS -valued Function-like V18( the Sorts of (FreeMSA SCS) . dSCS, the Sorts of (FreeMSA SCS) . dSCS) Element of bool [:( the Sorts of (FreeMSA SCS) . dSCS),( the Sorts of (FreeMSA SCS) . dSCS):]
[:( the Sorts of (FreeMSA SCS) . dSCS),( the Sorts of (FreeMSA SCS) . dSCS):] is Relation-like set
bool [:( the Sorts of (FreeMSA SCS) . dSCS),( the Sorts of (FreeMSA SCS) . dSCS):] is set
s1 is Relation-like NAT -defined Function-like finite countable FinSequence-like FinSubsequence-like DTree-yielding set
[(action_at dSCS), the carrier of IIG] -tree s1 is Relation-like Function-like DecoratedTree-like set
iv .. s1 is Relation-like Function-like set
s2 is Relation-like Function-like non empty finite countable DecoratedTree-like Element of the Sorts of (FreeMSA SCS) . dSCS
(InpFs . dSCS) . s2 is Relation-like Function-like non empty finite countable DecoratedTree-like Element of the Sorts of (FreeMSA SCS) . dSCS
Cs1 is Element of the carrier' of IIG
the_result_sort_of Cs1 is Element of the carrier of IIG
len s1 is V21() V22() V23() V27() finite cardinal countable V133() V134() ext-real V148() V149() V150() V151() V152() V153() V154() V155() V163() V164() V165() Element of NAT
the_arity_of Cs1 is Relation-like NAT -defined the carrier of IIG -valued Function-like finite countable FinSequence-like FinSubsequence-like Element of the carrier of IIG *
len (the_arity_of Cs1) is V21() V22() V23() V27() finite cardinal countable V133() V134() ext-real V148() V149() V150() V151() V152() V153() V154() V155() V163() V164() V165() Element of NAT
dom s1 is finite countable V150() V151() V152() V153() V154() V155() V163() V164() V165() Element of bool NAT
dom (the_arity_of Cs1) is finite countable V150() V151() V152() V153() V154() V155() V163() V164() V165() Element of bool NAT
rng (the_arity_of Cs1) is finite countable set
dom InpFs is non empty set
dom iv is set
FreeSort SCS is Relation-like non-empty non empty-yielding the carrier of IIG -defined Function-like non empty total set
FreeOper SCS is Relation-like the carrier' of IIG -defined Function-like non empty total Function-yielding V42() ManySortedFunction of the Arity of IIG * ((FreeSort SCS) #), the ResultSort of IIG * (FreeSort SCS)
the Arity of IIG is Relation-like the carrier' of IIG -defined the carrier of IIG * -valued Function-like V18( the carrier' of IIG, the carrier of IIG * ) Function-yielding V42() 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 SCS) # is Relation-like the carrier of IIG * -defined Function-like non empty total set
the Arity of IIG * ((FreeSort SCS) #) is Relation-like the carrier' of IIG -defined Function-like non empty total set
the ResultSort of IIG * (FreeSort SCS) is Relation-like non-empty non empty-yielding the carrier' of IIG -defined Function-like non empty total set
MSAlgebra(# (FreeSort SCS),(FreeOper SCS) #) is strict MSAlgebra over IIG
FreeSort (SCS,dSCS) is functional non empty constituted-DTrees Element of bool (TS (DTConMSA SCS))
DTConMSA SCS is non empty strict with_terminals with_nonterminals with_useful_nonterminals L13()
TS (DTConMSA SCS) is functional constituted-DTrees Element of bool (FinTrees the carrier of (DTConMSA SCS))
the carrier of (DTConMSA SCS) is non empty set
FinTrees the carrier of (DTConMSA SCS) is functional non empty constituted-DTrees DTree-set of the carrier of (DTConMSA SCS)
bool (FinTrees the carrier of (DTConMSA SCS)) is set
bool (TS (DTConMSA SCS)) is set
[Cs1, the carrier of IIG] is set
[Cs1, the carrier of IIG] -tree s1 is Relation-like Function-like DecoratedTree-like set
SCS . dSCS is non empty set
{ b₁ where b₁ is Relation-like Function-like Element of TS (DTConMSA SCS) : ( ex b₂ being set st
( b₂ in SCS . dSCS & b₁ = root-tree [b₂,dSCS] ) or ex b₂ being Element of the carrier' of IIG st
( [b₂, the carrier of IIG] = b₁ . {} & the_result_sort_of b₂ = dSCS ) ) } is set
Cs2 is Relation-like Function-like set
dom Cs2 is set
(the_arity_of Cs1) * InpFs is Relation-like NAT -defined Function-like finite countable Function-yielding V42() set
x9 is V21() V22() V23() V27() finite cardinal countable V133() V134() ext-real set
Seg x9 is finite x9 -element countable V150() V151() V152() V153() V154() V155() V163() V164() V165() Element of bool NAT
x is Relation-like NAT -defined Function-like finite countable FinSequence-like FinSubsequence-like set
p is set
x . p is set
iv . p is Relation-like Function-like set
dom x is finite countable V150() V151() V152() V153() V154() V155() V163() V164() V165() Element of bool NAT
p is Relation-like Function-like set
p9 is V21() V22() V23() V27() finite cardinal countable V133() V134() ext-real V148() V149() V150() V151() V152() V153() V154() V155() V163() V164() V165() Element of NAT
s1 . p9 is set
p . (s1 . p9) is set
x9 is Relation-like NAT -defined Function-like finite countable FinSequence-like FinSubsequence-like set
len x9 is V21() V22() V23() V27() finite cardinal countable V133() V134() ext-real V148() V149() V150() V151() V152() V153() V154() V155() V163() V164() V165() Element of NAT
dom x9 is finite countable V150() V151() V152() V153() V154() V155() V163() V164() V165() Element of bool NAT
(the_arity_of Cs1) . p9 is set
Fp is Element of the carrier of IIG
InpFs . Fp is Relation-like the Sorts of (FreeMSA SCS) . Fp -defined the Sorts of (FreeMSA SCS) . Fp -valued Function-like V18( the Sorts of (FreeMSA SCS) . Fp, the Sorts of (FreeMSA SCS) . Fp) Element of bool [:( the Sorts of (FreeMSA SCS) . Fp),( the Sorts of (FreeMSA SCS) . Fp):]
the Sorts of (FreeMSA SCS) . Fp is non empty set
[:( the Sorts of (FreeMSA SCS) . Fp),( the Sorts of (FreeMSA SCS) . Fp):] is Relation-like set
bool [:( the Sorts of (FreeMSA SCS) . Fp),( the Sorts of (FreeMSA SCS) . Fp):] is set
(the_arity_of Cs1) * the Sorts of (FreeMSA SCS) is Relation-like non-empty NAT -defined Function-like finite countable set
dom the Arity of IIG is set
the Sorts of (FreeMSA SCS) # is Relation-like the carrier of IIG * -defined Function-like non empty total set
the Arity of IIG * ( the Sorts of (FreeMSA SCS) #) is Relation-like the carrier' of IIG -defined Function-like non empty total set
( the Arity of IIG * ( the Sorts of (FreeMSA SCS) #)) . Cs1 is set
the Arity of IIG . Cs1 is Relation-like NAT -defined Function-like finite countable FinSequence-like FinSubsequence-like Element of the carrier of IIG *
( the Sorts of (FreeMSA SCS) #) . ( the Arity of IIG . Cs1) is set
( the Sorts of (FreeMSA SCS) #) . (the_arity_of Cs1) is set
product ((the_arity_of Cs1) * the Sorts of (FreeMSA SCS)) is functional non empty with_common_domain product-like set
ods is Relation-like Function-like Element of TS (DTConMSA SCS)
ods . {} is set
p is set
[p,dSCS] is set
root-tree [p,dSCS] is Relation-like Function-like finite countable DecoratedTree-like set
p9 is Element of the carrier' of IIG
[p9, the carrier of IIG] is set
the_result_sort_of p9 is Element of the carrier of IIG
p is set
[p,dSCS] is set
root-tree [p,dSCS] is Relation-like Function-like finite countable DecoratedTree-like set
dom the Sorts of (FreeMSA SCS) is non empty set
dom ((the_arity_of Cs1) * the Sorts of (FreeMSA SCS)) is finite countable set
p9 is set
(the_arity_of Cs1) . p9 is set
Fp is V21() V22() V23() V27() finite cardinal countable V133() V134() ext-real V148() V149() V150() V151() V152() V153() V154() V155() V163() V164() V165() Element of NAT
((the_arity_of Cs1) * the Sorts of (FreeMSA SCS)) . p9 is set
x is Element of the carrier of IIG
the Sorts of (FreeMSA SCS) . x is non empty set
s1 . p9 is set
Args (Cs1,(FreeMSA SCS)) is functional non empty Element of rng ( the Sorts of (FreeMSA SCS) #)
rng ( the Sorts of (FreeMSA SCS) #) is non empty set
p9 is Relation-like Function-like Element of Args (Cs1,(FreeMSA SCS))
InpFs # p9 is Relation-like Function-like Element of Args (Cs1,(FreeMSA SCS))
x is set
v1 is V21() V22() V23() V27() finite cardinal countable V133() V134() ext-real V148() V149() V150() V151() V152() V153() V154() V155() V163() V164() V165() Element of NAT
(the_arity_of Cs1) . v1 is set
Fp is Relation-like Function-like set
Fp . v1 is set
(the_arity_of Cs1) /. v1 is Element of the carrier of IIG
InpFs . ((the_arity_of Cs1) /. v1) is Relation-like the Sorts of (FreeMSA SCS) . ((the_arity_of Cs1) /. v1) -defined the Sorts of (FreeMSA SCS) . ((the_arity_of Cs1) /. v1) -valued Function-like V18( the Sorts of (FreeMSA SCS) . ((the_arity_of Cs1) /. v1), the Sorts of (FreeMSA SCS) . ((the_arity_of Cs1) /. v1)) Element of bool [:( the Sorts of (FreeMSA SCS) . ((the_arity_of Cs1) /. v1)),( the Sorts of (FreeMSA SCS) . ((the_arity_of Cs1) /. v1)):]
the Sorts of (FreeMSA SCS) . ((the_arity_of Cs1) /. v1) is non empty set
[:( the Sorts of (FreeMSA SCS) . ((the_arity_of Cs1) /. v1)),( the Sorts of (FreeMSA SCS) . ((the_arity_of Cs1) /. v1)):] is Relation-like set
bool [:( the Sorts of (FreeMSA SCS) . ((the_arity_of Cs1) /. v1)),( the Sorts of (FreeMSA SCS) . ((the_arity_of Cs1) /. v1)):] is set
s1 . v1 is set
(InpFs . ((the_arity_of Cs1) /. v1)) . (s1 . v1) is set
x9 is Element of the carrier of IIG
InpFs . x9 is Relation-like the Sorts of (FreeMSA SCS) . x9 -defined the Sorts of (FreeMSA SCS) . x9 -valued Function-like V18( the Sorts of (FreeMSA SCS) . x9, the Sorts of (FreeMSA SCS) . x9) Element of bool [:( the Sorts of (FreeMSA SCS) . x9),( the Sorts of (FreeMSA SCS) . x9):]
the Sorts of (FreeMSA SCS) . x9 is non empty set
[:( the Sorts of (FreeMSA SCS) . x9),( the Sorts of (FreeMSA SCS) . x9):] is Relation-like set
bool [:( the Sorts of (FreeMSA SCS) . x9),( the Sorts of (FreeMSA SCS) . x9):] is set
(InpFs . x9) . (s1 . v1) is set
Fp . x is set
iv . x is Relation-like Function-like set
s1 . x is set
(iv . x) . (s1 . x) is set
dom Fp is set
p is Relation-like NAT -defined Function-like finite countable FinSequence-like FinSubsequence-like DTree-yielding set
x is Element of the carrier' of IIG
[x, the carrier of IIG] is 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
the_result_sort_of x is 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
K355((DTConMSA SCS)) is non empty Element of bool the carrier of (DTConMSA SCS)
bool the carrier of (DTConMSA SCS) is set
v1 is Element of K355((DTConMSA SCS))
x9 is Relation-like NAT -defined FinTrees the carrier of (DTConMSA SCS) -valued Function-like finite countable Function-yielding V42() FinSequence-like FinSubsequence-like FinSequence of TS (DTConMSA SCS)
v1 -tree x9 is Relation-like the carrier of (DTConMSA SCS) -valued Function-like finite countable DecoratedTree-like Element of FinTrees the carrier of (DTConMSA SCS)
roots x9 is Relation-like NAT -defined the carrier of (DTConMSA SCS) -valued Function-like finite countable FinSequence-like FinSubsequence-like FinSequence of the carrier of (DTConMSA SCS)
[(action_at dSCS), the carrier of IIG] -tree p is Relation-like Function-like DecoratedTree-like set
Sym (Cs1,SCS) is Element of K355((DTConMSA SCS))
E1 is set
iv . E1 is Relation-like Function-like set
p . E1 is set
E2 is Relation-like Function-like set
s1 . E1 is set
E2 . (s1 . E1) is set
(the_arity_of Cs1) . E1 is set
((the_arity_of Cs1) * the Sorts of (FreeMSA SCS)) . E1 is set
It1 is Element of the carrier of IIG
the Sorts of (FreeMSA SCS) . It1 is non empty set
InpFs . It1 is Relation-like the Sorts of (FreeMSA SCS) . It1 -defined the Sorts of (FreeMSA SCS) . It1 -valued Function-like V18( the Sorts of (FreeMSA SCS) . It1, the Sorts of (FreeMSA SCS) . It1) Element of bool [:( the Sorts of (FreeMSA SCS) . It1),( the Sorts of (FreeMSA SCS) . It1):]
[:( the Sorts of (FreeMSA SCS) . It1),( the Sorts of (FreeMSA SCS) . It1):] is Relation-like set
bool [:( the Sorts of (FreeMSA SCS) . It1),( the Sorts of (FreeMSA SCS) . It1):] is set
( the Arity of IIG * ((FreeSort SCS) #)) . Cs1 is set
E1 is Relation-like NAT -defined FinTrees the carrier of (DTConMSA SCS) -valued Function-like finite countable Function-yielding V42() FinSequence-like FinSubsequence-like FinSequence of TS (DTConMSA SCS)
roots E1 is Relation-like NAT -defined the carrier of (DTConMSA SCS) -valued Function-like finite countable FinSequence-like FinSubsequence-like FinSequence of the carrier of (DTConMSA SCS)
DenOp (Cs1,SCS) is Relation-like ( the Arity of IIG * ((FreeSort SCS) #)) . Cs1 -defined ( the ResultSort of IIG * (FreeSort SCS)) . Cs1 -valued Function-like V18(( the Arity of IIG * ((FreeSort SCS) #)) . Cs1,( the ResultSort of IIG * (FreeSort SCS)) . Cs1) Element of bool [:(( the Arity of IIG * ((FreeSort SCS) #)) . Cs1),(( the ResultSort of IIG * (FreeSort SCS)) . Cs1):]
( the ResultSort of IIG * (FreeSort SCS)) . Cs1 is non empty set
[:(( the Arity of IIG * ((FreeSort SCS) #)) . Cs1),(( the ResultSort of IIG * (FreeSort SCS)) . Cs1):] is Relation-like set
bool [:(( the Arity of IIG * ((FreeSort SCS) #)) . Cs1),(( the ResultSort of IIG * (FreeSort SCS)) . Cs1):] is set
E2 is Relation-like NAT -defined FinTrees the carrier of (DTConMSA SCS) -valued Function-like finite countable Function-yielding V42() FinSequence-like FinSubsequence-like FinSequence of TS (DTConMSA SCS)
(DenOp (Cs1,SCS)) . E2 is set
Den (Cs1,(FreeMSA SCS)) is Relation-like Args (Cs1,(FreeMSA SCS)) -defined Result (Cs1,(FreeMSA SCS)) -valued Function-like V18( Args (Cs1,(FreeMSA SCS)), Result (Cs1,(FreeMSA SCS))) Element of bool [:(Args (Cs1,(FreeMSA SCS))),(Result (Cs1,(FreeMSA SCS))):]
Result (Cs1,(FreeMSA SCS)) is non empty Element of rng the Sorts of (FreeMSA SCS)
rng the Sorts of (FreeMSA SCS) is non empty set
[:(Args (Cs1,(FreeMSA SCS))),(Result (Cs1,(FreeMSA SCS))):] is Relation-like set
bool [:(Args (Cs1,(FreeMSA SCS))),(Result (Cs1,(FreeMSA SCS))):] is set
(FreeOper SCS) . Cs1 is Relation-like ( the Arity of IIG * ((FreeSort SCS) #)) . Cs1 -defined ( the ResultSort of IIG * (FreeSort SCS)) . Cs1 -valued Function-like V18(( the Arity of IIG * ((FreeSort SCS) #)) . Cs1,( the ResultSort of IIG * (FreeSort SCS)) . Cs1) Element of bool [:(( the Arity of IIG * ((FreeSort SCS) #)) . Cs1),(( the ResultSort of IIG * (FreeSort SCS)) . Cs1):]
(DenOp (Cs1,SCS)) . p is set
IIG is non empty non void V56() Circuit-like monotonic ManySortedSign
the carrier of IIG is non empty set
SCS is non-empty finitely-generated finite-yielding MSAlgebra over IIG
the Sorts of SCS is Relation-like non-empty non empty-yielding the carrier of IIG -defined Function-like non empty total set
product the Sorts of SCS is functional non empty with_common_domain product-like 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 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
K539( the carrier of IIG, the ResultSort of IIG) is Element of bool the carrier of IIG
the carrier of IIG \ K539( the carrier of IIG, the ResultSort of IIG) is Element of bool the carrier of IIG
InpFs is Relation-like the carrier of IIG -defined Function-like the Sorts of SCS -compatible non empty total Element of product the Sorts of SCS
iv is Relation-like InputVertices IIG -defined Function-like total InputValues of SCS
InpFs +* iv is Relation-like Function-like set
dom iv is set
dom the Sorts of SCS is non empty set
dSCS is set
iv . dSCS is set
the Sorts of SCS . dSCS is set
IIG is non empty non void V56() Circuit-like monotonic 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 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
K539( the carrier of IIG, the ResultSort of IIG) is Element of bool the carrier of IIG
the carrier of IIG \ K539( the carrier of IIG, the ResultSort of IIG) is Element of bool the carrier of IIG
SCS is non-empty finitely-generated finite-yielding MSAlgebra over IIG
the Sorts of SCS is Relation-like non-empty non empty-yielding the carrier of IIG -defined Function-like non empty total set
FreeGen the Sorts of SCS is Relation-like the carrier of IIG -defined Function-like non empty total GeneratorSet of FreeMSA the Sorts of SCS
FreeMSA the Sorts of SCS is strict non-empty MSAlgebra over IIG
FreeEnv SCS is strict non-empty free MSAlgebra over IIG
the Sorts of (FreeEnv SCS) is Relation-like non-empty non empty-yielding the carrier of IIG -defined Function-like non empty total set
InpFs is Relation-like InputVertices IIG -defined Function-like total InputValues of SCS
SortsWithConstants IIG is Element of bool the carrier of IIG
InnerVertices IIG is non empty Element of bool the carrier of IIG
(InnerVertices IIG) \ (SortsWithConstants IIG) is Element of bool the carrier of IIG
iv is set
dSCS is Element of the carrier of IIG
(InputVertices IIG) \/ (InnerVertices IIG) is non empty Element of bool the carrier of IIG
((InnerVertices IIG) \ (SortsWithConstants IIG)) \/ (SortsWithConstants IIG) is Element of bool the carrier of IIG
FreeGen (dSCS, the Sorts of SCS) is non empty Element of bool ((FreeSort the Sorts of SCS) . dSCS)
FreeSort the Sorts of SCS is Relation-like non-empty non empty-yielding the carrier of IIG -defined Function-like non empty total set
(FreeSort the Sorts of SCS) . dSCS is non empty set
bool ((FreeSort the Sorts of SCS) . dSCS) is set
InpFs . dSCS is set
[(InpFs . dSCS),dSCS] is set
root-tree [(InpFs . dSCS),dSCS] is Relation-like Function-like finite countable DecoratedTree-like set
(FreeGen (dSCS, the Sorts of SCS)) --> (root-tree [(InpFs . dSCS),dSCS]) is Relation-like FreeGen (dSCS, the Sorts of SCS) -defined {(root-tree [(InpFs . dSCS),dSCS])} -valued Function-like constant non empty total V18( FreeGen (dSCS, the Sorts of SCS),{(root-tree [(InpFs . dSCS),dSCS])}) Function-yielding V42() Element of bool [:(FreeGen (dSCS, the Sorts of SCS)),{(root-tree [(InpFs . dSCS),dSCS])}:]
{(root-tree [(InpFs . dSCS),dSCS])} is functional non empty trivial finite V32() 1 -element with_common_domain countable set
[:(FreeGen (dSCS, the Sorts of SCS)),{(root-tree [(InpFs . dSCS),dSCS])}:] is Relation-like set
bool [:(FreeGen (dSCS, the Sorts of SCS)),{(root-tree [(InpFs . dSCS),dSCS])}:] is set
s1 is set
action_at dSCS is Element of the carrier' of IIG
[(action_at dSCS), the carrier of IIG] is set
root-tree [(action_at dSCS), the carrier of IIG] is Relation-like Function-like finite countable DecoratedTree-like set
(FreeGen (dSCS, the Sorts of SCS)) --> (root-tree [(action_at dSCS), the carrier of IIG]) is Relation-like FreeGen (dSCS, the Sorts of SCS) -defined {(root-tree [(action_at dSCS), the carrier of IIG])} -valued Function-like constant non empty total V18( FreeGen (dSCS, the Sorts of SCS),{(root-tree [(action_at dSCS), the carrier of IIG])}) Function-yielding V42() Element of bool [:(FreeGen (dSCS, the Sorts of SCS)),{(root-tree [(action_at dSCS), the carrier of IIG])}:]
{(root-tree [(action_at dSCS), the carrier of IIG])} is functional non empty trivial finite V32() 1 -element with_common_domain countable set
[:(FreeGen (dSCS, the Sorts of SCS)),{(root-tree [(action_at dSCS), the carrier of IIG])}:] is Relation-like set
bool [:(FreeGen (dSCS, the Sorts of SCS)),{(root-tree [(action_at dSCS), the carrier of IIG])}:] is set
id (FreeGen (dSCS, the Sorts of SCS)) is Relation-like FreeGen (dSCS, the Sorts of SCS) -defined FreeGen (dSCS, the Sorts of SCS) -valued Function-like one-to-one non empty total Element of bool [:(FreeGen (dSCS, the Sorts of SCS)),(FreeGen (dSCS, the Sorts of SCS)):]
[:(FreeGen (dSCS, the Sorts of SCS)),(FreeGen (dSCS, the Sorts of SCS)):] is Relation-like set
bool [:(FreeGen (dSCS, the Sorts of SCS)),(FreeGen (dSCS, the Sorts of SCS)):] is set
FreeGen (dSCS, the Sorts of SCS) is non empty Element of bool ((FreeSort the Sorts of SCS) . dSCS)
FreeSort the Sorts of SCS is Relation-like non-empty non empty-yielding the carrier of IIG -defined Function-like non empty total set
(FreeSort the Sorts of SCS) . dSCS is non empty set
bool ((FreeSort the Sorts of SCS) . dSCS) is set
action_at dSCS is Element of the carrier' of IIG
[(action_at dSCS), the carrier of IIG] is set
root-tree [(action_at dSCS), the carrier of IIG] is Relation-like Function-like finite countable DecoratedTree-like set
(FreeGen (dSCS, the Sorts of SCS)) --> (root-tree [(action_at dSCS), the carrier of IIG]) is Relation-like FreeGen (dSCS, the Sorts of SCS) -defined {(root-tree [(action_at dSCS), the carrier of IIG])} -valued Function-like constant non empty total V18( FreeGen (dSCS, the Sorts of SCS),{(root-tree [(action_at dSCS), the carrier of IIG])}) Function-yielding V42() Element of bool [:(FreeGen (dSCS, the Sorts of SCS)),{(root-tree [(action_at dSCS), the carrier of IIG])}:]
{(root-tree [(action_at dSCS), the carrier of IIG])} is functional non empty trivial finite V32() 1 -element with_common_domain countable set
[:(FreeGen (dSCS, the Sorts of SCS)),{(root-tree [(action_at dSCS), the carrier of IIG])}:] is Relation-like set
bool [:(FreeGen (dSCS, the Sorts of SCS)),{(root-tree [(action_at dSCS), the carrier of IIG])}:] is set
s1 is set
InpFs . dSCS is set
[(InpFs . dSCS),dSCS] is set
root-tree [(InpFs . dSCS),dSCS] is Relation-like Function-like finite countable DecoratedTree-like set
(FreeGen (dSCS, the Sorts of SCS)) --> (root-tree [(InpFs . dSCS),dSCS]) is Relation-like FreeGen (dSCS, the Sorts of SCS) -defined {(root-tree [(InpFs . dSCS),dSCS])} -valued Function-like constant non empty total V18( FreeGen (dSCS, the Sorts of SCS),{(root-tree [(InpFs . dSCS),dSCS])}) Function-yielding V42() Element of bool [:(FreeGen (dSCS, the Sorts of SCS)),{(root-tree [(InpFs . dSCS),dSCS])}:]
{(root-tree [(InpFs . dSCS),dSCS])} is functional non empty trivial finite V32() 1 -element with_common_domain countable set
[:(FreeGen (dSCS, the Sorts of SCS)),{(root-tree [(InpFs . dSCS),dSCS])}:] is Relation-like set
bool [:(FreeGen (dSCS, the Sorts of SCS)),{(root-tree [(InpFs . dSCS),dSCS])}:] is set
id (FreeGen (dSCS, the Sorts of SCS)) is Relation-like FreeGen (dSCS, the Sorts of SCS) -defined FreeGen (dSCS, the Sorts of SCS) -valued Function-like one-to-one non empty total Element of bool [:(FreeGen (dSCS, the Sorts of SCS)),(FreeGen (dSCS, the Sorts of SCS)):]
[:(FreeGen (dSCS, the Sorts of SCS)),(FreeGen (dSCS, the Sorts of SCS)):] is Relation-like set
bool [:(FreeGen (dSCS, the Sorts of SCS)),(FreeGen (dSCS, the Sorts of SCS)):] is set
FreeGen (dSCS, the Sorts of SCS) is non empty Element of bool ((FreeSort the Sorts of SCS) . dSCS)
FreeSort the Sorts of SCS is Relation-like non-empty non empty-yielding the carrier of IIG -defined Function-like non empty total set
(FreeSort the Sorts of SCS) . dSCS is non empty set
bool ((FreeSort the Sorts of SCS) . dSCS) is set
id (FreeGen (dSCS, the Sorts of SCS)) is Relation-like FreeGen (dSCS, the Sorts of SCS) -defined FreeGen (dSCS, the Sorts of SCS) -valued Function-like one-to-one non empty total Element of bool [:(FreeGen (dSCS, the Sorts of SCS)),(FreeGen (dSCS, the Sorts of SCS)):]
[:(FreeGen (dSCS, the Sorts of SCS)),(FreeGen (dSCS, the Sorts of SCS)):] is Relation-like set
bool [:(FreeGen (dSCS, the Sorts of SCS)),(FreeGen (dSCS, the Sorts of SCS)):] is set
s1 is set
InpFs . dSCS is set
[(InpFs . dSCS),dSCS] is set
root-tree [(InpFs . dSCS),dSCS] is Relation-like Function-like finite countable DecoratedTree-like set
(FreeGen (dSCS, the Sorts of SCS)) --> (root-tree [(InpFs . dSCS),dSCS]) is Relation-like FreeGen (dSCS, the Sorts of SCS) -defined {(root-tree [(InpFs . dSCS),dSCS])} -valued Function-like constant non empty total V18( FreeGen (dSCS, the Sorts of SCS),{(root-tree [(InpFs . dSCS),dSCS])}) Function-yielding V42() Element of bool [:(FreeGen (dSCS, the Sorts of SCS)),{(root-tree [(InpFs . dSCS),dSCS])}:]
{(root-tree [(InpFs . dSCS),dSCS])} is functional non empty trivial finite V32() 1 -element with_common_domain countable set
[:(FreeGen (dSCS, the Sorts of SCS)),{(root-tree [(InpFs . dSCS),dSCS])}:] is Relation-like set
bool [:(FreeGen (dSCS, the Sorts of SCS)),{(root-tree [(InpFs . dSCS),dSCS])}:] is set
action_at dSCS is Element of the carrier' of IIG
[(action_at dSCS), the carrier of IIG] is set
root-tree [(action_at dSCS), the carrier of IIG] is Relation-like Function-like finite countable DecoratedTree-like set
(FreeGen (dSCS, the Sorts of SCS)) --> (root-tree [(action_at dSCS), the carrier of IIG]) is Relation-like FreeGen (dSCS, the Sorts of SCS) -defined {(root-tree [(action_at dSCS), the carrier of IIG])} -valued Function-like constant non empty total V18( FreeGen (dSCS, the Sorts of SCS),{(root-tree [(action_at dSCS), the carrier of IIG])}) Function-yielding V42() Element of bool [:(FreeGen (dSCS, the Sorts of SCS)),{(root-tree [(action_at dSCS), the carrier of IIG])}:]
{(root-tree [(action_at dSCS), the carrier of IIG])} is functional non empty trivial finite V32() 1 -element with_common_domain countable set
[:(FreeGen (dSCS, the Sorts of SCS)),{(root-tree [(action_at dSCS), the carrier of IIG])}:] is Relation-like set
bool [:(FreeGen (dSCS, the Sorts of SCS)),{(root-tree [(action_at dSCS), the carrier of IIG])}:] is set
iv is Relation-like the carrier of IIG -defined Function-like non empty total set
dSCS is set
s1 is Element of the carrier of IIG
FreeGen (s1, the Sorts of SCS) is non empty Element of bool ((FreeSort the Sorts of SCS) . s1)
FreeSort the Sorts of SCS is Relation-like non-empty non empty-yielding the carrier of IIG -defined Function-like non empty total set
(FreeSort the Sorts of SCS) . s1 is non empty set
bool ((FreeSort the Sorts of SCS) . s1) is set
(FreeGen the Sorts of SCS) . s1 is set
FreeOper the Sorts of SCS is Relation-like the carrier' of IIG -defined Function-like non empty total Function-yielding V42() ManySortedFunction of the Arity of IIG * ((FreeSort the Sorts of SCS) #), the ResultSort of IIG * (FreeSort the Sorts of SCS)
the Arity of IIG is Relation-like the carrier' of IIG -defined the carrier of IIG * -valued Function-like V18( the carrier' of IIG, the carrier of IIG * ) Function-yielding V42() Element of bool [: the carrier' of IIG,( the carrier of IIG *):]
the carrier of IIG * is functional non empty FinSequence-membered M8( 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 SCS) # is Relation-like the carrier of IIG * -defined Function-like non empty total set
the Arity of IIG * ((FreeSort the Sorts of SCS) #) is Relation-like the carrier' of IIG -defined Function-like non empty total set
the ResultSort of IIG * (FreeSort the Sorts of SCS) is Relation-like non-empty non empty-yielding the carrier' of IIG -defined Function-like non empty total set
MSAlgebra(# (FreeSort the Sorts of SCS),(FreeOper the Sorts of SCS) #) is strict MSAlgebra over IIG
InpFs . s1 is set
the Sorts of SCS . s1 is non empty set
[(InpFs . s1),s1] is set
root-tree [(InpFs . s1),s1] is Relation-like Function-like finite countable DecoratedTree-like set
iv . s1 is set
iv . dSCS is set
(FreeGen the Sorts of SCS) . dSCS is set
the Sorts of (FreeEnv SCS) . dSCS is set
[:((FreeGen the Sorts of SCS) . dSCS),( the Sorts of (FreeEnv SCS) . dSCS):] is Relation-like set
bool [:((FreeGen the Sorts of SCS) . dSCS),( the Sorts of (FreeEnv SCS) . dSCS):] is set
s2 is Element of the carrier of IIG
FreeGen (s2, the Sorts of SCS) is non empty Element of bool ((FreeSort the Sorts of SCS) . s2)
(FreeSort the Sorts of SCS) . s2 is non empty set
bool ((FreeSort the Sorts of SCS) . s2) is set
InpFs . s2 is set
[(InpFs . s2),s2] is set
root-tree [(InpFs . s2),s2] is Relation-like Function-like finite countable DecoratedTree-like set
(FreeGen (s2, the Sorts of SCS)) --> (root-tree [(InpFs . s2),s2]) is Relation-like FreeGen (s2, the Sorts of SCS) -defined {(root-tree [(InpFs . s2),s2])} -valued Function-like constant non empty total V18( FreeGen (s2, the Sorts of SCS),{(root-tree [(InpFs . s2),s2])}) Function-yielding V42() Element of bool [:(FreeGen (s2, the Sorts of SCS)),{(root-tree [(InpFs . s2),s2])}:]
{(root-tree [(InpFs . s2),s2])} is functional non empty trivial finite V32() 1 -element with_common_domain countable set
[:(FreeGen (s2, the Sorts of SCS)),{(root-tree [(InpFs . s2),s2])}:] is Relation-like set
bool [:(FreeGen (s2, the Sorts of SCS)),{(root-tree [(InpFs . s2),s2])}:] is set
action_at s2 is Element of the carrier' of IIG
[(action_at s2), the carrier of IIG] is set
root-tree [(action_at s2), the carrier of IIG] is Relation-like Function-like finite countable DecoratedTree-like set
(FreeGen (s2, the Sorts of SCS)) --> (root-tree [(action_at s2), the carrier of IIG]) is Relation-like FreeGen (s2, the Sorts of SCS) -defined {(root-tree [(action_at s2), the carrier of IIG])} -valued Function-like constant non empty total V18( FreeGen (s2, the Sorts of SCS),{(root-tree [(action_at s2), the carrier of IIG])}) Function-yielding V42() Element of bool [:(FreeGen (s2, the Sorts of SCS)),{(root-tree [(action_at s2), the carrier of IIG])}:]
{(root-tree [(action_at s2), the carrier of IIG])} is functional non empty trivial finite V32() 1 -element with_common_domain countable set
[:(FreeGen (s2, the Sorts of SCS)),{(root-tree [(action_at s2), the carrier of IIG])}:] is Relation-like set
bool [:(FreeGen (s2, the Sorts of SCS)),{(root-tree [(action_at s2), the carrier of IIG])}:] is set
id (FreeGen (s2, the Sorts of SCS)) is Relation-like FreeGen (s2, the Sorts of SCS) -defined FreeGen (s2, the Sorts of SCS) -valued Function-like one-to-one non empty total Element of bool [:(FreeGen (s2, the Sorts of SCS)),(FreeGen (s2, the Sorts of SCS)):]
[:(FreeGen (s2, the Sorts of SCS)),(FreeGen (s2, the Sorts of SCS)):] is Relation-like set
bool [:(FreeGen (s2, the Sorts of SCS)),(FreeGen (s2, the Sorts of SCS)):] is set
DTConMSA the Sorts of SCS is non empty strict with_terminals with_nonterminals with_useful_nonterminals L13()
the carrier of (DTConMSA the Sorts of SCS) is non empty set
K355((DTConMSA the Sorts of SCS)) is non empty Element of bool the carrier of (DTConMSA the Sorts of SCS)
bool the carrier of (DTConMSA the Sorts of SCS) is set
action_at s1 is Element of the carrier' of IIG
Sym ((action_at s1), the Sorts of SCS) is Element of K355((DTConMSA the Sorts of SCS))
TS (DTConMSA the Sorts of SCS) is functional constituted-DTrees Element of bool (FinTrees the carrier of (DTConMSA the Sorts of SCS))
FinTrees the carrier of (DTConMSA the Sorts of SCS) is functional non empty constituted-DTrees DTree-set of the carrier of (DTConMSA the Sorts of SCS)
bool (FinTrees the carrier of (DTConMSA the Sorts of SCS)) is set
<*> (TS (DTConMSA the Sorts of SCS)) is Relation-like non-empty empty-yielding NAT -defined TS (DTConMSA the Sorts of SCS) -valued Function-like one-to-one constant functional empty V21() V22() V23() V25() V26() V27() finite finite-yielding V32() cardinal {} -element Cardinal-yielding countable Function-yielding V42() FinSequence-like FinSubsequence-like FinSequence-membered constituted-Trees constituted-FinTrees constituted-DTrees Tree-yielding FinTree-yielding DTree-yielding V133() V134() ext-real V150() V151() V152() V153() V154() V155() V156() V163() V164() V165() V166() FinSequence of TS (DTConMSA the Sorts of SCS)
[(action_at s1), the carrier of IIG] is set
root-tree [(action_at s1), the carrier of IIG] is Relation-like Function-like finite countable DecoratedTree-like set
{ b₁ where b₁ is Element of the carrier of IIG : b₁ is with_const_op } is set
x is Element of the carrier of IIG
x is Element of the carrier' of IIG
the Arity of IIG . x is Relation-like NAT -defined Function-like finite countable FinSequence-like FinSubsequence-like Element of the carrier of IIG *
the ResultSort of IIG . x is Element of the carrier of IIG
dom (<*> (TS (DTConMSA the Sorts of SCS))) is Relation-like non-empty empty-yielding NAT -defined Function-like one-to-one constant functional empty V21() V22() V23() V25() V26() V27() finite finite-yielding V32() cardinal {} -element Cardinal-yielding countable Function-yielding V42() FinSequence-like FinSubsequence-like FinSequence-membered constituted-Trees constituted-FinTrees constituted-DTrees Tree-yielding FinTree-yielding DTree-yielding V133() V134() ext-real V150() V151() V152() V153() V154() V155() V156() V163() V164() V165() V166() Element of bool NAT
the_arity_of x is Relation-like NAT -defined the carrier of IIG -valued Function-like finite countable FinSequence-like FinSubsequence-like Element of the carrier of IIG *
x9 is V21() V22() V23() V27() finite cardinal countable V133() V134() ext-real set
(<*> (TS (DTConMSA the Sorts of SCS))) . x9 is Relation-like non-empty empty-yielding NAT -defined Function-like one-to-one constant functional empty V21() V22() V23() V25() V26() V27() finite finite-yielding V32() cardinal {} -element Cardinal-yielding countable Function-yielding V42() FinSequence-like FinSubsequence-like FinSequence-membered constituted-Trees constituted-FinTrees constituted-DTrees Tree-yielding FinTree-yielding DTree-yielding V133() V134() ext-real V150() V151() V152() V153() V154() V155() V156() V163() V164() V165() V166() set
(the_arity_of x) /. x9 is Element of the carrier of IIG
FreeSort ( the Sorts of SCS,((the_arity_of x) /. x9)) is functional non empty constituted-DTrees Element of bool (TS (DTConMSA the Sorts of SCS))
bool (TS (DTConMSA the Sorts of SCS)) is set
( the Arity of IIG * ((FreeSort the Sorts of SCS) #)) . x is set
the_result_sort_of x is Element of the carrier of IIG
s2 is Element of K355((DTConMSA the Sorts of SCS))
roots (<*> (TS (DTConMSA the Sorts of SCS))) is Relation-like NAT -defined Function-like finite countable FinSequence-like FinSubsequence-like set
IIG -Terms the Sorts of SCS is functional constituted-DTrees Element of bool (FinTrees the carrier of (DTConMSA the Sorts of SCS))
<*> (IIG -Terms the Sorts of SCS) is Relation-like non-empty empty-yielding NAT -defined IIG -Terms the Sorts of SCS -valued Function-like one-to-one constant functional empty V21() V22() V23() V25() V26() V27() finite finite-yielding V32() cardinal {} -element Cardinal-yielding countable Function-yielding V42() FinSequence-like FinSubsequence-like FinSequence-membered constituted-Trees constituted-FinTrees constituted-DTrees Tree-yielding FinTree-yielding DTree-yielding V133() V134() ext-real V150() V151() V152() V153() V154() V155() V156() V163() V164() V165() V166() FinSequence of IIG -Terms the Sorts of SCS
[(action_at s1), the carrier of IIG] -tree {} is Relation-like Function-like DecoratedTree-like set
x9 is Relation-like Function-like Element of TS (DTConMSA the Sorts of SCS)
x9 . {} is set
the_result_sort_of (action_at s1) is Element of the carrier of IIG
the Sorts of SCS . s1 is non empty set
{ b₁ where b₁ is Relation-like Function-like Element of TS (DTConMSA the Sorts of SCS) : ( ex b₂ being set st
( b₂ in the Sorts of SCS . s1 & b₁ = root-tree [b₂,s1] ) or ex b₂ being Element of the carrier' of IIG st
( [b₂, the carrier of IIG] = b₁ . {} & the_result_sort_of b₂ = s1 ) ) } is set
FreeSort ( the Sorts of SCS,s1) is functional non empty constituted-DTrees Element of bool (TS (DTConMSA the Sorts of SCS))
bool (TS (DTConMSA the Sorts of SCS)) is set
the Sorts of (FreeEnv SCS) . s1 is non empty finite countable set
iv . s1 is set
iv . dSCS is set
(FreeGen the Sorts of SCS) . dSCS is set
the Sorts of (FreeEnv SCS) . dSCS is set
[:((FreeGen the Sorts of SCS) . dSCS),( the Sorts of (FreeEnv SCS) . dSCS):] is Relation-like set
bool [:((FreeGen the Sorts of SCS) . dSCS),( the Sorts of (FreeEnv SCS) . dSCS):] is set
p is Element of the carrier of IIG
FreeGen (p, the Sorts of SCS) is non empty Element of bool ((FreeSort the Sorts of SCS) . p)
(FreeSort the Sorts of SCS) . p is non empty set
bool ((FreeSort the Sorts of SCS) . p) is set
InpFs . p is set
[(InpFs . p),p] is set
root-tree [(InpFs . p),p] is Relation-like Function-like finite countable DecoratedTree-like set
(FreeGen (p, the Sorts of SCS)) --> (root-tree [(InpFs . p),p]) is Relation-like FreeGen (p, the Sorts of SCS) -defined {(root-tree [(InpFs . p),p])} -valued Function-like constant non empty total V18( FreeGen (p, the Sorts of SCS),{(root-tree [(InpFs . p),p])}) Function-yielding V42() Element of bool [:(FreeGen (p, the Sorts of SCS)),{(root-tree [(InpFs . p),p])}:]
{(root-tree [(InpFs . p),p])} is functional non empty trivial finite V32() 1 -element with_common_domain countable set
[:(FreeGen (p, the Sorts of SCS)),{(root-tree [(InpFs . p),p])}:] is Relation-like set
bool [:(FreeGen (p, the Sorts of SCS)),{(root-tree [(InpFs . p),p])}:] is set
action_at p is Element of the carrier' of IIG
[(action_at p), the carrier of IIG] is set
root-tree [(action_at p), the carrier of IIG] is Relation-like Function-like finite countable DecoratedTree-like set
(FreeGen (p, the Sorts of SCS)) --> (root-tree [(action_at p), the carrier of IIG]) is Relation-like FreeGen (p, the Sorts of SCS) -defined {(root-tree [(action_at p), the carrier of IIG])} -valued Function-like constant non empty total V18( FreeGen (p, the Sorts of SCS),{(root-tree [(action_at p), the carrier of IIG])}) Function-yielding V42() Element of bool [:(FreeGen (p, the Sorts of SCS)),{(root-tree [(action_at p), the carrier of IIG])}:]
{(root-tree [(action_at p), the carrier of IIG])} is functional non empty trivial finite V32() 1 -element with_common_domain countable set
[:(FreeGen (p, the Sorts of SCS)),{(root-tree [(action_at p), the carrier of IIG])}:] is Relation-like set
bool [:(FreeGen (p, the Sorts of SCS)),{(root-tree [(action_at p), the carrier of IIG])}:] is set
id (FreeGen (p, the Sorts of SCS)) is Relation-like FreeGen (p, the Sorts of SCS) -defined FreeGen (p, the Sorts of SCS) -valued Function-like one-to-one non empty total Element of bool [:(FreeGen (p, the Sorts of SCS)),(FreeGen (p, the Sorts of SCS)):]
[:(FreeGen (p, the Sorts of SCS)),(FreeGen (p, the Sorts of SCS)):] is Relation-like set
bool [:(FreeGen (p, the Sorts of SCS)),(FreeGen (p, the Sorts of SCS)):] is set
id (FreeGen (s1, the Sorts of SCS)) is Relation-like FreeGen (s1, the Sorts of SCS) -defined FreeGen (s1, the Sorts of SCS) -valued Function-like one-to-one non empty total Element of bool [:(FreeGen (s1, the Sorts of SCS)),(FreeGen (s1, the Sorts of SCS)):]
[:(FreeGen (s1, the Sorts of SCS)),(FreeGen (s1, the Sorts of SCS)):] is Relation-like set
bool [:(FreeGen (s1, the Sorts of SCS)),(FreeGen (s1, the Sorts of SCS)):] is set
dom (id (FreeGen (s1, the Sorts of SCS))) is non empty set
rng (id (FreeGen (s1, the Sorts of SCS))) is non empty set
iv . s1 is set
iv . dSCS is set
(FreeGen the Sorts of SCS) . dSCS is set
the Sorts of (FreeEnv SCS) . dSCS is set
[:((FreeGen the Sorts of SCS) . dSCS),( the Sorts of (FreeEnv SCS) . dSCS):] is Relation-like set
bool [:((FreeGen the Sorts of SCS) . dSCS),( the Sorts of (FreeEnv SCS) . dSCS):] is set
s2 is Element of the carrier of IIG
FreeGen (s2, the Sorts of SCS) is non empty Element of bool ((FreeSort the Sorts of SCS) . s2)
(FreeSort the Sorts of SCS) . s2 is non empty set
bool ((FreeSort the Sorts of SCS) . s2) is set
InpFs . s2 is set
[(InpFs . s2),s2] is set
root-tree [(InpFs . s2),s2] is Relation-like Function-like finite countable DecoratedTree-like set
(FreeGen (s2, the Sorts of SCS)) --> (root-tree [(InpFs . s2),s2]) is Relation-like FreeGen (s2, the Sorts of SCS) -defined {(root-tree [(InpFs . s2),s2])} -valued Function-like constant non empty total V18( FreeGen (s2, the Sorts of SCS),{(root-tree [(InpFs . s2),s2])}) Function-yielding V42() Element of bool [:(FreeGen (s2, the Sorts of SCS)),{(root-tree [(InpFs . s2),s2])}:]
{(root-tree [(InpFs . s2),s2])} is functional non empty trivial finite V32() 1 -element with_common_domain countable set
[:(FreeGen (s2, the Sorts of SCS)),{(root-tree [(InpFs . s2),s2])}:] is Relation-like set
bool [:(FreeGen (s2, the Sorts of SCS)),{(root-tree [(InpFs . s2),s2])}:] is set
action_at s2 is Element of the carrier' of IIG
[(action_at s2), the carrier of IIG] is set
root-tree [(action_at s2), the carrier of IIG] is Relation-like Function-like finite countable DecoratedTree-like set
(FreeGen (s2, the Sorts of SCS)) --> (root-tree [(action_at s2), the carrier of IIG]) is Relation-like FreeGen (s2, the Sorts of SCS) -defined {(root-tree [(action_at s2), the carrier of IIG])} -valued Function-like constant non empty total V18( FreeGen (s2, the Sorts of SCS),{(root-tree [(action_at s2), the carrier of IIG])}) Function-yielding V42() Element of bool [:(FreeGen (s2, the Sorts of SCS)),{(root-tree [(action_at s2), the carrier of IIG])}:]
{(root-tree [(action_at s2), the carrier of IIG])} is functional non empty trivial finite V32() 1 -element with_common_domain countable set
[:(FreeGen (s2, the Sorts of SCS)),{(root-tree [(action_at s2), the carrier of IIG])}:] is Relation-like set
bool [:(FreeGen (s2, the Sorts of SCS)),{(root-tree [(action_at s2), the carrier of IIG])}:] is set
id (FreeGen (s2, the Sorts of SCS)) is Relation-like FreeGen (s2, the Sorts of SCS) -defined FreeGen (s2, the Sorts of SCS) -valued Function-like one-to-one non empty total Element of bool [:(FreeGen (s2, the Sorts of SCS)),(FreeGen (s2, the Sorts of SCS)):]
[:(FreeGen (s2, the Sorts of SCS)),(FreeGen (s2, the Sorts of SCS)):] is Relation-like set
bool [:(FreeGen (s2, the Sorts of SCS)),(FreeGen (s2, the Sorts of SCS)):] is set
dSCS is set
dom iv is non empty set
iv . dSCS is set
dSCS is Relation-like the carrier of IIG -defined Function-like non empty total Function-yielding V42() set
s1 is Relation-like the carrier of IIG -defined Function-like non empty total Function-yielding V42() ManySortedFunction of FreeGen the Sorts of SCS, the Sorts of (FreeEnv SCS)
s2 is Element of the carrier of IIG
(FreeGen the Sorts of SCS) . s2 is set
the Sorts of (FreeEnv SCS) . s2 is non empty finite countable set
FreeGen (s2, the Sorts of SCS) is non empty Element of bool ((FreeSort the Sorts of SCS) . s2)
(FreeSort the Sorts of SCS) . s2 is non empty set
bool ((FreeSort the Sorts of SCS) . s2) is set
InpFs . s2 is set
[(InpFs . s2),s2] is set
root-tree [(InpFs . s2),s2] is Relation-like Function-like finite countable DecoratedTree-like set
{(root-tree [(InpFs . s2),s2])} is functional non empty trivial finite V32() 1 -element with_common_domain countable set
s1 . s2 is Relation-like (FreeGen the Sorts of SCS) . s2 -defined the Sorts of (FreeEnv SCS) . s2 -valued Function-like V18((FreeGen the Sorts of SCS) . s2, the Sorts of (FreeEnv SCS) . s2) Element of bool [:((FreeGen the Sorts of SCS) . s2),( the Sorts of (FreeEnv SCS) . s2):]
[:((FreeGen the Sorts of SCS) . s2),( the Sorts of (FreeEnv SCS) . s2):] is Relation-like set
bool [:((FreeGen the Sorts of SCS) . s2),( the Sorts of (FreeEnv SCS) . s2):] is set
(FreeGen (s2, the Sorts of SCS)) --> (root-tree [(InpFs . s2),s2]) is Relation-like FreeGen (s2, the Sorts of SCS) -defined {(root-tree [(InpFs . s2),s2])} -valued Function-like constant non empty total V18( FreeGen (s2, the Sorts of SCS),{(root-tree [(InpFs . s2),s2])}) Function-yielding V42() Element of bool [:(FreeGen (s2, the Sorts of SCS)),{(root-tree [(InpFs . s2),s2])}:]
[:(FreeGen (s2, the Sorts of SCS)),{(root-tree [(InpFs . s2),s2])}:] is Relation-like set
bool [:(FreeGen (s2, the Sorts of SCS)),{(root-tree [(InpFs . s2),s2])}:] is set
action_at s2 is Element of the carrier' of IIG
[(action_at s2), the carrier of IIG] is set
root-tree [(action_at s2), the carrier of IIG] is Relation-like Function-like finite countable DecoratedTree-like set
{(root-tree [(action_at s2), the carrier of IIG])} is functional non empty trivial finite V32() 1 -element with_common_domain countable set
(FreeGen (s2, the Sorts of SCS)) --> (root-tree [(action_at s2), the carrier of IIG]) is Relation-like FreeGen (s2, the Sorts of SCS) -defined {(root-tree [(action_at s2), the carrier of IIG])} -valued Function-like constant non empty total V18( FreeGen (s2, the Sorts of SCS),{(root-tree [(action_at s2), the carrier of IIG])}) Function-yielding V42() Element of bool [:(FreeGen (s2, the Sorts of SCS)),{(root-tree [(action_at s2), the carrier of IIG])}:]
[:(FreeGen (s2, the Sorts of SCS)),{(root-tree [(action_at s2), the carrier of IIG])}:] is Relation-like set
bool [:(FreeGen (s2, the Sorts of SCS)),{(root-tree [(action_at s2), the carrier of IIG])}:] is set
id (FreeGen (s2, the Sorts of SCS)) is Relation-like FreeGen (s2, the Sorts of SCS) -defined FreeGen (s2, the Sorts of SCS) -valued Function-like one-to-one non empty total Element of bool [:(FreeGen (s2, the Sorts of SCS)),(FreeGen (s2, the Sorts of SCS)):]
[:(FreeGen (s2, the Sorts of SCS)),(FreeGen (s2, the Sorts of SCS)):] is Relation-like set
bool [:(FreeGen (s2, the Sorts of SCS)),(FreeGen (s2, the Sorts of SCS)):] is set
Cs1 is Element of the carrier of IIG
FreeGen (Cs1, the Sorts of SCS) is non empty Element of bool ((FreeSort the Sorts of SCS) . Cs1)
(FreeSort the Sorts of SCS) . Cs1 is non empty set
bool ((FreeSort the Sorts of SCS) . Cs1) is set
InpFs . Cs1 is set
[(InpFs . Cs1),Cs1] is set
root-tree [(InpFs . Cs1),Cs1] is Relation-like Function-like finite countable DecoratedTree-like set
(FreeGen (Cs1, the Sorts of SCS)) --> (root-tree [(InpFs . Cs1),Cs1]) is Relation-like FreeGen (Cs1, the Sorts of SCS) -defined {(root-tree [(InpFs . Cs1),Cs1])} -valued Function-like constant non empty total V18( FreeGen (Cs1, the Sorts of SCS),{(root-tree [(InpFs . Cs1),Cs1])}) Function-yielding V42() Element of bool [:(FreeGen (Cs1, the Sorts of SCS)),{(root-tree [(InpFs . Cs1),Cs1])}:]
{(root-tree [(InpFs . Cs1),Cs1])} is functional non empty trivial finite V32() 1 -element with_common_domain countable set
[:(FreeGen (Cs1, the Sorts of SCS)),{(root-tree [(InpFs . Cs1),Cs1])}:] is Relation-like set
bool [:(FreeGen (Cs1, the Sorts of SCS)),{(root-tree [(InpFs . Cs1),Cs1])}:] is set
action_at Cs1 is Element of the carrier' of IIG
[(action_at Cs1), the carrier of IIG] is set
root-tree [(action_at Cs1), the carrier of IIG] is Relation-like Function-like finite countable DecoratedTree-like set
(FreeGen (Cs1, the Sorts of SCS)) --> (root-tree [(action_at Cs1), the carrier of IIG]) is Relation-like FreeGen (Cs1, the Sorts of SCS) -defined {(root-tree [(action_at Cs1), the carrier of IIG])} -valued Function-like constant non empty total V18( FreeGen (Cs1, the Sorts of SCS),{(root-tree [(action_at Cs1), the carrier of IIG])}) Function-yielding V42() Element of bool [:(FreeGen (Cs1, the Sorts of SCS)),{(root-tree [(action_at Cs1), the carrier of IIG])}:]
{(root-tree [(action_at Cs1), the carrier of IIG])} is functional non empty trivial finite V32() 1 -element with_common_domain countable set
[:(FreeGen (Cs1, the Sorts of SCS)),{(root-tree [(action_at Cs1), the carrier of IIG])}:] is Relation-like set
bool [:(FreeGen (Cs1, the Sorts of SCS)),{(root-tree [(action_at Cs1), the carrier of IIG])}:] is set
id (FreeGen (Cs1, the Sorts of SCS)) is Relation-like FreeGen (Cs1, the Sorts of SCS) -defined FreeGen (Cs1, the Sorts of SCS) -valued Function-like one-to-one non empty total Element of bool [:(FreeGen (Cs1, the Sorts of SCS)),(FreeGen (Cs1, the Sorts of SCS)):]
[:(FreeGen (Cs1, the Sorts of SCS)),(FreeGen (Cs1, the Sorts of SCS)):] is Relation-like set
bool [:(FreeGen (Cs1, the Sorts of SCS)),(FreeGen (Cs1, the Sorts of SCS)):] is set
Cs1 is Element of the carrier of IIG
FreeGen (Cs1, the Sorts of SCS) is non empty Element of bool ((FreeSort the Sorts of SCS) . Cs1)
(FreeSort the Sorts of SCS) . Cs1 is non empty set
bool ((FreeSort the Sorts of SCS) . Cs1) is set
InpFs . Cs1 is set
[(InpFs . Cs1),Cs1] is set
root-tree [(InpFs . Cs1),Cs1] is Relation-like Function-like finite countable DecoratedTree-like set
(FreeGen (Cs1, the Sorts of SCS)) --> (root-tree [(InpFs . Cs1),Cs1]) is Relation-like FreeGen (Cs1, the Sorts of SCS) -defined {(root-tree [(InpFs . Cs1),Cs1])} -valued Function-like constant non empty total V18( FreeGen (Cs1, the Sorts of SCS),{(root-tree [(InpFs . Cs1),Cs1])}) Function-yielding V42() Element of bool [:(FreeGen (Cs1, the Sorts of SCS)),{(root-tree [(InpFs . Cs1),Cs1])}:]
{(root-tree [(InpFs . Cs1),Cs1])} is functional non empty trivial finite V32() 1 -element with_common_domain countable set
[:(FreeGen (Cs1, the Sorts of SCS)),{(root-tree [(InpFs . Cs1),Cs1])}:] is Relation-like set
bool [:(FreeGen (Cs1, the Sorts of SCS)),{(root-tree [(InpFs . Cs1),Cs1])}:] is set
action_at Cs1 is Element of the carrier' of IIG
[(action_at Cs1), the carrier of IIG] is set
root-tree [(action_at Cs1), the carrier of IIG] is Relation-like Function-like finite countable DecoratedTree-like set
(FreeGen (Cs1, the Sorts of SCS)) --> (root-tree [(action_at Cs1), the carrier of IIG]) is Relation-like FreeGen (Cs1, the Sorts of SCS) -defined {(root-tree [(action_at Cs1), the carrier of IIG])} -valued Function-like constant non empty total V18( FreeGen (Cs1, the Sorts of SCS),{(root-tree [(action_at Cs1), the carrier of IIG])}) Function-yielding V42() Element of bool [:(FreeGen (Cs1, the Sorts of SCS)),{(root-tree [(action_at Cs1), the carrier of IIG])}:]
{(root-tree [(action_at Cs1), the carrier of IIG])} is functional non empty trivial finite V32() 1 -element with_common_domain countable set
[:(FreeGen (Cs1, the Sorts of SCS)),{(root-tree [(action_at Cs1), the carrier of IIG])}:] is Relation-like set
bool [:(FreeGen (Cs1, the Sorts of SCS)),{(root-tree [(action_at Cs1), the carrier of IIG])}:] is set
id (FreeGen (Cs1, the Sorts of SCS)) is Relation-like FreeGen (Cs1, the Sorts of SCS) -defined FreeGen (Cs1, the Sorts of SCS) -valued Function-like one-to-one non empty total Element of bool [:(FreeGen (Cs1, the Sorts of SCS)),(FreeGen (Cs1, the Sorts of SCS)):]
[:(FreeGen (Cs1, the Sorts of SCS)),(FreeGen (Cs1, the Sorts of SCS)):] is Relation-like set
bool [:(FreeGen (Cs1, the Sorts of SCS)),(FreeGen (Cs1, the Sorts of SCS)):] is set
Cs1 is Element of the carrier of IIG
FreeGen (Cs1, the Sorts of SCS) is non empty Element of bool ((FreeSort the Sorts of SCS) . Cs1)
(FreeSort the Sorts of SCS) . Cs1 is non empty set
bool ((FreeSort the Sorts of SCS) . Cs1) is set
InpFs . Cs1 is set
[(InpFs . Cs1),Cs1] is set
root-tree [(InpFs . Cs1),Cs1] is Relation-like Function-like finite countable DecoratedTree-like set
(FreeGen (Cs1, the Sorts of SCS)) --> (root-tree [(InpFs . Cs1),Cs1]) is Relation-like FreeGen (Cs1, the Sorts of SCS) -defined {(root-tree [(InpFs . Cs1),Cs1])} -valued Function-like constant non empty total V18( FreeGen (Cs1, the Sorts of SCS),{(root-tree [(InpFs . Cs1),Cs1])}) Function-yielding V42() Element of bool [:(FreeGen (Cs1, the Sorts of SCS)),{(root-tree [(InpFs . Cs1),Cs1])}:]
{(root-tree [(InpFs . Cs1),Cs1])} is functional non empty trivial finite V32() 1 -element with_common_domain countable set
[:(FreeGen (Cs1, the Sorts of SCS)),{(root-tree [(InpFs . Cs1),Cs1])}:] is Relation-like set
bool [:(FreeGen (Cs1, the Sorts of SCS)),{(root-tree [(InpFs . Cs1),Cs1])}:] is set
action_at Cs1 is Element of the carrier' of IIG
[(action_at Cs1), the carrier of IIG] is set
root-tree [(action_at Cs1), the carrier of IIG] is Relation-like Function-like finite countable DecoratedTree-like set
(FreeGen (Cs1, the Sorts of SCS)) --> (root-tree [(action_at Cs1), the carrier of IIG]) is Relation-like FreeGen (Cs1, the Sorts of SCS) -defined {(root-tree [(action_at Cs1), the carrier of IIG])} -valued Function-like constant non empty total V18( FreeGen (Cs1, the Sorts of SCS),{(root-tree [(action_at Cs1), the carrier of IIG])}) Function-yielding V42() Element of bool [:(FreeGen (Cs1, the Sorts of SCS)),{(root-tree [(action_at Cs1), the carrier of IIG])}:]
{(root-tree [(action_at Cs1), the carrier of IIG])} is functional non empty trivial finite V32() 1 -element with_common_domain countable set
[:(FreeGen (Cs1, the Sorts of SCS)),{(root-tree [(action_at Cs1), the carrier of IIG])}:] is Relation-like set
bool [:(FreeGen (Cs1, the Sorts of SCS)),{(root-tree [(action_at Cs1), the carrier of IIG])}:] is set
id (FreeGen (Cs1, the Sorts of SCS)) is Relation-like FreeGen (Cs1, the Sorts of SCS) -defined FreeGen (Cs1, the Sorts of SCS) -valued Function-like one-to-one non empty total Element of bool [:(FreeGen (Cs1, the Sorts of SCS)),(FreeGen (Cs1, the Sorts of SCS)):]
[:(FreeGen (Cs1, the Sorts of SCS)),(FreeGen (Cs1, the Sorts of SCS)):] is Relation-like set
bool [:(FreeGen (Cs1, the Sorts of SCS)),(FreeGen (Cs1, the Sorts of SCS)):] is set
iv is Relation-like the carrier of IIG -defined Function-like non empty total Function-yielding V42() ManySortedFunction of FreeGen the Sorts of SCS, the Sorts of (FreeEnv SCS)
dSCS is Relation-like the carrier of IIG -defined Function-like non empty total Function-yielding V42() ManySortedFunction of FreeGen the Sorts of SCS, the Sorts of (FreeEnv SCS)
((InnerVertices IIG) \ (SortsWithConstants IIG)) \/ (SortsWithConstants IIG) is Element of bool the carrier of IIG
s1 is set
s2 is Element of the carrier of IIG
(InputVertices IIG) \/ (InnerVertices IIG) is non empty Element of bool the carrier of IIG
(FreeGen the Sorts of SCS) . s2 is set
the Sorts of (FreeEnv SCS) . s2 is non empty finite countable set
FreeGen (s2, the Sorts of SCS) is non empty Element of bool ((FreeSort the Sorts of SCS) . s2)
FreeSort the Sorts of SCS is Relation-like non-empty non empty-yielding the carrier of IIG -defined Function-like non empty total set
(FreeSort the Sorts of SCS) . s2 is non empty set
bool ((FreeSort the Sorts of SCS) . s2) is set
InpFs . s2 is set
[(InpFs . s2),s2] is set
root-tree [(InpFs . s2),s2] is Relation-like Function-like finite countable DecoratedTree-like set
{(root-tree [(InpFs . s2),s2])} is functional non empty trivial finite V32() 1 -element with_common_domain countable set
iv . s2 is Relation-like (FreeGen the Sorts of SCS) . s2 -defined the Sorts of (FreeEnv SCS) . s2 -valued Function-like V18((FreeGen the Sorts of SCS) . s2, the Sorts of (FreeEnv SCS) . s2) Element of bool [:((FreeGen the Sorts of SCS) . s2),( the Sorts of (FreeEnv SCS) . s2):]
[:((FreeGen the Sorts of SCS) . s2),( the Sorts of (FreeEnv SCS) . s2):] is Relation-like set
bool [:((FreeGen the Sorts of SCS) . s2),( the Sorts of (FreeEnv SCS) . s2):] is set
(FreeGen (s2, the Sorts of SCS)) --> (root-tree [(InpFs . s2),s2]) is Relation-like FreeGen (s2, the Sorts of SCS) -defined {(root-tree [(InpFs . s2),s2])} -valued Function-like constant non empty total V18( FreeGen (s2, the Sorts of SCS),{(root-tree [(InpFs . s2),s2])}) Function-yielding V42() Element of bool [:(FreeGen (s2, the Sorts of SCS)),{(root-tree [(InpFs . s2),s2])}:]
[:(FreeGen (s2, the Sorts of SCS)),{(root-tree [(InpFs . s2),s2])}:] is Relation-like set
bool [:(FreeGen (s2, the Sorts of SCS)),{(root-tree [(InpFs . s2),s2])}:] is set
iv . s1 is Relation-like Function-like set
dSCS . s1 is Relation-like Function-like set
(FreeGen the Sorts of SCS) . s2 is set
the Sorts of (FreeEnv SCS) . s2 is non empty finite countable set
FreeGen (s2, the Sorts of SCS) is non empty Element of bool ((FreeSort the Sorts of SCS) . s2)
FreeSort the Sorts of SCS is Relation-like non-empty non empty-yielding the carrier of IIG -defined Function-like non empty total set
(FreeSort the Sorts of SCS) . s2 is non empty set
bool ((FreeSort the Sorts of SCS) . s2) is set
action_at s2 is Element of the carrier' of IIG
[(action_at s2), the carrier of IIG] is set
root-tree [(action_at s2), the carrier of IIG] is Relation-like Function-like finite countable DecoratedTree-like set
{(root-tree [(action_at s2), the carrier of IIG])} is functional non empty trivial finite V32() 1 -element with_common_domain countable set
iv . s2 is Relation-like (FreeGen the Sorts of SCS) . s2 -defined the Sorts of (FreeEnv SCS) . s2 -valued Function-like V18((FreeGen the Sorts of SCS) . s2, the Sorts of (FreeEnv SCS) . s2) Element of bool [:((FreeGen the Sorts of SCS) . s2),( the Sorts of (FreeEnv SCS) . s2):]
[:((FreeGen the Sorts of SCS) . s2),( the Sorts of (FreeEnv SCS) . s2):] is Relation-like set
bool [:((FreeGen the Sorts of SCS) . s2),( the Sorts of (FreeEnv SCS) . s2):] is set
(FreeGen (s2, the Sorts of SCS)) --> (root-tree [(action_at s2), the carrier of IIG]) is Relation-like FreeGen (s2, the Sorts of SCS) -defined {(root-tree [(action_at s2), the carrier of IIG])} -valued Function-like constant non empty total V18( FreeGen (s2, the Sorts of SCS),{(root-tree [(action_at s2), the carrier of IIG])}) Function-yielding V42() Element of bool [:(FreeGen (s2, the Sorts of SCS)),{(root-tree [(action_at s2), the carrier of IIG])}:]
[:(FreeGen (s2, the Sorts of SCS)),{(root-tree [(action_at s2), the carrier of IIG])}:] is Relation-like set
bool [:(FreeGen (s2, the Sorts of SCS)),{(root-tree [(action_at s2), the carrier of IIG])}:] is set
iv . s1 is Relation-like Function-like set
dSCS . s1 is Relation-like Function-like set
iv . s2 is Relation-like (FreeGen the Sorts of SCS) . s2 -defined the Sorts of (FreeEnv SCS) . s2 -valued Function-like V18((FreeGen the Sorts of SCS) . s2, the Sorts of (FreeEnv SCS) . s2) Element of bool [:((FreeGen the Sorts of SCS) . s2),( the Sorts of (FreeEnv SCS) . s2):]
(FreeGen the Sorts of SCS) . s2 is set
the Sorts of (FreeEnv SCS) . s2 is non empty finite countable set
[:((FreeGen the Sorts of SCS) . s2),( the Sorts of (FreeEnv SCS) . s2):] is Relation-like set
bool [:((FreeGen the Sorts of SCS) . s2),( the Sorts of (FreeEnv SCS) . s2):] is set
FreeGen (s2, the Sorts of SCS) is non empty Element of bool ((FreeSort the Sorts of SCS) . s2)
FreeSort the Sorts of SCS is Relation-like non-empty non empty-yielding the carrier of IIG -defined Function-like non empty total set
(FreeSort the Sorts of SCS) . s2 is non empty set
bool ((FreeSort the Sorts of SCS) . s2) is set
id (FreeGen (s2, the Sorts of SCS)) is Relation-like FreeGen (s2, the Sorts of SCS) -defined FreeGen (s2, the Sorts of SCS) -valued Function-like one-to-one non empty total Element of bool [:(FreeGen (s2, the Sorts of SCS)),(FreeGen (s2, the Sorts of SCS)):]
[:(FreeGen (s2, the Sorts of SCS)),(FreeGen (s2, the Sorts of SCS)):] is Relation-like set
bool [:(FreeGen (s2, the Sorts of SCS)),(FreeGen (s2, the Sorts of SCS)):] is set
iv . s1 is Relation-like Function-like set
dSCS . s1 is Relation-like Function-like set
IIG is non empty non void V56() Circuit-like monotonic 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 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
K539( the carrier of IIG, the ResultSort of IIG) is Element of bool the carrier of IIG
the carrier of IIG \ K539( the carrier of IIG, the ResultSort of IIG) is Element of bool the carrier of IIG
SCS is non-empty finitely-generated finite-yielding MSAlgebra over IIG
FreeEnv SCS is strict non-empty free MSAlgebra over IIG
the Sorts of SCS is Relation-like non-empty non empty-yielding the carrier of IIG -defined Function-like non empty total set
FreeMSA the Sorts of SCS is strict non-empty MSAlgebra over IIG
the Sorts of (FreeEnv SCS) is Relation-like non-empty non empty-yielding the carrier of IIG -defined Function-like non empty total set
InpFs is Relation-like InputVertices IIG -defined Function-like total InputValues of SCS
(IIG,SCS,InpFs) is Relation-like the carrier of IIG -defined Function-like non empty total Function-yielding V42() ManySortedFunction of FreeGen the Sorts of SCS, the Sorts of (FreeEnv SCS)
FreeGen the Sorts of SCS is Relation-like the carrier of IIG -defined Function-like non empty total GeneratorSet of FreeMSA the Sorts of SCS
iv is Relation-like the carrier of IIG -defined Function-like non empty total free GeneratorSet of FreeEnv SCS
dSCS is Relation-like the carrier of IIG -defined Function-like non empty total Function-yielding V42() ManySortedFunction of the Sorts of (FreeEnv SCS), the Sorts of (FreeEnv SCS)
dSCS || iv is Relation-like the carrier of IIG -defined Function-like non empty total Function-yielding V42() ManySortedFunction of iv, the Sorts of (FreeEnv SCS)
s1 is set
(IIG,SCS,InpFs) . s1 is Relation-like Function-like set
dSCS . s1 is Relation-like Function-like set
the Sorts of (FreeEnv SCS) . s1 is set
[:( the Sorts of (FreeEnv SCS) . s1),( the Sorts of (FreeEnv SCS) . s1):] is Relation-like set
bool [:( the Sorts of (FreeEnv SCS) . s1),( the Sorts of (FreeEnv SCS) . s1):] is set
s2 is Relation-like the Sorts of (FreeEnv SCS) . s1 -defined the Sorts of (FreeEnv SCS) . s1 -valued Function-like V18( the Sorts of (FreeEnv SCS) . s1, the Sorts of (FreeEnv SCS) . s1) Element of bool [:( the Sorts of (FreeEnv SCS) . s1),( the Sorts of (FreeEnv SCS) . s1):]
iv . s1 is set
s2 | (iv . s1) is Relation-like the Sorts of (FreeEnv SCS) . s1 -defined iv . s1 -defined the Sorts of (FreeEnv SCS) . s1 -defined the Sorts of (FreeEnv SCS) . s1 -valued Function-like Element of bool [:( the Sorts of (FreeEnv SCS) . s1),( the Sorts of (FreeEnv SCS) . s1):]
iv is Relation-like the carrier of IIG -defined Function-like non empty total Function-yielding V42() ManySortedFunction of the Sorts of (FreeEnv SCS), the Sorts of (FreeEnv SCS)
dSCS is Relation-like the carrier of IIG -defined Function-like non empty total Function-yielding V42() ManySortedFunction of the Sorts of (FreeEnv SCS), the Sorts of (FreeEnv SCS)
the Sorts of (FreeMSA the Sorts of SCS) is Relation-like non-empty non empty-yielding the carrier of IIG -defined Function-like non empty total set
Cs1 is set
the Sorts of (FreeMSA the Sorts of SCS) . Cs1 is set
[:( the Sorts of (FreeMSA the Sorts of SCS) . Cs1),( the Sorts of (FreeMSA the Sorts of SCS) . Cs1):] is Relation-like set
bool [:( the Sorts of (FreeMSA the Sorts of SCS) . Cs1),( the Sorts of (FreeMSA the Sorts of SCS) . Cs1):] is set
s2 is Relation-like the carrier of IIG -defined Function-like non empty total Function-yielding V42() ManySortedFunction of the Sorts of (FreeMSA the Sorts of SCS), the Sorts of (FreeMSA the Sorts of SCS)
s2 . Cs1 is Relation-like Function-like set
(IIG,SCS,InpFs) . Cs1 is Relation-like Function-like set
Cs2 is Relation-like the Sorts of (FreeMSA the Sorts of SCS) . Cs1 -defined the Sorts of (FreeMSA the Sorts of SCS) . Cs1 -valued Function-like V18( the Sorts of (FreeMSA the Sorts of SCS) . Cs1, the Sorts of (FreeMSA the Sorts of SCS) . Cs1) Element of bool [:( the Sorts of (FreeMSA the Sorts of SCS) . Cs1),( the Sorts of (FreeMSA the Sorts of SCS) . Cs1):]
x is Relation-like Function-like set
(FreeGen the Sorts of SCS) . Cs1 is set
[:((FreeGen the Sorts of SCS) . Cs1),( the Sorts of (FreeMSA the Sorts of SCS) . Cs1):] is Relation-like set
bool [:((FreeGen the Sorts of SCS) . Cs1),( the Sorts of (FreeMSA the Sorts of SCS) . Cs1):] is set
dom x is set
x9 is Relation-like the Sorts of (FreeMSA the Sorts of SCS) . Cs1 -defined the Sorts of (FreeMSA the Sorts of SCS) . Cs1 -valued Function-like V18( the Sorts of (FreeMSA the Sorts of SCS) . Cs1, the Sorts of (FreeMSA the Sorts of SCS) . Cs1) Element of bool [:( the Sorts of (FreeMSA the Sorts of SCS) . Cs1),( the Sorts of (FreeMSA the Sorts of SCS) . Cs1):]
s1 is Relation-like the carrier of IIG -defined Function-like non empty total Function-yielding V42() ManySortedFunction of the Sorts of (FreeMSA the Sorts of SCS), the Sorts of (FreeMSA the Sorts of SCS)
s1 . Cs1 is Relation-like Function-like set
s2 || (FreeGen the Sorts of SCS) is Relation-like the carrier of IIG -defined Function-like non empty total Function-yielding V42() ManySortedFunction of FreeGen the Sorts of SCS, the Sorts of (FreeMSA the Sorts of SCS)
(s2 || (FreeGen the Sorts of SCS)) . Cs1 is Relation-like Function-like set
Cs2 | ((FreeGen the Sorts of SCS) . Cs1) is Relation-like the Sorts of (FreeMSA the Sorts of SCS) . Cs1 -defined (FreeGen the Sorts of SCS) . Cs1 -defined the Sorts of (FreeMSA the Sorts of SCS) . Cs1 -defined the Sorts of (FreeMSA the Sorts of SCS) . Cs1 -valued Function-like Element of bool [:( the Sorts of (FreeMSA the Sorts of SCS) . Cs1),( the Sorts of (FreeMSA the Sorts of SCS) . Cs1):]
x9 | ((FreeGen the Sorts of SCS) . Cs1) is Relation-like the Sorts of (FreeMSA the Sorts of SCS) . Cs1 -defined (FreeGen the Sorts of SCS) . Cs1 -defined the Sorts of (FreeMSA the Sorts of SCS) . Cs1 -defined the Sorts of (FreeMSA the Sorts of SCS) . Cs1 -valued Function-like Element of bool [:( the Sorts of (FreeMSA the Sorts of SCS) . Cs1),( the Sorts of (FreeMSA the Sorts of SCS) . Cs1):]
s1 || (FreeGen the Sorts of SCS) is Relation-like the carrier of IIG -defined Function-like non empty total Function-yielding V42() ManySortedFunction of FreeGen the Sorts of SCS, the Sorts of (FreeMSA the Sorts of SCS)
IIG is non empty non void V56() Circuit-like monotonic 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 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
K539( the carrier of IIG, the ResultSort of IIG) is Element of bool the carrier of IIG
the carrier of IIG \ K539( the carrier of IIG, the ResultSort of IIG) is Element of bool the carrier of IIG
InnerVertices 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
SCS is non-empty finitely-generated finite-yielding MSAlgebra over IIG
FreeEnv SCS is strict non-empty free MSAlgebra over IIG
the Sorts of SCS is Relation-like non-empty non empty-yielding the carrier of IIG -defined Function-like non empty total set
FreeMSA the Sorts of SCS is strict non-empty MSAlgebra over IIG
the Sorts of (FreeEnv SCS) is Relation-like non-empty non empty-yielding the carrier of IIG -defined Function-like non empty total set
InpFs is Relation-like InputVertices IIG -defined Function-like total InputValues of SCS
(IIG,SCS,InpFs) is Relation-like the carrier of IIG -defined Function-like non empty total Function-yielding V42() ManySortedFunction of the Sorts of (FreeEnv SCS), the Sorts of (FreeEnv SCS)
iv is Element of the carrier of IIG
the Sorts of (FreeEnv SCS) . iv is non empty finite countable set
(IIG,SCS,InpFs) . iv is Relation-like the Sorts of (FreeEnv SCS) . iv -defined the Sorts of (FreeEnv SCS) . iv -valued Function-like V18( the Sorts of (FreeEnv SCS) . iv, the Sorts of (FreeEnv SCS) . iv) finite countable Element of bool [:( the Sorts of (FreeEnv SCS) . iv),( the Sorts of (FreeEnv SCS) . iv):]
[:( the Sorts of (FreeEnv SCS) . iv),( the Sorts of (FreeEnv SCS) . iv):] is Relation-like finite countable set
bool [:( the Sorts of (FreeEnv SCS) . iv),( the Sorts of (FreeEnv SCS) . iv):] is finite V32() countable set
dSCS is Relation-like Function-like non empty finite countable DecoratedTree-like Element of the Sorts of (FreeEnv SCS) . iv
((IIG,SCS,InpFs) . iv) . dSCS is Relation-like Function-like non empty finite countable DecoratedTree-like Element of the Sorts of (FreeEnv SCS) . iv
s1 is set
[s1,iv] is set
root-tree [s1,iv] is Relation-like Function-like finite countable DecoratedTree-like set
dSCS . {} is set
s2 is Element of the carrier' of IIG
[s2, the carrier of IIG] is set
the_result_sort_of s2 is Element of the carrier of IIG
FreeSort the Sorts of SCS is Relation-like non-empty non empty-yielding the carrier of IIG -defined Function-like non empty total set
FreeOper the Sorts of SCS is Relation-like the carrier' of IIG -defined Function-like non empty total Function-yielding V42() ManySortedFunction of the Arity of IIG * ((FreeSort the Sorts of SCS) #), the ResultSort of IIG * (FreeSort the Sorts of SCS)
the Arity of IIG is Relation-like the carrier' of IIG -defined the carrier of IIG * -valued Function-like V18( the carrier' of IIG, the carrier of IIG * ) Function-yielding V42() Element of bool [: the carrier' of IIG,( the carrier of IIG *):]
the carrier of IIG * is functional non empty FinSequence-membered M8( 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 SCS) # is Relation-like the carrier of IIG * -defined Function-like non empty total set
the Arity of IIG * ((FreeSort the Sorts of SCS) #) is Relation-like the carrier' of IIG -defined Function-like non empty total set
the ResultSort of IIG * (FreeSort the Sorts of SCS) is Relation-like non-empty non empty-yielding the carrier' of IIG -defined Function-like non empty total set
MSAlgebra(# (FreeSort the Sorts of SCS),(FreeOper the Sorts of SCS) #) is strict MSAlgebra over IIG
(FreeSort the Sorts of SCS) . iv is non empty set
FreeSort ( the Sorts of SCS,iv) is functional non empty constituted-DTrees Element of bool (TS (DTConMSA the Sorts of SCS))
DTConMSA the Sorts of SCS is non empty strict with_terminals with_nonterminals with_useful_nonterminals L13()
TS (DTConMSA the Sorts of SCS) is functional constituted-DTrees Element of bool (FinTrees the carrier of (DTConMSA the Sorts of SCS))
the carrier of (DTConMSA the Sorts of SCS) is non empty set
FinTrees the carrier of (DTConMSA the Sorts of SCS) is functional non empty constituted-DTrees DTree-set of the carrier of (DTConMSA the Sorts of SCS)
bool (FinTrees the carrier of (DTConMSA the Sorts of SCS)) is set
bool (TS (DTConMSA the Sorts of SCS)) is set
(IIG,SCS,InpFs) is Relation-like the carrier of IIG -defined Function-like non empty total Function-yielding V42() ManySortedFunction of FreeGen the Sorts of SCS, the Sorts of (FreeEnv SCS)
FreeGen the Sorts of SCS is Relation-like the carrier of IIG -defined Function-like non empty total GeneratorSet of FreeMSA the Sorts of SCS
(IIG,SCS,InpFs) . iv is Relation-like (FreeGen the Sorts of SCS) . iv -defined the Sorts of (FreeEnv SCS) . iv -valued Function-like V18((FreeGen the Sorts of SCS) . iv, the Sorts of (FreeEnv SCS) . iv) Element of bool [:((FreeGen the Sorts of SCS) . iv),( the Sorts of (FreeEnv SCS) . iv):]
(FreeGen the Sorts of SCS) . iv is set
[:((FreeGen the Sorts of SCS) . iv),( the Sorts of (FreeEnv SCS) . iv):] is Relation-like set
bool [:((FreeGen the Sorts of SCS) . iv),( the Sorts of (FreeEnv SCS) . iv):] is set
the Sorts of SCS . iv is non empty set
{ b₁ where b₁ is Relation-like Function-like Element of TS (DTConMSA the Sorts of SCS) : ( ex b₂ being set st
( b₂ in the Sorts of SCS . iv & b₁ = root-tree [b₂,iv] ) or ex b₂ being Element of the carrier' of IIG st
( [b₂, the carrier of IIG] = b₁ . {} & the_result_sort_of b₂ = iv ) ) } is set
FreeGen (iv, the Sorts of SCS) is non empty Element of bool ((FreeSort the Sorts of SCS) . iv)
bool ((FreeSort the Sorts of SCS) . iv) is set
Cs1 is Relation-like Function-like Element of TS (DTConMSA the Sorts of SCS)
Cs2 is set
[Cs2,iv] is set
root-tree [Cs2,iv] 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
Cs1 . {} is set
the_result_sort_of x is Element of the carrier of IIG
dom ((IIG,SCS,InpFs) . iv) is set
((IIG,SCS,InpFs) . iv) . dSCS is set
id (FreeGen (iv, the Sorts of SCS)) is Relation-like FreeGen (iv, the Sorts of SCS) -defined FreeGen (iv, the Sorts of SCS) -valued Function-like one-to-one non empty total Element of bool [:(FreeGen (iv, the Sorts of SCS)),(FreeGen (iv, the Sorts of SCS)):]
[:(FreeGen (iv, the Sorts of SCS)),(FreeGen (iv, the Sorts of SCS)):] is Relation-like set
bool [:(FreeGen (iv, the Sorts of SCS)),(FreeGen (iv, the Sorts of SCS)):] is set
(id (FreeGen (iv, the Sorts of SCS))) . dSCS is set
IIG is non empty non void V56() Circuit-like monotonic 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 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
K539( the carrier of IIG, the ResultSort of IIG) is Element of bool the carrier of IIG
the carrier of IIG \ K539( the carrier of IIG, the ResultSort of IIG) is Element of bool the carrier of IIG
SCS is non-empty finitely-generated finite-yielding MSAlgebra over IIG
the Sorts of SCS is Relation-like non-empty non empty-yielding the carrier of IIG -defined Function-like non empty total set
FreeEnv SCS is strict non-empty free MSAlgebra over IIG
FreeMSA the Sorts of SCS is strict non-empty MSAlgebra over IIG
the Sorts of (FreeEnv SCS) is Relation-like non-empty non empty-yielding the carrier of IIG -defined Function-like non empty total set
InpFs is Relation-like InputVertices IIG -defined Function-like total InputValues of SCS
(IIG,SCS,InpFs) is Relation-like the carrier of IIG -defined Function-like non empty total Function-yielding V42() ManySortedFunction of the Sorts of (FreeEnv SCS), the Sorts of (FreeEnv SCS)
iv is Element of the carrier of IIG
the Sorts of SCS . iv is non empty set
(IIG,SCS,InpFs) . iv is Relation-like the Sorts of (FreeEnv SCS) . iv -defined the Sorts of (FreeEnv SCS) . iv -valued Function-like V18( the Sorts of (FreeEnv SCS) . iv, the Sorts of (FreeEnv SCS) . iv) finite countable Element of bool [:( the Sorts of (FreeEnv SCS) . iv),( the Sorts of (FreeEnv SCS) . iv):]
the Sorts of (FreeEnv SCS) . iv is non empty finite countable set
[:( the Sorts of (FreeEnv SCS) . iv),( the Sorts of (FreeEnv SCS) . iv):] is Relation-like finite countable set
bool [:( the Sorts of (FreeEnv SCS) . iv),( the Sorts of (FreeEnv SCS) . iv):] is finite V32() countable set
InpFs . iv is set
[(InpFs . iv),iv] is set
root-tree [(InpFs . iv),iv] is Relation-like Function-like finite countable DecoratedTree-like set
dSCS is Element of the Sorts of SCS . iv
[dSCS,iv] is set
root-tree [dSCS,iv] is Relation-like Function-like finite countable DecoratedTree-like set
((IIG,SCS,InpFs) . iv) . (root-tree [dSCS,iv]) is set
FreeGen (iv, the Sorts of SCS) is non empty Element of bool ((FreeSort the Sorts of SCS) . iv)
FreeSort the Sorts of SCS is Relation-like non-empty non empty-yielding the carrier of IIG -defined Function-like non empty total set
(FreeSort the Sorts of SCS) . iv is non empty set
bool ((FreeSort the Sorts of SCS) . iv) is set
(IIG,SCS,InpFs) is Relation-like the carrier of IIG -defined Function-like non empty total Function-yielding V42() ManySortedFunction of FreeGen the Sorts of SCS, the Sorts of (FreeEnv SCS)
FreeGen the Sorts of SCS is Relation-like the carrier of IIG -defined Function-like non empty total GeneratorSet of FreeMSA the Sorts of SCS
(IIG,SCS,InpFs) . iv is Relation-like (FreeGen the Sorts of SCS) . iv -defined the Sorts of (FreeEnv SCS) . iv -valued Function-like V18((FreeGen the Sorts of SCS) . iv, the Sorts of (FreeEnv SCS) . iv) Element of bool [:((FreeGen the Sorts of SCS) . iv),( the Sorts of (FreeEnv SCS) . iv):]
(FreeGen the Sorts of SCS) . iv is set
[:((FreeGen the Sorts of SCS) . iv),( the Sorts of (FreeEnv SCS) . iv):] is Relation-like set
bool [:((FreeGen the Sorts of SCS) . iv),( the Sorts of (FreeEnv SCS) . iv):] is set
FreeOper the Sorts of SCS is Relation-like the carrier' of IIG -defined Function-like non empty total Function-yielding V42() ManySortedFunction of the Arity of IIG * ((FreeSort the Sorts of SCS) #), the ResultSort of IIG * (FreeSort the Sorts of SCS)
the Arity of IIG is Relation-like the carrier' of IIG -defined the carrier of IIG * -valued Function-like V18( the carrier' of IIG, the carrier of IIG * ) Function-yielding V42() Element of bool [: the carrier' of IIG,( the carrier of IIG *):]
the carrier of IIG * is functional non empty FinSequence-membered M8( 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 SCS) # is Relation-like the carrier of IIG * -defined Function-like non empty total set
the Arity of IIG * ((FreeSort the Sorts of SCS) #) is Relation-like the carrier' of IIG -defined Function-like non empty total set
the ResultSort of IIG * (FreeSort the Sorts of SCS) is Relation-like non-empty non empty-yielding the carrier' of IIG -defined Function-like non empty total set
MSAlgebra(# (FreeSort the Sorts of SCS),(FreeOper the Sorts of SCS) #) is strict MSAlgebra over IIG
s2 is Relation-like Function-like non empty finite countable DecoratedTree-like Element of the Sorts of (FreeEnv SCS) . iv
dom ((IIG,SCS,InpFs) . iv) is set
((IIG,SCS,InpFs) . iv) . s2 is set
(FreeGen (iv, the Sorts of SCS)) --> (root-tree [(InpFs . iv),iv]) is Relation-like FreeGen (iv, the Sorts of SCS) -defined {(root-tree [(InpFs . iv),iv])} -valued Function-like constant non empty total V18( FreeGen (iv, the Sorts of SCS),{(root-tree [(InpFs . iv),iv])}) Function-yielding V42() Element of bool [:(FreeGen (iv, the Sorts of SCS)),{(root-tree [(InpFs . iv),iv])}:]
{(root-tree [(InpFs . iv),iv])} is functional non empty trivial finite V32() 1 -element with_common_domain countable set
[:(FreeGen (iv, the Sorts of SCS)),{(root-tree [(InpFs . iv),iv])}:] is Relation-like set
bool [:(FreeGen (iv, the Sorts of SCS)),{(root-tree [(InpFs . iv),iv])}:] is set
((FreeGen (iv, the Sorts of SCS)) --> (root-tree [(InpFs . iv),iv])) . s2 is Relation-like Function-like set
IIG is non empty non void V56() Circuit-like monotonic 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 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
K539( the carrier of IIG, the ResultSort of IIG) is Element of bool the carrier of IIG
the carrier of IIG \ K539( the carrier of IIG, the ResultSort of IIG) is Element of bool the carrier of IIG
InnerVertices IIG is non empty Element of bool the carrier of IIG
SCS is non-empty finitely-generated finite-yielding MSAlgebra over IIG
FreeEnv SCS is strict non-empty free MSAlgebra over IIG
the Sorts of SCS is Relation-like non-empty non empty-yielding the carrier of IIG -defined Function-like non empty total set
FreeMSA the Sorts of SCS is strict non-empty MSAlgebra over IIG
the Sorts of (FreeEnv SCS) is Relation-like non-empty non empty-yielding the carrier of IIG -defined Function-like non empty total set
InpFs is Relation-like InputVertices IIG -defined Function-like total InputValues of SCS
(IIG,SCS,InpFs) is Relation-like the carrier of IIG -defined Function-like non empty total Function-yielding V42() ManySortedFunction of the Sorts of (FreeEnv SCS), the Sorts of (FreeEnv SCS)
iv is Element of the carrier of IIG
the Sorts of (FreeEnv SCS) . iv is non empty finite countable set
action_at iv is Element of the carrier' of IIG
[(action_at iv), the carrier of IIG] is set
the_arity_of (action_at iv) is Relation-like NAT -defined the carrier of IIG -valued Function-like finite countable FinSequence-like FinSubsequence-like Element of the carrier of IIG *
the carrier of IIG * is functional non empty FinSequence-membered M8( the carrier of IIG)
(IIG,SCS,InpFs) . iv is Relation-like the Sorts of (FreeEnv SCS) . iv -defined the Sorts of (FreeEnv SCS) . iv -valued Function-like V18( the Sorts of (FreeEnv SCS) . iv, the Sorts of (FreeEnv SCS) . iv) finite countable Element of bool [:( the Sorts of (FreeEnv SCS) . iv),( the Sorts of (FreeEnv SCS) . iv):]
[:( the Sorts of (FreeEnv SCS) . iv),( the Sorts of (FreeEnv SCS) . iv):] is Relation-like finite countable set
bool [:( the Sorts of (FreeEnv SCS) . iv),( the Sorts of (FreeEnv SCS) . iv):] is finite V32() countable set
dSCS is Relation-like Function-like non empty finite countable DecoratedTree-like Element of the Sorts of (FreeEnv SCS) . iv
((IIG,SCS,InpFs) . iv) . dSCS is Relation-like Function-like non empty finite countable DecoratedTree-like Element of the Sorts of (FreeEnv SCS) . iv
s1 is Relation-like NAT -defined Function-like finite countable FinSequence-like FinSubsequence-like DTree-yielding set
[(action_at iv), the carrier of IIG] -tree s1 is Relation-like Function-like DecoratedTree-like set
dom s1 is finite countable V150() V151() V152() V153() V154() V155() V163() V164() V165() Element of bool NAT
s2 is Relation-like NAT -defined Function-like finite countable FinSequence-like FinSubsequence-like DTree-yielding set
dom s2 is finite countable V150() V151() V152() V153() V154() V155() V163() V164() V165() Element of bool NAT
[(action_at iv), the carrier of IIG] -tree s2 is Relation-like Function-like DecoratedTree-like set
the_result_sort_of (action_at iv) is Element of the carrier of IIG
len s1 is V21() V22() V23() V27() finite cardinal countable V133() V134() ext-real V148() V149() V150() V151() V152() V153() V154() V155() V163() V164() V165() Element of NAT
len (the_arity_of (action_at iv)) is V21() V22() V23() V27() finite cardinal countable V133() V134() ext-real V148() V149() V150() V151() V152() V153() V154() V155() V163() V164() V165() Element of NAT
Cs2 is V21() V22() V23() V27() finite cardinal countable V133() V134() ext-real set
dom (the_arity_of (action_at iv)) is finite countable V150() V151() V152() V153() V154() V155() V163() V164() V165() Element of bool NAT
s1 . Cs2 is set
(the_arity_of (action_at iv)) . Cs2 is set
the Sorts of (FreeEnv SCS) . ((the_arity_of (action_at iv)) . Cs2) is set
(the_arity_of (action_at iv)) /. Cs2 is Element of the carrier of IIG
the Sorts of (FreeEnv SCS) . ((the_arity_of (action_at iv)) /. Cs2) is non empty finite countable set
s2 . Cs2 is set
(IIG,SCS,InpFs) . ((the_arity_of (action_at iv)) /. Cs2) is Relation-like the Sorts of (FreeEnv SCS) . ((the_arity_of (action_at iv)) /. Cs2) -defined the Sorts of (FreeEnv SCS) . ((the_arity_of (action_at iv)) /. Cs2) -valued Function-like V18( the Sorts of (FreeEnv SCS) . ((the_arity_of (action_at iv)) /. Cs2), the Sorts of (FreeEnv SCS) . ((the_arity_of (action_at iv)) /. Cs2)) finite countable Element of bool [:( the Sorts of (FreeEnv SCS) . ((the_arity_of (action_at iv)) /. Cs2)),( the Sorts of (FreeEnv SCS) . ((the_arity_of (action_at iv)) /. Cs2)):]
[:( the Sorts of (FreeEnv SCS) . ((the_arity_of (action_at iv)) /. Cs2)),( the Sorts of (FreeEnv SCS) . ((the_arity_of (action_at iv)) /. Cs2)):] is Relation-like finite countable set
bool [:( the Sorts of (FreeEnv SCS) . ((the_arity_of (action_at iv)) /. Cs2)),( the Sorts of (FreeEnv SCS) . ((the_arity_of (action_at iv)) /. Cs2)):] is finite V32() countable set
((IIG,SCS,InpFs) . ((the_arity_of (action_at iv)) /. Cs2)) . (s1 . Cs2) is set
Cs2 is V21() V22() V23() V27() finite cardinal countable V133() V134() ext-real set
s1 . Cs2 is set
(the_arity_of (action_at iv)) . Cs2 is set
the Sorts of (FreeEnv SCS) . ((the_arity_of (action_at iv)) . Cs2) is set
(the_arity_of (action_at iv)) /. Cs2 is Element of the carrier of IIG
the Sorts of (FreeEnv SCS) . ((the_arity_of (action_at iv)) /. Cs2) is non empty finite countable set
Args ((action_at iv),(FreeEnv SCS)) is functional non empty Element of rng ( the Sorts of (FreeEnv SCS) #)
the Sorts of (FreeEnv SCS) # is Relation-like the carrier of IIG * -defined Function-like non empty total set
rng ( the Sorts of (FreeEnv SCS) #) is non empty set
FreeSort the Sorts of SCS is Relation-like non-empty non empty-yielding the carrier of IIG -defined Function-like non empty total set
FreeOper the Sorts of SCS is Relation-like the carrier' of IIG -defined Function-like non empty total Function-yielding V42() ManySortedFunction of the Arity of IIG * ((FreeSort the Sorts of SCS) #), the ResultSort of IIG * (FreeSort the Sorts of SCS)
the Arity of IIG is Relation-like the carrier' of IIG -defined the carrier of IIG * -valued Function-like V18( the carrier' of IIG, the carrier of IIG * ) Function-yielding V42() 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 SCS) # is Relation-like the carrier of IIG * -defined Function-like non empty total set
the Arity of IIG * ((FreeSort the Sorts of SCS) #) is Relation-like the carrier' of IIG -defined Function-like non empty total set
the ResultSort of IIG * (FreeSort the Sorts of SCS) is Relation-like non-empty non empty-yielding the carrier' of IIG -defined Function-like non empty total set
MSAlgebra(# (FreeSort the Sorts of SCS),(FreeOper the Sorts of SCS) #) is strict MSAlgebra over IIG
( the Arity of IIG * ((FreeSort the Sorts of SCS) #)) . (action_at iv) is set
DTConMSA the Sorts of SCS is non empty strict with_terminals with_nonterminals with_useful_nonterminals L13()
the carrier of (DTConMSA the Sorts of SCS) is non empty set
FinTrees the carrier of (DTConMSA the Sorts of SCS) is functional non empty constituted-DTrees DTree-set of the carrier of (DTConMSA the Sorts of SCS)
TS (DTConMSA the Sorts of SCS) is functional constituted-DTrees Element of bool (FinTrees the carrier of (DTConMSA the Sorts of SCS))
bool (FinTrees the carrier of (DTConMSA the Sorts of SCS)) is set
Sym ((action_at iv), the Sorts of SCS) is Element of K355((DTConMSA the Sorts of SCS))
K355((DTConMSA the Sorts of SCS)) is non empty Element of bool the carrier of (DTConMSA the Sorts of SCS)
bool the carrier of (DTConMSA the Sorts of SCS) is set
x is Relation-like NAT -defined FinTrees the carrier of (DTConMSA the Sorts of SCS) -valued Function-like finite countable Function-yielding V42() FinSequence-like FinSubsequence-like FinSequence of TS (DTConMSA the Sorts of SCS)
roots x is Relation-like NAT -defined the carrier of (DTConMSA the Sorts of SCS) -valued Function-like finite countable FinSequence-like FinSubsequence-like FinSequence of the carrier of (DTConMSA the Sorts of SCS)
len s2 is V21() V22() V23() V27() finite cardinal countable V133() V134() ext-real V148() V149() V150() V151() V152() V153() V154() V155() V163() V164() V165() Element of NAT
p is Relation-like NAT -defined FinTrees the carrier of (DTConMSA the Sorts of SCS) -valued Function-like finite countable Function-yielding V42() FinSequence-like FinSubsequence-like FinSequence of TS (DTConMSA the Sorts of SCS)
roots p is Relation-like NAT -defined the carrier of (DTConMSA the Sorts of SCS) -valued Function-like finite countable FinSequence-like FinSubsequence-like FinSequence of the carrier of (DTConMSA the Sorts of SCS)
ods is V21() V22() V23() V27() finite cardinal countable V133() V134() ext-real set
s2 . ods is set
(the_arity_of (action_at iv)) /. ods is Element of the carrier of IIG
(IIG,SCS,InpFs) . ((the_arity_of (action_at iv)) /. ods) is Relation-like the Sorts of (FreeEnv SCS) . ((the_arity_of (action_at iv)) /. ods) -defined the Sorts of (FreeEnv SCS) . ((the_arity_of (action_at iv)) /. ods) -valued Function-like V18( the Sorts of (FreeEnv SCS) . ((the_arity_of (action_at iv)) /. ods), the Sorts of (FreeEnv SCS) . ((the_arity_of (action_at iv)) /. ods)) finite countable Element of bool [:( the Sorts of (FreeEnv SCS) . ((the_arity_of (action_at iv)) /. ods)),( the Sorts of (FreeEnv SCS) . ((the_arity_of (action_at iv)) /. ods)):]
the Sorts of (FreeEnv SCS) . ((the_arity_of (action_at iv)) /. ods) is non empty finite countable set
[:( the Sorts of (FreeEnv SCS) . ((the_arity_of (action_at iv)) /. ods)),( the Sorts of (FreeEnv SCS) . ((the_arity_of (action_at iv)) /. ods)):] is Relation-like finite countable set
bool [:( the Sorts of (FreeEnv SCS) . ((the_arity_of (action_at iv)) /. ods)),( the Sorts of (FreeEnv SCS) . ((the_arity_of (action_at iv)) /. ods)):] is finite V32() countable set
s1 . ods is set
((IIG,SCS,InpFs) . ((the_arity_of (action_at iv)) /. ods)) . (s1 . ods) is set
x9 is Relation-like Function-like Element of Args ((action_at iv),(FreeEnv SCS))
Cs2 is Relation-like Function-like Element of Args ((action_at iv),(FreeEnv SCS))
(IIG,SCS,InpFs) # Cs2 is Relation-like Function-like Element of Args ((action_at iv),(FreeEnv SCS))
(Sym ((action_at iv), the Sorts of SCS)) -tree x is Relation-like the carrier of (DTConMSA the Sorts of SCS) -valued Function-like finite countable DecoratedTree-like Element of FinTrees the carrier of (DTConMSA the Sorts of SCS)
DenOp ((action_at iv), the Sorts of SCS) is Relation-like ( the Arity of IIG * ((FreeSort the Sorts of SCS) #)) . (action_at iv) -defined ( the ResultSort of IIG * (FreeSort the Sorts of SCS)) . (action_at iv) -valued Function-like V18(( the Arity of IIG * ((FreeSort the Sorts of SCS) #)) . (action_at iv),( the ResultSort of IIG * (FreeSort the Sorts of SCS)) . (action_at iv)) Element of bool [:(( the Arity of IIG * ((FreeSort the Sorts of SCS) #)) . (action_at iv)),(( the ResultSort of IIG * (FreeSort the Sorts of SCS)) . (action_at iv)):]
( the ResultSort of IIG * (FreeSort the Sorts of SCS)) . (action_at iv) is non empty set
[:(( the Arity of IIG * ((FreeSort the Sorts of SCS) #)) . (action_at iv)),(( the ResultSort of IIG * (FreeSort the Sorts of SCS)) . (action_at iv)):] is Relation-like set
bool [:(( the Arity of IIG * ((FreeSort the Sorts of SCS) #)) . (action_at iv)),(( the ResultSort of IIG * (FreeSort the Sorts of SCS)) . (action_at iv)):] is set
(DenOp ((action_at iv), the Sorts of SCS)) . Cs2 is set
the Arity of IIG * ( the Sorts of (FreeEnv SCS) #) is Relation-like the carrier' of IIG -defined Function-like non empty total set
the ResultSort of IIG * the Sorts of (FreeEnv SCS) is Relation-like non-empty non empty-yielding the carrier' of IIG -defined Function-like non empty total set
the Charact of (FreeEnv SCS) is Relation-like the carrier' of IIG -defined Function-like non empty total Function-yielding V42() ManySortedFunction of the Arity of IIG * ( the Sorts of (FreeEnv SCS) #), the ResultSort of IIG * the Sorts of (FreeEnv SCS)
the Charact of (FreeEnv SCS) . (action_at iv) is Relation-like ( the Arity of IIG * ( the Sorts of (FreeEnv SCS) #)) . (action_at iv) -defined ( the ResultSort of IIG * the Sorts of (FreeEnv SCS)) . (action_at iv) -valued Function-like V18(( the Arity of IIG * ( the Sorts of (FreeEnv SCS) #)) . (action_at iv),( the ResultSort of IIG * the Sorts of (FreeEnv SCS)) . (action_at iv)) Element of bool [:(( the Arity of IIG * ( the Sorts of (FreeEnv SCS) #)) . (action_at iv)),(( the ResultSort of IIG * the Sorts of (FreeEnv SCS)) . (action_at iv)):]
( the Arity of IIG * ( the Sorts of (FreeEnv SCS) #)) . (action_at iv) is set
( the ResultSort of IIG * the Sorts of (FreeEnv SCS)) . (action_at iv) is non empty set
[:(( the Arity of IIG * ( the Sorts of (FreeEnv SCS) #)) . (action_at iv)),(( the ResultSort of IIG * the Sorts of (FreeEnv SCS)) . (action_at iv)):] is Relation-like set
bool [:(( the Arity of IIG * ( the Sorts of (FreeEnv SCS) #)) . (action_at iv)),(( the ResultSort of IIG * the Sorts of (FreeEnv SCS)) . (action_at iv)):] is set
( the Charact of (FreeEnv SCS) . (action_at iv)) . Cs2 is set
Result ((action_at iv),(FreeEnv SCS)) is non empty Element of rng the Sorts of (FreeEnv SCS)
rng the Sorts of (FreeEnv SCS) is non empty set
Den ((action_at iv),(FreeEnv SCS)) is Relation-like Args ((action_at iv),(FreeEnv SCS)) -defined Result ((action_at iv),(FreeEnv SCS)) -valued Function-like V18( Args ((action_at iv),(FreeEnv SCS)), Result ((action_at iv),(FreeEnv SCS))) Element of bool [:(Args ((action_at iv),(FreeEnv SCS))),(Result ((action_at iv),(FreeEnv SCS))):]
[:(Args ((action_at iv),(FreeEnv SCS))),(Result ((action_at iv),(FreeEnv SCS))):] is Relation-like set
bool [:(Args ((action_at iv),(FreeEnv SCS))),(Result ((action_at iv),(FreeEnv SCS))):] is set
(Den ((action_at iv),(FreeEnv SCS))) . Cs2 is Element of Result ((action_at iv),(FreeEnv SCS))
(Den ((action_at iv),(FreeEnv SCS))) . s2 is set
(FreeOper the Sorts of SCS) . (action_at iv) is Relation-like ( the Arity of IIG * ((FreeSort the Sorts of SCS) #)) . (action_at iv) -defined ( the ResultSort of IIG * (FreeSort the Sorts of SCS)) . (action_at iv) -valued Function-like V18(( the Arity of IIG * ((FreeSort the Sorts of SCS) #)) . (action_at iv),( the ResultSort of IIG * (FreeSort the Sorts of SCS)) . (action_at iv)) Element of bool [:(( the Arity of IIG * ((FreeSort the Sorts of SCS) #)) . (action_at iv)),(( the ResultSort of IIG * (FreeSort the Sorts of SCS)) . (action_at iv)):]
((FreeOper the Sorts of SCS) . (action_at iv)) . s2 is set
(DenOp ((action_at iv), the Sorts of SCS)) . s2 is set
(Sym ((action_at iv), the Sorts of SCS)) -tree p is Relation-like the carrier of (DTConMSA the Sorts of SCS) -valued Function-like finite countable DecoratedTree-like Element of FinTrees the carrier of (DTConMSA the Sorts of SCS)
IIG is non empty non void V56() Circuit-like monotonic 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 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
K539( the carrier of IIG, the ResultSort of IIG) is Element of bool the carrier of IIG
the carrier of IIG \ K539( the carrier of IIG, the ResultSort of IIG) is Element of bool the carrier of IIG
SortsWithConstants IIG is Element of bool the carrier of IIG
SCS is non-empty finitely-generated finite-yielding MSAlgebra over IIG
FreeEnv SCS is strict non-empty free MSAlgebra over IIG
the Sorts of SCS is Relation-like non-empty non empty-yielding the carrier of IIG -defined Function-like non empty total set
FreeMSA the Sorts of SCS is strict non-empty MSAlgebra over IIG
the Sorts of (FreeEnv SCS) is Relation-like non-empty non empty-yielding the carrier of IIG -defined Function-like non empty total set
InpFs is Relation-like InputVertices IIG -defined Function-like total InputValues of SCS
(IIG,SCS,InpFs) is Relation-like the carrier of IIG -defined Function-like non empty total Function-yielding V42() ManySortedFunction of the Sorts of (FreeEnv SCS), the Sorts of (FreeEnv SCS)
iv is Element of the carrier of IIG
the Sorts of (FreeEnv SCS) . iv is non empty finite countable set
(IIG,SCS,InpFs) . iv is Relation-like the Sorts of (FreeEnv SCS) . iv -defined the Sorts of (FreeEnv SCS) . iv -valued Function-like V18( the Sorts of (FreeEnv SCS) . iv, the Sorts of (FreeEnv SCS) . iv) finite countable Element of bool [:( the Sorts of (FreeEnv SCS) . iv),( the Sorts of (FreeEnv SCS) . iv):]
[:( the Sorts of (FreeEnv SCS) . iv),( the Sorts of (FreeEnv SCS) . iv):] is Relation-like finite countable set
bool [:( the Sorts of (FreeEnv SCS) . iv),( the Sorts of (FreeEnv SCS) . iv):] is finite V32() countable set
action_at iv is Element of the carrier' of IIG
[(action_at iv), the carrier of IIG] is set
root-tree [(action_at iv), the carrier of IIG] is Relation-like Function-like finite countable DecoratedTree-like set
dSCS is Relation-like Function-like non empty finite countable DecoratedTree-like Element of the Sorts of (FreeEnv SCS) . iv
((IIG,SCS,InpFs) . iv) . dSCS is Relation-like Function-like non empty finite countable DecoratedTree-like Element of the Sorts of (FreeEnv SCS) . iv
FreeSort the Sorts of SCS is Relation-like non-empty non empty-yielding the carrier of IIG -defined Function-like non empty total set
FreeOper the Sorts of SCS is Relation-like the carrier' of IIG -defined Function-like non empty total Function-yielding V42() ManySortedFunction of the Arity of IIG * ((FreeSort the Sorts of SCS) #), the ResultSort of IIG * (FreeSort the Sorts of SCS)
the Arity of IIG is Relation-like the carrier' of IIG -defined the carrier of IIG * -valued Function-like V18( the carrier' of IIG, the carrier of IIG * ) Function-yielding V42() Element of bool [: the carrier' of IIG,( the carrier of IIG *):]
the carrier of IIG * is functional non empty FinSequence-membered M8( 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 SCS) # is Relation-like the carrier of IIG * -defined Function-like non empty total set
the Arity of IIG * ((FreeSort the Sorts of SCS) #) is Relation-like the carrier' of IIG -defined Function-like non empty total set
the ResultSort of IIG * (FreeSort the Sorts of SCS) is Relation-like non-empty non empty-yielding the carrier' of IIG -defined Function-like non empty total set
MSAlgebra(# (FreeSort the Sorts of SCS),(FreeOper the Sorts of SCS) #) is strict MSAlgebra over IIG
(FreeSort the Sorts of SCS) . iv is non empty set
FreeSort ( the Sorts of SCS,iv) is functional non empty constituted-DTrees Element of bool (TS (DTConMSA the Sorts of SCS))
DTConMSA the Sorts of SCS is non empty strict with_terminals with_nonterminals with_useful_nonterminals L13()
TS (DTConMSA the Sorts of SCS) is functional constituted-DTrees Element of bool (FinTrees the carrier of (DTConMSA the Sorts of SCS))
the carrier of (DTConMSA the Sorts of SCS) is non empty set
FinTrees the carrier of (DTConMSA the Sorts of SCS) is functional non empty constituted-DTrees DTree-set of the carrier of (DTConMSA the Sorts of SCS)
bool (FinTrees the carrier of (DTConMSA the Sorts of SCS)) is set
bool (TS (DTConMSA the Sorts of SCS)) is set
the Sorts of SCS . iv is non empty set
{ b₁ where b₁ is Relation-like Function-like Element of TS (DTConMSA the Sorts of SCS) : ( ex b₂ being set st
( b₂ in the Sorts of SCS . iv & b₁ = root-tree [b₂,iv] ) or ex b₂ being Element of the carrier' of IIG st
( [b₂, the carrier of IIG] = b₁ . {} & the_result_sort_of b₂ = iv ) ) } is set
(IIG,SCS,InpFs) is Relation-like the carrier of IIG -defined Function-like non empty total Function-yielding V42() ManySortedFunction of FreeGen the Sorts of SCS, the Sorts of (FreeEnv SCS)
FreeGen the Sorts of SCS is Relation-like the carrier of IIG -defined Function-like non empty total GeneratorSet of FreeMSA the Sorts of SCS
(IIG,SCS,InpFs) . iv is Relation-like (FreeGen the Sorts of SCS) . iv -defined the Sorts of (FreeEnv SCS) . iv -valued Function-like V18((FreeGen the Sorts of SCS) . iv, the Sorts of (FreeEnv SCS) . iv) Element of bool [:((FreeGen the Sorts of SCS) . iv),( the Sorts of (FreeEnv SCS) . iv):]
(FreeGen the Sorts of SCS) . iv is set
[:((FreeGen the Sorts of SCS) . iv),( the Sorts of (FreeEnv SCS) . iv):] is Relation-like set
bool [:((FreeGen the Sorts of SCS) . iv),( the Sorts of (FreeEnv SCS) . iv):] is set
FreeGen (iv, the Sorts of SCS) is non empty Element of bool ((FreeSort the Sorts of SCS) . iv)
bool ((FreeSort the Sorts of SCS) . iv) is set
s2 is set
[s2,iv] is set
root-tree [s2,iv] is Relation-like Function-like finite countable DecoratedTree-like set
dom ((IIG,SCS,InpFs) . iv) is set
((IIG,SCS,InpFs) . iv) . dSCS is set
(FreeGen (iv, the Sorts of SCS)) --> (root-tree [(action_at iv), the carrier of IIG]) is Relation-like FreeGen (iv, the Sorts of SCS) -defined {(root-tree [(action_at iv), the carrier of IIG])} -valued Function-like constant non empty total V18( FreeGen (iv, the Sorts of SCS),{(root-tree [(action_at iv), the carrier of IIG])}) Function-yielding V42() Element of bool [:(FreeGen (iv, the Sorts of SCS)),{(root-tree [(action_at iv), the carrier of IIG])}:]
{(root-tree [(action_at iv), the carrier of IIG])} is functional non empty trivial finite V32() 1 -element with_common_domain countable set
[:(FreeGen (iv, the Sorts of SCS)),{(root-tree [(action_at iv), the carrier of IIG])}:] is Relation-like set
bool [:(FreeGen (iv, the Sorts of SCS)),{(root-tree [(action_at iv), the carrier of IIG])}:] is set
((FreeGen (iv, the Sorts of SCS)) --> (root-tree [(action_at iv), the carrier of IIG])) . dSCS is Relation-like Function-like set
dSCS . {} is set
s2 is Element of the carrier' of IIG
[s2, the carrier of IIG] is set
the_result_sort_of s2 is Element of the carrier of IIG
s2 is Element of the carrier' of IIG
[s2, the carrier of IIG] is set
the_result_sort_of s2 is Element of the carrier of IIG
InnerVertices IIG is non empty Element of bool the carrier of IIG
Cs1 is Relation-like NAT -defined Function-like finite countable FinSequence-like FinSubsequence-like DTree-yielding set
[(action_at iv), the carrier of IIG] -tree Cs1 is Relation-like Function-like DecoratedTree-like set
{ b₁ where b₁ is Element of the carrier of IIG : b₁ is with_const_op } is set
Cs2 is Element of the carrier of IIG
Cs2 is Element of the carrier' of IIG
the Arity of IIG . Cs2 is Relation-like NAT -defined Function-like finite countable FinSequence-like FinSubsequence-like Element of the carrier of IIG *
the ResultSort of IIG . Cs2 is Element of the carrier of IIG
the_result_sort_of Cs2 is Element of the carrier of IIG
dom the Arity of IIG is set
Args ((action_at iv),(FreeEnv SCS)) is functional non empty Element of rng ( the Sorts of (FreeEnv SCS) #)
the Sorts of (FreeEnv SCS) # is Relation-like the carrier of IIG * -defined Function-like non empty total set
rng ( the Sorts of (FreeEnv SCS) #) is non empty set
the Arity of IIG * ( the Sorts of (FreeEnv SCS) #) is Relation-like the carrier' of IIG -defined Function-like non empty total set
( the Arity of IIG * ( the Sorts of (FreeEnv SCS) #)) . (action_at iv) 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 V21() V22() V23() V25() V26() V27() finite finite-yielding V32() cardinal {} -element Cardinal-yielding countable Function-yielding V42() FinSequence-like FinSubsequence-like FinSequence-membered constituted-Trees constituted-FinTrees constituted-DTrees Tree-yielding FinTree-yielding DTree-yielding V133() V134() ext-real V150() V151() V152() V153() V154() V155() V156() V163() V164() V165() V166() FinSequence of the carrier of IIG
( the Sorts of (FreeEnv SCS) #) . (<*> the carrier of IIG) is set
x is Relation-like Function-like Element of Args ((action_at iv),(FreeEnv SCS))
(IIG,SCS,InpFs) # x is Relation-like Function-like Element of Args ((action_at iv),(FreeEnv SCS))
( the Arity of IIG * ((FreeSort the Sorts of SCS) #)) . Cs2 is set
Sym ((action_at iv), the Sorts of SCS) is Element of K355((DTConMSA the Sorts of SCS))
K355((DTConMSA the Sorts of SCS)) is non empty Element of bool the carrier of (DTConMSA the Sorts of SCS)
bool the carrier of (DTConMSA the Sorts of SCS) is set
x9 is Relation-like NAT -defined FinTrees the carrier of (DTConMSA the Sorts of SCS) -valued Function-like finite countable Function-yielding V42() FinSequence-like FinSubsequence-like FinSequence of TS (DTConMSA the Sorts of SCS)
roots x9 is Relation-like NAT -defined the carrier of (DTConMSA the Sorts of SCS) -valued Function-like finite countable FinSequence-like FinSubsequence-like FinSequence of the carrier of (DTConMSA the Sorts of SCS)
the_result_sort_of (action_at iv) is Element of the carrier of IIG
len Cs1 is V21() V22() V23() V27() finite cardinal countable V133() V134() ext-real V148() V149() V150() V151() V152() V153() V154() V155() V163() V164() V165() Element of NAT
the_arity_of (action_at iv) is Relation-like NAT -defined the carrier of IIG -valued Function-like finite countable FinSequence-like FinSubsequence-like Element of the carrier of IIG *
len (the_arity_of (action_at iv)) is V21() V22() V23() V27() finite cardinal countable V133() V134() ext-real V148() V149() V150() V151() V152() V153() V154() V155() V163() V164() V165() Element of NAT
len {} is Relation-like non-empty empty-yielding NAT -defined Function-like one-to-one constant functional empty V21() V22() V23() V25() V26() V27() finite finite-yielding V32() cardinal {} -element Cardinal-yielding countable Function-yielding V42() FinSequence-like FinSubsequence-like FinSequence-membered constituted-Trees constituted-FinTrees constituted-DTrees Tree-yielding FinTree-yielding DTree-yielding V133() V134() ext-real V148() V149() V150() V151() V152() V153() V154() V155() V156() V163() V164() V165() V166() Element of NAT
Result ((action_at iv),(FreeEnv SCS)) is non empty Element of rng the Sorts of (FreeEnv SCS)
rng the Sorts of (FreeEnv SCS) is non empty set
Den ((action_at iv),(FreeEnv SCS)) is Relation-like Args ((action_at iv),(FreeEnv SCS)) -defined Result ((action_at iv),(FreeEnv SCS)) -valued Function-like V18( Args ((action_at iv),(FreeEnv SCS)), Result ((action_at iv),(FreeEnv SCS))) Element of bool [:(Args ((action_at iv),(FreeEnv SCS))),(Result ((action_at iv),(FreeEnv SCS))):]
[:(Args ((action_at iv),(FreeEnv SCS))),(Result ((action_at iv),(FreeEnv SCS))):] is Relation-like set
bool [:(Args ((action_at iv),(FreeEnv SCS))),(Result ((action_at iv),(FreeEnv SCS))):] is set
(Den ((action_at iv),(FreeEnv SCS))) . x is Element of Result ((action_at iv),(FreeEnv SCS))
(FreeOper the Sorts of SCS) . (action_at iv) is Relation-like ( the Arity of IIG * ((FreeSort the Sorts of SCS) #)) . (action_at iv) -defined ( the ResultSort of IIG * (FreeSort the Sorts of SCS)) . (action_at iv) -valued Function-like V18(( the Arity of IIG * ((FreeSort the Sorts of SCS) #)) . (action_at iv),( the ResultSort of IIG * (FreeSort the Sorts of SCS)) . (action_at iv)) Element of bool [:(( the Arity of IIG * ((FreeSort the Sorts of SCS) #)) . (action_at iv)),(( the ResultSort of IIG * (FreeSort the Sorts of SCS)) . (action_at iv)):]
( the Arity of IIG * ((FreeSort the Sorts of SCS) #)) . (action_at iv) is set
( the ResultSort of IIG * (FreeSort the Sorts of SCS)) . (action_at iv) is non empty set
[:(( the Arity of IIG * ((FreeSort the Sorts of SCS) #)) . (action_at iv)),(( the ResultSort of IIG * (FreeSort the Sorts of SCS)) . (action_at iv)):] is Relation-like set
bool [:(( the Arity of IIG * ((FreeSort the Sorts of SCS) #)) . (action_at iv)),(( the ResultSort of IIG * (FreeSort the Sorts of SCS)) . (action_at iv)):] is set
((FreeOper the Sorts of SCS) . (action_at iv)) . x is set
DenOp ((action_at iv), the Sorts of SCS) is Relation-like ( the Arity of IIG * ((FreeSort the Sorts of SCS) #)) . (action_at iv) -defined ( the ResultSort of IIG * (FreeSort the Sorts of SCS)) . (action_at iv) -valued Function-like V18(( the Arity of IIG * ((FreeSort the Sorts of SCS) #)) . (action_at iv),( the ResultSort of IIG * (FreeSort the Sorts of SCS)) . (action_at iv)) Element of bool [:(( the Arity of IIG * ((FreeSort the Sorts of SCS) #)) . (action_at iv)),(( the ResultSort of IIG * (FreeSort the Sorts of SCS)) . (action_at iv)):]
(DenOp ((action_at iv), the Sorts of SCS)) . x is set
(Sym ((action_at iv), the Sorts of SCS)) -tree x9 is Relation-like the carrier of (DTConMSA the Sorts of SCS) -valued Function-like finite countable DecoratedTree-like Element of FinTrees the carrier of (DTConMSA the Sorts of SCS)
[(action_at iv), the carrier of IIG] -tree x9 is Relation-like Function-like DecoratedTree-like set
dSCS . {} is set
s2 is Relation-like Function-like Element of TS (DTConMSA the Sorts of SCS)
Cs1 is set
[Cs1,iv] is set
root-tree [Cs1,iv] is Relation-like Function-like finite countable DecoratedTree-like set
Cs2 is Element of the carrier' of IIG
[Cs2, the carrier of IIG] is set
s2 . {} is set
the_result_sort_of Cs2 is Element of the carrier of IIG
IIG is non empty non void V56() Circuit-like monotonic 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 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
K539( the carrier of IIG, the ResultSort of IIG) is Element of bool the carrier of IIG
the carrier of IIG \ K539( the carrier of IIG, the ResultSort of IIG) is Element of bool the carrier of IIG
SCS is non-empty finitely-generated finite-yielding MSAlgebra over IIG
FreeEnv SCS is strict non-empty free MSAlgebra over IIG
the Sorts of SCS is Relation-like non-empty non empty-yielding the carrier of IIG -defined Function-like non empty total set
FreeMSA the Sorts of SCS is strict non-empty MSAlgebra over IIG
the Sorts of (FreeEnv SCS) is Relation-like non-empty non empty-yielding the carrier of IIG -defined Function-like non empty total set
InpFs is Relation-like InputVertices IIG -defined Function-like total InputValues of SCS
(IIG,SCS,InpFs) is Relation-like the carrier of IIG -defined Function-like non empty total Function-yielding V42() ManySortedFunction of the Sorts of (FreeEnv SCS), the Sorts of (FreeEnv SCS)
iv is Element of the carrier of IIG
the Sorts of (FreeEnv SCS) . iv is non empty finite countable set
(IIG,SCS,InpFs) . iv is Relation-like the Sorts of (FreeEnv SCS) . iv -defined the Sorts of (FreeEnv SCS) . iv -valued Function-like V18( the Sorts of (FreeEnv SCS) . iv, the Sorts of (FreeEnv SCS) . iv) finite countable Element of bool [:( the Sorts of (FreeEnv SCS) . iv),( the Sorts of (FreeEnv SCS) . iv):]
[:( the Sorts of (FreeEnv SCS) . iv),( the Sorts of (FreeEnv SCS) . iv):] is Relation-like finite countable set
bool [:( the Sorts of (FreeEnv SCS) . iv),( the Sorts of (FreeEnv SCS) . iv):] is finite V32() countable set
dSCS is Relation-like Function-like non empty finite countable DecoratedTree-like Element of the Sorts of (FreeEnv SCS) . iv
s1 is Relation-like Function-like non empty finite countable DecoratedTree-like Element of the Sorts of (FreeEnv SCS) . iv
((IIG,SCS,InpFs) . iv) . dSCS is Relation-like Function-like non empty finite countable DecoratedTree-like Element of the Sorts of (FreeEnv SCS) . iv
s2 is Relation-like Function-like DecoratedTree-like set
Cs1 is Relation-like Function-like DecoratedTree-like set
dom s2 is set
dom Cs1 is set
depth (iv,SCS) is V21() V22() V23() V27() finite cardinal countable V133() V134() ext-real set
x9 is V21() V22() V23() V27() finite cardinal countable V133() V134() ext-real V148() V149() V150() V151() V152() V153() V154() V155() V163() V164() V165() Element of NAT
FreeSort the Sorts of SCS is Relation-like non-empty non empty-yielding the carrier of IIG -defined Function-like non empty total set
FreeOper the Sorts of SCS is Relation-like the carrier' of IIG -defined Function-like non empty total Function-yielding V42() ManySortedFunction of the Arity of IIG * ((FreeSort the Sorts of SCS) #), the ResultSort of IIG * (FreeSort the Sorts of SCS)
the Arity of IIG is Relation-like the carrier' of IIG -defined the carrier of IIG * -valued Function-like V18( the carrier' of IIG, the carrier of IIG * ) Function-yielding V42() Element of bool [: the carrier' of IIG,( the carrier of IIG *):]
the carrier of IIG * is functional non empty FinSequence-membered M8( 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 SCS) # is Relation-like the carrier of IIG * -defined Function-like non empty total set
the Arity of IIG * ((FreeSort the Sorts of SCS) #) is Relation-like the carrier' of IIG -defined Function-like non empty total set
the ResultSort of IIG * (FreeSort the Sorts of SCS) is Relation-like non-empty non empty-yielding the carrier' of IIG -defined Function-like non empty total set
MSAlgebra(# (FreeSort the Sorts of SCS),(FreeOper the Sorts of SCS) #) is strict MSAlgebra over IIG
InnerVertices 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
((InnerVertices IIG) \ (SortsWithConstants IIG)) \/ (SortsWithConstants IIG) is Element of bool the carrier of IIG
p is V21() V22() V23() V27() finite cardinal countable V133() V134() ext-real V148() V149() V150() V151() V152() V153() V154() V155() V163() V164() V165() Element of NAT
p + 1 is V21() V22() V23() V27() finite cardinal countable V133() V134() ext-real V148() V149() V150() V151() V152() V153() V154() V155() V163() V164() V165() Element of NAT
ods is Element of the carrier of IIG
the Sorts of (FreeEnv SCS) . ods is non empty finite countable set
depth (ods,SCS) is V21() V22() V23() V27() finite cardinal countable V133() V134() ext-real set
(IIG,SCS,InpFs) . ods is Relation-like the Sorts of (FreeEnv SCS) . ods -defined the Sorts of (FreeEnv SCS) . ods -valued Function-like V18( the Sorts of (FreeEnv SCS) . ods, the Sorts of (FreeEnv SCS) . ods) finite countable Element of bool [:( the Sorts of (FreeEnv SCS) . ods),( the Sorts of (FreeEnv SCS) . ods):]
[:( the Sorts of (FreeEnv SCS) . ods),( the Sorts of (FreeEnv SCS) . ods):] is Relation-like finite countable set
bool [:( the Sorts of (FreeEnv SCS) . ods),( the Sorts of (FreeEnv SCS) . ods):] is finite V32() countable set
p is Relation-like Function-like non empty finite countable DecoratedTree-like Element of the Sorts of (FreeEnv SCS) . ods
p9 is Relation-like Function-like non empty finite countable DecoratedTree-like Element of the Sorts of (FreeEnv SCS) . ods
((IIG,SCS,InpFs) . ods) . p is Relation-like Function-like non empty finite countable DecoratedTree-like Element of the Sorts of (FreeEnv SCS) . ods
Fp is Relation-like Function-like DecoratedTree-like set
x is Relation-like Function-like DecoratedTree-like set
dom Fp is set
dom x is set
FreeSort ( the Sorts of SCS,ods) is functional non empty constituted-DTrees Element of bool (TS (DTConMSA the Sorts of SCS))
DTConMSA the Sorts of SCS is non empty strict with_terminals with_nonterminals with_useful_nonterminals L13()
TS (DTConMSA the Sorts of SCS) is functional constituted-DTrees Element of bool (FinTrees the carrier of (DTConMSA the Sorts of SCS))
the carrier of (DTConMSA the Sorts of SCS) is non empty set
FinTrees the carrier of (DTConMSA the Sorts of SCS) is functional non empty constituted-DTrees DTree-set of the carrier of (DTConMSA the Sorts of SCS)
bool (FinTrees the carrier of (DTConMSA the Sorts of SCS)) is set
bool (TS (DTConMSA the Sorts of SCS)) is set
the Sorts of SCS . ods is non empty set
{ b₁ where b₁ is Relation-like Function-like Element of TS (DTConMSA the Sorts of SCS) : ( ex b₂ being set st
( b₂ in the Sorts of SCS . ods & b₁ = root-tree [b₂,ods] ) or ex b₂ being Element of the carrier' of IIG st
( [b₂, the carrier of IIG] = b₁ . {} & the_result_sort_of b₂ = ods ) ) } is set
(InputVertices IIG) \/ (InnerVertices IIG) is non empty Element of bool the carrier of IIG
(FreeSort the Sorts of SCS) . ods is non empty set
v1 is Relation-like Function-like Element of TS (DTConMSA the Sorts of SCS)
v1 . {} is set
((IIG,SCS,InpFs) . ods) . v1 is set
InpFs . ods is set
[(InpFs . ods),ods] is set
root-tree [(InpFs . ods),ods] is Relation-like Function-like finite countable DecoratedTree-like set
x9 is set
[x9,ods] is set
root-tree [x9,ods] is Relation-like Function-like finite countable DecoratedTree-like set
E1 is Element of the carrier' of IIG
[E1, the carrier of IIG] is set
the_result_sort_of E1 is Element of the carrier of IIG
x9 is set
[x9,ods] is set
root-tree [x9,ods] is Relation-like Function-like finite countable DecoratedTree-like set
E1 is Element of the carrier' of IIG
[E1, the carrier of IIG] is set
the_result_sort_of E1 is Element of the carrier of IIG
x9 is set
[x9,ods] is set
root-tree [x9,ods] is Relation-like Function-like finite countable DecoratedTree-like set
((IIG,SCS,InpFs) . ods) . v1 is set
action_at ods is Element of the carrier' of IIG
[(action_at ods), the carrier of IIG] is set
root-tree [(action_at ods), the carrier of IIG] is Relation-like Function-like finite countable DecoratedTree-like set
x9 is set
[x9,ods] is set
root-tree [x9,ods] is Relation-like Function-like finite countable DecoratedTree-like set
x9 is Element of the carrier' of IIG
[x9, the carrier of IIG] is set
the_result_sort_of x9 is Element of the carrier of IIG
x9 is Element of the carrier' of IIG
[x9, the carrier of IIG] is set
the_result_sort_of x9 is Element of the carrier of IIG
action_at ods is Element of the carrier' of IIG
[(action_at ods), the carrier of IIG] is set
E1 is Relation-like NAT -defined Function-like finite countable FinSequence-like FinSubsequence-like DTree-yielding set
[(action_at ods), the carrier of IIG] -tree E1 is Relation-like Function-like DecoratedTree-like set
the_arity_of (action_at ods) is Relation-like NAT -defined the carrier of IIG -valued Function-like finite countable FinSequence-like FinSubsequence-like Element of the carrier of IIG *
len E1 is V21() V22() V23() V27() finite cardinal countable V133() V134() ext-real V148() V149() V150() V151() V152() V153() V154() V155() V163() V164() V165() Element of NAT
E2 is Relation-like NAT -defined Function-like finite countable FinSequence-like FinSubsequence-like set
len E2 is V21() V22() V23() V27() finite cardinal countable V133() V134() ext-real V148() V149() V150() V151() V152() V153() V154() V155() V163() V164() V165() Element of NAT
dom E2 is finite countable V150() V151() V152() V153() V154() V155() V163() V164() V165() Element of bool NAT
dom E1 is finite countable V150() V151() V152() V153() V154() V155() V163() V164() V165() Element of bool NAT
len (the_arity_of (action_at ods)) is V21() V22() V23() V27() finite cardinal countable V133() V134() ext-real V148() V149() V150() V151() V152() V153() V154() V155() V163() V164() V165() Element of NAT
dom (the_arity_of (action_at ods)) is finite countable V150() V151() V152() V153() V154() V155() V163() V164() V165() Element of bool NAT
It1 is set
It2 is V21() V22() V23() V27() finite cardinal countable V133() V134() ext-real V148() V149() V150() V151() V152() V153() V154() V155() V163() V164() V165() Element of NAT
(the_arity_of (action_at ods)) /. It2 is Element of the carrier of IIG
the_arity_of x9 is Relation-like NAT -defined the carrier of IIG -valued Function-like finite countable FinSequence-like FinSubsequence-like Element of the carrier of IIG *
(the_arity_of x9) . It2 is set
the Sorts of (FreeEnv SCS) . ((the_arity_of (action_at ods)) /. It2) is non empty finite countable set
E1 . It2 is set
[:( the Sorts of (FreeEnv SCS) . ((the_arity_of (action_at ods)) /. It2)),( the Sorts of (FreeEnv SCS) . ((the_arity_of (action_at ods)) /. It2)):] is Relation-like finite countable set
bool [:( the Sorts of (FreeEnv SCS) . ((the_arity_of (action_at ods)) /. It2)),( the Sorts of (FreeEnv SCS) . ((the_arity_of (action_at ods)) /. It2)):] is finite V32() countable set
(IIG,SCS,InpFs) . ((the_arity_of (action_at ods)) /. It2) is Relation-like the Sorts of (FreeEnv SCS) . ((the_arity_of (action_at ods)) /. It2) -defined the Sorts of (FreeEnv SCS) . ((the_arity_of (action_at ods)) /. It2) -valued Function-like V18( the Sorts of (FreeEnv SCS) . ((the_arity_of (action_at ods)) /. It2), the Sorts of (FreeEnv SCS) . ((the_arity_of (action_at ods)) /. It2)) finite countable Element of bool [:( the Sorts of (FreeEnv SCS) . ((the_arity_of (action_at ods)) /. It2)),( the Sorts of (FreeEnv SCS) . ((the_arity_of (action_at ods)) /. It2)):]
E2 . It2 is set
ee is Relation-like the Sorts of (FreeEnv SCS) . ((the_arity_of (action_at ods)) /. It2) -defined the Sorts of (FreeEnv SCS) . ((the_arity_of (action_at ods)) /. It2) -valued Function-like V18( the Sorts of (FreeEnv SCS) . ((the_arity_of (action_at ods)) /. It2), the Sorts of (FreeEnv SCS) . ((the_arity_of (action_at ods)) /. It2)) finite countable Element of bool [:( the Sorts of (FreeEnv SCS) . ((the_arity_of (action_at ods)) /. It2)),( the Sorts of (FreeEnv SCS) . ((the_arity_of (action_at ods)) /. It2)):]
fv1 is Relation-like Function-like non empty finite countable DecoratedTree-like Element of the Sorts of (FreeEnv SCS) . ((the_arity_of (action_at ods)) /. It2)
ee . fv1 is Relation-like Function-like non empty finite countable DecoratedTree-like Element of the Sorts of (FreeEnv SCS) . ((the_arity_of (action_at ods)) /. It2)
E2 . It1 is set
It1 is V21() V22() V23() V27() finite cardinal countable V133() V134() ext-real V148() V149() V150() V151() V152() V153() V154() V155() V163() V164() V165() Element of NAT
E2 . It1 is set
(the_arity_of (action_at ods)) /. It1 is Element of the carrier of IIG
(IIG,SCS,InpFs) . ((the_arity_of (action_at ods)) /. It1) is Relation-like the Sorts of (FreeEnv SCS) . ((the_arity_of (action_at ods)) /. It1) -defined the Sorts of (FreeEnv SCS) . ((the_arity_of (action_at ods)) /. It1) -valued Function-like V18( the Sorts of (FreeEnv SCS) . ((the_arity_of (action_at ods)) /. It1), the Sorts of (FreeEnv SCS) . ((the_arity_of (action_at ods)) /. It1)) finite countable Element of bool [:( the Sorts of (FreeEnv SCS) . ((the_arity_of (action_at ods)) /. It1)),( the Sorts of (FreeEnv SCS) . ((the_arity_of (action_at ods)) /. It1)):]
the Sorts of (FreeEnv SCS) . ((the_arity_of (action_at ods)) /. It1) is non empty finite countable set
[:( the Sorts of (FreeEnv SCS) . ((the_arity_of (action_at ods)) /. It1)),( the Sorts of (FreeEnv SCS) . ((the_arity_of (action_at ods)) /. It1)):] is Relation-like finite countable set
bool [:( the Sorts of (FreeEnv SCS) . ((the_arity_of (action_at ods)) /. It1)),( the Sorts of (FreeEnv SCS) . ((the_arity_of (action_at ods)) /. It1)):] is finite V32() countable set
E1 . It1 is set
((IIG,SCS,InpFs) . ((the_arity_of (action_at ods)) /. It1)) . (E1 . It1) is set
It1 is Relation-like NAT -defined Function-like finite countable FinSequence-like FinSubsequence-like DTree-yielding set
[(action_at ods), the carrier of IIG] -tree It1 is Relation-like Function-like DecoratedTree-like set
doms E1 is Relation-like NAT -defined Function-like finite countable FinSequence-like FinSubsequence-like Tree-yielding set
dom (doms E1) is finite countable V150() V151() V152() V153() V154() V155() V163() V164() V165() Element of bool NAT
It2 is V21() V22() V23() V27() finite cardinal countable V133() V134() ext-real set
(the_arity_of (action_at ods)) /. It2 is Element of the carrier of IIG
the Sorts of (FreeEnv SCS) . ((the_arity_of (action_at ods)) /. It2) is non empty finite countable set
[:( the Sorts of (FreeEnv SCS) . ((the_arity_of (action_at ods)) /. It2)),( the Sorts of (FreeEnv SCS) . ((the_arity_of (action_at ods)) /. It2)):] is Relation-like finite countable set
bool [:( the Sorts of (FreeEnv SCS) . ((the_arity_of (action_at ods)) /. It2)),( the Sorts of (FreeEnv SCS) . ((the_arity_of (action_at ods)) /. It2)):] is finite V32() countable set
(IIG,SCS,InpFs) . ((the_arity_of (action_at ods)) /. It2) is Relation-like the Sorts of (FreeEnv SCS) . ((the_arity_of (action_at ods)) /. It2) -defined the Sorts of (FreeEnv SCS) . ((the_arity_of (action_at ods)) /. It2) -valued Function-like V18( the Sorts of (FreeEnv SCS) . ((the_arity_of (action_at ods)) /. It2), the Sorts of (FreeEnv SCS) . ((the_arity_of (action_at ods)) /. It2)) finite countable Element of bool [:( the Sorts of (FreeEnv SCS) . ((the_arity_of (action_at ods)) /. It2)),( the Sorts of (FreeEnv SCS) . ((the_arity_of (action_at ods)) /. It2)):]
(the_arity_of x9) . It2 is set
E1 . It2 is set
It1 . It2 is set
fv1 is Relation-like the Sorts of (FreeEnv SCS) . ((the_arity_of (action_at ods)) /. It2) -defined the Sorts of (FreeEnv SCS) . ((the_arity_of (action_at ods)) /. It2) -valued Function-like V18( the Sorts of (FreeEnv SCS) . ((the_arity_of (action_at ods)) /. It2), the Sorts of (FreeEnv SCS) . ((the_arity_of (action_at ods)) /. It2)) finite countable Element of bool [:( the Sorts of (FreeEnv SCS) . ((the_arity_of (action_at ods)) /. It2)),( the Sorts of (FreeEnv SCS) . ((the_arity_of (action_at ods)) /. It2)):]
ee is Relation-like Function-like non empty finite countable DecoratedTree-like Element of the Sorts of (FreeEnv SCS) . ((the_arity_of (action_at ods)) /. It2)
fv1 . ee is Relation-like Function-like non empty finite countable DecoratedTree-like Element of the Sorts of (FreeEnv SCS) . ((the_arity_of (action_at ods)) /. It2)
rng (the_arity_of (action_at ods)) is finite countable set
depth (((the_arity_of (action_at ods)) /. It2),SCS) is V21() V22() V23() V27() finite cardinal countable V133() V134() ext-real set
((IIG,SCS,InpFs) . ((the_arity_of (action_at ods)) /. It2)) . (E1 . It2) is set
dom ee is non empty finite countable set
ee1 is Relation-like Function-like non empty finite countable DecoratedTree-like Element of the Sorts of (FreeEnv SCS) . ((the_arity_of (action_at ods)) /. It2)
dom ee1 is non empty finite countable set
(doms E1) . It2 is set
doms It1 is Relation-like NAT -defined Function-like finite countable FinSequence-like FinSubsequence-like Tree-yielding set
(doms It1) . It2 is set
dom It1 is finite countable V150() V151() V152() V153() V154() V155() V163() V164() V165() Element of bool NAT
dom (doms It1) is finite countable V150() V151() V152() V153() V154() V155() V163() V164() V165() Element of bool NAT
tree (doms It1) is non empty V108() set
x9 is set
[x9,ods] is set
root-tree [x9,ods] is Relation-like Function-like finite countable DecoratedTree-like set
E1 is Element of the carrier' of IIG
[E1, the carrier of IIG] is set
the_result_sort_of E1 is Element of the carrier of IIG
p is Element of the carrier of IIG
the Sorts of (FreeEnv SCS) . p is non empty finite countable set
depth (p,SCS) is V21() V22() V23() V27() finite cardinal countable V133() V134() ext-real set
(IIG,SCS,InpFs) . p is Relation-like the Sorts of (FreeEnv SCS) . p -defined the Sorts of (FreeEnv SCS) . p -valued Function-like V18( the Sorts of (FreeEnv SCS) . p, the Sorts of (FreeEnv SCS) . p) finite countable Element of bool [:( the Sorts of (FreeEnv SCS) . p),( the Sorts of (FreeEnv SCS) . p):]
[:( the Sorts of (FreeEnv SCS) . p),( the Sorts of (FreeEnv SCS) . p):] is Relation-like finite countable set
bool [:( the Sorts of (FreeEnv SCS) . p),( the Sorts of (FreeEnv SCS) . p):] is finite V32() countable set
ods is Relation-like Function-like non empty finite countable DecoratedTree-like Element of the Sorts of (FreeEnv SCS) . p
p is Relation-like Function-like non empty finite countable DecoratedTree-like Element of the Sorts of (FreeEnv SCS) . p
((IIG,SCS,InpFs) . p) . ods is Relation-like Function-like non empty finite countable DecoratedTree-like Element of the Sorts of (FreeEnv SCS) . p
p9 is Relation-like Function-like DecoratedTree-like set
Fp is Relation-like Function-like DecoratedTree-like set
dom p9 is set
dom Fp is set
FreeSort ( the Sorts of SCS,p) is functional non empty constituted-DTrees Element of bool (TS (DTConMSA the Sorts of SCS))
DTConMSA the Sorts of SCS is non empty strict with_terminals with_nonterminals with_useful_nonterminals L13()
TS (DTConMSA the Sorts of SCS) is functional constituted-DTrees Element of bool (FinTrees the carrier of (DTConMSA the Sorts of SCS))
the carrier of (DTConMSA the Sorts of SCS) is non empty set
FinTrees the carrier of (DTConMSA the Sorts of SCS) is functional non empty constituted-DTrees DTree-set of the carrier of (DTConMSA the Sorts of SCS)
bool (FinTrees the carrier of (DTConMSA the Sorts of SCS)) is set
bool (TS (DTConMSA the Sorts of SCS)) is set
the Sorts of SCS . p is non empty set
{ b₁ where b₁ is Relation-like Function-like Element of TS (DTConMSA the Sorts of SCS) : ( ex b₂ being set st
( b₂ in the Sorts of SCS . p & b₁ = root-tree [b₂,p] ) or ex b₂ being Element of the carrier' of IIG st
( [b₂, the carrier of IIG] = b₁ . {} & the_result_sort_of b₂ = p ) ) } is set
(FreeSort the Sorts of SCS) . p is non empty set
x is Relation-like Function-like Element of TS (DTConMSA the Sorts of SCS)
x . {} is set
((IIG,SCS,InpFs) . p) . x is set
InpFs . p is set
[(InpFs . p),p] is set
root-tree [(InpFs . p),p] is Relation-like Function-like finite countable DecoratedTree-like set
v1 is set
[v1,p] is set
root-tree [v1,p] is Relation-like Function-like finite countable DecoratedTree-like set
x9 is Element of the carrier' of IIG
[x9, the carrier of IIG] is set
the_result_sort_of x9 is Element of the carrier of IIG
v1 is set
[v1,p] is set
root-tree [v1,p] is Relation-like Function-like finite countable DecoratedTree-like set
x9 is Element of the carrier' of IIG
[x9, the carrier of IIG] is set
the_result_sort_of x9 is Element of the carrier of IIG
SortsWithConstants IIG is Element of bool the carrier of IIG
((IIG,SCS,InpFs) . p) . x is set
action_at p is Element of the carrier' of IIG
[(action_at p), the carrier of IIG] is set
root-tree [(action_at p), the carrier of IIG] is Relation-like Function-like finite countable DecoratedTree-like set
v1 is set
[v1,p] is set
root-tree [v1,p] is Relation-like Function-like finite countable DecoratedTree-like set
SortsWithConstants IIG is Element of bool the carrier of IIG
((IIG,SCS,InpFs) . p) . x is set
action_at p is Element of the carrier' of IIG
[(action_at p), the carrier of IIG] is set
root-tree [(action_at p), the carrier of IIG] is Relation-like Function-like finite countable DecoratedTree-like set
v1 is Element of the carrier' of IIG
[v1, the carrier of IIG] is set
the_result_sort_of v1 is Element of the carrier of IIG
v1 is Element of the carrier' of IIG
[v1, the carrier of IIG] is set
the_result_sort_of v1 is Element of the carrier of IIG
InnerVertices IIG is non empty Element of bool the carrier of IIG
x9 is Relation-like NAT -defined Function-like finite countable FinSequence-like FinSubsequence-like DTree-yielding set
[(action_at p), the carrier of IIG] -tree x9 is Relation-like Function-like DecoratedTree-like set
{ b₁ where b₁ is Element of the carrier of IIG : b₁ is with_const_op } is set
E1 is Element of the carrier of IIG
E1 is Element of the carrier' of IIG
the Arity of IIG . E1 is Relation-like NAT -defined Function-like finite countable FinSequence-like FinSubsequence-like Element of the carrier of IIG *
the ResultSort of IIG . E1 is Element of the carrier of IIG
the_result_sort_of E1 is Element of the carrier of IIG
len x9 is V21() V22() V23() V27() finite cardinal countable V133() V134() ext-real V148() V149() V150() V151() V152() V153() V154() V155() V163() V164() V165() Element of NAT
the_arity_of E1 is Relation-like NAT -defined the carrier of IIG -valued Function-like finite countable FinSequence-like FinSubsequence-like Element of the carrier of IIG *
len (the_arity_of E1) is V21() V22() V23() V27() finite cardinal countable V133() V134() ext-real V148() V149() V150() V151() V152() V153() V154() V155() V163() V164() V165() Element of NAT
len {} is Relation-like non-empty empty-yielding NAT -defined Function-like one-to-one constant functional empty V21() V22() V23() V25() V26() V27() finite finite-yielding V32() cardinal {} -element Cardinal-yielding countable Function-yielding V42() FinSequence-like FinSubsequence-like FinSequence-membered constituted-Trees constituted-FinTrees constituted-DTrees Tree-yielding FinTree-yielding DTree-yielding V133() V134() ext-real V148() V149() V150() V151() V152() V153() V154() V155() V156() V163() V164() V165() V166() Element of NAT
[E1, the carrier of IIG] is set
root-tree [E1, the carrier of IIG] is Relation-like Function-like finite countable DecoratedTree-like set
SortsWithConstants IIG is Element of bool the carrier of IIG
v1 is set
[v1,p] is set
root-tree [v1,p] is Relation-like Function-like finite countable DecoratedTree-like set
x9 is Element of the carrier' of IIG
[x9, the carrier of IIG] is set
the_result_sort_of x9 is Element of the carrier of IIG
IIG is non empty non void V56() Circuit-like monotonic 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 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
K539( the carrier of IIG, the ResultSort of IIG) is Element of bool the carrier of IIG
the carrier of IIG \ K539( the carrier of IIG, the ResultSort of IIG) is Element of bool the carrier of IIG
SCS is non-empty finitely-generated finite-yielding MSAlgebra over IIG
FreeEnv SCS is strict non-empty free MSAlgebra over IIG
the Sorts of SCS is Relation-like non-empty non empty-yielding the carrier of IIG -defined Function-like non empty total set
FreeMSA the Sorts of SCS is strict non-empty MSAlgebra over IIG
the Sorts of (FreeEnv SCS) is Relation-like non-empty non empty-yielding the carrier of IIG -defined Function-like non empty total set
InpFs is Relation-like InputVertices IIG -defined Function-like total InputValues of SCS
(IIG,SCS,InpFs) is Relation-like the carrier of IIG -defined Function-like non empty total Function-yielding V42() ManySortedFunction of the Sorts of (FreeEnv SCS), the Sorts of (FreeEnv SCS)
iv is Element of the carrier of IIG
the Sorts of (FreeEnv SCS) . iv is non empty finite countable set
(IIG,SCS,InpFs) . iv is Relation-like the Sorts of (FreeEnv SCS) . iv -defined the Sorts of (FreeEnv SCS) . iv -valued Function-like V18( the Sorts of (FreeEnv SCS) . iv, the Sorts of (FreeEnv SCS) . iv) finite countable Element of bool [:( the Sorts of (FreeEnv SCS) . iv),( the Sorts of (FreeEnv SCS) . iv):]
[:( the Sorts of (FreeEnv SCS) . iv),( the Sorts of (FreeEnv SCS) . iv):] is Relation-like finite countable set
bool [:( the Sorts of (FreeEnv SCS) . iv),( the Sorts of (FreeEnv SCS) . iv):] is finite V32() countable set
s1 is Relation-like Function-like non empty finite countable DecoratedTree-like Element of the Sorts of (FreeEnv SCS) . iv
dSCS is Relation-like Function-like non empty finite countable DecoratedTree-like Element of the Sorts of (FreeEnv SCS) . iv
((IIG,SCS,InpFs) . iv) . dSCS is Relation-like Function-like non empty finite countable DecoratedTree-like Element of the Sorts of (FreeEnv SCS) . iv
card dSCS is non empty V21() V22() V23() V27() finite cardinal countable V133() V134() ext-real V148() V149() V150() V151() V152() V153() V154() V155() V161() V162() V163() V164() V165() Element of NAT
card s1 is non empty V21() V22() V23() V27() finite cardinal countable V133() V134() ext-real V148() V149() V150() V151() V152() V153() V154() V155() V161() V162() V163() V164() V165() Element of NAT
dom dSCS is non empty finite countable set
dom s1 is non empty finite countable set
card (dom s1) is non empty V21() V22() V23() V27() finite cardinal countable V133() V134() ext-real V148() V149() V150() V151() V152() V153() V154() V155() V161() V162() V163() V164() V165() Element of NAT
IIG is non empty non void V56() 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 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
K539( the carrier of IIG, the ResultSort of IIG) is Element of bool the carrier of IIG
the carrier of IIG \ K539( the carrier of IIG, the ResultSort of IIG) is Element of bool the carrier of IIG
SCS is non-empty finitely-generated finite-yielding MSAlgebra over IIG
FreeEnv SCS is strict non-empty free MSAlgebra over IIG
the Sorts of SCS is Relation-like non-empty non empty-yielding the carrier of IIG -defined Function-like non empty total set
FreeMSA the Sorts of SCS is strict non-empty MSAlgebra over IIG
the Sorts of (FreeEnv SCS) is Relation-like non-empty non empty-yielding the carrier of IIG -defined Function-like non empty total set
InpFs is Element of the carrier of IIG
the Sorts of (FreeEnv SCS) . InpFs is non empty finite countable set
size (InpFs,SCS) is V21() V22() V23() V27() finite cardinal countable V133() V134() ext-real set
iv is Relation-like InputVertices IIG -defined Function-like total InputValues of SCS
(IIG,SCS,iv) is Relation-like the carrier of IIG -defined Function-like non empty total Function-yielding V42() ManySortedFunction of the Sorts of (FreeEnv SCS), the Sorts of (FreeEnv SCS)
(IIG,SCS,iv) . InpFs is Relation-like the Sorts of (FreeEnv SCS) . InpFs -defined the Sorts of (FreeEnv SCS) . InpFs -valued Function-like V18( the Sorts of (FreeEnv SCS) . InpFs, the Sorts of (FreeEnv SCS) . InpFs) finite countable Element of bool [:( the Sorts of (FreeEnv SCS) . InpFs),( the Sorts of (FreeEnv SCS) . InpFs):]
[:( the Sorts of (FreeEnv SCS) . InpFs),( the Sorts of (FreeEnv SCS) . InpFs):] is Relation-like finite countable set
bool [:( the Sorts of (FreeEnv SCS) . InpFs),( the Sorts of (FreeEnv SCS) . InpFs):] is finite V32() countable set
{ (card b₁) where b₁ is Relation-like Function-like non empty finite countable DecoratedTree-like Element of the Sorts of (FreeEnv SCS) . InpFs : verum } is set
s1 is non empty finite countable V150() V151() V152() V153() V154() V155() V161() V162() V163() V164() V165() Element of bool NAT
max s1 is V21() V22() V23() V27() finite cardinal countable V133() V134() ext-real V148() V149() set
s2 is Relation-like Function-like non empty finite countable DecoratedTree-like Element of the Sorts of (FreeEnv SCS) . InpFs
card s2 is non empty V21() V22() V23() V27() finite cardinal countable V133() V134() ext-real V148() V149() V150() V151() V152() V153() V154() V155() V161() V162() V163() V164() V165() Element of NAT
dSCS is non empty set
[:dSCS,dSCS:] is Relation-like set
bool [:dSCS,dSCS:] is set
Cs1 is Relation-like dSCS -defined dSCS -valued Function-like V18(dSCS,dSCS) Element of bool [:dSCS,dSCS:]
Cs2 is Element of dSCS
Cs1 . Cs2 is Element of dSCS
x is Element of dSCS
x9 is Relation-like Function-like non empty finite countable DecoratedTree-like Element of the Sorts of (FreeEnv SCS) . InpFs
((IIG,SCS,iv) . InpFs) . s2 is Relation-like Function-like non empty finite countable DecoratedTree-like Element of the Sorts of (FreeEnv SCS) . InpFs
dSCS is Relation-like Function-like non empty finite countable DecoratedTree-like Element of the Sorts of (FreeEnv SCS) . InpFs
s1 is Relation-like Function-like non empty finite countable DecoratedTree-like Element of the Sorts of (FreeEnv SCS) . InpFs
s2 is V21() V22() V23() V27() finite cardinal countable V133() V134() ext-real set
Cs1 is Element of the carrier of IIG
the Sorts of (FreeEnv SCS) . Cs1 is non empty finite countable set
size (Cs1,SCS) is V21() V22() V23() V27() finite cardinal countable V133() V134() ext-real set
x9 is Relation-like Function-like non empty finite countable DecoratedTree-like Element of the Sorts of (FreeEnv SCS) . Cs1
card x9 is non empty V21() V22() V23() V27() finite cardinal countable V133() V134() ext-real V148() V149() V150() V151() V152() V153() V154() V155() V161() V162() V163() V164() V165() Element of NAT
Cs2 is Relation-like Function-like non empty finite countable DecoratedTree-like Element of the Sorts of (FreeEnv SCS) . Cs1
(IIG,SCS,iv) . Cs1 is Relation-like the Sorts of (FreeEnv SCS) . Cs1 -defined the Sorts of (FreeEnv SCS) . Cs1 -valued Function-like V18( the Sorts of (FreeEnv SCS) . Cs1, the Sorts of (FreeEnv SCS) . Cs1) finite countable Element of bool [:( the Sorts of (FreeEnv SCS) . Cs1),( the Sorts of (FreeEnv SCS) . Cs1):]
[:( the Sorts of (FreeEnv SCS) . Cs1),( the Sorts of (FreeEnv SCS) . Cs1):] is Relation-like finite countable set
bool [:( the Sorts of (FreeEnv SCS) . Cs1),( the Sorts of (FreeEnv SCS) . Cs1):] is finite V32() countable set
((IIG,SCS,iv) . Cs1) . x9 is Relation-like Function-like non empty finite countable DecoratedTree-like Element of the Sorts of (FreeEnv SCS) . Cs1
p is Relation-like Function-like non empty finite countable DecoratedTree-like Element of the Sorts of (FreeEnv SCS) . Cs1
card p is non empty V21() V22() V23() V27() finite cardinal countable V133() V134() ext-real V148() V149() V150() V151() V152() V153() V154() V155() V161() V162() V163() V164() V165() Element of NAT
x is Relation-like Function-like non empty finite countable DecoratedTree-like Element of the Sorts of (FreeEnv SCS) . Cs1
((IIG,SCS,iv) . Cs1) . p is Relation-like Function-like non empty finite countable DecoratedTree-like Element of the Sorts of (FreeEnv SCS) . Cs1
Cs1 is Element of the carrier of IIG
the Sorts of (FreeEnv SCS) . Cs1 is non empty finite countable set
size (Cs1,SCS) is V21() V22() V23() V27() finite cardinal countable V133() V134() ext-real set
Cs2 is Relation-like Function-like non empty finite countable DecoratedTree-like Element of the Sorts of (FreeEnv SCS) . Cs1
(IIG,SCS,iv) . Cs1 is Relation-like the Sorts of (FreeEnv SCS) . Cs1 -defined the Sorts of (FreeEnv SCS) . Cs1 -valued Function-like V18( the Sorts of (FreeEnv SCS) . Cs1, the Sorts of (FreeEnv SCS) . Cs1) finite countable Element of bool [:( the Sorts of (FreeEnv SCS) . Cs1),( the Sorts of (FreeEnv SCS) . Cs1):]
[:( the Sorts of (FreeEnv SCS) . Cs1),( the Sorts of (FreeEnv SCS) . Cs1):] is Relation-like finite countable set
bool [:( the Sorts of (FreeEnv SCS) . Cs1),( the Sorts of (FreeEnv SCS) . Cs1):] is finite V32() countable set
x is Relation-like Function-like non empty finite countable DecoratedTree-like Element of the Sorts of (FreeEnv SCS) . Cs1
x9 is Relation-like Function-like non empty finite countable DecoratedTree-like Element of the Sorts of (FreeEnv SCS) . Cs1
card x9 is non empty V21() V22() V23() V27() finite cardinal countable V133() V134() ext-real V148() V149() V150() V151() V152() V153() V154() V155() V161() V162() V163() V164() V165() Element of NAT
((IIG,SCS,iv) . Cs1) . x9 is Relation-like Function-like non empty finite countable DecoratedTree-like Element of the Sorts of (FreeEnv SCS) . Cs1
x9 is Relation-like Function-like non empty finite countable DecoratedTree-like Element of the Sorts of (FreeEnv SCS) . Cs1
card x9 is non empty V21() V22() V23() V27() finite cardinal countable V133() V134() ext-real V148() V149() V150() V151() V152() V153() V154() V155() V161() V162() V163() V164() V165() Element of NAT
((IIG,SCS,iv) . Cs1) . x9 is Relation-like Function-like non empty finite countable DecoratedTree-like Element of the Sorts of (FreeEnv SCS) . Cs1
p is Relation-like Function-like non empty finite countable DecoratedTree-like Element of the Sorts of (FreeEnv SCS) . Cs1
card p is non empty V21() V22() V23() V27() finite cardinal countable V133() V134() ext-real V148() V149() V150() V151() V152() V153() V154() V155() V161() V162() V163() V164() V165() Element of NAT
((IIG,SCS,iv) . Cs1) . p is Relation-like Function-like non empty finite countable DecoratedTree-like Element of the Sorts of (FreeEnv SCS) . Cs1
p is Relation-like Function-like non empty finite countable DecoratedTree-like Element of the Sorts of (FreeEnv SCS) . Cs1
card p is non empty V21() V22() V23() V27() finite cardinal countable V133() V134() ext-real V148() V149() V150() V151() V152() V153() V154() V155() V161() V162() V163() V164() V165() Element of NAT
((IIG,SCS,iv) . Cs1) . p is Relation-like Function-like non empty finite countable DecoratedTree-like Element of the Sorts of (FreeEnv SCS) . Cs1
the Sorts of SCS . Cs1 is non empty set
iv . Cs1 is set
[(iv . Cs1),Cs1] is set
root-tree [(iv . Cs1),Cs1] is Relation-like Function-like finite countable DecoratedTree-like set
ods is Element of the Sorts of SCS . Cs1
[ods,Cs1] is set
root-tree [ods,Cs1] is Relation-like Function-like finite countable DecoratedTree-like set
ods is Element of the Sorts of SCS . Cs1
[ods,Cs1] is set
root-tree [ods,Cs1] is Relation-like Function-like finite countable DecoratedTree-like set
SortsWithConstants IIG is Element of bool the carrier of IIG
action_at Cs1 is Element of the carrier' of IIG
[(action_at Cs1), the carrier of IIG] is set
root-tree [(action_at Cs1), the carrier of IIG] is Relation-like Function-like finite countable DecoratedTree-like set
SortsWithConstants IIG is Element of bool the carrier of IIG
action_at Cs1 is Element of the carrier' of IIG
the_arity_of (action_at Cs1) is Relation-like NAT -defined the carrier of IIG -valued Function-like finite countable FinSequence-like FinSubsequence-like Element of the carrier of IIG *
the carrier of IIG * is functional non empty FinSequence-membered M8( the carrier of IIG)
(the_arity_of (action_at Cs1)) * (IIG,SCS,iv) is Relation-like NAT -defined Function-like finite countable Function-yielding V42() 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
(InnerVertices IIG) \ (SortsWithConstants IIG) is Element of bool the carrier of IIG
[(action_at Cs1), the carrier of IIG] is set
p is Relation-like NAT -defined Function-like finite countable FinSequence-like FinSubsequence-like DTree-yielding set
[(action_at Cs1), the carrier of IIG] -tree p is Relation-like Function-like DecoratedTree-like set
p9 is Relation-like NAT -defined Function-like finite countable FinSequence-like FinSubsequence-like DTree-yielding set
[(action_at Cs1), the carrier of IIG] -tree p9 is Relation-like Function-like DecoratedTree-like set
the_result_sort_of (action_at Cs1) is Element of the carrier of IIG
the Sorts of (FreeEnv SCS) . (the_result_sort_of (action_at Cs1)) is non empty finite countable set
((the_arity_of (action_at Cs1)) * (IIG,SCS,iv)) .. p is Relation-like Function-like set
Fp is Relation-like NAT -defined Function-like finite countable FinSequence-like FinSubsequence-like DTree-yielding set
[(action_at Cs1), the carrier of IIG] -tree Fp is Relation-like Function-like DecoratedTree-like set
((the_arity_of (action_at Cs1)) * (IIG,SCS,iv)) .. p9 is Relation-like Function-like set
x is Relation-like NAT -defined Function-like finite countable FinSequence-like FinSubsequence-like DTree-yielding set
[(action_at Cs1), the carrier of IIG] -tree x is Relation-like Function-like DecoratedTree-like set
dom Fp is finite countable V150() V151() V152() V153() V154() V155() V163() V164() V165() Element of bool NAT
dom ((the_arity_of (action_at Cs1)) * (IIG,SCS,iv)) is finite countable set
dom x is finite countable V150() V151() V152() V153() V154() V155() V163() V164() V165() Element of bool NAT
len Fp is V21() V22() V23() V27() finite cardinal countable V133() V134() ext-real V148() V149() V150() V151() V152() V153() V154() V155() V163() V164() V165() Element of NAT
len x is V21() V22() V23() V27() finite cardinal countable V133() V134() ext-real V148() V149() V150() V151() V152() V153() V154() V155() V163() V164() V165() Element of NAT
v1 is V21() V22() V23() V27() finite cardinal countable V133() V134() ext-real set
Fp . v1 is set
x . v1 is set
rng (the_arity_of (action_at Cs1)) is finite countable set
dom (IIG,SCS,iv) is non empty set
dom (the_arity_of (action_at Cs1)) is finite countable V150() V151() V152() V153() V154() V155() V163() V164() V165() Element of bool NAT
(the_arity_of (action_at Cs1)) . v1 is set
x9 is Element of the carrier of IIG
the Sorts of (FreeEnv SCS) . x9 is non empty finite countable set
p . v1 is set
p9 . v1 is set
((the_arity_of (action_at Cs1)) * (IIG,SCS,iv)) . v1 is Relation-like Function-like set
Hti is Relation-like Function-like set
(IIG,SCS,iv) . ((the_arity_of (action_at Cs1)) . v1) is Relation-like Function-like set
It2 is Relation-like Function-like non empty finite countable DecoratedTree-like Element of the Sorts of (FreeEnv SCS) . x9
(IIG,SCS,iv) . x9 is Relation-like the Sorts of (FreeEnv SCS) . x9 -defined the Sorts of (FreeEnv SCS) . x9 -valued Function-like V18( the Sorts of (FreeEnv SCS) . x9, the Sorts of (FreeEnv SCS) . x9) finite countable Element of bool [:( the Sorts of (FreeEnv SCS) . x9),( the Sorts of (FreeEnv SCS) . x9):]
[:( the Sorts of (FreeEnv SCS) . x9),( the Sorts of (FreeEnv SCS) . x9):] is Relation-like finite countable set
bool [:( the Sorts of (FreeEnv SCS) . x9),( the Sorts of (FreeEnv SCS) . x9):] is finite V32() countable set
E2 is Relation-like Function-like non empty finite countable DecoratedTree-like Element of the Sorts of (FreeEnv SCS) . x9
((IIG,SCS,iv) . x9) . E2 is Relation-like Function-like non empty finite countable DecoratedTree-like Element of the Sorts of (FreeEnv SCS) . x9
len p9 is V21() V22() V23() V27() finite cardinal countable V133() V134() ext-real V148() V149() V150() V151() V152() V153() V154() V155() V163() V164() V165() Element of NAT
len (the_arity_of (action_at Cs1)) is V21() V22() V23() V27() finite cardinal countable V133() V134() ext-real V148() V149() V150() V151() V152() V153() V154() V155() V163() V164() V165() Element of NAT
dom p9 is finite countable V150() V151() V152() V153() V154() V155() V163() V164() V165() Element of bool NAT
rng p9 is finite countable set
card E2 is non empty V21() V22() V23() V27() finite cardinal countable V133() V134() ext-real V148() V149() V150() V151() V152() V153() V154() V155() V161() V162() V163() V164() V165() Element of NAT
size (x9,SCS) is V21() V22() V23() V27() finite cardinal countable V133() V134() ext-real set
len p is V21() V22() V23() V27() finite cardinal countable V133() V134() ext-real V148() V149() V150() V151() V152() V153() V154() V155() V163() V164() V165() Element of NAT
dom p is finite countable V150() V151() V152() V153() V154() V155() V163() V164() V165() Element of bool NAT
E1 is Relation-like Function-like non empty finite countable DecoratedTree-like Element of the Sorts of (FreeEnv SCS) . x9
rng p is finite countable set
card E1 is non empty V21() V22() V23() V27() finite cardinal countable V133() V134() ext-real V148() V149() V150() V151() V152() V153() V154() V155() V161() V162() V163() V164() V165() Element of NAT
It1 is Relation-like Function-like non empty finite countable DecoratedTree-like Element of the Sorts of (FreeEnv SCS) . x9
((IIG,SCS,iv) . x9) . E1 is Relation-like Function-like non empty finite countable DecoratedTree-like Element of the Sorts of (FreeEnv SCS) . x9
SortsWithConstants IIG is Element of bool the carrier of IIG
s2 is Relation-like Function-like non empty finite countable DecoratedTree-like Element of the Sorts of (FreeEnv SCS) . InpFs
card s2 is non empty V21() V22() V23() V27() finite cardinal countable V133() V134() ext-real V148() V149() V150() V151() V152() V153() V154() V155() V161() V162() V163() V164() V165() Element of NAT
((IIG,SCS,iv) . InpFs) . s2 is Relation-like Function-like non empty finite countable DecoratedTree-like Element of the Sorts of (FreeEnv SCS) . InpFs
Cs1 is Relation-like Function-like non empty finite countable DecoratedTree-like Element of the Sorts of (FreeEnv SCS) . InpFs
card Cs1 is non empty V21() V22() V23() V27() finite cardinal countable V133() V134() ext-real V148() V149() V150() V151() V152() V153() V154() V155() V161() V162() V163() V164() V165() Element of NAT
((IIG,SCS,iv) . InpFs) . Cs1 is Relation-like Function-like non empty finite countable DecoratedTree-like Element of the Sorts of (FreeEnv SCS) . InpFs
IIG is non empty non void V56() 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 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
K539( the carrier of IIG, the ResultSort of IIG) is Element of bool the carrier of IIG
the carrier of IIG \ K539( the carrier of IIG, the ResultSort of IIG) is Element of bool the carrier of IIG
SCS is non-empty finitely-generated finite-yielding MSAlgebra over IIG
FreeEnv SCS is strict non-empty free MSAlgebra over IIG
the Sorts of SCS is Relation-like non-empty non empty-yielding the carrier of IIG -defined Function-like non empty total set
FreeMSA the Sorts of SCS is strict non-empty MSAlgebra over IIG
the Sorts of (FreeEnv SCS) is Relation-like non-empty non empty-yielding the carrier of IIG -defined Function-like non empty total set
InpFs is Element of the carrier of IIG
the Sorts of (FreeEnv SCS) . InpFs is non empty finite countable set
iv is Relation-like InputVertices IIG -defined Function-like total InputValues of SCS
(IIG,SCS,InpFs,iv) is Relation-like Function-like non empty finite countable DecoratedTree-like Element of the Sorts of (FreeEnv SCS) . InpFs
(IIG,SCS,iv) is Relation-like the carrier of IIG -defined Function-like non empty total Function-yielding V42() ManySortedFunction of the Sorts of (FreeEnv SCS), the Sorts of (FreeEnv SCS)
(IIG,SCS,iv) . InpFs is Relation-like the Sorts of (FreeEnv SCS) . InpFs -defined the Sorts of (FreeEnv SCS) . InpFs -valued Function-like V18( the Sorts of (FreeEnv SCS) . InpFs, the Sorts of (FreeEnv SCS) . InpFs) finite countable Element of bool [:( the Sorts of (FreeEnv SCS) . InpFs),( the Sorts of (FreeEnv SCS) . InpFs):]
[:( the Sorts of (FreeEnv SCS) . InpFs),( the Sorts of (FreeEnv SCS) . InpFs):] is Relation-like finite countable set
bool [:( the Sorts of (FreeEnv SCS) . InpFs),( the Sorts of (FreeEnv SCS) . InpFs):] is finite V32() countable set
((IIG,SCS,iv) . InpFs) . (IIG,SCS,InpFs,iv) is Relation-like Function-like non empty finite countable DecoratedTree-like Element of the Sorts of (FreeEnv SCS) . InpFs
size (InpFs,SCS) is V21() V22() V23() V27() finite cardinal countable V133() V134() ext-real set
dSCS is Relation-like Function-like non empty finite countable DecoratedTree-like Element of the Sorts of (FreeEnv SCS) . InpFs
card dSCS is non empty V21() V22() V23() V27() finite cardinal countable V133() V134() ext-real V148() V149() V150() V151() V152() V153() V154() V155() V161() V162() V163() V164() V165() Element of NAT
s1 is Relation-like Function-like non empty finite countable DecoratedTree-like Element of the Sorts of (FreeEnv SCS) . InpFs
card s1 is non empty V21() V22() V23() V27() finite cardinal countable V133() V134() ext-real V148() V149() V150() V151() V152() V153() V154() V155() V161() V162() V163() V164() V165() Element of NAT
((IIG,SCS,iv) . InpFs) . s1 is Relation-like Function-like non empty finite countable DecoratedTree-like Element of the Sorts of (FreeEnv SCS) . InpFs
IIG is non empty non void V56() 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 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
K539( the carrier of IIG, the ResultSort of IIG) is Element of bool the carrier of IIG
the carrier of IIG \ K539( the carrier of IIG, the ResultSort of IIG) is Element of bool the carrier of IIG
InnerVertices IIG is non empty Element of bool the carrier of IIG
SCS is non-empty finitely-generated finite-yielding MSAlgebra over IIG
InpFs is Element of the carrier of IIG
action_at InpFs is Element of the carrier' of IIG
the_arity_of (action_at InpFs) is Relation-like NAT -defined the carrier of IIG -valued Function-like finite countable FinSequence-like FinSubsequence-like Element of the carrier of IIG *
the carrier of IIG * is functional non empty FinSequence-membered M8( the carrier of IIG)
dom (the_arity_of (action_at InpFs)) is finite countable V150() V151() V152() V153() V154() V155() V163() V164() V165() Element of bool NAT
[(action_at InpFs), the carrier of IIG] is set
iv is Relation-like InputVertices IIG -defined Function-like total InputValues of SCS
(IIG,SCS,InpFs,iv) is Relation-like Function-like non empty finite countable DecoratedTree-like Element of the Sorts of (FreeEnv SCS) . InpFs
FreeEnv SCS is strict non-empty free MSAlgebra over IIG
the Sorts of SCS is Relation-like non-empty non empty-yielding the carrier of IIG -defined Function-like non empty total set
FreeMSA the Sorts of SCS is strict non-empty MSAlgebra over IIG
the Sorts of (FreeEnv SCS) is Relation-like non-empty non empty-yielding the carrier of IIG -defined Function-like non empty total set
the Sorts of (FreeEnv SCS) . InpFs is non empty finite countable set
dSCS is Relation-like NAT -defined Function-like finite countable FinSequence-like FinSubsequence-like DTree-yielding set
dom dSCS is finite countable V150() V151() V152() V153() V154() V155() V163() V164() V165() Element of bool NAT
[(action_at InpFs), the carrier of IIG] -tree dSCS is Relation-like Function-like DecoratedTree-like set
Cs1 is V21() V22() V23() V27() finite cardinal countable V133() V134() ext-real set
dSCS . Cs1 is set
(the_arity_of (action_at InpFs)) /. Cs1 is Element of the carrier of IIG
(IIG,SCS,((the_arity_of (action_at InpFs)) /. Cs1),iv) is Relation-like Function-like non empty finite countable DecoratedTree-like Element of the Sorts of (FreeEnv SCS) . ((the_arity_of (action_at InpFs)) /. Cs1)
the Sorts of (FreeEnv SCS) . ((the_arity_of (action_at InpFs)) /. Cs1) is non empty finite countable set
len dSCS is V21() V22() V23() V27() finite cardinal countable V133() V134() ext-real V148() V149() V150() V151() V152() V153() V154() V155() V163() V164() V165() Element of NAT
len (the_arity_of (action_at InpFs)) is V21() V22() V23() V27() finite cardinal countable V133() V134() ext-real V148() V149() V150() V151() V152() V153() V154() V155() V163() V164() V165() Element of NAT
Args ((action_at InpFs),(FreeEnv SCS)) is functional non empty Element of rng ( the Sorts of (FreeEnv SCS) #)
the Sorts of (FreeEnv SCS) # is Relation-like the carrier of IIG * -defined Function-like non empty total set
rng ( the Sorts of (FreeEnv SCS) #) is non empty set
dom the ResultSort of IIG is set
Result ((action_at InpFs),(FreeEnv SCS)) is non empty Element of rng the Sorts of (FreeEnv SCS)
rng the Sorts of (FreeEnv SCS) is non empty set
the ResultSort of IIG * the Sorts of (FreeEnv SCS) 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 (FreeEnv SCS)) . (action_at InpFs) is non empty set
the ResultSort of IIG . (action_at InpFs) is Element of the carrier of IIG
the Sorts of (FreeEnv SCS) . ( the ResultSort of IIG . (action_at InpFs)) is non empty finite countable set
FreeSort the Sorts of SCS is Relation-like non-empty non empty-yielding the carrier of IIG -defined Function-like non empty total set
FreeOper the Sorts of SCS is Relation-like the carrier' of IIG -defined Function-like non empty total Function-yielding V42() ManySortedFunction of the Arity of IIG * ((FreeSort the Sorts of SCS) #), the ResultSort of IIG * (FreeSort the Sorts of SCS)
the Arity of IIG is Relation-like the carrier' of IIG -defined the carrier of IIG * -valued Function-like V18( the carrier' of IIG, the carrier of IIG * ) Function-yielding V42() 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 SCS) # is Relation-like the carrier of IIG * -defined Function-like non empty total set
the Arity of IIG * ((FreeSort the Sorts of SCS) #) is Relation-like the carrier' of IIG -defined Function-like non empty total set
the ResultSort of IIG * (FreeSort the Sorts of SCS) is Relation-like non-empty non empty-yielding the carrier' of IIG -defined Function-like non empty total set
MSAlgebra(# (FreeSort the Sorts of SCS),(FreeOper the Sorts of SCS) #) is strict MSAlgebra over IIG
the Arity of IIG * ( the Sorts of (FreeEnv SCS) #) is Relation-like the carrier' of IIG -defined Function-like non empty total set
( the Arity of IIG * ( the Sorts of (FreeEnv SCS) #)) . (action_at InpFs) is set
DTConMSA the Sorts of SCS is non empty strict with_terminals with_nonterminals with_useful_nonterminals L13()
the carrier of (DTConMSA the Sorts of SCS) is non empty set
FinTrees the carrier of (DTConMSA the Sorts of SCS) is functional non empty constituted-DTrees DTree-set of the carrier of (DTConMSA the Sorts of SCS)
TS (DTConMSA the Sorts of SCS) is functional constituted-DTrees Element of bool (FinTrees the carrier of (DTConMSA the Sorts of SCS))
bool (FinTrees the carrier of (DTConMSA the Sorts of SCS)) is set
Cs1 is Relation-like Function-like Element of Args ((action_at InpFs),(FreeEnv SCS))
Den ((action_at InpFs),(FreeEnv SCS)) is Relation-like Args ((action_at InpFs),(FreeEnv SCS)) -defined Result ((action_at InpFs),(FreeEnv SCS)) -valued Function-like V18( Args ((action_at InpFs),(FreeEnv SCS)), Result ((action_at InpFs),(FreeEnv SCS))) Element of bool [:(Args ((action_at InpFs),(FreeEnv SCS))),(Result ((action_at InpFs),(FreeEnv SCS))):]
[:(Args ((action_at InpFs),(FreeEnv SCS))),(Result ((action_at InpFs),(FreeEnv SCS))):] is Relation-like set
bool [:(Args ((action_at InpFs),(FreeEnv SCS))),(Result ((action_at InpFs),(FreeEnv SCS))):] is set
(FreeOper the Sorts of SCS) . (action_at InpFs) is Relation-like ( the Arity of IIG * ((FreeSort the Sorts of SCS) #)) . (action_at InpFs) -defined ( the ResultSort of IIG * (FreeSort the Sorts of SCS)) . (action_at InpFs) -valued Function-like V18(( the Arity of IIG * ((FreeSort the Sorts of SCS) #)) . (action_at InpFs),( the ResultSort of IIG * (FreeSort the Sorts of SCS)) . (action_at InpFs)) Element of bool [:(( the Arity of IIG * ((FreeSort the Sorts of SCS) #)) . (action_at InpFs)),(( the ResultSort of IIG * (FreeSort the Sorts of SCS)) . (action_at InpFs)):]
( the Arity of IIG * ((FreeSort the Sorts of SCS) #)) . (action_at InpFs) is set
( the ResultSort of IIG * (FreeSort the Sorts of SCS)) . (action_at InpFs) is non empty set
[:(( the Arity of IIG * ((FreeSort the Sorts of SCS) #)) . (action_at InpFs)),(( the ResultSort of IIG * (FreeSort the Sorts of SCS)) . (action_at InpFs)):] is Relation-like set
bool [:(( the Arity of IIG * ((FreeSort the Sorts of SCS) #)) . (action_at InpFs)),(( the ResultSort of IIG * (FreeSort the Sorts of SCS)) . (action_at InpFs)):] is set
DenOp ((action_at InpFs), the Sorts of SCS) is Relation-like ( the Arity of IIG * ((FreeSort the Sorts of SCS) #)) . (action_at InpFs) -defined ( the ResultSort of IIG * (FreeSort the Sorts of SCS)) . (action_at InpFs) -valued Function-like V18(( the Arity of IIG * ((FreeSort the Sorts of SCS) #)) . (action_at InpFs),( the ResultSort of IIG * (FreeSort the Sorts of SCS)) . (action_at InpFs)) Element of bool [:(( the Arity of IIG * ((FreeSort the Sorts of SCS) #)) . (action_at InpFs)),(( the ResultSort of IIG * (FreeSort the Sorts of SCS)) . (action_at InpFs)):]
Sym ((action_at InpFs), the Sorts of SCS) is Element of K355((DTConMSA the Sorts of SCS))
K355((DTConMSA the Sorts of SCS)) is non empty Element of bool the carrier of (DTConMSA the Sorts of SCS)
bool the carrier of (DTConMSA the Sorts of SCS) is set
x is Relation-like NAT -defined FinTrees the carrier of (DTConMSA the Sorts of SCS) -valued Function-like finite countable Function-yielding V42() FinSequence-like FinSubsequence-like FinSequence of TS (DTConMSA the Sorts of SCS)
roots x is Relation-like NAT -defined the carrier of (DTConMSA the Sorts of SCS) -valued Function-like finite countable FinSequence-like FinSubsequence-like FinSequence of the carrier of (DTConMSA the Sorts of SCS)
(Den ((action_at InpFs),(FreeEnv SCS))) . dSCS is set
(Sym ((action_at InpFs), the Sorts of SCS)) -tree x is Relation-like the carrier of (DTConMSA the Sorts of SCS) -valued Function-like finite countable DecoratedTree-like Element of FinTrees the carrier of (DTConMSA the Sorts of SCS)
[(action_at InpFs), the carrier of IIG] -tree x is Relation-like Function-like DecoratedTree-like set
the_result_sort_of (action_at InpFs) is Element of the carrier of IIG
the Sorts of (FreeMSA the Sorts of SCS) 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 SCS) . InpFs is non empty set
p is V21() V22() V23() V27() finite cardinal countable V133() V134() ext-real V148() V149() V150() V151() V152() V153() V154() V155() V163() V164() V165() Element of NAT
(the_arity_of (action_at InpFs)) /. p is Element of the carrier of IIG
dSCS . p is set
(IIG,SCS,((the_arity_of (action_at InpFs)) /. p),iv) is Relation-like Function-like non empty finite countable DecoratedTree-like Element of the Sorts of (FreeEnv SCS) . ((the_arity_of (action_at InpFs)) /. p)
the Sorts of (FreeEnv SCS) . ((the_arity_of (action_at InpFs)) /. p) is non empty finite countable set
p is Relation-like Function-like non empty finite countable DecoratedTree-like Element of the Sorts of (FreeEnv SCS) . ((the_arity_of (action_at InpFs)) /. p)
p9 is Relation-like Function-like non empty finite countable DecoratedTree-like Element of the Sorts of (FreeEnv SCS) . ((the_arity_of (action_at InpFs)) /. p)
the Sorts of (FreeMSA the Sorts of SCS) . ((the_arity_of (action_at InpFs)) /. p) is non empty set
size (((the_arity_of (action_at InpFs)) /. p),SCS) is V21() V22() V23() V27() finite cardinal countable V133() V134() ext-real set
(IIG,SCS,iv) is Relation-like the carrier of IIG -defined Function-like non empty total Function-yielding V42() ManySortedFunction of the Sorts of (FreeEnv SCS), the Sorts of (FreeEnv SCS)
(IIG,SCS,iv) . ((the_arity_of (action_at InpFs)) /. p) is Relation-like the Sorts of (FreeEnv SCS) . ((the_arity_of (action_at InpFs)) /. p) -defined the Sorts of (FreeEnv SCS) . ((the_arity_of (action_at InpFs)) /. p) -valued Function-like V18( the Sorts of (FreeEnv SCS) . ((the_arity_of (action_at InpFs)) /. p), the Sorts of (FreeEnv SCS) . ((the_arity_of (action_at InpFs)) /. p)) finite countable Element of bool [:( the Sorts of (FreeEnv SCS) . ((the_arity_of (action_at InpFs)) /. p)),( the Sorts of (FreeEnv SCS) . ((the_arity_of (action_at InpFs)) /. p)):]
[:( the Sorts of (FreeEnv SCS) . ((the_arity_of (action_at InpFs)) /. p)),( the Sorts of (FreeEnv SCS) . ((the_arity_of (action_at InpFs)) /. p)):] is Relation-like finite countable set
bool [:( the Sorts of (FreeEnv SCS) . ((the_arity_of (action_at InpFs)) /. p)),( the Sorts of (FreeEnv SCS) . ((the_arity_of (action_at InpFs)) /. p)):] is finite V32() countable set
card p9 is non empty V21() V22() V23() V27() finite cardinal countable V133() V134() ext-real V148() V149() V150() V151() V152() V153() V154() V155() V161() V162() V163() V164() V165() Element of NAT
Fp is Relation-like Function-like non empty finite countable DecoratedTree-like Element of the Sorts of (FreeMSA the Sorts of SCS) . ((the_arity_of (action_at InpFs)) /. p)
card Fp is non empty V21() V22() V23() V27() finite cardinal countable V133() V134() ext-real V148() V149() V150() V151() V152() V153() V154() V155() V161() V162() V163() V164() V165() Element of NAT
((IIG,SCS,iv) . ((the_arity_of (action_at InpFs)) /. p)) . Fp is set
x9 is Relation-like Function-like non empty finite countable DecoratedTree-like Element of the Sorts of (FreeMSA the Sorts of SCS) . InpFs
card x9 is non empty V21() V22() V23() V27() finite cardinal countable V133() V134() ext-real V148() V149() V150() V151() V152() V153() V154() V155() V161() V162() V163() V164() V165() Element of NAT
size (InpFs,SCS) is V21() V22() V23() V27() finite cardinal countable V133() V134() ext-real set
p is V21() V22() V23() V27() finite cardinal countable V133() V134() ext-real V148() V149() V150() V151() V152() V153() V154() V155() V163() V164() V165() Element of NAT
dSCS . p is set
(the_arity_of (action_at InpFs)) /. p is Element of the carrier of IIG
(IIG,SCS,((the_arity_of (action_at InpFs)) /. p),iv) is Relation-like Function-like non empty finite countable DecoratedTree-like Element of the Sorts of (FreeEnv SCS) . ((the_arity_of (action_at InpFs)) /. p)
the Sorts of (FreeEnv SCS) . ((the_arity_of (action_at InpFs)) /. p) is non empty finite countable set
(IIG,SCS,iv) . ((the_arity_of (action_at InpFs)) /. p) is Relation-like the Sorts of (FreeEnv SCS) . ((the_arity_of (action_at InpFs)) /. p) -defined the Sorts of (FreeEnv SCS) . ((the_arity_of (action_at InpFs)) /. p) -valued Function-like V18( the Sorts of (FreeEnv SCS) . ((the_arity_of (action_at InpFs)) /. p), the Sorts of (FreeEnv SCS) . ((the_arity_of (action_at InpFs)) /. p)) finite countable Element of bool [:( the Sorts of (FreeEnv SCS) . ((the_arity_of (action_at InpFs)) /. p)),( the Sorts of (FreeEnv SCS) . ((the_arity_of (action_at InpFs)) /. p)):]
[:( the Sorts of (FreeEnv SCS) . ((the_arity_of (action_at InpFs)) /. p)),( the Sorts of (FreeEnv SCS) . ((the_arity_of (action_at InpFs)) /. p)):] is Relation-like finite countable set
bool [:( the Sorts of (FreeEnv SCS) . ((the_arity_of (action_at InpFs)) /. p)),( the Sorts of (FreeEnv SCS) . ((the_arity_of (action_at InpFs)) /. p)):] is finite V32() countable set
((IIG,SCS,iv) . ((the_arity_of (action_at InpFs)) /. p)) . (dSCS . p) is set
(IIG,SCS,iv) . InpFs is Relation-like the Sorts of (FreeEnv SCS) . InpFs -defined the Sorts of (FreeEnv SCS) . InpFs -valued Function-like V18( the Sorts of (FreeEnv SCS) . InpFs, the Sorts of (FreeEnv SCS) . InpFs) finite countable Element of bool [:( the Sorts of (FreeEnv SCS) . InpFs),( the Sorts of (FreeEnv SCS) . InpFs):]
[:( the Sorts of (FreeEnv SCS) . InpFs),( the Sorts of (FreeEnv SCS) . InpFs):] is Relation-like finite countable set
bool [:( the Sorts of (FreeEnv SCS) . InpFs),( the Sorts of (FreeEnv SCS) . InpFs):] is finite V32() countable set
((IIG,SCS,iv) . InpFs) . x9 is set
IIG is non empty non void V56() 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 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
K539( the carrier of IIG, the ResultSort of IIG) is Element of bool the carrier of IIG
the carrier of IIG \ K539( the carrier of IIG, the ResultSort of IIG) is Element of bool the carrier of IIG
SCS is non-empty finitely-generated finite-yielding MSAlgebra over IIG
FreeEnv SCS is strict non-empty free MSAlgebra over IIG
the Sorts of SCS is Relation-like non-empty non empty-yielding the carrier of IIG -defined Function-like non empty total set
FreeMSA the Sorts of SCS is strict non-empty MSAlgebra over IIG
the Sorts of (FreeEnv SCS) is Relation-like non-empty non empty-yielding the carrier of IIG -defined Function-like non empty total set
InpFs is Element of the carrier of IIG
the Sorts of (FreeEnv SCS) . InpFs is non empty finite countable set
the Sorts of SCS . InpFs is non empty set
Eval SCS is Relation-like the carrier of IIG -defined Function-like non empty total Function-yielding V42() ManySortedFunction of the Sorts of (FreeEnv SCS), the Sorts of SCS
(Eval SCS) . InpFs is Relation-like the Sorts of (FreeEnv SCS) . InpFs -defined the Sorts of SCS . InpFs -valued Function-like V18( the Sorts of (FreeEnv SCS) . InpFs, the Sorts of SCS . InpFs) finite countable Element of bool [:( the Sorts of (FreeEnv SCS) . InpFs),( the Sorts of SCS . InpFs):]
[:( the Sorts of (FreeEnv SCS) . InpFs),( the Sorts of SCS . InpFs):] is Relation-like set
bool [:( the Sorts of (FreeEnv SCS) . InpFs),( the Sorts of SCS . InpFs):] is set
iv is Relation-like InputVertices IIG -defined Function-like total InputValues of SCS
(IIG,SCS,InpFs,iv) is Relation-like Function-like non empty finite countable DecoratedTree-like Element of the Sorts of (FreeEnv SCS) . InpFs
((Eval SCS) . InpFs) . (IIG,SCS,InpFs,iv) is Element of the Sorts of SCS . InpFs
IIG is non empty non void V56() 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 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
K539( the carrier of IIG, the ResultSort of IIG) is Element of bool the carrier of IIG
the carrier of IIG \ K539( the carrier of IIG, the ResultSort of IIG) is Element of bool the carrier of IIG
SCS is non-empty finitely-generated finite-yielding MSAlgebra over IIG
InpFs is Element of the carrier of IIG
iv is Relation-like InputVertices IIG -defined Function-like total InputValues of SCS
(IIG,SCS,InpFs,iv) is Element of the Sorts of SCS . InpFs
the Sorts of SCS is Relation-like non-empty non empty-yielding the carrier of IIG -defined Function-like non empty total set
the Sorts of SCS . InpFs is non empty set
FreeEnv SCS is strict non-empty free MSAlgebra over IIG
FreeMSA the Sorts of SCS is strict non-empty MSAlgebra over IIG
the Sorts of (FreeEnv SCS) is Relation-like non-empty non empty-yielding the carrier of IIG -defined Function-like non empty total set
the Sorts of (FreeEnv SCS) . InpFs is non empty finite countable set
Eval SCS is Relation-like the carrier of IIG -defined Function-like non empty total Function-yielding V42() ManySortedFunction of the Sorts of (FreeEnv SCS), the Sorts of SCS
(Eval SCS) . InpFs is Relation-like the Sorts of (FreeEnv SCS) . InpFs -defined the Sorts of SCS . InpFs -valued Function-like V18( the Sorts of (FreeEnv SCS) . InpFs, the Sorts of SCS . InpFs) finite countable Element of bool [:( the Sorts of (FreeEnv SCS) . InpFs),( the Sorts of SCS . InpFs):]
[:( the Sorts of (FreeEnv SCS) . InpFs),( the Sorts of SCS . InpFs):] is Relation-like set
bool [:( the Sorts of (FreeEnv SCS) . InpFs),( the Sorts of SCS . InpFs):] is set
(IIG,SCS,InpFs,iv) is Relation-like Function-like non empty finite countable DecoratedTree-like Element of the Sorts of (FreeEnv SCS) . InpFs
((Eval SCS) . InpFs) . (IIG,SCS,InpFs,iv) is Element of the Sorts of SCS . InpFs
iv . InpFs is set
FreeSort the Sorts of SCS is Relation-like non-empty non empty-yielding the carrier of IIG -defined Function-like non empty total set
(FreeSort the Sorts of SCS) . InpFs is non empty set
FreeSort ( the Sorts of SCS,InpFs) is functional non empty constituted-DTrees Element of bool (TS (DTConMSA the Sorts of SCS))
DTConMSA the Sorts of SCS is non empty strict with_terminals with_nonterminals with_useful_nonterminals L13()
TS (DTConMSA the Sorts of SCS) is functional constituted-DTrees Element of bool (FinTrees the carrier of (DTConMSA the Sorts of SCS))
the carrier of (DTConMSA the Sorts of SCS) is non empty set
FinTrees the carrier of (DTConMSA the Sorts of SCS) is functional non empty constituted-DTrees DTree-set of the carrier of (DTConMSA the Sorts of SCS)
bool (FinTrees the carrier of (DTConMSA the Sorts of SCS)) is set
bool (TS (DTConMSA the Sorts of SCS)) is set
{ b₁ where b₁ is Relation-like Function-like Element of TS (DTConMSA the Sorts of SCS) : ( ex b₂ being set st
( b₂ in the Sorts of SCS . InpFs & b₁ = root-tree [b₂,InpFs] ) or ex b₂ being Element of the carrier' of IIG st
( [b₂, the carrier of IIG] = b₁ . {} & the_result_sort_of b₂ = InpFs ) ) } is set
[(iv . InpFs),InpFs] is set
root-tree [(iv . InpFs),InpFs] is Relation-like Function-like finite countable DecoratedTree-like set
FreeGen (InpFs, the Sorts of SCS) is non empty Element of bool ((FreeSort the Sorts of SCS) . InpFs)
bool ((FreeSort the Sorts of SCS) . InpFs) is set
size (InpFs,SCS) is V21() V22() V23() V27() finite cardinal countable V133() V134() ext-real set
(IIG,SCS,iv) is Relation-like the carrier of IIG -defined Function-like non empty total Function-yielding V42() ManySortedFunction of the Sorts of (FreeEnv SCS), the Sorts of (FreeEnv SCS)
(IIG,SCS,iv) . InpFs is Relation-like the Sorts of (FreeEnv SCS) . InpFs -defined the Sorts of (FreeEnv SCS) . InpFs -valued Function-like V18( the Sorts of (FreeEnv SCS) . InpFs, the Sorts of (FreeEnv SCS) . InpFs) finite countable Element of bool [:( the Sorts of (FreeEnv SCS) . InpFs),( the Sorts of (FreeEnv SCS) . InpFs):]
[:( the Sorts of (FreeEnv SCS) . InpFs),( the Sorts of (FreeEnv SCS) . InpFs):] is Relation-like finite countable set
bool [:( the Sorts of (FreeEnv SCS) . InpFs),( the Sorts of (FreeEnv SCS) . InpFs):] is finite V32() countable set
s1 is Relation-like Function-like non empty finite countable DecoratedTree-like Element of the Sorts of (FreeEnv SCS) . InpFs
card s1 is non empty V21() V22() V23() V27() finite cardinal countable V133() V134() ext-real V148() V149() V150() V151() V152() V153() V154() V155() V161() V162() V163() V164() V165() Element of NAT
((IIG,SCS,iv) . InpFs) . s1 is Relation-like Function-like non empty finite countable DecoratedTree-like Element of the Sorts of (FreeEnv SCS) . InpFs
the Sorts of (FreeMSA the Sorts of SCS) 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 SCS) . InpFs is non empty set
FreeOper the Sorts of SCS is Relation-like the carrier' of IIG -defined Function-like non empty total Function-yielding V42() ManySortedFunction of the Arity of IIG * ((FreeSort the Sorts of SCS) #), the ResultSort of IIG * (FreeSort the Sorts of SCS)
the Arity of IIG is Relation-like the carrier' of IIG -defined the carrier of IIG * -valued Function-like V18( the carrier' of IIG, the carrier of IIG * ) Function-yielding V42() Element of bool [: the carrier' of IIG,( the carrier of IIG *):]
the carrier of IIG * is functional non empty FinSequence-membered M8( 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 SCS) # is Relation-like the carrier of IIG * -defined Function-like non empty total set
the Arity of IIG * ((FreeSort the Sorts of SCS) #) is Relation-like the carrier' of IIG -defined Function-like non empty total set
the ResultSort of IIG * (FreeSort the Sorts of SCS) is Relation-like non-empty non empty-yielding the carrier' of IIG -defined Function-like non empty total set
MSAlgebra(# (FreeSort the Sorts of SCS),(FreeOper the Sorts of SCS) #) is strict MSAlgebra over IIG
s2 is Relation-like Function-like Element of TS (DTConMSA the Sorts of SCS)
Cs1 is set
[Cs1,InpFs] is set
root-tree [Cs1,InpFs] is Relation-like Function-like finite countable DecoratedTree-like set
Cs2 is Element of the carrier' of IIG
[Cs2, the carrier of IIG] is set
s2 . {} is set
the_result_sort_of Cs2 is Element of the carrier of IIG
(IIG,SCS,iv) is Relation-like the carrier of IIG -defined Function-like non empty total Function-yielding V42() ManySortedFunction of FreeGen the Sorts of SCS, the Sorts of (FreeEnv SCS)
FreeGen the Sorts of SCS is Relation-like the carrier of IIG -defined Function-like non empty total GeneratorSet of FreeMSA the Sorts of SCS
(IIG,SCS,iv) . InpFs is Relation-like (FreeGen the Sorts of SCS) . InpFs -defined the Sorts of (FreeEnv SCS) . InpFs -valued Function-like V18((FreeGen the Sorts of SCS) . InpFs, the Sorts of (FreeEnv SCS) . InpFs) Element of bool [:((FreeGen the Sorts of SCS) . InpFs),( the Sorts of (FreeEnv SCS) . InpFs):]
(FreeGen the Sorts of SCS) . InpFs is set
[:((FreeGen the Sorts of SCS) . InpFs),( the Sorts of (FreeEnv SCS) . InpFs):] is Relation-like set
bool [:((FreeGen the Sorts of SCS) . InpFs),( the Sorts of (FreeEnv SCS) . InpFs):] is set
{(root-tree [(iv . InpFs),InpFs])} is functional non empty trivial finite V32() 1 -element with_common_domain countable set
(FreeGen (InpFs, the Sorts of SCS)) --> (root-tree [(iv . InpFs),InpFs]) is Relation-like FreeGen (InpFs, the Sorts of SCS) -defined {(root-tree [(iv . InpFs),InpFs])} -valued Function-like constant non empty total V18( FreeGen (InpFs, the Sorts of SCS),{(root-tree [(iv . InpFs),InpFs])}) Function-yielding V42() Element of bool [:(FreeGen (InpFs, the Sorts of SCS)),{(root-tree [(iv . InpFs),InpFs])}:]
[:(FreeGen (InpFs, the Sorts of SCS)),{(root-tree [(iv . InpFs),InpFs])}:] is Relation-like set
bool [:(FreeGen (InpFs, the Sorts of SCS)),{(root-tree [(iv . InpFs),InpFs])}:] is set
dom ((IIG,SCS,iv) . InpFs) is set
((IIG,SCS,iv) . InpFs) . s1 is set
((Eval SCS) . InpFs) . (root-tree [(iv . InpFs),InpFs]) is set
IIG is non empty non void V56() 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 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
K539( the carrier of IIG, the ResultSort of IIG) is Element of bool the carrier of IIG
the carrier of IIG \ K539( the carrier of IIG, the ResultSort of IIG) is Element of bool the carrier of IIG
SortsWithConstants IIG is Element of bool the carrier of IIG
InpFs is non-empty finitely-generated finite-yielding MSAlgebra over IIG
Set-Constants InpFs is Relation-like SortsWithConstants IIG -defined Function-like total set
iv is Element of the carrier of IIG
(Set-Constants InpFs) . iv is set
dSCS is Relation-like InputVertices IIG -defined Function-like total InputValues of InpFs
(IIG,InpFs,iv,dSCS) is Element of the Sorts of InpFs . iv
the Sorts of InpFs is Relation-like non-empty non empty-yielding the carrier of IIG -defined Function-like non empty total set
the Sorts of InpFs . iv is non empty set
FreeEnv InpFs is strict non-empty free MSAlgebra over IIG
FreeMSA the Sorts of InpFs is strict non-empty MSAlgebra over IIG
the Sorts of (FreeEnv InpFs) is Relation-like non-empty non empty-yielding the carrier of IIG -defined Function-like non empty total set
the Sorts of (FreeEnv InpFs) . iv is non empty finite countable set
Eval InpFs is Relation-like the carrier of IIG -defined Function-like non empty total Function-yielding V42() ManySortedFunction of the Sorts of (FreeEnv InpFs), the Sorts of InpFs
(Eval InpFs) . iv is Relation-like the Sorts of (FreeEnv InpFs) . iv -defined the Sorts of InpFs . iv -valued Function-like V18( the Sorts of (FreeEnv InpFs) . iv, the Sorts of InpFs . iv) finite countable Element of bool [:( the Sorts of (FreeEnv InpFs) . iv),( the Sorts of InpFs . iv):]
[:( the Sorts of (FreeEnv InpFs) . iv),( the Sorts of InpFs . iv):] is Relation-like set
bool [:( the Sorts of (FreeEnv InpFs) . iv),( the Sorts of InpFs . iv):] is set
(IIG,InpFs,iv,dSCS) is Relation-like Function-like non empty finite countable DecoratedTree-like Element of the Sorts of (FreeEnv InpFs) . iv
((Eval InpFs) . iv) . (IIG,InpFs,iv,dSCS) is Element of the Sorts of InpFs . iv
action_at iv is Element of the carrier' of IIG
[(action_at iv), the carrier of IIG] is set
root-tree [(action_at iv), the carrier of IIG] is Relation-like Function-like finite countable DecoratedTree-like set
((Eval InpFs) . iv) . (root-tree [(action_at iv), the carrier of IIG]) 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 V21() V22() V23() V25() V26() V27() finite finite-yielding V32() cardinal {} -element Cardinal-yielding countable Function-yielding V42() FinSequence-like FinSubsequence-like FinSequence-membered constituted-Trees constituted-FinTrees constituted-DTrees Tree-yielding FinTree-yielding DTree-yielding V133() V134() ext-real V150() V151() V152() V153() V154() V155() V156() V163() V164() V165() V166() FinSequence of the carrier of IIG
the Arity of IIG is Relation-like the carrier' of IIG -defined the carrier of IIG * -valued Function-like V18( the carrier' of IIG, the carrier of IIG * ) Function-yielding V42() Element of bool [: the carrier' of IIG,( the carrier of IIG *):]
the carrier of IIG * is functional non empty FinSequence-membered M8( 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 set
dom the ResultSort of IIG is set
InnerVertices IIG is non empty Element of bool the carrier of IIG
the_result_sort_of (action_at iv) is Element of the carrier of IIG
{ b₁ where b₁ is Element of the carrier of IIG : b₁ is with_const_op } is set
x is Element of the carrier of IIG
x9 is Element of the carrier' of IIG
the Arity of IIG . x9 is Relation-like NAT -defined Function-like finite countable FinSequence-like FinSubsequence-like Element of the carrier of IIG *
the ResultSort of IIG . x9 is Element of the carrier of IIG
the_result_sort_of x9 is Element of the carrier of IIG
Args ((action_at iv),(FreeEnv InpFs)) is functional non empty Element of rng ( the Sorts of (FreeEnv InpFs) #)
the Sorts of (FreeEnv InpFs) # is Relation-like the carrier of IIG * -defined Function-like non empty total set
rng ( the Sorts of (FreeEnv InpFs) #) is non empty set
the Arity of IIG * ( the Sorts of (FreeEnv InpFs) #) is Relation-like the carrier' of IIG -defined Function-like non empty total set
( the Arity of IIG * ( the Sorts of (FreeEnv InpFs) #)) . (action_at iv) is set
the Arity of IIG . (action_at iv) is Relation-like NAT -defined Function-like finite countable FinSequence-like FinSubsequence-like Element of the carrier of IIG *
( the Sorts of (FreeEnv InpFs) #) . ( the Arity of IIG . (action_at iv)) is set
Args ((action_at iv),InpFs) is functional non empty Element of rng ( the Sorts of InpFs #)
the Sorts of InpFs # is Relation-like the carrier of IIG * -defined Function-like non empty total set
rng ( the Sorts of InpFs #) is non empty set
p is Relation-like Function-like Element of Args ((action_at iv),(FreeEnv InpFs))
(Eval InpFs) # p is Relation-like Function-like Element of Args ((action_at iv),InpFs)
(Eval InpFs) . (the_result_sort_of (action_at iv)) is Relation-like the Sorts of (FreeEnv InpFs) . (the_result_sort_of (action_at iv)) -defined the Sorts of InpFs . (the_result_sort_of (action_at iv)) -valued Function-like V18( the Sorts of (FreeEnv InpFs) . (the_result_sort_of (action_at iv)), the Sorts of InpFs . (the_result_sort_of (action_at iv))) finite countable Element of bool [:( the Sorts of (FreeEnv InpFs) . (the_result_sort_of (action_at iv))),( the Sorts of InpFs . (the_result_sort_of (action_at iv))):]
the Sorts of (FreeEnv InpFs) . (the_result_sort_of (action_at iv)) is non empty finite countable set
the Sorts of InpFs . (the_result_sort_of (action_at iv)) is non empty set
[:( the Sorts of (FreeEnv InpFs) . (the_result_sort_of (action_at iv))),( the Sorts of InpFs . (the_result_sort_of (action_at iv))):] is Relation-like set
bool [:( the Sorts of (FreeEnv InpFs) . (the_result_sort_of (action_at iv))),( the Sorts of InpFs . (the_result_sort_of (action_at iv))):] is set
Result ((action_at iv),(FreeEnv InpFs)) is non empty Element of rng the Sorts of (FreeEnv InpFs)
rng the Sorts of (FreeEnv InpFs) is non empty set
Den ((action_at iv),(FreeEnv InpFs)) is Relation-like Args ((action_at iv),(FreeEnv InpFs)) -defined Result ((action_at iv),(FreeEnv InpFs)) -valued Function-like V18( Args ((action_at iv),(FreeEnv InpFs)), Result ((action_at iv),(FreeEnv InpFs))) Element of bool [:(Args ((action_at iv),(FreeEnv InpFs))),(Result ((action_at iv),(FreeEnv InpFs))):]
[:(Args ((action_at iv),(FreeEnv InpFs))),(Result ((action_at iv),(FreeEnv InpFs))):] is Relation-like set
bool [:(Args ((action_at iv),(FreeEnv InpFs))),(Result ((action_at iv),(FreeEnv InpFs))):] is set
(Den ((action_at iv),(FreeEnv InpFs))) . p is Element of Result ((action_at iv),(FreeEnv InpFs))
((Eval InpFs) . (the_result_sort_of (action_at iv))) . ((Den ((action_at iv),(FreeEnv InpFs))) . p) is set
Result ((action_at iv),InpFs) is non empty Element of rng the Sorts of InpFs
rng the Sorts of InpFs is non empty set
Den ((action_at iv),InpFs) is Relation-like Args ((action_at iv),InpFs) -defined Result ((action_at iv),InpFs) -valued Function-like V18( Args ((action_at iv),InpFs), Result ((action_at iv),InpFs)) Element of bool [:(Args ((action_at iv),InpFs)),(Result ((action_at iv),InpFs)):]
[:(Args ((action_at iv),InpFs)),(Result ((action_at iv),InpFs)):] is Relation-like set
bool [:(Args ((action_at iv),InpFs)),(Result ((action_at iv),InpFs)):] is set
ods is Relation-like Function-like Element of Args ((action_at iv),InpFs)
(Den ((action_at iv),InpFs)) . ods is Element of Result ((action_at iv),InpFs)
FreeSort the Sorts of InpFs is Relation-like non-empty non empty-yielding the carrier of IIG -defined Function-like non empty total set
FreeOper the Sorts of InpFs is Relation-like the carrier' of IIG -defined Function-like non empty total Function-yielding V42() ManySortedFunction of the Arity of IIG * ((FreeSort the Sorts of InpFs) #), the ResultSort of IIG * (FreeSort the Sorts of InpFs)
(FreeSort the Sorts of InpFs) # is Relation-like the carrier of IIG * -defined Function-like non empty total set
the Arity of IIG * ((FreeSort the Sorts of InpFs) #) is Relation-like the carrier' of IIG -defined Function-like non empty total set
the ResultSort of IIG * (FreeSort the Sorts of InpFs) is Relation-like non-empty non empty-yielding the carrier' of IIG -defined Function-like non empty total set
MSAlgebra(# (FreeSort the Sorts of InpFs),(FreeOper the Sorts of InpFs) #) is strict MSAlgebra over IIG
(FreeOper the Sorts of InpFs) . (action_at iv) is Relation-like ( the Arity of IIG * ((FreeSort the Sorts of InpFs) #)) . (action_at iv) -defined ( the ResultSort of IIG * (FreeSort the Sorts of InpFs)) . (action_at iv) -valued Function-like V18(( the Arity of IIG * ((FreeSort the Sorts of InpFs) #)) . (action_at iv),( the ResultSort of IIG * (FreeSort the Sorts of InpFs)) . (action_at iv)) Element of bool [:(( the Arity of IIG * ((FreeSort the Sorts of InpFs) #)) . (action_at iv)),(( the ResultSort of IIG * (FreeSort the Sorts of InpFs)) . (action_at iv)):]
( the Arity of IIG * ((FreeSort the Sorts of InpFs) #)) . (action_at iv) is set
( the ResultSort of IIG * (FreeSort the Sorts of InpFs)) . (action_at iv) is non empty set
[:(( the Arity of IIG * ((FreeSort the Sorts of InpFs) #)) . (action_at iv)),(( the ResultSort of IIG * (FreeSort the Sorts of InpFs)) . (action_at iv)):] is Relation-like set
bool [:(( the Arity of IIG * ((FreeSort the Sorts of InpFs) #)) . (action_at iv)),(( the ResultSort of IIG * (FreeSort the Sorts of InpFs)) . (action_at iv)):] is set
DenOp ((action_at iv), the Sorts of InpFs) is Relation-like ( the Arity of IIG * ((FreeSort the Sorts of InpFs) #)) . (action_at iv) -defined ( the ResultSort of IIG * (FreeSort the Sorts of InpFs)) . (action_at iv) -valued Function-like V18(( the Arity of IIG * ((FreeSort the Sorts of InpFs) #)) . (action_at iv),( the ResultSort of IIG * (FreeSort the Sorts of InpFs)) . (action_at iv)) Element of bool [:(( the Arity of IIG * ((FreeSort the Sorts of InpFs) #)) . (action_at iv)),(( the ResultSort of IIG * (FreeSort the Sorts of InpFs)) . (action_at iv)):]
SCS is Relation-like NAT -defined Function-like finite countable FinSequence-like FinSubsequence-like DTree-yielding set
DTConMSA the Sorts of InpFs is non empty strict with_terminals with_nonterminals with_useful_nonterminals L13()
the carrier of (DTConMSA the Sorts of InpFs) is non empty set
FinTrees the carrier of (DTConMSA the Sorts of InpFs) is functional non empty constituted-DTrees DTree-set of the carrier of (DTConMSA the Sorts of InpFs)
TS (DTConMSA the Sorts of InpFs) is functional constituted-DTrees Element of bool (FinTrees the carrier of (DTConMSA the Sorts of InpFs))
bool (FinTrees the carrier of (DTConMSA the Sorts of InpFs)) is set
Sym ((action_at iv), the Sorts of InpFs) is Element of K355((DTConMSA the Sorts of InpFs))
K355((DTConMSA the Sorts of InpFs)) is non empty Element of bool the carrier of (DTConMSA the Sorts of InpFs)
bool the carrier of (DTConMSA the Sorts of InpFs) is set
p is Relation-like NAT -defined FinTrees the carrier of (DTConMSA the Sorts of InpFs) -valued Function-like finite countable Function-yielding V42() FinSequence-like FinSubsequence-like FinSequence of TS (DTConMSA the Sorts of InpFs)
roots p is Relation-like NAT -defined the carrier of (DTConMSA the Sorts of InpFs) -valued Function-like finite countable FinSequence-like FinSubsequence-like FinSequence of the carrier of (DTConMSA the Sorts of InpFs)
(Den ((action_at iv),(FreeEnv InpFs))) . {} is set
(Sym ((action_at iv), the Sorts of InpFs)) -tree SCS is Relation-like Function-like DecoratedTree-like set
[(action_at iv), the carrier of IIG] -tree {} is Relation-like Function-like DecoratedTree-like set
dom (Den ((action_at iv),InpFs)) is set
rng (Den ((action_at iv),InpFs)) is set
the ResultSort of IIG * the Sorts of InpFs 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 InpFs) . (action_at iv) is non empty set
the ResultSort of IIG . (action_at iv) is Element of the carrier of IIG
the Sorts of InpFs . ( the ResultSort of IIG . (action_at iv)) is non empty set
Constants (InpFs,iv) is Element of bool ( the Sorts of InpFs . iv)
bool ( the Sorts of InpFs . iv) is set
p9 is Element of the Sorts of InpFs . iv
Fp is non empty set
{ b₁ where b₁ is Element of Fp : ex b₂ being Element of the carrier' of IIG st
( the Arity of IIG . b₂ = {} & the ResultSort of IIG . b₂ = iv & b₁ in rng (Den (b₂,InpFs)) ) } is set
size (iv,InpFs) is V21() V22() V23() V27() finite cardinal countable V133() V134() ext-real set
(IIG,InpFs,dSCS) is Relation-like the carrier of IIG -defined Function-like non empty total Function-yielding V42() ManySortedFunction of the Sorts of (FreeEnv InpFs), the Sorts of (FreeEnv InpFs)
(IIG,InpFs,dSCS) . iv is Relation-like the Sorts of (FreeEnv InpFs) . iv -defined the Sorts of (FreeEnv InpFs) . iv -valued Function-like V18( the Sorts of (FreeEnv InpFs) . iv, the Sorts of (FreeEnv InpFs) . iv) finite countable Element of bool [:( the Sorts of (FreeEnv InpFs) . iv),( the Sorts of (FreeEnv InpFs) . iv):]
[:( the Sorts of (FreeEnv InpFs) . iv),( the Sorts of (FreeEnv InpFs) . iv):] is Relation-like finite countable set
bool [:( the Sorts of (FreeEnv InpFs) . iv),( the Sorts of (FreeEnv InpFs) . iv):] is finite V32() countable set
Fp is Relation-like Function-like non empty finite countable DecoratedTree-like Element of the Sorts of (FreeEnv InpFs) . iv
card Fp is non empty V21() V22() V23() V27() finite cardinal countable V133() V134() ext-real V148() V149() V150() V151() V152() V153() V154() V155() V161() V162() V163() V164() V165() Element of NAT
((IIG,InpFs,dSCS) . iv) . Fp is Relation-like Function-like non empty finite countable DecoratedTree-like Element of the Sorts of (FreeEnv InpFs) . iv
IIG is non empty non void V56() Circuit-like ManySortedSign
the carrier of IIG is non empty set
SCS is non-empty finitely-generated finite-yielding MSAlgebra over IIG
the Sorts of SCS is Relation-like non-empty non empty-yielding the carrier of IIG -defined Function-like non empty total set
product the Sorts of SCS is functional non empty with_common_domain product-like 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 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
K539( the carrier of IIG, the ResultSort of IIG) is Element of bool the carrier of IIG
the carrier of IIG \ K539( the carrier of IIG, the ResultSort of IIG) is Element of bool the carrier of IIG
InpFs is Relation-like the carrier of IIG -defined Function-like the Sorts of SCS -compatible non empty total Element of product the Sorts of SCS
InnerVertices IIG is non empty Element of bool the carrier of IIG
iv is Relation-like the carrier of IIG -defined Function-like non empty total set
dSCS is set
dom the Sorts of SCS is non empty set
s1 is Element of the carrier of IIG
iv . s1 is set
InpFs . s1 is set
iv . dSCS is set
the Sorts of SCS . dSCS is set
s1 is Element of the carrier of IIG
(InputVertices IIG) \/ (InnerVertices IIG) is non empty Element of bool the carrier of IIG
action_at s1 is Element of the carrier' of IIG
the_result_sort_of (action_at s1) is Element of the carrier of IIG
iv . dSCS is set
Args ((action_at s1),SCS) is functional non empty Element of rng ( the Sorts of SCS #)
the Sorts of SCS # is Relation-like the carrier of IIG * -defined Function-like non empty total set
the carrier of IIG * is functional non empty FinSequence-membered M8( the carrier of IIG)
rng ( the Sorts of SCS #) is non empty set
Result ((action_at s1),SCS) is non empty Element of rng the Sorts of SCS
rng the Sorts of SCS is non empty set
Den ((action_at s1),SCS) is Relation-like Args ((action_at s1),SCS) -defined Result ((action_at s1),SCS) -valued Function-like V18( Args ((action_at s1),SCS), Result ((action_at s1),SCS)) Element of bool [:(Args ((action_at s1),SCS)),(Result ((action_at s1),SCS)):]
[:(Args ((action_at s1),SCS)),(Result ((action_at s1),SCS)):] is Relation-like set
bool [:(Args ((action_at s1),SCS)),(Result ((action_at s1),SCS)):] is set
(action_at s1) depends_on_in InpFs is Relation-like Function-like Element of Args ((action_at s1),SCS)
(Den ((action_at s1),SCS)) . ((action_at s1) depends_on_in InpFs) is Element of Result ((action_at s1),SCS)
the Sorts of SCS . dSCS is set
s1 is Element of the carrier of IIG
dom iv is non empty set
dSCS is Relation-like the carrier of IIG -defined Function-like the Sorts of SCS -compatible non empty total Element of product the Sorts of SCS
s1 is Element of the carrier of IIG
dSCS . s1 is set
InpFs . s1 is set
action_at s1 is Element of the carrier' of IIG
Args ((action_at s1),SCS) is functional non empty Element of rng ( the Sorts of SCS #)
the Sorts of SCS # is Relation-like the carrier of IIG * -defined Function-like non empty total set
the carrier of IIG * is functional non empty FinSequence-membered M8( the carrier of IIG)
rng ( the Sorts of SCS #) is non empty set
Result ((action_at s1),SCS) is non empty Element of rng the Sorts of SCS
rng the Sorts of SCS is non empty set
Den ((action_at s1),SCS) is Relation-like Args ((action_at s1),SCS) -defined Result ((action_at s1),SCS) -valued Function-like V18( Args ((action_at s1),SCS), Result ((action_at s1),SCS)) Element of bool [:(Args ((action_at s1),SCS)),(Result ((action_at s1),SCS)):]
[:(Args ((action_at s1),SCS)),(Result ((action_at s1),SCS)):] is Relation-like set
bool [:(Args ((action_at s1),SCS)),(Result ((action_at s1),SCS)):] is set
(action_at s1) depends_on_in InpFs is Relation-like Function-like Element of Args ((action_at s1),SCS)
(Den ((action_at s1),SCS)) . ((action_at s1) depends_on_in InpFs) is Element of Result ((action_at s1),SCS)
iv is Relation-like the carrier of IIG -defined Function-like the Sorts of SCS -compatible non empty total Element of product the Sorts of SCS
dSCS is Relation-like the carrier of IIG -defined Function-like the Sorts of SCS -compatible non empty total Element of product the Sorts of SCS
dom dSCS is non empty set
dom iv is non empty set
s1 is set
iv . s1 is set
dSCS . s1 is set
s2 is Element of the carrier of IIG
iv . s2 is set
action_at s2 is Element of the carrier' of IIG
Args ((action_at s2),SCS) is functional non empty Element of rng ( the Sorts of SCS #)
the Sorts of SCS # is Relation-like the carrier of IIG * -defined Function-like non empty total set
the carrier of IIG * is functional non empty FinSequence-membered M8( the carrier of IIG)
rng ( the Sorts of SCS #) is non empty set
Result ((action_at s2),SCS) is non empty Element of rng the Sorts of SCS
rng the Sorts of SCS is non empty set
Den ((action_at s2),SCS) is Relation-like Args ((action_at s2),SCS) -defined Result ((action_at s2),SCS) -valued Function-like V18( Args ((action_at s2),SCS), Result ((action_at s2),SCS)) Element of bool [:(Args ((action_at s2),SCS)),(Result ((action_at s2),SCS)):]
[:(Args ((action_at s2),SCS)),(Result ((action_at s2),SCS)):] is Relation-like set
bool [:(Args ((action_at s2),SCS)),(Result ((action_at s2),SCS)):] is set
(action_at s2) depends_on_in InpFs is Relation-like Function-like Element of Args ((action_at s2),SCS)
(Den ((action_at s2),SCS)) . ((action_at s2) depends_on_in InpFs) is Element of Result ((action_at s2),SCS)
(InputVertices IIG) \/ (InnerVertices IIG) is non empty Element of bool the carrier of IIG
InpFs . s2 is set
IIG is non empty non void V56() 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 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
K539( the carrier of IIG, the ResultSort of IIG) is Element of bool the carrier of IIG
the carrier of IIG \ K539( the carrier of IIG, the ResultSort of IIG) is Element of bool the carrier of IIG
SCS is non-empty finitely-generated finite-yielding MSAlgebra over IIG
the Sorts of SCS is Relation-like non-empty non empty-yielding the carrier of IIG -defined Function-like non empty total set
product the Sorts of SCS is functional non empty with_common_domain product-like set
InpFs is Relation-like the carrier of IIG -defined Function-like the Sorts of SCS -compatible non empty total Element of product the Sorts of SCS
(IIG,SCS,InpFs) is Relation-like the carrier of IIG -defined Function-like the Sorts of SCS -compatible non empty total Element of product the Sorts of SCS
iv is Relation-like InputVertices IIG -defined Function-like total InputValues of SCS
dom InpFs is non empty set
dom (IIG,SCS,InpFs) is non empty set
dom iv is set
dSCS is set
s1 is Element of the carrier of IIG
iv . s1 is set
InpFs . s1 is set
iv . dSCS is set
(IIG,SCS,InpFs) . dSCS is set
IIG is non empty non void V56() Circuit-like ManySortedSign
the carrier of IIG is non empty set
SCS is non-empty finitely-generated finite-yielding MSAlgebra over IIG
the Sorts of SCS is Relation-like non-empty non empty-yielding the carrier of IIG -defined Function-like non empty total set
product the Sorts of SCS is functional non empty with_common_domain product-like set
IIG is non empty non void V56() Circuit-like monotonic ManySortedSign
the carrier of IIG is non empty set
SCS is non-empty finitely-generated finite-yielding MSAlgebra over IIG
the Sorts of SCS is Relation-like non-empty non empty-yielding the carrier of IIG -defined Function-like non empty total set
product the Sorts of SCS is functional non empty with_common_domain product-like 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 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
K539( the carrier of IIG, the ResultSort of IIG) is Element of bool the carrier of IIG
the carrier of IIG \ K539( the carrier of IIG, the ResultSort of IIG) is Element of bool the carrier of IIG
InpFs is Relation-like the carrier of IIG -defined Function-like the Sorts of SCS -compatible non empty total Element of product the Sorts of SCS
iv is Relation-like InputVertices IIG -defined Function-like total InputValues of SCS
(IIG,SCS,InpFs,iv) is Relation-like the carrier of IIG -defined Function-like the Sorts of SCS -compatible non empty total Element of product the Sorts of SCS
(IIG,SCS,(IIG,SCS,InpFs,iv)) is Relation-like the carrier of IIG -defined Function-like the Sorts of SCS -compatible non empty total Element of product the Sorts of SCS
IIG is non empty non void V56() Circuit-like monotonic 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 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
K539( the carrier of IIG, the ResultSort of IIG) is Element of bool the carrier of IIG
the carrier of IIG \ K539( the carrier of IIG, the ResultSort of IIG) is Element of bool the carrier of IIG
(InputVertices IIG) --> NAT is Relation-like non-empty InputVertices IIG -defined {NAT} -valued Function-like constant 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
SCS is non-empty finitely-generated finite-yielding MSAlgebra over IIG
the Sorts of SCS is Relation-like non-empty non empty-yielding the carrier of IIG -defined Function-like non empty total set
the Sorts of SCS | (InputVertices IIG) is Relation-like non-empty InputVertices IIG -defined the carrier of IIG -defined InputVertices IIG -defined Function-like total set
product the Sorts of SCS is functional non empty with_common_domain product-like set
iv is Relation-like the carrier of IIG -defined Function-like the Sorts of SCS -compatible non empty total Element of product the Sorts of SCS
InpFs is Relation-like InputVertices IIG -defined Function-like total Function-yielding V42() ManySortedFunction of (InputVertices IIG) --> NAT, the Sorts of SCS | (InputVertices IIG)
0 -th_InputValues InpFs is Relation-like InputVertices IIG -defined Function-like total InputValues of SCS
(IIG,SCS,iv,(0 -th_InputValues InpFs)) is Relation-like the carrier of IIG -defined Function-like the Sorts of SCS -compatible non empty total Element of product the Sorts of SCS
Set-Constants SCS is Relation-like SortsWithConstants IIG -defined Function-like total set
SortsWithConstants IIG is Element of bool the carrier of IIG
(IIG,SCS,iv,(0 -th_InputValues InpFs)) +* (Set-Constants SCS) is Relation-like Function-like set
dom (Set-Constants SCS) is set
s1 is set
(Set-Constants SCS) . s1 is set
s2 is Element of the carrier of IIG
Constants (SCS,s2) is Element of bool ( the Sorts of SCS . s2)
the Sorts of SCS . s2 is non empty set
bool ( the Sorts of SCS . s2) is set
the Sorts of SCS . s1 is set
dom the Sorts of SCS is non empty set
IIG is non empty non void V56() Circuit-like monotonic 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 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
K539( the carrier of IIG, the ResultSort of IIG) is Element of bool the carrier of IIG
the carrier of IIG \ K539( the carrier of IIG, the ResultSort of IIG) is Element of bool the carrier of IIG
(InputVertices IIG) --> NAT is Relation-like non-empty InputVertices IIG -defined {NAT} -valued Function-like constant total V18( InputVertices IIG,{NAT}) Cardinal-yielding Element of bool [:(InputVertices IIG),{NAT}:]
[:(InputVertices IIG),{NAT}:] is Relation-like set
bool [:(InputVertices IIG),{NAT}:] is set
SCS is non-empty finitely-generated finite-yielding MSAlgebra over IIG
the Sorts of SCS is Relation-like non-empty non empty-yielding the carrier of IIG -defined Function-like non empty total set
the Sorts of SCS | (InputVertices IIG) is Relation-like non-empty InputVertices IIG -defined the carrier of IIG -defined InputVertices IIG -defined Function-like total set
product the Sorts of SCS is functional non empty with_common_domain product-like set
[:NAT,(product the Sorts of SCS):] is Relation-like non trivial non finite set
bool [:NAT,(product the Sorts of SCS):] is non trivial non finite set
InpFs is Relation-like InputVertices IIG -defined Function-like total Function-yielding V42() ManySortedFunction of (InputVertices IIG) --> NAT, the Sorts of SCS | (InputVertices IIG)
iv is Relation-like the carrier of IIG -defined Function-like the Sorts of SCS -compatible non empty total Element of product the Sorts of SCS
(IIG,SCS,InpFs,iv) is Relation-like the carrier of IIG -defined Function-like the Sorts of SCS -compatible non empty total Element of product the Sorts of SCS
0 -th_InputValues InpFs is Relation-like InputVertices IIG -defined Function-like total InputValues of SCS
(IIG,SCS,iv,(0 -th_InputValues InpFs)) is Relation-like the carrier of IIG -defined Function-like the Sorts of SCS -compatible non empty total Element of product the Sorts of SCS
Set-Constants SCS is Relation-like SortsWithConstants IIG -defined Function-like total set
SortsWithConstants IIG is Element of bool the carrier of IIG
(IIG,SCS,iv,(0 -th_InputValues InpFs)) +* (Set-Constants SCS) is Relation-like Function-like set
IIG is non empty non void V56() 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 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
K539( the carrier of IIG, the ResultSort of IIG) is Element of bool the carrier of IIG
the carrier of IIG \ K539( the carrier of IIG, the ResultSort of IIG) is Element of bool the carrier of IIG
SCS is non-empty finitely-generated finite-yielding MSAlgebra over IIG
the Sorts of SCS is Relation-like non-empty non empty-yielding the carrier of IIG -defined Function-like non empty total set
product the Sorts of SCS is functional non empty with_common_domain product-like set
InpFs is Relation-like the carrier of IIG -defined Function-like the Sorts of SCS -compatible non empty total Element of product the Sorts of SCS
(IIG,SCS,InpFs) is Relation-like the carrier of IIG -defined Function-like the Sorts of SCS -compatible non empty total Element of product the Sorts of SCS
iv is Relation-like InputVertices IIG -defined Function-like total InputValues of SCS
dSCS is V21() V22() V23() V27() finite cardinal countable V133() V134() ext-real V148() V149() V150() V151() V152() V153() V154() V155() V163() V164() V165() Element of NAT
dSCS + 1 is V21() V22() V23() V27() finite cardinal countable V133() V134() ext-real V148() V149() V150() V151() V152() V153() V154() V155() V163() V164() V165() Element of NAT
s1 is Element of the carrier of IIG
depth (s1,SCS) is V21() V22() V23() V27() finite cardinal countable V133() V134() ext-real set
(IIG,SCS,InpFs) . s1 is set
(IIG,SCS,s1,iv) is Element of the Sorts of SCS . s1
the Sorts of SCS . s1 is non empty set
FreeEnv SCS is strict non-empty free MSAlgebra over IIG
FreeMSA the Sorts of SCS is strict non-empty MSAlgebra over IIG
the Sorts of (FreeEnv SCS) is Relation-like non-empty non empty-yielding the carrier of IIG -defined Function-like non empty total set
the Sorts of (FreeEnv SCS) . s1 is non empty finite countable set
Eval SCS is Relation-like the carrier of IIG -defined Function-like non empty total Function-yielding V42() ManySortedFunction of the Sorts of (FreeEnv SCS), the Sorts of SCS
(Eval SCS) . s1 is Relation-like the Sorts of (FreeEnv SCS) . s1 -defined the Sorts of SCS . s1 -valued Function-like V18( the Sorts of (FreeEnv SCS) . s1, the Sorts of SCS . s1) finite countable Element of bool [:( the Sorts of (FreeEnv SCS) . s1),( the Sorts of SCS . s1):]
[:( the Sorts of (FreeEnv SCS) . s1),( the Sorts of SCS . s1):] is Relation-like set
bool [:( the Sorts of (FreeEnv SCS) . s1),( the Sorts of SCS . s1):] is set
(IIG,SCS,s1,iv) is Relation-like Function-like non empty finite countable DecoratedTree-like Element of the Sorts of (FreeEnv SCS) . s1
((Eval SCS) . s1) . (IIG,SCS,s1,iv) is Element of the Sorts of SCS . s1
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
InpFs . s1 is set
action_at s1 is Element of the carrier' of IIG
the_arity_of (action_at s1) is Relation-like NAT -defined the carrier of IIG -valued Function-like finite countable FinSequence-like FinSubsequence-like Element of the carrier of IIG *
the carrier of IIG * is functional non empty FinSequence-membered M8( the carrier of IIG)
len (the_arity_of (action_at s1)) is V21() V22() V23() V27() finite cardinal countable V133() V134() ext-real V148() V149() V150() V151() V152() V153() V154() V155() V163() V164() V165() Element of NAT
p is Relation-like NAT -defined Function-like finite countable FinSequence-like FinSubsequence-like set
len p is V21() V22() V23() V27() finite cardinal countable V133() V134() ext-real V148() V149() V150() V151() V152() V153() V154() V155() V163() V164() V165() Element of NAT
dom p is finite countable V150() V151() V152() V153() V154() V155() V163() V164() V165() Element of bool NAT
ods is V21() V22() V23() V27() finite cardinal countable V133() V134() ext-real V148() V149() V150() V151() V152() V153() V154() V155() V163() V164() V165() Element of NAT
p . ods is set
(the_arity_of (action_at s1)) /. ods is Element of the carrier of IIG
(IIG,SCS,((the_arity_of (action_at s1)) /. ods),iv) is Relation-like Function-like non empty finite countable DecoratedTree-like Element of the Sorts of (FreeEnv SCS) . ((the_arity_of (action_at s1)) /. ods)
the Sorts of (FreeEnv SCS) . ((the_arity_of (action_at s1)) /. ods) is non empty finite countable set
ods is V21() V22() V23() V27() finite cardinal countable V133() V134() ext-real set
p . ods is set
(the_arity_of (action_at s1)) /. ods is Element of the carrier of IIG
(IIG,SCS,((the_arity_of (action_at s1)) /. ods),iv) is Relation-like Function-like non empty finite countable DecoratedTree-like Element of the Sorts of (FreeEnv SCS) . ((the_arity_of (action_at s1)) /. ods)
the Sorts of (FreeEnv SCS) . ((the_arity_of (action_at s1)) /. ods) is non empty finite countable set
FreeSort the Sorts of SCS is Relation-like non-empty non empty-yielding the carrier of IIG -defined Function-like non empty total set
FreeOper the Sorts of SCS is Relation-like the carrier' of IIG -defined Function-like non empty total Function-yielding V42() ManySortedFunction of the Arity of IIG * ((FreeSort the Sorts of SCS) #), the ResultSort of IIG * (FreeSort the Sorts of SCS)
the Arity of IIG is Relation-like the carrier' of IIG -defined the carrier of IIG * -valued Function-like V18( the carrier' of IIG, the carrier of IIG * ) Function-yielding V42() 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 SCS) # is Relation-like the carrier of IIG * -defined Function-like non empty total set
the Arity of IIG * ((FreeSort the Sorts of SCS) #) is Relation-like the carrier' of IIG -defined Function-like non empty total set
the ResultSort of IIG * (FreeSort the Sorts of SCS) is Relation-like non-empty non empty-yielding the carrier' of IIG -defined Function-like non empty total set
MSAlgebra(# (FreeSort the Sorts of SCS),(FreeOper the Sorts of SCS) #) is strict MSAlgebra over IIG
Den ((action_at s1),(FreeEnv SCS)) is Relation-like Args ((action_at s1),(FreeEnv SCS)) -defined Result ((action_at s1),(FreeEnv SCS)) -valued Function-like V18( Args ((action_at s1),(FreeEnv SCS)), Result ((action_at s1),(FreeEnv SCS))) Element of bool [:(Args ((action_at s1),(FreeEnv SCS))),(Result ((action_at s1),(FreeEnv SCS))):]
Args ((action_at s1),(FreeEnv SCS)) is functional non empty Element of rng ( the Sorts of (FreeEnv SCS) #)
the Sorts of (FreeEnv SCS) # is Relation-like the carrier of IIG * -defined Function-like non empty total set
rng ( the Sorts of (FreeEnv SCS) #) is non empty set
Result ((action_at s1),(FreeEnv SCS)) is non empty Element of rng the Sorts of (FreeEnv SCS)
rng the Sorts of (FreeEnv SCS) is non empty set
[:(Args ((action_at s1),(FreeEnv SCS))),(Result ((action_at s1),(FreeEnv SCS))):] is Relation-like set
bool [:(Args ((action_at s1),(FreeEnv SCS))),(Result ((action_at s1),(FreeEnv SCS))):] is set
(FreeOper the Sorts of SCS) . (action_at s1) is Relation-like ( the Arity of IIG * ((FreeSort the Sorts of SCS) #)) . (action_at s1) -defined ( the ResultSort of IIG * (FreeSort the Sorts of SCS)) . (action_at s1) -valued Function-like V18(( the Arity of IIG * ((FreeSort the Sorts of SCS) #)) . (action_at s1),( the ResultSort of IIG * (FreeSort the Sorts of SCS)) . (action_at s1)) Element of bool [:(( the Arity of IIG * ((FreeSort the Sorts of SCS) #)) . (action_at s1)),(( the ResultSort of IIG * (FreeSort the Sorts of SCS)) . (action_at s1)):]
( the Arity of IIG * ((FreeSort the Sorts of SCS) #)) . (action_at s1) is set
( the ResultSort of IIG * (FreeSort the Sorts of SCS)) . (action_at s1) is non empty set
[:(( the Arity of IIG * ((FreeSort the Sorts of SCS) #)) . (action_at s1)),(( the ResultSort of IIG * (FreeSort the Sorts of SCS)) . (action_at s1)):] is Relation-like set
bool [:(( the Arity of IIG * ((FreeSort the Sorts of SCS) #)) . (action_at s1)),(( the ResultSort of IIG * (FreeSort the Sorts of SCS)) . (action_at s1)):] is set
DenOp ((action_at s1), the Sorts of SCS) is Relation-like ( the Arity of IIG * ((FreeSort the Sorts of SCS) #)) . (action_at s1) -defined ( the ResultSort of IIG * (FreeSort the Sorts of SCS)) . (action_at s1) -valued Function-like V18(( the Arity of IIG * ((FreeSort the Sorts of SCS) #)) . (action_at s1),( the ResultSort of IIG * (FreeSort the Sorts of SCS)) . (action_at s1)) Element of bool [:(( the Arity of IIG * ((FreeSort the Sorts of SCS) #)) . (action_at s1)),(( the ResultSort of IIG * (FreeSort the Sorts of SCS)) . (action_at s1)):]
(action_at s1) depends_on_in InpFs is Relation-like Function-like Element of Args ((action_at s1),SCS)
Args ((action_at s1),SCS) is functional non empty Element of rng ( the Sorts of SCS #)
the Sorts of SCS # is Relation-like the carrier of IIG * -defined Function-like non empty total set
rng ( the Sorts of SCS #) is non empty set
dom the Arity of IIG is set
the Arity of IIG * ( the Sorts of SCS #) is Relation-like the carrier' of IIG -defined Function-like non empty total set
( the Arity of IIG * ( the Sorts of SCS #)) . (action_at s1) is set
the Arity of IIG . (action_at s1) is Relation-like NAT -defined Function-like finite countable FinSequence-like FinSubsequence-like Element of the carrier of IIG *
( the Sorts of SCS #) . ( the Arity of IIG . (action_at s1)) is set
( the Sorts of SCS #) . (the_arity_of (action_at s1)) is set
(the_arity_of (action_at s1)) * the Sorts of SCS is Relation-like non-empty NAT -defined Function-like finite countable set
product ((the_arity_of (action_at s1)) * the Sorts of SCS) is functional non empty with_common_domain product-like set
dom (the_arity_of (action_at s1)) is finite countable V150() V151() V152() V153() V154() V155() V163() V164() V165() Element of bool NAT
the Arity of IIG * ( the Sorts of (FreeEnv SCS) #) is Relation-like the carrier' of IIG -defined Function-like non empty total set
( the Arity of IIG * ( the Sorts of (FreeEnv SCS) #)) . (action_at s1) is set
DTConMSA the Sorts of SCS is non empty strict with_terminals with_nonterminals with_useful_nonterminals L13()
the carrier of (DTConMSA the Sorts of SCS) is non empty set
FinTrees the carrier of (DTConMSA the Sorts of SCS) is functional non empty constituted-DTrees DTree-set of the carrier of (DTConMSA the Sorts of SCS)
TS (DTConMSA the Sorts of SCS) is functional constituted-DTrees Element of bool (FinTrees the carrier of (DTConMSA the Sorts of SCS))
bool (FinTrees the carrier of (DTConMSA the Sorts of SCS)) is set
p is Relation-like Function-like Element of Args ((action_at s1),(FreeEnv SCS))
Sym ((action_at s1), the Sorts of SCS) is Element of K355((DTConMSA the Sorts of SCS))
K355((DTConMSA the Sorts of SCS)) is non empty Element of bool the carrier of (DTConMSA the Sorts of SCS)
bool the carrier of (DTConMSA the Sorts of SCS) is set
p9 is Relation-like NAT -defined FinTrees the carrier of (DTConMSA the Sorts of SCS) -valued Function-like finite countable Function-yielding V42() FinSequence-like FinSubsequence-like FinSequence of TS (DTConMSA the Sorts of SCS)
roots p9 is Relation-like NAT -defined the carrier of (DTConMSA the Sorts of SCS) -valued Function-like finite countable FinSequence-like FinSubsequence-like FinSequence of the carrier of (DTConMSA the Sorts of SCS)
(Den ((action_at s1),(FreeEnv SCS))) . p is Element of Result ((action_at s1),(FreeEnv SCS))
(Sym ((action_at s1), the Sorts of SCS)) -tree p9 is Relation-like the carrier of (DTConMSA the Sorts of SCS) -valued Function-like finite countable DecoratedTree-like Element of FinTrees the carrier of (DTConMSA the Sorts of SCS)
[(action_at s1), the carrier of IIG] is set
[(action_at s1), the carrier of IIG] -tree p9 is Relation-like Function-like DecoratedTree-like set
(Eval SCS) # p is Relation-like Function-like Element of Args ((action_at s1),SCS)
dom the Sorts of SCS is non empty set
rng (the_arity_of (action_at s1)) is finite countable set
dom ((the_arity_of (action_at s1)) * the Sorts of SCS) is finite countable set
Fp is Relation-like Function-like set
dom Fp is set
dom InpFs is non empty set
(the_arity_of (action_at s1)) * InpFs is Relation-like NAT -defined Function-like finite countable set
dom ((the_arity_of (action_at s1)) * InpFs) is finite countable set
ods is Relation-like Function-like set
dom ods is set
x is set
(the_arity_of (action_at s1)) /. x is Element of the carrier of IIG
v1 is Element of the carrier of IIG
x9 is V21() V22() V23() V27() finite cardinal countable V133() V134() ext-real V148() V149() V150() V151() V152() V153() V154() V155() V163() V164() V165() Element of NAT
(the_arity_of (action_at s1)) . x9 is set
depth (v1,SCS) is V21() V22() V23() V27() finite cardinal countable V133() V134() ext-real set
Fp . x is set
(Eval SCS) . v1 is Relation-like the Sorts of (FreeEnv SCS) . v1 -defined the Sorts of SCS . v1 -valued Function-like V18( the Sorts of (FreeEnv SCS) . v1, the Sorts of SCS . v1) finite countable Element of bool [:( the Sorts of (FreeEnv SCS) . v1),( the Sorts of SCS . v1):]
the Sorts of (FreeEnv SCS) . v1 is non empty finite countable set
the Sorts of SCS . v1 is non empty set
[:( the Sorts of (FreeEnv SCS) . v1),( the Sorts of SCS . v1):] is Relation-like set
bool [:( the Sorts of (FreeEnv SCS) . v1),( the Sorts of SCS . v1):] is set
p9 . x9 is Relation-like Function-like set
((Eval SCS) . v1) . (p9 . x9) is set
(IIG,SCS,v1,iv) is Element of the Sorts of SCS . v1
(IIG,SCS,v1,iv) is Relation-like Function-like non empty finite countable DecoratedTree-like Element of the Sorts of (FreeEnv SCS) . v1
((Eval SCS) . v1) . (IIG,SCS,v1,iv) is Element of the Sorts of SCS . v1
InpFs . v1 is set
((the_arity_of (action_at s1)) * InpFs) . x is set
ods . x is set
Result ((action_at s1),SCS) is non empty Element of rng the Sorts of SCS
rng the Sorts of SCS is non empty set
Den ((action_at s1),SCS) is Relation-like Args ((action_at s1),SCS) -defined Result ((action_at s1),SCS) -valued Function-like V18( Args ((action_at s1),SCS), Result ((action_at s1),SCS)) Element of bool [:(Args ((action_at s1),SCS)),(Result ((action_at s1),SCS)):]
[:(Args ((action_at s1),SCS)),(Result ((action_at s1),SCS)):] is Relation-like set
bool [:(Args ((action_at s1),SCS)),(Result ((action_at s1),SCS)):] is set
(Den ((action_at s1),SCS)) . ((Eval SCS) # p) is Element of Result ((action_at s1),SCS)
the_result_sort_of (action_at s1) is Element of the carrier of IIG
(Eval SCS) . (the_result_sort_of (action_at s1)) is Relation-like the Sorts of (FreeEnv SCS) . (the_result_sort_of (action_at s1)) -defined the Sorts of SCS . (the_result_sort_of (action_at s1)) -valued Function-like V18( the Sorts of (FreeEnv SCS) . (the_result_sort_of (action_at s1)), the Sorts of SCS . (the_result_sort_of (action_at s1))) finite countable Element of bool [:( the Sorts of (FreeEnv SCS) . (the_result_sort_of (action_at s1))),( the Sorts of SCS . (the_result_sort_of (action_at s1))):]
the Sorts of (FreeEnv SCS) . (the_result_sort_of (action_at s1)) is non empty finite countable set
the Sorts of SCS . (the_result_sort_of (action_at s1)) is non empty set
[:( the Sorts of (FreeEnv SCS) . (the_result_sort_of (action_at s1))),( the Sorts of SCS . (the_result_sort_of (action_at s1))):] is Relation-like set
bool [:( the Sorts of (FreeEnv SCS) . (the_result_sort_of (action_at s1))),( the Sorts of SCS . (the_result_sort_of (action_at s1))):] is set
((Eval SCS) . (the_result_sort_of (action_at s1))) . ((Den ((action_at s1),(FreeEnv SCS))) . p) is set
IIG is non empty finite non void V56() Circuit-like monotonic ManySortedSign
InputVertices IIG is finite countable Element of bool the carrier of IIG
the carrier of IIG is non empty finite countable set
bool the carrier of IIG is finite V32() countable set
the ResultSort of IIG is Relation-like the carrier' of IIG -defined the carrier of IIG -valued Function-like 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
K539( the carrier of IIG, the ResultSort of IIG) is finite countable Element of bool the carrier of IIG
the carrier of IIG \ K539( the carrier of IIG, the ResultSort of IIG) is finite countable Element of bool the carrier of IIG
(InputVertices IIG) --> NAT is Relation-like non-empty InputVertices IIG -defined {NAT} -valued Function-like constant total V18( InputVertices IIG,{NAT}) finite Cardinal-yielding countable Element of bool [:(InputVertices IIG),{NAT}:]
[:(InputVertices IIG),{NAT}:] is Relation-like finite countable set
bool [:(InputVertices IIG),{NAT}:] is finite V32() countable set
SCS is non-empty finitely-generated finite-yielding MSAlgebra over IIG
the Sorts of SCS is Relation-like non-empty non empty-yielding the carrier of IIG -defined Function-like non empty total set
the Sorts of SCS | (InputVertices IIG) is Relation-like non-empty InputVertices IIG -defined the carrier of IIG -defined InputVertices IIG -defined Function-like total finite countable set
product the Sorts of SCS is functional non empty with_common_domain product-like set
InpFs is Relation-like InputVertices IIG -defined Function-like total Function-yielding V42() ManySortedFunction of (InputVertices IIG) --> NAT, the Sorts of SCS | (InputVertices IIG)
commute InpFs is Relation-like Function-like Function-yielding V42() set
(commute InpFs) . 0 is Relation-like Function-like set
dom (commute InpFs) is set
iv is Relation-like the carrier of IIG -defined Function-like the Sorts of SCS -compatible non empty total Element of product the Sorts of SCS
(IIG,SCS,InpFs,iv) is Relation-like NAT -defined product the Sorts of SCS -valued Function-like V18( NAT , product the Sorts of SCS) Function-yielding V42() Element of bool [:NAT,(product the Sorts of SCS):]
[:NAT,(product the Sorts of SCS):] is Relation-like non trivial non finite set
bool [:NAT,(product the Sorts of SCS):] is non trivial non finite set
dSCS is Relation-like InputVertices IIG -defined Function-like total InputValues of SCS
s1 is V21() V22() V23() V27() finite cardinal countable V133() V134() ext-real V148() V149() V150() V151() V152() V153() V154() V155() V163() V164() V165() Element of NAT
(IIG,SCS,InpFs,iv) . s1 is Relation-like the carrier of IIG -defined Function-like the Sorts of SCS -compatible non empty total Element of product the Sorts of SCS
s1 -th_InputValues InpFs is Relation-like InputVertices IIG -defined Function-like total InputValues of SCS
(commute InpFs) . s1 is Relation-like Function-like set
dom dSCS is set
Set-Constants SCS is Relation-like SortsWithConstants IIG -defined Function-like total set
SortsWithConstants IIG is finite countable Element of bool the carrier of IIG
dom (Set-Constants SCS) is set
(IIG,SCS,InpFs,iv) is Relation-like the carrier of IIG -defined Function-like the Sorts of SCS -compatible non empty total Element of product the Sorts of SCS
0 -th_InputValues InpFs is Relation-like InputVertices IIG -defined Function-like total InputValues of SCS
(IIG,SCS,iv,(0 -th_InputValues InpFs)) is Relation-like the carrier of IIG -defined Function-like the Sorts of SCS -compatible non empty total Element of product the Sorts of SCS
(IIG,SCS,iv,(0 -th_InputValues InpFs)) +* (Set-Constants SCS) is Relation-like Function-like set
Cs1 is V21() V22() V23() V27() finite cardinal countable V133() V134() ext-real set
Cs1 + 1 is V21() V22() V23() V27() finite cardinal countable V133() V134() ext-real V148() V149() V150() V151() V152() V153() V154() V155() V163() V164() V165() Element of NAT
Cs1 is V21() V22() V23() V27() finite cardinal countable V133() V134() ext-real set
Cs1 + 1 is V21() V22() V23() V27() finite cardinal countable V133() V134() ext-real V148() V149() V150() V151() V152() V153() V154() V155() V163() V164() V165() Element of NAT
Cs2 is V21() V22() V23() V27() finite cardinal countable V133() V134() ext-real V148() V149() V150() V151() V152() V153() V154() V155() V163() V164() V165() Element of NAT
(IIG,SCS,InpFs,iv) . Cs2 is Relation-like the carrier of IIG -defined Function-like the Sorts of SCS -compatible non empty total Element of product the Sorts of SCS
x is Relation-like the carrier of IIG -defined Function-like the Sorts of SCS -compatible non empty total Element of product the Sorts of SCS
(IIG,SCS,x,(s1 -th_InputValues InpFs)) is Relation-like the carrier of IIG -defined Function-like the Sorts of SCS -compatible non empty total Element of product the Sorts of SCS
(IIG,SCS,x,(s1 -th_InputValues InpFs)) is Relation-like the carrier of IIG -defined Function-like the Sorts of SCS -compatible non empty total Element of product the Sorts of SCS
(IIG,SCS,(IIG,SCS,x,(s1 -th_InputValues InpFs))) is Relation-like the carrier of IIG -defined Function-like the Sorts of SCS -compatible non empty total Element of product the Sorts of SCS
(IIG,SCS,x,dSCS) is Relation-like the carrier of IIG -defined Function-like the Sorts of SCS -compatible non empty total Element of product the Sorts of SCS
(IIG,SCS,(IIG,SCS,x,dSCS)) is Relation-like the carrier of IIG -defined Function-like the Sorts of SCS -compatible non empty total Element of product the Sorts of SCS
IIG is non empty finite non void V56() Circuit-like monotonic ManySortedSign
InputVertices IIG is finite countable Element of bool the carrier of IIG
the carrier of IIG is non empty finite countable set
bool the carrier of IIG is finite V32() countable set
the ResultSort of IIG is Relation-like the carrier' of IIG -defined the carrier of IIG -valued Function-like 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
K539( the carrier of IIG, the ResultSort of IIG) is finite countable Element of bool the carrier of IIG
the carrier of IIG \ K539( the carrier of IIG, the ResultSort of IIG) is finite countable Element of bool the carrier of IIG
(InputVertices IIG) --> NAT is Relation-like non-empty InputVertices IIG -defined {NAT} -valued Function-like constant total V18( InputVertices IIG,{NAT}) finite Cardinal-yielding countable Element of bool [:(InputVertices IIG),{NAT}:]
[:(InputVertices IIG),{NAT}:] is Relation-like finite countable set
bool [:(InputVertices IIG),{NAT}:] is finite V32() countable set
SCS is non-empty finitely-generated finite-yielding MSAlgebra over IIG
the Sorts of SCS is Relation-like non-empty non empty-yielding the carrier of IIG -defined Function-like non empty total set
the Sorts of SCS | (InputVertices IIG) is Relation-like non-empty InputVertices IIG -defined the carrier of IIG -defined InputVertices IIG -defined Function-like total finite countable set
product the Sorts of SCS is functional non empty with_common_domain product-like set
InpFs is Relation-like InputVertices IIG -defined Function-like total Function-yielding V42() ManySortedFunction of (InputVertices IIG) --> NAT, the Sorts of SCS | (InputVertices IIG)
commute InpFs is Relation-like Function-like Function-yielding V42() set
iv is Relation-like the carrier of IIG -defined Function-like the Sorts of SCS -compatible non empty total Element of product the Sorts of SCS
(IIG,SCS,InpFs,iv) is Relation-like NAT -defined product the Sorts of SCS -valued Function-like V18( NAT , product the Sorts of SCS) Function-yielding V42() Element of bool [:NAT,(product the Sorts of SCS):]
[:NAT,(product the Sorts of SCS):] is Relation-like non trivial non finite set
bool [:NAT,(product the Sorts of SCS):] is non trivial non finite set
dSCS is V21() V22() V23() V27() finite cardinal countable V133() V134() ext-real V148() V149() V150() V151() V152() V153() V154() V155() V163() V164() V165() Element of NAT
(IIG,SCS,InpFs,iv) . dSCS is Relation-like the carrier of IIG -defined Function-like the Sorts of SCS -compatible non empty total Element of product the Sorts of SCS
s1 is V21() V22() V23() V27() finite cardinal countable V133() V134() ext-real V148() V149() V150() V151() V152() V153() V154() V155() V163() V164() V165() Element of NAT
(IIG,SCS,InpFs,iv) . s1 is Relation-like the carrier of IIG -defined Function-like the Sorts of SCS -compatible non empty total Element of product the Sorts of SCS
s1 + 1 is V21() V22() V23() V27() finite cardinal countable V133() V134() ext-real V148() V149() V150() V151() V152() V153() V154() V155() V163() V164() V165() Element of NAT
(IIG,SCS,InpFs,iv) . (s1 + 1) is Relation-like the carrier of IIG -defined Function-like the Sorts of SCS -compatible non empty total Element of product the Sorts of SCS
(commute InpFs) . 0 is Relation-like Function-like set
dom (commute InpFs) is set
(s1 + 1) -th_InputValues InpFs is Relation-like InputVertices IIG -defined Function-like total InputValues of SCS
(commute InpFs) . (s1 + 1) is Relation-like Function-like set
s2 is Relation-like InputVertices IIG -defined Function-like total InputValues of SCS
Cs1 is Relation-like the carrier of IIG -defined Function-like the Sorts of SCS -compatible non empty total Element of product the Sorts of SCS
(IIG,SCS,Cs1) is Relation-like the carrier of IIG -defined Function-like the Sorts of SCS -compatible non empty total Element of product the Sorts of SCS
(IIG,SCS,((IIG,SCS,InpFs,iv) . s1),((s1 + 1) -th_InputValues InpFs)) is Relation-like the carrier of IIG -defined Function-like the Sorts of SCS -compatible non empty total Element of product the Sorts of SCS
(IIG,SCS,((IIG,SCS,InpFs,iv) . s1),((s1 + 1) -th_InputValues InpFs)) is Relation-like the carrier of IIG -defined Function-like the Sorts of SCS -compatible non empty total Element of product the Sorts of SCS
(IIG,SCS,(IIG,SCS,((IIG,SCS,InpFs,iv) . s1),((s1 + 1) -th_InputValues InpFs))) is Relation-like the carrier of IIG -defined Function-like the Sorts of SCS -compatible non empty total Element of product the Sorts of SCS
(IIG,SCS,InpFs,iv) . 0 is Relation-like the carrier of IIG -defined Function-like the Sorts of SCS -compatible non empty total Element of product the Sorts of SCS
IIG is non empty finite non void V56() Circuit-like monotonic ManySortedSign
InputVertices IIG is finite countable Element of bool the carrier of IIG
the carrier of IIG is non empty finite countable set
bool the carrier of IIG is finite V32() countable set
the ResultSort of IIG is Relation-like the carrier' of IIG -defined the carrier of IIG -valued Function-like 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
K539( the carrier of IIG, the ResultSort of IIG) is finite countable Element of bool the carrier of IIG
the carrier of IIG \ K539( the carrier of IIG, the ResultSort of IIG) is finite countable Element of bool the carrier of IIG
(InputVertices IIG) --> NAT is Relation-like non-empty InputVertices IIG -defined {NAT} -valued Function-like constant total V18( InputVertices IIG,{NAT}) finite Cardinal-yielding countable Element of bool [:(InputVertices IIG),{NAT}:]
[:(InputVertices IIG),{NAT}:] is Relation-like finite countable set
bool [:(InputVertices IIG),{NAT}:] is finite V32() countable set
SCS is non-empty finitely-generated finite-yielding MSAlgebra over IIG
the Sorts of SCS is Relation-like non-empty non empty-yielding the carrier of IIG -defined Function-like non empty total set
the Sorts of SCS | (InputVertices IIG) is Relation-like non-empty InputVertices IIG -defined the carrier of IIG -defined InputVertices IIG -defined Function-like total finite countable set
product the Sorts of SCS is functional non empty with_common_domain product-like set
InpFs is Relation-like InputVertices IIG -defined Function-like total Function-yielding V42() ManySortedFunction of (InputVertices IIG) --> NAT, the Sorts of SCS | (InputVertices IIG)
commute InpFs is Relation-like Function-like Function-yielding V42() set
(commute InpFs) . 0 is Relation-like Function-like set
iv is Relation-like the carrier of IIG -defined Function-like the Sorts of SCS -compatible non empty total Element of product the Sorts of SCS
(IIG,SCS,InpFs,iv) is Relation-like NAT -defined product the Sorts of SCS -valued Function-like V18( NAT , product the Sorts of SCS) Function-yielding V42() Element of bool [:NAT,(product the Sorts of SCS):]
[:NAT,(product the Sorts of SCS):] is Relation-like non trivial non finite set
bool [:NAT,(product the Sorts of SCS):] is non trivial non finite set
dSCS is Relation-like InputVertices IIG -defined Function-like total InputValues of SCS
(IIG,SCS,InpFs,iv) . 0 is Relation-like the carrier of IIG -defined Function-like the Sorts of SCS -compatible non empty total Element of product the Sorts of SCS
s1 is Element of the carrier of IIG
depth (s1,SCS) is V21() V22() V23() V27() finite cardinal countable V133() V134() ext-real set
((IIG,SCS,InpFs,iv) . 0) . s1 is set
(IIG,SCS,s1,dSCS) is Element of the Sorts of SCS . s1
the Sorts of SCS . s1 is non empty set
FreeEnv SCS is strict non-empty free MSAlgebra over IIG
FreeMSA the Sorts of SCS is strict non-empty MSAlgebra over IIG
the Sorts of (FreeEnv SCS) is Relation-like non-empty non empty-yielding the carrier of IIG -defined Function-like non empty total set
the Sorts of (FreeEnv SCS) . s1 is non empty finite countable set
Eval SCS is Relation-like the carrier of IIG -defined Function-like non empty total Function-yielding V42() ManySortedFunction of the Sorts of (FreeEnv SCS), the Sorts of SCS
(Eval SCS) . s1 is Relation-like the Sorts of (FreeEnv SCS) . s1 -defined the Sorts of SCS . s1 -valued Function-like V18( the Sorts of (FreeEnv SCS) . s1, the Sorts of SCS . s1) finite countable Element of bool [:( the Sorts of (FreeEnv SCS) . s1),( the Sorts of SCS . s1):]
[:( the Sorts of (FreeEnv SCS) . s1),( the Sorts of SCS . s1):] is Relation-like set
bool [:( the Sorts of (FreeEnv SCS) . s1),( the Sorts of SCS . s1):] is set
(IIG,SCS,s1,dSCS) is Relation-like Function-like non empty finite countable DecoratedTree-like Element of the Sorts of (FreeEnv SCS) . s1
((Eval SCS) . s1) . (IIG,SCS,s1,dSCS) is Element of the Sorts of SCS . s1
(IIG,SCS,InpFs,iv) is Relation-like the carrier of IIG -defined Function-like the Sorts of SCS -compatible non empty total Element of product the Sorts of SCS
0 -th_InputValues InpFs is Relation-like InputVertices IIG -defined Function-like total InputValues of SCS
(IIG,SCS,iv,(0 -th_InputValues InpFs)) is Relation-like the carrier of IIG -defined Function-like the Sorts of SCS -compatible non empty total Element of product the Sorts of SCS
Set-Constants SCS is Relation-like SortsWithConstants IIG -defined Function-like total set
SortsWithConstants IIG is finite countable Element of bool the carrier of IIG
(IIG,SCS,iv,(0 -th_InputValues InpFs)) +* (Set-Constants SCS) is Relation-like Function-like set
dom (0 -th_InputValues InpFs) is set
dom (Set-Constants SCS) is set
(IIG,SCS,iv,(0 -th_InputValues InpFs)) . s1 is set
(0 -th_InputValues InpFs) . s1 is set
dSCS . s1 is set
dom (Set-Constants SCS) is set
(Set-Constants SCS) . s1 is set
s1 is V21() V22() V23() V27() finite cardinal countable V133() V134() ext-real V148() V149() V150() V151() V152() V153() V154() V155() V163() V164() V165() Element of NAT
(IIG,SCS,InpFs,iv) . s1 is Relation-like the carrier of IIG -defined Function-like the Sorts of SCS -compatible non empty total Element of product the Sorts of SCS
s1 + 1 is V21() V22() V23() V27() finite cardinal countable V133() V134() ext-real V148() V149() V150() V151() V152() V153() V154() V155() V163() V164() V165() Element of NAT
(IIG,SCS,InpFs,iv) . (s1 + 1) is Relation-like the carrier of IIG -defined Function-like the Sorts of SCS -compatible non empty total Element of product the Sorts of SCS
Cs1 is Element of the carrier of IIG
depth (Cs1,SCS) is V21() V22() V23() V27() finite cardinal countable V133() V134() ext-real set
((IIG,SCS,InpFs,iv) . (s1 + 1)) . Cs1 is set
(IIG,SCS,Cs1,dSCS) is Element of the Sorts of SCS . Cs1
the Sorts of SCS . Cs1 is non empty set
FreeEnv SCS is strict non-empty free MSAlgebra over IIG
FreeMSA the Sorts of SCS is strict non-empty MSAlgebra over IIG
the Sorts of (FreeEnv SCS) is Relation-like non-empty non empty-yielding the carrier of IIG -defined Function-like non empty total set
the Sorts of (FreeEnv SCS) . Cs1 is non empty finite countable set
Eval SCS is Relation-like the carrier of IIG -defined Function-like non empty total Function-yielding V42() ManySortedFunction of the Sorts of (FreeEnv SCS), the Sorts of SCS
(Eval SCS) . Cs1 is Relation-like the Sorts of (FreeEnv SCS) . Cs1 -defined the Sorts of SCS . Cs1 -valued Function-like V18( the Sorts of (FreeEnv SCS) . Cs1, the Sorts of SCS . Cs1) finite countable Element of bool [:( the Sorts of (FreeEnv SCS) . Cs1),( the Sorts of SCS . Cs1):]
[:( the Sorts of (FreeEnv SCS) . Cs1),( the Sorts of SCS . Cs1):] is Relation-like set
bool [:( the Sorts of (FreeEnv SCS) . Cs1),( the Sorts of SCS . Cs1):] is set
(IIG,SCS,Cs1,dSCS) is Relation-like Function-like non empty finite countable DecoratedTree-like Element of the Sorts of (FreeEnv SCS) . Cs1
((Eval SCS) . Cs1) . (IIG,SCS,Cs1,dSCS) is Element of the Sorts of SCS . Cs1
dom (commute InpFs) is set
(s1 + 1) -th_InputValues InpFs is Relation-like InputVertices IIG -defined Function-like total InputValues of SCS
(commute InpFs) . (s1 + 1) is Relation-like Function-like set
s2 is Relation-like the carrier of IIG -defined Function-like the Sorts of SCS -compatible non empty total Element of product the Sorts of SCS
(IIG,SCS,s2,((s1 + 1) -th_InputValues InpFs)) is Relation-like the carrier of IIG -defined Function-like the Sorts of SCS -compatible non empty total Element of product the Sorts of SCS
(IIG,SCS,s2,((s1 + 1) -th_InputValues InpFs)) is Relation-like the carrier of IIG -defined Function-like the Sorts of SCS -compatible non empty total Element of product the Sorts of SCS
(IIG,SCS,(IIG,SCS,s2,((s1 + 1) -th_InputValues InpFs))) is Relation-like the carrier of IIG -defined Function-like the Sorts of SCS -compatible non empty total Element of product the Sorts of SCS
(IIG,SCS,s2,((s1 + 1) -th_InputValues InpFs)) . Cs1 is set
(IIG,SCS,s2) is Relation-like the carrier of IIG -defined Function-like the Sorts of SCS -compatible non empty total Element of product the Sorts of SCS
(IIG,SCS,s2) . Cs1 is set
IIG is non empty finite non void V56() Circuit-like monotonic ManySortedSign
InputVertices IIG is finite countable Element of bool the carrier of IIG
the carrier of IIG is non empty finite countable set
bool the carrier of IIG is finite V32() countable set
the ResultSort of IIG is Relation-like the carrier' of IIG -defined the carrier of IIG -valued Function-like 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
K539( the carrier of IIG, the ResultSort of IIG) is finite countable Element of bool the carrier of IIG
the carrier of IIG \ K539( the carrier of IIG, the ResultSort of IIG) is finite countable Element of bool the carrier of IIG
(InputVertices IIG) --> NAT is Relation-like non-empty InputVertices IIG -defined {NAT} -valued Function-like constant total V18( InputVertices IIG,{NAT}) finite Cardinal-yielding countable Element of bool [:(InputVertices IIG),{NAT}:]
[:(InputVertices IIG),{NAT}:] is Relation-like finite countable set
bool [:(InputVertices IIG),{NAT}:] is finite V32() countable set
SCS is non-empty finitely-generated finite-yielding MSAlgebra over IIG
the Sorts of SCS is Relation-like non-empty non empty-yielding the carrier of IIG -defined Function-like non empty total set
the Sorts of SCS | (InputVertices IIG) is Relation-like non-empty InputVertices IIG -defined the carrier of IIG -defined InputVertices IIG -defined Function-like total finite countable set
product the Sorts of SCS is functional non empty with_common_domain product-like set
depth SCS is V21() V22() V23() V27() finite cardinal countable V133() V134() ext-real set
InpFs is Relation-like InputVertices IIG -defined Function-like total Function-yielding V42() ManySortedFunction of (InputVertices IIG) --> NAT, the Sorts of SCS | (InputVertices IIG)
commute InpFs is Relation-like Function-like Function-yielding V42() set
(commute InpFs) . 0 is Relation-like Function-like set
iv is Relation-like InputVertices IIG -defined Function-like total InputValues of SCS
dSCS is Relation-like the carrier of IIG -defined Function-like the Sorts of SCS -compatible non empty total Element of product the Sorts of SCS
(IIG,SCS,InpFs,dSCS) is Relation-like NAT -defined product the Sorts of SCS -valued Function-like V18( NAT , product the Sorts of SCS) Function-yielding V42() Element of bool [:NAT,(product the Sorts of SCS):]
[:NAT,(product the Sorts of SCS):] is Relation-like non trivial non finite set
bool [:NAT,(product the Sorts of SCS):] is non trivial non finite set
s1 is Element of the carrier of IIG
(IIG,SCS,s1,iv) is Element of the Sorts of SCS . s1
the Sorts of SCS . s1 is non empty set
FreeEnv SCS is strict non-empty free MSAlgebra over IIG
FreeMSA the Sorts of SCS is strict non-empty MSAlgebra over IIG
the Sorts of (FreeEnv SCS) is Relation-like non-empty non empty-yielding the carrier of IIG -defined Function-like non empty total set
the Sorts of (FreeEnv SCS) . s1 is non empty finite countable set
Eval SCS is Relation-like the carrier of IIG -defined Function-like non empty total Function-yielding V42() ManySortedFunction of the Sorts of (FreeEnv SCS), the Sorts of SCS
(Eval SCS) . s1 is Relation-like the Sorts of (FreeEnv SCS) . s1 -defined the Sorts of SCS . s1 -valued Function-like V18( the Sorts of (FreeEnv SCS) . s1, the Sorts of SCS . s1) finite countable Element of bool [:( the Sorts of (FreeEnv SCS) . s1),( the Sorts of SCS . s1):]
[:( the Sorts of (FreeEnv SCS) . s1),( the Sorts of SCS . s1):] is Relation-like set
bool [:( the Sorts of (FreeEnv SCS) . s1),( the Sorts of SCS . s1):] is set
(IIG,SCS,s1,iv) is Relation-like Function-like non empty finite countable DecoratedTree-like Element of the Sorts of (FreeEnv SCS) . s1
((Eval SCS) . s1) . (IIG,SCS,s1,iv) is Element of the Sorts of SCS . s1
depth (s1,SCS) is V21() V22() V23() V27() finite cardinal countable V133() V134() ext-real set
s2 is V21() V22() V23() V27() finite cardinal countable V133() V134() ext-real V148() V149() V150() V151() V152() V153() V154() V155() V163() V164() V165() Element of NAT
(IIG,SCS,InpFs,dSCS) . s2 is Relation-like the carrier of IIG -defined Function-like the Sorts of SCS -compatible non empty total Element of product the Sorts of SCS
((IIG,SCS,InpFs,dSCS) . s2) . s1 is set
IIG is non empty finite non void V56() Circuit-like monotonic ManySortedSign
InputVertices IIG is finite countable Element of bool the carrier of IIG
the carrier of IIG is non empty finite countable set
bool the carrier of IIG is finite V32() countable set
the ResultSort of IIG is Relation-like the carrier' of IIG -defined the carrier of IIG -valued Function-like 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
K539( the carrier of IIG, the ResultSort of IIG) is finite countable Element of bool the carrier of IIG
the carrier of IIG \ K539( the carrier of IIG, the ResultSort of IIG) is finite countable Element of bool the carrier of IIG
(InputVertices IIG) --> NAT is Relation-like non-empty InputVertices IIG -defined {NAT} -valued Function-like constant total V18( InputVertices IIG,{NAT}) finite Cardinal-yielding countable Element of bool [:(InputVertices IIG),{NAT}:]
[:(InputVertices IIG),{NAT}:] is Relation-like finite countable set
bool [:(InputVertices IIG),{NAT}:] is finite V32() countable set
SCS is non-empty finitely-generated finite-yielding MSAlgebra over IIG
the Sorts of SCS is Relation-like non-empty non empty-yielding the carrier of IIG -defined Function-like non empty total set
the Sorts of SCS | (InputVertices IIG) is Relation-like non-empty InputVertices IIG -defined the carrier of IIG -defined InputVertices IIG -defined Function-like total finite countable set
product the Sorts of SCS is functional non empty with_common_domain product-like set
depth SCS is V21() V22() V23() V27() finite cardinal countable V133() V134() ext-real set
InpFs is Relation-like InputVertices IIG -defined Function-like total Function-yielding V42() ManySortedFunction of (InputVertices IIG) --> NAT, the Sorts of SCS | (InputVertices IIG)
commute InpFs is Relation-like Function-like Function-yielding V42() set
dom (commute InpFs) is set
(commute InpFs) . 0 is Relation-like Function-like set
dSCS is Relation-like the carrier of IIG -defined Function-like the Sorts of SCS -compatible non empty total Element of product the Sorts of SCS
(IIG,SCS,InpFs,dSCS) is Relation-like NAT -defined product the Sorts of SCS -valued Function-like V18( NAT , product the Sorts of SCS) Function-yielding V42() Element of bool [:NAT,(product the Sorts of SCS):]
[:NAT,(product the Sorts of SCS):] is Relation-like non trivial non finite set
bool [:NAT,(product the Sorts of SCS):] is non trivial non finite set
s1 is V21() V22() V23() V27() finite cardinal countable V133() V134() ext-real V148() V149() V150() V151() V152() V153() V154() V155() V163() V164() V165() Element of NAT
(IIG,SCS,InpFs,dSCS) . s1 is Relation-like the carrier of IIG -defined Function-like the Sorts of SCS -compatible non empty total Element of product the Sorts of SCS
iv is Relation-like InputVertices IIG -defined Function-like total InputValues of SCS
s2 is Relation-like the carrier of IIG -defined Function-like the Sorts of SCS -compatible non empty total Element of product the Sorts of SCS
s1 + 1 is V21() V22() V23() V27() finite cardinal countable V133() V134() ext-real V148() V149() V150() V151() V152() V153() V154() V155() V163() V164() V165() Element of NAT
(s1 + 1) -th_InputValues InpFs is Relation-like InputVertices IIG -defined Function-like total InputValues of SCS
(commute InpFs) . (s1 + 1) is Relation-like Function-like set
(IIG,SCS,InpFs,dSCS) . (s1 + 1) is Relation-like the carrier of IIG -defined Function-like the Sorts of SCS -compatible non empty total Element of product the Sorts of SCS
dom s2 is non empty set
Cs1 is Relation-like the carrier of IIG -defined Function-like the Sorts of SCS -compatible non empty total Element of product the Sorts of SCS
dom Cs1 is non empty set
Cs2 is set
x is Element of the carrier of IIG
depth (x,SCS) is V21() V22() V23() V27() finite cardinal countable V133() V134() ext-real set
s2 . x is set
(IIG,SCS,x,iv) is Element of the Sorts of SCS . x
the Sorts of SCS . x is non empty set
FreeEnv SCS is strict non-empty free MSAlgebra over IIG
FreeMSA the Sorts of SCS is strict non-empty MSAlgebra over IIG
the Sorts of (FreeEnv SCS) is Relation-like non-empty non empty-yielding the carrier of IIG -defined Function-like non empty total set
the Sorts of (FreeEnv SCS) . x is non empty finite countable set
Eval SCS is Relation-like the carrier of IIG -defined Function-like non empty total Function-yielding V42() ManySortedFunction of the Sorts of (FreeEnv SCS), the Sorts of SCS
(Eval SCS) . x is Relation-like the Sorts of (FreeEnv SCS) . x -defined the Sorts of SCS . x -valued Function-like V18( the Sorts of (FreeEnv SCS) . x, the Sorts of SCS . x) finite countable Element of bool [:( the Sorts of (FreeEnv SCS) . x),( the Sorts of SCS . x):]
[:( the Sorts of (FreeEnv SCS) . x),( the Sorts of SCS . x):] is Relation-like set
bool [:( the Sorts of (FreeEnv SCS) . x),( the Sorts of SCS . x):] is set
(IIG,SCS,x,iv) is Relation-like Function-like non empty finite countable DecoratedTree-like Element of the Sorts of (FreeEnv SCS) . x
((Eval SCS) . x) . (IIG,SCS,x,iv) is Element of the Sorts of SCS . x
s2 . Cs2 is set
Cs1 . Cs2 is set
(IIG,SCS,s2,((s1 + 1) -th_InputValues InpFs)) is Relation-like the carrier of IIG -defined Function-like the Sorts of SCS -compatible non empty total Element of product the Sorts of SCS
(IIG,SCS,s2,((s1 + 1) -th_InputValues InpFs)) is Relation-like the carrier of IIG -defined Function-like the Sorts of SCS -compatible non empty total Element of product the Sorts of SCS
(IIG,SCS,(IIG,SCS,s2,((s1 + 1) -th_InputValues InpFs))) is Relation-like the carrier of IIG -defined Function-like the Sorts of SCS -compatible non empty total Element of product the Sorts of SCS
(IIG,SCS,((IIG,SCS,InpFs,dSCS) . s1)) is Relation-like the carrier of IIG -defined Function-like the Sorts of SCS -compatible non empty total Element of product the Sorts of SCS
IIG is non empty finite non void V56() Circuit-like monotonic ManySortedSign
InputVertices IIG is finite countable Element of bool the carrier of IIG
the carrier of IIG is non empty finite countable set
bool the carrier of IIG is finite V32() countable set
the ResultSort of IIG is Relation-like the carrier' of IIG -defined the carrier of IIG -valued Function-like 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
K539( the carrier of IIG, the ResultSort of IIG) is finite countable Element of bool the carrier of IIG
the carrier of IIG \ K539( the carrier of IIG, the ResultSort of IIG) is finite countable Element of bool the carrier of IIG
(InputVertices IIG) --> NAT is Relation-like non-empty InputVertices IIG -defined {NAT} -valued Function-like constant total V18( InputVertices IIG,{NAT}) finite Cardinal-yielding countable Element of bool [:(InputVertices IIG),{NAT}:]
[:(InputVertices IIG),{NAT}:] is Relation-like finite countable set
bool [:(InputVertices IIG),{NAT}:] is finite V32() countable set
SCS is non-empty finitely-generated finite-yielding MSAlgebra over IIG
the Sorts of SCS is Relation-like non-empty non empty-yielding the carrier of IIG -defined Function-like non empty total set
the Sorts of SCS | (InputVertices IIG) is Relation-like non-empty InputVertices IIG -defined the carrier of IIG -defined InputVertices IIG -defined Function-like total finite countable set
product the Sorts of SCS is functional non empty with_common_domain product-like set
depth SCS is V21() V22() V23() V27() finite cardinal countable V133() V134() ext-real set
InpFs is Relation-like InputVertices IIG -defined Function-like total Function-yielding V42() ManySortedFunction of (InputVertices IIG) --> NAT, the Sorts of SCS | (InputVertices IIG)
commute InpFs is Relation-like Function-like Function-yielding V42() set
(commute InpFs) . 0 is Relation-like Function-like set
s1 is Relation-like the carrier of IIG -defined Function-like the Sorts of SCS -compatible non empty total Element of product the Sorts of SCS
(IIG,SCS,InpFs,s1) is Relation-like NAT -defined product the Sorts of SCS -valued Function-like V18( NAT , product the Sorts of SCS) Function-yielding V42() Element of bool [:NAT,(product the Sorts of SCS):]
[:NAT,(product the Sorts of SCS):] is Relation-like non trivial non finite set
bool [:NAT,(product the Sorts of SCS):] is non trivial non finite set
(IIG,SCS,InpFs,s1) . (depth SCS) is Relation-like the carrier of IIG -defined Function-like the Sorts of SCS -compatible non empty total Element of product the Sorts of SCS
s2 is Relation-like the carrier of IIG -defined Function-like the Sorts of SCS -compatible non empty total Element of product the Sorts of SCS
(IIG,SCS,InpFs,s2) is Relation-like NAT -defined product the Sorts of SCS -valued Function-like V18( NAT , product the Sorts of SCS) Function-yielding V42() Element of bool [:NAT,(product the Sorts of SCS):]
(IIG,SCS,InpFs,s2) . (depth SCS) is Relation-like the carrier of IIG -defined Function-like the Sorts of SCS -compatible non empty total Element of product the Sorts of SCS
dSCS is V21() V22() V23() V27() finite cardinal countable V133() V134() ext-real V148() V149() V150() V151() V152() V153() V154() V155() V163() V164() V165() Element of NAT
(IIG,SCS,InpFs,s1) . dSCS is Relation-like the carrier of IIG -defined Function-like the Sorts of SCS -compatible non empty total Element of product the Sorts of SCS
(IIG,SCS,InpFs,s2) . dSCS is Relation-like the carrier of IIG -defined Function-like the Sorts of SCS -compatible non empty total Element of product the Sorts of SCS
Cs1 is Relation-like the carrier of IIG -defined Function-like the Sorts of SCS -compatible non empty total Element of product the Sorts of SCS
dom Cs1 is non empty set
Cs2 is Relation-like the carrier of IIG -defined Function-like the Sorts of SCS -compatible non empty total Element of product the Sorts of SCS
dom Cs2 is non empty set
x is set
x9 is Element of the carrier of IIG
Cs1 . x9 is set
iv is Relation-like InputVertices IIG -defined Function-like total InputValues of SCS
(IIG,SCS,x9,iv) is Element of the Sorts of SCS . x9
the Sorts of SCS . x9 is non empty set
FreeEnv SCS is strict non-empty free MSAlgebra over IIG
FreeMSA the Sorts of SCS is strict non-empty MSAlgebra over IIG
the Sorts of (FreeEnv SCS) is Relation-like non-empty non empty-yielding the carrier of IIG -defined Function-like non empty total set
the Sorts of (FreeEnv SCS) . x9 is non empty finite countable set
Eval SCS is Relation-like the carrier of IIG -defined Function-like non empty total Function-yielding V42() ManySortedFunction of the Sorts of (FreeEnv SCS), the Sorts of SCS
(Eval SCS) . x9 is Relation-like the Sorts of (FreeEnv SCS) . x9 -defined the Sorts of SCS . x9 -valued Function-like V18( the Sorts of (FreeEnv SCS) . x9, the Sorts of SCS . x9) finite countable Element of bool [:( the Sorts of (FreeEnv SCS) . x9),( the Sorts of SCS . x9):]
[:( the Sorts of (FreeEnv SCS) . x9),( the Sorts of SCS . x9):] is Relation-like set
bool [:( the Sorts of (FreeEnv SCS) . x9),( the Sorts of SCS . x9):] is set
(IIG,SCS,x9,iv) is Relation-like Function-like non empty finite countable DecoratedTree-like Element of the Sorts of (FreeEnv SCS) . x9
((Eval SCS) . x9) . (IIG,SCS,x9,iv) is Element of the Sorts of SCS . x9
Cs1 . x is set
Cs2 . x is set