---

Step * of Lemma iterate-rec-dataflow

∀[S,A,B:Type]. ∀[next:S ─→ A ─→ (S × B)]. ∀[L:A List]. ∀[s0:S].
  (rec-dataflow(s0;s,m.next[s;m])*(L) ~ rec-dataflow(rec-dataflow-state(s0;s,m.next[s;m];L);s,m.next[s;m]))
BY
{ (Unfold `rec-dataflow-state` 0
   THEN InductionOnList
   THEN Reduce 0
   THEN Auto
   THEN GenConclAtAddr [1;1;1;1]
   THEN D -2
   THEN Reduce 0
   THEN BackThruSomeHyp) }

---

Latex:

---

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


By

---

Latex:
(Unfold  `rec-dataflow-state`  0
  THEN  InductionOnList
  THEN  Reduce  0
  THEN  Auto
  THEN  GenConclAtAddr  [1;1;1;1]
  THEN  D  -2
  THEN  Reduce  0
  THEN  BackThruSomeHyp)

---

Home Index