+++ /dev/null
-(**************************************************************************)
-(* ___ *)
-(* ||M|| *)
-(* ||A|| A project by Andrea Asperti *)
-(* ||T|| *)
-(* ||I|| Developers: *)
-(* ||T|| The HELM team. *)
-(* ||A|| http://helm.cs.unibo.it *)
-(* \ / *)
-(* \ / This file is distributed under the terms of the *)
-(* v GNU General Public License Version 2 *)
-(* *)
-(**************************************************************************)
-
-include "basic_2/syntax/lenv.ma".
-
-(* CONTEXT-SENSITIVE EQUIVALENCES FOR TERMS *********************************)
-
-definition ceq: relation3 lenv term term ≝ λL,T1,T2. T1 = T2.
-
-definition cfull: relation3 lenv term term ≝ λL,T1,T2. ⊤.
-
-(* Basic properties *********************************************************)
-
-lemma ceq_refl (L): reflexive … (ceq L).
-// qed.
-
-lemma cfull_refl (L): reflexive … (cfull L).
-// qed.
-
-lemma ceq_sym (L): symmetric … (ceq L).
-// qed-.
-
-lemma cfull_sym (L): symmetric … (cfull L).
-// qed-.
-
-lemma cfull_top (R:relation3 lenv term term) (L) (T1) (T2):
- R L T1 T2 → cfull L T1 T2.
-// qed-.
-
-lemma ceq_cfull (L) (T1) (T2): ceq L T1 T2 → cfull L T1 T2.
-// qed.
+++ /dev/null
-(**************************************************************************)
-(* ___ *)
-(* ||M|| *)
-(* ||A|| A project by Andrea Asperti *)
-(* ||T|| *)
-(* ||I|| Developers: *)
-(* ||T|| The HELM team. *)
-(* ||A|| http://helm.cs.unibo.it *)
-(* \ / *)
-(* \ / This file is distributed under the terms of the *)
-(* v GNU General Public License Version 2 *)
-(* *)
-(**************************************************************************)
-
-include "basic_2/syntax/ceq.ma".
-
-(* CONTEXT-SENSITIVE EQUIVALENCES FOR TERMS *********************************)
-
-(* Main properties **********************************************************)
-
-theorem ceq_trans (L): Transitive … (ceq L).
-// qed-.
-
-lemma ceq_canc_sn (L): left_cancellable … (ceq L).
-// qed-.
-
-lemma ceq_canc_dx (L): right_cancellable … (ceq L).
-// qed-.
-
-theorem cfull_trans (L): Transitive … (cfull L).
-// qed-.
-
-lemma cfull_canc_sn (L): left_cancellable … (cfull L).
-// qed-.
-
-lemma cfull_canc_dx (L): right_cancellable … (cfull L).
-// qed-.
\ No newline at end of file
--- /dev/null
+(**************************************************************************)
+(* ___ *)
+(* ||M|| *)
+(* ||A|| A project by Andrea Asperti *)
+(* ||T|| *)
+(* ||I|| Developers: *)
+(* ||T|| The HELM team. *)
+(* ||A|| http://helm.cs.unibo.it *)
+(* \ / *)
+(* \ / This file is distributed under the terms of the *)
+(* v GNU General Public License Version 2 *)
+(* *)
+(**************************************************************************)
+
+include "basic_2/substitution/drop_lreq.ma".
+include "basic_2/reduction/cpx.ma".
+
+(* UNCOUNTED CONTEXT-SENSITIVE PARALLEL RT-TRANSITION FOR TERMS *************)
+
+(* Properties on equivalence for local environments *************************)
+
+lemma lreq_cpx_trans: ∀h,o,G. lsub_trans … (cpx h o G) (lreq 0 (∞)).
+#h #o #G #L1 #T1 #T2 #H elim H -G -L1 -T1 -T2
+[ //
+| /2 width=2 by cpx_st/
+| #I #G #L1 #K1 #V1 #V2 #W2 #i #HLK1 #_ #HVW2 #IHV12 #L2 #HL12
+ elim (lreq_drop_trans_be … HL12 … HLK1) // -HL12 -HLK1 /3 width=7 by cpx_delta/
+|4,9: /4 width=1 by cpx_bind, cpx_beta, lreq_pair_O_Y/
+|5,7,8: /3 width=1 by cpx_flat, cpx_eps, cpx_ct/
+|6,10: /4 width=3 by cpx_zeta, cpx_theta, lreq_pair_O_Y/
+]
+qed-.
--- /dev/null
+(**************************************************************************)
+(* ___ *)
+(* ||M|| *)
+(* ||A|| A project by Andrea Asperti *)
+(* ||T|| *)
+(* ||I|| Developers: *)
+(* ||T|| The HELM team. *)
+(* ||A|| http://helm.cs.unibo.it *)
+(* \ / *)
+(* \ / This file is distributed under the terms of the *)
+(* v GNU General Public License Version 2 *)
+(* *)
+(**************************************************************************)
+
+(* NOTATION FOR THE FORMAL SYSTEM λδ ****************************************)
+
+notation "hvbox( ⦃ term 46 G , break term 46 L ⦄ ⊢ break term 46 T1 break ▶ [ term 46 l , break term 46 m ] break term 46 T2 )"
+ non associative with precedence 45
+ for @{ 'PSubst $G $L $T1 $l $k $T2 }.
--- /dev/null
+(**************************************************************************)
+(* ___ *)
+(* ||M|| *)
+(* ||A|| A project by Andrea Asperti *)
+(* ||T|| *)
+(* ||I|| Developers: *)
+(* ||T|| The HELM team. *)
+(* ||A|| http://helm.cs.unibo.it *)
+(* \ / *)
+(* \ / This file is distributed under the terms of the *)
+(* v GNU General Public License Version 2 *)
+(* *)
+(**************************************************************************)
+
+(* NOTATION FOR THE FORMAL SYSTEM λδ ****************************************)
+
+notation "hvbox( ⦃ term 46 G , break term 46 L ⦄ ⊢ break term 46 T1 break ▶ * [ term 46 l , break term 46 m ] break term 46 T2 )"
+ non associative with precedence 45
+ for @{ 'PSubstStar $G $L $T1 $l $k $T2 }.
--- /dev/null
+(**************************************************************************)
+(* ___ *)
+(* ||M|| *)
+(* ||A|| A project by Andrea Asperti *)
+(* ||T|| *)
+(* ||I|| Developers: *)
+(* ||T|| The HELM team. *)
+(* ||A|| http://helm.cs.unibo.it *)
+(* \ / *)
+(* \ / This file is distributed under the terms of the *)
+(* v GNU General Public License Version 2 *)
+(* *)
+(**************************************************************************)
+
+(* NOTATION FOR THE FORMAL SYSTEM λδ ****************************************)
+
+notation "hvbox( ⦃ term 46 G , break term 46 L ⦄ ⊢ break term 46 T1 break ▶ ▶ * [ term 46 l , break term 46 m ] break term 46 T2 )"
+ non associative with precedence 45
+ for @{ 'PSubstStarAlt $G $L $T1 $l $k $T2 }.
+++ /dev/null
-(**************************************************************************)
-(* ___ *)
-(* ||M|| *)
-(* ||A|| A project by Andrea Asperti *)
-(* ||T|| *)
-(* ||I|| Developers: *)
-(* ||T|| The HELM team. *)
-(* ||A|| http://helm.cs.unibo.it *)
-(* \ / *)
-(* \ / This file is distributed under the terms of the *)
-(* v GNU General Public License Version 2 *)
-(* *)
-(**************************************************************************)
-
-(* NOTATION FOR THE FORMAL SYSTEM λδ ****************************************)
-
-notation "hvbox( ⫱ * [ term 46 L , break term 46 K ] term 46 f )"
- non associative with precedence 46
- for @{ 'DropPreds $L $K $f }.
--- /dev/null
+(**************************************************************************)
+(* ___ *)
+(* ||M|| *)
+(* ||A|| A project by Andrea Asperti *)
+(* ||T|| *)
+(* ||I|| Developers: *)
+(* ||T|| The HELM team. *)
+(* ||A|| http://helm.cs.unibo.it *)
+(* \ / *)
+(* \ / This file is distributed under the terms of the *)
+(* v GNU General Public License Version 2 *)
+(* *)
+(**************************************************************************)
+
+include "basic_2/unfold/lstas_da.ma".
+include "basic_2/reduction/cpx_lift.ma".
+include "basic_2/reduction/fpb.ma".
+
+(* "RST" PROPER PARALLEL COMPUTATION FOR CLOSURES ***************************)
+
+(* Advanced properties ******************************************************)
+
+lemma sta_fpb: ∀h,o,G,L,T1,T2,d. ⦃G, L⦄ ⊢ T1 ▪[h, o] d+1 →
+ ⦃G, L⦄ ⊢ T1 •*[h, 1] T2 → ⦃G, L, T1⦄ ≻[h, o] ⦃G, L, T2⦄.
+#h #o #G #L #T1 #T2 #d #HT1 #HT12 elim (eq_term_dec T1 T2)
+/3 width=2 by fpb_cpx, sta_cpx/ #H destruct
+elim (lstas_inv_refl_pos h G L T2 0) //
+qed.
--- /dev/null
+(**************************************************************************)
+(* ___ *)
+(* ||M|| *)
+(* ||A|| A project by Andrea Asperti *)
+(* ||T|| *)
+(* ||I|| Developers: *)
+(* ||T|| The HELM team. *)
+(* ||A|| http://helm.cs.unibo.it *)
+(* \ / *)
+(* \ / This file is distributed under the terms of the *)
+(* v GNU General Public License Version 2 *)
+(* *)
+(**************************************************************************)
+
+include "basic_2/reduction/cpx_lift.ma".
+include "basic_2/reduction/fpbq.ma".
+
+(* "QRST" PARALLEL REDUCTION FOR CLOSURES ***********************************)
+
+(* Advanced properties ******************************************************)
+
+lemma sta_fpbq: ∀h,o,G,L,T1,T2,d.
+ ⦃G, L⦄ ⊢ T1 ▪[h, o] d+1 → ⦃G, L⦄ ⊢ T1 •*[h, 1] T2 →
+ ⦃G, L, T1⦄ ≽[h, o] ⦃G, L, T2⦄.
+/3 width=4 by fpbq_cpx, sta_cpx/ qed.
+++ /dev/null
-(**************************************************************************)
-(* ___ *)
-(* ||M|| *)
-(* ||A|| A project by Andrea Asperti *)
-(* ||T|| *)
-(* ||I|| Developers: *)
-(* ||T|| The HELM team. *)
-(* ||A|| http://helm.cs.unibo.it *)
-(* \ / *)
-(* \ / This file is distributed under the terms of the *)
-(* v GNU General Public License Version 2 *)
-(* *)
-(**************************************************************************)
-
-(* NOTATION FOR THE FORMAL SYSTEM λδ ****************************************)
-
-notation "hvbox( L1 ⋓ break [ term 46 T , break term 46 f ] break term 46 L2 ≡ break term 46 L )"
- non associative with precedence 45
- for @{ 'LazyOr $L1 $T $f $L2 $L }.
+++ /dev/null
-(**************************************************************************)
-(* ___ *)
-(* ||M|| *)
-(* ||A|| A project by Andrea Asperti *)
-(* ||T|| *)
-(* ||I|| Developers: *)
-(* ||T|| The HELM team. *)
-(* ||A|| http://helm.cs.unibo.it *)
-(* \ / *)
-(* \ / This file is distributed under the terms of the *)
-(* v GNU General Public License Version 2 *)
-(* *)
-(**************************************************************************)
-
-include "basic_2/rt_transition/lfpr_lfpr.ma".
-
-(* PARALLEL R-TRANSITION FOR LOCAL ENV.S ON REFERRED ENTRIES ****************)
-
-definition lfxs_confluent_R: relation2 … ≝
- λRP1,RP2.
- ∀L0,T0,T1. RP1 L0 T0 T1 → ∀T2. RP2 L0 T0 T2 →
- ∀L1. L0 ⦻*[RP1, T0] L1 → ∀L2. L0 ⦻*[RP2, T0] L2 →
- ∃∃L. L1 ⦻*[RP2, T1] L & L2 ⦻*[RP1, T2] L.
-
-(* Main properties **********************************************************)
-
-fact lfpr_conf_cpr_atom_atom:
- ∀h,I,G,L0. (
- ∀L,T. ⦃G, L0, ⓪{I}⦄ ⊐+ ⦃G, L, T⦄ →
- ∀T1. ⦃G, L⦄ ⊢ T ➡[h] T1 → ∀T2. ⦃G, L⦄ ⊢ T ➡[h] T2 →
- ∀L1. ⦃G, L⦄ ⊢ ➡[h, T] L1 → ∀L2. ⦃G, L⦄ ⊢ ➡[h, T] L2 →
- ∃∃K0. ⦃G, L1⦄ ⊢ ➡[h, T1] K0 & ⦃G, L2⦄ ⊢ ➡[h, T2] K0
- ) →
- ∀L1. ⦃G, L0⦄ ⊢ ➡[h, ⓪{I}] L1 → ∀L2. ⦃G, L0⦄ ⊢ ➡[h, ⓪{I}] L2 →
- ∃∃L. ⦃G, L1⦄ ⊢ ➡[h, ⓪{I}] L & ⦃G, L2⦄ ⊢ ➡[h, ⓪{I}] L.
-#h #I #G * [ | #K0 #J #V0 cases I -I [ | * | ] ]
-[ #_ #L1 #HL01 #L2 #HL02
- lapply (lfpr_inv_atom_sn … HL01) -HL01 #H destruct
- lapply (lfpr_inv_atom_sn … HL02) -HL02 #H destruct
- /2 width=3 by ex2_intro/
-| #s #IH #L1 #HL01 #L2 #HL02
- elim (lfxs_inv_sort_pair_sn … HL01) -HL01 #K1 #V1 #HK01 #H destruct
- elim (lfxs_inv_sort_pair_sn … HL02) -HL02 #K2 #V2 #HK02 #H destruct
- elim (IH … HK01 … HK02) -IH -HK01 -HK02
- /3 width=5 by lfpr_sort, fqu_fqup, fqu_drop, ex2_intro/
-| #IH #L1 #HL01 #L2 #HL02
- elim (lfpr_inv_zero_pair_sn … HL01) -HL01 #K1 #V1 #HK01 #HV01 #H destruct
- elim (lfpr_inv_zero_pair_sn … HL02) -HL02 #K2 #V2 #HK02 #HV02 #H destruct
- elim (cpr_conf_lfpr … HV01 … HV02 … HK01 … HK02) #V #HV1 #HV2
- elim (IH … HV01 … HV02 … HK01 … HK02) -IH -HV01 -HV02 -HK01 -HK02
- /3 width=5 by lfpr_zero, fqu_fqup, fqu_drop, ex2_intro/
-| #i #IH #L1 #HL01 #L2 #HL02
- elim (lfxs_inv_lref_pair_sn … HL01) -HL01 #K1 #V1 #HK01 #H destruct
- elim (lfxs_inv_lref_pair_sn … HL02) -HL02 #K2 #V2 #HK02 #H destruct
- elim (IH … HK01 … HK02) -IH -HK01 -HK02
- /3 width=5 by lfpr_lref, fqu_fqup, fqu_drop, ex2_intro/
-| #l #IH #L1 #HL01 #L2 #HL02
- elim (lfxs_inv_gref_pair_sn … HL01) -HL01 #K1 #V1 #HK01 #H destruct
- elim (lfxs_inv_gref_pair_sn … HL02) -HL02 #K2 #V2 #HK02 #H destruct
- elim (IH … HK01 … HK02) -IH -HK01 -HK02
- /3 width=5 by lfpr_gref, fqu_fqup, fqu_drop, ex2_intro/
-]
-qed-.
-
-theorem lfpr_conf_cpr: ∀h,G. lfxs_confluent_R (cpm 0 h G) (cpm 0 h G).
-#h #G #L0 #T0 @(fqup_wf_ind_eq … G L0 T0) -G -L0 -T0 #G #L #T #IH #G0 #L0 * [| * ]
-[ #I0 #HG #HL #HT #T1 #H1 #T2 #H2 #L1 #HL01 #L2 #HL02 destruct
- elim (cpr_inv_atom1_drops … H1) -H1
- elim (cpr_inv_atom1_drops … H2) -H2
- [ #H2 #H1 destruct
- /3 width=7 by lfpr_conf_cpr_atom_atom/
- | * #K0 #V0 #V2 * [2: #i2 ] #HLK0 #HV02 #HVT2 #H2 #H1 destruct
-
-(*
-
-theorem lpr_conf: ∀G. confluent … (lpr G).
-/3 width=6 by lpx_sn_conf, cpr_conf_lpr/
-qed-.
-
-*)
+++ /dev/null
-(**************************************************************************)
-(* ___ *)
-(* ||M|| *)
-(* ||A|| A project by Andrea Asperti *)
-(* ||T|| *)
-(* ||I|| Developers: *)
-(* ||T|| The HELM team. *)
-(* ||A|| http://helm.cs.unibo.it *)
-(* \ / *)
-(* \ / This file is distributed under the terms of the *)
-(* v GNU General Public License Version 2 *)
-(* *)
-(**************************************************************************)
-
-include "ground_2/relocation/rtmap_id.ma".
-include "basic_2/notation/relations/relationstar_4.ma".
-include "basic_2/relocation/lexs.ma".
-include "basic_2/static/frees.ma".
-
-(* GENERIC EXTENSION ON REFERRED ENTRIES OF A CONTEXT-SENSITIVE REALTION ****)
-
-definition lfxs (R) (T): relation lenv ≝
- λL1,L2. ∃∃f. L1 ⊢ 𝐅*⦃T⦄ ≡ f & L1 ⦻*[R, cfull, f] L2.
-
-interpretation "generic extension on referred entries (local environment)"
- 'RelationStar R T L1 L2 = (lfxs R T L1 L2).
-
-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 ***********************************************************)
-
-lemma lfxs_atom: ∀R,I. ⋆ ⦻*[R, ⓪{I}] ⋆.
-/3 width=3 by lexs_atom, frees_atom, ex2_intro/
-qed.
-
-lemma lfxs_sort: ∀R,I,L1,L2,V1,V2,s.
- L1 ⦻*[R, ⋆s] L2 → L1.ⓑ{I}V1 ⦻*[R, ⋆s] L2.ⓑ{I}V2.
-#R #I #L1 #L2 #V1 #V2 #s * /3 width=3 by lexs_push, frees_sort, ex2_intro/
-qed.
-
-lemma lfxs_zero: ∀R,I,L1,L2,V1,V2. L1 ⦻*[R, V1] L2 →
- R L1 V1 V2 → L1.ⓑ{I}V1 ⦻*[R, #0] L2.ⓑ{I}V2.
-#R #I #L1 #L2 #V1 #V2 * /3 width=3 by lexs_next, frees_zero, ex2_intro/
-qed.
-
-lemma lfxs_lref: ∀R,I,L1,L2,V1,V2,i.
- L1 ⦻*[R, #i] L2 → L1.ⓑ{I}V1 ⦻*[R, #⫯i] L2.ⓑ{I}V2.
-#R #I #L1 #L2 #V1 #V2 #i * /3 width=3 by lexs_push, frees_lref, ex2_intro/
-qed.
-
-lemma lfxs_gref: ∀R,I,L1,L2,V1,V2,l.
- L1 ⦻*[R, §l] L2 → L1.ⓑ{I}V1 ⦻*[R, §l] L2.ⓑ{I}V2.
-#R #I #L1 #L2 #V1 #V2 #l * /3 width=3 by lexs_push, frees_gref, ex2_intro/
-qed.
-
-lemma lfxs_pair_repl_dx: ∀R,I,L1,L2,T,V,V1.
- L1.ⓑ{I}V ⦻*[R, T] L2.ⓑ{I}V1 →
- ∀V2. R L1 V V2 →
- L1.ⓑ{I}V ⦻*[R, T] L2.ⓑ{I}V2.
-#R #I #L1 #L2 #T #V #V1 * #f #Hf #HL12 #V2 #HR
-/3 width=5 by lexs_pair_repl, ex2_intro/
-qed-.
-
-lemma lfxs_sym: ∀R. lexs_frees_confluent R cfull →
- (∀L1,L2,T1,T2. R L1 T1 T2 → R L2 T2 T1) →
- ∀T. symmetric … (lfxs R T).
-#R #H1R #H2R #T #L1 #L2 * #f1 #Hf1 #HL12 elim (H1R … Hf1 … HL12) -Hf1
-/4 width=5 by sle_lexs_trans, lexs_sym, ex2_intro/
-qed-.
-
-lemma lfxs_co: ∀R1,R2. (∀L,T1,T2. R1 L T1 T2 → R2 L T1 T2) →
- ∀L1,L2,T. L1 ⦻*[R1, T] L2 → L1 ⦻*[R2, T] L2.
-#R1 #R2 #HR #L1 #L2 #T * /4 width=7 by lexs_co, ex2_intro/
-qed-.
-
-(* Basic inversion lemmas ***************************************************)
-
-lemma lfxs_inv_atom_sn: ∀R,I,Y2. ⋆ ⦻*[R, ⓪{I}] Y2 → Y2 = ⋆.
-#R #I #Y2 * /2 width=4 by lexs_inv_atom1/
-qed-.
-
-lemma lfxs_inv_atom_dx: ∀R,I,Y1. Y1 ⦻*[R, ⓪{I}] ⋆ → Y1 = ⋆.
-#R #I #Y1 * /2 width=4 by lexs_inv_atom2/
-qed-.
-
-lemma lfxs_inv_sort: ∀R,Y1,Y2,s. Y1 ⦻*[R, ⋆s] Y2 →
- (Y1 = ⋆ ∧ Y2 = ⋆) ∨
- ∃∃I,L1,L2,V1,V2. L1 ⦻*[R, ⋆s] L2 &
- Y1 = L1.ⓑ{I}V1 & Y2 = L2.ⓑ{I}V2.
-#R * [ | #Y1 #I #V1 ] #Y2 #s * #f #H1 #H2
-[ lapply (lexs_inv_atom1 … H2) -H2 /3 width=1 by or_introl, conj/
-| lapply (frees_inv_sort … H1) -H1 #Hf
- elim (isid_inv_gen … Hf) -Hf #g #Hg #H destruct
- elim (lexs_inv_push1 … H2) -H2 #L2 #V2 #H12 #_ #H destruct
- /5 width=8 by frees_sort_gen, ex3_5_intro, ex2_intro, or_intror/
-]
-qed-.
-
-lemma lfxs_inv_zero: ∀R,Y1,Y2. Y1 ⦻*[R, #0] Y2 →
- (Y1 = ⋆ ∧ Y2 = ⋆) ∨
- ∃∃I,L1,L2,V1,V2. L1 ⦻*[R, V1] L2 & R L1 V1 V2 &
- Y1 = L1.ⓑ{I}V1 & Y2 = L2.ⓑ{I}V2.
-#R #Y1 #Y2 * #f #H1 #H2 elim (frees_inv_zero … H1) -H1 *
-[ #H #_ lapply (lexs_inv_atom1_aux … H2 H) -H2 /3 width=1 by or_introl, conj/
-| #I1 #L1 #V1 #g #HV1 #HY1 #Hg elim (lexs_inv_next1_aux … H2 … HY1 Hg) -H2 -Hg
- /4 width=9 by ex4_5_intro, ex2_intro, or_intror/
-]
-qed-.
-
-lemma lfxs_inv_lref: ∀R,Y1,Y2,i. Y1 ⦻*[R, #⫯i] Y2 →
- (Y1 = ⋆ ∧ Y2 = ⋆) ∨
- ∃∃I,L1,L2,V1,V2. L1 ⦻*[R, #i] L2 &
- Y1 = L1.ⓑ{I}V1 & Y2 = L2.ⓑ{I}V2.
-#R #Y1 #Y2 #i * #f #H1 #H2 elim (frees_inv_lref … H1) -H1 *
-[ #H #_ lapply (lexs_inv_atom1_aux … H2 H) -H2 /3 width=1 by or_introl, conj/
-| #I1 #L1 #V1 #g #HV1 #HY1 #Hg elim (lexs_inv_push1_aux … H2 … HY1 Hg) -H2 -Hg
- /4 width=8 by ex3_5_intro, ex2_intro, or_intror/
-]
-qed-.
-
-lemma lfxs_inv_gref: ∀R,Y1,Y2,l. Y1 ⦻*[R, §l] Y2 →
- (Y1 = ⋆ ∧ Y2 = ⋆) ∨
- ∃∃I,L1,L2,V1,V2. L1 ⦻*[R, §l] L2 &
- Y1 = L1.ⓑ{I}V1 & Y2 = L2.ⓑ{I}V2.
-#R * [ | #Y1 #I #V1 ] #Y2 #l * #f #H1 #H2
-[ lapply (lexs_inv_atom1 … H2) -H2 /3 width=1 by or_introl, conj/
-| lapply (frees_inv_gref … H1) -H1 #Hf
- elim (isid_inv_gen … Hf) -Hf #g #Hg #H destruct
- elim (lexs_inv_push1 … H2) -H2 #L2 #V2 #H12 #_ #H destruct
- /5 width=8 by frees_gref_gen, ex3_5_intro, ex2_intro, or_intror/
-]
-qed-.
-
-lemma lfxs_inv_bind: ∀R,p,I,L1,L2,V1,V2,T. L1 ⦻*[R, ⓑ{p,I}V1.T] L2 → R L1 V1 V2 →
- L1 ⦻*[R, V1] L2 ∧ L1.ⓑ{I}V1 ⦻*[R, T] L2.ⓑ{I}V2.
-#R #p #I #L1 #L2 #V1 #V2 #T * #f #Hf #HL #HV elim (frees_inv_bind … Hf) -Hf
-/6 width=6 by sle_lexs_trans, lexs_inv_tl, sor_inv_sle_dx, sor_inv_sle_sn, ex2_intro, conj/
-qed-.
-
-lemma lfxs_inv_flat: ∀R,I,L1,L2,V,T. L1 ⦻*[R, ⓕ{I}V.T] L2 →
- L1 ⦻*[R, V] L2 ∧ L1 ⦻*[R, T] L2.
-#R #I #L1 #L2 #V #T * #f #Hf #HL elim (frees_inv_flat … Hf) -Hf
-/5 width=6 by sle_lexs_trans, sor_inv_sle_dx, sor_inv_sle_sn, ex2_intro, conj/
-qed-.
-
-(* Advanced inversion lemmas ************************************************)
-
-lemma lfxs_inv_sort_pair_sn: ∀R,I,Y2,L1,V1,s. L1.ⓑ{I}V1 ⦻*[R, ⋆s] Y2 →
- ∃∃L2,V2. L1 ⦻*[R, ⋆s] L2 & Y2 = L2.ⓑ{I}V2.
-#R #I #Y2 #L1 #V1 #s #H elim (lfxs_inv_sort … H) -H *
-[ #H destruct
-| #J #Y1 #L2 #X1 #V2 #Hs #H1 #H2 destruct /2 width=4 by ex2_2_intro/
-]
-qed-.
-
-lemma lfxs_inv_sort_pair_dx: ∀R,I,Y1,L2,V2,s. Y1 ⦻*[R, ⋆s] L2.ⓑ{I}V2 →
- ∃∃L1,V1. L1 ⦻*[R, ⋆s] L2 & Y1 = L1.ⓑ{I}V1.
-#R #I #Y1 #L2 #V2 #s #H elim (lfxs_inv_sort … H) -H *
-[ #_ #H destruct
-| #J #L1 #Y2 #V1 #X2 #Hs #H1 #H2 destruct /2 width=4 by ex2_2_intro/
-]
-qed-.
-
-lemma lfxs_inv_zero_pair_sn: ∀R,I,Y2,L1,V1. L1.ⓑ{I}V1 ⦻*[R, #0] Y2 →
- ∃∃L2,V2. L1 ⦻*[R, V1] L2 & R L1 V1 V2 &
- Y2 = L2.ⓑ{I}V2.
-#R #I #Y2 #L1 #V1 #H elim (lfxs_inv_zero … H) -H *
-[ #H destruct
-| #J #Y1 #L2 #X1 #V2 #HV1 #HV12 #H1 #H2 destruct
- /2 width=5 by ex3_2_intro/
-]
-qed-.
-
-lemma lfxs_inv_zero_pair_dx: ∀R,I,Y1,L2,V2. Y1 ⦻*[R, #0] L2.ⓑ{I}V2 →
- ∃∃L1,V1. L1 ⦻*[R, V1] L2 & R L1 V1 V2 &
- Y1 = L1.ⓑ{I}V1.
-#R #I #Y1 #L2 #V2 #H elim (lfxs_inv_zero … H) -H *
-[ #_ #H destruct
-| #J #L1 #Y2 #V1 #X2 #HV1 #HV12 #H1 #H2 destruct
- /2 width=5 by ex3_2_intro/
-]
-qed-.
-
-lemma lfxs_inv_lref_pair_sn: ∀R,I,Y2,L1,V1,i. L1.ⓑ{I}V1 ⦻*[R, #⫯i] Y2 →
- ∃∃L2,V2. L1 ⦻*[R, #i] L2 & Y2 = L2.ⓑ{I}V2.
-#R #I #Y2 #L1 #V1 #i #H elim (lfxs_inv_lref … H) -H *
-[ #H destruct
-| #J #Y1 #L2 #X1 #V2 #Hi #H1 #H2 destruct /2 width=4 by ex2_2_intro/
-]
-qed-.
-
-lemma lfxs_inv_lref_pair_dx: ∀R,I,Y1,L2,V2,i. Y1 ⦻*[R, #⫯i] L2.ⓑ{I}V2 →
- ∃∃L1,V1. L1 ⦻*[R, #i] L2 & Y1 = L1.ⓑ{I}V1.
-#R #I #Y1 #L2 #V2 #i #H elim (lfxs_inv_lref … H) -H *
-[ #_ #H destruct
-| #J #L1 #Y2 #V1 #X2 #Hi #H1 #H2 destruct /2 width=4 by ex2_2_intro/
-]
-qed-.
-
-lemma lfxs_inv_gref_pair_sn: ∀R,I,Y2,L1,V1,l. L1.ⓑ{I}V1 ⦻*[R, §l] Y2 →
- ∃∃L2,V2. L1 ⦻*[R, §l] L2 & Y2 = L2.ⓑ{I}V2.
-#R #I #Y2 #L1 #V1 #l #H elim (lfxs_inv_gref … H) -H *
-[ #H destruct
-| #J #Y1 #L2 #X1 #V2 #Hl #H1 #H2 destruct /2 width=4 by ex2_2_intro/
-]
-qed-.
-
-lemma lfxs_inv_gref_pair_dx: ∀R,I,Y1,L2,V2,l. Y1 ⦻*[R, §l] L2.ⓑ{I}V2 →
- ∃∃L1,V1. L1 ⦻*[R, §l] L2 & Y1 = L1.ⓑ{I}V1.
-#R #I #Y1 #L2 #V2 #l #H elim (lfxs_inv_gref … H) -H *
-[ #_ #H destruct
-| #J #L1 #Y2 #V1 #X2 #Hl #H1 #H2 destruct /2 width=4 by ex2_2_intro/
-]
-qed-.
-
-(* Basic forward lemmas *****************************************************)
-
-lemma lfxs_fwd_bind_sn: ∀R,p,I,L1,L2,V,T. L1 ⦻*[R, ⓑ{p,I}V.T] L2 → L1 ⦻*[R, V] L2.
-#R #p #I #L1 #L2 #V #T * #f #Hf #HL elim (frees_inv_bind … Hf) -Hf
-/4 width=6 by sle_lexs_trans, sor_inv_sle_sn, ex2_intro/
-qed-.
-
-lemma lfxs_fwd_bind_dx: ∀R,p,I,L1,L2,V1,V2,T. L1 ⦻*[R, ⓑ{p,I}V1.T] L2 →
- R L1 V1 V2 → L1.ⓑ{I}V1 ⦻*[R, T] L2.ⓑ{I}V2.
-#R #p #I #L1 #L2 #V1 #V2 #T #H #HV elim (lfxs_inv_bind … H HV) -H -HV //
-qed-.
-
-lemma lfxs_fwd_flat_sn: ∀R,I,L1,L2,V,T. L1 ⦻*[R, ⓕ{I}V.T] L2 → L1 ⦻*[R, V] L2.
-#R #I #L1 #L2 #V #T #H elim (lfxs_inv_flat … H) -H //
-qed-.
-
-lemma lfxs_fwd_flat_dx: ∀R,I,L1,L2,V,T. L1 ⦻*[R, ⓕ{I}V.T] L2 → L1 ⦻*[R, T] L2.
-#R #I #L1 #L2 #V #T #H elim (lfxs_inv_flat … H) -H //
-qed-.
-
-lemma lfxs_fwd_pair_sn: ∀R,I,L1,L2,V,T. L1 ⦻*[R, ②{I}V.T] L2 → L1 ⦻*[R, V] L2.
-#R * /2 width=4 by lfxs_fwd_flat_sn, lfxs_fwd_bind_sn/
-qed-.
-
-(* Basic_2A1: removed theorems 24:
- llpx_sn_sort llpx_sn_skip llpx_sn_lref llpx_sn_free llpx_sn_gref
- llpx_sn_bind llpx_sn_flat
- llpx_sn_inv_bind llpx_sn_inv_flat
- llpx_sn_fwd_lref llpx_sn_fwd_pair_sn llpx_sn_fwd_length
- llpx_sn_fwd_bind_sn llpx_sn_fwd_bind_dx llpx_sn_fwd_flat_sn llpx_sn_fwd_flat_dx
- llpx_sn_refl llpx_sn_Y llpx_sn_bind_O llpx_sn_ge_up llpx_sn_ge llpx_sn_co
- llpx_sn_fwd_drop_sn llpx_sn_fwd_drop_dx
-*)
--- /dev/null
+(**************************************************************************)
+(* ___ *)
+(* ||M|| *)
+(* ||A|| A project by Andrea Asperti *)
+(* ||T|| *)
+(* ||I|| Developers: *)
+(* ||T|| The HELM team. *)
+(* ||A|| http://helm.cs.unibo.it *)
+(* \ / *)
+(* \ / This file is distributed under the terms of the *)
+(* v GNU General Public License Version 2 *)
+(* *)
+(**************************************************************************)
+
+include "ground_2/relocation/rtmap_id.ma".
+include "basic_2/notation/relations/relationstar_4.ma".
+include "basic_2/relocation/lexs.ma".
+include "basic_2/static/frees.ma".
+
+(* GENERIC EXTENSION ON REFERRED ENTRIES OF A CONTEXT-SENSITIVE REALTION ****)
+
+definition lfxs (R) (T): relation lenv ≝
+ λL1,L2. ∃∃f. L1 ⊢ 𝐅*⦃T⦄ ≡ f & L1 ⦻*[R, cfull, f] L2.
+
+interpretation "generic extension on referred entries (local environment)"
+ 'RelationStar R T L1 L2 = (lfxs R T L1 L2).
+
+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 ***********************************************************)
+
+lemma lfxs_atom: ∀R,I. ⋆ ⦻*[R, ⓪{I}] ⋆.
+/3 width=3 by lexs_atom, frees_atom, ex2_intro/
+qed.
+
+lemma lfxs_sort: ∀R,I,L1,L2,V1,V2,s.
+ L1 ⦻*[R, ⋆s] L2 → L1.ⓑ{I}V1 ⦻*[R, ⋆s] L2.ⓑ{I}V2.
+#R #I #L1 #L2 #V1 #V2 #s * /3 width=3 by lexs_push, frees_sort, ex2_intro/
+qed.
+
+lemma lfxs_zero: ∀R,I,L1,L2,V1,V2. L1 ⦻*[R, V1] L2 →
+ R L1 V1 V2 → L1.ⓑ{I}V1 ⦻*[R, #0] L2.ⓑ{I}V2.
+#R #I #L1 #L2 #V1 #V2 * /3 width=3 by lexs_next, frees_zero, ex2_intro/
+qed.
+
+lemma lfxs_lref: ∀R,I,L1,L2,V1,V2,i.
+ L1 ⦻*[R, #i] L2 → L1.ⓑ{I}V1 ⦻*[R, #⫯i] L2.ⓑ{I}V2.
+#R #I #L1 #L2 #V1 #V2 #i * /3 width=3 by lexs_push, frees_lref, ex2_intro/
+qed.
+
+lemma lfxs_gref: ∀R,I,L1,L2,V1,V2,l.
+ L1 ⦻*[R, §l] L2 → L1.ⓑ{I}V1 ⦻*[R, §l] L2.ⓑ{I}V2.
+#R #I #L1 #L2 #V1 #V2 #l * /3 width=3 by lexs_push, frees_gref, ex2_intro/
+qed.
+
+lemma lfxs_pair_repl_dx: ∀R,I,L1,L2,T,V,V1.
+ L1.ⓑ{I}V ⦻*[R, T] L2.ⓑ{I}V1 →
+ ∀V2. R L1 V V2 →
+ L1.ⓑ{I}V ⦻*[R, T] L2.ⓑ{I}V2.
+#R #I #L1 #L2 #T #V #V1 * #f #Hf #HL12 #V2 #HR
+/3 width=5 by lexs_pair_repl, ex2_intro/
+qed-.
+
+lemma lfxs_sym: ∀R. lexs_frees_confluent R cfull →
+ (∀L1,L2,T1,T2. R L1 T1 T2 → R L2 T2 T1) →
+ ∀T. symmetric … (lfxs R T).
+#R #H1R #H2R #T #L1 #L2 * #f1 #Hf1 #HL12 elim (H1R … Hf1 … HL12) -Hf1
+/4 width=5 by sle_lexs_trans, lexs_sym, ex2_intro/
+qed-.
+
+lemma lfxs_co: ∀R1,R2. (∀L,T1,T2. R1 L T1 T2 → R2 L T1 T2) →
+ ∀L1,L2,T. L1 ⦻*[R1, T] L2 → L1 ⦻*[R2, T] L2.
+#R1 #R2 #HR #L1 #L2 #T * /4 width=7 by lexs_co, ex2_intro/
+qed-.
+
+(* Basic inversion lemmas ***************************************************)
+
+lemma lfxs_inv_atom_sn: ∀R,I,Y2. ⋆ ⦻*[R, ⓪{I}] Y2 → Y2 = ⋆.
+#R #I #Y2 * /2 width=4 by lexs_inv_atom1/
+qed-.
+
+lemma lfxs_inv_atom_dx: ∀R,I,Y1. Y1 ⦻*[R, ⓪{I}] ⋆ → Y1 = ⋆.
+#R #I #Y1 * /2 width=4 by lexs_inv_atom2/
+qed-.
+
+lemma lfxs_inv_sort: ∀R,Y1,Y2,s. Y1 ⦻*[R, ⋆s] Y2 →
+ (Y1 = ⋆ ∧ Y2 = ⋆) ∨
+ ∃∃I,L1,L2,V1,V2. L1 ⦻*[R, ⋆s] L2 &
+ Y1 = L1.ⓑ{I}V1 & Y2 = L2.ⓑ{I}V2.
+#R * [ | #Y1 #I #V1 ] #Y2 #s * #f #H1 #H2
+[ lapply (lexs_inv_atom1 … H2) -H2 /3 width=1 by or_introl, conj/
+| lapply (frees_inv_sort … H1) -H1 #Hf
+ elim (isid_inv_gen … Hf) -Hf #g #Hg #H destruct
+ elim (lexs_inv_push1 … H2) -H2 #L2 #V2 #H12 #_ #H destruct
+ /5 width=8 by frees_sort_gen, ex3_5_intro, ex2_intro, or_intror/
+]
+qed-.
+
+lemma lfxs_inv_zero: ∀R,Y1,Y2. Y1 ⦻*[R, #0] Y2 →
+ (Y1 = ⋆ ∧ Y2 = ⋆) ∨
+ ∃∃I,L1,L2,V1,V2. L1 ⦻*[R, V1] L2 & R L1 V1 V2 &
+ Y1 = L1.ⓑ{I}V1 & Y2 = L2.ⓑ{I}V2.
+#R #Y1 #Y2 * #f #H1 #H2 elim (frees_inv_zero … H1) -H1 *
+[ #H #_ lapply (lexs_inv_atom1_aux … H2 H) -H2 /3 width=1 by or_introl, conj/
+| #I1 #L1 #V1 #g #HV1 #HY1 #Hg elim (lexs_inv_next1_aux … H2 … HY1 Hg) -H2 -Hg
+ /4 width=9 by ex4_5_intro, ex2_intro, or_intror/
+]
+qed-.
+
+lemma lfxs_inv_lref: ∀R,Y1,Y2,i. Y1 ⦻*[R, #⫯i] Y2 →
+ (Y1 = ⋆ ∧ Y2 = ⋆) ∨
+ ∃∃I,L1,L2,V1,V2. L1 ⦻*[R, #i] L2 &
+ Y1 = L1.ⓑ{I}V1 & Y2 = L2.ⓑ{I}V2.
+#R #Y1 #Y2 #i * #f #H1 #H2 elim (frees_inv_lref … H1) -H1 *
+[ #H #_ lapply (lexs_inv_atom1_aux … H2 H) -H2 /3 width=1 by or_introl, conj/
+| #I1 #L1 #V1 #g #HV1 #HY1 #Hg elim (lexs_inv_push1_aux … H2 … HY1 Hg) -H2 -Hg
+ /4 width=8 by ex3_5_intro, ex2_intro, or_intror/
+]
+qed-.
+
+lemma lfxs_inv_gref: ∀R,Y1,Y2,l. Y1 ⦻*[R, §l] Y2 →
+ (Y1 = ⋆ ∧ Y2 = ⋆) ∨
+ ∃∃I,L1,L2,V1,V2. L1 ⦻*[R, §l] L2 &
+ Y1 = L1.ⓑ{I}V1 & Y2 = L2.ⓑ{I}V2.
+#R * [ | #Y1 #I #V1 ] #Y2 #l * #f #H1 #H2
+[ lapply (lexs_inv_atom1 … H2) -H2 /3 width=1 by or_introl, conj/
+| lapply (frees_inv_gref … H1) -H1 #Hf
+ elim (isid_inv_gen … Hf) -Hf #g #Hg #H destruct
+ elim (lexs_inv_push1 … H2) -H2 #L2 #V2 #H12 #_ #H destruct
+ /5 width=8 by frees_gref_gen, ex3_5_intro, ex2_intro, or_intror/
+]
+qed-.
+
+lemma lfxs_inv_bind: ∀R,p,I,L1,L2,V1,V2,T. L1 ⦻*[R, ⓑ{p,I}V1.T] L2 → R L1 V1 V2 →
+ L1 ⦻*[R, V1] L2 ∧ L1.ⓑ{I}V1 ⦻*[R, T] L2.ⓑ{I}V2.
+#R #p #I #L1 #L2 #V1 #V2 #T * #f #Hf #HL #HV elim (frees_inv_bind … Hf) -Hf
+/6 width=6 by sle_lexs_trans, lexs_inv_tl, sor_inv_sle_dx, sor_inv_sle_sn, ex2_intro, conj/
+qed-.
+
+lemma lfxs_inv_flat: ∀R,I,L1,L2,V,T. L1 ⦻*[R, ⓕ{I}V.T] L2 →
+ L1 ⦻*[R, V] L2 ∧ L1 ⦻*[R, T] L2.
+#R #I #L1 #L2 #V #T * #f #Hf #HL elim (frees_inv_flat … Hf) -Hf
+/5 width=6 by sle_lexs_trans, sor_inv_sle_dx, sor_inv_sle_sn, ex2_intro, conj/
+qed-.
+
+(* Advanced inversion lemmas ************************************************)
+
+lemma lfxs_inv_sort_pair_sn: ∀R,I,Y2,L1,V1,s. L1.ⓑ{I}V1 ⦻*[R, ⋆s] Y2 →
+ ∃∃L2,V2. L1 ⦻*[R, ⋆s] L2 & Y2 = L2.ⓑ{I}V2.
+#R #I #Y2 #L1 #V1 #s #H elim (lfxs_inv_sort … H) -H *
+[ #H destruct
+| #J #Y1 #L2 #X1 #V2 #Hs #H1 #H2 destruct /2 width=4 by ex2_2_intro/
+]
+qed-.
+
+lemma lfxs_inv_sort_pair_dx: ∀R,I,Y1,L2,V2,s. Y1 ⦻*[R, ⋆s] L2.ⓑ{I}V2 →
+ ∃∃L1,V1. L1 ⦻*[R, ⋆s] L2 & Y1 = L1.ⓑ{I}V1.
+#R #I #Y1 #L2 #V2 #s #H elim (lfxs_inv_sort … H) -H *
+[ #_ #H destruct
+| #J #L1 #Y2 #V1 #X2 #Hs #H1 #H2 destruct /2 width=4 by ex2_2_intro/
+]
+qed-.
+
+lemma lfxs_inv_zero_pair_sn: ∀R,I,Y2,L1,V1. L1.ⓑ{I}V1 ⦻*[R, #0] Y2 →
+ ∃∃L2,V2. L1 ⦻*[R, V1] L2 & R L1 V1 V2 &
+ Y2 = L2.ⓑ{I}V2.
+#R #I #Y2 #L1 #V1 #H elim (lfxs_inv_zero … H) -H *
+[ #H destruct
+| #J #Y1 #L2 #X1 #V2 #HV1 #HV12 #H1 #H2 destruct
+ /2 width=5 by ex3_2_intro/
+]
+qed-.
+
+lemma lfxs_inv_zero_pair_dx: ∀R,I,Y1,L2,V2. Y1 ⦻*[R, #0] L2.ⓑ{I}V2 →
+ ∃∃L1,V1. L1 ⦻*[R, V1] L2 & R L1 V1 V2 &
+ Y1 = L1.ⓑ{I}V1.
+#R #I #Y1 #L2 #V2 #H elim (lfxs_inv_zero … H) -H *
+[ #_ #H destruct
+| #J #L1 #Y2 #V1 #X2 #HV1 #HV12 #H1 #H2 destruct
+ /2 width=5 by ex3_2_intro/
+]
+qed-.
+
+lemma lfxs_inv_lref_pair_sn: ∀R,I,Y2,L1,V1,i. L1.ⓑ{I}V1 ⦻*[R, #⫯i] Y2 →
+ ∃∃L2,V2. L1 ⦻*[R, #i] L2 & Y2 = L2.ⓑ{I}V2.
+#R #I #Y2 #L1 #V1 #i #H elim (lfxs_inv_lref … H) -H *
+[ #H destruct
+| #J #Y1 #L2 #X1 #V2 #Hi #H1 #H2 destruct /2 width=4 by ex2_2_intro/
+]
+qed-.
+
+lemma lfxs_inv_lref_pair_dx: ∀R,I,Y1,L2,V2,i. Y1 ⦻*[R, #⫯i] L2.ⓑ{I}V2 →
+ ∃∃L1,V1. L1 ⦻*[R, #i] L2 & Y1 = L1.ⓑ{I}V1.
+#R #I #Y1 #L2 #V2 #i #H elim (lfxs_inv_lref … H) -H *
+[ #_ #H destruct
+| #J #L1 #Y2 #V1 #X2 #Hi #H1 #H2 destruct /2 width=4 by ex2_2_intro/
+]
+qed-.
+
+lemma lfxs_inv_gref_pair_sn: ∀R,I,Y2,L1,V1,l. L1.ⓑ{I}V1 ⦻*[R, §l] Y2 →
+ ∃∃L2,V2. L1 ⦻*[R, §l] L2 & Y2 = L2.ⓑ{I}V2.
+#R #I #Y2 #L1 #V1 #l #H elim (lfxs_inv_gref … H) -H *
+[ #H destruct
+| #J #Y1 #L2 #X1 #V2 #Hl #H1 #H2 destruct /2 width=4 by ex2_2_intro/
+]
+qed-.
+
+lemma lfxs_inv_gref_pair_dx: ∀R,I,Y1,L2,V2,l. Y1 ⦻*[R, §l] L2.ⓑ{I}V2 →
+ ∃∃L1,V1. L1 ⦻*[R, §l] L2 & Y1 = L1.ⓑ{I}V1.
+#R #I #Y1 #L2 #V2 #l #H elim (lfxs_inv_gref … H) -H *
+[ #_ #H destruct
+| #J #L1 #Y2 #V1 #X2 #Hl #H1 #H2 destruct /2 width=4 by ex2_2_intro/
+]
+qed-.
+
+(* Basic forward lemmas *****************************************************)
+
+lemma lfxs_fwd_bind_sn: ∀R,p,I,L1,L2,V,T. L1 ⦻*[R, ⓑ{p,I}V.T] L2 → L1 ⦻*[R, V] L2.
+#R #p #I #L1 #L2 #V #T * #f #Hf #HL elim (frees_inv_bind … Hf) -Hf
+/4 width=6 by sle_lexs_trans, sor_inv_sle_sn, ex2_intro/
+qed-.
+
+lemma lfxs_fwd_bind_dx: ∀R,p,I,L1,L2,V1,V2,T. L1 ⦻*[R, ⓑ{p,I}V1.T] L2 →
+ R L1 V1 V2 → L1.ⓑ{I}V1 ⦻*[R, T] L2.ⓑ{I}V2.
+#R #p #I #L1 #L2 #V1 #V2 #T #H #HV elim (lfxs_inv_bind … H HV) -H -HV //
+qed-.
+
+lemma lfxs_fwd_flat_sn: ∀R,I,L1,L2,V,T. L1 ⦻*[R, ⓕ{I}V.T] L2 → L1 ⦻*[R, V] L2.
+#R #I #L1 #L2 #V #T #H elim (lfxs_inv_flat … H) -H //
+qed-.
+
+lemma lfxs_fwd_flat_dx: ∀R,I,L1,L2,V,T. L1 ⦻*[R, ⓕ{I}V.T] L2 → L1 ⦻*[R, T] L2.
+#R #I #L1 #L2 #V #T #H elim (lfxs_inv_flat … H) -H //
+qed-.
+
+lemma lfxs_fwd_pair_sn: ∀R,I,L1,L2,V,T. L1 ⦻*[R, ②{I}V.T] L2 → L1 ⦻*[R, V] L2.
+#R * /2 width=4 by lfxs_fwd_flat_sn, lfxs_fwd_bind_sn/
+qed-.
+
+(* Basic_2A1: removed theorems 24:
+ llpx_sn_sort llpx_sn_skip llpx_sn_lref llpx_sn_free llpx_sn_gref
+ llpx_sn_bind llpx_sn_flat
+ llpx_sn_inv_bind llpx_sn_inv_flat
+ llpx_sn_fwd_lref llpx_sn_fwd_pair_sn llpx_sn_fwd_length
+ llpx_sn_fwd_bind_sn llpx_sn_fwd_bind_dx llpx_sn_fwd_flat_sn llpx_sn_fwd_flat_dx
+ llpx_sn_refl llpx_sn_Y llpx_sn_bind_O llpx_sn_ge_up llpx_sn_ge llpx_sn_co
+ llpx_sn_fwd_drop_sn llpx_sn_fwd_drop_dx
+*)
--- /dev/null
+(**************************************************************************)
+(* ___ *)
+(* ||M|| *)
+(* ||A|| A project by Andrea Asperti *)
+(* ||T|| *)
+(* ||I|| Developers: *)
+(* ||T|| The HELM team. *)
+(* ||A|| http://helm.cs.unibo.it *)
+(* \ / *)
+(* \ / This file is distributed under the terms of the *)
+(* v GNU General Public License Version 2 *)
+(* *)
+(**************************************************************************)
+
+include "basic_2/relocation/drops_ceq.ma".
+include "basic_2/relocation/drops_lexs.ma".
+include "basic_2/static/frees_drops.ma".
+include "basic_2/static/lfxs.ma".
+
+(* GENERIC EXTENSION ON REFERRED ENTRIES OF A CONTEXT-SENSITIVE REALTION ****)
+
+definition dedropable_sn: predicate (relation3 lenv term term) ≝
+ λR. ∀b,f,L1,K1. ⬇*[b, f] L1 ≡ K1 →
+ ∀K2,T. K1 ⦻*[R, T] K2 → ∀U. ⬆*[f] T ≡ U →
+ ∃∃L2. L1 ⦻*[R, U] L2 & ⬇*[b, f] L2 ≡ K2 & L1 ≡[f] L2.
+
+definition dropable_sn: predicate (relation3 lenv term term) ≝
+ λR. ∀b,f,L1,K1. ⬇*[b, f] L1 ≡ K1 → 𝐔⦃f⦄ →
+ ∀L2,U. L1 ⦻*[R, U] L2 → ∀T. ⬆*[f] T ≡ U →
+ ∃∃K2. K1 ⦻*[R, T] K2 & ⬇*[b, f] L2 ≡ K2.
+
+definition dropable_dx: predicate (relation3 lenv term term) ≝
+ λR. ∀L1,L2,U. L1 ⦻*[R, U] L2 →
+ ∀b,f,K2. ⬇*[b, f] L2 ≡ K2 → 𝐔⦃f⦄ → ∀T. ⬆*[f] T ≡ U →
+ ∃∃K1. ⬇*[b, f] L1 ≡ K1 & K1 ⦻*[R, T] K2.
+
+(* Properties with generic slicing for local environments *******************)
+
+(* Basic_2A1: includes: llpx_sn_lift_le llpx_sn_lift_ge *)
+lemma lfxs_liftable_dedropable: ∀R. (∀L. reflexive ? (R L)) →
+ d_liftable2 R → dedropable_sn R.
+#R #H1R #H2R #b #f #L1 #K1 #HLK1 #K2 #T * #f1 #Hf1 #HK12 #U #HTU
+elim (frees_total L1 U) #f2 #Hf2
+lapply (frees_fwd_coafter … Hf2 … HLK1 … HTU … Hf1) -HTU #Hf
+elim (lexs_liftable_co_dedropable … H1R … H2R … HLK1 … HK12 … Hf) -f1 -K1
+/3 width=6 by cfull_lift, ex3_intro, ex2_intro/
+qed-.
+
+(* Inversion lemmas with generic slicing for local environments *************)
+
+(* Basic_2A1: restricts: llpx_sn_inv_lift_le llpx_sn_inv_lift_be llpx_sn_inv_lift_ge *)
+(* Basic_2A1: was: llpx_sn_drop_conf_O *)
+lemma lfxs_dropable_sn: ∀R. dropable_sn R.
+#R #b #f #L1 #K1 #HLK1 #H1f #L2 #U * #f2 #Hf2 #HL12 #T #HTU
+elim (frees_total K1 T) #f1 #Hf1
+lapply (frees_fwd_coafter … Hf2 … HLK1 … HTU … Hf1) -HTU #H2f
+elim (lexs_co_dropable_sn … HLK1 … HL12 … H2f) -f2 -L1
+/3 width=3 by ex2_intro/
+qed-.
+
+(* Basic_2A1: was: llpx_sn_drop_trans_O *)
+(* Note: the proof might be simplified *)
+lemma lfxs_dropable_dx: ∀R. dropable_dx R.
+#R #L1 #L2 #U * #f2 #Hf2 #HL12 #b #f #K2 #HLK2 #H1f #T #HTU
+elim (drops_isuni_ex … H1f L1) #K1 #HLK1
+elim (frees_total K1 T) #f1 #Hf1
+lapply (frees_fwd_coafter … Hf2 … HLK1 … HTU … Hf1) -K1 #H2f
+elim (lexs_co_dropable_dx … HL12 … HLK2 … H2f) -L2
+/4 width=9 by frees_inv_lifts, ex2_intro/
+qed-.
+
+(* Basic_2A1: was: llpx_sn_inv_lift_O *)
+lemma lfxs_inv_lift_bi: ∀R,L1,L2,U. L1 ⦻*[R, U] L2 →
+ ∀K1,K2,i. ⬇*[i] L1 ≡ K1 → ⬇*[i] L2 ≡ K2 →
+ ∀T. ⬆*[i] T ≡ U → K1 ⦻*[R, T] K2.
+#R #L1 #L2 #U #HL12 #K1 #K2 #i #HLK1 #HLK2 #T #HTU
+elim (lfxs_dropable_sn … HLK1 … HL12 … HTU) -L1 -U // #Y #HK12 #HY
+lapply (drops_mono … HY … HLK2) -L2 -i #H destruct //
+qed-.
+
+lemma lfxs_inv_lref_sn: ∀R,L1,L2,i. L1 ⦻*[R, #i] L2 → ∀I,K1,V1. ⬇*[i] L1 ≡ K1.ⓑ{I}V1 →
+ ∃∃K2,V2. ⬇*[i] L2 ≡ K2.ⓑ{I}V2 & K1 ⦻*[R, V1] K2 & R K1 V1 V2.
+#R #L1 #L2 #i #HL12 #I #K1 #V1 #HLK1 elim (lfxs_dropable_sn … HLK1 … HL12 (#0)) -HLK1 -HL12 //
+#Y #HY #HLK2 elim (lfxs_inv_zero_pair_sn … HY) -HY
+#K2 #V2 #HK12 #HV12 #H destruct /2 width=5 by ex3_2_intro/
+qed-.
+
+lemma lfxs_inv_lref_dx: ∀R,L1,L2,i. L1 ⦻*[R, #i] L2 → ∀I,K2,V2. ⬇*[i] L2 ≡ K2.ⓑ{I}V2 →
+ ∃∃K1,V1. ⬇*[i] L1 ≡ K1.ⓑ{I}V1 & K1 ⦻*[R, V1] K2 & R K1 V1 V2.
+#R #L1 #L2 #i #HL12 #I #K2 #V2 #HLK2 elim (lfxs_dropable_dx … HL12 … HLK2 … (#0)) -HLK2 -HL12 //
+#Y #HLK1 #HY elim (lfxs_inv_zero_pair_dx … HY) -HY
+#K1 #V1 #HK12 #HV12 #H destruct /2 width=5 by ex3_2_intro/
+qed-.
--- /dev/null
+(**************************************************************************)
+(* ___ *)
+(* ||M|| *)
+(* ||A|| A project by Andrea Asperti *)
+(* ||T|| *)
+(* ||I|| Developers: *)
+(* ||T|| The HELM team. *)
+(* ||A|| http://helm.cs.unibo.it *)
+(* \ / *)
+(* \ / This file is distributed under the terms of the *)
+(* v GNU General Public License Version 2 *)
+(* *)
+(**************************************************************************)
+
+include "basic_2/static/frees_fqup.ma".
+include "basic_2/static/lfxs.ma".
+
+(* GENERIC EXTENSION ON REFERRED ENTRIES OF A CONTEXT-SENSITIVE REALTION ****)
+
+(* Advanced properties ******************************************************)
+
+lemma lfxs_refl: ∀R. (∀L. reflexive … (R L)) → ∀L,T. L ⦻*[R, T] L.
+#R #HR #L #T elim (frees_total L T) /3 width=3 by lexs_refl, ex2_intro/
+qed.
--- /dev/null
+(**************************************************************************)
+(* ___ *)
+(* ||M|| *)
+(* ||A|| A project by Andrea Asperti *)
+(* ||T|| *)
+(* ||I|| Developers: *)
+(* ||T|| The HELM team. *)
+(* ||A|| http://helm.cs.unibo.it *)
+(* \ / *)
+(* \ / This file is distributed under the terms of the *)
+(* v GNU General Public License Version 2 *)
+(* *)
+(**************************************************************************)
+
+include "basic_2/relocation/lexs_length.ma".
+include "basic_2/static/lfxs.ma".
+
+(* GENERIC EXTENSION ON REFERRED ENTRIES OF A CONTEXT-SENSITIVE REALTION ****)
+
+(* Forward lemmas with length for local environments ************************)
+
+lemma lfxs_fwd_length: ∀R,L1,L2,T. L1 ⦻*[R, T] L2 → |L1| = |L2|.
+#R #L1 #L2 #T * /2 width=4 by lexs_fwd_length/
+qed-.
--- /dev/null
+(**************************************************************************)
+(* ___ *)
+(* ||M|| *)
+(* ||A|| A project by Andrea Asperti *)
+(* ||T|| *)
+(* ||I|| Developers: *)
+(* ||T|| The HELM team. *)
+(* ||A|| http://helm.cs.unibo.it *)
+(* \ / *)
+(* \ / This file is distributed under the terms of the *)
+(* v GNU General Public License Version 2 *)
+(* *)
+(**************************************************************************)
+
+include "basic_2/relocation/lexs_lexs.ma".
+include "basic_2/static/frees_fqup.ma".
+include "basic_2/static/frees_frees.ma".
+include "basic_2/static/lfxs.ma".
+
+(* GENERIC EXTENSION ON REFERRED ENTRIES OF A CONTEXT-SENSITIVE REALTION ****)
+
+(* Main properties **********************************************************)
+
+theorem lfxs_bind: ∀R,p,I,L1,L2,V1,V2,T.
+ L1 ⦻*[R, V1] L2 → L1.ⓑ{I}V1 ⦻*[R, T] L2.ⓑ{I}V2 →
+ L1 ⦻*[R, ⓑ{p,I}V1.T] L2.
+#R #p #I #L1 #L2 #V1 #V2 #T * #f1 #HV #Hf1 * #f2 #HT #Hf2
+elim (lexs_fwd_pair … Hf2) -Hf2 #Hf2 #_ elim (sor_isfin_ex f1 (⫱f2))
+/3 width=7 by frees_fwd_isfin, frees_bind, lexs_join, isfin_tl, ex2_intro/
+qed.
+
+theorem lfxs_flat: ∀R,I,L1,L2,V,T.
+ L1 ⦻*[R, V] L2 → L1 ⦻*[R, T] L2 →
+ L1 ⦻*[R, ⓕ{I}V.T] L2.
+#R #I #L1 #L2 #V #T * #f1 #HV #Hf1 * #f2 #HT #Hf2 elim (sor_isfin_ex f1 f2)
+/3 width=7 by frees_fwd_isfin, frees_flat, lexs_join, ex2_intro/
+qed.
+
+theorem lfxs_trans: ∀R. lexs_frees_confluent R cfull →
+ ∀T. Transitive … (lfxs R T).
+#R #H1R #T #L1 #L * #f1 #Hf1 #HL1 #L2 * #f2 #Hf2 #HL2
+elim (H1R … Hf1 … HL1) #f #H0 #H1
+lapply (frees_mono … Hf2 … H0) -Hf2 -H0 #Hf2
+lapply (lexs_eq_repl_back … HL2 … Hf2) -f2 #HL2
+lapply (sle_lexs_trans … HL1 … H1) -HL1 // #Hl1
+@(ex2_intro … f)
+
+/4 width=7 by lreq_trans, lexs_eq_repl_back, ex2_intro/
+qed-.
+
+theorem lfxs_conf: ∀R. lexs_frees_confluent R cfull →
+ R_confluent2_lfxs R R R R →
+ ∀T. confluent … (lfxs R T).
+#R #H1R #H2R #T #L0 #L1 * #f1 #Hf1 #HL01 #L2 * #f #Hf #HL02
+lapply (frees_mono … Hf1 … Hf) -Hf1 #Hf12
+lapply (lexs_eq_repl_back … HL01 … Hf12) -f1 #HL01
+elim (lexs_conf … HL01 … HL02) /2 width=3 by ex2_intro/ [ | -HL01 -HL02 ]
+[ #L #HL1 #HL2
+ elim (H1R … Hf … HL01) -HL01 #f1 #Hf1 #H1
+ elim (H1R … Hf … HL02) -HL02 #f2 #Hf2 #H2
+ lapply (sle_lexs_trans … HL1 … H1) // -HL1 -H1 #HL1
+ lapply (sle_lexs_trans … HL2 … H2) // -HL2 -H2 #HL2
+ /3 width=5 by ex2_intro/
+| #g #I #K0 #V0 #n #HLK0 #Hgf #V1 #HV01 #V2 #HV02 #K1 #HK01 #K2 #HK02
+ elim (frees_drops_next … Hf … HLK0 … Hgf) -Hf -HLK0 -Hgf #g0 #Hg0 #H0
+ lapply (sle_lexs_trans … HK01 … H0) // -HK01 #HK01
+ lapply (sle_lexs_trans … HK02 … H0) // -HK02 #HK02
+ elim (H2R … HV01 … HV02 K1 … K2) /2 width=3 by ex2_intro/
+]
+qed-.
+++ /dev/null
-(**************************************************************************)
-(* ___ *)
-(* ||M|| *)
-(* ||A|| A project by Andrea Asperti *)
-(* ||T|| *)
-(* ||I|| Developers: *)
-(* ||T|| The HELM team. *)
-(* ||A|| http://helm.cs.unibo.it *)
-(* \ / *)
-(* \ / This file is distributed under the terms of the *)
-(* v GNU General Public License Version 2 *)
-(* *)
-(**************************************************************************)
-
-include "basic_2/relocation/drops_ceq.ma".
-include "basic_2/relocation/drops_lexs.ma".
-include "basic_2/static/frees_drops.ma".
-include "basic_2/static/lfxs.ma".
-
-(* GENERIC EXTENSION ON REFERRED ENTRIES OF A CONTEXT-SENSITIVE REALTION ****)
-
-definition dedropable_sn: predicate (relation3 lenv term term) ≝
- λR. ∀b,f,L1,K1. ⬇*[b, f] L1 ≡ K1 →
- ∀K2,T. K1 ⦻*[R, T] K2 → ∀U. ⬆*[f] T ≡ U →
- ∃∃L2. L1 ⦻*[R, U] L2 & ⬇*[b, f] L2 ≡ K2 & L1 ≡[f] L2.
-
-definition dropable_sn: predicate (relation3 lenv term term) ≝
- λR. ∀b,f,L1,K1. ⬇*[b, f] L1 ≡ K1 → 𝐔⦃f⦄ →
- ∀L2,U. L1 ⦻*[R, U] L2 → ∀T. ⬆*[f] T ≡ U →
- ∃∃K2. K1 ⦻*[R, T] K2 & ⬇*[b, f] L2 ≡ K2.
-
-definition dropable_dx: predicate (relation3 lenv term term) ≝
- λR. ∀L1,L2,U. L1 ⦻*[R, U] L2 →
- ∀b,f,K2. ⬇*[b, f] L2 ≡ K2 → 𝐔⦃f⦄ → ∀T. ⬆*[f] T ≡ U →
- ∃∃K1. ⬇*[b, f] L1 ≡ K1 & K1 ⦻*[R, T] K2.
-
-(* Properties with generic slicing for local environments *******************)
-
-(* Basic_2A1: includes: llpx_sn_lift_le llpx_sn_lift_ge *)
-lemma lfxs_liftable_dedropable: ∀R. (∀L. reflexive ? (R L)) →
- d_liftable2 R → dedropable_sn R.
-#R #H1R #H2R #b #f #L1 #K1 #HLK1 #K2 #T * #f1 #Hf1 #HK12 #U #HTU
-elim (frees_total L1 U) #f2 #Hf2
-lapply (frees_fwd_coafter … Hf2 … HLK1 … HTU … Hf1) -HTU #Hf
-elim (lexs_liftable_co_dedropable … H1R … H2R … HLK1 … HK12 … Hf) -f1 -K1
-/3 width=6 by cfull_lift, ex3_intro, ex2_intro/
-qed-.
-
-(* Inversion lemmas with generic slicing for local environments *************)
-
-(* Basic_2A1: restricts: llpx_sn_inv_lift_le llpx_sn_inv_lift_be llpx_sn_inv_lift_ge *)
-(* Basic_2A1: was: llpx_sn_drop_conf_O *)
-lemma lfxs_dropable_sn: ∀R. dropable_sn R.
-#R #b #f #L1 #K1 #HLK1 #H1f #L2 #U * #f2 #Hf2 #HL12 #T #HTU
-elim (frees_total K1 T) #f1 #Hf1
-lapply (frees_fwd_coafter … Hf2 … HLK1 … HTU … Hf1) -HTU #H2f
-elim (lexs_co_dropable_sn … HLK1 … HL12 … H2f) -f2 -L1
-/3 width=3 by ex2_intro/
-qed-.
-
-(* Basic_2A1: was: llpx_sn_drop_trans_O *)
-(* Note: the proof might be simplified *)
-lemma lfxs_dropable_dx: ∀R. dropable_dx R.
-#R #L1 #L2 #U * #f2 #Hf2 #HL12 #b #f #K2 #HLK2 #H1f #T #HTU
-elim (drops_isuni_ex … H1f L1) #K1 #HLK1
-elim (frees_total K1 T) #f1 #Hf1
-lapply (frees_fwd_coafter … Hf2 … HLK1 … HTU … Hf1) -K1 #H2f
-elim (lexs_co_dropable_dx … HL12 … HLK2 … H2f) -L2
-/4 width=9 by frees_inv_lifts, ex2_intro/
-qed-.
-
-(* Basic_2A1: was: llpx_sn_inv_lift_O *)
-lemma lfxs_inv_lift_bi: ∀R,L1,L2,U. L1 ⦻*[R, U] L2 →
- ∀K1,K2,i. ⬇*[i] L1 ≡ K1 → ⬇*[i] L2 ≡ K2 →
- ∀T. ⬆*[i] T ≡ U → K1 ⦻*[R, T] K2.
-#R #L1 #L2 #U #HL12 #K1 #K2 #i #HLK1 #HLK2 #T #HTU
-elim (lfxs_dropable_sn … HLK1 … HL12 … HTU) -L1 -U // #Y #HK12 #HY
-lapply (drops_mono … HY … HLK2) -L2 -i #H destruct //
-qed-.
-
-lemma lfxs_inv_lref_sn: ∀R,L1,L2,i. L1 ⦻*[R, #i] L2 → ∀I,K1,V1. ⬇*[i] L1 ≡ K1.ⓑ{I}V1 →
- ∃∃K2,V2. ⬇*[i] L2 ≡ K2.ⓑ{I}V2 & K1 ⦻*[R, V1] K2 & R K1 V1 V2.
-#R #L1 #L2 #i #HL12 #I #K1 #V1 #HLK1 elim (lfxs_dropable_sn … HLK1 … HL12 (#0)) -HLK1 -HL12 //
-#Y #HY #HLK2 elim (lfxs_inv_zero_pair_sn … HY) -HY
-#K2 #V2 #HK12 #HV12 #H destruct /2 width=5 by ex3_2_intro/
-qed-.
-
-lemma lfxs_inv_lref_dx: ∀R,L1,L2,i. L1 ⦻*[R, #i] L2 → ∀I,K2,V2. ⬇*[i] L2 ≡ K2.ⓑ{I}V2 →
- ∃∃K1,V1. ⬇*[i] L1 ≡ K1.ⓑ{I}V1 & K1 ⦻*[R, V1] K2 & R K1 V1 V2.
-#R #L1 #L2 #i #HL12 #I #K2 #V2 #HLK2 elim (lfxs_dropable_dx … HL12 … HLK2 … (#0)) -HLK2 -HL12 //
-#Y #HLK1 #HY elim (lfxs_inv_zero_pair_dx … HY) -HY
-#K1 #V1 #HK12 #HV12 #H destruct /2 width=5 by ex3_2_intro/
-qed-.
+++ /dev/null
-(**************************************************************************)
-(* ___ *)
-(* ||M|| *)
-(* ||A|| A project by Andrea Asperti *)
-(* ||T|| *)
-(* ||I|| Developers: *)
-(* ||T|| The HELM team. *)
-(* ||A|| http://helm.cs.unibo.it *)
-(* \ / *)
-(* \ / This file is distributed under the terms of the *)
-(* v GNU General Public License Version 2 *)
-(* *)
-(**************************************************************************)
-
-include "basic_2/static/frees_fqup.ma".
-include "basic_2/static/lfxs.ma".
-
-(* GENERIC EXTENSION ON REFERRED ENTRIES OF A CONTEXT-SENSITIVE REALTION ****)
-
-(* Advanced properties ******************************************************)
-
-lemma lfxs_refl: ∀R. (∀L. reflexive … (R L)) → ∀L,T. L ⦻*[R, T] L.
-#R #HR #L #T elim (frees_total L T) /3 width=3 by lexs_refl, ex2_intro/
-qed.
+++ /dev/null
-(**************************************************************************)
-(* ___ *)
-(* ||M|| *)
-(* ||A|| A project by Andrea Asperti *)
-(* ||T|| *)
-(* ||I|| Developers: *)
-(* ||T|| The HELM team. *)
-(* ||A|| http://helm.cs.unibo.it *)
-(* \ / *)
-(* \ / This file is distributed under the terms of the *)
-(* v GNU General Public License Version 2 *)
-(* *)
-(**************************************************************************)
-
-include "basic_2/relocation/lexs_length.ma".
-include "basic_2/static/lfxs.ma".
-
-(* GENERIC EXTENSION ON REFERRED ENTRIES OF A CONTEXT-SENSITIVE REALTION ****)
-
-(* Forward lemmas with length for local environments ************************)
-
-lemma lfxs_fwd_length: ∀R,L1,L2,T. L1 ⦻*[R, T] L2 → |L1| = |L2|.
-#R #L1 #L2 #T * /2 width=4 by lexs_fwd_length/
-qed-.
+++ /dev/null
-(**************************************************************************)
-(* ___ *)
-(* ||M|| *)
-(* ||A|| A project by Andrea Asperti *)
-(* ||T|| *)
-(* ||I|| Developers: *)
-(* ||T|| The HELM team. *)
-(* ||A|| http://helm.cs.unibo.it *)
-(* \ / *)
-(* \ / This file is distributed under the terms of the *)
-(* v GNU General Public License Version 2 *)
-(* *)
-(**************************************************************************)
-
-include "basic_2/relocation/lexs_lexs.ma".
-include "basic_2/static/frees_fqup.ma".
-include "basic_2/static/frees_frees.ma".
-include "basic_2/static/lfxs.ma".
-
-(* GENERIC EXTENSION ON REFERRED ENTRIES OF A CONTEXT-SENSITIVE REALTION ****)
-
-(* Main properties **********************************************************)
-
-theorem lfxs_bind: ∀R,p,I,L1,L2,V1,V2,T.
- L1 ⦻*[R, V1] L2 → L1.ⓑ{I}V1 ⦻*[R, T] L2.ⓑ{I}V2 →
- L1 ⦻*[R, ⓑ{p,I}V1.T] L2.
-#R #p #I #L1 #L2 #V1 #V2 #T * #f1 #HV #Hf1 * #f2 #HT #Hf2
-elim (lexs_fwd_pair … Hf2) -Hf2 #Hf2 #_ elim (sor_isfin_ex f1 (⫱f2))
-/3 width=7 by frees_fwd_isfin, frees_bind, lexs_join, isfin_tl, ex2_intro/
-qed.
-
-theorem lfxs_flat: ∀R,I,L1,L2,V,T.
- L1 ⦻*[R, V] L2 → L1 ⦻*[R, T] L2 →
- L1 ⦻*[R, ⓕ{I}V.T] L2.
-#R #I #L1 #L2 #V #T * #f1 #HV #Hf1 * #f2 #HT #Hf2 elim (sor_isfin_ex f1 f2)
-/3 width=7 by frees_fwd_isfin, frees_flat, lexs_join, ex2_intro/
-qed.
-
-theorem lfxs_trans: ∀R. lexs_frees_confluent R cfull →
- ∀T. Transitive … (lfxs R T).
-#R #H1R #T #L1 #L * #f1 #Hf1 #HL1 #L2 * #f2 #Hf2 #HL2
-elim (H1R … Hf1 … HL1) #f #H0 #H1
-lapply (frees_mono … Hf2 … H0) -Hf2 -H0 #Hf2
-lapply (lexs_eq_repl_back … HL2 … Hf2) -f2 #HL2
-lapply (sle_lexs_trans … HL1 … H1) -HL1 // #Hl1
-@(ex2_intro … f)
-
-/4 width=7 by lreq_trans, lexs_eq_repl_back, ex2_intro/
-qed-.
-
-theorem lfxs_conf: ∀R. lexs_frees_confluent R cfull →
- R_confluent2_lfxs R R R R →
- ∀T. confluent … (lfxs R T).
-#R #H1R #H2R #T #L0 #L1 * #f1 #Hf1 #HL01 #L2 * #f #Hf #HL02
-lapply (frees_mono … Hf1 … Hf) -Hf1 #Hf12
-lapply (lexs_eq_repl_back … HL01 … Hf12) -f1 #HL01
-elim (lexs_conf … HL01 … HL02) /2 width=3 by ex2_intro/ [ | -HL01 -HL02 ]
-[ #L #HL1 #HL2
- elim (H1R … Hf … HL01) -HL01 #f1 #Hf1 #H1
- elim (H1R … Hf … HL02) -HL02 #f2 #Hf2 #H2
- lapply (sle_lexs_trans … HL1 … H1) // -HL1 -H1 #HL1
- lapply (sle_lexs_trans … HL2 … H2) // -HL2 -H2 #HL2
- /3 width=5 by ex2_intro/
-| #g #I #K0 #V0 #n #HLK0 #Hgf #V1 #HV01 #V2 #HV02 #K1 #HK01 #K2 #HK02
- elim (frees_drops_next … Hf … HLK0 … Hgf) -Hf -HLK0 -Hgf #g0 #Hg0 #H0
- lapply (sle_lexs_trans … HK01 … H0) // -HK01 #HK01
- lapply (sle_lexs_trans … HK02 … H0) // -HK02 #HK02
- elim (H2R … HV01 … HV02 K1 … K2) /2 width=3 by ex2_intro/
-]
-qed-.
+++ /dev/null
-(**************************************************************************)
-(* ___ *)
-(* ||M|| *)
-(* ||A|| A project by Andrea Asperti *)
-(* ||T|| *)
-(* ||I|| Developers: *)
-(* ||T|| The HELM team. *)
-(* ||A|| http://helm.cs.unibo.it *)
-(* \ / *)
-(* \ / This file is distributed under the terms of the *)
-(* v GNU General Public License Version 2 *)
-(* *)
-(**************************************************************************)
-
-(* NOTATION FOR THE FORMAL SYSTEM λδ ****************************************)
-
-notation "hvbox( L1 break ⊆ [ term 46 l , break term 46 m ] break term 46 L2 )"
- non associative with precedence 45
- for @{ 'LRSubEq $L1 $l $k $L2 }.
--- /dev/null
+(**************************************************************************)
+(* ___ *)
+(* ||M|| *)
+(* ||A|| A project by Andrea Asperti *)
+(* ||T|| *)
+(* ||I|| Developers: *)
+(* ||T|| The HELM team. *)
+(* ||A|| http://helm.cs.unibo.it *)
+(* \ / *)
+(* \ / This file is distributed under the terms of the *)
+(* v GNU General Public License Version 2 *)
+(* *)
+(**************************************************************************)
+
+(* NOTATION FOR THE FORMAL SYSTEM λδ ****************************************)
+
+notation "hvbox( L1 break ⊆ [ term 46 l , break term 46 m ] break term 46 L2 )"
+ non associative with precedence 45
+ for @{ 'LRSubEq $L1 $l $k $L2 }.
+++ /dev/null
-include "basic_2/notation/functions/droppreds_3.ma".
-include "basic_2/grammar/lenv_length.ma".
-
-axiom pred_minus: ∀x,y. y < x → ⫰(x - y) = x - ⫯y.
-
-(*
-axiom drops_T_isuni_inv_refl: ∀n,L. ⬇*[n] L ≡ L → n = 0.
-
-lemma le_succ_trans: ∀m,n. ⫯m ≤ n → m ≤ n.
-/2 width=1 by lt_to_le/ qed-.
-*)
-
-lemma tls_pred: ∀f,n. 0 < n → ⫱*[n] f = ⫱ ⫱*[⫰n] f.
-#f #n #Hn >tls_S >S_pred //
-qed-.
-
-definition ltls (f): lenv → lenv → rtmap ≝ λL,K. ⫱*[|L|-|K|] f.
-
-interpretation "ltls (rtmap)" 'DropPreds L K f = (ltls f L K).
-
-lemma ltls_refl: ∀f,L1,L2. |L1| ≤ |L2| → ⫱*[L1, L2] f = f.
-#f #L1 #L2 #HL12 whd in ⊢ (??%?); >(eq_minus_O … HL12) -HL12 //
-qed.
-
-lemma ltls_pair2: ∀f,I,L1,L2,V. |L2| < |L1| → ⫱⫱*[L1, L2.ⓑ{I}V] f = ⫱*[L1, L2] f.
-#f #I #L1 #L2 #V #HL12 whd in ⊢ (??(?%)%); <pred_minus // <tls_pred //
-/2 width=1 by lt_plus_to_minus_r/
-qed-.
-
-lemma ltls_pair1_push: ∀f,I,L1,L2,V. |L2| ≤ |L1| → ⫱*[L1.ⓑ{I}V, L2] ↑f = ⫱*[L1, L2] f.
-#f #I #L1 #L2 #V #HL12 whd in ⊢ (??%%); >minus_Sn_m //
-qed.
-
-lemma ltls_pair1_next: ∀f,I,L1,L2,V. |L2| ≤ |L1| → ⫱*[L1.ⓑ{I}V, L2] ⫯f = ⫱*[L1, L2] f.
-#f #I #L1 #L2 #V #HL12 whd in ⊢ (??%%); >minus_Sn_m //
-qed.
-
-lemma ltls_sle_pair: ∀f1,f2,L1,L2. ⫱*[L2, L1] f2 ⊆ ⫱*[L1, L2] f1 →
- ∀I,V1. ⫱*[L2, L1.ⓑ{I}V1] f2 ⊆ ⫱*[L1.ⓑ{I}V1, L2] ⫯f1.
-#f1 #f2 #L1 #L2 elim (lt_or_ge (|L1|) (|L2|))
-[ #HL12 >ltls_refl in ⊢ (??%→?); /2 width=1 by lt_to_le/
- #Hf21 #I #V1 >ltls_refl in ⊢ (??%); //
- <(ltls_pair2 … I … V1 HL12) in Hf21; -HL12 /2 width=1 by sle_inv_tl1/
-| #HL21 >ltls_refl // #Hf21 #I #V1 >ltls_refl /2 width=1 by le_S/
- >ltls_pair1_next //
-]
-qed.
--- /dev/null
+(**************************************************************************)
+(* ___ *)
+(* ||M|| *)
+(* ||A|| A project by Andrea Asperti *)
+(* ||T|| *)
+(* ||I|| Developers: *)
+(* ||T|| The HELM team. *)
+(* ||A|| http://helm.cs.unibo.it *)
+(* \ / *)
+(* \ / This file is distributed under the terms of the *)
+(* v GNU General Public License Version 2 *)
+(* *)
+(**************************************************************************)
+
+(* NOTATION FOR THE FORMAL SYSTEM λδ ****************************************)
+
+notation "hvbox( ⫱ * [ term 46 L , break term 46 K ] term 46 f )"
+ non associative with precedence 46
+ for @{ 'DropPreds $L $K $f }.
--- /dev/null
+include "basic_2/notation/functions/droppreds_3.ma".
+include "basic_2/grammar/lenv_length.ma".
+
+axiom pred_minus: ∀x,y. y < x → ⫰(x - y) = x - ⫯y.
+
+(*
+axiom drops_T_isuni_inv_refl: ∀n,L. ⬇*[n] L ≡ L → n = 0.
+
+lemma le_succ_trans: ∀m,n. ⫯m ≤ n → m ≤ n.
+/2 width=1 by lt_to_le/ qed-.
+*)
+
+lemma tls_pred: ∀f,n. 0 < n → ⫱*[n] f = ⫱ ⫱*[⫰n] f.
+#f #n #Hn >tls_S >S_pred //
+qed-.
+
+definition ltls (f): lenv → lenv → rtmap ≝ λL,K. ⫱*[|L|-|K|] f.
+
+interpretation "ltls (rtmap)" 'DropPreds L K f = (ltls f L K).
+
+lemma ltls_refl: ∀f,L1,L2. |L1| ≤ |L2| → ⫱*[L1, L2] f = f.
+#f #L1 #L2 #HL12 whd in ⊢ (??%?); >(eq_minus_O … HL12) -HL12 //
+qed.
+
+lemma ltls_pair2: ∀f,I,L1,L2,V. |L2| < |L1| → ⫱⫱*[L1, L2.ⓑ{I}V] f = ⫱*[L1, L2] f.
+#f #I #L1 #L2 #V #HL12 whd in ⊢ (??(?%)%); <pred_minus // <tls_pred //
+/2 width=1 by lt_plus_to_minus_r/
+qed-.
+
+lemma ltls_pair1_push: ∀f,I,L1,L2,V. |L2| ≤ |L1| → ⫱*[L1.ⓑ{I}V, L2] ↑f = ⫱*[L1, L2] f.
+#f #I #L1 #L2 #V #HL12 whd in ⊢ (??%%); >minus_Sn_m //
+qed.
+
+lemma ltls_pair1_next: ∀f,I,L1,L2,V. |L2| ≤ |L1| → ⫱*[L1.ⓑ{I}V, L2] ⫯f = ⫱*[L1, L2] f.
+#f #I #L1 #L2 #V #HL12 whd in ⊢ (??%%); >minus_Sn_m //
+qed.
+
+lemma ltls_sle_pair: ∀f1,f2,L1,L2. ⫱*[L2, L1] f2 ⊆ ⫱*[L1, L2] f1 →
+ ∀I,V1. ⫱*[L2, L1.ⓑ{I}V1] f2 ⊆ ⫱*[L1.ⓑ{I}V1, L2] ⫯f1.
+#f1 #f2 #L1 #L2 elim (lt_or_ge (|L1|) (|L2|))
+[ #HL12 >ltls_refl in ⊢ (??%→?); /2 width=1 by lt_to_le/
+ #Hf21 #I #V1 >ltls_refl in ⊢ (??%); //
+ <(ltls_pair2 … I … V1 HL12) in Hf21; -HL12 /2 width=1 by sle_inv_tl1/
+| #HL21 >ltls_refl // #Hf21 #I #V1 >ltls_refl /2 width=1 by le_S/
+ >ltls_pair1_next //
+]
+qed.
--- /dev/null
+(**************************************************************************)
+(* ___ *)
+(* ||M|| *)
+(* ||A|| A project by Andrea Asperti *)
+(* ||T|| *)
+(* ||I|| Developers: *)
+(* ||T|| The HELM team. *)
+(* ||A|| http://helm.cs.unibo.it *)
+(* \ / *)
+(* \ / This file is distributed under the terms of the *)
+(* v GNU General Public License Version 2 *)
+(* *)
+(**************************************************************************)
+
+(* NOTATION FOR THE FORMAL SYSTEM λδ ****************************************)
+
+notation "hvbox( L1 ⋓ break [ term 46 T , break term 46 f ] break term 46 L2 ≡ break term 46 L )"
+ non associative with precedence 45
+ for @{ 'LazyOr $L1 $T $f $L2 $L }.
--- /dev/null
+(**************************************************************************)
+(* ___ *)
+(* ||M|| *)
+(* ||A|| A project by Andrea Asperti *)
+(* ||T|| *)
+(* ||I|| Developers: *)
+(* ||T|| The HELM team. *)
+(* ||A|| http://helm.cs.unibo.it *)
+(* \ / *)
+(* \ / This file is distributed under the terms of the *)
+(* v GNU General Public License Version 2 *)
+(* *)
+(**************************************************************************)
+
+(* NOTATION FOR THE FORMAL SYSTEM λδ ****************************************)
+
+notation "hvbox( ⦃G, L⦄ ⊢ break ⌘ ⦃ term 46 T ⦄ ≡ break term 46 k )"
+ non associative with precedence 45
+ for @{ 'ICM $L $T $s }.
+
+notation "hvbox( ⦃ term 46 h , break term 46 L ⦄ ⊢ break term 46 T ÷ break term 46 A )"
+ non associative with precedence 45
+ for @{ 'BinaryArity $h $L $T $A }.
+
+notation "hvbox( h ⊢ break term 46 L1 ÷ ⫃ break term 46 L2 )"
+ non associative with precedence 45
+ for @{ 'LRSubEqB $h $L1 $L2 }.
+
+notation "hvbox( L1 ⊢ ⬌ break term 46 L2 )"
+ non associative with precedence 45
+ for @{ 'PConvSn $L1 $L2 }.
+
+notation "hvbox( L1 ⊢ ⬌* break term 46 L2 )"
+ non associative with precedence 45
+ for @{ 'PConvSnStar $L1 $L2 }.
+
+notation "hvbox( ⦃ term 46 h , break term 46 L ⦄ ⊢ break term 46 T1 : break term 46 T2 )"
+ non associative with precedence 45
+ for @{ 'NativeType $h $L $T1 $T2 }.
+
+notation "hvbox( ⦃ term 46 h , break term 46 L ⦄ ⊢ break term 46 T1 : : break term 46 T2 )"
+ non associative with precedence 45
+ for @{ 'NativeTypeAlt $h $L $T1 $T2 }.
+
+notation "hvbox( ⦃ term 46 h , break term 46 L ⦄ ⊢ break term 46 T1 : * break term 46 T2 )"
+ non associative with precedence 45
+ for @{ 'NativeTypeStar $h $L $T1 $T2 }.
+++ /dev/null
-(**************************************************************************)
-(* ___ *)
-(* ||M|| *)
-(* ||A|| A project by Andrea Asperti *)
-(* ||T|| *)
-(* ||I|| Developers: *)
-(* ||T|| The HELM team. *)
-(* ||A|| http://helm.cs.unibo.it *)
-(* \ / *)
-(* \ / This file is distributed under the terms of the *)
-(* v GNU General Public License Version 2 *)
-(* *)
-(**************************************************************************)
-
-(* NOTATION FOR THE FORMAL SYSTEM λδ ****************************************)
-
-notation "hvbox( ⦃ term 46 G , break term 46 L ⦄ ⊢ break term 46 T1 break ▶ [ term 46 l , break term 46 m ] break term 46 T2 )"
- non associative with precedence 45
- for @{ 'PSubst $G $L $T1 $l $k $T2 }.
+++ /dev/null
-(**************************************************************************)
-(* ___ *)
-(* ||M|| *)
-(* ||A|| A project by Andrea Asperti *)
-(* ||T|| *)
-(* ||I|| Developers: *)
-(* ||T|| The HELM team. *)
-(* ||A|| http://helm.cs.unibo.it *)
-(* \ / *)
-(* \ / This file is distributed under the terms of the *)
-(* v GNU General Public License Version 2 *)
-(* *)
-(**************************************************************************)
-
-(* NOTATION FOR THE FORMAL SYSTEM λδ ****************************************)
-
-notation "hvbox( ⦃ term 46 G , break term 46 L ⦄ ⊢ break term 46 T1 break ▶ * [ term 46 l , break term 46 m ] break term 46 T2 )"
- non associative with precedence 45
- for @{ 'PSubstStar $G $L $T1 $l $k $T2 }.
+++ /dev/null
-(**************************************************************************)
-(* ___ *)
-(* ||M|| *)
-(* ||A|| A project by Andrea Asperti *)
-(* ||T|| *)
-(* ||I|| Developers: *)
-(* ||T|| The HELM team. *)
-(* ||A|| http://helm.cs.unibo.it *)
-(* \ / *)
-(* \ / This file is distributed under the terms of the *)
-(* v GNU General Public License Version 2 *)
-(* *)
-(**************************************************************************)
-
-(* NOTATION FOR THE FORMAL SYSTEM λδ ****************************************)
-
-notation "hvbox( ⦃ term 46 G , break term 46 L ⦄ ⊢ break term 46 T1 break ▶ ▶ * [ term 46 l , break term 46 m ] break term 46 T2 )"
- non associative with precedence 45
- for @{ 'PSubstStarAlt $G $L $T1 $l $k $T2 }.
+++ /dev/null
-(**************************************************************************)
-(* ___ *)
-(* ||M|| *)
-(* ||A|| A project by Andrea Asperti *)
-(* ||T|| *)
-(* ||I|| Developers: *)
-(* ||T|| The HELM team. *)
-(* ||A|| http://helm.cs.unibo.it *)
-(* \ / *)
-(* \ / This file is distributed under the terms of the *)
-(* v GNU General Public License Version 2 *)
-(* *)
-(**************************************************************************)
-
-(* NOTATION FOR THE FORMAL SYSTEM λδ ****************************************)
-
-notation "hvbox( ⦃G, L⦄ ⊢ break ⌘ ⦃ term 46 T ⦄ ≡ break term 46 k )"
- non associative with precedence 45
- for @{ 'ICM $L $T $s }.
-
-notation "hvbox( ⦃ term 46 h , break term 46 L ⦄ ⊢ break term 46 T ÷ break term 46 A )"
- non associative with precedence 45
- for @{ 'BinaryArity $h $L $T $A }.
-
-notation "hvbox( h ⊢ break term 46 L1 ÷ ⫃ break term 46 L2 )"
- non associative with precedence 45
- for @{ 'LRSubEqB $h $L1 $L2 }.
-
-notation "hvbox( L1 ⊢ ⬌ break term 46 L2 )"
- non associative with precedence 45
- for @{ 'PConvSn $L1 $L2 }.
-
-notation "hvbox( L1 ⊢ ⬌* break term 46 L2 )"
- non associative with precedence 45
- for @{ 'PConvSnStar $L1 $L2 }.
-
-notation "hvbox( ⦃ term 46 h , break term 46 L ⦄ ⊢ break term 46 T1 : break term 46 T2 )"
- non associative with precedence 45
- for @{ 'NativeType $h $L $T1 $T2 }.
-
-notation "hvbox( ⦃ term 46 h , break term 46 L ⦄ ⊢ break term 46 T1 : : break term 46 T2 )"
- non associative with precedence 45
- for @{ 'NativeTypeAlt $h $L $T1 $T2 }.
-
-notation "hvbox( ⦃ term 46 h , break term 46 L ⦄ ⊢ break term 46 T1 : * break term 46 T2 )"
- non associative with precedence 45
- for @{ 'NativeTypeStar $h $L $T1 $T2 }.
--- /dev/null
+(**************************************************************************)
+(* ___ *)
+(* ||M|| *)
+(* ||A|| A project by Andrea Asperti *)
+(* ||T|| *)
+(* ||I|| Developers: *)
+(* ||T|| The HELM team. *)
+(* ||A|| http://helm.cs.unibo.it *)
+(* \ / *)
+(* \ / This file is distributed under the terms of the *)
+(* v GNU General Public License Version 2 *)
+(* *)
+(**************************************************************************)
+
+include "basic_2/rt_transition/cpx_lfxs.ma".
+include "basic_2/rt_transition/cpm_cpx.ma".
+
+(* CONTEXT-SENSITIVE PARALLEL REDUCTION FOR TERMS ***************************)
+
+(* Properties with generic extension on referred entries ********************)
+
+(* Basic_2A1: was just: cpr_llpx_sn_conf *)
+lemma cpm_lfxs_conf: ∀R,n,h,G. s_r_confluent1 … (cpm n h G) (lfxs R).
+/3 width=5 by cpm_fwd_cpx, cpx_lfxs_conf/ qed-.
+++ /dev/null
-(**************************************************************************)
-(* ___ *)
-(* ||M|| *)
-(* ||A|| A project by Andrea Asperti *)
-(* ||T|| *)
-(* ||I|| Developers: *)
-(* ||T|| The HELM team. *)
-(* ||A|| http://helm.cs.unibo.it *)
-(* \ / *)
-(* \ / This file is distributed under the terms of the *)
-(* v GNU General Public License Version 2 *)
-(* *)
-(**************************************************************************)
-
-include "basic_2/multiple/llpx_sn_drop.ma".
-include "basic_2/reduction/cpr.ma".
-
-(* CONTEXT-SENSITIVE PARALLEL REDUCTION FOR TERMS ***************************)
-
-(* Properties on lazy sn pointwise extensions *******************************)
-
-lemma cpr_llpx_sn_conf: ∀R. (∀L. reflexive … (R L)) → d_liftable R → d_deliftable_sn R →
- ∀G. b_c_confluent1 … (cpr G) (llpx_sn R 0).
-#R #H1R #H2R #H3R #G #Ls #T1 #T2 #H elim H -G -Ls -T1 -T2
-[ //
-| #G #Ls #Ks #V1b #V2b #W2b #i #HLKs #_ #HVW2b #IHV12b #Ld #H elim (llpx_sn_inv_lref_ge_sn … H … HLKs) // -H
- #Kd #V1l #HLKd #HV1b #HV1sd
- lapply (drop_fwd_drop2 … HLKs) -HLKs #HLKs
- lapply (drop_fwd_drop2 … HLKd) -HLKd #HLKd
- @(llpx_sn_lift_le … HLKs HLKd … HVW2b) -HLKs -HLKd -HVW2b /2 width=1 by/ (**) (* full auto too slow *)
-| #a #I #G #Ls #V1 #V2 #T1 #T2 #_ #_ #IHV12 #IHT12 #Ld #H elim (llpx_sn_inv_bind_O … H) -H
- /4 width=5 by llpx_sn_bind_repl_SO, llpx_sn_bind/
-| #I #G #Ls #V1 #V2 #T1 #T2 #_ #_ #IHV12 #IHT12 #Ld #H elim (llpx_sn_inv_flat … H) -H
- /3 width=1 by llpx_sn_flat/
-| #G #Ls #V #T1 #T2 #T #_ #HT2 #IHT12 #Ld #H elim (llpx_sn_inv_bind_O … H) -H
- /3 width=10 by llpx_sn_inv_lift_le, drop_drop/
-| #G #Ls #V #T1 #T2 #_ #IHT12 #Ld #H elim (llpx_sn_inv_flat … H) -H /2 width=1 by/
-| #a #G #Ls #V1 #V2 #W1 #W2 #T1 #T2 #_ #_ #_ #IHV12 #IHW12 #IHT12 #Ld #H elim (llpx_sn_inv_flat … H) -H
- #HV1 #H elim (llpx_sn_inv_bind_O … H) -H
- /4 width=5 by llpx_sn_bind_repl_SO, llpx_sn_flat, llpx_sn_bind/
-| #a #G #Ls #V1 #V2 #V #W1 #W2 #T1 #T2 #_ #HV2 #_ #_ #IHV12 #IHW12 #IHT12 #Ld #H elim (llpx_sn_inv_flat … H) -H
- #HV1 #H elim (llpx_sn_inv_bind_O … H) -H //
- #HW1 #HT1 @llpx_sn_bind_O /2 width=1 by/ @llpx_sn_flat (**) (* full auto too slow *)
- [ /3 width=10 by llpx_sn_lift_le, drop_drop/
- | /3 width=4 by llpx_sn_bind_repl_O/
-]
-qed-.
#h #I #G #L #V1 #T1 #T * #c #H #p elim (cpg_fwd_bind1_minus … H p) -H
/3 width=4 by ex2_2_intro, ex_intro/
qed-.
+
+(* Basic eliminators ********************************************************)
+
+lemma cpx_ind: ∀h. ∀R:relation4 genv lenv term term.
+ (∀I,G,L. R G L (⓪{I}) (⓪{I})) →
+ (∀G,L,s. R G L (⋆s) (⋆(next h s))) →
+ (∀I,G,K,V1,V2,W2. ⦃G, K⦄ ⊢ V1 ⬈[h] V2 → R G K V1 V2 →
+ ⬆*[1] V2 ≡ W2 → R G (K.ⓑ{I}V1) (#0) W2
+ ) → (∀I,G,K,V,T,U,i. ⦃G, K⦄ ⊢ #i ⬈[h] T → R G K (#i) T →
+ ⬆*[1] T ≡ U → R G (K.ⓑ{I}V) (#⫯i) (U)
+ ) → (∀p,I,G,L,V1,V2,T1,T2. ⦃G, L⦄ ⊢ V1 ⬈[h] V2 → ⦃G, L.ⓑ{I}V1⦄ ⊢ T1 ⬈[h] T2 →
+ R G L V1 V2 → R G (L.ⓑ{I}V1) T1 T2 → R G L (ⓑ{p,I}V1.T1) (ⓑ{p,I}V2.T2)
+ ) → (∀I,G,L,V1,V2,T1,T2. ⦃G, L⦄ ⊢ V1 ⬈[h] V2 → ⦃G, L⦄ ⊢ T1 ⬈[h] T2 →
+ R G L V1 V2 → R G L T1 T2 → R G L (ⓕ{I}V1.T1) (ⓕ{I}V2.T2)
+ ) → (∀G,L,V,T1,T,T2. ⦃G, L.ⓓV⦄ ⊢ T1 ⬈[h] T → R G (L.ⓓV) T1 T →
+ ⬆*[1] T2 ≡ T → R G L (+ⓓV.T1) T2
+ ) → (∀G,L,V,T1,T2. ⦃G, L⦄ ⊢ T1 ⬈[h] T2 → R G L T1 T2 →
+ R G L (ⓝV.T1) T2
+ ) → (∀G,L,V1,V2,T. ⦃G, L⦄ ⊢ V1 ⬈[h] V2 → R G L V1 V2 →
+ R G L (ⓝV1.T) V2
+ ) → (∀p,G,L,V1,V2,W1,W2,T1,T2. ⦃G, L⦄ ⊢ V1 ⬈[h] V2 → ⦃G, L⦄ ⊢ W1 ⬈[h] W2 → ⦃G, L.ⓛW1⦄ ⊢ T1 ⬈[h] T2 →
+ R G L V1 V2 → R G L W1 W2 → R G (L.ⓛW1) T1 T2 →
+ R G L (ⓐV1.ⓛ{p}W1.T1) (ⓓ{p}ⓝW2.V2.T2)
+ ) → (∀p,G,L,V1,V,V2,W1,W2,T1,T2. ⦃G, L⦄ ⊢ V1 ⬈[h] V → ⦃G, L⦄ ⊢ W1 ⬈[h] W2 → ⦃G, L.ⓓW1⦄ ⊢ T1 ⬈[h] T2 →
+ R G L V1 V → R G L W1 W2 → R G (L.ⓓW1) T1 T2 →
+ ⬆*[1] V ≡ V2 → R G L (ⓐV1.ⓓ{p}W1.T1) (ⓓ{p}W2.ⓐV2.T2)
+ ) →
+ ∀G,L,T1,T2. ⦃G, L⦄ ⊢ T1 ⬈[h] T2 → R G L T1 T2.
+#h #R #IH1 #IH2 #IH3 #IH4 #IH5 #IH6 #IH7 #IH8 #IH9 #IH10 #IH11 #G #L #T1 #T2
+* #c #H elim H -c -G -L -T1 -T2 /3 width=4 by ex_intro/
+qed-.
--- /dev/null
+(**************************************************************************)
+(* ___ *)
+(* ||M|| *)
+(* ||A|| A project by Andrea Asperti *)
+(* ||T|| *)
+(* ||I|| Developers: *)
+(* ||T|| The HELM team. *)
+(* ||A|| http://helm.cs.unibo.it *)
+(* \ / *)
+(* \ / This file is distributed under the terms of the *)
+(* v GNU General Public License Version 2 *)
+(* *)
+(**************************************************************************)
+
+include "basic_2/relocation/lifts_tdeq.ma".
+include "basic_2/static/lfdeq.ma".
+include "basic_2/rt_transition/lfpx.ma".
+
+(* UNCOUNTED CONTEXT-SENSITIVE PARALLEL RT-TRANSITION FOR TERMS *************)
+
+(* Properties with degree-based equivalence for terms ***********************)
+
+(* Basic_2A1: was just: cpx_lleq_conf *)
+lemma cpx_tdeq_conf_lexs: ∀h,o,G. R_confluent2_lfxs … (cpx h G) (cdeq h o) (cpx h G) (cdeq h o).
+#h #o #G #L0 #T0 #T1 #H @(cpx_ind … H) -G -L0 -T0 -T1 /2 width=3 by ex2_intro/
+[ #G #L0 #s0 #X0 #H0 #L1 #HL01 #L2 #HL02
+ elim (tdeq_inv_sort1 … H0) -H0 #s1 #d1 #Hs0 #Hs1 #H destruct
+ /4 width=3 by tdeq_sort, deg_next, ex2_intro/
+| #I #G #K0 #V0 #V1 #W1 #_ #IH #HVW1 #T2 #H0 #L1 #H1 #L2 #H2
+ >(tdeq_inv_lref1 … H0) -H0
+ elim (lfpx_inv_zero_pair_sn … H1) -H1 #K1 #X1 #HK01 #HX1 #H destruct
+ elim (lfdeq_inv_zero_pair_sn … H2) -H2 #K2 #X2 #HK02 #HX2 #H destruct
+ elim (IH X2 … HK01 … HK02) // -K0 -V0 #V #HV1 #HV2
+ elim (tdeq_lifts … HV1 … HVW1) -V1 /3 width=5 by cpx_delta, ex2_intro/
+| #I #G #K0 #V0 #V1 #W1 #i #_ #IH #HVW1 #T2 #H0 #L1 #H1 #L2 #H2
+ >(tdeq_inv_lref1 … H0) -H0
+ elim (lfpx_inv_lref_pair_sn … H1) -H1 #K1 #X1 #HK01 #H destruct
+ elim (lfdeq_inv_lref_pair_sn … H2) -H2 #K2 #X2 #HK02 #H destruct
+ elim (IH … HK01 … HK02) [|*: //] -K0 -V0 #V #HV1 #HV2
+ elim (tdeq_lifts … HV1 … HVW1) -V1 /3 width=5 by cpx_lref, ex2_intro/
+| #p #I #G #L0 #V0 #V1 #T0 #T1 #_ #_ #IHV #IHT #X0 #H0 #L1 #H1 #L2 #H2
+ elim (tdeq_inv_pair1 … H0) -H0 #V2 #T2 #HV02 #HT02 #H destruct
+ elim (lfpx_inv_bind … H1) -H1 #HL01 #H1
+ elim (lfdeq_inv_bind … H2) -H2 #HL02 #H2
+ lapply (lfdeq_pair_repl_dx … H2 … HV02) -H2 #H2
+ elim (IHV … HV02 … HL01 … HL02) -IHV -HV02 -HL01 -HL02
+ elim (IHT … HT02 … H1 … H2) -L0 -T0
+ /3 width=5 by cpx_bind, tdeq_pair, ex2_intro/
+| #I #G #L0 #V0 #V1 #T0 #T1 #_ #_ #IHV #IHT #X0 #H0 #L1 #H1 #L2 #H2
+ elim (tdeq_inv_pair1 … H0) -H0 #V2 #T2 #HV02 #HT02 #H destruct
+ elim (lfpx_inv_flat … H1) -H1 #HL01 #H1
+ elim (lfdeq_inv_flat … H2) -H2 #HL02 #H2
+ elim (IHV … HV02 … HL01 … HL02) -IHV -HV02 -HL01 -HL02
+ elim (IHT … HT02 … H1 … H2) -L0 -V0 -T0
+ /3 width=5 by cpx_flat, tdeq_pair, ex2_intro/
+| #G #L0 #V0 #T0 #T1 #U1 #_ #IH #HUT1 #X0 #H0 #L1 #H1 #L2 #H2
+ elim (tdeq_inv_pair1 … H0) -H0 #V2 #T2 #HV02 #HT02 #H destruct
+ elim (lfpx_inv_bind … H1) -H1 #HL01 #H1
+ elim (lfdeq_inv_bind … H2) -H2 #HL02 #H2
+ lapply (lfdeq_pair_repl_dx … H2 … HV02) -H2 -HV02 #H2
+ elim (IH … HT02 … H1 … H2) -L0 -T0 #T #HT1
+ elim (tdeq_inv_lifts … HT1 … HUT1) -T1
+ /3 width=5 by cpx_zeta, ex2_intro/
+| #G #L0 #V0 #T0 #T1 #_ #IH #X0 #H0 #L1 #H1 #L2 #H2
+ elim (tdeq_inv_pair1 … H0) -H0 #V2 #T2 #_ #HT02 #H destruct
+ elim (lfpx_inv_flat … H1) -H1 #HL01 #H1
+ elim (lfdeq_inv_flat … H2) -H2 #HL02 #H2
+ elim (IH … HT02 … H1 … H2) -L0 -V0 -T0
+ /3 width=3 by cpx_eps, ex2_intro/
+| #G #L0 #V0 #T0 #T1 #_ #IH #X0 #H0 #L1 #H1 #L2 #H2
+ elim (tdeq_inv_pair1 … H0) -H0 #V2 #T2 #HV02 #_ #H destruct
+ elim (lfpx_inv_flat … H1) -H1 #HL01 #H1
+ elim (lfdeq_inv_flat … H2) -H2 #HL02 #H2
+ elim (IH … HV02 … HL01 … HL02) -L0 -V0 -T1
+ /3 width=3 by cpx_ee, ex2_intro/
+| #p #G #L0 #V0 #V1 #W0 #W1 #T0 #T1 #_ #_ #_ #IHV #IHW #IHT #X0 #H0 #L1 #H1 #L2 #H2
+ elim (tdeq_inv_pair1 … H0) -H0 #V2 #X #HV02 #H0 #H destruct
+ elim (tdeq_inv_pair1 … H0) -H0 #W2 #T2 #HW02 #HT02 #H destruct
+ elim (lfpx_inv_flat … H1) -H1 #H1LV0 #H1
+ elim (lfpx_inv_bind … H1) -H1 #H1LW0 #H1LT0
+ elim (lfdeq_inv_flat … H2) -H2 #H2LV0 #H2
+ elim (lfdeq_inv_bind … H2) -H2 #H2LW0 #H2LT0
+ lapply (lfdeq_pair_repl_dx … H2LT0 … HW02) -H2LT0 #H2LT0
+ elim (IHV … HV02 … H1LV0 … H2LV0) -IHV -HV02 -H1LV0 -H2LV0
+ elim (IHW … HW02 … H1LW0 … H2LW0) -IHW -HW02 -H1LW0 -H2LW0
+ elim (IHT … HT02 … H1LT0 … H2LT0) -L0 -V0 -T0
+ /4 width=7 by cpx_beta, tdeq_pair, ex2_intro/ (* note: 2 tdeq_pair *)
+| #p #G #L0 #V0 #V1 #U1 #W0 #W1 #T0 #T1 #_ #_ #_ #IHV #IHW #IHT #HVU1 #X0 #H0 #L1 #H1 #L2 #H2
+ elim (tdeq_inv_pair1 … H0) -H0 #V2 #X #HV02 #H0 #H destruct
+ elim (tdeq_inv_pair1 … H0) -H0 #W2 #T2 #HW02 #HT02 #H destruct
+ elim (lfpx_inv_flat … H1) -H1 #H1LV0 #H1
+ elim (lfpx_inv_bind … H1) -H1 #H1LW0 #H1LT0
+ elim (lfdeq_inv_flat … H2) -H2 #H2LV0 #H2
+ elim (lfdeq_inv_bind … H2) -H2 #H2LW0 #H2LT0
+ lapply (lfdeq_pair_repl_dx … H2LT0 … HW02) -H2LT0 #H2LT0
+ elim (IHV … HV02 … H1LV0 … H2LV0) -IHV -HV02 -H1LV0 -H2LV0 #V #HV1
+ elim (IHW … HW02 … H1LW0 … H2LW0) -IHW -HW02 -H1LW0 -H2LW0
+ elim (IHT … HT02 … H1LT0 … H2LT0) -L0 -V0 -T0
+ elim (tdeq_lifts … HV1 … HVU1) -V1
+ /4 width=9 by cpx_theta, tdeq_pair, ex2_intro/ (* note: 2 tdeq_pair *)
+]
+qed-.
+(*
+lemma cpx_lleq_conf: ∀h,o,G,L2,T1,T2. ⦃G, L2⦄ ⊢ T1 ⬈[h, o] T2 →
+ ∀L1. L2 ≡[T1, 0] L1 → ⦃G, L1⦄ ⊢ T1 ⬈[h, o] T2.
+/3 width=3 by lleq_cpx_trans, lleq_sym/ qed-.
+
+lemma cpx_lleq_conf_sn: ∀h,o,G. s_r_confluent1 … (cpx h o G) (lleq 0).
+/3 width=6 by cpx_llpx_sn_conf, lift_mono, ex2_intro/ qed-.
+
+lemma cpx_lleq_conf_dx: ∀h,o,G,L2,T1,T2. ⦃G, L2⦄ ⊢ T1 ⬈[h, o] T2 →
+ ∀L1. L1 ≡[T1, 0] L2 → L1 ≡[T2, 0] L2.
+/4 width=6 by cpx_lleq_conf_sn, lleq_sym/ qed-.
+*)
\ No newline at end of file
--- /dev/null
+(**************************************************************************)
+(* ___ *)
+(* ||M|| *)
+(* ||A|| A project by Andrea Asperti *)
+(* ||T|| *)
+(* ||I|| Developers: *)
+(* ||T|| The HELM team. *)
+(* ||A|| http://helm.cs.unibo.it *)
+(* \ / *)
+(* \ / This file is distributed under the terms of the *)
+(* v GNU General Public License Version 2 *)
+(* *)
+(**************************************************************************)
+
+include "basic_2/rt_transition/lfpx_frees.ma".
+
+(* UNCOUNTED CONTEXT-SENSITIVE PARALLEL RT-TRANSITION FOR TERMS *************)
+
+(* Properties with generic extension on referred entries ********************)
+
+(* Note: lemma 1000 *)
+(* Basic_2A1: was just: cpx_llpx_sn_conf *)
+lemma cpx_lfxs_conf: ∀R,h,G. s_r_confluent1 … (cpx h G) (lfxs R).
+#R #h #G #L1 #T1 #T2 #H #L2 * #f1 #Hf1 elim (cpx_frees_conf … Hf1 … H) -T1
+/3 width=5 by sle_lexs_trans, ex2_intro/
+qed-.
+++ /dev/null
-(**************************************************************************)
-(* ___ *)
-(* ||M|| *)
-(* ||A|| A project by Andrea Asperti *)
-(* ||T|| *)
-(* ||I|| Developers: *)
-(* ||T|| The HELM team. *)
-(* ||A|| http://helm.cs.unibo.it *)
-(* \ / *)
-(* \ / This file is distributed under the terms of the *)
-(* v GNU General Public License Version 2 *)
-(* *)
-(**************************************************************************)
-
-include "basic_2/multiple/lleq_drop.ma".
-include "basic_2/reduction/cpx_llpx_sn.ma".
-
-(* UNCOUNTED CONTEXT-SENSITIVE PARALLEL RT-TRANSITION FOR TERMS *************)
-
-(* Properties on lazy equivalence for local environments ********************)
-
-lemma lleq_cpx_trans: ∀h,o,G,L2,T1,T2. ⦃G, L2⦄ ⊢ T1 ⬈[h, o] T2 →
- ∀L1. L1 ≡[T1, 0] L2 → ⦃G, L1⦄ ⊢ T1 ⬈[h, o] T2.
-#h #o #G #L2 #T1 #T2 #H elim H -G -L2 -T1 -T2 /2 width=2 by cpx_st/
-[ #I #G #L2 #K2 #V1 #V2 #W2 #i #HLK2 #_ #HVW2 #IHV12 #L1 #H elim (lleq_fwd_lref_dx … H … HLK2) -L2
- [ #H elim (ylt_yle_false … H) //
- | * /3 width=7 by cpx_delta/
- ]
-| #a #I #G #L2 #V1 #V2 #T1 #T2 #_ #_ #IHV12 #IHT12 #L1 #H elim (lleq_inv_bind_O … H) -H
- /3 width=1 by cpx_bind/
-| #I #G #L2 #V1 #V2 #T1 #T2 #_ #_ #IHV12 #IHT12 #L1 #H elim (lleq_inv_flat … H) -H
- /3 width=1 by cpx_flat/
-| #G #L2 #V2 #T1 #T #T2 #_ #HT2 #IHT1 #L1 #H elim (lleq_inv_bind_O … H) -H
- /3 width=3 by cpx_zeta/
-| #G #L2 #W1 #T1 #T2 #_ #IHT12 #L1 #H elim (lleq_inv_flat … H) -H
- /3 width=1 by cpx_eps/
-| #G #L2 #W1 #W2 #T1 #_ #IHW12 #L1 #H elim (lleq_inv_flat … H) -H
- /3 width=1 by cpx_ct/
-| #a #G #L1 #V1 #V2 #W1 #W2 #T1 #T2 #_ #_ #_ #IHV12 #IHW12 #IHT12 #L1 #H elim (lleq_inv_flat … H) -H
- #HV1 #H elim (lleq_inv_bind_O … H) -H /3 width=1 by cpx_beta/
-| #a #G #L1 #V1 #V #V2 #W1 #W2 #T1 #T2 #_ #HV2 #_ #_ #IHV1 #IHW12 #IHT12 #L1 #H elim (lleq_inv_flat … H) -H
- #HV1 #H elim (lleq_inv_bind_O … H) -H /3 width=3 by cpx_theta/
-]
-qed-.
-
-lemma cpx_lleq_conf: ∀h,o,G,L2,T1,T2. ⦃G, L2⦄ ⊢ T1 ⬈[h, o] T2 →
- ∀L1. L2 ≡[T1, 0] L1 → ⦃G, L1⦄ ⊢ T1 ⬈[h, o] T2.
-/3 width=3 by lleq_cpx_trans, lleq_sym/ qed-.
-
-lemma cpx_lleq_conf_sn: ∀h,o,G. b_c_confluent1 … (cpx h o G) (lleq 0).
-/3 width=6 by cpx_llpx_sn_conf, lift_mono, ex2_intro/ qed-.
-
-lemma cpx_lleq_conf_dx: ∀h,o,G,L2,T1,T2. ⦃G, L2⦄ ⊢ T1 ⬈[h, o] T2 →
- ∀L1. L1 ≡[T1, 0] L2 → L1 ≡[T2, 0] L2.
-/4 width=6 by cpx_lleq_conf_sn, lleq_sym/ qed-.
+++ /dev/null
-(**************************************************************************)
-(* ___ *)
-(* ||M|| *)
-(* ||A|| A project by Andrea Asperti *)
-(* ||T|| *)
-(* ||I|| Developers: *)
-(* ||T|| The HELM team. *)
-(* ||A|| http://helm.cs.unibo.it *)
-(* \ / *)
-(* \ / This file is distributed under the terms of the *)
-(* v GNU General Public License Version 2 *)
-(* *)
-(**************************************************************************)
-
-include "basic_2/multiple/llpx_sn_drop.ma".
-include "basic_2/reduction/cpx.ma".
-
-(* UNCOUNTED CONTEXT-SENSITIVE PARALLEL RT-TRANSITION FOR TERMS *************)
-
-(* Properties on lazy sn pointwise extensions *******************************)
-
-(* Note: lemma 1000 *)
-lemma cpx_llpx_sn_conf: ∀R. (∀L. reflexive … (R L)) → d_liftable R → d_deliftable_sn R →
- ∀h,o,G. b_c_confluent1 … (cpx h o G) (llpx_sn R 0).
-#R #H1R #H2R #H3R #h #o #G #Ls #T1 #T2 #H elim H -G -Ls -T1 -T2
-[ //
-| /3 width=4 by llpx_sn_fwd_length, llpx_sn_sort/
-| #I #G #Ls #Ks #V1b #V2b #W2b #i #HLKs #_ #HVW2b #IHV12b #Ld #H elim (llpx_sn_inv_lref_ge_sn … H … HLKs) // -H
- #Kd #V1l #HLKd #HV1b #HV1sd
- lapply (drop_fwd_drop2 … HLKs) -HLKs #HLKs
- lapply (drop_fwd_drop2 … HLKd) -HLKd #HLKd
- @(llpx_sn_lift_le … HLKs HLKd … HVW2b) -HLKs -HLKd -HVW2b /2 width=1 by/ (**) (* full auto too slow *)
-| #a #I #G #Ls #V1 #V2 #T1 #T2 #_ #_ #IHV12 #IHT12 #Ld #H elim (llpx_sn_inv_bind_O … H) -H
- /4 width=5 by llpx_sn_bind_repl_SO, llpx_sn_bind/
-| #I #G #Ls #V1 #V2 #T1 #T2 #_ #_ #IHV12 #IHT12 #Ld #H elim (llpx_sn_inv_flat … H) -H
- /3 width=1 by llpx_sn_flat/
-| #G #Ls #V #T1 #T2 #T #_ #HT2 #IHT12 #Ld #H elim (llpx_sn_inv_bind_O … H) -H
- /3 width=10 by llpx_sn_inv_lift_le, drop_drop/
-| #G #Ls #V #T1 #T2 #_ #IHT12 #Ld #H elim (llpx_sn_inv_flat … H) -H /2 width=1 by/
-| #G #Ls #V1 #V2 #T #_ #IHV12 #Ld #H elim (llpx_sn_inv_flat … H) -H /2 width=1 by/
-| #a #G #Ls #V1 #V2 #W1 #W2 #T1 #T2 #_ #_ #_ #IHV12 #IHW12 #IHT12 #Ld #H elim (llpx_sn_inv_flat … H) -H
- #HV1 #H elim (llpx_sn_inv_bind_O … H) -H
- /4 width=5 by llpx_sn_bind_repl_SO, llpx_sn_flat, llpx_sn_bind/
-| #a #G #Ls #V1 #V2 #V #W1 #W2 #T1 #T2 #_ #HV2 #_ #_ #IHV12 #IHW12 #IHT12 #Ld #H elim (llpx_sn_inv_flat … H) -H
- #HV1 #H elim (llpx_sn_inv_bind_O … H) -H //
- #HW1 #HT1 @llpx_sn_bind_O /2 width=1 by/ @llpx_sn_flat (**) (* full auto too slow *)
- [ /3 width=10 by llpx_sn_lift_le, drop_drop/
- | /3 width=4 by llpx_sn_bind_repl_O/
-]
-qed-.
+++ /dev/null
-(**************************************************************************)
-(* ___ *)
-(* ||M|| *)
-(* ||A|| A project by Andrea Asperti *)
-(* ||T|| *)
-(* ||I|| Developers: *)
-(* ||T|| The HELM team. *)
-(* ||A|| http://helm.cs.unibo.it *)
-(* \ / *)
-(* \ / This file is distributed under the terms of the *)
-(* v GNU General Public License Version 2 *)
-(* *)
-(**************************************************************************)
-
-include "basic_2/substitution/drop_lreq.ma".
-include "basic_2/reduction/cpx.ma".
-
-(* UNCOUNTED CONTEXT-SENSITIVE PARALLEL RT-TRANSITION FOR TERMS *************)
-
-(* Properties on equivalence for local environments *************************)
-
-lemma lreq_cpx_trans: ∀h,o,G. lsub_trans … (cpx h o G) (lreq 0 (∞)).
-#h #o #G #L1 #T1 #T2 #H elim H -G -L1 -T1 -T2
-[ //
-| /2 width=2 by cpx_st/
-| #I #G #L1 #K1 #V1 #V2 #W2 #i #HLK1 #_ #HVW2 #IHV12 #L2 #HL12
- elim (lreq_drop_trans_be … HL12 … HLK1) // -HL12 -HLK1 /3 width=7 by cpx_delta/
-|4,9: /4 width=1 by cpx_bind, cpx_beta, lreq_pair_O_Y/
-|5,7,8: /3 width=1 by cpx_flat, cpx_eps, cpx_ct/
-|6,10: /4 width=3 by cpx_zeta, cpx_theta, lreq_pair_O_Y/
-]
-qed-.
(**************************************************************************)
include "basic_2/notation/relations/btpredproper_8.ma".
-include "basic_2/substitution/fqu.ma".
-include "basic_2/multiple/lleq.ma".
-include "basic_2/reduction/lpx.ma".
+include "basic_2/s_transition/fqu.ma".
+include "basic_2/static/lfdeq.ma".
+include "basic_2/rt_transition/lfpr_lfpx.ma".
-(* "RST" PROPER PARALLEL COMPUTATION FOR CLOSURES ***************************)
+(* PROPER PARALLEL RST-TRANSITION FOR CLOSURES ******************************)
inductive fpb (h) (o) (G1) (L1) (T1): relation3 genv lenv term ≝
| fpb_fqu: ∀G2,L2,T2. ⦃G1, L1, T1⦄ ⊐ ⦃G2, L2, T2⦄ → fpb h o G1 L1 T1 G2 L2 T2
-| fpb_cpx: â\88\80T2. â¦\83G1, L1â¦\84 â\8a¢ T1 â\9e¡[h, o] T2 â\86\92 (T1 = T2 → ⊥) → fpb h o G1 L1 T1 G1 L1 T2
-| fpb_lpx: â\88\80L2. â¦\83G1, L1â¦\84 â\8a¢ â\9e¡[h, o] L2 â\86\92 (L1 â\89¡[T1, 0] L2 → ⊥) → fpb h o G1 L1 T1 G1 L2 T1
+| fpb_cpx: â\88\80T2. â¦\83G1, L1â¦\84 â\8a¢ T1 â¬\88[h] T2 â\86\92 (T1 â\89¡[h, o] T2 → ⊥) → fpb h o G1 L1 T1 G1 L1 T2
+| fpb_lpx: â\88\80L2. â¦\83G1, L1â¦\84 â\8a¢ â¬\88[h, T1] L2 â\86\92 (L1 â\89¡[h, o, T1] L2 → ⊥) → fpb h o G1 L1 T1 G1 L2 T1
.
interpretation
- "'rst' proper parallel reduction (closure)"
+ "proper parallel rst-transition (closure)"
'BTPRedProper h o G1 L1 T1 G2 L2 T2 = (fpb h o G1 L1 T1 G2 L2 T2).
(* Basic properties *********************************************************)
-lemma cpr_fpb: ∀h,o,G,L,T1,T2. ⦃G, L⦄ ⊢ T1 ➡ T2 → (T1 = T2 → ⊥) →
+(* Basic_2A1: includes: cpr_fpb *)
+lemma cpm_fpb: ∀n,h,o,G,L,T1,T2. ⦃G, L⦄ ⊢ T1 ➡[n, h] T2 → (T1 ≡[h, o] T2 → ⊥) →
⦃G, L, T1⦄ ≻[h, o] ⦃G, L, T2⦄.
-/3 width=1 by fpb_cpx, cpr_cpx/ qed.
+/3 width=2 by fpb_cpx, cpm_fwd_cpx/ qed.
-lemma lpr_fpb: ∀h,o,G,L1,L2,T. ⦃G, L1⦄ ⊢ ➡ L2 → (L1 ≡[T, 0] L2 → ⊥) →
+lemma lpr_fpb: ∀h,o,G,L1,L2,T. ⦃G, L1⦄ ⊢ ➡[h, T] L2 → (L1 ≡[h, o, T] L2 → ⊥) →
⦃G, L1, T⦄ ≻[h, o] ⦃G, L2, T⦄.
-/3 width=1 by fpb_lpx, lpr_lpx/ qed.
+/3 width=1 by fpb_lpx, lfpr_fwd_lfpx/ qed.
+++ /dev/null
-(**************************************************************************)
-(* ___ *)
-(* ||M|| *)
-(* ||A|| A project by Andrea Asperti *)
-(* ||T|| *)
-(* ||I|| Developers: *)
-(* ||T|| The HELM team. *)
-(* ||A|| http://helm.cs.unibo.it *)
-(* \ / *)
-(* \ / This file is distributed under the terms of the *)
-(* v GNU General Public License Version 2 *)
-(* *)
-(**************************************************************************)
-
-include "basic_2/unfold/lstas_da.ma".
-include "basic_2/reduction/cpx_lift.ma".
-include "basic_2/reduction/fpb.ma".
-
-(* "RST" PROPER PARALLEL COMPUTATION FOR CLOSURES ***************************)
-
-(* Advanced properties ******************************************************)
-
-lemma sta_fpb: ∀h,o,G,L,T1,T2,d. ⦃G, L⦄ ⊢ T1 ▪[h, o] d+1 →
- ⦃G, L⦄ ⊢ T1 •*[h, 1] T2 → ⦃G, L, T1⦄ ≻[h, o] ⦃G, L, T2⦄.
-#h #o #G #L #T1 #T2 #d #HT1 #HT12 elim (eq_term_dec T1 T2)
-/3 width=2 by fpb_cpx, sta_cpx/ #H destruct
-elim (lstas_inv_refl_pos h G L T2 0) //
-qed.
+++ /dev/null
-(**************************************************************************)
-(* ___ *)
-(* ||M|| *)
-(* ||A|| A project by Andrea Asperti *)
-(* ||T|| *)
-(* ||I|| Developers: *)
-(* ||T|| The HELM team. *)
-(* ||A|| http://helm.cs.unibo.it *)
-(* \ / *)
-(* \ / This file is distributed under the terms of the *)
-(* v GNU General Public License Version 2 *)
-(* *)
-(**************************************************************************)
-
-include "basic_2/reduction/cpx_lift.ma".
-include "basic_2/reduction/fpbq.ma".
-
-(* "QRST" PARALLEL REDUCTION FOR CLOSURES ***********************************)
-
-(* Advanced properties ******************************************************)
-
-lemma sta_fpbq: ∀h,o,G,L,T1,T2,d.
- ⦃G, L⦄ ⊢ T1 ▪[h, o] d+1 → ⦃G, L⦄ ⊢ T1 •*[h, 1] T2 →
- ⦃G, L, T1⦄ ≽[h, o] ⦃G, L, T2⦄.
-/3 width=4 by fpbq_cpx, sta_cpx/ qed.
cpg.ma cpg_simple.ma cpg_drops.ma cpg_lsubr.ma
-cpx.ma cpx_simple.ma cpx_drops.ma cpx_fqus.ma cpx_lsubr.ma
+cpx.ma cpx_simple.ma cpx_drops.ma cpx_fqus.ma cpx_lsubr.ma cpx_lfxs.ma cpx_lfdeq.ma
lfpx.ma lfpx_length.ma lfpx_drops.ma lfpx_fqup.ma lfpx_frees.ma lfpx_aaa.ma
-cpm.ma cpm_simple.ma cpm_drops.ma cpm_lsubr.ma cpm_cpx.ma
+cpm.ma cpm_simple.ma cpm_drops.ma cpm_lsubr.ma cpm_lfxs.ma cpm_cpx.ma
cpr.ma cpr_drops.ma
lfpr.ma lfpr_length.ma lfpr_drops.ma lfpr_fqup.ma lfpr_frees.ma lfpr_aaa.ma lfpr_lfpx.ma lfpr_lfpr.ma
+fpb.ma
include "basic_2/notation/relations/lazyeq_8.ma".
include "basic_2/syntax/genv.ma".
-include "basic_2/static/lfdeq_fqup.ma".
+include "basic_2/static/lfdeq.ma".
(* DEGREE-BASED EQUIVALENCE FOR CLOSURES ON REFERRED ENTRIES ****************)
*)
class "water"
[ { "rt-transition" * } {
-(*
- [ { "parallel qrst-reduction" * } {
- [ "fpbq ( ⦃?,?,?⦄ ≽[?,?] ⦃?,?,?⦄ )" "fpbq_alt ( ⦃?,?,?⦄ ≽≽[?,?] ⦃?,?,?⦄ )" "fpbq_lift" + "fpbq_aaa" * ]
- [ "fpb ( ⦃?,?,?⦄ ≻[?,?] ⦃?,?,?⦄ )" "fpb_lift" + "fpb_lleq" + "fpb_fleq" * ]
+ [ { "parallel qrst-rtransition" * } {
+(* [ "fpbq ( ⦃?,?,?⦄ ≽[?,?] ⦃?,?,?⦄ )" "fpbq_alt ( ⦃?,?,?⦄ ≽≽[?,?] ⦃?,?,?⦄ )" + "fpbq_aaa" * ] *)
+ [ "fpb ( ⦃?,?,?⦄ ≻[?,?] ⦃?,?,?⦄ )" (* "fpb_lleq" + "fpb_fleq" *) * ]
}
]
+(*
[ { "context-sensitive rt-reduction" * } {
[ "lpx_lleq" * ]
- [ "cpx_lreq" + "cpx_llpx_sn" + "cpx_lleq" * ]
+ [ "cpx_lleq" * ]
}
]
*)
[ { "t-bound context-sensitive rt-transition" * } {
[ "lfpr ( ⦃?,?⦄ ⊢ ➡[?,?] ? )" "lfpr_length" + "lfpr_drops" + "lfpr_fqup" + "lfpr_frees" + "lfpr_aaa" + "lfpr_lfpx" + "lfpr_lfpr" * ]
- [ "cpr ( ⦃?,?⦄ ⊢ ? ➡[?] ? )" "cpr_drops" (* + "cpr_llpx_sn" + "cpr_cir" *) * ]
- [ "cpm ( ⦃?,?⦄ ⊢ ? ➡[?,?] ? )" "cpm_simple" + "cpm_drops" + "cpm_lsubr" + "cpm_cpx" * ]
+ [ "cpr ( ⦃?,?⦄ ⊢ ? ➡[?] ? )" "cpr_drops" * ]
+ [ "cpm ( ⦃?,?⦄ ⊢ ? ➡[?,?] ? )" "cpm_simple" + "cpm_drops" + "cpm_lsubr" + "cpm_lfxs" + "cpm_cpx" * ]
}
]
[ { "uncounted context-sensitive rt-transition" * } {
[ "lfpx ( ⦃?,?⦄ ⊢ ⬈[?,?] ? )" "lfpx_length" + "lfpx_drops" + "lfpx_fqup" + "lfpx_frees" + "lfpx_aaa" * ]
- [ "cpx ( ⦃?,?⦄ ⊢ ? ⬈[?] ? )" "cpx_simple" + "cpx_drops" + "cpx_fqus" + "cpx_lsubr" * ]
+ [ "cpx ( ⦃?,?⦄ ⊢ ? ⬈[?] ? )" "cpx_simple" + "cpx_drops" + "cpx_fqus" + "cpx_lsubr" + "cpx_lfxs" + "cpx_lfdeq" * ]
}
]
[ { "counted context-sensitive rt-transition" * } {
[ "lpx_sn" "lpx_sn_alt" + "lpx_sn_tc" + "lpx_sn_drop" + "lpx_sn_lpx_sn" * ]
}
]
+ [ "cpx_lreq" + "cpr_cir" + "fpb_lift" + "fpbq_lift" ]
[ "lleq ( ? ≡[?,?] ? )" "lleq_alt" + "lleq_alt_rec" + "lleq_lreq" + "lleq_drop" + "lleq_fqus" + "lleq_llor" + "lleq_lleq" * ]
*)
projects / helm.git / commitdiff