eval_eq_rfindOpt — Mathlib

English

The evaluation scheme evaln is primitive recursive in its arguments, as described above.

Русский

Схема вычисления evaln является примитивно вычислимой по своим аргументам, как описано выше.

LaTeX

$$$\\mathrm{Primrec}\\;\\mathrm{evaln}$$$

Lean4

theorem eval_eq_rfindOpt (c n) : eval c n = Nat.rfindOpt fun k => evaln k c n :=
  Part.ext fun x => by
    refine evaln_complete.trans (Nat.rfindOpt_mono ?_).symm
    intro a m n hl; apply evaln_mono hl

Похожие утверждения