Step
*
2
1
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 c≤ e2
11. (snd < rcv)
12. Send(snd) = Rcv(rcv) ∈ SecurityData
⊢ ses-flow(s;es;a;e1;snd) ∈ Type
BY
{ ((InstLemma `es-rank_le` [⌈es⌉;⌈e1⌉;⌈snd⌉]⋅ THENA Auto)
THEN InstHyp [⌈es-rank(es;snd) - es-rank(es;e1)⌉;⌈e1⌉;⌈snd⌉;⌈a⌉] 3⋅
THEN Auto) }
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 c\mleq{} e2
11. (snd < rcv)
12. Send(snd) = Rcv(rcv)
\mvdash{} ses-flow(s;es;a;e1;snd) \mmember{} Type
By
Latex:
((InstLemma `es-rank\_le` [\mkleeneopen{}es\mkleeneclose{};\mkleeneopen{}e1\mkleeneclose{};\mkleeneopen{}snd\mkleeneclose{}]\mcdot{} THENA Auto)
THEN InstHyp [\mkleeneopen{}es-rank(es;snd) - es-rank(es;e1)\mkleeneclose{};\mkleeneopen{}e1\mkleeneclose{};\mkleeneopen{}snd\mkleeneclose{};\mkleeneopen{}a\mkleeneclose{}] 3\mcdot{}
THEN Auto)
Home
Index