---

Step * 2 of Lemma failure-known-effective


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
BY
{ (InstHyp [⌈x⌉] 4⋅ THEN Auto) }

---

Latex:



1.  es  :  EO
2.  i  :  Id
3.  e  :  E
4.  \mforall{}x:E.  ((loc(x)  =  i)  {}\mRightarrow{}  e  c\mleq{}  x  {}\mRightarrow{}  (\mneg{}(\mexists{}e':E.  (x  c\mleq{}  e'  \mwedge{}  (\mneg{}(loc(e')  =  loc(x)))))))
5.  x  :  E@i
6.  loc(x)  =  i@i
7.  e  c\mleq{}  x@i
8.  j  :  Id@i
9.  \mneg{}(j  =  i)@i
10.  y  :  E@i
11.  loc(y)  =  j@i
\mvdash{}  \mneg{}x  c\mleq{}  y


By

(InstHyp  [\mkleeneopen{}x\mkleeneclose{}]  4\mcdot{}  THEN  Auto)

---

Home Index