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


1. Type ⟶ Type
2. S0 System(P.M[P])@i
3. fulpRunType(P.M[P])@i
4. (r 0) = <inr ⋅ S0> ∈ (ℤ × Id × Id × pMsg(P.M[P])? × System(P.M[P]))
5. : ℕ@i
6. ∀n1:ℕn. ∀x:Id.
     ∃m:ℕn1
      ((run-prior-state(S0;r;<n1, x>let info,Cs,G 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. Id@i
8. 0 < n
9. r ∈ pRunType(P.M[P])
10. ¬(n 1 ∈ ℤ)
11. ↑is-run-event(r;n 1;x)
⊢ case inl <1, x>
 of inl(e') =>
 run-event-state(r;e')
 inr(x@0) =>
 mapfilter(λc.(snd(c));λc.fst(c) run-event-loc(<n, x>);fst(S0))
let info,Cs,G (n 1) in 
  mapfilter(λc.(snd(c));λc.fst(c) x;Cs)
∈ (Process(P.M[P]) List)
BY
(Reduce 0
   THEN RepUR ``run-event-state`` 0
   THEN Thin (-3)
   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{}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.  \muparrow{}is-run-event(r;n  -  1;x)
\mvdash{}  case  inl  <n  -  1,  x>
  of  inl(e')  =>
  run-event-state(r;e')
  |  inr(x@0)  =>
  mapfilter(\mlambda{}c.(snd(c));\mlambda{}c.fst(c)  =  run-event-loc(<n,  x>);fst(S0))
=  let  info,Cs,G  =  r  (n  -  1)  in 
    mapfilter(\mlambda{}c.(snd(c));\mlambda{}c.fst(c)  =  x;Cs)


By


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




Home Index