{ 
[M:Type 
Type]
[n2m:
pMsg(P.M[P])]. [l2m:Id pMsg(P.M[P])]. [S0:System(P.M[P])].
[env:pEnvType(P.M[P])].
runEO(n2m;l2m;env;S0) 
EO+(pMsg(P.M[P]))
supposing run-initialization(pRun(S0;env;n2m;l2m);snd(S0))
supposing Continuous+(P.M[P]) }
{ Proof }
Definitions occuring in Statement :
runEO: runEO(n2m;l2m;env;S),
run-initialization: run-initialization(r;G),
pRun: pRun(S0;env;nat2msg;loc2msg),
pEnvType: pEnvType(T.M[T]),
System: System(P.M[P]),
pMsg: pMsg(P.M[P]),
event-ordering+: EO+(Info),
Id: Id,
strong-type-continuous: Continuous+(T.F[T]),
nat: ,
uimplies: b supposing a,
uall: [x:A]. B[x],
so_apply: x[s],
pi2: snd(t),
member: t T,
function: x:A B[x],
universe: Type
Definitions :
component: component(P.M[P]),
spread: spread def,
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],
natural_number: $n,
run-event-step: run-event-step(e),
run-info: run-info(r;e),
pi1: fst(t),
runEvents: runEvents(r),
run-eo: EO(r),
axiom: Ax,
runEO: runEO(n2m;l2m;env;S),
event-ordering+: EO+(Info),
void: Void,
nat_plus: 
,
fpf-dom: x dom(f),
false: False,
guard: {T},
pair: <a, b>,
pInTransit: pInTransit(P.M[P]),
unit: Unit,
int: 
,
subtype: S 
T,
tag-by: z
T,
rev_implies: P 
Q,
or: P 
Q,
implies: P 
Q,
iff: P Q,
labeled-graph: LabeledGraph(T),
record+: record+,
record: record(x.T[x]),
fset: FSet{T},
isect2: T1 
T2,
b-union: A 
B,
union: left + right,
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,
eclass: EClass(A[eo; e]),
fpf: a:A fp-> B[a],
strong-subtype: strong-subtype(A;B),
ext-eq: A 
B,
set: {x:A| B[x]} ,
ldag: LabeledDAG(T),
list: type List,
le: A 
B,
ge: i 
j ,
not: 
A,
less_than: a < b,
and: P 
Q,
uiff: uiff(P;Q),
subtype_rel: A r B,
fulpRunType: fulpRunType(T.M[T]),
product: x:A B[x],
pi2: snd(t),
run-initialization: run-initialization(r;G),
pEnvType: pEnvType(T.M[T]),
System: System(P.M[P]),
Id: Id,
nat: ,
uimplies: b supposing a,
prop: 
,
strong-type-continuous: Continuous+(T.F[T]),
all: x:A. B[x],
isect: x:A. B[x],
so_lambda: 
x.t[x],
equal: s = t,
lambda: x.A[x],
apply: f a,
universe: Type,
uall: [x:A]. B[x],
function: x:A B[x],
pMsg: pMsg(P.M[P]),
Auto: Error :Auto,
CollapseTHEN: Error :CollapseTHEN,
MaAuto: Error :MaAuto,
pRun: pRun(S0;env;nat2msg;loc2msg),
so_apply: x[s],
pRunType: pRunType(T.M[T]),
member: t T,
AssertBY: Error :AssertBY,
tactic: Error :tactic
Lemmas :
pRunType_wf,
subtype_rel_wf,
fulpRunType_wf,
member_wf,
pRun_wf,
pEnvType_wf,
System_wf,
pMsg_wf,
Id_wf,
nat_wf,
strong-type-continuous_wf,
pInTransit_wf,
ldag_wf,
top_wf,
unit_wf,
subtype_rel_function,
subtype_rel_self,
subtype_rel_simple_product,
run-initialization_wf,
labeled-graph_wf,
run-eo_wf,
runEvents_wf,
component_wf,
run-initialization-property
\mforall{}[M:Type {}\mrightarrow{} Type]
\mforall{}[n2m:\mBbbN{} {}\mrightarrow{} pMsg(P.M[P])]. \mforall{}[l2m:Id {}\mrightarrow{} pMsg(P.M[P])]. \mforall{}[S0:System(P.M[P])].
\mforall{}[env:pEnvType(P.M[P])].
runEO(n2m;l2m;env;S0) \mmember{} EO+(pMsg(P.M[P]))
supposing run-initialization(pRun(S0;env;n2m;l2m);snd(S0))
supposing Continuous+(P.M[P])
Date html generated:
2011_08_17-PM-03_40_49
Last ObjectModification:
2011_06_18-AM-11_22_18
Home
Index