---

Step * of Lemma hdf-sqequal6-1

∀[s,F,G:Top].
  (fix((λmk-hdf,s0. (inl (λa.let bs' ⟵ ⋃b∈s0.[G[a;b]]
                             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 Try (RWO "bag-combine-unit-left-top" 0 THENA Auto THEN Reduce 0)⋅
         THEN (RWW "bag-append-empty" 0⋅⋅ THENA Auto))
   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:

---

Latex:
\mforall{}[s,F,G:Top].
    (fix((\mlambda{}mk-hdf,s0.  (inl  (\mlambda{}a.let  bs'  \mleftarrow{}{}  \mcup{}b\mmember{}s0.[G[a;b]]
                                                          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

---

Latex:
(MutualFixpointInduction  `s'
  THEN  RW  (AddrC  [2]  UnrollRecursionC  )  0
  THEN  Reduce  0
  THEN  (RepeatFor  2  (SqLeCD)
              THEN  Try  (RWO  "bag-combine-unit-left-top"  0  THENA  Auto  THEN  Reduce  0)\mcdot{}
              THEN  (RWW  "bag-append-empty"  0\mcdot{}\mcdot{}  THENA  Auto))
  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)\mcdot{})

---

Home Index