---

Step * of Lemma es-interface-local-state-prior

∀[Info:Type]. ∀[es:EO+(Info)]. ∀[A,T:Type]. ∀[X:EClass(A)]. ∀[base:T]. ∀[f:T ─→ A ─→ T]. ∀[e:E].
  (prior-state(f;base;X;e) = if e ∈b prior(X) then local-state(f;base;X;prior(X)(e)) else base fi  ∈ T)
BY
{ 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
⊢ prior-state(f;base;X;e) = if e ∈b prior(X) then local-state(f;base;X;prior(X)(e)) else base fi  ∈ T

---

Latex:

---

Latex:
\mforall{}[Info:Type].  \mforall{}[es:EO+(Info)].  \mforall{}[A,T:Type].  \mforall{}[X:EClass(A)].  \mforall{}[base:T].  \mforall{}[f:T  {}\mrightarrow{}  A  {}\mrightarrow{}  T].  \mforall{}[e:E].
    (prior-state(f;base;X;e)  =  if  e  \mmember{}\msubb{}  prior(X)  then  local-state(f;base;X;prior(X)(e))  else  base  fi  )


By

---

Latex:
Auto

---

Home Index