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).
+ 'Tuple ri rs ti ts = (mk_rtc ri rs ti ts).
interpretation "one structural step (rtc)"
'ZeroZero = (mk_rtc O O O O).