English
normEDSRec' is a strong recursion principle for a normalised elliptic divisibility sequence: if a predicate P on natural numbers is true for 0,1,2,3,4 and if for every m, P(2(m+3)) follows from P(k) for k < 2(m+3) and P(2(m+2)+1) follows from P(k) for k < 2(m+2)+1, then P(n) holds for all n.
Русский
normEDSRec' задаёт сильный принцип рекурсии для нормализованной эллиптической последовательности делимости: если для естественных чисел справедливо P(0)=P(1)=P(2)=P(3)=P(4) и для каждого m выполняется, что P(2(m+3)) следует из значений P(k) при k < 2(m+3), а P(2(m+2)+1) следует из значений P(k) при k < 2(m+2)+1, то P(n) верно для всех n.
LaTeX
$$$\exists P:\mathbb{N}\to \text{Sort},\ P(0),P(1),P(2),P(3),P(4)\ \wedge\ \forall m\in\mathbb{N},\big(\forall k<2(m+3),P(k)\Rightarrow P(2(m+3))\big) \wedge \forall m\big(\forall k<2(m+2)+1, P(k)\Rightarrow P(2(m+2)+1)\big) \Rightarrow \forall n\ P(n)$$$
Lean4
/-- Strong recursion principle for a normalised EDS: if we have
* `P 0`, `P 1`, `P 2`, `P 3`, and `P 4`,
* for all `m : ℕ` we can prove `P (2 * (m + 3))` from `P k` for all `k < 2 * (m + 3)`, and
* for all `m : ℕ` we can prove `P (2 * (m + 2) + 1)` from `P k` for all `k < 2 * (m + 2) + 1`,
then we have `P n` for all `n : ℕ`.
-/
@[elab_as_elim]
noncomputable def normEDSRec' {P : ℕ → Sort u} (zero : P 0) (one : P 1) (two : P 2) (three : P 3) (four : P 4)
(even : ∀ m : ℕ, (∀ k < 2 * (m + 3), P k) → P (2 * (m + 3)))
(odd : ∀ m : ℕ, (∀ k < 2 * (m + 2) + 1, P k) → P (2 * (m + 2) + 1)) (n : ℕ) : P n :=
n.evenOddStrongRec (by rintro (_ | _ | _ | _) h; exacts [zero, two, four, even _ h])
(by rintro (_ | _ | _) h; exacts [one, three, odd _ h])
