Nuprl Lemma : run-event-interval-cases
∀[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) ∈ (Process(P.M[P]) List))
∧ (run-event-interval(r;e1;e2) = [e2] ∈ (runEvents(r) List)))
∨ (∃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) ∈ Id)
∧ (run-prior-state(S0;r;e2) = run-event-state(r;e) ∈ (Process(P.M[P]) List)))
∧ (run-event-interval(r;e1;e2) = (run-event-interval(r;e1;e) @ [e2]) ∈ (runEvents(r) List))))) supposing
((run-event-step(e1) ≤ run-event-step(e2)) and
(run-event-loc(e1) = run-event-loc(e2) ∈ Id))
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,
cons: [a / b],
nil: [],
list: T List,
less_than: a < b,
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,
function: x:A ⟶ B[x],
universe: Type,
equal: s = t ∈ T
Definitions unfolded in proof :
uall: ∀[x:A]. B[x],
member: t ∈ T,
all: ∀x:A. B[x],
subtype_rel: A ⊆r B,
so_lambda: λ2x.t[x],
so_apply: x[s],
uimplies: b supposing a,
le: A ≤ B,
and: P ∧ Q,
not: ¬A,
implies: P ⇒ Q,
false: False,
nat: ℕ,
prop: ℙ,
or: P ∨ Q,
runEvents: runEvents(r),
guard: {T},
exists: ∃x:A. B[x],
cand: A c∧ B,
run-prior-state: run-prior-state(S0;r;e),
Id: Id,
sq_type: SQType(T),
System: System(P.M[P]),
mapfilter: mapfilter(f;P;L),
pi1: fst(t),
component: component(P.M[P]),
pi2: snd(t),
top: Top
Latex:
\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:
2016_05_17-AM-10_45_30
Last ObjectModification:
2015_12_29-PM-05_22_41
Theory : process-model
Home
Index