Nuprl Lemma : loop-class-state-prior
∀[Info,B:Type]. ∀[X:EClass(B ─→ B)]. ∀[init:Id ─→ bag(B)].
∀es:EO+(Info). ∀e:E.
∀[v:B]
uiff(v ∈ Prior(loop-class-state(X;init))?init(e);((↑first(e)) ∧ v ↓∈ init loc(e))
∨ ((¬↑first(e)) ∧ v ∈ loop-class-state(X;init)(pred(e))))
Proof
Definitions occuring in Statement :
loop-class-state: loop-class-state(X;init),
primed-class-opt: Prior(X)?b,
classrel: v ∈ 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,
assert: ↑b,
uiff: uiff(P;Q),
uall: ∀[x:A]. B[x],
all: ∀x:A. B[x],
not: ¬A,
or: P ∨ Q,
and: P ∧ Q,
apply: f a,
function: x:A ─→ B[x],
universe: Type,
bag-member: x ↓∈ bs,
bag: bag(T)
Lemmas :
primed-class-opt-classrel,
loop-class-state_wf,
sq_stable__bag-member,
es-loc_wf,
event-ordering+_subtype,
es-locl-first,
assert_elim,
btrue_neq_bfalse,
classrel_wf,
es-locl_wf,
es-E_wf,
exists_wf,
es-p-local-pred_wf,
squash_wf,
sq_stable__classrel,
es-pred_wf,
es-pred_property,
es-pred-locl,
es-causl_weakening,
true_wf,
event-ordering+_wf,
eclass_wf,
iff_weakening_equal,
es-loc-pred,
loop-class-state-exists,
subtype_base_sq,
Id_wf,
atom2_subtype_base,
es-init_wf,
es-init-locl,
bag-size-bag-member,
es-loc-init,
and_wf,
equal_wf,
bag_wf,
bag-member_wf,
all_wf,
not_wf,
es-locl_transitivity2,
es-le_weakening_eq,
es-locl_irreflexivity,
es-causl_transitivity2,
es-causle_weakening,
es-causl_irreflexivity
Latex:
\mforall{}[Info,B:Type]. \mforall{}[X:EClass(B {}\mrightarrow{} B)]. \mforall{}[init:Id {}\mrightarrow{} bag(B)].
\mforall{}es:EO+(Info). \mforall{}e:E.
\mforall{}[v:B]
uiff(v \mmember{} Prior(loop-class-state(X;init))?init(e);((\muparrow{}first(e)) \mwedge{} v \mdownarrow{}\mmember{} init loc(e))
\mvee{} ((\mneg{}\muparrow{}first(e)) \mwedge{} v \mmember{} loop-class-state(X;init)(pred(e))))
Date html generated:
2015_07_21-PM-02_33_11
Last ObjectModification:
2015_02_04-PM-06_23_04
Home
Index