update in static_2 and basic_2

+ restricted rt-computation;
  more results towards preservation

diff --git a/matita/matita/contribs/lambdadelta/basic_2/dynamic/cnv_cpm_tdeq.ma b/matita/matita/contribs/lambdadelta/basic_2/dynamic/cnv_cpm_tdeq.ma
index 85abc0c653b6cfea6fb069c446b22139bbae9681..4919e3eae1e717701e0dfbab19e8e70e80367fea 100644 (file)
--- a/matita/matita/contribs/lambdadelta/basic_2/dynamic/cnv_cpm_tdeq.ma
+++ b/matita/matita/contribs/lambdadelta/basic_2/dynamic/cnv_cpm_tdeq.ma
@@ -115,6 +115,16 @@ elim (cpm_inv_cast1 … H1) -H1 [ * || * ]
 ]
 qed-.
 
 ]
 qed-.
 

+lemma cpm_tdeq_inv_bind_dx (a) (h) (o) (n) (p) (I) (G) (L):
+                           ∀X. ⦃G, L⦄ ⊢ X ![a,h] →
+                           ∀V,T2. ⦃G, L⦄ ⊢ X ➡[n,h] ⓑ{p,I}V.T2 → X ≛[h,o]  ⓑ{p,I}V.T2 →
+                           ∃∃T1. ⦃G,L⦄ ⊢ V ![a,h] & ⦃G, L.ⓑ{I}V⦄ ⊢ T1 ![a,h] & ⦃G, L.ⓑ{I}V⦄ ⊢ T1 ➡[n,h] T2 & T1 ≛[h,o] T2 & X = ⓑ{p,I}V.T1.
+#a #h #o #n #p #I #G #L #X #H0 #V #T2 #H1 #H2
+elim (tdeq_inv_pair2 … H2) #V0 #T1 #_ #_ #H destruct
+elim (cpm_tdeq_inv_bind_sn … H0 … H1 H2) -H0 -H1 -H2 #T0 #HV #HT1 #H1T12 #H2T12 #H destruct
+/2 width=5 by ex5_intro/
+qed-.
+

 (* Eliminators with restricted rt-transition for terms **********************)
 
 lemma cpm_tdeq_ind (a) (h) (o) (n) (G) (Q:relation3 …):
 (* Eliminators with restricted rt-transition for terms **********************)
 
 lemma cpm_tdeq_ind (a) (h) (o) (n) (G) (Q:relation3 …):

