non associative with precedence 45
for @{ 'HApStar $M $p $N }.
-lemma lhap1_lhap: ∀p,M1,M2. M1 ⓗ⇀[p] M2 → M1 ⓗ⇀*[p::◊] M2.
+lemma lhap_step_rc: ∀p,M1,M2. M1 ⓗ⇀[p] M2 → M1 ⓗ⇀*[p::◊] M2.
/2 width=1/
qed.
/2 width=3 by lstar_inv_cons/
qed-.
-lemma lhap_inv_lhap1: ∀p,M1,M2. M1 ⓗ⇀*[p::◊] M2 → M1 ⓗ⇀[p] M2.
+lemma lhap_inv_step_rc: ∀p,M1,M2. M1 ⓗ⇀*[p::◊] M2 → M1 ⓗ⇀[p] M2.
/2 width=1 by lstar_inv_step/
qed-.
+lemma lhap_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 lhap_compatible_dx: ho_compatible_dx lhap.
+/3 width=1/
+qed.
+
lemma lhap_lift: ∀s. liftable (lhap s).
/2 width=1/
qed.
/3 width=7 by lstar_singlevalued, lhap1_mono/
qed-.
-theorem lhap_trans: ∀s1,M1,M. M1 ⓗ⇀*[s1] M →
- ∀s2,M2. M ⓗ⇀*[s2] M2 → M1 ⓗ⇀*[s1@s2] M2.
-/2 width=3 by lstar_trans/
+theorem lhap_trans: ltransitive … lhap.
+/2 width=3 by lstar_ltransitive/
qed-.
-lemma lhap_appl: ∀s,B,A1,A2. A1 ⓗ⇀*[s] A2 → @B.A1 ⓗ⇀*[dx:::s] @B.A2.
-#s #B #A1 #A2 #H @(lstar_ind_l ????????? H) -s -A1 // /3 width=3/
-qed.
+lemma lhap_step_dx: ∀s,M1,M. M1 ⓗ⇀*[s] M →
+ ∀p,M2. M ⓗ⇀[p] M2 → M1 ⓗ⇀*[s@p::◊] M2.
+#s #M1 #M #HM1 #p #M2 #HM2
+@(lhap_trans … HM1) /2 width=1/
+qed-.
lemma head_lsreds_lhap: ∀s,M1,M2. M1 ⇀*[s] M2 → is_head s → M1 ⓗ⇀*[s] M2.
#s #M1 #M2 #H @(lstar_ind_l ????????? H) -s -M1 //
#p #s #M1 #M #HM1 #_ #IHM2
lapply (lhap1_inv_lsred … HM1) -HM1 /2 width=3/
qed-.
-
-lemma lhap_fwd_le: ∀s,M1,M2. M1 ⓗ⇀*[s] M2 → is_le s.
-#s #M1 #M2 #H @(lstar_ind_l ????????? H) -s -M1 /3 width=3/
-#a1 #s #M1 #M #HM1 #IHM1
-generalize in match HM1; -HM1
-cases IHM1 -s -M -M2 //
-#a #M0 #M #HM0 #s #M2 #_ #HM10 #H -M2
-lapply (lhap1_fwd_le … HM10 … HM0) -M -M0 -M1 /2 width=1/
-qed-.