---

Step * 1 of Lemma bag-filter-no-repeats


1. T : Type
2. p : T ⟶ 𝔹
3. bs : T List
4. L@0 : T List
5. L@0 = bs ∈ (as,bs:T List//permutation(T;as;bs))
6. L@0 ∈ T List
7. bs ∈ T List
8. permutation(T;L@0;bs)
9. no_repeats(T;L@0)
⊢ ↓∃L@0:T List. ((L@0 = [x∈bs|p[x]] ∈ bag(T)) ∧ no_repeats(T;L@0))
BY
{ (D 0
   THEN Unfold `bag-filter` 0
   THEN With ⌜filter(λx.p[x];bs)⌝ (D 0)⋅
   THEN Auto
   THEN BLemma `no_repeats_filter`
   THEN Auto)⋅ }

---

Latex:

---

Latex:

1.  T  :  Type
2.  p  :  T  {}\mrightarrow{}  \mBbbB{}
3.  bs  :  T  List
4.  L@0  :  T  List
5.  L@0  =  bs
6.  L@0  \mmember{}  T  List
7.  bs  \mmember{}  T  List
8.  permutation(T;L@0;bs)
9.  no\_repeats(T;L@0)
\mvdash{}  \mdownarrow{}\mexists{}L@0:T  List.  ((L@0  =  [x\mmember{}bs|p[x]])  \mwedge{}  no\_repeats(T;L@0))


By

---

Latex:
(D  0
  THEN  Unfold  `bag-filter`  0
  THEN  With  \mkleeneopen{}filter(\mlambda{}x.p[x];bs)\mkleeneclose{}  (D  0)\mcdot{}
  THEN  Auto
  THEN  BLemma  `no\_repeats\_filter`
  THEN  Auto)\mcdot{}

---

Home Index