Hola, me parece un poco rara la siguiente regla, no hace referencia a la memoria inicial, es acaso delta 1? como es en el caso de xWhileTrue.
Hola.
La regla está bien y si, delta1 es la memoria inicial.
En palabras:
SI ejecutar la instrucción del cuerpo del repeat a partir de una memoria m1 produce una memoria m2 y ejecutar luego n veces dicha instrucción (repeat con n) a partir de m2 produce una memoria m3,
ENTONCES ejecutar n+1 veces dicha instrucción (repeat con n+1) a partir de m1 produce una memoria m3,
Saludos, Carlos