:: CIRCCMB3 semantic presentation

REAL is V140() V141() V142() V146() V149() V150() V152() set

NAT is non empty non trivial V17() V18() V19() non finite V95() V96() V140() V141() V142() V143() V144() V145() V146() V147() V149() Element of bool REAL

bool REAL is set

NAT is non empty non trivial V17() V18() V19() non finite V95() V96() V140() V141() V142() V143() V144() V145() V146() V147() V149() set

bool NAT is set

bool NAT is set

{} is non pair empty Relation-like non-empty empty-yielding NAT -defined Function-like one-to-one constant functional V17() V18() V19() V21() V22() V23() Function-yielding V34() finite finite-yielding V39() FinSequence-like FinSubsequence-like FinSequence-membered V47() V92() V95() non with_pair ext-real V140() V141() V142() V143() V144() V145() V146() V149() V150() V151() V152() V153() set

the non pair empty Relation-like non-empty empty-yielding NAT -defined Function-like one-to-one constant functional V17() V18() V19() V21() V22() V23() Function-yielding V34() finite finite-yielding V39() FinSequence-like FinSubsequence-like FinSequence-membered V47() V92() V95() non with_pair ext-real V140() V141() V142() V143() V144() V145() V146() V149() V150() V151() V152() V153() set is non pair empty Relation-like non-empty empty-yielding NAT -defined Function-like one-to-one constant functional V17() V18() V19() V21() V22() V23() Function-yielding V34() finite finite-yielding V39() FinSequence-like FinSubsequence-like FinSequence-membered V47() V92() V95() non with_pair ext-real V140() V141() V142() V143() V144() V145() V146() V149() V150() V151() V152() V153() set

1 is non pair non empty V17() V18() V19() V23() V47() ext-real positive V140() V141() V142() V143() V144() V145() V147() V149() V153() Element of NAT

{{},1} is non empty finite V95() non with_pair V140() V141() V142() V143() V144() V145() V147() V148() V149() V150() V151() set

K298() is set

bool K298() is set

K299() is Element of bool K298()

K339() is non empty V108() L10()

the carrier of K339() is non empty set

K302( the carrier of K339()) is non empty M21( the carrier of K339())

K338(K339()) is Element of bool K302( the carrier of K339())

bool K302( the carrier of K339()) is set

[:K338(K339()),NAT:] is Relation-like set

bool [:K338(K339()),NAT:] is set

[:NAT,K338(K339()):] is Relation-like set

bool [:NAT,K338(K339()):] is set

K420() is set

2 is non pair non empty V17() V18() V19() V23() V47() ext-real positive V140() V141() V142() V143() V144() V145() V147() V149() V153() Element of NAT

2 -tuples_on K420() is functional FinSequence-membered FinSequenceSet of K420()

[:(2 -tuples_on K420()),K420():] is Relation-like set

bool [:(2 -tuples_on K420()),K420():] is set

3 is non pair non empty V17() V18() V19() V23() V47() ext-real positive V140() V141() V142() V143() V144() V145() V147() V149() V153() Element of NAT

3 -tuples_on K420() is functional FinSequence-membered FinSequenceSet of K420()

[:(3 -tuples_on K420()),K420():] is Relation-like set

bool [:(3 -tuples_on K420()),K420():] is set

K441() is Relation-like 2 -tuples_on K420() -defined K420() -valued Function-like V30(2 -tuples_on K420(),K420()) Element of bool [:(2 -tuples_on K420()),K420():]

0 is non pair empty Relation-like non-empty empty-yielding NAT -defined Function-like one-to-one constant functional V17() V18() V19() V21() V22() V23() Function-yielding V34() finite finite-yielding V39() FinSequence-like FinSubsequence-like FinSequence-membered V47() V92() V95() non with_pair ext-real V140() V141() V142() V143() V144() V145() V146() V149() V150() V151() V152() V153() Element of NAT

4 is non pair non empty V17() V18() V19() V23() V47() ext-real positive V140() V141() V142() V143() V144() V145() V147() V149() V153() Element of NAT

5 is non pair non empty V17() V18() V19() V23() V47() ext-real positive V140() V141() V142() V143() V144() V145() V147() V149() V153() Element of NAT

Seg 1 is non empty finite V42(1) V95() V140() V141() V142() V143() V144() V145() V147() V148() V149() V150() V151() Element of bool NAT

Seg 4 is non empty finite V42(4) V95() V140() V141() V142() V143() V144() V145() V147() V148() V149() V150() V151() Element of bool NAT

{1,2,3,4} is finite V95() set

Seg 5 is non empty finite V42(5) V95() V140() V141() V142() V143() V144() V145() V147() V148() V149() V150() V151() Element of bool NAT

{1,2,3,4,5} is finite V95() set

proj1 {} is non pair empty Relation-like non-empty empty-yielding NAT -defined Function-like one-to-one constant functional V17() V18() V19() V21() V22() V23() Function-yielding V34() finite finite-yielding V39() FinSequence-like FinSubsequence-like FinSequence-membered V47() V92() V95() non with_pair ext-real V140() V141() V142() V143() V144() V145() V146() V149() V150() V151() V152() V153() set

proj2 {} is non pair empty trivial Relation-like non-empty empty-yielding NAT -defined Function-like one-to-one constant functional V17() V18() V19() V21() V22() V23() Function-yielding V34() finite finite-yielding V39() FinSequence-like FinSubsequence-like FinSequence-membered V47() V92() V95() non with_pair ext-real V140() V141() V142() V143() V144() V145() V146() V149() V150() V151() V152() V153() set

X is non empty non void V79() Circuit-like ManySortedSign

the carrier of X is non empty set

InputVertices X is Element of bool the carrier of X

bool the carrier of X is set

