---

Step * of Lemma hdf-parallel-transformation1

∀[L1,L2:Base]. ∀[m1,m2:ℕ+].
  (fix((λmk-hdf.(inl (λa.simple-cbva-seq(L1[a];λout.<mk-hdf, out>;m1)))))
   || fix((λmk-hdf.(inl (λa.simple-cbva-seq(L2[a];λout.<mk-hdf, out>;m2))))) 
  ~ fix((λmk-hdf.(inl (λa.simple-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(λout1.mk_lambdas(λout2.(out1 + out2);m2 - 1);m1 - 1)
                                             fi ;λout.<mk-hdf, out>;(m1 + m2) + 1))))))
BY
{ (Auto
   THEN RepUR ``hdf-parallel mk-hdf ifthenelse hdf-halted hdf-halt hdf-run isr band btrue hdf-ap`` 0
   THEN LiftAll 0
   THEN Reduce 0
   THEN SqequalInduction
   THEN (UnivCD THENA Auto)
   THEN UnrollLoopsOnceExcept [`simple-cbva-seq`;`mk_lambdas`;`bag-append`;`it`]
   THEN RepeatFor 2 ((RWO "simple-cbva-seq-spread" 0 THENA Auto))
   THEN (RWO "simple-cbva-seq-extend-2" 0 THENA Auto)
   THEN (RWO "simple-cbva-seq-combine" 0 THENA Auto)
   THEN Reduce 0
   THEN RepUR ``ifthenelse lt_int btrue eq_int`` 0
   THEN LiftAll 0
   THEN Reduce 0
   THEN Repeat ((SqequalInductionAuxAux false THEN Try (Complete (Auto))))
   THEN (Subst ⌈m1 + m2 + 1 ~ (m1 + m2) + 1⌉ 0⋅ THENA Auto)
   THEN (RWO "simple-cbva-seq-list-case1" 0 THENA Auto)
   THEN BLemma `simple-cbva-seq-sqequal-n`
   THEN Try (Complete (Auto))
   THEN (Subst ⌈(n - 1 - 1) + 2 ~ n⌉ 0⋅ THENA Auto)
   THEN (Subst ⌈(n - 1 - 1 - (m1 + m2) + 1) + 2 ~ n - (m1 + m2) + 1⌉ 0⋅ THENA Auto)
   THEN (D 0 THENA Auto)
   THEN RepeatFor 2 ((SqequalNCanonicalCD THENA Auto'))
   THEN Try (Complete (Auto))
   THEN (Subst ⌈n - (m1 + m2) + 1 - 1 ~ n - (m1 + m2) + 2⌉ 0⋅ THENA Auto)
   THEN All (RepUR ``it empty-bag nil lt_int btrue bfalse``)
   THEN LiftAll 2
   THEN Reduce 2
   THEN BackThruSomeHyp
   THEN Auto') }

---

Latex:


\mforall{}[L1,L2:Base].  \mforall{}[m1,m2:\mBbbN{}\msupplus{}].
    (fix((\mlambda{}mk-hdf.(inl  (\mlambda{}a.simple-cbva-seq(L1[a];\mlambda{}out.<mk-hdf,  out>m1)))))
      ||  fix((\mlambda{}mk-hdf.(inl  (\mlambda{}a.simple-cbva-seq(L2[a];\mlambda{}out.<mk-hdf,  out>m2))))) 
    \msim{}  fix((\mlambda{}mk-hdf.(inl  (\mlambda{}a.simple-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(\mlambda{}out1.mk\_lambdas(\mlambda{}out2.(out1
                                                                                                                                                                        +  out2);m2 
                                                                                                                                      -  1);m1  -  1)
                                                                                          fi  ;\mlambda{}out.<mk-hdf,  out>(m1  +  m2)  +  1))))))


By

(Auto
  THEN  RepUR  ``hdf-parallel  mk-hdf  ifthenelse  hdf-halted  hdf-halt  hdf-run  isr  band  btrue  hdf-ap``  0
  THEN  LiftAll  0
  THEN  Reduce  0
  THEN  SqequalInduction
  THEN  (UnivCD  THENA  Auto)
  THEN  UnrollLoopsOnceExcept  [`simple-cbva-seq`;`mk\_lambdas`;`bag-append`;`it`]
  THEN  RepeatFor  2  ((RWO  "simple-cbva-seq-spread"  0  THENA  Auto))
  THEN  (RWO  "simple-cbva-seq-extend-2"  0  THENA  Auto)
  THEN  (RWO  "simple-cbva-seq-combine"  0  THENA  Auto)
  THEN  Reduce  0
  THEN  RepUR  ``ifthenelse  lt\_int  btrue  eq\_int``  0
  THEN  LiftAll  0
  THEN  Reduce  0
  THEN  Repeat  ((SqequalInductionAuxAux  false  THEN  Try  (Complete  (Auto))))
  THEN  (Subst  \mkleeneopen{}m1  +  m2  +  1  \msim{}  (m1  +  m2)  +  1\mkleeneclose{}  0\mcdot{}  THENA  Auto)
  THEN  (RWO  "simple-cbva-seq-list-case1"  0  THENA  Auto)
  THEN  BLemma  `simple-cbva-seq-sqequal-n`
  THEN  Try  (Complete  (Auto))
  THEN  (Subst  \mkleeneopen{}(n  -  1  -  1)  +  2  \msim{}  n\mkleeneclose{}  0\mcdot{}  THENA  Auto)
  THEN  (Subst  \mkleeneopen{}(n  -  1  -  1  -  (m1  +  m2)  +  1)  +  2  \msim{}  n  -  (m1  +  m2)  +  1\mkleeneclose{}  0\mcdot{}  THENA  Auto)
  THEN  (D  0  THENA  Auto)
  THEN  RepeatFor  2  ((SqequalNCanonicalCD  THENA  Auto'))
  THEN  Try  (Complete  (Auto))
  THEN  (Subst  \mkleeneopen{}n  -  (m1  +  m2)  +  1  -  1  \msim{}  n  -  (m1  +  m2)  +  2\mkleeneclose{}  0\mcdot{}  THENA  Auto)
  THEN  All  (RepUR  ``it  empty-bag  nil  lt\_int  btrue  bfalse``)
  THEN  LiftAll  2
  THEN  Reduce  2
  THEN  BackThruSomeHyp
  THEN  Auto')

---

Home Index