English
In the recursive step, if eval of prec cf cg at (a,k) yields ih, then eval of prec cf cg at (a, succ k) equals cg applied to (a, pair(k, ih)).
Русский
На рекурсивном шаге, если для prec cf cg на (a,k) получено ih, то для (a, succ k) равно cg( (a, (k, ih) ) ).
LaTeX
$$$\text{If } \mathrm{eval}((\\mathrm{prec}\\ cf\\ cg)) (\\mathrm{pair}(a,k)) = \\mathrm{Some}(i) \text{ then } \\mathrm{eval}((\\mathrm{prec}\\ cf\\ cg)) (\\mathrm{pair}(a,\\mathrm{pair}(k,i))) = \\mathrm{Some}(cg(\\mathrm{pair}(a,\\mathrm{pair}(k,i))))$$$
Lean4
/-- Helper lemma for the evaluation of `prec` in the recursive case. -/
theorem eval_prec_succ (cf cg : Code) (a k : ℕ) :
eval (prec cf cg) (Nat.pair a (Nat.succ k)) = do {
let ih ← eval (prec cf cg) (Nat.pair a k);
eval cg (Nat.pair a (Nat.pair k ih))
} :=
by
rw [eval, Nat.unpaired, Part.bind_eq_bind, Nat.unpair_pair]
simp
