--- /dev/null
+lemma lprs_cpr_trans: ∀G. b_c_transitive … (cpr G) (λ_. lprs G).
+/3 width=5 by b_c_trans_CTC2, lpr_cprs_trans/ qed-.
+
+(* Basic_1: was just: pr3_pr3_pr3_t *)
+(* Note: alternative proof /3 width=5 by s_r_trans_CTC1, lprs_cpr_trans/ *)
+lemma lprs_cprs_trans: ∀G. b_rs_transitive … (cpr G) (λ_. lprs G).
+#G @b_c_to_b_rs_trans @b_c_trans_CTC2
+@b_rs_trans_TC1 /2 width=3 by lpr_cprs_trans/ (**) (* full auto too slow *)
+qed-.
(* *)
(**************************************************************************)
-include "basic_2/rt_transition/lpr_lpr.ma".
include "basic_2/rt_computation/cpms_lpr.ma".
include "basic_2/rt_computation/cprs_cpr.ma".
(* Basic properties *********************************************************)
-lemma lprs_refl (h) (G): ∀L. ⦃G, L⦄ ⊢ ➡*[h] L.
-/2 width=1 by lex_refl/ qed.
-
(* Basic_2A1: uses: lprs_pair_refl *)
lemma lprs_bind_refl_dx (h) (G): ∀L1,L2. ⦃G, L1⦄ ⊢ ➡*[h] L2 →
∀I. ⦃G, L1.ⓘ{I}⦄ ⊢ ➡*[h] L2.ⓘ{I}.
/2 width=1 by lex_bind_refl_dx/ qed.
+lemma lprs_pair (h) (G): ∀L1,L2. ⦃G, L1⦄ ⊢ ➡*[h] L2 →
+ ∀V1,V2. ⦃G, L1⦄ ⊢ V1 ➡*[h] V2 →
+ ∀I. ⦃G, L1.ⓑ{I}V1⦄ ⊢ ➡*[h] L2.ⓑ{I}V2.
+/2 width=1 by lex_pair/ qed.
+
+lemma lprs_refl (h) (G): ∀L. ⦃G, L⦄ ⊢ ➡*[h] L.
+/2 width=1 by lex_refl/ qed.
+
(* Basic inversion lemmas ***************************************************)
(* Basic_2A1: uses: lprs_inv_atom1 *)
lemma lprs_inv_atom_sn (h) (G): ∀L2. ⦃G, ⋆⦄ ⊢ ➡*[h] L2 → L2 = ⋆.
/2 width=2 by lex_inv_atom_sn/ qed-.
+(* Basic_2A1: was: lprs_inv_pair1 *)
+lemma lprs_inv_pair_sn (h) (G):
+ ∀I,K1,L2,V1. ⦃G, K1.ⓑ{I}V1⦄ ⊢ ➡*[h] L2 →
+ ∃∃K2,V2. ⦃G, K1⦄ ⊢ ➡*[h] K2 & ⦃G, K1⦄ ⊢ V1 ➡*[h] V2 & L2 = K2.ⓑ{I}V2.
+/2 width=1 by lex_inv_pair_sn/ qed-.
+
(* Basic_2A1: uses: lprs_inv_atom2 *)
lemma lprs_inv_atom_dx (h) (G): ∀L1. ⦃G, L1⦄ ⊢ ➡*[h] ⋆ → L1 = ⋆.
/2 width=2 by lex_inv_atom_dx/ qed-.
+
+(* Basic_2A1: was: lprs_inv_pair2 *)
+lemma lprs_inv_pair_dx (h) (G):
+ ∀I,L1,K2,V2. ⦃G, L1⦄ ⊢ ➡*[h] K2.ⓑ{I}V2 →
+ ∃∃K1,V1. ⦃G, K1⦄ ⊢ ➡*[h] K2 & ⦃G, K1⦄ ⊢ V1 ➡*[h] V2 & L1 = K1.ⓑ{I}V1.
+/2 width=1 by lex_inv_pair_dx/ qed-.
+
+(* Basic eliminators ********************************************************)
+
+(* Basic_2A1: was: lprs_ind_alt *)
+lemma lprs_ind (h) (G): ∀R:relation lenv.
+ R (⋆) (⋆) → (
+ ∀I,K1,K2.
+ ⦃G, K1⦄ ⊢ ➡*[h] K2 →
+ R K1 K2 → R (K1.ⓘ{I}) (K2.ⓘ{I})
+ ) → (
+ ∀I,K1,K2,V1,V2.
+ ⦃G, K1⦄ ⊢ ➡*[h] K2 → ⦃G, K1⦄ ⊢ V1 ➡*[h] V2 →
+ R K1 K2 → R (K1.ⓑ{I}V1) (K2.ⓑ{I}V2)
+ ) →
+ ∀L1,L2. ⦃G, L1⦄ ⊢ ➡*[h] L2 → R L1 L2.
+/3 width=4 by lex_ind/ 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_lpr.ma".
+
+(* PARALLEL R-COMPUTATION FOR FULL LOCAL ENVIRONMENTS ***********************)
+
+(* Properties with t-bound context-sensitive rt-computarion for terms *******)
+
+lemma lprs_cpms_trans (n) (h) (G):
+ ∀L2,T1,T2. ⦃G, L2⦄ ⊢ T1 ➡*[n, h] T2 →
+ ∀L1. ⦃G, L1⦄ ⊢ ➡*[h] L2 → ⦃G, L1⦄ ⊢ T1 ➡*[n, h] T2.
+#n #h #G #L2 #T1 #T2 #HT12 #L1 #H
+@(lprs_ind_sn … H) -L1 /2 width=3 by lpr_cpms_trans/
+qed-.
+
+lemma lprs_cpm_trans (n) (h) (G):
+ ∀L2,T1,T2. ⦃G, L2⦄ ⊢ T1 ➡[n, h] T2 →
+ ∀L1. ⦃G, L1⦄ ⊢ ➡*[h] L2 → ⦃G, L1⦄ ⊢ T1 ➡*[n, h] T2.
+/3 width=3 by lprs_cpms_trans, cpm_cpms/ qed-.
+
+(* Basic_2A1: includes cprs_bind2 *)
+lemma cpms_bind_dx (n) (h) (G) (L):
+ ∀V1,V2. ⦃G, L⦄ ⊢ V1 ➡*[h] V2 →
+ ∀I,T1,T2. ⦃G, L.ⓑ{I}V2⦄ ⊢ T1 ➡*[n, h] T2 →
+ ∀p. ⦃G, L⦄ ⊢ ⓑ{p,I}V1.T1 ➡*[n, h] ⓑ{p,I}V2.T2.
+/4 width=5 by lprs_cpms_trans, lprs_pair, cpms_bind/ qed.
+
+(* Inversion lemmas with t-bound context-sensitive rt-computarion for terms *)
+
+(* Basic_1: was: pr3_gen_abst *)
+(* Basic_2A1: includes: cprs_inv_abst1 *)
+(* Basic_2A1: uses: scpds_inv_abst1 *)
+lemma cpms_inv_abst_sn (n) (h) (G) (L):
+ ∀p,V1,T1,X2. ⦃G, L⦄ ⊢ ⓛ{p}V1.T1 ➡*[n, h] X2 →
+ ∃∃V2,T2. ⦃G, L⦄ ⊢ V1 ➡*[h] V2 & ⦃G, L.ⓛV1⦄ ⊢ T1 ➡*[n, h] T2 &
+ X2 = ⓛ{p}V2.T2.
+#n #h #G #L #p #V1 #T1 #X2 #H
+@(cpms_ind_dx … H) -X2 /2 width=5 by ex3_2_intro/
+#n1 #n2 #X #X2 #_ * #V #T #HV1 #HT1 #H1 #H2 destruct
+elim (cpm_inv_abst1 … H2) -H2 #V2 #T2 #HV2 #HT2 #H2 destruct
+/5 width=7 by lprs_cpm_trans, lprs_pair, cprs_step_dx, cpms_trans, ex3_2_intro/
+qed-.
+
+(* Basic_2A1: includes: cprs_inv_abst *)
+lemma cpms_inv_abst_bi (n) (h) (G) (L):
+ ∀p,W1,W2,T1,T2. ⦃G, L⦄ ⊢ ⓛ{p}W1.T1 ➡*[n, h] ⓛ{p}W2.T2 →
+ ∧∧ ⦃G, L⦄ ⊢ W1 ➡*[h] W2 & ⦃G, L.ⓛW1⦄ ⊢ T1 ➡*[n, h] T2.
+#n #h #G #L #p #W1 #W2 #T1 #T2 #H
+elim (cpms_inv_abst_sn … H) -H #W #T #HW1 #HT1 #H destruct
+/2 width=1 by conj/
+qed-.
+
+(* Basic_1: was pr3_gen_abbr *)
+(* Basic_2A1: includes: cprs_inv_abbr1 *)
+lemma cpms_inv_abbr_sn (n) (h) (G) (L):
+ ∀p,V1,T1,X2. ⦃G, L⦄ ⊢ ⓓ{p}V1.T1 ➡*[n, h] X2 →
+ ∨∨ ∃∃V2,T2. ⦃G, L⦄ ⊢ V1 ➡*[h] V2 & ⦃G, L.ⓓV1⦄ ⊢ T1 ➡*[n, h] T2 & X2 = ⓓ{p}V2.T2
+ | ∃∃T2. ⦃G, L.ⓓV1⦄ ⊢ T1 ➡*[n ,h] T2 & ⬆*[1] X2 ≘ T2 & p = Ⓣ.
+#n #h #G #L #p #V1 #T1 #X2 #H
+@(cpms_ind_dx … H) -X2 -n /3 width=5 by ex3_2_intro, or_introl/
+#n1 #n2 #X #X2 #_ * *
+[ #V #T #HV1 #HT1 #H #HX2 destruct
+ elim (cpm_inv_abbr1 … HX2) -HX2 *
+ [ #V2 #T2 #HV2 #HT2 #H destruct
+ /6 width=7 by lprs_cpm_trans, lprs_pair, cprs_step_dx, cpms_trans, ex3_2_intro, or_introl/
+ | #T2 #HT2 #HXT2 #Hp
+ /6 width=7 by lprs_cpm_trans, lprs_pair, cpms_trans, ex3_intro, or_intror/
+ ]
+| #T #HT1 #HXT #Hp #HX2
+ elim (cpm_lifts_sn … HX2 (Ⓣ) … (L.ⓓV1) … HXT) -X
+ /4 width=3 by cpms_step_dx, drops_refl, drops_drop, ex3_intro, or_intror/
+]
+qed-.
+
+(* Basic_2A1: uses: scpds_inv_abbr_abst *)
+lemma cpms_inv_abbr_abst (n) (h) (G) (L):
+ ∀p1,p2,V1,W2,T1,T2. ⦃G, L⦄ ⊢ ⓓ{p1}V1.T1 ➡*[n, h] ⓛ{p2}W2.T2 →
+ ∃∃T. ⦃G, L.ⓓV1⦄ ⊢ T1 ➡*[n, h] T & ⬆*[1] ⓛ{p2}W2.T2 ≘ T & p1 = Ⓣ.
+#n #h #G #L #p1 #p2 #V1 #W2 #T1 #T2 #H
+elim (cpms_inv_abbr_sn … H) -H *
+[ #V #T #_ #_ #H destruct
+| /2 width=3 by ex3_intro/
+]
+qed-.
(* *)
(**************************************************************************)
-include "basic_2/computation/cprs_cprs.ma".
-include "basic_2/computation/lprs.ma".
+include "basic_2/rt_computation/cprs_cprs.ma".
+include "basic_2/rt_computation/lprs_cpms.ma".
-(* SN PARALLEL COMPUTATION ON LOCAL ENVIRONMENTS ****************************)
+(* PARALLEL R-COMPUTATION FOR FULL LOCAL ENVIRONMENTS ***********************)
(* Advanced properties ******************************************************)
-lemma lprs_pair: ∀I,G,L1,L2. ⦃G, L1⦄ ⊢ ➡* L2 →
- ∀V1,V2. ⦃G, L1⦄ ⊢ V1 ➡* V2 → ⦃G, L1.ⓑ{I}V1⦄ ⊢ ➡* L2.ⓑ{I}V2.
-/2 width=1 by TC_lpx_sn_pair/ qed.
+(* Basic_2A1: was: lprs_pair2 *)
+lemma lprs_pair_dx (h) (G): ∀L1,L2. ⦃G, L1⦄ ⊢ ➡*[h] L2 →
+ ∀V1,V2. ⦃G, L2⦄ ⊢ V1 ➡*[h] V2 →
+ ∀I. ⦃G, L1.ⓑ{I}V1⦄ ⊢ ➡*[h] L2.ⓑ{I}V2.
+/3 width=3 by lprs_pair, lprs_cpms_trans/ qed.
-(* Advanced inversion lemmas ************************************************)
+(* Properties on context-sensitive parallel r-computation for terms *********)
-lemma lprs_inv_pair1: ∀I,G,K1,L2,V1. ⦃G, K1.ⓑ{I}V1⦄ ⊢ ➡* L2 →
- ∃∃K2,V2. ⦃G, K1⦄ ⊢ ➡* K2 & ⦃G, K1⦄ ⊢ V1 ➡* V2 &
- L2 = K2.ⓑ{I}V2.
-/3 width=3 by TC_lpx_sn_inv_pair1, lpr_cprs_trans/ qed-.
-
-lemma lprs_inv_pair2: ∀I,G,L1,K2,V2. ⦃G, L1⦄ ⊢ ➡* K2.ⓑ{I}V2 →
- ∃∃K1,V1. ⦃G, K1⦄ ⊢ ➡* K2 & ⦃G, K1⦄ ⊢ V1 ➡* V2 &
- L1 = K1.ⓑ{I}V1.
-/3 width=3 by TC_lpx_sn_inv_pair2, lpr_cprs_trans/ qed-.
-
-(* Advanced eliminators *****************************************************)
-
-lemma lprs_ind_alt: ∀G. ∀R:relation lenv.
- R (⋆) (⋆) → (
- ∀I,K1,K2,V1,V2.
- ⦃G, K1⦄ ⊢ ➡* K2 → ⦃G, K1⦄ ⊢ V1 ➡* V2 →
- R K1 K2 → R (K1.ⓑ{I}V1) (K2.ⓑ{I}V2)
- ) →
- ∀L1,L2. ⦃G, L1⦄ ⊢ ➡* L2 → R L1 L2.
-/3 width=4 by TC_lpx_sn_ind, lpr_cprs_trans/ qed-.
-
-(* Properties on context-sensitive parallel computation for terms ***********)
-
-lemma lprs_cpr_trans: ∀G. b_c_transitive … (cpr G) (λ_. lprs G).
-/3 width=5 by b_c_trans_CTC2, lpr_cprs_trans/ qed-.
-
-(* Basic_1: was just: pr3_pr3_pr3_t *)
-(* Note: alternative proof /3 width=5 by s_r_trans_CTC1, lprs_cpr_trans/ *)
-lemma lprs_cprs_trans: ∀G. b_rs_transitive … (cpr G) (λ_. lprs G).
-#G @b_c_to_b_rs_trans @b_c_trans_CTC2
-@b_rs_trans_TC1 /2 width=3 by lpr_cprs_trans/ (**) (* full auto too slow *)
-qed-.
-
-lemma lprs_cprs_conf_dx: ∀G,L0,T0,T1. ⦃G, L0⦄ ⊢ T0 ➡* T1 →
- ∀L1. ⦃G, L0⦄ ⊢ ➡* L1 →
- ∃∃T. ⦃G, L1⦄ ⊢ T1 ➡* T & ⦃G, L1⦄ ⊢ T0 ➡* T.
-#G #L0 #T0 #T1 #HT01 #L1 #H @(lprs_ind … H) -L1 /2 width=3 by ex2_intro/
+lemma lprs_cprs_conf_dx (h) (G): ∀L0.∀T0,T1:term. ⦃G, L0⦄ ⊢ T0 ➡*[h] T1 →
+ ∀L1. ⦃G, L0⦄ ⊢ ➡*[h] L1 →
+ ∃∃T. ⦃G, L1⦄ ⊢ T1 ➡*[h] T & ⦃G, L1⦄ ⊢ T0 ➡*[h] T.
+#h #G #L0 #T0 #T1 #HT01 #L1 #H
+@(lprs_ind_dx … H) -L1 /2 width=3 by ex2_intro/
#L #L1 #_ #HL1 * #T #HT1 #HT0 -L0
elim (cprs_lpr_conf_dx … HT1 … HL1) -HT1 #T2 #HT2
elim (cprs_lpr_conf_dx … HT0 … HL1) -L #T3 #HT3
/3 width=5 by cprs_trans, ex2_intro/
qed-.
-lemma lprs_cpr_conf_dx: ∀G,L0,T0,T1. ⦃G, L0⦄ ⊢ T0 ➡ T1 →
- ∀L1. ⦃G, L0⦄ ⊢ ➡* L1 →
- ∃∃T. ⦃G, L1⦄ ⊢ T1 ➡* T & ⦃G, L1⦄ ⊢ T0 ➡* T.
-/3 width=3 by lprs_cprs_conf_dx, cpr_cprs/ qed-.
+lemma lprs_cpr_conf_dx (h) (G): ∀L0. ∀T0,T1:term. ⦃G, L0⦄ ⊢ T0 ➡[h] T1 →
+ ∀L1. ⦃G, L0⦄ ⊢ ➡*[h] L1 →
+ ∃∃T. ⦃G, L1⦄ ⊢ T1 ➡*[h] T & ⦃G, L1⦄ ⊢ T0 ➡*[h] T.
+/3 width=3 by lprs_cprs_conf_dx, cpm_cpms/ qed-.
-(* Note: this can be proved on its own using lprs_ind_dx *)
-lemma lprs_cprs_conf_sn: ∀G,L0,T0,T1. ⦃G, L0⦄ ⊢ T0 ➡* T1 →
- ∀L1. ⦃G, L0⦄ ⊢ ➡* L1 →
- ∃∃T. ⦃G, L0⦄ ⊢ T1 ➡* T & ⦃G, L1⦄ ⊢ T0 ➡* T.
-#G #L0 #T0 #T1 #HT01 #L1 #HL01
+(* Note: this can be proved on its own using lprs_ind_sn *)
+lemma lprs_cprs_conf_sn (h) (G): ∀L0. ∀T0,T1:term. ⦃G, L0⦄ ⊢ T0 ➡*[h] T1 →
+ ∀L1. ⦃G, L0⦄ ⊢ ➡*[h] L1 →
+ ∃∃T. ⦃G, L0⦄ ⊢ T1 ➡*[h] T & ⦃G, L1⦄ ⊢ T0 ➡*[h] T.
+#h #G #L0 #T0 #T1 #HT01 #L1 #HL01
elim (lprs_cprs_conf_dx … HT01 … HL01) -HT01
-/3 width=3 by lprs_cprs_trans, ex2_intro/
+/3 width=3 by lprs_cpms_trans, ex2_intro/
qed-.
-lemma lprs_cpr_conf_sn: ∀G,L0,T0,T1. ⦃G, L0⦄ ⊢ T0 ➡ T1 →
- ∀L1. ⦃G, L0⦄ ⊢ ➡* L1 →
- ∃∃T. ⦃G, L0⦄ ⊢ T1 ➡* T & ⦃G, L1⦄ ⊢ T0 ➡* T.
-/3 width=3 by lprs_cprs_conf_sn, cpr_cprs/ qed-.
-
-lemma cprs_bind2: ∀G,L,V1,V2. ⦃G, L⦄ ⊢ V1 ➡* V2 →
- ∀I,T1,T2. ⦃G, L.ⓑ{I}V2⦄ ⊢ T1 ➡* T2 →
- ∀a. ⦃G, L⦄ ⊢ ⓑ{a,I}V1.T1 ➡* ⓑ{a,I}V2.T2.
-/4 width=5 by lprs_cprs_trans, lprs_pair, cprs_bind/ qed.
-
-(* Inversion lemmas on context-sensitive parallel computation for terms *****)
-
-(* Basic_1: was: pr3_gen_abst *)
-lemma cprs_inv_abst1: ∀a,G,L,W1,T1,U2. ⦃G, L⦄ ⊢ ⓛ{a}W1.T1 ➡* U2 →
- ∃∃W2,T2. ⦃G, L⦄ ⊢ W1 ➡* W2 & ⦃G, L.ⓛW1⦄ ⊢ T1 ➡* T2 &
- U2 = ⓛ{a}W2.T2.
-#a #G #L #V1 #T1 #U2 #H @(cprs_ind … H) -U2 /2 width=5 by ex3_2_intro/
-#U0 #U2 #_ #HU02 * #V0 #T0 #HV10 #HT10 #H destruct
-elim (cpr_inv_abst1 … HU02) -HU02 #V2 #T2 #HV02 #HT02 #H destruct
-lapply (lprs_cpr_trans … HT02 (L.ⓛV1) ?)
-/3 width=5 by lprs_pair, cprs_trans, cprs_strap1, ex3_2_intro/
-qed-.
-
-lemma cprs_inv_abst: ∀a,G,L,W1,W2,T1,T2. ⦃G, L⦄ ⊢ ⓛ{a}W1.T1 ➡* ⓛ{a}W2.T2 →
- ⦃G, L⦄ ⊢ W1 ➡* W2 ∧ ⦃G, L.ⓛW1⦄ ⊢ T1 ➡* T2.
-#a #G #L #W1 #W2 #T1 #T2 #H elim (cprs_inv_abst1 … H) -H
-#W #T #HW1 #HT1 #H destruct /2 width=1 by conj/
-qed-.
-
-(* Basic_1: was pr3_gen_abbr *)
-lemma cprs_inv_abbr1: ∀a,G,L,V1,T1,U2. ⦃G, L⦄ ⊢ ⓓ{a}V1.T1 ➡* U2 → (
- ∃∃V2,T2. ⦃G, L⦄ ⊢ V1 ➡* V2 & ⦃G, L.ⓓV1⦄ ⊢ T1 ➡* T2 &
- U2 = ⓓ{a}V2.T2
- ) ∨
- ∃∃T2. ⦃G, L.ⓓV1⦄ ⊢ T1 ➡* T2 & ⬆[0, 1] U2 ≘ T2 & a = true.
-#a #G #L #V1 #T1 #U2 #H @(cprs_ind … H) -U2 /3 width=5 by ex3_2_intro, or_introl/
-#U0 #U2 #_ #HU02 * *
-[ #V0 #T0 #HV10 #HT10 #H destruct
- elim (cpr_inv_abbr1 … HU02) -HU02 *
- [ #V2 #T2 #HV02 #HT02 #H destruct
- lapply (lprs_cpr_trans … HT02 (L.ⓓV1) ?)
- /4 width=5 by lprs_pair, cprs_trans, cprs_strap1, ex3_2_intro, or_introl/
- | #T2 #HT02 #HUT2
- lapply (lprs_cpr_trans … HT02 (L.ⓓV1) ?) -HT02
- /4 width=3 by lprs_pair, cprs_trans, ex3_intro, or_intror/
- ]
-| #U1 #HTU1 #HU01 elim (lift_total U2 0 1)
- #U #HU2 lapply (cpr_lift … HU02 (L.ⓓV1) … HU01 … HU2) -U0
- /4 width=3 by cprs_strap1, drop_drop, ex3_intro, or_intror/
-]
-qed-.
-
-(* More advanced properties *************************************************)
-
-lemma lprs_pair2: ∀I,G,L1,L2. ⦃G, L1⦄ ⊢ ➡* L2 →
- ∀V1,V2. ⦃G, L2⦄ ⊢ V1 ➡* V2 → ⦃G, L1.ⓑ{I}V1⦄ ⊢ ➡* L2.ⓑ{I}V2.
-/3 width=3 by lprs_pair, lprs_cprs_trans/ qed.
-
-(* Advanced inversion lemmas ************************************************)
-
-(* Basic_2A1: uses: scpds_inv_abst1 *)
-lemma cpms_inv_abst_sn (n) (h) (G) (L):
- ∀p,V1,T1,X2. ⦃G, L⦄ ⊢ ⓛ{p}V1.T1 ➡*[n, h] X2 →
- ∃∃V2,T2. ⦃G, L⦄ ⊢ V1 ➡*[h] V2 & ⦃G, L.ⓛV1⦄ ⊢ T1 ➡*[n, h] T2 &
- X2 = ⓛ{p}V2.T2.
-#n #h #G #L #p #V1 #T1 #X2 #H
-@(cpms_ind_dx … H) -X2 /2 width=5 by ex3_2_intro/
-#n1 #n2 #X #X2 #_ * #V #T #HV1 #HT1 #H1 #H2 destruct
-elim (cpm_inv_abst1 … H2) -H2 #V2 #T2 #HV2 #HT2 #H2 destruct
-@ex3_2_intro [1,2,5: // ]
-[ /2 width=3 by cprs_step_dx/
-| @(cpms_trans … HT1) -T1 -V2 -n1
-
-/3 width=5 by cprs_step_dx, cpms_step_dx, ex3_2_intro/
-
-
-
-#d2 * #X #d1 #Hd21 #Hd1 #H1 #H2
-lapply (da_inv_bind … Hd1) -Hd1 #Hd1
-elim (lstas_inv_bind1 … H1) -H1 #U #HTU1 #H destruct
-elim (cprs_inv_abst1 … H2) -H2 #V2 #T2 #HV12 #HUT2 #H destruct
-/3 width=6 by ex4_2_intro, ex3_2_intro/
-qed-.
-
-lemma scpds_inv_abbr_abst: ∀h,o,a1,a2,G,L,V1,W2,T1,T2,d. ⦃G, L⦄ ⊢ ⓓ{a1}V1.T1 •*➡*[h, o, d] ⓛ{a2}W2.T2 →
- ∃∃T. ⦃G, L.ⓓV1⦄ ⊢ T1 •*➡*[h, o, d] T & ⬆[0, 1] ⓛ{a2}W2.T2 ≘ T & a1 = true.
-#h #o #a1 #a2 #G #L #V1 #W2 #T1 #T2 #d2 * #X #d1 #Hd21 #Hd1 #H1 #H2
-lapply (da_inv_bind … Hd1) -Hd1 #Hd1
-elim (lstas_inv_bind1 … H1) -H1 #U1 #HTU1 #H destruct
-elim (cprs_inv_abbr1 … H2) -H2 *
-[ #V2 #U2 #HV12 #HU12 #H destruct
-| /3 width=6 by ex4_2_intro, ex3_intro/
-]
-qed-.
-*)
+lemma lprs_cpr_conf_sn (h) (G): ∀L0. ∀T0,T1:term. ⦃G, L0⦄ ⊢ T0 ➡[h] T1 →
+ ∀L1. ⦃G, L0⦄ ⊢ ➡*[h] L1 →
+ ∃∃T. ⦃G, L0⦄ ⊢ T1 ➡*[h] T & ⦃G, L1⦄ ⊢ T0 ➡*[h] T.
+/3 width=3 by lprs_cprs_conf_sn, cpm_cpms/ qed-.
(* *)
(**************************************************************************)
-include "basic_2/relocation/lex_tc.ma".
-include "basic_2/rt_computation/cprs_lpr.ma".
-include "basic_2/rt_computation/lprs_ctc.ma".
+include "basic_2/rt_computation/lprs_tc.ma".
(* PARALLEL R-COMPUTATION FOR FULL LOCAL ENVIRONMENTS ***********************)
lemma lprs_step_dx (h) (G): ∀L1,L. ⦃G, L1⦄ ⊢ ➡*[h] L →
∀L2. ⦃G, L⦄ ⊢ ➡[h] L2 → ⦃G, L1⦄ ⊢ ➡*[h] L2.
/4 width=3 by lprs_inv_CTC, lprs_CTC, lpr_cprs_trans, lex_CTC_step_dx/ qed-.
+
+lemma lprs_strip (h) (G): confluent2 … (lprs h G) (lpr h G).
+#h #G #L0 #L1 #HL01 #L2 #HL02
+elim (TC_strip1 … L1 ?? HL02) -HL02
+[ /3 width=3 by lprs_TC, ex2_intro/ | skip
+| /2 width=1 by lprs_inv_TC/
+| /2 width=3 by lpr_conf/
+]
+qed-.
(* *)
(**************************************************************************)
-include "basic_2/reduction/lpr_lpr.ma".
-include "basic_2/computation/lprs.ma".
+include "basic_2/rt_computation/cprs_cprs.ma".
+include "basic_2/rt_computation/lprs_cpms.ma".
-(* SN PARALLEL COMPUTATION ON LOCAL ENVIRONMENTS ****************************)
-
-(* Advanced properties ******************************************************)
-
-lemma lprs_strip: ∀G. confluent2 … (lprs G) (lpr G).
-/3 width=3 by TC_strip1, lpr_conf/ qed-.
+(* PARALLEL R-COMPUTATION FOR FULL LOCAL ENVIRONMENTS ***********************)
(* Main properties **********************************************************)
-theorem lprs_conf: ∀G. confluent2 … (lprs G) (lprs G).
-/3 width=3 by TC_confluent2, lpr_conf/ qed-.
+theorem lprs_trans (h) (G): Transitive … (lprs h G).
+/4 width=5 by lprs_cpms_trans, cprs_trans, lex_trans/ qed-.
-theorem lprs_trans: ∀G. Transitive … (lprs G).
-/2 width=3 by trans_TC/ qed-.
+theorem lprs_conf (h) (G): confluent2 … (lprs h G) (lprs h G).
+#h #G #L0 #L1 #HL01 #L2 #HL02
+elim (TC_confluent2 … L0 L1 … L2)
+[ /3 width=3 by lprs_TC, ex2_intro/ |5,6: skip
+| /2 width=1 by lprs_inv_TC/
+| /2 width=1 by lprs_inv_TC/
+| /2 width=3 by lpr_conf/
+]
+qed-.
--- /dev/null
+(**************************************************************************)
+(* ___ *)
+(* ||M|| *)
+(* ||A|| A project by Andrea Asperti *)
+(* ||T|| *)
+(* ||I|| Developers: *)
+(* ||T|| The HELM team. *)
+(* ||A|| http://helm.cs.unibo.it *)
+(* \ / *)
+(* \ / This file is distributed under the terms of the *)
+(* v GNU General Public License Version 2 *)
+(* *)
+(**************************************************************************)
+
+include "basic_2/relocation/lex_tc.ma".
+include "basic_2/rt_computation/lprs_ctc.ma".
+include "basic_2/rt_computation/cprs_lpr.ma".
+
+(* PARALLEL R-COMPUTATION FOR FULL LOCAL ENVIRONMENTS ***********************)
+
+(* Properties with transitive closure ***************************************)
+
+lemma lprs_TC (h) (G):
+ ∀L1,L2. TC … (lex (λL.cpm h G L 0)) L1 L2 → ⦃G, L1⦄⊢ ➡*[h] L2.
+/4 width=3 by lprs_CTC, lex_CTC, lpr_cprs_trans/ qed.
+
+(* Inversion lemmas with transitive closure *********************************)
+
+lemma lprs_inv_TC (h) (G):
+ ∀L1,L2. ⦃G, L1⦄⊢ ➡*[h] L2 → TC … (lex (λL.cpm h G L 0)) L1 L2.
+/3 width=3 by lprs_inv_CTC, lex_inv_CTC/ qed-.
lemma lpxs_inv_atom_sn (h) (G): ∀L2. ⦃G, ⋆⦄ ⊢ ⬈*[h] L2 → L2 = ⋆.
/2 width=2 by lex_inv_atom_sn/ qed-.
-lemma lpxs_inv_bind_sn (h) (G): ∀I1,L2,K1. ⦃G, K1.ⓘ{I1}⦄ ⊢⬈*[h] L2 →
- ∃∃I2,K2. ⦃G, K1⦄ ⊢⬈*[h] K2 & ⦃G, K1⦄ ⊢ I1 ⬈*[h] I2 & L2 = K2.ⓘ{I2}.
+lemma lpxs_inv_bind_sn (h) (G): ∀I1,L2,K1. ⦃G, K1.ⓘ{I1}⦄ ⊢ ⬈*[h] L2 →
+ ∃∃I2,K2. ⦃G, K1⦄ ⊢ ⬈*[h] K2 & ⦃G, K1⦄ ⊢ I1 ⬈*[h] I2 & L2 = K2.ⓘ{I2}.
/2 width=1 by lex_inv_bind_sn/ qed-.
(* Basic_2A1: was: lpxs_inv_pair1 *)
-lemma lpxs_inv_pair_sn (h) (G): ∀I,L2,K1,V1. ⦃G, K1.ⓑ{I}V1⦄ ⊢⬈*[h] L2 →
- ∃∃K2,V2. ⦃G, K1⦄ ⊢⬈*[h] K2 & ⦃G, K1⦄ ⊢ V1 ⬈*[h] V2 & L2 = K2.ⓑ{I}V2.
+lemma lpxs_inv_pair_sn (h) (G): ∀I,L2,K1,V1. ⦃G, K1.ⓑ{I}V1⦄ ⊢ ⬈*[h] L2 →
+ ∃∃K2,V2. ⦃G, K1⦄ ⊢ ⬈*[h] K2 & ⦃G, K1⦄ ⊢ V1 ⬈*[h] V2 & L2 = K2.ⓑ{I}V2.
/2 width=1 by lex_inv_pair_sn/ qed-.
(* Basic_2A1: was: lpxs_inv_atom2 *)
+++ /dev/null
-cpxs.ma cpxs_tdeq.ma cpxs_theq.ma cpxs_theq_vector.ma cpxs_drops.ma cpxs_fqus.ma cpxs_lsubr.ma cpxs_lfdeq.ma cpxs_ffdeq.ma cpxs_aaa.ma cpxs_lpx.ma cpxs_cnx.ma cpxs_cpxs.ma
-cpxs_ext.ma
-lpxs.ma lpxs_length.ma lpxs_drops.ma lpxs_lfdeq.ma lpxs_ffdeq.ma lpxs_aaa.ma lpxs_lpx.ma lpxs_cpxs.ma lpxs_lpxs.ma
-csx.ma csx_simple.ma csx_simple_theq.ma csx_drops.ma csx_fqus.ma csx_lsubr.ma csx_lfdeq.ma csx_ffdeq.ma csx_aaa.ma csx_gcp.ma csx_gcr.ma csx_lpx.ma csx_cnx.ma csx_fpbq.ma csx_cpxs.ma csx_lpxs.ma csx_csx.ma
-csx_vector.ma csx_cnx_vector.ma csx_csx_vector.ma
-rdsx.ma rdsx_length.ma rdsx_drops.ma rdsx_fqup.ma rdsx_lpxs.ma rdsx_csx.ma rdsx_rdsx.ma
-lsubsx.ma lsubsx_rdsx.ma lsubsx_lsubsx.ma
-fpbs.ma fpbs_fqup.ma fpbs_fqus.ma fpbs_aaa.ma fpbs_cpx.ma fpbs_fpb.ma fpbs_cpxs.ma fpbs_lpxs.ma fpbs_lpxs.ma fpbs_csx.ma fpbs_fpbs.ma
-fpbg.ma fpbg_fqup.ma fpbg_cpxs.ma fpbg_lpxs.ma fpbg_fpbs.ma fpbg_fpbg.ma
-fsb.ma fsb_ffdeq.ma fsb_aaa.ma fsb_csx.ma fsb_fpbg.ma
-cpms.ma cpms_drops.ma cpms_lsubr.ma cpms_aaa.ma cpms_lpr.ma cpms_cpxs.ma cpms_cpms.ma
-cprs.ma cprs_ctc.ma cprs_drops.ma cprs_cpr.ma cprs_lpr.ma cprs_cprs.ma
-cprs_ext.ma
-lprs.ma lprs_ctc.ma lprs_length.ma lprs_drops.ma lprs_aaa.ma lprs_lpr.ma lprs_lpxs.ma
<subsection name="A2">Stage "A2": "Extending the Applicability Condition"</subsection>
+ <news class="alpha" date="2018 June 8.">
+ Behavioral component rt_computation completed.
+ </news>
<news class="alpha" date="2018 April 16.">
"Big tree" theorem
(anniversary milestone).
(anniversary milestone).
</news>
<news class="alpha" date="2017 March 16.">
- First behavioral component completed:
- rt_transition.
+ Behavioral component rt_transition completed.
</news>
<news class="alpha" date="2017 February 19.">
Generic candidates of reducibility.
]
*)
[ { "context-sensitive parallel r-computation" * } {
- [ [ "for lenvs on all entries" ] "lprs ( ⦃?,?⦄ ⊢ ➡*[?] ? )" "lprs_ctc" + "lprs_length" + "lprs_drops" + "lprs_aaa" + "lprs_lpr" + "lprs_lpxs" (* + "lprs_cprs" + "lprs_lprs" *) * ]
+ [ [ "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" * ]
[ [ "for binders" ] "cprs_ext" + "( ⦃?,?⦄ ⊢ ? ➡*[?] ?)" * ]
[ [ "for terms" ] "cprs" + "( ⦃?,?⦄ ⊢ ? ➡*[?] ?)" "cprs_ctc" + "cprs_drops" + "cprs_cpr" + "cprs_lpr" + "cprs_cprs" * ]
}
../../matitac.opt `cat partial.txt`
-cd basic_2/rt_computation/
-../../../../matitac.opt `cat partial.txt`
-cd ../rt_equivalence/
+cd basic_2/rt_equivalence/
../../../../matitac.opt `cat partial.txt`
cd ../dynamic/
../../../../matitac.opt `cat partial.txt`
basic_2/static
basic_2/i_static
basic_2/rt_transition
+basic_2/rt_computation
basic_2/rt_conversion
apps_2/examples/ex_cpr_omega.ma
apps_2/models/
projects / helm.git / commitdiff