---

Step * of Lemma hdf-parallel-halt-right

∀[A,B:Type]. ∀[X:hdataflow(A;B)].  X || hdf-halt() = X ∈ hdataflow(A;B) supposing valueall-type(B)
BY
{ (Auto
   THEN (BLemma `hdataflow-equal` THENA Auto)
   THEN (D 0 THENA Auto)
   THEN MoveToConcl (-3)
   THEN ListInd (-1)
   THEN Reduce 0
   THEN (UnivCD THENA Auto)
   THEN RepUR ``hdf-parallel`` 0
   THEN RecUnfold `mk-hdf` 0
   THEN Reduce 0
   THEN AutoSplit
   THEN Try (((FLemma `hdf-halted-is-halt` [-1] THENA Auto)
              THEN HypSubst' (-1) 0
              THEN Reduce 0
              THEN Try ((RWO "iterate-hdf-halt" 0 THENA Auto))
              THEN Reduce 0
              THEN Auto))
   THEN Try ((RWO "hdf-out-run" 0 THEN Auto))
   THEN Auto
   THEN HDataflowHDAll
   THEN Try ((RWO "bag-append-empty" 0 THENA Auto))
   THEN Repeat (((RW (NthC 1 CallByValueallC) 0 THENA Complete (Auto)) THEN Reduce 0))
   THEN Try ((RWO "hdf-out-inl" 0 THEN Auto))
   THEN Try ((RWO "hdf-out-run" 0 THEN Auto))
   THEN Fold `hdf-parallel` 0
   THEN Try (Fold `hdf-halt` 0)
   THEN BackThruSomeHyp) }

---

Latex:


\mforall{}[A,B:Type].  \mforall{}[X:hdataflow(A;B)].    X  ||  hdf-halt()  =  X  supposing  valueall-type(B)


By

(Auto
  THEN  (BLemma  `hdataflow-equal`  THENA  Auto)
  THEN  (D  0  THENA  Auto)
  THEN  MoveToConcl  (-3)
  THEN  ListInd  (-1)
  THEN  Reduce  0
  THEN  (UnivCD  THENA  Auto)
  THEN  RepUR  ``hdf-parallel``  0
  THEN  RecUnfold  `mk-hdf`  0
  THEN  Reduce  0
  THEN  AutoSplit
  THEN  Try  (((FLemma  `hdf-halted-is-halt`  [-1]  THENA  Auto)
                        THEN  HypSubst'  (-1)  0
                        THEN  Reduce  0
                        THEN  Try  ((RWO  "iterate-hdf-halt"  0  THENA  Auto))
                        THEN  Reduce  0
                        THEN  Auto))
  THEN  Try  ((RWO  "hdf-out-run"  0  THEN  Auto))
  THEN  Auto
  THEN  HDataflowHDAll
  THEN  Try  ((RWO  "bag-append-empty"  0  THENA  Auto))
  THEN  Repeat  (((RW  (NthC  1  CallByValueallC)  0  THENA  Complete  (Auto))  THEN  Reduce  0))
  THEN  Try  ((RWO  "hdf-out-inl"  0  THEN  Auto))
  THEN  Try  ((RWO  "hdf-out-run"  0  THEN  Auto))
  THEN  Fold  `hdf-parallel`  0
  THEN  Try  (Fold  `hdf-halt`  0)
  THEN  BackThruSomeHyp)

---

Home Index