the ResultSort of X is Relation-like the carrier' of X -defined the carrier of X -valued Function-like V30( the carrier' of X, the carrier of X) Element of bool [: the carrier' of X, the carrier of X:]

the carrier' of X is non empty set

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

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

K488( the carrier of X, the ResultSort of X) is Element of bool the carrier of X

the carrier of X \ K488( the carrier of X, the ResultSort of X) is Element of bool the carrier of X

S is non-empty finite-yielding MSAlgebra over X

the Sorts of S is non empty Relation-like non-empty non empty-yielding the carrier of X -defined Function-like total set

K246( the Sorts of S) is non empty functional V93() V94() set

x1 is non empty Relation-like the carrier of X -defined Function-like the Sorts of S -compatible total Element of K246( the Sorts of S)

x2 is set

x1 . x2 is set

x3 is non pair V17() V18() V19() V23() V47() ext-real V140() V141() V142() V143() V144() V145() V149() V153() Element of NAT

Following (x1,x3) is non empty Relation-like the carrier of X -defined Function-like the Sorts of S -compatible total Element of K246( the Sorts of S)

(Following (x1,x3)) . x2 is set

x3 + 1 is non pair V17() V18() V19() V23() V47() ext-real V140() V141() V142() V143() V144() V145() V149() V153() Element of NAT

Following (x1,(x3 + 1)) is non empty Relation-like the carrier of X -defined Function-like the Sorts of S -compatible total Element of K246( the Sorts of S)

(Following (x1,(x3 + 1))) . x2 is set

Following (Following (x1,x3)) is non empty Relation-like the carrier of X -defined Function-like the Sorts of S -compatible total Element of K246( the Sorts of S)

(Following (Following (x1,x3))) . x2 is set

Following (x1,0) is non empty Relation-like the carrier of X -defined Function-like the Sorts of S -compatible total Element of K246( the Sorts of S)

(Following (x1,0)) . x2 is set

X is non empty non void V79() Circuit-like ManySortedSign

the carrier of X is non empty set

S is non-empty finite-yielding MSAlgebra over X

the Sorts of S is non empty Relation-like non-empty non empty-yielding the carrier of X -defined Function-like total set

K246( the Sorts of S) is non empty functional V93() V94() set

X is non empty non void V79() Circuit-like ManySortedSign

X is non empty non void V79() Circuit-like ManySortedSign

S is non-empty finite-yielding MSAlgebra over X

the carrier of X is non empty set

the Sorts of S is non empty Relation-like non-empty non empty-yielding the carrier of X -defined Function-like total set

K246( the Sorts of S) is non empty functional V93() V94() set

x1 is non pair V17() V18() V19() V23() V47() ext-real V140() V141() V142() V143() V144() V145() V149() V153() Element of NAT

x2 is non empty Relation-like the carrier of X -defined Function-like the Sorts of S -compatible total Element of K246( the Sorts of S)

Following (x2,x1) is non empty Relation-like the carrier of X -defined Function-like the Sorts of S -compatible total Element of K246( the Sorts of S)

X is non empty non void V79() Circuit-like ManySortedSign

the carrier of X is non empty set

S is non-empty finite-yielding MSAlgebra over X

the Sorts of S is non empty Relation-like non-empty non empty-yielding the carrier of X -defined Function-like total set

K246( the Sorts of S) is non empty functional V93() V94() set

x1 is non empty Relation-like the carrier of X -defined Function-like the Sorts of S -compatible total Element of K246( the Sorts of S)

x2 is non pair V17() V18() V19() V23() V47() ext-real V140() V141() V142() V143() V144() V145() V149() V153() Element of NAT

Following (x1,x2) is non empty Relation-like the carrier of X -defined Function-like the Sorts of S -compatible total Element of K246( the Sorts of S)

x2 is non empty Relation-like the carrier of X -defined Function-like the Sorts of S -compatible total Element of K246( the Sorts of S)

x3 is non empty Relation-like the carrier of X -defined Function-like the Sorts of S -compatible total Element of K246( the Sorts of S)

f is non pair V17() V18() V19() V23() V47() ext-real V140() V141() V142() V143() V144() V145() V149() V153() Element of NAT

Following (x1,f) is non empty Relation-like the carrier of X -defined Function-like the Sorts of S -compatible total Element of K246( the Sorts of S)

f is non pair V17() V18() V19() V23() V47() ext-real V140() V141() V142() V143() V144() V145() V149() V153() Element of NAT

Following (x1,f) is non empty Relation-like the carrier of X -defined Function-like the Sorts of S -compatible total Element of K246( the Sorts of S)

a is non pair V17() V18() V19() V23() V47() ext-real V140() V141() V142() V143() V144() V145() V149() V153() Element of NAT

Following (x1,a) is non empty Relation-like the carrier of X -defined Function-like the Sorts of S -compatible total Element of K246( the Sorts of S)

a is non pair V17() V18() V19() V23() V47() ext-real V140() V141() V142() V143() V144() V145() V149() V153() Element of NAT

Following (x1,a) is non empty Relation-like the carrier of X -defined Function-like the Sorts of S -compatible total Element of K246( the Sorts of S)

X is non empty non void V79() Circuit-like ManySortedSign

the carrier of X is non empty set

S is non-empty finite-yielding MSAlgebra over X

the Sorts of S is non empty Relation-like non-empty non empty-yielding the carrier of X -defined Function-like total set

K246( the Sorts of S) is non empty functional V93() V94() set

x1 is non empty Relation-like the carrier of X -defined Function-like the Sorts of S -compatible total Element of K246( the Sorts of S)

x2 is non pair V17() V18() V19() V23() V47() ext-real V140() V141() V142() V143() V144() V145() V149() V153() Element of NAT

Following (x1,x2) is non empty Relation-like the carrier of X -defined Function-like the Sorts of S -compatible total Element of K246( the Sorts of S)

x2 is non pair V17() V18() V19() V23() V47() ext-real V153() set

Following (x1,x2) is non empty Relation-like the carrier of X -defined Function-like the Sorts of S -compatible total Element of K246( the Sorts of S)

x3 is non pair V17() V18() V19() V23() V47() ext-real V140() V141() V142() V143() V144() V145() V149() V153() Element of NAT

Following (x1,x3) is non empty Relation-like the carrier of X -defined Function-like the Sorts of S -compatible total Element of K246( the Sorts of S)

f is non pair V17() V18() V19() V23() V47() ext-real V140() V141() V142() V143() V144() V145() V149() V153() Element of NAT

Following (x1,f) is non empty Relation-like the carrier of X -defined Function-like the Sorts of S -compatible total Element of K246( the Sorts of S)

x2 is non pair V17() V18() V19() V23() V47() ext-real V140() V141() V142() V143() V144() V145() V149() V153() Element of NAT

Following (x1,x2) is non empty Relation-like the carrier of X -defined Function-like the Sorts of S -compatible total Element of K246( the Sorts of S)

x3 is non pair V17() V18() V19() V23() V47() ext-real V140() V141() V142() V143() V144() V145() V149() V153() Element of NAT

Following (x1,x3) is non empty Relation-like the carrier of X -defined Function-like the Sorts of S -compatible total Element of K246( the Sorts of S)

X is non empty non void V79() Circuit-like ManySortedSign

the carrier of X is non empty set

S is non-empty finite-yielding MSAlgebra over X

the Sorts of S is non empty Relation-like non-empty non empty-yielding the carrier of X -defined Function-like total set

K246( the Sorts of S) is non empty functional V93() V94() set

x1 is non empty Relation-like the carrier of X -defined Function-like the Sorts of S -compatible total Element of K246( the Sorts of S)

(X,S,x1) is non empty Relation-like the carrier of X -defined Function-like the Sorts of S -compatible total Element of K246( the Sorts of S)

(X,S,x1) is non pair V17() V18() V19() V23() V47() ext-real V140() V141() V142() V143() V144() V145() V149() V153() Element of NAT

Following (x1,(X,S,x1)) is non empty Relation-like the carrier of X -defined Function-like the Sorts of S -compatible total Element of K246( the Sorts of S)

X is non empty non void V79() Circuit-like ManySortedSign

the carrier of X is non empty set

S is non-empty finite-yielding MSAlgebra over X

the Sorts of S is non empty Relation-like non-empty non empty-yielding the carrier of X -defined Function-like total set

K246( the Sorts of S) is non empty functional V93() V94() set

x1 is non empty Relation-like the carrier of X -defined Function-like the Sorts of S -compatible total Element of K246( the Sorts of S)

(X,S,x1) is non pair V17() V18() V19() V23() V47() ext-real V140() V141() V142() V143() V144() V145() V149() V153() Element of NAT

x2 is non pair V17() V18() V19() V23() V47() ext-real V140() V141() V142() V143() V144() V145() V149() V153() Element of NAT

Following (x1,x2) is non empty Relation-like the carrier of X -defined Function-like the Sorts of S -compatible total Element of K246( the Sorts of S)

X is non empty non void V79() Circuit-like ManySortedSign

the carrier of X is non empty set

S is non-empty finite-yielding MSAlgebra over X

the Sorts of S is non empty Relation-like non-empty non empty-yielding the carrier of X -defined Function-like total set

K246( the Sorts of S) is non empty functional V93() V94() set

x1 is non empty Relation-like the carrier of X -defined Function-like the Sorts of S -compatible total Element of K246( the Sorts of S)

(X,S,x1) is non empty Relation-like the carrier of X -defined Function-like the Sorts of S -compatible total Element of K246( the Sorts of S)

x2 is non pair V17() V18() V19() V23() V47() ext-real V140() V141() V142() V143() V144() V145() V149() V153() Element of NAT

Following (x1,x2) is non empty Relation-like the carrier of X -defined Function-like the Sorts of S -compatible total Element of K246( the Sorts of S)

X is non empty non void V79() Circuit-like ManySortedSign

the carrier of X is non empty set

S is non-empty finite-yielding MSAlgebra over X

the Sorts of S is non empty Relation-like non-empty non empty-yielding the carrier of X -defined Function-like total set

K246( the Sorts of S) is non empty functional V93() V94() set

x1 is non empty Relation-like the carrier of X -defined Function-like the Sorts of S -compatible total Element of K246( the Sorts of S)

(X,S,x1) is non pair V17() V18() V19() V23() V47() ext-real V140() V141() V142() V143() V144() V145() V149() V153() Element of NAT

(X,S,x1) is non empty Relation-like the carrier of X -defined Function-like the Sorts of S -compatible total Element of K246( the Sorts of S)

x2 is non pair V17() V18() V19() V23() V47() ext-real V140() V141() V142() V143() V144() V145() V149() V153() Element of NAT

Following (x1,x2) is non empty Relation-like the carrier of X -defined Function-like the Sorts of S -compatible total Element of K246( the Sorts of S)

Following (x1,(X,S,x1)) is non empty Relation-like the carrier of X -defined Function-like the Sorts of S -compatible total Element of K246( the Sorts of S)

X is non empty non void V79() Circuit-like ManySortedSign

the carrier of X is non empty set

InputVertices X is Element of bool the carrier of X

bool the carrier of X is set

the ResultSort of X is Relation-like the carrier' of X -defined the carrier of X -valued Function-like V30( the carrier' of X, the carrier of X) Element of bool [: the carrier' of X, the carrier of X:]

the carrier' of X is non empty set

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

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

K488( the carrier of X, the ResultSort of X) is Element of bool the carrier of X

the carrier of X \ K488( the carrier of X, the ResultSort of X) is Element of bool the carrier of X

S is non-empty finite-yielding MSAlgebra over X

the Sorts of S is non empty Relation-like non-empty non empty-yielding the carrier of X -defined Function-like total set

K246( the Sorts of S) is non empty functional V93() V94() set

x1 is non empty Relation-like the carrier of X -defined Function-like the Sorts of S -compatible total Element of K246( the Sorts of S)

(X,S,x1) is non empty Relation-like the carrier of X -defined Function-like the Sorts of S -compatible total Element of K246( the Sorts of S)

(X,S,x1) is non pair V17() V18() V19() V23() V47() ext-real V140() V141() V142() V143() V144() V145() V149() V153() Element of NAT

Following (x1,(X,S,x1)) is non empty Relation-like the carrier of X -defined Function-like the Sorts of S -compatible total Element of K246( the Sorts of S)

x2 is set

(X,S,x1) . x2 is set

x1 . x2 is set

X is non empty non void V79() Circuit-like ManySortedSign

InputVertices X is Element of bool the carrier of X

the carrier of X is non empty set

bool the carrier of X is set

the ResultSort of X is Relation-like the carrier' of X -defined the carrier of X -valued Function-like V30( the carrier' of X, the carrier of X) Element of bool [: the carrier' of X, the carrier of X:]

the carrier' of X is non empty set

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

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

K488( the carrier of X, the ResultSort of X) is Element of bool the carrier of X

the carrier of X \ K488( the carrier of X, the ResultSort of X) is Element of bool the carrier of X

S is non empty non void V79() Circuit-like ManySortedSign

InnerVertices S is Element of bool the carrier of S

the carrier of S is non empty set

bool the carrier of S is set

the ResultSort of S is Relation-like the carrier' of S -defined the carrier of S -valued Function-like V30( the carrier' of S, the carrier of S) Element of bool [: the carrier' of S, the carrier of S:]

the carrier' of S is non empty set

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

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

K488( the carrier of S, the ResultSort of S) is Element of bool the carrier of S

InputVertices S is Element of bool the carrier of S

the carrier of S \ K488( the carrier of S, the ResultSort of S) is Element of bool the carrier of S

InnerVertices X is Element of bool the carrier of X

X +* S is non empty non void V79() strict ManySortedSign

x1 is non empty non void V79() Circuit-like ManySortedSign

the carrier of x1 is non empty set

x2 is non-empty finite-yielding MSAlgebra over X

the Sorts of x2 is non empty Relation-like non-empty non empty-yielding the carrier of X -defined Function-like total set

K246( the Sorts of x2) is non empty functional V93() V94() set

x3 is non-empty finite-yielding MSAlgebra over S

x2 +* x3 is strict non-empty MSAlgebra over X +* S

the Sorts of x3 is non empty Relation-like non-empty non empty-yielding the carrier of S -defined Function-like total set

K246( the Sorts of x3) is non empty functional V93() V94() set

f is non-empty finite-yielding MSAlgebra over x1

the Sorts of f is non empty Relation-like non-empty non empty-yielding the carrier of x1 -defined Function-like total set

K246( the Sorts of f) is non empty functional V93() V94() set

a is non empty Relation-like the carrier of x1 -defined Function-like the Sorts of f -compatible total Element of K246( the Sorts of f)

a | the carrier of X is Relation-like the carrier of X -defined the carrier of x1 -defined Function-like the Sorts of f -compatible set

a | the carrier of S is Relation-like the carrier of S -defined the carrier of x1 -defined Function-like the Sorts of f -compatible set

b is non empty Relation-like the carrier of X -defined Function-like the Sorts of x2 -compatible total Element of K246( the Sorts of x2)

c is non empty Relation-like the carrier of S -defined Function-like the Sorts of x3 -compatible total Element of K246( the Sorts of x3)

g is non pair V17() V18() V19() V23() V47() ext-real V140() V141() V142() V143() V144() V145() V149() V153() Element of NAT

Following (b,g) is non empty Relation-like the carrier of X -defined Function-like the Sorts of x2 -compatible total Element of K246( the Sorts of x2)

k is non pair V17() V18() V19() V23() V47() ext-real V140() V141() V142() V143() V144() V145() V149() V153() Element of NAT

Following (c,k) is non empty Relation-like the carrier of S -defined Function-like the Sorts of x3 -compatible total Element of K246( the Sorts of x3)

max (g,k) is non pair V17() V18() V19() V23() V47() ext-real V140() V141() V142() V143() V144() V145() V149() V153() Element of NAT

Following (a,(max (g,k))) is non empty Relation-like the carrier of x1 -defined Function-like the Sorts of f -compatible total Element of K246( the Sorts of f)

X is non empty non void V79() Circuit-like ManySortedSign

InputVertices X is Element of bool the carrier of X

the carrier of X is non empty set

bool the carrier of X is set

the ResultSort of X is Relation-like the carrier' of X -defined the carrier of X -valued Function-like V30( the carrier' of X, the carrier of X) Element of bool [: the carrier' of X, the carrier of X:]

the carrier' of X is non empty set

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

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

K488( the carrier of X, the ResultSort of X) is Element of bool the carrier of X

the carrier of X \ K488( the carrier of X, the ResultSort of X) is Element of bool the carrier of X

S is non empty non void V79() Circuit-like ManySortedSign

InnerVertices S is Element of bool the carrier of S

the carrier of S is non empty set

bool the carrier of S is set

the ResultSort of S is Relation-like the carrier' of S -defined the carrier of S -valued Function-like V30( the carrier' of S, the carrier of S) Element of bool [: the carrier' of S, the carrier of S:]

the carrier' of S is non empty set

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

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

K488( the carrier of S, the ResultSort of S) is Element of bool the carrier of S

InputVertices S is Element of bool the carrier of S

the carrier of S \ K488( the carrier of S, the ResultSort of S) is Element of bool the carrier of S

InnerVertices X is Element of bool the carrier of X

X +* S is non empty non void V79() strict ManySortedSign

x1 is non empty non void V79() Circuit-like ManySortedSign

the carrier of x1 is non empty set

x2 is non-empty finite-yielding MSAlgebra over X

the Sorts of x2 is non empty Relation-like non-empty non empty-yielding the carrier of X -defined Function-like total set

K246( the Sorts of x2) is non empty functional V93() V94() set

x3 is non-empty finite-yielding MSAlgebra over S

x2 +* x3 is strict non-empty MSAlgebra over X +* S

the Sorts of x3 is non empty Relation-like non-empty non empty-yielding the carrier of S -defined Function-like total set

K246( the Sorts of x3) is non empty functional V93() V94() set

f is non-empty finite-yielding MSAlgebra over x1

the Sorts of f is non empty Relation-like non-empty non empty-yielding the carrier of x1 -defined Function-like total set

K246( the Sorts of f) is non empty functional V93() V94() set

a is non empty Relation-like the carrier of x1 -defined Function-like the Sorts of f -compatible total Element of K246( the Sorts of f)

a | the carrier of X is Relation-like the carrier of X -defined the carrier of x1 -defined Function-like the Sorts of f -compatible set

a | the carrier of S is Relation-like the carrier of S -defined the carrier of x1 -defined Function-like the Sorts of f -compatible set

(x1,f,a) is non pair V17() V18() V19() V23() V47() ext-real V140() V141() V142() V143() V144() V145() V149() V153() Element of NAT

b is non empty Relation-like the carrier of X -defined Function-like the Sorts of x2 -compatible total Element of K246( the Sorts of x2)

(X,x2,b) is non pair V17() V18() V19() V23() V47() ext-real V140() V141() V142() V143() V144() V145() V149() V153() Element of NAT

g is non empty Relation-like the carrier of S -defined Function-like the Sorts of x3 -compatible total Element of K246( the Sorts of x3)

(S,x3,g) is non pair V17() V18() V19() V23() V47() ext-real V140() V141() V142() V143() V144() V145() V149() V153() Element of NAT

max ((X,x2,b),(S,x3,g)) is non pair V17() V18() V19() V23() V47() ext-real V140() V141() V142() V143() V144() V145() V149() V153() Element of NAT

Following (b,(X,x2,b)) is non empty Relation-like the carrier of X -defined Function-like the Sorts of x2 -compatible total Element of K246( the Sorts of x2)

a1 is non pair V17() V18() V19() V23() V47() ext-real V140() V141() V142() V143() V144() V145() V149() V153() Element of NAT

Following (g,a1) is non empty Relation-like the carrier of S -defined Function-like the Sorts of x3 -compatible total Element of K246( the Sorts of x3)

Following (a,a1) is non empty Relation-like the carrier of x1 -defined Function-like the Sorts of f -compatible total Element of K246( the Sorts of f)

Following (b,a1) is non empty Relation-like the carrier of X -defined Function-like the Sorts of x2 -compatible total Element of K246( the Sorts of x2)

Following (a,a1) is non empty Relation-like the carrier of x1 -defined Function-like the Sorts of f -compatible total Element of K246( the Sorts of f)

Following (g,(S,x3,g)) is non empty Relation-like the carrier of S -defined Function-like the Sorts of x3 -compatible total Element of K246( the Sorts of x3)

Following (a,(max ((X,x2,b),(S,x3,g)))) is non empty Relation-like the carrier of x1 -defined Function-like the Sorts of f -compatible total Element of K246( the Sorts of f)

X is non empty non void V79() Circuit-like ManySortedSign

InputVertices X is Element of bool the carrier of X

the carrier of X is non empty set

bool the carrier of X is set

the ResultSort of X is Relation-like the carrier' of X -defined the carrier of X -valued Function-like V30( the carrier' of X, the carrier of X) Element of bool [: the carrier' of X, the carrier of X:]

the carrier' of X is non empty set

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

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

K488( the carrier of X, the ResultSort of X) is Element of bool the carrier of X

the carrier of X \ K488( the carrier of X, the ResultSort of X) is Element of bool the carrier of X

S is non empty non void V79() Circuit-like ManySortedSign

InnerVertices S is Element of bool the carrier of S

the carrier of S is non empty set

bool the carrier of S is set

the ResultSort of S is Relation-like the carrier' of S -defined the carrier of S -valued Function-like V30( the carrier' of S, the carrier of S) Element of bool [: the carrier' of S, the carrier of S:]

the carrier' of S is non empty set

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

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

K488( the carrier of S, the ResultSort of S) is Element of bool the carrier of S

X +* S is non empty non void V79() strict ManySortedSign

x1 is non empty non void V79() Circuit-like ManySortedSign

the carrier of x1 is non empty set

x2 is non-empty finite-yielding MSAlgebra over X

the Sorts of x2 is non empty Relation-like non-empty non empty-yielding the carrier of X -defined Function-like total set

K246( the Sorts of x2) is non empty functional V93() V94() set

x3 is non-empty finite-yielding MSAlgebra over S

x2 +* x3 is strict non-empty MSAlgebra over X +* S

the Sorts of x3 is non empty Relation-like non-empty non empty-yielding the carrier of S -defined Function-like total set

K246( the Sorts of x3) is non empty functional V93() V94() set

f is non-empty finite-yielding MSAlgebra over x1

the Sorts of f is non empty Relation-like non-empty non empty-yielding the carrier of x1 -defined Function-like total set

K246( the Sorts of f) is non empty functional V93() V94() set

a is non empty Relation-like the carrier of x1 -defined Function-like the Sorts of f -compatible total Element of K246( the Sorts of f)

a | the carrier of X is Relation-like the carrier of X -defined the carrier of x1 -defined Function-like the Sorts of f -compatible set

b is non empty Relation-like the carrier of X -defined Function-like the Sorts of x2 -compatible total Element of K246( the Sorts of x2)

(X,x2,b) is non pair V17() V18() V19() V23() V47() ext-real V140() V141() V142() V143() V144() V145() V149() V153() Element of NAT

Following (a,(X,x2,b)) is non empty Relation-like the carrier of x1 -defined Function-like the Sorts of f -compatible total Element of K246( the Sorts of f)

(Following (a,(X,x2,b))) | the carrier of S is Relation-like the carrier of S -defined the carrier of x1 -defined Function-like the Sorts of f -compatible set

Following (b,(X,x2,b)) is non empty Relation-like the carrier of X -defined Function-like the Sorts of x2 -compatible total Element of K246( the Sorts of x2)

g is non empty Relation-like the carrier of S -defined Function-like the Sorts of x3 -compatible total Element of K246( the Sorts of x3)

(S,x3,g) is non pair V17() V18() V19() V23() V47() ext-real V140() V141() V142() V143() V144() V145() V149() V153() Element of NAT

Following (g,(S,x3,g)) is non empty Relation-like the carrier of S -defined Function-like the Sorts of x3 -compatible total Element of K246( the Sorts of x3)

(X,x2,b) + (S,x3,g) is non pair V17() V18() V19() V23() V47() ext-real V140() V141() V142() V143() V144() V145() V149() V153() Element of NAT

Following (a,((X,x2,b) + (S,x3,g))) is non empty Relation-like the carrier of x1 -defined Function-like the Sorts of f -compatible total Element of K246( the Sorts of f)

X is non empty non void V79() Circuit-like ManySortedSign

InputVertices X is Element of bool the carrier of X

the carrier of X is non empty set

bool the carrier of X is set

the ResultSort of X is Relation-like the carrier' of X -defined the carrier of X -valued Function-like V30( the carrier' of X, the carrier of X) Element of bool [: the carrier' of X, the carrier of X:]

the carrier' of X is non empty set

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

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

K488( the carrier of X, the ResultSort of X) is Element of bool the carrier of X

the carrier of X \ K488( the carrier of X, the ResultSort of X) is Element of bool the carrier of X

S is non empty non void V79() Circuit-like ManySortedSign

InnerVertices S is Element of bool the carrier of S

the carrier of S is non empty set

bool the carrier of S is set

the ResultSort of S is Relation-like the carrier' of S -defined the carrier of S -valued Function-like V30( the carrier' of S, the carrier of S) Element of bool [: the carrier' of S, the carrier of S:]

the carrier' of S is non empty set

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

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

K488( the carrier of S, the ResultSort of S) is Element of bool the carrier of S

X +* S is non empty non void V79() strict ManySortedSign

x1 is non empty non void V79() Circuit-like ManySortedSign

the carrier of x1 is non empty set

x2 is non-empty finite-yielding MSAlgebra over X

the Sorts of x2 is non empty Relation-like non-empty non empty-yielding the carrier of X -defined Function-like total set

K246( the Sorts of x2) is non empty functional V93() V94() set

x3 is non-empty finite-yielding MSAlgebra over S

x2 +* x3 is strict non-empty MSAlgebra over X +* S

the Sorts of x3 is non empty Relation-like non-empty non empty-yielding the carrier of S -defined Function-like total set

K246( the Sorts of x3) is non empty functional V93() V94() set

f is non-empty finite-yielding MSAlgebra over x1

the Sorts of f is non empty Relation-like non-empty non empty-yielding the carrier of x1 -defined Function-like total set

K246( the Sorts of f) is non empty functional V93() V94() set

a is non empty Relation-like the carrier of x1 -defined Function-like the Sorts of f -compatible total Element of K246( the Sorts of f)

a | the carrier of X is Relation-like the carrier of X -defined the carrier of x1 -defined Function-like the Sorts of f -compatible set

(x1,f,a) is non pair V17() V18() V19() V23() V47() ext-real V140() V141() V142() V143() V144() V145() V149() V153() Element of NAT

b is non empty Relation-like the carrier of X -defined Function-like the Sorts of x2 -compatible total Element of K246( the Sorts of x2)

(X,x2,b) is non pair V17() V18() V19() V23() V47() ext-real V140() V141() V142() V143() V144() V145() V149() V153() Element of NAT

Following (a,(X,x2,b)) is non empty Relation-like the carrier of x1 -defined Function-like the Sorts of f -compatible total Element of K246( the Sorts of f)

(Following (a,(X,x2,b))) | the carrier of S is Relation-like the carrier of S -defined the carrier of x1 -defined Function-like the Sorts of f -compatible set

g is non empty Relation-like the carrier of S -defined Function-like the Sorts of x3 -compatible total Element of K246( the Sorts of x3)

(S,x3,g) is non pair V17() V18() V19() V23() V47() ext-real V140() V141() V142() V143() V144() V145() V149() V153() Element of NAT

(X,x2,b) + (S,x3,g) is non pair V17() V18() V19() V23() V47() ext-real V140() V141() V142() V143() V144() V145() V149() V153() Element of NAT

Following (b,(X,x2,b)) is non empty Relation-like the carrier of X -defined Function-like the Sorts of x2 -compatible total Element of K246( the Sorts of x2)

a1 is non pair V17() V18() V19() V23() V47() ext-real V140() V141() V142() V143() V144() V145() V149() V153() Element of NAT

x is non pair V17() V18() V19() V23() V47() ext-real V153() set

(X,x2,b) + x is non pair V17() V18() V19() V23() V47() ext-real V140() V141() V142() V143() V144() V145() V149() V153() Element of NAT

k is non pair V17() V18() V19() V23() V47() ext-real V140() V141() V142() V143() V144() V145() V149() V153() Element of NAT

Following (g,k) is non empty Relation-like the carrier of S -defined Function-like the Sorts of x3 -compatible total Element of K246( the Sorts of x3)

(Following (a,(X,x2,b))) | the carrier of X is Relation-like the carrier of X -defined the carrier of x1 -defined Function-like the Sorts of f -compatible set

Following ((Following (a,(X,x2,b))),k) is non empty Relation-like the carrier of x1 -defined Function-like the Sorts of f -compatible total Element of K246( the Sorts of f)

(Following ((Following (a,(X,x2,b))),k)) | the carrier of S is Relation-like the carrier of S -defined the carrier of x1 -defined Function-like the Sorts of f -compatible set

Following (a,a1) is non empty Relation-like the carrier of x1 -defined Function-like the Sorts of f -compatible total Element of K246( the Sorts of f)

(Following (a,a1)) | the carrier of S is Relation-like the carrier of S -defined the carrier of x1 -defined Function-like the Sorts of f -compatible set

Following (b,a1) is non empty Relation-like the carrier of X -defined Function-like the Sorts of x2 -compatible total Element of K246( the Sorts of x2)

Following (a,a1) is non empty Relation-like the carrier of x1 -defined Function-like the Sorts of f -compatible total Element of K246( the Sorts of f)

(Following (a,a1)) | the carrier of X is Relation-like the carrier of X -defined the carrier of x1 -defined Function-like the Sorts of f -compatible set

Following (g,(S,x3,g)) is non empty Relation-like the carrier of S -defined Function-like the Sorts of x3 -compatible total Element of K246( the Sorts of x3)

Following (a,((X,x2,b) + (S,x3,g))) is non empty Relation-like the carrier of x1 -defined Function-like the Sorts of f -compatible total Element of K246( the Sorts of f)

X is non empty non void V79() Circuit-like ManySortedSign

InputVertices X is Element of bool the carrier of X

the carrier of X is non empty set

bool the carrier of X is set

the ResultSort of X is Relation-like the carrier' of X -defined the carrier of X -valued Function-like V30( the carrier' of X, the carrier of X) Element of bool [: the carrier' of X, the carrier of X:]

the carrier' of X is non empty set

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

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

K488( the carrier of X, the ResultSort of X) is Element of bool the carrier of X

the carrier of X \ K488( the carrier of X, the ResultSort of X) is Element of bool the carrier of X

S is non empty non void V79() Circuit-like ManySortedSign

InnerVertices S is Element of bool the carrier of S

the carrier of S is non empty set

bool the carrier of S is set

the ResultSort of S is Relation-like the carrier' of S -defined the carrier of S -valued Function-like V30( the carrier' of S, the carrier of S) Element of bool [: the carrier' of S, the carrier of S:]

the carrier' of S is non empty set

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

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

K488( the carrier of S, the ResultSort of S) is Element of bool the carrier of S

x1 is non empty non void V79() Circuit-like ManySortedSign

X +* S is non empty non void V79() strict ManySortedSign

the carrier of x1 is non empty set

x2 is non-empty finite-yielding MSAlgebra over X

the Sorts of x2 is non empty Relation-like non-empty non empty-yielding the carrier of X -defined Function-like total set

K246( the Sorts of x2) is non empty functional V93() V94() set

x3 is non-empty finite-yielding MSAlgebra over S

x2 +* x3 is strict non-empty MSAlgebra over X +* S

the Sorts of x3 is non empty Relation-like non-empty non empty-yielding the carrier of S -defined Function-like total set

K246( the Sorts of x3) is non empty functional V93() V94() set

f is non-empty finite-yielding MSAlgebra over x1

the Sorts of f is non empty Relation-like non-empty non empty-yielding the carrier of x1 -defined Function-like total set

K246( the Sorts of f) is non empty functional V93() V94() set

a is non empty Relation-like the carrier of x1 -defined Function-like the Sorts of f -compatible total Element of K246( the Sorts of f)

a | the carrier of X is Relation-like the carrier of X -defined the carrier of x1 -defined Function-like the Sorts of f -compatible set

(x1,f,a) is non empty Relation-like the carrier of x1 -defined Function-like the Sorts of f -compatible total Element of K246( the Sorts of f)

(x1,f,a) | the carrier of X is Relation-like the carrier of X -defined the carrier of x1 -defined Function-like the Sorts of f -compatible set

b is non empty Relation-like the carrier of X -defined Function-like the Sorts of x2 -compatible total Element of K246( the Sorts of x2)

(X,x2,b) is non pair V17() V18() V19() V23() V47() ext-real V140() V141() V142() V143() V144() V145() V149() V153() Element of NAT

Following (a,(X,x2,b)) is non empty Relation-like the carrier of x1 -defined Function-like the Sorts of f -compatible total Element of K246( the Sorts of f)

(Following (a,(X,x2,b))) | the carrier of S is Relation-like the carrier of S -defined the carrier of x1 -defined Function-like the Sorts of f -compatible set

(X,x2,b) is non empty Relation-like the carrier of X -defined Function-like the Sorts of x2 -compatible total Element of K246( the Sorts of x2)

c is non empty Relation-like the carrier of S -defined Function-like the Sorts of x3 -compatible total Element of K246( the Sorts of x3)

(x1,f,a) is non pair V17() V18() V19() V23() V47() ext-real V140() V141() V142() V143() V144() V145() V149() V153() Element of NAT

(S,x3,c) is non pair V17() V18() V19() V23() V47() ext-real V140() V141() V142() V143() V144() V145() V149() V153() Element of NAT

(X,x2,b) + (S,x3,c) is non pair V17() V18() V19() V23() V47() ext-real V140() V141() V142() V143() V144() V145() V149() V153() Element of NAT

Following (a,(x1,f,a)) is non empty Relation-like the carrier of x1 -defined Function-like the Sorts of f -compatible total Element of K246( the Sorts of f)

(Following (a,(x1,f,a))) | the carrier of X is Relation-like the carrier of X -defined the carrier of x1 -defined Function-like the Sorts of f -compatible set

Following (b,(x1,f,a)) is non empty Relation-like the carrier of X -defined Function-like the Sorts of x2 -compatible total Element of K246( the Sorts of x2)

S is non empty finite V95() set

x1 is non pair V17() V18() V19() V23() V47() ext-real V140() V141() V142() V143() V144() V145() V149() V153() Element of NAT

x1 -tuples_on S is non empty functional FinSequence-membered FinSequenceSet of S

[:(x1 -tuples_on S),S:] is Relation-like set

bool [:(x1 -tuples_on S),S:] is set

x2 is Relation-like NAT -defined Function-like finite V42(x1) FinSequence-like FinSubsequence-like V95() set

x3 is Relation-like x1 -tuples_on S -defined S -valued Function-like V30(x1 -tuples_on S,S) Element of bool [:(x1 -tuples_on S),S:]

1GateCircStr (x2,x3) is non empty non void V79() strict Circuit-like unsplit gate`1=arity gate`2=den ManySortedSign

the carrier of (1GateCircStr (x2,x3)) is non empty set

1GateCircuit (x2,x3) is strict non-empty finite-yielding gate`2=den MSAlgebra over 1GateCircStr (x2,x3)

the Sorts of (1GateCircuit (x2,x3)) is non empty Relation-like non-empty non empty-yielding the carrier of (1GateCircStr (x2,x3)) -defined Function-like total set

K246( the Sorts of (1GateCircuit (x2,x3))) is non empty functional V93() V94() set

f is non empty Relation-like the carrier of (1GateCircStr (x2,x3)) -defined Function-like the Sorts of (1GateCircuit (x2,x3)) -compatible total Element of K246( the Sorts of (1GateCircuit (x2,x3)))

x2 * f is Relation-like NAT -defined Function-like finite V95() set

proj2 (x2 * f) is finite V95() set

c is set

proj2 f is non empty set

k is set

g is non empty set

proj1 f is non empty set

x is set

f . x is set

a1 is non empty Relation-like non-empty non empty-yielding g -defined Function-like total set

proj1 a1 is non empty set

k is Element of the carrier of (1GateCircStr (x2,x3))

f . k is set

the Sorts of (1GateCircuit (x2,x3)) . k is non empty set

proj2 x2 is finite V95() set

proj1 f is non empty set

c is set

[x2,x3] is pair non empty set

{x2,x3} is non empty functional finite V95() set

{x2} is non empty functional finite V39() V93() V95() set

{{x2,x3},{x2}} is non empty finite V39() V95() set

{[x2,x3]} is non empty Relation-like Function-like finite V95() set

(proj2 x2) \/ {[x2,x3]} is non empty finite V95() set

c is Relation-like NAT -defined S -valued Function-like finite FinSequence-like FinSubsequence-like V95() FinSequence of S

len c is non pair V17() V18() V19() V23() V47() ext-real V140() V141() V142() V143() V144() V145() V149() V153() Element of NAT

len x2 is non pair V17() V18() V19() V23() V47() ext-real V140() V141() V142() V143() V144() V145() V149() V153() Element of NAT

X is set

S is set

x1 is set

x2 is set

<*X,S,x1,x2*> is non empty Relation-like NAT -defined Function-like finite V42(4) FinSequence-like FinSubsequence-like V95() set

proj2 <*X,S,x1,x2*> is non empty finite V95() set

{X,S,x1,x2} is finite V95() set

dom <*X,S,x1,x2*> is non empty finite V95() V140() V141() V142() V143() V144() V145() V147() V148() V149() V150() V151() Element of bool NAT

x3 is set

<*X,S,x1,x2*> . 1 is set

<*X,S,x1,x2*> . 2 is set

<*X,S,x1,x2*> . 3 is set

<*X,S,x1,x2*> . 4 is set

f is set

<*X,S,x1,x2*> . f is set

X is set

S is set

x1 is set

x2 is set

x3 is set

<*X,S,x1,x2,x3*> is non empty Relation-like NAT -defined Function-like finite V42(5) FinSequence-like FinSubsequence-like V95() set

proj2 <*X,S,x1,x2,x3*> is non empty finite V95() set

{X,S,x1,x2,x3} is finite V95() set

dom <*X,S,x1,x2,x3*> is non empty finite V95() V140() V141() V142() V143() V144() V145() V147() V148() V149() V150() V151() Element of bool NAT

f is set

<*X,S,x1,x2,x3*> . 1 is set

<*X,S,x1,x2,x3*> . 2 is set

<*X,S,x1,x2,x3*> . 3 is set

<*X,S,x1,x2,x3*> . 4 is set

<*X,S,x1,x2,x3*> . 5 is set

a is set

<*X,S,x1,x2,x3*> . a is set

X is non empty V79() ManySortedSign

S is set

X is Relation-like NAT -defined Function-like finite FinSequence-like FinSubsequence-like V95() set

1GateCircStr (X,S) is non empty non void V79() strict Circuit-like unsplit gate`1=arity ManySortedSign

the carrier of (1GateCircStr (X,S)) is non empty set

proj2 X is finite V95() set

[X,S] is pair non empty set

{X,S} is non empty finite V95() set

{X} is non empty functional finite V39() V93() V95() set

{{X,S},{X}} is non empty finite V39() V95() set

{[X,S]} is non empty Relation-like Function-like finite V95() set

(proj2 X) \/ {[X,S]} is non empty finite V95() set

X is ManySortedSign

x1 is non pair V17() V18() V19() V23() V47() ext-real V140() V141() V142() V143() V144() V145() V149() V153() Element of NAT

S is non empty finite V95() set

x1 -tuples_on S is non empty functional FinSequence-membered FinSequenceSet of S

[:(x1 -tuples_on S),S:] is Relation-like set

bool [:(x1 -tuples_on S),S:] is set

x3 is Relation-like x1 -tuples_on S -defined S -valued Function-like V30(x1 -tuples_on S,S) Element of bool [:(x1 -tuples_on S),S:]

x2 is Relation-like NAT -defined Function-like finite V42(x1) FinSequence-like FinSubsequence-like V95() set

1GateCircStr (x2,x3) is non empty finite non void V79() strict Circuit-like unsplit gate`1=arity gate`2=den ManySortedSign

X is non empty V79() ManySortedSign

x1 is non pair V17() V18() V19() V23() V47() ext-real V140() V141() V142() V143() V144() V145() V149() V153() Element of NAT

S is non empty finite V95() set

x1 -tuples_on S is non empty functional FinSequence-membered FinSequenceSet of S

[:(x1 -tuples_on S),S:] is Relation-like set

bool [:(x1 -tuples_on S),S:] is set

x3 is Relation-like x1 -tuples_on S -defined S -valued Function-like V30(x1 -tuples_on S,S) Element of bool [:(x1 -tuples_on S),S:]

x2 is Relation-like NAT -defined Function-like finite V42(x1) FinSequence-like FinSubsequence-like V95() set

1GateCircStr (x2,x3) is non empty finite non void V79() strict Circuit-like unsplit gate`1=arity gate`2=den ManySortedSign

S is non pair V17() V18() V19() V23() V47() ext-real V140() V141() V142() V143() V144() V145() V149() V153() Element of NAT

X is non empty finite V95() set

S -tuples_on X is non empty functional FinSequence-membered FinSequenceSet of X

[:(S -tuples_on X),X:] is Relation-like set

bool [:(S -tuples_on X),X:] is set

x2 is Relation-like S -tuples_on X -defined X -valued Function-like V30(S -tuples_on X,X) Element of bool [:(S -tuples_on X),X:]

x1 is Relation-like NAT -defined Function-like finite V42(S) FinSequence-like FinSubsequence-like V95() set

1GateCircStr (x1,x2) is non empty finite non void V79() strict Circuit-like unsplit gate`1=arity gate`2=den ManySortedSign

the non empty finite V95() set is non empty finite V95() set

the non pair V17() V18() V19() V23() V47() ext-real V140() V141() V142() V143() V144() V145() V149() V153() Element of NAT is non pair V17() V18() V19() V23() V47() ext-real V140() V141() V142() V143() V144() V145() V149() V153() Element of NAT

the Relation-like NAT -defined Function-like finite V42( the non pair V17() V18() V19() V23() V47() ext-real V140() V141() V142() V143() V144() V145() V149() V153() Element of NAT ) FinSequence-like FinSubsequence-like V95() set is Relation-like NAT -defined Function-like finite V42( the non pair V17() V18() V19() V23() V47() ext-real V140() V141() V142() V143() V144() V145() V149() V153() Element of NAT ) FinSequence-like FinSubsequence-like V95() set

the non pair V17() V18() V19() V23() V47() ext-real V140() V141() V142() V143() V144() V145() V149() V153() Element of NAT -tuples_on the non empty finite V95() set is non empty functional FinSequence-membered FinSequenceSet of the non empty finite V95() set

[:( the non pair V17() V18() V19() V23() V47() ext-real V140() V141() V142() V143() V144() V145() V149() V153() Element of NAT -tuples_on the non empty finite V95() set ), the non empty finite V95() set :] is Relation-like set

bool [:( the non pair V17() V18() V19() V23() V47() ext-real V140() V141() V142() V143() V144() V145() V149() V153() Element of NAT -tuples_on the non empty finite V95() set ), the non empty finite V95() set :] is set

the Relation-like the non pair V17() V18() V19() V23() V47() ext-real V140() V141() V142() V143() V144() V145() V149() V153() Element of NAT -tuples_on the non empty finite V95() set -defined the non empty finite V95() set -valued Function-like V30( the non pair V17() V18() V19() V23() V47() ext-real V140() V141() V142() V143() V144() V145() V149() V153() Element of NAT -tuples_on the non empty finite V95() set , the non empty finite V95() set ) Element of bool [:( the non pair V17() V18() V19() V23() V47() ext-real V140() V141() V142() V143() V144() V145() V149() V153() Element of NAT -tuples_on the non empty finite V95() set ), the non empty finite V95() set :] is Relation-like the non pair V17() V18() V19() V23() V47() ext-real V140() V141() V142() V143() V144() V145() V149() V153() Element of NAT -tuples_on the non empty finite V95() set -defined the non empty finite V95() set -valued Function-like V30( the non pair V17() V18() V19() V23() V47() ext-real V140() V141() V142() V143() V144() V145() V149() V153() Element of NAT -tuples_on the non empty finite V95() set , the non empty finite V95() set ) Element of bool [:( the non pair V17() V18() V19() V23() V47() ext-real V140() V141() V142() V143() V144() V145() V149() V153() Element of NAT -tuples_on the non empty finite V95() set ), the non empty finite V95() set :]

1GateCircStr ( the Relation-like NAT -defined Function-like finite V42( the non pair V17() V18() V19() V23() V47() ext-real V140() V141() V142() V143() V144() V145() V149() V153() Element of NAT ) FinSequence-like FinSubsequence-like V95() set , the Relation-like the non pair V17() V18() V19() V23() V47() ext-real V140() V141() V142() V143() V144() V145() V149() V153() Element of NAT -tuples_on the non empty finite V95() set -defined the non empty finite V95() set -valued Function-like V30( the non pair V17() V18() V19() V23() V47() ext-real V140() V141() V142() V143() V144() V145() V149() V153() Element of NAT -tuples_on the non empty finite V95() set , the non empty finite V95() set ) Element of bool [:( the non pair V17() V18() V19() V23() V47() ext-real V140() V141() V142() V143() V144() V145() V149() V153() Element of NAT -tuples_on the non empty finite V95() set ), the non empty finite V95() set :]) is non empty finite non void V79() strict Circuit-like unsplit gate`1=arity gate`2=den () ManySortedSign

X is non empty finite non void V79() strict Circuit-like unsplit gate`1=arity gate`2=den () ManySortedSign

S is finite-yielding MSAlgebra over X

x2 is non pair V17() V18() V19() V23() V47() ext-real V140() V141() V142() V143() V144() V145() V149() V153() Element of NAT

x1 is non empty finite V95() set

x2 -tuples_on x1 is non empty functional FinSequence-membered FinSequenceSet of x1

[:(x2 -tuples_on x1),x1:] is Relation-like set

bool [:(x2 -tuples_on x1),x1:] is set

f is Relation-like x2 -tuples_on x1 -defined x1 -valued Function-like V30(x2 -tuples_on x1,x1) Element of bool [:(x2 -tuples_on x1),x1:]

x3 is Relation-like NAT -defined Function-like finite V42(x2) FinSequence-like FinSubsequence-like V95() set

1GateCircStr (x3,f) is non empty finite non void V79() strict Circuit-like unsplit gate`1=arity gate`2=den () ManySortedSign

1GateCircuit (x3,f) is strict non-empty finite-yielding gate`2=den MSAlgebra over 1GateCircStr (x3,f)

S is non pair V17() V18() V19() V23() V47() ext-real V140() V141() V142() V143() V144() V145() V149() V153() Element of NAT

X is non empty finite V95() set

S -tuples_on X is non empty functional FinSequence-membered FinSequenceSet of X

[:(S -tuples_on X),X:] is Relation-like set

bool [:(S -tuples_on X),X:] is set

x2 is Relation-like S -tuples_on X -defined X -valued Function-like V30(S -tuples_on X,X) Element of bool [:(S -tuples_on X),X:]

x1 is Relation-like NAT -defined Function-like finite V42(S) FinSequence-like FinSubsequence-like V95() set

1GateCircStr (x1,x2) is non empty finite non void V79() strict Circuit-like unsplit gate`1=arity gate`2=den () ManySortedSign

1GateCircuit (x1,x2) is strict non-empty finite-yielding gate`2=den MSAlgebra over 1GateCircStr (x1,x2)

X is non empty finite non void V79() strict Circuit-like unsplit gate`1=arity gate`2=den () ManySortedSign

x1 is non pair V17() V18() V19() V23() V47() ext-real V140() V141() V142() V143() V144() V145() V149() V153() Element of NAT

S is non empty finite V95() set

x1 -tuples_on S is non empty functional FinSequence-membered FinSequenceSet of S

[:(x1 -tuples_on S),S:] is Relation-like set

bool [:(x1 -tuples_on S),S:] is set

x3 is Relation-like x1 -tuples_on S -defined S -valued Function-like V30(x1 -tuples_on S,S) Element of bool [:(x1 -tuples_on S),S:]

x2 is Relation-like NAT -defined Function-like finite V42(x1) FinSequence-like FinSubsequence-like V95() set

1GateCircStr (x2,x3) is non empty finite non void V79() strict Circuit-like unsplit gate`1=arity gate`2=den () ManySortedSign

1GateCircuit (x2,x3) is strict non-empty finite-yielding gate`2=den ( 1GateCircStr (x2,x3)) MSAlgebra over 1GateCircStr (x2,x3)

f is finite-yielding MSAlgebra over X

X is non empty finite non void V79() strict Circuit-like unsplit gate`1=arity gate`2=den () ManySortedSign

the carrier' of X is non empty set

union the carrier' of X is set

the carrier of X is non empty finite V95() set

x1 is non pair V17() V18() V19() V23() V47() ext-real V140() V141() V142() V143() V144() V145() V149() V153() Element of NAT

S is non empty finite V95() set

x1 -tuples_on S is non empty functional FinSequence-membered FinSequenceSet of S

[:(x1 -tuples_on S),S:] is Relation-like set

bool [:(x1 -tuples_on S),S:] is set

x3 is Relation-like x1 -tuples_on S -defined S -valued Function-like V30(x1 -tuples_on S,S) Element of bool [:(x1 -tuples_on S),S:]

x2 is Relation-like NAT -defined Function-like finite V42(x1) FinSequence-like FinSubsequence-like V95() set

1GateCircStr (x2,x3) is non empty finite non void V79() strict Circuit-like unsplit gate`1=arity gate`2=den () ManySortedSign

[x2,x3] is pair non empty set

{x2,x3} is non empty functional finite V95() set

{x2} is non empty functional finite V39() V93() V95() set

{{x2,x3},{x2}} is non empty finite V39() V95() set

{[x2,x3]} is non empty Relation-like Function-like finite V95() set

proj2 x2 is finite V95() set

(proj2 x2) \/ {[x2,x3]} is non empty finite V95() set

X is non empty finite non void V79() strict Circuit-like unsplit gate`1=arity gate`2=den () ManySortedSign

(X) is Element of the carrier of X

the carrier of X is non empty finite V95() set

the carrier' of X is non empty set

union the carrier' of X is set

x1 is non pair V17() V18() V19() V23() V47() ext-real V140() V141() V142() V143() V144() V145() V149() V153() Element of NAT

S is non empty finite V95() set

x1 -tuples_on S is non empty functional FinSequence-membered FinSequenceSet of S

[:(x1 -tuples_on S),S:] is Relation-like set

bool [:(x1 -tuples_on S),S:] is set

x3 is Relation-like x1 -tuples_on S -defined S -valued Function-like V30(x1 -tuples_on S,S) Element of bool [:(x1 -tuples_on S),S:]

x2 is Relation-like NAT -defined Function-like finite V42(x1) FinSequence-like FinSubsequence-like V95() set

1GateCircStr (x2,x3) is non empty finite non void V79() strict Circuit-like unsplit gate`1=arity gate`2=den () ManySortedSign

[x2,x3] is pair non empty set

{x2,x3} is non empty functional finite V95() set

{x2} is non empty functional finite V39() V93() V95() set

{{x2,x3},{x2}} is non empty finite V39() V95() set

{[x2,x3]} is non empty Relation-like Function-like finite V95() set

X is non empty finite non void V79() strict Circuit-like unsplit gate`1=arity gate`2=den () ManySortedSign

(X) is pair non empty Element of the carrier of X

the carrier of X is non empty finite V95() set

the carrier' of X is non empty set

union the carrier' of X is set

S is Relation-like NAT -defined Function-like finite FinSequence-like FinSubsequence-like V95() set

x1 is set

1GateCircStr (S,x1) is non empty finite non void V79() strict Circuit-like unsplit gate`1=arity ManySortedSign

[S,x1] is pair non empty set

{S,x1} is non empty finite V95() set

{S} is non empty functional finite V39() V93() V95() set

{{S,x1},{S}} is non empty finite V39() V95() set

{[S,x1]} is non empty Relation-like Function-like finite V95() set

union {[S,x1]} is set

X is non empty finite non void V79() strict Circuit-like unsplit gate`1=arity gate`2=den () ManySortedSign

InnerVertices X is finite V95() Element of bool the carrier of X

the carrier of X is non empty finite V95() set

bool the carrier of X is finite V39() V95() set

the ResultSort of X is Relation-like the carrier' of X -defined the carrier of X -valued Function-like V30( the carrier' of X, the carrier of X) Element of bool [: the carrier' of X, the carrier of X:]

the carrier' of X is non empty set

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

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

K488( the carrier of X, the ResultSort of X) is finite V95() Element of bool the carrier of X

(X) is pair non empty Element of the carrier of X

union the carrier' of X is set

{(X)} is non empty Relation-like finite V95() set

x1 is non pair V17() V18() V19() V23() V47() ext-real V140() V141() V142() V143() V144() V145() V149() V153() Element of NAT

S is non empty finite V95() set

x1 -tuples_on S is non empty functional FinSequence-membered FinSequenceSet of S

[:(x1 -tuples_on S),S:] is Relation-like set

bool [:(x1 -tuples_on S),S:] is set

x3 is Relation-like x1 -tuples_on S -defined S -valued Function-like V30(x1 -tuples_on S,S) Element of bool [:(x1 -tuples_on S),S:]

x2 is Relation-like NAT -defined Function-like finite V42(x1) FinSequence-like FinSubsequence-like V95() set

1GateCircStr (x2,x3) is non empty finite non void V79() strict Circuit-like unsplit gate`1=arity gate`2=den () ManySortedSign

[x2,x3] is pair non empty set

{x2,x3} is non empty functional finite V95() set

{x2} is non empty functional finite V39() V93() V95() set

{{x2,x3},{x2}} is non empty finite V39() V95() set

X is non empty finite non void V79() strict Circuit-like unsplit gate`1=arity gate`2=den () ManySortedSign

S is strict non-empty finite-yielding (X) MSAlgebra over X

x1 is non pair V17() V18() V19() V23() V47() ext-real V140() V141() V142() V143() V144() V145() V149() V153() Element of NAT

x2 is non empty finite V95() set

x1 -tuples_on x2 is non empty functional FinSequence-membered FinSequenceSet of x2

[:(x1 -tuples_on x2),x2:] is Relation-like set

bool [:(x1 -tuples_on x2),x2:] is set

x3 is Relation-like x1 -tuples_on x2 -defined x2 -valued Function-like V30(x1 -tuples_on x2,x2) Element of bool [:(x1 -tuples_on x2),x2:]

f is Relation-like NAT -defined Function-like finite V42(x1) FinSequence-like FinSubsequence-like V95() set

1GateCircuit (f,x3) is strict non-empty finite-yielding gate`2=den ( 1GateCircStr (f,x3)) MSAlgebra over 1GateCircStr (f,x3)

1GateCircStr (f,x3) is non empty finite non void V79() strict Circuit-like unsplit gate`1=arity gate`2=den () ManySortedSign

b is non pair V17() V18() V19() V23() V47() ext-real V140() V141() V142() V143() V144() V145() V149() V153() Element of NAT

a is non empty finite V95() set

b -tuples_on a is non empty functional FinSequence-membered FinSequenceSet of a

[:(b -tuples_on a),a:] is Relation-like set

bool [:(b -tuples_on a),a:] is set

g is Relation-like b -tuples_on a -defined a -valued Function-like V30(b -tuples_on a,a) Element of bool [:(b -tuples_on a),a:]

c is Relation-like NAT -defined Function-like finite V42(b) FinSequence-like FinSubsequence-like V95() set

1GateCircStr (c,g) is non empty finite non void V79() strict Circuit-like unsplit gate`1=arity gate`2=den () ManySortedSign

1GateCircuit (c,g) is strict non-empty finite-yielding gate`2=den ( 1GateCircStr (c,g)) MSAlgebra over 1GateCircStr (c,g)

[f,x3] is pair non empty set

{f,x3} is non empty functional finite V95() set

{f} is non empty functional finite V39() V93() V95() set

{{f,x3},{f}} is non empty finite V39() V95() set

{[f,x3]} is non empty Relation-like Function-like finite V95() set

the carrier' of (1GateCircStr (f,x3)) is non empty set

the Charact of (1GateCircuit (c,g)) is non empty Relation-like the carrier' of (1GateCircStr (c,g)) -defined Function-like total Function-yielding V34() ManySortedFunction of the Arity of (1GateCircStr (c,g)) * ( the Sorts of (1GateCircuit (c,g)) #), the ResultSort of (1GateCircStr (c,g)) * the Sorts of (1GateCircuit (c,g))

the carrier' of (1GateCircStr (c,g)) is non empty set

the Arity of (1GateCircStr (c,g)) is Relation-like the carrier' of (1GateCircStr (c,g)) -defined the carrier of (1GateCircStr (c,g)) * -valued Function-like V30( the carrier' of (1GateCircStr (c,g)), the carrier of (1GateCircStr (c,g)) * ) Function-yielding V34() Element of bool [: the carrier' of (1GateCircStr (c,g)),( the carrier of (1GateCircStr (c,g)) *):]

the carrier of (1GateCircStr (c,g)) is non empty finite V95() set

the carrier of (1GateCircStr (c,g)) * is non empty functional FinSequence-membered FinSequenceSet of the carrier of (1GateCircStr (c,g))

[: the carrier' of (1GateCircStr (c,g)),( the carrier of (1GateCircStr (c,g)) *):] is Relation-like set

bool [: the carrier' of (1GateCircStr (c,g)),( the carrier of (1GateCircStr (c,g)) *):] is set

the Sorts of (1GateCircuit (c,g)) is non empty Relation-like non-empty non empty-yielding the carrier of (1GateCircStr (c,g)) -defined Function-like total set

the Sorts of (1GateCircuit (c,g)) # is non empty Relation-like non-empty non empty-yielding the carrier of (1GateCircStr (c,g)) * -defined Function-like total set

the Arity of (1GateCircStr (c,g)) * ( the Sorts of (1GateCircuit (c,g)) #) is non empty Relation-like non-empty non empty-yielding the carrier' of (1GateCircStr (c,g)) -defined Function-like total set

the ResultSort of (1GateCircStr (c,g)) is Relation-like the carrier' of (1GateCircStr (c,g)) -defined the carrier of (1GateCircStr (c,g)) -valued Function-like V30( the carrier' of (1GateCircStr (c,g)), the carrier of (1GateCircStr (c,g))) Element of bool [: the carrier' of (1GateCircStr (c,g)), the carrier of (1GateCircStr (c,g)):]

[: the carrier' of (1GateCircStr (c,g)), the carrier of (1GateCircStr (c,g)):] is Relation-like set

bool [: the carrier' of (1GateCircStr (c,g)), the carrier of (1GateCircStr (c,g)):] is set

the ResultSort of (1GateCircStr (c,g)) * the Sorts of (1GateCircuit (c,g)) is non empty Relation-like non-empty non empty-yielding the carrier' of (1GateCircStr (c,g)) -defined Function-like total set

proj1 the Charact of (1GateCircuit (c,g)) is non empty set

[c,g] is pair non empty set

{c,g} is non empty functional finite V95() set

{c} is non empty functional finite V39() V93() V95() set

{{c,g},{c}} is non empty finite V39() V95() set

{[c,g]} is non empty Relation-like Function-like finite V95() set

X is non pair V17() V18() V19() V23() V47() ext-real V140() V141() V142() V143() V144() V145() V149() V153() Element of NAT

S is non empty finite V95() set

X -tuples_on S is non empty functional FinSequence-membered FinSequenceSet of S

[:(X -tuples_on S),S:] is Relation-like set

bool [:(X -tuples_on S),S:] is set

x1 is Relation-like X -tuples_on S -defined S -valued Function-like V30(X -tuples_on S,S) Element of bool [:(X -tuples_on S),S:]

x2 is Relation-like NAT -defined Function-like finite V42(X) FinSequence-like FinSubsequence-like V95() set

1GateCircStr (x2,x1) is non empty finite non void V79() strict Circuit-like unsplit gate`1=arity gate`2=den () ManySortedSign

the carrier of (1GateCircStr (x2,x1)) is non empty finite V95() set

1GateCircuit (x2,x1) is strict non-empty finite-yielding gate`2=den ( 1GateCircStr (x2,x1)) MSAlgebra over 1GateCircStr (x2,x1)

the Sorts of (1GateCircuit (x2,x1)) is non empty Relation-like non-empty non empty-yielding the carrier of (1GateCircStr (x2,x1)) -defined Function-like total set

K246( the Sorts of (1GateCircuit (x2,x1))) is non empty functional V93() V94() set

((1GateCircStr (x2,x1))) is pair non empty Element of the carrier of (1GateCircStr (x2,x1))

the carrier' of (1GateCircStr (x2,x1)) is non empty set

union the carrier' of (1GateCircStr (x2,x1)) is set

x3 is non empty Relation-like the carrier of (1GateCircStr (x2,x1)) -defined Function-like the Sorts of (1GateCircuit (x2,x1)) -compatible total Element of K246( the Sorts of (1GateCircuit (x2,x1)))

Following x3 is non empty Relation-like the carrier of (1GateCircStr (x2,x1)) -defined Function-like the Sorts of (1GateCircuit (x2,x1)) -compatible total Element of K246( the Sorts of (1GateCircuit (x2,x1)))

(Following x3) . ((1GateCircStr (x2,x1))) is set

x2 * x3 is Relation-like NAT -defined Function-like finite V95() set

x1 . (x2 * x3) is set

[x2,x1] is pair non empty set

{x2,x1} is non empty functional finite V95() set

{x2} is non empty functional finite V39() V93() V95() set

{{x2,x1},{x2}} is non empty finite V39() V95() set

X is non empty finite non void V79() strict Circuit-like unsplit gate`1=arity gate`2=den () ManySortedSign

the carrier of X is non empty finite V95() set

S is strict non-empty finite-yielding (X) MSAlgebra over X

the Sorts of S is non empty Relation-like non-empty non empty-yielding the carrier of X -defined Function-like total set

K246( the Sorts of S) is non empty functional V93() V94() set

x1 is non empty Relation-like the carrier of X -defined Function-like the Sorts of S -compatible total Element of K246( the Sorts of S)

Following x1 is non empty Relation-like the carrier of X -defined Function-like the Sorts of S -compatible total Element of K246( the Sorts of S)

x3 is non pair V17() V18() V19() V23() V47() ext-real V140() V141() V142() V143() V144() V145() V149() V153() Element of NAT

x2 is non empty finite V95() set

x3 -tuples_on x2 is non empty functional FinSequence-membered FinSequenceSet of x2

[:(x3 -tuples_on x2),x2:] is Relation-like set

bool [:(x3 -tuples_on x2),x2:] is set

a is Relation-like x3 -tuples_on x2 -defined x2 -valued Function-like V30(x3 -tuples_on x2,x2) Element of bool [:(x3 -tuples_on x2),x2:]

f is Relation-like NAT -defined Function-like finite V42(x3) FinSequence-like FinSubsequence-like V95() set

1GateCircStr (f,a) is non empty finite non void V79() strict Circuit-like unsplit gate`1=arity gate`2=den () ManySortedSign

1GateCircuit (f,a) is strict non-empty finite-yielding gate`2=den ( 1GateCircStr (f,a)) MSAlgebra over 1GateCircStr (f,a)

X is non empty non void V79() Circuit-like ManySortedSign

S is non-empty finite-yielding MSAlgebra over X

x3 is non pair V17() V18() V19() V23() V47() ext-real V140() V141() V142() V143() V144() V145() V149() V153() Element of NAT

x2 is non empty finite V95() set

x3 -tuples_on x2 is non empty functional FinSequence-membered FinSequenceSet of x2

[:(x3 -tuples_on x2),x2:] is Relation-like set

bool [:(x3 -tuples_on x2),x2:] is set

a is Relation-like x3 -tuples_on x2 -defined x2 -valued Function-like V30(x3 -tuples_on x2,x2) Element of bool [:(x3 -tuples_on x2),x2:]

f is Relation-like NAT -defined Function-like finite V42(x3) FinSequence-like FinSubsequence-like V95() set

1GateCircStr (f,a) is non empty finite non void V79() strict Circuit-like unsplit gate`1=arity gate`2=den () ManySortedSign

1GateCircuit (f,a) is strict non-empty finite-yielding gate`2=den ( 1GateCircStr (f,a)) MSAlgebra over 1GateCircStr (f,a)

x1 is non empty finite non void V79() strict Circuit-like unsplit gate`1=arity gate`2=den () ManySortedSign

the carrier of X is non empty set

the Sorts of S is non empty Relation-like non-empty non empty-yielding the carrier of X -defined Function-like total set

K246( the Sorts of S) is non empty functional V93() V94() set

x3 is non empty Relation-like the carrier of X -defined Function-like the Sorts of S -compatible total Element of K246( the Sorts of S)

Following (x3,1) is non empty Relation-like the carrier of X -defined Function-like the Sorts of S -compatible total Element of K246( the Sorts of S)

the carrier of x1 is non empty finite V95() set

x2 is strict non-empty finite-yielding (x1) MSAlgebra over x1

the Sorts of x2 is non empty Relation-like non-empty non empty-yielding the carrier of x1 -defined Function-like total set

K246( the Sorts of x2) is non empty functional V93() V94() set

f is non empty Relation-like the carrier of x1 -defined Function-like the Sorts of x2 -compatible total Element of K246( the Sorts of x2)

Following f is non empty Relation-like the carrier of x1 -defined Function-like the Sorts of x2 -compatible total Element of K246( the Sorts of x2)

X is non empty finite non void V79() strict Circuit-like unsplit gate`1=arity gate`2=den () ManySortedSign

the carrier of X is non empty finite V95() set

S is strict non-empty finite-yielding (X) (X) (X) MSAlgebra over X

the Sorts of S is non empty Relation-like non-empty non empty-yielding the carrier of X -defined Function-like total set

K246( the Sorts of S) is non empty functional V93() V94() set

x1 is non empty Relation-like the carrier of X -defined Function-like the Sorts of S -compatible total Element of K246( the Sorts of S)

(X,S,x1) is non empty Relation-like the carrier of X -defined Function-like the Sorts of S -compatible total Element of K246( the Sorts of S)

Following x1 is non empty Relation-like the carrier of X -defined Function-like the Sorts of S -compatible total Element of K246( the Sorts of S)

Following (x1,1) is non empty Relation-like the carrier of X -defined Function-like the Sorts of S -compatible total Element of K246( the Sorts of S)

X is non empty finite non void V79() strict Circuit-like unsplit gate`1=arity gate`2=den () ManySortedSign

the carrier of X is non empty finite V95() set

S is strict non-empty finite-yielding (X) (X) (X) MSAlgebra over X

the Sorts of S is non empty Relation-like non-empty non empty-yielding the carrier of X -defined Function-like total set

K246( the Sorts of S) is non empty functional V93() V94() set

x1 is non empty Relation-like the carrier of X -defined Function-like the Sorts of S -compatible total Element of K246( the Sorts of S)

(X,S,x1) is non pair V17() V18() V19() V23() V47() ext-real V140() V141() V142() V143() V144() V145() V149() V153() Element of NAT

Following x1 is non empty Relation-like the carrier of X -defined Function-like the Sorts of S -compatible total Element of K246( the Sorts of S)

Following (x1,1) is non empty Relation-like the carrier of X -defined Function-like the Sorts of S -compatible total Element of K246( the Sorts of S)

F

F

{F

1 -tuples_on F

[:(1 -tuples_on F

bool [:(1 -tuples_on F

X is Relation-like 1 -tuples_on F

<*F

1GateCircStr (<*F

S is non empty finite non void V79() strict Circuit-like unsplit gate`1=arity gate`2=den () ManySortedSign

InputVertices S is finite V95() Element of bool the carrier of S

the carrier of S is non empty finite V95() set

bool the carrier of S is finite V39() V95() set

the ResultSort of S is Relation-like the carrier' of S -defined the carrier of S -valued Function-like V30( the carrier' of S, the carrier of S) Element of bool [: the carrier' of S, the carrier of S:]

the carrier' of S is non empty set

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

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

K488( the carrier of S, the ResultSort of S) is finite V95() Element of bool the carrier of S

the carrier of S \ K488( the carrier of S, the ResultSort of S) is finite V95() Element of bool the carrier of S

(S) is pair non empty Element of the carrier of S

union the carrier' of S is set

1GateCircuit (<*F

x1 is strict non-empty finite-yielding (S) (S) (S) MSAlgebra over S

the Sorts of x1 is non empty Relation-like non-empty non empty-yielding the carrier of S -defined Function-like total set

K246( the Sorts of x1) is non empty functional V93() V94() set

proj2 <*F

x2 is non empty Relation-like the carrier of S -defined Function-like the Sorts of x1 -compatible total Element of K246( the Sorts of x1)

(S,x1,x2) is non empty Relation-like the carrier of S -defined Function-like the Sorts of x1 -compatible total Element of K246( the Sorts of x1)

(S,x1,x2) . (S) is set

x2 . F

F

<*F

dom <*F