From 5ad776e509cd35fa003292e8bf2ed8f31d2c0a4b Mon Sep 17 00:00:00 2001 From: Ferruccio Guidi Date: Fri, 28 Apr 2017 10:52:19 +0000 Subject: [PATCH] refactoring completed --- .../contribs/lambdadelta/basic_2/i_static/tc_lfxs.ma | 1 + .../lambdadelta/basic_2/relocation/drops_lstar.ma | 1 + .../contribs/lambdadelta/basic_2/rt_computation/cpxs.ma | 1 + .../contribs/lambdadelta/basic_2/s_computation/fqup.ma | 1 + .../contribs/lambdadelta/basic_2/s_computation/fqus.ma | 1 + .../contribs/lambdadelta/ground_2/lib/relations.ma | 9 +++++++++ matita/matita/contribs/lambdadelta/ground_2/lib/star.ma | 7 ------- 7 files changed, 14 insertions(+), 7 deletions(-) diff --git a/matita/matita/contribs/lambdadelta/basic_2/i_static/tc_lfxs.ma b/matita/matita/contribs/lambdadelta/basic_2/i_static/tc_lfxs.ma index 54fdb7119..b8976cbd9 100644 --- a/matita/matita/contribs/lambdadelta/basic_2/i_static/tc_lfxs.ma +++ b/matita/matita/contribs/lambdadelta/basic_2/i_static/tc_lfxs.ma @@ -12,6 +12,7 @@ (* *) (**************************************************************************) +include "ground_2/lib/star.ma". include "basic_2/notation/relations/relationstarstar_4.ma". include "basic_2/static/lfxs.ma". diff --git a/matita/matita/contribs/lambdadelta/basic_2/relocation/drops_lstar.ma b/matita/matita/contribs/lambdadelta/basic_2/relocation/drops_lstar.ma index b3785339f..1c109075a 100644 --- a/matita/matita/contribs/lambdadelta/basic_2/relocation/drops_lstar.ma +++ b/matita/matita/contribs/lambdadelta/basic_2/relocation/drops_lstar.ma @@ -12,6 +12,7 @@ (* *) (**************************************************************************) +include "ground_2/lib/star.ma". include "ground_2/lib/lstar.ma". include "basic_2/relocation/lreq_lreq.ma". 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 e13e044c3..f1bb3e025 100644 --- a/matita/matita/contribs/lambdadelta/basic_2/rt_computation/cpxs.ma +++ b/matita/matita/contribs/lambdadelta/basic_2/rt_computation/cpxs.ma @@ -12,6 +12,7 @@ (* *) (**************************************************************************) +include "ground_2/lib/star.ma". include "basic_2/notation/relations/predtystar_5.ma". include "basic_2/rt_transition/cpx.ma". diff --git a/matita/matita/contribs/lambdadelta/basic_2/s_computation/fqup.ma b/matita/matita/contribs/lambdadelta/basic_2/s_computation/fqup.ma index 808164b69..e7ce5449c 100644 --- a/matita/matita/contribs/lambdadelta/basic_2/s_computation/fqup.ma +++ b/matita/matita/contribs/lambdadelta/basic_2/s_computation/fqup.ma @@ -12,6 +12,7 @@ (* *) (**************************************************************************) +include "ground_2/lib/star.ma". include "basic_2/notation/relations/suptermplus_6.ma". include "basic_2/s_transition/fqu.ma". diff --git a/matita/matita/contribs/lambdadelta/basic_2/s_computation/fqus.ma b/matita/matita/contribs/lambdadelta/basic_2/s_computation/fqus.ma index 8f37fd071..3fa8e4a65 100644 --- a/matita/matita/contribs/lambdadelta/basic_2/s_computation/fqus.ma +++ b/matita/matita/contribs/lambdadelta/basic_2/s_computation/fqus.ma @@ -12,6 +12,7 @@ (* *) (**************************************************************************) +include "ground_2/lib/star.ma". include "basic_2/notation/relations/suptermstar_6.ma". include "basic_2/s_transition/fquq.ma". diff --git a/matita/matita/contribs/lambdadelta/ground_2/lib/relations.ma b/matita/matita/contribs/lambdadelta/ground_2/lib/relations.ma index 3f5c3b409..e62b1fcda 100644 --- a/matita/matita/contribs/lambdadelta/ground_2/lib/relations.ma +++ b/matita/matita/contribs/lambdadelta/ground_2/lib/relations.ma @@ -94,3 +94,12 @@ lemma NF_to_SN_sn: ∀A,R,S,a. NF_sn A R S a → SN_sn A R S a. @SN_sn_intro #a1 #HRa12 #HSa12 elim HSa12 -HSa12 /2 width=1 by/ qed. + +(* Relations on unboxed triples *********************************************) + +definition tri_RC: ∀A,B,C. tri_relation A B C → tri_relation A B C ≝ + λA,B,C,R,a1,b1,c1,a2,b2,c2. R … a1 b1 c1 a2 b2 c2 ∨ + ∧∧ a1 = a2 & b1 = b2 & c1 = c2. + +lemma tri_RC_reflexive: ∀A,B,C,R. tri_reflexive A B C (tri_RC … R). +/3 width=1 by and3_intro, or_intror/ qed. diff --git a/matita/matita/contribs/lambdadelta/ground_2/lib/star.ma b/matita/matita/contribs/lambdadelta/ground_2/lib/star.ma index fdf2ae5a4..cc8a4318c 100644 --- a/matita/matita/contribs/lambdadelta/ground_2/lib/star.ma +++ b/matita/matita/contribs/lambdadelta/ground_2/lib/star.ma @@ -192,13 +192,6 @@ qed-. (* Relations on unboxed triples *********************************************) -definition tri_RC: ∀A,B,C. tri_relation A B C → tri_relation A B C ≝ - λA,B,C,R,a1,b1,c1,a2,b2,c2. R … a1 b1 c1 a2 b2 c2 ∨ - ∧∧ a1 = a2 & b1 = b2 & c1 = c2. - -lemma tri_RC_reflexive: ∀A,B,C,R. tri_reflexive A B C (tri_RC … R). -/3 width=1 by and3_intro, or_intror/ qed. - definition tri_star: ∀A,B,C,R. tri_relation A B C ≝ λA,B,C,R. tri_RC A B C (tri_TC … R). -- 2.39.2