Step
*
1
of Lemma
hdf-parallel-transformation2-2
1. L1 : Top
2. m2 : ℕ
3. j : ℤ
4. j ≠ 0
5. 0 < j
6. ∀L2,G1,G2,S1,S2,init1,init2:Top. ∀m1:ℕ.
(λ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 @ []
in <mk-hdf <X', inr ⋅ >, out>)
| inr(y) =>
case Y of inl(y) => inl (λa.let Y',ys = y a in let out ⟵ ys in <mk-hdf <inr ⋅ , Y'>, out>) | inr(\000Cy) => inr ⋅ ^j - 1
⊥
<fix((λmk-hdf,s. (inl (λa.cbva_seq(L1 s a; λg.<mk-hdf (S1 g s), G1 g>; m1))))) init1
, fix((λmk-hdf,s. (inl (λa.cbva_seq(L2 s a; λg.<mk-hdf (S2 g s), G2 g>; m2))))) init2
> ≤ fix((λmk-hdf,s. (inl (λa.cbva_seq(λn.if (n) < (m1)
then L1 (fst(s)) a n
else if (n) < (m1 + m2)
then mk_lambdas(L2 (snd(s)) a (n - m1);m1)
else mk_lambdas_fun(λg1.mk_lambdas_fun(λg2.((G1 g1)
@ (G2 g2));m2);m1);
λg.<mk-hdf
<S1 partial_ap_gen(g;(m1 + m2) + 1;0;m1) (fst(s))
, S2 partial_ap_gen(g;(m1 + m2) + 1;m1;m2) (snd(s))
>
, select_fun_last(g;m1 + m2)
>; (m1 + m2) + 1)))))
<init1, init2>)
7. L2 : Top@i
8. G1 : Top@i
9. G2 : Top@i
10. S1 : Top@i
11. S2 : Top@i
12. init1 : Top@i
13. init2 : Top@i
14. m1 : ℕ@i
⊢ inl (λa.let X',xs = cbva_seq(L1 init1 a; λg.<fix((λmk-hdf,s. (inl (λa.cbva_seq(L1 s a; λg.<mk-hdf (S1 g s), G1 g>;
m1)))))
(S1 g init1)
, G1 g
>; m1)
in let Y',ys = cbva_seq(L2 init2 a; λg.<fix((λmk-hdf,s. (inl (λa.cbva_seq(L2 s a; λg.<mk-hdf (S2 g s), G2 g>;
m2)))))
(S2 g init2)
, G2 g
>; m2)
in let out ⟵ xs @ 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 @ []
in <mk-hdf <X', inr ⋅ >, out>)
| inr(y) =>
case Y
of inl(y) =>
inl (λa.let Y',ys = y a
in let out ⟵ ys
in <mk-hdf <inr ⋅ , Y'>, out>)
| inr(y) =>
inr ⋅ ^j - 1
⊥
<X', Y'>
, out
>)
≤ fix((λmk-hdf,s. (inl (λa.cbva_seq(λn.if (n) < (m1)
then L1 (fst(s)) a n
else if (n) < (m1 + m2)
then mk_lambdas(L2 (snd(s)) a (n - m1);m1)
else mk_lambdas_fun(λg1.mk_lambdas_fun(λg2.((G1 g1)
@ (G2 g2));m2);m1);
λg.<mk-hdf
<S1 partial_ap_gen(g;(m1 + m2) + 1;0;m1) (fst(s))
, S2 partial_ap_gen(g;(m1 + m2) + 1;m1;m2) (snd(s))
>
, select_fun_last(g;m1 + m2)
>; (m1 + m2) + 1)))))
<init1, init2>
BY
{ (RW (AddrC [2] (UnrollLoopsOnceExceptC SqequalProcTransLst)) 0
THEN RepeatFor 2 ((SqLeCD THEN Try (Complete (Auto))))
THEN Repeat ((RWO "cbva_seq-spread" 0 THENA Auto))
THEN (RWO "cbva_seq_extend" 0 THENA Auto)
THEN (RWO "cbva_seq-combine2" 0 THENA Auto)
THEN RepUR ``ifthenelse eq_int lt_int btrue bfalse bag-map`` 0
THEN (RW (AddrC [1;1] LiftAllC) 0 THENA Auto)
THEN (Subst ⌜m1 + m2 + 1 ~ (m1 + m2) + 1⌝ 0⋅ THENA Auto')
THEN Fold `select_fun_last` 0
THEN (RWO "cbva_seq-list-case2" 0 THENA Auto)
THEN (RWO "select_fun_last_partial_ap_gen1" 0 THENA Auto)
THEN (RWO "partial_ap_of_partial_ap_gen1" 0 THENA Auto)
THEN (RWO "partial_ap_is_gen" 0 THENA Auto')
THEN Folds ``pi1 pi2`` 0
THEN RepeatFor 3 ((SqLeCD THEN Try (Complete (Auto))))
THEN All (Unfold `subtract`)
THEN BackThruSomeHyp) }
Latex:
Latex:
1. L1 : Top
2. m2 : \mBbbN{}
3. j : \mBbbZ{}
4. j \mneq{} 0
5. 0 < j
6. \mforall{}L2,G1,G2,S1,S2,init1,init2:Top. \mforall{}m1:\mBbbN{}.
(\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 @ []
in <mk-hdf <X', inr \mcdot{} >, 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 \mcdot{} , Y'>, out>)
| inr(y) =>
inr \mcdot{} \^{}j - 1
\mbot{}
<fix((\mlambda{}mk-hdf,s. (inl (\mlambda{}a.cbva\_seq(L1 s a; \mlambda{}g.<mk-hdf (S1 g s), G1 g> m1))))) init1
, fix((\mlambda{}mk-hdf,s. (inl (\mlambda{}a.cbva\_seq(L2 s a; \mlambda{}g.<mk-hdf (S2 g s), G2 g> m2))))) init2
>
\mleq{} fix((\mlambda{}mk-hdf,s.
(inl (\mlambda{}a.cbva\_seq(\mlambda{}n.if (n) < (m1)
then L1 (fst(s)) a n
else if (n) < (m1 + m2)
then mk\_lambdas(L2 (snd(s)) a (n - m1);m1)
else mk\_lambdas\_fun(\mlambda{}g1....;m1);
\mlambda{}g.<mk-hdf
<S1 partial\_ap\_gen(g;(m1 + m2) + 1;0;m1) (fst(s))
, S2 partial\_ap\_gen(g;(m1 + m2) + 1;m1;m2) (snd(s))
>
, select\_fun\_last(g;m1 + m2)
> (m1 + m2) + 1)))))
<init1, init2>)
7. L2 : Top@i
8. G1 : Top@i
9. G2 : Top@i
10. S1 : Top@i
11. S2 : Top@i
12. init1 : Top@i
13. init2 : Top@i
14. m1 : \mBbbN{}@i
\mvdash{} inl (\mlambda{}a.let X',xs = cbva\_seq(L1 init1 a; \mlambda{}g.<fix((\mlambda{}mk-hdf,s. (inl (\mlambda{}a.cbva\_seq(L1 s a; \mlambda{}g.<mk-hdf
(S1 g
s)
, G1 g
> m1)))\000C))
(S1 g init1)
, G1 g
> m1)
in let Y',ys = cbva\_seq(L2 init2 a;
\mlambda{}g.<fix((\mlambda{}mk-hdf,s. (inl (\mlambda{}a.cbva\_seq(L2 s a; \mlambda{}g.<mk-hdf (S2 g s)
, G2 g
> m2)))))
(S2 g init2)
, G2 g
> m2)
in let out \mleftarrow{}{} xs @ 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 @ []
in <mk-hdf <X', inr \mcdot{} >, 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 \mcdot{} , Y'>, out>)
| inr(y) =>
inr \mcdot{} \^{}j - 1
\mbot{}
<X', Y'>
, out
>)
\mleq{} fix((\mlambda{}mk-hdf,s.
(inl (\mlambda{}a.cbva\_seq(\mlambda{}n.if (n) < (m1)
then L1 (fst(s)) a n
else if (n) < (m1 + m2)
then mk\_lambdas(L2 (snd(s)) a (n - m1);m1)
else mk\_lambdas\_fun(...;m1);
\mlambda{}g.<mk-hdf
<S1 partial\_ap\_gen(g;(m1 + m2) + 1;0;m1) (fst(s))
, S2 partial\_ap\_gen(g;(m1 + m2) + 1;m1;m2) (snd(s))
>
, select\_fun\_last(g;m1 + m2)
> (m1 + m2) + 1)))))
<init1, init2>
By
Latex:
(RW (AddrC [2] (UnrollLoopsOnceExceptC SqequalProcTransLst)) 0
THEN RepeatFor 2 ((SqLeCD THEN Try (Complete (Auto))))
THEN Repeat ((RWO "cbva\_seq-spread" 0 THENA Auto))
THEN (RWO "cbva\_seq\_extend" 0 THENA Auto)
THEN (RWO "cbva\_seq-combine2" 0 THENA Auto)
THEN RepUR ``ifthenelse eq\_int lt\_int btrue bfalse bag-map`` 0
THEN (RW (AddrC [1;1] LiftAllC) 0 THENA Auto)
THEN (Subst \mkleeneopen{}m1 + m2 + 1 \msim{} (m1 + m2) + 1\mkleeneclose{} 0\mcdot{} THENA Auto')
THEN Fold `select\_fun\_last` 0
THEN (RWO "cbva\_seq-list-case2" 0 THENA Auto)
THEN (RWO "select\_fun\_last\_partial\_ap\_gen1" 0 THENA Auto)
THEN (RWO "partial\_ap\_of\_partial\_ap\_gen1" 0 THENA Auto)
THEN (RWO "partial\_ap\_is\_gen" 0 THENA Auto')
THEN Folds ``pi1 pi2`` 0
THEN RepeatFor 3 ((SqLeCD THEN Try (Complete (Auto))))
THEN All (Unfold `subtract`)
THEN BackThruSomeHyp)
Home
Index