---

Step * 1 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
17. ¬(x = u ∈ T)
⊢ x ↓∈ as @ bs
BY
{ ((InstHyp [⌜x⌝] (-10)⋅ THENA (Auto THEN BagMemberD 0 THEN D 0 THEN Auto))⋅
   THEN (RWO "-5" (-1) THENA (Auto THEN RemoveLabel THEN HypSubst' (-1) 0 THEN Auto))
   THEN BagMemberD 0
   THEN RepeatFor 2 ((BagMemberD (-1)
                      THEN D (-1)
                      THEN (Unhide THENA Auto)
                      THEN D (-1)
                      THEN Try (Complete ((D 0 THEN Auto)))))
   THEN Assert ⌜False⌝⋅
   THEN Auto
   THEN BagMemberD (-1)
   THEN D (-1)
   THEN (Unhide THENA Auto)
   THEN D (-1)
   THEN Auto
   THEN BagMemberD (-1)
   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.  x  :  T
16.  x  \mdownarrow{}\mmember{}  v
17.  \mneg{}(x  =  u)
\mvdash{}  x  \mdownarrow{}\mmember{}  as  @  bs


By

---

Latex:
((InstHyp  [\mkleeneopen{}x\mkleeneclose{}]  (-10)\mcdot{}  THENA  (Auto  THEN  BagMemberD  0  THEN  D  0  THEN  Auto))\mcdot{}
  THEN  (RWO  "-5"  (-1)  THENA  (Auto  THEN  RemoveLabel  THEN  HypSubst'  (-1)  0  THEN  Auto))
  THEN  BagMemberD  0
  THEN  RepeatFor  2  ((BagMemberD  (-1)
                                        THEN  D  (-1)
                                        THEN  (Unhide  THENA  Auto)
                                        THEN  D  (-1)
                                        THEN  Try  (Complete  ((D  0  THEN  Auto)))))
  THEN  Assert  \mkleeneopen{}False\mkleeneclose{}\mcdot{}
  THEN  Auto
  THEN  BagMemberD  (-1)
  THEN  D  (-1)
  THEN  (Unhide  THENA  Auto)
  THEN  D  (-1)
  THEN  Auto
  THEN  BagMemberD  (-1)
  THEN  Auto)

---

Home Index