+++ /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/pconvstar_4.ma".
-include "basic_2/conversion/cpc.ma".
-
-(* CONTEXT-SENSITIVE PARALLEL EQUIVALENCE ON TERMS **************************)
-
-definition cpcs: relation4 genv lenv term term ≝
- λG. CTC … (cpc G).
-
-interpretation "context-sensitive parallel equivalence (term)"
- 'PConvStar G L T1 T2 = (cpcs G L T1 T2).
-
-(* Basic eliminators ********************************************************)
-
-lemma cpcs_ind: ∀G,L,T1. ∀R:predicate term. R T1 →
- (∀T,T2. ⦃G, L⦄ ⊢ T1 ⬌* T → ⦃G, L⦄ ⊢ T ⬌ T2 → R T → R T2) →
- ∀T2. ⦃G, L⦄ ⊢ T1 ⬌* T2 → R T2.
-normalize /3 width=6 by TC_star_ind/
-qed-.
-
-lemma cpcs_ind_dx: ∀G,L,T2. ∀R:predicate term. R T2 →
- (∀T1,T. ⦃G, L⦄ ⊢ T1 ⬌ T → ⦃G, L⦄ ⊢ T ⬌* T2 → R T → R T1) →
- ∀T1. ⦃G, L⦄ ⊢ T1 ⬌* T2 → R T1.
-normalize /3 width=6 by TC_star_ind_dx/
-qed-.
-
-(* Basic properties *********************************************************)
-
-(* Basic_1: was: pc3_refl *)
-lemma cpcs_refl: ∀G,L. reflexive … (cpcs G L).
-/2 width=1 by inj/ qed.
-
-(* Basic_1: was: pc3_s *)
-lemma cpcs_sym: ∀G,L. symmetric … (cpcs G L).
-normalize /3 width=1 by cpc_sym, TC_symmetric/
-qed-.
-
-lemma cpc_cpcs: ∀G,L,T1,T2. ⦃G, L⦄ ⊢ T1 ⬌ T2 → ⦃G, L⦄ ⊢ T1 ⬌* T2.
-/2 width=1 by inj/ qed.
-
-lemma cpcs_strap1: ∀G,L,T1,T,T2. ⦃G, L⦄ ⊢ T1 ⬌* T → ⦃G, L⦄ ⊢ T ⬌ T2 → ⦃G, L⦄ ⊢ T1 ⬌* T2.
-normalize /2 width=3 by step/
-qed-.
-
-lemma cpcs_strap2: ∀G,L,T1,T,T2. ⦃G, L⦄ ⊢ T1 ⬌ T → ⦃G, L⦄ ⊢ T ⬌* T2 → ⦃G, L⦄ ⊢ T1 ⬌* T2.
-normalize /2 width=3 by TC_strap/
-qed-.
-
-(* Basic_1: was: pc3_pr2_r *)
-lemma cpr_cpcs_dx: ∀G,L,T1,T2. ⦃G, L⦄ ⊢ T1 ➡ T2 → ⦃G, L⦄ ⊢ T1 ⬌* T2.
-/3 width=1 by cpc_cpcs, or_introl/ qed.
-
-(* Basic_1: was: pc3_pr2_x *)
-lemma cpr_cpcs_sn: ∀G,L,T1,T2. ⦃G, L⦄ ⊢ T2 ➡ T1 → ⦃G, L⦄ ⊢ T1 ⬌* T2.
-/3 width=1 by cpc_cpcs, or_intror/ qed.
-
-lemma cpcs_cpr_strap1: ∀G,L,T1,T. ⦃G, L⦄ ⊢ T1 ⬌* T → ∀T2. ⦃G, L⦄ ⊢ T ➡ T2 → ⦃G, L⦄ ⊢ T1 ⬌* T2.
-/3 width=3 by cpcs_strap1, or_introl/ qed-.
-
-(* Basic_1: was: pc3_pr2_u *)
-lemma cpcs_cpr_strap2: ∀G,L,T1,T. ⦃G, L⦄ ⊢ T1 ➡ T → ∀T2. ⦃G, L⦄ ⊢ T ⬌* T2 → ⦃G, L⦄ ⊢ T1 ⬌* T2.
-/3 width=3 by cpcs_strap2, or_introl/ qed-.
-
-lemma cpcs_cpr_div: ∀G,L,T1,T. ⦃G, L⦄ ⊢ T1 ⬌* T → ∀T2. ⦃G, L⦄ ⊢ T2 ➡ T → ⦃G, L⦄ ⊢ T1 ⬌* T2.
-/3 width=3 by cpcs_strap1, or_intror/ qed-.
-
-lemma cpr_div: ∀G,L,T1,T. ⦃G, L⦄ ⊢ T1 ➡ T → ∀T2. ⦃G, L⦄ ⊢ T2 ➡ T → ⦃G, L⦄ ⊢ T1 ⬌* T2.
-/3 width=3 by cpr_cpcs_dx, cpcs_strap1, or_intror/ qed-.
-
-(* Basic_1: was: pc3_pr2_u2 *)
-lemma cpcs_cpr_conf: ∀G,L,T1,T. ⦃G, L⦄ ⊢ T ➡ T1 → ∀T2. ⦃G, L⦄ ⊢ T ⬌* T2 → ⦃G, L⦄ ⊢ T1 ⬌* T2.
-/3 width=3 by cpcs_strap2, or_intror/ qed-.
-
-(* Basic_1: removed theorems 9:
- clear_pc3_trans pc3_ind_left
- pc3_head_1 pc3_head_2 pc3_head_12 pc3_head_21
- pc3_pr2_fqubst0 pc3_pr2_fqubst0_back pc3_fqubst0
- pc3_gen_abst pc3_gen_abst_shift
-*)
-(* Basic_1: removed local theorems 6:
- pc3_left_pr3 pc3_left_trans pc3_left_sym pc3_left_pc3 pc3_pc3_left
- pc3_wcpr0_t_aux
-*)
+++ /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/computation/cpxs_aaa.ma".
-include "basic_2/equivalence/cpcs_cpcs.ma".
-
-(* CONTEXT-SENSITIVE PARALLEL EQUIVALENCE ON TERMS **************************)
-
-(* Main inversion lemmas about atomic arity assignment on terms *************)
-
-theorem cpcs_aaa_mono: ∀G,L,T1,T2. ⦃G, L⦄ ⊢ T1 ⬌* T2 →
- ∀A1. ⦃G, L⦄ ⊢ T1 ⁝ A1 → ∀A2. ⦃G, L⦄ ⊢ T2 ⁝ A2 →
- A1 = A2.
-#G #L #T1 #T2 #HT12 #A1 #HA1 #A2 #HA2
-elim (cpcs_inv_cprs … HT12) -HT12 #T #HT1 #HT2
-lapply (cprs_aaa_conf … HA1 … HT1) -T1 #HA1
-lapply (cprs_aaa_conf … HA2 … HT2) -T2 #HA2
-lapply (aaa_mono … HA1 … HA2) -L -T //
-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/computation/lprs_cprs.ma".
-include "basic_2/conversion/cpc_cpc.ma".
-include "basic_2/equivalence/cpcs_cprs.ma".
-
-(* CONTEXT-SENSITIVE PARALLEL EQUIVALENCE ON TERMS **************************)
-
-(* Advanced inversion lemmas ************************************************)
-
-lemma cpcs_inv_cprs: ∀G,L,T1,T2. ⦃G, L⦄ ⊢ T1 ⬌* T2 →
- ∃∃T. ⦃G, L⦄ ⊢ T1 ➡* T & ⦃G, L⦄ ⊢ T2 ➡* T.
-#G #L #T1 #T2 #H @(cpcs_ind … H) -T2
-[ /3 width=3 by ex2_intro/
-| #T #T2 #_ #HT2 * #T0 #HT10 elim HT2 -HT2 #HT2 #HT0
- [ elim (cprs_strip … HT0 … HT2) -T /3 width=3 by cprs_strap1, ex2_intro/
- | /3 width=5 by cprs_strap2, ex2_intro/
- ]
-]
-qed-.
-
-(* Basic_1: was: pc3_gen_sort *)
-lemma cpcs_inv_sort: ∀G,L,s1,s2. ⦃G, L⦄ ⊢ ⋆s1 ⬌* ⋆s2 → s1 = s2.
-#G #L #s1 #s2 #H elim (cpcs_inv_cprs … H) -H
-#T #H1 >(cprs_inv_sort1 … H1) -T #H2
-lapply (cprs_inv_sort1 … H2) -L #H destruct //
-qed-.
-
-lemma cpcs_inv_abst1: ∀a,G,L,W1,T1,T. ⦃G, L⦄ ⊢ ⓛ{a}W1.T1 ⬌* T →
- ∃∃W2,T2. ⦃G, L⦄ ⊢ T ➡* ⓛ{a}W2.T2 & ⦃G, L⦄ ⊢ ⓛ{a}W1.T1 ➡* ⓛ{a}W2.T2.
-#a #G #L #W1 #T1 #T #H
-elim (cpcs_inv_cprs … H) -H #X #H1 #H2
-elim (cprs_inv_abst1 … H1) -H1 #W2 #T2 #HW12 #HT12 #H destruct
-/3 width=6 by cprs_bind, ex2_2_intro/
-qed-.
-
-lemma cpcs_inv_abst2: ∀a,G,L,W1,T1,T. ⦃G, L⦄ ⊢ T ⬌* ⓛ{a}W1.T1 →
- ∃∃W2,T2. ⦃G, L⦄ ⊢ T ➡* ⓛ{a}W2.T2 & ⦃G, L⦄ ⊢ ⓛ{a}W1.T1 ➡* ⓛ{a}W2.T2.
-/3 width=1 by cpcs_inv_abst1, cpcs_sym/ qed-.
-
-(* Basic_1: was: pc3_gen_sort_abst *)
-lemma cpcs_inv_sort_abst: ∀a,G,L,W,T,s. ⦃G, L⦄ ⊢ ⋆s ⬌* ⓛ{a}W.T → ⊥.
-#a #G #L #W #T #s #H
-elim (cpcs_inv_cprs … H) -H #X #H1
->(cprs_inv_sort1 … H1) -X #H2
-elim (cprs_inv_abst1 … H2) -H2 #W0 #T0 #_ #_ #H destruct
-qed-.
-
-(* Basic_1: was: pc3_gen_lift *)
-lemma cpcs_inv_lift: ∀G,L,K,b,l,k. ⬇[b, l, k] L ≘ K →
- ∀T1,U1. ⬆[l, k] T1 ≘ U1 → ∀T2,U2. ⬆[l, k] T2 ≘ U2 →
- ⦃G, L⦄ ⊢ U1 ⬌* U2 → ⦃G, K⦄ ⊢ T1 ⬌* T2.
-#G #L #K #b #l #k #HLK #T1 #U1 #HTU1 #T2 #U2 #HTU2 #HU12
-elim (cpcs_inv_cprs … HU12) -HU12 #U #HU1 #HU2
-elim (cprs_inv_lift1 … HU1 … HLK … HTU1) -U1 #T #HTU #HT1
-elim (cprs_inv_lift1 … HU2 … HLK … HTU2) -L -U2 #X #HXU
->(lift_inj … HXU … HTU) -X -U -l -k /2 width=3 by cprs_div/
-qed-.
-
-(* Advanced properties ******************************************************)
-
-lemma lpr_cpcs_trans: ∀G,L1,L2. ⦃G, L1⦄ ⊢ ➡ L2 →
- ∀T1,T2. ⦃G, L2⦄ ⊢ T1 ⬌* T2 → ⦃G, L1⦄ ⊢ T1 ⬌* T2.
-#G #L1 #L2 #HL12 #T1 #T2 #H elim (cpcs_inv_cprs … H) -H
-/4 width=5 by cprs_div, lpr_cprs_trans/
-qed-.
-
-lemma lprs_cpcs_trans: ∀G,L1,L2. ⦃G, L1⦄ ⊢ ➡* L2 →
- ∀T1,T2. ⦃G, L2⦄ ⊢ T1 ⬌* T2 → ⦃G, L1⦄ ⊢ T1 ⬌* T2.
-#G #L1 #L2 #HL12 #T1 #T2 #H elim (cpcs_inv_cprs … H) -H
-/4 width=5 by cprs_div, lprs_cprs_trans/
-qed-.
-
-lemma cpr_cprs_conf_cpcs: ∀G,L,T,T1,T2. ⦃G, L⦄ ⊢ T ➡* T1 → ⦃G, L⦄ ⊢ T ➡ T2 → ⦃G, L⦄ ⊢ T1 ⬌* T2.
-#G #L #T #T1 #T2 #HT1 #HT2 elim (cprs_strip … HT1 … HT2) -HT1 -HT2
-/2 width=3 by cpr_cprs_div/
-qed-.
-
-lemma cprs_cpr_conf_cpcs: ∀G,L,T,T1,T2. ⦃G, L⦄ ⊢ T ➡* T1 → ⦃G, L⦄ ⊢ T ➡ T2 → ⦃G, L⦄ ⊢ T2 ⬌* T1.
-#G #L #T #T1 #T2 #HT1 #HT2 elim (cprs_strip … HT1 … HT2) -HT1 -HT2
-/2 width=3 by cprs_cpr_div/
-qed-.
-
-lemma cprs_conf_cpcs: ∀G,L,T,T1,T2. ⦃G, L⦄ ⊢ T ➡* T1 → ⦃G, L⦄ ⊢ T ➡* T2 → ⦃G, L⦄ ⊢ T1 ⬌* T2.
-#G #L #T #T1 #T2 #HT1 #HT2 elim (cprs_conf … HT1 … HT2) -HT1 -HT2
-/2 width=3 by cprs_div/
-qed-.
-
-lemma lprs_cprs_conf: ∀G,L1,L2. ⦃G, L1⦄ ⊢ ➡* L2 →
- ∀T1,T2. ⦃G, L1⦄ ⊢ T1 ➡* T2 → ⦃G, L2⦄ ⊢ T1 ⬌* T2.
-#G #L1 #L2 #HL12 #T1 #T2 #HT12 elim (lprs_cprs_conf_dx … HT12 … HL12) -L1
-/2 width=3 by cprs_div/
-qed-.
-
-(* Basic_1: was: pc3_wcpr0_t *)
-(* Basic_1: note: pc3_wcpr0_t should be renamed *)
-(* Note: alternative proof /3 width=5 by lprs_cprs_conf, lpr_lprs/ *)
-lemma lpr_cprs_conf: ∀G,L1,L2. ⦃G, L1⦄ ⊢ ➡ L2 →
- ∀T1,T2. ⦃G, L1⦄ ⊢ T1 ➡* T2 → ⦃G, L2⦄ ⊢ T1 ⬌* T2.
-#G #L1 #L2 #HL12 #T1 #T2 #HT12 elim (cprs_lpr_conf_dx … HT12 … HL12) -L1
-/2 width=3 by cprs_div/
-qed-.
-
-(* Basic_1: was only: pc3_pr0_pr2_t *)
-(* Basic_1: note: pc3_pr0_pr2_t should be renamed *)
-lemma lpr_cpr_conf: ∀G,L1,L2. ⦃G, L1⦄ ⊢ ➡ L2 →
- ∀T1,T2. ⦃G, L1⦄ ⊢ T1 ➡ T2 → ⦃G, L2⦄ ⊢ T1 ⬌* T2.
-/3 width=5 by lpr_cprs_conf, cpr_cprs/ qed-.
-
-(* Basic_1: was only: pc3_thin_dx *)
-lemma cpcs_flat: ∀G,L,V1,V2. ⦃G, L⦄ ⊢ V1 ⬌* V2 → ∀T1,T2. ⦃G, L⦄ ⊢ T1 ⬌* T2 →
- ∀I. ⦃G, L⦄ ⊢ ⓕ{I}V1.T1 ⬌* ⓕ{I}V2.T2.
-#G #L #V1 #V2 #HV12 #T1 #T2 #HT12
-elim (cpcs_inv_cprs … HV12) -HV12
-elim (cpcs_inv_cprs … HT12) -HT12
-/3 width=5 by cprs_flat, cprs_div/
-qed.
-
-lemma cpcs_flat_dx_cpr_rev: ∀G,L,V1,V2. ⦃G, L⦄ ⊢ V2 ➡ V1 → ∀T1,T2. ⦃G, L⦄ ⊢ T1 ⬌* T2 →
- ∀I. ⦃G, L⦄ ⊢ ⓕ{I}V1.T1 ⬌* ⓕ{I}V2.T2.
-/3 width=1 by cpr_cpcs_sn, cpcs_flat/ qed.
-
-lemma cpcs_bind_dx: ∀a,I,G,L,V,T1,T2. ⦃G, L.ⓑ{I}V⦄ ⊢ T1 ⬌* T2 →
- ⦃G, L⦄ ⊢ ⓑ{a,I}V.T1 ⬌* ⓑ{a,I}V.T2.
-#a #I #G #L #V #T1 #T2 #HT12 elim (cpcs_inv_cprs … HT12) -HT12
-/3 width=5 by cprs_div, cprs_bind/
-qed.
-
-lemma cpcs_bind_sn: ∀a,I,G,L,V1,V2,T. ⦃G, L⦄ ⊢ V1 ⬌* V2 → ⦃G, L⦄ ⊢ ⓑ{a,I}V1. T ⬌* ⓑ{a,I}V2. T.
-#a #I #G #L #V1 #V2 #T #HV12 elim (cpcs_inv_cprs … HV12) -HV12
-/3 width=5 by cprs_div, cprs_bind/
-qed.
-
-lemma lsubr_cpcs_trans: ∀G,L1,T1,T2. ⦃G, L1⦄ ⊢ T1 ⬌* T2 →
- ∀L2. L2 ⫃ L1 → ⦃G, L2⦄ ⊢ T1 ⬌* T2.
-#G #L1 #T1 #T2 #HT12 elim (cpcs_inv_cprs … HT12) -HT12
-/3 width=5 by cprs_div, lsubr_cprs_trans/
-qed-.
-
-(* Basic_1: was: pc3_lift *)
-lemma cpcs_lift: ∀G,L,K,b,l,k. ⬇[b, l, k] L ≘ K →
- ∀T1,U1. ⬆[l, k] T1 ≘ U1 → ∀T2,U2. ⬆[l, k] T2 ≘ U2 →
- ⦃G, K⦄ ⊢ T1 ⬌* T2 → ⦃G, L⦄ ⊢ U1 ⬌* U2.
-#G #L #K #b #l #k #HLK #T1 #U1 #HTU1 #T2 #U2 #HTU2 #HT12
-elim (cpcs_inv_cprs … HT12) -HT12 #T #HT1 #HT2
-elim (lift_total T l k) /3 width=12 by cprs_div, cprs_lift/
-qed.
-
-lemma cpcs_strip: ∀G,L,T1,T. ⦃G, L⦄ ⊢ T ⬌* T1 → ∀T2. ⦃G, L⦄ ⊢ T ⬌ T2 →
- ∃∃T0. ⦃G, L⦄ ⊢ T1 ⬌ T0 & ⦃G, L⦄ ⊢ T2 ⬌* T0.
-#G #L #T1 #T @TC_strip1 /2 width=3 by cpc_conf/ qed-.
-
-(* More inversion lemmas ****************************************************)
-
-(* Note: there must be a proof suitable for llpr *)
-lemma cpcs_inv_abst_sn: ∀a1,a2,G,L,W1,W2,T1,T2. ⦃G, L⦄ ⊢ ⓛ{a1}W1.T1 ⬌* ⓛ{a2}W2.T2 →
- ∧∧ ⦃G, L⦄ ⊢ W1 ⬌* W2 & ⦃G, L.ⓛW1⦄ ⊢ T1 ⬌* T2 & a1 = a2.
-#a1 #a2 #G #L #W1 #W2 #T1 #T2 #H
-elim (cpcs_inv_cprs … H) -H #T #H1 #H2
-elim (cprs_inv_abst1 … H1) -H1 #W0 #T0 #HW10 #HT10 #H destruct
-elim (cprs_inv_abst1 … H2) -H2 #W #T #HW2 #HT2 #H destruct
-lapply (lprs_cprs_conf … (L.ⓛW) … HT2) /2 width=1 by lprs_pair/ -HT2 #HT2
-lapply (lprs_cpcs_trans … (L.ⓛW1) … HT2) /2 width=1 by lprs_pair/ -HT2 #HT2
-/4 width=3 by and3_intro, cprs_div, cpcs_cprs_div, cpcs_sym/
-qed-.
-
-lemma cpcs_inv_abst_dx: ∀a1,a2,G,L,W1,W2,T1,T2. ⦃G, L⦄ ⊢ ⓛ{a1}W1.T1 ⬌* ⓛ{a2}W2.T2 →
- ∧∧ ⦃G, L⦄ ⊢ W1 ⬌* W2 & ⦃G, L.ⓛW2⦄ ⊢ T1 ⬌* T2 & a1 = a2.
-#a1 #a2 #G #L #W1 #W2 #T1 #T2 #HT12 lapply (cpcs_sym … HT12) -HT12
-#HT12 elim (cpcs_inv_abst_sn … HT12) -HT12 /3 width=1 by cpcs_sym, and3_intro/
-qed-.
-
-(* Main properties **********************************************************)
-
-(* Basic_1: was pc3_t *)
-theorem cpcs_trans: ∀G,L,T1,T. ⦃G, L⦄ ⊢ T1 ⬌* T → ∀T2. ⦃G, L⦄ ⊢ T ⬌* T2 → ⦃G, L⦄ ⊢ T1 ⬌* T2.
-#G #L #T1 #T #HT1 #T2 @(trans_TC … HT1) qed-.
-
-theorem cpcs_canc_sn: ∀G,L,T,T1,T2. ⦃G, L⦄ ⊢ T ⬌* T1 → ⦃G, L⦄ ⊢ T ⬌* T2 → ⦃G, L⦄ ⊢ T1 ⬌* T2.
-/3 width=3 by cpcs_trans, cpcs_sym/ qed-.
-
-theorem cpcs_canc_dx: ∀G,L,T,T1,T2. ⦃G, L⦄ ⊢ T1 ⬌* T → ⦃G, L⦄ ⊢ T2 ⬌* T → ⦃G, L⦄ ⊢ T1 ⬌* T2.
-/3 width=3 by cpcs_trans, cpcs_sym/ qed-.
-
-lemma cpcs_bind1: ∀a,I,G,L,V1,V2. ⦃G, L⦄ ⊢ V1 ⬌* V2 →
- ∀T1,T2. ⦃G, L.ⓑ{I}V1⦄ ⊢ T1 ⬌* T2 →
- ⦃G, L⦄ ⊢ ⓑ{a,I}V1. T1 ⬌* ⓑ{a,I}V2. T2.
-/3 width=3 by cpcs_trans, cpcs_bind_sn, cpcs_bind_dx/ qed.
-
-lemma cpcs_bind2: ∀a,I,G,L,V1,V2. ⦃G, L⦄ ⊢ V1 ⬌* V2 →
- ∀T1,T2. ⦃G, L.ⓑ{I}V2⦄ ⊢ T1 ⬌* T2 →
- ⦃G, L⦄ ⊢ ⓑ{a,I}V1. T1 ⬌* ⓑ{a,I}V2. T2.
-/3 width=3 by cpcs_trans, cpcs_bind_sn, cpcs_bind_dx/ qed.
-
-(* Basic_1: was: pc3_wcpr0 *)
-lemma lpr_cpcs_conf: ∀G,L1,L2. ⦃G, L1⦄ ⊢ ➡ L2 →
- ∀T1,T2. ⦃G, L1⦄ ⊢ T1 ⬌* T2 → ⦃G, L2⦄ ⊢ T1 ⬌* T2.
-#G #L1 #L2 #HL12 #T1 #T2 #H elim (cpcs_inv_cprs … H) -H
-/3 width=5 by cpcs_canc_dx, lpr_cprs_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/computation/cprs.ma".
-include "basic_2/equivalence/cpcs.ma".
-
-(* CONTEXT-SENSITIVE PARALLEL EQUIVALENCE ON TERMS **************************)
-
-(* Properties about context sensitive computation on terms ******************)
-
-(* Basic_1: was: pc3_pr3_r *)
-lemma cpcs_cprs_dx: ∀G,L,T1,T2. ⦃G, L⦄ ⊢ T1 ➡* T2 → ⦃G, L⦄ ⊢ T1 ⬌* T2.
-#G #L #T1 #T2 #H @(cprs_ind … H) -T2
-/3 width=3 by cpcs_cpr_strap1, cpcs_strap1, cpc_cpcs/
-qed.
-
-(* Basic_1: was: pc3_pr3_x *)
-lemma cpcs_cprs_sn: ∀G,L,T1,T2. ⦃G, L⦄ ⊢ T2 ➡* T1 → ⦃G, L⦄ ⊢ T1 ⬌* T2.
-#G #L #T1 #T2 #H @(cprs_ind_dx … H) -T2
-/3 width=3 by cpcs_cpr_div, cpcs_strap1, cpcs_cprs_dx/
-qed.
-
-lemma cpcs_cprs_strap1: ∀G,L,T1,T. ⦃G, L⦄ ⊢ T1 ⬌* T → ∀T2. ⦃G, L⦄ ⊢ T ➡* T2 → ⦃G, L⦄ ⊢ T1 ⬌* T2.
-#G #L #T1 #T #HT1 #T2 #H @(cprs_ind … H) -T2 /2 width=3 by cpcs_cpr_strap1/
-qed-.
-
-lemma cpcs_cprs_strap2: ∀G,L,T1,T. ⦃G, L⦄ ⊢ T1 ➡* T → ∀T2. ⦃G, L⦄ ⊢ T ⬌* T2 → ⦃G, L⦄ ⊢ T1 ⬌* T2.
-#G #L #T1 #T #H #T2 #HT2 @(cprs_ind_dx … H) -T1 /2 width=3 by cpcs_cpr_strap2/
-qed-.
-
-lemma cpcs_cprs_div: ∀G,L,T1,T. ⦃G, L⦄ ⊢ T1 ⬌* T → ∀T2. ⦃G, L⦄ ⊢ T2 ➡* T → ⦃G, L⦄ ⊢ T1 ⬌* T2.
-#G #L #T1 #T #HT1 #T2 #H @(cprs_ind_dx … H) -T2 /2 width=3 by cpcs_cpr_div/
-qed-.
-
-(* Basic_1: was: pc3_pr3_conf *)
-lemma cpcs_cprs_conf: ∀G,L,T1,T. ⦃G, L⦄ ⊢ T ➡* T1 → ∀T2. ⦃G, L⦄ ⊢ T ⬌* T2 → ⦃G, L⦄ ⊢ T1 ⬌* T2.
-#G #L #T1 #T #H #T2 #HT2 @(cprs_ind … H) -T1 /2 width=3 by cpcs_cpr_conf/
-qed-.
-
-(* Basic_1: was: pc3_pr3_t *)
-(* Basic_1: note: pc3_pr3_t should be renamed *)
-lemma cprs_div: ∀G,L,T1,T. ⦃G, L⦄ ⊢ T1 ➡* T → ∀T2. ⦃G, L⦄ ⊢ T2 ➡* T → ⦃G, L⦄ ⊢ T1 ⬌* T2.
-#G #L #T1 #T #HT1 #T2 #H @(cprs_ind_dx … H) -T2
-/2 width=3 by cpcs_cpr_div, cpcs_cprs_dx/
-qed.
-
-lemma cprs_cpr_div: ∀G,L,T1,T. ⦃G, L⦄ ⊢ T1 ➡* T → ∀T2. ⦃G, L⦄ ⊢ T2 ➡ T → ⦃G, L⦄ ⊢ T1 ⬌* T2.
-/3 width=5 by cpr_cprs, cprs_div/ qed-.
-
-lemma cpr_cprs_div: ∀G,L,T1,T. ⦃G, L⦄ ⊢ T1 ➡ T → ∀T2. ⦃G, L⦄ ⊢ T2 ➡* T → ⦃G, L⦄ ⊢ T1 ⬌* T2.
-/3 width=3 by cpr_cprs, cprs_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/notation/relations/dpconvstar_8.ma".
-include "basic_2/computation/scpds.ma".
-
-(* STRATIFIED DECOMPOSED PARALLEL EQUIVALENCE FOR TERMS *********************)
-
-definition scpes: ∀h. sd h → nat → nat → relation4 genv lenv term term ≝
- λh,o,d1,d2,G,L,T1,T2.
- ∃∃T. ⦃G, L⦄ ⊢ T1 •*➡*[h, o, d1] T & ⦃G, L⦄ ⊢ T2 •*➡*[h, o, d2] T.
-
-interpretation "stratified decomposed parallel equivalence (term)"
- 'DPConvStar h o d1 d2 G L T1 T2 = (scpes h o d1 d2 G L T1 T2).
-
-(* Basic properties *********************************************************)
-
-lemma scpds_div: ∀h,o,G,L,T1,T2,T,d1,d2.
- ⦃G, L⦄ ⊢ T1 •*➡*[h, o, d1] T → ⦃G, L⦄ ⊢ T2 •*➡*[h, o, d2] T →
- ⦃G, L⦄ ⊢ T1 •*⬌*[h, o, d1, d2] T2.
-/2 width=3 by ex2_intro/ qed.
-
-lemma scpes_sym: ∀h,o,G,L,T1,T2,d1,d2. ⦃G, L⦄ ⊢ T1 •*⬌*[h, o, d1, d2] T2 →
- ⦃G, L⦄ ⊢ T2 •*⬌*[h, o, d2, d1] T1.
-#h #o #G #L #T1 #T2 #L1 #d2 * /2 width=3 by scpds_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/computation/scpds_aaa.ma".
-include "basic_2/equivalence/scpes.ma".
-
-(* DECOMPOSED EXTENDED PARALLEL EQUIVALENCE FOR TERMS ***********************)
-
-(* Main inversion lemmas about atomic arity assignment on terms *************)
-
-theorem scpes_aaa_mono: ∀h,o,G,L,T1,T2,d1,d2. ⦃G, L⦄ ⊢ T1 •*⬌*[h, o, d1, d2] T2 →
- ∀A1. ⦃G, L⦄ ⊢ T1 ⁝ A1 → ∀A2. ⦃G, L⦄ ⊢ T2 ⁝ A2 →
- A1 = A2.
-#h #o #G #L #T1 #T2 #d1 #d2 * #T #HT1 #HT2 #A1 #HA1 #A2 #HA2
-lapply (scpds_aaa_conf … HA1 … HT1) -T1 #HA1
-lapply (scpds_aaa_conf … HA2 … HT2) -T2 #HA2
-lapply (aaa_mono … HA1 … HA2) -L -T //
-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/computation/scpds_scpds.ma".
-include "basic_2/equivalence/cpcs_cpcs.ma".
-include "basic_2/equivalence/scpes.ma".
-
-(* STRATIFIED DECOMPOSED PARALLEL EQUIVALENCE FOR TERMS *********************)
-
-(* Inversion lemmas on parallel equivalence for terms ***********************)
-
-lemma scpes_inv_lstas_eq: ∀h,o,G,L,T1,T2,d1,d2. ⦃G, L⦄ ⊢ T1 •*⬌*[h, o, d1, d2] T2 →
- ∀U1. ⦃G, L⦄ ⊢ T1 •*[h, d1] U1 →
- ∀U2. ⦃G, L⦄ ⊢ T2 •*[h, d2] U2 → ⦃G, L⦄ ⊢ U1 ⬌* U2.
-#h #o #G #L #T1 #T2 #d1 #d2 * #T #HT1 #HT2 #U1 #HTU1 #U2 #HTU2
-/3 width=8 by scpds_inv_lstas_eq, cprs_div/
-qed-.
-
-(* Properties on parallel equivalence for terms *****************************)
-
-lemma cpcs_scpes: ∀h,o,G,L,T1,d11. ⦃G, L⦄ ⊢ T1 ▪[h, o] d11 →
- ∀U1,d12. d12 ≤ d11 → ⦃G, L⦄ ⊢ T1 •*[h, d12] U1 →
- ∀T2,d21. ⦃G, L⦄ ⊢ T2 ▪[h, o] d21 →
- ∀U2,d22. d22 ≤ d21 → ⦃G, L⦄ ⊢ T2 •*[h, d22] U2 →
- ⦃G, L⦄ ⊢ U1 ⬌* U2 → ⦃G, L⦄ ⊢ T1 •*⬌*[h, o, d12, d22] T2.
-#h #o #G #L #T1 #d11 #HT1 #U1 #d12 #Hd121 #HTU1 #T2 #d21 #HT2 #U2 #d22 #Hd221 #HTU2 #HU12
-elim (cpcs_inv_cprs … HU12) -HU12 /3 width=6 by scpds_div, ex4_2_intro/
-qed.
+++ /dev/null
-(**************************************************************************)
-(* ___ *)
-(* ||M|| *)
-(* ||A|| A project by Andrea Asperti *)
-(* ||T|| *)
-(* ||I|| Developers: *)
-(* ||T|| The HELM team. *)
-(* ||A|| http://helm.cs.unibo.it *)
-(* \ / *)
-(* \ / This file is distributed under the terms of the *)
-(* v GNU General Public License Version 2 *)
-(* *)
-(**************************************************************************)
-
-include "basic_2/computation/scpds_scpds.ma".
-include "basic_2/equivalence/scpes.ma".
-
-(* STRATIFIED DECOMPOSED PARALLEL EQUIVALENCE FOR TERMS *********************)
-
-(* Advanced inversion lemmas ************************************************)
-
-lemma scpes_inv_abst2: ∀h,o,a,G,L,T1,T2,W2,d1,d2. ⦃G, L⦄ ⊢ T1 •*⬌*[h, o, d1, d2] ⓛ{a}W2.T2 →
- ∃∃W,T. ⦃G, L⦄ ⊢ T1 •*➡*[h, o, d1] ⓛ{a}W.T & ⦃G, L⦄ ⊢ W2 ➡* W &
- ⦃G, L.ⓛW2⦄ ⊢ T2 •*➡*[h, o, d2] T.
-#h #o #a #G #L #T1 #T2 #W2 #d1 #d2 * #T0 #HT10 #H
-elim (scpds_inv_abst1 … H) -H #W #T #HW2 #HT2 #H destruct /2 width=5 by ex3_2_intro/
-qed-.
-
-(* Advanced properties ******************************************************)
-
-lemma scpes_refl: ∀h,o,G,L,T,d1,d2. d2 ≤ d1 → ⦃G, L⦄ ⊢ T ▪[h, o] d1 →
- ⦃G, L⦄ ⊢ T •*⬌*[h, o, d2, d2] T.
-#h #o #G #L #T #d1 #d2 #Hd21 #Hd1
-elim (da_lstas … Hd1 … d2) #U #HTU #_
-/3 width=3 by scpds_div, lstas_scpds/
-qed.
-
-lemma lstas_scpes_trans: ∀h,o,G,L,T1,d0,d1. ⦃G, L⦄ ⊢ T1 ▪[h, o] d0 → d1 ≤ d0 →
- ∀T. ⦃G, L⦄ ⊢ T1 •*[h, d1] T →
- ∀T2,d,d2. ⦃G, L⦄ ⊢ T •*⬌*[h,o,d,d2] T2 → ⦃G, L⦄ ⊢ T1 •*⬌*[h,o,d1+d,d2] T2.
-#h #o #G #L #T1 #d0 #d1 #Hd0 #Hd10 #T #HT1 #T2 #d #d2 *
-/3 width=3 by scpds_div, lstas_scpds_trans/ qed-.
-
-(* Properties on parallel computation for terms *****************************)
-
-lemma cprs_scpds_div: ∀h,o,G,L,T1,T. ⦃G, L⦄ ⊢ T1 ➡* T →
- ∀d. ⦃G, L⦄ ⊢ T1 ▪[h, o] d →
- ∀T2,d2. ⦃G, L⦄ ⊢ T2 •*➡*[h, o, d2] T →
- ⦃G, L⦄⊢ T1 •*⬌*[h, o, 0, d2] T2.
-#h #o #G #L #T1 #T #HT1 #d #Hd elim (da_lstas … Hd 0)
-#X1 #HTX1 #_ elim (cprs_strip … HT1 X1) -HT1
-/3 width=5 by scpds_strap1, scpds_div, lstas_cpr, ex4_2_intro/
-qed.
-
-(* Main properties **********************************************************)
-
-theorem scpes_trans: ∀h,o,G,L,T1,T,d1,d. ⦃G, L⦄ ⊢ T1 •*⬌*[h, o, d1, d] T →
- ∀T2,d2. ⦃G, L⦄ ⊢ T •*⬌*[h, o, d, d2] T2 → ⦃G, L⦄ ⊢ T1 •*⬌*[h, o, d1, d2] T2.
-#h #o #G #L #T1 #T #d1 #d * #X1 #HT1X1 #HTX1 #T2 #d2 * #X2 #HTX2 #HT2X2
-elim (scpds_conf_eq … HTX1 … HTX2) -T -d /3 width=5 by scpds_cprs_trans, scpds_div/
-qed-.
-
-theorem scpes_canc_sn: ∀h,o,G,L,T,T1,d,d1. ⦃G, L⦄ ⊢ T •*⬌*[h, o, d, d1] T1 →
- ∀T2,d2. ⦃G, L⦄ ⊢ T •*⬌*[h, o, d, d2] T2 → ⦃G, L⦄ ⊢ T1 •*⬌*[h, o, d1, d2] T2.
-/3 width=4 by scpes_trans, scpes_sym/ qed-.
-
-theorem scpes_canc_dx: ∀h,o,G,L,T1,T,d1,d. ⦃G, L⦄ ⊢ T1 •*⬌*[h, o, d1, d] T →
- ∀T2,d2. ⦃G, L⦄ ⊢ T2 •*⬌*[h, o, d2, d] T → ⦃G, L⦄ ⊢ T1 •*⬌*[h, o, d1, d2] T2.
-/3 width=4 by scpes_trans, scpes_sym/ qed-.
(* 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 )"
+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 @{ 'PConv $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 T2 )"
- non associative with precedence 45
- for @{ 'PConvStar $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 @{ 'PConvStar $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 "ground_2/lib/star.ma".
+include "basic_2/notation/relations/pconvstar_5.ma".
+include "basic_2/rt_conversion/cpc.ma".
+
+(* CONTEXT-SENSITIVE PARALLEL R-EQUIVALENCE FOR TERMS ***********************)
+
+definition cpcs: sh → relation4 genv lenv term term ≝
+ λh,G. CTC … (cpc h G).
+
+interpretation "context-sensitive parallel r-equivalence (term)"
+ 'PConvStar h G L T1 T2 = (cpcs h G L T1 T2).
+
+(* Basic eliminators ********************************************************)
+
+(* Basic_2A1: was: cpcs_ind_dx *)
+lemma cpcs_ind_sn (h): ∀G,L,T2. ∀R:predicate term. R T2 →
+ (∀T1,T. ⦃G, L⦄ ⊢ T1 ⬌[h] T → ⦃G, L⦄ ⊢ T ⬌*[h] T2 → R T → R T1) →
+ ∀T1. ⦃G, L⦄ ⊢ T1 ⬌*[h] T2 → R T1.
+normalize /3 width=6 by TC_star_ind_dx/
+qed-.
+
+(* Basic_2A1: was: cpcs_ind *)
+lemma cpcs_ind_dx (h): ∀G,L,T1. ∀R:predicate term. R T1 →
+ (∀T,T2. ⦃G, L⦄ ⊢ T1 ⬌*[h] T → ⦃G, L⦄ ⊢ T ⬌[h] T2 → R T → R T2) →
+ ∀T2. ⦃G, L⦄ ⊢ T1 ⬌*[h] T2 → R T2.
+normalize /3 width=6 by TC_star_ind/
+qed-.
+
+(* Basic properties *********************************************************)
+
+(* Basic_1: was: pc3_refl *)
+lemma cpcs_refl (h): ∀G. c_reflexive … (cpcs h G).
+/2 width=1 by inj/ qed.
+
+(* Basic_1: was: pc3_s *)
+lemma cpcs_sym (h): ∀G,L. symmetric … (cpcs h G L).
+#h #G #L @TC_symmetric
+/2 width=1 by cpc_sym/
+qed-.
+
+lemma cpc_cpcs (h): ∀G,L,T1,T2. ⦃G, L⦄ ⊢ T1 ⬌[h] T2 → ⦃G, L⦄ ⊢ T1 ⬌*[h] T2.
+/2 width=1 by inj/ qed.
+
+(* Basic_2A1: was: cpcs_strap2 *)
+lemma cpcs_step_sn (h): ∀G,L,T1,T,T2. ⦃G, L⦄ ⊢ T1 ⬌[h] T → ⦃G, L⦄ ⊢ T ⬌*[h] T2 → ⦃G, L⦄ ⊢ T1 ⬌*[h] T2.
+normalize /2 width=3 by TC_strap/
+qed-.
+
+(* Basic_2A1: was: cpcs_strap1 *)
+lemma cpcs_step_dx (h): ∀G,L,T1,T,T2. ⦃G, L⦄ ⊢ T1 ⬌*[h] T → ⦃G, L⦄ ⊢ T ⬌[h] T2 → ⦃G, L⦄ ⊢ T1 ⬌*[h] T2.
+normalize /2 width=3 by step/
+qed-.
+
+(* Basic_1: was: pc3_pr2_r *)
+lemma cpr_cpcs_dx (h): ∀G,L,T1,T2. ⦃G, L⦄ ⊢ T1 ➡[h] T2 → ⦃G, L⦄ ⊢ T1 ⬌*[h] T2.
+/3 width=1 by cpc_cpcs, or_introl/ qed.
+
+(* Basic_1: was: pc3_pr2_x *)
+lemma cpr_cpcs_sn (h): ∀G,L,T1,T2. ⦃G, L⦄ ⊢ T2 ➡[h] T1 → ⦃G, L⦄ ⊢ T1 ⬌*[h] T2.
+/3 width=1 by cpc_cpcs, or_intror/ qed.
+
+(* Basic_1: was: pc3_pr2_u *)
+(* Basic_2A1: was: cpcs_cpr_strap2 *)
+lemma cpcs_cpr_step_sn (h): ∀G,L,T1,T. ⦃G, L⦄ ⊢ T1 ➡[h] T → ∀T2. ⦃G, L⦄ ⊢ T ⬌*[h] T2 → ⦃G, L⦄ ⊢ T1 ⬌*[h] T2.
+/3 width=3 by cpcs_step_sn, or_introl/ qed-.
+
+(* Basic_2A1: was: cpcs_cpr_strap1 *)
+lemma cpcs_cpr_step_dx (h): ∀G,L,T1,T. ⦃G, L⦄ ⊢ T1 ⬌*[h] T → ∀T2. ⦃G, L⦄ ⊢ T ➡[h] T2 → ⦃G, L⦄ ⊢ T1 ⬌*[h] T2.
+/3 width=3 by cpcs_step_dx, or_introl/ qed-.
+
+lemma cpcs_cpr_div (h): ∀G,L,T1,T. ⦃G, L⦄ ⊢ T1 ⬌*[h] T → ∀T2. ⦃G, L⦄ ⊢ T2 ➡[h] T → ⦃G, L⦄ ⊢ T1 ⬌*[h] T2.
+/3 width=3 by cpcs_step_dx, or_intror/ qed-.
+
+lemma cpr_div (h): ∀G,L,T1,T. ⦃G, L⦄ ⊢ T1 ➡[h] T → ∀T2. ⦃G, L⦄ ⊢ T2 ➡[h] T → ⦃G, L⦄ ⊢ T1 ⬌*[h] T2.
+/3 width=3 by cpr_cpcs_dx, cpcs_step_dx, or_intror/ qed-.
+
+(* Basic_1: was: pc3_pr2_u2 *)
+lemma cpcs_cpr_conf (h): ∀G,L,T1,T. ⦃G, L⦄ ⊢ T ➡[h] T1 → ∀T2. ⦃G, L⦄ ⊢ T ⬌*[h] T2 → ⦃G, L⦄ ⊢ T1 ⬌*[h] T2.
+/3 width=3 by cpcs_step_sn, or_intror/ qed-.
+
+(* Basic_1: removed theorems 9:
+ clear_pc3_trans pc3_ind_left
+ pc3_head_1 pc3_head_2 pc3_head_12 pc3_head_21
+ pc3_pr2_fqubst0 pc3_pr2_fqubst0_back pc3_fqubst0
+ pc3_gen_abst pc3_gen_abst_shift
+*)
+(* Basic_1: removed local theorems 6:
+ pc3_left_pr3 pc3_left_trans pc3_left_sym pc3_left_pc3 pc3_pc3_left
+ pc3_wcpr0_t_aux
+*)
--- /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/computation/cpxs_aaa.ma".
+include "basic_2/equivalence/cpcs_cpcs.ma".
+
+(* CONTEXT-SENSITIVE PARALLEL EQUIVALENCE ON TERMS **************************)
+
+(* Main inversion lemmas about atomic arity assignment on terms *************)
+
+theorem cpcs_aaa_mono: ∀G,L,T1,T2. ⦃G, L⦄ ⊢ T1 ⬌* T2 →
+ ∀A1. ⦃G, L⦄ ⊢ T1 ⁝ A1 → ∀A2. ⦃G, L⦄ ⊢ T2 ⁝ A2 →
+ A1 = A2.
+#G #L #T1 #T2 #HT12 #A1 #HA1 #A2 #HA2
+elim (cpcs_inv_cprs … HT12) -HT12 #T #HT1 #HT2
+lapply (cprs_aaa_conf … HA1 … HT1) -T1 #HA1
+lapply (cprs_aaa_conf … HA2 … HT2) -T2 #HA2
+lapply (aaa_mono … HA1 … HA2) -L -T //
+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/computation/lprs_cprs.ma".
+include "basic_2/conversion/cpc_cpc.ma".
+include "basic_2/equivalence/cpcs_cprs.ma".
+
+(* CONTEXT-SENSITIVE PARALLEL EQUIVALENCE ON TERMS **************************)
+
+(* Advanced inversion lemmas ************************************************)
+
+lemma cpcs_inv_cprs: ∀G,L,T1,T2. ⦃G, L⦄ ⊢ T1 ⬌* T2 →
+ ∃∃T. ⦃G, L⦄ ⊢ T1 ➡* T & ⦃G, L⦄ ⊢ T2 ➡* T.
+#G #L #T1 #T2 #H @(cpcs_ind … H) -T2
+[ /3 width=3 by ex2_intro/
+| #T #T2 #_ #HT2 * #T0 #HT10 elim HT2 -HT2 #HT2 #HT0
+ [ elim (cprs_strip … HT0 … HT2) -T /3 width=3 by cprs_strap1, ex2_intro/
+ | /3 width=5 by cprs_strap2, ex2_intro/
+ ]
+]
+qed-.
+
+(* Basic_1: was: pc3_gen_sort *)
+lemma cpcs_inv_sort: ∀G,L,s1,s2. ⦃G, L⦄ ⊢ ⋆s1 ⬌* ⋆s2 → s1 = s2.
+#G #L #s1 #s2 #H elim (cpcs_inv_cprs … H) -H
+#T #H1 >(cprs_inv_sort1 … H1) -T #H2
+lapply (cprs_inv_sort1 … H2) -L #H destruct //
+qed-.
+
+lemma cpcs_inv_abst1: ∀a,G,L,W1,T1,T. ⦃G, L⦄ ⊢ ⓛ{a}W1.T1 ⬌* T →
+ ∃∃W2,T2. ⦃G, L⦄ ⊢ T ➡* ⓛ{a}W2.T2 & ⦃G, L⦄ ⊢ ⓛ{a}W1.T1 ➡* ⓛ{a}W2.T2.
+#a #G #L #W1 #T1 #T #H
+elim (cpcs_inv_cprs … H) -H #X #H1 #H2
+elim (cprs_inv_abst1 … H1) -H1 #W2 #T2 #HW12 #HT12 #H destruct
+/3 width=6 by cprs_bind, ex2_2_intro/
+qed-.
+
+lemma cpcs_inv_abst2: ∀a,G,L,W1,T1,T. ⦃G, L⦄ ⊢ T ⬌* ⓛ{a}W1.T1 →
+ ∃∃W2,T2. ⦃G, L⦄ ⊢ T ➡* ⓛ{a}W2.T2 & ⦃G, L⦄ ⊢ ⓛ{a}W1.T1 ➡* ⓛ{a}W2.T2.
+/3 width=1 by cpcs_inv_abst1, cpcs_sym/ qed-.
+
+(* Basic_1: was: pc3_gen_sort_abst *)
+lemma cpcs_inv_sort_abst: ∀a,G,L,W,T,s. ⦃G, L⦄ ⊢ ⋆s ⬌* ⓛ{a}W.T → ⊥.
+#a #G #L #W #T #s #H
+elim (cpcs_inv_cprs … H) -H #X #H1
+>(cprs_inv_sort1 … H1) -X #H2
+elim (cprs_inv_abst1 … H2) -H2 #W0 #T0 #_ #_ #H destruct
+qed-.
+
+(* Basic_1: was: pc3_gen_lift *)
+lemma cpcs_inv_lift: ∀G,L,K,b,l,k. ⬇[b, l, k] L ≘ K →
+ ∀T1,U1. ⬆[l, k] T1 ≘ U1 → ∀T2,U2. ⬆[l, k] T2 ≘ U2 →
+ ⦃G, L⦄ ⊢ U1 ⬌* U2 → ⦃G, K⦄ ⊢ T1 ⬌* T2.
+#G #L #K #b #l #k #HLK #T1 #U1 #HTU1 #T2 #U2 #HTU2 #HU12
+elim (cpcs_inv_cprs … HU12) -HU12 #U #HU1 #HU2
+elim (cprs_inv_lift1 … HU1 … HLK … HTU1) -U1 #T #HTU #HT1
+elim (cprs_inv_lift1 … HU2 … HLK … HTU2) -L -U2 #X #HXU
+>(lift_inj … HXU … HTU) -X -U -l -k /2 width=3 by cprs_div/
+qed-.
+
+(* Advanced properties ******************************************************)
+
+lemma lpr_cpcs_trans: ∀G,L1,L2. ⦃G, L1⦄ ⊢ ➡ L2 →
+ ∀T1,T2. ⦃G, L2⦄ ⊢ T1 ⬌* T2 → ⦃G, L1⦄ ⊢ T1 ⬌* T2.
+#G #L1 #L2 #HL12 #T1 #T2 #H elim (cpcs_inv_cprs … H) -H
+/4 width=5 by cprs_div, lpr_cprs_trans/
+qed-.
+
+lemma lprs_cpcs_trans: ∀G,L1,L2. ⦃G, L1⦄ ⊢ ➡* L2 →
+ ∀T1,T2. ⦃G, L2⦄ ⊢ T1 ⬌* T2 → ⦃G, L1⦄ ⊢ T1 ⬌* T2.
+#G #L1 #L2 #HL12 #T1 #T2 #H elim (cpcs_inv_cprs … H) -H
+/4 width=5 by cprs_div, lprs_cprs_trans/
+qed-.
+
+lemma cpr_cprs_conf_cpcs: ∀G,L,T,T1,T2. ⦃G, L⦄ ⊢ T ➡* T1 → ⦃G, L⦄ ⊢ T ➡ T2 → ⦃G, L⦄ ⊢ T1 ⬌* T2.
+#G #L #T #T1 #T2 #HT1 #HT2 elim (cprs_strip … HT1 … HT2) -HT1 -HT2
+/2 width=3 by cpr_cprs_div/
+qed-.
+
+lemma cprs_cpr_conf_cpcs: ∀G,L,T,T1,T2. ⦃G, L⦄ ⊢ T ➡* T1 → ⦃G, L⦄ ⊢ T ➡ T2 → ⦃G, L⦄ ⊢ T2 ⬌* T1.
+#G #L #T #T1 #T2 #HT1 #HT2 elim (cprs_strip … HT1 … HT2) -HT1 -HT2
+/2 width=3 by cprs_cpr_div/
+qed-.
+
+lemma cprs_conf_cpcs: ∀G,L,T,T1,T2. ⦃G, L⦄ ⊢ T ➡* T1 → ⦃G, L⦄ ⊢ T ➡* T2 → ⦃G, L⦄ ⊢ T1 ⬌* T2.
+#G #L #T #T1 #T2 #HT1 #HT2 elim (cprs_conf … HT1 … HT2) -HT1 -HT2
+/2 width=3 by cprs_div/
+qed-.
+
+lemma lprs_cprs_conf: ∀G,L1,L2. ⦃G, L1⦄ ⊢ ➡* L2 →
+ ∀T1,T2. ⦃G, L1⦄ ⊢ T1 ➡* T2 → ⦃G, L2⦄ ⊢ T1 ⬌* T2.
+#G #L1 #L2 #HL12 #T1 #T2 #HT12 elim (lprs_cprs_conf_dx … HT12 … HL12) -L1
+/2 width=3 by cprs_div/
+qed-.
+
+(* Basic_1: was: pc3_wcpr0_t *)
+(* Basic_1: note: pc3_wcpr0_t should be renamed *)
+(* Note: alternative proof /3 width=5 by lprs_cprs_conf, lpr_lprs/ *)
+lemma lpr_cprs_conf: ∀G,L1,L2. ⦃G, L1⦄ ⊢ ➡ L2 →
+ ∀T1,T2. ⦃G, L1⦄ ⊢ T1 ➡* T2 → ⦃G, L2⦄ ⊢ T1 ⬌* T2.
+#G #L1 #L2 #HL12 #T1 #T2 #HT12 elim (cprs_lpr_conf_dx … HT12 … HL12) -L1
+/2 width=3 by cprs_div/
+qed-.
+
+(* Basic_1: was only: pc3_pr0_pr2_t *)
+(* Basic_1: note: pc3_pr0_pr2_t should be renamed *)
+lemma lpr_cpr_conf: ∀G,L1,L2. ⦃G, L1⦄ ⊢ ➡ L2 →
+ ∀T1,T2. ⦃G, L1⦄ ⊢ T1 ➡ T2 → ⦃G, L2⦄ ⊢ T1 ⬌* T2.
+/3 width=5 by lpr_cprs_conf, cpr_cprs/ qed-.
+
+(* Basic_1: was only: pc3_thin_dx *)
+lemma cpcs_flat: ∀G,L,V1,V2. ⦃G, L⦄ ⊢ V1 ⬌* V2 → ∀T1,T2. ⦃G, L⦄ ⊢ T1 ⬌* T2 →
+ ∀I. ⦃G, L⦄ ⊢ ⓕ{I}V1.T1 ⬌* ⓕ{I}V2.T2.
+#G #L #V1 #V2 #HV12 #T1 #T2 #HT12
+elim (cpcs_inv_cprs … HV12) -HV12
+elim (cpcs_inv_cprs … HT12) -HT12
+/3 width=5 by cprs_flat, cprs_div/
+qed.
+
+lemma cpcs_flat_dx_cpr_rev: ∀G,L,V1,V2. ⦃G, L⦄ ⊢ V2 ➡ V1 → ∀T1,T2. ⦃G, L⦄ ⊢ T1 ⬌* T2 →
+ ∀I. ⦃G, L⦄ ⊢ ⓕ{I}V1.T1 ⬌* ⓕ{I}V2.T2.
+/3 width=1 by cpr_cpcs_sn, cpcs_flat/ qed.
+
+lemma cpcs_bind_dx: ∀a,I,G,L,V,T1,T2. ⦃G, L.ⓑ{I}V⦄ ⊢ T1 ⬌* T2 →
+ ⦃G, L⦄ ⊢ ⓑ{a,I}V.T1 ⬌* ⓑ{a,I}V.T2.
+#a #I #G #L #V #T1 #T2 #HT12 elim (cpcs_inv_cprs … HT12) -HT12
+/3 width=5 by cprs_div, cprs_bind/
+qed.
+
+lemma cpcs_bind_sn: ∀a,I,G,L,V1,V2,T. ⦃G, L⦄ ⊢ V1 ⬌* V2 → ⦃G, L⦄ ⊢ ⓑ{a,I}V1. T ⬌* ⓑ{a,I}V2. T.
+#a #I #G #L #V1 #V2 #T #HV12 elim (cpcs_inv_cprs … HV12) -HV12
+/3 width=5 by cprs_div, cprs_bind/
+qed.
+
+lemma lsubr_cpcs_trans: ∀G,L1,T1,T2. ⦃G, L1⦄ ⊢ T1 ⬌* T2 →
+ ∀L2. L2 ⫃ L1 → ⦃G, L2⦄ ⊢ T1 ⬌* T2.
+#G #L1 #T1 #T2 #HT12 elim (cpcs_inv_cprs … HT12) -HT12
+/3 width=5 by cprs_div, lsubr_cprs_trans/
+qed-.
+
+(* Basic_1: was: pc3_lift *)
+lemma cpcs_lift: ∀G,L,K,b,l,k. ⬇[b, l, k] L ≘ K →
+ ∀T1,U1. ⬆[l, k] T1 ≘ U1 → ∀T2,U2. ⬆[l, k] T2 ≘ U2 →
+ ⦃G, K⦄ ⊢ T1 ⬌* T2 → ⦃G, L⦄ ⊢ U1 ⬌* U2.
+#G #L #K #b #l #k #HLK #T1 #U1 #HTU1 #T2 #U2 #HTU2 #HT12
+elim (cpcs_inv_cprs … HT12) -HT12 #T #HT1 #HT2
+elim (lift_total T l k) /3 width=12 by cprs_div, cprs_lift/
+qed.
+
+lemma cpcs_strip: ∀G,L,T1,T. ⦃G, L⦄ ⊢ T ⬌* T1 → ∀T2. ⦃G, L⦄ ⊢ T ⬌ T2 →
+ ∃∃T0. ⦃G, L⦄ ⊢ T1 ⬌ T0 & ⦃G, L⦄ ⊢ T2 ⬌* T0.
+#G #L #T1 #T @TC_strip1 /2 width=3 by cpc_conf/ qed-.
+
+(* More inversion lemmas ****************************************************)
+
+(* Note: there must be a proof suitable for llpr *)
+lemma cpcs_inv_abst_sn: ∀a1,a2,G,L,W1,W2,T1,T2. ⦃G, L⦄ ⊢ ⓛ{a1}W1.T1 ⬌* ⓛ{a2}W2.T2 →
+ ∧∧ ⦃G, L⦄ ⊢ W1 ⬌* W2 & ⦃G, L.ⓛW1⦄ ⊢ T1 ⬌* T2 & a1 = a2.
+#a1 #a2 #G #L #W1 #W2 #T1 #T2 #H
+elim (cpcs_inv_cprs … H) -H #T #H1 #H2
+elim (cprs_inv_abst1 … H1) -H1 #W0 #T0 #HW10 #HT10 #H destruct
+elim (cprs_inv_abst1 … H2) -H2 #W #T #HW2 #HT2 #H destruct
+lapply (lprs_cprs_conf … (L.ⓛW) … HT2) /2 width=1 by lprs_pair/ -HT2 #HT2
+lapply (lprs_cpcs_trans … (L.ⓛW1) … HT2) /2 width=1 by lprs_pair/ -HT2 #HT2
+/4 width=3 by and3_intro, cprs_div, cpcs_cprs_div, cpcs_sym/
+qed-.
+
+lemma cpcs_inv_abst_dx: ∀a1,a2,G,L,W1,W2,T1,T2. ⦃G, L⦄ ⊢ ⓛ{a1}W1.T1 ⬌* ⓛ{a2}W2.T2 →
+ ∧∧ ⦃G, L⦄ ⊢ W1 ⬌* W2 & ⦃G, L.ⓛW2⦄ ⊢ T1 ⬌* T2 & a1 = a2.
+#a1 #a2 #G #L #W1 #W2 #T1 #T2 #HT12 lapply (cpcs_sym … HT12) -HT12
+#HT12 elim (cpcs_inv_abst_sn … HT12) -HT12 /3 width=1 by cpcs_sym, and3_intro/
+qed-.
+
+(* Main properties **********************************************************)
+
+(* Basic_1: was pc3_t *)
+theorem cpcs_trans: ∀G,L,T1,T. ⦃G, L⦄ ⊢ T1 ⬌* T → ∀T2. ⦃G, L⦄ ⊢ T ⬌* T2 → ⦃G, L⦄ ⊢ T1 ⬌* T2.
+#G #L #T1 #T #HT1 #T2 @(trans_TC … HT1) qed-.
+
+theorem cpcs_canc_sn: ∀G,L,T,T1,T2. ⦃G, L⦄ ⊢ T ⬌* T1 → ⦃G, L⦄ ⊢ T ⬌* T2 → ⦃G, L⦄ ⊢ T1 ⬌* T2.
+/3 width=3 by cpcs_trans, cpcs_sym/ qed-.
+
+theorem cpcs_canc_dx: ∀G,L,T,T1,T2. ⦃G, L⦄ ⊢ T1 ⬌* T → ⦃G, L⦄ ⊢ T2 ⬌* T → ⦃G, L⦄ ⊢ T1 ⬌* T2.
+/3 width=3 by cpcs_trans, cpcs_sym/ qed-.
+
+lemma cpcs_bind1: ∀a,I,G,L,V1,V2. ⦃G, L⦄ ⊢ V1 ⬌* V2 →
+ ∀T1,T2. ⦃G, L.ⓑ{I}V1⦄ ⊢ T1 ⬌* T2 →
+ ⦃G, L⦄ ⊢ ⓑ{a,I}V1. T1 ⬌* ⓑ{a,I}V2. T2.
+/3 width=3 by cpcs_trans, cpcs_bind_sn, cpcs_bind_dx/ qed.
+
+lemma cpcs_bind2: ∀a,I,G,L,V1,V2. ⦃G, L⦄ ⊢ V1 ⬌* V2 →
+ ∀T1,T2. ⦃G, L.ⓑ{I}V2⦄ ⊢ T1 ⬌* T2 →
+ ⦃G, L⦄ ⊢ ⓑ{a,I}V1. T1 ⬌* ⓑ{a,I}V2. T2.
+/3 width=3 by cpcs_trans, cpcs_bind_sn, cpcs_bind_dx/ qed.
+
+(* Basic_1: was: pc3_wcpr0 *)
+lemma lpr_cpcs_conf: ∀G,L1,L2. ⦃G, L1⦄ ⊢ ➡ L2 →
+ ∀T1,T2. ⦃G, L1⦄ ⊢ T1 ⬌* T2 → ⦃G, L2⦄ ⊢ T1 ⬌* T2.
+#G #L1 #L2 #HL12 #T1 #T2 #H elim (cpcs_inv_cprs … H) -H
+/3 width=5 by cpcs_canc_dx, lpr_cprs_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/computation/cprs.ma".
+include "basic_2/equivalence/cpcs.ma".
+
+(* CONTEXT-SENSITIVE PARALLEL EQUIVALENCE ON TERMS **************************)
+
+(* Properties about context sensitive computation on terms ******************)
+
+(* Basic_1: was: pc3_pr3_r *)
+lemma cpcs_cprs_dx: ∀G,L,T1,T2. ⦃G, L⦄ ⊢ T1 ➡* T2 → ⦃G, L⦄ ⊢ T1 ⬌* T2.
+#G #L #T1 #T2 #H @(cprs_ind … H) -T2
+/3 width=3 by cpcs_cpr_strap1, cpcs_strap1, cpc_cpcs/
+qed.
+
+(* Basic_1: was: pc3_pr3_x *)
+lemma cpcs_cprs_sn: ∀G,L,T1,T2. ⦃G, L⦄ ⊢ T2 ➡* T1 → ⦃G, L⦄ ⊢ T1 ⬌* T2.
+#G #L #T1 #T2 #H @(cprs_ind_dx … H) -T2
+/3 width=3 by cpcs_cpr_div, cpcs_strap1, cpcs_cprs_dx/
+qed.
+
+lemma cpcs_cprs_strap1: ∀G,L,T1,T. ⦃G, L⦄ ⊢ T1 ⬌* T → ∀T2. ⦃G, L⦄ ⊢ T ➡* T2 → ⦃G, L⦄ ⊢ T1 ⬌* T2.
+#G #L #T1 #T #HT1 #T2 #H @(cprs_ind … H) -T2 /2 width=3 by cpcs_cpr_strap1/
+qed-.
+
+lemma cpcs_cprs_strap2: ∀G,L,T1,T. ⦃G, L⦄ ⊢ T1 ➡* T → ∀T2. ⦃G, L⦄ ⊢ T ⬌* T2 → ⦃G, L⦄ ⊢ T1 ⬌* T2.
+#G #L #T1 #T #H #T2 #HT2 @(cprs_ind_dx … H) -T1 /2 width=3 by cpcs_cpr_strap2/
+qed-.
+
+lemma cpcs_cprs_div: ∀G,L,T1,T. ⦃G, L⦄ ⊢ T1 ⬌* T → ∀T2. ⦃G, L⦄ ⊢ T2 ➡* T → ⦃G, L⦄ ⊢ T1 ⬌* T2.
+#G #L #T1 #T #HT1 #T2 #H @(cprs_ind_dx … H) -T2 /2 width=3 by cpcs_cpr_div/
+qed-.
+
+(* Basic_1: was: pc3_pr3_conf *)
+lemma cpcs_cprs_conf: ∀G,L,T1,T. ⦃G, L⦄ ⊢ T ➡* T1 → ∀T2. ⦃G, L⦄ ⊢ T ⬌* T2 → ⦃G, L⦄ ⊢ T1 ⬌* T2.
+#G #L #T1 #T #H #T2 #HT2 @(cprs_ind … H) -T1 /2 width=3 by cpcs_cpr_conf/
+qed-.
+
+(* Basic_1: was: pc3_pr3_t *)
+(* Basic_1: note: pc3_pr3_t should be renamed *)
+lemma cprs_div: ∀G,L,T1,T. ⦃G, L⦄ ⊢ T1 ➡* T → ∀T2. ⦃G, L⦄ ⊢ T2 ➡* T → ⦃G, L⦄ ⊢ T1 ⬌* T2.
+#G #L #T1 #T #HT1 #T2 #H @(cprs_ind_dx … H) -T2
+/2 width=3 by cpcs_cpr_div, cpcs_cprs_dx/
+qed.
+
+lemma cprs_cpr_div: ∀G,L,T1,T. ⦃G, L⦄ ⊢ T1 ➡* T → ∀T2. ⦃G, L⦄ ⊢ T2 ➡ T → ⦃G, L⦄ ⊢ T1 ⬌* T2.
+/3 width=5 by cpr_cprs, cprs_div/ qed-.
+
+lemma cpr_cprs_div: ∀G,L,T1,T. ⦃G, L⦄ ⊢ T1 ➡ T → ∀T2. ⦃G, L⦄ ⊢ T2 ➡* T → ⦃G, L⦄ ⊢ T1 ⬌* T2.
+/3 width=3 by cpr_cprs, cprs_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/notation/relations/dpconvstar_8.ma".
+include "basic_2/computation/scpds.ma".
+
+(* STRATIFIED DECOMPOSED PARALLEL EQUIVALENCE FOR TERMS *********************)
+
+definition scpes: ∀h. sd h → nat → nat → relation4 genv lenv term term ≝
+ λh,o,d1,d2,G,L,T1,T2.
+ ∃∃T. ⦃G, L⦄ ⊢ T1 •*➡*[h, o, d1] T & ⦃G, L⦄ ⊢ T2 •*➡*[h, o, d2] T.
+
+interpretation "stratified decomposed parallel equivalence (term)"
+ 'DPConvStar h o d1 d2 G L T1 T2 = (scpes h o d1 d2 G L T1 T2).
+
+(* Basic properties *********************************************************)
+
+lemma scpds_div: ∀h,o,G,L,T1,T2,T,d1,d2.
+ ⦃G, L⦄ ⊢ T1 •*➡*[h, o, d1] T → ⦃G, L⦄ ⊢ T2 •*➡*[h, o, d2] T →
+ ⦃G, L⦄ ⊢ T1 •*⬌*[h, o, d1, d2] T2.
+/2 width=3 by ex2_intro/ qed.
+
+lemma scpes_sym: ∀h,o,G,L,T1,T2,d1,d2. ⦃G, L⦄ ⊢ T1 •*⬌*[h, o, d1, d2] T2 →
+ ⦃G, L⦄ ⊢ T2 •*⬌*[h, o, d2, d1] T1.
+#h #o #G #L #T1 #T2 #L1 #d2 * /2 width=3 by scpds_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/computation/scpds_aaa.ma".
+include "basic_2/equivalence/scpes.ma".
+
+(* DECOMPOSED EXTENDED PARALLEL EQUIVALENCE FOR TERMS ***********************)
+
+(* Main inversion lemmas about atomic arity assignment on terms *************)
+
+theorem scpes_aaa_mono: ∀h,o,G,L,T1,T2,d1,d2. ⦃G, L⦄ ⊢ T1 •*⬌*[h, o, d1, d2] T2 →
+ ∀A1. ⦃G, L⦄ ⊢ T1 ⁝ A1 → ∀A2. ⦃G, L⦄ ⊢ T2 ⁝ A2 →
+ A1 = A2.
+#h #o #G #L #T1 #T2 #d1 #d2 * #T #HT1 #HT2 #A1 #HA1 #A2 #HA2
+lapply (scpds_aaa_conf … HA1 … HT1) -T1 #HA1
+lapply (scpds_aaa_conf … HA2 … HT2) -T2 #HA2
+lapply (aaa_mono … HA1 … HA2) -L -T //
+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/computation/scpds_scpds.ma".
+include "basic_2/equivalence/cpcs_cpcs.ma".
+include "basic_2/equivalence/scpes.ma".
+
+(* STRATIFIED DECOMPOSED PARALLEL EQUIVALENCE FOR TERMS *********************)
+
+(* Inversion lemmas on parallel equivalence for terms ***********************)
+
+lemma scpes_inv_lstas_eq: ∀h,o,G,L,T1,T2,d1,d2. ⦃G, L⦄ ⊢ T1 •*⬌*[h, o, d1, d2] T2 →
+ ∀U1. ⦃G, L⦄ ⊢ T1 •*[h, d1] U1 →
+ ∀U2. ⦃G, L⦄ ⊢ T2 •*[h, d2] U2 → ⦃G, L⦄ ⊢ U1 ⬌* U2.
+#h #o #G #L #T1 #T2 #d1 #d2 * #T #HT1 #HT2 #U1 #HTU1 #U2 #HTU2
+/3 width=8 by scpds_inv_lstas_eq, cprs_div/
+qed-.
+
+(* Properties on parallel equivalence for terms *****************************)
+
+lemma cpcs_scpes: ∀h,o,G,L,T1,d11. ⦃G, L⦄ ⊢ T1 ▪[h, o] d11 →
+ ∀U1,d12. d12 ≤ d11 → ⦃G, L⦄ ⊢ T1 •*[h, d12] U1 →
+ ∀T2,d21. ⦃G, L⦄ ⊢ T2 ▪[h, o] d21 →
+ ∀U2,d22. d22 ≤ d21 → ⦃G, L⦄ ⊢ T2 •*[h, d22] U2 →
+ ⦃G, L⦄ ⊢ U1 ⬌* U2 → ⦃G, L⦄ ⊢ T1 •*⬌*[h, o, d12, d22] T2.
+#h #o #G #L #T1 #d11 #HT1 #U1 #d12 #Hd121 #HTU1 #T2 #d21 #HT2 #U2 #d22 #Hd221 #HTU2 #HU12
+elim (cpcs_inv_cprs … HU12) -HU12 /3 width=6 by scpds_div, ex4_2_intro/
+qed.
--- /dev/null
+(**************************************************************************)
+(* ___ *)
+(* ||M|| *)
+(* ||A|| A project by Andrea Asperti *)
+(* ||T|| *)
+(* ||I|| Developers: *)
+(* ||T|| The HELM team. *)
+(* ||A|| http://helm.cs.unibo.it *)
+(* \ / *)
+(* \ / This file is distributed under the terms of the *)
+(* v GNU General Public License Version 2 *)
+(* *)
+(**************************************************************************)
+
+include "basic_2/computation/scpds_scpds.ma".
+include "basic_2/equivalence/scpes.ma".
+
+(* STRATIFIED DECOMPOSED PARALLEL EQUIVALENCE FOR TERMS *********************)
+
+(* Advanced inversion lemmas ************************************************)
+
+lemma scpes_inv_abst2: ∀h,o,a,G,L,T1,T2,W2,d1,d2. ⦃G, L⦄ ⊢ T1 •*⬌*[h, o, d1, d2] ⓛ{a}W2.T2 →
+ ∃∃W,T. ⦃G, L⦄ ⊢ T1 •*➡*[h, o, d1] ⓛ{a}W.T & ⦃G, L⦄ ⊢ W2 ➡* W &
+ ⦃G, L.ⓛW2⦄ ⊢ T2 •*➡*[h, o, d2] T.
+#h #o #a #G #L #T1 #T2 #W2 #d1 #d2 * #T0 #HT10 #H
+elim (scpds_inv_abst1 … H) -H #W #T #HW2 #HT2 #H destruct /2 width=5 by ex3_2_intro/
+qed-.
+
+(* Advanced properties ******************************************************)
+
+lemma scpes_refl: ∀h,o,G,L,T,d1,d2. d2 ≤ d1 → ⦃G, L⦄ ⊢ T ▪[h, o] d1 →
+ ⦃G, L⦄ ⊢ T •*⬌*[h, o, d2, d2] T.
+#h #o #G #L #T #d1 #d2 #Hd21 #Hd1
+elim (da_lstas … Hd1 … d2) #U #HTU #_
+/3 width=3 by scpds_div, lstas_scpds/
+qed.
+
+lemma lstas_scpes_trans: ∀h,o,G,L,T1,d0,d1. ⦃G, L⦄ ⊢ T1 ▪[h, o] d0 → d1 ≤ d0 →
+ ∀T. ⦃G, L⦄ ⊢ T1 •*[h, d1] T →
+ ∀T2,d,d2. ⦃G, L⦄ ⊢ T •*⬌*[h,o,d,d2] T2 → ⦃G, L⦄ ⊢ T1 •*⬌*[h,o,d1+d,d2] T2.
+#h #o #G #L #T1 #d0 #d1 #Hd0 #Hd10 #T #HT1 #T2 #d #d2 *
+/3 width=3 by scpds_div, lstas_scpds_trans/ qed-.
+
+(* Properties on parallel computation for terms *****************************)
+
+lemma cprs_scpds_div: ∀h,o,G,L,T1,T. ⦃G, L⦄ ⊢ T1 ➡* T →
+ ∀d. ⦃G, L⦄ ⊢ T1 ▪[h, o] d →
+ ∀T2,d2. ⦃G, L⦄ ⊢ T2 •*➡*[h, o, d2] T →
+ ⦃G, L⦄⊢ T1 •*⬌*[h, o, 0, d2] T2.
+#h #o #G #L #T1 #T #HT1 #d #Hd elim (da_lstas … Hd 0)
+#X1 #HTX1 #_ elim (cprs_strip … HT1 X1) -HT1
+/3 width=5 by scpds_strap1, scpds_div, lstas_cpr, ex4_2_intro/
+qed.
+
+(* Main properties **********************************************************)
+
+theorem scpes_trans: ∀h,o,G,L,T1,T,d1,d. ⦃G, L⦄ ⊢ T1 •*⬌*[h, o, d1, d] T →
+ ∀T2,d2. ⦃G, L⦄ ⊢ T •*⬌*[h, o, d, d2] T2 → ⦃G, L⦄ ⊢ T1 •*⬌*[h, o, d1, d2] T2.
+#h #o #G #L #T1 #T #d1 #d * #X1 #HT1X1 #HTX1 #T2 #d2 * #X2 #HTX2 #HT2X2
+elim (scpds_conf_eq … HTX1 … HTX2) -T -d /3 width=5 by scpds_cprs_trans, scpds_div/
+qed-.
+
+theorem scpes_canc_sn: ∀h,o,G,L,T,T1,d,d1. ⦃G, L⦄ ⊢ T •*⬌*[h, o, d, d1] T1 →
+ ∀T2,d2. ⦃G, L⦄ ⊢ T •*⬌*[h, o, d, d2] T2 → ⦃G, L⦄ ⊢ T1 •*⬌*[h, o, d1, d2] T2.
+/3 width=4 by scpes_trans, scpes_sym/ qed-.
+
+theorem scpes_canc_dx: ∀h,o,G,L,T1,T,d1,d. ⦃G, L⦄ ⊢ T1 •*⬌*[h, o, d1, d] T →
+ ∀T2,d2. ⦃G, L⦄ ⊢ T2 •*⬌*[h, o, d2, d] T → ⦃G, L⦄ ⊢ T1 •*⬌*[h, o, d1, d2] T2.
+/3 width=4 by scpes_trans, scpes_sym/ qed-.
]
}
]
-(*
class "prune"
- [ { "equivalence" * } {
+ [ { "rt-equivalence" * } {
+(*
[ { "decomposed rt-equivalence" * } {
[ [ "" ] "scpes ( ⦃?,?⦄ ⊢ ? •*⬌*[?,?,?,?] ? )" "scpes_aaa" + "scpes_cpcs" + "scpes_scpes" * ]
}
]
- [ { "context-sensitive equivalence" * } {
- [ [ "" ] "cpcs ( ⦃?,?⦄ ⊢ ? ⬌* ? )" "cpcs_aaa" + "cpcs_cprs" + "cpcs_cpcs" * ]
+*)
+ [ { "context-sensitive parallel r-equivalence" * } {
+ [ [ "for terms" ] "cpcs ( ⦃?,?⦄ ⊢ ? ⬌*[?] ? )" (* "cpcs_aaa" + "cpcs_cprs" + "cpcs_cpcs" *) * ]
}
]
}
]
-*)
class "blue"
[ { "rt-conversion" * } {
[ { "context-sensitive parallel r-conversion" * } {
../../matitac.opt `cat partial.txt`
cd basic_2/rt_computation/
../../../../matitac.opt `cat partial.txt`
+cd ../rt_equivalence/
+../../../../matitac.opt `cat partial.txt`
cd ../dynamic/
../../../../matitac.opt `cat partial.txt`
cd ../../
projects / helm.git / commitdiff