From: Ferruccio Guidi Date: Sat, 10 Mar 2018 15:46:54 +0000 (+0100) Subject: bugfix update in basic_2 X-Git-Tag: make_still_working~356 X-Git-Url: http://matita.cs.unibo.it/gitweb/?a=commitdiff_plain;h=b3afed9fd3cc38ecd4578f6b0741be50872a2828;p=helm.git bugfix update in basic_2 + bugfix in ffdeq + bugfix in fpbq + minor fixes --- 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 deleted file mode 100644 index c4af5a9a4..000000000 --- a/matita/matita/contribs/lambdadelta/basic_2/notation/relations/btpred_7.ma +++ /dev/null @@ -1,19 +0,0 @@ -(**************************************************************************) -(* ___ *) -(* ||M|| *) -(* ||A|| A project by Andrea Asperti *) -(* ||T|| *) -(* ||I|| Developers: *) -(* ||T|| The HELM team. *) -(* ||A|| http://helm.cs.unibo.it *) -(* \ / *) -(* \ / This file is distributed under the terms of the *) -(* v GNU General Public License Version 2 *) -(* *) -(**************************************************************************) - -(* NOTATION FOR THE FORMAL SYSTEM λδ ****************************************) - -notation "hvbox( ⦃ term 46 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 deleted file mode 100644 index b9e0ccc98..000000000 --- a/matita/matita/contribs/lambdadelta/basic_2/notation/relations/btpredproper_8.ma +++ /dev/null @@ -1,19 +0,0 @@ -(**************************************************************************) -(* ___ *) -(* ||M|| *) -(* ||A|| A project by Andrea Asperti *) -(* ||T|| *) -(* ||I|| Developers: *) -(* ||T|| The HELM team. *) -(* ||A|| http://helm.cs.unibo.it *) -(* \ / *) -(* \ / This file is distributed under the terms of the *) -(* v GNU General Public License Version 2 *) -(* *) -(**************************************************************************) - -(* NOTATION FOR THE FORMAL SYSTEM λδ ****************************************) - -notation "hvbox( ⦃ term 46 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 deleted file mode 100644 index 065d3769e..000000000 --- a/matita/matita/contribs/lambdadelta/basic_2/notation/relations/btpredstar_8.ma +++ /dev/null @@ -1,19 +0,0 @@ -(**************************************************************************) -(* ___ *) -(* ||M|| *) -(* ||A|| A project by Andrea Asperti *) -(* ||T|| *) -(* ||I|| Developers: *) -(* ||T|| The HELM team. *) -(* ||A|| http://helm.cs.unibo.it *) -(* \ / *) -(* \ / This file is distributed under the terms of the *) -(* v GNU General Public License Version 2 *) -(* *) -(**************************************************************************) - -(* NOTATION FOR THE FORMAL SYSTEM λδ ****************************************) - -notation "hvbox( ⦃ term 46 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/predsubty_8.ma b/matita/matita/contribs/lambdadelta/basic_2/notation/relations/predsubty_8.ma new file mode 100644 index 000000000..d7a706d71 --- /dev/null +++ b/matita/matita/contribs/lambdadelta/basic_2/notation/relations/predsubty_8.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 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 @{ 'PRedSubTy $h $o $G1 $L1 $T1 $G2 $L2 $T2 }. diff --git a/matita/matita/contribs/lambdadelta/basic_2/notation/relations/predsubtyproper_8.ma b/matita/matita/contribs/lambdadelta/basic_2/notation/relations/predsubtyproper_8.ma new file mode 100644 index 000000000..6dc58b058 --- /dev/null +++ b/matita/matita/contribs/lambdadelta/basic_2/notation/relations/predsubtyproper_8.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 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 @{ 'PRedSubTyProper $h $o $G1 $L1 $T1 $G2 $L2 $T2 }. diff --git a/matita/matita/contribs/lambdadelta/basic_2/notation/relations/predsubtystar_8.ma b/matita/matita/contribs/lambdadelta/basic_2/notation/relations/predsubtystar_8.ma new file mode 100644 index 000000000..75f409cee --- /dev/null +++ b/matita/matita/contribs/lambdadelta/basic_2/notation/relations/predsubtystar_8.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 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 @{ 'PRedSubTyStar $h $o $G1 $L1 $T1 $G2 $L2 $T2 }. 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 1ccc9ca6d..39de38ce2 100644 --- a/matita/matita/contribs/lambdadelta/basic_2/rt_transition/fpb.ma +++ b/matita/matita/contribs/lambdadelta/basic_2/rt_transition/fpb.ma @@ -12,7 +12,7 @@ (* *) (**************************************************************************) -include "basic_2/notation/relations/btpredproper_8.ma". +include "basic_2/notation/relations/predsubtyproper_8.ma". include "basic_2/s_transition/fqu.ma". include "basic_2/static/lfdeq.ma". include "basic_2/rt_transition/lfpr_lfpx.ma". @@ -27,7 +27,7 @@ inductive fpb (h) (o) (G1) (L1) (T1): relation3 genv lenv term ≝ interpretation "proper parallel rst-transition (closure)" - 'BTPRedProper h o G1 L1 T1 G2 L2 T2 = (fpb h o G1 L1 T1 G2 L2 T2). + 'PRedSubTyProper h o G1 L1 T1 G2 L2 T2 = (fpb h o G1 L1 T1 G2 L2 T2). (* Basic properties *********************************************************) 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 1bacae106..c4489bccf 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 @@ -29,8 +29,8 @@ lemma lfdeq_fpb_trans: ∀h,o,F,K1,K2,T. K1 ≛[h, o, T] K2 → [ #G #L2 #U #H2 elim (lfdeq_fqu_trans … H2 … HT) -K2 /3 width=5 by fpb_fqu, ex3_2_intro/ | #U #HTU #HnTU elim (lfdeq_cpx_trans … HT … HTU) -HTU - /5 width=10 by fpb_cpx, cpx_lfdeq_conf_sn, tdeq_trans, tdeq_lfdeq_conf_sn, ex3_2_intro/ + /5 width=10 by fpb_cpx, cpx_lfdeq_conf_sn, tdeq_trans, tdeq_lfdeq_conf, ex3_2_intro/ | #L2 #HKL2 #HnKL2 elim (lfdeq_lfpx_trans … HKL2 … HT) -HKL2 - /6 width=5 by fpb_lfpx, lfdeq_canc_sn, ex3_2_intro/ (* 2 lleq_canc_sn *) + /6 width=5 by fpb_lfpx, (* 2x *) lfdeq_canc_sn, ex3_2_intro/ ] qed-. diff --git a/matita/matita/contribs/lambdadelta/basic_2/rt_transition/fpbq.ma b/matita/matita/contribs/lambdadelta/basic_2/rt_transition/fpbq.ma index 023c39fa2..869f3e118 100644 --- a/matita/matita/contribs/lambdadelta/basic_2/rt_transition/fpbq.ma +++ b/matita/matita/contribs/lambdadelta/basic_2/rt_transition/fpbq.ma @@ -12,33 +12,35 @@ (* *) (**************************************************************************) -include "basic_2/notation/relations/btpred_7.ma". +include "basic_2/notation/relations/predsubty_8.ma". +include "basic_2/static/ffdeq.ma". include "basic_2/s_transition/fquq.ma". include "basic_2/rt_transition/lfpr_lfpx.ma". (* PARALLEL RST-TRANSITION FOR CLOSURES *************************************) (* Basic_2A1: includes: fpbq_lleq *) -inductive fpbq (h) (G1) (L1) (T1): relation3 genv lenv term ≝ -| fpbq_fquq: ∀G2,L2,T2. ⦃G1, L1, T1⦄ ⊐⸮ ⦃G2, L2, T2⦄ → fpbq h G1 L1 T1 G2 L2 T2 -| fpbq_cpx : ∀T2. ⦃G1, L1⦄ ⊢ T1 ⬈[h] T2 → fpbq h G1 L1 T1 G1 L1 T2 -| fpbq_lfpx: ∀L2. ⦃G1, L1⦄ ⊢ ⬈[h, T1] L2 → fpbq h G1 L1 T1 G1 L2 T1 +inductive fpbq (h) (o) (G1) (L1) (T1): relation3 genv lenv term ≝ +| fpbq_fquq : ∀G2,L2,T2. ⦃G1, L1, T1⦄ ⊐⸮ ⦃G2, L2, T2⦄ → fpbq h o G1 L1 T1 G2 L2 T2 +| fpbq_cpx : ∀T2. ⦃G1, L1⦄ ⊢ T1 ⬈[h] T2 → fpbq h o G1 L1 T1 G1 L1 T2 +| fpbq_lfpx : ∀L2. ⦃G1, L1⦄ ⊢ ⬈[h, T1] L2 → fpbq h o G1 L1 T1 G1 L2 T1 +| ffpq_lfdeq: ∀G2,L2,T2. ⦃G1, L1, T1⦄ ≛[h, o] ⦃G2, L2, T2⦄ → fpbq h o G1 L1 T1 G2 L2 T2 . interpretation "parallel rst-transition (closure)" - 'BTPRed h G1 L1 T1 G2 L2 T2 = (fpbq h G1 L1 T1 G2 L2 T2). + 'PRedSubTy h o G1 L1 T1 G2 L2 T2 = (fpbq h o G1 L1 T1 G2 L2 T2). (* Basic properties *********************************************************) -lemma fpbq_refl: ∀h. tri_reflexive … (fpbq h). +lemma fpbq_refl: ∀h,o. tri_reflexive … (fpbq h o). /2 width=1 by fpbq_cpx/ qed. (* Basic_2A1: includes: cpr_fpbq *) -lemma cpm_fpbq: ∀n,h,G,L,T1,T2. ⦃G, L⦄ ⊢ T1 ➡[n, h] T2 → ⦃G, L, T1⦄ ≽[h] ⦃G, L, T2⦄. +lemma cpm_fpbq: ∀n,h,o,G,L,T1,T2. ⦃G, L⦄ ⊢ T1 ➡[n, h] T2 → ⦃G, L, T1⦄ ≽[h, o] ⦃G, L, T2⦄. /3 width=2 by fpbq_cpx, cpm_fwd_cpx/ qed. -lemma lfpr_fpbq: ∀h,G,L1,L2,T. ⦃G, L1⦄ ⊢ ➡[h, T] L2 → ⦃G, L1, T⦄ ≽[h] ⦃G, L2, T⦄. +lemma lfpr_fpbq: ∀h,o,G,L1,L2,T. ⦃G, L1⦄ ⊢ ➡[h, T] L2 → ⦃G, L1, T⦄ ≽[h, o] ⦃G, L2, T⦄. /3 width=1 by fpbq_lfpx, lfpr_fwd_lfpx/ qed. (* Basic_2A1: removed theorems 2: diff --git a/matita/matita/contribs/lambdadelta/basic_2/rt_transition/fpbq_aaa.ma b/matita/matita/contribs/lambdadelta/basic_2/rt_transition/fpbq_aaa.ma index a6c5f719e..4330c1852 100644 --- a/matita/matita/contribs/lambdadelta/basic_2/rt_transition/fpbq_aaa.ma +++ b/matita/matita/contribs/lambdadelta/basic_2/rt_transition/fpbq_aaa.ma @@ -13,6 +13,7 @@ (**************************************************************************) include "basic_2/static/aaa_fqus.ma". +include "basic_2/static/aaa_ffdeq.ma". include "basic_2/rt_transition/lfpx_aaa.ma". include "basic_2/rt_transition/fpbq.ma". @@ -20,8 +21,8 @@ include "basic_2/rt_transition/fpbq.ma". (* Properties with atomic arity assignment for terms ************************) -lemma fpbq_aaa_conf: ∀h,G1,G2,L1,L2,T1,T2. ⦃G1, L1, T1⦄ ≽[h] ⦃G2, L2, T2⦄ → +lemma fpbq_aaa_conf: ∀h,o,G1,G2,L1,L2,T1,T2. ⦃G1, L1, T1⦄ ≽[h, o] ⦃G2, L2, T2⦄ → ∀A1. ⦃G1, L1⦄ ⊢ T1 ⁝ A1 → ∃A2. ⦃G2, L2⦄ ⊢ T2 ⁝ A2. -#h #G1 #G2 #L1 #L2 #T1 #T2 * -G2 -L2 -T2 -/3 width=6 by lfpx_aaa_conf, cpx_aaa_conf, aaa_fquq_conf, ex_intro/ +#h #o #G1 #G2 #L1 #L2 #T1 #T2 * -G2 -L2 -T2 +/3 width=8 by lfpx_aaa_conf, cpx_aaa_conf, aaa_ffdeq_conf, aaa_fquq_conf, ex_intro/ qed-. diff --git a/matita/matita/contribs/lambdadelta/basic_2/static/aaa_ffdeq.ma b/matita/matita/contribs/lambdadelta/basic_2/static/aaa_ffdeq.ma new file mode 100644 index 000000000..f9495e62d --- /dev/null +++ b/matita/matita/contribs/lambdadelta/basic_2/static/aaa_ffdeq.ma @@ -0,0 +1,25 @@ +(**************************************************************************) +(* ___ *) +(* ||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/static/ffdeq.ma". +include "basic_2/static/aaa_lfdeq.ma". + +(* ATONIC ARITY ASSIGNMENT ON TERMS *****************************************) + +(* Properties with degree-based equivalence on referred entries *************) + +lemma aaa_ffdeq_conf: ∀h,o,G1,G2,L1,L2,T1,T2. ⦃G1, L1, T1⦄ ≛[h, o] ⦃G2, L2, T2⦄ → + ∀A. ⦃G1, L1⦄ ⊢ T1 ⁝ A → ⦃G2, L2⦄ ⊢ T2 ⁝ A. +#h #o #G1 #G2 #L1 #L2 #T1 #T2 * -G2 -L2 -T2 +/2 width=7 by aaa_tdeq_conf_lfdeq/ qed-. 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 e71dbe35e..a01878128 100644 --- a/matita/matita/contribs/lambdadelta/basic_2/static/aaa_lfdeq.ma +++ b/matita/matita/contribs/lambdadelta/basic_2/static/aaa_lfdeq.ma @@ -19,7 +19,7 @@ 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 → +lemma aaa_tdeq_conf_lfdeq: ∀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 // diff --git a/matita/matita/contribs/lambdadelta/basic_2/static/ffdeq.ma b/matita/matita/contribs/lambdadelta/basic_2/static/ffdeq.ma index 7e4392488..ac4a6b169 100644 --- a/matita/matita/contribs/lambdadelta/basic_2/static/ffdeq.ma +++ b/matita/matita/contribs/lambdadelta/basic_2/static/ffdeq.ma @@ -18,21 +18,34 @@ 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 +inductive ffdeq (h) (o) (G) (L1) (T1): relation3 genv lenv term ≝ +| ffdeq_intro_sn: ∀L2,T2. L1 ≛[h, o, T1] L2 → T1 ≛[h, o] T2 → + ffdeq h o G L1 T1 G L2 T2 . interpretation "degree-based equivalence on referred entries (closure)" 'StarEqSn h o G1 L1 T1 G2 L2 T2 = (ffdeq h o G1 L1 T1 G2 L2 T2). +(* Basic_properties *********************************************************) + +lemma ffdeq_intro_dx (h) (o) (G): ∀L1,L2,T2. L1 ≛[h, o, T2] L2 → + ∀T1. T1 ≛[h, o] T2 → ⦃G, L1, T1⦄ ≛[h, o] ⦃G, L2, T2⦄. +/3 width=3 by ffdeq_intro_sn, tdeq_lfdeq_div/ 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_sn: ∀h,o,G1,G2,L1,L2,T1,T2. ⦃G1, L1, T1⦄ ≛[h, o] ⦃G2, L2, T2⦄ → + ∧∧ G1 = G2 & L1 ≛[h, o, T1] L2 & T1 ≛[h, o] T2. #h #o #G1 #G2 #L1 #L2 #T1 #T2 * -G2 -L2 -T2 /2 width=1 by and3_intro/ qed-. +lemma ffdeq_inv_gen_dx: ∀h,o,G1,G2,L1,L2,T1,T2. ⦃G1, L1, T1⦄ ≛[h, o] ⦃G2, L2, T2⦄ → + ∧∧ G1 = G2 & L1 ≛[h, o, T2] L2 & T1 ≛[h, o] T2. +#h #o #G1 #G2 #L1 #L2 #T1 #T2 * -G2 -L2 -T2 +/3 width=3 by tdeq_lfdeq_conf, and3_intro/ +qed-. + (* Basic_2A1: removed theorems 6: fleq_refl fleq_sym fleq_inv_gen fleq_trans fleq_canc_sn fleq_canc_dx 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 101463609..40a805259 100644 --- a/matita/matita/contribs/lambdadelta/basic_2/static/ffdeq_ffdeq.ma +++ b/matita/matita/contribs/lambdadelta/basic_2/static/ffdeq_ffdeq.ma @@ -20,14 +20,16 @@ include "basic_2/static/ffdeq.ma". (* Advanced properties ******************************************************) lemma ffdeq_sym: ∀h,o. tri_symmetric … (ffdeq h o). -#h #o #G1 #G2 #L1 #L2 #T1 #T2 * -G1 -L1 -T1 /3 width=1 by ffdeq_intro, lfdeq_sym/ +#h #o #G1 #G2 #L1 #L2 #T1 #T2 * -G1 -L1 -T1 +/3 width=1 by ffdeq_intro_dx, lfdeq_sym, tdeq_sym/ qed-. (* Main properties **********************************************************) theorem ffdeq_trans: ∀h,o. tri_transitive … (ffdeq h o). #h #o #G1 #G #L1 #L #T1 #T * -G -L -T -#L #HL1 #G2 #L2 #T2 * -G2 -L2 -T2 /3 width=3 by ffdeq_intro, lfdeq_trans/ +#L #T #HL1 #HT1 #G2 #L2 #T2 * -G2 -L2 -T2 +/4 width=5 by ffdeq_intro_sn, lfdeq_trans, tdeq_lfdeq_div, tdeq_trans/ qed-. theorem ffdeq_canc_sn: ∀h,o,G,G1,G2,L,L1,L2,T,T1,T2. diff --git a/matita/matita/contribs/lambdadelta/basic_2/static/ffdeq_fqup.ma b/matita/matita/contribs/lambdadelta/basic_2/static/ffdeq_fqup.ma index ab06d6d90..5d1288abb 100644 --- a/matita/matita/contribs/lambdadelta/basic_2/static/ffdeq_fqup.ma +++ b/matita/matita/contribs/lambdadelta/basic_2/static/ffdeq_fqup.ma @@ -20,4 +20,4 @@ include "basic_2/static/ffdeq.ma". (* Advanced properties ******************************************************) lemma ffdeq_refl: ∀h,o. tri_reflexive … (ffdeq h o). -/2 width=1 by ffdeq_intro/ qed. +/2 width=1 by ffdeq_intro_sn/ qed. diff --git a/matita/matita/contribs/lambdadelta/basic_2/static/lfdeq.ma b/matita/matita/contribs/lambdadelta/basic_2/static/lfdeq.ma index 3963c91bd..14994967a 100644 --- a/matita/matita/contribs/lambdadelta/basic_2/static/lfdeq.ma +++ b/matita/matita/contribs/lambdadelta/basic_2/static/lfdeq.ma @@ -73,11 +73,15 @@ lemma frees_lfdeq_conf: ∀h,o,f,L1,T. L1 ⊢ 𝐅*⦃T⦄ ≡ f → ∀L2. L1 ≛[h, o, f] L2 → L2 ⊢ 𝐅*⦃T⦄ ≡ f. /2 width=7 by frees_tdeq_conf_lfdeq, tdeq_refl/ qed-. -lemma tdeq_lfdeq_conf_sn: ∀h,o. s_r_confluent1 … (cdeq h o) (lfdeq h o). +lemma tdeq_lfdeq_conf: ∀h,o. s_r_confluent1 … (cdeq h o) (lfdeq h o). #h #o #L1 #T1 #T2 #HT12 #L2 * /3 width=5 by frees_tdeq_conf, ex2_intro/ qed-. +lemma tdeq_lfdeq_div: ∀h,o,T1,T2. T1 ≛[h, o] T2 → + ∀L1,L2. L1 ≛[h, o, T2] L2 → L1 ≛[h, o, T1] L2. +/3 width=3 by tdeq_lfdeq_conf, tdeq_sym/ qed-. + lemma lfdeq_atom: ∀h,o,I. ⋆ ≛[h, o, ⓪{I}] ⋆. /2 width=1 by lfxs_atom/ 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 9d4c4a67b..f78c3e8eb 100644 --- a/matita/matita/contribs/lambdadelta/basic_2/static/lfdeq_fqus.ma +++ b/matita/matita/contribs/lambdadelta/basic_2/static/lfdeq_fqus.ma @@ -60,7 +60,7 @@ lemma lfdeq_fqu_trans: ∀h,o,b,G1,G2,L2,K2,T,U. ⦃G1, L2, T⦄ ⊐[b] ⦃G2, K #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 - /3 width=7 by tdeq_lfdeq_conf_sn, fqu_lref_O, ex3_2_intro/ + /3 width=7 by tdeq_lfdeq_conf, fqu_lref_O, ex3_2_intro/ | * [ #p ] #I #G #L2 #V #T #L1 #H [ elim (lfdeq_inv_bind … H) | elim (lfdeq_inv_flat … H) @@ -100,7 +100,7 @@ lemma lfdeq_fqup_trans: ∀h,o,b,G1,G2,L2,K2,T,U. ⦃G1, L2, T⦄ ⊐+[b] ⦃G2, elim (lfdeq_fqu_trans … HU2 … HK0) -K #K1 #U1 #HU1 #HU12 #HK12 elim (tdeq_fqu_trans … HU1 … HU0) -U #K3 #U3 #HU03 #HU31 #HK31 @(ex3_2_intro … K3 U3) (**) (* full auto too slow *) - /3 width=5 by lfdeq_trans, tdeq_lfdeq_conf_sn, fqup_strap1, tdeq_trans/ + /3 width=5 by lfdeq_trans, tdeq_lfdeq_conf, fqup_strap1, tdeq_trans/ ] 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 40e94b86f..4da8d232f 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 @@ -107,7 +107,7 @@ table { ] *) [ { "uncounted context-sensitive parallel rt-computation" * } { - [ [ "refinement for lenvs" ] "lsubsx" + "( ? ⊢ ? ⊆ⓧ[?,?,?] ? )" "lsubsx_lfsx" + "lsubsx_lsubsx" * ] + [ [ "refinement for lenvs on selected entries" ] "lsubsx" + "( ? ⊢ ? ⊆ⓧ[?,?,?] ? )" "lsubsx_lfsx" + "lsubsx_lsubsx" * ] [ [ "strongly normalizing for lenvs on referred entries" ] "lfsx" + "( ? ⊢ ⬈*[?,?,?] 𝐒⦃?⦄ )" "lfsx_drops" + "lfsx_fqup" + "lfsx_cpx" + "lfsx_cpxs" + "lfsx_lfpxs" + "lfsx_lfsx" * ] [ [ "strongly normalizing for term vectors" ] "csx_vector" + "( ⦃?,?⦄ ⊢ ⬈*[?,?] 𝐒⦃?⦄ )" "csx_cnx_vector" + "csx_csx_vector" * ] [ [ "strongly normalizing for terms" ] "csx" + "( ⦃?,?⦄ ⊢ ⬈*[?,?] 𝐒⦃?⦄ )" "csx_simple" + "csx_simple_theq" + "csx_drops" + "csx_fqus" + "csx_lsubr" + "csx_lfdeq" + "csx_aaa" + "csx_gcp" + "csx_gcr" + "csx_lfpx" + "csx_cnx" + "csx_cpxs" + "csx_lfpxs" + "csx_csx" * ] @@ -122,8 +122,8 @@ table { class "cyan" [ { "rt-transition" * } { [ { "uncounted parallel rst-transition" * } { - [ [ "for closures" ] "fpbq" + "( ⦃?,?,?⦄ ≽[?] ⦃?,?,?⦄ )" "fpbq_aaa" * ] - [ [ "proper for closures" ] "fpb" + "( ⦃?,?,?⦄ ≻[?] ⦃?,?,?⦄ )" "fpb_lfdeq" * ] + [ [ "for closures" ] "fpbq" + "( ⦃?,?,?⦄ ≽[?,?] ⦃?,?,?⦄ )" "fpbq_aaa" * ] + [ [ "proper for closures" ] "fpb" + "( ⦃?,?,?⦄ ≻[?,?] ⦃?,?,?⦄ )" "fpb_lfdeq" * ] } ] [ { "context-sensitive parallel r-transition" * } { @@ -168,7 +168,7 @@ table { ] [ { "atomic arity assignment" * } { [ [ "restricted refinement for lenvs" ] "lsuba" + "( ? ⊢ ? ⫃⁝ ? )" "lsuba_drops" + "lsuba_lsubr" + "lsuba_aaa" + "lsuba_lsuba" * ] - [ [ "for terms" ] "aaa" + "( ⦃?,?⦄ ⊢ ? ⁝ ? )" "aaa_drops" + "aaa_fqus" + "aaa_lfdeq" + "aaa_aaa" * ] + [ [ "for terms" ] "aaa" + "( ⦃?,?⦄ ⊢ ? ⁝ ? )" "aaa_drops" + "aaa_fqus" + "aaa_lfdeq" + "aaa_ffdeq" + "aaa_aaa" * ] } ] [ { "degree-based equivalence" * } { @@ -177,7 +177,7 @@ table { } ] [ { "syntactic equivalence" * } { - [ [ "for lenvs on referred entries" ] "lfeq" + "( ? ≡[?] ? )" "lfeq_fqup" + "lfeq_fsle" * ] + [ [ "for lenvs on referred entries" ] "lfeq" + "( ? ≐[?] ? )" "lfeq_fqup" + "lfeq_fsle" * ] } ] [ { "generic extension of a context-sensitive relation" * } { @@ -227,7 +227,7 @@ table { } ] [ { "syntactic equivalence" * } { - [ [ "for lenvs on selected entries" ] "lreq" + "( ? ≡[?] ? )" "lreq_length" + "lreq_lreq" * ] + [ [ "for lenvs on selected entries" ] "lreq" + "( ? ≐[?] ? )" "lreq_length" + "lreq_lreq" * ] } ] [ { "generic entrywise extension" * } {