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