let x1, x2 be set ; for X being non empty finite set
for f being Function of (2 -tuples_on X),X
for S being Signature of X st x1 in the carrier of S & not x2 in InnerVertices S & not Output (1GateCircStr (<*x1,x2*>,f)) in InputVertices S holds
InputVertices (S +* (1GateCircStr (<*x1,x2*>,f))) = (InputVertices S) \/ {x2}
let X be non empty finite set ; for f being Function of (2 -tuples_on X),X
for S being Signature of X st x1 in the carrier of S & not x2 in InnerVertices S & not Output (1GateCircStr (<*x1,x2*>,f)) in InputVertices S holds
InputVertices (S +* (1GateCircStr (<*x1,x2*>,f))) = (InputVertices S) \/ {x2}
set p = <*x1,x2*>;
let f be Function of (2 -tuples_on X),X; for S being Signature of X st x1 in the carrier of S & not x2 in InnerVertices S & not Output (1GateCircStr (<*x1,x2*>,f)) in InputVertices S holds
InputVertices (S +* (1GateCircStr (<*x1,x2*>,f))) = (InputVertices S) \/ {x2}
let S be Signature of X; ( x1 in the carrier of S & not x2 in InnerVertices S & not Output (1GateCircStr (<*x1,x2*>,f)) in InputVertices S implies InputVertices (S +* (1GateCircStr (<*x1,x2*>,f))) = (InputVertices S) \/ {x2} )
assume that
A1:
x1 in the carrier of S
and
A2:
not x2 in InnerVertices S
; ( Output (1GateCircStr (<*x1,x2*>,f)) in InputVertices S or InputVertices (S +* (1GateCircStr (<*x1,x2*>,f))) = (InputVertices S) \/ {x2} )
A3: rng <*x1,x2*> =
{x1,x2}
by FINSEQ_2:127
.=
{x1} \/ {x2}
by ENUMSET1:1
;
{x1} c= the carrier of S
by A1, ZFMISC_1:31;
hence
( Output (1GateCircStr (<*x1,x2*>,f)) in InputVertices S or InputVertices (S +* (1GateCircStr (<*x1,x2*>,f))) = (InputVertices S) \/ {x2} )
by A2, A3, Th36, ZFMISC_1:50; verum