141def IsOrderCompatible (R : Recognizer C E) (R_cmp : ComparativeRecognizer C E') 142 (gt_events : Set E') (hp : InducesPreorder R_cmp gt_events) : Prop :=
proof body
Definition body.
143 ∀ c₁ c₂, Indistinguishable R c₁ c₂ → comparativeEquiv R_cmp gt_events c₁ c₂ 144 145/-- If R is order-compatible, the order descends to the quotient -/
used by (2)
From the project-wide theorem graph. These declarations reference this one in their body.