From 5c186c72f508da0849058afeecc6877cd9ed6303 Mon Sep 17 00:00:00 2001 From: Ferruccio Guidi Date: Sat, 23 Jun 2018 20:03:00 +0200 Subject: [PATCH] renaming + the predicate in elimination principles in now Q uniformly --- .../basic_2/i_static/tc_lfxs_fqup.ma | 16 +++---- .../contribs/lambdadelta/basic_2/names.txt | 6 ++- .../basic_2/relocation/lexs_lexs.ma | 2 +- .../basic_2/rt_computation/cpms.ma | 4 +- .../basic_2/rt_computation/cprs.ma | 20 ++++----- .../basic_2/rt_computation/cpxs.ma | 16 +++---- .../lambdadelta/basic_2/rt_computation/csx.ma | 10 ++--- .../basic_2/rt_computation/csx_aaa.ma | 28 ++++++------ .../basic_2/rt_computation/csx_cpxs.ma | 16 +++---- .../basic_2/rt_computation/fpbs.ma | 12 ++--- .../lambdadelta/basic_2/rt_computation/fsb.ma | 10 ++--- .../basic_2/rt_computation/fsb_aaa.ma | 34 +++++++------- .../basic_2/rt_computation/fsb_csx.ma | 16 +++---- .../basic_2/rt_computation/fsb_fpbg.ma | 20 ++++----- .../basic_2/rt_computation/lprs.ma | 10 ++--- .../basic_2/rt_computation/lprs_lpr.ma | 12 ++--- .../basic_2/rt_computation/lpxs.ma | 10 ++--- .../basic_2/rt_computation/lpxs_lpx.ma | 12 ++--- .../basic_2/rt_computation/rdsx.ma | 10 ++--- .../basic_2/rt_computation/rdsx_lpxs.ma | 20 ++++----- .../basic_2/rt_equivalence/cpcs.ma | 12 ++--- .../lambdadelta/basic_2/rt_transition/cpm.ma | 44 +++++++++---------- .../lambdadelta/basic_2/rt_transition/cpr.ma | 36 +++++++-------- .../lambdadelta/basic_2/rt_transition/cpx.ma | 42 +++++++++--------- .../lambdadelta/basic_2/s_computation/fqup.ma | 20 ++++----- .../basic_2/s_computation/fqup_weight.ma | 20 ++++----- .../lambdadelta/basic_2/s_computation/fqus.ma | 14 +++--- .../basic_2/s_transition/fqu_weight.ma | 10 ++--- .../lambdadelta/basic_2/static/frees_fqup.ma | 22 +++++----- .../lambdadelta/basic_2/static/lfxs.ma | 2 +- .../lambdadelta/basic_2/static/lfxs_drops.ma | 6 +-- .../basic_2/syntax/append_length.ma | 6 +-- 32 files changed, 260 insertions(+), 258 deletions(-) diff --git a/matita/matita/contribs/lambdadelta/basic_2/i_static/tc_lfxs_fqup.ma b/matita/matita/contribs/lambdadelta/basic_2/i_static/tc_lfxs_fqup.ma index 8eaf23735..3392f1e1a 100644 --- a/matita/matita/contribs/lambdadelta/basic_2/i_static/tc_lfxs_fqup.ma +++ b/matita/matita/contribs/lambdadelta/basic_2/i_static/tc_lfxs_fqup.ma @@ -40,18 +40,18 @@ qed. (* Advanced eliminators *****************************************************) lemma tc_lfxs_ind_sn: ∀R. c_reflexive … R → - ∀L1,T. ∀R0:predicate …. R0 L1 → - (∀L,L2. L1 ⪤**[R, T] L → L ⪤*[R, T] L2 → R0 L → R0 L2) → - ∀L2. L1 ⪤**[R, T] L2 → R0 L2. -#R #HR #L1 #T #R0 #HL1 #IHL1 #L2 #HL12 + ∀L1,T. ∀Q:predicate …. Q L1 → + (∀L,L2. L1 ⪤**[R, T] L → L ⪤*[R, T] L2 → Q L → Q L2) → + ∀L2. L1 ⪤**[R, T] L2 → Q L2. +#R #HR #L1 #T #Q #HL1 #IHL1 #L2 #HL12 @(TC_star_ind … HL1 IHL1 … HL12) /2 width=1 by lfxs_refl/ qed-. lemma tc_lfxs_ind_dx: ∀R. c_reflexive … R → - ∀L2,T. ∀R0:predicate …. R0 L2 → - (∀L1,L. L1 ⪤*[R, T] L → L ⪤**[R, T] L2 → R0 L → R0 L1) → - ∀L1. L1 ⪤**[R, T] L2 → R0 L1. -#R #HR #L2 #R0 #HL2 #IHL2 #L1 #HL12 + ∀L2,T. ∀Q:predicate …. Q L2 → + (∀L1,L. L1 ⪤*[R, T] L → L ⪤**[R, T] L2 → Q L → Q L1) → + ∀L1. L1 ⪤**[R, T] L2 → Q L1. +#R #HR #L2 #Q #HL2 #IHL2 #L1 #HL12 @(TC_star_ind_dx … HL2 IHL2 … HL12) /2 width=4 by lfxs_refl/ qed-. diff --git a/matita/matita/contribs/lambdadelta/basic_2/names.txt b/matita/matita/contribs/lambdadelta/basic_2/names.txt index 1f1d889d7..d80ea011a 100644 --- a/matita/matita/contribs/lambdadelta/basic_2/names.txt +++ b/matita/matita/contribs/lambdadelta/basic_2/names.txt @@ -9,8 +9,10 @@ IH : reserved: inductive premise I,J : item K,L : local environment M,N : reserved: future use -O,P,Q : -R : generic predicate (relation) +O : +P : relocation environment +Q : elimination predicate +R : generic predicate/relation S : RTM stack T,U,V,W: term X,Y,Z : reserved: transient objet denoted by a capital letter 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 20e2f91a2..753b43b2e 100644 --- a/matita/matita/contribs/lambdadelta/basic_2/relocation/lexs_lexs.ma +++ b/matita/matita/contribs/lambdadelta/basic_2/relocation/lexs_lexs.ma @@ -51,7 +51,7 @@ theorem lexs_trans (RN) (RP) (f): (∀g,I,K. lexs_transitive RN RN RN RN RP g K /2 width=9 by lexs_trans_gen/ qed-. theorem lexs_trans_id_cfull: ∀R1,R2,R3,L1,L,f. L1 ⪤*[R1, cfull, f] L → 𝐈⦃f⦄ → - ∀L2. L ⪤*[R2, cfull, f] L2 → L1 ⪤*[R3, cfull, f] L2. + ∀L2. L ⪤*[R2, cfull, f] L2 → L1 ⪤*[R3, cfull, f] L2. #R1 #R2 #R3 #L1 #L #f #H elim H -L1 -L -f [ #f #Hf #L2 #H >(lexs_inv_atom1 … H) -L2 // ] #f #I1 #I #K1 #K #HK1 #_ #IH #Hf #L2 #H diff --git a/matita/matita/contribs/lambdadelta/basic_2/rt_computation/cpms.ma b/matita/matita/contribs/lambdadelta/basic_2/rt_computation/cpms.ma index 8d27710bd..2846c7536 100644 --- a/matita/matita/contribs/lambdadelta/basic_2/rt_computation/cpms.ma +++ b/matita/matita/contribs/lambdadelta/basic_2/rt_computation/cpms.ma @@ -37,14 +37,14 @@ lemma cpms_ind_sn (h) (G) (L) (T2) (Q:relation2 …): Q 0 T2 → (∀n1,n2,T1,T. ⦃G, L⦄ ⊢ T1 ➡[n1, h] T → ⦃G, L⦄ ⊢ T ➡*[n2, h] T2 → Q n2 T → Q (n1+n2) T1) → ∀n,T1. ⦃G, L⦄ ⊢ T1 ➡*[n, h] T2 → Q n T1. -#h #G #L #T2 #R @ltc_ind_sn_refl // +#h #G #L #T2 #Q @ltc_ind_sn_refl // qed-. lemma cpms_ind_dx (h) (G) (L) (T1) (Q:relation2 …): Q 0 T1 → (∀n1,n2,T,T2. ⦃G, L⦄ ⊢ T1 ➡*[n1, h] T → Q n1 T → ⦃G, L⦄ ⊢ T ➡[n2, h] T2 → Q (n1+n2) T2) → ∀n,T2. ⦃G, L⦄ ⊢ T1 ➡*[n, h] T2 → Q n T2. -#h #G #L #T1 #R @ltc_ind_dx_refl // +#h #G #L #T1 #Q @ltc_ind_dx_refl // qed-. (* Basic inversion lemmas ***************************************************) diff --git a/matita/matita/contribs/lambdadelta/basic_2/rt_computation/cprs.ma b/matita/matita/contribs/lambdadelta/basic_2/rt_computation/cprs.ma index 36d7644e6..230160ac7 100644 --- a/matita/matita/contribs/lambdadelta/basic_2/rt_computation/cprs.ma +++ b/matita/matita/contribs/lambdadelta/basic_2/rt_computation/cprs.ma @@ -20,11 +20,11 @@ include "basic_2/rt_computation/cpms.ma". (* Basic eliminators ********************************************************) (* Basic_2A1: was: cprs_ind_dx *) -lemma cprs_ind_sn (h) (G) (L) (T2) (R:predicate …): - R T2 → - (∀T1,T. ⦃G, L⦄ ⊢ T1 ➡[h] T → ⦃G, L⦄ ⊢ T ➡*[h] T2 → R T → R T1) → - ∀T1. ⦃G, L⦄ ⊢ T1 ➡*[h] T2 → R T1. -#h #G #L #T2 #R #IH1 #IH2 #T1 +lemma cprs_ind_sn (h) (G) (L) (T2) (Q:predicate …): + Q T2 → + (∀T1,T. ⦃G, L⦄ ⊢ T1 ➡[h] T → ⦃G, L⦄ ⊢ T ➡*[h] T2 → Q T → Q T1) → + ∀T1. ⦃G, L⦄ ⊢ T1 ➡*[h] T2 → Q T1. +#h #G #L #T2 #Q #IH1 #IH2 #T1 @(insert_eq_0 … 0) #n #H @(cpms_ind_sn … H) -n -T1 // #n1 #n2 #T1 #T #HT1 #HT2 #IH #H @@ -33,11 +33,11 @@ elim (plus_inv_O3 n1 n2) // -H #H1 #H2 destruct qed-. (* Basic_2A1: was: cprs_ind *) -lemma cprs_ind_dx (h) (G) (L) (T1) (R:predicate …): - R T1 → - (∀T,T2. ⦃G, L⦄ ⊢ T1 ➡*[h] T → ⦃G, L⦄ ⊢ T ➡[h] T2 → R T → R T2) → - ∀T2. ⦃G, L⦄ ⊢ T1 ➡*[h] T2 → R T2. -#h #G #L #T1 #R #IH1 #IH2 #T2 +lemma cprs_ind_dx (h) (G) (L) (T1) (Q:predicate …): + Q T1 → + (∀T,T2. ⦃G, L⦄ ⊢ T1 ➡*[h] T → ⦃G, L⦄ ⊢ T ➡[h] T2 → Q T → Q T2) → + ∀T2. ⦃G, L⦄ ⊢ T1 ➡*[h] T2 → Q T2. +#h #G #L #T1 #Q #IH1 #IH2 #T2 @(insert_eq_0 … 0) #n #H @(cpms_ind_dx … H) -n -T2 // #n1 #n2 #T #T2 #HT1 #IH #HT2 #H diff --git a/matita/matita/contribs/lambdadelta/basic_2/rt_computation/cpxs.ma b/matita/matita/contribs/lambdadelta/basic_2/rt_computation/cpxs.ma index 88924f4e0..5b7495bd4 100644 --- a/matita/matita/contribs/lambdadelta/basic_2/rt_computation/cpxs.ma +++ b/matita/matita/contribs/lambdadelta/basic_2/rt_computation/cpxs.ma @@ -26,17 +26,17 @@ interpretation "unbound context-sensitive parallel rt-computation (term)" (* Basic eliminators ********************************************************) -lemma cpxs_ind: ∀h,G,L,T1. ∀R:predicate term. R T1 → - (∀T,T2. ⦃G, L⦄ ⊢ T1 ⬈*[h] T → ⦃G, L⦄ ⊢ T ⬈[h] T2 → R T → R T2) → - ∀T2. ⦃G, L⦄ ⊢ T1 ⬈*[h] T2 → R T2. -#h #L #G #T1 #R #HT1 #IHT1 #T2 #HT12 +lemma cpxs_ind: ∀h,G,L,T1. ∀Q:predicate term. Q T1 → + (∀T,T2. ⦃G, L⦄ ⊢ T1 ⬈*[h] T → ⦃G, L⦄ ⊢ T ⬈[h] T2 → Q T → Q T2) → + ∀T2. ⦃G, L⦄ ⊢ T1 ⬈*[h] T2 → Q T2. +#h #L #G #T1 #Q #HT1 #IHT1 #T2 #HT12 @(TC_star_ind … HT1 IHT1 … HT12) // qed-. -lemma cpxs_ind_dx: ∀h,G,L,T2. ∀R:predicate term. R T2 → - (∀T1,T. ⦃G, L⦄ ⊢ T1 ⬈[h] T → ⦃G, L⦄ ⊢ T ⬈*[h] T2 → R T → R T1) → - ∀T1. ⦃G, L⦄ ⊢ T1 ⬈*[h] T2 → R T1. -#h #G #L #T2 #R #HT2 #IHT2 #T1 #HT12 +lemma cpxs_ind_dx: ∀h,G,L,T2. ∀Q:predicate term. Q T2 → + (∀T1,T. ⦃G, L⦄ ⊢ T1 ⬈[h] T → ⦃G, L⦄ ⊢ T ⬈*[h] T2 → Q T → Q T1) → + ∀T1. ⦃G, L⦄ ⊢ T1 ⬈*[h] T2 → Q T1. +#h #G #L #T2 #Q #HT2 #IHT2 #T1 #HT12 @(TC_star_ind_dx … HT2 IHT2 … HT12) // qed-. diff --git a/matita/matita/contribs/lambdadelta/basic_2/rt_computation/csx.ma b/matita/matita/contribs/lambdadelta/basic_2/rt_computation/csx.ma index 5e255d297..da0bbe1ee 100644 --- a/matita/matita/contribs/lambdadelta/basic_2/rt_computation/csx.ma +++ b/matita/matita/contribs/lambdadelta/basic_2/rt_computation/csx.ma @@ -27,13 +27,13 @@ interpretation (* Basic eliminators ********************************************************) -lemma csx_ind: ∀h,o,G,L. ∀R:predicate term. +lemma csx_ind: ∀h,o,G,L. ∀Q:predicate term. (∀T1. ⦃G, L⦄ ⊢ ⬈*[h, o] 𝐒⦃T1⦄ → - (∀T2. ⦃G, L⦄ ⊢ T1 ⬈[h] T2 → (T1 ≛[h, o] T2 → ⊥) → R T2) → - R T1 + (∀T2. ⦃G, L⦄ ⊢ T1 ⬈[h] T2 → (T1 ≛[h, o] T2 → ⊥) → Q T2) → + Q T1 ) → - ∀T. ⦃G, L⦄ ⊢ ⬈*[h, o] 𝐒⦃T⦄ → R T. -#h #o #G #L #R #H0 #T1 #H elim H -T1 + ∀T. ⦃G, L⦄ ⊢ ⬈*[h, o] 𝐒⦃T⦄ → Q T. +#h #o #G #L #Q #H0 #T1 #H elim H -T1 /5 width=1 by SN_intro/ qed-. diff --git a/matita/matita/contribs/lambdadelta/basic_2/rt_computation/csx_aaa.ma b/matita/matita/contribs/lambdadelta/basic_2/rt_computation/csx_aaa.ma index 722e8d8b6..4d54a74a5 100644 --- a/matita/matita/contribs/lambdadelta/basic_2/rt_computation/csx_aaa.ma +++ b/matita/matita/contribs/lambdadelta/basic_2/rt_computation/csx_aaa.ma @@ -28,33 +28,33 @@ qed. (* Advanced eliminators *****************************************************) -fact aaa_ind_csx_aux: ∀h,o,G,L,A. ∀R:predicate term. +fact aaa_ind_csx_aux: ∀h,o,G,L,A. ∀Q:predicate term. (∀T1. ⦃G, L⦄ ⊢ T1 ⁝ A → - (∀T2. ⦃G, L⦄ ⊢ T1 ⬈[h] T2 → (T1 ≛[h, o] T2 → ⊥) → R T2) → R T1 + (∀T2. ⦃G, L⦄ ⊢ T1 ⬈[h] T2 → (T1 ≛[h, o] T2 → ⊥) → Q T2) → Q T1 ) → - ∀T. ⦃G, L⦄ ⊢ ⬈*[h, o] 𝐒⦃T⦄ → ⦃G, L⦄ ⊢ T ⁝ A → R T. -#h #o #G #L #A #R #IH #T #H @(csx_ind … H) -T /4 width=5 by cpx_aaa_conf/ + ∀T. ⦃G, L⦄ ⊢ ⬈*[h, o] 𝐒⦃T⦄ → ⦃G, L⦄ ⊢ T ⁝ A → Q T. +#h #o #G #L #A #Q #IH #T #H @(csx_ind … H) -T /4 width=5 by cpx_aaa_conf/ qed-. -lemma aaa_ind_csx: ∀h,o,G,L,A. ∀R:predicate term. +lemma aaa_ind_csx: ∀h,o,G,L,A. ∀Q:predicate term. (∀T1. ⦃G, L⦄ ⊢ T1 ⁝ A → - (∀T2. ⦃G, L⦄ ⊢ T1 ⬈[h] T2 → (T1 ≛[h, o] T2 → ⊥) → R T2) → R T1 + (∀T2. ⦃G, L⦄ ⊢ T1 ⬈[h] T2 → (T1 ≛[h, o] T2 → ⊥) → Q T2) → Q T1 ) → - ∀T. ⦃G, L⦄ ⊢ T ⁝ A → R T. + ∀T. ⦃G, L⦄ ⊢ T ⁝ A → Q T. /5 width=9 by aaa_ind_csx_aux, aaa_csx/ qed-. -fact aaa_ind_csx_cpxs_aux: ∀h,o,G,L,A. ∀R:predicate term. +fact aaa_ind_csx_cpxs_aux: ∀h,o,G,L,A. ∀Q:predicate term. (∀T1. ⦃G, L⦄ ⊢ T1 ⁝ A → - (∀T2. ⦃G, L⦄ ⊢ T1 ⬈*[h] T2 → (T1 ≛[h, o] T2 → ⊥) → R T2) → R T1 + (∀T2. ⦃G, L⦄ ⊢ T1 ⬈*[h] T2 → (T1 ≛[h, o] T2 → ⊥) → Q T2) → Q T1 ) → - ∀T. ⦃G, L⦄ ⊢ ⬈*[h, o] 𝐒⦃T⦄ → ⦃G, L⦄ ⊢ T ⁝ A → R T. -#h #o #G #L #A #R #IH #T #H @(csx_ind_cpxs … H) -T /4 width=5 by cpxs_aaa_conf/ + ∀T. ⦃G, L⦄ ⊢ ⬈*[h, o] 𝐒⦃T⦄ → ⦃G, L⦄ ⊢ T ⁝ A → Q T. +#h #o #G #L #A #Q #IH #T #H @(csx_ind_cpxs … H) -T /4 width=5 by cpxs_aaa_conf/ qed-. (* Basic_2A1: was: aaa_ind_csx_alt *) -lemma aaa_ind_csx_cpxs: ∀h,o,G,L,A. ∀R:predicate term. +lemma aaa_ind_csx_cpxs: ∀h,o,G,L,A. ∀Q:predicate term. (∀T1. ⦃G, L⦄ ⊢ T1 ⁝ A → - (∀T2. ⦃G, L⦄ ⊢ T1 ⬈*[h] T2 → (T1 ≛[h, o] T2 → ⊥) → R T2) → R T1 + (∀T2. ⦃G, L⦄ ⊢ T1 ⬈*[h] T2 → (T1 ≛[h, o] T2 → ⊥) → Q T2) → Q T1 ) → - ∀T. ⦃G, L⦄ ⊢ T ⁝ A → R T. + ∀T. ⦃G, L⦄ ⊢ T ⁝ A → Q T. /5 width=9 by aaa_ind_csx_cpxs_aux, aaa_csx/ qed-. diff --git a/matita/matita/contribs/lambdadelta/basic_2/rt_computation/csx_cpxs.ma b/matita/matita/contribs/lambdadelta/basic_2/rt_computation/csx_cpxs.ma index cfc4d6314..3a8a70ef9 100644 --- a/matita/matita/contribs/lambdadelta/basic_2/rt_computation/csx_cpxs.ma +++ b/matita/matita/contribs/lambdadelta/basic_2/rt_computation/csx_cpxs.ma @@ -35,13 +35,13 @@ qed-. (* Eliminators with unbound context-sensitive rt-computation for terms ******) -lemma csx_ind_cpxs_tdeq: ∀h,o,G,L. ∀R:predicate term. +lemma csx_ind_cpxs_tdeq: ∀h,o,G,L. ∀Q:predicate term. (∀T1. ⦃G, L⦄ ⊢ ⬈*[h, o] 𝐒⦃T1⦄ → - (∀T2. ⦃G, L⦄ ⊢ T1 ⬈*[h] T2 → (T1 ≛[h, o] T2 → ⊥) → R T2) → R T1 + (∀T2. ⦃G, L⦄ ⊢ T1 ⬈*[h] T2 → (T1 ≛[h, o] T2 → ⊥) → Q T2) → Q T1 ) → ∀T1. ⦃G, L⦄ ⊢ ⬈*[h, o] 𝐒⦃T1⦄ → - ∀T0. ⦃G, L⦄ ⊢ T1 ⬈*[h] T0 → ∀T2. T0 ≛[h, o] T2 → R T2. -#h #o #G #L #R #IH #T1 #H @(csx_ind … H) -T1 + ∀T0. ⦃G, L⦄ ⊢ T1 ⬈*[h] T0 → ∀T2. T0 ≛[h, o] T2 → Q T2. +#h #o #G #L #Q #IH #T1 #H @(csx_ind … H) -T1 #T1 #HT1 #IH1 #T0 #HT10 #T2 #HT02 @IH -IH /3 width=3 by csx_cpxs_trans, csx_tdeq_trans/ -HT1 #V2 #HTV2 #HnTV2 lapply (tdeq_tdneq_trans … HT02 … HnTV2) -HnTV2 #H @@ -59,11 +59,11 @@ elim (tdeq_dec h o T1 T0) #H qed-. (* Basic_2A1: was: csx_ind_alt *) -lemma csx_ind_cpxs: ∀h,o,G,L. ∀R:predicate term. +lemma csx_ind_cpxs: ∀h,o,G,L. ∀Q:predicate term. (∀T1. ⦃G, L⦄ ⊢ ⬈*[h, o] 𝐒⦃T1⦄ → - (∀T2. ⦃G, L⦄ ⊢ T1 ⬈*[h] T2 → (T1 ≛[h, o] T2 → ⊥) → R T2) → R T1 + (∀T2. ⦃G, L⦄ ⊢ T1 ⬈*[h] T2 → (T1 ≛[h, o] T2 → ⊥) → Q T2) → Q T1 ) → - ∀T. ⦃G, L⦄ ⊢ ⬈*[h, o] 𝐒⦃T⦄ → R T. -#h #o #G #L #R #IH #T #HT + ∀T. ⦃G, L⦄ ⊢ ⬈*[h, o] 𝐒⦃T⦄ → Q T. +#h #o #G #L #Q #IH #T #HT @(csx_ind_cpxs_tdeq … IH … HT) -IH -HT // (**) (* full auto fails *) qed-. diff --git a/matita/matita/contribs/lambdadelta/basic_2/rt_computation/fpbs.ma b/matita/matita/contribs/lambdadelta/basic_2/rt_computation/fpbs.ma index 78c6b2ef7..af6ca54c9 100644 --- a/matita/matita/contribs/lambdadelta/basic_2/rt_computation/fpbs.ma +++ b/matita/matita/contribs/lambdadelta/basic_2/rt_computation/fpbs.ma @@ -26,14 +26,14 @@ interpretation "parallel rst-computation (closure)" (* Basic eliminators ********************************************************) -lemma fpbs_ind: ∀h,o,G1,L1,T1. ∀R:relation3 genv lenv term. R G1 L1 T1 → - (∀G,G2,L,L2,T,T2. ⦃G1, L1, T1⦄ ≥[h, o] ⦃G, L, T⦄ → ⦃G, L, T⦄ ≽[h, o] ⦃G2, L2, T2⦄ → R G L T → R G2 L2 T2) → - ∀G2,L2,T2. ⦃G1, L1, T1⦄ ≥[h, o] ⦃G2, L2, T2⦄ → R G2 L2 T2. +lemma fpbs_ind: ∀h,o,G1,L1,T1. ∀Q:relation3 genv lenv term. Q G1 L1 T1 → + (∀G,G2,L,L2,T,T2. ⦃G1, L1, T1⦄ ≥[h, o] ⦃G, L, T⦄ → ⦃G, L, T⦄ ≽[h, o] ⦃G2, L2, T2⦄ → Q G L T → Q G2 L2 T2) → + ∀G2,L2,T2. ⦃G1, L1, T1⦄ ≥[h, o] ⦃G2, L2, T2⦄ → Q G2 L2 T2. /3 width=8 by tri_TC_star_ind/ qed-. -lemma fpbs_ind_dx: ∀h,o,G2,L2,T2. ∀R:relation3 genv lenv term. R G2 L2 T2 → - (∀G1,G,L1,L,T1,T. ⦃G1, L1, T1⦄ ≽[h, o] ⦃G, L, T⦄ → ⦃G, L, T⦄ ≥[h, o] ⦃G2, L2, T2⦄ → R G L T → R G1 L1 T1) → - ∀G1,L1,T1. ⦃G1, L1, T1⦄ ≥[h, o] ⦃G2, L2, T2⦄ → R G1 L1 T1. +lemma fpbs_ind_dx: ∀h,o,G2,L2,T2. ∀Q:relation3 genv lenv term. Q G2 L2 T2 → + (∀G1,G,L1,L,T1,T. ⦃G1, L1, T1⦄ ≽[h, o] ⦃G, L, T⦄ → ⦃G, L, T⦄ ≥[h, o] ⦃G2, L2, T2⦄ → Q G L T → Q G1 L1 T1) → + ∀G1,L1,T1. ⦃G1, L1, T1⦄ ≥[h, o] ⦃G2, L2, T2⦄ → Q G1 L1 T1. /3 width=8 by tri_TC_star_ind_dx/ qed-. (* Basic properties *********************************************************) diff --git a/matita/matita/contribs/lambdadelta/basic_2/rt_computation/fsb.ma b/matita/matita/contribs/lambdadelta/basic_2/rt_computation/fsb.ma index 62fd4fe10..8ae6b26e8 100644 --- a/matita/matita/contribs/lambdadelta/basic_2/rt_computation/fsb.ma +++ b/matita/matita/contribs/lambdadelta/basic_2/rt_computation/fsb.ma @@ -31,13 +31,13 @@ interpretation (* Note: eliminator with shorter ground hypothesis *) (* Note: to be named fsb_ind when fsb becomes a definition like csx, lfsx ***) -lemma fsb_ind_alt: ∀h,o. ∀R: relation3 …. ( +lemma fsb_ind_alt: ∀h,o. ∀Q: relation3 …. ( ∀G1,L1,T1. ≥[h,o] 𝐒⦃G1, L1, T1⦄ → ( - ∀G2,L2,T2. ⦃G1, L1, T1⦄ ≻[h, o] ⦃G2, L2, T2⦄ → R G2 L2 T2 - ) → R G1 L1 T1 + ∀G2,L2,T2. ⦃G1, L1, T1⦄ ≻[h, o] ⦃G2, L2, T2⦄ → Q G2 L2 T2 + ) → Q G1 L1 T1 ) → - ∀G,L,T. ≥[h, o] 𝐒⦃G, L, T⦄ → R G L T. -#h #o #R #IH #G #L #T #H elim H -G -L -T + ∀G,L,T. ≥[h, o] 𝐒⦃G, L, T⦄ → Q G L T. +#h #o #Q #IH #G #L #T #H elim H -G -L -T /4 width=1 by fsb_intro/ qed-. diff --git a/matita/matita/contribs/lambdadelta/basic_2/rt_computation/fsb_aaa.ma b/matita/matita/contribs/lambdadelta/basic_2/rt_computation/fsb_aaa.ma index 5b27cd1a9..43eb814dc 100644 --- a/matita/matita/contribs/lambdadelta/basic_2/rt_computation/fsb_aaa.ma +++ b/matita/matita/contribs/lambdadelta/basic_2/rt_computation/fsb_aaa.ma @@ -27,42 +27,42 @@ theorem aaa_fsb: ∀h,o,G,L,T,A. ⦃G, L⦄ ⊢ T ⁝ A → ≥[h, o] 𝐒⦃G, (* Advanced eliminators with atomic arity assignment for terms **************) -fact aaa_ind_fpb_aux: ∀h,o. ∀R:relation3 …. +fact aaa_ind_fpb_aux: ∀h,o. ∀Q:relation3 …. (∀G1,L1,T1,A. ⦃G1, L1⦄ ⊢ T1 ⁝ A → - (∀G2,L2,T2. ⦃G1, L1, T1⦄ ≻[h, o] ⦃G2, L2, T2⦄ → R G2 L2 T2) → - R G1 L1 T1 + (∀G2,L2,T2. ⦃G1, L1, T1⦄ ≻[h, o] ⦃G2, L2, T2⦄ → Q G2 L2 T2) → + Q G1 L1 T1 ) → - ∀G,L,T. ⦃G, L⦄ ⊢ ⬈*[h, o] 𝐒⦃T⦄ → ∀A. ⦃G, L⦄ ⊢ T ⁝ A → R G L T. + ∀G,L,T. ⦃G, L⦄ ⊢ ⬈*[h, o] 𝐒⦃T⦄ → ∀A. ⦃G, L⦄ ⊢ T ⁝ A → Q G L T. #h #o #R #IH #G #L #T #H @(csx_ind_fpb … H) -G -L -T #G1 #L1 #T1 #H1 #IH1 #A1 #HTA1 @IH -IH // #G2 #L2 #T2 #H12 elim (fpbs_aaa_conf h o … G2 … L2 … T2 … HTA1) -A1 /2 width=2 by fpb_fpbs/ qed-. -lemma aaa_ind_fpb: ∀h,o. ∀R:relation3 …. +lemma aaa_ind_fpb: ∀h,o. ∀Q:relation3 …. (∀G1,L1,T1,A. ⦃G1, L1⦄ ⊢ T1 ⁝ A → - (∀G2,L2,T2. ⦃G1, L1, T1⦄ ≻[h, o] ⦃G2, L2, T2⦄ → R G2 L2 T2) → - R G1 L1 T1 + (∀G2,L2,T2. ⦃G1, L1, T1⦄ ≻[h, o] ⦃G2, L2, T2⦄ → Q G2 L2 T2) → + Q G1 L1 T1 ) → - ∀G,L,T,A. ⦃G, L⦄ ⊢ T ⁝ A → R G L T. + ∀G,L,T,A. ⦃G, L⦄ ⊢ T ⁝ A → Q G L T. /4 width=4 by aaa_ind_fpb_aux, aaa_csx/ qed-. -fact aaa_ind_fpbg_aux: ∀h,o. ∀R:relation3 …. +fact aaa_ind_fpbg_aux: ∀h,o. ∀Q:relation3 …. (∀G1,L1,T1,A. ⦃G1, L1⦄ ⊢ T1 ⁝ A → - (∀G2,L2,T2. ⦃G1, L1, T1⦄ >[h, o] ⦃G2, L2, T2⦄ → R G2 L2 T2) → - R G1 L1 T1 + (∀G2,L2,T2. ⦃G1, L1, T1⦄ >[h, o] ⦃G2, L2, T2⦄ → Q G2 L2 T2) → + Q G1 L1 T1 ) → - ∀G,L,T. ⦃G, L⦄ ⊢ ⬈*[h, o] 𝐒⦃T⦄ → ∀A. ⦃G, L⦄ ⊢ T ⁝ A → R G L T. -#h #o #R #IH #G #L #T #H @(csx_ind_fpbg … H) -G -L -T + ∀G,L,T. ⦃G, L⦄ ⊢ ⬈*[h, o] 𝐒⦃T⦄ → ∀A. ⦃G, L⦄ ⊢ T ⁝ A → Q G L T. +#h #o #Q #IH #G #L #T #H @(csx_ind_fpbg … H) -G -L -T #G1 #L1 #T1 #H1 #IH1 #A1 #HTA1 @IH -IH // #G2 #L2 #T2 #H12 elim (fpbs_aaa_conf h o … G2 … L2 … T2 … HTA1) -A1 /2 width=2 by fpbg_fwd_fpbs/ qed-. -lemma aaa_ind_fpbg: ∀h,o. ∀R:relation3 …. +lemma aaa_ind_fpbg: ∀h,o. ∀Q:relation3 …. (∀G1,L1,T1,A. ⦃G1, L1⦄ ⊢ T1 ⁝ A → - (∀G2,L2,T2. ⦃G1, L1, T1⦄ >[h, o] ⦃G2, L2, T2⦄ → R G2 L2 T2) → - R G1 L1 T1 + (∀G2,L2,T2. ⦃G1, L1, T1⦄ >[h, o] ⦃G2, L2, T2⦄ → Q G2 L2 T2) → + Q G1 L1 T1 ) → - ∀G,L,T,A. ⦃G, L⦄ ⊢ T ⁝ A → R G L T. + ∀G,L,T,A. ⦃G, L⦄ ⊢ T ⁝ A → Q G L T. /4 width=4 by aaa_ind_fpbg_aux, aaa_csx/ qed-. diff --git a/matita/matita/contribs/lambdadelta/basic_2/rt_computation/fsb_csx.ma b/matita/matita/contribs/lambdadelta/basic_2/rt_computation/fsb_csx.ma index d1cc73d89..ffcbc3d80 100644 --- a/matita/matita/contribs/lambdadelta/basic_2/rt_computation/fsb_csx.ma +++ b/matita/matita/contribs/lambdadelta/basic_2/rt_computation/fsb_csx.ma @@ -61,18 +61,18 @@ lemma csx_fsb: ∀h,o,G,L,T. ⦃G, L⦄ ⊢ ⬈*[h, o] 𝐒⦃T⦄ → ≥[h, o] (* Advanced eliminators *****************************************************) -lemma csx_ind_fpb: ∀h,o. ∀R:relation3 genv lenv term. +lemma csx_ind_fpb: ∀h,o. ∀Q:relation3 genv lenv term. (∀G1,L1,T1. ⦃G1, L1⦄ ⊢ ⬈*[h, o] 𝐒⦃T1⦄ → - (∀G2,L2,T2. ⦃G1, L1, T1⦄ ≻[h, o] ⦃G2, L2, T2⦄ → R G2 L2 T2) → - R G1 L1 T1 + (∀G2,L2,T2. ⦃G1, L1, T1⦄ ≻[h, o] ⦃G2, L2, T2⦄ → Q G2 L2 T2) → + Q G1 L1 T1 ) → - ∀G,L,T. ⦃G, L⦄ ⊢ ⬈*[h, o] 𝐒⦃T⦄ → R G L T. + ∀G,L,T. ⦃G, L⦄ ⊢ ⬈*[h, o] 𝐒⦃T⦄ → Q G L T. /4 width=4 by fsb_inv_csx, csx_fsb, fsb_ind_alt/ qed-. -lemma csx_ind_fpbg: ∀h,o. ∀R:relation3 genv lenv term. +lemma csx_ind_fpbg: ∀h,o. ∀Q:relation3 genv lenv term. (∀G1,L1,T1. ⦃G1, L1⦄ ⊢ ⬈*[h, o] 𝐒⦃T1⦄ → - (∀G2,L2,T2. ⦃G1, L1, T1⦄ >[h, o] ⦃G2, L2, T2⦄ → R G2 L2 T2) → - R G1 L1 T1 + (∀G2,L2,T2. ⦃G1, L1, T1⦄ >[h, o] ⦃G2, L2, T2⦄ → Q G2 L2 T2) → + Q G1 L1 T1 ) → - ∀G,L,T. ⦃G, L⦄ ⊢ ⬈*[h, o] 𝐒⦃T⦄ → R G L T. + ∀G,L,T. ⦃G, L⦄ ⊢ ⬈*[h, o] 𝐒⦃T⦄ → Q G L T. /4 width=4 by fsb_inv_csx, csx_fsb, fsb_ind_fpbg/ qed-. diff --git a/matita/matita/contribs/lambdadelta/basic_2/rt_computation/fsb_fpbg.ma b/matita/matita/contribs/lambdadelta/basic_2/rt_computation/fsb_fpbg.ma index 4dbe33e07..b2093e068 100644 --- a/matita/matita/contribs/lambdadelta/basic_2/rt_computation/fsb_fpbg.ma +++ b/matita/matita/contribs/lambdadelta/basic_2/rt_computation/fsb_fpbg.ma @@ -38,14 +38,14 @@ lemma fsb_intro_fpbg: ∀h,o,G1,L1,T1. ( (* Eliminators with proper parallel rst-computation for closures ************) -lemma fsb_ind_fpbg_fpbs: ∀h,o. ∀R:relation3 genv lenv term. +lemma fsb_ind_fpbg_fpbs: ∀h,o. ∀Q:relation3 genv lenv term. (∀G1,L1,T1. ≥[h, o] 𝐒⦃G1, L1, T1⦄ → - (∀G2,L2,T2. ⦃G1, L1, T1⦄ >[h, o] ⦃G2, L2, T2⦄ → R G2 L2 T2) → - R G1 L1 T1 + (∀G2,L2,T2. ⦃G1, L1, T1⦄ >[h, o] ⦃G2, L2, T2⦄ → Q G2 L2 T2) → + Q G1 L1 T1 ) → ∀G1,L1,T1. ≥[h, o] 𝐒⦃G1, L1, T1⦄ → - ∀G2,L2,T2. ⦃G1, L1, T1⦄ ≥[h, o] ⦃G2, L2, T2⦄ → R G2 L2 T2. -#h #o #R #IH1 #G1 #L1 #T1 #H @(fsb_ind_alt … H) -G1 -L1 -T1 + ∀G2,L2,T2. ⦃G1, L1, T1⦄ ≥[h, o] ⦃G2, L2, T2⦄ → Q G2 L2 T2. +#h #o #Q #IH1 #G1 #L1 #T1 #H @(fsb_ind_alt … H) -G1 -L1 -T1 #G1 #L1 #T1 #H1 #IH #G2 #L2 #T2 #H12 @IH1 -IH1 [ -IH /2 width=5 by fsb_fpbs_trans/ @@ -55,12 +55,12 @@ lemma fsb_ind_fpbg_fpbs: ∀h,o. ∀R:relation3 genv lenv term. ] qed-. -lemma fsb_ind_fpbg: ∀h,o. ∀R:relation3 genv lenv term. +lemma fsb_ind_fpbg: ∀h,o. ∀Q:relation3 genv lenv term. (∀G1,L1,T1. ≥[h, o] 𝐒⦃G1, L1, T1⦄ → - (∀G2,L2,T2. ⦃G1, L1, T1⦄ >[h, o] ⦃G2, L2, T2⦄ → R G2 L2 T2) → - R G1 L1 T1 + (∀G2,L2,T2. ⦃G1, L1, T1⦄ >[h, o] ⦃G2, L2, T2⦄ → Q G2 L2 T2) → + Q G1 L1 T1 ) → - ∀G1,L1,T1. ≥[h, o] 𝐒⦃G1, L1, T1⦄ → R G1 L1 T1. -#h #o #R #IH #G1 #L1 #T1 #H @(fsb_ind_fpbg_fpbs … H) -H + ∀G1,L1,T1. ≥[h, o] 𝐒⦃G1, L1, T1⦄ → Q G1 L1 T1. +#h #o #Q #IH #G1 #L1 #T1 #H @(fsb_ind_fpbg_fpbs … H) -H /3 width=1 by/ qed-. diff --git a/matita/matita/contribs/lambdadelta/basic_2/rt_computation/lprs.ma b/matita/matita/contribs/lambdadelta/basic_2/rt_computation/lprs.ma index 827a963be..1ee9f365b 100644 --- a/matita/matita/contribs/lambdadelta/basic_2/rt_computation/lprs.ma +++ b/matita/matita/contribs/lambdadelta/basic_2/rt_computation/lprs.ma @@ -65,15 +65,15 @@ lemma lprs_inv_pair_dx (h) (G): (* Basic eliminators ********************************************************) (* Basic_2A1: was: lprs_ind_alt *) -lemma lprs_ind (h) (G): ∀R:relation lenv. - R (⋆) (⋆) → ( +lemma lprs_ind (h) (G): ∀Q:relation lenv. + Q (⋆) (⋆) → ( ∀I,K1,K2. ⦃G, K1⦄ ⊢ ➡*[h] K2 → - R K1 K2 → R (K1.ⓘ{I}) (K2.ⓘ{I}) + Q K1 K2 → Q (K1.ⓘ{I}) (K2.ⓘ{I}) ) → ( ∀I,K1,K2,V1,V2. ⦃G, K1⦄ ⊢ ➡*[h] K2 → ⦃G, K1⦄ ⊢ V1 ➡*[h] V2 → - R K1 K2 → R (K1.ⓑ{I}V1) (K2.ⓑ{I}V2) + Q K1 K2 → Q (K1.ⓑ{I}V1) (K2.ⓑ{I}V2) ) → - ∀L1,L2. ⦃G, L1⦄ ⊢ ➡*[h] L2 → R L1 L2. + ∀L1,L2. ⦃G, L1⦄ ⊢ ➡*[h] L2 → Q L1 L2. /3 width=4 by lex_ind/ qed-. diff --git a/matita/matita/contribs/lambdadelta/basic_2/rt_computation/lprs_lpr.ma b/matita/matita/contribs/lambdadelta/basic_2/rt_computation/lprs_lpr.ma index e442a66b2..120177208 100644 --- a/matita/matita/contribs/lambdadelta/basic_2/rt_computation/lprs_lpr.ma +++ b/matita/matita/contribs/lambdadelta/basic_2/rt_computation/lprs_lpr.ma @@ -19,15 +19,15 @@ include "basic_2/rt_computation/lprs_tc.ma". (* Eliminators with r-transition for full local environments ****************) (* Basic_2A1: was: lprs_ind_dx *) -lemma lprs_ind_sn (h) (G) (L2): ∀R:predicate lenv. R L2 → - (∀L1,L. ⦃G, L1⦄ ⊢ ➡[h] L → ⦃G, L⦄ ⊢ ➡*[h] L2 → R L → R L1) → - ∀L1. ⦃G, L1⦄ ⊢ ➡*[h] L2 → R L1. +lemma lprs_ind_sn (h) (G) (L2): ∀Q:predicate lenv. Q L2 → + (∀L1,L. ⦃G, L1⦄ ⊢ ➡[h] L → ⦃G, L⦄ ⊢ ➡*[h] L2 → Q L → Q L1) → + ∀L1. ⦃G, L1⦄ ⊢ ➡*[h] L2 → Q L1. /4 width=8 by lprs_inv_CTC, lprs_CTC, lpr_cprs_trans, cpr_refl, lex_CTC_ind_sn/ qed-. (* Basic_2A1: was: lprs_ind *) -lemma lprs_ind_dx (h) (G) (L1): ∀R:predicate lenv. R L1 → - (∀L,L2. ⦃G, L1⦄ ⊢ ➡*[h] L → ⦃G, L⦄ ⊢ ➡[h] L2 → R L → R L2) → - ∀L2. ⦃G, L1⦄ ⊢ ➡*[h] L2 → R L2. +lemma lprs_ind_dx (h) (G) (L1): ∀Q:predicate lenv. Q L1 → + (∀L,L2. ⦃G, L1⦄ ⊢ ➡*[h] L → ⦃G, L⦄ ⊢ ➡[h] L2 → Q L → Q L2) → + ∀L2. ⦃G, L1⦄ ⊢ ➡*[h] L2 → Q L2. /4 width=8 by lprs_inv_CTC, lprs_CTC, lpr_cprs_trans, cpr_refl, lex_CTC_ind_dx/ qed-. (* Properties with unbound rt-transition for full local environments ********) diff --git a/matita/matita/contribs/lambdadelta/basic_2/rt_computation/lpxs.ma b/matita/matita/contribs/lambdadelta/basic_2/rt_computation/lpxs.ma index 9375fee8d..61fa33126 100644 --- a/matita/matita/contribs/lambdadelta/basic_2/rt_computation/lpxs.ma +++ b/matita/matita/contribs/lambdadelta/basic_2/rt_computation/lpxs.ma @@ -67,15 +67,15 @@ lemma lpxs_inv_pair_dx (h) (G): ∀I,L1,K2,V2. ⦃G, L1⦄ ⊢ ⬈*[h] K2.ⓑ{I} (* Basic eliminators ********************************************************) (* Basic_2A1: was: lpxs_ind_alt *) -lemma lpxs_ind (h) (G): ∀R:relation lenv. - R (⋆) (⋆) → ( +lemma lpxs_ind (h) (G): ∀Q:relation lenv. + Q (⋆) (⋆) → ( ∀I,K1,K2. ⦃G, K1⦄ ⊢ ⬈*[h] K2 → - R K1 K2 → R (K1.ⓘ{I}) (K2.ⓘ{I}) + Q K1 K2 → Q (K1.ⓘ{I}) (K2.ⓘ{I}) ) → ( ∀I,K1,K2,V1,V2. ⦃G, K1⦄ ⊢ ⬈*[h] K2 → ⦃G, K1⦄ ⊢ V1 ⬈*[h] V2 → - R K1 K2 → R (K1.ⓑ{I}V1) (K2.ⓑ{I}V2) + Q K1 K2 → Q (K1.ⓑ{I}V1) (K2.ⓑ{I}V2) ) → - ∀L1,L2. ⦃G, L1⦄ ⊢ ⬈*[h] L2 → R L1 L2. + ∀L1,L2. ⦃G, L1⦄ ⊢ ⬈*[h] L2 → Q L1 L2. /3 width=4 by lex_ind/ qed-. diff --git a/matita/matita/contribs/lambdadelta/basic_2/rt_computation/lpxs_lpx.ma b/matita/matita/contribs/lambdadelta/basic_2/rt_computation/lpxs_lpx.ma index f64f762ee..96def5301 100644 --- a/matita/matita/contribs/lambdadelta/basic_2/rt_computation/lpxs_lpx.ma +++ b/matita/matita/contribs/lambdadelta/basic_2/rt_computation/lpxs_lpx.ma @@ -36,15 +36,15 @@ lemma lpxs_step_dx (h) (G): ∀L1,L. ⦃G, L1⦄ ⊢ ⬈*[h] L → (* Eliminators with unbound rt-transition for full local environments *******) (* Basic_2A1: was: lpxs_ind_dx *) -lemma lpxs_ind_sn (h) (G) (L2): ∀R:predicate lenv. R L2 → - (∀L1,L. ⦃G, L1⦄ ⊢ ⬈[h] L → ⦃G, L⦄ ⊢ ⬈*[h] L2 → R L → R L1) → - ∀L1. ⦃G, L1⦄ ⊢ ⬈*[h] L2 → R L1. +lemma lpxs_ind_sn (h) (G) (L2): ∀Q:predicate lenv. Q L2 → + (∀L1,L. ⦃G, L1⦄ ⊢ ⬈[h] L → ⦃G, L⦄ ⊢ ⬈*[h] L2 → Q L → Q L1) → + ∀L1. ⦃G, L1⦄ ⊢ ⬈*[h] L2 → Q L1. /3 width=7 by lpx_cpxs_trans, cpx_refl, lex_CTC_ind_sn/ qed-. (* Basic_2A1: was: lpxs_ind *) -lemma lpxs_ind_dx (h) (G) (L1): ∀R:predicate lenv. R L1 → - (∀L,L2. ⦃G, L1⦄ ⊢ ⬈*[h] L → ⦃G, L⦄ ⊢ ⬈[h] L2 → R L → R L2) → - ∀L2. ⦃G, L1⦄ ⊢ ⬈*[h] L2 → R L2. +lemma lpxs_ind_dx (h) (G) (L1): ∀Q:predicate lenv. Q L1 → + (∀L,L2. ⦃G, L1⦄ ⊢ ⬈*[h] L → ⦃G, L⦄ ⊢ ⬈[h] L2 → Q L → Q L2) → + ∀L2. ⦃G, L1⦄ ⊢ ⬈*[h] L2 → Q L2. /3 width=7 by lpx_cpxs_trans, cpx_refl, lex_CTC_ind_dx/ qed-. (* Properties with context-sensitive extended rt-transition for terms *******) diff --git a/matita/matita/contribs/lambdadelta/basic_2/rt_computation/rdsx.ma b/matita/matita/contribs/lambdadelta/basic_2/rt_computation/rdsx.ma index ff62c4d6b..4503f5e3e 100644 --- a/matita/matita/contribs/lambdadelta/basic_2/rt_computation/rdsx.ma +++ b/matita/matita/contribs/lambdadelta/basic_2/rt_computation/rdsx.ma @@ -29,13 +29,13 @@ interpretation (* Basic_2A1: uses: lsx_ind *) lemma rdsx_ind (h) (o) (G) (T): - ∀R:predicate lenv. + ∀Q:predicate lenv. (∀L1. G ⊢ ⬈*[h, o, T] 𝐒⦃L1⦄ → - (∀L2. ⦃G, L1⦄ ⊢ ⬈[h] L2 → (L1 ≛[h, o, T] L2 → ⊥) → R L2) → - R L1 + (∀L2. ⦃G, L1⦄ ⊢ ⬈[h] L2 → (L1 ≛[h, o, T] L2 → ⊥) → Q L2) → + Q L1 ) → - ∀L. G ⊢ ⬈*[h, o, T] 𝐒⦃L⦄ → R L. -#h #o #G #T #R #H0 #L1 #H elim H -L1 + ∀L. G ⊢ ⬈*[h, o, T] 𝐒⦃L⦄ → Q L. +#h #o #G #T #Q #H0 #L1 #H elim H -L1 /5 width=1 by SN_intro/ qed-. diff --git a/matita/matita/contribs/lambdadelta/basic_2/rt_computation/rdsx_lpxs.ma b/matita/matita/contribs/lambdadelta/basic_2/rt_computation/rdsx_lpxs.ma index 6f6676e9c..c9f49cfe1 100644 --- a/matita/matita/contribs/lambdadelta/basic_2/rt_computation/rdsx_lpxs.ma +++ b/matita/matita/contribs/lambdadelta/basic_2/rt_computation/rdsx_lpxs.ma @@ -36,14 +36,14 @@ qed-. (* Eliminators with unbound rt-computation for full local environments ******) lemma rdsx_ind_lpxs_lfdeq (h) (o) (G): - ∀T. ∀R:predicate lenv. + ∀T. ∀Q:predicate lenv. (∀L1. G ⊢ ⬈*[h, o, T] 𝐒⦃L1⦄ → - (∀L2. ⦃G, L1⦄ ⊢ ⬈*[h] L2 → (L1 ≛[h, o, T] L2 → ⊥) → R L2) → - R L1 + (∀L2. ⦃G, L1⦄ ⊢ ⬈*[h] L2 → (L1 ≛[h, o, T] L2 → ⊥) → Q L2) → + Q L1 ) → ∀L1. G ⊢ ⬈*[h, o, T] 𝐒⦃L1⦄ → - ∀L0. ⦃G, L1⦄ ⊢ ⬈*[h] L0 → ∀L2. L0 ≛[h, o, T] L2 → R L2. -#h #o #G #T #R #IH #L1 #H @(rdsx_ind … H) -L1 + ∀L0. ⦃G, L1⦄ ⊢ ⬈*[h] L0 → ∀L2. L0 ≛[h, o, T] L2 → Q L2. +#h #o #G #T #Q #IH #L1 #H @(rdsx_ind … H) -L1 #L1 #HL1 #IH1 #L0 #HL10 #L2 #HL02 @IH -IH /3 width=3 by rdsx_lpxs_trans, rdsx_lfdeq_trans/ -HL1 #K2 #HLK2 #HnLK2 lapply (lfdeq_lfdneq_trans … HL02 … HnLK2) -HnLK2 #H @@ -62,13 +62,13 @@ qed-. (* Basic_2A1: uses: lsx_ind_alt *) lemma rdsx_ind_lpxs (h) (o) (G): - ∀T. ∀R:predicate lenv. + ∀T. ∀Q:predicate lenv. (∀L1. G ⊢ ⬈*[h, o, T] 𝐒⦃L1⦄ → - (∀L2. ⦃G, L1⦄ ⊢ ⬈*[h] L2 → (L1 ≛[h, o, T] L2 → ⊥) → R L2) → - R L1 + (∀L2. ⦃G, L1⦄ ⊢ ⬈*[h] L2 → (L1 ≛[h, o, T] L2 → ⊥) → Q L2) → + Q L1 ) → - ∀L. G ⊢ ⬈*[h, o, T] 𝐒⦃L⦄ → R L. -#h #o #G #T #R #IH #L #HL + ∀L. G ⊢ ⬈*[h, o, T] 𝐒⦃L⦄ → Q L. +#h #o #G #T #Q #IH #L #HL @(rdsx_ind_lpxs_lfdeq … IH … HL) -IH -HL // (**) (* full auto fails *) qed-. diff --git a/matita/matita/contribs/lambdadelta/basic_2/rt_equivalence/cpcs.ma b/matita/matita/contribs/lambdadelta/basic_2/rt_equivalence/cpcs.ma index 22d3b8ebf..59848b068 100644 --- a/matita/matita/contribs/lambdadelta/basic_2/rt_equivalence/cpcs.ma +++ b/matita/matita/contribs/lambdadelta/basic_2/rt_equivalence/cpcs.ma @@ -28,17 +28,17 @@ interpretation "context-sensitive parallel r-equivalence (term)" (* Basic_2A1: was: cpcs_ind_dx *) lemma cpcs_ind_sn (h) (G) (L) (T2): - ∀R:predicate term. R T2 → - (∀T1,T. ⦃G, L⦄ ⊢ T1 ⬌[h] T → ⦃G, L⦄ ⊢ T ⬌*[h] T2 → R T → R T1) → - ∀T1. ⦃G, L⦄ ⊢ T1 ⬌*[h] T2 → R T1. + ∀Q:predicate term. Q T2 → + (∀T1,T. ⦃G, L⦄ ⊢ T1 ⬌[h] T → ⦃G, L⦄ ⊢ T ⬌*[h] T2 → Q T → Q T1) → + ∀T1. ⦃G, L⦄ ⊢ T1 ⬌*[h] T2 → Q T1. normalize /3 width=6 by TC_star_ind_dx/ qed-. (* Basic_2A1: was: cpcs_ind *) lemma cpcs_ind_dx (h) (G) (L) (T1): - ∀R:predicate term. R T1 → - (∀T,T2. ⦃G, L⦄ ⊢ T1 ⬌*[h] T → ⦃G, L⦄ ⊢ T ⬌[h] T2 → R T → R T2) → - ∀T2. ⦃G, L⦄ ⊢ T1 ⬌*[h] T2 → R T2. + ∀Q:predicate term. Q T1 → + (∀T,T2. ⦃G, L⦄ ⊢ T1 ⬌*[h] T → ⦃G, L⦄ ⊢ T ⬌[h] T2 → Q T → Q T2) → + ∀T2. ⦃G, L⦄ ⊢ T1 ⬌*[h] T2 → Q T2. normalize /3 width=6 by TC_star_ind/ qed-. diff --git a/matita/matita/contribs/lambdadelta/basic_2/rt_transition/cpm.ma b/matita/matita/contribs/lambdadelta/basic_2/rt_transition/cpm.ma index 8d917e55f..3158b8b03 100644 --- a/matita/matita/contribs/lambdadelta/basic_2/rt_transition/cpm.ma +++ b/matita/matita/contribs/lambdadelta/basic_2/rt_transition/cpm.ma @@ -289,36 +289,36 @@ qed-. (* Basic eliminators ********************************************************) -lemma cpm_ind (h): ∀R:relation5 nat genv lenv term term. - (∀I,G,L. R 0 G L (⓪{I}) (⓪{I})) → - (∀G,L,s. R 1 G L (⋆s) (⋆(next h s))) → - (∀n,G,K,V1,V2,W2. ⦃G, K⦄ ⊢ V1 ➡[n, h] V2 → R n G K V1 V2 → - ⬆*[1] V2 ≘ W2 → R n G (K.ⓓV1) (#0) W2 - ) → (∀n,G,K,V1,V2,W2. ⦃G, K⦄ ⊢ V1 ➡[n, h] V2 → R n G K V1 V2 → - ⬆*[1] V2 ≘ W2 → R (↑n) G (K.ⓛV1) (#0) W2 - ) → (∀n,I,G,K,T,U,i. ⦃G, K⦄ ⊢ #i ➡[n, h] T → R n G K (#i) T → - ⬆*[1] T ≘ U → R n G (K.ⓘ{I}) (#↑i) (U) +lemma cpm_ind (h): ∀Q:relation5 nat genv lenv term term. + (∀I,G,L. Q 0 G L (⓪{I}) (⓪{I})) → + (∀G,L,s. Q 1 G L (⋆s) (⋆(next h s))) → + (∀n,G,K,V1,V2,W2. ⦃G, K⦄ ⊢ V1 ➡[n, h] V2 → Q n G K V1 V2 → + ⬆*[1] V2 ≘ W2 → Q n G (K.ⓓV1) (#0) W2 + ) → (∀n,G,K,V1,V2,W2. ⦃G, K⦄ ⊢ V1 ➡[n, h] V2 → Q n G K V1 V2 → + ⬆*[1] V2 ≘ W2 → Q (↑n) G (K.ⓛV1) (#0) W2 + ) → (∀n,I,G,K,T,U,i. ⦃G, K⦄ ⊢ #i ➡[n, h] T → Q n G K (#i) T → + ⬆*[1] T ≘ U → Q n G (K.ⓘ{I}) (#↑i) (U) ) → (∀n,p,I,G,L,V1,V2,T1,T2. ⦃G, L⦄ ⊢ V1 ➡[h] V2 → ⦃G, L.ⓑ{I}V1⦄ ⊢ T1 ➡[n, h] T2 → - R 0 G L V1 V2 → R n G (L.ⓑ{I}V1) T1 T2 → R n G L (ⓑ{p,I}V1.T1) (ⓑ{p,I}V2.T2) + Q 0 G L V1 V2 → Q n G (L.ⓑ{I}V1) T1 T2 → Q n G L (ⓑ{p,I}V1.T1) (ⓑ{p,I}V2.T2) ) → (∀n,G,L,V1,V2,T1,T2. ⦃G, L⦄ ⊢ V1 ➡[h] V2 → ⦃G, L⦄ ⊢ T1 ➡[n, h] T2 → - R 0 G L V1 V2 → R n G L T1 T2 → R n G L (ⓐV1.T1) (ⓐV2.T2) + Q 0 G L V1 V2 → Q n G L T1 T2 → Q n G L (ⓐV1.T1) (ⓐV2.T2) ) → (∀n,G,L,V1,V2,T1,T2. ⦃G, L⦄ ⊢ V1 ➡[n, h] V2 → ⦃G, L⦄ ⊢ T1 ➡[n, h] T2 → - R n G L V1 V2 → R n G L T1 T2 → R n G L (ⓝV1.T1) (ⓝV2.T2) - ) → (∀n,G,L,V,T1,T,T2. ⦃G, L.ⓓV⦄ ⊢ T1 ➡[n, h] T → R n G (L.ⓓV) T1 T → - ⬆*[1] T2 ≘ T → R n G L (+ⓓV.T1) T2 + Q n G L V1 V2 → Q n G L T1 T2 → Q n G L (ⓝV1.T1) (ⓝV2.T2) + ) → (∀n,G,L,V,T1,T,T2. ⦃G, L.ⓓV⦄ ⊢ T1 ➡[n, h] T → Q n G (L.ⓓV) T1 T → + ⬆*[1] T2 ≘ T → Q n G L (+ⓓV.T1) T2 ) → (∀n,G,L,V,T1,T2. ⦃G, L⦄ ⊢ T1 ➡[n, h] T2 → - R n G L T1 T2 → R n G L (ⓝV.T1) T2 + Q n G L T1 T2 → Q n G L (ⓝV.T1) T2 ) → (∀n,G,L,V1,V2,T. ⦃G, L⦄ ⊢ V1 ➡[n, h] V2 → - R n G L V1 V2 → R (↑n) G L (ⓝV1.T) V2 + Q n G L V1 V2 → Q (↑n) G L (ⓝV1.T) V2 ) → (∀n,p,G,L,V1,V2,W1,W2,T1,T2. ⦃G, L⦄ ⊢ V1 ➡[h] V2 → ⦃G, L⦄ ⊢ W1 ➡[h] W2 → ⦃G, L.ⓛW1⦄ ⊢ T1 ➡[n, h] T2 → - R 0 G L V1 V2 → R 0 G L W1 W2 → R n G (L.ⓛW1) T1 T2 → - R n G L (ⓐV1.ⓛ{p}W1.T1) (ⓓ{p}ⓝW2.V2.T2) + Q 0 G L V1 V2 → Q 0 G L W1 W2 → Q n G (L.ⓛW1) T1 T2 → + Q n G L (ⓐV1.ⓛ{p}W1.T1) (ⓓ{p}ⓝW2.V2.T2) ) → (∀n,p,G,L,V1,V,V2,W1,W2,T1,T2. ⦃G, L⦄ ⊢ V1 ➡[h] V → ⦃G, L⦄ ⊢ W1 ➡[h] W2 → ⦃G, L.ⓓW1⦄ ⊢ T1 ➡[n, h] T2 → - R 0 G L V1 V → R 0 G L W1 W2 → R n G (L.ⓓW1) T1 T2 → - ⬆*[1] V ≘ V2 → R n G L (ⓐV1.ⓓ{p}W1.T1) (ⓓ{p}W2.ⓐV2.T2) + Q 0 G L V1 V → Q 0 G L W1 W2 → Q n G (L.ⓓW1) T1 T2 → + ⬆*[1] V ≘ V2 → Q n G L (ⓐV1.ⓓ{p}W1.T1) (ⓓ{p}W2.ⓐV2.T2) ) → - ∀n,G,L,T1,T2. ⦃G, L⦄ ⊢ T1 ➡[n, h] T2 → R n G L T1 T2. -#h #R #IH1 #IH2 #IH3 #IH4 #IH5 #IH6 #IH7 #IH8 #IH9 #IH10 #IH11 #IH12 #IH13 #n #G #L #T1 #T2 + ∀n,G,L,T1,T2. ⦃G, L⦄ ⊢ T1 ➡[n, h] T2 → Q n G L T1 T2. +#h #Q #IH1 #IH2 #IH3 #IH4 #IH5 #IH6 #IH7 #IH8 #IH9 #IH10 #IH11 #IH12 #IH13 #n #G #L #T1 #T2 * #c #HC #H generalize in match HC; -HC generalize in match n; -n elim H -c -G -L -T1 -T2 [ #I #G #L #n #H <(isrt_inv_00 … H) -H // diff --git a/matita/matita/contribs/lambdadelta/basic_2/rt_transition/cpr.ma b/matita/matita/contribs/lambdadelta/basic_2/rt_transition/cpr.ma index 5751df0c9..091282ef3 100644 --- a/matita/matita/contribs/lambdadelta/basic_2/rt_transition/cpr.ma +++ b/matita/matita/contribs/lambdadelta/basic_2/rt_transition/cpr.ma @@ -101,29 +101,29 @@ qed-. (* Basic eliminators ********************************************************) -lemma cpr_ind (h): ∀R:relation4 genv lenv term term. - (∀I,G,L. R G L (⓪{I}) (⓪{I})) → - (∀G,K,V1,V2,W2. ⦃G, K⦄ ⊢ V1 ➡[h] V2 → R G K V1 V2 → - ⬆*[1] V2 ≘ W2 → R G (K.ⓓV1) (#0) W2 - ) → (∀I,G,K,T,U,i. ⦃G, K⦄ ⊢ #i ➡[h] T → R G K (#i) T → - ⬆*[1] T ≘ U → R G (K.ⓘ{I}) (#↑i) (U) +lemma cpr_ind (h): ∀Q:relation4 genv lenv term term. + (∀I,G,L. Q G L (⓪{I}) (⓪{I})) → + (∀G,K,V1,V2,W2. ⦃G, K⦄ ⊢ V1 ➡[h] V2 → Q G K V1 V2 → + ⬆*[1] V2 ≘ W2 → Q G (K.ⓓV1) (#0) W2 + ) → (∀I,G,K,T,U,i. ⦃G, K⦄ ⊢ #i ➡[h] T → Q G K (#i) T → + ⬆*[1] T ≘ U → Q G (K.ⓘ{I}) (#↑i) (U) ) → (∀p,I,G,L,V1,V2,T1,T2. ⦃G, L⦄ ⊢ V1 ➡[h] V2 → ⦃G, L.ⓑ{I}V1⦄ ⊢ T1 ➡[h] T2 → - R G L V1 V2 → R G (L.ⓑ{I}V1) T1 T2 → R G L (ⓑ{p,I}V1.T1) (ⓑ{p,I}V2.T2) + Q G L V1 V2 → Q G (L.ⓑ{I}V1) T1 T2 → Q G L (ⓑ{p,I}V1.T1) (ⓑ{p,I}V2.T2) ) → (∀I,G,L,V1,V2,T1,T2. ⦃G, L⦄ ⊢ V1 ➡[h] V2 → ⦃G, L⦄ ⊢ T1 ➡[h] T2 → - R G L V1 V2 → R G L T1 T2 → R G L (ⓕ{I}V1.T1) (ⓕ{I}V2.T2) - ) → (∀G,L,V,T1,T,T2. ⦃G, L.ⓓV⦄ ⊢ T1 ➡[h] T → R G (L.ⓓV) T1 T → - ⬆*[1] T2 ≘ T → R G L (+ⓓV.T1) T2 - ) → (∀G,L,V,T1,T2. ⦃G, L⦄ ⊢ T1 ➡[h] T2 → R G L T1 T2 → - R G L (ⓝV.T1) T2 + Q G L V1 V2 → Q G L T1 T2 → Q G L (ⓕ{I}V1.T1) (ⓕ{I}V2.T2) + ) → (∀G,L,V,T1,T,T2. ⦃G, L.ⓓV⦄ ⊢ T1 ➡[h] T → Q G (L.ⓓV) T1 T → + ⬆*[1] T2 ≘ T → Q G L (+ⓓV.T1) T2 + ) → (∀G,L,V,T1,T2. ⦃G, L⦄ ⊢ T1 ➡[h] T2 → Q G L T1 T2 → + Q G L (ⓝV.T1) T2 ) → (∀p,G,L,V1,V2,W1,W2,T1,T2. ⦃G, L⦄ ⊢ V1 ➡[h] V2 → ⦃G, L⦄ ⊢ W1 ➡[h] W2 → ⦃G, L.ⓛW1⦄ ⊢ T1 ➡[h] T2 → - R G L V1 V2 → R G L W1 W2 → R G (L.ⓛW1) T1 T2 → - R G L (ⓐV1.ⓛ{p}W1.T1) (ⓓ{p}ⓝW2.V2.T2) + Q G L V1 V2 → Q G L W1 W2 → Q G (L.ⓛW1) T1 T2 → + Q G L (ⓐV1.ⓛ{p}W1.T1) (ⓓ{p}ⓝW2.V2.T2) ) → (∀p,G,L,V1,V,V2,W1,W2,T1,T2. ⦃G, L⦄ ⊢ V1 ➡[h] V → ⦃G, L⦄ ⊢ W1 ➡[h] W2 → ⦃G, L.ⓓW1⦄ ⊢ T1 ➡[h] T2 → - R G L V1 V → R G L W1 W2 → R G (L.ⓓW1) T1 T2 → - ⬆*[1] V ≘ V2 → R G L (ⓐV1.ⓓ{p}W1.T1) (ⓓ{p}W2.ⓐV2.T2) + Q G L V1 V → Q G L W1 W2 → Q G (L.ⓓW1) T1 T2 → + ⬆*[1] V ≘ V2 → Q G L (ⓐV1.ⓓ{p}W1.T1) (ⓓ{p}W2.ⓐV2.T2) ) → - ∀G,L,T1,T2. ⦃G, L⦄ ⊢ T1 ➡[h] T2 → R G L T1 T2. -#h #R #IH1 #IH2 #IH3 #IH4 #IH5 #IH6 #IH7 #IH8 #IH9 #G #L #T1 #T2 + ∀G,L,T1,T2. ⦃G, L⦄ ⊢ T1 ➡[h] T2 → Q G L T1 T2. +#h #Q #IH1 #IH2 #IH3 #IH4 #IH5 #IH6 #IH7 #IH8 #IH9 #G #L #T1 #T2 @(insert_eq_0 … 0) #n #H @(cpm_ind … H) -G -L -T1 -T2 -n /3 width=4 by/ [ #G #L #s #H destruct diff --git a/matita/matita/contribs/lambdadelta/basic_2/rt_transition/cpx.ma b/matita/matita/contribs/lambdadelta/basic_2/rt_transition/cpx.ma index f01bb675b..c66c7e94d 100644 --- a/matita/matita/contribs/lambdadelta/basic_2/rt_transition/cpx.ma +++ b/matita/matita/contribs/lambdadelta/basic_2/rt_transition/cpx.ma @@ -231,31 +231,31 @@ qed-. (* Basic eliminators ********************************************************) -lemma cpx_ind: ∀h. ∀R:relation4 genv lenv term term. - (∀I,G,L. R G L (⓪{I}) (⓪{I})) → - (∀G,L,s. R G L (⋆s) (⋆(next h s))) → - (∀I,G,K,V1,V2,W2. ⦃G, K⦄ ⊢ V1 ⬈[h] V2 → R G K V1 V2 → - ⬆*[1] V2 ≘ W2 → R G (K.ⓑ{I}V1) (#0) W2 - ) → (∀I,G,K,T,U,i. ⦃G, K⦄ ⊢ #i ⬈[h] T → R G K (#i) T → - ⬆*[1] T ≘ U → R G (K.ⓘ{I}) (#↑i) (U) +lemma cpx_ind: ∀h. ∀Q:relation4 genv lenv term term. + (∀I,G,L. Q G L (⓪{I}) (⓪{I})) → + (∀G,L,s. Q G L (⋆s) (⋆(next h s))) → + (∀I,G,K,V1,V2,W2. ⦃G, K⦄ ⊢ V1 ⬈[h] V2 → Q G K V1 V2 → + ⬆*[1] V2 ≘ W2 → Q G (K.ⓑ{I}V1) (#0) W2 + ) → (∀I,G,K,T,U,i. ⦃G, K⦄ ⊢ #i ⬈[h] T → Q G K (#i) T → + ⬆*[1] T ≘ U → Q G (K.ⓘ{I}) (#↑i) (U) ) → (∀p,I,G,L,V1,V2,T1,T2. ⦃G, L⦄ ⊢ V1 ⬈[h] V2 → ⦃G, L.ⓑ{I}V1⦄ ⊢ T1 ⬈[h] T2 → - R G L V1 V2 → R G (L.ⓑ{I}V1) T1 T2 → R G L (ⓑ{p,I}V1.T1) (ⓑ{p,I}V2.T2) + Q G L V1 V2 → Q G (L.ⓑ{I}V1) T1 T2 → Q G L (ⓑ{p,I}V1.T1) (ⓑ{p,I}V2.T2) ) → (∀I,G,L,V1,V2,T1,T2. ⦃G, L⦄ ⊢ V1 ⬈[h] V2 → ⦃G, L⦄ ⊢ T1 ⬈[h] T2 → - R G L V1 V2 → R G L T1 T2 → R G L (ⓕ{I}V1.T1) (ⓕ{I}V2.T2) - ) → (∀G,L,V,T1,T,T2. ⦃G, L.ⓓV⦄ ⊢ T1 ⬈[h] T → R G (L.ⓓV) T1 T → - ⬆*[1] T2 ≘ T → R G L (+ⓓV.T1) T2 - ) → (∀G,L,V,T1,T2. ⦃G, L⦄ ⊢ T1 ⬈[h] T2 → R G L T1 T2 → - R G L (ⓝV.T1) T2 - ) → (∀G,L,V1,V2,T. ⦃G, L⦄ ⊢ V1 ⬈[h] V2 → R G L V1 V2 → - R G L (ⓝV1.T) V2 + Q G L V1 V2 → Q G L T1 T2 → Q G L (ⓕ{I}V1.T1) (ⓕ{I}V2.T2) + ) → (∀G,L,V,T1,T,T2. ⦃G, L.ⓓV⦄ ⊢ T1 ⬈[h] T → Q G (L.ⓓV) T1 T → + ⬆*[1] T2 ≘ T → Q G L (+ⓓV.T1) T2 + ) → (∀G,L,V,T1,T2. ⦃G, L⦄ ⊢ T1 ⬈[h] T2 → Q G L T1 T2 → + Q G L (ⓝV.T1) T2 + ) → (∀G,L,V1,V2,T. ⦃G, L⦄ ⊢ V1 ⬈[h] V2 → Q G L V1 V2 → + Q G L (ⓝV1.T) V2 ) → (∀p,G,L,V1,V2,W1,W2,T1,T2. ⦃G, L⦄ ⊢ V1 ⬈[h] V2 → ⦃G, L⦄ ⊢ W1 ⬈[h] W2 → ⦃G, L.ⓛW1⦄ ⊢ T1 ⬈[h] T2 → - R G L V1 V2 → R G L W1 W2 → R G (L.ⓛW1) T1 T2 → - R G L (ⓐV1.ⓛ{p}W1.T1) (ⓓ{p}ⓝW2.V2.T2) + Q G L V1 V2 → Q G L W1 W2 → Q G (L.ⓛW1) T1 T2 → + Q G L (ⓐV1.ⓛ{p}W1.T1) (ⓓ{p}ⓝW2.V2.T2) ) → (∀p,G,L,V1,V,V2,W1,W2,T1,T2. ⦃G, L⦄ ⊢ V1 ⬈[h] V → ⦃G, L⦄ ⊢ W1 ⬈[h] W2 → ⦃G, L.ⓓW1⦄ ⊢ T1 ⬈[h] T2 → - R G L V1 V → R G L W1 W2 → R G (L.ⓓW1) T1 T2 → - ⬆*[1] V ≘ V2 → R G L (ⓐV1.ⓓ{p}W1.T1) (ⓓ{p}W2.ⓐV2.T2) + Q G L V1 V → Q G L W1 W2 → Q G (L.ⓓW1) T1 T2 → + ⬆*[1] V ≘ V2 → Q G L (ⓐV1.ⓓ{p}W1.T1) (ⓓ{p}W2.ⓐV2.T2) ) → - ∀G,L,T1,T2. ⦃G, L⦄ ⊢ T1 ⬈[h] T2 → R G L T1 T2. -#h #R #IH1 #IH2 #IH3 #IH4 #IH5 #IH6 #IH7 #IH8 #IH9 #IH10 #IH11 #G #L #T1 #T2 + ∀G,L,T1,T2. ⦃G, L⦄ ⊢ T1 ⬈[h] T2 → Q G L T1 T2. +#h #Q #IH1 #IH2 #IH3 #IH4 #IH5 #IH6 #IH7 #IH8 #IH9 #IH10 #IH11 #G #L #T1 #T2 * #c #H elim H -c -G -L -T1 -T2 /3 width=4 by ex_intro/ qed-. diff --git a/matita/matita/contribs/lambdadelta/basic_2/s_computation/fqup.ma b/matita/matita/contribs/lambdadelta/basic_2/s_computation/fqup.ma index 5f14e8cec..a30e03a45 100644 --- a/matita/matita/contribs/lambdadelta/basic_2/s_computation/fqup.ma +++ b/matita/matita/contribs/lambdadelta/basic_2/s_computation/fqup.ma @@ -67,19 +67,19 @@ lemma fqup_flat_dx_bind_dx: ∀b,p,I1,I2,G,L,V1,V2,T. ⦃G, L, ⓕ{I1}V1.ⓑ{p,I (* Basic eliminators ********************************************************) -lemma fqup_ind: ∀b,G1,L1,T1. ∀R:relation3 …. - (∀G2,L2,T2. ⦃G1, L1, T1⦄ ⊐[b] ⦃G2, L2, T2⦄ → R G2 L2 T2) → - (∀G,G2,L,L2,T,T2. ⦃G1, L1, T1⦄ ⊐+[b] ⦃G, L, T⦄ → ⦃G, L, T⦄ ⊐[b] ⦃G2, L2, T2⦄ → R G L T → R G2 L2 T2) → - ∀G2,L2,T2. ⦃G1, L1, T1⦄ ⊐+[b] ⦃G2, L2, T2⦄ → R G2 L2 T2. -#b #G1 #L1 #T1 #R #IH1 #IH2 #G2 #L2 #T2 #H +lemma fqup_ind: ∀b,G1,L1,T1. ∀Q:relation3 …. + (∀G2,L2,T2. ⦃G1, L1, T1⦄ ⊐[b] ⦃G2, L2, T2⦄ → Q G2 L2 T2) → + (∀G,G2,L,L2,T,T2. ⦃G1, L1, T1⦄ ⊐+[b] ⦃G, L, T⦄ → ⦃G, L, T⦄ ⊐[b] ⦃G2, L2, T2⦄ → Q G L T → Q G2 L2 T2) → + ∀G2,L2,T2. ⦃G1, L1, T1⦄ ⊐+[b] ⦃G2, L2, T2⦄ → Q G2 L2 T2. +#b #G1 #L1 #T1 #Q #IH1 #IH2 #G2 #L2 #T2 #H @(tri_TC_ind … IH1 IH2 G2 L2 T2 H) qed-. -lemma fqup_ind_dx: ∀b,G2,L2,T2. ∀R:relation3 …. - (∀G1,L1,T1. ⦃G1, L1, T1⦄ ⊐[b] ⦃G2, L2, T2⦄ → R G1 L1 T1) → - (∀G1,G,L1,L,T1,T. ⦃G1, L1, T1⦄ ⊐[b] ⦃G, L, T⦄ → ⦃G, L, T⦄ ⊐+[b] ⦃G2, L2, T2⦄ → R G L T → R G1 L1 T1) → - ∀G1,L1,T1. ⦃G1, L1, T1⦄ ⊐+[b] ⦃G2, L2, T2⦄ → R G1 L1 T1. -#b #G2 #L2 #T2 #R #IH1 #IH2 #G1 #L1 #T1 #H +lemma fqup_ind_dx: ∀b,G2,L2,T2. ∀Q:relation3 …. + (∀G1,L1,T1. ⦃G1, L1, T1⦄ ⊐[b] ⦃G2, L2, T2⦄ → Q G1 L1 T1) → + (∀G1,G,L1,L,T1,T. ⦃G1, L1, T1⦄ ⊐[b] ⦃G, L, T⦄ → ⦃G, L, T⦄ ⊐+[b] ⦃G2, L2, T2⦄ → Q G L T → Q G1 L1 T1) → + ∀G1,L1,T1. ⦃G1, L1, T1⦄ ⊐+[b] ⦃G2, L2, T2⦄ → Q G1 L1 T1. +#b #G2 #L2 #T2 #Q #IH1 #IH2 #G1 #L1 #T1 #H @(tri_TC_ind_dx … IH1 IH2 G1 L1 T1 H) qed-. diff --git a/matita/matita/contribs/lambdadelta/basic_2/s_computation/fqup_weight.ma b/matita/matita/contribs/lambdadelta/basic_2/s_computation/fqup_weight.ma index 6b1f08b14..69af2d033 100644 --- a/matita/matita/contribs/lambdadelta/basic_2/s_computation/fqup_weight.ma +++ b/matita/matita/contribs/lambdadelta/basic_2/s_computation/fqup_weight.ma @@ -27,18 +27,18 @@ qed-. (* Advanced eliminators *****************************************************) -lemma fqup_wf_ind: ∀b. ∀R:relation3 …. ( - ∀G1,L1,T1. (∀G2,L2,T2. ⦃G1, L1, T1⦄ ⊐+[b] ⦃G2, L2, T2⦄ → R G2 L2 T2) → - R G1 L1 T1 - ) → ∀G1,L1,T1. R G1 L1 T1. -#b #R #HR @(f3_ind … fw) #x #IHx #G1 #L1 #T1 #H destruct +lemma fqup_wf_ind: ∀b. ∀Q:relation3 …. ( + ∀G1,L1,T1. (∀G2,L2,T2. ⦃G1, L1, T1⦄ ⊐+[b] ⦃G2, L2, T2⦄ → Q G2 L2 T2) → + Q G1 L1 T1 + ) → ∀G1,L1,T1. Q G1 L1 T1. +#b #Q #HQ @(f3_ind … fw) #x #IHx #G1 #L1 #T1 #H destruct /4 width=2 by fqup_fwd_fw/ qed-. -lemma fqup_wf_ind_eq: ∀b. ∀R:relation3 …. ( - ∀G1,L1,T1. (∀G2,L2,T2. ⦃G1, L1, T1⦄ ⊐+[b] ⦃G2, L2, T2⦄ → R G2 L2 T2) → - ∀G2,L2,T2. G1 = G2 → L1 = L2 → T1 = T2 → R G2 L2 T2 - ) → ∀G1,L1,T1. R G1 L1 T1. -#b #R #HR @(f3_ind … fw) #x #IHx #G1 #L1 #T1 #H destruct +lemma fqup_wf_ind_eq: ∀b. ∀Q:relation3 …. ( + ∀G1,L1,T1. (∀G2,L2,T2. ⦃G1, L1, T1⦄ ⊐+[b] ⦃G2, L2, T2⦄ → Q G2 L2 T2) → + ∀G2,L2,T2. G1 = G2 → L1 = L2 → T1 = T2 → Q G2 L2 T2 + ) → ∀G1,L1,T1. Q G1 L1 T1. +#b #Q #HQ @(f3_ind … fw) #x #IHx #G1 #L1 #T1 #H destruct /4 width=7 by fqup_fwd_fw/ qed-. diff --git a/matita/matita/contribs/lambdadelta/basic_2/s_computation/fqus.ma b/matita/matita/contribs/lambdadelta/basic_2/s_computation/fqus.ma index 5cc34a456..32555f1f6 100644 --- a/matita/matita/contribs/lambdadelta/basic_2/s_computation/fqus.ma +++ b/matita/matita/contribs/lambdadelta/basic_2/s_computation/fqus.ma @@ -30,17 +30,17 @@ interpretation "star-iterated structural successor (closure)" (* Basic eliminators ********************************************************) -lemma fqus_ind: ∀b,G1,L1,T1. ∀R:relation3 …. R G1 L1 T1 → - (∀G,G2,L,L2,T,T2. ⦃G1, L1, T1⦄ ⊐*[b] ⦃G, L, T⦄ → ⦃G, L, T⦄ ⊐⸮[b] ⦃G2, L2, T2⦄ → R G L T → R G2 L2 T2) → - ∀G2,L2,T2. ⦃G1, L1, T1⦄ ⊐*[b] ⦃G2, L2, T2⦄ → R G2 L2 T2. +lemma fqus_ind: ∀b,G1,L1,T1. ∀Q:relation3 …. Q G1 L1 T1 → + (∀G,G2,L,L2,T,T2. ⦃G1, L1, T1⦄ ⊐*[b] ⦃G, L, T⦄ → ⦃G, L, T⦄ ⊐⸮[b] ⦃G2, L2, T2⦄ → Q G L T → Q G2 L2 T2) → + ∀G2,L2,T2. ⦃G1, L1, T1⦄ ⊐*[b] ⦃G2, L2, T2⦄ → Q G2 L2 T2. #b #G1 #L1 #T1 #R #IH1 #IH2 #G2 #L2 #T2 #H @(tri_TC_star_ind … IH1 IH2 G2 L2 T2 H) // qed-. -lemma fqus_ind_dx: ∀b,G2,L2,T2. ∀R:relation3 …. R G2 L2 T2 → - (∀G1,G,L1,L,T1,T. ⦃G1, L1, T1⦄ ⊐⸮[b] ⦃G, L, T⦄ → ⦃G, L, T⦄ ⊐*[b] ⦃G2, L2, T2⦄ → R G L T → R G1 L1 T1) → - ∀G1,L1,T1. ⦃G1, L1, T1⦄ ⊐*[b] ⦃G2, L2, T2⦄ → R G1 L1 T1. -#b #G2 #L2 #T2 #R #IH1 #IH2 #G1 #L1 #T1 #H +lemma fqus_ind_dx: ∀b,G2,L2,T2. ∀Q:relation3 …. Q G2 L2 T2 → + (∀G1,G,L1,L,T1,T. ⦃G1, L1, T1⦄ ⊐⸮[b] ⦃G, L, T⦄ → ⦃G, L, T⦄ ⊐*[b] ⦃G2, L2, T2⦄ → Q G L T → Q G1 L1 T1) → + ∀G1,L1,T1. ⦃G1, L1, T1⦄ ⊐*[b] ⦃G2, L2, T2⦄ → Q G1 L1 T1. +#b #G2 #L2 #T2 #Q #IH1 #IH2 #G1 #L1 #T1 #H @(tri_TC_star_ind_dx … IH1 IH2 G1 L1 T1 H) // qed-. diff --git a/matita/matita/contribs/lambdadelta/basic_2/s_transition/fqu_weight.ma b/matita/matita/contribs/lambdadelta/basic_2/s_transition/fqu_weight.ma index 0ab12e5cc..8f6d321a2 100644 --- a/matita/matita/contribs/lambdadelta/basic_2/s_transition/fqu_weight.ma +++ b/matita/matita/contribs/lambdadelta/basic_2/s_transition/fqu_weight.ma @@ -29,9 +29,9 @@ qed-. (* Advanced eliminators *****************************************************) -lemma fqu_wf_ind: ∀b. ∀R:relation3 …. ( - ∀G1,L1,T1. (∀G2,L2,T2. ⦃G1, L1, T1⦄ ⊐[b] ⦃G2, L2, T2⦄ → R G2 L2 T2) → - R G1 L1 T1 - ) → ∀G1,L1,T1. R G1 L1 T1. -#b #R #HR @(f3_ind … fw) #x #IHx #G1 #L1 #T1 #H destruct /4 width=2 by fqu_fwd_fw/ +lemma fqu_wf_ind: ∀b. ∀Q:relation3 …. ( + ∀G1,L1,T1. (∀G2,L2,T2. ⦃G1, L1, T1⦄ ⊐[b] ⦃G2, L2, T2⦄ → Q G2 L2 T2) → + Q G1 L1 T1 + ) → ∀G1,L1,T1. Q G1 L1 T1. +#b #Q #HQ @(f3_ind … fw) #x #IHx #G1 #L1 #T1 #H destruct /4 width=2 by fqu_fwd_fw/ 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 fab29bbe6..217534a14 100644 --- a/matita/matita/contribs/lambdadelta/basic_2/static/frees_fqup.ma +++ b/matita/matita/contribs/lambdadelta/basic_2/static/frees_fqup.ma @@ -100,32 +100,32 @@ elim (pn_split f0) * #g0 #H destruct ] qed-. -lemma frees_ind_void: ∀R:relation3 …. +lemma frees_ind_void: ∀Q:relation3 …. ( - ∀f,L,s. 𝐈⦃f⦄ → R L (⋆s) f + ∀f,L,s. 𝐈⦃f⦄ → Q L (⋆s) f ) → ( - ∀f,i. 𝐈⦃f⦄ → R (⋆) (#i) (⫯*[i]↑f) + ∀f,i. 𝐈⦃f⦄ → Q (⋆) (#i) (⫯*[i]↑f) ) → ( ∀f,I,L,V. - L ⊢ 𝐅*⦃V⦄ ≘ f → R L V f→ R (L.ⓑ{I}V) (#O) (↑f) + L ⊢ 𝐅*⦃V⦄ ≘ f → Q L V f→ Q (L.ⓑ{I}V) (#O) (↑f) ) → ( - ∀f,I,L. 𝐈⦃f⦄ → R (L.ⓤ{I}) (#O) (↑f) + ∀f,I,L. 𝐈⦃f⦄ → Q (L.ⓤ{I}) (#O) (↑f) ) → ( ∀f,I,L,i. - L ⊢ 𝐅*⦃#i⦄ ≘ f → R L (#i) f → R (L.ⓘ{I}) (#(↑i)) (⫯f) + L ⊢ 𝐅*⦃#i⦄ ≘ f → Q L (#i) f → Q (L.ⓘ{I}) (#(↑i)) (⫯f) ) → ( - ∀f,L,l. 𝐈⦃f⦄ → R L (§l) f + ∀f,L,l. 𝐈⦃f⦄ → Q L (§l) f ) → ( ∀f1,f2,f,p,I,L,V,T. L ⊢ 𝐅*⦃V⦄ ≘ f1 → L.ⓧ ⊢𝐅*⦃T⦄≘ f2 → f1 ⋓ ⫱f2 ≘ f → - R L V f1 →R (L.ⓧ) T f2 → R L (ⓑ{p,I}V.T) f + Q L V f1 → Q (L.ⓧ) T f2 → Q L (ⓑ{p,I}V.T) f ) → ( ∀f1,f2,f,I,L,V,T. L ⊢ 𝐅*⦃V⦄ ≘ f1 → L ⊢𝐅*⦃T⦄ ≘ f2 → f1 ⋓ f2 ≘ f → - R L V f1 → R L T f2 → R L (ⓕ{I}V.T) f + Q L V f1 → Q L T f2 → Q L (ⓕ{I}V.T) f ) → - ∀L,T,f. L ⊢ 𝐅*⦃T⦄ ≘ f → R L T f. -#R #IH1 #IH2 #IH3 #IH4 #IH5 #IH6 #IH7 #IH8 #L #T + ∀L,T,f. L ⊢ 𝐅*⦃T⦄ ≘ f → Q L T f. +#Q #IH1 #IH2 #IH3 #IH4 #IH5 #IH6 #IH7 #IH8 #L #T @(fqup_wf_ind_eq (Ⓕ) … (⋆) L T) -L -T #G0 #L0 #T0 #IH #G #L * * [ #s #HG #HL #HT #f #H destruct -IH lapply (frees_inv_sort … H) -H /2 width=1 by/ diff --git a/matita/matita/contribs/lambdadelta/basic_2/static/lfxs.ma b/matita/matita/contribs/lambdadelta/basic_2/static/lfxs.ma index cc5b1e623..c9d55b73f 100644 --- a/matita/matita/contribs/lambdadelta/basic_2/static/lfxs.ma +++ b/matita/matita/contribs/lambdadelta/basic_2/static/lfxs.ma @@ -272,7 +272,7 @@ lemma lfxs_unit (R): ∀f,I,L1,L2. 𝐈⦃f⦄ → L1 ⪤*[cext2 R, cfull, f] L2 /4 width=3 by frees_unit, lexs_next, ext2_unit, ex2_intro/ qed. lemma lfxs_lref (R): ∀I1,I2,L1,L2,i. - L1 ⪤*[R, #i] L2 → L1.ⓘ{I1} ⪤*[R, #↑i] L2.ⓘ{I2}. + L1 ⪤*[R, #i] L2 → L1.ⓘ{I1} ⪤*[R, #↑i] L2.ⓘ{I2}. #R #I1 #I2 #L1 #L2 #i * /3 width=3 by lexs_push, frees_lref, ex2_intro/ qed. diff --git a/matita/matita/contribs/lambdadelta/basic_2/static/lfxs_drops.ma b/matita/matita/contribs/lambdadelta/basic_2/static/lfxs_drops.ma index 8e198ac76..76adfa38b 100644 --- a/matita/matita/contribs/lambdadelta/basic_2/static/lfxs_drops.ma +++ b/matita/matita/contribs/lambdadelta/basic_2/static/lfxs_drops.ma @@ -25,9 +25,9 @@ definition f_dedropable_sn: predicate (relation3 lenv term term) ≝ ∃∃L2. L1 ⪤*[R, U] L2 & ⬇*[b, f] L2 ≘ K2 & L1 ≡[f] L2. definition f_dropable_sn: predicate (relation3 lenv term term) ≝ - λR. ∀b,f,L1,K1. ⬇*[b, f] L1 ≘ K1 → 𝐔⦃f⦄ → - ∀L2,U. L1 ⪤*[R, U] L2 → ∀T. ⬆*[f] T ≘ U → - ∃∃K2. K1 ⪤*[R, T] K2 & ⬇*[b, f] L2 ≘ K2. + λR. ∀b,f,L1,K1. ⬇*[b, f] L1 ≘ K1 → 𝐔⦃f⦄ → + ∀L2,U. L1 ⪤*[R, U] L2 → ∀T. ⬆*[f] T ≘ U → + ∃∃K2. K1 ⪤*[R, T] K2 & ⬇*[b, f] L2 ≘ K2. definition f_dropable_dx: predicate (relation3 lenv term term) ≝ λR. ∀L1,L2,U. L1 ⪤*[R, U] L2 → diff --git a/matita/matita/contribs/lambdadelta/basic_2/syntax/append_length.ma b/matita/matita/contribs/lambdadelta/basic_2/syntax/append_length.ma index c1133e8c0..e7c79ebee 100644 --- a/matita/matita/contribs/lambdadelta/basic_2/syntax/append_length.ma +++ b/matita/matita/contribs/lambdadelta/basic_2/syntax/append_length.ma @@ -103,9 +103,9 @@ qed-. (* Basic_1: was: c_tail_ind *) (* Basic_2A1: was: lenv_ind_alt *) -lemma lenv_ind_tail: ∀R:predicate lenv. - R (⋆) → (∀I,L. R L → R (ⓘ{I}.L)) → ∀L. R L. -#R #IH1 #IH2 #L @(f_ind … length … L) -L #x #IHx * // +lemma lenv_ind_tail: ∀Q:predicate lenv. + Q (⋆) → (∀I,L. Q L → Q (ⓘ{I}.L)) → ∀L. Q L. +#Q #IH1 #IH2 #L @(f_ind … length … L) -L #x #IHx * // #L #I -IH1 #H destruct elim (lenv_case_tail … L) [2: * #K #J ] #H destruct /3 width=1 by/ -- 2.39.2