deg : relation nat; (* degree of the sort *)
deg_total: ∀s. ∃d. deg s d; (* functional relation axioms *)
deg_mono : ∀s,d1,d2. deg s d1 → deg s d2 → d1 = d2;
- deg_next : â\88\80s,d. deg s d â\86\92 deg (next h s) (â«°d) (* compatibility condition *)
+ deg_next : â\88\80s,d. deg s d â\86\92 deg (next h s) (â\86\93d) (* compatibility condition *)
}.
(* Notable specifications ***************************************************)
(* Basic_2A1: includes: deg_SO_pos *)
inductive deg_SO (h:sh) (s:nat) (s0:nat): predicate nat ≝
-| deg_SO_succ : â\88\80n. (next h)^n s0 = s â\86\92 deg_SO h s s0 (⫯n)
+| deg_SO_succ : â\88\80n. (next h)^n s0 = s â\86\92 deg_SO h s s0 (â\86\91n)
| deg_SO_zero: ((∃n. (next h)^n s0 = s) → ⊥) → deg_SO h s s0 0
.
-fact deg_SO_inv_succ_aux: â\88\80h,s,s0,n0. deg_SO h s s0 n0 â\86\92 â\88\80n. n0 = ⫯n →
+fact deg_SO_inv_succ_aux: â\88\80h,s,s0,n0. deg_SO h s s0 n0 â\86\92 â\88\80n. n0 = â\86\91n →
(next h)^n s0 = s.
#h #s #s0 #n0 * -n0
[ #n #Hn #x #H destruct //
qed-.
(* Basic_2A1: was: deg_SO_inv_pos *)
-lemma deg_SO_inv_succ: â\88\80h,s,s0,n. deg_SO h s s0 (⫯n) → (next h)^n s0 = s.
+lemma deg_SO_inv_succ: â\88\80h,s,s0,n. deg_SO h s s0 (â\86\91n) → (next 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 1.
[ #d #H destruct elim d -d normalize
/2 width=1 by deg_SO_gt, deg_SO_succ, next_lt/
| #H1 @deg_SO_zero * #d #H2 destruct
- @H1 -H1 @(ex_intro â\80¦ (⫯d)) /2 width=1 by sym_eq/ (**) (* explicit constructor *)
+ @H1 -H1 @(ex_intro â\80¦ (â\86\91d)) /2 width=1 by sym_eq/ (**) (* explicit constructor *)
]
]
defined.
(* Basic inversion lemmas ***************************************************)
-lemma deg_inv_pred: â\88\80h,o,s,d. deg h o (next h s) (⫯d) â\86\92 deg h o s (⫯⫯d).
+lemma deg_inv_pred: â\88\80h,o,s,d. deg h o (next h s) (â\86\91d) â\86\92 deg h o s (â\86\91â\86\91d).
#h #o #s #d #H1
elim (deg_total h o s) #n #H0
lapply (deg_next … H0) #H2
lapply (deg_mono … H1 H2) -H1 -H2 #H >H >S_pred /2 width=2 by ltn_to_ltO/
qed-.
-lemma deg_inv_prec: â\88\80h,o,s,n,d. deg h o ((next h)^n s) (⫯d) â\86\92 deg h o s (⫯(d+n)).
+lemma deg_inv_prec: â\88\80h,o,s,n,d. deg h o ((next h)^n s) (â\86\91d) â\86\92 deg h o s (â\86\91(d+n)).
#h #o #s #n elim n -n normalize /3 width=1 by deg_inv_pred/
qed-.
#h #o #s #d #n elim n -n normalize /3 width=1 by deg_next/
qed.
-lemma deg_next_SO: â\88\80h,o,s,d. deg h o s (⫯d) → deg h o (next h s) d.
+lemma deg_next_SO: â\88\80h,o,s,d. deg h o s (â\86\91d) → deg h o (next h s) d.
/2 width=1 by deg_next/ qed-.
-lemma sd_d_SS: â\88\80h,s,d. sd_d h s (⫯⫯d) = sd_d h (next h s) (⫯d).
+lemma sd_d_SS: â\88\80h,s,d. sd_d h s (â\86\91â\86\91d) = sd_d h (next h s) (â\86\91d).
// qed.
lemma sd_d_correct: ∀h,d,s. deg h (sd_d h s d) s d.