Step
*
of Lemma
hdf-parallel-transformation2-0
∀[L1,L2,G1,G2:Top]. ∀[m1,m2:ℕ].
(fix((λmk-hdf.(inl (λa.cbva_seq(L1[a]; λg.<mk-hdf, G1[a;g]>; m1)))))
|| fix((λmk-hdf.(inl (λa.cbva_seq(L2[a]; λg.<mk-hdf, G2[a;g]>; m2)))))
~ fix((λmk-hdf.(inl (λa.cbva_seq(λn.if n <z m1 then L1[a] n
if n <z m1 + m2 then mk_lambdas(L2[a] (n - m1);m1)
else mk_lambdas_fun(λg1.mk_lambdas_fun(λg2.(G1[a;g1] + G2[a;g2]);m2);m1)
fi ; λg.<mk-hdf, select_fun_last(g;m1 + m2)>; (m1 + m2) + 1))))))
BY
{ (Auto
THEN ProcTransRepUR ``hdf-parallel so_apply bag-null empty-bag bag-append lt_int`` 0
THEN (RW LiftAllC 0 THEN Reduce 0)
THEN Refine `sqequalSqle` []
THEN OneFixpointLeast
THEN RepeatFor 4 (MoveToConcl (-3))
THEN NatInd (-1)
THEN (UnivCD THENA Auto)
THEN Try ((ThinVar `j' THEN UnrollLoopsOnce THEN Strictness THEN Auto))
THEN (RWO "fun_exp_unroll" 0 THENA Auto)
THEN AutoSplit) }
1
1. L1 : Top
2. m2 : ℕ
3. j : ℤ
4. j ≠ 0
5. 0 < j
6. ∀L2,G1,G2: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.(inl (λa.cbva_seq(L1 a; λg.<mk-hdf, G1 a g>; m1)))))
, fix((λmk-hdf.(inl (λa.cbva_seq(L2 a; λg.<mk-hdf, G2 a g>; m2)))))
> ≤ fix((λmk-hdf.(inl (λa.cbva_seq(λn.if (n) < (m1)
then L1 a n
else if (n) < (m1 + m2)
then mk_lambdas(L2 a (n - m1);m1)
else mk_lambdas_fun(λg1.mk_lambdas_fun(λg2.((G1 a g1)
@ (G2 a g2));m2);m1);
λg.<mk-hdf, select_fun_last(g;m1 + m2)>; (m1 + m2) + 1))))))
7. L2 : Top@i
8. G1 : Top@i
9. G2 : Top@i
10. m1 : ℕ@i
⊢ inl (λa.let X',xs = cbva_seq(L1 a; λg.<fix((λmk-hdf.(inl (λa.cbva_seq(L1 a; λg.<mk-hdf, G1 a g>; m1))))), G1 a g>;
m1)
in let Y',ys = cbva_seq(L2 a; λg.<fix((λmk-hdf.(inl (λa.cbva_seq(L2 a; λg.<mk-hdf, G2 a g>; m2))))), G2 a 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.(inl (λa.cbva_seq(λn.if (n) < (m1)
then L1 a n
else if (n) < (m1 + m2)
then mk_lambdas(L2 a (n - m1);m1)
else mk_lambdas_fun(λg1.mk_lambdas_fun(λg2.((G1 a g1)
@ (G2 a g2));m2);m1);
λg.<mk-hdf, select_fun_last(g;m1 + m2)>; (m1 + m2) + 1)))))
2
1. L1 : Top
2. m2 : ℕ
3. j : ℤ
4. j ≠ 0
5. 0 < j
6. ∀L2,G1,G2:Top. ∀m1:ℕ.
(λmk-hdf.(inl (λa.cbva_seq(λn.if (n) < (m1)
then L1 a n
else if (n) < (m1 + m2)
then mk_lambdas(L2 a (n - m1);m1)
else mk_lambdas_fun(λg1.mk_lambdas_fun(λg2.((G1 a g1)
@ (G2 a g2));m2);m1);
λg.<mk-hdf, select_fun_last(g;m1 + m2)>; (m1 + m2) + 1)))^j - 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\000C>) | inr(y) => inr ⋅ ))
<fix((λmk-hdf.(inl (λa.cbva_seq(L1 a; λg.<mk-hdf, G1 a g>; m1)))))
, fix((λmk-hdf.(inl (λa.cbva_seq(L2 a; λg.<mk-hdf, G2 a g>; m2)))))
>)
7. L2 : Top@i
8. G1 : Top@i
9. G2 : Top@i
10. m1 : ℕ@i
⊢ inl (λa.cbva_seq(λn.if (n) < (m1)
then L1 a n
else if (n) < (m1 + m2)
then mk_lambdas(L2 a (n - m1);m1)
else mk_lambdas_fun(λg1.mk_lambdas_fun(λg2.((G1 a g1) @ (G2 a g2));m2);m1);
λg.<λmk-hdf.(inl (λa.cbva_seq(λn.if (n) < (m1)
then L1 a n
else if (n) < (m1 + m2)
then mk_lambdas(L2 a (n - m1);m1)
else mk_lambdas_fun(...;m1); λg.<mk-hdf
, select_fun_last(g;m1
+ m2)
>; (m1 + m2) + 1)))^j
- 1
⊥
, 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.(inl (λa.cbva_seq(L1 a; λg.<mk-hdf, G1 a g>; m1)))))
, fix((λmk-hdf.(inl (λa.cbva_seq(L2 a; λg.<mk-hdf, G2 a g>; m2)))))
>
Latex:
Latex:
\mforall{}[L1,L2,G1,G2:Top]. \mforall{}[m1,m2:\mBbbN{}].
(fix((\mlambda{}mk-hdf.(inl (\mlambda{}a.cbva\_seq(L1[a]; \mlambda{}g.<mk-hdf, G1[a;g]> m1)))))
|| fix((\mlambda{}mk-hdf.(inl (\mlambda{}a.cbva\_seq(L2[a]; \mlambda{}g.<mk-hdf, G2[a;g]> m2)))))
\msim{} fix((\mlambda{}mk-hdf.(inl (\mlambda{}a.cbva\_seq(\mlambda{}n.if n <z m1 then L1[a] n
if n <z m1 + m2 then mk\_lambdas(L2[a] (n - m1);m1)
else mk\_lambdas\_fun(\mlambda{}g1.mk\_lambdas\_fun(\mlambda{}g2.(G1[a;g1]
+ G2[a;g2]);m2);m1)
fi ; \mlambda{}g.<mk-hdf, select\_fun\_last(g;m1 + m2)> (m1 + m2)
+ 1))))))
By
Latex:
(Auto
THEN ProcTransRepUR ``hdf-parallel so\_apply bag-null empty-bag bag-append lt\_int`` 0
THEN (RW LiftAllC 0 THEN Reduce 0)
THEN Refine `sqequalSqle` []
THEN OneFixpointLeast
THEN RepeatFor 4 (MoveToConcl (-3))
THEN NatInd (-1)
THEN (UnivCD THENA Auto)
THEN Try ((ThinVar `j' THEN UnrollLoopsOnce THEN Strictness THEN Auto))
THEN (RWO "fun\_exp\_unroll" 0 THENA Auto)
THEN AutoSplit)
Home
Index