Nuprl Lemma : es-prior-fixedpoints-causle
[Info:Type]
es:EO+(Info). X:EClass(Top). f:E(X) 
E(X).
((x:E(X). f x c
x) 
(e,e':E(X). ((e' 
prior-f-fixedpoints(e)) e' c e)))
Proof not projected
Definitions occuring in Statement :
es-prior-fixedpoints: prior-f-fixedpoints(e),
es-E-interface: E(X),
eclass: EClass(A[eo; e]),
event-ordering+: EO+(Info),
es-causle: e c e',
uall: [x:A]. B[x],
top: Top,
all: x:A. B[x],
implies: P Q,
apply: f a,
function: x:A B[x],
universe: Type,
l_member: (x l)
Definitions :
bfalse: ff,
btrue: tt,
ifthenelse: if b then t else f fi ,
false: False,
not: 
A,
le: A B,
ge: i 
j ,
ycomb: Y,
so_lambda: 
x y.t[x; y],
guard: {T},
nat: 
,
subtype: S 
T,
so_lambda: x.t[x],
member: t T,
prop: 
,
es-prior-fixedpoints: prior-f-fixedpoints(e),
implies: P Q,
top: Top,
all: x:A. B[x],
uall: [x:A]. B[x],
and: P 
Q,
uiff: uiff(P;Q),
unit: Unit,
bool: 
,
so_apply: x[s1;s2],
exists: 
x:A. B[x],
strongwellfounded: SWellFounded(R[x; y]),
uimplies: b supposing a,
so_apply: x[s],
es-E-interface: E(X),
iff: P 
Q,
or: P 
Q,
es-locl: (e <loc e'),
es-causle: e c e',
it: 
,
!hyp_hide: x
Lemmas :
not_functionality_wrt_uiff,
assert_of_bnot,
eqff_to_assert,
assert-es-eq-E-2,
eqtt_to_assert,
uiff_transitivity,
ge_wf,
nat_properties,
not_wf,
bnot_wf,
es-interface-subtype_rel2,
es-prior-interface_wf,
in-eclass_wf,
assert_wf,
bool_wf,
es-eq-E_wf,
es-causl_wf,
less_than_wf,
event-ordering+_wf,
top_wf,
eclass_wf,
es-causle_wf,
all_wf,
l_member_wf,
le_wf,
nat_wf,
es-causl-swellfnd,
es-prior-fixedpoints_wf,
sq_stable__equal,
es-E-interface-subtype_rel,
event-ordering+_inc,
es-E_wf,
equal_wf,
es-E-interface_wf,
property-from-l_member,
eclass-val_wf2,
append_wf,
member_append,
es-prior-interface-locl,
es-causle_weakening,
es-causl_transitivity1,
es-causl_weakening,
and_wf,
es-causle_weakening_eq,
member_singleton,
es-fix_wf2,
es-causle_transitivity,
es-fix-causle,
es-fix-equal
\mforall{}[Info:Type]
\mforall{}es:EO+(Info). \mforall{}X:EClass(Top). \mforall{}f:E(X) {}\mrightarrow{} E(X).
((\mforall{}x:E(X). f x c\mleq{} x) {}\mRightarrow{} (\mforall{}e,e':E(X). ((e' \mmember{} prior-f-fixedpoints(e)) {}\mRightarrow{} e' c\mleq{} e)))
Date html generated:
2012_01_23-PM-12_28_14
Last ObjectModification:
2011_12_13-PM-02_36_55
Home
Index