{ 
[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.
((e1 <loc e2) 
(e1 
run-event-history(pRun(S0;env;n2m;l2m);e2)))
supposing Continuous+(P.M[P]) }
{ Proof }
Definitions occuring in Statement :
stdEO: stdEO(n2m;l2m;env;S),
InitialSystem: InitialSystem(P.M[P]),
run-event-history: run-event-history(r;e),
runEvents: runEvents(r),
pRun: pRun(S0;env;nat2msg;loc2msg),
pEnvType: pEnvType(T.M[T]),
pMsg: pMsg(P.M[P]),
es-locl: (e <loc 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],
all: x:A. B[x],
iff: P Q,
function: x:A B[x],
universe: Type,
l_member: (x l)
Definitions :
real: 
,
grp_car: |g|,
run-lt: run-lt(r),
mk-eo: mk-eo(E;dom;l;R;a;b;c;d;e;f),
eq_atom: x =a y,
eq_atom: eq_atom$n(x;y),
rec_select_update: rec_select_update{rec_select_update_compseq_tag_def:o}(y; v; x; r),
run-eo: EO(r),
runEO: runEO(n2m;l2m;env;S),
void: Void,
nat_plus: 
,
fpf-dom: x dom(f),
false: False,
guard: {T},
es-loc: loc(e),
pInTransit: pInTransit(P.M[P]),
unit: Unit,
tag-by: z
T,
or: P 
Q,
ldag: LabeledDAG(T),
labeled-graph: LabeledGraph(T),
record+: record+,
record: record(x.T[x]),
fset: FSet{T},
isect2: T1 
T2,
b-union: A 
B,
union: left + right,
bag: bag(T),
list: type List,
top: Top,
true: True,
fpf-sub: f 
g,
deq: EqDecider(T),
ma-state: State(ds),
class-program: ClassProgram(T),
es-E-interface: E(X),
fpf-cap: f(x)?z,
System: System(P.M[P]),
bool: 
,
eclass: EClass(A[eo; e]),
fpf: a:A fp-> B[a],
strong-subtype: strong-subtype(A;B),
infix_ap: x f y,
es-causl: (e < e'),
record-select: r.x,
decide: case b of inl(x) => s[x] | inr(y) => t[y],
ifthenelse: if b then t else f fi ,
assert: 
b,
lg-all: xG.P[x],
std-initial: std-initial(S),
le: A 
B,
ge: i 
j ,
not: 
A,
uiff: uiff(P;Q),
int: 
,
limited-type: LimitedType,
subtype: S T,
lambda: 
x.A[x],
pair: <a, b>,
subtype_rel: A r B,
ext-eq: A 
B,
prop: 
,
run-event-step: run-event-step(e),
less_than: a < b,
run-event-loc: run-event-loc(e),
rev_implies: P Q,
run-event-history: run-event-history(r;e),
apply: f a,
equal: s = t,
set: {x:A| B[x]} ,
exists: 
x:A. B[x],
implies: P Q,
product: x:A B[x],
and: P 
Q,
universe: Type,
strong-type-continuous: Continuous+(T.F[T]),
InitialSystem: InitialSystem(P.M[P]),
nat: ,
Id: Id,
pMsg: pMsg(P.M[P]),
pEnvType: pEnvType(T.M[T]),
uall: [x:A]. B[x],
uimplies: b supposing a,
isect: x:A. B[x],
all: x:A. B[x],
function: x:A B[x],
iff: P Q,
l_member: (x l),
fulpRunType: fulpRunType(T.M[T]),
runEvents: runEvents(r),
es-locl: (e <loc e'),
es-E: E,
stdEO: stdEO(n2m;l2m;env;S),
so_lambda: 
x.t[x],
event-ordering+: EO+(Info),
event_ordering: EO,
Auto: Error :Auto,
Complete: Error :Complete,
RepUR: Error :RepUR,
CollapseTHEN: Error :CollapseTHEN,
it: 
,
MaAuto: Error :MaAuto,
pRun: pRun(S0;env;nat2msg;loc2msg),
so_apply: x[s],
pRunType: pRunType(T.M[T]),
member: t T,
AssertBY: Error :AssertBY,
Try: Error :Try,
CollapseTHENA: Error :CollapseTHENA,
RepeatFor: Error :RepeatFor,
tactic: Error :tactic,
AllHyps: Error :AllHyps,
spread: spread def,
atom: Atom$n,
squash: 
T,
btrue: tt,
pi2: snd(t),
pi1: fst(t),
sq_type: SQType(T),
is-run-event: is-run-event(r;t;x),
from-upto: [n, m),
let: let,
natural_number: $n,
cand: A c B,
atom: Atom,
sqequal: s ~ t,
D: Error :D,
ExRepD: Error :ExRepD,
is_list_splitting: is_list_splitting(T;L;LL;L2;f),
is_accum_splitting: is_accum_splitting(T;A;L;LL;L2;f;g;x),
req: x = y,
rnonneg: rnonneg(r),
rleq: x y,
i-member: r I,
partitions: partitions(I;p),
modulus-of-ccontinuity: modulus-of-ccontinuity(omega;I;f),
sq_stable: SqStable(P)
Lemmas :
sq_stable__assert,
member-from-upto,
not_wf,
assert_witness,
atom2_subtype_base,
int_subtype_base,
set_subtype_base,
product_subtype_base,
pi1_wf,
squash_wf,
assert_wf,
le_wf,
is-run-event_wf,
from-upto_wf,
member-mapfilter,
true_wf,
false_wf,
ifthenelse_wf,
bool_wf,
subtype_base_sq,
bool_subtype_base,
assert_elim,
pi1_wf_top,
pi2_wf,
pRun_wf2,
es-E_wf,
stdEO_wf,
iff_wf,
es-locl_wf,
l_member_wf,
pRun_wf,
InitialSystem_wf,
nat_wf,
pMsg_wf,
Id_wf,
pEnvType_wf,
strong-type-continuous_wf,
uall_wf,
stdEO-locl,
event-ordering+_wf,
event-ordering+_inc,
iff_functionality_wrt_iff,
rev_implies_wf,
member_wf,
run-event-loc_wf,
run-event-step_wf,
subtype_rel_wf,
pRunType_wf,
fulpRunType_wf,
pInTransit_wf,
ldag_wf,
top_wf,
unit_wf,
System_wf,
subtype_rel_function,
subtype_rel_self,
subtype_rel_simple_product,
runEvents_wf,
run-event-history_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.
((e1 <loc e2) \mLeftarrow{}{}\mRightarrow{} (e1 \mmember{} run-event-history(pRun(S0;env;n2m;l2m);e2)))
supposing Continuous+(P.M[P])
Date html generated:
2011_08_17-PM-03_42_09
Last ObjectModification:
2011_06_18-AM-11_23_25
Home
Index