---

Step * of Lemma hdf-parallel-transformation2-1

∀[L1,L2,G1,G2:Top]. ∀[m1,m2:ℕ].
  (fix((λmk-hdf.(inl (λa.cbva_seq(L1[a]; λg.<mk-hdf, G1[g]>; m1))))) || fix((λmk-hdf.(inl (λa.cbva_seq(L2[a]; λg.<mk-hdf
                                                                                                                 , G2[g]
                                                                                                                 >;
                                                                                                       m2))))) 
  ~ fix((λmk-hdf.(inl (λa.cbva_seq(λn.if n <z m1 then L1[a] n
                                      if n <z m1 + m2 then mk_lambdas(L2[a] (n - m1);m1)
                                      else mk_lambdas_fun(λg1.mk_lambdas_fun(λg2.(G1[g1] + G2[g2]);m2);m1)
                                      fi ; λg.<mk-hdf, select_fun_last(g;m1 + m2)>; (m1 + m2) + 1))))))
BY
{ (Auto
   THEN ProcTransRepUR 
        ``hdf-parallel so_apply bag-null empty-bag bag-append lt_int`` 0⋅
   THEN (LiftAll 0 THEN Reduce 0)
   THEN Refine `sqequalSqle` []
   THEN OneFixpointLeast
   THEN RepeatFor 4 (MoveToConcl (-3))
   THEN NatInd (-1)
   THEN (UnivCD THENA Auto)
   THEN Try (Complete ((UnrollLoopsOnce THEN Strictness THEN Auto)))
   THEN (RWO "fun_exp_unroll" 0 THENA Auto)
   THEN AutoSplit) }

---

Latex:


\mforall{}[L1,L2,G1,G2:Top].  \mforall{}[m1,m2:\mBbbN{}].
    (fix((\mlambda{}mk-hdf.(inl  (\mlambda{}a.cbva\_seq(L1[a];  \mlambda{}g.<mk-hdf,  G1[g]>  m1)))))
      ||  fix((\mlambda{}mk-hdf.(inl  (\mlambda{}a.cbva\_seq(L2[a];  \mlambda{}g.<mk-hdf,  G2[g]>  m2))))) 
    \msim{}  fix((\mlambda{}mk-hdf.(inl  (\mlambda{}a.cbva\_seq(\mlambda{}n.if  n  <z  m1  then  L1[a]  n
                                                                            if  n  <z  m1  +  m2  then  mk\_lambdas(L2[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,  select\_fun\_last(g;m1  +  m2)>  (m1  +  m2)
                                                                      +  1))))))


By

(Auto
  THEN  ProcTransRepUR 
            ``hdf-parallel  so\_apply  bag-null  empty-bag  bag-append  lt\_int``  0\mcdot{}
  THEN  (LiftAll  0  THEN  Reduce  0)
  THEN  Refine  `sqequalSqle`  []
  THEN  OneFixpointLeast
  THEN  RepeatFor  4  (MoveToConcl  (-3))
  THEN  NatInd  (-1)
  THEN  (UnivCD  THENA  Auto)
  THEN  Try  (Complete  ((UnrollLoopsOnce  THEN  Strictness  THEN  Auto)))
  THEN  (RWO  "fun\_exp\_unroll"  0  THENA  Auto)
  THEN  AutoSplit)

---

Home Index