:: CIRCCMB2 semantic presentation

REAL is set

NAT is non empty V21() V22() V23() non finite V79() V80() M2(K19(REAL))

K19(REAL) is set

NAT is non empty V21() V22() V23() non finite V79() V80() set

K19(NAT) is set

K19(NAT) is set

{} is set

1 is non empty non pair V21() V22() V23() V27() V28() V121() ext-real non negative M3( REAL , NAT )

{{},1} is set

K236() is set

K19(K236()) is set

K237() is M2(K19(K236()))

K277() is non empty V92() L10()

the carrier of K277() is non empty set

K240( the carrier of K277()) is non empty M19( the carrier of K277())

K276(K277()) is M2(K19(K240( the carrier of K277())))

K19(K240( the carrier of K277())) is set

K20(K276(K277()),NAT) is Relation-like set

K19(K20(K276(K277()),NAT)) is set

K20(NAT,K276(K277())) is Relation-like set

K19(K20(NAT,K276(K277()))) is set

BOOLEAN is non empty set

2 is non empty non pair V21() V22() V23() V27() V28() V121() ext-real non negative M3( REAL , NAT )

2 -tuples_on BOOLEAN is FinSequenceSet of BOOLEAN

K20((2 -tuples_on BOOLEAN),BOOLEAN) is Relation-like set

K19(K20((2 -tuples_on BOOLEAN),BOOLEAN)) is set

3 is non empty non pair V21() V22() V23() V27() V28() V121() ext-real non negative M3( REAL , NAT )

3 -tuples_on BOOLEAN is FinSequenceSet of BOOLEAN

K20((3 -tuples_on BOOLEAN),BOOLEAN) is Relation-like set

K19(K20((3 -tuples_on BOOLEAN),BOOLEAN)) is set

K379() is Relation-like Function-like V18(2 -tuples_on BOOLEAN, BOOLEAN ) boolean-valued M2(K19(K20((2 -tuples_on BOOLEAN),BOOLEAN)))

0 is non pair V21() V22() V23() V27() V28() V121() ext-real non negative M3( REAL , NAT )

f is non pair V21() V22() V23() V27() V28() V121() ext-real non negative set

f -tuples_on BOOLEAN is FinSequenceSet of BOOLEAN

K20((f -tuples_on BOOLEAN),BOOLEAN) is Relation-like set

K19(K20((f -tuples_on BOOLEAN),BOOLEAN)) is set

g is Relation-like Function-like V18(f -tuples_on BOOLEAN, BOOLEAN ) boolean-valued M2(K19(K20((f -tuples_on BOOLEAN),BOOLEAN)))

n is Relation-like Function-like V44(f) V64() set

