---

Step * of Lemma hdf-with-state-pair-left-axiom

∀[L,S,G,init:Top]. ∀[m:ℕ].
  (fix((λmk-hdf,s. (inl (λa.cbva_seq(L[s;a]; λg.<mk-hdf <Ax, S[s;a;g]>, G[s;a;g]>; m))))) <Ax, init> ~ fix((λmk-hdf,s. (\000Cinl (λa.cbva_seq(L[<Ax, s>;a]; λg.<mk-hdf S[<Ax, s>;a;g], G[<Ax, s>;a;g]>; m))))) init)
BY
{ ((UnivCD THENA Auto)
   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)
   THEN Reduce 0
   THEN RW (AddrC [2] (UnrollLoopsOnceExceptC SqequalProcTransLst)) 0
   THEN Reduce 0
   THEN All (RepUR ``so_apply``)
   THEN RepeatFor 5 ((SqLeCD THEN Try (Complete (Auto))))
   THEN BackThruSomeHyp) }

---

Latex:


\mforall{}[L,S,G,init:Top].  \mforall{}[m:\mBbbN{}].
    (fix((\mlambda{}mk-hdf,s.  (inl  (\mlambda{}a.cbva\_seq(L[s;a];  \mlambda{}g.<mk-hdf  <Ax,  S[s;a;g]>,  G[s;a;g]>  m)))))  <Ax,  init>\000C  \msim{}  fix((\mlambda{}mk-hdf,s.  (inl  (\mlambda{}a.cbva\_seq(L[<Ax,  s>a];  \mlambda{}g.<mk-hdf  S[<Ax,  s>a;g],  G[<Ax,  s>a;g]>  m))))\000C)  init)


By

((UnivCD  THENA  Auto)
  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)
  THEN  Reduce  0
  THEN  RW  (AddrC  [2]  (UnrollLoopsOnceExceptC  SqequalProcTransLst))  0
  THEN  Reduce  0
  THEN  All  (RepUR  ``so\_apply``)
  THEN  RepeatFor  5  ((SqLeCD  THEN  Try  (Complete  (Auto))))
  THEN  BackThruSomeHyp)

---

Home Index