---

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


1. T : Type
2. L : T List
3. f : T ⟶ partial(ℕ)
4. (Σ(f[L[i]] | i < ||L||))↓
5. x : T@i
6. (x ∈ L)
⊢ (f[x])↓
BY
{ TACTIC:(InstLemma `sum-partial-has-value` [⌜||L||⌝;⌜λ2i.f[L[i]]⌝]⋅ THENA Auto) }

1
1. T : Type
2. L : T List
3. f : T ⟶ partial(ℕ)
4. (Σ(f[L[i]] | i < ||L||))↓
5. x : T@i
6. (x ∈ L)
7. ∀i:ℕ||L||. (f[L[i]])↓
⊢ (f[x])↓

---

Latex:

---

Latex:

1.  T  :  Type
2.  L  :  T  List
3.  f  :  T  {}\mrightarrow{}  partial(\mBbbN{})
4.  (\mSigma{}(f[L[i]]  |  i  <  ||L||))\mdownarrow{}
5.  x  :  T@i
6.  (x  \mmember{}  L)
\mvdash{}  (f[x])\mdownarrow{}


By

---

Latex:
TACTIC:(InstLemma  `sum-partial-has-value`  [\mkleeneopen{}||L||\mkleeneclose{};\mkleeneopen{}\mlambda{}\msubtwo{}i.f[L[i]]\mkleeneclose{}]\mcdot{}  THENA  Auto)

---

Home Index