---

Step * 1 1 1 of Lemma class-output-support-no-repeats


1. Info : Type
2. es : EO+(Info)
3. L : E List
4. no_repeats(E;L)
5. ∀e1,e2:E.  (e1 ↓∈ L ⇒ e2 ↓∈ L ⇒ (¬(e1 <loc e2)))
6. i : ℕ||L||@i
7. j : {j:ℕ||L||| ¬(i = j ∈ ℤ)} @i
8. k : ℕ||map(λe.≤loc(e);L)[i]||@i
⊢ ¬(≤loc(L[i])[k] ∈ ≤loc(L[j]))
BY
{ ((RWO "select-map" (-1) THENA Auto) THEN Reduce (-1) THEN ((RWO "member-es-le-before" 0 THENM D 0) THENA Auto)⋅) }

1
1. Info : Type
2. es : EO+(Info)
3. L : E List
4. no_repeats(E;L)
5. ∀e1,e2:E.  (e1 ↓∈ L ⇒ e2 ↓∈ L ⇒ (¬(e1 <loc e2)))
6. i : ℕ||L||@i
7. j : {j:ℕ||L||| ¬(i = j ∈ ℤ)} @i
8. k : ℕ||≤loc(L[i])||@i
9. ≤loc(L[i])[k] ≤loc L[j] @i
⊢ False

---

Latex:

---

Latex:

1.  Info  :  Type
2.  es  :  EO+(Info)
3.  L  :  E  List
4.  no\_repeats(E;L)
5.  \mforall{}e1,e2:E.    (e1  \mdownarrow{}\mmember{}  L  {}\mRightarrow{}  e2  \mdownarrow{}\mmember{}  L  {}\mRightarrow{}  (\mneg{}(e1  <loc  e2)))
6.  i  :  \mBbbN{}||L||@i
7.  j  :  \{j:\mBbbN{}||L|||  \mneg{}(i  =  j)\}  @i
8.  k  :  \mBbbN{}||map(\mlambda{}e.\mleq{}loc(e);L)[i]||@i
\mvdash{}  \mneg{}(\mleq{}loc(L[i])[k]  \mmember{}  \mleq{}loc(L[j]))


By

---

Latex:
((RWO  "select-map"  (-1)  THENA  Auto)
  THEN  Reduce  (-1)
  THEN  ((RWO  "member-es-le-before"  0  THENM  D  0)  THENA  Auto)\mcdot{})

---

Home Index