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

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

provided

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