Nuprl Lemma : sequence-classrel
∀[Info,A,B:Type]. ∀[X:EClass(A)]. ∀[Y:EClass(B)]. ∀[Z:EClass(A)]. ∀[es:EO+(Info)]. ∀[e:E]. ∀[v:A].
uiff(v ∈ sequence-class(X;Y;Z)(e);↓((∀e':E. (e' ≤loc e ⇒ (↑e' ∈b Y) ⇒ (↑e' ∈b X))) ∧ v ∈ X(e))
∨ (∃e':E
(e' ≤loc e
∧ (↑e' ∈b Y)
∧ (¬↑e' ∈b X)
∧ (∀e'':E. ((e'' <loc e') ⇒ (↑e'' ∈b Y) ⇒ (↑e'' ∈b X)))
∧ v ∈ Z(e))))
Proof
Definitions occuring in Statement :
sequence-class: sequence-class(X;Y;Z),
classrel: v ∈ X(e),
member-eclass: e ∈b X,
eclass: EClass(A[eo; e]),
eo-forward: eo.e,
event-ordering+: EO+(Info),
es-le: e ≤loc e' ,
es-locl: (e <loc e'),
es-E: E,
assert: ↑b,
uiff: uiff(P;Q),
uall: ∀[x:A]. B[x],
all: ∀x:A. B[x],
exists: ∃x:A. B[x],
not: ¬A,
squash: ↓T,
implies: P ⇒ Q,
or: P ∨ Q,
and: P ∧ Q,
universe: Type
Lemmas :
classrel_wf,
sequence-class_wf,
squash_wf,
or_wf,
all_wf,
es-E_wf,
event-ordering+_subtype,
es-le_wf,
assert_wf,
member-eclass_wf,
exists_wf,
not_wf,
es-locl_wf,
eo-forward_wf,
member-eo-forward-E,
equal_wf,
Id_wf,
es-loc_wf,
event-ordering+_wf,
eclass_wf,
es-first-event_wf,
bnot_wf,
bool_wf,
eqtt_to_assert,
bool_cases_sqequal,
subtype_base_sq,
bool_subtype_base,
eqff_to_assert,
assert-bnot,
sq_exists_wf,
bag-member_wf,
class-ap_wf,
equal-wf-T-base,
iff_transitivity,
iff_weakening_uiff,
assert_of_band,
assert_of_bnot,
not_over_and,
decidable__not,
decidable__assert,
es-locl-trichotomy,
es-le-loc,
and_wf,
true_wf,
sq_stable__bag-member,
assert_elim,
not_assert_elim,
band_wf,
btrue_neq_bfalse
Latex:
\mforall{}[Info,A,B:Type]. \mforall{}[X:EClass(A)]. \mforall{}[Y:EClass(B)]. \mforall{}[Z:EClass(A)]. \mforall{}[es:EO+(Info)]. \mforall{}[e:E]. \mforall{}[v:A].
uiff(v \mmember{} sequence-class(X;Y;Z)(e);\mdownarrow{}((\mforall{}e':E. (e' \mleq{}loc e {}\mRightarrow{} (\muparrow{}e' \mmember{}\msubb{} Y) {}\mRightarrow{} (\muparrow{}e' \mmember{}\msubb{} X))) \mwedge{} v \mmember{} X(e))
\mvee{} (\mexists{}e':E
(e' \mleq{}loc e
\mwedge{} (\muparrow{}e' \mmember{}\msubb{} Y)
\mwedge{} (\mneg{}\muparrow{}e' \mmember{}\msubb{} X)
\mwedge{} (\mforall{}e'':E. ((e'' <loc e') {}\mRightarrow{} (\muparrow{}e'' \mmember{}\msubb{} Y) {}\mRightarrow{} (\muparrow{}e'' \mmember{}\msubb{} X)))
\mwedge{} v \mmember{} Z(e))))
Date html generated:
2015_07_21-PM-03_04_50
Last ObjectModification:
2015_01_27-PM-07_31_30
Home
Index