--- /dev/null
+lemma cpr_delift: ∀G,K,V,T1,L,l. ⬇[l] L ≡ (K.ⓓV) →
+ ∃∃T2,T. ⦃G, L⦄ ⊢ T1 ➡ T2 & ⬆[l, 1] T ≡ T2.
+#G #K #V #T1 elim T1 -T1
+[ * /2 width=4 by cpr_atom, lift_sort, lift_gref, ex2_2_intro/
+ #i #L #l #HLK elim (lt_or_eq_or_gt i l)
+ #Hil [1,3: /4 width=4 by lift_lref_ge_minus, lift_lref_lt, ylt_inj, yle_inj, ex2_2_intro/ ]
+ destruct
+ elim (lift_total V 0 (i+1)) #W #HVW
+ elim (lift_split … HVW i i) /3 width=6 by cpr_delta, ex2_2_intro/
+| * [ #a ] #I #W1 #U1 #IHW1 #IHU1 #L #l #HLK
+ elim (IHW1 … HLK) -IHW1 #W2 #W #HW12 #HW2
+ [ elim (IHU1 (L. ⓑ{I}W1) (l+1)) -IHU1 /3 width=9 by drop_drop, cpr_bind, lift_bind, ex2_2_intro/
+ | elim (IHU1 … HLK) -IHU1 -HLK /3 width=8 by cpr_flat, lift_flat, ex2_2_intro/
+ ]
+]
+qed-.
+
+fact lstas_cpr_aux: ∀h,G,L,T1,T2,d. ⦃G, L⦄ ⊢ T1 •*[h, d] T2 →
+ d = 0 → ⦃G, L⦄ ⊢ T1 ➡ T2.
+#h #G #L #T1 #T2 #d #H elim H -G -L -T1 -T2 -d
+/3 width=1 by cpr_eps, cpr_flat, cpr_bind/
+[ #G #L #K #V1 #V2 #W2 #i #d #HLK #_ #HVW2 #IHV12 #H destruct
+ /3 width=6 by cpr_delta/
+| #G #L #K #V1 #V2 #W2 #i #d #_ #_ #_ #_ <plus_n_Sm #H destruct
+]
+qed-.
+
+lemma lstas_cpr: ∀h,G,L,T1,T2. ⦃G, L⦄ ⊢ T1 •*[h, 0] T2 → ⦃G, L⦄ ⊢ T1 ➡ T2.
+/2 width=4 by lstas_cpr_aux/ 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/cir.ma".
+include "basic_2/reduction/cpr.ma".
+
+(* CONTEXT-SENSITIVE PARALLEL REDUCTION FOR TERMS ***************************)
+
+(* Advanced forward lemmas on irreducibility ********************************)
+
+lemma cpr_fwd_cir: ∀G,L,T1,T2. ⦃G, L⦄ ⊢ T1 ➡ T2 → ⦃G, L⦄ ⊢ ➡ 𝐈⦃T1⦄ → T2 = T1.
+#G #L #T1 #T2 #H elim H -G -L -T1 -T2
+[ //
+| #G #L #K #V1 #V2 #W2 #i #HLK #_ #HVW2 #IHV12 #H
+ elim (cir_inv_delta … HLK) //
+| #a * #G #L #V1 #V2 #T1 #T2 #_ #_ #IHV1 #IHT1 #H
+ [ elim (cir_inv_bind … H) -H #HV1 #HT1 * #H destruct
+ lapply (IHV1 … HV1) -IHV1 -HV1 #H destruct
+ lapply (IHT1 … HT1) -IHT1 #H destruct //
+ | elim (cir_inv_ib2 … H) -H /3 width=2 by or_introl, eq_f2/
+ ]
+| * #G #L #V1 #V2 #T1 #T2 #_ #_ #IHV1 #IHT1 #H
+ [ elim (cir_inv_appl … H) -H #HV1 #HT1 #_
+ >IHV1 -IHV1 // -HV1 >IHT1 -IHT1 //
+ | elim (cir_inv_ri2 … H) /2 width=1 by/
+ ]
+| #G #L #V1 #T1 #T #T2 #_ #_ #_ #H
+ elim (cir_inv_ri2 … H) /2 width=1 by or_introl/
+| #G #L #V1 #T1 #T2 #_ #_ #H
+ elim (cir_inv_ri2 … H) /2 width=1 by/
+| #a #G #L #V1 #V2 #W1 #W2 #T1 #T2 #_ #_ #_ #_ #_ #_ #H
+ elim (cir_inv_appl … H) -H #_ #_ #H
+ elim (simple_inv_bind … H)
+| #a #G #L #V #V1 #V2 #W1 #W2 #T1 #T2 #_ #_ #_ #_ #_ #_ #_ #H
+ elim (cir_inv_appl … H) -H #_ #_ #H
+ elim (simple_inv_bind … H)
+]
+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/rt_transition/cpx.ma".
+include "basic_2/rt_transition/cpm.ma".
+
+(* T-BOUND CONTEXT-SENSITIVE PARALLEL RT-TRANSITION FOR TERMS ***************)
+
+(* Forward lemmas with uncounted context-sensitive rt-transition for terms **)
+
+(* Basic_2A1: includes: cpr_cpx *)
+lemma cpm_fwd_cpx: ∀n,h,G,L,T1,T2. ⦃G, L⦄ ⊢ T1 ➡[n, h] T2 → ⦃G, L⦄ ⊢ T1 ⬈[h] T2.
+#n #h #G #L #T1 #T2 * #c #Hc #H elim H -L -T1 -T2
+/2 width=3 by cpx_theta, cpx_beta, cpx_ee, cpx_eps, cpx_zeta, cpx_flat, cpx_bind, cpx_lref, cpx_delta/
+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/rt_transition/cpg_drops.ma".
+include "basic_2/rt_transition/cpm.ma".
+
+(* T-BOUND CONTEXT-SENSITIVE PARALLEL RT-TRANSITION FOR TERMS ***************)
+
+(* Advanced properties ******************************************************)
+
+(* Basic_1: includes: pr2_delta1 *)
+(* Basic_2A1: includes: cpr_delta *)
+lemma cpm_delta_drops: ∀n,h,G,L,K,V,V2,W2,i.
+ ⬇*[i] L ≡ K.ⓓV → ⦃G, K⦄ ⊢ V ➡[n, h] V2 →
+ ⬆*[⫯i] V2 ≡ W2 → ⦃G, L⦄ ⊢ #i ➡[n, h] W2.
+#n #h #G #L #K #V #V2 #W2 #i #HLK *
+/3 width=8 by cpg_delta_drops, ex2_intro/
+qed.
+
+lemma cpm_ell_drops: ∀n,h,G,L,K,V,V2,W2,i.
+ ⬇*[i] L ≡ K.ⓛV → ⦃G, K⦄ ⊢ V ➡[n, h] V2 →
+ ⬆*[⫯i] V2 ≡ W2 → ⦃G, L⦄ ⊢ #i ➡[⫯n, h] W2.
+#n #h #G #L #K #V #V2 #W2 #i #HLK *
+/3 width=8 by cpg_ell_drops, isrt_succ, ex2_intro/
+qed.
+
+(* Advanced inversion lemmas ************************************************)
+
+lemma cpm_inv_atom1_drops: ∀n,h,I,G,L,T2. ⦃G, L⦄ ⊢ ⓪{I} ➡[n, h] T2 →
+ ∨∨ T2 = ⓪{I} ∧ n = 0
+ | ∃∃s. T2 = ⋆(next h s) & I = Sort s & n = 1
+ | ∃∃K,V,V2,i. ⬇*[i] L ≡ K.ⓓV & ⦃G, K⦄ ⊢ V ➡[n, h] V2 &
+ ⬆*[⫯i] V2 ≡ T2 & I = LRef i
+ | ∃∃m,K,V,V2,i. ⬇*[i] L ≡ K.ⓛV & ⦃G, K⦄ ⊢ V ➡[m, h] V2 &
+ ⬆*[⫯i] V2 ≡ T2 & I = LRef i & n = ⫯m.
+#n #h #I #G #L #T2 * #c #Hc #H elim (cpg_inv_atom1_drops … H) -H *
+[ #H1 #H2 destruct lapply (isrt_inv_00 … Hc) -Hc
+ /3 width=1 by or4_intro0, conj/
+| #s #H1 #H2 #H3 destruct lapply (isrt_inv_01 … Hc) -Hc
+ /4 width=3 by or4_intro1, ex3_intro, sym_eq/ (**) (* sym_eq *)
+| #cV #i #K #V1 #V2 #HLK #HV12 #HVT2 #H1 #H2 destruct
+ /4 width=8 by ex4_4_intro, ex2_intro, or4_intro2/
+| #cV #i #K #V1 #V2 #HLK #HV12 #HVT2 #H1 #H2 destruct
+ elim (isrt_inv_plus_SO_dx … Hc) -Hc
+ /4 width=10 by ex5_5_intro, ex2_intro, or4_intro3/
+]
+qed-.
+
+lemma cpm_inv_lref1_drops: ∀n,h,G,L,T2,i. ⦃G, L⦄ ⊢ #i ➡[n, h] T2 →
+ ∨∨ T2 = #i ∧ n = 0
+ | ∃∃K,V,V2. ⬇*[i] L ≡ K. ⓓV & ⦃G, K⦄ ⊢ V ➡[n, h] V2 &
+ ⬆*[⫯i] V2 ≡ T2
+ | ∃∃m,K,V,V2. ⬇*[i] L ≡ K. ⓛV & ⦃G, K⦄ ⊢ V ➡[m, h] V2 &
+ ⬆*[⫯i] V2 ≡ T2 & n = ⫯m.
+#n #h #G #L #T2 #i * #c #Hc #H elim (cpg_inv_lref1_drops … H) -H *
+[ #H1 #H2 destruct lapply (isrt_inv_00 … Hc) -Hc
+ /3 width=1 by or3_intro0, conj/
+| #cV #K #V1 #V2 #HLK #HV12 #HVT2 #H destruct
+ /4 width=6 by ex3_3_intro, ex2_intro, or3_intro1/
+| #cV #K #V1 #V2 #HLK #HV12 #HVT2 #H destruct
+ elim (isrt_inv_plus_SO_dx … Hc) -Hc
+ /4 width=8 by ex4_4_intro, ex2_intro, or3_intro2/
+]
+qed-.
+
+(* Properties with generic slicing for local environments *******************)
+
+(* Basic_1: includes: pr0_lift pr2_lift *)
+(* Basic_2A1: includes: cpr_lift *)
+lemma cpm_lifts: ∀n,h,G. d_liftable2 (cpm n h G).
+#n #h #G #K #T1 #T2 * #c #Hc #HT12 #b #f #L #HLK #U1 #HTU1
+elim (cpg_lifts … HT12 … HLK … HTU1) -K -T1
+/3 width=5 by ex2_intro/
+qed-.
+
+(* Inversion lemmas with generic slicing for local environments *************)
+
+(* Basic_1: includes: pr0_gen_lift pr2_gen_lift *)
+(* Basic_2A1: includes: cpr_inv_lift1 *)
+lemma cpm_inv_lifts1: ∀n,h,G. d_deliftable2_sn (cpm n h G).
+#n #h #G #L #U1 #U2 * #c #Hc #HU12 #b #f #K #HLK #T1 #HTU1
+elim (cpg_inv_lifts1 … HU12 … HLK … HTU1) -L -U1
+/3 width=5 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/rt_transition/cpg_lsubr.ma".
+include "basic_2/rt_transition/cpm.ma".
+
+(* T-BOUND CONTEXT-SENSITIVE PARALLEL RT-TRANSITION FOR TERMS ***************)
+
+(* Properties with restricted refinement for local environments *************)
+
+(* Basic_2A1: includes: lsubr_cpr_trans *)
+lemma lsubr_cpm_trans: ∀n,h,G. lsub_trans … (cpm n h G) lsubr.
+#n #h #G #L1 #T1 #T2 * /3 width=5 by lsubr_cpg_trans, ex2_intro/
+qed-.
+
+(* Advanced properties ******************************************************)
+
+(* Basic_1: was by definition: pr2_free *)
+(* Basic_2A1: includes: tpr_cpr *)
+lemma tpm_cpm: ∀n,h,G,T1,T2. ⦃G, ⋆⦄ ⊢ T1 ➡[n, h] T2 → ∀L. ⦃G, L⦄ ⊢ T1 ➡[n, h] T2.
+#n #h #G #T1 #T2 #HT12 #L lapply (lsubr_cpm_trans … HT12 L ?) //
+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/rt_transition/cpg_simple.ma".
+include "basic_2/rt_transition/cpm.ma".
+
+(* T-BOUND CONTEXT-SENSITIVE PARALLEL RT-TRANSITION FOR TERMS ***************)
+
+(* Properties with simple terms *********************************************)
+
+(* Basic_2A1: includes: cpr_inv_appl1_simple *)
+lemma cpm_inv_appl1_simple: ∀n,h,G,L,V1,T1,U. ⦃G, L⦄ ⊢ ⓐV1.T1 ➡[n, h] U → 𝐒⦃T1⦄ →
+ ∃∃V2,T2. ⦃G, L⦄ ⊢ V1 ➡[h] V2 & ⦃G, L⦄ ⊢ T1 ➡[n, h] T2 &
+ U = ⓐV2.T2.
+#n #h #G #L #V1 #T1 #U * #c #Hc #H #HT1 elim (cpg_inv_appl1_simple … H HT1) -H -HT1
+#cV #cT #V2 #T2 #HV12 #HT12 #H1 #H2 destruct elim (isrt_inv_max … Hc) -Hc
+#nV #nT #HnV #HnT #H destruct elim (isrt_inv_shift … HnV) -HnV
+#HnV #H destruct /3 width=5 by ex3_2_intro, ex2_intro/
+qed-.
+++ /dev/null
-(* Basic_1: includes: pr2_delta1 *)
-| cpr_delta: ∀G,L,K,V,V2,W2,i.
- ⬇[i] L ≡ K. ⓓV → cpr G K V V2 →
- ⬆[0, i + 1] V2 ≡ W2 → cpr G L (#i) W2
-
-lemma cpr_cpx: ∀h,G,L,T1,T2. ⦃G, L⦄ ⊢ T1 ➡ T2 → ⦃G, L⦄ ⊢ T1 ➡[h] T2.
-#h #o #G #L #T1 #T2 #H elim H -L -T1 -T2
-/2 width=7 by cpx_delta, cpx_bind, cpx_flat, cpx_zeta, cpx_eps, cpx_beta, cpx_theta/
-qed.
-
-lemma lsubr_cpr_trans: ∀G. lsub_trans … (cpr G) lsubr.
-#G #L1 #T1 #T2 #H elim H -G -L1 -T1 -T2
-[ //
-| #G #L1 #K1 #V1 #V2 #W2 #i #HLK1 #_ #HVW2 #IHV12 #L2 #HL12
- elim (lsubr_fwd_drop2_abbr … HL12 … HLK1) -L1 *
- /3 width=6 by cpr_delta/
-|3,7: /4 width=1 by lsubr_pair, cpr_bind, cpr_beta/
-|4,6: /3 width=1 by cpr_flat, cpr_eps/
-|5,8: /4 width=3 by lsubr_pair, cpr_zeta, cpr_theta/
-]
-qed-.
-
-(* Basic_1: was by definition: pr2_free *)
-lemma tpr_cpr: ∀G,T1,T2. ⦃G, ⋆⦄ ⊢ T1 ➡ T2 → ∀L. ⦃G, L⦄ ⊢ T1 ➡ T2.
-#G #T1 #T2 #HT12 #L
-lapply (lsubr_cpr_trans … HT12 L ?) //
-qed.
-
-lemma cpr_delift: ∀G,K,V,T1,L,l. ⬇[l] L ≡ (K.ⓓV) →
- ∃∃T2,T. ⦃G, L⦄ ⊢ T1 ➡ T2 & ⬆[l, 1] T ≡ T2.
-#G #K #V #T1 elim T1 -T1
-[ * /2 width=4 by cpr_atom, lift_sort, lift_gref, ex2_2_intro/
- #i #L #l #HLK elim (lt_or_eq_or_gt i l)
- #Hil [1,3: /4 width=4 by lift_lref_ge_minus, lift_lref_lt, ylt_inj, yle_inj, ex2_2_intro/ ]
- destruct
- elim (lift_total V 0 (i+1)) #W #HVW
- elim (lift_split … HVW i i) /3 width=6 by cpr_delta, ex2_2_intro/
-| * [ #a ] #I #W1 #U1 #IHW1 #IHU1 #L #l #HLK
- elim (IHW1 … HLK) -IHW1 #W2 #W #HW12 #HW2
- [ elim (IHU1 (L. ⓑ{I}W1) (l+1)) -IHU1 /3 width=9 by drop_drop, cpr_bind, lift_bind, ex2_2_intro/
- | elim (IHU1 … HLK) -IHU1 -HLK /3 width=8 by cpr_flat, lift_flat, ex2_2_intro/
- ]
-]
-qed-.
-
-fact lstas_cpr_aux: ∀h,G,L,T1,T2,d. ⦃G, L⦄ ⊢ T1 •*[h, d] T2 →
- d = 0 → ⦃G, L⦄ ⊢ T1 ➡ T2.
-#h #G #L #T1 #T2 #d #H elim H -G -L -T1 -T2 -d
-/3 width=1 by cpr_eps, cpr_flat, cpr_bind/
-[ #G #L #K #V1 #V2 #W2 #i #d #HLK #_ #HVW2 #IHV12 #H destruct
- /3 width=6 by cpr_delta/
-| #G #L #K #V1 #V2 #W2 #i #d #_ #_ #_ #_ <plus_n_Sm #H destruct
-]
-qed-.
-
-lemma lstas_cpr: ∀h,G,L,T1,T2. ⦃G, L⦄ ⊢ T1 •*[h, 0] T2 → ⦃G, L⦄ ⊢ T1 ➡ T2.
-/2 width=4 by lstas_cpr_aux/ qed.
-
-lemma cpr_inv_atom1: ∀I,G,L,T2. ⦃G, L⦄ ⊢ ⓪{I} ➡ T2 →
- T2 = ⓪{I} ∨
- ∃∃K,V,V2,i. ⬇[i] L ≡ K. ⓓV & ⦃G, K⦄ ⊢ V ➡ V2 &
- ⬆[O, i + 1] V2 ≡ T2 & I = LRef i.
-/2 width=3 by cpr_inv_atom1_aux/ qed-.
-
-(* Basic_1: includes: pr0_gen_lref pr2_gen_lref *)
-lemma cpr_inv_lref1: ∀G,L,T2,i. ⦃G, L⦄ ⊢ #i ➡ T2 →
- T2 = #i ∨
- ∃∃K,V,V2. ⬇[i] L ≡ K. ⓓV & ⦃G, K⦄ ⊢ V ➡ V2 &
- ⬆[O, i + 1] V2 ≡ T2.
-#G #L #T2 #i #H
-elim (cpr_inv_atom1 … H) -H /2 width=1 by or_introl/
-* #K #V #V2 #j #HLK #HV2 #HVT2 #H destruct /3 width=6 by ex3_3_intro, or_intror/
-qed-.
-
-(* Note: the main property of simple terms *)
-lemma cpr_inv_appl1_simple: ∀G,L,V1,T1,U. ⦃G, L⦄ ⊢ ⓐV1. T1 ➡ U → 𝐒⦃T1⦄ →
- ∃∃V2,T2. ⦃G, L⦄ ⊢ V1 ➡ V2 & ⦃G, L⦄ ⊢ T1 ➡ T2 &
- U = ⓐV2. T2.
-#G #L #V1 #T1 #U #H #HT1
-elim (cpr_inv_appl1 … H) -H *
-[ /2 width=5 by ex3_2_intro/
-| #a #V2 #W1 #W2 #U1 #U2 #_ #_ #_ #H #_ destruct
- elim (simple_inv_bind … HT1)
-| #a #V #V2 #W1 #W2 #U1 #U2 #_ #_ #_ #_ #H #_ destruct
- elim (simple_inv_bind … HT1)
-]
-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/cir.ma".
-include "basic_2/reduction/cpr.ma".
-
-(* CONTEXT-SENSITIVE PARALLEL REDUCTION FOR TERMS ***************************)
-
-(* Advanced forward lemmas on irreducibility ********************************)
-
-lemma cpr_fwd_cir: ∀G,L,T1,T2. ⦃G, L⦄ ⊢ T1 ➡ T2 → ⦃G, L⦄ ⊢ ➡ 𝐈⦃T1⦄ → T2 = T1.
-#G #L #T1 #T2 #H elim H -G -L -T1 -T2
-[ //
-| #G #L #K #V1 #V2 #W2 #i #HLK #_ #HVW2 #IHV12 #H
- elim (cir_inv_delta … HLK) //
-| #a * #G #L #V1 #V2 #T1 #T2 #_ #_ #IHV1 #IHT1 #H
- [ elim (cir_inv_bind … H) -H #HV1 #HT1 * #H destruct
- lapply (IHV1 … HV1) -IHV1 -HV1 #H destruct
- lapply (IHT1 … HT1) -IHT1 #H destruct //
- | elim (cir_inv_ib2 … H) -H /3 width=2 by or_introl, eq_f2/
- ]
-| * #G #L #V1 #V2 #T1 #T2 #_ #_ #IHV1 #IHT1 #H
- [ elim (cir_inv_appl … H) -H #HV1 #HT1 #_
- >IHV1 -IHV1 // -HV1 >IHT1 -IHT1 //
- | elim (cir_inv_ri2 … H) /2 width=1 by/
- ]
-| #G #L #V1 #T1 #T #T2 #_ #_ #_ #H
- elim (cir_inv_ri2 … H) /2 width=1 by or_introl/
-| #G #L #V1 #T1 #T2 #_ #_ #H
- elim (cir_inv_ri2 … H) /2 width=1 by/
-| #a #G #L #V1 #V2 #W1 #W2 #T1 #T2 #_ #_ #_ #_ #_ #_ #H
- elim (cir_inv_appl … H) -H #_ #_ #H
- elim (simple_inv_bind … H)
-| #a #G #L #V #V1 #V2 #W1 #W2 #T1 #T2 #_ #_ #_ #_ #_ #_ #_ #H
- elim (cir_inv_appl … H) -H #_ #_ #H
- elim (simple_inv_bind … H)
-]
-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/rt_transition/cpm_drops.ma".
+
+(* CONTEXT-SENSITIVE PARALLEL R-TRANSITION FOR TERMS ************************)
+
+(* Advanced inversion lemmas ************************************************)
+
+(* Basic_2A1: includes: cpr_inv_atom1 *)
+lemma cpr_inv_atom1_drops: ∀h,I,G,L,T2. ⦃G, L⦄ ⊢ ⓪{I} ➡[h] T2 →
+ T2 = ⓪{I} ∨
+ ∃∃K,V,V2,i. ⬇*[i] L ≡ K.ⓓV & ⦃G, K⦄ ⊢ V ➡[h] V2 &
+ ⬆*[⫯i] V2 ≡ T2 & I = LRef i.
+#h #I #G #L #T2 #H elim (cpm_inv_atom1_drops … H) -H *
+[ /2 width=1 by or_introl/
+| #s #_ #_ #H destruct
+| /3 width=8 by ex4_4_intro, or_intror/
+| #m #K #V1 #V2 #i #_ #_ #_ #_ #H destruct
+]
+qed-.
+
+(* Basic_1: includes: pr0_gen_lref pr2_gen_lref *)
+(* Basic_2A1: includes: cpr_inv_lref1 *)
+lemma cpr_inv_lref1_drops: ∀h,G,L,T2,i. ⦃G, L⦄ ⊢ #i ➡[h] T2 →
+ T2 = #i ∨
+ ∃∃K,V,V2. ⬇*[i] L ≡ K. ⓓV & ⦃G, K⦄ ⊢ V ➡[h] V2 &
+ ⬆*[⫯i] V2 ≡ T2.
+#h #G #L #T2 #i #H elim (cpm_inv_lref1_drops … H) -H *
+[ /2 width=1 by or_introl/
+| /3 width=6 by ex3_3_intro, or_intror/
+| #m #K #V1 #V2 #_ #_ #_ #H destruct
+]
+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/ynat/ynat_max.ma".
-include "basic_2/substitution/drop_drop.ma".
-include "basic_2/reduction/cpr.ma".
-
-(* CONTEXT-SENSITIVE PARALLEL REDUCTION FOR TERMS ***************************)
-
-(* Relocation properties ****************************************************)
-
-(* Basic_1: includes: pr0_lift pr2_lift *)
-lemma cpr_lift: ∀G. d_liftable (cpr G).
-#G #K #T1 #T2 #H elim H -G -K -T1 -T2
-[ #I #G #K #L #b #l #k #_ #U1 #H1 #U2 #H2
- >(lift_mono … H1 … H2) -H1 -H2 //
-| #G #K #KV #V #V2 #W2 #i #HKV #HV2 #HVW2 #IHV2 #L #b #l #k #HLK #U1 #H #U2 #HWU2
- elim (lift_inv_lref1 … H) * #Hil #H destruct
- [ elim (lift_trans_ge … HVW2 … HWU2) -W2 /2 width=1 by ylt_fwd_le_succ1/ #W2 #HVW2 #HWU2
- elim (drop_trans_le … HLK … HKV) -K /2 width=2 by ylt_fwd_le/ #X #HLK #H
- elim (drop_inv_skip2 … H) -H /2 width=1 by ylt_to_minus/ -Hil
- #K #Y #HKV #HVY #H destruct /3 width=9 by cpr_delta/
- | lapply (lift_trans_be … HVW2 … HWU2 ? ?) -W2 /2 width=1 by yle_succ_dx/ >plus_plus_comm_23 #HVU2
- lapply (drop_trans_ge_comm … HLK … HKV ?) -K // -Hil /3 width=6 by cpr_delta, drop_inv_gen/
- ]
-| #a #I #G #K #V1 #V2 #T1 #T2 #_ #_ #IHV12 #IHT12 #L #b #l #k #HLK #U1 #H1 #U2 #H2
- elim (lift_inv_bind1 … H1) -H1 #VV1 #TT1 #HVV1 #HTT1 #H1 destruct
- elim (lift_inv_bind1 … H2) -H2 #VV2 #TT2 #HVV2 #HTT2 #H2 destruct /4 width=6 by cpr_bind, drop_skip/
-| #I #G #K #V1 #V2 #T1 #T2 #_ #_ #IHV12 #IHT12 #L #b #l #k #HLK #U1 #H1 #U2 #H2
- elim (lift_inv_flat1 … H1) -H1 #VV1 #TT1 #HVV1 #HTT1 #H1 destruct
- elim (lift_inv_flat1 … H2) -H2 #VV2 #TT2 #HVV2 #HTT2 #H2 destruct /3 width=6 by cpr_flat/
-| #G #K #V #T1 #T #T2 #_ #HT2 #IHT1 #L #b #l #k #HLK #U1 #H #U2 #HTU2
- elim (lift_inv_bind1 … H) -H #VV1 #TT1 #HVV1 #HTT1 #H destruct
- elim (lift_conf_O1 … HTU2 … HT2) -T2 /4 width=6 by cpr_zeta, drop_skip/
-| #G #K #V #T1 #T2 #_ #IHT12 #L #b #l #k #HLK #U1 #H #U2 #HTU2
- elim (lift_inv_flat1 … H) -H #VV1 #TT1 #HVV1 #HTT1 #H destruct /3 width=6 by cpr_eps/
-| #a #G #K #V1 #V2 #W1 #W2 #T1 #T2 #_ #_ #_ #IHV12 #IHW12 #IHT12 #L #b #l #k #HLK #X1 #HX1 #X2 #HX2
- elim (lift_inv_flat1 … HX1) -HX1 #V0 #X #HV10 #HX #HX1 destruct
- elim (lift_inv_bind1 … HX) -HX #W0 #T0 #HW0 #HT10 #HX destruct
- elim (lift_inv_bind1 … HX2) -HX2 #X #T3 #HX #HT23 #HX2 destruct
- elim (lift_inv_flat1 … HX) -HX #W3 #V3 #HW23 #HV23 #HX destruct /4 width=6 by cpr_beta, drop_skip/
-| #a #G #K #V1 #V #V2 #W1 #W2 #T1 #T2 #_ #HV2 #_ #_ #IHV1 #IHW12 #IHT12 #L #b #l #k #HLK #X1 #HX1 #X2 #HX2
- elim (lift_inv_flat1 … HX1) -HX1 #V0 #X #HV10 #HX #HX1 destruct
- elim (lift_inv_bind1 … HX) -HX #W0 #T0 #HW0 #HT10 #HX destruct
- elim (lift_inv_bind1 … HX2) -HX2 #W3 #X #HW23 #HX #HX2 destruct
- elim (lift_inv_flat1 … HX) -HX #V3 #T3 #HV3 #HT23 #HX destruct
- elim (lift_trans_ge … HV2 … HV3) -V2 /4 width=6 by cpr_theta, drop_skip/
-]
-qed.
-
-(* Basic_1: includes: pr0_gen_lift pr2_gen_lift *)
-lemma cpr_inv_lift1: ∀G. d_deliftable_sn (cpr G).
-#G #L #U1 #U2 #H elim H -G -L -U1 -U2
-[ * #i #G #L #K #b #l #k #_ #T1 #H
- [ lapply (lift_inv_sort2 … H) -H #H destruct /2 width=3 by ex2_intro/
- | elim (lift_inv_lref2 … H) -H * #Hil #H destruct /3 width=3 by lift_lref_ge_minus, lift_lref_lt, ex2_intro/
- | lapply (lift_inv_gref2 … H) -H #H destruct /2 width=3 by ex2_intro/
- ]
-| #G #L #LV #V #V2 #W2 #i #HLV #HV2 #HVW2 #IHV2 #K #b #l #k #HLK #T1 #H
- elim (lift_inv_lref2 … H) -H * #Hil #H destruct
- [ elim (drop_conf_lt … HLK … HLV) -L // #L #U #HKL #HLV #HUV
- elim (IHV2 … HLV … HUV) -V #U2 #HUV2 #HU2
- elim (lift_trans_le … HUV2 … HVW2) -V2 // <yminus_succ2 <yplus_inj >yplus_SO2 >ymax_pre_sn /3 width=8 by cpr_delta, ylt_fwd_le_succ1, ex2_intro/
- | elim (yle_inv_plus_inj2 … Hil) #Hlim #Hmi
- lapply (yle_inv_inj … Hmi) -Hmi #Hmi
- lapply (drop_conf_ge … HLK … HLV ?) -L // #HKLV
- elim (lift_split … HVW2 l (i - k + 1)) -HVW2 [2,3,4: /2 width=1 by yle_succ_dx, le_S_S/ ] -Hil -Hlim
- #V1 #HV1 >plus_minus // <minus_minus /2 width=1 by le_S/ <minus_n_n <plus_n_O
- /3 width=8 by cpr_delta, ex2_intro/
- ]
-| #a #I #G #L #V1 #V2 #U1 #U2 #_ #_ #IHV12 #IHU12 #K #b #l #k #HLK #X #H
- elim (lift_inv_bind2 … H) -H #W1 #T1 #HWV1 #HTU1 #H destruct
- elim (IHV12 … HLK … HWV1) -IHV12 #W2 #HW12 #HWV2
- elim (IHU12 … HTU1) -IHU12 -HTU1 /3 width=6 by cpr_bind, drop_skip, lift_bind, ex2_intro/
-| #I #G #L #V1 #V2 #U1 #U2 #_ #_ #IHV12 #IHU12 #K #b #l #k #HLK #X #H
- elim (lift_inv_flat2 … H) -H #W1 #T1 #HWV1 #HTU1 #H destruct
- elim (IHV12 … HLK … HWV1) -V1
- elim (IHU12 … HLK … HTU1) -U1 -HLK /3 width=6 by cpr_flat, lift_flat, ex2_intro/
-| #G #L #V #U1 #U #U2 #_ #HU2 #IHU1 #K #b #l #k #HLK #X #H
- elim (lift_inv_bind2 … H) -H #W1 #T1 #HWV1 #HTU1 #H destruct
- elim (IHU1 (K.ⓓW1) b … HTU1) /2 width=1 by drop_skip/ -L -U1 #T #HTU #HT1
- elim (lift_div_le … HU2 … HTU) -U /3 width=6 by cpr_zeta, ex2_intro/
-| #G #L #V #U1 #U2 #_ #IHU12 #K #b #l #k #HLK #X #H
- elim (lift_inv_flat2 … H) -H #W1 #T1 #HWV1 #HTU1 #H destruct
- elim (IHU12 … HLK … HTU1) -L -U1 /3 width=3 by cpr_eps, ex2_intro/
-| #a #G #L #V1 #V2 #W1 #W2 #T1 #T2 #_ #_ #_ #IHV12 #IHW12 #IHT12 #K #b #l #k #HLK #X #HX
- elim (lift_inv_flat2 … HX) -HX #V0 #Y #HV01 #HY #HX destruct
- elim (lift_inv_bind2 … HY) -HY #W0 #T0 #HW01 #HT01 #HY destruct
- elim (IHV12 … HLK … HV01) -V1
- elim (IHT12 (K.ⓛW0) b … HT01) -T1 /2 width=1 by drop_skip/
- elim (IHW12 … HLK … HW01) -W1 /4 width=7 by cpr_beta, lift_flat, lift_bind, ex2_intro/
-| #a #G #L #V1 #V #V2 #W1 #W2 #T1 #T2 #_ #HV2 #_ #_ #IHV1 #IHW12 #IHT12 #K #b #l #k #HLK #X #HX
- elim (lift_inv_flat2 … HX) -HX #V0 #Y #HV01 #HY #HX destruct
- elim (lift_inv_bind2 … HY) -HY #W0 #T0 #HW01 #HT01 #HY destruct
- elim (IHV1 … HLK … HV01) -V1 #V3 #HV3 #HV03
- elim (IHT12 (K.ⓓW0) b … HT01) -T1 /2 width=1 by drop_skip/ #T3 #HT32 #HT03
- elim (IHW12 … HLK … HW01) -W1
- elim (lift_trans_le … HV3 … HV2) -V
- /4 width=9 by cpr_theta, lift_flat, lift_bind, ex2_intro/
-]
-qed-.
(* Inversion lemmas with generic slicing for local environments *************)
(* Basic_2A1: includes: cpx_inv_lift1 *)
-lemma cpx_inv_lift1: ∀h,G. d_deliftable2_sn (cpx h G).
+lemma cpx_inv_lifts: ∀h,G. d_deliftable2_sn (cpx h G).
#h #G #L #U1 #U2 * #cU #HU12 #b #f #K #HLK #T1 #HTU1
elim (cpg_inv_lifts1 … HU12 … HLK … HTU1) -L -U1
/3 width=4 by ex2_intro, ex_intro/
(* UNCOUNTED CONTEXT-SENSITIVE PARALLEL RT-TRANSITION FOR TERMS *************)
+(* Properties with restricted refinement for local environments *************)
+
lemma lsubr_cpx_trans: ∀h,G. lsub_trans … (cpx h G) lsubr.
#h #G #L1 #T1 #T2 * /3 width=4 by lsubr_cpg_trans, ex_intro/
qed-.
cpg.ma cpg_simple.ma cpg_drops.ma cpg_lsubr.ma
cpx.ma cpx_simple.ma cpx_drops.ma cpx_lsubr.ma
lfpx.ma lfpx_length.ma lfpx_drops.ma lfpx_fqup.ma
-cpm.ma
-cpr.ma
+cpm.ma cpm_simple.ma cpm_drops.ma cpm_lsubr.ma cpm_cpx.ma
+cpr.ma cpr_drops.ma
[ "cpx_lreq" + "cpx_fqus" + "cpx_llpx_sn" + "cpx_lleq" * ]
}
]
- [ { "context-sensitive reduction" * } {
- [ "lpr ( ⦃?,?⦄ ⊢ ➡ ? )" "lpr_drop" + "lpr_lpr" * ]
- [ "cpr ( ⦃?,?⦄ ⊢ ? ➡ ? )" "cpr_lift" + "cpr_llpx_sn" + "cpr_cir" * ]
+*)
+ [ { "t-bound context-sensitive rt-transition" * } {
+(* [ "lpr ( ⦃?,?⦄ ⊢ ➡ ? )" "lpr_drop" + "lpr_lpr" * ] *)
+ [ "cpr ( ⦃?,?⦄ ⊢ ? ➡[?] ? )" "cpr_drops" (* + "cpr_llpx_sn" + "cpr_cir" *) * ]
+ [ "cpm ( ⦃?,?⦄ ⊢ ? ➡[?,?] ? )" "cpm_simple" + "cpm_drops" + "cpm_lsubr" + "cpm_cpx" * ]
}
]
-*)
[ { "uncounted context-sensitive rt-transition" * } {
[ "lfpx ( ⦃?,?⦄ ⊢ ⬈[?,?] ? )" "lfpx_length" + "lfpx_drops" + "lfpx_fqup" * ]
[ "cpx ( ⦃?,?⦄ ⊢ ? ⬈[?] ? )" "cpx_simple" + "cpx_drops" + "cpx_lsubr" * ]
projects / helm.git / commitdiff