From f129bbbfda0e65a5f92ec086246f6e288376d4f9 Mon Sep 17 00:00:00 2001 From: Ferruccio Guidi Date: Fri, 27 Apr 2018 12:16:13 +0200 Subject: [PATCH] update in basic_2 + first results on cpms + minor improvements --- .../basic_2/notation/relations/predstar_4.ma | 19 ----- .../{dpredstar_7.ma => predstar_5.ma} | 4 +- .../basic_2/notation/relations/predstar_6.ma | 4 +- .../basic_2/rt_computation/cpms.ma | 70 +++++++++++++++++++ .../basic_2/rt_computation/cpxs.ma | 4 +- .../basic_2/rt_computation/cpxs_aaa.ma | 2 +- .../basic_2/rt_computation/cpxs_cnx.ma | 2 +- .../basic_2/rt_computation/cpxs_cpxs.ma | 2 +- .../basic_2/rt_computation/cpxs_drops.ma | 2 +- .../basic_2/rt_computation/cpxs_ext.ma | 4 +- .../basic_2/rt_computation/cpxs_ffdeq.ma | 2 +- .../basic_2/rt_computation/cpxs_fqus.ma | 2 +- .../basic_2/rt_computation/cpxs_lfdeq.ma | 2 +- .../basic_2/rt_computation/cpxs_lfpx.ma | 4 +- .../basic_2/rt_computation/cpxs_lpx.ma | 4 +- .../basic_2/rt_computation/cpxs_lsubr.ma | 2 +- .../basic_2/rt_computation/cpxs_tdeq.ma | 2 +- .../basic_2/rt_computation/cpxs_theq.ma | 2 +- .../rt_computation/cpxs_theq_vector.ma | 2 +- .../lambdadelta/basic_2/rt_computation/csx.ma | 4 +- .../basic_2/rt_computation/csx_aaa.ma | 2 +- .../basic_2/rt_computation/csx_cnx.ma | 4 +- .../basic_2/rt_computation/csx_cnx_vector.ma | 4 +- .../basic_2/rt_computation/csx_cpxs.ma | 6 +- .../basic_2/rt_computation/csx_csx.ma | 2 +- .../basic_2/rt_computation/csx_csx_vector.ma | 2 +- .../basic_2/rt_computation/csx_drops.ma | 2 +- .../basic_2/rt_computation/csx_ffdeq.ma | 2 +- .../basic_2/rt_computation/csx_fpbq.ma | 2 +- .../basic_2/rt_computation/csx_fqus.ma | 2 +- .../basic_2/rt_computation/csx_gcp.ma | 2 +- .../basic_2/rt_computation/csx_gcr.ma | 2 +- .../basic_2/rt_computation/csx_lfdeq.ma | 2 +- .../basic_2/rt_computation/csx_lfpx.ma | 4 +- .../basic_2/rt_computation/csx_lfpxs.ma | 4 +- .../basic_2/rt_computation/csx_lsubr.ma | 2 +- .../basic_2/rt_computation/csx_simple.ma | 2 +- .../basic_2/rt_computation/csx_simple_theq.ma | 2 +- .../basic_2/rt_computation/csx_vector.ma | 4 +- .../basic_2/rt_computation/fpbg_cpxs.ma | 4 +- .../basic_2/rt_computation/fpbg_lfpxs.ma | 2 +- .../basic_2/rt_computation/fpbs_cpx.ma | 2 +- .../basic_2/rt_computation/fpbs_cpxs.ma | 2 +- .../basic_2/rt_computation/fpbs_csx.ma | 2 +- .../basic_2/rt_computation/fpbs_lfpxs.ma | 4 +- .../basic_2/rt_computation/fpbs_lpxs.ma | 4 +- .../basic_2/rt_computation/lfpxs.ma | 4 +- .../basic_2/rt_computation/lfpxs_aaa.ma | 4 +- .../basic_2/rt_computation/lfpxs_cpxs.ma | 8 +-- .../basic_2/rt_computation/lfpxs_drops.ma | 2 +- .../basic_2/rt_computation/lfpxs_ffdeq.ma | 2 +- .../basic_2/rt_computation/lfpxs_fqup.ma | 2 +- .../basic_2/rt_computation/lfpxs_length.ma | 2 +- .../basic_2/rt_computation/lfpxs_lfdeq.ma | 2 +- .../basic_2/rt_computation/lfpxs_lfpxs.ma | 2 +- .../basic_2/rt_computation/lfpxs_lpxs.ma | 6 +- .../basic_2/rt_computation/lfsx.ma | 4 +- .../basic_2/rt_computation/lfsx_csx.ma | 2 +- .../basic_2/rt_computation/lfsx_drops.ma | 2 +- .../basic_2/rt_computation/lfsx_fqup.ma | 2 +- .../basic_2/rt_computation/lfsx_lfpxs.ma | 6 +- .../basic_2/rt_computation/lfsx_lfsx.ma | 2 +- .../basic_2/rt_computation/lfsx_lpx.ma | 6 +- .../basic_2/rt_computation/lfsx_lpxs.ma | 6 +- .../basic_2/rt_computation/lpxs.ma | 4 +- .../basic_2/rt_computation/lpxs_cpxs.ma | 4 +- .../basic_2/rt_computation/lpxs_length.ma | 2 +- .../basic_2/rt_computation/lpxs_lpx.ma | 4 +- .../basic_2/rt_computation/lsubsx.ma | 2 +- .../basic_2/rt_computation/lsubsx_lfsx.ma | 6 +- .../basic_2/rt_computation/lsubsx_lsubsx.ma | 2 +- .../basic_2/rt_computation/partial.txt | 1 + .../basic_2/rt_computation/scpds.ma | 48 ------------- .../lambdadelta/basic_2/rt_transition/cnx.ma | 4 +- .../basic_2/rt_transition/cnx_cnx.ma | 2 +- .../basic_2/rt_transition/cnx_drops.ma | 2 +- .../basic_2/rt_transition/cnx_simple.ma | 2 +- .../lambdadelta/basic_2/rt_transition/cpg.ma | 4 +- .../basic_2/rt_transition/cpg_drops.ma | 2 +- .../basic_2/rt_transition/cpg_lsubr.ma | 2 +- .../basic_2/rt_transition/cpg_simple.ma | 2 +- .../lambdadelta/basic_2/rt_transition/cpm.ma | 15 ++-- .../basic_2/rt_transition/cpm_cpx.ma | 2 +- .../basic_2/rt_transition/cpm_drops.ma | 8 +-- .../basic_2/rt_transition/cpm_fsle.ma | 6 +- .../basic_2/rt_transition/cpm_lsubr.ma | 2 +- .../basic_2/rt_transition/cpr_ext.ma | 2 +- .../lambdadelta/basic_2/rt_transition/cpx.ma | 4 +- .../basic_2/rt_transition/cpx_drops.ma | 2 +- .../basic_2/rt_transition/cpx_ext.ma | 4 +- .../basic_2/rt_transition/cpx_ffdeq.ma | 2 +- .../basic_2/rt_transition/cpx_fqus.ma | 2 +- .../basic_2/rt_transition/cpx_lfdeq.ma | 2 +- .../basic_2/rt_transition/cpx_lfeq.ma | 4 +- .../basic_2/rt_transition/cpx_lsubr.ma | 2 +- .../basic_2/rt_transition/cpx_simple.ma | 4 +- .../lambdadelta/basic_2/rt_transition/lfpr.ma | 2 +- .../basic_2/rt_transition/lfpr_aaa.ma | 2 +- .../basic_2/rt_transition/lfpr_drops.ma | 6 +- .../basic_2/rt_transition/lfpr_lfpr.ma | 4 +- .../lambdadelta/basic_2/rt_transition/lfpx.ma | 4 +- .../basic_2/rt_transition/lfpx_aaa.ma | 2 +- .../basic_2/rt_transition/lfpx_drops.ma | 2 +- .../basic_2/rt_transition/lfpx_fqup.ma | 2 +- .../basic_2/rt_transition/lfpx_fquq.ma | 2 +- .../basic_2/rt_transition/lfpx_fsle.ma | 2 +- .../basic_2/rt_transition/lfpx_length.ma | 2 +- .../basic_2/rt_transition/lfpx_lfdeq.ma | 2 +- .../basic_2/rt_transition/lfpx_lfpx.ma | 2 +- .../basic_2/rt_transition/lfpx_lpx.ma | 6 +- .../lambdadelta/basic_2/rt_transition/lpx.ma | 4 +- .../lambdadelta/basic_2/web/basic_2_src.tbl | 14 ++-- 112 files changed, 249 insertions(+), 238 deletions(-) delete mode 100644 matita/matita/contribs/lambdadelta/basic_2/notation/relations/predstar_4.ma rename matita/matita/contribs/lambdadelta/basic_2/notation/relations/{dpredstar_7.ma => predstar_5.ma} (89%) create mode 100644 matita/matita/contribs/lambdadelta/basic_2/rt_computation/cpms.ma delete mode 100644 matita/matita/contribs/lambdadelta/basic_2/rt_computation/scpds.ma diff --git a/matita/matita/contribs/lambdadelta/basic_2/notation/relations/predstar_4.ma b/matita/matita/contribs/lambdadelta/basic_2/notation/relations/predstar_4.ma deleted file mode 100644 index 7f374e050..000000000 --- a/matita/matita/contribs/lambdadelta/basic_2/notation/relations/predstar_4.ma +++ /dev/null @@ -1,19 +0,0 @@ -(**************************************************************************) -(* ___ *) -(* ||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 }. diff --git a/matita/matita/contribs/lambdadelta/basic_2/notation/relations/dpredstar_7.ma b/matita/matita/contribs/lambdadelta/basic_2/notation/relations/predstar_5.ma similarity index 89% rename from matita/matita/contribs/lambdadelta/basic_2/notation/relations/dpredstar_7.ma rename to matita/matita/contribs/lambdadelta/basic_2/notation/relations/predstar_5.ma index 2dc0e2f8d..30a38be9e 100644 --- a/matita/matita/contribs/lambdadelta/basic_2/notation/relations/dpredstar_7.ma +++ b/matita/matita/contribs/lambdadelta/basic_2/notation/relations/predstar_5.ma @@ -14,6 +14,6 @@ (* 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 )" +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 @{ 'DPRedStar $h $o $n $G $L $T1 $T2 }. + for @{ 'PRedStar $h $G $L $T1 $T2 }. diff --git a/matita/matita/contribs/lambdadelta/basic_2/notation/relations/predstar_6.ma b/matita/matita/contribs/lambdadelta/basic_2/notation/relations/predstar_6.ma index 20c5b48c3..baa4e8721 100644 --- a/matita/matita/contribs/lambdadelta/basic_2/notation/relations/predstar_6.ma +++ b/matita/matita/contribs/lambdadelta/basic_2/notation/relations/predstar_6.ma @@ -14,6 +14,6 @@ (* 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 }. diff --git a/matita/matita/contribs/lambdadelta/basic_2/rt_computation/cpms.ma b/matita/matita/contribs/lambdadelta/basic_2/rt_computation/cpms.ma new file mode 100644 index 000000000..cbfd28726 --- /dev/null +++ b/matita/matita/contribs/lambdadelta/basic_2/rt_computation/cpms.ma @@ -0,0 +1,70 @@ +(**************************************************************************) +(* ___ *) +(* ||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 +*) diff --git a/matita/matita/contribs/lambdadelta/basic_2/rt_computation/cpxs.ma b/matita/matita/contribs/lambdadelta/basic_2/rt_computation/cpxs.ma index e79ed15f5..88924f4e0 100644 --- a/matita/matita/contribs/lambdadelta/basic_2/rt_computation/cpxs.ma +++ b/matita/matita/contribs/lambdadelta/basic_2/rt_computation/cpxs.ma @@ -16,12 +16,12 @@ include "ground_2/lib/star.ma". 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 ********************************************************) diff --git a/matita/matita/contribs/lambdadelta/basic_2/rt_computation/cpxs_aaa.ma b/matita/matita/contribs/lambdadelta/basic_2/rt_computation/cpxs_aaa.ma index 24aa4a6aa..9f27d5fe4 100644 --- a/matita/matita/contribs/lambdadelta/basic_2/rt_computation/cpxs_aaa.ma +++ b/matita/matita/contribs/lambdadelta/basic_2/rt_computation/cpxs_aaa.ma @@ -15,7 +15,7 @@ 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 *************************) diff --git a/matita/matita/contribs/lambdadelta/basic_2/rt_computation/cpxs_cnx.ma b/matita/matita/contribs/lambdadelta/basic_2/rt_computation/cpxs_cnx.ma index 001efe155..49f74a202 100644 --- a/matita/matita/contribs/lambdadelta/basic_2/rt_computation/cpxs_cnx.ma +++ b/matita/matita/contribs/lambdadelta/basic_2/rt_computation/cpxs_cnx.ma @@ -15,7 +15,7 @@ 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 ***************************************) diff --git a/matita/matita/contribs/lambdadelta/basic_2/rt_computation/cpxs_cpxs.ma b/matita/matita/contribs/lambdadelta/basic_2/rt_computation/cpxs_cpxs.ma index 880a3d9b8..4740fc092 100644 --- a/matita/matita/contribs/lambdadelta/basic_2/rt_computation/cpxs_cpxs.ma +++ b/matita/matita/contribs/lambdadelta/basic_2/rt_computation/cpxs_cpxs.ma @@ -15,7 +15,7 @@ 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 **********************************************************) diff --git a/matita/matita/contribs/lambdadelta/basic_2/rt_computation/cpxs_drops.ma b/matita/matita/contribs/lambdadelta/basic_2/rt_computation/cpxs_drops.ma index 04a376981..aac7f8c36 100644 --- a/matita/matita/contribs/lambdadelta/basic_2/rt_computation/cpxs_drops.ma +++ b/matita/matita/contribs/lambdadelta/basic_2/rt_computation/cpxs_drops.ma @@ -16,7 +16,7 @@ include "basic_2/relocation/drops_ctc.ma". 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 ******************************************************) diff --git a/matita/matita/contribs/lambdadelta/basic_2/rt_computation/cpxs_ext.ma b/matita/matita/contribs/lambdadelta/basic_2/rt_computation/cpxs_ext.ma index 7da6fa4f2..c600cc7d0 100644 --- a/matita/matita/contribs/lambdadelta/basic_2/rt_computation/cpxs_ext.ma +++ b/matita/matita/contribs/lambdadelta/basic_2/rt_computation/cpxs_ext.ma @@ -15,11 +15,11 @@ 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). diff --git a/matita/matita/contribs/lambdadelta/basic_2/rt_computation/cpxs_ffdeq.ma b/matita/matita/contribs/lambdadelta/basic_2/rt_computation/cpxs_ffdeq.ma index f4777a7fb..c0b475a3e 100644 --- a/matita/matita/contribs/lambdadelta/basic_2/rt_computation/cpxs_ffdeq.ma +++ b/matita/matita/contribs/lambdadelta/basic_2/rt_computation/cpxs_ffdeq.ma @@ -15,7 +15,7 @@ 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 ********************) diff --git a/matita/matita/contribs/lambdadelta/basic_2/rt_computation/cpxs_fqus.ma b/matita/matita/contribs/lambdadelta/basic_2/rt_computation/cpxs_fqus.ma index 8dc5a03a3..3460879b1 100644 --- a/matita/matita/contribs/lambdadelta/basic_2/rt_computation/cpxs_fqus.ma +++ b/matita/matita/contribs/lambdadelta/basic_2/rt_computation/cpxs_fqus.ma @@ -12,7 +12,7 @@ (* *) (**************************************************************************) -(* 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". diff --git a/matita/matita/contribs/lambdadelta/basic_2/rt_computation/cpxs_lfdeq.ma b/matita/matita/contribs/lambdadelta/basic_2/rt_computation/cpxs_lfdeq.ma index 12142f2c9..d8cfade21 100644 --- a/matita/matita/contribs/lambdadelta/basic_2/rt_computation/cpxs_lfdeq.ma +++ b/matita/matita/contribs/lambdadelta/basic_2/rt_computation/cpxs_lfdeq.ma @@ -15,7 +15,7 @@ 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 **********) diff --git a/matita/matita/contribs/lambdadelta/basic_2/rt_computation/cpxs_lfpx.ma b/matita/matita/contribs/lambdadelta/basic_2/rt_computation/cpxs_lfpx.ma index 0ae68d2c2..ed187cce6 100644 --- a/matita/matita/contribs/lambdadelta/basic_2/rt_computation/cpxs_lfpx.ma +++ b/matita/matita/contribs/lambdadelta/basic_2/rt_computation/cpxs_lfpx.ma @@ -17,9 +17,9 @@ include "basic_2/rt_transition/lfpx_fquq.ma". 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-. diff --git a/matita/matita/contribs/lambdadelta/basic_2/rt_computation/cpxs_lpx.ma b/matita/matita/contribs/lambdadelta/basic_2/rt_computation/cpxs_lpx.ma index ff4aa6c09..5e17096f6 100644 --- a/matita/matita/contribs/lambdadelta/basic_2/rt_computation/cpxs_lpx.ma +++ b/matita/matita/contribs/lambdadelta/basic_2/rt_computation/cpxs_lpx.ma @@ -16,9 +16,9 @@ include "basic_2/rt_transition/lpx.ma". 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 diff --git a/matita/matita/contribs/lambdadelta/basic_2/rt_computation/cpxs_lsubr.ma b/matita/matita/contribs/lambdadelta/basic_2/rt_computation/cpxs_lsubr.ma index c4844c2e1..a4b533b19 100644 --- a/matita/matita/contribs/lambdadelta/basic_2/rt_computation/cpxs_lsubr.ma +++ b/matita/matita/contribs/lambdadelta/basic_2/rt_computation/cpxs_lsubr.ma @@ -15,7 +15,7 @@ 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 *************) diff --git a/matita/matita/contribs/lambdadelta/basic_2/rt_computation/cpxs_tdeq.ma b/matita/matita/contribs/lambdadelta/basic_2/rt_computation/cpxs_tdeq.ma index 3d1fa9e71..f86f4396f 100644 --- a/matita/matita/contribs/lambdadelta/basic_2/rt_computation/cpxs_tdeq.ma +++ b/matita/matita/contribs/lambdadelta/basic_2/rt_computation/cpxs_tdeq.ma @@ -15,7 +15,7 @@ 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 ***********************) diff --git a/matita/matita/contribs/lambdadelta/basic_2/rt_computation/cpxs_theq.ma b/matita/matita/contribs/lambdadelta/basic_2/rt_computation/cpxs_theq.ma index 22f20ecb0..4235b4e30 100644 --- a/matita/matita/contribs/lambdadelta/basic_2/rt_computation/cpxs_theq.ma +++ b/matita/matita/contribs/lambdadelta/basic_2/rt_computation/cpxs_theq.ma @@ -17,7 +17,7 @@ include "basic_2/rt_computation/cpxs_lsubr.ma". 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 ***************************) diff --git a/matita/matita/contribs/lambdadelta/basic_2/rt_computation/cpxs_theq_vector.ma b/matita/matita/contribs/lambdadelta/basic_2/rt_computation/cpxs_theq_vector.ma index 529c90c25..9fb405b0c 100644 --- a/matita/matita/contribs/lambdadelta/basic_2/rt_computation/cpxs_theq_vector.ma +++ b/matita/matita/contribs/lambdadelta/basic_2/rt_computation/cpxs_theq_vector.ma @@ -16,7 +16,7 @@ include "basic_2/syntax/theq_simple_vector.ma". 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 ************) diff --git a/matita/matita/contribs/lambdadelta/basic_2/rt_computation/csx.ma b/matita/matita/contribs/lambdadelta/basic_2/rt_computation/csx.ma index 49f221911..5e255d297 100644 --- a/matita/matita/contribs/lambdadelta/basic_2/rt_computation/csx.ma +++ b/matita/matita/contribs/lambdadelta/basic_2/rt_computation/csx.ma @@ -16,13 +16,13 @@ include "basic_2/notation/relations/predtystrong_5.ma". 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 ********************************************************) diff --git a/matita/matita/contribs/lambdadelta/basic_2/rt_computation/csx_aaa.ma b/matita/matita/contribs/lambdadelta/basic_2/rt_computation/csx_aaa.ma index 7cf220ebd..722e8d8b6 100644 --- a/matita/matita/contribs/lambdadelta/basic_2/rt_computation/csx_aaa.ma +++ b/matita/matita/contribs/lambdadelta/basic_2/rt_computation/csx_aaa.ma @@ -17,7 +17,7 @@ include "basic_2/rt_computation/cpxs_aaa.ma". 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 *****************************) diff --git a/matita/matita/contribs/lambdadelta/basic_2/rt_computation/csx_cnx.ma b/matita/matita/contribs/lambdadelta/basic_2/rt_computation/csx_cnx.ma index ea34597b9..24320b69f 100644 --- a/matita/matita/contribs/lambdadelta/basic_2/rt_computation/csx_cnx.ma +++ b/matita/matita/contribs/lambdadelta/basic_2/rt_computation/csx_cnx.ma @@ -12,12 +12,12 @@ (* *) (**************************************************************************) -(* 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⦄. diff --git a/matita/matita/contribs/lambdadelta/basic_2/rt_computation/csx_cnx_vector.ma b/matita/matita/contribs/lambdadelta/basic_2/rt_computation/csx_cnx_vector.ma index ef3d1c20b..9e0de4217 100644 --- a/matita/matita/contribs/lambdadelta/basic_2/rt_computation/csx_cnx_vector.ma +++ b/matita/matita/contribs/lambdadelta/basic_2/rt_computation/csx_cnx_vector.ma @@ -12,7 +12,7 @@ (* *) (**************************************************************************) -(* 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". @@ -20,7 +20,7 @@ include "basic_2/rt_computation/csx_cnx.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⦄ → diff --git a/matita/matita/contribs/lambdadelta/basic_2/rt_computation/csx_cpxs.ma b/matita/matita/contribs/lambdadelta/basic_2/rt_computation/csx_cpxs.ma index a709858ad..cfc4d6314 100644 --- a/matita/matita/contribs/lambdadelta/basic_2/rt_computation/csx_cpxs.ma +++ b/matita/matita/contribs/lambdadelta/basic_2/rt_computation/csx_cpxs.ma @@ -16,9 +16,9 @@ include "basic_2/rt_computation/cpxs_tdeq.ma". 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. @@ -33,7 +33,7 @@ lemma csx_cpxs_trans: ∀h,o,G,L,T1. ⦃G, L⦄ ⊢ ⬈*[h, o] 𝐒⦃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⦄ → diff --git a/matita/matita/contribs/lambdadelta/basic_2/rt_computation/csx_csx.ma b/matita/matita/contribs/lambdadelta/basic_2/rt_computation/csx_csx.ma index 34ccf92d0..e8d85a309 100644 --- a/matita/matita/contribs/lambdadelta/basic_2/rt_computation/csx_csx.ma +++ b/matita/matita/contribs/lambdadelta/basic_2/rt_computation/csx_csx.ma @@ -15,7 +15,7 @@ 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 ******************************************************) diff --git a/matita/matita/contribs/lambdadelta/basic_2/rt_computation/csx_csx_vector.ma b/matita/matita/contribs/lambdadelta/basic_2/rt_computation/csx_csx_vector.ma index e1166a0fd..767ac4db6 100644 --- a/matita/matita/contribs/lambdadelta/basic_2/rt_computation/csx_csx_vector.ma +++ b/matita/matita/contribs/lambdadelta/basic_2/rt_computation/csx_csx_vector.ma @@ -18,7 +18,7 @@ include "basic_2/rt_computation/csx_lsubr.ma". 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 ************************************* ****************) diff --git a/matita/matita/contribs/lambdadelta/basic_2/rt_computation/csx_drops.ma b/matita/matita/contribs/lambdadelta/basic_2/rt_computation/csx_drops.ma index 2a1981169..84c7ec146 100644 --- a/matita/matita/contribs/lambdadelta/basic_2/rt_computation/csx_drops.ma +++ b/matita/matita/contribs/lambdadelta/basic_2/rt_computation/csx_drops.ma @@ -16,7 +16,7 @@ include "basic_2/relocation/lifts_tdeq.ma". 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 ***************************************) diff --git a/matita/matita/contribs/lambdadelta/basic_2/rt_computation/csx_ffdeq.ma b/matita/matita/contribs/lambdadelta/basic_2/rt_computation/csx_ffdeq.ma index 5645c46b8..69a6aa002 100644 --- a/matita/matita/contribs/lambdadelta/basic_2/rt_computation/csx_ffdeq.ma +++ b/matita/matita/contribs/lambdadelta/basic_2/rt_computation/csx_ffdeq.ma @@ -15,7 +15,7 @@ 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 ********************) diff --git a/matita/matita/contribs/lambdadelta/basic_2/rt_computation/csx_fpbq.ma b/matita/matita/contribs/lambdadelta/basic_2/rt_computation/csx_fpbq.ma index 3df556855..b238a54d0 100644 --- a/matita/matita/contribs/lambdadelta/basic_2/rt_computation/csx_fpbq.ma +++ b/matita/matita/contribs/lambdadelta/basic_2/rt_computation/csx_fpbq.ma @@ -17,7 +17,7 @@ include "basic_2/rt_computation/csx_fqus.ma". 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 *********************) diff --git a/matita/matita/contribs/lambdadelta/basic_2/rt_computation/csx_fqus.ma b/matita/matita/contribs/lambdadelta/basic_2/rt_computation/csx_fqus.ma index 9515e64b9..69cf8e20a 100644 --- a/matita/matita/contribs/lambdadelta/basic_2/rt_computation/csx_fqus.ma +++ b/matita/matita/contribs/lambdadelta/basic_2/rt_computation/csx_fqus.ma @@ -15,7 +15,7 @@ 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 **************************************) diff --git a/matita/matita/contribs/lambdadelta/basic_2/rt_computation/csx_gcp.ma b/matita/matita/contribs/lambdadelta/basic_2/rt_computation/csx_gcp.ma index 5a0426628..8ff4067e0 100644 --- a/matita/matita/contribs/lambdadelta/basic_2/rt_computation/csx_gcp.ma +++ b/matita/matita/contribs/lambdadelta/basic_2/rt_computation/csx_gcp.ma @@ -16,7 +16,7 @@ include "basic_2/static/gcp.ma". 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 **********************) diff --git a/matita/matita/contribs/lambdadelta/basic_2/rt_computation/csx_gcr.ma b/matita/matita/contribs/lambdadelta/basic_2/rt_computation/csx_gcr.ma index f1f1393f0..668b023d5 100644 --- a/matita/matita/contribs/lambdadelta/basic_2/rt_computation/csx_gcr.ma +++ b/matita/matita/contribs/lambdadelta/basic_2/rt_computation/csx_gcr.ma @@ -16,7 +16,7 @@ include "basic_2/static/gcp_cr.ma". 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 ******************) diff --git a/matita/matita/contribs/lambdadelta/basic_2/rt_computation/csx_lfdeq.ma b/matita/matita/contribs/lambdadelta/basic_2/rt_computation/csx_lfdeq.ma index 2f4655814..69f78e094 100644 --- a/matita/matita/contribs/lambdadelta/basic_2/rt_computation/csx_lfdeq.ma +++ b/matita/matita/contribs/lambdadelta/basic_2/rt_computation/csx_lfdeq.ma @@ -15,7 +15,7 @@ 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 **********) diff --git a/matita/matita/contribs/lambdadelta/basic_2/rt_computation/csx_lfpx.ma b/matita/matita/contribs/lambdadelta/basic_2/rt_computation/csx_lfpx.ma index 44fc48fae..353f9b84f 100644 --- a/matita/matita/contribs/lambdadelta/basic_2/rt_computation/csx_lfpx.ma +++ b/matita/matita/contribs/lambdadelta/basic_2/rt_computation/csx_lfpx.ma @@ -15,9 +15,9 @@ 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⦄ → diff --git a/matita/matita/contribs/lambdadelta/basic_2/rt_computation/csx_lfpxs.ma b/matita/matita/contribs/lambdadelta/basic_2/rt_computation/csx_lfpxs.ma index bc21143cd..9f286eef3 100644 --- a/matita/matita/contribs/lambdadelta/basic_2/rt_computation/csx_lfpxs.ma +++ b/matita/matita/contribs/lambdadelta/basic_2/rt_computation/csx_lfpxs.ma @@ -15,9 +15,9 @@ 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 → diff --git a/matita/matita/contribs/lambdadelta/basic_2/rt_computation/csx_lsubr.ma b/matita/matita/contribs/lambdadelta/basic_2/rt_computation/csx_lsubr.ma index 694ce6b3c..169970ed1 100644 --- a/matita/matita/contribs/lambdadelta/basic_2/rt_computation/csx_lsubr.ma +++ b/matita/matita/contribs/lambdadelta/basic_2/rt_computation/csx_lsubr.ma @@ -15,7 +15,7 @@ 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 ******************************************************) diff --git a/matita/matita/contribs/lambdadelta/basic_2/rt_computation/csx_simple.ma b/matita/matita/contribs/lambdadelta/basic_2/rt_computation/csx_simple.ma index 7d1137af7..efa69cff7 100644 --- a/matita/matita/contribs/lambdadelta/basic_2/rt_computation/csx_simple.ma +++ b/matita/matita/contribs/lambdadelta/basic_2/rt_computation/csx_simple.ma @@ -15,7 +15,7 @@ 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 *********************************************) diff --git a/matita/matita/contribs/lambdadelta/basic_2/rt_computation/csx_simple_theq.ma b/matita/matita/contribs/lambdadelta/basic_2/rt_computation/csx_simple_theq.ma index 83c8fd43e..54ef85a48 100644 --- a/matita/matita/contribs/lambdadelta/basic_2/rt_computation/csx_simple_theq.ma +++ b/matita/matita/contribs/lambdadelta/basic_2/rt_computation/csx_simple_theq.ma @@ -18,7 +18,7 @@ include "basic_2/rt_transition/cpx_simple.ma". 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 *******************************) diff --git a/matita/matita/contribs/lambdadelta/basic_2/rt_computation/csx_vector.ma b/matita/matita/contribs/lambdadelta/basic_2/rt_computation/csx_vector.ma index 03651de12..6fdda2bbf 100644 --- a/matita/matita/contribs/lambdadelta/basic_2/rt_computation/csx_vector.ma +++ b/matita/matita/contribs/lambdadelta/basic_2/rt_computation/csx_vector.ma @@ -15,13 +15,13 @@ 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 ***************************************************) diff --git a/matita/matita/contribs/lambdadelta/basic_2/rt_computation/fpbg_cpxs.ma b/matita/matita/contribs/lambdadelta/basic_2/rt_computation/fpbg_cpxs.ma index ee1e1ecad..960979cac 100644 --- a/matita/matita/contribs/lambdadelta/basic_2/rt_computation/fpbg_cpxs.ma +++ b/matita/matita/contribs/lambdadelta/basic_2/rt_computation/fpbg_cpxs.ma @@ -16,9 +16,9 @@ include "basic_2/rt_computation/cpxs_tdeq.ma". 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 → diff --git a/matita/matita/contribs/lambdadelta/basic_2/rt_computation/fpbg_lfpxs.ma b/matita/matita/contribs/lambdadelta/basic_2/rt_computation/fpbg_lfpxs.ma index d4c447c81..1cfc428ff 100644 --- a/matita/matita/contribs/lambdadelta/basic_2/rt_computation/fpbg_lfpxs.ma +++ b/matita/matita/contribs/lambdadelta/basic_2/rt_computation/fpbg_lfpxs.ma @@ -17,7 +17,7 @@ include "basic_2/rt_computation/fpbg.ma". (* 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 → diff --git a/matita/matita/contribs/lambdadelta/basic_2/rt_computation/fpbs_cpx.ma b/matita/matita/contribs/lambdadelta/basic_2/rt_computation/fpbs_cpx.ma index 9677e98ee..3acf1a168 100644 --- a/matita/matita/contribs/lambdadelta/basic_2/rt_computation/fpbs_cpx.ma +++ b/matita/matita/contribs/lambdadelta/basic_2/rt_computation/fpbs_cpx.ma @@ -18,7 +18,7 @@ include "basic_2/rt_computation/fpbs_lpxs.ma". (* 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⦄ → diff --git a/matita/matita/contribs/lambdadelta/basic_2/rt_computation/fpbs_cpxs.ma b/matita/matita/contribs/lambdadelta/basic_2/rt_computation/fpbs_cpxs.ma index 9269fd393..3551e1f7e 100644 --- a/matita/matita/contribs/lambdadelta/basic_2/rt_computation/fpbs_cpxs.ma +++ b/matita/matita/contribs/lambdadelta/basic_2/rt_computation/fpbs_cpxs.ma @@ -17,7 +17,7 @@ include "basic_2/rt_computation/fpbs_fqup.ma". (* 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 diff --git a/matita/matita/contribs/lambdadelta/basic_2/rt_computation/fpbs_csx.ma b/matita/matita/contribs/lambdadelta/basic_2/rt_computation/fpbs_csx.ma index a15e715f1..ce44e7e7b 100644 --- a/matita/matita/contribs/lambdadelta/basic_2/rt_computation/fpbs_csx.ma +++ b/matita/matita/contribs/lambdadelta/basic_2/rt_computation/fpbs_csx.ma @@ -17,7 +17,7 @@ include "basic_2/rt_computation/fpbs.ma". (* 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⦄ → diff --git a/matita/matita/contribs/lambdadelta/basic_2/rt_computation/fpbs_lfpxs.ma b/matita/matita/contribs/lambdadelta/basic_2/rt_computation/fpbs_lfpxs.ma index 9bccf418d..87818e45b 100644 --- a/matita/matita/contribs/lambdadelta/basic_2/rt_computation/fpbs_lfpxs.ma +++ b/matita/matita/contribs/lambdadelta/basic_2/rt_computation/fpbs_lfpxs.ma @@ -22,7 +22,7 @@ include "basic_2/rt_computation/fpbs_cpxs.ma". (* 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⦄. @@ -60,7 +60,7 @@ lemma fqus_lfpxs_fpbs: ∀h,o,G1,G2,L1,L,T1,T2. ⦃G1, L1, T1⦄ ⊐* ⦃G2, L, ∀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 → diff --git a/matita/matita/contribs/lambdadelta/basic_2/rt_computation/fpbs_lpxs.ma b/matita/matita/contribs/lambdadelta/basic_2/rt_computation/fpbs_lpxs.ma index 8a0a18405..6f1c51695 100644 --- a/matita/matita/contribs/lambdadelta/basic_2/rt_computation/fpbs_lpxs.ma +++ b/matita/matita/contribs/lambdadelta/basic_2/rt_computation/fpbs_lpxs.ma @@ -18,7 +18,7 @@ include "basic_2/rt_computation/fpbs_lfpxs.ma". (* 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 → @@ -27,7 +27,7 @@ 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⦄ → diff --git a/matita/matita/contribs/lambdadelta/basic_2/rt_computation/lfpxs.ma b/matita/matita/contribs/lambdadelta/basic_2/rt_computation/lfpxs.ma index fc6ad071e..0e1bee1d1 100644 --- a/matita/matita/contribs/lambdadelta/basic_2/rt_computation/lfpxs.ma +++ b/matita/matita/contribs/lambdadelta/basic_2/rt_computation/lfpxs.ma @@ -16,13 +16,13 @@ include "basic_2/notation/relations/predtysnstar_5.ma". 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 *********************************************************) diff --git a/matita/matita/contribs/lambdadelta/basic_2/rt_computation/lfpxs_aaa.ma b/matita/matita/contribs/lambdadelta/basic_2/rt_computation/lfpxs_aaa.ma index e3cbc16a4..43febff41 100644 --- a/matita/matita/contribs/lambdadelta/basic_2/rt_computation/lfpxs_aaa.ma +++ b/matita/matita/contribs/lambdadelta/basic_2/rt_computation/lfpxs_aaa.ma @@ -15,9 +15,9 @@ 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). diff --git a/matita/matita/contribs/lambdadelta/basic_2/rt_computation/lfpxs_cpxs.ma b/matita/matita/contribs/lambdadelta/basic_2/rt_computation/lfpxs_cpxs.ma index 6c951084e..a5288e11a 100644 --- a/matita/matita/contribs/lambdadelta/basic_2/rt_computation/lfpxs_cpxs.ma +++ b/matita/matita/contribs/lambdadelta/basic_2/rt_computation/lfpxs_cpxs.ma @@ -15,9 +15,9 @@ 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 → @@ -34,14 +34,14 @@ lemma lfpxs_cpxs_trans: ∀h,G. s_rs_transitive … (cpx h G) (lfpxs h G). @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 & diff --git a/matita/matita/contribs/lambdadelta/basic_2/rt_computation/lfpxs_drops.ma b/matita/matita/contribs/lambdadelta/basic_2/rt_computation/lfpxs_drops.ma index a1c78b6fd..caeb2bf77 100644 --- a/matita/matita/contribs/lambdadelta/basic_2/rt_computation/lfpxs_drops.ma +++ b/matita/matita/contribs/lambdadelta/basic_2/rt_computation/lfpxs_drops.ma @@ -15,7 +15,7 @@ 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 *******************) diff --git a/matita/matita/contribs/lambdadelta/basic_2/rt_computation/lfpxs_ffdeq.ma b/matita/matita/contribs/lambdadelta/basic_2/rt_computation/lfpxs_ffdeq.ma index 04f0d89fc..35ed9931b 100644 --- a/matita/matita/contribs/lambdadelta/basic_2/rt_computation/lfpxs_ffdeq.ma +++ b/matita/matita/contribs/lambdadelta/basic_2/rt_computation/lfpxs_ffdeq.ma @@ -15,7 +15,7 @@ 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 *********************) diff --git a/matita/matita/contribs/lambdadelta/basic_2/rt_computation/lfpxs_fqup.ma b/matita/matita/contribs/lambdadelta/basic_2/rt_computation/lfpxs_fqup.ma index 6c7615ce4..1ca306ddb 100644 --- a/matita/matita/contribs/lambdadelta/basic_2/rt_computation/lfpxs_fqup.ma +++ b/matita/matita/contribs/lambdadelta/basic_2/rt_computation/lfpxs_fqup.ma @@ -15,7 +15,7 @@ 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 ******************************************************) diff --git a/matita/matita/contribs/lambdadelta/basic_2/rt_computation/lfpxs_length.ma b/matita/matita/contribs/lambdadelta/basic_2/rt_computation/lfpxs_length.ma index 70c9539c9..27bf18d49 100644 --- a/matita/matita/contribs/lambdadelta/basic_2/rt_computation/lfpxs_length.ma +++ b/matita/matita/contribs/lambdadelta/basic_2/rt_computation/lfpxs_length.ma @@ -15,7 +15,7 @@ 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 ************************) diff --git a/matita/matita/contribs/lambdadelta/basic_2/rt_computation/lfpxs_lfdeq.ma b/matita/matita/contribs/lambdadelta/basic_2/rt_computation/lfpxs_lfdeq.ma index 2eda15369..2d6871c34 100644 --- a/matita/matita/contribs/lambdadelta/basic_2/rt_computation/lfpxs_lfdeq.ma +++ b/matita/matita/contribs/lambdadelta/basic_2/rt_computation/lfpxs_lfdeq.ma @@ -15,7 +15,7 @@ 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 ************************) diff --git a/matita/matita/contribs/lambdadelta/basic_2/rt_computation/lfpxs_lfpxs.ma b/matita/matita/contribs/lambdadelta/basic_2/rt_computation/lfpxs_lfpxs.ma index 09d004b2c..9f2b0b6e1 100644 --- a/matita/matita/contribs/lambdadelta/basic_2/rt_computation/lfpxs_lfpxs.ma +++ b/matita/matita/contribs/lambdadelta/basic_2/rt_computation/lfpxs_lfpxs.ma @@ -15,7 +15,7 @@ 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 **********************************************************) diff --git a/matita/matita/contribs/lambdadelta/basic_2/rt_computation/lfpxs_lpxs.ma b/matita/matita/contribs/lambdadelta/basic_2/rt_computation/lfpxs_lpxs.ma index 79b41f785..aa13ac53a 100644 --- a/matita/matita/contribs/lambdadelta/basic_2/rt_computation/lfpxs_lpxs.ma +++ b/matita/matita/contribs/lambdadelta/basic_2/rt_computation/lfpxs_lpxs.ma @@ -18,9 +18,9 @@ include "basic_2/rt_computation/cpxs_lpx.ma". 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. @@ -29,7 +29,7 @@ lemma lfpxs_lpxs_lfeq: ∀h,G,L1,L. ⦃G, L1⦄ ⊢ ⬈*[h] L → ∀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. diff --git a/matita/matita/contribs/lambdadelta/basic_2/rt_computation/lfsx.ma b/matita/matita/contribs/lambdadelta/basic_2/rt_computation/lfsx.ma index 4258c13dd..955d70edb 100644 --- a/matita/matita/contribs/lambdadelta/basic_2/rt_computation/lfsx.ma +++ b/matita/matita/contribs/lambdadelta/basic_2/rt_computation/lfsx.ma @@ -16,13 +16,13 @@ include "basic_2/notation/relations/predtysnstrong_5.ma". 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 ********************************************************) diff --git a/matita/matita/contribs/lambdadelta/basic_2/rt_computation/lfsx_csx.ma b/matita/matita/contribs/lambdadelta/basic_2/rt_computation/lfsx_csx.ma index b34b79890..bdaca97bc 100644 --- a/matita/matita/contribs/lambdadelta/basic_2/rt_computation/lfsx_csx.ma +++ b/matita/matita/contribs/lambdadelta/basic_2/rt_computation/lfsx_csx.ma @@ -19,7 +19,7 @@ include "basic_2/rt_computation/csx_lsubr.ma". 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 ******************************************************) diff --git a/matita/matita/contribs/lambdadelta/basic_2/rt_computation/lfsx_drops.ma b/matita/matita/contribs/lambdadelta/basic_2/rt_computation/lfsx_drops.ma index 488bb09cc..80adb96b2 100644 --- a/matita/matita/contribs/lambdadelta/basic_2/rt_computation/lfsx_drops.ma +++ b/matita/matita/contribs/lambdadelta/basic_2/rt_computation/lfsx_drops.ma @@ -18,7 +18,7 @@ include "basic_2/rt_transition/lfpx_length.ma". 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 ***************************************) diff --git a/matita/matita/contribs/lambdadelta/basic_2/rt_computation/lfsx_fqup.ma b/matita/matita/contribs/lambdadelta/basic_2/rt_computation/lfsx_fqup.ma index e9879a17c..a14bccf50 100644 --- a/matita/matita/contribs/lambdadelta/basic_2/rt_computation/lfsx_fqup.ma +++ b/matita/matita/contribs/lambdadelta/basic_2/rt_computation/lfsx_fqup.ma @@ -15,7 +15,7 @@ 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 ******************************************************) diff --git a/matita/matita/contribs/lambdadelta/basic_2/rt_computation/lfsx_lfpxs.ma b/matita/matita/contribs/lambdadelta/basic_2/rt_computation/lfsx_lfpxs.ma index 23250e0f6..5388d8b24 100644 --- a/matita/matita/contribs/lambdadelta/basic_2/rt_computation/lfsx_lfpxs.ma +++ b/matita/matita/contribs/lambdadelta/basic_2/rt_computation/lfsx_lfpxs.ma @@ -17,9 +17,9 @@ include "basic_2/rt_computation/lfpxs_cpxs.ma". 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. @@ -34,7 +34,7 @@ lemma lfsx_lfpxs_trans: ∀h,o,G,L1,T. G ⊢ ⬈*[h, o, T] 𝐒⦃L1⦄ → /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⦄ → diff --git a/matita/matita/contribs/lambdadelta/basic_2/rt_computation/lfsx_lfsx.ma b/matita/matita/contribs/lambdadelta/basic_2/rt_computation/lfsx_lfsx.ma index acb4447e3..350d4717d 100644 --- a/matita/matita/contribs/lambdadelta/basic_2/rt_computation/lfsx_lfsx.ma +++ b/matita/matita/contribs/lambdadelta/basic_2/rt_computation/lfsx_lfsx.ma @@ -15,7 +15,7 @@ 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 ******************************************************) diff --git a/matita/matita/contribs/lambdadelta/basic_2/rt_computation/lfsx_lpx.ma b/matita/matita/contribs/lambdadelta/basic_2/rt_computation/lfsx_lpx.ma index 3fa42466e..9b70b3b65 100644 --- a/matita/matita/contribs/lambdadelta/basic_2/rt_computation/lfsx_lpx.ma +++ b/matita/matita/contribs/lambdadelta/basic_2/rt_computation/lfsx_lpx.ma @@ -16,9 +16,9 @@ include "basic_2/static/lfdeq_lfeq.ma". 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⦄) → @@ -33,7 +33,7 @@ lemma lfsx_lpx_trans: ∀h,o,G,L1,T. G ⊢ ⬈*[h, o, T] 𝐒⦃L1⦄ → ∀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⦄ → diff --git a/matita/matita/contribs/lambdadelta/basic_2/rt_computation/lfsx_lpxs.ma b/matita/matita/contribs/lambdadelta/basic_2/rt_computation/lfsx_lpxs.ma index 8c8bd5a54..a534c3f72 100644 --- a/matita/matita/contribs/lambdadelta/basic_2/rt_computation/lfsx_lpxs.ma +++ b/matita/matita/contribs/lambdadelta/basic_2/rt_computation/lfsx_lpxs.ma @@ -16,9 +16,9 @@ include "basic_2/static/lfdeq_lfeq.ma". 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⦄) → @@ -33,7 +33,7 @@ lemma lfsx_lpxs_trans: ∀h,o,G,L1,T. G ⊢ ⬈*[h, o, T] 𝐒⦃L1⦄ → ∀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⦄ → diff --git a/matita/matita/contribs/lambdadelta/basic_2/rt_computation/lpxs.ma b/matita/matita/contribs/lambdadelta/basic_2/rt_computation/lpxs.ma index 8b08043fd..4969c4c73 100644 --- a/matita/matita/contribs/lambdadelta/basic_2/rt_computation/lpxs.ma +++ b/matita/matita/contribs/lambdadelta/basic_2/rt_computation/lpxs.ma @@ -16,13 +16,13 @@ include "basic_2/notation/relations/predtysnstar_4.ma". 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 *********************************************************) diff --git a/matita/matita/contribs/lambdadelta/basic_2/rt_computation/lpxs_cpxs.ma b/matita/matita/contribs/lambdadelta/basic_2/rt_computation/lpxs_cpxs.ma index b663f6a61..19cc746fc 100644 --- a/matita/matita/contribs/lambdadelta/basic_2/rt_computation/lpxs_cpxs.ma +++ b/matita/matita/contribs/lambdadelta/basic_2/rt_computation/lpxs_cpxs.ma @@ -15,9 +15,9 @@ 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-. diff --git a/matita/matita/contribs/lambdadelta/basic_2/rt_computation/lpxs_length.ma b/matita/matita/contribs/lambdadelta/basic_2/rt_computation/lpxs_length.ma index 8b086f40c..40c4dc8ef 100644 --- a/matita/matita/contribs/lambdadelta/basic_2/rt_computation/lpxs_length.ma +++ b/matita/matita/contribs/lambdadelta/basic_2/rt_computation/lpxs_length.ma @@ -15,7 +15,7 @@ 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 ************************) diff --git a/matita/matita/contribs/lambdadelta/basic_2/rt_computation/lpxs_lpx.ma b/matita/matita/contribs/lambdadelta/basic_2/rt_computation/lpxs_lpx.ma index d43fd613f..d12f1fe67 100644 --- a/matita/matita/contribs/lambdadelta/basic_2/rt_computation/lpxs_lpx.ma +++ b/matita/matita/contribs/lambdadelta/basic_2/rt_computation/lpxs_lpx.ma @@ -16,9 +16,9 @@ include "basic_2/relocation/lex_tc.ma". 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 → diff --git a/matita/matita/contribs/lambdadelta/basic_2/rt_computation/lsubsx.ma b/matita/matita/contribs/lambdadelta/basic_2/rt_computation/lsubsx.ma index 1a73fa89c..d7d552461 100644 --- a/matita/matita/contribs/lambdadelta/basic_2/rt_computation/lsubsx.ma +++ b/matita/matita/contribs/lambdadelta/basic_2/rt_computation/lsubsx.ma @@ -15,7 +15,7 @@ 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 *) diff --git a/matita/matita/contribs/lambdadelta/basic_2/rt_computation/lsubsx_lfsx.ma b/matita/matita/contribs/lambdadelta/basic_2/rt_computation/lsubsx_lfsx.ma index 059cb1ece..511e62369 100644 --- a/matita/matita/contribs/lambdadelta/basic_2/rt_computation/lsubsx_lfsx.ma +++ b/matita/matita/contribs/lambdadelta/basic_2/rt_computation/lsubsx_lfsx.ma @@ -16,9 +16,9 @@ include "basic_2/rt_computation/lfsx_drops.ma". 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 → @@ -63,7 +63,7 @@ lemma lfsx_cpx_trans: ∀h,o,G,L,T1,T2. ⦃G, L⦄ ⊢ 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⦄. diff --git a/matita/matita/contribs/lambdadelta/basic_2/rt_computation/lsubsx_lsubsx.ma b/matita/matita/contribs/lambdadelta/basic_2/rt_computation/lsubsx_lsubsx.ma index cf0daeaf4..018e5c262 100644 --- a/matita/matita/contribs/lambdadelta/basic_2/rt_computation/lsubsx_lsubsx.ma +++ b/matita/matita/contribs/lambdadelta/basic_2/rt_computation/lsubsx_lsubsx.ma @@ -14,7 +14,7 @@ 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 **********************************************************) diff --git a/matita/matita/contribs/lambdadelta/basic_2/rt_computation/partial.txt b/matita/matita/contribs/lambdadelta/basic_2/rt_computation/partial.txt index f5778c98f..24215a065 100644 --- a/matita/matita/contribs/lambdadelta/basic_2/rt_computation/partial.txt +++ b/matita/matita/contribs/lambdadelta/basic_2/rt_computation/partial.txt @@ -9,3 +9,4 @@ lsubsx.ma lsubsx_lfsx.ma lsubsx_lsubsx.ma fpbs.ma fpbs_fqup.ma fpbs_fqus.ma fpbs_aaa.ma fpbs_cpx.ma fpbs_fpb.ma fpbs_cpxs.ma fpbs_lpxs.ma fpbs_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 diff --git a/matita/matita/contribs/lambdadelta/basic_2/rt_computation/scpds.ma b/matita/matita/contribs/lambdadelta/basic_2/rt_computation/scpds.ma deleted file mode 100644 index 1f189c15e..000000000 --- a/matita/matita/contribs/lambdadelta/basic_2/rt_computation/scpds.ma +++ /dev/null @@ -1,48 +0,0 @@ -(**************************************************************************) -(* ___ *) -(* ||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-. diff --git a/matita/matita/contribs/lambdadelta/basic_2/rt_transition/cnx.ma b/matita/matita/contribs/lambdadelta/basic_2/rt_transition/cnx.ma index 5eb721b20..5aa9c9710 100644 --- a/matita/matita/contribs/lambdadelta/basic_2/rt_transition/cnx.ma +++ b/matita/matita/contribs/lambdadelta/basic_2/rt_transition/cnx.ma @@ -16,13 +16,13 @@ include "basic_2/notation/relations/predtynormal_5.ma". 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 ***************************************************) diff --git a/matita/matita/contribs/lambdadelta/basic_2/rt_transition/cnx_cnx.ma b/matita/matita/contribs/lambdadelta/basic_2/rt_transition/cnx_cnx.ma index ad6e5d0ec..4fd229e59 100644 --- a/matita/matita/contribs/lambdadelta/basic_2/rt_transition/cnx_cnx.ma +++ b/matita/matita/contribs/lambdadelta/basic_2/rt_transition/cnx_cnx.ma @@ -15,7 +15,7 @@ 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 ******************************************************) diff --git a/matita/matita/contribs/lambdadelta/basic_2/rt_transition/cnx_drops.ma b/matita/matita/contribs/lambdadelta/basic_2/rt_transition/cnx_drops.ma index 8b97e1bc4..c2479807a 100644 --- a/matita/matita/contribs/lambdadelta/basic_2/rt_transition/cnx_drops.ma +++ b/matita/matita/contribs/lambdadelta/basic_2/rt_transition/cnx_drops.ma @@ -16,7 +16,7 @@ include "basic_2/relocation/lifts_tdeq.ma". 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 ******************************************) diff --git a/matita/matita/contribs/lambdadelta/basic_2/rt_transition/cnx_simple.ma b/matita/matita/contribs/lambdadelta/basic_2/rt_transition/cnx_simple.ma index 272b82442..640e24d37 100644 --- a/matita/matita/contribs/lambdadelta/basic_2/rt_transition/cnx_simple.ma +++ b/matita/matita/contribs/lambdadelta/basic_2/rt_transition/cnx_simple.ma @@ -15,7 +15,7 @@ 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 ***************************************) diff --git a/matita/matita/contribs/lambdadelta/basic_2/rt_transition/cpg.ma b/matita/matita/contribs/lambdadelta/basic_2/rt_transition/cpg.ma index 317f69e05..f640625ca 100644 --- a/matita/matita/contribs/lambdadelta/basic_2/rt_transition/cpg.ma +++ b/matita/matita/contribs/lambdadelta/basic_2/rt_transition/cpg.ma @@ -20,7 +20,7 @@ include "basic_2/syntax/lenv.ma". 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 ≝ @@ -55,7 +55,7 @@ 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 *********************************************************) diff --git a/matita/matita/contribs/lambdadelta/basic_2/rt_transition/cpg_drops.ma b/matita/matita/contribs/lambdadelta/basic_2/rt_transition/cpg_drops.ma index 8b33836a2..8a5f96f91 100644 --- a/matita/matita/contribs/lambdadelta/basic_2/rt_transition/cpg_drops.ma +++ b/matita/matita/contribs/lambdadelta/basic_2/rt_transition/cpg_drops.ma @@ -17,7 +17,7 @@ include "basic_2/s_computation/fqup_weight.ma". 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 ******************************************************) diff --git a/matita/matita/contribs/lambdadelta/basic_2/rt_transition/cpg_lsubr.ma b/matita/matita/contribs/lambdadelta/basic_2/rt_transition/cpg_lsubr.ma index 77425cce7..fcb9275a1 100644 --- a/matita/matita/contribs/lambdadelta/basic_2/rt_transition/cpg_lsubr.ma +++ b/matita/matita/contribs/lambdadelta/basic_2/rt_transition/cpg_lsubr.ma @@ -15,7 +15,7 @@ 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 *************) diff --git a/matita/matita/contribs/lambdadelta/basic_2/rt_transition/cpg_simple.ma b/matita/matita/contribs/lambdadelta/basic_2/rt_transition/cpg_simple.ma index ee36acaac..c914decba 100644 --- a/matita/matita/contribs/lambdadelta/basic_2/rt_transition/cpg_simple.ma +++ b/matita/matita/contribs/lambdadelta/basic_2/rt_transition/cpg_simple.ma @@ -15,7 +15,7 @@ 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 *********************************************) diff --git a/matita/matita/contribs/lambdadelta/basic_2/rt_transition/cpm.ma b/matita/matita/contribs/lambdadelta/basic_2/rt_transition/cpm.ma index 81f381bf5..fa5499ccb 100644 --- a/matita/matita/contribs/lambdadelta/basic_2/rt_transition/cpm.ma +++ b/matita/matita/contribs/lambdadelta/basic_2/rt_transition/cpm.ma @@ -19,16 +19,16 @@ include "basic_2/rt_transition/cpg.ma". (* 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 *********************************************************) @@ -110,11 +110,12 @@ lemma cpm_theta: ∀n,h,p,G,L,V1,V,V2,W1,W2,T1,T2. /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 ***************************************************) diff --git a/matita/matita/contribs/lambdadelta/basic_2/rt_transition/cpm_cpx.ma b/matita/matita/contribs/lambdadelta/basic_2/rt_transition/cpm_cpx.ma index d459fff2a..6f07b0647 100644 --- a/matita/matita/contribs/lambdadelta/basic_2/rt_transition/cpm_cpx.ma +++ b/matita/matita/contribs/lambdadelta/basic_2/rt_transition/cpm_cpx.ma @@ -17,7 +17,7 @@ include "basic_2/rt_transition/cpm.ma". (* 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. diff --git a/matita/matita/contribs/lambdadelta/basic_2/rt_transition/cpm_drops.ma b/matita/matita/contribs/lambdadelta/basic_2/rt_transition/cpm_drops.ma index 4f04adc8f..f5915aeff 100644 --- a/matita/matita/contribs/lambdadelta/basic_2/rt_transition/cpm_drops.ma +++ b/matita/matita/contribs/lambdadelta/basic_2/rt_transition/cpm_drops.ma @@ -78,13 +78,13 @@ qed-. (* 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-. @@ -92,12 +92,12 @@ 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-. diff --git a/matita/matita/contribs/lambdadelta/basic_2/rt_transition/cpm_fsle.ma b/matita/matita/contribs/lambdadelta/basic_2/rt_transition/cpm_fsle.ma index 32aeee69b..c9d76fc51 100644 --- a/matita/matita/contribs/lambdadelta/basic_2/rt_transition/cpm_fsle.ma +++ b/matita/matita/contribs/lambdadelta/basic_2/rt_transition/cpm_fsle.ma @@ -19,14 +19,14 @@ include "basic_2/rt_transition/cpm_cpx.ma". (* 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-. diff --git a/matita/matita/contribs/lambdadelta/basic_2/rt_transition/cpm_lsubr.ma b/matita/matita/contribs/lambdadelta/basic_2/rt_transition/cpm_lsubr.ma index 4b246a283..20385588f 100644 --- a/matita/matita/contribs/lambdadelta/basic_2/rt_transition/cpm_lsubr.ma +++ b/matita/matita/contribs/lambdadelta/basic_2/rt_transition/cpm_lsubr.ma @@ -20,6 +20,6 @@ include "basic_2/rt_transition/cpm.ma". (* 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-. diff --git a/matita/matita/contribs/lambdadelta/basic_2/rt_transition/cpr_ext.ma b/matita/matita/contribs/lambdadelta/basic_2/rt_transition/cpr_ext.ma index b47bfc3e9..c76a80fcc 100644 --- a/matita/matita/contribs/lambdadelta/basic_2/rt_transition/cpr_ext.ma +++ b/matita/matita/contribs/lambdadelta/basic_2/rt_transition/cpr_ext.ma @@ -18,7 +18,7 @@ include "basic_2/rt_transition/cpm.ma". (* 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)" diff --git a/matita/matita/contribs/lambdadelta/basic_2/rt_transition/cpx.ma b/matita/matita/contribs/lambdadelta/basic_2/rt_transition/cpx.ma index 64d2c2128..f01bb675b 100644 --- a/matita/matita/contribs/lambdadelta/basic_2/rt_transition/cpx.ma +++ b/matita/matita/contribs/lambdadelta/basic_2/rt_transition/cpx.ma @@ -15,13 +15,13 @@ 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 *********************************************************) diff --git a/matita/matita/contribs/lambdadelta/basic_2/rt_transition/cpx_drops.ma b/matita/matita/contribs/lambdadelta/basic_2/rt_transition/cpx_drops.ma index 49b2f29d5..4fcea0470 100644 --- a/matita/matita/contribs/lambdadelta/basic_2/rt_transition/cpx_drops.ma +++ b/matita/matita/contribs/lambdadelta/basic_2/rt_transition/cpx_drops.ma @@ -15,7 +15,7 @@ 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 ******************************************************) diff --git a/matita/matita/contribs/lambdadelta/basic_2/rt_transition/cpx_ext.ma b/matita/matita/contribs/lambdadelta/basic_2/rt_transition/cpx_ext.ma index 16e73c92b..a12c86faa 100644 --- a/matita/matita/contribs/lambdadelta/basic_2/rt_transition/cpx_ext.ma +++ b/matita/matita/contribs/lambdadelta/basic_2/rt_transition/cpx_ext.ma @@ -15,11 +15,11 @@ 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). diff --git a/matita/matita/contribs/lambdadelta/basic_2/rt_transition/cpx_ffdeq.ma b/matita/matita/contribs/lambdadelta/basic_2/rt_transition/cpx_ffdeq.ma index 3b029ea5a..decfa484a 100644 --- a/matita/matita/contribs/lambdadelta/basic_2/rt_transition/cpx_ffdeq.ma +++ b/matita/matita/contribs/lambdadelta/basic_2/rt_transition/cpx_ffdeq.ma @@ -16,7 +16,7 @@ include "basic_2/static/ffdeq.ma". 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 ********************) diff --git a/matita/matita/contribs/lambdadelta/basic_2/rt_transition/cpx_fqus.ma b/matita/matita/contribs/lambdadelta/basic_2/rt_transition/cpx_fqus.ma index 06a3573c0..e4c7db152 100644 --- a/matita/matita/contribs/lambdadelta/basic_2/rt_transition/cpx_fqus.ma +++ b/matita/matita/contribs/lambdadelta/basic_2/rt_transition/cpx_fqus.ma @@ -12,7 +12,7 @@ (* *) (**************************************************************************) -(* 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". diff --git a/matita/matita/contribs/lambdadelta/basic_2/rt_transition/cpx_lfdeq.ma b/matita/matita/contribs/lambdadelta/basic_2/rt_transition/cpx_lfdeq.ma index c9fc90513..45a707603 100644 --- a/matita/matita/contribs/lambdadelta/basic_2/rt_transition/cpx_lfdeq.ma +++ b/matita/matita/contribs/lambdadelta/basic_2/rt_transition/cpx_lfdeq.ma @@ -15,7 +15,7 @@ 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 **********) diff --git a/matita/matita/contribs/lambdadelta/basic_2/rt_transition/cpx_lfeq.ma b/matita/matita/contribs/lambdadelta/basic_2/rt_transition/cpx_lfeq.ma index 441377d0d..48ae7a970 100644 --- a/matita/matita/contribs/lambdadelta/basic_2/rt_transition/cpx_lfeq.ma +++ b/matita/matita/contribs/lambdadelta/basic_2/rt_transition/cpx_lfeq.ma @@ -15,7 +15,7 @@ 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 ******) @@ -60,4 +60,4 @@ lemma cpx_lfeq_conf_sn: ∀h,G. s_r_confluent1 … (cpx h G) lfeq. 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 +*) diff --git a/matita/matita/contribs/lambdadelta/basic_2/rt_transition/cpx_lsubr.ma b/matita/matita/contribs/lambdadelta/basic_2/rt_transition/cpx_lsubr.ma index 58350fb86..864f8eb99 100644 --- a/matita/matita/contribs/lambdadelta/basic_2/rt_transition/cpx_lsubr.ma +++ b/matita/matita/contribs/lambdadelta/basic_2/rt_transition/cpx_lsubr.ma @@ -15,7 +15,7 @@ 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 *************) diff --git a/matita/matita/contribs/lambdadelta/basic_2/rt_transition/cpx_simple.ma b/matita/matita/contribs/lambdadelta/basic_2/rt_transition/cpx_simple.ma index fbc9eb644..a18e14b6c 100644 --- a/matita/matita/contribs/lambdadelta/basic_2/rt_transition/cpx_simple.ma +++ b/matita/matita/contribs/lambdadelta/basic_2/rt_transition/cpx_simple.ma @@ -15,7 +15,9 @@ 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 & diff --git a/matita/matita/contribs/lambdadelta/basic_2/rt_transition/lfpr.ma b/matita/matita/contribs/lambdadelta/basic_2/rt_transition/lfpr.ma index 072675fba..8781d1fdf 100644 --- a/matita/matita/contribs/lambdadelta/basic_2/rt_transition/lfpr.ma +++ b/matita/matita/contribs/lambdadelta/basic_2/rt_transition/lfpr.ma @@ -19,7 +19,7 @@ include "basic_2/rt_transition/cpr_ext.ma". (* 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)" diff --git a/matita/matita/contribs/lambdadelta/basic_2/rt_transition/lfpr_aaa.ma b/matita/matita/contribs/lambdadelta/basic_2/rt_transition/lfpr_aaa.ma index 899bfc1cf..d3dd5dd0d 100644 --- a/matita/matita/contribs/lambdadelta/basic_2/rt_transition/lfpr_aaa.ma +++ b/matita/matita/contribs/lambdadelta/basic_2/rt_transition/lfpr_aaa.ma @@ -19,7 +19,7 @@ include "basic_2/rt_transition/lfpr_lfpx.ma". (* 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 *) diff --git a/matita/matita/contribs/lambdadelta/basic_2/rt_transition/lfpr_drops.ma b/matita/matita/contribs/lambdadelta/basic_2/rt_transition/lfpr_drops.ma index 239200568..c0ceb1ef6 100644 --- a/matita/matita/contribs/lambdadelta/basic_2/rt_transition/lfpr_drops.ma +++ b/matita/matita/contribs/lambdadelta/basic_2/rt_transition/lfpr_drops.ma @@ -21,17 +21,17 @@ include "basic_2/rt_transition/lfpr.ma". (* 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 → diff --git a/matita/matita/contribs/lambdadelta/basic_2/rt_transition/lfpr_lfpr.ma b/matita/matita/contribs/lambdadelta/basic_2/rt_transition/lfpr_lfpr.ma index 498ecdb3b..7d3264482 100644 --- a/matita/matita/contribs/lambdadelta/basic_2/rt_transition/lfpr_lfpr.ma +++ b/matita/matita/contribs/lambdadelta/basic_2/rt_transition/lfpr_lfpr.ma @@ -302,7 +302,7 @@ lapply (lifts_mono … HX … HVU) -HX #H destruct /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 @@ -359,7 +359,7 @@ theorem cpr_conf_lfpr: ∀h,G. R_confluent2_lfxs (cpm 0 h G) (cpm 0 h G) (cpm 0 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 ********) diff --git a/matita/matita/contribs/lambdadelta/basic_2/rt_transition/lfpx.ma b/matita/matita/contribs/lambdadelta/basic_2/rt_transition/lfpx.ma index 68aed2bfb..29cbfe765 100644 --- a/matita/matita/contribs/lambdadelta/basic_2/rt_transition/lfpx.ma +++ b/matita/matita/contribs/lambdadelta/basic_2/rt_transition/lfpx.ma @@ -16,13 +16,13 @@ include "basic_2/notation/relations/predtysn_5.ma". 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 ***********************************************************) diff --git a/matita/matita/contribs/lambdadelta/basic_2/rt_transition/lfpx_aaa.ma b/matita/matita/contribs/lambdadelta/basic_2/rt_transition/lfpx_aaa.ma index 1b8b6d763..6dc8c1946 100644 --- a/matita/matita/contribs/lambdadelta/basic_2/rt_transition/lfpx_aaa.ma +++ b/matita/matita/contribs/lambdadelta/basic_2/rt_transition/lfpx_aaa.ma @@ -16,7 +16,7 @@ include "basic_2/static/aaa_drops.ma". 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 ************************) diff --git a/matita/matita/contribs/lambdadelta/basic_2/rt_transition/lfpx_drops.ma b/matita/matita/contribs/lambdadelta/basic_2/rt_transition/lfpx_drops.ma index 94ed9d8bf..9353adda6 100644 --- a/matita/matita/contribs/lambdadelta/basic_2/rt_transition/lfpx_drops.ma +++ b/matita/matita/contribs/lambdadelta/basic_2/rt_transition/lfpx_drops.ma @@ -16,7 +16,7 @@ include "basic_2/static/lfxs_drops.ma". 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 *******************) diff --git a/matita/matita/contribs/lambdadelta/basic_2/rt_transition/lfpx_fqup.ma b/matita/matita/contribs/lambdadelta/basic_2/rt_transition/lfpx_fqup.ma index c4963ad99..ab3d5b2a0 100644 --- a/matita/matita/contribs/lambdadelta/basic_2/rt_transition/lfpx_fqup.ma +++ b/matita/matita/contribs/lambdadelta/basic_2/rt_transition/lfpx_fqup.ma @@ -15,7 +15,7 @@ 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 ******************************************************) diff --git a/matita/matita/contribs/lambdadelta/basic_2/rt_transition/lfpx_fquq.ma b/matita/matita/contribs/lambdadelta/basic_2/rt_transition/lfpx_fquq.ma index 7378f0cd7..f08b90319 100644 --- a/matita/matita/contribs/lambdadelta/basic_2/rt_transition/lfpx_fquq.ma +++ b/matita/matita/contribs/lambdadelta/basic_2/rt_transition/lfpx_fquq.ma @@ -16,7 +16,7 @@ include "basic_2/rt_transition/lfpx_drops.ma". 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 ***************) diff --git a/matita/matita/contribs/lambdadelta/basic_2/rt_transition/lfpx_fsle.ma b/matita/matita/contribs/lambdadelta/basic_2/rt_transition/lfpx_fsle.ma index 58fcbf307..047fd37ae 100644 --- a/matita/matita/contribs/lambdadelta/basic_2/rt_transition/lfpx_fsle.ma +++ b/matita/matita/contribs/lambdadelta/basic_2/rt_transition/lfpx_fsle.ma @@ -17,7 +17,7 @@ include "basic_2/static/lfxs_fsle.ma". 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 *****) diff --git a/matita/matita/contribs/lambdadelta/basic_2/rt_transition/lfpx_length.ma b/matita/matita/contribs/lambdadelta/basic_2/rt_transition/lfpx_length.ma index 7b194bd71..6db77f62e 100644 --- a/matita/matita/contribs/lambdadelta/basic_2/rt_transition/lfpx_length.ma +++ b/matita/matita/contribs/lambdadelta/basic_2/rt_transition/lfpx_length.ma @@ -15,7 +15,7 @@ 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 ************************) diff --git a/matita/matita/contribs/lambdadelta/basic_2/rt_transition/lfpx_lfdeq.ma b/matita/matita/contribs/lambdadelta/basic_2/rt_transition/lfpx_lfdeq.ma index 856fccf53..090ec1cbf 100644 --- a/matita/matita/contribs/lambdadelta/basic_2/rt_transition/lfpx_lfdeq.ma +++ b/matita/matita/contribs/lambdadelta/basic_2/rt_transition/lfpx_lfdeq.ma @@ -16,7 +16,7 @@ include "basic_2/static/lfdeq_fqup.ma". 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 **********) diff --git a/matita/matita/contribs/lambdadelta/basic_2/rt_transition/lfpx_lfpx.ma b/matita/matita/contribs/lambdadelta/basic_2/rt_transition/lfpx_lfpx.ma index c63d7120e..102ae91db 100644 --- a/matita/matita/contribs/lambdadelta/basic_2/rt_transition/lfpx_lfpx.ma +++ b/matita/matita/contribs/lambdadelta/basic_2/rt_transition/lfpx_lfpx.ma @@ -15,7 +15,7 @@ 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 **********************************************************) diff --git a/matita/matita/contribs/lambdadelta/basic_2/rt_transition/lfpx_lpx.ma b/matita/matita/contribs/lambdadelta/basic_2/rt_transition/lfpx_lpx.ma index 034ce9c7e..7fa9f9508 100644 --- a/matita/matita/contribs/lambdadelta/basic_2/rt_transition/lfpx_lpx.ma +++ b/matita/matita/contribs/lambdadelta/basic_2/rt_transition/lfpx_lpx.ma @@ -16,14 +16,14 @@ include "basic_2/static/lfxs_lex.ma". 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. diff --git a/matita/matita/contribs/lambdadelta/basic_2/rt_transition/lpx.ma b/matita/matita/contribs/lambdadelta/basic_2/rt_transition/lpx.ma index a5d9966be..96305c55b 100644 --- a/matita/matita/contribs/lambdadelta/basic_2/rt_transition/lpx.ma +++ b/matita/matita/contribs/lambdadelta/basic_2/rt_transition/lpx.ma @@ -16,13 +16,13 @@ include "basic_2/notation/relations/predtysn_4.ma". 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 *********************************************************) diff --git a/matita/matita/contribs/lambdadelta/basic_2/web/basic_2_src.tbl b/matita/matita/contribs/lambdadelta/basic_2/web/basic_2_src.tbl index f6b46722c..03ea90426 100644 --- a/matita/matita/contribs/lambdadelta/basic_2/web/basic_2_src.tbl +++ b/matita/matita/contribs/lambdadelta/basic_2/web/basic_2_src.tbl @@ -84,13 +84,17 @@ table { } ] *) - [ { "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" * ] @@ -105,7 +109,7 @@ table { ] 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" * ] } @@ -120,7 +124,7 @@ table { [ [ "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" + "( ⦃?,?⦄ ⊢ ⬈[?] ? )" * ] @@ -128,7 +132,7 @@ table { [ [ "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" * ] } ] -- 2.39.2