---

Step * of Lemma hdf-parallel-transformation2-3

∀[L,G,H,S,init,out:Top]. ∀[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 RW LiftAllC 0
   THEN Reduce 0
   THEN UnrollLoopsOnceExcept ``cbva_seq mk_lambdas_fun select_fun_last partial_ap bag-append pi1 pi2``
   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 RW LiftAllC 0
   THEN Reduce 0
   THEN Fold `select_fun_last` 0
   THEN RepeatFor 3 ((MemCD THEN Try (Complete (Auto))))
   THEN Refine `sqequalSqle` []
   THEN OneFixpointLeast
   THEN RepeatFor 9 (MoveToConcl (-2))
   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. j : ℤ
2. j ≠ 0
3. 0 < j
4. ∀L,G,H,S,init,out:Top. ∀m:ℕ. ∀a,g:Base.
     (λmk-hdf,s0. let X,Y = s0 
                  in case X
                      of inl(y) =>
                      inl (λa.let X',xs = y a 
                              in case Y
                                  of inl(P) =>
                                  let Y',ys = P a 
                                  in let out ←─ xs + ys
                                     in <mk-hdf <X', Y'>, out>
                                  | inr(P) =>
                                  let out ←─ xs + Ax
                                  in <mk-hdf <X', inr Ax >, out>)
                      | inr(y) =>
                      case Y of inl(y) => inl (λa.let Y',ys = y a in let out ←─ ys in <mk-hdf <inr Ax , Y'>, out>) | inr\000C(y) => inr Ax ^j - 1 
      ⊥ 
      <inr Ax 
      , case H partial_ap(g;m + 1;m) init
         of inl() =>
         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))))) 
         (S partial_ap(g;m + 1;m) init)
         | inr() =>
         inr Ax 
      > ≤ case H partial_ap(g;m + 1;m) init
       of inl() =>
       fix((λmk-hdf,s. (inl (λa.cbva_seq(λn.if n=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); λ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))))) 
       <inr Ax , S partial_ap(g;m + 1;m) init>
       | inr() =>
       inr Ax )
5. L : Top@i
6. G : Top@i
7. H : Top@i
8. S : Top@i
9. init : Top@i
10. out : Top@i
11. m : ℕ@i
12. a : Base@i
13. g : Base@i
⊢ case case H partial_ap(g;m + 1;m) init
        of inl() =>
        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))))) 
        (S partial_ap(g;m + 1;m) init)
        | inr() =>
        inr Ax 
   of inl(y) =>
   inl (λa.let Y',ys = y a 
           in let out ←─ ys
              in <λmk-hdf,s0. let X,Y = s0 
                              in case X
                                  of inl(y) =>
                                  inl (λa.let X',xs = y a 
                                          in case Y
                                              of inl(P) =>
                                              let Y',ys = P a 
                                              in let out ←─ xs + ys
                                                 in <mk-hdf <X', Y'>, out>
                                              | inr(P) =>
                                              let out ←─ xs + Ax
                                              in <mk-hdf <X', inr Ax >, out>)
                                  | inr(y) =>
                                  case Y
                                   of inl(y) =>
                                   inl (λa.let Y',ys = y a 
                                           in let out ←─ ys
                                              in <mk-hdf <inr Ax , Y'>, out>)
                                   | inr(y) =>
                                   inr Ax ^j - 1 
                  ⊥ 
                  <inr Ax , Y'>
                 , out
                 >)
   | inr(y) =>
   inr Ax  ≤ case H partial_ap(g;m + 1;m) init
   of inl() =>
   fix((λmk-hdf,s. (inl (λa.cbva_seq(λn.if n=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); λ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))))) 
   <inr Ax , S partial_ap(g;m + 1;m) init>
   | inr() =>
   inr Ax 

2
1. j : ℤ
2. j ≠ 0
3. 0 < j
4. ∀L,G,H,S,init,out:Top. ∀m:ℕ. ∀a,g:Base.
     (case H partial_ap(g;m + 1;m) init
       of inl() =>
       λmk-hdf,s. (inl (λa.cbva_seq(λn.if n=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); λ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)))^j - 1 
       ⊥ 
       <inr Ax , S partial_ap(g;m + 1;m) init>
       | inr() =>
       inr Ax  ≤ fix((λmk-hdf,s0. let X,Y = s0 
                                  in case X
                                      of inl(y) =>
                                      inl (λa.let X',xs = y a 
                                              in case Y
                                                  of inl(P) =>
                                                  let Y',ys = P a 
                                                  in let out ←─ xs + ys
                                                     in <mk-hdf <X', Y'>, out>
                                                  | inr(P) =>
                                                  let out ←─ xs + Ax
                                                  in <mk-hdf <X', inr Ax >, out>)
                                      | inr(y) =>
                                      case Y
                                       of inl(y) =>
                                       inl (λa.let Y',ys = y a 
                                               in let out ←─ ys
                                                  in <mk-hdf <inr Ax , Y'>, out>)
                                       | inr(y) =>
                                       inr Ax )) 
                 <inr Ax 
                 , case H partial_ap(g;m + 1;m) init
                    of inl() =>
                    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))))) 
                    (S partial_ap(g;m + 1;m) init)
                    | inr() =>
                    inr Ax 
                 >)
