X-Git-Url: http://matita.cs.unibo.it/gitweb/?p=helm.git;a=blobdiff_plain;f=matita%2Fmatita%2Fcontribs%2Flambdadelta%2Fstatic_2%2Fsyntax%2Fsd_d.ma;h=10620b0bf19f96e8393fd81af2fdef640a708daa;hp=7c6f680e84f750f72900f7af7983691fb1b56761;hb=8fe4dc148d50a0352313633bea61441bc817afbf;hpb=cab35e3d6c09d266c1372b5cc9a0045578bae79b

diff --git a/matita/matita/contribs/lambdadelta/static_2/syntax/sd_d.ma b/matita/matita/contribs/lambdadelta/static_2/syntax/sd_d.ma
index 7c6f680e8..10620b0bf 100644
--- a/matita/matita/contribs/lambdadelta/static_2/syntax/sd_d.ma
+++ b/matita/matita/contribs/lambdadelta/static_2/syntax/sd_d.ma
@@ -12,6 +12,8 @@
 (*                                                                        *)
 (**************************************************************************)
 
+include "ground/generated/pull_2.ma".
+include "ground/arith/pnat_pred.ma".
 include "static_2/syntax/sh_props.ma".
 include "static_2/syntax/sd.ma".
 
@@ -36,13 +38,16 @@ lemma deg_SO_inv_succ (h) (s) (s0):
       ∀n. deg_SO h s s0 (↑n) → ⇡*[h,n]s0 = s.
 /2 width=3 by deg_SO_inv_succ_aux/ qed-.
 
-lemma deg_SO_refl (h) (s): deg_SO h s s 𝟏.
+lemma deg_SO_refl (h) (s):
+      deg_SO h s s 𝟏.
 #h #s @(deg_SO_succ … 𝟎 ?) //
 qed.
 
-definition sd_SO (h) (s): sd ≝ mk_sd (deg_SO h s).
+definition sd_SO (h) (s):
+           sd ≝ mk_sd (deg_SO h s).
 
-lemma sd_SO_props (h) (s): sh_decidable h → sh_acyclic h →
+lemma sd_SO_props (h) (s):
+      sh_decidable h → sh_acyclic h →
       sd_props h (sd_SO h s).
 #h #s #Hhd #Hha
 @mk_sd_props
@@ -61,26 +66,31 @@ lemma sd_SO_props (h) (s): sh_decidable h → sh_acyclic h →
 | #s0 #d *
   [ #n #H destruct
     <npred_succ @(nat_ind_succ … n) -n
-    [ @deg_SO_zero #n >(sh_nexts_succ_next h n s0) #H 
-      lapply (sh_nexts_inj … Hha ???) -H #H destruct
-    | #n @deg_SO_succ >sh_nexts_swap //
+    [ @deg_SO_zero #n >sh_nexts_succ_next #H
+      lapply (sh_nexts_inj … Hha … H) -H #H
+      elim (eq_inv_nsucc_zero … H)
+    | #n #_ /2 width=1 by deg_SO_succ/
     ]
-  | #H0 @deg_SO_zero #n >sh_nexts_swap #H destruct
+  | #H0 @deg_SO_zero #n >sh_nexts_succ_next #H destruct
     /2 width=2 by/
   ]
 ]
 qed.
 
-rec definition sd_d (h:?) (s:?) (d:?) on d: sd ≝
-   match d with
-   [ O   ⇒ sd_O
-   | S d ⇒ match d with
-           [ O ⇒ sd_SO h s
-           | _ ⇒ sd_d h (pr_next h s) d
-           ]
-   ].
+rec definition sd_d_pnat (h) (s) (d) on d: sd ≝
+match d with
+[ punit   ⇒ sd_SO h s
+| psucc d ⇒ sd_d_pnat h (⇡[h]s) d
+].
 
-lemma sd_d_props (h) (s) (d): sh_decidable h → sh_acyclic h →
+definition sd_d (h) (s) (d): sd ≝
+match d with
+[ nzero  ⇒ sd_O
+| ninj d ⇒ sd_d_pnat h s d
+].
+
+lemma sd_d_props (h) (s) (d):
+      sh_decidable h → sh_acyclic h →
       sd_props h (sd_d h s d).
 #h @pull_2 * [ // ]
 #d elim d -d /2 width=1 by sd_SO_props/
@@ -89,11 +99,17 @@ qed.
 (* Properties with sd_d *****************************************************)
 
 lemma sd_d_SS (h):
-      ∀s,d. sd_d h s (↑↑d) = sd_d h (⫯[h]s) (↑d).
+      ∀s,d. sd_d h s (↑↑d) = sd_d h (⇡[h]s) (↑d).
 // qed.
 
-lemma sd_d_correct (h): sh_decidable h → sh_acyclic h →
+lemma sd_d_correct (h):
+      sh_decidable h → sh_acyclic h →
       ∀s,d. deg (sd_d h s d) s d.
-#h #Hhd #Hha @pull_2 #d elim d -d [ // ]
-#d elim d -d /3 width=3 by deg_inv_pred, sd_d_props/
+#h #Hhd #Hha @pull_2 * [ // ]
+#d elim d -d [ // ] #d #IH #s
+>(npsucc_pred d) in ⊢ (???%);
+@(deg_inv_pred h)
+[ /2 width=1 by sd_d_props/
+| <nsucc_pnpred //
+]
 qed.