---

Step * 1 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)
7. ∀i:ℕ||L||. (f[L[i]])↓
⊢ (f[x])↓
BY
{ TACTIC:(RepeatFor 2 (D -2) THEN (InstHyp [⌜i⌝] (-1)⋅ 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. i : ℕ
7. i < ||L||
8. x = L[i] ∈ T
9. ∀i:ℕ||L||. (f[L[i]])↓
10. (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)
7.  \mforall{}i:\mBbbN{}||L||.  (f[L[i]])\mdownarrow{}
\mvdash{}  (f[x])\mdownarrow{}


By

---

Latex:
TACTIC:(RepeatFor  2  (D  -2)  THEN  (InstHyp  [\mkleeneopen{}i\mkleeneclose{}]  (-1)\mcdot{}  THENA  Auto))

---

Home Index