pith. machine review for the scientific record. sign in
theorem proved term proof

comparativeEquiv_trans

show as:
view Lean formalization →

No prose has been written for this declaration yet. The Lean source and graph data below render without it.

generate prose now

formal statement (Lean)

 130theorem comparativeEquiv_trans (R : ComparativeRecognizer C E) (gt_events : Set E)
 131    (hp : InducesPreorder R gt_events)
 132    {c₁ c₂ c₃ : C} (h₁ : comparativeEquiv R gt_events c₁ c₂)
 133    (h₂ : comparativeEquiv R gt_events c₂ c₃) :
 134    comparativeEquiv R gt_events c₁ c₃ :=

proof body

Term-mode proof.

 135  ⟨hp.trans c₁ c₂ c₃ h₁.1 h₂.1, hp.trans c₃ c₂ c₁ h₂.2 h₁.2⟩
 136
 137/-! ## Order-Respecting Recognizers -/
 138
 139/-- A standard recognizer R is compatible with a comparative recognizer R_cmp if
 140    indistinguishable configurations are also comparatively equivalent -/

depends on (12)

Lean names referenced from this declaration's body.