let x, y, z be set ; :: thesis: InnerVertices (GFA2AdderStr x,y,z) = {[<*x,y*>,xor2c ]} \/ {(GFA2AdderOutput x,y,z)}
set S2 = GFA2AdderStr x,y,z;
set A2 = GFA2AdderOutput x,y,z;
set S1 = GFA1AdderStr x,y,z;
set A1 = GFA1AdderOutput x,y,z;
GFA2AdderOutput x,y,z = GFA1AdderOutput x,y,z ;
hence InnerVertices (GFA2AdderStr x,y,z) = {[<*x,y*>,xor2c ]} \/ {(GFA2AdderOutput x,y,z)} by Th63; :: thesis: verum