From: Ferruccio Guidi Date: Fri, 31 Jan 2014 15:03:31 +0000 (+0000) Subject: some notation renamed and fixed X-Git-Tag: make_still_working~982 X-Git-Url: http://matita.cs.unibo.it/gitweb/?a=commitdiff_plain;h=1f30483032488ac4df2310b68fe8146e05524fec;p=helm.git some notation renamed and fixed --- diff --git a/matita/matita/contribs/lambdadelta/basic_2/computation/cpre.ma b/matita/matita/contribs/lambdadelta/basic_2/computation/cpre.ma index 2e81a1a0a..6b998fb13 100644 --- a/matita/matita/contribs/lambdadelta/basic_2/computation/cpre.ma +++ b/matita/matita/contribs/lambdadelta/basic_2/computation/cpre.ma @@ -12,17 +12,17 @@ (* *) (**************************************************************************) -include "basic_2/notation/relations/peval_4.ma". +include "basic_2/notation/relations/predeval_4.ma". include "basic_2/computation/cprs.ma". include "basic_2/computation/csx.ma". -(* CONTEXT-SENSITIVE PARALLEL EVALUATION ON TERMS **************************) +(* EVALUATION FOR CONTEXT-SENSITIVE PARALLEL REDUCTION ON TERMS *************) definition cpre: relation4 genv lenv term term ≝ λG,L,T1,T2. ⦃G, L⦄ ⊢ T1 ➡* T2 ∧ ⦃G, L⦄ ⊢ ➡ 𝐍⦃T2⦄. -interpretation "context-sensitive parallel evaluation (term)" - 'PEval G L T1 T2 = (cpre G L T1 T2). +interpretation "evaluation for context-sensitive parallel reduction (term)" + 'PRedEval G L T1 T2 = (cpre G L T1 T2). (* Basic_properties *********************************************************) diff --git a/matita/matita/contribs/lambdadelta/basic_2/computation/cpre_cpre.ma b/matita/matita/contribs/lambdadelta/basic_2/computation/cpre_cpre.ma index 5d570c724..4fd418119 100644 --- a/matita/matita/contribs/lambdadelta/basic_2/computation/cpre_cpre.ma +++ b/matita/matita/contribs/lambdadelta/basic_2/computation/cpre_cpre.ma @@ -15,7 +15,7 @@ include "basic_2/computation/cprs_cprs.ma". include "basic_2/computation/cpre.ma". -(* CONTEXT-SENSITIVE PARALLEL EVALUATION ON TERMS **************************) +(* EVALUATION FOR CONTEXT-SENSITIVE PARALLEL REDUCTION ON TERMS *************) (* Main properties *********************************************************) diff --git a/matita/matita/contribs/lambdadelta/basic_2/computation/cpxe.ma b/matita/matita/contribs/lambdadelta/basic_2/computation/cpxe.ma index e2975c54a..b2e05f37e 100644 --- a/matita/matita/contribs/lambdadelta/basic_2/computation/cpxe.ma +++ b/matita/matita/contribs/lambdadelta/basic_2/computation/cpxe.ma @@ -12,17 +12,17 @@ (* *) (**************************************************************************) -include "basic_2/notation/relations/peval_6.ma". +include "basic_2/notation/relations/predeval_6.ma". include "basic_2/computation/cpxs.ma". include "basic_2/computation/csx.ma". -(* CONTEXT-SENSITIVE EXTENDED PARALLEL EVALUATION ON TERMS ******************) +(* EVALUATION FOR CONTEXT-SENSITIVE EXTENDED PARALLEL REDUCTION ON TERMS ****) definition cpxe: ∀h. sd h → relation4 genv lenv term term ≝ λh,g,G,L,T1,T2. ⦃G, L⦄ ⊢ T1 ➡*[h, g] T2 ∧ ⦃G, L⦄ ⊢ ➡[h, g] 𝐍⦃T2⦄. -interpretation "context-sensitive extended parallel evaluation (term)" - 'PEval h g G L T1 T2 = (cpxe h g G L T1 T2). +interpretation "evaluation for context-sensitive extended parallel reduction (term)" + 'PRedEval h g G L T1 T2 = (cpxe h g G L T1 T2). (* Basic_properties *********************************************************) diff --git a/matita/matita/contribs/lambdadelta/basic_2/computation/lpxs_lleq.ma b/matita/matita/contribs/lambdadelta/basic_2/computation/lpxs_lleq.ma index a78d6c70d..522d36f97 100644 --- a/matita/matita/contribs/lambdadelta/basic_2/computation/lpxs_lleq.ma +++ b/matita/matita/contribs/lambdadelta/basic_2/computation/lpxs_lleq.ma @@ -25,21 +25,21 @@ fact le_repl_sn_aux: ∀x,y,z:nat. x ≤ z → x = y → y ≤ z. axiom cpxs_cpys_conf_lpxs: ∀h,g,G,d,e. ∀L0,T0,T1. ⦃G, L0⦄ ⊢ T0 ➡*[h, g] T1 → - ∀T2. ⦃G, L0⦄ ⊢ T0 ▶*×[d, e] T2 → + ∀T2. ⦃G, L0⦄ ⊢ T0 ▶*[d, e] T2 → ∀L1. ⦃G, L0⦄ ⊢ ➡*[h, g] L1 → - ∃∃T. ⦃G, L1⦄ ⊢ T1 ▶*×[d, e] T & ⦃G, L0⦄ ⊢ T2 ➡*[h, g] T. + ∃∃T. ⦃G, L1⦄ ⊢ T1 ▶*[d, e] T & ⦃G, L0⦄ ⊢ T2 ➡*[h, g] T. axiom cpxs_conf_lpxs_lpys: ∀h,g,G,d,e. ∀I,L0,V0,T0,T1. ⦃G, L0.ⓑ{I}V0⦄ ⊢ T0 ➡*[h, g] T1 → - ∀L1. ⦃G, L0⦄ ⊢ ➡*[h, g] L1 → ∀V2. ⦃G, L0⦄ ⊢ V0 ▶*×[d, e] V2 → - ∃∃T. ⦃G, L1.ⓑ{I}V0⦄ ⊢ T1 ▶*×[⫯d, e] T & ⦃G, L0.ⓑ{I}V2⦄ ⊢ T0 ➡*[h, g] T. + ∀L1. ⦃G, L0⦄ ⊢ ➡*[h, g] L1 → ∀V2. ⦃G, L0⦄ ⊢ V0 ▶*[d, e] V2 → + ∃∃T. ⦃G, L1.ⓑ{I}V0⦄ ⊢ T1 ▶*[⫯d, e] T & ⦃G, L0.ⓑ{I}V2⦄ ⊢ T0 ➡*[h, g] T. include "basic_2/reduction/cpx_cpys.ma". -fact pippo_aux: ∀h,g,G,L1,T,T1,d,e. ⦃G, L1⦄ ⊢ T ▶*×[d, e] T1 → e = ∞ → +fact pippo_aux: ∀h,g,G,L1,T,T1,d,e. ⦃G, L1⦄ ⊢ T ▶*[d, e] T1 → e = ∞ → ∀L2. ⦃G, L1⦄ ⊢ ➡*[h, g] L2 → - ∃∃T2. ⦃G, L2⦄ ⊢ T ▶*×[d, e] T2 & ⦃G, L1⦄ ⊢ T1 ➡*[h, g] T2 & + ∃∃T2. ⦃G, L2⦄ ⊢ T ▶*[d, e] T2 & ⦃G, L1⦄ ⊢ T1 ➡*[h, g] T2 & L1 ⋕[T, d] L2 ↔ T1 = T2. #h #g #G #L1 #T #T1 #d #e #H @(cpys_ind_alt … H) -G -L1 -T -T1 -d -e [ * ] [ /5 width=5 by lpxs_fwd_length, lleq_sort, ex3_intro, conj/ diff --git a/matita/matita/contribs/lambdadelta/basic_2/notation/relations/extpsubst_6.ma b/matita/matita/contribs/lambdadelta/basic_2/notation/relations/extpsubst_6.ma deleted file mode 100644 index 9dde8aa0f..000000000 --- a/matita/matita/contribs/lambdadelta/basic_2/notation/relations/extpsubst_6.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 G , break term 46 L ⦄ ⊢ break term 46 T1 break ▶ × [ term 46 d , break term 46 e ] break term 46 T2 )" - non associative with precedence 45 - for @{ 'ExtPSubst $G $L $T1 $d $e $T2 }. diff --git a/matita/matita/contribs/lambdadelta/basic_2/notation/relations/extpsubststar_6.ma b/matita/matita/contribs/lambdadelta/basic_2/notation/relations/extpsubststar_6.ma deleted file mode 100644 index bd89b8d85..000000000 --- a/matita/matita/contribs/lambdadelta/basic_2/notation/relations/extpsubststar_6.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 G , break term 46 L ⦄ ⊢ break term 46 T1 break ▶ * × [ term 46 d , break term 46 e ] break term 46 T2 )" - non associative with precedence 45 - for @{ 'ExtPSubstStar $G $L $T1 $d $e $T2 }. diff --git a/matita/matita/contribs/lambdadelta/basic_2/notation/relations/extpsubststaralt_6.ma b/matita/matita/contribs/lambdadelta/basic_2/notation/relations/extpsubststaralt_6.ma deleted file mode 100644 index d74b372e8..000000000 --- a/matita/matita/contribs/lambdadelta/basic_2/notation/relations/extpsubststaralt_6.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 G , break term 46 L ⦄ ⊢ break term 46 T1 break ▶ ▶ * × [ term 46 d , break term 46 e ] break term 46 T2 )" - non associative with precedence 45 - for @{ 'ExtPSubstStarAlt $G $L $T1 $d $e $T2 }. diff --git a/matita/matita/contribs/lambdadelta/basic_2/notation/relations/normal_3.ma b/matita/matita/contribs/lambdadelta/basic_2/notation/relations/normal_3.ma deleted file mode 100644 index e94aea008..000000000 --- a/matita/matita/contribs/lambdadelta/basic_2/notation/relations/normal_3.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 G , break term 46 L ⦄ ⊢ ➡ 𝐍 break ⦃ term 46 T ⦄ )" - non associative with precedence 45 - for @{ 'Normal $G $L $T }. diff --git a/matita/matita/contribs/lambdadelta/basic_2/notation/relations/normal_5.ma b/matita/matita/contribs/lambdadelta/basic_2/notation/relations/normal_5.ma deleted file mode 100644 index 20844ce63..000000000 --- a/matita/matita/contribs/lambdadelta/basic_2/notation/relations/normal_5.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 G, break term 46 L ⦄ ⊢ ➡ break [ term 46 h , break term 46 g ] 𝐍 break ⦃ term 46 T ⦄ )" - non associative with precedence 45 - for @{ 'Normal $h $g $G $L $T }. diff --git a/matita/matita/contribs/lambdadelta/basic_2/notation/relations/notreducible_3.ma b/matita/matita/contribs/lambdadelta/basic_2/notation/relations/notreducible_3.ma deleted file mode 100644 index 4cebc3027..000000000 --- a/matita/matita/contribs/lambdadelta/basic_2/notation/relations/notreducible_3.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 G , break term 46 L ⦄ ⊢ ➡ 𝐈 break ⦃ term 46 T ⦄ )" - non associative with precedence 45 - for @{ 'NotReducible $G $L $T }. diff --git a/matita/matita/contribs/lambdadelta/basic_2/notation/relations/notreducible_5.ma b/matita/matita/contribs/lambdadelta/basic_2/notation/relations/notreducible_5.ma deleted file mode 100644 index 4a4e3f3a9..000000000 --- a/matita/matita/contribs/lambdadelta/basic_2/notation/relations/notreducible_5.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 G, break term 46 L ⦄ ⊢ ➡ break [ term 46 h , break term 46 g ] 𝐈 break ⦃ term 46 T ⦄ )" - non associative with precedence 45 - for @{ 'NotReducible $h $g $G $L $T }. diff --git a/matita/matita/contribs/lambdadelta/basic_2/notation/relations/peval_4.ma b/matita/matita/contribs/lambdadelta/basic_2/notation/relations/peval_4.ma deleted file mode 100644 index 558ce7d05..000000000 --- a/matita/matita/contribs/lambdadelta/basic_2/notation/relations/peval_4.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 G, break term 46 L ⦄ ⊢ break term 46 T1 ➡ * break 𝐍 ⦃ term 46 T2 ⦄ )" - non associative with precedence 45 - for @{ 'PEval $G $L $T1 $T2 }. diff --git a/matita/matita/contribs/lambdadelta/basic_2/notation/relations/peval_6.ma b/matita/matita/contribs/lambdadelta/basic_2/notation/relations/peval_6.ma deleted file mode 100644 index aa2a6c499..000000000 --- a/matita/matita/contribs/lambdadelta/basic_2/notation/relations/peval_6.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 G, break term 46 L ⦄ ⊢ break term 46 T1 ➡ * break [ term 46 h , break term 46 g ] break 𝐍 ⦃ term 46 T2 ⦄ )" - non associative with precedence 45 - for @{ 'PEval $h $g $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 new file mode 100644 index 000000000..e26cfe6d3 --- /dev/null +++ b/matita/matita/contribs/lambdadelta/basic_2/notation/relations/predeval_4.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 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 new file mode 100644 index 000000000..8360d142a --- /dev/null +++ b/matita/matita/contribs/lambdadelta/basic_2/notation/relations/predeval_6.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 g ] break 𝐍 ⦃ term 46 T2 ⦄ )" + non associative with precedence 45 + for @{ 'PRedEval $h $g $G $L $T1 $T2 }. diff --git a/matita/matita/contribs/lambdadelta/basic_2/notation/relations/prednormal_3.ma b/matita/matita/contribs/lambdadelta/basic_2/notation/relations/prednormal_3.ma new file mode 100644 index 000000000..a8806a1c7 --- /dev/null +++ b/matita/matita/contribs/lambdadelta/basic_2/notation/relations/prednormal_3.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 T ⦄ )" + non associative with precedence 45 + for @{ 'PRedNormal $G $L $T }. diff --git a/matita/matita/contribs/lambdadelta/basic_2/notation/relations/prednormal_5.ma b/matita/matita/contribs/lambdadelta/basic_2/notation/relations/prednormal_5.ma new file mode 100644 index 000000000..d1e001d85 --- /dev/null +++ b/matita/matita/contribs/lambdadelta/basic_2/notation/relations/prednormal_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 g ] 𝐍 break ⦃ term 46 T ⦄ )" + non associative with precedence 45 + for @{ 'PRedNormal $h $g $G $L $T }. diff --git a/matita/matita/contribs/lambdadelta/basic_2/notation/relations/prednotreducible_3.ma b/matita/matita/contribs/lambdadelta/basic_2/notation/relations/prednotreducible_3.ma new file mode 100644 index 000000000..4ad7cbc72 --- /dev/null +++ b/matita/matita/contribs/lambdadelta/basic_2/notation/relations/prednotreducible_3.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 T ⦄ )" + non associative with precedence 45 + for @{ 'PRedNotReducible $G $L $T }. diff --git a/matita/matita/contribs/lambdadelta/basic_2/notation/relations/prednotreducible_5.ma b/matita/matita/contribs/lambdadelta/basic_2/notation/relations/prednotreducible_5.ma new file mode 100644 index 000000000..cb33d31e2 --- /dev/null +++ b/matita/matita/contribs/lambdadelta/basic_2/notation/relations/prednotreducible_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 g ] 𝐈 break ⦃ term 46 T ⦄ )" + non associative with precedence 45 + for @{ 'PRedNotReducible $h $g $G $L $T }. diff --git a/matita/matita/contribs/lambdadelta/basic_2/notation/relations/predreducible_3.ma b/matita/matita/contribs/lambdadelta/basic_2/notation/relations/predreducible_3.ma new file mode 100644 index 000000000..5d84a363d --- /dev/null +++ b/matita/matita/contribs/lambdadelta/basic_2/notation/relations/predreducible_3.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 T ⦄ )" + non associative with precedence 45 + for @{ 'PRedReducible $G $L $T }. diff --git a/matita/matita/contribs/lambdadelta/basic_2/notation/relations/predreducible_5.ma b/matita/matita/contribs/lambdadelta/basic_2/notation/relations/predreducible_5.ma new file mode 100644 index 000000000..82ded9c03 --- /dev/null +++ b/matita/matita/contribs/lambdadelta/basic_2/notation/relations/predreducible_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 g ] 𝐑 break ⦃ term 46 T ⦄ )" + non associative with precedence 45 + for @{ 'PRedReducible $h $g $G $L $T }. diff --git a/matita/matita/contribs/lambdadelta/basic_2/notation/relations/psubst_6.ma b/matita/matita/contribs/lambdadelta/basic_2/notation/relations/psubst_6.ma new file mode 100644 index 000000000..31fe21410 --- /dev/null +++ b/matita/matita/contribs/lambdadelta/basic_2/notation/relations/psubst_6.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 d , break term 46 e ] break term 46 T2 )" + non associative with precedence 45 + for @{ 'PSubst $G $L $T1 $d $e $T2 }. diff --git a/matita/matita/contribs/lambdadelta/basic_2/notation/relations/psubstnormal_5.ma b/matita/matita/contribs/lambdadelta/basic_2/notation/relations/psubstnormal_5.ma index ebe23f937..4a7a78afc 100644 --- a/matita/matita/contribs/lambdadelta/basic_2/notation/relations/psubstnormal_5.ma +++ b/matita/matita/contribs/lambdadelta/basic_2/notation/relations/psubstnormal_5.ma @@ -14,6 +14,6 @@ (* NOTATION FOR THE FORMAL SYSTEM λδ ****************************************) -notation "hvbox( ⦃ term 46 G, break term 46 L ⦄ ⊢ ▶ break [ term 46 d , break term 46 e ] 𝐍 break ⦃ term 46 T ⦄ )" +notation "hvbox( ⦃ term 46 G, break term 46 L ⦄ ⊢ ▶ break [ term 46 d , break term 46 e ] 𝐍 break ⦃ term 46 T ⦄ )" non associative with precedence 45 for @{ 'PSubstNormal $G $L $T $d $e }. diff --git a/matita/matita/contribs/lambdadelta/basic_2/notation/relations/psubststar_6.ma b/matita/matita/contribs/lambdadelta/basic_2/notation/relations/psubststar_6.ma new file mode 100644 index 000000000..f2bb4bd78 --- /dev/null +++ b/matita/matita/contribs/lambdadelta/basic_2/notation/relations/psubststar_6.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 d , break term 46 e ] break term 46 T2 )" + non associative with precedence 45 + for @{ 'PSubstStar $G $L $T1 $d $e $T2 }. diff --git a/matita/matita/contribs/lambdadelta/basic_2/notation/relations/psubststaralt_6.ma b/matita/matita/contribs/lambdadelta/basic_2/notation/relations/psubststaralt_6.ma new file mode 100644 index 000000000..e727d4945 --- /dev/null +++ b/matita/matita/contribs/lambdadelta/basic_2/notation/relations/psubststaralt_6.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 d , break term 46 e ] break term 46 T2 )" + non associative with precedence 45 + for @{ 'PSubstStarAlt $G $L $T1 $d $e $T2 }. diff --git a/matita/matita/contribs/lambdadelta/basic_2/notation/relations/reducible_3.ma b/matita/matita/contribs/lambdadelta/basic_2/notation/relations/reducible_3.ma deleted file mode 100644 index d1b688b8c..000000000 --- a/matita/matita/contribs/lambdadelta/basic_2/notation/relations/reducible_3.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 G , break term 46 L ⦄ ⊢ ➡ 𝐑 break ⦃ term 46 T ⦄ )" - non associative with precedence 45 - for @{ 'Reducible $G $L $T }. diff --git a/matita/matita/contribs/lambdadelta/basic_2/notation/relations/reducible_5.ma b/matita/matita/contribs/lambdadelta/basic_2/notation/relations/reducible_5.ma deleted file mode 100644 index c63231648..000000000 --- a/matita/matita/contribs/lambdadelta/basic_2/notation/relations/reducible_5.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 G, break term 46 L ⦄ ⊢ ➡ break [ term 46 h , break term 46 g ] 𝐑 break ⦃ term 46 T ⦄ )" - non associative with precedence 45 - for @{ 'Reducible $h $g $G $L $T }. diff --git a/matita/matita/contribs/lambdadelta/basic_2/reduction/cir.ma b/matita/matita/contribs/lambdadelta/basic_2/reduction/cir.ma index a8a5bcc9c..b315e29bc 100644 --- a/matita/matita/contribs/lambdadelta/basic_2/reduction/cir.ma +++ b/matita/matita/contribs/lambdadelta/basic_2/reduction/cir.ma @@ -12,15 +12,15 @@ (* *) (**************************************************************************) -include "basic_2/notation/relations/notreducible_3.ma". +include "basic_2/notation/relations/prednotreducible_3.ma". include "basic_2/reduction/crr.ma". -(* CONTEXT-SENSITIVE IRREDUCIBLE TERMS **************************************) +(* IRREDUCIBLE TERMS FOR CONTEXT-SENSITIVE REDUCTION ************************) definition cir: relation3 genv lenv term ≝ λG,L,T. ⦃G, L⦄ ⊢ ➡ 𝐑⦃T⦄ → ⊥. -interpretation "context-sensitive irreducibility (term)" - 'NotReducible G L T = (cir G L T). +interpretation "irreducibility for context-sensitive reduction (term)" + 'PRedNotReducible G L T = (cir G L T). (* Basic inversion lemmas ***************************************************) diff --git a/matita/matita/contribs/lambdadelta/basic_2/reduction/cir_append.ma b/matita/matita/contribs/lambdadelta/basic_2/reduction/cir_append.ma index 2f0461191..efd097f84 100644 --- a/matita/matita/contribs/lambdadelta/basic_2/reduction/cir_append.ma +++ b/matita/matita/contribs/lambdadelta/basic_2/reduction/cir_append.ma @@ -15,7 +15,7 @@ include "basic_2/reduction/crr_append.ma". include "basic_2/reduction/cir.ma". -(* CONTEXT-SENSITIVE IRREDUCIBLE TERMS **************************************) +(* IRREDUCIBLE TERMS FOR CONTEXT-SENSITIVE REDUCTION ************************) (* Advanved properties ******************************************************) diff --git a/matita/matita/contribs/lambdadelta/basic_2/reduction/cir_lift.ma b/matita/matita/contribs/lambdadelta/basic_2/reduction/cir_lift.ma index 0cea0de9c..b570745d9 100644 --- a/matita/matita/contribs/lambdadelta/basic_2/reduction/cir_lift.ma +++ b/matita/matita/contribs/lambdadelta/basic_2/reduction/cir_lift.ma @@ -15,7 +15,7 @@ include "basic_2/reduction/crr_lift.ma". include "basic_2/reduction/cir.ma". -(* CONTEXT-SENSITIVE IRREDUCIBLE TERMS **************************************) +(* IRREDUCIBLE TERMS FOR CONTEXT-SENSITIVE REDUCTION ************************) (* Properties on relocation *************************************************) diff --git a/matita/matita/contribs/lambdadelta/basic_2/reduction/cix.ma b/matita/matita/contribs/lambdadelta/basic_2/reduction/cix.ma index ad3c60831..61d14f011 100644 --- a/matita/matita/contribs/lambdadelta/basic_2/reduction/cix.ma +++ b/matita/matita/contribs/lambdadelta/basic_2/reduction/cix.ma @@ -12,17 +12,17 @@ (* *) (**************************************************************************) -include "basic_2/notation/relations/notreducible_5.ma". +include "basic_2/notation/relations/prednotreducible_5.ma". include "basic_2/reduction/cir.ma". include "basic_2/reduction/crx.ma". -(* CONTEXT-SENSITIVE EXTENDED IRREDUCIBLE TERMS *****************************) +(* IRREDUCIBLE TERMS FOR CONTEXT-SENSITIVE EXTENDED REDUCTION ***************) definition cix: ∀h. sd h → relation3 genv lenv term ≝ λh,g,G,L,T. ⦃G, L⦄ ⊢ ➡[h, g] 𝐑⦃T⦄ → ⊥. -interpretation "context-sensitive extended irreducibility (term)" - 'NotReducible h g G L T = (cix h g G L T). +interpretation "irreducibility for context-sensitive extended reduction (term)" + 'PRedNotReducible h g G L T = (cix h g G L T). (* Basic inversion lemmas ***************************************************) diff --git a/matita/matita/contribs/lambdadelta/basic_2/reduction/cix_append.ma b/matita/matita/contribs/lambdadelta/basic_2/reduction/cix_append.ma index ba1eb8b2a..7b5522ebd 100644 --- a/matita/matita/contribs/lambdadelta/basic_2/reduction/cix_append.ma +++ b/matita/matita/contribs/lambdadelta/basic_2/reduction/cix_append.ma @@ -15,7 +15,7 @@ include "basic_2/reduction/crx_append.ma". include "basic_2/reduction/cix.ma". -(* CONTEXT-SENSITIVE EXTENDED IRREDUCIBLE TERMS *****************************) +(* IRREDUCIBLE TERMS FOR CONTEXT-SENSITIVE EXTENDED REDUCTION ***************) (* Advanced inversion lemmas ************************************************) diff --git a/matita/matita/contribs/lambdadelta/basic_2/reduction/cix_lift.ma b/matita/matita/contribs/lambdadelta/basic_2/reduction/cix_lift.ma index 64a17731b..7a3d5e68b 100644 --- a/matita/matita/contribs/lambdadelta/basic_2/reduction/cix_lift.ma +++ b/matita/matita/contribs/lambdadelta/basic_2/reduction/cix_lift.ma @@ -15,7 +15,7 @@ include "basic_2/reduction/crx_lift.ma". include "basic_2/reduction/cix.ma". -(* CONTEXT-SENSITIVE EXTENDED IRREDUCIBLE TERMS *****************************) +(* IRREDUCIBLE TERMS FOR CONTEXT-SENSITIVE EXTENDED REDUCTION ***************) (* Advanced properties ******************************************************) diff --git a/matita/matita/contribs/lambdadelta/basic_2/reduction/cnr.ma b/matita/matita/contribs/lambdadelta/basic_2/reduction/cnr.ma index ad48736fa..e0e84742f 100644 --- a/matita/matita/contribs/lambdadelta/basic_2/reduction/cnr.ma +++ b/matita/matita/contribs/lambdadelta/basic_2/reduction/cnr.ma @@ -12,16 +12,16 @@ (* *) (**************************************************************************) -include "basic_2/notation/relations/normal_3.ma". +include "basic_2/notation/relations/prednormal_3.ma". include "basic_2/reduction/cpr.ma". -(* CONTEXT-SENSITIVE NORMAL TERMS *******************************************) +(* NORMAL TERMS FOR CONTEXT-SENSITIVE REDUCTION *****************************) definition cnr: relation3 genv lenv term ≝ λG,L. NF … (cpr G L) (eq …). interpretation - "context-sensitive normality (term)" - 'Normal G L T = (cnr G L T). + "normality for context-sensitive reduction (term)" + 'PRedNormal G L T = (cnr G L T). (* Basic inversion lemmas ***************************************************) diff --git a/matita/matita/contribs/lambdadelta/basic_2/reduction/cnr_cir.ma b/matita/matita/contribs/lambdadelta/basic_2/reduction/cnr_cir.ma index 7c596245f..480e359cb 100644 --- a/matita/matita/contribs/lambdadelta/basic_2/reduction/cnr_cir.ma +++ b/matita/matita/contribs/lambdadelta/basic_2/reduction/cnr_cir.ma @@ -15,14 +15,14 @@ include "basic_2/reduction/cpr_cir.ma". include "basic_2/reduction/cnr_crr.ma". -(* CONTEXT-SENSITIVE NORMAL TERMS *******************************************) +(* NORMAL TERMS FOR CONTEXT-SENSITIVE REDUCTION *****************************) -(* Main properties on context-sensitive irreducible terms *******************) +(* Main properties on irreducibility ****************************************) theorem cir_cnr: ∀G,L,T. ⦃G, L⦄ ⊢ ➡ 𝐈⦃T⦄ → ⦃G, L⦄ ⊢ ➡ 𝐍⦃T⦄. /2 width=4 by cpr_fwd_cir/ qed. -(* Main inversion lemmas on context-sensitive irreducible terms *************) +(* Main inversion lemmas on irreducibility **********************************) theorem cnr_inv_cir: ∀G,L,T. ⦃G, L⦄ ⊢ ➡ 𝐍⦃T⦄ → ⦃G, L⦄ ⊢ ➡ 𝐈⦃T⦄. /2 width=5 by cnr_inv_crr/ qed-. diff --git a/matita/matita/contribs/lambdadelta/basic_2/reduction/cnr_crr.ma b/matita/matita/contribs/lambdadelta/basic_2/reduction/cnr_crr.ma index c72c3315e..35937fb41 100644 --- a/matita/matita/contribs/lambdadelta/basic_2/reduction/cnr_crr.ma +++ b/matita/matita/contribs/lambdadelta/basic_2/reduction/cnr_crr.ma @@ -15,9 +15,9 @@ include "basic_2/reduction/crr.ma". include "basic_2/reduction/cnr.ma". -(* CONTEXT-SENSITIVE NORMAL TERMS *******************************************) +(* NORMAL TERMS FOR CONTEXT-SENSITIVE REDUCTION *****************************) -(* Advanced inversion lemmas on context-sensitive reducible terms ***********) +(* Advanced inversion lemmas on reducibility ********************************) (* Note: this property is unusual *) lemma cnr_inv_crr: ∀G,L,T. ⦃G, L⦄ ⊢ ➡ 𝐑⦃T⦄ → ⦃G, L⦄ ⊢ ➡ 𝐍⦃T⦄ → ⊥. diff --git a/matita/matita/contribs/lambdadelta/basic_2/reduction/cnr_lift.ma b/matita/matita/contribs/lambdadelta/basic_2/reduction/cnr_lift.ma index 217646acf..83def4723 100644 --- a/matita/matita/contribs/lambdadelta/basic_2/reduction/cnr_lift.ma +++ b/matita/matita/contribs/lambdadelta/basic_2/reduction/cnr_lift.ma @@ -15,7 +15,7 @@ include "basic_2/reduction/cpr_lift.ma". include "basic_2/reduction/cnr.ma". -(* CONTEXT-SENSITIVE NORMAL TERMS *******************************************) +(* NORMAL TERMS FOR CONTEXT-SENSITIVE REDUCTION *****************************) (* Advanced properties ******************************************************) diff --git a/matita/matita/contribs/lambdadelta/basic_2/reduction/cnx.ma b/matita/matita/contribs/lambdadelta/basic_2/reduction/cnx.ma index 47f92caaa..983e2ac36 100644 --- a/matita/matita/contribs/lambdadelta/basic_2/reduction/cnx.ma +++ b/matita/matita/contribs/lambdadelta/basic_2/reduction/cnx.ma @@ -12,18 +12,18 @@ (* *) (**************************************************************************) -include "basic_2/notation/relations/normal_5.ma". +include "basic_2/notation/relations/prednormal_5.ma". include "basic_2/reduction/cnr.ma". include "basic_2/reduction/cpx.ma". -(* CONTEXT-SENSITIVE EXTENDED NORMAL TERMS **********************************) +(* NORMAL TERMS FOR CONTEXT-SENSITIVE EXTENDED REDUCTION ********************) definition cnx: ∀h. sd h → relation3 genv lenv term ≝ λh,g,G,L. NF … (cpx h g G L) (eq …). interpretation - "context-sensitive extended normality (term)" - 'Normal h g L T = (cnx h g L T). + "normality for context-sensitive extended reduction (term)" + 'PRedNormal h g L T = (cnx h g L T). (* Basic inversion lemmas ***************************************************) diff --git a/matita/matita/contribs/lambdadelta/basic_2/reduction/cnx_cix.ma b/matita/matita/contribs/lambdadelta/basic_2/reduction/cnx_cix.ma index 18dc60e3e..484306007 100644 --- a/matita/matita/contribs/lambdadelta/basic_2/reduction/cnx_cix.ma +++ b/matita/matita/contribs/lambdadelta/basic_2/reduction/cnx_cix.ma @@ -15,14 +15,14 @@ include "basic_2/reduction/cpx_cix.ma". include "basic_2/reduction/cnx_crx.ma". -(* CONTEXT-SENSITIVE EXTENDED NORMAL TERMS **********************************) +(* NORMAL TERMS FOR CONTEXT-SENSITIVE EXTENDED REDUCTION ********************) -(* Main properties on context-sensitive extended irreducible terms **********) +(* Main properties on irreducibility ****************************************) theorem cix_cnr: ∀h,g,G,L,T. ⦃G, L⦄ ⊢ ➡[h, g] 𝐈⦃T⦄ → ⦃G, L⦄ ⊢ ➡[h, g] 𝐍⦃T⦄. /2 width=6 by cpx_fwd_cix/ qed. -(* Main inversion lemmas on context-sensitive extended irreducible terms ****) +(* Main inversion lemmas on irreducibility **********************************) theorem cnr_inv_cix: ∀h,g,G,L,T. ⦃G, L⦄ ⊢ ➡[h, g] 𝐍⦃T⦄ → ⦃G, L⦄ ⊢ ➡[h, g] 𝐈⦃T⦄. /2 width=7 by cnx_inv_crx/ qed-. diff --git a/matita/matita/contribs/lambdadelta/basic_2/reduction/cnx_crx.ma b/matita/matita/contribs/lambdadelta/basic_2/reduction/cnx_crx.ma index c6d51c630..db2da4fb8 100644 --- a/matita/matita/contribs/lambdadelta/basic_2/reduction/cnx_crx.ma +++ b/matita/matita/contribs/lambdadelta/basic_2/reduction/cnx_crx.ma @@ -15,9 +15,9 @@ include "basic_2/reduction/crx.ma". include "basic_2/reduction/cnx.ma". -(* CONTEXT-SENSITIVE EXTENDED NORMAL TERMS **********************************) +(* NORMAL TERMS FOR CONTEXT-SENSITIVE EXTENDED REDUCTION ********************) -(* Advanced inversion lemmas on context-sensitive reducible terms ***********) +(* Advanced inversion lemmas on reducibility ********************************) (* Note: this property is unusual *) lemma cnx_inv_crx: ∀h,g,G,L,T. ⦃G, L⦄ ⊢ ➡[h, g] 𝐑⦃T⦄ → ⦃G, L⦄ ⊢ ➡[h, g] 𝐍⦃T⦄ → ⊥. diff --git a/matita/matita/contribs/lambdadelta/basic_2/reduction/cnx_lift.ma b/matita/matita/contribs/lambdadelta/basic_2/reduction/cnx_lift.ma index 7f3bedbd0..91ea0091b 100644 --- a/matita/matita/contribs/lambdadelta/basic_2/reduction/cnx_lift.ma +++ b/matita/matita/contribs/lambdadelta/basic_2/reduction/cnx_lift.ma @@ -15,7 +15,7 @@ include "basic_2/reduction/cpx_lift.ma". include "basic_2/reduction/cnx.ma". -(* CONTEXT-SENSITIVE EXTENDED NORMAL TERMS **********************************) +(* NORMAL TERMS FOR CONTEXT-SENSITIVE EXTENDED REDUCTION ********************) (* Relocation properties ****************************************************) diff --git a/matita/matita/contribs/lambdadelta/basic_2/reduction/cpr_cir.ma b/matita/matita/contribs/lambdadelta/basic_2/reduction/cpr_cir.ma index d0e1e19ac..99846d67a 100644 --- a/matita/matita/contribs/lambdadelta/basic_2/reduction/cpr_cir.ma +++ b/matita/matita/contribs/lambdadelta/basic_2/reduction/cpr_cir.ma @@ -17,7 +17,7 @@ include "basic_2/reduction/cpr.ma". (* CONTEXT-SENSITIVE PARALLEL REDUCTION FOR TERMS ***************************) -(* Advanced forward lemmas on context-sensitive irreducible terms ***********) +(* Advanced forward lemmas on irreducibility ********************************) lemma cpr_fwd_cir: ∀G,L,T1,T2. ⦃G, L⦄ ⊢ T1 ➡ T2 → ⦃G, L⦄ ⊢ ➡ 𝐈⦃T1⦄ → T2 = T1. #G #L #T1 #T2 #H elim H -G -L -T1 -T2 diff --git a/matita/matita/contribs/lambdadelta/basic_2/reduction/cpx_cix.ma b/matita/matita/contribs/lambdadelta/basic_2/reduction/cpx_cix.ma index ce54e9a7e..b6e057702 100644 --- a/matita/matita/contribs/lambdadelta/basic_2/reduction/cpx_cix.ma +++ b/matita/matita/contribs/lambdadelta/basic_2/reduction/cpx_cix.ma @@ -17,7 +17,7 @@ include "basic_2/reduction/cpx.ma". (* CONTEXT-SENSITIVE EXTENDED PARALLEL REDUCTION FOR TERMS ******************) -(* Advanced forward lemmas on context-sensitive extended irreducible terms **) +(* Advanced forward lemmas on irreducibility ********************************) lemma cpx_fwd_cix: ∀h,g,G,L,T1,T2. ⦃G, L⦄ ⊢ T1 ➡[h, g] T2 → ⦃G, L⦄ ⊢ ➡[h, g] 𝐈⦃T1⦄ → T2 = T1. #h #g #G #L #T1 #T2 #H elim H -G -L -T1 -T2 diff --git a/matita/matita/contribs/lambdadelta/basic_2/reduction/cpx_cpys.ma b/matita/matita/contribs/lambdadelta/basic_2/reduction/cpx_cpys.ma index 3c0507b32..6cb5a00ba 100644 --- a/matita/matita/contribs/lambdadelta/basic_2/reduction/cpx_cpys.ma +++ b/matita/matita/contribs/lambdadelta/basic_2/reduction/cpx_cpys.ma @@ -19,10 +19,10 @@ include "basic_2/reduction/cpx.ma". (* Properties on context-sensitive extended multiple substitution for terms *) -lemma cpys_cpx: ∀h,g,G,L,T1,T2,d,e. ⦃G, L⦄ ⊢ T1 ▶*×[d, e] T2 → ⦃G, L⦄ ⊢ T1 ➡[h, g] T2. +lemma cpys_cpx: ∀h,g,G,L,T1,T2,d,e. ⦃G, L⦄ ⊢ T1 ▶*[d, e] T2 → ⦃G, L⦄ ⊢ T1 ➡[h, g] T2. #h #g #G #L #T1 #T2 #d #e #H @(cpys_ind_alt … H) -G -L -T1 -T2 -d -e /2 width=7 by cpx_delta, cpx_bind, cpx_flat/ qed. -lemma cpy_cpx: ∀h,g,G,L,T1,T2,d,e. ⦃G, L⦄ ⊢ T1 ▶×[d, e] T2 → ⦃G, L⦄ ⊢ T1 ➡[h, g] T2. +lemma cpy_cpx: ∀h,g,G,L,T1,T2,d,e. ⦃G, L⦄ ⊢ T1 ▶[d, e] T2 → ⦃G, L⦄ ⊢ T1 ➡[h, g] T2. /3 width=3 by cpy_cpys, cpys_cpx/ qed. diff --git a/matita/matita/contribs/lambdadelta/basic_2/reduction/crr.ma b/matita/matita/contribs/lambdadelta/basic_2/reduction/crr.ma index 02aaa8209..9158a53af 100644 --- a/matita/matita/contribs/lambdadelta/basic_2/reduction/crr.ma +++ b/matita/matita/contribs/lambdadelta/basic_2/reduction/crr.ma @@ -12,11 +12,11 @@ (* *) (**************************************************************************) -include "basic_2/notation/relations/reducible_3.ma". +include "basic_2/notation/relations/predreducible_3.ma". include "basic_2/grammar/genv.ma". include "basic_2/relocation/ldrop.ma". -(* CONTEXT-SENSITIVE REDUCIBLE TERMS ****************************************) +(* REDUCIBLE TERMS FOR CONTEXT-SENSITIVE REDUCTION **************************) (* reducible binary items *) definition ri2: predicate item2 ≝ @@ -40,8 +40,8 @@ inductive crr (G:genv): relation2 lenv term ≝ . interpretation - "context-sensitive reducibility (term)" - 'Reducible G L T = (crr G L T). + "reducibility for context-sensitive reduction (term)" + 'PRedReducible G L T = (crr G L T). (* Basic inversion lemmas ***************************************************) diff --git a/matita/matita/contribs/lambdadelta/basic_2/reduction/crr_append.ma b/matita/matita/contribs/lambdadelta/basic_2/reduction/crr_append.ma index 8b4cfb336..dbf794d99 100644 --- a/matita/matita/contribs/lambdadelta/basic_2/reduction/crr_append.ma +++ b/matita/matita/contribs/lambdadelta/basic_2/reduction/crr_append.ma @@ -15,7 +15,7 @@ include "basic_2/relocation/ldrop_append.ma". include "basic_2/reduction/crr.ma". -(* CONTEXT-SENSITIVE REDUCIBLE TERMS ****************************************) +(* REDUCIBLE TERMS FOR CONTEXT-SENSITIVE REDUCTION **************************) (* Advanved properties ******************************************************) diff --git a/matita/matita/contribs/lambdadelta/basic_2/reduction/crr_lift.ma b/matita/matita/contribs/lambdadelta/basic_2/reduction/crr_lift.ma index 41f626cee..ddb58a580 100644 --- a/matita/matita/contribs/lambdadelta/basic_2/reduction/crr_lift.ma +++ b/matita/matita/contribs/lambdadelta/basic_2/reduction/crr_lift.ma @@ -15,7 +15,7 @@ include "basic_2/relocation/ldrop_ldrop.ma". include "basic_2/reduction/crr.ma". -(* CONTEXT-SENSITIVE REDUCIBLE TERMS ****************************************) +(* REDUCIBLE TERMS FOR CONTEXT-SENSITIVE REDUCTION **************************) (* Properties on relocation *************************************************) diff --git a/matita/matita/contribs/lambdadelta/basic_2/reduction/crx.ma b/matita/matita/contribs/lambdadelta/basic_2/reduction/crx.ma index 86796ae0b..818374e6e 100644 --- a/matita/matita/contribs/lambdadelta/basic_2/reduction/crx.ma +++ b/matita/matita/contribs/lambdadelta/basic_2/reduction/crx.ma @@ -12,11 +12,11 @@ (* *) (**************************************************************************) -include "basic_2/notation/relations/reducible_5.ma". +include "basic_2/notation/relations/predreducible_5.ma". include "basic_2/static/sd.ma". include "basic_2/reduction/crr.ma". -(* CONTEXT-SENSITIVE EXTENDED REDUCIBLE TERMS *******************************) +(* REDUCIBLE TERMS FOR CONTEXT-SENSITIVE EXTENDED REDUCTION *****************) (* activate genv *) (* extended reducible terms *) @@ -33,8 +33,8 @@ inductive crx (h) (g) (G:genv): relation2 lenv term ≝ . interpretation - "context-sensitive extended reducibility (term)" - 'Reducible h g G L T = (crx h g G L T). + "reducibility for context-sensitive extended reduction (term)" + 'PRedReducible h g G L T = (crx h g G L T). (* Basic properties *********************************************************) diff --git a/matita/matita/contribs/lambdadelta/basic_2/reduction/crx_append.ma b/matita/matita/contribs/lambdadelta/basic_2/reduction/crx_append.ma index ca86ad11e..56667b20f 100644 --- a/matita/matita/contribs/lambdadelta/basic_2/reduction/crx_append.ma +++ b/matita/matita/contribs/lambdadelta/basic_2/reduction/crx_append.ma @@ -15,7 +15,7 @@ include "basic_2/relocation/ldrop_append.ma". include "basic_2/reduction/crx.ma". -(* CONTEXT-SENSITIVE EXTENDED REDUCIBLE TERMS *******************************) +(* REDUCIBLE TERMS FOR CONTEXT-SENSITIVE EXTENDED REDUCTION *****************) (* Advanved properties ******************************************************) diff --git a/matita/matita/contribs/lambdadelta/basic_2/reduction/crx_lift.ma b/matita/matita/contribs/lambdadelta/basic_2/reduction/crx_lift.ma index 9c268927a..b1afecdc5 100644 --- a/matita/matita/contribs/lambdadelta/basic_2/reduction/crx_lift.ma +++ b/matita/matita/contribs/lambdadelta/basic_2/reduction/crx_lift.ma @@ -15,7 +15,7 @@ include "basic_2/relocation/ldrop_ldrop.ma". include "basic_2/reduction/crx.ma". -(* CONTEXT-SENSITIVE EXTENDED REDUCIBLE TERMS *******************************) +(* REDUCIBLE TERMS FOR CONTEXT-SENSITIVE EXTENDED REDUCTION *****************) (* Properties on relocation *************************************************) diff --git a/matita/matita/contribs/lambdadelta/basic_2/relocation/cpy.ma b/matita/matita/contribs/lambdadelta/basic_2/relocation/cpy.ma index 0e440cf7f..06e4a43c9 100644 --- a/matita/matita/contribs/lambdadelta/basic_2/relocation/cpy.ma +++ b/matita/matita/contribs/lambdadelta/basic_2/relocation/cpy.ma @@ -13,7 +13,7 @@ (**************************************************************************) include "ground_2/ynat/ynat_max.ma". -include "basic_2/notation/relations/extpsubst_6.ma". +include "basic_2/notation/relations/psubst_6.ma". include "basic_2/grammar/genv.ma". include "basic_2/grammar/cl_shift.ma". include "basic_2/relocation/ldrop_append.ma". @@ -35,7 +35,7 @@ inductive cpy: ynat → ynat → relation4 genv lenv term term ≝ . interpretation "context-sensitive extended ordinary substritution (term)" - 'ExtPSubst G L T1 d e T2 = (cpy d e G L T1 T2). + 'PSubst G L T1 d e T2 = (cpy d e G L T1 T2). (* Basic properties *********************************************************) @@ -49,13 +49,13 @@ lemma lsuby_cpy_trans: ∀G,d,e. lsub_trans … (cpy d e G) (lsuby d e). ] qed-. -lemma cpy_refl: ∀G,T,L,d,e. ⦃G, L⦄ ⊢ T ▶×[d, e] T. +lemma cpy_refl: ∀G,T,L,d,e. ⦃G, L⦄ ⊢ T ▶[d, e] T. #G #T elim T -T // * /2 width=1 by cpy_bind, cpy_flat/ qed. (* Basic_1: was: subst1_ex *) lemma cpy_full: ∀I,G,K,V,T1,L,d. ⇩[d] L ≡ K.ⓑ{I}V → - ∃∃T2,T. ⦃G, L⦄ ⊢ T1 ▶×[d, 1] T2 & ⇧[d, 1] T ≡ T2. + ∃∃T2,T. ⦃G, L⦄ ⊢ T1 ▶[d, 1] T2 & ⇧[d, 1] T ≡ T2. #I #G #K #V #T1 elim T1 -T1 [ * #i #L #d #HLK /2 width=4 by lift_sort, lift_gref, ex2_2_intro/ @@ -75,9 +75,9 @@ lemma cpy_full: ∀I,G,K,V,T1,L,d. ⇩[d] L ≡ K.ⓑ{I}V → ] qed-. -lemma cpy_weak: ∀G,L,T1,T2,d1,e1. ⦃G, L⦄ ⊢ T1 ▶×[d1, e1] T2 → +lemma cpy_weak: ∀G,L,T1,T2,d1,e1. ⦃G, L⦄ ⊢ T1 ▶[d1, e1] T2 → ∀d2,e2. d2 ≤ d1 → d1 + e1 ≤ d2 + e2 → - ⦃G, L⦄ ⊢ T1 ▶×[d2, e2] T2. + ⦃G, L⦄ ⊢ T1 ▶[d2, e2] T2. #G #L #T1 #T2 #d1 #e1 #H elim H -G -L -T1 -T2 -d1 -e1 // [ /3 width=5 by cpy_subst, ylt_yle_trans, yle_trans/ | /4 width=3 by cpy_bind, ylt_yle_trans, yle_succ/ @@ -86,7 +86,7 @@ lemma cpy_weak: ∀G,L,T1,T2,d1,e1. ⦃G, L⦄ ⊢ T1 ▶×[d1, e1] T2 → qed-. lemma cpy_weak_top: ∀G,L,T1,T2,d,e. - ⦃G, L⦄ ⊢ T1 ▶×[d, e] T2 → ⦃G, L⦄ ⊢ T1 ▶×[d, |L| - d] T2. + ⦃G, L⦄ ⊢ T1 ▶[d, e] T2 → ⦃G, L⦄ ⊢ T1 ▶[d, |L| - d] T2. #G #L #T1 #T2 #d #e #H elim H -G -L -T1 -T2 -d -e // [ #I #G #L #K #V #W #i #d #e #Hdi #_ #HLK #HVW lapply (ldrop_fwd_length_lt2 … HLK) @@ -98,16 +98,16 @@ lemma cpy_weak_top: ∀G,L,T1,T2,d,e. qed-. lemma cpy_weak_full: ∀G,L,T1,T2,d,e. - ⦃G, L⦄ ⊢ T1 ▶×[d, e] T2 → ⦃G, L⦄ ⊢ T1 ▶×[0, |L|] T2. + ⦃G, L⦄ ⊢ T1 ▶[d, e] T2 → ⦃G, L⦄ ⊢ T1 ▶[0, |L|] T2. #G #L #T1 #T2 #d #e #HT12 lapply (cpy_weak … HT12 0 (d + e) ? ?) -HT12 /2 width=2 by cpy_weak_top/ qed-. -lemma cpy_up: ∀G,L,U1,U2,dt,et. ⦃G, L⦄ ⊢ U1 ▶×[dt, et] U2 → +lemma cpy_up: ∀G,L,U1,U2,dt,et. ⦃G, L⦄ ⊢ U1 ▶[dt, et] U2 → ∀T1,d,e. ⇧[d, e] T1 ≡ U1 → d ≤ dt → d + e ≤ dt + et → - ∃∃T2. ⦃G, L⦄ ⊢ U1 ▶×[d+e, dt+et-(d+e)] U2 & ⇧[d, e] T2 ≡ U2. + ∃∃T2. ⦃G, L⦄ ⊢ U1 ▶[d+e, dt+et-(d+e)] U2 & ⇧[d, e] T2 ≡ U2. #G #L #U1 #U2 #dt #et #H elim H -G -L -U1 -U2 -dt -et [ * #i #G #L #dt #et #T1 #d #e #H #_ [ lapply (lift_inv_sort2 … H) -H #H destruct /2 width=3 by ex2_intro/ @@ -135,8 +135,8 @@ lemma cpy_up: ∀G,L,U1,U2,dt,et. ⦃G, L⦄ ⊢ U1 ▶×[dt, et] U2 → ] qed-. -lemma cpy_split_up: ∀G,L,T1,T2,d,e. ⦃G, L⦄ ⊢ T1 ▶×[d, e] T2 → ∀i. i ≤ d + e → - ∃∃T. ⦃G, L⦄ ⊢ T1 ▶×[d, i-d] T & ⦃G, L⦄ ⊢ T ▶×[i, d+e-i] T2. +lemma cpy_split_up: ∀G,L,T1,T2,d,e. ⦃G, L⦄ ⊢ T1 ▶[d, e] T2 → ∀i. i ≤ d + e → + ∃∃T. ⦃G, L⦄ ⊢ T1 ▶[d, i-d] T & ⦃G, L⦄ ⊢ T ▶[i, d+e-i] T2. #G #L #T1 #T2 #d #e #H elim H -G -L -T1 -T2 -d -e [ /2 width=3 by ex2_intro/ | #I #G #L #K #V #W #i #d #e #Hdi #Hide #HLK #HVW #j #Hjde @@ -154,8 +154,8 @@ lemma cpy_split_up: ∀G,L,T1,T2,d,e. ⦃G, L⦄ ⊢ T1 ▶×[d, e] T2 → ∀i. ] qed-. -lemma cpy_split_down: ∀G,L,T1,T2,d,e. ⦃G, L⦄ ⊢ T1 ▶×[d, e] T2 → ∀i. i ≤ d + e → - ∃∃T. ⦃G, L⦄ ⊢ T1 ▶×[i, d+e-i] T & ⦃G, L⦄ ⊢ T ▶×[d, i-d] T2. +lemma cpy_split_down: ∀G,L,T1,T2,d,e. ⦃G, L⦄ ⊢ T1 ▶[d, e] T2 → ∀i. i ≤ d + e → + ∃∃T. ⦃G, L⦄ ⊢ T1 ▶[i, d+e-i] T & ⦃G, L⦄ ⊢ T ▶[d, i-d] T2. #G #L #T1 #T2 #d #e #H elim H -G -L -T1 -T2 -d -e [ /2 width=3 by ex2_intro/ | #I #G #L #K #V #W #i #d #e #Hdi #Hide #HLK #HVW #j #Hjde @@ -184,7 +184,7 @@ qed-. (* Basic inversion lemmas ***************************************************) -fact cpy_inv_atom1_aux: ∀G,L,T1,T2,d,e. ⦃G, L⦄ ⊢ T1 ▶×[d, e] T2 → ∀J. T1 = ⓪{J} → +fact cpy_inv_atom1_aux: ∀G,L,T1,T2,d,e. ⦃G, L⦄ ⊢ T1 ▶[d, e] T2 → ∀J. T1 = ⓪{J} → T2 = ⓪{J} ∨ ∃∃I,K,V,i. d ≤ yinj i & i < d + e & ⇩[i] L ≡ K.ⓑ{I}V & @@ -198,7 +198,7 @@ fact cpy_inv_atom1_aux: ∀G,L,T1,T2,d,e. ⦃G, L⦄ ⊢ T1 ▶×[d, e] T2 → ] qed-. -lemma cpy_inv_atom1: ∀I,G,L,T2,d,e. ⦃G, L⦄ ⊢ ⓪{I} ▶×[d, e] T2 → +lemma cpy_inv_atom1: ∀I,G,L,T2,d,e. ⦃G, L⦄ ⊢ ⓪{I} ▶[d, e] T2 → T2 = ⓪{I} ∨ ∃∃J,K,V,i. d ≤ yinj i & i < d + e & ⇩[i] L ≡ K.ⓑ{J}V & @@ -207,14 +207,14 @@ lemma cpy_inv_atom1: ∀I,G,L,T2,d,e. ⦃G, L⦄ ⊢ ⓪{I} ▶×[d, e] T2 → /2 width=4 by cpy_inv_atom1_aux/ qed-. (* Basic_1: was: subst1_gen_sort *) -lemma cpy_inv_sort1: ∀G,L,T2,k,d,e. ⦃G, L⦄ ⊢ ⋆k ▶×[d, e] T2 → T2 = ⋆k. +lemma cpy_inv_sort1: ∀G,L,T2,k,d,e. ⦃G, L⦄ ⊢ ⋆k ▶[d, e] T2 → T2 = ⋆k. #G #L #T2 #k #d #e #H elim (cpy_inv_atom1 … H) -H // * #I #K #V #i #_ #_ #_ #_ #H destruct qed-. (* Basic_1: was: subst1_gen_lref *) -lemma cpy_inv_lref1: ∀G,L,T2,i,d,e. ⦃G, L⦄ ⊢ #i ▶×[d, e] T2 → +lemma cpy_inv_lref1: ∀G,L,T2,i,d,e. ⦃G, L⦄ ⊢ #i ▶[d, e] T2 → T2 = #i ∨ ∃∃I,K,V. d ≤ i & i < d + e & ⇩[i] L ≡ K.ⓑ{I}V & @@ -224,16 +224,16 @@ elim (cpy_inv_atom1 … H) -H /2 width=1 by or_introl/ * #I #K #V #j #Hdj #Hjde #HLK #HVT2 #H destruct /3 width=5 by ex4_3_intro, or_intror/ qed-. -lemma cpy_inv_gref1: ∀G,L,T2,p,d,e. ⦃G, L⦄ ⊢ §p ▶×[d, e] T2 → T2 = §p. +lemma cpy_inv_gref1: ∀G,L,T2,p,d,e. ⦃G, L⦄ ⊢ §p ▶[d, e] T2 → T2 = §p. #G #L #T2 #p #d #e #H elim (cpy_inv_atom1 … H) -H // * #I #K #V #i #_ #_ #_ #_ #H destruct qed-. -fact cpy_inv_bind1_aux: ∀G,L,U1,U2,d,e. ⦃G, L⦄ ⊢ U1 ▶×[d, e] U2 → +fact cpy_inv_bind1_aux: ∀G,L,U1,U2,d,e. ⦃G, L⦄ ⊢ U1 ▶[d, e] U2 → ∀a,I,V1,T1. U1 = ⓑ{a,I}V1.T1 → - ∃∃V2,T2. ⦃G, L⦄ ⊢ V1 ▶×[d, e] V2 & - ⦃G, L. ⓑ{I}V1⦄ ⊢ T1 ▶×[⫯d, e] T2 & + ∃∃V2,T2. ⦃G, L⦄ ⊢ V1 ▶[d, e] V2 & + ⦃G, L. ⓑ{I}V1⦄ ⊢ T1 ▶[⫯d, e] T2 & U2 = ⓑ{a,I}V2.T2. #G #L #U1 #U2 #d #e * -G -L -U1 -U2 -d -e [ #I #G #L #d #e #b #J #W1 #U1 #H destruct @@ -243,16 +243,16 @@ fact cpy_inv_bind1_aux: ∀G,L,U1,U2,d,e. ⦃G, L⦄ ⊢ U1 ▶×[d, e] U2 → ] qed-. -lemma cpy_inv_bind1: ∀a,I,G,L,V1,T1,U2,d,e. ⦃G, L⦄ ⊢ ⓑ{a,I} V1. T1 ▶×[d, e] U2 → - ∃∃V2,T2. ⦃G, L⦄ ⊢ V1 ▶×[d, e] V2 & - ⦃G, L.ⓑ{I}V1⦄ ⊢ T1 ▶×[⫯d, e] T2 & +lemma cpy_inv_bind1: ∀a,I,G,L,V1,T1,U2,d,e. ⦃G, L⦄ ⊢ ⓑ{a,I} V1. T1 ▶[d, e] U2 → + ∃∃V2,T2. ⦃G, L⦄ ⊢ V1 ▶[d, e] V2 & + ⦃G, L.ⓑ{I}V1⦄ ⊢ T1 ▶[⫯d, e] T2 & U2 = ⓑ{a,I}V2.T2. /2 width=3 by cpy_inv_bind1_aux/ qed-. -fact cpy_inv_flat1_aux: ∀G,L,U1,U2,d,e. ⦃G, L⦄ ⊢ U1 ▶×[d, e] U2 → +fact cpy_inv_flat1_aux: ∀G,L,U1,U2,d,e. ⦃G, L⦄ ⊢ U1 ▶[d, e] U2 → ∀I,V1,T1. U1 = ⓕ{I}V1.T1 → - ∃∃V2,T2. ⦃G, L⦄ ⊢ V1 ▶×[d, e] V2 & - ⦃G, L⦄ ⊢ T1 ▶×[d, e] T2 & + ∃∃V2,T2. ⦃G, L⦄ ⊢ V1 ▶[d, e] V2 & + ⦃G, L⦄ ⊢ T1 ▶[d, e] T2 & U2 = ⓕ{I}V2.T2. #G #L #U1 #U2 #d #e * -G -L -U1 -U2 -d -e [ #I #G #L #d #e #J #W1 #U1 #H destruct @@ -262,14 +262,14 @@ fact cpy_inv_flat1_aux: ∀G,L,U1,U2,d,e. ⦃G, L⦄ ⊢ U1 ▶×[d, e] U2 → ] qed-. -lemma cpy_inv_flat1: ∀I,G,L,V1,T1,U2,d,e. ⦃G, L⦄ ⊢ ⓕ{I} V1. T1 ▶×[d, e] U2 → - ∃∃V2,T2. ⦃G, L⦄ ⊢ V1 ▶×[d, e] V2 & - ⦃G, L⦄ ⊢ T1 ▶×[d, e] T2 & +lemma cpy_inv_flat1: ∀I,G,L,V1,T1,U2,d,e. ⦃G, L⦄ ⊢ ⓕ{I} V1. T1 ▶[d, e] U2 → + ∃∃V2,T2. ⦃G, L⦄ ⊢ V1 ▶[d, e] V2 & + ⦃G, L⦄ ⊢ T1 ▶[d, e] T2 & U2 = ⓕ{I}V2.T2. /2 width=3 by cpy_inv_flat1_aux/ qed-. -fact cpy_inv_refl_O2_aux: ∀G,L,T1,T2,d,e. ⦃G, L⦄ ⊢ T1 ▶×[d, e] T2 → e = 0 → T1 = T2. +fact cpy_inv_refl_O2_aux: ∀G,L,T1,T2,d,e. ⦃G, L⦄ ⊢ T1 ▶[d, e] T2 → e = 0 → T1 = T2. #G #L #T1 #T2 #d #e #H elim H -G -L -T1 -T2 -d -e [ // | #I #G #L #K #V #W #i #d #e #Hdi #Hide #_ #_ #H destruct @@ -279,24 +279,24 @@ fact cpy_inv_refl_O2_aux: ∀G,L,T1,T2,d,e. ⦃G, L⦄ ⊢ T1 ▶×[d, e] T2 → ] qed-. -lemma cpy_inv_refl_O2: ∀G,L,T1,T2,d. ⦃G, L⦄ ⊢ T1 ▶×[d, 0] T2 → T1 = T2. +lemma cpy_inv_refl_O2: ∀G,L,T1,T2,d. ⦃G, L⦄ ⊢ T1 ▶[d, 0] T2 → T1 = T2. /2 width=6 by cpy_inv_refl_O2_aux/ qed-. (* Basic_1: was: subst1_gen_lift_eq *) lemma cpy_inv_lift1_eq: ∀G,T1,U1,d,e. ⇧[d, e] T1 ≡ U1 → - ∀L,U2. ⦃G, L⦄ ⊢ U1 ▶×[d, e] U2 → U1 = U2. + ∀L,U2. ⦃G, L⦄ ⊢ U1 ▶[d, e] U2 → U1 = U2. #G #T1 #U1 #d #e #HTU1 #L #U2 #HU12 elim (cpy_up … HU12 … HTU1) -HU12 -HTU1 /2 width=4 by cpy_inv_refl_O2/ qed-. (* Basic forward lemmas *****************************************************) -lemma cpy_fwd_tw: ∀G,L,T1,T2,d,e. ⦃G, L⦄ ⊢ T1 ▶×[d, e] T2 → ♯{T1} ≤ ♯{T2}. +lemma cpy_fwd_tw: ∀G,L,T1,T2,d,e. ⦃G, L⦄ ⊢ T1 ▶[d, e] T2 → ♯{T1} ≤ ♯{T2}. #G #L #T1 #T2 #d #e #H elim H -G -L -T1 -T2 -d -e normalize /3 width=1 by monotonic_le_plus_l, le_plus/ qed-. -lemma cpy_fwd_shift1: ∀G,L1,L,T1,T,d,e. ⦃G, L⦄ ⊢ L1 @@ T1 ▶×[d, e] T → +lemma cpy_fwd_shift1: ∀G,L1,L,T1,T,d,e. ⦃G, L⦄ ⊢ L1 @@ T1 ▶[d, e] T → ∃∃L2,T2. |L1| = |L2| & T = L2 @@ T2. #G #L1 @(lenv_ind_dx … L1) -L1 normalize [ #L #T1 #T #d #e #HT1 diff --git a/matita/matita/contribs/lambdadelta/basic_2/relocation/cpy_cpy.ma b/matita/matita/contribs/lambdadelta/basic_2/relocation/cpy_cpy.ma index 055fe055d..66b0487db 100644 --- a/matita/matita/contribs/lambdadelta/basic_2/relocation/cpy_cpy.ma +++ b/matita/matita/contribs/lambdadelta/basic_2/relocation/cpy_cpy.ma @@ -19,9 +19,9 @@ include "basic_2/relocation/cpy_lift.ma". (* Main properties **********************************************************) (* Basic_1: was: subst1_confluence_eq *) -theorem cpy_conf_eq: ∀G,L,T0,T1,d1,e1. ⦃G, L⦄ ⊢ T0 ▶×[d1, e1] T1 → - ∀T2,d2,e2. ⦃G, L⦄ ⊢ T0 ▶×[d2, e2] T2 → - ∃∃T. ⦃G, L⦄ ⊢ T1 ▶×[d2, e2] T & ⦃G, L⦄ ⊢ T2 ▶×[d1, e1] T. +theorem cpy_conf_eq: ∀G,L,T0,T1,d1,e1. ⦃G, L⦄ ⊢ T0 ▶[d1, e1] T1 → + ∀T2,d2,e2. ⦃G, L⦄ ⊢ T0 ▶[d2, e2] T2 → + ∃∃T. ⦃G, L⦄ ⊢ T1 ▶[d2, e2] T & ⦃G, L⦄ ⊢ T2 ▶[d1, e1] T. #G #L #T0 #T1 #d1 #e1 #H elim H -G -L -T0 -T1 -d1 -e1 [ /2 width=3 by ex2_intro/ | #I1 #G #L #K1 #V1 #T1 #i0 #d1 #e1 #Hd1 #Hde1 #HLK1 #HVT1 #T2 #d2 #e2 #H @@ -46,10 +46,10 @@ theorem cpy_conf_eq: ∀G,L,T0,T1,d1,e1. ⦃G, L⦄ ⊢ T0 ▶×[d1, e1] T1 → qed-. (* Basic_1: was: subst1_confluence_neq *) -theorem cpy_conf_neq: ∀G,L1,T0,T1,d1,e1. ⦃G, L1⦄ ⊢ T0 ▶×[d1, e1] T1 → - ∀L2,T2,d2,e2. ⦃G, L2⦄ ⊢ T0 ▶×[d2, e2] T2 → +theorem cpy_conf_neq: ∀G,L1,T0,T1,d1,e1. ⦃G, L1⦄ ⊢ T0 ▶[d1, e1] T1 → + ∀L2,T2,d2,e2. ⦃G, L2⦄ ⊢ T0 ▶[d2, e2] T2 → (d1 + e1 ≤ d2 ∨ d2 + e2 ≤ d1) → - ∃∃T. ⦃G, L2⦄ ⊢ T1 ▶×[d2, e2] T & ⦃G, L1⦄ ⊢ T2 ▶×[d1, e1] T. + ∃∃T. ⦃G, L2⦄ ⊢ T1 ▶[d2, e2] T & ⦃G, L1⦄ ⊢ T2 ▶[d1, e1] T. #G #L1 #T0 #T1 #d1 #e1 #H elim H -G -L1 -T0 -T1 -d1 -e1 [ /2 width=3 by ex2_intro/ | #I1 #G #L1 #K1 #V1 #T1 #i0 #d1 #e1 #Hd1 #Hde1 #HLK1 #HVT1 #L2 #T2 #d2 #e2 #H1 #H2 @@ -78,8 +78,8 @@ qed-. (* Note: the constant 1 comes from cpy_subst *) (* Basic_1: was: subst1_trans *) -theorem cpy_trans_ge: ∀G,L,T1,T0,d,e. ⦃G, L⦄ ⊢ T1 ▶×[d, e] T0 → - ∀T2. ⦃G, L⦄ ⊢ T0 ▶×[d, 1] T2 → 1 ≤ e → ⦃G, L⦄ ⊢ T1 ▶×[d, e] T2. +theorem cpy_trans_ge: ∀G,L,T1,T0,d,e. ⦃G, L⦄ ⊢ T1 ▶[d, e] T0 → + ∀T2. ⦃G, L⦄ ⊢ T0 ▶[d, 1] T2 → 1 ≤ e → ⦃G, L⦄ ⊢ T1 ▶[d, e] T2. #G #L #T1 #T0 #d #e #H elim H -G -L -T1 -T0 -d -e [ #I #G #L #d #e #T2 #H #He elim (cpy_inv_atom1 … H) -H @@ -99,9 +99,9 @@ theorem cpy_trans_ge: ∀G,L,T1,T0,d,e. ⦃G, L⦄ ⊢ T1 ▶×[d, e] T0 → ] qed-. -theorem cpy_trans_down: ∀G,L,T1,T0,d1,e1. ⦃G, L⦄ ⊢ T1 ▶×[d1, e1] T0 → - ∀T2,d2,e2. ⦃G, L⦄ ⊢ T0 ▶×[d2, e2] T2 → d2 + e2 ≤ d1 → - ∃∃T. ⦃G, L⦄ ⊢ T1 ▶×[d2, e2] T & ⦃G, L⦄ ⊢ T ▶×[d1, e1] T2. +theorem cpy_trans_down: ∀G,L,T1,T0,d1,e1. ⦃G, L⦄ ⊢ T1 ▶[d1, e1] T0 → + ∀T2,d2,e2. ⦃G, L⦄ ⊢ T0 ▶[d2, e2] T2 → d2 + e2 ≤ d1 → + ∃∃T. ⦃G, L⦄ ⊢ T1 ▶[d2, e2] T & ⦃G, L⦄ ⊢ T ▶[d1, e1] T2. #G #L #T1 #T0 #d1 #e1 #H elim H -G -L -T1 -T0 -d1 -e1 [ /2 width=3 by ex2_intro/ | #I #G #L #K #V #W #i1 #d1 #e1 #Hdi1 #Hide1 #HLK #HVW #T2 #d2 #e2 #HWT2 #Hde2d1 diff --git a/matita/matita/contribs/lambdadelta/basic_2/relocation/cpy_lift.ma b/matita/matita/contribs/lambdadelta/basic_2/relocation/cpy_lift.ma index 715035121..aa0b2416a 100644 --- a/matita/matita/contribs/lambdadelta/basic_2/relocation/cpy_lift.ma +++ b/matita/matita/contribs/lambdadelta/basic_2/relocation/cpy_lift.ma @@ -20,10 +20,10 @@ include "basic_2/relocation/cpy.ma". (* Properties on relocation *************************************************) (* Basic_1: was: subst1_lift_lt *) -lemma cpy_lift_le: ∀G,K,T1,T2,dt,et. ⦃G, K⦄ ⊢ T1 ▶×[dt, et] T2 → +lemma cpy_lift_le: ∀G,K,T1,T2,dt,et. ⦃G, K⦄ ⊢ T1 ▶[dt, et] T2 → ∀L,U1,U2,s,d,e. ⇩[s, d, e] L ≡ K → ⇧[d, e] T1 ≡ U1 → ⇧[d, e] T2 ≡ U2 → - dt + et ≤ d → ⦃G, L⦄ ⊢ U1 ▶×[dt, et] U2. + dt + et ≤ d → ⦃G, L⦄ ⊢ U1 ▶[dt, et] U2. #G #K #T1 #T2 #dt #et #H elim H -G -K -T1 -T2 -dt -et [ #I #G #K #dt #et #L #U1 #U2 #s #d #e #_ #H1 #H2 #_ >(lift_mono … H1 … H2) -H1 -H2 // @@ -46,10 +46,10 @@ lemma cpy_lift_le: ∀G,K,T1,T2,dt,et. ⦃G, K⦄ ⊢ T1 ▶×[dt, et] T2 → ] qed-. -lemma cpy_lift_be: ∀G,K,T1,T2,dt,et. ⦃G, K⦄ ⊢ T1 ▶×[dt, et] T2 → +lemma cpy_lift_be: ∀G,K,T1,T2,dt,et. ⦃G, K⦄ ⊢ T1 ▶[dt, et] T2 → ∀L,U1,U2,s,d,e. ⇩[s, d, e] L ≡ K → ⇧[d, e] T1 ≡ U1 → ⇧[d, e] T2 ≡ U2 → - dt ≤ d → d ≤ dt + et → ⦃G, L⦄ ⊢ U1 ▶×[dt, et + e] U2. + dt ≤ d → d ≤ dt + et → ⦃G, L⦄ ⊢ U1 ▶[dt, et + e] U2. #G #K #T1 #T2 #dt #et #H elim H -G -K -T1 -T2 -dt -et [ #I #G #K #dt #et #L #U1 #U2 #s #d #e #_ #H1 #H2 #_ #_ >(lift_mono … H1 … H2) -H1 -H2 // @@ -80,10 +80,10 @@ lemma cpy_lift_be: ∀G,K,T1,T2,dt,et. ⦃G, K⦄ ⊢ T1 ▶×[dt, et] T2 → qed-. (* Basic_1: was: subst1_lift_ge *) -lemma cpy_lift_ge: ∀G,K,T1,T2,dt,et. ⦃G, K⦄ ⊢ T1 ▶×[dt, et] T2 → +lemma cpy_lift_ge: ∀G,K,T1,T2,dt,et. ⦃G, K⦄ ⊢ T1 ▶[dt, et] T2 → ∀L,U1,U2,s,d,e. ⇩[s, d, e] L ≡ K → ⇧[d, e] T1 ≡ U1 → ⇧[d, e] T2 ≡ U2 → - d ≤ dt → ⦃G, L⦄ ⊢ U1 ▶×[dt+e, et] U2. + d ≤ dt → ⦃G, L⦄ ⊢ U1 ▶[dt+e, et] U2. #G #K #T1 #T2 #dt #et #H elim H -G -K -T1 -T2 -dt -et [ #I #G #K #dt #et #L #U1 #U2 #s #d #e #_ #H1 #H2 #_ >(lift_mono … H1 … H2) -H1 -H2 // @@ -108,10 +108,10 @@ qed-. (* Inversion lemmas on relocation *******************************************) (* Basic_1: was: subst1_gen_lift_lt *) -lemma cpy_inv_lift1_le: ∀G,L,U1,U2,dt,et. ⦃G, L⦄ ⊢ U1 ▶×[dt, et] U2 → +lemma cpy_inv_lift1_le: ∀G,L,U1,U2,dt,et. ⦃G, L⦄ ⊢ U1 ▶[dt, et] U2 → ∀K,s,d,e. ⇩[s, d, e] L ≡ K → ∀T1. ⇧[d, e] T1 ≡ U1 → dt + et ≤ d → - ∃∃T2. ⦃G, K⦄ ⊢ T1 ▶×[dt, et] T2 & ⇧[d, e] T2 ≡ U2. + ∃∃T2. ⦃G, K⦄ ⊢ T1 ▶[dt, et] T2 & ⇧[d, e] T2 ≡ U2. #G #L #U1 #U2 #dt #et #H elim H -G -L -U1 -U2 -dt -et [ * #i #G #L #dt #et #K #s #d #e #_ #T1 #H #_ [ lapply (lift_inv_sort2 … H) -H #H destruct /2 width=3 by ex2_intro/ @@ -137,10 +137,10 @@ lemma cpy_inv_lift1_le: ∀G,L,U1,U2,dt,et. ⦃G, L⦄ ⊢ U1 ▶×[dt, et] U2 ] qed-. -lemma cpy_inv_lift1_be: ∀G,L,U1,U2,dt,et. ⦃G, L⦄ ⊢ U1 ▶×[dt, et] U2 → +lemma cpy_inv_lift1_be: ∀G,L,U1,U2,dt,et. ⦃G, L⦄ ⊢ U1 ▶[dt, et] U2 → ∀K,s,d,e. ⇩[s, d, e] L ≡ K → ∀T1. ⇧[d, e] T1 ≡ U1 → dt ≤ d → yinj d + e ≤ dt + et → - ∃∃T2. ⦃G, K⦄ ⊢ T1 ▶×[dt, et-e] T2 & ⇧[d, e] T2 ≡ U2. + ∃∃T2. ⦃G, K⦄ ⊢ T1 ▶[dt, et-e] T2 & ⇧[d, e] T2 ≡ U2. #G #L #U1 #U2 #dt #et #H elim H -G -L -U1 -U2 -dt -et [ * #i #G #L #dt #et #K #s #d #e #_ #T1 #H #_ #_ [ lapply (lift_inv_sort2 … H) -H #H destruct /2 width=3 by ex2_intro/ @@ -177,10 +177,10 @@ lemma cpy_inv_lift1_be: ∀G,L,U1,U2,dt,et. ⦃G, L⦄ ⊢ U1 ▶×[dt, et] U2 qed-. (* Basic_1: was: subst1_gen_lift_ge *) -lemma cpy_inv_lift1_ge: ∀G,L,U1,U2,dt,et. ⦃G, L⦄ ⊢ U1 ▶×[dt, et] U2 → +lemma cpy_inv_lift1_ge: ∀G,L,U1,U2,dt,et. ⦃G, L⦄ ⊢ U1 ▶[dt, et] U2 → ∀K,s,d,e. ⇩[s, d, e] L ≡ K → ∀T1. ⇧[d, e] T1 ≡ U1 → yinj d + e ≤ dt → - ∃∃T2. ⦃G, K⦄ ⊢ T1 ▶×[dt-e, et] T2 & ⇧[d, e] T2 ≡ U2. + ∃∃T2. ⦃G, K⦄ ⊢ T1 ▶[dt-e, et] T2 & ⇧[d, e] T2 ≡ U2. #G #L #U1 #U2 #dt #et #H elim H -G -L -U1 -U2 -dt -et [ * #i #G #L #dt #et #K #s #d #e #_ #T1 #H #_ [ lapply (lift_inv_sort2 … H) -H #H destruct /2 width=3 by ex2_intro/ @@ -214,10 +214,10 @@ qed-. (* Advancd inversion lemmas on relocation ***********************************) -lemma cpy_inv_lift1_ge_up: ∀G,L,U1,U2,dt,et. ⦃G, L⦄ ⊢ U1 ▶×[dt, et] U2 → +lemma cpy_inv_lift1_ge_up: ∀G,L,U1,U2,dt,et. ⦃G, L⦄ ⊢ U1 ▶[dt, et] U2 → ∀K,s,d,e. ⇩[s, d, e] L ≡ K → ∀T1. ⇧[d, e] T1 ≡ U1 → d ≤ dt → dt ≤ yinj d + e → yinj d + e ≤ dt + et → - ∃∃T2. ⦃G, K⦄ ⊢ T1 ▶×[d, dt + et - (yinj d + e)] T2 & ⇧[d, e] T2 ≡ U2. + ∃∃T2. ⦃G, K⦄ ⊢ T1 ▶[d, dt + et - (yinj d + e)] T2 & ⇧[d, e] T2 ≡ U2. #G #L #U1 #U2 #dt #et #HU12 #K #s #d #e #HLK #T1 #HTU1 #Hddt #Hdtde #Hdedet elim (cpy_split_up … HU12 (d + e)) -HU12 // -Hdedet #U #HU1 #HU2 lapply (cpy_weak … HU1 d e ? ?) -HU1 // [ >ymax_pre_sn_comm // ] -Hddt -Hdtde #HU1 @@ -225,20 +225,20 @@ lapply (cpy_inv_lift1_eq … HTU1 … HU1) -HU1 #HU1 destruct elim (cpy_inv_lift1_ge … HU2 … HLK … HTU1) -U -L /2 width=3 by ex2_intro/ qed-. -lemma cpy_inv_lift1_be_up: ∀G,L,U1,U2,dt,et. ⦃G, L⦄ ⊢ U1 ▶×[dt, et] U2 → +lemma cpy_inv_lift1_be_up: ∀G,L,U1,U2,dt,et. ⦃G, L⦄ ⊢ U1 ▶[dt, et] U2 → ∀K,s,d,e. ⇩[s, d, e] L ≡ K → ∀T1. ⇧[d, e] T1 ≡ U1 → dt ≤ d → dt + et ≤ yinj d + e → - ∃∃T2. ⦃G, K⦄ ⊢ T1 ▶×[dt, d-dt] T2 & ⇧[d, e] T2 ≡ U2. + ∃∃T2. ⦃G, K⦄ ⊢ T1 ▶[dt, d-dt] T2 & ⇧[d, e] T2 ≡ U2. #G #L #U1 #U2 #dt #et #HU12 #K #s #d #e #HLK #T1 #HTU1 #Hdtd #Hdetde lapply (cpy_weak … HU12 dt (d+e-dt) ? ?) -HU12 // [ >ymax_pre_sn_comm /2 width=1 by yle_plus_dx1_trans/ ] -Hdetde #HU12 elim (cpy_inv_lift1_be … HU12 … HLK … HTU1) -U1 -L /2 width=3 by ex2_intro/ qed-. -lemma cpy_inv_lift1_le_up: ∀G,L,U1,U2,dt,et. ⦃G, L⦄ ⊢ U1 ▶×[dt, et] U2 → +lemma cpy_inv_lift1_le_up: ∀G,L,U1,U2,dt,et. ⦃G, L⦄ ⊢ U1 ▶[dt, et] U2 → ∀K,s,d,e. ⇩[s, d, e] L ≡ K → ∀T1. ⇧[d, e] T1 ≡ U1 → dt ≤ d → d ≤ dt + et → dt + et ≤ yinj d + e → - ∃∃T2. ⦃G, K⦄ ⊢ T1 ▶×[dt, d - dt] T2 & ⇧[d, e] T2 ≡ U2. + ∃∃T2. ⦃G, K⦄ ⊢ T1 ▶[dt, d - dt] T2 & ⇧[d, e] T2 ≡ U2. #G #L #U1 #U2 #dt #et #HU12 #K #s #d #e #HLK #T1 #HTU1 #Hdtd #Hddet #Hdetde elim (cpy_split_up … HU12 d) -HU12 // #U #HU1 #HU2 elim (cpy_inv_lift1_le … HU1 … HLK … HTU1) -U1 diff --git a/matita/matita/contribs/lambdadelta/basic_2/substitution/cpys.ma b/matita/matita/contribs/lambdadelta/basic_2/substitution/cpys.ma index 3aae4505c..422c56878 100644 --- a/matita/matita/contribs/lambdadelta/basic_2/substitution/cpys.ma +++ b/matita/matita/contribs/lambdadelta/basic_2/substitution/cpys.ma @@ -12,7 +12,7 @@ (* *) (**************************************************************************) -include "basic_2/notation/relations/extpsubststar_6.ma". +include "basic_2/notation/relations/psubststar_6.ma". include "basic_2/relocation/cpy.ma". (* CONTEXT-SENSITIVE EXTENDED MULTIPLE SUBSTITUTION FOR TERMS ***************) @@ -21,35 +21,35 @@ definition cpys: ynat → ynat → relation4 genv lenv term term ≝ λd,e,G. LTC … (cpy d e G). interpretation "context-sensitive extended multiple substritution (term)" - 'ExtPSubstStar G L T1 d e T2 = (cpys d e G L T1 T2). + 'PSubstStar G L T1 d e T2 = (cpys d e G L T1 T2). (* Basic eliminators ********************************************************) lemma cpys_ind: ∀G,L,T1,d,e. ∀R:predicate term. R T1 → - (∀T,T2. ⦃G, L⦄ ⊢ T1 ▶*×[d, e] T → ⦃G, L⦄ ⊢ T ▶×[d, e] T2 → R T → R T2) → - ∀T2. ⦃G, L⦄ ⊢ T1 ▶*×[d, e] T2 → R T2. + (∀T,T2. ⦃G, L⦄ ⊢ T1 ▶*[d, e] T → ⦃G, L⦄ ⊢ T ▶[d, e] T2 → R T → R T2) → + ∀T2. ⦃G, L⦄ ⊢ T1 ▶*[d, e] T2 → R T2. #G #L #T1 #d #e #R #HT1 #IHT1 #T2 #HT12 @(TC_star_ind … HT1 IHT1 … HT12) // qed-. lemma cpys_ind_dx: ∀G,L,T2,d,e. ∀R:predicate term. R T2 → - (∀T1,T. ⦃G, L⦄ ⊢ T1 ▶×[d, e] T → ⦃G, L⦄ ⊢ T ▶*×[d, e] T2 → R T → R T1) → - ∀T1. ⦃G, L⦄ ⊢ T1 ▶*×[d, e] T2 → R T1. + (∀T1,T. ⦃G, L⦄ ⊢ T1 ▶[d, e] T → ⦃G, L⦄ ⊢ T ▶*[d, e] T2 → R T → R T1) → + ∀T1. ⦃G, L⦄ ⊢ T1 ▶*[d, e] T2 → R T1. #G #L #T2 #d #e #R #HT2 #IHT2 #T1 #HT12 @(TC_star_ind_dx … HT2 IHT2 … HT12) // qed-. (* Basic properties *********************************************************) -lemma cpy_cpys: ∀G,L,T1,T2,d,e. ⦃G, L⦄ ⊢ T1 ▶×[d, e] T2 → ⦃G, L⦄ ⊢ T1 ▶*×[d, e] T2. +lemma cpy_cpys: ∀G,L,T1,T2,d,e. ⦃G, L⦄ ⊢ T1 ▶[d, e] T2 → ⦃G, L⦄ ⊢ T1 ▶*[d, e] T2. /2 width=1 by inj/ qed. lemma cpys_strap1: ∀G,L,T1,T,T2,d,e. - ⦃G, L⦄ ⊢ T1 ▶*×[d, e] T → ⦃G, L⦄ ⊢ T ▶×[d, e] T2 → ⦃G, L⦄ ⊢ T1 ▶*×[d, e] T2. + ⦃G, L⦄ ⊢ T1 ▶*[d, e] T → ⦃G, L⦄ ⊢ T ▶[d, e] T2 → ⦃G, L⦄ ⊢ T1 ▶*[d, e] T2. normalize /2 width=3 by step/ qed-. lemma cpys_strap2: ∀G,L,T1,T,T2,d,e. - ⦃G, L⦄ ⊢ T1 ▶×[d, e] T → ⦃G, L⦄ ⊢ T ▶*×[d, e] T2 → ⦃G, L⦄ ⊢ T1 ▶*×[d, e] T2. + ⦃G, L⦄ ⊢ T1 ▶[d, e] T → ⦃G, L⦄ ⊢ T ▶*[d, e] T2 → ⦃G, L⦄ ⊢ T1 ▶*[d, e] T2. normalize /2 width=3 by TC_strap/ qed-. lemma lsuby_cpys_trans: ∀G,d,e. lsub_trans … (cpys d e G) (lsuby d e). @@ -59,46 +59,46 @@ qed-. lemma cpys_refl: ∀G,L,d,e. reflexive … (cpys d e G L). /2 width=1 by cpy_cpys/ qed. -lemma cpys_bind: ∀G,L,V1,V2,d,e. ⦃G, L⦄ ⊢ V1 ▶*×[d, e] V2 → - ∀I,T1,T2. ⦃G, L.ⓑ{I}V1⦄ ⊢ T1 ▶*×[⫯d, e] T2 → - ∀a. ⦃G, L⦄ ⊢ ⓑ{a,I}V1.T1 ▶*×[d, e] ⓑ{a,I}V2.T2. +lemma cpys_bind: ∀G,L,V1,V2,d,e. ⦃G, L⦄ ⊢ V1 ▶*[d, e] V2 → + ∀I,T1,T2. ⦃G, L.ⓑ{I}V1⦄ ⊢ T1 ▶*[⫯d, e] T2 → + ∀a. ⦃G, L⦄ ⊢ ⓑ{a,I}V1.T1 ▶*[d, e] ⓑ{a,I}V2.T2. #G #L #V1 #V2 #d #e #HV12 @(cpys_ind … HV12) -V2 [ #I #T1 #T2 #HT12 @(cpys_ind … HT12) -T2 /3 width=5 by cpys_strap1, cpy_bind/ | /3 width=5 by cpys_strap1, cpy_bind/ ] qed. -lemma cpys_flat: ∀G,L,V1,V2,d,e. ⦃G, L⦄ ⊢ V1 ▶*×[d, e] V2 → - ∀T1,T2. ⦃G, L⦄ ⊢ T1 ▶*×[d, e] T2 → - ∀I. ⦃G, L⦄ ⊢ ⓕ{I}V1.T1 ▶*×[d, e] ⓕ{I}V2.T2. +lemma cpys_flat: ∀G,L,V1,V2,d,e. ⦃G, L⦄ ⊢ V1 ▶*[d, e] V2 → + ∀T1,T2. ⦃G, L⦄ ⊢ T1 ▶*[d, e] T2 → + ∀I. ⦃G, L⦄ ⊢ ⓕ{I}V1.T1 ▶*[d, e] ⓕ{I}V2.T2. #G #L #V1 #V2 #d #e #HV12 @(cpys_ind … HV12) -V2 [ #T1 #T2 #HT12 @(cpys_ind … HT12) -T2 /3 width=5 by cpys_strap1, cpy_flat/ | /3 width=5 by cpys_strap1, cpy_flat/ qed. -lemma cpys_weak: ∀G,L,T1,T2,d1,e1. ⦃G, L⦄ ⊢ T1 ▶*×[d1, e1] T2 → +lemma cpys_weak: ∀G,L,T1,T2,d1,e1. ⦃G, L⦄ ⊢ T1 ▶*[d1, e1] T2 → ∀d2,e2. d2 ≤ d1 → d1 + e1 ≤ d2 + e2 → - ⦃G, L⦄ ⊢ T1 ▶*×[d2, e2] T2. + ⦃G, L⦄ ⊢ T1 ▶*[d2, e2] T2. #G #L #T1 #T2 #d1 #e1 #H #d1 #d2 #Hd21 #Hde12 @(cpys_ind … H) -T2 /3 width=7 by cpys_strap1, cpy_weak/ qed-. lemma cpys_weak_top: ∀G,L,T1,T2,d,e. - ⦃G, L⦄ ⊢ T1 ▶*×[d, e] T2 → ⦃G, L⦄ ⊢ T1 ▶*×[d, |L| - d] T2. + ⦃G, L⦄ ⊢ T1 ▶*[d, e] T2 → ⦃G, L⦄ ⊢ T1 ▶*[d, |L| - d] T2. #G #L #T1 #T2 #d #e #H @(cpys_ind … H) -T2 /3 width=4 by cpys_strap1, cpy_weak_top/ qed-. lemma cpys_weak_full: ∀G,L,T1,T2,d,e. - ⦃G, L⦄ ⊢ T1 ▶*×[d, e] T2 → ⦃G, L⦄ ⊢ T1 ▶*×[0, |L|] T2. + ⦃G, L⦄ ⊢ T1 ▶*[d, e] T2 → ⦃G, L⦄ ⊢ T1 ▶*[0, |L|] T2. #G #L #T1 #T2 #d #e #H @(cpys_ind … H) -T2 /3 width=5 by cpys_strap1, cpy_weak_full/ qed-. -lemma cpys_up: ∀G,L,U1,U2,dt,et. ⦃G, L⦄ ⊢ U1 ▶*×[dt, et] U2 → +lemma cpys_up: ∀G,L,U1,U2,dt,et. ⦃G, L⦄ ⊢ U1 ▶*[dt, et] U2 → ∀T1,d,e. ⇧[d, e] T1 ≡ U1 → d ≤ dt → d + e ≤ dt + et → - ∃∃T2. ⦃G, L⦄ ⊢ U1 ▶*×[d+e, dt+et-(d+e)] U2 & ⇧[d, e] T2 ≡ U2. + ∃∃T2. ⦃G, L⦄ ⊢ U1 ▶*[d+e, dt+et-(d+e)] U2 & ⇧[d, e] T2 ≡ U2. #G #L #U1 #U2 #dt #et #H #T1 #d #e #HTU1 #Hddt #Hdedet @(cpys_ind … H) -U2 [ /2 width=3 by ex2_intro/ | -HTU1 #U #U2 #_ #HU2 * #T #HU1 #HTU @@ -114,22 +114,22 @@ qed-. (* Basic inversion lemmas ***************************************************) (* Note: this can be derived from cpys_inv_atom1 *) -lemma cpys_inv_sort1: ∀G,L,T2,k,d,e. ⦃G, L⦄ ⊢ ⋆k ▶*×[d, e] T2 → T2 = ⋆k. +lemma cpys_inv_sort1: ∀G,L,T2,k,d,e. ⦃G, L⦄ ⊢ ⋆k ▶*[d, e] T2 → T2 = ⋆k. #G #L #T2 #k #d #e #H @(cpys_ind … H) -T2 // #T #T2 #_ #HT2 #IHT1 destruct >(cpy_inv_sort1 … HT2) -HT2 // qed-. (* Note: this can be derived from cpys_inv_atom1 *) -lemma cpys_inv_gref1: ∀G,L,T2,p,d,e. ⦃G, L⦄ ⊢ §p ▶*×[d, e] T2 → T2 = §p. +lemma cpys_inv_gref1: ∀G,L,T2,p,d,e. ⦃G, L⦄ ⊢ §p ▶*[d, e] T2 → T2 = §p. #G #L #T2 #p #d #e #H @(cpys_ind … H) -T2 // #T #T2 #_ #HT2 #IHT1 destruct >(cpy_inv_gref1 … HT2) -HT2 // qed-. -lemma cpys_inv_bind1: ∀a,I,G,L,V1,T1,U2,d,e. ⦃G, L⦄ ⊢ ⓑ{a,I}V1.T1 ▶*×[d, e] U2 → - ∃∃V2,T2. ⦃G, L⦄ ⊢ V1 ▶*×[d, e] V2 & - ⦃G, L.ⓑ{I}V1⦄ ⊢ T1 ▶*×[⫯d, e] T2 & +lemma cpys_inv_bind1: ∀a,I,G,L,V1,T1,U2,d,e. ⦃G, L⦄ ⊢ ⓑ{a,I}V1.T1 ▶*[d, e] U2 → + ∃∃V2,T2. ⦃G, L⦄ ⊢ V1 ▶*[d, e] V2 & + ⦃G, L.ⓑ{I}V1⦄ ⊢ T1 ▶*[⫯d, e] T2 & U2 = ⓑ{a,I}V2.T2. #a #I #G #L #V1 #T1 #U2 #d #e #H @(cpys_ind … H) -U2 [ /2 width=5 by ex3_2_intro/ @@ -140,8 +140,8 @@ lemma cpys_inv_bind1: ∀a,I,G,L,V1,T1,U2,d,e. ⦃G, L⦄ ⊢ ⓑ{a,I}V1.T1 ▶* ] qed-. -lemma cpys_inv_flat1: ∀I,G,L,V1,T1,U2,d,e. ⦃G, L⦄ ⊢ ⓕ{I}V1.T1 ▶*×[d, e] U2 → - ∃∃V2,T2. ⦃G, L⦄ ⊢ V1 ▶*×[d, e] V2 & ⦃G, L⦄ ⊢ T1 ▶*×[d, e] T2 & +lemma cpys_inv_flat1: ∀I,G,L,V1,T1,U2,d,e. ⦃G, L⦄ ⊢ ⓕ{I}V1.T1 ▶*[d, e] U2 → + ∃∃V2,T2. ⦃G, L⦄ ⊢ V1 ▶*[d, e] V2 & ⦃G, L⦄ ⊢ T1 ▶*[d, e] T2 & U2 = ⓕ{I}V2.T2. #I #G #L #V1 #T1 #U2 #d #e #H @(cpys_ind … H) -U2 [ /2 width=5 by ex3_2_intro/ @@ -151,26 +151,26 @@ lemma cpys_inv_flat1: ∀I,G,L,V1,T1,U2,d,e. ⦃G, L⦄ ⊢ ⓕ{I}V1.T1 ▶*×[d ] qed-. -lemma cpys_inv_refl_O2: ∀G,L,T1,T2,d. ⦃G, L⦄ ⊢ T1 ▶*×[d, 0] T2 → T1 = T2. +lemma cpys_inv_refl_O2: ∀G,L,T1,T2,d. ⦃G, L⦄ ⊢ T1 ▶*[d, 0] T2 → T1 = T2. #G #L #T1 #T2 #d #H @(cpys_ind … H) -T2 // #T #T2 #_ #HT2 #IHT1 <(cpy_inv_refl_O2 … HT2) -HT2 // qed-. lemma cpys_inv_lift1_eq: ∀G,L,U1,U2. ∀d,e:nat. - ⦃G, L⦄ ⊢ U1 ▶*×[d, e] U2 → ∀T1. ⇧[d, e] T1 ≡ U1 → U1 = U2. + ⦃G, L⦄ ⊢ U1 ▶*[d, e] U2 → ∀T1. ⇧[d, e] T1 ≡ U1 → U1 = U2. #G #L #U1 #U2 #d #e #H #T1 #HTU1 @(cpys_ind … H) -U2 /2 width=7 by cpy_inv_lift1_eq/ qed-. (* Basic forward lemmas *****************************************************) -lemma cpys_fwd_tw: ∀G,L,T1,T2,d,e. ⦃G, L⦄ ⊢ T1 ▶*×[d, e] T2 → ♯{T1} ≤ ♯{T2}. +lemma cpys_fwd_tw: ∀G,L,T1,T2,d,e. ⦃G, L⦄ ⊢ T1 ▶*[d, e] T2 → ♯{T1} ≤ ♯{T2}. #G #L #T1 #T2 #d #e #H @(cpys_ind … H) -T2 // #T #T2 #_ #HT2 #IHT1 lapply (cpy_fwd_tw … HT2) -HT2 /2 width=3 by transitive_le/ qed-. -lemma cpys_fwd_shift1: ∀G,L,L1,T1,T,d,e. ⦃G, L⦄ ⊢ L1 @@ T1 ▶*×[d, e] T → +lemma cpys_fwd_shift1: ∀G,L,L1,T1,T,d,e. ⦃G, L⦄ ⊢ L1 @@ T1 ▶*[d, e] T → ∃∃L2,T2. |L1| = |L2| & T = L2 @@ T2. #G #L #L1 #T1 #T #d #e #H @(cpys_ind … H) -T [ /2 width=4 by ex2_2_intro/ diff --git a/matita/matita/contribs/lambdadelta/basic_2/substitution/cpys_alt.ma b/matita/matita/contribs/lambdadelta/basic_2/substitution/cpys_alt.ma index 746b5c4f4..02f291022 100644 --- a/matita/matita/contribs/lambdadelta/basic_2/substitution/cpys_alt.ma +++ b/matita/matita/contribs/lambdadelta/basic_2/substitution/cpys_alt.ma @@ -12,7 +12,7 @@ (* *) (**************************************************************************) -include "basic_2/notation/relations/extpsubststaralt_6.ma". +include "basic_2/notation/relations/psubststaralt_6.ma". include "basic_2/substitution/cpys_lift.ma". (* CONTEXT-SENSITIVE EXTENDED MULTIPLE SUBSTITUTION FOR TERMS ***************) @@ -33,7 +33,7 @@ inductive cpysa: ynat → ynat → relation4 genv lenv term term ≝ interpretation "context-sensitive extended multiple substritution (term) alternative" - 'ExtPSubstStarAlt G L T1 d e T2 = (cpysa d e G L T1 T2). + 'PSubstStarAlt G L T1 d e T2 = (cpysa d e G L T1 T2). (* Basic properties *********************************************************) @@ -47,13 +47,13 @@ lemma lsuby_cpysa_trans: ∀G,d,e. lsub_trans … (cpysa d e G) (lsuby d e). ] qed-. -lemma cpysa_refl: ∀G,T,L,d,e. ⦃G, L⦄ ⊢ T ▶▶*×[d, e] T. +lemma cpysa_refl: ∀G,T,L,d,e. ⦃G, L⦄ ⊢ T ▶▶*[d, e] T. #G #T elim T -T // #I elim I -I /2 width=1 by cpysa_bind, cpysa_flat/ qed. -lemma cpysa_cpy_trans: ∀G,L,T1,T,d,e. ⦃G, L⦄ ⊢ T1 ▶▶*×[d, e] T → - ∀T2. ⦃G, L⦄ ⊢ T ▶×[d, e] T2 → ⦃G, L⦄ ⊢ T1 ▶▶*×[d, e] T2. +lemma cpysa_cpy_trans: ∀G,L,T1,T,d,e. ⦃G, L⦄ ⊢ T1 ▶▶*[d, e] T → + ∀T2. ⦃G, L⦄ ⊢ T ▶[d, e] T2 → ⦃G, L⦄ ⊢ T1 ▶▶*[d, e] T2. #G #L #T1 #T #d #e #H elim H -G -L -T1 -T -d -e [ #I #G #L #d #e #X #H elim (cpy_inv_atom1 … H) -H // * /2 width=7 by cpysa_subst/ @@ -70,12 +70,12 @@ lemma cpysa_cpy_trans: ∀G,L,T1,T,d,e. ⦃G, L⦄ ⊢ T1 ▶▶*×[d, e] T → ] qed-. -lemma cpys_cpysa: ∀G,L,T1,T2,d,e. ⦃G, L⦄ ⊢ T1 ▶*×[d, e] T2 → ⦃G, L⦄ ⊢ T1 ▶▶*×[d, e] T2. +lemma cpys_cpysa: ∀G,L,T1,T2,d,e. ⦃G, L⦄ ⊢ T1 ▶*[d, e] T2 → ⦃G, L⦄ ⊢ T1 ▶▶*[d, e] T2. /3 width=8 by cpysa_cpy_trans, cpys_ind/ qed. (* Basic inversion lemmas ***************************************************) -lemma cpysa_cpys: ∀G,L,T1,T2,d,e. ⦃G, L⦄ ⊢ T1 ▶▶*×[d, e] T2 → ⦃G, L⦄ ⊢ T1 ▶*×[d, e] T2. +lemma cpysa_cpys: ∀G,L,T1,T2,d,e. ⦃G, L⦄ ⊢ T1 ▶▶*[d, e] T2 → ⦃G, L⦄ ⊢ T1 ▶*[d, e] T2. #G #L #T1 #T2 #d #e #H elim H -G -L -T1 -T2 -d -e /2 width=7 by cpys_subst, cpys_flat, cpys_bind, cpy_cpys/ qed-. @@ -83,18 +83,18 @@ qed-. lemma cpys_ind_alt: ∀R:ynat→ynat→relation4 genv lenv term term. (∀I,G,L,d,e. R d e G L (⓪{I}) (⓪{I})) → (∀I,G,L,K,V1,V2,W2,i,d,e. d ≤ yinj i → i < d + e → - ⇩[i] L ≡ K.ⓑ{I}V1 → ⦃G, K⦄ ⊢ V1 ▶*×[O, ⫰(d+e-i)] V2 → + ⇩[i] L ≡ K.ⓑ{I}V1 → ⦃G, K⦄ ⊢ V1 ▶*[O, ⫰(d+e-i)] V2 → ⇧[O, i+1] V2 ≡ W2 → R O (⫰(d+e-i)) G K V1 V2 → R d e G L (#i) W2 ) → - (∀a,I,G,L,V1,V2,T1,T2,d,e. ⦃G, L⦄ ⊢ V1 ▶*×[d, e] V2 → - ⦃G, L.ⓑ{I}V1⦄ ⊢ T1 ▶*×[⫯d, e] T2 → R d e G L V1 V2 → + (∀a,I,G,L,V1,V2,T1,T2,d,e. ⦃G, L⦄ ⊢ V1 ▶*[d, e] V2 → + ⦃G, L.ⓑ{I}V1⦄ ⊢ T1 ▶*[⫯d, e] T2 → R d e G L V1 V2 → R (⫯d) e G (L.ⓑ{I}V1) T1 T2 → R d e G L (ⓑ{a,I}V1.T1) (ⓑ{a,I}V2.T2) ) → - (∀I,G,L,V1,V2,T1,T2,d,e. ⦃G, L⦄ ⊢ V1 ▶*×[d, e] V2 → - ⦃G, L⦄ ⊢ T1 ▶*×[d, e] T2 → R d e G L V1 V2 → + (∀I,G,L,V1,V2,T1,T2,d,e. ⦃G, L⦄ ⊢ V1 ▶*[d, e] V2 → + ⦃G, L⦄ ⊢ T1 ▶*[d, e] T2 → R d e G L V1 V2 → R d e G L T1 T2 → R d e G L (ⓕ{I}V1.T1) (ⓕ{I}V2.T2) ) → - ∀d,e,G,L,T1,T2. ⦃G, L⦄ ⊢ T1 ▶*×[d, e] T2 → R d e G L T1 T2. + ∀d,e,G,L,T1,T2. ⦃G, L⦄ ⊢ T1 ▶*[d, e] T2 → R d e G L T1 T2. #R #H1 #H2 #H3 #H4 #d #e #G #L #T1 #T2 #H elim (cpys_cpysa … H) -G -L -T1 -T2 -d -e /3 width=8 by cpysa_cpys/ qed-. diff --git a/matita/matita/contribs/lambdadelta/basic_2/substitution/cpys_cpys.ma b/matita/matita/contribs/lambdadelta/basic_2/substitution/cpys_cpys.ma index a3eedc255..52759ca7f 100644 --- a/matita/matita/contribs/lambdadelta/basic_2/substitution/cpys_cpys.ma +++ b/matita/matita/contribs/lambdadelta/basic_2/substitution/cpys_cpys.ma @@ -19,36 +19,36 @@ include "basic_2/substitution/cpys_alt.ma". (* Advanced inversion lemmas ************************************************) -lemma cpys_inv_SO2: ∀G,L,T1,T2,d. ⦃G, L⦄ ⊢ T1 ▶*×[d, 1] T2 → ⦃G, L⦄ ⊢ T1 ▶×[d, 1] T2. +lemma cpys_inv_SO2: ∀G,L,T1,T2,d. ⦃G, L⦄ ⊢ T1 ▶*[d, 1] T2 → ⦃G, L⦄ ⊢ T1 ▶[d, 1] T2. #G #L #T1 #T2 #d #H @(cpys_ind … H) -T2 /2 width=3 by cpy_trans_ge/ qed-. (* Advanced properties ******************************************************) -lemma cpys_strip_eq: ∀G,L,T0,T1,d1,e1. ⦃G, L⦄ ⊢ T0 ▶*×[d1, e1] T1 → - ∀T2,d2,e2. ⦃G, L⦄ ⊢ T0 ▶×[d2, e2] T2 → - ∃∃T. ⦃G, L⦄ ⊢ T1 ▶×[d2, e2] T & ⦃G, L⦄ ⊢ T2 ▶*×[d1, e1] T. +lemma cpys_strip_eq: ∀G,L,T0,T1,d1,e1. ⦃G, L⦄ ⊢ T0 ▶*[d1, e1] T1 → + ∀T2,d2,e2. ⦃G, L⦄ ⊢ T0 ▶[d2, e2] T2 → + ∃∃T. ⦃G, L⦄ ⊢ T1 ▶[d2, e2] T & ⦃G, L⦄ ⊢ T2 ▶*[d1, e1] T. normalize /3 width=3 by cpy_conf_eq, TC_strip1/ qed-. -lemma cpys_strip_neq: ∀G,L1,T0,T1,d1,e1. ⦃G, L1⦄ ⊢ T0 ▶*×[d1, e1] T1 → - ∀L2,T2,d2,e2. ⦃G, L2⦄ ⊢ T0 ▶×[d2, e2] T2 → +lemma cpys_strip_neq: ∀G,L1,T0,T1,d1,e1. ⦃G, L1⦄ ⊢ T0 ▶*[d1, e1] T1 → + ∀L2,T2,d2,e2. ⦃G, L2⦄ ⊢ T0 ▶[d2, e2] T2 → (d1 + e1 ≤ d2 ∨ d2 + e2 ≤ d1) → - ∃∃T. ⦃G, L2⦄ ⊢ T1 ▶×[d2, e2] T & ⦃G, L1⦄ ⊢ T2 ▶*×[d1, e1] T. + ∃∃T. ⦃G, L2⦄ ⊢ T1 ▶[d2, e2] T & ⦃G, L1⦄ ⊢ T2 ▶*[d1, e1] T. normalize /3 width=3 by cpy_conf_neq, TC_strip1/ qed-. -lemma cpys_strap1_down: ∀G,L,T1,T0,d1,e1. ⦃G, L⦄ ⊢ T1 ▶*×[d1, e1] T0 → - ∀T2,d2,e2. ⦃G, L⦄ ⊢ T0 ▶×[d2, e2] T2 → d2 + e2 ≤ d1 → - ∃∃T. ⦃G, L⦄ ⊢ T1 ▶×[d2, e2] T & ⦃G, L⦄ ⊢ T ▶*×[d1, e1] T2. +lemma cpys_strap1_down: ∀G,L,T1,T0,d1,e1. ⦃G, L⦄ ⊢ T1 ▶*[d1, e1] T0 → + ∀T2,d2,e2. ⦃G, L⦄ ⊢ T0 ▶[d2, e2] T2 → d2 + e2 ≤ d1 → + ∃∃T. ⦃G, L⦄ ⊢ T1 ▶[d2, e2] T & ⦃G, L⦄ ⊢ T ▶*[d1, e1] T2. normalize /3 width=3 by cpy_trans_down, TC_strap1/ qed. -lemma cpys_strap2_down: ∀G,L,T1,T0,d1,e1. ⦃G, L⦄ ⊢ T1 ▶×[d1, e1] T0 → - ∀T2,d2,e2. ⦃G, L⦄ ⊢ T0 ▶*×[d2, e2] T2 → d2 + e2 ≤ d1 → - ∃∃T. ⦃G, L⦄ ⊢ T1 ▶*×[d2, e2] T & ⦃G, L⦄ ⊢ T ▶×[d1, e1] T2. +lemma cpys_strap2_down: ∀G,L,T1,T0,d1,e1. ⦃G, L⦄ ⊢ T1 ▶[d1, e1] T0 → + ∀T2,d2,e2. ⦃G, L⦄ ⊢ T0 ▶*[d2, e2] T2 → d2 + e2 ≤ d1 → + ∃∃T. ⦃G, L⦄ ⊢ T1 ▶*[d2, e2] T & ⦃G, L⦄ ⊢ T ▶[d1, e1] T2. normalize /3 width=3 by cpy_trans_down, TC_strap2/ qed-. -lemma cpys_split_up: ∀G,L,T1,T2,d,e. ⦃G, L⦄ ⊢ T1 ▶*×[d, e] T2 → +lemma cpys_split_up: ∀G,L,T1,T2,d,e. ⦃G, L⦄ ⊢ T1 ▶*[d, e] T2 → ∀i. d ≤ i → i ≤ d + e → - ∃∃T. ⦃G, L⦄ ⊢ T1 ▶*×[d, i - d] T & ⦃G, L⦄ ⊢ T ▶*×[i, d + e - i] T2. + ∃∃T. ⦃G, L⦄ ⊢ T1 ▶*[d, i - d] T & ⦃G, L⦄ ⊢ T ▶*[i, d + e - i] T2. #G #L #T1 #T2 #d #e #H #i #Hdi #Hide @(cpys_ind … H) -T2 [ /2 width=3 by ex2_intro/ | #T #T2 #_ #HT12 * #T3 #HT13 #HT3 @@ -58,10 +58,10 @@ lemma cpys_split_up: ∀G,L,T1,T2,d,e. ⦃G, L⦄ ⊢ T1 ▶*×[d, e] T2 → ] qed-. -lemma cpys_inv_lift1_up: ∀G,L,U1,U2,dt,et. ⦃G, L⦄ ⊢ U1 ▶*×[dt, et] U2 → +lemma cpys_inv_lift1_up: ∀G,L,U1,U2,dt,et. ⦃G, L⦄ ⊢ U1 ▶*[dt, et] U2 → ∀K,s,d,e. ⇩[s, d, e] L ≡ K → ∀T1. ⇧[d, e] T1 ≡ U1 → d ≤ dt → dt ≤ yinj d + e → yinj d + e ≤ dt + et → - ∃∃T2. ⦃G, K⦄ ⊢ T1 ▶*×[d, dt + et - (yinj d + e)] T2 & + ∃∃T2. ⦃G, K⦄ ⊢ T1 ▶*[d, dt + et - (yinj d + e)] T2 & ⇧[d, e] T2 ≡ U2. #G #L #U1 #U2 #dt #et #HU12 #K #s #d #e #HLK #T1 #HTU1 #Hddt #Hdtde #Hdedet elim (cpys_split_up … HU12 (d + e)) -HU12 // -Hdedet #U #HU1 #HU2 @@ -73,29 +73,29 @@ qed-. (* Main properties **********************************************************) -theorem cpys_conf_eq: ∀G,L,T0,T1,d1,e1. ⦃G, L⦄ ⊢ T0 ▶*×[d1, e1] T1 → - ∀T2,d2,e2. ⦃G, L⦄ ⊢ T0 ▶*×[d2, e2] T2 → - ∃∃T. ⦃G, L⦄ ⊢ T1 ▶*×[d2, e2] T & ⦃G, L⦄ ⊢ T2 ▶*×[d1, e1] T. +theorem cpys_conf_eq: ∀G,L,T0,T1,d1,e1. ⦃G, L⦄ ⊢ T0 ▶*[d1, e1] T1 → + ∀T2,d2,e2. ⦃G, L⦄ ⊢ T0 ▶*[d2, e2] T2 → + ∃∃T. ⦃G, L⦄ ⊢ T1 ▶*[d2, e2] T & ⦃G, L⦄ ⊢ T2 ▶*[d1, e1] T. normalize /3 width=3 by cpy_conf_eq, TC_confluent2/ qed-. -theorem cpys_conf_neq: ∀G,L1,T0,T1,d1,e1. ⦃G, L1⦄ ⊢ T0 ▶*×[d1, e1] T1 → - ∀L2,T2,d2,e2. ⦃G, L2⦄ ⊢ T0 ▶*×[d2, e2] T2 → +theorem cpys_conf_neq: ∀G,L1,T0,T1,d1,e1. ⦃G, L1⦄ ⊢ T0 ▶*[d1, e1] T1 → + ∀L2,T2,d2,e2. ⦃G, L2⦄ ⊢ T0 ▶*[d2, e2] T2 → (d1 + e1 ≤ d2 ∨ d2 + e2 ≤ d1) → - ∃∃T. ⦃G, L2⦄ ⊢ T1 ▶*×[d2, e2] T & ⦃G, L1⦄ ⊢ T2 ▶*×[d1, e1] T. + ∃∃T. ⦃G, L2⦄ ⊢ T1 ▶*[d2, e2] T & ⦃G, L1⦄ ⊢ T2 ▶*[d1, e1] T. normalize /3 width=3 by cpy_conf_neq, TC_confluent2/ qed-. theorem cpys_trans_eq: ∀G,L,T1,T,T2,d,e. - ⦃G, L⦄ ⊢ T1 ▶*×[d, e] T → ⦃G, L⦄ ⊢ T ▶*×[d, e] T2 → - ⦃G, L⦄ ⊢ T1 ▶*×[d, e] T2. + ⦃G, L⦄ ⊢ T1 ▶*[d, e] T → ⦃G, L⦄ ⊢ T ▶*[d, e] T2 → + ⦃G, L⦄ ⊢ T1 ▶*[d, e] T2. normalize /2 width=3 by trans_TC/ qed-. -theorem cpys_trans_down: ∀G,L,T1,T0,d1,e1. ⦃G, L⦄ ⊢ T1 ▶*×[d1, e1] T0 → - ∀T2,d2,e2. ⦃G, L⦄ ⊢ T0 ▶*×[d2, e2] T2 → d2 + e2 ≤ d1 → - ∃∃T. ⦃G, L⦄ ⊢ T1 ▶*×[d2, e2] T & ⦃G, L⦄ ⊢ T ▶*×[d1, e1] T2. +theorem cpys_trans_down: ∀G,L,T1,T0,d1,e1. ⦃G, L⦄ ⊢ T1 ▶*[d1, e1] T0 → + ∀T2,d2,e2. ⦃G, L⦄ ⊢ T0 ▶*[d2, e2] T2 → d2 + e2 ≤ d1 → + ∃∃T. ⦃G, L⦄ ⊢ T1 ▶*[d2, e2] T & ⦃G, L⦄ ⊢ T ▶*[d1, e1] T2. normalize /3 width=3 by cpy_trans_down, TC_transitive2/ qed-. -theorem cpys_antisym_eq: ∀G,L1,T1,T2,d,e. ⦃G, L1⦄ ⊢ T1 ▶*×[d, e] T2 → - ∀L2. ⦃G, L2⦄ ⊢ T2 ▶*×[d, e] T1 → T1 = T2. +theorem cpys_antisym_eq: ∀G,L1,T1,T2,d,e. ⦃G, L1⦄ ⊢ T1 ▶*[d, e] T2 → + ∀L2. ⦃G, L2⦄ ⊢ T2 ▶*[d, e] T1 → T1 = T2. #G #L1 #T1 #T2 #d #e #H @(cpys_ind_alt … H) -G -L1 -T1 -T2 // [ #I1 #G #L1 #K1 #V1 #V2 #W2 #i #d #e #Hdi #Hide #_ #_ #HVW2 #_ #L2 #HW2 elim (lt_or_ge (|L2|) (i+1)) #Hi [ -Hdi -Hide | ] diff --git a/matita/matita/contribs/lambdadelta/basic_2/substitution/cpys_lift.ma b/matita/matita/contribs/lambdadelta/basic_2/substitution/cpys_lift.ma index 4a621d7d6..eaccf49f7 100644 --- a/matita/matita/contribs/lambdadelta/basic_2/substitution/cpys_lift.ma +++ b/matita/matita/contribs/lambdadelta/basic_2/substitution/cpys_lift.ma @@ -21,8 +21,8 @@ include "basic_2/substitution/cpys.ma". lemma cpys_subst: ∀I,G,L,K,V,U1,i,d,e. d ≤ yinj i → i < d + e → - ⇩[i] L ≡ K.ⓑ{I}V → ⦃G, K⦄ ⊢ V ▶*×[0, ⫰(d+e-i)] U1 → - ∀U2. ⇧[0, i+1] U1 ≡ U2 → ⦃G, L⦄ ⊢ #i ▶*×[d, e] U2. + ⇩[i] L ≡ K.ⓑ{I}V → ⦃G, K⦄ ⊢ V ▶*[0, ⫰(d+e-i)] U1 → + ∀U2. ⇧[0, i+1] U1 ≡ U2 → ⦃G, L⦄ ⊢ #i ▶*[d, e] U2. #I #G #L #K #V #U1 #i #d #e #Hdi #Hide #HLK #H @(cpys_ind … H) -U1 [ /3 width=5 by cpy_cpys, cpy_subst/ | #U #U1 #_ #HU1 #IHU #U2 #HU12 @@ -38,19 +38,19 @@ qed. lemma cpys_subst_Y2: ∀I,G,L,K,V,U1,i,d. d ≤ yinj i → - ⇩[i] L ≡ K.ⓑ{I}V → ⦃G, K⦄ ⊢ V ▶*×[0, ∞] U1 → - ∀U2. ⇧[0, i+1] U1 ≡ U2 → ⦃G, L⦄ ⊢ #i ▶*×[d, ∞] U2. + ⇩[i] L ≡ K.ⓑ{I}V → ⦃G, K⦄ ⊢ V ▶*[0, ∞] U1 → + ∀U2. ⇧[0, i+1] U1 ≡ U2 → ⦃G, L⦄ ⊢ #i ▶*[d, ∞] U2. #I #G #L #K #V #U1 #i #d #Hdi #HLK #HVU1 #U2 #HU12 @(cpys_subst … HLK … HU12) >yminus_Y_inj // qed. (* Advanced inverion lemmas *************************************************) -lemma cpys_inv_atom1: ∀I,G,L,T2,d,e. ⦃G, L⦄ ⊢ ⓪{I} ▶*×[d, e] T2 → +lemma cpys_inv_atom1: ∀I,G,L,T2,d,e. ⦃G, L⦄ ⊢ ⓪{I} ▶*[d, e] T2 → T2 = ⓪{I} ∨ ∃∃J,K,V1,V2,i. d ≤ yinj i & i < d + e & ⇩[i] L ≡ K.ⓑ{J}V1 & - ⦃G, K⦄ ⊢ V1 ▶*×[0, ⫰(d+e-i)] V2 & + ⦃G, K⦄ ⊢ V1 ▶*[0, ⫰(d+e-i)] V2 & ⇧[O, i+1] V2 ≡ T2 & I = LRef i. #I #G #L #T2 #d #e #H @(cpys_ind … H) -T2 @@ -67,20 +67,20 @@ lemma cpys_inv_atom1: ∀I,G,L,T2,d,e. ⦃G, L⦄ ⊢ ⓪{I} ▶*×[d, e] T2 → ] qed-. -lemma cpys_inv_lref1: ∀G,L,T2,i,d,e. ⦃G, L⦄ ⊢ #i ▶*×[d, e] T2 → +lemma cpys_inv_lref1: ∀G,L,T2,i,d,e. ⦃G, L⦄ ⊢ #i ▶*[d, e] T2 → T2 = #i ∨ ∃∃I,K,V1,V2. d ≤ i & i < d + e & ⇩[i] L ≡ K.ⓑ{I}V1 & - ⦃G, K⦄ ⊢ V1 ▶*×[0, ⫰(d+e-i)] V2 & + ⦃G, K⦄ ⊢ V1 ▶*[0, ⫰(d+e-i)] V2 & ⇧[O, i+1] V2 ≡ T2. #G #L #T2 #i #d #e #H elim (cpys_inv_atom1 … H) -H /2 width=1 by or_introl/ * #I #K #V1 #V2 #j #Hdj #Hjde #HLK #HV12 #HVT2 #H destruct /3 width=7 by ex5_4_intro, or_intror/ qed-. -lemma cpys_inv_lref1_ldrop: ∀G,L,T2,i,d,e. ⦃G, L⦄ ⊢ #i ▶*×[d, e] T2 → +lemma cpys_inv_lref1_ldrop: ∀G,L,T2,i,d,e. ⦃G, L⦄ ⊢ #i ▶*[d, e] T2 → ∀I,K,V1. ⇩[i] L ≡ K.ⓑ{I}V1 → ∀V2. ⇧[O, i+1] V2 ≡ T2 → - ∧∧ ⦃G, K⦄ ⊢ V1 ▶*×[0, ⫰(d+e-i)] V2 + ∧∧ ⦃G, K⦄ ⊢ V1 ▶*[0, ⫰(d+e-i)] V2 & d ≤ i & i < d + e. #G #L #T2 #i #d #e #H #I #K #V1 #HLK #V2 #HVT2 elim (cpys_inv_lref1 … H) -H @@ -94,10 +94,10 @@ qed-. (* Properties on relocation *************************************************) -lemma cpys_lift_le: ∀G,K,T1,T2,dt,et. ⦃G, K⦄ ⊢ T1 ▶*×[dt, et] T2 → +lemma cpys_lift_le: ∀G,K,T1,T2,dt,et. ⦃G, K⦄ ⊢ T1 ▶*[dt, et] T2 → ∀L,U1,s,d,e. dt + et ≤ yinj d → ⇩[s, d, e] L ≡ K → ⇧[d, e] T1 ≡ U1 → ∀U2. ⇧[d, e] T2 ≡ U2 → - ⦃G, L⦄ ⊢ U1 ▶*×[dt, et] U2. + ⦃G, L⦄ ⊢ U1 ▶*[dt, et] U2. #G #K #T1 #T2 #dt #et #H #L #U1 #s #d #e #Hdetd #HLK #HTU1 @(cpys_ind … H) -T2 [ #U2 #H >(lift_mono … HTU1 … H) -H // | -HTU1 #T #T2 #_ #HT2 #IHT #U2 #HTU2 @@ -107,10 +107,10 @@ lemma cpys_lift_le: ∀G,K,T1,T2,dt,et. ⦃G, K⦄ ⊢ T1 ▶*×[dt, et] T2 → ] qed-. -lemma cpys_lift_be: ∀G,K,T1,T2,dt,et. ⦃G, K⦄ ⊢ T1 ▶*×[dt, et] T2 → +lemma cpys_lift_be: ∀G,K,T1,T2,dt,et. ⦃G, K⦄ ⊢ T1 ▶*[dt, et] T2 → ∀L,U1,s,d,e. dt ≤ yinj d → d ≤ dt + et → ⇩[s, d, e] L ≡ K → ⇧[d, e] T1 ≡ U1 → - ∀U2. ⇧[d, e] T2 ≡ U2 → ⦃G, L⦄ ⊢ U1 ▶*×[dt, et + e] U2. + ∀U2. ⇧[d, e] T2 ≡ U2 → ⦃G, L⦄ ⊢ U1 ▶*[dt, et + e] U2. #G #K #T1 #T2 #dt #et #H #L #U1 #s #d #e #Hdtd #Hddet #HLK #HTU1 @(cpys_ind … H) -T2 [ #U2 #H >(lift_mono … HTU1 … H) -H // | -HTU1 #T #T2 #_ #HT2 #IHT #U2 #HTU2 @@ -120,10 +120,10 @@ lemma cpys_lift_be: ∀G,K,T1,T2,dt,et. ⦃G, K⦄ ⊢ T1 ▶*×[dt, et] T2 → ] qed-. -lemma cpys_lift_ge: ∀G,K,T1,T2,dt,et. ⦃G, K⦄ ⊢ T1 ▶*×[dt, et] T2 → +lemma cpys_lift_ge: ∀G,K,T1,T2,dt,et. ⦃G, K⦄ ⊢ T1 ▶*[dt, et] T2 → ∀L,U1,s,d,e. yinj d ≤ dt → ⇩[s, d, e] L ≡ K → ⇧[d, e] T1 ≡ U1 → ∀U2. ⇧[d, e] T2 ≡ U2 → - ⦃G, L⦄ ⊢ U1 ▶*×[dt+e, et] U2. + ⦃G, L⦄ ⊢ U1 ▶*[dt+e, et] U2. #G #K #T1 #T2 #dt #et #H #L #U1 #s #d #e #Hddt #HLK #HTU1 @(cpys_ind … H) -T2 [ #U2 #H >(lift_mono … HTU1 … H) -H // | -HTU1 #T #T2 #_ #HT2 #IHT #U2 #HTU2 @@ -135,10 +135,10 @@ qed-. (* Inversion lemmas for relocation ******************************************) -lemma cpys_inv_lift1_le: ∀G,L,U1,U2,dt,et. ⦃G, L⦄ ⊢ U1 ▶*×[dt, et] U2 → +lemma cpys_inv_lift1_le: ∀G,L,U1,U2,dt,et. ⦃G, L⦄ ⊢ U1 ▶*[dt, et] U2 → ∀K,s,d,e. ⇩[s, d, e] L ≡ K → ∀T1. ⇧[d, e] T1 ≡ U1 → dt + et ≤ d → - ∃∃T2. ⦃G, K⦄ ⊢ T1 ▶*×[dt, et] T2 & ⇧[d, e] T2 ≡ U2. + ∃∃T2. ⦃G, K⦄ ⊢ T1 ▶*[dt, et] T2 & ⇧[d, e] T2 ≡ U2. #G #L #U1 #U2 #dt #et #H #K #s #d #e #HLK #T1 #HTU1 #Hdetd @(cpys_ind … H) -U2 [ /2 width=3 by ex2_intro/ | -HTU1 #U #U2 #_ #HU2 * #T #HT1 #HTU @@ -146,10 +146,10 @@ lemma cpys_inv_lift1_le: ∀G,L,U1,U2,dt,et. ⦃G, L⦄ ⊢ U1 ▶*×[dt, et] U2 ] qed-. -lemma cpys_inv_lift1_be: ∀G,L,U1,U2,dt,et. ⦃G, L⦄ ⊢ U1 ▶*×[dt, et] U2 → +lemma cpys_inv_lift1_be: ∀G,L,U1,U2,dt,et. ⦃G, L⦄ ⊢ U1 ▶*[dt, et] U2 → ∀K,s,d,e. ⇩[s, d, e] L ≡ K → ∀T1. ⇧[d, e] T1 ≡ U1 → dt ≤ d → yinj d + e ≤ dt + et → - ∃∃T2. ⦃G, K⦄ ⊢ T1 ▶*×[dt, et - e] T2 & ⇧[d, e] T2 ≡ U2. + ∃∃T2. ⦃G, K⦄ ⊢ T1 ▶*[dt, et - e] T2 & ⇧[d, e] T2 ≡ U2. #G #L #U1 #U2 #dt #et #H #K #s #d #e #HLK #T1 #HTU1 #Hdtd #Hdedet @(cpys_ind … H) -U2 [ /2 width=3 by ex2_intro/ | -HTU1 #U #U2 #_ #HU2 * #T #HT1 #HTU @@ -157,10 +157,10 @@ lemma cpys_inv_lift1_be: ∀G,L,U1,U2,dt,et. ⦃G, L⦄ ⊢ U1 ▶*×[dt, et] U2 ] qed-. -lemma cpys_inv_lift1_ge: ∀G,L,U1,U2,dt,et. ⦃G, L⦄ ⊢ U1 ▶*×[dt, et] U2 → +lemma cpys_inv_lift1_ge: ∀G,L,U1,U2,dt,et. ⦃G, L⦄ ⊢ U1 ▶*[dt, et] U2 → ∀K,s,d,e. ⇩[s, d, e] L ≡ K → ∀T1. ⇧[d, e] T1 ≡ U1 → yinj d + e ≤ dt → - ∃∃T2. ⦃G, K⦄ ⊢ T1 ▶*×[dt - e, et] T2 & ⇧[d, e] T2 ≡ U2. + ∃∃T2. ⦃G, K⦄ ⊢ T1 ▶*[dt - e, et] T2 & ⇧[d, e] T2 ≡ U2. #G #L #U1 #U2 #dt #et #H #K #s #d #e #HLK #T1 #HTU1 #Hdedt @(cpys_ind … H) -U2 [ /2 width=3 by ex2_intro/ | -HTU1 #U #U2 #_ #HU2 * #T #HT1 #HTU @@ -170,10 +170,10 @@ qed-. (* Advanced inversion lemmas on relocation **********************************) -lemma cpys_inv_lift1_ge_up: ∀G,L,U1,U2,dt,et. ⦃G, L⦄ ⊢ U1 ▶*×[dt, et] U2 → +lemma cpys_inv_lift1_ge_up: ∀G,L,U1,U2,dt,et. ⦃G, L⦄ ⊢ U1 ▶*[dt, et] U2 → ∀K,s,d,e. ⇩[s, d, e] L ≡ K → ∀T1. ⇧[d, e] T1 ≡ U1 → d ≤ dt → dt ≤ yinj d + e → yinj d + e ≤ dt + et → - ∃∃T2. ⦃G, K⦄ ⊢ T1 ▶*×[d, dt + et - (yinj d + e)] T2 & + ∃∃T2. ⦃G, K⦄ ⊢ T1 ▶*[d, dt + et - (yinj d + e)] T2 & ⇧[d, e] T2 ≡ U2. #G #L #U1 #U2 #dt #et #H #K #s #d #e #HLK #T1 #HTU1 #Hddt #Hdtde #Hdedet @(cpys_ind … H) -U2 [ /2 width=3 by ex2_intro/ @@ -182,10 +182,10 @@ lemma cpys_inv_lift1_ge_up: ∀G,L,U1,U2,dt,et. ⦃G, L⦄ ⊢ U1 ▶*×[dt, et] ] qed-. -lemma cpys_inv_lift1_be_up: ∀G,L,U1,U2,dt,et. ⦃G, L⦄ ⊢ U1 ▶*×[dt, et] U2 → +lemma cpys_inv_lift1_be_up: ∀G,L,U1,U2,dt,et. ⦃G, L⦄ ⊢ U1 ▶*[dt, et] U2 → ∀K,s,d,e. ⇩[s, d, e] L ≡ K → ∀T1. ⇧[d, e] T1 ≡ U1 → dt ≤ d → dt + et ≤ yinj d + e → - ∃∃T2. ⦃G, K⦄ ⊢ T1 ▶*×[dt, d - dt] T2 & ⇧[d, e] T2 ≡ U2. + ∃∃T2. ⦃G, K⦄ ⊢ T1 ▶*[dt, d - dt] T2 & ⇧[d, e] T2 ≡ U2. #G #L #U1 #U2 #dt #et #H #K #s #d #e #HLK #T1 #HTU1 #Hdtd #Hdetde @(cpys_ind … H) -U2 [ /2 width=3 by ex2_intro/ | -HTU1 #U #U2 #_ #HU2 * #T #HT1 #HTU @@ -193,10 +193,10 @@ lemma cpys_inv_lift1_be_up: ∀G,L,U1,U2,dt,et. ⦃G, L⦄ ⊢ U1 ▶*×[dt, et] ] qed-. -lemma cpys_inv_lift1_le_up: ∀G,L,U1,U2,dt,et. ⦃G, L⦄ ⊢ U1 ▶*×[dt, et] U2 → +lemma cpys_inv_lift1_le_up: ∀G,L,U1,U2,dt,et. ⦃G, L⦄ ⊢ U1 ▶*[dt, et] U2 → ∀K,s,d,e. ⇩[s, d, e] L ≡ K → ∀T1. ⇧[d, e] T1 ≡ U1 → dt ≤ d → d ≤ dt + et → dt + et ≤ yinj d + e → - ∃∃T2. ⦃G, K⦄ ⊢ T1 ▶*×[dt, d - dt] T2 & ⇧[d, e] T2 ≡ U2. + ∃∃T2. ⦃G, K⦄ ⊢ T1 ▶*[dt, d - dt] T2 & ⇧[d, e] T2 ≡ U2. #G #L #U1 #U2 #dt #et #H #K #s #d #e #HLK #T1 #HTU1 #Hdtd #Hddet #Hdetde @(cpys_ind … H) -U2 [ /2 width=3 by ex2_intro/ | -HTU1 #U #U2 #_ #HU2 * #T #HT1 #HTU diff --git a/matita/matita/contribs/lambdadelta/basic_2/substitution/lleq.ma b/matita/matita/contribs/lambdadelta/basic_2/substitution/lleq.ma index d6bef52ec..6bce82987 100644 --- a/matita/matita/contribs/lambdadelta/basic_2/substitution/lleq.ma +++ b/matita/matita/contribs/lambdadelta/basic_2/substitution/lleq.ma @@ -19,7 +19,7 @@ include "basic_2/substitution/cpys.ma". definition lleq: relation4 ynat term lenv lenv ≝ λd,T,L1,L2. |L1| = |L2| ∧ - (∀U. ⦃⋆, L1⦄ ⊢ T ▶*×[d, ∞] U ↔ ⦃⋆, L2⦄ ⊢ T ▶*×[d, ∞] U). + (∀U. ⦃⋆, L1⦄ ⊢ T ▶*[d, ∞] U ↔ ⦃⋆, L2⦄ ⊢ T ▶*[d, ∞] U). interpretation "lazy equivalence (local environment)"