---

Step * of Lemma hdf-sequence_wf

∀[A,B,C:Type]. ∀[X:hdataflow(A;B)]. ∀[Y:hdataflow(A;C)]. ∀[Z:hdataflow(A;B)].
  hdf-sequence(X;Y;Z) ∈ hdataflow(A;B) supposing valueall-type(B)
BY
{ ((UnivCD THENA Auto)
   THEN UnfoldAtAddr [2] 0
   THEN Using [`S',⌈hdataflow(A;B) × hdataflow(A;C) + hdataflow(A;B)⌉] MemCD⋅
   THEN Auto) }

---

Latex:


\mforall{}[A,B,C:Type].  \mforall{}[X:hdataflow(A;B)].  \mforall{}[Y:hdataflow(A;C)].  \mforall{}[Z:hdataflow(A;B)].
    hdf-sequence(X;Y;Z)  \mmember{}  hdataflow(A;B)  supposing  valueall-type(B)


By

((UnivCD  THENA  Auto)
  THEN  UnfoldAtAddr  [2]  0
  THEN  Using  [`S',\mkleeneopen{}hdataflow(A;B)  \mtimes{}  hdataflow(A;C)  +  hdataflow(A;B)\mkleeneclose{}]  MemCD\mcdot{}
  THEN  Auto)

---

Home Index