---

Step * 1 1 of Lemma list-decomp-no_repeats


1. T : Type
2. l1 : T List
3. l2 : T List
4. l3 : T List
5. l4 : T List
6. x : T
7. no_repeats(T;(l1 @ [x]) @ l2)
8. ((l1 @ [x]) @ l2) = ((l3 @ [x]) @ l4) ∈ (T List)
9. ((||l1|| + 1) + ||l2||) = ((||l3|| + 1) + ||l4||) ∈ ℤ
10. ∀i:ℕ(||l1|| + 1) + ||l2||. ((l1 @ [x]) @ l2[i] = (l3 @ [x]) @ l4[i] ∈ T)
⊢ ||l1|| = ||l3|| ∈ ℤ
BY
{ (SupposeNot
   THEN Assert ⌜False⌝⋅
   THEN Auto
   THEN (InstHyp [⌜||l1||⌝] (-2)⋅ THENA Auto')
   THEN (RW (AddrC [2] (LemmaC `select_append_front`)) (-1)⋅ THENA Auto')
   THEN (RW (AddrC [2] (LemmaC `select_append_back`)) (-1)⋅ THENA Auto')
   THEN (Subst ⌜||l1|| - ||l1|| ~ 0⌝ (-1)⋅ THENA Auto)
   THEN Reduce (-1)
   THEN (Assert ⌜||l1|| < ||l3|| ∨ ||l3|| < ||l1||⌝⋅ THENA Auto')
   THEN D (-1)) }

1
1. T : Type
2. l1 : T List
3. l2 : T List
4. l3 : T List
5. l4 : T List
6. x : T
7. no_repeats(T;(l1 @ [x]) @ l2)
8. ((l1 @ [x]) @ l2) = ((l3 @ [x]) @ l4) ∈ (T List)
9. ((||l1|| + 1) + ||l2||) = ((||l3|| + 1) + ||l4||) ∈ ℤ
10. ∀i:ℕ(||l1|| + 1) + ||l2||. ((l1 @ [x]) @ l2[i] = (l3 @ [x]) @ l4[i] ∈ T)
11. ¬(||l1|| = ||l3|| ∈ ℤ)
12. x = (l3 @ [x]) @ l4[||l1||] ∈ T
13. ||l1|| < ||l3||
⊢ False

2
1. T : Type
2. l1 : T List
3. l2 : T List
4. l3 : T List
5. l4 : T List
6. x : T
7. no_repeats(T;(l1 @ [x]) @ l2)
8. ((l1 @ [x]) @ l2) = ((l3 @ [x]) @ l4) ∈ (T List)
9. ((||l1|| + 1) + ||l2||) = ((||l3|| + 1) + ||l4||) ∈ ℤ
10. ∀i:ℕ(||l1|| + 1) + ||l2||. ((l1 @ [x]) @ l2[i] = (l3 @ [x]) @ l4[i] ∈ T)
11. ¬(||l1|| = ||l3|| ∈ ℤ)
12. x = (l3 @ [x]) @ l4[||l1||] ∈ T
13. ||l3|| < ||l1||
⊢ False

---

Latex:

---

Latex:

1.  T  :  Type
2.  l1  :  T  List
3.  l2  :  T  List
4.  l3  :  T  List
5.  l4  :  T  List
6.  x  :  T
7.  no\_repeats(T;(l1  @  [x])  @  l2)
8.  ((l1  @  [x])  @  l2)  =  ((l3  @  [x])  @  l4)
9.  ((||l1||  +  1)  +  ||l2||)  =  ((||l3||  +  1)  +  ||l4||)
10.  \mforall{}i:\mBbbN{}(||l1||  +  1)  +  ||l2||.  ((l1  @  [x])  @  l2[i]  =  (l3  @  [x])  @  l4[i])
\mvdash{}  ||l1||  =  ||l3||


By

---

Latex:
(SupposeNot
  THEN  Assert  \mkleeneopen{}False\mkleeneclose{}\mcdot{}
  THEN  Auto
  THEN  (InstHyp  [\mkleeneopen{}||l1||\mkleeneclose{}]  (-2)\mcdot{}  THENA  Auto')
  THEN  (RW  (AddrC  [2]  (LemmaC  `select\_append\_front`))  (-1)\mcdot{}  THENA  Auto')
  THEN  (RW  (AddrC  [2]  (LemmaC  `select\_append\_back`))  (-1)\mcdot{}  THENA  Auto')
  THEN  (Subst  \mkleeneopen{}||l1||  -  ||l1||  \msim{}  0\mkleeneclose{}  (-1)\mcdot{}  THENA  Auto)
  THEN  Reduce  (-1)
  THEN  (Assert  \mkleeneopen{}||l1||  <  ||l3||  \mvee{}  ||l3||  <  ||l1||\mkleeneclose{}\mcdot{}  THENA  Auto')
  THEN  D  (-1))

---

Home Index