Step
*
1
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
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
BY
{ (All (Unfold `subtract`)
THEN NthHypSq (-1)
THEN RepeatFor 4 ((EqCD THEN Try (Trivial)))
THEN RW (AddrC [2] UnrollRecursionC) 0
THEN Reduce 0
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.
(\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
15. a@0 : Base
16. g@0 : Base
17. \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@0;m + 1;m) (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 partial\_ap(g@0;m + 1;m) (S partial\_ap(g;m + 1;m) init))
| inr() =>
inr Ax
> \mleq{} 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
\mvdash{} \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@0;m + 1;m) (S partial\_ap(g;m + 1;m) init)
of inl() =>
inl (\mlambda{}a.cbva\_seq(L (S partial\_ap(g@0;m + 1;m) (S partial\_ap(g;m + 1;m) init)) a;
\mlambda{}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((\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 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
> \mleq{} 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
By
(All (Unfold `subtract`)
THEN NthHypSq (-1)
THEN RepeatFor 4 ((EqCD THEN Try (Trivial)))
THEN RW (AddrC [2] UnrollRecursionC) 0
THEN Reduce 0
THEN Auto)
Home
Index