update in static_2 and basic_2

[helm.git] / matita / matita / contribs / lambdadelta / static_2 / syntax / ac.ma

diff --git a/matita/matita/contribs/lambdadelta/static_2/syntax/ac.ma b/matita/matita/contribs/lambdadelta/static_2/syntax/ac.ma
index 9968544cb9dfff4ac0dc483b2bbe50251e6a002f..1c411bb41a7d28f03ad5ee65a6e59a600c44dd3f 100644 (file)
--- a/matita/matita/contribs/lambdadelta/static_2/syntax/ac.ma
+++ b/matita/matita/contribs/lambdadelta/static_2/syntax/ac.ma
@@ -13,18 +13,21 @@
 (**************************************************************************)
 
 include "ground_2/lib/arith.ma".
+include "static_2/notation/functions/one_0.ma".
+include "static_2/notation/functions/two_0.ma".
+include "static_2/notation/functions/omega_0.ma".
 
 (* APPLICABILITY CONDITION  *************************************************)
 
 (* applicability condition specification *)
 record ac: Type[0] ≝ {
-(* degree of the sort *)
-   appl: predicate nat
+(* applicability domain *)
+   ad: predicate nat
 }.
 
 (* applicability condition postulates *)
 record ac_props (a): Prop ≝ {
-   ac_dec: ∀m. Decidable (∃∃n. m ≤ n & appl a n)
+   ac_dec: ∀m. Decidable (∃∃n. m ≤ n & ad a n)
 }.
 
 (* Notable specifications ***************************************************)
@@ -33,12 +36,21 @@ definition apply_top: predicate nat ≝ λn. ⊤.
 
 definition ac_top: ac ≝ mk_ac apply_top.
 
+interpretation "any number (applicability domain)"
+  'Omega = (ac_top).
+
 lemma ac_top_props: ac_props ac_top ≝ mk_ac_props ….
 /3 width=3 by or_introl, ex2_intro/
 qed.
 
 definition ac_eq (k): ac ≝ mk_ac (eq … k).
 
+interpretation "one (applicability domain)"
+  'Two = (ac_eq (S O)).
+
+interpretation "zero (applicability domain)"
+  'One = (ac_eq O).
+
 lemma ac_eq_props (k): ac_props (ac_eq k) ≝ mk_ac_props ….
 #m elim (le_dec m k) #Hm
 [ /3 width=3 by or_introl, ex2_intro/