Nuprl Lemma : es-history-accum_wf
[B,A:
']. [f:A 
B B]. [x:B]. [es:EO']. [L:(A 
E) List]. (es-history-accum(es;A;B;x;f;L) 
B)
Proof not projected
Definitions occuring in Statement :
es-history-accum: es-history-accum(es;A;B;x;f;L),
Message: Message,
event-ordering+: EO+(Info),
es-E: E,
uall: [x:A]. B[x],
member: t T,
function: x:A B[x],
product: x:A B[x],
list: type List,
universe: Type
Definitions :
uall: [x:A]. B[x],
member: t T,
es-history-accum: es-history-accum(es;A;B;x;f;L),
top: Top,
all: x:A. B[x],
subtype: S 
T,
so_lambda: 
x y.t[x; y],
so_apply: x[s1;s2]
Lemmas :
list_accum_wf,
map_wf,
pi1_wf_top,
es-E_wf,
event-ordering+_inc,
Message_wf,
event-ordering+_wf
\mforall{}[B,A:\mBbbU{}']. \mforall{}[f:A {}\mrightarrow{} B {}\mrightarrow{} B]. \mforall{}[x:B]. \mforall{}[es:EO']. \mforall{}[L:(A \mtimes{} E) List].
(es-history-accum(es;A;B;x;f;L) \mmember{} B)
Date html generated:
2012_01_23-PM-01_18_41
Last ObjectModification:
2012_01_07-PM-02_38_29
Home
Index