Buenas,
Estoy intentando resolver esta parte tomando la sugerencia de https://eva.fing.edu.uy/mod/forum/discuss.php?d=222338.
El problema es que cuando llego al paso inductivo tengo:
1 goal
m1, m2, m3 : Memoria
n1, n2 : nat
i : Instr
Hr12 : Execute (repeatI (S n1) i) m1 m2
Hr23 : Execute (repeatI n2 i) m2 m3
IHn1 : Execute (repeatI n1 i) m1 m2 -> Execute (repeatI (n1 + n2) i) m1 m3
______________________________________(1/1)
Execute (repeatI (S (n1 + n2)) i) m1 m3
La hipotesis inductiva no me sirve de mucho ya que si se cumple Hr12 entonces no se cumple la primera parte de la hipótesis inductiva (salvo para el caso m1=m2=m3).
Aplicando inversion y el constructor de repeat llego a:
1 goal
m1, m2, m3 : Memoria
n1, n2 : nat
i : Instr
Hr23 : Execute (repeatI n2 i) m2 m3
IHn1 : Execute (repeatI n1 i) m1 m2 -> Execute (repeatI (n1 + n2) i) m1 m3
m4 : Memoria
H : Execute i m1 m4
H0 : Execute (repeatI n1 i) m4 m2
______________________________________(1/1)
Execute (repeatI (n1 + n2) i) m4 m3
Que es volver al comienzo (m4 en vez de m1) y la hipotesis inductiva no me sirve.
Agradezco la ayuda.
Saludos.