---

Step * of Lemma hdf-compose1-transformation3

∀[f,L,S,G,init:Top]. ∀[m:ℕ].
  (f o (fix((λmk-hdf,s. (inl (λa.cbva_seq(L[s;a]; λg.<mk-hdf S[s;a;g], G[s;a;g]>; m))))) init) 
  ~ fix((λmk-hdf,s. (inl (λa.cbva_seq(λn.if (n =z m) then mk_lambdas_fun(λg.bag-map(f;G[s;a;g]);m) else L[s;a] n fi ;
                                      λg.<mk-hdf S[s;a;partial_ap(g;m + 1;m)], select_fun_ap(g;m + 1;m)>; m + 1))))) 
    init)
BY
{ (Auto
   THEN ProcTransRepUR ``hdf-compose1 so_apply`` 0
   THEN (RW LiftAllC 0 THEN Reduce 0)
   THEN SqequalSqle
   THEN OneFixpointLeast
   THEN Repeat (MoveToConcl (-2))
   THEN NatInd (-1)
   THEN (UnivCD THENA Auto)
   THEN Try (Complete ((Reduce 0 THEN Strictness THEN Auto)))
   THEN (RWO "fun_exp_unroll_1" 0 THENA Auto)) }

1
1. j : ℤ
2. 0 < j
3. ∀f,L,S,G,init:Top. ∀m:ℕ.
     (λ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,s. (inl (λa.cbva_seq(L s a; λg.<mk-hdf (S s a g), G s a g>; m))))) init) 
      ≤ fix((λmk-hdf,s. (inl (λa.cbva_seq(λn.if n=m  then mk_lambdas_fun(λg.bag-map(f;G s a g);m)  else (L s a n);
                                          λg.<mk-hdf (S s a partial_ap(g;m + 1;m)), select_fun_ap(g;m + 1;m)>; m + 1))))\000C) 
        init)
4. f : Top@i
5. L : Top@i
6. S : Top@i
7. G : Top@i
8. init : Top@i
9. m : ℕ@i
⊢ (λx.((λ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(\000Cy) => inr ⋅ ) 
       (λ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(\000Cy) => inr ⋅ ^j - 1 x))) 
  ⊥ 
  (fix((λmk-hdf,s. (inl (λa.cbva_seq(L s a; λg.<mk-hdf (S s a g), G s a g>; m))))) init) 
  ≤ fix((λmk-hdf,s. (inl (λa.cbva_seq(λn.if n=m  then mk_lambdas_fun(λg.bag-map(f;G s a g);m)  else (L s a n);
                                      λg.<mk-hdf (S s a partial_ap(g;m + 1;m)), select_fun_ap(g;m + 1;m)>; m + 1))))) 
    init

2
1. j : ℤ
2. 0 < j
3. ∀f,L,S,G,init:Top. ∀m:ℕ.
     (λmk-hdf,s. (inl (λa.cbva_seq(λn.if n=m  then mk_lambdas_fun(λg.bag-map(f;G s a g);m)  else (L s a n);
                                   λg.<mk-hdf (S s a partial_ap(g;m + 1;m)), select_fun_ap(g;m + 1;m)>; m + 1)))^j - 1 
      ⊥ 
      init ≤ 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,s. (inl (λa.cbva_seq(L s a; λg.<mk-hdf (S s a g), G s a g>; m))))) init))
4. f : Top@i
5. L : Top@i
6. S : Top@i
7. G : Top@i
8. init : Top@i
9. m : ℕ@i
⊢ (λx.((λmk-hdf,s. (inl (λa.cbva_seq(λn.if n=m  then mk_lambdas_fun(λg.bag-map(f;G s a g);m)  else (L s a n);
                                     λg.<mk-hdf (S s a partial_ap(g;m + 1;m)), select_fun_ap(g;m + 1;m)>; m + 1)))) 
       (λmk-hdf,s. (inl (λa.cbva_seq(λn.if n=m  then mk_lambdas_fun(λg.bag-map(f;G s a g);m)  else (L s a n);
                                     λg.<mk-hdf (S s a partial_ap(g;m + 1;m)), select_fun_ap(g;m + 1;m)>; m + 1)))^j - 1\000C 
        x))) 
  ⊥ 
  init ≤ 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,s. (inl (λa.cbva_seq(L s a; λg.<mk-hdf (S s a g), G s a g>; m))))) init)

---

Latex:


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


By

(Auto
  THEN  ProcTransRepUR  ``hdf-compose1  so\_apply``  0
  THEN  (RW  LiftAllC  0  THEN  Reduce  0)
  THEN  SqequalSqle
  THEN  OneFixpointLeast
  THEN  Repeat  (MoveToConcl  (-2))
  THEN  NatInd  (-1)
  THEN  (UnivCD  THENA  Auto)
  THEN  Try  (Complete  ((Reduce  0  THEN  Strictness  THEN  Auto)))
  THEN  (RWO  "fun\_exp\_unroll\_1"  0  THENA  Auto))

---

Home Index