---

Step * of Lemma hdf-compose0-transformation1

∀[f,L,S,G,s:Top]. ∀[m:ℕ].
  (hdf-compose0(f;fix((λmk-hdf,s. (inl (λa.cbva_seq(L[s;a]; λg.<mk-hdf S[s;a;g], G[s;a;g]>; m))))) s) 
  ~ fix((λmk-hdf,s. (inl (λa.cbva_seq(λn.if (n =z m) then mk_lambdas_fun(λg.∪b∈G[s;a;g].f b;m) else L[s;a] n fi ;
                                      λg.<mk-hdf S[s;a;partial_ap(g;m + 1;m)], select_fun_last(g;m)>; m + 1))))) 
    s)
BY
{ (Auto
   THEN ProcTransRepUR ``hdf-compose0 so_apply`` 0
   THEN (RW LiftAllC 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. f : Top
2. L : Top
3. m : ℕ
4. j : ℤ
5. j ≠ 0
6. 0 < j
7. ∀S,G,s: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,s. (inl (λa.cbva_seq(L s a; λg.<mk-hdf (S s a g), G s a g>; m))))) s) 
      ≤ fix((λmk-hdf,s. (inl (λa.cbva_seq(λn.if n=m  then mk_lambdas_fun(λg.∪b∈G s a g.f b;m)  else (L s a n);
                                          λg.<mk-hdf (S s a partial_ap(g;m + 1;m)), select_fun_last(g;m)>; m + 1))))) 
        s)
8. S : Top@i
9. G : Top@i
10. s : Top@i
⊢ inl (λa.let X',bs = cbva_seq(L s a; λg.<fix((λmk-hdf,s. (inl (λa.cbva_seq(L s a; λg.<mk-hdf (S s a g), G s a g>; m))))\000C) 
                                          (S s a g)
                                         , G s 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,s. (inl (λa.cbva_seq(λn.if n=m  then mk_lambdas_fun(λg.∪b∈G s a g.f b;m)  else (L s a n);
                                      λg.<mk-hdf (S s a partial_ap(g;m + 1;m)), select_fun_last(g;m)>; m + 1))))) 
    s

2
1. f : Top
2. L : Top
3. m : ℕ
4. j : ℤ
5. j ≠ 0
6. 0 < j
7. ∀S,G,s:Top.
     (λmk-hdf,s. (inl (λa.cbva_seq(λn.if n=m  then mk_lambdas_fun(λg.∪b∈G s a g.f b;m)  else (L s a n);
                                   λg.<mk-hdf (S s a partial_ap(g;m + 1;m)), select_fun_last(g;m)>; m + 1)))^j - 1 
      ⊥ 
      s ≤ 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,s. (inl (λa.cbva_seq(L s a; λg.<mk-hdf (S s a g), G s a g>; m))))) s))
8. S : Top@i
9. G : Top@i
10. s : Top@i
⊢ inl (λa.cbva_seq(λn.if n=m  then mk_lambdas_fun(λg.∪b∈G s a g.f b;m)  else (L s a n);
                   λg.<λmk-hdf,s. (inl (λa.cbva_seq(λn.if n=m  then mk_lambdas_fun(λg.∪b∈G s a g.f b;m)  else (L s a n);
                                                    λg.<mk-hdf (S s a partial_ap(g;m + 1;m)), select_fun_last(g;m)>; m
                                                    + 1)))^j - 1 
                       ⊥ 
                       (S s a partial_ap(g;m + 1;m))
                      , select_fun_last(g;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,s. (inl (λa.cbva_seq(L s a; λg.<mk-hdf (S s a g), G s a g>; m))))) s)

---

Latex:


\mforall{}[f,L,S,G,s:Top].  \mforall{}[m:\mBbbN{}].
    (hdf-compose0(f;fix((\mlambda{}mk-hdf,s.  (inl  (\mlambda{}a.cbva\_seq(L[s;a];  \mlambda{}g.<mk-hdf  S[s;a;g],  G[s;a;g]>  m)))))  s\000C) 
    \msim{}  fix((\mlambda{}mk-hdf,s.  (inl  (\mlambda{}a.cbva\_seq(\mlambda{}n.if  (n  =\msubz{}  m)
                                                                                  then  mk\_lambdas\_fun(\mlambda{}g.\mcup{}b\mmember{}G[s;a;g].f  b;m)
                                                                                  else  L[s;a]  n
                                                                                  fi  ;  \mlambda{}g.<mk-hdf  S[s;a;partial\_ap(g;m  +  1;m)]
                                                                                                  ,  select\_fun\_last(g;m)
                                                                                                  >  m  +  1))))) 
        s)


By

(Auto
  THEN  ProcTransRepUR  ``hdf-compose0  so\_apply``  0
  THEN  (RW  LiftAllC  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