---

Step * of Lemma ses-nonce-release

∀s:SES. (PropertyN ⇒ PropertyNR)
BY
{ (Auto
   THEN All (Unfolds ``ses-nonce ses-NR``)
   THEN ((ParallelLast' THENA Auto) THEN ParallelLast THEN Try (ParallelLast))
   THEN Auto
   THEN Try ((InstHyp [⌈e'⌉] 5⋅
              THEN Auto
              THEN (D -1 THENA (ParallelOp -3 THEN Auto))
              THEN (ExRepD THEN RenameVar `snd' (-4))⋅))) }

1
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')

---

Latex:

---

Latex:
\mforall{}s:SES.  (PropertyN  {}\mRightarrow{}  PropertyNR)


By

---

Latex:
(Auto
  THEN  All  (Unfolds  ``ses-nonce  ses-NR``)
  THEN  ((ParallelLast'  THENA  Auto)  THEN  ParallelLast  THEN  Try  (ParallelLast))
  THEN  Auto
  THEN  Try  ((InstHyp  [\mkleeneopen{}e'\mkleeneclose{}]  5\mcdot{}
                        THEN  Auto
                        THEN  (D  -1  THENA  (ParallelOp  -3  THEN  Auto))
                        THEN  (ExRepD  THEN  RenameVar  `snd'  (-4))\mcdot{})))

---

Home Index