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

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

provided

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