---

Step * of Lemma rec-dataflow_wf2

∀[S,A,B:Type ─→ Type].
  (let Proc = corec(P.A[P] ─→ (P × B[P])) in
       ∀s0:S[Proc]. ∀next:∩T:{T:Type| Proc ⊆r T} . (S[A[T] ─→ (T × B[T])] ─→ A[T] ─→ (S[T] × B[T])).
         (rec-dataflow(s0;s,m.next[s;m]) ∈ Proc)) supposing 
     (Continuous+(T.B[T]) and 
     Continuous+(T.A[T]) and 
     Continuous+(T.S[T]))
BY
{ (Auto
   THEN RepUR ``let`` 0
   THEN Auto
   THEN Unfold `rec-dataflow` 0
   THEN Using [`A',⌈S⌉] (BLemma `fix_wf_corec_parameter3`)⋅
   THEN Auto
   THEN Isect2CD
   THEN Auto) }

---

Latex:

---

Latex:
\mforall{}[S,A,B:Type  {}\mrightarrow{}  Type].
    (let  Proc  =  corec(P.A[P]  {}\mrightarrow{}  (P  \mtimes{}  B[P]))  in
              \mforall{}s0:S[Proc].  \mforall{}next:\mcap{}T:\{T:Type|  Proc  \msubseteq{}r  T\}  .  (S[A[T]  {}\mrightarrow{}  (T  \mtimes{}  B[T])]  {}\mrightarrow{}  A[T]  {}\mrightarrow{}  (S[T]  \mtimes{}  B[T])).
                  (rec-dataflow(s0;s,m.next[s;m])  \mmember{}  Proc))  supposing 
          (Continuous+(T.B[T])  and 
          Continuous+(T.A[T])  and 
          Continuous+(T.S[T]))


By

---

Latex:
(Auto
  THEN  RepUR  ``let``  0
  THEN  Auto
  THEN  Unfold  `rec-dataflow`  0
  THEN  Using  [`A',\mkleeneopen{}S\mkleeneclose{}]  (BLemma  `fix\_wf\_corec\_parameter3`)\mcdot{}
  THEN  Auto
  THEN  Isect2CD
  THEN  Auto)

---

Home Index