1GateCircStr (n,g) is non empty non void V58() strict Circuit-like unsplit gate`1=arity gate`2isBoolean gate`2=den ManySortedSign

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

f is non empty finite V79() set

g is non pair V21() V22() V23() V27() V28() V121() ext-real non negative set

g -tuples_on f is FinSequenceSet of f

K20((g -tuples_on f),f) is Relation-like set

K19(K20((g -tuples_on f),f)) is set

n is Relation-like Function-like V44(g) V64() set

S is Relation-like Function-like V18(g -tuples_on f,f) M2(K19(K20((g -tuples_on f),f)))

1GateCircStr (n,S) is non empty non void V58() strict Circuit-like unsplit gate`1=arity gate`2=den ManySortedSign

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

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

the Sorts of (1GateCircuit (n,S)) is Relation-like the carrier of (1GateCircStr (n,S)) -defined Function-like total set

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

K184( the Sorts of (1GateCircuit (n,S))) is functional V77() V78() set

A is M2( the carrier' of (1GateCircStr (n,S)))

x is Relation-like Function-like M2(K184( the Sorts of (1GateCircuit (n,S))))

A depends_on_in x is M2( Args (A,(1GateCircuit (n,S))))

Args (A,(1GateCircuit (n,S))) is M2( proj2 ( the Sorts of (1GateCircuit (n,S)) #))

the Sorts of (1GateCircuit (n,S)) # is Relation-like the carrier of (1GateCircStr (n,S)) * -defined Function-like total set

the carrier of (1GateCircStr (n,S)) * is FinSequenceSet of the carrier of (1GateCircStr (n,S))

proj2 ( the Sorts of (1GateCircuit (n,S)) #) is set

n * x is Relation-like Function-like set

the_arity_of A is Relation-like Function-like V64() M12( the carrier of (1GateCircStr (n,S)), the carrier of (1GateCircStr (n,S)) * )

(the_arity_of A) * x is Relation-like Function-like set

f is non empty finite V79() set

g is non pair V21() V22() V23() V27() V28() V121() ext-real non negative set

g -tuples_on f is FinSequenceSet of f

K20((g -tuples_on f),f) is Relation-like set

K19(K20((g -tuples_on f),f)) is set

n is Relation-like Function-like V44(g) V64() set

S is Relation-like Function-like V18(g -tuples_on f,f) M2(K19(K20((g -tuples_on f),f)))

1GateCircStr (n,S) is non empty non void V58() strict Circuit-like unsplit gate`1=arity gate`2=den ManySortedSign

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

the Sorts of (1GateCircuit (n,S)) is Relation-like the carrier of (1GateCircStr (n,S)) -defined Function-like total set

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

K184( the Sorts of (1GateCircuit (n,S))) is functional V77() V78() set

x is Relation-like Function-like M2(K184( the Sorts of (1GateCircuit (n,S))))

Following x is Relation-like Function-like M2(K184( the Sorts of (1GateCircuit (n,S))))

Following (Following x) is Relation-like Function-like M2(K184( the Sorts of (1GateCircuit (n,S))))

proj1 (Following x) is set

proj2 n is set

[n,S] is non empty pair set

{[n,S]} is Relation-like Function-like set

(proj2 n) \/ {[n,S]} is set

InputVertices (1GateCircStr (n,S)) is M2(K19( the carrier of (1GateCircStr (n,S))))

K19( the carrier of (1GateCircStr (n,S))) is set

the ResultSort of (1GateCircStr (n,S)) is Relation-like Function-like V18( the carrier' of (1GateCircStr (n,S)), the carrier of (1GateCircStr (n,S))) M2(K19(K20( the carrier' of (1GateCircStr (n,S)), the carrier of (1GateCircStr (n,S)))))

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

K20( the carrier' of (1GateCircStr (n,S)), the carrier of (1GateCircStr (n,S))) is Relation-like set

K19(K20( the carrier' of (1GateCircStr (n,S)), the carrier of (1GateCircStr (n,S)))) is set

K422( the carrier of (1GateCircStr (n,S)), the ResultSort of (1GateCircStr (n,S))) is M2(K19( the carrier of (1GateCircStr (n,S))))

K28( the carrier of (1GateCircStr (n,S)),K422( the carrier of (1GateCircStr (n,S)), the ResultSort of (1GateCircStr (n,S)))) is M2(K19( the carrier of (1GateCircStr (n,S))))

InnerVertices (1GateCircStr (n,S)) is M2(K19( the carrier of (1GateCircStr (n,S))))

A2 is set

proj1 x is set

n * x is Relation-like Function-like set

proj1 (n * x) is set

proj1 n is set

n * (Following x) is Relation-like Function-like set

proj1 (n * (Following x)) is set

s is set

n . s is set

(n * (Following x)) . s is set

(Following x) . (n . s) is set

(n * x) . s is set

x . (n . s) is set

AA is M2( the carrier of (1GateCircStr (n,S)))

(Following (Following x)) . AA is set

(Following x) . AA is set

action_at AA is M2( the carrier' of (1GateCircStr (n,S)))

Den ((action_at AA),(1GateCircuit (n,S))) is Relation-like Function-like V18( Args ((action_at AA),(1GateCircuit (n,S))), Result ((action_at AA),(1GateCircuit (n,S)))) M2(K19(K20((Args ((action_at AA),(1GateCircuit (n,S)))),(Result ((action_at AA),(1GateCircuit (n,S)))))))

Args ((action_at AA),(1GateCircuit (n,S))) is M2( proj2 ( the Sorts of (1GateCircuit (n,S)) #))

the Sorts of (1GateCircuit (n,S)) # is Relation-like the carrier of (1GateCircStr (n,S)) * -defined Function-like total set

the carrier of (1GateCircStr (n,S)) * is FinSequenceSet of the carrier of (1GateCircStr (n,S))

proj2 ( the Sorts of (1GateCircuit (n,S)) #) is set

Result ((action_at AA),(1GateCircuit (n,S))) is M2( proj2 the Sorts of (1GateCircuit (n,S)))

proj2 the Sorts of (1GateCircuit (n,S)) is set

K20((Args ((action_at AA),(1GateCircuit (n,S)))),(Result ((action_at AA),(1GateCircuit (n,S))))) is Relation-like set

K19(K20((Args ((action_at AA),(1GateCircuit (n,S)))),(Result ((action_at AA),(1GateCircuit (n,S)))))) is set

(action_at AA) depends_on_in (Following x) is M2( Args ((action_at AA),(1GateCircuit (n,S))))

(Den ((action_at AA),(1GateCircuit (n,S)))) . ((action_at AA) depends_on_in (Following x)) is set

(action_at AA) depends_on_in x is M2( Args ((action_at AA),(1GateCircuit (n,S))))

(Den ((action_at AA),(1GateCircuit (n,S)))) . ((action_at AA) depends_on_in x) is set

(Following (Following x)) . A2 is set

(Following x) . A2 is set

proj1 (Following (Following x)) is set

f is non empty non void V58() Circuit-like ManySortedSign

g is non-empty finite-yielding MSAlgebra over f

the Sorts of g is Relation-like the carrier of f -defined Function-like total set

the carrier of f is non empty set

K184( the Sorts of g) is functional V77() V78() set

n is Relation-like Function-like M2(K184( the Sorts of g))

S is non pair V21() V22() V23() V27() V28() V121() ext-real non negative set

Following (n,S) is Relation-like Function-like M2(K184( the Sorts of g))

Following (Following (n,S)) is Relation-like Function-like M2(K184( the Sorts of g))

S + 1 is non empty non pair V21() V22() V23() V27() V28() V121() ext-real non negative M3( REAL , NAT )

Following (n,(S + 1)) is Relation-like Function-like M2(K184( the Sorts of g))

Following (n,0) is Relation-like Function-like M2(K184( the Sorts of g))

f is non empty non void V58() Circuit-like ManySortedSign

g is non-empty finite-yielding MSAlgebra over f

the Sorts of g is Relation-like the carrier of f -defined Function-like total set

the carrier of f is non empty set

K184( the Sorts of g) is functional V77() V78() set

n is Relation-like Function-like M2(K184( the Sorts of g))

S is non pair V21() V22() V23() V27() V28() V121() ext-real non negative set

Following (n,S) is Relation-like Function-like M2(K184( the Sorts of g))

A is non pair V21() V22() V23() V27() V28() V121() ext-real non negative set

Following (n,A) is Relation-like Function-like M2(K184( the Sorts of g))

x is non pair V21() V22() V23() V27() V28() V121() ext-real non negative set

S + x is non pair V21() V22() V23() V27() V28() V121() ext-real non negative set

S9 is non pair V21() V22() V23() V27() V28() V121() ext-real non negative set

Following ((Following (n,S)),S9) is Relation-like Function-like M2(K184( the Sorts of g))

F

F

[F

f is Relation-like Function-like set

proj1 f is set

f . 0 is set

g is Relation-like NAT -defined Function-like total set

n is Relation-like NAT -defined Function-like total set

g . 0 is set

n . 0 is set

(f . 0) `1 is set

(f . 0) `2 is set

S is non pair V21() V22() V23() V27() V28() V121() ext-real non negative set

g . S is set

n . S is set

S + 1 is non empty non pair V21() V22() V23() V27() V28() V121() ext-real non negative M3( REAL , NAT )

g . (S + 1) is set

n . (S + 1) is set

A is non empty V58() ManySortedSign

x is set

F

F

f . S is set

(f . S) `2 is set

(f . S) `1 is set

f . (S + 1) is set

F

F

[F

(f . (S + 1)) `1 is set

