{ 
[M:Type 
Type]
S0:System(P.M[P]). r:fulpRunType(P.M[P]). e1,e2:runEvents(r).
(((run-prior-state(S0;r;e2) = run-prior-state(S0;r;e1))
(run-event-interval(r;e1;e2) = [e2]))
(
e:runEvents(r)
((run-event-step(e) < run-event-step(e2))
(run-event-step(e1) 
run-event-step(e))
((run-event-loc(e1) = run-event-loc(e))
(run-prior-state(S0;r;e2) = run-event-state(r;e)))
(run-event-interval(r;e1;e2)
= (run-event-interval(r;e1;e) @ [e2]))))) supposing
((run-event-step(e1) run-event-step(e2)) and
(run-event-loc(e1) = run-event-loc(e2))) }
{ Proof }
Definitions occuring in Statement :
run-prior-state: run-prior-state(S0;r;e),
run-event-interval: run-event-interval(r;e1;e2),
run-event-step: run-event-step(e),
run-event-loc: run-event-loc(e),
run-event-state: run-event-state(r;e),
runEvents: runEvents(r),
fulpRunType: fulpRunType(T.M[T]),
System: System(P.M[P]),
Process: Process(P.M[P]),
Id: Id,
append: as @ bs,
uimplies: b supposing a,
uall: [x:A]. B[x],
so_apply: x[s],
le: A B,
all: x:A. B[x],
exists: x:A. B[x],
or: P Q,
and: P Q,
less_than: a < b,
function: x:A B[x],
cons: [car / cdr],
nil: [],
list: type List,
universe: Type,
equal: s = t
Definitions :
uall: [x:A]. B[x],
all: x:A. B[x],
so_apply: x[s],
fulpRunType: fulpRunType(T.M[T]),
runEvents: runEvents(r),
uimplies: b supposing a,
Id: Id,
le: A B,
or: P Q,
and: P Q,
run-prior-state: run-prior-state(S0;r;e),
exists: x:A. B[x],
pRunType: pRunType(T.M[T]),
member: t 
T,
nat: 
,
top: Top,
so_lambda: 
x.t[x],
not: 
A,
implies: P 
Q,
false: False,
prop: 
,
guard: {T},
subtype: S 
T,
cand: A c B,
pi2: snd(t),
pi1: fst(t),
System: System(P.M[P]),
sq_type: SQType(T),
component: component(P.M[P])
Lemmas :
run-event-cases,
subtype_rel_function,
nat_wf,
Id_wf,
pMsg_wf,
unit_wf,
System_wf,
top_wf,
ldag_wf,
pInTransit_wf,
subtype_rel_self,
subtype_rel_simple_product,
fulpRunType_wf,
pRunType_wf,
run-event-step_wf,
le_wf,
run-event-loc_wf,
Process_wf,
run-prior-state_wf,
run-event-state_wf,
append_wf,
run-event-interval_wf,
subtype_base_sq,
union_subtype_base,
set_subtype_base,
assert_wf,
is-run-event_wf,
pi1_wf_top,
pi2_wf,
product_subtype_base,
int_subtype_base,
atom2_subtype_base,
unit_subtype_base,
runEvents_wf,
mapfilter_wf,
component_wf,
eq_id_wf
\mforall{}[M:Type {}\mrightarrow{} Type]
\mforall{}S0:System(P.M[P]). \mforall{}r:fulpRunType(P.M[P]). \mforall{}e1,e2:runEvents(r).
(((run-prior-state(S0;r;e2) = run-prior-state(S0;r;e1)) \mwedge{} (run-event-interval(r;e1;e2) = [e2]))
\mvee{} (\mexists{}e:runEvents(r)
((run-event-step(e) < run-event-step(e2))
\mwedge{} (run-event-step(e1) \mleq{} run-event-step(e))
\mwedge{} ((run-event-loc(e1) = run-event-loc(e))
\mwedge{} (run-prior-state(S0;r;e2) = run-event-state(r;e)))
\mwedge{} (run-event-interval(r;e1;e2) = (run-event-interval(r;e1;e) @ [e2]))))) supposing
((run-event-step(e1) \mleq{} run-event-step(e2)) and
(run-event-loc(e1) = run-event-loc(e2)))
Date html generated:
2011_08_16-PM-07_01_08
Last ObjectModification:
2011_06_18-AM-11_15_24
Home
Index