+++ /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 n ] break term 46 T2 )"
- non associative with precedence 45
- for @{ 'DPRedStar $h $o $n $G $L $T1 $T2 }.
+++ /dev/null
-(**************************************************************************)
-(* ___ *)
-(* ||M|| *)
-(* ||A|| A project by Andrea Asperti *)
-(* ||T|| *)
-(* ||I|| Developers: *)
-(* ||T|| The HELM team. *)
-(* ||A|| http://helm.cs.unibo.it *)
-(* \ / *)
-(* \ / This file is distributed under the terms of the *)
-(* v GNU General Public License Version 2 *)
-(* *)
-(**************************************************************************)
-
-(* NOTATION FOR THE FORMAL SYSTEM λδ ****************************************)
-
-notation "hvbox( ⦃ term 46 G, term 46 L ⦄ ⊢ break term 46 T1 ➡ * break term 46 T2 )"
- non associative with precedence 45
- for @{ 'PRedStar $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 @{ 'PRedStar $h $G $L $T1 $T2 }.
(* 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 T2 )"
+notation "hvbox( ⦃ term 46 G, break term 46 L ⦄ ⊢ break term 46 T1 ➡* [ break term 46 n, break term 46 h ] break term 46 T2 )"
non associative with precedence 45
- for @{ 'PRedStar $h $o $G $L $T1 $T2 }.
+ for @{ 'PRedStar $n $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/ltc.ma".
+include "basic_2/notation/relations/predstar_6.ma".
+include "basic_2/notation/relations/predstar_5.ma".
+include "basic_2/rt_transition/cpm.ma".
+
+(* T-BOUND CONTEXT-SENSITIVE PARALLEL RT-COMPUTATION FOR TERMS **************)
+
+(* Basic_2A1: uses: scpds *)
+definition cpms (h) (G) (L): relation3 nat term term ≝
+ ltc … plus … (cpm h G L).
+
+interpretation
+ "t-bound context-sensitive parallel rt-computarion (term)"
+ 'PRedStar n h G L T1 T2 = (cpms h G L n T1 T2).
+
+interpretation
+ "context-sensitive parallel r-computation (term)"
+ 'PRedStar h G L T1 T2 = (cpms h G L O T1 T2).
+
+(* Basic properties *********************************************************)
+
+lemma cpm_cpms (h) (G) (L): ∀n,T1,T2. ⦃G, L⦄ ⊢ T1 ➡[n, h] T2 → ⦃G, L⦄ ⊢ T1 ➡*[n, h] T2.
+/2 width=1 by ltc_rc/ qed.
+
+lemma cpms_step_sn (h) (G) (L): ∀n1,T1,T. ⦃G, L⦄ ⊢ T1 ➡[n1, h] T →
+ ∀n2,T2. ⦃G, L⦄ ⊢ T ➡*[n2, h] T2 → ⦃G, L⦄ ⊢ T1 ➡*[n1+n2, h] T2.
+/2 width=3 by ltc_sn/ qed-.
+
+lemma cpms_step_dx (h) (G) (L): ∀n1,T1,T. ⦃G, L⦄ ⊢ T1 ➡*[n1, h] T →
+ ∀n2,T2. ⦃G, L⦄ ⊢ T ➡[n2, h] T2 → ⦃G, L⦄ ⊢ T1 ➡*[n1+n2, h] T2.
+/2 width=3 by ltc_dx/ qed-.
+
+(* Basic properties with r-transition ***************************************)
+
+lemma cprs_refl: ∀h,G,L. reflexive … (cpms h G L 0).
+/2 width=1 by cpm_cpms/ qed.
+
+(* Basic eliminators ********************************************************)
+
+lemma cpms_ind_sn (h) (G) (L) (T2) (Q:relation2 …):
+ Q 0 T2 →
+ (∀n1,n2,T1,T. ⦃G, L⦄ ⊢ T1 ➡[n1, h] T → ⦃G, L⦄ ⊢ T ➡*[n2, h] T2 → Q n2 T → Q (n1+n2) T1) →
+ ∀n,T1. ⦃G, L⦄ ⊢ T1 ➡*[n, h] T2 → Q n T1.
+#h #G #L #T2 #R @ltc_ind_sn_refl //
+qed-.
+
+lemma cpms_ind_dx (h) (G) (L) (T1) (Q:relation2 …):
+ Q 0 T1 →
+ (∀n1,n2,T,T2. ⦃G, L⦄ ⊢ T1 ➡*[n1, h] T → Q n1 T → ⦃G, L⦄ ⊢ T ➡[n2, h] T2 → Q (n1+n2) T2) →
+ ∀n,T2. ⦃G, L⦄ ⊢ T1 ➡*[n, h] T2 → Q n T2.
+#h #G #L #T1 #R @ltc_ind_dx_refl //
+qed-.
+
+(* Basic_2A1: removed theorems 4:
+ sta_cprs_scpds lstas_scpds scpds_strap1 scpds_fwd_cprs
+*)
include "basic_2/notation/relations/predtystar_5.ma".
include "basic_2/rt_transition/cpx.ma".
-(* UNCOUNTED CONTEXT-SENSITIVE PARALLEL RT-COMPUTATION FOR TERMS ************)
+(* UNBOUND CONTEXT-SENSITIVE PARALLEL RT-COMPUTATION FOR TERMS **************)
definition cpxs: sh → relation4 genv lenv term term ≝
λh,G. CTC … (cpx h G).
-interpretation "uncounted context-sensitive parallel rt-computation (term)"
+interpretation "unbound context-sensitive parallel rt-computation (term)"
'PRedTyStar h G L T1 T2 = (cpxs h G L T1 T2).
(* Basic eliminators ********************************************************)
include "basic_2/rt_transition/lfpx_aaa.ma".
include "basic_2/rt_computation/cpxs.ma".
-(* UNCOUNTED CONTEXT-SENSITIVE PARALLEL RT-COMPUTATION FOR TERMS ************)
+(* UNBOUND CONTEXT-SENSITIVE PARALLEL RT-COMPUTATION FOR TERMS **************)
(* Properties with atomic arity assignment on terms *************************)
include "basic_2/rt_transition/cnx_cnx.ma".
include "basic_2/rt_computation/cpxs.ma".
-(* UNCOUNTED CONTEXT-SENSITIVE PARALLEL RT-COMPUTATION FOR TERMS ************)
+(* UNBOUND CONTEXT-SENSITIVE PARALLEL RT-COMPUTATION FOR TERMS **************)
(* Inversion lemmas with normal terms ***************************************)
include "basic_2/rt_transition/cpx_lsubr.ma".
include "basic_2/rt_computation/cpxs.ma".
-(* UNCOUNTED CONTEXT-SENSITIVE PARALLEL RT-COMPUTATION FOR TERMS ************)
+(* UNBOUND CONTEXT-SENSITIVE PARALLEL RT-COMPUTATION FOR TERMS **************)
(* Main properties **********************************************************)
include "basic_2/rt_transition/cpx_drops.ma".
include "basic_2/rt_computation/cpxs.ma".
-(* UNCOUNTED CONTEXT-SENSITIVE PARALLEL RT-COMPUTATION FOR TERMS ************)
+(* UNBOUND CONTEXT-SENSITIVE PARALLEL RT-COMPUTATION FOR TERMS **************)
(* Advanced properties ******************************************************)
include "basic_2/syntax/cext2.ma".
include "basic_2/rt_computation/cpxs.ma".
-(* UNCOUNTED CONTEXT-SENSITIVE PARALLEL RT-COMPUTATION FOR BINDERS **********)
+(* UNBOUND CONTEXT-SENSITIVE PARALLEL RT-COMPUTATION FOR BINDERS ************)
definition cpxs_ext (h) (G): relation3 lenv bind bind ≝
cext2 (cpxs h G).
interpretation
- "uncounted context-sensitive parallel rt-computation (binder)"
+ "unbound context-sensitive parallel rt-computation (binder)"
'PRedTyStar h G L I1 I2 = (cpxs_ext h G L I1 I2).
include "basic_2/static/ffdeq.ma".
include "basic_2/rt_computation/cpxs_lfdeq.ma".
-(* UNCOUNTED CONTEXT-SENSITIVE PARALLEL RT-COMPUTATION FOR TERMS ************)
+(* UNBOUND CONTEXT-SENSITIVE PARALLEL RT-COMPUTATION FOR TERMS **************)
(* Properties with degree-based equivalence for closures ********************)
(* *)
(**************************************************************************)
-(* UNCOUNTED CONTEXT-SENSITIVE PARALLEL RT-COMPUTATION FOR TERMS ************)
+(* UNBOUND CONTEXT-SENSITIVE PARALLEL RT-COMPUTATION FOR TERMS **************)
include "basic_2/rt_transition/cpx_fqus.ma".
include "basic_2/rt_computation/cpxs_drops.ma".
include "basic_2/rt_transition/cpx_lfdeq.ma".
include "basic_2/rt_computation/cpxs_tdeq.ma".
-(* UNCOUNTED CONTEXT-SENSITIVE PARALLEL RT-COMPUTATION FOR TERMS ************)
+(* UNBOUND CONTEXT-SENSITIVE PARALLEL RT-COMPUTATION FOR TERMS **************)
(* Properties with degree-based equivalence for local environments **********)
include "basic_2/rt_computation/cpxs_drops.ma".
include "basic_2/rt_computation/cpxs_cpxs.ma".
-(* UNCOUNTED CONTEXT-SENSITIVE PARALLEL RT-COMPUTATION FOR TERMS ************)
+(* UNBOUND CONTEXT-SENSITIVE PARALLEL RT-COMPUTATION FOR TERMS **************)
-(* Properties with uncounted parallel rt-transition on referred entries *****)
+(* Properties with unbound parallel rt-transition on referred entries *******)
lemma lfpx_cpxs_conf: ∀h,G. s_r_confluent1 … (cpxs h G) (lfpx h G).
/3 width=5 by lfpx_cpx_conf, s_r_conf1_CTC1/ qed-.
include "basic_2/rt_computation/cpxs_drops.ma".
include "basic_2/rt_computation/cpxs_cpxs.ma".
-(* UNCOUNTED CONTEXT-SENSITIVE PARALLEL RT-COMPUTATION FOR TERMS ************)
+(* UNBOUND CONTEXT-SENSITIVE PARALLEL RT-COMPUTATION FOR TERMS **************)
-(* Properties with uncounted parallel rt-transition for local environments **)
+(* Properties with unbound parallel rt-transition for local environments ****)
lemma lpx_cpx_trans: ∀h,G. s_r_transitive … (cpx h G) (λ_.lpx h G).
#h #G #L2 #T1 #T2 #H @(cpx_ind … H) -G -L2 -T1 -T2
include "basic_2/rt_transition/cpx_lsubr.ma".
include "basic_2/rt_computation/cpxs.ma".
-(* UNCOUNTED CONTEXT-SENSITIVE PARALLEL RT-COMPUTATION FOR TERMS ************)
+(* UNBOUND CONTEXT-SENSITIVE PARALLEL RT-COMPUTATION FOR TERMS **************)
(* Properties with restricted refinement for local environments *************)
include "basic_2/rt_transition/lfpx_lfdeq.ma".
include "basic_2/rt_computation/cpxs.ma".
-(* UNCOUNTED CONTEXT-SENSITIVE PARALLEL RT-COMPUTATION FOR TERMS ************)
+(* UNBOUND CONTEXT-SENSITIVE PARALLEL RT-COMPUTATION FOR TERMS **************)
(* Properties with degree-based equivalence for terms ***********************)
include "basic_2/rt_computation/cpxs_cnx.ma".
include "basic_2/rt_computation/lfpxs_cpxs.ma".
-(* UNCOUNTED CONTEXT-SENSITIVE PARALLEL RT-COMPUTATION FOR TERMS ************)
+(* UNBOUND CONTEXT-SENSITIVE PARALLEL RT-COMPUTATION FOR TERMS **************)
(* Forward lemmas with head equivalence for terms ***************************)
include "basic_2/relocation/lifts_vector.ma".
include "basic_2/rt_computation/cpxs_theq.ma".
-(* UNCOUNTED CONTEXT-SENSITIVE PARALLEL RT-COMPUTATION FOR TERMS ************)
+(* UNBOUND CONTEXT-SENSITIVE PARALLEL RT-COMPUTATION FOR TERMS **************)
(* Vector form of forward lemmas with head equivalence for terms ************)
include "basic_2/syntax/tdeq.ma".
include "basic_2/rt_transition/cpx.ma".
-(* STRONGLY NORMALIZING TERMS FOR UNCOUNTED PARALLEL RT-TRANSITION **********)
+(* STRONGLY NORMALIZING TERMS FOR UNBOUND PARALLEL RT-TRANSITION ************)
definition csx: ∀h. sd h → relation3 genv lenv term ≝
λh,o,G,L. SN … (cpx h G L) (tdeq h o …).
interpretation
- "strong normalization for uncounted context-sensitive parallel rt-transition (term)"
+ "strong normalization for unbound context-sensitive parallel rt-transition (term)"
'PRedTyStrong h o G L T = (csx h o G L T).
(* Basic eliminators ********************************************************)
include "basic_2/rt_computation/csx_gcp.ma".
include "basic_2/rt_computation/csx_gcr.ma".
-(* STRONGLY NORMALIZING TERMS FOR UNCOUNTED PARALLEL RT-TRANSITION **********)
+(* STRONGLY NORMALIZING TERMS FOR UNBOUND PARALLEL RT-TRANSITION ************)
(* Main properties with atomic arity assignment *****************************)
(* *)
(**************************************************************************)
-(* STRONGLY NORMALIZING TERMS FOR UNCOUNTED PARALLEL RT-TRANSITION **********)
+(* STRONGLY NORMALIZING TERMS FOR UNBOUND PARALLEL RT-TRANSITION ************)
include "basic_2/rt_transition/cnx.ma".
include "basic_2/rt_computation/csx.ma".
-(* Properties with normal terms for uncounted parallel rt-transition ********)
+(* Properties with normal terms for unbound parallel rt-transition **********)
(* Basic_1: was just: sn3_nf2 *)
lemma cnx_csx: ∀h,o,G,L,T. ⦃G, L⦄ ⊢ ⬈[h, o] 𝐍⦃T⦄ → ⦃G, L⦄ ⊢ ⬈*[h, o] 𝐒⦃T⦄.
(* *)
(**************************************************************************)
-(* STRONGLY NORMALIZING TERM VECTORS FOR UNCOUNTED PARALLEL RT-TRANSITION ***)
+(* STRONGLY NORMALIZING TERM VECTORS FOR UNBOUND PARALLEL RT-TRANSITION *****)
include "basic_2/rt_computation/cpxs_theq_vector.ma".
include "basic_2/rt_computation/csx_simple_theq.ma".
include "basic_2/rt_computation/csx_cpxs.ma".
include "basic_2/rt_computation/csx_vector.ma".
-(* Properties with normal terms for uncounted parallel rt-transition ********)
+(* Properties with normal terms for unbound parallel rt-transition **********)
(* Basic_1: was just: sn3_appls_lref *)
lemma csx_applv_cnx: ∀h,o,G,L,T. 𝐒⦃T⦄ → ⦃G, L⦄ ⊢ ⬈[h, o] 𝐍⦃T⦄ →
include "basic_2/rt_computation/cpxs_cpxs.ma".
include "basic_2/rt_computation/csx_csx.ma".
-(* UNCOUNTED CONTEXT-SENSITIVE PARALLEL RT-COMPUTATION FOR TERMS ************)
+(* UNBOUND CONTEXT-SENSITIVE PARALLEL RT-COMPUTATION FOR TERMS **************)
-(* Properties with uncounted context-sensitive rt-computation for terms *****)
+(* Properties with unbound context-sensitive rt-computation for terms *******)
(* Basic_1: was just: sn3_intro *)
lemma csx_intro_cpxs: ∀h,o,G,L,T1.
/2 width=3 by csx_cpx_trans/
qed-.
-(* Eliminators with uncounted context-sensitive rt-computation for terms ****)
+(* Eliminators with unbound context-sensitive rt-computation for terms ******)
lemma csx_ind_cpxs_tdeq: ∀h,o,G,L. ∀R:predicate term.
(∀T1. ⦃G, L⦄ ⊢ ⬈*[h, o] 𝐒⦃T1⦄ →
include "basic_2/rt_transition/lfpx_lfdeq.ma".
include "basic_2/rt_computation/csx_drops.ma".
-(* STRONGLY NORMALIZING TERMS FOR UNCOUNTED PARALLEL RT-TRANSITION **********)
+(* STRONGLY NORMALIZING TERMS FOR UNBOUND PARALLEL RT-TRANSITION ************)
(* Advanced properties ******************************************************)
include "basic_2/rt_computation/csx_lfpx.ma".
include "basic_2/rt_computation/csx_vector.ma".
-(* STRONGLY NORMALIZING TERM VECTORS FOR UNCOUNTED PARALLEL RT-TRANSITION ***)
+(* STRONGLY NORMALIZING TERM VECTORS FOR UNBOUND PARALLEL RT-TRANSITION *****)
(* Advanced properties ************************************* ****************)
include "basic_2/rt_transition/cpx_drops.ma".
include "basic_2/rt_computation/csx.ma".
-(* STRONGLY NORMALIZING TERMS FOR UNCOUNTED PARALLEL RT-TRANSITION **********)
+(* STRONGLY NORMALIZING TERMS FOR UNBOUND PARALLEL RT-TRANSITION ************)
(* Properties with generic relocation ***************************************)
include "basic_2/static/ffdeq.ma".
include "basic_2/rt_computation/csx_lfdeq.ma".
-(* STRONGLY NORMALIZING TERMS FOR UNCOUNTED PARALLEL RT-TRANSITION **********)
+(* STRONGLY NORMALIZING TERMS FOR UNBOUND PARALLEL RT-TRANSITION ************)
(* Properties with degree-based equivalence for closures ********************)
include "basic_2/rt_computation/csx_ffdeq.ma".
include "basic_2/rt_computation/csx_lfpx.ma".
-(* STRONGLY NORMALIZING TERMS FOR UNCOUNTED PARALLEL RT-TRANSITION **********)
+(* STRONGLY NORMALIZING TERMS FOR UNBOUND PARALLEL RT-TRANSITION ************)
(* Properties with parallel rst-transition for closures *********************)
include "basic_2/s_computation/fqus.ma".
include "basic_2/rt_computation/csx_lsubr.ma".
-(* STRONGLY NORMALIZING TERMS FOR UNCOUNTED PARALLEL RT-TRANSITION **********)
+(* STRONGLY NORMALIZING TERMS FOR UNBOUND PARALLEL RT-TRANSITION ************)
(* Properties with extended supclosure **************************************)
include "basic_2/rt_transition/cnx_drops.ma".
include "basic_2/rt_computation/csx_drops.ma".
-(* STRONGLY NORMALIZING TERMS FOR UNCOUNTED PARALLEL RT-TRANSITION **********)
+(* STRONGLY NORMALIZING TERMS FOR UNBOUND PARALLEL RT-TRANSITION ************)
(* Main properties with generic computation properties **********************)
include "basic_2/rt_computation/csx_cnx_vector.ma".
include "basic_2/rt_computation/csx_csx_vector.ma".
-(* STRONGLY NORMALIZING TERMS FOR UNCOUNTED PARALLEL RT-TRANSITION **********)
+(* STRONGLY NORMALIZING TERMS FOR UNBOUND PARALLEL RT-TRANSITION ************)
(* Main properties with generic candidates of reducibility ******************)
include "basic_2/rt_transition/cpx_lfdeq.ma".
include "basic_2/rt_computation/csx_csx.ma".
-(* STRONGLY NORMALIZING TERMS FOR UNCOUNTED PARALLEL RT-TRANSITION **********)
+(* STRONGLY NORMALIZING TERMS FOR UNBOUND PARALLEL RT-TRANSITION ************)
(* Properties with degree-based equivalence for local environments **********)
include "basic_2/rt_computation/cpxs_lfpx.ma".
include "basic_2/rt_computation/csx_cpxs.ma".
-(* STRONGLY NORMALIZING TERMS FOR UNCOUNTED PARALLEL RT-TRANSITION **********)
+(* STRONGLY NORMALIZING TERMS FOR UNBOUND PARALLEL RT-TRANSITION ************)
-(* Properties with uncounted parallel rt-transition on referred entries *****)
+(* Properties with unbound parallel rt-transition on referred entries *******)
(* Basic_2A1: was just: csx_lpx_conf *)
lemma csx_lfpx_conf: ∀h,o,G,L1,T. ⦃G, L1⦄ ⊢ ⬈*[h, o] 𝐒⦃T⦄ →
include "basic_2/rt_computation/csx_lfpx.ma".
include "basic_2/rt_computation/lfpxs_fqup.ma".
-(* STRONGLY NORMALIZING TERMS FOR UNCOUNTED PARALLEL RT-TRANSITION **********)
+(* STRONGLY NORMALIZING TERMS FOR UNBOUND PARALLEL RT-TRANSITION ************)
-(* Properties with uncounted parallel rt-computation on referred entries ****)
+(* Properties with unbound parallel rt-computation on referred entries ******)
(* Basic_2A1: uses: csx_lpxs_conf *)
lemma csx_lfpxs_conf: ∀h,o,G,L1,L2,T. ⦃G, L1⦄ ⊢ ⬈*[h, T] L2 →
include "basic_2/rt_transition/cpx_lsubr.ma".
include "basic_2/rt_computation/csx_csx.ma".
-(* STRONGLY NORMALIZING TERMS FOR UNCOUNTED PARALLEL RT-TRANSITION **********)
+(* STRONGLY NORMALIZING TERMS FOR UNBOUND PARALLEL RT-TRANSITION ************)
(* Advanced properties ******************************************************)
include "basic_2/rt_transition/cpx_simple.ma".
include "basic_2/rt_computation/csx_csx.ma".
-(* STRONGLY NORMALIZING TERMS FOR UNCOUNTED PARALLEL RT-TRANSITION **********)
+(* STRONGLY NORMALIZING TERMS FOR UNBOUND PARALLEL RT-TRANSITION ************)
(* Properties with simple terms *********************************************)
include "basic_2/rt_computation/cpxs.ma".
include "basic_2/rt_computation/csx_csx.ma".
-(* STRONGLY NORMALIZING TERMS FOR UNCOUNTED PARALLEL RT-TRANSITION **********)
+(* STRONGLY NORMALIZING TERMS FOR UNBOUND PARALLEL RT-TRANSITION ************)
(* Properties with head equivalence for terms *******************************)
include "basic_2/syntax/term_vector.ma".
include "basic_2/rt_computation/csx.ma".
-(* STRONGLY NORMALIZING TERMS VECTORS FOR UNCOUNTED PARALLEL RT-TRANSITION **)
+(* STRONGLY NORMALIZING TERMS VECTORS FOR UNBOUND PARALLEL RT-TRANSITION ****)
definition csxv: ∀h. sd h → relation3 genv lenv (list term) ≝
λh,o,G,L. all … (csx h o G L).
interpretation
- "strong normalization for uncounted context-sensitive parallel rt-transition (term vector)"
+ "strong normalization for unbound context-sensitive parallel rt-transition (term vector)"
'PRedTyStrong h o G L Ts = (csxv h o G L Ts).
(* Basic inversion lemmas ***************************************************)
include "basic_2/rt_computation/fpbs_cpxs.ma".
include "basic_2/rt_computation/fpbg.ma".
-(* PROPER PARALLEL RST-COMPUTATION FOR CLOSURES **************************)
+(* PROPER PARALLEL RST-COMPUTATION FOR CLOSURES *****************************)
-(* Properties with uncounted context-sensitive parallel rt-computation ******)
+(* Properties with unbound context-sensitive parallel rt-computation ********)
(* Basic_2A1: was: cpxs_fpbg *)
lemma cpxs_tdneq_fpbg: ∀h,o,G,L,T1,T2. ⦃G, L⦄ ⊢ T1 ⬈*[h] T2 →
(* PROPER PARALLEL RST-COMPUTATION FOR CLOSURES *****************************)
-(* Properties with uncounted parallel rt-computation on referred entries ****)
+(* Properties with unbound parallel rt-computation on referred entries ******)
(* Basic_2A1: uses: lpxs_fpbg *)
lemma lfpxs_lfdneq_fpbg: ∀h,o,G,L1,L2,T. ⦃G, L1⦄ ⊢ ⬈*[h, T] L2 →
(* PARALLEL RST-COMPUTATION FOR CLOSURES ************************************)
-(* Properties with uncounted context-sensitive parallel rt-transition *******)
+(* Properties with unbound context-sensitive parallel rt-transition *********)
(* Basic_2A1: uses: fpbs_cpx_trans_neq *)
lemma fpbs_cpx_tdneq_trans: ∀h,o,G1,G2,L1,L2,T1,T2. ⦃G1, L1, T1⦄ ≥[h, o] ⦃G2, L2, T2⦄ →
(* PARALLEL RST-COMPUTATION FOR CLOSURES ************************************)
-(* Properties with uncounted context-sensitive parallel rt-computation ******)
+(* Properties with unbound context-sensitive parallel rt-computation ********)
lemma cpxs_fpbs: ∀h,o,G,L,T1,T2. ⦃G, L⦄ ⊢ T1 ⬈*[h] T2 → ⦃G, L, T1⦄ ≥[h, o] ⦃G, L, T2⦄.
#h #o #G #L #T1 #T2 #H @(cpxs_ind … H) -T2
(* PARALLEL RST-COMPUTATION FOR CLOSURES ************************************)
-(* Properties with sn for uncounted parallel rt-transition for terms ********)
+(* Properties with sn for unbound parallel rt-transition for terms **********)
(* Basic_2A1: was: csx_fpbs_conf *)
lemma fpbs_csx_conf: ∀h,o,G1,L1,T1. ⦃G1, L1⦄ ⊢ ⬈*[h, o] 𝐒⦃T1⦄ →
(* PARALLEL RST-COMPUTATION FOR CLOSURES ************************************)
-(* Properties with uncounted parallel rt-computation on referred entries ****)
+(* Properties with unbound parallel rt-computation on referred entries ******)
(* Basic_2A1: uses: lpxs_fpbs *)
lemma lfpxs_fpbs: ∀h,o,G,L1,L2,T. ⦃G, L1⦄ ⊢ ⬈*[h, T] L2 → ⦃G, L1, T⦄ ≥[h, o] ⦃G, L2, T⦄.
∀L2. ⦃G2, L⦄ ⊢ ⬈*[h, T2] L2 → ⦃G1, L1, T1⦄ ≥[h, o] ⦃G2, L2, T2⦄.
/3 width=3 by fpbs_lfpxs_trans, fqus_fpbs/ qed.
-(* Properties with uncounted context-sensitive parallel rt-computation ******)
+(* Properties with unbound context-sensitive parallel rt-computation ********)
(* Basic_2A1: uses: cpxs_fqus_lpxs_fpbs *)
lemma cpxs_fqus_lfpxs_fpbs: ∀h,o,G1,L1,T1,T. ⦃G1, L1⦄ ⊢ T1 ⬈*[h] T →
(* PARALLEL RST-COMPUTATION FOR CLOSURES ************************************)
-(* Properties with uncounted parallel rt-computation on local environments **)
+(* Properties with unbound parallel rt-computation on local environments ****)
(* Basic_2A1: uses: fpbs_intro_alt *)
lemma fpbs_intro_star: ∀h,o,G1,L1,T1,T. ⦃G1, L1⦄ ⊢ T1 ⬈*[h] T →
∀G2,L2,T2. ⦃G, L0, T0⦄ ≛[h, o] ⦃G2, L2, T2⦄ → ⦃G1, L1, T1⦄ ≥[h, o] ⦃G2, L2, T2⦄ .
/3 width=9 by fpbs_intro_fstar, lfpxs_lpxs/ qed.
-(* Eliminators with uncounted parallel rt-computation on local environments *)
+(* Eliminators with unbound parallel rt-computation on local environments ***)
(* Basic_2A1: uses: fpbs_inv_alt *)
lemma fpbs_inv_star: ∀h,o,G1,G2,L1,L2,T1,T2. ⦃G1, L1, T1⦄ ≥[h, o] ⦃G2, L2, T2⦄ →
include "basic_2/i_static/tc_lfxs.ma".
include "basic_2/rt_transition/lfpx.ma".
-(* UNCOUNTED PARALLEL RT-COMPUTATION FOR LOCAL ENV.S ON REFERRED ENTRIES ****)
+(* UNBOUND PARALLEL RT-COMPUTATION FOR LOCAL ENV.S ON REFERRED ENTRIES ******)
definition lfpxs: ∀h. relation4 genv term lenv lenv ≝
λh,G. tc_lfxs (cpx h G).
interpretation
- "uncounted parallel rt-computation on referred entries (local environment)"
+ "unbound parallel rt-computation on referred entries (local environment)"
'PRedTySnStar h T G L1 L2 = (lfpxs h G T L1 L2).
(* Basic properties *********************************************************)
include "basic_2/rt_transition/lfpx_aaa.ma".
include "basic_2/rt_computation/lfpxs.ma".
-(* UNCOUNTED PARALLEL RT-COMPUTATION FOR LOCAL ENV.S ON REFERRED ENTRIES ****)
+(* UNBOUND PARALLEL RT-COMPUTATION FOR LOCAL ENV.S ON REFERRED ENTRIES ******)
-(* Properties with atomic arity assignment on terms **************************)
+(* Properties with atomic arity assignment on terms *************************)
(* Basic_2A1: uses: lpxs_aaa_conf *)
lemma lfpxs_aaa_conf: ∀h,G,T. Conf3 … (λL. aaa G L T) (lfpxs h G T).
include "basic_2/rt_computation/cpxs_lfpx.ma".
include "basic_2/rt_computation/lfpxs_fqup.ma".
-(* UNCOUNTED PARALLEL RT-COMPUTATION FOR LOCAL ENV.S ON REFERRED ENTRIES ****)
+(* UNBOUND PARALLEL RT-COMPUTATION FOR LOCAL ENV.S ON REFERRED ENTRIES ******)
-(* Properties with uncounted context-sensitive rt-computation for terms *****)
+(* Properties with unbound context-sensitive rt-computation for terms *******)
(* Basic_2A1: uses: lpxs_pair lpxs_pair_refl *)
lemma lfpxs_pair_refl: ∀h,G,L,V1,V2. ⦃G, L⦄ ⊢ V1 ⬈*[h] V2 →
@s_rs_trans_TC1 /2 width=3 by lfpx_cpxs_trans/ (**) (* full auto too slow *)
qed-.
-(* Advanced properties on uncounted rt-computation for terms ****************)
+(* Advanced properties on unbound rt-computation for terms ******************)
lemma cpxs_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.
/4 width=3 by lfpxs_cpxs_trans, lfpxs_pair_refl, cpxs_bind/ qed.
-(* Advanced inversion lemmas on uncounted rt-computation for terms **********)
+(* Advanced inversion lemmas on unbound rt-computation for terms ************)
lemma cpxs_inv_abst1: ∀h,p,G,L,V1,T1,U2. ⦃G, L⦄ ⊢ ⓛ{p}V1.T1 ⬈*[h] U2 →
∃∃V2,T2. ⦃G, L⦄ ⊢ V1 ⬈*[h] V2 & ⦃G, L.ⓛV1⦄ ⊢ T1 ⬈*[h] T2 &
include "basic_2/i_static/tc_lfxs_drops.ma".
include "basic_2/rt_transition/lfpx_drops.ma".
-(* UNCOUNTED PARALLEL RT-COMPUTATION FOR LOCAL ENV.S ON REFERRED ENTRIES ****)
+(* UNBOUND PARALLEL RT-COMPUTATION FOR LOCAL ENV.S ON REFERRED ENTRIES ******)
(* Properties with generic slicing for local environments *******************)
include "basic_2/static/ffdeq.ma".
include "basic_2/rt_computation/lfpxs_lfdeq.ma".
-(* UNCOUNTED PARALLEL RT-COMPUTATION FOR LOCAL ENV.S ON REFERRED ENTRIES ****)
+(* UNBOUND PARALLEL RT-COMPUTATION FOR LOCAL ENV.S ON REFERRED ENTRIES ******)
(* Properties with degree-based equivalence on closures *********************)
include "basic_2/i_static/tc_lfxs_fqup.ma".
include "basic_2/rt_computation/lfpxs.ma".
-(* UNCOUNTED PARALLEL RT-COMPUTATION FOR LOCAL ENV.S ON REFERRED ENTRIES ****)
+(* UNBOUND PARALLEL RT-COMPUTATION FOR LOCAL ENV.S ON REFERRED ENTRIES ******)
(* Advanced properties ******************************************************)
include "basic_2/i_static/tc_lfxs_length.ma".
include "basic_2/rt_computation/lfpxs.ma".
-(* UNCOUNTED PARALLEL RT-COMPUTATION FOR LOCAL ENV.S ON REFERRED ENTRIES ****)
+(* UNBOUND PARALLEL RT-COMPUTATION FOR LOCAL ENV.S ON REFERRED ENTRIES ******)
(* Forward lemmas with length for local environments ************************)
include "basic_2/rt_transition/lfpx_lfdeq.ma".
include "basic_2/rt_computation/lfpxs_fqup.ma".
-(* UNCOUNTED PARALLEL RT-COMPUTATION FOR LOCAL ENV.S ON REFERRED ENTRIES ****)
+(* UNBOUND PARALLEL RT-COMPUTATION FOR LOCAL ENV.S ON REFERRED ENTRIES ******)
(* Properties with degree-based equivalence on terms ************************)
include "basic_2/i_static/tc_lfxs_tc_lfxs.ma".
include "basic_2/rt_computation/lfpxs.ma".
-(* UNCOUNTED PARALLEL RT-COMPUTATION FOR LOCAL ENV.S ON REFERRED ENTRIES ****)
+(* UNBOUND PARALLEL RT-COMPUTATION FOR LOCAL ENV.S ON REFERRED ENTRIES ******)
(* Main properties **********************************************************)
include "basic_2/rt_computation/lpxs.ma".
include "basic_2/rt_computation/lfpxs.ma".
-(* UNCOUNTED PARALLEL RT-COMPUTATION FOR LOCAL ENV.S ON REFERRED ENTRIES ****)
+(* UNBOUND PARALLEL RT-COMPUTATION FOR LOCAL ENV.S ON REFERRED ENTRIES ******)
-(* Properties with uncounted parallel rt-computation for local environments *)
+(* Properties with unbound parallel rt-computation for local environments ***)
lemma lfpxs_lpxs: ∀h,G,L1,L2,T. ⦃G, L1⦄ ⊢ ⬈*[h] L2 → ⦃G, L1⦄ ⊢ ⬈*[h, T] L2.
/2 width=1 by tc_lfxs_lex/ qed.
∀L2,T. L ≡[T] L2 → ⦃G, L1⦄ ⊢ ⬈*[h, T] L2.
/2 width=3 by tc_lfxs_lex_lfeq/ qed.
-(* Inversion lemmas with uncounted parallel rt-computation for local envs ***)
+(* Inversion lemmas with unbound parallel rt-computation for local envs *****)
lemma lfpxs_inv_lpxs_lfeq: ∀h,G,L1,L2,T. ⦃G, L1⦄ ⊢ ⬈*[h, T] L2 →
∃∃L. ⦃G, L1⦄ ⊢ ⬈*[h] L & L ≡[T] L2.
include "basic_2/static/lfdeq.ma".
include "basic_2/rt_transition/lfpx.ma".
-(* STRONGLY NORMALIZING LOCAL ENV.S FOR UNCOUNTED PARALLEL RT-TRANSITION ****)
+(* STRONGLY NORMALIZING LOCAL ENV.S FOR UNBOUND PARALLEL RT-TRANSITION ******)
definition lfsx: ∀h. sd h → relation3 term genv lenv ≝
λh,o,T,G. SN … (lfpx h G T) (lfdeq h o T).
interpretation
- "strong normalization for uncounted context-sensitive parallel rt-transition on referred entries (local environment)"
+ "strong normalization for unbound context-sensitive parallel rt-transition on referred entries (local environment)"
'PRedTySNStrong h o T G L = (lfsx h o T G L).
(* Basic eliminators ********************************************************)
include "basic_2/rt_computation/lfsx_lpx.ma".
include "basic_2/rt_computation/lsubsx_lfsx.ma".
-(* STRONGLY NORMALIZING LOCAL ENV.S FOR UNCOUNTED PARALLEL RT-TRANSITION ****)
+(* STRONGLY NORMALIZING LOCAL ENV.S FOR UNBOUND PARALLEL RT-TRANSITION ******)
(* Advanced properties ******************************************************)
include "basic_2/rt_transition/lfpx_drops.ma".
include "basic_2/rt_computation/lfsx_fqup.ma".
-(* STRONGLY NORMALIZING LOCAL ENV.S FOR UNCOUNTED PARALLEL RT-TRANSITION ****)
+(* STRONGLY NORMALIZING LOCAL ENV.S FOR UNBOUND PARALLEL RT-TRANSITION ******)
(* Properties with generic relocation ***************************************)
include "basic_2/static/lfdeq_fqup.ma".
include "basic_2/rt_computation/lfsx.ma".
-(* STRONGLY NORMALIZING LOCAL ENV.S FOR UNCOUNTED PARALLEL RT-TRANSITION ****)
+(* STRONGLY NORMALIZING LOCAL ENV.S FOR UNBOUND PARALLEL RT-TRANSITION ******)
(* Advanced properties ******************************************************)
include "basic_2/rt_computation/lfpxs_lfpxs.ma".
include "basic_2/rt_computation/lfsx_lfsx.ma".
-(* STRONGLY NORMALIZING LOCAL ENV.S FOR UNCOUNTED PARALLEL RT-TRANSITION ****)
+(* STRONGLY NORMALIZING LOCAL ENV.S FOR UNBOUND PARALLEL RT-TRANSITION ******)
-(* Properties with uncounted rt-computation on referred entries *************)
+(* Properties with unbound rt-computation on referred entries ***************)
(* Basic_2A1: uses: lsx_intro_alt *)
lemma lfsx_intro_lfpxs: ∀h,o,G,L1,T.
/2 width=3 by lfsx_lfpx_trans/
qed-.
-(* Eliminators with uncounted rt-computation on referred entries ************)
+(* Eliminators with unbound rt-computation on referred entries **************)
lemma lfsx_ind_lfpxs_lfdeq: ∀h,o,G,T. ∀R:predicate lenv.
(∀L1. G ⊢ ⬈*[h, o, T] 𝐒⦃L1⦄ →
include "basic_2/rt_transition/lfpx_lfdeq.ma".
include "basic_2/rt_computation/lfsx.ma".
-(* STRONGLY NORMALIZING LOCAL ENV.S FOR UNCOUNTED PARALLEL RT-TRANSITION ****)
+(* STRONGLY NORMALIZING LOCAL ENV.S FOR UNBOUND PARALLEL RT-TRANSITION ******)
(* Advanced properties ******************************************************)
include "basic_2/rt_transition/lfpx_lpx.ma".
include "basic_2/rt_computation/lfsx_lfsx.ma".
-(* STRONGLY NORMALIZING LOCAL ENV.S FOR UNCOUNTED PARALLEL RT-TRANSITION ****)
+(* STRONGLY NORMALIZING LOCAL ENV.S FOR UNBOUND PARALLEL RT-TRANSITION ******)
-(* Properties with uncounted rt-transition **********************************)
+(* Properties with unbound rt-transition ************************************)
lemma lfsx_intro_lpx: ∀h,o,G,L1,T.
(∀L2. ⦃G, L1⦄ ⊢ ⬈[h] L2 → (L1 ≛[h, o, T] L2 → ⊥) → G ⊢ ⬈*[h, o, T] 𝐒⦃L2⦄) →
∀L2. ⦃G, L1⦄ ⊢ ⬈[h] L2 → G ⊢ ⬈*[h, o, T] 𝐒⦃L2⦄.
/3 width=3 by lfsx_lfpx_trans, lfpx_lpx/ qed-.
-(* Eliminators with uncounted rt-transition *********************************)
+(* Eliminators with unbound rt-transition ***********************************)
lemma lfsx_ind_lpx: ∀h,o,G,T. ∀R:predicate lenv.
(∀L1. G ⊢ ⬈*[h, o, T] 𝐒⦃L1⦄ →
include "basic_2/rt_computation/lfpxs_lpxs.ma".
include "basic_2/rt_computation/lfsx_lfpxs.ma".
-(* STRONGLY NORMALIZING LOCAL ENV.S FOR UNCOUNTED PARALLEL RT-TRANSITION ****)
+(* STRONGLY NORMALIZING LOCAL ENV.S FOR UNBOUND PARALLEL RT-TRANSITION ******)
-(* Properties with uncounted rt-computation *********************************)
+(* Properties with unbound rt-computation ***********************************)
lemma lfsx_intro_lpxs: ∀h,o,G,L1,T.
(∀L2. ⦃G, L1⦄ ⊢ ⬈*[h] L2 → (L1 ≛[h, o, T] L2 → ⊥) → G ⊢ ⬈*[h, o, T] 𝐒⦃L2⦄) →
∀L2. ⦃G, L1⦄ ⊢ ⬈*[h] L2 → G ⊢ ⬈*[h, o, T] 𝐒⦃L2⦄.
/3 width=3 by lfsx_lfpxs_trans, lfpxs_lpxs/ qed-.
-(* Eliminators with uncounted rt-computation ********************************)
+(* Eliminators with unbound rt-computation **********************************)
lemma lfsx_ind_lpxs: ∀h,o,G,T. ∀R:predicate lenv.
(∀L1. G ⊢ ⬈*[h, o, T] 𝐒⦃L1⦄ →
include "basic_2/relocation/lex.ma".
include "basic_2/rt_computation/cpxs_ext.ma".
-(* UNCOUNTED PARALLEL RT-COMPUTATION FOR LOCAL ENVIRONMENTS *****************)
+(* UNBOUND PARALLEL RT-COMPUTATION FOR LOCAL ENVIRONMENTS *******************)
definition lpxs: ∀h. relation3 genv lenv lenv ≝
λh,G. lex (cpxs h G).
interpretation
- "uncounted parallel rt-computation (local environment)"
+ "unbound parallel rt-computation (local environment)"
'PRedTySnStar h G L1 L2 = (lpxs h G L1 L2).
(* Basic properties *********************************************************)
include "basic_2/rt_computation/lfpxs_cpxs.ma".
include "basic_2/rt_computation/lfpxs_lpxs.ma".
-(* UNCOUNTED PARALLEL RT-COMPUTATION FOR LOCAL ENVIRONMENTS *****************)
+(* UNBOUND PARALLEL RT-COMPUTATION FOR LOCAL ENVIRONMENTS *******************)
-(* Properties with uncounted context-sensitive rt-computation for terms *****)
+(* Properties with unbound context-sensitive rt-computation for terms *******)
lemma lpxs_cpx_trans: ∀h,G. s_r_transitive … (cpx h G) (λ_.lpxs h G).
/3 width=3 by lfpxs_cpx_trans, lfpxs_lpxs/ qed-.
include "basic_2/relocation/lex_length.ma".
include "basic_2/rt_computation/lpxs.ma".
-(* UNCOUNTED PARALLEL RT-COMPUTATION FOR LOCAL ENVIRONMENTS *****************)
+(* UNBOUND PARALLEL RT-COMPUTATION FOR LOCAL ENVIRONMENTS *******************)
(* Forward lemmas with length for local environments ************************)
include "basic_2/rt_computation/lpxs.ma".
include "basic_2/rt_computation/cpxs_lpx.ma".
-(* UNCOUNTED PARALLEL RT-COMPUTATION FOR LOCAL ENVIRONMENTS *****************)
+(* UNBOUND PARALLEL RT-COMPUTATION FOR LOCAL ENVIRONMENTS *******************)
-(* Properties with uncounted rt-transition for local environments ***********)
+(* Properties with unbound rt-transition for local environments *************)
(* Basic_2A1: was: lpxs_strap1 *)
lemma lpxs_step_dx: ∀h,G,L1,L. ⦃G, L1⦄ ⊢ ⬈*[h] L →
include "basic_2/notation/relations/lsubeqx_6.ma".
include "basic_2/rt_computation/lfsx.ma".
-(* CLEAR OF STRONGLY NORMALIZING ENTRIES FOR UNCOUNTED RT-TRANSITION ********)
+(* CLEAR OF STRONGLY NORMALIZING ENTRIES FOR UNBOUND RT-TRANSITION **********)
(* Note: this should be an instance of a more general lexs *)
(* Basic_2A1: uses: lcosx *)
include "basic_2/rt_computation/lfsx_lfpxs.ma".
include "basic_2/rt_computation/lsubsx.ma".
-(* CLEAR OF STRONGLY NORMALIZING ENTRIES FOR UNCOUNTED RT-TRANSITION ********)
+(* CLEAR OF STRONGLY NORMALIZING ENTRIES FOR UNBOUND RT-TRANSITION **********)
-(* Properties with strong normalizing env's for uncounted rt-transition *****)
+(* Properties with strong normalizing env's for unbound rt-transition *******)
(* Basic_2A1: uses: lsx_cpx_trans_lcosx *)
lemma lfsx_cpx_trans_lsubsx: ∀h,o,G,L0,T1,T2. ⦃G, L0⦄ ⊢ T1 ⬈[h] T2 →
G ⊢ ⬈*[h, o, T1] 𝐒⦃L⦄ → G ⊢ ⬈*[h, o, T2] 𝐒⦃L⦄.
/3 width=6 by lfsx_cpx_trans_lsubsx, lsubsx_refl/ qed-.
-(* Properties with strong normalizing env's for uncounted rt-computation ****)
+(* Properties with strong normalizing env's for unbound rt-computation ******)
lemma lfsx_cpxs_trans: ∀h,o,G,L,T1,T2. ⦃G, L⦄ ⊢ T1 ⬈*[h] T2 →
G ⊢ ⬈*[h, o, T1] 𝐒⦃L⦄ → G ⊢ ⬈*[h, o, T2] 𝐒⦃L⦄.
include "basic_2/rt_computation/lsubsx.ma".
-(* CLEAR OF STRONGLY NORMALIZING ENTRIES FOR UNCOUNTED RT-TRANSITION ********)
+(* CLEAR OF STRONGLY NORMALIZING ENTRIES FOR UNBOUND RT-TRANSITION **********)
(* Main properties **********************************************************)
fpbs.ma fpbs_fqup.ma fpbs_fqus.ma fpbs_aaa.ma fpbs_cpx.ma fpbs_fpb.ma fpbs_cpxs.ma fpbs_lpxs.ma fpbs_lfpxs.ma fpbs_csx.ma fpbs_fpbs.ma
fpbg.ma fpbg_fqup.ma fpbg_cpxs.ma fpbg_lfpxs.ma fpbg_fpbs.ma fpbg_fpbg.ma
fsb.ma fsb_ffdeq.ma fsb_aaa.ma fsb_csx.ma fsb_fpbg.ma
+cpms.ma
+++ /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/dpredstar_7.ma".
-include "basic_2/static/da.ma".
-include "basic_2/computation/cprs.ma".
-
-(* STRATIFIED DECOMPOSED PARALLEL COMPUTATION ON TERMS **********************)
-
-definition scpds: ∀h. sd h → nat → relation4 genv lenv term term ≝
- λh,o,d2,G,L,T1,T2.
- ∃∃T,d1. d2 ≤ d1 & ⦃G, L⦄ ⊢ T1 ▪[h, o] d1 & ⦃G, L⦄ ⊢ T1 •*[h, d2] T & ⦃G, L⦄ ⊢ T ➡* T2.
-
-interpretation "stratified decomposed parallel computation (term)"
- 'DPRedStar h o d G L T1 T2 = (scpds h o d G L T1 T2).
-
-(* Basic properties *********************************************************)
-
-lemma sta_cprs_scpds: ∀h,o,G,L,T1,T,T2,d. ⦃G, L⦄ ⊢ T1 ▪[h, o] d+1 → ⦃G, L⦄ ⊢ T1 •*[h, 1] T →
- ⦃G, L⦄ ⊢ T ➡* T2 → ⦃G, L⦄ ⊢ T1 •*➡*[h, o, 1] T2.
-/2 width=6 by ex4_2_intro/ qed.
-
-lemma lstas_scpds: ∀h,o,G,L,T1,T2,d1. ⦃G, L⦄ ⊢ T1 ▪[h, o] d1 →
- ∀d2. d2 ≤ d1 → ⦃G, L⦄ ⊢ T1 •*[h, d2] T2 → ⦃G, L⦄ ⊢ T1 •*➡*[h, o, d2] T2.
-/2 width=6 by ex4_2_intro/ qed.
-
-lemma scpds_strap1: ∀h,o,G,L,T1,T,T2,d.
- ⦃G, L⦄ ⊢ T1 •*➡*[h, o, d] T → ⦃G, L⦄ ⊢ T ➡ T2 → ⦃G, L⦄ ⊢ T1 •*➡*[h, o, d] T2.
-#h #o #G #L #T1 #T #T2 #d * /3 width=8 by cprs_strap1, ex4_2_intro/
-qed.
-
-(* Basic forward lemmas *****************************************************)
-
-lemma scpds_fwd_cprs: ∀h,o,G,L,T1,T2. ⦃G, L⦄ ⊢ T1 •*➡*[h, o, 0] T2 →
- ⦃G, L⦄ ⊢ T1 ➡* T2.
-#h #o #G #L #T1 #T2 * /3 width=3 by cprs_strap2, lstas_cpr/
-qed-.
include "basic_2/syntax/tdeq.ma".
include "basic_2/rt_transition/cpx.ma".
-(* NORMAL TERMS FOR UNCOUNTED CONTEXT-SENSITIVE PARALLEL RT-TRANSITION ******)
+(* NORMAL TERMS FOR UNBOUND CONTEXT-SENSITIVE PARALLEL RT-TRANSITION ********)
definition cnx: ∀h. sd h → relation3 genv lenv term ≝
λh,o,G,L. NF … (cpx h G L) (tdeq h o …).
interpretation
- "normality for uncounted context-sensitive parallel rt-transition (term)"
+ "normality for unbound context-sensitive parallel rt-transition (term)"
'PRedTyNormal h o G L T = (cnx h o G L T).
(* Basic inversion lemmas ***************************************************)
include "basic_2/rt_transition/lfpx_lfdeq.ma".
include "basic_2/rt_transition/cnx.ma".
-(* NORMAL TERMS FOR UNCOUNTED CONTEXT-SENSITIVE PARALLEL RT-TRANSITION ******)
+(* NORMAL TERMS FOR UNBOUND CONTEXT-SENSITIVE PARALLEL RT-TRANSITION ********)
(* Advanced properties ******************************************************)
include "basic_2/rt_transition/cpx_drops.ma".
include "basic_2/rt_transition/cnx.ma".
-(* NORMAL TERMS FOR UNCOUNTED CONTEXT-SENSITIVE PARALLEL RT-TRANSITION ******)
+(* NORMAL TERMS FOR UNBOUND CONTEXT-SENSITIVE PARALLEL RT-TRANSITION ********)
(* Properties with generic slicing ******************************************)
include "basic_2/rt_transition/cpx_simple.ma".
include "basic_2/rt_transition/cnx.ma".
-(* NORMAL TERMS FOR UNCOUNTED CONTEXT-SENSITIVE PARALLEL RT-TRANSITION ******)
+(* NORMAL TERMS FOR UNBOUND CONTEXT-SENSITIVE PARALLEL RT-TRANSITION ********)
(* Inversion lemmas with simple terms ***************************************)
include "basic_2/syntax/genv.ma".
include "basic_2/relocation/lifts.ma".
-(* COUNTED CONTEXT-SENSITIVE PARALLEL RT-TRANSITION FOR TERMS ***************)
+(* BOUND CONTEXT-SENSITIVE PARALLEL RT-TRANSITION FOR TERMS *****************)
(* avtivate genv *)
inductive cpg (Rt:relation rtc) (h): rtc → relation4 genv lenv term term ≝
.
interpretation
- "counted context-sensitive parallel rt-transition (term)"
+ "bound context-sensitive parallel rt-transition (term)"
'PRedTy Rt c h G L T1 T2 = (cpg Rt h c G L T1 T2).
(* Basic properties *********************************************************)
include "basic_2/s_computation/fqup_drops.ma".
include "basic_2/rt_transition/cpg.ma".
-(* COUNTED CONTEXT-SENSITIVE PARALLEL RT-TRANSITION FOR TERMS ***************)
+(* BOUND CONTEXT-SENSITIVE PARALLEL RT-TRANSITION FOR TERMS *****************)
(* Advanced properties ******************************************************)
include "basic_2/static/lsubr.ma".
include "basic_2/rt_transition/cpg.ma".
-(* COUNTED CONTEXT-SENSITIVE PARALLEL RT-TRANSITION FOR TERMS ***************)
+(* BOUND CONTEXT-SENSITIVE PARALLEL RT-TRANSITION FOR TERMS *****************)
(* Properties with restricted refinement for local environments *************)
include "basic_2/syntax/term_simple.ma".
include "basic_2/rt_transition/cpg.ma".
-(* COUNTED CONTEXT-SENSITIVE PARALLEL RT-TRANSITION FOR TERMS ***************)
+(* BOUND CONTEXT-SENSITIVE PARALLEL RT-TRANSITION FOR TERMS *****************)
(* Properties with simple terms *********************************************)
(* T-BOUND CONTEXT-SENSITIVE PARALLEL RT-TRANSITION FOR TERMS ***************)
(* Basic_2A1: includes: cpr *)
-definition cpm (n) (h): relation4 genv lenv term term ≝
- λG,L,T1,T2. ∃∃c. 𝐑𝐓⦃n, c⦄ & ⦃G, L⦄ ⊢ T1 ⬈[eq_t, c, h] T2.
+definition cpm (h) (G) (L) (n): relation2 term term ≝
+ λT1,T2. ∃∃c. 𝐑𝐓⦃n, c⦄ & ⦃G, L⦄ ⊢ T1 ⬈[eq_t, c, h] T2.
interpretation
- "semi-counted context-sensitive parallel rt-transition (term)"
- 'PRed n h G L T1 T2 = (cpm n h G L T1 T2).
+ "t-bound context-sensitive parallel rt-transition (term)"
+ 'PRed n h G L T1 T2 = (cpm h G L n T1 T2).
interpretation
"context-sensitive parallel r-transition (term)"
- 'PRed h G L T1 T2 = (cpm O h G L T1 T2).
+ 'PRed h G L T1 T2 = (cpm h G L O T1 T2).
(* Basic properties *********************************************************)
/6 width=9 by cpg_theta, isrt_plus_O2, isrt_max, isr_shift, ex2_intro/
qed.
-(* Basic properties on r-transition *****************************************)
+(* Basic properties with r-transition ***************************************)
+(* Note: this is needed by cpms_ind_sn and cpms_ind_dx *)
(* Basic_1: includes by definition: pr0_refl *)
(* Basic_2A1: includes: cpr_atom *)
-lemma cpr_refl: ∀h,G,L. reflexive … (cpm 0 h G L).
+lemma cpr_refl: ∀h,G,L. reflexive … (cpm h G L 0).
/3 width=3 by cpg_refl, ex2_intro/ qed.
(* Basic inversion lemmas ***************************************************)
(* T-BOUND CONTEXT-SENSITIVE PARALLEL RT-TRANSITION FOR TERMS ***************)
-(* Forward lemmas with uncounted context-sensitive rt-transition for terms **)
+(* Forward lemmas with unbound context-sensitive rt-transition for terms ****)
(* Basic_2A1: includes: cpr_cpx *)
lemma cpm_fwd_cpx: ∀n,h,G,L,T1,T2. ⦃G, L⦄ ⊢ T1 ➡[n, h] T2 → ⦃G, L⦄ ⊢ T1 ⬈[h] T2.
(* Basic_1: includes: pr0_lift pr2_lift *)
(* Basic_2A1: includes: cpr_lift *)
-lemma cpm_lifts_sn: ∀n,h,G. d_liftable2_sn … lifts (cpm n h G).
+lemma cpm_lifts_sn: ∀n,h,G. d_liftable2_sn … lifts (λL. cpm h G L n).
#n #h #G #K #T1 #T2 * #c #Hc #HT12 #b #f #L #HLK #U1 #HTU1
elim (cpg_lifts_sn … HT12 … HLK … HTU1) -K -T1
/3 width=5 by ex2_intro/
qed-.
-lemma cpm_lifts_bi: ∀n,h,G. d_liftable2_bi … lifts (cpm n h G).
+lemma cpm_lifts_bi: ∀n,h,G. d_liftable2_bi … lifts (λL. cpm h G L n).
#n #h #G #K #T1 #T2 * /3 width=11 by cpg_lifts_bi, ex2_intro/
qed-.
(* Basic_1: includes: pr0_gen_lift pr2_gen_lift *)
(* Basic_2A1: includes: cpr_inv_lift1 *)
-lemma cpm_inv_lifts_sn: ∀n,h,G. d_deliftable2_sn … lifts (cpm n h G).
+lemma cpm_inv_lifts_sn: ∀n,h,G. d_deliftable2_sn … lifts (λL. cpm h G L n).
#n #h #G #L #U1 #U2 * #c #Hc #HU12 #b #f #K #HLK #T1 #HTU1
elim (cpg_inv_lifts_sn … HU12 … HLK … HTU1) -L -U1
/3 width=5 by ex2_intro/
qed-.
-lemma cpm_inv_lifts_bi: ∀n,h,G. d_deliftable2_bi … lifts (cpm n h G).
+lemma cpm_inv_lifts_bi: ∀n,h,G. d_deliftable2_bi … lifts (λL. cpm h G L n).
#n #h #G #L #U1 #U2 * /3 width=11 by cpg_inv_lifts_bi, ex2_intro/
qed-.
(* Forward lemmas with free variables inclusion for restricted closures *****)
-lemma cpm_fsge_comp: ∀n,h,G. R_fsge_compatible (cpm n h G).
+lemma cpm_fsge_comp: ∀n,h,G. R_fsge_compatible (λL. cpm h G L n).
/3 width=6 by cpm_fwd_cpx, cpx_fsge_comp/ qed-.
-lemma lfpr_fsge_comp: ∀h,G. lfxs_fsge_compatible (cpm 0 h G).
+lemma lfpr_fsge_comp: ∀h,G. lfxs_fsge_compatible (λL. cpm h G L 0).
/4 width=5 by cpm_fwd_cpx, lfpx_fsge_comp, lfxs_co/ qed-.
(* Properties with generic extension on referred entries ********************)
(* Basic_2A1: was just: cpr_llpx_sn_conf *)
-lemma cpm_lfxs_conf: ∀R,n,h,G. s_r_confluent1 … (cpm n h G) (lfxs R).
+lemma cpm_lfxs_conf: ∀R,n,h,G. s_r_confluent1 … (λL. cpm h G L n) (lfxs R).
/3 width=5 by cpm_fwd_cpx, cpx_lfxs_conf/ qed-.
(* Properties with restricted refinement for local environments *************)
(* Basic_2A1: includes: lsubr_cpr_trans *)
-lemma lsubr_cpm_trans: ∀n,h,G. lsub_trans … (cpm n h G) lsubr.
+lemma lsubr_cpm_trans: ∀n,h,G. lsub_trans … (λL. cpm h G L n) lsubr.
#n #h #G #L1 #T1 #T2 * /3 width=5 by lsubr_cpg_trans, ex2_intro/
qed-.
(* CONTEXT-SENSITIVE PARALLEL R-TRANSITION FOR BINDERS **********************)
definition cpr_ext (h) (G): relation3 lenv bind bind ≝
- cext2 (cpm 0 h G).
+ cext2 (λL. cpm h G L 0).
interpretation
"context-sensitive parallel r-transition (binder)"
include "basic_2/notation/relations/predty_5.ma".
include "basic_2/rt_transition/cpg.ma".
-(* UNCOUNTED CONTEXT-SENSITIVE PARALLEL RT-TRANSITION FOR TERMS *************)
+(* UNBOUND CONTEXT-SENSITIVE PARALLEL RT-TRANSITION FOR TERMS ***************)
definition cpx (h): relation4 genv lenv term term ≝
λG,L,T1,T2. ∃c. ⦃G, L⦄ ⊢ T1 ⬈[eq_f, c, h] T2.
interpretation
- "uncounted context-sensitive parallel rt-transition (term)"
+ "unbound context-sensitive parallel rt-transition (term)"
'PRedTy h G L T1 T2 = (cpx h G L T1 T2).
(* Basic properties *********************************************************)
include "basic_2/rt_transition/cpg_drops.ma".
include "basic_2/rt_transition/cpx.ma".
-(* UNCOUNTED CONTEXT-SENSITIVE PARALLEL RT-TRANSITION FOR TERMS *************)
+(* UNBOUND CONTEXT-SENSITIVE PARALLEL RT-TRANSITION FOR TERMS ***************)
(* Advanced properties ******************************************************)
include "basic_2/syntax/cext2.ma".
include "basic_2/rt_transition/cpx.ma".
-(* UNCOUNTED CONTEXT-SENSITIVE PARALLEL RT-TRANSITION FOR BINDERS ***********)
+(* UNBOUND CONTEXT-SENSITIVE PARALLEL RT-TRANSITION FOR BINDERS *************)
definition cpx_ext (h) (G): relation3 lenv bind bind ≝
cext2 (cpx h G).
interpretation
- "uncounted context-sensitive parallel rt-transition (binder)"
+ "unbound context-sensitive parallel rt-transition (binder)"
'PRedTy h G L I1 I2 = (cpx_ext h G L I1 I2).
include "basic_2/rt_transition/cpx_lfdeq.ma".
include "basic_2/rt_transition/lfpx_lfdeq.ma".
-(* UNCOUNTED CONTEXT-SENSITIVE PARALLEL RT-TRANSITION FOR TERMS *************)
+(* UNBOUND CONTEXT-SENSITIVE PARALLEL RT-TRANSITION FOR TERMS ***************)
(* Properties with degree-based equivalence for closures ********************)
(* *)
(**************************************************************************)
-(* UNCOUNTED CONTEXT-SENSITIVE PARALLEL RT-TRANSITION FOR TERMS *************)
+(* UNBOUND CONTEXT-SENSITIVE PARALLEL RT-TRANSITION FOR TERMS ***************)
include "basic_2/relocation/lifts_tdeq.ma".
include "basic_2/s_computation/fqus_fqup.ma".
include "basic_2/static/lfdeq_lfdeq.ma".
include "basic_2/rt_transition/lfpx_fsle.ma".
-(* UNCOUNTED CONTEXT-SENSITIVE PARALLEL RT-TRANSITION FOR TERMS *************)
+(* UNBOUND CONTEXT-SENSITIVE PARALLEL RT-TRANSITION FOR TERMS ***************)
(* Properties with degree-based equivalence for local environments **********)
include "basic_2/static/lfeq.ma".
include "basic_2/rt_transition/lfpx_fsle.ma".
-(* UNCOUNTED CONTEXT-SENSITIVE PARALLEL RT-TRANSITION FOR TERMS *************)
+(* UNBOUND CONTEXT-SENSITIVE PARALLEL RT-TRANSITION FOR TERMS ***************)
(* Properties with syntactic equivalence for lenvs on referred entries ******)
lemma cpx_lfeq_conf_dx: ∀h,G,L2,T1,T2. ⦃G, L2⦄ ⊢ T1 ⬈[h] T2 →
∀L1. L1 ≘[T1] L2 → L1 ≘[T2] L2.
/4 width=6 by cpx_lfeq_conf_sn, lfeq_sym/ qed-.
-*)
\ No newline at end of file
+*)
include "basic_2/rt_transition/cpg_lsubr.ma".
include "basic_2/rt_transition/cpx.ma".
-(* UNCOUNTED CONTEXT-SENSITIVE PARALLEL RT-TRANSITION FOR TERMS *************)
+(* UNBOUND CONTEXT-SENSITIVE PARALLEL RT-TRANSITION FOR TERMS ***************)
(* Properties with restricted refinement for local environments *************)
include "basic_2/rt_transition/cpg_simple.ma".
include "basic_2/rt_transition/cpx.ma".
-(* UNCOUNTED CONTEXT-SENSITIVE PARALLEL RT-TRANSITION FOR TERMS *************)
+(* UNBOUND CONTEXT-SENSITIVE PARALLEL RT-TRANSITION FOR TERMS ***************)
+
+(* Inversion lemmas with simple terms ***************************************)
lemma cpx_inv_appl1_simple: ∀h,G,L,V1,T1,U. ⦃G, L⦄ ⊢ ⓐV1.T1 ⬈[h] U → 𝐒⦃T1⦄ →
∃∃V2,T2. ⦃G, L⦄ ⊢ V1 ⬈[h] V2 & ⦃G, L⦄ ⊢ T1 ⬈[h] T2 &
(* PARALLEL R-TRANSITION FOR LOCAL ENV.S ON REFERRED ENTRIES ****************)
definition lfpr: sh → genv → relation3 term lenv lenv ≝
- λh,G. lfxs (cpm 0 h G).
+ λh,G. lfxs (λL. cpm h G L 0).
interpretation
"parallel r-transition on referred entries (local environment)"
(* Properties with atomic arity assignment for terms ************************)
-lemma cpr_aaa_conf: ∀h,G,L. Conf3 … (aaa G L) (cpm 0 h G L).
+lemma cpr_aaa_conf: ∀h,G,L. Conf3 … (aaa G L) (cpm h G L 0).
/3 width=5 by cpx_aaa_conf, cpm_fwd_cpx/ qed-.
(* Basic_2A1: uses: lpr_aaa_conf *)
(* Properties with generic slicing for local environments *******************)
(* Basic_2A1: uses: drop_lpr_trans *)
-lemma drops_lfpr_trans: ∀h,G. dedropable_sn (cpm 0 h G).
+lemma drops_lfpr_trans: ∀h,G. dedropable_sn (λL. cpm h G L 0).
/3 width=6 by lfxs_liftable_dedropable_sn, cpm_lifts_sn/ qed-.
(* Inversion lemmas with generic slicing for local environments *************)
(* Basic_2A1: uses: lpr_drop_conf *)
-lemma lfpr_drops_conf: ∀h,G. dropable_sn (cpm 0 h G).
+lemma lfpr_drops_conf: ∀h,G. dropable_sn (λL. cpm h G L 0).
/2 width=5 by lfxs_dropable_sn/ qed-.
(* Basic_2A1: uses: lpr_drop_trans_O1 *)
-lemma lfpr_drops_trans: ∀h,G. dropable_dx (cpm 0 h G).
+lemma lfpr_drops_trans: ∀h,G. dropable_dx (λL. cpm h G L 0).
/2 width=5 by lfxs_dropable_dx/ qed-.
lemma lfpr_inv_lref_pair_sn: ∀h,G,L1,L2,i. ⦃G, L1⦄ ⊢ ➡[h, #i] L2 → ∀I,K1,V1. ⬇*[i] L1 ≘ K1.ⓑ{I}V1 →
/4 width=7 by cpm_bind, cpr_flat, ex2_intro/ (**) (* full auto not tried *)
qed-.
-theorem cpr_conf_lfpr: ∀h,G. R_confluent2_lfxs (cpm 0 h G) (cpm 0 h G) (cpm 0 h G) (cpm 0 h G).
+theorem cpr_conf_lfpr: ∀h,G. R_confluent2_lfxs (λL. cpm h G L 0) (λL. cpm h G L 0) (λL. cpm h G L 0) (λL. cpm h G L 0).
#h #G #L0 #T0 @(fqup_wf_ind_eq (Ⓣ) … G L0 T0) -G -L0 -T0 #G #L #T #IH #G0 #L0 * [| * ]
[ #I0 #HG #HL #HT #T1 #H1 #T2 #H2 #L1 #HL01 #L2 #HL02 destruct
elim (cpr_inv_atom1_drops … H1) -H1
qed-.
(* Basic_1: includes: pr0_confluence pr2_confluence *)
-theorem cpr_conf: ∀h,G,L. confluent … (cpm 0 h G L).
+theorem cpr_conf: ∀h,G,L. confluent … (cpm h G L 0).
/2 width=6 by cpr_conf_lfpr/ qed-.
(* Properties with context-sensitive parallel r-transition for terms ********)
include "basic_2/static/lfxs.ma".
include "basic_2/rt_transition/cpx_ext.ma".
-(* UNCOUNTED PARALLEL RT-TRANSITION FOR LOCAL ENV.S ON REFERRED ENTRIES *****)
+(* UNBOUND PARALLEL RT-TRANSITION FOR LOCAL ENV.S ON REFERRED ENTRIES *******)
definition lfpx: sh → genv → relation3 term lenv lenv ≝
λh,G. lfxs (cpx h G).
interpretation
- "uncounted parallel rt-transition on referred entries (local environment)"
+ "unbound parallel rt-transition on referred entries (local environment)"
'PRedTySn h T G L1 L2 = (lfpx h G T L1 L2).
(* Basic properties ***********************************************************)
include "basic_2/static/lsuba_aaa.ma".
include "basic_2/rt_transition/lfpx_fqup.ma".
-(* UNCOUNTED PARALLEL RT-TRANSITION FOR LOCAL ENV.S ON REFERRED ENTRIES *****)
+(* UNBOUND PARALLEL RT-TRANSITION FOR LOCAL ENV.S ON REFERRED ENTRIES *******)
(* Properties with atomic arity assignment for terms ************************)
include "basic_2/rt_transition/cpx_drops.ma".
include "basic_2/rt_transition/lfpx.ma".
-(* UNCOUNTED PARALLEL RT-TRANSITION FOR LOCAL ENV.S ON REFERRED ENTRIES *****)
+(* UNBOUND PARALLEL RT-TRANSITION FOR LOCAL ENV.S ON REFERRED ENTRIES *******)
(* Properties with generic slicing for local environments *******************)
include "basic_2/static/lfxs_fqup.ma".
include "basic_2/rt_transition/lfpx.ma".
-(* UNCOUNTED PARALLEL RT-TRANSITION FOR LOCAL ENV.S ON REFERRED ENTRIES *****)
+(* UNBOUND PARALLEL RT-TRANSITION FOR LOCAL ENV.S ON REFERRED ENTRIES *******)
(* Advanced properties ******************************************************)
include "basic_2/rt_transition/lfpx_fsle.ma".
include "basic_2/s_transition/fquq.ma".
-(* UNCOUNTED PARALLEL RT-TRANSITION FOR LOCAL ENV.S ON REFERRED ENTRIES *****)
+(* UNBOUND PARALLEL RT-TRANSITION FOR LOCAL ENV.S ON REFERRED ENTRIES *******)
(* Properties with extended structural successor for closures ***************)
include "basic_2/rt_transition/lfpx_length.ma".
include "basic_2/rt_transition/lfpx_fqup.ma".
-(* UNCOUNTED CONTEXT-SENSITIVE PARALLEL RT-TRANSITION FOR TERMS *************)
+(* UNBOUND CONTEXT-SENSITIVE PARALLEL RT-TRANSITION FOR TERMS ***************)
(* Forward lemmas with free variables inclusion for restricted closures *****)
include "basic_2/static/lfxs_length.ma".
include "basic_2/rt_transition/lfpx.ma".
-(* UNCOUNTED PARALLEL RT-TRANSITION FOR LOCAL ENV.S ON REFERRED ENTRIES *****)
+(* UNBOUND PARALLEL RT-TRANSITION FOR LOCAL ENV.S ON REFERRED ENTRIES *******)
(* Forward lemmas with length for local environments ************************)
include "basic_2/static/lfdeq_lfdeq.ma".
include "basic_2/rt_transition/lfpx_fsle.ma".
-(* UNCOUNTED PARALLEL RT-TRANSITION FOR LOCAL ENV.S ON REFERRED ENTRIES *****)
+(* UNBOUND PARALLEL RT-TRANSITION FOR LOCAL ENV.S ON REFERRED ENTRIES *******)
(* Properties with degree-based equivalence for local environments **********)
include "basic_2/static/lfxs_lfxs.ma".
include "basic_2/rt_transition/lfpx.ma".
-(* UNCOUNTED PARALLEL RT-TRANSITION FOR LOCAL ENV.S ON REFERRED ENTRIES *****)
+(* UNBOUND PARALLEL RT-TRANSITION FOR LOCAL ENV.S ON REFERRED ENTRIES *******)
(* Main properties **********************************************************)
include "basic_2/rt_transition/lfpx_fsle.ma".
include "basic_2/rt_transition/lpx.ma".
-(* UNCOUNTED PARALLEL RT-TRANSITION FOR LOCAL ENV.S ON REFERRED ENTRIES *****)
+(* UNBOUND PARALLEL RT-TRANSITION FOR LOCAL ENV.S ON REFERRED ENTRIES *******)
-(* Properties with uncounted parallel rt-transition for local environments **)
+(* Properties with unbound parallel rt-transition for local environments ****)
lemma lfpx_lpx: ∀h,G,L1,L2,T. ⦃G, L1⦄ ⊢ ⬈[h] L2 → ⦃G, L1⦄ ⊢ ⬈[h, T] L2.
/2 width=1 by lfxs_lex/ qed.
-(* Inversion lemmas with uncounted parallel rt-transition for local envs ****)
+(* Inversion lemmas with unbound parallel rt-transition for local envs ******)
lemma lfpx_inv_lpx_lfeq: ∀h,G,L1,L2,T. ⦃G, L1⦄ ⊢ ⬈[h, T] L2 →
∃∃L. ⦃G, L1⦄ ⊢ ⬈[h] L & L ≡[T] L2.
include "basic_2/relocation/lex.ma".
include "basic_2/rt_transition/cpx_ext.ma".
-(* UNCOUNTED PARALLEL RT-TRANSITION FOR LOCAL ENVIRONMENTS ******************)
+(* UNBOUND PARALLEL RT-TRANSITION FOR LOCAL ENVIRONMENTS ********************)
definition lpx: sh → genv → relation lenv ≝
λh,G. lex (cpx h G).
interpretation
- "uncounted parallel rt-transition (local environment)"
+ "unbound parallel rt-transition (local environment)"
'PRedTySn h G L1 L2 = (lpx h G L1 L2).
(* Basic properties *********************************************************)
}
]
*)
- [ { "uncounted context-sensitive parallel rst-computation" * } {
+ [ { "t-bound context-sensitive parallel rt-computation" * } {
+ [ [ "for terms" ] "cpms" + "( ⦃?,?⦄ ⊢ ? ➡*[?,?] ? )" * ]
+ }
+ ]
+ [ { "unbound context-sensitive parallel rst-computation" * } {
[ [ "strongly normalizing for closures" ] "fsb" + "( ≥[?,?] 𝐒⦃?,?,?⦄ )" "fsb_ffdeq" + "fsb_aaa" + "fsb_csx" + "fsb_fpbg" * ]
[ [ "proper for closures" ] "fpbg" + "( ⦃?,?,?⦄ >[?,?] ⦃?,?,?⦄ )" "fpbg_fqup" + "fpbg_cpxs" + "fpbg_lfpxs" + "fpbg_fpbs" + "fpbg_fpbg" * ]
[ [ "for closures" ] "fpbs" + "( ⦃?,?,?⦄ ≥[?,?] ⦃?,?,?⦄ )" "fpbs_fqup" + "fpbs_fqus" + "fpbs_aaa" + "fpbs_cpx" + "fpbs_fpb" + "fpbs_cpxs" + "fpbs_lpxs" + "fpbs_lfpxs" + "fpbs_csx" + "fpbs_fpbs" * ]
}
]
- [ { "uncounted context-sensitive parallel rt-computation" * } {
+ [ { "unbound context-sensitive parallel rt-computation" * } {
[ [ "refinement for lenvs on selected entries" ] "lsubsx" + "( ? ⊢ ? ⊆ⓧ[?,?,?] ? )" "lsubsx_lfsx" + "lsubsx_lsubsx" * ]
[ [ "strongly normalizing for lenvs on referred entries" ] "lfsx" + "( ? ⊢ ⬈*[?,?,?] 𝐒⦃?⦄ )" "lfsx_drops" + "lfsx_fqup" + "lfsx_cpx" + "lfsx_cpxs" + "lfsx_lfpxs" + "lfsx_lfsx" * ]
[ [ "strongly normalizing for term vectors" ] "csx_vector" + "( ⦃?,?⦄ ⊢ ⬈*[?,?] 𝐒⦃?⦄ )" "csx_cnx_vector" + "csx_csx_vector" * ]
]
class "cyan"
[ { "rt-transition" * } {
- [ { "uncounted parallel rst-transition" * } {
+ [ { "unbound parallel rst-transition" * } {
[ [ "for closures" ] "fpbq" + "( ⦃?,?,?⦄ ≽[?,?] ⦃?,?,?⦄ )" "fpbq_aaa" + "fpbq_fpb" * ]
[ [ "proper for closures" ] "fpb" + "( ⦃?,?,?⦄ ≻[?,?] ⦃?,?,?⦄ )" "fpb_lfdeq" + "fpb_ffdeq" * ]
}
[ [ "for terms" ] "cpm" + "( ⦃?,?⦄ ⊢ ? ➡[?,?] ? )" "cpm_simple" + "cpm_drops" + "cpm_lsubr" + "cpm_fsle" + "cpm_cpx" * ]
}
]
- [ { "uncounted context-sensitive parallel rt-transition" * } {
+ [ { "unbound context-sensitive parallel rt-transition" * } {
[ [ "normal form for terms" ] "cnx" + "( ⦃?,?⦄ ⊢ ⬈[?,?] 𝐍⦃?⦄ )" "cnx_simple" + "cnx_drops" + "cnx_cnx" * ]
[ [ "for lenvs on referred entries" ] "lfpx" + "( ⦃?,?⦄ ⊢ ⬈[?,?] ? )" "lfpx_length" + "lfpx_drops" + "lfpx_fquq" + "lfpx_fqup" + "lfpx_fsle" + "lfpx_lfdeq" + "lfpx_aaa" + "lfpx_lpx" + "lfpx_lfpx" * ]
[ [ "for lenvs on all entries" ] "lpx" + "( ⦃?,?⦄ ⊢ ⬈[?] ? )" * ]
[ [ "for terms" ] "cpx" + "( ⦃?,?⦄ ⊢ ? ⬈[?] ? )" "cpx_simple" + "cpx_drops" + "cpx_fqus" + "cpx_lsubr" + "cpx_lfeq" + "cpx_lfdeq" + "cpx_ffdeq" * ]
}
]
- [ { "counted context-sensitive parallel rt-transition" * } {
+ [ { "bound context-sensitive parallel rt-transition" * } {
[ [ "for terms" ] "cpg" + "( ⦃?,?⦄ ⊢ ? ⬈[?,?] ? )" "cpg_simple" + "cpg_drops" + "cpg_lsubr" * ]
}
]
projects / helm.git / commitdiff