{ 
[M:Type 
Type]. [r:pRunType(P.M[P])].
[x,y:runEvents(r)].
run-event-step(x) < run-event-step(y) supposing x run-lt(r) y
supposing e:runEvents(r). ((fst(fst(run-info(r;e)))) < run-event-step(e)) }
{ Proof }
Definitions occuring in Statement :
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]),
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],
less_than: a < b,
function: x:A B[x],
universe: Type
Definitions :
uall: [x:A]. B[x],
so_apply: x[s],
uimplies: b supposing a,
all: x:A. B[x],
infix_ap: x f y,
member: t 
T,
implies: P 
Q,
nat: 
,
so_lambda: 
x.t[x],
le: A 
B,
prop: 
,
not: 
A,
false: False,
and: P 
Q,
top: Top,
subtype: S 
T,
run-lt: run-lt(r),
rel_plus: R
,
exists: 
x:A. B[x],
nat_plus: ,
decidable: Dec(P),
or: P 
Q,
sq_type: SQType(T),
guard: {T},
iff: P 
Q,
cand: A c B
Lemmas :
run-pred-step-less,
nat_plus_properties,
run-event-step_wf,
nat_wf,
rel_exp_wf,
le_wf,
run-pred_wf,
decidable__equal_int,
subtype_base_sq,
int_subtype_base,
rel_exp_one,
rel_exp_iff,
run-lt_wf,
runEvents_wf,
pi1_wf_top,
top_wf,
run-info_wf,
Id_wf,
pMsg_wf,
pRunType_wf
\mforall{}[M:Type {}\mrightarrow{} Type]. \mforall{}[r:pRunType(P.M[P])].
\mforall{}[x,y:runEvents(r)]. run-event-step(x) < run-event-step(y) supposing x run-lt(r) y
supposing \mforall{}e:runEvents(r). ((fst(fst(run-info(r;e)))) < run-event-step(e))
Date html generated:
2011_08_16-PM-07_05_08
Last ObjectModification:
2011_06_18-AM-11_18_18
Home
Index