Nuprl Lemma : class-opt-class-classrel

[Info,T:Type]. ∀[X,Y:EClass(T)]. ∀[v:T]. ∀[es:EO+(Info)]. ∀[e:E].
  uiff(v ∈ X?Y(e);↓((↑bag-null(X es e)) ∧ v ∈ Y(e)) ∨ ((¬↑bag-null(X es e)) ∧ v ∈ X(e)))


Proof




Definitions occuring in Statement :  class-opt-class: X?Y classrel: v ∈ X(e) eclass: EClass(A[eo; e]) event-ordering+: EO+(Info) es-E: E assert: b uiff: uiff(P;Q) uall: [x:A]. B[x] not: ¬A squash: T or: P ∨ Q and: P ∧ Q apply: a universe: Type bag-null: bag-null(bs)
Lemmas :  classrel_wf class-opt-class_wf squash_wf or_wf assert_wf bag-null_wf not_wf es-E_wf event-ordering+_subtype event-ordering+_wf eclass_wf bool_cases subtype_base_sq bool_wf bool_subtype_base eqtt_to_assert assert-bag-null eqff_to_assert iff_transitivity bnot_wf equal-wf-T-base bag_wf iff_weakening_uiff assert_of_bnot sq_stable__classrel uiff_transitivity

Latex:
\mforall{}[Info,T:Type].  \mforall{}[X,Y:EClass(T)].  \mforall{}[v:T].  \mforall{}[es:EO+(Info)].  \mforall{}[e:E].
    uiff(v  \mmember{}  X?Y(e);\mdownarrow{}((\muparrow{}bag-null(X  es  e))  \mwedge{}  v  \mmember{}  Y(e))  \mvee{}  ((\mneg{}\muparrow{}bag-null(X  es  e))  \mwedge{}  v  \mmember{}  X(e)))



Date html generated: 2015_07_22-PM-00_08_19
Last ObjectModification: 2015_01_28-AM-11_41_58

Home Index