{ 
[M:Type 
Type]
S0:System(P.M[P]). r:fulpRunType(P.M[P]).
n:
. x:Id.
m:n
((run-prior-state(S0;r;<n, x>)
= let info,Cs,G = r m in
mapfilter(
c.(snd(c));c.fst(c) = x;Cs))
(t:{m + 1..n
}. (
is-run-event(r;t;x))))
supposing 0 < n
supposing (r 0) = <inr 
, S0> }
{ Proof }
Definitions occuring in Statement :
run-prior-state: run-prior-state(S0;r;e),
is-run-event: is-run-event(r;t;x),
fulpRunType: fulpRunType(T.M[T]),
System: System(P.M[P]),
pMsg: pMsg(P.M[P]),
Process: Process(P.M[P]),
eq_id: a = b,
Id: Id,
assert: b,
int_seg: {i..j},
nat: ,
it: ,
spreadn: spread3,
uimplies: b supposing a,
uall: [x:A]. B[x],
so_apply: x[s],
pi1: fst(t),
pi2: snd(t),
all: x:A. B[x],
exists: x:A. B[x],
not: A,
and: P Q,
unit: Unit,
less_than: a < b,
apply: f a,
lambda: x.A[x],
function: x:A B[x],
pair: <a, b>,
product: x:A 
B[x],
inr: inr x ,
union: left + right,
list: type List,
add: n + m,
natural_number: $n,
int: 
,
universe: Type,
equal: s = t,
mapfilter: mapfilter(f;P;L)
Definitions :
uall: [x:A]. B[x],
all: x:A. B[x],
so_apply: x[s],
fulpRunType: fulpRunType(T.M[T]),
uimplies: b supposing a,
nat: ,
not: A,
member: t 
T,
implies: P 
Q,
ge: i 
j ,
le: A 
B,
false: False,
prop: 
,
pRunType: pRunType(T.M[T]),
top: Top,
so_lambda: 
x.t[x],
exists: x:A. B[x],
int_seg: {i..j},
and: P Q,
lelt: i j < k,
spreadn: spread3,
pi2: snd(t),
assert: b,
is-run-event: is-run-event(r;t;x),
band: p 
q,
isl: isl(x),
btrue: tt,
bfalse: ff,
ifthenelse: if b then t else f fi ,
run-prior-state: run-prior-state(S0;r;e),
mapfilter: mapfilter(f;P;L),
pi1: fst(t),
run-event-local-pred: run-event-local-pred(r;e),
run-event-loc: run-event-loc(e),
null: null(as),
run-event-history: run-event-history(r;e),
let: let,
from-upto: [n, m),
run-event-step: run-event-step(e),
ycomb: Y,
lt_int: i <z j,
map: map(f;as),
filter: filter(P;l),
reduce: reduce(f;k;as),
nat_plus: 
,
last: last(L),
select: l[i],
length: ||as||,
le_int: i z j,
bnot: b,
run-event-state: run-event-state(r;e),
cand: A c B,
runEvents: runEvents(r),
subtype: S 
T,
true: True,
System: System(P.M[P]),
decidable: Dec(P),
or: P 
Q,
sq_type: SQType(T),
guard: {T},
component: component(P.M[P]),
unit: Unit,
bool: 
,
iff: P 
Q,
it: ,
upto: upto(n)
Lemmas :
nat_properties,
ge_wf,
nat_wf,
subtype_rel_function,
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,
le_wf,
it_wf,
decidable__equal_int,
subtype_base_sq,
int_subtype_base,
assert_wf,
is-run-event_wf,
int_seg_wf,
Process_wf,
run-prior-state_wf,
not_wf,
mapfilter_wf,
component_wf,
eq_id_wf,
pi1_wf_top,
false_wf,
isl_wf,
bool_wf,
iff_weakening_uiff,
eqtt_to_assert,
outl_wf,
uiff_transitivity,
bnot_wf,
eqff_to_assert,
assert_of_bnot,
bfalse_wf,
map_wf,
filter_wf,
int_seg_properties,
decidable__assert,
upto_decomp1,
from-upto_wf,
l_member_wf,
mapfilter-append,
null_append,
last_append,
null_wf3,
run-event-state_wf,
append-nil,
runEvents_wf,
filter_wf3,
bool_subtype_base,
pi2_wf,
assert_elim,
last_wf
\mforall{}[M:Type {}\mrightarrow{} Type]
\mforall{}S0:System(P.M[P]). \mforall{}r:fulpRunType(P.M[P]).
\mforall{}n:\mBbbN{}. \mforall{}x:Id.
\mexists{}m:\mBbbN{}n
((run-prior-state(S0;r;<n, x>)
= let info,Cs,G = r m in
mapfilter(\mlambda{}c.(snd(c));\mlambda{}c.fst(c) = x;Cs))
\mwedge{} (\mforall{}t:\{m + 1..n\msupminus{}\}. (\mneg{}\muparrow{}is-run-event(r;t;x))))
supposing 0 < n
supposing (r 0) = <inr \mcdot{} , S0>
Date html generated:
2011_08_16-PM-07_00_23
Last ObjectModification:
2011_06_18-AM-11_15_02
Home
Index