English
Let lLim be a succ-limit. For motive and o, the value at the successor index equals H2 o applied to the recursive result at o.
Русский
Пусть lLim — succ-ограничение. Для motive и o значение на индексе-предшественнике равно H2 o, применённому к рекурсивному результату на o.
LaTeX
$$$$ \forall l\ (lLim : IsSuccLimit l) \ {motive} (o\ H_1 H_2 H_3):\; \mathrm{boundedLimitRecOn}(l, lLim, motive)\langle\mathrm{succ} o.1, lLim.succ\_lt o.2\rangle H_1 H_2 H_3 = H_2\ o\ (\mathrm{boundedLimitRecOn}(l, lLim, motive, o, H_1, H_2, H_3)) \,$$$
Lean4
@[simp]
theorem boundedLimitRec_succ {l} (lLim : IsSuccLimit l) {motive} (o H₁ H₂ H₃) :
@boundedLimitRecOn l lLim motive ⟨succ o.1, lLim.succ_lt o.2⟩ H₁ H₂ H₃ =
H₂ o (@boundedLimitRecOn l lLim motive o H₁ H₂ H₃) :=
by
rw [boundedLimitRecOn, limitRecOn_succ]
rfl
