Documentation

Foundation.Modal.Kripke.GL.MDP

@[reducible, inline]
Equations
  • One or more equations did not get rendered due to their size.
Equations
Equations
theorem LO.Modal.GL.Kripke.MDPCounterexampleFrame.through_original_root {F₁ F₂ : Kripke.FiniteTransitiveTree} {x : (MDPCounterexampleFrame F₁ F₂).World} (h : (MDPCounterexampleFrame F₁ F₂).root x) :
(x = (Sum.inr Sum.inl) F₁.root Sum.inr (Sum.inl F₁.root) x) x = (Sum.inr Sum.inr) F₂.root Sum.inr (Sum.inr F₂.root) x
@[reducible, inline]
Equations
  • One or more equations did not get rendered due to their size.