]> matita.cs.unibo.it Git - helm.git/blobdiff - matita/matita/contribs/lambdadelta/ground_2/steps/rtc.ma
first definition of cpm:
[helm.git] / matita / matita / contribs / lambdadelta / ground_2 / steps / rtc.ma
index 75960e4cbde202255edf4aee43b63bb6eec66a54..62228d229e21af156c36c43980e8956f51a4fd48 100644 (file)
@@ -22,28 +22,19 @@ include "ground_2/lib/arith.ma".
 
 record rtc: Type[0] ≝ {
    ri: nat; (* Note: inner r-steps *)
-   rh: nat; (* Note: head  r-steps *)
+   rs: nat; (* Note: spine r-steps *)
    ti: nat; (* Note: inner t-steps *)
-   th: nat  (* Note: head  t-steps *)
+   ts: nat  (* Note: spine t-steps *)
 }.
 
 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〉.
+   'Tuple ri rs ti ts = (mk_rtc ri rs ti ts).
 
 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)).