---

{ [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  X
        then f 
             if e  prior(X)
             then local-state(f;base;X;prior(X)(e))
             else base
             fi  
             X(e)
      if e  prior(X) then local-state(f;base;X;prior(X)(e))
      else base
      fi ) }

{ Proof }

---

Definitions occuring in Statement :  es-interface-local-state: local-state(f;base;X;e),  es-prior-interface: prior(X),  eclass-val: X(e),  in-eclass: e  X,  eclass: EClass(A[eo; e]),  event-ordering+: EO+(Info),  es-E: E,  ifthenelse: if b then t else f fi ,  uall: [x:A]. B[x],  apply: f a,  function: x:A  B[x],  universe: Type,  equal: s = t
Definitions :  uall: [x:A]. B[x],  es-interface-local-state: local-state(f;base;X;e),  member: t  T,  so_lambda: x y.t[x; y],  prop: ,  ifthenelse: if b then t else f fi ,  all: x:A. B[x],  implies: P  Q,  btrue: tt,  bfalse: ff,  and: P  Q,  so_apply: x[s1;s2],  bool: ,  unit: Unit,  iff: P  Q,  uimplies: b supposing a,  subtype: S  T,  it:
Lemmas :  es-interface-local-state-prior,  es-E_wf,  event-ordering+_inc,  eclass_wf,  event-ordering+_wf,  in-eclass_wf,  es-interface-top,  bool_wf,  assert_wf,  not_wf,  bnot_wf,  iff_weakening_uiff,  eqtt_to_assert,  uiff_transitivity,  eqff_to_assert,  assert_of_bnot,  eclass-val_wf

---

\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  )


Date html generated: 2011_08_16-PM-05_34_28
Last ObjectModification: 2011_06_20-AM-01_27_20

Home Index