Nuprl Lemma : State1-prior
∀[Info,A,B:Type]. ∀[init:Id ─→ B]. ∀[f:Id ─→ A ─→ B ─→ B]. ∀[X:EClass(A)]. ∀[es:EO+(Info)]. ∀[e:E].
(Prior(State1(init;f;X))?λloc.{init loc}(e)
= if first(e) then {init loc(e)} else State1(init;f;X)(pred(e)) fi
∈ bag(B))
Proof
Definitions occuring in Statement :
State1: State1(init;tr;X),
primed-class-opt: Prior(X)?b,
class-ap: X(e),
eclass: EClass(A[eo; e]),
event-ordering+: EO+(Info),
es-first: first(e),
es-pred: pred(e),
es-loc: loc(e),
es-E: E,
Id: Id,
ifthenelse: if b then t else f fi ,
uall: ∀[x:A]. B[x],
apply: f a,
lambda: λx.A[x],
function: x:A ─→ B[x],
universe: Type,
equal: s = t ∈ T,
single-bag: {x},
bag: bag(T)
Lemmas :
es-local-pred_wf,
lt_int_wf,
bag-size_wf,
class-ap_wf,
State1_wf,
nat_wf,
or_wf,
sq_exists_wf,
es-locl_wf,
assert_wf,
all_wf,
not_wf,
eqtt_to_assert,
es-locl-first,
assert_elim,
btrue_neq_bfalse,
eqff_to_assert,
equal_wf,
bool_wf,
bool_cases_sqequal,
subtype_base_sq,
bool_subtype_base,
assert-bnot,
single-bag_wf,
es-loc_wf,
es-E_wf,
event-ordering+_subtype,
event-ordering+_wf,
eclass_wf,
Id_wf,
es-pred_property,
es-pred-locl,
es-causl_weakening,
bag_wf,
iff_weakening_equal,
es-pred_wf,
es-loc-pred,
assert_of_lt_int,
bag-size-bag-member,
State1-loc-exists
Latex:
\mforall{}[Info,A,B:Type]. \mforall{}[init:Id {}\mrightarrow{} B]. \mforall{}[f:Id {}\mrightarrow{} A {}\mrightarrow{} B {}\mrightarrow{} B]. \mforall{}[X:EClass(A)]. \mforall{}[es:EO+(Info)]. \mforall{}[e:E].
(Prior(State1(init;f;X))?\mlambda{}loc.\{init loc\}(e)
= if first(e) then \{init loc(e)\} else State1(init;f;X)(pred(e)) fi )
Date html generated:
2015_07_22-PM-00_25_07
Last ObjectModification:
2015_02_04-PM-04_38_47
Home
Index