scheme :: CIRCCMB3:sch 10
OneGate2Result{ F₁() -> object , F₂() -> object , F₃() -> non empty finite set , F₄( object , object ) -> Element of F₃(), F₅() -> Function of (2 -tuples_on F₃()),F₃() } :

for s being State of (1GateCircuit (<*F₁(),F₂()*>,F₅()))
for a1, a2 being Element of F₃() st a1 = s . F₁() & 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) )