Step
*
of Lemma
hdf-memory-base
∀[f,C,F,s:Top].
(hdf-memory((λx,s. f[x;s]) o hdf-base(a.if C[a] then [F[a]] else [] fi );[s])
~ fix((λmk-hdf,s. (inl (λa.cbva_seq(λn.if C[a] then f[F[a];s] else s fi ; λg.<mk-hdf (g (λx.x)), [s]>; 1))))) s)
BY
{ (((UnivCD THENA Auto) THEN SqEqualTopToBase)
THEN (RWO "hdf-base-transformation1" 0 THENA Auto)
THEN (RWO "hdf-compose1-transformation1-2" 0 THENA Auto)
THEN (RWO "hdf-memory-transformation2" 0 THENA Auto)
THEN RepUR ``cbva_seq mk_lambdas_fun select_fun_ap select_fun_last mk_lambdas bag-map`` 0
THEN Repeat ((RecUnfold `callbyvalueall_seq` 0 THEN Reduce 0))
THEN Repeat ((RecUnfold `mk_lambdas-fun` 0 THEN Reduce 0))
THEN (RWO "primrec-unroll" 0 THENA Auto)
THEN Reduce 0
THEN (RWO "map-ifthenelse" 0 THENA Auto)
THEN HdfStateTransDefault `s') }
Latex:
\mforall{}[f,C,F,s:Top].
(hdf-memory((\mlambda{}x,s. f[x;s]) o hdf-base(a.if C[a] then [F[a]] else [] fi );[s])
\msim{} fix((\mlambda{}mk-hdf,s. (inl (\mlambda{}a.cbva\_seq(\mlambda{}n.if C[a] then f[F[a];s] else s fi ; \mlambda{}g.<mk-hdf (g (\mlambda{}x.x))
, [s]
> 1)))))
s)
By
(((UnivCD THENA Auto) THEN SqEqualTopToBase)
THEN (RWO "hdf-base-transformation1" 0 THENA Auto)
THEN (RWO "hdf-compose1-transformation1-2" 0 THENA Auto)
THEN (RWO "hdf-memory-transformation2" 0 THENA Auto)
THEN RepUR ``cbva\_seq mk\_lambdas\_fun select\_fun\_ap select\_fun\_last mk\_lambdas bag-map`` 0
THEN Repeat ((RecUnfold `callbyvalueall\_seq` 0 THEN Reduce 0))
THEN Repeat ((RecUnfold `mk\_lambdas-fun` 0 THEN Reduce 0))
THEN (RWO "primrec-unroll" 0 THENA Auto)
THEN Reduce 0
THEN (RWO "map-ifthenelse" 0 THENA Auto)
THEN HdfStateTransDefault `s')
Home
Index