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 ( {x2} is without_pairs & InputVertices (S +* (1GateCircStr (<*x1,x2,x3*>,f))) = {x2} \/ (InputVertices S) ) or ( {x1} is without_pairs & InputVertices (S +* (1GateCircStr (<*x1,x2,x3*>,f))) = {x1} \/ (InputVertices S) ) or ( {x3} is without_pairs & InputVertices (S +* (1GateCircStr (<*x1,x2,x3*>,f))) = {x3} \/ (InputVertices S) ) or ( {x1,x2} is without_pairs & InputVertices (S +* (1GateCircStr (<*x1,x2,x3*>,f))) = {x1,x2} \/ (InputVertices S) ) or ( {x2,x3} is without_pairs & InputVertices (S +* (1GateCircStr (<*x1,x2,x3*>,f))) = {x2,x3} \/ (InputVertices S) ) or ( {x1,x3} is without_pairs & InputVertices (S +* (1GateCircStr (<*x1,x2,x3*>,f))) = {x1,x3} \/ (InputVertices S) ) ) by A1, A2, Th41, Th42, Th43, Th44, Th45, Th46, Th47;
hence InputVertices (S +* (1GateCircStr (<*x1,x2,x3*>,f))) is without_pairs ; :: 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} by FINSEQ_2:128;
hence InputVertices (S +* (1GateCircStr (<*x1,x2,x3*>,f))) is without_pairs ; :: according to CIRCCMB3:def 11 :: thesis: verum
end;
end;