---

Step * 1 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. j : ℕ||L||@i
9. ¬(i = j ∈ ℤ)@i
10. k : ℕ||≤loc(L[i])||@i
11. (≤loc(L[i])[k] ∈ ≤loc(L[j]))@i
⊢ False
BY
{ (Assert loc(≤loc(L[i])[k]) = loc(L[j]) ∈ Id BY
         (RWO "member-es-le-before" (-1) THEN Auto)) }

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
12. loc(≤loc(L[i])[k]) = loc(L[j]) ∈ Id
⊢ 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.  j  :  \mBbbN{}||L||@i
9.  \mneg{}(i  =  j)@i
10.  k  :  \mBbbN{}||\mleq{}loc(L[i])||@i
11.  (\mleq{}loc(L[i])[k]  \mmember{}  \mleq{}loc(L[j]))@i
\mvdash{}  False


By

(Assert  loc(\mleq{}loc(L[i])[k])  =  loc(L[j])  BY
              (RWO  "member-es-le-before"  (-1)  THEN  Auto))

---

Home Index