Nuprl Lemma : run-event-step_wf

[M:Type ─→ Type]. ∀[r:pRunType(P.M[P])]. ∀[e:runEvents(r)].  (run-event-step(e) ∈ ℕ)


Proof




Definitions occuring in Statement :  run-event-step: run-event-step(e) runEvents: runEvents(r) pRunType: pRunType(T.M[T]) nat: uall: [x:A]. B[x] so_apply: x[s] member: t ∈ T function: x:A ─→ B[x] universe: Type
Lemmas :  runEvents_wf pRunType_wf

Latex:
\mforall{}[M:Type  {}\mrightarrow{}  Type].  \mforall{}[r:pRunType(P.M[P])].  \mforall{}[e:runEvents(r)].    (run-event-step(e)  \mmember{}  \mBbbN{})



Date html generated: 2015_07_23-AM-11_11_07
Last ObjectModification: 2015_01_29-AM-00_06_57

Home Index