5. L : Top@i
6. G : Top@i
7. H : Top@i
8. S : Top@i
9. init : Top@i
10. out : Top@i
11. m : ℕ@i
12. a : Base@i
13. g : Base@i
⊢ case H partial_ap(g;m + 1;m) init
   of inl() =>
   inl (λa.cbva_seq(λn.if n=m  then mk_lambdas_fun(λg.(G g);m)  else (L (S partial_ap(g;m + 1;m) init) a n);
                    λg@0.<case H partial_ap(g@0;m + 1;m) (S partial_ap(g;m + 1;m) init)
                           of inl() =>
                           λmk-hdf,s. (inl (λa.cbva_seq(λn.if n=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); λ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)))^j - 1 
                           ⊥ 
                           <inr Ax , S partial_ap(g@0;m + 1;m) (S partial_ap(g;m + 1;m) init)>
                           | inr() =>
                           inr Ax 
                         , select_fun_last(g@0;m)
                         >; m + 1))
   | inr() =>
   inr Ax  ≤ fix((λmk-hdf,s0. let X,Y = s0 
                              in case X
                                  of inl(y) =>
                                  inl (λa.let X',xs = y a 
                                          in case Y
                                              of inl(P) =>
                                              let Y',ys = P a 
                                              in let out ←─ xs + ys
                                                 in <mk-hdf <X', Y'>, out>
                                              | inr(P) =>
                                              let out ←─ xs + Ax
                                              in <mk-hdf <X', inr Ax >, out>)
                                  | inr(y) =>
                                  case Y
                                   of inl(y) =>
                                   inl (λa.let Y',ys = y a 
                                           in let out ←─ ys
                                              in <mk-hdf <inr Ax , Y'>, out>)
                                   | inr(y) =>
                                   inr Ax )) 
             <inr Ax 
             , case H partial_ap(g;m + 1;m) init
                of inl() =>
                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))))) 
                (S partial_ap(g;m + 1;m) init)
                | inr() =>
                inr Ax 
             >

---

Latex:


\mforall{}[L,G,H,S,init,out:Top].  \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

(Auto
  THEN  ProcTransRepUR  ``hdf-parallel``  0
  THEN  RW  LiftAllC  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  RW  LiftAllC  0
  THEN  Reduce  0
  THEN  Fold  `select\_fun\_last`  0
  THEN  RepeatFor  3  ((MemCD  THEN  Try  (Complete  (Auto))))
  THEN  Refine  `sqequalSqle`  []
  THEN  OneFixpointLeast
  THEN  RepeatFor  9  (MoveToConcl  (-2))
  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