---

Step * 1 of Lemma ses-nonce-release


1. s : SES@i'
2. es : EO+(Info)@i'
3. ∀n:E(New). ∀e:E.
     (e has* New(n)
     ⇒ (n c≤ e ∧ ((¬(loc(e) = loc(n) ∈ Id)) ⇒ (∃e':E(Send). ((n <loc e') ∧ e' has* New(n) ∧ (e' < e))))))
4. n : E(New)@i
5. ∀e:E
     (e has* New(n)
     ⇒ (n c≤ e ∧ ((¬(loc(e) = loc(n) ∈ Id)) ⇒ (∃e':E(Send). ((n <loc e') ∧ e' has* New(n) ∧ (e' < e))))))
6. e : E@i
7. e has* New(n) ⇒ (n c≤ e ∧ ((¬(loc(e) = loc(n) ∈ Id)) ⇒ (∃e':E(Send). ((n <loc e') ∧ e' has* New(n) ∧ (e' < e)))))
8. loc(e) = loc(n) ∈ Id@i
9. ¬(New(n) released before e)@i
10. e' : E@i
11. ¬(loc(e') = loc(e) ∈ Id)@i
12. e' has* New(n)@i
13. n c≤ e'
14. snd : E(Send)
15. (n <loc snd)
16. snd has* New(n)
17. (snd < e')
⊢ (e < e')
BY
{ (Assert ⌈e ≤loc snd ⌉⋅ THEN Auto) }

1
.....assertion..... 
1. s : SES@i'
2. es : EO+(Info)@i'
3. ∀n:E(New). ∀e:E.
     (e has* New(n)
     ⇒ (n c≤ e ∧ ((¬(loc(e) = loc(n) ∈ Id)) ⇒ (∃e':E(Send). ((n <loc e') ∧ e' has* New(n) ∧ (e' < e))))))
4. n : E(New)@i
5. ∀e:E
     (e has* New(n)
     ⇒ (n c≤ e ∧ ((¬(loc(e) = loc(n) ∈ Id)) ⇒ (∃e':E(Send). ((n <loc e') ∧ e' has* New(n) ∧ (e' < e))))))
6. e : E@i
7. e has* New(n) ⇒ (n c≤ e ∧ ((¬(loc(e) = loc(n) ∈ Id)) ⇒ (∃e':E(Send). ((n <loc e') ∧ e' has* New(n) ∧ (e' < e)))))
8. loc(e) = loc(n) ∈ Id@i
9. ¬(New(n) released before e)@i
10. e' : E@i
11. ¬(loc(e') = loc(e) ∈ Id)@i
12. e' has* New(n)@i
13. n c≤ e'
14. snd : E(Send)
15. (n <loc snd)
16. snd has* New(n)
17. (snd < e')
⊢ e ≤loc snd 

---

Latex:

---

Latex:

1.  s  :  SES@i'
2.  es  :  EO+(Info)@i'
3.  \mforall{}n:E(New).  \mforall{}e:E.
          (e  has*  New(n)
          {}\mRightarrow{}  (n  c\mleq{}  e
                \mwedge{}  ((\mneg{}(loc(e)  =  loc(n)))  {}\mRightarrow{}  (\mexists{}e':E(Send).  ((n  <loc  e')  \mwedge{}  e'  has*  New(n)  \mwedge{}  (e'  <  e))))))
4.  n  :  E(New)@i
5.  \mforall{}e:E
          (e  has*  New(n)
          {}\mRightarrow{}  (n  c\mleq{}  e
                \mwedge{}  ((\mneg{}(loc(e)  =  loc(n)))  {}\mRightarrow{}  (\mexists{}e':E(Send).  ((n  <loc  e')  \mwedge{}  e'  has*  New(n)  \mwedge{}  (e'  <  e))))))
6.  e  :  E@i
7.  e  has*  New(n)
{}\mRightarrow{}  (n  c\mleq{}  e  \mwedge{}  ((\mneg{}(loc(e)  =  loc(n)))  {}\mRightarrow{}  (\mexists{}e':E(Send).  ((n  <loc  e')  \mwedge{}  e'  has*  New(n)  \mwedge{}  (e'  <  e)))))
8.  loc(e)  =  loc(n)@i
9.  \mneg{}(New(n)  released  before  e)@i
10.  e'  :  E@i
11.  \mneg{}(loc(e')  =  loc(e))@i
12.  e'  has*  New(n)@i
13.  n  c\mleq{}  e'
14.  snd  :  E(Send)
15.  (n  <loc  snd)
16.  snd  has*  New(n)
17.  (snd  <  e')
\mvdash{}  (e  <  e')


By

---

Latex:
(Assert  \mkleeneopen{}e  \mleq{}loc  snd  \mkleeneclose{}\mcdot{}  THEN  Auto)

---

Home Index