---

Step * of Lemma hdf-parallel-halted

∀[A,B:Type].
  ∀[inputs:A List]. ∀[X,Y:hdataflow(A;B)].
    hdf-halted(X || Y*(inputs)) = hdf-halted(X*(inputs)) ∧b hdf-halted(Y*(inputs)) 
  supposing valueall-type(B)
BY
{ (InductionOnList
   THEN Auto
   THEN Reduce 0
   THEN Try (((RWO "hdf-parallel-ap" 0 THENM Reduce 0) THEN Auto))
   THEN Unfold `hdf-parallel` 0
   THEN RecUnfold `mk-hdf` 0
   THEN Reduce 0
   THEN RepeatFor 2 (AutoSplit)) }

---

Latex:


\mforall{}[A,B:Type].
    \mforall{}[inputs:A  List].  \mforall{}[X,Y:hdataflow(A;B)].
        hdf-halted(X  ||  Y*(inputs))  =  hdf-halted(X*(inputs))  \mwedge{}\msubb{}  hdf-halted(Y*(inputs)) 
    supposing  valueall-type(B)


By

(InductionOnList
  THEN  Auto
  THEN  Reduce  0
  THEN  Try  (((RWO  "hdf-parallel-ap"  0  THENM  Reduce  0)  THEN  Auto))
  THEN  Unfold  `hdf-parallel`  0
  THEN  RecUnfold  `mk-hdf`  0
  THEN  Reduce  0
  THEN  RepeatFor  2  (AutoSplit))

---

Home Index