Commit 005887ee authored by Robbert Krebbers's avatar Robbert Krebbers

Show that accessible elements do not loop.

parent 498fe5f9
Pipeline #13187 passed with stage
in 14 minutes and 49 seconds
......@@ -171,6 +171,9 @@ Section rtc.
Lemma tc_rtc x y : tc R x y rtc R x y.
Proof. induction 1; eauto. Qed.
Lemma acc_not_ex_loop x : Acc (flip R) x ¬ex_loop R x.
Proof. unfold not. induction 1; destruct 1; eauto. Qed.
Lemma all_loop_red x : all_loop R x red R x.
Proof. destruct 1; auto. Qed.
Lemma all_loop_step x y : all_loop R x R x y all_loop R y.
Markdown is supported
You are about to add 0 people to the discussion. Proceed with caution.
Finish editing this message first!
Please register or to comment