From: Ferruccio Guidi Date: Sat, 16 Apr 2016 12:43:32 +0000 (+0000) Subject: - former llpx_sn an lleq reactivated as lfxs and lfeq X-Git-Tag: make_still_working~603 X-Git-Url: http://matita.cs.unibo.it/gitweb/?a=commitdiff_plain;h=e39d1924cd572acdf0cf8dba08f3b650dfd6abee;p=helm.git - former llpx_sn an lleq reactivated as lfxs and lfeq --- diff --git a/matita/matita/contribs/lambdadelta/basic_2/etc_new/aaa/aaa_freq.etc b/matita/matita/contribs/lambdadelta/basic_2/etc_new/aaa/aaa_freq.etc deleted file mode 100644 index a81eb6166..000000000 --- a/matita/matita/contribs/lambdadelta/basic_2/etc_new/aaa/aaa_freq.etc +++ /dev/null @@ -1,42 +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 *) -(* *) -(**************************************************************************) - -include "basic_2/multiple/lleq_drop.ma". -include "basic_2/static/aaa.ma". - -(* ATONIC ARITY ASSIGNMENT ON TERMS *****************************************) - -(* Properties on lazy equivalence for local environments ********************) - -lemma lleq_aaa_trans: ∀G,L2,T,A. ⦃G, L2⦄ ⊢ T ⁝ A → - ∀L1. L1 ≡[T, 0] L2 → ⦃G, L1⦄ ⊢ T ⁝ A. -#G #L2 #T #A #H elim H -G -L2 -T -A /2 width=1 by aaa_sort/ -[ #I #G #L2 #K2 #V2 #A #i #HLK2 #_ #IHV2 #L1 #H elim (lleq_fwd_lref_dx … H … HLK2) -L2 - [ #H elim (ylt_yle_false … H) // - | * /3 width=5 by aaa_lref/ - ] -| #a #G #L2 #V #T #B #A #_ #_ #IHV #IHT #L1 #H elim (lleq_inv_bind_O … H) -H - /3 width=2 by aaa_abbr/ -| #a #G #L2 #V #T #B #A #_ #_ #IHV #IHT #L1 #H elim (lleq_inv_bind_O … H) -H - /3 width=1 by aaa_abst/ -| #G #L2 #V #T #B #A #_ #_ #IHV #IHT #L1 #H elim (lleq_inv_flat … H) -H - /3 width=3 by aaa_appl/ -| #G #L2 #V #T #A #_ #_ #IHV #IHT #L1 #H elim (lleq_inv_flat … H) -H - /3 width=1 by aaa_cast/ -] -qed-. - -lemma aaa_lleq_conf: ∀G,L2,T,A. ⦃G, L2⦄ ⊢ T ⁝ A → - ∀L1. L2 ≡[T, 0] L1 → ⦃G, L1⦄ ⊢ T ⁝ A. -/3 width=3 by lleq_aaa_trans, lleq_sym/ qed-. diff --git a/matita/matita/contribs/lambdadelta/basic_2/etc_new/lleq/lleq.etc b/matita/matita/contribs/lambdadelta/basic_2/etc_new/lleq/lleq.etc index 521ad356d..ac55a2c8a 100644 --- a/matita/matita/contribs/lambdadelta/basic_2/etc_new/lleq/lleq.etc +++ b/matita/matita/contribs/lambdadelta/basic_2/etc_new/lleq/lleq.etc @@ -17,17 +17,6 @@ include "basic_2/multiple/llpx_sn.ma". (* LAZY EQUIVALENCE FOR LOCAL ENVIRONMENTS **********************************) -definition ceq: relation3 lenv term term ≝ λL,T1,T2. T1 = T2. - -definition lleq: relation4 ynat term lenv lenv ≝ llpx_sn ceq. - -interpretation - "lazy equivalence (local environment)" - 'LazyEq T l L1 L2 = (lleq l T L1 L2). - -definition lleq_transitive: predicate (relation3 lenv term term) ≝ - λR. ∀L2,T1,T2. R L2 T1 T2 → ∀L1. L1 ≡[T1, 0] L2 → R L1 T1 T2. - (* Basic inversion lemmas ***************************************************) lemma lleq_ind: ∀R:relation4 ynat term lenv lenv. ( @@ -55,19 +44,8 @@ lemma lleq_ind: ∀R:relation4 ynat term lenv lenv. ( #R #H1 #H2 #H3 #H4 #H5 #H6 #H7 #l #T #L1 #L2 #H elim H -L1 -L2 -T -l /2 width=8 by/ qed-. -lemma lleq_inv_bind: ∀a,I,L1,L2,V,T,l. L1 ≡[ⓑ{a,I}V.T, l] L2 → - L1 ≡[V, l] L2 ∧ L1.ⓑ{I}V ≡[T, ⫯l] L2.ⓑ{I}V. -/2 width=2 by llpx_sn_inv_bind/ qed-. - -lemma lleq_inv_flat: ∀I,L1,L2,V,T,l. L1 ≡[ⓕ{I}V.T, l] L2 → - L1 ≡[V, l] L2 ∧ L1 ≡[T, l] L2. -/2 width=2 by llpx_sn_inv_flat/ qed-. - (* Basic forward lemmas *****************************************************) -lemma lleq_fwd_length: ∀L1,L2,T,l. L1 ≡[T, l] L2 → |L1| = |L2|. -/2 width=4 by llpx_sn_fwd_length/ qed-. - lemma lleq_fwd_lref: ∀L1,L2,l,i. L1 ≡[#i, l] L2 → ∨∨ |L1| ≤ i ∧ |L2| ≤ i | yinj i < l @@ -86,75 +64,9 @@ lemma lleq_fwd_drop_dx: ∀L1,L2,T,l. L1 ≡[l, T] L2 → ∀K2,i. ⬇[i] L2 ≡ ∃K1. ⬇[i] L1 ≡ K1. /2 width=7 by llpx_sn_fwd_drop_dx/ qed-. -lemma lleq_fwd_bind_sn: ∀a,I,L1,L2,V,T,l. - L1 ≡[ⓑ{a,I}V.T, l] L2 → L1 ≡[V, l] L2. -/2 width=4 by llpx_sn_fwd_bind_sn/ qed-. - -lemma lleq_fwd_bind_dx: ∀a,I,L1,L2,V,T,l. - L1 ≡[ⓑ{a,I}V.T, l] L2 → L1.ⓑ{I}V ≡[T, ⫯l] L2.ⓑ{I}V. -/2 width=2 by llpx_sn_fwd_bind_dx/ qed-. - -lemma lleq_fwd_flat_sn: ∀I,L1,L2,V,T,l. - L1 ≡[ⓕ{I}V.T, l] L2 → L1 ≡[V, l] L2. -/2 width=3 by llpx_sn_fwd_flat_sn/ qed-. - -lemma lleq_fwd_flat_dx: ∀I,L1,L2,V,T,l. - L1 ≡[ⓕ{I}V.T, l] L2 → L1 ≡[T, l] L2. -/2 width=3 by llpx_sn_fwd_flat_dx/ qed-. - (* Basic properties *********************************************************) -lemma lleq_sort: ∀L1,L2,l,s. |L1| = |L2| → L1 ≡[⋆s, l] L2. -/2 width=1 by llpx_sn_sort/ qed. - -lemma lleq_skip: ∀L1,L2,l,i. yinj i < l → |L1| = |L2| → L1 ≡[#i, l] L2. -/2 width=1 by llpx_sn_skip/ qed. - lemma lleq_lref: ∀I,L1,L2,K1,K2,V,l,i. l ≤ yinj i → ⬇[i] L1 ≡ K1.ⓑ{I}V → ⬇[i] L2 ≡ K2.ⓑ{I}V → K1 ≡[V, 0] K2 → L1 ≡[#i, l] L2. /2 width=9 by llpx_sn_lref/ qed. - -lemma lleq_free: ∀L1,L2,l,i. |L1| ≤ i → |L2| ≤ i → |L1| = |L2| → L1 ≡[#i, l] L2. -/2 width=1 by llpx_sn_free/ qed. - -lemma lleq_gref: ∀L1,L2,l,p. |L1| = |L2| → L1 ≡[§p, l] L2. -/2 width=1 by llpx_sn_gref/ qed. - -lemma lleq_bind: ∀a,I,L1,L2,V,T,l. - L1 ≡[V, l] L2 → L1.ⓑ{I}V ≡[T, ⫯l] L2.ⓑ{I}V → - L1 ≡[ⓑ{a,I}V.T, l] L2. -/2 width=1 by llpx_sn_bind/ qed. - -lemma lleq_flat: ∀I,L1,L2,V,T,l. - L1 ≡[V, l] L2 → L1 ≡[T, l] L2 → L1 ≡[ⓕ{I}V.T, l] L2. -/2 width=1 by llpx_sn_flat/ qed. - -lemma lleq_refl: ∀l,T. reflexive … (lleq l T). -/2 width=1 by llpx_sn_refl/ qed. - -lemma lleq_Y: ∀L1,L2,T. |L1| = |L2| → L1 ≡[T, ∞] L2. -/2 width=1 by llpx_sn_Y/ qed. - -lemma lleq_sym: ∀l,T. symmetric … (lleq l T). -#l #T #L1 #L2 #H @(lleq_ind … H) -l -T -L1 -L2 -/2 width=7 by lleq_sort, lleq_skip, lleq_lref, lleq_free, lleq_gref, lleq_bind, lleq_flat/ -qed-. - -lemma lleq_ge_up: ∀L1,L2,U,lt. L1 ≡[U, lt] L2 → - ∀T,l,k. ⬆[l, k] T ≡ U → - lt ≤ l + k → L1 ≡[U, l] L2. -/2 width=6 by llpx_sn_ge_up/ qed-. - -lemma lleq_ge: ∀L1,L2,T,l1. L1 ≡[T, l1] L2 → ∀l2. l1 ≤ l2 → L1 ≡[T, l2] L2. -/2 width=3 by llpx_sn_ge/ qed-. - -lemma lleq_bind_O: ∀a,I,L1,L2,V,T. L1 ≡[V, 0] L2 → L1.ⓑ{I}V ≡[T, 0] L2.ⓑ{I}V → - L1 ≡[ⓑ{a,I}V.T, 0] L2. -/2 width=1 by llpx_sn_bind_O/ qed-. - -(* Advanceded properties on lazy pointwise extensions ************************) - -lemma llpx_sn_lrefl: ∀R. (∀L. reflexive … (R L)) → - ∀L1,L2,T,l. L1 ≡[T, l] L2 → llpx_sn R l T L1 L2. -/2 width=3 by llpx_sn_co/ qed-. diff --git a/matita/matita/contribs/lambdadelta/basic_2/etc_new/lleq/lleq_lleq.etc b/matita/matita/contribs/lambdadelta/basic_2/etc_new/lleq/lleq_lleq.etc deleted file mode 100644 index 630b41a32..000000000 --- a/matita/matita/contribs/lambdadelta/basic_2/etc_new/lleq/lleq_lleq.etc +++ /dev/null @@ -1,39 +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 *) -(* *) -(**************************************************************************) - -include "basic_2/multiple/lleq_drop.ma". - -(* LAZY EQUIVALENCE FOR LOCAL ENVIRONMENTS **********************************) - -(* Main properties **********************************************************) - -theorem lleq_trans: ∀l,T. Transitive … (lleq l T). -/2 width=3 by lleq_llpx_sn_trans/ qed-. - -theorem lleq_canc_sn: ∀L,L1,L2,T,l. L ≡[l, T] L1→ L ≡[l, T] L2 → L1 ≡[l, T] L2. -/3 width=3 by lleq_trans, lleq_sym/ qed-. - -theorem lleq_canc_dx: ∀L1,L2,L,T,l. L1 ≡[l, T] L → L2 ≡[l, T] L → L1 ≡[l, T] L2. -/3 width=3 by lleq_trans, lleq_sym/ qed-. - -(* Advanced properies on negated lazy equivalence *****************************) - -(* Note: for use in auto, works with /4 width=8/ so lleq_canc_sn is preferred *) -lemma lleq_nlleq_trans: ∀l,T,L1,L. L1 ≡[T, l] L → - ∀L2. (L ≡[T, l] L2 → ⊥) → (L1 ≡[T, l] L2 → ⊥). -/3 width=3 by lleq_canc_sn/ qed-. - -lemma nlleq_lleq_div: ∀l,T,L2,L. L2 ≡[T, l] L → - ∀L1. (L1 ≡[T, l] L → ⊥) → (L1 ≡[T, l] L2 → ⊥). -/3 width=3 by lleq_trans/ qed-. diff --git a/matita/matita/contribs/lambdadelta/basic_2/etc_new/llpx_sn/llpx_sn.etc b/matita/matita/contribs/lambdadelta/basic_2/etc_new/llpx_sn/llpx_sn.etc index ffe9501f6..5a1124b5c 100644 --- a/matita/matita/contribs/lambdadelta/basic_2/etc_new/llpx_sn/llpx_sn.etc +++ b/matita/matita/contribs/lambdadelta/basic_2/etc_new/llpx_sn/llpx_sn.etc @@ -17,69 +17,12 @@ include "basic_2/substitution/drop.ma". (* LAZY SN POINTWISE EXTENSION OF A CONTEXT-SENSITIVE REALTION FOR TERMS ****) -inductive llpx_sn (R:relation3 lenv term term): relation4 ynat term lenv lenv ≝ -| llpx_sn_sort: ∀L1,L2,l,s. |L1| = |L2| → llpx_sn R l (⋆s) L1 L2 -| llpx_sn_skip: ∀L1,L2,l,i. |L1| = |L2| → yinj i < l → llpx_sn R l (#i) L1 L2 | llpx_sn_lref: ∀I,L1,L2,K1,K2,V1,V2,l,i. l ≤ yinj i → ⬇[i] L1 ≡ K1.ⓑ{I}V1 → ⬇[i] L2 ≡ K2.ⓑ{I}V2 → llpx_sn R (yinj 0) V1 K1 K2 → R K1 V1 V2 → llpx_sn R l (#i) L1 L2 -| llpx_sn_free: ∀L1,L2,l,i. |L1| ≤ i → |L2| ≤ i → |L1| = |L2| → llpx_sn R l (#i) L1 L2 -| llpx_sn_gref: ∀L1,L2,l,p. |L1| = |L2| → llpx_sn R l (§p) L1 L2 -| llpx_sn_bind: ∀a,I,L1,L2,V,T,l. - llpx_sn R l V L1 L2 → llpx_sn R (⫯l) T (L1.ⓑ{I}V) (L2.ⓑ{I}V) → - llpx_sn R l (ⓑ{a,I}V.T) L1 L2 -| llpx_sn_flat: ∀I,L1,L2,V,T,l. - llpx_sn R l V L1 L2 → llpx_sn R l T L1 L2 → llpx_sn R l (ⓕ{I}V.T) L1 L2 -. - -(* Basic inversion lemmas ***************************************************) - -fact llpx_sn_inv_bind_aux: ∀R,L1,L2,X,l. llpx_sn R l X L1 L2 → - ∀a,I,V,T. X = ⓑ{a,I}V.T → - llpx_sn R l V L1 L2 ∧ llpx_sn R (⫯l) T (L1.ⓑ{I}V) (L2.ⓑ{I}V). -#R #L1 #L2 #X #l * -L1 -L2 -X -l -[ #L1 #L2 #l #s #_ #b #J #W #U #H destruct -| #L1 #L2 #l #i #_ #_ #b #J #W #U #H destruct -| #I #L1 #L2 #K1 #K2 #V1 #V2 #l #i #_ #_ #_ #_ #_ #b #J #W #U #H destruct -| #L1 #L2 #l #i #_ #_ #_ #b #J #W #U #H destruct -| #L1 #L2 #l #p #_ #b #J #W #U #H destruct -| #a #I #L1 #L2 #V #T #l #HV #HT #b #J #W #U #H destruct /2 width=1 by conj/ -| #I #L1 #L2 #V #T #l #_ #_ #b #J #W #U #H destruct -] -qed-. - -lemma llpx_sn_inv_bind: ∀R,a,I,L1,L2,V,T,l. llpx_sn R l (ⓑ{a,I}V.T) L1 L2 → - llpx_sn R l V L1 L2 ∧ llpx_sn R (⫯l) T (L1.ⓑ{I}V) (L2.ⓑ{I}V). -/2 width=4 by llpx_sn_inv_bind_aux/ qed-. - -fact llpx_sn_inv_flat_aux: ∀R,L1,L2,X,l. llpx_sn R l X L1 L2 → - ∀I,V,T. X = ⓕ{I}V.T → - llpx_sn R l V L1 L2 ∧ llpx_sn R l T L1 L2. -#R #L1 #L2 #X #l * -L1 -L2 -X -l -[ #L1 #L2 #l #s #_ #J #W #U #H destruct -| #L1 #L2 #l #i #_ #_ #J #W #U #H destruct -| #I #L1 #L2 #K1 #K2 #V1 #V2 #l #i #_ #_ #_ #_ #_ #J #W #U #H destruct -| #L1 #L2 #l #i #_ #_ #_ #J #W #U #H destruct -| #L1 #L2 #l #p #_ #J #W #U #H destruct -| #a #I #L1 #L2 #V #T #l #_ #_ #J #W #U #H destruct -| #I #L1 #L2 #V #T #l #HV #HT #J #W #U #H destruct /2 width=1 by conj/ -] -qed-. - -lemma llpx_sn_inv_flat: ∀R,I,L1,L2,V,T,l. llpx_sn R l (ⓕ{I}V.T) L1 L2 → - llpx_sn R l V L1 L2 ∧ llpx_sn R l T L1 L2. -/2 width=4 by llpx_sn_inv_flat_aux/ qed-. (* Basic forward lemmas *****************************************************) -lemma llpx_sn_fwd_length: ∀R,L1,L2,T,l. llpx_sn R l T L1 L2 → |L1| = |L2|. -#R #L1 #L2 #T #l #H elim H -L1 -L2 -T -l // -#I #L1 #L2 #K1 #K2 #V1 #V2 #l #i #_ #HLK1 #HLK2 #_ #_ #HK12 -lapply (drop_fwd_length … HLK1) -HLK1 -lapply (drop_fwd_length … HLK2) -HLK2 -normalize // -qed-. - lemma llpx_sn_fwd_drop_sn: ∀R,L1,L2,T,l. llpx_sn R l T L1 L2 → ∀K1,i. ⬇[i] L1 ≡ K1 → ∃K2. ⬇[i] L2 ≡ K2. #R #L1 #L2 #T #l #H #K1 #i #HLK1 lapply (llpx_sn_fwd_length … H) -H @@ -92,25 +35,6 @@ lemma llpx_sn_fwd_drop_dx: ∀R,L1,L2,T,l. llpx_sn R l T L1 L2 → #HL12 lapply (drop_fwd_length_le2 … HLK2) -HLK2 /2 width=1 by drop_O1_le/ qed-. -fact llpx_sn_fwd_lref_aux: ∀R,L1,L2,X,l. llpx_sn R l X L1 L2 → ∀i. X = #i → - ∨∨ |L1| ≤ i ∧ |L2| ≤ i - | yinj i < l - | ∃∃I,K1,K2,V1,V2. ⬇[i] L1 ≡ K1.ⓑ{I}V1 & - ⬇[i] L2 ≡ K2.ⓑ{I}V2 & - llpx_sn R (yinj 0) V1 K1 K2 & - R K1 V1 V2 & l ≤ yinj i. -#R #L1 #L2 #X #l * -L1 -L2 -X -l -[ #L1 #L2 #l #s #_ #j #H destruct -| #L1 #L2 #l #i #_ #Hil #j #H destruct /2 width=1 by or3_intro1/ -| #I #L1 #L2 #K1 #K2 #V1 #V2 #l #i #Hli #HLK1 #HLK2 #HK12 #HV12 #j #H destruct - /3 width=9 by or3_intro2, ex5_5_intro/ -| #L1 #L2 #l #i #HL1 #HL2 #_ #j #H destruct /3 width=1 by or3_intro0, conj/ -| #L1 #L2 #l #p #_ #j #H destruct -| #a #I #L1 #L2 #V #T #l #_ #_ #j #H destruct -| #I #L1 #L2 #V #T #l #_ #_ #j #H destruct -] -qed-. - lemma llpx_sn_fwd_lref: ∀R,L1,L2,l,i. llpx_sn R l (#i) L1 L2 → ∨∨ |L1| ≤ i ∧ |L2| ≤ i | yinj i < l @@ -119,91 +43,3 @@ lemma llpx_sn_fwd_lref: ∀R,L1,L2,l,i. llpx_sn R l (#i) L1 L2 → llpx_sn R (yinj 0) V1 K1 K2 & R K1 V1 V2 & l ≤ yinj i. /2 width=3 by llpx_sn_fwd_lref_aux/ qed-. - -lemma llpx_sn_fwd_bind_sn: ∀R,a,I,L1,L2,V,T,l. llpx_sn R l (ⓑ{a,I}V.T) L1 L2 → - llpx_sn R l V L1 L2. -#R #a #I #L1 #L2 #V #T #l #H elim (llpx_sn_inv_bind … H) -H // -qed-. - -lemma llpx_sn_fwd_bind_dx: ∀R,a,I,L1,L2,V,T,l. llpx_sn R l (ⓑ{a,I}V.T) L1 L2 → - llpx_sn R (⫯l) T (L1.ⓑ{I}V) (L2.ⓑ{I}V). -#R #a #I #L1 #L2 #V #T #l #H elim (llpx_sn_inv_bind … H) -H // -qed-. - -lemma llpx_sn_fwd_flat_sn: ∀R,I,L1,L2,V,T,l. llpx_sn R l (ⓕ{I}V.T) L1 L2 → - llpx_sn R l V L1 L2. -#R #I #L1 #L2 #V #T #l #H elim (llpx_sn_inv_flat … H) -H // -qed-. - -lemma llpx_sn_fwd_flat_dx: ∀R,I,L1,L2,V,T,l. llpx_sn R l (ⓕ{I}V.T) L1 L2 → - llpx_sn R l T L1 L2. -#R #I #L1 #L2 #V #T #l #H elim (llpx_sn_inv_flat … H) -H // -qed-. - -lemma llpx_sn_fwd_pair_sn: ∀R,I,L1,L2,V,T,l. llpx_sn R l (②{I}V.T) L1 L2 → - llpx_sn R l V L1 L2. -#R * /2 width=4 by llpx_sn_fwd_flat_sn, llpx_sn_fwd_bind_sn/ -qed-. - -(* Basic properties *********************************************************) - -lemma llpx_sn_refl: ∀R. (∀L. reflexive … (R L)) → ∀T,L,l. llpx_sn R l T L L. -#R #HR #T #L @(f2_ind … rfw … L T) -L -T -#x #IH #L * * /3 width=1 by llpx_sn_sort, llpx_sn_gref, llpx_sn_bind, llpx_sn_flat/ -#i #Hx elim (lt_or_ge i (|L|)) /2 width=1 by llpx_sn_free/ -#HiL #l elim (ylt_split i l) /2 width=1 by llpx_sn_skip/ -elim (drop_O1_lt … HiL) -HiL destruct /4 width=9 by llpx_sn_lref, drop_fwd_rfw/ -qed-. - -lemma llpx_sn_Y: ∀R,T,L1,L2. |L1| = |L2| → llpx_sn R (∞) T L1 L2. -#R #T #L1 @(f2_ind … rfw … L1 T) -L1 -T -#x #IH #L1 * * /3 width=1 by llpx_sn_sort, llpx_sn_skip, llpx_sn_gref, llpx_sn_flat/ -#a #I #V1 #T1 #Hx #L2 #HL12 -@llpx_sn_bind /2 width=1 by/ (**) (* explicit constructor *) -@IH -IH // normalize /2 width=1 by eq_f2/ -qed-. - -lemma llpx_sn_ge_up: ∀R,L1,L2,U,lt. llpx_sn R lt U L1 L2 → ∀T,l,k. ⬆[l, k] T ≡ U → - lt ≤ l + k → llpx_sn R l U L1 L2. -#R #L1 #L2 #U #lt #H elim H -L1 -L2 -U -lt -[ #L1 #L2 #lt #s #HL12 #X #l #k #H #_ >(lift_inv_sort2 … H) -H /2 width=1 by llpx_sn_sort/ -| #L1 #L2 #lt #i #HL12 #Hilt #X #l #k #H #Hltlm - elim (lift_inv_lref2 … H) -H * #Hil #H destruct /3 width=1 by llpx_sn_skip, ylt_inj/ -HL12 - elim (ylt_yle_false … Hilt) -Hilt - @(yle_trans … Hltlm) /2 width=1 by yle_inj/ (**) (* full auto too slow 11s *) -| #I #L1 #L2 #K1 #K2 #W1 #W2 #lt #i #Hlti #HLK1 #HLK2 #HW1 #HW12 #_ #X #l #k #H #_ - elim (lift_inv_lref2 … H) -H * #Hil #H destruct - [ lapply (llpx_sn_fwd_length … HW1) -HW1 #HK12 - lapply (drop_fwd_length … HLK1) lapply (drop_fwd_length … HLK2) - normalize in ⊢ (%→%→?); -I -W1 -W2 -lt /3 width=1 by llpx_sn_skip, ylt_inj/ - | /3 width=9 by llpx_sn_lref, yle_fwd_plus_sn1/ - ] -| /2 width=1 by llpx_sn_free/ -| #L1 #L2 #lt #p #HL12 #X #l #k #H #_ >(lift_inv_gref2 … H) -H /2 width=1 by llpx_sn_gref/ -| #a #I #L1 #L2 #W #U #lt #_ #_ #IHV #IHT #X #l #k #H #Hltlm destruct - elim (lift_inv_bind2 … H) -H #V #T #HVW #HTU #H destruct - @(llpx_sn_bind) /2 width=4 by/ (**) (* full auto fails *) - @(IHT … HTU) /2 width=1 by yle_succ/ -| #I #L1 #L2 #W #U #lt #_ #_ #IHV #IHT #X #l #k #H #Hltlm destruct - elim (lift_inv_flat2 … H) -H #HVW #HTU #H destruct - /3 width=4 by llpx_sn_flat/ -] -qed-. - -(**) (* the minor premise comes first *) -lemma llpx_sn_ge: ∀R,L1,L2,T,l1,l2. l1 ≤ l2 → - llpx_sn R l1 T L1 L2 → llpx_sn R l2 T L1 L2. -#R #L1 #L2 #T #l1 #l2 * -l1 -l2 (**) (* destructed yle *) -/3 width=6 by llpx_sn_ge_up, llpx_sn_Y, llpx_sn_fwd_length, yle_inj/ -qed-. - -lemma llpx_sn_bind_O: ∀R,a,I,L1,L2,V,T. llpx_sn R 0 V L1 L2 → - llpx_sn R 0 T (L1.ⓑ{I}V) (L2.ⓑ{I}V) → - llpx_sn R 0 (ⓑ{a,I}V.T) L1 L2. -/3 width=3 by llpx_sn_ge, llpx_sn_bind/ qed-. - -lemma llpx_sn_co: ∀R1,R2. (∀L,T1,T2. R1 L T1 T2 → R2 L T1 T2) → - ∀L1,L2,T,l. llpx_sn R1 l T L1 L2 → llpx_sn R2 l T L1 L2. -#R1 #R2 #HR12 #L1 #L2 #T #l #H elim H -L1 -L2 -T -l -/3 width=9 by llpx_sn_sort, llpx_sn_skip, llpx_sn_lref, llpx_sn_free, llpx_sn_gref, llpx_sn_bind, llpx_sn_flat/ -qed-. diff --git a/matita/matita/contribs/lambdadelta/basic_2/notation/relations/relationstar_4.ma b/matita/matita/contribs/lambdadelta/basic_2/notation/relations/relationstar_4.ma new file mode 100644 index 000000000..a306fa3d9 --- /dev/null +++ b/matita/matita/contribs/lambdadelta/basic_2/notation/relations/relationstar_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( L1 ⦻ * break [ term 46 R , break term 46 T ] break term 46 L2 )" + non associative with precedence 45 + for @{ 'RelationStar $R $T $L1 $L2 }. diff --git a/matita/matita/contribs/lambdadelta/basic_2/relocation/lexs.ma b/matita/matita/contribs/lambdadelta/basic_2/relocation/lexs.ma index 753a62bc5..e1fdd74f4 100644 --- a/matita/matita/contribs/lambdadelta/basic_2/relocation/lexs.ma +++ b/matita/matita/contribs/lambdadelta/basic_2/relocation/lexs.ma @@ -18,12 +18,6 @@ include "basic_2/grammar/lenv.ma". (* GENERIC ENTRYWISE EXTENSION OF CONTEXT-SENSITIVE REALTIONS FOR TERMS *****) -definition relation5 : Type[0] → Type[0] → Type[0] → Type[0] → Type[0] → Type[0] -≝ λA,B,C,D,E.A→B→C→D→E→Prop. - -definition relation6 : Type[0] → Type[0] → Type[0] → Type[0] → Type[0] → Type[0] → Type[0] -≝ λA,B,C,D,E,F.A→B→C→D→E→F→Prop. - (* Basic_2A1: includes: lpx_sn_atom lpx_sn_pair *) inductive lexs (RN,RP:relation3 lenv term term): rtmap → relation lenv ≝ | lexs_atom: ∀f. lexs RN RP f (⋆) (⋆) @@ -35,21 +29,21 @@ inductive lexs (RN,RP:relation3 lenv term term): rtmap → relation lenv ≝ lexs RN RP (↑f) (L1.ⓑ{I}V1) (L2.ⓑ{I}V2) . -interpretation "general entrywise extension (local environment)" +interpretation "generic entrywise extension (local environment)" 'RelationStar RN RP f L1 L2 = (lexs RN RP f L1 L2). -definition lpx_sn_confluent: relation6 (relation3 lenv term term) - (relation3 lenv term term) … ≝ - λR1,R2,RN1,RP1,RN2,RP2. - ∀f,L0,T0,T1. R1 L0 T0 T1 → ∀T2. R2 L0 T0 T2 → - ∀L1. L0 ⦻*[RN1, RP1, f] L1 → ∀L2. L0 ⦻*[RN2, RP2, f] L2 → - ∃∃T. R2 L1 T1 T & R1 L2 T2 T. +definition lexs_confluent: relation6 (relation3 lenv term term) + (relation3 lenv term term) … ≝ + λR1,R2,RN1,RP1,RN2,RP2. + ∀f,L0,T0,T1. R1 L0 T0 T1 → ∀T2. R2 L0 T0 T2 → + ∀L1. L0 ⦻*[RN1, RP1, f] L1 → ∀L2. L0 ⦻*[RN2, RP2, f] L2 → + ∃∃T. R2 L1 T1 T & R1 L2 T2 T. -definition lexs_transitive: relation4 (relation3 lenv term term) +definition lexs_transitive: relation5 (relation3 lenv term term) (relation3 lenv term term) … ≝ - λR1,R2,RN,RP. + λR1,R2,R3,RN,RP. ∀f,L1,T1,T. R1 L1 T1 T → ∀L2. L1 ⦻*[RN, RP, f] L2 → - ∀T2. R2 L2 T T2 → R1 L1 T1 T2. + ∀T2. R2 L2 T T2 → R3 L1 T1 T2. (* Basic inversion lemmas ***************************************************) @@ -152,6 +146,17 @@ lemma lexs_inv_tl: ∀RN,RP,I,L1,L2,V1,V2,f. L1 ⦻*[RN, RP, ⫱f] L2 → /2 width=1 by lexs_next, lexs_push/ qed-. +(* Basic forward lemmas *****************************************************) + +lemma lexs_fwd_pair: ∀RN,RP,I1,I2,L1,L2,V1,V2,f. + L1.ⓑ{I1}V1 ⦻*[RN, RP, f] L2.ⓑ{I2}V2 → + L1 ⦻*[RN, RP, ⫱f] L2 ∧ I1 = I2. +#RN #RP #I1 #I2 #L2 #L2 #V1 #V2 #f #Hf +elim (pn_split f) * #g #H destruct +[ elim (lexs_inv_push … Hf) | elim (lexs_inv_next … Hf) ] -Hf +/2 width=1 by conj/ +qed-. + (* Basic properties *********************************************************) lemma lexs_eq_repl_back: ∀RN,RP,L1,L2. eq_repl_back … (λf. L1 ⦻*[RN, RP, f] L2). @@ -209,11 +214,3 @@ lemma lexs_co: ∀RN1,RP1,RN2,RP2. #RN1 #RP1 #RN2 #RP2 #HRN #HRP #L1 #L2 #f #H elim H -L1 -L2 -f /3 width=1 by lexs_atom, lexs_next, lexs_push/ qed-. - -(* Basic_2A1: removed theorems 17: - llpx_sn_inv_bind llpx_sn_inv_flat - llpx_sn_fwd_lref llpx_sn_fwd_pair_sn llpx_sn_fwd_length - llpx_sn_fwd_bind_sn llpx_sn_fwd_bind_dx llpx_sn_fwd_flat_sn llpx_sn_fwd_flat_dx - llpx_sn_refl llpx_sn_Y llpx_sn_bind_O llpx_sn_ge_up llpx_sn_ge llpx_sn_co - llpx_sn_fwd_drop_sn llpx_sn_fwd_drop_dx -*) diff --git a/matita/matita/contribs/lambdadelta/basic_2/relocation/lexs_lexs.ma b/matita/matita/contribs/lambdadelta/basic_2/relocation/lexs_lexs.ma index dbe74e5fd..35badac0e 100644 --- a/matita/matita/contribs/lambdadelta/basic_2/relocation/lexs_lexs.ma +++ b/matita/matita/contribs/lambdadelta/basic_2/relocation/lexs_lexs.ma @@ -21,11 +21,13 @@ include "basic_2/relocation/lexs.ma". (* Main properties **********************************************************) -(* Basic_2A1: includes: lpx_sn_trans *) -theorem lexs_trans (RN) (RP) (f): lexs_transitive RN RN RN RP → - lexs_transitive RP RP RN RP → - Transitive … (lexs RN RP f). -#RN #RP #f #HN #HP #L1 #L0 #H elim H -L1 -L0 -f +theorem lexs_trans_gen (RN1) (RP1) (RN2) (RP2) (RN) (RP) (f): + lexs_transitive RN1 RN2 RN RN1 RP1 → + lexs_transitive RP1 RP2 RP RN1 RP1 → + ∀L1,L0. L1 ⦻*[RN1, RP1, f] L0 → + ∀L2. L0 ⦻*[RN2, RP2, f] L2 → + L1 ⦻*[RN, RP, f] L2. +#RN1 #RP1 #RN2 #RP2 #RN #RP #f #HN #HP #L1 #L0 #H elim H -L1 -L0 -f [ #f #L2 #H >(lexs_inv_atom1 … H) -L2 // | #I #K1 #K #V1 #V #f #HK1 #HV1 #IH #L2 #H elim (lexs_inv_next1 … H) -H #K2 #V2 #HK2 #HV2 #H destruct /4 width=6 by lexs_next/ @@ -34,10 +36,16 @@ theorem lexs_trans (RN) (RP) (f): lexs_transitive RN RN RN RP → ] qed-. +(* Basic_2A1: includes: lpx_sn_trans *) +theorem lexs_trans (RN) (RP) (f): lexs_transitive RN RN RN RN RP → + lexs_transitive RP RP RP RN RP → + Transitive … (lexs RN RP f). +/2 width=9 by lexs_trans_gen/ qed-. + (* Basic_2A1: includes: lpx_sn_conf *) theorem lexs_conf: ∀RN1,RP1,RN2,RP2. - lpx_sn_confluent RN1 RN2 RN1 RP1 RN2 RP2 → - lpx_sn_confluent RP1 RP2 RN1 RP1 RN2 RP2 → + lexs_confluent RN1 RN2 RN1 RP1 RN2 RP2 → + lexs_confluent RP1 RP2 RN1 RP1 RN2 RP2 → ∀f. confluent2 … (lexs RN1 RP1 f) (lexs RN2 RP2 f). #RN1 #RP1 #RN2 #RP2 #HRN #HRP #f #L0 generalize in match f; -f @(f_ind … lw … L0) -L0 #x #IH * @@ -68,26 +76,28 @@ theorem lexs_canc_dx: ∀RN,RP,f. Transitive … (lexs RN RP f) → right_cancellable … (lexs RN RP f). /3 width=3 by/ qed-. -theorem lexs_meet: ∀RN,RP,L1,L2,f1. L1 ⦻*[RN, RP, f1] L2 → - ∀f2. L1 ⦻*[RN, RP, f2] L2 → - ∀f. f1 ⋒ f2 ≡ f → L1 ⦻*[RN, RP, f] L2. +lemma lexs_meet: ∀RN,RP,L1,L2. + ∀f1. L1 ⦻*[RN, RP, f1] L2 → + ∀f2. L1 ⦻*[RN, RP, f2] L2 → + ∀f. f1 ⋒ f2 ≡ f → L1 ⦻*[RN, RP, f] L2. #RN #RP #L1 #L2 #f1 #H elim H -L1 -L2 -f1 // -#I #L1 #L2 #V1 #V2 #f1 #_ #H1V #IH #f2 elim (pn_split f2) * -#g2 #H #H2 #f #Hf destruct -[1,3: elim (lexs_inv_push … H2) |2,4: elim (lexs_inv_next … H2) ] -H2 -#H2 #H2V #_ -[ elim (sand_inv_npx … Hf) | elim (sand_inv_ppx … Hf) | elim (sand_inv_nnx … Hf) | elim (sand_inv_pnx … Hf) ] -Hf -/3 width=5 by lexs_next, lexs_push/ +#I #L1 #L2 #V1 #V2 #f1 #_ #HV12 #IH #f2 #H #f #Hf +elim (pn_split f2) * #g2 #H2 destruct +try elim (lexs_inv_push … H) try elim (lexs_inv_next … H) -H +[ elim (sand_inv_npx … Hf) | elim (sand_inv_nnx … Hf) +| elim (sand_inv_ppx … Hf) | elim (sand_inv_pnx … Hf) +] -Hf /3 width=5 by lexs_next, lexs_push/ qed-. -theorem lexs_join: ∀RN,RP,L1,L2,f1. L1 ⦻*[RN, RP, f1] L2 → - ∀f2. L1 ⦻*[RN, RP, f2] L2 → - ∀f. f1 ⋓ f2 ≡ f → L1 ⦻*[RN, RP, f] L2. +lemma lexs_join: ∀RN,RP,L1,L2. + ∀f1. L1 ⦻*[RN, RP, f1] L2 → + ∀f2. L1 ⦻*[RN, RP, f2] L2 → + ∀f. f1 ⋓ f2 ≡ f → L1 ⦻*[RN, RP, f] L2. #RN #RP #L1 #L2 #f1 #H elim H -L1 -L2 -f1 // -#I #L1 #L2 #V1 #V2 #f1 #_ #H1V #IH #f2 elim (pn_split f2) * -#g2 #H #H2 #f #Hf destruct -[1,3: elim (lexs_inv_push … H2) |2,4: elim (lexs_inv_next … H2) ] -H2 -#H2 #H2V #_ -[ elim (sor_inv_npx … Hf) | elim (sor_inv_ppx … Hf) | elim (sor_inv_nnx … Hf) | elim (sor_inv_pnx … Hf) ] -Hf -/3 width=5 by lexs_next, lexs_push/ +#I #L1 #L2 #V1 #V2 #f1 #_ #HV12 #IH #f2 #H #f #Hf +elim (pn_split f2) * #g2 #H2 destruct +try elim (lexs_inv_push … H) try elim (lexs_inv_next … H) -H +[ elim (sor_inv_npx … Hf) | elim (sor_inv_nnx … Hf) +| elim (sor_inv_ppx … Hf) | elim (sor_inv_pnx … Hf) +] -Hf /3 width=5 by lexs_next, lexs_push/ qed-. diff --git a/matita/matita/contribs/lambdadelta/basic_2/static/aaa_lfeq.ma b/matita/matita/contribs/lambdadelta/basic_2/static/aaa_lfeq.ma new file mode 100644 index 000000000..e5d7d0b5b --- /dev/null +++ b/matita/matita/contribs/lambdadelta/basic_2/static/aaa_lfeq.ma @@ -0,0 +1,42 @@ +(**************************************************************************) +(* ___ *) +(* ||M|| *) +(* ||A|| A project by Andrea Asperti *) +(* ||T|| *) +(* ||I|| Developers: *) +(* ||T|| The HELM team. *) +(* ||A|| http://helm.cs.unibo.it *) +(* \ / *) +(* \ / This file is distributed under the terms of the *) +(* v GNU General Public License Version 2 *) +(* *) +(**************************************************************************) + +include "basic_2/static/lfeq_lreq.ma". +include "basic_2/static/aaa.ma". + +(* ATONIC ARITY ASSIGNMENT ON TERMS *****************************************) + +(* Properties with equivalence on referred entries **************************) + +lemma lfeq_aaa_trans: ∀G,L2,T,A. ⦃G, L2⦄ ⊢ T ⁝ A → + ∀L1. L1 ≡[T] L2 → ⦃G, L1⦄ ⊢ T ⁝ A. +#G #L2 #T #A #H elim H -G -L2 -T -A /2 width=1 by aaa_sort/ +[ #I #G #L2 #V2 #A #_ #IH #L1 #H + elim (lfeq_inv_zero_pair_dx … H) -H /3 width=1 by aaa_zero/ +| #I #G #L2 #V2 #A #i #_ #IH #L1 #H + elim (lfeq_inv_lref_pair_dx … H) -H /3 width=1 by aaa_lref/ +| #p #G #L2 #V #T #B #A #_ #_ #IHV #IHT #L1 #H + elim (lfeq_inv_bind … H) -H /3 width=2 by aaa_abbr/ +| #p #G #L2 #V #T #B #A #_ #_ #IHV #IHT #L1 #H + elim (lfeq_inv_bind … H) -H /3 width=1 by aaa_abst/ +| #G #L2 #V #T #B #A #_ #_ #IHV #IHT #L1 #H + elim (lfeq_inv_flat … H) -H /3 width=3 by aaa_appl/ +| #G #L2 #V #T #A #_ #_ #IHV #IHT #L1 #H + elim (lfeq_inv_flat … H) -H /3 width=1 by aaa_cast/ +] +qed-. + +lemma aaa_lfeq_conf: ∀G,L2,T,A. ⦃G, L2⦄ ⊢ T ⁝ A → + ∀L1. L2 ≡[T] L1 → ⦃G, L1⦄ ⊢ T ⁝ A. +/3 width=3 by lfeq_aaa_trans, lfeq_sym/ qed-. diff --git a/matita/matita/contribs/lambdadelta/basic_2/static/ffeq.ma b/matita/matita/contribs/lambdadelta/basic_2/static/ffeq.ma new file mode 100644 index 000000000..48eb1ec0f --- /dev/null +++ b/matita/matita/contribs/lambdadelta/basic_2/static/ffeq.ma @@ -0,0 +1,48 @@ +(**************************************************************************) +(* ___ *) +(* ||M|| *) +(* ||A|| A project by Andrea Asperti *) +(* ||T|| *) +(* ||I|| Developers: *) +(* ||T|| The HELM team. *) +(* ||A|| http://helm.cs.unibo.it *) +(* \ / *) +(* \ / This file is distributed under the terms of the *) +(* v GNU General Public License Version 2 *) +(* *) +(**************************************************************************) + +include "basic_2/notation/relations/lazyeq_6.ma". +include "basic_2/static/lfeq_lreq.ma". +include "basic_2/static/lfeq_fqup.ma". + +(* EQUIVALENCE FOR CLOSURES ON REFERRED ENTRIES *****************************) + +inductive ffeq (G) (L1) (T): relation3 genv lenv term ≝ +| fleq_intro: ∀L2. L1 ≡[T] L2 → ffeq G L1 T G L2 T +. + +interpretation + "equivalence on referred entries (closure)" + 'LazyEq G1 L1 T1 G2 L2 T2 = (ffeq G1 L1 T1 G2 L2 T2). + +(* Basic properties *********************************************************) + +lemma ffeq_refl: tri_reflexive … ffeq. +/2 width=1 by fleq_intro/ qed. + +lemma ffeq_sym: tri_symmetric … ffeq. +#G1 #G2 #L1 #L2 #T1 #T2 * -G1 -L1 -T1 /3 width=1 by fleq_intro, lfeq_sym/ +qed-. + +(* Basic inversion lemmas ***************************************************) + +lemma ffeq_inv_gen: ∀G1,G2,L1,L2,T1,T2. ⦃G1, L1, T1⦄ ≡ ⦃G2, L2, T2⦄ → + ∧∧ G1 = G2 & L1 ≡[T1] L2 & T1 = T2. +#G1 #G2 #L1 #L2 #T1 #T2 * -G2 -L2 -T2 /2 width=1 by and3_intro/ +qed-. + +(* Basic_2A1: removed theorems 6: + fleq_refl fleq_sym fleq_inv_gen + fleq_trans fleq_canc_sn fleq_canc_dx +*) diff --git a/matita/matita/contribs/lambdadelta/basic_2/static/ffeq_ffeq.ma b/matita/matita/contribs/lambdadelta/basic_2/static/ffeq_ffeq.ma new file mode 100644 index 000000000..e4a4cdd87 --- /dev/null +++ b/matita/matita/contribs/lambdadelta/basic_2/static/ffeq_ffeq.ma @@ -0,0 +1,33 @@ +(**************************************************************************) +(* ___ *) +(* ||M|| *) +(* ||A|| A project by Andrea Asperti *) +(* ||T|| *) +(* ||I|| Developers: *) +(* ||T|| The HELM team. *) +(* ||A|| http://helm.cs.unibo.it *) +(* \ / *) +(* \ / This file is distributed under the terms of the *) +(* v GNU General Public License Version 2 *) +(* *) +(**************************************************************************) + +include "basic_2/static/lfeq_lfeq.ma". +include "basic_2/static/ffeq.ma". + +(* EQUIVALENCE FOR CLOSURES ON REFERRED ENTRIES *****************************) + +(* Main properties **********************************************************) + +theorem ffeq_trans: tri_transitive … ffeq. +#G1 #G #L1 #L #T1 #T * -G -L -T +#L #HL1 #G2 #L2 #T2 * -G2 -L2 -T2 /3 width=3 by fleq_intro, lfeq_trans/ +qed-. + +theorem ffeq_canc_sn: ∀G,G1,G2,L,L1,L2,T,T1,T2. + ⦃G, L, T⦄ ≡ ⦃G1, L1, T1⦄→ ⦃G, L, T⦄ ≡ ⦃G2, L2, T2⦄ → ⦃G1, L1, T1⦄ ≡ ⦃G2, L2, T2⦄. +/3 width=5 by ffeq_trans, ffeq_sym/ qed-. + +theorem ffeq_canc_dx: ∀G1,G2,G,L1,L2,L,T1,T2,T. + ⦃G1, L1, T1⦄ ≡ ⦃G, L, T⦄ → ⦃G2, L2, T2⦄ ≡ ⦃G, L, T⦄ → ⦃G1, L1, T1⦄ ≡ ⦃G2, L2, T2⦄. +/3 width=5 by ffeq_trans, ffeq_sym/ qed-. diff --git a/matita/matita/contribs/lambdadelta/basic_2/static/frees_fqup.ma b/matita/matita/contribs/lambdadelta/basic_2/static/frees_fqup.ma index 8b182b560..797e4f324 100644 --- a/matita/matita/contribs/lambdadelta/basic_2/static/frees_fqup.ma +++ b/matita/matita/contribs/lambdadelta/basic_2/static/frees_fqup.ma @@ -12,7 +12,6 @@ (* *) (**************************************************************************) -include "ground_2/relocation/rtmap_id.ma". include "basic_2/s_computation/fqup_weight.ma". include "basic_2/static/frees.ma". diff --git a/matita/matita/contribs/lambdadelta/basic_2/static/freq.ma b/matita/matita/contribs/lambdadelta/basic_2/static/freq.ma deleted file mode 100644 index a66eb6487..000000000 --- a/matita/matita/contribs/lambdadelta/basic_2/static/freq.ma +++ /dev/null @@ -1,50 +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 *) -(* *) -(**************************************************************************) - -include "basic_2/notation/relations/lazyeq_6.ma". -include "basic_2/grammar/genv.ma". -include "basic_2/static/frees_fqup.ma". -include "basic_2/static/frees_lreq.ma". - -(* RANGED EQUIVALENCE FOR CLOSURES ******************************************) - -inductive freq (G) (L1) (T): relation3 genv lenv term ≝ -| fleq_intro: ∀L2,f. L1 ⊢ 𝐅*⦃T⦄ ≡ f → L1 ≡[f] L2 → freq G L1 T G L2 T -. - -interpretation - "ranged equivalence (closure)" - 'LazyEq G1 L1 T1 G2 L2 T2 = (freq G1 L1 T1 G2 L2 T2). - -(* Basic properties *********************************************************) - -lemma freq_refl: tri_reflexive … freq. -#G #L #T elim (frees_total L T) /2 width=3 by fleq_intro/ -qed. - -lemma freq_sym: tri_symmetric … freq. -#G1 #L1 #T1 #G2 #L2 #T2 * /4 width=3 by fleq_intro, frees_lreq_conf, lreq_sym/ -qed-. - -(* Basic inversion lemmas ***************************************************) - -lemma freq_inv_gen: ∀G1,G2,L1,L2,T1,T2. ⦃G1, L1, T1⦄ ≡ ⦃G2, L2, T2⦄ → - ∃∃f. G1 = G2 & L1 ⊢ 𝐅*⦃T1⦄ ≡ f & L1 ≡[f] L2 & T1 = T2. -#G1 #G2 #L1 #L2 #T1 #T2 * -G2 -L2 -T2 /2 width=3 by ex4_intro/ -qed-. - -(* Basic_2A1: removed theorems 6: - fleq_refl fleq_sym fleq_inv_gen - fleq_trans fleq_canc_sn fleq_canc_dx -*) diff --git a/matita/matita/contribs/lambdadelta/basic_2/static/freq_freq.ma b/matita/matita/contribs/lambdadelta/basic_2/static/freq_freq.ma deleted file mode 100644 index 4ff819570..000000000 --- a/matita/matita/contribs/lambdadelta/basic_2/static/freq_freq.ma +++ /dev/null @@ -1,37 +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 *) -(* *) -(**************************************************************************) - -include "basic_2/relocation/lreq_lreq.ma". -include "basic_2/static/frees_frees.ma". -include "basic_2/static/freq.ma". - -(* RANGED EQUIVALENCE FOR CLOSURES *****************************************) - -(* Main properties **********************************************************) - -theorem freq_trans: tri_transitive … freq. -#G1 #G #L1 #L #T1 #T * -G -L -T -#L #f1 #H1T11 #Hf1 #G2 #L2 #T2 * -G2 -L2 -T2 #L2 #f2 #HT12 #Hf2 -lapply (frees_lreq_conf … H1T11 … Hf1) #HT11 -lapply (frees_mono … HT12 … HT11) -HT11 -HT12 -/4 width=7 by fleq_intro, lreq_eq_repl_back, lreq_trans/ -qed-. - -theorem freq_canc_sn: ∀G,G1,G2,L,L1,L2,T,T1,T2. - ⦃G, L, T⦄ ≡ ⦃G1, L1, T1⦄→ ⦃G, L, T⦄ ≡ ⦃G2, L2, T2⦄ → ⦃G1, L1, T1⦄ ≡ ⦃G2, L2, T2⦄. -/3 width=5 by freq_trans, freq_sym/ qed-. - -theorem freq_canc_dx: ∀G1,G2,G,L1,L2,L,T1,T2,T. - ⦃G1, L1, T1⦄ ≡ ⦃G, L, T⦄ → ⦃G2, L2, T2⦄ ≡ ⦃G, L, T⦄ → ⦃G1, L1, T1⦄ ≡ ⦃G2, L2, T2⦄. -/3 width=5 by freq_trans, freq_sym/ qed-. diff --git a/matita/matita/contribs/lambdadelta/basic_2/static/lfeq.ma b/matita/matita/contribs/lambdadelta/basic_2/static/lfeq.ma new file mode 100644 index 000000000..28da143b8 --- /dev/null +++ b/matita/matita/contribs/lambdadelta/basic_2/static/lfeq.ma @@ -0,0 +1,136 @@ +(**************************************************************************) +(* ___ *) +(* ||M|| *) +(* ||A|| A project by Andrea Asperti *) +(* ||T|| *) +(* ||I|| Developers: *) +(* ||T|| The HELM team. *) +(* ||A|| http://helm.cs.unibo.it *) +(* \ / *) +(* \ / This file is distributed under the terms of the *) +(* v GNU General Public License Version 2 *) +(* *) +(**************************************************************************) + +include "basic_2/notation/relations/lazyeq_3.ma". +include "basic_2/static/lfxs.ma". + +(* EQUIVALENCE FOR LOCAL ENVIRONMENTS ON REFERRED ENTRIES *******************) + +definition lfeq: relation3 term lenv lenv ≝ lfxs ceq. + +interpretation + "equivalence on referred entries (local environment)" + 'LazyEq T L1 L2 = (lfeq T L1 L2). + +definition lfeq_transitive: predicate (relation3 lenv term term) ≝ + λR. ∀L2,T1,T2. R L2 T1 T2 → ∀L1. L1 ≡[T1] L2 → R L1 T1 T2. + +(* Basic properties ***********************************************************) + +lemma lfeq_atom: ∀I. ⋆ ≡[⓪{I}] ⋆. +/2 width=1 by lfxs_atom/ qed. + +lemma lfeq_sort: ∀I,L1,L2,V1,V2,s. + L1 ≡[⋆s] L2 → L1.ⓑ{I}V1 ≡[⋆s] L2.ⓑ{I}V2. +/2 width=1 by lfxs_sort/ qed. + +lemma lfeq_zero: ∀I,L1,L2,V. + L1 ≡[V] L2 → L1.ⓑ{I}V ≡[#0] L2.ⓑ{I}V. +/2 width=1 by lfxs_zero/ qed. + +lemma lfeq_lref: ∀I,L1,L2,V1,V2,i. + L1 ≡[#i] L2 → L1.ⓑ{I}V1 ≡[#⫯i] L2.ⓑ{I}V2. +/2 width=1 by lfxs_lref/ qed. + +lemma lfeq_gref: ∀I,L1,L2,V1,V2,l. + L1 ≡[§l] L2 → L1.ⓑ{I}V1 ≡[§l] L2.ⓑ{I}V2. +/2 width=1 by lfxs_gref/ qed. + +(* Basic inversion lemmas ***************************************************) + +lemma lfeq_inv_atom_sn: ∀I,Y2. ⋆ ≡[⓪{I}] Y2 → Y2 = ⋆. +/2 width=3 by lfxs_inv_atom_sn/ qed-. + +lemma lfeq_inv_atom_dx: ∀I,Y1. Y1 ≡[⓪{I}] ⋆ → Y1 = ⋆. +/2 width=3 by lfxs_inv_atom_dx/ qed-. + +lemma lfeq_inv_zero: ∀Y1,Y2. Y1 ≡[#0] Y2 → + (Y1 = ⋆ ∧ Y2 = ⋆) ∨ + ∃∃I,L1,L2,V. L1 ≡[V] L2 & + Y1 = L1.ⓑ{I}V & Y2 = L2.ⓑ{I}V. +#Y1 #Y2 #H elim (lfxs_inv_zero … H) -H * +/3 width=7 by ex3_4_intro, or_introl, or_intror, conj/ +qed-. + +lemma lfeq_inv_lref: ∀Y1,Y2,i. Y1 ≡[#⫯i] Y2 → + (Y1 = ⋆ ∧ Y2 = ⋆) ∨ + ∃∃I,L1,L2,V1,V2. L1 ≡[#i] L2 & + Y1 = L1.ⓑ{I}V1 & Y2 = L2.ⓑ{I}V2. +#Y1 #Y2 #i #H elim (lfxs_inv_lref … H) -H * +/3 width=8 by ex3_5_intro, or_introl, or_intror, conj/ +qed-. + +lemma lfeq_inv_bind: ∀I,L1,L2,V,T,p. L1 ≡[ⓑ{p,I}V.T] L2 → + L1 ≡[V] L2 ∧ L1.ⓑ{I}V ≡[T] L2.ⓑ{I}V. +#I #L1 #L2 #V #T #p #H elim (lfxs_inv_bind … H) -H /2 width=3 by conj/ +qed-. + +lemma lfeq_inv_flat: ∀I,L1,L2,V,T. L1 ≡[ⓕ{I}V.T] L2 → + L1 ≡[V] L2 ∧ L1 ≡[T] L2. +#I #L1 #L2 #V #T #H elim (lfxs_inv_flat … H) -H /2 width=3 by conj/ +qed-. + +(* Advanced inversion lemmas ************************************************) + +lemma lfeq_inv_zero_pair_sn: ∀I,Y2,L1,V. L1.ⓑ{I}V ≡[#0] Y2 → + ∃∃L2. L1 ≡[V] L2 & Y2 = L2.ⓑ{I}V. +#I #Y2 #L1 #V #H elim (lfxs_inv_zero_pair_sn … H) -H /2 width=3 by ex2_intro/ +qed-. + +lemma lfeq_inv_zero_pair_dx: ∀I,Y1,L2,V. Y1 ≡[#0] L2.ⓑ{I}V → + ∃∃L1. L1 ≡[V] L2 & Y1 = L1.ⓑ{I}V. +#I #Y1 #L2 #V #H elim (lfxs_inv_zero_pair_dx … H) -H +#L1 #X #HL12 #HX #H destruct /2 width=3 by ex2_intro/ +qed-. + +lemma lfeq_inv_lref_pair_sn: ∀I,Y2,L1,V1,i. L1.ⓑ{I}V1 ≡[#⫯i] Y2 → + ∃∃L2,V2. L1 ≡[#i] L2 & Y2 = L2.ⓑ{I}V2. +/2 width=2 by lfxs_inv_lref_pair_sn/ qed-. + +lemma lfeq_inv_lref_pair_dx: ∀I,Y1,L2,V2,i. Y1 ≡[#⫯i] L2.ⓑ{I}V2 → + ∃∃L1,V1. L1 ≡[#i] L2 & Y1 = L1.ⓑ{I}V1. +/2 width=2 by lfxs_inv_lref_pair_dx/ qed-. + +(* Basic forward lemmas *****************************************************) + +lemma lfeq_fwd_bind_sn: ∀I,L1,L2,V,T,p. L1 ≡[ⓑ{p,I}V.T] L2 → L1 ≡[V] L2. +/2 width=4 by lfxs_fwd_bind_sn/ qed-. + +lemma lfeq_fwd_bind_dx: ∀I,L1,L2,V,T,p. + L1 ≡[ⓑ{p,I}V.T] L2 → L1.ⓑ{I}V ≡[T] L2.ⓑ{I}V. +/2 width=2 by lfxs_fwd_bind_dx/ qed-. + +lemma lfeq_fwd_flat_sn: ∀I,L1,L2,V,T. L1 ≡[ⓕ{I}V.T] L2 → L1 ≡[V] L2. +/2 width=3 by lfxs_fwd_flat_sn/ qed-. + +lemma lfeq_fwd_flat_dx: ∀I,L1,L2,V,T. L1 ≡[ⓕ{I}V.T] L2 → L1 ≡[T] L2. +/2 width=3 by lfxs_fwd_flat_dx/ qed-. + +lemma lfeq_fwd_pair_sn: ∀I,L1,L2,V,T. L1 ≡[②{I}V.T] L2 → L1 ≡[V] L2. +/2 width=3 by lfxs_fwd_pair_sn/ qed-. + +(* Advanceded forward lemmas with generic extension on referred entries *****) + +lemma lfex_fwd_lfxs_refl: ∀R. (∀L. reflexive … (R L)) → + ∀L1,L2,T. L1 ≡[T] L2 → L1 ⦻*[R, T] L2. +/2 width=3 by lfxs_co/ qed-. + +(* Basic_2A1: removed theorems 30: + lleq_ind lleq_inv_bind lleq_inv_flat lleq_fwd_length lleq_fwd_lref + lleq_fwd_drop_sn lleq_fwd_drop_dx + lleq_fwd_bind_sn lleq_fwd_bind_dx lleq_fwd_flat_sn lleq_fwd_flat_dx + lleq_sort lleq_skip lleq_lref lleq_free lleq_gref lleq_bind lleq_flat + lleq_refl lleq_Y lleq_sym lleq_ge_up lleq_ge lleq_bind_O llpx_sn_lrefl + lleq_trans lleq_canc_sn lleq_canc_dx lleq_nlleq_trans nlleq_lleq_div +*) diff --git a/matita/matita/contribs/lambdadelta/basic_2/static/lfeq_fqup.ma b/matita/matita/contribs/lambdadelta/basic_2/static/lfeq_fqup.ma new file mode 100644 index 000000000..bb513ab37 --- /dev/null +++ b/matita/matita/contribs/lambdadelta/basic_2/static/lfeq_fqup.ma @@ -0,0 +1,23 @@ +(**************************************************************************) +(* ___ *) +(* ||M|| *) +(* ||A|| A project by Andrea Asperti *) +(* ||T|| *) +(* ||I|| Developers: *) +(* ||T|| The HELM team. *) +(* ||A|| http://helm.cs.unibo.it *) +(* \ / *) +(* \ / This file is distributed under the terms of the *) +(* v GNU General Public License Version 2 *) +(* *) +(**************************************************************************) + +include "basic_2/static/lfxs_fqup.ma". +include "basic_2/static/lfeq.ma". + +(* EQUIVALENCE FOR LOCAL ENVIRONMENTS ON REFERRED ENTRIES *******************) + +(* Advanced properties ******************************************************) + +lemma lfeq_refl: ∀T. reflexive … (lfeq T). +/2 width=1 by lfxs_refl/ qed. diff --git a/matita/matita/contribs/lambdadelta/basic_2/static/lfeq_length.ma b/matita/matita/contribs/lambdadelta/basic_2/static/lfeq_length.ma new file mode 100644 index 000000000..db2217702 --- /dev/null +++ b/matita/matita/contribs/lambdadelta/basic_2/static/lfeq_length.ma @@ -0,0 +1,23 @@ +(**************************************************************************) +(* ___ *) +(* ||M|| *) +(* ||A|| A project by Andrea Asperti *) +(* ||T|| *) +(* ||I|| Developers: *) +(* ||T|| The HELM team. *) +(* ||A|| http://helm.cs.unibo.it *) +(* \ / *) +(* \ / This file is distributed under the terms of the *) +(* v GNU General Public License Version 2 *) +(* *) +(**************************************************************************) + +include "basic_2/static/lfxs_length.ma". +include "basic_2/static/lfeq.ma". + +(* EQUIVALENCE FOR LOCAL ENVIRONMENTS ON REFERRED ENTRIES *******************) + +(* Forward lemmas with length for local environments ************************) + +lemma lfeq_fwd_length: ∀L1,L2,T. L1 ≡[T] L2 → |L1| = |L2|. +/2 width=3 by lfxs_fwd_length/ qed-. diff --git a/matita/matita/contribs/lambdadelta/basic_2/static/lfeq_lfeq.ma b/matita/matita/contribs/lambdadelta/basic_2/static/lfeq_lfeq.ma new file mode 100644 index 000000000..a6f564763 --- /dev/null +++ b/matita/matita/contribs/lambdadelta/basic_2/static/lfeq_lfeq.ma @@ -0,0 +1,56 @@ +(**************************************************************************) +(* ___ *) +(* ||M|| *) +(* ||A|| A project by Andrea Asperti *) +(* ||T|| *) +(* ||I|| Developers: *) +(* ||T|| The HELM team. *) +(* ||A|| http://helm.cs.unibo.it *) +(* \ / *) +(* \ / This file is distributed under the terms of the *) +(* v GNU General Public License Version 2 *) +(* *) +(**************************************************************************) + +include "basic_2/relocation/lreq_lreq.ma". +include "basic_2/static/frees_frees.ma". +include "basic_2/static/lfxs_lfxs.ma". +include "basic_2/static/lfeq_lreq.ma". + +(* EQUIVALENCE FOR LOCAL ENVIRONMENTS ON REFERRED ENTRIES *******************) + +(* Main properties **********************************************************) + +theorem lfeq_bind: ∀I,L1,L2,V1,V2,T,p. + L1 ≡[V1] L2 → L1.ⓑ{I}V1 ≡[T] L2.ⓑ{I}V2 → + L1 ≡[ⓑ{p,I}V1.T] L2. +/2 width=2 by lfxs_bind/ qed. + +theorem lfeq_flat: ∀I,L1,L2,V,T. L1 ≡[V] L2 → L1 ≡[T] L2 → + L1 ≡[ⓕ{I}V.T] L2. +/2 width=1 by lfxs_flat/ qed. + +(* Note: /2 width=3 by lfeq_lfxs_trans/ *) +theorem lfeq_trans: ∀T. Transitive … (lfeq T). +#T #L1 #L * #f1 #Hf1 #HL1 #L2 * #f2 #Hf2 #HL2 +lapply (frees_lreq_conf … Hf1 … HL1) #H0 +lapply (frees_mono … Hf2 … H0) -Hf2 -H0 +/4 width=7 by lreq_trans, lexs_eq_repl_back, ex2_intro/ +qed-. + +theorem lfeq_canc_sn: ∀T. left_cancellable … (lfeq T). +/3 width=3 by lfeq_trans, lfeq_sym/ qed-. + +theorem lfeq_canc_dx: ∀T. right_cancellable … (lfeq T). +/3 width=3 by lfeq_trans, lfeq_sym/ qed-. + +(* Advanced properies on negated lazy equivalence *****************************) + +(* Note: for use in auto, works with /4 width=8/ so lfeq_canc_sn is preferred *) +lemma lfeq_nlfeq_trans: ∀T,L1,L. L1 ≡[T] L → + ∀L2. (L ≡[T] L2 → ⊥) → (L1 ≡[T] L2 → ⊥). +/3 width=3 by lfeq_canc_sn/ qed-. + +lemma nlfeq_lfeq_div: ∀T,L2,L. L2 ≡[T] L → + ∀L1. (L1 ≡[T] L → ⊥) → (L1 ≡[T] L2 → ⊥). +/3 width=3 by lfeq_trans/ qed-. diff --git a/matita/matita/contribs/lambdadelta/basic_2/static/lfeq_lreq.ma b/matita/matita/contribs/lambdadelta/basic_2/static/lfeq_lreq.ma new file mode 100644 index 000000000..9021fbb75 --- /dev/null +++ b/matita/matita/contribs/lambdadelta/basic_2/static/lfeq_lreq.ma @@ -0,0 +1,36 @@ +(**************************************************************************) +(* ___ *) +(* ||M|| *) +(* ||A|| A project by Andrea Asperti *) +(* ||T|| *) +(* ||I|| Developers: *) +(* ||T|| The HELM team. *) +(* ||A|| http://helm.cs.unibo.it *) +(* \ / *) +(* \ / This file is distributed under the terms of the *) +(* v GNU General Public License Version 2 *) +(* *) +(**************************************************************************) + +include "basic_2/static/frees_lreq.ma". +include "basic_2/static/lfeq.ma". + +(* EQUIVALENCE FOR LOCAL ENVIRONMENTS ON REFERRED ENTRIES *******************) + +(* Inversion lemmas with ranged equivalence for local environments **********) + +lemma lfeq_inv_lreq: ∀L1,L2,T. L1 ≡[T] L2 → ∃∃f. L1 ⊢ 𝐅*⦃T⦄ ≡ f & L1 ≡[f] L2. +#L1 #L2 #T * /2 width=3 by ex2_intro/ +qed-. + +(* Properties with ranged equivalence for local environments ****************) + +lemma lreq_lfeq: ∀L1,L2,T,f. L1 ⊢ 𝐅*⦃T⦄ ≡ f → L1 ≡[f] L2 → L1 ≡[T] L2. +/2 width=3 by ex2_intro/ qed. + +(* Advanced properties ******************************************************) + +lemma lfeq_sym: ∀T. symmetric … (lfeq T). +#T #L1 #L2 #H elim (lfeq_inv_lreq … H) -H +/3 width=3 by lreq_lfeq, frees_lreq_conf, lreq_sym/ +qed-. diff --git a/matita/matita/contribs/lambdadelta/basic_2/static/lfxs.ma b/matita/matita/contribs/lambdadelta/basic_2/static/lfxs.ma new file mode 100644 index 000000000..5dcac52f0 --- /dev/null +++ b/matita/matita/contribs/lambdadelta/basic_2/static/lfxs.ma @@ -0,0 +1,174 @@ +(**************************************************************************) +(* ___ *) +(* ||M|| *) +(* ||A|| A project by Andrea Asperti *) +(* ||T|| *) +(* ||I|| Developers: *) +(* ||T|| The HELM team. *) +(* ||A|| http://helm.cs.unibo.it *) +(* \ / *) +(* \ / This file is distributed under the terms of the *) +(* v GNU General Public License Version 2 *) +(* *) +(**************************************************************************) + +include "ground_2/relocation/rtmap_id.ma". +include "basic_2/notation/relations/relationstar_4.ma". +include "basic_2/grammar/ceq.ma". +include "basic_2/relocation/lexs.ma". +include "basic_2/static/frees.ma". + +(* GENERIC EXTENSION ON REFERRED ENTRIES OF A CONTEXT-SENSITIVE REALTION ****) + +definition lfxs (R) (T): relation lenv ≝ + λL1,L2. ∃∃f. L1 ⊢ 𝐅*⦃T⦄ ≡ f & L1 ⦻*[R, cfull, f] L2. + +interpretation "generic extension on referred entries (local environment)" + 'RelationStar R T L1 L2 = (lfxs R T L1 L2). + +(* Basic properties ***********************************************************) + +lemma lfxs_atom: ∀R,I. ⋆ ⦻*[R, ⓪{I}] ⋆. +/3 width=3 by lexs_atom, frees_atom, ex2_intro/ +qed. + +lemma lfxs_sort: ∀R,I,L1,L2,V1,V2,s. + L1 ⦻*[R, ⋆s] L2 → L1.ⓑ{I}V1 ⦻*[R, ⋆s] L2.ⓑ{I}V2. +#R #I #L1 #L2 #V1 #V2 #s * /3 width=3 by lexs_push, frees_sort, ex2_intro/ +qed. + +lemma lfxs_zero: ∀R,I,L1,L2,V1,V2. L1 ⦻*[R, V1] L2 → + R L1 V1 V2 → L1.ⓑ{I}V1 ⦻*[R, #0] L2.ⓑ{I}V2. +#R #I #L1 #L2 #V1 #V2 * /3 width=3 by lexs_next, frees_zero, ex2_intro/ +qed. + +lemma lfxs_lref: ∀R,I,L1,L2,V1,V2,i. + L1 ⦻*[R, #i] L2 → L1.ⓑ{I}V1 ⦻*[R, #⫯i] L2.ⓑ{I}V2. +#R #I #L1 #L2 #V1 #V2 #i * /3 width=3 by lexs_push, frees_lref, ex2_intro/ +qed. + +lemma lfxs_gref: ∀R,I,L1,L2,V1,V2,l. + L1 ⦻*[R, §l] L2 → L1.ⓑ{I}V1 ⦻*[R, §l] L2.ⓑ{I}V2. +#R #I #L1 #L2 #V1 #V2 #l * /3 width=3 by lexs_push, frees_gref, ex2_intro/ +qed. + +lemma lfxs_co: ∀R1,R2. (∀L,T1,T2. R1 L T1 T2 → R2 L T1 T2) → + ∀L1,L2,T. L1 ⦻*[R1, T] L2 → L1 ⦻*[R2, T] L2. +#R1 #R2 #HR #L1 #L2 #T * /4 width=7 by lexs_co, ex2_intro/ +qed-. + +(* Basic inversion lemmas ***************************************************) + +lemma lfxs_inv_atom_sn: ∀R,I,Y2. ⋆ ⦻*[R, ⓪{I}] Y2 → Y2 = ⋆. +#R #I #Y2 * /2 width=4 by lexs_inv_atom1/ +qed-. + +lemma lfxs_inv_atom_dx: ∀R,I,Y1. Y1 ⦻*[R, ⓪{I}] ⋆ → Y1 = ⋆. +#R #I #Y1 * /2 width=4 by lexs_inv_atom2/ +qed-. + +lemma lfxs_inv_zero: ∀R,Y1,Y2. Y1 ⦻*[R, #0] Y2 → + (Y1 = ⋆ ∧ Y2 = ⋆) ∨ + ∃∃I,L1,L2,V1,V2. L1 ⦻*[R, V1] L2 & R L1 V1 V2 & + Y1 = L1.ⓑ{I}V1 & Y2 = L2.ⓑ{I}V2. +#R #Y1 #Y2 * #f #H1 #H2 elim (frees_inv_zero … H1) -H1 * +[ #H #_ lapply (lexs_inv_atom1_aux … H2 H) -H2 /3 width=1 by or_introl, conj/ +| #I1 #L1 #V1 #g #HV1 #HY1 #Hg elim (lexs_inv_next1_aux … H2 … HY1 Hg) -H2 -Hg + /4 width=9 by ex4_5_intro, ex2_intro, or_intror/ +] +qed-. + +lemma lfxs_inv_lref: ∀R,Y1,Y2,i. Y1 ⦻*[R, #⫯i] Y2 → + (Y1 = ⋆ ∧ Y2 = ⋆) ∨ + ∃∃I,L1,L2,V1,V2. L1 ⦻*[R, #i] L2 & + Y1 = L1.ⓑ{I}V1 & Y2 = L2.ⓑ{I}V2. +#R #Y1 #Y2 #i * #f #H1 #H2 elim (frees_inv_lref … H1) -H1 * +[ #H #_ lapply (lexs_inv_atom1_aux … H2 H) -H2 /3 width=1 by or_introl, conj/ +| #I1 #L1 #V1 #g #HV1 #HY1 #Hg elim (lexs_inv_push1_aux … H2 … HY1 Hg) -H2 -Hg + /4 width=8 by ex3_5_intro, ex2_intro, or_intror/ +] +qed-. + +lemma lfxs_inv_bind: ∀R,I,L1,L2,V1,V2,T,p. L1 ⦻*[R, ⓑ{p,I}V1.T] L2 → R L1 V1 V2 → + L1 ⦻*[R, V1] L2 ∧ L1.ⓑ{I}V1 ⦻*[R, T] L2.ⓑ{I}V2. +#R #I #L1 #L2 #V1 #V2 #T #p * #f #Hf #HL #HV elim (frees_inv_bind … Hf) -Hf +/6 width=6 by sle_lexs_trans, lexs_inv_tl, sor_inv_sle_dx, sor_inv_sle_sn, ex2_intro, conj/ +qed-. + +lemma lfxs_inv_flat: ∀R,I,L1,L2,V,T. L1 ⦻*[R, ⓕ{I}V.T] L2 → + L1 ⦻*[R, V] L2 ∧ L1 ⦻*[R, T] L2. +#R #I #L1 #L2 #V #T * #f #Hf #HL elim (frees_inv_flat … Hf) -Hf +/5 width=6 by sle_lexs_trans, sor_inv_sle_dx, sor_inv_sle_sn, ex2_intro, conj/ +qed-. + +(* Advanced inversion lemmas ************************************************) + +lemma lfxs_inv_zero_pair_sn: ∀R,I,Y2,L1,V1. L1.ⓑ{I}V1 ⦻*[R, #0] Y2 → + ∃∃L2,V2. L1 ⦻*[R, V1] L2 & R L1 V1 V2 & + Y2 = L2.ⓑ{I}V2. +#R #I #Y2 #L1 #V1 #H elim (lfxs_inv_zero … H) -H * +[ #H destruct +| #J #Y1 #L2 #X1 #V2 #HV1 #HV12 #H1 #H2 destruct + /2 width=5 by ex3_2_intro/ +] +qed-. + +lemma lfxs_inv_zero_pair_dx: ∀R,I,Y1,L2,V2. Y1 ⦻*[R, #0] L2.ⓑ{I}V2 → + ∃∃L1,V1. L1 ⦻*[R, V1] L2 & R L1 V1 V2 & + Y1 = L1.ⓑ{I}V1. +#R #I #Y1 #L2 #V2 #H elim (lfxs_inv_zero … H) -H * +[ #_ #H destruct +| #J #L1 #Y2 #V1 #X2 #HV1 #HV12 #H1 #H2 destruct + /2 width=5 by ex3_2_intro/ +] +qed-. + +lemma lfxs_inv_lref_pair_sn: ∀R,I,Y2,L1,V1,i. L1.ⓑ{I}V1 ⦻*[R, #⫯i] Y2 → + ∃∃L2,V2. L1 ⦻*[R, #i] L2 & Y2 = L2.ⓑ{I}V2. +#R #I #Y2 #L1 #V1 #i #H elim (lfxs_inv_lref … H) -H * +[ #H destruct +| #J #Y1 #L2 #X1 #V2 #Hi #H1 #H2 destruct /2 width=4 by ex2_2_intro/ +] +qed-. + +lemma lfxs_inv_lref_pair_dx: ∀R,I,Y1,L2,V2,i. Y1 ⦻*[R, #⫯i] L2.ⓑ{I}V2 → + ∃∃L1,V1. L1 ⦻*[R, #i] L2 & Y1 = L1.ⓑ{I}V1. +#R #I #Y1 #L2 #V2 #i #H elim (lfxs_inv_lref … H) -H * +[ #_ #H destruct +| #J #L1 #Y2 #V1 #X2 #Hi #H1 #H2 destruct /2 width=4 by ex2_2_intro/ +] +qed-. + +(* Basic forward lemmas *****************************************************) + +lemma lfxs_fwd_bind_sn: ∀R,I,L1,L2,V,T,p. L1 ⦻*[R, ⓑ{p,I}V.T] L2 → L1 ⦻*[R, V] L2. +#R #I #L1 #L2 #V #T #p * #f #Hf #HL elim (frees_inv_bind … Hf) -Hf +/4 width=6 by sle_lexs_trans, sor_inv_sle_sn, ex2_intro/ +qed-. + +lemma lfxs_fwd_bind_dx: ∀R,I,L1,L2,V1,V2,T,p. L1 ⦻*[R, ⓑ{p,I}V1.T] L2 → + R L1 V1 V2 → L1.ⓑ{I}V1 ⦻*[R, T] L2.ⓑ{I}V2. +#R #I #L1 #L2 #V1 #V2 #T #p #H #HV elim (lfxs_inv_bind … H HV) -H -HV // +qed-. + +lemma lfxs_fwd_flat_sn: ∀R,I,L1,L2,V,T. L1 ⦻*[R, ⓕ{I}V.T] L2 → L1 ⦻*[R, V] L2. +#R #I #L1 #L2 #V #T #H elim (lfxs_inv_flat … H) -H // +qed-. + +lemma lfxs_fwd_flat_dx: ∀R,I,L1,L2,V,T. L1 ⦻*[R, ⓕ{I}V.T] L2 → L1 ⦻*[R, T] L2. +#R #I #L1 #L2 #V #T #H elim (lfxs_inv_flat … H) -H // +qed-. + +lemma lfxs_fwd_pair_sn: ∀R,I,L1,L2,V,T. L1 ⦻*[R, ②{I}V.T] L2 → L1 ⦻*[R, V] L2. +#R * /2 width=4 by lfxs_fwd_flat_sn, lfxs_fwd_bind_sn/ +qed-. + +(* Basic_2A1: removed theorems 24: + llpx_sn_sort llpx_sn_skip llpx_sn_lref llpx_sn_free llpx_sn_gref + llpx_sn_bind llpx_sn_flat + llpx_sn_inv_bind llpx_sn_inv_flat + llpx_sn_fwd_lref llpx_sn_fwd_pair_sn llpx_sn_fwd_length + llpx_sn_fwd_bind_sn llpx_sn_fwd_bind_dx llpx_sn_fwd_flat_sn llpx_sn_fwd_flat_dx + llpx_sn_refl llpx_sn_Y llpx_sn_bind_O llpx_sn_ge_up llpx_sn_ge llpx_sn_co + llpx_sn_fwd_drop_sn llpx_sn_fwd_drop_dx +*) diff --git a/matita/matita/contribs/lambdadelta/basic_2/static/lfxs_fqup.ma b/matita/matita/contribs/lambdadelta/basic_2/static/lfxs_fqup.ma new file mode 100644 index 000000000..62c5b0564 --- /dev/null +++ b/matita/matita/contribs/lambdadelta/basic_2/static/lfxs_fqup.ma @@ -0,0 +1,24 @@ +(**************************************************************************) +(* ___ *) +(* ||M|| *) +(* ||A|| A project by Andrea Asperti *) +(* ||T|| *) +(* ||I|| Developers: *) +(* ||T|| The HELM team. *) +(* ||A|| http://helm.cs.unibo.it *) +(* \ / *) +(* \ / This file is distributed under the terms of the *) +(* v GNU General Public License Version 2 *) +(* *) +(**************************************************************************) + +include "basic_2/static/frees_fqup.ma". +include "basic_2/static/lfxs.ma". + +(* GENERIC EXTENSION ON REFERRED ENTRIES OF A CONTEXT-SENSITIVE REALTION ****) + +(* Advanced properties ******************************************************) + +lemma lfxs_refl: ∀R. (∀L. reflexive … (R L)) → ∀L,T. L ⦻*[R, T] L. +#R #HR #L #T elim (frees_total L T) /3 width=3 by lexs_refl, ex2_intro/ +qed. diff --git a/matita/matita/contribs/lambdadelta/basic_2/static/lfxs_length.ma b/matita/matita/contribs/lambdadelta/basic_2/static/lfxs_length.ma new file mode 100644 index 000000000..01dd82cf4 --- /dev/null +++ b/matita/matita/contribs/lambdadelta/basic_2/static/lfxs_length.ma @@ -0,0 +1,24 @@ +(**************************************************************************) +(* ___ *) +(* ||M|| *) +(* ||A|| A project by Andrea Asperti *) +(* ||T|| *) +(* ||I|| Developers: *) +(* ||T|| The HELM team. *) +(* ||A|| http://helm.cs.unibo.it *) +(* \ / *) +(* \ / This file is distributed under the terms of the *) +(* v GNU General Public License Version 2 *) +(* *) +(**************************************************************************) + +include "basic_2/relocation/lexs_length.ma". +include "basic_2/static/lfxs.ma". + +(* GENERIC EXTENSION ON REFERRED ENTRIES OF A CONTEXT-SENSITIVE REALTION ****) + +(* Forward lemmas with length for local environments ************************) + +lemma lfxs_fwd_length: ∀R,L1,L2,T. L1 ⦻*[R, T] L2 → |L1| = |L2|. +#R #L1 #L2 #T * /2 width=4 by lexs_fwd_length/ +qed-. diff --git a/matita/matita/contribs/lambdadelta/basic_2/static/lfxs_lfxs.ma b/matita/matita/contribs/lambdadelta/basic_2/static/lfxs_lfxs.ma new file mode 100644 index 000000000..04b4044be --- /dev/null +++ b/matita/matita/contribs/lambdadelta/basic_2/static/lfxs_lfxs.ma @@ -0,0 +1,35 @@ +(**************************************************************************) +(* ___ *) +(* ||M|| *) +(* ||A|| A project by Andrea Asperti *) +(* ||T|| *) +(* ||I|| Developers: *) +(* ||T|| The HELM team. *) +(* ||A|| http://helm.cs.unibo.it *) +(* \ / *) +(* \ / This file is distributed under the terms of the *) +(* v GNU General Public License Version 2 *) +(* *) +(**************************************************************************) + +include "basic_2/relocation/lexs_lexs.ma". +include "basic_2/static/lfxs.ma". + +(* GENERIC EXTENSION ON REFERRED ENTRIES OF A CONTEXT-SENSITIVE REALTION ****) + +(* Main properties ******************************************************) + +theorem lfxs_bind: ∀R,I,L1,L2,V1,V2,T,p. + L1 ⦻*[R, V1] L2 → L1.ⓑ{I}V1 ⦻*[R, T] L2.ⓑ{I}V2 → + L1 ⦻*[R, ⓑ{p,I}V1.T] L2. +#R #I #L1 #L2 #V1 #V2 #T #p * #f1 #HV #Hf1 * #f2 #HT #Hf2 +elim (lexs_fwd_pair … Hf2) -Hf2 #Hf2 #_ elim (sor_isfin_ex f1 (⫱f2)) +/3 width=7 by frees_fwd_isfin, frees_bind, lexs_join, isfin_tl, ex2_intro/ +qed. + +theorem lfxs_flat: ∀R,I,L1,L2,V,T. + L1 ⦻*[R, V] L2 → L1 ⦻*[R, T] L2 → + L1 ⦻*[R, ⓕ{I}V.T] L2. +#R #I #L1 #L2 #V #T * #f1 #HV #Hf1 * #f2 #HT #Hf2 elim (sor_isfin_ex f1 f2) +/3 width=7 by frees_fwd_isfin, frees_flat, lexs_join, ex2_intro/ +qed. diff --git a/matita/matita/contribs/lambdadelta/basic_2/web/basic_2_src.tbl b/matita/matita/contribs/lambdadelta/basic_2/web/basic_2_src.tbl index 35447f814..9d6e316b0 100644 --- a/matita/matita/contribs/lambdadelta/basic_2/web/basic_2_src.tbl +++ b/matita/matita/contribs/lambdadelta/basic_2/web/basic_2_src.tbl @@ -195,15 +195,23 @@ table { } ] [ { "atomic arity assignment" * } { - [ "aaa ( ⦃?,?⦄ ⊢ ? ⁝ ? )" "aaa_drops" + "aaa_fqus" + (* "aaa_lleq" + *) "aaa_aaa" * ] + [ "aaa ( ⦃?,?⦄ ⊢ ? ⁝ ? )" "aaa_drops" + "aaa_fqus" + "aaa_lfeq" + "aaa_aaa" * ] } ] [ { "restricted ref. for local env." * } { [ "lsubr ( ? ⫃ ? )" "lsubr_length" + "lsubr_drops" + "lsubr_lsubr" * ] } ] - [ { "ranged equivalence for closures" * } { - [ "freq ( ⦃?,?,?⦄ ≡ ⦃?,?,?⦄ )" "freq_freq" * ] + [ { "equivalence for closures on referred entries" * } { + [ "ffeq ( ⦃?,?,?⦄ ≡ ⦃?,?,?⦄ )" "ffeq_freq" * ] + } + ] + [ { "equivalence for local environments on referred entries" * } { + [ "lfeq ( ? ≡[?] ? )" "lfeq_length" + "lfeq_lreq" + "lfeq_fqup" + "lfeq_lfeq" * ] + } + ] + [ { "generic extension on referred entries" * } { + [ "lfxs ( ? ⦻*[?,?] ? )" "lfxs_length" + "lfxs_fqup" + "lfxs_lfxs" * ] } ] [ { "context-sensitive free variables" * } { @@ -246,7 +254,7 @@ table { [ "lreq ( ? ≡[?] ? )" "lreq_length" + "lreq_lreq" * ] } ] - [ { "generic entrywise extension of context-sensitive relations for terma" * } { + [ { "generic entrywise extension" * } { [ "lexs ( ? ⦻*[?,?,?] ? )" "lexs_length" + "lexs_lexs" * ] } ] diff --git a/matita/matita/contribs/lambdadelta/ground_2/lib/star.ma b/matita/matita/contribs/lambdadelta/ground_2/lib/star.ma index bf7f3b11f..8849d759b 100644 --- a/matita/matita/contribs/lambdadelta/ground_2/lib/star.ma +++ b/matita/matita/contribs/lambdadelta/ground_2/lib/star.ma @@ -17,6 +17,12 @@ include "ground_2/xoa/xoa_props.ma". (* PROPERTIES OF RELATIONS **************************************************) +definition relation5 : Type[0] → Type[0] → Type[0] → Type[0] → Type[0] → Type[0] +≝ λA,B,C,D,E.A→B→C→D→E→Prop. + +definition relation6 : Type[0] → Type[0] → Type[0] → Type[0] → Type[0] → Type[0] → Type[0] +≝ λA,B,C,D,E,F.A→B→C→D→E→F→Prop. + definition Decidable: Prop → Prop ≝ λR. R ∨ (R → ⊥). definition Transitive: ∀A. ∀R: relation A. Prop ≝ λA,R. diff --git a/matita/matita/contribs/lambdadelta/ground_2/notation/xoa_notation.ma b/matita/matita/contribs/lambdadelta/ground_2/notation/xoa_notation.ma index 6054aa308..dd3338c01 100644 --- a/matita/matita/contribs/lambdadelta/ground_2/notation/xoa_notation.ma +++ b/matita/matita/contribs/lambdadelta/ground_2/notation/xoa_notation.ma @@ -14,7 +14,7 @@ (* This file was generated by xoa.native: do not edit *********************) -(* multiple existental quantifier (1, 2) *) +(* multiple inductive existental quantifier (1, 2) *) notation > "hvbox(∃∃ ident x0 , ident x1 break . term 19 P0)" non associative with precedence 20 @@ -24,7 +24,7 @@ notation < "hvbox(∃∃ ident x0 , ident x1 break . term 19 P0)" non associative with precedence 20 for @{ 'Ex (λ${ident x0}:$T0.λ${ident x1}:$T1.$P0) }. -(* multiple existental quantifier (1, 3) *) +(* multiple inductive existental quantifier (1, 3) *) notation > "hvbox(∃∃ ident x0 , ident x1 , ident x2 break . term 19 P0)" non associative with precedence 20 @@ -34,7 +34,7 @@ notation < "hvbox(∃∃ ident x0 , ident x1 , ident x2 break . term 19 P0)" non associative with precedence 20 for @{ 'Ex (λ${ident x0}:$T0.λ${ident x1}:$T1.λ${ident x2}:$T2.$P0) }. -(* multiple existental quantifier (2, 2) *) +(* multiple inductive existental quantifier (2, 2) *) notation > "hvbox(∃∃ ident x0 , ident x1 break . term 19 P0 break & term 19 P1)" non associative with precedence 20 @@ -44,7 +44,7 @@ notation < "hvbox(∃∃ ident x0 , ident x1 break . term 19 P0 break & term 19 non associative with precedence 20 for @{ 'Ex (λ${ident x0}:$T0.λ${ident x1}:$T1.$P0) (λ${ident x0}:$T0.λ${ident x1}:$T1.$P1) }. -(* multiple existental quantifier (2, 3) *) +(* multiple inductive existental quantifier (2, 3) *) notation > "hvbox(∃∃ ident x0 , ident x1 , ident x2 break . term 19 P0 break & term 19 P1)" non associative with precedence 20 @@ -54,7 +54,7 @@ notation < "hvbox(∃∃ ident x0 , ident x1 , ident x2 break . term 19 P0 break non associative with precedence 20 for @{ 'Ex (λ${ident x0}:$T0.λ${ident x1}:$T1.λ${ident x2}:$T2.$P0) (λ${ident x0}:$T0.λ${ident x1}:$T1.λ${ident x2}:$T2.$P1) }. -(* multiple existental quantifier (3, 1) *) +(* multiple inductive existental quantifier (3, 1) *) notation > "hvbox(∃∃ ident x0 break . term 19 P0 break & term 19 P1 break & term 19 P2)" non associative with precedence 20 @@ -64,7 +64,7 @@ notation < "hvbox(∃∃ ident x0 break . term 19 P0 break & term 19 P1 break & non associative with precedence 20 for @{ 'Ex (λ${ident x0}:$T0.$P0) (λ${ident x0}:$T0.$P1) (λ${ident x0}:$T0.$P2) }. -(* multiple existental quantifier (3, 2) *) +(* multiple inductive existental quantifier (3, 2) *) notation > "hvbox(∃∃ ident x0 , ident x1 break . term 19 P0 break & term 19 P1 break & term 19 P2)" non associative with precedence 20 @@ -74,7 +74,7 @@ notation < "hvbox(∃∃ ident x0 , ident x1 break . term 19 P0 break & term 19 non associative with precedence 20 for @{ 'Ex (λ${ident x0}:$T0.λ${ident x1}:$T1.$P0) (λ${ident x0}:$T0.λ${ident x1}:$T1.$P1) (λ${ident x0}:$T0.λ${ident x1}:$T1.$P2) }. -(* multiple existental quantifier (3, 3) *) +(* multiple inductive existental quantifier (3, 3) *) notation > "hvbox(∃∃ ident x0 , ident x1 , ident x2 break . term 19 P0 break & term 19 P1 break & term 19 P2)" non associative with precedence 20 @@ -84,7 +84,7 @@ notation < "hvbox(∃∃ ident x0 , ident x1 , ident x2 break . term 19 P0 break non associative with precedence 20 for @{ 'Ex (λ${ident x0}:$T0.λ${ident x1}:$T1.λ${ident x2}:$T2.$P0) (λ${ident x0}:$T0.λ${ident x1}:$T1.λ${ident x2}:$T2.$P1) (λ${ident x0}:$T0.λ${ident x1}:$T1.λ${ident x2}:$T2.$P2) }. -(* multiple existental quantifier (3, 4) *) +(* multiple inductive existental quantifier (3, 4) *) notation > "hvbox(∃∃ ident x0 , ident x1 , ident x2 , ident x3 break . term 19 P0 break & term 19 P1 break & term 19 P2)" non associative with precedence 20 @@ -94,7 +94,17 @@ notation < "hvbox(∃∃ ident x0 , ident x1 , ident x2 , ident x3 break . term non associative with precedence 20 for @{ 'Ex (λ${ident x0}:$T0.λ${ident x1}:$T1.λ${ident x2}:$T2.λ${ident x3}:$T3.$P0) (λ${ident x0}:$T0.λ${ident x1}:$T1.λ${ident x2}:$T2.λ${ident x3}:$T3.$P1) (λ${ident x0}:$T0.λ${ident x1}:$T1.λ${ident x2}:$T2.λ${ident x3}:$T3.$P2) }. -(* multiple existental quantifier (4, 1) *) +(* multiple inductive existental quantifier (3, 5) *) + +notation > "hvbox(∃∃ ident x0 , ident x1 , ident x2 , ident x3 , ident x4 break . term 19 P0 break & term 19 P1 break & term 19 P2)" + non associative with precedence 20 + for @{ 'Ex (λ${ident x0}.λ${ident x1}.λ${ident x2}.λ${ident x3}.λ${ident x4}.$P0) (λ${ident x0}.λ${ident x1}.λ${ident x2}.λ${ident x3}.λ${ident x4}.$P1) (λ${ident x0}.λ${ident x1}.λ${ident x2}.λ${ident x3}.λ${ident x4}.$P2) }. + +notation < "hvbox(∃∃ ident x0 , ident x1 , ident x2 , ident x3 , ident x4 break . term 19 P0 break & term 19 P1 break & term 19 P2)" + non associative with precedence 20 + for @{ 'Ex (λ${ident x0}:$T0.λ${ident x1}:$T1.λ${ident x2}:$T2.λ${ident x3}:$T3.λ${ident x4}:$T4.$P0) (λ${ident x0}:$T0.λ${ident x1}:$T1.λ${ident x2}:$T2.λ${ident x3}:$T3.λ${ident x4}:$T4.$P1) (λ${ident x0}:$T0.λ${ident x1}:$T1.λ${ident x2}:$T2.λ${ident x3}:$T3.λ${ident x4}:$T4.$P2) }. + +(* multiple inductive existental quantifier (4, 1) *) notation > "hvbox(∃∃ ident x0 break . term 19 P0 break & term 19 P1 break & term 19 P2 break & term 19 P3)" non associative with precedence 20 @@ -104,7 +114,7 @@ notation < "hvbox(∃∃ ident x0 break . term 19 P0 break & term 19 P1 break & non associative with precedence 20 for @{ 'Ex (λ${ident x0}:$T0.$P0) (λ${ident x0}:$T0.$P1) (λ${ident x0}:$T0.$P2) (λ${ident x0}:$T0.$P3) }. -(* multiple existental quantifier (4, 2) *) +(* multiple inductive existental quantifier (4, 2) *) notation > "hvbox(∃∃ ident x0 , ident x1 break . term 19 P0 break & term 19 P1 break & term 19 P2 break & term 19 P3)" non associative with precedence 20 @@ -114,7 +124,7 @@ notation < "hvbox(∃∃ ident x0 , ident x1 break . term 19 P0 break & term 19 non associative with precedence 20 for @{ 'Ex (λ${ident x0}:$T0.λ${ident x1}:$T1.$P0) (λ${ident x0}:$T0.λ${ident x1}:$T1.$P1) (λ${ident x0}:$T0.λ${ident x1}:$T1.$P2) (λ${ident x0}:$T0.λ${ident x1}:$T1.$P3) }. -(* multiple existental quantifier (4, 3) *) +(* multiple inductive existental quantifier (4, 3) *) notation > "hvbox(∃∃ ident x0 , ident x1 , ident x2 break . term 19 P0 break & term 19 P1 break & term 19 P2 break & term 19 P3)" non associative with precedence 20 @@ -124,7 +134,7 @@ notation < "hvbox(∃∃ ident x0 , ident x1 , ident x2 break . term 19 P0 break non associative with precedence 20 for @{ 'Ex (λ${ident x0}:$T0.λ${ident x1}:$T1.λ${ident x2}:$T2.$P0) (λ${ident x0}:$T0.λ${ident x1}:$T1.λ${ident x2}:$T2.$P1) (λ${ident x0}:$T0.λ${ident x1}:$T1.λ${ident x2}:$T2.$P2) (λ${ident x0}:$T0.λ${ident x1}:$T1.λ${ident x2}:$T2.$P3) }. -(* multiple existental quantifier (4, 4) *) +(* multiple inductive existental quantifier (4, 4) *) notation > "hvbox(∃∃ ident x0 , ident x1 , ident x2 , ident x3 break . term 19 P0 break & term 19 P1 break & term 19 P2 break & term 19 P3)" non associative with precedence 20 @@ -134,7 +144,7 @@ notation < "hvbox(∃∃ ident x0 , ident x1 , ident x2 , ident x3 break . term non associative with precedence 20 for @{ 'Ex (λ${ident x0}:$T0.λ${ident x1}:$T1.λ${ident x2}:$T2.λ${ident x3}:$T3.$P0) (λ${ident x0}:$T0.λ${ident x1}:$T1.λ${ident x2}:$T2.λ${ident x3}:$T3.$P1) (λ${ident x0}:$T0.λ${ident x1}:$T1.λ${ident x2}:$T2.λ${ident x3}:$T3.$P2) (λ${ident x0}:$T0.λ${ident x1}:$T1.λ${ident x2}:$T2.λ${ident x3}:$T3.$P3) }. -(* multiple existental quantifier (4, 5) *) +(* multiple inductive existental quantifier (4, 5) *) notation > "hvbox(∃∃ ident x0 , ident x1 , ident x2 , ident x3 , ident x4 break . term 19 P0 break & term 19 P1 break & term 19 P2 break & term 19 P3)" non associative with precedence 20 @@ -144,7 +154,7 @@ notation < "hvbox(∃∃ ident x0 , ident x1 , ident x2 , ident x3 , ident x4 br non associative with precedence 20 for @{ 'Ex (λ${ident x0}:$T0.λ${ident x1}:$T1.λ${ident x2}:$T2.λ${ident x3}:$T3.λ${ident x4}:$T4.$P0) (λ${ident x0}:$T0.λ${ident x1}:$T1.λ${ident x2}:$T2.λ${ident x3}:$T3.λ${ident x4}:$T4.$P1) (λ${ident x0}:$T0.λ${ident x1}:$T1.λ${ident x2}:$T2.λ${ident x3}:$T3.λ${ident x4}:$T4.$P2) (λ${ident x0}:$T0.λ${ident x1}:$T1.λ${ident x2}:$T2.λ${ident x3}:$T3.λ${ident x4}:$T4.$P3) }. -(* multiple existental quantifier (5, 2) *) +(* multiple inductive existental quantifier (5, 2) *) notation > "hvbox(∃∃ ident x0 , ident x1 break . term 19 P0 break & term 19 P1 break & term 19 P2 break & term 19 P3 break & term 19 P4)" non associative with precedence 20 @@ -154,7 +164,7 @@ notation < "hvbox(∃∃ ident x0 , ident x1 break . term 19 P0 break & term 19 non associative with precedence 20 for @{ 'Ex (λ${ident x0}:$T0.λ${ident x1}:$T1.$P0) (λ${ident x0}:$T0.λ${ident x1}:$T1.$P1) (λ${ident x0}:$T0.λ${ident x1}:$T1.$P2) (λ${ident x0}:$T0.λ${ident x1}:$T1.$P3) (λ${ident x0}:$T0.λ${ident x1}:$T1.$P4) }. -(* multiple existental quantifier (5, 3) *) +(* multiple inductive existental quantifier (5, 3) *) notation > "hvbox(∃∃ ident x0 , ident x1 , ident x2 break . term 19 P0 break & term 19 P1 break & term 19 P2 break & term 19 P3 break & term 19 P4)" non associative with precedence 20 @@ -164,7 +174,7 @@ notation < "hvbox(∃∃ ident x0 , ident x1 , ident x2 break . term 19 P0 break non associative with precedence 20 for @{ 'Ex (λ${ident x0}:$T0.λ${ident x1}:$T1.λ${ident x2}:$T2.$P0) (λ${ident x0}:$T0.λ${ident x1}:$T1.λ${ident x2}:$T2.$P1) (λ${ident x0}:$T0.λ${ident x1}:$T1.λ${ident x2}:$T2.$P2) (λ${ident x0}:$T0.λ${ident x1}:$T1.λ${ident x2}:$T2.$P3) (λ${ident x0}:$T0.λ${ident x1}:$T1.λ${ident x2}:$T2.$P4) }. -(* multiple existental quantifier (5, 4) *) +(* multiple inductive existental quantifier (5, 4) *) notation > "hvbox(∃∃ ident x0 , ident x1 , ident x2 , ident x3 break . term 19 P0 break & term 19 P1 break & term 19 P2 break & term 19 P3 break & term 19 P4)" non associative with precedence 20 @@ -174,7 +184,7 @@ notation < "hvbox(∃∃ ident x0 , ident x1 , ident x2 , ident x3 break . term non associative with precedence 20 for @{ 'Ex (λ${ident x0}:$T0.λ${ident x1}:$T1.λ${ident x2}:$T2.λ${ident x3}:$T3.$P0) (λ${ident x0}:$T0.λ${ident x1}:$T1.λ${ident x2}:$T2.λ${ident x3}:$T3.$P1) (λ${ident x0}:$T0.λ${ident x1}:$T1.λ${ident x2}:$T2.λ${ident x3}:$T3.$P2) (λ${ident x0}:$T0.λ${ident x1}:$T1.λ${ident x2}:$T2.λ${ident x3}:$T3.$P3) (λ${ident x0}:$T0.λ${ident x1}:$T1.λ${ident x2}:$T2.λ${ident x3}:$T3.$P4) }. -(* multiple existental quantifier (5, 5) *) +(* multiple inductive existental quantifier (5, 5) *) notation > "hvbox(∃∃ ident x0 , ident x1 , ident x2 , ident x3 , ident x4 break . term 19 P0 break & term 19 P1 break & term 19 P2 break & term 19 P3 break & term 19 P4)" non associative with precedence 20 @@ -184,7 +194,7 @@ notation < "hvbox(∃∃ ident x0 , ident x1 , ident x2 , ident x3 , ident x4 br non associative with precedence 20 for @{ 'Ex (λ${ident x0}:$T0.λ${ident x1}:$T1.λ${ident x2}:$T2.λ${ident x3}:$T3.λ${ident x4}:$T4.$P0) (λ${ident x0}:$T0.λ${ident x1}:$T1.λ${ident x2}:$T2.λ${ident x3}:$T3.λ${ident x4}:$T4.$P1) (λ${ident x0}:$T0.λ${ident x1}:$T1.λ${ident x2}:$T2.λ${ident x3}:$T3.λ${ident x4}:$T4.$P2) (λ${ident x0}:$T0.λ${ident x1}:$T1.λ${ident x2}:$T2.λ${ident x3}:$T3.λ${ident x4}:$T4.$P3) (λ${ident x0}:$T0.λ${ident x1}:$T1.λ${ident x2}:$T2.λ${ident x3}:$T3.λ${ident x4}:$T4.$P4) }. -(* multiple existental quantifier (5, 6) *) +(* multiple inductive existental quantifier (5, 6) *) notation > "hvbox(∃∃ ident x0 , ident x1 , ident x2 , ident x3 , ident x4 , ident x5 break . term 19 P0 break & term 19 P1 break & term 19 P2 break & term 19 P3 break & term 19 P4)" non associative with precedence 20 @@ -194,7 +204,7 @@ notation < "hvbox(∃∃ ident x0 , ident x1 , ident x2 , ident x3 , ident x4 , non associative with precedence 20 for @{ 'Ex (λ${ident x0}:$T0.λ${ident x1}:$T1.λ${ident x2}:$T2.λ${ident x3}:$T3.λ${ident x4}:$T4.λ${ident x5}:$T5.$P0) (λ${ident x0}:$T0.λ${ident x1}:$T1.λ${ident x2}:$T2.λ${ident x3}:$T3.λ${ident x4}:$T4.λ${ident x5}:$T5.$P1) (λ${ident x0}:$T0.λ${ident x1}:$T1.λ${ident x2}:$T2.λ${ident x3}:$T3.λ${ident x4}:$T4.λ${ident x5}:$T5.$P2) (λ${ident x0}:$T0.λ${ident x1}:$T1.λ${ident x2}:$T2.λ${ident x3}:$T3.λ${ident x4}:$T4.λ${ident x5}:$T5.$P3) (λ${ident x0}:$T0.λ${ident x1}:$T1.λ${ident x2}:$T2.λ${ident x3}:$T3.λ${ident x4}:$T4.λ${ident x5}:$T5.$P4) }. -(* multiple existental quantifier (6, 3) *) +(* multiple inductive existental quantifier (6, 3) *) notation > "hvbox(∃∃ ident x0 , ident x1 , ident x2 break . term 19 P0 break & term 19 P1 break & term 19 P2 break & term 19 P3 break & term 19 P4 break & term 19 P5)" non associative with precedence 20 @@ -204,7 +214,7 @@ notation < "hvbox(∃∃ ident x0 , ident x1 , ident x2 break . term 19 P0 break non associative with precedence 20 for @{ 'Ex (λ${ident x0}:$T0.λ${ident x1}:$T1.λ${ident x2}:$T2.$P0) (λ${ident x0}:$T0.λ${ident x1}:$T1.λ${ident x2}:$T2.$P1) (λ${ident x0}:$T0.λ${ident x1}:$T1.λ${ident x2}:$T2.$P2) (λ${ident x0}:$T0.λ${ident x1}:$T1.λ${ident x2}:$T2.$P3) (λ${ident x0}:$T0.λ${ident x1}:$T1.λ${ident x2}:$T2.$P4) (λ${ident x0}:$T0.λ${ident x1}:$T1.λ${ident x2}:$T2.$P5) }. -(* multiple existental quantifier (6, 4) *) +(* multiple inductive existental quantifier (6, 4) *) notation > "hvbox(∃∃ ident x0 , ident x1 , ident x2 , ident x3 break . term 19 P0 break & term 19 P1 break & term 19 P2 break & term 19 P3 break & term 19 P4 break & term 19 P5)" non associative with precedence 20 @@ -214,7 +224,7 @@ notation < "hvbox(∃∃ ident x0 , ident x1 , ident x2 , ident x3 break . term non associative with precedence 20 for @{ 'Ex (λ${ident x0}:$T0.λ${ident x1}:$T1.λ${ident x2}:$T2.λ${ident x3}:$T3.$P0) (λ${ident x0}:$T0.λ${ident x1}:$T1.λ${ident x2}:$T2.λ${ident x3}:$T3.$P1) (λ${ident x0}:$T0.λ${ident x1}:$T1.λ${ident x2}:$T2.λ${ident x3}:$T3.$P2) (λ${ident x0}:$T0.λ${ident x1}:$T1.λ${ident x2}:$T2.λ${ident x3}:$T3.$P3) (λ${ident x0}:$T0.λ${ident x1}:$T1.λ${ident x2}:$T2.λ${ident x3}:$T3.$P4) (λ${ident x0}:$T0.λ${ident x1}:$T1.λ${ident x2}:$T2.λ${ident x3}:$T3.$P5) }. -(* multiple existental quantifier (6, 5) *) +(* multiple inductive existental quantifier (6, 5) *) notation > "hvbox(∃∃ ident x0 , ident x1 , ident x2 , ident x3 , ident x4 break . term 19 P0 break & term 19 P1 break & term 19 P2 break & term 19 P3 break & term 19 P4 break & term 19 P5)" non associative with precedence 20 @@ -224,7 +234,7 @@ notation < "hvbox(∃∃ ident x0 , ident x1 , ident x2 , ident x3 , ident x4 br non associative with precedence 20 for @{ 'Ex (λ${ident x0}:$T0.λ${ident x1}:$T1.λ${ident x2}:$T2.λ${ident x3}:$T3.λ${ident x4}:$T4.$P0) (λ${ident x0}:$T0.λ${ident x1}:$T1.λ${ident x2}:$T2.λ${ident x3}:$T3.λ${ident x4}:$T4.$P1) (λ${ident x0}:$T0.λ${ident x1}:$T1.λ${ident x2}:$T2.λ${ident x3}:$T3.λ${ident x4}:$T4.$P2) (λ${ident x0}:$T0.λ${ident x1}:$T1.λ${ident x2}:$T2.λ${ident x3}:$T3.λ${ident x4}:$T4.$P3) (λ${ident x0}:$T0.λ${ident x1}:$T1.λ${ident x2}:$T2.λ${ident x3}:$T3.λ${ident x4}:$T4.$P4) (λ${ident x0}:$T0.λ${ident x1}:$T1.λ${ident x2}:$T2.λ${ident x3}:$T3.λ${ident x4}:$T4.$P5) }. -(* multiple existental quantifier (6, 6) *) +(* multiple inductive existental quantifier (6, 6) *) notation > "hvbox(∃∃ ident x0 , ident x1 , ident x2 , ident x3 , ident x4 , ident x5 break . term 19 P0 break & term 19 P1 break & term 19 P2 break & term 19 P3 break & term 19 P4 break & term 19 P5)" non associative with precedence 20 @@ -234,7 +244,7 @@ notation < "hvbox(∃∃ ident x0 , ident x1 , ident x2 , ident x3 , ident x4 , non associative with precedence 20 for @{ 'Ex (λ${ident x0}:$T0.λ${ident x1}:$T1.λ${ident x2}:$T2.λ${ident x3}:$T3.λ${ident x4}:$T4.λ${ident x5}:$T5.$P0) (λ${ident x0}:$T0.λ${ident x1}:$T1.λ${ident x2}:$T2.λ${ident x3}:$T3.λ${ident x4}:$T4.λ${ident x5}:$T5.$P1) (λ${ident x0}:$T0.λ${ident x1}:$T1.λ${ident x2}:$T2.λ${ident x3}:$T3.λ${ident x4}:$T4.λ${ident x5}:$T5.$P2) (λ${ident x0}:$T0.λ${ident x1}:$T1.λ${ident x2}:$T2.λ${ident x3}:$T3.λ${ident x4}:$T4.λ${ident x5}:$T5.$P3) (λ${ident x0}:$T0.λ${ident x1}:$T1.λ${ident x2}:$T2.λ${ident x3}:$T3.λ${ident x4}:$T4.λ${ident x5}:$T5.$P4) (λ${ident x0}:$T0.λ${ident x1}:$T1.λ${ident x2}:$T2.λ${ident x3}:$T3.λ${ident x4}:$T4.λ${ident x5}:$T5.$P5) }. -(* multiple existental quantifier (6, 7) *) +(* multiple inductive existental quantifier (6, 7) *) notation > "hvbox(∃∃ ident x0 , ident x1 , ident x2 , ident x3 , ident x4 , ident x5 , ident x6 break . term 19 P0 break & term 19 P1 break & term 19 P2 break & term 19 P3 break & term 19 P4 break & term 19 P5)" non associative with precedence 20 @@ -244,7 +254,7 @@ notation < "hvbox(∃∃ ident x0 , ident x1 , ident x2 , ident x3 , ident x4 , non associative with precedence 20 for @{ 'Ex (λ${ident x0}:$T0.λ${ident x1}:$T1.λ${ident x2}:$T2.λ${ident x3}:$T3.λ${ident x4}:$T4.λ${ident x5}:$T5.λ${ident x6}:$T6.$P0) (λ${ident x0}:$T0.λ${ident x1}:$T1.λ${ident x2}:$T2.λ${ident x3}:$T3.λ${ident x4}:$T4.λ${ident x5}:$T5.λ${ident x6}:$T6.$P1) (λ${ident x0}:$T0.λ${ident x1}:$T1.λ${ident x2}:$T2.λ${ident x3}:$T3.λ${ident x4}:$T4.λ${ident x5}:$T5.λ${ident x6}:$T6.$P2) (λ${ident x0}:$T0.λ${ident x1}:$T1.λ${ident x2}:$T2.λ${ident x3}:$T3.λ${ident x4}:$T4.λ${ident x5}:$T5.λ${ident x6}:$T6.$P3) (λ${ident x0}:$T0.λ${ident x1}:$T1.λ${ident x2}:$T2.λ${ident x3}:$T3.λ${ident x4}:$T4.λ${ident x5}:$T5.λ${ident x6}:$T6.$P4) (λ${ident x0}:$T0.λ${ident x1}:$T1.λ${ident x2}:$T2.λ${ident x3}:$T3.λ${ident x4}:$T4.λ${ident x5}:$T5.λ${ident x6}:$T6.$P5) }. -(* multiple existental quantifier (7, 3) *) +(* multiple inductive existental quantifier (7, 3) *) notation > "hvbox(∃∃ ident x0 , ident x1 , ident x2 break . term 19 P0 break & term 19 P1 break & term 19 P2 break & term 19 P3 break & term 19 P4 break & term 19 P5 break & term 19 P6)" non associative with precedence 20 @@ -254,7 +264,7 @@ notation < "hvbox(∃∃ ident x0 , ident x1 , ident x2 break . term 19 P0 break non associative with precedence 20 for @{ 'Ex (λ${ident x0}:$T0.λ${ident x1}:$T1.λ${ident x2}:$T2.$P0) (λ${ident x0}:$T0.λ${ident x1}:$T1.λ${ident x2}:$T2.$P1) (λ${ident x0}:$T0.λ${ident x1}:$T1.λ${ident x2}:$T2.$P2) (λ${ident x0}:$T0.λ${ident x1}:$T1.λ${ident x2}:$T2.$P3) (λ${ident x0}:$T0.λ${ident x1}:$T1.λ${ident x2}:$T2.$P4) (λ${ident x0}:$T0.λ${ident x1}:$T1.λ${ident x2}:$T2.$P5) (λ${ident x0}:$T0.λ${ident x1}:$T1.λ${ident x2}:$T2.$P6) }. -(* multiple existental quantifier (7, 4) *) +(* multiple inductive existental quantifier (7, 4) *) notation > "hvbox(∃∃ ident x0 , ident x1 , ident x2 , ident x3 break . term 19 P0 break & term 19 P1 break & term 19 P2 break & term 19 P3 break & term 19 P4 break & term 19 P5 break & term 19 P6)" non associative with precedence 20 @@ -264,7 +274,7 @@ notation < "hvbox(∃∃ ident x0 , ident x1 , ident x2 , ident x3 break . term non associative with precedence 20 for @{ 'Ex (λ${ident x0}:$T0.λ${ident x1}:$T1.λ${ident x2}:$T2.λ${ident x3}:$T3.$P0) (λ${ident x0}:$T0.λ${ident x1}:$T1.λ${ident x2}:$T2.λ${ident x3}:$T3.$P1) (λ${ident x0}:$T0.λ${ident x1}:$T1.λ${ident x2}:$T2.λ${ident x3}:$T3.$P2) (λ${ident x0}:$T0.λ${ident x1}:$T1.λ${ident x2}:$T2.λ${ident x3}:$T3.$P3) (λ${ident x0}:$T0.λ${ident x1}:$T1.λ${ident x2}:$T2.λ${ident x3}:$T3.$P4) (λ${ident x0}:$T0.λ${ident x1}:$T1.λ${ident x2}:$T2.λ${ident x3}:$T3.$P5) (λ${ident x0}:$T0.λ${ident x1}:$T1.λ${ident x2}:$T2.λ${ident x3}:$T3.$P6) }. -(* multiple existental quantifier (7, 7) *) +(* multiple inductive existental quantifier (7, 7) *) notation > "hvbox(∃∃ ident x0 , ident x1 , ident x2 , ident x3 , ident x4 , ident x5 , ident x6 break . term 19 P0 break & term 19 P1 break & term 19 P2 break & term 19 P3 break & term 19 P4 break & term 19 P5 break & term 19 P6)" non associative with precedence 20 @@ -274,7 +284,7 @@ notation < "hvbox(∃∃ ident x0 , ident x1 , ident x2 , ident x3 , ident x4 , non associative with precedence 20 for @{ 'Ex (λ${ident x0}:$T0.λ${ident x1}:$T1.λ${ident x2}:$T2.λ${ident x3}:$T3.λ${ident x4}:$T4.λ${ident x5}:$T5.λ${ident x6}:$T6.$P0) (λ${ident x0}:$T0.λ${ident x1}:$T1.λ${ident x2}:$T2.λ${ident x3}:$T3.λ${ident x4}:$T4.λ${ident x5}:$T5.λ${ident x6}:$T6.$P1) (λ${ident x0}:$T0.λ${ident x1}:$T1.λ${ident x2}:$T2.λ${ident x3}:$T3.λ${ident x4}:$T4.λ${ident x5}:$T5.λ${ident x6}:$T6.$P2) (λ${ident x0}:$T0.λ${ident x1}:$T1.λ${ident x2}:$T2.λ${ident x3}:$T3.λ${ident x4}:$T4.λ${ident x5}:$T5.λ${ident x6}:$T6.$P3) (λ${ident x0}:$T0.λ${ident x1}:$T1.λ${ident x2}:$T2.λ${ident x3}:$T3.λ${ident x4}:$T4.λ${ident x5}:$T5.λ${ident x6}:$T6.$P4) (λ${ident x0}:$T0.λ${ident x1}:$T1.λ${ident x2}:$T2.λ${ident x3}:$T3.λ${ident x4}:$T4.λ${ident x5}:$T5.λ${ident x6}:$T6.$P5) (λ${ident x0}:$T0.λ${ident x1}:$T1.λ${ident x2}:$T2.λ${ident x3}:$T3.λ${ident x4}:$T4.λ${ident x5}:$T5.λ${ident x6}:$T6.$P6) }. -(* multiple existental quantifier (8, 4) *) +(* multiple inductive existental quantifier (8, 4) *) notation > "hvbox(∃∃ ident x0 , ident x1 , ident x2 , ident x3 break . term 19 P0 break & term 19 P1 break & term 19 P2 break & term 19 P3 break & term 19 P4 break & term 19 P5 break & term 19 P6 break & term 19 P7)" non associative with precedence 20 @@ -284,7 +294,7 @@ notation < "hvbox(∃∃ ident x0 , ident x1 , ident x2 , ident x3 break . term non associative with precedence 20 for @{ 'Ex (λ${ident x0}:$T0.λ${ident x1}:$T1.λ${ident x2}:$T2.λ${ident x3}:$T3.$P0) (λ${ident x0}:$T0.λ${ident x1}:$T1.λ${ident x2}:$T2.λ${ident x3}:$T3.$P1) (λ${ident x0}:$T0.λ${ident x1}:$T1.λ${ident x2}:$T2.λ${ident x3}:$T3.$P2) (λ${ident x0}:$T0.λ${ident x1}:$T1.λ${ident x2}:$T2.λ${ident x3}:$T3.$P3) (λ${ident x0}:$T0.λ${ident x1}:$T1.λ${ident x2}:$T2.λ${ident x3}:$T3.$P4) (λ${ident x0}:$T0.λ${ident x1}:$T1.λ${ident x2}:$T2.λ${ident x3}:$T3.$P5) (λ${ident x0}:$T0.λ${ident x1}:$T1.λ${ident x2}:$T2.λ${ident x3}:$T3.$P6) (λ${ident x0}:$T0.λ${ident x1}:$T1.λ${ident x2}:$T2.λ${ident x3}:$T3.$P7) }. -(* multiple existental quantifier (8, 5) *) +(* multiple inductive existental quantifier (8, 5) *) notation > "hvbox(∃∃ ident x0 , ident x1 , ident x2 , ident x3 , ident x4 break . term 19 P0 break & term 19 P1 break & term 19 P2 break & term 19 P3 break & term 19 P4 break & term 19 P5 break & term 19 P6 break & term 19 P7)" non associative with precedence 20 diff --git a/matita/matita/contribs/lambdadelta/ground_2/xoa.conf.xml b/matita/matita/contribs/lambdadelta/ground_2/xoa.conf.xml index 6a564d40d..55e67257b 100644 --- a/matita/matita/contribs/lambdadelta/ground_2/xoa.conf.xml +++ b/matita/matita/contribs/lambdadelta/ground_2/xoa.conf.xml @@ -13,6 +13,7 @@ 3 2 3 3 3 4 + 3 5 4 1 4 2 4 3 diff --git a/matita/matita/contribs/lambdadelta/ground_2/xoa/xoa.ma b/matita/matita/contribs/lambdadelta/ground_2/xoa/xoa.ma index f103fe747..7f46fe493 100644 --- a/matita/matita/contribs/lambdadelta/ground_2/xoa/xoa.ma +++ b/matita/matita/contribs/lambdadelta/ground_2/xoa/xoa.ma @@ -18,229 +18,237 @@ include "basics/pts.ma". include "ground_2/notation/xoa_notation.ma". -(* multiple existental quantifier (1, 2) *) +(* multiple inductive existental quantifier (1, 2) *) inductive ex1_2 (A0,A1:Type[0]) (P0:A0→A1→Prop) : Prop ≝ | ex1_2_intro: ∀x0,x1. P0 x0 x1 → ex1_2 ? ? ? . -interpretation "multiple existental quantifier (1, 2)" 'Ex P0 = (ex1_2 ? ? P0). +interpretation "multiple inductive existental quantifier (1, 2)" 'Ex P0 = (ex1_2 ? ? P0). -(* multiple existental quantifier (1, 3) *) +(* multiple inductive existental quantifier (1, 3) *) inductive ex1_3 (A0,A1,A2:Type[0]) (P0:A0→A1→A2→Prop) : Prop ≝ | ex1_3_intro: ∀x0,x1,x2. P0 x0 x1 x2 → ex1_3 ? ? ? ? . -interpretation "multiple existental quantifier (1, 3)" 'Ex P0 = (ex1_3 ? ? ? P0). +interpretation "multiple inductive existental quantifier (1, 3)" 'Ex P0 = (ex1_3 ? ? ? P0). -(* multiple existental quantifier (2, 2) *) +(* multiple inductive existental quantifier (2, 2) *) inductive ex2_2 (A0,A1:Type[0]) (P0,P1:A0→A1→Prop) : Prop ≝ | ex2_2_intro: ∀x0,x1. P0 x0 x1 → P1 x0 x1 → ex2_2 ? ? ? ? . -interpretation "multiple existental quantifier (2, 2)" 'Ex P0 P1 = (ex2_2 ? ? P0 P1). +interpretation "multiple inductive existental quantifier (2, 2)" 'Ex P0 P1 = (ex2_2 ? ? P0 P1). -(* multiple existental quantifier (2, 3) *) +(* multiple inductive existental quantifier (2, 3) *) inductive ex2_3 (A0,A1,A2:Type[0]) (P0,P1:A0→A1→A2→Prop) : Prop ≝ | ex2_3_intro: ∀x0,x1,x2. P0 x0 x1 x2 → P1 x0 x1 x2 → ex2_3 ? ? ? ? ? . -interpretation "multiple existental quantifier (2, 3)" 'Ex P0 P1 = (ex2_3 ? ? ? P0 P1). +interpretation "multiple inductive existental quantifier (2, 3)" 'Ex P0 P1 = (ex2_3 ? ? ? P0 P1). -(* multiple existental quantifier (3, 1) *) +(* multiple inductive existental quantifier (3, 1) *) inductive ex3 (A0:Type[0]) (P0,P1,P2:A0→Prop) : Prop ≝ | ex3_intro: ∀x0. P0 x0 → P1 x0 → P2 x0 → ex3 ? ? ? ? . -interpretation "multiple existental quantifier (3, 1)" 'Ex P0 P1 P2 = (ex3 ? P0 P1 P2). +interpretation "multiple inductive existental quantifier (3, 1)" 'Ex P0 P1 P2 = (ex3 ? P0 P1 P2). -(* multiple existental quantifier (3, 2) *) +(* multiple inductive existental quantifier (3, 2) *) inductive ex3_2 (A0,A1:Type[0]) (P0,P1,P2:A0→A1→Prop) : Prop ≝ | ex3_2_intro: ∀x0,x1. P0 x0 x1 → P1 x0 x1 → P2 x0 x1 → ex3_2 ? ? ? ? ? . -interpretation "multiple existental quantifier (3, 2)" 'Ex P0 P1 P2 = (ex3_2 ? ? P0 P1 P2). +interpretation "multiple inductive existental quantifier (3, 2)" 'Ex P0 P1 P2 = (ex3_2 ? ? P0 P1 P2). -(* multiple existental quantifier (3, 3) *) +(* multiple inductive existental quantifier (3, 3) *) inductive ex3_3 (A0,A1,A2:Type[0]) (P0,P1,P2:A0→A1→A2→Prop) : Prop ≝ | ex3_3_intro: ∀x0,x1,x2. P0 x0 x1 x2 → P1 x0 x1 x2 → P2 x0 x1 x2 → ex3_3 ? ? ? ? ? ? . -interpretation "multiple existental quantifier (3, 3)" 'Ex P0 P1 P2 = (ex3_3 ? ? ? P0 P1 P2). +interpretation "multiple inductive existental quantifier (3, 3)" 'Ex P0 P1 P2 = (ex3_3 ? ? ? P0 P1 P2). -(* multiple existental quantifier (3, 4) *) +(* multiple inductive existental quantifier (3, 4) *) inductive ex3_4 (A0,A1,A2,A3:Type[0]) (P0,P1,P2:A0→A1→A2→A3→Prop) : Prop ≝ | ex3_4_intro: ∀x0,x1,x2,x3. P0 x0 x1 x2 x3 → P1 x0 x1 x2 x3 → P2 x0 x1 x2 x3 → ex3_4 ? ? ? ? ? ? ? . -interpretation "multiple existental quantifier (3, 4)" 'Ex P0 P1 P2 = (ex3_4 ? ? ? ? P0 P1 P2). +interpretation "multiple inductive existental quantifier (3, 4)" 'Ex P0 P1 P2 = (ex3_4 ? ? ? ? P0 P1 P2). -(* multiple existental quantifier (4, 1) *) +(* multiple inductive existental quantifier (3, 5) *) + +inductive ex3_5 (A0,A1,A2,A3,A4:Type[0]) (P0,P1,P2:A0→A1→A2→A3→A4→Prop) : Prop ≝ + | ex3_5_intro: ∀x0,x1,x2,x3,x4. P0 x0 x1 x2 x3 x4 → P1 x0 x1 x2 x3 x4 → P2 x0 x1 x2 x3 x4 → ex3_5 ? ? ? ? ? ? ? ? +. + +interpretation "multiple inductive existental quantifier (3, 5)" 'Ex P0 P1 P2 = (ex3_5 ? ? ? ? ? P0 P1 P2). + +(* multiple inductive existental quantifier (4, 1) *) inductive ex4 (A0:Type[0]) (P0,P1,P2,P3:A0→Prop) : Prop ≝ | ex4_intro: ∀x0. P0 x0 → P1 x0 → P2 x0 → P3 x0 → ex4 ? ? ? ? ? . -interpretation "multiple existental quantifier (4, 1)" 'Ex P0 P1 P2 P3 = (ex4 ? P0 P1 P2 P3). +interpretation "multiple inductive existental quantifier (4, 1)" 'Ex P0 P1 P2 P3 = (ex4 ? P0 P1 P2 P3). -(* multiple existental quantifier (4, 2) *) +(* multiple inductive existental quantifier (4, 2) *) inductive ex4_2 (A0,A1:Type[0]) (P0,P1,P2,P3:A0→A1→Prop) : Prop ≝ | ex4_2_intro: ∀x0,x1. P0 x0 x1 → P1 x0 x1 → P2 x0 x1 → P3 x0 x1 → ex4_2 ? ? ? ? ? ? . -interpretation "multiple existental quantifier (4, 2)" 'Ex P0 P1 P2 P3 = (ex4_2 ? ? P0 P1 P2 P3). +interpretation "multiple inductive existental quantifier (4, 2)" 'Ex P0 P1 P2 P3 = (ex4_2 ? ? P0 P1 P2 P3). -(* multiple existental quantifier (4, 3) *) +(* multiple inductive existental quantifier (4, 3) *) inductive ex4_3 (A0,A1,A2:Type[0]) (P0,P1,P2,P3:A0→A1→A2→Prop) : Prop ≝ | ex4_3_intro: ∀x0,x1,x2. P0 x0 x1 x2 → P1 x0 x1 x2 → P2 x0 x1 x2 → P3 x0 x1 x2 → ex4_3 ? ? ? ? ? ? ? . -interpretation "multiple existental quantifier (4, 3)" 'Ex P0 P1 P2 P3 = (ex4_3 ? ? ? P0 P1 P2 P3). +interpretation "multiple inductive existental quantifier (4, 3)" 'Ex P0 P1 P2 P3 = (ex4_3 ? ? ? P0 P1 P2 P3). -(* multiple existental quantifier (4, 4) *) +(* multiple inductive existental quantifier (4, 4) *) inductive ex4_4 (A0,A1,A2,A3:Type[0]) (P0,P1,P2,P3:A0→A1→A2→A3→Prop) : Prop ≝ | ex4_4_intro: ∀x0,x1,x2,x3. P0 x0 x1 x2 x3 → P1 x0 x1 x2 x3 → P2 x0 x1 x2 x3 → P3 x0 x1 x2 x3 → ex4_4 ? ? ? ? ? ? ? ? . -interpretation "multiple existental quantifier (4, 4)" 'Ex P0 P1 P2 P3 = (ex4_4 ? ? ? ? P0 P1 P2 P3). +interpretation "multiple inductive existental quantifier (4, 4)" 'Ex P0 P1 P2 P3 = (ex4_4 ? ? ? ? P0 P1 P2 P3). -(* multiple existental quantifier (4, 5) *) +(* multiple inductive existental quantifier (4, 5) *) inductive ex4_5 (A0,A1,A2,A3,A4:Type[0]) (P0,P1,P2,P3:A0→A1→A2→A3→A4→Prop) : Prop ≝ | ex4_5_intro: ∀x0,x1,x2,x3,x4. P0 x0 x1 x2 x3 x4 → P1 x0 x1 x2 x3 x4 → P2 x0 x1 x2 x3 x4 → P3 x0 x1 x2 x3 x4 → ex4_5 ? ? ? ? ? ? ? ? ? . -interpretation "multiple existental quantifier (4, 5)" 'Ex P0 P1 P2 P3 = (ex4_5 ? ? ? ? ? P0 P1 P2 P3). +interpretation "multiple inductive existental quantifier (4, 5)" 'Ex P0 P1 P2 P3 = (ex4_5 ? ? ? ? ? P0 P1 P2 P3). -(* multiple existental quantifier (5, 2) *) +(* multiple inductive existental quantifier (5, 2) *) inductive ex5_2 (A0,A1:Type[0]) (P0,P1,P2,P3,P4:A0→A1→Prop) : Prop ≝ | ex5_2_intro: ∀x0,x1. P0 x0 x1 → P1 x0 x1 → P2 x0 x1 → P3 x0 x1 → P4 x0 x1 → ex5_2 ? ? ? ? ? ? ? . -interpretation "multiple existental quantifier (5, 2)" 'Ex P0 P1 P2 P3 P4 = (ex5_2 ? ? P0 P1 P2 P3 P4). +interpretation "multiple inductive existental quantifier (5, 2)" 'Ex P0 P1 P2 P3 P4 = (ex5_2 ? ? P0 P1 P2 P3 P4). -(* multiple existental quantifier (5, 3) *) +(* multiple inductive existental quantifier (5, 3) *) inductive ex5_3 (A0,A1,A2:Type[0]) (P0,P1,P2,P3,P4:A0→A1→A2→Prop) : Prop ≝ | ex5_3_intro: ∀x0,x1,x2. P0 x0 x1 x2 → P1 x0 x1 x2 → P2 x0 x1 x2 → P3 x0 x1 x2 → P4 x0 x1 x2 → ex5_3 ? ? ? ? ? ? ? ? . -interpretation "multiple existental quantifier (5, 3)" 'Ex P0 P1 P2 P3 P4 = (ex5_3 ? ? ? P0 P1 P2 P3 P4). +interpretation "multiple inductive existental quantifier (5, 3)" 'Ex P0 P1 P2 P3 P4 = (ex5_3 ? ? ? P0 P1 P2 P3 P4). -(* multiple existental quantifier (5, 4) *) +(* multiple inductive existental quantifier (5, 4) *) inductive ex5_4 (A0,A1,A2,A3:Type[0]) (P0,P1,P2,P3,P4:A0→A1→A2→A3→Prop) : Prop ≝ | ex5_4_intro: ∀x0,x1,x2,x3. P0 x0 x1 x2 x3 → P1 x0 x1 x2 x3 → P2 x0 x1 x2 x3 → P3 x0 x1 x2 x3 → P4 x0 x1 x2 x3 → ex5_4 ? ? ? ? ? ? ? ? ? . -interpretation "multiple existental quantifier (5, 4)" 'Ex P0 P1 P2 P3 P4 = (ex5_4 ? ? ? ? P0 P1 P2 P3 P4). +interpretation "multiple inductive existental quantifier (5, 4)" 'Ex P0 P1 P2 P3 P4 = (ex5_4 ? ? ? ? P0 P1 P2 P3 P4). -(* multiple existental quantifier (5, 5) *) +(* multiple inductive existental quantifier (5, 5) *) inductive ex5_5 (A0,A1,A2,A3,A4:Type[0]) (P0,P1,P2,P3,P4:A0→A1→A2→A3→A4→Prop) : Prop ≝ | ex5_5_intro: ∀x0,x1,x2,x3,x4. P0 x0 x1 x2 x3 x4 → P1 x0 x1 x2 x3 x4 → P2 x0 x1 x2 x3 x4 → P3 x0 x1 x2 x3 x4 → P4 x0 x1 x2 x3 x4 → ex5_5 ? ? ? ? ? ? ? ? ? ? . -interpretation "multiple existental quantifier (5, 5)" 'Ex P0 P1 P2 P3 P4 = (ex5_5 ? ? ? ? ? P0 P1 P2 P3 P4). +interpretation "multiple inductive existental quantifier (5, 5)" 'Ex P0 P1 P2 P3 P4 = (ex5_5 ? ? ? ? ? P0 P1 P2 P3 P4). -(* multiple existental quantifier (5, 6) *) +(* multiple inductive existental quantifier (5, 6) *) inductive ex5_6 (A0,A1,A2,A3,A4,A5:Type[0]) (P0,P1,P2,P3,P4:A0→A1→A2→A3→A4→A5→Prop) : Prop ≝ | ex5_6_intro: ∀x0,x1,x2,x3,x4,x5. P0 x0 x1 x2 x3 x4 x5 → P1 x0 x1 x2 x3 x4 x5 → P2 x0 x1 x2 x3 x4 x5 → P3 x0 x1 x2 x3 x4 x5 → P4 x0 x1 x2 x3 x4 x5 → ex5_6 ? ? ? ? ? ? ? ? ? ? ? . -interpretation "multiple existental quantifier (5, 6)" 'Ex P0 P1 P2 P3 P4 = (ex5_6 ? ? ? ? ? ? P0 P1 P2 P3 P4). +interpretation "multiple inductive existental quantifier (5, 6)" 'Ex P0 P1 P2 P3 P4 = (ex5_6 ? ? ? ? ? ? P0 P1 P2 P3 P4). -(* multiple existental quantifier (6, 3) *) +(* multiple inductive existental quantifier (6, 3) *) inductive ex6_3 (A0,A1,A2:Type[0]) (P0,P1,P2,P3,P4,P5:A0→A1→A2→Prop) : Prop ≝ | ex6_3_intro: ∀x0,x1,x2. P0 x0 x1 x2 → P1 x0 x1 x2 → P2 x0 x1 x2 → P3 x0 x1 x2 → P4 x0 x1 x2 → P5 x0 x1 x2 → ex6_3 ? ? ? ? ? ? ? ? ? . -interpretation "multiple existental quantifier (6, 3)" 'Ex P0 P1 P2 P3 P4 P5 = (ex6_3 ? ? ? P0 P1 P2 P3 P4 P5). +interpretation "multiple inductive existental quantifier (6, 3)" 'Ex P0 P1 P2 P3 P4 P5 = (ex6_3 ? ? ? P0 P1 P2 P3 P4 P5). -(* multiple existental quantifier (6, 4) *) +(* multiple inductive existental quantifier (6, 4) *) inductive ex6_4 (A0,A1,A2,A3:Type[0]) (P0,P1,P2,P3,P4,P5:A0→A1→A2→A3→Prop) : Prop ≝ | ex6_4_intro: ∀x0,x1,x2,x3. P0 x0 x1 x2 x3 → P1 x0 x1 x2 x3 → P2 x0 x1 x2 x3 → P3 x0 x1 x2 x3 → P4 x0 x1 x2 x3 → P5 x0 x1 x2 x3 → ex6_4 ? ? ? ? ? ? ? ? ? ? . -interpretation "multiple existental quantifier (6, 4)" 'Ex P0 P1 P2 P3 P4 P5 = (ex6_4 ? ? ? ? P0 P1 P2 P3 P4 P5). +interpretation "multiple inductive existental quantifier (6, 4)" 'Ex P0 P1 P2 P3 P4 P5 = (ex6_4 ? ? ? ? P0 P1 P2 P3 P4 P5). -(* multiple existental quantifier (6, 5) *) +(* multiple inductive existental quantifier (6, 5) *) inductive ex6_5 (A0,A1,A2,A3,A4:Type[0]) (P0,P1,P2,P3,P4,P5:A0→A1→A2→A3→A4→Prop) : Prop ≝ | ex6_5_intro: ∀x0,x1,x2,x3,x4. P0 x0 x1 x2 x3 x4 → P1 x0 x1 x2 x3 x4 → P2 x0 x1 x2 x3 x4 → P3 x0 x1 x2 x3 x4 → P4 x0 x1 x2 x3 x4 → P5 x0 x1 x2 x3 x4 → ex6_5 ? ? ? ? ? ? ? ? ? ? ? . -interpretation "multiple existental quantifier (6, 5)" 'Ex P0 P1 P2 P3 P4 P5 = (ex6_5 ? ? ? ? ? P0 P1 P2 P3 P4 P5). +interpretation "multiple inductive existental quantifier (6, 5)" 'Ex P0 P1 P2 P3 P4 P5 = (ex6_5 ? ? ? ? ? P0 P1 P2 P3 P4 P5). -(* multiple existental quantifier (6, 6) *) +(* multiple inductive existental quantifier (6, 6) *) inductive ex6_6 (A0,A1,A2,A3,A4,A5:Type[0]) (P0,P1,P2,P3,P4,P5:A0→A1→A2→A3→A4→A5→Prop) : Prop ≝ | ex6_6_intro: ∀x0,x1,x2,x3,x4,x5. P0 x0 x1 x2 x3 x4 x5 → P1 x0 x1 x2 x3 x4 x5 → P2 x0 x1 x2 x3 x4 x5 → P3 x0 x1 x2 x3 x4 x5 → P4 x0 x1 x2 x3 x4 x5 → P5 x0 x1 x2 x3 x4 x5 → ex6_6 ? ? ? ? ? ? ? ? ? ? ? ? . -interpretation "multiple existental quantifier (6, 6)" 'Ex P0 P1 P2 P3 P4 P5 = (ex6_6 ? ? ? ? ? ? P0 P1 P2 P3 P4 P5). +interpretation "multiple inductive existental quantifier (6, 6)" 'Ex P0 P1 P2 P3 P4 P5 = (ex6_6 ? ? ? ? ? ? P0 P1 P2 P3 P4 P5). -(* multiple existental quantifier (6, 7) *) +(* multiple inductive existental quantifier (6, 7) *) inductive ex6_7 (A0,A1,A2,A3,A4,A5,A6:Type[0]) (P0,P1,P2,P3,P4,P5:A0→A1→A2→A3→A4→A5→A6→Prop) : Prop ≝ | ex6_7_intro: ∀x0,x1,x2,x3,x4,x5,x6. P0 x0 x1 x2 x3 x4 x5 x6 → P1 x0 x1 x2 x3 x4 x5 x6 → P2 x0 x1 x2 x3 x4 x5 x6 → P3 x0 x1 x2 x3 x4 x5 x6 → P4 x0 x1 x2 x3 x4 x5 x6 → P5 x0 x1 x2 x3 x4 x5 x6 → ex6_7 ? ? ? ? ? ? ? ? ? ? ? ? ? . -interpretation "multiple existental quantifier (6, 7)" 'Ex P0 P1 P2 P3 P4 P5 = (ex6_7 ? ? ? ? ? ? ? P0 P1 P2 P3 P4 P5). +interpretation "multiple inductive existental quantifier (6, 7)" 'Ex P0 P1 P2 P3 P4 P5 = (ex6_7 ? ? ? ? ? ? ? P0 P1 P2 P3 P4 P5). -(* multiple existental quantifier (7, 3) *) +(* multiple inductive existental quantifier (7, 3) *) inductive ex7_3 (A0,A1,A2:Type[0]) (P0,P1,P2,P3,P4,P5,P6:A0→A1→A2→Prop) : Prop ≝ | ex7_3_intro: ∀x0,x1,x2. P0 x0 x1 x2 → P1 x0 x1 x2 → P2 x0 x1 x2 → P3 x0 x1 x2 → P4 x0 x1 x2 → P5 x0 x1 x2 → P6 x0 x1 x2 → ex7_3 ? ? ? ? ? ? ? ? ? ? . -interpretation "multiple existental quantifier (7, 3)" 'Ex P0 P1 P2 P3 P4 P5 P6 = (ex7_3 ? ? ? P0 P1 P2 P3 P4 P5 P6). +interpretation "multiple inductive existental quantifier (7, 3)" 'Ex P0 P1 P2 P3 P4 P5 P6 = (ex7_3 ? ? ? P0 P1 P2 P3 P4 P5 P6). -(* multiple existental quantifier (7, 4) *) +(* multiple inductive existental quantifier (7, 4) *) inductive ex7_4 (A0,A1,A2,A3:Type[0]) (P0,P1,P2,P3,P4,P5,P6:A0→A1→A2→A3→Prop) : Prop ≝ | ex7_4_intro: ∀x0,x1,x2,x3. P0 x0 x1 x2 x3 → P1 x0 x1 x2 x3 → P2 x0 x1 x2 x3 → P3 x0 x1 x2 x3 → P4 x0 x1 x2 x3 → P5 x0 x1 x2 x3 → P6 x0 x1 x2 x3 → ex7_4 ? ? ? ? ? ? ? ? ? ? ? . -interpretation "multiple existental quantifier (7, 4)" 'Ex P0 P1 P2 P3 P4 P5 P6 = (ex7_4 ? ? ? ? P0 P1 P2 P3 P4 P5 P6). +interpretation "multiple inductive existental quantifier (7, 4)" 'Ex P0 P1 P2 P3 P4 P5 P6 = (ex7_4 ? ? ? ? P0 P1 P2 P3 P4 P5 P6). -(* multiple existental quantifier (7, 7) *) +(* multiple inductive existental quantifier (7, 7) *) inductive ex7_7 (A0,A1,A2,A3,A4,A5,A6:Type[0]) (P0,P1,P2,P3,P4,P5,P6:A0→A1→A2→A3→A4→A5→A6→Prop) : Prop ≝ | ex7_7_intro: ∀x0,x1,x2,x3,x4,x5,x6. P0 x0 x1 x2 x3 x4 x5 x6 → P1 x0 x1 x2 x3 x4 x5 x6 → P2 x0 x1 x2 x3 x4 x5 x6 → P3 x0 x1 x2 x3 x4 x5 x6 → P4 x0 x1 x2 x3 x4 x5 x6 → P5 x0 x1 x2 x3 x4 x5 x6 → P6 x0 x1 x2 x3 x4 x5 x6 → ex7_7 ? ? ? ? ? ? ? ? ? ? ? ? ? ? . -interpretation "multiple existental quantifier (7, 7)" 'Ex P0 P1 P2 P3 P4 P5 P6 = (ex7_7 ? ? ? ? ? ? ? P0 P1 P2 P3 P4 P5 P6). +interpretation "multiple inductive existental quantifier (7, 7)" 'Ex P0 P1 P2 P3 P4 P5 P6 = (ex7_7 ? ? ? ? ? ? ? P0 P1 P2 P3 P4 P5 P6). -(* multiple existental quantifier (8, 4) *) +(* multiple inductive existental quantifier (8, 4) *) inductive ex8_4 (A0,A1,A2,A3:Type[0]) (P0,P1,P2,P3,P4,P5,P6,P7:A0→A1→A2→A3→Prop) : Prop ≝ | ex8_4_intro: ∀x0,x1,x2,x3. P0 x0 x1 x2 x3 → P1 x0 x1 x2 x3 → P2 x0 x1 x2 x3 → P3 x0 x1 x2 x3 → P4 x0 x1 x2 x3 → P5 x0 x1 x2 x3 → P6 x0 x1 x2 x3 → P7 x0 x1 x2 x3 → ex8_4 ? ? ? ? ? ? ? ? ? ? ? ? . -interpretation "multiple existental quantifier (8, 4)" 'Ex P0 P1 P2 P3 P4 P5 P6 P7 = (ex8_4 ? ? ? ? P0 P1 P2 P3 P4 P5 P6 P7). +interpretation "multiple inductive existental quantifier (8, 4)" 'Ex P0 P1 P2 P3 P4 P5 P6 P7 = (ex8_4 ? ? ? ? P0 P1 P2 P3 P4 P5 P6 P7). -(* multiple existental quantifier (8, 5) *) +(* multiple inductive existental quantifier (8, 5) *) inductive ex8_5 (A0,A1,A2,A3,A4:Type[0]) (P0,P1,P2,P3,P4,P5,P6,P7:A0→A1→A2→A3→A4→Prop) : Prop ≝ | ex8_5_intro: ∀x0,x1,x2,x3,x4. P0 x0 x1 x2 x3 x4 → P1 x0 x1 x2 x3 x4 → P2 x0 x1 x2 x3 x4 → P3 x0 x1 x2 x3 x4 → P4 x0 x1 x2 x3 x4 → P5 x0 x1 x2 x3 x4 → P6 x0 x1 x2 x3 x4 → P7 x0 x1 x2 x3 x4 → ex8_5 ? ? ? ? ? ? ? ? ? ? ? ? ? . -interpretation "multiple existental quantifier (8, 5)" 'Ex P0 P1 P2 P3 P4 P5 P6 P7 = (ex8_5 ? ? ? ? ? P0 P1 P2 P3 P4 P5 P6 P7). +interpretation "multiple inductive existental quantifier (8, 5)" 'Ex P0 P1 P2 P3 P4 P5 P6 P7 = (ex8_5 ? ? ? ? ? P0 P1 P2 P3 P4 P5 P6 P7). (* multiple disjunction connective (3) *)