REAL is set
NAT is non empty V5() V7() V8() V9() non finite V44() V45() countable denumerable Element of K19(REAL)
K19(REAL) is set
COMPLEX is set
RAT is set
INT is set
K20(COMPLEX,COMPLEX) is Relation-like set
K19(K20(COMPLEX,COMPLEX)) is set
K20(K20(COMPLEX,COMPLEX),COMPLEX) is Relation-like set
K19(K20(K20(COMPLEX,COMPLEX),COMPLEX)) is set
K20(REAL,REAL) is Relation-like set
K19(K20(REAL,REAL)) is set
K20(K20(REAL,REAL),REAL) is Relation-like set
K19(K20(K20(REAL,REAL),REAL)) is set
K20(RAT,RAT) is Relation-like set
K19(K20(RAT,RAT)) is set
K20(K20(RAT,RAT),RAT) is Relation-like set
K19(K20(K20(RAT,RAT),RAT)) is set
K20(INT,INT) is Relation-like set
K19(K20(INT,INT)) is set
K20(K20(INT,INT),INT) is Relation-like set
K19(K20(K20(INT,INT),INT)) is set
K20(NAT,NAT) is V5() Relation-like non finite set
K20(K20(NAT,NAT),NAT) is V5() Relation-like non finite set
K19(K20(K20(NAT,NAT),NAT)) is V5() non finite set
NAT is non empty V5() V7() V8() V9() non finite V44() V45() countable denumerable set
K19(NAT) is V5() non finite set
K19(NAT) is V5() non finite set
BOOLEAN is non empty set
0 is V1() V2() V3() empty V7() V8() V9() V11() V12() V13() V14() Relation-like non-empty empty-yielding NAT -defined Function-like one-to-one constant functional finite finite-yielding V43() V44() V46( {} ) FinSequence-like FinSubsequence-like FinSequence-membered Cardinal-yielding with_common_domain countable Element of NAT
{} is V1() V2() V3() empty V7() V8() V9() V11() V12() V13() V14() Relation-like non-empty empty-yielding NAT -defined Function-like one-to-one constant functional finite finite-yielding V43() V44() V46( {} ) FinSequence-like FinSubsequence-like FinSequence-membered Cardinal-yielding with_common_domain countable set
the V1() V2() V3() empty V7() V8() V9() V11() V12() V13() V14() Relation-like non-empty empty-yielding NAT -defined Function-like one-to-one constant functional finite finite-yielding V43() V44() V46( {} ) FinSequence-like FinSubsequence-like FinSequence-membered Cardinal-yielding with_common_domain countable set is V1() V2() V3() empty V7() V8() V9() V11() V12() V13() V14() Relation-like non-empty empty-yielding NAT -defined Function-like one-to-one constant functional finite finite-yielding V43() V44() V46( {} ) FinSequence-like FinSubsequence-like FinSequence-membered Cardinal-yielding with_common_domain countable set
1 is V1() V2() V3() non empty V7() V8() V9() V13() V14() finite V44() countable Element of NAT
{0,1} is non empty finite V43() countable set
{{},1} is non empty finite V43() countable set
K363() is set
K19(K363()) is set
K364() is Element of K19(K363())
K404() is non empty V98() L10()
the carrier of K404() is non empty set
K367( the carrier of K404()) is non empty M24( the carrier of K404())
K403(K404()) is Element of K19(K367( the carrier of K404()))
K19(K367( the carrier of K404())) is set
K20(K403(K404()),NAT) is Relation-like set
K19(K20(K403(K404()),NAT)) is set
K20(NAT,K403(K404())) is Relation-like set
K19(K20(NAT,K403(K404()))) is set
2 is V1() V2() V3() non empty V7() V8() V9() V13() V14() finite V44() countable Element of NAT
3 is V1() V2() V3() non empty V7() V8() V9() V13() V14() finite V44() countable Element of NAT
x is set
y is set
c is set
[y,c] is pair set
{y,c} is non empty finite countable set
{y} is non empty V5() finite V46(1) countable set
{{y,c},{y}} is non empty finite V43() countable set
x is set
y is set
[x,y] is non empty pair set
{x,y} is non empty finite countable set
{x} is non empty V5() finite V46(1) countable set
{{x,y},{x}} is non empty finite V43() countable set
x is V1() V3() V7() V8() V9() V13() V14() finite V44() countable set
y is set
c is set
[y,c] is non empty pair set
{y,c} is non empty finite countable set
{y} is non empty V5() finite V46(1) countable set
{{y,c},{y}} is non empty finite V43() countable set
{ b1 where b1 is V1() V3() V7() V8() V9() V13() V14() finite V44() countable Element of NAT : b1 < x } is set
x is set
y is non empty pair set
x is non pair set
{x} is non empty V5() finite V46(1) countable set
y is non empty pair set
y is non pair set
{x,y} is non empty finite countable set
c is non empty pair set
c is non pair set
{x,y,c} is finite countable set
S1 is non empty pair set
the non pair set is non pair set
{ the non pair set } is non empty V5() finite V46(1) countable () set
x is () set
y is () set
x \/ y is set
c is non empty pair set
x is () set
y is set
x \ y is Element of K19(x)
K19(x) is set
c is non empty pair set
x /\ y is set
c is non empty pair set
y /\ x is () set
x is non empty pair set
{x} is non empty V5() finite V46(1) countable set
y is set
y is non empty pair set
{x,y} is non empty finite countable set
c is set
c is non empty pair set
{x,y,c} is finite countable set
S1 is set
x is set
y is non empty set
the Element of y is Element of y
S1 is set
S2 is set
[S1,S2] is non empty pair set
{S1,S2} is non empty finite countable set
{S1} is non empty V5() finite V46(1) countable set
{{S1,S2},{S1}} is non empty finite V43() countable set
x is non pair set
<*x*> is non empty V5() Relation-like NAT -defined Function-like constant finite V46(1) FinSequence-like FinSubsequence-like countable set
y is set
proj1 <*x*> is non empty V5() finite V46(1) countable set
<*x*> . y is set
dom <*x*> is non empty V5() finite V46(1) countable Element of K19(NAT)
proj2 <*x*> is non empty V5() finite V46(1) countable set
{x} is non empty V5() finite V46(1) countable () set
y is non pair set
<*x,y*> is non empty Relation-like NAT -defined Function-like finite V46(2) FinSequence-like FinSubsequence-like countable set
c is set
proj1 <*x,y*> is non empty finite V46(2) countable set
<*x,y*> . c is set
dom <*x,y*> is non empty finite V46(2) countable Element of K19(NAT)
proj2 <*x,y*> is non empty finite countable set
{x,y} is non empty finite countable () set
c is non pair set
<*x,y,c*> is non empty Relation-like NAT -defined Function-like finite V46(3) FinSequence-like FinSubsequence-like countable set
S1 is set
proj1 <*x,y,c*> is non empty finite V46(3) countable set
<*x,y,c*> . S1 is set
dom <*x,y,c*> is non empty finite V46(3) countable Element of K19(NAT)
proj2 <*x,y,c*> is non empty finite countable set
{x,y,c} is finite countable () set
x is Relation-like Function-like set
proj2 x is set
proj1 x is set
y is non empty pair set
c is set
x . c is set
x is V1() V3() V7() V8() V9() V13() V14() non pair finite V44() countable set
Seg x is finite V46(x) countable Element of K19(NAT)
id (Seg x) is Relation-like Seg x -defined Seg x -valued Function-like one-to-one total finite countable Element of K19(K20((Seg x),(Seg x)))
K20((Seg x),(Seg x)) is Relation-like finite countable set
K19(K20((Seg x),(Seg x))) is finite V43() countable set
y is Relation-like NAT -defined Function-like finite FinSequence-like FinSubsequence-like countable set
len y is V1() V3() V7() V8() V9() V13() V14() non pair finite V44() countable Element of NAT
idseq x is Relation-like NAT -defined Function-like finite V46(x) FinSequence-like FinSubsequence-like countable set
len (idseq x) is V1() V3() V7() V8() V9() V13() V14() non pair finite V44() countable Element of NAT
c is Relation-like NAT -defined Function-like finite V46(x) FinSequence-like FinSubsequence-like countable set
S1 is set
proj1 c is finite V46(x) countable set
c . S1 is set
dom c is finite V46(x) countable Element of K19(NAT)
the V1() V3() V7() V8() V9() V13() V14() non pair finite V44() countable set is V1() V3() V7() V8() V9() V13() V14() non pair finite V44() countable set
the Relation-like NAT -defined Function-like one-to-one finite V46( the V1() V3() V7() V8() V9() V13() V14() non pair finite V44() countable set ) FinSequence-like FinSubsequence-like countable () set is Relation-like NAT -defined Function-like one-to-one finite V46( the V1() V3() V7() V8() V9() V13() V14() non pair finite V44() countable set ) FinSequence-like FinSubsequence-like countable () set
x is Relation-like Function-like () set
proj2 x is set
x is non empty V74() ManySortedSign
y is non empty V74() ManySortedSign
InnerVertices x is Element of K19( the carrier of x)
the carrier of x is non empty set
K19( the carrier of x) is set
the ResultSort of x is Relation-like Function-like V29( the carrier' of x, the carrier of x) Element of K19(K20( the carrier' of x, the carrier of x))
the carrier' of x is set
K20( the carrier' of x, the carrier of x) is Relation-like set
K19(K20( the carrier' of x, the carrier of x)) is set
K480( the carrier of x, the ResultSort of x) is Element of K19( the carrier of x)
InnerVertices y is Element of K19( the carrier of y)
the carrier of y is non empty set
K19( the carrier of y) is set
the ResultSort of y is Relation-like Function-like V29( the carrier' of y, the carrier of y) Element of K19(K20( the carrier' of y, the carrier of y))
the carrier' of y is set
K20( the carrier' of y, the carrier of y) is Relation-like set
K19(K20( the carrier' of y, the carrier of y)) is set
K480( the carrier of y, the ResultSort of y) is Element of K19( the carrier of y)
x +* y is non empty V74() strict ManySortedSign
InnerVertices (x +* y) is Element of K19( the carrier of (x +* y))
the carrier of (x +* y) is non empty set
K19( the carrier of (x +* y)) is set
the ResultSort of (x +* y) is Relation-like Function-like V29( the carrier' of (x +* y), the carrier of (x +* y)) Element of K19(K20( the carrier' of (x +* y), the carrier of (x +* y)))
the carrier' of (x +* y) is set
K20( the carrier' of (x +* y), the carrier of (x +* y)) is Relation-like set
K19(K20( the carrier' of (x +* y), the carrier of (x +* y))) is set
K480( the carrier of (x +* y), the ResultSort of (x +* y)) is Element of K19( the carrier of (x +* y))
c is Relation-like set
S1 is Relation-like set
c \/ S1 is Relation-like set
x is non empty V74() Circuit-like unsplit gate`1=arity ManySortedSign
InnerVertices x is Element of K19( the carrier of x)
the carrier of x is non empty set
K19( the carrier of x) is set
the ResultSort of x is Relation-like Function-like V29( the carrier' of x, the carrier of x) Element of K19(K20( the carrier' of x, the carrier of x))
the carrier' of x is set
K20( the carrier' of x, the carrier of x) is Relation-like set
K19(K20( the carrier' of x, the carrier of x)) is set
K480( the carrier of x, the ResultSort of x) is Element of K19( the carrier of x)
y is non empty V74() Circuit-like unsplit gate`1=arity ManySortedSign
InnerVertices y is Element of K19( the carrier of y)
the carrier of y is non empty set
K19( the carrier of y) is set
the ResultSort of y is Relation-like Function-like V29( the carrier' of y, the carrier of y) Element of K19(K20( the carrier' of y, the carrier of y))
the carrier' of y is set
K20( the carrier' of y, the carrier of y) is Relation-like set
K19(K20( the carrier' of y, the carrier of y)) is set
K480( the carrier of y, the ResultSort of y) is Element of K19( the carrier of y)
x +* y is non empty V74() strict Circuit-like unsplit gate`1=arity ManySortedSign
InnerVertices (x +* y) is Element of K19( the carrier of (x +* y))
the carrier of (x +* y) is non empty set
K19( the carrier of (x +* y)) is set
the ResultSort of (x +* y) is Relation-like Function-like V29( the carrier' of (x +* y), the carrier of (x +* y)) Element of K19(K20( the carrier' of (x +* y), the carrier of (x +* y)))
the carrier' of (x +* y) is set
K20( the carrier' of (x +* y), the carrier of (x +* y)) is Relation-like set
K19(K20( the carrier' of (x +* y), the carrier of (x +* y))) is set
K480( the carrier of (x +* y), the ResultSort of (x +* y)) is Element of K19( the carrier of (x +* y))
x is non empty V74() ManySortedSign
y is non empty V74() ManySortedSign
InnerVertices y is Element of K19( the carrier of y)
the carrier of y is non empty set
K19( the carrier of y) is set
the ResultSort of y is Relation-like Function-like V29( the carrier' of y, the carrier of y) Element of K19(K20( the carrier' of y, the carrier of y))
the carrier' of y is set
K20( the carrier' of y, the carrier of y) is Relation-like set
K19(K20( the carrier' of y, the carrier of y)) is set
K480( the carrier of y, the ResultSort of y) is Element of K19( the carrier of y)
InputVertices x is Element of K19( the carrier of x)
the carrier of x is non empty set
K19( the carrier of x) is set
the ResultSort of x is Relation-like Function-like V29( the carrier' of x, the carrier of x) Element of K19(K20( the carrier' of x, the carrier of x))
the carrier' of x is set
K20( the carrier' of x, the carrier of x) is Relation-like set
K19(K20( the carrier' of x, the carrier of x)) is set
K480( the carrier of x, the ResultSort of x) is Element of K19( the carrier of x)
the carrier of x \ K480( the carrier of x, the ResultSort of x) is Element of K19( the carrier of x)
x +* y is non empty V74() strict ManySortedSign
InputVertices (x +* y) is Element of K19( the carrier of (x +* y))
the carrier of (x +* y) is non empty set
K19( the carrier of (x +* y)) is set
the ResultSort of (x +* y) is Relation-like Function-like V29( the carrier' of (x +* y), the carrier of (x +* y)) Element of K19(K20( the carrier' of (x +* y), the carrier of (x +* y)))
the carrier' of (x +* y) is set
K20( the carrier' of (x +* y), the carrier of (x +* y)) is Relation-like set
K19(K20( the carrier' of (x +* y), the carrier of (x +* y))) is set
K480( the carrier of (x +* y), the ResultSort of (x +* y)) is Element of K19( the carrier of (x +* y))
the carrier of (x +* y) \ K480( the carrier of (x +* y), the ResultSort of (x +* y)) is Element of K19( the carrier of (x +* y))
InputVertices y is Element of K19( the carrier of y)
the carrier of y \ K480( the carrier of y, the ResultSort of y) is Element of K19( the carrier of y)
InnerVertices x is Element of K19( the carrier of x)
(InputVertices y) \ (InnerVertices x) is Element of K19( the carrier of y)
(InputVertices x) \/ ((InputVertices y) \ (InnerVertices x)) is set
InnerVertices (x +* y) is Element of K19( the carrier of (x +* y))
proj2 the ResultSort of (x +* y) is set
proj2 the ResultSort of x is set
proj2 the ResultSort of y is set
(proj2 the ResultSort of x) \/ (proj2 the ResultSort of y) is set
the carrier of x \/ the carrier of y is non empty set
A1 is set
(InputVertices x) \/ (InputVertices y) is set
A1 is set
A1 is set
(InputVertices y) \ (proj2 the ResultSort of x) is Element of K19( the carrier of y)
x is set
y is set
c is set
S1 is set
S2 is set
[S1,S2] is non empty pair set
{S1,S2} is non empty finite countable set
{S1} is non empty V5() finite V46(1) countable set
{{S1,S2},{S1}} is non empty finite V43() countable set
x is non empty V74() Circuit-like unsplit gate`1=arity ManySortedSign
InputVertices x is Element of K19( the carrier of x)
the carrier of x is non empty set
K19( the carrier of x) is set
the ResultSort of x is Relation-like Function-like V29( the carrier' of x, the carrier of x) Element of K19(K20( the carrier' of x, the carrier of x))
the carrier' of x is set
K20( the carrier' of x, the carrier of x) is Relation-like set
K19(K20( the carrier' of x, the carrier of x)) is set
K480( the carrier of x, the ResultSort of x) is Element of K19( the carrier of x)
the carrier of x \ K480( the carrier of x, the ResultSort of x) is Element of K19( the carrier of x)
y is non empty V74() Circuit-like unsplit gate`1=arity ManySortedSign
InnerVertices y is Element of K19( the carrier of y)
the carrier of y is non empty set
K19( the carrier of y) is set
the ResultSort of y is Relation-like Function-like V29( the carrier' of y, the carrier of y) Element of K19(K20( the carrier' of y, the carrier of y))
the carrier' of y is set
K20( the carrier' of y, the carrier of y) is Relation-like set
K19(K20( the carrier' of y, the carrier of y)) is set
K480( the carrier of y, the ResultSort of y) is Element of K19( the carrier of y)
x +* y is non empty V74() strict Circuit-like unsplit gate`1=arity ManySortedSign
InputVertices (x +* y) is Element of K19( the carrier of (x +* y))
the carrier of (x +* y) is non empty set
K19( the carrier of (x +* y)) is set
the ResultSort of (x +* y) is Relation-like Function-like V29( the carrier' of (x +* y), the carrier of (x +* y)) Element of K19(K20( the carrier' of (x +* y), the carrier of (x +* y)))
the carrier' of (x +* y) is set
K20( the carrier' of (x +* y), the carrier of (x +* y)) is Relation-like set
K19(K20( the carrier' of (x +* y), the carrier of (x +* y))) is set
K480( the carrier of (x +* y), the ResultSort of (x +* y)) is Element of K19( the carrier of (x +* y))
the carrier of (x +* y) \ K480( the carrier of (x +* y), the ResultSort of (x +* y)) is Element of K19( the carrier of (x +* y))
InputVertices y is Element of K19( the carrier of y)
the carrier of y \ K480( the carrier of y, the ResultSort of y) is Element of K19( the carrier of y)
InnerVertices x is Element of K19( the carrier of x)
(InputVertices y) \ (InnerVertices x) is Element of K19( the carrier of y)
(InputVertices x) \/ ((InputVertices y) \ (InnerVertices x)) is set
x is non empty V74() Circuit-like unsplit gate`1=arity ManySortedSign
InputVertices x is Element of K19( the carrier of x)
the carrier of x is non empty set
K19( the carrier of x) is set
the ResultSort of x is Relation-like Function-like V29( the carrier' of x, the carrier of x) Element of K19(K20( the carrier' of x, the carrier of x))
the carrier' of x is set
K20( the carrier' of x, the carrier of x) is Relation-like set
K19(K20( the carrier' of x, the carrier of x)) is set
K480( the carrier of x, the ResultSort of x) is Element of K19( the carrier of x)
the carrier of x \ K480( the carrier of x, the ResultSort of x) is Element of K19( the carrier of x)
InnerVertices x is Element of K19( the carrier of x)
y is non empty V74() Circuit-like unsplit gate`1=arity ManySortedSign
InputVertices y is Element of K19( the carrier of y)
the carrier of y is non empty set
K19( the carrier of y) is set
the ResultSort of y is Relation-like Function-like V29( the carrier' of y, the carrier of y) Element of K19(K20( the carrier' of y, the carrier of y))
the carrier' of y is set
K20( the carrier' of y, the carrier of y) is Relation-like set
K19(K20( the carrier' of y, the carrier of y)) is set
K480( the carrier of y, the ResultSort of y) is Element of K19( the carrier of y)
the carrier of y \ K480( the carrier of y, the ResultSort of y) is Element of K19( the carrier of y)
InnerVertices y is Element of K19( the carrier of y)
x +* y is non empty V74() strict Circuit-like unsplit gate`1=arity ManySortedSign
InputVertices (x +* y) is Element of K19( the carrier of (x +* y))
the carrier of (x +* y) is non empty set
K19( the carrier of (x +* y)) is set
the ResultSort of (x +* y) is Relation-like Function-like V29( the carrier' of (x +* y), the carrier of (x +* y)) Element of K19(K20( the carrier' of (x +* y), the carrier of (x +* y)))
the carrier' of (x +* y) is set
K20( the carrier' of (x +* y), the carrier of (x +* y)) is Relation-like set
K19(K20( the carrier' of (x +* y), the carrier of (x +* y))) is set
K480( the carrier of (x +* y), the ResultSort of (x +* y)) is Element of K19( the carrier of (x +* y))
the carrier of (x +* y) \ K480( the carrier of (x +* y), the ResultSort of (x +* y)) is Element of K19( the carrier of (x +* y))
(InputVertices x) \/ (InputVertices y) is set
(InputVertices y) \ (InnerVertices x) is Element of K19( the carrier of y)
(InputVertices x) \/ ((InputVertices y) \ (InnerVertices x)) is set
x is non empty V74() ManySortedSign
y is non empty V74() ManySortedSign
InputVertices x is Element of K19( the carrier of x)
the carrier of x is non empty set
K19( the carrier of x) is set
the ResultSort of x is Relation-like Function-like V29( the carrier' of x, the carrier of x) Element of K19(K20( the carrier' of x, the carrier of x))
the carrier' of x is set
K20( the carrier' of x, the carrier of x) is Relation-like set
K19(K20( the carrier' of x, the carrier of x)) is set
K480( the carrier of x, the ResultSort of x) is Element of K19( the carrier of x)
the carrier of x \ K480( the carrier of x, the ResultSort of x) is Element of K19( the carrier of x)
InputVertices y is Element of K19( the carrier of y)
the carrier of y is non empty set
K19( the carrier of y) is set
the ResultSort of y is Relation-like Function-like V29( the carrier' of y, the carrier of y) Element of K19(K20( the carrier' of y, the carrier of y))
the carrier' of y is set
K20( the carrier' of y, the carrier of y) is Relation-like set
K19(K20( the carrier' of y, the carrier of y)) is set
K480( the carrier of y, the ResultSort of y) is Element of K19( the carrier of y)
the carrier of y \ K480( the carrier of y, the ResultSort of y) is Element of K19( the carrier of y)
x +* y is non empty V74() strict ManySortedSign
InputVertices (x +* y) is Element of K19( the carrier of (x +* y))
the carrier of (x +* y) is non empty set
K19( the carrier of (x +* y)) is set
the ResultSort of (x +* y) is Relation-like Function-like V29( the carrier' of (x +* y), the carrier of (x +* y)) Element of K19(K20( the carrier' of (x +* y), the carrier of (x +* y)))
the carrier' of (x +* y) is set
K20( the carrier' of (x +* y), the carrier of (x +* y)) is Relation-like set
K19(K20( the carrier' of (x +* y), the carrier of (x +* y))) is set
K480( the carrier of (x +* y), the ResultSort of (x +* y)) is Element of K19( the carrier of (x +* y))
the carrier of (x +* y) \ K480( the carrier of (x +* y), the ResultSort of (x +* y)) is Element of K19( the carrier of (x +* y))
(InputVertices x) \/ (InputVertices y) is set
c is non empty pair set
x is non empty V74() Circuit-like unsplit gate`1=arity ManySortedSign
InputVertices x is Element of K19( the carrier of x)
the carrier of x is non empty set
K19( the carrier of x) is set
the ResultSort of x is Relation-like Function-like V29( the carrier' of x, the carrier of x) Element of K19(K20( the carrier' of x, the carrier of x))
the carrier' of x is set
K20( the carrier' of x, the carrier of x) is Relation-like set
K19(K20( the carrier' of x, the carrier of x)) is set
K480( the carrier of x, the ResultSort of x) is Element of K19( the carrier of x)
the carrier of x \ K480( the carrier of x, the ResultSort of x) is Element of K19( the carrier of x)
y is non empty V74() Circuit-like unsplit gate`1=arity ManySortedSign
InputVertices y is Element of K19( the carrier of y)
the carrier of y is non empty set
K19( the carrier of y) is set
the ResultSort of y is Relation-like Function-like V29( the carrier' of y, the carrier of y) Element of K19(K20( the carrier' of y, the carrier of y))
the carrier' of y is set
K20( the carrier' of y, the carrier of y) is Relation-like set
K19(K20( the carrier' of y, the carrier of y)) is set
K480( the carrier of y, the ResultSort of y) is Element of K19( the carrier of y)
the carrier of y \ K480( the carrier of y, the ResultSort of y) is Element of K19( the carrier of y)
x +* y is non empty V74() strict Circuit-like unsplit gate`1=arity ManySortedSign
InputVertices (x +* y) is Element of K19( the carrier of (x +* y))
the carrier of (x +* y) is non empty set
K19( the carrier of (x +* y)) is set
the ResultSort of (x +* y) is Relation-like Function-like V29( the carrier' of (x +* y), the carrier of (x +* y)) Element of K19(K20( the carrier' of (x +* y), the carrier of (x +* y)))
the carrier' of (x +* y) is set
K20( the carrier' of (x +* y), the carrier of (x +* y)) is Relation-like set
K19(K20( the carrier' of (x +* y), the carrier of (x +* y))) is set
K480( the carrier of (x +* y), the ResultSort of (x +* y)) is Element of K19( the carrier of (x +* y))
the carrier of (x +* y) \ K480( the carrier of (x +* y), the ResultSort of (x +* y)) is Element of K19( the carrier of (x +* y))
2 -tuples_on BOOLEAN is non empty functional FinSequence-membered FinSequenceSet of BOOLEAN
K20((2 -tuples_on BOOLEAN),BOOLEAN) is Relation-like set
K19(K20((2 -tuples_on BOOLEAN),BOOLEAN)) is set
x is Relation-like Function-like V29(2 -tuples_on BOOLEAN, BOOLEAN ) boolean-valued Element of K19(K20((2 -tuples_on BOOLEAN),BOOLEAN))
c is boolean Element of BOOLEAN
S1 is boolean Element of BOOLEAN
<*c,S1*> is non empty Relation-like NAT -defined Function-like finite V46(2) FinSequence-like FinSubsequence-like countable set
y is Relation-like Function-like V29(2 -tuples_on BOOLEAN, BOOLEAN ) boolean-valued Element of K19(K20((2 -tuples_on BOOLEAN),BOOLEAN))
y . <*c,S1*> is boolean set
S2 is Relation-like NAT -defined BOOLEAN -valued Function-like finite V46(2) FinSequence-like FinSubsequence-like countable Element of 2 -tuples_on BOOLEAN
S2 . 1 is set
S2 . 2 is set
F1((S2 . 1),(S2 . 2)) is boolean Element of BOOLEAN
F1(c,(S2 . 2)) is boolean Element of BOOLEAN
F1(c,S1) is boolean Element of BOOLEAN
2 -tuples_on BOOLEAN is non empty functional FinSequence-membered FinSequenceSet of BOOLEAN
K20((2 -tuples_on BOOLEAN),BOOLEAN) is Relation-like set
K19(K20((2 -tuples_on BOOLEAN),BOOLEAN)) is set
x is Relation-like Function-like V29(2 -tuples_on BOOLEAN, BOOLEAN ) boolean-valued Element of K19(K20((2 -tuples_on BOOLEAN),BOOLEAN))
y is Relation-like Function-like V29(2 -tuples_on BOOLEAN, BOOLEAN ) boolean-valued Element of K19(K20((2 -tuples_on BOOLEAN),BOOLEAN))
c is Relation-like NAT -defined BOOLEAN -valued Function-like finite V46(2) FinSequence-like FinSubsequence-like countable Element of 2 -tuples_on BOOLEAN
S1 is boolean Element of BOOLEAN
S2 is boolean Element of BOOLEAN
<*S1,S2*> is non empty Relation-like NAT -defined Function-like finite V46(2) FinSequence-like FinSubsequence-like countable set
x . c is boolean Element of BOOLEAN
F1(S1,S2) is boolean Element of BOOLEAN
y . c is boolean Element of BOOLEAN
2 -tuples_on BOOLEAN is non empty functional FinSequence-membered FinSequenceSet of BOOLEAN
K20((2 -tuples_on BOOLEAN),BOOLEAN) is Relation-like set
K19(K20((2 -tuples_on BOOLEAN),BOOLEAN)) is set
x is Relation-like Function-like V29(2 -tuples_on BOOLEAN, BOOLEAN ) boolean-valued Element of K19(K20((2 -tuples_on BOOLEAN),BOOLEAN))
c is boolean Element of BOOLEAN
S1 is boolean Element of BOOLEAN
<*c,S1*> is non empty Relation-like NAT -defined Function-like finite V46(2) FinSequence-like FinSubsequence-like countable set
y is Relation-like Function-like V29(2 -tuples_on BOOLEAN, BOOLEAN ) boolean-valued Element of K19(K20((2 -tuples_on BOOLEAN),BOOLEAN))
y . <*c,S1*> is boolean set
S2 is Relation-like NAT -defined BOOLEAN -valued Function-like finite V46(2) FinSequence-like FinSubsequence-like countable Element of 2 -tuples_on BOOLEAN
S2 . 1 is set
S2 . 2 is set
F1((S2 . 1),(S2 . 2)) is boolean Element of BOOLEAN
F1(c,(S2 . 2)) is boolean Element of BOOLEAN
F1(c,S1) is boolean Element of BOOLEAN
y is Relation-like Function-like V29(2 -tuples_on BOOLEAN, BOOLEAN ) boolean-valued Element of K19(K20((2 -tuples_on BOOLEAN),BOOLEAN))
c is Relation-like Function-like V29(2 -tuples_on BOOLEAN, BOOLEAN ) boolean-valued Element of K19(K20((2 -tuples_on BOOLEAN),BOOLEAN))
S1 is Relation-like NAT -defined BOOLEAN -valued Function-like finite V46(2) FinSequence-like FinSubsequence-like countable Element of 2 -tuples_on BOOLEAN
S2 is boolean Element of BOOLEAN
A is boolean Element of BOOLEAN
<*S2,A*> is non empty Relation-like NAT -defined Function-like finite V46(2) FinSequence-like FinSubsequence-like countable set
y . S1 is boolean Element of BOOLEAN
F1(S2,A) is boolean Element of BOOLEAN
c . S1 is boolean Element of BOOLEAN
3 -tuples_on BOOLEAN is non empty functional FinSequence-membered FinSequenceSet of BOOLEAN
K20((3 -tuples_on BOOLEAN),BOOLEAN) is Relation-like set
K19(K20((3 -tuples_on BOOLEAN),BOOLEAN)) is set
x is Relation-like Function-like V29(3 -tuples_on BOOLEAN, BOOLEAN ) boolean-valued Element of K19(K20((3 -tuples_on BOOLEAN),BOOLEAN))
c is boolean Element of BOOLEAN
S1 is boolean Element of BOOLEAN
S2 is boolean Element of BOOLEAN
<*c,S1,S2*> is non empty Relation-like NAT -defined Function-like finite V46(3) FinSequence-like FinSubsequence-like countable set
y is Relation-like Function-like V29(3 -tuples_on BOOLEAN, BOOLEAN ) boolean-valued Element of K19(K20((3 -tuples_on BOOLEAN),BOOLEAN))
y . <*c,S1,S2*> is boolean set
A is Relation-like NAT -defined BOOLEAN -valued Function-like finite V46(3) FinSequence-like FinSubsequence-like countable Element of 3 -tuples_on BOOLEAN
A . 1 is set
A . 2 is set
A . 3 is set
F1((A . 1),(A . 2),(A . 3)) is boolean Element of BOOLEAN
F1(c,(A . 2),(A . 3)) is boolean Element of BOOLEAN
F1(c,S1,(A . 3)) is boolean Element of BOOLEAN
F1(c,S1,S2) is boolean Element of BOOLEAN
3 -tuples_on BOOLEAN is non empty functional FinSequence-membered FinSequenceSet of BOOLEAN
K20((3 -tuples_on BOOLEAN),BOOLEAN) is Relation-like set
K19(K20((3 -tuples_on BOOLEAN),BOOLEAN)) is set
x is Relation-like Function-like V29(3 -tuples_on BOOLEAN, BOOLEAN ) boolean-valued Element of K19(K20((3 -tuples_on BOOLEAN),BOOLEAN))
y is Relation-like Function-like V29(3 -tuples_on BOOLEAN, BOOLEAN ) boolean-valued Element of K19(K20((3 -tuples_on BOOLEAN),BOOLEAN))
c is Relation-like NAT -defined BOOLEAN -valued Function-like finite V46(3) FinSequence-like FinSubsequence-like countable Element of 3 -tuples_on BOOLEAN
S1 is boolean Element of BOOLEAN
S2 is boolean Element of BOOLEAN
A is boolean Element of BOOLEAN
<*S1,S2,A*> is non empty Relation-like NAT -defined Function-like finite V46(3) FinSequence-like FinSubsequence-like countable set
x . c is boolean Element of BOOLEAN
F1(S1,S2,A) is boolean Element of BOOLEAN
y . c is boolean Element of BOOLEAN
3 -tuples_on BOOLEAN is non empty functional FinSequence-membered FinSequenceSet of BOOLEAN
K20((3 -tuples_on BOOLEAN),BOOLEAN) is Relation-like set
K19(K20((3 -tuples_on BOOLEAN),BOOLEAN)) is set
x is Relation-like Function-like V29(3 -tuples_on BOOLEAN, BOOLEAN ) boolean-valued Element of K19(K20((3 -tuples_on BOOLEAN),BOOLEAN))
c is boolean Element of BOOLEAN
S1 is boolean Element of BOOLEAN
S2 is boolean Element of BOOLEAN
<*c,S1,S2*> is non empty Relation-like NAT -defined Function-like finite V46(3) FinSequence-like FinSubsequence-like countable set
y is Relation-like Function-like V29(3 -tuples_on BOOLEAN, BOOLEAN ) boolean-valued Element of K19(K20((3 -tuples_on BOOLEAN),BOOLEAN))
y . <*c,S1,S2*> is boolean set
A is Relation-like NAT -defined BOOLEAN -valued Function-like finite V46(3) FinSequence-like FinSubsequence-like countable Element of 3 -tuples_on BOOLEAN
A . 1 is set
A . 2 is set
A . 3 is set
F1((A . 1),(A . 2),(A . 3)) is boolean Element of BOOLEAN
F1(c,(A . 2),(A . 3)) is boolean Element of BOOLEAN
F1(c,S1,(A . 3)) is boolean Element of BOOLEAN
F1(c,S1,S2) is boolean Element of BOOLEAN
y is Relation-like Function-like V29(3 -tuples_on BOOLEAN, BOOLEAN ) boolean-valued Element of K19(K20((3 -tuples_on BOOLEAN),BOOLEAN))
c is Relation-like Function-like V29(3 -tuples_on BOOLEAN, BOOLEAN ) boolean-valued Element of K19(K20((3 -tuples_on BOOLEAN),BOOLEAN))
S1 is Relation-like NAT -defined BOOLEAN -valued Function-like finite V46(3) FinSequence-like FinSubsequence-like countable Element of 3 -tuples_on BOOLEAN
S2 is boolean Element of BOOLEAN
A is boolean Element of BOOLEAN
A1 is boolean Element of BOOLEAN
<*S2,A,A1*> is non empty Relation-like NAT -defined Function-like finite V46(3) FinSequence-like FinSubsequence-like countable set
y . S1 is boolean Element of BOOLEAN
F1(S2,A,A1) is boolean Element of BOOLEAN
c . S1 is boolean Element of BOOLEAN
2 -tuples_on BOOLEAN is non empty functional FinSequence-membered FinSequenceSet of BOOLEAN
K20((2 -tuples_on BOOLEAN),BOOLEAN) is Relation-like set
K19(K20((2 -tuples_on BOOLEAN),BOOLEAN)) is set
x is Relation-like Function-like V29(2 -tuples_on BOOLEAN, BOOLEAN ) boolean-valued Element of K19(K20((2 -tuples_on BOOLEAN),BOOLEAN))
y is Relation-like Function-like V29(2 -tuples_on BOOLEAN, BOOLEAN ) boolean-valued Element of K19(K20((2 -tuples_on BOOLEAN),BOOLEAN))
c is Relation-like Function-like V29(2 -tuples_on BOOLEAN, BOOLEAN ) boolean-valued Element of K19(K20((2 -tuples_on BOOLEAN),BOOLEAN))
x is Relation-like Function-like V29(2 -tuples_on BOOLEAN, BOOLEAN ) boolean-valued Element of K19(K20((2 -tuples_on BOOLEAN),BOOLEAN))
y is Relation-like Function-like V29(2 -tuples_on BOOLEAN, BOOLEAN ) boolean-valued Element of K19(K20((2 -tuples_on BOOLEAN),BOOLEAN))
c is Relation-like Function-like V29(2 -tuples_on BOOLEAN, BOOLEAN ) boolean-valued Element of K19(K20((2 -tuples_on BOOLEAN),BOOLEAN))
x is Relation-like Function-like V29(2 -tuples_on BOOLEAN, BOOLEAN ) boolean-valued Element of K19(K20((2 -tuples_on BOOLEAN),BOOLEAN))
y is Relation-like Function-like V29(2 -tuples_on BOOLEAN, BOOLEAN ) boolean-valued Element of K19(K20((2 -tuples_on BOOLEAN),BOOLEAN))
c is Relation-like Function-like V29(2 -tuples_on BOOLEAN, BOOLEAN ) boolean-valued Element of K19(K20((2 -tuples_on BOOLEAN),BOOLEAN))
() is Relation-like Function-like V29(2 -tuples_on BOOLEAN, BOOLEAN ) boolean-valued Element of K19(K20((2 -tuples_on BOOLEAN),BOOLEAN))
() is Relation-like Function-like V29(2 -tuples_on BOOLEAN, BOOLEAN ) boolean-valued Element of K19(K20((2 -tuples_on BOOLEAN),BOOLEAN))
() is Relation-like Function-like V29(2 -tuples_on BOOLEAN, BOOLEAN ) boolean-valued Element of K19(K20((2 -tuples_on BOOLEAN),BOOLEAN))
3 -tuples_on BOOLEAN is non empty functional FinSequence-membered FinSequenceSet of BOOLEAN
K20((3 -tuples_on BOOLEAN),BOOLEAN) is Relation-like set
K19(K20((3 -tuples_on BOOLEAN),BOOLEAN)) is set
x is Relation-like Function-like V29(3 -tuples_on BOOLEAN, BOOLEAN ) boolean-valued Element of K19(K20((3 -tuples_on BOOLEAN),BOOLEAN))
y is Relation-like Function-like V29(3 -tuples_on BOOLEAN, BOOLEAN ) boolean-valued Element of K19(K20((3 -tuples_on BOOLEAN),BOOLEAN))
c is Relation-like Function-like V29(3 -tuples_on BOOLEAN, BOOLEAN ) boolean-valued Element of K19(K20((3 -tuples_on BOOLEAN),BOOLEAN))
() is Relation-like Function-like V29(3 -tuples_on BOOLEAN, BOOLEAN ) boolean-valued Element of K19(K20((3 -tuples_on BOOLEAN),BOOLEAN))
x is non empty non void V74() Circuit-like ManySortedSign
the carrier of x is non empty set
the carrier' of x is non empty set
y is non-empty finitely-generated finite-yielding MSAlgebra over x
the Sorts of y is Relation-like non-empty the carrier of x -defined Function-like total set
product the Sorts of y is non empty functional with_common_domain product-like set
c is Relation-like the carrier of x -defined Function-like the Sorts of y -compatible total Element of product the Sorts of y
Following c is Relation-like the carrier of x -defined Function-like the Sorts of y -compatible total Element of product the Sorts of y
S1 is Element of the carrier' of x
the_result_sort_of S1 is Element of the carrier of x
(Following c) . (the_result_sort_of S1) is set
Den (S1,y) is Relation-like Function-like V29( Args (S1,y), Result (S1,y)) Element of K19(K20((Args (S1,y)),(Result (S1,y))))
Args (S1,y) is non empty Element of proj2 K260( the carrier of x, the Sorts of y)
K260( the carrier of x, the Sorts of y) is Relation-like non-empty the carrier of x * -defined Function-like total set
the carrier of x * is non empty functional FinSequence-membered FinSequenceSet of the carrier of x
proj2 K260( the carrier of x, the Sorts of y) is set
Result (S1,y) is non empty Element of proj2 the Sorts of y
proj2 the Sorts of y is set
K20((Args (S1,y)),(Result (S1,y))) is Relation-like set
K19(K20((Args (S1,y)),(Result (S1,y)))) is set
the_arity_of S1 is Relation-like NAT -defined the carrier of x -valued Function-like finite FinSequence-like FinSubsequence-like countable Element of the carrier of x *
(the_arity_of S1) * c is Relation-like NAT -defined Function-like finite countable set
(Den (S1,y)) . ((the_arity_of S1) * c) is set
the ResultSort of x is Relation-like Function-like V29( the carrier' of x, the carrier of x) Element of K19(K20( the carrier' of x, the carrier of x))
K20( the carrier' of x, the carrier of x) is Relation-like set
K19(K20( the carrier' of x, the carrier of x)) is set
proj1 the ResultSort of x is set
the ResultSort of x . S1 is Element of the carrier of x
proj2 the ResultSort of x is set
InnerVertices x is non empty Element of K19( the carrier of x)
K19( the carrier of x) is set
K480( the carrier of x, the ResultSort of x) is Element of K19( the carrier of x)
S1 depends_on_in c is Element of Args (S1,y)
action_at (the_result_sort_of S1) is Element of the carrier' of x
x is non empty non void V74() Circuit-like ManySortedSign
the carrier of x is non empty set
y is non-empty finitely-generated finite-yielding MSAlgebra over x
the Sorts of y is Relation-like non-empty the carrier of x -defined Function-like total set
product the Sorts of y is non empty functional with_common_domain product-like set
K20(NAT,(product the Sorts of y)) is V5() Relation-like non finite set
K19(K20(NAT,(product the Sorts of y))) is V5() non finite set
S1 is V1() V3() V7() V8() V9() V13() V14() non pair finite V44() countable set
c is Relation-like the carrier of x -defined Function-like the Sorts of y -compatible total Element of product the Sorts of y
A is Relation-like the carrier of x -defined Function-like the Sorts of y -compatible total Element of product the Sorts of y
A2 is Relation-like Function-like V29( NAT , product the Sorts of y) Element of K19(K20(NAT,(product the Sorts of y)))
A2 . S1 is Relation-like the carrier of x -defined Function-like the Sorts of y -compatible total Element of product the Sorts of y
A2 . 0 is Relation-like the carrier of x -defined Function-like the Sorts of y -compatible total Element of product the Sorts of y
A1 is Relation-like the carrier of x -defined Function-like the Sorts of y -compatible total Element of product the Sorts of y
s is Relation-like Function-like V29( NAT , product the Sorts of y) Element of K19(K20(NAT,(product the Sorts of y)))
s . S1 is Relation-like the carrier of x -defined Function-like the Sorts of y -compatible total Element of product the Sorts of y
s . 0 is Relation-like the carrier of x -defined Function-like the Sorts of y -compatible total Element of product the Sorts of y
s2 is Relation-like the carrier of x -defined Function-like the Sorts of y -compatible total Element of product the Sorts of y
t is Relation-like Function-like V29( NAT , product the Sorts of y) Element of K19(K20(NAT,(product the Sorts of y)))
t . S1 is Relation-like the carrier of x -defined Function-like the Sorts of y -compatible total Element of product the Sorts of y
t . 0 is Relation-like the carrier of x -defined Function-like the Sorts of y -compatible total Element of product the Sorts of y
x is non empty non void V74() Circuit-like ManySortedSign
the carrier of x is non empty set
y is non-empty finitely-generated finite-yielding MSAlgebra over x
the Sorts of y is Relation-like non-empty the carrier of x -defined Function-like total set
product the Sorts of y is non empty functional with_common_domain product-like set
c is Relation-like the carrier of x -defined Function-like the Sorts of y -compatible total Element of product the Sorts of y
(x,y,c,0) is Relation-like the carrier of x -defined Function-like the Sorts of y -compatible total Element of product the Sorts of y
K20(NAT,(product the Sorts of y)) is V5() Relation-like non finite set
K19(K20(NAT,(product the Sorts of y))) is V5() non finite set
S1 is Relation-like Function-like V29( NAT , product the Sorts of y) Element of K19(K20(NAT,(product the Sorts of y)))
S1 . 0 is Relation-like the carrier of x -defined Function-like the Sorts of y -compatible total Element of product the Sorts of y
x is non empty non void V74() Circuit-like ManySortedSign
the carrier of x is non empty set
y is non-empty finitely-generated finite-yielding MSAlgebra over x
the Sorts of y is Relation-like non-empty the carrier of x -defined Function-like total set
product the Sorts of y is non empty functional with_common_domain product-like set
c is Relation-like the carrier of x -defined Function-like the Sorts of y -compatible total Element of product the Sorts of y
S1 is V1() V3() V7() V8() V9() V13() V14() non pair finite V44() countable set
S1 + 1 is V1() V2() V3() non empty V7() V8() V9() V13() V14() non pair finite V44() countable Element of NAT
(x,y,c,(S1 + 1)) is Relation-like the carrier of x -defined Function-like the Sorts of y -compatible total Element of product the Sorts of y
(x,y,c,S1) is Relation-like the carrier of x -defined Function-like the Sorts of y -compatible total Element of product the Sorts of y
Following (x,y,c,S1) is Relation-like the carrier of x -defined Function-like the Sorts of y -compatible total Element of product the Sorts of y
K20(NAT,(product the Sorts of y)) is V5() Relation-like non finite set
K19(K20(NAT,(product the Sorts of y))) is V5() non finite set
S2 is Relation-like Function-like V29( NAT , product the Sorts of y) Element of K19(K20(NAT,(product the Sorts of y)))
S2 . S1 is Relation-like the carrier of x -defined Function-like the Sorts of y -compatible total Element of product the Sorts of y
S2 . 0 is Relation-like the carrier of x -defined Function-like the Sorts of y -compatible total Element of product the Sorts of y
S2 . (S1 + 1) is Relation-like the carrier of x -defined Function-like the Sorts of y -compatible total Element of product the Sorts of y
x is non empty non void V74() Circuit-like ManySortedSign
the carrier of x is non empty set
y is non-empty finitely-generated finite-yielding MSAlgebra over x
the Sorts of y is Relation-like non-empty the carrier of x -defined Function-like total set
product the Sorts of y is non empty functional with_common_domain product-like set
c is Relation-like the carrier of x -defined Function-like the Sorts of y -compatible total Element of product the Sorts of y
S1 is V1() V3() V7() V8() V9() V13() V14() non pair finite V44() countable set
(x,y,c,S1) is Relation-like the carrier of x -defined Function-like the Sorts of y -compatible total Element of product the Sorts of y
S2 is V1() V3() V7() V8() V9() V13() V14() non pair finite V44() countable set
S1 + S2 is V1() V3() V7() V8() V9() V13() V14() non pair finite V44() countable set
(x,y,c,(S1 + S2)) is Relation-like the carrier of x -defined Function-like the Sorts of y -compatible total Element of product the Sorts of y
(x,y,(x,y,c,S1),S2) is Relation-like the carrier of x -defined Function-like the Sorts of y -compatible total Element of product the Sorts of y
S2 + 1 is V1() V2() V3() non empty V7() V8() V9() V13() V14() non pair finite V44() countable Element of NAT
S1 + (S2 + 1) is V1() V2() V3() non empty V7() V8() V9() V13() V14() non pair finite V44() countable set
(x,y,c,(S1 + (S2 + 1))) is Relation-like the carrier of x -defined Function-like the Sorts of y -compatible total Element of product the Sorts of y
(x,y,(x,y,c,S1),(S2 + 1)) is Relation-like the carrier of x -defined Function-like the Sorts of y -compatible total Element of product the Sorts of y
S1 + (S2 + 1) is V1() V2() V3() non empty V7() V8() V9() V13() V14() non pair finite V44() countable Element of NAT
(x,y,c,(S1 + (S2 + 1))) is Relation-like the carrier of x -defined Function-like the Sorts of y -compatible total Element of product the Sorts of y
(S1 + S2) + 1 is V1() V2() V3() non empty V7() V8() V9() V13() V14() non pair finite V44() countable Element of NAT
(x,y,c,((S1 + S2) + 1)) is Relation-like the carrier of x -defined Function-like the Sorts of y -compatible total Element of product the Sorts of y
Following (x,y,c,(S1 + S2)) is Relation-like the carrier of x -defined Function-like the Sorts of y -compatible total Element of product the Sorts of y
S1 + 0 is V1() V3() V7() V8() V9() V13() V14() non pair finite V44() countable set
(x,y,c,(S1 + 0)) is Relation-like the carrier of x -defined Function-like the Sorts of y -compatible total Element of product the Sorts of y
(x,y,(x,y,c,S1),0) is Relation-like the carrier of x -defined Function-like the Sorts of y -compatible total Element of product the Sorts of y
x is non empty non void V74() Circuit-like ManySortedSign
the carrier of x is non empty set
y is non-empty finitely-generated finite-yielding MSAlgebra over x
the Sorts of y is Relation-like non-empty the carrier of x -defined Function-like total set
product the Sorts of y is non empty functional with_common_domain product-like set
c is Relation-like the carrier of x -defined Function-like the Sorts of y -compatible total Element of product the Sorts of y
(x,y,c,1) is Relation-like the carrier of x -defined Function-like the Sorts of y -compatible total Element of product the Sorts of y
Following c is Relation-like the carrier of x -defined Function-like the Sorts of y -compatible total Element of product the Sorts of y
0 + 1 is V1() V2() V3() non empty V7() V8() V9() V13() V14() non pair finite V44() countable Element of NAT
(x,y,c,0) is Relation-like the carrier of x -defined Function-like the Sorts of y -compatible total Element of product the Sorts of y
Following (x,y,c,0) is Relation-like the carrier of x -defined Function-like the Sorts of y -compatible total Element of product the Sorts of y
x is non empty non void V74() Circuit-like ManySortedSign
the carrier of x is non empty set
y is non-empty finitely-generated finite-yielding MSAlgebra over x
the Sorts of y is Relation-like non-empty the carrier of x -defined Function-like total set
product the Sorts of y is non empty functional with_common_domain product-like set
c is Relation-like the carrier of x -defined Function-like the Sorts of y -compatible total Element of product the Sorts of y
(x,y,c,2) is Relation-like the carrier of x -defined Function-like the Sorts of y -compatible total Element of product the Sorts of y
Following c is Relation-like the carrier of x -defined Function-like the Sorts of y -compatible total Element of product the Sorts of y
Following (Following c) is Relation-like the carrier of x -defined Function-like the Sorts of y -compatible total Element of product the Sorts of y
1 + 1 is V1() V2() V3() non empty V7() V8() V9() V13() V14() non pair finite V44() countable Element of NAT
0 + 1 is V1() V2() V3() non empty V7() V8() V9() V13() V14() non pair finite V44() countable Element of NAT
(x,y,c,(0 + 1)) is Relation-like the carrier of x -defined Function-like the Sorts of y -compatible total Element of product the Sorts of y
Following (x,y,c,(0 + 1)) is Relation-like the carrier of x -defined Function-like the Sorts of y -compatible total Element of product the Sorts of y
x is non empty non void V74() Circuit-like ManySortedSign
the carrier of x is non empty set
y is non-empty finitely-generated finite-yielding MSAlgebra over x
the Sorts of y is Relation-like non-empty the carrier of x -defined Function-like total set
product the Sorts of y is non empty functional with_common_domain product-like set
c is Relation-like the carrier of x -defined Function-like the Sorts of y -compatible total Element of product the Sorts of y
Following c is Relation-like the carrier of x -defined Function-like the Sorts of y -compatible total Element of product the Sorts of y
S1 is V1() V3() V7() V8() V9() V13() V14() non pair finite V44() countable set
S1 + 1 is V1() V2() V3() non empty V7() V8() V9() V13() V14() non pair finite V44() countable Element of NAT
(x,y,c,(S1 + 1)) is Relation-like the carrier of x -defined Function-like the Sorts of y -compatible total Element of product the Sorts of y
(x,y,(Following c),S1) is Relation-like the carrier of x -defined Function-like the Sorts of y -compatible total Element of product the Sorts of y
(x,y,c,1) is Relation-like the carrier of x -defined Function-like the Sorts of y -compatible total Element of product the Sorts of y
(x,y,(x,y,c,1),S1) is Relation-like the carrier of x -defined Function-like the Sorts of y -compatible total Element of product the Sorts of y
x is non empty non void V74() Circuit-like ManySortedSign
the carrier of x is non empty set
y is non-empty finitely-generated finite-yielding MSAlgebra over x
the Sorts of y is Relation-like non-empty the carrier of x -defined Function-like total set
product the Sorts of y is non empty functional with_common_domain product-like set
x is non empty non void V74() Circuit-like ManySortedSign
the carrier of x is non empty set
y is non-empty finitely-generated finite-yielding MSAlgebra over x
the Sorts of y is Relation-like non-empty the carrier of x -defined Function-like total set
product the Sorts of y is non empty functional with_common_domain product-like set
c is Relation-like the carrier of x -defined Function-like the Sorts of y -compatible total Element of product the Sorts of y
S1 is set
c . S1 is set
S2 is V1() V3() V7() V8() V9() V13() V14() non pair finite V44() countable set
(x,y,c,S2) is Relation-like the carrier of x -defined Function-like the Sorts of y -compatible total Element of product the Sorts of y
A is V1() V3() V7() V8() V9() V13() V14() non pair finite V44() countable set
(x,y,(x,y,c,S2),A) is Relation-like the carrier of x -defined Function-like the Sorts of y -compatible total Element of product the Sorts of y
(x,y,(x,y,c,S2),A) . S1 is set
(x,y,c,S2) . S1 is set
S2 + A is V1() V3() V7() V8() V9() V13() V14() non pair finite V44() countable set
(x,y,c,(S2 + A)) is Relation-like the carrier of x -defined Function-like the Sorts of y -compatible total Element of product the Sorts of y
(x,y,c,(S2 + A)) . S1 is set
x is non empty non void V74() Circuit-like ManySortedSign
the carrier of x is non empty set
InputVertices x is Element of K19( the carrier of x)
K19( the carrier of x) is set
the ResultSort of x is Relation-like Function-like V29( the carrier' of x, the carrier of x) Element of K19(K20( the carrier' of x, the carrier of x))
the carrier' of x is non empty set
K20( the carrier' of x, the carrier of x) is Relation-like set
K19(K20( the carrier' of x, the carrier of x)) is set
K480( the carrier of x, the ResultSort of x) is Element of K19( the carrier of x)
the carrier of x \ K480( the carrier of x, the ResultSort of x) is Element of K19( the carrier of x)
y is non-empty finitely-generated finite-yielding MSAlgebra over x
the Sorts of y is Relation-like non-empty the carrier of x -defined Function-like total set
product the Sorts of y is non empty functional with_common_domain product-like set
c is Relation-like the carrier of x -defined Function-like the Sorts of y -compatible total Element of product the Sorts of y
S1 is set
c . S1 is set
S2 is V1() V3() V7() V8() V9() V13() V14() non pair finite V44() countable set
(x,y,c,S2) is Relation-like the carrier of x -defined Function-like the Sorts of y -compatible total Element of product the Sorts of y
(x,y,c,S2) . S1 is set
S2 + 1 is V1() V2() V3() non empty V7() V8() V9() V13() V14() non pair finite V44() countable Element of NAT
(x,y,c,(S2 + 1)) is Relation-like the carrier of x -defined Function-like the Sorts of y -compatible total Element of product the Sorts of y
(x,y,c,(S2 + 1)) . S1 is set
Following (x,y,c,S2) is Relation-like the carrier of x -defined Function-like the Sorts of y -compatible total Element of product the Sorts of y
(Following (x,y,c,S2)) . S1 is set
(x,y,c,0) is Relation-like the carrier of x -defined Function-like the Sorts of y -compatible total Element of product the Sorts of y
(x,y,c,0) . S1 is set
x is non empty non void V74() Circuit-like ManySortedSign
the carrier of x is non empty set
the carrier' of x is non empty set
y is non-empty finitely-generated finite-yielding MSAlgebra over x
the Sorts of y is Relation-like non-empty the carrier of x -defined Function-like total set
product the Sorts of y is non empty functional with_common_domain product-like set
c is Relation-like the carrier of x -defined Function-like the Sorts of y -compatible total Element of product the Sorts of y
Following c is Relation-like the carrier of x -defined Function-like the Sorts of y -compatible total Element of product the Sorts of y
S1 is Element of the carrier' of x
the_arity_of S1 is Relation-like NAT -defined the carrier of x -valued Function-like finite FinSequence-like FinSubsequence-like countable Element of the carrier of x *
the carrier of x * is non empty functional FinSequence-membered FinSequenceSet of the carrier of x
proj2 (the_arity_of S1) is finite countable set
the_result_sort_of S1 is Element of the carrier of x
A is V1() V3() V7() V8() V9() V13() V14() non pair finite V44() countable set
(x,y,(Following c),A) is Relation-like the carrier of x -defined Function-like the Sorts of y -compatible total Element of product the Sorts of y
(x,y,(Following c),A) . (the_result_sort_of S1) is set
(Following c) . (the_result_sort_of S1) is set
A1 is set
dom (the_arity_of S1) is finite countable Element of K19(NAT)
(the_arity_of S1) . A1 is set
(x,y,c,A) is Relation-like the carrier of x -defined Function-like the Sorts of y -compatible total Element of product the Sorts of y
(the_arity_of S1) * (x,y,c,A) is Relation-like NAT -defined Function-like finite countable set
((the_arity_of S1) * (x,y,c,A)) . A1 is set
(x,y,c,A) . ((the_arity_of S1) . A1) is set
(the_arity_of S1) * c is Relation-like NAT -defined Function-like finite countable set
((the_arity_of S1) * c) . A1 is set
c . ((the_arity_of S1) . A1) is set
proj1 (x,y,c,A) is set
proj1 ((the_arity_of S1) * (x,y,c,A)) is finite countable set
proj1 c is set
proj1 ((the_arity_of S1) * c) is finite countable set
A + 1 is V1() V2() V3() non empty V7() V8() V9() V13() V14() non pair finite V44() countable Element of NAT
(x,y,c,(A + 1)) is Relation-like the carrier of x -defined Function-like the Sorts of y -compatible total Element of product the Sorts of y
(x,y,c,(A + 1)) . (the_result_sort_of S1) is set
Following (x,y,c,A) is Relation-like the carrier of x -defined Function-like the Sorts of y -compatible total Element of product the Sorts of y
(Following (x,y,c,A)) . (the_result_sort_of S1) is set
Den (S1,y) is Relation-like Function-like V29( Args (S1,y), Result (S1,y)) Element of K19(K20((Args (S1,y)),(Result (S1,y))))
Args (S1,y) is non empty Element of proj2 K260( the carrier of x, the Sorts of y)
K260( the carrier of x, the Sorts of y) is Relation-like non-empty the carrier of x * -defined Function-like total set
proj2 K260( the carrier of x, the Sorts of y) is set
Result (S1,y) is non empty Element of proj2 the Sorts of y
proj2 the Sorts of y is set
K20((Args (S1,y)),(Result (S1,y))) is Relation-like set
K19(K20((Args (S1,y)),(Result (S1,y)))) is set
(Den (S1,y)) . ((the_arity_of S1) * (x,y,c,A)) is set
x is non empty V74() ManySortedSign
the carrier of x is non empty set
y is non empty V74() ManySortedSign
x +* y is non empty V74() strict ManySortedSign
the carrier of (x +* y) is non empty set
y +* x is non empty V74() strict ManySortedSign
the carrier of (y +* x) is non empty set
c is Element of the carrier of x
the carrier of y is non empty set
the carrier of x \/ the carrier of y is non empty set
the carrier of y \/ the carrier of x is non empty set
x is non empty V74() Circuit-like unsplit gate`1=arity ManySortedSign
InnerVertices x is Element of K19( the carrier of x)
the carrier of x is non empty set
K19( the carrier of x) is set
the ResultSort of x is Relation-like Function-like V29( the carrier' of x, the carrier of x) Element of K19(K20( the carrier' of x, the carrier of x))
the carrier' of x is set
K20( the carrier' of x, the carrier of x) is Relation-like set
K19(K20( the carrier' of x, the carrier of x)) is set
K480( the carrier of x, the ResultSort of x) is Element of K19( the carrier of x)
y is non empty V74() Circuit-like unsplit gate`1=arity ManySortedSign
x +* y is non empty V74() strict Circuit-like unsplit gate`1=arity ManySortedSign
InnerVertices (x +* y) is Element of K19( the carrier of (x +* y))
the carrier of (x +* y) is non empty set
K19( the carrier of (x +* y)) is set
the ResultSort of (x +* y) is Relation-like Function-like V29( the carrier' of (x +* y), the carrier of (x +* y)) Element of K19(K20( the carrier' of (x +* y), the carrier of (x +* y)))
the carrier' of (x +* y) is set
K20( the carrier' of (x +* y), the carrier of (x +* y)) is Relation-like set
K19(K20( the carrier' of (x +* y), the carrier of (x +* y))) is set
K480( the carrier of (x +* y), the ResultSort of (x +* y)) is Element of K19( the carrier of (x +* y))
y +* x is non empty V74() strict Circuit-like unsplit gate`1=arity ManySortedSign
InnerVertices (y +* x) is Element of K19( the carrier of (y +* x))
the carrier of (y +* x) is non empty set
K19( the carrier of (y +* x)) is set
the ResultSort of (y +* x) is Relation-like Function-like V29( the carrier' of (y +* x), the carrier of (y +* x)) Element of K19(K20( the carrier' of (y +* x), the carrier of (y +* x)))
the carrier' of (y +* x) is set
K20( the carrier' of (y +* x), the carrier of (y +* x)) is Relation-like set
K19(K20( the carrier' of (y +* x), the carrier of (y +* x))) is set
K480( the carrier of (y +* x), the ResultSort of (y +* x)) is Element of K19( the carrier of (y +* x))
InnerVertices y is Element of K19( the carrier of y)
the carrier of y is non empty set
K19( the carrier of y) is set
the ResultSort of y is Relation-like Function-like V29( the carrier' of y, the carrier of y) Element of K19(K20( the carrier' of y, the carrier of y))
the carrier' of y is set
K20( the carrier' of y, the carrier of y) is Relation-like set
K19(K20( the carrier' of y, the carrier of y)) is set
K480( the carrier of y, the ResultSort of y) is Element of K19( the carrier of y)
(InnerVertices x) \/ (InnerVertices y) is set
(InnerVertices y) \/ (InnerVertices x) is set
c is set
y is non empty V74() ManySortedSign
InnerVertices y is Element of K19( the carrier of y)
the carrier of y is non empty set
K19( the carrier of y) is set
the ResultSort of y is Relation-like Function-like V29( the carrier' of y, the carrier of y) Element of K19(K20( the carrier' of y, the carrier of y))
the carrier' of y is set
K20( the carrier' of y, the carrier of y) is Relation-like set
K19(K20( the carrier' of y, the carrier of y)) is set
K480( the carrier of y, the ResultSort of y) is Element of K19( the carrier of y)
x is non empty V74() ManySortedSign
x +* y is non empty V74() strict ManySortedSign
InnerVertices (x +* y) is Element of K19( the carrier of (x +* y))
the carrier of (x +* y) is non empty set
K19( the carrier of (x +* y)) is set
the ResultSort of (x +* y) is Relation-like Function-like V29( the carrier' of (x +* y), the carrier of (x +* y)) Element of K19(K20( the carrier' of (x +* y), the carrier of (x +* y)))
the carrier' of (x +* y) is set
K20( the carrier' of (x +* y), the carrier of (x +* y)) is Relation-like set
K19(K20( the carrier' of (x +* y), the carrier of (x +* y))) is set
K480( the carrier of (x +* y), the ResultSort of (x +* y)) is Element of K19( the carrier of (x +* y))
the ResultSort of x is Relation-like Function-like V29( the carrier' of x, the carrier of x) Element of K19(K20( the carrier' of x, the carrier of x))
the carrier' of x is set
the carrier of x is non empty set
K20( the carrier' of x, the carrier of x) is Relation-like set
K19(K20( the carrier' of x, the carrier of x)) is set
the ResultSort of x +* the ResultSort of y is Relation-like Function-like set
proj2 ( the ResultSort of x +* the ResultSort of y) is set
S2 is set
x is non empty V74() Circuit-like unsplit gate`1=arity ManySortedSign
y is non empty V74() Circuit-like unsplit gate`1=arity ManySortedSign
x +* y is non empty V74() strict Circuit-like unsplit gate`1=arity ManySortedSign
y +* x is non empty V74() strict Circuit-like unsplit gate`1=arity ManySortedSign
x is non empty non void V74() Circuit-like unsplit gate`1=arity gate`2isBoolean gate`2=den ManySortedSign
y is non empty non void V74() Circuit-like unsplit gate`1=arity gate`2isBoolean gate`2=den ManySortedSign
c is non-empty finitely-generated finite-yielding gate`2=den Boolean MSAlgebra over x
S1 is non-empty finitely-generated finite-yielding gate`2=den Boolean MSAlgebra over y
c +* S1 is strict non-empty finitely-generated finite-yielding gate`2=den Boolean MSAlgebra over x +* y
x +* y is non empty non void V74() strict Circuit-like unsplit gate`1=arity gate`2isBoolean gate`2=den ManySortedSign
S1 +* c is strict non-empty finitely-generated finite-yielding gate`2=den Boolean MSAlgebra over y +* x
y +* x is non empty non void V74() strict Circuit-like unsplit gate`1=arity gate`2isBoolean gate`2=den ManySortedSign
x is non empty non void V74() Circuit-like unsplit gate`1=arity gate`2isBoolean gate`2=den ManySortedSign
y is non empty non void V74() Circuit-like unsplit gate`1=arity gate`2isBoolean gate`2=den ManySortedSign
c is non empty non void V74() Circuit-like unsplit gate`1=arity gate`2isBoolean gate`2=den ManySortedSign
x +* y is non empty non void V74() strict Circuit-like unsplit gate`1=arity gate`2isBoolean gate`2=den ManySortedSign
y +* c is non empty non void V74() strict Circuit-like unsplit gate`1=arity gate`2isBoolean gate`2=den ManySortedSign
S1 is non-empty finitely-generated finite-yielding Boolean MSAlgebra over x
S2 is non-empty finitely-generated finite-yielding Boolean MSAlgebra over y
S1 +* S2 is strict non-empty MSAlgebra over x +* y
A is non-empty finitely-generated finite-yielding Boolean MSAlgebra over c
(S1 +* S2) +* A is strict non-empty MSAlgebra over (x +* y) +* c
(x +* y) +* c is non empty non void V74() strict Circuit-like unsplit gate`1=arity gate`2isBoolean gate`2=den ManySortedSign
S2 +* A is strict non-empty MSAlgebra over y +* c
S1 +* (S2 +* A) is strict non-empty MSAlgebra over x +* (y +* c)
x +* (y +* c) is non empty non void V74() strict Circuit-like unsplit gate`1=arity gate`2isBoolean gate`2=den ManySortedSign
the Sorts of A is Relation-like non-empty the carrier of c -defined Function-like total set
the carrier of c is non empty set
the Sorts of S1 is Relation-like non-empty the carrier of x -defined Function-like total set
the carrier of x is non empty set
the Sorts of S2 is Relation-like non-empty the carrier of y -defined Function-like total set
the carrier of y is non empty set
x is non empty non void V74() Circuit-like unsplit gate`1=arity gate`2isBoolean gate`2=den ManySortedSign
y is non empty non void V74() Circuit-like unsplit gate`1=arity gate`2isBoolean gate`2=den ManySortedSign
x +* y is non empty non void V74() strict Circuit-like unsplit gate`1=arity gate`2isBoolean gate`2=den ManySortedSign
the carrier of (x +* y) is non empty set
the carrier of x is non empty set
the carrier of y is non empty set
c is non-empty finitely-generated finite-yielding gate`2=den Boolean MSAlgebra over x
the Sorts of c is Relation-like non-empty the carrier of x -defined Function-like total set
product the Sorts of c is non empty functional with_common_domain product-like set
S1 is non-empty finitely-generated finite-yielding gate`2=den Boolean MSAlgebra over y
c +* S1 is strict non-empty finitely-generated finite-yielding gate`2=den Boolean MSAlgebra over x +* y
the Sorts of (c +* S1) is Relation-like non-empty the carrier of (x +* y) -defined Function-like total set
product the Sorts of (c +* S1) is non empty functional with_common_domain product-like set
the Sorts of S1 is Relation-like non-empty the carrier of y -defined Function-like total set
product the Sorts of S1 is non empty functional with_common_domain product-like set
S2 is Relation-like the carrier of (x +* y) -defined Function-like the Sorts of (c +* S1) -compatible total Element of product the Sorts of (c +* S1)
S2 | the carrier of x is Relation-like the carrier of x -defined the carrier of (x +* y) -defined Function-like the Sorts of (c +* S1) -compatible Element of sproduct the Sorts of (c +* S1)
sproduct the Sorts of (c +* S1) is non empty functional set
S2 | the carrier of y is Relation-like the carrier of y -defined the carrier of (x +* y) -defined Function-like the Sorts of (c +* S1) -compatible Element of sproduct the Sorts of (c +* S1)
x is non empty V74() Circuit-like unsplit gate`1=arity ManySortedSign
y is non empty V74() Circuit-like unsplit gate`1=arity ManySortedSign
x +* y is non empty V74() strict Circuit-like unsplit gate`1=arity ManySortedSign
InnerVertices (x +* y) is Element of K19( the carrier of (x +* y))
the carrier of (x +* y) is non empty set
K19( the carrier of (x +* y)) is set
the ResultSort of (x +* y) is Relation-like Function-like V29( the carrier' of (x +* y), the carrier of (x +* y)) Element of K19(K20( the carrier' of (x +* y), the carrier of (x +* y)))
the carrier' of (x +* y) is set
K20( the carrier' of (x +* y), the carrier of (x +* y)) is Relation-like set
K19(K20( the carrier' of (x +* y), the carrier of (x +* y))) is set
K480( the carrier of (x +* y), the ResultSort of (x +* y)) is Element of K19( the carrier of (x +* y))
InnerVertices x is Element of K19( the carrier of x)
the carrier of x is non empty set
K19( the carrier of x) is set
the ResultSort of x is Relation-like Function-like V29( the carrier' of x, the carrier of x) Element of K19(K20( the carrier' of x, the carrier of x))
the carrier' of x is set
K20( the carrier' of x, the carrier of x) is Relation-like set
K19(K20( the carrier' of x, the carrier of x)) is set
K480( the carrier of x, the ResultSort of x) is Element of K19( the carrier of x)
InnerVertices y is Element of K19( the carrier of y)
the carrier of y is non empty set
K19( the carrier of y) is set
the ResultSort of y is Relation-like Function-like V29( the carrier' of y, the carrier of y) Element of K19(K20( the carrier' of y, the carrier of y))
the carrier' of y is set
K20( the carrier' of y, the carrier of y) is Relation-like set
K19(K20( the carrier' of y, the carrier of y)) is set
K480( the carrier of y, the ResultSort of y) is Element of K19( the carrier of y)
(InnerVertices x) \/ (InnerVertices y) is set
y is non empty non void V74() Circuit-like unsplit gate`1=arity gate`2isBoolean gate`2=den ManySortedSign
InnerVertices y is non empty Element of K19( the carrier of y)
the carrier of y is non empty set
K19( the carrier of y) is set
the ResultSort of y is Relation-like Function-like V29( the carrier' of y, the carrier of y) Element of K19(K20( the carrier' of y, the carrier of y))
the carrier' of y is non empty set
K20( the carrier' of y, the carrier of y) is Relation-like set
K19(K20( the carrier' of y, the carrier of y)) is set
K480( the carrier of y, the ResultSort of y) is Element of K19( the carrier of y)
x is non empty non void V74() Circuit-like unsplit gate`1=arity gate`2isBoolean gate`2=den ManySortedSign
InputVertices x is Element of K19( the carrier of x)
the carrier of x is non empty set
K19( the carrier of x) is set
the ResultSort of x is Relation-like Function-like V29( the carrier' of x, the carrier of x) Element of K19(K20( the carrier' of x, the carrier of x))
the carrier' of x is non empty set
K20( the carrier' of x, the carrier of x) is Relation-like set
K19(K20( the carrier' of x, the carrier of x)) is set
K480( the carrier of x, the ResultSort of x) is Element of K19( the carrier of x)
the carrier of x \ K480( the carrier of x, the ResultSort of x) is Element of K19( the carrier of x)
x +* y is non empty non void V74() strict Circuit-like unsplit gate`1=arity gate`2isBoolean gate`2=den ManySortedSign
the carrier of (x +* y) is non empty set
c is non-empty finitely-generated finite-yielding gate`2=den Boolean MSAlgebra over x
the Sorts of c is Relation-like non-empty the carrier of x -defined Function-like total set
product the Sorts of c is non empty functional with_common_domain product-like set
S1 is non-empty finitely-generated finite-yielding gate`2=den Boolean MSAlgebra over y
c +* S1 is strict non-empty finitely-generated finite-yielding gate`2=den Boolean MSAlgebra over x +* y
the Sorts of (c +* S1) is Relation-like non-empty the carrier of (x +* y) -defined Function-like total set
product the Sorts of (c +* S1) is non empty functional with_common_domain product-like set
S2 is Relation-like the carrier of (x +* y) -defined Function-like the Sorts of (c +* S1) -compatible total Element of product the Sorts of (c +* S1)
S2 | the carrier of x is Relation-like the carrier of x -defined the carrier of (x +* y) -defined Function-like the Sorts of (c +* S1) -compatible Element of sproduct the Sorts of (c +* S1)
sproduct the Sorts of (c +* S1) is non empty functional set
Following S2 is Relation-like the carrier of (x +* y) -defined Function-like the Sorts of (c +* S1) -compatible total Element of product the Sorts of (c +* S1)
(Following S2) | the carrier of x is Relation-like the carrier of x -defined the carrier of (x +* y) -defined Function-like the Sorts of (c +* S1) -compatible Element of sproduct the Sorts of (c +* S1)
A is Relation-like the carrier of x -defined Function-like the Sorts of c -compatible total Element of product the Sorts of c
Following A is Relation-like the carrier of x -defined Function-like the Sorts of c -compatible total Element of product the Sorts of c
the Sorts of S1 is Relation-like non-empty the carrier of y -defined Function-like total set
product the Sorts of S1 is non empty functional with_common_domain product-like set
S2 | the carrier of y is Relation-like the carrier of y -defined the carrier of (x +* y) -defined Function-like the Sorts of (c +* S1) -compatible Element of sproduct the Sorts of (c +* S1)
proj1 (Following A) is set
A1 is Relation-like the carrier of y -defined Function-like the Sorts of S1 -compatible total Element of product the Sorts of S1
Following A1 is Relation-like the carrier of y -defined Function-like the Sorts of S1 -compatible total Element of product the Sorts of S1
(Following A1) +* (Following A) is Relation-like the carrier of y \/ the carrier of x -defined Function-like total set
the carrier of y \/ the carrier of x is non empty set
x is non empty non void V74() Circuit-like unsplit gate`1=arity gate`2isBoolean gate`2=den ManySortedSign
InnerVertices x is non empty Element of K19( the carrier of x)
the carrier of x is non empty set
K19( the carrier of x) is set
the ResultSort of x is Relation-like Function-like V29( the carrier' of x, the carrier of x) Element of K19(K20( the carrier' of x, the carrier of x))
the carrier' of x is non empty set
K20( the carrier' of x, the carrier of x) is Relation-like set
K19(K20( the carrier' of x, the carrier of x)) is set
K480( the carrier of x, the ResultSort of x) is Element of K19( the carrier of x)
y is non empty non void V74() Circuit-like unsplit gate`1=arity gate`2isBoolean gate`2=den ManySortedSign
InputVertices y is Element of K19( the carrier of y)
the carrier of y is non empty set
K19( the carrier of y) is set
the ResultSort of y is Relation-like Function-like V29( the carrier' of y, the carrier of y) Element of K19(K20( the carrier' of y, the carrier of y))
the carrier' of y is non empty set
K20( the carrier' of y, the carrier of y) is Relation-like set
K19(K20( the carrier' of y, the carrier of y)) is set
K480( the carrier of y, the ResultSort of y) is Element of K19( the carrier of y)
the carrier of y \ K480( the carrier of y, the ResultSort of y) is Element of K19( the carrier of y)
x +* y is non empty non void V74() strict Circuit-like unsplit gate`1=arity gate`2isBoolean gate`2=den ManySortedSign
the carrier of (x +* y) is non empty set
c is non-empty finitely-generated finite-yielding gate`2=den Boolean MSAlgebra over x
S1 is non-empty finitely-generated finite-yielding gate`2=den Boolean MSAlgebra over y
c +* S1 is strict non-empty finitely-generated finite-yielding gate`2=den Boolean MSAlgebra over x +* y
the Sorts of (c +* S1) is Relation-like non-empty the carrier of (x +* y) -defined Function-like total set
product the Sorts of (c +* S1) is non empty functional with_common_domain product-like set
the Sorts of S1 is Relation-like non-empty the carrier of y -defined Function-like total set
product the Sorts of S1 is non empty functional with_common_domain product-like set
S2 is Relation-like the carrier of (x +* y) -defined Function-like the Sorts of (c +* S1) -compatible total Element of product the Sorts of (c +* S1)
S2 | the carrier of y is Relation-like the carrier of y -defined the carrier of (x +* y) -defined Function-like the Sorts of (c +* S1) -compatible Element of sproduct the Sorts of (c +* S1)
sproduct the Sorts of (c +* S1) is non empty functional set
Following S2 is Relation-like the carrier of (x +* y) -defined Function-like the Sorts of (c +* S1) -compatible total Element of product the Sorts of (c +* S1)
(Following S2) | the carrier of y is Relation-like the carrier of y -defined the carrier of (x +* y) -defined Function-like the Sorts of (c +* S1) -compatible Element of sproduct the Sorts of (c +* S1)
A is Relation-like the carrier of y -defined Function-like the Sorts of S1 -compatible total Element of product the Sorts of S1
Following A is Relation-like the carrier of y -defined Function-like the Sorts of S1 -compatible total Element of product the Sorts of S1
the Sorts of c is Relation-like non-empty the carrier of x -defined Function-like total set
product the Sorts of c is non empty functional with_common_domain product-like set
S2 | the carrier of x is Relation-like the carrier of x -defined the carrier of (x +* y) -defined Function-like the Sorts of (c +* S1) -compatible Element of sproduct the Sorts of (c +* S1)
proj1 (Following A) is set
A1 is Relation-like the carrier of x -defined Function-like the Sorts of c -compatible total Element of product the Sorts of c
Following A1 is Relation-like the carrier of x -defined Function-like the Sorts of c -compatible total Element of product the Sorts of c
(Following A1) +* (Following A) is Relation-like the carrier of x \/ the carrier of y -defined Function-like total set
the carrier of x \/ the carrier of y is non empty set
y is non empty non void V74() Circuit-like unsplit gate`1=arity gate`2isBoolean gate`2=den ManySortedSign
InnerVertices y is non empty Element of K19( the carrier of y)
the carrier of y is non empty set
K19( the carrier of y) is set
the ResultSort of y is Relation-like Function-like V29( the carrier' of y, the carrier of y) Element of K19(K20( the carrier' of y, the carrier of y))
the carrier' of y is non empty set
K20( the carrier' of y, the carrier of y) is Relation-like set
K19(K20( the carrier' of y, the carrier of y)) is set
K480( the carrier of y, the ResultSort of y) is Element of K19( the carrier of y)
x is non empty non void V74() Circuit-like unsplit gate`1=arity gate`2isBoolean gate`2=den ManySortedSign
InputVertices x is Element of K19( the carrier of x)
the carrier of x is non empty set
K19( the carrier of x) is set
the ResultSort of x is Relation-like Function-like V29( the carrier' of x, the carrier of x) Element of K19(K20( the carrier' of x, the carrier of x))
the carrier' of x is non empty set
K20( the carrier' of x, the carrier of x) is