---

Step * of Lemma ml-accum-abort-sq

∀[A,B:Type]. ∀[F:A ⟶ B ⟶ (B?)].
  ∀[L:A List]. ∀[s:B?].  (ml-accum-abort(F;s;L) ~ accumulate_abort(x,sofar.F x sofar;s;L)) 
  supposing valueall-type(A) ∧ valueall-type(B) ∧ A ∧ B
BY
{ (InductionOnList
   THEN (D 0 THENA Auto)
   THEN Unfold `ml-accum-abort` 0
   THEN (RW (AddrC [1] (LemmaC `ml_apply-sq`)) 0 THEN Auto)
   THEN (RW (AddrC [1;1] (LemmaC `ml_apply-sq`)) 0 THEN Auto)
   THEN RW (AddrC [1;1;1] (LemmaC `ml_apply-sq`)) 0
   THEN Auto
   THEN RW  (SweepUpC UnrollRecursionC) 0
   THEN Reduce 0
   THEN (Fold `ml-accum-abort` 0 ORELSE Trivial)) }

1
1. A : Type
2. B : Type
3. F : A ⟶ B ⟶ (B?)
4. valueall-type(A)
5. valueall-type(B)
6. A
7. B
8. u : A
9. v : A List
10. ∀[s:B?]. (ml-accum-abort(F;s;v) ~ accumulate_abort(x,sofar.F x sofar;s;v))
11. s : B?
⊢ if isr(s) then s else let x.y = [u / v] in ml-accum-abort(F;F(x)(outl(s));y) fi  
~ let s' ⟵ case s of inl(sofar) => F u sofar | inr(_) => s
  in accumulate_abort(x,sofar.F x sofar;s';v)

---

Latex:

---

Latex:
\mforall{}[A,B:Type].  \mforall{}[F:A  {}\mrightarrow{}  B  {}\mrightarrow{}  (B?)].
    \mforall{}[L:A  List].  \mforall{}[s:B?].    (ml-accum-abort(F;s;L)  \msim{}  accumulate\_abort(x,sofar.F  x  sofar;s;L)) 
    supposing  valueall-type(A)  \mwedge{}  valueall-type(B)  \mwedge{}  A  \mwedge{}  B


By

---

Latex:
(InductionOnList
  THEN  (D  0  THENA  Auto)
  THEN  Unfold  `ml-accum-abort`  0
  THEN  (RW  (AddrC  [1]  (LemmaC  `ml\_apply-sq`))  0  THEN  Auto)
  THEN  (RW  (AddrC  [1;1]  (LemmaC  `ml\_apply-sq`))  0  THEN  Auto)
  THEN  RW  (AddrC  [1;1;1]  (LemmaC  `ml\_apply-sq`))  0
  THEN  Auto
  THEN  RW    (SweepUpC  UnrollRecursionC)  0
  THEN  Reduce  0
  THEN  (Fold  `ml-accum-abort`  0  ORELSE  Trivial))

---

Home Index