---

Step * 1 of Lemma rec-process_wf_Process


1. S : Type ─→ Type
2. M : Type ─→ Type
3. Continuous+(T.S[T])
4. Continuous+(T.M[T])
5. s0 : S[Process(T.M[T])]
6. next : ∩T:{T:Type| Process(T.M[T]) ⊆r T} 
            (S[M[T] ─→ (T × LabeledDAG(Id × (Com(T.M[T]) T)))] ─→ M[T] ─→ (S[T] × LabeledDAG(Id × (Com(T.M[T]) T))))
⊢ Continuous+(T.Com(T.M[T]) T)
BY
{ (RepUR ``Com tagged+`` 0 THEN Auto)⋅ }

---

Latex:

---

Latex:

1.  S  :  Type  {}\mrightarrow{}  Type
2.  M  :  Type  {}\mrightarrow{}  Type
3.  Continuous+(T.S[T])
4.  Continuous+(T.M[T])
5.  s0  :  S[Process(T.M[T])]
6.  next  :  \mcap{}T:\{T:Type|  Process(T.M[T])  \msubseteq{}r  T\} 
                        (S[M[T]  {}\mrightarrow{}  (T  \mtimes{}  LabeledDAG(Id  \mtimes{}  (Com(T.M[T])  T)))]
                        {}\mrightarrow{}  M[T]
                        {}\mrightarrow{}  (S[T]  \mtimes{}  LabeledDAG(Id  \mtimes{}  (Com(T.M[T])  T))))
\mvdash{}  Continuous+(T.Com(T.M[T])  T)


By

---

Latex:
(RepUR  ``Com  tagged+``  0  THEN  Auto)\mcdot{}

---

Home Index