:: CIRCUIT1 semantic presentation

REAL is non empty non trivial non finite complex-membered ext-real-membered real-membered V144() V151() V152() V154() set

NAT is non empty non trivial epsilon-transitive epsilon-connected ordinal non finite cardinal limit_cardinal countable denumerable complex-membered ext-real-membered real-membered rational-membered integer-membered natural-membered V144() V149() V151() Element of bool REAL

bool REAL is non trivial non finite set

omega is non empty non trivial epsilon-transitive epsilon-connected ordinal non finite cardinal limit_cardinal countable denumerable complex-membered ext-real-membered real-membered rational-membered integer-membered natural-membered V144() V149() V151() set

bool omega is non trivial non finite set

bool NAT is non trivial non finite set

{} is Relation-like non-empty empty-yielding NAT -defined Function-like one-to-one constant functional empty epsilon-transitive epsilon-connected ordinal T-Sequence-like c=-linear natural V28() real finite finite-yielding V34() cardinal {} -element FinSequence-like FinSubsequence-like FinSequence-membered Cardinal-yielding countable constituted-Trees constituted-FinTrees constituted-DTrees Tree-yielding FinTree-yielding DTree-yielding ext-real non positive non negative complex-membered ext-real-membered real-membered rational-membered integer-membered natural-membered V144() V151() V152() V153() V154() set

1 is non empty epsilon-transitive epsilon-connected ordinal natural V28() real finite cardinal countable ext-real positive non negative V136() V137() complex-membered ext-real-membered real-membered rational-membered integer-membered natural-membered V149() V150() V151() V152() V153() Element of NAT

{{},1} is non empty finite V34() countable complex-membered ext-real-membered real-membered rational-membered integer-membered natural-membered V149() V150() V151() V152() V153() set

Trees is non empty constituted-Trees set

bool Trees is set

FinTrees is non empty constituted-Trees constituted-FinTrees Element of bool Trees

PeanoNat is non empty strict with_terminals with_nonterminals with_useful_nonterminals DTConstrStr

the carrier of PeanoNat is non empty set

FinTrees the carrier of PeanoNat is functional non empty constituted-DTrees DTree-set of the carrier of PeanoNat

TS PeanoNat is functional non empty constituted-DTrees Element of bool (FinTrees the carrier of PeanoNat)

bool (FinTrees the carrier of PeanoNat) is set

[:(TS PeanoNat),NAT:] is Relation-like non trivial non finite set

bool [:(TS PeanoNat),NAT:] is non trivial non finite set

[:NAT,(TS PeanoNat):] is Relation-like non trivial non finite set

bool [:NAT,(TS PeanoNat):] is non trivial non finite set

COMPLEX is non empty non trivial non finite complex-membered V144() set

RAT is non empty non trivial non finite complex-membered ext-real-membered real-membered rational-membered V144() set

INT is non empty non trivial non finite complex-membered ext-real-membered real-membered rational-membered integer-membered V144() set

[:COMPLEX,COMPLEX:] is Relation-like non trivial non finite set

bool [:COMPLEX,COMPLEX:] is non trivial non finite set

[:COMPLEX,REAL:] is Relation-like non trivial non finite set

bool [:COMPLEX,REAL:] is non trivial non finite set

2 is non empty epsilon-transitive epsilon-connected ordinal natural V28() real finite cardinal countable ext-real positive non negative V136() V137() complex-membered ext-real-membered real-membered rational-membered integer-membered natural-membered V149() V150() V151() V152() V153() Element of NAT

3 is non empty epsilon-transitive epsilon-connected ordinal natural V28() real finite cardinal countable ext-real positive non negative V136() V137() complex-membered ext-real-membered real-membered rational-membered integer-membered natural-membered V149() V150() V151() V152() V153() Element of NAT

0 is Relation-like non-empty empty-yielding NAT -defined Function-like one-to-one constant functional empty epsilon-transitive epsilon-connected ordinal T-Sequence-like c=-linear natural V28() real finite finite-yielding V34() cardinal {} -element FinSequence-like FinSubsequence-like FinSequence-membered Cardinal-yielding countable constituted-Trees constituted-FinTrees constituted-DTrees Tree-yielding FinTree-yielding DTree-yielding ext-real non positive non negative V136() V137() complex-membered ext-real-membered real-membered rational-membered integer-membered natural-membered V144() V151() V152() V153() V154() Element of NAT

Seg 1 is non empty trivial finite 1 -element countable complex-membered ext-real-membered real-membered rational-membered integer-membered natural-membered V149() V150() V151() V152() V153() Element of bool NAT

{1} is non empty trivial finite V34() 1 -element countable complex-membered ext-real-membered real-membered rational-membered integer-membered natural-membered V149() V150() V151() V152() V153() set

Seg 2 is non empty finite 2 -element countable complex-membered ext-real-membered real-membered rational-membered integer-membered natural-membered V149() V150() V151() V152() V153() Element of bool NAT

{1,2} is non empty finite V34() countable complex-membered ext-real-membered real-membered rational-membered integer-membered natural-membered V149() V150() V151() V152() V153() set

<*> NAT is Relation-like non-empty empty-yielding NAT -defined NAT -valued Function-like one-to-one constant functional empty epsilon-transitive epsilon-connected ordinal T-Sequence-like c=-linear natural V28() real finite finite-yielding V34() cardinal {} -element FinSequence-like FinSubsequence-like FinSequence-membered Cardinal-yielding countable constituted-Trees constituted-FinTrees constituted-DTrees Tree-yielding FinTree-yielding DTree-yielding ext-real non positive non negative complex-membered ext-real-membered real-membered rational-membered integer-membered natural-membered V144() V151() V152() V153() V154() FinSequence of NAT

elementary_tree 0 is non empty finite countable Tree-like set

{{}} is functional non empty trivial finite V34() 1 -element with_common_domain countable Tree-like complex-membered ext-real-membered real-membered rational-membered integer-membered natural-membered V149() V150() V151() V152() V153() set

height (elementary_tree 0) is epsilon-transitive epsilon-connected ordinal natural V28() real finite cardinal countable ext-real non negative V136() V137() complex-membered ext-real-membered real-membered rational-membered integer-membered natural-membered V151() V152() V153() Element of NAT

IIG is non empty non void V51() Circuit-like ManySortedSign

SortsWithConstants IIG is Element of bool the carrier of IIG

the carrier of IIG is non empty set

bool the carrier of IIG is set

A is non-empty finitely-generated finite-yielding MSAlgebra over IIG

