Step
*
of Lemma
hdf-state-transformation2
∀[init,L,G:Top]. ∀[m:ℕ].
(hdf-state(fix((λmk-hdf.(inl (λa.cbva_seq(L[a]; λg.<mk-hdf, G[g]>; m)))));init)
~ fix((λmk-hdf,s. (inl (λa.cbva_seq(λn.if (n =z m + 1)
then mk_lambdas_fun(λg.if bag-null(select_fun_last(g;m))
then s
else select_fun_last(g;m)
fi ;m + 1)
if (n =z m) then mk_lambdas_fun(λg.∪f∈G[g].bag-map(f;s);m)
else L[a] n
fi ; λg.<mk-hdf select_fun_last(g;m + 1), select_fun_last(g;m + 1)>; m + 2)))))\000C
init)
BY
{ (Auto
THEN ProcTransRepUR ``hdf-state so_apply bag-null`` 0
THEN RepeatFor 4 (RW LiftRedOneC 0 THENA Try (CompleteAuto)⋅)
THEN skip{(RWW "hdf-sqequal8-4" 0 THENA Auto)}
THEN SqequalSqle
THEN OneFixpointLeast
THEN Reduce 0
THEN Repeat (MoveToConcl (-2))
THEN NatInd (-1)
THEN (UnivCD THENA Auto)
THEN Reduce 0
THEN Strictness
THEN Try (Complete (Auto))
THEN (RWO "fun_exp_unroll_1" 0 THENA Auto)
THEN Reduce 0) }
1
1. j : ℤ
2. 0 < j
3. ∀init,L,G:Top. ∀m:ℕ.
(λmk-hdf,s0. (inl (λa.let X,s = s0
in let X',fs = case X of inl(P) => P a | inr(z) => <inr ⋅ , {}>
in let b ←─ ∪f∈fs.bag-map(f;s)
in let s' ←─ case null(b) of inl() => s | inr() => b
in <mk-hdf <X', s'>, s'>))^j - 1
⊥
<fix((λmk-hdf.(inl (λa.cbva_seq(L a; λg.<mk-hdf, G g>; m))))), init>
≤ fix((λmk-hdf,s. (inl (λa.cbva_seq(λn.if n=m + 1
then mk_lambdas_fun(λg.case null(select_fun_last(g;m))
of inl() =>
s
| inr() =>
select_fun_last(g;m);m + 1)
else if n=m
then mk_lambdas_fun(λg.∪f∈G g.bag-map(f;s);m)
else (L a n); λg.<mk-hdf select_fun_last(g;m + 1)
, select_fun_last(g;m + 1)
>; m + 2)))))
init)
4. init : Top@i
5. L : Top@i
6. G : Top@i
7. m : ℕ@i
⊢ inl (λa.let X',fs = cbva_seq(L a; λg.<fix((λmk-hdf.(inl (λa.cbva_seq(L a; λg.<mk-hdf, G g>; m))))), G g>; m)
in let b ←─ ∪f∈fs.bag-map(f;init)
in let s' ←─ case null(b) of inl() => init | inr() => b
in <λmk-hdf,s0. (inl (λa.let X,s = s0
in let X',fs = case X of inl(P) => P a | inr(z) => <inr ⋅ , {}>
in let b ←─ ∪f∈fs.bag-map(f;s)
in let s' ←─ case null(b) of inl() => s | inr() => b
in <mk-hdf <X', s'>, s'>))^j - 1
⊥
<X', s'>
, s'
>) ≤ fix((λmk-hdf,s. (inl (λa.cbva_seq(λn.if n=m + 1
then mk_lambdas_fun(λg.case null(select_fun_last(g;m))
of inl() =>
s
| inr() =>
select_fun_last(g;m);m + 1)
else if n=m
then mk_lambdas_fun(λg.∪f∈G g.bag-map(f;s);m)
else (L a n); λg.<mk-hdf select_fun_last(g;m + 1)
, select_fun_last(g;m + 1)
>; m + 2)))))
init
2
1. j : ℤ
2. 0 < j
3. ∀init,L,G:Top. ∀m:ℕ.
(λmk-hdf,s. (inl (λa.cbva_seq(λn.if n=m + 1
then mk_lambdas_fun(λg.case null(select_fun_last(g;m))
of inl() =>
s
| inr() =>
select_fun_last(g;m);m + 1)
else if n=m then mk_lambdas_fun(λg.∪f∈G g.bag-map(f;s);m) else (L a n);
λg.<mk-hdf select_fun_last(g;m + 1), select_fun_last(g;m + 1)>; m + 2)))^j - 1
⊥
init ≤ fix((λmk-hdf,s0. (inl (λa.let X,s = s0
in let X',fs = case X of inl(P) => P a | inr(z) => <inr ⋅ , {}>
in let b ←─ ∪f∈fs.bag-map(f;s)
in let s' ←─ case null(b) of inl() => s | inr() => b
in <mk-hdf <X', s'>, s'>))))
<fix((λmk-hdf.(inl (λa.cbva_seq(L a; λg.<mk-hdf, G g>; m))))), init>)
4. init : Top@i
5. L : Top@i
6. G : Top@i
7. m : ℕ@i
⊢ inl (λa.cbva_seq(λn.if n=m + 1
then mk_lambdas_fun(λg.case null(select_fun_last(g;m))
of inl() =>
init
| inr() =>
select_fun_last(g;m);m + 1)
else if n=m then mk_lambdas_fun(λg.∪f∈G g.bag-map(f;init);m) else (L a n);
λg.<λmk-hdf,s. (inl (λa.cbva_seq(λn.if n=m + 1
then mk_lambdas_fun(λg.case null(select_fun_last(g;m))
of inl() =>
s
| inr() =>
select_fun_last(g;m);m + 1)
else if n=m
then mk_lambdas_fun(λg.∪f∈G g.bag-map(f;s);m)
else (L a n); λg.<mk-hdf select_fun_last(g;m + 1)
, select_fun_last(g;m + 1)
>; m + 2)))^j - 1
⊥
select_fun_last(g;m + 1)
, select_fun_last(g;m + 1)
>; m + 2)) ≤ fix((λmk-hdf,s0. (inl (λa.let X,s = s0
in let X',fs = case X
of inl(P) =>
P a
| inr(z) =>
<inr ⋅ , {}>
in let b ←─ ∪f∈fs.bag-map(f;s)
in let s' ←─ case null(b) of inl() => s | inr() => b
in <mk-hdf <X', s'>, s'>))))
<fix((λmk-hdf.(inl (λa.cbva_seq(L a; λg.<mk-hdf, G g>; m))))), init>
Latex:
\mforall{}[init,L,G:Top]. \mforall{}[m:\mBbbN{}].
(hdf-state(fix((\mlambda{}mk-hdf.(inl (\mlambda{}a.cbva\_seq(L[a]; \mlambda{}g.<mk-hdf, G[g]> m)))));init)
\msim{} fix((\mlambda{}mk-hdf,s. (inl (\mlambda{}a.cbva\_seq(\mlambda{}n.if (n =\msubz{} m + 1)
then mk\_lambdas\_fun(\mlambda{}g.if bag-null(select\_fun\_last(g;m))
then s
else select\_fun\_last(g;m)
fi ;m + 1)
if (n =\msubz{} m) then mk\_lambdas\_fun(\mlambda{}g.\mcup{}f\mmember{}G[g].bag-map(f;s);m)
else L[a] n
fi ; \mlambda{}g.<mk-hdf select\_fun\_last(g;m + 1)
, select\_fun\_last(g;m + 1)
> m + 2)))))
init)
By
(Auto
THEN ProcTransRepUR ``hdf-state so\_apply bag-null`` 0
THEN RepeatFor 4 (RW LiftRedOneC 0 THENA Try (CompleteAuto)\mcdot{})
THEN skip\{(RWW "hdf-sqequal8-4" 0 THENA Auto)\}
THEN SqequalSqle
THEN OneFixpointLeast
THEN Reduce 0
THEN Repeat (MoveToConcl (-2))
THEN NatInd (-1)
THEN (UnivCD THENA Auto)
THEN Reduce 0
THEN Strictness
THEN Try (Complete (Auto))
THEN (RWO "fun\_exp\_unroll\_1" 0 THENA Auto)
THEN Reduce 0)
Home
Index