Step
*
1
of Lemma
run-event-state-when_wf
1. M : Type ─→ Type
2. r : fulpRunType(P.M[P])
3. e : ℕ+ × Id
⊢ run-event-state-when(r;e) ∈ Process(P.M[P]) List
BY
{ (D -1
THEN Unfold `run-event-state-when` 0
THEN Reduce 0
THEN (Assert λc.fst(c) = e2 ∈ component(P.M[P]) ─→ 𝔹 BY
Auto)
THEN Auto) }
Latex:
Latex:
1. M : Type {}\mrightarrow{} Type
2. r : fulpRunType(P.M[P])
3. e : \mBbbN{}\msupplus{} \mtimes{} Id
\mvdash{} run-event-state-when(r;e) \mmember{} Process(P.M[P]) List
By
Latex:
(D -1
THEN Unfold `run-event-state-when` 0
THEN Reduce 0
THEN (Assert \mlambda{}c.fst(c) = e2 \mmember{} component(P.M[P]) {}\mrightarrow{} \mBbbB{} BY
Auto)
THEN Auto)
Home
Index