---

Step * of Lemma hdf-parallel-transformation2-2

∀[L1,L2,G1,G2,S1,S2,init1,init2:Top]. ∀[m1,m2:ℕ].
  (fix((λmk-hdf,s. (inl (λa.cbva_seq(L1[s;a]; λg.<mk-hdf S1[g;s], G1[g]>; m1))))) init1
   || fix((λmk-hdf,s. (inl (λa.cbva_seq(L2[s;a]; λg.<mk-hdf S2[g;s], G2[g]>; m2))))) init2 
  ~ fix((λmk-hdf,s. (inl (λa.cbva_seq(λn.if n <z m1 then L1[fst(s);a] n
                                         if n <z m1 + m2 then mk_lambdas(L2[snd(s);a] (n - m1);m1)
                                         else mk_lambdas_fun(λg1.mk_lambdas_fun(λg2.(G1[g1] + G2[g2]);m2);m1)
                                         fi ; λg.<mk-hdf 
                                                  <S1[partial_ap_gen(g;(m1 + m2) + 1;0;m1);fst(s)]
                                                  , S2[partial_ap_gen(g;(m1 + m2) + 1;m1;m2);snd(s)]
                                                  >
                                                 , select_fun_last(g;m1 + m2)
                                                 >; (m1 + m2) + 1))))) 
    <init1, init2>)
BY
{ (Auto
   THEN ProcTransRepUR ``hdf-parallel so_apply bag-null empty-bag bag-append lt_int`` 0
   THEN (RW LiftAllC 0 THEN Reduce 0)
   THEN Refine `sqequalSqle` []
   THEN OneFixpointLeast
   THEN RepeatFor 8 (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. L1 : Top
2. m2 : ℕ
3. j : ℤ
4. j ≠ 0
5. 0 < j
6. ∀L2,G1,G2,S1,S2,init1,init2:Top. ∀m1:ℕ.
     (λ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 @ []
                                  in <mk-hdf <X', inr ⋅ >, out>)
                      | inr(y) =>
                      case Y of inl(y) => inl (λa.let Y',ys = y a in let out ⟵ ys in <mk-hdf <inr ⋅ , Y'>, out>) | inr(\000Cy) => inr ⋅ ^j - 1 
      ⊥ 
      <fix((λmk-hdf,s. (inl (λa.cbva_seq(L1 s a; λg.<mk-hdf (S1 g s), G1 g>; m1))))) init1
      , fix((λmk-hdf,s. (inl (λa.cbva_seq(L2 s a; λg.<mk-hdf (S2 g s), G2 g>; m2))))) init2
      > ≤ fix((λmk-hdf,s. (inl (λa.cbva_seq(λn.if (n) < (m1)
                                                  then L1 (fst(s)) a n
                                                  else if (n) < (m1 + m2)
                                                          then mk_lambdas(L2 (snd(s)) a (n - m1);m1)
                                                          else mk_lambdas_fun(λg1.mk_lambdas_fun(λg2.((G1 g1)
                                                                                                     @ (G2 g2));m2);m1);
                                            λg.<mk-hdf 
                                                <S1 partial_ap_gen(g;(m1 + m2) + 1;0;m1) (fst(s))
                                                , S2 partial_ap_gen(g;(m1 + m2) + 1;m1;m2) (snd(s))
                                                >
                                               , select_fun_last(g;m1 + m2)
                                               >; (m1 + m2) + 1))))) 
          <init1, init2>)
7. L2 : Top@i
8. G1 : Top@i
9. G2 : Top@i
10. S1 : Top@i
11. S2 : Top@i
12. init1 : Top@i
13. init2 : Top@i
14. m1 : ℕ@i
⊢ inl (λa.let X',xs = cbva_seq(L1 init1 a; λg.<fix((λmk-hdf,s. (inl (λa.cbva_seq(L1 s a; λg.<mk-hdf (S1 g s), G1 g>;
                                                                                 m1))))) 
                                               (S1 g init1)
                                              , G1 g
                                              >; m1) 
          in let Y',ys = cbva_seq(L2 init2 a; λg.<fix((λmk-hdf,s. (inl (λa.cbva_seq(L2 s a; λg.<mk-hdf (S2 g s), G2 g>;
                                                                                    m2))))) 
                                                  (S2 g init2)
                                                 , G2 g
                                                 >; m2) 
             in let out ⟵ xs @ 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 @ []
                                                in <mk-hdf <X', inr ⋅ >, out>)
                                    | inr(y) =>
                                    case Y
                                     of inl(y) =>
                                     inl (λa.let Y',ys = y a 
                                             in let out ⟵ ys
                                                in <mk-hdf <inr ⋅ , Y'>, out>)
                                     | inr(y) =>
                                     inr ⋅ ^j - 1 
                    ⊥ 
                    <X', Y'>
                   , out
                   >) 
  ≤ fix((λmk-hdf,s. (inl (λa.cbva_seq(λn.if (n) < (m1)
                                            then L1 (fst(s)) a n
                                            else if (n) < (m1 + m2)
                                                    then mk_lambdas(L2 (snd(s)) a (n - m1);m1)
                                                    else mk_lambdas_fun(λg1.mk_lambdas_fun(λg2.((G1 g1)
                                                                                               @ (G2 g2));m2);m1);
                                      λg.<mk-hdf 
                                          <S1 partial_ap_gen(g;(m1 + m2) + 1;0;m1) (fst(s))
                                          , S2 partial_ap_gen(g;(m1 + m2) + 1;m1;m2) (snd(s))
                                          >
                                         , select_fun_last(g;m1 + m2)
                                         >; (m1 + m2) + 1))))) 
    <init1, init2>

