Nuprl Lemma : es-interface-predecessors-le

{

[Info:Type].

es:EO+(Info).

X:EClass(Top).

e:E. (

a

(X)(e).a

loc e ) }

{ Proof }

Definitions occuring in Statement : es-interface-predecessors:

(X)(e), es-E-interface: E(X), eclass: EClass(A[eo; e]), event-ordering+: EO+(Info), es-le: e

loc e' , es-E: E, uall:

[x:A]. B[x], top: Top, all:

x:A. B[x], universe: Type, l_all: (

x

L.P[x])
Definitions : uall:

[x:A]. B[x], all:

x:A. B[x], l_all: (

x

L.P[x]), es-interface-predecessors:

(X)(e), implies: P

Q, member: t

T, subtype: S

T, so_lambda:

x y.t[x; y], so_apply: x[s1;s2], iff: P

Q, and: P

Q, es-E-interface: E(X), prop:

Lemmas : l_member_wf, es-E-interface_wf, eclass-events_wf, es-le-before_wf, es-E_wf, Id_wf, es-loc_wf, event-ordering+_inc, eclass_wf, top_wf, event-ordering+_wf, member-es-interface-events, member-es-le-before

\mforall{}[Info:Type]. \mforall{}es:EO+(Info). \mforall{}X:EClass(Top). \mforall{}e:E. (\mforall{}a\mmember{}\mleq{}(X)(e).a \mleq{}loc e ) Date html generated: 2011_08_16-PM-05_15_54 Last ObjectModification: 2011_06_20-AM-01_18_11 Home Index