---

Step * 1 1 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. ∀n1:ℕn. ∀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.M[P]\000C) List))
      ∧ (∀t:{m + 1..n1-}. (¬↑is-run-event(r;t;x)))) 
     supposing 0 < n1@i
7. x : Id@i
8. 0 < n
9. r ∈ pRunType(P.M[P])
10. n = 1 ∈ ℤ
⊢ ∃m:ℕ1
   ((run-prior-state(S0;r;<1, x>) = let info,Cs,G = r m in mapfilter(λc.(snd(c));λc.fst(c) = x;Cs) ∈ (Process(P.M[P]) Li\000Cst))
   ∧ (∀t:{m + 1..1-}. (¬↑is-run-event(r;t;x))))
BY
{ (With ⌈0⌉ (D 0)⋅ THEN Auto) }

1
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. ∀n1:ℕn. ∀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.M[P]\000C) List))
      ∧ (∀t:{m + 1..n1-}. (¬↑is-run-event(r;t;x)))) 
     supposing 0 < n1@i
7. x : Id@i
8. 0 < n
9. r ∈ pRunType(P.M[P])
10. n = 1 ∈ ℤ
⊢ run-prior-state(S0;r;<1, x>) = let info,Cs,G = r 0 in mapfilter(λc.(snd(c));λc.fst(c) = x;Cs) ∈ (Process(P.M[P]) List)

2
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. ∀n1:ℕn. ∀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.M[P]\000C) List))
      ∧ (∀t:{m + 1..n1-}. (¬↑is-run-event(r;t;x)))) 
     supposing 0 < n1@i
7. x : Id@i
8. 0 < n
9. r ∈ pRunType(P.M[P])
10. n = 1 ∈ ℤ
11. m : ℕ1
⊢ let info,Cs,G = r m in 
  mapfilter(λc.(snd(c));λc.fst(c) = x;Cs) ∈ Process(P.M[P]) List

---

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{}n1:\mBbbN{}n.  \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)  =  x;C\000Cs))
            \mwedge{}  (\mforall{}t:\{m  +  1..n1\msupminus{}\}.  (\mneg{}\muparrow{}is-run-event(r;t;x)))) 
          supposing  0  <  n1@i
7.  x  :  Id@i
8.  0  <  n
9.  r  \mmember{}  pRunType(P.M[P])
10.  n  =  1
\mvdash{}  \mexists{}m:\mBbbN{}1
      ((run-prior-state(S0;r;ə,  x>)  =  let  info,Cs,G  =  r  m  in  mapfilter(\mlambda{}c.(snd(c));\mlambda{}c.fst(c)  =  x;Cs))
      \mwedge{}  (\mforall{}t:\{m  +  1..1\msupminus{}\}.  (\mneg{}\muparrow{}is-run-event(r;t;x))))


By

---

Latex:
(With  \mkleeneopen{}0\mkleeneclose{}  (D  0)\mcdot{}  THEN  Auto)

---

Home Index