From 2002da6bcdbf12203a87a7d9630d738f67ede68c Mon Sep 17 00:00:00 2001 From: Ferruccio Guidi Date: Thu, 16 Feb 2017 11:22:04 +0000 Subject: [PATCH] - cprs and cnx on the way - breaks repositioning in notation - corrections in NF and SN - refactoring --- .../lambdadelta/basic_2/etc/cnx/cnx.etc | 91 --------- .../lambdadelta/basic_2/etc/cpxs/cpxs.etc | 26 +++ .../etc/{cnx => notation}/prednormal_5.etc | 0 .../notation/relations/atomicarity_4.ma | 2 +- .../basic_2/notation/relations/btpred_8.ma | 2 +- .../basic_2/notation/relations/btpredalt_8.ma | 2 +- .../notation/relations/btpredproper_8.ma | 2 +- .../notation/relations/btpredstar_8.ma | 2 +- .../notation/relations/btpredstaralt_8.ma | 2 +- .../basic_2/notation/relations/btsn_5.ma | 2 +- .../basic_2/notation/relations/btsnalt_5.ma | 2 +- .../basic_2/notation/relations/cosn_5.ma | 2 +- .../notation/relations/dpconvstar_8.ma | 2 +- .../basic_2/notation/relations/dpredstar_7.ma | 2 +- .../basic_2/notation/relations/freestar_3.ma | 2 +- .../basic_2/notation/relations/ineint_5.ma | 2 +- .../relations/lazybtpredstarproper_8.ma | 2 +- .../basic_2/notation/relations/lazyeq_3.ma | 2 +- .../basic_2/notation/relations/lazyeq_4.ma | 2 +- .../basic_2/notation/relations/lazyeq_5.ma | 2 +- .../basic_2/notation/relations/lrsubeqc_4.ma | 2 +- .../basic_2/notation/relations/lrsubeqf_4.ma | 2 +- .../basic_2/notation/relations/lrsubeqv_5.ma | 2 +- .../notation/relations/nativevalid_5.ma | 2 +- .../notation/relations/nativevalid_6.ma | 2 +- .../basic_2/notation/relations/pred_5.ma | 2 +- .../basic_2/notation/relations/pred_6.ma | 2 +- .../basic_2/notation/relations/predeval_4.ma | 2 +- .../basic_2/notation/relations/predeval_6.ma | 2 +- .../basic_2/notation/relations/predsn_5.ma | 2 +- .../notation/relations/predsnstar_5.ma | 2 +- .../basic_2/notation/relations/predstar_6.ma | 2 +- .../basic_2/notation/relations/predty_5.ma | 2 +- .../basic_2/notation/relations/predty_7.ma | 2 +- .../notation/relations/predtynormal_5.ma | 19 ++ .../basic_2/notation/relations/predtysn_5.ma | 2 +- .../notation/relations/predtystar_5.ma | 19 ++ .../notation/relations/relationstar_4.ma | 2 +- .../notation/relations/relationstar_5.ma | 2 +- .../basic_2/notation/relations/sn_5.ma | 2 +- .../basic_2/notation/relations/sn_6.ma | 2 +- .../basic_2/notation/relations/snalt_5.ma | 2 +- .../basic_2/notation/relations/snalt_6.ma | 2 +- .../basic_2/notation/relations/supterm_6.ma | 2 +- .../notation/relations/suptermopt_6.ma | 2 +- .../notation/relations/suptermplus_6.ma | 2 +- .../notation/relations/suptermstar_6.ma | 2 +- .../basic_2/rt_computation/cpxs.ma | 181 +++++++----------- .../basic_2/rt_computation/cpxs_tdeq.ma | 55 ++++++ .../basic_2/rt_computation/partial.txt | 1 + .../lambdadelta/basic_2/rt_transition/cnx.ma | 81 ++++++++ .../cnx_drops.ma} | 26 ++- .../basic_2/rt_transition/cnx_simple.ma | 47 +++++ .../basic_2/rt_transition/partial.txt | 1 + .../lambdadelta/basic_2/syntax/tdeq.ma | 17 +- .../lambdadelta/basic_2/web/basic_2_src.tbl | 39 ++-- .../contribs/lambdadelta/ground_2/lib/star.ma | 10 +- .../{basic_2/rt_transition => }/hls.ml | 0 58 files changed, 423 insertions(+), 274 deletions(-) create mode 100644 matita/matita/contribs/lambdadelta/basic_2/etc/cpxs/cpxs.etc rename matita/matita/contribs/lambdadelta/basic_2/etc/{cnx => notation}/prednormal_5.etc (100%) create mode 100644 matita/matita/contribs/lambdadelta/basic_2/notation/relations/predtynormal_5.ma create mode 100644 matita/matita/contribs/lambdadelta/basic_2/notation/relations/predtystar_5.ma create mode 100644 matita/matita/contribs/lambdadelta/basic_2/rt_computation/cpxs_tdeq.ma create mode 100644 matita/matita/contribs/lambdadelta/basic_2/rt_computation/partial.txt create mode 100644 matita/matita/contribs/lambdadelta/basic_2/rt_transition/cnx.ma rename matita/matita/contribs/lambdadelta/basic_2/{etc/cnx/cnx_lift.etc => rt_transition/cnx_drops.ma} (67%) create mode 100644 matita/matita/contribs/lambdadelta/basic_2/rt_transition/cnx_simple.ma rename matita/matita/contribs/lambdadelta/{basic_2/rt_transition => }/hls.ml (100%) diff --git a/matita/matita/contribs/lambdadelta/basic_2/etc/cnx/cnx.etc b/matita/matita/contribs/lambdadelta/basic_2/etc/cnx/cnx.etc index 0259a08aa..aaee69bfe 100644 --- a/matita/matita/contribs/lambdadelta/basic_2/etc/cnx/cnx.etc +++ b/matita/matita/contribs/lambdadelta/basic_2/etc/cnx/cnx.etc @@ -12,53 +12,10 @@ (* *) (**************************************************************************) -include "basic_2/notation/relations/prednormal_5.ma". include "basic_2/reduction/cnr.ma". -include "basic_2/reduction/cpx.ma". - -(* NORMAL TERMS FOR CONTEXT-SENSITIVE EXTENDED REDUCTION ********************) - -definition cnx: ∀h. sd h → relation3 genv lenv term ≝ - λh,o,G,L. NF … (cpx h o G L) (eq …). - -interpretation - "normality for context-sensitive extended reduction (term)" - 'PRedNormal h o L T = (cnx h o L T). (* Basic inversion lemmas ***************************************************) -lemma cnx_inv_sort: ∀h,o,G,L,s. ⦃G, L⦄ ⊢ ➡[h, o] 𝐍⦃⋆s⦄ → deg h o s 0. -#h #o #G #L #s #H elim (deg_total h o s) -#d @(nat_ind_plus … d) -d // #d #_ #Hkd -lapply (H (⋆(next h s)) ?) -H /2 width=2 by cpx_st/ -L -d #H -lapply (destruct_tatom_tatom_aux … H) -H #H (**) (* destruct lemma needed *) -lapply (destruct_sort_sort_aux … H) -H #H (**) (* destruct lemma needed *) -lapply (next_lt h s) >H -H #H elim (lt_refl_false … H) -qed-. - -lemma cnx_inv_delta: ∀h,o,I,G,L,K,V,i. ⬇[i] L ≡ K.ⓑ{I}V → ⦃G, L⦄ ⊢ ➡[h, o] 𝐍⦃#i⦄ → ⊥. -#h #o #I #G #L #K #V #i #HLK #H -elim (lift_total V 0 (i+1)) #W #HVW -lapply (H W ?) -H [ /3 width=7 by cpx_delta/ ] -HLK #H destruct -elim (lift_inv_lref2_be … HVW) -HVW /2 width=1 by ylt_inj/ -qed-. - -lemma cnx_inv_abst: ∀h,o,a,G,L,V,T. ⦃G, L⦄ ⊢ ➡[h, o] 𝐍⦃ⓛ{a}V.T⦄ → - ⦃G, L⦄ ⊢ ➡[h, o] 𝐍⦃V⦄ ∧ ⦃G, L.ⓛV⦄ ⊢ ➡[h, o] 𝐍⦃T⦄. -#h #o #a #G #L #V1 #T1 #HVT1 @conj -[ #V2 #HV2 lapply (HVT1 (ⓛ{a}V2.T1) ?) -HVT1 /2 width=2 by cpx_pair_sn/ -HV2 #H destruct // -| #T2 #HT2 lapply (HVT1 (ⓛ{a}V1.T2) ?) -HVT1 /2 width=2 by cpx_bind/ -HT2 #H destruct // -] -qed-. - -lemma cnx_inv_abbr: ∀h,o,G,L,V,T. ⦃G, L⦄ ⊢ ➡[h, o] 𝐍⦃-ⓓV.T⦄ → - ⦃G, L⦄ ⊢ ➡[h, o] 𝐍⦃V⦄ ∧ ⦃G, L.ⓓV⦄ ⊢ ➡[h, o] 𝐍⦃T⦄. -#h #o #G #L #V1 #T1 #HVT1 @conj -[ #V2 #HV2 lapply (HVT1 (-ⓓV2.T1) ?) -HVT1 /2 width=2 by cpx_pair_sn/ -HV2 #H destruct // -| #T2 #HT2 lapply (HVT1 (-ⓓV1.T2) ?) -HVT1 /2 width=2 by cpx_bind/ -HT2 #H destruct // -] -qed-. - lemma cnx_inv_zeta: ∀h,o,G,L,V,T. ⦃G, L⦄ ⊢ ➡[h, o] 𝐍⦃+ⓓV.T⦄ → ⊥. #h #o #G #L #V #T #H elim (is_lift_dec T 0 1) [ * #U #HTU @@ -71,24 +28,6 @@ lemma cnx_inv_zeta: ∀h,o,G,L,V,T. ⦃G, L⦄ ⊢ ➡[h, o] 𝐍⦃+ⓓV.T⦄ ] qed-. -lemma cnx_inv_appl: ∀h,o,G,L,V,T. ⦃G, L⦄ ⊢ ➡[h, o] 𝐍⦃ⓐV.T⦄ → - ∧∧ ⦃G, L⦄ ⊢ ➡[h, o] 𝐍⦃V⦄ & ⦃G, L⦄ ⊢ ➡[h, o] 𝐍⦃T⦄ & 𝐒⦃T⦄. -#h #o #G #L #V1 #T1 #HVT1 @and3_intro -[ #V2 #HV2 lapply (HVT1 (ⓐV2.T1) ?) -HVT1 /2 width=1 by cpx_pair_sn/ -HV2 #H destruct // -| #T2 #HT2 lapply (HVT1 (ⓐV1.T2) ?) -HVT1 /2 width=1 by cpx_flat/ -HT2 #H destruct // -| generalize in match HVT1; -HVT1 elim T1 -T1 * // #a * #W1 #U1 #_ #_ #H - [ elim (lift_total V1 0 1) #V2 #HV12 - lapply (H (ⓓ{a}W1.ⓐV2.U1) ?) -H /3 width=3 by cpr_cpx, cpr_theta/ -HV12 #H destruct - | lapply (H (ⓓ{a}ⓝW1.V1.U1) ?) -H /3 width=1 by cpr_cpx, cpr_beta/ #H destruct - ] -] -qed-. - -lemma cnx_inv_eps: ∀h,o,G,L,V,T. ⦃G, L⦄ ⊢ ➡[h, o] 𝐍⦃ⓝV.T⦄ → ⊥. -#h #o #G #L #V #T #H lapply (H T ?) -H -/2 width=4 by cpx_eps, discr_tpair_xy_y/ -qed-. - (* Basic forward lemmas *****************************************************) lemma cnx_fwd_cnr: ∀h,o,G,L,T. ⦃G, L⦄ ⊢ ➡[h, o] 𝐍⦃T⦄ → ⦃G, L⦄ ⊢ ➡ 𝐍⦃T⦄. @@ -98,39 +37,9 @@ qed-. (* Basic properties *********************************************************) -lemma cnx_sort: ∀h,o,G,L,s. deg h o s 0 → ⦃G, L⦄ ⊢ ➡[h, o] 𝐍⦃⋆s⦄. -#h #o #G #L #s #Hk #X #H elim (cpx_inv_sort1 … H) -H // * #d #Hkd #_ -lapply (deg_mono … Hkd Hk) -h -L (drop_fwd_length … HL) -HL // qed. -lemma cnx_abst: ∀h,o,a,G,L,W,T. ⦃G, L⦄ ⊢ ➡[h, o] 𝐍⦃W⦄ → ⦃G, L.ⓛW⦄ ⊢ ➡[h, o] 𝐍⦃T⦄ → - ⦃G, L⦄ ⊢ ➡[h, o] 𝐍⦃ⓛ{a}W.T⦄. -#h #o #a #G #L #W #T #HW #HT #X #H -elim (cpx_inv_abst1 … H) -H #W0 #T0 #HW0 #HT0 #H destruct ->(HW … HW0) -W0 >(HT … HT0) -T0 // -qed. - -lemma cnx_appl_simple: ∀h,o,G,L,V,T. ⦃G, L⦄ ⊢ ➡[h, o] 𝐍⦃V⦄ → ⦃G, L⦄ ⊢ ➡[h, o] 𝐍⦃T⦄ → 𝐒⦃T⦄ → - ⦃G, L⦄ ⊢ ➡[h, o] 𝐍⦃ⓐV.T⦄. -#h #o #G #L #V #T #HV #HT #HS #X #H -elim (cpx_inv_appl1_simple … H) -H // #V0 #T0 #HV0 #HT0 #H destruct ->(HV … HV0) -V0 >(HT … HT0) -T0 // -qed. - axiom cnx_dec: ∀h,o,G,L,T1. ⦃G, L⦄ ⊢ ➡[h, o] 𝐍⦃T1⦄ ∨ ∃∃T2. ⦃G, L⦄ ⊢ T1 ➡[h, o] T2 & (T1 = T2 → ⊥). diff --git a/matita/matita/contribs/lambdadelta/basic_2/etc/cpxs/cpxs.etc b/matita/matita/contribs/lambdadelta/basic_2/etc/cpxs/cpxs.etc new file mode 100644 index 000000000..89e1466f7 --- /dev/null +++ b/matita/matita/contribs/lambdadelta/basic_2/etc/cpxs/cpxs.etc @@ -0,0 +1,26 @@ +lemma lsubr_cpxs_trans: ∀h,o,G. lsub_trans … (cpxs h o G) lsubr. +/3 width=5 by lsubr_cpx_trans, LTC_lsub_trans/ +qed-. + +lemma cprs_cpxs: ∀h,o,G,L,T1,T2. ⦃G, L⦄ ⊢ T1 ⬈* T2 → ⦃G, L⦄ ⊢ T1 ⬈*[h] T2. +#h #o #G #L #T1 #T2 #H @(cprs_ind … H) -T2 /3 width=3 by cpxs_strap1, +cpr_cpx/ +qed. + +lemma cpxs_inv_cnx1: ∀h,o,G,L,T,U. ⦃G, L⦄ ⊢ T ⬈*[h] U → ⦃G, L⦄ ⊢ ⬈[h] +𝐍⦃T⦄ → T = U. +#h #o #G #L #T #U #H @(cpxs_ind_dx … H) -T // +#T0 #T #H1T0 #_ #IHT #H2T0 +lapply (H2T0 … H1T0) -H1T0 #H destruct /2 width=1 by/ +qed-. + +lemma cpxs_neq_inv_step_sn: ∀h,o,G,L,T1,T2. ⦃G, L⦄ ⊢ T1 ⬈*[h] T2 → (T1 = T2 → ⊥) → + ∃∃T. ⦃G, L⦄ ⊢ T1 ⬈[h] T & T1 = T → ⊥ & ⦃G, L⦄ ⊢ T ⬈*[h] T2. +#h #o #G #L #T1 #T2 #H @(cpxs_ind_dx … H) -T1 +[ #H elim H -H // +| #T1 #T #H1 #H2 #IH2 #H12 elim (eq_term_dec T1 T) #H destruct + [ -H1 -H2 /3 width=1 by/ + | -IH2 /3 width=4 by ex3_intro/ (**) (* auto fails without clear *) + ] +] +qed-. diff --git a/matita/matita/contribs/lambdadelta/basic_2/etc/cnx/prednormal_5.etc b/matita/matita/contribs/lambdadelta/basic_2/etc/notation/prednormal_5.etc similarity index 100% rename from matita/matita/contribs/lambdadelta/basic_2/etc/cnx/prednormal_5.etc rename to matita/matita/contribs/lambdadelta/basic_2/etc/notation/prednormal_5.etc diff --git a/matita/matita/contribs/lambdadelta/basic_2/notation/relations/atomicarity_4.ma b/matita/matita/contribs/lambdadelta/basic_2/notation/relations/atomicarity_4.ma index e6a1b0924..9659409b9 100644 --- a/matita/matita/contribs/lambdadelta/basic_2/notation/relations/atomicarity_4.ma +++ b/matita/matita/contribs/lambdadelta/basic_2/notation/relations/atomicarity_4.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 A )" +notation "hvbox( ⦃ term 46 G, break term 46 L⦄ ⊢ break term 46 T ⁝ break term 46 A )" non associative with precedence 45 for @{ 'AtomicArity $G $L $T $A }. diff --git a/matita/matita/contribs/lambdadelta/basic_2/notation/relations/btpred_8.ma b/matita/matita/contribs/lambdadelta/basic_2/notation/relations/btpred_8.ma index 7e58d203e..63d6a704b 100644 --- a/matita/matita/contribs/lambdadelta/basic_2/notation/relations/btpred_8.ma +++ b/matita/matita/contribs/lambdadelta/basic_2/notation/relations/btpred_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 @{ 'BTPRed $h $o $G1 $L1 $T1 $G2 $L2 $T2 }. diff --git a/matita/matita/contribs/lambdadelta/basic_2/notation/relations/btpredalt_8.ma b/matita/matita/contribs/lambdadelta/basic_2/notation/relations/btpredalt_8.ma index 2e0ebf5a0..8418bda60 100644 --- a/matita/matita/contribs/lambdadelta/basic_2/notation/relations/btpredalt_8.ma +++ b/matita/matita/contribs/lambdadelta/basic_2/notation/relations/btpredalt_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 @{ 'BTPRedAlt $h $o $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 e036aa7d5..45c244ce4 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 6d216e2fa..22478c48b 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 3b2cd2bfe..8aec3b1df 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/btsn_5.ma b/matita/matita/contribs/lambdadelta/basic_2/notation/relations/btsn_5.ma index 7abf15de8..fa72d2355 100644 --- a/matita/matita/contribs/lambdadelta/basic_2/notation/relations/btsn_5.ma +++ b/matita/matita/contribs/lambdadelta/basic_2/notation/relations/btsn_5.ma @@ -14,6 +14,6 @@ (* NOTATION FOR THE FORMAL SYSTEM λδ ****************************************) -notation "hvbox( ⦥ [ term 46 h, break term 46 o ] break ⦃ term 46 G, break term 46 L, break term 46 T ⦄ )" +notation "hvbox( ⦥ [ term 46 h, break term 46 o ] ⦃ break term 46 G, break term 46 L, break term 46 T ⦄ )" non associative with precedence 45 for @{ 'BTSN $h $o $G $L $T }. diff --git a/matita/matita/contribs/lambdadelta/basic_2/notation/relations/btsnalt_5.ma b/matita/matita/contribs/lambdadelta/basic_2/notation/relations/btsnalt_5.ma index 5e9d1ec67..e9984754d 100644 --- a/matita/matita/contribs/lambdadelta/basic_2/notation/relations/btsnalt_5.ma +++ b/matita/matita/contribs/lambdadelta/basic_2/notation/relations/btsnalt_5.ma @@ -14,6 +14,6 @@ (* NOTATION FOR THE FORMAL SYSTEM λδ ****************************************) -notation "hvbox( ⦥ ⦥ [ term 46 h, break term 46 o ] break ⦃ term 46 G, break term 46 L, break term 46 T ⦄ )" +notation "hvbox( ⦥ ⦥ [ term 46 h, break term 46 o ] ⦃ break term 46 G, break term 46 L, break term 46 T ⦄ )" non associative with precedence 45 for @{ 'BTSNAlt $h $o $G $L $T }. diff --git a/matita/matita/contribs/lambdadelta/basic_2/notation/relations/cosn_5.ma b/matita/matita/contribs/lambdadelta/basic_2/notation/relations/cosn_5.ma index ef632cba9..e69a4ac02 100644 --- a/matita/matita/contribs/lambdadelta/basic_2/notation/relations/cosn_5.ma +++ b/matita/matita/contribs/lambdadelta/basic_2/notation/relations/cosn_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 f ] break term 46 L )" +notation "hvbox( G ⊢ ~ ⬊ * [ break term 46 h , break term 46 o , break term 46 f ] break term 46 L )" non associative with precedence 45 for @{ 'CoSN $h $o $f $G $L }. 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 8d37f5217..5632e2996 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 d9ab259ab..21e256dbb 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/freestar_3.ma b/matita/matita/contribs/lambdadelta/basic_2/notation/relations/freestar_3.ma index d9cfb81bd..fe106086e 100644 --- a/matita/matita/contribs/lambdadelta/basic_2/notation/relations/freestar_3.ma +++ b/matita/matita/contribs/lambdadelta/basic_2/notation/relations/freestar_3.ma @@ -14,6 +14,6 @@ (* NOTATION FOR THE FORMAL SYSTEM λδ ****************************************) -notation "hvbox( L ⊢ break 𝐅 * ⦃ term 46 T ⦄ ≡ break term 46 f )" +notation "hvbox( L ⊢ 𝐅 * ⦃ break term 46 T ⦄ ≡ break term 46 f )" non associative with precedence 45 for @{ 'FreeStar $L $T $f }. diff --git a/matita/matita/contribs/lambdadelta/basic_2/notation/relations/ineint_5.ma b/matita/matita/contribs/lambdadelta/basic_2/notation/relations/ineint_5.ma index 83f23ef23..1705b31be 100644 --- a/matita/matita/contribs/lambdadelta/basic_2/notation/relations/ineint_5.ma +++ b/matita/matita/contribs/lambdadelta/basic_2/notation/relations/ineint_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 R ] break 〚term 46 A 〛 )" +notation "hvbox( ⦃ term 46 G, break term 46 L, break term 46 T ⦄ ϵ [ break term 46 R ] 〚 break term 46 A 〛 )" non associative with precedence 45 for @{ 'InEInt $R $G $L $T $A }. 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 9c1252ac7..94236004b 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/lazyeq_3.ma b/matita/matita/contribs/lambdadelta/basic_2/notation/relations/lazyeq_3.ma index e2c7c0aff..1ffdc2b10 100644 --- a/matita/matita/contribs/lambdadelta/basic_2/notation/relations/lazyeq_3.ma +++ b/matita/matita/contribs/lambdadelta/basic_2/notation/relations/lazyeq_3.ma @@ -14,6 +14,6 @@ (* NOTATION FOR THE FORMAL SYSTEM λδ ****************************************) -notation "hvbox( L1 ≡ break [ term 46 f ] break term 46 L2 )" +notation "hvbox( L1 ≡ [ break term 46 f ] break term 46 L2 )" non associative with precedence 45 for @{ 'LazyEq $f $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/lazyeq_4.ma index aec1914f1..9e302cf79 100644 --- a/matita/matita/contribs/lambdadelta/basic_2/notation/relations/lazyeq_4.ma +++ b/matita/matita/contribs/lambdadelta/basic_2/notation/relations/lazyeq_4.ma @@ -14,6 +14,6 @@ (* NOTATION FOR THE FORMAL SYSTEM λδ ****************************************) -notation "hvbox( T1 ≡ break [ term 46 h , term 46 o ] break term 46 T2 )" +notation "hvbox( T1 ≡ [ break term 46 h , term 46 o ] break term 46 T2 )" non associative with precedence 45 for @{ 'LazyEq $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/lazyeq_5.ma index dd6a6046a..c0b3b0bce 100644 --- a/matita/matita/contribs/lambdadelta/basic_2/notation/relations/lazyeq_5.ma +++ b/matita/matita/contribs/lambdadelta/basic_2/notation/relations/lazyeq_5.ma @@ -14,6 +14,6 @@ (* NOTATION FOR THE FORMAL SYSTEM λδ ****************************************) -notation "hvbox( L1 ≡ break [ term 46 h , term 46 o , 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 @{ 'LazyEq $h $o $T $L1 $L2 }. diff --git a/matita/matita/contribs/lambdadelta/basic_2/notation/relations/lrsubeqc_4.ma b/matita/matita/contribs/lambdadelta/basic_2/notation/relations/lrsubeqc_4.ma index 823d6bebf..6b9fa4dfd 100644 --- a/matita/matita/contribs/lambdadelta/basic_2/notation/relations/lrsubeqc_4.ma +++ b/matita/matita/contribs/lambdadelta/basic_2/notation/relations/lrsubeqc_4.ma @@ -14,6 +14,6 @@ (* NOTATION FOR THE FORMAL SYSTEM λδ ****************************************) -notation "hvbox( G ⊢ break term 46 L1 ⫃ break [ term 46 R ] break term 46 L2 )" +notation "hvbox( G ⊢ break term 46 L1 ⫃ [ break term 46 R ] break term 46 L2 )" non associative with precedence 45 for @{ 'LRSubEqC $R $G $L1 $L2 }. diff --git a/matita/matita/contribs/lambdadelta/basic_2/notation/relations/lrsubeqf_4.ma b/matita/matita/contribs/lambdadelta/basic_2/notation/relations/lrsubeqf_4.ma index 76865bf55..413553ccd 100644 --- a/matita/matita/contribs/lambdadelta/basic_2/notation/relations/lrsubeqf_4.ma +++ b/matita/matita/contribs/lambdadelta/basic_2/notation/relations/lrsubeqf_4.ma @@ -14,6 +14,6 @@ (* NOTATION FOR THE FORMAL SYSTEM λδ ****************************************) -notation "hvbox( ⦃ term 46 L1, break term 46 f1 ⦄ ⫃ 𝐅* break ⦃ term 46 L2, break term 46 f2 ⦄ )" +notation "hvbox( ⦃ term 46 L1, break term 46 f1 ⦄ ⫃ 𝐅* ⦃ break term 46 L2, break term 46 f2 ⦄ )" non associative with precedence 45 for @{ 'LRSubEqF $L1 $f1 $L2 $f2 }. diff --git a/matita/matita/contribs/lambdadelta/basic_2/notation/relations/lrsubeqv_5.ma b/matita/matita/contribs/lambdadelta/basic_2/notation/relations/lrsubeqv_5.ma index d404926bf..78eeb36a2 100644 --- a/matita/matita/contribs/lambdadelta/basic_2/notation/relations/lrsubeqv_5.ma +++ b/matita/matita/contribs/lambdadelta/basic_2/notation/relations/lrsubeqv_5.ma @@ -14,6 +14,6 @@ (* NOTATION FOR THE FORMAL SYSTEM λδ ****************************************) -notation "hvbox( G ⊢ break term 46 L1 ⫃ ¡ break [ term 46 h, break term 46 o ] break term 46 L2 )" +notation "hvbox( G ⊢ break term 46 L1 ⫃ ¡ [ break term 46 h, break term 46 o ] break term 46 L2 )" non associative with precedence 45 for @{ 'LRSubEqV $h $o $G $L1 $L2 }. 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 4efadabad..4bf3b4763 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 d387e60be..237b7e74e 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/pred_5.ma b/matita/matita/contribs/lambdadelta/basic_2/notation/relations/pred_5.ma index d2fe2d9f6..37faf805a 100644 --- a/matita/matita/contribs/lambdadelta/basic_2/notation/relations/pred_5.ma +++ b/matita/matita/contribs/lambdadelta/basic_2/notation/relations/pred_5.ma @@ -14,6 +14,6 @@ (* NOTATION FOR THE FORMAL SYSTEM λδ ****************************************) -notation "hvbox( ⦃ term 46 G, break term 46 L ⦄ ⊢ break term 46 T1 ➡ break [ term 46 h ] break term 46 T2 )" +notation "hvbox( ⦃ term 46 G, break term 46 L ⦄ ⊢ break term 46 T1 ➡ [ break term 46 h ] break term 46 T2 )" non associative with precedence 45 for @{ 'PRed $h $G $L $T1 $T2 }. diff --git a/matita/matita/contribs/lambdadelta/basic_2/notation/relations/pred_6.ma b/matita/matita/contribs/lambdadelta/basic_2/notation/relations/pred_6.ma index 3bc75f682..4d7807e0f 100644 --- a/matita/matita/contribs/lambdadelta/basic_2/notation/relations/pred_6.ma +++ b/matita/matita/contribs/lambdadelta/basic_2/notation/relations/pred_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 n, break term 46 h ] break term 46 T2 )" +notation "hvbox( ⦃ term 46 G, break term 46 L ⦄ ⊢ break term 46 T1 ➡ [ break term 46 n, break term 46 h ] break term 46 T2 )" non associative with precedence 45 for @{ 'PRed $n $h $G $L $T1 $T2 }. diff --git a/matita/matita/contribs/lambdadelta/basic_2/notation/relations/predeval_4.ma b/matita/matita/contribs/lambdadelta/basic_2/notation/relations/predeval_4.ma index e26cfe6d3..abf7b6558 100644 --- a/matita/matita/contribs/lambdadelta/basic_2/notation/relations/predeval_4.ma +++ b/matita/matita/contribs/lambdadelta/basic_2/notation/relations/predeval_4.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 T2 ⦄ )" +notation "hvbox( ⦃ term 46 G, break term 46 L ⦄ ⊢ break term 46 T1 ➡ * 𝐍 ⦃ break term 46 T2 ⦄ )" non associative with precedence 45 for @{ 'PRedEval $G $L $T1 $T2 }. diff --git a/matita/matita/contribs/lambdadelta/basic_2/notation/relations/predeval_6.ma b/matita/matita/contribs/lambdadelta/basic_2/notation/relations/predeval_6.ma index 391f21f3c..ab5882337 100644 --- a/matita/matita/contribs/lambdadelta/basic_2/notation/relations/predeval_6.ma +++ b/matita/matita/contribs/lambdadelta/basic_2/notation/relations/predeval_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 @{ 'PRedEval $h $o $G $L $T1 $T2 }. 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 e1f79764c..759a18874 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_5.ma b/matita/matita/contribs/lambdadelta/basic_2/notation/relations/predsnstar_5.ma index bb2d10464..5debc4550 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_6.ma b/matita/matita/contribs/lambdadelta/basic_2/notation/relations/predstar_6.ma index 265244809..0d349e77c 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_5.ma b/matita/matita/contribs/lambdadelta/basic_2/notation/relations/predty_5.ma index 8ffd00516..8ec99d4db 100644 --- a/matita/matita/contribs/lambdadelta/basic_2/notation/relations/predty_5.ma +++ b/matita/matita/contribs/lambdadelta/basic_2/notation/relations/predty_5.ma @@ -14,6 +14,6 @@ (* NOTATION FOR THE FORMAL SYSTEM λδ ****************************************) -notation "hvbox( ⦃ term 46 G, break term 46 L ⦄ ⊢ break term 46 T1 ⬈ break [ term 46 h ] break term 46 T2 )" +notation "hvbox( ⦃ term 46 G, break term 46 L ⦄ ⊢ break term 46 T1 ⬈ [ break term 46 h ] break term 46 T2 )" non associative with precedence 45 for @{ 'PRedTy $h $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 291bf9075..aadb001f9 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 new file mode 100644 index 000000000..fabfe36de --- /dev/null +++ b/matita/matita/contribs/lambdadelta/basic_2/notation/relations/predtynormal_5.ma @@ -0,0 +1,19 @@ +(**************************************************************************) +(* ___ *) +(* ||M|| *) +(* ||A|| A project by Andrea Asperti *) +(* ||T|| *) +(* ||I|| Developers: *) +(* ||T|| The HELM team. *) +(* ||A|| http://helm.cs.unibo.it *) +(* \ / *) +(* \ / This file is distributed under the terms of the *) +(* v GNU General Public License Version 2 *) +(* *) +(**************************************************************************) + +(* NOTATION FOR THE FORMAL SYSTEM λδ ****************************************) + +notation "hvbox( ⦃ term 46 G, break term 46 L ⦄ ⊢ ⬈ [ break term 46 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 8f82a99b2..ac96ccb5b 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/predtystar_5.ma b/matita/matita/contribs/lambdadelta/basic_2/notation/relations/predtystar_5.ma new file mode 100644 index 000000000..347c93284 --- /dev/null +++ b/matita/matita/contribs/lambdadelta/basic_2/notation/relations/predtystar_5.ma @@ -0,0 +1,19 @@ +(**************************************************************************) +(* ___ *) +(* ||M|| *) +(* ||A|| A project by Andrea Asperti *) +(* ||T|| *) +(* ||I|| Developers: *) +(* ||T|| The HELM team. *) +(* ||A|| http://helm.cs.unibo.it *) +(* \ / *) +(* \ / This file is distributed under the terms of the *) +(* v GNU General Public License Version 2 *) +(* *) +(**************************************************************************) + +(* NOTATION FOR THE FORMAL SYSTEM λδ ****************************************) + +notation "hvbox( ⦃ term 46 G, break term 46 L ⦄ ⊢ break term 46 T1 ⬈ * [ break term 46 h ] break term 46 T2 )" + non associative with precedence 45 + for @{ 'PRedTyStar $h $G $L $T1 $T2 }. 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 a306fa3d9..9e3581baa 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 698b130c3..f6df0bec5 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/sn_5.ma b/matita/matita/contribs/lambdadelta/basic_2/notation/relations/sn_5.ma index 4ac3bc7aa..b7ce19c7a 100644 --- a/matita/matita/contribs/lambdadelta/basic_2/notation/relations/sn_5.ma +++ b/matita/matita/contribs/lambdadelta/basic_2/notation/relations/sn_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 @{ 'SN $h $o $G $L $T }. diff --git a/matita/matita/contribs/lambdadelta/basic_2/notation/relations/sn_6.ma b/matita/matita/contribs/lambdadelta/basic_2/notation/relations/sn_6.ma index 268bd0b61..14f27aab0 100644 --- a/matita/matita/contribs/lambdadelta/basic_2/notation/relations/sn_6.ma +++ b/matita/matita/contribs/lambdadelta/basic_2/notation/relations/sn_6.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 f ] break term 46 L )" +notation "hvbox( G ⊢ ⬊ * [ break term 46 h , break term 46 o , break term 46 T , break term 46 f ] break term 46 L )" non associative with precedence 45 for @{ 'SN $h $o $T $f $G $L }. diff --git a/matita/matita/contribs/lambdadelta/basic_2/notation/relations/snalt_5.ma b/matita/matita/contribs/lambdadelta/basic_2/notation/relations/snalt_5.ma index 59196e5b1..207c25ded 100644 --- a/matita/matita/contribs/lambdadelta/basic_2/notation/relations/snalt_5.ma +++ b/matita/matita/contribs/lambdadelta/basic_2/notation/relations/snalt_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 @{ 'SNAlt $h $o $G $L $T }. diff --git a/matita/matita/contribs/lambdadelta/basic_2/notation/relations/snalt_6.ma b/matita/matita/contribs/lambdadelta/basic_2/notation/relations/snalt_6.ma index 8f59a5f1c..ce52c4ca3 100644 --- a/matita/matita/contribs/lambdadelta/basic_2/notation/relations/snalt_6.ma +++ b/matita/matita/contribs/lambdadelta/basic_2/notation/relations/snalt_6.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 f ] break term 46 L )" +notation "hvbox( G ⊢ ⬊ ⬊ * [ break term 46 h , break term 46 o , break term 46 T , break term 46 f ] break term 46 L )" non associative with precedence 45 for @{ 'SNAlt $h $o $T $f $G $L }. 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 1300f0fa5..9737e1aa3 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/suptermopt_6.ma b/matita/matita/contribs/lambdadelta/basic_2/notation/relations/suptermopt_6.ma index 8ed1123b4..cca092323 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/suptermplus_6.ma b/matita/matita/contribs/lambdadelta/basic_2/notation/relations/suptermplus_6.ma index 533b88cdf..ae285d31e 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/suptermstar_6.ma b/matita/matita/contribs/lambdadelta/basic_2/notation/relations/suptermstar_6.ma index f2abfc20f..10af7fbd1 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, 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/rt_computation/cpxs.ma b/matita/matita/contribs/lambdadelta/basic_2/rt_computation/cpxs.ma index d21a90427..f09fab54c 100644 --- a/matita/matita/contribs/lambdadelta/basic_2/rt_computation/cpxs.ma +++ b/matita/matita/contribs/lambdadelta/basic_2/rt_computation/cpxs.ma @@ -12,149 +12,131 @@ (* *) (**************************************************************************) -include "basic_2/notation/relations/predstar_6.ma". -include "basic_2/reduction/cnx.ma". -include "basic_2/computation/cprs.ma". +include "basic_2/notation/relations/predtystar_5.ma". +include "basic_2/rt_transition/cpx.ma". -(* CONTEXT-SENSITIVE EXTENDED PARALLEL COMPUTATION ON TERMS *****************) +(* UNCOUNTED CONTEXT-SENSITIVE PARALLEL RT-COMPUTATION FOR TERMS ************) -definition cpxs: ∀h. sd h → relation4 genv lenv term term ≝ - λh,o,G. LTC … (cpx h o G). +definition cpxs: sh → relation4 genv lenv term term ≝ + λh,G. LTC … (cpx h G). -interpretation "extended context-sensitive parallel computation (term)" - 'PRedStar h o G L T1 T2 = (cpxs h o G L T1 T2). +interpretation "uncounted context-sensitive parallel rt-computation (term)" + 'PRedTyStar h G L T1 T2 = (cpxs h G L T1 T2). (* Basic eliminators ********************************************************) -lemma cpxs_ind: ∀h,o,G,L,T1. ∀R:predicate term. R T1 → - (∀T,T2. ⦃G, L⦄ ⊢ T1 ⬈*[h, o] T → ⦃G, L⦄ ⊢ T ⬈[h, o] T2 → R T → R T2) → - ∀T2. ⦃G, L⦄ ⊢ T1 ⬈*[h, o] T2 → R T2. -#h #o #L #G #T1 #R #HT1 #IHT1 #T2 #HT12 +lemma cpxs_ind: ∀h,G,L,T1. ∀R:predicate term. R T1 → + (∀T,T2. ⦃G, L⦄ ⊢ T1 ⬈*[h] T → ⦃G, L⦄ ⊢ T ⬈[h] T2 → R T → R T2) → + ∀T2. ⦃G, L⦄ ⊢ T1 ⬈*[h] T2 → R T2. +#h #L #G #T1 #R #HT1 #IHT1 #T2 #HT12 @(TC_star_ind … HT1 IHT1 … HT12) // qed-. -lemma cpxs_ind_dx: ∀h,o,G,L,T2. ∀R:predicate term. R T2 → - (∀T1,T. ⦃G, L⦄ ⊢ T1 ⬈[h, o] T → ⦃G, L⦄ ⊢ T ⬈*[h, o] T2 → R T → R T1) → - ∀T1. ⦃G, L⦄ ⊢ T1 ⬈*[h, o] T2 → R T1. -#h #o #G #L #T2 #R #HT2 #IHT2 #T1 #HT12 +lemma cpxs_ind_dx: ∀h,G,L,T2. ∀R:predicate term. R T2 → + (∀T1,T. ⦃G, L⦄ ⊢ T1 ⬈[h] T → ⦃G, L⦄ ⊢ T ⬈*[h] T2 → R T → R T1) → + ∀T1. ⦃G, L⦄ ⊢ T1 ⬈*[h] T2 → R T1. +#h #G #L #T2 #R #HT2 #IHT2 #T1 #HT12 @(TC_star_ind_dx … HT2 IHT2 … HT12) // qed-. (* Basic properties *********************************************************) -lemma cpxs_refl: ∀h,o,G,L,T. ⦃G, L⦄ ⊢ T ⬈*[h, o] T. +lemma cpxs_refl: ∀h,G,L,T. ⦃G, L⦄ ⊢ T ⬈*[h] T. /2 width=1 by inj/ qed. -lemma cpx_cpxs: ∀h,o,G,L,T1,T2. ⦃G, L⦄ ⊢ T1 ⬈[h, o] T2 → ⦃G, L⦄ ⊢ T1 ⬈*[h, o] T2. +lemma cpx_cpxs: ∀h,G,L,T1,T2. ⦃G, L⦄ ⊢ T1 ⬈[h] T2 → ⦃G, L⦄ ⊢ T1 ⬈*[h] T2. /2 width=1 by inj/ qed. -lemma cpxs_strap1: ∀h,o,G,L,T1,T. ⦃G, L⦄ ⊢ T1 ⬈*[h, o] T → - ∀T2. ⦃G, L⦄ ⊢ T ⬈[h, o] T2 → ⦃G, L⦄ ⊢ T1 ⬈*[h, o] T2. -normalize /2 width=3 by step/ qed. +lemma cpxs_strap1: ∀h,G,L,T1,T. ⦃G, L⦄ ⊢ T1 ⬈*[h] T → + ∀T2. ⦃G, L⦄ ⊢ T ⬈[h] T2 → ⦃G, L⦄ ⊢ T1 ⬈*[h] T2. +normalize /2 width=3 by step/ qed-. -lemma cpxs_strap2: ∀h,o,G,L,T1,T. ⦃G, L⦄ ⊢ T1 ⬈[h, o] T → - ∀T2. ⦃G, L⦄ ⊢ T ⬈*[h, o] T2 → ⦃G, L⦄ ⊢ T1 ⬈*[h, o] T2. -normalize /2 width=3 by TC_strap/ qed. +lemma cpxs_strap2: ∀h,G,L,T1,T. ⦃G, L⦄ ⊢ T1 ⬈[h] T → + ∀T2. ⦃G, L⦄ ⊢ T ⬈*[h] T2 → ⦃G, L⦄ ⊢ T1 ⬈*[h] T2. +normalize /2 width=3 by TC_strap/ qed-. -lemma lsubr_cpxs_trans: ∀h,o,G. lsub_trans … (cpxs h o G) lsubr. -/3 width=5 by lsubr_cpx_trans, LTC_lsub_trans/ -qed-. - -lemma cprs_cpxs: ∀h,o,G,L,T1,T2. ⦃G, L⦄ ⊢ T1 ⬈* T2 → ⦃G, L⦄ ⊢ T1 ⬈*[h, o] T2. -#h #o #G #L #T1 #T2 #H @(cprs_ind … H) -T2 /3 width=3 by cpxs_strap1, cpr_cpx/ -qed. - -lemma cpxs_sort: ∀h,o,G,L,s,d1. deg h o s d1 → - ∀d2. d2 ≤ d1 → ⦃G, L⦄ ⊢ ⋆s ⬈*[h, o] ⋆((next h)^d2 s). -#h #o #G #L #s #d1 #Hkd1 #d2 @(nat_ind_plus … d2) -d2 /2 width=1 by cpx_cpxs/ -#d2 #IHd2 #Hd21 >iter_SO -@(cpxs_strap1 … (⋆(iter d2 ℕ (next h) s))) -[ /3 width=3 by lt_to_le/ -| @(cpx_st … (d1-d2-1)) iter_S /2 width=3 by cpxs_strap1/ qed. -lemma cpxs_bind_dx: ∀h,o,G,L,V1,V2. ⦃G, L⦄ ⊢ V1 ⬈[h, o] V2 → - ∀I,T1,T2. ⦃G, L. ⓑ{I}V1⦄ ⊢ T1 ⬈*[h, o] T2 → - ∀a. ⦃G, L⦄ ⊢ ⓑ{a,I}V1.T1 ⬈*[h, o] ⓑ{a,I}V2.T2. -#h #o #G #L #V1 #V2 #HV12 #I #T1 #T2 #HT12 #a @(cpxs_ind_dx … HT12) -T1 +lemma cpxs_bind_dx: ∀h,G,L,V1,V2. ⦃G, L⦄ ⊢ V1 ⬈[h] V2 → + ∀I,T1,T2. ⦃G, L. ⓑ{I}V1⦄ ⊢ T1 ⬈*[h] T2 → + ∀p. ⦃G, L⦄ ⊢ ⓑ{p,I}V1.T1 ⬈*[h] ⓑ{p,I}V2.T2. +#h #G #L #V1 #V2 #HV12 #I #T1 #T2 #HT12 #a @(cpxs_ind_dx … HT12) -T1 /3 width=3 by cpxs_strap2, cpx_cpxs, cpx_pair_sn, cpx_bind/ qed. -lemma cpxs_flat_dx: ∀h,o,G,L,V1,V2. ⦃G, L⦄ ⊢ V1 ⬈[h, o] V2 → - ∀T1,T2. ⦃G, L⦄ ⊢ T1 ⬈*[h, o] T2 → - ∀I. ⦃G, L⦄ ⊢ ⓕ{I}V1.T1 ⬈*[h, o] ⓕ{I}V2.T2. -#h #o #G #L #V1 #V2 #HV12 #T1 #T2 #HT12 @(cpxs_ind … HT12) -T2 +lemma cpxs_flat_dx: ∀h,G,L,V1,V2. ⦃G, L⦄ ⊢ V1 ⬈[h] V2 → + ∀T1,T2. ⦃G, L⦄ ⊢ T1 ⬈*[h] T2 → + ∀I. ⦃G, L⦄ ⊢ ⓕ{I}V1.T1 ⬈*[h] ⓕ{I}V2.T2. +#h #G #L #V1 #V2 #HV12 #T1 #T2 #HT12 @(cpxs_ind … HT12) -T2 /3 width=5 by cpxs_strap1, cpx_cpxs, cpx_pair_sn, cpx_flat/ qed. -lemma cpxs_flat_sn: ∀h,o,G,L,T1,T2. ⦃G, L⦄ ⊢ T1 ⬈[h, o] T2 → - ∀V1,V2. ⦃G, L⦄ ⊢ V1 ⬈*[h, o] V2 → - ∀I. ⦃G, L⦄ ⊢ ⓕ{I}V1.T1 ⬈*[h, o] ⓕ{I}V2.T2. -#h #o #G #L #T1 #T2 #HT12 #V1 #V2 #H @(cpxs_ind … H) -V2 +lemma cpxs_flat_sn: ∀h,G,L,T1,T2. ⦃G, L⦄ ⊢ T1 ⬈[h] T2 → + ∀V1,V2. ⦃G, L⦄ ⊢ V1 ⬈*[h] V2 → + ∀I. ⦃G, L⦄ ⊢ ⓕ{I}V1.T1 ⬈*[h] ⓕ{I}V2.T2. +#h #G #L #T1 #T2 #HT12 #V1 #V2 #H @(cpxs_ind … H) -V2 /3 width=5 by cpxs_strap1, cpx_cpxs, cpx_pair_sn, cpx_flat/ qed. -lemma cpxs_pair_sn: ∀h,o,I,G,L,V1,V2. ⦃G, L⦄ ⊢ V1 ⬈*[h, o] V2 → - ∀T. ⦃G, L⦄ ⊢ ②{I}V1.T ⬈*[h, o] ②{I}V2.T. -#h #o #I #G #L #V1 #V2 #H @(cpxs_ind … H) -V2 +lemma cpxs_pair_sn: ∀h,I,G,L,V1,V2. ⦃G, L⦄ ⊢ V1 ⬈*[h] V2 → + ∀T. ⦃G, L⦄ ⊢ ②{I}V1.T ⬈*[h] ②{I}V2.T. +#h #I #G #L #V1 #V2 #H @(cpxs_ind … H) -V2 /3 width=3 by cpxs_strap1, cpx_pair_sn/ qed. -lemma cpxs_zeta: ∀h,o,G,L,V,T1,T,T2. ⬆[0, 1] T2 ≡ T → - ⦃G, L.ⓓV⦄ ⊢ T1 ⬈*[h, o] T → ⦃G, L⦄ ⊢ +ⓓV.T1 ⬈*[h, o] T2. -#h #o #G #L #V #T1 #T #T2 #HT2 #H @(cpxs_ind_dx … H) -T1 +lemma cpxs_zeta: ∀h,G,L,V,T1,T,T2. ⬆*[1] T2 ≡ T → + ⦃G, L.ⓓV⦄ ⊢ T1 ⬈*[h] T → ⦃G, L⦄ ⊢ +ⓓV.T1 ⬈*[h] T2. +#h #G #L #V #T1 #T #T2 #HT2 #H @(cpxs_ind_dx … H) -T1 /3 width=3 by cpxs_strap2, cpx_cpxs, cpx_bind, cpx_zeta/ qed. -lemma cpxs_eps: ∀h,o,G,L,T1,T2. ⦃G, L⦄ ⊢ T1 ⬈*[h, o] T2 → - ∀V. ⦃G, L⦄ ⊢ ⓝV.T1 ⬈*[h, o] T2. -#h #o #G #L #T1 #T2 #H @(cpxs_ind … H) -T2 +lemma cpxs_eps: ∀h,G,L,T1,T2. ⦃G, L⦄ ⊢ T1 ⬈*[h] T2 → + ∀V. ⦃G, L⦄ ⊢ ⓝV.T1 ⬈*[h] T2. +#h #G #L #T1 #T2 #H @(cpxs_ind … H) -T2 /3 width=3 by cpxs_strap1, cpx_cpxs, cpx_eps/ qed. -lemma cpxs_ct: ∀h,o,G,L,V1,V2. ⦃G, L⦄ ⊢ V1 ⬈*[h, o] V2 → - ∀T. ⦃G, L⦄ ⊢ ⓝV1.T ⬈*[h, o] V2. -#h #o #G #L #V1 #V2 #H @(cpxs_ind … H) -V2 -/3 width=3 by cpxs_strap1, cpx_cpxs, cpx_ct/ +(* Basic_2A1: was: cpxs_ct *) +lemma cpxs_ee: ∀h,G,L,V1,V2. ⦃G, L⦄ ⊢ V1 ⬈*[h] V2 → + ∀T. ⦃G, L⦄ ⊢ ⓝV1.T ⬈*[h] V2. +#h #G #L #V1 #V2 #H @(cpxs_ind … H) -V2 +/3 width=3 by cpxs_strap1, cpx_cpxs, cpx_ee/ qed. -lemma cpxs_beta_dx: ∀h,o,a,G,L,V1,V2,W1,W2,T1,T2. - ⦃G, L⦄ ⊢ V1 ⬈[h, o] V2 → ⦃G, L.ⓛW1⦄ ⊢ T1 ⬈*[h, o] T2 → ⦃G, L⦄ ⊢ W1 ⬈[h, o] W2 → - ⦃G, L⦄ ⊢ ⓐV1.ⓛ{a}W1.T1 ⬈*[h, o] ⓓ{a}ⓝW2.V2.T2. -#h #o #a #G #L #V1 #V2 #W1 #W2 #T1 #T2 #HV12 * -T2 +lemma cpxs_beta_dx: ∀h,p,G,L,V1,V2,W1,W2,T1,T2. + ⦃G, L⦄ ⊢ V1 ⬈[h] V2 → ⦃G, L.ⓛW1⦄ ⊢ T1 ⬈*[h] T2 → ⦃G, L⦄ ⊢ W1 ⬈[h] W2 → + ⦃G, L⦄ ⊢ ⓐV1.ⓛ{p}W1.T1 ⬈*[h] ⓓ{p}ⓝW2.V2.T2. +#h #p #G #L #V1 #V2 #W1 #W2 #T1 #T2 #HV12 * -T2 /4 width=7 by cpx_cpxs, cpxs_strap1, cpxs_bind_dx, cpxs_flat_dx, cpx_beta/ qed. -lemma cpxs_theta_dx: ∀h,o,a,G,L,V1,V,V2,W1,W2,T1,T2. - ⦃G, L⦄ ⊢ V1 ⬈[h, o] V → ⬆[0, 1] V ≡ V2 → ⦃G, L.ⓓW1⦄ ⊢ T1 ⬈*[h, o] T2 → - ⦃G, L⦄ ⊢ W1 ⬈[h, o] W2 → ⦃G, L⦄ ⊢ ⓐV1.ⓓ{a}W1.T1 ⬈*[h, o] ⓓ{a}W2.ⓐV2.T2. -#h #o #a #G #L #V1 #V #V2 #W1 #W2 #T1 #T2 #HV1 #HV2 * -T2 +lemma cpxs_theta_dx: ∀h,p,G,L,V1,V,V2,W1,W2,T1,T2. + ⦃G, L⦄ ⊢ V1 ⬈[h] V → ⬆*[1] V ≡ V2 → ⦃G, L.ⓓW1⦄ ⊢ T1 ⬈*[h] T2 → + ⦃G, L⦄ ⊢ W1 ⬈[h] W2 → ⦃G, L⦄ ⊢ ⓐV1.ⓓ{p}W1.T1 ⬈*[h] ⓓ{p}W2.ⓐV2.T2. +#h #p #G #L #V1 #V #V2 #W1 #W2 #T1 #T2 #HV1 #HV2 * -T2 /4 width=9 by cpx_cpxs, cpxs_strap1, cpxs_bind_dx, cpxs_flat_dx, cpx_theta/ qed. (* Basic inversion lemmas ***************************************************) -lemma cpxs_inv_sort1: ∀h,o,G,L,U2,s. ⦃G, L⦄ ⊢ ⋆s ⬈*[h, o] U2 → - ∃∃n,d. deg h o s (n+d) & U2 = ⋆((next h)^n s). -#h #o #G #L #U2 #s #H @(cpxs_ind … H) -U2 -[ elim (deg_total h o s) #d #Hkd - @(ex2_2_intro … 0 … Hkd) -Hkd // -| #U #U2 #_ #HU2 * #n #d #Hknd #H destruct - elim (cpx_inv_sort1 … HU2) -HU2 - [ #H destruct /2 width=4 by ex2_2_intro/ - | * #d0 #Hkd0 #H destruct -d - @(ex2_2_intro … (n+1) d0) /2 width=1 by deg_inv_prec/ >iter_SO // - ] -] +(* Basic_2A1: wa just: cpxs_inv_sort1 *) +lemma cpxs_inv_sort1: ∀h,G,L,X2,s. ⦃G, L⦄ ⊢ ⋆s ⬈*[h] X2 → + ∃n. X2 = ⋆((next h)^n s). +#h #G #L #X2 #s #H @(cpxs_ind … H) -X2 /2 width=2 by ex_intro/ +#X #X2 #_ #HX2 * #n #H destruct +elim (cpx_inv_sort1 … HX2) -HX2 #H destruct /2 width=2 by ex_intro/ +@(ex_intro … (⫯n)) >iter_S // qed-. -lemma cpxs_inv_cast1: ∀h,o,G,L,W1,T1,U2. ⦃G, L⦄ ⊢ ⓝW1.T1 ⬈*[h, o] U2 → - ∨∨ ∃∃W2,T2. ⦃G, L⦄ ⊢ W1 ⬈*[h, o] W2 & ⦃G, L⦄ ⊢ T1 ⬈*[h, o] T2 & U2 = ⓝW2.T2 - | ⦃G, L⦄ ⊢ T1 ⬈*[h, o] U2 - | ⦃G, L⦄ ⊢ W1 ⬈*[h, o] U2. -#h #o #G #L #W1 #T1 #U2 #H @(cpxs_ind … H) -U2 /3 width=5 by or3_intro0, ex3_2_intro/ +lemma cpxs_inv_cast1: ∀h,G,L,W1,T1,U2. ⦃G, L⦄ ⊢ ⓝW1.T1 ⬈*[h] U2 → + ∨∨ ∃∃W2,T2. ⦃G, L⦄ ⊢ W1 ⬈*[h] W2 & ⦃G, L⦄ ⊢ T1 ⬈*[h] T2 & U2 = ⓝW2.T2 + | ⦃G, L⦄ ⊢ T1 ⬈*[h] U2 + | ⦃G, L⦄ ⊢ W1 ⬈*[h] U2. +#h #G #L #W1 #T1 #U2 #H @(cpxs_ind … H) -U2 /3 width=5 by or3_intro0, ex3_2_intro/ #U2 #U #_ #HU2 * /3 width=3 by cpxs_strap1, or3_intro1, or3_intro2/ * #W #T #HW1 #HT1 #H destruct elim (cpx_inv_cast1 … HU2) -HU2 /3 width=3 by cpxs_strap1, or3_intro1, or3_intro2/ * @@ -162,20 +144,3 @@ elim (cpx_inv_cast1 … HU2) -HU2 /3 width=3 by cpxs_strap1, or3_intro1, or3_int lapply (cpxs_strap1 … HW1 … HW2) -W lapply (cpxs_strap1 … HT1 … HT2) -T /3 width=5 by or3_intro0, ex3_2_intro/ qed-. - -lemma cpxs_inv_cnx1: ∀h,o,G,L,T,U. ⦃G, L⦄ ⊢ T ⬈*[h, o] U → ⦃G, L⦄ ⊢ ⬈[h, o] 𝐍⦃T⦄ → T = U. -#h #o #G #L #T #U #H @(cpxs_ind_dx … H) -T // -#T0 #T #H1T0 #_ #IHT #H2T0 -lapply (H2T0 … H1T0) -H1T0 #H destruct /2 width=1 by/ -qed-. - -lemma cpxs_neq_inv_step_sn: ∀h,o,G,L,T1,T2. ⦃G, L⦄ ⊢ T1 ⬈*[h, o] T2 → (T1 = T2 → ⊥) → - ∃∃T. ⦃G, L⦄ ⊢ T1 ⬈[h, o] T & T1 = T → ⊥ & ⦃G, L⦄ ⊢ T ⬈*[h, o] T2. -#h #o #G #L #T1 #T2 #H @(cpxs_ind_dx … H) -T1 -[ #H elim H -H // -| #T1 #T #H1 #H2 #IH2 #H12 elim (eq_term_dec T1 T) #H destruct - [ -H1 -H2 /3 width=1 by/ - | -IH2 /3 width=4 by ex3_intro/ (**) (* auto fails without clear *) - ] -] -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 new file mode 100644 index 000000000..027135514 --- /dev/null +++ b/matita/matita/contribs/lambdadelta/basic_2/rt_computation/cpxs_tdeq.ma @@ -0,0 +1,55 @@ +(**************************************************************************) +(* ___ *) +(* ||M|| *) +(* ||A|| A project by Andrea Asperti *) +(* ||T|| *) +(* ||I|| Developers: *) +(* ||T|| The HELM team. *) +(* ||A|| http://helm.cs.unibo.it *) +(* \ / *) +(* \ / This file is distributed under the terms of the *) +(* v GNU General Public License Version 2 *) +(* *) +(**************************************************************************) + +include "basic_2/syntax/tdeq_tdeq.ma". +include "basic_2/rt_computation/cpxs.ma". +include "basic_2/rt_transition/cpx_lfdeq.ma". +include "basic_2/static/lfdeq_fqup.ma". +include "basic_2/rt_transition/lfpx_fqup.ma". + +(* UNCOUNTED CONTEXT-SENSITIVE PARALLEL RT-COMPUTATION FOR TERMS ************) + +axiom tdeq_dec: ∀h,o,T1,T2. Decidable (tdeq h o T1 T2). + +axiom tdeq_canc_sn: ∀h,o. left_cancellable … (tdeq h o). + +lemma tdeq_cpx_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 +elim (cpx_tdeq_conf_lexs … o … HT12 … U1 … L … L) /3 width=3 by tdeq_sym, ex2_intro/ +qed-. + +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. +#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 + [ -H1 -H2 elim IH -IH /3 width=3 by tdeq_trans/ -Hn12 + #X #X2 #HTX #HnTX #HX2 #HXT2 elim (tdeq_cpx_trans … H … HTX) -HTX + #X1 #HTX1 #HX1 elim (tdeq_cpxs_trans … HX1 … HX2) -HX2 + /5 width=8 by tdeq_canc_sn, tdeq_trans, ex4_2_intro/ (* Note: 2 tdeq_trans *) + | -IH -Hn12 /3 width=6 by ex4_2_intro/ + ] +] +qed-. + +(* Basic_2A1: removed theorems 1: cpxs_neq_inv_step_sn *) diff --git a/matita/matita/contribs/lambdadelta/basic_2/rt_computation/partial.txt b/matita/matita/contribs/lambdadelta/basic_2/rt_computation/partial.txt new file mode 100644 index 000000000..41a6c9556 --- /dev/null +++ b/matita/matita/contribs/lambdadelta/basic_2/rt_computation/partial.txt @@ -0,0 +1 @@ +cpxs.ma diff --git a/matita/matita/contribs/lambdadelta/basic_2/rt_transition/cnx.ma b/matita/matita/contribs/lambdadelta/basic_2/rt_transition/cnx.ma new file mode 100644 index 000000000..5eb721b20 --- /dev/null +++ b/matita/matita/contribs/lambdadelta/basic_2/rt_transition/cnx.ma @@ -0,0 +1,81 @@ +(**************************************************************************) +(* ___ *) +(* ||M|| *) +(* ||A|| A project by Andrea Asperti *) +(* ||T|| *) +(* ||I|| Developers: *) +(* ||T|| The HELM team. *) +(* ||A|| http://helm.cs.unibo.it *) +(* \ / *) +(* \ / This file is distributed under the terms of the *) +(* v GNU General Public License Version 2 *) +(* *) +(**************************************************************************) + +include "basic_2/notation/relations/predtynormal_5.ma". +include "basic_2/syntax/tdeq.ma". +include "basic_2/rt_transition/cpx.ma". + +(* NORMAL TERMS FOR UNCOUNTED CONTEXT-SENSITIVE PARALLEL RT-TRANSITION ******) + +definition cnx: ∀h. sd h → relation3 genv lenv term ≝ + λh,o,G,L. NF … (cpx h G L) (tdeq h o …). + +interpretation + "normality for uncounted context-sensitive parallel rt-transition (term)" + 'PRedTyNormal h o G L T = (cnx h o G L T). + +(* Basic inversion lemmas ***************************************************) + +lemma cnx_inv_sort: ∀h,o,G,L,s. ⦃G, L⦄ ⊢ ⬈[h, o] 𝐍⦃⋆s⦄ → deg h o s 0. +#h #o #G #L #s #H +lapply (H (⋆(next h s)) ?) -H /2 width=2 by cpx_ess/ -G -L #H +elim (tdeq_inv_sort1 … H) -H #s0 #d #H1 #H2 #H destruct +lapply (deg_next … H1) #H0 +lapply (deg_mono … H0 … H2) -H0 -H2 #H +<(pred_inv_refl … H) -H // +qed-. + +lemma cnx_inv_abst: ∀h,o,p,G,L,V,T. ⦃G, L⦄ ⊢ ⬈[h, o] 𝐍⦃ⓛ{p}V.T⦄ → + ⦃G, L⦄ ⊢ ⬈[h, o] 𝐍⦃V⦄ ∧ ⦃G, L.ⓛV⦄ ⊢ ⬈[h, o] 𝐍⦃T⦄. +#h #o #p #G #L #V1 #T1 #HVT1 @conj +[ #V2 #HV2 lapply (HVT1 (ⓛ{p}V2.T1) ?) -HVT1 /2 width=2 by cpx_pair_sn/ -HV2 +| #T2 #HT2 lapply (HVT1 (ⓛ{p}V1.T2) ?) -HVT1 /2 width=2 by cpx_bind/ -HT2 +] +#H elim (tdeq_inv_pair … H) -H // +qed-. + +(* Basic_2A1: was: cnx_inv_abbr *) +lemma cnx_inv_abbr_neg: ∀h,o,G,L,V,T. ⦃G, L⦄ ⊢ ⬈[h, o] 𝐍⦃-ⓓV.T⦄ → + ⦃G, L⦄ ⊢ ⬈[h, o] 𝐍⦃V⦄ ∧ ⦃G, L.ⓓV⦄ ⊢ ⬈[h, o] 𝐍⦃T⦄. +#h #o #G #L #V1 #T1 #HVT1 @conj +[ #V2 #HV2 lapply (HVT1 (-ⓓV2.T1) ?) -HVT1 /2 width=2 by cpx_pair_sn/ -HV2 +| #T2 #HT2 lapply (HVT1 (-ⓓV1.T2) ?) -HVT1 /2 width=2 by cpx_bind/ -HT2 +] +#H elim (tdeq_inv_pair … H) -H // +qed-. + +(* Basic_2A1: was: cnx_inv_eps *) +lemma cnx_inv_cast: ∀h,o,G,L,V,T. ⦃G, L⦄ ⊢ ⬈[h, o] 𝐍⦃ⓝV.T⦄ → ⊥. +#h #o #G #L #V #T #H lapply (H T ?) -H +/2 width=6 by cpx_eps, tdeq_inv_pair_xy_y/ +qed-. + +(* Basic properties *********************************************************) + +lemma cnx_sort: ∀h,o,G,L,s. deg h o s 0 → ⦃G, L⦄ ⊢ ⬈[h, o] 𝐍⦃⋆s⦄. +#h #o #G #L #s #Hs #X #H elim (cpx_inv_sort1 … H) -H +/3 width=3 by tdeq_sort, deg_next/ +qed. + +lemma cnx_sort_iter: ∀h,o,G,L,s,d. deg h o s d → ⦃G, L⦄ ⊢ ⬈[h, o] 𝐍⦃⋆((next h)^d s)⦄. +#h #o #G #L #s #d #Hs lapply (deg_iter … d Hs) -Hs +(HLT0 … HTX0) in HX0; -L0 -X0 #H >(lift_inj … H … HT0) -T0 -X -l -k // qed-. +*) diff --git a/matita/matita/contribs/lambdadelta/basic_2/rt_transition/cnx_simple.ma b/matita/matita/contribs/lambdadelta/basic_2/rt_transition/cnx_simple.ma new file mode 100644 index 000000000..272b82442 --- /dev/null +++ b/matita/matita/contribs/lambdadelta/basic_2/rt_transition/cnx_simple.ma @@ -0,0 +1,47 @@ +(**************************************************************************) +(* ___ *) +(* ||M|| *) +(* ||A|| A project by Andrea Asperti *) +(* ||T|| *) +(* ||I|| Developers: *) +(* ||T|| The HELM team. *) +(* ||A|| http://helm.cs.unibo.it *) +(* \ / *) +(* \ / This file is distributed under the terms of the *) +(* v GNU General Public License Version 2 *) +(* *) +(**************************************************************************) + +include "basic_2/rt_transition/cpx_simple.ma". +include "basic_2/rt_transition/cnx.ma". + +(* NORMAL TERMS FOR UNCOUNTED CONTEXT-SENSITIVE PARALLEL RT-TRANSITION ******) + +(* Inversion lemmas with simple terms ***************************************) + +lemma cnx_inv_appl: ∀h,o,G,L,V,T. ⦃G, L⦄ ⊢ ⬈[h, o] 𝐍⦃ⓐV.T⦄ → + ∧∧ ⦃G, L⦄ ⊢ ⬈[h, o] 𝐍⦃V⦄ & ⦃G, L⦄ ⊢ ⬈[h, o] 𝐍⦃T⦄ & 𝐒⦃T⦄. +#h #o #G #L #V1 #T1 #HVT1 @and3_intro +[ #V2 #HV2 lapply (HVT1 (ⓐV2.T1) ?) -HVT1 /2 width=1 by cpx_pair_sn/ -HV2 + #H elim (tdeq_inv_pair … H) -H // +| #T2 #HT2 lapply (HVT1 (ⓐV1.T2) ?) -HVT1 /2 width=1 by cpx_flat/ -HT2 + #H elim (tdeq_inv_pair … H) -H // +| generalize in match HVT1; -HVT1 elim T1 -T1 * // + #p * #W1 #U1 #_ #_ #H + [ elim (lifts_total V1 (𝐔❴1❵)) #V2 #HV12 + lapply (H (ⓓ{p}W1.ⓐV2.U1) ?) -H /2 width=3 by cpx_theta/ -HV12 + #H elim (tdeq_inv_pair … H) -H #H destruct + | lapply (H (ⓓ{p}ⓝW1.V1.U1) ?) -H /2 width=1 by cpx_beta/ + #H elim (tdeq_inv_pair … H) -H #H destruct + ] +] +qed-. + +(* Properties with simple terms *********************************************) + +lemma cnx_appl_simple: ∀h,o,G,L,V,T. ⦃G, L⦄ ⊢ ⬈[h, o] 𝐍⦃V⦄ → ⦃G, L⦄ ⊢ ⬈[h, o] 𝐍⦃T⦄ → 𝐒⦃T⦄ → + ⦃G, L⦄ ⊢ ⬈[h, o] 𝐍⦃ⓐV.T⦄. +#h #o #G #L #V #T #HV #HT #HS #X #H elim (cpx_inv_appl1_simple … H) -H // +#V0 #T0 #HV0 #HT0 #H destruct +@tdeq_pair [ @HV | @HT ] // (**) (* auto fails because δ-expansion gets in the way *) +qed. diff --git a/matita/matita/contribs/lambdadelta/basic_2/rt_transition/partial.txt b/matita/matita/contribs/lambdadelta/basic_2/rt_transition/partial.txt index d00ba2bea..9760148c1 100644 --- a/matita/matita/contribs/lambdadelta/basic_2/rt_transition/partial.txt +++ b/matita/matita/contribs/lambdadelta/basic_2/rt_transition/partial.txt @@ -1,6 +1,7 @@ cpg.ma cpg_simple.ma cpg_drops.ma cpg_lsubr.ma cpx.ma cpx_simple.ma cpx_drops.ma cpx_fqus.ma cpx_lsubr.ma cpx_lfxs.ma cpx_lfdeq.ma lfpx.ma lfpx_length.ma lfpx_drops.ma lfpx_fqup.ma lfpx_frees.ma lfpx_aaa.ma +cnx.ma cnx_simple.ma cpm.ma cpm_simple.ma cpm_drops.ma cpm_lsubr.ma cpm_lfxs.ma cpm_cpx.ma cpr.ma cpr_drops.ma lfpr.ma lfpr_length.ma lfpr_drops.ma lfpr_fqup.ma lfpr_frees.ma lfpr_aaa.ma lfpr_lfpx.ma lfpr_lfpr.ma diff --git a/matita/matita/contribs/lambdadelta/basic_2/syntax/tdeq.ma b/matita/matita/contribs/lambdadelta/basic_2/syntax/tdeq.ma index 21d140e51..c79c1940c 100644 --- a/matita/matita/contribs/lambdadelta/basic_2/syntax/tdeq.ma +++ b/matita/matita/contribs/lambdadelta/basic_2/syntax/tdeq.ma @@ -103,11 +103,18 @@ lemma tdeq_inv_sort1_deg: ∀h,o,Y,s1. ⋆s1 ≡[h, o] Y → ∀d. deg h o s1 d #s2 #x #Hx <(deg_mono h o … Hx … Hs1) -s1 -d /2 width=3 by ex2_intro/ qed-. -lemma tdeq_inv_pair: ∀h,o,I,V1,V2,T1,T2. ②{I}V1.T1 ≡[h, o] ②{I}V2.T2 → - V1 ≡[h, o] V2 ∧ T1 ≡[h, o] T2. -#h #o #I #V1 #V2 #T1 #T2 #H elim (tdeq_inv_pair1 … H) -H -#V0 #T0 #HV #HT #H destruct /2 width=1 by conj/ -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. +#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 → ⊥. +#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/ +] +qed-. (* Basic forward lemmas *****************************************************) 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 e920f2c0d..bd2ddaa42 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 @@ -78,8 +78,10 @@ table { ] } ] +*) class "cyan" - [ { "computation" * } { + [ { "rt-computation" * } { +(* [ { "evaluation for context-sensitive rt-reduction" * } { [ "cpxe ( ⦃?,?⦄ ⊢ ➡*[?,?] 𝐍⦃?⦄ )" * ] } @@ -108,16 +110,21 @@ table { [ "scpds ( ⦃?,?⦄ ⊢ ? •*➡*[?,?,?] ? )" "scpds_lift" + "scpds_aaa" + "scpds_scpds" * ] } ] - [ { "context-sensitive rt-computation" * } { - [ "lpxs ( ⦃?,?⦄ ⊢ ➡*[?,?] ? )" "lpxs_drop" + "lpxs_lleq" + "lpxs_aaa" + "lpxs_cpxs" + "lpxs_lpxs" * ] - [ "cpxs ( ⦃?,?⦄ ⊢ ? ➡*[?,?] ? )" "cpxs_tsts" + "cpxs_tsts_vector" + "cpxs_lreq" + "cpxs_lift" + "cpxs_lleq" + "cpxs_aaa" + "cpxs_cpxs" * ] - } - ] [ { "context-sensitive computation" * } { [ "lprs ( ⦃?,?⦄ ⊢ ➡* ? )" "lprs_drop" + "lprs_cprs" + "lprs_lprs" * ] [ "cprs ( ⦃?,?⦄ ⊢ ? ➡* ?)" "cprs_lift" + "cprs_cprs" * ] } ] +*) + [ { "uncounted context-sensitive rt-transition" * } { +(* + [ "lpxs ( ⦃?,?⦄ ⊢ ➡*[?,?] ? )" "lpxs_drop" + "lpxs_lleq" + "lpxs_aaa" + "lpxs_cpxs" + "lpxs_lpxs" * ] + [ "cpxs_tsts" + "cpxs_tsts_vector" + "cpxs_lreq" + "cpxs_lift" + "cpxs_lleq" + "cpxs_aaa" + "cpxs_cpxs" * ] +*) + [ "cpxs ( ⦃?,?⦄ ⊢ ? ⬈*[?] ? )" * ] + } + ] +(* [ { "local env. ref. for generic reducibility" * } { [ "lsubc ( ? ⊢ ? ⫃[?] ? )" "lsubc_drop" + "lsubc_drops" + "lsubc_lsuba" * ] } @@ -126,9 +133,9 @@ table { [ "gcp" "gcp_cr ( ⦃?,?,?⦄ ϵ[?] 〚?〛 )" "gcp_aaa" * ] } ] +*) } ] -*) class "water" [ { "rt-transition" * } { [ { "parallel qrst-rtransition" * } { @@ -150,6 +157,7 @@ table { } ] [ { "uncounted context-sensitive rt-transition" * } { + [ "cnx ( ⦃?,?⦄ ⊢ ⬈[?,?] 𝐍⦃?⦄ )" "cnx_simple" + "cnx_drops" * ] [ "lfpx ( ⦃?,?⦄ ⊢ ⬈[?,?] ? )" "lfpx_length" + "lfpx_drops" + "lfpx_fqup" + "lfpx_frees" + "lfpx_aaa" * ] [ "cpx ( ⦃?,?⦄ ⊢ ? ⬈[?] ? )" "cpx_simple" + "cpx_drops" + "cpx_fqus" + "cpx_lsubr" + "cpx_lfxs" + "cpx_lfdeq" * ] } @@ -162,19 +170,13 @@ table { ] class "green" [ { "static typing" * } { - [ { "restricted ref. for atomic arity assignment" * } { - [ "lsuba ( ? ⊢ ? ⫃⁝ ? )" "lsuba_drops" + "lsuba_lsubr" + "lsuba_aaa" + "lsuba_lsuba" * ] - } - ] [ { "atomic arity assignment" * } { + [ "lsuba ( ? ⊢ ? ⫃⁝ ? )" "lsuba_drops" + "lsuba_lsubr" + "lsuba_aaa" + "lsuba_lsuba" * ] [ "aaa ( ⦃?,?⦄ ⊢ ? ⁝ ? )" "aaa_drops" + "aaa_fqus" + "aaa_lfdeq" + "aaa_aaa" * ] } ] - [ { "degree-based equivalence for closures on referred entries" * } { + [ { "degree-based equivalence on referred entries" * } { [ "ffdeq ( ⦃?,?,?⦄ ≡[?,?] ⦃?,?,?⦄ )" "ffdeq_fqup" + "ffdeq_ffdeq" * ] - } - ] - [ { "degree-based equivalence for local environments on referred entries" * } { [ "lfdeq ( ? ≡[?,?,?] ? )" "lfdeq_length" + "lfdeq_fqup" + "lfdeq_lfdeq" * ] } ] @@ -182,11 +184,8 @@ table { [ "lfxs ( ? ⦻*[?,?] ? )" "lfxs_length" + "lfxs_drops" + "lfxs_fqup" + "lfxs_lfxs" * ] } ] - [ { "restricted ref. for context-sensitive free variables" * } { - [ "lsubf ( ⦃?,?⦄ ⫃𝐅* ⦃?,?⦄ )" "lsubf_frees" * ] - } - ] [ { "context-sensitive free variables" * } { + [ "lsubf ( ⦃?,?⦄ ⫃𝐅* ⦃?,?⦄ )" "lsubf_frees" * ] [ "frees ( ? ⊢ 𝐅*⦃?⦄ ≡ ? )" "frees_weight" + "frees_drops" + "frees_fqup" + "frees_frees" * ] } ] @@ -293,7 +292,7 @@ class "capitalize italic" { 0 } class "italic" { 1 } (* [ { "normal forms for context-sensitive rt-reduction" * } { - [ "cnx ( ⦃?,?⦄ ⊢ ➡[?,?] 𝐍⦃?⦄ )" "cnx_lift" + "cnx_crx" + "cnx_cix" * ] + [ "cnx_crx" + "cnx_cix" * ] } ] [ { "irreducible forms for context-sensitive rt-reduction" * } { diff --git a/matita/matita/contribs/lambdadelta/ground_2/lib/star.ma b/matita/matita/contribs/lambdadelta/ground_2/lib/star.ma index b0e3e6be6..26832eb42 100644 --- a/matita/matita/contribs/lambdadelta/ground_2/lib/star.ma +++ b/matita/matita/contribs/lambdadelta/ground_2/lib/star.ma @@ -135,14 +135,14 @@ lemma TC_transitive2: ∀A,R1,R2. qed. definition NF: ∀A. relation A → relation A → predicate A ≝ - λA,R,S,a1. ∀a2. R a1 a2 → S a2 a1. + λA,R,S,a1. ∀a2. R a1 a2 → S a1 a2. definition NF_dec: ∀A. relation A → relation A → Prop ≝ λA,R,S. ∀a1. NF A R S a1 ∨ - ∃∃a2. R … a1 a2 & (S a2 a1 → ⊥). + ∃∃a2. R … a1 a2 & (S a1 a2 → ⊥). inductive SN (A) (R,S:relation A): predicate A ≝ -| SN_intro: ∀a1. (∀a2. R a1 a2 → (S a2 a1 → ⊥) → SN A R S a2) → SN A R S a1 +| SN_intro: ∀a1. (∀a2. R a1 a2 → (S a1 a2 → ⊥) → SN A R S a2) → SN A R S a1 . lemma NF_to_SN: ∀A,R,S,a. NF A R S a → SN A R S a. @@ -160,10 +160,10 @@ lemma SN_to_NF: ∀A,R,S. NF_dec A R S → qed-. definition NF_sn: ∀A. relation A → relation A → predicate A ≝ - λA,R,S,a2. ∀a1. R a1 a2 → S a2 a1. + λA,R,S,a2. ∀a1. R a1 a2 → S a1 a2. inductive SN_sn (A) (R,S:relation A): predicate A ≝ -| SN_sn_intro: ∀a2. (∀a1. R a1 a2 → (S a2 a1 → ⊥) → SN_sn A R S a1) → SN_sn A R S a2 +| SN_sn_intro: ∀a2. (∀a1. R a1 a2 → (S a1 a2 → ⊥) → SN_sn A R S a1) → SN_sn A R S a2 . lemma NF_to_SN_sn: ∀A,R,S,a. NF_sn A R S a → SN_sn A R S a. diff --git a/matita/matita/contribs/lambdadelta/basic_2/rt_transition/hls.ml b/matita/matita/contribs/lambdadelta/hls.ml similarity index 100% rename from matita/matita/contribs/lambdadelta/basic_2/rt_transition/hls.ml rename to matita/matita/contribs/lambdadelta/hls.ml -- 2.39.2