---

Step * of Lemma rec-process_wf_pi_simple_state

∀[S:Type]. ∀[s0:S]. ∀[next:⋂T:{T:Type| pi-process() ⊆r T} . (S ⟶ piM(T) ⟶ (S × LabeledDAG(Id × (Com(T.piM(T)) T))))].
  (RecProcess(s0;s,m.next[s;m]) ∈ pi-process())
BY
{ (Auto THEN Using [`S',⌜λ2T.S⌝] (BLemma `rec-process_wf_pi`)⋅ THEN Auto) }

---

Latex:

---

Latex:
\mforall{}[S:Type].  \mforall{}[s0:S].  \mforall{}[next:\mcap{}T:\{T:Type|  pi-process()  \msubseteq{}r  T\} 
                                                          (S  {}\mrightarrow{}  piM(T)  {}\mrightarrow{}  (S  \mtimes{}  LabeledDAG(Id  \mtimes{}  (Com(T.piM(T))  T))))].
    (RecProcess(s0;s,m.next[s;m])  \mmember{}  pi-process())


By

---

Latex:
(Auto  THEN  Using  [`S',\mkleeneopen{}\mlambda{}\msubtwo{}T.S\mkleeneclose{}]  (BLemma  `rec-process\_wf\_pi`)\mcdot{}  THEN  Auto)

---

Home Index