let x, y, z be set ; :: thesis: ( x <> [<*y,z*>,and2b] & y <> [<*z,x*>,and2b] & z <> [<*x,y*>,and2b] implies InputVertices (GFA3CarryStr (x,y,z)) = {x,y,z} )
set f1 = and2b ;
set f2 = and2b ;
set f3 = and2b ;
set f4 = nor3 ;
set xy = [<*x,y*>,and2b];
set yz = [<*y,z*>,and2b];
set zx = [<*z,x*>,and2b];
set xyz = [<*[<*x,y*>,and2b],[<*y,z*>,and2b],[<*z,x*>,and2b]*>,nor3];
set S = 1GateCircStr (<*[<*x,y*>,and2b],[<*y,z*>,and2b],[<*z,x*>,and2b]*>,nor3);
set MI = GFA3CarryIStr (x,y,z);
A1: InputVertices (1GateCircStr (<*[<*x,y*>,and2b],[<*y,z*>,and2b],[<*z,x*>,and2b]*>,nor3)) = rng <*[<*x,y*>,and2b],[<*y,z*>,and2b],[<*z,x*>,and2b]*> by CIRCCOMB:49
.= {[<*x,y*>,and2b],[<*y,z*>,and2b],[<*z,x*>,and2b]} by FINSEQ_2:148 ;
assume A2: ( x <> [<*y,z*>,and2b] & y <> [<*z,x*>,and2b] & z <> [<*x,y*>,and2b] ) ; :: thesis: InputVertices (GFA3CarryStr (x,y,z)) = {x,y,z}
A3: ( InnerVertices (1GateCircStr (<*[<*x,y*>,and2b],[<*y,z*>,and2b],[<*z,x*>,and2b]*>,nor3)) = {[<*[<*x,y*>,and2b],[<*y,z*>,and2b],[<*z,x*>,and2b]*>,nor3]} & {x,y,z} \ {[<*[<*x,y*>,and2b],[<*y,z*>,and2b],[<*z,x*>,and2b]*>,nor3]} = {x,y,z} ) by Lm2, CIRCCOMB:49;
A4: {[<*x,y*>,and2b],[<*y,z*>,and2b],[<*z,x*>,and2b]} \ {[<*x,y*>,and2b],[<*y,z*>,and2b],[<*z,x*>,and2b]} = {} by XBOOLE_1:37;
thus InputVertices (GFA3CarryStr (x,y,z)) = ((InputVertices (GFA3CarryIStr (x,y,z))) \ (InnerVertices (1GateCircStr (<*[<*x,y*>,and2b],[<*y,z*>,and2b],[<*z,x*>,and2b]*>,nor3)))) \/ ((InputVertices (1GateCircStr (<*[<*x,y*>,and2b],[<*y,z*>,and2b],[<*z,x*>,and2b]*>,nor3))) \ (InnerVertices (GFA3CarryIStr (x,y,z)))) by CIRCCMB2:6, CIRCCOMB:55
.= {x,y,z} \/ ({[<*x,y*>,and2b],[<*y,z*>,and2b],[<*z,x*>,and2b]} \ (InnerVertices (GFA3CarryIStr (x,y,z)))) by A1, A2, A3, Th126
.= {x,y,z} \/ {} by A4, Th123
.= {x,y,z} ; :: thesis: verum