set f1 = and2b ;
set f2 = and2b ;
set f3 = and2b ;
set f4 = nor3 ;
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 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: InnerVertices (1GateCircStr <*[<*x,y*>,and2b ],[<*y,z*>,and2b ],[<*z,x*>,and2b ]*>,nor3 ) = {[<*[<*x,y*>,and2b ],[<*y,z*>,and2b ],[<*z,x*>,and2b ]*>,nor3 ]} by CIRCCOMB:49;
A2: 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 A3: ( x <> [<*y,z*>,and2b ] & y <> [<*z,x*>,and2b ] & z <> [<*x,y*>,and2b ] ) ; :: thesis: InputVertices (GFA3CarryStr x,y,z) = {x,y,z}
A4: {x,y,z} \ {[<*[<*x,y*>,and2b ],[<*y,z*>,and2b ],[<*z,x*>,and2b ]*>,nor3 ]} = {x,y,z} by Lm2;
A5: {[<*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, A4, Th126
.= {x,y,z} \/ {} by A5, Th123
.= {x,y,z} ; :: thesis: verum