let x, y, z be set ; ( x <> [<*y,z*>,nor2] & y <> [<*z,x*>,nor2] & z <> [<*x,y*>,nor2] implies 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 xyz = [<*[<*x,y*>,nor2],[<*y,z*>,nor2],[<*z,x*>,nor2]*>,nor3];
set S = 1GateCircStr (<*[<*x,y*>,nor2],[<*y,z*>,nor2],[<*z,x*>,nor2]*>,nor3);
set MI = GFA3CarryIStr (x,y,z);
A1: InputVertices (1GateCircStr (<*[<*x,y*>,nor2],[<*y,z*>,nor2],[<*z,x*>,nor2]*>,nor3)) =
rng <*[<*x,y*>,nor2],[<*y,z*>,nor2],[<*z,x*>,nor2]*>
by CIRCCOMB:42
.=
{[<*x,y*>,nor2],[<*y,z*>,nor2],[<*z,x*>,nor2]}
by FINSEQ_2:128
;
assume A2:
( x <> [<*y,z*>,nor2] & y <> [<*z,x*>,nor2] & z <> [<*x,y*>,nor2] )
; InputVertices (GFA3CarryStr (x,y,z)) = {x,y,z}
A3:
( InnerVertices (1GateCircStr (<*[<*x,y*>,nor2],[<*y,z*>,nor2],[<*z,x*>,nor2]*>,nor3)) = {[<*[<*x,y*>,nor2],[<*y,z*>,nor2],[<*z,x*>,nor2]*>,nor3]} & {x,y,z} \ {[<*[<*x,y*>,nor2],[<*y,z*>,nor2],[<*z,x*>,nor2]*>,nor3]} = {x,y,z} )
by Lm2, CIRCCOMB:42;
A4:
{[<*x,y*>,nor2],[<*y,z*>,nor2],[<*z,x*>,nor2]} \ {[<*x,y*>,nor2],[<*y,z*>,nor2],[<*z,x*>,nor2]} = {}
by XBOOLE_1:37;
thus InputVertices (GFA3CarryStr (x,y,z)) =
((InputVertices (GFA3CarryIStr (x,y,z))) \ (InnerVertices (1GateCircStr (<*[<*x,y*>,nor2],[<*y,z*>,nor2],[<*z,x*>,nor2]*>,nor3)))) \/ ((InputVertices (1GateCircStr (<*[<*x,y*>,nor2],[<*y,z*>,nor2],[<*z,x*>,nor2]*>,nor3))) \ (InnerVertices (GFA3CarryIStr (x,y,z))))
by CIRCCMB2:5, CIRCCOMB:47
.=
{x,y,z} \/ ({[<*x,y*>,nor2],[<*y,z*>,nor2],[<*z,x*>,nor2]} \ (InnerVertices (GFA3CarryIStr (x,y,z))))
by A1, A2, A3, Th108
.=
{x,y,z} \/ {}
by A4, Th105
.=
{x,y,z}
; verum