Nuprl Lemma : well-founded-run-pred

[M:Type ─→ Type]
  ∀r:pRunType(P.M[P])
    SWellFounded(x run-pred(r) y) supposing ∀e:runEvents(r). fst(fst(run-info(r;e))) < run-event-step(e)


Proof




Definitions occuring in Statement :  run-pred: run-pred(r) run-event-step: run-event-step(e) runEvents: runEvents(r) run-info: run-info(r;e) pRunType: pRunType(T.M[T]) strongwellfounded: SWellFounded(R[x; y]) less_than: a < b uimplies: supposing a uall: [x:A]. B[x] infix_ap: y so_apply: x[s] pi1: fst(t) all: x:A. B[x] function: x:A ─→ B[x] universe: Type
Lemmas :  run-pred-step-less member-less_than run-info_wf Id_wf pMsg_wf run-event-step_wf nat_wf runEvents_wf infix_ap_wf run-pred_wf all_wf less_than_wf pRunType_wf

Latex:
\mforall{}[M:Type  {}\mrightarrow{}  Type]
    \mforall{}r:pRunType(P.M[P])
        SWellFounded(x  run-pred(r)  y) 
        supposing  \mforall{}e:runEvents(r).  fst(fst(run-info(r;e)))  <  run-event-step(e)



Date html generated: 2015_07_23-AM-11_14_50
Last ObjectModification: 2015_01_29-AM-00_05_29

Home Index