Step
*
of Lemma
hdf-compose2-transformation2
∀[L1,L2,G1,G2,init,S:Top]. ∀[m1,m2:ℕ].
(fix((λmk-hdf.(inl (λa.cbva_seq(L1[a]; λg.<mk-hdf, G1[g]>; m1)))))
o (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 <z m1 then L1[a] n
if n <z 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)
fi ; λ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
{ (Auto
THEN ProcTransRepUR ``hdf-compose2 so_apply bag-null lt_int`` 0
THEN (RW LiftAllC 0 THEN Reduce 0)
THEN Refine `sqequalSqle` []
THEN OneFixpointLeast
THEN RepeatFor 6 (MoveToConcl (-4))
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. 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
2
1. m1 : ℕ
2. m2 : ℕ
3. j : ℤ
4. j ≠ 0
5. 0 < j
6. ∀L1,L2,G1,G2,init,S:Top.
(λ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)))^j - 1
⊥
init ≤ fix((λ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 ⋅ ))
<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
>)
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.cbva_seq(λn.if (n) < (m1)
then L1 a n
else if (n) < (m1 + m2)
then mk_lambdas(L2 init a (n - m1);m1)
else mk_lambdas_fun(λg1.mk_lambdas_fun(λg2.⋃f∈G1 g1.⋃b∈G2 g2 init.f b;m2);m1);
λg.<λ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)))^j - 1
⊥
(S partial_ap_gen(g;(m1 + m2) + 1;m1;m2) init)
, select_fun_last(g;m1 + m2)
>; (m1 + m2) + 1)) ≤ fix((λ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 ⋅ ))
<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
>
Latex:
Latex:
\mforall{}[L1,L2,G1,G2,init,S:Top]. \mforall{}[m1,m2:\mBbbN{}].
(fix((\mlambda{}mk-hdf.(inl (\mlambda{}a.cbva\_seq(L1[a]; \mlambda{}g.<mk-hdf, G1[g]> m1)))))
o (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)
\msim{} fix((\mlambda{}mk-hdf,s. (inl (\mlambda{}a.cbva\_seq(\mlambda{}n.if n <z m1 then L1[a] n
if n <z m1 + m2 then mk\_lambdas(L2[s;a] (n - m1);m1)
else mk\_lambdas\_fun(\mlambda{}g1.mk\_lambdas\_fun(\mlambda{}g2.\mcup{}f\mmember{}G1[g1].
\mcup{}b\mmember{}G2[g2;s].
f b;m2);m1)
fi ; \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:
(Auto
THEN ProcTransRepUR ``hdf-compose2 so\_apply bag-null lt\_int`` 0
THEN (RW LiftAllC 0 THEN Reduce 0)
THEN Refine `sqequalSqle` []
THEN OneFixpointLeast
THEN RepeatFor 6 (MoveToConcl (-4))
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