- list.ma: improved notation for constant lists (a "term 19" was missing)

[helm.git] / matita / matita / contribs / lambda / st_computation.ma

diff --git a/matita/matita/contribs/lambda/st_computation.ma b/matita/matita/contribs/lambda/st_computation.ma
index c9f9aa9477f6dc1be2369b003948b2fe9aaf6704..028cd8a41bfc3ae80657c7c21e7dfc4542fadd56 100644 (file)
--- a/matita/matita/contribs/lambda/st_computation.ma
+++ b/matita/matita/contribs/lambda/st_computation.ma
@@ -20,8 +20,24 @@ include "labelled_hap_computation.ma".
          R. Kashima: "A proof of the Standization Theorem in λ-Calculus". Typescript note, (2000).
 *)
 inductive st: relation term ≝
-| st_vref: ∀s,M,i. lhap s M (#i) → st M (#i)
-| st_abst: ∀s,M,A1,A2. lhap s M (𝛌.A1) → st A1 A2 → st M (𝛌.A2)
-| st_appl: ∀s,M,B1,B2,A1,A2. lhap s M (@B1.A1) → st B1 B2 → st A1 A2 → st M (@B2.A2)
+| st_vref: ∀s,M,i. M ⓗ⇀*[s] #i → st M (#i)
+| st_abst: ∀s,M,A1,A2. M ⓗ⇀*[s] 𝛌.A1 → st A1 A2 → st M (𝛌.A2)
+| st_appl: ∀s,M,B1,B2,A1,A2. M ⓗ⇀*[s] @B1.A1 → st B1 B2 → st A1 A2 → st M (@B2.A2)
 .
 
+interpretation "'st' computation"
+    'Std M N = (st M N).
+
+notation "hvbox( M ⓢ⥤* break term 46 N )"
+   non associative with precedence 45
+   for @{ 'Std $M $N }.
+
+axiom st_refl: reflexive … st.
+
+axiom st_step_sn: ∀N1,N2. N1 ⓢ⥤* N2 → ∀s,M. M ⓗ⇀*[s] N1 → M ⓢ⥤* N2.
+
+axiom st_lift: liftable st.
+
+axiom st_inv_lift: deliftable_sn st.
+
+axiom st_dsubst: dsubstable st.