lemma vnv_restricted (h) (p): ∀G,L,s. ⦃G,L.ⓛ⋆s.ⓛⓛ{p}⋆s.⋆s.ⓛⓛ{p}⋆s.ⓐ#0.#1⦄ ⊢ ⓐ#2.#0 ![h].
#h #p #G #L #s
@(cnv_appl … 1 p … (⋆s) … (ⓐ#0.#2))
-[ /2 width=1 by ylt_inj/
+[ //
| /4 width=1 by cnv_sort, cnv_zero, cnv_lref/
| @cnv_zero
@cnv_bind //
@(cnv_appl … 1 p … (⋆s) … (⋆s))
- [ /2 width=1 by ylt_inj/
+ [ //
| /2 width=1 by cnv_sort, cnv_zero/
| /4 width=1 by cnv_sort, cnv_zero, cnv_lref, cnv_bind/
| /2 width=3 by cpms_ell, lifts_sort/
(* *)
(**************************************************************************)
-include "ground_2/ynat/ynat_lt.ma".
+include "static_2/syntax/ac.ma".
include "basic_2/notation/relations/exclaim_5.ma".
include "basic_2/notation/relations/exclaim_4.ma".
include "basic_2/notation/relations/exclaimstar_4.ma".
(* activate genv *)
(* Basic_2A1: uses: snv *)
-inductive cnv (a:ynat) (h): relation3 genv lenv term ≝
+inductive cnv (a) (h): relation3 genv lenv term ≝
| cnv_sort: ∀G,L,s. cnv a h G L (⋆s)
| cnv_zero: ∀I,G,K,V. cnv a h G K V → cnv a h G (K.ⓑ{I}V) (#0)
| cnv_lref: ∀I,G,K,i. cnv a h G K (#i) → cnv a h G (K.ⓘ{I}) (#↑i)
| cnv_bind: ∀p,I,G,L,V,T. cnv a h G L V → cnv a h G (L.ⓑ{I}V) T → cnv a h G L (ⓑ{p,I}V.T)
-| cnv_appl: ∀n,p,G,L,V,W0,T,U0. yinj n < a → cnv a h G L V → cnv a h G L T →
+| cnv_appl: ∀n,p,G,L,V,W0,T,U0. appl a n → cnv a h G L V → cnv a h G L T →
⦃G,L⦄ ⊢ V ➡*[1,h] W0 → ⦃G,L⦄ ⊢ T ➡*[n,h] ⓛ{p}W0.U0 → cnv a h G L (ⓐV.T)
| cnv_cast: ∀G,L,U,T,U0. cnv a h G L U → cnv a h G L T →
⦃G,L⦄ ⊢ U ➡*[h] U0 → ⦃G,L⦄ ⊢ T ➡*[1,h] U0 → cnv a h G L (ⓝU.T)
'Exclaim a h G L T = (cnv a h G L T).
interpretation "context-sensitive restricted native validity (term)"
- 'Exclaim h G L T = (cnv (yinj (S (S O))) h G L T).
+ 'Exclaim h G L T = (cnv (ac_eq (S O)) h G L T).
interpretation "context-sensitive extended native validity (term)"
- 'ExclaimStar h G L T = (cnv Y h G L T).
+ 'ExclaimStar h G L T = (cnv ac_top h G L T).
(* Basic inversion lemmas ***************************************************)
fact cnv_inv_appl_aux (a) (h):
∀G,L,X. ⦃G,L⦄ ⊢ X ![a,h] → ∀V,T. X = ⓐV.T →
- ∃∃n,p,W0,U0. yinj n < a & ⦃G,L⦄ ⊢ V ![a,h] & ⦃G,L⦄ ⊢ T ![a,h] &
+ ∃∃n,p,W0,U0. appl a n & ⦃G,L⦄ ⊢ V ![a,h] & ⦃G,L⦄ ⊢ T ![a,h] &
⦃G,L⦄ ⊢ V ➡*[1,h] W0 & ⦃G,L⦄ ⊢ T ➡*[n,h] ⓛ{p}W0.U0.
#a #h #G #L #X * -L -X
[ #G #L #s #X1 #X2 #H destruct
(* Basic_2A1: uses: snv_inv_appl *)
lemma cnv_inv_appl (a) (h):
∀G,L,V,T. ⦃G,L⦄ ⊢ ⓐV.T ![a,h] →
- ∃∃n,p,W0,U0. yinj n < a & ⦃G,L⦄ ⊢ V ![a,h] & ⦃G,L⦄ ⊢ T ![a,h] &
+ ∃∃n,p,W0,U0. appl a n & ⦃G,L⦄ ⊢ V ![a,h] & ⦃G,L⦄ ⊢ T ![a,h] &
⦃G,L⦄ ⊢ V ➡*[1,h] W0 & ⦃G,L⦄ ⊢ T ➡*[n,h] ⓛ{p}W0.U0.
/2 width=3 by cnv_inv_appl_aux/ qed-.
(* *)
(**************************************************************************)
-include "ground_2/lib/arith_2b.ma".
include "basic_2/rt_computation/cpms_aaa.ma".
-include "basic_2/rt_computation/lprs_cpms.ma".
include "basic_2/dynamic/cnv.ma".
(* CONTEXT-SENSITIVE NATIVE VALIDITY FOR TERMS ******************************)
/2 width=2 by cpms_total_aaa/
qed-.
-(* Advanced inversion lemmas ************************************************)
-
-lemma cnv_inv_appl_pred (a) (h) (G) (L):
- ∀V,T. ⦃G,L⦄ ⊢ ⓐV.T ![yinj a,h] →
- ∃∃p,W0,U0. ⦃G,L⦄ ⊢ V ![a,h] & ⦃G,L⦄ ⊢ T ![a,h] &
- ⦃G,L⦄ ⊢ V ➡*[1,h] W0 & ⦃G,L⦄ ⊢ T ➡*[↓a,h] ⓛ{p}W0.U0.
-#a #h #G #L #V #T #H
-elim (cnv_inv_appl … H) -H #n #p #W #U #Ha #HV #HT #HVW #HTU
-lapply (ylt_inv_inj … Ha) -Ha #Ha
-elim (cnv_fwd_aaa … HT) #A #HA
-elim (cpms_total_aaa h … (a-↑n) … (ⓛ{p}W.U))
-[|*: /2 width=8 by cpms_aaa_conf/ ] -HA #X #HU0
-elim (cpms_inv_abst_sn … HU0) #W0 #U0 #HW0 #_ #H destruct
-lapply (cpms_trans … HVW … HW0) -HVW -HW0 #HVW0
-lapply (cpms_trans … HTU … HU0) -HTU -HU0
->(arith_m2 … Ha) -Ha #HTU0
-/2 width=5 by ex4_3_intro/
+lemma cnv_fwd_cpms_abst_dx_le (a) (h) (G) (L) (W) (p):
+ ∀T. ⦃G,L⦄ ⊢ T ![a,h] →
+ ∀n1,U1. ⦃G,L⦄ ⊢ T ➡*[n1,h] ⓛ{p}W.U1 → ∀n2. n1 ≤ n2 →
+ ∃∃U2. ⦃G,L⦄ ⊢ T ➡*[n2,h] ⓛ{p}W.U2 & ⦃G,L.ⓛW⦄ ⊢ U1 ➡*[n2-n1,h] U2.
+#a #h #G #L #W #p #T #H
+elim (cnv_fwd_aaa … H) -H #A #HA
+/2 width=2 by cpms_abst_dx_le_aaa/
qed-.
+
+(* Advanced properties ******************************************************)
+
+lemma cnv_appl_ge (a) (h) (n1) (p) (G) (L):
+ ∀n2. n1 ≤ n2 → appl a n2 →
+ ∀V. ⦃G,L⦄ ⊢ V ![a,h] → ∀T. ⦃G,L⦄ ⊢ T ![a,h] →
+ ∀X. ⦃G,L⦄ ⊢ V ➡*[1,h] X → ∀W. ⦃G,L⦄ ⊢ W ➡*[h] X →
+ ∀U. ⦃G,L⦄ ⊢ T ➡*[n1,h] ⓛ{p}W.U → ⦃G,L⦄ ⊢ ⓐV.T ![a,h].
+#a #h #n1 #p #G #L #n2 #Hn12 #Ha #V #HV #T #HT #X #HVX #W #HW #X #HTX
+elim (cnv_fwd_cpms_abst_dx_le … HT … HTX … Hn12) #U #HTU #_ -n1
+/4 width=11 by cnv_appl, cpms_bind, cpms_cprs_trans/
+qed.
(* *)
(**************************************************************************)
-include "basic_2/rt_computation/cpue_csx.ma".
include "basic_2/rt_conversion/cpce_drops.ma".
-include "basic_2/dynamic/cnv_cpue.ma".
+include "basic_2/dynamic/cnv_cpmhe.ma".
(* CONTEXT-SENSITIVE NATIVE VALIDITY FOR TERMS ******************************)
elim (drops_ldec_dec L i) [ * #K #W #HLK | -H1i -IH #HnX ]
[ lapply (cnv_inv_lref_pair … H2i … HLK) -H2i #H2W
lapply (csx_inv_lref_pair_drops … HLK H1i) -H1i #H1W
- elim (cpue_total_csx … H1W) -H1W #X
+ elim (cpmhe_total_csx … H1W) -H1W #X #n #HWX
elim (abst_dec X) [ * | -IH ]
- [ #p #V1 #U #H destruct * #n #HWU #_
+ [ #p #V1 #U #H destruct
+ lapply (cpmhe_fwd_cpms … HWX) -HWX #HWX
elim (IH G K V1) -IH
[ #V2 #HV12
elim (lifts_total V2 (𝐔❴↑i❵)) #W2 #HVW2
| /3 width=6 by cnv_cpms_trans, cnv_fwd_pair_sn/
| /4 width=6 by fqup_cpms_fwd_fpbg, fpbg_fqu_trans, fqup_lref/
]
- | #HnX #HWX
+ | #HnX
@(ex_intro … (#i))
@cpce_zero_drops #n0 #p #K0 #W0 #V0 #U0 #HLK0 #HWU0
lapply (drops_mono … HLK0 … HLK) -i -L #H destruct
- elim (cnv_cpue_cpms_conf … H2W … HWU0 … HWX) -n0 -W #X0 * #n0 #HUX0 #_ #HX0
- elim (cpms_inv_abst_sn … HUX0) -HUX0 #V1 #U1 #_ #_ #H destruct -n0 -K -V0 -U0
- elim (tueq_inv_bind2 … HX0) -HX0 #U0 #_ #H destruct -U1
+ lapply (cpmhe_abst … HWU0) -HWU0 #HWU0
+ elim (cnv_cpmhe_mono … H2W … HWU0 … HWX) #_ #H -a -n -n0 -W
+ elim (theq_inv_pair1 … H) -V0 -U0 #V0 #U0 #H destruct
/2 width=4 by/
]
| /5 width=3 by cpce_zero_drops, ex1_2_intro, ex_intro/
(* *)
(**************************************************************************)
+include "basic_2/rt_computation/cpms_cpms.ma".
include "basic_2/rt_equivalence/cpes.ma".
-include "basic_2/dynamic/cnv_aaa.ma".
+include "basic_2/dynamic/cnv.ma".
(* CONTEXT-SENSITIVE NATIVE VALIDITY FOR TERMS ******************************)
(* Properties with t-bound rt-equivalence for terms *************************)
lemma cnv_appl_cpes (a) (h) (G) (L):
- ∀n. yinj n < a →
+ ∀n. appl a n →
∀V. ⦃G,L⦄ ⊢ V ![a,h] → ∀T. ⦃G,L⦄ ⊢ T ![a,h] →
∀W. ⦃G,L⦄ ⊢ V ⬌*[h,1,0] W →
∀p,U. ⦃G,L⦄ ⊢ T ➡*[n,h] ⓛ{p}W.U → ⦃G,L⦄ ⊢ ⓐV.T ![a,h].
lemma cnv_inv_appl_cpes (a) (h) (G) (L):
∀V,T. ⦃G,L⦄ ⊢ ⓐV.T ![a,h] →
- ∃∃n,p,W,U. yinj n < a & ⦃G,L⦄ ⊢ V ![a,h] & ⦃G,L⦄ ⊢ T ![a,h] &
+ ∃∃n,p,W,U. appl a n & ⦃G,L⦄ ⊢ V ![a,h] & ⦃G,L⦄ ⊢ T ![a,h] &
⦃G,L⦄ ⊢ V ⬌*[h,1,0] W & ⦃G,L⦄ ⊢ T ➡*[n,h] ⓛ{p}W.U.
#a #h #G #L #V #T #H
elim (cnv_inv_appl … H) -H #n #p #W #U #Hn #HV #HT #HVW #HTU
/3 width=7 by cpms_div, ex5_4_intro/
qed-.
-lemma cnv_inv_appl_pred_cpes (a) (h) (G) (L):
- ∀V,T. ⦃G,L⦄ ⊢ ⓐV.T ![yinj a,h] →
- ∃∃p,W,U. ⦃G,L⦄ ⊢ V ![a,h] & ⦃G,L⦄ ⊢ T ![a,h] &
- ⦃G,L⦄ ⊢ V ⬌*[h,1,0] W & ⦃G,L⦄ ⊢ T ➡*[↓a,h] ⓛ{p}W.U.
-#a #h #G #L #V #T #H
-elim (cnv_inv_appl_pred … H) -H #p #W #U #HV #HT #HVW #HTU
-/3 width=7 by cpms_div, ex4_3_intro/
-qed-.
-
lemma cnv_inv_cast_cpes (a) (h) (G) (L):
∀U,T. ⦃G,L⦄ ⊢ ⓝU.T ![a,h] →
∧∧ ⦃G,L⦄ ⊢ U ![a,h] & ⦃G,L⦄ ⊢ T ![a,h] & ⦃G,L⦄ ⊢ U ⬌*[h,0,1] T.
(∀p,I,G,L,V,T. ⦃G,L⦄ ⊢ V![a,h] → ⦃G,L.ⓑ{I}V⦄⊢T![a,h] →
Q G L V →Q G (L.ⓑ{I}V) T →Q G L (ⓑ{p,I}V.T)
) →
- (∀n,p,G,L,V,W,T,U. yinj n < a → ⦃G,L⦄ ⊢ V![a,h] → ⦃G,L⦄ ⊢ T![a,h] →
+ (∀n,p,G,L,V,W,T,U. appl a n → ⦃G,L⦄ ⊢ V![a,h] → ⦃G,L⦄ ⊢ T![a,h] →
⦃G,L⦄ ⊢ V ⬌*[h,1,0]W → ⦃G,L⦄ ⊢ T ➡*[n,h] ⓛ{p}W.U →
Q G L V → Q G L T → Q G L (ⓐV.T)
) →
lemma cpm_tdeq_inv_appl_sn (a) (h) (n) (G) (L):
∀V,T1. ⦃G,L⦄ ⊢ ⓐV.T1 ![a,h] →
∀X. ⦃G,L⦄ ⊢ ⓐV.T1 ➡[n,h] X → ⓐV.T1 ≛ X →
- ∃∃m,q,W,U1,T2. yinj m < a & ⦃G,L⦄ ⊢ V ![a,h] & ⦃G,L⦄ ⊢ V ➡*[1,h] W & ⦃G,L⦄ ⊢ T1 ➡*[m,h] ⓛ{q}W.U1
+ ∃∃m,q,W,U1,T2. appl a m & ⦃G,L⦄ ⊢ V ![a,h] & ⦃G,L⦄ ⊢ V ➡*[1,h] W & ⦃G,L⦄ ⊢ T1 ➡*[m,h] ⓛ{q}W.U1
& ⦃G,L⦄⊢ T1 ![a,h] & ⦃G,L⦄ ⊢ T1 ➡[n,h] T2 & T1 ≛ T2 & X = ⓐV.T2.
#a #h #n #G #L #V #T1 #H0 #X #H1 #H2
elim (cpm_inv_appl1 … H1) -H1 *
∀T2. ⦃G,L.ⓑ{I}V⦄ ⊢ T1 ➡[n,h] T2 → T1 ≛ T2 →
Q (L.ⓑ{I}V) T1 T2 → Q L (ⓑ{p,I}V.T1) (ⓑ{p,I}V.T2)
) →
- (∀m. yinj m < a →
+ (∀m. appl a m →
∀L,V. ⦃G,L⦄ ⊢ V ![a,h] → ∀W. ⦃G,L⦄ ⊢ V ➡*[1,h] W →
∀p,T1,U1. ⦃G,L⦄ ⊢ T1 ➡*[m,h] ⓛ{p}W.U1 → ⦃G,L⦄⊢ T1 ![a,h] →
∀T2. ⦃G,L⦄ ⊢ T1 ➡[n,h] T2 → T1 ≛ T2 →
include "ground_2/lib/arith_2b.ma".
include "basic_2/rt_computation/cprs_cprs.ma".
-include "basic_2/rt_computation/lprs_cpms.ma".
include "basic_2/dynamic/cnv_drops.ma".
include "basic_2/dynamic/cnv_preserve_sub.ma".
+include "basic_2/dynamic/cnv_aaa.ma".
include "basic_2/dynamic/lsubv_cnv.ma".
(* CONTEXT-SENSITIVE NATIVE VALIDITY FOR TERMS ******************************)
elim (cnv_cpms_strip_lpr_sub … IH2 … HVW1 … HV12 … HL12 … HL12) [|*: /2 width=2 by fqup_fpbg/ ] -HVW1 -HV12
<minus_n_O <minus_O_n #XW1 #HXW1 #HXV2
elim (cnv_cpms_strip_lpr_sub … IH2 … HTU1 … HT12 … HL12 … HL12) [|*: /2 width=2 by fqup_fpbg/ ] -HTU1 -HT12
- #X #H #HTU2 -IH2 -IH1 -L1 -V1 -T1
- elim (cpms_inv_abst_sn … H) -H #W2 #U2 #HW12 #_ #H destruct
+ #X #H #HTX2 -IH2 -IH1 -L1 -V1 -T1
+ elim (cpms_inv_abst_sn … H) -H #W2 #X2 #HW12 #_ #H destruct
elim (cprs_conf … HXW1 … HW12) -W1 #W1 #HXW1 #HW21
lapply (cpms_trans … HXV2 … HXW1) -XW1 <plus_n_O #HV2W1
- lapply (cpms_trans … HTU2 … (ⓛ{p}W1.U2) ?)
- [3:|*: /2 width=2 by cpms_bind/ ] -W2 <plus_n_O #HTU2
- /3 width=7 by cnv_appl, le_ylt_trans/
+ lapply (cpms_trans … HTX2 … (ⓛ{p}W1.X2) ?)
+ [3:|*: /2 width=2 by cpms_bind/ ] -W2 <plus_n_O #HTX2
+ elim (cnv_fwd_cpms_abst_dx_le … HT2 … HTX2 n) -HTX2 [| // ] #U2 #HTU2 #_ -X2
+ /2 width=7 by cnv_appl/
| #q #V2 #W10 #W20 #T10 #T20 #HV12 #HW120 #HT120 #H1 #H2 destruct
elim (cnv_inv_bind … HT1) -HT1 #HW10 #HT10
elim (cpms_inv_abst_sn … HTU1) -HTU1 #W30 #T30 #HW130 #_ #H destruct -T30
elim (cnv_cpms_strip_lpr_sub … IH2 … HVW1 … HV10 … HL12 … HL12) [|*: /2 width=2 by fqup_fpbg/ ] -HVW1 -HV10
<minus_n_O <minus_O_n #XW1 #HXW1 #HXV0
elim (cnv_cpms_strip_lpr_sub … IH2 … HTU0 … HT02 … (L2.ⓓW2) … (L2.ⓓW2)) [|*: /2 width=2 by fqup_fpbg, lpr_pair/ ] -HTU0 -HT02 -HW02
- #X #H #HTU2 -IH2 -IH1 -L1 -W0 -T0 -U1
- elim (cpms_inv_abst_sn … H) -H #W #U2 #HW3 #_ #H destruct -U3
+ #X #H #HTX2 -IH2 -IH1 -L1 -W0 -T0 -U1
+ elim (cpms_inv_abst_sn … H) -H #W #X2 #HW3 #_ #H destruct -U3
lapply (cnv_lifts … HV0 (Ⓣ) … (L2.ⓓW2) … HV02) /3 width=1 by drops_refl, drops_drop/ -HV0 #HV2
elim (cpms_lifts_sn … HXV0 (Ⓣ) … (L2.ⓓW2) … HV02) /3 width=1 by drops_refl, drops_drop/ -V0 #XW2 #HXW12 #HXVW2
lapply (cpms_lifts_bi … HXW1 (Ⓣ) … (L2.ⓓW2) … HW13 … HXW12) /3 width=1 by drops_refl, drops_drop/ -W1 -XW1 #HXW32
elim (cprs_conf … HXW32 … HW3) -W3 #W3 #HXW23 #HW3
lapply (cpms_trans … HXVW2 … HXW23) -XW2 <plus_n_O #H1
- lapply (cpms_trans … HTU2 ? (ⓛ{p}W3.U2) ?) [3:|*:/2 width=2 by cpms_bind/ ] -W #H2
- /4 width=7 by cnv_appl, cnv_bind, le_ylt_trans/
+ lapply (cpms_trans … HTX2 ? (ⓛ{p}W3.X2) ?) [3:|*:/2 width=2 by cpms_bind/ ] -W #H2
+ elim (cnv_fwd_cpms_abst_dx_le … HT2 … H2 n) -H2 [| // ] #U2 #HTU2 #_ -X2
+ /3 width=7 by cnv_appl, cnv_bind/
]
| #W1 #T1 #HG0 #HL0 #HT0 #H1 #x #X #H2 #L2 #HL12 destruct
elim (cnv_inv_cast … H1) -H1 #U1 #HW1 #HT1 #HWU1 #HTU1
--- /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_computation/cpms_cnh.ma".
+include "basic_2/rt_computation/cpmhe_csx.ma".
+include "basic_2/rt_equivalence/cpes.ma".
+include "basic_2/dynamic/cnv_preserve.ma".
+
+(* CONTEXT-SENSITIVE NATIVE VALIDITY FOR TERMS ******************************)
+
+(* Properties with head evaluation for t-bound rt-transition on terms *******)
+
+lemma cnv_cpmhe_trans (a) (h) (G) (L):
+ ∀T1. ⦃G,L⦄ ⊢ T1 ![a,h] →
+ ∀T2,n. ⦃G,L⦄ ⊢ T1 ➡*[h,n] 𝐍*⦃T2⦄ → ⦃G,L⦄ ⊢ T2 ![a,h].
+/3 width=4 by cpmhe_fwd_cpms, cnv_cpms_trans/ qed-.
+
+lemma cnv_R_cpmhe_total (a) (h) (G) (L):
+ ∀T1. ⦃G,L⦄ ⊢ T1 ![a,h] → ∃n. R_cpmhe h G L T1 n.
+/4 width=2 by cnv_fwd_fsb, fsb_inv_csx, R_cpmhe_total_csx/ qed-.
+
+axiom cnv_R_cpmhe_dec (a) (h) (G) (L):
+ ∀T. ⦃G,L⦄ ⊢ T ![a,h] → ∀n. Decidable (R_cpmhe h G L T n).
+
+(* Main inversions with head evaluation for t-bound rt-transition on terms **)
+
+theorem cnv_cpmhe_mono (a) (h) (G) (L):
+ ∀T0. ⦃G,L⦄ ⊢ T0 ![a,h] → ∀T1,n1. ⦃G,L⦄ ⊢ T0 ➡*[h,n1] 𝐍*⦃T1⦄ →
+ ∀T2,n2. ⦃G,L⦄ ⊢ T0 ➡*[h,n2] 𝐍*⦃T2⦄ →
+ ∧∧ ⦃G,L⦄ ⊢ T1 ⬌*[h,n2-n1,n1-n2] T2 & T1 ⩳ T2.
+#a #h #G #L #T0 #HT0 #T1 #n1 * #HT01 #HT1 #T2 #n2 * #HT02 #HT2
+elim (cnv_cpms_conf … HT0 … HT01 … HT02) -T0 #T0 #HT10 #HT20
+/4 width=8 by cpms_div, cpms_inv_cnh_sn, theq_canc_dx, conj/
+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_computation/cpms_cnu.ma".
-include "basic_2/rt_computation/cpue.ma".
-include "basic_2/dynamic/cnv_preserve.ma".
-
-(* CONTEXT-SENSITIVE NATIVE VALIDITY FOR TERMS ******************************)
-
-(* Properties with evaluation for t-unbound rt-transition on terms **********)
-
-lemma cnv_cpue_trans (a) (h) (G) (L):
- ∀T1. ⦃G,L⦄ ⊢ T1 ![a,h] →
- ∀T2. ⦃G,L⦄ ⊢ T1 ⥲*[h] 𝐍⦃T2⦄ → ⦃G,L⦄ ⊢ T2 ![a,h].
-#a #h #G #L #T1 #HT1 #T2 * #n #HT12 #_
-/2 width=4 by cnv_cpms_trans/
-qed-.
-
-lemma cnv_cpue_cpms_conf (a) (h) (n) (G) (L):
- ∀T0. ⦃G,L⦄ ⊢ T0 ![a,h] → ∀T1. ⦃G,L⦄ ⊢ T0 ➡*[n,h] T1 →
- ∀T2. ⦃G,L⦄ ⊢ T0 ⥲*[h] 𝐍⦃T2⦄ →
- ∃∃T. ⦃G,L⦄ ⊢ T1 ⥲*[h] 𝐍⦃T⦄ & T2 ≅ T.
-#a #h #n1 #G #L #T0 #HT0 #T1 #HT01 #T2 * #n2 #HT02 #HT2
-elim (cnv_cpms_conf … HT0 … HT01 … HT02) -T0 #T0 #HT10 #HT20
-lapply (cpms_inv_cnu_sn … HT20 HT2) -HT20 #HT20
-/4 width=8 by cnu_tueq_trans, ex2_intro/
-qed-.
-
-(* Main properties with evaluation for t-unbound rt-transition on terms *****)
-
-theorem cnv_cpue_mono (a) (h) (G) (L):
- ∀T0. ⦃G,L⦄ ⊢ T0 ![a,h] → ∀T1. ⦃G,L⦄ ⊢ T0 ⥲*[h] 𝐍⦃T1⦄ →
- ∀T2. ⦃G,L⦄ ⊢ T0 ⥲*[h] 𝐍⦃T2⦄ → T1 ≅ T2.
-#a #h #G #L #T0 #HT0 #T1 * #n1 #HT01 #HT1 #T2 * #n2 #HT02 #HT2
-elim (cnv_cpms_conf … HT0 … HT01 … HT02) -T0 #T0 #HT10 #HT20
-/3 width=8 by cpms_inv_cnu_sn, tueq_canc_dx/
-qed-.
(* *)
(**************************************************************************)
-include "basic_2/rt_computation/cpue_csx.ma".
-include "basic_2/rt_equivalence/cpes_cprs.ma".
-include "basic_2/dynamic/cnv_cpue.ma".
+include "basic_2/rt_equivalence/cpes_cpes.ma".
+include "basic_2/dynamic/cnv_cpmhe.ma".
include "basic_2/dynamic/cnv_cpes.ma".
include "basic_2/dynamic/cnv_preserve_cpes.ma".
(* main properties with evaluations for rt-transition on terms **************)
-theorem cnv_dec (a) (h) (G) (L) (T):
+theorem cnv_dec (a) (h) (G) (L) (T): ac_props a →
Decidable (⦃G,L⦄ ⊢ T ![a,h]).
-#a #h #G #L #T
+#a #h #G #L #T #Ha
@(fqup_wf_ind_eq (Ⓣ) … G L T) -G -L -T #G0 #L0 #T0 #IH #G #L * * [|||| * ]
-[ #s #HG #HL #HT destruct -IH
+[ #s #HG #HL #HT destruct -Ha -IH
/2 width=1 by cnv_sort, or_introl/
-| #i #HG #HL #HT destruct
+| #i #HG #HL #HT destruct -Ha
elim (drops_F_uni L i) [| * * ]
[ /3 width=8 by cnv_inv_lref_atom, or_intror/
| /3 width=9 by cnv_inv_lref_unit, or_intror/
| /4 width=5 by cnv_inv_lref_pair, or_intror/
]
]
-| #l #HG #HL #HT destruct -IH
+| #l #HG #HL #HT destruct -Ha -IH
/3 width=6 by cnv_inv_gref, or_intror/
-| #p #I #V #T #HG #HL #HT destruct
+| #p #I #V #T #HG #HL #HT destruct -Ha
elim (IH G L V) [| -IH | // ] #HV
[ elim (IH G (L.ⓑ{I}V) T) -IH [3: // ] #HT
[ /3 width=1 by cnv_bind, or_introl/ ]
| #V #T #HG #HL #HT destruct
elim (IH G L V) [| -IH #HV | // ]
[ elim (IH G L T) -IH [| #HT #HV | // ]
- [ cases a -a [ * [| #a ]] #HT #HV
- [ @or_intror #H
- elim (cnv_inv_appl … H) -H #n #p #W #U #H #_ #_ #_ #_
- /3 width=2 by lt_zero_false, ylt_inv_inj/
- | elim (cnv_fwd_aaa … HT) #A #HA
- elim (cpme_total_aaa h a … HA) #X
- elim (abst_dec X) [ * ]
- [ #p #W #U #H #HTU destruct
+ [ #HT #HV
+ elim (cnv_R_cpmhe_total … HT) #n #Hn
+ elim (dec_min (R_cpmhe h G L T) … Hn) -Hn
+ [| /2 width=2 by cnv_R_cpmhe_dec/ ] #n0 #_ -n
+ elim (ac_dec … Ha n0) -Ha
+ [ * #n #Hn #Ha * #X0 #HX0 #_
+ elim (abst_dec X0)
+ [ * #p #W #U0 #H destruct
elim (cnv_cpes_dec … 1 0 … HV W) [ #HVW | #HnVW ]
- [ elim HTU -HTU #HTU #_
- /4 width=7 by ylt_inj, cnv_appl_cpes, or_introl/
- | @or_intror #H
- elim (cnv_inv_appl_pred_cpes … H) -H #q #W0 #U0 #_ #_ #HVW0 #HTU0
- elim (cnv_cpme_cpms_conf … HT … HTU0 … HTU) -T #HU0 #_
- elim (cpms_inv_abst_bi … HU0) -HU0 #_ #HW0 #_ -p -q -U0
- /3 width=3 by cpes_cprs_trans/
- | lapply (cnv_cpme_trans … HT … HTU) -T #H
+ [ lapply (cpmhe_fwd_cpms … HX0) -HX0 #HTU0
+ elim (cnv_fwd_cpms_abst_dx_le … HT … HTU0 … Hn) #U #HTU #_ -U0 -n0
+ /3 width=7 by cnv_appl_cpes, or_introl/
+(* Note: argument type mismatch *)
+ | @or_intror #H -n
+ elim (cnv_inv_appl_cpes … H) -H #m0 #q #WX #UX #_ #_ #_ #HVWX #HTUX
+ lapply (cpmhe_abst … HTUX) -HTUX #HTUX
+ elim (cnv_cpmhe_mono … HT … HTUX … HX0) -a -T #H #_
+ elim (cpes_fwd_abst_bi … H) -H #_ #HWX -n0 -m0 -p -q -UX -U0
+ /3 width=3 by cpes_cpes_trans/
+ | lapply (cnv_cpmhe_trans … HT … HX0) -T #H
elim (cnv_inv_bind … H) -H #HW #_ //
]
- | #HnTU #HTX
+(* Note: no expected type *)
+ | #HnX0
@or_intror #H
- elim (cnv_inv_appl_pred_cpes … H) -H #q #W0 #U0 #_ #_ #_ #HTU0
- elim (cnv_cpme_cpms_conf … HT … HTU0 … HTX) -T #HX #_
- elim (cpms_inv_abst_sn … HX) -HX #V0 #T0 #_ #_ #H destruct -W0 -U0
- /2 width=4 by/
- ]
- | elim (cpue_total_csx h G L T)
- [| /3 width=2 by cnv_fwd_fsb, fsb_inv_csx/ ] #X
- elim (abst_dec X) [ * ]
- [ #p #W #U #H #HTU destruct
- elim (cnv_cpes_dec … 1 0 … HV W) [ #HVW | #HnVW ]
- [ elim HTU -HTU #n #HTU #_
- /3 width=7 by cnv_appl_cpes, or_introl/
- | @or_intror #H
- elim (cnv_inv_appl_cpes … H) -H #m1 #q #W0 #U0 #_ #_ #_ #HVW0 #HTU0
- elim (cnv_cpue_cpms_conf … HT … HTU0 … HTU) -m1 -T #X * #m2 #HU0X #_ #HUX
- elim (tueq_inv_bind1 … HUX) -HUX #X0 #_ #H destruct -U
- elim (cpms_inv_abst_bi … HU0X) -HU0X #_ #HW0 #_ -p -q -m2 -U0 -X0
- /3 width=3 by cpes_cprs_trans/
- | lapply (cnv_cpue_trans … HT … HTU) -T #H
- elim (cnv_inv_bind … H) -H #HW #_ //
- ]
- | #HnTU #HTX
- @or_intror #H
- elim (cnv_inv_appl_cpes … H) -H #m1 #q #W0 #U0 #_ #_ #_ #_ #HTU0
- elim (cnv_cpue_cpms_conf … HT … HTU0 … HTX) -m1 -T #X0 * #m2 #HUX0 #_ #HX0
- elim (cpms_inv_abst_sn … HUX0) -HUX0 #V0 #T0 #_ #_ #H destruct -m2 -W0 -U0
- elim (tueq_inv_bind2 … HX0) -HX0 #X0 #_ #H destruct
+ elim (cnv_inv_appl_cpes … H) -H #m0 #q #W0 #U0 #_ #_ #_ #_ #HTU0
+ lapply (cpmhe_abst … HTU0) -HTU0 #HTU0
+ elim (cnv_cpmhe_mono … HT … HTU0 … HX0) -T #_ #H
+ elim (theq_inv_pair1 … H) -W0 -U0 #W0 #U0 #H destruct
/2 width=4 by/
]
+(* Note: failed applicability *)
+ | #Hge #_ #Hlt
+ @or_intror #H
+ elim (cnv_inv_appl … H) -H #m0 #q #W0 #U0 #Hm0 #_ #_ #_ #HTU0
+ elim (lt_or_ge m0 n0) #H0 [| /3 width=3 by ex2_intro/ ] -Hm0 -Hge
+ /4 width=6 by cpmhe_abst, ex_intro/
]
]
]
(* NATIVE TYPE ASSIGNMENT FOR TERMS *****************************************)
definition nta (a) (h): relation4 genv lenv term term ≝
- λG,L,T,U. ⦃G,L⦄ ⊢ ⓝU.T ![a,h].
+ λG,L,T,U. ⦃G,L⦄ ⊢ ⓝU.T ![a,h].
interpretation "native type assignment (term)"
'Colon a h G L T U = (nta a h G L T U).
interpretation "restricted native type assignment (term)"
- 'Colon h G L T U = (nta (yinj (S (S O))) h G L T U).
+ 'Colon h G L T U = (nta (ac_eq (S O)) h G L T U).
interpretation "extended native type assignment (term)"
- 'ColonStar h G L T U = (nta Y h G L T U).
+ 'ColonStar h G L T U = (nta ac_top h G L T U).
(* Basic properties *********************************************************)
include "basic_2/rt_computation/cprs_cprs.ma".
include "basic_2/rt_computation/lprs_cpms.ma".
+include "basic_2/dynamic/cnv_aaa.ma".
include "basic_2/dynamic/nta.ma".
(* NATIVE TYPE ASSIGNMENT FOR TERMS *****************************************)
(* Properties with advanced rt_computation for terms ************************)
-(* Basic_2A1: was by definition nta_appl ntaa_appl *)
-lemma nta_appl_abst (a) (h) (p) (G) (K): yinj 0 < a →
- ∀V,W. ⦃G,K⦄ ⊢ V :[a,h] W →
- ∀T,U. ⦃G,K.ⓛW⦄ ⊢ T :[a,h] U → ⦃G,K⦄ ⊢ ⓐV.ⓛ{p}W.T :[a,h] ⓐV.ⓛ{p}W.U.
-#a #h #p #G #K #Ha #V #W #H1 #T #U #H2
+(* Basic_2A1: uses by definition nta_appl ntaa_appl *)
+lemma nta_appl_abst (a) (h) (p) (G) (L):
+ ∀n. appl a n →
+ ∀V,W. ⦃G,L⦄ ⊢ V :[a,h] W →
+ ∀T,U. ⦃G,L.ⓛW⦄ ⊢ T :[a,h] U → ⦃G,L⦄ ⊢ ⓐV.ⓛ{p}W.T :[a,h] ⓐV.ⓛ{p}W.U.
+#a #h #p #G #L #n #Ha #V #W #H1 #T #U #H2
elim (cnv_inv_cast … H1) -H1 #X1 #HW #HV #HWX1 #HVX1
elim (cnv_inv_cast … H2) -H2 #X2 #HU #HT #HUX2 #HTX2
-/4 width=7 by cnv_bind, cnv_appl, cnv_cast, cpms_appl_dx, cpms_bind_dx/
+/4 width=11 by cnv_appl_ge, cnv_cast, cnv_bind, cpms_appl_dx, cpms_bind_dx/
qed.
(* Basic_1: was by definition: ty3_appl *)
(* Basic_2A1: was nta_appl_old *)
-lemma nta_appl (a) (h) (p) (G) (L): yinj 1 < a →
+lemma nta_appl (a) (h) (p) (G) (L):
+ ∀n. 1 ≤ n → appl a n →
∀V,W. ⦃G,L⦄ ⊢ V :[a,h] W →
∀T,U. ⦃G,L⦄ ⊢ T :[a,h] ⓛ{p}W.U → ⦃G,L⦄ ⊢ ⓐV.T :[a,h] ⓐV.ⓛ{p}W.U.
-#a #h #p #G #L #Ha #V #W #H1 #T #U #H2
+#a #h #p #G #L #n #Hn #Ha #V #W #H1 #T #U #H2
elim (cnv_inv_cast … H1) -H1 #X1 #HW #HV #HWX1 #HVX1
elim (cnv_inv_cast … H2) -H2 #X2 #HU #HT #HUX2 #HTX2
elim (cpms_inv_abst_sn … HUX2) #W0 #U0 #HW0 #HU0 #H destruct
elim (cprs_conf … HWX1 … HW0) -HW0 #X0 #HX10 #HWX0
@(cnv_cast … (ⓐV.ⓛ{p}W0.U0)) (**) (* full auto too slow *)
-[ /3 width=7 by cnv_appl, cpms_bind, lt_ylt_trans/
-| /4 width=11 by cnv_appl, cpms_cprs_trans, cpms_bind/
+[ /2 width=11 by cnv_appl_ge/
+| /3 width=11 by cnv_appl_ge, cpms_cprs_trans/
| /2 width=1 by cpms_appl_dx/
| /2 width=1 by cpms_appl_dx/
]
(* Properties with evaluations for rt-transition on terms *******************)
-lemma nta_typecheck_dec (a) (h) (G) (L):
+lemma nta_typecheck_dec (a) (h) (G) (L): ac_props a →
∀T,U. Decidable … (⦃G,L⦄ ⊢ T :[a,h] U).
/2 width=1 by cnv_dec/ qed-.
(* Basic_1: uses: ty3_inference *)
-lemma nta_inference_dec (a) (h) (G) (L) (T):
+lemma nta_inference_dec (a) (h) (G) (L) (T): ac_props a →
∨∨ ∃U. ⦃G,L⦄ ⊢ T :[a,h] U
| ∀U. (⦃G,L⦄ ⊢ T :[a,h] U → ⊥).
-#a #h #G #L #T
-elim (cnv_dec a h G L T)
+#a #h #G #L #T #Ha
+elim (cnv_dec … h G L T Ha) -Ha
[ /3 width=1 by cnv_nta_sn, or_introl/
| /4 width=2 by nta_fwd_cnv_sn, or_intror/
]
/4 width=5 by nta_bind_cnv/
| #V #T #HG #HL #HT #X #H destruct
elim (nta_inv_appl_sn … H) -H #p #W #U #HVW #HTU #HUX #HX
- /4 width=9 by nta_appl, ylt_inj/
+ /4 width=9 by nta_appl/
| #U #T #HG #HL #HT #X #H destruct
elim (nta_inv_cast_sn … H) -H #HTU #HUX #HX
/4 width=4 by nta_cast/
∃∃p,W,U. ⦃G,L⦄ ⊢ V :[h] W & ⦃G,L⦄ ⊢ T :[h] ⓛ{p}W.U & ⦃G,L⦄ ⊢ ⓐV.ⓛ{p}W.U ⬌*[h] X2 & ⦃G,L⦄ ⊢ X2 ![h].
#h #G #L #X2 #V #T #H
elim (cnv_inv_cast … H) -H #X #HX2 #H1 #HX2 #H2
-elim (cnv_inv_appl_pred … H1) #p #W #U #HV #HT #HVW #HTU
+elim (cnv_inv_appl … H1) #n #p #W #U #H <H -n #HV #HT #HVW #HTU
/5 width=11 by cnv_cpms_nta, cnv_cpms_conf_eq, cpcs_cprs_div, cpms_appl_dx, ex4_3_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/notation/relations/preditnormal_4.ma".
+include "static_2/syntax/tueq.ma".
+include "basic_2/rt_transition/cpm.ma".
+
+(* NORMAL TERMS FOR T-UNUNBOUND RT-TRANSITION *******************************)
+
+definition cnu (h) (G) (L): predicate term ≝
+ λT1. ∀n,T2. ⦃G,L⦄ ⊢ T1 ➡[n,h] T2 → T1 ≅ T2.
+
+interpretation
+ "normality for t-unbound context-sensitive parallel rt-transition (term)"
+ 'PRedITNormal h G L T = (cnu h G L T).
+
+(* Basic properties *********************************************************)
+
+lemma cnu_sort (h) (G) (L): ∀s. ⦃G,L⦄ ⊢ ⥲[h] 𝐍⦃⋆s⦄.
+#h #G #L #s1 #n #X #H
+elim (cpm_inv_sort1 … H) -H #H #_ destruct //
+qed.
+
+lemma cnu_ctop (h) (G): ∀i. ⦃G,⋆⦄ ⊢ ⥲[h] 𝐍⦃#i⦄.
+#h #G * [| #i ] #n #X #H
+[ elim (cpm_inv_zero1 … H) -H *
+ [ #H #_ destruct //
+ | #Y #X1 #X2 #_ #_ #H destruct
+ | #m #Y #X1 #X2 #_ #_ #H destruct
+ ]
+| elim (cpm_inv_lref1 … H) -H *
+ [ #H #_ destruct //
+ | #Z #Y #X0 #_ #_ #H destruct
+ ]
+]
+qed.
+
+lemma cnu_zero (h) (G) (L): ∀I. ⦃G,L.ⓤ{I}⦄ ⊢ ⥲[h] 𝐍⦃#0⦄.
+#h #G #L #I #n #X #H
+elim (cpm_inv_zero1 … H) -H *
+[ #H #_ destruct //
+| #Y #X1 #X2 #_ #_ #H destruct
+| #m #Y #X1 #X2 #_ #_ #H destruct
+]
+qed.
+
+lemma cnu_gref (h) (G) (L): ∀l. ⦃G,L⦄ ⊢ ⥲[h] 𝐍⦃§l⦄.
+#h #G #L #l1 #n #X #H
+elim (cpm_inv_gref1 … H) -H #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 "basic_2/rt_transition/cnr.ma".
+include "basic_2/rt_transition/cnu.ma".
+
+(* NORMAL TERMS FOR T-UNUNBOUND RT-TRANSITION *******************************)
+
+(* Advanced properties with normal terms for r-transition *******************)
+
+lemma cnu_abst (h) (p) (G) (L):
+ ∀W. ⦃G,L⦄ ⊢ ➡[h] 𝐍⦃W⦄ → ∀T.⦃G,L.ⓛW⦄ ⊢ ⥲[h] 𝐍⦃T⦄ → ⦃G,L⦄ ⊢ ⥲[h] 𝐍⦃ⓛ{p}W.T⦄.
+#h #p #G #L #W1 #HW1 #T1 #HT1 #n #X #H
+elim (cpm_inv_abst1 … H) -H #W2 #T2 #HW12 #HT12 #H destruct
+<(HW1 … HW12) -W2 /3 width=2 by tueq_bind/
+qed.
+
+lemma cnu_abbr_neg (h) (G) (L):
+ ∀V. ⦃G,L⦄ ⊢ ➡[h] 𝐍⦃V⦄ → ∀T.⦃G,L.ⓓV⦄ ⊢ ⥲[h] 𝐍⦃T⦄ → ⦃G,L⦄ ⊢ ⥲[h] 𝐍⦃-ⓓV.T⦄.
+#h #G #L #V1 #HV1 #T1 #HT1 #n #X #H
+elim (cpm_inv_abbr1 … H) -H *
+[ #V2 #T2 #HV12 #HT12 #H destruct
+ <(HV1 … HV12) -V2 /3 width=2 by tueq_bind/
+| #X1 #_ #_ #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 "basic_2/rt_transition/cpm_simple.ma".
+include "basic_2/rt_transition/cnr.ma".
+include "basic_2/rt_transition/cnu.ma".
+
+(* NORMAL TERMS FOR T-UNUNBOUND RT-TRANSITION *******************************)
+
+(* Advanced properties with simple terms and normal terms for r-transition **)
+
+lemma cnu_appl_simple (h) (G) (L):
+ ∀V,T. ⦃G,L⦄ ⊢ ➡[h] 𝐍⦃V⦄ → ⦃G,L⦄ ⊢ ⥲[h] 𝐍⦃T⦄ → 𝐒⦃T⦄ → ⦃G,L⦄ ⊢ ⥲[h] 𝐍⦃ⓐV.T⦄.
+#h #G #L #V1 #T1 #HV1 #HT1 #HS #n #X #H
+elim (cpm_inv_appl1_simple … H HS) -H -HS #V2 #T2 #HV12 #HT12 #H destruct
+lapply (HV1 … HV12) -HV1 -HV12 #H destruct
+/3 width=2 by tueq_appl/
+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/syntax/tueq_tueq.ma".
+include "basic_2/rt_transition/cpm_tueq.ma".
+include "basic_2/rt_transition/cnu.ma".
+
+(* NORMAL TERMS FOR T-UNUNBOUND RT-TRANSITION *******************************)
+
+(* Advanced properties ******************************************************)
+
+lemma cnu_tueq_trans (h) (G) (L):
+ ∀T1. ⦃G,L⦄ ⊢ ⥲[h] 𝐍⦃T1⦄ → ∀T2.T1 ≅ T2 → ⦃G,L⦄ ⊢ ⥲[h] 𝐍⦃T2⦄.
+#h #G #L #T1 #HT1 #T2 #HT12 #n #T0 #HT20
+@(tueq_canc_sn … HT12)
+elim (tueq_cpm_trans … HT12 … HT20) -T2 #T2 #HT13 #HT30
+/3 width=3 by tueq_trans/
+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_tueq.ma".
+include "basic_2/rt_transition/cpm_drops.ma".
+include "basic_2/rt_transition/cnu.ma".
+
+(* NORMAL TERMS FOR T-UNUNBOUND RT-TRANSITION *******************************)
+
+(* Advanced properties ******************************************************)
+
+lemma cnu_atom_drops (h) (b) (G) (L):
+ ∀i. ⬇*[b,𝐔❴i❵] L ≘ ⋆ → ⦃G,L⦄ ⊢ ⥲[h] 𝐍⦃#i⦄.
+#h #b #G #L #i #Hi #n #X #H
+elim (cpm_inv_lref1_drops … H) -H * [ // || #m ] #K #V1 #V2 #HLK
+lapply (drops_gen b … HLK) -HLK #HLK
+lapply (drops_mono … Hi … HLK) -L #H destruct
+qed.
+
+lemma cnu_unit_drops (h) (I) (G) (L):
+ ∀K,i. ⬇*[i] L ≘ K.ⓤ{I} → ⦃G,L⦄ ⊢ ⥲[h] 𝐍⦃#i⦄.
+#h #I #G #L #K #i #HLK #n #X #H
+elim (cpm_inv_lref1_drops … H) -H * [ // || #m ] #Y #V1 #V2 #HLY
+lapply (drops_mono … HLK … HLY) -L #H destruct
+qed.
+
+(* Properties with generic relocation ***************************************)
+
+lemma cnu_lifts (h) (G): d_liftable1 … (cnu h G).
+#h #G #K #T #HT #b #f #L #HLK #U #HTU #n #U0 #H
+elim (cpm_inv_lifts_sn … H … HLK … HTU) -b -L #T0 #HTU0 #HT0
+lapply (HT … HT0) -G -K /2 width=6 by tueq_lifts_bi/
+qed-.
+
+(* Inversion lemmas with generic relocation *********************************)
+
+lemma cnu_inv_lifts (h) (G): d_deliftable1 … (cnu h G).
+#h #G #L #U #HU #b #f #K #HLK #T #HTU #n #T0 #H
+elim (cpm_lifts_sn … H … HLK … HTU) -b -K #U0 #HTU0 #HU0
+lapply (HU … HU0) -G -L /2 width=6 by tueq_inv_lifts_bi/
+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_tueq.ma".
+include "basic_2/rt_transition/cnu.ma".
+
+(* NORMAL TERMS FOR T-UNUNBOUND RT-TRANSITION *******************************)
+
+(* Advanced properties with uniform relocation for terms ********************)
+
+lemma cnu_lref (h) (I) (G) (L):
+ ∀i. ⦃G,L⦄ ⊢ ⥲[h] 𝐍⦃#i⦄ → ⦃G,L.ⓘ{I}⦄ ⊢ ⥲[h] 𝐍⦃#↑i⦄.
+#h #I #G #L #i #Hi #n #X #H
+elim (cpm_inv_lref1 … H) -H *
+[ #H #_ destruct //
+| #J #K #V #HV #HVX #H destruct
+ lapply (Hi … HV) -Hi -HV #HV
+ elim (tueq_lifts_dx … HV … HVX) -V #Xi #Hi #HX
+ lapply (lifts_inv_lref1_uni … Hi) -Hi #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 "basic_2/rt_transition/cnr_tdeq.ma".
+include "basic_2/rt_transition/cnu_drops.ma".
+include "basic_2/rt_transition/cnu_cnr.ma".
+include "basic_2/rt_transition/cnu_cnr_simple.ma".
+
+(* NORMAL TERMS FOR T-UNUNBOUND RT-TRANSITION *******************************)
+
+(* Properties with context-free sort-irrelevant equivalence for terms *******)
+
+lemma cnu_dec_tdeq (h) (G) (L):
+ ∀T1. ∨∨ ⦃G,L⦄ ⊢ ⥲[h] 𝐍⦃T1⦄
+ | ∃∃n,T2. ⦃G,L⦄ ⊢ T1 ➡[n,h] T2 & (T1 ≛ T2 → ⊥).
+#h #G #L #T1
+@(fqup_wf_ind_eq (Ⓣ) … G L T1) -G -L -T1 #G0 #L0 #T0 #IH #G #L * *
+[ #s #HG #HL #HT destruct -IH
+ /3 width=5 by cnu_sort, or_introl/
+| #i #HG #HL #HT destruct -IH
+ elim (drops_F_uni L i)
+ [ /3 width=7 by cnu_atom_drops, or_introl/
+ | * * [ #I | * #V ] #K #HLK
+ [ /3 width=8 by cnu_unit_drops, or_introl/
+ | elim (lifts_total V 𝐔❴↑i❵) #W #HVW
+ @or_intror @(ex2_2_intro … W) [1,2: /2 width=7 by cpm_delta_drops/ ] #H
+ lapply (tdeq_inv_lref1 … H) -H #H destruct
+ /2 width=5 by lifts_inv_lref2_uni_lt/
+ | elim (lifts_total V 𝐔❴↑i❵) #W #HVW
+ @or_intror @(ex2_2_intro … W) [1,2: /2 width=7 by cpm_ell_drops/ ] #H
+ lapply (tdeq_inv_lref1 … H) -H #H destruct
+ /2 width=5 by lifts_inv_lref2_uni_lt/
+ ]
+ ]
+| #l #HG #HL #HT destruct -IH
+ /3 width=5 by cnu_gref, or_introl/
+| #p * [ cases p ] #V1 #T1 #HG #HL #HT destruct
+ [ elim (cpr_subst h G (L.ⓓV1) T1 0 L V1) [| /2 width=1 by drops_refl/ ] #T2 #X2 #HT12 #HXT2 -IH
+ elim (tdeq_dec T1 T2) [ -HT12 #HT12 | #HnT12 ]
+ [ elim (tdeq_inv_lifts_dx … HT12 … HXT2) -T2 #X1 #HXT1 #_ -X2
+ @or_intror @(ex2_2_intro … X1) [1,2: /2 width=4 by cpm_zeta/ ] #H
+ /2 width=7 by tdeq_lifts_inv_pair_sn/
+ | @or_intror @(ex2_2_intro … (+ⓓV1.T2)) [1,2: /2 width=2 by cpm_bind/ ] #H
+ elim (tdeq_inv_pair … H) -H /2 width=1 by/
+ ]
+ | elim (cnr_dec_tdeq h G L V1) [ elim (IH G (L.ⓓV1) T1) [| * | // ] | * ] -IH
+ [ #HT1 #HV1 /3 width=7 by cnu_abbr_neg, or_introl/
+ | #n #T2 #HT12 #HnT12 #_
+ @or_intror @(ex2_2_intro … (-ⓓV1.T2)) [1,2: /2 width=2 by cpm_bind/ ] #H
+ elim (tdeq_inv_pair … H) -H /2 width=1 by/
+ | #V2 #HV12 #HnV12
+ @or_intror @(ex2_2_intro … (-ⓓV2.T1)) [1,2: /2 width=2 by cpr_pair_sn/ ] #H
+ elim (tdeq_inv_pair … H) -H /2 width=1 by/
+ ]
+ | elim (cnr_dec_tdeq h G L V1) [ elim (IH G (L.ⓛV1) T1) [| * | // ] | * ] -IH
+ [ #HT1 #HV1 /3 width=7 by cnu_abst, or_introl/
+ | #n #T2 #HT12 #HnT12 #_
+ @or_intror @(ex2_2_intro … (ⓛ{p}V1.T2)) [1,2: /2 width=2 by cpm_bind/ ] #H
+ elim (tdeq_inv_pair … H) -H /2 width=1 by/
+ | #V2 #HV12 #HnV12
+ @or_intror @(ex2_2_intro … (ⓛ{p}V2.T1)) [1,2: /2 width=2 by cpr_pair_sn/ ] #H
+ elim (tdeq_inv_pair … H) -H /2 width=1 by/
+ ]
+ ]
+| * #V1 #T1 #HG #HL #HT destruct [| -IH ]
+ [ elim (cnr_dec_tdeq h G L V1) [ elim (IH G L T1) [| * | // ] | * ] -IH
+ [ #HT1 #HV1
+ elim (simple_dec_ex T1) [| * #p * #W1 #U1 #H destruct ]
+ [ /3 width=7 by cnu_appl_simple, or_introl/
+ | elim (lifts_total V1 𝐔❴1❵) #X1 #HVX1
+ @or_intror @(ex2_2_intro … (ⓓ{p}W1.ⓐX1.U1)) [1,2: /2 width=3 by cpm_theta/ ] #H
+ elim (tdeq_inv_pair … H) -H #H destruct
+ | @or_intror @(ex2_2_intro … (ⓓ{p}ⓝW1.V1.U1)) [1,2: /2 width=2 by cpm_beta/ ] #H
+ elim (tdeq_inv_pair … H) -H #H destruct
+ ]
+ | #n #T2 #HT12 #HnT12 #_
+ @or_intror @(ex2_2_intro … (ⓐV1.T2)) [1,2: /2 width=2 by cpm_appl/ ] #H
+ elim (tdeq_inv_pair … H) -H /2 width=1 by/
+ | #V2 #HV12 #HnV12
+ @or_intror @(ex2_2_intro … (ⓐV2.T1)) [1,2: /2 width=2 by cpr_pair_sn/ ] #H
+ elim (tdeq_inv_pair … H) -H /2 width=1 by/
+ ]
+ | @or_intror @(ex2_2_intro … T1) [1,2: /2 width=2 by cpm_eps/ ] #H
+ /2 width=4 by tdeq_inv_pair_xy_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 *)
+(* *)
+(**************************************************************************)
+
+include "basic_2/rt_computation/cpms_cnu.ma".
+include "basic_2/rt_computation/cpmue.ma".
+include "basic_2/dynamic/cnv_preserve.ma".
+
+(* T-UNBOUND EVALUATION FOR T-BOUND RT-TRANSITION ON TERMS ******************)
+
+(* Properties with evaluation for t-unbound rt-transition on terms **********)
+
+lemma cnv_cpmue_trans (a) (h) (G) (L):
+ ∀T1. ⦃G,L⦄ ⊢ T1 ![a,h] →
+ ∀T2,n. ⦃G,L⦄ ⊢ T1 ➡*[h,n] 𝐍*⦃T2⦄ → ⦃G,L⦄ ⊢ T2 ![a,h].
+/3 width=4 by cpmue_fwd_cpms, cnv_cpms_trans/ qed-.
+
+lemma cnv_cpmue_cpms_conf (a) (h) (G) (L):
+ ∀T0. ⦃G,L⦄ ⊢ T0 ![a,h] → ∀T1,n1. ⦃G,L⦄ ⊢ T0 ➡*[n1,h] T1 →
+ ∀T2,n2. ⦃G,L⦄ ⊢ T0 ➡*[h,n2] 𝐍*⦃T2⦄ →
+ ∃∃T. ⦃G,L⦄ ⊢ T1 ➡*[h,n2-n1] 𝐍*⦃T⦄ & T2 ≅ T.
+#a #h #G #L #T0 #HT0 #T1 #n1 #HT01 #T2 #n2 * #HT02 #HT2
+elim (cnv_cpms_conf … HT0 … HT01 … HT02) -T0 #T0 #HT10 #HT20
+lapply (cpms_inv_cnu_sn … HT20 HT2) -HT20 #HT20
+/4 width=8 by cpmue_intro, cnu_tueq_trans, ex2_intro/
+qed-.
+
+(* Main properties with evaluation for t-unbound rt-transition on terms *****)
+
+theorem cnv_cpmue_mono (a) (h) (G) (L):
+ ∀T0. ⦃G,L⦄ ⊢ T0 ![a,h] → ∀T1,n1. ⦃G,L⦄ ⊢ T0 ➡*[h,n1] 𝐍*⦃T1⦄ →
+ ∀T2,n2. ⦃G,L⦄ ⊢ T0 ➡*[h,n2] 𝐍*⦃T2⦄ → T1 ≅ T2.
+#a #h #G #L #T0 #HT0 #T1 #n1 * #HT01 #HT1 #T2 #n2 * #HT02 #HT2
+elim (cnv_cpms_conf … HT0 … HT01 … HT02) -T0 #T0 #HT10 #HT20
+/3 width=8 by cpms_inv_cnu_sn, tueq_canc_dx/
+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_computation/cpms_cnu.ma".
+include "basic_2/rt_computation/cpue.ma".
+include "basic_2/dynamic/cnv_preserve.ma".
+
+(* CONTEXT-SENSITIVE NATIVE VALIDITY FOR TERMS ******************************)
+
+(* Properties with evaluation for t-unbound rt-transition on terms **********)
+
+lemma cnv_cpue_trans (a) (h) (G) (L):
+ ∀T1. ⦃G,L⦄ ⊢ T1 ![a,h] →
+ ∀T2. ⦃G,L⦄ ⊢ T1 ⥲*[h] 𝐍⦃T2⦄ → ⦃G,L⦄ ⊢ T2 ![a,h].
+#a #h #G #L #T1 #HT1 #T2 * #n #HT12 #_
+/2 width=4 by cnv_cpms_trans/
+qed-.
+
+lemma cnv_cpue_cpms_conf (a) (h) (n) (G) (L):
+ ∀T0. ⦃G,L⦄ ⊢ T0 ![a,h] → ∀T1. ⦃G,L⦄ ⊢ T0 ➡*[n,h] T1 →
+ ∀T2. ⦃G,L⦄ ⊢ T0 ⥲*[h] 𝐍⦃T2⦄ →
+ ∃∃T. ⦃G,L⦄ ⊢ T1 ⥲*[h] 𝐍⦃T⦄ & T2 ≅ T.
+#a #h #n1 #G #L #T0 #HT0 #T1 #HT01 #T2 * #n2 #HT02 #HT2
+elim (cnv_cpms_conf … HT0 … HT01 … HT02) -T0 #T0 #HT10 #HT20
+lapply (cpms_inv_cnu_sn … HT20 HT2) -HT20 #HT20
+/4 width=8 by cnu_tueq_trans, ex2_intro/
+qed-.
+
+(* Main properties with evaluation for t-unbound rt-transition on terms *****)
+
+theorem cnv_cpue_mono (a) (h) (G) (L):
+ ∀T0. ⦃G,L⦄ ⊢ T0 ![a,h] → ∀T1. ⦃G,L⦄ ⊢ T0 ⥲*[h] 𝐍⦃T1⦄ →
+ ∀T2. ⦃G,L⦄ ⊢ T0 ⥲*[h] 𝐍⦃T2⦄ → T1 ≅ T2.
+#a #h #G #L #T0 #HT0 #T1 * #n1 #HT01 #HT1 #T2 * #n2 #HT02 #HT2
+elim (cnv_cpms_conf … HT0 … HT01 … HT02) -T0 #T0 #HT10 #HT20
+/3 width=8 by cpms_inv_cnu_sn, tueq_canc_dx/
+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_tueq.ma".
+include "basic_2/rt_transition/cpm.ma".
+
+(* T-BOUND CONTEXT-SENSITIVE PARALLEL RT-TRANSITION FOR TERMS ***************)
+
+(* Properties with tail sort-irrelevant equivalence on terms ****************)
+
+lemma cpm_tueq_conf (h) (n) (G) (L) (T0):
+ ∀T1. ⦃G,L⦄ ⊢ T0 ➡[n,h] T1 → ∀T2. T0 ≅ T2 →
+ ∃∃T. ⦃G,L⦄ ⊢ T2 ➡[n,h] T & T1 ≅ T.
+#h #n #G #L #T0 #T1 #H @(cpm_ind … H) -G -L -T0 -T1 -n
+[ /2 width=3 by ex2_intro/
+| #G #L #s0 #X2 #H2
+ elim (tueq_inv_sort1 … H2) -H2 #s2 #H destruct
+ /3 width=3 by tueq_sort, ex2_intro/
+| #n #G #K0 #V0 #V1 #W1 #_ #IH #HVW1 #X2 #H2
+ >(tueq_inv_lref1 … H2) -X2
+ elim (IH V0) [| // ] -IH #V #HV0 #HV1
+ elim (tueq_lifts_sn … HV1 … HVW1) -V1
+ /3 width=3 by cpm_delta, ex2_intro/
+| #n #G #K0 #V0 #V1 #W1 #_ #IH #HVW1 #X2 #H2
+ >(tueq_inv_lref1 … H2) -X2
+ elim (IH V0) [| // ] -IH #V #HV0 #HV1
+ elim (tueq_lifts_sn … HV1 … HVW1) -V1
+ /3 width=3 by cpm_ell, ex2_intro/
+| #n #I #G #K0 #V1 #W1 #i #_ #IH #HVW1 #X2 #H2
+ >(tueq_inv_lref1 … H2) -X2
+ elim (IH (#i)) [| // ] -IH #V #HV0 #HV1
+ elim (tueq_lifts_sn … HV1 … HVW1) -V1
+ /3 width=3 by cpm_lref, ex2_intro/
+| #n #p #I #G #L #V0 #V1 #T0 #T1 #HV01 #_ #_ #IHT #X2 #H2
+ elim (tueq_inv_bind1 … H2) -H2 #T2 #HT02 #H destruct
+ elim (IHT … HT02) -T0 #T #HT2 #HT1
+ /3 width=3 by cpm_bind, tueq_bind, ex2_intro/
+| #n #G #L #V0 #V1 #T0 #T1 #HV10 #_ #_ #IHT #X2 #H2
+ elim (tueq_inv_appl1 … H2) -H2 #T2 #HT02 #H destruct
+ elim (IHT … HT02) -T0 #T #HT2 #HT1
+ /3 width=3 by cpm_appl, tueq_appl, ex2_intro/
+| #n #G #L #V0 #V1 #T0 #T1 #_ #_ #IHV #IHT #X2 #H2
+ elim (tueq_inv_cast1 … H2) -H2 #V2 #T2 #HV02 #HT02 #H destruct
+ elim (IHV … HV02) -V0 #V #HV2 #HV1
+ elim (IHT … HT02) -T0 #T #HT2 #HT1
+ /3 width=5 by cpm_cast, tueq_cast, ex2_intro/
+| #n #G #L #V0 #U0 #T0 #T1 #HTU0 #_ #IH #X2 #H2
+ elim (tueq_inv_bind1 … H2) -H2 #U2 #HU02 #H destruct
+ elim (tueq_inv_lifts_sn … HU02 … HTU0) -U0 #T2 #HTU2 #HT02
+ elim (IH … HT02) -T0 #T #HT2 #HT1
+ /3 width=3 by cpm_zeta, ex2_intro/
+| #n #G #L #V0 #T0 #T1 #_ #IH #X2 #H2
+ elim (tueq_inv_cast1 … H2) -H2 #V2 #T2 #_ #HT02 #H destruct
+ elim (IH … HT02) -V0 -T0
+ /3 width=3 by cpm_eps, ex2_intro/
+| #n #G #L #V0 #T0 #T1 #_ #IH #X2 #H2
+ elim (tueq_inv_cast1 … H2) -H2 #V2 #T2 #HV02 #_ #H destruct
+ elim (IH … HV02) -V0 -T1
+ /3 width=3 by cpm_ee, ex2_intro/
+| #n #p #G #L #V0 #V1 #W0 #W1 #T0 #T1 #HV01 #HW01 #_ #_ #_ #IHT #X2 #H2
+ elim (tueq_inv_appl1 … H2) -H2 #X #H2 #H destruct
+ elim (tueq_inv_bind1 … H2) -H2 #T2 #HT02 #H destruct
+ elim (IHT … HT02) -T0
+ /4 width=3 by cpm_beta, tueq_cast, tueq_bind, ex2_intro/
+| #n #p #G #L #V0 #V1 #U1 #W0 #W1 #T0 #T1 #HV01 #HW01 #_ #_ #_ #IHT #HVU1 #X2 #H2
+ elim (tueq_inv_appl1 … H2) -H2 #X #H2 #H destruct
+ elim (tueq_inv_bind1 … H2) -H2 #T2 #HT02 #H destruct
+ elim (IHT … HT02) -T0 #T #HT2 #HT1
+ /4 width=3 by cpm_theta, tueq_appl, tueq_bind, ex2_intro/
+]
+qed-.
+
+lemma tueq_cpm_trans (h) (n) (G) (L) (T0):
+ ∀T1. T1 ≅ T0 → ∀T2. ⦃G,L⦄ ⊢ T0 ➡[n,h] T2 →
+ ∃∃T. ⦃G,L⦄ ⊢ T1 ➡[n,h] T & T ≅ T2.
+#h #n #G #L #T0 #T1 #HT10 #T2 #HT02
+elim (cpm_tueq_conf … HT02 T1)
+/3 width=3 by tueq_sym, 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/cnu_cnu.ma".
+include "basic_2/rt_computation/cpms.ma".
+
+(* T-BOUND CONTEXT-SENSITIVE PARALLEL RT-COMPUTATION FOR TERMS **************)
+
+(* Inversion lemmas with normal terms for t-unbound rt-transition ***********)
+
+lemma cpms_inv_cnu_sn (h) (n) (G) (L):
+ ∀T1,T2. ⦃G,L⦄ ⊢ T1 ➡*[n,h] T2 → ⦃G,L⦄ ⊢ ⥲[h] 𝐍⦃T1⦄ → T1 ≅ T2.
+#h #n #G #L #T1 #T2 #H @(cpms_ind_sn … H) -T1 //
+#n1 #n2 #T1 #T0 #HT10 #_ #IH #HT1
+/5 width=8 by cnu_tueq_trans, tueq_trans/
+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/notation/relations/predevalstar_6.ma".
+include "basic_2/rt_transition/cnu.ma".
+include "basic_2/rt_computation/cpms.ma".
+
+(* T-UNBOUND EVALUATION FOR T-BOUND RT-TRANSITION ON TERMS ******************)
+
+definition cpmue (h) (n) (G) (L): relation2 term term ≝
+ λT1,T2. ∧∧ ⦃G,L⦄ ⊢ T1 ➡*[n,h] T2 & ⦃G,L⦄ ⊢ ⥲[h] 𝐍⦃T2⦄.
+
+interpretation "t-unbound evaluation for t-bound context-sensitive parallel rt-transition (term)"
+ 'PRedEvalStar h n G L T1 T2 = (cpmue h n G L T1 T2).
+
+definition R_cpmue (h) (G) (L) (T): predicate nat ≝
+ λn. ∃U. ⦃G,L⦄ ⊢ T ➡*[h,n] 𝐍*⦃U⦄.
+
+(* Basic properties *********************************************************)
+
+lemma cpmue_intro (h) (n) (G) (L):
+ ∀T1,T2. ⦃G,L⦄ ⊢ T1 ➡*[n,h] T2 → ⦃G,L⦄ ⊢ ⥲[h] 𝐍⦃T2⦄ → ⦃G,L⦄ ⊢ T1 ➡*[h,n] 𝐍*⦃T2⦄.
+/2 width=1 by conj/ qed.
+
+(* Basic forward lemmas *****************************************************)
+
+lemma cpmue_fwd_cpms (h) (n) (G) (L):
+ ∀T1,T2. ⦃G,L⦄ ⊢ T1 ➡*[h,n] 𝐍*⦃T2⦄ → ⦃G,L⦄ ⊢ T1 ➡*[n,h] T2.
+#h #n #G #L #T1 #T2 * #HT12 #_ //
+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_cpx.ma".
+include "basic_2/rt_transition/cnu_tdeq.ma".
+include "basic_2/rt_computation/csx.ma".
+include "basic_2/rt_computation/cpmue.ma".
+
+(* T-UNBOUND EVALUATION FOR T-BOUND RT-TRANSITION ON TERMS ******************)
+
+(* Properties with strong normalization for unbound rt-transition for terms *)
+
+lemma cpmue_total_csx (h) (G) (L):
+ ∀T1. ⦃G,L⦄ ⊢ ⬈*[h] 𝐒⦃T1⦄ → ∃∃T2,n. ⦃G,L⦄ ⊢ T1 ➡*[h,n] 𝐍*⦃T2⦄.
+#h #G #L #T1 #H
+@(csx_ind … H) -T1 #T1 #_ #IHT1
+elim (cnu_dec_tdeq h G L T1)
+[ -IHT1 #HT1 /3 width=4 by cpmue_intro, ex1_2_intro/
+| * #n1 #T0 #HT10 #HnT10
+ elim (IHT1 … HnT10) -IHT1 -HnT10 [| /2 width=2 by cpm_fwd_cpx/ ]
+ #T2 #n2 * #HT02 #HT2 /4 width=5 by cpms_step_sn, cpmue_intro, ex1_2_intro/
+]
+qed-.
+
+lemma R_cpmue_total_csx (h) (G) (L):
+ ∀T1. ⦃G,L⦄ ⊢ ⬈*[h] 𝐒⦃T1⦄ → ∃n. R_cpmue h G L T1 n.
+#h #G #L #T1 #H
+elim (cpmue_total_csx … H) -H #T2 #n #HT12
+/3 width=3 by ex_intro (* 2x *)/
+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/notation/relations/prediteval_5.ma".
+include "basic_2/rt_transition/cnu.ma".
+include "basic_2/rt_computation/cpms.ma".
+
+(* EVALUATION FOR T-UNBOUND RT-TRANSITION ON TERMS **************************)
+
+definition cpue (h) (G) (L): relation2 term term ≝
+ λT1,T2. ∃∃n. ⦃G,L⦄ ⊢ T1 ➡*[n,h] T2 & ⦃G,L⦄ ⊢ ⥲[h] 𝐍⦃T2⦄.
+
+interpretation "evaluation for t-unbound context-sensitive parallel rt-transition (term)"
+ 'PRedITEval h G L T1 T2 = (cpue h G 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/cpm_cpx.ma".
+include "basic_2/rt_transition/cnu_tdeq.ma".
+include "basic_2/rt_computation/csx.ma".
+include "basic_2/rt_computation/cpue.ma".
+
+(* EVALUATION FOR T-UNBOUND RT-TRANSITION ON TERMS **************************)
+
+(* Properties with strong normalization for unbound rt-transition for terms *)
+
+lemma cpue_total_csx (h) (G) (L):
+ ∀T1. ⦃G,L⦄ ⊢ ⬈*[h] 𝐒⦃T1⦄ → ∃T2. ⦃G,L⦄ ⊢ T1 ⥲*[h] 𝐍⦃T2⦄.
+#h #G #L #T1 #H
+@(csx_ind … H) -T1 #T1 #_ #IHT1
+elim (cnu_dec_tdeq h G L T1) [ /3 width=4 by ex2_intro, ex_intro/ ] *
+#n1 #T0 #HT10 #HnT10
+elim (IHT1 … HnT10) -IHT1 -HnT10 [| /2 width=2 by cpm_fwd_cpx/ ]
+#T2 * #n2 #HT02 #HT2 /4 width=7 by cpms_step_sn, ex2_intro, 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 *)
+(* *)
+(**************************************************************************)
+
+(* NOTATION FOR THE FORMAL SYSTEM λδ ****************************************)
+
+notation "hvbox( ⦃ term 46 G, break term 46 L ⦄ ⊢ break term 46 T1 ⥲* [ break term 46 h ] 𝐍 ⦃ break term 46 T2 ⦄ )"
+ non associative with precedence 45
+ for @{ 'PRedITEval $h $G $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 h, break term 46 n ] 𝐍 *⦃ break term 46 T2 ⦄ )"
+ non associative with precedence 45
+ for @{ 'PRedEvalStar $h $n $G $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 h ] 𝐍 ⦃ break term 46 T2 ⦄ )"
- non associative with precedence 45
- for @{ 'PRedITEval $h $G $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/notation/relations/predevalstar_6.ma".
+include "basic_2/rt_transition/cnh.ma".
+include "basic_2/rt_computation/cpms.ma".
+
+(* HEAD T-UNBOUND EVALUATION FOR T-BOUND RT-TRANSITION ON TERMS *************)
+
+definition cpmhe (h) (n) (G) (L): relation2 term term ≝
+ λT1,T2. ∧∧ ⦃G,L⦄ ⊢ T1 ➡*[n,h] T2 & ⦃G,L⦄ ⊢ ⥲[h] 𝐍⦃T2⦄.
+
+interpretation "t-unbound evaluation for t-bound context-sensitive parallel rt-transition (term)"
+ 'PRedEvalStar h n G L T1 T2 = (cpmhe h n G L T1 T2).
+
+definition R_cpmhe (h) (G) (L) (T): predicate nat ≝
+ λn. ∃U. ⦃G,L⦄ ⊢ T ➡*[h,n] 𝐍*⦃U⦄.
+
+(* Basic properties *********************************************************)
+
+lemma cpmhe_intro (h) (n) (G) (L):
+ ∀T1,T2. ⦃G,L⦄ ⊢ T1 ➡*[n,h] T2 → ⦃G,L⦄ ⊢ ⥲[h] 𝐍⦃T2⦄ → ⦃G,L⦄ ⊢ T1 ➡*[h,n] 𝐍*⦃T2⦄.
+/2 width=1 by conj/ qed.
+
+(* Advanced properties ******************************************************)
+
+lemma cpmhe_sort (h) (n) (G) (L) (T):
+ ∀s. ⦃G,L⦄ ⊢ T ➡*[n,h] ⋆s → ⦃G,L⦄ ⊢ T ➡*[h,n] 𝐍*⦃⋆s⦄.
+/3 width=5 by cnh_sort, cpmhe_intro/ qed.
+
+lemma cpmhe_ctop (h) (n) (G) (T):
+ ∀i. ⦃G,⋆⦄ ⊢ T ➡*[n,h] #i → ⦃G,⋆⦄ ⊢ T ➡*[h,n] 𝐍*⦃#i⦄.
+/3 width=5 by cnh_ctop, cpmhe_intro/ qed.
+
+lemma cpmhe_zero (h) (n) (G) (L) (T):
+ ∀I. ⦃G,L.ⓤ{I}⦄ ⊢ T ➡*[n,h] #0 → ⦃G,L.ⓤ{I}⦄ ⊢ T ➡*[h,n] 𝐍*⦃#0⦄.
+/3 width=6 by cnh_zero, cpmhe_intro/ qed.
+
+lemma cpmhe_gref (h) (n) (G) (L) (T):
+ ∀l. ⦃G,L⦄ ⊢ T ➡*[n,h] §l → ⦃G,L⦄ ⊢ T ➡*[h,n] 𝐍*⦃§l⦄.
+/3 width=5 by cnh_gref, cpmhe_intro/ qed.
+
+lemma cpmhe_abst (h) (n) (p) (G) (L) (T):
+ ∀W,U. ⦃G,L⦄ ⊢ T ➡*[n,h] ⓛ{p}W.U → ⦃G,L⦄ ⊢ T ➡*[h,n] 𝐍*⦃ⓛ{p}W.U⦄.
+/3 width=5 by cnh_abst, cpmhe_intro/ qed.
+
+lemma cpmhe_abbr_neg (h) (n) (G) (L) (T):
+ ∀V,U. ⦃G,L⦄ ⊢ T ➡*[n,h] -ⓓV.U → ⦃G,L⦄ ⊢ T ➡*[h,n] 𝐍*⦃-ⓓV.U⦄.
+/3 width=5 by cnh_abbr_neg, cpmhe_intro/ qed.
+
+(* Basic forward lemmas *****************************************************)
+
+lemma cpmhe_fwd_cpms (h) (n) (G) (L):
+ ∀T1,T2. ⦃G,L⦄ ⊢ T1 ➡*[h,n] 𝐍*⦃T2⦄ → ⦃G,L⦄ ⊢ T1 ➡*[n,h] T2.
+#h #n #G #L #T1 #T2 * #HT12 #_ //
+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_cpx.ma".
+include "basic_2/rt_transition/cnh_tdeq.ma".
+include "basic_2/rt_computation/csx.ma".
+include "basic_2/rt_computation/cpmhe.ma".
+
+(* HEAD T-UNBOUND EVALUATION FOR T-BOUND RT-TRANSITION ON TERMS *************)
+
+(* Properties with strong normalization for unbound rt-transition for terms *)
+
+lemma cpmhe_total_csx (h) (G) (L):
+ ∀T1. ⦃G,L⦄ ⊢ ⬈*[h] 𝐒⦃T1⦄ → ∃∃T2,n. ⦃G,L⦄ ⊢ T1 ➡*[h,n] 𝐍*⦃T2⦄.
+#h #G #L #T1 #H
+@(csx_ind … H) -T1 #T1 #_ #IHT1
+elim (cnh_dec_tdeq h G L T1)
+[ -IHT1 #HT1 /3 width=4 by cpmhe_intro, ex1_2_intro/
+| * #n1 #T0 #HT10 #HnT10
+ elim (IHT1 … HnT10) -IHT1 -HnT10 [| /2 width=2 by cpm_fwd_cpx/ ]
+ #T2 #n2 * #HT02 #HT2 /4 width=5 by cpms_step_sn, cpmhe_intro, ex1_2_intro/
+]
+qed-.
+
+lemma R_cpmhe_total_csx (h) (G) (L):
+ ∀T1. ⦃G,L⦄ ⊢ ⬈*[h] 𝐒⦃T1⦄ → ∃n. R_cpmhe h G L T1 n.
+#h #G #L #T1 #H
+elim (cpmhe_total_csx … H) -H #T2 #n #HT12
+/3 width=3 by ex_intro (* 2x *)/
+qed-.
include "basic_2/rt_transition/cpm_aaa.ma".
include "basic_2/rt_computation/cpxs_aaa.ma".
include "basic_2/rt_computation/cpms_cpxs.ma".
+include "basic_2/rt_computation/lprs_cpms.ma".
(* T-BOUND CONTEXT-SENSITIVE PARALLEL RT-COMPUTATION FOR TERMS **************)
(* Basic_2A1: uses: scpds_aaa_conf *)
(* Basic_2A1: includes: cprs_aaa_conf *)
-lemma cpms_aaa_conf (n) (h): ∀G,L. Conf3 … (aaa G L) (cpms h G L n).
+lemma cpms_aaa_conf (h) (G) (L) (n): Conf3 … (aaa G L) (cpms h G L n).
/3 width=5 by cpms_fwd_cpxs, cpxs_aaa_conf/ qed-.
lemma cpms_total_aaa (h) (G) (L) (n) (A):
/3 width=4 by cpms_step_dx, ex_intro/
]
qed-.
+
+lemma cpms_abst_dx_le_aaa (h) (G) (L) (T) (W) (p):
+ ∀A. ⦃G,L⦄ ⊢ T ⁝ A →
+ ∀n1,U1. ⦃G,L⦄ ⊢ T ➡*[n1,h] ⓛ{p}W.U1 → ∀n2. n1 ≤ n2 →
+ ∃∃U2. ⦃G,L⦄ ⊢ T ➡*[n2,h] ⓛ{p}W.U2 & ⦃G,L.ⓛW⦄ ⊢ U1 ➡*[n2-n1,h] U2.
+#h #G #L #T #W #p #A #HA #n1 #U1 #HTU1 #n2 #Hn12
+lapply (cpms_aaa_conf … HA … HTU1) -HA #HA
+elim (cpms_total_aaa h … (n2-n1) … HA) -HA #X #H
+elim (cpms_inv_abst_sn … H) -H #W0 #U2 #_ #HU12 #H destruct -W0
+>(plus_minus_m_m_commutative … Hn12) in ⊢ (??%?); -Hn12
+/4 width=5 by cpms_trans, cpms_bind_dx, 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 "static_2/syntax/theq_theq.ma".
+include "basic_2/rt_transition/cnh_cnh.ma".
+include "basic_2/rt_computation/cpms.ma".
+
+(* T-BOUND CONTEXT-SENSITIVE PARALLEL RT-COMPUTATION FOR TERMS **************)
+
+(* Inversion lemmas with normal terms for head t-unbound rt-transition ******)
+
+lemma cpms_inv_cnh_sn (h) (n) (G) (L):
+ ∀T1,T2. ⦃G,L⦄ ⊢ T1 ➡*[n,h] T2 → ⦃G,L⦄ ⊢ ⥲[h] 𝐍⦃T1⦄ → T1 ⩳ T2.
+#h #n #G #L #T1 #T2 #H @(cpms_ind_sn … H) -T1 //
+#n1 #n2 #T1 #T0 #HT10 #_ #IH #HT1
+/4 width=9 by cnh_cpm_trans, theq_trans/
+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/cnu_cnu.ma".
-include "basic_2/rt_computation/cpms.ma".
-
-(* T-BOUND CONTEXT-SENSITIVE PARALLEL RT-COMPUTATION FOR TERMS **************)
-
-(* Inversion lemmas with normal terms for t-unbound rt-transition ***********)
-
-lemma cpms_inv_cnu_sn (h) (n) (G) (L):
- ∀T1,T2. ⦃G,L⦄ ⊢ T1 ➡*[n,h] T2 → ⦃G,L⦄ ⊢ ⥲[h] 𝐍⦃T1⦄ → T1 ≅ T2.
-#h #n #G #L #T1 #T2 #H @(cpms_ind_sn … H) -T1 //
-#n1 #n2 #T1 #T0 #HT10 #_ #IH #HT1
-/5 width=8 by cnu_tueq_trans, tueq_trans/
-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/notation/relations/prediteval_5.ma".
-include "basic_2/rt_transition/cnu.ma".
-include "basic_2/rt_computation/cpms.ma".
-
-(* EVALUATION FOR T-UNBOUND RT-TRANSITION ON TERMS **************************)
-
-definition cpue (h) (G) (L): relation2 term term ≝
- λT1,T2. ∃∃n. ⦃G,L⦄ ⊢ T1 ➡*[n,h] T2 & ⦃G,L⦄ ⊢ ⥲[h] 𝐍⦃T2⦄.
-
-interpretation "evaluation for t-unbound context-sensitive parallel rt-transition (term)"
- 'PRedITEval h G L T1 T2 = (cpue h G 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/cpm_cpx.ma".
-include "basic_2/rt_transition/cnu_tdeq.ma".
-include "basic_2/rt_computation/csx.ma".
-include "basic_2/rt_computation/cpue.ma".
-
-(* EVALUATION FOR T-UNBOUND RT-TRANSITION ON TERMS **************************)
-
-(* Properties with strong normalization for unbound rt-transition for terms *)
-
-lemma cpue_total_csx (h) (G) (L):
- ∀T1. ⦃G,L⦄ ⊢ ⬈*[h] 𝐒⦃T1⦄ → ∃T2. ⦃G,L⦄ ⊢ T1 ⥲*[h] 𝐍⦃T2⦄.
-#h #G #L #T1 #H
-@(csx_ind … H) -T1 #T1 #_ #IHT1
-elim (cnu_dec_tdeq h G L T1) [ /3 width=4 by ex2_intro, ex_intro/ ] *
-#n1 #T0 #HT10 #HnT10
-elim (IHT1 … HnT10) -IHT1 -HnT10 [| /2 width=2 by cpm_fwd_cpx/ ]
-#T2 * #n2 #HT02 #HT2 /4 width=7 by cpms_step_sn, ex2_intro, 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/rt_computation/lprs_cpms.ma".
+include "basic_2/rt_equivalence/cpes_cpms.ma".
+
+(* T-BOUND CONTEXT-SENSITIVE PARALLEL RT-EQUIVALENCE FOR TERMS **************)
+
+(* Advanced forward lemmas **************************************************)
+
+lemma cpes_fwd_abst_bi (h) (n1) (n2) (p1) (p2) (G) (L):
+ ∀W1,W2,T1,T2. ⦃G,L⦄ ⊢ ⓛ{p1}W1.T1 ⬌*[h,n1,n2] ⓛ{p2}W2.T2 →
+ ∧∧ p1 = p2 & ⦃G,L⦄ ⊢ W1 ⬌*[h,0,O] W2.
+#h #n1 #n2 #p1 #p2 #G #L #W1 #W2 #T1 #T2 * #X #H1 #H2
+elim (cpms_inv_abst_sn … H1) #W0 #X0 #HW10 #_ #H destruct
+elim (cpms_inv_abst_bi … H2) #H #HW20 #_ destruct
+/3 width=3 by cpms_div, conj/
+qed-.
+
+(* Main properties **********************************************************)
+
+theorem cpes_cpes_trans (h) (n1) (n2) (G) (L) (T):
+ ∀T1. ⦃G,L⦄ ⊢ T ⬌*[h,n1,0] T1 →
+ ∀T2. ⦃G,L⦄ ⊢ T1 ⬌*[h,0,n2] T2 → ⦃G,L⦄ ⊢ T ⬌*[h,n1,n2] T2.
+#h #n1 #n2 #G #L #T #T1 #HT1 #T2 * #X #HX1 #HX2
+lapply (cpes_cprs_trans … HT1 … HX1) -T1 #HTX
+lapply (cpes_cpms_div … HTX … HX2) -X //
+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_computation/cprs_cprs.ma".
+include "basic_2/rt_equivalence/cpes.ma".
+
+(* T-BOUND CONTEXT-SENSITIVE PARALLEL RT-EQUIVALENCE FOR TERMS **************)
+
+(* Properties with t-bound rt-computation on terms **************************)
+
+lemma cpes_cprs_trans (h) (n) (G) (L) (T0):
+ ∀T1. ⦃G,L⦄ ⊢ T1 ⬌*[h,n,0] T0 →
+ ∀T2. ⦃G,L⦄ ⊢ T0 ➡*[h] T2 → ⦃G,L⦄ ⊢ T1 ⬌*[h,n,0] T2.
+#h #n #G #L #T0 #T1 * #T #HT1 #HT0 #T2 #HT02
+elim (cprs_conf … HT0 … HT02) -T0 #T0 #HT0 #HT20
+/3 width=3 by cpms_div, cpms_cprs_trans/
+qed-.
+
+lemma cpes_cpms_div (h) (n) (n1) (n2) (G) (L) (T0):
+ ∀T1. ⦃G,L⦄ ⊢ T1 ⬌*[h,n,n1] T0 →
+ ∀T2. ⦃G,L⦄ ⊢ T2 ➡*[n2,h] T0 → ⦃G,L⦄ ⊢ T1 ⬌*[h,n,n2+n1] T2.
+#h #n #n1 #n2 #G #L #T0 #T1 * #T #HT1 #HT0 #T2 #HT20
+lapply (cpms_trans … HT20 … HT0) -T0 #HT2
+/2 width=3 by cpms_div/
+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_computation/cprs_cprs.ma".
-include "basic_2/rt_equivalence/cpes.ma".
-
-(* T-BOUND CONTEXT-SENSITIVE PARALLEL RT-EQUIVALENCE FOR TERMS **************)
-
-(* Properties with context-sensitive parallel r-computation on terms ********)
-
-lemma cpes_cprs_trans (h) (n) (G) (L) (T0):
- ∀T1. ⦃G,L⦄ ⊢ T1 ⬌*[h,n,0] T0 →
- ∀T2. ⦃G,L⦄ ⊢ T0 ➡*[h] T2 → ⦃G,L⦄ ⊢ T1 ⬌*[h,n,0] T2.
-#h #n #G #L #T0 #T1 * #T #HT1 #HT0 #T2 #HT02
-elim (cprs_conf … HT0 … HT02) -T0 #T0 #HT0 #HT20
-/3 width=3 by cpms_div, cpms_cprs_trans/
-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/notation/relations/preditnormal_4.ma".
+include "static_2/syntax/theq.ma".
+include "basic_2/rt_transition/cpm.ma".
+
+(* NORMAL TERMS FOR HEAD T-UNUNBOUND RT-TRANSITION **************************)
+
+definition cnh (h) (G) (L): predicate term ≝
+ λT1. ∀n,T2. ⦃G,L⦄ ⊢ T1 ➡[n,h] T2 → T1 ⩳ T2.
+
+interpretation
+ "normality for head t-unbound context-sensitive parallel rt-transition (term)"
+ 'PRedITNormal h G L T = (cnh h G L T).
+
+(* Basic properties *********************************************************)
+
+lemma cnh_sort (h) (G) (L): ∀s. ⦃G,L⦄ ⊢ ⥲[h] 𝐍⦃⋆s⦄.
+#h #G #L #s1 #n #X #H
+elim (cpm_inv_sort1 … H) -H #H #_ destruct //
+qed.
+
+lemma cnh_ctop (h) (G): ∀i. ⦃G,⋆⦄ ⊢ ⥲[h] 𝐍⦃#i⦄.
+#h #G * [| #i ] #n #X #H
+[ elim (cpm_inv_zero1 … H) -H *
+ [ #H #_ destruct //
+ | #Y #X1 #X2 #_ #_ #H destruct
+ | #m #Y #X1 #X2 #_ #_ #H destruct
+ ]
+| elim (cpm_inv_lref1 … H) -H *
+ [ #H #_ destruct //
+ | #Z #Y #X0 #_ #_ #H destruct
+ ]
+]
+qed.
+
+lemma cnh_zero (h) (G) (L): ∀I. ⦃G,L.ⓤ{I}⦄ ⊢ ⥲[h] 𝐍⦃#0⦄.
+#h #G #L #I #n #X #H
+elim (cpm_inv_zero1 … H) -H *
+[ #H #_ destruct //
+| #Y #X1 #X2 #_ #_ #H destruct
+| #m #Y #X1 #X2 #_ #_ #H destruct
+]
+qed.
+
+lemma cnh_gref (h) (G) (L): ∀l. ⦃G,L⦄ ⊢ ⥲[h] 𝐍⦃§l⦄.
+#h #G #L #l1 #n #X #H
+elim (cpm_inv_gref1 … H) -H #H #_ destruct //
+qed.
+
+lemma cnh_abst (h) (p) (G) (L): ∀W,T. ⦃G,L⦄ ⊢ ⥲[h] 𝐍⦃ⓛ{p}W.T⦄.
+#h #p #G #L #W1 #T1 #n #X #H
+elim (cpm_inv_abst1 … H) -H #W2 #T2 #_ #_ #H destruct
+/1 width=1 by theq_pair/
+qed.
+
+lemma cnh_abbr_neg (h) (G) (L): ∀V,T. ⦃G,L⦄ ⊢ ⥲[h] 𝐍⦃-ⓓV.T⦄.
+#h #G #L #V1 #T1 #n #X #H
+elim (cpm_inv_abbr1 … H) -H *
+[ #W2 #T2 #_ #_ #H destruct /1 width=1 by theq_pair/
+| #X1 #_ #_ #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 "basic_2/rt_transition/cpm.ma".
+include "basic_2/rt_transition/cnh.ma".
+
+(* NORMAL TERMS FOR HEAD T-UNUNBOUND RT-TRANSITION **************************)
+
+(* Advanced properties ******************************************************)
+
+axiom cnh_cpm_trans (h) (n) (G) (L):
+ ∀T1,T2. ⦃G,L⦄ ⊢ T1 ➡[n,h] T2 → ⦃G,L⦄ ⊢ ⥲[h] 𝐍⦃T1⦄ → ⦃G,L⦄ ⊢ ⥲[h] 𝐍⦃T2⦄.
+(*
+#h #n #G #L #T1 #T2 #HT1 #n #T2 #HT12 #k #X #HX
+*)
--- /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_theq.ma".
+include "basic_2/rt_transition/cpm_drops.ma".
+include "basic_2/rt_transition/cnh.ma".
+
+(* NORMAL TERMS FOR HEAD T-UNUNBOUND RT-TRANSITION **************************)
+
+(* Advanced properties ******************************************************)
+
+lemma cnh_atom_drops (h) (b) (G) (L):
+ ∀i. ⬇*[b,𝐔❴i❵] L ≘ ⋆ → ⦃G,L⦄ ⊢ ⥲[h] 𝐍⦃#i⦄.
+#h #b #G #L #i #Hi #n #X #H
+elim (cpm_inv_lref1_drops … H) -H * [ // || #m ] #K #V1 #V2 #HLK
+lapply (drops_gen b … HLK) -HLK #HLK
+lapply (drops_mono … Hi … HLK) -L #H destruct
+qed.
+
+lemma cnh_unit_drops (h) (I) (G) (L):
+ ∀K,i. ⬇*[i] L ≘ K.ⓤ{I} → ⦃G,L⦄ ⊢ ⥲[h] 𝐍⦃#i⦄.
+#h #I #G #L #K #i #HLK #n #X #H
+elim (cpm_inv_lref1_drops … H) -H * [ // || #m ] #Y #V1 #V2 #HLY
+lapply (drops_mono … HLK … HLY) -L #H destruct
+qed.
+
+(* Properties with generic relocation ***************************************)
+
+lemma cnh_lifts (h) (G): d_liftable1 … (cnh h G).
+#h #G #K #T #HT #b #f #L #HLK #U #HTU #n #U0 #H
+elim (cpm_inv_lifts_sn … H … HLK … HTU) -b -L #T0 #HTU0 #HT0
+lapply (HT … HT0) -G -K /2 width=6 by theq_lifts_bi/
+qed-.
+
+(* Inversion lemmas with generic relocation *********************************)
+
+lemma cnh_inv_lifts (h) (G): d_deliftable1 … (cnh h G).
+#h #G #L #U #HU #b #f #K #HLK #T #HTU #n #T0 #H
+elim (cpm_lifts_sn … H … HLK … HTU) -b -K #U0 #HTU0 #HU0
+lapply (HU … HU0) -G -L /2 width=6 by theq_inv_lifts_bi/
+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.ma".
+include "basic_2/rt_transition/cnh.ma".
+
+(* NORMAL TERMS FOR HEAD T-UNUNBOUND RT-TRANSITION **************************)
+
+(* Advanced properties with uniform relocation for terms ********************)
+
+lemma cnh_lref (h) (I) (G) (L):
+ ∀i. ⦃G,L⦄ ⊢ ⥲[h] 𝐍⦃#i⦄ → ⦃G,L.ⓘ{I}⦄ ⊢ ⥲[h] 𝐍⦃#↑i⦄.
+#h #I #G #L #i #Hi #n #X #H
+elim (cpm_inv_lref1 … H) -H *
+[ #H #_ destruct //
+| #J #K #V #HV #HVX #H destruct
+ lapply (Hi … HV) -Hi -HV #HV
+ lapply (theq_inv_lref1 … HV) -HV #H destruct
+ lapply (lifts_inv_lref1_uni … HVX) -HVX #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 "basic_2/rt_transition/cpm_simple.ma".
+include "basic_2/rt_transition/cnh.ma".
+
+(* NORMAL TERMS HEAD FOR T-UNUNBOUND RT-TRANSITION **************************)
+
+(* Advanced properties with simple terms ************************************)
+
+lemma cnh_appl_simple (h) (G) (L): ∀V,T. 𝐒⦃T⦄ → ⦃G,L⦄ ⊢ ⥲[h] 𝐍⦃ⓐV.T⦄.
+#h #G #L #V1 #T1 #HT1 #n #X #H
+elim (cpm_inv_appl1_simple … H HT1) -H -HT1 #V2 #T2 #_ #_ #H destruct
+/1 width=1 by theq_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 "basic_2/rt_transition/cpr_tdeq.ma".
+include "basic_2/rt_transition/cnh_simple.ma".
+include "basic_2/rt_transition/cnh_drops.ma".
+
+(* NORMAL TERMS FOR HEAD T-UNUNBOUND RT-TRANSITION **************************)
+
+(* Properties with context-free sort-irrelevant equivalence for terms *******)
+
+lemma cnh_dec_tdeq (h) (G) (L):
+ ∀T1. ∨∨ ⦃G,L⦄ ⊢ ⥲[h] 𝐍⦃T1⦄
+ | ∃∃n,T2. ⦃G,L⦄ ⊢ T1 ➡[n,h] T2 & (T1 ≛ T2 → ⊥).
+#h #G #L * *
+[ #s /3 width=5 by cnh_sort, or_introl/
+| #i elim (drops_F_uni L i)
+ [ /3 width=7 by cnh_atom_drops, or_introl/
+ | * * [ #I | * #V ] #K #HLK
+ [ /3 width=8 by cnh_unit_drops, or_introl/
+ | elim (lifts_total V 𝐔❴↑i❵) #W #HVW
+ @or_intror @(ex2_2_intro … W) [1,2: /2 width=7 by cpm_delta_drops/ ] #H
+ lapply (tdeq_inv_lref1 … H) -H #H destruct
+ /2 width=5 by lifts_inv_lref2_uni_lt/
+ | elim (lifts_total V 𝐔❴↑i❵) #W #HVW
+ @or_intror @(ex2_2_intro … W) [1,2: /2 width=7 by cpm_ell_drops/ ] #H
+ lapply (tdeq_inv_lref1 … H) -H #H destruct
+ /2 width=5 by lifts_inv_lref2_uni_lt/
+ ]
+ ]
+| #l /3 width=5 by cnh_gref, or_introl/
+| #p * [ cases p ] #V1 #T1
+ [ elim (cpr_subst h G (L.ⓓV1) T1 0 L V1) [| /2 width=1 by drops_refl/ ] #T2 #X2 #HT12 #HXT2
+ elim (tdeq_dec T1 T2) [ -HT12 #HT12 | #HnT12 ]
+ [ elim (tdeq_inv_lifts_dx … HT12 … HXT2) -T2 #X1 #HXT1 #_ -X2
+ @or_intror @(ex2_2_intro … X1) [1,2: /2 width=4 by cpm_zeta/ ] #H
+ /2 width=7 by tdeq_lifts_inv_pair_sn/
+ | @or_intror @(ex2_2_intro … (+ⓓV1.T2)) [1,2: /2 width=2 by cpm_bind/ ] #H
+ elim (tdeq_inv_pair … H) -H /2 width=1 by/
+ ]
+ | /3 width=5 by cnh_abbr_neg, or_introl/
+ | /3 width=5 by cnh_abst, or_introl/
+ ]
+| * #V1 #T1
+ [ elim (simple_dec_ex T1) [ #HT1 | * #p * #W1 #U1 #H destruct ]
+ [ /3 width=5 by cnh_appl_simple, or_introl/
+ | elim (lifts_total V1 𝐔❴1❵) #X1 #HVX1
+ @or_intror @(ex2_2_intro … (ⓓ{p}W1.ⓐX1.U1)) [1,2: /2 width=3 by cpm_theta/ ] #H
+ elim (tdeq_inv_pair … H) -H #H destruct
+ | @or_intror @(ex2_2_intro … (ⓓ{p}ⓝW1.V1.U1)) [1,2: /2 width=2 by cpm_beta/ ] #H
+ elim (tdeq_inv_pair … H) -H #H destruct
+ ]
+ | @or_intror @(ex2_2_intro … T1) [1,2: /2 width=2 by cpm_eps/ ] #H
+ /2 width=4 by tdeq_inv_pair_xy_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 *)
-(* *)
-(**************************************************************************)
-
-include "basic_2/notation/relations/preditnormal_4.ma".
-include "static_2/syntax/tueq.ma".
-include "basic_2/rt_transition/cpm.ma".
-
-(* NORMAL TERMS FOR T-UNUNBOUND RT-TRANSITION *******************************)
-
-definition cnu (h) (G) (L): predicate term ≝
- λT1. ∀n,T2. ⦃G,L⦄ ⊢ T1 ➡[n,h] T2 → T1 ≅ T2.
-
-interpretation
- "normality for t-unbound context-sensitive parallel rt-transition (term)"
- 'PRedITNormal h G L T = (cnu h G L T).
-
-(* Basic properties *********************************************************)
-
-lemma cnu_sort (h) (G) (L): ∀s. ⦃G,L⦄ ⊢ ⥲[h] 𝐍⦃⋆s⦄.
-#h #G #L #s1 #n #X #H
-elim (cpm_inv_sort1 … H) -H #H #_ destruct //
-qed.
-
-lemma cnu_ctop (h) (G): ∀i. ⦃G,⋆⦄ ⊢ ⥲[h] 𝐍⦃#i⦄.
-#h #G * [| #i ] #n #X #H
-[ elim (cpm_inv_zero1 … H) -H *
- [ #H #_ destruct //
- | #Y #X1 #X2 #_ #_ #H destruct
- | #m #Y #X1 #X2 #_ #_ #H destruct
- ]
-| elim (cpm_inv_lref1 … H) -H *
- [ #H #_ destruct //
- | #Z #Y #X0 #_ #_ #H destruct
- ]
-]
-qed.
-
-lemma cnu_zero (h) (G) (L): ∀I. ⦃G,L.ⓤ{I}⦄ ⊢ ⥲[h] 𝐍⦃#0⦄.
-#h #G #L #I #n #X #H
-elim (cpm_inv_zero1 … H) -H *
-[ #H #_ destruct //
-| #Y #X1 #X2 #_ #_ #H destruct
-| #m #Y #X1 #X2 #_ #_ #H destruct
-]
-qed.
-
-lemma cnu_gref (h) (G) (L): ∀l. ⦃G,L⦄ ⊢ ⥲[h] 𝐍⦃§l⦄.
-#h #G #L #l1 #n #X #H
-elim (cpm_inv_gref1 … H) -H #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 "basic_2/rt_transition/cnr.ma".
-include "basic_2/rt_transition/cnu.ma".
-
-(* NORMAL TERMS FOR T-UNUNBOUND RT-TRANSITION *******************************)
-
-(* Advanced properties with normal terms for r-transition *******************)
-
-lemma cnu_abst (h) (p) (G) (L):
- ∀W. ⦃G,L⦄ ⊢ ➡[h] 𝐍⦃W⦄ → ∀T.⦃G,L.ⓛW⦄ ⊢ ⥲[h] 𝐍⦃T⦄ → ⦃G,L⦄ ⊢ ⥲[h] 𝐍⦃ⓛ{p}W.T⦄.
-#h #p #G #L #W1 #HW1 #T1 #HT1 #n #X #H
-elim (cpm_inv_abst1 … H) -H #W2 #T2 #HW12 #HT12 #H destruct
-<(HW1 … HW12) -W2 /3 width=2 by tueq_bind/
-qed.
-
-lemma cnu_abbr_neg (h) (G) (L):
- ∀V. ⦃G,L⦄ ⊢ ➡[h] 𝐍⦃V⦄ → ∀T.⦃G,L.ⓓV⦄ ⊢ ⥲[h] 𝐍⦃T⦄ → ⦃G,L⦄ ⊢ ⥲[h] 𝐍⦃-ⓓV.T⦄.
-#h #G #L #V1 #HV1 #T1 #HT1 #n #X #H
-elim (cpm_inv_abbr1 … H) -H *
-[ #V2 #T2 #HV12 #HT12 #H destruct
- <(HV1 … HV12) -V2 /3 width=2 by tueq_bind/
-| #X1 #_ #_ #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 "basic_2/rt_transition/cpm_simple.ma".
-include "basic_2/rt_transition/cnr.ma".
-include "basic_2/rt_transition/cnu.ma".
-
-(* NORMAL TERMS FOR T-UNUNBOUND RT-TRANSITION *******************************)
-
-(* Advanced properties with simple terms and normal terms for r-transition **)
-
-lemma cnu_appl_simple (h) (G) (L):
- ∀V,T. ⦃G,L⦄ ⊢ ➡[h] 𝐍⦃V⦄ → ⦃G,L⦄ ⊢ ⥲[h] 𝐍⦃T⦄ → 𝐒⦃T⦄ → ⦃G,L⦄ ⊢ ⥲[h] 𝐍⦃ⓐV.T⦄.
-#h #G #L #V1 #T1 #HV1 #HT1 #HS #n #X #H
-elim (cpm_inv_appl1_simple … H HS) -H -HS #V2 #T2 #HV12 #HT12 #H destruct
-lapply (HV1 … HV12) -HV1 -HV12 #H destruct
-/3 width=2 by tueq_appl/
-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/syntax/tueq_tueq.ma".
-include "basic_2/rt_transition/cpm_tueq.ma".
-include "basic_2/rt_transition/cnu.ma".
-
-(* NORMAL TERMS FOR T-UNUNBOUND RT-TRANSITION *******************************)
-
-(* Advanced properties ******************************************************)
-
-lemma cnu_tueq_trans (h) (G) (L):
- ∀T1. ⦃G,L⦄ ⊢ ⥲[h] 𝐍⦃T1⦄ → ∀T2.T1 ≅ T2 → ⦃G,L⦄ ⊢ ⥲[h] 𝐍⦃T2⦄.
-#h #G #L #T1 #HT1 #T2 #HT12 #n #T0 #HT20
-@(tueq_canc_sn … HT12)
-elim (tueq_cpm_trans … HT12 … HT20) -T2 #T2 #HT13 #HT30
-/3 width=3 by tueq_trans/
-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_tueq.ma".
-include "basic_2/rt_transition/cpm_drops.ma".
-include "basic_2/rt_transition/cnu.ma".
-
-(* NORMAL TERMS FOR T-UNUNBOUND RT-TRANSITION *******************************)
-
-(* Advanced properties ******************************************************)
-
-lemma cnu_atom_drops (h) (b) (G) (L):
- ∀i. ⬇*[b,𝐔❴i❵] L ≘ ⋆ → ⦃G,L⦄ ⊢ ⥲[h] 𝐍⦃#i⦄.
-#h #b #G #L #i #Hi #n #X #H
-elim (cpm_inv_lref1_drops … H) -H * [ // || #m ] #K #V1 #V2 #HLK
-lapply (drops_gen b … HLK) -HLK #HLK
-lapply (drops_mono … Hi … HLK) -L #H destruct
-qed.
-
-lemma cnu_unit_drops (h) (I) (G) (L):
- ∀K,i. ⬇*[i] L ≘ K.ⓤ{I} → ⦃G,L⦄ ⊢ ⥲[h] 𝐍⦃#i⦄.
-#h #I #G #L #K #i #HLK #n #X #H
-elim (cpm_inv_lref1_drops … H) -H * [ // || #m ] #Y #V1 #V2 #HLY
-lapply (drops_mono … HLK … HLY) -L #H destruct
-qed.
-
-(* Properties with generic relocation ***************************************)
-
-lemma cnu_lifts (h) (G): d_liftable1 … (cnu h G).
-#h #G #K #T #HT #b #f #L #HLK #U #HTU #n #U0 #H
-elim (cpm_inv_lifts_sn … H … HLK … HTU) -b -L #T0 #HTU0 #HT0
-lapply (HT … HT0) -G -K /2 width=6 by tueq_lifts_bi/
-qed-.
-
-(* Inversion lemmas with generic relocation *********************************)
-
-lemma cnu_inv_lifts (h) (G): d_deliftable1 … (cnu h G).
-#h #G #L #U #HU #b #f #K #HLK #T #HTU #n #T0 #H
-elim (cpm_lifts_sn … H … HLK … HTU) -b -K #U0 #HTU0 #HU0
-lapply (HU … HU0) -G -L /2 width=6 by tueq_inv_lifts_bi/
-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_tueq.ma".
-include "basic_2/rt_transition/cnu.ma".
-
-(* NORMAL TERMS FOR T-UNUNBOUND RT-TRANSITION *******************************)
-
-(* Advanced properties with uniform relocation for terms ********************)
-
-lemma cnu_lref (h) (I) (G) (L):
- ∀i. ⦃G,L⦄ ⊢ ⥲[h] 𝐍⦃#i⦄ → ⦃G,L.ⓘ{I}⦄ ⊢ ⥲[h] 𝐍⦃#↑i⦄.
-#h #I #G #L #i #Hi #n #X #H
-elim (cpm_inv_lref1 … H) -H *
-[ #H #_ destruct //
-| #J #K #V #HV #HVX #H destruct
- lapply (Hi … HV) -Hi -HV #HV
- elim (tueq_lifts_dx … HV … HVX) -V #Xi #Hi #HX
- lapply (lifts_inv_lref1_uni … Hi) -Hi #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 "basic_2/rt_transition/cnr_tdeq.ma".
-include "basic_2/rt_transition/cnu_drops.ma".
-include "basic_2/rt_transition/cnu_cnr.ma".
-include "basic_2/rt_transition/cnu_cnr_simple.ma".
-
-(* NORMAL TERMS FOR T-UNUNBOUND RT-TRANSITION *******************************)
-
-(* Properties with context-free sort-irrelevant equivalence for terms *******)
-
-lemma cnu_dec_tdeq (h) (G) (L):
- ∀T1. ∨∨ ⦃G,L⦄ ⊢ ⥲[h] 𝐍⦃T1⦄
- | ∃∃n,T2. ⦃G,L⦄ ⊢ T1 ➡[n,h] T2 & (T1 ≛ T2 → ⊥).
-#h #G #L #T1
-@(fqup_wf_ind_eq (Ⓣ) … G L T1) -G -L -T1 #G0 #L0 #T0 #IH #G #L * *
-[ #s #HG #HL #HT destruct -IH
- /3 width=5 by cnu_sort, or_introl/
-| #i #HG #HL #HT destruct -IH
- elim (drops_F_uni L i)
- [ /3 width=7 by cnu_atom_drops, or_introl/
- | * * [ #I | * #V ] #K #HLK
- [ /3 width=8 by cnu_unit_drops, or_introl/
- | elim (lifts_total V 𝐔❴↑i❵) #W #HVW
- @or_intror @(ex2_2_intro … W) [1,2: /2 width=7 by cpm_delta_drops/ ] #H
- lapply (tdeq_inv_lref1 … H) -H #H destruct
- /2 width=5 by lifts_inv_lref2_uni_lt/
- | elim (lifts_total V 𝐔❴↑i❵) #W #HVW
- @or_intror @(ex2_2_intro … W) [1,2: /2 width=7 by cpm_ell_drops/ ] #H
- lapply (tdeq_inv_lref1 … H) -H #H destruct
- /2 width=5 by lifts_inv_lref2_uni_lt/
- ]
- ]
-| #l #HG #HL #HT destruct -IH
- /3 width=5 by cnu_gref, or_introl/
-| #p * [ cases p ] #V1 #T1 #HG #HL #HT destruct
- [ elim (cpr_subst h G (L.ⓓV1) T1 0 L V1) [| /2 width=1 by drops_refl/ ] #T2 #X2 #HT12 #HXT2 -IH
- elim (tdeq_dec T1 T2) [ -HT12 #HT12 | #HnT12 ]
- [ elim (tdeq_inv_lifts_dx … HT12 … HXT2) -T2 #X1 #HXT1 #_ -X2
- @or_intror @(ex2_2_intro … X1) [1,2: /2 width=4 by cpm_zeta/ ] #H
- /2 width=7 by tdeq_lifts_inv_pair_sn/
- | @or_intror @(ex2_2_intro … (+ⓓV1.T2)) [1,2: /2 width=2 by cpm_bind/ ] #H
- elim (tdeq_inv_pair … H) -H /2 width=1 by/
- ]
- | elim (cnr_dec_tdeq h G L V1) [ elim (IH G (L.ⓓV1) T1) [| * | // ] | * ] -IH
- [ #HT1 #HV1 /3 width=7 by cnu_abbr_neg, or_introl/
- | #n #T2 #HT12 #HnT12 #_
- @or_intror @(ex2_2_intro … (-ⓓV1.T2)) [1,2: /2 width=2 by cpm_bind/ ] #H
- elim (tdeq_inv_pair … H) -H /2 width=1 by/
- | #V2 #HV12 #HnV12
- @or_intror @(ex2_2_intro … (-ⓓV2.T1)) [1,2: /2 width=2 by cpr_pair_sn/ ] #H
- elim (tdeq_inv_pair … H) -H /2 width=1 by/
- ]
- | elim (cnr_dec_tdeq h G L V1) [ elim (IH G (L.ⓛV1) T1) [| * | // ] | * ] -IH
- [ #HT1 #HV1 /3 width=7 by cnu_abst, or_introl/
- | #n #T2 #HT12 #HnT12 #_
- @or_intror @(ex2_2_intro … (ⓛ{p}V1.T2)) [1,2: /2 width=2 by cpm_bind/ ] #H
- elim (tdeq_inv_pair … H) -H /2 width=1 by/
- | #V2 #HV12 #HnV12
- @or_intror @(ex2_2_intro … (ⓛ{p}V2.T1)) [1,2: /2 width=2 by cpr_pair_sn/ ] #H
- elim (tdeq_inv_pair … H) -H /2 width=1 by/
- ]
- ]
-| * #V1 #T1 #HG #HL #HT destruct [| -IH ]
- [ elim (cnr_dec_tdeq h G L V1) [ elim (IH G L T1) [| * | // ] | * ] -IH
- [ #HT1 #HV1
- elim (simple_dec_ex T1) [| * #p * #W1 #U1 #H destruct ]
- [ /3 width=7 by cnu_appl_simple, or_introl/
- | elim (lifts_total V1 𝐔❴1❵) #X1 #HVX1
- @or_intror @(ex2_2_intro … (ⓓ{p}W1.ⓐX1.U1)) [1,2: /2 width=3 by cpm_theta/ ] #H
- elim (tdeq_inv_pair … H) -H #H destruct
- | @or_intror @(ex2_2_intro … (ⓓ{p}ⓝW1.V1.U1)) [1,2: /2 width=2 by cpm_beta/ ] #H
- elim (tdeq_inv_pair … H) -H #H destruct
- ]
- | #n #T2 #HT12 #HnT12 #_
- @or_intror @(ex2_2_intro … (ⓐV1.T2)) [1,2: /2 width=2 by cpm_appl/ ] #H
- elim (tdeq_inv_pair … H) -H /2 width=1 by/
- | #V2 #HV12 #HnV12
- @or_intror @(ex2_2_intro … (ⓐV2.T1)) [1,2: /2 width=2 by cpr_pair_sn/ ] #H
- elim (tdeq_inv_pair … H) -H /2 width=1 by/
- ]
- | @or_intror @(ex2_2_intro … T1) [1,2: /2 width=2 by cpm_eps/ ] #H
- /2 width=4 by tdeq_inv_pair_xy_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 *)
-(* *)
-(**************************************************************************)
-
-include "static_2/relocation/lifts_tueq.ma".
-include "basic_2/rt_transition/cpm.ma".
-
-(* T-BOUND CONTEXT-SENSITIVE PARALLEL RT-TRANSITION FOR TERMS ***************)
-
-(* Properties with tail sort-irrelevant equivalence on terms ****************)
-
-lemma cpm_tueq_conf (h) (n) (G) (L) (T0):
- ∀T1. ⦃G,L⦄ ⊢ T0 ➡[n,h] T1 → ∀T2. T0 ≅ T2 →
- ∃∃T. ⦃G,L⦄ ⊢ T2 ➡[n,h] T & T1 ≅ T.
-#h #n #G #L #T0 #T1 #H @(cpm_ind … H) -G -L -T0 -T1 -n
-[ /2 width=3 by ex2_intro/
-| #G #L #s0 #X2 #H2
- elim (tueq_inv_sort1 … H2) -H2 #s2 #H destruct
- /3 width=3 by tueq_sort, ex2_intro/
-| #n #G #K0 #V0 #V1 #W1 #_ #IH #HVW1 #X2 #H2
- >(tueq_inv_lref1 … H2) -X2
- elim (IH V0) [| // ] -IH #V #HV0 #HV1
- elim (tueq_lifts_sn … HV1 … HVW1) -V1
- /3 width=3 by cpm_delta, ex2_intro/
-| #n #G #K0 #V0 #V1 #W1 #_ #IH #HVW1 #X2 #H2
- >(tueq_inv_lref1 … H2) -X2
- elim (IH V0) [| // ] -IH #V #HV0 #HV1
- elim (tueq_lifts_sn … HV1 … HVW1) -V1
- /3 width=3 by cpm_ell, ex2_intro/
-| #n #I #G #K0 #V1 #W1 #i #_ #IH #HVW1 #X2 #H2
- >(tueq_inv_lref1 … H2) -X2
- elim (IH (#i)) [| // ] -IH #V #HV0 #HV1
- elim (tueq_lifts_sn … HV1 … HVW1) -V1
- /3 width=3 by cpm_lref, ex2_intro/
-| #n #p #I #G #L #V0 #V1 #T0 #T1 #HV01 #_ #_ #IHT #X2 #H2
- elim (tueq_inv_bind1 … H2) -H2 #T2 #HT02 #H destruct
- elim (IHT … HT02) -T0 #T #HT2 #HT1
- /3 width=3 by cpm_bind, tueq_bind, ex2_intro/
-| #n #G #L #V0 #V1 #T0 #T1 #HV10 #_ #_ #IHT #X2 #H2
- elim (tueq_inv_appl1 … H2) -H2 #T2 #HT02 #H destruct
- elim (IHT … HT02) -T0 #T #HT2 #HT1
- /3 width=3 by cpm_appl, tueq_appl, ex2_intro/
-| #n #G #L #V0 #V1 #T0 #T1 #_ #_ #IHV #IHT #X2 #H2
- elim (tueq_inv_cast1 … H2) -H2 #V2 #T2 #HV02 #HT02 #H destruct
- elim (IHV … HV02) -V0 #V #HV2 #HV1
- elim (IHT … HT02) -T0 #T #HT2 #HT1
- /3 width=5 by cpm_cast, tueq_cast, ex2_intro/
-| #n #G #L #V0 #U0 #T0 #T1 #HTU0 #_ #IH #X2 #H2
- elim (tueq_inv_bind1 … H2) -H2 #U2 #HU02 #H destruct
- elim (tueq_inv_lifts_sn … HU02 … HTU0) -U0 #T2 #HTU2 #HT02
- elim (IH … HT02) -T0 #T #HT2 #HT1
- /3 width=3 by cpm_zeta, ex2_intro/
-| #n #G #L #V0 #T0 #T1 #_ #IH #X2 #H2
- elim (tueq_inv_cast1 … H2) -H2 #V2 #T2 #_ #HT02 #H destruct
- elim (IH … HT02) -V0 -T0
- /3 width=3 by cpm_eps, ex2_intro/
-| #n #G #L #V0 #T0 #T1 #_ #IH #X2 #H2
- elim (tueq_inv_cast1 … H2) -H2 #V2 #T2 #HV02 #_ #H destruct
- elim (IH … HV02) -V0 -T1
- /3 width=3 by cpm_ee, ex2_intro/
-| #n #p #G #L #V0 #V1 #W0 #W1 #T0 #T1 #HV01 #HW01 #_ #_ #_ #IHT #X2 #H2
- elim (tueq_inv_appl1 … H2) -H2 #X #H2 #H destruct
- elim (tueq_inv_bind1 … H2) -H2 #T2 #HT02 #H destruct
- elim (IHT … HT02) -T0
- /4 width=3 by cpm_beta, tueq_cast, tueq_bind, ex2_intro/
-| #n #p #G #L #V0 #V1 #U1 #W0 #W1 #T0 #T1 #HV01 #HW01 #_ #_ #_ #IHT #HVU1 #X2 #H2
- elim (tueq_inv_appl1 … H2) -H2 #X #H2 #H destruct
- elim (tueq_inv_bind1 … H2) -H2 #T2 #HT02 #H destruct
- elim (IHT … HT02) -T0 #T #HT2 #HT1
- /4 width=3 by cpm_theta, tueq_appl, tueq_bind, ex2_intro/
-]
-qed-.
-
-lemma tueq_cpm_trans (h) (n) (G) (L) (T0):
- ∀T1. T1 ≅ T0 → ∀T2. ⦃G,L⦄ ⊢ T0 ➡[n,h] T2 →
- ∃∃T. ⦃G,L⦄ ⊢ T1 ➡[n,h] T & T ≅ T2.
-#h #n #G #L #T0 #T1 #HT10 #T2 #HT02
-elim (cpm_tueq_conf … HT02 T1)
-/3 width=3 by tueq_sym, ex2_intro/
-qed-.
]
[ { "context-sensitive native validity" * } {
[ [ "restricted refinement for lenvs" ] "lsubv ( ? ⊢ ? ⫃![?,?] ? )" "lsubv_drops" + "lsubv_lsubr" + "lsubv_lsuba" + "lsubv_cpms" + "lsubv_cpcs" + "lsubv_cnv" + "lsubv_lsubv" * ]
- [ [ "for terms" ] "cnv" + "( ⦃?,?⦄ ⊢ ? ![?,?] )" + "( ⦃?,?⦄ ⊢ ? ![?] )" + "( ⦃?,?⦄ ⊢ ? !*[?] )" "cnv_drops" + "cnv_fqus" + "cnv_aaa" + "cnv_fsb" + "cnv_cpm_trans" + "cnv_cpm_conf" + "cnv_cpm_tdeq" + "cnv_cpm_tdeq_trans" + "cnv_cpm_tdeq_conf" + "cnv_cpms_tdeq" + "cnv_cpms_conf" + "cnv_cpms_tdeq_conf" + "cnv_cpme" + "cnv_cpue" + "cnv_eval" + "cnv_cpce" + "cnv_cpes" + "cnv_cpcs" + "cnv_preserve_sub" + "cnv_preserve" + "cnv_preserve_cpes" + "cnv_preserve_cpcs" * ]
+ [ [ "for terms" ] "cnv" + "( ⦃?,?⦄ ⊢ ? ![?,?] )" + "( ⦃?,?⦄ ⊢ ? ![?] )" + "( ⦃?,?⦄ ⊢ ? !*[?] )" "cnv_drops" + "cnv_fqus" + "cnv_aaa" + "cnv_fsb" + "cnv_cpm_trans" + "cnv_cpm_conf" + "cnv_cpm_tdeq" + "cnv_cpm_tdeq_trans" + "cnv_cpm_tdeq_conf" + "cnv_cpms_tdeq" + "cnv_cpms_conf" + "cnv_cpms_tdeq_conf" + "cnv_cpme" + "cnv_cpmhe" + "cnv_eval" + "cnv_cpce" + "cnv_cpes" + "cnv_cpcs" + "cnv_preserve_sub" + "cnv_preserve" + "cnv_preserve_cpes" + "cnv_preserve_cpcs" * ]
}
]
}
}
]
[ { "t-bound context-sensitive parallel rt-equivalence" * } {
- [ [ "for terms" ] "cpes ( ⦃?,?⦄ ⊢ ? ⬌*[?,?,?] ? )" "cpes_aaa" + "cpes_cprs" * ]
+ [ [ "for terms" ] "cpes ( ⦃?,?⦄ ⊢ ? ⬌*[?,?,?] ? )" "cpes_aaa" + "cpes_cpms" + "cpes_cpes" * ]
}
]
}
]
class "sky"
[ { "rt-computation" * } {
- [ { "t-unbound context-sensitive parallel rt-computation" * } {
- [ [ "evaluation for terms" ] "cpue ( ⦃?,?⦄ ⊢ ? ⥲*[?] 𝐍⦃?⦄ )" "cpue_csx" * ]
- }
- ]
[ { "context-sensitive parallel r-computation" * } {
[ [ "evaluation for terms" ] "cpre ( ⦃?,?⦄ ⊢ ? ➡*[?] 𝐍⦃?⦄ )" "cpre_csx" + "cpre_cpms" + "cpre_cpre" * ]
[ [ "for lenvs on all entries" ] "lprs ( ⦃?,?⦄ ⊢ ➡*[?] ? )" "lprs_tc" + "lprs_ctc" + "lprs_length" + "lprs_drops" + "lprs_aaa" + "lprs_lpr" + "lprs_lpxs" + "lprs_cpms" + "lprs_cprs" + "lprs_lprs" * ]
}
]
[ { "t-bound context-sensitive parallel rt-computation" * } {
+ [ [ "t-unbound head evaluation for terms" ] "cpmhe ( ⦃?,?⦄ ⊢ ? ⬌*[?] 𝐍*⦃?⦄ )" "cpmhe_csx" * ]
[ [ "evaluation for terms" ] "cpme ( ⦃?,?⦄ ⊢ ? ➡*[?,?] 𝐍⦃?⦄ )" "cpme_aaa" * ]
- [ [ "for terms" ] "cpms" + "( ⦃?,?⦄ ⊢ ? ➡*[?,?] ? )" "cpms_drops" + "cpms_lsubr" + "cpms_rdeq" + "cpms_aaa" + "cpms_lpr" + "cpms_cnu" + "cpms_cpxs" + "cpms_fpbs" + "cpms_fpbg" + "cpms_cpms" * ]
+ [ [ "for terms" ] "cpms" + "( ⦃?,?⦄ ⊢ ? ➡*[?,?] ? )" "cpms_drops" + "cpms_lsubr" + "cpms_rdeq" + "cpms_aaa" + "cpms_lpr" + "cpms_cnh" + "cpms_cpxs" + "cpms_fpbs" + "cpms_fpbg" + "cpms_cpms" * ]
}
]
[ { "unbound context-sensitive parallel rst-computation" * } {
class "cyan"
[ { "rt-transition" * } {
[ { "t-unbound context-sensitive parallel rt-transition" * } {
- [ [ "normal form for terms" ] "cnu ( ⦃?,?⦄ ⊢ ⥲[?] 𝐍⦃?⦄ )" "cnu_tdeq" + "cnu_lifts" + "cnu_drops" + "cnu_cnr" + "cnu_cnr_simple" + "cnu_cnu" * ]
+ [ [ "head normal form for terms" ] "cnh ( ⦃?,?⦄ ⊢ ⥲[?] 𝐍⦃?⦄ )" "cnh_tdeq" + "cnh_lifts" + "cnh_drops" + "cnh_cnr" + "cnh_cnr_simple" + "cnh_cnh" * ]
}
]
[ { "context-sensitive parallel r-transition" * } {
}
]
[ { "t-bound context-sensitive parallel rt-transition" * } {
- [ [ "for terms" ] "cpm" + "( ⦃?,?⦄ ⊢ ? ➡[?,?] ? )" "cpm_simple" + "cpm_tdeq" + "cpm_tueq" + "cpm_drops" + "cpm_lsubr" + "cpm_fsle" + "cpm_aaa" + "cpm_cpx" * ]
+ [ [ "for terms" ] "cpm" + "( ⦃?,?⦄ ⊢ ? ➡[?,?] ? )" "cpm_simple" + "cpm_tdeq" + "cpm_drops" + "cpm_lsubr" + "cpm_fsle" + "cpm_aaa" + "cpm_cpx" * ]
}
]
[ { "unbound parallel rst-transition" * } {
[ [ "" ] "lsuby ( ? ⊆[?,?] ? )" "lsuby_lsuby" * ]
}
]
+ [ { "tail sort-irrelevant equivalence" * } {
+ [ [ "" ] "tueq" + "( ? ≅ ? )" "tueq_tueq" * ]
+ }
+ ]
*)
#x #y #H elim (decidable_lt x y) /2 width=1 by not_lt_to_le/
#Hxy elim (H Hxy)
qed-.
+
+lemma arith_m2 (x) (y): x < y → x+(y-↑x) = ↓y.
+#x #y #Hxy >minus_minus [|*: // ] <minus_Sn_n //
+qed-.
lemma minus_plus_m_m_commutative: ∀n,m:nat. n = m + n - m.
// qed-.
+lemma plus_minus_m_m_commutative (n) (m): m ≤ n → n = m+(n-m).
+/2 width=1 by plus_minus_associative/ qed-.
+
lemma plus_to_minus_2: ∀m1,m2,n1,n2. n1 ≤ m1 → n2 ≤ m2 →
m1+n2 = m2+n1 → m1-n1 = m2-n2.
#m1 #m2 #n1 #n2 #H1 #H2 #H
lemma lt_le_false: ∀x,y. x < y → y ≤ x → ⊥.
/3 width=4 by lt_refl_false, lt_to_le_to_lt/ qed-.
+lemma le_dec (n) (m): Decidable (n≤m).
+#n elim n -n [ /2 width=1 by or_introl/ ]
+#n #IH * [ /3 width=2 by lt_zero_false, or_intror/ ]
+#m elim (IH m) -IH
+[ /3 width=1 by or_introl, le_S_S/
+| /4 width=1 by or_intror, le_S_S_to_le/
+]
+qed-.
+
lemma succ_inv_refl_sn: ∀x. ↑x = x → ⊥.
#x #H @(lt_le_false x (↑x)) //
qed-.
| #n1 #IH #n2 elim n2 -n2 /3 width=1 by monotonic_lt_pred/
]
qed.
+
+(* Decidability of predicates ***********************************************)
+
+lemma dec_lt (R:predicate nat):
+ (∀n. Decidable … (R n)) →
+ ∀n. Decidable … (∃∃m. m < n & R m).
+#R #HR #n elim n -n [| #n * ]
+[ @or_intror * /2 width=2 by lt_zero_false/
+| * /4 width=3 by lt_S, or_introl, ex2_intro/
+| #H0 elim (HR n) -HR
+ [ /3 width=3 by or_introl, ex2_intro/
+ | #Hn @or_intror * #m #Hmn #Hm
+ elim (le_to_or_lt_eq … Hmn) -Hmn #H destruct [ -Hn | -H0 ]
+ /4 width=3 by lt_S_S_to_lt, ex2_intro/
+ ]
+]
+qed-.
+
+lemma dec_min (R:predicate nat):
+ (∀n. Decidable … (R n)) → ∀n. R n →
+ ∃∃m. m ≤ n & R m & (∀p. p < m → R p → ⊥).
+#R #HR #n
+@(nat_elim1 n) -n #n #IH #Hn
+elim (dec_lt … HR n) -HR [ -Hn | -IH ]
+[ * #p #Hpn #Hp
+ elim (IH … Hpn Hp) -IH -Hp #m #Hmp #Hm #HNm
+ @(ex3_intro … Hm HNm) -HNm
+ /3 width=3 by lt_to_le, le_to_lt_to_lt/
+| /4 width=4 by ex3_intro, ex2_intro/
+]
+qed-.
lemma arith_l1: ∀x. 1 = 1-x+(x-(x-1)).
#x <arith_l2 //
qed.
-
-lemma arith_m2 (x) (y): x < y → x+(y-↑x) = ↓y.
-#x #y #Hxy >minus_minus [|*: // ] <minus_Sn_n //
-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( T1 ≅ break term 46 T2 )"
+ non associative with precedence 45
+ for @{ 'ApproxEq $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 "static_2/syntax/tueq.ma".
+include "static_2/relocation/lifts_lifts.ma".
+
+(* GENERIC RELOCATION FOR TERMS *********************************************)
+
+(* Properties with tail sort-irrelevant equivalence for terms ***************)
+
+lemma tueq_lifts_sn: liftable2_sn tueq.
+#T1 #T2 #H elim H -T1 -T2
+[ #s1 #s2 #f #X #H >(lifts_inv_sort1 … H) -H
+ /3 width=3 by lifts_sort, tueq_sort, ex2_intro/
+| #i #f #X #H elim (lifts_inv_lref1 … H) -H
+ /3 width=3 by lifts_lref, tueq_lref, ex2_intro/
+| #l #f #X #H >(lifts_inv_gref1 … H) -H
+ /2 width=3 by lifts_gref, tueq_gref, ex2_intro/
+| #p #I #V #T1 #T2 #_ #IHT #f #X #H elim (lifts_inv_bind1 … H) -H
+ #W1 #U1 #HVW1 #HTU1 #H destruct
+ elim (IHT … HTU1) -T1
+ /3 width=3 by lifts_bind, tueq_bind, ex2_intro/
+| #V #T1 #T2 #_ #IHT #f #X #H elim (lifts_inv_flat1 … H) -H
+ #W1 #U1 #HVW1 #HTU1 #H destruct
+ elim (IHT … HTU1) -T1
+ /3 width=3 by lifts_flat, tueq_appl, ex2_intro/
+| #V1 #V2 #T1 #T2 #_ #_ #IHV #IHT #f #X #H elim (lifts_inv_flat1 … H) -H
+ #W1 #U1 #HVW1 #HTU1 #H destruct
+ elim (IHV … HVW1) -V1 elim (IHT … HTU1) -T1
+ /3 width=5 by lifts_flat, tueq_cast, ex2_intro/
+]
+qed-.
+
+lemma tueq_lifts_dx: liftable2_dx tueq.
+/3 width=3 by tueq_lifts_sn, liftable2_sn_dx, tueq_sym/ qed-.
+
+lemma tueq_lifts_bi: liftable2_bi tueq.
+/3 width=6 by tueq_lifts_sn, liftable2_sn_bi/ qed-.
+
+(* Inversion lemmas with tail sort-irrelevant equivalence for terms *********)
+
+lemma tueq_inv_lifts_sn: deliftable2_sn tueq.
+#U1 #U2 #H elim H -U1 -U2
+[ #s1 #s2 #f #X #H >(lifts_inv_sort2 … H) -H
+ /3 width=3 by lifts_sort, tueq_sort, ex2_intro/
+| #i #f #X #H elim (lifts_inv_lref2 … H) -H
+ /3 width=3 by lifts_lref, tueq_lref, ex2_intro/
+| #l #f #X #H >(lifts_inv_gref2 … H) -H
+ /2 width=3 by lifts_gref, tueq_gref, ex2_intro/
+| #p #I #W #U1 #U2 #_ #IHU #f #X #H elim (lifts_inv_bind2 … H) -H
+ #V1 #T1 #HVW1 #HTU1 #H destruct
+ elim (IHU … HTU1) -U1
+ /3 width=3 by lifts_bind, tueq_bind, ex2_intro/
+| #W #U1 #U2 #_ #IHU #f #X #H elim (lifts_inv_flat2 … H) -H
+ #V1 #T1 #HVW1 #HTU1 #H destruct
+ elim (IHU … HTU1) -U1
+ /3 width=3 by lifts_flat, tueq_appl, ex2_intro/
+| #W1 #W2 #U1 #U2 #_ #_ #IHW #IHU #f #X #H elim (lifts_inv_flat2 … H) -H
+ #V1 #T1 #HVW1 #HTU1 #H destruct
+ elim (IHW … HVW1) -W1 elim (IHU … HTU1) -U1
+ /3 width=5 by lifts_flat, tueq_cast, ex2_intro/
+]
+qed-.
+
+lemma tueq_inv_lifts_dx: deliftable2_dx tueq.
+/3 width=3 by tueq_inv_lifts_sn, deliftable2_sn_dx, tueq_sym/ qed-.
+
+lemma tueq_inv_lifts_bi: deliftable2_bi tueq.
+/3 width=6 by tueq_inv_lifts_sn, deliftable2_sn_bi/ 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/notation/relations/approxeq_2.ma".
+include "static_2/syntax/term.ma".
+
+(* TAIL SORT-IRRELEVANT EQUIVALENCE ON TERMS ********************************)
+
+inductive tueq: relation term ≝
+| tueq_sort: ∀s1,s2. tueq (⋆s1) (⋆s2)
+| tueq_lref: ∀i. tueq (#i) (#i)
+| tueq_gref: ∀l. tueq (§l) (§l)
+| tueq_bind: ∀p,I,V,T1,T2. tueq T1 T2 → tueq (ⓑ{p,I}V.T1) (ⓑ{p,I}V.T2)
+| tueq_appl: ∀V,T1,T2. tueq T1 T2 → tueq (ⓐV.T1) (ⓐV.T2)
+| tueq_cast: ∀V1,V2,T1,T2. tueq V1 V2 → tueq T1 T2 → tueq (ⓝV1.T1) (ⓝV2.T2)
+.
+
+interpretation
+ "context-free tail sort-irrelevant equivalence (term)"
+ 'ApproxEq T1 T2 = (tueq T1 T2).
+
+(* Basic properties *********************************************************)
+
+lemma tueq_refl: reflexive … tueq.
+#T elim T -T * [|||| * ]
+/2 width=1 by tueq_sort, tueq_lref, tueq_gref, tueq_bind, tueq_appl, tueq_cast/
+qed.
+
+lemma tueq_sym: symmetric … tueq.
+#T1 #T2 #H elim H -T1 -T2
+/2 width=3 by tueq_sort, tueq_bind, tueq_appl, tueq_cast/
+qed-.
+
+(* Left basic inversion lemmas **********************************************)
+
+fact tueq_inv_sort1_aux: ∀X,Y. X ≅ Y → ∀s1. X = ⋆s1 →
+ ∃s2. Y = ⋆s2.
+#X #Y * -X -Y
+[ #s1 #s2 #s #H destruct /2 width=2 by ex_intro/
+| #i #s #H destruct
+| #l #s #H destruct
+| #p #I #V #T1 #T2 #_ #s #H destruct
+| #V #T1 #T2 #_ #s #H destruct
+| #V1 #V2 #T1 #T2 #_ #_ #s #H destruct
+]
+qed-.
+
+lemma tueq_inv_sort1: ∀Y,s1. ⋆s1 ≅ Y →
+ ∃s2. Y = ⋆s2.
+/2 width=4 by tueq_inv_sort1_aux/ qed-.
+
+fact tueq_inv_lref1_aux: ∀X,Y. X ≅ Y → ∀i. X = #i → Y = #i.
+#X #Y * -X -Y //
+[ #s1 #s2 #j #H destruct
+| #p #I #V #T1 #T2 #_ #j #H destruct
+| #V #T1 #T2 #_ #j #H destruct
+| #V1 #V2 #T1 #T2 #_ #_ #j #H destruct
+]
+qed-.
+
+lemma tueq_inv_lref1: ∀Y,i. #i ≅ Y → Y = #i.
+/2 width=5 by tueq_inv_lref1_aux/ qed-.
+
+fact tueq_inv_gref1_aux: ∀X,Y. X ≅ Y → ∀l. X = §l → Y = §l.
+#X #Y * -X -Y //
+[ #s1 #s2 #k #H destruct
+| #p #I #V #T1 #T2 #_ #k #H destruct
+| #V #T1 #T2 #_ #k #H destruct
+| #V1 #V2 #T1 #T2 #_ #_ #k #H destruct
+]
+qed-.
+
+lemma tueq_inv_gref1: ∀Y,l. §l ≅ Y → Y = §l.
+/2 width=5 by tueq_inv_gref1_aux/ qed-.
+
+fact tueq_inv_bind1_aux: ∀X,Y. X ≅ Y → ∀p,I,V,T1. X = ⓑ{p,I}V.T1 →
+ ∃∃T2. T1 ≅ T2 & Y = ⓑ{p,I}V.T2.
+#X #Y * -X -Y
+[ #s1 #s2 #q #J #W #U1 #H destruct
+| #i #q #J #W #U1 #H destruct
+| #l #q #J #W #U1 #H destruct
+| #p #I #V #T1 #T2 #HT #q #J #W #U1 #H destruct /2 width=3 by ex2_intro/
+| #V #T1 #T2 #_ #q #J #W #U1 #H destruct
+| #V1 #V2 #T1 #T2 #_ #_ #q #J #W #U1 #H destruct
+]
+qed-.
+
+lemma tueq_inv_bind1: ∀p,I,V,T1,Y. ⓑ{p,I}V.T1 ≅ Y →
+ ∃∃T2. T1 ≅ T2 & Y = ⓑ{p,I}V.T2.
+/2 width=3 by tueq_inv_bind1_aux/ qed-.
+
+fact tueq_inv_appl1_aux: ∀X,Y. X ≅ Y → ∀V,T1. X = ⓐV.T1 →
+ ∃∃T2. T1 ≅ T2 & Y = ⓐV.T2.
+#X #Y * -X -Y
+[ #s1 #s2 #W #U1 #H destruct
+| #i #W #U1 #H destruct
+| #l #W #U1 #H destruct
+| #p #I #V #T1 #T2 #_ #W #U1 #H destruct
+| #V #T1 #T2 #HT #W #U1 #H destruct /2 width=3 by ex2_intro/
+| #V1 #V2 #T1 #T2 #_ #_ #W #U1 #H destruct
+]
+qed-.
+
+lemma tueq_inv_appl1: ∀V,T1,Y. ⓐV.T1 ≅ Y →
+ ∃∃T2. T1 ≅ T2 & Y = ⓐV.T2.
+/2 width=3 by tueq_inv_appl1_aux/ qed-.
+
+fact tueq_inv_cast1_aux: ∀X,Y. X ≅ Y → ∀V1,T1. X = ⓝV1.T1 →
+ ∃∃V2,T2. V1 ≅ V2 & T1 ≅ T2 & Y = ⓝV2.T2.
+#X #Y * -X -Y
+[ #s1 #s2 #W1 #U1 #H destruct
+| #i #W1 #U1 #H destruct
+| #l #W1 #U1 #H destruct
+| #p #I #V #T1 #T2 #_ #W1 #U1 #H destruct
+| #V #T1 #T2 #_ #W1 #U1 #H destruct
+| #V1 #V2 #T1 #T2 #HV #HT #W1 #U1 #H destruct /2 width=5 by ex3_2_intro/
+]
+qed-.
+
+lemma tueq_inv_cast1: ∀V1,T1,Y. ⓝV1.T1 ≅ Y →
+ ∃∃V2,T2. V1 ≅ V2 & T1 ≅ T2 & Y = ⓝV2.T2.
+/2 width=3 by tueq_inv_cast1_aux/ qed-.
+
+(* Right basic inversion lemmas *********************************************)
+
+lemma tueq_inv_bind2: ∀p,I,V,T2,X1. X1 ≅ ⓑ{p,I}V.T2 →
+ ∃∃T1. T1 ≅ T2 & X1 = ⓑ{p,I}V.T1.
+#p #I #V #T2 #X1 #H
+elim (tueq_inv_bind1 p I V T2 X1)
+[ #T1 #HT #H destruct ]
+/3 width=3 by tueq_sym, 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 "static_2/syntax/tueq.ma".
+
+(* TAIL SORT-IRRELEVANT EQUIVALENCE ON TERMS ********************************)
+
+(* Main properties **********************************************************)
+
+theorem tueq_trans: Transitive … tueq.
+#T1 #T #H elim H -T1 -T
+[ #s1 #s #X #H
+ elim (tueq_inv_sort1 … H) -s /2 width=1 by tueq_sort/
+| #i1 #i #H //
+| #l1 #l #H //
+| #p #I #V #T1 #T #_ #IHT #X #H
+ elim (tueq_inv_bind1 … H) -H /3 width=1 by tueq_bind/
+| #V #T1 #T #_ #IHT #X #H
+ elim (tueq_inv_appl1 … H) -H /3 width=1 by tueq_appl/
+| #V1 #V #T1 #T #_ #_ #IHV #IHT #X #H
+ elim (tueq_inv_cast1 … H) -H /3 width=1 by tueq_cast/
+]
+qed-.
+
+theorem tueq_canc_sn: left_cancellable … tueq.
+/3 width=3 by tueq_trans, tueq_sym/ qed-.
+
+theorem tueq_canc_dx: right_cancellable … tueq.
+/3 width=3 by tueq_trans, tueq_sym/ qed-.
+
+theorem tueq_repl: ∀T1,T2. T1 ≅ T2 →
+ ∀U1. T1 ≅ U1 → ∀U2. T2 ≅ U2 → U1 ≅ U2.
+/3 width=3 by tueq_canc_sn, tueq_trans/ 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( T1 ≅ break term 46 T2 )"
- non associative with precedence 45
- for @{ 'ApproxEq $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 "static_2/syntax/theq.ma".
+include "static_2/relocation/lifts_lifts.ma".
+
+(* GENERIC RELOCATION FOR TERMS *********************************************)
+
+(* Properties with tail sort-irrelevant head equivalence for terms **********)
+
+lemma theq_lifts_bi: liftable2_bi theq.
+#T1 #T2 #H elim H -T1 -T2 [||| * ]
+[ #s1 #s2 #f #X1 #H1 #X2 #H2
+ >(lifts_inv_sort1 … H1) -H1 >(lifts_inv_sort1 … H2) -H2
+ /1 width=1 by theq_sort/
+| #i #f #X1 #H1 #X2 #H2
+ elim (lifts_inv_lref1 … H1) -H1 #j1 #Hj1 #H destruct
+ elim (lifts_inv_lref1 … H2) -H2 #j2 #Hj2 #H destruct
+ <(at_mono … Hj2 … Hj1) -i -f -j2
+ /1 width=1 by theq_lref/
+| #l #f #X1 #H1 #X2 #H2
+ >(lifts_inv_gref1 … H1) -H1 >(lifts_inv_gref1 … H2) -H2
+ /1 width=1 by theq_gref/
+| #p #I #V1 #V2 #T1 #T2 #f #X1 #H1 #X2 #H2
+ elim (lifts_inv_bind1 … H1) -H1 #W1 #U1 #_ #_ #H destruct
+ elim (lifts_inv_bind1 … H2) -H2 #W2 #U2 #_ #_ #H destruct
+ /1 width=1 by theq_pair/
+| #I #V1 #V2 #T1 #T2 #f #X1 #H1 #X2 #H2
+ elim (lifts_inv_flat1 … H1) -H1 #W1 #U1 #_ #_ #H destruct
+ elim (lifts_inv_flat1 … H2) -H2 #W2 #U2 #_ #_ #H destruct
+ /1 width=1 by theq_pair/
+]
+qed-.
+
+(* Inversion lemmas with tail sort-irrelevant head equivalence for terms ****)
+
+lemma theq_inv_lifts_bi: deliftable2_bi theq.
+#U1 #U2 #H elim H -U1 -U2 [||| * ]
+[ #s1 #s2 #f #X1 #H1 #X2 #H2
+ >(lifts_inv_sort2 … H1) -H1 >(lifts_inv_sort2 … H2) -H2
+ /1 width=1 by theq_sort/
+| #j #f #X1 #H1 #X2 #H2
+ elim (lifts_inv_lref2 … H1) -H1 #i1 #Hj1 #H destruct
+ elim (lifts_inv_lref2 … H2) -H2 #i2 #Hj2 #H destruct
+ <(at_inj … Hj2 … Hj1) -j -f -i1
+ /1 width=1 by theq_lref/
+| #l #f #X1 #H1 #X2 #H2
+ >(lifts_inv_gref2 … H1) -H1 >(lifts_inv_gref2 … H2) -H2
+ /1 width=1 by theq_gref/
+| #p #I #W1 #W2 #U1 #U2 #f #X1 #H1 #X2 #H2
+ elim (lifts_inv_bind2 … H1) -H1 #V1 #T1 #_ #_ #H destruct
+ elim (lifts_inv_bind2 … H2) -H2 #V2 #T2 #_ #_ #H destruct
+ /1 width=1 by theq_pair/
+| #I #W1 #W2 #U1 #U2 #f #X1 #H1 #X2 #H2
+ elim (lifts_inv_flat2 … H1) -H1 #V1 #T1 #_ #_ #H destruct
+ elim (lifts_inv_flat2 … H2) -H2 #V2 #T2 #_ #_ #H destruct
+ /1 width=1 by theq_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/syntax/tueq.ma".
-include "static_2/relocation/lifts_lifts.ma".
-
-(* GENERIC RELOCATION FOR TERMS *********************************************)
-
-(* Properties with tail sort-irrelevant equivalence for terms ***************)
-
-lemma tueq_lifts_sn: liftable2_sn tueq.
-#T1 #T2 #H elim H -T1 -T2
-[ #s1 #s2 #f #X #H >(lifts_inv_sort1 … H) -H
- /3 width=3 by lifts_sort, tueq_sort, ex2_intro/
-| #i #f #X #H elim (lifts_inv_lref1 … H) -H
- /3 width=3 by lifts_lref, tueq_lref, ex2_intro/
-| #l #f #X #H >(lifts_inv_gref1 … H) -H
- /2 width=3 by lifts_gref, tueq_gref, ex2_intro/
-| #p #I #V #T1 #T2 #_ #IHT #f #X #H elim (lifts_inv_bind1 … H) -H
- #W1 #U1 #HVW1 #HTU1 #H destruct
- elim (IHT … HTU1) -T1
- /3 width=3 by lifts_bind, tueq_bind, ex2_intro/
-| #V #T1 #T2 #_ #IHT #f #X #H elim (lifts_inv_flat1 … H) -H
- #W1 #U1 #HVW1 #HTU1 #H destruct
- elim (IHT … HTU1) -T1
- /3 width=3 by lifts_flat, tueq_appl, ex2_intro/
-| #V1 #V2 #T1 #T2 #_ #_ #IHV #IHT #f #X #H elim (lifts_inv_flat1 … H) -H
- #W1 #U1 #HVW1 #HTU1 #H destruct
- elim (IHV … HVW1) -V1 elim (IHT … HTU1) -T1
- /3 width=5 by lifts_flat, tueq_cast, ex2_intro/
-]
-qed-.
-
-lemma tueq_lifts_dx: liftable2_dx tueq.
-/3 width=3 by tueq_lifts_sn, liftable2_sn_dx, tueq_sym/ qed-.
-
-lemma tueq_lifts_bi: liftable2_bi tueq.
-/3 width=6 by tueq_lifts_sn, liftable2_sn_bi/ qed-.
-
-(* Inversion lemmas with tail sort-irrelevant equivalence for terms *********)
-
-lemma tueq_inv_lifts_sn: deliftable2_sn tueq.
-#U1 #U2 #H elim H -U1 -U2
-[ #s1 #s2 #f #X #H >(lifts_inv_sort2 … H) -H
- /3 width=3 by lifts_sort, tueq_sort, ex2_intro/
-| #i #f #X #H elim (lifts_inv_lref2 … H) -H
- /3 width=3 by lifts_lref, tueq_lref, ex2_intro/
-| #l #f #X #H >(lifts_inv_gref2 … H) -H
- /2 width=3 by lifts_gref, tueq_gref, ex2_intro/
-| #p #I #W #U1 #U2 #_ #IHU #f #X #H elim (lifts_inv_bind2 … H) -H
- #V1 #T1 #HVW1 #HTU1 #H destruct
- elim (IHU … HTU1) -U1
- /3 width=3 by lifts_bind, tueq_bind, ex2_intro/
-| #W #U1 #U2 #_ #IHU #f #X #H elim (lifts_inv_flat2 … H) -H
- #V1 #T1 #HVW1 #HTU1 #H destruct
- elim (IHU … HTU1) -U1
- /3 width=3 by lifts_flat, tueq_appl, ex2_intro/
-| #W1 #W2 #U1 #U2 #_ #_ #IHW #IHU #f #X #H elim (lifts_inv_flat2 … H) -H
- #V1 #T1 #HVW1 #HTU1 #H destruct
- elim (IHW … HVW1) -W1 elim (IHU … HTU1) -U1
- /3 width=5 by lifts_flat, tueq_cast, ex2_intro/
-]
-qed-.
-
-lemma tueq_inv_lifts_dx: deliftable2_dx tueq.
-/3 width=3 by tueq_inv_lifts_sn, deliftable2_sn_dx, tueq_sym/ qed-.
-
-lemma tueq_inv_lifts_bi: deliftable2_bi tueq.
-/3 width=6 by tueq_inv_lifts_sn, deliftable2_sn_bi/ 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/lib/arith.ma".
+
+(* APPLICABILITY CONDITION *************************************************)
+
+(* applicability condition specification *)
+record ac: Type[0] ≝ {
+(* degree of the sort *)
+ appl: predicate nat
+}.
+
+(* applicability condition postulates *)
+record ac_props (a): Prop ≝ {
+ ac_dec: ∀m. Decidable (∃∃n. m ≤ n & appl a n)
+}.
+
+(* Notable specifications ***************************************************)
+
+definition apply_top: predicate nat ≝ λn. ⊤.
+
+definition ac_top: ac ≝ mk_ac apply_top.
+
+lemma ac_top_props: ac_props ac_top ≝ mk_ac_props ….
+/3 width=3 by or_introl, ex2_intro/
+qed.
+
+definition ac_eq (k): ac ≝ mk_ac (eq … k).
+
+lemma ac_eq_props (k): ac_props (ac_eq k) ≝ mk_ac_props ….
+#m elim (le_dec m k) #Hm
+[ /3 width=3 by or_introl, ex2_intro/
+| @or_intror * #n #Hmn #H destruct /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/notation/relations/approxeq_2.ma".
-include "static_2/syntax/term.ma".
-
-(* TAIL SORT-IRRELEVANT EQUIVALENCE ON TERMS ********************************)
-
-inductive tueq: relation term ≝
-| tueq_sort: ∀s1,s2. tueq (⋆s1) (⋆s2)
-| tueq_lref: ∀i. tueq (#i) (#i)
-| tueq_gref: ∀l. tueq (§l) (§l)
-| tueq_bind: ∀p,I,V,T1,T2. tueq T1 T2 → tueq (ⓑ{p,I}V.T1) (ⓑ{p,I}V.T2)
-| tueq_appl: ∀V,T1,T2. tueq T1 T2 → tueq (ⓐV.T1) (ⓐV.T2)
-| tueq_cast: ∀V1,V2,T1,T2. tueq V1 V2 → tueq T1 T2 → tueq (ⓝV1.T1) (ⓝV2.T2)
-.
-
-interpretation
- "context-free tail sort-irrelevant equivalence (term)"
- 'ApproxEq T1 T2 = (tueq T1 T2).
-
-(* Basic properties *********************************************************)
-
-lemma tueq_refl: reflexive … tueq.
-#T elim T -T * [|||| * ]
-/2 width=1 by tueq_sort, tueq_lref, tueq_gref, tueq_bind, tueq_appl, tueq_cast/
-qed.
-
-lemma tueq_sym: symmetric … tueq.
-#T1 #T2 #H elim H -T1 -T2
-/2 width=3 by tueq_sort, tueq_bind, tueq_appl, tueq_cast/
-qed-.
-
-(* Left basic inversion lemmas **********************************************)
-
-fact tueq_inv_sort1_aux: ∀X,Y. X ≅ Y → ∀s1. X = ⋆s1 →
- ∃s2. Y = ⋆s2.
-#X #Y * -X -Y
-[ #s1 #s2 #s #H destruct /2 width=2 by ex_intro/
-| #i #s #H destruct
-| #l #s #H destruct
-| #p #I #V #T1 #T2 #_ #s #H destruct
-| #V #T1 #T2 #_ #s #H destruct
-| #V1 #V2 #T1 #T2 #_ #_ #s #H destruct
-]
-qed-.
-
-lemma tueq_inv_sort1: ∀Y,s1. ⋆s1 ≅ Y →
- ∃s2. Y = ⋆s2.
-/2 width=4 by tueq_inv_sort1_aux/ qed-.
-
-fact tueq_inv_lref1_aux: ∀X,Y. X ≅ Y → ∀i. X = #i → Y = #i.
-#X #Y * -X -Y //
-[ #s1 #s2 #j #H destruct
-| #p #I #V #T1 #T2 #_ #j #H destruct
-| #V #T1 #T2 #_ #j #H destruct
-| #V1 #V2 #T1 #T2 #_ #_ #j #H destruct
-]
-qed-.
-
-lemma tueq_inv_lref1: ∀Y,i. #i ≅ Y → Y = #i.
-/2 width=5 by tueq_inv_lref1_aux/ qed-.
-
-fact tueq_inv_gref1_aux: ∀X,Y. X ≅ Y → ∀l. X = §l → Y = §l.
-#X #Y * -X -Y //
-[ #s1 #s2 #k #H destruct
-| #p #I #V #T1 #T2 #_ #k #H destruct
-| #V #T1 #T2 #_ #k #H destruct
-| #V1 #V2 #T1 #T2 #_ #_ #k #H destruct
-]
-qed-.
-
-lemma tueq_inv_gref1: ∀Y,l. §l ≅ Y → Y = §l.
-/2 width=5 by tueq_inv_gref1_aux/ qed-.
-
-fact tueq_inv_bind1_aux: ∀X,Y. X ≅ Y → ∀p,I,V,T1. X = ⓑ{p,I}V.T1 →
- ∃∃T2. T1 ≅ T2 & Y = ⓑ{p,I}V.T2.
-#X #Y * -X -Y
-[ #s1 #s2 #q #J #W #U1 #H destruct
-| #i #q #J #W #U1 #H destruct
-| #l #q #J #W #U1 #H destruct
-| #p #I #V #T1 #T2 #HT #q #J #W #U1 #H destruct /2 width=3 by ex2_intro/
-| #V #T1 #T2 #_ #q #J #W #U1 #H destruct
-| #V1 #V2 #T1 #T2 #_ #_ #q #J #W #U1 #H destruct
-]
-qed-.
-
-lemma tueq_inv_bind1: ∀p,I,V,T1,Y. ⓑ{p,I}V.T1 ≅ Y →
- ∃∃T2. T1 ≅ T2 & Y = ⓑ{p,I}V.T2.
-/2 width=3 by tueq_inv_bind1_aux/ qed-.
-
-fact tueq_inv_appl1_aux: ∀X,Y. X ≅ Y → ∀V,T1. X = ⓐV.T1 →
- ∃∃T2. T1 ≅ T2 & Y = ⓐV.T2.
-#X #Y * -X -Y
-[ #s1 #s2 #W #U1 #H destruct
-| #i #W #U1 #H destruct
-| #l #W #U1 #H destruct
-| #p #I #V #T1 #T2 #_ #W #U1 #H destruct
-| #V #T1 #T2 #HT #W #U1 #H destruct /2 width=3 by ex2_intro/
-| #V1 #V2 #T1 #T2 #_ #_ #W #U1 #H destruct
-]
-qed-.
-
-lemma tueq_inv_appl1: ∀V,T1,Y. ⓐV.T1 ≅ Y →
- ∃∃T2. T1 ≅ T2 & Y = ⓐV.T2.
-/2 width=3 by tueq_inv_appl1_aux/ qed-.
-
-fact tueq_inv_cast1_aux: ∀X,Y. X ≅ Y → ∀V1,T1. X = ⓝV1.T1 →
- ∃∃V2,T2. V1 ≅ V2 & T1 ≅ T2 & Y = ⓝV2.T2.
-#X #Y * -X -Y
-[ #s1 #s2 #W1 #U1 #H destruct
-| #i #W1 #U1 #H destruct
-| #l #W1 #U1 #H destruct
-| #p #I #V #T1 #T2 #_ #W1 #U1 #H destruct
-| #V #T1 #T2 #_ #W1 #U1 #H destruct
-| #V1 #V2 #T1 #T2 #HV #HT #W1 #U1 #H destruct /2 width=5 by ex3_2_intro/
-]
-qed-.
-
-lemma tueq_inv_cast1: ∀V1,T1,Y. ⓝV1.T1 ≅ Y →
- ∃∃V2,T2. V1 ≅ V2 & T1 ≅ T2 & Y = ⓝV2.T2.
-/2 width=3 by tueq_inv_cast1_aux/ qed-.
-
-(* Right basic inversion lemmas *********************************************)
-
-lemma tueq_inv_bind2: ∀p,I,V,T2,X1. X1 ≅ ⓑ{p,I}V.T2 →
- ∃∃T1. T1 ≅ T2 & X1 = ⓑ{p,I}V.T1.
-#p #I #V #T2 #X1 #H
-elim (tueq_inv_bind1 p I V T2 X1)
-[ #T1 #HT #H destruct ]
-/3 width=3 by tueq_sym, 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 "static_2/syntax/tueq.ma".
-
-(* TAIL SORT-IRRELEVANT EQUIVALENCE ON TERMS ********************************)
-
-(* Main properties **********************************************************)
-
-theorem tueq_trans: Transitive … tueq.
-#T1 #T #H elim H -T1 -T
-[ #s1 #s #X #H
- elim (tueq_inv_sort1 … H) -s /2 width=1 by tueq_sort/
-| #i1 #i #H //
-| #l1 #l #H //
-| #p #I #V #T1 #T #_ #IHT #X #H
- elim (tueq_inv_bind1 … H) -H /3 width=1 by tueq_bind/
-| #V #T1 #T #_ #IHT #X #H
- elim (tueq_inv_appl1 … H) -H /3 width=1 by tueq_appl/
-| #V1 #V #T1 #T #_ #_ #IHV #IHT #X #H
- elim (tueq_inv_cast1 … H) -H /3 width=1 by tueq_cast/
-]
-qed-.
-
-theorem tueq_canc_sn: left_cancellable … tueq.
-/3 width=3 by tueq_trans, tueq_sym/ qed-.
-
-theorem tueq_canc_dx: right_cancellable … tueq.
-/3 width=3 by tueq_trans, tueq_sym/ qed-.
-
-theorem tueq_repl: ∀T1,T2. T1 ≅ T2 →
- ∀U1. T1 ≅ U1 → ∀U2. T2 ≅ U2 → U1 ≅ U2.
-/3 width=3 by tueq_canc_sn, tueq_trans/ qed-.
]
class "red"
[ { "syntax" * } {
+ [ { "applicability condition" * } {
+ [ [ "properties" ] "ac" * ]
+ }
+ ]
[ { "equivalence up to exclusion binders" * } {
[ [ "for lenvs" ] "lveq" + "( ? ≋ⓧ*[?,?] ? )" "lveq_length" + "lveq_lveq" * ]
}
[ [ "for lenvs" ] "append" + "( ? + ? )" "append_length" * ]
}
]
- [ { "head equivalence" * } {
+ [ { "sort-irrelevant head equivalence" * } {
[ [ "for terms" ] "theq" + "( ? ⩳ ? )" "theq_simple" + "theq_tdeq" + "theq_theq" + "theq_simple_vector" * ]
}
]
- [ { "tail sort-irrelevant equivalence" * } {
- [ [ "" ] "tueq" + "( ? ≅ ? )" "tueq_tueq" * ]
- }
- ]
[ { "sort-irrelevant equivalence" * } {
[ [ "" ] "tdeq_ext" + "( ? ≛ ? )" + "( ? ⊢ ? ≛ ? )" * ]
[ [ "" ] "tdeq" + "( ? ≛ ? )" "tdeq_tdeq" * ]
projects / helm.git / commitdiff