Buenas, sobre la notación en estos apartados del ejercicio 7.
En ambos enunciados las hipotesis tienen una lista de instrucciones
7.4 : ((If c Then p Else Skip); While c Do p, mem) » mem' -> (While c Do p, mem) » mem'
7.5 (i;(Repeat n i), mem1) » mem2 -> (Repeat n+1 i, mem1) » mem2
Mi duda es si debemos tomarlo como bloques BeginEnd o objetos de tipo LInstr. Ya que de ser lo segundo no coinciden con el tipo de la relación Execute : Instr -> Memoria -> Memoria -> Prop.
Gracias, Saludos.