Nuprl Lemma : es-r-immediate-pred

{

[es:EO].

[R:E

E

].

[e,e':E]. (es-r-immediate-pred(es;R;e';e)

) }

{ Proof }

Definitions occuring in Statement : es-r-immediate-pred: es-r-immediate-pred(es;R;e';e), es-E: E, event_ordering: EO, uall:

[x:A]. B[x], prop:

, member: t

T, function: x:A

B[x]
Definitions : uall:

[x:A]. B[x], prop:

, member: t

T, es-r-immediate-pred: es-r-immediate-pred(es;R;e';e)
Lemmas : rel-immediate_wf, es-E_wf, event_ordering_wf

\mforall{}[es:EO]. \mforall{}[R:E {}\mrightarrow{} E {}\mrightarrow{} \mBbbP{}]. \mforall{}[e,e':E]. (es-r-immediate-pred(es;R;e';e) \mmember{} \mBbbP{}) Date html generated: 2011_08_16-AM-11_14_14 Last ObjectModification: 2011_06_20-AM-00_21_25 Home Index