---

Step * 1 1 1 1 1 1 2 of Lemma run-prior-state-property


1. M : Type ─→ Type
2. S1 : component(P.M[P]) List@i
3. S2 : LabeledDAG(pInTransit(P.M[P]))@i
4. r : fulpRunType(P.M[P])@i
5. (r 0) = <inr ⋅ , S1, S2> ∈ (ℤ × Id × Id × pMsg(P.M[P])? × System(P.M[P]))
6. n : ℕ@i
7. ∀n1:ℕn. ∀x:Id.
     ∃m:ℕn1
      ((run-prior-state(<S1, S2>;r;<n1, x>) = let info,Cs,G = r m in mapfilter(λc.(snd(c));λc.fst(c) = x;Cs) ∈ (Process(\000CP.M[P]) List))
      ∧ (∀t:{m + 1..n1-}. (¬↑is-run-event(r;t;x)))) 
     supposing 0 < n1@i
8. x : Id@i
9. 0 < n
10. n = 1 ∈ ℤ
11. λc.fst(c) = x ∈ component(P.M[P]) ─→ 𝔹
12. ¬↑is-run-event(r;0;x)
⊢ run-prior-state(<S1, S2>;r;<1, x>) = mapfilter(λc.(snd(c));λc.fst(c) = x;S1) ∈ (Process(P.M[P]) List)
BY
{ (RepUR ``run-prior-state run-event-local-pred run-event-history`` 0
   THEN RepUR ``run-event-loc run-event-step let`` 0
   THEN RecUnfold `from-upto` 0
   THEN RepUR ``mapfilter`` 0
   THEN AutoSplit)⋅ }

1
.....wf..... 
1. M : Type ─→ Type
2. S1 : component(P.M[P]) List@i
3. S2 : LabeledDAG(pInTransit(P.M[P]))@i
4. r : fulpRunType(P.M[P])@i
5. (r 0) = <inr ⋅ , S1, S2> ∈ (ℤ × Id × Id × pMsg(P.M[P])? × System(P.M[P]))
6. n : ℕ@i
7. ∀n1:ℕn. ∀x:Id.
     ∃m:ℕn1
      ((run-prior-state(<S1, S2>;r;<n1, x>) = let info,Cs,G = r m in mapfilter(λc.(snd(c));λc.fst(c) = x;Cs) ∈ (Process(\000CP.M[P]) List))
      ∧ (∀t:{m + 1..n1-}. (¬↑is-run-event(r;t;x)))) 
     supposing 0 < n1@i
8. x : Id@i
9. 0 < n
10. n = 1 ∈ ℤ
11. λc.fst(c) = x ∈ component(P.M[P]) ─→ 𝔹
12. ¬↑is-run-event(r;0;x)
⊢ is-run-event(r;0;x) ∈ 𝔹

---

Latex:

---

Latex:

1.  M  :  Type  {}\mrightarrow{}  Type
2.  S1  :  component(P.M[P])  List@i
3.  S2  :  LabeledDAG(pInTransit(P.M[P]))@i
4.  r  :  fulpRunType(P.M[P])@i
5.  (r  0)  =  <inr  \mcdot{}  ,  S1,  S2>
6.  n  :  \mBbbN{}@i
7.  \mforall{}n1:\mBbbN{}n.  \mforall{}x:Id.
          \mexists{}m:\mBbbN{}n1
            ((run-prior-state(<S1,  S2>r;<n1,  x>)  =  let  info,Cs,G  =  r  m  in  mapfilter(\mlambda{}c.(snd(c));\mlambda{}c.fst(c)\000C  =  x;Cs))
            \mwedge{}  (\mforall{}t:\{m  +  1..n1\msupminus{}\}.  (\mneg{}\muparrow{}is-run-event(r;t;x)))) 
          supposing  0  <  n1@i
8.  x  :  Id@i
9.  0  <  n
10.  n  =  1
11.  \mlambda{}c.fst(c)  =  x  \mmember{}  component(P.M[P])  {}\mrightarrow{}  \mBbbB{}
12.  \mneg{}\muparrow{}is-run-event(r;0;x)
\mvdash{}  run-prior-state(<S1,  S2>r;ə,  x>)  =  mapfilter(\mlambda{}c.(snd(c));\mlambda{}c.fst(c)  =  x;S1)


By

---

Latex:
(RepUR  ``run-prior-state  run-event-local-pred  run-event-history``  0
  THEN  RepUR  ``run-event-loc  run-event-step  let``  0
  THEN  RecUnfold  `from-upto`  0
  THEN  RepUR  ``mapfilter``  0
  THEN  AutoSplit)\mcdot{}

---

Home Index