diff --git a/matita/matita/contribs/lambdadelta/basic_2/dynamic/cnv_cpm_tdeq_trans.ma b/matita/matita/contribs/lambdadelta/basic_2/dynamic/cnv_cpm_tdeq_trans.ma
new file mode 100644 (file)
index 0000000..a0bda53
--- /dev/null
+++ b/matita/matita/contribs/lambdadelta/basic_2/dynamic/cnv_cpm_tdeq_trans.ma
@@ -0,0 +1,97 @@
+(**************************************************************************)
+(*       ___                                                              *)
+(*      ||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/dynamic/cnv_cpm_trans.ma".
+include "basic_2/dynamic/cnv_cpm_tdeq.ma".
+
+(* CONTEXT-SENSITIVE NATIVE VALIDITY FOR TERMS ******************************)
+
+definition IH_cnv_cpm_tdeq_cpm_trans (a) (h) (o): relation3 genv lenv term ≝
+           λG,L,T1. ⦃G, L⦄ ⊢ T1 ![a,h] →
+           ∀n1,T.  ⦃G,L⦄ ⊢ T1 ➡[n1,h] T → T1 ≛[h,o] T →
+           ∀n2,T2. ⦃G,L⦄ ⊢ T ➡[n2,h] T2 →
+           ∃∃T0. ⦃G,L⦄ ⊢ T1 ➡[n2,h] T0 & ⦃G,L⦄ ⊢ T0 ➡[n1,h] T2 & T0 ≛[h,o] T2.
+
+(* Transitive properties restricted rt-transition for terms *****************)
+
+fact cnv_cpm_tdeq_cpm_trans_sub (a) (h) (o) (G0) (L0) (T0):
+     (∀G,L,T. ⦃G0, L0, T0⦄ >[h,o] ⦃G, L, T⦄ → IH_cnv_cpm_trans_lpr a h G L T) →
+     (∀G,L,T. ⦃G0,L0,T0⦄ ⊐+ ⦃G,L,T⦄ → IH_cnv_cpm_tdeq_cpm_trans a h o G L T) →
+     ∀G,L,T1. G0 = G → L0 = L → T0 = T1 → IH_cnv_cpm_tdeq_cpm_trans a h o G L T1.
+#a #h #o #G0 #L0 #T0 #IH2 #IH1 #G #L * [| * [| * ]]
+[ #I #_ #_ #_ #_ #n1 #X1 #H1X #H2X #n2 #X2 #HX2 destruct -G0 -L0 -T0
+  elim (cpm_tdeq_inv_atom_sn … H1X H2X) -H1X -H2X *
+  [ #H1 #H2 destruct /2 width=4 by ex3_intro/
+  | #s #H1 #H2 #H3 #Hs destruct
+    elim (cpm_inv_sort1 … HX2) -HX2 #H #Hn2 destruct >iter_n_Sm
+    /5 width=6 by cpm_sort_iter, tdeq_sort, deg_iter, deg_next, ex3_intro/
+  ]
+| #p #I #V1 #T1 #HG #HL #HT #H0 #n1 #X1 #H1X #H2X #n2 #X2 #HX2 destruct
+  elim (cpm_tdeq_inv_bind_sn … H0 … H1X H2X) -H0 -H1X -H2X #T #_ #H0T1 #H1T1 #H2T1 #H destruct
+  elim (cpm_inv_bind1 … HX2) -HX2 *
+  [ #V2 #T2 #HV12 #HT2 #H destruct
+    elim (IH1 … H0T1 … H1T1 H2T1 … HT2) -T -IH1 [| // ] #T0 #HT10 #H1T02 #H2T02
+    lapply (IH2 … H0T1 … HT10 (L.ⓑ{I}V1) ?) -IH2 -H0T1 [3:|*: /2 width=1 by fqup_fpbg/ ] #HT0
+    lapply (cpm_tdeq_free … HT0 … H1T02 H2T02 G (L.ⓑ{I}V2)) -H1T02 #H1T02
+    /3 width=6 by cpm_bind, tdeq_pair, ex3_intro/
+  | #T2 #HT2 #HTX2 #H1 #H2 destruct -IH2
+    elim (tdeq_inv_lifts_dx … H2T1 … HT2) -H2T1 #XT #HXT1 #H2XT2
+    lapply (cpm_inv_lifts_bi … H1T1 (Ⓣ) … HXT1 … HT2) -T [3:|*: /3 width=2 by drops_refl, drops_drop/ ] #H1XT2
+    lapply (cnv_inv_lifts … H0T1 (Ⓣ) … HXT1) -H0T1 [3:|*: /3 width=2 by drops_refl, drops_drop/ ] #H0XT2
+    elim (IH1 … H0XT2 … H1XT2 H2XT2 … HTX2) -T2 -IH1 -H0XT2 [| /2 width=1 by fqup_zeta/ ] #T2 #HXT2 #H1TX2 #H2XT2
+    /3 width=4 by cpm_zeta, ex3_intro/
+  ]
+| #V1 #XT1 #HG #HL #HT #H0 #n1 #X1 #H1X #H2X #n2 #X2 #HX2 destruct
+  elim (cpm_tdeq_inv_appl_sn … H0 … H1X H2X) -H0 -H1X -H2X #m #q #W1 #U1 #XT #_ #_ #_ #_ #H0T1 #H1T1 #H2T1 #H destruct -m -q -W1 -U1
+  elim (cpm_inv_appl1 … HX2) -HX2 *
+  [ #V2 #T2 #HV12 #HT2 #H destruct -IH2
+    elim (IH1 … H0T1 … H1T1 H2T1 … HT2) -XT -IH1 -H0T1 [| // ] #T0 #HT10 #H1T02 #H2T02
+    /3 width=6 by cpm_appl, tdeq_pair, ex3_intro/
+  | #p #V2 #W1 #W2 #T #T2 #HV12 #HW12 #HT2 #H1 #H2 destruct
+    elim (cpm_tdeq_inv_bind_dx … H0T1 … H1T1 H2T1) -H0T1 -H1T1 -H2T1 #T1 #_ #H0T1 #H1T1 #H2T1 #H destruct
+    elim (IH1 … H0T1 … H1T1 H2T1 … HT2) -T -IH1 [| // ] #T0 #HT10 #H1T02 #H2T02
+    lapply (IH2 … H0T1 … HT10 (L.ⓛW1) ?) -IH2 -H0T1 [3:|*: /2 width=1 by fqup_fpbg/ ] #HT0
+    lapply (cpm_tdeq_free … HT0 … H1T02 H2T02 G (L.ⓓⓝW2.V2)) -H1T02 #H1T02
+    /3 width=6 by cpm_beta, cpm_bind, tdeq_pair, ex3_intro/
+  | #p #V2 #V0 #W1 #W2 #T #T2 #HV12 #HV20 #HW12 #HT2 #H1 #H2 destruct
+    elim (cpm_tdeq_inv_bind_dx … H0T1 … H1T1 H2T1) -H0T1 -H1T1 -H2T1 #T1 #_ #H0T1 #H1T1 #H2T1 #H destruct 
+    elim (IH1 … H0T1 … H1T1 H2T1 … HT2) -T -IH1 [| // ] #T0 #HT10 #H1T02 #H2T02
+    lapply (IH2 … H0T1 … HT10 (L.ⓓW1) ?) -IH2 -H0T1 [3:|*: /2 width=1 by fqup_fpbg/ ] #HT0
+    lapply (cpm_tdeq_free … HT0 … H1T02 H2T02 G (L.ⓓW2)) -H1T02
+    /4 width=8 by cpm_theta, cpm_appl, cpm_bind, tdeq_pair, ex3_intro/
+  ]
+| #U1 #T1 #HG #HL #HT #H0 #n1 #X1 #H1X #H2X #n2 #X2 #HX2 destruct -IH2
+  elim (cpm_tdeq_inv_cast_sn … H0 … H1X H2X) -H0 -H1X -H2X #U0 #U #T #_ #_ #H0U1 #H1U1 #H2U1 #H0T1 #H1T1 #H2T1 #H destruct -U0
+  elim (cpm_inv_cast1 … HX2) -HX2 [ * || * ]
+  [ #U2 #T2 #HU2 #HT2 #H destruct
+    elim (IH1 … H0U1 … H1U1 H2U1 … HU2) -U -H0U1 [| // ] #U0 #HU10 #H1U02 #H2U02
+    elim (IH1 … H0T1 … H1T1 H2T1 … HT2) -T -IH1 -H0T1 [| // ] #T0 #HT10 #H1T02 #H2T02
+    /3 width=6 by cpm_cast, tdeq_pair, ex3_intro/
+  | #HTX2 -U -H0U1
+    elim (IH1 … H0T1 … H1T1 H2T1 … HTX2) -T -IH1 -H0T1 [| // ] #T0 #HT10 #H1T02 #H2T02
+    /3 width=4 by cpm_eps, ex3_intro/
+  | #m2 #HUX2 #H destruct -T -H0T1
+    elim (IH1 … H0U1 … H1U1 H2U1 … HUX2) -U -H0U1 [| // ] #U0 #HU10 #H1U02 #H2U02
+    /3 width=4 by cpm_ee, ex3_intro/
+  ]
+]
+qed-.
+
+fact cnv_cpm_tdeq_cpm_trans_aux (a) (h) (o) (G0) (L0) (T0):
+     (∀G,L,T. ⦃G0, L0, T0⦄ >[h, o] ⦃G, L, T⦄ → IH_cnv_cpm_trans_lpr a h G L T) →
+     IH_cnv_cpm_tdeq_cpm_trans a h o G0 L0 T0.
+#a #h #o #G0 #L0 #T0
+@(fqup_wf_ind (Ⓣ) … G0 L0 T0) -G0 -L0 -T0 #G0 #L0 #T0 #IH #IH0
+/5 width=10 by cnv_cpm_tdeq_cpm_trans_sub, fqup_fpbg_trans/
+qed-.

diff --git a/matita/matita/contribs/lambdadelta/basic_2/dynamic/cnv_cpms_tdeq.ma b/matita/matita/contribs/lambdadelta/basic_2/dynamic/cnv_cpms_tdeq.ma
new file mode 100644 (file)
index 0000000..3950479
--- /dev/null
+++ b/matita/matita/contribs/lambdadelta/basic_2/dynamic/cnv_cpms_tdeq.ma
@@ -0,0 +1,65 @@
+(**************************************************************************)
+(*       ___                                                              *)
+(*      ||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/dynamic/cnv_cpm_tdeq_trans.ma".
+
+(* CONTEXT-SENSITIVE NATIVE VALIDITY FOR TERMS ******************************)
+
+(* Properties with restricted rt-computation for terms **********************)
+
+fact cpms_tdneq_fwd_step_sn_aux (a) (h) (n) (o) (G) (L) (T1):
+     ∀T2.  ⦃G, L⦄ ⊢ T1 ➡*[n,h] T2 → ⦃G, L⦄ ⊢ T1 ![a,h] → (T1 ≛[h,o] T2 → ⊥) →
+     (∀G0,L0,T0. ⦃G,L,T1⦄ >[h,o] ⦃G0,L0,T0⦄ → IH_cnv_cpms_conf_lpr a h G0 L0 T0) →
+     (∀G0,L0,T0. ⦃G,L,T1⦄ >[h,o] ⦃G0,L0,T0⦄ → IH_cnv_cpm_trans_lpr a h G0 L0 T0) →
+     ∃∃n1,n2,T0. ⦃G, L⦄ ⊢ T1 ➡[n1,h] T0 & T1 ≛[h,o] T0 → ⊥ & ⦃G, L⦄ ⊢ T0 ➡*[n2,h] T2 & n1+n2 = n.
+#a #h #n #o #G #L #T1 #T2 #H
+@(cpms_ind_sn … H) -n -T1
+[ #_ #H2T2 elim H2T2 -H2T2 //
+| #n1 #n2 #T1 #T #H1T1 #H1T2 #IH #H0T1 #H2T12 #IH2 #IH1
+  elim (tdeq_dec h o T1 T) #H2T1
+  [ elim (tdeq_dec h o T T2) #H2T2
+    [ -IH -IH2 -IH1 -H0T1 /4 width=7 by tdeq_trans, ex4_3_intro/
+    | lapply (cnv_cpm_trans_lpr_aux … IH2 IH1 … H1T1 L ?) [6:|*: // ] -H1T2 -H2T12 #H0T
+      elim (IH H0T H2T2) [|*: /4 width=5 by cpm_fpbq, fpbq_fpbg_trans/ ] -IH -IH2 -H0T -H2T2
+      #m1 #m2 #T0 #H1T0 #H2T0 #H1T02 #H destruct
+      elim (cnv_cpm_tdeq_cpm_trans_aux … IH1 … H0T1 … H1T1 H2T1 … H1T0) -IH1 -H0T1 -H1T1 -H1T0
+      #T3 #H1T13 #H1T30 #H2T30
+      @(ex4_3_intro … H1T13) /4 width=3 by cpms_step_sn, tdeq_canc_sn/ (**) (* explicit constructor *)
+    ]
+  | -IH -IH2 -IH1 -H2T12 /3 width=7 by tdeq_trans, ex4_3_intro/
+  ]
+]
+qed-.
+
+fact cpms_tdeq_ind_sn (a) (h) (o) (G) (L) (T2) (Q:relation2 …):
+     (⦃G, L⦄ ⊢ T2 ![a,h] → Q 0 T2) →
+     (∀n1,n2,T1,T. ⦃G,L⦄ ⊢ T1 ➡[n1,h] T → ⦃G, L⦄ ⊢ T1 ![a,h] → T1 ≛[h,o] T → ⦃G, L⦄ ⊢ T ➡*[n2,h] T2 → ⦃G, L⦄ ⊢ T ![a,h] → T ≛[h,o] T2 → Q n2 T → Q (n1+n2) T1) →
+     ∀n,T1. ⦃G, L⦄ ⊢ T1 ➡*[n,h] T2 → ⦃G, L⦄ ⊢ T1 ![a,h] → T1 ≛[h,o] T2 →
+     (∀G0,L0,T0. ⦃G,L,T1⦄ >[h,o] ⦃G0,L0,T0⦄ → IH_cnv_cpms_conf_lpr a h G0 L0 T0) →
+     (∀G0,L0,T0. ⦃G,L,T1⦄ >[h,o] ⦃G0,L0,T0⦄ → IH_cnv_cpm_trans_lpr a h G0 L0 T0) → 
+     Q n T1.
+#a #h #o #G #L #T2 #Q #IB1 #IB2 #n #T1 #H
+@(cpms_ind_sn … H) -n -T1
+[ -IB2 #H0T2 #_ #_ #_ /2 width=1 by/
+| #n1 #n2 #T1 #T #H1T1 #H1T2 #IH #H0T1 #H2T12 #IH2 #IH1 -IB1
+  elim (tdeq_dec h o T1 T) #H2T1
+  [ lapply (cnv_cpm_trans_lpr_aux … IH2 IH1 … H1T1 L ?) [6:|*: // ] #H0T
+    lapply (tdeq_canc_sn … H2T1 … H2T12) -H2T12 #H2T2
+    /6 width=7 by cpm_fpbq, fpbq_fpbg_trans/
+  | -IB2 -IH -IH2 -IH1
+    elim (cnv_fpbg_refl_false … o … H0T1) -a -Q
+    /3 width=8 by cpm_tdneq_cpm_cpms_tdeq_sym_fwd_fpbg/
+  ]
+]
+qed-.

diff --git a/matita/matita/contribs/lambdadelta/basic_2/etc/tdpos/cnv_cpm_tdpos.etc b/matita/matita/contribs/lambdadelta/basic_2/etc/tdpos/cnv_cpm_tdpos.etc
new file mode 100644 (file)
index 0000000..4cb3209
--- /dev/null
+++ b/matita/matita/contribs/lambdadelta/basic_2/etc/tdpos/cnv_cpm_tdpos.etc
@@ -0,0 +1,55 @@
+(**************************************************************************)
+(*       ___                                                              *)
+(*      ||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 "static_2/syntax/tdpos.ma".
+include "basic_2/dynamic/cnv_cpm_tdeq.ma".
+
+(* CONTEXT-SENSITIVE NATIVE VALIDITY FOR TERMS ******************************)
+
+(* Forward lemmas with positive rt-transition for terms *********************)
+
+lemma cpm_tdeq_fwd_tdpos_sn (a) (h) (o) (n) (G):
+                            ∀L,T1. ⦃G,L⦄ ⊢ T1 ![a,h] →
+                            ∀T2. ⦃G,L⦄ ⊢ T1 ➡[n,h] T2 → T1 ≛[h,o] T2 → 𝐏[h,o]⦃T1⦄ →
+                            ∧∧ T1 = T2 & 0 = n.
+#a #h #o #n #G #L #T1 #H0 #T2 #H1 #H2
+@(cpm_tdeq_ind … H0 … H1 H2) -L -T1 -T2
+[ /2 width=1 by conj/
+| #L #s #_ #H1 #H
+  elim (tdpos_inv_sort … H) -H #d #H2
+  lapply (deg_mono … H2 H1) -H1 -H2 #H destruct
+| #p #I #L #V #T1 #_ #_ #T2 #_ #_ #IH #H
+  elim (tdpos_inv_pair … H) -H #_ #HT1
+  elim IH // -IH -HT1 #H1 #H2 destruct
+  /2 width=1 by conj/
+| #m #_ #L #V #_ #W #_ #q #T1 #U1 #_ #_ #T2 #_ #_ #IH #H -a -m -q -G -L -W -U1
+  elim (tdpos_inv_pair … H) -H #_ #HT1
+  elim IH // -IH -HT1 #H1 #H2 destruct
+  /2 width=1 by conj/
+| #L #U0 #U1 #T1 #_ #_ #U2 #_ #_ #_ #T2 #_ #_ #_ #IHU #IHT #H
+  elim (tdpos_inv_pair … H) -H #HU1 #HT1
+  elim IHU // -IHU -HU1 #H1 #H2 destruct
+  elim IHT // -IHT -HT1 #H1 #H2 destruct
+  /2 width=1 by conj/
+]
+qed-.
+
+lemma cpm_fwd_tdpos_sn (a) (h) (o) (n) (G) (L):
+                       ∀T1. ⦃G,L⦄ ⊢ T1 ![a,h] → 𝐏[h,o]⦃T1⦄ →
+                       ∀T2. ⦃G,L⦄ ⊢ T1 ➡[n,h] T2 →
+                       ∨∨ ∧∧ T1 = T2 & 0 = n | (T1 ≛[h,o] T2 → ⊥).
+#a #h #o #n #G #L #T1 #H1T1 #H2T1 #T2 #HT12
+elim (tdeq_dec h o T1 T2) #H
+/3 width=9 by cpm_tdeq_fwd_tdpos_sn, or_intror, or_introl/
+qed-.

diff --git a/matita/matita/contribs/lambdadelta/basic_2/etc/tdpos/cnv_cpms_tdpos.etc b/matita/matita/contribs/lambdadelta/basic_2/etc/tdpos/cnv_cpms_tdpos.etc
new file mode 100644 (file)
index 0000000..049e072
--- /dev/null
+++ b/matita/matita/contribs/lambdadelta/basic_2/etc/tdpos/cnv_cpms_tdpos.etc
@@ -0,0 +1,39 @@
+(**************************************************************************)
+(*       ___                                                              *)
+(*      ||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/dynamic/cnv_cpm_tdpos.ma".
+
+(* CONTEXT-SENSITIVE NATIVE VALIDITY FOR TERMS ******************************)
+
+(* Forward lemmas with positive rt-computation for terms ********************)
+
+lemma cpms_fwd_tdpos_sn (a) (h) (o) (n) (G) (L):
+                        ∀T1. ⦃G,L⦄ ⊢ T1 ![a,h] → 𝐏[h,o]⦃T1⦄ →
+                        ∀T2. ⦃G,L⦄ ⊢ T1 ➡*[n,h] T2 →
+                        ∨∨ ∧∧ T1 = T2 & 0 = n
+                         | ∃∃n1,n2,T. ⦃G,L⦄ ⊢ T1 ➡[n1,h] T & (T1 ≛[h,o] T → ⊥) & ⦃G,L⦄ ⊢ T ➡*[n2,h] T2 & n1+n2=n.
+#a #h #o #n #G #L #T1 #H1T1 #H2T1 #T2 #H
+@(cpms_ind_dx … H) -n -T2
+[ /3 width=1 by or_introl, conj/
+| #n1 #n2 #T #T2 #HT1 * *
+  [ #H1 #H2 #HT2 destruct -HT1
+    elim (cpm_fwd_tdpos_sn … H1T1 H2T1 … HT2) -H1T1 -H2T1
+    [ * #H1 #H2 destruct -HT2 /3 width=1 by or_introl, conj/
+    | #HnT2 >commutative_plus in ⊢ (??%); /4 width=7 by ex4_3_intro, or_intror/
+    ]
+  | #m1 #m2 #T0 #H1T10 #H2T10 #HT0 #H #HT2 destruct -H1T1 -H2T1 -HT1
+    >associative_plus in ⊢ (??%); /4 width=7 by cpms_step_dx, ex4_3_intro, or_intror/
+  ]
+]
+qed-.

diff --git a/matita/matita/contribs/lambdadelta/basic_2/etc/tdpos/positive_3.etc b/matita/matita/contribs/lambdadelta/basic_2/etc/tdpos/positive_3.etc
new file mode 100644 (file)
index 0000000..e73de49
--- /dev/null
+++ b/matita/matita/contribs/lambdadelta/basic_2/etc/tdpos/positive_3.etc
@@ -0,0 +1,19 @@
+(**************************************************************************)
+(*       ___                                                              *)
+(*      ||M||                                                             *)
+(*      ||A||       A project by Andrea Asperti                           *)
+(*      ||T||                                                             *)
+(*      ||I||       Developers:                                           *)
+(*      ||T||         The HELM team.                                      *)
+(*      ||A||         http://helm.cs.unibo.it                             *)
+(*      \   /                                                             *)
+(*       \ /        This file is distributed under the terms of the       *)
+(*        v         GNU General Public License Version 2                  *)
+(*                                                                        *)
+(**************************************************************************)
+
+(* NOTATION FOR THE FORMAL SYSTEM λδ ****************************************)
+
+notation "hvbox( 𝐏 [ term 46 h, term 46 o ] ⦃ term 46 T ⦄ )"
+   non associative with precedence 45
+   for @{ 'Positive $h $o $T }.

diff --git a/matita/matita/contribs/lambdadelta/basic_2/etc/tdpos/tdpos.etc b/matita/matita/contribs/lambdadelta/basic_2/etc/tdpos/tdpos.etc
new file mode 100644 (file)
index 0000000..1b6b119
--- /dev/null
+++ b/matita/matita/contribs/lambdadelta/basic_2/etc/tdpos/tdpos.etc
@@ -0,0 +1,63 @@
+(**************************************************************************)
+(*       ___                                                              *)
+(*      ||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 "static_2/notation/relations/positive_3.ma".
+include "static_2/syntax/item_sd.ma".
+include "static_2/syntax/term.ma".
+
+(* DEGREE POSITIVITY ON TERMS ***********************************************)
+
+inductive tdpos (h) (o): predicate term ≝
+| tdpos_sort: ∀s,d. deg h o s (↑d) → tdpos h o (⋆s)
+| tdpos_lref: ∀i. tdpos h o (#i)
+| tdpos_gref: ∀l. tdpos h o (§l)
+| tdpos_pair: ∀I,V,T. tdpos h o V → tdpos h o T → tdpos h o (②{I}V.T)
+.
+
+interpretation
+   "context-free degree positivity (term)"
+   'Positive h o T = (tdpos h o T).
+
+(* Basic inversion lemmas ***************************************************)
+
+fact tdpos_inv_sort_aux (h) (o): 
+                        ∀X. 𝐏[h,o]⦃X⦄ → ∀s. X = ⋆s → ∃d. deg h o s (↑d).
+#h #o #H *
+[ #s #d #Hsd #x #H destruct /2 width=2 by ex_intro/
+| #i #x #H destruct
+| #l #x #H destruct
+| #I #V #T #_ #_ #x #H destruct
+]
+qed-.
+
+lemma tdpos_inv_sort (h) (o): ∀s. 𝐏[h,o]⦃⋆s⦄ → ∃d. deg h o s (↑d).
+/2 width=3 by tdpos_inv_sort_aux/ qed-.
+
+fact tdpos_inv_pair_aux (h) (o): ∀X. 𝐏[h,o]⦃X⦄ → ∀I,V,T. X = ②{I}V.T →
+                                 ∧∧ 𝐏[h,o]⦃V⦄ & 𝐏[h,o]⦃T⦄.
+#h #o #H *
+[ #s #d #_ #Z #X1 #X2 #H destruct
+| #i #Z #X1 #X2 #H destruct
+| #l #Z #X1 #X2 #H destruct
+| #I #V #T #HV #HT #Z #X1 #X2 #H destruct /2 width=1 by conj/
+]
+qed-.
+
+lemma tdpos_inv_pair (h) (o): ∀I,V,T. 𝐏[h,o]⦃②{I}V.T⦄ →
+                              ∧∧ 𝐏[h,o]⦃V⦄ & 𝐏[h,o]⦃T⦄.
+/2 width=4 by tdpos_inv_pair_aux/ qed-.
+
+(* Basic properties *********************************************************)
+
+axiom tdpos_total (h): ∀T. ∃o. 𝐏[h,o]⦃T⦄.

diff --git a/matita/matita/contribs/lambdadelta/basic_2/rt_computation/cpms_fpbg.ma b/matita/matita/contribs/lambdadelta/basic_2/rt_computation/cpms_fpbg.ma
index ea81fda63064b3edb93c7029293187503f983fd3..7584e81c958387d86623830876b0c4b01bd3955c 100644 (file)
--- a/matita/matita/contribs/lambdadelta/basic_2/rt_computation/cpms_fpbg.ma
+++ b/matita/matita/contribs/lambdadelta/basic_2/rt_computation/cpms_fpbg.ma
@@ -20,10 +20,6 @@ include "basic_2/rt_computation/cpms_fpbs.ma".
 
 (* Forward lemmas with proper parallel rst-computation for closures *********)
 
 
 (* Forward lemmas with proper parallel rst-computation for closures *********)
 

-lemma fqup_cpms_fwd_fpbg (h) (o): ∀G1,G2,L1,L2,T1,T. ⦃G1, L1, T1⦄ ⊐+ ⦃G2, L2, T⦄ →
-                                  ∀n,T2. ⦃G2, L2⦄ ⊢ T ➡*[n,h] T2 → ⦃G1, L1, T1⦄ >[h,o] ⦃G2, L2, T2⦄.
-/3 width=5 by cpms_fwd_fpbs, fqup_fpbg,fpbg_fpbs_trans/ qed-.
-

 lemma fpbg_cpms_trans (h) (o) (n): ∀G1,G2,L1,L2,T1,T. ⦃G1, L1, T1⦄ >[h,o] ⦃G2, L2, T⦄ →
                                    ∀T2. ⦃G2, L2⦄ ⊢ T ➡*[n,h] T2 → ⦃G1, L1, T1⦄ >[h,o] ⦃G2, L2, T2⦄.
 /3 width=5 by fpbg_fpbs_trans, cpms_fwd_fpbs/ qed-.
 lemma fpbg_cpms_trans (h) (o) (n): ∀G1,G2,L1,L2,T1,T. ⦃G1, L1, T1⦄ >[h,o] ⦃G2, L2, T⦄ →
                                    ∀T2. ⦃G2, L2⦄ ⊢ T ➡*[n,h] T2 → ⦃G1, L1, T1⦄ >[h,o] ⦃G2, L2, T2⦄.
 /3 width=5 by fpbg_fpbs_trans, cpms_fwd_fpbs/ qed-.


@@ -31,3 +27,14 @@ lemma fpbg_cpms_trans (h) (o) (n): ∀G1,G2,L1,L2,T1,T. ⦃G1, L1, T1⦄ >[h,o]
 lemma cpms_fpbg_trans (h) (o) (n): ∀G1,L1,T1,T. ⦃G1, L1⦄ ⊢ T1 ➡*[n,h] T →
                                    ∀G2,L2,T2. ⦃G1, L1, T⦄ >[h,o] ⦃G2, L2, T2⦄ → ⦃G1, L1, T1⦄ >[h,o] ⦃G2, L2, T2⦄.
 /3 width=5 by fpbs_fpbg_trans, cpms_fwd_fpbs/ qed-.
 lemma cpms_fpbg_trans (h) (o) (n): ∀G1,L1,T1,T. ⦃G1, L1⦄ ⊢ T1 ➡*[n,h] T →
                                    ∀G2,L2,T2. ⦃G1, L1, T⦄ >[h,o] ⦃G2, L2, T2⦄ → ⦃G1, L1, T1⦄ >[h,o] ⦃G2, L2, T2⦄.
 /3 width=5 by fpbs_fpbg_trans, cpms_fwd_fpbs/ qed-.

+
+lemma fqup_cpms_fwd_fpbg (h) (o): ∀G1,G2,L1,L2,T1,T. ⦃G1, L1, T1⦄ ⊐+ ⦃G2, L2, T⦄ →
+                                  ∀n,T2. ⦃G2, L2⦄ ⊢ T ➡*[n,h] T2 → ⦃G1, L1, T1⦄ >[h,o] ⦃G2, L2, T2⦄.
+/3 width=5 by cpms_fwd_fpbs, fqup_fpbg,fpbg_fpbs_trans/ qed-.
+
+lemma cpm_tdneq_cpm_cpms_tdeq_sym_fwd_fpbg (h) (o) (G) (L) (T1):
+      ∀n1,T. ⦃G,L⦄ ⊢ T1 ➡[n1,h] T → (T1 ≛[h,o] T → ⊥) →
+      ∀n2,T2. ⦃G,L⦄⊢ T ➡*[n2,h] T2 → T1 ≛[h,o] T2 → ⦃G,L,T1⦄ >[h,o] ⦃G,L,T1⦄.
+#h #o #G #L #T1 #n1 #T #H1T1 #H2T1 #n2 #T2 #H1T2 #H2T12
+/4 width=7 by cpms_fwd_fpbs, cpm_fpb, fpbs_tdeq_trans, tdeq_sym, ex2_3_intro/
+qed-.

diff --git a/matita/matita/contribs/lambdadelta/basic_2/rt_computation/fpbg_fpbs.ma b/matita/matita/contribs/lambdadelta/basic_2/rt_computation/fpbg_fpbs.ma
index 3641326f8177364d577bedc2f4d0e964177c08cf..d7a1ccae06e091ef9a0396aa2af7c639a53cdae3 100644 (file)
--- a/matita/matita/contribs/lambdadelta/basic_2/rt_computation/fpbg_fpbs.ma
+++ b/matita/matita/contribs/lambdadelta/basic_2/rt_computation/fpbg_fpbs.ma
@@ -12,9 +12,9 @@
 (*                                                                        *)
 (**************************************************************************)
 
 (*                                                                        *)
 (**************************************************************************)
 

-include "static_2/static/fdeq_fqup.ma".

 include "static_2/static/fdeq_fdeq.ma".
 include "basic_2/rt_transition/fpbq_fpb.ma".
 include "static_2/static/fdeq_fdeq.ma".
 include "basic_2/rt_transition/fpbq_fpb.ma".

+include "basic_2/rt_computation/fpbs_fqup.ma".

 include "basic_2/rt_computation/fpbg.ma".
 
 (* PROPER PARALLEL RST-COMPUTATION FOR CLOSURES *****************************)
 include "basic_2/rt_computation/fpbg.ma".
 
 (* PROPER PARALLEL RST-COMPUTATION FOR CLOSURES *****************************)


@@ -61,6 +61,13 @@ lemma fpbs_fpbg_trans: ∀h,o,G1,G,L1,L,T1,T. ⦃G1, L1, T1⦄ ≥[h, o] ⦃G, L
 #h #o #G1 #G #L1 #L #T1 #T #H @(fpbs_ind … H) -G -L -T /3 width=5 by fpbq_fpbg_trans/
 qed-.
 
 #h #o #G1 #G #L1 #L #T1 #T #H @(fpbs_ind … H) -G -L -T /3 width=5 by fpbq_fpbg_trans/
 qed-.
 

+(* Advanced properties with plus-iterated structural successor for closures *)
+
+lemma fqup_fpbg_trans (h) (o):
+      ∀G1,G,L1,L,T1,T. ⦃G1,L1,T1⦄ ⊐+ ⦃G,L,T⦄ →
+      ∀G2,L2,T2. ⦃G,L,T⦄ >[h,o] ⦃G2,L2,T2⦄ → ⦃G1,L1,T1⦄ >[h,o] ⦃G2,L2,T2⦄.
+/3 width=5 by fpbs_fpbg_trans, fqup_fpbs/ qed-.
+

 (* Advanced inversion lemmas of parallel rst-computation on closures ********)
 
 (* Basic_2A1: was: fpbs_fpbg *)
 (* Advanced inversion lemmas of parallel rst-computation on closures ********)
 
 (* Basic_2A1: was: fpbs_fpbg *)

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 4ab5cff5158f89858a59da58262be730d804d42f..d0d19e4a757f10ddc6a73badfe35d69b0564dd72 100644 (file)
--- a/matita/matita/contribs/lambdadelta/basic_2/rt_transition/cpm.ma
+++ b/matita/matita/contribs/lambdadelta/basic_2/rt_transition/cpm.ma
@@ -232,6 +232,13 @@ elim (cpm_inv_bind1 … H) -H
 ]
 qed-.
 
 ]
 qed-.
 

+lemma cpm_inv_abst_bi: ∀n,h,p1,p2,G,L,V1,V2,T1,T2. ⦃G,L⦄ ⊢ ⓛ{p1}V1.T1 ➡[n,h] ⓛ{p2}V2.T2 →
+                       ∧∧ ⦃G,L⦄ ⊢ V1 ➡[h] V2 & ⦃G,L.ⓛV1⦄ ⊢ T1 ➡[n,h] T2 & p1 = p2.
+#n #h #p1 #p2 #G #L #V1 #V2 #T1 #T2 #H
+elim (cpm_inv_abst1 … H) -H #XV #XT #HV #HT #H destruct
+/2 width=1 by and3_intro/  
+qed-.
+

 (* Basic_1: includes: pr0_gen_appl pr2_gen_appl *)
 (* Basic_2A1: includes: cpr_inv_appl1 *)
 lemma cpm_inv_appl1: ∀n,h,G,L,V1,U1,U2. ⦃G, L⦄ ⊢ ⓐ V1.U1 ➡[n, h] U2 →
 (* Basic_1: includes: pr0_gen_appl pr2_gen_appl *)
 (* Basic_2A1: includes: cpr_inv_appl1 *)
 lemma cpm_inv_appl1: ∀n,h,G,L,V1,U1,U2. ⦃G, L⦄ ⊢ ⓐ V1.U1 ➡[n, h] U2 →

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 336b99505200d567a0526766bb125a98d31ab3fb..e10340776579bb9acad0c7b502e2e06ac54a9967 100644 (file)
--- a/matita/matita/contribs/lambdadelta/basic_2/web/basic_2_src.tbl
+++ b/matita/matita/contribs/lambdadelta/basic_2/web/basic_2_src.tbl
@@ -31,7 +31,7 @@ table {
 *)
         [ { "context-sensitive native validity" * } {
              [ [ "restricted refinement for lenvs" ] "lsubv ( ? ⊢ ? ⫃![?,?] ? )" "lsubv_drops" + "lsubv_lsubr" + "lsubv_lsuba" + "lsubv_cpms" + "lsubv_cpcs" + "lsubv_cnv" + "lsubv_lsubv" * ]
 *)
         [ { "context-sensitive native validity" * } {
              [ [ "restricted refinement for lenvs" ] "lsubv ( ? ⊢ ? ⫃![?,?] ? )" "lsubv_drops" + "lsubv_lsubr" + "lsubv_lsuba" + "lsubv_cpms" + "lsubv_cpcs" + "lsubv_cnv" + "lsubv_lsubv" * ]

-             [ [ "for terms" ] "cnv" + "( ⦃?,?⦄ ⊢ ? ![?,?] )" "cnv_drops" + "cnv_fqus" + "cnv_aaa" + "cnv_fsb" + "cnv_cpm_trans" + "cnv_cpm_conf" + "cnv_cpm_tdeq" + "cnv_cpm_tdpos" + "cnv_cpms_tdpos" + "cnv_cpms_conf" + "cnv_preserve_sub" + "cnv_preserve" * ]
+             [ [ "for terms" ] "cnv" + "( ⦃?,?⦄ ⊢ ? ![?,?] )" "cnv_drops" + "cnv_fqus" + "cnv_aaa" + "cnv_fsb" + "cnv_cpm_trans" + "cnv_cpm_conf" + "cnv_cpm_tdeq" + "cnv_cpm_tfeq_trans" + "cnv_cpms_tdeq" + "cnv_cpms_conf" + "cnv_preserve_sub" + "cnv_preserve" * ]

           }
         ]
      }
           }
         ]
      }

diff --git a/matita/matita/contribs/lambdadelta/static_2/relocation/lifts.ma b/matita/matita/contribs/lambdadelta/static_2/relocation/lifts.ma
index 1d6225393ab9c483dee902e2184ac9fddd898fd5..060f3b8057d843e509201ed69a526d62895c6f01 100644 (file)
--- a/matita/matita/contribs/lambdadelta/static_2/relocation/lifts.ma
+++ b/matita/matita/contribs/lambdadelta/static_2/relocation/lifts.ma
@@ -56,6 +56,10 @@ definition deliftable2_bi: predicate (relation term) ≝
                            λR. ∀U1,U2. R U1 U2 → ∀f,T1. ⬆*[f] T1 ≘ U1 →
                            ∀T2. ⬆*[f] T2 ≘ U2 → R T1 T2.
 
                            λR. ∀U1,U2. R U1 U2 → ∀f,T1. ⬆*[f] T1 ≘ U1 →
                            ∀T2. ⬆*[f] T2 ≘ U2 → R T1 T2.
 

+definition deliftable2_dx: predicate (relation term) ≝
+                           λR. ∀U1,U2. R U1 U2 → ∀f,T2. ⬆*[f] T2 ≘ U2 →
+                           ∃∃T1. ⬆*[f] T1 ≘ U1 & R T1 T2.
+

 (* Basic inversion lemmas ***************************************************)
 
 fact lifts_inv_sort1_aux: ∀f,X,Y. ⬆*[f] X ≘ Y → ∀s. X = ⋆s → Y = ⋆s.
 (* Basic inversion lemmas ***************************************************)
 
 fact lifts_inv_sort1_aux: ∀f,X,Y. ⬆*[f] X ≘ Y → ∀s. X = ⋆s → Y = ⋆s.


@@ -329,6 +333,11 @@ qed-.
 
 (* Basic properties *********************************************************)
 
 
 (* Basic properties *********************************************************)
 

+lemma deliftable2_sn_dx (R): symmetric … R → deliftable2_sn R → deliftable2_dx R.
+#R #H2R #H1R #U1 #U2 #HU12 #f #T2 #HTU2
+elim (H1R … U1 … HTU2) -H1R /3 width=3 by ex2_intro/
+qed-.
+

 lemma lifts_eq_repl_back: ∀T1,T2. eq_repl_back … (λf. ⬆*[f] T1 ≘ T2).
 #T1 #T2 #f1 #H elim H -T1 -T2 -f1
 /4 width=5 by lifts_flat, lifts_bind, lifts_lref, at_eq_repl_back, eq_push/
 lemma lifts_eq_repl_back: ∀T1,T2. eq_repl_back … (λf. ⬆*[f] T1 ≘ T2).
 #T1 #T2 #f1 #H elim H -T1 -T2 -f1
 /4 width=5 by lifts_flat, lifts_bind, lifts_lref, at_eq_repl_back, eq_push/

diff --git a/matita/matita/contribs/lambdadelta/static_2/relocation/lifts_tdeq.ma b/matita/matita/contribs/lambdadelta/static_2/relocation/lifts_tdeq.ma
index fb5d8247f0d32188a677b6b18effa26094d79fb6..12affa3a16a3af71a20070431cb5b934cf22cabc 100644 (file)
--- a/matita/matita/contribs/lambdadelta/static_2/relocation/lifts_tdeq.ma
+++ b/matita/matita/contribs/lambdadelta/static_2/relocation/lifts_tdeq.ma
@@ -62,6 +62,9 @@ lemma tdeq_inv_lifts_sn: ∀h,o. deliftable2_sn (tdeq h o).
 ]
 qed-.
 
 ]
 qed-.
 

+lemma tdeq_inv_lifts_dx (h) (o): deliftable2_dx (tdeq h o).
+/3 width=3 by tdeq_inv_lifts_sn, deliftable2_sn_dx, tdeq_sym/ qed-.
+

 lemma tdeq_inv_lifts_bi: ∀h,o. deliftable2_bi (tdeq h o).
 /3 width=6 by tdeq_inv_lifts_sn, deliftable2_sn_bi/ qed-.
 
 lemma tdeq_inv_lifts_bi: ∀h,o. deliftable2_bi (tdeq h o).
 /3 width=6 by tdeq_inv_lifts_sn, deliftable2_sn_bi/ qed-.
 

diff --git a/matita/matita/contribs/lambdadelta/static_2/syntax/tdeq.ma b/matita/matita/contribs/lambdadelta/static_2/syntax/tdeq.ma
index d008d5e86653bc6b3cb20fed35948f96039e9da0..828e2ad0fbdb4b985f86efe6a5b1699368753217 100644 (file)
--- a/matita/matita/contribs/lambdadelta/static_2/syntax/tdeq.ma
+++ b/matita/matita/contribs/lambdadelta/static_2/syntax/tdeq.ma
@@ -29,6 +29,19 @@ interpretation
    "context-free degree-based equivalence (term)"
    'StarEq h o T1 T2 = (tdeq h o T1 T2).
 
    "context-free degree-based equivalence (term)"
    'StarEq h o T1 T2 = (tdeq h o T1 T2).
 

+(* Basic properties *********************************************************)
+
+lemma tdeq_refl: ∀h,o. reflexive … (tdeq h o).
+#h #o #T elim T -T /2 width=1 by tdeq_pair/
+* /2 width=1 by tdeq_lref, tdeq_gref/
+#s elim (deg_total h o s) /2 width=3 by tdeq_sort/
+qed.
+
+lemma tdeq_sym: ∀h,o. symmetric … (tdeq h o).
+#h #o #T1 #T2 #H elim H -T1 -T2
+/2 width=3 by tdeq_sort, tdeq_lref, tdeq_gref, tdeq_pair/
+qed-.
+

 (* Basic inversion lemmas ***************************************************)
 
 fact tdeq_inv_sort1_aux: ∀h,o,X,Y. X ≛[h, o] Y → ∀s1. X = ⋆s1 →
 (* Basic inversion lemmas ***************************************************)
 
 fact tdeq_inv_sort1_aux: ∀h,o,X,Y. X ≛[h, o] Y → ∀s1. X = ⋆s1 →


@@ -79,6 +92,14 @@ lemma tdeq_inv_pair1: ∀h,o,I,V1,T1,Y. ②{I}V1.T1 ≛[h, o] Y →
                       ∃∃V2,T2. V1 ≛[h, o] V2 & T1 ≛[h, o] T2 & Y = ②{I}V2.T2.
 /2 width=3 by tdeq_inv_pair1_aux/ qed-.
 
                       ∃∃V2,T2. V1 ≛[h, o] V2 & T1 ≛[h, o] T2 & Y = ②{I}V2.T2.
 /2 width=3 by tdeq_inv_pair1_aux/ qed-.
 

+lemma tdeq_inv_pair2: ∀h,o,I,X1,V2,T2. X1 ≛[h, o] ②{I}V2.T2 →
+                      ∃∃V1,T1. V1 ≛[h, o] V2 & T1 ≛[h, o] T2 & X1 = ②{I}V1.T1.
+#h #o #I #X1 #V2 #T2 #H
+elim (tdeq_inv_pair1 h o I V2 T2 X1)
+[ #V1 #T1 #HV #HT #H destruct ]
+/3 width=5 by tdeq_sym, ex3_2_intro/
+qed-.
+

 (* Advanced inversion lemmas ************************************************)
 
 lemma tdeq_inv_sort1_deg: ∀h,o,Y,s1. ⋆s1 ≛[h, o] Y → ∀d. deg h o s1 d →
 (* Advanced inversion lemmas ************************************************)
 
 lemma tdeq_inv_sort1_deg: ∀h,o,Y,s1. ⋆s1 ≛[h, o] Y → ∀d. deg h o s1 d →


@@ -122,18 +143,7 @@ lemma tdeq_fwd_atom1: ∀h,o,I,Y. ⓪{I} ≛[h, o] Y → ∃J. Y = ⓪{J}.
 /3 width=4 by tdeq_inv_gref1, tdeq_inv_lref1, ex_intro/
 qed-.
 
 /3 width=4 by tdeq_inv_gref1, tdeq_inv_lref1, ex_intro/
 qed-.
 

-(* Basic properties *********************************************************)
-
-lemma tdeq_refl: ∀h,o. reflexive … (tdeq h o).
-#h #o #T elim T -T /2 width=1 by tdeq_pair/
-* /2 width=1 by tdeq_lref, tdeq_gref/
-#s elim (deg_total h o s) /2 width=3 by tdeq_sort/
-qed.
-
-lemma tdeq_sym: ∀h,o. symmetric … (tdeq h o).
-#h #o #T1 #T2 #H elim H -T1 -T2
-/2 width=3 by tdeq_sort, tdeq_lref, tdeq_gref, tdeq_pair/
-qed-.
+(* Advanced properties ******************************************************)

 
 lemma tdeq_dec: ∀h,o,T1,T2. Decidable (T1 ≛[h, o] T2).
 #h #o #T1 elim T1 -T1 [ * #s1 | #I1 #V1 #T1 #IHV #IHT ] * [1,3,5,7: * #s2 |*: #I2 #V2 #T2 ]
 
 lemma tdeq_dec: ∀h,o,T1,T2. Decidable (T1 ≛[h, o] T2).
 #h #o #T1 elim T1 -T1 [ * #s1 | #I1 #V1 #T1 #IHV #IHT ] * [1,3,5,7: * #s2 |*: #I2 #V2 #T2 ]

diff --git a/matita/matita/contribs/lambdadelta/static_2/web/static_2_src.tbl b/matita/matita/contribs/lambdadelta/static_2/web/static_2_src.tbl
index 1f7d34c0b7e8b5c2aad79159281d015c7d331539..4dcb17989792c92c27f91ceed6ccd0f3bc47d2c5 100644 (file)
--- a/matita/matita/contribs/lambdadelta/static_2/web/static_2_src.tbl
+++ b/matita/matita/contribs/lambdadelta/static_2/web/static_2_src.tbl
@@ -111,10 +111,6 @@ table {
              [ [ "for terms" ] "theq" + "( ? ⩳[?,?] ? )" "theq_simple" + "theq_tdeq" + "theq_theq" + "theq_simple_vector" * ]
           }
         ]
              [ [ "for terms" ] "theq" + "( ? ⩳[?,?] ? )" "theq_simple" + "theq_tdeq" + "theq_theq" + "theq_simple_vector" * ]
           }
         ]

-        [ { "degree positivity" * } {
-             [ [ "for terms" ] "tdpos" + "( 𝐏[?,?]⦃?⦄ )" * ]
-          }
-        ]

         [ { "degree-based equivalence" * } {
              [ [ "" ] "tdeq_ext" + "( ? ≛[?,?] ? )" + "( ? ⊢ ? ≛[?,?] ? )" * ]
              [ [ "" ] "tdeq" + "( ? ≛[?,?] ? )" "tdeq_tdeq" * ]
         [ { "degree-based equivalence" * } {
              [ [ "" ] "tdeq_ext" + "( ? ≛[?,?] ? )" + "( ? ⊢ ? ≛[?,?] ? )" * ]
              [ [ "" ] "tdeq" + "( ? ≛[?,?] ? )" "tdeq_tdeq" * ]