---

Step * 1 of Lemma ses-info-flow-exp_functionality


1. s : SES@i'
2. ActionsDisjoint@i'
3. es : EO+(Info)@i'
4. x : E@i
5. y : E@i
6. same-action(x;y)@i
7. e : E@i
8. n : ℕ+@i
9. z : E
10. 0 < n c∧ ((e ->>^n - 1 z) ∧ (z ->> x))
11. 0 < n
12. e ->>^n - 1 z
⊢ z ->> y
BY
{ (RepeatFor 2 (D -3) THEN FLemma `ses-info-flow_functionality` [6;-3] THEN Auto) }

---

Latex:

---

Latex:

1.  s  :  SES@i'
2.  ActionsDisjoint@i'
3.  es  :  EO+(Info)@i'
4.  x  :  E@i
5.  y  :  E@i
6.  same-action(x;y)@i
7.  e  :  E@i
8.  n  :  \mBbbN{}\msupplus{}@i
9.  z  :  E
10.  0  <  n  c\mwedge{}  ((e  rel\_exp(E;  ->>  n  -  1)  z)  \mwedge{}  (z  ->>  x))
11.  0  <  n
12.  e  rel\_exp(E;  ->>  n  -  1)  z
\mvdash{}  z  ->>  y


By

---

Latex:
(RepeatFor  2  (D  -3)  THEN  FLemma  `ses-info-flow\_functionality`  [6;-3]  THEN  Auto)

---

Home Index