---

Step * of Lemma hdf-compose1-transformation2

∀[f,L,G:Top]. ∀[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 ProcTransRepUR ``hdf-compose1 so_apply`` 0
   THEN (LiftAll 0 THEN Reduce 0)
   THEN SqequalSqle
   THEN (OneFixpointLeast
         THEN RepeatFor 3 (MoveToConcl (-3))
         THEN NatInd (-1)
         THEN ((UnivCD THENA Auto) THEN (Reduce 0 THEN Strictness THEN Try (Complete (Auto)))⋅)
         THEN (RWO "fun_exp_unroll" 0 THENA Auto)
         THEN AutoSplit)⋅) }

1
1. m : ℕ
2. j : ℤ
3. j ≠ 0
4. 0 < j
5. ∀f,L,G:Top.
     (λmk-hdf,s0. case s0 of inl(y) => inl (λa.let X',bs = y a in let out ⟵ bag-map(f;bs) in <mk-hdf X', out>) | inr(y)\000C => inr ⋅ ^j - 1 ⊥ 
      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=m  then mk_lambdas_fun(λg.bag-map(f;G a g);m)  else (L a n);
                                       λg.<mk-hdf, select_fun_ap(g;m + 1;m)>; m + 1))))))
6. f : Top@i
7. L : Top@i
8. G : Top@i
⊢ inl (λa.let X',bs = cbva_seq(L a; λg.<fix((λmk-hdf.(inl (λa.cbva_seq(L a; λg.<mk-hdf, G a g>; m))))), G a g>; m) 
          in let out ⟵ bag-map(f;bs)
             in <λmk-hdf,s0. case s0
                             of inl(y) =>
                             inl (λa.let X',bs = y a 
                                     in let out ⟵ bag-map(f;bs)
                                        in <mk-hdf X', out>)
                             | inr(y) =>
                             inr ⋅ ^j - 1 
                 ⊥ 
                 X'
                , out
                >) ≤ fix((λmk-hdf.(inl (λa.cbva_seq(λn.if n=m  then mk_lambdas_fun(λg.bag-map(f;G a g);m)  else (L a n);
                                                 λg.<mk-hdf, select_fun_ap(g;m + 1;m)>; m + 1)))))

2
1. m : ℕ
2. j : ℤ
3. j ≠ 0
4. 0 < j
5. ∀f,L,G:Top.
     (λmk-hdf.(inl (λa.cbva_seq(λn.if n=m  then mk_lambdas_fun(λg.bag-map(f;G a g);m)  else (L a n);
                                λg.<mk-hdf, select_fun_ap(g;m + 1;m)>; m + 1)))^j - 1 
      ⊥ ≤ fix((λmk-hdf,s0. case s0 of inl(y) => inl (λa.let X',bs = y a in let out ⟵ bag-map(f;bs) in <mk-hdf X', out>)\000C | inr(y) => inr ⋅ )) 
          fix((λmk-hdf.(inl (λa.cbva_seq(L a; λg.<mk-hdf, G a g>; m))))))
6. f : Top@i
7. L : Top@i
8. G : Top@i
⊢ inl (λa.cbva_seq(λn.if n=m  then mk_lambdas_fun(λg.bag-map(f;G a g);m)  else (L a n);
                   λg.<λmk-hdf.(inl (λa.cbva_seq(λn.if n=m  then mk_lambdas_fun(λg.bag-map(f;G a g);m)  else (L a n);
                                                 λg.<mk-hdf, select_fun_ap(g;m + 1;m)>; m + 1)))^j - 1 
                       ⊥
                      , select_fun_ap(g;m + 1;m)
                      >; m + 1)) ≤ fix((λmk-hdf,s0. case s0
                                                    of inl(y) =>
                                                    inl (λa.let X',bs = y a 
                                                            in let out ⟵ bag-map(f;bs)
                                                               in <mk-hdf X', out>)
                                                    | inr(y) =>
                                                    inr ⋅ )) 
                                   fix((λmk-hdf.(inl (λa.cbva_seq(L a; λg.<mk-hdf, G a g>; m)))))

---

Latex:

---

Latex:
\mforall{}[f,L,G:Top].  \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

---

Latex:
(Auto
  THEN  ProcTransRepUR  ``hdf-compose1  so\_apply``  0
  THEN  (LiftAll  0  THEN  Reduce  0)
  THEN  SqequalSqle
  THEN  (OneFixpointLeast
              THEN  RepeatFor  3  (MoveToConcl  (-3))
              THEN  NatInd  (-1)
              THEN  ((UnivCD  THENA  Auto)  THEN  (Reduce  0  THEN  Strictness  THEN  Try  (Complete  (Auto)))\mcdot{})
              THEN  (RWO  "fun\_exp\_unroll"  0  THENA  Auto)
              THEN  AutoSplit)\mcdot{})

---

Home Index