---

Step * 1 1 of Lemma failure-known-effective


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
8. e' : E@i
9. x c≤ e'@i
10. ¬(loc(e') = loc(x) ∈ Id)@i
⊢ False
BY
{ (InstHyp [⌈x⌉;⌈loc(e')⌉;⌈e'⌉] 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{}  (\mforall{}j:Id.  ((\mneg{}(j  =  i))  {}\mRightarrow{}  (\mforall{}y:E.  ((loc(y)  =  j)  {}\mRightarrow{}  (\mneg{}x  c\mleq{}  y))))))
5.  x  :  E@i
6.  loc(x)  =  i@i
7.  e  c\mleq{}  x@i
8.  e'  :  E@i
9.  x  c\mleq{}  e'@i
10.  \mneg{}(loc(e')  =  loc(x))@i
\mvdash{}  False


By

(InstHyp  [\mkleeneopen{}x\mkleeneclose{};\mkleeneopen{}loc(e')\mkleeneclose{};\mkleeneopen{}e'\mkleeneclose{}]  4\mcdot{}  THEN  Auto)

---

Home Index