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