Step
*
2
of Lemma
hdf-parallel-transformation2-3
1. j : ℤ
2. j ≠ 0
3. 0 < j
4. ∀L,G,H,S,init,out:Top. ∀m:ℕ. ∀a,g:Base.
(case H partial_ap(g;m + 1;m) init
of inl() =>
λmk-hdf,s. (inl (λa.cbva_seq(λn.if n=m
then case fst(s)
of inl(x) =>
mk_lambdas_fun(λg.(out + (G g));m)
| inr(x) =>
mk_lambdas_fun(λg.(G g);m)
else (L (snd(s)) a n); λg.<case H partial_ap(g;m + 1;m) (snd(s))
of inl() =>
mk-hdf <inr Ax , S partial_ap(g;m + 1;m) (snd(s))>
| inr() =>
inr Ax
, select_fun_last(g;m)
>; m + 1)))^j - 1
⊥
<inr Ax , S partial_ap(g;m + 1;m) init>
| inr() =>
inr Ax ≤ fix((λmk-hdf,s0. let X,Y = s0
in case X
of inl(y) =>
inl (λa.let X',xs = y a
in case Y
of inl(P) =>
let Y',ys = P a
in let out ←─ xs + ys
in <mk-hdf <X', Y'>, out>
| inr(P) =>
let out ←─ xs + Ax
in <mk-hdf <X', inr Ax >, out>)
| inr(y) =>
case Y
of inl(y) =>
inl (λa.let Y',ys = y a
in let out ←─ ys
in <mk-hdf <inr Ax , Y'>, out>)
| inr(y) =>
inr Ax ))
<inr Ax
, case H partial_ap(g;m + 1;m) init
of inl() =>
fix((λmk-hdf,s. (inl (λa.cbva_seq(L s a; λg.<case H g s
of inl() =>
mk-hdf (S g s)
| inr() =>
inr Ax
, G g
>; m)))))
(S partial_ap(g;m + 1;m) init)
| inr() =>
inr Ax
>)
5. L : Top@i
6. G : Top@i
7. H : Top@i
8. S : Top@i
9. init : Top@i
10. out : Top@i
11. m : ℕ@i
12. a : Base@i
13. g : Base@i
⊢ case H partial_ap(g;m + 1;m) init
of inl() =>
inl (λa.cbva_seq(λn.if n=m then mk_lambdas_fun(λg.(G g);m) else (L (S partial_ap(g;m + 1;m) init) a n);
λg@0.<case H partial_ap(g@0;m + 1;m) (S partial_ap(g;m + 1;m) init)
of inl() =>
λmk-hdf,s. (inl (λa.cbva_seq(λn.if n=m
then case fst(s)
of inl(x) =>
mk_lambdas_fun(λg.(out + (G g));m)
| inr(x) =>
mk_lambdas_fun(λg.(G g);m)
else (L (snd(s)) a n); λg.<case H partial_ap(g;m + 1;m)
(snd(s))
of inl() =>
mk-hdf
<inr Ax
, S partial_ap(g;m + 1;m)
(snd(s))
>
| inr() =>
inr Ax
, select_fun_last(g;m)
>; m + 1)))^j - 1
⊥
<inr Ax , S partial_ap(g@0;m + 1;m) (S partial_ap(g;m + 1;m) init)>
| inr() =>
inr Ax
, select_fun_last(g@0;m)
>; m + 1))
| inr() =>
inr Ax ≤ fix((λmk-hdf,s0. let X,Y = s0
in case X
of inl(y) =>
inl (λa.let X',xs = y a
in case Y
of inl(P) =>
let Y',ys = P a
in let out ←─ xs + ys
in <mk-hdf <X', Y'>, out>
| inr(P) =>
let out ←─ xs + Ax
in <mk-hdf <X', inr Ax >, out>)
| inr(y) =>
case Y
of inl(y) =>
inl (λa.let Y',ys = y a
in let out ←─ ys
in <mk-hdf <inr Ax , Y'>, out>)
| inr(y) =>
inr Ax ))
<inr Ax
, case H partial_ap(g;m + 1;m) init
of inl() =>
fix((λmk-hdf,s. (inl (λa.cbva_seq(L s a; λg.<case H g s of inl() => mk-hdf (S g s) | inr() => inr Ax
, G g
>; m)))))
(S partial_ap(g;m + 1;m) init)
| inr() =>
inr Ax
>
BY
{ (RW (AddrC [2] (UnrollLoopsOnceExceptC (``pi1 pi2`` @ SqequalProcTransLst))) 0
THEN RepeatFor 3 ((SqLeCD THEN Try (Complete (Auto))))
THEN (RWO "cbva_seq-spread" 0 THENA Auto)
THEN (RWO "cbva_seq_extend" 0 THENA Auto)
THEN RepUR ``ifthenelse eq_int lt_int btrue bfalse bag-map`` 0
THEN (RW (AddrC [2;1] LiftAllC) 0 THENA Auto)
THEN Fold `select_fun_last` 0
THEN All(RepUR ``bag-append``)
THEN RepeatFor 3 ((SqLeCD THEN Try (Complete (Auto))))
THEN InstHyp [⌈L⌉;⌈G⌉;⌈H⌉;⌈S⌉;⌈S partial_ap(g;m + 1;m) init⌉;⌈out⌉;⌈m⌉;⌈a⌉;⌈g@0⌉] 4⋅
THEN Auto) }
Latex:
1. j : \mBbbZ{}
2. j \mneq{} 0
3. 0 < j
4. \mforall{}L,G,H,S,init,out:Top. \mforall{}m:\mBbbN{}. \mforall{}a,g:Base.
(case H partial\_ap(g;m + 1;m) init
of inl() =>
\mlambda{}mk-hdf,s. (inl (\mlambda{}a.cbva\_seq(\mlambda{}n.if n=m
then case fst(s)
of inl(x) =>
mk\_lambdas\_fun(\mlambda{}g.(out + (G g));m)
| inr(x) =>
mk\_lambdas\_fun(\mlambda{}g.(G g);m)
else (L (snd(s)) a n); \mlambda{}g.<case H partial\_ap(g;m + 1;m)
(snd(s))
of inl() =>
mk-hdf
<inr Ax
, S partial\_ap(g;m + 1;m)
(snd(s))
>
| inr() =>
inr Ax
, select\_fun\_last(g;m)
> m + 1)))\^{}j - 1
\mbot{}
<inr Ax , S partial\_ap(g;m + 1;m) init>
| inr() =>
inr Ax \mleq{} fix((\mlambda{}mk-hdf,s0. let X,Y = s0
in case X
of inl(y) =>
inl (\mlambda{}a.let X',xs = y a
in case Y
of inl(P) =>
let Y',ys = P a
in let out \mleftarrow{}{} xs + ys
in <mk-hdf <X', Y'>, out>
| inr(P) =>
let out \mleftarrow{}{} xs + Ax
in <mk-hdf <X', inr Ax >, out>)
| inr(y) =>
case Y
of inl(y) =>
inl (\mlambda{}a.let Y',ys = y a
in let out \mleftarrow{}{} ys
in <mk-hdf <inr Ax , Y'>, out>)
| inr(y) =>
inr Ax ))
<inr Ax
, case H partial\_ap(g;m + 1;m) init
of inl() =>
fix((\mlambda{}mk-hdf,s. (inl (\mlambda{}a.cbva\_seq(L s a; \mlambda{}g.<case H g s
of inl() =>
mk-hdf (S g s)
| inr() =>
inr Ax
, G g
> m)))))
(S partial\_ap(g;m + 1;m) init)
| inr() =>
inr Ax
>)
5. L : Top@i
6. G : Top@i
7. H : Top@i
8. S : Top@i
9. init : Top@i
10. out : Top@i
11. m : \mBbbN{}@i
12. a : Base@i
13. g : Base@i
\mvdash{} case H partial\_ap(g;m + 1;m) init
of inl() =>
inl (\mlambda{}a.cbva\_seq(\mlambda{}n.if n=m
then mk\_lambdas\_fun(\mlambda{}g.(G g);m)
else (L (S partial\_ap(g;m + 1;m) init) a n);
\mlambda{}g@0.<case H partial\_ap(g@0;m + 1;m) (S partial\_ap(g;m + 1;m) init)
of inl() =>
\mlambda{}mk-hdf,s. (inl (\mlambda{}a.cbva\_seq(\mlambda{}n.if n=m
then case fst(s)
of inl(x) =>
mk\_lambdas\_fun(\mlambda{}g.(out
+ (G g));m)
| inr(x) =>
mk\_lambdas\_fun(\mlambda{}g.(G g);m)
else (L (snd(s)) a n);
\mlambda{}g.<case H partial\_ap(g;m + 1;m) (snd(s))
of inl() =>
mk-hdf
<inr Ax
, S partial\_ap(g;m + 1;m) (snd(s))
>
| inr() =>
inr Ax
, select\_fun\_last(g;m)
> m + 1)))\^{}j - 1
\mbot{}
<inr Ax , S partial\_ap(g@0;m + 1;m) (S partial\_ap(g;m + 1;m) init)>
| inr() =>
inr Ax
, select\_fun\_last(g@0;m)
> m + 1))
| inr() =>
inr Ax \mleq{} fix((\mlambda{}mk-hdf,s0. let X,Y = s0
in case X
of inl(y) =>
inl (\mlambda{}a.let X',xs = y a
in case Y
of inl(P) =>
let Y',ys = P a
in let out \mleftarrow{}{} xs + ys
in <mk-hdf <X', Y'>, out>
| inr(P) =>
let out \mleftarrow{}{} xs + Ax
in <mk-hdf <X', inr Ax >, out>)
| inr(y) =>
case Y
of inl(y) =>
inl (\mlambda{}a.let Y',ys = y a
in let out \mleftarrow{}{} ys
in <mk-hdf <inr Ax , Y'>, out>)
| inr(y) =>
inr Ax ))
<inr Ax
, case H partial\_ap(g;m + 1;m) init
of inl() =>
fix((\mlambda{}mk-hdf,s. (inl (\mlambda{}a.cbva\_seq(L s a; \mlambda{}g.<case H g s
of inl() =>
mk-hdf (S g s)
| inr() =>
inr Ax
, G g
> m)))))
(S partial\_ap(g;m + 1;m) init)
| inr() =>
inr Ax
>
By
(RW (AddrC [2] (UnrollLoopsOnceExceptC (``pi1 pi2`` @ SqequalProcTransLst))) 0
THEN RepeatFor 3 ((SqLeCD THEN Try (Complete (Auto))))
THEN (RWO "cbva\_seq-spread" 0 THENA Auto)
THEN (RWO "cbva\_seq\_extend" 0 THENA Auto)
THEN RepUR ``ifthenelse eq\_int lt\_int btrue bfalse bag-map`` 0
THEN (RW (AddrC [2;1] LiftAllC) 0 THENA Auto)
THEN Fold `select\_fun\_last` 0
THEN All(RepUR ``bag-append``)
THEN RepeatFor 3 ((SqLeCD THEN Try (Complete (Auto))))
THEN InstHyp [\mkleeneopen{}L\mkleeneclose{};\mkleeneopen{}G\mkleeneclose{};\mkleeneopen{}H\mkleeneclose{};\mkleeneopen{}S\mkleeneclose{};\mkleeneopen{}S partial\_ap(g;m + 1;m) init\mkleeneclose{};\mkleeneopen{}out\mkleeneclose{};\mkleeneopen{}m\mkleeneclose{};\mkleeneopen{}a\mkleeneclose{};\mkleeneopen{}g@0\mkleeneclose{}] 4\mcdot{}
THEN Auto)
Home
Index