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

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

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

then ( InputVertices (S +* (1GateCircStr <*x1,x2,x3*>,f)) = InputVertices S or ( not {x2} is with_pair & InputVertices (S +* (1GateCircStr <*x1,x2,x3*>,f)) = {x2} \/ (InputVertices S) ) or ( not {x1} is with_pair & InputVertices (S +* (1GateCircStr <*x1,x2,x3*>,f)) = {x1} \/ (InputVertices S) ) or ( not {x3} is with_pair & InputVertices (S +* (1GateCircStr <*x1,x2,x3*>,f)) = {x3} \/ (InputVertices S) ) or ( not {x1,x2} is with_pair & InputVertices (S +* (1GateCircStr <*x1,x2,x3*>,f)) = {x1,x2} \/ (InputVertices S) ) or ( not {x2,x3} is with_pair & InputVertices (S +* (1GateCircStr <*x1,x2,x3*>,f)) = {x2,x3} \/ (InputVertices S) ) or ( not {x1,x3} is with_pair & InputVertices (S +* (1GateCircStr <*x1,x2,x3*>,f)) = {x1,x3} \/ (InputVertices S) ) ) by A1, A2, Th45, Th46, Th47, Th48, Th49, Th50, Th51;
hence not InputVertices (S +* (1GateCircStr <*x1,x2,x3*>,f)) is with_pair ; :: according to CIRCCMB3:def 11 :: thesis: verum

end;

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

then reconsider a = x1, b = x2, c = x3 as non pair set ;
( rng <*x1,x2,x3*> = {a,b,c} & {a,b,c} = {} \/ {a,b,c} & {} c= the carrier of S & {a,b,c} misses InnerVertices S ) by FACIRC_1:5, FINSEQ_2:148, XBOOLE_1:2;
then InputVertices (S +* (1GateCircStr <*x1,x2,x3*>,f)) = (InputVertices S) \/ {a,b,c} by A2, Th40;
hence not InputVertices (S +* (1GateCircStr <*x1,x2,x3*>,f)) is with_pair ; :: according to CIRCCMB3:def 11 :: thesis: verum

end;

end;