scheme :: CIRCCMB3:sch 16
Comb3CircResult{ F₁() -> object , F₂() -> object , F₃() -> object , F₄() -> non empty finite set , F₅( object , object , object ) -> Element of F₄(), F₆() -> finite Signature of F₄(), F₇() -> Circuit of F₄(),F₆(), F₈() -> Function of (3 -tuples_on F₄()),F₄() } :

for s being State of (F₇() +* (1GateCircuit (<*F₁(),F₂(),F₃()*>,F₈())))
for s9 being State of F₇() st s9 = s | the carrier of F₆() holds
for a1, a2, a3 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₃() ) holds
(Result s) . (Output (1GateCircStr (<*F₁(),F₂(),F₃()*>,F₈()))) = F₅(a1,a2,a3)

provided

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