Step
*
1
of Lemma
hdf-compose2-transformation2
1. m1 : ℕ
2. m2 : ℕ
3. j : ℤ
4. j ≠ 0
5. 0 < j
6. ∀L1,L2,G1,G2,init,S:Top.
(λmk-hdf,s0. let X,Y = s0
in case X
of inl(y) =>
case Y
of inl(y1) =>
inl (λa.let X',fs = y a
in let Y',bs = y1 a
in let out ⟵ ⋃f∈fs.⋃b∈bs.f b
in <mk-hdf <X', Y'>, out>)
| inr(y1) =>
inr ⋅
| inr(y) =>
inr ⋅ ^j - 1
⊥
<fix((λmk-hdf.(inl (λa.cbva_seq(L1 a; λg.<mk-hdf, G1 g>; m1)))))
, fix((λmk-hdf,s. (inl (λa.cbva_seq(L2 s a; λg.<mk-hdf (S g s), G2 g s>; m2))))) init
> ≤ fix((λmk-hdf,s. (inl (λa.cbva_seq(λn.if (n) < (m1)
then L1 a n
else if (n) < (m1 + m2)
then mk_lambdas(L2 s a (n - m1);m1)
else mk_lambdas_fun(λg1.mk_lambdas_fun(λg2.⋃f∈G1 g1.
⋃b∈G2 g2 s.
f b;m2);m1);
λg.<mk-hdf (S partial_ap_gen(g;(m1 + m2) + 1;m1;m2) s)
, select_fun_last(g;m1 + m2)
>; (m1 + m2) + 1)))))
init)
7. L1 : Top@i
8. L2 : Top@i
9. G1 : Top@i
10. G2 : Top@i
11. init : Top@i
12. S : Top@i
⊢ inl (λa.let X',fs = cbva_seq(L1 a; λg.<fix((λmk-hdf.(inl (λa.cbva_seq(L1 a; λg.<mk-hdf, G1 g>; m1))))), G1 g>; m1)
in let Y',bs = cbva_seq(L2 init a; λg.<fix((λmk-hdf,s. (inl (λa.cbva_seq(L2 s a; λg.<mk-hdf (S g s), G2 g s>;
m2)))))
(S g init)
, G2 g init
>; m2)
in let out ⟵ ⋃f∈fs.⋃b∈bs.f b
in <λmk-hdf,s0. let X,Y = s0
in case X
of inl(y) =>
case Y
of inl(y1) =>
inl (λa.let X',fs = y a
in let Y',bs = y1 a
in let out ⟵ ⋃f∈fs.⋃b∈bs.f b
in <mk-hdf <X', Y'>, out>)
| inr(y1) =>
inr ⋅
| inr(y) =>
inr ⋅ ^j - 1
⊥
<X', Y'>
, out
>)
≤ fix((λmk-hdf,s. (inl (λa.cbva_seq(λn.if (n) < (m1)
then L1 a n
else if (n) < (m1 + m2)
then mk_lambdas(L2 s a (n - m1);m1)
else mk_lambdas_fun(λg1.mk_lambdas_fun(λg2.⋃f∈G1 g1.⋃b∈G2 g2 s.
f b;m2);m1);
λg.<mk-hdf (S partial_ap_gen(g;(m1 + m2) + 1;m1;m2) s)
, select_fun_last(g;m1 + m2)
>; (m1 + m2) + 1)))))
init
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 Repeat ((RWO "cbva_seq_extend" 0 THENA Auto))
THEN (RWO "cbva_seq-combine" 0 THENA Auto)
THEN RepUR ``ifthenelse eq_int btrue bfalse bag-map bag-null lt_int`` 0
THEN (RW (AddrC [1;1] LiftAllC) 0 THENA Auto)
THEN Reduce 0
THEN (Subst ⌜m1 + m2 + 1 ~ (m1 + m2) + 1⌝ 0⋅ THENA Auto)
THEN (RWO "cbva_seq-list-case2" 0 THENA Auto)
THEN Fold `select_fun_last` 0
THEN (RWO "select_fun_last_partial_ap_gen1" 0 THENA Auto)
THEN (RWO "partial_ap_of_partial_ap_gen1" 0 THENA Auto)
THEN RepeatFor 3 ((SqLeCD THEN Try (Complete (Auto))))
THEN All (Unfold `subtract`)
THEN Try (BackThruSomeHyp)) }
Latex:
Latex:
1. m1 : \mBbbN{}
2. m2 : \mBbbN{}
3. j : \mBbbZ{}
4. j \mneq{} 0
5. 0 < j
6. \mforall{}L1,L2,G1,G2,init,S:Top.
(\mlambda{}mk-hdf,s0. let X,Y = s0
in case X
of inl(y) =>
case Y
of inl(y1) =>
inl (\mlambda{}a.let X',fs = y a
in let Y',bs = y1 a
in let out \mleftarrow{}{} \mcup{}f\mmember{}fs.\mcup{}b\mmember{}bs.f b
in <mk-hdf <X', Y'>, out>)
| inr(y1) =>
inr \mcdot{}
| inr(y) =>
inr \mcdot{} \^{}j - 1
\mbot{}
<fix((\mlambda{}mk-hdf.(inl (\mlambda{}a.cbva\_seq(L1 a; \mlambda{}g.<mk-hdf, G1 g> m1)))))
, fix((\mlambda{}mk-hdf,s. (inl (\mlambda{}a.cbva\_seq(L2 s a; \mlambda{}g.<mk-hdf (S g s), G2 g s> m2))))) init
>
\mleq{} fix((\mlambda{}mk-hdf,s.
(inl (\mlambda{}a.cbva\_seq(\mlambda{}n.if (n) < (m1)
then L1 a n
else if (n) < (m1 + m2)
then mk\_lambdas(L2 s a (n - m1);m1)
else mk\_lambdas\_fun(\mlambda{}g1....;m1);
\mlambda{}g.<mk-hdf (S partial\_ap\_gen(g;(m1 + m2) + 1;m1;m2) s)
, select\_fun\_last(g;m1 + m2)
> (m1 + m2) + 1)))))
init)
7. L1 : Top@i
8. L2 : Top@i
9. G1 : Top@i
10. G2 : Top@i
11. init : Top@i
12. S : Top@i
\mvdash{} inl (\mlambda{}a.let X',fs = cbva\_seq(L1 a; \mlambda{}g.<fix((\mlambda{}mk-hdf.(inl (\mlambda{}a.cbva\_seq(L1 a; \mlambda{}g.<mk-hdf, G1 g>
m1)))))
, G1 g
> m1)
in let Y',bs =
cbva\_seq(L2 init a; \mlambda{}g.<fix((\mlambda{}mk-hdf,s. (inl (\mlambda{}a.cbva\_seq(L2 s a; \mlambda{}g.<mk-hdf (S g s)
, G2 g s
> m2)))))
(S g init)
, G2 g init
> m2)
in let out \mleftarrow{}{} \mcup{}f\mmember{}fs.\mcup{}b\mmember{}bs.f b
in <\mlambda{}mk-hdf,s0. let X,Y = s0
in case X
of inl(y) =>
case Y
of inl(y1) =>
inl (\mlambda{}a.let X',fs = y a
in let Y',bs = y1 a
in let out \mleftarrow{}{} \mcup{}f\mmember{}fs.\mcup{}b\mmember{}bs.f b
in <mk-hdf <X', Y'>, out>)
| inr(y1) =>
inr \mcdot{}
| 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 a n
else if (n) < (m1 + m2)
then mk\_lambdas(L2 s a (n - m1);m1)
else mk\_lambdas\_fun(...;m1);
\mlambda{}g.<mk-hdf (S partial\_ap\_gen(g;(m1 + m2) + 1;m1;m2) s)
, select\_fun\_last(g;m1 + m2)
> (m1 + m2) + 1)))))
init
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 Repeat ((RWO "cbva\_seq\_extend" 0 THENA Auto))
THEN (RWO "cbva\_seq-combine" 0 THENA Auto)
THEN RepUR ``ifthenelse eq\_int btrue bfalse bag-map bag-null lt\_int`` 0
THEN (RW (AddrC [1;1] LiftAllC) 0 THENA Auto)
THEN Reduce 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 Fold `select\_fun\_last` 0
THEN (RWO "select\_fun\_last\_partial\_ap\_gen1" 0 THENA Auto)
THEN (RWO "partial\_ap\_of\_partial\_ap\_gen1" 0 THENA Auto)
THEN RepeatFor 3 ((SqLeCD THEN Try (Complete (Auto))))
THEN All (Unfold `subtract`)
THEN Try (BackThruSomeHyp))
Home
Index