---

Step * of Lemma hdf-once-transformation3

∀[L,G:Top]. ∀[m:ℕ].
  (hdf-once(fix((λmk-hdf.(inl (λa.cbva_seq(L[a]; λg.<mk-hdf, G[a;g]>; m)))))) 
  ~ fix((λmk-hdf.(inl (λa.cbva_seq(L[a]; λg.<case null(G[a;g]) of inl() => mk-hdf | inr() => inr Ax , G[a;g]>; m))))))
BY
{ (Auto
   THEN ProcTransRepUR ``hdf-once bag-null it`` 0
   THEN (RW LiftLemAllC 0 THENA Auto)
   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 SqequalSqle
   THEN OneFixpointLeast
   THEN Repeat (MoveToConcl (-2))
   THEN NatInd (-1)
   THEN (UnivCD THENA Auto)
   THEN Try ((ThinVar `j' THEN UnrollLoopsOnce THEN Strictness THEN Auto))
   THEN (RWO "fun_exp_unroll_1" 0 THENA Auto)
   THEN Reduce 0) }

1
1. j : ℤ
2. 0 < j
3. ∀L,G: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 a g) of inl() => fix((λmk-hdf.(inl (λa.cbva_seq(L a; λg.<mk-hdf, G a g>; m))))) | inr() => inr Ax  
      ≤ case null(G a g)
       of inl() =>
       fix((λmk-hdf.(inl (λa.cbva_seq(L a; λg.<case null(G a g) of inl() => mk-hdf | inr() => inr Ax , G a g>; m)))))
       | inr() =>
       inr Ax )
4. L : Top@i
5. G : Top@i
6. m : ℕ@i
7. a : Base@i
8. g : Base@i
⊢ case case null(G a g) of inl() => fix((λmk-hdf.(inl (λa.cbva_seq(L a; λg.<mk-hdf, G a g>; m))))) | 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 a g)
   of inl() =>
   fix((λmk-hdf.(inl (λa.cbva_seq(L a; λg.<case null(G a g) of inl() => mk-hdf | inr() => inr Ax , G a g>; m)))))
   | inr() =>
   inr Ax 

2
1. j : ℤ
2. 0 < j
3. ∀L,G:Top. ∀m:ℕ. ∀a,g:Base.
     (case null(G a g)
       of inl() =>
       λmk-hdf.(inl (λa.cbva_seq(L a; λg.<case null(G a g) of inl() => mk-hdf | inr() => inr Ax , G a g>; m)))^j - 1 ⊥
       | 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 a g)
                  of inl() =>
                  fix((λmk-hdf.(inl (λa.cbva_seq(L a; λg.<mk-hdf, G a g>; m)))))
                  | inr() =>
                  inr Ax )
4. L : Top@i
5. G : Top@i
6. m : ℕ@i
7. a : Base@i
8. g : Base@i
⊢ case null(G a g)
   of inl() =>
   inl (λa.cbva_seq(L a; λg.<case null(G a g)
                              of inl() =>
                              λmk-hdf.(inl (λa.cbva_seq(L a; λg.<case null(G a g) of inl() => mk-hdf | inr() => inr Ax 
                                                                , G a g
                                                                >; m)))^j - 1 
                              ⊥
                              | inr() =>
                              inr Ax 
                            , G a g
                            >; 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 a g)
              of inl() =>
              fix((λmk-hdf.(inl (λa.cbva_seq(L a; λg.<mk-hdf, G a g>; m)))))
              | inr() =>
              inr Ax 

---

Latex:


\mforall{}[L,G:Top].  \mforall{}[m:\mBbbN{}].
    (hdf-once(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(L[a];  \mlambda{}g.<case  null(G[a;g])  of  inl()  =>  mk-hdf  |  inr()  =>  inr  Ax 
                                                                                        ,  G[a;g]
                                                                                        >  m))))))


By

(Auto
  THEN  ProcTransRepUR  ``hdf-once  bag-null  it``  0
  THEN  (RW  LiftLemAllC  0  THENA  Auto)
  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  SqequalSqle
  THEN  OneFixpointLeast
  THEN  Repeat  (MoveToConcl  (-2))
  THEN  NatInd  (-1)
  THEN  (UnivCD  THENA  Auto)
  THEN  Try  ((ThinVar  `j'  THEN  UnrollLoopsOnce  THEN  Strictness  THEN  Auto))
  THEN  (RWO  "fun\_exp\_unroll\_1"  0  THENA  Auto)
  THEN  Reduce  0)

---

Home Index