From fed8c1a61273b0eb4a719fda70e2b5dd31933c8a Mon Sep 17 00:00:00 2001 From: Ferruccio Guidi Date: Sun, 16 Apr 2017 13:42:16 +0000 Subject: [PATCH] - strong normalization for rt-comutation - advances on lfpxs ... --- .../basic_2/i_static/tc_lfxs_tc_lfxs.ma | 23 +++++++++++++++++++ .../csx_aaa.etc => rt_computation/csx_aaa.ma} | 0 .../basic_2/rt_computation/lfpxs_lfpxs.ma | 4 ++-- .../basic_2/rt_computation/partial.txt | 2 +- .../lambdadelta/basic_2/web/basic_2.ldw.xml | 5 ++++ .../lambdadelta/basic_2/web/basic_2_src.tbl | 4 ++-- 6 files changed, 33 insertions(+), 5 deletions(-) create mode 100644 matita/matita/contribs/lambdadelta/basic_2/i_static/tc_lfxs_tc_lfxs.ma rename matita/matita/contribs/lambdadelta/basic_2/{etc/csx_aaa.etc => rt_computation/csx_aaa.ma} (100%) diff --git a/matita/matita/contribs/lambdadelta/basic_2/i_static/tc_lfxs_tc_lfxs.ma b/matita/matita/contribs/lambdadelta/basic_2/i_static/tc_lfxs_tc_lfxs.ma new file mode 100644 index 000000000..4fe37f452 --- /dev/null +++ b/matita/matita/contribs/lambdadelta/basic_2/i_static/tc_lfxs_tc_lfxs.ma @@ -0,0 +1,23 @@ +(**************************************************************************) +(* ___ *) +(* ||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/i_static/tc_lfxs.ma". + +(* ITERATED EXTENSION ON REFERRED ENTRIES OF A CONTEXT-SENSITIVE REALTION ***) + +(* Main properties **********************************************************) + +theorem tc_lfxs_trans: ∀R,T. Transitive … (tc_lfxs R T). +#R #T #L1 #L #HL1 #L2 #HL2 @(trans_TC … HL1 HL2) (**) (* auto fails *) +qed-. diff --git a/matita/matita/contribs/lambdadelta/basic_2/etc/csx_aaa.etc b/matita/matita/contribs/lambdadelta/basic_2/rt_computation/csx_aaa.ma similarity index 100% rename from matita/matita/contribs/lambdadelta/basic_2/etc/csx_aaa.etc rename to matita/matita/contribs/lambdadelta/basic_2/rt_computation/csx_aaa.ma diff --git a/matita/matita/contribs/lambdadelta/basic_2/rt_computation/lfpxs_lfpxs.ma b/matita/matita/contribs/lambdadelta/basic_2/rt_computation/lfpxs_lfpxs.ma index e2a5ee4d9..09d004b2c 100644 --- a/matita/matita/contribs/lambdadelta/basic_2/rt_computation/lfpxs_lfpxs.ma +++ b/matita/matita/contribs/lambdadelta/basic_2/rt_computation/lfpxs_lfpxs.ma @@ -12,6 +12,7 @@ (* *) (**************************************************************************) +include "basic_2/i_static/tc_lfxs_tc_lfxs.ma". include "basic_2/rt_computation/lfpxs.ma". (* UNCOUNTED PARALLEL RT-COMPUTATION FOR LOCAL ENV.S ON REFERRED ENTRIES ****) @@ -20,5 +21,4 @@ include "basic_2/rt_computation/lfpxs.ma". (* Basic_2A1: uses: lpxs_trans *) theorem lfpxs_trans: ∀h,G,T. Transitive … (lfpxs h G T). -#h #G #T #L1 #L #HL1 #L2 #HL2 @(trans_TC … HL1 HL2) (**) (* auto fails *) -qed-. +/2 width=3 by tc_lfxs_trans/ qed-. diff --git a/matita/matita/contribs/lambdadelta/basic_2/rt_computation/partial.txt b/matita/matita/contribs/lambdadelta/basic_2/rt_computation/partial.txt index 16ff258d1..876994e66 100644 --- a/matita/matita/contribs/lambdadelta/basic_2/rt_computation/partial.txt +++ b/matita/matita/contribs/lambdadelta/basic_2/rt_computation/partial.txt @@ -1,5 +1,5 @@ cpxs.ma cpxs_tdeq.ma cpxs_theq.ma cpxs_theq_vector.ma cpxs_drops.ma cpxs_lsubr.ma cpxs_aaa.ma cpxs_lfpx.ma cpxs_cnx.ma cpxs_cpxs.ma lfpxs.ma lfpxs_length.ma lfpxs_fqup.ma lfpxs_lfdeq.ma lfpxs_cpxs.ma lfpxs_lfpxs.ma -csx.ma csx_simple.ma csx_simple_theq.ma csx_drops.ma csx_lsubr.ma csx_gcp.ma csx_gcr.ma csx_lfpx.ma csx_cnx.ma csx_cpxs.ma csx_csx.ma +csx.ma csx_simple.ma csx_simple_theq.ma csx_drops.ma csx_lsubr.ma csx_aaa.ma csx_gcp.ma csx_gcr.ma csx_lfpx.ma csx_cnx.ma csx_cpxs.ma csx_csx.ma csx_vector.ma csx_cnx_vector.ma csx_csx_vector.ma lfsx.ma lfsx_fqup.ma lfsx_lfpxs.ma lfsx_lfsx.ma diff --git a/matita/matita/contribs/lambdadelta/basic_2/web/basic_2.ldw.xml b/matita/matita/contribs/lambdadelta/basic_2/web/basic_2.ldw.xml index f55e45f41..a11a40126 100644 --- a/matita/matita/contribs/lambdadelta/basic_2/web/basic_2.ldw.xml +++ b/matita/matita/contribs/lambdadelta/basic_2/web/basic_2.ldw.xml @@ -34,6 +34,11 @@ Stage "A2": "Extending the Applicability Condition" + + Strong rt-normalization + for simply typed terms + (anniversary milestone). + First behavioral component reconstructed: rt_transition. 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 bf098d4a9..db3bcf966 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 @@ -115,7 +115,7 @@ table { *) [ "lfsx ( ? ⊢ ⬈*[?,?,?] 𝐒⦃?⦄ )" "lfsx_fqup" + "lfsx_lfpxs" + "lfsx_lfsx" * ] [ "csx_vector ( ⦃?,?⦄ ⊢ ⬈*[?,?] 𝐒⦃?⦄ )" "csx_cnx_vector" + "csx_csx_vector" * ] - [ "csx ( ⦃?,?⦄ ⊢ ⬈*[?,?] 𝐒⦃?⦄ )" "csx_simple" + "csx_simple_theq" + "csx_drops" + "csx_lsubr" + "csx_gcp" + "csx_gcr" + "csx_lfpx" + "csx_cnx" + "csx_cpxs" + "csx_csx" * ] + [ "csx ( ⦃?,?⦄ ⊢ ⬈*[?,?] 𝐒⦃?⦄ )" "csx_simple" + "csx_simple_theq" + "csx_drops" + "csx_lsubr" + "csx_aaa" + "csx_gcp" + "csx_gcr" + "csx_lfpx" + "csx_cnx" + "csx_cpxs" + "csx_csx" * ] [ "lfpxs ( ⦃?,?⦄ ⊢ ⬈*[?,?] ? )" "lfpxs_length" + "lfpxs_fqup" + "lfpxs_lfdeq" + "lfpxs_cpxs" + "lfpxs_lfpxs" * ] [ "cpxs ( ⦃?,?⦄ ⊢ ? ⬈*[?] ? )" "cpxs_tdeq" + "cpxs_theq" + "cpxs_theq_vector" + "cpxs_drops" + "cpxs_lsubr" + "cpxs_aaa" + "cpxs_lfpx" + "cpxs_cnx" + "cpxs_cpxs" * ] } @@ -150,7 +150,7 @@ table { class "water" [ { "iterated static typing" * } { [ { "iterated extension on referred entries" * } { - [ "tc_lfxs ( ? ⦻**[?,?] ? )" "tc_lfxs_length" + "tc_lfxs_fqup" * ] + [ "tc_lfxs ( ? ⦻**[?,?] ? )" "tc_lfxs_length" + "tc_lfxs_fqup" + "tc_lfxs_tc_lfxs" * ] } ] } -- 2.39.2