---

Step * 1 1 1 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. x : T
16. x ↓∈ v
⊢ x ↓∈ as @ bs
BY
{ (Assert ⌜¬(x = u ∈ T)⌝⋅ THENA ((D 0 THENA Auto) THEN FLemma `not-list-member-not-bag-member` [-13] THEN Auto)) }

1
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. x : T
16. x ↓∈ v
17. ¬(x = u ∈ T)
⊢ x ↓∈ as @ bs

---

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.  x  :  T
16.  x  \mdownarrow{}\mmember{}  v
\mvdash{}  x  \mdownarrow{}\mmember{}  as  @  bs


By

---

Latex:
(Assert  \mkleeneopen{}\mneg{}(x  =  u)\mkleeneclose{}\mcdot{}
  THENA  ((D  0  THENA  Auto)  THEN  FLemma  `not-list-member-not-bag-member`  [-13]  THEN  Auto)
  )

---

Home Index