---

Step * 1 1 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 : ℕ||≤loc(L[i])||@i
9. ≤loc(L[i])[k] ≤loc L[j] @i
10. ≤loc(L[i])[k] ≤loc L[i] 
⊢ False
BY
{ (InstLemma `es-locl-trichotomy` [⌜es⌝;⌜L[i]⌝;⌜L[j]⌝]⋅ 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
10. ≤loc(L[i])[k] ≤loc L[i] 
11. loc(L[i]) = loc(L[j]) ∈ Id ⇐⇒ (L[i] <loc L[j]) ∨ (L[i] = L[j] ∈ E) ∨ (L[j] <loc L[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{}||\mleq{}loc(L[i])||@i
9.  \mleq{}loc(L[i])[k]  \mleq{}loc  L[j]  @i
10.  \mleq{}loc(L[i])[k]  \mleq{}loc  L[i] 
\mvdash{}  False


By

---

Latex:
(InstLemma  `es-locl-trichotomy`  [\mkleeneopen{}es\mkleeneclose{};\mkleeneopen{}L[i]\mkleeneclose{};\mkleeneopen{}L[j]\mkleeneclose{}]\mcdot{}  THENA  Auto)\mcdot{}

---

Home Index