---

Step * of Lemma run-prior-state-property

∀[M:Type ⟶ Type]
  ∀S0:System(P.M[P]). ∀r:fulpRunType(P.M[P]).
    ∀n:ℕ. ∀x:Id.
      ∃m:ℕn
       ((run-prior-state(S0;r;<n, 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..n-}. (¬↑is-run-event(r;t;x)))) 
      supposing 0 < n 
    supposing (r 0) = <inr ⋅ , S0> ∈ (ℤ × Id × Id × pMsg(P.M[P])? × System(P.M[P]))
BY
{ ((CompleteInductionOnNat THEN Auto)
   THEN (Assert r ∈ pRunType(P.M[P]) BY
               (DoSubsume THEN Auto))
   THEN Try (Complete (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])
⊢ ∃m:ℕn
   ((run-prior-state(S0;r;<n, 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..n-}. (¬↑is-run-event(r;t;x))))

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@i
7. x : Id@i
8. 0 < n1@i
9. m : ℕn1@i
10. 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

3
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

---

Latex:

---

Latex:
\mforall{}[M:Type  {}\mrightarrow{}  Type]
    \mforall{}S0:System(P.M[P]).  \mforall{}r:fulpRunType(P.M[P]).
        \mforall{}n:\mBbbN{}.  \mforall{}x:Id.
            \mexists{}m:\mBbbN{}n
              ((run-prior-state(S0;r;<n,  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..n\msupminus{}\}.  (\mneg{}\muparrow{}is-run-event(r;t;x)))) 
            supposing  0  <  n 
        supposing  (r  0)  =  <inr  \mcdot{}  ,  S0>


By

---

Latex:
((CompleteInductionOnNat  THEN  Auto)
  THEN  (Assert  r  \mmember{}  pRunType(P.M[P])  BY
                          (DoSubsume  THEN  Auto))
  THEN  Try  (Complete  (Auto)))

---

Home Index