2
1. L1 : Top
2. m2 : ℕ
3. j : ℤ
4. j ≠ 0
5. 0 < j
6. ∀L2,G1,G2,S1,S2,init1,init2:Top. ∀m1:ℕ.
     (λmk-hdf,s. (inl (λa.cbva_seq(λn.if (n) < (m1)
                                         then L1 (fst(s)) a n
                                         else if (n) < (m1 + m2)
                                                 then mk_lambdas(L2 (snd(s)) a (n - m1);m1)
                                                 else mk_lambdas_fun(λg1.mk_lambdas_fun(λg2.((G1 g1) @ (G2 g2));m2);m1);
                                   λg.<mk-hdf 
                                       <S1 partial_ap_gen(g;(m1 + m2) + 1;0;m1) (fst(s))
                                       , S2 partial_ap_gen(g;(m1 + m2) + 1;m1;m2) (snd(s))
                                       >
                                      , select_fun_last(g;m1 + m2)
                                      >; (m1 + m2) + 1)))^j - 1 
      ⊥ 
      <init1, init2> ≤ 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 @ []
                                                        in <mk-hdf <X', inr ⋅ >, out>)
                                            | inr(y) =>
                                            case Y
                                             of inl(y) =>
                                             inl (λa.let Y',ys = y a 
                                                     in let out ⟵ ys
                                                        in <mk-hdf <inr ⋅ , Y'>, out>)
                                             | inr(y) =>
                                             inr ⋅ )) 
                       <fix((λmk-hdf,s. (inl (λa.cbva_seq(L1 s a; λg.<mk-hdf (S1 g s), G1 g>; m1))))) init1
                       , fix((λmk-hdf,s. (inl (λa.cbva_seq(L2 s a; λg.<mk-hdf (S2 g s), G2 g>; m2))))) init2
                       >)
