---

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

.....subterm..... T:t
3:n
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. ¬↑is-run-event(r;n - 1;x)
12. m : ℕn - 1
13. ∀t:{m + 1..n - 1-}. (¬↑is-run-event(r;t;x))
14. run-prior-state(S0;r;<n - 1, x>) = let info,Cs,G = r m in mapfilter(λc.(snd(c));λc.fst(c) = x;Cs) ∈ (Process(P.M[P])\000C List)
15. x@0 : Unit
16. run-event-local-pred(r;<n, x>) = (inr x@0 ) ∈ (runEvents(r)?)
⊢ mapfilter(λc.(snd(c));λc.fst(c) = run-event-loc(<n, x>);fst(S0)) = mapfilter(λc.(snd(c));λc.fst(c) = run-event-loc(<n \000C- 1, x>);fst(S0)) ∈ (Process(P.M[P]) List)
BY
{ (D 2 THEN RepUR ``run-event-loc`` 0 THEN (Assert λc.fst(c) = x ∈ component(P.M[P]) ⟶ 𝔹 BY Auto)) }

1
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. r ∈ pRunType(P.M[P])
11. ¬(n = 1 ∈ ℤ)
12. ¬↑is-run-event(r;n - 1;x)
13. m : ℕn - 1
14. ∀t:{m + 1..n - 1-}. (¬↑is-run-event(r;t;x))
15. run-prior-state(<S1, S2>;r;<n - 1, x>) = let info,Cs,G = r m in mapfilter(λc.(snd(c));λc.fst(c) = x;Cs) ∈ (Process(P\000C.M[P]) List)
16. x@0 : Unit
17. run-event-local-pred(r;<n, x>) = (inr x@0 ) ∈ (runEvents(r)?)
18. λc.fst(c) = x ∈ component(P.M[P]) ⟶ 𝔹
⊢ mapfilter(λc.(snd(c));λc.fst(c) = x;S1) = mapfilter(λc.(snd(c));λc.fst(c) = x;S1) ∈ (Process(P.M[P]) List)

---

Latex:

---

Latex:
.....subterm.....  T:t
3:n
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.  \mneg{}(n  =  1)
11.  \mneg{}\muparrow{}is-run-event(r;n  -  1;x)
12.  m  :  \mBbbN{}n  -  1
13.  \mforall{}t:\{m  +  1..n  -  1\msupminus{}\}.  (\mneg{}\muparrow{}is-run-event(r;t;x))
14.  run-prior-state(S0;r;<n  -  1,  x>)  =  let  info,Cs,G  =  r  m  in  mapfilter(\mlambda{}c.(snd(c));\mlambda{}c.fst(c)  =  x;Cs\000C)
15.  x@0  :  Unit
16.  run-event-local-pred(r;<n,  x>)  =  (inr  x@0  )
\mvdash{}  mapfilter(\mlambda{}c.(snd(c));\mlambda{}c.fst(c)  =  run-event-loc(<n,  x>);fst(S0))
=  mapfilter(\mlambda{}c.(snd(c));\mlambda{}c.fst(c)  =  run-event-loc(<n  -  1,  x>);fst(S0))


By

---

Latex:
(D  2  THEN  RepUR  ``run-event-loc``  0  THEN  (Assert  \mlambda{}c.fst(c)  =  x  \mmember{}  component(P.M[P])  {}\mrightarrow{}  \mBbbB{}  BY  Auto))

---

Home Index