---

Step * 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
⊢ (||v|| + 1) ≤ ||L||
BY
{ ((Assert ⌜∃as,bs:T List. (L = (as @ [u] @ bs) ∈ (T List))⌝⋅
    THENA ((HypSubst' (-1) 0 THENA Auto) THEN BLemma `list_decomp_member` THEN Auto)
    )
   THEN ExRepD⋅
   THEN (InstHyp [⌜as @ bs⌝] (-9)⋅ THENA 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
⊢ x ↓∈ as @ bs

2
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||

---

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]
\mvdash{}  (||v||  +  1)  \mleq{}  ||L||


By

---

Latex:
((Assert  \mkleeneopen{}\mexists{}as,bs:T  List.  (L  =  (as  @  [u]  @  bs))\mkleeneclose{}\mcdot{}
    THENA  ((HypSubst'  (-1)  0  THENA  Auto)  THEN  BLemma  `list\_decomp\_member`  THEN  Auto)
    )
  THEN  ExRepD\mcdot{}
  THEN  (InstHyp  [\mkleeneopen{}as  @  bs\mkleeneclose{}]  (-9)\mcdot{}  THENA  Auto))

---

Home Index