---

Step * 1 1 1 of Lemma class-output-support-no_repeats


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

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

---

Latex:



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


By

(Thin  (-3)  THEN  (RWW  "select-map"  (-1)\mcdot{}  THENM  Reduce  (-1)  THENM  D  0)  THEN  Auto  THEN  D  (-3))

---

Home Index