---

Step * 1 of Lemma run-prior-state_wf


1. M : Type ─→ Type
2. S0 : System(P.M[P])
3. r : fulpRunType(P.M[P])
4. e1 : ℕ
5. e2 : Id
6. r ∈ pRunType(P.M[P])
7. v : (ℕ × Id) List@i
8. ¬(v = [] ∈ ((ℕ × Id) List))
9. mapfilter(λt.<t, e2>;λt.is-run-event(r;t;e2);[0, e1)) = v ∈ ((ℕ × Id) List)@i
10. λc.fst(c) = e2 ∈ component(P.M[P]) ─→ 𝔹
⊢ let t,x = last(v) 
  in let info,Cs,G = r t in 
     mapfilter(λc.(snd(c));λc.fst(c) = x;Cs) ∈ Process(P.M[P]) List
BY
{ (GenConclAtAddr [2;1] THEN D -2 THEN Reduce 0) }

1
1. M : Type ─→ Type
2. S0 : System(P.M[P])
3. r : fulpRunType(P.M[P])
4. e1 : ℕ
5. e2 : Id
6. r ∈ pRunType(P.M[P])
7. v : (ℕ × Id) List@i
8. ¬(v = [] ∈ ((ℕ × Id) List))
9. mapfilter(λt.<t, e2>;λt.is-run-event(r;t;e2);[0, e1)) = v ∈ ((ℕ × Id) List)@i
10. λc.fst(c) = e2 ∈ component(P.M[P]) ─→ 𝔹
11. v2 : ℕ@i
12. v3 : Id@i
13. last(v) = <v2, v3> ∈ (ℕ × Id)@i
⊢ let info,Cs,G = r v2 in 
  mapfilter(λc.(snd(c));λc.fst(c) = v3;Cs) ∈ Process(P.M[P]) List

---

Latex:

---

Latex:

1.  M  :  Type  {}\mrightarrow{}  Type
2.  S0  :  System(P.M[P])
3.  r  :  fulpRunType(P.M[P])
4.  e1  :  \mBbbN{}
5.  e2  :  Id
6.  r  \mmember{}  pRunType(P.M[P])
7.  v  :  (\mBbbN{}  \mtimes{}  Id)  List@i
8.  \mneg{}(v  =  [])
9.  mapfilter(\mlambda{}t.<t,  e2>\mlambda{}t.is-run-event(r;t;e2);[0,  e1))  =  v@i
10.  \mlambda{}c.fst(c)  =  e2  \mmember{}  component(P.M[P])  {}\mrightarrow{}  \mBbbB{}
\mvdash{}  let  t,x  =  last(v) 
    in  let  info,Cs,G  =  r  t  in 
          mapfilter(\mlambda{}c.(snd(c));\mlambda{}c.fst(c)  =  x;Cs)  \mmember{}  Process(P.M[P])  List


By

---

Latex:
(GenConclAtAddr  [2;1]  THEN  D  -2  THEN  Reduce  0)

---

Home Index