(* *)
(**************************************************************************)
+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".
โ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
| #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/
(* Properties with sd_d *****************************************************)
lemma sd_d_SS (h):
- รข\88\80s,d. sd_d h s (รข\86\91รข\86\91d) = sd_d h (รขยซยฏ[h]s) (โd).
+ รข\88\80s,d. sd_d h s (รข\86\91รข\86\91d) = sd_d h (รข\87ยก[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.