---

Step * 1 1 2 2 1 of Lemma decidable__exists-last-classrel-between3


1. [Info] : Type
2. [T] : Type
3. X : EClass(T)@i'
4. es : EO+(Info)@i'
5. e1 : E@i
6. e2 : E@i
7. ∀e':E
     ((e' < e2)
     ⇒ (loc(e1) = loc(e') ∈ Id)
     ⇒ (e1 <loc e')
     ⇒ Dec(∃e:E
             ((e1 <loc e)
             ∧ e ≤loc e' 
             ∧ (↓∃v:T. v ∈ X(e))
             ∧ (∀e'':E. ((e <loc e'') ⇒ e'' ≤loc e'  ⇒ (∀x:T. (¬x ∈ X(e''))))))))
8. loc(e1) = loc(e2) ∈ Id@i
9. (e1 <loc e2)@i
10. ¬↓∃v:T. v ∈ X(e2)
11. e1 = pred(e2) ∈ E
12. e : E@i
13. (e1 <loc e)@i
14. e ≤loc e2 @i
15. ↓∃v:T. v ∈ X(e)@i
16. ∀e'':E. ((e <loc e'') ⇒ e'' ≤loc e2  ⇒ (∀x:T. (¬x ∈ X(e''))))@i
⊢ False
BY
{ ((Assert ⌈e = e2 ∈ E⌉⋅ THENM (HypSubst' (-1) (-3) THEN Auto))
   THENA (D (-3)
          THEN Auto
          THEN (Assert ⌈False⌉⋅ THEN Auto)
          THEN InstLemma `es-pred_property` [⌈es⌉;⌈e2⌉]⋅
          THEN Auto
          THEN (InstHyp [⌈e⌉] (-1)⋅ THENA Auto)
          THEN D (-1)
          THEN Try (Complete (Auto)))
   ) }

---

Latex:



1.  [Info]  :  Type
2.  [T]  :  Type
3.  X  :  EClass(T)@i'
4.  es  :  EO+(Info)@i'
5.  e1  :  E@i
6.  e2  :  E@i
7.  \mforall{}e':E
          ((e'  <  e2)
          {}\mRightarrow{}  (loc(e1)  =  loc(e'))
          {}\mRightarrow{}  (e1  <loc  e')
          {}\mRightarrow{}  Dec(\mexists{}e:E
                          ((e1  <loc  e)
                          \mwedge{}  e  \mleq{}loc  e' 
                          \mwedge{}  (\mdownarrow{}\mexists{}v:T.  v  \mmember{}  X(e))
                          \mwedge{}  (\mforall{}e'':E.  ((e  <loc  e'')  {}\mRightarrow{}  e''  \mleq{}loc  e'    {}\mRightarrow{}  (\mforall{}x:T.  (\mneg{}x  \mmember{}  X(e''))))))))
8.  loc(e1)  =  loc(e2)@i
9.  (e1  <loc  e2)@i
10.  \mneg{}\mdownarrow{}\mexists{}v:T.  v  \mmember{}  X(e2)
11.  e1  =  pred(e2)
12.  e  :  E@i
13.  (e1  <loc  e)@i
14.  e  \mleq{}loc  e2  @i
15.  \mdownarrow{}\mexists{}v:T.  v  \mmember{}  X(e)@i
16.  \mforall{}e'':E.  ((e  <loc  e'')  {}\mRightarrow{}  e''  \mleq{}loc  e2    {}\mRightarrow{}  (\mforall{}x:T.  (\mneg{}x  \mmember{}  X(e''))))@i
\mvdash{}  False


By

((Assert  \mkleeneopen{}e  =  e2\mkleeneclose{}\mcdot{}  THENM  (HypSubst'  (-1)  (-3)  THEN  Auto))
  THENA  (D  (-3)
                THEN  Auto
                THEN  (Assert  \mkleeneopen{}False\mkleeneclose{}\mcdot{}  THEN  Auto)
                THEN  InstLemma  `es-pred\_property`  [\mkleeneopen{}es\mkleeneclose{};\mkleeneopen{}e2\mkleeneclose{}]\mcdot{}
                THEN  Auto
                THEN  (InstHyp  [\mkleeneopen{}e\mkleeneclose{}]  (-1)\mcdot{}  THENA  Auto)
                THEN  D  (-1)
                THEN  Try  (Complete  (Auto)))
  )

---

Home Index