---

Step * of Lemma strict-bag-function_wf

∀[L:Type List]. ∀[B:Type]. ∀[G:tuple-type(map(λT.bag(T);L)) ⟶ bag(B)]. ∀[S:ℕ||L|| List].
  (strict-bag-function(G;L;B;S) ∈ ℙ)
BY
{ ProveWfLemma }

1
1. L : Type List
2. B : Type
3. G : tuple-type(map(λT.bag(T);L)) ⟶ bag(B)
4. S : ℕ||L|| List
5. x : tuple-type(map(λT.bag(T);L))@i
6. ∀x:ℕ||L||. ((x ∈ S) ∈ Type)
7. i : ℕ||L||@i
8. (i ∈ S)@i
⊢ x.i ∈ bag(L[i])

---

Latex:

---

Latex:
\mforall{}[L:Type  List].  \mforall{}[B:Type].  \mforall{}[G:tuple-type(map(\mlambda{}T.bag(T);L))  {}\mrightarrow{}  bag(B)].  \mforall{}[S:\mBbbN{}||L||  List].
    (strict-bag-function(G;L;B;S)  \mmember{}  \mBbbP{})


By

---

Latex:
ProveWfLemma

---

Home Index