---

Step * of Lemma es-effective-causle

∀es:EO. ∀e,e':E.  (e c≤ e' ⇒ es-effective(es;e') ⇒ es-effective(es;e))
BY
{ (((Auto THEN ParallelLast) THEN ExRepD) THEN (Decide loc(e'@0) = loc(e) ∈ Id THENA Auto)) }

1
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)))

2
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)))

---

Latex:


\mforall{}es:EO.  \mforall{}e,e':E.    (e  c\mleq{}  e'  {}\mRightarrow{}  es-effective(es;e')  {}\mRightarrow{}  es-effective(es;e))


By

(((Auto  THEN  ParallelLast)  THEN  ExRepD)  THEN  (Decide  loc(e'@0)  =  loc(e)  THENA  Auto))

---

Home Index