include "ground/notation/functions/zerozero_0.ma".
include "ground/notation/functions/zeroone_0.ma".
include "ground/notation/functions/onezero_0.ma".
-include "ground/insert_eq/insert_eq_1.ma".
+include "ground/generated/insert_eq_1.ma".
include "ground/arith/nat.ma".
(* RT-TRANSITION COUNTERS ***************************************************)
}.
interpretation
- "constructor (rtc)"
+ "construction (rt-transition counters)"
'Tuple ri rs ti ts = (mk_rtc ri rs ti ts).
interpretation
- "one structural step (rtc)"
+ "one structural step (rt-transition counters)"
'ZeroZero = (mk_rtc nzero nzero nzero nzero).
interpretation
- "one r-step (rtc)"
+ "one r-step (rt-transition counters)"
'OneZero = (mk_rtc nzero (ninj punit) nzero nzero).
interpretation
- "one t-step (rtc)"
+ "one t-step (rt-transition counters)"
'ZeroOne = (mk_rtc nzero nzero nzero (ninj punit)).
definition rtc_eq_f: relation rtc ≝ λc1,c2. ⊤.
(* Basic constructions ******************************************************)
-lemma rtc_eq_t_refl: reflexive … rtc_eq_t.
+lemma rtc_eq_t_refl:
+ reflexive … rtc_eq_t.
* // qed.
(* Basic inversions *********************************************************)