Nuprl - mb_event_system_2 LEMMAs for decidable__es_DASH

IF YOU CAN SEE THIS go to /sfa/Nuprl/Shared/Xindentation_hack_doc.html

Rank	Theorem	Name
2	Thm* the_es:ES, e',e:E. Dec((e <loc e'))	[decidable__es-locl]
cites the following:
0	Thm* the_es:ES, j,e:E. first(j) (e <loc j)	[es-first-implies]
0	Thm* Dec(P) Dec(Q) Dec(P Q)	[decidable__or]
0	Thm* Dec(P) Dec(Q) Dec(P & Q)	[decidable__and]
1	Thm* the_es:ES, e,e':E. Thm* (e <loc e') first(e') & e = pred(e') E (e <loc pred(e'))	[es-locl-iff]
0	Thm* the_es:ES, j:E. first(j) (pred(j) <loc j)	[es-pred-locl]

IF YOU CAN SEE THIS go to /sfa/Nuprl/Shared/Xindentation_hack_doc.html