Step
*
of Lemma
hdf-parallel-halt-left
∀[A,B:Type]. ∀[X:hdataflow(A;B)]. hdf-halt() || X = 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 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 (Complete ((InstHyp [⌈z1⌉] (-5)⋅ THEN Auto)))
THEN Try (Complete ((InstHyp [⌈z1⌉] (-6)⋅ THEN Auto)))) }
Latex:
\mforall{}[A,B:Type]. \mforall{}[X:hdataflow(A;B)]. hdf-halt() || X = 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 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 (Complete ((InstHyp [\mkleeneopen{}z1\mkleeneclose{}] (-5)\mcdot{} THEN Auto)))
THEN Try (Complete ((InstHyp [\mkleeneopen{}z1\mkleeneclose{}] (-6)\mcdot{} THEN Auto))))
Home
Index