---

Step * of Lemma hdf-parallel-transformation2

∀[L,G,H,S,init,out:Base]. ∀[m:ℕ].
  (inl (λa.<inr Ax , out>) || fix((λmk-hdf,s. (inl (λa.cbva_seq(L[s;a]; λg.<case H[g;s]
                                                                             of inl() =>
                                                                             mk-hdf S[g;s]
                                                                             | inr() =>
                                                                             inr Ax 
                                                                           , G[g]
                                                                           >; m))))) 
                              init ~ fix((λmk-hdf,s. (inl (λa.cbva_seq(λn.if (n =z m)
                                                                          then case fst(s)
                                                                                of inl(x) =>
                                                                                mk_lambdas_fun(λg.(out + G[g]);m)
                                                                                | inr(x) =>
                                                                                mk_lambdas_fun(λg.G[g];m)
                                                                          else L[snd(s);a] n
                                                                          fi ; λg.<case H[partial_ap(g;m + 1;m);snd(s)]
                                                                                    of inl() =>
                                                                                    mk-hdf 
                                                                                    <inr Ax 
                                                                                    , S[partial_ap(g;m + 1;m);snd(s)]
                                                                                    >
                                                                                    | inr() =>
                                                                                    inr Ax 
                                                                                  , select_fun_last(g;m)
                                                                                  >; m + 1))))) 
                                     <inl Ax, init>)
BY
{ (Auto
   THEN ProcTransRepUR ``hdf-parallel`` 0
   THEN LiftAll 0
   THEN Reduce 0
   THEN UnrollLoopsOnceExcept [`cbva_seq`;`mk_lambdas_fun`;`select_fun_last`;`partial_ap`;`bag-append`]
   THEN (RWO "cbva_seq-spread" 0 THENA Auto)
   THEN (RWO "cbva_seq_extend" 0 THENA Auto)
   THEN RepUR ``ifthenelse lt_int btrue eq_int`` 0
   THEN LiftAll 0
   THEN Reduce 0
   THEN Fold `select_fun_last` 0
   THEN RepeatFor 3 ((MemCD THEN Try (Complete (Auto))))
   THEN SqequalInduction
   THEN (UnivCD THENA Auto)
   THEN UnrollLoopsOnceExcept [`cbva_seq`;`mk_lambdas_fun`;`select_fun_last`;`partial_ap`;`bag-append`]
   THEN (SqequalNNonCanonicalCD THEN Try (Complete (Auto)))
   THEN RepeatFor 2 ((SqequalNCanonicalCD THEN Try (Complete (Auto))))
   THEN (RWO "cbva_seq-spread" 0 THENA Auto)
   THEN (RWO "cbva_seq_extend" 0 THENA Auto)
   THEN RepUR ``ifthenelse lt_int btrue eq_int`` 0
   THEN LiftAll 0
   THEN Reduce 0
   THEN Fold `select_fun_last` 0
   THEN BLemma `cbva_seq-sqequal-n`
   THEN Try (Complete (Auto))
   THEN RepeatFor 2 ((SqequalNCanonicalCD THEN Try (Complete (Auto))))
   THEN BackThruSomeHyp
   THEN Auto) }

---

Latex:

---

Latex:
\mforall{}[L,G,H,S,init,out:Base].  \mforall{}[m:\mBbbN{}].
    (inl  (\mlambda{}a.<inr  Ax  ,  out>)  ||  fix((\mlambda{}mk-hdf,s.  (inl  (\mlambda{}a.cbva\_seq(L[s;a];  \mlambda{}g.<case  H[g;s]
                                                                                                                                                          of  inl()  =>
                                                                                                                                                          mk-hdf  S[g;s]
                                                                                                                                                          |  inr()  =>
                                                                                                                                                          inr  Ax 
                                                                                                                                                      ,  G[g]
                                                                                                                                                      >  m))))) 
                                                            init 
    \msim{}  fix((\mlambda{}mk-hdf,s.  (inl  (\mlambda{}a.cbva\_seq(\mlambda{}n.if  (n  =\msubz{}  m)
                                                                                  then  case  fst(s)
                                                                                              of  inl(x)  =>
                                                                                              mk\_lambdas\_fun(\mlambda{}g.(out  +  G[g]);m)
                                                                                              |  inr(x)  =>
                                                                                              mk\_lambdas\_fun(\mlambda{}g.G[g];m)
                                                                                  else  L[snd(s);a]  n
                                                                                  fi  ;  \mlambda{}g.<case  H[partial\_ap(g;m  +  1;m);snd(s)]
                                                                                                      of  inl()  =>
                                                                                                      mk-hdf  <inr  Ax  ,  S[partial\_ap(g;m  +  1;m);snd(s)]>
                                                                                                      |  inr()  =>
                                                                                                      inr  Ax 
                                                                                                  ,  select\_fun\_last(g;m)
                                                                                                  >  m  +  1))))) 
        <inl  Ax,  init>)


By

---

Latex:
(Auto
  THEN  ProcTransRepUR  ``hdf-parallel``  0
  THEN  LiftAll  0
  THEN  Reduce  0
  THEN  ...
  THEN  (RWO  "cbva\_seq-spread"  0  THENA  Auto)
  THEN  (RWO  "cbva\_seq\_extend"  0  THENA  Auto)
  THEN  RepUR  ``ifthenelse  lt\_int  btrue  eq\_int``  0
  THEN  LiftAll  0
  THEN  Reduce  0
  THEN  Fold  `select\_fun\_last`  0
  THEN  RepeatFor  3  ((MemCD  THEN  Try  (Complete  (Auto))))
  THEN  SqequalInduction
  THEN  (UnivCD  THENA  Auto)
  THEN  ...
  THEN  (SqequalNNonCanonicalCD  THEN  Try  (Complete  (Auto)))
  THEN  RepeatFor  2  ((SqequalNCanonicalCD  THEN  Try  (Complete  (Auto))))
  THEN  (RWO  "cbva\_seq-spread"  0  THENA  Auto)
  THEN  (RWO  "cbva\_seq\_extend"  0  THENA  Auto)
  THEN  RepUR  ``ifthenelse  lt\_int  btrue  eq\_int``  0
  THEN  LiftAll  0
  THEN  Reduce  0
  THEN  Fold  `select\_fun\_last`  0
  THEN  BLemma  `cbva\_seq-sqequal-n`
  THEN  Try  (Complete  (Auto))
  THEN  RepeatFor  2  ((SqequalNCanonicalCD  THEN  Try  (Complete  (Auto))))
  THEN  BackThruSomeHyp
  THEN  Auto)

---

Home Index