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

( b

( [b

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

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

( b

( [b

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 (