---

Step * 1 of Lemma bag-map-trivial


1. A : Type
2. f : A ⟶ A
3. ∀x:A. ((f x) = x ∈ A)
4. as : A List
5. bs : A List
6. permutation(A;as;bs)
7. as = bs ∈ bag(A)
⊢ bag-map(f;bs) = bs ∈ bag(A)
BY
{ (SubsumeC ⌜A List⌝⋅ THEN RepUR ``bag-map`` 0 THEN ThinVar `as' THEN Auto) }

---

Latex:

---

Latex:

1.  A  :  Type
2.  f  :  A  {}\mrightarrow{}  A
3.  \mforall{}x:A.  ((f  x)  =  x)
4.  as  :  A  List
5.  bs  :  A  List
6.  permutation(A;as;bs)
7.  as  =  bs
\mvdash{}  bag-map(f;bs)  =  bs


By

---

Latex:
(SubsumeC  \mkleeneopen{}A  List\mkleeneclose{}\mcdot{}  THEN  RepUR  ``bag-map``  0  THEN  ThinVar  `as'  THEN  Auto)

---

Home Index