English
If b is in eval f a, then no nontrivial one-step reachability from b exists; equivalently, for every c, not Reaches₁ f b c.
Русский
Если b находится в eval f a, то из b далее нельзя сделать нетривиального перехода; для любого c верно, что не Reaches₁ f b c.
LaTeX
$$$b \\in \\mathrm{eval}\\ f\\ a \\Rightarrow \\forall c, \\neg \\mathrm{Reaches}_1\\ f\\ b\\ c$$$
Lean4
theorem eval_maximal₁ {σ} {f : σ → Option σ} {a b} (h : b ∈ eval f a) (c) : ¬Reaches₁ f b c
| bc => by
let ⟨_, b0⟩ := mem_eval.1 h
let ⟨b', h', _⟩ := TransGen.head'_iff.1 bc
cases b0.symm.trans h'