let x, y, z be set ; :: thesis: ( x <> [<*y,z*>,and2a] & y <> [<*z,x*>,and2] & z <> [<*x,y*>,and2c] implies InputVertices (GFA1CarryIStr (x,y,z)) = {x,y,z} )
set f1 = and2c ;
set f2 = and2a ;
set f3 = and2 ;
set xy = [<*x,y*>,and2c];
set yz = [<*y,z*>,and2a];
set zx = [<*z,x*>,and2];
set Cxy = 1GateCircStr (<*x,y*>,and2c);
set Cyz = 1GateCircStr (<*y,z*>,and2a);
set Czx = 1GateCircStr (<*z,x*>,and2);
assume that
A1: x <> [<*y,z*>,and2a] and
A2: ( y <> [<*z,x*>,and2] & z <> [<*x,y*>,and2c] ) ; :: thesis: InputVertices (GFA1CarryIStr (x,y,z)) = {x,y,z}
A3: not [<*x,y*>,and2c] in {y,z} by A1, A2, Lm1;
A4: not [<*z,x*>,and2] in {x,y,z} by A1, A2, Lm1;
A5: y <> [<*y,z*>,and2a] by FACIRC_2:2;
A6: ( not z in {[<*x,y*>,and2c],[<*y,z*>,and2a]} & not x in {[<*x,y*>,and2c],[<*y,z*>,and2a]} ) by A1, A2, Lm1;
A7: 1GateCircStr (<*x,y*>,and2c) tolerates 1GateCircStr (<*y,z*>,and2a) by CIRCCOMB:47;
InputVertices (GFA1CarryIStr (x,y,z)) = ((InputVertices ((1GateCircStr (<*x,y*>,and2c)) +* (1GateCircStr (<*y,z*>,and2a)))) \ (InnerVertices (1GateCircStr (<*z,x*>,and2)))) \/ ((InputVertices (1GateCircStr (<*z,x*>,and2))) \ (InnerVertices ((1GateCircStr (<*x,y*>,and2c)) +* (1GateCircStr (<*y,z*>,and2a))))) by CIRCCMB2:5, CIRCCOMB:47
.= ((((InputVertices (1GateCircStr (<*x,y*>,and2c))) \ (InnerVertices (1GateCircStr (<*y,z*>,and2a)))) \/ ((InputVertices (1GateCircStr (<*y,z*>,and2a))) \ (InnerVertices (1GateCircStr (<*x,y*>,and2c))))) \ (InnerVertices (1GateCircStr (<*z,x*>,and2)))) \/ ((InputVertices (1GateCircStr (<*z,x*>,and2))) \ (InnerVertices ((1GateCircStr (<*x,y*>,and2c)) +* (1GateCircStr (<*y,z*>,and2a))))) by CIRCCMB2:5, CIRCCOMB:47
.= ((((InputVertices (1GateCircStr (<*x,y*>,and2c))) \ (InnerVertices (1GateCircStr (<*y,z*>,and2a)))) \/ ((InputVertices (1GateCircStr (<*y,z*>,and2a))) \ (InnerVertices (1GateCircStr (<*x,y*>,and2c))))) \ (InnerVertices (1GateCircStr (<*z,x*>,and2)))) \/ ((InputVertices (1GateCircStr (<*z,x*>,and2))) \ ((InnerVertices (1GateCircStr (<*x,y*>,and2c))) \/ (InnerVertices (1GateCircStr (<*y,z*>,and2a))))) by A7, CIRCCOMB:11
.= ((((InputVertices (1GateCircStr (<*x,y*>,and2c))) \ {[<*y,z*>,and2a]}) \/ ((InputVertices (1GateCircStr (<*y,z*>,and2a))) \ (InnerVertices (1GateCircStr (<*x,y*>,and2c))))) \ (InnerVertices (1GateCircStr (<*z,x*>,and2)))) \/ ((InputVertices (1GateCircStr (<*z,x*>,and2))) \ ((InnerVertices (1GateCircStr (<*x,y*>,and2c))) \/ (InnerVertices (1GateCircStr (<*y,z*>,and2a))))) by CIRCCOMB:42
.= ((((InputVertices (1GateCircStr (<*x,y*>,and2c))) \ {[<*y,z*>,and2a]}) \/ ((InputVertices (1GateCircStr (<*y,z*>,and2a))) \ {[<*x,y*>,and2c]})) \ (InnerVertices (1GateCircStr (<*z,x*>,and2)))) \/ ((InputVertices (1GateCircStr (<*z,x*>,and2))) \ ((InnerVertices (1GateCircStr (<*x,y*>,and2c))) \/ (InnerVertices (1GateCircStr (<*y,z*>,and2a))))) by CIRCCOMB:42
.= ((((InputVertices (1GateCircStr (<*x,y*>,and2c))) \ {[<*y,z*>,and2a]}) \/ ((InputVertices (1GateCircStr (<*y,z*>,and2a))) \ {[<*x,y*>,and2c]})) \ {[<*z,x*>,and2]}) \/ ((InputVertices (1GateCircStr (<*z,x*>,and2))) \ ((InnerVertices (1GateCircStr (<*x,y*>,and2c))) \/ (InnerVertices (1GateCircStr (<*y,z*>,and2a))))) by CIRCCOMB:42
.= ((((InputVertices (1GateCircStr (<*x,y*>,and2c))) \ {[<*y,z*>,and2a]}) \/ ((InputVertices (1GateCircStr (<*y,z*>,and2a))) \ {[<*x,y*>,and2c]})) \ {[<*z,x*>,and2]}) \/ ((InputVertices (1GateCircStr (<*z,x*>,and2))) \ ({[<*x,y*>,and2c]} \/ (InnerVertices (1GateCircStr (<*y,z*>,and2a))))) by CIRCCOMB:42
.= ((((InputVertices (1GateCircStr (<*x,y*>,and2c))) \ {[<*y,z*>,and2a]}) \/ ((InputVertices (1GateCircStr (<*y,z*>,and2a))) \ {[<*x,y*>,and2c]})) \ {[<*z,x*>,and2]}) \/ ((InputVertices (1GateCircStr (<*z,x*>,and2))) \ ({[<*x,y*>,and2c]} \/ {[<*y,z*>,and2a]})) by CIRCCOMB:42
.= ((({x,y} \ {[<*y,z*>,and2a]}) \/ ((InputVertices (1GateCircStr (<*y,z*>,and2a))) \ {[<*x,y*>,and2c]})) \ {[<*z,x*>,and2]}) \/ ((InputVertices (1GateCircStr (<*z,x*>,and2))) \ ({[<*x,y*>,and2c]} \/ {[<*y,z*>,and2a]})) by FACIRC_1:40
.= ((({x,y} \ {[<*y,z*>,and2a]}) \/ ({y,z} \ {[<*x,y*>,and2c]})) \ {[<*z,x*>,and2]}) \/ ((InputVertices (1GateCircStr (<*z,x*>,and2))) \ ({[<*x,y*>,and2c]} \/ {[<*y,z*>,and2a]})) by FACIRC_1:40
.= ((({x,y} \ {[<*y,z*>,and2a]}) \/ ({y,z} \ {[<*x,y*>,and2c]})) \ {[<*z,x*>,and2]}) \/ ({z,x} \ ({[<*x,y*>,and2c]} \/ {[<*y,z*>,and2a]})) by FACIRC_1:40
.= ((({x,y} \ {[<*y,z*>,and2a]}) \/ ({y,z} \ {[<*x,y*>,and2c]})) \ {[<*z,x*>,and2]}) \/ ({z,x} \ {[<*x,y*>,and2c],[<*y,z*>,and2a]}) by ENUMSET1:1
.= (({x,y} \/ ({y,z} \ {[<*x,y*>,and2c]})) \ {[<*z,x*>,and2]}) \/ ({z,x} \ {[<*x,y*>,and2c],[<*y,z*>,and2a]}) by A1, A5, FACIRC_2:1
.= (({x,y} \/ {y,z}) \ {[<*z,x*>,and2]}) \/ ({z,x} \ {[<*x,y*>,and2c],[<*y,z*>,and2a]}) by A3, ZFMISC_1:57
.= (({x,y} \/ {y,z}) \ {[<*z,x*>,and2]}) \/ {z,x} by A6, ZFMISC_1:63
.= ({x,y,y,z} \ {[<*z,x*>,and2]}) \/ {z,x} by ENUMSET1:5
.= ({y,y,x,z} \ {[<*z,x*>,and2]}) \/ {z,x} by ENUMSET1:67
.= ({y,x,z} \ {[<*z,x*>,and2]}) \/ {z,x} by ENUMSET1:31
.= ({x,y,z} \ {[<*z,x*>,and2]}) \/ {z,x} by ENUMSET1:58
.= {x,y,z} \/ {z,x} by A4, ZFMISC_1:57
.= {x,y,z,z,x} by ENUMSET1:9
.= {x,y,z,z} \/ {x} by ENUMSET1:10
.= {z,z,x,y} \/ {x} by ENUMSET1:73
.= {z,x,y} \/ {x} by ENUMSET1:31
.= {z,x,y,x} by ENUMSET1:6
.= {x,x,y,z} by ENUMSET1:70
.= {x,y,z} by ENUMSET1:31 ;
hence InputVertices (GFA1CarryIStr (x,y,z)) = {x,y,z} ; :: thesis: verum