From 69592aa1d0c0d122fb09f11cc53bf4c5a1532fdd Mon Sep 17 00:00:00 2001 From: Ferruccio Guidi Date: Tue, 21 Mar 2017 15:17:27 +0000 Subject: [PATCH] we finally understood what tsts is, :) so we renamed it as theq --- .../{cpxs_tsts.ma => cpxs_theq.ma} | 12 +-- ...pxs_tsts_vector.ma => cpxs_theq_vector.ma} | 42 ++++---- .../basic_2/rt_computation/csx_aaa.ma | 2 +- .../basic_2/rt_computation/csx_lpx.ma | 1 - .../{csx_tsts.ma => csx_theq.ma} | 13 +-- ...{csx_tsts_vector.ma => csx_theq_vector.ma} | 14 +-- .../basic_2/rt_computation/partial.txt | 4 +- .../basic_2/syntax/{tsts.ma => theq.ma} | 99 ++++++++++--------- .../syntax/{tsts_simple.ma => theq_simple.ma} | 12 ++- ...simple_vector.ma => theq_simple_vector.ma} | 8 +- .../syntax/{tsts_tdeq.ma => theq_tdeq.ma} | 8 +- .../syntax/{tsts_tsts.ma => theq_theq.ma} | 25 ++--- .../lambdadelta/basic_2/web/basic_2_src.tbl | 10 +- 13 files changed, 130 insertions(+), 120 deletions(-) rename matita/matita/contribs/lambdadelta/basic_2/rt_computation/{cpxs_tsts.ma => cpxs_theq.ma} (93%) rename matita/matita/contribs/lambdadelta/basic_2/rt_computation/{cpxs_tsts_vector.ma => cpxs_theq_vector.ma} (87%) rename matita/matita/contribs/lambdadelta/basic_2/rt_computation/{csx_tsts.ma => csx_theq.ma} (84%) rename matita/matita/contribs/lambdadelta/basic_2/rt_computation/{csx_tsts_vector.ma => csx_theq_vector.ma} (92%) rename matita/matita/contribs/lambdadelta/basic_2/syntax/{tsts.ma => theq.ma} (59%) rename matita/matita/contribs/lambdadelta/basic_2/syntax/{tsts_simple.ma => theq_simple.ma} (78%) rename matita/matita/contribs/lambdadelta/basic_2/syntax/{tsts_simple_vector.ma => theq_simple_vector.ma} (86%) rename matita/matita/contribs/lambdadelta/basic_2/syntax/{tsts_tdeq.ma => theq_tdeq.ma} (83%) rename matita/matita/contribs/lambdadelta/basic_2/syntax/{tsts_tsts.ma => theq_theq.ma} (64%) diff --git a/matita/matita/contribs/lambdadelta/basic_2/rt_computation/cpxs_tsts.ma b/matita/matita/contribs/lambdadelta/basic_2/rt_computation/cpxs_theq.ma similarity index 93% rename from matita/matita/contribs/lambdadelta/basic_2/rt_computation/cpxs_tsts.ma rename to matita/matita/contribs/lambdadelta/basic_2/rt_computation/cpxs_theq.ma index e7d1e9ed9..d8a6f77a3 100644 --- a/matita/matita/contribs/lambdadelta/basic_2/rt_computation/cpxs_tsts.ma +++ b/matita/matita/contribs/lambdadelta/basic_2/rt_computation/cpxs_theq.ma @@ -12,14 +12,14 @@ (* *) (**************************************************************************) -include "basic_2/syntax/tsts_tdeq.ma". +include "basic_2/syntax/theq_tdeq.ma". 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 ************) -(* Forward lemmas with same top term structure ******************************) +(* Forward lemmas with head equivalence for terms ***************************) lemma cpxs_fwd_sort: ∀h,o,G,L,U,s. ⦃G, L⦄ ⊢ ⋆s ⬈*[h] U → ⋆s ⩳[h, o] U ∨ ⦃G, L⦄ ⊢ ⋆(next h s) ⬈*[h] U. @@ -48,7 +48,7 @@ qed-. lemma cpxs_fwd_beta: ∀h,o,p,G,L,V,W,T,U. ⦃G, L⦄ ⊢ ⓐV.ⓛ{p}W.T ⬈*[h] U → ⓐV.ⓛ{p}W.T ⩳[h, o] U ∨ ⦃G, L⦄ ⊢ ⓓ{p}ⓝW.V.T ⬈*[h] U. #h #o #p #G #L #V #W #T #U #H elim (cpxs_inv_appl1 … H) -H * -[ #V0 #T0 #_ #_ #H destruct /2 width=1 by tsts_pair, or_introl/ +[ #V0 #T0 #_ #_ #H destruct /2 width=1 by theq_pair, or_introl/ | #b #W0 #T0 #HT0 #HU elim (cpxs_inv_abst1 … HT0) -HT0 #W1 #T1 #HW1 #HT1 #H destruct lapply (lsubr_cpxs_trans … HT1 (L.ⓓⓝW.V) ?) -HT1 @@ -63,7 +63,7 @@ lemma cpxs_fwd_theta: ∀h,o,p,G,L,V1,V,T,U. ⦃G, L⦄ ⊢ ⓐV1.ⓓ{p}V.T ⬈* ⦃G, L⦄ ⊢ ⓓ{p}V.ⓐV2.T ⬈*[h] U. #h #o #p #G #L #V1 #V #T #U #H #V2 #HV12 elim (cpxs_inv_appl1 … H) -H * -[ -HV12 #V0 #T0 #_ #_ #H destruct /2 width=1 by tsts_pair, or_introl/ +[ -HV12 #V0 #T0 #_ #_ #H destruct /2 width=1 by theq_pair, or_introl/ | #q #W #T0 #HT0 #HU elim (cpxs_inv_abbr1 … HT0) -HT0 * [ #V3 #T3 #_ #_ #H destruct @@ -95,9 +95,9 @@ lemma cpxs_fwd_cast: ∀h,o,G,L,W,T,U. ⦃G, L⦄ ⊢ ⓝW.T ⬈*[h] U → ∨∨ ⓝW. T ⩳[h, o] U | ⦃G, L⦄ ⊢ T ⬈*[h] U | ⦃G, L⦄ ⊢ W ⬈*[h] U. #h #o #G #L #W #T #U #H elim (cpxs_inv_cast1 … H) -H /2 width=1 by or3_intro1, or3_intro2/ * -#W0 #T0 #_ #_ #H destruct /2 width=1 by tsts_pair, or3_intro0/ +#W0 #T0 #_ #_ #H destruct /2 width=1 by theq_pair, or3_intro0/ qed-. lemma cpxs_fwd_cnx: ∀h,o,G,L,T. ⦃G, L⦄ ⊢ ⬈[h, o] 𝐍⦃T⦄ → ∀U. ⦃G, L⦄ ⊢ T ⬈*[h] U → T ⩳[h, o] U. -/3 width=4 by cpxs_inv_cnx1, tdeq_tsts/ qed-. +/3 width=4 by cpxs_inv_cnx1, tdeq_theq/ qed-. diff --git a/matita/matita/contribs/lambdadelta/basic_2/rt_computation/cpxs_tsts_vector.ma b/matita/matita/contribs/lambdadelta/basic_2/rt_computation/cpxs_theq_vector.ma similarity index 87% rename from matita/matita/contribs/lambdadelta/basic_2/rt_computation/cpxs_tsts_vector.ma rename to matita/matita/contribs/lambdadelta/basic_2/rt_computation/cpxs_theq_vector.ma index cf7cdba9d..4d7cf8baf 100644 --- a/matita/matita/contribs/lambdadelta/basic_2/rt_computation/cpxs_tsts_vector.ma +++ b/matita/matita/contribs/lambdadelta/basic_2/rt_computation/cpxs_theq_vector.ma @@ -12,30 +12,30 @@ (* *) (**************************************************************************) -include "basic_2/syntax/tsts_simple_vector.ma". +include "basic_2/syntax/theq_simple_vector.ma". include "basic_2/relocation/lifts_vector.ma". -include "basic_2/rt_computation/cpxs_tsts.ma". +include "basic_2/rt_computation/cpxs_theq.ma". (* UNCOUNTED CONTEXT-SENSITIVE PARALLEL RT-COMPUTATION FOR TERMS ************) -(* Vector form of forward lemmas with same top term structure ***************) +(* Vector form of forward lemmas with head equivalence for terms ************) lemma cpxs_fwd_sort_vector: ∀h,o,G,L,s,Vs,U. ⦃G, L⦄ ⊢ ⒶVs.⋆s ⬈*[h] U → ⒶVs.⋆s ⩳[h, o] U ∨ ⦃G, L⦄ ⊢ ⒶVs.⋆(next h s) ⬈*[h] U. #h #o #G #L #s #Vs elim Vs -Vs /2 width=1 by cpxs_fwd_sort/ #V #Vs #IHVs #U #H elim (cpxs_inv_appl1 … H) -H * -[ -IHVs #V1 #T1 #_ #_ #H destruct /2 width=1 by tsts_pair, or_introl/ +[ -IHVs #V1 #T1 #_ #_ #H destruct /2 width=1 by theq_pair, or_introl/ | #p #W1 #T1 #HT1 #HU elim (IHVs … HT1) -IHVs -HT1 #HT1 - [ elim (tsts_inv_applv_bind_simple … HT1) // + [ elim (theq_inv_applv_bind_simple … HT1) // | @or_intror (**) (* explicit constructor *) @(cpxs_trans … HU) -U @(cpxs_strap1 … (ⓐV.ⓛ{p}W1.T1)) /3 width=1 by cpxs_flat_dx, cpx_beta/ ] | #p #V1 #V2 #V3 #T1 #HV01 #HV12 #HT1 #HU elim (IHVs … HT1) -IHVs -HT1 #HT1 - [ elim (tsts_inv_applv_bind_simple … HT1) // + [ elim (theq_inv_applv_bind_simple … HT1) // | @or_intror (**) (* explicit constructor *) @(cpxs_trans … HU) -U @(cpxs_strap1 … (ⓐV1.ⓓ{p}V3.T1)) /3 width=3 by cpxs_flat, cpx_theta/ @@ -51,17 +51,17 @@ lemma cpxs_fwd_delta_drops_vector: ∀h,o,I,G,L,K,V1,i. ⬇*[i] L ≡ K.ⓑ{I}V1 #h #o #I #G #L #K #V1 #i #HLK #V2 #HV12 #Vs elim Vs -Vs /2 width=5 by cpxs_fwd_delta_drops/ #V #Vs #IHVs #U #H -K -V1 elim (cpxs_inv_appl1 … H) -H * -[ -IHVs #V0 #T0 #_ #_ #H destruct /2 width=1 by tsts_pair, or_introl/ +[ -IHVs #V0 #T0 #_ #_ #H destruct /2 width=1 by theq_pair, or_introl/ | #q #W0 #T0 #HT0 #HU elim (IHVs … HT0) -IHVs -HT0 #HT0 - [ elim (tsts_inv_applv_bind_simple … HT0) // + [ elim (theq_inv_applv_bind_simple … HT0) // | @or_intror -i (**) (* explicit constructor *) @(cpxs_trans … HU) -U @(cpxs_strap1 … (ⓐV.ⓛ{q}W0.T0)) /3 width=1 by cpxs_flat_dx, cpx_beta/ ] | #q #V0 #V1 #V3 #T0 #HV0 #HV01 #HT0 #HU elim (IHVs … HT0) -IHVs -HT0 #HT0 - [ elim (tsts_inv_applv_bind_simple … HT0) // + [ elim (theq_inv_applv_bind_simple … HT0) // | @or_intror -i (**) (* explicit constructor *) @(cpxs_trans … HU) -U @(cpxs_strap1 … (ⓐV0.ⓓ{q}V3.T0)) /3 width=3 by cpxs_flat, cpx_theta/ @@ -75,17 +75,17 @@ lemma cpxs_fwd_beta_vector: ∀h,o,p,G,L,Vs,V,W,T,U. ⦃G, L⦄ ⊢ ⒶVs.ⓐV. #h #o #p #G #L #Vs elim Vs -Vs /2 width=1 by cpxs_fwd_beta/ #V0 #Vs #IHVs #V #W #T #U #H elim (cpxs_inv_appl1 … H) -H * -[ -IHVs #V1 #T1 #_ #_ #H destruct /2 width=1 by tsts_pair, or_introl/ +[ -IHVs #V1 #T1 #_ #_ #H destruct /2 width=1 by theq_pair, or_introl/ | #q #W1 #T1 #HT1 #HU elim (IHVs … HT1) -IHVs -HT1 #HT1 - [ elim (tsts_inv_applv_bind_simple … HT1) // + [ elim (theq_inv_applv_bind_simple … HT1) // | @or_intror (**) (* explicit constructor *) @(cpxs_trans … HU) -U @(cpxs_strap1 … (ⓐV0.ⓛ{q}W1.T1)) /3 width=1 by cpxs_flat_dx, cpx_beta/ ] | #q #V1 #V2 #V3 #T1 #HV01 #HV12 #HT1 #HU elim (IHVs … HT1) -IHVs -HT1 #HT1 - [ elim (tsts_inv_applv_bind_simple … HT1) // + [ elim (theq_inv_applv_bind_simple … HT1) // | @or_intror (**) (* explicit constructor *) @(cpxs_trans … HU) -U @(cpxs_strap1 … (ⓐV1.ⓓ{q}V3.T1)) /3 width=3 by cpxs_flat, cpx_theta/ @@ -105,11 +105,11 @@ generalize in match V1a; -V1a elim HV12b -V1b -V2b /2 width=1 by cpxs_fwd_theta/ #V1b #V2b #V1b #V2b #HV12b #_ #IHV12b #V1a #V2a #HV12a #V #T #U #H elim (cpxs_inv_appl1 … H) -H * -[ -IHV12b -HV12a -HV12b #V0 #T0 #_ #_ #H destruct /2 width=1 by tsts_pair, or_introl/ +[ -IHV12b -HV12a -HV12b #V0 #T0 #_ #_ #H destruct /2 width=1 by theq_pair, or_introl/ | #q #W0 #T0 #HT0 #HU elim (IHV12b … HV12b … HT0) -IHV12b -HT0 #HT0 [ -HV12a -HV12b -HU - elim (tsts_inv_pair1 … HT0) #V1 #T1 #H destruct + elim (theq_inv_pair1 … HT0) #V1 #T1 #H destruct | @or_intror -V1b (**) (* explicit constructor *) @(cpxs_trans … HU) -U elim (cpxs_inv_abbr1 … HT0) -HT0 * @@ -124,7 +124,7 @@ elim (cpxs_inv_appl1 … H) -H * | #q #V0a #Va #V0 #T0 #HV10a #HV0a #HT0 #HU elim (IHV12b … HV12b … HT0) -HV12b -IHV12b -HT0 #HT0 [ -HV12a -HV10a -HV0a -HU - elim (tsts_inv_pair1 … HT0) #V1 #T1 #H destruct + elim (theq_inv_pair1 … HT0) #V1 #T1 #H destruct | @or_intror -V1b -V1b (**) (* explicit constructor *) @(cpxs_trans … HU) -U elim (cpxs_inv_abbr1 … HT0) -HT0 * @@ -152,9 +152,9 @@ lemma cpxs_fwd_cast_vector: ∀h,o,G,L,Vs,W,T,U. ⦃G, L⦄ ⊢ ⒶVs.ⓝW.T ⬈ #h #o #G #L #Vs elim Vs -Vs /2 width=1 by cpxs_fwd_cast/ #V #Vs #IHVs #W #T #U #H elim (cpxs_inv_appl1 … H) -H * -[ -IHVs #V0 #T0 #_ #_ #H destruct /2 width=1 by tsts_pair, or3_intro0/ +[ -IHVs #V0 #T0 #_ #_ #H destruct /2 width=1 by theq_pair, or3_intro0/ | #q #W0 #T0 #HT0 #HU elim (IHVs … HT0) -IHVs -HT0 #HT0 - [ elim (tsts_inv_applv_bind_simple … HT0) // + [ elim (theq_inv_applv_bind_simple … HT0) // | @or3_intro1 -W (**) (* explicit constructor *) @(cpxs_trans … HU) -U @(cpxs_strap1 … (ⓐV.ⓛ{q}W0.T0)) /2 width=1 by cpxs_flat_dx, cpx_beta/ @@ -164,7 +164,7 @@ elim (cpxs_inv_appl1 … H) -H * ] | #q #V0 #V1 #V2 #T0 #HV0 #HV01 #HT0 #HU elim (IHVs … HT0) -IHVs -HT0 #HT0 - [ elim (tsts_inv_applv_bind_simple … HT0) // + [ elim (theq_inv_applv_bind_simple … HT0) // | @or3_intro1 -W (**) (* explicit constructor *) @(cpxs_trans … HU) -U @(cpxs_strap1 … (ⓐV0.ⓓ{q}V2.T0)) /2 width=3 by cpxs_flat, cpx_theta/ @@ -181,12 +181,12 @@ lemma cpxs_fwd_cnx_vector: ∀h,o,G,L,T. 𝐒⦃T⦄ → ⦃G, L⦄ ⊢ ⬈[h, o #h #o #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 #U #H elim (cpxs_inv_appl1 … H) -H * -[ -IHVs #V0 #T0 #_ #_ #H destruct /2 width=1 by tsts_pair/ +[ -IHVs #V0 #T0 #_ #_ #H destruct /2 width=1 by theq_pair/ | #p #W0 #T0 #HT0 #HU lapply (IHVs … HT0) -IHVs -HT0 #HT0 - elim (tsts_inv_applv_bind_simple … HT0) // + elim (theq_inv_applv_bind_simple … HT0) // | #p #V1 #V2 #V0 #T0 #HV1 #HV12 #HT0 #HU lapply (IHVs … HT0) -IHVs -HT0 #HT0 - elim (tsts_inv_applv_bind_simple … HT0) // + elim (theq_inv_applv_bind_simple … HT0) // ] qed-. 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 a9d3e4cae..89f226a30 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 @@ -14,7 +14,7 @@ include "basic_2/computation/gcp_aaa.ma". include "basic_2/computation/cpxs_aaa.ma". -include "basic_2/computation/csx_tsts_vector.ma". +include "basic_2/computation/csx_theq_vector.ma". (* CONTEXT-SENSITIVE EXTENDED STRONGLY NORMALIZING TERMS ********************) 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 da5803ae0..8caea5831 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 @@ -12,7 +12,6 @@ (* *) (**************************************************************************) -include "basic_2/syntax/tsts_tsts.ma". include "basic_2/computation/cpxs_cpxs.ma". include "basic_2/computation/csx_alt.ma". include "basic_2/computation/csx_lift.ma". diff --git a/matita/matita/contribs/lambdadelta/basic_2/rt_computation/csx_tsts.ma b/matita/matita/contribs/lambdadelta/basic_2/rt_computation/csx_theq.ma similarity index 84% rename from matita/matita/contribs/lambdadelta/basic_2/rt_computation/csx_tsts.ma rename to matita/matita/contribs/lambdadelta/basic_2/rt_computation/csx_theq.ma index d0c9837c7..83c8fd43e 100644 --- a/matita/matita/contribs/lambdadelta/basic_2/rt_computation/csx_tsts.ma +++ b/matita/matita/contribs/lambdadelta/basic_2/rt_computation/csx_theq.ma @@ -12,18 +12,19 @@ (* *) (**************************************************************************) -include "basic_2/syntax/tsts_simple.ma". -include "basic_2/syntax/tsts_tsts.ma". +include "basic_2/syntax/theq_simple.ma". +include "basic_2/syntax/theq_theq.ma". 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 **********) -(* Properties with same top term structure **********************************) +(* Properties with head equivalence for terms *******************************) (* Basic_1: was just: sn3_appl_appl *) -lemma csx_appl_simple_tsts: ∀h,o,G,L,V. ⦃G, L⦄ ⊢ ⬈*[h, o] 𝐒⦃V⦄ → ∀T1. ⦃G, L⦄ ⊢ ⬈*[h, o] 𝐒⦃T1⦄ → +(* Basic_2A1: was: csx_appl_simple_tsts *) +lemma csx_appl_simple_theq: ∀h,o,G,L,V. ⦃G, L⦄ ⊢ ⬈*[h, o] 𝐒⦃V⦄ → ∀T1. ⦃G, L⦄ ⊢ ⬈*[h, o] 𝐒⦃T1⦄ → (∀T2. ⦃G, L⦄ ⊢ T1 ⬈*[h] T2 → (T1 ⩳[h, o] T2 → ⊥) → ⦃G, L⦄ ⊢ ⬈*[h, o] 𝐒⦃ⓐV.T2⦄) → 𝐒⦃T1⦄ → ⦃G, L⦄ ⊢ ⬈*[h, o] 𝐒⦃ⓐV.T1⦄. #h #o #G #L #V #H @(csx_ind … H) -V @@ -39,8 +40,8 @@ elim (tdneq_inv_pair … H) -H @IHV -IHV /4 width=3 by csx_cpx_trans, cpx_pair_sn/ | -IHV -H1T1 #H1T10 @(csx_cpx_trans … (ⓐV.T0)) /2 width=1 by cpx_flat/ -HLV0 - elim (tsts_dec h o T1 T0) #H2T10 - [ @IHT1 -IHT1 /4 width=5 by cpxs_strap2, cpxs_strap1, tsts_canc_sn, simple_tsts_repl_dx/ + elim (theq_dec h o T1 T0) #H2T10 + [ @IHT1 -IHT1 /4 width=5 by cpxs_strap2, cpxs_strap1, theq_canc_sn, simple_theq_repl_dx/ | -IHT1 -H3T1 -H1T10 /3 width=1 by cpx_cpxs/ ] ] diff --git a/matita/matita/contribs/lambdadelta/basic_2/rt_computation/csx_tsts_vector.ma b/matita/matita/contribs/lambdadelta/basic_2/rt_computation/csx_theq_vector.ma similarity index 92% rename from matita/matita/contribs/lambdadelta/basic_2/rt_computation/csx_tsts_vector.ma rename to matita/matita/contribs/lambdadelta/basic_2/rt_computation/csx_theq_vector.ma index c8250d40c..2c8dda2dc 100644 --- a/matita/matita/contribs/lambdadelta/basic_2/rt_computation/csx_tsts_vector.ma +++ b/matita/matita/contribs/lambdadelta/basic_2/rt_computation/csx_theq_vector.ma @@ -13,7 +13,7 @@ (**************************************************************************) include "basic_2/computation/gcp_cr.ma". -include "basic_2/computation/cpxs_tsts_vector.ma". +include "basic_2/computation/cpxs_theq_vector.ma". include "basic_2/computation/csx_lpx.ma". include "basic_2/computation/csx_vector.ma". @@ -27,7 +27,7 @@ lemma csx_applv_cnx: ∀h,o,G,L,T. 𝐒⦃T⦄ → ⦃G, L⦄ ⊢ ➡[h, o] 𝐍 #h #o #G #L #T #H1T #H2T #Vs elim Vs -Vs [ #_ @(cnx_csx … H2T) ] (**) (* /2 width=1/ does not work *) #V #Vs #IHV #H elim (csxv_inv_cons … H) -H #HV #HVs -@csx_appl_simple_tsts /2 width=1 by applv_simple/ -IHV -HV -HVs +@csx_appl_simple_theq /2 width=1 by applv_simple/ -IHV -HV -HVs #X #H #H0 lapply (cpxs_fwd_cnx_vector … H) -H // -H1T -H2T #H elim (H0) -H0 // @@ -40,7 +40,7 @@ lemma csx_applv_sort: ∀h,o,G,L,s,Vs. ⦃G, L⦄ ⊢ ⬊*[h, o] Vs → ⦃G, L #Hkd #Vs elim Vs -Vs /2 width=1 by/ #V #Vs #IHVs #HVVs elim (csxv_inv_cons … HVVs) #HV #HVs -@csx_appl_simple_tsts /2 width=1 by applv_simple, simple_atom/ -IHVs -HV -HVs +@csx_appl_simple_theq /2 width=1 by applv_simple, simple_atom/ -IHVs -HV -HVs #X #H #H0 elim (cpxs_fwd_sort_vector … H) -H #H [ elim H0 -H0 // @@ -55,7 +55,7 @@ lemma csx_applv_beta: ∀h,o,a,G,L,Vs,V,W,T. ⦃G, L⦄ ⊢ ⬊*[h, o] ⒶVs.ⓓ #V0 #Vs #IHV #V #W #T #H1T lapply (csx_fwd_pair_sn … H1T) #HV0 lapply (csx_fwd_flat_dx … H1T) #H2T -@csx_appl_simple_tsts /2 width=1 by applv_simple, simple_flat/ -IHV -HV0 -H2T +@csx_appl_simple_theq /2 width=1 by applv_simple, simple_flat/ -IHV -HV0 -H2T #X #H #H0 elim (cpxs_fwd_beta_vector … H) -H #H [ -H1T elim H0 -H0 // @@ -71,7 +71,7 @@ lemma csx_applv_delta: ∀h,o,I,G,L,K,V1,i. ⬇[i] L ≡ K.ⓑ{I}V1 → | #V #Vs #IHV #H1T lapply (csx_fwd_pair_sn … H1T) #HV lapply (csx_fwd_flat_dx … H1T) #H2T - @csx_appl_simple_tsts /2 width=1 by applv_simple, simple_atom/ -IHV -HV -H2T + @csx_appl_simple_theq /2 width=1 by applv_simple, simple_atom/ -IHV -HV -H2T #X #H #H0 elim (cpxs_fwd_delta_vector … HLK … HV12 … H) -HLK -HV12 -H #H [ -H1T elim H0 -H0 // @@ -92,7 +92,7 @@ elim H -V1b -V2b /2 width=3 by csx_appl_theta/ lapply (csx_appl_theta … HW12 … H) -H -HW12 #H lapply (csx_fwd_pair_sn … H) #HW1 lapply (csx_fwd_flat_dx … H) #H1 -@csx_appl_simple_tsts /2 width=3 by simple_flat/ -IHV12b -HW1 -H1 #X #H1 #H2 +@csx_appl_simple_theq /2 width=3 by simple_flat/ -IHV12b -HW1 -H1 #X #H1 #H2 elim (cpxs_fwd_theta_vector … (V2@V2b) … H1) -H1 /2 width=1 by liftv_cons/ -HV12b -HV12 [ -H #H elim H2 -H2 // | -H2 /3 width=5 by csx_cpxs_trans, cpxs_flat_dx/ @@ -107,7 +107,7 @@ lemma csx_applv_cast: ∀h,o,G,L,Vs,W,T. ⦃G, L⦄ ⊢ ⬊*[h, o] ⒶVs.W → lapply (csx_fwd_pair_sn … H1W) #HV lapply (csx_fwd_flat_dx … H1W) #H2W lapply (csx_fwd_flat_dx … H1T) #H2T -@csx_appl_simple_tsts /2 width=1 by applv_simple, simple_flat/ -IHV -HV -H2W -H2T +@csx_appl_simple_theq /2 width=1 by applv_simple, simple_flat/ -IHV -HV -H2W -H2T #X #H #H0 elim (cpxs_fwd_cast_vector … H) -H #H [ -H1W -H1T elim H0 -H0 // 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 0ff5a431f..5136af26a 100644 --- a/matita/matita/contribs/lambdadelta/basic_2/rt_computation/partial.txt +++ b/matita/matita/contribs/lambdadelta/basic_2/rt_computation/partial.txt @@ -1,4 +1,4 @@ -cpxs.ma cpxs_tdeq.ma cpxs_tsts.ma cpxs_tsts_vector.ma cpxs_drops.ma cpxs_lsubr.ma cpxs_lfpx.ma cpxs_cnx.ma cpxs_cpxs.ma +cpxs.ma cpxs_tdeq.ma cpxs_theq.ma cpxs_theq_vector.ma cpxs_drops.ma cpxs_lsubr.ma cpxs_lfpx.ma cpxs_cnx.ma cpxs_cpxs.ma lfpxs.ma lfpxs_fqup.ma lfpxs_cpxs.ma -csx.ma csx_simple.ma csx_tsts.ma csx_drops.ma csx_gcp.ma csx_cnx.ma csx_cpxs.ma csx_csx.ma +csx.ma csx_simple.ma csx_theq.ma csx_drops.ma csx_gcp.ma csx_cnx.ma csx_cpxs.ma csx_csx.ma csx_vector.ma diff --git a/matita/matita/contribs/lambdadelta/basic_2/syntax/tsts.ma b/matita/matita/contribs/lambdadelta/basic_2/syntax/theq.ma similarity index 59% rename from matita/matita/contribs/lambdadelta/basic_2/syntax/tsts.ma rename to matita/matita/contribs/lambdadelta/basic_2/syntax/theq.ma index 6ea5dc782..a09a53533 100644 --- a/matita/matita/contribs/lambdadelta/basic_2/syntax/tsts.ma +++ b/matita/matita/contribs/lambdadelta/basic_2/syntax/theq.ma @@ -16,21 +16,21 @@ include "basic_2/notation/relations/topiso_4.ma". include "basic_2/syntax/item_sd.ma". include "basic_2/syntax/term.ma". -(* SAME TOP TERM STRUCTURE **************************************************) - -(* Basic_2A1: includes: tsts_atom *) -inductive tsts (h) (o): relation term ≝ -| tsts_sort: ∀s1,s2,d. deg h o s1 d → deg h o s2 d → tsts h o (⋆s1) (⋆s2) -| tsts_lref: ∀i. tsts h o (#i) (#i) -| tsts_gref: ∀l. tsts h o (§l) (§l) -| tsts_pair: ∀I,V1,V2,T1,T2. tsts h o (②{I}V1.T1) (②{I}V2.T2) +(* HEAD EQUIVALENCE FOR TERMS ***********************************************) + +(* Basic_2A1: includes: tsts_atom tsts_pair *) +inductive theq (h) (o): relation term ≝ +| theq_sort: ∀s1,s2,d. deg h o s1 d → deg h o s2 d → theq h o (⋆s1) (⋆s2) +| theq_lref: ∀i. theq h o (#i) (#i) +| theq_gref: ∀l. theq h o (§l) (§l) +| theq_pair: ∀I,V1,V2,T1,T2. theq h o (②{I}V1.T1) (②{I}V2.T2) . -interpretation "same top structure (term)" 'TopIso h o T1 T2 = (tsts h o T1 T2). +interpretation "head equivalence (term)" 'TopIso h o T1 T2 = (theq h o T1 T2). (* Basic inversion lemmas ***************************************************) -fact tsts_inv_sort1_aux: ∀h,o,X,Y. X ⩳[h, o] Y → ∀s1. X = ⋆s1 → +fact theq_inv_sort1_aux: ∀h,o,X,Y. X ⩳[h, o] Y → ∀s1. X = ⋆s1 → ∃∃s2,d. deg h o s1 d & deg h o s2 d & Y = ⋆s2. #h #o #X #Y * -X -Y [ #s1 #s2 #d #Hs1 #Hs2 #s #H destruct /2 width=5 by ex3_2_intro/ @@ -41,11 +41,11 @@ fact tsts_inv_sort1_aux: ∀h,o,X,Y. X ⩳[h, o] Y → ∀s1. X = ⋆s1 → qed-. (* Basic_1: was just: iso_gen_sort *) -lemma tsts_inv_sort1: ∀h,o,Y,s1. ⋆s1 ⩳[h, o] Y → +lemma theq_inv_sort1: ∀h,o,Y,s1. ⋆s1 ⩳[h, o] Y → ∃∃s2,d. deg h o s1 d & deg h o s2 d & Y = ⋆s2. -/2 width=3 by tsts_inv_sort1_aux/ qed-. +/2 width=3 by theq_inv_sort1_aux/ qed-. -fact tsts_inv_lref1_aux: ∀h,o,X,Y. X ⩳[h, o] Y → ∀i. X = #i → Y = #i. +fact theq_inv_lref1_aux: ∀h,o,X,Y. X ⩳[h, o] Y → ∀i. X = #i → Y = #i. #h #o #X #Y * -X -Y // [ #s1 #s2 #d #_ #_ #j #H destruct | #I #V1 #V2 #T1 #T2 #j #H destruct @@ -53,20 +53,20 @@ fact tsts_inv_lref1_aux: ∀h,o,X,Y. X ⩳[h, o] Y → ∀i. X = #i → Y = #i. qed-. (* Basic_1: was: iso_gen_lref *) -lemma tsts_inv_lref1: ∀h,o,Y,i. #i ⩳[h, o] Y → Y = #i. -/2 width=5 by tsts_inv_lref1_aux/ qed-. +lemma theq_inv_lref1: ∀h,o,Y,i. #i ⩳[h, o] Y → Y = #i. +/2 width=5 by theq_inv_lref1_aux/ qed-. -fact tsts_inv_gref1_aux: ∀h,o,X,Y. X ⩳[h, o] Y → ∀l. X = §l → Y = §l. +fact theq_inv_gref1_aux: ∀h,o,X,Y. X ⩳[h, o] Y → ∀l. X = §l → Y = §l. #h #o #X #Y * -X -Y // [ #s1 #s2 #d #_ #_ #k #H destruct | #I #V1 #V2 #T1 #T2 #k #H destruct ] qed-. -lemma tsts_inv_gref1: ∀h,o,Y,l. §l ⩳[h, o] Y → Y = §l. -/2 width=5 by tsts_inv_gref1_aux/ qed-. +lemma theq_inv_gref1: ∀h,o,Y,l. §l ⩳[h, o] Y → Y = §l. +/2 width=5 by theq_inv_gref1_aux/ qed-. -fact tsts_inv_pair1_aux: ∀h,o,T1,T2. T1 ⩳[h, o] T2 → +fact theq_inv_pair1_aux: ∀h,o,T1,T2. T1 ⩳[h, o] T2 → ∀J,W1,U1. T1 = ②{J}W1.U1 → ∃∃W2,U2. T2 = ②{J}W2.U2. #h #o #T1 #T2 * -T1 -T2 @@ -78,11 +78,12 @@ fact tsts_inv_pair1_aux: ∀h,o,T1,T2. T1 ⩳[h, o] T2 → qed-. (* Basic_1: was: iso_gen_head *) -lemma tsts_inv_pair1: ∀h,o,J,W1,U1,T2. ②{J}W1.U1 ⩳[h, o] T2 → +(* Basic_2A1: was: tsts_inv_pair1 *) +lemma theq_inv_pair1: ∀h,o,J,W1,U1,T2. ②{J}W1.U1 ⩳[h, o] T2 → ∃∃W2,U2. T2 = ②{J}W2. U2. -/2 width=7 by tsts_inv_pair1_aux/ qed-. +/2 width=7 by theq_inv_pair1_aux/ qed-. -fact tsts_inv_pair2_aux: ∀h,o,T1,T2. T1 ⩳[h, o] T2 → +fact theq_inv_pair2_aux: ∀h,o,T1,T2. T1 ⩳[h, o] T2 → ∀J,W2,U2. T2 = ②{J}W2.U2 → ∃∃W1,U1. T1 = ②{J}W1.U1. #h #o #T1 #T2 * -T1 -T2 @@ -93,80 +94,84 @@ fact tsts_inv_pair2_aux: ∀h,o,T1,T2. T1 ⩳[h, o] T2 → ] qed-. -lemma tsts_inv_pair2: ∀h,o,J,T1,W2,U2. T1 ⩳[h, o] ②{J}W2.U2 → +(* Basic_2A1: was: tsts_inv_pair2 *) +lemma theq_inv_pair2: ∀h,o,J,T1,W2,U2. T1 ⩳[h, o] ②{J}W2.U2 → ∃∃W1,U1. T1 = ②{J}W1.U1. -/2 width=7 by tsts_inv_pair2_aux/ qed-. +/2 width=7 by theq_inv_pair2_aux/ qed-. (* Advanced inversion lemmas ************************************************) -lemma tsts_inv_sort1_deg: ∀h,o,Y,s1. ⋆s1 ⩳[h, o] Y → ∀d. deg h o s1 d → +lemma theq_inv_sort1_deg: ∀h,o,Y,s1. ⋆s1 ⩳[h, o] Y → ∀d. deg h o s1 d → ∃∃s2. deg h o s2 d & Y = ⋆s2. -#h #o #Y #s1 #H #d #Hs1 elim (tsts_inv_sort1 … H) -H +#h #o #Y #s1 #H #d #Hs1 elim (theq_inv_sort1 … H) -H #s2 #x #Hx <(deg_mono h o … Hx … Hs1) -s1 -d /2 width=3 by ex2_intro/ qed-. -lemma tsts_inv_sort_deg: ∀h,o,s1,s2. ⋆s1 ⩳[h, o] ⋆s2 → +lemma theq_inv_sort_deg: ∀h,o,s1,s2. ⋆s1 ⩳[h, o] ⋆s2 → ∀d1,d2. deg h o s1 d1 → deg h o s2 d2 → d1 = d2. #h #o #s1 #y #H #d1 #d2 #Hs1 #Hy -elim (tsts_inv_sort1_deg … H … Hs1) -s1 #s2 #Hs2 #H destruct +elim (theq_inv_sort1_deg … H … Hs1) -s1 #s2 #Hs2 #H destruct <(deg_mono h o … Hy … Hs2) -s2 -d1 // qed-. -lemma tsts_inv_pair: ∀h,o,I1,I2,V1,V2,T1,T2. ②{I1}V1.T1 ⩳[h, o] ②{I2}V2.T2 → +lemma theq_inv_pair: ∀h,o,I1,I2,V1,V2,T1,T2. ②{I1}V1.T1 ⩳[h, o] ②{I2}V2.T2 → I1 = I2. -#h #o #I1 #I2 #V1 #V2 #T1 #T2 #H elim (tsts_inv_pair1 … H) -H +#h #o #I1 #I2 #V1 #V2 #T1 #T2 #H elim (theq_inv_pair1 … H) -H #V0 #T0 #H destruct // qed-. (* Basic properties *********************************************************) (* Basic_1: was: iso_refl *) -lemma tsts_refl: ∀h,o. reflexive … (tsts h o). +(* Basic_2A1: was: tsts_refl *) +lemma theq_refl: ∀h,o. reflexive … (theq h o). #h #o * // -* /2 width=1 by tsts_lref, tsts_gref/ -#s elim (deg_total h o s) /2 width=3 by tsts_sort/ +* /2 width=1 by theq_lref, theq_gref/ +#s elim (deg_total h o s) /2 width=3 by theq_sort/ qed. -lemma tsts_sym: ∀h,o. symmetric … (tsts h o). -#h #o #T1 #T2 * -T1 -T2 /2 width=3 by tsts_sort/ +(* Basic_2A1: was: tsts_sym *) +lemma theq_sym: ∀h,o. symmetric … (theq h o). +#h #o #T1 #T2 * -T1 -T2 /2 width=3 by theq_sort/ qed-. -lemma tsts_dec: ∀h,o,T1,T2. Decidable (T1 ⩳[h, o] T2). +(* Basic_2A1: was: tsts_dec *) +lemma theq_dec: ∀h,o,T1,T2. Decidable (T1 ⩳[h, o] T2). #h #o * [ * #s1 | #I1 #V1 #T1 ] * [1,3,5,7: * #s2 |*: #I2 #V2 #T2 ] [ elim (deg_total h o s1) #d1 #H1 elim (deg_total h o s2) #d2 #H2 - elim (eq_nat_dec d1 d2) #Hd12 destruct /3 width=3 by tsts_sort, or_introl/ + elim (eq_nat_dec d1 d2) #Hd12 destruct /3 width=3 by theq_sort, or_introl/ @or_intror #H - lapply (tsts_inv_sort_deg … H … H1 H2) -H -H1 -H2 /2 width=1 by/ + lapply (theq_inv_sort_deg … H … H1 H2) -H -H1 -H2 /2 width=1 by/ |2,3,13: @or_intror #H - elim (tsts_inv_sort1 … H) -H #x1 #x2 #_ #_ #H destruct + elim (theq_inv_sort1 … H) -H #x1 #x2 #_ #_ #H destruct |4,6,14: @or_intror #H - lapply (tsts_inv_lref1 … H) -H #H destruct + lapply (theq_inv_lref1 … H) -H #H destruct |5: elim (eq_nat_dec s1 s2) #Hs12 destruct /2 width=1 by or_introl/ @or_intror #H - lapply (tsts_inv_lref1 … H) -H #H destruct /2 width=1 by/ + lapply (theq_inv_lref1 … H) -H #H destruct /2 width=1 by/ |7,8,15: @or_intror #H - lapply (tsts_inv_gref1 … H) -H #H destruct + lapply (theq_inv_gref1 … H) -H #H destruct |9: elim (eq_nat_dec s1 s2) #Hs12 destruct /2 width=1 by or_introl/ @or_intror #H - lapply (tsts_inv_gref1 … H) -H #H destruct /2 width=1 by/ + lapply (theq_inv_gref1 … H) -H #H destruct /2 width=1 by/ |10,11,12: @or_intror #H - elim (tsts_inv_pair1 … H) -H #X1 #X2 #H destruct + elim (theq_inv_pair1 … H) -H #X1 #X2 #H destruct |16: elim (eq_item2_dec I1 I2) #HI12 destruct - [ /3 width=1 by tsts_pair, or_introl/ ] + [ /3 width=1 by theq_pair, or_introl/ ] @or_intror #H - lapply (tsts_inv_pair … H) -H /2 width=1 by/ + lapply (theq_inv_pair … H) -H /2 width=1 by/ ] qed-. -(* Basic_2A1: removed theorems 4: +(* Basic_2A1: removed theorems 2: tsts_inv_atom1 tsts_inv_atom2 *) diff --git a/matita/matita/contribs/lambdadelta/basic_2/syntax/tsts_simple.ma b/matita/matita/contribs/lambdadelta/basic_2/syntax/theq_simple.ma similarity index 78% rename from matita/matita/contribs/lambdadelta/basic_2/syntax/tsts_simple.ma rename to matita/matita/contribs/lambdadelta/basic_2/syntax/theq_simple.ma index fe3613e8d..a260edd75 100644 --- a/matita/matita/contribs/lambdadelta/basic_2/syntax/tsts_simple.ma +++ b/matita/matita/contribs/lambdadelta/basic_2/syntax/theq_simple.ma @@ -13,17 +13,19 @@ (**************************************************************************) include "basic_2/syntax/term_simple.ma". -include "basic_2/syntax/tsts.ma". +include "basic_2/syntax/theq.ma". -(* SAME TOP TERM STRUCTURE **************************************************) +(* HEAD EQUIVALENCE FOR TERMS ***********************************************) (* Properies with simple (neutral) terms ************************************) -lemma simple_tsts_repl_dx: ∀h,o,T1,T2. T1 ⩳[h, o] T2 → 𝐒⦃T1⦄ → 𝐒⦃T2⦄. +(* Basic_2A1: was: simple_tsts_repl_dx *) +lemma simple_theq_repl_dx: ∀h,o,T1,T2. T1 ⩳[h, o] T2 → 𝐒⦃T1⦄ → 𝐒⦃T2⦄. #h #o #T1 #T2 * -T1 -T2 // #I #V1 #V2 #T1 #T2 #H elim (simple_inv_pair … H) -H #J #H destruct // qed-. -lemma simple_tsts_repl_sn: ∀h,o,T1,T2. T1 ⩳[h, o] T2 → 𝐒⦃T2⦄ → 𝐒⦃T1⦄. -/3 width=5 by simple_tsts_repl_dx, tsts_sym/ qed-. +(* Basic_2A1: was: simple_tsts_repl_sn *) +lemma simple_theq_repl_sn: ∀h,o,T1,T2. T1 ⩳[h, o] T2 → 𝐒⦃T2⦄ → 𝐒⦃T1⦄. +/3 width=5 by simple_theq_repl_dx, theq_sym/ qed-. diff --git a/matita/matita/contribs/lambdadelta/basic_2/syntax/tsts_simple_vector.ma b/matita/matita/contribs/lambdadelta/basic_2/syntax/theq_simple_vector.ma similarity index 86% rename from matita/matita/contribs/lambdadelta/basic_2/syntax/tsts_simple_vector.ma rename to matita/matita/contribs/lambdadelta/basic_2/syntax/theq_simple_vector.ma index 2320a0cf9..a17c97090 100644 --- a/matita/matita/contribs/lambdadelta/basic_2/syntax/tsts_simple_vector.ma +++ b/matita/matita/contribs/lambdadelta/basic_2/syntax/theq_simple_vector.ma @@ -13,17 +13,17 @@ (**************************************************************************) include "basic_2/syntax/term_vector.ma". -include "basic_2/syntax/tsts_simple.ma". +include "basic_2/syntax/theq_simple.ma". -(* SAME TOP TERM STRUCTURE **************************************************) +(* HEAD EQUIVALENCE FOR TERMS ***********************************************) (* Advanced inversion lemmas with simple (neutral) terms ********************) (* Basic_1: was only: iso_flats_lref_bind_false iso_flats_flat_bind_false *) (* Basic_2A1: was: tsts_inv_bind_applv_simple *) -lemma tsts_inv_applv_bind_simple: ∀h,o,p,I,Vs,V2,T1,T2. ⒶVs.T1 ⩳[h, o] ⓑ{p,I}V2.T2 → +lemma theq_inv_applv_bind_simple: ∀h,o,p,I,Vs,V2,T1,T2. ⒶVs.T1 ⩳[h, o] ⓑ{p,I}V2.T2 → 𝐒⦃T1⦄ → ⊥. -#h #o #p #I #Vs #V2 #T1 #T2 #H elim (tsts_inv_pair2 … H) -H +#h #o #p #I #Vs #V2 #T1 #T2 #H elim (theq_inv_pair2 … H) -H #V0 #T0 elim Vs -Vs normalize [ #H destruct #H /2 width=5 by simple_inv_bind/ | #V #Vs #_ #H destruct diff --git a/matita/matita/contribs/lambdadelta/basic_2/syntax/tsts_tdeq.ma b/matita/matita/contribs/lambdadelta/basic_2/syntax/theq_tdeq.ma similarity index 83% rename from matita/matita/contribs/lambdadelta/basic_2/syntax/tsts_tdeq.ma rename to matita/matita/contribs/lambdadelta/basic_2/syntax/theq_tdeq.ma index 08e358784..2a111b40f 100644 --- a/matita/matita/contribs/lambdadelta/basic_2/syntax/tsts_tdeq.ma +++ b/matita/matita/contribs/lambdadelta/basic_2/syntax/theq_tdeq.ma @@ -13,12 +13,12 @@ (**************************************************************************) include "basic_2/syntax/tdeq.ma". -include "basic_2/syntax/tsts.ma". +include "basic_2/syntax/theq.ma". -(* SAME TOP TERM STRUCTURE **************************************************) +(* HEAD EQUIVALENCE FOR TERMS ***********************************************) (* Properties with degree-based equivalence for terms ***********************) -lemma tdeq_tsts: ∀h,o,T1,T2. T1 ≡[h, o] T2 → T1 ⩳[h, o] T2. -#h #o #T1 #T2 * -T1 -T2 /2 width=3 by tsts_sort, tsts_pair/ +lemma tdeq_theq: ∀h,o,T1,T2. T1 ≡[h, o] T2 → T1 ⩳[h, o] T2. +#h #o #T1 #T2 * -T1 -T2 /2 width=3 by theq_sort, theq_pair/ qed. diff --git a/matita/matita/contribs/lambdadelta/basic_2/syntax/tsts_tsts.ma b/matita/matita/contribs/lambdadelta/basic_2/syntax/theq_theq.ma similarity index 64% rename from matita/matita/contribs/lambdadelta/basic_2/syntax/tsts_tsts.ma rename to matita/matita/contribs/lambdadelta/basic_2/syntax/theq_theq.ma index b3c790e53..88547d98e 100644 --- a/matita/matita/contribs/lambdadelta/basic_2/syntax/tsts_tsts.ma +++ b/matita/matita/contribs/lambdadelta/basic_2/syntax/theq_theq.ma @@ -12,26 +12,29 @@ (* *) (**************************************************************************) -include "basic_2/syntax/tsts.ma". +include "basic_2/syntax/theq.ma". -(* SAME TOP TERM STRUCTURE **************************************************) +(* HEAD EQUIVALENCE FOR TERMS ***********************************************) (* Main properties **********************************************************) (* Basic_1: was: iso_trans *) -theorem tsts_trans: ∀h,o. Transitive … (tsts h o). +(* Basic_2A1: was: tsts_trans *) +theorem theq_trans: ∀h,o. Transitive … (theq h o). #h #o #T1 #T * -T1 -T [ #s1 #s #d #Hs1 #Hs #X #H - elim (tsts_inv_sort1_deg … H … Hs) -s /2 width=3 by tsts_sort/ -| #i1 #i #H <(tsts_inv_lref1 … H) -H // -| #l1 #l #H <(tsts_inv_gref1 … H) -H // + elim (theq_inv_sort1_deg … H … Hs) -s /2 width=3 by theq_sort/ +| #i1 #i #H <(theq_inv_lref1 … H) -H // +| #l1 #l #H <(theq_inv_gref1 … H) -H // | #I #V1 #V #T1 #T #X #H - elim (tsts_inv_pair1 … H) -H #V2 #T2 #H destruct // + elim (theq_inv_pair1 … H) -H #V2 #T2 #H destruct // ] qed-. -theorem tsts_canc_sn: ∀h,o. left_cancellable … (tsts h o). -/3 width=3 by tsts_trans, tsts_sym/ qed-. +(* Basic_2A1: was: tsts_canc_sn *) +theorem theq_canc_sn: ∀h,o. left_cancellable … (theq h o). +/3 width=3 by theq_trans, theq_sym/ qed-. -theorem tsts_canc_dx: ∀h,o. right_cancellable … (tsts h o). -/3 width=3 by tsts_trans, tsts_sym/ qed-. +(* Basic_2A1: was: tsts_canc_dx *) +theorem theq_canc_dx: ∀h,o. right_cancellable … (theq h o). +/3 width=3 by theq_trans, theq_sym/ qed-. 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 ed35813d2..efb95c8e3 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 @@ -89,7 +89,7 @@ table { [ { "strongly normalizing rt-computation" * } { [ "lcosx ( ? ⊢ ~⬊*[?,?,?] ? )" "lcosx_cpx" * ] [ "lsx ( ? ⊢ ⬊*[?,?,?,?] ? )" "lsx_alt ( ? ⊢ ⬊⬊*[?,?,?,?] ? )" "lsx_drop" + "lsx_lpx" + "lsx_lpxs" + "llsx_csx" * ] - [ "csx_vector ( ⦃?,?⦄ ⊢ ⬊*[?,?] ? )" "csx_tsts_vector" + "csx_aaa" * ] + [ "csx_vector ( ⦃?,?⦄ ⊢ ⬊*[?,?] ? )" "csx_theq_vector" + "csx_aaa" * ] [ "csx ( ⦃?,?⦄ ⊢ ⬊*[?,?] ? )" "csx_alt ( ⦃?,?⦄ ⊢ ⬊⬊*[?,?] ? )" "csx_lift" + "csx_lleq" + "csx_lpx" + "csx_lpxs" + "csx_fpbs" * ] } ] @@ -114,9 +114,9 @@ table { [ "cpxs_lreq" + "cpxs_lleq" + "cpxs_aaa" * ] *) [ "csx_vector ( ⦃?,?⦄ ⊢ ⬈*[?,?] 𝐒⦃?⦄ )" * ] - [ "csx ( ⦃?,?⦄ ⊢ ⬈*[?,?] 𝐒⦃?⦄ )" "csx_simple" + "csx_tsts" + "csx_drops" + "csx_gcp" + "csx_cnx" + "csx_cpxs" + "csx_csx" * ] + [ "csx ( ⦃?,?⦄ ⊢ ⬈*[?,?] 𝐒⦃?⦄ )" "csx_simple" + "csx_theq" + "csx_drops" + "csx_gcp" + "csx_cnx" + "csx_cpxs" + "csx_csx" * ] [ "lfpxs ( ⦃?,?⦄ ⊢ ⬈*[?,?] ? )" "lfpxs_length" + "lfpxs_fqup" + "lfpxs_cpxs" * ] - [ "cpxs ( ⦃?,?⦄ ⊢ ? ⬈*[?] ? )" "cpxs_tdeq" + "cpxs_tsts" + "cpxs_tsts_vector" + "cpxs_drops" + "cpxs_lsubr" + "cpxs_lfpx" + "cpxs_cnx" + "cpxs_cpxs" * ] + [ "cpxs ( ⦃?,?⦄ ⊢ ? ⬈*[?] ? )" "cpxs_tdeq" + "cpxs_theq" + "cpxs_theq_vector" + "cpxs_drops" + "cpxs_lsubr" + "cpxs_lfpx" + "cpxs_cnx" + "cpxs_cpxs" * ] } ] } @@ -233,8 +233,8 @@ table { [ "append ( ? @@ ? )" "append_length" * ] } ] - [ { "same top term structure" * } { - [ "tsts ( ? ⩳[?,?] ? )" "tsts_simple" + "tsts_tdeq" + "tsts_tsts" + "tsts_simple_vector" * ] + [ { "head equivalence for terms" * } { + [ "theq ( ? ⩳[?,?] ? )" "theq_simple" + "theq_tdeq" + "theq_theq" + "theq_simple_vector" * ] } ] [ { "degree-based equivalence for terms" * } { -- 2.39.2