include "ground_2/relocation/rtmap_id.ma".
include "basic_2/notation/relations/relationstar_4.ma".
-include "basic_2/grammar/ceq.ma".
include "basic_2/relocation/lexs.ma".
include "basic_2/static/frees.ma".
interpretation "generic extension on referred entries (local environment)"
'RelationStar R T L1 L2 = (lfxs R T L1 L2).
-definition R_confluent_lfxs: relation4 (relation3 lenv term term)
- (relation3 lenv term term) … ≝
- λR1,R2,RP1,RP2.
- ∀L0,T0,T1. R1 L0 T0 T1 → ∀T2. R2 L0 T0 T2 →
- ∀L1. L0 ⦻*[RP1, T0] L1 → ∀L2. L0 ⦻*[RP2, T0] L2 →
- ∃∃T. R2 L1 T1 T & R1 L2 T2 T.
+definition R_frees_confluent: predicate (relation3 lenv term term) ≝
+ λRN.
+ ∀f1,L,T1. L ⊢ 𝐅*⦃T1⦄ ≡ f1 → ∀T2. RN L T1 T2 →
+ ∃∃f2. L ⊢ 𝐅*⦃T2⦄ ≡ f2 & f2 ⊆ f1.
+
+definition lexs_frees_confluent: relation (relation3 lenv term term) ≝
+ λRN,RP.
+ ∀f1,L1,T. L1 ⊢ 𝐅*⦃T⦄ ≡ f1 →
+ ∀L2. L1 ⦻*[RN, RP, f1] L2 →
+ ∃∃f2. L2 ⊢ 𝐅*⦃T⦄ ≡ f2 & f2 ⊆ f1.
+
+definition R_confluent2_lfxs: relation4 (relation3 lenv term term)
+ (relation3 lenv term term) … ≝
+ λR1,R2,RP1,RP2.
+ ∀L0,T0,T1. R1 L0 T0 T1 → ∀T2. R2 L0 T0 T2 →
+ ∀L1. L0 ⦻*[RP1, T0] L1 → ∀L2. L0 ⦻*[RP2, T0] L2 →
+ ∃∃T. R2 L1 T1 T & R1 L2 T2 T.
(* Basic properties ***********************************************************)
#R1 #R2 #HR #L1 #L2 #T * /4 width=7 by lexs_co, ex2_intro/
qed-.
-lemma pippo: ∀R1,R2,RP1,RP2. R_confluent_lfxs R1 R2 RP1 RP2 →
- lexs_confluent R1 R2 RP1 cfull RP2 cfull.
-#R1 #R2 #RP1 #RP2 #HR #f #L0 #T0 #T1 #HT01 #T2 #HT02 #L1 #HL01 #L2 #HL02
-
(* Basic inversion lemmas ***************************************************)
lemma lfxs_inv_atom_sn: ∀R,I,Y2. ⋆ ⦻*[R, ⓪{I}] Y2 → Y2 = ⋆.