Step
*
1
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,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)))))
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-combine" 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 RepeatFor 3 ((SqLeCD THEN Try (Complete (Auto))))
THEN All (Unfold `subtract`)
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,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.(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)))))
>
\mleq{} fix((\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))))))
7. L2 : Top@i
8. G1 : Top@i
9. G2 : Top@i
10. m1 : \mBbbN{}@i
\mvdash{} inl (\mlambda{}a.let X',xs = cbva\_seq(L1 a; \mlambda{}g.<fix((\mlambda{}mk-hdf.(inl (\mlambda{}a.cbva\_seq(L1 a; \mlambda{}g.<mk-hdf, G1 a g>
m1)))))
, G1 a g
> m1)
in let Y',ys =
cbva\_seq(L2 a; \mlambda{}g.<fix((\mlambda{}mk-hdf.(inl (\mlambda{}a.cbva\_seq(L2 a; \mlambda{}g.<mk-hdf, G2 a g> m2)))))
, G2 a 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.(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(...;m2);m1);
\mlambda{}g.<mk-hdf, select\_fun\_last(g;m1 + m2)> (m1 + m2) + 1)))))
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-combine" 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 RepeatFor 3 ((SqLeCD THEN Try (Complete (Auto))))
THEN All (Unfold `subtract`)
THEN BackThruSomeHyp)
Home
Index