---

Step * 1 1 of Lemma hdf-compose1-transformation1


1. n : ℕ@i
2. ∀n1:ℕn. ∀f,L:Base. ∀m:ℕ+.
     (fix((λmk-hdf,s0. case s0 of inl(y) => inl (λa.let X',bs = y a in let out ←─ map(f;bs) in <mk-hdf X', out>) | inr(y\000C) => inr Ax )) 
      fix((λmk-hdf.(inl (λa.simple-cbva-seq(L a;λout.<mk-hdf, out>;m))))) 
     ~n1 fix((λmk-hdf.(inl (λa.simple-cbva-seq(λn.if n=m
                                                     then mk_lambdas(λout.map(f;out);m - 1)
                                                     else (L a n);λout.<mk-hdf, out>;m + 1))))))@i
3. f : Base@i
4. L : Base@i
5. m : ℕ+@i
6. 0 < n
7. 0 < n - 1
8. a : Base
⊢ simple-cbva-seq(λn.if n=m
                        then mk_lambdas(λout.map(f;out);m - 1)
                        else (L a n);λout.<fix((λmk-hdf,s0. case s0
                                                            of inl(y) =>
                                                            inl (λa.let X',bs = y a 
                                                                    in let out ←─ map(f;bs)
                                                                       in <mk-hdf X', out>)
                                                            | inr(y) =>
                                                            inr Ax )) 
                                           fix((λmk-hdf.(inl (λa.simple-cbva-seq(L a;λout.<mk-hdf, out>;m)))))
                                          , out
                                          >;m + 1) ~n - 1 
- 1 simple-cbva-seq(λn.if n=m
                          then mk_lambdas(λout.map(f;out);m - 1)
                          else (L a 
                                n);λout.<fix((λmk-hdf.(inl (λa.simple-cbva-seq(λn.if n=m
                                                                                     then mk_lambdas(λout.map(f;out);m 
                                                                                          - 1)
                                                                                     else (L a n);λout.<mk-hdf, out>;m
                                                               + 1)))))
                                        , out
                                        >;m + 1)
BY
{ (BLemma `simple-cbva-seq-sqequal-n` THEN Try (Complete (Auto))) }

1
1. n : ℕ@i
2. ∀n1:ℕn. ∀f,L:Base. ∀m:ℕ+.
     (fix((λmk-hdf,s0. case s0 of inl(y) => inl (λa.let X',bs = y a in let out ←─ map(f;bs) in <mk-hdf X', out>) | inr(y\000C) => inr Ax )) 
      fix((λmk-hdf.(inl (λa.simple-cbva-seq(L a;λout.<mk-hdf, out>;m))))) 
     ~n1 fix((λmk-hdf.(inl (λa.simple-cbva-seq(λn.if n=m
                                                     then mk_lambdas(λout.map(f;out);m - 1)
                                                     else (L a n);λout.<mk-hdf, out>;m + 1))))))@i
3. f : Base@i
4. L : Base@i
5. m : ℕ+@i
6. 0 < n
7. 0 < n - 1
8. a : Base
⊢ ((m + 1) ≤ ((n - 1 - 1) + 2))
⇒ (λout.<fix((λmk-hdf,s0. case s0 of inl(y) => inl (λa.let X',bs = y a in let out ←─ map(f;bs) in <mk-hdf X', out>) | i\000Cnr(y) => inr Ax )) 
          fix((λmk-hdf.(inl (λa.simple-cbva-seq(L a;λout.<mk-hdf, out>;m)))))
         , out
         > ~(n - 1 - 1 - m + 1) + 2 λout.<fix((λmk-hdf.(inl (λa.simple-cbva-seq(λn.if n=m
                                                                                      then mk_lambdas(λout.map(f;out);m 
                                                                                           - 1)
                                                                                      else (L a n);λout.<mk-hdf, out>;m
                                                                + 1)))))
                                         , out
                                         >)

---

Latex:



1.  n  :  \mBbbN{}@i
2.  \mforall{}n1:\mBbbN{}n.  \mforall{}f,L:Base.  \mforall{}m:\mBbbN{}\msupplus{}.
          (fix((\mlambda{}mk-hdf,s0.  case  s0
                                              of  inl(y)  =>
                                              inl  (\mlambda{}a.let  X',bs  =  y  a 
                                                              in  let  out  \mleftarrow{}{}  map(f;bs)
                                                                    in  <mk-hdf  X',  out>)
                                              |  inr(y)  =>
                                              inr  Ax  )) 
            fix((\mlambda{}mk-hdf.(inl  (\mlambda{}a.simple-cbva-seq(L  a;\mlambda{}out.<mk-hdf,  out>m))))) 
          \msim{}n1  fix((\mlambda{}mk-hdf.(inl  (\mlambda{}a.simple-cbva-seq(\mlambda{}n.if  n=m
                                                                                                          then  mk\_lambdas(\mlambda{}out.map(f;out);m  -  1)
                                                                                                          else  (L  a  n);\mlambda{}out.<mk-hdf,  out>m  +  1))))))@i
3.  f  :  Base@i
4.  L  :  Base@i
5.  m  :  \mBbbN{}\msupplus{}@i
6.  0  <  n
7.  0  <  n  -  1
8.  a  :  Base
\mvdash{}  simple-cbva-seq(\mlambda{}n.if  n=m
                                                then  mk\_lambdas(\mlambda{}out.map(f;out);m  -  1)
                                                else  (L  a  n);\mlambda{}out.<fix((\mlambda{}mk-hdf,s0.  case  s0
                                                                                                                        of  inl(y)  =>
                                                                                                                        inl  (\mlambda{}a.let  X',bs  =  y  a 
                                                                                                                                        in  let  out  \mleftarrow{}{}  map(f;bs)
                                                                                                                                              in  <mk-hdf  X',  out>)
                                                                                                                        |  inr(y)  =>
                                                                                                                        inr  Ax  )) 
                                                                                      fix((\mlambda{}mk-hdf.(inl  (\mlambda{}a.simple-cbva-seq(L  a;\mlambda{}out.<mk-hdf
                                                                                                                                                                                    ,  out
                                                                                                                                                                                    >m)))))
                                                                                    ,  out
                                                                                    >m  +  1)  \msim{}n  -  1 
-  1  simple-cbva-seq(\mlambda{}n.if  n=m
                                                    then  mk\_lambdas(\mlambda{}out.map(f;out);m  -  1)
                                                    else  (L  a 
                                                                n);\mlambda{}out.<fix((\mlambda{}mk-hdf.(inl  (\mlambda{}a.simple-cbva-seq(\mlambda{}n.if  n=m
                                                                                                                                                                          then  ...
                                                                                                                                                                          else  (L  a 
                                                                                                                                                                                      n);...;m
                                                                                                                              +  1)))))
                                                                                ,  out
                                                                                >m  +  1)


By

(BLemma  `simple-cbva-seq-sqequal-n`  THEN  Try  (Complete  (Auto)))

---

Home Index