let x, y, z be non pair set ; InputVertices (GFA2CarryStr (x,y,z)) = {x,y,z}
set f1 = and2a ;
set f2 = and2c ;
set f3 = nor2 ;
set f4 = nor3 ;
set xy = [<*x,y*>,and2a];
set yz = [<*y,z*>,and2c];
set zx = [<*z,x*>,nor2];
set Cxy = 1GateCircStr (<*x,y*>,and2a);
set Cyz = 1GateCircStr (<*y,z*>,and2c);
set Czx = 1GateCircStr (<*z,x*>,nor2);
set M = GFA2CarryStr (x,y,z);
set MI = GFA2CarryIStr (x,y,z);
set S = 1GateCircStr (<*[<*x,y*>,and2a],[<*y,z*>,and2c],[<*z,x*>,nor2]*>,nor3);
A1:
( InputVertices (1GateCircStr (<*x,y*>,and2a)) = {x,y} & InputVertices (1GateCircStr (<*y,z*>,and2c)) = {y,z} )
by FACIRC_1:40;
A2:
InputVertices (1GateCircStr (<*z,x*>,nor2)) = {z,x}
by FACIRC_1:40;
A3:
InputVertices (1GateCircStr (<*[<*x,y*>,and2a],[<*y,z*>,and2c],[<*z,x*>,nor2]*>,nor3)) = {[<*x,y*>,and2a],[<*y,z*>,and2c],[<*z,x*>,nor2]}
by FACIRC_1:42;
A4:
InnerVertices (1GateCircStr (<*[<*x,y*>,and2a],[<*y,z*>,and2c],[<*z,x*>,nor2]*>,nor3)) is Relation
by FACIRC_1:38;
A5:
( InnerVertices (1GateCircStr (<*x,y*>,and2a)) = {[<*x,y*>,and2a]} & InnerVertices (1GateCircStr (<*y,z*>,and2c)) = {[<*y,z*>,and2c]} )
by CIRCCOMB:42;
1GateCircStr (<*x,y*>,and2a) tolerates 1GateCircStr (<*y,z*>,and2c)
by CIRCCOMB:47;
then A6:
( InnerVertices (1GateCircStr (<*z,x*>,nor2)) = {[<*z,x*>,nor2]} & InnerVertices ((1GateCircStr (<*x,y*>,and2a)) +* (1GateCircStr (<*y,z*>,and2c))) = {[<*x,y*>,and2a]} \/ {[<*y,z*>,and2c]} )
by A5, CIRCCOMB:11, CIRCCOMB:42;
(1GateCircStr (<*x,y*>,and2a)) +* (1GateCircStr (<*y,z*>,and2c)) tolerates 1GateCircStr (<*z,x*>,nor2)
by CIRCCOMB:47;
then InnerVertices (GFA2CarryIStr (x,y,z)) =
({[<*x,y*>,and2a]} \/ {[<*y,z*>,and2c]}) \/ {[<*z,x*>,nor2]}
by A6, CIRCCOMB:11
.=
{[<*x,y*>,and2a],[<*y,z*>,and2c]} \/ {[<*z,x*>,nor2]}
by ENUMSET1:1
.=
{[<*x,y*>,and2a],[<*y,z*>,and2c],[<*z,x*>,nor2]}
by ENUMSET1:3
;
then A7:
(InputVertices (1GateCircStr (<*[<*x,y*>,and2a],[<*y,z*>,and2c],[<*z,x*>,nor2]*>,nor3))) \ (InnerVertices (GFA2CarryIStr (x,y,z))) = {}
by A3, XBOOLE_1:37;
A8:
( InputVertices (1GateCircStr (<*x,y*>,and2a)) is without_pairs & InputVertices (1GateCircStr (<*y,z*>,and2c)) is without_pairs )
by FACIRC_1:41;
then A9:
( InputVertices (1GateCircStr (<*z,x*>,nor2)) is without_pairs & InputVertices ((1GateCircStr (<*x,y*>,and2a)) +* (1GateCircStr (<*y,z*>,and2c))) is without_pairs )
by FACIRC_1:9, FACIRC_1:41;
then
InputVertices (GFA2CarryIStr (x,y,z)) is without_pairs
by FACIRC_1:9;
then
InputVertices (GFA2CarryStr (x,y,z)) = (InputVertices (GFA2CarryIStr (x,y,z))) \/ ((InputVertices (1GateCircStr (<*[<*x,y*>,and2a],[<*y,z*>,and2c],[<*z,x*>,nor2]*>,nor3))) \ (InnerVertices (GFA2CarryIStr (x,y,z))))
by A4, FACIRC_1:6;
hence InputVertices (GFA2CarryStr (x,y,z)) =
(InputVertices ((1GateCircStr (<*x,y*>,and2a)) +* (1GateCircStr (<*y,z*>,and2c)))) \/ (InputVertices (1GateCircStr (<*z,x*>,nor2)))
by A9, A6, A7, FACIRC_1:7
.=
((InputVertices (1GateCircStr (<*x,y*>,and2a))) \/ (InputVertices (1GateCircStr (<*y,z*>,and2c)))) \/ (InputVertices (1GateCircStr (<*z,x*>,nor2)))
by A8, A5, FACIRC_1:7
.=
{x,y,y,z} \/ {z,x}
by A1, A2, ENUMSET1:5
.=
{y,y,x,z} \/ {z,x}
by ENUMSET1:67
.=
{y,x,z} \/ {z,x}
by ENUMSET1:31
.=
{x,y,z} \/ {z,x}
by ENUMSET1:58
.=
{x,y,z} \/ ({z} \/ {x})
by ENUMSET1:1
.=
({x,y,z} \/ {z}) \/ {x}
by XBOOLE_1:4
.=
({z,x,y} \/ {z}) \/ {x}
by ENUMSET1:59
.=
{z,z,x,y} \/ {x}
by ENUMSET1:4
.=
{z,x,y} \/ {x}
by ENUMSET1:31
.=
{x,y,z} \/ {x}
by ENUMSET1:59
.=
{x,x,y,z}
by ENUMSET1:4
.=
{x,y,z}
by ENUMSET1:31
;
verum