scheme :: CIRCCMB2:sch 11
CIRCCMB29sch11{ F₁( set ) -> non empty non void unsplit gate`1=arity gate`2isBoolean ManySortedSign , F₂() -> ManySortedSet of NAT , F₃( object , object ) -> non empty non void unsplit gate`1=arity gate`2isBoolean ManySortedSign , F₄( object , object ) -> object } :

for n being Nat holds
( InputVertices F₁((n + 1)) = (InputVertices F₁(n)) \/ ((InputVertices F₃((F₂() . n),n)) \ {(F₂() . n)}) & InnerVertices F₁(n) is Relation & InputVertices F₁(n) is without_pairs )

provided

A1: InnerVertices F₁(0) is Relation and
A2: InputVertices F₁(0) is without_pairs and
A3: F₂() . 0 in InnerVertices F₁(0) and
A4: for n being Nat
for x being set holds InnerVertices F₃(x,n) is Relation and
A5: for n being Nat
for x being set st x = F₂() . n holds
(InputVertices F₃(x,n)) \ {x} is without_pairs and
A6: for n being Nat
for S being non empty ManySortedSign
for x being set st S = F₁(n) & x = F₂() . n holds
( F₁((n + 1)) = S +* F₃(x,n) & F₂() . (n + 1) = F₄(x,n) & x in InputVertices F₃(x,n) & F₄(x,n) in InnerVertices F₃(x,n) )