---

Step * of Lemma rec-process_wf_pi

∀[S:Type ─→ Type]
  ∀[s0:S[pi-process()]]. ∀[next:∩T:{T:Type| pi-process() ⊆r T} 
                                  (S[piM(T) ─→ (T × LabeledDAG(Id × (Com(T.piM(T)) T)))]
                                  ─→ piM(T)
                                  ─→ (S[T] × LabeledDAG(Id × (Com(T.piM(T)) T))))].
    (RecProcess(s0;s,m.next[s;m]) ∈ pi-process()) 
  supposing Continuous+(T.S[T])
BY
{ (Unfold `pi-process` 0 THEN Auto THEN Using [`S',⌈S⌉] (BLemma `rec-process_wf_Process`)⋅ THEN Auto) }

---

Latex:

---

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


By

---

Latex:
(Unfold  `pi-process`  0  THEN  Auto  THEN  Using  [`S',\mkleeneopen{}S\mkleeneclose{}]  (BLemma  `rec-process\_wf\_Process`)\mcdot{}  THEN  Auto)

---

Home Index