Nuprl Lemma : not-r-immediate-pred
es:EO
[R:E 
E 
]
((e,e':E. Dec(R e' e))
R => 
x,y.(x < y)
(e,e':E. ((e' R e) 
c:E. ((e' R c) 
(c R e)) supposing 
es-r-immediate-pred(es;R;e';e))))
Proof not projected
Definitions occuring in Statement :
es-r-immediate-pred: es-r-immediate-pred(es;R;e';e),
es-causl: (e < e'),
es-E: E,
event_ordering: EO,
decidable: Dec(P),
uimplies: b supposing a,
uall: [x:A]. B[x],
prop: ,
infix_ap: x f y,
all: x:A. B[x],
exists: x:A. B[x],
not: A,
implies: P Q,
and: P Q,
apply: f a,
lambda: x.A[x],
function: x:A B[x],
rel_implies: R1 => R2
Definitions :
rel-immediate: R!,
cand: A c B,
so_lambda: 
x.t[x],
false: False,
member: t 
T,
and: P Q,
exists: x:A. B[x],
es-r-immediate-pred: es-r-immediate-pred(es;R;e';e),
not: A,
uimplies: b supposing a,
infix_ap: x f y,
implies: P Q,
prop: ,
uall: [x:A]. B[x],
all: x:A. B[x],
or: P 
Q,
decidable: Dec(P),
so_apply: x[s],
rel_implies: R1 => R2
Lemmas :
decidable__cand,
decidable__existse-causl,
and_wf,
event_ordering_wf,
decidable_wf,
all_wf,
es-causl_wf,
rel_implies_wf,
es-E_wf,
not_wf,
es-r-immediate-pred_wf
\mforall{}es:EO
\mforall{}[R:E {}\mrightarrow{} E {}\mrightarrow{} \mBbbP{}]
((\mforall{}e,e':E. Dec(R e' e))
{}\mRightarrow{} R => \mlambda{}x,y.(x < y)
{}\mRightarrow{} (\mforall{}e,e':E.
((e' R e) {}\mRightarrow{} \mexists{}c:E. ((e' R c) \mwedge{} (c R e)) supposing \mneg{}es-r-immediate-pred(es;R;e';e))))
Date html generated:
2012_01_23-PM-12_14_55
Last ObjectModification:
2011_12_13-PM-12_45_27
Home
Index