scheme :: CIRCCMB2:sch 10
CIRCCMB29sch10{ F₁() -> non empty non void unsplit gate`1=arity gate`2isBoolean ManySortedSign , F₂( object ) -> object , 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 ex S1, S2 being non empty non void unsplit gate`1=arity gate`2isBoolean ManySortedSign st
( S1 = F₂(n) & S2 = F₂((n + 1)) & InputVertices S2 = (InputVertices S1) \/ ((InputVertices F₄((F₃() . n),n)) \ {(F₃() . n)}) & InnerVertices S1 is Relation & InputVertices S1 is without_pairs )

provided

A1: InnerVertices F₁() is Relation and
A2: InputVertices F₁() is without_pairs and
A3: ( F₂(0) = F₁() & F₃() . 0 in InnerVertices F₁() ) 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) )