---

Step * of Lemma hdf-buffer-transformation3

∀[init,s,L,S,G:Top]. ∀[m:ℕ].
  (hdf-buffer(fix((λmk-hdf,s. (inl (λa.cbva_seq(L[s;a]; λg.<mk-hdf S[s;a;g], G[s;a;g]>; m))))) s;init) 
  ~ fix((λmk-hdf,s. (inl (λa.cbva_seq(λn.if (n =z m)
                                         then mk_lambdas_fun(λg.∪f∈G[fst(s);a;g].∪b∈snd(s).f b;m)
                                         else L[fst(s);a] n
                                         fi ; λg.<mk-hdf 
                                                  <S[fst(s);a;partial_ap(g;m + 1;m)]
                                                  , if bag-null(select_fun_last(g;m))
                                                    then snd(s)
                                                    else select_fun_last(g;m)
                                                    fi 
                                                  >
                                                 , select_fun_last(g;m)
                                                 >; m + 1))))) 
    <s, init>)
BY
{ (Auto
   THEN ProcTransRepUR ``hdf-buffer so_apply bag-null`` 0
   THEN (RW LiftAllC 0 THEN Reduce 0)
   THEN SqequalSqle
   THEN OneFixpointLeast
   THEN Repeat (MoveToConcl (-2))
   THEN NatInd (-1)
   THEN (UnivCD THENA Auto)
   THEN Try (Complete ((Reduce 0 THEN Strictness THEN Auto)))
   THEN (RWO "fun_exp_unroll_1" 0 THENA Auto)) }

1
1. j : ℤ
2. 0 < j
3. ∀init,s,L,S,G:Top. ∀m:ℕ.
     (λ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,s. (inl (λa.cbva_seq(L s a; λg.<mk-hdf (S s a g), G s a g>; m))))) s, init> 
      ≤ fix((λmk-hdf,s. (inl (λa.cbva_seq(λn.if n=m
                                                then mk_lambdas_fun(λg.∪f∈G (fst(s)) a g.∪b∈snd(s).f b;m)
                                                else (L (fst(s)) a n); λg.<mk-hdf 
                                                                           <S (fst(s)) a partial_ap(g;m + 1;m)
                                                                           , case null(select_fun_last(g;m))
                                                                              of inl() =>
                                                                              snd(s)
                                                                              | inr() =>
                                                                              select_fun_last(g;m)
                                                                           >
                                                                          , select_fun_last(g;m)
                                                                          >; m + 1))))) 
        <s, init>)
4. init : Top@i
5. s : Top@i
6. L : Top@i
7. S : Top@i
8. G : Top@i
9. m : ℕ@i
⊢ (λx.((λ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 ⋅ ) 
       (λ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))) 
  ⊥ 
  <fix((λmk-hdf,s. (inl (λa.cbva_seq(L s a; λg.<mk-hdf (S s a g), G s a g>; m))))) s, init> 
  ≤ fix((λmk-hdf,s. (inl (λa.cbva_seq(λn.if n=m
                                            then mk_lambdas_fun(λg.∪f∈G (fst(s)) a g.∪b∈snd(s).f b;m)
                                            else (L (fst(s)) a n); λg.<mk-hdf 
                                                                       <S (fst(s)) a partial_ap(g;m + 1;m)
                                                                       , case null(select_fun_last(g;m))
                                                                          of inl() =>
                                                                          snd(s)
                                                                          | inr() =>
                                                                          select_fun_last(g;m)
                                                                       >
                                                                      , select_fun_last(g;m)
                                                                      >; m + 1))))) 
    <s, init>

