Buenas,
Estoy tratando de probar one_step_preserves_prop_iii. Lo estoy haciendo por inducción en la acción a.
Estoy en el caso del write y lo que me está costando en particular es probar que se cumple trusted_os ctxt s a partir de trusted_os ctxt s' .
Yo por cierto one-step execution lo definí como
Definition one_step s a s' := valid_state s /\ Pre s a /\ Post s a s'
valid_state(s) Pre s a Post s a s'
----------------------------------------
a ⇒ s ↪ s'
Voy bien encaminado? Alguna idea para lo de trusted_os ctxt ?
Saludos!