Step
*
2
of Lemma
hdf-parallel-transformation2-0
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)))))
>
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-combine" 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 (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 RepeatFor 3 ((SqLeCD THEN Try (Complete (Auto))))
THEN BackThruSomeHyp) }
Latex:
1. L1 : Top
2. m2 : \mBbbN{}
3. j : \mBbbZ{}
4. j \mneq{} 0
5. 0 < j
6. \mforall{}L2,G1,G2:Top. \mforall{}m1:\mBbbN{}.
(\mlambda{}mk-hdf.(inl (\mlambda{}a.cbva\_seq(\mlambda{}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); \mlambda{}g.<mk-hdf
, select\_fun\_last(g;m1
+ m2)
> (m1 + m2) + 1)))\^{}j
- 1
\mbot{} \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.(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)))))
>)
7. L2 : Top@i
8. G1 : Top@i
9. G2 : Top@i
10. m1 : \mBbbN{}@i
\mvdash{} inl (\mlambda{}a.cbva\_seq(\mlambda{}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(\mlambda{}g1.mk\_lambdas\_fun(\mlambda{}g2.((G1 a g1)
@ (G2 a g2));m2);m1);
\mlambda{}g.<\mlambda{}mk-hdf.(inl (\mlambda{}a.cbva\_seq(\mlambda{}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(\mlambda{}g1....;m1);
\mlambda{}g.<mk-hdf, select\_fun\_last(g;m1 + m2)> (m1 + m2)
+ 1)))\^{}j - 1
\mbot{}
, 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.(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)))))
>
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-combine" 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 (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 RepeatFor 3 ((SqLeCD THEN Try (Complete (Auto))))
THEN BackThruSomeHyp)
Home
Index