English
The size measure strictly decreases under a step when r ≠ 0, ensuring termination: Size(u.step) < Size(u).
Русский
При шаге для r ≠ 0 размерность строго уменьшается: Size(u.step) < Size(u).
LaTeX
$$$u.r \\neq 0 \\Rightarrow\\ SizeOf.sizeOf(u.step) < SizeOf.sizeOf(u)$$$
Lean4
/-- We will apply the above step recursively. The following result
is used to ensure that the process terminates. -/
theorem step_wf (hr : u.r ≠ 0) : SizeOf.sizeOf u.step < SizeOf.sizeOf u :=
by
change u.r - 1 < u.bp
have h₀ : u.r - 1 + 1 = u.r := Nat.succ_pred_eq_of_pos (Nat.pos_of_ne_zero hr)
have h₁ : u.r < u.bp + 1 := Nat.mod_lt (u.ap + 1) u.bp.succ_pos
rw [← h₀] at h₁
exact lt_of_succ_lt_succ h₁
