---

Step * 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 ∈ ℕ)
⊢ ¬(bs @ as[i] = bs @ as[j] ∈ T)
BY
{ xxx(((All (RWO "length-append")) THENA Auto)
      THEN (Decide i < ||bs|| THENA Auto)
      THEN (Decide j < ||bs|| THENA Auto))xxx }

1
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)

2
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)

3
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)

4
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)

---

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)
\mvdash{}  \mneg{}(bs  @  as[i]  =  bs  @  as[j])


By

---

Latex:
xxx(((All  (RWO  "length-append"))  THENA  Auto)
        THEN  (Decide  i  <  ||bs||  THENA  Auto)
        THEN  (Decide  j  <  ||bs||  THENA  Auto))xxx

---

Home Index