7. L2 : Top@i
8. G1 : Top@i
9. G2 : Top@i
10. S1 : Top@i
11. S2 : Top@i
12. init1 : Top@i
13. init2 : Top@i
14. m1 : ℕ@i
⊢ inl (λa.cbva_seq(λn.if (n) < (m1)
                         then L1 init1 a n
                         else if (n) < (m1 + m2)
                                 then mk_lambdas(L2 init2 a (n - m1);m1)
                                 else mk_lambdas_fun(λg1.mk_lambdas_fun(λg2.((G1 g1) @ (G2 g2));m2);m1);
                   λg.<λmk-hdf,s.
                                 (inl (λa.cbva_seq(λn.if (n) < (m1)
                                                         then L1 (fst(s)) a n
                                                         else if (n) < (m1 + m2)
                                                                 then mk_lambdas(L2 (snd(s)) a (n - m1);m1)
                                                                 else mk_lambdas_fun(...;m1); λg.<mk-hdf 
                                                                                                  <S1 
                                                                                                   partial_ap_gen(g;(m1
                                                                                                   + m2)
                                                                                                   + 1;0;m1) 
                                                                                                   (fst(s))
                                                                                                  , S2 
                                                                                                    partial_ap_gen(g;(m1
                                                                                                    + m2)
                                                                                                    + 1;m1;m2) 
                                                                                                    (snd(s))
                                                                                                  >
                                                                                                 , select_fun_last(g;m1
                                                                                                   + m2)
                                                                                                 >; (m1 + m2) + 1)))^j -\000C 1 
                       ⊥ 
                       <S1 partial_ap_gen(g;(m1 + m2) + 1;0;m1) init1, S2 partial_ap_gen(g;(m1 + m2) + 1;m1;m2) init2>
                      , select_fun_last(g;m1 + m2)
                      >; (m1 + m2) + 1)) ≤ 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 @ []
                                                                            in <mk-hdf <X', inr ⋅ >, out>)
                                                                | inr(y) =>
                                                                case Y
                                                                 of inl(y) =>
                                                                 inl (λa.let Y',ys = y a 
                                                                         in let out ⟵ ys
                                                                            in <mk-hdf <inr ⋅ , Y'>, out>)
                                                                 | inr(y) =>
                                                                 inr ⋅ )) 
                                           <fix((λmk-hdf,s. (inl (λa.cbva_seq(L1 s a; λg.<mk-hdf (S1 g s), G1 g>; m1))))\000C) init1
                                           , fix((λmk-hdf,s. (inl (λa.cbva_seq(L2 s a; λg.<mk-hdf (S2 g s), G2 g>; m2)))\000C)) init2
                                           >

---

Latex:

---

Latex:
\mforall{}[L1,L2,G1,G2,S1,S2,init1,init2:Top].  \mforall{}[m1,m2:\mBbbN{}].
    (fix((\mlambda{}mk-hdf,s.  (inl  (\mlambda{}a.cbva\_seq(L1[s;a];  \mlambda{}g.<mk-hdf  S1[g;s],  G1[g]>  m1)))))  init1
      ||  fix((\mlambda{}mk-hdf,s.  (inl  (\mlambda{}a.cbva\_seq(L2[s;a];  \mlambda{}g.<mk-hdf  S2[g;s],  G2[g]>  m2)))))  init2 
    \msim{}  fix((\mlambda{}mk-hdf,s.
                                      (inl  (\mlambda{}a.cbva\_seq(\mlambda{}n.if  n  <z  m1  then  L1[fst(s);a]  n
                                                                                if  n  <z  m1  +  m2  then  mk\_lambdas(L2[snd(s);a]  (n  -  m1);m1)
                                                                                else  mk\_lambdas\_fun(\mlambda{}g1.mk\_lambdas\_fun(\mlambda{}g2.(G1[g1]
                                                                                                                                                                      +  G2[g2]);m2);m1)
                                                                                fi  ;  \mlambda{}g.<mk-hdf 
                                                                                                  <S1[partial\_ap\_gen(g;(m1  +  m2)  +  1;0;m1);fst(s)]
                                                                                                  ,  S2[partial\_ap\_gen(g;(m1  +  m2)  +  1;m1;m2);snd(s)]
                                                                                                  >
                                                                                                ,  select\_fun\_last(g;m1  +  m2)
                                                                                                >  (m1  +  m2)  +  1))))) 
        <init1,  init2>)


By

---

Latex:
(Auto
  THEN  ProcTransRepUR  ``hdf-parallel  so\_apply  bag-null  empty-bag  bag-append  lt\_int``  0
  THEN  (RW  LiftAllC  0  THEN  Reduce  0)
  THEN  Refine  `sqequalSqle`  []
  THEN  OneFixpointLeast
  THEN  RepeatFor  8  (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