--- /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 h ] 𝐖𝐇 ⦃ break term 46 T ⦄ )"
+ non associative with precedence 45
+ for @{ 'PRedTyWHead $h $G $L $T }.
+++ /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 h, break term 46 o ] 𝐖𝐇 ⦃ break term 46 T ⦄ )"
- non associative with precedence 45
- for @{ 'PRedTyWHead $h $o $G $L $T }.
--- /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/cpr_tdeq.ma".
+include "basic_2/rt_transition/cwhx_drops.ma".
+include "basic_2/rt_transition/cwhx_rdeq.ma".
+include "basic_2/rt_computation/fsb_aaa.ma".
+include "basic_2/rt_computation/cpms_cpms.ma".
+include "basic_2/rt_computation/cpms_fpbg.ma".
+
+(* T-BOUND CONTEXT-SENSITIVE PARALLEL RT-COMPUTATION FOR TERMS **************)
+
+(* Properties with whd normality for unbound rt-transition ******************)
+
+lemma aaa_cpms_cwhx (h) (G) (L):
+ ∀T1,A. ⦃G,L⦄ ⊢ T1 ⁝ A →
+ ∃∃n,T2. ⦃G,L⦄ ⊢ T1 ➡*[n,h] T2 & ⦃G,L⦄ ⊢ ⬈[h] 𝐖𝐇⦃T2⦄.
+#h #G #L #T1 #A #H
+letin o ≝ (sd_O h)
+@(aaa_ind_fpbg … o … H) -G -L -T1 -A
+#G #L #T1 #A * -G -L -T1 -A
+[ #G #L #s #_ /2 width=4 by cwhx_sort, ex2_2_intro/
+| * #G #K #V1 #A #_ #IH -A
+ elim (IH … G K V1) [2,4: /3 width=1 by fpb_fpbg, fpb_fqu, fqu_lref_O/ ] -IH #n #V2 #HV12 #HV2
+ elim (lifts_total … V2 (𝐔❴1❵)) #T2 #HVT2
+ /5 width=10 by cpms_ell, cpms_delta, cwhx_lifts, drops_refl, drops_drop, ex2_2_intro/
+| #I #G #K #A #i #_ #IH -A
+ elim (IH … G K (#i)) [| /3 width=1 by fpb_fpbg, fpb_fqu/ ] -IH #n #V2 #HV12 #HV2
+ elim (lifts_total … V2 (𝐔❴1❵)) #T2 #HVT2
+ /5 width=10 by cpms_lref, cwhx_lifts, drops_refl, drops_drop, ex2_2_intro/
+| * #G #L #V #T1 #B #A #_ #_ #IH -B -A
+ [ elim (cpr_abbr_pos h o G L V T1) #T0 #HT10 #HnT10
+ elim (IH G L T0) -IH [| /4 width=2 by fpb_fpbg, cpm_fpb/ ] -HnT10 #n #T2 #HT02 #HT2
+ /3 width=5 by cpms_step_sn, ex2_2_intro/
+ | elim (IH … G (L.ⓓV) T1) -IH [| /3 width=1 by fpb_fpbg, fpb_fqu, fqu_bind_dx/ ] #n #T2 #HT12 #HT2
+ /3 width=5 by cwhx_ldef, cpms_bind_dx, ex2_2_intro/
+ ]
+| #p #G #L #W #T1 #B #A #_ #_ #_ -B -A
+ /2 width=5 by cwhx_abst, ex2_2_intro/
+| #G #L #V #T1 #B #A #_ #HT1 #IH
+ elim (IH … G L T1) [| /3 width=1 by fpb_fpbg, fpb_fqu, fqu_flat_dx/ ] #n1 #T2 #HT12 #HT2
+ elim (tdeq_dec h o T1 T2) [ -n1 #HT12 | -HT2 #HnT12 ]
+ [ lapply (tdeq_cwhx_trans … HT2 … HT12) -T2
+ @(insert_eq_0 … L) #Y @(insert_eq_0 … T1) #X * -Y -X
+ [ #L0 #s0 #H1 #H2 destruct -IH
+ lapply (aaa_inv_sort … HT1) -HT1 #H destruct
+ | #p #L0 #W0 #T0 #H1 #H2 destruct -HT1
+ elim (IH G L0 (ⓓ{p}ⓝW0.V.T0)) -IH [ /4 width=5 by cpms_step_sn, cpm_beta, ex2_2_intro/ ]
+ @fpb_fpbg @fpb_cpx [ /2 width=1 by cpx_beta/ ] #H
+ elim (tdeq_inv_pair … H) -H #H #_ #_ destruct
+ | #L0 #V0 #T0 #_ #H1 #H2 destruct -HT1
+ elim (lifts_total V (𝐔❴1❵)) #W #HVW
+ elim (IH G L0 (-ⓓV0.ⓐW.T0)) -IH [ /4 width=5 by cpms_step_sn, cpm_theta, ex2_2_intro/ ]
+ @fpb_fpbg @fpb_cpx [ /2 width=3 by cpx_theta/ ] #H
+ elim (tdeq_inv_pair … H) -H #H #_ #_ destruct
+ ]
+ | elim (IH G L (ⓐV.T2)) -IH [ /4 width=5 by cpms_trans, cpms_appl_dx, ex2_2_intro/ ]
+ @(cpms_tdneq_fwd_fpbg … n1) [ /2 width=3 by cpms_appl_dx/ ] #H
+ elim (tdeq_inv_pair … H) -H #_ #_ #H /2 width=1 by/
+ ]
+| #G #L #U #T1 #A #_ #_ #IH -A
+ elim (IH … G L T1) [| /3 width=1 by fpb_fpbg, fpb_fqu, fqu_flat_dx/ ] #n #T2 #HT12 #HT2
+ /3 width=4 by cpms_eps, ex2_2_intro/
+]
+qed-.
(**************************************************************************)
include "basic_2/rt_computation/fpbg_fqup.ma".
-include "basic_2/rt_computation/fpbg_fpbs.ma".
+include "basic_2/rt_computation/fpbg_cpxs.ma".
include "basic_2/rt_computation/cpms_fpbs.ma".
(* T-BOUND CONTEXT-SENSITIVE PARALLEL RT-COMPUTATION FOR TERMS **************)
(* Forward lemmas with proper parallel rst-computation for closures *********)
+lemma cpms_tdneq_fwd_fpbg (h) (o) (n): ∀G,L,T1,T2. ⦃G,L⦄ ⊢ T1 ➡*[n,h] T2 →
+ (T1 ≛[h,o] T2 → ⊥) → ⦃G,L,T1⦄ >[h,o] ⦃G,L,T2⦄.
+/3 width=2 by cpms_fwd_cpxs, cpxs_tdneq_fpbg/ qed-.
+
lemma fpbg_cpms_trans (h) (o) (n): ∀G1,G2,L1,L2,T1,T. ⦃G1, L1, T1⦄ >[h,o] ⦃G2, L2, T⦄ →
∀T2. ⦃G2, L2⦄ ⊢ T ➡*[n,h] T2 → ⦃G1, L1, T1⦄ >[h,o] ⦃G2, L2, T2⦄.
/3 width=5 by fpbg_fpbs_trans, cpms_fwd_fpbs/ 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 "static_2/relocation/lifts_tdeq.ma".
+include "basic_2/rt_transition/cpx_drops_basic.ma".
+include "basic_2/rt_transition/cnx.ma".
+
+(* NORMAL TERMS FOR UNBOUND CONTEXT-SENSITIVE PARALLEL RT-TRANSITION ********)
+
+(* Advanced inversion lemmas ************************************************)
+
+lemma cnx_inv_abbr_pos (h) (o) (G) (L): ∀V,T. ⦃G,L⦄ ⊢ ⬈[h,o] 𝐍⦃+ⓓV.T⦄ → ⊥.
+#h #o #G #L #V #U1 #H
+elim (cpx_subst h G (L.ⓓV) U1 … 0) [|*: /2 width=4 by drops_refl/ ] #U2 #T2 #HU12 #HTU2
+elim (tdeq_dec h o U1 U2) #HnU12 [ -HU12 | -HTU2 ]
+[ elim (tdeq_inv_lifts_dx … HnU12 … HTU2) -U2 #T1 #HTU1 #_ -T2
+ lapply (H T1 ?) -H [ /2 width=3 by cpx_zeta/ ] #H
+ /2 width=9 by tdeq_lifts_inv_pair_sn/
+| lapply (H (+ⓓV.U2) ?) -H [ /2 width=1 by cpx_bind/ ] -HU12 #H
+ elim (tdeq_inv_pair … H) -H #_ #_ /2 width=1 by/
+]
+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 "static_2/relocation/lifts_basic.ma".
+include "basic_2/rt_transition/cpm_drops.ma".
+include "basic_2/rt_transition/cpr.ma".
+
+(* CONTEXT-SENSITIVE PARALLEL R-TRANSITION FOR TERMS ************************)
+
+(* Properties with basic relocation *****************************************)
+
+lemma cpr_subst (h) (G) (L) (U1) (i):
+ ∀K,V. ⬇*[i] L ≘ K.ⓓV →
+ ∃∃U2,T2. ⦃G, L⦄ ⊢ U1 ➡[h] U2 & ⬆[i,1] T2 ≘ U2.
+#h #G #L #U1 @(fqup_wf_ind_eq (Ⓣ) … G L U1) -G -L -U1
+#G0 #L0 #U0 #IH #G #L * *
+[ #s #HG #HL #HT #i #K #V #_ destruct -IH
+ /2 width=4 by lifts_sort, ex2_2_intro/
+| #j #HG #HL #HT #i #K #V #HLK destruct -IH
+ elim (lt_or_eq_or_gt i j) #Hij
+ [ /3 width=4 by lifts_lref_ge_minus, cpr_refl, ex2_2_intro/
+ | elim (lifts_total V (𝐔❴↑i❵)) #U2 #HU2
+ elim (lifts_split_trans … HU2 (𝐔❴i❵) (𝐁❴i,1❵)) [2: @(after_basic_rc i 0) ]
+ /3 width=7 by cpm_delta_drops, ex2_2_intro/
+ | /3 width=4 by lifts_lref_lt, cpr_refl, ex2_2_intro/
+ ]
+| #l #HG #HL #HT #i #K #V #_ destruct -IH
+ /2 width=4 by lifts_gref, ex2_2_intro/
+| #p #J #W1 #U1 #HG #HL #HT #i #K #V #HLK destruct
+ elim (IH G L W1 … HLK) [| // ] #W2 #V2 #HW12 #HVW2
+ elim (IH G (L.ⓑ{J}W1) U1 … (↑i)) [|*: /3 width=4 by drops_drop/ ] #U2 #T2 #HU12 #HTU2
+ /3 width=9 by cpm_bind, lifts_bind, ex2_2_intro/
+| #J #W1 #U1 #HG #HL #HT #i #K #V #HLK destruct
+ elim (IH G L W1 … HLK) [| // ] #W2 #V2 #HW12 #HVW2
+ elim (IH G L U1 … HLK) [| // ] #U2 #T2 #HU12 #HTU2
+ /3 width=8 by cpr_flat, lifts_flat, ex2_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 "static_2/relocation/lifts_tdeq.ma".
+include "basic_2/rt_transition/cpr_drops_basic.ma".
+
+(* CONTEXT-SENSITIVE PARALLEL R-TRANSITION FOR TERMS ************************)
+
+(* Properties with context-free degree-based equivalence ********************)
+
+lemma cpr_abbr_pos (h) (o) (G) (L) (V) (T1):
+ ∃∃T2. ⦃G,L⦄ ⊢ +ⓓV.T1 ➡[h] T2 & (+ⓓV.T1 ≛[h, o] T2 → ⊥).
+#h #o #G #L #V #U1
+elim (cpr_subst h G (L.ⓓV) U1 … 0) [|*: /2 width=4 by drops_refl/ ] #U2 #T2 #HU12 #HTU2
+elim (tdeq_dec h o U1 U2) [ -HU12 #HU12 | -HTU2 #HnU12 ]
+[ elim (tdeq_inv_lifts_dx … HU12 … HTU2) -U2 #T1 #HTU1 #_ -T2
+ /3 width=9 by cpm_zeta, tdeq_lifts_inv_pair_sn, ex2_intro/
+| @(ex2_intro … (+ⓓV.U2)) [ /2 width=1 by cpm_bind/ ] -HU12 #H
+ elim (tdeq_inv_pair … H) -H #_ #_ /2 width=1 by/
+]
+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 "static_2/relocation/lifts_basic.ma".
+include "basic_2/rt_transition/cpx_drops.ma".
+
+(* UNBOUND CONTEXT-SENSITIVE PARALLEL RT-TRANSITION FOR TERMS ***************)
+
+(* Properties with basic relocation *****************************************)
+
+lemma cpx_subst (h) (G) (L) (U1) (i):
+ ∀I,K,V. ⬇*[i] L ≘ K.ⓑ{I}V →
+ ∃∃U2,T2. ⦃G, L⦄ ⊢ U1 ⬈[h] U2 & ⬆[i,1] T2 ≘ U2.
+#h #G #L #U1 @(fqup_wf_ind_eq (Ⓣ) … G L U1) -G -L -U1
+#G0 #L0 #U0 #IH #G #L * *
+[ #s #HG #HL #HT #i #I #K #V #_ destruct -IH
+ /2 width=4 by lifts_sort, ex2_2_intro/
+| #j #HG #HL #HT #i #I #K #V #HLK destruct -IH
+ elim (lt_or_eq_or_gt i j) #Hij
+ [ /3 width=4 by lifts_lref_ge_minus, cpx_refl, ex2_2_intro/
+ | elim (lifts_total V (𝐔❴↑i❵)) #U2 #HU2
+ elim (lifts_split_trans … HU2 (𝐔❴i❵) (𝐁❴i,1❵)) [2: @(after_basic_rc i 0) ]
+ /3 width=7 by cpx_delta_drops, ex2_2_intro/
+ | /3 width=4 by lifts_lref_lt, cpx_refl, ex2_2_intro/
+ ]
+| #l #HG #HL #HT #i #I #K #V #_ destruct -IH
+ /2 width=4 by lifts_gref, ex2_2_intro/
+| #p #J #W1 #U1 #HG #HL #HT #i #I #K #V #HLK destruct
+ elim (IH G L W1 … HLK) [| // ] #W2 #V2 #HW12 #HVW2
+ elim (IH G (L.ⓑ{J}W1) U1 … (↑i)) [|*: /3 width=4 by drops_drop/ ] #U2 #T2 #HU12 #HTU2
+ /3 width=9 by cpx_bind, lifts_bind, ex2_2_intro/
+| #J #W1 #U1 #HG #HL #HT #i #I #K #V #HLK destruct
+ elim (IH G L W1 … HLK) [| // ] #W2 #V2 #HW12 #HVW2
+ elim (IH G L U1 … HLK) [| // ] #U2 #T2 #HU12 #HTU2
+ /3 width=8 by cpx_flat, lifts_flat, ex2_2_intro/
+]
+qed-.
(* *)
(**************************************************************************)
-include "basic_2/notation/relations/predtywhead_5.ma".
-include "static_2/syntax/item_sd.ma".
+include "basic_2/notation/relations/predtywhead_4.ma".
+include "static_2/syntax/item_sh.ma".
include "static_2/syntax/lenv.ma".
include "static_2/syntax/genv.ma".
(* WHD NORMAL TERMS FOR UNBOUND CONTEXT-SENSITIVE PARALLEL RT-TRANSITION ****)
-inductive cwhx (h) (o:sd h) (G:genv): relation2 lenv term ≝
-| cwhx_sort: ∀L,s. cwhx h o G L (⋆s)
-| cwhx_abst: ∀p,L,W,T. cwhx h o G L (ⓛ{p}W.T)
-| cwhx_neg : ∀L,V,T. cwhx h o G (L.ⓓV) T → cwhx h o G L (-ⓓV.T)
+inductive cwhx (h:sh) (G:genv): relation2 lenv term ≝
+| cwhx_sort: ∀L,s. cwhx h G L (⋆s)
+| cwhx_abst: ∀p,L,W,T. cwhx h G L (ⓛ{p}W.T)
+| cwhx_ldef: ∀L,V,T. cwhx h G (L.ⓓV) T → cwhx h G L (-ⓓV.T)
.
interpretation
"whd normality for unbound context-sensitive parallel rt-transition (term)"
- 'PRedTyWHead h o G L T = (cwhx h o G L T).
+ 'PRedTyWHead h G L T = (cwhx h G L T).
(* Basic inversion lemmas ***************************************************)
-fact cwhx_inv_lref_aux (h) (o) (G):
- ∀Y,X. ⦃G,Y⦄ ⊢ ⬈[h,o] 𝐖𝐇⦃X⦄ →
+fact cwhx_inv_lref_aux (h) (G):
+ ∀Y,X. ⦃G,Y⦄ ⊢ ⬈[h] 𝐖𝐇⦃X⦄ →
∀i. X = #i → ⊥.
-#h #o #G #Y #X * - X -Y
+#h #G #Y #X * - X -Y
[ #L #s #i #H destruct
| #p #L #W #T #i #H destruct
| #L #V #T #_ #i #H destruct
]
qed-.
-lemma cwhx_inv_lref (h) (o) (G):
- ∀L,i. ⦃G,L⦄ ⊢ ⬈[h,o] 𝐖𝐇⦃#i⦄ → ⊥.
-/2 width=8 by cwhx_inv_lref_aux/ qed-.
+lemma cwhx_inv_lref (h) (G):
+ ∀L,i. ⦃G,L⦄ ⊢ ⬈[h] 𝐖𝐇⦃#i⦄ → ⊥.
+/2 width=7 by cwhx_inv_lref_aux/ qed-.
-fact cwhx_inv_gref_aux (h) (o) (G):
- ∀Y,X. ⦃G,Y⦄ ⊢ ⬈[h,o] 𝐖𝐇⦃X⦄ →
+fact cwhx_inv_gref_aux (h) (G):
+ ∀Y,X. ⦃G,Y⦄ ⊢ ⬈[h] 𝐖𝐇⦃X⦄ →
∀l. X = §l → ⊥.
-#h #o #G #Y #X * - X -Y
+#h #G #Y #X * - X -Y
[ #L #s #l #H destruct
| #p #L #W #T #l #H destruct
| #L #V #T #_ #l #H destruct
]
qed-.
-lemma cwhx_inv_gref (h) (o) (G):
- ∀L,l. ⦃G,L⦄ ⊢ ⬈[h,o] 𝐖𝐇⦃§l⦄ → ⊥.
-/2 width=8 by cwhx_inv_gref_aux/ qed-.
+lemma cwhx_inv_gref (h) (G):
+ ∀L,l. ⦃G,L⦄ ⊢ ⬈[h] 𝐖𝐇⦃§l⦄ → ⊥.
+/2 width=7 by cwhx_inv_gref_aux/ qed-.
-fact cwhx_inv_pos_aux (h) (o) (G):
- ∀Y,X. ⦃G,Y⦄ ⊢ ⬈[h,o] 𝐖𝐇⦃X⦄ →
- ∀W,U. X = +ⓓW.U → ⊥.
-#h #o #G #Y #X * - X -Y
+fact cwhx_inv_abbr_aux (h) (G):
+ ∀Y,X. ⦃G,Y⦄ ⊢ ⬈[h] 𝐖𝐇⦃X⦄ →
+ ∀V,T. X = +ⓓV.T → ⊥.
+#h #G #Y #X * - X -Y
[ #L #s #X1 #X2 #H destruct
| #p #L #W #T #X1 #X2 #H destruct
| #L #V #T #_ #X1 #X2 #H destruct
]
qed-.
-lemma cwhx_inv_pos (h) (o) (G):
- ∀Y,V,T. ⦃G,Y⦄ ⊢ ⬈[h,o] 𝐖𝐇⦃+ⓓV.T⦄ → ⊥.
-/2 width=9 by cwhx_inv_pos_aux/ qed-.
+lemma cwhx_inv_abbr (h) (G):
+ ∀Y,V,T. ⦃G,Y⦄ ⊢ ⬈[h] 𝐖𝐇⦃+ⓓV.T⦄ → ⊥.
+/2 width=8 by cwhx_inv_abbr_aux/ qed-.
+
+fact cwhx_inv_ldef_aux (h) (G):
+ ∀Y,X. ⦃G,Y⦄ ⊢ ⬈[h] 𝐖𝐇⦃X⦄ →
+ ∀V,T. X = -ⓓV.T → ⦃G,Y.ⓓV⦄ ⊢ ⬈[h] 𝐖𝐇⦃T⦄.
+#h #G #Y #X * - X -Y
+[ #L #s #X1 #X2 #H destruct
+| #p #L #W #T #X1 #X2 #H destruct
+| #L #V #T #HT #X1 #X2 #H destruct //
+]
+qed-.
+
+lemma cwhx_inv_ldef (h) (G):
+ ∀Y,V,T. ⦃G,Y⦄ ⊢ ⬈[h] 𝐖𝐇⦃-ⓓV.T⦄ → ⦃G,Y.ⓓV⦄ ⊢ ⬈[h] 𝐖𝐇⦃T⦄.
+/2 width=3 by cwhx_inv_ldef_aux/ qed-.
+
+fact cwhx_inv_appl_aux (h) (G):
+ ∀Y,X. ⦃G,Y⦄ ⊢ ⬈[h] 𝐖𝐇⦃X⦄ →
+ ∀V,T. X = ⓐV.T → ⊥.
+#h #G #Y #X * - X -Y
+[ #L #s #X1 #X2 #H destruct
+| #p #L #W #T #X1 #X2 #H destruct
+| #L #V #T #_ #X1 #X2 #H destruct
+]
+qed-.
+
+lemma cwhx_inv_appl (h) (G):
+ ∀Y,V,T. ⦃G,Y⦄ ⊢ ⬈[h] 𝐖𝐇⦃ⓐV.T⦄ → ⊥.
+/2 width=8 by cwhx_inv_appl_aux/ qed-.
+
+fact cwhx_inv_cast_aux (h) (G):
+ ∀Y,X. ⦃G,Y⦄ ⊢ ⬈[h] 𝐖𝐇⦃X⦄ →
+ ∀U,T. X = ⓝU.T → ⊥.
+#h #G #Y #X * - X -Y
+[ #L #s #X1 #X2 #H destruct
+| #p #L #W #T #X1 #X2 #H destruct
+| #L #V #T #_ #X1 #X2 #H destruct
+]
+qed-.
+
+lemma cwhx_inv_cast (h) (G):
+ ∀Y,U,T. ⦃G,Y⦄ ⊢ ⬈[h] 𝐖𝐇⦃ⓝU.T⦄ → ⊥.
+/2 width=8 by cwhx_inv_cast_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 "static_2/relocation/drops.ma".
+include "basic_2/rt_transition/cwhx.ma".
+
+(* WHD NORMAL TERMS FOR UNBOUND CONTEXT-SENSITIVE PARALLEL RT-TRANSITION ****)
+
+(* Properties with generic slicing ******************************************)
+
+lemma cwhx_lifts (h) (G): d_liftable1 … (cwhx h G).
+#h #G #K #T #H elim H -K -T
+[ #K #s #b #f #L #HLK #X #H
+ lapply (lifts_inv_sort1 … H) -H #H destruct //
+| #p #K #V #T #b #f #L #HLK #X #H
+ elim (lifts_inv_bind1 … H) -H #W #U #HVW #HTU #H destruct //
+| #K #V #T #_ #IH #b #f #L #HLK #X #H
+ elim (lifts_inv_bind1 … H) -H #W #U #HVW #HTU #H destruct
+ /5 width=4 by cwhx_ldef, drops_skip, ext2_pair/
+]
+qed-.
+
+(* Inversion lemmas with generic slicing ************************************)
+
+lemma cwhx_inv_lifts (h) (G): d_deliftable1 … (cwhx h G).
+#h #G #L #U #H elim H -L -U
+[ #L #s #b #f #K #HLK #X #H
+ lapply (lifts_inv_sort2 … H) -H #H destruct //
+| #p #L #W #U #b #f #K #HLK #X #H
+ elim (lifts_inv_bind2 … H) -H #V #T #HVW #HTU #H destruct //
+| #L #W #U #_ #IH #b #f #K #HLK #X #H
+ elim (lifts_inv_bind2 … H) -H #V #T #HVW #HTU #H destruct
+ /5 width=4 by cwhx_ldef, drops_skip, ext2_pair/
+]
+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 "static_2/static/rdeq_fqup.ma".
+include "basic_2/rt_transition/cwhx.ma".
+
+(* WHD NORMAL TERMS FOR UNBOUND CONTEXT-SENSITIVE PARALLEL RT-TRANSITION ****)
+
+(* Properties with degree-based equivalence *********************************)
+
+lemma rdeq_tdeq_cwhx_trans (h) (o) (G):
+ ∀L2,T2. ⦃G,L2⦄ ⊢ ⬈[h] 𝐖𝐇⦃T2⦄ →
+ ∀T1. T1 ≛[h,o] T2 →
+ ∀L1. L1 ≛[h,o,T1] L2 → ⦃G,L1⦄ ⊢ ⬈[h] 𝐖𝐇⦃T1⦄.
+#h #o #G #L2 #T2 #H elim H -L2 -T2
+[ #L2 #s2 #X1 #HX #L1 #HL
+ elim (tdeq_inv_sort2 … HX) -HX #s1 #d #_ #_ #H destruct -s2 -d //
+| #p #L2 #W2 #T2 #X1 #HX #L1 #HL
+ elim (tdeq_inv_pair2 … HX) -HX #W1 #T1 #_ #_ #H destruct -W2 -T2 //
+| #L2 #V2 #T2 #_ #IH #X1 #HX #L1 #HL
+ elim (tdeq_inv_pair2 … HX) -HX #V1 #T1 #HV12 #HT12 #H destruct
+ elim (rdeq_inv_bind … HL) -HL #HV1 #HT1
+ /5 width=2 by cwhx_ldef, rdeq_bind_repl_dx, ext2_pair/
+]
+qed-.
+
+lemma tdeq_cwhx_trans (h) (o) (G) (L):
+ ∀T2. ⦃G,L⦄ ⊢ ⬈[h] 𝐖𝐇⦃T2⦄ →
+ ∀T1. T1 ≛[h,o] T2 → ⦃G,L⦄ ⊢ ⬈[h] 𝐖𝐇⦃T1⦄.
+/3 width=6 by rdeq_tdeq_cwhx_trans/ qed-.
}
]
[ { "t-bound context-sensitive parallel rt-computation" * } {
- [ [ "for terms" ] "cpms" + "( ⦃?,?⦄ ⊢ ? ➡*[?,?] ? )" "cpms_drops" + "cpms_lsubr" + "cpms_rdeq" + "cpms_aaa" + "cpms_lpr" + "cpms_cpxs" + "cpms_fpbs" + "cpms_fpbg" + "cpms_cpms" * ]
+ [ [ "for terms" ] "cpms" + "( ⦃?,?⦄ ⊢ ? ➡*[?,?] ? )" "cpms_drops" + "cpms_lsubr" + "cpms_rdeq" + "cpms_aaa" + "cpms_cwhx" + "cpms_lpr" + "cpms_cpxs" + "cpms_fpbs" + "cpms_fpbg" + "cpms_cpms" * ]
}
]
[ { "unbound context-sensitive parallel rst-computation" * } {
[ { "context-sensitive parallel r-transition" * } {
[ [ "for lenvs on all entries" ] "lpr" + "( ⦃?,?⦄ ⊢ ➡[?] ? )" "lpr_length" + "lpr_drops" + "lpr_fquq" + "lpr_aaa" + "lpr_lpx" + "lpr_lpr" * ]
[ [ "for binders" ] "cpr_ext" + "( ⦃?,?⦄ ⊢ ? ➡[?] ? )" * ]
- [ [ "for terms" ] "cpr" + "( ⦃?,?⦄ ⊢ ? ➡[?] ? )" "cpr_drops" + "cpr_cpr" * ]
+ [ [ "for terms" ] "cpr" + "( ⦃?,?⦄ ⊢ ? ➡[?] ? )" "cpr_drops" + "cpr_drops_basic" + "cpr_tdeq" + "cpr_cpr" * ]
}
]
[ { "t-bound context-sensitive parallel rt-transition" * } {
}
]
[ { "unbound context-sensitive parallel rt-transition" * } {
- [ [ "normal form for terms" ] "cnx" + "( ⦃?,?⦄ ⊢ ⬈[?,?] 𝐍⦃?⦄ )" "cnx_simple" + "cnx_drops" + "cnx_cnx" * ]
+ [ [ "whd normal form for terms" ] "cwhx" + "( ⦃?,?⦄ ⊢ ⬈[?] 𝐖𝐇⦃?⦄ )" "cwhx_drops" + "cwhx_rdeq" * ]
+ [ [ "normal form for terms" ] "cnx" + "( ⦃?,?⦄ ⊢ ⬈[?,?] 𝐍⦃?⦄ )" "cnx_simple" + "cnx_drops" + "cnx_basic" + "cnx_cnx" * ]
[ [ "for lenvs on referred entries" ] "rpx" + "( ⦃?,?⦄ ⊢ ⬈[?,?] ? )" "rpx_length" + "rpx_drops" + "rpx_fqup" + "rpx_fsle" + "rpx_rdeq" + "rpx_lpx" + "rpx_rpx" * ]
[ [ "for lenvs on all entries" ] "lpx" + "( ⦃?,?⦄ ⊢ ⬈[?] ? )" "lpx_length" + "lpx_drops" + "lpx_fquq" + "lpx_fsle" + "lpx_rdeq" + "lpx_aaa" * ]
[ [ "for binders" ] "cpx_ext" + "( ⦃?,?⦄ ⊢ ? ⬈[?] ? )" * ]
- [ [ "for terms" ] "cpx" + "( ⦃?,?⦄ ⊢ ? ⬈[?] ? )" "cpx_simple" + "cpx_drops" + "cpx_fqus" + "cpx_lsubr" + "cpx_req" + "cpx_rdeq" + "cpx_fdeq" * ]
+ [ [ "for terms" ] "cpx" + "( ⦃?,?⦄ ⊢ ? ⬈[?] ? )" "cpx_simple" + "cpx_drops" + "cpx_drops_basic" + "cpx_fqus" + "cpx_lsubr" + "cpx_req" + "cpx_rdeq" + "cpx_fdeq" * ]
}
]
[ { "bound context-sensitive parallel rt-transition" * } {
lemma le_plus_to_minus_comm: ∀n,m,p. n ≤ p+m → n-p ≤ m.
/2 width=1 by le_plus_to_minus/ qed-.
+lemma le_inv_S1: ∀m,n. ↑m ≤ n → ∃∃p. m ≤ p & ↑p = n.
+#m *
+[ #H lapply (le_n_O_to_eq … H) -H
+ #H destruct
+| /3 width=3 by monotonic_pred, ex2_intro/
+]
+qed-.
+
(* Note: this might interfere with nat.ma *)
lemma monotonic_lt_pred: ∀m,n. m < n → 0 < m → pred m < pred n.
#m #n #Hmn #Hm whd >(S_pred … Hm)
--- /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_after.ma".
+include "ground_2/relocation/rtmap_basic.ma".
+
+(* RELOCATION MAP ***********************************************************)
+
+(* Properties with composition **********************************************)
+
+lemma after_basic_rc (m2,m1,n2,n1):
+ m1 ≤ m2 → m2 ≤ m1+n1 → 𝐁❴m2,n2❵ ⊚ 𝐁❴m1,n1❵ ≘ 𝐁❴m1,n2+n1❵.
+#m2 elim m2 -m2
+[ #m1 #n2 #n1 #Hm21 #_
+ <(le_n_O_to_eq … Hm21) -m1 //
+| #m2 #IH *
+ [ #n2 #n1 #_ < plus_O_n #H
+ elim (le_inv_S1 … H) -H #x #Hx #H destruct
+ <plus_n_Sm
+ @after_push [4:|*: // ]
+ @(IH 0 … Hx) -IH -n2 -x //
+ | #m1 #n2 #n1 #H1 #H2
+ lapply (le_S_S_to_le … H1) -H1 #H1
+ lapply (le_S_S_to_le … H2) -H2 #H2
+ /3 width=7 by after_refl/
+ ]
+]
+qed.
"rtmap_fcla ( 𝐂⦃?⦄ ≘ ? )" "rtmap_isfin ( 𝐅⦃?⦄ )" "rtmap_isuni ( 𝐔⦃?⦄ )" "rtmap_uni ( 𝐔❴?❵ )"
"rtmap_sle ( ? ⊆ ? )" "rtmap_sdj ( ? ∥ ? )" "rtmap_sand ( ? ⋒ ? ≘ ? )" "rtmap_sor ( ? ⋓ ? ≘ ? )"
"rtmap_at ( @⦃?,?⦄ ≘ ? )" "rtmap_istot ( 𝐓⦃?⦄ )" "rtmap_after ( ? ⊚ ? ≘ ? )" "rtmap_coafter ( ? ~⊚ ? ≘ ? )"
- "rtmap_basic ( 𝐁❴?,?❵ )"
+ "rtmap_basic ( 𝐁❴?,?❵ )" "rtmap_basic_after"
* ]
[ "nstream ( ⫯? ) ( ↑? )" "nstream_eq" "" ""
"" "" "nstream_isid" "nstream_id ( 𝐈𝐝 )" ""
"" "" "" ""
"" "" "" "nstream_sor"
"" "nstream_istot ( ?@❴?❵ )" "nstream_after ( ? ∘ ? )" "nstream_coafter ( ? ~∘ ? )"
- "nstream_basic"
+ "nstream_basic" ""
* ]
(*
[ "trace ( ∥?∥ )" "trace_at ( @⦃?,?⦄ ≘ ? )" "trace_after ( ? ⊚ ? ≘ ? )" "trace_isid ( 𝐈⦃?⦄ )" "trace_isun ( 𝐔⦃?⦄ )"
--- /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 m, break term 46 n ] break term 46 T1 ≘ break term 46 T2 )"
+ non associative with precedence 45
+ for @{ 'RLift $m $n $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 "ground_2/relocation/rtmap_basic_after.ma".
+include "static_2/notation/relations/rlift_4.ma".
+include "static_2/relocation/lifts.ma".
+
+(* GENERIC RELOCATION FOR TERMS *********************************************)
+
+interpretation "basic relocation (term)"
+ 'RLift m n T1 T2 = (lifts (basic m n) T1 T2).
+
+(* Properties with basic relocation *****************************************)
+
+lemma lifts_lref_lt (m,n,i): i < m → ⬆[m,n] #i ≘ #i.
+/3 width=1 by lifts_lref, at_basic_lt/ qed.
+
+lemma lifts_lref_ge (m,n,i): m ≤ i → ⬆[m,n] #i ≘ #(n+i).
+/3 width=1 by lifts_lref, at_basic_ge/ qed.
+
+lemma lifts_lref_ge_minus (m,n,i): n+m ≤ i → ⬆[m,n] #(i-n) ≘ #i.
+#m #n #i #Hi
+>(plus_minus_m_m i n) in ⊢ (???%);
+/3 width=2 by lifts_lref_ge, le_plus_to_minus_l, le_plus_b/
+qed.
∃∃V2,T2. V1 ≛[h, o] V2 & T1 ≛[h, o] T2 & Y = ②{I}V2.T2.
/2 width=3 by tdeq_inv_pair1_aux/ qed-.
+lemma tdeq_inv_sort2: ∀h,o,X1,s2. X1 ≛[h, o] ⋆s2 →
+ ∃∃s1,d. deg h o s1 d & deg h o s2 d & X1 = ⋆s1.
+#h #o #X1 #s2 #H
+elim (tdeq_inv_sort1 h o X1 s2)
+/2 width=5 by tdeq_sym, ex3_2_intro/
+qed-.
+
lemma tdeq_inv_pair2: ∀h,o,I,X1,V2,T2. X1 ≛[h, o] ②{I}V2.T2 →
∃∃V1,T1. V1 ≛[h, o] V2 & T1 ≛[h, o] T2 & X1 = ②{I}V1.T1.
#h #o #I #X1 #V2 #T2 #H
]
class "orange"
[ { "relocation" * } {
- [ { "generic slicing" * } {
+ [ { "generic and uniform slicing" * } {
[ [ "for lenvs" ] "drops" + "( ⬇*[?,?] ? ≘ ? )" + "( ⬇*[?] ? ≘ ? )" "drops_ctc" + "drops_ltc" + "drops_weight" + "drops_length" + "drops_cext2" + "drops_sex" + "drops_lex" + "drops_seq" + "drops_drops" + "drops_vector" * ]
}
]
- [ { "generic relocation" * } {
+ [ { "basic relocation" * } {
+ [ [ "for terms" ] "lifts_basic" + "( ⬆[?,?] ? ≘ ? )" * ]
+ }
+ ]
+ [ { "generic and uniform relocation" * } {
[ [ "for binders" ] "lifts_bind" + "( ⬆*[?] ? ≘ ? )" "lifts_weight_bind" + "lifts_lifts_bind" * ]
[ [ "for term vectors" ] "lifts_vector" + "( ⬆*[?] ? ≘ ? )" "lifts_lifts_vector" * ]
[ [ "for terms" ] "lifts" + "( ⬆*[?] ? ≘ ? )" "lifts_simple" + "lifts_weight" + "lifts_tdeq" + "lifts_lifts" * ]