---

Step * 1 of Lemma strict-bag-function_wf


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])
BY
{ ((DoSubsume THEN Auto) THEN (RWO "length-map select-map" 0 THENM Reduce 0) THEN Auto)⋅ }

---

Latex:

---

Latex:

1.  L  :  Type  List
2.  B  :  Type
3.  G  :  tuple-type(map(\mlambda{}T.bag(T);L))  {}\mrightarrow{}  bag(B)
4.  S  :  \mBbbN{}||L||  List
5.  x  :  tuple-type(map(\mlambda{}T.bag(T);L))@i
6.  \mforall{}x:\mBbbN{}||L||.  ((x  \mmember{}  S)  \mmember{}  Type)
7.  i  :  \mBbbN{}||L||@i
8.  (i  \mmember{}  S)@i
\mvdash{}  x.i  \mmember{}  bag(L[i])


By

---

Latex:
((DoSubsume  THEN  Auto)  THEN  (RWO  "length-map  select-map"  0  THENM  Reduce  0)  THEN  Auto)\mcdot{}

---

Home Index