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
Lemmas :
run-event-cases,
fulpRunType-subtype,
less_than_wf,
run-event-step_wf,
nat_wf,
exists_wf,
runEvents_wf,
le_wf,
Id_wf,
run-event-loc_wf,
list_wf,
Process_wf,
run-prior-state_wf,
run-event-state_wf,
append_wf,
run-event-interval_wf,
cons_wf,
nil_wf,
length_wf,
equal_wf,
fulpRunType_wf,
System_wf,
subtype_base_sq,
atom2_subtype_base,
filter_wf5,
component_wf,
l_member_wf,
eq_id_wf,
map_wf,
unit_wf2,
union_subtype_base,
set_subtype_base,
assert_wf,
is-run-event_wf,
product_subtype_base,
int_subtype_base,
unit_subtype_base
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:
2015_07_23-AM-11_12_25
Last ObjectModification:
2015_01_29-AM-00_08_04
Home
Index