:: 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 (