---

Step * of Lemma hdf-compose1-transformation1-2

∀[f,L,G:Base]. ∀[m:ℕ].
  (f o fix((λmk-hdf.(inl (λa.cbva_seq(L[a]; λg.<mk-hdf, G[a;g]>; m))))) 
  ~ fix((λmk-hdf.(inl (λa.cbva_seq(λn.if (n =z m) then mk_lambdas_fun(λg.bag-map(f;G[a;g]);m) else L[a] n fi ;
                                   λg.<mk-hdf, select_fun_ap(g;m + 1;m)>; m + 1))))))
BY
{ (Auto
   THEN RepUR ``hdf-compose1 mk-hdf hdf-halt hdf-halted isr hdf-ap hdf-run ifthenelse eq_int btrue bfalse so_apply`` 0
   THEN RW LiftAllC 0
   THEN Reduce 0
   THEN SqequalInduction
   THEN (UnivCD THENA Auto)
   THEN UnrollLoopsOnceExcept [`cbva_seq`;`mk_lambdas_fun`;`select_fun_ap`;`bag-map`;`it`]
   THEN (RWO "cbva_seq-spread" 0 THENA Auto)
   THEN (RWO "cbva_seq_extend" 0 THENA Auto)
   THEN RepUR ``ifthenelse eq_int btrue bfalse`` 0
   THEN RW LiftAllC 0
   THEN Reduce 0
   THEN Repeat ((SqequalInductionAuxAux false THEN Try (Complete (Auto))))
   THEN BLemma `cbva_seq-sqequal-n`
   THEN Try (Complete (Auto))
   THEN Repeat ((SqequalNCanonicalCD THENA Auto'))
   THEN Try (Complete (Auto))
   THEN BackThruSomeHyp
   THEN Auto) }

---

Latex:


\mforall{}[f,L,G:Base].  \mforall{}[m:\mBbbN{}].
    (f  o  fix((\mlambda{}mk-hdf.(inl  (\mlambda{}a.cbva\_seq(L[a];  \mlambda{}g.<mk-hdf,  G[a;g]>  m))))) 
    \msim{}  fix((\mlambda{}mk-hdf.(inl  (\mlambda{}a.cbva\_seq(\mlambda{}n.if  (n  =\msubz{}  m)
                                                                            then  mk\_lambdas\_fun(\mlambda{}g.bag-map(f;G[a;g]);m)
                                                                            else  L[a]  n
                                                                            fi  ;  \mlambda{}g.<mk-hdf,  select\_fun\_ap(g;m  +  1;m)>  m  +  1))))))


By

(Auto
  THEN  ...
  THEN  RW  LiftAllC  0
  THEN  Reduce  0
  THEN  SqequalInduction
  THEN  (UnivCD  THENA  Auto)
  THEN  UnrollLoopsOnceExcept  [`cbva\_seq`;`mk\_lambdas\_fun`;`select\_fun\_ap`;`bag-map`;`it`]
  THEN  (RWO  "cbva\_seq-spread"  0  THENA  Auto)
  THEN  (RWO  "cbva\_seq\_extend"  0  THENA  Auto)
  THEN  RepUR  ``ifthenelse  eq\_int  btrue  bfalse``  0
  THEN  RW  LiftAllC  0
  THEN  Reduce  0
  THEN  Repeat  ((SqequalInductionAuxAux  false  THEN  Try  (Complete  (Auto))))
  THEN  BLemma  `cbva\_seq-sqequal-n`
  THEN  Try  (Complete  (Auto))
  THEN  Repeat  ((SqequalNCanonicalCD  THENA  Auto'))
  THEN  Try  (Complete  (Auto))
  THEN  BackThruSomeHyp
  THEN  Auto)

---

Home Index