---

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

.....truecase..... 
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)
⊢ (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
{ (InstLemma `es-prior-interface_wf` [⌈Info⌉;⌈X⌉]⋅ THENA Auto) }

1
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

---

Latex:

---

Latex:
.....truecase..... 
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)
\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:
(InstLemma  `es-prior-interface\_wf`  [\mkleeneopen{}Info\mkleeneclose{};\mkleeneopen{}X\mkleeneclose{}]\mcdot{}  THENA  Auto)

---

Home Index