---

Step * 1 2 2 1 1 of Lemma bag-decomp_wf


1. T : Type
2. v : T List
⊢ ∀f:ℕ||v|| ⟶ ℕ||v||
    (Inj(ℕ||v||;ℕ||v||;f)
    ⇒ (map(λn.remove-nth(n;(v o f));upto(||v||)) = map(λn.remove-nth(n;v);(upto(||v||) o f)) ∈ ((T × bag(T)) List)))
BY
{ (RenameVar `b1' (-1) THEN Auto) }

1
1. T : Type
2. b1 : T List
3. f : ℕ||b1|| ⟶ ℕ||b1||
4. Inj(ℕ||b1||;ℕ||b1||;f)
⊢ map(λn.remove-nth(n;(b1 o f));upto(||b1||)) = map(λn.remove-nth(n;b1);(upto(||b1||) o f)) ∈ ((T × bag(T)) List)

---

Latex:

---

Latex:

1.  T  :  Type
2.  v  :  T  List
\mvdash{}  \mforall{}f:\mBbbN{}||v||  {}\mrightarrow{}  \mBbbN{}||v||
        (Inj(\mBbbN{}||v||;\mBbbN{}||v||;f)
        {}\mRightarrow{}  (map(\mlambda{}n.remove-nth(n;(v  o  f));upto(||v||))  =  map(\mlambda{}n.remove-nth(n;v);(upto(||v||)  o  f))))


By

---

Latex:
(RenameVar  `b1'  (-1)  THEN  Auto)

---

Home Index