---

Step * of Lemma dataflow-to-Process_wf

∀[A,B:Type]. ∀[F:dataflow(A;B)]. ∀[g:B ─→ LabeledDAG(Id × (Com(P.A) Process(P.A)))].
  (dataflow-to-Process(
   F;
   g) ∈ Process(P.A))
BY
{ (Auto
   THEN Unfold `dataflow-to-Process` 0
   THEN (InstLemma `rec-process_wf_Process` [⌈λ2P.dataflow(A;B)⌉]⋅ THENM BHyp (-1))
   THEN Try (QuickAuto)) }

1
.....wf..... 
1. A : Type
2. B : Type
3. F : dataflow(A;B)
4. g : B ─→ LabeledDAG(Id × (Com(P.A) Process(P.A)))
5. ∀[M:Type ─→ Type]
     (∀[s0:dataflow(A;B)]. ∀[next:∩T:{T:Type| Process(T.M[T]) ⊆r T} 
                                    (dataflow(A;B) ─→ M[T] ─→ (dataflow(A;B) × 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.dataflow(A;B)))
⊢ λs,m. let s',x = s(m) in <s', g x> ∈ ∩T:{T:Type| Process(T.A) ⊆r T} 
                                     (dataflow(A;B) ─→ A ─→ (dataflow(A;B) × LabeledDAG(Id × (Com(T.A) T))))

---

Latex:

---

Latex:
\mforall{}[A,B:Type].  \mforall{}[F:dataflow(A;B)].  \mforall{}[g:B  {}\mrightarrow{}  LabeledDAG(Id  \mtimes{}  (Com(P.A)  Process(P.A)))].
    (dataflow-to-Process(
      F;
      g)  \mmember{}  Process(P.A))


By

---

Latex:
(Auto
  THEN  Unfold  `dataflow-to-Process`  0
  THEN  (InstLemma  `rec-process\_wf\_Process`  [\mkleeneopen{}\mlambda{}\msubtwo{}P.dataflow(A;B)\mkleeneclose{}]\mcdot{}  THENM  BHyp  (-1))
  THEN  Try  (QuickAuto))

---

Home Index