English
Bisimilarity over a sum of Computation objects: a relation defined by left equality, right relation, or false otherwise.
Русский
Бисимиляция над суммой вычислений: отношение задаётся равенством левых элементов, отношением справа, либо ложью в противном случае.
LaTeX
$$$\\mathrm{BisimO}_R(a,b) = \\begin{cases} a=a', & \\text{if } a,b \\text{ are in the left component}, \\\\ R\\ s\\ s', & \\text{if } s,s' \\ are in the right component, \\\\ \\text{False}, & \\text{otherwise}. \\end{cases}$$$
Lean4
/-- Bisimilarity over a sum of `Computation`s -/
def BisimO : α ⊕ (Computation α) → α ⊕ (Computation α) → Prop
| Sum.inl a, Sum.inl a' => a = a'
| Sum.inr s, Sum.inr s' => R s s'
| _, _ => False
