theorem Th42:
for
x1,
x2,
x3 being
set for
X being non
empty finite set for
f being
Function of
(3 -tuples_on X),
X for
S being
Signature of
X st
x2 in the
carrier of
S & not
x1 in InnerVertices S & not
x3 in InnerVertices S & not
Output (1GateCircStr (<*x1,x2,x3*>,f)) in InputVertices S holds
InputVertices (S +* (1GateCircStr (<*x1,x2,x3*>,f))) = (InputVertices S) \/ {x1,x3}