---

Step * 1 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
12. loc(≤loc(L[i])[k]) = loc(L[j]) ∈ Id
⊢ False
BY
{ ((Assert ⌈loc(≤loc(L[i])[k]) = loc(L[i]) ∈ Id⌉⋅
    THENA ((Assert ⌈(≤loc(L[i])[k] ∈ ≤loc(L[i]))⌉⋅ THENA (BLemma `select_member` THEN Auto))
           THEN (RWO "member-es-le-before" (-1) THENA Auto)
           THEN Auto)
    )
   THEN HypSubst' (-2) (-1)
   THEN (InstLemma `es-causl-total` [⌈es⌉;⌈L[j]⌉;⌈L[i]⌉]⋅ THENA Auto)
   THEN D (-1)
   THEN Try (Complete ((Unfold `no_repeats` (-10) THEN InstHyp [⌈i⌉;⌈j⌉] (-10)⋅ THEN Auto')))
   THEN (Assert ⌈(L[j] <loc L[i]) ∨ (L[i] <loc L[j])⌉⋅
         THENA (D (-1) THEN Try (Complete ((Sel 1 (D 0) THEN Auto))) THEN Try (Complete ((Sel 2 (D 0) THEN Auto))))
         )
   THEN Thin (-2)
   THEN (InstHyp [⌈L[j]⌉;⌈L[i]⌉] (-9)⋅
         THENA (Auto
                THEN Unfold `bag-member` 0
                THEN D 0
                THEN InstConcl [⌈L⌉]⋅
                THEN Auto
                THEN BLemma `select_member`
                THEN Auto)
         )
   THEN (InstHyp [⌈L[i]⌉;⌈L[j]⌉] (-10)⋅
         THENA (Auto
                THEN Unfold `bag-member` 0
                THEN D 0
                THEN InstConcl [⌈L⌉]⋅
                THEN Auto
                THEN BLemma `select_member`
                THEN Auto)
         )
   THEN D (-3)
   THEN Auto)⋅ }

---

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
12.  loc(\mleq{}loc(L[i])[k])  =  loc(L[j])
\mvdash{}  False


By

((Assert  \mkleeneopen{}loc(\mleq{}loc(L[i])[k])  =  loc(L[i])\mkleeneclose{}\mcdot{}
    THENA  ((Assert  \mkleeneopen{}(\mleq{}loc(L[i])[k]  \mmember{}  \mleq{}loc(L[i]))\mkleeneclose{}\mcdot{}  THENA  (BLemma  `select\_member`  THEN  Auto))
                  THEN  (RWO  "member-es-le-before"  (-1)  THENA  Auto)
                  THEN  Auto)
    )
  THEN  HypSubst'  (-2)  (-1)
  THEN  (InstLemma  `es-causl-total`  [\mkleeneopen{}es\mkleeneclose{};\mkleeneopen{}L[j]\mkleeneclose{};\mkleeneopen{}L[i]\mkleeneclose{}]\mcdot{}  THENA  Auto)
  THEN  D  (-1)
  THEN  Try  (Complete  ((Unfold  `no\_repeats`  (-10)  THEN  InstHyp  [\mkleeneopen{}i\mkleeneclose{};\mkleeneopen{}j\mkleeneclose{}]  (-10)\mcdot{}  THEN  Auto')))
  THEN  (Assert  \mkleeneopen{}(L[j]  <loc  L[i])  \mvee{}  (L[i]  <loc  L[j])\mkleeneclose{}\mcdot{}
              THENA  (D  (-1)
                            THEN  Try  (Complete  ((Sel  1  (D  0)  THEN  Auto)))
                            THEN  Try  (Complete  ((Sel  2  (D  0)  THEN  Auto))))
              )
  THEN  Thin  (-2)
  THEN  (InstHyp  [\mkleeneopen{}L[j]\mkleeneclose{};\mkleeneopen{}L[i]\mkleeneclose{}]  (-9)\mcdot{}
              THENA  (Auto
                            THEN  Unfold  `bag-member`  0
                            THEN  D  0
                            THEN  InstConcl  [\mkleeneopen{}L\mkleeneclose{}]\mcdot{}
                            THEN  Auto
                            THEN  BLemma  `select\_member`
                            THEN  Auto)
              )
  THEN  (InstHyp  [\mkleeneopen{}L[i]\mkleeneclose{};\mkleeneopen{}L[j]\mkleeneclose{}]  (-10)\mcdot{}
              THENA  (Auto
                            THEN  Unfold  `bag-member`  0
                            THEN  D  0
                            THEN  InstConcl  [\mkleeneopen{}L\mkleeneclose{}]\mcdot{}
                            THEN  Auto
                            THEN  BLemma  `select\_member`
                            THEN  Auto)
              )
  THEN  D  (-3)
  THEN  Auto)\mcdot{}

---

Home Index