- we introduced the pointer_step rc in the perspective of proving

[helm.git] / matita / matita / contribs / lambda_delta / basic_2 / static / sh.ma

diff --git a/matita/matita/contribs/lambda_delta/basic_2/static/sh.ma b/matita/matita/contribs/lambda_delta/basic_2/static/sh.ma
index 4eeac01b881f8d8073a5cc84ac94a911d61dd6af..72df7717ec4eec724ca02d2d5502c8a5f7a16457 100644 (file)
--- a/matita/matita/contribs/lambda_delta/basic_2/static/sh.ma
+++ b/matita/matita/contribs/lambda_delta/basic_2/static/sh.ma
@@ -16,8 +16,21 @@ include "ground_2/arith.ma".
 
 (* SORT HIERARCHY ***********************************************************)
 
-(* sort hierarchy specifications *)
+(* sort hierarchy specification *)
 record sh: Type[0] ≝ {
-   next: nat → nat;        (* next sort in the hierarchy *)
+   next   : nat → nat;     (* next sort in the hierarchy *)
    next_lt: ∀k. k < next k (* strict monotonicity condition *)
 }.
+
+(* Basic properties *********************************************************)
+
+lemma nexts_le: ∀h,k,l. k ≤ (next h)^l k.
+#h #k #l elim l -l // normalize #l #IHl
+lapply (next_lt h ((next h)^l k)) #H
+lapply (le_to_lt_to_lt … IHl H) -IHl -H /2 width=2/
+qed.
+
+axiom nexts_dec: ∀h,k1,k2. Decidable (∃l. (next h)^l k1 = k2).
+
+axiom nexts_inj: ∀h,k,l1,l2. (next h)^l1 k = (next h)^l2 k → l1 = l2.
+