---

Step * 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. 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)
BY
{ ((D -1 THEN RepUR ``spreadcons`` 0) THEN (CallByValueReduce 0 THEN Auto) THEN RWO "-2" 0 THEN Auto) }

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. x : B
⊢ F(u)(x) ~ F u x

---

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.  s  :  B?
\mvdash{}  if  isr(s)  then  s  else  let  x.y  =  [u  /  v]  in  ml-accum-abort(F;F(x)(outl(s));y)  fi   
\msim{}  let  s'  \mleftarrow{}{}  case  s  of  inl(sofar)  =>  F  u  sofar  |  inr($_{}$)  =>  s
    in  accumulate\_abort(x,sofar.F  x  sofar;s';v)


By

---

Latex:
((D  -1  THEN  RepUR  ``spreadcons``  0)  THEN  (CallByValueReduce  0  THEN  Auto)  THEN  RWO  "-2"  0  THEN  Auto)

---

Home Index