---

Step * of Lemma hdf-buffer-transformation2

∀[init,L,G:Top]. ∀[m:ℕ].
  (hdf-buffer(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) then mk_lambdas_fun(λg.∪f∈G[g].∪b∈s.f b;m) else L[a] n fi ;
                                      λg.<mk-hdf if bag-null(select_fun_last(g;m)) then s else select_fun_last(g;m) fi 
                                         , select_fun_last(g;m)
                                         >; m + 1))))) 
    init)
BY
{ (Auto
   THEN ProcTransRepUR ``hdf-buffer so_apply bag-null`` 0
   THEN (RW LiftAllC 0 THEN Reduce 0)
   THEN Refine `sqequalSqle` []
   THEN OneFixpointLeast
   THEN RepeatFor 3 (MoveToConcl (-3))
   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. m : ℕ
2. j : ℤ
3. j ≠ 0
4. 0 < j
5. ∀init,L,G:Top.
     (λmk-hdf,s0. let X,bs = s0 
                  in case X
                      of inl(y) =>
                      inl (λa.let X',fs = y a 
                              in let bs' ←─ ∪f∈fs.∪b∈bs.f b
                                 in <mk-hdf <X', case null(bs') of inl() => bs | inr() => bs'>, bs'>)
                      | inr(y) =>
                      inr ⋅ ^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  then mk_lambdas_fun(λg.∪f∈G g.∪b∈s.f b;m)  else (L a n);
                                          λg.<mk-hdf 
                                              case null(select_fun_last(g;m))
                                               of inl() =>
                                               s
                                               | inr() =>
                                               select_fun_last(g;m)
                                             , select_fun_last(g;m)
                                             >; m + 1))))) 
        init)
6. init : Top@i
7. L : Top@i
8. G : Top@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 bs' ←─ ∪f∈fs.∪b∈init.f b
             in <λmk-hdf,s0. let X,bs = s0 
                             in case X
                                 of inl(y) =>
                                 inl (λa.let X',fs = y a 
                                         in let bs' ←─ ∪f∈fs.∪b∈bs.f b
                                            in <mk-hdf <X', case null(bs') of inl() => bs | inr() => bs'>, bs'>)
                                 | inr(y) =>
                                 inr ⋅ ^j - 1 
                 ⊥ 
                 <X', case null(bs') of inl() => init | inr() => bs'>
                , bs'
                >) ≤ fix((λmk-hdf,s. (inl (λa.cbva_seq(λn.if n=m  then mk_lambdas_fun(λg.∪f∈G g.∪b∈s.f b;m)  else (L a n\000C);
                                                    λg.<mk-hdf 
                                                        case null(select_fun_last(g;m))
                                                         of inl() =>
                                                         s
                                                         | inr() =>
                                                         select_fun_last(g;m)
                                                       , select_fun_last(g;m)
                                                       >; m + 1))))) 
                  init

2
1. m : ℕ
2. j : ℤ
3. j ≠ 0
4. 0 < j
5. ∀init,L,G:Top.
     (λmk-hdf,s. (inl (λa.cbva_seq(λn.if n=m  then mk_lambdas_fun(λg.∪f∈G g.∪b∈s.f b;m)  else (L a n);
                                   λg.<mk-hdf 
                                       case null(select_fun_last(g;m)) of inl() => s | inr() => select_fun_last(g;m)
                                      , select_fun_last(g;m)
                                      >; m + 1)))^j - 1 
      ⊥ 
      init ≤ fix((λmk-hdf,s0. let X,bs = s0 
                              in case X
                                  of inl(y) =>
                                  inl (λa.let X',fs = y a 
                                          in let bs' ←─ ∪f∈fs.∪b∈bs.f b
                                             in <mk-hdf <X', case null(bs') of inl() => bs | inr() => bs'>, bs'>)
                                  | inr(y) =>
                                  inr ⋅ )) 
             <fix((λmk-hdf.(inl (λa.cbva_seq(L a; λg.<mk-hdf, G g>; m))))), init>)
6. init : Top@i
7. L : Top@i
8. G : Top@i
⊢ inl (λa.cbva_seq(λn.if n=m  then mk_lambdas_fun(λg.∪f∈G g.∪b∈init.f b;m)  else (L a n);
                   λg.<λmk-hdf,s. (inl (λa.cbva_seq(λn.if n=m  then mk_lambdas_fun(λg.∪f∈G g.∪b∈s.f b;m)  else (L a n);
                                                    λg.<mk-hdf 
                                                        case null(select_fun_last(g;m))
                                                         of inl() =>
                                                         s
                                                         | inr() =>
                                                         select_fun_last(g;m)
                                                       , select_fun_last(g;m)
                                                       >; m + 1)))^j - 1 
                       ⊥ 
                       case null(select_fun_last(g;m)) of inl() => init | inr() => select_fun_last(g;m)
                      , select_fun_last(g;m)
                      >; m + 1)) ≤ fix((λmk-hdf,s0. let X,bs = s0 
                                                    in case X
                                                        of inl(y) =>
                                                        inl (λa.let X',fs = y a 
                                                                in let bs' ←─ ∪f∈fs.∪b∈bs.f b
                                                                   in <mk-hdf 
                                                                       <X'
                                                                       , case null(bs') of inl() => bs | inr() => bs'
                                                                       >
                                                                      , bs'
                                                                      >)
                                                        | inr(y) =>
                                                        inr ⋅ )) 
                                   <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-buffer(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)
                                                                                  then  mk\_lambdas\_fun(\mlambda{}g.\mcup{}f\mmember{}G[g].\mcup{}b\mmember{}s.f  b;m)
                                                                                  else  L[a]  n
                                                                                  fi  ;  \mlambda{}g.<mk-hdf 
                                                                                                    if  bag-null(select\_fun\_last(g;m))
                                                                                                    then  s
                                                                                                    else  select\_fun\_last(g;m)
                                                                                                    fi 
                                                                                                  ,  select\_fun\_last(g;m)
                                                                                                  >  m  +  1))))) 
        init)


By

(Auto
  THEN  ProcTransRepUR  ``hdf-buffer  so\_apply  bag-null``  0
  THEN  (RW  LiftAllC  0  THEN  Reduce  0)
  THEN  Refine  `sqequalSqle`  []
  THEN  OneFixpointLeast
  THEN  RepeatFor  3  (MoveToConcl  (-3))
  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