Step
*
2
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,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)))^j - 1
⊥
<init1, init2> ≤ 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 @ []
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 ⋅ ))
<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
>)
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.cbva_seq(λn.if (n) < (m1)
then L1 init1 a n
else if (n) < (m1 + m2)
then mk_lambdas(L2 init2 a (n - m1);m1)
else mk_lambdas_fun(λg1.mk_lambdas_fun(λg2.((G1 g1) @ (G2 g2));m2);m1);
λg.<λ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(...;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)))^j -\000C 1
⊥
<S1 partial_ap_gen(g;(m1 + m2) + 1;0;m1) init1, S2 partial_ap_gen(g;(m1 + m2) + 1;m1;m2) init2>
, select_fun_last(g;m1 + m2)
>; (m1 + m2) + 1)) ≤ 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 @ []
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 ⋅ ))
<fix((λmk-hdf,s. (inl (λa.cbva_seq(L1 s a; λg.<mk-hdf (S1 g s), G1 g>; m1))))\000C) init1
, fix((λmk-hdf,s. (inl (λa.cbva_seq(L2 s a; λg.<mk-hdf (S2 g s), G2 g>; m2)))\000C)) init2
>
BY
{ ((RW (AddrC [2;1] (UnrollLoopsOnceExceptC SqequalProcTransLst)) 0 THEN Reduce 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 [2;1] LiftAllC) 0 THENA Auto)
THEN Fold `select_fun_last` 0
THEN (Subst ⌜m1 + m2 + 1 ~ (m1 + m2) + 1⌝ 0⋅ THENA Auto')
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 RepeatFor 3 ((SqLeCD THEN Try (Complete (Auto))))
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,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.mk\_lambdas\_fun(...;m2);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)))\^{}j - 1
\mbot{}
<init1, init2> \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 @ []
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{} ))
<fix((\mlambda{}mk-hdf,s. (inl (\mlambda{}a.cbva\_seq(L1 s a; \mlambda{}g.<mk-hdf (S1 g s), G1 g> m1))))\000C) init1
, fix((\mlambda{}mk-hdf,s. (inl (\mlambda{}a.cbva\_seq(L2 s a; \mlambda{}g.<mk-hdf (S2 g s), G2 g> m2)))\000C)) 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.cbva\_seq(\mlambda{}n.if (n) < (m1)
then L1 init1 a n
else if (n) < (m1 + m2)
then mk\_lambdas(L2 init2 a (n - m1);m1)
else mk\_lambdas\_fun(\mlambda{}g1.mk\_lambdas\_fun(\mlambda{}g2.((G1 g1)
@ (G2 g2));m2);m1);
\mlambda{}g.<\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)))\^{}j - 1
\mbot{}
<S1 partial\_ap\_gen(g;(m1 + m2) + 1;0;m1) init1
, S2 partial\_ap\_gen(g;(m1 + m2) + 1;m1;m2) init2
>
, select\_fun\_last(g;m1 + m2)
> (m1 + m2) + 1)) \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'>, \000Cout>
| inr(P) =>
let out \mleftarrow{}{} xs @ []
in <mk-hdf <X', inr \mcdot{} >,\000C 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'>,\000C out>)
| inr(y) =>
inr \mcdot{} ))
<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)))))\000C
init2
>
By
Latex:
((RW (AddrC [2;1] (UnrollLoopsOnceExceptC SqequalProcTransLst)) 0 THEN Reduce 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 [2;1] LiftAllC) 0 THENA Auto)
THEN Fold `select\_fun\_last` 0
THEN (Subst \mkleeneopen{}m1 + m2 + 1 \msim{} (m1 + m2) + 1\mkleeneclose{} 0\mcdot{} THENA Auto')
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 RepeatFor 3 ((SqLeCD THEN Try (Complete (Auto))))
THEN BackThruSomeHyp)
Home
Index