:: FACIRC_1 semantic presentation

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

{ b

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

F

F

F

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

F

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

F

F

F

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

F

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

F

F

F

F

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

F

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

F

F

F

F

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

F

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