---

Step * of Lemma hdf-parallel-transformation1-2-1

∀[L1,L2,G1,G2,S1,S2,init1,init2:Base]. ∀[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 ...
   THEN LiftAll 0
   THEN Reduce 0
   THEN SqequalInduction
   THEN (UnivCD THENA Auto)
   THEN ...
   THEN RepeatFor 2 ((RWO "cbva_seq-spread" 0 THENA Auto))
   THEN (RWO "cbva_seq_extend" 0 THENA Auto)
   THEN (RWO "cbva_seq-combine2" 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 "cbva_seq-list-case2" 0 THENA Auto)
   THEN BLemma `cbva_seq-sqequal-n`
   THEN Try (Complete (Auto'))
   THEN Fold `select_fun_last` 0
   THEN RepeatFor 2 ((SqequalNCanonicalCD THENA Auto'))
   THEN Try (Complete (Auto))
   THEN Try (Complete ((RWO "select_fun_last_partial_ap_gen1" 0 THEN Auto)))
   THEN (Subst ⌈partial_ap(partial_ap_gen(g;(m1 + m2) + 1;m1;m2 + 1);m2 + 1;m2) ~ partial_ap_gen(g;(m1 + m2) + 1;m1;m2)⌉
          0⋅
         THENA (BLemma `partial_ap_of_partial_ap_gen1` THEN Auto)
         )
   THEN (Subst ⌈partial_ap(g;(m1 + m2) + 1;m1) ~ partial_ap_gen(g;(m1 + m2) + 1;0;m1)⌉ 0⋅
         THENA (BLemma `partial_ap_is_gen` THEN Auto')
         )
   THEN All (RepUR ``pi1 pi2``)
   THEN BackThruSomeHyp
   THEN Auto) }

---

Latex:


\mforall{}[L1,L2,G1,G2,S1,S2,init1,init2:Base].  \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

(Auto
  THEN  ...
  THEN  LiftAll  0
  THEN  Reduce  0
  THEN  SqequalInduction
  THEN  (UnivCD  THENA  Auto)
  THEN  ...
  THEN  RepeatFor  2  ((RWO  "cbva\_seq-spread"  0  THENA  Auto))
  THEN  (RWO  "cbva\_seq\_extend"  0  THENA  Auto)
  THEN  (RWO  "cbva\_seq-combine2"  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  "cbva\_seq-list-case2"  0  THENA  Auto)
  THEN  BLemma  `cbva\_seq-sqequal-n`
  THEN  Try  (Complete  (Auto'))
  THEN  Fold  `select\_fun\_last`  0
  THEN  RepeatFor  2  ((SqequalNCanonicalCD  THENA  Auto'))
  THEN  Try  (Complete  (Auto))
  THEN  Try  (Complete  ((RWO  "select\_fun\_last\_partial\_ap\_gen1"  0  THEN  Auto)))
  THEN  (Subst  \mkleeneopen{}partial\_ap(partial\_ap\_gen(g;(m1  +  m2)  +  1;m1;m2  +  1);m2  +  1;m2)  \msim{}  partial\_ap\_gen(g;(m1
                            +  m2)
                            +  1;m1;m2)\mkleeneclose{}  0\mcdot{}
              THENA  (BLemma  `partial\_ap\_of\_partial\_ap\_gen1`  THEN  Auto)
              )
  THEN  (Subst  \mkleeneopen{}partial\_ap(g;(m1  +  m2)  +  1;m1)  \msim{}  partial\_ap\_gen(g;(m1  +  m2)  +  1;0;m1)\mkleeneclose{}  0\mcdot{}
              THENA  (BLemma  `partial\_ap\_is\_gen`  THEN  Auto')
              )
  THEN  All  (RepUR  ``pi1  pi2``)
  THEN  BackThruSomeHyp
  THEN  Auto)

---

Home Index