---

Step * of Lemma ses-legal-thread-has*-signature

∀s:SES
  (SecurityAxioms
  ⇒ (∀es:EO+(Info). ∀A:Id. ∀thr:Thread.
        ((Legal(thr)@A ∧ noncelike-signatures(s;es;thr))
        ⇒ (∀sg:E(Sign). ∀e:Act.
              (e ∈ thr
              ⇒ e has* signature(sg)
              ⇒ (∃e':E. ((e' <loc e) ∧ Action(e') ∧ e' has* signature(sg) ∧ e' ∈ thr)) ∨ (e = sg ∈ E) 
                 supposing ∀e':E
                             ((e' < e)
                             ⇒ Action(e')
                             ⇒ e' has* signature(sg)
                             ⇒ ((loc(e') = A ∈ Id) ∧ (¬↑e' ∈b Send))))))))
BY
{ (RepeatFor 8 ((D 0 THENA Auto))
   THEN (Assert Action(e) BY
               ((D -1 THEN Unhide) THEN Auto))
   THEN D -2
   THEN Thin (-2)
   THEN Auto
   THEN RenameVar `a' (-5)
   THEN Assert ⌜∀e:E
                  (Action(e)
                  ⇒ e ∈ thr
                  ⇒ e ≤loc a 
                  ⇒ (∀m:ℕ. ∀e':E.
                        ((e' ->>^m e)
                        ⇒ (e' has signature(sg))
                        ⇒ ((∃e':E. ((e' <loc e) ∧ Action(e') ∧ e' has* signature(sg) ∧ e' ∈ thr)) ∨ (e = sg ∈ E)))))⌝
   ⋅) }

1
.....assertion..... 
1. s : SES@i'
2. SecurityAxioms@i'
3. es : EO+(Info)@i'
4. A : Id@i
5. thr : Thread@i
6. Legal(thr)@A@i
7. noncelike-signatures(s;es;thr)@i
8. sg : E(Sign)@i
9. a : E@i
10. Action(a)
11. a ∈ thr@i
12. a has* signature(sg)@i
13. ∀e':E. ((e' < a) ⇒ Action(e') ⇒ e' has* signature(sg) ⇒ ((loc(e') = A ∈ Id) ∧ (¬↑e' ∈b Send)))
⊢ ∀e:E
    (Action(e)
    ⇒ e ∈ thr
    ⇒ e ≤loc a 
    ⇒ (∀m:ℕ. ∀e':E.
          ((e' ->>^m e)
          ⇒ (e' has signature(sg))
          ⇒ ((∃e':E. ((e' <loc e) ∧ Action(e') ∧ e' has* signature(sg) ∧ e' ∈ thr)) ∨ (e = sg ∈ E)))))

2
1. s : SES@i'
2. SecurityAxioms@i'
3. es : EO+(Info)@i'
4. A : Id@i
5. thr : Thread@i
6. Legal(thr)@A@i
7. noncelike-signatures(s;es;thr)@i
8. sg : E(Sign)@i
9. a : E@i
10. Action(a)
11. a ∈ thr@i
12. a has* signature(sg)@i
13. ∀e':E. ((e' < a) ⇒ Action(e') ⇒ e' has* signature(sg) ⇒ ((loc(e') = A ∈ Id) ∧ (¬↑e' ∈b Send)))
14. ∀e:E
      (Action(e)
      ⇒ e ∈ thr
      ⇒ e ≤loc a 
      ⇒ (∀m:ℕ. ∀e':E.
            ((e' ->>^m e)
            ⇒ (e' has signature(sg))
            ⇒ ((∃e':E. ((e' <loc e) ∧ Action(e') ∧ e' has* signature(sg) ∧ e' ∈ thr)) ∨ (e = sg ∈ E)))))
⊢ (∃e':E. ((e' <loc a) ∧ Action(e') ∧ e' has* signature(sg) ∧ e' ∈ thr)) ∨ (a = sg ∈ E)

---

Latex:

---

Latex:
\mforall{}s:SES
    (SecurityAxioms
    {}\mRightarrow{}  (\mforall{}es:EO+(Info).  \mforall{}A:Id.  \mforall{}thr:Thread.
                ((Legal(thr)@A  \mwedge{}  noncelike-signatures(s;es;thr))
                {}\mRightarrow{}  (\mforall{}sg:E(Sign).  \mforall{}e:Act.
                            (e  \mmember{}  thr
                            {}\mRightarrow{}  e  has*  signature(sg)
                            {}\mRightarrow{}  (\mexists{}e':E.  ((e'  <loc  e)  \mwedge{}  Action(e')  \mwedge{}  e'  has*  signature(sg)  \mwedge{}  e'  \mmember{}  thr))  \mvee{}  (e  =  sg) 
                                  supposing  \mforall{}e':E
                                                          ((e'  <  e)
                                                          {}\mRightarrow{}  Action(e')
                                                          {}\mRightarrow{}  e'  has*  signature(sg)
                                                          {}\mRightarrow{}  ((loc(e')  =  A)  \mwedge{}  (\mneg{}\muparrow{}e'  \mmember{}\msubb{}  Send))))))))


By

---

Latex:
(RepeatFor  8  ((D  0  THENA  Auto))
  THEN  (Assert  Action(e)  BY
                          ((D  -1  THEN  Unhide)  THEN  Auto))
  THEN  D  -2
  THEN  Thin  (-2)
  THEN  Auto
  THEN  RenameVar  `a'  (-5)
  THEN  Assert  \mkleeneopen{}\mforall{}e:E
                                (Action(e)
                                {}\mRightarrow{}  e  \mmember{}  thr
                                {}\mRightarrow{}  e  \mleq{}loc  a 
                                {}\mRightarrow{}  (\mforall{}m:\mBbbN{}.  \mforall{}e':E.
                                            ((e'  rel\_exp(E;  ->>  m)  e)
                                            {}\mRightarrow{}  (e'  has  signature(sg))
                                            {}\mRightarrow{}  ((\mexists{}e':E.  ((e'  <loc  e)  \mwedge{}  Action(e')  \mwedge{}  e'  has*  signature(sg)  \mwedge{}  e'  \mmember{}  thr))
                                                  \mvee{}  (e  =  sg)))))\mkleeneclose{}\mcdot{})

---

Home Index