---

Step * 1 1 2 1 1 2 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 : ℤ@i
6. [%3] : 0 < n@i
7. S : E List@i
8. sorted-by(λx,y. (y < x);S)@i
9. ||S|| = (n - 1) ∈ ℕ@i
10. ∀i:ℕ||S||. (S[i] ∈ L)@i
11. ∀i:ℕ||S||. ∀j:ℕi.  (S[i] < S[j])@i
12. ¬(n = 1 ∈ ℤ)
⊢ ∃S:E List. (sorted-by(λx,y. (y < x);S) ∧ (||S|| = n ∈ ℕ) ∧ (∀i:ℕ||S||. (S[i] ∈ L)))
BY
{ ((With ⌜S[0]⌝ (D 4)⋅ THENA (MemTypeCD THEN Auto)) THEN ExRepD) }

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

---

Latex:

---

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.  n  :  \mBbbZ{}@i
6.  [\%3]  :  0  <  n@i
7.  S  :  E  List@i
8.  sorted-by(\mlambda{}x,y.  (y  <  x);S)@i
9.  ||S||  =  (n  -  1)@i
10.  \mforall{}i:\mBbbN{}||S||.  (S[i]  \mmember{}  L)@i
11.  \mforall{}i:\mBbbN{}||S||.  \mforall{}j:\mBbbN{}i.    (S[i]  <  S[j])@i
12.  \mneg{}(n  =  1)
\mvdash{}  \mexists{}S:E  List.  (sorted-by(\mlambda{}x,y.  (y  <  x);S)  \mwedge{}  (||S||  =  n)  \mwedge{}  (\mforall{}i:\mBbbN{}||S||.  (S[i]  \mmember{}  L)))


By

---

Latex:
((With  \mkleeneopen{}S[0]\mkleeneclose{}  (D  4)\mcdot{}  THENA  (MemTypeCD  THEN  Auto))  THEN  ExRepD)

---

Home Index