let x1, x2 be set ; :: thesis: for X being non empty finite set
for n being Element of NAT
for f being Function of (n -tuples_on X),X
for p being FinSeqLen of n
for S being Signature of X st rng p = x1 \/ x2 & x1 c= the carrier of S & x2 misses InnerVertices S & not Output (1GateCircStr (p,f)) in InputVertices S holds
InputVertices (S +* (1GateCircStr (p,f))) = (InputVertices S) \/ x2
let X be non empty finite set ; :: thesis: for n being Element of NAT
for f being Function of (n -tuples_on X),X
for p being FinSeqLen of n
for S being Signature of X st rng p = x1 \/ x2 & x1 c= the carrier of S & x2 misses InnerVertices S & not Output (1GateCircStr (p,f)) in InputVertices S holds
InputVertices (S +* (1GateCircStr (p,f))) = (InputVertices S) \/ x2
let n be Element of NAT ; :: thesis: for f being Function of (n -tuples_on X),X
for p being FinSeqLen of n
for S being Signature of X st rng p = x1 \/ x2 & x1 c= the carrier of S & x2 misses InnerVertices S & not Output (1GateCircStr (p,f)) in InputVertices S holds
InputVertices (S +* (1GateCircStr (p,f))) = (InputVertices S) \/ x2
let f be Function of (n -tuples_on X),X; :: thesis: for p being FinSeqLen of n
for S being Signature of X st rng p = x1 \/ x2 & x1 c= the carrier of S & x2 misses InnerVertices S & not Output (1GateCircStr (p,f)) in InputVertices S holds
InputVertices (S +* (1GateCircStr (p,f))) = (InputVertices S) \/ x2
let p be FinSeqLen of n; :: thesis: for S being Signature of X st rng p = x1 \/ x2 & x1 c= the carrier of S & x2 misses InnerVertices S & not Output (1GateCircStr (p,f)) in InputVertices S holds
InputVertices (S +* (1GateCircStr (p,f))) = (InputVertices S) \/ x2
let S be Signature of X; :: thesis: ( rng p = x1 \/ x2 & x1 c= the carrier of S & x2 misses InnerVertices S & not Output (1GateCircStr (p,f)) in InputVertices S implies InputVertices (S +* (1GateCircStr (p,f))) = (InputVertices S) \/ x2 )
assume that
A1: rng p = x1 \/ x2 and
A2: x1 c= the carrier of S and
A3: x2 misses InnerVertices S and
A4: not Output (1GateCircStr (p,f)) in InputVertices S ; :: thesis: InputVertices (S +* (1GateCircStr (p,f))) = (InputVertices S) \/ x2
A5: the carrier of S = (InputVertices S) \/ (InnerVertices S) by XBOOLE_1:45;
thus InputVertices (S +* (1GateCircStr (p,f))) = ((InputVertices S) \ (InnerVertices (1GateCircStr (p,f)))) \/ ((InputVertices (1GateCircStr (p,f))) \ (InnerVertices S)) by CIRCCMB2:5, CIRCCOMB:47
.= ((InputVertices S) \ (InnerVertices (1GateCircStr (p,f)))) \/ ((rng p) \ (InnerVertices S)) by CIRCCOMB:42
.= ((InputVertices S) \ (InnerVertices (1GateCircStr (p,f)))) \/ ((x1 \ (InnerVertices S)) \/ x2) by A1, A3, XBOOLE_1:87
.= (((InputVertices S) \ (InnerVertices (1GateCircStr (p,f)))) \/ (x1 \ (InnerVertices S))) \/ x2 by XBOOLE_1:4
.= (((InputVertices S) \ {(Output (1GateCircStr (p,f)))}) \/ (x1 \ (InnerVertices S))) \/ x2 by Th17
.= ((InputVertices S) \/ (x1 \ (InnerVertices S))) \/ x2 by A4, ZFMISC_1:57
.= (InputVertices S) \/ x2 by A2, A5, XBOOLE_1:12, XBOOLE_1:43 ; :: thesis: verum