From 6167cca50de37eba76a062537b24f7caef5b34f2 Mon Sep 17 00:00:00 2001 From: Ferruccio Guidi Date: Tue, 14 Nov 2017 15:07:38 +0000 Subject: [PATCH] - notation change for tdeq and related notions - extra spaces removed in notation files - bug fixed in replace.sh: the case of a wrong sed should be handeled correctly --- .../lambdadelta/basic_2/dynamic/snv_da_lpr.ma | 6 +- .../lambdadelta/basic_2/dynamic/snv_lpr.ma | 8 +- .../lambdadelta/basic_2/dynamic/snv_lstas.ma | 8 +- .../basic_2/dynamic/snv_lstas_lpr.ma | 8 +- .../lambdadelta/basic_2/dynamic/snv_scpes.ma | 72 ++++++++-------- .../basic_2/notation/constructors/dxabbr_2.ma | 2 +- .../basic_2/notation/constructors/dxabst_2.ma | 2 +- .../notation/constructors/dxbind1_2.ma | 2 +- .../notation/constructors/dxbind2_3.ma | 2 +- .../basic_2/notation/constructors/dxitem_2.ma | 2 +- .../basic_2/notation/constructors/dxvoid_1.ma | 2 +- .../basic_2/notation/constructors/snabbr_3.ma | 2 +- .../notation/constructors/snabbrneg_2.ma | 2 +- .../notation/constructors/snabbrpos_2.ma | 2 +- .../basic_2/notation/constructors/snabst_3.ma | 2 +- .../notation/constructors/snabstneg_2.ma | 2 +- .../notation/constructors/snabstpos_2.ma | 2 +- .../basic_2/notation/constructors/snappl_2.ma | 2 +- .../notation/constructors/snbind2_4.ma | 2 +- .../notation/constructors/snbind2neg_3.ma | 2 +- .../notation/constructors/snbind2pos_3.ma | 2 +- .../basic_2/notation/constructors/sncast_2.ma | 2 +- .../notation/constructors/snflat2_3.ma | 2 +- .../notation/constructors/snitem2_2.ma | 2 +- .../notation/constructors/snitem2_3.ma | 2 +- .../basic_2/notation/functions/snabbr_2.ma | 2 +- .../basic_2/notation/functions/snabst_2.ma | 2 +- .../notation/functions/snapplvector_2.ma | 2 +- .../basic_2/notation/functions/snbind1_2.ma | 2 +- .../basic_2/notation/functions/snbind2_3.ma | 2 +- .../basic_2/notation/functions/snitem_2.ma | 2 +- .../basic_2/notation/functions/snvoid_1.ma | 2 +- .../basic_2/notation/functions/weight_2.ma | 2 +- .../basic_2/notation/functions/weight_3.ma | 2 +- .../basic_2/notation/relations/btpred_7.ma | 2 +- .../notation/relations/btpredproper_8.ma | 2 +- .../notation/relations/btpredstar_8.ma | 2 +- .../notation/relations/btpredstaralt_8.ma | 2 +- .../notation/relations/dpconvstar_8.ma | 2 +- .../basic_2/notation/relations/dpredstar_7.ma | 2 +- .../relations/lazybtpredstarproper_8.ma | 2 +- .../notation/relations/nativevalid_5.ma | 2 +- .../notation/relations/nativevalid_6.ma | 2 +- .../basic_2/notation/relations/predsn_5.ma | 2 +- .../notation/relations/predsnstar_3.ma | 2 +- .../notation/relations/predsnstar_5.ma | 2 +- .../basic_2/notation/relations/predstar_4.ma | 2 +- .../basic_2/notation/relations/predstar_6.ma | 2 +- .../basic_2/notation/relations/predty_7.ma | 2 +- .../notation/relations/predtynormal_5.ma | 2 +- .../basic_2/notation/relations/predtysn_5.ma | 2 +- .../notation/relations/predtysnstar_5.ma | 2 +- .../notation/relations/predtysnstrong_5.ma | 2 +- .../notation/relations/predtystrong_5.ma | 2 +- .../basic_2/notation/relations/rdropstar_4.ma | 2 +- .../notation/relations/relationstar_4.ma | 2 +- .../notation/relations/relationstar_5.ma | 2 +- .../notation/relations/relationstarstar_4.ma | 2 +- .../relations/{lazyeq_4.ma => stareq_4.ma} | 4 +- .../relations/{lazyeq_5.ma => stareq_5.ma} | 4 +- .../{lazyeqsn_5.ma => stareqsn_5.ma} | 4 +- .../{lazyeqsn_8.ma => stareqsn_8.ma} | 4 +- .../basic_2/notation/relations/supterm_6.ma | 2 +- .../basic_2/notation/relations/supterm_7.ma | 2 +- .../notation/relations/suptermopt_6.ma | 2 +- .../notation/relations/suptermopt_7.ma | 2 +- .../notation/relations/suptermplus_6.ma | 2 +- .../notation/relations/suptermplus_7.ma | 2 +- .../notation/relations/suptermstar_6.ma | 2 +- .../notation/relations/suptermstar_7.ma | 2 +- .../basic_2/notation/relations/topiso_4.ma | 2 +- .../basic_2/rt_computation/cpxs_cnx.ma | 2 +- .../basic_2/rt_computation/cpxs_fqus.ma | 16 ++-- .../basic_2/rt_computation/cpxs_lfdeq.ma | 12 +-- .../basic_2/rt_computation/cpxs_tdeq.ma | 8 +- .../lambdadelta/basic_2/rt_computation/csx.ma | 4 +- .../basic_2/rt_computation/csx_aaa.ma | 8 +- .../basic_2/rt_computation/csx_cpxs.ma | 8 +- .../basic_2/rt_computation/csx_csx.ma | 2 +- .../basic_2/rt_computation/csx_lfdeq.ma | 4 +- .../basic_2/rt_computation/csx_simple.ma | 2 +- .../basic_2/rt_computation/fpbg.ma | 6 +- .../basic_2/rt_computation/fpbg_fleq.ma | 12 +-- .../basic_2/rt_computation/fpbg_fpbs.ma | 20 ++--- .../basic_2/rt_computation/fpbg_lift.ma | 2 +- .../basic_2/rt_computation/fsb_aaa.ma | 4 +- .../basic_2/rt_computation/fsb_alt.ma | 6 +- .../basic_2/rt_computation/fsb_csx.ma | 2 +- .../basic_2/rt_computation/lfpxs_lfdeq.ma | 8 +- .../basic_2/rt_computation/lfsx.ma | 4 +- .../basic_2/rt_computation/lfsx_lfpxs.ma | 8 +- .../basic_2/rt_computation/lfsx_lfsx.ma | 2 +- .../basic_2/rt_transition/cnx_cnx.ma | 2 +- .../basic_2/rt_transition/cpx_fqus.ma | 16 ++-- .../basic_2/rt_transition/cpx_lfdeq.ma | 2 +- .../lambdadelta/basic_2/rt_transition/fpb.ma | 8 +- .../basic_2/rt_transition/fpb_lfdeq.ma | 4 +- .../basic_2/rt_transition/lfpx_lfdeq.ma | 28 +++---- .../lambdadelta/basic_2/static/aaa_lfdeq.ma | 4 +- .../lambdadelta/basic_2/static/ffdeq.ma | 10 +-- .../lambdadelta/basic_2/static/ffdeq_ffdeq.ma | 4 +- .../lambdadelta/basic_2/static/lfdeq.ma | 82 +++++++++---------- .../lambdadelta/basic_2/static/lfdeq_drops.ma | 12 +-- .../lambdadelta/basic_2/static/lfdeq_fqup.ma | 10 +-- .../lambdadelta/basic_2/static/lfdeq_fqus.ma | 24 +++--- .../basic_2/static/lfdeq_length.ma | 6 +- .../lambdadelta/basic_2/static/lfdeq_lfdeq.ma | 42 +++++----- .../lambdadelta/basic_2/syntax/tdeq.ma | 44 +++++----- .../lambdadelta/basic_2/syntax/tdeq_ext.ma | 8 +- .../lambdadelta/basic_2/syntax/tdeq_tdeq.ma | 12 +-- .../lambdadelta/basic_2/syntax/theq_tdeq.ma | 2 +- .../lambdadelta/basic_2/web/basic_2_src.tbl | 10 +-- matita/matita/contribs/lambdadelta/replace.sh | 8 +- matita/matita/contribs/lambdadelta/restore.sh | 8 ++ 114 files changed, 368 insertions(+), 360 deletions(-) rename matita/matita/contribs/lambdadelta/basic_2/notation/relations/{lazyeq_4.ma => stareq_4.ma} (90%) rename matita/matita/contribs/lambdadelta/basic_2/notation/relations/{lazyeq_5.ma => stareq_5.ma} (88%) rename matita/matita/contribs/lambdadelta/basic_2/notation/relations/{lazyeqsn_5.ma => stareqsn_5.ma} (88%) rename matita/matita/contribs/lambdadelta/basic_2/notation/relations/{lazyeqsn_8.ma => stareqsn_8.ma} (87%) create mode 100644 matita/matita/contribs/lambdadelta/restore.sh diff --git a/matita/matita/contribs/lambdadelta/basic_2/dynamic/snv_da_lpr.ma b/matita/matita/contribs/lambdadelta/basic_2/dynamic/snv_da_lpr.ma index 5f7b2ed20..acaf6f038 100644 --- a/matita/matita/contribs/lambdadelta/basic_2/dynamic/snv_da_lpr.ma +++ b/matita/matita/contribs/lambdadelta/basic_2/dynamic/snv_da_lpr.ma @@ -21,9 +21,9 @@ include "basic_2/dynamic/snv_scpes.ma". (* Properties on degree assignment for terms ********************************) fact da_cpr_lpr_aux: ∀h,o,G0,L0,T0. - (∀G1,L1,T1. ⦃G0, L0, T0⦄ >≡[h, o] ⦃G1, L1, T1⦄ → IH_snv_lstas h o G1 L1 T1) → - (∀G1,L1,T1. ⦃G0, L0, T0⦄ >≡[h, o] ⦃G1, L1, T1⦄ → IH_snv_cpr_lpr h o G1 L1 T1) → - (∀G1,L1,T1. ⦃G0, L0, T0⦄ >≡[h, o] ⦃G1, L1, T1⦄ → IH_da_cpr_lpr h o G1 L1 T1) → + (∀G1,L1,T1. ⦃G0, L0, T0⦄ >≛[h, o] ⦃G1, L1, T1⦄ → IH_snv_lstas h o G1 L1 T1) → + (∀G1,L1,T1. ⦃G0, L0, T0⦄ >≛[h, o] ⦃G1, L1, T1⦄ → IH_snv_cpr_lpr h o G1 L1 T1) → + (∀G1,L1,T1. ⦃G0, L0, T0⦄ >≛[h, o] ⦃G1, L1, T1⦄ → IH_da_cpr_lpr h o G1 L1 T1) → ∀G1,L1,T1. G0 = G1 → L0 = L1 → T0 = T1 → IH_da_cpr_lpr h o G1 L1 T1. #h #o #G0 #L0 #T0 #IH3 #IH2 #IH1 #G1 #L1 * * [|||| * ] [ #s #_ #_ #_ #_ #d #H2 #X3 #H3 #L2 #_ -IH3 -IH2 -IH1 diff --git a/matita/matita/contribs/lambdadelta/basic_2/dynamic/snv_lpr.ma b/matita/matita/contribs/lambdadelta/basic_2/dynamic/snv_lpr.ma index 148f6f148..101a50306 100644 --- a/matita/matita/contribs/lambdadelta/basic_2/dynamic/snv_lpr.ma +++ b/matita/matita/contribs/lambdadelta/basic_2/dynamic/snv_lpr.ma @@ -22,10 +22,10 @@ include "basic_2/dynamic/lsubsv_snv.ma". (* Properties on context-free parallel reduction for local environments *****) fact snv_cpr_lpr_aux: ∀h,o,G0,L0,T0. - (∀G1,L1,T1. ⦃G0, L0, T0⦄ >≡[h, o] ⦃G1, L1, T1⦄ → IH_snv_lstas h o G1 L1 T1) → - (∀G1,L1,T1. ⦃G0, L0, T0⦄ >≡[h, o] ⦃G1, L1, T1⦄ → IH_lstas_cpr_lpr h o G1 L1 T1) → - (∀G1,L1,T1. ⦃G0, L0, T0⦄ >≡[h, o] ⦃G1, L1, T1⦄ → IH_da_cpr_lpr h o G1 L1 T1) → - (∀G1,L1,T1. ⦃G0, L0, T0⦄ >≡[h, o] ⦃G1, L1, T1⦄ → IH_snv_cpr_lpr h o G1 L1 T1) → + (∀G1,L1,T1. ⦃G0, L0, T0⦄ >≛[h, o] ⦃G1, L1, T1⦄ → IH_snv_lstas h o G1 L1 T1) → + (∀G1,L1,T1. ⦃G0, L0, T0⦄ >≛[h, o] ⦃G1, L1, T1⦄ → IH_lstas_cpr_lpr h o G1 L1 T1) → + (∀G1,L1,T1. ⦃G0, L0, T0⦄ >≛[h, o] ⦃G1, L1, T1⦄ → IH_da_cpr_lpr h o G1 L1 T1) → + (∀G1,L1,T1. ⦃G0, L0, T0⦄ >≛[h, o] ⦃G1, L1, T1⦄ → IH_snv_cpr_lpr h o G1 L1 T1) → ∀G1,L1,T1. G0 = G1 → L0 = L1 → T0 = T1 → IH_snv_cpr_lpr h o G1 L1 T1. #h #o #G0 #L0 #T0 #IH4 #IH3 #IH2 #IH1 #G1 #L1 * * [|||| * ] [ #s #HG0 #HL0 #HT0 #H1 #X #H2 #L2 #_ destruct -IH4 -IH3 -IH2 -IH1 -H1 diff --git a/matita/matita/contribs/lambdadelta/basic_2/dynamic/snv_lstas.ma b/matita/matita/contribs/lambdadelta/basic_2/dynamic/snv_lstas.ma index 627fb38ff..47c9cae13 100644 --- a/matita/matita/contribs/lambdadelta/basic_2/dynamic/snv_lstas.ma +++ b/matita/matita/contribs/lambdadelta/basic_2/dynamic/snv_lstas.ma @@ -20,10 +20,10 @@ include "basic_2/dynamic/snv_scpes.ma". (* Properties on nat-iterated stratified static type assignment for terms ***) fact snv_lstas_aux: ∀h,o,G0,L0,T0. - (∀G1,L1,T1. ⦃G0, L0, T0⦄ >≡[h, o] ⦃G1, L1, T1⦄ → IH_snv_cpr_lpr h o G1 L1 T1) → - (∀G1,L1,T1. ⦃G0, L0, T0⦄ >≡[h, o] ⦃G1, L1, T1⦄ → IH_da_cpr_lpr h o G1 L1 T1) → - (∀G1,L1,T1. ⦃G0, L0, T0⦄ >≡[h, o] ⦃G1, L1, T1⦄ → IH_lstas_cpr_lpr h o G1 L1 T1) → - (∀G1,L1,T1. ⦃G0, L0, T0⦄ >≡[h, o] ⦃G1, L1, T1⦄ → IH_snv_lstas h o G1 L1 T1) → + (∀G1,L1,T1. ⦃G0, L0, T0⦄ >≛[h, o] ⦃G1, L1, T1⦄ → IH_snv_cpr_lpr h o G1 L1 T1) → + (∀G1,L1,T1. ⦃G0, L0, T0⦄ >≛[h, o] ⦃G1, L1, T1⦄ → IH_da_cpr_lpr h o G1 L1 T1) → + (∀G1,L1,T1. ⦃G0, L0, T0⦄ >≛[h, o] ⦃G1, L1, T1⦄ → IH_lstas_cpr_lpr h o G1 L1 T1) → + (∀G1,L1,T1. ⦃G0, L0, T0⦄ >≛[h, o] ⦃G1, L1, T1⦄ → IH_snv_lstas h o G1 L1 T1) → ∀G1,L1,T1. G0 = G1 → L0 = L1 → T0 = T1 → IH_snv_lstas h o G1 L1 T1. #h #o #G0 #L0 #T0 #IH4 #IH3 #IH2 #IH1 #G1 #L1 * * [|||| * ] [ #s #HG0 #HL0 #HT0 #_ #d1 #d2 #Hd21 #Hd1 #X #H2 destruct -IH4 -IH3 -IH2 -IH1 diff --git a/matita/matita/contribs/lambdadelta/basic_2/dynamic/snv_lstas_lpr.ma b/matita/matita/contribs/lambdadelta/basic_2/dynamic/snv_lstas_lpr.ma index 2f282eb76..ed9b4e2fa 100644 --- a/matita/matita/contribs/lambdadelta/basic_2/dynamic/snv_lstas_lpr.ma +++ b/matita/matita/contribs/lambdadelta/basic_2/dynamic/snv_lstas_lpr.ma @@ -21,10 +21,10 @@ include "basic_2/dynamic/lsubsv_lstas.ma". (* Properties on sn parallel reduction for local environments ***************) fact lstas_cpr_lpr_aux: ∀h,o,G0,L0,T0. - (∀G1,L1,T1. ⦃G0, L0, T0⦄ >≡[h, o] ⦃G1, L1, T1⦄ → IH_snv_lstas h o G1 L1 T1) → - (∀G1,L1,T1. ⦃G0, L0, T0⦄ >≡[h, o] ⦃G1, L1, T1⦄ → IH_snv_cpr_lpr h o G1 L1 T1) → - (∀G1,L1,T1. ⦃G0, L0, T0⦄ >≡[h, o] ⦃G1, L1, T1⦄ → IH_da_cpr_lpr h o G1 L1 T1) → - (∀G1,L1,T1. ⦃G0, L0, T0⦄ >≡[h, o] ⦃G1, L1, T1⦄ → IH_lstas_cpr_lpr h o G1 L1 T1) → + (∀G1,L1,T1. ⦃G0, L0, T0⦄ >≛[h, o] ⦃G1, L1, T1⦄ → IH_snv_lstas h o G1 L1 T1) → + (∀G1,L1,T1. ⦃G0, L0, T0⦄ >≛[h, o] ⦃G1, L1, T1⦄ → IH_snv_cpr_lpr h o G1 L1 T1) → + (∀G1,L1,T1. ⦃G0, L0, T0⦄ >≛[h, o] ⦃G1, L1, T1⦄ → IH_da_cpr_lpr h o G1 L1 T1) → + (∀G1,L1,T1. ⦃G0, L0, T0⦄ >≛[h, o] ⦃G1, L1, T1⦄ → IH_lstas_cpr_lpr h o G1 L1 T1) → ∀G1,L1,T1. G0 = G1 → L0 = L1 → T0 = T1 → IH_lstas_cpr_lpr h o G1 L1 T1. #h #o #G0 #L0 #T0 #IH4 #IH3 #IH2 #IH1 #G1 #L1 * * [|||| * ] [ #s #_ #_ #_ #_ #d1 #d2 #_ #_ #X2 #H2 #X3 #H3 #L2 #_ -IH4 -IH3 -IH2 -IH1 diff --git a/matita/matita/contribs/lambdadelta/basic_2/dynamic/snv_scpes.ma b/matita/matita/contribs/lambdadelta/basic_2/dynamic/snv_scpes.ma index b6bc8c7c5..61d7fbdea 100644 --- a/matita/matita/contribs/lambdadelta/basic_2/dynamic/snv_scpes.ma +++ b/matita/matita/contribs/lambdadelta/basic_2/dynamic/snv_scpes.ma @@ -46,17 +46,17 @@ definition IH_snv_lstas: ∀h:sh. sd h → relation3 genv lenv term ≝ (* Properties for the preservation results **********************************) fact snv_cprs_lpr_aux: ∀h,o,G0,L0,T0. - (∀G1,L1,T1. ⦃G0, L0, T0⦄ >≡[h, o] ⦃G1, L1, T1⦄ → IH_snv_cpr_lpr h o G1 L1 T1) → - ∀G,L1,T1. ⦃G0, L0, T0⦄ >≡[h, o] ⦃G, L1, T1⦄ → ⦃G, L1⦄ ⊢ T1 ¡[h, o] → + (∀G1,L1,T1. ⦃G0, L0, T0⦄ >≛[h, o] ⦃G1, L1, T1⦄ → IH_snv_cpr_lpr h o G1 L1 T1) → + ∀G,L1,T1. ⦃G0, L0, T0⦄ >≛[h, o] ⦃G, L1, T1⦄ → ⦃G, L1⦄ ⊢ T1 ¡[h, o] → ∀T2. ⦃G, L1⦄ ⊢ T1 ➡* T2 → ∀L2. ⦃G, L1⦄ ⊢ ➡ L2 → ⦃G, L2⦄ ⊢ T2 ¡[h, o]. #h #o #G0 #L0 #T0 #IH #G #L1 #T1 #HLT0 #HT1 #T2 #H @(cprs_ind … H) -T2 /4 width=6 by fpbg_fpbs_trans, cprs_fpbs/ qed-. fact da_cprs_lpr_aux: ∀h,o,G0,L0,T0. - (∀G1,L1,T1. ⦃G0, L0, T0⦄ >≡[h, o] ⦃G1, L1, T1⦄ → IH_snv_cpr_lpr h o G1 L1 T1) → - (∀G1,L1,T1. ⦃G0, L0, T0⦄ >≡[h, o] ⦃G1, L1, T1⦄ → IH_da_cpr_lpr h o G1 L1 T1) → - ∀G,L1,T1. ⦃G0, L0, T0⦄ >≡[h, o] ⦃G, L1, T1⦄ → ⦃G, L1⦄ ⊢ T1 ¡[h, o] → + (∀G1,L1,T1. ⦃G0, L0, T0⦄ >≛[h, o] ⦃G1, L1, T1⦄ → IH_snv_cpr_lpr h o G1 L1 T1) → + (∀G1,L1,T1. ⦃G0, L0, T0⦄ >≛[h, o] ⦃G1, L1, T1⦄ → IH_da_cpr_lpr h o G1 L1 T1) → + ∀G,L1,T1. ⦃G0, L0, T0⦄ >≛[h, o] ⦃G, L1, T1⦄ → ⦃G, L1⦄ ⊢ T1 ¡[h, o] → ∀d. ⦃G, L1⦄ ⊢ T1 ▪[h, o] d → ∀T2. ⦃G, L1⦄ ⊢ T1 ➡* T2 → ∀L2. ⦃G, L1⦄ ⊢ ➡ L2 → ⦃G, L2⦄ ⊢ T2 ▪[h, o] d. #h #o #G0 #L0 #T0 #IH2 #IH1 #G #L1 #T1 #HLT0 #HT1 #d #Hd #T2 #H @@ -64,10 +64,10 @@ fact da_cprs_lpr_aux: ∀h,o,G0,L0,T0. qed-. fact da_scpds_lpr_aux: ∀h,o,G0,L0,T0. - (∀G1,L1,T1. ⦃G0, L0, T0⦄ >≡[h, o] ⦃G1, L1, T1⦄ → IH_snv_lstas h o G1 L1 T1) → - (∀G1,L1,T1. ⦃G0, L0, T0⦄ >≡[h, o] ⦃G1, L1, T1⦄ → IH_snv_cpr_lpr h o G1 L1 T1) → - (∀G1,L1,T1. ⦃G0, L0, T0⦄ >≡[h, o] ⦃G1, L1, T1⦄ → IH_da_cpr_lpr h o G1 L1 T1) → - ∀G,L1,T1. ⦃G0, L0, T0⦄ >≡[h, o] ⦃G, L1, T1⦄ → ⦃G, L1⦄ ⊢ T1 ¡[h, o] → + (∀G1,L1,T1. ⦃G0, L0, T0⦄ >≛[h, o] ⦃G1, L1, T1⦄ → IH_snv_lstas h o G1 L1 T1) → + (∀G1,L1,T1. ⦃G0, L0, T0⦄ >≛[h, o] ⦃G1, L1, T1⦄ → IH_snv_cpr_lpr h o G1 L1 T1) → + (∀G1,L1,T1. ⦃G0, L0, T0⦄ >≛[h, o] ⦃G1, L1, T1⦄ → IH_da_cpr_lpr h o G1 L1 T1) → + ∀G,L1,T1. ⦃G0, L0, T0⦄ >≛[h, o] ⦃G, L1, T1⦄ → ⦃G, L1⦄ ⊢ T1 ¡[h, o] → ∀d1. ⦃G, L1⦄ ⊢ T1 ▪[h, o] d1 → ∀T2,d2. ⦃G, L1⦄ ⊢ T1 •*➡*[h, o, d2] T2 → ∀L2. ⦃G, L1⦄ ⊢ ➡ L2 → d2 ≤ d1 ∧ ⦃G, L2⦄ ⊢ T2 ▪[h, o] d1-d2. @@ -79,11 +79,11 @@ lapply (da_cprs_lpr_aux … IH2 IH1 … Hd12 … HT2 … HL12) -IH2 -IH1 -HT2 -H qed-. fact da_scpes_aux: ∀h,o,G0,L0,T0. - (∀G1,L1,T1. ⦃G0, L0, T0⦄ >≡[h, o] ⦃G1, L1, T1⦄ → IH_snv_lstas h o G1 L1 T1) → - (∀G1,L1,T1. ⦃G0, L0, T0⦄ >≡[h, o] ⦃G1, L1, T1⦄ → IH_snv_cpr_lpr h o G1 L1 T1) → - (∀G1,L1,T1. ⦃G0, L0, T0⦄ >≡[h, o] ⦃G1, L1, T1⦄ → IH_da_cpr_lpr h o G1 L1 T1) → - ∀G,L,T1. ⦃G0, L0, T0⦄ >≡[h, o] ⦃G, L, T1⦄ → ⦃G, L⦄ ⊢ T1 ¡[h, o] → - ∀T2. ⦃G0, L0, T0⦄ >≡[h, o] ⦃G, L, T2⦄ → ⦃G, L⦄ ⊢ T2 ¡[h, o] → + (∀G1,L1,T1. ⦃G0, L0, T0⦄ >≛[h, o] ⦃G1, L1, T1⦄ → IH_snv_lstas h o G1 L1 T1) → + (∀G1,L1,T1. ⦃G0, L0, T0⦄ >≛[h, o] ⦃G1, L1, T1⦄ → IH_snv_cpr_lpr h o G1 L1 T1) → + (∀G1,L1,T1. ⦃G0, L0, T0⦄ >≛[h, o] ⦃G1, L1, T1⦄ → IH_da_cpr_lpr h o G1 L1 T1) → + ∀G,L,T1. ⦃G0, L0, T0⦄ >≛[h, o] ⦃G, L, T1⦄ → ⦃G, L⦄ ⊢ T1 ¡[h, o] → + ∀T2. ⦃G0, L0, T0⦄ >≛[h, o] ⦃G, L, T2⦄ → ⦃G, L⦄ ⊢ T2 ¡[h, o] → ∀d11. ⦃G, L⦄ ⊢ T1 ▪[h, o] d11 → ∀d12. ⦃G, L⦄ ⊢ T2 ▪[h, o] d12 → ∀d21,d22. ⦃G, L⦄ ⊢ T1 •*⬌*[h, o, d21, d22] T2 → ∧∧ d21 ≤ d11 & d22 ≤ d12 & d11 - d21 = d12 - d22. @@ -94,10 +94,10 @@ elim (da_scpds_lpr_aux … IH3 IH2 IH1 … Hd12 … HT2 … L) -Hd12 -HT2 // qed-. fact lstas_cprs_lpr_aux: ∀h,o,G0,L0,T0. - (∀G1,L1,T1. ⦃G0, L0, T0⦄ >≡[h, o] ⦃G1, L1, T1⦄ → IH_snv_cpr_lpr h o G1 L1 T1) → - (∀G1,L1,T1. ⦃G0, L0, T0⦄ >≡[h, o] ⦃G1, L1, T1⦄ → IH_da_cpr_lpr h o G1 L1 T1) → - (∀G1,L1,T1. ⦃G0, L0, T0⦄ >≡[h, o] ⦃G1, L1, T1⦄ → IH_lstas_cpr_lpr h o G1 L1 T1) → - ∀G,L1,T1. ⦃G0, L0, T0⦄ >≡[h, o] ⦃G, L1, T1⦄ → ⦃G, L1⦄ ⊢ T1 ¡[h, o] → + (∀G1,L1,T1. ⦃G0, L0, T0⦄ >≛[h, o] ⦃G1, L1, T1⦄ → IH_snv_cpr_lpr h o G1 L1 T1) → + (∀G1,L1,T1. ⦃G0, L0, T0⦄ >≛[h, o] ⦃G1, L1, T1⦄ → IH_da_cpr_lpr h o G1 L1 T1) → + (∀G1,L1,T1. ⦃G0, L0, T0⦄ >≛[h, o] ⦃G1, L1, T1⦄ → IH_lstas_cpr_lpr h o G1 L1 T1) → + ∀G,L1,T1. ⦃G0, L0, T0⦄ >≛[h, o] ⦃G, L1, T1⦄ → ⦃G, L1⦄ ⊢ T1 ¡[h, o] → ∀d1,d2. d2 ≤ d1 → ⦃G, L1⦄ ⊢ T1 ▪[h, o] d1 → ∀U1. ⦃G, L1⦄ ⊢ T1 •*[h, d2] U1 → ∀T2. ⦃G, L1⦄ ⊢ T1 ➡* T2 → ∀L2. ⦃G, L1⦄ ⊢ ➡ L2 → @@ -115,9 +115,9 @@ elim (IH1 … Hd21 … HTU … HTT2 … HL12) -IH1 -HTU -HTT2 qed-. fact scpds_cpr_lpr_aux: ∀h,o,G0,L0,T0. - (∀G1,L1,T1. ⦃G0, L0, T0⦄ >≡[h, o] ⦃G1, L1, T1⦄ → IH_da_cpr_lpr h o G1 L1 T1) → - (∀G1,L1,T1. ⦃G0, L0, T0⦄ >≡[h, o] ⦃G1, L1, T1⦄ → IH_lstas_cpr_lpr h o G1 L1 T1) → - ∀G,L1,T1. ⦃G0, L0, T0⦄ >≡[h, o] ⦃G, L1, T1⦄ → ⦃G, L1⦄ ⊢ T1 ¡[h, o] → + (∀G1,L1,T1. ⦃G0, L0, T0⦄ >≛[h, o] ⦃G1, L1, T1⦄ → IH_da_cpr_lpr h o G1 L1 T1) → + (∀G1,L1,T1. ⦃G0, L0, T0⦄ >≛[h, o] ⦃G1, L1, T1⦄ → IH_lstas_cpr_lpr h o G1 L1 T1) → + ∀G,L1,T1. ⦃G0, L0, T0⦄ >≛[h, o] ⦃G, L1, T1⦄ → ⦃G, L1⦄ ⊢ T1 ¡[h, o] → ∀U1,d. ⦃G, L1⦄ ⊢ T1 •*➡*[h, o, d] U1 → ∀T2. ⦃G, L1⦄ ⊢ T1 ➡ T2 → ∀L2. ⦃G, L1⦄ ⊢ ➡ L2 → ∃∃U2. ⦃G, L2⦄ ⊢ T2 •*➡*[h, o, d] U2 & ⦃G, L2⦄ ⊢ U1 ➡* U2. @@ -130,10 +130,10 @@ elim (cpcs_inv_cprs … H) -H /3 width=6 by ex4_2_intro, ex2_intro/ qed-. fact scpes_cpr_lpr_aux: ∀h,o,G0,L0,T0. - (∀G1,L1,T1. ⦃G0, L0, T0⦄ >≡[h, o] ⦃G1, L1, T1⦄ → IH_da_cpr_lpr h o G1 L1 T1) → - (∀G1,L1,T1. ⦃G0, L0, T0⦄ >≡[h, o] ⦃G1, L1, T1⦄ → IH_lstas_cpr_lpr h o G1 L1 T1) → - ∀G,L1,T1. ⦃G0, L0, T0⦄ >≡[h, o] ⦃G, L1, T1⦄ → ⦃G, L1⦄ ⊢ T1 ¡[h, o] → - ∀T2. ⦃G0, L0, T0⦄ >≡[h, o] ⦃G, L1, T2⦄ → ⦃G, L1⦄ ⊢ T2 ¡[h, o] → + (∀G1,L1,T1. ⦃G0, L0, T0⦄ >≛[h, o] ⦃G1, L1, T1⦄ → IH_da_cpr_lpr h o G1 L1 T1) → + (∀G1,L1,T1. ⦃G0, L0, T0⦄ >≛[h, o] ⦃G1, L1, T1⦄ → IH_lstas_cpr_lpr h o G1 L1 T1) → + ∀G,L1,T1. ⦃G0, L0, T0⦄ >≛[h, o] ⦃G, L1, T1⦄ → ⦃G, L1⦄ ⊢ T1 ¡[h, o] → + ∀T2. ⦃G0, L0, T0⦄ >≛[h, o] ⦃G, L1, T2⦄ → ⦃G, L1⦄ ⊢ T2 ¡[h, o] → ∀d1,d2. ⦃G, L1⦄ ⊢ T1 •*⬌*[h, o, d1, d2] T2 → ∀U1. ⦃G, L1⦄ ⊢ T1 ➡ U1 → ∀U2. ⦃G, L1⦄ ⊢ T2 ➡ U2 → ∀L2. ⦃G, L1⦄ ⊢ ➡ L2 → ⦃G, L2⦄ ⊢ U1 •*⬌*[h, o, d1, d2] U2. @@ -145,11 +145,11 @@ elim (cprs_conf … H1 … H2) -T0 qed-. fact lstas_scpds_aux: ∀h,o,G0,L0,T0. - (∀G1,L1,T1. ⦃G0, L0, T0⦄ >≡[h, o] ⦃G1, L1, T1⦄ → IH_snv_lstas h o G1 L1 T1) → - (∀G1,L1,T1. ⦃G0, L0, T0⦄ >≡[h, o] ⦃G1, L1, T1⦄ → IH_snv_cpr_lpr h o G1 L1 T1) → - (∀G1,L1,T1. ⦃G0, L0, T0⦄ >≡[h, o] ⦃G1, L1, T1⦄ → IH_da_cpr_lpr h o G1 L1 T1) → - (∀G1,L1,T1. ⦃G0, L0, T0⦄ >≡[h, o] ⦃G1, L1, T1⦄ → IH_lstas_cpr_lpr h o G1 L1 T1) → - ∀G,L,T. ⦃G0, L0, T0⦄ >≡[h, o] ⦃G, L, T⦄ → ⦃G, L⦄ ⊢ T ¡[h, o] → + (∀G1,L1,T1. ⦃G0, L0, T0⦄ >≛[h, o] ⦃G1, L1, T1⦄ → IH_snv_lstas h o G1 L1 T1) → + (∀G1,L1,T1. ⦃G0, L0, T0⦄ >≛[h, o] ⦃G1, L1, T1⦄ → IH_snv_cpr_lpr h o G1 L1 T1) → + (∀G1,L1,T1. ⦃G0, L0, T0⦄ >≛[h, o] ⦃G1, L1, T1⦄ → IH_da_cpr_lpr h o G1 L1 T1) → + (∀G1,L1,T1. ⦃G0, L0, T0⦄ >≛[h, o] ⦃G1, L1, T1⦄ → IH_lstas_cpr_lpr h o G1 L1 T1) → + ∀G,L,T. ⦃G0, L0, T0⦄ >≛[h, o] ⦃G, L, T⦄ → ⦃G, L⦄ ⊢ T ¡[h, o] → ∀d,d1. d1 ≤ d → ⦃G, L⦄ ⊢ T ▪[h, o] d → ∀T1. ⦃G, L⦄ ⊢ T •*[h, d1] T1 → ∀T2,d2. ⦃G, L⦄ ⊢ T •*➡*[h, o, d2] T2 → ⦃G, L⦄ ⊢ T1 •*⬌*[h, o, d2-d1, d1-d2] T2. #h #o #G0 #L0 #T0 #IH4 #IH3 #IH2 #IH1 #G #L #T #H0 #HT #d #d1 #Hd1 #HTd #T1 #HT1 #T2 #d2 * #X #d0 #Hd20 #H #HTX #HXT2 @@ -169,12 +169,12 @@ elim (le_or_ge d1 d2) #Hd12 >(eq_minus_O … Hd12) qed-. fact scpes_le_aux: ∀h,o,G0,L0,T0. - (∀G1,L1,T1. ⦃G0, L0, T0⦄ >≡[h, o] ⦃G1, L1, T1⦄ → IH_snv_lstas h o G1 L1 T1) → - (∀G1,L1,T1. ⦃G0, L0, T0⦄ >≡[h, o] ⦃G1, L1, T1⦄ → IH_snv_cpr_lpr h o G1 L1 T1) → - (∀G1,L1,T1. ⦃G0, L0, T0⦄ >≡[h, o] ⦃G1, L1, T1⦄ → IH_da_cpr_lpr h o G1 L1 T1) → - (∀G1,L1,T1. ⦃G0, L0, T0⦄ >≡[h, o] ⦃G1, L1, T1⦄ → IH_lstas_cpr_lpr h o G1 L1 T1) → - ∀G,L,T1. ⦃G0, L0, T0⦄ >≡[h, o] ⦃G, L, T1⦄ → ⦃G, L⦄ ⊢ T1 ¡[h, o] → - ∀T2. ⦃G0, L0, T0⦄ >≡[h, o] ⦃G, L, T2⦄ → ⦃G, L⦄ ⊢ T2 ¡[h, o] → + (∀G1,L1,T1. ⦃G0, L0, T0⦄ >≛[h, o] ⦃G1, L1, T1⦄ → IH_snv_lstas h o G1 L1 T1) → + (∀G1,L1,T1. ⦃G0, L0, T0⦄ >≛[h, o] ⦃G1, L1, T1⦄ → IH_snv_cpr_lpr h o G1 L1 T1) → + (∀G1,L1,T1. ⦃G0, L0, T0⦄ >≛[h, o] ⦃G1, L1, T1⦄ → IH_da_cpr_lpr h o G1 L1 T1) → + (∀G1,L1,T1. ⦃G0, L0, T0⦄ >≛[h, o] ⦃G1, L1, T1⦄ → IH_lstas_cpr_lpr h o G1 L1 T1) → + ∀G,L,T1. ⦃G0, L0, T0⦄ >≛[h, o] ⦃G, L, T1⦄ → ⦃G, L⦄ ⊢ T1 ¡[h, o] → + ∀T2. ⦃G0, L0, T0⦄ >≛[h, o] ⦃G, L, T2⦄ → ⦃G, L⦄ ⊢ T2 ¡[h, o] → ∀d11. ⦃G, L⦄ ⊢ T1 ▪[h, o] d11 → ∀d12. ⦃G, L⦄ ⊢ T2 ▪[h, o] d12 → ∀d21,d22,d. d21 + d ≤ d11 → d22 + d ≤ d12 → ⦃G, L⦄ ⊢ T1 •*⬌*[h, o, d21, d22] T2 → ⦃G, L⦄ ⊢ T1 •*⬌*[h, o, d21+d, d22+d] T2. diff --git a/matita/matita/contribs/lambdadelta/basic_2/notation/constructors/dxabbr_2.ma b/matita/matita/contribs/lambdadelta/basic_2/notation/constructors/dxabbr_2.ma index 57b921a88..1eea5226e 100644 --- a/matita/matita/contribs/lambdadelta/basic_2/notation/constructors/dxabbr_2.ma +++ b/matita/matita/contribs/lambdadelta/basic_2/notation/constructors/dxabbr_2.ma @@ -14,6 +14,6 @@ (* NOTATION FOR THE FORMAL SYSTEM λδ ****************************************) -notation "hvbox( L . break ⓓ T1 )" +notation "hvbox( L. break ⓓ T1 )" left associative with precedence 50 for @{ 'DxAbbr $L $T1 }. diff --git a/matita/matita/contribs/lambdadelta/basic_2/notation/constructors/dxabst_2.ma b/matita/matita/contribs/lambdadelta/basic_2/notation/constructors/dxabst_2.ma index d9b504ce3..3bb334e86 100644 --- a/matita/matita/contribs/lambdadelta/basic_2/notation/constructors/dxabst_2.ma +++ b/matita/matita/contribs/lambdadelta/basic_2/notation/constructors/dxabst_2.ma @@ -14,6 +14,6 @@ (* NOTATION FOR THE FORMAL SYSTEM λδ ****************************************) -notation "hvbox( L . break ⓛ T1 )" +notation "hvbox( L. break ⓛ T1 )" left associative with precedence 51 for @{ 'DxAbst $L $T1 }. diff --git a/matita/matita/contribs/lambdadelta/basic_2/notation/constructors/dxbind1_2.ma b/matita/matita/contribs/lambdadelta/basic_2/notation/constructors/dxbind1_2.ma index 023e50eb4..5e78eeb18 100644 --- a/matita/matita/contribs/lambdadelta/basic_2/notation/constructors/dxbind1_2.ma +++ b/matita/matita/contribs/lambdadelta/basic_2/notation/constructors/dxbind1_2.ma @@ -14,6 +14,6 @@ (* NOTATION FOR THE FORMAL SYSTEM λδ ****************************************) -notation "hvbox( L . break ⓤ { term 46 I } )" +notation "hvbox( L. break ⓤ { term 46 I } )" non associative with precedence 47 for @{ 'DxBind1 $L $I }. diff --git a/matita/matita/contribs/lambdadelta/basic_2/notation/constructors/dxbind2_3.ma b/matita/matita/contribs/lambdadelta/basic_2/notation/constructors/dxbind2_3.ma index 2deb5e842..6800d8e5c 100644 --- a/matita/matita/contribs/lambdadelta/basic_2/notation/constructors/dxbind2_3.ma +++ b/matita/matita/contribs/lambdadelta/basic_2/notation/constructors/dxbind2_3.ma @@ -14,6 +14,6 @@ (* NOTATION FOR THE FORMAL SYSTEM λδ ****************************************) -notation "hvbox( L . break ⓑ { term 46 I } break term 49 T1 )" +notation "hvbox( L. break ⓑ { term 46 I } break term 49 T1 )" non associative with precedence 48 for @{ 'DxBind2 $L $I $T1 }. diff --git a/matita/matita/contribs/lambdadelta/basic_2/notation/constructors/dxitem_2.ma b/matita/matita/contribs/lambdadelta/basic_2/notation/constructors/dxitem_2.ma index 51e9522f6..c2e0b42dd 100644 --- a/matita/matita/contribs/lambdadelta/basic_2/notation/constructors/dxitem_2.ma +++ b/matita/matita/contribs/lambdadelta/basic_2/notation/constructors/dxitem_2.ma @@ -14,6 +14,6 @@ (* NOTATION FOR THE FORMAL SYSTEM λδ ****************************************) -notation "hvbox( L . ⓘ { break term 46 I } )" +notation "hvbox( L. ⓘ { break term 46 I } )" non associative with precedence 46 for @{'DxItem $L $I }. diff --git a/matita/matita/contribs/lambdadelta/basic_2/notation/constructors/dxvoid_1.ma b/matita/matita/contribs/lambdadelta/basic_2/notation/constructors/dxvoid_1.ma index 96f543c2b..58faf0664 100644 --- a/matita/matita/contribs/lambdadelta/basic_2/notation/constructors/dxvoid_1.ma +++ b/matita/matita/contribs/lambdadelta/basic_2/notation/constructors/dxvoid_1.ma @@ -14,6 +14,6 @@ (* NOTATION FOR THE FORMAL SYSTEM λδ ****************************************) -notation "hvbox( L . ⓧ )" +notation "hvbox( L. ⓧ )" non associative with precedence 49 for @{ 'DxVoid $L }. diff --git a/matita/matita/contribs/lambdadelta/basic_2/notation/constructors/snabbr_3.ma b/matita/matita/contribs/lambdadelta/basic_2/notation/constructors/snabbr_3.ma index f57a89c30..192f6cd70 100644 --- a/matita/matita/contribs/lambdadelta/basic_2/notation/constructors/snabbr_3.ma +++ b/matita/matita/contribs/lambdadelta/basic_2/notation/constructors/snabbr_3.ma @@ -14,6 +14,6 @@ (* NOTATION FOR THE FORMAL SYSTEM λδ ****************************************) -notation "hvbox( ⓓ { term 46 p } break term 55 T1 . break term 55 T2 )" +notation "hvbox( ⓓ { term 46 p } break term 55 T1. break term 55 T2 )" non associative with precedence 55 for @{ 'SnAbbr $p $T1 $T2 }. diff --git a/matita/matita/contribs/lambdadelta/basic_2/notation/constructors/snabbrneg_2.ma b/matita/matita/contribs/lambdadelta/basic_2/notation/constructors/snabbrneg_2.ma index 13786d9bc..ecd1a7c63 100644 --- a/matita/matita/contribs/lambdadelta/basic_2/notation/constructors/snabbrneg_2.ma +++ b/matita/matita/contribs/lambdadelta/basic_2/notation/constructors/snabbrneg_2.ma @@ -14,6 +14,6 @@ (* NOTATION FOR THE FORMAL SYSTEM λδ ****************************************) -notation "hvbox( - ⓓ term 55 T1 . break term 55 T2 )" +notation "hvbox( - ⓓ term 55 T1. break term 55 T2 )" non associative with precedence 55 for @{ 'SnAbbrNeg $T1 $T2 }. diff --git a/matita/matita/contribs/lambdadelta/basic_2/notation/constructors/snabbrpos_2.ma b/matita/matita/contribs/lambdadelta/basic_2/notation/constructors/snabbrpos_2.ma index ae76f1958..84aa4d213 100644 --- a/matita/matita/contribs/lambdadelta/basic_2/notation/constructors/snabbrpos_2.ma +++ b/matita/matita/contribs/lambdadelta/basic_2/notation/constructors/snabbrpos_2.ma @@ -14,6 +14,6 @@ (* NOTATION FOR THE FORMAL SYSTEM λδ ****************************************) -notation "hvbox( + ⓓ term 55 T1 . break term 55 T2 )" +notation "hvbox( + ⓓ term 55 T1. break term 55 T2 )" non associative with precedence 55 for @{ 'SnAbbrPos $T1 $T2 }. diff --git a/matita/matita/contribs/lambdadelta/basic_2/notation/constructors/snabst_3.ma b/matita/matita/contribs/lambdadelta/basic_2/notation/constructors/snabst_3.ma index 8622fb7a9..2c9253d98 100644 --- a/matita/matita/contribs/lambdadelta/basic_2/notation/constructors/snabst_3.ma +++ b/matita/matita/contribs/lambdadelta/basic_2/notation/constructors/snabst_3.ma @@ -14,6 +14,6 @@ (* NOTATION FOR THE FORMAL SYSTEM λδ ****************************************) -notation "hvbox( ⓛ { term 46 p } break term 55 T1 . break term 55 T2 )" +notation "hvbox( ⓛ { term 46 p } break term 55 T1. break term 55 T2 )" non associative with precedence 55 for @{ 'SnAbst $p $T1 $T2 }. diff --git a/matita/matita/contribs/lambdadelta/basic_2/notation/constructors/snabstneg_2.ma b/matita/matita/contribs/lambdadelta/basic_2/notation/constructors/snabstneg_2.ma index 277b58b11..e4dc84a10 100644 --- a/matita/matita/contribs/lambdadelta/basic_2/notation/constructors/snabstneg_2.ma +++ b/matita/matita/contribs/lambdadelta/basic_2/notation/constructors/snabstneg_2.ma @@ -14,6 +14,6 @@ (* NOTATION FOR THE FORMAL SYSTEM λδ ****************************************) -notation "hvbox( - ⓛ term 55 T1 . break term 55 T2 )" +notation "hvbox( - ⓛ term 55 T1. break term 55 T2 )" non associative with precedence 55 for @{ 'SnAbstNeg $T1 $T2 }. diff --git a/matita/matita/contribs/lambdadelta/basic_2/notation/constructors/snabstpos_2.ma b/matita/matita/contribs/lambdadelta/basic_2/notation/constructors/snabstpos_2.ma index 9e22bc7ac..a54fadce2 100644 --- a/matita/matita/contribs/lambdadelta/basic_2/notation/constructors/snabstpos_2.ma +++ b/matita/matita/contribs/lambdadelta/basic_2/notation/constructors/snabstpos_2.ma @@ -14,6 +14,6 @@ (* NOTATION FOR THE FORMAL SYSTEM λδ ****************************************) -notation "hvbox( + ⓛ term 55 T1 . break term 55 T2 )" +notation "hvbox( + ⓛ term 55 T1. break term 55 T2 )" non associative with precedence 55 for @{ 'SnAbstPos $T1 $T2 }. diff --git a/matita/matita/contribs/lambdadelta/basic_2/notation/constructors/snappl_2.ma b/matita/matita/contribs/lambdadelta/basic_2/notation/constructors/snappl_2.ma index c1acadba2..615e70bd3 100644 --- a/matita/matita/contribs/lambdadelta/basic_2/notation/constructors/snappl_2.ma +++ b/matita/matita/contribs/lambdadelta/basic_2/notation/constructors/snappl_2.ma @@ -14,6 +14,6 @@ (* NOTATION FOR THE FORMAL SYSTEM λδ ****************************************) -notation "hvbox( ⓐ term 55 T1 . break term 55 T2 )" +notation "hvbox( ⓐ term 55 T1. break term 55 T2 )" non associative with precedence 55 for @{ 'SnAppl $T1 $T2 }. diff --git a/matita/matita/contribs/lambdadelta/basic_2/notation/constructors/snbind2_4.ma b/matita/matita/contribs/lambdadelta/basic_2/notation/constructors/snbind2_4.ma index 40804a359..b36457861 100644 --- a/matita/matita/contribs/lambdadelta/basic_2/notation/constructors/snbind2_4.ma +++ b/matita/matita/contribs/lambdadelta/basic_2/notation/constructors/snbind2_4.ma @@ -14,6 +14,6 @@ (* NOTATION FOR THE FORMAL SYSTEM λδ ****************************************) -notation "hvbox( ⓑ { term 46 p , break term 46 I } break term 55 T1 . break term 55 T )" +notation "hvbox( ⓑ { term 46 p, break term 46 I } break term 55 T1. break term 55 T )" non associative with precedence 55 for @{ 'SnBind2 $p $I $T1 $T }. diff --git a/matita/matita/contribs/lambdadelta/basic_2/notation/constructors/snbind2neg_3.ma b/matita/matita/contribs/lambdadelta/basic_2/notation/constructors/snbind2neg_3.ma index 428fe734d..c75fe170d 100644 --- a/matita/matita/contribs/lambdadelta/basic_2/notation/constructors/snbind2neg_3.ma +++ b/matita/matita/contribs/lambdadelta/basic_2/notation/constructors/snbind2neg_3.ma @@ -14,6 +14,6 @@ (* NOTATION FOR THE FORMAL SYSTEM λδ ****************************************) -notation "hvbox( - ⓑ { term 46 I } break term 55 T1 . break term 55 T )" +notation "hvbox( - ⓑ { term 46 I } break term 55 T1. break term 55 T )" non associative with precedence 55 for @{ 'SnBind2Neg $I $T1 $T }. diff --git a/matita/matita/contribs/lambdadelta/basic_2/notation/constructors/snbind2pos_3.ma b/matita/matita/contribs/lambdadelta/basic_2/notation/constructors/snbind2pos_3.ma index b89b95822..ca7a9d921 100644 --- a/matita/matita/contribs/lambdadelta/basic_2/notation/constructors/snbind2pos_3.ma +++ b/matita/matita/contribs/lambdadelta/basic_2/notation/constructors/snbind2pos_3.ma @@ -14,6 +14,6 @@ (* NOTATION FOR THE FORMAL SYSTEM λδ ****************************************) -notation "hvbox( + ⓑ { term 46 I } break term 55 T1 . break term 55 T )" +notation "hvbox( + ⓑ { term 46 I } break term 55 T1. break term 55 T )" non associative with precedence 55 for @{ 'SnBind2Pos $I $T1 $T }. diff --git a/matita/matita/contribs/lambdadelta/basic_2/notation/constructors/sncast_2.ma b/matita/matita/contribs/lambdadelta/basic_2/notation/constructors/sncast_2.ma index 55565d099..eddb2e583 100644 --- a/matita/matita/contribs/lambdadelta/basic_2/notation/constructors/sncast_2.ma +++ b/matita/matita/contribs/lambdadelta/basic_2/notation/constructors/sncast_2.ma @@ -14,6 +14,6 @@ (* NOTATION FOR THE FORMAL SYSTEM λδ ****************************************) -notation "hvbox( ⓝ term 55 T1 . break term 55 T2 )" +notation "hvbox( ⓝ term 55 T1. break term 55 T2 )" non associative with precedence 55 for @{ 'SnCast $T1 $T2 }. diff --git a/matita/matita/contribs/lambdadelta/basic_2/notation/constructors/snflat2_3.ma b/matita/matita/contribs/lambdadelta/basic_2/notation/constructors/snflat2_3.ma index ef0bdb8cb..b0fdc8987 100644 --- a/matita/matita/contribs/lambdadelta/basic_2/notation/constructors/snflat2_3.ma +++ b/matita/matita/contribs/lambdadelta/basic_2/notation/constructors/snflat2_3.ma @@ -14,6 +14,6 @@ (* NOTATION FOR THE FORMAL SYSTEM λδ ****************************************) -notation "hvbox( ⓕ { term 46 I } break term 55 T1 . break term 55 T )" +notation "hvbox( ⓕ { term 46 I } break term 55 T1. break term 55 T )" non associative with precedence 55 for @{ 'SnFlat2 $I $T1 $T }. diff --git a/matita/matita/contribs/lambdadelta/basic_2/notation/constructors/snitem2_2.ma b/matita/matita/contribs/lambdadelta/basic_2/notation/constructors/snitem2_2.ma index 82044eae6..90bc4ed5b 100644 --- a/matita/matita/contribs/lambdadelta/basic_2/notation/constructors/snitem2_2.ma +++ b/matita/matita/contribs/lambdadelta/basic_2/notation/constructors/snitem2_2.ma @@ -14,6 +14,6 @@ (* NOTATION FOR THE FORMAL SYSTEM λδ ****************************************) -notation "hvbox( ② term 55 T1 . break term 55 T )" +notation "hvbox( ② term 55 T1. break term 55 T )" non associative with precedence 55 for @{ 'SnItem2 $T1 $T }. diff --git a/matita/matita/contribs/lambdadelta/basic_2/notation/constructors/snitem2_3.ma b/matita/matita/contribs/lambdadelta/basic_2/notation/constructors/snitem2_3.ma index 9fdf70bf2..d455b5103 100644 --- a/matita/matita/contribs/lambdadelta/basic_2/notation/constructors/snitem2_3.ma +++ b/matita/matita/contribs/lambdadelta/basic_2/notation/constructors/snitem2_3.ma @@ -14,6 +14,6 @@ (* NOTATION FOR THE FORMAL SYSTEM λδ ****************************************) -notation "hvbox( ② { term 46 I } break term 55 T1 . break term 55 T )" +notation "hvbox( ② { term 46 I } break term 55 T1. break term 55 T )" non associative with precedence 55 for @{ 'SnItem2 $I $T1 $T }. diff --git a/matita/matita/contribs/lambdadelta/basic_2/notation/functions/snabbr_2.ma b/matita/matita/contribs/lambdadelta/basic_2/notation/functions/snabbr_2.ma index 4051c2085..25c3ca773 100644 --- a/matita/matita/contribs/lambdadelta/basic_2/notation/functions/snabbr_2.ma +++ b/matita/matita/contribs/lambdadelta/basic_2/notation/functions/snabbr_2.ma @@ -14,6 +14,6 @@ (* NOTATION FOR THE FORMAL SYSTEM λδ ****************************************) -notation "hvbox( ⓓ term 55 T . break term 55 L )" +notation "hvbox( ⓓ term 55 T. break term 55 L )" non associative with precedence 55 for @{ 'SnAbbr $T $L }. diff --git a/matita/matita/contribs/lambdadelta/basic_2/notation/functions/snabst_2.ma b/matita/matita/contribs/lambdadelta/basic_2/notation/functions/snabst_2.ma index 838bd007f..f5219bf69 100644 --- a/matita/matita/contribs/lambdadelta/basic_2/notation/functions/snabst_2.ma +++ b/matita/matita/contribs/lambdadelta/basic_2/notation/functions/snabst_2.ma @@ -14,6 +14,6 @@ (* NOTATION FOR THE FORMAL SYSTEM λδ ****************************************) -notation "hvbox( ⓛ term 55 T . break term 55 L )" +notation "hvbox( ⓛ term 55 T. break term 55 L )" non associative with precedence 55 for @{ 'SnAbst $T $L }. diff --git a/matita/matita/contribs/lambdadelta/basic_2/notation/functions/snapplvector_2.ma b/matita/matita/contribs/lambdadelta/basic_2/notation/functions/snapplvector_2.ma index e59520265..a7c92b4fe 100644 --- a/matita/matita/contribs/lambdadelta/basic_2/notation/functions/snapplvector_2.ma +++ b/matita/matita/contribs/lambdadelta/basic_2/notation/functions/snapplvector_2.ma @@ -14,6 +14,6 @@ (* NOTATION FOR THE FORMAL SYSTEM λδ ****************************************) -notation "hvbox( Ⓐ term 55 T1 . break term 55 T )" +notation "hvbox( Ⓐ term 55 T1. break term 55 T )" non associative with precedence 55 for @{ 'SnApplVector $T1 $T }. diff --git a/matita/matita/contribs/lambdadelta/basic_2/notation/functions/snbind1_2.ma b/matita/matita/contribs/lambdadelta/basic_2/notation/functions/snbind1_2.ma index aaaf81391..8cac6eac6 100644 --- a/matita/matita/contribs/lambdadelta/basic_2/notation/functions/snbind1_2.ma +++ b/matita/matita/contribs/lambdadelta/basic_2/notation/functions/snbind1_2.ma @@ -14,6 +14,6 @@ (* NOTATION FOR THE FORMAL SYSTEM λδ ****************************************) -notation "hvbox( ⓤ { term 46 I } . break term 55 L )" +notation "hvbox( ⓤ { term 46 I }. break term 55 L )" non associative with precedence 55 for @{ 'SnBind1 $I $L }. diff --git a/matita/matita/contribs/lambdadelta/basic_2/notation/functions/snbind2_3.ma b/matita/matita/contribs/lambdadelta/basic_2/notation/functions/snbind2_3.ma index fa44f2928..7e73c0fb5 100644 --- a/matita/matita/contribs/lambdadelta/basic_2/notation/functions/snbind2_3.ma +++ b/matita/matita/contribs/lambdadelta/basic_2/notation/functions/snbind2_3.ma @@ -14,6 +14,6 @@ (* NOTATION FOR THE FORMAL SYSTEM λδ ****************************************) -notation "hvbox( ⓑ { term 46 I } break term 55 T . break term 55 L )" +notation "hvbox( ⓑ { term 46 I } break term 55 T. break term 55 L )" non associative with precedence 55 for @{ 'SnBind2 $I $T $L }. diff --git a/matita/matita/contribs/lambdadelta/basic_2/notation/functions/snitem_2.ma b/matita/matita/contribs/lambdadelta/basic_2/notation/functions/snitem_2.ma index 000993bf0..7046d2247 100644 --- a/matita/matita/contribs/lambdadelta/basic_2/notation/functions/snitem_2.ma +++ b/matita/matita/contribs/lambdadelta/basic_2/notation/functions/snitem_2.ma @@ -14,6 +14,6 @@ (* NOTATION FOR THE FORMAL SYSTEM λδ ****************************************) -notation "hvbox( ⓘ { term 46 I } . break term 55 L )" +notation "hvbox( ⓘ { term 46 I }. break term 55 L )" non associative with precedence 55 for @{ 'SnItem $I $L }. diff --git a/matita/matita/contribs/lambdadelta/basic_2/notation/functions/snvoid_1.ma b/matita/matita/contribs/lambdadelta/basic_2/notation/functions/snvoid_1.ma index 36522d22b..2615d8c66 100644 --- a/matita/matita/contribs/lambdadelta/basic_2/notation/functions/snvoid_1.ma +++ b/matita/matita/contribs/lambdadelta/basic_2/notation/functions/snvoid_1.ma @@ -14,6 +14,6 @@ (* NOTATION FOR THE FORMAL SYSTEM λδ ****************************************) -notation "hvbox( ⓧ . term 55 L )" +notation "hvbox( ⓧ. term 55 L )" non associative with precedence 55 for @{ 'SnVoid $L }. diff --git a/matita/matita/contribs/lambdadelta/basic_2/notation/functions/weight_2.ma b/matita/matita/contribs/lambdadelta/basic_2/notation/functions/weight_2.ma index a2b9b474b..8d13242c1 100644 --- a/matita/matita/contribs/lambdadelta/basic_2/notation/functions/weight_2.ma +++ b/matita/matita/contribs/lambdadelta/basic_2/notation/functions/weight_2.ma @@ -14,6 +14,6 @@ (* NOTATION FOR THE FORMAL SYSTEM λδ ****************************************) -notation "hvbox( ♯ { term 46 L , break term 46 T } )" +notation "hvbox( ♯ { term 46 L, break term 46 T } )" non associative with precedence 90 for @{ 'Weight $L $T }. diff --git a/matita/matita/contribs/lambdadelta/basic_2/notation/functions/weight_3.ma b/matita/matita/contribs/lambdadelta/basic_2/notation/functions/weight_3.ma index 42b3c60ec..de765db43 100644 --- a/matita/matita/contribs/lambdadelta/basic_2/notation/functions/weight_3.ma +++ b/matita/matita/contribs/lambdadelta/basic_2/notation/functions/weight_3.ma @@ -14,6 +14,6 @@ (* NOTATION FOR THE FORMAL SYSTEM λδ ****************************************) -notation "hvbox( ♯ { term 46 G , break term 46 L , break term 46 T } )" +notation "hvbox( ♯ { term 46 G, break term 46 L, break term 46 T } )" non associative with precedence 90 for @{ 'Weight $G $L $T }. diff --git a/matita/matita/contribs/lambdadelta/basic_2/notation/relations/btpred_7.ma b/matita/matita/contribs/lambdadelta/basic_2/notation/relations/btpred_7.ma index 4d62df987..c4af5a9a4 100644 --- a/matita/matita/contribs/lambdadelta/basic_2/notation/relations/btpred_7.ma +++ b/matita/matita/contribs/lambdadelta/basic_2/notation/relations/btpred_7.ma @@ -14,6 +14,6 @@ (* NOTATION FOR THE FORMAL SYSTEM λδ ****************************************) -notation "hvbox( ⦃ term 46 G1, break term 46 L1, break term 46 T1 ⦄ ≽ [ break term 46 h ] ⦃ break term 46 G2, break term 46 L2 , break term 46 T2 ⦄ )" +notation "hvbox( ⦃ term 46 G1, break term 46 L1, break term 46 T1 ⦄ ≽ [ break term 46 h ] ⦃ break term 46 G2, break term 46 L2, break term 46 T2 ⦄ )" non associative with precedence 45 for @{ 'BTPRed $h $G1 $L1 $T1 $G2 $L2 $T2 }. diff --git a/matita/matita/contribs/lambdadelta/basic_2/notation/relations/btpredproper_8.ma b/matita/matita/contribs/lambdadelta/basic_2/notation/relations/btpredproper_8.ma index 45c244ce4..b9e0ccc98 100644 --- a/matita/matita/contribs/lambdadelta/basic_2/notation/relations/btpredproper_8.ma +++ b/matita/matita/contribs/lambdadelta/basic_2/notation/relations/btpredproper_8.ma @@ -14,6 +14,6 @@ (* NOTATION FOR THE FORMAL SYSTEM λδ ****************************************) -notation "hvbox( ⦃ term 46 G1, break term 46 L1, break term 46 T1 ⦄ ≻ [ break term 46 h, break term 46 o ] ⦃ break term 46 G2, break term 46 L2 , break term 46 T2 ⦄ )" +notation "hvbox( ⦃ term 46 G1, break term 46 L1, break term 46 T1 ⦄ ≻ [ break term 46 h, break term 46 o ] ⦃ break term 46 G2, break term 46 L2, break term 46 T2 ⦄ )" non associative with precedence 45 for @{ 'BTPRedProper $h $o $G1 $L1 $T1 $G2 $L2 $T2 }. diff --git a/matita/matita/contribs/lambdadelta/basic_2/notation/relations/btpredstar_8.ma b/matita/matita/contribs/lambdadelta/basic_2/notation/relations/btpredstar_8.ma index 22478c48b..065d3769e 100644 --- a/matita/matita/contribs/lambdadelta/basic_2/notation/relations/btpredstar_8.ma +++ b/matita/matita/contribs/lambdadelta/basic_2/notation/relations/btpredstar_8.ma @@ -14,6 +14,6 @@ (* NOTATION FOR THE FORMAL SYSTEM λδ ****************************************) -notation "hvbox( ⦃ term 46 G1, break term 46 L1, break term 46 T1 ⦄ ≥ [ break term 46 h, break term 46 o ] ⦃ break term 46 G2, break term 46 L2 , break term 46 T2 ⦄ )" +notation "hvbox( ⦃ term 46 G1, break term 46 L1, break term 46 T1 ⦄ ≥ [ break term 46 h, break term 46 o ] ⦃ break term 46 G2, break term 46 L2, break term 46 T2 ⦄ )" non associative with precedence 45 for @{ 'BTPRedStar $h $o $G1 $L1 $T1 $G2 $L2 $T2 }. diff --git a/matita/matita/contribs/lambdadelta/basic_2/notation/relations/btpredstaralt_8.ma b/matita/matita/contribs/lambdadelta/basic_2/notation/relations/btpredstaralt_8.ma index 8aec3b1df..dff2063a3 100644 --- a/matita/matita/contribs/lambdadelta/basic_2/notation/relations/btpredstaralt_8.ma +++ b/matita/matita/contribs/lambdadelta/basic_2/notation/relations/btpredstaralt_8.ma @@ -14,6 +14,6 @@ (* NOTATION FOR THE FORMAL SYSTEM λδ ****************************************) -notation "hvbox( ⦃ term 46 G1, break term 46 L1, break term 46 T1 ⦄ ≥ ≥ [ break term 46 h, break term 46 o ] ⦃ break term 46 G2, break term 46 L2 , break term 46 T2 ⦄ )" +notation "hvbox( ⦃ term 46 G1, break term 46 L1, break term 46 T1 ⦄ ≥ ≥ [ break term 46 h, break term 46 o ] ⦃ break term 46 G2, break term 46 L2, break term 46 T2 ⦄ )" non associative with precedence 45 for @{ 'BTPRedStarAlt $h $o $G1 $L1 $T1 $G2 $L2 $T2 }. diff --git a/matita/matita/contribs/lambdadelta/basic_2/notation/relations/dpconvstar_8.ma b/matita/matita/contribs/lambdadelta/basic_2/notation/relations/dpconvstar_8.ma index 5632e2996..f0210a6b8 100644 --- a/matita/matita/contribs/lambdadelta/basic_2/notation/relations/dpconvstar_8.ma +++ b/matita/matita/contribs/lambdadelta/basic_2/notation/relations/dpconvstar_8.ma @@ -14,6 +14,6 @@ (* NOTATION FOR THE FORMAL SYSTEM λδ ****************************************) -notation "hvbox( ⦃ term 46 G , break term 46 L ⦄ ⊢ break term 46 T1 • * ⬌ * [ break term 46 h , break term 46 o , break term 46 n1 , break term 46 n2 ] break term 46 T2 )" +notation "hvbox( ⦃ term 46 G, break term 46 L ⦄ ⊢ break term 46 T1 • * ⬌ * [ break term 46 h, break term 46 o, break term 46 n1, break term 46 n2 ] break term 46 T2 )" non associative with precedence 45 for @{ 'DPConvStar $h $o $n1 $n2 $G $L $T1 $T2 }. diff --git a/matita/matita/contribs/lambdadelta/basic_2/notation/relations/dpredstar_7.ma b/matita/matita/contribs/lambdadelta/basic_2/notation/relations/dpredstar_7.ma index 21e256dbb..2dc0e2f8d 100644 --- a/matita/matita/contribs/lambdadelta/basic_2/notation/relations/dpredstar_7.ma +++ b/matita/matita/contribs/lambdadelta/basic_2/notation/relations/dpredstar_7.ma @@ -14,6 +14,6 @@ (* NOTATION FOR THE FORMAL SYSTEM λδ ****************************************) -notation "hvbox( ⦃ term 46 G , break term 46 L ⦄ ⊢ break term 46 T1 • * ➡ * [ break term 46 h , break term 46 o , break term 46 n ] break term 46 T2 )" +notation "hvbox( ⦃ term 46 G, break term 46 L ⦄ ⊢ break term 46 T1 • * ➡ * [ break term 46 h, break term 46 o, break term 46 n ] break term 46 T2 )" non associative with precedence 45 for @{ 'DPRedStar $h $o $n $G $L $T1 $T2 }. diff --git a/matita/matita/contribs/lambdadelta/basic_2/notation/relations/lazybtpredstarproper_8.ma b/matita/matita/contribs/lambdadelta/basic_2/notation/relations/lazybtpredstarproper_8.ma index 94236004b..b1dcc127a 100644 --- a/matita/matita/contribs/lambdadelta/basic_2/notation/relations/lazybtpredstarproper_8.ma +++ b/matita/matita/contribs/lambdadelta/basic_2/notation/relations/lazybtpredstarproper_8.ma @@ -14,6 +14,6 @@ (* NOTATION FOR THE FORMAL SYSTEM λδ ****************************************) -notation "hvbox( ⦃ term 46 G1, break term 46 L1, break term 46 T1 ⦄ >≡ [ break term 46 h, break term 46 o ] ⦃ break term 46 G2, break term 46 L2 , break term 46 T2 ⦄ )" +notation "hvbox( ⦃ term 46 G1, break term 46 L1, break term 46 T1 ⦄ >≡ [ break term 46 h, break term 46 o ] ⦃ break term 46 G2, break term 46 L2, break term 46 T2 ⦄ )" non associative with precedence 45 for @{ 'LazyBTPRedStarProper $h $o $G1 $L1 $T1 $G2 $L2 $T2 }. diff --git a/matita/matita/contribs/lambdadelta/basic_2/notation/relations/nativevalid_5.ma b/matita/matita/contribs/lambdadelta/basic_2/notation/relations/nativevalid_5.ma index 4bf3b4763..1d92e8c8d 100644 --- a/matita/matita/contribs/lambdadelta/basic_2/notation/relations/nativevalid_5.ma +++ b/matita/matita/contribs/lambdadelta/basic_2/notation/relations/nativevalid_5.ma @@ -14,6 +14,6 @@ (* NOTATION FOR THE FORMAL SYSTEM λδ ****************************************) -notation "hvbox( ⦃ term 46 G , break term 46 L ⦄ ⊢ break term 46 T ¡ [ break term 46 h, break term 46 o ] )" +notation "hvbox( ⦃ term 46 G, break term 46 L ⦄ ⊢ break term 46 T ¡ [ break term 46 h, break term 46 o ] )" non associative with precedence 45 for @{ 'NativeValid $h $o $G $L $T }. diff --git a/matita/matita/contribs/lambdadelta/basic_2/notation/relations/nativevalid_6.ma b/matita/matita/contribs/lambdadelta/basic_2/notation/relations/nativevalid_6.ma index 237b7e74e..92363e0ec 100644 --- a/matita/matita/contribs/lambdadelta/basic_2/notation/relations/nativevalid_6.ma +++ b/matita/matita/contribs/lambdadelta/basic_2/notation/relations/nativevalid_6.ma @@ -14,6 +14,6 @@ (* NOTATION FOR THE FORMAL SYSTEM λδ ****************************************) -notation "hvbox( ⦃ term 46 G , break term 46 L ⦄ ⊢ break term 46 T ¡ [ break term 46 h , break term 46 o , break term 46 d ] )" +notation "hvbox( ⦃ term 46 G, break term 46 L ⦄ ⊢ break term 46 T ¡ [ break term 46 h, break term 46 o, break term 46 d ] )" non associative with precedence 45 for @{ 'NativeValid $h $o $d $G $L $T }. diff --git a/matita/matita/contribs/lambdadelta/basic_2/notation/relations/predsn_5.ma b/matita/matita/contribs/lambdadelta/basic_2/notation/relations/predsn_5.ma index 759a18874..567f64f42 100644 --- a/matita/matita/contribs/lambdadelta/basic_2/notation/relations/predsn_5.ma +++ b/matita/matita/contribs/lambdadelta/basic_2/notation/relations/predsn_5.ma @@ -14,6 +14,6 @@ (* NOTATION FOR THE FORMAL SYSTEM λδ ****************************************) -notation "hvbox( ⦃ term 46 G, break term 46 L1 ⦄ ⊢ ➡ [ break term 46 h , break term 46 T ] break term 46 L2 )" +notation "hvbox( ⦃ term 46 G, break term 46 L1 ⦄ ⊢ ➡ [ break term 46 h, break term 46 T ] break term 46 L2 )" non associative with precedence 45 for @{ 'PRedSn $h $T $G $L1 $L2 }. diff --git a/matita/matita/contribs/lambdadelta/basic_2/notation/relations/predsnstar_3.ma b/matita/matita/contribs/lambdadelta/basic_2/notation/relations/predsnstar_3.ma index 2bcf32665..75777fb17 100644 --- a/matita/matita/contribs/lambdadelta/basic_2/notation/relations/predsnstar_3.ma +++ b/matita/matita/contribs/lambdadelta/basic_2/notation/relations/predsnstar_3.ma @@ -14,6 +14,6 @@ (* NOTATION FOR THE FORMAL SYSTEM λδ ****************************************) -notation "hvbox( ⦃ term 46 G , break term 46 L1 ⦄ ⊢ ➡* break term 46 L2 )" +notation "hvbox( ⦃ term 46 G, break term 46 L1 ⦄ ⊢ ➡* break term 46 L2 )" non associative with precedence 45 for @{ 'PRedSnStar $G $L1 $L2 }. diff --git a/matita/matita/contribs/lambdadelta/basic_2/notation/relations/predsnstar_5.ma b/matita/matita/contribs/lambdadelta/basic_2/notation/relations/predsnstar_5.ma index 5debc4550..095cc3e31 100644 --- a/matita/matita/contribs/lambdadelta/basic_2/notation/relations/predsnstar_5.ma +++ b/matita/matita/contribs/lambdadelta/basic_2/notation/relations/predsnstar_5.ma @@ -14,6 +14,6 @@ (* NOTATION FOR THE FORMAL SYSTEM λδ ****************************************) -notation "hvbox( ⦃ term 46 G, break term 46 L1 ⦄ ⊢ ➡ * [ break term 46 h , break term 46 o ] break term 46 L2 )" +notation "hvbox( ⦃ term 46 G, break term 46 L1 ⦄ ⊢ ➡ * [ break term 46 h, break term 46 o ] break term 46 L2 )" non associative with precedence 45 for @{ 'PRedSnStar $h $o $G $L1 $L2 }. diff --git a/matita/matita/contribs/lambdadelta/basic_2/notation/relations/predstar_4.ma b/matita/matita/contribs/lambdadelta/basic_2/notation/relations/predstar_4.ma index 24984270d..7f374e050 100644 --- a/matita/matita/contribs/lambdadelta/basic_2/notation/relations/predstar_4.ma +++ b/matita/matita/contribs/lambdadelta/basic_2/notation/relations/predstar_4.ma @@ -14,6 +14,6 @@ (* NOTATION FOR THE FORMAL SYSTEM λδ ****************************************) -notation "hvbox( ⦃ term 46 G , term 46 L ⦄ ⊢ break term 46 T1 ➡ * break term 46 T2 )" +notation "hvbox( ⦃ term 46 G, term 46 L ⦄ ⊢ break term 46 T1 ➡ * break term 46 T2 )" non associative with precedence 45 for @{ 'PRedStar $G $L $T1 $T2 }. diff --git a/matita/matita/contribs/lambdadelta/basic_2/notation/relations/predstar_6.ma b/matita/matita/contribs/lambdadelta/basic_2/notation/relations/predstar_6.ma index 0d349e77c..20c5b48c3 100644 --- a/matita/matita/contribs/lambdadelta/basic_2/notation/relations/predstar_6.ma +++ b/matita/matita/contribs/lambdadelta/basic_2/notation/relations/predstar_6.ma @@ -14,6 +14,6 @@ (* NOTATION FOR THE FORMAL SYSTEM λδ ****************************************) -notation "hvbox( ⦃ term 46 G, break term 46 L ⦄ ⊢ break term 46 T1 ➡ * [ break term 46 h , break term 46 o ] break term 46 T2 )" +notation "hvbox( ⦃ term 46 G, break term 46 L ⦄ ⊢ break term 46 T1 ➡ * [ break term 46 h, break term 46 o ] break term 46 T2 )" non associative with precedence 45 for @{ 'PRedStar $h $o $G $L $T1 $T2 }. diff --git a/matita/matita/contribs/lambdadelta/basic_2/notation/relations/predty_7.ma b/matita/matita/contribs/lambdadelta/basic_2/notation/relations/predty_7.ma index aadb001f9..40f9f3a53 100644 --- a/matita/matita/contribs/lambdadelta/basic_2/notation/relations/predty_7.ma +++ b/matita/matita/contribs/lambdadelta/basic_2/notation/relations/predty_7.ma @@ -14,6 +14,6 @@ (* NOTATION FOR THE FORMAL SYSTEM λδ ****************************************) -notation "hvbox( ⦃ term 46 G, break term 46 L ⦄ ⊢ break term 46 T1 ⬈ [ break term 46 Rt , break term 46 c , break term 46 h ] break term 46 T2 )" +notation "hvbox( ⦃ term 46 G, break term 46 L ⦄ ⊢ break term 46 T1 ⬈ [ break term 46 Rt, break term 46 c, break term 46 h ] break term 46 T2 )" non associative with precedence 45 for @{ 'PRedTy $Rt $c $h $G $L $T1 $T2 }. diff --git a/matita/matita/contribs/lambdadelta/basic_2/notation/relations/predtynormal_5.ma b/matita/matita/contribs/lambdadelta/basic_2/notation/relations/predtynormal_5.ma index fabfe36de..dca225a8e 100644 --- a/matita/matita/contribs/lambdadelta/basic_2/notation/relations/predtynormal_5.ma +++ b/matita/matita/contribs/lambdadelta/basic_2/notation/relations/predtynormal_5.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 o ] 𝐍 ⦃ break term 46 T ⦄ )" +notation "hvbox( ⦃ term 46 G, break term 46 L ⦄ ⊢ ⬈ [ break term 46 h, break term 46 o ] 𝐍 ⦃ break term 46 T ⦄ )" non associative with precedence 45 for @{ 'PRedTyNormal $h $o $G $L $T }. diff --git a/matita/matita/contribs/lambdadelta/basic_2/notation/relations/predtysn_5.ma b/matita/matita/contribs/lambdadelta/basic_2/notation/relations/predtysn_5.ma index ac96ccb5b..0ba8150f1 100644 --- a/matita/matita/contribs/lambdadelta/basic_2/notation/relations/predtysn_5.ma +++ b/matita/matita/contribs/lambdadelta/basic_2/notation/relations/predtysn_5.ma @@ -14,6 +14,6 @@ (* NOTATION FOR THE FORMAL SYSTEM λδ ****************************************) -notation "hvbox( ⦃ term 46 G, break term 46 L1 ⦄ ⊢ ⬈ [ break term 46 h , break term 46 T ] break term 46 L2 )" +notation "hvbox( ⦃ term 46 G, break term 46 L1 ⦄ ⊢ ⬈ [ break term 46 h, break term 46 T ] break term 46 L2 )" non associative with precedence 45 for @{ 'PRedTySn $h $T $G $L1 $L2 }. diff --git a/matita/matita/contribs/lambdadelta/basic_2/notation/relations/predtysnstar_5.ma b/matita/matita/contribs/lambdadelta/basic_2/notation/relations/predtysnstar_5.ma index d0362ba88..5bb15a4f0 100644 --- a/matita/matita/contribs/lambdadelta/basic_2/notation/relations/predtysnstar_5.ma +++ b/matita/matita/contribs/lambdadelta/basic_2/notation/relations/predtysnstar_5.ma @@ -14,6 +14,6 @@ (* NOTATION FOR THE FORMAL SYSTEM λδ ****************************************) -notation "hvbox( ⦃ term 46 G, break term 46 L1 ⦄ ⊢ ⬈ * [ break term 46 h , break term 46 T ] break term 46 L2 )" +notation "hvbox( ⦃ term 46 G, break term 46 L1 ⦄ ⊢ ⬈ * [ break term 46 h, break term 46 T ] break term 46 L2 )" non associative with precedence 45 for @{ 'PRedTySnStar $h $T $G $L1 $L2 }. diff --git a/matita/matita/contribs/lambdadelta/basic_2/notation/relations/predtysnstrong_5.ma b/matita/matita/contribs/lambdadelta/basic_2/notation/relations/predtysnstrong_5.ma index ea068dd8d..c86dc8658 100644 --- a/matita/matita/contribs/lambdadelta/basic_2/notation/relations/predtysnstrong_5.ma +++ b/matita/matita/contribs/lambdadelta/basic_2/notation/relations/predtysnstrong_5.ma @@ -14,6 +14,6 @@ (* NOTATION FOR THE FORMAL SYSTEM λδ ****************************************) -notation "hvbox( G ⊢ ⬈ * [ break term 46 h , break term 46 o , break term 46 T ] 𝐒 ⦃ break term 46 L ⦄ )" +notation "hvbox( G ⊢ ⬈ * [ break term 46 h, break term 46 o, break term 46 T ] 𝐒 ⦃ break term 46 L ⦄ )" non associative with precedence 45 for @{ 'PRedTySNStrong $h $o $T $G $L }. diff --git a/matita/matita/contribs/lambdadelta/basic_2/notation/relations/predtystrong_5.ma b/matita/matita/contribs/lambdadelta/basic_2/notation/relations/predtystrong_5.ma index 680679e5f..141a8e832 100644 --- a/matita/matita/contribs/lambdadelta/basic_2/notation/relations/predtystrong_5.ma +++ b/matita/matita/contribs/lambdadelta/basic_2/notation/relations/predtystrong_5.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 o ] 𝐒 ⦃ break term 46 T ⦄ )" +notation "hvbox( ⦃ term 46 G, break term 46 L ⦄ ⊢ ⬈ * [ break term 46 h, break term 46 o ] 𝐒 ⦃ break term 46 T ⦄ )" non associative with precedence 45 for @{ 'PRedTyStrong $h $o $G $L $T }. diff --git a/matita/matita/contribs/lambdadelta/basic_2/notation/relations/rdropstar_4.ma b/matita/matita/contribs/lambdadelta/basic_2/notation/relations/rdropstar_4.ma index 30c2ac774..e60d5916f 100644 --- a/matita/matita/contribs/lambdadelta/basic_2/notation/relations/rdropstar_4.ma +++ b/matita/matita/contribs/lambdadelta/basic_2/notation/relations/rdropstar_4.ma @@ -14,6 +14,6 @@ (* NOTATION FOR THE FORMAL SYSTEM λδ ****************************************) -notation "hvbox( ⬇ * [ term 46 b , break term 46 f ] break term 46 L1 ≡ break term 46 L2 )" +notation "hvbox( ⬇ * [ term 46 b, break term 46 f ] break term 46 L1 ≡ break term 46 L2 )" non associative with precedence 45 for @{ 'RDropStar $b $f $L1 $L2 }. diff --git a/matita/matita/contribs/lambdadelta/basic_2/notation/relations/relationstar_4.ma b/matita/matita/contribs/lambdadelta/basic_2/notation/relations/relationstar_4.ma index 141856a66..227148db7 100644 --- a/matita/matita/contribs/lambdadelta/basic_2/notation/relations/relationstar_4.ma +++ b/matita/matita/contribs/lambdadelta/basic_2/notation/relations/relationstar_4.ma @@ -14,6 +14,6 @@ (* NOTATION FOR THE FORMAL SYSTEM λδ ****************************************) -notation "hvbox( L1 ⪤ * [ break term 46 R , break term 46 T ] break term 46 L2 )" +notation "hvbox( L1 ⪤ * [ break term 46 R, break term 46 T ] break term 46 L2 )" non associative with precedence 45 for @{ 'RelationStar $R $T $L1 $L2 }. diff --git a/matita/matita/contribs/lambdadelta/basic_2/notation/relations/relationstar_5.ma b/matita/matita/contribs/lambdadelta/basic_2/notation/relations/relationstar_5.ma index 135111ba3..2324f561f 100644 --- a/matita/matita/contribs/lambdadelta/basic_2/notation/relations/relationstar_5.ma +++ b/matita/matita/contribs/lambdadelta/basic_2/notation/relations/relationstar_5.ma @@ -14,6 +14,6 @@ (* NOTATION FOR THE FORMAL SYSTEM λδ ****************************************) -notation "hvbox( L1 ⪤ * [ break term 46 R1 , break term 46 R2 , break term 46 f ] break term 46 L2 )" +notation "hvbox( L1 ⪤ * [ break term 46 R1, break term 46 R2, break term 46 f ] break term 46 L2 )" non associative with precedence 45 for @{ 'RelationStar $R1 $R2 $f $L1 $L2 }. diff --git a/matita/matita/contribs/lambdadelta/basic_2/notation/relations/relationstarstar_4.ma b/matita/matita/contribs/lambdadelta/basic_2/notation/relations/relationstarstar_4.ma index f03b54a77..abec81497 100644 --- a/matita/matita/contribs/lambdadelta/basic_2/notation/relations/relationstarstar_4.ma +++ b/matita/matita/contribs/lambdadelta/basic_2/notation/relations/relationstarstar_4.ma @@ -14,6 +14,6 @@ (* NOTATION FOR THE FORMAL SYSTEM λδ ****************************************) -notation "hvbox( L1 ⪤ * * [ break term 46 R , break term 46 T ] break term 46 L2 )" +notation "hvbox( L1 ⪤ * * [ break term 46 R, break term 46 T ] break term 46 L2 )" non associative with precedence 45 for @{ 'RelationStarStar $R $T $L1 $L2 }. diff --git a/matita/matita/contribs/lambdadelta/basic_2/notation/relations/lazyeq_4.ma b/matita/matita/contribs/lambdadelta/basic_2/notation/relations/stareq_4.ma similarity index 90% rename from matita/matita/contribs/lambdadelta/basic_2/notation/relations/lazyeq_4.ma rename to matita/matita/contribs/lambdadelta/basic_2/notation/relations/stareq_4.ma index ab30a9936..0f67a8382 100644 --- a/matita/matita/contribs/lambdadelta/basic_2/notation/relations/lazyeq_4.ma +++ b/matita/matita/contribs/lambdadelta/basic_2/notation/relations/stareq_4.ma @@ -14,6 +14,6 @@ (* NOTATION FOR THE FORMAL SYSTEM λδ ****************************************) -notation "hvbox( T1 ≡ [ break term 46 h , break term 46 o ] break term 46 T2 )" +notation "hvbox( T1 ≛ [ break term 46 h, break term 46 o ] break term 46 T2 )" non associative with precedence 45 - for @{ 'LazyEq $h $o $T1 $T2 }. + for @{ 'StarEq $h $o $T1 $T2 }. diff --git a/matita/matita/contribs/lambdadelta/basic_2/notation/relations/lazyeq_5.ma b/matita/matita/contribs/lambdadelta/basic_2/notation/relations/stareq_5.ma similarity index 88% rename from matita/matita/contribs/lambdadelta/basic_2/notation/relations/lazyeq_5.ma rename to matita/matita/contribs/lambdadelta/basic_2/notation/relations/stareq_5.ma index 2a5cff3b3..553205960 100644 --- a/matita/matita/contribs/lambdadelta/basic_2/notation/relations/lazyeq_5.ma +++ b/matita/matita/contribs/lambdadelta/basic_2/notation/relations/stareq_5.ma @@ -14,6 +14,6 @@ (* NOTATION FOR THE FORMAL SYSTEM λδ ****************************************) -notation "hvbox( L ⊢ break term 46 T1 ≡ [ break term 46 h , break term 46 o ] break term 46 T2 )" +notation "hvbox( L ⊢ break term 46 T1 ≛ [ break term 46 h, break term 46 o ] break term 46 T2 )" non associative with precedence 45 - for @{ 'LazyEq $h $o $L $T1 $T2 }. + for @{ 'StarEq $h $o $L $T1 $T2 }. diff --git a/matita/matita/contribs/lambdadelta/basic_2/notation/relations/lazyeqsn_5.ma b/matita/matita/contribs/lambdadelta/basic_2/notation/relations/stareqsn_5.ma similarity index 88% rename from matita/matita/contribs/lambdadelta/basic_2/notation/relations/lazyeqsn_5.ma rename to matita/matita/contribs/lambdadelta/basic_2/notation/relations/stareqsn_5.ma index 9f361b254..af611f765 100644 --- a/matita/matita/contribs/lambdadelta/basic_2/notation/relations/lazyeqsn_5.ma +++ b/matita/matita/contribs/lambdadelta/basic_2/notation/relations/stareqsn_5.ma @@ -14,6 +14,6 @@ (* NOTATION FOR THE FORMAL SYSTEM λδ ****************************************) -notation "hvbox( L1 ≡ [ break term 46 h , break term 46 o , break term 46 T ] break term 46 L2 )" +notation "hvbox( L1 ≛ [ break term 46 h, break term 46 o, break term 46 T ] break term 46 L2 )" non associative with precedence 45 - for @{ 'LazyEqSn $h $o $T $L1 $L2 }. + for @{ 'StarEqSn $h $o $T $L1 $L2 }. diff --git a/matita/matita/contribs/lambdadelta/basic_2/notation/relations/lazyeqsn_8.ma b/matita/matita/contribs/lambdadelta/basic_2/notation/relations/stareqsn_8.ma similarity index 87% rename from matita/matita/contribs/lambdadelta/basic_2/notation/relations/lazyeqsn_8.ma rename to matita/matita/contribs/lambdadelta/basic_2/notation/relations/stareqsn_8.ma index 7c9fbae7d..6e4ed5d11 100644 --- a/matita/matita/contribs/lambdadelta/basic_2/notation/relations/lazyeqsn_8.ma +++ b/matita/matita/contribs/lambdadelta/basic_2/notation/relations/stareqsn_8.ma @@ -14,6 +14,6 @@ (* NOTATION FOR THE FORMAL SYSTEM λδ ****************************************) -notation "hvbox( ⦃ term 46 G1, break term 46 L1, break term 46 T1 ⦄ ≡ [ break term 46 h , break term 46 o ] ⦃ break term 46 G2, break term 46 L2 , break term 46 T2 ⦄ )" +notation "hvbox( ⦃ term 46 G1, break term 46 L1, break term 46 T1 ⦄ ≛ [ break term 46 h, break term 46 o ] ⦃ break term 46 G2, break term 46 L2, break term 46 T2 ⦄ )" non associative with precedence 45 - for @{ 'LazyEqSn $h $o $G1 $L1 $T1 $G2 $L2 $T2 }. + for @{ 'StarEqSn $h $o $G1 $L1 $T1 $G2 $L2 $T2 }. diff --git a/matita/matita/contribs/lambdadelta/basic_2/notation/relations/supterm_6.ma b/matita/matita/contribs/lambdadelta/basic_2/notation/relations/supterm_6.ma index 9737e1aa3..72533dc3c 100644 --- a/matita/matita/contribs/lambdadelta/basic_2/notation/relations/supterm_6.ma +++ b/matita/matita/contribs/lambdadelta/basic_2/notation/relations/supterm_6.ma @@ -14,6 +14,6 @@ (* NOTATION FOR THE FORMAL SYSTEM λδ ****************************************) -notation "hvbox( ⦃ term 46 G1, break term 46 L1, break term 46 T1 ⦄ ⊐ ⦃ break term 46 G2, break term 46 L2 , break term 46 T2 ⦄ )" +notation "hvbox( ⦃ term 46 G1, break term 46 L1, break term 46 T1 ⦄ ⊐ ⦃ break term 46 G2, break term 46 L2, break term 46 T2 ⦄ )" non associative with precedence 45 for @{ 'SupTerm $G1 $L1 $T1 $G2 $L2 $T2 }. diff --git a/matita/matita/contribs/lambdadelta/basic_2/notation/relations/supterm_7.ma b/matita/matita/contribs/lambdadelta/basic_2/notation/relations/supterm_7.ma index a312023d1..2e12296b4 100644 --- a/matita/matita/contribs/lambdadelta/basic_2/notation/relations/supterm_7.ma +++ b/matita/matita/contribs/lambdadelta/basic_2/notation/relations/supterm_7.ma @@ -14,6 +14,6 @@ (* NOTATION FOR THE FORMAL SYSTEM λδ ****************************************) -notation "hvbox( ⦃ term 46 G1, break term 46 L1, break term 46 T1 ⦄ ⊐ [ break term 46 b ] ⦃ break term 46 G2, break term 46 L2 , break term 46 T2 ⦄ )" +notation "hvbox( ⦃ term 46 G1, break term 46 L1, break term 46 T1 ⦄ ⊐ [ break term 46 b ] ⦃ break term 46 G2, break term 46 L2, break term 46 T2 ⦄ )" non associative with precedence 45 for @{ 'SupTerm $b $G1 $L1 $T1 $G2 $L2 $T2 }. diff --git a/matita/matita/contribs/lambdadelta/basic_2/notation/relations/suptermopt_6.ma b/matita/matita/contribs/lambdadelta/basic_2/notation/relations/suptermopt_6.ma index cca092323..62a8cbb0b 100644 --- a/matita/matita/contribs/lambdadelta/basic_2/notation/relations/suptermopt_6.ma +++ b/matita/matita/contribs/lambdadelta/basic_2/notation/relations/suptermopt_6.ma @@ -14,6 +14,6 @@ (* NOTATION FOR THE FORMAL SYSTEM λδ ****************************************) -notation "hvbox( ⦃ term 46 G1, break term 46 L1, break term 46 T1 ⦄ ⊐⸮ ⦃ break term 46 G2, break term 46 L2 , break term 46 T2 ⦄ )" +notation "hvbox( ⦃ term 46 G1, break term 46 L1, break term 46 T1 ⦄ ⊐⸮ ⦃ break term 46 G2, break term 46 L2, break term 46 T2 ⦄ )" non associative with precedence 45 for @{ 'SupTermOpt $G1 $L1 $T1 $G2 $L2 $T2 }. diff --git a/matita/matita/contribs/lambdadelta/basic_2/notation/relations/suptermopt_7.ma b/matita/matita/contribs/lambdadelta/basic_2/notation/relations/suptermopt_7.ma index 307ecd3a5..dd6db78c2 100644 --- a/matita/matita/contribs/lambdadelta/basic_2/notation/relations/suptermopt_7.ma +++ b/matita/matita/contribs/lambdadelta/basic_2/notation/relations/suptermopt_7.ma @@ -14,6 +14,6 @@ (* NOTATION FOR THE FORMAL SYSTEM λδ ****************************************) -notation "hvbox( ⦃ term 46 G1, break term 46 L1, break term 46 T1 ⦄ ⊐⸮ [ break term 46 b ] ⦃ break term 46 G2, break term 46 L2 , break term 46 T2 ⦄ )" +notation "hvbox( ⦃ term 46 G1, break term 46 L1, break term 46 T1 ⦄ ⊐⸮ [ break term 46 b ] ⦃ break term 46 G2, break term 46 L2, break term 46 T2 ⦄ )" non associative with precedence 45 for @{ 'SupTermOpt $b $G1 $L1 $T1 $G2 $L2 $T2 }. diff --git a/matita/matita/contribs/lambdadelta/basic_2/notation/relations/suptermplus_6.ma b/matita/matita/contribs/lambdadelta/basic_2/notation/relations/suptermplus_6.ma index ae285d31e..57bdc3d94 100644 --- a/matita/matita/contribs/lambdadelta/basic_2/notation/relations/suptermplus_6.ma +++ b/matita/matita/contribs/lambdadelta/basic_2/notation/relations/suptermplus_6.ma @@ -14,6 +14,6 @@ (* NOTATION FOR THE FORMAL SYSTEM λδ ****************************************) -notation "hvbox( ⦃ term 46 G1, term 46 L1, break term 46 T1 ⦄ ⊐ + ⦃ break term 46 G2, term 46 L2 , break term 46 T2 ⦄ )" +notation "hvbox( ⦃ term 46 G1, term 46 L1, break term 46 T1 ⦄ ⊐ + ⦃ break term 46 G2, term 46 L2, break term 46 T2 ⦄ )" non associative with precedence 45 for @{ 'SupTermPlus $G1 $L1 $T1 $G2 $L2 $T2 }. diff --git a/matita/matita/contribs/lambdadelta/basic_2/notation/relations/suptermplus_7.ma b/matita/matita/contribs/lambdadelta/basic_2/notation/relations/suptermplus_7.ma index 83b76de13..3bbe31a83 100644 --- a/matita/matita/contribs/lambdadelta/basic_2/notation/relations/suptermplus_7.ma +++ b/matita/matita/contribs/lambdadelta/basic_2/notation/relations/suptermplus_7.ma @@ -14,6 +14,6 @@ (* NOTATION FOR THE FORMAL SYSTEM λδ ****************************************) -notation "hvbox( ⦃ term 46 G1, term 46 L1, break term 46 T1 ⦄ ⊐ + [ break term 46 b ] ⦃ break term 46 G2, term 46 L2 , break term 46 T2 ⦄ )" +notation "hvbox( ⦃ term 46 G1, term 46 L1, break term 46 T1 ⦄ ⊐ + [ break term 46 b ] ⦃ break term 46 G2, term 46 L2, break term 46 T2 ⦄ )" non associative with precedence 45 for @{ 'SupTermPlus $b $G1 $L1 $T1 $G2 $L2 $T2 }. diff --git a/matita/matita/contribs/lambdadelta/basic_2/notation/relations/suptermstar_6.ma b/matita/matita/contribs/lambdadelta/basic_2/notation/relations/suptermstar_6.ma index 10af7fbd1..a0bf55faa 100644 --- a/matita/matita/contribs/lambdadelta/basic_2/notation/relations/suptermstar_6.ma +++ b/matita/matita/contribs/lambdadelta/basic_2/notation/relations/suptermstar_6.ma @@ -14,6 +14,6 @@ (* NOTATION FOR THE FORMAL SYSTEM λδ ****************************************) -notation "hvbox( ⦃ term 46 G1, term 46 L1, break term 46 T1 ⦄ ⊐ * ⦃ break term 46 G2, break term 46 L2 , break term 46 T2 ⦄ )" +notation "hvbox( ⦃ term 46 G1, term 46 L1, break term 46 T1 ⦄ ⊐ * ⦃ break term 46 G2, break term 46 L2, break term 46 T2 ⦄ )" non associative with precedence 45 for @{ 'SupTermStar $G1 $L1 $T1 $G2 $L2 $T2 }. diff --git a/matita/matita/contribs/lambdadelta/basic_2/notation/relations/suptermstar_7.ma b/matita/matita/contribs/lambdadelta/basic_2/notation/relations/suptermstar_7.ma index db96fc7e9..865019860 100644 --- a/matita/matita/contribs/lambdadelta/basic_2/notation/relations/suptermstar_7.ma +++ b/matita/matita/contribs/lambdadelta/basic_2/notation/relations/suptermstar_7.ma @@ -14,6 +14,6 @@ (* NOTATION FOR THE FORMAL SYSTEM λδ ****************************************) -notation "hvbox( ⦃ term 46 G1, term 46 L1, break term 46 T1 ⦄ ⊐ * [ break term 46 b ] ⦃ break term 46 G2, break term 46 L2 , break term 46 T2 ⦄ )" +notation "hvbox( ⦃ term 46 G1, term 46 L1, break term 46 T1 ⦄ ⊐ * [ break term 46 b ] ⦃ break term 46 G2, break term 46 L2, break term 46 T2 ⦄ )" non associative with precedence 45 for @{ 'SupTermStar $b $G1 $L1 $T1 $G2 $L2 $T2 }. diff --git a/matita/matita/contribs/lambdadelta/basic_2/notation/relations/topiso_4.ma b/matita/matita/contribs/lambdadelta/basic_2/notation/relations/topiso_4.ma index bcb7fa345..e8c080f6a 100644 --- a/matita/matita/contribs/lambdadelta/basic_2/notation/relations/topiso_4.ma +++ b/matita/matita/contribs/lambdadelta/basic_2/notation/relations/topiso_4.ma @@ -14,6 +14,6 @@ (* NOTATION FOR THE FORMAL SYSTEM λδ ****************************************) -notation "hvbox( T1 ⩳ [ break term 46 h , break term 46 o ] break term 46 T2 )" +notation "hvbox( T1 ⩳ [ break term 46 h, break term 46 o ] break term 46 T2 )" non associative with precedence 45 for @{ 'TopIso $h $o $T1 $T2 }. 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 1dfedff90..001efe155 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,7 +20,7 @@ include "basic_2/rt_computation/cpxs.ma". (* Inversion lemmas with normal terms ***************************************) lemma cpxs_inv_cnx1: ∀h,o,G,L,T1,T2. ⦃G, L⦄ ⊢ T1 ⬈*[h] T2 → ⦃G, L⦄ ⊢ ⬈[h, o] 𝐍⦃T1⦄ → - T1 ≡[h, o] T2. + T1 ≛[h, o] T2. #h #o #G #L #T1 #T2 #H @(cpxs_ind_dx … H) -T1 /5 width=8 by cnx_tdeq_trans, tdeq_trans/ qed-. diff --git a/matita/matita/contribs/lambdadelta/basic_2/rt_computation/cpxs_fqus.ma b/matita/matita/contribs/lambdadelta/basic_2/rt_computation/cpxs_fqus.ma index 9ecbc31c6..27fd06b7b 100644 --- a/matita/matita/contribs/lambdadelta/basic_2/rt_computation/cpxs_fqus.ma +++ b/matita/matita/contribs/lambdadelta/basic_2/rt_computation/cpxs_fqus.ma @@ -55,8 +55,8 @@ qed-. (* Note: a proof based on fqu_cpx_trans_ntdeq might exist *) lemma fqu_cpxs_trans_ntdeq: ∀h,o,b,G1,G2,L1,L2,T1,T2. ⦃G1, L1, T1⦄ ⊐[b] ⦃G2, L2, T2⦄ → - ∀U2. ⦃G2, L2⦄ ⊢ T2 ⬈*[h] U2 → (T2 ≡[h, o] U2 → ⊥) → - ∃∃U1. ⦃G1, L1⦄ ⊢ T1 ⬈*[h] U1 & T1 ≡[h, o] U1 → ⊥ & ⦃G1, L1, U1⦄ ⊐[b] ⦃G2, L2, U2⦄. + ∀U2. ⦃G2, L2⦄ ⊢ T2 ⬈*[h] U2 → (T2 ≛[h, o] U2 → ⊥) → + ∃∃U1. ⦃G1, L1⦄ ⊢ T1 ⬈*[h] U1 & T1 ≛[h, o] U1 → ⊥ & ⦃G1, L1, U1⦄ ⊐[b] ⦃G2, L2, U2⦄. #h #o #b #G1 #G2 #L1 #L2 #T1 #T2 #H elim H -G1 -G2 -L1 -L2 -T1 -T2 [ #I #G #L #V1 #V2 #HV12 #_ elim (lifts_total V2 𝐔❴1❵) #U2 #HVU2 @(ex3_intro … U2) @@ -87,8 +87,8 @@ lemma fqu_cpxs_trans_ntdeq: ∀h,o,b,G1,G2,L1,L2,T1,T2. ⦃G1, L1, T1⦄ ⊐[b] qed-. lemma fquq_cpxs_trans_ntdeq: ∀h,o,b,G1,G2,L1,L2,T1,T2. ⦃G1, L1, T1⦄ ⊐⸮[b] ⦃G2, L2, T2⦄ → - ∀U2. ⦃G2, L2⦄ ⊢ T2 ⬈*[h] U2 → (T2 ≡[h, o] U2 → ⊥) → - ∃∃U1. ⦃G1, L1⦄ ⊢ T1 ⬈*[h] U1 & T1 ≡[h, o] U1 → ⊥ & ⦃G1, L1, U1⦄ ⊐⸮[b] ⦃G2, L2, U2⦄. + ∀U2. ⦃G2, L2⦄ ⊢ T2 ⬈*[h] U2 → (T2 ≛[h, o] U2 → ⊥) → + ∃∃U1. ⦃G1, L1⦄ ⊢ T1 ⬈*[h] U1 & T1 ≛[h, o] U1 → ⊥ & ⦃G1, L1, U1⦄ ⊐⸮[b] ⦃G2, L2, U2⦄. #h #o #b #G1 #G2 #L1 #L2 #T1 #T2 #H12 elim H12 -H12 [ #H12 #U2 #HTU2 #H elim (fqu_cpxs_trans_ntdeq … H12 … HTU2 H) -T2 /3 width=4 by fqu_fquq, ex3_intro/ @@ -97,8 +97,8 @@ lemma fquq_cpxs_trans_ntdeq: ∀h,o,b,G1,G2,L1,L2,T1,T2. ⦃G1, L1, T1⦄ ⊐⸮ qed-. lemma fqup_cpxs_trans_ntdeq: ∀h,o,b,G1,G2,L1,L2,T1,T2. ⦃G1, L1, T1⦄ ⊐+[b] ⦃G2, L2, T2⦄ → - ∀U2. ⦃G2, L2⦄ ⊢ T2 ⬈*[h] U2 → (T2 ≡[h, o] U2 → ⊥) → - ∃∃U1. ⦃G1, L1⦄ ⊢ T1 ⬈*[h] U1 & T1 ≡[h, o] U1 → ⊥ & ⦃G1, L1, U1⦄ ⊐+[b] ⦃G2, L2, U2⦄. + ∀U2. ⦃G2, L2⦄ ⊢ T2 ⬈*[h] U2 → (T2 ≛[h, o] U2 → ⊥) → + ∃∃U1. ⦃G1, L1⦄ ⊢ T1 ⬈*[h] U1 & T1 ≛[h, o] U1 → ⊥ & ⦃G1, L1, U1⦄ ⊐+[b] ⦃G2, L2, U2⦄. #h #o #b #G1 #G2 #L1 #L2 #T1 #T2 #H @(fqup_ind_dx … H) -G1 -L1 -T1 [ #G1 #L1 #T1 #H12 #U2 #HTU2 #H elim (fqu_cpxs_trans_ntdeq … H12 … HTU2 H) -T2 /3 width=4 by fqu_fqup, ex3_intro/ @@ -109,8 +109,8 @@ lemma fqup_cpxs_trans_ntdeq: ∀h,o,b,G1,G2,L1,L2,T1,T2. ⦃G1, L1, T1⦄ ⊐+[b qed-. lemma fqus_cpxs_trans_ntdeq: ∀h,o,b,G1,G2,L1,L2,T1,T2. ⦃G1, L1, T1⦄ ⊐*[b] ⦃G2, L2, T2⦄ → - ∀U2. ⦃G2, L2⦄ ⊢ T2 ⬈*[h] U2 → (T2 ≡[h, o] U2 → ⊥) → - ∃∃U1. ⦃G1, L1⦄ ⊢ T1 ⬈*[h] U1 & T1 ≡[h, o] U1 → ⊥ & ⦃G1, L1, U1⦄ ⊐*[b] ⦃G2, L2, U2⦄. + ∀U2. ⦃G2, L2⦄ ⊢ T2 ⬈*[h] U2 → (T2 ≛[h, o] U2 → ⊥) → + ∃∃U1. ⦃G1, L1⦄ ⊢ T1 ⬈*[h] U1 & T1 ≛[h, o] U1 → ⊥ & ⦃G1, L1, U1⦄ ⊐*[b] ⦃G2, L2, U2⦄. #h #o #b #G1 #G2 #L1 #L2 #T1 #T2 #H12 #U2 #HTU2 #H elim (fqus_inv_fqup … H12) -H12 [ #H12 elim (fqup_cpxs_trans_ntdeq … H12 … HTU2 H) -T2 /3 width=4 by fqup_fqus, ex3_intro/ diff --git a/matita/matita/contribs/lambdadelta/basic_2/rt_computation/cpxs_lfdeq.ma b/matita/matita/contribs/lambdadelta/basic_2/rt_computation/cpxs_lfdeq.ma index 73119ad53..2a331abf9 100644 --- a/matita/matita/contribs/lambdadelta/basic_2/rt_computation/cpxs_lfdeq.ma +++ b/matita/matita/contribs/lambdadelta/basic_2/rt_computation/cpxs_lfdeq.ma @@ -21,8 +21,8 @@ include "basic_2/rt_computation/cpxs_tdeq.ma". (* Basic_2A1: was just: lleq_cpxs_trans *) lemma lfdeq_cpxs_trans: ∀h,o,G,L0,T0,T1. ⦃G, L0⦄ ⊢ T0 ⬈*[h] T1 → - ∀L2. L2 ≡[h, o, T0] L0 → - ∃∃T. ⦃G, L2⦄ ⊢ T0 ⬈*[h] T & T ≡[h, o] T1. + ∀L2. L2 ≛[h, o, T0] L0 → + ∃∃T. ⦃G, L2⦄ ⊢ T0 ⬈*[h] T & T ≛[h, o] T1. #h #o #G #L0 #T0 #T1 #H @(cpxs_ind_dx … H) -T0 /2 width=3 by ex2_intro/ #T0 #T #HT0 #_ #IH #L2 #HL2 elim (lfdeq_cpx_trans … HL2 … HT0) #U1 #H1 #H2 @@ -33,17 +33,17 @@ qed-. (* Basic_2A1: was just: cpxs_lleq_conf *) lemma cpxs_lfdeq_trans: ∀h,o,G,L0,T0,T1. ⦃G, L0⦄ ⊢ T0 ⬈*[h] T1 → - ∀L2. L0 ≡[h, o, T0] L2 → - ∃∃T. ⦃G, L2⦄ ⊢ T0 ⬈*[h] T & T ≡[h, o] T1. + ∀L2. L0 ≛[h, o, T0] L2 → + ∃∃T. ⦃G, L2⦄ ⊢ T0 ⬈*[h] T & T ≛[h, o] T1. /3 width=3 by lfdeq_cpxs_trans, lfdeq_sym/ qed-. (* Basic_2A1: was just: cpxs_lleq_conf_dx *) lemma cpxs_lfdeq_conf_dx: ∀h,o,G,L2,T1,T2. ⦃G, L2⦄ ⊢ T1 ⬈*[h] T2 → - ∀L1. L1 ≡[h, o, T1] L2 → L1 ≡[h, o, T2] L2. + ∀L1. L1 ≛[h, o, T1] L2 → L1 ≛[h, o, T2] L2. #h #o #G #L2 #T1 #T2 #H @(cpxs_ind … H) -T2 /3 width=6 by cpx_lfdeq_conf_dx/ qed-. (* Basic_2A1: was just: lleq_conf_sn *) lemma cpxs_lfdeq_conf_sn: ∀h,o,G,L1,T1,T2. ⦃G, L1⦄ ⊢ T1 ⬈*[h] T2 → - ∀L2. L1 ≡[h, o, T1] L2 → L1 ≡[h, o, T2] L2. + ∀L2. L1 ≛[h, o, T1] L2 → L1 ≛[h, o, T2] L2. /4 width=6 by cpxs_lfdeq_conf_dx, lfdeq_sym/ qed-. diff --git a/matita/matita/contribs/lambdadelta/basic_2/rt_computation/cpxs_tdeq.ma b/matita/matita/contribs/lambdadelta/basic_2/rt_computation/cpxs_tdeq.ma index 4960595ff..c2f308c96 100644 --- a/matita/matita/contribs/lambdadelta/basic_2/rt_computation/cpxs_tdeq.ma +++ b/matita/matita/contribs/lambdadelta/basic_2/rt_computation/cpxs_tdeq.ma @@ -21,16 +21,16 @@ include "basic_2/rt_computation/cpxs.ma". (* Properties with degree-based equivalence for terms ***********************) -lemma tdeq_cpxs_trans: ∀h,o,U1,T1. U1 ≡[h, o] T1 → ∀G,L,T2. ⦃G, L⦄ ⊢ T1 ⬈*[h] T2 → - ∃∃U2. ⦃G, L⦄ ⊢ U1 ⬈*[h] U2 & U2 ≡[h, o] T2. +lemma tdeq_cpxs_trans: ∀h,o,U1,T1. U1 ≛[h, o] T1 → ∀G,L,T2. ⦃G, L⦄ ⊢ T1 ⬈*[h] T2 → + ∃∃U2. ⦃G, L⦄ ⊢ U1 ⬈*[h] U2 & U2 ≛[h, o] T2. #h #o #U1 #T1 #HUT1 #G #L #T2 #HT12 @(cpxs_ind … HT12) -T2 /2 width=3 by ex2_intro/ #T #T2 #_ #HT2 * #U #HU1 #HUT elim (tdeq_cpx_trans … HUT … HT2) -T -T1 /3 width=3 by ex2_intro, cpxs_strap1/ qed-. (* Note: this requires tdeq to be symmetric *) -lemma cpxs_tdneq_inv_step_sn: ∀h,o,G,L,T1,T2. ⦃G, L⦄ ⊢ T1 ⬈*[h] T2 → (T1 ≡[h, o] T2 → ⊥) → - ∃∃T,T0. ⦃G, L⦄ ⊢ T1 ⬈[h] T & T1 ≡[h, o] T → ⊥ & ⦃G, L⦄ ⊢ T ⬈*[h] T0 & T0 ≡[h, o] T2. +lemma cpxs_tdneq_inv_step_sn: ∀h,o,G,L,T1,T2. ⦃G, L⦄ ⊢ T1 ⬈*[h] T2 → (T1 ≛[h, o] T2 → ⊥) → + ∃∃T,T0. ⦃G, L⦄ ⊢ T1 ⬈[h] T & T1 ≛[h, o] T → ⊥ & ⦃G, L⦄ ⊢ T ⬈*[h] T0 & T0 ≛[h, o] T2. #h #o #G #L #T1 #T2 #H @(cpxs_ind_dx … H) -T1 [ #H elim H -H // | #T1 #T #H1 #H2 #IH #Hn12 elim (tdeq_dec h o T1 T) #H destruct 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 c7e8e3dd3..49f221911 100644 --- a/matita/matita/contribs/lambdadelta/basic_2/rt_computation/csx.ma +++ b/matita/matita/contribs/lambdadelta/basic_2/rt_computation/csx.ma @@ -29,7 +29,7 @@ interpretation lemma csx_ind: ∀h,o,G,L. ∀R:predicate term. (∀T1. ⦃G, L⦄ ⊢ ⬈*[h, o] 𝐒⦃T1⦄ → - (∀T2. ⦃G, L⦄ ⊢ T1 ⬈[h] T2 → (T1 ≡[h, o] T2 → ⊥) → R T2) → + (∀T2. ⦃G, L⦄ ⊢ T1 ⬈[h] T2 → (T1 ≛[h, o] T2 → ⊥) → R T2) → R T1 ) → ∀T. ⦃G, L⦄ ⊢ ⬈*[h, o] 𝐒⦃T⦄ → R T. @@ -41,7 +41,7 @@ qed-. (* Basic_1: was just: sn3_pr2_intro *) lemma csx_intro: ∀h,o,G,L,T1. - (∀T2. ⦃G, L⦄ ⊢ T1 ⬈[h] T2 → (T1 ≡[h, o] T2 → ⊥) → ⦃G, L⦄ ⊢ ⬈*[h, o] 𝐒⦃T2⦄) → + (∀T2. ⦃G, L⦄ ⊢ T1 ⬈[h] T2 → (T1 ≛[h, o] T2 → ⊥) → ⦃G, L⦄ ⊢ ⬈*[h, o] 𝐒⦃T2⦄) → ⦃G, L⦄ ⊢ ⬈*[h, o] 𝐒⦃T1⦄. /4 width=1 by SN_intro/ 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 fb7dad498..7cf220ebd 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 @@ -30,7 +30,7 @@ qed. fact aaa_ind_csx_aux: ∀h,o,G,L,A. ∀R:predicate term. (∀T1. ⦃G, L⦄ ⊢ T1 ⁝ A → - (∀T2. ⦃G, L⦄ ⊢ T1 ⬈[h] T2 → (T1 ≡[h, o] T2 → ⊥) → R T2) → R T1 + (∀T2. ⦃G, L⦄ ⊢ T1 ⬈[h] T2 → (T1 ≛[h, o] T2 → ⊥) → R T2) → R T1 ) → ∀T. ⦃G, L⦄ ⊢ ⬈*[h, o] 𝐒⦃T⦄ → ⦃G, L⦄ ⊢ T ⁝ A → R T. #h #o #G #L #A #R #IH #T #H @(csx_ind … H) -T /4 width=5 by cpx_aaa_conf/ @@ -38,14 +38,14 @@ qed-. lemma aaa_ind_csx: ∀h,o,G,L,A. ∀R:predicate term. (∀T1. ⦃G, L⦄ ⊢ T1 ⁝ A → - (∀T2. ⦃G, L⦄ ⊢ T1 ⬈[h] T2 → (T1 ≡[h, o] T2 → ⊥) → R T2) → R T1 + (∀T2. ⦃G, L⦄ ⊢ T1 ⬈[h] T2 → (T1 ≛[h, o] T2 → ⊥) → R T2) → R T1 ) → ∀T. ⦃G, L⦄ ⊢ T ⁝ A → R T. /5 width=9 by aaa_ind_csx_aux, aaa_csx/ qed-. fact aaa_ind_csx_cpxs_aux: ∀h,o,G,L,A. ∀R:predicate term. (∀T1. ⦃G, L⦄ ⊢ T1 ⁝ A → - (∀T2. ⦃G, L⦄ ⊢ T1 ⬈*[h] T2 → (T1 ≡[h, o] T2 → ⊥) → R T2) → R T1 + (∀T2. ⦃G, L⦄ ⊢ T1 ⬈*[h] T2 → (T1 ≛[h, o] T2 → ⊥) → R T2) → R T1 ) → ∀T. ⦃G, L⦄ ⊢ ⬈*[h, o] 𝐒⦃T⦄ → ⦃G, L⦄ ⊢ T ⁝ A → R T. #h #o #G #L #A #R #IH #T #H @(csx_ind_cpxs … H) -T /4 width=5 by cpxs_aaa_conf/ @@ -54,7 +54,7 @@ qed-. (* Basic_2A1: was: aaa_ind_csx_alt *) lemma aaa_ind_csx_cpxs: ∀h,o,G,L,A. ∀R:predicate term. (∀T1. ⦃G, L⦄ ⊢ T1 ⁝ A → - (∀T2. ⦃G, L⦄ ⊢ T1 ⬈*[h] T2 → (T1 ≡[h, o] T2 → ⊥) → R T2) → R T1 + (∀T2. ⦃G, L⦄ ⊢ T1 ⬈*[h] T2 → (T1 ≛[h, o] T2 → ⊥) → R T2) → R T1 ) → ∀T. ⦃G, L⦄ ⊢ T ⁝ A → R 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_cpxs.ma b/matita/matita/contribs/lambdadelta/basic_2/rt_computation/csx_cpxs.ma index 8d066e53b..87a5e890f 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 @@ -22,7 +22,7 @@ include "basic_2/rt_computation/csx_csx.ma". (* Basic_1: was just: sn3_intro *) lemma csx_intro_cpxs: ∀h,o,G,L,T1. - (∀T2. ⦃G, L⦄ ⊢ T1 ⬈*[h] T2 → (T1 ≡[h, o] T2 → ⊥) → ⦃G, L⦄ ⊢ ⬈*[h, o] 𝐒⦃T2⦄) → + (∀T2. ⦃G, L⦄ ⊢ T1 ⬈*[h] T2 → (T1 ≛[h, o] T2 → ⊥) → ⦃G, L⦄ ⊢ ⬈*[h, o] 𝐒⦃T2⦄) → ⦃G, L⦄ ⊢ ⬈*[h, o] 𝐒⦃T1⦄. /4 width=1 by cpx_cpxs, csx_intro/ qed-. @@ -37,10 +37,10 @@ qed-. lemma csx_ind_cpxs_tdeq: ∀h,o,G,L. ∀R:predicate term. (∀T1. ⦃G, L⦄ ⊢ ⬈*[h, o] 𝐒⦃T1⦄ → - (∀T2. ⦃G, L⦄ ⊢ T1 ⬈*[h] T2 → (T1 ≡[h, o] T2 → ⊥) → R T2) → R T1 + (∀T2. ⦃G, L⦄ ⊢ T1 ⬈*[h] T2 → (T1 ≛[h, o] T2 → ⊥) → R T2) → R T1 ) → ∀T1. ⦃G, L⦄ ⊢ ⬈*[h, o] 𝐒⦃T1⦄ → - ∀T0. ⦃G, L⦄ ⊢ T1 ⬈*[h] T0 → ∀T2. T0 ≡[h, o] T2 → R T2. + ∀T0. ⦃G, L⦄ ⊢ T1 ⬈*[h] T0 → ∀T2. T0 ≛[h, o] T2 → R T2. #h #o #G #L #R #IH #T1 #H @(csx_ind … H) -T1 #T1 #HT1 #IH1 #T0 #HT10 #T2 #HT02 @IH -IH /3 width=3 by csx_cpxs_trans, csx_tdeq_trans/ -HT1 #V2 #HTV2 #HnTV2 @@ -61,7 +61,7 @@ qed-. (* Basic_2A1: was: csx_ind_alt *) lemma csx_ind_cpxs: ∀h,o,G,L. ∀R:predicate term. (∀T1. ⦃G, L⦄ ⊢ ⬈*[h, o] 𝐒⦃T1⦄ → - (∀T2. ⦃G, L⦄ ⊢ T1 ⬈*[h] T2 → (T1 ≡[h, o] T2 → ⊥) → R T2) → R T1 + (∀T2. ⦃G, L⦄ ⊢ T1 ⬈*[h] T2 → (T1 ≛[h, o] T2 → ⊥) → R T2) → R T1 ) → ∀T. ⦃G, L⦄ ⊢ ⬈*[h, o] 𝐒⦃T⦄ → R T. #h #o #G #L #R #IH #T #HT 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 69ca48513..a877af8b7 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 @@ -21,7 +21,7 @@ include "basic_2/rt_computation/csx_drops.ma". (* Advanced properties ******************************************************) lemma csx_tdeq_trans: ∀h,o,G,L,T1. ⦃G, L⦄ ⊢ ⬈*[h, o] 𝐒⦃T1⦄ → - ∀T2. T1 ≡[h, o] T2 → ⦃G, L⦄ ⊢ ⬈*[h, o] 𝐒⦃T2⦄. + ∀T2. T1 ≛[h, o] T2 → ⦃G, L⦄ ⊢ ⬈*[h, o] 𝐒⦃T2⦄. #h #o #G #L #T1 #H @(csx_ind … H) -T1 #T #_ #IH #T2 #HT2 @csx_intro #T1 #HT21 #HnT21 elim (tdeq_cpx_trans … HT2 … HT21) -HT21 /4 width=5 by tdeq_repl/ diff --git a/matita/matita/contribs/lambdadelta/basic_2/rt_computation/csx_lfdeq.ma b/matita/matita/contribs/lambdadelta/basic_2/rt_computation/csx_lfdeq.ma index 67e63613a..2f4655814 100644 --- a/matita/matita/contribs/lambdadelta/basic_2/rt_computation/csx_lfdeq.ma +++ b/matita/matita/contribs/lambdadelta/basic_2/rt_computation/csx_lfdeq.ma @@ -21,7 +21,7 @@ include "basic_2/rt_computation/csx_csx.ma". (* Basic_2A1: uses: csx_lleq_conf *) lemma csx_lfdeq_conf: ∀h,o,G,L1,T. ⦃G, L1⦄ ⊢ ⬈*[h, o] 𝐒⦃T⦄ → - ∀L2. L1 ≡[h, o, T] L2 → ⦃G, L2⦄ ⊢ ⬈*[h, o] 𝐒⦃T⦄. + ∀L2. L1 ≛[h, o, T] L2 → ⦃G, L2⦄ ⊢ ⬈*[h, o] 𝐒⦃T⦄. #h #o #G #L1 #T #H @(csx_ind … H) -T #T1 #_ #IH #L2 #HL12 @csx_intro #T2 #HT12 #HnT12 @@ -30,6 +30,6 @@ elim (lfdeq_cpx_trans … HL12 … HT12) -HT12 qed-. (* Basic_2A1: uses: csx_lleq_conf *) -lemma csx_lfdeq_trans: ∀h,o,L1,L2,T. L1 ≡[h, o, T] L2 → +lemma csx_lfdeq_trans: ∀h,o,L1,L2,T. L1 ≛[h, o, T] L2 → ∀G. ⦃G, L2⦄ ⊢ ⬈*[h, o] 𝐒⦃T⦄ → ⦃G, L1⦄ ⊢ ⬈*[h, o] 𝐒⦃T⦄. /3 width=3 by csx_lfdeq_conf, lfdeq_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 d6d1c1094..7d1137af7 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 @@ -20,7 +20,7 @@ include "basic_2/rt_computation/csx_csx.ma". (* Properties with simple terms *********************************************) lemma csx_appl_simple: ∀h,o,G,L,V. ⦃G, L⦄ ⊢ ⬈*[h, o] 𝐒⦃V⦄ → ∀T1. - (∀T2. ⦃G, L⦄ ⊢ T1 ⬈[h] T2 → (T1 ≡[h, o] T2 → ⊥) → ⦃G, L⦄ ⊢ ⬈*[h, o] 𝐒⦃ⓐV.T2⦄) → + (∀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 #V #_ #IHV #T1 #IHT1 #HT1 diff --git a/matita/matita/contribs/lambdadelta/basic_2/rt_computation/fpbg.ma b/matita/matita/contribs/lambdadelta/basic_2/rt_computation/fpbg.ma index c1e2b94c1..49376aad6 100644 --- a/matita/matita/contribs/lambdadelta/basic_2/rt_computation/fpbg.ma +++ b/matita/matita/contribs/lambdadelta/basic_2/rt_computation/fpbg.ma @@ -28,12 +28,12 @@ interpretation "'qrst' proper parallel computation (closure)" (* Basic properties *********************************************************) lemma fpb_fpbg: ∀h,o,G1,G2,L1,L2,T1,T2. ⦃G1, L1, T1⦄ ≻[h, o] ⦃G2, L2, T2⦄ → - ⦃G1, L1, T1⦄ >≡[h, o] ⦃G2, L2, T2⦄. + ⦃G1, L1, T1⦄ >≛[h, o] ⦃G2, L2, T2⦄. /2 width=5 by ex2_3_intro/ qed. lemma fpbg_fpbq_trans: ∀h,o,G1,G,G2,L1,L,L2,T1,T,T2. - ⦃G1, L1, T1⦄ >≡[h, o] ⦃G, L, T⦄ → ⦃G, L, T⦄ ≽[h, o] ⦃G2, L2, T2⦄ → - ⦃G1, L1, T1⦄ >≡[h, o] ⦃G2, L2, T2⦄. + ⦃G1, L1, T1⦄ >≛[h, o] ⦃G, L, T⦄ → ⦃G, L, T⦄ ≽[h, o] ⦃G2, L2, T2⦄ → + ⦃G1, L1, T1⦄ >≛[h, o] ⦃G2, L2, T2⦄. #h #o #G1 #G #G2 #L1 #L #L2 #T1 #T #T2 * /3 width=9 by fpbs_strap1, ex2_3_intro/ qed-. diff --git a/matita/matita/contribs/lambdadelta/basic_2/rt_computation/fpbg_fleq.ma b/matita/matita/contribs/lambdadelta/basic_2/rt_computation/fpbg_fleq.ma index ed03b2549..2196b8ad1 100644 --- a/matita/matita/contribs/lambdadelta/basic_2/rt_computation/fpbg_fleq.ma +++ b/matita/matita/contribs/lambdadelta/basic_2/rt_computation/fpbg_fleq.ma @@ -20,12 +20,12 @@ include "basic_2/computation/fpbg.ma". (* Properties on lazy equivalence for closures ******************************) -lemma fpbg_fleq_trans: ∀h,o,G1,G,L1,L,T1,T. ⦃G1, L1, T1⦄ >≡[h, o] ⦃G, L, T⦄ → - ∀G2,L2,T2. ⦃G, L, T⦄ ≡[0] ⦃G2, L2, T2⦄ → ⦃G1, L1, T1⦄ >≡[h, o] ⦃G2, L2, T2⦄. +lemma fpbg_fleq_trans: ∀h,o,G1,G,L1,L,T1,T. ⦃G1, L1, T1⦄ >≛[h, o] ⦃G, L, T⦄ → + ∀G2,L2,T2. ⦃G, L, T⦄ ≡[0] ⦃G2, L2, T2⦄ → ⦃G1, L1, T1⦄ >≛[h, o] ⦃G2, L2, T2⦄. /3 width=5 by fpbg_fpbq_trans, fleq_fpbq/ qed-. -lemma fleq_fpbg_trans: ∀h,o,G,G2,L,L2,T,T2. ⦃G, L, T⦄ >≡[h, o] ⦃G2, L2, T2⦄ → - ∀G1,L1,T1. ⦃G1, L1, T1⦄ ≡[0] ⦃G, L, T⦄ → ⦃G1, L1, T1⦄ >≡[h, o] ⦃G2, L2, T2⦄. +lemma fleq_fpbg_trans: ∀h,o,G,G2,L,L2,T,T2. ⦃G, L, T⦄ >≛[h, o] ⦃G2, L2, T2⦄ → + ∀G1,L1,T1. ⦃G1, L1, T1⦄ ≡[0] ⦃G, L, T⦄ → ⦃G1, L1, T1⦄ >≛[h, o] ⦃G2, L2, T2⦄. #h #o #G #G2 #L #L2 #T #T2 * #G0 #L0 #T0 #H0 #H02 #G1 #L1 #T1 #H1 elim (fleq_fpb_trans … H1 … H0) -G -L -T /4 width=9 by fpbs_strap2, fleq_fpbq, ex2_3_intro/ @@ -39,14 +39,14 @@ lemma fleq_fpbs: ∀h,o,G1,G2,L1,L2,T1,T2. qed. lemma fpbg_fwd_fpbs: ∀h,o,G1,G2,L1,L2,T1,T2. - ⦃G1, L1, T1⦄ >≡[h,o] ⦃G2, L2, T2⦄ → ⦃G1, L1, T1⦄ ≥[h, o] ⦃G2, L2, T2⦄. + ⦃G1, L1, T1⦄ >≛[h,o] ⦃G2, L2, T2⦄ → ⦃G1, L1, T1⦄ ≥[h, o] ⦃G2, L2, T2⦄. #h #o #G1 #G2 #L1 #L2 #T1 #T2 * /3 width=5 by fpbs_strap2, fpb_fpbq/ qed-. lemma fpbs_fpbg: ∀h,o,G1,G2,L1,L2,T1,T2. ⦃G1, L1, T1⦄ ≥[h, o] ⦃G2, L2, T2⦄ → ⦃G1, L1, T1⦄ ≡[0] ⦃G2, L2, T2⦄ ∨ - ⦃G1, L1, T1⦄ >≡[h, o] ⦃G2, L2, T2⦄. + ⦃G1, L1, T1⦄ >≛[h, o] ⦃G2, L2, T2⦄. #h #o #G1 #G2 #L1 #L2 #T1 #T2 #H @(fpbs_ind … H) -G2 -L2 -T2 [ /2 width=1 by or_introl/ | #G #G2 #L #L2 #T #T2 #_ #H2 * #H1 @(fpbq_ind_alt … H2) -H2 #H2 diff --git a/matita/matita/contribs/lambdadelta/basic_2/rt_computation/fpbg_fpbs.ma b/matita/matita/contribs/lambdadelta/basic_2/rt_computation/fpbg_fpbs.ma index df666294c..2118c2c16 100644 --- a/matita/matita/contribs/lambdadelta/basic_2/rt_computation/fpbg_fpbs.ma +++ b/matita/matita/contribs/lambdadelta/basic_2/rt_computation/fpbg_fpbs.ma @@ -21,13 +21,13 @@ include "basic_2/computation/fpbg_fleq.ma". (* Properties on "qrst" parallel reduction on closures **********************) lemma fpb_fpbg_trans: ∀h,o,G1,G,G2,L1,L,L2,T1,T,T2. - ⦃G1, L1, T1⦄ ≻[h, o] ⦃G, L, T⦄ → ⦃G, L, T⦄ >≡[h, o] ⦃G2, L2, T2⦄ → - ⦃G1, L1, T1⦄ >≡[h, o] ⦃G2, L2, T2⦄. + ⦃G1, L1, T1⦄ ≻[h, o] ⦃G, L, T⦄ → ⦃G, L, T⦄ >≛[h, o] ⦃G2, L2, T2⦄ → + ⦃G1, L1, T1⦄ >≛[h, o] ⦃G2, L2, T2⦄. /3 width=5 by fpbg_fwd_fpbs, ex2_3_intro/ qed-. lemma fpbq_fpbg_trans: ∀h,o,G1,G,G2,L1,L,L2,T1,T,T2. - ⦃G1, L1, T1⦄ ≽[h, o] ⦃G, L, T⦄ → ⦃G, L, T⦄ >≡[h, o] ⦃G2, L2, T2⦄ → - ⦃G1, L1, T1⦄ >≡[h, o] ⦃G2, L2, T2⦄. + ⦃G1, L1, T1⦄ ≽[h, o] ⦃G, L, T⦄ → ⦃G, L, T⦄ >≛[h, o] ⦃G2, L2, T2⦄ → + ⦃G1, L1, T1⦄ >≛[h, o] ⦃G2, L2, T2⦄. #h #o #G1 #G #G2 #L1 #L #L2 #T1 #T #T2 #H1 #H2 @(fpbq_ind_alt … H1) -H1 /2 width=5 by fleq_fpbg_trans, fpb_fpbg_trans/ qed-. @@ -35,34 +35,34 @@ qed-. (* Properties on "qrst" parallel compuutation on closures *******************) lemma fpbs_fpbg_trans: ∀h,o,G1,G,L1,L,T1,T. ⦃G1, L1, T1⦄ ≥[h, o] ⦃G, L, T⦄ → - ∀G2,L2,T2. ⦃G, L, T⦄ >≡[h, o] ⦃G2, L2, T2⦄ → ⦃G1, L1, T1⦄ >≡[h, o] ⦃G2, L2, T2⦄. + ∀G2,L2,T2. ⦃G, L, T⦄ >≛[h, o] ⦃G2, L2, T2⦄ → ⦃G1, L1, T1⦄ >≛[h, o] ⦃G2, L2, T2⦄. #h #o #G1 #G #L1 #L #T1 #T #H @(fpbs_ind … H) -G -L -T /3 width=5 by fpbq_fpbg_trans/ qed-. (* Note: this is used in the closure proof *) lemma fpbg_fpbs_trans: ∀h,o,G,G2,L,L2,T,T2. ⦃G, L, T⦄ ≥[h, o] ⦃G2, L2, T2⦄ → - ∀G1,L1,T1. ⦃G1, L1, T1⦄ >≡[h, o] ⦃G, L, T⦄ → ⦃G1, L1, T1⦄ >≡[h, o] ⦃G2, L2, T2⦄. + ∀G1,L1,T1. ⦃G1, L1, T1⦄ >≛[h, o] ⦃G, L, T⦄ → ⦃G1, L1, T1⦄ >≛[h, o] ⦃G2, L2, T2⦄. #h #o #G #G2 #L #L2 #T #T2 #H @(fpbs_ind_dx … H) -G -L -T /3 width=5 by fpbg_fpbq_trans/ qed-. (* Note: this is used in the closure proof *) -lemma fqup_fpbg: ∀h,o,G1,G2,L1,L2,T1,T2. ⦃G1, L1, T1⦄ ⊐+ ⦃G2, L2, T2⦄ → ⦃G1, L1, T1⦄ >≡[h, o] ⦃G2, L2, T2⦄. +lemma fqup_fpbg: ∀h,o,G1,G2,L1,L2,T1,T2. ⦃G1, L1, T1⦄ ⊐+ ⦃G2, L2, T2⦄ → ⦃G1, L1, T1⦄ >≛[h, o] ⦃G2, L2, T2⦄. #h #o #G1 #G2 #L1 #L2 #T1 #T2 #H elim (fqup_inv_step_sn … H) -H /3 width=5 by fqus_fpbs, fpb_fqu, ex2_3_intro/ qed. lemma cpxs_fpbg: ∀h,o,G,L,T1,T2. ⦃G, L⦄ ⊢ T1 ➡*[h, o] T2 → - (T1 = T2 → ⊥) → ⦃G, L, T1⦄ >≡[h, o] ⦃G, L, T2⦄. + (T1 = T2 → ⊥) → ⦃G, L, T1⦄ >≛[h, o] ⦃G, L, T2⦄. #h #o #G #L #T1 #T2 #H #H0 elim (cpxs_neq_inv_step_sn … H … H0) -H -H0 /4 width=5 by cpxs_fpbs, fpb_cpx, ex2_3_intro/ qed. lemma lstas_fpbg: ∀h,o,G,L,T1,T2,d2. ⦃G, L⦄ ⊢ T1 •*[h, d2] T2 → (T1 = T2 → ⊥) → - ∀d1. d2 ≤ d1 → ⦃G, L⦄ ⊢ T1 ▪[h, o] d1 → ⦃G, L, T1⦄ >≡[h, o] ⦃G, L, T2⦄. + ∀d1. d2 ≤ d1 → ⦃G, L⦄ ⊢ T1 ▪[h, o] d1 → ⦃G, L, T1⦄ >≛[h, o] ⦃G, L, T2⦄. /3 width=5 by lstas_cpxs, cpxs_fpbg/ qed. lemma lpxs_fpbg: ∀h,o,G,L1,L2,T. ⦃G, L1⦄ ⊢ ➡*[h, o] L2 → - (L1 ≡[T, 0] L2 → ⊥) → ⦃G, L1, T⦄ >≡[h, o] ⦃G, L2, T⦄. + (L1 ≡[T, 0] L2 → ⊥) → ⦃G, L1, T⦄ >≛[h, o] ⦃G, L2, T⦄. #h #o #G #L1 #L2 #T #H #H0 elim (lpxs_nlleq_inv_step_sn … H … H0) -H -H0 /4 width=5 by fpb_lpx, lpxs_lleq_fpbs, ex2_3_intro/ qed. diff --git a/matita/matita/contribs/lambdadelta/basic_2/rt_computation/fpbg_lift.ma b/matita/matita/contribs/lambdadelta/basic_2/rt_computation/fpbg_lift.ma index a0f4edbb8..4fe3be22f 100644 --- a/matita/matita/contribs/lambdadelta/basic_2/rt_computation/fpbg_lift.ma +++ b/matita/matita/contribs/lambdadelta/basic_2/rt_computation/fpbg_lift.ma @@ -20,5 +20,5 @@ include "basic_2/computation/fpbg.ma". (* Advanced properties ******************************************************) lemma sta_fpbg: ∀h,o,G,L,T1,T2,d. ⦃G, L⦄ ⊢ T1 ▪[h, o] d+1 → - ⦃G, L⦄ ⊢ T1 •*[h, 1] T2 → ⦃G, L, T1⦄ >≡[h, o] ⦃G, L, T2⦄. + ⦃G, L⦄ ⊢ T1 •*[h, 1] T2 → ⦃G, L, T1⦄ >≛[h, o] ⦃G, L, T2⦄. /4 width=2 by fpb_fpbg, sta_fpb/ 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 05bb29c01..e40fbc1d3 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 @@ -52,7 +52,7 @@ lemma aaa_ind_fpb: ∀h,o. ∀R:relation3 genv lenv term. fact aaa_ind_fpbg_aux: ∀h,o. ∀R:relation3 genv lenv term. (∀G1,L1,T1,A. ⦃G1, L1⦄ ⊢ T1 ⁝ A → - (∀G2,L2,T2. ⦃G1, L1, T1⦄ >≡[h, o] ⦃G2, L2, T2⦄ → R G2 L2 T2) → + (∀G2,L2,T2. ⦃G1, L1, T1⦄ >≛[h, o] ⦃G2, L2, T2⦄ → R G2 L2 T2) → R G1 L1 T1 ) → ∀G,L,T. ⦃G, L⦄ ⊢ ⬊*[h, o] T → ∀A. ⦃G, L⦄ ⊢ T ⁝ A → R G L T. @@ -64,7 +64,7 @@ qed-. lemma aaa_ind_fpbg: ∀h,o. ∀R:relation3 genv lenv term. (∀G1,L1,T1,A. ⦃G1, L1⦄ ⊢ T1 ⁝ A → - (∀G2,L2,T2. ⦃G1, L1, T1⦄ >≡[h, o] ⦃G2, L2, T2⦄ → R G2 L2 T2) → + (∀G2,L2,T2. ⦃G1, L1, T1⦄ >≛[h, o] ⦃G2, L2, T2⦄ → R G2 L2 T2) → R G1 L1 T1 ) → ∀G,L,T,A. ⦃G, L⦄ ⊢ T ⁝ A → R G L T. diff --git a/matita/matita/contribs/lambdadelta/basic_2/rt_computation/fsb_alt.ma b/matita/matita/contribs/lambdadelta/basic_2/rt_computation/fsb_alt.ma index 80c7a6449..eadfece46 100644 --- a/matita/matita/contribs/lambdadelta/basic_2/rt_computation/fsb_alt.ma +++ b/matita/matita/contribs/lambdadelta/basic_2/rt_computation/fsb_alt.ma @@ -21,7 +21,7 @@ include "basic_2/computation/fsb.ma". (* Note: alternative definition of fsb *) inductive fsba (h) (o): relation3 genv lenv term ≝ | fsba_intro: ∀G1,L1,T1. ( - ∀G2,L2,T2. ⦃G1, L1, T1⦄ >≡[h, o] ⦃G2, L2, T2⦄ → fsba h o G2 L2 T2 + ∀G2,L2,T2. ⦃G1, L1, T1⦄ >≛[h, o] ⦃G2, L2, T2⦄ → fsba h o G2 L2 T2 ) → fsba h o G1 L1 T1. interpretation @@ -32,7 +32,7 @@ interpretation lemma fsba_ind_alt: ∀h,o. ∀R: relation3 …. ( ∀G1,L1,T1. ⦥⦥[h,o] ⦃G1, L1, T1⦄ → ( - ∀G2,L2,T2. ⦃G1, L1, T1⦄ >≡[h, o] ⦃G2, L2, T2⦄ → R G2 L2 T2 + ∀G2,L2,T2. ⦃G1, L1, T1⦄ >≛[h, o] ⦃G2, L2, T2⦄ → R G2 L2 T2 ) → R G1 L1 T1 ) → ∀G,L,T. ⦥⦥[h, o] ⦃G, L, T⦄ → R G L T. @@ -73,7 +73,7 @@ lemma fsb_fpbs_trans: ∀h,o,G1,L1,T1. ⦥[h, o] ⦃G1, L1, T1⦄ → lemma fsb_ind_fpbg: ∀h,o. ∀R:relation3 genv lenv term. (∀G1,L1,T1. ⦥[h, o] ⦃G1, L1, T1⦄ → - (∀G2,L2,T2. ⦃G1, L1, T1⦄ >≡[h, o] ⦃G2, L2, T2⦄ → R G2 L2 T2) → + (∀G2,L2,T2. ⦃G1, L1, T1⦄ >≛[h, o] ⦃G2, L2, T2⦄ → R G2 L2 T2) → R G1 L1 T1 ) → ∀G1,L1,T1. ⦥[h, o] ⦃G1, L1, T1⦄ → R G1 L1 T1. 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 e86c302b8..58325a948 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 @@ -63,7 +63,7 @@ lemma csx_ind_fpb: ∀h,o. ∀R:relation3 genv lenv term. lemma csx_ind_fpbg: ∀h,o. ∀R:relation3 genv lenv term. (∀G1,L1,T1. ⦃G1, L1⦄ ⊢ ⬊*[h, o] T1 → - (∀G2,L2,T2. ⦃G1, L1, T1⦄ >≡[h, o] ⦃G2, L2, T2⦄ → R G2 L2 T2) → + (∀G2,L2,T2. ⦃G1, L1, T1⦄ >≛[h, o] ⦃G2, L2, T2⦄ → R G2 L2 T2) → R G1 L1 T1 ) → ∀G,L,T. ⦃G, L⦄ ⊢ ⬊*[h, o] T → R G L T. diff --git a/matita/matita/contribs/lambdadelta/basic_2/rt_computation/lfpxs_lfdeq.ma b/matita/matita/contribs/lambdadelta/basic_2/rt_computation/lfpxs_lfdeq.ma index 9389dd099..897199a9e 100644 --- a/matita/matita/contribs/lambdadelta/basic_2/rt_computation/lfpxs_lfdeq.ma +++ b/matita/matita/contribs/lambdadelta/basic_2/rt_computation/lfpxs_lfdeq.ma @@ -22,8 +22,8 @@ include "basic_2/rt_computation/lfpxs_fqup.ma". (* Basic_2A1: was: lleq_lpxs_trans *) lemma lfdeq_lfpxs_trans: ∀h,o,G,L2,K2,T. ⦃G, L2⦄ ⊢ ⬈*[h, T] K2 → - ∀L1. L1 ≡[h, o, T] L2 → - ∃∃K1. ⦃G, L1⦄ ⊢ ⬈*[h, T] K1 & K1 ≡[h, o, T] K2. + ∀L1. L1 ≛[h, o, T] L2 → + ∃∃K1. ⦃G, L1⦄ ⊢ ⬈*[h, T] K1 & K1 ≛[h, o, T] K2. #h #o #G #L2 #K2 #T #H @(lfpxs_ind_sn … H) -K2 /2 width=3 by ex2_intro/ #K #K2 #_ #HK2 #IH #L1 #HT elim (IH … HT) -L2 #L #HL1 #HT elim (lfdeq_lfpx_trans … HK2 … HT) -K @@ -31,8 +31,8 @@ lemma lfdeq_lfpxs_trans: ∀h,o,G,L2,K2,T. ⦃G, L2⦄ ⊢ ⬈*[h, T] K2 → qed-. (* Basic_2A1: was: lpxs_nlleq_inv_step_sn *) -lemma lfpxs_lfdneq_inv_step_sn: ∀h,o,G,L1,L2,T. ⦃G, L1⦄ ⊢ ⬈*[h, T] L2 → (L1 ≡[h, o, T] L2 → ⊥) → - ∃∃L,L0. ⦃G, L1⦄ ⊢ ⬈[h, T] L & L1 ≡[h, o, T] L → ⊥ & ⦃G, L⦄ ⊢ ⬈*[h, T] L0 & L0 ≡[h, o, T] L2. +lemma lfpxs_lfdneq_inv_step_sn: ∀h,o,G,L1,L2,T. ⦃G, L1⦄ ⊢ ⬈*[h, T] L2 → (L1 ≛[h, o, T] L2 → ⊥) → + ∃∃L,L0. ⦃G, L1⦄ ⊢ ⬈[h, T] L & L1 ≛[h, o, T] L → ⊥ & ⦃G, L⦄ ⊢ ⬈*[h, T] L0 & L0 ≛[h, o, T] L2. #h #o #G #L1 #L2 #T #H @(lfpxs_ind_dx … H) -L1 [ #H elim H -H // | #L1 #L #H1 #H2 #IH2 #H12 elim (lfdeq_dec h o L1 L T) #H diff --git a/matita/matita/contribs/lambdadelta/basic_2/rt_computation/lfsx.ma b/matita/matita/contribs/lambdadelta/basic_2/rt_computation/lfsx.ma index 74181a037..bf17640dd 100644 --- a/matita/matita/contribs/lambdadelta/basic_2/rt_computation/lfsx.ma +++ b/matita/matita/contribs/lambdadelta/basic_2/rt_computation/lfsx.ma @@ -30,7 +30,7 @@ interpretation (* Basic_2A1: uses: lsx_ind *) lemma lfsx_ind: ∀h,o,G,T. ∀R:predicate lenv. (∀L1. G ⊢ ⬈*[h, o, T] 𝐒⦃L1⦄ → - (∀L2. ⦃G, L1⦄ ⊢ ⬈[h, T] L2 → (L1 ≡[h, o, T] L2 → ⊥) → R L2) → + (∀L2. ⦃G, L1⦄ ⊢ ⬈[h, T] L2 → (L1 ≛[h, o, T] L2 → ⊥) → R L2) → R L1 ) → ∀L. G ⊢ ⬈*[h, o, T] 𝐒⦃L⦄ → R L. @@ -42,7 +42,7 @@ qed-. (* Basic_2A1: uses: lsx_intro *) lemma lfsx_intro: ∀h,o,G,L1,T. - (∀L2. ⦃G, L1⦄ ⊢ ⬈[h, T] L2 → (L1 ≡[h, o, T] L2 → ⊥) → G ⊢ ⬈*[h, o, T] 𝐒⦃L2⦄) → + (∀L2. ⦃G, L1⦄ ⊢ ⬈[h, T] L2 → (L1 ≛[h, o, T] L2 → ⊥) → G ⊢ ⬈*[h, o, T] 𝐒⦃L2⦄) → G ⊢ ⬈*[h, o, T] 𝐒⦃L1⦄. /5 width=1 by lfdeq_sym, SN_intro/ qed. diff --git a/matita/matita/contribs/lambdadelta/basic_2/rt_computation/lfsx_lfpxs.ma b/matita/matita/contribs/lambdadelta/basic_2/rt_computation/lfsx_lfpxs.ma index ff5ddc304..23250e0f6 100644 --- a/matita/matita/contribs/lambdadelta/basic_2/rt_computation/lfsx_lfpxs.ma +++ b/matita/matita/contribs/lambdadelta/basic_2/rt_computation/lfsx_lfpxs.ma @@ -23,7 +23,7 @@ include "basic_2/rt_computation/lfsx_lfsx.ma". (* Basic_2A1: uses: lsx_intro_alt *) lemma lfsx_intro_lfpxs: ∀h,o,G,L1,T. - (∀L2. ⦃G, L1⦄ ⊢ ⬈*[h, T] L2 → (L1 ≡[h, o, T] L2 → ⊥) → G ⊢ ⬈*[h, o, T] 𝐒⦃L2⦄) → + (∀L2. ⦃G, L1⦄ ⊢ ⬈*[h, T] L2 → (L1 ≛[h, o, T] L2 → ⊥) → G ⊢ ⬈*[h, o, T] 𝐒⦃L2⦄) → G ⊢ ⬈*[h, o, T] 𝐒⦃L1⦄. /4 width=1 by lfpx_lfpxs, lfsx_intro/ qed-. @@ -38,11 +38,11 @@ qed-. lemma lfsx_ind_lfpxs_lfdeq: ∀h,o,G,T. ∀R:predicate lenv. (∀L1. G ⊢ ⬈*[h, o, T] 𝐒⦃L1⦄ → - (∀L2. ⦃G, L1⦄ ⊢ ⬈*[h, T] L2 → (L1 ≡[h, o, T] L2 → ⊥) → R L2) → + (∀L2. ⦃G, L1⦄ ⊢ ⬈*[h, T] L2 → (L1 ≛[h, o, T] L2 → ⊥) → R L2) → R L1 ) → ∀L1. G ⊢ ⬈*[h, o, T] 𝐒⦃L1⦄ → - ∀L0. ⦃G, L1⦄ ⊢ ⬈*[h, T] L0 → ∀L2. L0 ≡[h, o, T] L2 → R L2. + ∀L0. ⦃G, L1⦄ ⊢ ⬈*[h, T] L0 → ∀L2. L0 ≛[h, o, T] L2 → R L2. #h #o #G #T #R #IH #L1 #H @(lfsx_ind … H) -L1 #L1 #HL1 #IH1 #L0 #HL10 #L2 #HL02 @IH -IH /3 width=3 by lfsx_lfpxs_trans, lfsx_lfdeq_trans/ -HL1 #K2 #HLK2 #HnLK2 @@ -63,7 +63,7 @@ qed-. (* Basic_2A1: uses: lsx_ind_alt *) lemma lfsx_ind_lfpxs: ∀h,o,G,T. ∀R:predicate lenv. (∀L1. G ⊢ ⬈*[h, o, T] 𝐒⦃L1⦄ → - (∀L2. ⦃G, L1⦄ ⊢ ⬈*[h, T] L2 → (L1 ≡[h, o, T] L2 → ⊥) → R L2) → + (∀L2. ⦃G, L1⦄ ⊢ ⬈*[h, T] L2 → (L1 ≛[h, o, T] L2 → ⊥) → R L2) → R L1 ) → ∀L. G ⊢ ⬈*[h, o, T] 𝐒⦃L⦄ → R L. diff --git a/matita/matita/contribs/lambdadelta/basic_2/rt_computation/lfsx_lfsx.ma b/matita/matita/contribs/lambdadelta/basic_2/rt_computation/lfsx_lfsx.ma index 24dcd4c1f..a6ef10ba9 100644 --- a/matita/matita/contribs/lambdadelta/basic_2/rt_computation/lfsx_lfsx.ma +++ b/matita/matita/contribs/lambdadelta/basic_2/rt_computation/lfsx_lfsx.ma @@ -22,7 +22,7 @@ include "basic_2/rt_computation/lfsx.ma". (* Basic_2A1: uses: lsx_lleq_trans *) lemma lfsx_lfdeq_trans: ∀h,o,G,L1,T. G ⊢ ⬈*[h, o, T] 𝐒⦃L1⦄ → - ∀L2. L1 ≡[h, o, T] L2 → G ⊢ ⬈*[h, o, T] 𝐒⦃L2⦄. + ∀L2. L1 ≛[h, o, T] L2 → G ⊢ ⬈*[h, o, T] 𝐒⦃L2⦄. #h #o #G #L1 #T #H @(lfsx_ind … H) -L1 #L1 #_ #IHL1 #L2 #HL12 @lfsx_intro #L #HL2 #HnL2 elim (lfdeq_lfpx_trans … HL2 … HL12) -HL2 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 a60e62ada..2b6ef64ae 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 @@ -21,7 +21,7 @@ include "basic_2/rt_transition/cnx.ma". (* Advanced properties ******************************************************) lemma cnx_tdeq_trans: ∀h,o,G,L,T1. ⦃G, L⦄ ⊢ ⬈[h, o] 𝐍⦃T1⦄ → - ∀T2. T1 ≡[h, o] T2 → ⦃G, L⦄ ⊢ ⬈[h, o] 𝐍⦃T2⦄. + ∀T2. T1 ≛[h, o] T2 → ⦃G, L⦄ ⊢ ⬈[h, o] 𝐍⦃T2⦄. #h #o #G #L #T1 #HT1 #T2 #HT12 #T #HT2 elim (tdeq_cpx_trans … HT12 … HT2) -HT2 #T0 #HT10 #HT0 lapply (HT1 … HT10) -HT1 -HT10 /2 width=5 by tdeq_repl/ (**) (* full auto fails *) diff --git a/matita/matita/contribs/lambdadelta/basic_2/rt_transition/cpx_fqus.ma b/matita/matita/contribs/lambdadelta/basic_2/rt_transition/cpx_fqus.ma index 147114a11..0744bd0fc 100644 --- a/matita/matita/contribs/lambdadelta/basic_2/rt_transition/cpx_fqus.ma +++ b/matita/matita/contribs/lambdadelta/basic_2/rt_transition/cpx_fqus.ma @@ -67,8 +67,8 @@ lemma fqus_cpx_trans: ∀h,b,G1,G2,L1,L2,T1,T2. ⦃G1, L1, T1⦄ ⊐*[b] ⦃G2, qed-. lemma fqu_cpx_trans_ntdeq: ∀h,o,b,G1,G2,L1,L2,T1,T2. ⦃G1, L1, T1⦄ ⊐[b] ⦃G2, L2, T2⦄ → - ∀U2. ⦃G2, L2⦄ ⊢ T2 ⬈[h] U2 → (T2 ≡[h, o] U2 → ⊥) → - ∃∃U1. ⦃G1, L1⦄ ⊢ T1 ⬈[h] U1 & T1 ≡[h, o] U1 → ⊥ & ⦃G1, L1, U1⦄ ⊐[b] ⦃G2, L2, U2⦄. + ∀U2. ⦃G2, L2⦄ ⊢ T2 ⬈[h] U2 → (T2 ≛[h, o] U2 → ⊥) → + ∃∃U1. ⦃G1, L1⦄ ⊢ T1 ⬈[h] U1 & T1 ≛[h, o] U1 → ⊥ & ⦃G1, L1, U1⦄ ⊐[b] ⦃G2, L2, U2⦄. #h #o #b #G1 #G2 #L1 #L2 #T1 #T2 #H elim H -G1 -G2 -L1 -L2 -T1 -T2 [ #I #G #L #V1 #V2 #HV12 #_ elim (lifts_total V2 𝐔❴1❵) #U2 #HVU2 @(ex3_intro … U2) @@ -99,8 +99,8 @@ lemma fqu_cpx_trans_ntdeq: ∀h,o,b,G1,G2,L1,L2,T1,T2. ⦃G1, L1, T1⦄ ⊐[b] qed-. lemma fquq_cpx_trans_ntdeq: ∀h,o,b,G1,G2,L1,L2,T1,T2. ⦃G1, L1, T1⦄ ⊐⸮[b] ⦃G2, L2, T2⦄ → - ∀U2. ⦃G2, L2⦄ ⊢ T2 ⬈[h] U2 → (T2 ≡[h, o] U2 → ⊥) → - ∃∃U1. ⦃G1, L1⦄ ⊢ T1 ⬈[h] U1 & T1 ≡[h, o] U1 → ⊥ & ⦃G1, L1, U1⦄ ⊐⸮[b] ⦃G2, L2, U2⦄. + ∀U2. ⦃G2, L2⦄ ⊢ T2 ⬈[h] U2 → (T2 ≛[h, o] U2 → ⊥) → + ∃∃U1. ⦃G1, L1⦄ ⊢ T1 ⬈[h] U1 & T1 ≛[h, o] U1 → ⊥ & ⦃G1, L1, U1⦄ ⊐⸮[b] ⦃G2, L2, U2⦄. #h #o #b #G1 #G2 #L1 #L2 #T1 #T2 #H12 elim H12 -H12 [ #H12 #U2 #HTU2 #H elim (fqu_cpx_trans_ntdeq … H12 … HTU2 H) -T2 /3 width=4 by fqu_fquq, ex3_intro/ @@ -109,8 +109,8 @@ lemma fquq_cpx_trans_ntdeq: ∀h,o,b,G1,G2,L1,L2,T1,T2. ⦃G1, L1, T1⦄ ⊐⸮[ qed-. lemma fqup_cpx_trans_ntdeq: ∀h,o,b,G1,G2,L1,L2,T1,T2. ⦃G1, L1, T1⦄ ⊐+[b] ⦃G2, L2, T2⦄ → - ∀U2. ⦃G2, L2⦄ ⊢ T2 ⬈[h] U2 → (T2 ≡[h, o] U2 → ⊥) → - ∃∃U1. ⦃G1, L1⦄ ⊢ T1 ⬈[h] U1 & T1 ≡[h, o] U1 → ⊥ & ⦃G1, L1, U1⦄ ⊐+[b] ⦃G2, L2, U2⦄. + ∀U2. ⦃G2, L2⦄ ⊢ T2 ⬈[h] U2 → (T2 ≛[h, o] U2 → ⊥) → + ∃∃U1. ⦃G1, L1⦄ ⊢ T1 ⬈[h] U1 & T1 ≛[h, o] U1 → ⊥ & ⦃G1, L1, U1⦄ ⊐+[b] ⦃G2, L2, U2⦄. #h #o #b #G1 #G2 #L1 #L2 #T1 #T2 #H @(fqup_ind_dx … H) -G1 -L1 -T1 [ #G1 #L1 #T1 #H12 #U2 #HTU2 #H elim (fqu_cpx_trans_ntdeq … H12 … HTU2 H) -T2 /3 width=4 by fqu_fqup, ex3_intro/ @@ -121,8 +121,8 @@ lemma fqup_cpx_trans_ntdeq: ∀h,o,b,G1,G2,L1,L2,T1,T2. ⦃G1, L1, T1⦄ ⊐+[b] qed-. lemma fqus_cpx_trans_ntdeq: ∀h,o,b,G1,G2,L1,L2,T1,T2. ⦃G1, L1, T1⦄ ⊐*[b] ⦃G2, L2, T2⦄ → - ∀U2. ⦃G2, L2⦄ ⊢ T2 ⬈[h] U2 → (T2 ≡[h, o] U2 → ⊥) → - ∃∃U1. ⦃G1, L1⦄ ⊢ T1 ⬈[h] U1 & T1 ≡[h, o] U1 → ⊥ & ⦃G1, L1, U1⦄ ⊐*[b] ⦃G2, L2, U2⦄. + ∀U2. ⦃G2, L2⦄ ⊢ T2 ⬈[h] U2 → (T2 ≛[h, o] U2 → ⊥) → + ∃∃U1. ⦃G1, L1⦄ ⊢ T1 ⬈[h] U1 & T1 ≛[h, o] U1 → ⊥ & ⦃G1, L1, U1⦄ ⊐*[b] ⦃G2, L2, U2⦄. #h #o #b #G1 #G2 #L1 #L2 #T1 #T2 #H12 #U2 #HTU2 #H elim (fqus_inv_fqup … H12) -H12 [ #H12 elim (fqup_cpx_trans_ntdeq … H12 … HTU2 H) -T2 /3 width=4 by fqup_fqus, ex3_intro/ diff --git a/matita/matita/contribs/lambdadelta/basic_2/rt_transition/cpx_lfdeq.ma b/matita/matita/contribs/lambdadelta/basic_2/rt_transition/cpx_lfdeq.ma index 3aec365f7..f3ccf0616 100644 --- a/matita/matita/contribs/lambdadelta/basic_2/rt_transition/cpx_lfdeq.ma +++ b/matita/matita/contribs/lambdadelta/basic_2/rt_transition/cpx_lfdeq.ma @@ -25,5 +25,5 @@ lemma cpx_lfdeq_conf_sn: ∀h,o,G. s_r_confluent1 … (cpx h G) (lfdeq h o). (* Basic_2A1: was just: cpx_lleq_conf_dx *) lemma cpx_lfdeq_conf_dx: ∀h,o,G,L2,T1,T2. ⦃G, L2⦄ ⊢ T1 ⬈[h] T2 → - ∀L1. L1 ≡[h, o, T1] L2 → L1 ≡[h, o, T2] L2. + ∀L1. L1 ≛[h, o, T1] L2 → L1 ≛[h, o, T2] L2. /4 width=4 by cpx_lfdeq_conf_sn, lfdeq_sym/ qed-. diff --git a/matita/matita/contribs/lambdadelta/basic_2/rt_transition/fpb.ma b/matita/matita/contribs/lambdadelta/basic_2/rt_transition/fpb.ma index ca6ddfd09..1ccc9ca6d 100644 --- a/matita/matita/contribs/lambdadelta/basic_2/rt_transition/fpb.ma +++ b/matita/matita/contribs/lambdadelta/basic_2/rt_transition/fpb.ma @@ -21,8 +21,8 @@ include "basic_2/rt_transition/lfpr_lfpx.ma". inductive fpb (h) (o) (G1) (L1) (T1): relation3 genv lenv term ≝ | fpb_fqu : ∀G2,L2,T2. ⦃G1, L1, T1⦄ ⊐ ⦃G2, L2, T2⦄ → fpb h o G1 L1 T1 G2 L2 T2 -| fpb_cpx : ∀T2. ⦃G1, L1⦄ ⊢ T1 ⬈[h] T2 → (T1 ≡[h, o] T2 → ⊥) → fpb h o G1 L1 T1 G1 L1 T2 -| fpb_lfpx: ∀L2. ⦃G1, L1⦄ ⊢ ⬈[h, T1] L2 → (L1 ≡[h, o, T1] L2 → ⊥) → fpb h o G1 L1 T1 G1 L2 T1 +| fpb_cpx : ∀T2. ⦃G1, L1⦄ ⊢ T1 ⬈[h] T2 → (T1 ≛[h, o] T2 → ⊥) → fpb h o G1 L1 T1 G1 L1 T2 +| fpb_lfpx: ∀L2. ⦃G1, L1⦄ ⊢ ⬈[h, T1] L2 → (L1 ≛[h, o, T1] L2 → ⊥) → fpb h o G1 L1 T1 G1 L2 T1 . interpretation @@ -32,11 +32,11 @@ interpretation (* Basic properties *********************************************************) (* Basic_2A1: includes: cpr_fpb *) -lemma cpm_fpb: ∀n,h,o,G,L,T1,T2. ⦃G, L⦄ ⊢ T1 ➡[n, h] T2 → (T1 ≡[h, o] T2 → ⊥) → +lemma cpm_fpb: ∀n,h,o,G,L,T1,T2. ⦃G, L⦄ ⊢ T1 ➡[n, h] T2 → (T1 ≛[h, o] T2 → ⊥) → ⦃G, L, T1⦄ ≻[h, o] ⦃G, L, T2⦄. /3 width=2 by fpb_cpx, cpm_fwd_cpx/ qed. (* Basic_2A1: includes: lpr_fpb *) -lemma lfpr_fpb: ∀h,o,G,L1,L2,T. ⦃G, L1⦄ ⊢ ➡[h, T] L2 → (L1 ≡[h, o, T] L2 → ⊥) → +lemma lfpr_fpb: ∀h,o,G,L1,L2,T. ⦃G, L1⦄ ⊢ ➡[h, T] L2 → (L1 ≛[h, o, T] L2 → ⊥) → ⦃G, L1, T⦄ ≻[h, o] ⦃G, L2, T⦄. /3 width=1 by fpb_lfpx, lfpr_fwd_lfpx/ qed. diff --git a/matita/matita/contribs/lambdadelta/basic_2/rt_transition/fpb_lfdeq.ma b/matita/matita/contribs/lambdadelta/basic_2/rt_transition/fpb_lfdeq.ma index e37aa68f0..1bacae106 100644 --- a/matita/matita/contribs/lambdadelta/basic_2/rt_transition/fpb_lfdeq.ma +++ b/matita/matita/contribs/lambdadelta/basic_2/rt_transition/fpb_lfdeq.ma @@ -22,9 +22,9 @@ include "basic_2/rt_transition/fpb.ma". (* Properties with degree-based equivalence for local environments **********) (* Basic_2A1: was just: lleq_fpb_trans *) -lemma lfdeq_fpb_trans: ∀h,o,F,K1,K2,T. K1 ≡[h, o, T] K2 → +lemma lfdeq_fpb_trans: ∀h,o,F,K1,K2,T. K1 ≛[h, o, T] K2 → ∀G,L2,U. ⦃F, K2, T⦄ ≻[h, o] ⦃G, L2, U⦄ → - ∃∃L1,U0. ⦃F, K1, T⦄ ≻[h, o] ⦃G, L1, U0⦄ & U0 ≡[h, o] U & L1 ≡[h, o, U] L2. + ∃∃L1,U0. ⦃F, K1, T⦄ ≻[h, o] ⦃G, L1, U0⦄ & U0 ≛[h, o] U & L1 ≛[h, o, U] L2. #h #o #F #K1 #K2 #T #HT #G #L2 #U * -G -L2 -U [ #G #L2 #U #H2 elim (lfdeq_fqu_trans … H2 … HT) -K2 /3 width=5 by fpb_fqu, ex3_2_intro/ diff --git a/matita/matita/contribs/lambdadelta/basic_2/rt_transition/lfpx_lfdeq.ma b/matita/matita/contribs/lambdadelta/basic_2/rt_transition/lfpx_lfdeq.ma index 3e7750845..22fe953b4 100644 --- a/matita/matita/contribs/lambdadelta/basic_2/rt_transition/lfpx_lfdeq.ma +++ b/matita/matita/contribs/lambdadelta/basic_2/rt_transition/lfpx_lfdeq.ma @@ -23,19 +23,19 @@ include "basic_2/rt_transition/lfpx.ma". (**) (* should be in lfpx_frees.ma *) (* Properties with degree-based equivalence for local environments **********) lemma lfpx_pair_sn_split: ∀h,G,L1,L2,V. ⦃G, L1⦄ ⊢ ⬈[h, V] L2 → ∀o,I,T. - ∃∃L. ⦃G, L1⦄ ⊢ ⬈[h, ②{I}V.T] L & L ≡[h, o, V] L2. + ∃∃L. ⦃G, L1⦄ ⊢ ⬈[h, ②{I}V.T] L & L ≛[h, o, V] L2. /3 width=5 by lfpx_frees_conf, lfxs_pair_sn_split/ qed-. lemma lfpx_flat_dx_split: ∀h,G,L1,L2,T. ⦃G, L1⦄ ⊢ ⬈[h, T] L2 → ∀o,I,V. - ∃∃L. ⦃G, L1⦄ ⊢ ⬈[h, ⓕ{I}V.T] L & L ≡[h, o, T] L2. + ∃∃L. ⦃G, L1⦄ ⊢ ⬈[h, ⓕ{I}V.T] L & L ≛[h, o, T] L2. /3 width=5 by lfpx_frees_conf, lfxs_flat_dx_split/ qed-. lemma lfpx_bind_dx_split: ∀h,I,G,L1,L2,V1,T. ⦃G, L1.ⓑ{I}V1⦄ ⊢ ⬈[h, T] L2 → ∀o,p. - ∃∃L,V. ⦃G, L1⦄ ⊢ ⬈[h, ⓑ{p,I}V1.T] L & L.ⓑ{I}V ≡[h, o, T] L2 & ⦃G, L1⦄ ⊢ V1 ⬈[h] V. + ∃∃L,V. ⦃G, L1⦄ ⊢ ⬈[h, ⓑ{p,I}V1.T] L & L.ⓑ{I}V ≛[h, o, T] L2 & ⦃G, L1⦄ ⊢ V1 ⬈[h] V. /3 width=5 by lfpx_frees_conf, lfxs_bind_dx_split/ qed-. lemma lfpx_bind_dx_split_void: ∀h,G,K1,L2,T. ⦃G, K1.ⓧ⦄ ⊢ ⬈[h, T] L2 → ∀o,p,I,V. - ∃∃K2. ⦃G, K1⦄ ⊢ ⬈[h, ⓑ{p,I}V.T] K2 & K2.ⓧ ≡[h, o, T] L2. + ∃∃K2. ⦃G, K1⦄ ⊢ ⬈[h, ⓑ{p,I}V.T] K2 & K2.ⓧ ≛[h, o, T] L2. /3 width=5 by lfpx_frees_conf, lfxs_bind_dx_split_void/ qed-. lemma cpx_tdeq_conf_lexs: ∀h,o,G. R_confluent2_lfxs … (cpx h G) (cdeq h o) (cpx h G) (cdeq h o). @@ -119,33 +119,33 @@ lemma cpx_tdeq_conf_lexs: ∀h,o,G. R_confluent2_lfxs … (cpx h G) (cdeq h o) ( qed-. lemma cpx_tdeq_conf: ∀h,o,G,L. ∀T0:term. ∀T1. ⦃G, L⦄ ⊢ T0 ⬈[h] T1 → - ∀T2. T0 ≡[h, o] T2 → - ∃∃T. T1 ≡[h, o] T & ⦃G, L⦄ ⊢ T2 ⬈[h] T. + ∀T2. T0 ≛[h, o] T2 → + ∃∃T. T1 ≛[h, o] T & ⦃G, L⦄ ⊢ T2 ⬈[h] T. #h #o #G #L #T0 #T1 #HT01 #T2 #HT02 elim (cpx_tdeq_conf_lexs … HT01 … HT02 L … L) -HT01 -HT02 /2 width=3 by lfxs_refl, ex2_intro/ qed-. -lemma tdeq_cpx_trans: ∀h,o,G,L,T2. ∀T0:term. T2 ≡[h, o] T0 → +lemma tdeq_cpx_trans: ∀h,o,G,L,T2. ∀T0:term. T2 ≛[h, o] T0 → ∀T1. ⦃G, L⦄ ⊢ T0 ⬈[h] T1 → - ∃∃T. ⦃G, L⦄ ⊢ T2 ⬈[h] T & T ≡[h, o] T1. + ∃∃T. ⦃G, L⦄ ⊢ T2 ⬈[h] T & T ≛[h, o] T1. #h #o #G #L #T2 #T0 #HT20 #T1 #HT01 elim (cpx_tdeq_conf … HT01 T2) -HT01 /3 width=3 by tdeq_sym, ex2_intro/ qed-. (* Basic_2A1: uses: cpx_lleq_conf *) lemma cpx_lfdeq_conf: ∀h,o,G,L0,T0,T1. ⦃G, L0⦄ ⊢ T0 ⬈[h] T1 → - ∀L2. L0 ≡[h, o, T0] L2 → - ∃∃T. ⦃G, L2⦄ ⊢ T0 ⬈[h] T & T1 ≡[h, o] T. + ∀L2. L0 ≛[h, o, T0] L2 → + ∃∃T. ⦃G, L2⦄ ⊢ T0 ⬈[h] T & T1 ≛[h, o] T. #h #o #G #L0 #T0 #T1 #HT01 #L2 #HL02 elim (cpx_tdeq_conf_lexs … HT01 T0 … L0 … HL02) -HT01 -HL02 /2 width=3 by lfxs_refl, ex2_intro/ qed-. (* Basic_2A1: uses: lleq_cpx_trans *) -lemma lfdeq_cpx_trans: ∀h,o,G,L2,L0,T0. L2 ≡[h, o, T0] L0 → +lemma lfdeq_cpx_trans: ∀h,o,G,L2,L0,T0. L2 ≛[h, o, T0] L0 → ∀T1. ⦃G, L0⦄ ⊢ T0 ⬈[h] T1 → - ∃∃T. ⦃G, L2⦄ ⊢ T0 ⬈[h] T & T ≡[h, o] T1. + ∃∃T. ⦃G, L2⦄ ⊢ T0 ⬈[h] T & T ≛[h, o] T1. #h #o #G #L2 #L0 #T0 #HL20 #T1 #HT01 elim (cpx_lfdeq_conf … o … HT01 L2) -HT01 /3 width=3 by lfdeq_sym, tdeq_sym, ex2_intro/ @@ -156,8 +156,8 @@ lemma lfpx_lfdeq_conf: ∀h,o,G,T. confluent2 … (lfpx h G T) (lfdeq h o T). (* Basic_2A1: uses: lleq_lpx_trans *) lemma lfdeq_lfpx_trans: ∀h,o,G,T,L2,K2. ⦃G, L2⦄ ⊢ ⬈[h, T] K2 → - ∀L1. L1 ≡[h, o, T] L2 → - ∃∃K1. ⦃G, L1⦄ ⊢ ⬈[h, T] K1 & K1 ≡[h, o, T] K2. + ∀L1. L1 ≛[h, o, T] L2 → + ∃∃K1. ⦃G, L1⦄ ⊢ ⬈[h, T] K1 & K1 ≛[h, o, T] K2. #h #o #G #T #L2 #K2 #HLK2 #L1 #HL12 elim (lfpx_lfdeq_conf … o … HLK2 L1) /3 width=3 by lfdeq_sym, ex2_intro/ diff --git a/matita/matita/contribs/lambdadelta/basic_2/static/aaa_lfdeq.ma b/matita/matita/contribs/lambdadelta/basic_2/static/aaa_lfdeq.ma index e43f544cf..e71dbe35e 100644 --- a/matita/matita/contribs/lambdadelta/basic_2/static/aaa_lfdeq.ma +++ b/matita/matita/contribs/lambdadelta/basic_2/static/aaa_lfdeq.ma @@ -19,8 +19,8 @@ include "basic_2/static/aaa.ma". (* Properties with degree-based equivalence on referred entries *************) -lemma aaa_tdeq_conf_fldeq: ∀h,o,G,L1,T1,A. ⦃G, L1⦄ ⊢ T1 ⁝ A → ∀T2. T1 ≡[h, o] T2 → - ∀L2. L1 ≡[h, o, T1] L2 → ⦃G, L2⦄ ⊢ T2 ⁝ A. +lemma aaa_tdeq_conf_fldeq: ∀h,o,G,L1,T1,A. ⦃G, L1⦄ ⊢ T1 ⁝ A → ∀T2. T1 ≛[h, o] T2 → + ∀L2. L1 ≛[h, o, T1] L2 → ⦃G, L2⦄ ⊢ T2 ⁝ A. #h #o #G #L1 #T1 #A #H elim H -G -L1 -T1 -A [ #G #L1 #s1 #X #H1 elim (tdeq_inv_sort1 … H1) -H1 // | #I #G #L1 #V1 #B #_ #IH #X #H1 >(tdeq_inv_lref1 … H1) -H1 diff --git a/matita/matita/contribs/lambdadelta/basic_2/static/ffdeq.ma b/matita/matita/contribs/lambdadelta/basic_2/static/ffdeq.ma index fa2277996..ef74ef3c4 100644 --- a/matita/matita/contribs/lambdadelta/basic_2/static/ffdeq.ma +++ b/matita/matita/contribs/lambdadelta/basic_2/static/ffdeq.ma @@ -12,19 +12,19 @@ (* *) (**************************************************************************) -include "basic_2/notation/relations/lazyeqsn_8.ma". +include "basic_2/notation/relations/stareqsn_8.ma". include "basic_2/syntax/genv.ma". include "basic_2/static/lfdeq.ma". (* DEGREE-BASED EQUIVALENCE FOR CLOSURES ON REFERRED ENTRIES ****************) inductive ffdeq (h) (o) (G) (L1) (T): relation3 genv lenv term ≝ -| ffdeq_intro: ∀L2. L1 ≡[h, o, T] L2 → ffdeq h o G L1 T G L2 T +| ffdeq_intro: ∀L2. L1 ≛[h, o, T] L2 → ffdeq h o G L1 T G L2 T . interpretation "degree-based equivalence on referred entries (closure)" - 'LazyEqSn h o G1 L1 T1 G2 L2 T2 = (ffdeq h o G1 L1 T1 G2 L2 T2). + 'StarEqSn h o G1 L1 T1 G2 L2 T2 = (ffdeq h o G1 L1 T1 G2 L2 T2). (* Basic properties *********************************************************) @@ -34,8 +34,8 @@ qed-. (* Basic inversion lemmas ***************************************************) -lemma ffdeq_inv_gen: ∀h,o,G1,G2,L1,L2,T1,T2. ⦃G1, L1, T1⦄ ≡[h, o] ⦃G2, L2, T2⦄ → - ∧∧ G1 = G2 & L1 ≡[h, o, T1] L2 & T1 = T2. +lemma ffdeq_inv_gen: ∀h,o,G1,G2,L1,L2,T1,T2. ⦃G1, L1, T1⦄ ≛[h, o] ⦃G2, L2, T2⦄ → + ∧∧ G1 = G2 & L1 ≛[h, o, T1] L2 & T1 = T2. #h #o #G1 #G2 #L1 #L2 #T1 #T2 * -G2 -L2 -T2 /2 width=1 by and3_intro/ qed-. diff --git a/matita/matita/contribs/lambdadelta/basic_2/static/ffdeq_ffdeq.ma b/matita/matita/contribs/lambdadelta/basic_2/static/ffdeq_ffdeq.ma index 46400a913..47a38804c 100644 --- a/matita/matita/contribs/lambdadelta/basic_2/static/ffdeq_ffdeq.ma +++ b/matita/matita/contribs/lambdadelta/basic_2/static/ffdeq_ffdeq.ma @@ -25,9 +25,9 @@ theorem ffdeq_trans: ∀h,o. tri_transitive … (ffdeq h o). qed-. theorem ffdeq_canc_sn: ∀h,o,G,G1,G2,L,L1,L2,T,T1,T2. - ⦃G, L, T⦄ ≡[h, o] ⦃G1, L1, T1⦄→ ⦃G, L, T⦄ ≡[h, o] ⦃G2, L2, T2⦄ → ⦃G1, L1, T1⦄ ≡[h, o] ⦃G2, L2, T2⦄. + ⦃G, L, T⦄ ≛[h, o] ⦃G1, L1, T1⦄→ ⦃G, L, T⦄ ≛[h, o] ⦃G2, L2, T2⦄ → ⦃G1, L1, T1⦄ ≛[h, o] ⦃G2, L2, T2⦄. /3 width=5 by ffdeq_trans, ffdeq_sym/ qed-. theorem ffdeq_canc_dx: ∀h,o,G1,G2,G,L1,L2,L,T1,T2,T. - ⦃G1, L1, T1⦄ ≡[h, o] ⦃G, L, T⦄ → ⦃G2, L2, T2⦄ ≡[h, o] ⦃G, L, T⦄ → ⦃G1, L1, T1⦄ ≡[h, o] ⦃G2, L2, T2⦄. + ⦃G1, L1, T1⦄ ≛[h, o] ⦃G, L, T⦄ → ⦃G2, L2, T2⦄ ≛[h, o] ⦃G, L, T⦄ → ⦃G1, L1, T1⦄ ≛[h, o] ⦃G2, L2, T2⦄. /3 width=5 by ffdeq_trans, ffdeq_sym/ qed-. diff --git a/matita/matita/contribs/lambdadelta/basic_2/static/lfdeq.ma b/matita/matita/contribs/lambdadelta/basic_2/static/lfdeq.ma index 9123e9121..8a770328f 100644 --- a/matita/matita/contribs/lambdadelta/basic_2/static/lfdeq.ma +++ b/matita/matita/contribs/lambdadelta/basic_2/static/lfdeq.ma @@ -12,7 +12,7 @@ (* *) (**************************************************************************) -include "basic_2/notation/relations/lazyeqsn_5.ma". +include "basic_2/notation/relations/stareqsn_5.ma". include "basic_2/syntax/tdeq_ext.ma". include "basic_2/static/lfxs.ma". @@ -23,19 +23,19 @@ definition lfdeq: ∀h. sd h → relation3 term lenv lenv ≝ interpretation "degree-based equivalence on referred entries (local environment)" - 'LazyEqSn h o T L1 L2 = (lfdeq h o T L1 L2). + 'StarEqSn h o T L1 L2 = (lfdeq h o T L1 L2). interpretation "degree-based ranged equivalence (local environment)" - 'LazyEqSn h o f L1 L2 = (lexs (cdeq_ext h o) cfull f L1 L2). + 'StarEqSn h o f L1 L2 = (lexs (cdeq_ext h o) cfull f L1 L2). (* definition lfdeq_transitive: predicate (relation3 lenv term term) ≝ - λR. ∀L2,T1,T2. R L2 T1 T2 → ∀L1. L1 ≡[h, o, T1] L2 → R L1 T1 T2. + λR. ∀L2,T1,T2. R L2 T1 T2 → ∀L1. L1 ≛[h, o, T1] L2 → R L1 T1 T2. *) (* Basic properties ***********************************************************) -lemma frees_tdeq_conf_lexs: ∀h,o,f,L1,T1. L1 ⊢ 𝐅*⦃T1⦄ ≡ f → ∀T2. T1 ≡[h, o] T2 → - ∀L2. L1 ≡[h, o, f] L2 → L2 ⊢ 𝐅*⦃T2⦄ ≡ f. +lemma frees_tdeq_conf_lexs: ∀h,o,f,L1,T1. L1 ⊢ 𝐅*⦃T1⦄ ≡ f → ∀T2. T1 ≛[h, o] T2 → + ∀L2. L1 ≛[h, o, f] L2 → L2 ⊢ 𝐅*⦃T2⦄ ≡ f. #h #o #f #L1 #T1 #H elim H -f -L1 -T1 [ #f #L1 #s1 #Hf #X #H1 #L2 #_ elim (tdeq_inv_sort1 … H1) -H1 #s2 #d #_ #_ #H destruct @@ -69,11 +69,11 @@ lemma frees_tdeq_conf_lexs: ∀h,o,f,L1,T1. L1 ⊢ 𝐅*⦃T1⦄ ≡ f → ∀T2 qed-. lemma frees_tdeq_conf: ∀h,o,f,L,T1. L ⊢ 𝐅*⦃T1⦄ ≡ f → - ∀T2. T1 ≡[h, o] T2 → L ⊢ 𝐅*⦃T2⦄ ≡ f. + ∀T2. T1 ≛[h, o] T2 → L ⊢ 𝐅*⦃T2⦄ ≡ f. /4 width=7 by frees_tdeq_conf_lexs, lexs_refl, ext2_refl/ qed-. lemma frees_lexs_conf: ∀h,o,f,L1,T. L1 ⊢ 𝐅*⦃T⦄ ≡ f → - ∀L2. L1 ≡[h, o, f] L2 → L2 ⊢ 𝐅*⦃T⦄ ≡ f. + ∀L2. L1 ≛[h, o, f] L2 → L2 ⊢ 𝐅*⦃T⦄ ≡ f. /2 width=7 by frees_tdeq_conf_lexs, tdeq_refl/ qed-. lemma frees_lfdeq_conf_lexs: ∀h,o. lexs_frees_confluent (cdeq_ext h o) cfull. @@ -90,48 +90,48 @@ lemma lfdeq_sym: ∀h,o,T. symmetric … (lfdeq h o T). /4 width=7 by frees_tdeq_conf_lexs, lfxs_sym, tdeq_sym, ex2_intro/ qed-. -lemma lfdeq_atom: ∀h,o,I. ⋆ ≡[h, o, ⓪{I}] ⋆. +lemma lfdeq_atom: ∀h,o,I. ⋆ ≛[h, o, ⓪{I}] ⋆. /2 width=1 by lfxs_atom/ qed. (* Basic_2A1: uses: lleq_sort *) lemma lfdeq_sort: ∀h,o,I1,I2,L1,L2,s. - L1 ≡[h, o, ⋆s] L2 → L1.ⓘ{I1} ≡[h, o, ⋆s] L2.ⓘ{I2}. + L1 ≛[h, o, ⋆s] L2 → L1.ⓘ{I1} ≛[h, o, ⋆s] L2.ⓘ{I2}. /2 width=1 by lfxs_sort/ qed. -lemma lfdeq_pair: ∀h,o,I,L1,L2,V1,V2. L1 ≡[h, o, V1] L2 → V1 ≡[h, o] V2 → - L1.ⓑ{I}V1 ≡[h, o, #0] L2.ⓑ{I}V2. +lemma lfdeq_pair: ∀h,o,I,L1,L2,V1,V2. L1 ≛[h, o, V1] L2 → V1 ≛[h, o] V2 → + L1.ⓑ{I}V1 ≛[h, o, #0] L2.ⓑ{I}V2. /2 width=1 by lfxs_pair/ qed. (* lemma lfdeq_unit: ∀h,o,f,I,L1,L2. 𝐈⦃f⦄ → L1 ⪤*[cdeq_ext h o, cfull, f] L2 → - L1.ⓤ{I} ≡[h, o, #0] L2.ⓤ{I}. + L1.ⓤ{I} ≛[h, o, #0] L2.ⓤ{I}. /2 width=3 by lfxs_unit/ qed. *) lemma lfdeq_lref: ∀h,o,I1,I2,L1,L2,i. - L1 ≡[h, o, #i] L2 → L1.ⓘ{I1} ≡[h, o, #⫯i] L2.ⓘ{I2}. + L1 ≛[h, o, #i] L2 → L1.ⓘ{I1} ≛[h, o, #⫯i] L2.ⓘ{I2}. /2 width=1 by lfxs_lref/ qed. (* Basic_2A1: uses: lleq_gref *) lemma lfdeq_gref: ∀h,o,I1,I2,L1,L2,l. - L1 ≡[h, o, §l] L2 → L1.ⓘ{I1} ≡[h, o, §l] L2.ⓘ{I2}. + L1 ≛[h, o, §l] L2 → L1.ⓘ{I1} ≛[h, o, §l] L2.ⓘ{I2}. /2 width=1 by lfxs_gref/ qed. lemma lfdeq_bind_repl_dx: ∀h,o,I,I1,L1,L2.∀T:term. - L1.ⓘ{I} ≡[h, o, T] L2.ⓘ{I1} → - ∀I2. I ≡[h, o] I2 → - L1.ⓘ{I} ≡[h, o, T] L2.ⓘ{I2}. + L1.ⓘ{I} ≛[h, o, T] L2.ⓘ{I1} → + ∀I2. I ≛[h, o] I2 → + L1.ⓘ{I} ≛[h, o, T] L2.ⓘ{I2}. /2 width=2 by lfxs_bind_repl_dx/ qed-. (* Basic inversion lemmas ***************************************************) -lemma lfdeq_inv_atom_sn: ∀h,o,Y2. ∀T:term. ⋆ ≡[h, o, T] Y2 → Y2 = ⋆. +lemma lfdeq_inv_atom_sn: ∀h,o,Y2. ∀T:term. ⋆ ≛[h, o, T] Y2 → Y2 = ⋆. /2 width=3 by lfxs_inv_atom_sn/ qed-. -lemma lfdeq_inv_atom_dx: ∀h,o,Y1. ∀T:term. Y1 ≡[h, o, T] ⋆ → Y1 = ⋆. +lemma lfdeq_inv_atom_dx: ∀h,o,Y1. ∀T:term. Y1 ≛[h, o, T] ⋆ → Y1 = ⋆. /2 width=3 by lfxs_inv_atom_dx/ qed-. (* -lemma lfdeq_inv_zero: ∀h,o,Y1,Y2. Y1 ≡[h, o, #0] Y2 → +lemma lfdeq_inv_zero: ∀h,o,Y1,Y2. Y1 ≛[h, o, #0] Y2 → ∨∨ Y1 = ⋆ ∧ Y2 = ⋆ - | ∃∃I,L1,L2,V1,V2. L1 ≡[h, o, V1] L2 & V1 ≡[h, o] V2 & + | ∃∃I,L1,L2,V1,V2. L1 ≛[h, o, V1] L2 & V1 ≛[h, o] V2 & Y1 = L1.ⓑ{I}V1 & Y2 = L2.ⓑ{I}V2 | ∃∃f,I,L1,L2. 𝐈⦃f⦄ & L1 ⪤*[cdeq_ext h o, cfull, f] L2 & Y1 = L1.ⓤ{I} & Y2 = L2.ⓤ{I}. @@ -139,60 +139,60 @@ lemma lfdeq_inv_zero: ∀h,o,Y1,Y2. Y1 ≡[h, o, #0] Y2 → /3 width=9 by or3_intro0, or3_intro1, or3_intro2, ex4_5_intro, ex4_4_intro, conj/ qed-. *) -lemma lfdeq_inv_lref: ∀h,o,Y1,Y2,i. Y1 ≡[h, o, #⫯i] Y2 → +lemma lfdeq_inv_lref: ∀h,o,Y1,Y2,i. Y1 ≛[h, o, #⫯i] Y2 → (Y1 = ⋆ ∧ Y2 = ⋆) ∨ - ∃∃I1,I2,L1,L2. L1 ≡[h, o, #i] L2 & + ∃∃I1,I2,L1,L2. L1 ≛[h, o, #i] L2 & Y1 = L1.ⓘ{I1} & Y2 = L2.ⓘ{I2}. /2 width=1 by lfxs_inv_lref/ qed-. (* Basic_2A1: uses: lleq_inv_bind lleq_inv_bind_O *) -lemma lfdeq_inv_bind: ∀h,o,p,I,L1,L2,V,T. L1 ≡[h, o, ⓑ{p,I}V.T] L2 → - L1 ≡[h, o, V] L2 ∧ L1.ⓑ{I}V ≡[h, o, T] L2.ⓑ{I}V. +lemma lfdeq_inv_bind: ∀h,o,p,I,L1,L2,V,T. L1 ≛[h, o, ⓑ{p,I}V.T] L2 → + L1 ≛[h, o, V] L2 ∧ L1.ⓑ{I}V ≛[h, o, T] L2.ⓑ{I}V. /2 width=2 by lfxs_inv_bind/ qed-. (* Basic_2A1: uses: lleq_inv_flat *) -lemma lfdeq_inv_flat: ∀h,o,I,L1,L2,V,T. L1 ≡[h, o, ⓕ{I}V.T] L2 → - L1 ≡[h, o, V] L2 ∧ L1 ≡[h, o, T] L2. +lemma lfdeq_inv_flat: ∀h,o,I,L1,L2,V,T. L1 ≛[h, o, ⓕ{I}V.T] L2 → + L1 ≛[h, o, V] L2 ∧ L1 ≛[h, o, T] L2. /2 width=2 by lfxs_inv_flat/ qed-. (* Advanced inversion lemmas ************************************************) -lemma lfdeq_inv_zero_pair_sn: ∀h,o,I,Y2,L1,V1. L1.ⓑ{I}V1 ≡[h, o, #0] Y2 → - ∃∃L2,V2. L1 ≡[h, o, V1] L2 & V1 ≡[h, o] V2 & Y2 = L2.ⓑ{I}V2. +lemma lfdeq_inv_zero_pair_sn: ∀h,o,I,Y2,L1,V1. L1.ⓑ{I}V1 ≛[h, o, #0] Y2 → + ∃∃L2,V2. L1 ≛[h, o, V1] L2 & V1 ≛[h, o] V2 & Y2 = L2.ⓑ{I}V2. /2 width=1 by lfxs_inv_zero_pair_sn/ qed-. -lemma lfdeq_inv_zero_pair_dx: ∀h,o,I,Y1,L2,V2. Y1 ≡[h, o, #0] L2.ⓑ{I}V2 → - ∃∃L1,V1. L1 ≡[h, o, V1] L2 & V1 ≡[h, o] V2 & Y1 = L1.ⓑ{I}V1. +lemma lfdeq_inv_zero_pair_dx: ∀h,o,I,Y1,L2,V2. Y1 ≛[h, o, #0] L2.ⓑ{I}V2 → + ∃∃L1,V1. L1 ≛[h, o, V1] L2 & V1 ≛[h, o] V2 & Y1 = L1.ⓑ{I}V1. /2 width=1 by lfxs_inv_zero_pair_dx/ qed-. -lemma lfdeq_inv_lref_bind_sn: ∀h,o,I1,Y2,L1,i. L1.ⓘ{I1} ≡[h, o, #⫯i] Y2 → - ∃∃I2,L2. L1 ≡[h, o, #i] L2 & Y2 = L2.ⓘ{I2}. +lemma lfdeq_inv_lref_bind_sn: ∀h,o,I1,Y2,L1,i. L1.ⓘ{I1} ≛[h, o, #⫯i] Y2 → + ∃∃I2,L2. L1 ≛[h, o, #i] L2 & Y2 = L2.ⓘ{I2}. /2 width=2 by lfxs_inv_lref_bind_sn/ qed-. -lemma lfdeq_inv_lref_bind_dx: ∀h,o,I2,Y1,L2,i. Y1 ≡[h, o, #⫯i] L2.ⓘ{I2} → - ∃∃I1,L1. L1 ≡[h, o, #i] L2 & Y1 = L1.ⓘ{I1}. +lemma lfdeq_inv_lref_bind_dx: ∀h,o,I2,Y1,L2,i. Y1 ≛[h, o, #⫯i] L2.ⓘ{I2} → + ∃∃I1,L1. L1 ≛[h, o, #i] L2 & Y1 = L1.ⓘ{I1}. /2 width=2 by lfxs_inv_lref_bind_dx/ qed-. (* Basic forward lemmas *****************************************************) lemma lfdeq_fwd_zero_pair: ∀h,o,I,K1,K2,V1,V2. - K1.ⓑ{I}V1 ≡[h, o, #0] K2.ⓑ{I}V2 → K1 ≡[h, o, V1] K2. + K1.ⓑ{I}V1 ≛[h, o, #0] K2.ⓑ{I}V2 → K1 ≛[h, o, V1] K2. /2 width=3 by lfxs_fwd_zero_pair/ qed-. (* Basic_2A1: uses: lleq_fwd_bind_sn lleq_fwd_flat_sn *) -lemma lfdeq_fwd_pair_sn: ∀h,o,I,L1,L2,V,T. L1 ≡[h, o, ②{I}V.T] L2 → L1 ≡[h, o, V] L2. +lemma lfdeq_fwd_pair_sn: ∀h,o,I,L1,L2,V,T. L1 ≛[h, o, ②{I}V.T] L2 → L1 ≛[h, o, V] L2. /2 width=3 by lfxs_fwd_pair_sn/ qed-. (* Basic_2A1: uses: lleq_fwd_bind_dx lleq_fwd_bind_O_dx *) lemma lfdeq_fwd_bind_dx: ∀h,o,p,I,L1,L2,V,T. - L1 ≡[h, o, ⓑ{p,I}V.T] L2 → L1.ⓑ{I}V ≡[h, o, T] L2.ⓑ{I}V. + L1 ≛[h, o, ⓑ{p,I}V.T] L2 → L1.ⓑ{I}V ≛[h, o, T] L2.ⓑ{I}V. /2 width=2 by lfxs_fwd_bind_dx/ qed-. (* Basic_2A1: uses: lleq_fwd_flat_dx *) -lemma lfdeq_fwd_flat_dx: ∀h,o,I,L1,L2,V,T. L1 ≡[h, o, ⓕ{I}V.T] L2 → L1 ≡[h, o, T] L2. +lemma lfdeq_fwd_flat_dx: ∀h,o,I,L1,L2,V,T. L1 ≛[h, o, ⓕ{I}V.T] L2 → L1 ≛[h, o, T] L2. /2 width=3 by lfxs_fwd_flat_dx/ qed-. -lemma lfdeq_fwd_dx: ∀h,o,I2,L1,K2. ∀T:term. L1 ≡[h, o, T] K2.ⓘ{I2} → +lemma lfdeq_fwd_dx: ∀h,o,I2,L1,K2. ∀T:term. L1 ≛[h, o, T] K2.ⓘ{I2} → ∃∃I1,K1. L1 = K1.ⓘ{I1}. /2 width=5 by lfxs_fwd_dx/ qed-. diff --git a/matita/matita/contribs/lambdadelta/basic_2/static/lfdeq_drops.ma b/matita/matita/contribs/lambdadelta/basic_2/static/lfdeq_drops.ma index 4b8f2f92b..f77f0a0ff 100644 --- a/matita/matita/contribs/lambdadelta/basic_2/static/lfdeq_drops.ma +++ b/matita/matita/contribs/lambdadelta/basic_2/static/lfdeq_drops.ma @@ -33,15 +33,15 @@ lemma lfdeq_inv_lifts_dx: ∀h,o. dropable_dx (cdeq h o). /2 width=5 by lfxs_dropable_dx/ qed-. (* Basic_2A1: uses: lleq_inv_lift_le lleq_inv_lift_be lleq_inv_lift_ge *) -lemma lfdeq_inv_lifts_bi: ∀h,o,L1,L2,U. L1 ≡[h, o, U] L2 → ∀b,f. 𝐔⦃f⦄ → +lemma lfdeq_inv_lifts_bi: ∀h,o,L1,L2,U. L1 ≛[h, o, U] L2 → ∀b,f. 𝐔⦃f⦄ → ∀K1,K2. ⬇*[b, f] L1 ≡ K1 → ⬇*[b, f] L2 ≡ K2 → - ∀T. ⬆*[f] T ≡ U → K1 ≡[h, o, T] K2. + ∀T. ⬆*[f] T ≡ U → K1 ≛[h, o, T] K2. /2 width=10 by lfxs_inv_lifts_bi/ qed-. -lemma lfdeq_inv_lref_pair_sn: ∀h,o,L1,L2,i. L1 ≡[h, o, #i] L2 → ∀I,K1,V1. ⬇*[i] L1 ≡ K1.ⓑ{I}V1 → - ∃∃K2,V2. ⬇*[i] L2 ≡ K2.ⓑ{I}V2 & K1 ≡[h, o, V1] K2 & V1 ≡[h, o] V2. +lemma lfdeq_inv_lref_pair_sn: ∀h,o,L1,L2,i. L1 ≛[h, o, #i] L2 → ∀I,K1,V1. ⬇*[i] L1 ≡ K1.ⓑ{I}V1 → + ∃∃K2,V2. ⬇*[i] L2 ≡ K2.ⓑ{I}V2 & K1 ≛[h, o, V1] K2 & V1 ≛[h, o] V2. /2 width=3 by lfxs_inv_lref_pair_sn/ qed-. -lemma lfdeq_inv_lref_pair_dx: ∀h,o,L1,L2,i. L1 ≡[h, o, #i] L2 → ∀I,K2,V2. ⬇*[i] L2 ≡ K2.ⓑ{I}V2 → - ∃∃K1,V1. ⬇*[i] L1 ≡ K1.ⓑ{I}V1 & K1 ≡[h, o, V1] K2 & V1 ≡[h, o] V2. +lemma lfdeq_inv_lref_pair_dx: ∀h,o,L1,L2,i. L1 ≛[h, o, #i] L2 → ∀I,K2,V2. ⬇*[i] L2 ≡ K2.ⓑ{I}V2 → + ∃∃K1,V1. ⬇*[i] L1 ≡ K1.ⓑ{I}V1 & K1 ≛[h, o, V1] K2 & V1 ≛[h, o] V2. /2 width=3 by lfxs_inv_lref_pair_dx/ qed-. diff --git a/matita/matita/contribs/lambdadelta/basic_2/static/lfdeq_fqup.ma b/matita/matita/contribs/lambdadelta/basic_2/static/lfdeq_fqup.ma index 855c83b74..78320e1b1 100644 --- a/matita/matita/contribs/lambdadelta/basic_2/static/lfdeq_fqup.ma +++ b/matita/matita/contribs/lambdadelta/basic_2/static/lfdeq_fqup.ma @@ -23,18 +23,18 @@ include "basic_2/static/lfdeq.ma". lemma lfdeq_refl: ∀h,o,T. reflexive … (lfdeq h o T). /2 width=1 by lfxs_refl/ qed. -lemma lfdeq_pair_refl: ∀h,o,V1,V2. V1 ≡[h, o] V2 → - ∀I,L. ∀T:term. L.ⓑ{I}V1 ≡[h, o, T] L.ⓑ{I}V2. +lemma lfdeq_pair_refl: ∀h,o,V1,V2. V1 ≛[h, o] V2 → + ∀I,L. ∀T:term. L.ⓑ{I}V1 ≛[h, o, T] L.ⓑ{I}V2. /2 width=1 by lfxs_pair_refl/ qed. (* Advanced inversion lemmas ************************************************) -lemma lfdeq_inv_bind_void: ∀h,o,p,I,L1,L2,V,T. L1 ≡[h, o, ⓑ{p,I}V.T] L2 → - L1 ≡[h, o, V] L2 ∧ L1.ⓧ ≡[h, o, T] L2.ⓧ. +lemma lfdeq_inv_bind_void: ∀h,o,p,I,L1,L2,V,T. L1 ≛[h, o, ⓑ{p,I}V.T] L2 → + L1 ≛[h, o, V] L2 ∧ L1.ⓧ ≛[h, o, T] L2.ⓧ. /2 width=3 by lfxs_inv_bind_void/ qed-. (* Advanced forward lemmas **************************************************) lemma lfdeq_fwd_bind_dx_void: ∀h,o,p,I,L1,L2,V,T. - L1 ≡[h, o, ⓑ{p,I}V.T] L2 → L1.ⓧ ≡[h, o, T] L2.ⓧ. + L1 ≛[h, o, ⓑ{p,I}V.T] L2 → L1.ⓧ ≛[h, o, T] L2.ⓧ. /2 width=4 by lfxs_fwd_bind_dx_void/ qed-. diff --git a/matita/matita/contribs/lambdadelta/basic_2/static/lfdeq_fqus.ma b/matita/matita/contribs/lambdadelta/basic_2/static/lfdeq_fqus.ma index 58cf547d6..9d4c4a67b 100644 --- a/matita/matita/contribs/lambdadelta/basic_2/static/lfdeq_fqus.ma +++ b/matita/matita/contribs/lambdadelta/basic_2/static/lfdeq_fqus.ma @@ -22,8 +22,8 @@ include "basic_2/static/lfdeq_lfdeq.ma". (* Properties with supclosure ***********************************************) lemma fqu_tdeq_conf: ∀h,o,b,G1,G2,L1,L2,U1,T1. ⦃G1, L1, U1⦄ ⊐[b] ⦃G2, L2, T1⦄ → - ∀U2. U1 ≡[h, o] U2 → - ∃∃L,T2. ⦃G1, L1, U2⦄ ⊐[b] ⦃G2, L, T2⦄ & L2 ≡[h, o, T1] L & T1 ≡[h, o] T2. + ∀U2. U1 ≛[h, o] U2 → + ∃∃L,T2. ⦃G1, L1, U2⦄ ⊐[b] ⦃G2, L, T2⦄ & L2 ≛[h, o, T1] L & T1 ≛[h, o] T2. #h #o #b #G1 #G2 #L1 #L2 #U1 #T1 #H elim H -G1 -G2 -L1 -L2 -U1 -T1 [ #I #G #L #W #X #H >(tdeq_inv_lref1 … H) -X /2 width=5 by fqu_lref_O, ex3_2_intro/ @@ -46,8 +46,8 @@ lemma fqu_tdeq_conf: ∀h,o,b,G1,G2,L1,L2,U1,T1. ⦃G1, L1, U1⦄ ⊐[b] ⦃G2, qed-. lemma tdeq_fqu_trans: ∀h,o,b,G1,G2,L1,L2,U1,T1. ⦃G1, L1, U1⦄ ⊐[b] ⦃G2, L2, T1⦄ → - ∀U2. U2 ≡[h, o] U1 → - ∃∃L,T2. ⦃G1, L1, U2⦄ ⊐[b] ⦃G2, L, T2⦄ & T2 ≡[h, o] T1 & L ≡[h, o, T1] L2. + ∀U2. U2 ≛[h, o] U1 → + ∃∃L,T2. ⦃G1, L1, U2⦄ ⊐[b] ⦃G2, L, T2⦄ & T2 ≛[h, o] T1 & L ≛[h, o, T1] L2. #h #o #b #G1 #G2 #L1 #L2 #U1 #T1 #H12 #U2 #HU21 elim (fqu_tdeq_conf … o … H12 U2) -H12 /3 width=5 by lfdeq_sym, tdeq_sym, ex3_2_intro/ @@ -55,8 +55,8 @@ qed-. (* Basic_2A1: was just: lleq_fqu_trans *) lemma lfdeq_fqu_trans: ∀h,o,b,G1,G2,L2,K2,T,U. ⦃G1, L2, T⦄ ⊐[b] ⦃G2, K2, U⦄ → - ∀L1. L1 ≡[h, o, T] L2 → - ∃∃K1,U0. ⦃G1, L1, T⦄ ⊐[b] ⦃G2, K1, U0⦄ & U0 ≡[h, o] U & K1 ≡[h, o, U] K2. + ∀L1. L1 ≛[h, o, T] L2 → + ∃∃K1,U0. ⦃G1, L1, T⦄ ⊐[b] ⦃G2, K1, U0⦄ & U0 ≛[h, o] U & K1 ≛[h, o, U] K2. #h #o #b #G1 #G2 #L2 #K2 #T #U #H elim H -G1 -G2 -L2 -K2 -T -U [ #I #G #L2 #V2 #L1 #H elim (lfdeq_inv_zero_pair_dx … H) -H #K1 #V1 #HV1 #HV12 #H destruct @@ -80,8 +80,8 @@ qed-. (* Basic_2A1: was just: lleq_fquq_trans *) lemma lfdeq_fquq_trans: ∀h,o,b,G1,G2,L2,K2,T,U. ⦃G1, L2, T⦄ ⊐⸮[b] ⦃G2, K2, U⦄ → - ∀L1. L1 ≡[h, o, T] L2 → - ∃∃K1,U0. ⦃G1, L1, T⦄ ⊐⸮[b] ⦃G2, K1, U0⦄ & U0 ≡[h, o] U & K1 ≡[h, o, U] K2. + ∀L1. L1 ≛[h, o, T] L2 → + ∃∃K1,U0. ⦃G1, L1, T⦄ ⊐⸮[b] ⦃G2, K1, U0⦄ & U0 ≛[h, o] U & K1 ≛[h, o, U] K2. #h #o #b #G1 #G2 #L2 #K2 #T #U #H elim H -H [ #H #L1 #HL12 elim (lfdeq_fqu_trans … H … HL12) -L2 /3 width=5 by fqu_fquq, ex3_2_intro/ | * #HG #HL #HT destruct /2 width=5 by ex3_2_intro/ @@ -90,8 +90,8 @@ qed-. (* Basic_2A1: was just: lleq_fqup_trans *) lemma lfdeq_fqup_trans: ∀h,o,b,G1,G2,L2,K2,T,U. ⦃G1, L2, T⦄ ⊐+[b] ⦃G2, K2, U⦄ → - ∀L1. L1 ≡[h, o, T] L2 → - ∃∃K1,U0. ⦃G1, L1, T⦄ ⊐+[b] ⦃G2, K1, U0⦄ & U0 ≡[h, o] U & K1 ≡[h, o, U] K2. + ∀L1. L1 ≛[h, o, T] L2 → + ∃∃K1,U0. ⦃G1, L1, T⦄ ⊐+[b] ⦃G2, K1, U0⦄ & U0 ≛[h, o] U & K1 ≛[h, o, U] K2. #h #o #b #G1 #G2 #L2 #K2 #T #U #H @(fqup_ind … H) -G2 -K2 -U [ #G2 #K2 #U #HTU #L1 #HL12 elim (lfdeq_fqu_trans … HTU … HL12) -L2 /3 width=5 by fqu_fqup, ex3_2_intro/ @@ -106,8 +106,8 @@ qed-. (* Basic_2A1: was just: lleq_fqus_trans *) lemma lfdeq_fqus_trans: ∀h,o,b,G1,G2,L2,K2,T,U. ⦃G1, L2, T⦄ ⊐*[b] ⦃G2, K2, U⦄ → - ∀L1. L1 ≡[h, o, T] L2 → - ∃∃K1,U0. ⦃G1, L1, T⦄ ⊐*[b] ⦃G2, K1, U0⦄ & U0 ≡[h, o] U & K1 ≡[h, o, U] K2. + ∀L1. L1 ≛[h, o, T] L2 → + ∃∃K1,U0. ⦃G1, L1, T⦄ ⊐*[b] ⦃G2, K1, U0⦄ & U0 ≛[h, o] U & K1 ≛[h, o, U] K2. #h #o #b #G1 #G2 #L2 #K2 #T #U #H #L1 #HL12 elim(fqus_inv_fqup … H) -H [ #H elim (lfdeq_fqup_trans … H … HL12) -L2 /3 width=5 by fqup_fqus, ex3_2_intro/ | * #HG #HL #HT destruct /2 width=5 by ex3_2_intro/ diff --git a/matita/matita/contribs/lambdadelta/basic_2/static/lfdeq_length.ma b/matita/matita/contribs/lambdadelta/basic_2/static/lfdeq_length.ma index 8221e2ed8..37a33504f 100644 --- a/matita/matita/contribs/lambdadelta/basic_2/static/lfdeq_length.ma +++ b/matita/matita/contribs/lambdadelta/basic_2/static/lfdeq_length.ma @@ -21,13 +21,13 @@ include "basic_2/static/lfdeq.ma". (* Forward lemmas with length for local environments ************************) (* Basic_2A1: lleq_fwd_length *) -lemma lfdeq_fwd_length: ∀h,o,L1,L2. ∀T:term. L1 ≡[h, o, T] L2 → |L1| = |L2|. +lemma lfdeq_fwd_length: ∀h,o,L1,L2. ∀T:term. L1 ≛[h, o, T] L2 → |L1| = |L2|. /2 width=3 by lfxs_fwd_length/ qed-. (* Properties with length for local environments ****************************) (* Basic_2A1: uses: lleq_lift_le lleq_lift_ge *) -lemma lfdeq_lifts_bi: ∀L1,L2. |L1| = |L2| → ∀h,o,K1,K2,T. K1 ≡[h, o, T] K2 → +lemma lfdeq_lifts_bi: ∀L1,L2. |L1| = |L2| → ∀h,o,K1,K2,T. K1 ≛[h, o, T] K2 → ∀b,f. ⬇*[b, f] L1 ≡ K1 → ⬇*[b, f] L2 ≡ K2 → - ∀U. ⬆*[f] T ≡ U → L1 ≡[h, o, U] L2. + ∀U. ⬆*[f] T ≡ U → L1 ≛[h, o, U] L2. /3 width=9 by lfxs_lifts_bi, tdeq_lifts_sn/ qed-. diff --git a/matita/matita/contribs/lambdadelta/basic_2/static/lfdeq_lfdeq.ma b/matita/matita/contribs/lambdadelta/basic_2/static/lfdeq_lfdeq.ma index 92f66ba61..2edd66b91 100644 --- a/matita/matita/contribs/lambdadelta/basic_2/static/lfdeq_lfdeq.ma +++ b/matita/matita/contribs/lambdadelta/basic_2/static/lfdeq_lfdeq.ma @@ -22,25 +22,25 @@ include "basic_2/static/lfdeq.ma". (* Advanced properties ******************************************************) (* Basic_2A1: uses: lleq_dec *) -lemma lfdeq_dec: ∀h,o,L1,L2. ∀T:term. Decidable (L1 ≡[h, o, T] L2). +lemma lfdeq_dec: ∀h,o,L1,L2. ∀T:term. Decidable (L1 ≛[h, o, T] L2). /3 width=1 by lfxs_dec, tdeq_dec/ qed-. (* Main properties **********************************************************) (* Basic_2A1: uses: lleq_bind lleq_bind_O *) theorem lfdeq_bind: ∀h,o,p,I,L1,L2,V1,V2,T. - L1 ≡[h, o, V1] L2 → L1.ⓑ{I}V1 ≡[h, o, T] L2.ⓑ{I}V2 → - L1 ≡[h, o, ⓑ{p,I}V1.T] L2. + L1 ≛[h, o, V1] L2 → L1.ⓑ{I}V1 ≛[h, o, T] L2.ⓑ{I}V2 → + L1 ≛[h, o, ⓑ{p,I}V1.T] L2. /2 width=2 by lfxs_bind/ qed. (* Basic_2A1: uses: lleq_flat *) -theorem lfdeq_flat: ∀h,o,I,L1,L2,V,T. L1 ≡[h, o, V] L2 → L1 ≡[h, o, T] L2 → - L1 ≡[h, o, ⓕ{I}V.T] L2. +theorem lfdeq_flat: ∀h,o,I,L1,L2,V,T. L1 ≛[h, o, V] L2 → L1 ≛[h, o, T] L2 → + L1 ≛[h, o, ⓕ{I}V.T] L2. /2 width=1 by lfxs_flat/ qed. theorem lfdeq_bind_void: ∀h,o,p,I,L1,L2,V,T. - L1 ≡[h, o, V] L2 → L1.ⓧ ≡[h, o, T] L2.ⓧ → - L1 ≡[h, o, ⓑ{p,I}V.T] L2. + L1 ≛[h, o, V] L2 → L1.ⓧ ≛[h, o, T] L2.ⓧ → + L1 ≛[h, o, ⓑ{p,I}V.T] L2. /2 width=1 by lfxs_bind_void/ qed. (* Basic_2A1: uses: lleq_trans *) @@ -59,39 +59,39 @@ theorem lfdeq_canc_sn: ∀h,o,T. left_cancellable … (lfdeq h o T). theorem lfdeq_canc_dx: ∀h,o,T. right_cancellable … (lfdeq h o T). /3 width=3 by lfdeq_trans, lfdeq_sym/ qed-. -theorem lfdeq_repl: ∀h,o,L1,L2. ∀T:term. L1 ≡[h, o, T] L2 → - ∀K1. L1 ≡[h, o, T] K1 → ∀K2. L2 ≡[h, o, T] K2 → K1 ≡[h, o, T] K2. +theorem lfdeq_repl: ∀h,o,L1,L2. ∀T:term. L1 ≛[h, o, T] L2 → + ∀K1. L1 ≛[h, o, T] K1 → ∀K2. L2 ≛[h, o, T] K2 → K1 ≛[h, o, T] K2. /3 width=3 by lfdeq_canc_sn, lfdeq_trans/ qed-. (* Negated properties *******************************************************) (* Note: auto works with /4 width=8/ so lfdeq_canc_sn is preferred **********) (* Basic_2A1: uses: lleq_nlleq_trans *) -lemma lfdeq_lfdneq_trans: ∀h,o.∀T:term.∀L1,L. L1 ≡[h, o, T] L → - ∀L2. (L ≡[h, o, T] L2 → ⊥) → (L1 ≡[h, o, T] L2 → ⊥). +lemma lfdeq_lfdneq_trans: ∀h,o.∀T:term.∀L1,L. L1 ≛[h, o, T] L → + ∀L2. (L ≛[h, o, T] L2 → ⊥) → (L1 ≛[h, o, T] L2 → ⊥). /3 width=3 by lfdeq_canc_sn/ qed-. (* Basic_2A1: uses: nlleq_lleq_div *) -lemma lfdneq_lfdeq_div: ∀h,o.∀T:term.∀L2,L. L2 ≡[h, o, T] L → - ∀L1. (L1 ≡[h, o, T] L → ⊥) → (L1 ≡[h, o, T] L2 → ⊥). +lemma lfdneq_lfdeq_div: ∀h,o.∀T:term.∀L2,L. L2 ≛[h, o, T] L → + ∀L1. (L1 ≛[h, o, T] L → ⊥) → (L1 ≛[h, o, T] L2 → ⊥). /3 width=3 by lfdeq_trans/ qed-. -theorem lfdneq_lfdeq_canc_dx: ∀h,o,L1,L. ∀T:term. (L1 ≡[h, o, T] L → ⊥) → - ∀L2. L2 ≡[h, o, T] L → L1 ≡[h, o, T] L2 → ⊥. +theorem lfdneq_lfdeq_canc_dx: ∀h,o,L1,L. ∀T:term. (L1 ≛[h, o, T] L → ⊥) → + ∀L2. L2 ≛[h, o, T] L → L1 ≛[h, o, T] L2 → ⊥. /3 width=3 by lfdeq_trans/ qed-. (* Negated inversion lemmas *************************************************) (* Basic_2A1: uses: nlleq_inv_bind nlleq_inv_bind_O *) -lemma lfdneq_inv_bind: ∀h,o,p,I,L1,L2,V,T. (L1 ≡[h, o, ⓑ{p,I}V.T] L2 → ⊥) → - (L1 ≡[h, o, V] L2 → ⊥) ∨ (L1.ⓑ{I}V ≡[h, o, T] L2.ⓑ{I}V → ⊥). +lemma lfdneq_inv_bind: ∀h,o,p,I,L1,L2,V,T. (L1 ≛[h, o, ⓑ{p,I}V.T] L2 → ⊥) → + (L1 ≛[h, o, V] L2 → ⊥) ∨ (L1.ⓑ{I}V ≛[h, o, T] L2.ⓑ{I}V → ⊥). /3 width=2 by lfnxs_inv_bind, tdeq_dec/ qed-. (* Basic_2A1: uses: nlleq_inv_flat *) -lemma lfdneq_inv_flat: ∀h,o,I,L1,L2,V,T. (L1 ≡[h, o, ⓕ{I}V.T] L2 → ⊥) → - (L1 ≡[h, o, V] L2 → ⊥) ∨ (L1 ≡[h, o, T] L2 → ⊥). +lemma lfdneq_inv_flat: ∀h,o,I,L1,L2,V,T. (L1 ≛[h, o, ⓕ{I}V.T] L2 → ⊥) → + (L1 ≛[h, o, V] L2 → ⊥) ∨ (L1 ≛[h, o, T] L2 → ⊥). /3 width=2 by lfnxs_inv_flat, tdeq_dec/ qed-. -lemma lfdneq_inv_bind_void: ∀h,o,p,I,L1,L2,V,T. (L1 ≡[h, o, ⓑ{p,I}V.T] L2 → ⊥) → - (L1 ≡[h, o, V] L2 → ⊥) ∨ (L1.ⓧ ≡[h, o, T] L2.ⓧ → ⊥). +lemma lfdneq_inv_bind_void: ∀h,o,p,I,L1,L2,V,T. (L1 ≛[h, o, ⓑ{p,I}V.T] L2 → ⊥) → + (L1 ≛[h, o, V] L2 → ⊥) ∨ (L1.ⓧ ≛[h, o, T] L2.ⓧ → ⊥). /3 width=3 by lfnxs_inv_bind_void, tdeq_dec/ qed-. diff --git a/matita/matita/contribs/lambdadelta/basic_2/syntax/tdeq.ma b/matita/matita/contribs/lambdadelta/basic_2/syntax/tdeq.ma index 43f538794..516c42904 100644 --- a/matita/matita/contribs/lambdadelta/basic_2/syntax/tdeq.ma +++ b/matita/matita/contribs/lambdadelta/basic_2/syntax/tdeq.ma @@ -12,7 +12,7 @@ (* *) (**************************************************************************) -include "basic_2/notation/relations/lazyeq_4.ma". +include "basic_2/notation/relations/stareq_4.ma". include "basic_2/syntax/item_sd.ma". include "basic_2/syntax/term.ma". @@ -27,11 +27,11 @@ inductive tdeq (h) (o): relation term ≝ interpretation "context-free degree-based equivalence (term)" - 'LazyEq h o T1 T2 = (tdeq h o T1 T2). + 'StarEq h o T1 T2 = (tdeq h o T1 T2). (* Basic inversion lemmas ***************************************************) -fact tdeq_inv_sort1_aux: ∀h,o,X,Y. X ≡[h, o] Y → ∀s1. X = ⋆s1 → +fact tdeq_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,32 +41,32 @@ fact tdeq_inv_sort1_aux: ∀h,o,X,Y. X ≡[h, o] Y → ∀s1. X = ⋆s1 → ] qed-. -lemma tdeq_inv_sort1: ∀h,o,Y,s1. ⋆s1 ≡[h, o] Y → +lemma tdeq_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 tdeq_inv_sort1_aux/ qed-. -fact tdeq_inv_lref1_aux: ∀h,o,X,Y. X ≡[h, o] Y → ∀i. X = #i → Y = #i. +fact tdeq_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 ] qed-. -lemma tdeq_inv_lref1: ∀h,o,Y,i. #i ≡[h, o] Y → Y = #i. +lemma tdeq_inv_lref1: ∀h,o,Y,i. #i ≛[h, o] Y → Y = #i. /2 width=5 by tdeq_inv_lref1_aux/ qed-. -fact tdeq_inv_gref1_aux: ∀h,o,X,Y. X ≡[h, o] Y → ∀l. X = §l → Y = §l. +fact tdeq_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 tdeq_inv_gref1: ∀h,o,Y,l. §l ≡[h, o] Y → Y = §l. +lemma tdeq_inv_gref1: ∀h,o,Y,l. §l ≛[h, o] Y → Y = §l. /2 width=5 by tdeq_inv_gref1_aux/ qed-. -fact tdeq_inv_pair1_aux: ∀h,o,X,Y. X ≡[h, o] Y → ∀I,V1,T1. X = ②{I}V1.T1 → - ∃∃V2,T2. V1 ≡[h, o] V2 & T1 ≡[h, o] T2 & Y = ②{I}V2.T2. +fact tdeq_inv_pair1_aux: ∀h,o,X,Y. X ≛[h, o] Y → ∀I,V1,T1. X = ②{I}V1.T1 → + ∃∃V2,T2. V1 ≛[h, o] V2 & T1 ≛[h, o] T2 & Y = ②{I}V2.T2. #h #o #X #Y * -X -Y [ #s1 #s2 #d #_ #_ #J #W1 #U1 #H destruct | #i #J #W1 #U1 #H destruct @@ -75,19 +75,19 @@ fact tdeq_inv_pair1_aux: ∀h,o,X,Y. X ≡[h, o] Y → ∀I,V1,T1. X = ②{I}V1. ] qed-. -lemma tdeq_inv_pair1: ∀h,o,I,V1,T1,Y. ②{I}V1.T1 ≡[h, o] Y → - ∃∃V2,T2. V1 ≡[h, o] V2 & T1 ≡[h, o] T2 & Y = ②{I}V2.T2. +lemma tdeq_inv_pair1: ∀h,o,I,V1,T1,Y. ②{I}V1.T1 ≛[h, o] Y → + ∃∃V2,T2. V1 ≛[h, o] V2 & T1 ≛[h, o] T2 & Y = ②{I}V2.T2. /2 width=3 by tdeq_inv_pair1_aux/ qed-. (* Advanced inversion lemmas ************************************************) -lemma tdeq_inv_sort1_deg: ∀h,o,Y,s1. ⋆s1 ≡[h, o] Y → ∀d. deg h o s1 d → +lemma tdeq_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 (tdeq_inv_sort1 … H) -H #s2 #x #Hx <(deg_mono h o … Hx … Hs1) -s1 -d /2 width=3 by ex2_intro/ qed-. -lemma tdeq_inv_sort_deg: ∀h,o,s1,s2. ⋆s1 ≡[h, o] ⋆s2 → +lemma tdeq_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 @@ -95,13 +95,13 @@ elim (tdeq_inv_sort1_deg … H … Hs1) -s1 #s2 #Hs2 #H destruct <(deg_mono h o … Hy … Hs2) -s2 -d1 // qed-. -lemma tdeq_inv_pair: ∀h,o,I1,I2,V1,V2,T1,T2. ②{I1}V1.T1 ≡[h, o] ②{I2}V2.T2 → - ∧∧ I1 = I2 & V1 ≡[h, o] V2 & T1 ≡[h, o] T2. +lemma tdeq_inv_pair: ∀h,o,I1,I2,V1,V2,T1,T2. ②{I1}V1.T1 ≛[h, o] ②{I2}V2.T2 → + ∧∧ I1 = I2 & V1 ≛[h, o] V2 & T1 ≛[h, o] T2. #h #o #I1 #I2 #V1 #V2 #T1 #T2 #H elim (tdeq_inv_pair1 … H) -H #V0 #T0 #HV #HT #H destruct /2 width=1 by and3_intro/ qed-. -lemma tdeq_inv_pair_xy_y: ∀h,o,I,T,V. ②{I}V.T ≡[h, o] T → ⊥. +lemma tdeq_inv_pair_xy_y: ∀h,o,I,T,V. ②{I}V.T ≛[h, o] T → ⊥. #h #o #I #T elim T -T [ #J #V #H elim (tdeq_inv_pair1 … H) -H #X #Y #_ #_ #H destruct | #J #X #Y #_ #IHY #V #H elim (tdeq_inv_pair … H) -H #H #_ #HY destruct /2 width=2 by/ @@ -110,7 +110,7 @@ qed-. (* Basic forward lemmas *****************************************************) -lemma tdeq_fwd_atom1: ∀h,o,I,Y. ⓪{I} ≡[h, o] Y → ∃J. Y = ⓪{J}. +lemma tdeq_fwd_atom1: ∀h,o,I,Y. ⓪{I} ≛[h, o] Y → ∃J. Y = ⓪{J}. #h #o * #x #Y #H [ elim (tdeq_inv_sort1 … H) -H ] /3 width=4 by tdeq_inv_gref1, tdeq_inv_lref1, ex_intro/ qed-. @@ -128,7 +128,7 @@ lemma tdeq_sym: ∀h,o. symmetric … (tdeq h o). /2 width=3 by tdeq_sort, tdeq_lref, tdeq_gref, tdeq_pair/ qed-. -lemma tdeq_dec: ∀h,o,T1,T2. Decidable (T1 ≡[h, o] T2). +lemma tdeq_dec: ∀h,o,T1,T2. Decidable (T1 ≛[h, o] T2). #h #o #T1 elim T1 -T1 [ * #s1 | #I1 #V1 #T1 #IHV #IHT ] * [1,3,5,7: * #s2 |*: #I2 #V2 #T2 ] [ elim (deg_total h o s1) #d1 #H1 elim (deg_total h o s2) #d2 #H2 @@ -169,10 +169,10 @@ qed-. (* Negated inversion lemmas *************************************************) lemma tdneq_inv_pair: ∀h,o,I1,I2,V1,V2,T1,T2. - (②{I1}V1.T1 ≡[h, o] ②{I2}V2.T2 → ⊥) → + (②{I1}V1.T1 ≛[h, o] ②{I2}V2.T2 → ⊥) → ∨∨ I1 = I2 → ⊥ - | (V1 ≡[h, o] V2 → ⊥) - | (T1 ≡[h, o] T2 → ⊥). + | (V1 ≛[h, o] V2 → ⊥) + | (T1 ≛[h, o] T2 → ⊥). #h #o #I1 #I2 #V1 #V2 #T1 #T2 #H12 elim (eq_item2_dec I1 I2) /3 width=1 by or3_intro0/ #H destruct elim (tdeq_dec h o V1 V2) /3 width=1 by or3_intro1/ diff --git a/matita/matita/contribs/lambdadelta/basic_2/syntax/tdeq_ext.ma b/matita/matita/contribs/lambdadelta/basic_2/syntax/tdeq_ext.ma index 096f2420d..7cfeee246 100644 --- a/matita/matita/contribs/lambdadelta/basic_2/syntax/tdeq_ext.ma +++ b/matita/matita/contribs/lambdadelta/basic_2/syntax/tdeq_ext.ma @@ -12,7 +12,7 @@ (* *) (**************************************************************************) -include "basic_2/notation/relations/lazyeq_5.ma". +include "basic_2/notation/relations/stareq_5.ma". include "basic_2/syntax/tdeq.ma". include "basic_2/syntax/lenv_ext2.ma". @@ -29,12 +29,12 @@ definition cdeq_ext: ∀h. sd h → relation3 lenv bind bind ≝ interpretation "context-free degree-based equivalence (binder)" - 'LazyEq h o I1 I2 = (tdeq_ext h o I1 I2). + 'StarEq h o I1 I2 = (tdeq_ext h o I1 I2). interpretation "context-dependent degree-based equivalence (term)" - 'LazyEq h o L T1 T2 = (cdeq h o L T1 T2). + 'StarEq h o L T1 T2 = (cdeq h o L T1 T2). interpretation "context-dependent degree-based equivalence (binder)" - 'LazyEq h o L I1 I2 = (cdeq_ext h o L I1 I2). + 'StarEq h o L I1 I2 = (cdeq_ext h o L I1 I2). diff --git a/matita/matita/contribs/lambdadelta/basic_2/syntax/tdeq_tdeq.ma b/matita/matita/contribs/lambdadelta/basic_2/syntax/tdeq_tdeq.ma index 51d09c534..80d13f4e6 100644 --- a/matita/matita/contribs/lambdadelta/basic_2/syntax/tdeq_tdeq.ma +++ b/matita/matita/contribs/lambdadelta/basic_2/syntax/tdeq_tdeq.ma @@ -35,16 +35,16 @@ theorem tdeq_canc_sn: ∀h,o. left_cancellable … (tdeq h o). theorem tdeq_canc_dx: ∀h,o. right_cancellable … (tdeq h o). /3 width=3 by tdeq_trans, tdeq_sym/ qed-. -theorem tdeq_repl: ∀h,o,T1,T2. T1 ≡[h, o] T2 → - ∀U1. T1 ≡[h, o] U1 → ∀U2. T2 ≡[h, o] U2 → U1 ≡[h, o] U2. +theorem tdeq_repl: ∀h,o,T1,T2. T1 ≛[h, o] T2 → + ∀U1. T1 ≛[h, o] U1 → ∀U2. T2 ≛[h, o] U2 → U1 ≛[h, o] U2. /3 width=3 by tdeq_canc_sn, tdeq_trans/ qed-. (* Negated main properies ***************************************************) -theorem tdeq_tdneq_trans: ∀h,o,T1,T. T1 ≡[h, o] T → ∀T2. (T ≡[h, o] T2 → ⊥) → - T1 ≡[h, o] T2 → ⊥. +theorem tdeq_tdneq_trans: ∀h,o,T1,T. T1 ≛[h, o] T → ∀T2. (T ≛[h, o] T2 → ⊥) → + T1 ≛[h, o] T2 → ⊥. /3 width=3 by tdeq_canc_sn/ qed-. -theorem tdneq_tdeq_canc_dx: ∀h,o,T1,T. (T1 ≡[h, o] T → ⊥) → ∀T2. T2 ≡[h, o] T → - T1 ≡[h, o] T2 → ⊥. +theorem tdneq_tdeq_canc_dx: ∀h,o,T1,T. (T1 ≛[h, o] T → ⊥) → ∀T2. T2 ≛[h, o] T → + T1 ≛[h, o] T2 → ⊥. /3 width=3 by tdeq_trans/ qed-. diff --git a/matita/matita/contribs/lambdadelta/basic_2/syntax/theq_tdeq.ma b/matita/matita/contribs/lambdadelta/basic_2/syntax/theq_tdeq.ma index 2a111b40f..e151e40f0 100644 --- a/matita/matita/contribs/lambdadelta/basic_2/syntax/theq_tdeq.ma +++ b/matita/matita/contribs/lambdadelta/basic_2/syntax/theq_tdeq.ma @@ -19,6 +19,6 @@ include "basic_2/syntax/theq.ma". (* Properties with degree-based equivalence for terms ***********************) -lemma tdeq_theq: ∀h,o,T1,T2. T1 ≡[h, o] T2 → T1 ⩳[h, o] T2. +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/web/basic_2_src.tbl b/matita/matita/contribs/lambdadelta/basic_2/web/basic_2_src.tbl index 5719d23da..77fe48710 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 @@ -92,7 +92,7 @@ table { } ] [ { "parallel qrst-computation" * } { - [ "fpbg ( ⦃?,?,?⦄ >≡[?,?] ⦃?,?,?⦄ )" "fpbg_lift" + "fpbg_fleq" + "fpbg_fpbs" + "fpbg_fpbg" * ] + [ "fpbg ( ⦃?,?,?⦄ >≛[?,?] ⦃?,?,?⦄ )" "fpbg_lift" + "fpbg_fleq" + "fpbg_fpbs" + "fpbg_fpbg" * ] [ "fpbs ( ⦃?,?,?⦄ ≥[?,?] ⦃?,?,?⦄ )" "fpbs_alt ( ⦃?,?,?⦄ ≥≥[?,?] ⦃?,?,?⦄ )" "fpbs_lift" + "fpbs_aaa" + "fpbs_fpb" + "fpbs_fpbs" * ] } ] @@ -166,8 +166,8 @@ table { } ] [ { "degree-based equivalence on referred entries" * } { - [ "ffdeq ( ⦃?,?,?⦄ ≡[?,?] ⦃?,?,?⦄ )" "ffdeq_fqup" + "ffdeq_ffdeq" * ] - [ "lfdeq ( ? ≡[?,?,?] ? )" "lfdeq_length" + "lfdeq_drops" + "lfdeq_fqup" + "lfdeq_fqus" + "lfdeq_lfdeq" * ] + [ "ffdeq ( ⦃?,?,?⦄ ≛[?,?] ⦃?,?,?⦄ )" "ffdeq_fqup" + "ffdeq_ffdeq" * ] + [ "lfdeq ( ? ≛[?,?,?] ? )" "lfdeq_length" + "lfdeq_drops" + "lfdeq_fqup" + "lfdeq_fqus" + "lfdeq_lfdeq" * ] } ] [ { "generic extension on referred entries" * } { @@ -237,8 +237,8 @@ table { } ] [ { "degree-based equivalence" * } { - [ "tdeq_ext ( ? ≡[?,?] ? ) ( ? ⊢ ? ≡[?,?] ? )" * ] - [ "tdeq ( ? ≡[?,?] ? )" "tdeq_tdeq" * ] + [ "tdeq_ext ( ? ≛[?,?] ? ) ( ? ⊢ ? ≛[?,?] ? )" * ] + [ "tdeq ( ? ≛[?,?] ? )" "tdeq_tdeq" * ] } ] [ { "closures" * } { diff --git a/matita/matita/contribs/lambdadelta/replace.sh b/matita/matita/contribs/lambdadelta/replace.sh index 2f053dec9..a70adc669 100644 --- a/matita/matita/contribs/lambdadelta/replace.sh +++ b/matita/matita/contribs/lambdadelta/replace.sh @@ -1,10 +1,10 @@ #!/bin/sh -for MA in `find -name "*.ma"`; do +for MA in `find basic_2 -name "*.ma"`; do #for MA in `find -name "cpg*.ma" -or -name "cpx*.ma"`; do - echo ${MA}; sed "s!$1!$2!g" ${MA} > ${MA}.new - if diff ${MA} ${MA}.new > /dev/null; + sed "s!$1!$2!g" ${MA} > ${MA}.new + if [ ! -s ${MA}.new ] || diff ${MA} ${MA}.new > /dev/null; then rm -f ${MA}.new; - else mv -f ${MA} ${MA}.old; mv -f ${MA}.new ${MA}; + else echo ${MA}; mv -f ${MA} ${MA}.old; mv -f ${MA}.new ${MA}; fi done diff --git a/matita/matita/contribs/lambdadelta/restore.sh b/matita/matita/contribs/lambdadelta/restore.sh new file mode 100644 index 000000000..af7b5e096 --- /dev/null +++ b/matita/matita/contribs/lambdadelta/restore.sh @@ -0,0 +1,8 @@ +#!/bin/sh +for MA in `find -name "*.ma"`; do + if [ -s ${MA}.old ]; + then echo ${MA}; mv -f ${MA}.old ${MA}; + fi +done + +unset MA -- 2.39.2