Skip to content
Snippets Groups Projects
Commit 7ecb64e6 authored by Robbert Krebbers's avatar Robbert Krebbers
Browse files

Tweak docs of tc_finite_sn.

parent f6e466d1
No related branches found
No related tags found
No related merge requests found
Hide whitespace changes
Inline Side-by-side
Showing
with 2 additions and 2 deletions
theories/relations.v
+ 2
− 2
View file @ 7ecb64e6
...@@ -280,8 +280,8 @@ Section properties. ...@@ -280,8 +280,8 @@ Section properties.
Lemma wn_step_rtc x y : wn R y → rtc R x y → wn R x. Lemma wn_step_rtc x y : wn R y → rtc R x y → wn R x.
Proof. induction 2; eauto using wn_step. Qed. Proof. induction 2; eauto using wn_step. Qed.
(** An acyclic relation that can only take finitely many steps is strongly (** An acyclic relation that can only take finitely many steps (sometimes
normalizing *) called "globally finite") is strongly normalizing *)
Lemma tc_finite_sn x : Irreflexive (tc R) → pred_finite (tc R x) → sn R x. Lemma tc_finite_sn x : Irreflexive (tc R) → pred_finite (tc R x) → sn R x.
Proof. Proof.
intros Hirr [xs Hfin]. remember (length xs) as n eqn:Hn. intros Hirr [xs Hfin]. remember (length xs) as n eqn:Hn.
......
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