---

Step * of Lemma rec-dataflow_wf

∀[S,A,B:Type]. ∀[s0:S]. ∀[next:S ─→ A ─→ (S × B)].  (rec-dataflow(s0;s,m.next[s;m]) ∈ dataflow(A;B))
BY
{ (Unfold `dataflow` 0
   THEN (ProveWfLemma
         THEN (MoveToConcl (-3)
               THEN NatInd (-1)
               THEN Reduce 0
               THEN Auto
               THEN RW (SweepUpC UnrollRecursionC) 0
               THEN Reduce 0
               THEN (RWO "primrec-unroll" 0 THENA Auto)
               THEN AutoSplit)⋅
         )⋅
   ) }

---

Latex:

---

Latex:
\mforall{}[S,A,B:Type].  \mforall{}[s0:S].  \mforall{}[next:S  {}\mrightarrow{}  A  {}\mrightarrow{}  (S  \mtimes{}  B)].    (rec-dataflow(s0;s,m.next[s;m])  \mmember{}  dataflow(A;B))


By

---

Latex:
(Unfold  `dataflow`  0
  THEN  (ProveWfLemma
              THEN  (MoveToConcl  (-3)
                          THEN  NatInd  (-1)
                          THEN  Reduce  0
                          THEN  Auto
                          THEN  RW  (SweepUpC  UnrollRecursionC)  0
                          THEN  Reduce  0
                          THEN  (RWO  "primrec-unroll"  0  THENA  Auto)
                          THEN  AutoSplit)\mcdot{}
              )\mcdot{}
  )

---

Home Index