---

Step * 1 1 1 1 1 1 1 of Lemma streamless-implies-not-not-enum


1. T : Type
2. streamless(T)
3. ∀x,y:T.  Dec(x = y ∈ T)
4. s : T List
5. ∀t:T. ((¬no_repeats(T;s @ [t])) ∨ (¬¬(∃L:T List. ∀x:T. (x ∈ L))))
6. no_repeats(T;s)
7. ¬(∃L:T List. ∀x:T. (x ∈ L))
8. x : T
9. ¬(x ∈ s)
10. i : ℕ
11. j : ℕ
12. ¬j < ||s||
13. i < ||s @ [x]||
14. j < ||s @ [x]||
15. ¬(i = j ∈ ℕ)
16. i < ||s||
⊢ ¬(s[i] = [x][j - ||s||] ∈ T)
BY
{ xxxSubst' j - ||s|| ~ 0 0xxx }

1
.....equality..... 
1. T : Type
2. streamless(T)
3. ∀x,y:T.  Dec(x = y ∈ T)
4. s : T List
5. ∀t:T. ((¬no_repeats(T;s @ [t])) ∨ (¬¬(∃L:T List. ∀x:T. (x ∈ L))))
6. no_repeats(T;s)
7. ¬(∃L:T List. ∀x:T. (x ∈ L))
8. x : T
9. ¬(x ∈ s)
10. i : ℕ
11. j : ℕ
12. ¬j < ||s||
13. i < ||s @ [x]||
14. j < ||s @ [x]||
15. ¬(i = j ∈ ℕ)
16. i < ||s||
⊢ j - ||s|| ~ 0

2
1. T : Type
2. streamless(T)
3. ∀x,y:T.  Dec(x = y ∈ T)
4. s : T List
5. ∀t:T. ((¬no_repeats(T;s @ [t])) ∨ (¬¬(∃L:T List. ∀x:T. (x ∈ L))))
6. no_repeats(T;s)
7. ¬(∃L:T List. ∀x:T. (x ∈ L))
8. x : T
9. ¬(x ∈ s)
10. i : ℕ
11. j : ℕ
12. ¬j < ||s||
13. i < ||s @ [x]||
14. j < ||s @ [x]||
15. ¬(i = j ∈ ℕ)
16. i < ||s||
⊢ ¬(s[i] = [x][0] ∈ T)

---

Latex:

---

Latex:

1.  T  :  Type
2.  streamless(T)
3.  \mforall{}x,y:T.    Dec(x  =  y)
4.  s  :  T  List
5.  \mforall{}t:T.  ((\mneg{}no\_repeats(T;s  @  [t]))  \mvee{}  (\mneg{}\mneg{}(\mexists{}L:T  List.  \mforall{}x:T.  (x  \mmember{}  L))))
6.  no\_repeats(T;s)
7.  \mneg{}(\mexists{}L:T  List.  \mforall{}x:T.  (x  \mmember{}  L))
8.  x  :  T
9.  \mneg{}(x  \mmember{}  s)
10.  i  :  \mBbbN{}
11.  j  :  \mBbbN{}
12.  \mneg{}j  <  ||s||
13.  i  <  ||s  @  [x]||
14.  j  <  ||s  @  [x]||
15.  \mneg{}(i  =  j)
16.  i  <  ||s||
\mvdash{}  \mneg{}(s[i]  =  [x][j  -  ||s||])


By

---

Latex:
xxxSubst'  j  -  ||s||  \msim{}  0  0xxx

---

Home Index