Nuprl Lemma : member-class-output

[Info,T:Type]. ∀[X:EClass(T)]. ∀[es:EO+(Info)]. ∀[bg:bag(E)]. ∀[v:T].
  uiff(v ↓∈ class-output(X;es;bg);↓∃e:E. (e ↓∈ bg ∧ v ↓∈ class-le-before(X;es;e)))


Proof




Definitions occuring in Statement :  class-output: class-output(X;es;bg) class-le-before: class-le-before(X;es;e) eclass: EClass(A[eo; e]) event-ordering+: EO+(Info) es-E: E uiff: uiff(P;Q) uall: [x:A]. B[x] exists: x:A. B[x] squash: T and: P ∧ Q universe: Type bag-member: x ↓∈ bs bag: bag(T)
Definitions unfolded in proof :  class-output: class-output(X;es;bg) uiff: uiff(P;Q) and: P ∧ Q uimplies: supposing a member: t ∈ T uall: [x:A]. B[x] subtype_rel: A ⊆B so_lambda: λ2x.t[x] so_apply: x[s] squash: T prop: rev_uimplies: rev_uimplies(P;Q) bag-member: x ↓∈ bs so_lambda: λ2y.t[x; y] so_apply: x[s1;s2]

Latex:
\mforall{}[Info,T:Type].  \mforall{}[X:EClass(T)].  \mforall{}[es:EO+(Info)].  \mforall{}[bg:bag(E)].  \mforall{}[v:T].
    uiff(v  \mdownarrow{}\mmember{}  class-output(X;es;bg);\mdownarrow{}\mexists{}e:E.  (e  \mdownarrow{}\mmember{}  bg  \mwedge{}  v  \mdownarrow{}\mmember{}  class-le-before(X;es;e)))



Date html generated: 2016_05_16-PM-01_59_10
Last ObjectModification: 2016_01_17-PM-07_40_42

Theory : event-ordering


Home Index