English
complEDSRec is a recursion principle for the complement sequence on natural numbers, built from complEDSRec' by passing appropriate even/odd step rules.
Русский
complEDSRec — принцип рекурсии для последовательности дополняющих элементов на натуральных числах, получаемый из complEDSRec' через соответствующие правила чётного и нечётного шага.
LaTeX
$$$\text{complEDSRec}\;\{P:\mathbb{N}\to \text{Sort}\} \; P(0) \; P(1) \; (\forall m\, P(m+1) \to P(m+2) \to P(2(m+1))) \; (\forall m\, P(m+1) \to P(m+2) \to P(m+3) \to P(m+4) \to P(2(m+2)+1)) \to \forall n\; P(n)$$$
Lean4
/-- Recursion principle for the complement sequence for a normalised EDS: if we have
* `P 0`, `P 1`,
* for all `m : ℕ` we can prove `P (2 * (m + 3))` from `P (m + 1)`, `P (m + 2)`, `P (m + 3)`,
`P (m + 4)`, and `P (m + 5)`, and
* for all `m : ℕ` we can prove `P (2 * (m + 2) + 1)` from `P (m + 1)`, `P (m + 2)`, `P (m + 3)`,
and `P (m + 4)`,
then we have `P n` for all `n : ℕ`. -/
@[elab_as_elim]
noncomputable def complEDSRec {P : ℕ → Sort u} (zero : P 0) (one : P 1) (even : ∀ m : ℕ, P (m + 1) → P (2 * (m + 1)))
(odd : ∀ m : ℕ, P (m + 1) → P (m + 2) → P (2 * (m + 1) + 1)) (n : ℕ) : P n :=
complEDSRec' zero one (fun _ ih => even _ <| ih _ <| by linarith only)
(fun _ ih => odd _ (ih _ <| by linarith only) <| ih _ <| by linarith only) n
