---

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

∀[Info:Type]. ∀[es:EO+(Info)]. ∀[A,T:Type]. ∀[X:EClass(A)]. ∀[base:T]. ∀[f:T ⟶ A ⟶ T]. ∀[e:E].
  (local-state(f;base;X;e)
  = if e ∈b X then f if e ∈b prior(X) then local-state(f;base;X;prior(X)(e)) else base fi  X(e)
    if e ∈b prior(X) then local-state(f;base;X;prior(X)(e))
    else base
    fi 
  ∈ T)
BY
{ (((Auto THEN RW (AddrC [2] UnfoldTopAbC) 0)
    THEN (InstLemma `es-interface-local-state-prior`  [⌜Info⌝;⌜es⌝;⌜A⌝;⌜T⌝;⌜X⌝;⌜base⌝;⌜f⌝;⌜e⌝]⋅ THENA Auto)
    )
   THEN SplitOnConclITE
   THEN Auto) }

---

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].
    (local-state(f;base;X;e)
    =  if  e  \mmember{}\msubb{}  X  then  f  if  e  \mmember{}\msubb{}  prior(X)  then  local-state(f;base;X;prior(X)(e))  else  base  fi    X(e)
        if  e  \mmember{}\msubb{}  prior(X)  then  local-state(f;base;X;prior(X)(e))
        else  base
        fi  )


By

---

Latex:
(((Auto  THEN  RW  (AddrC  [2]  UnfoldTopAbC)  0)
    THEN  (InstLemma  `es-interface-local-state-prior` 
                [\mkleeneopen{}Info\mkleeneclose{};\mkleeneopen{}es\mkleeneclose{};\mkleeneopen{}A\mkleeneclose{};\mkleeneopen{}T\mkleeneclose{};\mkleeneopen{}X\mkleeneclose{};\mkleeneopen{}base\mkleeneclose{};\mkleeneopen{}f\mkleeneclose{};\mkleeneopen{}e\mkleeneclose{}]\mcdot{}
                THENA  Auto
                )
    )
  THEN  SplitOnConclITE
  THEN  Auto)

---

Home Index