Step
*
1
1
of Lemma
first-choosable_wf
.....wf.....
1. M : Type ─→ Type
2. t : ℕ+
3. r : ℕt ─→ (ℤ × Id × Id × pMsg(P.M[P])? × System(P.M[P]))
⊢ snd(run-system(r;t)) ∈ LabeledGraph(pInTransit(P.M[P]))
BY
{ (Unfold `run-system` 0 THEN (GenConclAtAddr [2;1;1] THEN D -2) THEN Reduce 0 THEN Auto) }
Latex:
Latex:
.....wf.....
1. M : Type {}\mrightarrow{} Type
2. t : \mBbbN{}\msupplus{}
3. r : \mBbbN{}t {}\mrightarrow{} (\mBbbZ{} \mtimes{} Id \mtimes{} Id \mtimes{} pMsg(P.M[P])? \mtimes{} System(P.M[P]))
\mvdash{} snd(run-system(r;t)) \mmember{} LabeledGraph(pInTransit(P.M[P]))
By
Latex:
(Unfold `run-system` 0 THEN (GenConclAtAddr [2;1;1] THEN D -2) THEN Reduce 0 THEN Auto)
Home
Index