-interpretation "labelled sequential computation"
- 'SeqRedStar M s N = (lsreds s M N).
-
-notation "hvbox( M break ↦* [ term 46 s ] break term 46 N )"
- non associative with precedence 45
- for @{ 'SeqRedStar $M $s $N }.
-
-lemma lsreds_refl: reflexive … (lsreds (◊)).
-//
-qed.
-
-lemma lsreds_step_sn: ∀p,M1,M. M1 ↦[p] M → ∀s,M2. M ↦*[s] M2 → M1 ↦*[p::s] M2.
-/2 width=3/
-qed-.
-
-lemma lsreds_step_dx: ∀s,M1,M. M1 ↦*[s] M → ∀p,M2. M ↦[p] M2 → M1 ↦*[s@p::◊] M2.
-/2 width=3/
-qed-.
-
-lemma lsreds_step_rc: ∀p,M1,M2. M1 ↦[p] M2 → M1 ↦*[p::◊] M2.
-/2 width=1/
-qed.
-
-lemma lsreds_inv_nil: ∀s,M1,M2. M1 ↦*[s] M2 → ◊ = s → M1 = M2.
-/2 width=5 by lstar_inv_nil/
-qed-.
-
-lemma lsreds_inv_cons: ∀s,M1,M2. M1 ↦*[s] M2 → ∀q,r. q::r = s →
- ∃∃M. M1 ↦[q] M & M ↦*[r] M2.
-/2 width=3 by lstar_inv_cons/
-qed-.
-
-lemma lsreds_inv_step_rc: ∀p,M1,M2. M1 ↦*[p::◊] M2 → M1 ↦[p] M2.
-/2 width=1 by lstar_inv_step/
-qed-.
-
-lemma lsreds_inv_pos: ∀s,M1,M2. M1 ↦*[s] M2 → 0 < |s| →
- ∃∃p,r,M. p::r = s & M1 ↦[p] M & M ↦*[r] M2.
-/2 width=1 by lstar_inv_pos/
-qed-.
-
-lemma lsred_compatible_rc: ho_compatible_rc lsreds.
-/3 width=1/
-qed.
-
-lemma lsreds_compatible_sn: ho_compatible_sn lsreds.
-/3 width=1/
-qed.
-
-lemma lsreds_compatible_dx: ho_compatible_dx lsreds.
-/3 width=1/
-qed.
-
-lemma lsreds_lift: ∀s. liftable (lsreds s).
-/2 width=1/
-qed.
-
-lemma lsreds_inv_lift: ∀s. deliftable_sn (lsreds s).
-/3 width=3 by lstar_deliftable_sn, lsred_inv_lift/
+lemma sreds_l_sreds: ∀S,R. (∀M,N. M ↦ N → ∃a. R a M N) →
+ ∀M,N. M ↦* N → ∃l. l_sreds S R l M N.
+#S #R #HR #M #N #H elim H -N
+[ #N #N0 #_ #HN0 * #l #HMN
+ elim (HR … HN0) -HR -HN0 /3 width=5/
+| /2 width=2/
+]