theorem :: GFACIRC1:110
for x, y, z being non pair set holds InputVertices (GFA3CarryStr (x,y,z)) is without_pairs