---

Step * of Lemma hdf-sqequal6-2

∀[s,F,G:Top].
  (fix((λmk-hdf,s0. (inl (λa.let bs' ←─ ∪f∈[λb.[G[a;b]]].∪b∈s0.f 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 (((RW (AddrC [1;1] (LemmaC `bag-combine-unit-left-top`)) 0 THENA Auto)
          THEN (RW (AddrC [1;1;1] (LemmaC `bag-combine-unit-left-top`)) 0 THENA Auto)
          THEN ((RWO "bag-append-assoc" 0⋅ THENM Reduce 0)⋅ THENA Auto)
          THEN (RW (AddrC [1;1] (LemmaC `bag-append-empty`)) 0⋅⋅ THENA Auto)⋅
          THEN BLemma `callbyvalueall-single-sqle2` THENA Auto⋅⋅)
   ORELSE ((RW (AddrC [2;1] (LemmaC `bag-combine-unit-left-top`)) 0 THENA Auto)
           THEN (RW (AddrC [2;1;1] (LemmaC `bag-combine-unit-left-top`)) 0 THENA Auto)
           THEN ((RWO "bag-append-assoc" 0⋅ THENM Reduce 0)⋅ THENA Auto)
           THEN (RW (AddrC [2;1] (LemmaC `bag-append-empty`)) 0⋅⋅ THENA Auto)⋅
           THEN BLemma `callbyvalueall-single-sqle` 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{}{}  \mcup{}f\mmember{}[\mlambda{}b.[G[a;b]]].\mcup{}b\mmember{}s0.f  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

(MutualFixpointInduction  `s'
  THEN  RW  (AddrC  [2]  UnrollRecursionC  )  0
  THEN  Reduce  0
  THEN  RepeatFor  2  (SqLeCD)
  THEN  (((RW  (AddrC  [1;1]  (LemmaC  `bag-combine-unit-left-top`))  0  THENA  Auto)
                THEN  (RW  (AddrC  [1;1;1]  (LemmaC  `bag-combine-unit-left-top`))  0  THENA  Auto)
                THEN  ((RWO  "bag-append-assoc"  0\mcdot{}  THENM  Reduce  0)\mcdot{}  THENA  Auto)
                THEN  (RW  (AddrC  [1;1]  (LemmaC  `bag-append-empty`))  0\mcdot{}\mcdot{}  THENA  Auto)\mcdot{}
                THEN  BLemma  `callbyvalueall-single-sqle2`  THENA  Auto\mcdot{}\mcdot{})
  ORELSE  ((RW  (AddrC  [2;1]  (LemmaC  `bag-combine-unit-left-top`))  0  THENA  Auto)
                  THEN  (RW  (AddrC  [2;1;1]  (LemmaC  `bag-combine-unit-left-top`))  0  THENA  Auto)
                  THEN  ((RWO  "bag-append-assoc"  0\mcdot{}  THENM  Reduce  0)\mcdot{}  THENA  Auto)
                  THEN  (RW  (AddrC  [2;1]  (LemmaC  `bag-append-empty`))  0\mcdot{}\mcdot{}  THENA  Auto)\mcdot{}
                  THEN  BLemma  `callbyvalueall-single-sqle`  THENA  Auto\mcdot{}\mcdot{})\mcdot{}
  )
  THEN  (Reduce  0  THEN  (D  0  THENA  Auto)  THEN  SqLeCD  THEN  Try  (BackThruSomeHyp)  THEN  Auto)\mcdot{})

---

Home Index