let x, y, z be set ; ( x <> [<*y,z*>,and2c] & y <> [<*z,x*>,and2b] & z <> [<*x,y*>,and2a] implies InputVertices (GFA2CarryIStr (x,y,z)) = {x,y,z} )
set f1 = and2a ;
set f2 = and2c ;
set f3 = and2b ;
set xy = [<*x,y*>,and2a];
set yz = [<*y,z*>,and2c];
set zx = [<*z,x*>,and2b];
set Cxy = 1GateCircStr (<*x,y*>,and2a);
set Cyz = 1GateCircStr (<*y,z*>,and2c);
set Czx = 1GateCircStr (<*z,x*>,and2b);
assume that
A1:
x <> [<*y,z*>,and2c]
and
A2:
( y <> [<*z,x*>,and2b] & z <> [<*x,y*>,and2a] )
; InputVertices (GFA2CarryIStr (x,y,z)) = {x,y,z}
A3:
not [<*x,y*>,and2a] in {y,z}
by A1, A2, Lm1;
A4:
not [<*z,x*>,and2b] in {x,y,z}
by A1, A2, Lm1;
A5:
y <> [<*y,z*>,and2c]
by FACIRC_2:3;
A6:
( not z in {[<*x,y*>,and2a],[<*y,z*>,and2c]} & not x in {[<*x,y*>,and2a],[<*y,z*>,and2c]} )
by A1, A2, Lm1;
A7:
1GateCircStr (<*x,y*>,and2a) tolerates 1GateCircStr (<*y,z*>,and2c)
by CIRCCOMB:55;
InputVertices (GFA2CarryIStr (x,y,z)) =
((InputVertices ((1GateCircStr (<*x,y*>,and2a)) +* (1GateCircStr (<*y,z*>,and2c)))) \ (InnerVertices (1GateCircStr (<*z,x*>,and2b)))) \/ ((InputVertices (1GateCircStr (<*z,x*>,and2b))) \ (InnerVertices ((1GateCircStr (<*x,y*>,and2a)) +* (1GateCircStr (<*y,z*>,and2c)))))
by CIRCCMB2:6, CIRCCOMB:55
.=
((((InputVertices (1GateCircStr (<*x,y*>,and2a))) \ (InnerVertices (1GateCircStr (<*y,z*>,and2c)))) \/ ((InputVertices (1GateCircStr (<*y,z*>,and2c))) \ (InnerVertices (1GateCircStr (<*x,y*>,and2a))))) \ (InnerVertices (1GateCircStr (<*z,x*>,and2b)))) \/ ((InputVertices (1GateCircStr (<*z,x*>,and2b))) \ (InnerVertices ((1GateCircStr (<*x,y*>,and2a)) +* (1GateCircStr (<*y,z*>,and2c)))))
by CIRCCMB2:6, CIRCCOMB:55
.=
((((InputVertices (1GateCircStr (<*x,y*>,and2a))) \ (InnerVertices (1GateCircStr (<*y,z*>,and2c)))) \/ ((InputVertices (1GateCircStr (<*y,z*>,and2c))) \ (InnerVertices (1GateCircStr (<*x,y*>,and2a))))) \ (InnerVertices (1GateCircStr (<*z,x*>,and2b)))) \/ ((InputVertices (1GateCircStr (<*z,x*>,and2b))) \ ((InnerVertices (1GateCircStr (<*x,y*>,and2a))) \/ (InnerVertices (1GateCircStr (<*y,z*>,and2c)))))
by A7, CIRCCOMB:15
.=
((((InputVertices (1GateCircStr (<*x,y*>,and2a))) \ {[<*y,z*>,and2c]}) \/ ((InputVertices (1GateCircStr (<*y,z*>,and2c))) \ (InnerVertices (1GateCircStr (<*x,y*>,and2a))))) \ (InnerVertices (1GateCircStr (<*z,x*>,and2b)))) \/ ((InputVertices (1GateCircStr (<*z,x*>,and2b))) \ ((InnerVertices (1GateCircStr (<*x,y*>,and2a))) \/ (InnerVertices (1GateCircStr (<*y,z*>,and2c)))))
by CIRCCOMB:49
.=
((((InputVertices (1GateCircStr (<*x,y*>,and2a))) \ {[<*y,z*>,and2c]}) \/ ((InputVertices (1GateCircStr (<*y,z*>,and2c))) \ {[<*x,y*>,and2a]})) \ (InnerVertices (1GateCircStr (<*z,x*>,and2b)))) \/ ((InputVertices (1GateCircStr (<*z,x*>,and2b))) \ ((InnerVertices (1GateCircStr (<*x,y*>,and2a))) \/ (InnerVertices (1GateCircStr (<*y,z*>,and2c)))))
by CIRCCOMB:49
.=
((((InputVertices (1GateCircStr (<*x,y*>,and2a))) \ {[<*y,z*>,and2c]}) \/ ((InputVertices (1GateCircStr (<*y,z*>,and2c))) \ {[<*x,y*>,and2a]})) \ {[<*z,x*>,and2b]}) \/ ((InputVertices (1GateCircStr (<*z,x*>,and2b))) \ ((InnerVertices (1GateCircStr (<*x,y*>,and2a))) \/ (InnerVertices (1GateCircStr (<*y,z*>,and2c)))))
by CIRCCOMB:49
.=
((((InputVertices (1GateCircStr (<*x,y*>,and2a))) \ {[<*y,z*>,and2c]}) \/ ((InputVertices (1GateCircStr (<*y,z*>,and2c))) \ {[<*x,y*>,and2a]})) \ {[<*z,x*>,and2b]}) \/ ((InputVertices (1GateCircStr (<*z,x*>,and2b))) \ ({[<*x,y*>,and2a]} \/ (InnerVertices (1GateCircStr (<*y,z*>,and2c)))))
by CIRCCOMB:49
.=
((((InputVertices (1GateCircStr (<*x,y*>,and2a))) \ {[<*y,z*>,and2c]}) \/ ((InputVertices (1GateCircStr (<*y,z*>,and2c))) \ {[<*x,y*>,and2a]})) \ {[<*z,x*>,and2b]}) \/ ((InputVertices (1GateCircStr (<*z,x*>,and2b))) \ ({[<*x,y*>,and2a]} \/ {[<*y,z*>,and2c]}))
by CIRCCOMB:49
.=
((({x,y} \ {[<*y,z*>,and2c]}) \/ ((InputVertices (1GateCircStr (<*y,z*>,and2c))) \ {[<*x,y*>,and2a]})) \ {[<*z,x*>,and2b]}) \/ ((InputVertices (1GateCircStr (<*z,x*>,and2b))) \ ({[<*x,y*>,and2a]} \/ {[<*y,z*>,and2c]}))
by FACIRC_1:40
.=
((({x,y} \ {[<*y,z*>,and2c]}) \/ ({y,z} \ {[<*x,y*>,and2a]})) \ {[<*z,x*>,and2b]}) \/ ((InputVertices (1GateCircStr (<*z,x*>,and2b))) \ ({[<*x,y*>,and2a]} \/ {[<*y,z*>,and2c]}))
by FACIRC_1:40
.=
((({x,y} \ {[<*y,z*>,and2c]}) \/ ({y,z} \ {[<*x,y*>,and2a]})) \ {[<*z,x*>,and2b]}) \/ ({z,x} \ ({[<*x,y*>,and2a]} \/ {[<*y,z*>,and2c]}))
by FACIRC_1:40
.=
((({x,y} \ {[<*y,z*>,and2c]}) \/ ({y,z} \ {[<*x,y*>,and2a]})) \ {[<*z,x*>,and2b]}) \/ ({z,x} \ {[<*x,y*>,and2a],[<*y,z*>,and2c]})
by ENUMSET1:41
.=
(({x,y} \/ ({y,z} \ {[<*x,y*>,and2a]})) \ {[<*z,x*>,and2b]}) \/ ({z,x} \ {[<*x,y*>,and2a],[<*y,z*>,and2c]})
by A1, A5, FACIRC_2:1
.=
(({x,y} \/ {y,z}) \ {[<*z,x*>,and2b]}) \/ ({z,x} \ {[<*x,y*>,and2a],[<*y,z*>,and2c]})
by A3, ZFMISC_1:65
.=
(({x,y} \/ {y,z}) \ {[<*z,x*>,and2b]}) \/ {z,x}
by A6, ZFMISC_1:72
.=
({x,y,y,z} \ {[<*z,x*>,and2b]}) \/ {z,x}
by ENUMSET1:45
.=
({y,y,x,z} \ {[<*z,x*>,and2b]}) \/ {z,x}
by ENUMSET1:110
.=
({y,x,z} \ {[<*z,x*>,and2b]}) \/ {z,x}
by ENUMSET1:71
.=
({x,y,z} \ {[<*z,x*>,and2b]}) \/ {z,x}
by ENUMSET1:99
.=
{x,y,z} \/ {z,x}
by A4, ZFMISC_1:65
.=
{x,y,z,z,x}
by ENUMSET1:49
.=
{x,y,z,z} \/ {x}
by ENUMSET1:50
.=
{z,z,x,y} \/ {x}
by ENUMSET1:118
.=
{z,x,y} \/ {x}
by ENUMSET1:71
.=
{z,x,y,x}
by ENUMSET1:46
.=
{x,x,y,z}
by ENUMSET1:113
.=
{x,y,z}
by ENUMSET1:71
;
hence
InputVertices (GFA2CarryIStr (x,y,z)) = {x,y,z}
; verum