1 (**************************************************************************)
4 (* ||A|| A project by Andrea Asperti *)
6 (* ||I|| Developers: *)
7 (* ||T|| The HELM team. *)
8 (* ||A|| http://helm.cs.unibo.it *)
10 (* \ / This file is distributed under the terms of the *)
11 (* v GNU General Public License Version 2 *)
13 (**************************************************************************)
15 include "ground_2/pull/pull_2.ma".
16 include "static_2/syntax/sh_props.ma".
17 include "static_2/syntax/sd.ma".
19 (* SORT DEGREE **************************************************************)
21 (* Basic_2A1: includes: deg_SO_pos *)
22 inductive deg_SO (h) (s) (s0): predicate nat ≝
23 | deg_SO_succ : ∀n. (next h)^n s0 = s → deg_SO h s s0 (↑n)
24 | deg_SO_zero: (∀n. (next h)^n s0 = s → ⊥) → deg_SO h s s0 0
27 fact deg_SO_inv_succ_aux (h) (s) (s0):
28 ∀n0. deg_SO h s s0 n0 → ∀n. n0 = ↑n → (next h)^n s0 = s.
30 [ #n #Hn #x #H destruct //
35 (* Basic_2A1: was: deg_SO_inv_pos *)
36 lemma deg_SO_inv_succ (h) (s) (s0):
37 ∀n. deg_SO h s s0 (↑n) → (next h)^n s0 = s.
38 /2 width=3 by deg_SO_inv_succ_aux/ qed-.
40 lemma deg_SO_refl (h) (s): deg_SO h s s 1.
41 #h #s @(deg_SO_succ … 0 ?) //
44 definition sd_SO (h) (s): sd ≝ mk_sd (deg_SO h s).
46 lemma sd_SO_props (h) (s): sh_decidable h → sh_acyclic h →
47 sd_props h (sd_SO h s).
51 elim (nexts_dec … Hhd s0 s) -Hhd
52 [ * /3 width=2 by deg_SO_succ, ex_intro/
53 | /5 width=2 by deg_SO_zero, ex_intro/
55 | #s0 #d1 #d2 * [ #n1 ] #H1 * [1,3: #n2 ] #H2
57 lapply (nexts_inj … Hha … H) -H #H destruct //
58 | elim H1 /2 width=2 by ex_intro/
59 | elim H2 /2 width=2 by ex_intro/
63 [ #n #H destruct cases n -n normalize
64 [ @deg_SO_zero #n >iter_n_Sm #H
65 lapply (nexts_inj … Hha … (↑n) 0 H) -H #H destruct
66 | #n @deg_SO_succ >iter_n_Sm //
68 | #H0 @deg_SO_zero #n >iter_n_Sm #H destruct
74 rec definition sd_d (h:?) (s:?) (d:?) on d: sd ≝
79 | _ ⇒ sd_d h (next h s) d
83 lemma sd_d_props (h) (s) (d): sh_decidable h → sh_acyclic h →
84 sd_props h (sd_d h s d).
86 #d elim d -d /2 width=1 by sd_SO_props/
89 (* Properties with sd_d *****************************************************)
92 ∀s,d. sd_d h s (↑↑d) = sd_d h (⫯[h]s) (↑d).
95 lemma sd_d_correct (h): sh_decidable h → sh_acyclic h →
96 ∀s,d. deg (sd_d h s d) s d.
97 #h #Hhd #Hha @pull_2 #d elim d -d [ // ]
98 #d elim d -d /3 width=3 by deg_inv_pred, sd_d_props/