Nuprl Lemma : member-prior-run-events
∀[M:Type ─→ Type]. ∀r:pRunType(P.M[P]). ∀t:ℕ. ∀e:runEvents(r). ((e ∈ prior-run-events(r;t)) ⇐⇒ run-event-step(e) < t)
Proof
Definitions occuring in Statement :
prior-run-events: prior-run-events(r;t),
run-event-step: run-event-step(e),
runEvents: runEvents(r),
pRunType: pRunType(T.M[T]),
l_member: (x ∈ l),
nat: ℕ,
less_than: a < b,
uall: ∀[x:A]. B[x],
so_apply: x[s],
all: ∀x:A. B[x],
iff: P ⇐⇒ Q,
function: x:A ─→ B[x],
universe: Type
Lemmas :
member-mapfilter,
int_seg_wf,
upto_wf,
l_member_wf,
isl_wf,
Id_wf,
pMsg_wf,
unit_wf2,
int_seg_subtype-nat,
false_wf,
top_wf,
ldag_wf,
pInTransit_wf,
runEvents_wf,
assert_wf,
spread_wf,
assert_elim,
and_wf,
equal_wf,
pi1_wf_top,
subtype_rel_product,
subtype_top,
bfalse_wf,
btrue_neq_bfalse,
is-run-event_wf,
assert-eq-id,
true_wf,
set_wf,
nat_wf,
lelt_wf,
member_upto2,
sq_stable__assert,
eq_id_wf
Latex:
\mforall{}[M:Type {}\mrightarrow{} Type]
\mforall{}r:pRunType(P.M[P]). \mforall{}t:\mBbbN{}. \mforall{}e:runEvents(r).
((e \mmember{} prior-run-events(r;t)) \mLeftarrow{}{}\mRightarrow{} run-event-step(e) < t)
Date html generated:
2015_07_23-AM-11_14_03
Last ObjectModification:
2015_01_29-AM-00_11_36
Home
Index