---

Step * 1 2 1 of Lemma es-causl-max-list


1. es : EO@i'
2. L : E List@i
3. 0 < ||L||@i
4. ∀e:{e:E| (e ∈ L)} . ∃e':{e:E| (e ∈ L)} . (e < e')@i
5. ∀n:ℕ. ∃S:E List. (sorted-by(λx,y. (y < x);S) ∧ (||S|| = n ∈ ℕ) ∧ (∀i:ℕ||S||. (S[i] ∈ L)))
6. S : E List
7. sorted-by(λx,y. (y < x);S)
8. ||S|| = (||L|| + 1) ∈ ℕ
9. ∀i:ℕ||S||. (S[i] ∈ L)
⊢ False
BY
{ (FLemma `sorted-by-strict-no_repeats` [-3] THEN Auto THEN Reduce 0 THEN Auto) }

1
1. es : EO@i'
2. L : E List@i
3. 0 < ||L||@i
4. ∀e:{e:E| (e ∈ L)} . ∃e':{e:E| (e ∈ L)} . (e < e')@i
5. ∀n:ℕ. ∃S:E List. (sorted-by(λx,y. (y < x);S) ∧ (||S|| = n ∈ ℕ) ∧ (∀i:ℕ||S||. (S[i] ∈ L)))
6. S : E List
7. sorted-by(λx,y. (y < x);S)
8. ||S|| = (||L|| + 1) ∈ ℕ
9. ∀i:ℕ||S||. (S[i] ∈ L)
10. no_repeats(E;S)
⊢ False

---

Latex:



1.  es  :  EO@i'
2.  L  :  E  List@i
3.  0  <  ||L||@i
4.  \mforall{}e:\{e:E|  (e  \mmember{}  L)\}  .  \mexists{}e':\{e:E|  (e  \mmember{}  L)\}  .  (e  <  e')@i
5.  \mforall{}n:\mBbbN{}.  \mexists{}S:E  List.  (sorted-by(\mlambda{}x,y.  (y  <  x);S)  \mwedge{}  (||S||  =  n)  \mwedge{}  (\mforall{}i:\mBbbN{}||S||.  (S[i]  \mmember{}  L)))
6.  S  :  E  List
7.  sorted-by(\mlambda{}x,y.  (y  <  x);S)
8.  ||S||  =  (||L||  +  1)
9.  \mforall{}i:\mBbbN{}||S||.  (S[i]  \mmember{}  L)
\mvdash{}  False


By

(FLemma  `sorted-by-strict-no\_repeats`  [-3]  THEN  Auto  THEN  Reduce  0  THEN  Auto)

---

Home Index