Nuprl Lemma : until-classrel
∀[Info,A,B:Type]. ∀[X:EClass(A)]. ∀[Y:EClass(B)]. ∀[es:EO+(Info)]. ∀[e:E]. ∀[v:A].
(v ∈ (X until Y)(e) ⇐⇒ (no Y prior to e) ∧ v ∈ X(e))
Proof
Definitions occuring in Statement :
until-class: (X until Y),
no-prior-classrel: (no X prior to e),
classrel: v ∈ X(e),
eclass: EClass(A[eo; e]),
event-ordering+: EO+(Info),
es-E: E,
uall: ∀[x:A]. B[x],
iff: P ⇐⇒ Q,
and: P ∧ Q,
universe: Type
Lemmas :
class-pred-cases,
classrel_wf,
until-class_wf,
es-interface-subtype_rel2,
es-E_wf,
event-ordering+_subtype,
event-ordering+_wf,
top_wf,
alle-lt_wf,
Id_wf,
es-loc_wf,
all_wf,
not_wf,
bag-member_wf,
squash_wf,
true_wf,
bag_wf,
empty-bag_wf,
iff_weakening_equal,
bag-member-empty
Latex:
\mforall{}[Info,A,B:Type]. \mforall{}[X:EClass(A)]. \mforall{}[Y:EClass(B)]. \mforall{}[es:EO+(Info)]. \mforall{}[e:E]. \mforall{}[v:A].
(v \mmember{} (X until Y)(e) \mLeftarrow{}{}\mRightarrow{} (no Y prior to e) \mwedge{} v \mmember{} X(e))
Date html generated:
2015_07_20-PM-03_59_07
Last ObjectModification:
2015_02_04-PM-05_28_35
Home
Index