Step
*
1
1
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.
(λ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\000C(y) => inr Ax ^j - 1
⊥
<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
> ≤ case H partial_ap(g;m + 1;m) init
of inl() =>
fix((λ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)))))
<inr Ax , 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
14. @0 : Base
⊢ inl (λa.let Y',ys = cbva_seq(L (S partial_ap(g;m + 1;m) init) a;
λg@0.<case H g@0 (S partial_ap(g;m + 1;m) init)
of inl() =>
inl (λa.cbva_seq(L (S g@0 (S partial_ap(g;m + 1;m) init)) a;
λg@1.<case H g@1 (S g@0 (S 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 g@1 (S g@0 (S partial_ap(g;m + 1;m) init)))
| inr() =>
inr Ax
, G g@1
>; m))
| inr() =>
inr Ax
, G g@0
>; m)
in let out ←─ ys
in <λ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 ^j + (-1)
⊥
<inr Ax , Y'>
, out
>) ≤ 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() =>
fix((λ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)))))
<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))
BY
{ (RepeatFor 2 ((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 (LiftAllAddr [1;1] 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)⋅ }
1
1. j : ℤ
2. j ≠ 0
3. 0 < j
4. ∀L,G,H,S,init,out:Top. ∀m:ℕ. ∀a,g:Base.
(λ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\000C(y) => inr Ax ^j - 1
⊥
<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
> ≤ case H partial_ap(g;m + 1;m) init
of inl() =>
fix((λ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)))))
<inr Ax , 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
14. @0 : Base
15. a@0 : Base
16. g@0 : Base
17. λ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\000C) => inr Ax ^j - 1
⊥
<inr Ax
, case H partial_ap(g@0;m + 1;m) (S 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)))\000C))
(S partial_ap(g@0;m + 1;m) (S partial_ap(g;m + 1;m) init))
| inr() =>
inr Ax
> ≤ case H partial_ap(g@0;m + 1;m) (S partial_ap(g;m + 1;m) init)
of inl() =>
fix((λ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)))))
<inr Ax , S partial_ap(g@0;m + 1;m) (S partial_ap(g;m + 1;m) init)>
| inr() =>
inr Ax
⊢ λ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) \000C=> inr Ax ^j + (-1)
⊥
<inr Ax
, case H partial_ap(g@0;m + 1;m) (S partial_ap(g;m + 1;m) init)
of inl() =>
inl (λa.cbva_seq(L (S partial_ap(g@0;m + 1;m) (S partial_ap(g;m + 1;m) init)) a;
λg@1.<case H g@1 (S partial_ap(g@0;m + 1;m) (S 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 g@1 (S partial_ap(g@0;m + 1;m) (S partial_ap(g;m + 1;m) init)))
| inr() =>
inr Ax
, G g@1
>; m))
| inr() =>
inr Ax
> ≤ case H partial_ap(g@0;m + 1;m) (S partial_ap(g;m + 1;m) init)
of inl() =>
fix((λ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)))))
<inr Ax , S partial_ap(g@0;m + 1;m) (S partial_ap(g;m + 1;m) init)>
| inr() =>
inr Ax
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.
(\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 \^{}j - 1
\mbot{}
<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
> \mleq{} case H partial\_ap(g;m + 1;m) init
of inl() =>
fix((\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)))))
<inr Ax , 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
14. @0 : Base
\mvdash{} inl (\mlambda{}a.let Y',ys =
cbva\_seq(L (S partial\_ap(g;m + 1;m) init) a;
\mlambda{}g@0.<case H g@0 (S partial\_ap(g;m + 1;m) init)
of inl() =>
inl (\mlambda{}a.cbva\_seq(L (S g@0 (S partial\_ap(g;m + 1;m) init)) a;
\mlambda{}g@1.<case H g@1 (S g@0 (S 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 g@1 (S g@0 (S partial\_ap(g;m + 1;m) init)))
| inr() =>
inr Ax
, G g@1
> m))
| inr() =>
inr Ax
, G g@0
> m)
in let out \mleftarrow{}{} ys
in <\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 \^{}j + (-1)
\mbot{}
<inr Ax , Y'>
, out
>)
\mleq{} 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() =>
fix((\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)))))
<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))
By
(RepeatFor 2 ((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 (LiftAllAddr [1;1] 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)\mcdot{}
Home
Index