update in ground_2, static_2, basic_2

[helm.git] / matita / matita / contribs / lambdadelta / basic_2 / etc / cnv / cnv_cpms_tdeq.etc

diff --git a/matita/matita/contribs/lambdadelta/basic_2/etc/cnv/cnv_cpms_tdeq.etc b/matita/matita/contribs/lambdadelta/basic_2/etc/cnv/cnv_cpms_tdeq.etc
deleted file mode 100644 (file)
index da15542..0000000
--- a/matita/matita/contribs/lambdadelta/basic_2/etc/cnv/cnv_cpms_tdeq.etc
+++ /dev/null
@@ -1,52 +0,0 @@
-(*
-axiom cpms_tdneq_fwd_step_sn (n) (h) (o) (G) (L):
-                             ∀T1,T2. ⦃G, L⦄ ⊢ T1 ➡*[n,h] T2 → (T1 ≛[h,o] T2 → ⊥) →
-                             ∃∃n1,n2,T,T0. ⦃G, L⦄ ⊢ T1 ➡[n1,h] T & T1 ≛[h,o] T → ⊥ & ⦃G, L⦄ ⊢ T ➡*[n2,h] T0 & T0 ≛[h,o] T2 & n1+n2 = n.
-axiom plus_Sxy_y_false: ∀y,x. ↑(x+y) = y → ⊥.
-
-lemma cnv_cpm_tdeq_trans (a) (h) (o) (G) (L):
-                         ∀T1. ⦃G,L⦄ ⊢ T1 ![a,h] →
-                         ∀n,T2.  ⦃G,L⦄ ⊢ T1 ➡[n,h] T2 → T1 ≛[h,o] T2 → ⦃G,L⦄ ⊢ T2 ![a,h].
-#a #h #o #G #L #T1 @(fqup_wf_ind_eq (Ⓣ) … G L T1) -G -L -T1
-#G0 #L0 #T0 #IH #G #L * [| * [| * ]]
-[ #I #_ #_ #_ #H0 #n #X #H1X #H2X -G0 -L0 -T0
-  elim (cpm_tdeq_inv_atom_sn … H1X H2X) -H1X -H2X *
-  [ #H #_ destruct //
-  | #s #H #_ #_ #_ destruct //
-  ]
-| #p #I #V1 #T1 #HG #HL #HT #H0 #n #X #H1X #H2X destruct
-  elim (cnv_inv_bind … H0) #HV1 #_
-  elim (cpm_tdeq_inv_bind_sn … H0 … H1X H2X) -H0 -H1X -H2X #T2 #H1T #H2T #H3T #H destruct
-  /3 width=6 by cnv_bind/
-| #V1 #T1 #HG #HL #HT #H0 #n #X #H1X #H2X destruct
-  elim (cnv_inv_appl … H0) #m #p #W1 #U1 #Hm #HV1 #_ #HVW1 #HTU1
-  elim (cpm_tdeq_inv_appl_sn … H0 … H1X H2X) -H0 -H1X -H2X #T2 #H1T #H2T #H3T #H destruct
-  @(cnv_appl … Hm … HVW1)
-
-(* Properties with restricted rt-transition for terms ***********************)
-
-lemma pippo (a) (h) (o) (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.
-#a #h #o #G #L #T1 @(fqup_wf_ind_eq (Ⓣ) … G L T1) -G -L -T1
-#G0 #L0 #T0 #IH #G #L * [| * [| * ]]
-[ #I #_ #_ #_ #_ #n1 #X1 #H1X #H2X #n2 #X2 #HX2 -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 #H1T1 #H2T1 #H3T1 #H destruct
-  elim (cpm_inv_bind1 … HX2) -HX2 *
-  [ #V2 #T2 #HV12 #HT2 #H destruct
-    elim (IH … H1T1 … H2T1 H3T1 … HT2) -IH -H1T1 -H2T1 -H3T1 -HT2 [2: // ] #T0 #HT10 #H1T02 #H2T02
-    @(ex3_intro … (ⓑ{p,I}V2.T0))
-    [ /2 width=1 by cpm_bind/
-    | 
-    | /2 width=1 by tdeq_pair/
-
-*)