### 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