---

Step * 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. concat(map(λe.≤loc(e);L)) = concat(map(λe.≤loc(e);L)) ∈ bag(E)
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 Thin (-4)) }

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 : ℕ||map(λe.≤loc(e);L)[i]||@i
⊢ ¬(≤loc(L[i])[k] ∈ ≤loc(L[j]))

---

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.  concat(map(\mlambda{}e.\mleq{}loc(e);L))  =  concat(map(\mlambda{}e.\mleq{}loc(e);L))
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

---

Latex:
(Thin  (-3)  THEN  Thin  (-4))

---

Home Index