### Nuprl Lemma : total-run-lt

`∀[M:Type ─→ Type]`
`  ∀r:pRunType(P.M[P]). ∀e1,e2:runEvents(r).`
`    (e1 = e2 ∈ runEvents(r)) ∨ (e1 run-lt(r) e2) ∨ (e2 run-lt(r) e1) `
`    supposing run-event-loc(e1) = run-event-loc(e2) ∈ Id`

Proof

Definitions occuring in Statement :  run-lt: `run-lt(r)` run-event-loc: `run-event-loc(e)` runEvents: `runEvents(r)` pRunType: `pRunType(T.M[T])` Id: `Id` uimplies: `b supposing a` uall: `∀[x:A]. B[x]` infix_ap: `x f y` so_apply: `x[s]` all: `∀x:A. B[x]` or: `P ∨ Q` function: `x:A ─→ B[x]` universe: `Type` equal: `s = t ∈ T`
Lemmas :  run-pred_wf rel_plus_wf runEvents_wf infix_ap_wf or_wf assert_wf bool_subtype_base bool_wf subtype_base_sq is-run-event_wf assert_elim le_wf le_antisymmetry nat_plus_subtype_nat rel_exp_wf pMsg_wf run-info_wf subtype_rel_self subtype_rel_product Id_wf equal_wf le-add-cancel add_functionality_wrt_le add-commutes add-swap minus-one-mul minus-add condition-implies-le not-le-2 false_wf nat_wf run-event-step_wf decidable__lt rel_exp_one less_than_wf

Latex:
\mforall{}[M:Type  {}\mrightarrow{}  Type]
\mforall{}r:pRunType(P.M[P]).  \mforall{}e1,e2:runEvents(r).
(e1  =  e2)  \mvee{}  (e1  run-lt(r)  e2)  \mvee{}  (e2  run-lt(r)  e1)
supposing  run-event-loc(e1)  =  run-event-loc(e2)

Date html generated: 2015_07_23-AM-11_15_34
Last ObjectModification: 2015_07_16-AM-09_38_36

Home Index