---

Step * of Lemma rec-process_wf_Process

∀[S,M:Type ⟶ Type].
  (∀[s0:S[Process(T.M[T])]]. ∀[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))))].
     (RecProcess(s0;s,m.next[s;m]) ∈ Process(T.M[T]))) supposing 
     (Continuous+(T.M[T]) and 
     Continuous+(T.S[T]))
BY
{ (Auto
   THEN InstLemma `rec-process_wf` [⌜S⌝;⌜M⌝;⌜λ2T.LabeledDAG(Id × (Com(T.M[T]) T))⌝;⌜s0⌝;⌜next⌝]⋅
   THEN All (Fold `Process`)
   THEN Auto) }

1
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)

---

Latex:

---

Latex:
\mforall{}[S,M:Type  {}\mrightarrow{}  Type].
    (\mforall{}[s0:S[Process(T.M[T])]].  \mforall{}[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))))].
          (RecProcess(s0;s,m.next[s;m])  \mmember{}  Process(T.M[T])))  supposing 
          (Continuous+(T.M[T])  and 
          Continuous+(T.S[T]))


By

---

Latex:
(Auto
  THEN  InstLemma  `rec-process\_wf`  [\mkleeneopen{}S\mkleeneclose{};\mkleeneopen{}M\mkleeneclose{};\mkleeneopen{}\mlambda{}\msubtwo{}T.LabeledDAG(Id  \mtimes{}  (Com(T.M[T])  T))\mkleeneclose{};\mkleeneopen{}s0\mkleeneclose{};\mkleeneopen{}next\mkleeneclose{}]\mcdot{}
  THEN  All  (Fold  `Process`)
  THEN  Auto)

---

Home Index