let x, y, z be set ; :: thesis: InnerVertices (GFA1AdderStr x,y,z) = {[<*x,y*>,xor2c ]} \/ {(GFA1AdderOutput x,y,z)}
set f = xor2c ;
set xy = [<*x,y*>,xor2c ];
set S = GFA1AdderStr x,y,z;
thus InnerVertices (GFA1AdderStr x,y,z) = {[<*x,y*>,xor2c ],(GFA1AdderOutput x,y,z)} by FACIRC_1:56
.= {[<*x,y*>,xor2c ]} \/ {(GFA1AdderOutput x,y,z)} by ENUMSET1:41 ; :: thesis: verum