---

Step * 1 1 of Lemma ml-accum-abort-sq


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. x : B
⊢ F(u)(x) ~ F u x
BY
{ RepeatFor 2 ((RW (AddrC [1] (LemmaC `ml_apply-sq`)) 0 THEN Auto)) }

---

Latex:

---

Latex:

1.  A  :  Type
2.  B  :  Type
3.  F  :  A  {}\mrightarrow{}  B  {}\mrightarrow{}  (B?)
4.  valueall-type(A)
5.  valueall-type(B)
6.  A
7.  B
8.  u  :  A
9.  v  :  A  List
10.  \mforall{}[s:B?].  (ml-accum-abort(F;s;v)  \msim{}  accumulate\_abort(x,sofar.F  x  sofar;s;v))
11.  x  :  B
\mvdash{}  F(u)(x)  \msim{}  F  u  x


By

---

Latex:
RepeatFor  2  ((RW  (AddrC  [1]  (LemmaC  `ml\_apply-sq`))  0  THEN  Auto))

---

Home Index