---

Step * of Lemma hdf-compose0-transformation2

∀[f,L,G:Top]. ∀[m:ℕ].
  (hdf-compose0(f;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.⋃b∈G[a;g].f b;m) else L[a] n fi ;
                                   λg.<mk-hdf, select_fun_ap(g;m + 1;m)>; m + 1))))))
BY
{ (Auto
   THEN ProcTransRepUR ``hdf-compose0 so_apply`` 0
   THEN (LiftAll 0 THEN Reduce 0)
   THEN Refine `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 ⟵ ⋃b∈bs.f b in <mk-hdf X', out>) | inr(y) => \000Cinr ⋅ ^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.⋃b∈G a g.f b;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 ⟵ ⋃b∈bs.f b
             in <λmk-hdf,s0. case s0 of inl(y) => inl (λa.let X',bs = y a in let out ⟵ ⋃b∈bs.f b in <mk-hdf X', out>) |\000C inr(y) => inr ⋅ ^j - 1 ⊥ X', out>) 
  ≤ fix((λmk-hdf.(inl (λa.cbva_seq(λn.if n=m  then mk_lambdas_fun(λg.⋃b∈G a g.f b;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.⋃b∈G a g.f b;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 ⟵ ⋃b∈bs.f b in <mk-hdf X', out>) | i\000Cnr(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.⋃b∈G a g.f b;m)  else (L a n);
                   λg.<λmk-hdf.(inl (λa.cbva_seq(λn.if n=m  then mk_lambdas_fun(λg.⋃b∈G a g.f b;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 ⟵ ⋃b∈bs.f b
                                                               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{}].
    (hdf-compose0(f;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.\mcup{}b\mmember{}G[a;g].f  b;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-compose0  so\_apply``  0
  THEN  (LiftAll  0  THEN  Reduce  0)
  THEN  Refine  `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)

---

Home Index