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


1. Type
2. streamless(T)
3. ∀x,y:T.  Dec(x y ∈ T)
4. 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))
⊢ False
BY
xxxAssert ⌜∀x:T. (x ∈ s)⌝⋅xxx }

1
.....assertion..... 
1. Type
2. streamless(T)
3. ∀x,y:T.  Dec(x y ∈ T)
4. 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))
⊢ ∀x:T. (x ∈ s)

2
1. Type
2. streamless(T)
3. ∀x,y:T.  Dec(x y ∈ T)
4. 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. (x ∈ s)
⊢ False


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))
\mvdash{}  False


By


Latex:
xxxAssert  \mkleeneopen{}\mforall{}x:T.  (x  \mmember{}  s)\mkleeneclose{}\mcdot{}xxx




Home Index