---

Step * 1 2 2 1 of Lemma bag-decomp_wf


1. T : Type
2. bs : Base
3. bs ∈ T List
4. f : ℕ||bs|| ⟶ ℕ||bs||
5. Inj(ℕ||bs||;ℕ||bs||;f)
⊢ map(λn.remove-nth(n;(bs o f));upto(||bs||)) = map(λn.remove-nth(n;bs);(upto(||bs||) o f)) ∈ ((T × bag(T)) List)
BY
{ (RepeatFor 2 (MoveToConcl (-1)) THEN (GenConclTerm ⌜bs⌝⋅ THENA Auto) THEN All Thin) }

1
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)))

---

Latex:

---

Latex:

1.  T  :  Type
2.  bs  :  Base
3.  bs  \mmember{}  T  List
4.  f  :  \mBbbN{}||bs||  {}\mrightarrow{}  \mBbbN{}||bs||
5.  Inj(\mBbbN{}||bs||;\mBbbN{}||bs||;f)
\mvdash{}  map(\mlambda{}n.remove-nth(n;(bs  o  f));upto(||bs||))  =  map(\mlambda{}n.remove-nth(n;bs);(upto(||bs||)  o  f))


By

---

Latex:
(RepeatFor  2  (MoveToConcl  (-1))  THEN  (GenConclTerm  \mkleeneopen{}bs\mkleeneclose{}\mcdot{}  THENA  Auto)  THEN  All  Thin)

---

Home Index