(* *)
(**************************************************************************)
-include "ground/notation/relations/ist_2.ma".
+include "ground/notation/relations/predicate_t_2.ma".
include "ground/counters/rtc.ma".
(* T-TRANSITION COUNTERS ****************************************************)
λts,c. 〈𝟎,𝟎,𝟎,ts〉 = c.
interpretation
- "t-transition counters (rtc)"
- 'IsT ts c = (rtc_ist ts c).
+ "construction (t-transition counters)"
+ 'PredicateT ts c = (rtc_ist ts c).
(* Basic constructions ******************************************************)