---

Step * 3 of Lemma run-prior-state-property


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

---

Latex:

---

Latex:

1.  M  :  Type  {}\mrightarrow{}  Type
2.  S0  :  System(P.M[P])@i
3.  r  :  fulpRunType(P.M[P])@i
4.  (r  0)  =  <inr  \mcdot{}  ,  S0>
5.  n  :  \mBbbN{}@i
6.  \mforall{}i:\mBbbN{}
          ((\mforall{}n1:\mBbbN{}i.  \mforall{}x:Id.
                  \mexists{}m:\mBbbN{}n1
                    ((run-prior-state(S0;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)
          {}\mRightarrow{}  (\mforall{}x:Id
                      \mexists{}m:\mBbbN{}i
                        ((run-prior-state(S0;r;<i,  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..i\msupminus{}\}.  (\mneg{}\muparrow{}is-run-event(r;t;x)))) 
                      supposing  0  <  i))
7.  n1  :  \mBbbN{}@i
8.  x  :  Id@i
9.  0  <  n1@i
10.  m  :  \mBbbN{}n1@i
11.  r  \mmember{}  pRunType(P.M[P])
\mvdash{}  let  info,Cs,G  =  r  m  in 
    mapfilter(\mlambda{}c.(snd(c));\mlambda{}c.fst(c)  =  x;Cs)  \mmember{}  Process(P.M[P])  List


By

---

Latex:
(Thin  (-1)  THEN  (Assert  \mlambda{}c.fst(c)  =  x  \mmember{}  component(P.M[P])  {}\mrightarrow{}  \mBbbB{}  BY  Auto)  THEN  Auto)

---

Home Index