---

Step * 1 1 1 of Lemma no_repeats-permute


1. T : Type
2. as : T List
3. bs : T List
4. ∀[i,j:ℕ].
     (¬(as @ bs[i] = as @ bs[j] ∈ T)) supposing ((¬(i = j ∈ ℕ)) and j < ||as|| + ||bs|| and i < ||as|| + ||bs||)
5. i : ℕ
6. j : ℕ
7. i < ||bs|| + ||as||
8. j < ||bs|| + ||as||
9. ¬(i = j ∈ ℕ)
10. i < ||bs||
11. j < ||bs||
⊢ ¬(bs @ as[i] = bs @ as[j] ∈ T)
BY
{ xxx((RWO "select_append_front" 0 THENA Auto)
      THEN ((InstHyp [⌜||as|| + i⌝; ⌜||as|| + j⌝] 4)⋅ THENA Auto')
      THEN ((RWO "select_append_back" (-1)) THENA Auto')
      THEN (RW IntNormC (-1))
      THEN Auto)xxx }

---

Latex:

---

Latex:

1.  T  :  Type
2.  as  :  T  List
3.  bs  :  T  List
4.  \mforall{}[i,j:\mBbbN{}].
          (\mneg{}(as  @  bs[i]  =  as  @  bs[j]))  supposing 
                ((\mneg{}(i  =  j))  and 
                j  <  ||as||  +  ||bs||  and 
                i  <  ||as||  +  ||bs||)
5.  i  :  \mBbbN{}
6.  j  :  \mBbbN{}
7.  i  <  ||bs||  +  ||as||
8.  j  <  ||bs||  +  ||as||
9.  \mneg{}(i  =  j)
10.  i  <  ||bs||
11.  j  <  ||bs||
\mvdash{}  \mneg{}(bs  @  as[i]  =  bs  @  as[j])


By

---

Latex:
xxx((RWO  "select\_append\_front"  0  THENA  Auto)
        THEN  ((InstHyp  [\mkleeneopen{}||as||  +  i\mkleeneclose{};  \mkleeneopen{}||as||  +  j\mkleeneclose{}]  4)\mcdot{}  THENA  Auto')
        THEN  ((RWO  "select\_append\_back"  (-1))  THENA  Auto')
        THEN  (RW  IntNormC  (-1))
        THEN  Auto)xxx

---

Home Index