---

Step * of Lemma hdf-once-transformation1

∀[L,G,S,init:Base]. ∀[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 SqequalInduction
   THEN (UnivCD THENA Auto)
   THEN UnrollLoopsOnceExcept [`cbva_seq`;`null`]
   THEN (RWO "cbva_seq-spread" 0 THENA Auto)
   THEN (SqequalNNonCanonicalCD THEN Try (Complete (Auto)))
   THEN Repeat ((SqequalNCanonicalCD THEN Try (Complete (Auto))))
   THEN BLemma `cbva_seq-sqequal-n`
   THEN Try (Complete (Auto))
   THEN Repeat ((SqequalNCanonicalCD THEN Try (Complete (Auto))))
   THEN BackThruSomeHyp
   THEN Auto) }

---

Latex:


\mforall{}[L,G,S,init:Base].  \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  SqequalInduction
  THEN  (UnivCD  THENA  Auto)
  THEN  UnrollLoopsOnceExcept  [`cbva\_seq`;`null`]
  THEN  (RWO  "cbva\_seq-spread"  0  THENA  Auto)
  THEN  (SqequalNNonCanonicalCD  THEN  Try  (Complete  (Auto)))
  THEN  Repeat  ((SqequalNCanonicalCD  THEN  Try  (Complete  (Auto))))
  THEN  BLemma  `cbva\_seq-sqequal-n`
  THEN  Try  (Complete  (Auto))
  THEN  Repeat  ((SqequalNCanonicalCD  THEN  Try  (Complete  (Auto))))
  THEN  BackThruSomeHyp
  THEN  Auto)

---

Home Index