Nuprl Lemma : member-run-event-interval
[M:Type 
Type]
r:pRunType(P.M[P]). e1,e2,e:runEvents(r).
((e 
run-event-interval(r;e1;e2))
(run-event-loc(e) = run-event-loc(e1))
(run-event-step(e1) 
run-event-step(e))
(run-event-step(e) run-event-step(e2)))
Proof not projected
Definitions occuring in Statement :
run-event-interval: run-event-interval(r;e1;e2),
run-event-step: run-event-step(e),
run-event-loc: run-event-loc(e),
runEvents: runEvents(r),
pRunType: pRunType(T.M[T]),
Id: Id,
uall: [x:A]. B[x],
so_apply: x[s],
le: A B,
all: x:A. B[x],
iff: P Q,
and: P Q,
function: x:A B[x],
universe: Type,
equal: s = t,
l_member: (x l)
Definitions :
squash: 
T,
rev_implies: P Q,
iff: P Q,
true: True,
ifthenelse: if b then t else f fi ,
btrue: tt,
implies: P Q,
exists: 
x:A. B[x],
subtype: S 
T,
top: Top,
pi2: snd(t),
pi1: fst(t),
nat: 
,
cand: A c B,
assert: 
b,
prop: 
,
so_lambda: 
x.t[x],
member: t T,
let: let,
and: P Q,
run-event-interval: run-event-interval(r;e1;e2),
runEvents: runEvents(r),
so_apply: x[s],
all: x:A. B[x],
uall: [x:A]. B[x],
false: False,
not: 
A,
Id: Id,
run-event-loc: run-event-loc(e),
run-event-step: run-event-step(e),
le: A B,
guard: {T},
sq_type: SQType(T),
uimplies: b supposing a,
sq_stable: SqStable(P)
Lemmas :
true_wf,
squash_wf,
member-mapfilter,
iff_functionality_wrt_iff,
equal_wf,
assert_elim,
bool_subtype_base,
bool_wf,
subtype_base_sq,
subtype_rel_self,
subtype_rel_sets,
exists_wf,
pi2_wf,
Id_wf,
pi1_wf_top,
assert_wf,
run-event-loc_wf,
is-run-event_wf,
less_than_wf,
and_wf,
from-upto_wf,
nat_wf,
run-event-step_wf,
le_wf,
mapfilter_wf,
l_member_wf,
pRunType_wf,
runEvents_wf,
atom2_subtype_base,
int_subtype_base,
product_subtype_base,
Error :pi2_wf,
set_subtype_base,
sq_stable__assert,
member-from-upto
\mforall{}[M:Type {}\mrightarrow{} Type]
\mforall{}r:pRunType(P.M[P]). \mforall{}e1,e2,e:runEvents(r).
((e \mmember{} run-event-interval(r;e1;e2))
\mLeftarrow{}{}\mRightarrow{} (run-event-loc(e) = run-event-loc(e1))
\mwedge{} (run-event-step(e1) \mleq{} run-event-step(e))
\mwedge{} (run-event-step(e) \mleq{} run-event-step(e2)))
Date html generated:
2012_01_23-PM-12_43_06
Last ObjectModification:
2011_12_14-PM-11_31_49
Home
Index