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