Gracias Julian, igual mi duda era más por el hecho de que ponele que a vos te dan la especificación, esa función y esa demostración que puse yo, ok?, así a secas, te dan todo eso, y si te crees que está bien demostrada la correctitud, uno debería creer que todo eso anda, entonces se va a un lenguaje, pongamosle c++, y la usa. Después, resulta que si probás, (agarrás el código que puse y lo corrés, pasa lo que dije al hacer prueba(x,x) ). Mi duda era si la falla, más allá de la forma en que yo uso la función, está en el poder de expresión de nuestra especificación, o qué, porque sino me da la impresión de que puedo tener cosas, más allá de este caso, en la que demuestro que todo anda, y dps la uso, y en alguna particularidad falla por algún detalle.

En fín, lo consultaré también a los profesores cuando vuelvan las clases
Saludos

ahh, ok, igual deberias ver, que para que haya swap deben participar 2 variables, lo aclara la especificacion, y vos en este caso llamaste a la funcion prueba con una sola.
Igual, pregunta a los docentes, y publica su respuesta asi tambien nos sacas de la duda

Perdón por la necromancia, pero también me surgió la duda a mí.
Yo me convencí de que el error está en los "yE2 == y@E1".
O sea. Si decís que, ponele, "//estado 1; x = 1; //estado 2; // vale (x@estado2 == x@estado1 + 1) ^ (y@estado2 == y@estado1)", la parte donde estás mintiendo es al final. Estás diciendo que no estás cambiando y, sin embargo eso no se corresponde con el código que escribís (y la prueba tiene sentido solo si se corresponde con el código que escribís) - x e y son dos nombres distintos para la misma cosa, entonces es falso que "y@estado2 == y@estado1". La confusión está en que en ningún momento se menciona a y explícitamente, sin embargo cambia. Es como imaginarse que haya, al final de cada estado, un , y ahí se vería clara la contradicción.