Nuprl Lemma : run-prior-state-property
∀[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) ∈ (Process(P.M[P]\000C) List))
∧ (∀t:{m + 1..n-}. (¬↑is-run-event(r;t;x))))
supposing 0 < n
supposing (r 0) = <inr ⋅ , S0> ∈ (ℤ × Id × Id × pMsg(P.M[P])? × System(P.M[P]))
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,
mapfilter: mapfilter(f;P;L),
list: T List,
int_seg: {i..j-},
nat: ℕ,
assert: ↑b,
less_than: a < b,
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,
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,
add: n + m,
natural_number: $n,
int: ℤ,
universe: Type,
equal: s = t ∈ T
Lemmas :
member-less_than,
fulpRunType-subtype,
less_than_wf,
all_wf,
int_seg_wf,
isect_wf,
exists_wf,
list_wf,
Process_wf,
run-prior-state_wf,
int_seg_subtype-nat,
not_wf,
assert_wf,
is-run-event_wf,
decidable__le,
false_wf,
not-le-2,
sq_stable__le,
condition-implies-le,
minus-add,
minus-one-mul,
zero-add,
add-associates,
add-swap,
add-commutes,
add_functionality_wrt_le,
add-zero,
le-add-cancel,
nat_wf,
complete_nat_ind,
equal_wf,
Id_wf,
pMsg_wf,
unit_wf2,
le_wf,
it_wf,
fulpRunType_wf,
System_wf,
decidable__equal_int,
subtype_base_sq,
int_subtype_base,
length_wf,
le-add-cancel2,
less-iff-le,
minus-zero,
lelt_wf,
component_wf,
eq_id_wf,
mapfilter_wf,
eqtt_to_assert,
bool_wf,
isl_wf,
set_wf,
subtype_rel_self,
l_member_wf,
subtype_rel_dep_function,
filter_wf5,
map_wf,
map_cons_lemma,
filter_cons_lemma,
decidable__assert,
subtract_wf,
minus-minus,
subtract-is-less,
upto_decomp1,
bnot_wf,
assert_elim,
last_singleton_append,
equal-wf-T-base,
assert-bnot,
bool_subtype_base,
bool_cases_sqequal,
eqff_to_assert,
btrue_neq_bfalse,
btrue_wf,
null_nil_lemma,
and_wf,
append_is_nil,
bfalse_wf,
null_cons_lemma,
assert_of_null,
top_wf,
subtype_rel_list,
nil_wf,
cons_wf,
subtype_rel_sets,
from-upto_wf,
append_wf,
null_wf3,
map_nil_lemma,
filter_nil_lemma,
mapfilter-append,
decidable__lt,
not-equal-2,
run-event-state_wf,
append-nil,
last_wf,
product_subtype_list,
equal-wf-base,
list-cases,
runEvents_wf,
filter_type,
assert_functionality_wrt_uiff,
not_assert_elim,
squash_wf,
true_wf,
pRunType_wf,
le-add-cancel-alt
Latex:
\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;C\000Cs))
\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:
2015_07_23-AM-11_11_58
Last ObjectModification:
2015_07_16-AM-09_38_48
Home
Index