---

Step * of Lemma failure-known-effective

∀[es:EO]. ∀[i:Id]. ∀[e:E].  uiff(failure-known(es;e;i);∀x@i.e c≤ x ⇒ (¬es-effective(es;x)))
BY
{ (RepUR ``failure-known alle-at es-effective`` 0⋅ THEN Auto) }

1
1. es : EO
2. i : Id
3. e : E
4. ∀x:E. ((loc(x) = i ∈ Id) ⇒ e c≤ x ⇒ (∀j:Id. ((¬(j = i ∈ Id)) ⇒ (∀y:E. ((loc(y) = j ∈ Id) ⇒ (¬x c≤ y))))))
5. x : E@i
6. loc(x) = i ∈ Id@i
7. e c≤ x@i
⊢ ¬(∃e':E. (x c≤ e' ∧ (¬(loc(e') = loc(x) ∈ Id))))

2
1. es : EO
2. i : Id
3. e : E
4. ∀x:E. ((loc(x) = i ∈ Id) ⇒ e c≤ x ⇒ (¬(∃e':E. (x c≤ e' ∧ (¬(loc(e') = loc(x) ∈ Id))))))
5. x : E@i
6. loc(x) = i ∈ Id@i
7. e c≤ x@i
8. j : Id@i
9. ¬(j = i ∈ Id)@i
10. y : E@i
11. loc(y) = j ∈ Id@i
⊢ ¬x c≤ y

---

Latex:

---

Latex:
\mforall{}[es:EO].  \mforall{}[i:Id].  \mforall{}[e:E].    uiff(failure-known(es;e;i);\mforall{}x@i.e  c\mleq{}  x  {}\mRightarrow{}  (\mneg{}es-effective(es;x)))


By

---

Latex:
(RepUR  ``failure-known  alle-at  es-effective``  0\mcdot{}  THEN  Auto)

---

Home Index