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 with_nonpair_inputs Signature of X st ( x1 in the carrier of S or not x1 is pair ) & ( x2 in the carrier of S or not x2 is pair ) holds
S +* (1GateCircStr (<*x1,x2*>,f)) is with_nonpair_inputs
let X be non empty finite set ; :: thesis: for f being Function of (2 -tuples_on X),X
for S being with_nonpair_inputs Signature of X st ( x1 in the carrier of S or not x1 is pair ) & ( x2 in the carrier of S or not x2 is pair ) holds
S +* (1GateCircStr (<*x1,x2*>,f)) is with_nonpair_inputs
let f be Function of (2 -tuples_on X),X; :: thesis: for S being with_nonpair_inputs Signature of X st ( x1 in the carrier of S or not x1 is pair ) & ( x2 in the carrier of S or not x2 is pair ) holds
S +* (1GateCircStr (<*x1,x2*>,f)) is with_nonpair_inputs
let S be with_nonpair_inputs Signature of X; :: thesis: ( ( x1 in the carrier of S or not x1 is pair ) & ( x2 in the carrier of S or not x2 is pair ) implies S +* (1GateCircStr (<*x1,x2*>,f)) is with_nonpair_inputs )
assume A1: ( ( x1 in the carrier of S or not x1 is pair ) & ( x2 in the carrier of S or not x2 is pair ) ) ; :: thesis: S +* (1GateCircStr (<*x1,x2*>,f)) is with_nonpair_inputs
A2: not Output (1GateCircStr (<*x1,x2*>,f)) in InputVertices S by FACIRC_1:def 2;

per cases ( ( x1 in the carrier of S & x2 in the carrier of S ) or ( x1 in the carrier of S & not x2 in InnerVertices S ) or ( x2 in the carrier of S & not x1 in InnerVertices S ) or ( not x1 is pair & not x2 is pair ) ) by A1;

suppose ( ( x1 in the carrier of S & x2 in the carrier of S ) or ( x1 in the carrier of S & not x2 in InnerVertices S ) or ( x2 in the carrier of S & not x1 in InnerVertices S ) ) ; :: thesis: S +* (1GateCircStr (<*x1,x2*>,f)) is with_nonpair_inputs

then ( InputVertices (S +* (1GateCircStr (<*x1,x2*>,f))) = InputVertices S or ( {x2} is without_pairs & InputVertices (S +* (1GateCircStr (<*x1,x2*>,f))) = {x2} \/ (InputVertices S) ) or ( {x1} is without_pairs & InputVertices (S +* (1GateCircStr (<*x1,x2*>,f))) = {x1} \/ (InputVertices S) ) ) by A1, A2, Th38, Th39, Th40;
hence InputVertices (S +* (1GateCircStr (<*x1,x2*>,f))) is without_pairs ; :: according to CIRCCMB3:def 11 :: thesis: verum

end;

suppose ( not x1 is pair & not x2 is pair ) ; :: thesis: S +* (1GateCircStr (<*x1,x2*>,f)) is with_nonpair_inputs

then reconsider a = x1, b = x2 as non pair set ;
rng <*x1,x2*> = {a,b} by FINSEQ_2:127;
hence InputVertices (S +* (1GateCircStr (<*x1,x2*>,f))) is without_pairs ; :: according to CIRCCMB3:def 11 :: thesis: verum

end;

end;