---

Step * 2 of Lemma es-effective-causle


1. es : EO@i'
2. e : E@i
3. e' : E@i
4. e c≤ e'@i
5. e'@0 : E@i
6. e' c≤ e'@0@i
7. ¬(loc(e'@0) = loc(e') ∈ Id)@i
8. ¬(loc(e'@0) = loc(e) ∈ Id)
⊢ ∃e':E. (e c≤ e' ∧ (¬(loc(e') = loc(e) ∈ Id)))
BY
{ (InstConcl [⌈e'@0⌉] ⋅ THEN Auto) }

---

Latex:



1.  es  :  EO@i'
2.  e  :  E@i
3.  e'  :  E@i
4.  e  c\mleq{}  e'@i
5.  e'@0  :  E@i
6.  e'  c\mleq{}  e'@0@i
7.  \mneg{}(loc(e'@0)  =  loc(e'))@i
8.  \mneg{}(loc(e'@0)  =  loc(e))
\mvdash{}  \mexists{}e':E.  (e  c\mleq{}  e'  \mwedge{}  (\mneg{}(loc(e')  =  loc(e))))


By

(InstConcl  [\mkleeneopen{}e'@0\mkleeneclose{}]  \mcdot{}  THEN  Auto)

---

Home Index