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