--- /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 o, break term 46 n1, break term 46 n2 ] break term 46 T2 )"
+ non associative with precedence 45
+ for @{ 'DPConvStar $h $o $n1 $n2 $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/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-.
+++ /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 o, break term 46 n1, break term 46 n2 ] break term 46 T2 )"
- non associative with precedence 45
- for @{ 'DPConvStar $h $o $n1 $n2 $G $L $T1 $T2 }.
(* CONTEXT-SENSITIVE PARALLEL R-EQUIVALENCE FOR TERMS ***********************)
-definition cpcs: sh → relation4 genv lenv term term ≝
- λh,G. CTC … (cpc h G).
+definition cpcs (h) (G): relation3 lenv term term ≝
+ 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.
+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.
+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).
+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).
+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.
+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.
+lemma cpcs_step_sn (h) (G) (L): ∀T1,T. ⦃G, L⦄ ⊢ T1 ⬌[h] T →
+ ∀T2. ⦃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.
+lemma cpcs_step_dx (h) (G) (L): ∀T1,T. ⦃G, L⦄ ⊢ T1 ⬌*[h] T →
+ ∀T2. ⦃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.
+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.
+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.
+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.
+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.
+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.
+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.
+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:
(* *)
(**************************************************************************)
-include "basic_2/computation/cpxs_aaa.ma".
-include "basic_2/equivalence/cpcs_cpcs.ma".
+include "basic_2/rt_computation/cpms_aaa.ma".
+include "basic_2/rt_equivalence/cpcs_cprs.ma".
(* CONTEXT-SENSITIVE PARALLEL EQUIVALENCE ON TERMS **************************)
-(* Main inversion lemmas about atomic arity assignment on terms *************)
+(* Main inversion lemmas with 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
+theorem cpcs_aaa_mono (h) (G) (L): ∀T1,T2. ⦃G, L⦄ ⊢ T1 ⬌*[h] T2 →
+ ∀A1. ⦃G, L⦄ ⊢ T1 ⁝ A1 → ∀A2. ⦃G, L⦄ ⊢ T2 ⁝ A2 →
+ A1 = A2.
+#h #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 (cpms_aaa_conf … HA1 … HT1) -T1 #HA1
+lapply (cpms_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/rt_conversion/cpc_cpc.ma".
+include "basic_2/rt_equivalence/cpcs.ma".
+
+(* CONTEXT-SENSITIVE PARALLEL R-EQUIVALENCE FOR TERMS ***********************)
+
+(* Properties with context-sensitive parallel r-conversion for terms ********)
+
+lemma cpcs_strip (h) (G) (L): confluent2 … (cpcs h G L) (cpc h G L).
+#h #G #L #T1 #T @TC_strip1 /2 width=3 by cpc_conf/
+qed-.
(* *)
(**************************************************************************)
-include "basic_2/computation/lprs_cprs.ma".
-include "basic_2/conversion/cpc_cpc.ma".
-include "basic_2/equivalence/cpcs_cprs.ma".
+include "basic_2/rt_equivalence/cpcs_lprs.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-.
+(* CONTEXT-SENSITIVE PARALLEL R-EQUIVALENCE FOR TERMS ***********************)
(* 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_trans (h) (G) (L): Transitive … (cpcs h G L).
+#h #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.
+theorem cpcs_canc_sn (h) (G) (L): left_cancellable … (cpcs h G L).
/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.
+theorem cpcs_canc_dx (h) (G) (L): right_cancellable … (cpcs h G L).
/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.
+(* Advanced properties ******************************************************)
+
+lemma cpcs_bind1 (h) (G) (L): ∀V1,V2. ⦃G, L⦄ ⊢ V1 ⬌*[h] V2 →
+ ∀I,T1,T2. ⦃G, L.ⓑ{I}V1⦄ ⊢ T1 ⬌*[h] T2 →
+ ∀p. ⦃G, L⦄ ⊢ ⓑ{p,I}V1.T1 ⬌*[h] ⓑ{p,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.
+lemma cpcs_bind2 (h) (G) (L): ∀V1,V2. ⦃G, L⦄ ⊢ V1 ⬌*[h] V2 →
+ ∀I,T1,T2. ⦃G, L.ⓑ{I}V2⦄ ⊢ T1 ⬌*[h] T2 →
+ ∀p. ⦃G, L⦄ ⊢ ⓑ{p,I}V1.T1 ⬌*[h] ⓑ{p,I}V2.T2.
/3 width=3 by cpcs_trans, cpcs_bind_sn, cpcs_bind_dx/ qed.
+(* Advanced properties with r-transition for full local environments ********)
+
(* 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
+lemma lpr_cpcs_conf (h) (G): ∀L1,L2. ⦃G, L1⦄ ⊢ ➡[h] L2 →
+ ∀T1,T2. ⦃G, L1⦄ ⊢ T1 ⬌*[h] T2 → ⦃G, L2⦄ ⊢ T1 ⬌*[h] T2.
+#h #G #L1 #L2 #HL12 #T1 #T2 #H elim (cpcs_inv_cprs … H) -H
/3 width=5 by cpcs_canc_dx, lpr_cprs_conf/
qed-.
(* *)
(**************************************************************************)
-include "basic_2/computation/cprs.ma".
-include "basic_2/equivalence/cpcs.ma".
+include "basic_2/rt_computation/cprs_cprs.ma".
+include "basic_2/rt_computation/lprs_cpms.ma".
+include "basic_2/rt_equivalence/cpcs.ma".
-(* CONTEXT-SENSITIVE PARALLEL EQUIVALENCE ON TERMS **************************)
+(* CONTEXT-SENSITIVE PARALLEL R-EQUIVALENCE FOR TERMS ***********************)
-(* Properties about context sensitive computation on terms ******************)
+(* Inversion lemmas with context sensitive r-computation on terms ***********)
+
+lemma cpcs_inv_cprs (h) (G) (L): ∀T1,T2. ⦃G, L⦄ ⊢ T1 ⬌*[h] T2 →
+ ∃∃T. ⦃G, L⦄ ⊢ T1 ➡*[h] T & ⦃G, L⦄ ⊢ T2 ➡*[h] T.
+#h #G #L #T1 #T2 #H @(cpcs_ind_dx … 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_step_dx, ex2_intro/
+ | /3 width=5 by cprs_step_sn, ex2_intro/
+ ]
+]
+qed-.
+
+(* Advanced inversion lemmas ************************************************)
+
+(* Basic_1: was: pc3_gen_sort *)
+(* Basic_2A1: was: cpcs_inv_sort *)
+lemma cpcs_inv_sort_bi (h) (G) (L): ∀s1,s2. ⦃G, L⦄ ⊢ ⋆s1 ⬌*[h] ⋆s2 → s1 = s2.
+#h #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-.
+
+(* Basic_2A1: was: cpcs_inv_abst1 *)
+lemma cpcs_inv_abst_sn (h) (G) (L):
+ ∀p,W1,T1,X. ⦃G, L⦄ ⊢ ⓛ{p}W1.T1 ⬌*[h] X →
+ ∃∃W2,T2. ⦃G, L⦄ ⊢ X ➡*[h] ⓛ{p}W2.T2 & ⦃G, L⦄ ⊢ ⓛ{p}W1.T1 ➡*[h] ⓛ{p}W2.T2.
+#h #G #L #p #W1 #T1 #T #H
+elim (cpcs_inv_cprs … H) -H #X #H1 #H2
+elim (cpms_inv_abst_sn … H1) -H1 #W2 #T2 #HW12 #HT12 #H destruct
+/3 width=6 by cpms_bind, ex2_2_intro/
+qed-.
+
+(* Basic_2A1: was: cpcs_inv_abst2 *)
+lemma cpcs_inv_abst_dx (h) (G) (L):
+ ∀p,W1,T1,X. ⦃G, L⦄ ⊢ X ⬌*[h] ⓛ{p}W1.T1 →
+ ∃∃W2,T2. ⦃G, L⦄ ⊢ X ➡*[h] ⓛ{p}W2.T2 & ⦃G, L⦄ ⊢ ⓛ{p}W1.T1 ➡*[h] ⓛ{p}W2.T2.
+/3 width=1 by cpcs_inv_abst_sn, cpcs_sym/ qed-.
+
+(* Basic_1: was: pc3_gen_sort_abst *)
+lemma cpcs_inv_sort_abst (h) (G) (L):
+ ∀p,W,T,s. ⦃G, L⦄ ⊢ ⋆s ⬌*[h] ⓛ{p}W.T → ⊥.
+#h #G #L #p #W #T #s #H
+elim (cpcs_inv_cprs … H) -H #X #H1
+>(cprs_inv_sort1 … H1) -X #H2
+elim (cpms_inv_abst_sn … H2) -H2 #W0 #T0 #_ #_ #H destruct
+qed-.
+
+(* Properties with context sensitive r-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/
+lemma cpcs_cprs_dx (h) (G) (L): ∀T1,T2. ⦃G, L⦄ ⊢ T1 ➡*[h] T2 → ⦃G, L⦄ ⊢ T1 ⬌*[h] T2.
+#h #G #L #T1 #T2 #H @(cprs_ind_dx … H) -T2
+/3 width=3 by cpcs_cpr_step_dx, cpcs_step_dx, 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/
+lemma cpcs_cprs_sn (h) (G) (L): ∀T1,T2. ⦃G, L⦄ ⊢ T2 ➡*[h] T1 → ⦃G, L⦄ ⊢ T1 ⬌*[h] T2.
+#h #G #L #T1 #T2 #H @(cprs_ind_sn … H) -T2
+/3 width=3 by cpcs_cpr_div, cpcs_step_sn, 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/
+(* Basic_2A1: was: cpcs_cprs_strap1 *)
+lemma cpcs_cprs_step_dx (h) (G) (L): ∀T1,T. ⦃G, L⦄ ⊢ T1 ⬌*[h] T →
+ ∀T2. ⦃G, L⦄ ⊢ T ➡*[h] T2 → ⦃G, L⦄ ⊢ T1 ⬌*[h] T2.
+#h #G #L #T1 #T #HT1 #T2 #H @(cprs_ind_dx … H) -T2 /2 width=3 by cpcs_cpr_step_dx/
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/
+(* Basic_2A1: was: cpcs_cprs_strap2 *)
+lemma cpcs_cprs_step_sn (h) (G) (L): ∀T1,T. ⦃G, L⦄ ⊢ T1 ➡*[h] T →
+ ∀T2. ⦃G, L⦄ ⊢ T ⬌*[h] T2 → ⦃G, L⦄ ⊢ T1 ⬌*[h] T2.
+#h #G #L #T1 #T #H #T2 #HT2 @(cprs_ind_sn … H) -T1 /2 width=3 by cpcs_cpr_step_sn/
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/
+lemma cpcs_cprs_div (h) (G) (L): ∀T1,T. ⦃G, L⦄ ⊢ T1 ⬌*[h] T →
+ ∀T2. ⦃G, L⦄ ⊢ T2 ➡*[h] T → ⦃G, L⦄ ⊢ T1 ⬌*[h] T2.
+#h #G #L #T1 #T #HT1 #T2 #H @(cprs_ind_sn … 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/
+lemma cpcs_cprs_conf (h) (G) (L): ∀T1,T. ⦃G, L⦄ ⊢ T ➡*[h] T1 →
+ ∀T2. ⦃G, L⦄ ⊢ T ⬌*[h] T2 → ⦃G, L⦄ ⊢ T1 ⬌*[h] T2.
+#h #G #L #T1 #T #H #T2 #HT2 @(cprs_ind_dx … 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
+lemma cprs_div (h) (G) (L): ∀T1,T. ⦃G, L⦄ ⊢ T1 ➡*[h] T →
+ ∀T2. ⦃G, L⦄ ⊢ T2 ➡*[h] T → ⦃G, L⦄ ⊢ T1 ⬌*[h] T2.
+#h #G #L #T1 #T #HT1 #T2 #H @(cprs_ind_sn … 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 cprs_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=5 by cpm_cpms, cprs_div/ qed-.
+
+lemma cpr_cprs_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 cpm_cpms, cprs_div/ qed-.
+
+lemma cpr_cprs_conf_cpcs (h) (G) (L): ∀T,T1. ⦃G, L⦄ ⊢ T ➡*[h] T1 →
+ ∀T2. ⦃G, L⦄ ⊢ T ➡[h] T2 → ⦃G, L⦄ ⊢ T1 ⬌*[h] T2.
+#h #G #L #T #T1 #HT1 #T2 #HT2 elim (cprs_strip … HT1 … HT2) -HT1 -HT2
+/2 width=3 by cpr_cprs_div/
+qed-.
+
+lemma cprs_cpr_conf_cpcs (h) (G) (L): ∀T,T1. ⦃G, L⦄ ⊢ T ➡*[h] T1 →
+ ∀T2. ⦃G, L⦄ ⊢ T ➡[h] T2 → ⦃G, L⦄ ⊢ T2 ⬌*[h] T1.
+#h #G #L #T #T1 #HT1 #T2 #HT2 elim (cprs_strip … HT1 … HT2) -HT1 -HT2
+/2 width=3 by cprs_cpr_div/
+qed-.
+
+lemma cprs_conf_cpcs (h) (G) (L): ∀T,T1. ⦃G, L⦄ ⊢ T ➡*[h] T1 →
+ ∀T2. ⦃G, L⦄ ⊢ T ➡*[h] T2 → ⦃G, L⦄ ⊢ T1 ⬌*[h] T2.
+#h #G #L #T #T1 #HT1 #T2 #HT2 elim (cprs_conf … HT1 … HT2) -HT1 -HT2
+/2 width=3 by cprs_div/
+qed-.
+
+(* Basic_1: was only: pc3_thin_dx *)
+lemma cpcs_flat (h) (G) (L): ∀V1,V2. ⦃G, L⦄ ⊢ V1 ⬌*[h] V2 →
+ ∀T1,T2. ⦃G, L⦄ ⊢ T1 ⬌*[h] T2 →
+ ∀I. ⦃G, L⦄ ⊢ ⓕ{I}V1.T1 ⬌*[h] ⓕ{I}V2.T2.
+#h #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 (h) (G) (L): ∀V1,V2. ⦃G, L⦄ ⊢ V2 ➡[h] V1 →
+ ∀T1,T2. ⦃G, L⦄ ⊢ T1 ⬌*[h] T2 →
+ ∀I. ⦃G, L⦄ ⊢ ⓕ{I}V1.T1 ⬌*[h] ⓕ{I}V2.T2.
+/3 width=1 by cpr_cpcs_sn, cpcs_flat/ 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-.
+lemma cpcs_bind_dx (h) (G) (L): ∀I,V,T1,T2. ⦃G, L.ⓑ{I}V⦄ ⊢ T1 ⬌*[h] T2 →
+ ∀p. ⦃G, L⦄ ⊢ ⓑ{p,I}V.T1 ⬌*[h] ⓑ{p,I}V.T2.
+#h #G #L #I #V #T1 #T2 #HT12 elim (cpcs_inv_cprs … HT12) -HT12
+/3 width=5 by cprs_div, cpms_bind/
+qed.
+
+lemma cpcs_bind_sn (h) (G) (L): ∀I,V1,V2,T. ⦃G, L⦄ ⊢ V1 ⬌*[h] V2 →
+ ∀p. ⦃G, L⦄ ⊢ ⓑ{p,I}V1.T ⬌*[h] ⓑ{p,I}V2.T.
+#h #G #L #I #V1 #V2 #T #HV12 elim (cpcs_inv_cprs … HV12) -HV12
+/3 width=5 by cprs_div, cpms_bind/
+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_equivalence/cpcs_cprs.ma".
+
+(* CONTEXT-SENSITIVE PARALLEL R-EQUIVALENCE FOR TERMS ***********************)
+
+(* Properties with generic slicing for local environments *******************)
+
+(* Basic_1: was: pc3_lift *)
+(* Basic_2A1: was: cpcs_lift *)
+lemma cpcs_lifts_bi (h) (G): d_liftable2_bi … lifts (cpcs h G).
+#h #G #K #T1 #T2 #HT12 #b #f #L #HLK #U1 #HTU1 #U2 #HTU2
+elim (cpcs_inv_cprs … HT12) -HT12 #T #HT1 #HT2
+elim (lifts_total T f) #U #HU
+/3 width=12 by cprs_div, cpms_lifts_bi/
+qed-.
+
+(* Inversion lemmas with generic slicing for local environments *************)
+
+(* Basic_1: was: pc3_gen_lift *)
+(* Basic_2A1: was cpcs_inv_lift *)
+lemma cpcs_inv_lifts_bi (h) (G): d_deliftable2_bi … lifts (cpcs h G).
+#h #G #L #U1 #U2 #HU12 #b #f #K #HLK #T1 #HTU1 #T2 #HTU2
+elim (cpcs_inv_cprs … HU12) -HU12 #U #HU1 #HU2
+elim (cpms_inv_lifts_sn … HU1 … HLK … HTU1) -U1 #T #HTU #HT1
+lapply (cpms_inv_lifts_bi … HU2 … HLK … HTU2 … HTU) -L -U -U2 -b -f #HT2
+/2 width=3 by 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/rt_computation/lprs_cprs.ma".
+include "basic_2/rt_equivalence/cpcs_cprs.ma".
+
+(* CONTEXT-SENSITIVE PARALLEL R-EQUIVALENCE FOR TERMS ***********************)
+
+(* Properties with parallel r-computation for full local environments *******)
+
+lemma lpr_cpcs_trans (h) (G): ∀L1,L2. ⦃G, L1⦄ ⊢ ➡[h] L2 →
+ ∀T1,T2. ⦃G, L2⦄ ⊢ T1 ⬌*[h] T2 → ⦃G, L1⦄ ⊢ T1 ⬌*[h] T2.
+#h #G #L1 #L2 #HL12 #T1 #T2 #H elim (cpcs_inv_cprs … H) -H
+ /4 width=5 by cprs_div, lpr_cpms_trans/
+qed-.
+
+lemma lprs_cpcs_trans (h) (G): ∀L1,L2. ⦃G, L1⦄ ⊢ ➡*[h] L2 →
+ ∀T1,T2. ⦃G, L2⦄ ⊢ T1 ⬌*[h] T2 → ⦃G, L1⦄ ⊢ T1 ⬌*[h] T2.
+#h #G #L1 #L2 #HL12 #T1 #T2 #H elim (cpcs_inv_cprs … H) -H
+/4 width=5 by cprs_div, lprs_cpms_trans/
+qed-.
+
+lemma lprs_cprs_conf (h) (G): ∀L1,L2. ⦃G, L1⦄ ⊢ ➡*[h] L2 →
+ ∀T1,T2. ⦃G, L1⦄ ⊢ T1 ➡*[h] T2 → ⦃G, L2⦄ ⊢ T1 ⬌*[h] T2.
+#h #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 (h) (G): ∀L1,L2. ⦃G, L1⦄ ⊢ ➡[h] L2 →
+ ∀T1,T2. ⦃G, L1⦄ ⊢ T1 ➡*[h] T2 → ⦃G, L2⦄ ⊢ T1 ⬌*[h] T2.
+#h #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 (h) (G): ∀L1,L2. ⦃G, L1⦄ ⊢ ➡[h] L2 →
+ ∀T1,T2. ⦃G, L1⦄ ⊢ T1 ➡[h] T2 → ⦃G, L2⦄ ⊢ T1 ⬌*[h] T2.
+/3 width=5 by lpr_cprs_conf, cpm_cpms/ qed-.
+
+(* Advanced inversion lemmas ************************************************)
+
+(* Note: there must be a proof suitable for lfpr *)
+lemma cpcs_inv_abst_sn (h) (G) (L): ∀p1,p2,W1,W2,T1,T2. ⦃G, L⦄ ⊢ ⓛ{p1}W1.T1 ⬌*[h] ⓛ{p2}W2.T2 →
+ ∧∧ ⦃G, L⦄ ⊢ W1 ⬌*[h] W2 & ⦃G, L.ⓛW1⦄ ⊢ T1 ⬌*[h] T2 & p1 = p2.
+#h #G #L #p1 #p2 #W1 #W2 #T1 #T2 #H
+elim (cpcs_inv_cprs … H) -H #T #H1 #H2
+elim (cpms_inv_abst_sn … H1) -H1 #W0 #T0 #HW10 #HT10 #H destruct
+elim (cpms_inv_abst_sn … 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 (h) (G) (L): ∀p1,p2,W1,W2,T1,T2. ⦃G, L⦄ ⊢ ⓛ{p1}W1.T1 ⬌*[h] ⓛ{p2}W2.T2 →
+ ∧∧ ⦃G, L⦄ ⊢ W1 ⬌*[h] W2 & ⦃G, L.ⓛW2⦄ ⊢ T1 ⬌*[h] T2 & p1 = p2.
+#h #G #L #p1 #p2 #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-.
--- /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_lsubr.ma".
+include "basic_2/rt_equivalence/cpcs_cprs.ma".
+
+(* CONTEXT-SENSITIVE PARALLEL R-EQUIVALENCE FOR TERMS ***********************)
+
+(* Properties with restricted refinement for local environments *************)
+
+lemma lsubr_cpcs_trans (h) (G): lsub_trans … (cpcs h G) lsubr.
+#h #G #L1 #T1 #T2 #HT12 elim (cpcs_inv_cprs … HT12) -HT12
+/3 width=5 by cprs_div, lsubr_cpms_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/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"
- [ { "rt-equivalence" * } {
-(*
- [ { "decomposed rt-equivalence" * } {
- [ [ "" ] "scpes ( ⦃?,?⦄ ⊢ ? •*⬌*[?,?,?,?] ? )" "scpes_aaa" + "scpes_cpcs" + "scpes_scpes" * ]
- }
- ]
-*)
+ [ { "rt-equivalence" * } {
[ { "context-sensitive parallel r-equivalence" * } {
- [ [ "for terms" ] "cpcs ( ⦃?,?⦄ ⊢ ? ⬌*[?] ? )" (* "cpcs_aaa" + "cpcs_cprs" + "cpcs_cpcs" *) * ]
+ [ [ "for terms" ] "cpcs ( ⦃?,?⦄ ⊢ ? ⬌*[?] ? )" "cpcs_drops" + "cpcs_lsubr" + "cpcs_aaa" + "cpcs_cprs" + "cpcs_lprs" + "cpcs_cpc" + "cpcs_cpcs" * ]
}
]
}
]
class "sky"
[ { "rt-computation" * } {
-(*
- [ { "decomposed rt-computation" * } {
- "scpds_scpds"
- }
- ]
-*)
[ { "context-sensitive parallel r-computation" * } {
[ [ "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" + "( ⦃?,?⦄ ⊢ ? ➡*[?] ?)" * ]
class "italic" { 2 }
(*
+ [ { "decomposed rt-equivalence" * } {
+ [ [ "" ] "scpes ( ⦃?,?⦄ ⊢ ? •*⬌*[?,?,?,?] ? )" "scpes_aaa" + "scpes_cpcs" + "scpes_scpes" * ]
+ }
+ ]
[ [ "for lenvs on referred entries" ] "lfpxs" + "( ⦃?,?⦄ ⊢ ⬈*[?,?] ? )" "lfpxs_length" + "lfpxs_drops" + "lfpxs_fqup" + "lfpxs_lfdeq" + "lfpxs_ffdeq" + "lfpxs_aaa" + "lfpxs_cpxs" + "lfpxs_lpxs" + "lfpxs_lfpxs" * ]
[ [ "for lenvs on referred entries" ]
"lfpr" + "( ⦃?,?⦄ ⊢ ➡[?,?] ? )" "lfpr_length" + "lfpr_drops" + "lfpr_fquq" + "lfpr_fqup" + "lfpr_aaa" + "lfpr_lfpx" + "lfpr_lfpr" * ]
../../matitac.opt `cat partial.txt`
-cd basic_2/rt_equivalence/
-../../../../matitac.opt `cat partial.txt`
-cd ../dynamic/
+cd basic_2/dynamic/
../../../../matitac.opt `cat partial.txt`
cd ../../
basic_2/rt_transition
basic_2/rt_computation
basic_2/rt_conversion
+basic_2/rt_equivalence
apps_2/examples/ex_cpr_omega.ma
apps_2/models/
projects / helm.git / commitdiff