---

Step * 2 2 2 of Lemma ses-flow_wf


1. s : SES
2. es : EO+(Info)
3. ∀n:ℕ. ∀e1,e2:E.  (((es-rank(es;e2) - es-rank(es;e1)) ≤ n) ⇒ (∀a:Atom1. (ses-flow(s;es;a;e1;e2) ∈ Type)))
4. e1 : E
5. e2 : E
6. a : Atom1
7. snd : E(Send)@i
8. rcv : E(Rcv)@i
9. e1 c≤ snd
10. rcv = e2 ∈ E
11. (snd < rcv)
12. Send(snd) = Rcv(rcv) ∈ SecurityData
13. ses-flow(s;es;a;e1;snd)
⊢ ses-flow(s;es;a;rcv;e2) ∈ Type
BY
{ skip{RecUnfold `ses-flow` 0} }

1
1. s : SES
2. es : EO+(Info)
3. ∀n:ℕ. ∀e1,e2:E.  (((es-rank(es;e2) - es-rank(es;e1)) ≤ n) ⇒ (∀a:Atom1. (ses-flow(s;es;a;e1;e2) ∈ Type)))
4. e1 : E
5. e2 : E
6. a : Atom1
7. snd : E(Send)@i
8. rcv : E(Rcv)@i
9. e1 c≤ snd
10. rcv = e2 ∈ E
11. (snd < rcv)
12. Send(snd) = Rcv(rcv) ∈ SecurityData
13. ses-flow(s;es;a;e1;snd)
⊢ ses-flow(s;es;a;rcv;e2) ∈ Type

---

Latex:

---

Latex:

1.  s  :  SES
2.  es  :  EO+(Info)
3.  \mforall{}n:\mBbbN{}.  \mforall{}e1,e2:E.
          (((es-rank(es;e2)  -  es-rank(es;e1))  \mleq{}  n)  {}\mRightarrow{}  (\mforall{}a:Atom1.  (ses-flow(s;es;a;e1;e2)  \mmember{}  Type)))
4.  e1  :  E
5.  e2  :  E
6.  a  :  Atom1
7.  snd  :  E(Send)@i
8.  rcv  :  E(Rcv)@i
9.  e1  c\mleq{}  snd
10.  rcv  =  e2
11.  (snd  <  rcv)
12.  Send(snd)  =  Rcv(rcv)
13.  ses-flow(s;es;a;e1;snd)
\mvdash{}  ses-flow(s;es;a;rcv;e2)  \mmember{}  Type


By

---

Latex:
skip\{RecUnfold  `ses-flow`  0\}

---

Home Index