:: 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₁() is non empty V58() ManySortedSign
F₂() is set
[F₁(),F₂()] is non empty pair set
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₃(A,x,S) is non empty V58() ManySortedSign
F₄(x,S) is set
f . S is set
(f . S) `2 is set
(f . S) `1 is set
f . (S + 1) is set
F₃(A,(n . S),S) is non empty V58() ManySortedSign
F₄((n . S),S) is set
[F₃(A,(n . S),S),F₄((n . S),S)] is non empty pair set
(f . (S + 1)) `1 is set
(f . (S + 1)) `2 is set
F₃() is Relation-like NAT -defined Function-like total set
F₃() . 0 is set
F₄() is Relation-like NAT -defined Function-like total set
F₄() . 0 is set
f is non pair V21() V22() V23() V27() V28() V121() ext-real non negative set
F₃() . f is set
F₄() . f is set
f + 1 is non empty non pair V21() V22() V23() V27() V28() V121() ext-real non negative M3( REAL , NAT )
F₃() . (f + 1) is set
F₄() . (f + 1) is set
g is non empty V58() ManySortedSign
F₁(g,(F₄() . f),f) is non empty V58() ManySortedSign
F₂((F₄() . f),f) is set
f is non empty V58() ManySortedSign
g is set
F₄() is Relation-like NAT -defined Function-like total set
F₄() . 0 is set
F₁() is non empty V58() ManySortedSign
F₅() is Relation-like NAT -defined Function-like total set
F₅() . 0 is set
f is non pair V21() V22() V23() V27() V28() V121() ext-real non negative set
F₅() . f is set
f + 1 is non empty non pair V21() V22() V23() V27() V28() V121() ext-real non negative M3( REAL , NAT )
F₅() . (f + 1) is set
g is set
F₃(g,f) 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
F₅() . n 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
F₅() . n is set
n + 1 is non empty non pair V21() V22() V23() V27() V28() V121() ext-real non negative M3( REAL , NAT )
F₄() . (n + 1) is set
F₂(S,A,n) is non empty V58() ManySortedSign
F₅() . (n + 1) is set
F₃(A,n) is set
F₄() . f is set
n is non empty V58() ManySortedSign
F₅() is non pair V21() V22() V23() V27() V28() V121() ext-real non negative set
F₁() is non empty V58() ManySortedSign
F₂() is set
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₅() is set
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₃(A,x,S) is non empty V58() ManySortedSign
g . (S + 1) is set
F₄(x,S) is set
F₅() is non pair V21() V22() V23() V27() V28() V121() ext-real non negative set
F₁() is non empty V58() ManySortedSign
F₂() is set
f is non empty V58() ManySortedSign
g is non empty V58() ManySortedSign
n is Relation-like NAT -defined Function-like total set
n . F₅() is set
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₃(x,S9,A) is non empty V58() ManySortedSign
S . (A + 1) is set
F₄(S9,A) 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 is Relation-like NAT -defined Function-like total set
A . F₅() is set
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₃(A9,A2,S9) is non empty V58() ManySortedSign
x . (S9 + 1) is set
F₄(A2,S9) 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 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₄((S . S9),S9) is set
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₃(A9,(S . S9),S9) is non empty V58() ManySortedSign
A . (S9 + 1) is set
F₅() is non pair V21() V22() V23() V27() V28() V121() ext-real non negative set
F₁() is non empty V58() ManySortedSign
F₂() is set
F₁() is non empty V58() ManySortedSign
F₅() is non pair V21() V22() V23() V27() V28() V121() ext-real non negative set
F₃() is set
f is non empty V58() ManySortedSign
g is Relation-like NAT -defined Function-like total set
g . F₅() is 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
g . S is set
x is set
n . S is set
F₂(A,x,S) is non empty V58() ManySortedSign
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<sub>2</sub>(x,S9,A) is non empty V58() ManySortedSign
n . (A + 1) is set
F<sub>4</sub>(S9,A) is set
F<sub>1</sub>() is non empty V58() ManySortedSign
F<sub>5</sub>() is non pair V21() V22() V23() V27() V28() V121() ext-real non negative set
F<sub>3</sub>() is set
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₂(g,n) is non empty non void V58() Circuit-like unsplit gate`1=arity gate`2isBoolean gate`2=den ManySortedSign
f +* F<sub>2</sub>(g,n) is non empty non void V58() strict Circuit-like unsplit gate`1=arity gate`2isBoolean gate`2=den ManySortedSign
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<sub>2</sub>(A,x) is non empty non void V58() Circuit-like unsplit gate`1=arity gate`2isBoolean gate`2=den ManySortedSign
S +* F₂(A,x) is non empty non void V58() strict Circuit-like unsplit gate`1=arity gate`2isBoolean gate`2=den ManySortedSign
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₂(A9,A2) is non empty non void V58() Circuit-like unsplit gate`1=arity gate`2isBoolean gate`2=den ManySortedSign
S9 +* F<sub>2</sub>(A9,A2) 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 set
s3 is non pair V21() V22() V23() V27() V28() V121() ext-real non negative set
F<sub>2</sub>(s,s3) is non empty non void V58() Circuit-like unsplit gate`1=arity gate`2isBoolean gate`2=den ManySortedSign
AA +* F₂(s,s3) is non empty non void V58() strict Circuit-like unsplit gate`1=arity gate`2isBoolean gate`2=den ManySortedSign
s0 is non empty non void V58() strict Circuit-like unsplit gate`1=arity gate`2isBoolean gate`2=den ManySortedSign
s2 is set
c₁₅ is non pair V21() V22() V23() V27() V28() V121() ext-real non negative set
F₂(s2,c₁₅) is non empty non void V58() Circuit-like unsplit gate`1=arity gate`2isBoolean gate`2=den ManySortedSign
s0 +* F<sub>2</sub>(s2,c<sub>15</sub>) is non empty non void V58() strict Circuit-like unsplit gate`1=arity gate`2isBoolean gate`2=den ManySortedSign
c₁₆ is non empty non void V58() strict Circuit-like unsplit gate`1=arity gate`2isBoolean gate`2=den ManySortedSign
c<sub>17</sub> is set
c<sub>18</sub> is non pair V21() V22() V23() V27() V28() V121() ext-real non negative set
F<sub>2</sub>(c<sub>17</sub>,c<sub>18</sub>) is non empty non void V58() Circuit-like unsplit gate`1=arity gate`2isBoolean gate`2=den ManySortedSign
c₁₆ +* F₂(c₁₇,c₁₈) is non empty non void V58() strict Circuit-like unsplit gate`1=arity gate`2isBoolean gate`2=den ManySortedSign
F<sub>5</sub>() is non pair V21() V22() V23() V27() V28() V121() ext-real non negative set
F<sub>1</sub>() is non empty V58() ManySortedSign
F<sub>2</sub>() is set
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₅() is set
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<sub>5</sub>() is set
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<sub>1</sub>() is non empty non void V58() Circuit-like unsplit gate`1=arity gate`2isBoolean gate`2=den ManySortedSign
InnerVertices 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 non empty 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₁()))
InputVertices 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₁()))
F₂(0) is set
F₃() is Relation-like NAT -defined Function-like total set
F₃() . 0 is set
F₄((F₃() . 0),0) is non empty non void V58() Circuit-like unsplit gate`1=arity gate`2isBoolean gate`2=den ManySortedSign
InnerVertices F<sub>4</sub>((F<sub>3</sub>() . 0),0) is M2(K19( the carrier of F<sub>4</sub>((F<sub>3</sub>() . 0),0)))
the carrier of F<sub>4</sub>((F<sub>3</sub>() . 0),0) is non empty set
K19( the carrier of F<sub>4</sub>((F<sub>3</sub>() . 0),0)) is set
the ResultSort of F<sub>4</sub>((F<sub>3</sub>() . 0),0) is Relation-like Function-like V18( the carrier' of F<sub>4</sub>((F<sub>3</sub>() . 0),0), the carrier of F<sub>4</sub>((F<sub>3</sub>() . 0),0)) M2(K19(K20( the carrier' of F<sub>4</sub>((F<sub>3</sub>() . 0),0), the carrier of F<sub>4</sub>((F<sub>3</sub>() . 0),0))))
the carrier' of F<sub>4</sub>((F<sub>3</sub>() . 0),0) is non empty set
K20( the carrier' of F<sub>4</sub>((F<sub>3</sub>() . 0),0), the carrier of F<sub>4</sub>((F<sub>3</sub>() . 0),0)) is Relation-like set
K19(K20( the carrier' of F<sub>4</sub>((F<sub>3</sub>() . 0),0), the carrier of F<sub>4</sub>((F<sub>3</sub>() . 0),0))) is set
K422( the carrier of F<sub>4</sub>((F<sub>3</sub>() . 0),0), the ResultSort of F<sub>4</sub>((F<sub>3</sub>() . 0),0)) is M2(K19( the carrier of F<sub>4</sub>((F<sub>3</sub>() . 0),0)))
f is non pair V21() V22() V23() V27() V28() V121() ext-real non negative set
F<sub>2</sub>(f) is set
f + 1 is non empty non pair V21() V22() V23() V27() V28() V121() ext-real non negative M3( REAL , NAT )
F<sub>2</sub>((f + 1)) is set
F<sub>3</sub>() . f is set
F<sub>4</sub>((F<sub>3</sub>() . f),f) is non empty non void V58() Circuit-like unsplit gate`1=arity gate`2isBoolean gate`2=den ManySortedSign
InputVertices F₄((F₃() . f),f) is M2(K19( the carrier of F₄((F₃() . f),f)))
the carrier of F₄((F₃() . f),f) is non empty set
K19( the carrier of F₄((F₃() . f),f)) is set
the ResultSort of F₄((F₃() . f),f) is Relation-like Function-like V18( the carrier' of F₄((F₃() . f),f), the carrier of F₄((F₃() . f),f)) M2(K19(K20( the carrier' of F₄((F₃() . f),f), the carrier of F₄((F₃() . f),f))))
the carrier' of F₄((F₃() . f),f) is non empty set
K20( the carrier' of F₄((F₃() . f),f), the carrier of F₄((F₃() . f),f)) is Relation-like set
K19(K20( the carrier' of F₄((F₃() . f),f), the carrier of F₄((F₃() . f),f))) is set
K422( the carrier of F₄((F₃() . f),f), the ResultSort of F₄((F₃() . f),f)) is M2(K19( the carrier of F₄((F₃() . f),f)))
K28( the carrier of F₄((F₃() . f),f),K422( the carrier of F₄((F₃() . f),f), the ResultSort of F₄((F₃() . f),f))) is M2(K19( the carrier of F₄((F₃() . f),f)))
{(F₃() . f)} is set
(InputVertices F₄((F₃() . f),f)) \ {(F₃() . f)} is set
F₃() . (f + 1) is set
(f + 1) + 1 is non empty non pair V21() V22() V23() V27() V28() V121() ext-real non negative M3( REAL , NAT )
F₂(((f + 1) + 1)) is set
F₄((F₃() . (f + 1)),(f + 1)) is non empty non void V58() Circuit-like unsplit gate`1=arity gate`2isBoolean gate`2=den ManySortedSign
InputVertices F<sub>4</sub>((F<sub>3</sub>() . (f + 1)),(f + 1)) is M2(K19( the carrier of F<sub>4</sub>((F<sub>3</sub>() . (f + 1)),(f + 1))))
the carrier of F<sub>4</sub>((F<sub>3</sub>() . (f + 1)),(f + 1)) is non empty set
K19( the carrier of F<sub>4</sub>((F<sub>3</sub>() . (f + 1)),(f + 1))) is set
the ResultSort of F<sub>4</sub>((F<sub>3</sub>() . (f + 1)),(f + 1)) is Relation-like Function-like V18( the carrier' of F<sub>4</sub>((F<sub>3</sub>() . (f + 1)),(f + 1)), the carrier of F<sub>4</sub>((F<sub>3</sub>() . (f + 1)),(f + 1))) M2(K19(K20( the carrier' of F<sub>4</sub>((F<sub>3</sub>() . (f + 1)),(f + 1)), the carrier of F<sub>4</sub>((F<sub>3</sub>() . (f + 1)),(f + 1)))))
the carrier' of F<sub>4</sub>((F<sub>3</sub>() . (f + 1)),(f + 1)) is non empty set
K20( the carrier' of F<sub>4</sub>((F<sub>3</sub>() . (f + 1)),(f + 1)), the carrier of F<sub>4</sub>((F<sub>3</sub>() . (f + 1)),(f + 1))) is Relation-like set
K19(K20( the carrier' of F<sub>4</sub>((F<sub>3</sub>() . (f + 1)),(f + 1)), the carrier of F<sub>4</sub>((F<sub>3</sub>() . (f + 1)),(f + 1)))) is set
K422( the carrier of F<sub>4</sub>((F<sub>3</sub>() . (f + 1)),(f + 1)), the ResultSort of F<sub>4</sub>((F<sub>3</sub>() . (f + 1)),(f + 1))) is M2(K19( the carrier of F<sub>4</sub>((F<sub>3</sub>() . (f + 1)),(f + 1))))
K28( the carrier of F<sub>4</sub>((F<sub>3</sub>() . (f + 1)),(f + 1)),K422( the carrier of F<sub>4</sub>((F<sub>3</sub>() . (f + 1)),(f + 1)), the ResultSort of F<sub>4</sub>((F<sub>3</sub>() . (f + 1)),(f + 1)))) is M2(K19( the carrier of F<sub>4</sub>((F<sub>3</sub>() . (f + 1)),(f + 1))))
{(F<sub>3</sub>() . (f + 1))} is set
(InputVertices F<sub>4</sub>((F<sub>3</sub>() . (f + 1)),(f + 1))) \ {(F<sub>3</sub>() . (f + 1))} is set
F<sub>3</sub>() . ((f + 1) + 1) is set
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<sub>4</sub>((F<sub>3</sub>() . f),f)) \ {(F<sub>3</sub>() . f)}) is set
InnerVertices n is M2(K19( the carrier of n))
(InputVertices n) \/ ((InputVertices F<sub>4</sub>((F<sub>3</sub>() . (f + 1)),(f + 1))) \ {(F<sub>3</sub>() . (f + 1))}) is set
n +* F<sub>4</sub>((F<sub>3</sub>() . (f + 1)),(f + 1)) is non empty non void V58() strict Circuit-like unsplit gate`1=arity gate`2isBoolean gate`2=den ManySortedSign
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<sub>2</sub>(((f + 1) + 1)) is set
InnerVertices F<sub>4</sub>((F<sub>3</sub>() . (f + 1)),(f + 1)) is M2(K19( the carrier of F<sub>4</sub>((F<sub>3</sub>() . (f + 1)),(f + 1))))
(InputVertices n) \ (InnerVertices F<sub>4</sub>((F<sub>3</sub>() . (f + 1)),(f + 1))) is set
(InputVertices F<sub>4</sub>((F<sub>3</sub>() . (f + 1)),(f + 1))) \ (InnerVertices n) is set
((InputVertices n) \ (InnerVertices F<sub>4</sub>((F<sub>3</sub>() . (f + 1)),(f + 1)))) \/ ((InputVertices F<sub>4</sub>((F<sub>3</sub>() . (f + 1)),(f + 1))) \ (InnerVertices n)) is set
(InputVertices n) \/ ((InputVertices F<sub>4</sub>((F<sub>3</sub>() . (f + 1)),(f + 1))) \ (InnerVertices n)) is set
A is non with_pair set
x is non with_pair set
A \/ x is non with_pair set
F<sub>3</sub>() . ((f + 1) + 1) is set
F<sub>5</sub>((F<sub>3</sub>() . (f + 1)),(f + 1)) is set
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<sub>2</sub>(f) is set
f + 1 is non empty non pair V21() V22() V23() V27() V28() V121() ext-real non negative M3( REAL , NAT )
F<sub>2</sub>((f + 1)) is set
F<sub>3</sub>() . f is set
F<sub>4</sub>((F<sub>3</sub>() . f),f) is non empty non void V58() Circuit-like unsplit gate`1=arity gate`2isBoolean gate`2=den ManySortedSign
InputVertices F₄((F₃() . f),f) is M2(K19( the carrier of F₄((F₃() . f),f)))
the carrier of F₄((F₃() . f),f) is non empty set
K19( the carrier of F₄((F₃() . f),f)) is set
the ResultSort of F₄((F₃() . f),f) is Relation-like Function-like V18( the carrier' of F₄((F₃() . f),f), the carrier of F₄((F₃() . f),f)) M2(K19(K20( the carrier' of F₄((F₃() . f),f), the carrier of F₄((F₃() . f),f))))
the carrier' of F₄((F₃() . f),f) is non empty set
K20( the carrier' of F₄((F₃() . f),f), the carrier of F₄((F₃() . f),f)) is Relation-like set
K19(K20( the carrier' of F₄((F₃() . f),f), the carrier of F₄((F₃() . f),f))) is set
K422( the carrier of F₄((F₃() . f),f), the ResultSort of F₄((F₃() . f),f)) is M2(K19( the carrier of F₄((F₃() . f),f)))
K28( the carrier of F₄((F₃() . f),f),K422( the carrier of F₄((F₃() . f),f), the ResultSort of F₄((F₃() . f),f))) is M2(K19( the carrier of F₄((F₃() . f),f)))
{(F₃() . f)} is set
(InputVertices F₄((F₃() . f),f)) \ {(F₃() . f)} is set
F₁() +* F₄((F₃() . 0),0) is non empty non void V58() strict Circuit-like unsplit gate`1=arity gate`2isBoolean gate`2=den ManySortedSign
InputVertices (F<sub>1</sub>() +* F<sub>4</sub>((F<sub>3</sub>() . 0),0)) is M2(K19( the carrier of (F<sub>1</sub>() +* F<sub>4</sub>((F<sub>3</sub>() . 0),0))))
the carrier of (F<sub>1</sub>() +* F<sub>4</sub>((F<sub>3</sub>() . 0),0)) is non empty set
K19( the carrier of (F<sub>1</sub>() +* F<sub>4</sub>((F<sub>3</sub>() . 0),0))) is set
the ResultSort of (F<sub>1</sub>() +* F<sub>4</sub>((F<sub>3</sub>() . 0),0)) is Relation-like Function-like V18( the carrier' of (F<sub>1</sub>() +* F<sub>4</sub>((F<sub>3</sub>() . 0),0)), the carrier of (F<sub>1</sub>() +* F<sub>4</sub>((F<sub>3</sub>() . 0),0))) M2(K19(K20( the carrier' of (F<sub>1</sub>() +* F<sub>4</sub>((F<sub>3</sub>() . 0),0)), the carrier of (F<sub>1</sub>() +* F<sub>4</sub>((F<sub>3</sub>() . 0),0)))))
the carrier' of (F<sub>1</sub>() +* F<sub>4</sub>((F<sub>3</sub>() . 0),0)) is non empty set
K20( the carrier' of (F<sub>1</sub>() +* F<sub>4</sub>((F<sub>3</sub>() . 0),0)), the carrier of (F<sub>1</sub>() +* F<sub>4</sub>((F<sub>3</sub>() . 0),0))) is Relation-like set
K19(K20( the carrier' of (F<sub>1</sub>() +* F<sub>4</sub>((F<sub>3</sub>() . 0),0)), the carrier of (F<sub>1</sub>() +* F<sub>4</sub>((F<sub>3</sub>() . 0),0)))) is set
K422( the carrier of (F<sub>1</sub>() +* F<sub>4</sub>((F<sub>3</sub>() . 0),0)), the ResultSort of (F<sub>1</sub>() +* F<sub>4</sub>((F<sub>3</sub>() . 0),0))) is M2(K19( the carrier of (F<sub>1</sub>() +* F<sub>4</sub>((F<sub>3</sub>() . 0),0))))
K28( the carrier of (F<sub>1</sub>() +* F<sub>4</sub>((F<sub>3</sub>() . 0),0)),K422( the carrier of (F<sub>1</sub>() +* F<sub>4</sub>((F<sub>3</sub>() . 0),0)), the ResultSort of (F<sub>1</sub>() +* F<sub>4</sub>((F<sub>3</sub>() . 0),0)))) is M2(K19( the carrier of (F<sub>1</sub>() +* F<sub>4</sub>((F<sub>3</sub>() . 0),0))))
(InputVertices F<sub>1</sub>()) \ (InnerVertices F<sub>4</sub>((F<sub>3</sub>() . 0),0)) is set
InputVertices F<sub>4</sub>((F<sub>3</sub>() . 0),0) is M2(K19( the carrier of F<sub>4</sub>((F<sub>3</sub>() . 0),0)))
K28( the carrier of F<sub>4</sub>((F<sub>3</sub>() . 0),0),K422( the carrier of F<sub>4</sub>((F<sub>3</sub>() . 0),0), the ResultSort of F<sub>4</sub>((F<sub>3</sub>() . 0),0))) is M2(K19( the carrier of F<sub>4</sub>((F<sub>3</sub>() . 0),0)))
(InputVertices F<sub>4</sub>((F<sub>3</sub>() . 0),0)) \ (InnerVertices F<sub>1</sub>()) is set
((InputVertices F<sub>1</sub>()) \ (InnerVertices F<sub>4</sub>((F<sub>3</sub>() . 0),0))) \/ ((InputVertices F<sub>4</sub>((F<sub>3</sub>() . 0),0)) \ (InnerVertices F<sub>1</sub>())) is set
(InputVertices F<sub>1</sub>()) \/ ((InputVertices F<sub>4</sub>((F<sub>3</sub>() . 0),0)) \ (InnerVertices F<sub>1</sub>())) is set
0 + 1 is non empty non pair V21() V22() V23() V27() V28() V121() ext-real non negative M3( REAL , NAT )
F<sub>2</sub>((0 + 1)) is set
{(F<sub>3</sub>() . 0)} is set
(InputVertices F<sub>4</sub>((F<sub>3</sub>() . 0),0)) \ {(F<sub>3</sub>() . 0)} is set
F<sub>3</sub>() . (0 + 1) is set
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₄((F₃() . 0),0)) \ {(F₃() . 0)}) is set
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<sub>2</sub>((0 + 1)) is set
A9 is set
n is non with_pair set
g is non with_pair set
n \/ g is non with_pair set
F<sub>3</sub>() . (0 + 1) is set
F<sub>5</sub>((F<sub>3</sub>() . 0),0) is set
S9 is Relation-like set
x is Relation-like set
x \/ S9 is Relation-like set
F<sub>3</sub>() . (f + 1) is set
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<sub>4</sub>((F<sub>3</sub>() . f),f)) \ {(F<sub>3</sub>() . f)}) is set
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<sub>2</sub>(A) is set
A + 1 is non empty non pair V21() V22() V23() V27() V28() V121() ext-real non negative M3( REAL , NAT )
F<sub>2</sub>((A + 1)) is set
F<sub>3</sub>() . A is set
F<sub>4</sub>((F<sub>3</sub>() . A),A) is non empty non void V58() Circuit-like unsplit gate`1=arity gate`2isBoolean gate`2=den ManySortedSign
InputVertices F₄((F₃() . A),A) is M2(K19( the carrier of F₄((F₃() . A),A)))
the carrier of F₄((F₃() . A),A) is non empty set
K19( the carrier of F₄((F₃() . A),A)) is set
the ResultSort of F₄((F₃() . A),A) is Relation-like Function-like V18( the carrier' of F₄((F₃() . A),A), the carrier of F₄((F₃() . A),A)) M2(K19(K20( the carrier' of F₄((F₃() . A),A), the carrier of F₄((F₃() . A),A))))
the carrier' of F₄((F₃() . A),A) is non empty set
K20( the carrier' of F₄((F₃() . A),A), the carrier of F₄((F₃() . A),A)) is Relation-like set
K19(K20( the carrier' of F₄((F₃() . A),A), the carrier of F₄((F₃() . A),A))) is set
K422( the carrier of F₄((F₃() . A),A), the ResultSort of F₄((F₃() . A),A)) is M2(K19( the carrier of F₄((F₃() . A),A)))
K28( the carrier of F₄((F₃() . A),A),K422( the carrier of F₄((F₃() . A),A), the ResultSort of F₄((F₃() . A),A))) is M2(K19( the carrier of F₄((F₃() . A),A)))
{(F₃() . A)} is set
(InputVertices F₄((F₃() . A),A)) \ {(F₃() . A)} is set
F₃() . (A + 1) is set
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₄((F₃() . A),A)) \ {(F₃() . A)}) is set
InnerVertices S9 is M2(K19( the carrier of S9))
F₁(0) is non empty non void V58() Circuit-like unsplit gate`1=arity gate`2isBoolean gate`2=den ManySortedSign
InnerVertices F<sub>1</sub>(0) is M2(K19( the carrier of F<sub>1</sub>(0)))
the carrier of F<sub>1</sub>(0) is non empty set
K19( the carrier of F<sub>1</sub>(0)) is set
the ResultSort of F<sub>1</sub>(0) is Relation-like Function-like V18( the carrier' of F<sub>1</sub>(0), the carrier of F<sub>1</sub>(0)) M2(K19(K20( the carrier' of F<sub>1</sub>(0), the carrier of F<sub>1</sub>(0))))
the carrier' of F<sub>1</sub>(0) is non empty set
K20( the carrier' of F<sub>1</sub>(0), the carrier of F<sub>1</sub>(0)) is Relation-like set
K19(K20( the carrier' of F<sub>1</sub>(0), the carrier of F<sub>1</sub>(0))) is set
K422( the carrier of F<sub>1</sub>(0), the ResultSort of F<sub>1</sub>(0)) is M2(K19( the carrier of F<sub>1</sub>(0)))
InputVertices F<sub>1</sub>(0) is M2(K19( the carrier of F<sub>1</sub>(0)))
K28( the carrier of F<sub>1</sub>(0),K422( the carrier of F<sub>1</sub>(0), the ResultSort of F<sub>1</sub>(0))) is M2(K19( the carrier of F<sub>1</sub>(0)))
F<sub>2</sub>() is Relation-like NAT -defined Function-like total set
F<sub>2</sub>() . 0 is set
g is non empty V58() ManySortedSign
f is non pair V21() V22() V23() V27() V28() V121() ext-real non negative set
F<sub>1</sub>(f) is non empty non void V58() Circuit-like unsplit gate`1=arity gate`2isBoolean gate`2=den ManySortedSign
n is set
F₂() . f is set
f + 1 is non empty non pair V21() V22() V23() V27() V28() V121() ext-real non negative M3( REAL , NAT )
F₁((f + 1)) is non empty non void V58() Circuit-like unsplit gate`1=arity gate`2isBoolean gate`2=den ManySortedSign
F<sub>3</sub>(n,f) is non empty non void V58() Circuit-like unsplit gate`1=arity gate`2isBoolean gate`2=den ManySortedSign
g +* F₃(n,f) is non empty non void V58() strict ManySortedSign
F₂() . (f + 1) is set
F₄(n,f) is set
InputVertices F₃(n,f) is M2(K19( the carrier of F₃(n,f)))
the carrier of F₃(n,f) is non empty set
K19( the carrier of F₃(n,f)) is set
the ResultSort of F₃(n,f) is Relation-like Function-like V18( the carrier' of F₃(n,f), the carrier of F₃(n,f)) M2(K19(K20( the carrier' of F₃(n,f), the carrier of F₃(n,f))))
the carrier' of F₃(n,f) is non empty set
K20( the carrier' of F₃(n,f), the carrier of F₃(n,f)) is Relation-like set
K19(K20( the carrier' of F₃(n,f), the carrier of F₃(n,f))) is set
K422( the carrier of F₃(n,f), the ResultSort of F₃(n,f)) is M2(K19( the carrier of F₃(n,f)))
K28( the carrier of F₃(n,f),K422( the carrier of F₃(n,f), the ResultSort of F₃(n,f))) is M2(K19( the carrier of F₃(n,f)))
InnerVertices F₃(n,f) is M2(K19( the carrier of F₃(n,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₁((f + 1)) is non empty non void V58() Circuit-like unsplit gate`1=arity gate`2isBoolean gate`2=den ManySortedSign
InputVertices F<sub>1</sub>((f + 1)) is M2(K19( the carrier of F<sub>1</sub>((f + 1))))
the carrier of F<sub>1</sub>((f + 1)) is non empty set
K19( the carrier of F<sub>1</sub>((f + 1))) is set
the ResultSort of F<sub>1</sub>((f + 1)) is Relation-like Function-like V18( the carrier' of F<sub>1</sub>((f + 1)), the carrier of F<sub>1</sub>((f + 1))) M2(K19(K20( the carrier' of F<sub>1</sub>((f + 1)), the carrier of F<sub>1</sub>((f + 1)))))
the carrier' of F<sub>1</sub>((f + 1)) is non empty set
K20( the carrier' of F<sub>1</sub>((f + 1)), the carrier of F<sub>1</sub>((f + 1))) is Relation-like set
K19(K20( the carrier' of F<sub>1</sub>((f + 1)), the carrier of F<sub>1</sub>((f + 1)))) is set
K422( the carrier of F<sub>1</sub>((f + 1)), the ResultSort of F<sub>1</sub>((f + 1))) is M2(K19( the carrier of F<sub>1</sub>((f + 1))))
K28( the carrier of F<sub>1</sub>((f + 1)),K422( the carrier of F<sub>1</sub>((f + 1)), the ResultSort of F<sub>1</sub>((f + 1)))) is M2(K19( the carrier of F<sub>1</sub>((f + 1))))
F<sub>1</sub>(f) is non empty non void V58() Circuit-like unsplit gate`1=arity gate`2isBoolean gate`2=den ManySortedSign
InputVertices F₁(f) is M2(K19( the carrier of F₁(f)))
the carrier of F₁(f) is non empty set
K19( the carrier of F₁(f)) is set
the ResultSort of F₁(f) is Relation-like Function-like V18( the carrier' of F₁(f), the carrier of F₁(f)) M2(K19(K20( the carrier' of F₁(f), the carrier of F₁(f))))
the carrier' of F₁(f) is non empty set
K20( the carrier' of F₁(f), the carrier of F₁(f)) is Relation-like set
K19(K20( the carrier' of F₁(f), the carrier of F₁(f))) is set
K422( the carrier of F₁(f), the ResultSort of F₁(f)) is M2(K19( the carrier of F₁(f)))
K28( the carrier of F₁(f),K422( the carrier of F₁(f), the ResultSort of F₁(f))) is M2(K19( the carrier of F₁(f)))
F₂() . f is set
F₃((F₂() . f),f) is non empty non void V58() Circuit-like unsplit gate`1=arity gate`2isBoolean gate`2=den ManySortedSign
InputVertices F<sub>3</sub>((F<sub>2</sub>() . f),f) is M2(K19( the carrier of F<sub>3</sub>((F<sub>2</sub>() . f),f)))
the carrier of F<sub>3</sub>((F<sub>2</sub>() . f),f) is non empty set
K19( the carrier of F<sub>3</sub>((F<sub>2</sub>() . f),f)) is set
the ResultSort of F<sub>3</sub>((F<sub>2</sub>() . f),f) is Relation-like Function-like V18( the carrier' of F<sub>3</sub>((F<sub>2</sub>() . f),f), the carrier of F<sub>3</sub>((F<sub>2</sub>() . f),f)) M2(K19(K20( the carrier' of F<sub>3</sub>((F<sub>2</sub>() . f),f), the carrier of F<sub>3</sub>((F<sub>2</sub>() . f),f))))
the carrier' of F<sub>3</sub>((F<sub>2</sub>() . f),f) is non empty set
K20( the carrier' of F<sub>3</sub>((F<sub>2</sub>() . f),f), the carrier of F<sub>3</sub>((F<sub>2</sub>() . f),f)) is Relation-like set
K19(K20( the carrier' of F<sub>3</sub>((F<sub>2</sub>() . f),f), the carrier of F<sub>3</sub>((F<sub>2</sub>() . f),f))) is set
K422( the carrier of F<sub>3</sub>((F<sub>2</sub>() . f),f), the ResultSort of F<sub>3</sub>((F<sub>2</sub>() . f),f)) is M2(K19( the carrier of F<sub>3</sub>((F<sub>2</sub>() . f),f)))
K28( the carrier of F<sub>3</sub>((F<sub>2</sub>() . f),f),K422( the carrier of F<sub>3</sub>((F<sub>2</sub>() . f),f), the ResultSort of F<sub>3</sub>((F<sub>2</sub>() . f),f))) is M2(K19( the carrier of F<sub>3</sub>((F<sub>2</sub>() . f),f)))
{(F<sub>2</sub>() . f)} is set
(InputVertices F<sub>3</sub>((F<sub>2</sub>() . f),f)) \ {(F<sub>2</sub>() . f)} is set
(InputVertices F<sub>1</sub>(f)) \/ ((InputVertices F<sub>3</sub>((F<sub>2</sub>() . f),f)) \ {(F<sub>2</sub>() . f)}) is set
InnerVertices F<sub>1</sub>(f) is M2(K19( the carrier of F<sub>1</sub>(f)))
n is set
g is non pair V21() V22() V23() V27() V28() V121() ext-real non negative set
F<sub>2</sub>() . g is set
F<sub>3</sub>(n,g) is non empty non void V58() Circuit-like unsplit gate`1=arity gate`2isBoolean gate`2=den ManySortedSign
InputVertices F₃(n,g) is M2(K19( the carrier of F₃(n,g)))
the carrier of F₃(n,g) is non empty set
K19( the carrier of F₃(n,g)) is set
the ResultSort of F₃(n,g) is Relation-like Function-like V18( the carrier' of F₃(n,g), the carrier of F₃(n,g)) M2(K19(K20( the carrier' of F₃(n,g), the carrier of F₃(n,g))))
the carrier' of F₃(n,g) is non empty set
K20( the carrier' of F₃(n,g), the carrier of F₃(n,g)) is Relation-like set
K19(K20( the carrier' of F₃(n,g), the carrier of F₃(n,g))) is set
K422( the carrier of F₃(n,g), the ResultSort of F₃(n,g)) is M2(K19( the carrier of F₃(n,g)))
K28( the carrier of F₃(n,g),K422( the carrier of F₃(n,g), the ResultSort of F₃(n,g))) is M2(K19( the carrier of F₃(n,g)))
{n} is set
(InputVertices F₃(n,g)) \ {n} is set
InnerVertices H₁( 0 ) is M2(K19( the carrier of H₁( 0 )))
the carrier of H₁( 0 ) is non empty set
K19( the carrier of H₁( 0 )) is set
n is set
g is non pair V21() V22() V23() V27() V28() V121() ext-real non negative set
F₃(n,g) is non empty non void V58() Circuit-like unsplit gate`1=arity gate`2isBoolean gate`2=den ManySortedSign
InnerVertices F<sub>3</sub>(n,g) is M2(K19( the carrier of F<sub>3</sub>(n,g)))
the carrier of F<sub>3</sub>(n,g) is non empty set
K19( the carrier of F<sub>3</sub>(n,g)) is set
the ResultSort of F<sub>3</sub>(n,g) is Relation-like Function-like V18( the carrier' of F<sub>3</sub>(n,g), the carrier of F<sub>3</sub>(n,g)) M2(K19(K20( the carrier' of F<sub>3</sub>(n,g), the carrier of F<sub>3</sub>(n,g))))
the carrier' of F<sub>3</sub>(n,g) is non empty set
K20( the carrier' of F<sub>3</sub>(n,g), the carrier of F<sub>3</sub>(n,g)) is Relation-like set
K19(K20( the carrier' of F<sub>3</sub>(n,g), the carrier of F<sub>3</sub>(n,g))) is set
K422( the carrier of F<sub>3</sub>(n,g), the ResultSort of F<sub>3</sub>(n,g)) is M2(K19( the carrier of F<sub>3</sub>(n,g)))
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<sub>3</sub>((F<sub>2</sub>() . f),f)) \ {(F<sub>2</sub>() . f)}) is set
InnerVertices g is M2(K19( the carrier of g))
F<sub>1</sub>() is non empty V58() ManySortedSign
F<sub>2</sub>() is non-empty MSAlgebra over F<sub>1</sub>()
F<sub>3</sub>() is set
[F<sub>1</sub>(),F<sub>2</sub>()] is non empty pair set
[[F<sub>1</sub>(),F<sub>2</sub>()],F<sub>3</sub>()] is non empty pair set
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₄(x,A9,A) is non empty V58() ManySortedSign
F₅(x,S9,A9,A) is set
F₆(A9,A) is set
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<sub>4</sub>(x,(n . A),A) is non empty V58() ManySortedSign
F<sub>5</sub>(x,S9,(n . A),A) is set
[F<sub>4</sub>(x,(n . A),A),F<sub>5</sub>(x,S9,(n . A),A)] is non empty pair set
F<sub>6</sub>((n . A),A) is set
[[F<sub>4</sub>(x,(n . A),A),F<sub>5</sub>(x,S9,(n . A),A)],F<sub>6</sub>((n . A),A)] is non empty pair set
(f . (A + 1)) `2 is set
(f . (A + 1)) `11 is set
(f . (A + 1)) `12 is set
F₄() is Relation-like NAT -defined Function-like total set
F₄() . 0 is set
F₅() is Relation-like NAT -defined Function-like total set
F₅() . 0 is set
F₆() is Relation-like NAT -defined Function-like total set
F₆() . 0 is set
f is non pair V21() V22() V23() V27() V28() V121() ext-real non negative set
F₄() . f is set
F₅() . f is set
F₆() . f is set
f + 1 is non empty non pair V21() V22() V23() V27() V28() V121() ext-real non negative M3( REAL , NAT )
F₄() . (f + 1) is set
F₅() . (f + 1) is set
F₆() . (f + 1) is set
g is non empty V58() ManySortedSign
n is non-empty MSAlgebra over g
S is set
F₁(g,S,f) is non empty V58() ManySortedSign
A is non empty V58() ManySortedSign
F₂(g,n,S,f) is set
x is non-empty MSAlgebra over A
S9 is set
F₃(S,f) is set
f is non pair V21() V22() V23() V27() V28() V121() ext-real non negative set
F₄() . f is set
F₅() . f is set
F₆() . f is set
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₄() is Relation-like NAT -defined Function-like total set
F₄() . 0 is set
F₆() is Relation-like NAT -defined Function-like total set
F₆() . 0 is set
F₅() is Relation-like NAT -defined Function-like total set
F₅() . 0 is set
F₇() is Relation-like NAT -defined Function-like total set
F₇() . 0 is set
F₈() is Relation-like NAT -defined Function-like total set
F₈() . 0 is set
F₉() is Relation-like NAT -defined Function-like total set
F₉() . 0 is set
g is non empty V58() ManySortedSign
f is non pair V21() V22() V23() V27() V28() V121() ext-real non negative set
F₄() . f is set
n is non-empty MSAlgebra over g
F₆() . f is set
S is set
F₈() . f is set
f + 1 is non empty non pair V21() V22() V23() V27() V28() V121() ext-real non negative M3( REAL , NAT )
F₄() . (f + 1) is set
F₁(g,S,f) is non empty V58() ManySortedSign
F₆() . (f + 1) is set
F₂(g,n,S,f) is set
F₈() . (f + 1) is set
F₃(S,f) 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
F₆() . S is set
S9 is set
F₈() . S is set
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₂(S,A,x,S9) is set
F₁(S,x,S9) is non empty V58() ManySortedSign
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₅() . S9 is set
A2 is non-empty MSAlgebra over A9
F₇() . S9 is set
AA is set
F₉() . S9 is set
A9 is non empty V58() ManySortedSign
S9 is non pair V21() V22() V23() V27() V28() V121() ext-real non negative set
F₅() . S9 is set
A2 is non-empty MSAlgebra over A9
F₇() . S9 is set
AA is set
F₉() . S9 is set
S9 + 1 is non empty non pair V21() V22() V23() V27() V28() V121() ext-real non negative M3( REAL , NAT )
F₅() . (S9 + 1) is set
F₁(A9,AA,S9) is non empty V58() ManySortedSign
F₇() . (S9 + 1) is set
F₂(A9,A2,AA,S9) is set
F₉() . (S9 + 1) is set
F₃(AA,S9) is set
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₈() . S9 is set
F₉() . S9 is set
F₄() . S9 is set
F₆() . S9 is set
S9 + 1 is non empty non pair V21() V22() V23() V27() V28() V121() ext-real non negative M3( REAL , NAT )
F₈() . (S9 + 1) is set
F₃((F₈() . S9),S9) is set
A9 is non empty V58() ManySortedSign
A2 is non-empty MSAlgebra over A9
F₅() . S9 is set
F₇() . S9 is set
F₉() . (S9 + 1) is set
A9 is non empty V58() ManySortedSign
A2 is non-empty MSAlgebra over A9
S9 is set
F₈() . S9 is set
F₉() . S9 is set
S9 is non pair V21() V22() V23() V27() V28() V121() ext-real non negative set
F₄() . S9 is set
F₅() . S9 is set
F₆() . S9 is set
F₇() . S9 is set
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₆() . (S9 + 1) is set
F₈() . S9 is set
F₂(A9,A2,(F₈() . S9),S9) is set
F₇() . (S9 + 1) is set
F₄() . (S9 + 1) is set
F₁(A9,(F₈() . S9),S9) is non empty V58() ManySortedSign
F₅() . (S9 + 1) is set
S9 is set
F₄() . S9 is set
F₅() . S9 is set
A9 is set
F₆() . A9 is set
F₇() . A9 is set
F₁() is non empty V58() ManySortedSign
F₆() is Relation-like NAT -defined Function-like total set
F₆() . 0 is set
F₇() is Relation-like NAT -defined Function-like total set
F₇() . 0 is set
F₂() is non-empty MSAlgebra over F₁()
F₈() is Relation-like NAT -defined Function-like total set
F₈() . 0 is set
f is non pair V21() V22() V23() V27() V28() V121() ext-real non negative set
F₆() . f is set
F₈() . f is set
f + 1 is non empty non pair V21() V22() V23() V27() V28() V121() ext-real non negative M3( REAL , NAT )
F₆() . (f + 1) is set
F₈() . (f + 1) is set
g is non empty V58() ManySortedSign
n is set
F₃(g,n,f) is non empty V58() ManySortedSign
F₅(n,f) 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
F₇() . S is set
S9 is set
F₈() . S is set
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₄(S,A,x,S9) is set
F₃(S,x,S9) 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 non-empty MSAlgebra over A
F₇() . S is set
S9 is set
F₈() . 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₃(A,S9,S) is non empty V58() ManySortedSign
F₇() . (S + 1) is set
F₄(A,x,S9,S) is set
F₈() . (S + 1) is set
F₅(S9,S) is set
F₇() . f is set
S is non empty V58() ManySortedSign
A is non-empty MSAlgebra over S
F₁() is non empty V58() ManySortedSign
F₇() is non pair V21() V22() V23() V27() V28() V121() ext-real non negative set
F₂() is non-empty MSAlgebra over F₁()
F₃() is set
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,g,n,S) is set
F₄(f,n,S) is non empty V58() ManySortedSign
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₇() is set
g . F₇() is set
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₄(S9,A2,x) is non empty V58() ManySortedSign
g . (x + 1) is set
F₅(S9,A9,A2,x) is set
n . (x + 1) is set
F₆(A2,x) is set
F₁() is non empty V58() ManySortedSign
F₂() is non empty V58() ManySortedSign
F₈() is non pair V21() V22() V23() V27() V28() V121() ext-real non negative set
F₄() is set
F₃() is non-empty MSAlgebra over 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,g,n,S) is set
F₅(f,n,S) is non empty V58() ManySortedSign
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₈() is set
g . F₈() is set
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₈() is set
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₈() is set
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₇((S9 . A9),A9) is set
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₅(A2,(S9 . A9),A9) is non empty V58() ManySortedSign
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₅(AA,s3,A2) is non empty V58() ManySortedSign
g . (A2 + 1) is set
F₆(AA,s,s3,A2) is set
n . (A2 + 1) is set
F₇(s3,A2) is set
F₁() is non empty V58() ManySortedSign
F₂() is non empty V58() ManySortedSign
F₈() is non pair V21() V22() V23() V27() V28() V121() ext-real non negative set
F₃() is non-empty MSAlgebra over F₁()
F₄() is set
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,g,n,S) is set
F₅(f,n,S) is non empty V58() ManySortedSign
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₈() is set
S is Relation-like NAT -defined Function-like total set
S . F₈() is set
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₈() is set
S9 is Relation-like NAT -defined Function-like total set
S9 . F₈() is set
x . 0 is set
S9 . 0 is set
A9 is Relation-like NAT -defined Function-like total set
A9 . 0 is set
F₁() is non empty non void V58() strict Circuit-like unsplit gate`1=arity gate`2isBoolean gate`2=den ManySortedSign
F<sub>2</sub>() is non empty non void V58() strict Circuit-like unsplit gate`1=arity gate`2isBoolean gate`2=den ManySortedSign
F₈() is non pair V21() V22() V23() V27() V28() V121() ext-real non negative set
F₆() is set
F₃() is strict non-empty finite-yielding gate`2=den Boolean MSAlgebra over F<sub>1</sub>()
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<sub>5</sub>(f,g,n,S) is set
F<sub>4</sub>(f,n,S) is non empty V58() ManySortedSign
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<sub>4</sub>(A,S9,S) is non empty V58() ManySortedSign
F<sub>5</sub>(A,x,S9,S) is set
F<sub>7</sub>(S9,S) is set
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₄(A9,S9,S) is non empty V58() ManySortedSign
A2 is strict non-empty finite-yielding gate`2=den Boolean MSAlgebra over A9
F<sub>5</sub>(A9,A2,S9,S) is set
AA is non empty non void V58() strict Circuit-like unsplit gate`1=arity gate`2isBoolean gate`2=den ManySortedSign
f . F₈() is set
g . F₈() is set
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₈() is set
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₈() is set
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₇((S9 . A9),A9) is set
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₄(A2,(S9 . A9),A9) is non empty V58() ManySortedSign
f . (A9 + 1) is set
A9 is set
x . A9 is set
f . A9 is set
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 strict non-empty finite-yielding gate`2=den Boolean MSAlgebra over F<sub>2</sub>()
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<sub>4</sub>(AA,s3,A2) is non empty V58() ManySortedSign
g . (A2 + 1) is set
F<sub>5</sub>(AA,s,s3,A2) is set
n . (A2 + 1) is set
F<sub>7</sub>(s3,A2) is set
g is set
f is non empty V58() ManySortedSign
n is non-empty MSAlgebra over f
S is non-empty MSAlgebra over f
F<sub>1</sub>() is non empty non void V58() strict Circuit-like unsplit gate`1=arity gate`2isBoolean gate`2=den ManySortedSign
F₂() is non empty non void V58() strict Circuit-like unsplit gate`1=arity gate`2isBoolean gate`2=den ManySortedSign
F<sub>8</sub>() is non pair V21() V22() V23() V27() V28() V121() ext-real non negative set
F<sub>6</sub>() is set
F<sub>3</sub>() is strict non-empty finite-yielding gate`2=den Boolean MSAlgebra over F₁()
f is Relation-like NAT -defined Function-like total set
f . F₈() is set
f . 0 is set
g is Relation-like NAT -defined Function-like total set
g . 0 is set
f is Relation-like NAT -defined Function-like total set
f . F₈() is set
f . 0 is set
g is Relation-like NAT -defined Function-like total set
g . 0 is set
n is non empty V58() ManySortedSign
A is set
x is non pair V21() V22() V23() V27() V28() V121() ext-real non negative set
F₄(A,x) is non empty non void V58() Circuit-like unsplit gate`1=arity gate`2isBoolean gate`2=den ManySortedSign
S is non-empty MSAlgebra over n
F<sub>5</sub>(A,x) is set
(F<sub>4</sub>(A,x),F<sub>5</sub>(A,x)) is non-empty MSAlgebra over F<sub>4</sub>(A,x)
S +* (F<sub>4</sub>(A,x),F<sub>5</sub>(A,x)) is strict non-empty MSAlgebra over n +* F<sub>4</sub>(A,x)
n +* F<sub>4</sub>(A,x) is non empty non void V58() strict ManySortedSign
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
n is Relation-like NAT -defined Function-like total set
n . 0 is set
S is Relation-like NAT -defined Function-like total set
S . 0 is set
A is Relation-like NAT -defined Function-like total set
A . 0 is set
S9 is non empty V58() ManySortedSign
x is non pair V21() V22() V23() V27() V28() V121() ext-real non negative set
n . x is set
A9 is non-empty MSAlgebra over S9
S . x is set
A2 is set
A . x is set
x is non pair V21() V22() V23() V27() V28() V121() ext-real non negative set
g . x is set
A . x is set
f . x is set
x + 1 is non empty non pair V21() V22() V23() V27() V28() V121() ext-real non negative M3( REAL , NAT )
g . (x + 1) is set
F<sub>7</sub>((g . x),x) is set
S9 is non empty V58() ManySortedSign
n . x is set
S . x is set
A . (x + 1) is set
S9 is non empty V58() ManySortedSign
A9 is non-empty MSAlgebra over S9
x is set
g . x is set
A . x is set
x is non pair V21() V22() V23() V27() V28() V121() ext-real non negative set
n . x is set
S . x is set
S9 is non empty V58() ManySortedSign
A9 is non-empty MSAlgebra over S9
f . 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
g . x is set
F<sub>4</sub>((g . x),x) is non empty non void V58() Circuit-like unsplit gate`1=arity gate`2isBoolean gate`2=den ManySortedSign
S9 +* F₄((g . x),x) is non empty non void V58() strict ManySortedSign
n . (x + 1) is set
x is non pair V21() V22() V23() V27() V28() V121() ext-real non negative set
n . x is set
S . x is set
A . x is set
x + 1 is non empty non pair V21() V22() V23() V27() V28() V121() ext-real non negative M3( REAL , NAT )
S9 is non empty V58() ManySortedSign
A9 is non-empty MSAlgebra over S9
A2 is set
F₄(A2,x) is non empty non void V58() Circuit-like unsplit gate`1=arity gate`2isBoolean gate`2=den ManySortedSign
S9 +* F<sub>4</sub>(A2,x) is non empty non void V58() strict ManySortedSign
F<sub>5</sub>(A2,x) is set
(F<sub>4</sub>(A2,x),F<sub>5</sub>(A2,x)) is non-empty MSAlgebra over F<sub>4</sub>(A2,x)
A9 +* (F<sub>4</sub>(A2,x),F<sub>5</sub>(A2,x)) is strict non-empty MSAlgebra over S9 +* F<sub>4</sub>(A2,x)
F<sub>7</sub>(A2,x) is set
F<sub>4</sub>(A2,0) is non empty non void V58() Circuit-like unsplit gate`1=arity gate`2isBoolean gate`2=den ManySortedSign
F₅(A2,0) is set
(F₄(A2,0),F₅(A2,0)) is non-empty MSAlgebra over F₄(A2,0)
F₃() +* (F₄(A2,0),F₅(A2,0)) is strict non-empty MSAlgebra over F₁() +* F₄(A2,0)
F₁() +* F₄(A2,0) 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 F₄(A2,0)
F₃() +* AA is strict non-empty finite-yielding gate`2=den Boolean MSAlgebra over F<sub>1</sub>() +* F<sub>4</sub>(A2,0)
s is non empty non void V58() strict Circuit-like unsplit gate`1=arity gate`2isBoolean gate`2=den ManySortedSign
s3 is strict non-empty finite-yielding gate`2=den Boolean MSAlgebra over s
AA is non empty non void V58() strict Circuit-like unsplit gate`1=arity gate`2isBoolean gate`2=den ManySortedSign
s3 is non empty non void V58() strict Circuit-like unsplit gate`1=arity gate`2isBoolean gate`2=den ManySortedSign
s0 is strict non-empty finite-yielding gate`2=den Boolean MSAlgebra over s3
s is strict non-empty finite-yielding gate`2=den Boolean MSAlgebra over AA
s +* (F<sub>4</sub>(A2,x),F<sub>5</sub>(A2,x)) is strict non-empty MSAlgebra over AA +* F<sub>4</sub>(A2,x)
AA +* F<sub>4</sub>(A2,x) is non empty non void V58() strict Circuit-like unsplit gate`1=arity gate`2isBoolean gate`2=den ManySortedSign
s3 is strict non-empty finite-yielding gate`2=den Boolean MSAlgebra over F<sub>4</sub>(A2,x)
s +* s3 is strict non-empty finite-yielding gate`2=den Boolean MSAlgebra over AA +* F₄(A2,x)
n . F₈() is set
S . F₈() is set
x is non empty V58() ManySortedSign
S9 is non-empty MSAlgebra over x
A9 is set
f . A9 is set
n . A9 is set
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 strict non-empty finite-yielding gate`2=den Boolean MSAlgebra over F<sub>2</sub>()
A2 is non pair V21() V22() V23() V27() V28() V121() ext-real non negative set
n . A2 is set
S . A2 is set
A . A2 is set
A2 + 1 is non empty non pair V21() V22() V23() V27() V28() V121() ext-real non negative M3( REAL , NAT )
n . (A2 + 1) is set
S . (A2 + 1) is set
A . (A2 + 1) is set
AA is non empty V58() ManySortedSign
s is non-empty MSAlgebra over AA
s3 is set
F<sub>4</sub>(s3,A2) is non empty non void V58() Circuit-like unsplit gate`1=arity gate`2isBoolean gate`2=den ManySortedSign
F₅(s3,A2) is set
AA +* F₄(s3,A2) is non empty non void V58() strict ManySortedSign
F₇(s3,A2) is set
s0 is non-empty MSAlgebra over F₄(s3,A2)
s +* s0 is strict non-empty MSAlgebra over AA +* F₄(s3,A2)
(F₄(s3,A2),s0) is non-empty MSAlgebra over F₄(s3,A2)
F₁() is non empty V58() ManySortedSign
F₂() is non empty non void V58() strict Circuit-like unsplit gate`1=arity gate`2isBoolean gate`2=den ManySortedSign
F<sub>8</sub>() is non pair V21() V22() V23() V27() V28() V121() ext-real non negative set
F<sub>3</sub>() is non-empty MSAlgebra over F<sub>1</sub>()
F<sub>4</sub>() is set
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<sub>6</sub>(f,g,n,S) is set
F<sub>5</sub>(f,n,S) is non empty V58() ManySortedSign
n is Relation-like NAT -defined Function-like total set
n . F<sub>8</sub>() is set
f is strict non-empty finite-yielding gate`2=den Boolean MSAlgebra over F₂()
S is Relation-like NAT -defined Function-like total set
S . F₈() is set
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₈() is set
g is strict non-empty finite-yielding gate`2=den Boolean MSAlgebra over F<sub>2</sub>()
S9 is Relation-like NAT -defined Function-like total set
S9 . F<sub>8</sub>() is set
x . 0 is set
S9 . 0 is set
A9 is Relation-like NAT -defined Function-like total set
A9 . 0 is set
f is non empty non void V58() Circuit-like ManySortedSign
InnerVertices 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 non empty 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))
g is non empty non void V58() Circuit-like ManySortedSign
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))
n is non empty non void V58() Circuit-like ManySortedSign
f +* g is non empty non void V58() strict ManySortedSign
S is non-empty finite-yielding MSAlgebra over f
A is non-empty finite-yielding MSAlgebra over g
S +* A is strict non-empty MSAlgebra over f +* g
the Sorts of A is Relation-like the carrier of g -defined Function-like total set
K184( the Sorts of A) is functional V77() V78() set
x is non-empty finite-yielding MSAlgebra over n
the Sorts of x is Relation-like the carrier of n -defined Function-like total set
the carrier of n is non empty set
K184( the Sorts of x) is functional V77() V78() set
S9 is Relation-like Function-like M2(K184( the Sorts of A))
Following S9 is Relation-like Function-like M2(K184( the Sorts of A))
A9 is Relation-like Function-like M2(K184( the Sorts of x))
A9 | the carrier of g is Relation-like Function-like set
Following A9 is Relation-like Function-like M2(K184( the Sorts of x))
(Following A9) | the carrier of g is Relation-like Function-like set
the Sorts of S is Relation-like the carrier of f -defined Function-like total set
K184( the Sorts of S) is functional V77() V78() set
A9 | the carrier of f is Relation-like Function-like set
proj1 (Following S9) is set
A2 is Relation-like Function-like M2(K184( the Sorts of S))
Following A2 is Relation-like Function-like M2(K184( the Sorts of S))
(Following A2) +* (Following S9) is Relation-like Function-like set
f is non empty non void V58() Circuit-like ManySortedSign
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 non empty 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))
g is non empty non void V58() Circuit-like ManySortedSign
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 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))
n is non empty non void V58() Circuit-like ManySortedSign
f +* g is non empty non void V58() strict ManySortedSign
S is non-empty finite-yielding MSAlgebra over f
the Sorts of S is Relation-like the carrier of f -defined Function-like total set
K184( the Sorts of S) is functional V77() V78() set
A is non-empty finite-yielding MSAlgebra over g
S +* A is strict non-empty MSAlgebra over f +* g
x is non-empty finite-yielding MSAlgebra over n
the Sorts of x is Relation-like the carrier of n -defined Function-like total set
the carrier of n is non empty set
K184( the Sorts of x) is functional V77() V78() set
S9 is Relation-like Function-like M2(K184( the Sorts of S))
Following S9 is Relation-like Function-like M2(K184( the Sorts of S))
A9 is Relation-like Function-like M2(K184( the Sorts of x))
A9 | the carrier of f is Relation-like Function-like set
Following A9 is Relation-like Function-like M2(K184( the Sorts of x))
(Following A9) | the carrier of f is Relation-like Function-like set
the Sorts of A is Relation-like the carrier of g -defined Function-like total set
K184( the Sorts of A) is functional V77() V78() set
A9 | the carrier of g is Relation-like Function-like set
proj1 (Following S9) is set
A2 is Relation-like Function-like M2(K184( the Sorts of A))
Following A2 is Relation-like Function-like M2(K184( the Sorts of A))
(Following A2) +* (Following S9) is Relation-like Function-like set
f is non empty non void V58() Circuit-like ManySortedSign
InnerVertices 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 non empty 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))
g is non empty non void V58() Circuit-like ManySortedSign
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))
n is non empty non void V58() Circuit-like ManySortedSign
f +* g is non empty non void V58() strict ManySortedSign
S is non-empty finite-yielding MSAlgebra over f
the Sorts of S is Relation-like the carrier of f -defined Function-like total set
K184( the Sorts of S) is functional V77() V78() set
A is non-empty finite-yielding MSAlgebra over g
S +* A is strict non-empty MSAlgebra over f +* g
the Sorts of A is Relation-like the carrier of g -defined Function-like total set
K184( the Sorts of A) is functional V77() V78() set
x is non-empty finite-yielding MSAlgebra over n
the Sorts of x is Relation-like the carrier of n -defined Function-like total set
the carrier of n is non empty set
K184( the Sorts of x) is functional V77() V78() set
S9 is Relation-like Function-like M2(K184( the Sorts of S))
A9 is Relation-like Function-like M2(K184( the Sorts of A))
A2 is Relation-like Function-like M2(K184( the Sorts of x))
A2 | the carrier of f is Relation-like Function-like set
A2 | the carrier of g is Relation-like Function-like set
proj1 A2 is set
the carrier of f \/ the carrier of g is set
S9 +* A9 is Relation-like Function-like set
Following S9 is Relation-like Function-like M2(K184( the Sorts of S))
(Following S9) +* A9 is Relation-like Function-like set
Following A9 is Relation-like Function-like M2(K184( the Sorts of A))
(Following S9) +* (Following A9) is Relation-like Function-like set
Following A2 is Relation-like Function-like M2(K184( the Sorts of x))
f is non empty non void V58() Circuit-like ManySortedSign
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 non empty 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))
g is non empty non void V58() Circuit-like ManySortedSign
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 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))
n is non empty non void V58() Circuit-like ManySortedSign
f +* g is non empty non void V58() strict ManySortedSign
S is non-empty finite-yielding MSAlgebra over f
the Sorts of S is Relation-like the carrier of f -defined Function-like total set
K184( the Sorts of S) is functional V77() V78() set
A is non-empty finite-yielding MSAlgebra over g
S +* A is strict non-empty MSAlgebra over f +* g
the Sorts of A is Relation-like the carrier of g -defined Function-like total set
K184( the Sorts of A) is functional V77() V78() set
x is non-empty finite-yielding MSAlgebra over n
the Sorts of x is Relation-like the carrier of n -defined Function-like total set
the carrier of n is non empty set
K184( the Sorts of x) is functional V77() V78() set
S9 is Relation-like Function-like M2(K184( the Sorts of S))
A9 is Relation-like Function-like M2(K184( the Sorts of A))
A2 is Relation-like Function-like M2(K184( the Sorts of x))
A2 | the carrier of f is Relation-like Function-like set
A2 | the carrier of g is Relation-like Function-like set
proj1 A2 is set
the carrier of f \/ the carrier of g is set
A9 +* S9 is Relation-like Function-like set
Following A9 is Relation-like Function-like M2(K184( the Sorts of A))
(Following A9) +* S9 is Relation-like Function-like set
Following S9 is Relation-like Function-like M2(K184( the Sorts of S))
(Following A9) +* (Following S9) is Relation-like Function-like set
Following A2 is Relation-like Function-like M2(K184( the Sorts of x))
f is non empty non void V58() Circuit-like ManySortedSign
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 non empty 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))
g is non empty non void V58() Circuit-like ManySortedSign
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 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))
n is non empty non void V58() Circuit-like ManySortedSign
f +* g is non empty non void V58() strict ManySortedSign
S is non-empty finite-yielding MSAlgebra over f
the Sorts of S is Relation-like the carrier of f -defined Function-like total set
K184( the Sorts of S) is functional V77() V78() set
A is non-empty finite-yielding MSAlgebra over g
S +* A is strict non-empty MSAlgebra over f +* g
x is non-empty finite-yielding MSAlgebra over n
the Sorts of x is Relation-like the carrier of n -defined Function-like total set
the carrier of n is non empty set
K184( the Sorts of x) is functional V77() V78() set
S9 is Relation-like Function-like M2(K184( the Sorts of x))
S9 | the carrier of f is Relation-like Function-like set
A9 is Relation-like Function-like M2(K184( the Sorts of S))
A2 is non pair V21() V22() V23() V27() V28() V121() ext-real non negative set
A2 + 1 is non empty non pair V21() V22() V23() V27() V28() V121() ext-real non negative M3( REAL , NAT )
Following (S9,(A2 + 1)) is Relation-like Function-like M2(K184( the Sorts of x))
Following (S9,A2) is Relation-like Function-like M2(K184( the Sorts of x))
Following (Following (S9,A2)) is Relation-like Function-like M2(K184( the Sorts of x))
Following (A9,A2) is Relation-like Function-like M2(K184( the Sorts of S))
Following (Following (A9,A2)) is Relation-like Function-like M2(K184( the Sorts of S))
Following (A9,(A2 + 1)) is Relation-like Function-like M2(K184( the Sorts of S))
(Following (S9,A2)) | the carrier of f is Relation-like Function-like set
(Following (S9,(A2 + 1))) | the carrier of f is Relation-like Function-like set
Following (S9,0) is Relation-like Function-like M2(K184( the Sorts of x))
(Following (S9,0)) | the carrier of f is Relation-like Function-like set
Following (A9,0) is Relation-like Function-like M2(K184( the Sorts of S))
g is non empty non void V58() Circuit-like ManySortedSign
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))
f is non empty non void V58() Circuit-like ManySortedSign
InnerVertices 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 non empty 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))
n is non empty non void V58() Circuit-like ManySortedSign
f +* g is non empty non void V58() strict ManySortedSign
S is non-empty finite-yielding MSAlgebra over f
A is non-empty finite-yielding MSAlgebra over g
S +* A is strict non-empty MSAlgebra over f +* g
the Sorts of A is Relation-like the carrier of g -defined Function-like total set
K184( the Sorts of A) is functional V77() V78() set
x is non-empty finite-yielding MSAlgebra over n
the Sorts of x is Relation-like the carrier of n -defined Function-like total set
the carrier of n is non empty set
K184( the Sorts of x) is functional V77() V78() set
g +* f is non empty non void V58() strict ManySortedSign
A +* S is strict non-empty MSAlgebra over g +* f
A9 is Relation-like Function-like M2(K184( the Sorts of A))
S9 is Relation-like Function-like M2(K184( the Sorts of x))
S9 | the carrier of g is Relation-like Function-like set
A2 is non pair V21() V22() V23() V27() V28() V121() ext-real non negative set
Following (S9,A2) is Relation-like Function-like M2(K184( the Sorts of x))
(Following (S9,A2)) | the carrier of g is Relation-like Function-like set
Following (A9,A2) is Relation-like Function-like M2(K184( the Sorts of A))
f is non empty non void V58() Circuit-like ManySortedSign
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 non empty 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))
g is non empty non void V58() Circuit-like ManySortedSign
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 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))
n is non empty non void V58() Circuit-like ManySortedSign
f +* g is non empty non void V58() strict ManySortedSign
the carrier of n is non empty set
the carrier of f \/ the carrier of g is set
S is non-empty finite-yielding MSAlgebra over f
the Sorts of S is Relation-like the carrier of f -defined Function-like total set
K184( the Sorts of S) is functional V77() V78() set
A is non-empty finite-yielding MSAlgebra over g
S +* A is strict non-empty MSAlgebra over f +* g
the Sorts of A is Relation-like the carrier of g -defined Function-like total set
K184( the Sorts of A) is functional V77() V78() set
x is non-empty finite-yielding MSAlgebra over n
the Sorts of x is Relation-like the carrier of n -defined Function-like total set
K184( the Sorts of x) is functional V77() V78() set
S9 is Relation-like Function-like M2(K184( the Sorts of x))
S9 | the carrier of f is Relation-like Function-like set
S9 | the carrier of g is Relation-like Function-like set
Following S9 is Relation-like Function-like M2(K184( the Sorts of x))
(Following S9) | the carrier of g is Relation-like Function-like set
A9 is Relation-like Function-like M2(K184( the Sorts of S))
A2 is Relation-like Function-like M2(K184( the Sorts of A))
Following A2 is Relation-like Function-like M2(K184( the Sorts of A))
AA is set
s is M2( the carrier of g)
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
s3 is M2( the carrier of n)
(Following S9) . s3 is set
Following A9 is Relation-like Function-like M2(K184( the Sorts of S))
(Following A9) . s3 is set
A9 . s is set
s0 is M2( the carrier of f)
S9 . s0 is set
A2 . s is set
(Following A2) . s3 is set
(InnerVertices g) \/ (InputVertices g) is set
(InputVertices f) \ (InnerVertices g) is set
InputVertices n is M2(K19( the carrier of n))
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 f) \/ ((InputVertices g) \ (InnerVertices f)) is set
((Following S9) | the carrier of g) . AA is set
(Following S9) . s is set
(Following A2) . AA is set
proj1 (Following S9) is set
proj1 (Following A2) is set
proj1 ((Following S9) | the carrier of g) is set
n is non empty non void V58() Circuit-like ManySortedSign
f is non empty non void V58() Circuit-like ManySortedSign
g is non empty non void V58() Circuit-like ManySortedSign
f +* g is non empty non void V58() strict ManySortedSign
the carrier of f is non empty set
the carrier of g is non empty set
S is non-empty finite-yielding MSAlgebra over f
the Sorts of S is Relation-like the carrier of f -defined Function-like total set
K184( the Sorts of S) is functional V77() V78() set
A is non-empty finite-yielding MSAlgebra over g
S +* A is strict non-empty MSAlgebra over f +* g
the Sorts of A is Relation-like the carrier of g -defined Function-like total set
K184( the Sorts of A) is functional V77() V78() set
x is non-empty finite-yielding MSAlgebra over n
the Sorts of x is Relation-like the carrier of n -defined Function-like total set
the carrier of n is non empty set
K184( the Sorts of x) is functional V77() V78() set
InnerVertices n is M2(K19( the carrier of n))
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))
InnerVertices f is M2(K19( the carrier of f))
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 non empty 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))
InnerVertices g is M2(K19( the carrier of g))
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))
(InnerVertices f) \/ (InnerVertices g) is set
S9 is Relation-like Function-like M2(K184( the Sorts of x))
S9 | the carrier of f is Relation-like Function-like set
S9 | the carrier of g is Relation-like Function-like set
A9 is Relation-like Function-like M2(K184( the Sorts of S))
Following A9 is Relation-like Function-like M2(K184( the Sorts of S))
A2 is Relation-like Function-like M2(K184( the Sorts of A))
Following A2 is Relation-like Function-like M2(K184( the Sorts of A))
the carrier of f \/ the carrier of g is set
AA is set
InputVertices 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 n) \/ (InnerVertices n) is set
s is M2( the carrier of n)
Following S9 is Relation-like Function-like M2(K184( the Sorts of x))
(Following S9) . s is set
A9 . s is set
A2 . s is set
S9 . AA is set
(Following S9) . AA is set
proj1 (Following S9) is set
proj1 S9 is set
n is non empty non void V58() Circuit-like ManySortedSign
f is non empty non void V58() Circuit-like ManySortedSign
g is non empty non void V58() Circuit-like ManySortedSign
f +* g is non empty non void V58() strict ManySortedSign
the carrier of f is non empty set
the carrier of g is non empty set
the carrier of n is non empty set
the carrier of f \/ the carrier of g is set
S is non-empty finite-yielding MSAlgebra over f
the Sorts of S is Relation-like the carrier of f -defined Function-like total set
K184( the Sorts of S) is functional V77() V78() set
A is non-empty finite-yielding MSAlgebra over g
S +* A is strict non-empty MSAlgebra over f +* g
the Sorts of A is Relation-like the carrier of g -defined Function-like total set
K184( the Sorts of A) is functional V77() V78() set
x is non-empty finite-yielding MSAlgebra over n
the Sorts of x is Relation-like the carrier of n -defined Function-like total set
K184( the Sorts of x) is functional V77() V78() set
S9 is Relation-like Function-like M2(K184( the Sorts of x))
S9 | the carrier of f is Relation-like Function-like set
S9 | the carrier of g is Relation-like Function-like set
Following S9 is Relation-like Function-like M2(K184( the Sorts of x))
A9 is Relation-like Function-like M2(K184( the Sorts of S))
A2 is set
AA is M2( the carrier of f)
InputVertices f is M2(K19( the carrier of f))
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 non empty 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 f is M2(K19( the carrier of f))
(InputVertices f) \/ (InnerVertices f) is set
s is M2( the carrier of n)
A9 . AA is set
Following A9 is Relation-like Function-like M2(K184( the Sorts of S))
(Following A9) . AA is set
S9 . s is set
A9 . A2 is set
(Following A9) . A2 is set
proj1 A9 is set
proj1 (Following A9) is set
A9 is Relation-like Function-like M2(K184( the Sorts of A))
A2 is set
AA is M2( the carrier of g)
InputVertices g is M2(K19( the carrier of g))
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))
InnerVertices g is M2(K19( the carrier of g))
(InputVertices g) \/ (InnerVertices g) is set
s is M2( the carrier of n)
A9 . AA is set
Following A9 is Relation-like Function-like M2(K184( the Sorts of A))
(Following A9) . AA is set
S9 . s is set
A9 . A2 is set
(Following A9) . A2 is set
proj1 A9 is set
proj1 (Following A9) is set
f is non empty non void V58() Circuit-like ManySortedSign
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 non empty 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))
g is non empty non void V58() Circuit-like ManySortedSign
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 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))
n is non empty non void V58() Circuit-like ManySortedSign
f +* g is non empty non void V58() strict ManySortedSign
S is non-empty finite-yielding MSAlgebra over f
the Sorts of S is Relation-like the carrier of f -defined Function-like total set
K184( the Sorts of S) is functional V77() V78() set
A is non-empty finite-yielding MSAlgebra over g
S +* A is strict non-empty MSAlgebra over f +* g
the Sorts of A is Relation-like the carrier of g -defined Function-like total set
K184( the Sorts of A) is functional V77() V78() set
x is non-empty finite-yielding MSAlgebra over n
the Sorts of x is Relation-like the carrier of n -defined Function-like total set
the carrier of n is non empty set
K184( the Sorts of x) is functional V77() V78() set
S9 is Relation-like Function-like M2(K184( the Sorts of S))
A9 is Relation-like Function-like M2(K184( the Sorts of A))
A2 is Relation-like Function-like M2(K184( the Sorts of x))
A2 | the carrier of f is Relation-like Function-like set
A2 | the carrier of g is Relation-like Function-like set
AA is non pair V21() V22() V23() V27() V28() V121() ext-real non negative set
AA + 1 is non empty non pair V21() V22() V23() V27() V28() V121() ext-real non negative M3( REAL , NAT )
Following (A2,(AA + 1)) is Relation-like Function-like M2(K184( the Sorts of x))
Following (A2,AA) is Relation-like Function-like M2(K184( the Sorts of x))
Following (Following (A2,AA)) is Relation-like Function-like M2(K184( the Sorts of x))
Following (A9,AA) is Relation-like Function-like M2(K184( the Sorts of A))
Following (Following (A9,AA)) is Relation-like Function-like M2(K184( the Sorts of A))
Following (A9,(AA + 1)) is Relation-like Function-like M2(K184( the Sorts of A))
(Following (A2,AA)) | the carrier of f is Relation-like Function-like set
Following (S9,AA) is Relation-like Function-like M2(K184( the Sorts of S))
s is Relation-like Function-like M2(K184( the Sorts of S))
(Following (A2,AA)) | the carrier of g is Relation-like Function-like set
(Following (A2,(AA + 1))) | the carrier of g is Relation-like Function-like set
Following (A2,0) is Relation-like Function-like M2(K184( the Sorts of x))
(Following (A2,0)) | the carrier of g is Relation-like Function-like set
Following (A9,0) is Relation-like Function-like M2(K184( the Sorts of A))
f is non empty non void V58() Circuit-like ManySortedSign
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 non empty 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))
g is non empty non void V58() Circuit-like ManySortedSign
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 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))
n is non empty non void V58() Circuit-like ManySortedSign
f +* g is non empty non void V58() strict ManySortedSign
S is non-empty finite-yielding MSAlgebra over f
the Sorts of S is Relation-like the carrier of f -defined Function-like total set
K184( the Sorts of S) is functional V77() V78() set
A is non-empty finite-yielding MSAlgebra over g
S +* A is strict non-empty MSAlgebra over f +* g
the Sorts of A is Relation-like the carrier of g -defined Function-like total set
K184( the Sorts of A) is functional V77() V78() set
x is non-empty finite-yielding MSAlgebra over n
the Sorts of x is Relation-like the carrier of n -defined Function-like total set
the carrier of n is non empty set
K184( the Sorts of x) is functional V77() V78() set
S9 is non pair V21() V22() V23() V27() V28() V121() ext-real non negative set
A9 is non pair V21() V22() V23() V27() V28() V121() ext-real non negative set
S9 + A9 is non pair V21() V22() V23() V27() V28() V121() ext-real non negative set
A2 is Relation-like Function-like M2(K184( the Sorts of x))
A2 | the carrier of f is Relation-like Function-like set
Following (A2,S9) is Relation-like Function-like M2(K184( the Sorts of x))
(Following (A2,S9)) | the carrier of g is Relation-like Function-like set
Following (A2,(S9 + A9)) is Relation-like Function-like M2(K184( the Sorts of x))
AA is Relation-like Function-like M2(K184( the Sorts of S))
Following (AA,S9) is Relation-like Function-like M2(K184( the Sorts of S))
s is Relation-like Function-like M2(K184( the Sorts of A))
Following (s,A9) is Relation-like Function-like M2(K184( the Sorts of A))
(Following (A2,S9)) | the carrier of f is Relation-like Function-like set
Following ((Following (A2,S9)),A9) is Relation-like Function-like M2(K184( the Sorts of x))
(Following (A2,(S9 + A9))) | the carrier of f is Relation-like Function-like set
s3 is Relation-like Function-like M2(K184( the Sorts of S))
Following (s3,A9) is Relation-like Function-like M2(K184( the Sorts of S))
proj1 (Following (A2,(S9 + A9))) is set
the carrier of f \/ the carrier of g is set
s0 is Relation-like Function-like M2(K184( the Sorts of S))
Following (s0,S9) is Relation-like Function-like M2(K184( the Sorts of S))
(Following (A2,(S9 + A9))) | the carrier of g is Relation-like Function-like set
s2 is Relation-like Function-like M2(K184( the Sorts of A))
Following (s2,A9) is Relation-like Function-like M2(K184( the Sorts of A))
Following (Following (A2,(S9 + A9))) is Relation-like Function-like M2(K184( the Sorts of x))
Following (Following (s2,A9)) is Relation-like Function-like M2(K184( the Sorts of A))
Following (Following (s3,A9)) is Relation-like Function-like M2(K184( the Sorts of S))
(Following (Following (s2,A9))) +* (Following (Following (s3,A9))) is Relation-like Function-like set
(Following (s2,A9)) +* (Following (Following (s3,A9))) is Relation-like Function-like set
A9 + 1 is non empty non pair V21() V22() V23() V27() V28() V121() ext-real non negative M3( REAL , NAT )
Following (s3,(A9 + 1)) is Relation-like Function-like M2(K184( the Sorts of S))
(Following (s2,A9)) +* (Following (s3,(A9 + 1))) is Relation-like Function-like set
(Following (s2,A9)) +* s3 is Relation-like Function-like set
(Following (s2,A9)) +* (Following (s3,A9)) is Relation-like Function-like set
f is non empty non void V58() Circuit-like ManySortedSign
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 non empty 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))
g is non empty non void V58() Circuit-like ManySortedSign
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 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))
n is non empty non void V58() Circuit-like ManySortedSign
f +* g is non empty non void V58() strict ManySortedSign
S is non-empty finite-yielding MSAlgebra over f
the Sorts of S is Relation-like the carrier of f -defined Function-like total set
K184( the Sorts of S) is functional V77() V78() set
A is non-empty finite-yielding MSAlgebra over g
S +* A is strict non-empty MSAlgebra over f +* g
the Sorts of A is Relation-like the carrier of g -defined Function-like total set
K184( the Sorts of A) is functional V77() V78() set
x is non-empty finite-yielding MSAlgebra over n
the Sorts of x is Relation-like the carrier of n -defined Function-like total set
the carrier of n is non empty set
K184( the Sorts of x) is functional V77() V78() set
S9 is non pair V21() V22() V23() V27() V28() V121() ext-real non negative set
A9 is non pair V21() V22() V23() V27() V28() V121() ext-real non negative set
S9 + A9 is non pair V21() V22() V23() V27() V28() V121() ext-real non negative set
A2 is Relation-like Function-like M2(K184( the Sorts of x))
Following (A2,(S9 + A9)) is Relation-like Function-like M2(K184( the Sorts of x))
A2 | the carrier of f is Relation-like Function-like set
Following (A2,S9) is Relation-like Function-like M2(K184( the Sorts of x))
(Following (A2,S9)) | the carrier of g is Relation-like Function-like set
AA is Relation-like Function-like M2(K184( the Sorts of S))
Following (AA,S9) is Relation-like Function-like M2(K184( the Sorts of S))
s is Relation-like Function-like M2(K184( the Sorts of A))
Following (s,A9) is Relation-like Function-like M2(K184( the Sorts of A))
f is non empty non void V58() Circuit-like ManySortedSign
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 non empty 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))
g is non empty non void V58() Circuit-like ManySortedSign
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 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))
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))
n is non empty non void V58() Circuit-like ManySortedSign
f +* g is non empty non void V58() strict ManySortedSign
S is non-empty finite-yielding MSAlgebra over f
the Sorts of S is Relation-like the carrier of f -defined Function-like total set
K184( the Sorts of S) is functional V77() V78() set
A is non-empty finite-yielding MSAlgebra over g
S +* A is strict non-empty MSAlgebra over f +* g
the Sorts of A is Relation-like the carrier of g -defined Function-like total set
K184( the Sorts of A) is functional V77() V78() set
x is non-empty finite-yielding MSAlgebra over n
the Sorts of x is Relation-like the carrier of n -defined Function-like total set
the carrier of n is non empty set
K184( the Sorts of x) is functional V77() V78() set
S9 is Relation-like Function-like M2(K184( the Sorts of x))
S9 | the carrier of f is Relation-like Function-like set
S9 | the carrier of g is Relation-like Function-like set
A9 is Relation-like Function-like M2(K184( the Sorts of S))
A2 is Relation-like Function-like M2(K184( the Sorts of A))
AA is non pair V21() V22() V23() V27() V28() V121() ext-real non negative set
Following (S9,AA) is Relation-like Function-like M2(K184( the Sorts of x))
Following (A9,AA) is Relation-like Function-like M2(K184( the Sorts of S))
Following (A2,AA) is Relation-like Function-like M2(K184( the Sorts of A))
(Following (A9,AA)) +* (Following (A2,AA)) is Relation-like Function-like set
(Following (S9,AA)) | the carrier of f is Relation-like Function-like set
proj1 (Following (S9,AA)) is set
the carrier of f \/ the carrier of g is set
g +* f is non empty non void V58() strict ManySortedSign
A +* S is strict non-empty MSAlgebra over g +* f
(Following (S9,AA)) | the carrier of g is Relation-like Function-like set
f is non empty non void V58() Circuit-like ManySortedSign
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 non empty 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))
g is non empty non void V58() Circuit-like ManySortedSign
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 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))
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))
n is non empty non void V58() Circuit-like ManySortedSign
f +* g is non empty non void V58() strict ManySortedSign
S is non-empty finite-yielding MSAlgebra over f
the Sorts of S is Relation-like the carrier of f -defined Function-like total set
K184( the Sorts of S) is functional V77() V78() set
A is non-empty finite-yielding MSAlgebra over g
S +* A is strict non-empty MSAlgebra over f +* g
the Sorts of A is Relation-like the carrier of g -defined Function-like total set
K184( the Sorts of A) is functional V77() V78() set
x is non-empty finite-yielding MSAlgebra over n
the Sorts of x is Relation-like the carrier of n -defined Function-like total set
the carrier of n is non empty set
K184( the Sorts of x) is functional V77() V78() set
S9 is non pair V21() V22() V23() V27() V28() V121() ext-real non negative set
A9 is non pair V21() V22() V23() V27() V28() V121() ext-real non negative set
max (S9,A9) is non pair V21() V22() V23() V27() V28() V121() ext-real non negative set
A2 is Relation-like Function-like M2(K184( the Sorts of x))
A2 | the carrier of f is Relation-like Function-like set
A2 | the carrier of g is Relation-like Function-like set
Following (A2,(max (S9,A9))) is Relation-like Function-like M2(K184( the Sorts of x))
s is Relation-like Function-like M2(K184( the Sorts of S))
Following (s,S9) is Relation-like Function-like M2(K184( the Sorts of S))
(Following (A2,(max (S9,A9)))) | the carrier of f is Relation-like Function-like set
Following (s,(max (S9,A9))) is Relation-like Function-like M2(K184( the Sorts of S))
g +* f is non empty non void V58() strict ManySortedSign
s3 is Relation-like Function-like M2(K184( the Sorts of A))
Following (s3,A9) is Relation-like Function-like M2(K184( the Sorts of A))
A +* S is strict non-empty MSAlgebra over g +* f
(Following (A2,(max (S9,A9)))) | the carrier of g is Relation-like Function-like set
Following (s3,(max (S9,A9))) is Relation-like Function-like M2(K184( the Sorts of A))
(Following (s,(max (S9,A9)))) +* (Following (s3,(max (S9,A9)))) is Relation-like Function-like set
Following (Following (s,(max (S9,A9)))) is Relation-like Function-like M2(K184( the Sorts of S))
(Following (Following (s,(max (S9,A9))))) +* (Following (s3,(max (S9,A9)))) is Relation-like Function-like set
Following (Following (s3,(max (S9,A9)))) is Relation-like Function-like M2(K184( the Sorts of A))
(Following (Following (s,(max (S9,A9))))) +* (Following (Following (s3,(max (S9,A9))))) is Relation-like Function-like set
Following (Following (A2,(max (S9,A9)))) is Relation-like Function-like M2(K184( the Sorts of x))
f is non empty non void V58() Circuit-like ManySortedSign
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 non empty 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))
g is non empty non void V58() Circuit-like ManySortedSign
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 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))
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))
n is non empty non void V58() Circuit-like ManySortedSign
f +* g is non empty non void V58() strict ManySortedSign
S is non-empty finite-yielding MSAlgebra over f
the Sorts of S is Relation-like the carrier of f -defined Function-like total set
K184( the Sorts of S) is functional V77() V78() set
A is non-empty finite-yielding MSAlgebra over g
S +* A is strict non-empty MSAlgebra over f +* g
the Sorts of A is Relation-like the carrier of g -defined Function-like total set
K184( the Sorts of A) is functional V77() V78() set
x is non-empty finite-yielding MSAlgebra over n
the Sorts of x is Relation-like the carrier of n -defined Function-like total set
the carrier of n is non empty set
K184( the Sorts of x) is functional V77() V78() set
S9 is non pair V21() V22() V23() V27() V28() V121() ext-real non negative set
A9 is Relation-like Function-like M2(K184( the Sorts of x))
A9 | the carrier of f is Relation-like Function-like set
A9 | the carrier of g is Relation-like Function-like set
Following (A9,S9) is Relation-like Function-like M2(K184( the Sorts of x))
A2 is Relation-like Function-like M2(K184( the Sorts of S))
Following (A2,S9) is Relation-like Function-like M2(K184( the Sorts of S))
(Following (A9,S9)) | the carrier of f is Relation-like Function-like set
AA is Relation-like Function-like M2(K184( the Sorts of A))
Following (AA,S9) is Relation-like Function-like M2(K184( the Sorts of A))
(Following (A9,S9)) | the carrier of g is Relation-like Function-like set
f is non empty non void V58() Circuit-like ManySortedSign
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 non empty 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))
g is non empty non void V58() Circuit-like ManySortedSign
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 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))
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))
n is non empty non void V58() Circuit-like ManySortedSign
f +* g is non empty non void V58() strict ManySortedSign
S is non-empty finite-yielding MSAlgebra over f
the Sorts of S is Relation-like the carrier of f -defined Function-like total set
K184( the Sorts of S) is functional V77() V78() set
A is non-empty finite-yielding MSAlgebra over g
S +* A is strict non-empty MSAlgebra over f +* g
the Sorts of A is Relation-like the carrier of g -defined Function-like total set
K184( the Sorts of A) is functional V77() V78() set
x is non-empty finite-yielding MSAlgebra over n
the Sorts of x is Relation-like the carrier of n -defined Function-like total set
the carrier of n is non empty set
K184( the Sorts of x) is functional V77() V78() set
S9 is non pair V21() V22() V23() V27() V28() V121() ext-real non negative set
A9 is non pair V21() V22() V23() V27() V28() V121() ext-real non negative set
max (S9,A9) is non pair V21() V22() V23() V27() V28() V121() ext-real non negative set
A2 is Relation-like Function-like M2(K184( the Sorts of x))
Following (A2,(max (S9,A9))) is Relation-like Function-like M2(K184( the Sorts of x))
A2 | the carrier of f is Relation-like Function-like set
A2 | the carrier of g is Relation-like Function-like set
AA is Relation-like Function-like M2(K184( the Sorts of S))
Following (AA,S9) is Relation-like Function-like M2(K184( the Sorts of S))
s is Relation-like Function-like M2(K184( the Sorts of A))
Following (s,A9) is Relation-like Function-like M2(K184( the Sorts of A))
F<sub>1</sub>() is non empty non void V58() strict Circuit-like unsplit gate`1=arity gate`2isBoolean gate`2=den ManySortedSign
F₂() is non empty non void V58() strict Circuit-like unsplit gate`1=arity gate`2isBoolean gate`2=den ManySortedSign
F<sub>3</sub>() is strict non-empty finite-yielding gate`2=den Boolean MSAlgebra over F₁()
the Sorts of F₃() is Relation-like the carrier of F₁() -defined Function-like total set
the carrier of F₁() is non empty set
K184( the Sorts of F₃()) is functional V77() V78() set
F₁₀(0) is non pair V21() V22() V23() V27() V28() V121() ext-real non negative set
F₇() is Relation-like NAT -defined Function-like total set
F₁₀(1) is non pair V21() V22() V23() V27() V28() V121() ext-real non negative set
F₁₀(2) is non pair V21() V22() V23() V27() V28() V121() ext-real non negative set
F₄() is strict non-empty finite-yielding gate`2=den Boolean MSAlgebra over F<sub>2</sub>()
F<sub>7</sub>() . 0 is set
F<sub>8</sub>() is set
InnerVertices F<sub>1</sub>() is M2(K19( the carrier of F<sub>1</sub>()))
K19( the carrier of F<sub>1</sub>()) is set
the ResultSort of F<sub>1</sub>() is Relation-like Function-like V18( the carrier' of F<sub>1</sub>(), the carrier of F<sub>1</sub>()) M2(K19(K20( the carrier' of F<sub>1</sub>(), the carrier of F<sub>1</sub>())))
the carrier' of F<sub>1</sub>() is non empty set
K20( the carrier' of F<sub>1</sub>(), the carrier of F<sub>1</sub>()) is Relation-like set
K19(K20( the carrier' of F<sub>1</sub>(), the carrier of F<sub>1</sub>())) is set
K422( the carrier of F<sub>1</sub>(), the ResultSort of F<sub>1</sub>()) is M2(K19( the carrier of F<sub>1</sub>()))
InputVertices F<sub>1</sub>() is M2(K19( the carrier of F<sub>1</sub>()))
K28( the carrier of F<sub>1</sub>(),K422( the carrier of F<sub>1</sub>(), the ResultSort of F<sub>1</sub>())) is M2(K19( the carrier of F<sub>1</sub>()))
the Sorts of F<sub>4</sub>() is Relation-like the carrier of F<sub>2</sub>() -defined Function-like total set
the carrier of F<sub>2</sub>() is non empty set
K184( the Sorts of F<sub>4</sub>()) is functional V77() V78() set
F<sub>10</sub>(2) * F<sub>10</sub>(1) is non pair V21() V22() V23() V27() V28() V121() ext-real non negative set
F<sub>10</sub>(0) + (F<sub>10</sub>(2) * F<sub>10</sub>(1)) is non pair V21() V22() V23() V27() V28() V121() ext-real non negative set
f is Relation-like NAT -defined Function-like total set
f . F<sub>10</sub>(2) is set
g is Relation-like NAT -defined Function-like total set
g . F<sub>10</sub>(2) is set
f . 0 is set
g . 0 is set
f is Relation-like NAT -defined Function-like total set
f . F<sub>10</sub>(2) is set
g is Relation-like NAT -defined Function-like total set
g . F<sub>10</sub>(2) is set
f . 0 is set
g . 0 is set
n is non pair V21() V22() V23() V27() V28() V121() ext-real non negative set
f . n is set
g . n is set
F<sub>7</sub>() . n is set
n + 1 is non empty non pair V21() V22() V23() V27() V28() V121() ext-real non negative M3( REAL , NAT )
f . (n + 1) is set
g . (n + 1) is set
F<sub>7</sub>() . (n + 1) is set
S is non empty V58() ManySortedSign
A is non-empty MSAlgebra over S
x is set
F<sub>5</sub>(x,n) is non empty non void V58() strict Circuit-like unsplit gate`1=arity gate`2isBoolean gate`2=den ManySortedSign
S +* F₅(x,n) is non empty non void V58() strict ManySortedSign
F₆(x,n) is set
(F₅(x,n),F₆(x,n)) is non-empty MSAlgebra over F₅(x,n)
A +* (F₅(x,n),F₆(x,n)) is strict non-empty MSAlgebra over S +* F₅(x,n)
F₉(x,n) is set
S9 is strict non-empty finite-yielding gate`2=den Boolean MSAlgebra over F<sub>5</sub>(x,n)
n is non pair V21() V22() V23() V27() V28() V121() ext-real non negative set
f . n is set
g . n is set
F<sub>7</sub>() . n is set
n * F<sub>10</sub>(1) is non pair V21() V22() V23() V27() V28() V121() ext-real non negative set
F<sub>10</sub>(0) + (n * F<sub>10</sub>(1)) is non pair V21() V22() V23() V27() V28() V121() ext-real non negative set
n + 1 is non empty non pair V21() V22() V23() V27() V28() V121() ext-real non negative M3( REAL , NAT )
F<sub>7</sub>() . (n + 1) is set
(n + 1) * F<sub>10</sub>(1) is non pair V21() V22() V23() V27() V28() V121() ext-real non negative set
F<sub>10</sub>(0) + ((n + 1) * F<sub>10</sub>(1)) is non pair V21() V22() V23() V27() V28() V121() ext-real non negative set
S is non empty V58() ManySortedSign
A is non-empty MSAlgebra over S
x is set
F<sub>5</sub>(x,n) is non empty non void V58() strict Circuit-like unsplit gate`1=arity gate`2isBoolean gate`2=den ManySortedSign
S +* F₅(x,n) is non empty non void V58() strict ManySortedSign
F₆(x,n) is set
(F₅(x,n),F₆(x,n)) is non-empty MSAlgebra over F₅(x,n)
A +* (F₅(x,n),F₆(x,n)) is strict non-empty MSAlgebra over S +* F₅(x,n)
F₉(x,n) is set
S9 is non empty non void V58() strict Circuit-like unsplit gate`1=arity gate`2isBoolean gate`2=den ManySortedSign
A9 is strict non-empty finite-yielding gate`2=den Boolean MSAlgebra over S9
the Sorts of A9 is Relation-like the carrier of S9 -defined Function-like total set
the carrier of S9 is non empty set
K184( the Sorts of A9) is functional V77() V78() set
S9 +* F₅(x,n) is non empty non void V58() strict Circuit-like unsplit gate`1=arity gate`2isBoolean gate`2=den ManySortedSign
AA is non empty V58() ManySortedSign
s3 is set
s0 is non pair V21() V22() V23() V27() V28() V121() ext-real non negative set
F<sub>5</sub>(s3,s0) is non empty non void V58() strict Circuit-like unsplit gate`1=arity gate`2isBoolean gate`2=den ManySortedSign
s is non-empty MSAlgebra over AA
F₆(s3,s0) is set
(F₅(s3,s0),F₆(s3,s0)) is non-empty MSAlgebra over F₅(s3,s0)
s +* (F₅(s3,s0),F₆(s3,s0)) is strict non-empty MSAlgebra over AA +* F₅(s3,s0)
AA +* F₅(s3,s0) is non empty non void V58() strict ManySortedSign
s is non empty V58() ManySortedSign
AA is non pair V21() V22() V23() V27() V28() V121() ext-real non negative set
f . AA is set
s3 is set
F₇() . AA is set
AA + 1 is non empty non pair V21() V22() V23() V27() V28() V121() ext-real non negative M3( REAL , NAT )
f . (AA + 1) is set
F₅(s3,AA) is non empty non void V58() strict Circuit-like unsplit gate`1=arity gate`2isBoolean gate`2=den ManySortedSign
s +* F<sub>5</sub>(s3,AA) is non empty non void V58() strict ManySortedSign
F<sub>7</sub>() . (AA + 1) is set
F<sub>9</sub>(s3,AA) is set
InputVertices F<sub>5</sub>(s3,AA) is M2(K19( the carrier of F<sub>5</sub>(s3,AA)))
the carrier of F<sub>5</sub>(s3,AA) is non empty set
K19( the carrier of F<sub>5</sub>(s3,AA)) is set
the ResultSort of F<sub>5</sub>(s3,AA) is Relation-like Function-like V18( the carrier' of F<sub>5</sub>(s3,AA), the carrier of F<sub>5</sub>(s3,AA)) M2(K19(K20( the carrier' of F<sub>5</sub>(s3,AA), the carrier of F<sub>5</sub>(s3,AA))))
the carrier' of F<sub>5</sub>(s3,AA) is non empty set
K20( the carrier' of F<sub>5</sub>(s3,AA), the carrier of F<sub>5</sub>(s3,AA)) is Relation-like set
K19(K20( the carrier' of F<sub>5</sub>(s3,AA), the carrier of F<sub>5</sub>(s3,AA))) is set
K422( the carrier of F<sub>5</sub>(s3,AA), the ResultSort of F<sub>5</sub>(s3,AA)) is M2(K19( the carrier of F<sub>5</sub>(s3,AA)))
K28( the carrier of F<sub>5</sub>(s3,AA),K422( the carrier of F<sub>5</sub>(s3,AA), the ResultSort of F<sub>5</sub>(s3,AA))) is M2(K19( the carrier of F<sub>5</sub>(s3,AA)))
InnerVertices F<sub>5</sub>(s3,AA) is M2(K19( the carrier of F<sub>5</sub>(s3,AA)))
A2 is strict non-empty finite-yielding gate`2=den Boolean MSAlgebra over F₅(x,n)
A9 +* A2 is strict non-empty finite-yielding gate`2=den Boolean MSAlgebra over S9 +* F<sub>5</sub>(x,n)
AA is strict non-empty finite-yielding gate`2=den Boolean MSAlgebra over S9 +* F₅(x,n)
the Sorts of AA is Relation-like the carrier of (S9 +* F₅(x,n)) -defined Function-like total set
the carrier of (S9 +* F₅(x,n)) is non empty set
K184( the Sorts of AA) is functional V77() V78() set
(n + 1) * F₁₀(1) is non pair V21() V22() V23() V27() V28() V121() ext-real non negative M3( REAL , NAT )
F₁₀(0) + ((n + 1) * F₁₀(1)) is non pair V21() V22() V23() V27() V28() V121() ext-real non negative M3( REAL , NAT )
(F₁₀(0) + (n * F₁₀(1))) + F₁₀(1) is non pair V21() V22() V23() V27() V28() V121() ext-real non negative set
s is Relation-like Function-like M2(K184( the Sorts of AA))
Following (s,(F₁₀(0) + ((n + 1) * F₁₀(1)))) is Relation-like Function-like M2(K184( the Sorts of AA))
s0 is set
s3 is non pair V21() V22() V23() V27() V28() V121() ext-real non negative set
F₇() . s3 is set
F₅(s0,s3) is non empty non void V58() strict Circuit-like unsplit gate`1=arity gate`2isBoolean gate`2=den ManySortedSign
InputVertices F<sub>5</sub>(s0,s3) is M2(K19( the carrier of F<sub>5</sub>(s0,s3)))
the carrier of F<sub>5</sub>(s0,s3) is non empty set
K19( the carrier of F<sub>5</sub>(s0,s3)) is set
the ResultSort of F<sub>5</sub>(s0,s3) is Relation-like Function-like V18( the carrier' of F<sub>5</sub>(s0,s3), the carrier of F<sub>5</sub>(s0,s3)) M2(K19(K20( the carrier' of F<sub>5</sub>(s0,s3), the carrier of F<sub>5</sub>(s0,s3))))
the carrier' of F<sub>5</sub>(s0,s3) is non empty set
K20( the carrier' of F<sub>5</sub>(s0,s3), the carrier of F<sub>5</sub>(s0,s3)) is Relation-like set
K19(K20( the carrier' of F<sub>5</sub>(s0,s3), the carrier of F<sub>5</sub>(s0,s3))) is set
K422( the carrier of F<sub>5</sub>(s0,s3), the ResultSort of F<sub>5</sub>(s0,s3)) is M2(K19( the carrier of F<sub>5</sub>(s0,s3)))
K28( the carrier of F<sub>5</sub>(s0,s3),K422( the carrier of F<sub>5</sub>(s0,s3), the ResultSort of F<sub>5</sub>(s0,s3))) is M2(K19( the carrier of F<sub>5</sub>(s0,s3)))
{s0} is set
(InputVertices F<sub>5</sub>(s0,s3)) \ {s0} is set
s0 is set
s3 is non pair V21() V22() V23() V27() V28() V121() ext-real non negative set
F<sub>5</sub>(s0,s3) is non empty non void V58() strict Circuit-like unsplit gate`1=arity gate`2isBoolean gate`2=den ManySortedSign
InnerVertices F₅(s0,s3) is M2(K19( the carrier of F₅(s0,s3)))
the carrier of F₅(s0,s3) is non empty set
K19( the carrier of F₅(s0,s3)) is set
the ResultSort of F₅(s0,s3) is Relation-like Function-like V18( the carrier' of F₅(s0,s3), the carrier of F₅(s0,s3)) M2(K19(K20( the carrier' of F₅(s0,s3), the carrier of F₅(s0,s3))))
the carrier' of F₅(s0,s3) is non empty set
K20( the carrier' of F₅(s0,s3), the carrier of F₅(s0,s3)) is Relation-like set
K19(K20( the carrier' of F₅(s0,s3), the carrier of F₅(s0,s3))) is set
K422( the carrier of F₅(s0,s3), the ResultSort of F₅(s0,s3)) is M2(K19( the carrier of F₅(s0,s3)))
f . (n + 1) is set
F₅(H₃(n),n) is non empty non void V58() strict Circuit-like unsplit gate`1=arity gate`2isBoolean gate`2=den ManySortedSign
InputVertices F<sub>5</sub>(H<sub>3</sub>(n),n) is M2(K19( the carrier of F<sub>5</sub>(H<sub>3</sub>(n),n)))
the carrier of F<sub>5</sub>(H<sub>3</sub>(n),n) is non empty set
K19( the carrier of F<sub>5</sub>(H<sub>3</sub>(n),n)) is set
the ResultSort of F<sub>5</sub>(H<sub>3</sub>(n),n) is Relation-like Function-like V18( the carrier' of F<sub>5</sub>(H<sub>3</sub>(n),n), the carrier of F<sub>5</sub>(H<sub>3</sub>(n),n)) M2(K19(K20( the carrier' of F<sub>5</sub>(H<sub>3</sub>(n),n), the carrier of F<sub>5</sub>(H<sub>3</sub>(n),n))))
the carrier' of F<sub>5</sub>(H<sub>3</sub>(n),n) is non empty set
K20( the carrier' of F<sub>5</sub>(H<sub>3</sub>(n),n), the carrier of F<sub>5</sub>(H<sub>3</sub>(n),n)) is Relation-like set
K19(K20( the carrier' of F<sub>5</sub>(H<sub>3</sub>(n),n), the carrier of F<sub>5</sub>(H<sub>3</sub>(n),n))) is set
K422( the carrier of F<sub>5</sub>(H<sub>3</sub>(n),n), the ResultSort of F<sub>5</sub>(H<sub>3</sub>(n),n)) is M2(K19( the carrier of F<sub>5</sub>(H<sub>3</sub>(n),n)))
K28( the carrier of F<sub>5</sub>(H<sub>3</sub>(n),n),K422( the carrier of F<sub>5</sub>(H<sub>3</sub>(n),n), the ResultSort of F<sub>5</sub>(H<sub>3</sub>(n),n))) is M2(K19( the carrier of F<sub>5</sub>(H<sub>3</sub>(n),n)))
{H<sub>3</sub>(n)} is set
(InputVertices F<sub>5</sub>(H<sub>3</sub>(n),n)) \ {H<sub>3</sub>(n)} is set
InputVertices S9 is M2(K19( the carrier of S9))
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))
InnerVertices F<sub>5</sub>(x,n) is M2(K19( the carrier of F<sub>5</sub>(x,n)))
the carrier of F<sub>5</sub>(x,n) is non empty set
K19( the carrier of F<sub>5</sub>(x,n)) is set
the ResultSort of F<sub>5</sub>(x,n) is Relation-like Function-like V18( the carrier' of F<sub>5</sub>(x,n), the carrier of F<sub>5</sub>(x,n)) M2(K19(K20( the carrier' of F<sub>5</sub>(x,n), the carrier of F<sub>5</sub>(x,n))))
the carrier' of F<sub>5</sub>(x,n) is non empty set
K20( the carrier' of F<sub>5</sub>(x,n), the carrier of F<sub>5</sub>(x,n)) is Relation-like set
K19(K20( the carrier' of F<sub>5</sub>(x,n), the carrier of F<sub>5</sub>(x,n))) is set
K422( the carrier of F<sub>5</sub>(x,n), the ResultSort of F<sub>5</sub>(x,n)) is M2(K19( the carrier of F<sub>5</sub>(x,n)))
s3 is non empty non void V58() Circuit-like unsplit gate`1=arity gate`2isBoolean gate`2=den ManySortedSign
s0 is non empty non void V58() Circuit-like unsplit gate`1=arity gate`2isBoolean gate`2=den ManySortedSign
InputVertices s0 is M2(K19( the carrier of s0))
the carrier of s0 is non empty set
K19( the carrier of s0) is set
the ResultSort of s0 is Relation-like Function-like V18( the carrier' of s0, the carrier of s0) M2(K19(K20( the carrier' of s0, the carrier of s0)))
the carrier' of s0 is non empty set
K20( the carrier' of s0, the carrier of s0) is Relation-like set
K19(K20( the carrier' of s0, the carrier of s0)) is set
K422( the carrier of s0, the ResultSort of s0) is M2(K19( the carrier of s0))
K28( the carrier of s0,K422( the carrier of s0, the ResultSort of s0)) is M2(K19( the carrier of s0))
InputVertices s3 is M2(K19( the carrier of s3))
the carrier of s3 is non empty set
K19( the carrier of s3) is set
the ResultSort of s3 is Relation-like Function-like V18( the carrier' of s3, the carrier of s3) M2(K19(K20( the carrier' of s3, the carrier of s3)))
the carrier' of s3 is non empty set
K20( the carrier' of s3, the carrier of s3) is Relation-like set
K19(K20( the carrier' of s3, the carrier of s3)) is set
K422( the carrier of s3, the ResultSort of s3) is M2(K19( the carrier of s3))
K28( the carrier of s3,K422( the carrier of s3, the ResultSort of s3)) is M2(K19( the carrier of s3))
(InputVertices s3) \/ ((InputVertices F<sub>5</sub>(H<sub>3</sub>(n),n)) \ {H<sub>3</sub>(n)}) is set
InnerVertices s3 is M2(K19( the carrier of s3))
the Sorts of A2 is Relation-like the carrier of F<sub>5</sub>(x,n) -defined Function-like total set
K184( the Sorts of A2) is functional V77() V78() set
s3 is Relation-like Function-like M2(K184( the Sorts of A2))
Following (s3,F<sub>10</sub>(1)) is Relation-like Function-like M2(K184( the Sorts of A2))
Following (s,(F<sub>10</sub>(0) + ((n + 1) * F<sub>10</sub>(1)))) is Relation-like Function-like M2(K184( the Sorts of AA))
n is non empty V58() ManySortedSign
A is set
x is non pair V21() V22() V23() V27() V28() V121() ext-real non negative set
F<sub>5</sub>(A,x) is non empty non void V58() strict Circuit-like unsplit gate`1=arity gate`2isBoolean gate`2=den ManySortedSign
S is non-empty MSAlgebra over n
F₆(A,x) is set
(F₅(A,x),F₆(A,x)) is non-empty MSAlgebra over F₅(A,x)
S +* (F₅(A,x),F₆(A,x)) is strict non-empty MSAlgebra over n +* F₅(A,x)
n +* F₅(A,x) is non empty non void V58() strict ManySortedSign
0 * F₁₀(1) is non pair V21() V22() V23() V27() V28() V121() ext-real non negative set
F₁₀(0) + (0 * F₁₀(1)) is non pair V21() V22() V23() V27() V28() V121() ext-real non negative set
F₇() . F₁₀(2) is set
S is non empty V58() ManySortedSign
x is non empty non void V58() strict Circuit-like unsplit gate`1=arity gate`2isBoolean gate`2=den ManySortedSign
n is Relation-like Function-like M2(K184( the Sorts of F<sub>4</sub>()))
Following (n,(F<sub>10</sub>(0) + (F<sub>10</sub>(2) * F<sub>10</sub>(1)))) is Relation-like Function-like M2(K184( the Sorts of F<sub>4</sub>()))
A is non-empty MSAlgebra over S
S9 is strict non-empty finite-yielding gate`2=den Boolean MSAlgebra over x
the Sorts of S9 is Relation-like the carrier of x -defined Function-like total set
the carrier of x is non empty set
K184( the Sorts of S9) is functional V77() V78() set