(f . (S + 1)) `2 is set

F

F

F

F

f is non pair V21() V22() V23() V27() V28() V121() ext-real non negative set

F

F

f + 1 is non empty non pair V21() V22() V23() V27() V28() V121() ext-real non negative M3( REAL , NAT )

F

F

g is non empty V58() ManySortedSign

F

F

f is non empty V58() ManySortedSign

g is set

F

F

F

F

F

f is non pair V21() V22() V23() V27() V28() V121() ext-real non negative set

F

f + 1 is non empty non pair V21() V22() V23() V27() V28() V121() ext-real non negative M3( REAL , NAT )

F

g is set

F

S is non empty V58() ManySortedSign

n is non pair V21() V22() V23() V27() V28() V121() ext-real non negative set

F

A is set

F

S is non empty V58() ManySortedSign

n is non pair V21() V22() V23() V27() V28() V121() ext-real non negative set

F

A is set

F

n + 1 is non empty non pair V21() V22() V23() V27() V28() V121() ext-real non negative M3( REAL , NAT )

F

F

F

F

F

n is non empty V58() ManySortedSign

F

F

F

f is Relation-like NAT -defined Function-like total set

f . 0 is set

g is Relation-like NAT -defined Function-like total set

g . 0 is set

S is non empty V58() ManySortedSign

n is non pair V21() V22() V23() V27() V28() V121() ext-real non negative set

f . n is set

A is set

g . n is set

f . F

n is non empty V58() ManySortedSign

A is non empty V58() ManySortedSign

S is non pair V21() V22() V23() V27() V28() V121() ext-real non negative set

f . S is set

x is set

g . S is set

S + 1 is non empty non pair V21() V22() V23() V27() V28() V121() ext-real non negative M3( REAL , NAT )

f . (S + 1) is set

F

g . (S + 1) is set

F

F

F

F

f is non empty V58() ManySortedSign

g is non empty V58() ManySortedSign

n is Relation-like NAT -defined Function-like total set

n . F

n . 0 is set

S is Relation-like NAT -defined Function-like total set

S . 0 is set

x is non empty V58() ManySortedSign

A is non pair V21() V22() V23() V27() V28() V121() ext-real non negative set

n . A is set

S9 is set

S . A is set

A + 1 is non empty non pair V21() V22() V23() V27() V28() V121() ext-real non negative M3( REAL , NAT )

n . (A + 1) is set

F

S . (A + 1) is set

F

x is non empty V58() ManySortedSign

A is non pair V21() V22() V23() V27() V28() V121() ext-real non negative set

n . A is set

S9 is set

S . A is set

A is Relation-like NAT -defined Function-like total set

A . F

A . 0 is set

x is Relation-like NAT -defined Function-like total set

x . 0 is set

A9 is non empty V58() ManySortedSign

S9 is non pair V21() V22() V23() V27() V28() V121() ext-real non negative set

A . S9 is set

A2 is set

x . S9 is set

S9 + 1 is non empty non pair V21() V22() V23() V27() V28() V121() ext-real non negative M3( REAL , NAT )

A . (S9 + 1) is set

F

x . (S9 + 1) is set

F

A9 is non empty V58() ManySortedSign

S9 is non pair V21() V22() V23() V27() V28() V121() ext-real non negative set

A . S9 is set

A2 is set

x . S9 is set

S9 is non pair V21() V22() V23() V27() V28() V121() ext-real non negative set

S . S9 is set

x . S9 is set

n . S9 is set

S9 + 1 is non empty non pair V21() V22() V23() V27() V28() V121() ext-real non negative M3( REAL , NAT )

S . (S9 + 1) is set

F

A9 is non empty V58() ManySortedSign

A . S9 is set

x . (S9 + 1) is set

A9 is non empty V58() ManySortedSign

S9 is set

S . S9 is set

x . S9 is set

S9 is non pair V21() V22() V23() V27() V28() V121() ext-real non negative set

n . S9 is set

A . S9 is set

S . S9 is set

A9 is non empty V58() ManySortedSign

S9 + 1 is non empty non pair V21() V22() V23() V27() V28() V121() ext-real non negative M3( REAL , NAT )

n . (S9 + 1) is set

F

A . (S9 + 1) is set

F

F

F

F

F

F

f is non empty V58() ManySortedSign

g is Relation-like NAT -defined Function-like total set

g . F

g . 0 is set

n is Relation-like NAT -defined Function-like total set

n . 0 is set

A is non empty V58() ManySortedSign

S is non pair V21() V22() V23() V27() V28() V121() ext-real non negative set

g . S is set

x is set

n . S is set

F

A is non empty V58() ManySortedSign

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

x is non empty V58() ManySortedSign

A is non pair V21() V22() V23() V27() V28() V121() ext-real non negative set

g . A is set

S9 is set

n . A is set

A + 1 is non empty non pair V21() V22() V23() V27() V28() V121() ext-real non negative M3( REAL , NAT )

g . (A + 1) is set

F

n . (A + 1) is set

F

F

F

F

f is non empty non void V58() strict Circuit-like unsplit gate`1=arity gate`2isBoolean gate`2=den ManySortedSign

g is set

n is non pair V21() V22() V23() V27() V28() V121() ext-real non negative set

F

f +* F

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

A is set

x is non pair V21() V22() V23() V27() V28() V121() ext-real non negative set

F

S +* F

S9 is non empty non void V58() strict Circuit-like unsplit gate`1=arity gate`2isBoolean gate`2=den ManySortedSign

A9 is set

A2 is non pair V21() V22() V23() V27() V28() V121() ext-real non negative set

F

S9 +* F

AA is non empty non void V58() strict Circuit-like unsplit gate`1=arity gate`2isBoolean gate`2=den ManySortedSign

s is set

s3 is non pair V21() V22() V23() V27() V28() V121() ext-real non negative set

F

AA +* F

s0 is non empty non void V58() strict Circuit-like unsplit gate`1=arity gate`2isBoolean gate`2=den ManySortedSign

s2 is set

c

F

s0 +* F

c

c

c

F

c

F

F

F

f is non empty non void V58() strict Circuit-like unsplit gate`1=arity gate`2isBoolean gate`2=den ManySortedSign

n is Relation-like NAT -defined Function-like total set

n . F

n . 0 is set

S is Relation-like NAT -defined Function-like total set

S . 0 is set

