let x, y, z be set ; ( 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 ] )
; 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:3;
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:55;
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:6, CIRCCOMB:55
.=
((((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:6, CIRCCOMB:55
.=
((((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:15
.=
((((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:49
.=
((((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:49
.=
((((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:49
.=
((((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:49
.=
((((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:49
.=
((({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:41
.=
(({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:65
.=
(({x,y} \/ {y,z}) \ {[<*z,x*>,and2 ]}) \/ {z,x}
by A6, ZFMISC_1:72
.=
({x,y,y,z} \ {[<*z,x*>,and2 ]}) \/ {z,x}
by ENUMSET1:45
.=
({y,y,x,z} \ {[<*z,x*>,and2 ]}) \/ {z,x}
by ENUMSET1:110
.=
({y,x,z} \ {[<*z,x*>,and2 ]}) \/ {z,x}
by ENUMSET1:71
.=
({x,y,z} \ {[<*z,x*>,and2 ]}) \/ {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 (GFA1CarryIStr x,y,z) = {x,y,z}
; verum