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