g is non empty non void V58() strict Circuit-like unsplit gate`1=arity gate`2isBoolean gate`2=den ManySortedSign

A is Relation-like NAT -defined Function-like total set

A . F

A . 0 is set

x is Relation-like NAT -defined Function-like total set

x . 0 is set

f is non empty V58() ManySortedSign

g is non empty V58() ManySortedSign

f +* g is non empty V58() strict ManySortedSign

InputVertices (f +* g) is M2(K19( the carrier of (f +* g)))

the carrier of (f +* g) is non empty set

K19( the carrier of (f +* g)) is set

the ResultSort of (f +* g) is Relation-like Function-like V18( the carrier' of (f +* g), the carrier of (f +* g)) M2(K19(K20( the carrier' of (f +* g), the carrier of (f +* g))))

the carrier' of (f +* g) is set

K20( the carrier' of (f +* g), the carrier of (f +* g)) is Relation-like set

K19(K20( the carrier' of (f +* g), the carrier of (f +* g))) is set

K422( the carrier of (f +* g), the ResultSort of (f +* g)) is M2(K19( the carrier of (f +* g)))

K28( the carrier of (f +* g),K422( the carrier of (f +* g), the ResultSort of (f +* g))) is M2(K19( the carrier of (f +* g)))

InputVertices f is M2(K19( the carrier of f))

the carrier of f is non empty set

K19( the carrier of f) is set

the ResultSort of f is Relation-like Function-like V18( the carrier' of f, the carrier of f) M2(K19(K20( the carrier' of f, the carrier of f)))

the carrier' of f is set

K20( the carrier' of f, the carrier of f) is Relation-like set

K19(K20( the carrier' of f, the carrier of f)) is set

K422( the carrier of f, the ResultSort of f) is M2(K19( the carrier of f))

K28( the carrier of f,K422( the carrier of f, the ResultSort of f)) is M2(K19( the carrier of f))

InnerVertices g is M2(K19( the carrier of g))

the carrier of g is non empty set

K19( the carrier of g) is set

the ResultSort of g is Relation-like Function-like V18( the carrier' of g, the carrier of g) M2(K19(K20( the carrier' of g, the carrier of g)))

the carrier' of g is set

K20( the carrier' of g, the carrier of g) is Relation-like set

K19(K20( the carrier' of g, the carrier of g)) is set

K422( the carrier of g, the ResultSort of g) is M2(K19( the carrier of g))

(InputVertices f) \ (InnerVertices g) is set

InputVertices g is M2(K19( the carrier of g))

K28( the carrier of g,K422( the carrier of g, the ResultSort of g)) is M2(K19( the carrier of g))

InnerVertices f is M2(K19( the carrier of f))

(InputVertices g) \ (InnerVertices f) is set

((InputVertices f) \ (InnerVertices g)) \/ ((InputVertices g) \ (InnerVertices f)) is set

proj2 the ResultSort of f is set

proj2 the ResultSort of g is set

(proj2 the ResultSort of f) \/ (proj2 the ResultSort of g) is set

the carrier of f \ ((proj2 the ResultSort of f) \/ (proj2 the ResultSort of g)) is set

the ResultSort of f +* the ResultSort of g is Relation-like Function-like set

proj2 ( the ResultSort of f +* the ResultSort of g) is set

the carrier of (f +* g) \ (proj2 ( the ResultSort of f +* the ResultSort of g)) is set

the carrier of f \/ the carrier of g is set

( the carrier of f \/ the carrier of g) \ (proj2 ( the ResultSort of f +* the ResultSort of g)) is set

( the carrier of f \/ the carrier of g) \ ((proj2 the ResultSort of f) \/ (proj2 the ResultSort of g)) is set

the carrier of g \ ((proj2 the ResultSort of f) \/ (proj2 the ResultSort of g)) is set

( the carrier of f \ ((proj2 the ResultSort of f) \/ (proj2 the ResultSort of g))) \/ ( the carrier of g \ ((proj2 the ResultSort of f) \/ (proj2 the ResultSort of g))) is set

f is non with_pair set

g is Relation-like set

f \ g is non with_pair set

f /\ g is Relation-like non-empty empty-yielding Function-like one-to-one constant functional empty non pair V21() V22() V23() V25() V26() V27() V28() V76() V77() non with_pair V121() ext-real non negative set

f is Relation-like set

n is set

g is set

g \ n is set

f \ g is Relation-like set

f \ n is Relation-like set

f /\ (g \ n) is Relation-like set

S is set

f \ (g \ n) is Relation-like set

(g \ n) \/ n is set

f \ ((g \ n) \/ n) is Relation-like set

g is set

f is set

f \ g is set

n is Relation-like set

f \ n is set

n \ g is Relation-like set

(n \ g) /\ (f \ g) is Relation-like set

S is set

(f \ g) \ (n \ g) is set

(n \ g) \/ g is set

f \ ((n \ g) \/ g) is set

F

InnerVertices F

the carrier of F

K19( the carrier of F

the ResultSort of F

the carrier' of F

K20( the carrier' of F

K19(K20( the carrier' of F

K422( the carrier of F

InputVertices F

K28( the carrier of F

F

F

F

F

InnerVertices F

the carrier of F

K19( the carrier of F

the ResultSort of F

the carrier' of F

K20( the carrier' of F

K19(K20( the carrier' of F

K422( the carrier of F

f is non pair V21() V22() V23() V27() V28() V121() ext-real non negative set

F

f + 1 is non empty non pair V21() V22() V23() V27() V28() V121() ext-real non negative M3( REAL , NAT )

F

F

F

InputVertices F

the carrier of F

K19( the carrier of F

the ResultSort of F

the carrier' of F

K20( the carrier' of F

K19(K20( the carrier' of F

K422( the carrier of F

K28( the carrier of F

{(F

(InputVertices F

F

(f + 1) + 1 is non empty non pair V21() V22() V23() V27() V28() V121() ext-real non negative M3( REAL , NAT )

F

F

InputVertices F

the carrier of F

K19( the carrier of F

the ResultSort of F

the carrier' of F

K20( the carrier' of F

K19(K20( the carrier' of F

K422( the carrier of F

K28( the carrier of F

{(F

(InputVertices F

F

g is non empty non void V58() Circuit-like unsplit gate`1=arity gate`2isBoolean gate`2=den ManySortedSign

