Commit 7adcba8f authored by Ralf Jung's avatar Ralf Jung

add a comment to final erasure theorem

parent 01c5924b
Pipeline #21427 failed with stage
in 33 minutes and 13 seconds
......@@ -741,6 +741,7 @@ Proof.
- right; eauto using reducible_no_obs_reducible.
Qed.
(** This is the top-level erasure theorem: erasure preserves adequacy. *)
Theorem erasure e σ φ :
adequate NotStuck e σ φ
adequate NotStuck (erase_expr e) (erase_state σ)
......
Markdown is supported
0% or .
You are about to add 0 people to the discussion. Proceed with caution.
Finish editing this message first!
Please register or to comment