scheme :: CIRCCMB3:sch 18
Comb5CircResult{ F₁() -> object , F₂() -> object , F₃() -> object , F₄() -> object , F₅() -> object , F₆() -> non empty finite set , F₇( object , object , object , object , object ) -> Element of F₆(), F₈() -> finite Signature of F₆(), F₉() -> Circuit of F₆(),F₈(), F₁₀() -> Function of (5 -tuples_on F₆()),F₆() } :

for s being State of (F₉() +* (1GateCircuit (<*F₁(),F₂(),F₃(),F₄(),F₅()*>,F₁₀())))
for s9 being State of F₉() st s9 = s | the carrier of F₈() holds
for a1, a2, a3, a4, a5 being Element of F₆() st ( F₁() in InnerVertices F₈() implies a1 = (Result s9) . F₁() ) & ( not F₁() in InnerVertices F₈() implies a1 = s . F₁() ) & ( F₂() in InnerVertices F₈() implies a2 = (Result s9) . F₂() ) & ( not F₂() in InnerVertices F₈() implies a2 = s . F₂() ) & ( F₃() in InnerVertices F₈() implies a3 = (Result s9) . F₃() ) & ( not F₃() in InnerVertices F₈() implies a3 = s . F₃() ) & ( F₄() in InnerVertices F₈() implies a4 = (Result s9) . F₄() ) & ( not F₄() in InnerVertices F₈() implies a4 = s . F₄() ) & ( F₅() in InnerVertices F₈() implies a5 = (Result s9) . F₅() ) & ( not F₅() in InnerVertices F₈() implies a5 = s . F₅() ) holds
(Result s) . (Output (1GateCircStr (<*F₁(),F₂(),F₃(),F₄(),F₅()*>,F₁₀()))) = F₇(a1,a2,a3,a4,a5)

provided

A1: for g being Function of (5 -tuples_on F₆()),F₆() holds
( g = F₁₀() iff for a1, a2, a3, a4, a5 being Element of F₆() holds g . <*a1,a2,a3,a4,a5*> = F₇(a1,a2,a3,a4,a5) ) and
A2: not Output (1GateCircStr (<*F₁(),F₂(),F₃(),F₄(),F₅()*>,F₁₀())) in InputVertices F₈()