---

Step * 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
⊢ ¬(∃e':E. (x c≤ e' ∧ (¬(loc(e') = loc(x) ∈ Id))))
BY
{ ((D 0 THENA Auto) THEN ExRepD) }

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
8. e' : E@i
9. x c≤ e'@i
10. ¬(loc(e') = loc(x) ∈ Id)@i
⊢ False

---

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
\mvdash{}  \mneg{}(\mexists{}e':E.  (x  c\mleq{}  e'  \mwedge{}  (\mneg{}(loc(e')  =  loc(x)))))


By

((D  0  THENA  Auto)  THEN  ExRepD)

---

Home Index