---

Step * of Lemma hdf-once-transformation2

∀[L,G,S,init:Top]. ∀[m:ℕ].
  (hdf-once(fix((λmk-hdf,s. (inl (λa.cbva_seq(L[s;a]; λg.<mk-hdf S[g;s], G[g]>; m))))) init) 
  ~ fix((λmk-hdf,s. (inl (λa.cbva_seq(L[s;a]; λg.<case null(G[g]) of inl() => mk-hdf S[g;s] | inr() => inr Ax , G[g]>;
                                      m))))) 
    init)
BY
{ (Auto
   THEN ProcTransRepUR ``hdf-once bag-null it`` 0
   THEN LiftAll 0
   THEN Reduce 0
   THEN UnrollLoopsOnceExcept [`cbva_seq`;`null`]
   THEN (RWO "cbva_seq-spread" 0 THENA Auto)
   THEN RepeatFor 3 ((MemCD THEN Try (Complete (Auto))))
   THEN Refine `sqequalSqle` []
   THEN OneFixpointLeast
   THEN RepeatFor 7 (MoveToConcl (-2))
   THEN NatInd (-1)
   THEN (UnivCD THENA Auto)
   THEN Try ((ThinVar `j' THEN UnrollLoopsOnce THEN Strictness THEN Auto))
   THEN (RWO "fun_exp_unroll" 0 THENA Auto)
   THEN AutoSplit) }

1
1. j : ℤ
2. j ≠ 0
3. 0 < j
4. ∀L,G,S,init:Top. ∀m:ℕ. ∀a,g:Base.
     (λmk-hdf,s0. case s0
                  of inl(y) =>
                  inl (λa.let X',b = y a 
                          in <mk-hdf case null(b) of inl() => X' | inr() => inr Ax , b>)
                  | inr(y) =>
                  inr Ax ^j - 1 
      ⊥ 
      case null(G g)
       of inl() =>
       fix((λmk-hdf,s. (inl (λa.cbva_seq(L s a; λg.<mk-hdf (S g s), G g>; m))))) (S g init)
       | inr() =>
       inr Ax  ≤ case null(G g)
       of inl() =>
       fix((λmk-hdf,s. (inl (λa.cbva_seq(L s a; λg.<case null(G g) of inl() => mk-hdf (S g s) | inr() => inr Ax , G g>;
                                         m))))) 
       (S g init)
       | inr() =>
       inr Ax )
5. L : Top@i
6. G : Top@i
7. S : Top@i
8. init : Top@i
9. m : ℕ@i
10. a : Base@i
11. g : Base@i
⊢ case case null(G g)
        of inl() =>
        fix((λmk-hdf,s. (inl (λa.cbva_seq(L s a; λg.<mk-hdf (S g s), G g>; m))))) (S g init)
        | inr() =>
        inr Ax 
   of inl(y) =>
   inl (λa.let X',b = y a 
           in <λmk-hdf,s0. case s0
                           of inl(y) =>
                           inl (λa.let X',b = y a 
                                   in <mk-hdf case null(b) of inl() => X' | inr() => inr Ax , b>)
                           | inr(y) =>
                           inr Ax ^j - 1 
               ⊥ 
               case null(b) of inl() => X' | inr() => inr Ax 
              , b
              >)
   | inr(y) =>
   inr Ax  ≤ case null(G g)
   of inl() =>
   fix((λmk-hdf,s. (inl (λa.cbva_seq(L s a; λg.<case null(G g) of inl() => mk-hdf (S g s) | inr() => inr Ax , G g>; m)))\000C)) 
   (S g init)
   | inr() =>
   inr Ax 

2
1. j : ℤ
2. j ≠ 0
3. 0 < j
4. ∀L,G,S,init:Top. ∀m:ℕ. ∀a,g:Base.
     (case null(G g)
       of inl() =>
       λmk-hdf,s. (inl (λa.cbva_seq(L s a; λg.<case null(G g) of inl() => mk-hdf (S g s) | inr() => inr Ax , G g>; m)))^\000Cj - 1 ⊥ 
       (S g init)
       | inr() =>
       inr Ax  ≤ fix((λmk-hdf,s0. case s0
                                  of inl(y) =>
                                  inl (λa.let X',b = y a 
                                          in <mk-hdf case null(b) of inl() => X' | inr() => inr Ax , b>)
                                  | inr(y) =>
                                  inr Ax )) 
                 case null(G g)
                  of inl() =>
                  fix((λmk-hdf,s. (inl (λa.cbva_seq(L s a; λg.<mk-hdf (S g s), G g>; m))))) (S g init)
                  | inr() =>
                  inr Ax )
5. L : Top@i
6. G : Top@i
7. S : Top@i
8. init : Top@i
9. m : ℕ@i
10. a : Base@i
11. g : Base@i
⊢ case null(G g)
   of inl() =>
   inl (λa.cbva_seq(L (S g init) a; λg@0.<case null(G g@0)
                                           of inl() =>
                                           λmk-hdf,s. (inl (λa.cbva_seq(L s a; λg.<case null(G g)
                                                                                    of inl() =>
                                                                                    mk-hdf (S g s)
                                                                                    | inr() =>
                                                                                    inr Ax 
                                                                                  , G g
                                                                                  >; m)))^j - 1 
                                           ⊥ 
                                           (S g@0 (S g init))
                                           | inr() =>
                                           inr Ax 
                                         , G g@0
                                         >; m))
   | inr() =>
   inr Ax  ≤ fix((λmk-hdf,s0. case s0
                              of inl(y) =>
                              inl (λa.let X',b = y a 
                                      in <mk-hdf case null(b) of inl() => X' | inr() => inr Ax , b>)
                              | inr(y) =>
                              inr Ax )) 
             case null(G g)
              of inl() =>
              fix((λmk-hdf,s. (inl (λa.cbva_seq(L s a; λg.<mk-hdf (S g s), G g>; m))))) (S g init)
              | inr() =>
              inr Ax 

---

Latex:


\mforall{}[L,G,S,init:Top].  \mforall{}[m:\mBbbN{}].
    (hdf-once(fix((\mlambda{}mk-hdf,s.  (inl  (\mlambda{}a.cbva\_seq(L[s;a];  \mlambda{}g.<mk-hdf  S[g;s],  G[g]>  m)))))  init) 
    \msim{}  fix((\mlambda{}mk-hdf,s.  (inl  (\mlambda{}a.cbva\_seq(L[s;a];  \mlambda{}g.<case  null(G[g])
                                                                                                      of  inl()  =>
                                                                                                      mk-hdf  S[g;s]
                                                                                                      |  inr()  =>
                                                                                                      inr  Ax 
                                                                                                  ,  G[g]
                                                                                                  >  m))))) 
        init)


By

(Auto
  THEN  ProcTransRepUR  ``hdf-once  bag-null  it``  0
  THEN  LiftAll  0
  THEN  Reduce  0
  THEN  UnrollLoopsOnceExcept  [`cbva\_seq`;`null`]
  THEN  (RWO  "cbva\_seq-spread"  0  THENA  Auto)
  THEN  RepeatFor  3  ((MemCD  THEN  Try  (Complete  (Auto))))
  THEN  Refine  `sqequalSqle`  []
  THEN  OneFixpointLeast
  THEN  RepeatFor  7  (MoveToConcl  (-2))
  THEN  NatInd  (-1)
  THEN  (UnivCD  THENA  Auto)
  THEN  Try  ((ThinVar  `j'  THEN  UnrollLoopsOnce  THEN  Strictness  THEN  Auto))
  THEN  (RWO  "fun\_exp\_unroll"  0  THENA  Auto)
  THEN  AutoSplit)

---

Home Index