Nuprl Lemma : es-before-decomp
∀the_es:EO. ∀e',e:E. ((e ∈ before(e')) ⇒ (∃l:E List. (before(e') = (before(e) @ [e] @ l) ∈ (E List))))
Proof
Definitions occuring in Statement :
es-before: before(e),
es-E: E,
event_ordering: EO,
l_member: (x ∈ l),
append: as @ bs,
cons: [a / b],
nil: [],
list: T List,
all: ∀x:A. B[x],
exists: ∃x:A. B[x],
implies: P ⇒ Q,
equal: s = t ∈ T
Lemmas :
l_member_decomp,
append_wf,
cons_wf,
nil_wf,
equal_wf,
es-before_wf,
exists_wf,
list_wf,
l_member_wf,
es-E_wf,
event_ordering_wf,
firstn-before,
length_wf_nat,
length_wf,
subtype_rel_list,
top_wf,
length_nil,
non_neg_length,
length_wf_nil,
length_cons,
less_than_wf,
squash_wf,
true_wf,
length_append,
add_functionality_wrt_eq,
iff_weakening_equal,
firstn_wf,
firstn_append,
firstn_length,
select_wf,
select_append_back,
list_ind_cons_lemma,
list_ind_nil_lemma,
length_of_cons_lemma,
select_append_front,
length_of_nil_lemma,
subtract_wf,
select-cons-hd
\mforall{}the$_{es}$:EO. \mforall{}e',e:E. ((e \mmember{} before(e')) {}\mRightarrow{} (\mexists{}l:E List. (before(e') = (before\000C(e) @ [e] @ l))))
Date html generated:
2015_07_17-AM-08_44_02
Last ObjectModification:
2015_02_04-AM-07_10_20
Home
Index