---

Step * of Lemma hdf-sqequal6

∀[s,F,G:Top].
  (fix((λmk-hdf,s0. (inl (λa.let bs' ←─ reduce(λl,l'. (l @ l');[];map(λb.[G[a;b]];s0))
                             in <mk-hdf case null(bs') of inl() => s0 | inr() => bs', F[s0;bs']>)))) 
   [s] ~ fix((λmk-hdf,s0. (inl (λa.let bs' ←─ G[a;s0] in <mk-hdf bs', F[[s0];[bs']]>)))) s)
BY
{ (MutualFixpointInduction `s'
   THEN RW (AddrC [2] UnrollRecursionC ) 0
   THEN Reduce 0
   THEN RepeatFor 2 (SqLeCD)
   THEN (BLemma `callbyvalueall-single-sqle` THENA Auto⋅ ORELSE BLemma `callbyvalueall-single-sqle2` THENA Auto⋅)
   THEN Reduce 0
   THEN (D 0 THENA Auto)
   THEN SqLeCD
   THEN Try (BackThruSomeHyp)
   THEN Auto) }

---

Latex:


\mforall{}[s,F,G:Top].
    (fix((\mlambda{}mk-hdf,s0.  (inl  (\mlambda{}a.let  bs'  \mleftarrow{}{}  reduce(\mlambda{}l,l'.  (l  @  l');[];map(\mlambda{}b.[G[a;b]];s0))
                                                          in  <mk-hdf  case  null(bs')  of  inl()  =>  s0  |  inr()  =>  bs',  F[s0;bs']>))))\000C 
      [s]  \msim{}  fix((\mlambda{}mk-hdf,s0.  (inl  (\mlambda{}a.let  bs'  \mleftarrow{}{}  G[a;s0]  in  <mk-hdf  bs',  F[[s0];[bs']]>))))  s)


By

(MutualFixpointInduction  `s'
  THEN  RW  (AddrC  [2]  UnrollRecursionC  )  0
  THEN  Reduce  0
  THEN  RepeatFor  2  (SqLeCD)
  THEN  (BLemma  `callbyvalueall-single-sqle`  THENA  Auto\mcdot{}
  ORELSE  BLemma  `callbyvalueall-single-sqle2`  THENA  Auto\mcdot{}
  )
  THEN  Reduce  0
  THEN  (D  0  THENA  Auto)
  THEN  SqLeCD
  THEN  Try  (BackThruSomeHyp)
  THEN  Auto)

---

Home Index