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