---

Step * 1 of Lemma sub-bag-list-if-bag-no-repeats-sq

.....antecedent..... 
1. A : Type
2. u : A
3. v : A List
4. ∀bs:A List. (no_repeats(A;v) ⇒ (∀x∈v.(x ∈ bs)) ⇒ (↓sub-bag(A;v;bs)))
5. bs : A List
6. no_repeats(A;v)
7. ¬(u ∈ v)
8. l1 : A List
9. l2 : A List
10. bs = (l1 @ [u] @ l2) ∈ (A List)
11. (∀x∈v.(x ∈ bs))
⊢ (∀x∈v.(x ∈ l1 @ l2))
BY
{ ((All(RWO "l_all_iff") THENA Auto)
   THEN RepeatFor 2 (ParallelLast)
   THEN (HypSubst (-5) (-1) THENA Auto)
   THEN Repeat (((RW ListC (-1) THENA Auto) THEN Try (DProdsAndUnions)))
   THEN (RW ListC 0 THEN Auto)
   THEN Assert ⌜False⌝⋅
   THEN Auto)⋅ }

---

Latex:

---

Latex:
.....antecedent..... 
1.  A  :  Type
2.  u  :  A
3.  v  :  A  List
4.  \mforall{}bs:A  List.  (no\_repeats(A;v)  {}\mRightarrow{}  (\mforall{}x\mmember{}v.(x  \mmember{}  bs))  {}\mRightarrow{}  (\mdownarrow{}sub-bag(A;v;bs)))
5.  bs  :  A  List
6.  no\_repeats(A;v)
7.  \mneg{}(u  \mmember{}  v)
8.  l1  :  A  List
9.  l2  :  A  List
10.  bs  =  (l1  @  [u]  @  l2)
11.  (\mforall{}x\mmember{}v.(x  \mmember{}  bs))
\mvdash{}  (\mforall{}x\mmember{}v.(x  \mmember{}  l1  @  l2))


By

---

Latex:
((All(RWO  "l\_all\_iff")  THENA  Auto)
  THEN  RepeatFor  2  (ParallelLast)
  THEN  (HypSubst  (-5)  (-1)  THENA  Auto)
  THEN  Repeat  (((RW  ListC  (-1)  THENA  Auto)  THEN  Try  (DProdsAndUnions)))
  THEN  (RW  ListC  0  THEN  Auto)
  THEN  Assert  \mkleeneopen{}False\mkleeneclose{}\mcdot{}
  THEN  Auto)\mcdot{}

---

Home Index