n is non empty non void V58() Circuit-like unsplit gate`1=arity gate`2isBoolean gate`2=den ManySortedSign

InputVertices n is M2(K19( the carrier of n))

the carrier of n is non empty set

K19( the carrier of n) is set

the ResultSort of n is Relation-like Function-like V18( the carrier' of n, the carrier of n) M2(K19(K20( the carrier' of n, the carrier of n)))

the carrier' of n is non empty set

K20( the carrier' of n, the carrier of n) is Relation-like set

K19(K20( the carrier' of n, the carrier of n)) is set

K422( the carrier of n, the ResultSort of n) is M2(K19( the carrier of n))

K28( the carrier of n,K422( the carrier of n, the ResultSort of n)) is M2(K19( the carrier of n))

InputVertices g is M2(K19( the carrier of g))

the carrier of g is non empty set

K19( the carrier of g) is set

the ResultSort of g is Relation-like Function-like V18( the carrier' of g, the carrier of g) M2(K19(K20( the carrier' of g, the carrier of g)))

the carrier' of g is non empty set

K20( the carrier' of g, the carrier of g) is Relation-like set

K19(K20( the carrier' of g, the carrier of g)) is set

K422( the carrier of g, the ResultSort of g) is M2(K19( the carrier of g))

K28( the carrier of g,K422( the carrier of g, the ResultSort of g)) is M2(K19( the carrier of g))

(InputVertices g) \/ ((InputVertices F

InnerVertices n is M2(K19( the carrier of n))

(InputVertices n) \/ ((InputVertices F

n +* F

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

InputVertices S is M2(K19( the carrier of S))

the carrier of S is non empty set

K19( the carrier of S) is set

the ResultSort of S is Relation-like Function-like V18( the carrier' of S, the carrier of S) M2(K19(K20( the carrier' of S, the carrier of S)))

the carrier' of S is non empty set

K20( the carrier' of S, the carrier of S) is Relation-like set

K19(K20( the carrier' of S, the carrier of S)) is set

K422( the carrier of S, the ResultSort of S) is M2(K19( the carrier of S))

K28( the carrier of S,K422( the carrier of S, the ResultSort of S)) is M2(K19( the carrier of S))

InnerVertices S is M2(K19( the carrier of S))

(f + 1) + 1 is non empty non pair V21() V22() V23() V27() V28() V121() ext-real non negative M3( REAL , NAT )

F

InnerVertices F

(InputVertices n) \ (InnerVertices F

(InputVertices F

((InputVertices n) \ (InnerVertices F

(InputVertices n) \/ ((InputVertices F

A is non with_pair set

x is non with_pair set

A \/ x is non with_pair set

F

F

S9 is Relation-like set

A9 is Relation-like set

S9 \/ A9 is Relation-like set

f is non pair V21() V22() V23() V27() V28() V121() ext-real non negative set

F

f + 1 is non empty non pair V21() V22() V23() V27() V28() V121() ext-real non negative M3( REAL , NAT )

F

F

F

InputVertices F

the carrier of F

K19( the carrier of F

the ResultSort of F

the carrier' of F

K20( the carrier' of F

K19(K20( the carrier' of F

K422( the carrier of F

K28( the carrier of F

{(F

(InputVertices F

F

InputVertices (F

the carrier of (F

K19( the carrier of (F

the ResultSort of (F

the carrier' of (F

K20( the carrier' of (F

K19(K20( the carrier' of (F

K422( the carrier of (F

K28( the carrier of (F

(InputVertices F

InputVertices F

K28( the carrier of F

(InputVertices F

((InputVertices F

(InputVertices F

0 + 1 is non empty non pair V21() V22() V23() V27() V28() V121() ext-real non negative M3( REAL , NAT )

F

{(F

(InputVertices F

F

S is non empty non void V58() Circuit-like unsplit gate`1=arity gate`2isBoolean gate`2=den ManySortedSign

InputVertices S is M2(K19( the carrier of S))

the carrier of S is non empty set

K19( the carrier of S) is set

the ResultSort of S is Relation-like Function-like V18( the carrier' of S, the carrier of S) M2(K19(K20( the carrier' of S, the carrier of S)))

the carrier' of S is non empty set

