From 57ae1762497a5f3ea75740e2908e04adb8642cc2 Mon Sep 17 00:00:00 2001 From: Ferruccio Guidi Date: Wed, 15 Jan 2020 20:22:26 +0100 Subject: [PATCH] update in basic_2 + notation update for cnx and related notions --- .../lambdadelta/basic_2/dynamic/cnv_fsb.ma | 4 +- .../lambdadelta/basic_2/dynamic/nta_fsb.ma | 2 +- .../notation/relations/predsubtystrong_4.ma | 2 +- .../notation/relations/predtynormal_4.ma | 2 +- .../notation/relations/predtysnstrong_4.ma | 2 +- .../notation/relations/predtystrong_4.ma | 2 +- .../basic_2/rt_computation/cpmuwe_csx.ma | 4 +- .../basic_2/rt_computation/cprre_csx.ma | 2 +- .../basic_2/rt_computation/cpxs_cnx.ma | 4 +- .../basic_2/rt_computation/cpxs_teqo.ma | 2 +- .../rt_computation/cpxs_teqo_vector.ma | 2 +- .../lambdadelta/basic_2/rt_computation/csx.ma | 60 +++++++++++-------- .../basic_2/rt_computation/csx_aaa.ma | 47 ++++++++------- .../basic_2/rt_computation/csx_cnx.ma | 6 +- .../basic_2/rt_computation/csx_cnx_vector.ma | 6 +- .../basic_2/rt_computation/csx_cpxs.ma | 34 ++++++----- .../basic_2/rt_computation/csx_csx.ma | 40 ++++++------- .../basic_2/rt_computation/csx_csx_vector.ma | 30 +++++----- .../basic_2/rt_computation/csx_drops.ma | 6 +- .../basic_2/rt_computation/csx_feqx.ma | 5 +- .../basic_2/rt_computation/csx_fpbq.ma | 5 +- .../basic_2/rt_computation/csx_fqus.ma | 8 +-- .../basic_2/rt_computation/csx_gcp.ma | 3 +- .../basic_2/rt_computation/csx_gcr.ma | 3 +- .../basic_2/rt_computation/csx_lpx.ma | 44 +++++++------- .../basic_2/rt_computation/csx_lpxs.ma | 4 +- .../basic_2/rt_computation/csx_lsubr.ma | 34 +++++------ .../basic_2/rt_computation/csx_reqx.ma | 11 ++-- .../basic_2/rt_computation/csx_simple.ma | 7 ++- .../basic_2/rt_computation/csx_simple_teqo.ma | 6 +- .../basic_2/rt_computation/csx_vector.ma | 14 +++-- .../basic_2/rt_computation/fpbs_csx.ma | 4 +- .../lambdadelta/basic_2/rt_computation/fsb.ma | 16 ++--- .../basic_2/rt_computation/fsb_aaa.ma | 55 +++++++++-------- .../basic_2/rt_computation/fsb_csx.ma | 37 +++++++----- .../basic_2/rt_computation/fsb_feqx.ma | 4 +- .../basic_2/rt_computation/fsb_fpbg.ma | 18 +++--- .../lambdadelta/basic_2/rt_computation/jsx.ma | 11 ++-- .../basic_2/rt_computation/jsx_csx.ma | 6 +- .../basic_2/rt_computation/jsx_drops.ma | 2 +- .../basic_2/rt_computation/jsx_lsubr.ma | 3 +- .../basic_2/rt_computation/jsx_rsx.ma | 6 +- .../lambdadelta/basic_2/rt_computation/rsx.ma | 36 +++++------ .../basic_2/rt_computation/rsx_csx.ma | 35 +++++------ .../basic_2/rt_computation/rsx_drops.ma | 16 +++-- .../basic_2/rt_computation/rsx_fqup.ma | 8 +-- .../basic_2/rt_computation/rsx_length.ma | 6 +- .../basic_2/rt_computation/rsx_lpxs.ma | 58 +++++++++--------- .../basic_2/rt_computation/rsx_rsx.ma | 8 +-- .../basic_2/rt_equivalence/cpcs_csx.ma | 2 +- .../lambdadelta/basic_2/rt_transition/cnx.ma | 16 ++--- .../basic_2/rt_transition/cnx_basic.ma | 3 +- .../basic_2/rt_transition/cnx_cnx.ma | 4 +- .../basic_2/rt_transition/cnx_drops.ma | 7 ++- .../basic_2/rt_transition/cnx_simple.ma | 8 +-- .../lambdadelta/basic_2/web/basic_2_src.tbl | 10 ++-- 56 files changed, 413 insertions(+), 367 deletions(-) diff --git a/matita/matita/contribs/lambdadelta/basic_2/dynamic/cnv_fsb.ma b/matita/matita/contribs/lambdadelta/basic_2/dynamic/cnv_fsb.ma index 381030317..866a48566 100644 --- a/matita/matita/contribs/lambdadelta/basic_2/dynamic/cnv_fsb.ma +++ b/matita/matita/contribs/lambdadelta/basic_2/dynamic/cnv_fsb.ma @@ -22,14 +22,14 @@ include "basic_2/dynamic/cnv_aaa.ma". (* Note: this is the "big tree" theorem *) (* Basic_2A1: uses: snv_fwd_fsb *) lemma cnv_fwd_fsb (h) (a): - ∀G,L,T. ❪G,L❫ ⊢ T ![h,a] → ≥[h] 𝐒❪G,L,T❫. + ∀G,L,T. ❪G,L❫ ⊢ T ![h,a] → ≥𝐒[h] ❪G,L,T❫. #h #a #G #L #T #H elim (cnv_fwd_aaa … H) -H /2 width=2 by aaa_fsb/ qed-. (* Forward lemmas with strongly rt-normalizing terms ************************) lemma cnv_fwd_csx (h) (a): - ∀G,L,T. ❪G,L❫ ⊢ T ![h,a] → ❪G,L❫ ⊢ ⬈*[h] 𝐒❪T❫. + ∀G,L,T. ❪G,L❫ ⊢ T ![h,a] → ❪G,L❫ ⊢ ⬈*𝐒[h] T. #h #a #G #L #T #H /3 width=2 by cnv_fwd_fsb, fsb_inv_csx/ qed-. diff --git a/matita/matita/contribs/lambdadelta/basic_2/dynamic/nta_fsb.ma b/matita/matita/contribs/lambdadelta/basic_2/dynamic/nta_fsb.ma index f3ae36256..7e94833d3 100644 --- a/matita/matita/contribs/lambdadelta/basic_2/dynamic/nta_fsb.ma +++ b/matita/matita/contribs/lambdadelta/basic_2/dynamic/nta_fsb.ma @@ -25,7 +25,7 @@ include "basic_2/dynamic/nta.ma". (* Basic_2A1: uses: nta_fwd_csn *) theorem nta_fwd_fsb (h) (a) (G) (L): ∀T,U. ❪G,L❫ ⊢ T :[h,a] U → - ∧∧ ≥[h] 𝐒❪G,L,T❫ & ≥[h] 𝐒❪G,L,U❫. + ∧∧ ≥𝐒[h] ❪G,L,T❫ & ≥𝐒[h] ❪G,L,U❫. #h #a #G #L #T #U #H elim (cnv_inv_cast … H) #X #HU #HT #_ #_ -X /3 width=2 by cnv_fwd_fsb, conj/ diff --git a/matita/matita/contribs/lambdadelta/basic_2/notation/relations/predsubtystrong_4.ma b/matita/matita/contribs/lambdadelta/basic_2/notation/relations/predsubtystrong_4.ma index 877f6941a..2006de0a7 100644 --- a/matita/matita/contribs/lambdadelta/basic_2/notation/relations/predsubtystrong_4.ma +++ b/matita/matita/contribs/lambdadelta/basic_2/notation/relations/predsubtystrong_4.ma @@ -14,6 +14,6 @@ (* NOTATION FOR THE FORMAL SYSTEM λδ ****************************************) -notation "hvbox( ≥[ term 46 h ] 𝐒❪ break term 46 G, break term 46 L, break term 46 T ❫ )" +notation "hvbox( ≥𝐒[ term 46 h ] ❪ break term 46 G, break term 46 L, break term 46 T ❫ )" non associative with precedence 45 for @{ 'PRedSubTyStrong $h $G $L $T }. diff --git a/matita/matita/contribs/lambdadelta/basic_2/notation/relations/predtynormal_4.ma b/matita/matita/contribs/lambdadelta/basic_2/notation/relations/predtynormal_4.ma index ebcc11f45..b31ae8a3b 100644 --- a/matita/matita/contribs/lambdadelta/basic_2/notation/relations/predtynormal_4.ma +++ b/matita/matita/contribs/lambdadelta/basic_2/notation/relations/predtynormal_4.ma @@ -14,6 +14,6 @@ (* NOTATION FOR THE FORMAL SYSTEM λδ ****************************************) -notation "hvbox( ❪ term 46 G, break term 46 L ❫ ⊢ ⬈[ break term 46 h ] 𝐍❪ break term 46 T ❫ )" +notation "hvbox( ❪ term 46 G, break term 46 L ❫ ⊢ ⬈𝐍[ break term 46 h ] break term 46 T )" non associative with precedence 45 for @{ 'PRedTyNormal $h $G $L $T }. diff --git a/matita/matita/contribs/lambdadelta/basic_2/notation/relations/predtysnstrong_4.ma b/matita/matita/contribs/lambdadelta/basic_2/notation/relations/predtysnstrong_4.ma index 790d5fd55..af9ca53c1 100644 --- a/matita/matita/contribs/lambdadelta/basic_2/notation/relations/predtysnstrong_4.ma +++ b/matita/matita/contribs/lambdadelta/basic_2/notation/relations/predtysnstrong_4.ma @@ -14,6 +14,6 @@ (* NOTATION FOR THE FORMAL SYSTEM λδ ****************************************) -notation "hvbox( G ⊢ ⬈*[ break term 46 h, break term 46 T ] 𝐒❪ break term 46 L ❫ )" +notation "hvbox( G ⊢ ⬈*𝐒[ break term 46 h, break term 46 T ] break term 46 L )" non associative with precedence 45 for @{ 'PRedTySNStrong $h $T $G $L }. diff --git a/matita/matita/contribs/lambdadelta/basic_2/notation/relations/predtystrong_4.ma b/matita/matita/contribs/lambdadelta/basic_2/notation/relations/predtystrong_4.ma index 97ad5aab0..e2da53d28 100644 --- a/matita/matita/contribs/lambdadelta/basic_2/notation/relations/predtystrong_4.ma +++ b/matita/matita/contribs/lambdadelta/basic_2/notation/relations/predtystrong_4.ma @@ -14,6 +14,6 @@ (* NOTATION FOR THE FORMAL SYSTEM λδ ****************************************) -notation "hvbox( ❪ term 46 G, break term 46 L ❫ ⊢ ⬈*[ break term 46 h] 𝐒❪ break term 46 T ❫ )" +notation "hvbox( ❪ term 46 G, break term 46 L ❫ ⊢ ⬈*𝐒[ break term 46 h ] break term 46 T )" non associative with precedence 45 for @{ 'PRedTyStrong $h $G $L $T }. diff --git a/matita/matita/contribs/lambdadelta/basic_2/rt_computation/cpmuwe_csx.ma b/matita/matita/contribs/lambdadelta/basic_2/rt_computation/cpmuwe_csx.ma index 026418f4b..3fb6d1cd9 100644 --- a/matita/matita/contribs/lambdadelta/basic_2/rt_computation/cpmuwe_csx.ma +++ b/matita/matita/contribs/lambdadelta/basic_2/rt_computation/cpmuwe_csx.ma @@ -23,7 +23,7 @@ include "basic_2/rt_computation/cpmuwe.ma". (* Properties with strong normalization for unbound rt-transition for terms *) lemma cpmuwe_total_csx (h) (G) (L): - ∀T1. ❪G,L❫ ⊢ ⬈*[h] 𝐒❪T1❫ → ∃∃T2,n. ❪G,L❫ ⊢ T1 ➡*𝐍𝐖*[h,n] T2. + ∀T1. ❪G,L❫ ⊢ ⬈*𝐒[h] T1 → ∃∃T2,n. ❪G,L❫ ⊢ T1 ➡*𝐍𝐖*[h,n] T2. #h #G #L #T1 #H @(csx_ind_cpxs … H) -T1 #T1 #_ #IHT1 elim (cnuw_dec_ex h G L T1) @@ -38,7 +38,7 @@ elim (cnuw_dec_ex h G L T1) qed-. lemma R_cpmuwe_total_csx (h) (G) (L): - ∀T1. ❪G,L❫ ⊢ ⬈*[h] 𝐒❪T1❫ → ∃n. R_cpmuwe h G L T1 n. + ∀T1. ❪G,L❫ ⊢ ⬈*𝐒[h] T1 → ∃n. R_cpmuwe h G L T1 n. #h #G #L #T1 #H elim (cpmuwe_total_csx … H) -H #T2 #n #HT12 /3 width=3 by ex_intro (* 2x *)/ diff --git a/matita/matita/contribs/lambdadelta/basic_2/rt_computation/cprre_csx.ma b/matita/matita/contribs/lambdadelta/basic_2/rt_computation/cprre_csx.ma index a6675e4b4..2642f686e 100644 --- a/matita/matita/contribs/lambdadelta/basic_2/rt_computation/cprre_csx.ma +++ b/matita/matita/contribs/lambdadelta/basic_2/rt_computation/cprre_csx.ma @@ -24,7 +24,7 @@ include "basic_2/rt_computation/cprre.ma". (* Basic_1: was just: nf2_sn3 *) (* Basic_2A1: was: csx_cpre *) lemma cprre_total_csx (h) (G) (L): - ∀T1. ❪G,L❫ ⊢ ⬈*[h] 𝐒❪T1❫ → ∃T2. ❪G,L❫ ⊢ T1 ➡*𝐍[h,0] T2. + ∀T1. ❪G,L❫ ⊢ ⬈*𝐒[h] T1 → ∃T2. ❪G,L❫ ⊢ T1 ➡*𝐍[h,0] T2. #h #G #L #T1 #H @(csx_ind … H) -T1 #T1 #_ #IHT1 elim (cnr_dec_teqx h G L T1) [ /3 width=3 by ex_intro, cpmre_intro/ ] * 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 98e81b543..a2dc4c885 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 @@ -20,13 +20,13 @@ include "basic_2/rt_computation/cpxs.ma". (* Properties with normal forms *********************************************) lemma cpxs_cnx (h) (G) (L) (T1): - (∀T2. ❪G,L❫ ⊢ T1 ⬈*[h] T2 → T1 ≛ T2) → ❪G,L❫ ⊢ ⬈[h] 𝐍❪T1❫. + (∀T2. ❪G,L❫ ⊢ T1 ⬈*[h] T2 → T1 ≛ T2) → ❪G,L❫ ⊢ ⬈𝐍[h] T1. /3 width=1 by cpx_cpxs/ qed. (* Inversion lemmas with normal terms ***************************************) lemma cpxs_inv_cnx1 (h) (G) (L): - ∀T1,T2. ❪G,L❫ ⊢ T1 ⬈*[h] T2 → ❪G,L❫ ⊢ ⬈[h] 𝐍❪T1❫ → T1 ≛ T2. + ∀T1,T2. ❪G,L❫ ⊢ T1 ⬈*[h] T2 → ❪G,L❫ ⊢ ⬈𝐍[h] T1 → T1 ≛ T2. #h #G #L #T1 #T2 #H @(cpxs_ind_dx … H) -T1 /5 width=9 by cnx_teqx_trans, teqx_trans/ qed-. diff --git a/matita/matita/contribs/lambdadelta/basic_2/rt_computation/cpxs_teqo.ma b/matita/matita/contribs/lambdadelta/basic_2/rt_computation/cpxs_teqo.ma index cd6c84688..b71b21075 100644 --- a/matita/matita/contribs/lambdadelta/basic_2/rt_computation/cpxs_teqo.ma +++ b/matita/matita/contribs/lambdadelta/basic_2/rt_computation/cpxs_teqo.ma @@ -97,6 +97,6 @@ elim (cpxs_inv_cast1 … H) -H /2 width=1 by or3_intro1, or3_intro2/ * qed-. lemma cpxs_fwd_cnx (h) (G) (L): - ∀T1. ❪G,L❫ ⊢ ⬈[h] 𝐍❪T1❫ → + ∀T1. ❪G,L❫ ⊢ ⬈𝐍[h] T1 → ∀X2. ❪G,L❫ ⊢ T1 ⬈*[h] X2 → T1 ⩳ X2. /3 width=5 by cpxs_inv_cnx1, teqx_teqo/ qed-. diff --git a/matita/matita/contribs/lambdadelta/basic_2/rt_computation/cpxs_teqo_vector.ma b/matita/matita/contribs/lambdadelta/basic_2/rt_computation/cpxs_teqo_vector.ma index b3236af74..96e1fbb61 100644 --- a/matita/matita/contribs/lambdadelta/basic_2/rt_computation/cpxs_teqo_vector.ma +++ b/matita/matita/contribs/lambdadelta/basic_2/rt_computation/cpxs_teqo_vector.ma @@ -172,7 +172,7 @@ qed-. (* Basic_1: was just: nf2_iso_appls_lref *) lemma cpxs_fwd_cnx_vector (h) (G) (L): - ∀T. 𝐒❪T❫ → ❪G,L❫ ⊢ ⬈[h] 𝐍❪T❫ → + ∀T. 𝐒❪T❫ → ❪G,L❫ ⊢ ⬈𝐍[h] T → ∀Vs,X2. ❪G,L❫ ⊢ ⒶVs.T ⬈*[h] X2 → ⒶVs.T ⩳ X2. #h #G #L #T #H1T #H2T #Vs elim Vs -Vs [ @(cpxs_fwd_cnx … H2T) ] (**) (* /2 width=3 by cpxs_fwd_cnx/ does not work *) #V #Vs #IHVs #X2 #H 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 9ed838235..31f2e017a 100644 --- a/matita/matita/contribs/lambdadelta/basic_2/rt_computation/csx.ma +++ b/matita/matita/contribs/lambdadelta/basic_2/rt_computation/csx.ma @@ -18,21 +18,21 @@ include "basic_2/rt_transition/cpx.ma". (* STRONGLY NORMALIZING TERMS FOR UNBOUND PARALLEL RT-TRANSITION ************) -definition csx: ∀h. relation3 genv lenv term ≝ - λh,G,L. SN … (cpx h G L) teqx. +definition csx (h) (G) (L): predicate term ≝ + SN … (cpx h G L) teqx. interpretation - "strong normalization for unbound context-sensitive parallel rt-transition (term)" - 'PRedTyStrong h G L T = (csx h G L T). + "strong normalization for unbound context-sensitive parallel rt-transition (term)" + 'PRedTyStrong h G L T = (csx h G L T). (* Basic eliminators ********************************************************) -lemma csx_ind: ∀h,G,L. ∀Q:predicate term. - (∀T1. ❪G,L❫ ⊢ ⬈*[h] 𝐒❪T1❫ → - (∀T2. ❪G,L❫ ⊢ T1 ⬈[h] T2 → (T1 ≛ T2 → ⊥) → Q T2) → - Q T1 - ) → - ∀T. ❪G,L❫ ⊢ ⬈*[h] 𝐒❪T❫ → Q T. +lemma csx_ind (h) (G) (L) (Q:predicate …): + (∀T1. ❪G,L❫ ⊢ ⬈*𝐒[h] T1 → + (∀T2. ❪G,L❫ ⊢ T1 ⬈[h] T2 → (T1 ≛ T2 → ⊥) → Q T2) → + Q T1 + ) → + ∀T. ❪G,L❫ ⊢ ⬈*𝐒[h] T → Q T. #h #G #L #Q #H0 #T1 #H elim H -T1 /5 width=1 by SN_intro/ qed-. @@ -40,15 +40,16 @@ qed-. (* Basic properties *********************************************************) (* Basic_1: was just: sn3_pr2_intro *) -lemma csx_intro: ∀h,G,L,T1. - (∀T2. ❪G,L❫ ⊢ T1 ⬈[h] T2 → (T1 ≛ T2 → ⊥) → ❪G,L❫ ⊢ ⬈*[h] 𝐒❪T2❫) → - ❪G,L❫ ⊢ ⬈*[h] 𝐒❪T1❫. +lemma csx_intro (h) (G) (L): + ∀T1. (∀T2. ❪G,L❫ ⊢ T1 ⬈[h] T2 → (T1 ≛ T2 → ⊥) → ❪G,L❫ ⊢ ⬈*𝐒[h] T2) → + ❪G,L❫ ⊢ ⬈*𝐒[h] T1. /4 width=1 by SN_intro/ qed. (* Basic forward lemmas *****************************************************) -fact csx_fwd_pair_sn_aux: ∀h,G,L,U. ❪G,L❫ ⊢ ⬈*[h] 𝐒❪U❫ → - ∀I,V,T. U = ②[I]V.T → ❪G,L❫ ⊢ ⬈*[h] 𝐒❪V❫. +fact csx_fwd_pair_sn_aux (h) (G) (L): + ∀U. ❪G,L❫ ⊢ ⬈*𝐒[h] U → + ∀I,V,T. U = ②[I]V.T → ❪G,L❫ ⊢ ⬈*𝐒[h] V. #h #G #L #U #H elim H -H #U0 #_ #IH #I #V #T #H destruct @csx_intro #V2 #HLV2 #HV2 @(IH (②[I]V2.T)) -IH /2 width=3 by cpx_pair_sn/ -HLV2 @@ -56,11 +57,13 @@ fact csx_fwd_pair_sn_aux: ∀h,G,L,U. ❪G,L❫ ⊢ ⬈*[h] 𝐒❪U❫ → qed-. (* Basic_1: was just: sn3_gen_head *) -lemma csx_fwd_pair_sn: ∀h,I,G,L,V,T. ❪G,L❫ ⊢ ⬈*[h] 𝐒❪②[I]V.T❫ → ❪G,L❫ ⊢ ⬈*[h] 𝐒❪V❫. +lemma csx_fwd_pair_sn (h) (G) (L): + ∀I,V,T. ❪G,L❫ ⊢ ⬈*𝐒[h] ②[I]V.T → ❪G,L❫ ⊢ ⬈*𝐒[h] V. /2 width=5 by csx_fwd_pair_sn_aux/ qed-. -fact csx_fwd_bind_dx_aux: ∀h,G,L,U. ❪G,L❫ ⊢ ⬈*[h] 𝐒❪U❫ → - ∀p,I,V,T. U = ⓑ[p,I]V.T → ❪G,L.ⓑ[I]V❫ ⊢ ⬈*[h] 𝐒❪T❫. +fact csx_fwd_bind_dx_aux (h) (G) (L): + ∀U. ❪G,L❫ ⊢ ⬈*𝐒[h] U → + ∀p,I,V,T. U = ⓑ[p,I]V.T → ❪G,L.ⓑ[I]V❫ ⊢ ⬈*𝐒[h] T. #h #G #L #U #H elim H -H #U0 #_ #IH #p #I #V #T #H destruct @csx_intro #T2 #HLT2 #HT2 @(IH (ⓑ[p, I]V.T2)) -IH /2 width=3 by cpx_bind/ -HLT2 @@ -68,11 +71,13 @@ fact csx_fwd_bind_dx_aux: ∀h,G,L,U. ❪G,L❫ ⊢ ⬈*[h] 𝐒❪U❫ → qed-. (* Basic_1: was just: sn3_gen_bind *) -lemma csx_fwd_bind_dx: ∀h,p,I,G,L,V,T. ❪G,L❫ ⊢ ⬈*[h] 𝐒❪ⓑ[p,I]V.T❫ → ❪G,L.ⓑ[I]V❫ ⊢ ⬈*[h] 𝐒❪T❫. +lemma csx_fwd_bind_dx (h) (G) (L): + ∀p,I,V,T. ❪G,L❫ ⊢ ⬈*𝐒[h] ⓑ[p,I]V.T → ❪G,L.ⓑ[I]V❫ ⊢ ⬈*𝐒[h] T. /2 width=4 by csx_fwd_bind_dx_aux/ qed-. -fact csx_fwd_flat_dx_aux: ∀h,G,L,U. ❪G,L❫ ⊢ ⬈*[h] 𝐒❪U❫ → - ∀I,V,T. U = ⓕ[I]V.T → ❪G,L❫ ⊢ ⬈*[h] 𝐒❪T❫. +fact csx_fwd_flat_dx_aux (h) (G) (L): + ∀U. ❪G,L❫ ⊢ ⬈*𝐒[h] U → + ∀I,V,T. U = ⓕ[I]V.T → ❪G,L❫ ⊢ ⬈*𝐒[h] T. #h #G #L #U #H elim H -H #U0 #_ #IH #I #V #T #H destruct @csx_intro #T2 #HLT2 #HT2 @(IH (ⓕ[I]V.T2)) -IH /2 width=3 by cpx_flat/ -HLT2 @@ -80,15 +85,18 @@ fact csx_fwd_flat_dx_aux: ∀h,G,L,U. ❪G,L❫ ⊢ ⬈*[h] 𝐒❪U❫ → qed-. (* Basic_1: was just: sn3_gen_flat *) -lemma csx_fwd_flat_dx: ∀h,I,G,L,V,T. ❪G,L❫ ⊢ ⬈*[h] 𝐒❪ⓕ[I]V.T❫ → ❪G,L❫ ⊢ ⬈*[h] 𝐒❪T❫. +lemma csx_fwd_flat_dx (h) (G) (L): + ∀I,V,T. ❪G,L❫ ⊢ ⬈*𝐒[h] ⓕ[I]V.T → ❪G,L❫ ⊢ ⬈*𝐒[h] T. /2 width=5 by csx_fwd_flat_dx_aux/ qed-. -lemma csx_fwd_bind: ∀h,p,I,G,L,V,T. ❪G,L❫ ⊢ ⬈*[h] 𝐒❪ⓑ[p,I]V.T❫ → - ❪G,L❫ ⊢ ⬈*[h] 𝐒❪V❫ ∧ ❪G,L.ⓑ[I]V❫ ⊢ ⬈*[h] 𝐒❪T❫. +lemma csx_fwd_bind (h) (G) (L): + ∀p,I,V,T. ❪G,L❫ ⊢ ⬈*𝐒[h] ⓑ[p,I]V.T → + ∧∧ ❪G,L❫ ⊢ ⬈*𝐒[h] V & ❪G,L.ⓑ[I]V❫ ⊢ ⬈*𝐒[h] T. /3 width=3 by csx_fwd_pair_sn, csx_fwd_bind_dx, conj/ qed-. -lemma csx_fwd_flat: ∀h,I,G,L,V,T. ❪G,L❫ ⊢ ⬈*[h] 𝐒❪ⓕ[I]V.T❫ → - ❪G,L❫ ⊢ ⬈*[h] 𝐒❪V❫ ∧ ❪G,L❫ ⊢ ⬈*[h] 𝐒❪T❫. +lemma csx_fwd_flat (h) (G) (L): + ∀I,V,T. ❪G,L❫ ⊢ ⬈*𝐒[h] ⓕ[I]V.T → + ∧∧ ❪G,L❫ ⊢ ⬈*𝐒[h] V & ❪G,L❫ ⊢ ⬈*𝐒[h] T. /3 width=3 by csx_fwd_pair_sn, csx_fwd_flat_dx, conj/ qed-. (* Basic_1: removed theorems 14: 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 c963c06a4..2f2544ad8 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 @@ -21,40 +21,45 @@ include "basic_2/rt_computation/csx_gcr.ma". (* Main properties with atomic arity assignment *****************************) -theorem aaa_csx: ∀h,G,L,T,A. ❪G,L❫ ⊢ T ⁝ A → ❪G,L❫ ⊢ ⬈*[h] 𝐒❪T❫. +theorem aaa_csx (h) (G) (L): + ∀T,A. ❪G,L❫ ⊢ T ⁝ A → ❪G,L❫ ⊢ ⬈*𝐒[h] T. #h #G #L #T #A #H @(gcr_aaa … (csx_gcp h) (csx_gcr h) … H) qed. (* Advanced eliminators *****************************************************) -fact aaa_ind_csx_aux: ∀h,G,L,A. ∀Q:predicate term. - (∀T1. ❪G,L❫ ⊢ T1 ⁝ A → - (∀T2. ❪G,L❫ ⊢ T1 ⬈[h] T2 → (T1 ≛ T2 → ⊥) → Q T2) → Q T1 - ) → - ∀T. ❪G,L❫ ⊢ ⬈*[h] 𝐒❪T❫ → ❪G,L❫ ⊢ T ⁝ A → Q T. +fact aaa_ind_csx_aux (h) (G) (L): + ∀A. ∀Q:predicate term. + (∀T1. ❪G,L❫ ⊢ T1 ⁝ A → + (∀T2. ❪G,L❫ ⊢ T1 ⬈[h] T2 → (T1 ≛ T2 → ⊥) → Q T2) → Q T1 + ) → + ∀T. ❪G,L❫ ⊢ ⬈*𝐒[h] T → ❪G,L❫ ⊢ T ⁝ A → Q T. #h #G #L #A #Q #IH #T #H @(csx_ind … H) -T /4 width=5 by cpx_aaa_conf/ qed-. -lemma aaa_ind_csx: ∀h,G,L,A. ∀Q:predicate term. - (∀T1. ❪G,L❫ ⊢ T1 ⁝ A → - (∀T2. ❪G,L❫ ⊢ T1 ⬈[h] T2 → (T1 ≛ T2 → ⊥) → Q T2) → Q T1 - ) → - ∀T. ❪G,L❫ ⊢ T ⁝ A → Q T. +lemma aaa_ind_csx (h) (G) (L): + ∀A. ∀Q:predicate term. + (∀T1. ❪G,L❫ ⊢ T1 ⁝ A → + (∀T2. ❪G,L❫ ⊢ T1 ⬈[h] T2 → (T1 ≛ T2 → ⊥) → Q T2) → Q T1 + ) → + ∀T. ❪G,L❫ ⊢ T ⁝ A → Q T. /5 width=9 by aaa_ind_csx_aux, aaa_csx/ qed-. -fact aaa_ind_csx_cpxs_aux: ∀h,G,L,A. ∀Q:predicate term. - (∀T1. ❪G,L❫ ⊢ T1 ⁝ A → - (∀T2. ❪G,L❫ ⊢ T1 ⬈*[h] T2 → (T1 ≛ T2 → ⊥) → Q T2) → Q T1 - ) → - ∀T. ❪G,L❫ ⊢ ⬈*[h] 𝐒❪T❫ → ❪G,L❫ ⊢ T ⁝ A → Q T. +fact aaa_ind_csx_cpxs_aux (h) (G) (L): + ∀A. ∀Q:predicate term. + (∀T1. ❪G,L❫ ⊢ T1 ⁝ A → + (∀T2. ❪G,L❫ ⊢ T1 ⬈*[h] T2 → (T1 ≛ T2 → ⊥) → Q T2) → Q T1 + ) → + ∀T. ❪G,L❫ ⊢ ⬈*𝐒[h] T → ❪G,L❫ ⊢ T ⁝ A → Q T. #h #G #L #A #Q #IH #T #H @(csx_ind_cpxs … H) -T /4 width=5 by cpxs_aaa_conf/ qed-. (* Basic_2A1: was: aaa_ind_csx_alt *) -lemma aaa_ind_csx_cpxs: ∀h,G,L,A. ∀Q:predicate term. - (∀T1. ❪G,L❫ ⊢ T1 ⁝ A → - (∀T2. ❪G,L❫ ⊢ T1 ⬈*[h] T2 → (T1 ≛ T2 → ⊥) → Q T2) → Q T1 - ) → - ∀T. ❪G,L❫ ⊢ T ⁝ A → Q T. +lemma aaa_ind_csx_cpxs (h) (G) (L): + ∀A. ∀Q:predicate term. + (∀T1. ❪G,L❫ ⊢ T1 ⁝ A → + (∀T2. ❪G,L❫ ⊢ T1 ⬈*[h] T2 → (T1 ≛ T2 → ⊥) → Q T2) → Q T1 + ) → + ∀T. ❪G,L❫ ⊢ T ⁝ A → Q T. /5 width=9 by aaa_ind_csx_cpxs_aux, aaa_csx/ qed-. 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 8cfec456c..feee761c6 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 @@ -20,10 +20,12 @@ include "basic_2/rt_computation/csx.ma". (* Properties with normal terms for unbound parallel rt-transition **********) (* Basic_1: was just: sn3_nf2 *) -lemma cnx_csx: ∀h,G,L,T. ❪G,L❫ ⊢ ⬈[h] 𝐍❪T❫ → ❪G,L❫ ⊢ ⬈*[h] 𝐒❪T❫. +lemma cnx_csx (h) (G) (L): + ∀T. ❪G,L❫ ⊢ ⬈𝐍[h] T → ❪G,L❫ ⊢ ⬈*𝐒[h] T. /2 width=1 by NF_to_SN/ qed. (* Advanced properties ******************************************************) -lemma csx_sort: ∀h,G,L,s. ❪G,L❫ ⊢ ⬈*[h] 𝐒❪⋆s❫. +lemma csx_sort (h) (G) (L): + ∀s. ❪G,L❫ ⊢ ⬈*𝐒[h] ⋆s. /3 width=4 by cnx_csx, cnx_sort/ qed. 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 1e33d469c..a1f659355 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 @@ -24,8 +24,8 @@ include "basic_2/rt_computation/csx_vector.ma". (* Basic_1: was just: sn3_appls_lref *) lemma csx_applv_cnx (h) (G) (L): - ∀T. 𝐒❪T❫ → ❪G,L❫ ⊢ ⬈[h] 𝐍❪T❫ → - ∀Vs. ❪G,L❫ ⊢ ⬈*[h] 𝐒❪Vs❫ → ❪G,L❫ ⊢ ⬈*[h] 𝐒❪ⒶVs.T❫. + ∀T. 𝐒❪T❫ → ❪G,L❫ ⊢ ⬈𝐍[h] T → + ∀Vs. ❪G,L❫ ⊢ ⬈*𝐒[h] Vs → ❪G,L❫ ⊢ ⬈*𝐒[h] ⒶVs.T. #h #G #L #T #H1T #H2T #Vs elim Vs -Vs [ #_ normalize in ⊢ (????%); /2 width=1 by cnx_csx/ | #V #Vs #IHV #H @@ -41,5 +41,5 @@ qed. (* Note: strong normalization does not depend on this any more *) lemma csx_applv_sort (h) (G) (L): - ∀s,Vs. ❪G,L❫ ⊢ ⬈*[h] 𝐒❪Vs❫ → ❪G,L❫ ⊢ ⬈*[h] 𝐒❪ⒶVs.⋆s❫. + ∀s,Vs. ❪G,L❫ ⊢ ⬈*𝐒[h] Vs → ❪G,L❫ ⊢ ⬈*𝐒[h] ⒶVs.⋆s. /3 width=6 by csx_applv_cnx, cnx_sort, simple_atom/ qed. 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 9ed4a0b59..1fecc55e4 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 @@ -21,26 +21,28 @@ include "basic_2/rt_computation/csx_csx.ma". (* Properties with unbound context-sensitive rt-computation for terms *******) (* Basic_1: was just: sn3_intro *) -lemma csx_intro_cpxs: ∀h,G,L,T1. - (∀T2. ❪G,L❫ ⊢ T1 ⬈*[h] T2 → (T1 ≛ T2 → ⊥) → ❪G,L❫ ⊢ ⬈*[h] 𝐒❪T2❫) → - ❪G,L❫ ⊢ ⬈*[h] 𝐒❪T1❫. +lemma csx_intro_cpxs (h) (G) (L): + ∀T1. (∀T2. ❪G,L❫ ⊢ T1 ⬈*[h] T2 → (T1 ≛ T2 → ⊥) → ❪G,L❫ ⊢ ⬈*𝐒[h] T2) → + ❪G,L❫ ⊢ ⬈*𝐒[h] T1. /4 width=1 by cpx_cpxs, csx_intro/ qed-. (* Basic_1: was just: sn3_pr3_trans *) -lemma csx_cpxs_trans: ∀h,G,L,T1. ❪G,L❫ ⊢ ⬈*[h] 𝐒❪T1❫ → - ∀T2. ❪G,L❫ ⊢ T1 ⬈*[h] T2 → ❪G,L❫ ⊢ ⬈*[h] 𝐒❪T2❫. +lemma csx_cpxs_trans (h) (G) (L): + ∀T1. ❪G,L❫ ⊢ ⬈*𝐒[h] T1 → + ∀T2. ❪G,L❫ ⊢ T1 ⬈*[h] T2 → ❪G,L❫ ⊢ ⬈*𝐒[h] T2. #h #G #L #T1 #HT1 #T2 #H @(cpxs_ind … H) -T2 /2 width=3 by csx_cpx_trans/ qed-. (* Eliminators with unbound context-sensitive rt-computation for terms ******) -lemma csx_ind_cpxs_teqx: ∀h,G,L. ∀Q:predicate term. - (∀T1. ❪G,L❫ ⊢ ⬈*[h] 𝐒❪T1❫ → - (∀T2. ❪G,L❫ ⊢ T1 ⬈*[h] T2 → (T1 ≛ T2 → ⊥) → Q T2) → Q T1 - ) → - ∀T1. ❪G,L❫ ⊢ ⬈*[h] 𝐒❪T1❫ → - ∀T0. ❪G,L❫ ⊢ T1 ⬈*[h] T0 → ∀T2. T0 ≛ T2 → Q T2. +lemma csx_ind_cpxs_teqx (h) (G) (L): + ∀Q:predicate term. + (∀T1. ❪G,L❫ ⊢ ⬈*𝐒[h] T1 → + (∀T2. ❪G,L❫ ⊢ T1 ⬈*[h] T2 → (T1 ≛ T2 → ⊥) → Q T2) → Q T1 + ) → + ∀T1. ❪G,L❫ ⊢ ⬈*𝐒[h] T1 → + ∀T0. ❪G,L❫ ⊢ T1 ⬈*[h] T0 → ∀T2. T0 ≛ T2 → Q T2. #h #G #L #Q #IH #T1 #H @(csx_ind … H) -T1 #T1 #HT1 #IH1 #T0 #HT10 #T2 #HT02 @IH -IH /3 width=3 by csx_cpxs_trans, csx_teqx_trans/ -HT1 #V2 #HTV2 #HnTV2 @@ -59,11 +61,11 @@ elim (teqx_dec T1 T0) #H qed-. (* Basic_2A1: was: csx_ind_alt *) -lemma csx_ind_cpxs: ∀h,G,L. ∀Q:predicate term. - (∀T1. ❪G,L❫ ⊢ ⬈*[h] 𝐒❪T1❫ → - (∀T2. ❪G,L❫ ⊢ T1 ⬈*[h] T2 → (T1 ≛ T2 → ⊥) → Q T2) → Q T1 - ) → - ∀T. ❪G,L❫ ⊢ ⬈*[h] 𝐒❪T❫ → Q T. +lemma csx_ind_cpxs (h) (G) (L) (Q:predicate …): + (∀T1. ❪G,L❫ ⊢ ⬈*𝐒[h] T1 → + (∀T2. ❪G,L❫ ⊢ T1 ⬈*[h] T2 → (T1 ≛ T2 → ⊥) → Q T2) → Q T1 + ) → + ∀T. ❪G,L❫ ⊢ ⬈*𝐒[h] T → Q T. #h #G #L #Q #IH #T #HT @(csx_ind_cpxs_teqx … IH … HT) -IH -HT // (**) (* full auto fails *) qed-. 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 6948d70bb..4a89de6b3 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 @@ -19,25 +19,25 @@ include "basic_2/rt_computation/csx_drops.ma". (* Advanced properties ******************************************************) -lemma csx_teqx_trans (h) (G): - ∀L,T1. ❪G,L❫ ⊢ ⬈*[h] 𝐒❪T1❫ → - ∀T2. T1 ≛ T2 → ❪G,L❫ ⊢ ⬈*[h] 𝐒❪T2❫. +lemma csx_teqx_trans (h) (G) (L): + ∀T1. ❪G,L❫ ⊢ ⬈*𝐒[h] T1 → + ∀T2. T1 ≛ T2 → ❪G,L❫ ⊢ ⬈*𝐒[h] T2. #h #G #L #T1 #H @(csx_ind … H) -T1 #T #_ #IH #T2 #HT2 @csx_intro #T1 #HT21 #HnT21 elim (teqx_cpx_trans … HT2 … HT21) -HT21 /4 width=5 by teqx_repl/ qed-. -lemma csx_cpx_trans (h) (G): - ∀L,T1. ❪G,L❫ ⊢ ⬈*[h] 𝐒❪T1❫ → - ∀T2. ❪G,L❫ ⊢ T1 ⬈[h] T2 → ❪G,L❫ ⊢ ⬈*[h] 𝐒❪T2❫. +lemma csx_cpx_trans (h) (G) (L): + ∀T1. ❪G,L❫ ⊢ ⬈*𝐒[h] T1 → + ∀T2. ❪G,L❫ ⊢ T1 ⬈[h] T2 → ❪G,L❫ ⊢ ⬈*𝐒[h] T2. #h #G #L #T1 #H @(csx_ind … H) -T1 #T1 #HT1 #IHT1 #T2 #HLT12 elim (teqx_dec T1 T2) /3 width=4 by csx_teqx_trans/ qed-. (* Basic_1: was just: sn3_cast *) -lemma csx_cast (h) (G): - ∀L,W. ❪G,L❫ ⊢ ⬈*[h] 𝐒❪W❫ → - ∀T. ❪G,L❫ ⊢ ⬈*[h] 𝐒❪T❫ → ❪G,L❫ ⊢ ⬈*[h] 𝐒❪ⓝW.T❫. +lemma csx_cast (h) (G) (L): + ∀W. ❪G,L❫ ⊢ ⬈*𝐒[h] W → + ∀T. ❪G,L❫ ⊢ ⬈*𝐒[h] T → ❪G,L❫ ⊢ ⬈*𝐒[h] ⓝW.T. #h #G #L #W #HW @(csx_ind … HW) -W #W #HW #IHW #T #HT @(csx_ind … HT) -T #T #HT #IHT @csx_intro @@ -54,10 +54,10 @@ qed. (* Basic_1: was just: sn3_abbr *) (* Basic_2A1: was: csx_lref_bind *) -lemma csx_lref_pair_drops (h) (G): - ∀I,L,K,V,i. ⇩[i] L ≘ K.ⓑ[I]V → - ❪G,K❫ ⊢ ⬈*[h] 𝐒❪V❫ → ❪G,L❫ ⊢ ⬈*[h] 𝐒❪#i❫. -#h #G #I #L #K #V #i #HLK #HV +lemma csx_lref_pair_drops (h) (G) (L): + ∀I,K,V,i. ⇩[i] L ≘ K.ⓑ[I]V → + ❪G,K❫ ⊢ ⬈*𝐒[h] V → ❪G,L❫ ⊢ ⬈*𝐒[h] #i. +#h #G #L #I #K #V #i #HLK #HV @csx_intro #X #H #Hi elim (cpx_inv_lref1_drops … H) -H [ #H destruct elim Hi // | -Hi * #I0 #K0 #V0 #V1 #HLK0 #HV01 #HV1 @@ -70,19 +70,19 @@ qed. (* Basic_1: was: sn3_gen_def *) (* Basic_2A1: was: csx_inv_lref_bind *) -lemma csx_inv_lref_pair_drops (h) (G): - ∀I,L,K,V,i. ⇩[i] L ≘ K.ⓑ[I]V → - ❪G,L❫ ⊢ ⬈*[h] 𝐒❪#i❫ → ❪G,K❫ ⊢ ⬈*[h] 𝐒❪V❫. -#h #G #I #L #K #V #i #HLK #Hi +lemma csx_inv_lref_pair_drops (h) (G) (L): + ∀I,K,V,i. ⇩[i] L ≘ K.ⓑ[I]V → + ❪G,L❫ ⊢ ⬈*𝐒[h] #i → ❪G,K❫ ⊢ ⬈*𝐒[h] V. +#h #G #L #I #K #V #i #HLK #Hi elim (lifts_total V (𝐔❨↑i❩)) /4 width=9 by csx_inv_lifts, csx_cpx_trans, cpx_delta_drops, drops_isuni_fwd_drop2/ qed-. -lemma csx_inv_lref_drops (h) (G): - ∀L,i. ❪G,L❫ ⊢ ⬈*[h] 𝐒❪#i❫ → +lemma csx_inv_lref_drops (h) (G) (L): + ∀i. ❪G,L❫ ⊢ ⬈*𝐒[h] #i → ∨∨ ⇩*[Ⓕ,𝐔❨i❩] L ≘ ⋆ | ∃∃I,K. ⇩[i] L ≘ K.ⓤ[I] - | ∃∃I,K,V. ⇩[i] L ≘ K.ⓑ[I]V & ❪G,K❫ ⊢ ⬈*[h] 𝐒❪V❫. + | ∃∃I,K,V. ⇩[i] L ≘ K.ⓑ[I]V & ❪G,K❫ ⊢ ⬈*𝐒[h] V. #h #G #L #i #H elim (drops_F_uni L i) /2 width=1 by or3_intro0/ * * /4 width=9 by csx_inv_lref_pair_drops, ex2_3_intro, ex1_2_intro, or3_intro2, or3_intro1/ qed-. 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 2aa49c5bd..39779d75a 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 @@ -23,10 +23,10 @@ include "basic_2/rt_computation/csx_vector.ma". (* Advanced properties ************************************* ****************) (* Basic_1: was just: sn3_appls_beta *) -lemma csx_applv_beta (h) (G): - ∀p,L,Vs,V,W,T. ❪G,L❫ ⊢ ⬈*[h] 𝐒❪ⒶVs.ⓓ[p]ⓝW.V.T❫ → - ❪G,L❫ ⊢ ⬈*[h] 𝐒❪ⒶVs.ⓐV.ⓛ[p]W.T❫. -#h #G #p #L #Vs elim Vs -Vs /2 width=1 by csx_appl_beta/ +lemma csx_applv_beta (h) (G) (L): + ∀p,Vs,V,W,T. ❪G,L❫ ⊢ ⬈*𝐒[h] ⒶVs.ⓓ[p]ⓝW.V.T → + ❪G,L❫ ⊢ ⬈*𝐒[h] ⒶVs.ⓐV.ⓛ[p]W.T. +#h #G #L #p #Vs elim Vs -Vs /2 width=1 by csx_appl_beta/ #V0 #Vs #IHV #V #W #T #H1T lapply (csx_fwd_pair_sn … H1T) #HV0 lapply (csx_fwd_flat_dx … H1T) #H2T @@ -38,11 +38,11 @@ elim (cpxs_fwd_beta_vector … H) -H #H ] qed. -lemma csx_applv_delta_drops (h) (G): - ∀I,L,K,V1,i. ⇩[i] L ≘ K.ⓑ[I]V1 → +lemma csx_applv_delta_drops (h) (G) (L): + ∀I,K,V1,i. ⇩[i] L ≘ K.ⓑ[I]V1 → ∀V2. ⇧[↑i] V1 ≘ V2 → - ∀Vs. ❪G,L❫ ⊢ ⬈*[h] 𝐒❪ⒶVs.V2❫ → ❪G,L❫ ⊢ ⬈*[h] 𝐒❪ⒶVs.#i❫. -#h #G #I #L #K #V1 #i #HLK #V2 #HV12 #Vs elim Vs -Vs + ∀Vs. ❪G,L❫ ⊢ ⬈*𝐒[h] ⒶVs.V2 → ❪G,L❫ ⊢ ⬈*𝐒[h] ⒶVs.#i. +#h #G #L #I #K #V1 #i #HLK #V2 #HV12 #Vs elim Vs -Vs [ /4 width=11 by csx_inv_lifts, csx_lref_pair_drops, drops_isuni_fwd_drop2/ | #V #Vs #IHV #H1T lapply (csx_fwd_pair_sn … H1T) #HV @@ -57,10 +57,10 @@ lemma csx_applv_delta_drops (h) (G): qed. (* Basic_1: was just: sn3_appls_abbr *) -lemma csx_applv_theta (h) (G): - ∀p,L,V1b,V2b. ⇧[1] V1b ≘ V2b → - ∀V,T. ❪G,L❫ ⊢ ⬈*[h] 𝐒❪ⓓ[p]V.ⒶV2b.T❫ → ❪G,L❫ ⊢ ⬈*[h] 𝐒❪ⒶV1b.ⓓ[p]V.T❫. -#h #G #p #L #V1b #V2b * -V1b -V2b /2 width=1 by/ +lemma csx_applv_theta (h) (G) (L): + ∀p,V1b,V2b. ⇧[1] V1b ≘ V2b → + ∀V,T. ❪G,L❫ ⊢ ⬈*𝐒[h] ⓓ[p]V.ⒶV2b.T → ❪G,L❫ ⊢ ⬈*𝐒[h] ⒶV1b.ⓓ[p]V.T. +#h #G #L #p #V1b #V2b * -V1b -V2b /2 width=1 by/ #V1b #V2b #V1 #V2 #HV12 #H generalize in match HV12; -HV12 generalize in match V2; -V2 generalize in match V1; -V1 elim H -V1b -V2b /2 width=3 by csx_appl_theta/ @@ -76,9 +76,9 @@ elim (cpxs_fwd_theta_vector … (V2⨮V2b) … H1) -H1 /2 width=1 by liftsv_cons qed. (* Basic_1: was just: sn3_appls_cast *) -lemma csx_applv_cast (h) (G): - ∀L,Vs,U. ❪G,L❫ ⊢ ⬈*[h] 𝐒❪ⒶVs.U❫ → - ∀T. ❪G,L❫ ⊢ ⬈*[h] 𝐒❪ⒶVs.T❫ → ❪G,L❫ ⊢ ⬈*[h] 𝐒❪ⒶVs.ⓝU.T❫. +lemma csx_applv_cast (h) (G) (L): + ∀Vs,U. ❪G,L❫ ⊢ ⬈*𝐒[h] ⒶVs.U → + ∀T. ❪G,L❫ ⊢ ⬈*𝐒[h] ⒶVs.T → ❪G,L❫ ⊢ ⬈*𝐒[h] ⒶVs.ⓝU.T. #h #G #L #Vs elim Vs -Vs /2 width=1 by csx_cast/ #V #Vs #IHV #U #H1U #T #H1T lapply (csx_fwd_pair_sn … H1U) #HV 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 c8b10e80c..c9b3c1ebf 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 @@ -22,7 +22,8 @@ include "basic_2/rt_computation/csx.ma". (* Basic_1: was just: sn3_lift *) (* Basic_2A1: was just: csx_lift *) -lemma csx_lifts: ∀h,G. d_liftable1 … (csx h G). +lemma csx_lifts (h) (G): + d_liftable1 … (csx h G). #h #G #K #T #H @(csx_ind … H) -T #T1 #_ #IH #b #f #L #HLK #U1 #HTU1 @csx_intro #U2 #HU12 #HnU12 @@ -34,7 +35,8 @@ qed-. (* Basic_1: was just: sn3_gen_lift *) (* Basic_2A1: was just: csx_inv_lift *) -lemma csx_inv_lifts: ∀h,G. d_deliftable1 … (csx h G). +lemma csx_inv_lifts (h) (G): + d_deliftable1 … (csx h G). #h #G #L #U #H @(csx_ind … H) -U #U1 #_ #IH #b #f #K #HLK #T1 #HTU1 @csx_intro #T2 #HT12 #HnT12 diff --git a/matita/matita/contribs/lambdadelta/basic_2/rt_computation/csx_feqx.ma b/matita/matita/contribs/lambdadelta/basic_2/rt_computation/csx_feqx.ma index 7cf01b28d..5c8c2c00c 100644 --- a/matita/matita/contribs/lambdadelta/basic_2/rt_computation/csx_feqx.ma +++ b/matita/matita/contribs/lambdadelta/basic_2/rt_computation/csx_feqx.ma @@ -19,8 +19,9 @@ include "basic_2/rt_computation/csx_reqx.ma". (* Properties with sort-irrelevant equivalence for closures *****************) -lemma csx_feqx_conf: ∀h,G1,L1,T1. ❪G1,L1❫ ⊢ ⬈*[h] 𝐒❪T1❫ → - ∀G2,L2,T2. ❪G1,L1,T1❫ ≛ ❪G2,L2,T2❫ → ❪G2,L2❫ ⊢ ⬈*[h] 𝐒❪T2❫. +lemma csx_feqx_conf (h): + ∀G1,L1,T1. ❪G1,L1❫ ⊢ ⬈*𝐒[h] T1 → + ∀G2,L2,T2. ❪G1,L1,T1❫ ≛ ❪G2,L2,T2❫ → ❪G2,L2❫ ⊢ ⬈*𝐒[h] T2. #h #G1 #L1 #T1 #HT1 #G2 #L2 #T2 * -G2 -L2 -T2 /3 width=3 by csx_reqx_conf, csx_teqx_trans/ qed-. 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 f16edc6cd..da10c5143 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 @@ -22,8 +22,9 @@ include "basic_2/rt_computation/csx_lpx.ma". (* Properties with parallel rst-transition for closures *********************) (* Basic_2A1: was: csx_fpb_conf *) -lemma csx_fpbq_conf: ∀h,G1,L1,T1. ❪G1,L1❫ ⊢ ⬈*[h] 𝐒❪T1❫ → - ∀G2,L2,T2. ❪G1,L1,T1❫ ≽[h] ❪G2,L2,T2❫ → ❪G2,L2❫ ⊢ ⬈*[h] 𝐒❪T2❫. +lemma csx_fpbq_conf (h): + ∀G1,L1,T1. ❪G1,L1❫ ⊢ ⬈*𝐒[h] T1 → + ∀G2,L2,T2. ❪G1,L1,T1❫ ≽[h] ❪G2,L2,T2❫ → ❪G2,L2❫ ⊢ ⬈*𝐒[h] T2. #h #G1 #L1 #T1 #HT1 #G2 #L2 #T2 * /2 width=6 by csx_cpx_trans, csx_fquq_conf, csx_lpx_conf, csx_feqx_conf/ qed-. 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 92c26c44c..811435f34 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 @@ -21,7 +21,7 @@ include "basic_2/rt_computation/csx_lsubr.ma". lemma csx_fqu_conf (h) (b): ∀G1,G2,L1,L2,T1,T2. ❪G1,L1,T1❫ ⬂[b] ❪G2,L2,T2❫ → - ❪G1,L1❫ ⊢ ⬈*[h] 𝐒❪T1❫ → ❪G2,L2❫ ⊢ ⬈*[h] 𝐒❪T2❫. + ❪G1,L1❫ ⊢ ⬈*𝐒[h] T1 → ❪G2,L2❫ ⊢ ⬈*𝐒[h] T2. #h #b #G1 #G2 #L1 #L2 #T1 #T2 #H elim H -G1 -G2 -L1 -L2 -T1 -T2 [ /3 width=5 by csx_inv_lref_pair_drops, drops_refl/ | /2 width=3 by csx_fwd_pair_sn/ @@ -34,21 +34,21 @@ qed-. lemma csx_fquq_conf (h) (b): ∀G1,G2,L1,L2,T1,T2. ❪G1,L1,T1❫ ⬂⸮[b] ❪G2,L2,T2❫ → - ❪G1,L1❫ ⊢ ⬈*[h] 𝐒❪T1❫ → ❪G2,L2❫ ⊢ ⬈*[h] 𝐒❪T2❫. + ❪G1,L1❫ ⊢ ⬈*𝐒[h] T1 → ❪G2,L2❫ ⊢ ⬈*𝐒[h] T2. #h #b #G1 #G2 #L1 #L2 #T1 #T2 * /2 width=6 by csx_fqu_conf/ * #HG #HL #HT destruct // qed-. lemma csx_fqup_conf (h) (b): ∀G1,G2,L1,L2,T1,T2. ❪G1,L1,T1❫ ⬂+[b] ❪G2,L2,T2❫ → - ❪G1,L1❫ ⊢ ⬈*[h] 𝐒❪T1❫ → ❪G2,L2❫ ⊢ ⬈*[h] 𝐒❪T2❫. + ❪G1,L1❫ ⊢ ⬈*𝐒[h] T1 → ❪G2,L2❫ ⊢ ⬈*𝐒[h] T2. #h #b #G1 #G2 #L1 #L2 #T1 #T2 #H @(fqup_ind … H) -G2 -L2 -T2 /3 width=6 by csx_fqu_conf/ qed-. lemma csx_fqus_conf (h) (b): ∀G1,G2,L1,L2,T1,T2. ❪G1,L1,T1❫ ⬂*[b] ❪G2,L2,T2❫ → - ❪G1,L1❫ ⊢ ⬈*[h] 𝐒❪T1❫ → ❪G2,L2❫ ⊢ ⬈*[h] 𝐒❪T2❫. + ❪G1,L1❫ ⊢ ⬈*𝐒[h] T1 → ❪G2,L2❫ ⊢ ⬈*𝐒[h] T2. #h #b #G1 #G2 #L1 #L2 #T1 #T2 #H @(fqus_ind … H) -H /3 width=6 by csx_fquq_conf/ qed-. 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 aff46798d..e042402ea 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 @@ -20,7 +20,8 @@ include "basic_2/rt_computation/csx_drops.ma". (* Main properties with generic computation properties **********************) -theorem csx_gcp: ∀h. gcp (cpx h) teqx (csx h). +theorem csx_gcp (h): + gcp (cpx h) teqx (csx h). #h @mk_gcp [ normalize /3 width=13 by cnx_lifts/ | /2 width=4 by cnx_sort/ 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 77a8bcabd..24ce3517d 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 @@ -20,7 +20,8 @@ include "basic_2/rt_computation/csx_csx_vector.ma". (* Main properties with generic candidates of reducibility ******************) -theorem csx_gcr (h): gcr (cpx h) teqx (csx h) (csx h). +theorem csx_gcr (h): + gcr (cpx h) teqx (csx h) (csx h). #h @mk_gcr [ // | #G #L #Vs #Hvs #T #HT #H diff --git a/matita/matita/contribs/lambdadelta/basic_2/rt_computation/csx_lpx.ma b/matita/matita/contribs/lambdadelta/basic_2/rt_computation/csx_lpx.ma index df0dc9948..04b75e3ea 100644 --- a/matita/matita/contribs/lambdadelta/basic_2/rt_computation/csx_lpx.ma +++ b/matita/matita/contribs/lambdadelta/basic_2/rt_computation/csx_lpx.ma @@ -19,19 +19,19 @@ include "basic_2/rt_computation/csx_cpxs.ma". (* Properties with unbound parallel rt-transition on all entries ************) -lemma csx_lpx_conf (h) (G): - ∀L1,T. ❪G,L1❫ ⊢ ⬈*[h] 𝐒❪T❫ → - ∀L2. ❪G,L1❫ ⊢ ⬈[h] L2 → ❪G,L2❫ ⊢ ⬈*[h] 𝐒❪T❫. +lemma csx_lpx_conf (h) (G) (L1): + ∀T. ❪G,L1❫ ⊢ ⬈*𝐒[h] T → + ∀L2. ❪G,L1❫ ⊢ ⬈[h] L2 → ❪G,L2❫ ⊢ ⬈*𝐒[h] T. #h #G #L1 #T #H @(csx_ind_cpxs … H) -T /4 width=3 by csx_intro, lpx_cpx_trans/ qed-. (* Advanced properties ******************************************************) -lemma csx_abst (h) (G): - ∀p,L,W. ❪G,L❫ ⊢ ⬈*[h] 𝐒❪W❫ → - ∀T. ❪G,L.ⓛW❫ ⊢ ⬈*[h] 𝐒❪T❫ → ❪G,L❫ ⊢ ⬈*[h] 𝐒❪ⓛ[p]W.T❫. -#h #G #p #L #W #HW +lemma csx_abst (h) (G) (L): + ∀p,W. ❪G,L❫ ⊢ ⬈*𝐒[h] W → + ∀T. ❪G,L.ⓛW❫ ⊢ ⬈*𝐒[h] T → ❪G,L❫ ⊢ ⬈*𝐒[h] ⓛ[p]W.T. +#h #G #L #p #W #HW @(csx_ind … HW) -W #W #_ #IHW #T #HT @(csx_ind … HT) -T #T #HT #IHT @csx_intro #X #H1 #H2 @@ -44,10 +44,10 @@ elim (tneqx_inv_pair … H2) -H2 ] qed. -lemma csx_abbr (h) (G): - ∀p,L,V. ❪G,L❫ ⊢ ⬈*[h] 𝐒❪V❫ → - ∀T. ❪G,L.ⓓV❫ ⊢ ⬈*[h] 𝐒❪T❫ → ❪G,L❫ ⊢ ⬈*[h] 𝐒❪ⓓ[p]V.T❫. -#h #G #p #L #V #HV +lemma csx_abbr (h) (G) (L): + ∀p,V. ❪G,L❫ ⊢ ⬈*𝐒[h] V → + ∀T. ❪G,L.ⓓV❫ ⊢ ⬈*𝐒[h] T → ❪G,L❫ ⊢ ⬈*𝐒[h] ⓓ[p]V.T. +#h #G #L #p #V #HV @(csx_ind … HV) -V #V #_ #IHV #T #HT @(csx_ind_cpxs … HT) -T #T #HT #IHT @csx_intro #X #H1 #H2 @@ -63,17 +63,17 @@ elim (cpx_inv_abbr1 … H1) -H1 * ] qed. -lemma csx_bind (h) (G): - ∀p,I,L,V. ❪G,L❫ ⊢ ⬈*[h] 𝐒❪V❫ → - ∀T. ❪G,L.ⓑ[I]V❫ ⊢ ⬈*[h] 𝐒❪T❫ → ❪G,L❫ ⊢ ⬈*[h] 𝐒❪ⓑ[p,I]V.T❫. -#h #G #p * #L #V #HV #T #HT +lemma csx_bind (h) (G) (L): + ∀p,I,V. ❪G,L❫ ⊢ ⬈*𝐒[h] V → + ∀T. ❪G,L.ⓑ[I]V❫ ⊢ ⬈*𝐒[h] T → ❪G,L❫ ⊢ ⬈*𝐒[h] ⓑ[p,I]V.T. +#h #G #L #p * #V #HV #T #HT /2 width=1 by csx_abbr, csx_abst/ qed. -fact csx_appl_theta_aux (h) (G): - ∀p,L,U. ❪G,L❫ ⊢ ⬈*[h] 𝐒❪U❫ → ∀V1,V2. ⇧[1] V1 ≘ V2 → - ∀V,T. U = ⓓ[p]V.ⓐV2.T → ❪G,L❫ ⊢ ⬈*[h] 𝐒❪ⓐV1.ⓓ[p]V.T❫. -#h #G #p #L #X #H +fact csx_appl_theta_aux (h) (G) (L): + ∀p,U. ❪G,L❫ ⊢ ⬈*𝐒[h] U → ∀V1,V2. ⇧[1] V1 ≘ V2 → + ∀V,T. U = ⓓ[p]V.ⓐV2.T → ❪G,L❫ ⊢ ⬈*𝐒[h] ⓐV1.ⓓ[p]V.T. +#h #G #L #p #X #H @(csx_ind_cpxs … H) -X #X #HVT #IHVT #V1 #V2 #HV12 #V #T #H destruct lapply (csx_fwd_pair_sn … HVT) #HV lapply (csx_fwd_bind_dx … HVT) -HVT #HVT @@ -105,7 +105,7 @@ elim (cpx_inv_appl1 … HL) -HL * ] qed-. -lemma csx_appl_theta (h) (G): - ∀p,L,V,V2,T. ❪G,L❫ ⊢ ⬈*[h] 𝐒❪ⓓ[p]V.ⓐV2.T❫ → - ∀V1. ⇧[1] V1 ≘ V2 → ❪G,L❫ ⊢ ⬈*[h] 𝐒❪ⓐV1.ⓓ[p]V.T❫. +lemma csx_appl_theta (h) (G) (L): + ∀p,V,V2,T. ❪G,L❫ ⊢ ⬈*𝐒[h] ⓓ[p]V.ⓐV2.T → + ∀V1. ⇧[1] V1 ≘ V2 → ❪G,L❫ ⊢ ⬈*𝐒[h] ⓐV1.ⓓ[p]V.T. /2 width=5 by csx_appl_theta_aux/ qed. diff --git a/matita/matita/contribs/lambdadelta/basic_2/rt_computation/csx_lpxs.ma b/matita/matita/contribs/lambdadelta/basic_2/rt_computation/csx_lpxs.ma index 1629eddcd..a8a930a31 100644 --- a/matita/matita/contribs/lambdadelta/basic_2/rt_computation/csx_lpxs.ma +++ b/matita/matita/contribs/lambdadelta/basic_2/rt_computation/csx_lpxs.ma @@ -19,8 +19,8 @@ include "basic_2/rt_computation/lpxs_lpx.ma". (* Properties with unbound parallel rt-computation on all entries ***********) -lemma csx_lpxs_conf: ∀h,G,L1,L2,T. ❪G,L1❫ ⊢ ⬈*[h] L2 → - ❪G,L1❫ ⊢ ⬈*[h] 𝐒❪T❫ → ❪G,L2❫ ⊢ ⬈*[h] 𝐒❪T❫. +lemma csx_lpxs_conf (h) (G) (L1): + ∀L2,T. ❪G,L1❫ ⊢ ⬈*[h] L2 → ❪G,L1❫ ⊢ ⬈*𝐒[h] T → ❪G,L2❫ ⊢ ⬈*𝐒[h] T. #h #G #L1 #L2 #T #H @(lpxs_ind_dx … H) -L2 /3 by lpxs_step_dx, csx_lpx_conf/ qed-. 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 5b180f3da..2be0d7fdb 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 @@ -19,10 +19,10 @@ include "basic_2/rt_computation/csx_csx.ma". (* Advanced properties ******************************************************) -fact csx_appl_beta_aux (h) (G): - ∀p,L,U1. ❪G,L❫ ⊢ ⬈*[h] 𝐒❪U1❫ → - ∀V,W,T1. U1 = ⓓ[p]ⓝW.V.T1 → ❪G,L❫ ⊢ ⬈*[h] 𝐒❪ⓐV.ⓛ[p]W.T1❫. -#h #G #p #L #X #H @(csx_ind … H) -X +fact csx_appl_beta_aux (h) (G) (L): + ∀p,U1. ❪G,L❫ ⊢ ⬈*𝐒[h] U1 → + ∀V,W,T1. U1 = ⓓ[p]ⓝW.V.T1 → ❪G,L❫ ⊢ ⬈*𝐒[h] ⓐV.ⓛ[p]W.T1. +#h #G #L #p #X #H @(csx_ind … H) -X #X #HT1 #IHT1 #V #W #T1 #H1 destruct @csx_intro #X #H1 #H2 elim (cpx_inv_appl1 … H1) -H1 * @@ -43,35 +43,35 @@ elim (cpx_inv_appl1 … H1) -H1 * qed-. (* Basic_1: was just: sn3_beta *) -lemma csx_appl_beta (h) (G): - ∀p,L,V,W,T. ❪G,L❫ ⊢ ⬈*[h] 𝐒❪ⓓ[p]ⓝW.V.T❫ → ❪G,L❫ ⊢ ⬈*[h] 𝐒❪ⓐV.ⓛ[p]W.T❫. +lemma csx_appl_beta (h) (G) (L): + ∀p,V,W,T. ❪G,L❫ ⊢ ⬈*𝐒[h] ⓓ[p]ⓝW.V.T → ❪G,L❫ ⊢ ⬈*𝐒[h] ⓐV.ⓛ[p]W.T. /2 width=3 by csx_appl_beta_aux/ qed. (* Advanced forward lemmas **************************************************) -fact csx_fwd_bind_dx_unit_aux (h) (G): - ∀L,U. ❪G,L❫ ⊢ ⬈*[h] 𝐒❪U❫ → - ∀p,I,J,V,T. U = ⓑ[p,I]V.T → ❪G,L.ⓤ[J]❫ ⊢ ⬈*[h] 𝐒❪T❫. +fact csx_fwd_bind_dx_unit_aux (h) (G) (L): + ∀U. ❪G,L❫ ⊢ ⬈*𝐒[h] U → + ∀p,I,J,V,T. U = ⓑ[p,I]V.T → ❪G,L.ⓤ[J]❫ ⊢ ⬈*𝐒[h] T. #h #G #L #U #H elim H -H #U0 #_ #IH #p #I #J #V #T #H destruct @csx_intro #T2 #HLT2 #HT2 @(IH (ⓑ[p, I]V.T2)) -IH /2 width=4 by cpx_bind_unit/ -HLT2 #H elim (teqx_inv_pair … H) -H /2 width=1 by/ qed-. -lemma csx_fwd_bind_dx_unit (h) (G): - ∀p,I,L,V,T. ❪G,L❫ ⊢ ⬈*[h] 𝐒❪ⓑ[p,I]V.T❫ → - ∀J. ❪G,L.ⓤ[J]❫ ⊢ ⬈*[h] 𝐒❪T❫. +lemma csx_fwd_bind_dx_unit (h) (G) (L): + ∀p,I,V,T. ❪G,L❫ ⊢ ⬈*𝐒[h] ⓑ[p,I]V.T → + ∀J. ❪G,L.ⓤ[J]❫ ⊢ ⬈*𝐒[h] T. /2 width=6 by csx_fwd_bind_dx_unit_aux/ qed-. -lemma csx_fwd_bind_unit (h) (G): - ∀p,I,L,V,T. ❪G,L❫ ⊢ ⬈*[h] 𝐒❪ⓑ[p,I]V.T❫ → - ∀J. ❪G,L❫ ⊢ ⬈*[h] 𝐒❪V❫ ∧ ❪G,L.ⓤ[J]❫ ⊢ ⬈*[h] 𝐒❪T❫. +lemma csx_fwd_bind_unit (h) (G) (L): + ∀p,I,V,T. ❪G,L❫ ⊢ ⬈*𝐒[h] ⓑ[p,I]V.T → + ∀J. ∧∧ ❪G,L❫ ⊢ ⬈*𝐒[h] V & ❪G,L.ⓤ[J]❫ ⊢ ⬈*𝐒[h] T. /3 width=4 by csx_fwd_pair_sn, csx_fwd_bind_dx_unit, conj/ qed-. (* Properties with restricted refinement for local environments *************) -lemma csx_lsubr_conf (h) (G): - ∀L1,T. ❪G,L1❫ ⊢ ⬈*[h] 𝐒❪T❫ → ∀L2. L1 ⫃ L2 → ❪G,L2❫ ⊢ ⬈*[h] 𝐒❪T❫. +lemma csx_lsubr_conf (h) (G) (L1): + ∀T. ❪G,L1❫ ⊢ ⬈*𝐒[h] T → ∀L2. L1 ⫃ L2 → ❪G,L2❫ ⊢ ⬈*𝐒[h] T. #h #G #L1 #T #H @(csx_ind … H) -T #T1 #_ #IH #L2 #HL12 @csx_intro #T2 #HT12 #HnT12 diff --git a/matita/matita/contribs/lambdadelta/basic_2/rt_computation/csx_reqx.ma b/matita/matita/contribs/lambdadelta/basic_2/rt_computation/csx_reqx.ma index a32c9380e..59e5eb289 100644 --- a/matita/matita/contribs/lambdadelta/basic_2/rt_computation/csx_reqx.ma +++ b/matita/matita/contribs/lambdadelta/basic_2/rt_computation/csx_reqx.ma @@ -20,8 +20,9 @@ include "basic_2/rt_computation/csx_csx.ma". (* Properties with sort-irrelevant equivalence for local environments *******) (* Basic_2A1: uses: csx_lleq_conf *) -lemma csx_reqx_conf: ∀h,G,L1,T. ❪G,L1❫ ⊢ ⬈*[h] 𝐒❪T❫ → - ∀L2. L1 ≛[T] L2 → ❪G,L2❫ ⊢ ⬈*[h] 𝐒❪T❫. +lemma csx_reqx_conf (h) (G) (L1): + ∀T. ❪G,L1❫ ⊢ ⬈*𝐒[h] T → + ∀L2. L1 ≛[T] L2 → ❪G,L2❫ ⊢ ⬈*𝐒[h] T. #h #G #L1 #T #H @(csx_ind … H) -T #T1 #_ #IH #L2 #HL12 @csx_intro #T2 #HT12 #HnT12 @@ -29,7 +30,7 @@ elim (reqx_cpx_trans … HL12 … HT12) -HT12 /5 width=5 by cpx_reqx_conf_sn, csx_teqx_trans, teqx_trans/ qed-. -(* Basic_2A1: uses: csx_lleq_conf *) -lemma csx_reqx_trans: ∀h,L1,L2,T. L1 ≛[T] L2 → - ∀G. ❪G,L2❫ ⊢ ⬈*[h] 𝐒❪T❫ → ❪G,L1❫ ⊢ ⬈*[h] 𝐒❪T❫. +(* Basic_2A1: uses: csx_lleq_trans *) +lemma csx_reqx_trans (h) (G) (L2): + ∀L1,T. L1 ≛[T] L2 → ❪G,L2❫ ⊢ ⬈*𝐒[h] T → ❪G,L1❫ ⊢ ⬈*𝐒[h] T. /3 width=3 by csx_reqx_conf, reqx_sym/ qed-. 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 765cc7a3c..1fbc8de21 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 @@ -19,9 +19,10 @@ include "basic_2/rt_computation/csx_csx.ma". (* Properties with simple terms *********************************************) -lemma csx_appl_simple: ∀h,G,L,V. ❪G,L❫ ⊢ ⬈*[h] 𝐒❪V❫ → ∀T1. - (∀T2. ❪G,L❫ ⊢ T1 ⬈[h] T2 → (T1 ≛ T2 → ⊥) → ❪G,L❫ ⊢ ⬈*[h] 𝐒❪ⓐV.T2❫) → - 𝐒❪T1❫ → ❪G,L❫ ⊢ ⬈*[h] 𝐒❪ⓐV.T1❫. +lemma csx_appl_simple (h) (G) (L): + ∀V. ❪G,L❫ ⊢ ⬈*𝐒[h] V → ∀T1. + (∀T2. ❪G,L❫ ⊢ T1 ⬈[h] T2 → (T1 ≛ T2 → ⊥) → ❪G,L❫ ⊢ ⬈*𝐒[h] ⓐV.T2) → + 𝐒❪T1❫ → ❪G,L❫ ⊢ ⬈*𝐒[h] ⓐV.T1. #h #G #L #V #H @(csx_ind … H) -V #V #_ #IHV #T1 #IHT1 #HT1 @csx_intro #X #H1 #H2 diff --git a/matita/matita/contribs/lambdadelta/basic_2/rt_computation/csx_simple_teqo.ma b/matita/matita/contribs/lambdadelta/basic_2/rt_computation/csx_simple_teqo.ma index 52f68f6ff..12815d38e 100644 --- a/matita/matita/contribs/lambdadelta/basic_2/rt_computation/csx_simple_teqo.ma +++ b/matita/matita/contribs/lambdadelta/basic_2/rt_computation/csx_simple_teqo.ma @@ -25,9 +25,9 @@ include "basic_2/rt_computation/csx_csx.ma". (* Basic_1: was just: sn3_appl_appl *) (* Basic_2A1: was: csx_appl_simple_tsts *) lemma csx_appl_simple_teqo (h) (G) (L): - ∀V. ❪G,L❫ ⊢ ⬈*[h] 𝐒❪V❫ → ∀T1. ❪G,L❫ ⊢ ⬈*[h] 𝐒❪T1❫ → - (∀T2. ❪G,L❫ ⊢ T1 ⬈*[h] T2 → (T1 ⩳ T2 → ⊥) → ❪G,L❫ ⊢ ⬈*[h] 𝐒❪ⓐV.T2❫) → - 𝐒❪T1❫ → ❪G,L❫ ⊢ ⬈*[h] 𝐒❪ⓐV.T1❫. + ∀V. ❪G,L❫ ⊢ ⬈*𝐒[h] V → ∀T1. ❪G,L❫ ⊢ ⬈*𝐒[h] T1 → + (∀T2. ❪G,L❫ ⊢ T1 ⬈*[h] T2 → (T1 ⩳ T2 → ⊥) → ❪G,L❫ ⊢ ⬈*𝐒[h] ⓐV.T2) → + 𝐒❪T1❫ → ❪G,L❫ ⊢ ⬈*𝐒[h] ⓐV.T1. #h #G #L #V #H @(csx_ind … H) -V #V #_ #IHV #T1 #H @(csx_ind … H) -T1 #T1 #H1T1 #IHT1 #H2T1 #H3T1 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 d436de774..ab7046fd1 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 @@ -17,8 +17,8 @@ include "basic_2/rt_computation/csx.ma". (* STRONGLY NORMALIZING TERMS VECTORS FOR UNBOUND PARALLEL RT-TRANSITION ****) -definition csxv: ∀h. relation3 genv lenv (list term) ≝ - λh,G,L. all … (csx h G L). +definition csxv (h) (G) (L): predicate (list term) ≝ + all … (csx h G L). interpretation "strong normalization for unbound context-sensitive parallel rt-transition (term vector)" @@ -26,14 +26,16 @@ interpretation (* Basic inversion lemmas ***************************************************) -lemma csxv_inv_cons: ∀h,G,L,T,Ts. ❪G,L❫ ⊢ ⬈*[h] 𝐒❪T⨮Ts❫ → - ❪G,L❫ ⊢ ⬈*[h] 𝐒❪T❫ ∧ ❪G,L❫ ⊢ ⬈*[h] 𝐒❪Ts❫. +lemma csxv_inv_cons (h) (G) (L): + ∀T,Ts. ❪G,L❫ ⊢ ⬈*𝐒[h] T⨮Ts → + ∧∧ ❪G,L❫ ⊢ ⬈*𝐒[h] T & ❪G,L❫ ⊢ ⬈*𝐒[h] Ts. normalize // qed-. (* Basic forward lemmas *****************************************************) -lemma csx_fwd_applv: ∀h,G,L,T,Vs. ❪G,L❫ ⊢ ⬈*[h] 𝐒❪ⒶVs.T❫ → - ❪G,L❫ ⊢ ⬈*[h] 𝐒❪Vs❫ ∧ ❪G,L❫ ⊢ ⬈*[h] 𝐒❪T❫. +lemma csx_fwd_applv (h) (G) (L): + ∀T,Vs. ❪G,L❫ ⊢ ⬈*𝐒[h] ⒶVs.T → + ∧∧ ❪G,L❫ ⊢ ⬈*𝐒[h] Vs & ❪G,L❫ ⊢ ⬈*𝐒[h] T. #h #G #L #T #Vs elim Vs -Vs /2 width=1 by conj/ #V #Vs #IHVs #HVs lapply (csx_fwd_pair_sn … HVs) #HV 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 091369ff4..4a1349f1a 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 @@ -20,8 +20,8 @@ include "basic_2/rt_computation/fpbs.ma". (* Properties with sn for unbound parallel rt-transition for terms **********) (* Basic_2A1: was: csx_fpbs_conf *) -lemma fpbs_csx_conf: ∀h,G1,L1,T1. ❪G1,L1❫ ⊢ ⬈*[h] 𝐒❪T1❫ → - ∀G2,L2,T2. ❪G1,L1,T1❫ ≥[h] ❪G2,L2,T2❫ → ❪G2,L2❫ ⊢ ⬈*[h] 𝐒❪T2❫. +lemma fpbs_csx_conf: ∀h,G1,L1,T1. ❪G1,L1❫ ⊢ ⬈*𝐒[h] T1 → + ∀G2,L2,T2. ❪G1,L1,T1❫ ≥[h] ❪G2,L2,T2❫ → ❪G2,L2❫ ⊢ ⬈*𝐒[h] T2. #h #G1 #L1 #T1 #HT1 #G2 #L2 #T2 #H @(fpbs_ind … H) -G2 -L2 -T2 /2 width=5 by csx_fpbq_conf/ qed-. diff --git a/matita/matita/contribs/lambdadelta/basic_2/rt_computation/fsb.ma b/matita/matita/contribs/lambdadelta/basic_2/rt_computation/fsb.ma index 919b91f61..72c73ae87 100644 --- a/matita/matita/contribs/lambdadelta/basic_2/rt_computation/fsb.ma +++ b/matita/matita/contribs/lambdadelta/basic_2/rt_computation/fsb.ma @@ -19,7 +19,7 @@ include "basic_2/rt_transition/fpb.ma". inductive fsb (h): relation3 genv lenv term ≝ | fsb_intro: ∀G1,L1,T1. ( - ∀G2,L2,T2. ❪G1,L1,T1❫ ≻[h] ❪G2,L2,T2❫ → fsb h G2 L2 T2 + ∀G2,L2,T2. ❪G1,L1,T1❫ ≻[h] ❪G2,L2,T2❫ → fsb h G2 L2 T2 ) → fsb h G1 L1 T1 . @@ -30,13 +30,13 @@ interpretation (* Basic eliminators ********************************************************) (* Note: eliminator with shorter ground hypothesis *) -(* Note: to be named fsb_ind when fsb becomes a definition like csx, lfsx ***) -lemma fsb_ind_alt: ∀h. ∀Q: relation3 …. ( - ∀G1,L1,T1. ≥[h] 𝐒❪G1,L1,T1❫ → ( - ∀G2,L2,T2. ❪G1,L1,T1❫ ≻[h] ❪G2,L2,T2❫ → Q G2 L2 T2 - ) → Q G1 L1 T1 - ) → - ∀G,L,T. ≥[h] 𝐒❪G,L,T❫ → Q G L T. +(* Note: to be named fsb_ind when fsb becomes a definition like csx, rsx ****) +lemma fsb_ind_alt (h) (Q:relation3 …): + (∀G1,L1,T1. ≥𝐒[h] ❪G1,L1,T1❫ → + (∀G2,L2,T2. ❪G1,L1,T1❫ ≻[h] ❪G2,L2,T2❫ → Q G2 L2 T2) → + Q G1 L1 T1 + ) → + ∀G,L,T. ≥𝐒[h] ❪G,L,T❫ → Q G L T. #h #Q #IH #G #L #T #H elim H -G -L -T /4 width=1 by fsb_intro/ qed-. diff --git a/matita/matita/contribs/lambdadelta/basic_2/rt_computation/fsb_aaa.ma b/matita/matita/contribs/lambdadelta/basic_2/rt_computation/fsb_aaa.ma index 756353fb3..a87de3b2b 100644 --- a/matita/matita/contribs/lambdadelta/basic_2/rt_computation/fsb_aaa.ma +++ b/matita/matita/contribs/lambdadelta/basic_2/rt_computation/fsb_aaa.ma @@ -21,47 +21,52 @@ include "basic_2/rt_computation/fsb_csx.ma". (* Main properties with atomic arity assignment for terms *******************) -theorem aaa_fsb: ∀h,G,L,T,A. ❪G,L❫ ⊢ T ⁝ A → ≥[h] 𝐒❪G,L,T❫. +theorem aaa_fsb (h): + ∀G,L,T,A. ❪G,L❫ ⊢ T ⁝ A → ≥𝐒[h] ❪G,L,T❫. /3 width=2 by aaa_csx, csx_fsb/ qed. (* Advanced eliminators with atomic arity assignment for terms **************) -fact aaa_ind_fpb_aux: ∀h. ∀Q:relation3 …. - (∀G1,L1,T1,A. ❪G1,L1❫ ⊢ T1 ⁝ A → - (∀G2,L2,T2. ❪G1,L1,T1❫ ≻[h] ❪G2,L2,T2❫ → Q G2 L2 T2) → - Q G1 L1 T1 - ) → - ∀G,L,T. ❪G,L❫ ⊢ ⬈*[h] 𝐒❪T❫ → ∀A. ❪G,L❫ ⊢ T ⁝ A → Q G L T. +fact aaa_ind_fpb_aux (h) (Q:relation3 …): + (∀G1,L1,T1,A. + ❪G1,L1❫ ⊢ T1 ⁝ A → + (∀G2,L2,T2. ❪G1,L1,T1❫ ≻[h] ❪G2,L2,T2❫ → Q G2 L2 T2) → + Q G1 L1 T1 + ) → + ∀G,L,T. ❪G,L❫ ⊢ ⬈*𝐒[h] T → ∀A. ❪G,L❫ ⊢ T ⁝ A → Q G L T. #h #R #IH #G #L #T #H @(csx_ind_fpb … H) -G -L -T #G1 #L1 #T1 #H1 #IH1 #A1 #HTA1 @IH -IH // #G2 #L2 #T2 #H12 elim (fpbs_aaa_conf … G2 … L2 … T2 … HTA1) -A1 /2 width=2 by fpb_fpbs/ qed-. -lemma aaa_ind_fpb: ∀h. ∀Q:relation3 …. - (∀G1,L1,T1,A. ❪G1,L1❫ ⊢ T1 ⁝ A → - (∀G2,L2,T2. ❪G1,L1,T1❫ ≻[h] ❪G2,L2,T2❫ → Q G2 L2 T2) → - Q G1 L1 T1 - ) → - ∀G,L,T,A. ❪G,L❫ ⊢ T ⁝ A → Q G L T. +lemma aaa_ind_fpb (h) (Q:relation3 …): + (∀G1,L1,T1,A. + ❪G1,L1❫ ⊢ T1 ⁝ A → + (∀G2,L2,T2. ❪G1,L1,T1❫ ≻[h] ❪G2,L2,T2❫ → Q G2 L2 T2) → + Q G1 L1 T1 + ) → + ∀G,L,T,A. ❪G,L❫ ⊢ T ⁝ A → Q G L T. /4 width=4 by aaa_ind_fpb_aux, aaa_csx/ qed-. -fact aaa_ind_fpbg_aux: ∀h. ∀Q:relation3 …. - (∀G1,L1,T1,A. ❪G1,L1❫ ⊢ T1 ⁝ A → - (∀G2,L2,T2. ❪G1,L1,T1❫ >[h] ❪G2,L2,T2❫ → Q G2 L2 T2) → - Q G1 L1 T1 - ) → - ∀G,L,T. ❪G,L❫ ⊢ ⬈*[h] 𝐒❪T❫ → ∀A. ❪G,L❫ ⊢ T ⁝ A → Q G L T. +fact aaa_ind_fpbg_aux (h) (Q:relation3 …): + (∀G1,L1,T1,A. + ❪G1,L1❫ ⊢ T1 ⁝ A → + (∀G2,L2,T2. ❪G1,L1,T1❫ >[h] ❪G2,L2,T2❫ → Q G2 L2 T2) → + Q G1 L1 T1 + ) → + ∀G,L,T. ❪G,L❫ ⊢ ⬈*𝐒[h] T → ∀A. ❪G,L❫ ⊢ T ⁝ A → Q G L T. #h #Q #IH #G #L #T #H @(csx_ind_fpbg … H) -G -L -T #G1 #L1 #T1 #H1 #IH1 #A1 #HTA1 @IH -IH // #G2 #L2 #T2 #H12 elim (fpbs_aaa_conf … G2 … L2 … T2 … HTA1) -A1 /2 width=2 by fpbg_fwd_fpbs/ qed-. -lemma aaa_ind_fpbg: ∀h. ∀Q:relation3 …. - (∀G1,L1,T1,A. ❪G1,L1❫ ⊢ T1 ⁝ A → - (∀G2,L2,T2. ❪G1,L1,T1❫ >[h] ❪G2,L2,T2❫ → Q G2 L2 T2) → - Q G1 L1 T1 - ) → - ∀G,L,T,A. ❪G,L❫ ⊢ T ⁝ A → Q G L T. +lemma aaa_ind_fpbg (h) (Q:relation3 …): + (∀G1,L1,T1,A. + ❪G1,L1❫ ⊢ T1 ⁝ A → + (∀G2,L2,T2. ❪G1,L1,T1❫ >[h] ❪G2,L2,T2❫ → Q G2 L2 T2) → + Q G1 L1 T1 + ) → + ∀G,L,T,A. ❪G,L❫ ⊢ T ⁝ A → Q G L T. /4 width=4 by aaa_ind_fpbg_aux, aaa_csx/ qed-. diff --git a/matita/matita/contribs/lambdadelta/basic_2/rt_computation/fsb_csx.ma b/matita/matita/contribs/lambdadelta/basic_2/rt_computation/fsb_csx.ma index 203f60b8a..0ee6c19fc 100644 --- a/matita/matita/contribs/lambdadelta/basic_2/rt_computation/fsb_csx.ma +++ b/matita/matita/contribs/lambdadelta/basic_2/rt_computation/fsb_csx.ma @@ -21,14 +21,16 @@ include "basic_2/rt_computation/fsb_fpbg.ma". (* Inversion lemmas with context-sensitive stringly rt-normalizing terms ****) -lemma fsb_inv_csx: ∀h,G,L,T. ≥[h] 𝐒❪G,L,T❫ → ❪G,L❫ ⊢ ⬈*[h] 𝐒❪T❫. +lemma fsb_inv_csx (h): + ∀G,L,T. ≥𝐒[h] ❪G,L,T❫ → ❪G,L❫ ⊢ ⬈*𝐒[h] T. #h #G #L #T #H @(fsb_ind_alt … H) -G -L -T /5 width=1 by csx_intro, fpb_cpx/ qed-. (* Propreties with context-sensitive stringly rt-normalizing terms **********) -lemma csx_fsb_fpbs: ∀h,G1,L1,T1. ❪G1,L1❫ ⊢ ⬈*[h] 𝐒❪T1❫ → - ∀G2,L2,T2. ❪G1,L1,T1❫ ≥[h] ❪G2,L2,T2❫ → ≥[h] 𝐒❪G2,L2,T2❫. +lemma csx_fsb_fpbs (h): + ∀G1,L1,T1. ❪G1,L1❫ ⊢ ⬈*𝐒[h] T1 → + ∀G2,L2,T2. ❪G1,L1,T1❫ ≥[h] ❪G2,L2,T2❫ → ≥𝐒[h] ❪G2,L2,T2❫. #h #G1 #L1 #T1 #H @(csx_ind … H) -T1 #T1 #HT1 #IHc #G2 #L2 #T2 @(fqup_wf_ind (Ⓣ) … G2 L2 T2) -G2 -L2 -T2 #G0 #L0 #T0 #IHu #H10 @@ -56,23 +58,26 @@ generalize in match IHu; -IHu generalize in match H10; -H10 ] qed. -lemma csx_fsb: ∀h,G,L,T. ❪G,L❫ ⊢ ⬈*[h] 𝐒❪T❫ → ≥[h] 𝐒❪G,L,T❫. +lemma csx_fsb (h): + ∀G,L,T. ❪G,L❫ ⊢ ⬈*𝐒[h] T → ≥𝐒[h] ❪G,L,T❫. /2 width=5 by csx_fsb_fpbs/ qed. (* Advanced eliminators *****************************************************) -lemma csx_ind_fpb: ∀h. ∀Q:relation3 genv lenv term. - (∀G1,L1,T1. ❪G1,L1❫ ⊢ ⬈*[h] 𝐒❪T1❫ → - (∀G2,L2,T2. ❪G1,L1,T1❫ ≻[h] ❪G2,L2,T2❫ → Q G2 L2 T2) → - Q G1 L1 T1 - ) → - ∀G,L,T. ❪G,L❫ ⊢ ⬈*[h] 𝐒❪T❫ → Q G L T. +lemma csx_ind_fpb (h) (Q:relation3 …): + (∀G1,L1,T1. + ❪G1,L1❫ ⊢ ⬈*𝐒[h] T1 → + (∀G2,L2,T2. ❪G1,L1,T1❫ ≻[h] ❪G2,L2,T2❫ → Q G2 L2 T2) → + Q G1 L1 T1 + ) → + ∀G,L,T. ❪G,L❫ ⊢ ⬈*𝐒[h] T → Q G L T. /4 width=4 by fsb_inv_csx, csx_fsb, fsb_ind_alt/ qed-. -lemma csx_ind_fpbg: ∀h. ∀Q:relation3 genv lenv term. - (∀G1,L1,T1. ❪G1,L1❫ ⊢ ⬈*[h] 𝐒❪T1❫ → - (∀G2,L2,T2. ❪G1,L1,T1❫ >[h] ❪G2,L2,T2❫ → Q G2 L2 T2) → - Q G1 L1 T1 - ) → - ∀G,L,T. ❪G,L❫ ⊢ ⬈*[h] 𝐒❪T❫ → Q G L T. +lemma csx_ind_fpbg (h) (Q:relation3 …): + (∀G1,L1,T1. + ❪G1,L1❫ ⊢ ⬈*𝐒[h] T1 → + (∀G2,L2,T2. ❪G1,L1,T1❫ >[h] ❪G2,L2,T2❫ → Q G2 L2 T2) → + Q G1 L1 T1 + ) → + ∀G,L,T. ❪G,L❫ ⊢ ⬈*𝐒[h] T → Q G L T. /4 width=4 by fsb_inv_csx, csx_fsb, fsb_ind_fpbg/ qed-. diff --git a/matita/matita/contribs/lambdadelta/basic_2/rt_computation/fsb_feqx.ma b/matita/matita/contribs/lambdadelta/basic_2/rt_computation/fsb_feqx.ma index c7311efe7..251fef0eb 100644 --- a/matita/matita/contribs/lambdadelta/basic_2/rt_computation/fsb_feqx.ma +++ b/matita/matita/contribs/lambdadelta/basic_2/rt_computation/fsb_feqx.ma @@ -19,8 +19,8 @@ include "basic_2/rt_computation/fsb.ma". (* Properties with sort-irrelevant equivalence for closures *****************) -lemma fsb_feqx_trans: ∀h,G1,L1,T1. ≥[h] 𝐒❪G1,L1,T1❫ → - ∀G2,L2,T2. ❪G1,L1,T1❫ ≛ ❪G2,L2,T2❫ → ≥[h] 𝐒❪G2,L2,T2❫. +lemma fsb_feqx_trans: ∀h,G1,L1,T1. ≥𝐒[h] ❪G1,L1,T1❫ → + ∀G2,L2,T2. ❪G1,L1,T1❫ ≛ ❪G2,L2,T2❫ → ≥𝐒[h] ❪G2,L2,T2❫. #h #G1 #L1 #T1 #H @(fsb_ind_alt … H) -G1 -L1 -T1 #G1 #L1 #T1 #_ #IH #G2 #L2 #T2 #H12 @fsb_intro #G #L #T #H2 diff --git a/matita/matita/contribs/lambdadelta/basic_2/rt_computation/fsb_fpbg.ma b/matita/matita/contribs/lambdadelta/basic_2/rt_computation/fsb_fpbg.ma index 81583f39e..20c010206 100644 --- a/matita/matita/contribs/lambdadelta/basic_2/rt_computation/fsb_fpbg.ma +++ b/matita/matita/contribs/lambdadelta/basic_2/rt_computation/fsb_fpbg.ma @@ -19,8 +19,8 @@ include "basic_2/rt_computation/fsb_feqx.ma". (* Properties with parallel rst-computation for closures ********************) -lemma fsb_fpbs_trans: ∀h,G1,L1,T1. ≥[h] 𝐒❪G1,L1,T1❫ → - ∀G2,L2,T2. ❪G1,L1,T1❫ ≥[h] ❪G2,L2,T2❫ → ≥[h] 𝐒❪G2,L2,T2❫. +lemma fsb_fpbs_trans: ∀h,G1,L1,T1. ≥𝐒[h] ❪G1,L1,T1❫ → + ∀G2,L2,T2. ❪G1,L1,T1❫ ≥[h] ❪G2,L2,T2❫ → ≥𝐒[h] ❪G2,L2,T2❫. #h #G1 #L1 #T1 #H @(fsb_ind_alt … H) -G1 -L1 -T1 #G1 #L1 #T1 #H1 #IH #G2 #L2 #T2 #H12 elim (fpbs_inv_fpbg … H12) -H12 @@ -32,18 +32,18 @@ qed-. (* Properties with proper parallel rst-computation for closures *************) lemma fsb_intro_fpbg: ∀h,G1,L1,T1. ( - ∀G2,L2,T2. ❪G1,L1,T1❫ >[h] ❪G2,L2,T2❫ → ≥[h] 𝐒❪G2,L2,T2❫ - ) → ≥[h] 𝐒❪G1,L1,T1❫. + ∀G2,L2,T2. ❪G1,L1,T1❫ >[h] ❪G2,L2,T2❫ → ≥𝐒[h] ❪G2,L2,T2❫ + ) → ≥𝐒[h] ❪G1,L1,T1❫. /4 width=1 by fsb_intro, fpb_fpbg/ qed. (* Eliminators with proper parallel rst-computation for closures ************) lemma fsb_ind_fpbg_fpbs: ∀h. ∀Q:relation3 genv lenv term. - (∀G1,L1,T1. ≥[h] 𝐒❪G1,L1,T1❫ → + (∀G1,L1,T1. ≥𝐒[h] ❪G1,L1,T1❫ → (∀G2,L2,T2. ❪G1,L1,T1❫ >[h] ❪G2,L2,T2❫ → Q G2 L2 T2) → Q G1 L1 T1 ) → - ∀G1,L1,T1. ≥[h] 𝐒❪G1,L1,T1❫ → + ∀G1,L1,T1. ≥𝐒[h] ❪G1,L1,T1❫ → ∀G2,L2,T2. ❪G1,L1,T1❫ ≥[h] ❪G2,L2,T2❫ → Q G2 L2 T2. #h #Q #IH1 #G1 #L1 #T1 #H @(fsb_ind_alt … H) -G1 -L1 -T1 #G1 #L1 #T1 #H1 #IH #G2 #L2 #T2 #H12 @@ -56,11 +56,11 @@ lemma fsb_ind_fpbg_fpbs: ∀h. ∀Q:relation3 genv lenv term. qed-. lemma fsb_ind_fpbg: ∀h. ∀Q:relation3 genv lenv term. - (∀G1,L1,T1. ≥[h] 𝐒❪G1,L1,T1❫ → + (∀G1,L1,T1. ≥𝐒[h] ❪G1,L1,T1❫ → (∀G2,L2,T2. ❪G1,L1,T1❫ >[h] ❪G2,L2,T2❫ → Q G2 L2 T2) → Q G1 L1 T1 ) → - ∀G1,L1,T1. ≥[h] 𝐒❪G1,L1,T1❫ → Q G1 L1 T1. + ∀G1,L1,T1. ≥𝐒[h] ❪G1,L1,T1❫ → Q G1 L1 T1. #h #Q #IH #G1 #L1 #T1 #H @(fsb_ind_fpbg_fpbs … H) -H /3 width=1 by/ qed-. @@ -68,7 +68,7 @@ qed-. (* Inversion lemmas with proper parallel rst-computation for closures *******) lemma fsb_fpbg_refl_false (h) (G) (L) (T): - ≥[h] 𝐒❪G,L,T❫ → ❪G,L,T❫ >[h] ❪G,L,T❫ → ⊥. + ≥𝐒[h] ❪G,L,T❫ → ❪G,L,T❫ >[h] ❪G,L,T❫ → ⊥. #h #G #L #T #H @(fsb_ind_fpbg … H) -G -L -T #G1 #L1 #T1 #_ #IH #H /2 width=5 by/ diff --git a/matita/matita/contribs/lambdadelta/basic_2/rt_computation/jsx.ma b/matita/matita/contribs/lambdadelta/basic_2/rt_computation/jsx.ma index a318423b5..2e477082b 100644 --- a/matita/matita/contribs/lambdadelta/basic_2/rt_computation/jsx.ma +++ b/matita/matita/contribs/lambdadelta/basic_2/rt_computation/jsx.ma @@ -25,7 +25,7 @@ inductive jsx (h) (G): relation lenv ≝ | jsx_bind: ∀I,K1,K2. jsx h G K1 K2 → jsx h G (K1.ⓘ[I]) (K2.ⓘ[I]) | jsx_pair: ∀I,K1,K2,V. jsx h G K1 K2 → - G ⊢ ⬈*[h,V] 𝐒❪K2❫ → jsx h G (K1.ⓑ[I]V) (K2.ⓧ) + G ⊢ ⬈*𝐒[h,V] K2 → jsx h G (K1.ⓑ[I]V) (K2.ⓧ) . interpretation @@ -43,14 +43,15 @@ fact jsx_inv_atom_sn_aux (h) (G): ] qed-. -lemma jsx_inv_atom_sn (h) (G): ∀L2. G ⊢ ⋆ ⊒[h] L2 → L2 = ⋆. +lemma jsx_inv_atom_sn (h) (G): + ∀L2. G ⊢ ⋆ ⊒[h] L2 → L2 = ⋆. /2 width=5 by jsx_inv_atom_sn_aux/ qed-. fact jsx_inv_bind_sn_aux (h) (G): ∀L1,L2. G ⊢ L1 ⊒[h] L2 → ∀I,K1. L1 = K1.ⓘ[I] → ∨∨ ∃∃K2. G ⊢ K1 ⊒[h] K2 & L2 = K2.ⓘ[I] - | ∃∃J,K2,V. G ⊢ K1 ⊒[h] K2 & G ⊢ ⬈*[h,V] 𝐒❪K2❫ & I = BPair J V & L2 = K2.ⓧ. + | ∃∃J,K2,V. G ⊢ K1 ⊒[h] K2 & G ⊢ ⬈*𝐒[h,V] K2 & I = BPair J V & L2 = K2.ⓧ. #h #G #L1 #L2 * -L1 -L2 [ #J #L1 #H destruct | #I #K1 #K2 #HK12 #J #L1 #H destruct /3 width=3 by ex2_intro, or_introl/ @@ -61,7 +62,7 @@ qed-. lemma jsx_inv_bind_sn (h) (G): ∀I,K1,L2. G ⊢ K1.ⓘ[I] ⊒[h] L2 → ∨∨ ∃∃K2. G ⊢ K1 ⊒[h] K2 & L2 = K2.ⓘ[I] - | ∃∃J,K2,V. G ⊢ K1 ⊒[h] K2 & G ⊢ ⬈*[h,V] 𝐒❪K2❫ & I = BPair J V & L2 = K2.ⓧ. + | ∃∃J,K2,V. G ⊢ K1 ⊒[h] K2 & G ⊢ ⬈*𝐒[h,V] K2 & I = BPair J V & L2 = K2.ⓧ. /2 width=3 by jsx_inv_bind_sn_aux/ qed-. (* Advanced inversion lemmas ************************************************) @@ -70,7 +71,7 @@ lemma jsx_inv_bind_sn (h) (G): lemma jsx_inv_pair_sn (h) (G): ∀I,K1,L2,V. G ⊢ K1.ⓑ[I]V ⊒[h] L2 → ∨∨ ∃∃K2. G ⊢ K1 ⊒[h] K2 & L2 = K2.ⓑ[I]V - | ∃∃K2. G ⊢ K1 ⊒[h] K2 & G ⊢ ⬈*[h,V] 𝐒❪K2❫ & L2 = K2.ⓧ. + | ∃∃K2. G ⊢ K1 ⊒[h] K2 & G ⊢ ⬈*𝐒[h,V] K2 & L2 = K2.ⓧ. #h #G #I #K1 #L2 #V #H elim (jsx_inv_bind_sn … H) -H * [ /3 width=3 by ex2_intro, or_introl/ | #J #K2 #X #HK12 #HX #H1 #H2 destruct /3 width=4 by ex3_intro, or_intror/ diff --git a/matita/matita/contribs/lambdadelta/basic_2/rt_computation/jsx_csx.ma b/matita/matita/contribs/lambdadelta/basic_2/rt_computation/jsx_csx.ma index 642520638..702869092 100644 --- a/matita/matita/contribs/lambdadelta/basic_2/rt_computation/jsx_csx.ma +++ b/matita/matita/contribs/lambdadelta/basic_2/rt_computation/jsx_csx.ma @@ -22,15 +22,15 @@ include "basic_2/rt_computation/jsx_lsubr.ma". lemma jsx_csx_conf (h) (G): ∀L1,L2. G ⊢ L1 ⊒[h] L2 → - ∀T. ❪G,L1❫ ⊢ ⬈*[h] 𝐒❪T❫ → ❪G,L2❫ ⊢ ⬈*[h] 𝐒❪T❫. + ∀T. ❪G,L1❫ ⊢ ⬈*𝐒[h] T → ❪G,L2❫ ⊢ ⬈*𝐒[h] T. /3 width=5 by jsx_fwd_lsubr, csx_lsubr_conf/ qed-. (* Properties with strongly rt-normalizing referred local environments ******) (* Note: Try by induction on the 2nd premise by generalizing V with f *) lemma rsx_jsx_trans (h) (G): - ∀L1,V. G ⊢ ⬈*[h,V] 𝐒❪L1❫ → - ∀L2. G ⊢ L1 ⊒[h] L2 → G ⊢ ⬈*[h,V] 𝐒❪L2❫. + ∀L1,V. G ⊢ ⬈*𝐒[h,V] L1 → + ∀L2. G ⊢ L1 ⊒[h] L2 → G ⊢ ⬈*𝐒[h,V] L2. #h #G #L1 #V @(fqup_wf_ind_eq (Ⓕ) … G L1 V) -G -L1 -V #G0 #L0 #V0 #IH #G #L1 * * [ // diff --git a/matita/matita/contribs/lambdadelta/basic_2/rt_computation/jsx_drops.ma b/matita/matita/contribs/lambdadelta/basic_2/rt_computation/jsx_drops.ma index 01fe99176..56148c3af 100644 --- a/matita/matita/contribs/lambdadelta/basic_2/rt_computation/jsx_drops.ma +++ b/matita/matita/contribs/lambdadelta/basic_2/rt_computation/jsx_drops.ma @@ -56,7 +56,7 @@ lemma jsx_fwd_drops_pair_sn (h) (b) (G): ∀L1,L2. G ⊢ L1 ⊒[h] L2 → ∀f. 𝐔❪f❫ → ∀I,K1,V. ⇩*[b,f]L1 ≘ K1.ⓑ[I]V → ∨∨ ∃∃K2. G ⊢ K1 ⊒[h] K2 & ⇩*[b,f]L2 ≘ K2.ⓑ[I]V - | ∃∃K2. G ⊢ K1 ⊒[h] K2 & ⇩*[b,f]L2 ≘ K2.ⓧ & G ⊢ ⬈*[h,V] 𝐒❪K2❫. + | ∃∃K2. G ⊢ K1 ⊒[h] K2 & ⇩*[b,f]L2 ≘ K2.ⓧ & G ⊢ ⬈*𝐒[h,V] K2. #h #b #G #L1 #L2 #H elim H -L1 -L2 [ #f #_ #J #Y1 #X1 #H lapply (drops_inv_atom1 … H) -H * #H #_ destruct diff --git a/matita/matita/contribs/lambdadelta/basic_2/rt_computation/jsx_lsubr.ma b/matita/matita/contribs/lambdadelta/basic_2/rt_computation/jsx_lsubr.ma index 6fc723294..4e048982b 100644 --- a/matita/matita/contribs/lambdadelta/basic_2/rt_computation/jsx_lsubr.ma +++ b/matita/matita/contribs/lambdadelta/basic_2/rt_computation/jsx_lsubr.ma @@ -19,7 +19,8 @@ include "basic_2/rt_computation/jsx.ma". (* Forward lemmas with restricted refinement for local environments *********) -lemma jsx_fwd_lsubr (h) (G): ∀L1,L2. G ⊢ L1 ⊒[h] L2 → L1 ⫃ L2. +lemma jsx_fwd_lsubr (h) (G): + ∀L1,L2. G ⊢ L1 ⊒[h] L2 → L1 ⫃ L2. #h #G #L1 #L2 #H elim H -L1 -L2 /2 width=1 by lsubr_bind, lsubr_unit/ qed-. diff --git a/matita/matita/contribs/lambdadelta/basic_2/rt_computation/jsx_rsx.ma b/matita/matita/contribs/lambdadelta/basic_2/rt_computation/jsx_rsx.ma index dd874f6aa..0137a4087 100644 --- a/matita/matita/contribs/lambdadelta/basic_2/rt_computation/jsx_rsx.ma +++ b/matita/matita/contribs/lambdadelta/basic_2/rt_computation/jsx_rsx.ma @@ -23,7 +23,7 @@ include "basic_2/rt_computation/jsx.ma". (* Basic_2A1: uses: lsx_cpx_trans_lcosx *) lemma rsx_cpx_trans_jsx (h) (G): ∀L0,T1,T2. ❪G,L0❫ ⊢ T1 ⬈[h] T2 → - ∀L. G ⊢ L0 ⊒[h] L → G ⊢ ⬈*[h,T1] 𝐒❪L❫ → G ⊢ ⬈*[h,T2] 𝐒❪L❫. + ∀L. G ⊢ L0 ⊒[h] L → G ⊢ ⬈*𝐒[h,T1] L → G ⊢ ⬈*𝐒[h,T2] L. #h #G #L0 #T1 #T2 #H @(cpx_ind … H) -G -L0 -T1 -T2 [ // | // @@ -65,12 +65,12 @@ qed-. (* Basic_2A1: uses: lsx_cpx_trans_O *) lemma rsx_cpx_trans (h) (G): ∀L,T1,T2. ❪G,L❫ ⊢ T1 ⬈[h] T2 → - G ⊢ ⬈*[h,T1] 𝐒❪L❫ → G ⊢ ⬈*[h,T2] 𝐒❪L❫. + G ⊢ ⬈*𝐒[h,T1] L → G ⊢ ⬈*𝐒[h,T2] L. /3 width=6 by rsx_cpx_trans_jsx, jsx_refl/ qed-. lemma rsx_cpxs_trans (h) (G): ∀L,T1,T2. ❪G,L❫ ⊢ T1 ⬈*[h] T2 → - G ⊢ ⬈*[h,T1] 𝐒❪L❫ → G ⊢ ⬈*[h,T2] 𝐒❪L❫. + G ⊢ ⬈*𝐒[h,T1] L → G ⊢ ⬈*𝐒[h,T2] L. #h #G #L #T1 #T2 #H @(cpxs_ind_dx ???????? H) -T1 // /3 width=3 by rsx_cpx_trans/ diff --git a/matita/matita/contribs/lambdadelta/basic_2/rt_computation/rsx.ma b/matita/matita/contribs/lambdadelta/basic_2/rt_computation/rsx.ma index 81e3d9154..35e326136 100644 --- a/matita/matita/contribs/lambdadelta/basic_2/rt_computation/rsx.ma +++ b/matita/matita/contribs/lambdadelta/basic_2/rt_computation/rsx.ma @@ -22,18 +22,18 @@ definition rsx (h) (G) (T): predicate lenv ≝ SN … (lpx h G) (reqx T). interpretation - "strong normalization for unbound context-sensitive parallel rt-transition on referred entries (local environment)" - 'PRedTySNStrong h T G L = (rsx h G T L). + "strong normalization for unbound context-sensitive parallel rt-transition on referred entries (local environment)" + 'PRedTySNStrong h T G L = (rsx h G T L). (* Basic eliminators ********************************************************) (* Basic_2A1: uses: lsx_ind *) -lemma rsx_ind (h) (G) (T) (Q:predicate lenv): - (∀L1. G ⊢ ⬈*[h,T] 𝐒❪L1❫ → - (∀L2. ❪G,L1❫ ⊢ ⬈[h] L2 → (L1 ≛[T] L2 → ⊥) → Q L2) → - Q L1 +lemma rsx_ind (h) (G) (T) (Q:predicate …): + (∀L1. G ⊢ ⬈*𝐒[h,T] L1 → + (∀L2. ❪G,L1❫ ⊢ ⬈[h] L2 → (L1 ≛[T] L2 → ⊥) → Q L2) → + Q L1 ) → - ∀L. G ⊢ ⬈*[h,T] 𝐒❪L❫ → Q L. + ∀L. G ⊢ ⬈*𝐒[h,T] L → Q L. #h #G #T #Q #H0 #L1 #H elim H -L1 /5 width=1 by SN_intro/ qed-. @@ -43,16 +43,16 @@ qed-. (* Basic_2A1: uses: lsx_intro *) lemma rsx_intro (h) (G) (T): ∀L1. - (∀L2. ❪G,L1❫ ⊢ ⬈[h] L2 → (L1 ≛[T] L2 → ⊥) → G ⊢ ⬈*[h,T] 𝐒❪L2❫) → - G ⊢ ⬈*[h,T] 𝐒❪L1❫. + (∀L2. ❪G,L1❫ ⊢ ⬈[h] L2 → (L1 ≛[T] L2 → ⊥) → G ⊢ ⬈*𝐒[h,T] L2) → + G ⊢ ⬈*𝐒[h,T] L1. /5 width=1 by SN_intro/ qed. (* Basic forward lemmas *****************************************************) (* Basic_2A1: uses: lsx_fwd_pair_sn lsx_fwd_bind_sn lsx_fwd_flat_sn *) lemma rsx_fwd_pair_sn (h) (G): - ∀I,L,V,T. G ⊢ ⬈*[h,②[I]V.T] 𝐒❪L❫ → - G ⊢ ⬈*[h,V] 𝐒❪L❫. + ∀I,L,V,T. G ⊢ ⬈*𝐒[h,②[I]V.T] L → + G ⊢ ⬈*𝐒[h,V] L. #h #G #I #L #V #T #H @(rsx_ind … H) -L #L1 #_ #IHL1 @rsx_intro #L2 #HL12 #HnL12 @@ -61,8 +61,8 @@ qed-. (* Basic_2A1: uses: lsx_fwd_flat_dx *) lemma rsx_fwd_flat_dx (h) (G): - ∀I,L,V,T. G ⊢ ⬈*[h,ⓕ[I]V.T] 𝐒❪L❫ → - G ⊢ ⬈*[h,T] 𝐒❪L❫. + ∀I,L,V,T. G ⊢ ⬈*𝐒[h,ⓕ[I]V.T] L → + G ⊢ ⬈*𝐒[h,T] L. #h #G #I #L #V #T #H @(rsx_ind … H) -L #L1 #_ #IHL1 @rsx_intro #L2 #HL12 #HnL12 @@ -70,23 +70,23 @@ lemma rsx_fwd_flat_dx (h) (G): qed-. fact rsx_fwd_pair_aux (h) (G): - ∀L. G ⊢ ⬈*[h,#0] 𝐒❪L❫ → - ∀I,K,V. L = K.ⓑ[I]V → G ⊢ ⬈*[h,V] 𝐒❪K❫. + ∀L. G ⊢ ⬈*𝐒[h,#0] L → + ∀I,K,V. L = K.ⓑ[I]V → G ⊢ ⬈*𝐒[h,V] K. #h #G #L #H @(rsx_ind … H) -L #L1 #_ #IH #I #K1 #V #H destruct /5 width=5 by lpx_pair, rsx_intro, reqx_fwd_zero_pair/ qed-. lemma rsx_fwd_pair (h) (G): - ∀I,K,V. G ⊢ ⬈*[h,#0] 𝐒❪K.ⓑ[I]V❫ → G ⊢ ⬈*[h,V] 𝐒❪K❫. + ∀I,K,V. G ⊢ ⬈*𝐒[h,#0] K.ⓑ[I]V → G ⊢ ⬈*𝐒[h,V] K. /2 width=4 by rsx_fwd_pair_aux/ qed-. (* Basic inversion lemmas ***************************************************) (* Basic_2A1: uses: lsx_inv_flat *) lemma rsx_inv_flat (h) (G): - ∀I,L,V,T. G ⊢ ⬈*[h,ⓕ[I]V.T] 𝐒❪L❫ → - ∧∧ G ⊢ ⬈*[h,V] 𝐒❪L❫ & G ⊢ ⬈*[h,T] 𝐒❪L❫. + ∀I,L,V,T. G ⊢ ⬈*𝐒[h,ⓕ[I]V.T] L → + ∧∧ G ⊢ ⬈*𝐒[h,V] L & G ⊢ ⬈*𝐒[h,T] L. /3 width=3 by rsx_fwd_pair_sn, rsx_fwd_flat_dx, conj/ qed-. (* Basic_2A1: removed theorems 9: diff --git a/matita/matita/contribs/lambdadelta/basic_2/rt_computation/rsx_csx.ma b/matita/matita/contribs/lambdadelta/basic_2/rt_computation/rsx_csx.ma index 24ff0f82a..e9e5f5a37 100644 --- a/matita/matita/contribs/lambdadelta/basic_2/rt_computation/rsx_csx.ma +++ b/matita/matita/contribs/lambdadelta/basic_2/rt_computation/rsx_csx.ma @@ -21,8 +21,8 @@ include "basic_2/rt_computation/jsx_rsx.ma". (* Forward lemmas with strongly rt-normalizing terms ************************) fact rsx_fwd_lref_pair_csx_aux (h) (G): - ∀L. G ⊢ ⬈*[h,#0] 𝐒❪L❫ → - ∀I,K,V. L = K.ⓑ[I]V → ❪G,K❫ ⊢ ⬈*[h] 𝐒❪V❫. + ∀L. G ⊢ ⬈*𝐒[h,#0] L → + ∀I,K,V. L = K.ⓑ[I]V → ❪G,K❫ ⊢ ⬈*𝐒[h] V. #h #G #L #H @(rsx_ind … H) -L #L #_ #IH #I #K #V1 #H destruct @csx_intro #V2 #HV12 #HnV12 @@ -34,11 +34,11 @@ fact rsx_fwd_lref_pair_csx_aux (h) (G): qed-. lemma rsx_fwd_lref_pair_csx (h) (G): - ∀I,K,V. G ⊢ ⬈*[h,#0] 𝐒❪K.ⓑ[I]V❫ → ❪G,K❫ ⊢ ⬈*[h] 𝐒❪V❫. + ∀I,K,V. G ⊢ ⬈*𝐒[h,#0] K.ⓑ[I]V → ❪G,K❫ ⊢ ⬈*𝐒[h] V. /2 width=4 by rsx_fwd_lref_pair_csx_aux/ qed-. lemma rsx_fwd_lref_pair_csx_drops (h) (G): - ∀I,K,V,i,L. ⇩[i] L ≘ K.ⓑ[I]V → G ⊢ ⬈*[h,#i] 𝐒❪L❫ → ❪G,K❫ ⊢ ⬈*[h] 𝐒❪V❫. + ∀I,K,V,i,L. ⇩[i] L ≘ K.ⓑ[I]V → G ⊢ ⬈*𝐒[h,#i] L → ❪G,K❫ ⊢ ⬈*𝐒[h] V. #h #G #I #K #V #i elim i -i [ #L #H >(drops_fwd_isid … H) -H /2 width=2 by rsx_fwd_lref_pair_csx/ @@ -52,20 +52,20 @@ qed-. (* Inversion lemmas with strongly rt-normalizing terms **********************) lemma rsx_inv_lref_pair (h) (G): - ∀I,K,V. G ⊢ ⬈*[h,#0] 𝐒❪K.ⓑ[I]V❫ → - ∧∧ ❪G,K❫ ⊢ ⬈*[h] 𝐒❪V❫ & G ⊢ ⬈*[h,V] 𝐒❪K❫. + ∀I,K,V. G ⊢ ⬈*𝐒[h,#0] K.ⓑ[I]V → + ∧∧ ❪G,K❫ ⊢ ⬈*𝐒[h] V & G ⊢ ⬈*𝐒[h,V] K. /3 width=2 by rsx_fwd_lref_pair_csx, rsx_fwd_pair, conj/ qed-. lemma rsx_inv_lref_pair_drops (h) (G): - ∀I,K,V,i,L. ⇩[i] L ≘ K.ⓑ[I]V → G ⊢ ⬈*[h,#i] 𝐒❪L❫ → - ∧∧ ❪G,K❫ ⊢ ⬈*[h] 𝐒❪V❫ & G ⊢ ⬈*[h,V] 𝐒❪K❫. + ∀I,K,V,i,L. ⇩[i] L ≘ K.ⓑ[I]V → G ⊢ ⬈*𝐒[h,#i] L → + ∧∧ ❪G,K❫ ⊢ ⬈*𝐒[h] V & G ⊢ ⬈*𝐒[h,V] K. /3 width=5 by rsx_fwd_lref_pair_csx_drops, rsx_fwd_lref_pair_drops, conj/ qed-. lemma rsx_inv_lref_drops (h) (G): - ∀L,i. G ⊢ ⬈*[h,#i] 𝐒❪L❫ → + ∀L,i. G ⊢ ⬈*𝐒[h,#i] L → ∨∨ ⇩*[Ⓕ,𝐔❨i❩] L ≘ ⋆ | ∃∃I,K. ⇩[i] L ≘ K.ⓤ[I] - | ∃∃I,K,V. ⇩[i] L ≘ K.ⓑ[I]V & ❪G,K❫ ⊢ ⬈*[h] 𝐒❪V❫ & G ⊢ ⬈*[h,V] 𝐒❪K❫. + | ∃∃I,K,V. ⇩[i] L ≘ K.ⓑ[I]V & ❪G,K❫ ⊢ ⬈*𝐒[h] V & G ⊢ ⬈*𝐒[h,V] K. #h #G #L #i #H elim (drops_F_uni L i) [ /2 width=1 by or3_intro0/ | * * /4 width=10 by rsx_fwd_lref_pair_csx_drops, rsx_fwd_lref_pair_drops, ex3_3_intro, ex1_2_intro, or3_intro2, or3_intro1/ @@ -77,9 +77,9 @@ qed-. (* Note: swapping the eliminations to avoid rsx_cpx_trans: no solution found *) (* Basic_2A1: uses: lsx_lref_be_lpxs *) lemma rsx_lref_pair_lpxs (h) (G): - ∀K1,V. ❪G,K1❫ ⊢ ⬈*[h] 𝐒❪V❫ → - ∀K2. G ⊢ ⬈*[h,V] 𝐒❪K2❫ → ❪G,K1❫ ⊢ ⬈*[h] K2 → - ∀I. G ⊢ ⬈*[h,#0] 𝐒❪K2.ⓑ[I]V❫. + ∀K1,V. ❪G,K1❫ ⊢ ⬈*𝐒[h] V → + ∀K2. G ⊢ ⬈*𝐒[h,V] K2 → ❪G,K1❫ ⊢ ⬈*[h] K2 → + ∀I. G ⊢ ⬈*𝐒[h,#0] K2.ⓑ[I]V. #h #G #K1 #V #H @(csx_ind_cpxs … H) -V #V0 #_ #IHV0 #K2 #H @(rsx_ind … H) -K2 #K0 #HK0 #IHK0 #HK10 #I @@ -96,13 +96,13 @@ elim (teqx_dec V0 V2) #HnV02 destruct [ -IHV0 -HV02 -HK0 | -IHK0 -HnY ] qed. lemma rsx_lref_pair (h) (G): - ∀K,V. ❪G,K❫ ⊢ ⬈*[h] 𝐒❪V❫ → G ⊢ ⬈*[h,V] 𝐒❪K❫ → ∀I. G ⊢ ⬈*[h,#0] 𝐒❪K.ⓑ[I]V❫. + ∀K,V. ❪G,K❫ ⊢ ⬈*𝐒[h] V → G ⊢ ⬈*𝐒[h,V] K → ∀I. G ⊢ ⬈*𝐒[h,#0] K.ⓑ[I]V. /2 width=3 by rsx_lref_pair_lpxs/ qed. (* Basic_2A1: uses: lsx_lref_be *) lemma rsx_lref_pair_drops (h) (G): - ∀K,V. ❪G,K❫ ⊢ ⬈*[h] 𝐒❪V❫ → G ⊢ ⬈*[h,V] 𝐒❪K❫ → - ∀I,i,L. ⇩[i] L ≘ K.ⓑ[I]V → G ⊢ ⬈*[h,#i] 𝐒❪L❫. + ∀K,V. ❪G,K❫ ⊢ ⬈*𝐒[h] V → G ⊢ ⬈*𝐒[h,V] K → + ∀I,i,L. ⇩[i] L ≘ K.ⓑ[I]V → G ⊢ ⬈*𝐒[h,#i] L. #h #G #K #V #HV #HK #I #i elim i -i [ #L #H >(drops_fwd_isid … H) -H /2 width=1 by rsx_lref_pair/ | #i #IH #L #H @@ -114,7 +114,8 @@ qed. (* Main properties with strongly rt-normalizing terms ***********************) (* Basic_2A1: uses: csx_lsx *) -theorem csx_rsx (h) (G): ∀L,T. ❪G,L❫ ⊢ ⬈*[h] 𝐒❪T❫ → G ⊢ ⬈*[h,T] 𝐒❪L❫. +theorem csx_rsx (h) (G): + ∀L,T. ❪G,L❫ ⊢ ⬈*𝐒[h] T → G ⊢ ⬈*𝐒[h,T] L. #h #G #L #T @(fqup_wf_ind_eq (Ⓣ) … G L T) -G -L -T #Z #Y #X #IH #G #L * * [ // diff --git a/matita/matita/contribs/lambdadelta/basic_2/rt_computation/rsx_drops.ma b/matita/matita/contribs/lambdadelta/basic_2/rt_computation/rsx_drops.ma index 55999f8f8..c4f6113ce 100644 --- a/matita/matita/contribs/lambdadelta/basic_2/rt_computation/rsx_drops.ma +++ b/matita/matita/contribs/lambdadelta/basic_2/rt_computation/rsx_drops.ma @@ -23,7 +23,8 @@ include "basic_2/rt_computation/rsx_fqup.ma". (* Note: this uses length *) (* Basic_2A1: uses: lsx_lift_le lsx_lift_ge *) -lemma rsx_lifts (h) (G): d_liftable1_isuni … (λL,T. G ⊢ ⬈*[h,T] 𝐒❪L❫). +lemma rsx_lifts (h) (G): + d_liftable1_isuni … (λL,T. G ⊢ ⬈*𝐒[h,T] L). #h #G #K #T #H @(rsx_ind … H) -K #K1 #_ #IH #b #f #L1 #HLK1 #Hf #U #HTU @rsx_intro #L2 #HL12 #HnL12 elim (lpx_drops_conf … HLK1 … HL12) @@ -33,7 +34,8 @@ qed-. (* Inversion lemmas on relocation *******************************************) (* Basic_2A1: uses: lsx_inv_lift_le lsx_inv_lift_be lsx_inv_lift_ge *) -lemma rsx_inv_lifts (h) (G): d_deliftable1_isuni … (λL,T. G ⊢ ⬈*[h,T] 𝐒❪L❫). +lemma rsx_inv_lifts (h) (G): + d_deliftable1_isuni … (λL,T. G ⊢ ⬈*𝐒[h,T] L). #h #G #L #U #H @(rsx_ind … H) -L #L1 #_ #IH #b #f #K1 #HLK1 #Hf #T #HTU @rsx_intro #K2 #HK12 #HnK12 elim (drops_lpx_trans … HLK1 … HK12) -HK12 @@ -43,13 +45,15 @@ qed-. (* Advanced properties ******************************************************) (* Basic_2A1: uses: lsx_lref_free *) -lemma rsx_lref_atom_drops (h) (G): ∀L,i. ⇩*[Ⓕ,𝐔❨i❩] L ≘ ⋆ → G ⊢ ⬈*[h,#i] 𝐒❪L❫. +lemma rsx_lref_atom_drops (h) (G): + ∀L,i. ⇩*[Ⓕ,𝐔❨i❩] L ≘ ⋆ → G ⊢ ⬈*𝐒[h,#i] L. #h #G #L1 #i #HL1 @(rsx_lifts … (#0) … HL1) -HL1 // qed. (* Basic_2A1: uses: lsx_lref_skip *) -lemma rsx_lref_unit_drops (h) (G): ∀I,L,K,i. ⇩[i] L ≘ K.ⓤ[I] → G ⊢ ⬈*[h,#i] 𝐒❪L❫. +lemma rsx_lref_unit_drops (h) (G): + ∀I,L,K,i. ⇩[i] L ≘ K.ⓤ[I] → G ⊢ ⬈*𝐒[h,#i] L. #h #G #I #L1 #K1 #i #HL1 @(rsx_lifts … (#0) … HL1) -HL1 // qed. @@ -58,8 +62,8 @@ qed. (* Basic_2A1: uses: lsx_fwd_lref_be *) lemma rsx_fwd_lref_pair_drops (h) (G): - ∀L,i. G ⊢ ⬈*[h,#i] 𝐒❪L❫ → - ∀I,K,V. ⇩[i] L ≘ K.ⓑ[I]V → G ⊢ ⬈*[h,V] 𝐒❪K❫. + ∀L,i. G ⊢ ⬈*𝐒[h,#i] L → + ∀I,K,V. ⇩[i] L ≘ K.ⓑ[I]V → G ⊢ ⬈*𝐒[h,V] K. #h #G #L #i #HL #I #K #V #HLK lapply (rsx_inv_lifts … HL … HLK … (#0) ?) -L /2 width=2 by rsx_fwd_pair/ diff --git a/matita/matita/contribs/lambdadelta/basic_2/rt_computation/rsx_fqup.ma b/matita/matita/contribs/lambdadelta/basic_2/rt_computation/rsx_fqup.ma index c654e3729..b638da30e 100644 --- a/matita/matita/contribs/lambdadelta/basic_2/rt_computation/rsx_fqup.ma +++ b/matita/matita/contribs/lambdadelta/basic_2/rt_computation/rsx_fqup.ma @@ -20,7 +20,7 @@ include "basic_2/rt_computation/rsx.ma". (* Advanced properties ******************************************************) (* Basic_2A1: uses: lsx_atom *) -lemma lfsx_atom (h) (G) (T): G ⊢ ⬈*[h,T] 𝐒❪⋆❫. +lemma lfsx_atom (h) (G) (T): G ⊢ ⬈*𝐒[h,T] ⋆. #h #G #T @rsx_intro #Y #H #HnT lapply (lpx_inv_atom_sn … H) -H #H destruct @@ -33,7 +33,7 @@ qed. (* Note: the exclusion binder (ⓧ) makes this more elegant and much simpler *) (* Note: the old proof without the exclusion binder requires lreq *) lemma rsx_fwd_bind_dx_void (h) (G): - ∀p,I,L,V,T. G ⊢ ⬈*[h,ⓑ[p,I]V.T] 𝐒❪L❫ → G ⊢ ⬈*[h,T] 𝐒❪L.ⓧ❫. + ∀p,I,L,V,T. G ⊢ ⬈*𝐒[h,ⓑ[p,I]V.T] L → G ⊢ ⬈*𝐒[h,T] L.ⓧ. #h #G #p #I #L #V #T #H @(rsx_ind … H) -L #L1 #_ #IH @rsx_intro #Y #H #HT @@ -45,6 +45,6 @@ qed-. (* Basic_2A1: uses: lsx_inv_bind *) lemma rsx_inv_bind_void (h) (G): - ∀p,I,L,V,T. G ⊢ ⬈*[h,ⓑ[p,I]V.T] 𝐒❪L❫ → - ∧∧ G ⊢ ⬈*[h,V] 𝐒❪L❫ & G ⊢ ⬈*[h,T] 𝐒❪L.ⓧ❫. + ∀p,I,L,V,T. G ⊢ ⬈*𝐒[h,ⓑ[p,I]V.T] L → + ∧∧ G ⊢ ⬈*𝐒[h,V] L & G ⊢ ⬈*𝐒[h,T] L.ⓧ. /3 width=4 by rsx_fwd_pair_sn, rsx_fwd_bind_dx_void, conj/ qed-. diff --git a/matita/matita/contribs/lambdadelta/basic_2/rt_computation/rsx_length.ma b/matita/matita/contribs/lambdadelta/basic_2/rt_computation/rsx_length.ma index 81021b2c8..4a5a8a4e5 100644 --- a/matita/matita/contribs/lambdadelta/basic_2/rt_computation/rsx_length.ma +++ b/matita/matita/contribs/lambdadelta/basic_2/rt_computation/rsx_length.ma @@ -21,18 +21,18 @@ include "basic_2/rt_computation/rsx.ma". (* Advanced properties ******************************************************) (* Basic_2A1: uses: lsx_sort *) -lemma rsx_sort (h) (G): ∀L,s. G ⊢ ⬈*[h,⋆s] 𝐒❪L❫. +lemma rsx_sort (h) (G): ∀L,s. G ⊢ ⬈*𝐒[h,⋆s] L. #h #G #L1 #s @rsx_intro #L2 #H #Hs elim Hs -Hs /3 width=3 by lpx_fwd_length, reqx_sort_length/ qed. (* Basic_2A1: uses: lsx_gref *) -lemma rsx_gref (h) (G): ∀L,l. G ⊢ ⬈*[h,§l] 𝐒❪L❫. +lemma rsx_gref (h) (G): ∀L,l. G ⊢ ⬈*𝐒[h,§l] L. #h #G #L1 #s @rsx_intro #L2 #H #Hs elim Hs -Hs /3 width=3 by lpx_fwd_length, reqx_gref_length/ qed. -lemma rsx_unit (h) (G): ∀I,L. G ⊢ ⬈*[h,#0] 𝐒❪L.ⓤ[I]❫. +lemma rsx_unit (h) (G): ∀I,L. G ⊢ ⬈*𝐒[h,#0] L.ⓤ[I]. #h #G #I #L1 @rsx_intro #Y #HY #HnY elim HnY -HnY elim (lpx_inv_unit_sn … HY) -HY #L2 #HL12 #H destruct diff --git a/matita/matita/contribs/lambdadelta/basic_2/rt_computation/rsx_lpxs.ma b/matita/matita/contribs/lambdadelta/basic_2/rt_computation/rsx_lpxs.ma index f0a53e660..5bbdcb180 100644 --- a/matita/matita/contribs/lambdadelta/basic_2/rt_computation/rsx_lpxs.ma +++ b/matita/matita/contribs/lambdadelta/basic_2/rt_computation/rsx_lpxs.ma @@ -22,14 +22,14 @@ include "basic_2/rt_computation/rsx_rsx.ma". (* Basic_2A1: uses: lsx_intro_alt *) lemma rsx_intro_lpxs (h) (G): - ∀L1,T. (∀L2. ❪G,L1❫ ⊢ ⬈*[h] L2 → (L1 ≛[T] L2 → ⊥) → G ⊢ ⬈*[h,T] 𝐒❪L2❫) → - G ⊢ ⬈*[h,T] 𝐒❪L1❫. + ∀L1,T. (∀L2. ❪G,L1❫ ⊢ ⬈*[h] L2 → (L1 ≛[T] L2 → ⊥) → G ⊢ ⬈*𝐒[h,T] L2) → + G ⊢ ⬈*𝐒[h,T] L1. /4 width=1 by lpx_lpxs, rsx_intro/ qed-. (* Basic_2A1: uses: lsx_lpxs_trans *) lemma rsx_lpxs_trans (h) (G): - ∀L1,T. G ⊢ ⬈*[h,T] 𝐒❪L1❫ → - ∀L2. ❪G,L1❫ ⊢ ⬈*[h] L2 → G ⊢ ⬈*[h,T] 𝐒❪L2❫. + ∀L1,T. G ⊢ ⬈*𝐒[h,T] L1 → + ∀L2. ❪G,L1❫ ⊢ ⬈*[h] L2 → G ⊢ ⬈*𝐒[h,T] L2. #h #G #L1 #T #HL1 #L2 #H @(lpxs_ind_dx … H) -L2 /2 width=3 by rsx_lpx_trans/ qed-. @@ -37,11 +37,11 @@ qed-. (* Eliminators with unbound rt-computation for full local environments ******) lemma rsx_ind_lpxs_reqx (h) (G) (T) (Q:predicate lenv): - (∀L1. G ⊢ ⬈*[h,T] 𝐒❪L1❫ → - (∀L2. ❪G,L1❫ ⊢ ⬈*[h] L2 → (L1 ≛[T] L2 → ⊥) → Q L2) → - Q L1 + (∀L1. G ⊢ ⬈*𝐒[h,T] L1 → + (∀L2. ❪G,L1❫ ⊢ ⬈*[h] L2 → (L1 ≛[T] L2 → ⊥) → Q L2) → + Q L1 ) → - ∀L1. G ⊢ ⬈*[h,T] 𝐒❪L1❫ → + ∀L1. G ⊢ ⬈*𝐒[h,T] L1 → ∀L0. ❪G,L1❫ ⊢ ⬈*[h] L0 → ∀L2. L0 ≛[T] L2 → Q L2. #h #G #T #Q #IH #L1 #H @(rsx_ind … H) -L1 #L1 #HL1 #IH1 #L0 #HL10 #L2 #HL02 @@ -62,11 +62,11 @@ qed-. (* Basic_2A1: uses: lsx_ind_alt *) lemma rsx_ind_lpxs (h) (G) (T) (Q:predicate lenv): - (∀L1. G ⊢ ⬈*[h,T] 𝐒❪L1❫ → - (∀L2. ❪G,L1❫ ⊢ ⬈*[h] L2 → (L1 ≛[T] L2 → ⊥) → Q L2) → - Q L1 + (∀L1. G ⊢ ⬈*𝐒[h,T] L1 → + (∀L2. ❪G,L1❫ ⊢ ⬈*[h] L2 → (L1 ≛[T] L2 → ⊥) → Q L2) → + Q L1 ) → - ∀L. G ⊢ ⬈*[h,T] 𝐒❪L❫ → Q L. + ∀L. G ⊢ ⬈*𝐒[h,T] L → Q L. #h #G #T #Q #IH #L #HL @(rsx_ind_lpxs_reqx … IH … HL) -IH -HL // (**) (* full auto fails *) qed-. @@ -74,10 +74,10 @@ qed-. (* Advanced properties ******************************************************) fact rsx_bind_lpxs_aux (h) (G): - ∀p,I,L1,V. G ⊢ ⬈*[h,V] 𝐒❪L1❫ → - ∀Y,T. G ⊢ ⬈*[h,T] 𝐒❪Y❫ → + ∀p,I,L1,V. G ⊢ ⬈*𝐒[h,V] L1 → + ∀Y,T. G ⊢ ⬈*𝐒[h,T] Y → ∀L2. Y = L2.ⓑ[I]V → ❪G,L1❫ ⊢ ⬈*[h] L2 → - G ⊢ ⬈*[h,ⓑ[p,I]V.T] 𝐒❪L2❫. + G ⊢ ⬈*𝐒[h,ⓑ[p,I]V.T] L2. #h #G #p #I #L1 #V #H @(rsx_ind_lpxs … H) -L1 #L1 #_ #IHL1 #Y #T #H @(rsx_ind_lpxs … H) -Y #Y #HY #IHY #L2 #H #HL12 destruct @@ -95,16 +95,16 @@ qed-. (* Basic_2A1: uses: lsx_bind *) lemma rsx_bind (h) (G): - ∀p,I,L,V. G ⊢ ⬈*[h,V] 𝐒❪L❫ → - ∀T. G ⊢ ⬈*[h,T] 𝐒❪L.ⓑ[I]V❫ → - G ⊢ ⬈*[h,ⓑ[p,I]V.T] 𝐒❪L❫. + ∀p,I,L,V. G ⊢ ⬈*𝐒[h,V] L → + ∀T. G ⊢ ⬈*𝐒[h,T] L.ⓑ[I]V → + G ⊢ ⬈*𝐒[h,ⓑ[p,I]V.T] L. /2 width=3 by rsx_bind_lpxs_aux/ qed. (* Basic_2A1: uses: lsx_flat_lpxs *) lemma rsx_flat_lpxs (h) (G): - ∀I,L1,V. G ⊢ ⬈*[h,V] 𝐒❪L1❫ → - ∀L2,T. G ⊢ ⬈*[h,T] 𝐒❪L2❫ → ❪G,L1❫ ⊢ ⬈*[h] L2 → - G ⊢ ⬈*[h,ⓕ[I]V.T] 𝐒❪L2❫. + ∀I,L1,V. G ⊢ ⬈*𝐒[h,V] L1 → + ∀L2,T. G ⊢ ⬈*𝐒[h,T] L2 → ❪G,L1❫ ⊢ ⬈*[h] L2 → + G ⊢ ⬈*𝐒[h,ⓕ[I]V.T] L2. #h #G #I #L1 #V #H @(rsx_ind_lpxs … H) -L1 #L1 #HL1 #IHL1 #L2 #T #H @(rsx_ind_lpxs … H) -L2 #L2 #HL2 #IHL2 #HL12 @rsx_intro_lpxs @@ -121,15 +121,15 @@ qed-. (* Basic_2A1: uses: lsx_flat *) lemma rsx_flat (h) (G): - ∀I,L,V. G ⊢ ⬈*[h,V] 𝐒❪L❫ → - ∀T. G ⊢ ⬈*[h,T] 𝐒❪L❫ → G ⊢ ⬈*[h,ⓕ[I]V.T] 𝐒❪L❫. + ∀I,L,V. G ⊢ ⬈*𝐒[h,V] L → + ∀T. G ⊢ ⬈*𝐒[h,T] L → G ⊢ ⬈*𝐒[h,ⓕ[I]V.T] L. /2 width=3 by rsx_flat_lpxs/ qed. fact rsx_bind_lpxs_void_aux (h) (G): - ∀p,I,L1,V. G ⊢ ⬈*[h,V] 𝐒❪L1❫ → - ∀Y,T. G ⊢ ⬈*[h,T] 𝐒❪Y❫ → + ∀p,I,L1,V. G ⊢ ⬈*𝐒[h,V] L1 → + ∀Y,T. G ⊢ ⬈*𝐒[h,T] Y → ∀L2. Y = L2.ⓧ → ❪G,L1❫ ⊢ ⬈*[h] L2 → - G ⊢ ⬈*[h,ⓑ[p,I]V.T] 𝐒❪L2❫. + G ⊢ ⬈*𝐒[h,ⓑ[p,I]V.T] L2. #h #G #p #I #L1 #V #H @(rsx_ind_lpxs … H) -L1 #L1 #_ #IHL1 #Y #T #H @(rsx_ind_lpxs … H) -Y #Y #HY #IHY #L2 #H #HL12 destruct @@ -146,7 +146,7 @@ elim (rneqx_inv_bind_void … H) -H [ -IHY | -HY -IHL1 -HL12 ] qed-. lemma rsx_bind_void (h) (G): - ∀p,I,L,V. G ⊢ ⬈*[h,V] 𝐒❪L❫ → - ∀T. G ⊢ ⬈*[h,T] 𝐒❪L.ⓧ❫ → - G ⊢ ⬈*[h,ⓑ[p,I]V.T] 𝐒❪L❫. + ∀p,I,L,V. G ⊢ ⬈*𝐒[h,V] L → + ∀T. G ⊢ ⬈*𝐒[h,T] L.ⓧ → + G ⊢ ⬈*𝐒[h,ⓑ[p,I]V.T] L. /2 width=3 by rsx_bind_lpxs_void_aux/ qed. diff --git a/matita/matita/contribs/lambdadelta/basic_2/rt_computation/rsx_rsx.ma b/matita/matita/contribs/lambdadelta/basic_2/rt_computation/rsx_rsx.ma index 230a56900..5e594b775 100644 --- a/matita/matita/contribs/lambdadelta/basic_2/rt_computation/rsx_rsx.ma +++ b/matita/matita/contribs/lambdadelta/basic_2/rt_computation/rsx_rsx.ma @@ -21,8 +21,8 @@ include "basic_2/rt_computation/rsx.ma". (* Basic_2A1: uses: lsx_lleq_trans *) lemma rsx_reqx_trans (h) (G): - ∀L1,T. G ⊢ ⬈*[h,T] 𝐒❪L1❫ → - ∀L2. L1 ≛[T] L2 → G ⊢ ⬈*[h,T] 𝐒❪L2❫. + ∀L1,T. G ⊢ ⬈*𝐒[h,T] L1 → + ∀L2. L1 ≛[T] L2 → G ⊢ ⬈*𝐒[h,T] L2. #h #G #L1 #T #H @(rsx_ind … H) -L1 #L1 #_ #IHL1 #L2 #HL12 @rsx_intro #L #HL2 #HnL2 elim (reqx_lpx_trans … HL2 … HL12) -HL2 @@ -31,8 +31,8 @@ qed-. (* Basic_2A1: uses: lsx_lpx_trans *) lemma rsx_lpx_trans (h) (G): - ∀L1,T. G ⊢ ⬈*[h,T] 𝐒❪L1❫ → - ∀L2. ❪G,L1❫ ⊢ ⬈[h] L2 → G ⊢ ⬈*[h,T] 𝐒❪L2❫. + ∀L1,T. G ⊢ ⬈*𝐒[h,T] L1 → + ∀L2. ❪G,L1❫ ⊢ ⬈[h] L2 → G ⊢ ⬈*𝐒[h,T] L2. #h #G #L1 #T #H @(rsx_ind … H) -L1 #L1 #HL1 #IHL1 #L2 #HL12 elim (reqx_dec L1 L2 T) /3 width=4 by rsx_reqx_trans/ qed-. diff --git a/matita/matita/contribs/lambdadelta/basic_2/rt_equivalence/cpcs_csx.ma b/matita/matita/contribs/lambdadelta/basic_2/rt_equivalence/cpcs_csx.ma index 849ebebf0..465871f60 100644 --- a/matita/matita/contribs/lambdadelta/basic_2/rt_equivalence/cpcs_csx.ma +++ b/matita/matita/contribs/lambdadelta/basic_2/rt_equivalence/cpcs_csx.ma @@ -22,7 +22,7 @@ include "basic_2/rt_equivalence/cpcs_cprs.ma". (* Basic_1: was: cpcs_dec *) lemma csx_cpcs_dec (h) (G) (L): - ∀T1. ❪G,L❫ ⊢ ⬈*[h] 𝐒❪T1❫ → ∀T2. ❪G,L❫ ⊢ ⬈*[h] 𝐒❪T2❫ → + ∀T1. ❪G,L❫ ⊢ ⬈*𝐒[h] T1 → ∀T2. ❪G,L❫ ⊢ ⬈*𝐒[h] T2 → Decidable … (❪G,L❫ ⊢ T1 ⬌*[h] T2). #h #G #L #T1 #HT1 #T2 #HT2 elim (cprre_total_csx … HT1) -HT1 #U1 #HTU1 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 4b9059643..1aa7d1daa 100644 --- a/matita/matita/contribs/lambdadelta/basic_2/rt_transition/cnx.ma +++ b/matita/matita/contribs/lambdadelta/basic_2/rt_transition/cnx.ma @@ -27,8 +27,8 @@ interpretation (* Basic inversion lemmas ***************************************************) -lemma cnx_inv_abst: ∀h,p,G,L,V,T. ❪G,L❫ ⊢ ⬈[h] 𝐍❪ⓛ[p]V.T❫ → - ❪G,L❫ ⊢ ⬈[h] 𝐍❪V❫ ∧ ❪G,L.ⓛV❫ ⊢ ⬈[h] 𝐍❪T❫. +lemma cnx_inv_abst: ∀h,p,G,L,V,T. ❪G,L❫ ⊢ ⬈𝐍[h] ⓛ[p]V.T → + ∧∧ ❪G,L❫ ⊢ ⬈𝐍[h] V & ❪G,L.ⓛV❫ ⊢ ⬈𝐍[h] T. #h #p #G #L #V1 #T1 #HVT1 @conj [ #V2 #HV2 lapply (HVT1 (ⓛ[p]V2.T1) ?) -HVT1 /2 width=2 by cpx_pair_sn/ -HV2 | #T2 #HT2 lapply (HVT1 (ⓛ[p]V1.T2) ?) -HVT1 /2 width=2 by cpx_bind/ -HT2 @@ -37,8 +37,8 @@ lemma cnx_inv_abst: ∀h,p,G,L,V,T. ❪G,L❫ ⊢ ⬈[h] 𝐍❪ⓛ[p]V.T❫ → qed-. (* Basic_2A1: was: cnx_inv_abbr *) -lemma cnx_inv_abbr_neg: ∀h,G,L,V,T. ❪G,L❫ ⊢ ⬈[h] 𝐍❪-ⓓV.T❫ → - ❪G,L❫ ⊢ ⬈[h] 𝐍❪V❫ ∧ ❪G,L.ⓓV❫ ⊢ ⬈[h] 𝐍❪T❫. +lemma cnx_inv_abbr_neg: ∀h,G,L,V,T. ❪G,L❫ ⊢ ⬈𝐍[h] -ⓓV.T → + ∧∧ ❪G,L❫ ⊢ ⬈𝐍[h] V & ❪G,L.ⓓV❫ ⊢ ⬈𝐍[h] T. #h #G #L #V1 #T1 #HVT1 @conj [ #V2 #HV2 lapply (HVT1 (-ⓓV2.T1) ?) -HVT1 /2 width=2 by cpx_pair_sn/ -HV2 | #T2 #HT2 lapply (HVT1 (-ⓓV1.T2) ?) -HVT1 /2 width=2 by cpx_bind/ -HT2 @@ -47,20 +47,20 @@ lemma cnx_inv_abbr_neg: ∀h,G,L,V,T. ❪G,L❫ ⊢ ⬈[h] 𝐍❪-ⓓV.T❫ → qed-. (* Basic_2A1: was: cnx_inv_eps *) -lemma cnx_inv_cast: ∀h,G,L,V,T. ❪G,L❫ ⊢ ⬈[h] 𝐍❪ⓝV.T❫ → ⊥. +lemma cnx_inv_cast: ∀h,G,L,V,T. ❪G,L❫ ⊢ ⬈𝐍[h] ⓝV.T → ⊥. #h #G #L #V #T #H lapply (H T ?) -H /2 width=6 by cpx_eps, teqx_inv_pair_xy_y/ qed-. (* Basic properties *********************************************************) -lemma cnx_sort: ∀h,G,L,s. ❪G,L❫ ⊢ ⬈[h] 𝐍❪⋆s❫. +lemma cnx_sort: ∀h,G,L,s. ❪G,L❫ ⊢ ⬈𝐍[h] ⋆s. #h #G #L #s #X #H elim (cpx_inv_sort1 … H) -H /2 width=1 by teqx_sort/ qed. -lemma cnx_abst: ∀h,p,G,L,W,T. ❪G,L❫ ⊢ ⬈[h] 𝐍❪W❫ → ❪G,L.ⓛW❫ ⊢ ⬈[h] 𝐍❪T❫ → - ❪G,L❫ ⊢ ⬈[h] 𝐍❪ⓛ[p]W.T❫. +lemma cnx_abst: ∀h,p,G,L,W,T. ❪G,L❫ ⊢ ⬈𝐍[h] W → ❪G,L.ⓛW❫ ⊢ ⬈𝐍[h] T → + ❪G,L❫ ⊢ ⬈𝐍[h] ⓛ[p]W.T. #h #p #G #L #W #T #HW #HT #X #H elim (cpx_inv_abst1 … H) -H #W0 #T0 #HW0 #HT0 #H destruct @teqx_pair [ @HW | @HT ] // (**) (* auto fails because δ-expansion gets in the way *) diff --git a/matita/matita/contribs/lambdadelta/basic_2/rt_transition/cnx_basic.ma b/matita/matita/contribs/lambdadelta/basic_2/rt_transition/cnx_basic.ma index 41cb6dad8..b99b444cc 100644 --- a/matita/matita/contribs/lambdadelta/basic_2/rt_transition/cnx_basic.ma +++ b/matita/matita/contribs/lambdadelta/basic_2/rt_transition/cnx_basic.ma @@ -20,7 +20,8 @@ include "basic_2/rt_transition/cnx.ma". (* Advanced inversion lemmas ************************************************) -lemma cnx_inv_abbr_pos (h) (G) (L): ∀V,T. ❪G,L❫ ⊢ ⬈[h] 𝐍❪+ⓓV.T❫ → ⊥. +lemma cnx_inv_abbr_pos (h) (G) (L): + ∀V,T. ❪G,L❫ ⊢ ⬈𝐍[h] +ⓓV.T → ⊥. #h #G #L #V #U1 #H elim (cpx_subst h G (L.ⓓV) U1 … 0) [|*: /2 width=4 by drops_refl/ ] #U2 #T2 #HU12 #HTU2 elim (teqx_dec U1 U2) #HnU12 [ -HU12 | -HTU2 ] 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 76739178d..a93454c7d 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 @@ -19,8 +19,8 @@ include "basic_2/rt_transition/cnx.ma". (* Advanced properties ******************************************************) -lemma cnx_teqx_trans: ∀h,G,L,T1. ❪G,L❫ ⊢ ⬈[h] 𝐍❪T1❫ → - ∀T2. T1 ≛ T2 → ❪G,L❫ ⊢ ⬈[h] 𝐍❪T2❫. +lemma cnx_teqx_trans: ∀h,G,L,T1. ❪G,L❫ ⊢ ⬈𝐍[h] T1 → + ∀T2. T1 ≛ T2 → ❪G,L❫ ⊢ ⬈𝐍[h] T2. #h #G #L #T1 #HT1 #T2 #HT12 #T #HT2 elim (teqx_cpx_trans … HT12 … HT2) -HT2 #T0 #HT10 #HT0 lapply (HT1 … HT10) -HT1 -HT10 /2 width=5 by teqx_repl/ (**) (* full auto fails *) 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 20b92902e..0f57cbb00 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 @@ -20,12 +20,12 @@ include "basic_2/rt_transition/cnx.ma". (* Properties with generic slicing ******************************************) -lemma cnx_lref_atom: ∀h,G,L,i. ⇩[i] L ≘ ⋆ → ❪G,L❫ ⊢ ⬈[h] 𝐍❪#i❫. +lemma cnx_lref_atom: ∀h,G,L,i. ⇩[i] L ≘ ⋆ → ❪G,L❫ ⊢ ⬈𝐍[h] #i. #h #G #L #i #Hi #X #H elim (cpx_inv_lref1_drops … H) -H // * #I #K #V1 #V2 #HLK lapply (drops_mono … Hi … HLK) -L #H destruct qed. -lemma cnx_lref_unit: ∀h,I,G,L,K,i. ⇩[i] L ≘ K.ⓤ[I] → ❪G,L❫ ⊢ ⬈[h] 𝐍❪#i❫. +lemma cnx_lref_unit: ∀h,I,G,L,K,i. ⇩[i] L ≘ K.ⓤ[I] → ❪G,L❫ ⊢ ⬈𝐍[h] #i. #h #I #G #L #K #i #HLK #X #H elim (cpx_inv_lref1_drops … H) -H // * #Z #Y #V1 #V2 #HLY lapply (drops_mono … HLK … HLY) -L #H destruct qed. @@ -40,7 +40,8 @@ qed-. (* Inversion lemmas with generic slicing ************************************) (* Basic_2A1: was: cnx_inv_delta *) -lemma cnx_inv_lref_pair: ∀h,I,G,L,K,V,i. ⇩[i] L ≘ K.ⓑ[I]V → ❪G,L❫ ⊢ ⬈[h] 𝐍❪#i❫ → ⊥. +lemma cnx_inv_lref_pair: + ∀h,I,G,L,K,V,i. ⇩[i] L ≘ K.ⓑ[I]V → ❪G,L❫ ⊢ ⬈𝐍[h] #i → ⊥. #h #I #G #L #K #V #i #HLK #H elim (lifts_total V (𝐔❨↑i❩)) #W #HVW lapply (H W ?) -H /2 width=7 by cpx_delta_drops/ -HLK 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 ad4afa831..dfee9d0e0 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 @@ -19,8 +19,8 @@ include "basic_2/rt_transition/cnx.ma". (* Inversion lemmas with simple terms ***************************************) -lemma cnx_inv_appl: ∀h,G,L,V,T. ❪G,L❫ ⊢ ⬈[h] 𝐍❪ⓐV.T❫ → - ∧∧ ❪G,L❫ ⊢ ⬈[h] 𝐍❪V❫ & ❪G,L❫ ⊢ ⬈[h] 𝐍❪T❫ & 𝐒❪T❫. +lemma cnx_inv_appl: ∀h,G,L,V,T. ❪G,L❫ ⊢ ⬈𝐍[h] ⓐV.T → + ∧∧ ❪G,L❫ ⊢ ⬈𝐍[h] V & ❪G,L❫ ⊢ ⬈𝐍[h] T & 𝐒❪T❫. #h #G #L #V1 #T1 #HVT1 @and3_intro [ #V2 #HV2 lapply (HVT1 (ⓐV2.T1) ?) -HVT1 /2 width=1 by cpx_pair_sn/ -HV2 #H elim (teqx_inv_pair … H) -H // @@ -39,8 +39,8 @@ qed-. (* Properties with simple terms *********************************************) -lemma cnx_appl_simple: ∀h,G,L,V,T. ❪G,L❫ ⊢ ⬈[h] 𝐍❪V❫ → ❪G,L❫ ⊢ ⬈[h] 𝐍❪T❫ → 𝐒❪T❫ → - ❪G,L❫ ⊢ ⬈[h] 𝐍❪ⓐV.T❫. +lemma cnx_appl_simple: ∀h,G,L,V,T. ❪G,L❫ ⊢ ⬈𝐍[h] V → ❪G,L❫ ⊢ ⬈𝐍[h] T → 𝐒❪T❫ → + ❪G,L❫ ⊢ ⬈𝐍[h] ⓐV.T. #h #G #L #V #T #HV #HT #HS #X #H elim (cpx_inv_appl1_simple … H) -H // #V0 #T0 #HV0 #HT0 #H destruct @teqx_pair [ @HV | @HT ] // (**) (* auto fails because δ-expansion gets in the way *) 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 4a8f9c713..385fa7433 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 @@ -79,16 +79,16 @@ table { } ] [ { "unbound context-sensitive parallel rst-computation" * } { - [ [ "strongly normalizing for closures" ] "fsb" + "( ≥[?] 𝐒❪?,?,?❫ )" "fsb_feqx" + "fsb_aaa" + "fsb_csx" + "fsb_fpbg" * ] + [ [ "strongly normalizing for closures" ] "fsb" + "( ≥𝐒[?] ❪?,?,?❫ )" "fsb_feqx" + "fsb_aaa" + "fsb_csx" + "fsb_fpbg" * ] [ [ "proper for closures" ] "fpbg" + "( ❪?,?,?❫ >[?] ❪?,?,?❫ )" "fpbg_fqup" + "fpbg_cpxs" + "fpbg_lpxs" + "fpbg_fpbs" + "fpbg_fpbg" * ] [ [ "for closures" ] "fpbs" + "( ❪?,?,?❫ ≥[?] ❪?,?,?❫ )" "fpbs_fqup" + "fpbs_fqus" + "fpbs_aaa" + "fpbs_cpx" + "fpbs_fpb" + "fpbs_cpxs" + "fpbs_lpxs" + "fpbs_csx" + "fpbs_fpbs" * ] } ] [ { "unbound context-sensitive parallel rt-computation" * } { [ [ "compatibility for lenvs" ] "jsx" + "( ? ⊢ ? ⊒[?] ? )" "jsx_drops" + "jsx_lsubr" + "jsx_csx" + "jsx_rsx" + "jsx_jsx" * ] - [ [ "strongly normalizing for lenvs on referred entries" ] "rsx" + "( ? ⊢ ⬈*[?,?] 𝐒❪?❫ )" "rsx_length" + "rsx_drops" + "rsx_fqup" + "rsx_cpxs" + "rsx_csx" + "rsx_rsx" * ] - [ [ "strongly normalizing for term vectors" ] "csx_vector" + "( ❪?,?❫ ⊢ ⬈*[?] 𝐒❪?❫ )" "csx_cnx_vector" + "csx_csx_vector" * ] - [ [ "strongly normalizing for terms" ] "csx" + "( ❪?,?❫ ⊢ ⬈*[?] 𝐒❪?❫ )" "csx_simple" + "csx_simple_teqo" + "csx_drops" + "csx_fqus" + "csx_lsubr" + "csx_reqx" + "csx_feqx" + "csx_aaa" + "csx_gcp" + "csx_gcr" + "csx_lpx" + "csx_cnx" + "csx_fpbq" + "csx_cpxs" + "csx_lpxs" + "csx_csx" * ] + [ [ "strongly normalizing for lenvs on referred entries" ] "rsx" + "( ? ⊢ ⬈*𝐒[?,?] ? )" "rsx_length" + "rsx_drops" + "rsx_fqup" + "rsx_cpxs" + "rsx_csx" + "rsx_rsx" * ] + [ [ "strongly normalizing for term vectors" ] "csx_vector" + "( ❪?,?❫ ⊢ ⬈*𝐒[?] ? )" "csx_cnx_vector" + "csx_csx_vector" * ] + [ [ "strongly normalizing for terms" ] "csx" + "( ❪?,?❫ ⊢ ⬈*𝐒[?] ? )" "csx_simple" + "csx_simple_teqo" + "csx_drops" + "csx_fqus" + "csx_lsubr" + "csx_reqx" + "csx_feqx" + "csx_aaa" + "csx_gcp" + "csx_gcr" + "csx_lpx" + "csx_cnx" + "csx_fpbq" + "csx_cpxs" + "csx_lpxs" + "csx_csx" * ] [ [ "for lenvs on all entries" ] "lpxs" + "( ❪?,?❫ ⊢ ⬈*[?] ? )" "lpxs_length" + "lpxs_drops" + "lpxs_reqx" + "lpxs_feqx" + "lpxs_aaa" + "lpxs_lpx" + "lpxs_cpxs" + "lpxs_lpxs" * ] [ [ "for binders" ] "cpxs_ext" + "( ❪?,?❫ ⊢ ? ⬈*[?] ? )" * ] [ [ "for terms" ] "cpxs" + "( ❪?,?❫ ⊢ ? ⬈*[?] ? )" "cpxs_teqx" + "cpxs_teqo" + "cpxs_teqo_vector" + "cpxs_drops" + "cpxs_fqus" + "cpxs_lsubr" + "cpxs_reqx" + "cpxs_feqx" + "cpxs_aaa" + "cpxs_lpx" + "cpxs_cnx" + "cpxs_cpxs" * ] @@ -119,7 +119,7 @@ table { } ] [ { "unbound context-sensitive parallel rt-transition" * } { - [ [ "normal form for terms" ] "cnx" + "( ❪?,?❫ ⊢ ⬈[?] 𝐍❪?❫ )" "cnx_simple" + "cnx_drops" + "cnx_basic" + "cnx_cnx" * ] + [ [ "normal form for terms" ] "cnx" + "( ❪?,?❫ ⊢ ⬈𝐍[?] ? )" "cnx_simple" + "cnx_drops" + "cnx_basic" + "cnx_cnx" * ] [ [ "for lenvs on referred entries" ] "rpx" + "( ❪?,?❫ ⊢ ⬈[?,?] ? )" "rpx_length" + "rpx_drops" + "rpx_fqup" + "rpx_fsle" + "rpx_reqx" + "rpx_lpx" + "rpx_rpx" * ] [ [ "for lenvs on all entries" ] "lpx" + "( ❪?,?❫ ⊢ ⬈[?] ? )" "lpx_length" + "lpx_drops" + "lpx_fquq" + "lpx_fsle" + "lpx_reqx" + "lpx_aaa" * ] [ [ "for binders" ] "cpx_ext" + "( ❪?,?❫ ⊢ ? ⬈[?] ? )" * ] -- 2.39.2