---

Step * 1 1 of Lemma local-prior-state-accumulate


1. Info : Type
2. es : EO+(Info)
3. A : Type
4. T : Type
5. X : EClass(A)
6. base : T
7. f : T ─→ A ─→ T
8. e : E@i
9. ∀e1:E
     ((e1 < e)
     ⇒ (prior-state(f;base;X;e1)
        = accumulate (with value x and list item a):
           f x a
          over list:
            X(<e1)
          with starting value:
           base)
        ∈ T))
10. ↑e ∈b prior(X)
11. prior(X) ∈ EClass(E(X))
⊢ (f prior-state(f;base;X;prior(X)(e)) X(prior(X)(e)))
= accumulate (with value x and list item a):
   f x a
  over list:
    X(<prior(X)(e)) @ [X(prior(X)(e))]
  with starting value:
   base)
∈ T
BY
{ ((RWO "list_accum_append" 0 THENA Auto) THEN Reduce 0 THEN EqCD THEN Auto THEN Reduce 0 THEN EqCD THEN Auto)⋅ }

---

Latex:

---

Latex:

1.  Info  :  Type
2.  es  :  EO+(Info)
3.  A  :  Type
4.  T  :  Type
5.  X  :  EClass(A)
6.  base  :  T
7.  f  :  T  {}\mrightarrow{}  A  {}\mrightarrow{}  T
8.  e  :  E@i
9.  \mforall{}e1:E
          ((e1  <  e)
          {}\mRightarrow{}  (prior-state(f;base;X;e1)
                =  accumulate  (with  value  x  and  list  item  a):
                      f  x  a
                    over  list:
                        X(<e1)
                    with  starting  value:
                      base)))
10.  \muparrow{}e  \mmember{}\msubb{}  prior(X)
11.  prior(X)  \mmember{}  EClass(E(X))
\mvdash{}  (f  prior-state(f;base;X;prior(X)(e))  X(prior(X)(e)))
=  accumulate  (with  value  x  and  list  item  a):
      f  x  a
    over  list:
        X(<prior(X)(e))  @  [X(prior(X)(e))]
    with  starting  value:
      base)


By

---

Latex:
((RWO  "list\_accum\_append"  0  THENA  Auto)
  THEN  Reduce  0
  THEN  EqCD
  THEN  Auto
  THEN  Reduce  0
  THEN  EqCD
  THEN  Auto)\mcdot{}

---

Home Index