Step
*
1
1
of Lemma
no_repeats_append
1. T : Type
2. l1 : T List
3. l2 : T List
4. ∀[i,j:ℕ].  (¬(l1 @ l2[i] = l1 @ l2[j] ∈ T)) supposing ((¬(i = j ∈ ℕ)) and j < ||l1 @ l2|| and i < ||l1 @ l2||)
5. x : T
6. i1 : ℕ
7. i1 < ||l1||
8. x = l1[i1] ∈ T
9. i : ℕ
10. i < ||l2||
11. x = l2[i] ∈ T
12. ¬(l1 @ l2[i1] = l1 @ l2[i + ||l1||] ∈ T)
⊢ False
BY
{ ((D (-1) THEN Subst l1 @ l2[i1] = x ∈ T 0) THENA Auto') }
1
1. T : Type
2. l1 : T List
3. l2 : T List
4. ∀[i,j:ℕ].  (¬(l1 @ l2[i] = l1 @ l2[j] ∈ T)) supposing ((¬(i = j ∈ ℕ)) and j < ||l1 @ l2|| and i < ||l1 @ l2||)
5. x : T
6. i1 : ℕ
7. i1 < ||l1||
8. x = l1[i1] ∈ T
9. i : ℕ
10. i < ||l2||
11. x = l2[i] ∈ T
⊢ x = l1 @ l2[i + ||l1||] ∈ T
Latex:
Latex:
1.  T  :  Type
2.  l1  :  T  List
3.  l2  :  T  List
4.  \mforall{}[i,j:\mBbbN{}].
          (\mneg{}(l1  @  l2[i]  =  l1  @  l2[j]))  supposing  ((\mneg{}(i  =  j))  and  j  <  ||l1  @  l2||  and  i  <  ||l1  @  l2||)
5.  x  :  T
6.  i1  :  \mBbbN{}
7.  i1  <  ||l1||
8.  x  =  l1[i1]
9.  i  :  \mBbbN{}
10.  i  <  ||l2||
11.  x  =  l2[i]
12.  \mneg{}(l1  @  l2[i1]  =  l1  @  l2[i  +  ||l1||])
\mvdash{}  False
By
Latex:
((D  (-1)  THEN  Subst  l1  @  l2[i1]  =  x  0)  THENA  Auto')
Home
Index