Lemma [efr-O92R]
  1. Sliding equivalence implies behavioural equivalence
  2. For charts over a deterministic base, sliding equivalence and behavioural equivalence coincide
  3. Given a faithful Markov functor \mathcal {C} \to \mathcal {C}' and a faithful map of modules \mathcal {D} \to \mathcal {D}' over it, the induced map on precharts in well-defined with respect to sliding equivalence, and injective with respect to behavioural equivalence, in the sense that precharts which become behavioural equivalent in the image are already behavioural equivalent, but not necessarily the other way around