---

Step * 1 of Lemma hdf-compose1-transformation1


1. f : Base
2. L : Base
3. m : ℕ+
⊢ fix((λmk-hdf,s0. if hdf-halted(s0)
                  then hdf-halt()
                  else hdf-run(λa.let s1,b = let X',bs = s0(a) 
                                             in let out ←─ bag-map(f;bs)
                                                in <X', out> 
                                  in <mk-hdf s1, b>)
                  fi )) 
  fix((λmk-hdf.(inl (λa.simple-cbva-seq(L[a];λout.<mk-hdf, out>;m))))) 
~ fix((λmk-hdf.(inl (λa.simple-cbva-seq(λn.if (n =z m)
                                           then mk_lambdas(λout.bag-map(f;out);m - 1)
                                           else L[a] n
                                           fi ;λout.<mk-hdf, out>;m + 1)))))
BY
{ (SqequalInduction
   THEN UnivCD
   THEN Try (Complete (Auto))
   THEN UnrollLoopsOnceExcept [`simple-cbva-seq`;`mk_lambdas`;`null`;`map`]⋅
   THEN (RWO "simple-cbva-seq-spread" 0 THENA Auto)
   THEN (RWO "simple-cbva-seq-extend-2" 0 THENA Auto)
   THEN RepUR ``so_lambda ifthenelse eq_int btrue bfalse`` 0
   THEN RW LiftAllC 0
   THEN Reduce 0
   THEN Repeat ((SqequalInductionAuxAux false THEN Try (Complete (Auto))))
   THEN RepUR ``ifthenelse hdf-halted hdf-halt isr bfalse btrue hdf-run hdf-ap bag-map it so_apply eq_int`` 2
   THEN RW LiftAllC 2
   THEN Reduce 2) }

1
1. n : ℕ@i
2. ∀n1:ℕn. ∀f,L:Base. ∀m:ℕ+.
     (fix((λmk-hdf,s0. case s0 of inl(y) => inl (λa.let X',bs = y a in let out ←─ map(f;bs) in <mk-hdf X', out>) | inr(y\000C) => inr Ax )) 
      fix((λmk-hdf.(inl (λa.simple-cbva-seq(L a;λout.<mk-hdf, out>;m))))) 
     ~n1 fix((λmk-hdf.(inl (λa.simple-cbva-seq(λn.if n=m
                                                     then mk_lambdas(λout.map(f;out);m - 1)
                                                     else (L a n);λout.<mk-hdf, out>;m + 1))))))@i
3. f : Base@i
4. L : Base@i
5. m : ℕ+@i
6. 0 < n
7. 0 < n - 1
8. a : Base
⊢ simple-cbva-seq(λn.if n=m
                        then mk_lambdas(λout.map(f;out);m - 1)
                        else (L a n);λout.<fix((λmk-hdf,s0. case s0
                                                            of inl(y) =>
                                                            inl (λa.let X',bs = y a 
                                                                    in let out ←─ map(f;bs)
                                                                       in <mk-hdf X', out>)
                                                            | inr(y) =>
                                                            inr Ax )) 
                                           fix((λmk-hdf.(inl (λa.simple-cbva-seq(L a;λout.<mk-hdf, out>;m)))))
                                          , out
                                          >;m + 1) ~n - 1 
- 1 simple-cbva-seq(λn.if n=m
                          then mk_lambdas(λout.map(f;out);m - 1)
                          else (L a 
                                n);λout.<fix((λmk-hdf.(inl (λa.simple-cbva-seq(λn.if n=m
                                                                                     then mk_lambdas(λout.map(f;out);m 
                                                                                          - 1)
                                                                                     else (L a n);λout.<mk-hdf, out>;m
                                                               + 1)))))
                                        , out
                                        >;m + 1)

---

Latex:



1.  f  :  Base
2.  L  :  Base
3.  m  :  \mBbbN{}\msupplus{}
\mvdash{}  fix((\mlambda{}mk-hdf,s0.  if  hdf-halted(s0)
                                    then  hdf-halt()
                                    else  hdf-run(\mlambda{}a.let  s1,b  =  let  X',bs  =  s0(a) 
                                                                                          in  let  out  \mleftarrow{}{}  bag-map(f;bs)
                                                                                                in  <X',  out> 
                                                                    in  <mk-hdf  s1,  b>)
                                    fi  )) 
    fix((\mlambda{}mk-hdf.(inl  (\mlambda{}a.simple-cbva-seq(L[a];\mlambda{}out.<mk-hdf,  out>m))))) 
\msim{}  fix((\mlambda{}mk-hdf.(inl  (\mlambda{}a.simple-cbva-seq(\mlambda{}n.if  (n  =\msubz{}  m)
                                                                                      then  mk\_lambdas(\mlambda{}out.bag-map(f;out);m  -  1)
                                                                                      else  L[a]  n
                                                                                      fi  ;\mlambda{}out.<mk-hdf,  out>m  +  1)))))


By

(SqequalInduction
  THEN  UnivCD
  THEN  Try  (Complete  (Auto))
  THEN  UnrollLoopsOnceExcept  [`simple-cbva-seq`;`mk\_lambdas`;`null`;`map`]\mcdot{}
  THEN  (RWO  "simple-cbva-seq-spread"  0  THENA  Auto)
  THEN  (RWO  "simple-cbva-seq-extend-2"  0  THENA  Auto)
  THEN  RepUR  ``so\_lambda  ifthenelse  eq\_int  btrue  bfalse``  0
  THEN  RW  LiftAllC  0
  THEN  Reduce  0
  THEN  Repeat  ((SqequalInductionAuxAux  false  THEN  Try  (Complete  (Auto))))
  THEN  ...
  THEN  RW  LiftAllC  2
  THEN  Reduce  2)

---

Home Index