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
Definitions unfolded in proof :
uall: ∀[x:A]. B[x],
all: ∀x:A. B[x],
uimplies: b supposing a,
member: t ∈ T,
implies: P ⇒ Q,
nat: ℕ,
subtype_rel: A ⊆r B,
so_lambda: λ2x.t[x],
so_apply: x[s],
prop: ℙ,
int_seg: {i..j-},
and: P ∧ Q,
guard: {T},
lelt: i ≤ j < k,
ge: i ≥ j ,
decidable: Dec(P),
or: P ∨ Q,
satisfiable_int_formula: satisfiable_int_formula(fmla),
exists: ∃x:A. B[x],
false: False,
not: ¬A,
top: Top,
fulpRunType: fulpRunType(T.M[T]),
le: A ≤ B,
less_than': less_than'(a;b),
sq_type: SQType(T),
less_than: a < b,
squash: ↓T,
true: True,
cand: A c∧ B,
component: component(P.M[P]),
pi1: fst(t),
spreadn: spread3,
System: System(P.M[P]),
pi2: snd(t),
is-run-event: is-run-event(r;t;x),
isl: isl(x),
outl: outl(x),
bfalse: ff,
band: p ∧b q,
ifthenelse: if b then t else f fi ,
assert: ↑b,
run-prior-state: run-prior-state(S0;r;e),
bool: 𝔹,
unit: Unit,
it: ⋅,
btrue: tt,
uiff: uiff(P;Q),
run-event-loc: run-event-loc(e),
run-event-local-pred: run-event-local-pred(r;e),
run-event-history: run-event-history(r;e),
run-event-step: run-event-step(e),
let: let,
from-upto: [n, m),
mapfilter: mapfilter(f;P;L),
lt_int: i <z j,
exposed-bfalse: exposed-bfalse,
null: null(as),
map: map(f;as),
list_ind: list_ind,
cons: [a / b],
filter: filter(P;l),
reduce: reduce(f;k;as),
nil: [],
upto: upto(n),
nat_plus: ℕ+,
bnot: ¬bb,
run-event-state: run-event-state(r;e),
runEvents: runEvents(r),
label: ...$L... t
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:
2016_05_17-AM-10_44_44
Last ObjectModification:
2016_01_18-AM-00_23_53
Theory : process-model
Home
Index