Nuprl Lemma : eo-forward-pred?
[Info:Type]. [eo:EO+(Info)]. [e:E].
e1:E. (es-pred?(eo.e;e1) = if es-eq(eo) e1 e then inr 
else es-pred?(eo;e1) fi )
Proof not projected
Definitions occuring in Statement :
eo-forward: eo.e,
event-ordering+: EO+(Info),
es-pred?: es-pred?(es;e),
es-eq: es-eq(es),
es-E: E,
ifthenelse: if b then t else f fi ,
it: ,
uall: [x:A]. B[x],
all: x:A. B[x],
unit: Unit,
apply: f a,
inr: inr x ,
union: left + right,
universe: Type,
equal: s = t
Definitions :
so_lambda: 
x.t[x],
prop: 
,
top: Top,
implies: P 
Q,
uimplies: b supposing a,
all: x:A. B[x],
member: t 
T,
guard: {T},
not: 
A,
or: P 
Q,
bfalse: ff,
btrue: tt,
exposed-bfalse: exposed-bfalse,
ifthenelse: if b then t else f fi ,
true: True,
squash: 
T,
and: P 
Q,
label: ...$L... t,
es-le: e 
loc e' ,
so_apply: x[s],
uall: [x:A]. B[x],
false: False,
decidable: Dec(P),
cand: A c B,
uiff: uiff(P;Q),
bool: 
,
unit: Unit,
es-locl: (e <loc e'),
subtype: S 
T,
it:
Lemmas :
eo-forward-less,
eo-forward-loc,
event-ordering+_wf,
event-ordering+_inc,
eo-forward_wf,
es-E_wf,
not_wf,
or_wf,
isect_wf,
all_wf,
es-causl_wf,
es-loc_wf,
Id_wf,
equal_wf,
and_wf,
unit_wf2,
es-pred?_wf,
es-pred?_property,
eo-forward-E-subtype,
es-le_wf,
decidable__es-le,
eo-forward-E-member,
not_functionality_wrt_uiff,
assert_of_bnot,
eqff_to_assert,
bnot_wf,
es-eq_wf,
assert-deq,
eqtt_to_assert,
assert_wf,
uiff_transitivity,
bool_wf,
true_wf,
squash_wf,
es-causle_wf,
es-causl_irreflexivity,
es-causle_weakening_locl,
es-causl_transitivity2,
es-causle_weakening_eq,
it_wf,
equal-unit,
member-eo-forward-E,
es-locl_wf
\mforall{}[Info:Type]. \mforall{}[eo:EO+(Info)]. \mforall{}[e:E].
\mforall{}e1:E. (es-pred?(eo.e;e1) = if es-eq(eo) e1 e then inr \mcdot{} else es-pred?(eo;e1) fi )
Date html generated:
2012_01_23-PM-12_15_31
Last ObjectModification:
2011_12_13-PM-12_38_40
Home
Index