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