K20( the carrier' of S, the carrier of S) is Relation-like set

K19(K20( the carrier' of S, the carrier of S)) is set

K422( the carrier of S, the ResultSort of S) is M2(K19( the carrier of S))

K28( the carrier of S,K422( the carrier of S, the ResultSort of S)) is M2(K19( the carrier of S))

(InputVertices S) \/ ((InputVertices F

A is non empty non void V58() strict Circuit-like unsplit gate`1=arity gate`2isBoolean gate`2=den ManySortedSign

InputVertices A is M2(K19( the carrier of A))

the carrier of A is non empty set

K19( the carrier of A) is set

the ResultSort of A is Relation-like Function-like V18( the carrier' of A, the carrier of A) M2(K19(K20( the carrier' of A, the carrier of A)))

the carrier' of A is non empty set

K20( the carrier' of A, the carrier of A) is Relation-like set

K19(K20( the carrier' of A, the carrier of A)) is set

K422( the carrier of A, the ResultSort of A) is M2(K19( the carrier of A))

K28( the carrier of A,K422( the carrier of A, the ResultSort of A)) is M2(K19( the carrier of A))

InnerVertices A is M2(K19( the carrier of A))

0 + 1 is non empty non pair V21() V22() V23() V27() V28() V121() ext-real non negative M3( REAL , NAT )

F

A9 is set

n is non with_pair set

g is non with_pair set

n \/ g is non with_pair set

F

F

S9 is Relation-like set

x is Relation-like set

x \/ S9 is Relation-like set

F

g is non empty non void V58() Circuit-like unsplit gate`1=arity gate`2isBoolean gate`2=den ManySortedSign

n is non empty non void V58() Circuit-like unsplit gate`1=arity gate`2isBoolean gate`2=den ManySortedSign

InputVertices n is M2(K19( the carrier of n))

the carrier of n is non empty set

K19( the carrier of n) is set

the ResultSort of n is Relation-like Function-like V18( the carrier' of n, the carrier of n) M2(K19(K20( the carrier' of n, the carrier of n)))

the carrier' of n is non empty set

K20( the carrier' of n, the carrier of n) is Relation-like set

K19(K20( the carrier' of n, the carrier of n)) is set

K422( the carrier of n, the ResultSort of n) is M2(K19( the carrier of n))

K28( the carrier of n,K422( the carrier of n, the ResultSort of n)) is M2(K19( the carrier of n))

InputVertices g is M2(K19( the carrier of g))

the carrier of g is non empty set

K19( the carrier of g) is set

the ResultSort of g is Relation-like Function-like V18( the carrier' of g, the carrier of g) M2(K19(K20( the carrier' of g, the carrier of g)))

the carrier' of g is non empty set

K20( the carrier' of g, the carrier of g) is Relation-like set

K19(K20( the carrier' of g, the carrier of g)) is set

K422( the carrier of g, the ResultSort of g) is M2(K19( the carrier of g))

K28( the carrier of g,K422( the carrier of g, the ResultSort of g)) is M2(K19( the carrier of g))

(InputVertices g) \/ ((InputVertices F

InnerVertices n is M2(K19( the carrier of n))

InnerVertices g is M2(K19( the carrier of g))

S is non pair V21() V22() V23() V27() V28() V121() ext-real non negative set

S + 1 is non empty non pair V21() V22() V23() V27() V28() V121() ext-real non negative M3( REAL , NAT )

S is non pair V21() V22() V23() V27() V28() V121() ext-real non negative set

S + 1 is non empty non pair V21() V22() V23() V27() V28() V121() ext-real non negative M3( REAL , NAT )

A is non pair V21() V22() V23() V27() V28() V121() ext-real non negative set

F

A + 1 is non empty non pair V21() V22() V23() V27() V28() V121() ext-real non negative M3( REAL , NAT )

F

F

F

InputVertices F

the carrier of F

K19( the carrier of F

the ResultSort of F

the carrier' of F

K20( the carrier' of F

K19(K20( the carrier' of F

K422( the carrier of F

K28( the carrier of F

{(F

(InputVertices F

F

x is non empty non void V58() Circuit-like unsplit gate`1=arity gate`2isBoolean gate`2=den ManySortedSign

S9 is non empty non void V58() Circuit-like unsplit gate`1=arity gate`2isBoolean gate`2=den ManySortedSign

InputVertices S9 is M2(K19( the carrier of S9))

the carrier of S9 is non empty set

K19( the carrier of S9) is set

the ResultSort of S9 is Relation-like Function-like V18( the carrier' of S9, the carrier of S9) M2(K19(K20( the carrier' of S9, the carrier of S9)))

the carrier' of S9 is non empty set

K20( the carrier' of S9, the carrier of S9) is Relation-like set

K19(K20( the carrier' of S9, the carrier of S9)) is set

K422( the carrier of S9, the ResultSort of S9) is M2(K19( the carrier of S9))

K28( the carrier of S9,K422( the carrier of S9, the ResultSort of S9)) is M2(K19( the carrier of S9))

InputVertices x is M2(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 V18( the carrier' of x, the carrier of x) M2(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

K422( the carrier of x, the ResultSort of x) is M2(K19( the carrier of x))

K28( the carrier of x,K422( the carrier of x, the ResultSort of x)) is M2(K19( the carrier of x))

(InputVertices x) \/ ((InputVertices F

InnerVertices S9 is M2(K19( the carrier of S9))

F

InnerVertices F

the carrier of F

K19( the carrier of F

the ResultSort of F

the carrier' of F

K20( the carrier' of F

K19(K20( the carrier' of F

K422( the carrier of F

InputVertices F

K28( the carrier of F

F

F

g is non empty V58() ManySortedSign

f is non pair V21() V22() V23() V27() V28() V121() ext-real non negative set

F

n is set

F

f + 1 is non empty non pair V21() V22() V23() V27() V28() V121() ext-real non negative M3( REAL , NAT )

F

F

g +* F

F

F

InputVertices F

the carrier of F

K19( the carrier of F

the ResultSort of F

the carrier' of F

K20( the carrier' of F

K19(K20( the carrier' of F

K422( the carrier of F

K28( the carrier of F

InnerVertices F

f is non pair V21() V22() V23() V27() V28() V121() ext-real non negative set

f + 1 is non empty non pair V21() V22() V23() V27() V28() V121() ext-real non negative M3( REAL , NAT )

F

InputVertices F

the carrier of F

K19( the carrier of F

the ResultSort of F

the carrier' of F

K20( the carrier' of F

K19(K20( the carrier' of F

K422( the carrier of F

K28( the carrier of F

F

InputVertices F

the carrier of F

K19( the carrier of F

the ResultSort of F

the carrier' of F

K20( the carrier' of F

K19(K20( the carrier' of F

K422( the carrier of F

K28( the carrier of F

F

F

InputVertices F

the carrier of F

K19( the carrier of F

the ResultSort of F

the carrier' of F

K20( the carrier' of F

K19(K20( the carrier' of F

K422( the carrier of F

K28( the carrier of F

{(F

(InputVertices F

(InputVertices F

InnerVertices F

n is set

g is non pair V21() V22() V23() V27() V28() V121() ext-real non negative set

F

F

InputVertices F

the carrier of F

K19( the carrier of F

the ResultSort of F

the carrier' of F

K20( the carrier' of F

K19(K20( the carrier' of F

K422( the carrier of F

K28( the carrier of F

{n} is set

(InputVertices F

InnerVertices H

the carrier of H

K19( the carrier of H

n is set

g is non pair V21() V22() V23() V27() V28() V121() ext-real non negative set

F

InnerVertices F

the carrier of F

K19( the carrier of F

the ResultSort of F

the carrier' of F

K20( the carrier' of F

K19(K20( the carrier' of F

K422( the carrier of F

g is non empty non void V58() Circuit-like unsplit gate`1=arity gate`2isBoolean gate`2=den ManySortedSign

n is non empty non void V58() Circuit-like unsplit gate`1=arity gate`2isBoolean gate`2=den ManySortedSign

InputVertices n is M2(K19( the carrier of n))

the carrier of n is non empty set

K19( the carrier of n) is set

the ResultSort of n is Relation-like Function-like V18( the carrier' of n, the carrier of n) M2(K19(K20( the carrier' of n, the carrier of n)))

the carrier' of n is non empty set

K20( the carrier' of n, the carrier of n) is Relation-like set

K19(K20( the carrier' of n, the carrier of n)) is set

K422( the carrier of n, the ResultSort of n) is M2(K19( the carrier of n))

K28( the carrier of n,K422( the carrier of n, the ResultSort of n)) is M2(K19( the carrier of n))

InputVertices g is M2(K19( the carrier of g))

the carrier of g is non empty set

K19( the carrier of g) is set

the ResultSort of g is Relation-like Function-like V18( the carrier' of g, the carrier of g) M2(K19(K20( the carrier' of g, the carrier of g)))

the carrier' of g is non empty set

K20( the carrier' of g, the carrier of g) is Relation-like set

K19(K20( the carrier' of g, the carrier of g)) is set

K422( the carrier of g, the ResultSort of g) is M2(K19( the carrier of g))

K28( the carrier of g,K422( the carrier of g, the ResultSort of g)) is M2(K19( the carrier of g))

(InputVertices g) \/ ((InputVertices F

InnerVertices g is M2(K19( the carrier of g))

F

F

F

[F

[[F

f is Relation-like Function-like set

proj1 f is set

f . 0 is set

(f . 0) `2 is set

g is Relation-like NAT -defined Function-like total set

n is Relation-like NAT -defined Function-like total set

S is Relation-like NAT -defined Function-like total set

g . 0 is set

S . 0 is set

n . 0 is set

(f . 0) `11 is set

(f . 0) `12 is set

A is non pair V21() V22() V23() V27() V28() V121() ext-real non negative set

g . A is set

S . A is set

n . A is set

A + 1 is non empty non pair V21() V22() V23() V27() V28() V121() ext-real non negative M3( REAL , NAT )

g . (A + 1) is set

S . (A + 1) is set

n . (A + 1) is set

x is non empty V58() ManySortedSign

S9 is non-empty MSAlgebra over x

A9 is set

F

F

F

f . A is set

(f . A) `2 is set

(f . A) `12 is set

(f . A) `11 is set

f . (A + 1) is set

F

F

[F

F

[[F

(f . (A + 1)) `2 is set

(f . (A + 1)) `11 is set

(f . (A + 1)) `12 is set

F

F

F

F

F

F

f is non pair V21() V22() V23() V27() V28() V121() ext-real non negative set

F

F

F

f + 1 is non empty non pair V21() V22() V23() V27() V28() V121() ext-real non negative M3( REAL , NAT )

F

F

F

g is non empty V58() ManySortedSign

n is non-empty MSAlgebra over g

S is set

F

A is non empty V58() ManySortedSign

F

x is non-empty MSAlgebra over A

S9 is set

F

f is non pair V21() V22() V23() V27() V28() V121() ext-real non negative set

F

F

F

g is non empty V58() ManySortedSign

n is non-empty MSAlgebra over g

S is set

g is non empty V58() ManySortedSign

n is non-empty MSAlgebra over g

S is set

F

F

F

F

F

F

F

F

F

F

F

F

g is non empty V58() ManySortedSign

f is non pair V21() V22() V23() V27() V28() V121() ext-real non negative set

F

n is non-empty MSAlgebra over g

F

S is set

F

f + 1 is non empty non pair V21() V22() V23() V27() V28() V121() ext-real non negative M3( REAL , NAT )

F

F

F

F

F

F

A is non empty V58() ManySortedSign

S is non pair V21() V22() V23() V27() V28() V121() ext-real non negative set

F

x is non-empty MSAlgebra over A

F

S9 is set

F

S is non empty V58() ManySortedSign

A is non-empty MSAlgebra over S

x is set

S9 is non pair V21() V22() V23() V27() V28() V121() ext-real non negative set

F

F

S is non empty V58() ManySortedSign

A is non-empty MSAlgebra over S

A9 is non empty V58() ManySortedSign

S9 is non pair V21() V22() V23() V27() V28() V121() ext-real non negative set

F

A2 is non-empty MSAlgebra over A9

F

AA is set

F

A9 is non empty V58() ManySortedSign

S9 is non pair V21() V22() V23() V27() V28() V121() ext-real non negative set

F

A2 is non-empty MSAlgebra over A9

F

AA is set

F

S9 + 1 is non empty non pair V21() V22() V23() V27() V28() V121() ext-real non negative M3( REAL , NAT )

F

F

F

F

F

F

S9 is non empty V58() ManySortedSign

A9 is non-empty MSAlgebra over S9

S9 is non pair V21() V22() V23() V27() V28() V121() ext-real non negative set

F

F

F

F

S9 + 1 is non empty non pair V21() V22() V23() V27() V28() V121() ext-real non negative M3( REAL , NAT )

F

F

A9 is non empty V58() ManySortedSign

A2 is non-empty MSAlgebra over A9

F

F

F

A9 is non empty V58() ManySortedSign

A2 is non-empty MSAlgebra over A9

S9 is set

F

F

S9 is non pair V21() V22() V23() V27() V28() V121() ext-real non negative set

F

F

F

F

A9 is non empty V58() ManySortedSign

A2 is non-empty MSAlgebra over A9

S9 + 1 is non empty non pair V21() V22() V23() V27() V28() V121() ext-real non negative M3( REAL , NAT )

F

F

F

F

F

F

F

S9 is set

F

F

A9 is set

F

F

F

F

F

F

F

F

F

F

f is non pair V21() V22() V23() V27() V28() V121() ext-real non negative set

F

F

f + 1 is non empty non pair V21() V22() V23() V27() V28() V121() ext-real non negative M3( REAL , NAT )

F

F

g is non empty V58() ManySortedSign

n is set

F

F

A is non empty V58() ManySortedSign

S is non pair V21() V22() V23() V27() V28() V121() ext-real non negative set

F

x is non-empty MSAlgebra over A

F

S9 is set

F

S is non empty V58() ManySortedSign

A is non-empty MSAlgebra over S

x is set

S9 is non pair V21() V22() V23() V27() V28() V121() ext-real non negative set

F

F

A is non empty V58() ManySortedSign

S is non pair V21() V22() V23() V27() V28() V121() ext-real non negative set

F

x is non-empty MSAlgebra over A

F

S9 is set

F

S + 1 is non empty non pair V21() V22() V23() V27() V28() V121() ext-real non negative M3( REAL , NAT )

F

F

F

F

F

F

F

S is non empty V58() ManySortedSign

A is non-empty MSAlgebra over S

F

F

F

F

f is non empty V58() ManySortedSign

g is non-empty MSAlgebra over f

n is set

S is non pair V21() V22() V23() V27() V28() V121() ext-real non negative set

F

F

f is Relation-like NAT -defined Function-like total set

f . 0 is set

g is Relation-like NAT -defined Function-like total set

g . 0 is set

n is Relation-like NAT -defined Function-like total set

n . 0 is set

A is non empty V58() ManySortedSign

S is non pair V21() V22() V23() V27() V28() V121() ext-real non negative set

f . S is set

x is non-empty MSAlgebra over A

g . S is set

S9 is set

n . S is set

f . F

g . F

S is non empty V58() ManySortedSign

A is non-empty MSAlgebra over S

S9 is non empty V58() ManySortedSign

x is non pair V21() V22() V23() V27() V28() V121() ext-real non negative set

f . x is set

A9 is non-empty MSAlgebra over S9

g . x is set

A2 is set

n . x is set

x + 1 is non empty non pair V21() V22() V23() V27() V28() V121() ext-real non negative M3( REAL , NAT )

f . (x + 1) is set

F

g . (x + 1) is set

F

n . (x + 1) is set

F

F

F

F

F

F

f is non empty V58() ManySortedSign

g is non-empty MSAlgebra over f

n is set

S is non pair V21() V22() V23() V27() V28() V121() ext-real non negative set

F

F

f is Relation-like NAT -defined Function-like total set

f . 0 is set

g is Relation-like NAT -defined Function-like total set

g . 0 is set

n is Relation-like NAT -defined Function-like total set

n . 0 is set

A is non empty V58() ManySortedSign

S is non pair V21() V22() V23() V27() V28() V121() ext-real non negative set

f . S is set

x is non-empty MSAlgebra over A

g . S is set

S9 is set

n . S is set

A is non empty V58() ManySortedSign

S is non pair V21() V22() V23() V27() V28() V121() ext-real non negative set

f . S is set

x is non-empty MSAlgebra over A

g . S is set

S9 is set

n . S is set

f . F

g . F

S is non empty V58() ManySortedSign

A is non-empty MSAlgebra over S

x is Relation-like NAT -defined Function-like total set

x . F

x . 0 is set

S9 is Relation-like NAT -defined Function-like total set

S9 . 0 is set

x is Relation-like NAT -defined Function-like total set

x . F

x . 0 is set

S9 is Relation-like NAT -defined Function-like total set

S9 . 0 is set

A2 is non empty V58() ManySortedSign

A9 is non pair V21() V22() V23() V27() V28() V121() ext-real non negative set

x . A9 is set

AA is set

S9 . A9 is set

A9 is non pair V21() V22() V23() V27() V28() V121() ext-real non negative set

S9 . A9 is set

n . A9 is set

x . A9 is set

A9 + 1 is non empty non pair V21() V22() V23() V27() V28() V121() ext-real non negative M3( REAL , NAT )

S9 . (A9 + 1) is set

F

A2 is non empty V58() ManySortedSign

f . A9 is set

g . A9 is set

n . (A9 + 1) is set

A2 is non empty V58() ManySortedSign

AA is non-empty MSAlgebra over A2

A9 is set

S9 . A9 is set

n . A9 is set

A9 is non pair V21() V22() V23() V27() V28() V121() ext-real non negative set

f . A9 is set

g . A9 is set

A2 is non empty V58() ManySortedSign

AA is non-empty MSAlgebra over A2

x . A9 is set

A9 + 1 is non empty non pair V21() V22() V23() V27() V28() V121() ext-real non negative M3( REAL , NAT )

x . (A9 + 1) is set

S9 . A9 is set

F

f . (A9 + 1) is set

A9 is set

x . A9 is set

f . A9 is set

A9 is non-empty MSAlgebra over F

AA is non empty V58() ManySortedSign

A2 is non pair V21() V22() V23() V27() V28() V121() ext-real non negative set

f . A2 is set

s is non-empty MSAlgebra over AA

g . A2 is set

s3 is set

n . A2 is set

A2 + 1 is non empty non pair V21() V22() V23() V27() V28() V121() ext-real non negative M3( REAL , NAT )

f . (A2 + 1) is set

F

g . (A2 + 1) is set

F

n . (A2 + 1) is set

F

F

F

F

F

F

f is non empty V58() ManySortedSign

g is non-empty MSAlgebra over f

n is set

S is non pair V21() V22() V23() V27() V28() V121() ext-real non negative set

F

F

f is non-empty MSAlgebra over F

g is non-empty MSAlgebra over F

n is Relation-like NAT -defined Function-like total set

n . F

S is Relation-like NAT -defined Function-like total set

S . F

n . 0 is set

S . 0 is set

A is Relation-like NAT -defined Function-like total set

A . 0 is set

x is Relation-like NAT -defined Function-like total set

x . F

S9 is Relation-like NAT -defined Function-like total set

S9 . F

x . 0 is set

S9 . 0 is set

A9 is Relation-like NAT -defined Function-like total set

A9 . 0 is set

F

F

F

F

F

f is non empty V58() ManySortedSign

g is non-empty MSAlgebra over f

n is set

S is non pair V21() V22() V23() V27() V28() V121() ext-real non negative set

F

F

f is Relation-like NAT -defined Function-like total set

f . 0 is set

g is Relation-like NAT -defined Function-like total set

g . 0 is set

n is Relation-like NAT -defined Function-like total set

n . 0 is set

A is non empty V58() ManySortedSign

S is non pair V21() V22() V23() V27() V28() V121() ext-real non negative set

f . S is set

x is non-empty MSAlgebra over A

g . S is set

S9 is set

n . S is set

S is non pair V21() V22() V23() V27() V28() V121() ext-real non negative set

f . S is set

g . S is set

n . S is set

S + 1 is non empty non pair V21() V22() V23() V27() V28() V121() ext-real non negative M3( REAL , NAT )

A is non empty V58() ManySortedSign

x is non-empty MSAlgebra over A

S9 is set

F

F

F

A2 is non empty non void V58() strict Circuit-like unsplit gate`1=arity gate`2isBoolean gate`2=den ManySortedSign

AA is strict non-empty finite-yielding gate`2=den Boolean MSAlgebra over A2

A9 is non empty non void V58() strict Circuit-like unsplit gate`1=arity gate`2isBoolean gate`2=den ManySortedSign

AA is non empty non void V58() strict Circuit-like unsplit gate`1=arity gate`2isBoolean gate`2=den ManySortedSign

s is strict non-empty finite-yielding gate`2=den Boolean MSAlgebra over AA

F

A2 is strict non-empty finite-yielding gate`2=den Boolean MSAlgebra over A9

F

AA is non empty non void V58() strict Circuit-like unsplit gate`1=arity gate`2isBoolean gate`2=den ManySortedSign

f . F

g . F

S is non empty V58() ManySortedSign

A is non-empty MSAlgebra over S

x is Relation-like NAT -defined Function-like total set

x . F

x . 0 is set

S9 is Relation-like NAT -defined Function-like total set

S9 . 0 is set

x is Relation-like NAT -defined Function-like total set

x . F

x . 0 is set

S9 is Relation-like NAT -defined Function-like total set

S9 . 0 is set

A2 is non empty V58() ManySortedSign

A9 is non pair V21() V22() V23() V27() V28() V121() ext-real non negative set

x . A9 is set

AA is set

S9 . A9 is set

A9 is non pair V21() V22() V23() V27() V28() V121() ext-real non negative set

S9 . A9 is