---

Step * 1 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. loc(e1) = loc(e2) ∈ Id
8. (e1 <loc e2)
⊢ Dec(∃e:E
       ((e1 <loc e)
       ∧ e ≤loc e2 
       ∧ (↓∃v:T. v ∈ X(e))
       ∧ (∀e'':E. ((e <loc e'') ⇒ e'' ≤loc e2  ⇒ (∀x:T. (¬x ∈ X(e'')))))))
BY
{ (RepeatFor 3 (MoveToConcl (-1))
   THEN VrCausalInd'
   THEN Auto
   THEN (InstLemma `decidable__exists_classrel` [⌈Info⌉;⌈T⌉;⌈X⌉;⌈es⌉;⌈e2⌉]⋅ THENA Auto)
   THEN D (-1)) }

1
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)
⊢ Dec(∃e:E
       ((e1 <loc e)
       ∧ e ≤loc e2 
       ∧ (↓∃v:T. v ∈ X(e))
       ∧ (∀e'':E. ((e <loc e'') ⇒ e'' ≤loc e2  ⇒ (∀x:T. (¬x ∈ X(e'')))))))

2
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)
⊢ Dec(∃e:E
       ((e1 <loc e)
       ∧ e ≤loc e2 
       ∧ (↓∃v:T. v ∈ X(e))
       ∧ (∀e'':E. ((e <loc e'') ⇒ e'' ≤loc e2  ⇒ (∀x:T. (¬x ∈ X(e'')))))))

---

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.  loc(e1)  =  loc(e2)
8.  (e1  <loc  e2)
\mvdash{}  Dec(\mexists{}e:E
              ((e1  <loc  e)
              \mwedge{}  e  \mleq{}loc  e2 
              \mwedge{}  (\mdownarrow{}\mexists{}v:T.  v  \mmember{}  X(e))
              \mwedge{}  (\mforall{}e'':E.  ((e  <loc  e'')  {}\mRightarrow{}  e''  \mleq{}loc  e2    {}\mRightarrow{}  (\mforall{}x:T.  (\mneg{}x  \mmember{}  X(e'')))))))


By

(RepeatFor  3  (MoveToConcl  (-1))
  THEN  VrCausalInd'
  THEN  Auto
  THEN  (InstLemma  `decidable\_\_exists\_classrel`  [\mkleeneopen{}Info\mkleeneclose{};\mkleeneopen{}T\mkleeneclose{};\mkleeneopen{}X\mkleeneclose{};\mkleeneopen{}es\mkleeneclose{};\mkleeneopen{}e2\mkleeneclose{}]\mcdot{}  THENA  Auto)
  THEN  D  (-1))

---

Home Index