let x1 be set ; :: thesis: for X being non empty finite set
for f being Function of (1 -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 ) holds
S +* (1GateCircStr (<*x1*>,f)) is with_nonpair_inputs
let X be non empty finite set ; :: thesis: for f being Function of (1 -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 ) holds
S +* (1GateCircStr (<*x1*>,f)) is with_nonpair_inputs
let f be Function of (1 -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 ) holds
S +* (1GateCircStr (<*x1*>,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 ) implies S +* (1GateCircStr (<*x1*>,f)) is with_nonpair_inputs )
assume A1: ( x1 in the carrier of S or not x1 is pair ) ; :: thesis: S +* (1GateCircStr (<*x1*>,f)) is with_nonpair_inputs
A2: not Output (1GateCircStr (<*x1*>,f)) in InputVertices S by FACIRC_1:def 2;
per cases ( x1 in the carrier of S or not x1 is pair ) by A1;
suppose x1 in the carrier of S ; :: thesis: S +* (1GateCircStr (<*x1*>,f)) is with_nonpair_inputs
hence InputVertices (S +* (1GateCircStr (<*x1*>,f))) is without_pairs by A2, Th37; :: according to CIRCCMB3:def 11 :: thesis: verum
end;
suppose not x1 is pair ; :: thesis: S +* (1GateCircStr (<*x1*>,f)) is with_nonpair_inputs
then reconsider a = x1 as non pair set ;
rng <*x1*> = {a} by FINSEQ_1:38;
hence InputVertices (S +* (1GateCircStr (<*x1*>,f))) is without_pairs ; :: according to CIRCCMB3:def 11 :: thesis: verum
end;
end;