(**************************************************************************)
include "ground_2/notation/relations/rafter_3.ma".
-include "ground_2/relocation/rtmap_sor.ma".
include "ground_2/relocation/rtmap_istot.ma".
(* RELOCATION MAP ***********************************************************)
lemma after_tls: ∀n,f1,f2,f. @⦃0, f1⦄ ≡ n →
f1 ⊚ f2 ≡ f → ⫱*[n]f1 ⊚ f2 ≡ ⫱*[n]f.
#n elim n -n //
-#n #IH #f1 #f2 #f #Hf1 #Hf cases (at_inv_pxn … Hf1) -Hf1 [ |*: // ]
-#g1 #Hg1 #H1 cases (after_inv_nxx … Hf … H1) -Hf /2 width=1 by/
+#n #IH #f1 #f2 #f #Hf1 #Hf
+cases (at_inv_pxn … Hf1) -Hf1 [ |*: // ] #g1 #Hg1 #H1
+cases (after_inv_nxx … Hf … H1) -Hf #g #Hg #H0 destruct
+<tls_xn <tls_xn /2 width=1 by/
qed.
(* Properties on isid *******************************************************)
/4 width=5 by after_uni_next2, after_isid_sn, after_isid_dx, after_next/
qed.
-(* Inversion lemmas on sor **************************************************)
-
-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.
-(*
-lemma after_inv_sor: ∀f. 𝐅⦃f⦄ → ∀f2,f1. f2 ⊚ f1 ≡ f → ∀fa,fb. fa ⋓ fb ≡ f →
- ∃∃f1a,f1b. f2 ⊚ f1a ≡ fa & f2 ⊚ f1b ≡ fb & f1a ⋓ f1b ≡ f1.
-@isfin_ind
-[ #f #Hf #f2 #f1 #H1f #fa #fb #H2f
- elim (after_inv_isid3 … H1f) -H1f //
- elim (sor_inv_isid3 … H2f) -H2f //
- /3 width=5 by ex3_2_intro, after_isid_sn, sor_isid/
-| #f #_ #IH #f2 #f1 #H1 #fa #fb #H2
- elim (after_inv_xxp … H1) -H1 [ |*: // ] #g2 #g1 #H1f
- elim (sor_inv_xxp … H2) -H2 [ |*: // ] #ga #gb #H2f
- elim (IH … H1f … H2f) -f /3 width=11 by sor_pp, after_refl, ex3_2_intro/
-| #f #_ #IH #f2 #f1 #H1 #fa #fb #H2
- elim (sor_inv_xxn … H2) -H2 [1,3,4: * |*: // ] #ga #gb #H2f
- elim (after_inv_xxn … H1) -H1 [1,3,5,7,9,11: * |*: // ] #g2 [1,3,5: #g1 ] #H1f
- elim (IH … H1f … H2f) -f
- /3 width=11 by sor_np, sor_pn, sor_nn, after_refl, after_push, after_next, ex3_2_intro/
- #x1a #x1b #H39 #H40 #H41 #H42 #H43 #H44
- [ @ex3_2_intro
- [3: /2 width=7 by after_next/ | skip
- |5: @H41 | skip
-*)
(* Forward lemmas on at *****************************************************)
lemma after_at_fwd: ∀i,i1,f. @⦃i1, f⦄ ≡ i → ∀f2,f1. f2 ⊚ f1 ≡ f →
elim (at_inv_xxn … Hf2) -Hf2 [1,3: * |*: // ]
[ #g2 #j1 #Hg2 #H1 #H2 destruct
elim (after_inv_pnx … Hf) -Hf [ |*: // ] #g #Hg #H destruct
- /3 width=5 by after_next/
+ <tls_xn /3 width=5 by after_next/
| #g2 #Hg2 #H2 destruct
elim (after_inv_nxx … Hf) -Hf [2,3: // ] #g #Hg #H destruct
- /3 width=5 by after_next/
+ <tls_xn /3 width=5 by after_next/
]
]
qed.
elim (at_inv_xxn … Hf2) -Hf2 [1,3: * |*: // ]
[ #g2 #j1 #Hg2 #H1 #H2 destruct
elim (after_inv_pnx … Hf) -Hf [ |*: // ] #g #Hg #H destruct
- /3 width=5 by after_next/
+ <tls_xn /3 width=5 by after_next/
| #g2 #Hg2 #H2 destruct
elim (after_inv_nxx … Hf) -Hf [2,3: // ] #g #Hg #H destruct
- /3 width=5 by after_next/
+ <tls_xn /3 width=5 by after_next/
]
]
qed.