---

Step * of Lemma failure-known-causle

∀[es:EO]. ∀[i:Id]. ∀[e,e':E].  (failure-known(es;e';i)) supposing (failure-known(es;e;i) and e c≤ e')
BY
{ (Auto THEN RepeatFor 5 ((ParallelLast'⋅ THENA Auto))) }

---

Latex:


\mforall{}[es:EO].  \mforall{}[i:Id].  \mforall{}[e,e':E].
    (failure-known(es;e';i))  supposing  (failure-known(es;e;i)  and  e  c\mleq{}  e')


By

(Auto  THEN  RepeatFor  5  ((ParallelLast'\mcdot{}  THENA  Auto)))

---

Home Index