theorem Th44: :: CIRCCMB3:44

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 x1 in the carrier of S & x2 in the carrier of 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) \/ {x3}