- paths and left residuals: third case of the equivalence proved!

[helm.git] / matita / matita / contribs / lambda / paths / standard_trace.ma

diff --git a/matita/matita/contribs/lambda/paths/standard_trace.ma b/matita/matita/contribs/lambda/paths/standard_trace.ma
index 0550ab24f01e28b02b1b60fd97989259ad535d28..edc77df25abea3ac108eca5a6b1708095f3bd7a6 100644 (file)
--- a/matita/matita/contribs/lambda/paths/standard_trace.ma
+++ b/matita/matita/contribs/lambda/paths/standard_trace.ma
@@ -28,6 +28,10 @@ lemma is_standard_fwd_cons: ∀p,s. is_standard (p::s) → is_standard s.
 /2 width=2 by Allr_fwd_cons/
 qed-.
 
+lemma is_standard_fwd_append_dx: ∀s,r. is_standard (s@r) → is_standard r.
+/2 width=2 by Allr_fwd_append_dx/
+qed-.
+
 lemma is_standard_compatible: ∀o,s. is_standard s → is_standard (o:::s).
 #o #s elim s -s // #p * //
 #q #s #IHs * /3 width=1/
@@ -43,6 +47,29 @@ lemma is_standard_append: ∀r. is_standard r → ∀s. is_standard s → is_sta
 #q #r #IHr * /3 width=1/
 qed.
 
+lemma is_standard_inv_compatible_sn: ∀s. is_standard (sn:::s) → is_standard s.
+#s elim s -s // #a1 * // #a2 #s #IHs * #H
+elim (sle_inv_sn … H ??) -H [3: // |2: skip ] (**) (* simplify line *)
+#a #Ha1 #H destruct /3 width=1/
+qed-.
+
+lemma is_standard_inv_compatible_rc: ∀s. is_standard (rc:::s) → is_standard s.
+#s elim s -s // #a1 * // #a2 #s #IHs * #H
+elim (sle_inv_rc … H ??) -H [4: // |2: skip ] * (**) (* simplify line *)
+[ #a #Ha1 #H destruct /3 width=1/
+| #a #H destruct
+]
+qed-.
+
+lemma is_standard_inv_compatible_dx: ∀s. is_standard (dx:::s) →
+                                     is_inner s → is_standard s.
+#s elim s -s // #a1 * // #a2 #s #IHs * #H
+elim (sle_inv_dx … H ??) -H [4: // |3: skip ] (**) (* simplify line *)
+[ * #_ #H1a1 #_ * #H2a1 #_ -IHs
+  elim (H2a1 ?) -H2a1 -a2 -s //
+| * #a #Ha2 #H destruct #H * #_ /3 width=1/
+qed-.
+
 lemma is_standard_fwd_sle: ∀s2,p2,s1,p1. is_standard ((p1::s1)@(p2::s2)) → p1 ≤ p2.
 #s2 #p2 #s1 elim s1 -s1
 [ #p1 * //
@@ -72,3 +99,8 @@ lapply (is_standard_fwd_cons … H)
 lapply (is_standard_fwd_sle … H) #Hqp
 lapply (sle_fwd_in_whd … Hqp Hp) /3 width=1/
 qed-.
+
+lemma is_standard_fwd_in_inner: ∀s,p. is_standard (p::s) → in_inner p → is_inner s.
+#s elim s -s // #q #s #IHs #p * #Hpq #Hs #Hp
+lapply (sle_fwd_in_inner … Hpq ?) // -p /3 width=3/
+qed.