---

Step * of Lemma ses-info-flow-exp_functionality

∀s:SES
  (ActionsDisjoint ⇒ (∀es:EO+(Info). ∀x,y:E.  (same-action(x;y) ⇒ (∀e:E. ∀n:ℕ+.  ((e ->>^n x) ⇒ (e ->>^n y))))))
BY
{ (Auto
   THEN ((RWO "rel_exp_iff" (-1) THENA Auto) THEN D -1 THEN Auto)
   THEN (RWO "rel_exp_iff" 0 THENA Auto)
   THEN OrLeft
   THEN Auto
   THEN All Reduce
   THEN ParallelLast
   THEN Auto) }

1
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

---

Latex:

---

Latex:
\mforall{}s:SES
    (ActionsDisjoint
    {}\mRightarrow{}  (\mforall{}es:EO+(Info).  \mforall{}x,y:E.
                (same-action(x;y)  {}\mRightarrow{}  (\mforall{}e:E.  \mforall{}n:\mBbbN{}\msupplus{}.    ((e  ->>\^{}n  x)  {}\mRightarrow{}  (e  ->>\^{}n  y))))))


By

---

Latex:
(Auto
  THEN  ((RWO  "rel\_exp\_iff"  (-1)  THENA  Auto)  THEN  D  -1  THEN  Auto)
  THEN  (RWO  "rel\_exp\_iff"  0  THENA  Auto)
  THEN  OrLeft
  THEN  Auto
  THEN  All  Reduce
  THEN  ParallelLast
  THEN  Auto)

---

Home Index