let x1, x2 be set ; :: thesis: 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 ; :: thesis: 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; :: thesis: 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; :: thesis: ( 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 A1: ( x1 in the carrier of S & not x2 in InnerVertices S ) ; :: thesis: ( Output (1GateCircStr <*x1,x2*>,f) in InputVertices S or InputVertices (S +* (1GateCircStr <*x1,x2*>,f)) = (InputVertices S) \/ {x2} )
A2: {x1} c= the carrier of S by A1, ZFMISC_1:37;
rng <*x1,x2*> = {x1,x2} by FINSEQ_2:147
.= {x1} \/ {x2} by ENUMSET1:41 ;
hence ( Output (1GateCircStr <*x1,x2*>,f) in InputVertices S or InputVertices (S +* (1GateCircStr <*x1,x2*>,f)) = (InputVertices S) \/ {x2} ) by A1, A2, Th40, ZFMISC_1:56; :: thesis: verum