---

Step * of Lemma hdf-memory-transformation2

∀[init,L,G:Top]. ∀[m:ℕ].
  (hdf-memory(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), s>; m + 2))))) 
    init)
BY
{ (Auto
   THEN ProcTransRepUR ``hdf-memory so_apply bag-null`` 0
   THEN RepeatFor 4 (RW LiftRedOneC 0    THENA Try (CompleteAuto)⋅)
   THEN skip{(RWO "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), s>; m + 2))))\000C) 
        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'>
                   , 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)
                                                                                      , s
                                                                                      >; 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), s>; 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), s>;
                                                    m + 2)))^j - 1 
                       ⊥ 
                       select_fun_last(g;m + 1)
                      , init
                      >; 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:

---

Latex:
\mforall{}[init,L,G:Top].  \mforall{}[m:\mBbbN{}].
    (hdf-memory(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),  s>  m  +  2))))) 
        init)


By

---

Latex:
(Auto
  THEN  ProcTransRepUR  ``hdf-memory  so\_apply  bag-null``  0
  THEN  RepeatFor  4  (RW  LiftRedOneC  0        THENA  Try  (CompleteAuto)\mcdot{})
  THEN  skip\{(RWO  "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