---

Step * 1 of Lemma dataflow-to-Process_wf

.....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))))
BY
{ ((MemCD THENA Auto)
   THEN DVar `T'
   THEN (Assert (Com(P.A) Process(P.A)) ⊆r (Com(T.A) T) BY
               (BLemma `Com-subtype` THEN Auto))
   THEN Auto) }

---

Latex:

---

Latex:
.....wf..... 
1.  A  :  Type
2.  B  :  Type
3.  F  :  dataflow(A;B)
4.  g  :  B  {}\mrightarrow{}  LabeledDAG(Id  \mtimes{}  (Com(P.A)  Process(P.A)))
5.  \mforall{}[M:Type  {}\mrightarrow{}  Type]
          (\mforall{}[s0:dataflow(A;B)].  \mforall{}[next:\mcap{}T:\{T:Type|  Process(T.M[T])  \msubseteq{}r  T\} 
                                                                        (dataflow(A;B)
                                                                        {}\mrightarrow{}  M[T]
                                                                        {}\mrightarrow{}  (dataflow(A;B)  \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.dataflow(A;B)))
\mvdash{}  \mlambda{}s,m.  let  s',x  =  s(m)  in  <s',  g  x>  \mmember{}  \mcap{}T:\{T:Type|  Process(T.A)  \msubseteq{}r  T\} 
                                                                          (dataflow(A;B)
                                                                          {}\mrightarrow{}  A
                                                                          {}\mrightarrow{}  (dataflow(A;B)  \mtimes{}  LabeledDAG(Id  \mtimes{}  (Com(T.A)  T))))


By

---

Latex:
((MemCD  THENA  Auto)
  THEN  DVar  `T'
  THEN  (Assert  (Com(P.A)  Process(P.A))  \msubseteq{}r  (Com(T.A)  T)  BY
                          (BLemma  `Com-subtype`  THEN  Auto))
  THEN  Auto)

---

Home Index