Hola Tomás.
Podés escribir por ejemplo:
... exists (ma : madd) (p : page), va_mapped_to_ma s va ma /\ memory s ma = Some p /\ is_RW (page_content p) ...
Saludos, Caros
Hola Tomás.
Podés escribir por ejemplo:
... exists (ma : madd) (p : page), va_mapped_to_ma s va ma /\ memory s ma = Some p /\ is_RW (page_content p) ...
Saludos, Caros