{ 
[M:Type 
Type]
[S0:InitialSystem(P.M[P])]. [n2m:
pMsg(P.M[P])].
[l2m:Id pMsg(P.M[P])]. [env:pEnvType(P.M[P])]. [e1,e2:E].
run-event-step(e1) < run-event-step(e2) supposing (e1 < e2)
supposing Continuous+(P.M[P]) }
{ Proof }
Definitions occuring in Statement :
stdEO: stdEO(n2m;l2m;env;S),
InitialSystem: InitialSystem(P.M[P]),
run-event-step: run-event-step(e),
pEnvType: pEnvType(T.M[T]),
pMsg: pMsg(P.M[P]),
es-causl: (e < e'),
es-E: E,
Id: Id,
strong-type-continuous: Continuous+(T.F[T]),
nat: ,
uimplies: b supposing a,
uall: [x:A]. B[x],
so_apply: x[s],
less_than: a < b,
function: x:A B[x],
universe: Type
Definitions :
implies: P 
Q,
proper-iseg: L1 < L2,
iseg: l1 
l2,
gt: i > j,
union: left + right,
or: P 
Q,
length: ||as||,
strong-subtype: strong-subtype(A;B),
infix_ap: x f y,
lg-all: x
G.P[x],
std-initial: std-initial(S),
le: A B,
ge: i 
j ,
natural_number: $n,
not: 
A,
uiff: uiff(P;Q),
run-event-step: run-event-step(e),
axiom: Ax,
less_than: a < b,
es-causl: (e < e'),
record-select: r.x,
subtype: S 
T,
event-ordering+: EO+(Info),
event_ordering: EO,
stdEO: stdEO(n2m;l2m;env;S),
es-E: E,
pEnvType: pEnvType(T.M[T]),
Id: Id,
set: {x:A| B[x]} ,
nat: ,
pMsg: pMsg(P.M[P]),
subtype_rel: A r B,
product: x:A 
B[x],
and: P 
Q,
ext-eq: A 
B,
InitialSystem: InitialSystem(P.M[P]),
apply: f a,
so_apply: x[s],
lambda: 
x.A[x],
isect: 
x:A. B[x],
all: x:A. B[x],
uall: [x:A]. B[x],
uimplies: b supposing a,
prop: 
,
universe: Type,
equal: s = t,
function: x:A B[x],
member: t T,
strong-type-continuous: Continuous+(T.F[T]),
so_lambda: 
x.t[x],
tactic: Error :tactic,
exists: 
x:A. B[x],
sq_type: SQType(T),
sqequal: s ~ t,
so_lambda: x y.t[x; y],
RepUR: Error :RepUR,
CollapseTHEN: Error :CollapseTHEN,
Auto: Error :Auto,
es-causl-swellfnd,
strongwellfounded: SWellFounded(R[x; y]),
spread: spread def,
Subst': Error :Subst',
pi1: fst(t),
void: Void,
top: Top,
real: 
,
grp_car: |g|,
int: 
,
it: 
,
pair: <a, b>,
pi2: snd(t)
Lemmas :
pi2_wf,
pi1_wf_top,
top_wf,
member_wf,
subtype_base_sq,
strongwellfounded_wf,
event_ordering_wf,
es-causl-swellfnd,
product_subtype_base,
strong-type-continuous_wf,
InitialSystem_wf,
nat_wf,
Id_wf,
pEnvType_wf,
es-E_wf,
es-causl_wf,
stdEO_wf,
event-ordering+_inc,
event-ordering+_wf,
pMsg_wf,
run-event-step_wf
\mforall{}[M:Type {}\mrightarrow{} Type]
\mforall{}[S0:InitialSystem(P.M[P])]. \mforall{}[n2m:\mBbbN{} {}\mrightarrow{} pMsg(P.M[P])]. \mforall{}[l2m:Id {}\mrightarrow{} pMsg(P.M[P])].
\mforall{}[env:pEnvType(P.M[P])]. \mforall{}[e1,e2:E].
run-event-step(e1) < run-event-step(e2) supposing (e1 < e2)
supposing Continuous+(P.M[P])
Date html generated:
2011_08_17-PM-03_41_23
Last ObjectModification:
2011_06_18-AM-11_22_51
Home
Index