Nuprl Lemma : primed-class-opt-classrel
∀[T,Info:Type]. ∀[X:EClass(T)]. ∀[init:Id ⟶ bag(T)]. ∀[es:EO+(Info)]. ∀[e:E]. ∀[v:T].
uiff(v ∈ Prior(X)?init(e);↓(∃e':E. ((es-p-local-pred(es;λe'.(↓∃w:T. w ∈ X(e'))) e e') ∧ v ∈ X(e')))
∨ ((∀e':E. ((e' <loc e) ⇒ (∀w:T. (¬w ∈ X(e'))))) ∧ v ↓∈ init loc(e)))
Proof
Definitions occuring in Statement :
primed-class-opt: Prior(X)?b,
classrel: v ∈ X(e),
eclass: EClass(A[eo; e]),
event-ordering+: EO+(Info),
es-p-local-pred: es-p-local-pred(es;P),
es-locl: (e <loc e'),
es-loc: loc(e),
es-E: E,
Id: Id,
uiff: uiff(P;Q),
uall: ∀[x:A]. B[x],
all: ∀x:A. B[x],
exists: ∃x:A. B[x],
not: ¬A,
squash: ↓T,
implies: P ⇒ Q,
or: P ∨ Q,
and: P ∧ Q,
apply: f a,
lambda: λx.A[x],
function: x:A ⟶ B[x],
universe: Type,
bag-member: x ↓∈ bs,
bag: bag(T)
Definitions unfolded in proof :
classrel: v ∈ X(e),
primed-class-opt: Prior(X)?b,
member: t ∈ T,
uall: ∀[x:A]. B[x],
eclass: EClass(A[eo; e]),
subtype_rel: A ⊆r B,
nat: ℕ,
all: ∀x:A. B[x],
implies: P ⇒ Q,
so_lambda: λ2x.t[x],
so_apply: x[s],
prop: ℙ,
uimplies: b supposing a,
do-apply: do-apply(f;x),
can-apply: can-apply(f;x),
and: P ∧ Q,
or: P ∨ Q,
isl: isl(x),
outl: outl(x),
assert: ↑b,
ifthenelse: if b then t else f fi ,
btrue: tt,
sq_exists: ∃x:{A| B[x]},
not: ¬A,
false: False,
bfalse: ff,
so_lambda: λ2x y.t[x; y],
so_apply: x[s1;s2],
uiff: uiff(P;Q),
squash: ↓T,
bag-member: x ↓∈ bs,
true: True,
exists: ∃x:A. B[x],
cand: A c∧ B,
es-p-local-pred: es-p-local-pred(es;P),
rev_uimplies: rev_uimplies(P;Q),
sq_stable: SqStable(P),
iff: P ⇐⇒ Q,
es-locl: (e <loc e'),
empty-bag: {},
bag-size: #(bs),
lt_int: i <z j,
guard: {T}
Latex:
\mforall{}[T,Info:Type]. \mforall{}[X:EClass(T)]. \mforall{}[init:Id {}\mrightarrow{} bag(T)]. \mforall{}[es:EO+(Info)]. \mforall{}[e:E]. \mforall{}[v:T].
uiff(v \mmember{} Prior(X)?init(
e);\mdownarrow{}(\mexists{}e':E. ((es-p-local-pred(es;\mlambda{}e'.(\mdownarrow{}\mexists{}w:T. w \mmember{} X(e'))) e e') \mwedge{} v \mmember{} X(e')))
\mvee{} ((\mforall{}e':E. ((e' <loc e) {}\mRightarrow{} (\mforall{}w:T. (\mneg{}w \mmember{} X(e'))))) \mwedge{} v \mdownarrow{}\mmember{} init loc(e)))
Date html generated:
2016_05_16-PM-11_32_38
Last ObjectModification:
2016_01_17-PM-07_20_41
Theory : event-ordering
Home
Index