---

Step * of Lemma ml-accum-abort_wf

∀[A,B:Type]. ∀[s:B?]. ∀[F:A ⟶ B ⟶ (B?)]. ∀[L:A List].
  ml-accum-abort(F;s;L) ∈ B? supposing valueall-type(A) ∧ valueall-type(B) ∧ A ∧ B
BY
{ (Auto THEN RWO  "ml-accum-abort-sq" 0 THEN Auto) }

---

Latex:

---

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


By

---

Latex:
(Auto  THEN  RWO    "ml-accum-abort-sq"  0  THEN  Auto)

---

Home Index