Здравствуйте дорогие участники русскоязычного форума!
Застряла на самой последней задаче в главе:
https://softwarefoundations.cis.upenn.edu/current/plf-current/Equiv.html
не могу понять, что за свойство такое.
(* REPLACE THIS LINE WITH ":= _your_definition_ ." *). Admitted.
Theorem zprop_preserving : ∀c c',
zprop c → capprox c c' → zprop c'.
Proof. (* FILL IN HERE *) Admitted.```
Это точно не "неравество стейтов... " уже на E_Ass становится понятно, что стейты могут быть равны...
Definition zprop (c : com) : Prop := forall (st st' : state),
st =[ c ]-> st' -> st <> st'.
Что ж это тогда... ? Может кто-то решал эту задачу, поделитесь решением или намекните, как свойство узреть.
Спасибо!