:: 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<sub>2</sub>() is non empty finite V95() set
F<sub>1</sub>() is set
{F<sub>1</sub>()} is non empty finite V95() set
1 -tuples_on F<sub>2</sub>() is non empty functional FinSequence-membered FinSequenceSet of F<sub>2</sub>()
[:(1 -tuples_on F<sub>2</sub>()),F<sub>2</sub>():] is Relation-like set
bool [:(1 -tuples_on F<sub>2</sub>()),F<sub>2</sub>():] is set
X is Relation-like 1 -tuples_on F<sub>2</sub>() -defined F<sub>2</sub>() -valued Function-like V30(1 -tuples_on F<sub>2</sub>(),F<sub>2</sub>()) Element of bool [:(1 -tuples_on F<sub>2</sub>()),F<sub>2</sub>():]
<*F<sub>1</sub>()*> is non empty Relation-like NAT -defined Function-like finite V42(1) FinSequence-like FinSubsequence-like V95() set
1GateCircStr (<*F<sub>1</sub>()*>,X) is non empty finite non void V79() strict Circuit-like unsplit gate`1=arity gate`2=den () ManySortedSign
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<sub>1</sub>()*>,X) is strict non-empty finite-yielding gate`2=den ( 1GateCircStr (<*F₁()*>,X)) ( 1GateCircStr (<*F₁()*>,X)) ( 1GateCircStr (<*F₁()*>,X)) MSAlgebra over 1GateCircStr (<*F₁()*>,X)
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₁()*> is non empty finite V95() set
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₁() is set
F₃((x2 . F₁())) is Element of F₂()
<*F₁()*> * x2 is Relation-like NAT -defined Function-like finite V95() set
dom <*F₁()*> is non empty finite V95() V140()