English
Bisimulation for M on P: existence of decompositions linking the heads via pathDestLeft/Right such that the right-hand sides match recursively; this characterizes when two states are equal by analyzing their immediate structure and subtrees.
Русский
Бимильная характеристика M: существование разложений, связывающих головы через pathDestLeft/Right, чтобы правая часть соответствовала рекурсивному соответствию поддеревьев; описывает равенство состояний через структуру и поддеревья.
LaTeX
$$$\forall {n} (P : MvPFunctor (n+1)) {\alpha} {a₁} {f₁} {a' } {f' } {f₁'} , (e₁ : M.dest P ⟨a₁, f₁⟩ = ⟨a', splitFun f' f₁'⟩) : \exists g₁', e₁', f' = M.pathDestLeft P e₁' f₁ \land f₁' = (\lambda x : (last P).B a' => ⟨g₁' x, M.pathDestRight P e₁' f₁ x⟩)$$$
Lean4
/-- Specialized destructor on `WPath` -/
def wPathDestRight {α : TypeVec n} {a : P.A} {f : P.last.B a → P.last.W} (h : P.WPath ⟨a, f⟩ ⟹ α) :
∀ j : P.last.B a, P.WPath (f j) ⟹ α := fun j i c => h i (WPath.child a f i j c)
