Step
*
2
1
of Lemma
hdf-bind-gen-left-halt
1. A : Type
2. B : Type
3. C : Type
4. valueall-type(C)
5. Y : B ─→ hdataflow(A;C)@i
6. hdfs : bag(hdataflow(A;C))@i
7. a : A@i
⊢ hdf-out(hdf-halt() (hdfs) >>= Y;a) = hdf-out(hdf-halt() (hdfs) >>= λx.hdf-return({x});a) ∈ bag(C)
BY
{ (RepUR ``hdf-bind-gen bind-nxt`` 0
THEN RecUnfold `mk-hdf` 0
THEN Reduce 0
THEN Repeat (AutoSplit⋅)
THEN (RWO "hdf-out-run" 0 THENA Auto)
THEN Reduce 0
THEN Fold `bind-nxt` 0
THEN (GenConcl ⌈bag-map(λP.P(a);hdfs + {}) = Z ∈ bag(hdataflow(A;C) × bag(C))⌉⋅ THENA Auto)
THEN (CallByValueReduce 0 THENA Auto)
THEN (GenConcl ⌈[y∈bag-map(λyb.(fst(yb));Z)|¬bhdf-halted(y)] = W ∈ bag(hdataflow(A;C))⌉⋅
THENA (Auto THEN Try ((BLemma `bag-filter-wf3` THEN Auto)))
)
THEN RepeatFor 2 ((CallByValueReduce 0 THEN Auto))
THEN Reduce 0
THEN Auto)⋅ }
Latex:
1. A : Type
2. B : Type
3. C : Type
4. valueall-type(C)
5. Y : B {}\mrightarrow{} hdataflow(A;C)@i
6. hdfs : bag(hdataflow(A;C))@i
7. a : A@i
\mvdash{} hdf-out(hdf-halt() (hdfs) >>= Y;a) = hdf-out(hdf-halt() (hdfs) >>= \mlambda{}x.hdf-return(\{x\});a)
By
(RepUR ``hdf-bind-gen bind-nxt`` 0
THEN RecUnfold `mk-hdf` 0
THEN Reduce 0
THEN Repeat (AutoSplit\mcdot{})
THEN (RWO "hdf-out-run" 0 THENA Auto)
THEN Reduce 0
THEN Fold `bind-nxt` 0
THEN (GenConcl \mkleeneopen{}bag-map(\mlambda{}P.P(a);hdfs + \{\}) = Z\mkleeneclose{}\mcdot{} THENA Auto)
THEN (CallByValueReduce 0 THENA Auto)
THEN (GenConcl \mkleeneopen{}[y\mmember{}bag-map(\mlambda{}yb.(fst(yb));Z)|\mneg{}\msubb{}hdf-halted(y)] = W\mkleeneclose{}\mcdot{}
THENA (Auto THEN Try ((BLemma `bag-filter-wf3` THEN Auto)))
)
THEN RepeatFor 2 ((CallByValueReduce 0 THEN Auto))
THEN Reduce 0
THEN Auto)\mcdot{}
Home
Index