---

Step * 1 of Lemma sum-partial-has-value

.....wf..... 
λn.∀[f:ℕn ⟶ partial(ℕ)]. ∀i:ℕn. (f[i])↓ supposing (Σ(f[x] | x < n))↓ ∈ ℕ ⟶ ℙ
BY
{ TACTIC:RepeatFor 2 ((MemCD THENA Auto)) }

1
.....subterm..... T:t
1:n
1. n : ℕ@i
⊢ ℕn ⟶ partial(ℕ) ∈ Type

2
.....subterm..... T:t
2:n
1. n : ℕ@i
2. f : ℕn ⟶ partial(ℕ)@i
⊢ ∀i:ℕn. (f[i])↓ supposing (Σ(f[x] | x < n))↓ ∈ ℙ

---

Latex:

---

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


By

---

Latex:
TACTIC:RepeatFor  2  ((MemCD  THENA  Auto))

---

Home Index