Nuprl Lemma : decd-run-lt_wf
[M:Type 
Type]. [r:pRunType(P.M[P])].
decd-run-lt(r) 
e1,e2:runEvents(r). Dec(e1 run-lt(r) e2)
supposing e:runEvents(r). ((fst(fst(run-info(r;e)))) < run-event-step(e))
Proof not projected
Definitions occuring in Statement :
decd-run-lt: decd-run-lt(r),
run-lt: run-lt(r),
run-event-step: run-event-step(e),
runEvents: runEvents(r),
run-info: run-info(r;e),
pRunType: pRunType(T.M[T]),
decidable: Dec(P),
uimplies: b supposing a,
uall: [x:A]. B[x],
infix_ap: x f y,
so_apply: x[s],
pi1: fst(t),
all: x:A. B[x],
member: t T,
less_than: a < b,
function: x:A B[x],
universe: Type
Definitions :
subtype: S 
T,
top: Top,
so_lambda: 
x.t[x],
member: t T,
all: x:A. B[x],
uimplies: b supposing a,
so_apply: x[s],
uall: [x:A]. B[x],
implies: P 
Q,
prop: 
,
infix_ap: x f y,
nat_properties,
bool_cases,
rel_exp_iff,
outl: outl(x),
spreadn: spread3,
run-event-loc: run-event-loc(e),
decidable__run-pred,
eq_int: (i =
j),
pi2: snd(t),
band: p 
q,
let: let,
ifthenelse: if b then t else f fi ,
lt_int: i <z j,
decidable__cand,
decidable__l_exists_better-extract,
finite-run-pred,
iff_functionality_wrt_iff,
eq_atom: eq_atom$n(x;y),
atom2-deq: Atom2Deq,
id-deq: IdDeq,
eq_id: a = b,
decidable__assert,
all_functionality_wrt_iff,
decidable__equal_Id,
bfalse: ff,
btrue: tt,
decidable__equal_int,
decidable__equal_nat,
decidable__equal_product,
decidable__equal_set,
decidable__equal_runEvents,
decidable__rel_exp_finite,
it: 
,
decidable__ex_int_seg,
iff_preserves_decidability,
decidable_functionality,
well-founded-run-pred,
decidable__rel_plus,
decidable__run-lt,
run-event-step: run-event-step(e),
run-info: run-info(r;e),
pi1: fst(t),
nat: 
,
spreadn: spread4,
decd-run-lt: decd-run-lt(r)
Lemmas :
pRunType_wf,
nat_wf,
run-event-step_wf,
pMsg_wf,
Id_wf,
run-info_wf,
top_wf,
pi1_wf_top,
less_than_wf,
runEvents_wf,
all_wf,
equal_wf,
run-lt_wf,
decidable_wf,
isect_wf,
uall_wf
\mforall{}[M:Type {}\mrightarrow{} Type]. \mforall{}[r:pRunType(P.M[P])].
decd-run-lt(r) \mmember{} \mforall{}e1,e2:runEvents(r). Dec(e1 run-lt(r) e2)
supposing \mforall{}e:runEvents(r). ((fst(fst(run-info(r;e)))) < run-event-step(e))
Date html generated:
2012_01_23-PM-12_44_01
Last ObjectModification:
2011_12_14-PM-12_06_35
Home
Index