---

Step * 1 1 2 of Lemma bag-no-repeats-le-bag-size


1. T : Type
2. u : T
3. v : T List
4. no_repeats(T;v)
5. ¬(u ∈ v)
6. ∀locs:T List. ((∀x:T. (x ↓∈ v ⇒ x ↓∈ locs)) ⇒ (||v|| ≤ ||locs||))
7. L : T List
8. ∀x:T. (x ↓∈ [u / v] ⇒ x ↓∈ L)
9. i : ℕ
10. i < ||L||
11. u = L[i] ∈ T
12. as : T List
13. bs : T List
14. L = (as @ [u] @ bs) ∈ (T List)
15. ||v|| ≤ ||as @ bs||
⊢ (||v|| + 1) ≤ ||L||
BY
{ (HypSubst' (-2) 0
   THEN RepeatFor 2 ((RWO "length_append" 0 THENA Auto))
   THEN Reduce 0
   THEN (RWO "length_append" (-1) THENA Auto)
   THEN Auto)⋅ }

---

Latex:

---

Latex:

1.  T  :  Type
2.  u  :  T
3.  v  :  T  List
4.  no\_repeats(T;v)
5.  \mneg{}(u  \mmember{}  v)
6.  \mforall{}locs:T  List.  ((\mforall{}x:T.  (x  \mdownarrow{}\mmember{}  v  {}\mRightarrow{}  x  \mdownarrow{}\mmember{}  locs))  {}\mRightarrow{}  (||v||  \mleq{}  ||locs||))
7.  L  :  T  List
8.  \mforall{}x:T.  (x  \mdownarrow{}\mmember{}  [u  /  v]  {}\mRightarrow{}  x  \mdownarrow{}\mmember{}  L)
9.  i  :  \mBbbN{}
10.  i  <  ||L||
11.  u  =  L[i]
12.  as  :  T  List
13.  bs  :  T  List
14.  L  =  (as  @  [u]  @  bs)
15.  ||v||  \mleq{}  ||as  @  bs||
\mvdash{}  (||v||  +  1)  \mleq{}  ||L||


By

---

Latex:
(HypSubst'  (-2)  0
  THEN  RepeatFor  2  ((RWO  "length\_append"  0  THENA  Auto))
  THEN  Reduce  0
  THEN  (RWO  "length\_append"  (-1)  THENA  Auto)
  THEN  Auto)\mcdot{}

---

Home Index