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