X-Git-Url: http://matita.cs.unibo.it/gitweb/?a=blobdiff_plain;f=matita%2Fmatita%2Fcontribs%2Flambdadelta%2Fground_2%2Fsteps%2Frtc.ma;fp=matita%2Fmatita%2Fcontribs%2Flambdadelta%2Fground_2%2Fsteps%2Frtc.ma;h=494650d04d9dff70e6bff2054b0aa538d2613ef5;hb=c3904c007394068ed823575e3be3d73a9ad92cce;hp=75960e4cbde202255edf4aee43b63bb6eec66a54;hpb=fb246e36bb7d2731016e686e2091f6a3704bb362;p=helm.git

diff --git a/matita/matita/contribs/lambdadelta/ground_2/steps/rtc.ma b/matita/matita/contribs/lambdadelta/ground_2/steps/rtc.ma
index 75960e4cb..494650d04 100644
--- a/matita/matita/contribs/lambdadelta/ground_2/steps/rtc.ma
+++ b/matita/matita/contribs/lambdadelta/ground_2/steps/rtc.ma
@@ -30,20 +30,11 @@ record rtc: Type[0] ≝ {
 interpretation "constructor (rtc)"
    'Tuple ri rh ti th = (mk_rtc ri rh ti th).
 
-(* Note: for one structural step *)
-definition OO: rtc ≝ 〈0, 0, 0, 0〉.
-
 interpretation "one structural step (rtc)"
-   'ZeroZero = (OO).
-
-(* Note: for one r-step *)
-definition UO: rtc ≝ 〈0, 1, 0, 0〉.
+   'ZeroZero = (mk_rtc O O O O).
 
 interpretation "one r-step (rtc)"
-   'OneZero = (UO).
-
-(* Note: for one t-step *)
-definition OU: rtc ≝ 〈0, 0, 0, 1〉.
+   'OneZero = (mk_rtc O (S O) O O).
 
 interpretation "one t-step (rtc)"
-   'ZeroOne = (OU).
+   'ZeroOne = (mk_rtc O O O (S O)).