Nuprl Lemma : delivered-with-headers-no_repeats
[es:EO']. [e:E]. [hdrs:Name List]. no_repeats(E;filter(
e.deq-member(NameDeq;es-header(es;e);hdrs);
loc(e)))
Proof not projected
Definitions occuring in Statement :
es-header: es-header(es;e),
Message: Message,
event-ordering+: EO+(Info),
es-le-before: loc(e),
es-E: E,
name-deq: NameDeq,
name: Name,
uall: [x:A]. B[x],
lambda: x.A[x],
list: type List,
no_repeats: no_repeats(T;l),
filter: filter(P;l),
deq-member: deq-member(eq;x;L)
Definitions :
member: t 
T,
all: x:A. B[x],
subtype: S 
T,
uall: [x:A]. B[x],
uimplies: b supposing a,
prop: 
Lemmas :
no_repeats_filter,
deq-member_wf,
name-deq_wf,
es-header_wf,
es-le-before_wf2,
es-le_wf,
es-le-before-no_repeats,
es-E_wf,
event-ordering+_inc,
Message_wf,
filter_wf,
name_wf,
event-ordering+_wf
\mforall{}[es:EO']. \mforall{}[e:E]. \mforall{}[hdrs:Name List].
no\_repeats(E;filter(\mlambda{}e.deq-member(NameDeq;es-header(es;e);hdrs);\mleq{}loc(e)))
Date html generated:
2011_10_20-PM-03_27_49
Last ObjectModification:
2011_09_05-PM-02_29_51
Home
Index