English
length(think s) equals length(s) plus one.
Русский
length(think s) равняется length(s) плюс один.
LaTeX
$$$\forall s\,[h:\,\text{Terminates}(s)],\; \text{length}(\text{think } s) = \text{length } s + 1$$$
Lean4
@[simp]
theorem length_think (s : Computation α) [h : Terminates s] : length (think s) = length s + 1 :=
by
apply le_antisymm
· exact Nat.find_min' _ (Nat.find_spec ((terminates_def _).1 h))
· have : (Option.isSome ((think s).val (length (think s))) : Prop) :=
Nat.find_spec ((terminates_def _).1 s.think_terminates)
revert this; rcases length (think s) with - | n <;> intro this
· simp [think, Stream'.cons] at this
· apply Nat.succ_le_succ
apply Nat.find_min'
apply this