{ b

v1 is set

s1 is Element of the carrier of IIG

Y1 is Element of the carrier of IIG

the carrier' of IIG is non empty set

the Arity of IIG is Relation-like the carrier' of IIG -defined the carrier of IIG * -valued Function-like non empty total V18( the carrier' of IIG, the carrier of IIG * ) Element of bool [: the carrier' of IIG,( the carrier of IIG *):]

the carrier of IIG * is functional non empty FinSequence-membered M11( the carrier of IIG)

[: the carrier' of IIG,( the carrier of IIG *):] is Relation-like set

bool [: the carrier' of IIG,( the carrier of IIG *):] is set

the ResultSort of IIG is Relation-like the carrier' of IIG -defined the carrier of IIG -valued Function-like non empty total V18( the carrier' of IIG, the carrier of IIG) Element of bool [: the carrier' of IIG, the carrier of IIG:]

[: the carrier' of IIG, the carrier of IIG:] is Relation-like set

bool [: the carrier' of IIG, the carrier of IIG:] is set

t1 is Element of the carrier' of IIG

the Arity of IIG . t1 is Relation-like NAT -defined Function-like finite FinSequence-like FinSubsequence-like countable set

the ResultSort of IIG . t1 is set

dom the ResultSort of IIG is non empty Element of bool the carrier' of IIG

bool the carrier' of IIG is set

Result (t1,A) is non empty Element of rng the Sorts of A

the Sorts of A is Relation-like non-empty non empty-yielding the carrier of IIG -defined Function-like non empty total set

rng the Sorts of A is non empty set

Den (t1,A) is Relation-like Args (t1,A) -defined Result (t1,A) -valued Function-like non empty total V18( Args (t1,A), Result (t1,A)) Element of bool [:(Args (t1,A)),(Result (t1,A)):]

Args (t1,A) is non empty Element of rng ( the Sorts of A #)

the Sorts of A # is Relation-like the carrier of IIG * -defined Function-like non empty total set

rng ( the Sorts of A #) is non empty set

[:(Args (t1,A)),(Result (t1,A)):] is Relation-like set

bool [:(Args (t1,A)),(Result (t1,A)):] is set

rng (Den (t1,A)) is non empty Element of bool (Result (t1,A))

bool (Result (t1,A)) is set

the Element of rng (Den (t1,A)) is Element of rng (Den (t1,A))

the ResultSort of IIG * the Sorts of A is Relation-like non-empty non empty-yielding the carrier' of IIG -defined Function-like non empty total set

( the ResultSort of IIG * the Sorts of A) . t1 is non empty set

the Sorts of A . ( the ResultSort of IIG . t1) is set

the Sorts of A . Y1 is non empty set

x is set

Constants (A,Y1) is Element of bool ( the Sorts of A . Y1)

bool ( the Sorts of A . Y1) is set

s is Element of the Sorts of A . Y1

Constants (A,s1) is Element of bool ( the Sorts of A . s1)

the Sorts of A . s1 is non empty set

bool ( the Sorts of A . s1) is set

t is non empty set

{ b

( the Arity of IIG . b

Y is set

v1 is Relation-like SortsWithConstants IIG -defined Function-like total set

dom v1 is Element of bool (SortsWithConstants IIG)

bool (SortsWithConstants IIG) is set

s1 is Element of the carrier of IIG

v1 . s1 is set

Constants (A,s1) is Element of bool ( the Sorts of A . s1)

the Sorts of A . s1 is non empty set

bool ( the Sorts of A . s1) is set

Y1 is Element of the carrier of IIG

Constants (A,Y1) is Element of bool ( the Sorts of A . Y1)

the Sorts of A . Y1 is non empty set

bool ( the Sorts of A . Y1) is set

v is Relation-like SortsWithConstants IIG -defined Function-like total set

dom v is Element of bool (SortsWithConstants IIG)

bool (SortsWithConstants IIG) is set

v1 is Relation-like SortsWithConstants IIG -defined Function-like total set

dom v1 is Element of bool (SortsWithConstants IIG)

the carrier' of IIG is non empty set

the Arity of IIG is Relation-like the carrier' of IIG -defined the carrier of IIG * -valued Function-like non empty total V18( the carrier' of IIG, the carrier of IIG * ) Element of bool [: the carrier' of IIG,( the carrier of IIG *):]

the carrier of IIG * is functional non empty FinSequence-membered M11( the carrier of IIG)

[: the carrier' of IIG,( the carrier of IIG *):] is Relation-like set

bool [: the carrier' of IIG,( the carrier of IIG *):] is set

dom the Arity of IIG is non empty Element of bool the carrier' of IIG

bool the carrier' of IIG is set

s1 is set

the Sorts of A is Relation-like non-empty non empty-yielding the carrier of IIG -defined Function-like non empty total set

Y1 is Element of the carrier of IIG

the Sorts of A . Y1 is non empty set

Constants (A,Y1) is Element of bool ( the Sorts of A . Y1)

bool ( the Sorts of A . Y1) is set

the ResultSort of IIG is Relation-like the carrier' of IIG -defined the carrier of IIG -valued Function-like non empty total V18( the carrier' of IIG, the carrier of IIG) Element of bool [: the carrier' of IIG, the carrier of IIG:]

[: the carrier' of IIG, the carrier of IIG:] is Relation-like set

bool [: the carrier' of IIG, the carrier of IIG:] is set

v1 . Y1 is set

t1 is non empty set

{ b

( the Arity of IIG . b

t1 is Element of the Sorts of A . Y1

av is Element of the carrier' of IIG

the Arity of IIG . av is Relation-like NAT -defined Function-like finite FinSequence-like FinSubsequence-like countable set

the ResultSort of IIG . av is set

Result (av,A) is non empty Element of rng the Sorts of A

rng the Sorts of A is non empty set

Den (av,A) is Relation-like Args (av,A) -defined Result (av,A) -valued Function-like non empty total V18( Args (av,A), Result (av,A)) Element of bool [:(Args (av,A)),(Result (av,A)):]

Args (av,A) is non empty Element of rng ( the Sorts of A #)

the Sorts of A # is Relation-like the carrier of IIG * -defined Function-like non empty total set

rng ( the Sorts of A #) is non empty set

[:(Args (av,A)),(Result (av,A)):] is Relation-like set

bool [:(Args (av,A)),(Result (av,A)):] is set

rng (Den (av,A)) is non empty Element of bool (Result (av,A))

bool (Result (av,A)) is set

av is Element of the carrier' of IIG

the Arity of IIG . av is Relation-like NAT -defined Function-like finite FinSequence-like FinSubsequence-like countable set

the ResultSort of IIG . av is set

Result (av,A) is non empty Element of rng the Sorts of A

rng the Sorts of A is non empty set

Den (av,A) is Relation-like Args (av,A) -defined Result (av,A) -valued Function-like non empty total V18( Args (av,A), Result (av,A)) Element of bool [:(Args (av,A)),(Result (av,A)):]

Args (av,A) is non empty Element of rng ( the Sorts of A #)

the Sorts of A # is Relation-like the carrier of IIG * -defined Function-like non empty total set

rng ( the Sorts of A #) is non empty set

[:(Args (av,A)),(Result (av,A)):] is Relation-like set

bool [:(Args (av,A)),(Result (av,A)):] is set

rng (Den (av,A)) is non empty Element of bool (Result (av,A))

bool (Result (av,A)) is set

the_result_sort_of av is Element of the carrier of IIG

v . Y1 is set

s is non empty set

{ b

( the Arity of IIG . b

s is Element of the Sorts of A . Y1

x is Element of the carrier' of IIG

the Arity of IIG . x is Relation-like NAT -defined Function-like finite FinSequence-like FinSubsequence-like countable set

the ResultSort of IIG . x is set

Result (x,A) is non empty Element of rng the Sorts of A

Den (x,A) is Relation-like Args (x,A) -defined Result (x,A) -valued Function-like non empty total V18( Args (x,A), Result (x,A)) Element of bool [:(Args (x,A)),(Result (x,A)):]

Args (x,A) is non empty Element of rng ( the Sorts of A #)

[:(Args (x,A)),(Result (x,A)):] is Relation-like set

bool [:(Args (x,A)),(Result (x,A)):] is set

rng (Den (x,A)) is non empty Element of bool (Result (x,A))

bool (Result (x,A)) is set

x is Element of the carrier' of IIG

the Arity of IIG . x is Relation-like NAT -defined Function-like finite FinSequence-like FinSubsequence-like countable set

the ResultSort of IIG . x is set

Result (x,A) is non empty Element of rng the Sorts of A

Den (x,A) is Relation-like Args (x,A) -defined Result (x,A) -valued Function-like non empty total V18( Args (x,A), Result (x,A)) Element of bool [:(Args (x,A)),(Result (x,A)):]

Args (x,A) is non empty Element of rng ( the Sorts of A #)

[:(Args (x,A)),(Result (x,A)):] is Relation-like set

bool [:(Args (x,A)),(Result (x,A)):] is set

rng (Den (x,A)) is non empty Element of bool (Result (x,A))

bool (Result (x,A)) is set

<*> the carrier of IIG is Relation-like non-empty empty-yielding NAT -defined the carrier of IIG -valued Function-like one-to-one constant functional empty epsilon-transitive epsilon-connected ordinal T-Sequence-like c=-linear natural V28() real finite finite-yielding V34() cardinal {} -element FinSequence-like FinSubsequence-like FinSequence-membered Cardinal-yielding countable constituted-Trees constituted-FinTrees constituted-DTrees Tree-yielding FinTree-yielding DTree-yielding ext-real non positive non negative complex-membered ext-real-membered real-membered rational-membered integer-membered natural-membered V144() V151() V152() V153() V154() FinSequence of the carrier of IIG

dom (Den (av,A)) is non empty Element of bool (Args (av,A))

bool (Args (av,A)) is set

the_result_sort_of x is Element of the carrier of IIG

dom (Den (x,A)) is non empty Element of bool (Args (x,A))

bool (Args (x,A)) is set

Y is set

(Den (x,A)) . Y is set

the Arity of IIG * ( the Sorts of A #) is Relation-like the carrier' of IIG -defined Function-like non empty total set

( the Arity of IIG * ( the Sorts of A #)) . x is set

( the Sorts of A #) . ( the Arity of IIG . x) is set

v . s1 is set

v1 . s1 is set

t is set

(Den (av,A)) . t is set

IIG is non empty non void V51() Circuit-like ManySortedSign

the carrier of IIG is non empty set

SortsWithConstants IIG is Element of bool the carrier of IIG

bool the carrier of IIG is set

A is non-empty finitely-generated finite-yielding MSAlgebra over IIG

the Sorts of A is Relation-like non-empty non empty-yielding the carrier of IIG -defined Function-like non empty total set

(IIG,A) is Relation-like SortsWithConstants IIG -defined Function-like total set

v is Element of the carrier of IIG

the Sorts of A . v is non empty set

Constants (A,v) is Element of bool ( the Sorts of A . v)

bool ( the Sorts of A . v) is set

(IIG,A) . v is set

v1 is Element of the Sorts of A . v

the carrier' of IIG is non empty set

the Arity of IIG is Relation-like the carrier' of IIG -defined the carrier of IIG * -valued Function-like non empty total V18( the carrier' of IIG, the carrier of IIG * ) Element of bool [: the carrier' of IIG,( the carrier of IIG *):]

the carrier of IIG * is functional non empty FinSequence-membered M11( the carrier of IIG)

[: the carrier' of IIG,( the carrier of IIG *):] is Relation-like set

bool [: the carrier' of IIG,( the carrier of IIG *):] is set

the ResultSort of IIG is Relation-like the carrier' of IIG -defined the carrier of IIG -valued Function-like non empty total V18( the carrier' of IIG, the carrier of IIG) Element of bool [: the carrier' of IIG, the carrier of IIG:]

[: the carrier' of IIG, the carrier of IIG:] is Relation-like set

bool [: the carrier' of IIG, the carrier of IIG:] is set

s1 is non empty set

{ b

( the Arity of IIG . b

s1 is Element of the Sorts of A . v

Y1 is Element of the carrier' of IIG

the Arity of IIG . Y1 is Relation-like NAT -defined Function-like finite FinSequence-like FinSubsequence-like countable set

the ResultSort of IIG . Y1 is set

Result (Y1,A) is non empty Element of rng the Sorts of A

rng the Sorts of A is non empty set

Den (Y1,A) is Relation-like Args (Y1,A) -defined Result (Y1,A) -valued Function-like non empty total V18( Args (Y1,A), Result (Y1,A)) Element of bool [:(Args (Y1,A)),(Result (Y1,A)):]

Args (Y1,A) is non empty Element of rng ( the Sorts of A #)

the Sorts of A # is Relation-like the carrier of IIG * -defined Function-like non empty total set

rng ( the Sorts of A #) is non empty set

[:(Args (Y1,A)),(Result (Y1,A)):] is Relation-like set

bool [:(Args (Y1,A)),(Result (Y1,A)):] is set

rng (Den (Y1,A)) is non empty Element of bool (Result (Y1,A))

bool (Result (Y1,A)) is set

s1 is Element of the carrier' of IIG

the Arity of IIG . s1 is Relation-like NAT -defined Function-like finite FinSequence-like FinSubsequence-like countable set

the ResultSort of IIG . s1 is set

Result (s1,A) is non empty Element of rng the Sorts of A

rng the Sorts of A is non empty set

Den (s1,A) is Relation-like Args (s1,A) -defined Result (s1,A) -valued Function-like non empty total V18( Args (s1,A), Result (s1,A)) Element of bool [:(Args (s1,A)),(Result (s1,A)):]

Args (s1,A) is non empty Element of rng ( the Sorts of A #)

the Sorts of A # is Relation-like the carrier of IIG * -defined Function-like non empty total set

rng ( the Sorts of A #) is non empty set

[:(Args (s1,A)),(Result (s1,A)):] is Relation-like set

bool [:(Args (s1,A)),(Result (s1,A)):] is set

rng (Den (s1,A)) is non empty Element of bool (Result (s1,A))

bool (Result (s1,A)) is set

<*> the carrier of IIG is Relation-like non-empty empty-yielding NAT -defined the carrier of IIG -valued Function-like one-to-one constant functional empty epsilon-transitive epsilon-connected ordinal T-Sequence-like c=-linear natural V28() real finite finite-yielding V34() cardinal {} -element FinSequence-like FinSubsequence-like FinSequence-membered Cardinal-yielding countable constituted-Trees constituted-FinTrees constituted-DTrees Tree-yielding FinTree-yielding DTree-yielding ext-real non positive non negative complex-membered ext-real-membered real-membered rational-membered integer-membered natural-membered V144() V151() V152() V153() V154() FinSequence of the carrier of IIG

dom (IIG,A) is Element of bool (SortsWithConstants IIG)

bool (SortsWithConstants IIG) is set

Y1 is non empty set

{ b

( the Arity of IIG . b

Y1 is Element of the Sorts of A . v

t1 is Element of the carrier' of IIG

the Arity of IIG . t1 is Relation-like NAT -defined Function-like finite FinSequence-like FinSubsequence-like countable set

the ResultSort of IIG . t1 is set

Result (t1,A) is non empty Element of rng the Sorts of A

Den (t1,A) is Relation-like Args (t1,A) -defined Result (t1,A) -valued Function-like non empty total V18( Args (t1,A), Result (t1,A)) Element of bool [:(Args (t1,A)),(Result (t1,A)):]

Args (t1,A) is non empty Element of rng ( the Sorts of A #)

[:(Args (t1,A)),(Result (t1,A)):] is Relation-like set

bool [:(Args (t1,A)),(Result (t1,A)):] is set

rng (Den (t1,A)) is non empty Element of bool (Result (t1,A))

bool (Result (t1,A)) is set

Y1 is Element of the carrier' of IIG

the Arity of IIG . Y1 is Relation-like NAT -defined Function-like finite FinSequence-like FinSubsequence-like countable set

the ResultSort of IIG . Y1 is set

Result (Y1,A) is non empty Element of rng the Sorts of A

Den (Y1,A) is Relation-like Args (Y1,A) -defined Result (Y1,A) -valued Function-like non empty total V18( Args (Y1,A), Result (Y1,A)) Element of bool [:(Args (Y1,A)),(Result (Y1,A)):]

Args (Y1,A) is non empty Element of rng ( the Sorts of A #)

[:(Args (Y1,A)),(Result (Y1,A)):] is Relation-like set

bool [:(Args (Y1,A)),(Result (Y1,A)):] is set

rng (Den (Y1,A)) is non empty Element of bool (Result (Y1,A))

bool (Result (Y1,A)) is set

dom (Den (Y1,A)) is non empty Element of bool (Args (Y1,A))

bool (Args (Y1,A)) is set

the_result_sort_of s1 is Element of the carrier of IIG

the_result_sort_of Y1 is Element of the carrier of IIG

dom (Den (s1,A)) is non empty Element of bool (Args (s1,A))

bool (Args (s1,A)) is set

t1 is set

(Den (s1,A)) . t1 is set

dom the Arity of IIG is non empty Element of bool the carrier' of IIG

bool the carrier' of IIG is set

the Arity of IIG * ( the Sorts of A #) is Relation-like the carrier' of IIG -defined Function-like non empty total set

( the Arity of IIG * ( the Sorts of A #)) . s1 is set

( the Sorts of A #) . ( the Arity of IIG . s1) is set

av is set

(Den (Y1,A)) . av is set

IIG is non empty non void V51() Circuit-like ManySortedSign

IIG is non empty non void V51() Circuit-like ManySortedSign

InputVertices IIG is Element of bool the carrier of IIG

the carrier of IIG is non empty set

bool the carrier of IIG is set

the ResultSort of IIG is Relation-like the carrier' of IIG -defined the carrier of IIG -valued Function-like non empty total V18( the carrier' of IIG, the carrier of IIG) Element of bool [: the carrier' of IIG, the carrier of IIG:]

the carrier' of IIG is non empty set

[: the carrier' of IIG, the carrier of IIG:] is Relation-like set

bool [: the carrier' of IIG, the carrier of IIG:] is set

rng the ResultSort of IIG is non empty Element of bool the carrier of IIG

the carrier of IIG \ (rng the ResultSort of IIG) is Element of bool the carrier of IIG

(InputVertices IIG) --> NAT is Relation-like InputVertices IIG -defined {NAT} -valued Function-like total V18( InputVertices IIG,{NAT}) Cardinal-yielding Element of bool [:(InputVertices IIG),{NAT}:]

{NAT} is non empty trivial finite 1 -element countable set

[:(InputVertices IIG),{NAT}:] is Relation-like set

bool [:(InputVertices IIG),{NAT}:] is set

A is non-empty finitely-generated finite-yielding MSAlgebra over IIG

the Sorts of A is Relation-like non-empty non empty-yielding the carrier of IIG -defined Function-like non empty total set

the Sorts of A | (InputVertices IIG) is Relation-like non-empty InputVertices IIG -defined the carrier of IIG -defined InputVertices IIG -defined Function-like total set

v is Relation-like InputVertices IIG -defined Function-like total Function-yielding ManySortedFunction of (InputVertices IIG) --> NAT, the Sorts of A | (InputVertices IIG)

commute v is Relation-like Function-like Function-yielding set

v1 is epsilon-transitive epsilon-connected ordinal natural V28() real finite cardinal countable ext-real non negative V136() V137() complex-membered ext-real-membered real-membered rational-membered integer-membered natural-membered V151() V152() V153() Element of NAT

(commute v) . v1 is set

s1 is Element of bool the carrier of IIG

t1 is non empty Element of bool the carrier of IIG

Y1 is Relation-like non-empty non empty-yielding the carrier of IIG -defined Function-like non empty total set

Y1 | t1 is Relation-like non-empty the carrier of IIG -defined t1 -defined the carrier of IIG -defined Function-like non empty total set

av is Relation-like t1 -defined Function-like non empty total set

s is Relation-like non-empty non empty-yielding t1 -defined Function-like non empty total set

x is Relation-like t1 -defined Function-like non empty total set

Y is Element of the carrier of IIG

s . Y is set

the Sorts of A . Y is non empty set

x . Y is set

IIG is non empty non void V51() Circuit-like ManySortedSign

InputVertices IIG is Element of bool the carrier of IIG

the carrier of IIG is non empty set

bool the carrier of IIG is set

the ResultSort of IIG is Relation-like the carrier' of IIG -defined the carrier of IIG -valued Function-like non empty total V18( the carrier' of IIG, the carrier of IIG) Element of bool [: the carrier' of IIG, the carrier of IIG:]

the carrier' of IIG is non empty set

[: the carrier' of IIG, the carrier of IIG:] is Relation-like set

bool [: the carrier' of IIG, the carrier of IIG:] is set

rng the ResultSort of IIG is non empty Element of bool the carrier of IIG

the carrier of IIG \ (rng the ResultSort of IIG) is Element of bool the carrier of IIG

(InputVertices IIG) --> NAT is Relation-like InputVertices IIG -defined {NAT} -valued Function-like total V18( InputVertices IIG,{NAT}) Cardinal-yielding Element of bool [:(InputVertices IIG),{NAT}:]

{NAT} is non empty trivial finite 1 -element countable set

[:(InputVertices IIG),{NAT}:] is Relation-like set

bool [:(InputVertices IIG),{NAT}:] is set

A is non-empty finitely-generated finite-yielding MSAlgebra over IIG

the Sorts of A is Relation-like non-empty non empty-yielding the carrier of IIG -defined Function-like non empty total set

the Sorts of A | (InputVertices IIG) is Relation-like non-empty InputVertices IIG -defined the carrier of IIG -defined InputVertices IIG -defined Function-like total set

v is Relation-like InputVertices IIG -defined Function-like total Function-yielding ManySortedFunction of (InputVertices IIG) --> NAT, the Sorts of A | (InputVertices IIG)

commute v is Relation-like Function-like Function-yielding set

v1 is epsilon-transitive epsilon-connected ordinal natural V28() real finite cardinal countable ext-real non negative V136() V137() complex-membered ext-real-membered real-membered rational-membered integer-membered natural-membered V151() V152() V153() Element of NAT

(commute v) . v1 is set

IIG is non empty non void V51() Circuit-like ManySortedSign

IIG is non empty non void V51() Circuit-like ManySortedSign

the carrier of IIG is non empty set

A is non-empty finitely-generated finite-yielding MSAlgebra over IIG

the Sorts of A is Relation-like non-empty non empty-yielding the carrier of IIG -defined Function-like non empty total set

product the Sorts of A is functional non empty with_common_domain product-like set

v is Relation-like the carrier of IIG -defined Function-like the Sorts of A -compatible non empty total Element of product the Sorts of A

dom v is non empty Element of bool the carrier of IIG

bool the carrier of IIG is set

IIG is non empty non void V51() Circuit-like ManySortedSign

the carrier of IIG is non empty set

A is non-empty finitely-generated finite-yielding MSAlgebra over IIG

the Sorts of A is Relation-like non-empty non empty-yielding the carrier of IIG -defined Function-like non empty total set

product the Sorts of A is functional non empty with_common_domain product-like set

v is Relation-like the carrier of IIG -defined Function-like the Sorts of A -compatible non empty total Element of product the Sorts of A

v1 is Element of the carrier of IIG

v . v1 is set

the Sorts of A . v1 is non empty set

dom the Sorts of A is non empty Element of bool the carrier of IIG

bool the carrier of IIG is set

s1 is Relation-like Function-like set

dom s1 is set

IIG is non empty non void V51() Circuit-like ManySortedSign

the carrier of IIG is non empty set

A is non-empty finitely-generated finite-yielding MSAlgebra over IIG

the Sorts of A is Relation-like non-empty non empty-yielding the carrier of IIG -defined Function-like non empty total set

product the Sorts of A is functional non empty with_common_domain product-like set

the carrier' of IIG is non empty set

v1 is Element of the carrier' of IIG

the_arity_of v1 is Relation-like NAT -defined the carrier of IIG -valued Function-like finite FinSequence-like FinSubsequence-like countable Element of the carrier of IIG *

the carrier of IIG * is functional non empty FinSequence-membered M11( the carrier of IIG)

v is Relation-like the carrier of IIG -defined Function-like the Sorts of A -compatible non empty total Element of product the Sorts of A

(the_arity_of v1) * v is Relation-like NAT -defined Function-like finite countable set

Args (v1,A) is non empty Element of rng ( the Sorts of A #)

the Sorts of A # is Relation-like the carrier of IIG * -defined Function-like non empty total set

rng ( the Sorts of A #) is non empty set

(the_arity_of v1) * the Sorts of A is Relation-like non-empty NAT -defined Function-like finite countable set

product ((the_arity_of v1) * the Sorts of A) is functional non empty with_common_domain product-like set

IIG is non empty non void V51() Circuit-like monotonic ManySortedSign

the carrier of IIG is non empty set

InnerVertices IIG is non empty Element of bool the carrier of IIG

bool the carrier of IIG is set

the ResultSort of IIG is Relation-like the carrier' of IIG -defined the carrier of IIG -valued Function-like non empty total V18( the carrier' of IIG, the carrier of IIG) Element of bool [: the carrier' of IIG, the carrier of IIG:]

the carrier' of IIG is non empty set

[: the carrier' of IIG, the carrier of IIG:] is Relation-like set

bool [: the carrier' of IIG, the carrier of IIG:] is set

rng the ResultSort of IIG is non empty Element of bool the carrier of IIG

A is non-empty finitely-generated finite-yielding MSAlgebra over IIG

FreeEnv A is strict non-empty V117(IIG) MSAlgebra over IIG

the Sorts of A is Relation-like non-empty non empty-yielding the carrier of IIG -defined Function-like non empty total set

FreeMSA the Sorts of A is strict non-empty MSAlgebra over IIG

the Sorts of (FreeEnv A) is Relation-like non-empty non empty-yielding the carrier of IIG -defined Function-like non empty total set

v is Element of the carrier of IIG

the Sorts of (FreeEnv A) . v is non empty set

action_at v is Element of the carrier' of IIG

[(action_at v), the carrier of IIG] is set

{(action_at v), the carrier of IIG} is non empty finite countable set

{(action_at v)} is non empty trivial finite 1 -element countable set

{{(action_at v), the carrier of IIG},{(action_at v)}} is non empty finite V34() countable set

v1 is Element of the carrier of IIG

the Sorts of (FreeEnv A) . v1 is non empty set

the_arity_of (action_at v) is Relation-like NAT -defined the carrier of IIG -valued Function-like finite FinSequence-like FinSubsequence-like countable Element of the carrier of IIG *

the carrier of IIG * is functional non empty FinSequence-membered M11( the carrier of IIG)

s1 is Element of the Sorts of (FreeEnv A) . v

Y1 is Relation-like NAT -defined Function-like finite FinSequence-like FinSubsequence-like countable DTree-yielding set

[(action_at v), the carrier of IIG] -tree Y1 is Relation-like Function-like DecoratedTree-like set

dom Y1 is finite countable complex-membered ext-real-membered real-membered rational-membered integer-membered natural-membered V151() V152() V153() Element of bool NAT

av is epsilon-transitive epsilon-connected ordinal natural V28() real finite cardinal countable ext-real non negative V136() V137() complex-membered ext-real-membered real-membered rational-membered integer-membered natural-membered V151() V152() V153() Element of NAT

Y1 . av is set

(the_arity_of (action_at v)) /. av is Element of the carrier of IIG

FreeSort the Sorts of A is Relation-like non-empty non empty-yielding the carrier of IIG -defined Function-like non empty total set

FreeOper the Sorts of A is Relation-like the carrier' of IIG -defined Function-like non empty total Function-yielding ManySortedFunction of the Arity of IIG * ((FreeSort the Sorts of A) #), the ResultSort of IIG * (FreeSort the Sorts of A)

the Arity of IIG is Relation-like the carrier' of IIG -defined the carrier of IIG * -valued Function-like non empty total V18( the carrier' of IIG, the carrier of IIG * ) Element of bool [: the carrier' of IIG,( the carrier of IIG *):]

[: the carrier' of IIG,( the carrier of IIG *):] is Relation-like set

bool [: the carrier' of IIG,( the carrier of IIG *):] is set

(FreeSort the Sorts of A) # is Relation-like the carrier of IIG * -defined Function-like non empty total set

the Arity of IIG * ((FreeSort the Sorts of A) #) is Relation-like the carrier' of IIG -defined Function-like non empty total set

the ResultSort of IIG * (FreeSort the Sorts of A) is Relation-like non-empty non empty-yielding the carrier' of IIG -defined Function-like non empty total set

MSAlgebra(# (FreeSort the Sorts of A),(FreeOper the Sorts of A) #) is strict MSAlgebra over IIG

t1 is Element of the carrier' of IIG

the_result_sort_of t1 is Element of the carrier of IIG

the Sorts of (FreeEnv A) . (the_result_sort_of t1) is non empty set

len Y1 is epsilon-transitive epsilon-connected ordinal natural V28() real finite cardinal countable ext-real non negative V136() V137() complex-membered ext-real-membered real-membered rational-membered integer-membered natural-membered V151() V152() V153() Element of NAT

the_arity_of t1 is Relation-like NAT -defined the carrier of IIG -valued Function-like finite FinSequence-like FinSubsequence-like countable Element of the carrier of IIG *

len (the_arity_of t1) is epsilon-transitive epsilon-connected ordinal natural V28() real finite cardinal countable ext-real non negative V136() V137() complex-membered ext-real-membered real-membered rational-membered integer-membered natural-membered V151() V152() V153() Element of NAT

dom (the_arity_of t1) is finite countable complex-membered ext-real-membered real-membered rational-membered integer-membered natural-membered V151() V152() V153() Element of bool NAT

(the_arity_of t1) . av is set

the Sorts of (FreeEnv A) . ((the_arity_of t1) . av) is set

(the_arity_of t1) /. av is Element of the carrier of IIG

(FreeSort the Sorts of A) . ((the_arity_of t1) /. av) is non empty set

(FreeSort the Sorts of A) . v1 is non empty set

((FreeSort the Sorts of A) . ((the_arity_of t1) /. av)) /\ ((FreeSort the Sorts of A) . v1) is set

IIG is non empty non void V51() Circuit-like monotonic ManySortedSign

the carrier of IIG is non empty set

A is non-empty finitely-generated finite-yielding MSAlgebra over IIG

FreeEnv A is strict non-empty V117(IIG) MSAlgebra over IIG

the Sorts of A is Relation-like non-empty non empty-yielding the carrier of IIG -defined Function-like non empty total set

FreeMSA the Sorts of A is strict non-empty MSAlgebra over IIG

the Sorts of (FreeEnv A) is Relation-like non-empty non empty-yielding the carrier of IIG -defined Function-like non empty total set

v is Element of the carrier of IIG

the Sorts of (FreeEnv A) . v is non empty set

v1 is Element of the Sorts of (FreeEnv A) . v

s1 is Element of the Sorts of (FreeEnv A) . v

Y1 is Element of the Sorts of (FreeEnv A) . v

t1 is Element of the Sorts of (FreeEnv A) . v

IIG is non empty non void V51() Circuit-like monotonic ManySortedSign

the carrier of IIG is non empty set

A is non-empty finitely-generated finite-yielding MSAlgebra over IIG

FreeEnv A is strict non-empty V117(IIG) MSAlgebra over IIG

the Sorts of A is Relation-like non-empty non empty-yielding the carrier of IIG -defined Function-like non empty total set

FreeMSA the Sorts of A is strict non-empty MSAlgebra over IIG

the Sorts of (FreeEnv A) is Relation-like non-empty non empty-yielding the carrier of IIG -defined Function-like non empty total set

v is Element of the carrier of IIG

the Sorts of (FreeEnv A) . v is non empty set

v1 is Relation-like Function-like non empty finite countable Element of the Sorts of (FreeEnv A) . v

A is non empty non void V51() Circuit-like monotonic ManySortedSign

the carrier of A is non empty set

InnerVertices A is non empty Element of bool the carrier of A

bool the carrier of A is set

the ResultSort of A is Relation-like the carrier' of A -defined the carrier of A -valued Function-like non empty total V18( the carrier' of A, the carrier of A) Element of bool [: the carrier' of A, the carrier of A:]

the carrier' of A is non empty set

[: the carrier' of A, the carrier of A:] is Relation-like set

bool [: the carrier' of A, the carrier of A:] is set

rng the ResultSort of A is non empty Element of bool the carrier of A

SortsWithConstants A is Element of bool the carrier of A

(InnerVertices A) \ (SortsWithConstants A) is Element of bool the carrier of A

v is non-empty finitely-generated finite-yielding MSAlgebra over A

FreeEnv v is strict non-empty V117(A) MSAlgebra over A

the Sorts of v is Relation-like non-empty non empty-yielding the carrier of A -defined Function-like non empty total set

FreeMSA the Sorts of v is strict non-empty MSAlgebra over A

the Sorts of (FreeEnv v) is Relation-like non-empty non empty-yielding the carrier of A -defined Function-like non empty total set

v1 is Element of the carrier of A

the Sorts of (FreeEnv v) . v1 is non empty set

s1 is Element of the carrier of A

the Sorts of (FreeEnv v) . s1 is non empty set

action_at v1 is Element of the carrier' of A

[(action_at v1), the carrier of A] is set

{(action_at v1), the carrier of A} is non empty finite countable set

{(action_at v1)} is non empty trivial finite 1 -element countable set

{{(action_at v1), the carrier of A},{(action_at v1)}} is non empty finite V34() countable set

Y1 is Relation-like Function-like non empty finite countable DecoratedTree-like Element of the Sorts of (FreeEnv v) . v1

t1 is Relation-like Function-like non empty finite countable DecoratedTree-like Element of the Sorts of (FreeEnv v) . s1

av is Relation-like NAT -defined Function-like finite FinSequence-like FinSubsequence-like countable DTree-yielding set

[(action_at v1), the carrier of A] -tree av is Relation-like Function-like DecoratedTree-like set

dom av is finite countable complex-membered ext-real-membered real-membered rational-membered integer-membered natural-membered V151() V152() V153() Element of bool NAT

s is epsilon-transitive epsilon-connected ordinal natural V28() real finite cardinal countable ext-real non negative V136() V137() complex-membered ext-real-membered real-membered rational-membered integer-membered natural-membered V151() V152() V153() Element of NAT

s + 1 is non empty epsilon-transitive epsilon-connected ordinal natural V28() real finite cardinal countable ext-real positive non negative V136() V137() complex-membered ext-real-membered real-membered rational-membered integer-membered natural-membered V149() V150() V151() V152() V153() Element of NAT

av . (s + 1) is set

<*s*> is Relation-like NAT -defined NAT -valued Function-like constant non empty trivial finite 1 -element FinSequence-like FinSubsequence-like countable FinSequence of NAT

Y1 with-replacement (<*s*>,t1) is Relation-like Function-like DecoratedTree-like set

{ the carrier of A} is non empty trivial finite 1 -element countable set

[: the carrier' of A,{ the carrier of A}:] is Relation-like set

coprod the Sorts of v is Relation-like non-empty non empty-yielding the carrier of A -defined Function-like non empty total set

Union (coprod the Sorts of v) is non empty set

[: the carrier' of A,{ the carrier of A}:] \/ (Union (coprod the Sorts of v)) is non empty set

t is non empty set

t * is functional non empty FinSequence-membered M11(t)

[:t,(t *):] is Relation-like set

bool [:t,(t *):] is set

REL the Sorts of v is Relation-like [: the carrier' of A,{ the carrier of A}:] \/ (Union (coprod the Sorts of v)) -defined ([: the carrier' of A,{ the carrier of A}:] \/ (Union (coprod the Sorts of v))) * -valued Element of bool [:([: the carrier' of A,{ the carrier of A}:] \/ (Union (coprod the Sorts of v))),(([: the carrier' of A,{ the carrier of A}:] \/ (Union (coprod the Sorts of v))) *):]

([: the carrier' of A,{ the carrier of A}:] \/ (Union (coprod the Sorts of v))) * is functional non empty FinSequence-membered M11([: the carrier' of A,{ the carrier of A}:] \/ (Union (coprod the Sorts of v)))

[:([: the carrier' of A,{ the carrier of A}:] \/ (Union (coprod the Sorts of v))),(([: the carrier' of A,{ the carrier of A}:] \/ (Union (coprod the Sorts of v))) *):] is Relation-like set

bool [:([: the carrier' of A,{ the carrier of A}:] \/ (Union (coprod the Sorts of v))),(([: the carrier' of A,{ the carrier of A}:] \/ (Union (coprod the Sorts of v))) *):] is set

DTConMSA the Sorts of v is non empty strict with_terminals with_nonterminals with_useful_nonterminals DTConstrStr

k is Relation-like t -defined t * -valued Element of bool [:t,(t *):]

DTConstrStr(# t,k #) is non empty strict DTConstrStr

FinTrees t is functional non empty constituted-DTrees DTree-set of t

bool (FinTrees t) is set

TS (DTConMSA the Sorts of v) is functional non empty constituted-DTrees Element of bool (FinTrees the carrier of (DTConMSA the Sorts of v))

the carrier of (DTConMSA the Sorts of v) is non empty set

FinTrees the carrier of (DTConMSA the Sorts of v) is functional non empty constituted-DTrees DTree-set of the carrier of (DTConMSA the Sorts of v)

bool (FinTrees the carrier of (DTConMSA the Sorts of v)) is set

k1 is functional constituted-DTrees Element of bool (FinTrees t)

f is set

e9 is Relation-like Function-like DecoratedTree-like set

dom e9 is non empty Tree-like set

dom Y1 is non empty finite countable Tree-like set

t19 is Relation-like NAT -defined Function-like finite FinSequence-like FinSubsequence-like countable DTree-yielding set

doms t19 is Relation-like NAT -defined Function-like finite FinSequence-like FinSubsequence-like countable Tree-yielding set

tree (doms t19) is non empty Tree-like set

dt19 is Relation-like NAT -defined NAT -valued Function-like finite FinSequence-like FinSubsequence-like countable Element of dom Y1

t19 is Relation-like NAT -defined REAL -valued Function-like finite FinSequence-like FinSubsequence-like countable FinSequence of NAT

Y1 with-replacement (t19,t1) is Relation-like Function-like DecoratedTree-like set

tft is Element of the carrier' of A

[tft, the carrier of A] is set

{tft, the carrier of A} is non empty finite countable set

{tft} is non empty trivial finite 1 -element countable set

{{tft, the carrier of A},{tft}} is non empty finite V34() countable set

len av is epsilon-transitive epsilon-connected ordinal natural V28() real finite cardinal countable ext-real non negative V136() V137() complex-membered ext-real-membered real-membered rational-membered integer-membered natural-membered V151() V152() V153() Element of NAT

a is Relation-like NAT -defined Function-like finite FinSequence-like FinSubsequence-like countable DTree-yielding set

[tft, the carrier of A] -tree a is Relation-like Function-like DecoratedTree-like set

len a is epsilon-transitive epsilon-connected ordinal natural V28() real finite cardinal countable ext-real non negative V136() V137() complex-membered ext-real-membered real-membered rational-membered integer-membered natural-membered V151() V152() V153() Element of NAT

a . (s + 1) is set

NonTerminals (DTConMSA the Sorts of v) is non empty Element of bool the carrier of (DTConMSA the Sorts of v)

bool the carrier of (DTConMSA the Sorts of v) is set

FreeSort the Sorts of v is Relation-like non-empty non empty-yielding the carrier of A -defined Function-like non empty total set

FreeOper the Sorts of v is Relation-like the carrier' of A -defined Function-like non empty total Function-yielding ManySortedFunction of the Arity of A * ((FreeSort the Sorts of v) #), the ResultSort of A * (FreeSort the Sorts of v)

the Arity of A is Relation-like the carrier' of A -defined the carrier of A * -valued Function-like non empty total V18( the carrier' of A, the carrier of A * ) Element of bool [: the carrier' of A,( the carrier of A *):]

the carrier of A * is functional non empty FinSequence-membered M11( the carrier of A)

[: the carrier' of A,( the carrier of A *):] is Relation-like set

bool [: the carrier' of A,( the carrier of A *):] is set

(FreeSort the Sorts of v) # is Relation-like the carrier of A * -defined Function-like non empty total set

the Arity of A * ((FreeSort the Sorts of v) #) is Relation-like the carrier' of A -defined Function-like non empty total set

the ResultSort of A * (FreeSort the Sorts of v) is Relation-like non-empty non empty-yielding the carrier' of A -defined Function-like non empty total set

MSAlgebra(# (FreeSort the Sorts of v),(FreeOper the Sorts of v) #) is strict MSAlgebra over A

FreeSort ( the Sorts of v,v1) is functional non empty constituted-DTrees Element of bool (TS (DTConMSA the Sorts of v))

bool (TS (DTConMSA the Sorts of v)) is set

Y1 . {} is set

o is Element of NonTerminals (DTConMSA the Sorts of v)

q is Relation-like NAT -defined FinTrees the carrier of (DTConMSA the Sorts of v) -valued Function-like finite FinSequence-like FinSubsequence-like countable DTree-yielding FinSequence of TS (DTConMSA the Sorts of v)

o -tree q is Relation-like the carrier of (DTConMSA the Sorts of v) -valued Function-like finite countable DecoratedTree-like Element of FinTrees the carrier of (DTConMSA the Sorts of v)

roots q is Relation-like NAT -defined the carrier of (DTConMSA the Sorts of v) -valued Function-like finite FinSequence-like FinSubsequence-like countable FinSequence of the carrier of (DTConMSA the Sorts of v)

FreeSort ( the Sorts of v,s1) is functional non empty constituted-DTrees Element of bool (TS (DTConMSA the Sorts of v))

the Sorts of v . s1 is non empty set

{ b

( b

( [b

q is Relation-like the carrier of (DTConMSA the Sorts of v) -valued Function-like DecoratedTree-like Element of TS (DTConMSA the Sorts of v)

q . {} is set

dom a is finite countable complex-membered ext-real-membered real-membered rational-membered integer-membered natural-membered V151() V152() V153() Element of bool NAT

rng a is finite countable set

q9 is set

qq is set

a . qq is set

tft is epsilon-transitive epsilon-connected ordinal natural V28() real finite cardinal countable ext-real non negative V136() V137() complex-membered ext-real-membered real-membered rational-membered integer-membered natural-membered V151() V152() V153() Element of NAT

tft is epsilon-transitive epsilon-connected ordinal natural V28() real finite cardinal countable ext-real non negative V136() V137() complex-membered ext-real-membered real-membered rational-membered integer-membered natural-membered V151() V152() V153() Element of NAT

a . tft is set

o9 is Relation-like NAT -defined FinTrees the carrier of (DTConMSA the Sorts of v) -valued Function-like finite FinSequence-like FinSubsequence-like countable DTree-yielding FinSequence of TS (DTConMSA the Sorts of v)

o9 . tft is Relation-like Function-like set

tft is epsilon-transitive epsilon-connected ordinal natural V28() real finite cardinal countable ext-real non negative V136() V137() complex-membered ext-real-membered real-membered rational-membered integer-membered natural-membered V151() V152() V153() Element of NAT

f is functional non empty constituted-DTrees DTree-set of t

q9 is Relation-like NAT -defined f -valued Function-like finite FinSequence-like FinSubsequence-like countable DTree-yielding FinSequence of f

roots q9 is Relation-like NAT -defined t -valued Function-like finite FinSequence-like FinSubsequence-like countable FinSequence of t

qq is Relation-like NAT -defined t -valued Function-like finite FinSequence-like FinSubsequence-like countable FinSequence of t

tft is Relation-like NAT -defined t -valued Function-like finite FinSequence-like FinSubsequence-like countable Element of t *

dom tft is finite countable complex-membered ext-real-membered real-membered rational-membered integer-membered natural-membered V151() V152() V153() Element of bool NAT

the_result_sort_of tft is Element of the carrier of A

the Sorts of (FreeEnv v) . (the_result_sort_of tft) is non empty set

the_arity_of tft is Relation-like NAT -defined the carrier of A -valued Function-like finite FinSequence-like FinSubsequence-like countable Element of the carrier of A *

len (the_arity_of tft) is epsilon-transitive epsilon-connected ordinal natural V28() real finite cardinal countable ext-real non negative V136() V137() complex-membered ext-real-membered real-membered rational-membered integer-membered natural-membered V151() V152() V153() Element of NAT

dom (the_arity_of tft) is finite countable complex-membered ext-real-membered real-membered rational-membered integer-membered natural-membered V151() V152() V153() Element of bool NAT

o9 is Relation-like NAT -defined FinTrees the carrier of (DTConMSA the Sorts of v) -valued Function-like finite FinSequence-like FinSubsequence-like countable DTree-yielding FinSequence of TS (DTConMSA the Sorts of v)

dttft is set

tft . dttft is set

(the_arity_of tft) . dttft is set

coprod (((the_arity_of tft) . dttft), the Sorts of v) is set

e9 is Relation-like NAT -defined f -valued Function-like finite FinSequence-like FinSubsequence-like countable DTree-yielding FinSequence of f

roots e9 is Relation-like NAT -defined t -valued Function-like finite FinSequence-like FinSubsequence-like countable FinSequence of t

ttft is Relation-like NAT -defined [: the carrier' of A,{ the carrier of A}:] \/ (Union (coprod the Sorts of v)) -valued Function-like finite FinSequence-like FinSubsequence-like countable Element of ([: the carrier' of A,{ the carrier of A}:] \/ (Union (coprod the Sorts of v))) *

S1 is epsilon-transitive epsilon-connected ordinal natural V28() real finite cardinal countable ext-real non negative V136() V137() complex-membered ext-real-membered real-membered rational-membered integer-membered natural-membered V151() V152() V153() Element of NAT

(the_arity_of tft) /. S1 is Element of the carrier of A

(the_arity_of tft) . S1 is set

s1 is epsilon-transitive epsilon-connected ordinal natural V28() real finite cardinal countable ext-real non negative set

av . s1 is set

(the_arity_of tft) /. s1 is Element of the carrier of A

FreeSort ( the Sorts of v,((the_arity_of tft) /. s1)) is functional non empty constituted-DTrees Element of bool (TS (DTConMSA the Sorts of v))

(the_arity_of tft) . s1 is set

the Sorts of (FreeEnv v) . ((the_arity_of tft) . s1) is set

( the Arity of A * ((FreeSort the Sorts of v) #)) . tft is set

Sym (tft, the Sorts of v) is Element of the carrier of (DTConMSA the Sorts of v)

dtft is Element of the carrier of (DTConMSA the Sorts of v)

f9 is Relation-like NAT -defined Function-like finite FinSequence-like FinSubsequence-like countable set

roots av is Relation-like NAT -defined Function-like finite FinSequence-like FinSubsequence-like countable set

dom (roots av) is finite countable complex-membered ext-real-membered real-membered rational-membered integer-membered natural-membered V151() V152() V153() Element of bool NAT

[dtft,f9] is set

{dtft,f9} is non empty finite countable set

{dtft} is non empty trivial finite 1 -element countable set

{{dtft,f9},{dtft}} is non empty finite V34() countable set

(the_arity_of tft) /. (s + 1) is Element of the carrier of A

a . S1 is set

tft . S1 is set

av . S1 is set

(roots av) . S1 is set

s1 is Element of the carrier' of A

[s1, the carrier of A] is set

{s1, the carrier of A} is non empty finite countable set

{s1} is non empty trivial finite 1 -element countable set

{{s1, the carrier of A},{s1}} is non empty finite V34() countable set

the_result_sort_of s1 is Element of the carrier of A

x99 is set

[x99,s1] is set

{x99,s1} is non empty finite countable set

{x99} is non empty trivial finite 1 -element countable set

{{x99,s1},{x99}} is non empty finite V34() countable set

root-tree [x99,s1] is Relation-like Function-like finite countable DecoratedTree-like set

x99 is set

[x99,s1] is set

{x99,s1} is non empty finite countable set

{x99} is non empty trivial finite 1 -element countable set

{{x99,s1},{x99}} is non empty finite V34() countable set

root-tree [x99,s1] is Relation-like Function-like finite countable DecoratedTree-like set

rqx is Relation-like Function-like DecoratedTree-like set

rqx . {} is set

rqx is set

x99 is Element of the carrier' of A

[x99, the carrier of A] is set

{x99, the carrier of A} is non empty finite countable set

{x99} is non empty trivial finite 1 -element countable set

{{x99, the carrier of A},{x99}} is non empty finite V34() countable set

the_result_sort_of x99 is Element of the carrier of A

rqx is Relation-like Function-like DecoratedTree-like set

rqx . {} is set

x99 is set

[x99,s1] is set

{x99,s1} is non empty finite countable set

{x99} is non empty trivial finite 1 -element countable set

{{x99,s1},{x99}} is non empty finite V34() countable set

root-tree [x99,s1] is Relation-like Function-like finite countable DecoratedTree-like set

rqx is Element of the carrier' of A

[rqx, the carrier of A] is set

{rqx, the carrier of A} is non empty finite countable set

{rqx} is non empty trivial finite 1 -element countable set

{{rqx, the carrier of A},{rqx}} is non empty finite V34() countable set

the_result_sort_of rqx is Element of the carrier of A

x99 is set

[x99,s1] is set

{x99,s1} is non empty finite countable set

{x99} is non empty trivial finite 1 -element countable set

{{x99,s1},{x99}} is non empty finite V34() countable set

root-tree [x99,s1] is Relation-like Function-like finite countable DecoratedTree-like set

rqx is Element of the carrier' of A

[rqx, the carrier of A] is set

{rqx, the carrier of A} is non empty finite countable set

{rqx} is non empty trivial finite 1 -element countable set

{{rqx, the carrier of A},{rqx}} is non empty finite V34() countable set

the_result_sort_of rqx is Element of the carrier of A

x99 is Relation-like Function-like DecoratedTree-like set

x99 . {} is set

rqx is Relation-like Function-like DecoratedTree-like set

rqx . {} is set

Terminals (DTConMSA the Sorts of v) is non empty Element of bool the carrier of (DTConMSA the Sorts of v)

x99 is set

s1 is Element of the carrier of A

the Sorts of v . s1 is non empty set

[x99,s1] is set

{x99,s1} is non empty finite countable set

{x99} is non empty trivial finite 1 -element countable set

{{x99,s1},{x99}} is non empty finite V34() countable set

rqx is Element of Terminals (DTConMSA the Sorts of v)

root-tree rqx is Relation-like the carrier of (DTConMSA the Sorts of v) -valued Function-like finite countable DecoratedTree-like Element of TS (DTConMSA the Sorts of v)

c

c

{ b

( b

( [b

FreeSort ( the Sorts of v,s1) is functional non empty constituted-DTrees Element of bool (TS (DTConMSA the Sorts of v))

(FreeSort the Sorts of v) . s1 is non empty set

(FreeSort the Sorts of v) . s1 is non empty set

((FreeSort the Sorts of v) . s1) /\ ((FreeSort the Sorts of v) . s1) is set

rqx is Relation-like Function-like DecoratedTree-like set

rqx . {} is set

c

c

len tft is epsilon-transitive epsilon-connected ordinal natural V28() real finite cardinal countable ext-real non negative V136() V137() complex-membered ext-real-membered real-membered rational-membered integer-membered natural-membered V151() V152() V153() Element of NAT

roots a is Relation-like NAT -defined Function-like finite FinSequence-like FinSubsequence-like countable set

[o,(roots a)] is set

{o,(roots a)} is non empty finite countable set

{o} is non empty trivial finite 1 -element countable set

{{o,(roots a)},{o}} is non empty finite V34() countable set

dtft is Relation-like NAT -defined FinTrees the carrier of (DTConMSA the Sorts of v) -valued Function-like finite FinSequence-like FinSubsequence-like countable DTree-yielding SubtreeSeq of o

o -tree dtft is Relation-like the carrier of (DTConMSA the Sorts of v) -valued Function-like DecoratedTree-like Element of TS (DTConMSA the Sorts of v)

dom t1 is non empty finite countable Tree-like set

(dom Y1) with-replacement (t19,(dom t1)) is non empty Tree-like set

(Y1 with-replacement (<*s*>,t1)) . (<*> NAT) is set

Y1 . (<*> NAT) is set

(Y1 with-replacement (<*s*>,t1)) . {} is set

dttft is Relation-like NAT -defined REAL -valued Function-like finite FinSequence-like FinSubsequence-like countable FinSequence of NAT

t19 ^ dttft is Relation-like NAT -defined NAT -valued Function-like finite FinSequence-like FinSubsequence-like countable FinSequence of NAT

t1 . dttft is set

dttft is Element of the carrier' of A

the_result_sort_of dttft is Element of the carrier of A

e9 is Relation-like the carrier of (DTConMSA the Sorts of v) -valued Function-like DecoratedTree-like Element of TS (DTConMSA the Sorts of v)

the Sorts of v . v1 is non empty set

{ b

( b

( [b

ttft is Element of the carrier' of A

[ttft, the carrier of A] is set

{ttft, the carrier of A} is non empty finite countable set

{ttft} is non empty trivial finite 1 -element countable set

{{ttft, the carrier of A},{ttft}} is non empty finite V34() countable set

the_result_sort_of ttft is Element of the carrier of A

dttft is Relation-like Function-like non empty finite countable DecoratedTree-like Element of the Sorts of (FreeEnv v) . v1

IIG is non empty non void V51() Circuit-like monotonic ManySortedSign

the carrier of IIG is non empty set

the carrier' of IIG is non empty set

A is non-empty finitely-generated finite-yielding MSAlgebra over IIG

FreeEnv A is strict non-empty V117(IIG) MSAlgebra over IIG

the Sorts of A is Relation-like non-empty non empty-yielding the carrier of IIG -defined Function-like non empty total set

FreeMSA the Sorts of A is strict non-empty MSAlgebra over IIG

the Sorts of (FreeEnv A) is Relation-like non-empty non empty-yielding the carrier of IIG -defined Function-like non empty total set

v is Element of the carrier of IIG

the Sorts of (FreeEnv A) . v is non empty set

v1 is Relation-like Function-like non empty finite countable DecoratedTree-like Element of the Sorts of (FreeEnv A) . v

card v1 is non empty epsilon-transitive epsilon-connected ordinal natural V28() real finite cardinal countable ext-real positive non negative V136() V137() complex-membered ext-real-membered real-membered rational-membered integer-membered natural-membered V149() V150() V151() V152() V153() Element of omega

v1 . {} is set

FreeSort the Sorts of A is Relation-like non-empty non empty-yielding the carrier of IIG -defined Function-like non empty total set

(FreeSort the Sorts of A) . v is non empty set

FreeSort ( the Sorts of A,v) is functional non empty constituted-DTrees Element of bool (TS (DTConMSA the Sorts of A))

DTConMSA the Sorts of A is non empty strict with_terminals with_nonterminals with_useful_nonterminals DTConstrStr

TS (DTConMSA the Sorts of A) is functional non empty constituted-DTrees Element of bool (FinTrees the carrier of (DTConMSA the Sorts of A))

the carrier of (DTConMSA the Sorts of A) is non empty set

FinTrees the carrier of (DTConMSA the Sorts of A) is functional non empty constituted-DTrees DTree-set of the carrier of (DTConMSA the Sorts of A)

bool (FinTrees the carrier of (DTConMSA the Sorts of A)) is set

bool (TS (DTConMSA the Sorts of A)) is set

the Sorts of A . v is non empty set

{ b

( b

( [b

the Sorts of (FreeMSA the Sorts of A) is Relation-like non-empty non empty-yielding the carrier of IIG -defined Function-like non empty total set

the Sorts of (FreeMSA the Sorts of A) . v is non empty set

FreeOper the Sorts of A is Relation-like the carrier' of IIG -defined Function-like non empty total Function-yielding ManySortedFunction of the Arity of IIG * ((FreeSort the Sorts of A) #), the ResultSort of IIG * (FreeSort the Sorts of A)

the Arity of IIG is Relation-like the carrier' of IIG -defined the carrier of IIG * -valued Function-like non empty total V18( the carrier' of IIG, the carrier of IIG * ) Element of bool [: the carrier' of IIG,( the carrier of IIG *):]

the carrier of IIG * is functional non empty FinSequence-membered M11( the carrier of IIG)

[: the carrier' of IIG,( the carrier of IIG *):] is Relation-like set

bool [: the carrier' of IIG,( the carrier of IIG *):] is set

(FreeSort the Sorts of A) # is Relation-like the carrier of IIG * -defined Function-like non empty total set

the Arity of IIG * ((FreeSort the Sorts of A) #) is Relation-like the carrier' of IIG -defined Function-like non empty total set

the ResultSort of IIG is Relation-like the carrier' of IIG -defined the carrier of IIG -valued Function-like non empty total V18( the carrier' of IIG, the carrier of IIG) Element of bool [: the carrier' of IIG, the carrier of IIG:]

[: the carrier' of IIG, the carrier of IIG:] is Relation-like set

bool [: the carrier' of IIG, the carrier of IIG:] is set

the ResultSort of IIG * (FreeSort the Sorts of A) is Relation-like non-empty non empty-yielding the carrier' of IIG -defined Function-like non empty total set

MSAlgebra(# (FreeSort the Sorts of A),(FreeOper the Sorts of A) #) is strict MSAlgebra over IIG

Y1 is Relation-like the carrier of (DTConMSA the Sorts of A) -valued Function-like DecoratedTree-like Element of TS (DTConMSA the Sorts of A)

t1 is set

[t1,v] is set

{t1,v} is non empty finite countable set

{t1} is non empty trivial finite 1 -element countable set

{{t1,v},{t1}} is non empty finite V34() countable set

root-tree [t1,v] is Relation-like Function-like finite countable DecoratedTree-like set

av is Element of the carrier' of IIG

[av, the carrier of IIG] is set

{av, the carrier of IIG} is non empty finite countable set

{av} is non empty trivial finite 1 -element countable set

{{av, the carrier of IIG},{av}} is non empty finite V34() countable set

Y1 . {} is set

the_result_sort_of av is Element of the carrier of IIG

IIG is non empty non void V51() Circuit-like ManySortedSign

the carrier of IIG is non empty set

the carrier' of IIG is non empty set

A is non-empty finitely-generated finite-yielding MSAlgebra over IIG

the Sorts of A is Relation-like non-empty non empty-yielding the carrier of IIG -defined Function-like non empty total set

product the Sorts of A is functional non empty with_common_domain product-like set

v is Relation-like the carrier of IIG -defined Function-like the Sorts of A -compatible non empty total Element of product the Sorts of A

v1 is Element of the carrier' of IIG

Den (v1,A) is Relation-like Args (v1,A) -defined Result (v1,A) -valued Function-like non empty total V18( Args (v1,A), Result (v1,A)) Element of bool [:(Args (v1,A)),(Result (v1,A)):]

Args (v1,A) is non empty Element of rng ( the Sorts of A #)

the Sorts of A # is Relation-like the carrier of IIG * -defined Function-like non empty total set

the carrier of IIG * is functional non empty FinSequence-membered M11( the carrier of IIG)

rng ( the Sorts of A #) is non empty set

Result (v1,A) is non empty Element of rng the Sorts of A

rng the Sorts of A is non empty set

[:(Args (v1,A)),(Result (v1,A)):] is Relation-like set

bool [:(Args (v1,A)),(Result (v1,A)):] is set

(IIG,A,v,v1) is Element of Args (v1,A)

the_arity_of v1 is Relation-like NAT -defined the carrier of IIG -valued Function-like finite FinSequence-like FinSubsequence-like countable Element of the carrier of IIG *

(the_arity_of v1) * v is Relation-like NAT -defined Function-like finite countable set

(Den (v1,A)) . (IIG,A,v,v1) is set

the_result_sort_of v1 is Element of the carrier of IIG

the Sorts of A . (the_result_sort_of v1) is non empty set

the ResultSort of IIG is Relation-like the carrier' of IIG -defined the carrier of IIG -valued Function-like non empty total V18( the carrier' of IIG, the carrier of IIG) Element of bool [: the carrier' of IIG, the carrier of IIG:]

[: the carrier' of IIG, the carrier of IIG:] is Relation-like set

bool [: the carrier' of IIG, the carrier of IIG:] is set

dom the ResultSort of IIG is non empty Element of bool the carrier' of IIG

bool the carrier' of IIG is set

the ResultSort of IIG * the Sorts of A is Relation-like non-empty non empty-yielding the carrier' of IIG -defined Function-like non empty total set

( the ResultSort of IIG * the Sorts of A) . v1 is non empty set

the ResultSort of IIG . v1 is set

the Sorts of A . ( the ResultSort of IIG . v1) is set

IIG is non empty non void V51() Circuit-like monotonic ManySortedSign

the carrier of IIG is non empty set

A is non-empty finitely-generated finite-yielding MSAlgebra over IIG

FreeEnv A is strict non-empty V117(IIG) MSAlgebra over IIG

the Sorts of A is Relation-like non-empty non empty-yielding the carrier of IIG -defined Function-like non empty total set

FreeMSA the Sorts of A is strict non-empty MSAlgebra over IIG

the Sorts of (FreeEnv A) is Relation-like non-empty non empty-yielding the carrier of IIG -defined Function-like non empty total set

v is Element of the carrier of IIG

the Sorts of (FreeEnv A) . v is non empty set

action_at v is Element of the carrier' of IIG

the carrier' of IIG is non empty set

[(action_at v), the carrier of IIG] is set

{(action_at v), the carrier of IIG} is non empty finite countable set

{(action_at v)} is non empty trivial finite 1 -element countable set

{{(action_at v), the carrier of IIG},{(action_at v)}} is non empty finite V34() countable set

v1 is Relation-like Function-like non empty finite countable DecoratedTree-like Element of the Sorts of (FreeEnv A) . v

v1 . {} is set

DTConMSA the Sorts of A is non empty strict with_terminals with_nonterminals with_useful_nonterminals DTConstrStr

NonTerminals (DTConMSA the Sorts of A) is non empty Element of bool the carrier of (DTConMSA the Sorts of A)

the carrier of (DTConMSA the Sorts of A) is non empty set

bool the carrier of (DTConMSA the Sorts of A) is set

{ the carrier of IIG} is non empty trivial finite 1 -element countable set

[: the carrier' of IIG,{ the carrier of IIG}:] is Relation-like set

FreeSort the Sorts of A is Relation-like non-empty non empty-yielding the carrier of IIG -defined Function-like non empty total set

FreeOper the Sorts of A is Relation-like the carrier' of IIG -defined Function-like non empty total Function-yielding ManySortedFunction of the Arity of IIG * ((FreeSort the Sorts of A) #), the ResultSort of IIG * (FreeSort the Sorts of A)

the Arity of IIG is Relation-like the carrier' of IIG -defined the carrier of IIG * -valued Function-like non empty total V18( the carrier' of IIG, the carrier of IIG * ) Element of bool [: the carrier' of IIG,( the carrier of IIG *):]

the carrier of IIG * is functional non empty FinSequence-membered M11( the carrier of IIG)

[: the carrier' of IIG,( the carrier of IIG *):] is Relation-like set

bool [: the carrier' of IIG,( the carrier of IIG *):] is set

(FreeSort the Sorts of A) # is Relation-like the carrier of IIG * -defined Function-like non empty total set

the Arity of IIG * ((FreeSort the Sorts of A) #) is Relation-like the carrier' of IIG -defined Function-like non empty total set

the ResultSort of IIG is Relation-like the carrier' of IIG -defined the carrier of IIG -valued Function-like non empty total V18( the carrier' of IIG, the carrier of IIG) Element of bool [: the carrier' of IIG, the carrier of IIG:]

[: the carrier' of IIG, the carrier of IIG:] is Relation-like set

bool [: the carrier' of IIG, the carrier of IIG:] is set

the ResultSort of IIG * (FreeSort the Sorts of A) is Relation-like non-empty non empty-yielding the carrier' of IIG -defined Function-like non empty total set

MSAlgebra(# (FreeSort the Sorts of A),(FreeOper the Sorts of A) #) is strict MSAlgebra over IIG

FreeSort ( the Sorts of A,v) is functional non empty constituted-DTrees Element of bool (TS (DTConMSA the Sorts of A))

TS (DTConMSA the Sorts of A) is functional non empty constituted-DTrees Element of bool (FinTrees the carrier of (DTConMSA the Sorts of A))

FinTrees the carrier of (DTConMSA the Sorts of A) is functional non empty constituted-DTrees DTree-set of the carrier of (DTConMSA the Sorts of A)

bool (FinTrees the carrier of (DTConMSA the Sorts of A)) is set

bool (TS (DTConMSA the Sorts of A)) is set

t1 is Relation-like the carrier of (DTConMSA the Sorts of A) -valued Function-like DecoratedTree-like Element of TS (DTConMSA the Sorts of A)

Y1 is Element of NonTerminals (DTConMSA the Sorts of A)

av is Relation-like NAT -defined FinTrees the carrier of (DTConMSA the Sorts of A) -valued Function-like finite FinSequence-like FinSubsequence-like countable DTree-yielding FinSequence of TS (DTConMSA the Sorts of A)

Y1 -tree av is Relation-like the carrier of (DTConMSA the Sorts of A) -valued Function-like finite countable DecoratedTree-like Element of FinTrees the carrier of (DTConMSA the Sorts of A)

roots av is Relation-like NAT -defined the carrier of (DTConMSA the Sorts of A) -valued Function-like finite FinSequence-like FinSubsequence-like countable FinSequence of the carrier of (DTConMSA the Sorts of A)

[(action_at v), the carrier of IIG] -tree av is Relation-like Function-like DecoratedTree-like set

IIG is non empty non void V51() monotonic ManySortedSign

the carrier of IIG is non empty set

A is non-empty finitely-generated finite-yielding MSAlgebra over IIG

FreeEnv A is strict non-empty V117(IIG) MSAlgebra over IIG

the Sorts of A is Relation-like non-empty non empty-yielding the carrier of IIG -defined Function-like non empty total set

FreeMSA the Sorts of A is strict non-empty MSAlgebra over IIG

the Sorts of (FreeEnv A) is Relation-like non-empty non empty-yielding the carrier of IIG -defined Function-like non empty total set

v is Element of the carrier of IIG

the Sorts of (FreeEnv A) . v is non empty set

IIG is non empty non void V51() Circuit-like monotonic ManySortedSign

the carrier of IIG is non empty set

A is non-empty finitely-generated finite-yielding MSAlgebra over IIG

FreeEnv A is strict non-empty V117(IIG) MSAlgebra over IIG

the Sorts of A is Relation-like non-empty non empty-yielding the carrier of IIG -defined Function-like non empty total set

FreeMSA the Sorts of A is strict non-empty MSAlgebra over IIG

the Sorts of (FreeEnv A) is Relation-like non-empty non empty-yielding the carrier of IIG -defined Function-like non empty total set

v is Element of the carrier of IIG

the Sorts of (FreeEnv A) . v is non empty finite countable set

{ (card b

{ H

the Relation-like Function-like non empty finite countable DecoratedTree-like Element of the Sorts of (FreeEnv A) . v is Relation-like Function-like non empty finite countable DecoratedTree-like Element of the Sorts of (FreeEnv A) . v

card the Relation-like Function-like non empty finite countable DecoratedTree-like Element of the Sorts of (FreeEnv A) . v is non empty epsilon-transitive epsilon-connected ordinal natural V28() real finite cardinal countable ext-real positive non negative V136() V137() complex-membered ext-real-membered real-membered rational-membered integer-membered natural-membered V149() V150() V151() V152() V153() Element of omega

Y1 is non empty finite countable complex-membered ext-real-membered real-membered rational-membered integer-membered natural-membered V149() V150() V151() V152() V153() Element of bool NAT

max Y1 is epsilon-transitive epsilon-connected ordinal natural V28() real finite cardinal countable ext-real non negative V136() V137() set

Y1 is non empty finite countable complex-membered ext-real-membered real-membered rational-membered integer-membered natural-membered V149() V150() V151() V152() V153() Element of bool NAT

v1 is epsilon-transitive epsilon-connected ordinal natural V28() real finite cardinal countable ext-real non negative set

max Y1 is epsilon-transitive epsilon-connected ordinal natural V28() real finite cardinal countable ext-real non negative V136() V137() set

t1 is non empty finite countable complex-membered ext-real-membered real-membered rational-membered integer-membered natural-membered V149() V150() V151() V152() V153() Element of bool NAT

s1 is epsilon-transitive epsilon-connected ordinal natural V28() real finite cardinal countable ext-real non negative set

max t1 is epsilon-transitive epsilon-connected ordinal natural V28() real finite cardinal countable ext-real non negative V136() V137() set

IIG is non empty non void V51() Circuit-like monotonic ManySortedSign

the carrier of IIG is non empty set

InputVertices IIG is Element of bool the carrier of IIG

bool the carrier of IIG is set

the ResultSort of IIG is Relation-like the carrier' of IIG -defined the carrier of IIG -valued Function-like non empty total V18( the carrier' of IIG, the carrier of IIG) Element of bool [: the carrier' of IIG, the carrier of IIG:]

the carrier' of IIG is non empty set

[: the carrier' of IIG, the carrier of IIG:] is Relation-like set

bool [: the carrier' of IIG, the carrier of IIG:] is set

rng the ResultSort of IIG is non empty Element of bool the carrier of IIG

the carrier of IIG \ (rng the ResultSort of IIG) is Element of bool the carrier of IIG

SortsWithConstants IIG is Element of bool the carrier of IIG

(InputVertices IIG) \/ (SortsWithConstants IIG) is Element of bool the carrier of IIG

A is non-empty finitely-generated