2
1. j : ℤ
2. 0 < j
3. ∀init,s,L,S,G:Top. ∀m:ℕ.
     (λmk-hdf,s. (inl (λa.cbva_seq(λn.if n=m
                                         then mk_lambdas_fun(λg.∪f∈G (fst(s)) a g.∪b∈snd(s).f b;m)
                                         else (L (fst(s)) a n); λg.<mk-hdf 
                                                                    <S (fst(s)) a partial_ap(g;m + 1;m)
                                                                    , case null(select_fun_last(g;m))
                                                                       of inl() =>
                                                                       snd(s)
                                                                       | inr() =>
                                                                       select_fun_last(g;m)
                                                                    >
                                                                   , select_fun_last(g;m)
                                                                   >; m + 1)))^j - 1 
      ⊥ 
      <s, 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,s. (inl (λa.cbva_seq(L s a; λg.<mk-hdf (S s a g), G s a g>; m))))) s, init>)
4. init : Top@i
5. s : Top@i
6. L : Top@i
7. S : Top@i
8. G : Top@i
9. m : ℕ@i
⊢ (λx.((λmk-hdf,s. (inl (λa.cbva_seq(λn.if n=m
                                           then mk_lambdas_fun(λg.∪f∈G (fst(s)) a g.∪b∈snd(s).f b;m)
                                           else (L (fst(s)) a n); λg.<mk-hdf 
                                                                      <S (fst(s)) a partial_ap(g;m + 1;m)
                                                                      , case null(select_fun_last(g;m))
                                                                         of inl() =>
                                                                         snd(s)
                                                                         | inr() =>
                                                                         select_fun_last(g;m)
                                                                      >
                                                                     , select_fun_last(g;m)
                                                                     >; m + 1)))) 
       (λmk-hdf,s. (inl (λa.cbva_seq(λn.if n=m
                                           then mk_lambdas_fun(λg.∪f∈G (fst(s)) a g.∪b∈snd(s).f b;m)
                                           else (L (fst(s)) a n); λg.<mk-hdf 
                                                                      <S (fst(s)) a partial_ap(g;m + 1;m)
                                                                      , case null(select_fun_last(g;m))
                                                                         of inl() =>
                                                                         snd(s)
                                                                         | inr() =>
                                                                         select_fun_last(g;m)
                                                                      >
                                                                     , select_fun_last(g;m)
                                                                     >; m + 1)))^j - 1 
        x))) 
  ⊥ 
  <s, 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,s. (inl (λa.cbva_seq(L s a; λg.<mk-hdf (S s a g), G s a g>; m))))) s, init>

---

Latex:


\mforall{}[init,s,L,S,G:Top].  \mforall{}[m:\mBbbN{}].
    (hdf-buffer(fix((\mlambda{}mk-hdf,s.  (inl  (\mlambda{}a.cbva\_seq(L[s;a];  \mlambda{}g.<mk-hdf  S[s;a;g],  G[s;a;g]>  m)))))  s;ini\000Ct) 
    \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[fst(s);a;g].\mcup{}b\mmember{}snd(s).f  b;m)
                                                                                  else  L[fst(s);a]  n
                                                                                  fi  ;  \mlambda{}g.<mk-hdf 
                                                                                                    <S[fst(s);a;partial\_ap(g;m  +  1;m)]
                                                                                                    ,  if  bag-null(select\_fun\_last(g;m))
                                                                                                        then  snd(s)
                                                                                                        else  select\_fun\_last(g;m)
                                                                                                        fi 
                                                                                                    >
                                                                                                  ,  select\_fun\_last(g;m)
                                                                                                  >  m  +  1))))) 
        <s,  init>)


By

(Auto
  THEN  ProcTransRepUR  ``hdf-buffer  so\_apply  bag-null``  0
  THEN  (RW  LiftAllC  0  THEN  Reduce  0)
  THEN  SqequalSqle
  THEN  OneFixpointLeast
  THEN  Repeat  (MoveToConcl  (-2))
  THEN  NatInd  (-1)
  THEN  (UnivCD  THENA  Auto)
  THEN  Try  (Complete  ((Reduce  0  THEN  Strictness  THEN  Auto)))
  THEN  (RWO  "fun\_exp\_unroll\_1"  0  THENA  Auto))

---

Home Index