X-Git-Url: http://matita.cs.unibo.it/gitweb/?a=blobdiff_plain;ds=sidebyside;f=matita%2Fmatita%2Fcontribs%2Flambda%2Fst_computation.ma;fp=matita%2Fmatita%2Fcontribs%2Flambda%2Fst_computation.ma;h=028cd8a41bfc3ae80657c7c21e7dfc4542fadd56;hb=23e75ebc00553e178e090ca1373ac075ee650a60;hp=c9f9aa9477f6dc1be2369b003948b2fe9aaf6704;hpb=178820be7648a60af17837727e51fd1f3f2791db;p=helm.git

diff --git a/matita/matita/contribs/lambda/st_computation.ma b/matita/matita/contribs/lambda/st_computation.ma
index c9f9aa947..028cd8a41 100644
--- 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.