- improved lfpr_lfpr

[helm.git] / matita / matita / contribs / lambdadelta / ground_2 / relocation / rtmap_sor.ma

diff --git a/matita/matita/contribs/lambdadelta/ground_2/relocation/rtmap_sor.ma b/matita/matita/contribs/lambdadelta/ground_2/relocation/rtmap_sor.ma
index 2a616742ccafe9f67b238217a9b38bab5aa5cf81..bc2a7dda6efd52eb61c36537bf43a5fdf8484e59 100644 (file)
--- a/matita/matita/contribs/lambdadelta/ground_2/relocation/rtmap_sor.ma
+++ b/matita/matita/contribs/lambdadelta/ground_2/relocation/rtmap_sor.ma
@@ -323,6 +323,18 @@ qed.
 lemma sor_isid: ∀f1,f2,f. 𝐈⦃f1⦄ → 𝐈⦃f2⦄ → 𝐈⦃f⦄ → f1 ⋓ f2 ≡ f.
 /4 width=3 by sor_eq_repl_back2, sor_eq_repl_back1, isid_inv_eq_repl/ qed.
 
+(* Inversion lemmas with tail ***********************************************)
+
+lemma sor_inv_tl_sn: ∀f1,f2,f. ⫱f1 ⋓ f2 ≡ f → f1 ⋓ ⫯f2 ≡ ⫯f.
+#f1 #f2 #f elim (pn_split f1) *
+#g1 #H destruct /2 width=7 by sor_pn, sor_nn/
+qed-.
+
+lemma sor_inv_tl_dx: ∀f1,f2,f. f1 ⋓ ⫱f2 ≡ f → ⫯f1 ⋓ f2 ≡ ⫯f.
+#f1 #f2 #f elim (pn_split f2) *
+#g2 #H destruct /2 width=7 by sor_np, sor_nn/
+qed-.
+
 (* Inversion lemmas with test for identity **********************************)
 
 lemma sor_isid_inv_sn: ∀f1,f2,f. f1 ⋓ f2 ≡ f → 𝐈⦃f1⦄ → f2 ≗ f.
@@ -438,6 +450,8 @@ lemma sor_inv_sle_sn_trans: ∀f1,f2,f. f1 ⋓ f2 ≡ f → ∀g. g ⊆ f1 → g
 lemma sor_inv_sle_dx_trans: ∀f1,f2,f. f1 ⋓ f2 ≡ f → ∀g. g ⊆ f2 → g ⊆ f.
 /3 width=4 by sor_inv_sle_dx, sle_trans/ qed-.
 
+axiom sor_inv_sle: ∀f1,f2,f. f1 ⋓ f2 ≡ f → ∀g. f1 ⊆ g → f2 ⊆ g → f ⊆ g.
+
 (* Properties with inclusion ************************************************)
 
 corec lemma sor_sle_dx: ∀f1,f2. f1 ⊆ f2 → f1 ⋓ f2 ≡ f2.