English
IsPath from s to u over concatenation x ++ y holds iff there exists an intermediate state t such that IsPath from s to t over x and t to u over y.
Русский
IsPath от s к u через x ++ y эквивалентно существованию пакета t, для которого IsPath(s,t,x) и IsPath(t,u,y).
LaTeX
$$M.IsPath s u (x ++ y) \\Leftrightarrow \exists t, M.IsPath s t x \wedge M.IsPath t u y$$
Lean4
theorem isPath_append {x y : List (Option α)} : M.IsPath s u (x ++ y) ↔ ∃ t, M.IsPath s t x ∧ M.IsPath t u y
where
mp := by
induction x generalizing s with
| nil =>
rw [List.nil_append]
tauto
| cons x a ih =>
rintro (_ | ⟨t, _, _, _, _, _, h⟩)
apply ih at h
tauto
mpr := by
intro ⟨t, hx, _⟩
induction x generalizing s <;> cases hx <;> tauto
