Nuprl Lemma : iseg-filter-es-interval

[es:EO]. ∀[L:E List]. ∀[e1,e2:E]. ∀[P:{x:E| (x ∈ [e1, e2])}  ─→ 𝔹].
  (L filter(P;[e1, last(L)]) ∈ (E List)) supposing ((¬↑null(L)) and L ≤ filter(P;[e1, e2]))


Definitions occuring in Statement :  es-interval: [e, e'] es-E: E event_ordering: EO iseg: l1 ≤ l2 last: last(L) l_member: (x ∈ l) filter: filter(P;l) null: null(as) list: List assert: b bool: 𝔹 uimplies: supposing a uall: [x:A]. B[x] not: ¬A set: {x:A| B[x]}  function: x:A ─→ B[x] equal: t ∈ T
Lemmas :  last_member iseg_member last_wf member_filter_2 not_wf assert_wf null_wf3 subtype_rel_list es-E_wf top_wf iseg_wf filter_wf5 es-interval_wf l_member_wf bool_wf list_wf event_ordering_wf l-ordered-equality es-locl_wf es-locl-antireflexive es-locl_transitivity2 es-le_weakening es-locl_irreflexivity member-es-interval es-le_transitivity subtype_rel_self set_wf subtype_rel_dep_function subtype_rel_sets l-ordered-filter2 es-interval-ordered iseg-l-ordered before_last_or es-le-self es-le_wf l-ordered-is-sorted-by l_before-sorted-by equal_wf member-iseg-sorted-by
\mforall{}[es:EO].  \mforall{}[L:E  List].  \mforall{}[e1,e2:E].  \mforall{}[P:\{x:E|  (x  \mmember{}  [e1,  e2])\}    {}\mrightarrow{}  \mBbbB{}].
    (L  =  filter(P;[e1,  last(L)]))  supposing  ((\mneg{}\muparrow{}null(L))  and  L  \mleq{}  filter(P;[e1,  e2]))

Date html generated: 2015_07_17-AM-08_44_49
Last ObjectModification: 2015_01_27-PM-02_30_54

Home Index