---

Step * of Lemma sum-partial-has-value

∀[n:ℕ]. ∀[f:ℕn ⟶ partial(ℕ)].  ∀i:ℕn. (f[i])↓ supposing (Σ(f[x] | x < n))↓
BY
{ TACTIC:(InstLemma `uniform-comp-nat-induction` [⌜λ2n.∀[f:ℕn ⟶ partial(ℕ)]
                                                         ∀i:ℕn. (f[i])↓ supposing (Σ(f[x] | x < n))↓⌝]⋅
THENM Trivial
) }

1
.....wf..... 
λn.∀[f:ℕn ⟶ partial(ℕ)]. ∀i:ℕn. (f[i])↓ supposing (Σ(f[x] | x < n))↓ ∈ ℕ ⟶ ℙ

2
.....antecedent..... 
∀[n:ℕ]
  ((∀[m:ℕn]. ∀[f:ℕm ⟶ partial(ℕ)].  ∀i:ℕm. (f[i])↓ supposing (Σ(f[x] | x < m))↓)
  ⇒ (∀[f:ℕn ⟶ partial(ℕ)]. ∀i:ℕn. (f[i])↓ supposing (Σ(f[x] | x < n))↓))

---

Latex:

---

Latex:
\mforall{}[n:\mBbbN{}].  \mforall{}[f:\mBbbN{}n  {}\mrightarrow{}  partial(\mBbbN{})].    \mforall{}i:\mBbbN{}n.  (f[i])\mdownarrow{}  supposing  (\mSigma{}(f[x]  |  x  <  n))\mdownarrow{}


By

---

Latex:
TACTIC:(InstLemma  `uniform-comp-nat-induction`  [\mkleeneopen{}\mlambda{}\msubtwo{}n.\mforall{}[f:\mBbbN{}n  {}\mrightarrow{}  partial(\mBbbN{})]
                                                                                                              \mforall{}i:\mBbbN{}n.  (f[i])\mdownarrow{}  supposing  (\mSigma{}(f[x]  |  x  <  n))\mdownarrow{}\mkleeneclose{}]
                \mcdot{}
THENM  Trivial
)

---

Home Index