---

Step * 1 1 2 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(((RW (AddrC [1; 3] (LemmaC `select_append_back`)) 0) THENA Auto')
      THEN ((RW (AddrC [1; 2] (LemmaC `select_append_front`)) 0) THENA Auto')
      THEN ((InstHyp [⌜i + ||as||⌝; ⌜j - ||bs||⌝] 4)⋅ THENA Auto')
      THEN ((RW (AddrC [1; 2] (LemmaC `select_append_back`)) (-1)) THENA Auto')
      THEN ((RW (AddrC [1; 3] (LemmaC `select_append_front`)) (-1)) THENA Auto')
      THEN ((RW IntNormC (-1)) THENM RW IntNormC 0)
      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.  \mneg{}j  <  ||bs||
\mvdash{}  \mneg{}(bs  @  as[i]  =  bs  @  as[j])


By

---

Latex:
xxx(((RW  (AddrC  [1;  3]  (LemmaC  `select\_append\_back`))  0)  THENA  Auto')
        THEN  ((RW  (AddrC  [1;  2]  (LemmaC  `select\_append\_front`))  0)  THENA  Auto')
        THEN  ((InstHyp  [\mkleeneopen{}i  +  ||as||\mkleeneclose{};  \mkleeneopen{}j  -  ||bs||\mkleeneclose{}]  4)\mcdot{}  THENA  Auto')
        THEN  ((RW  (AddrC  [1;  2]  (LemmaC  `select\_append\_back`))  (-1))  THENA  Auto')
        THEN  ((RW  (AddrC  [1;  3]  (LemmaC  `select\_append\_front`))  (-1))  THENA  Auto')
        THEN  ((RW  IntNormC  (-1))  THENM  RW  IntNormC  0)
        THEN  Auto')xxx

---

Home Index