Nuprl Lemma : iseg-es-interval

[es:EO]. ∀[L:E List]. ∀[e1,e2:E].  (L [e1, last(L)] ∈ (E List)) supposing ((¬↑null(L)) and L ≤ [e1, e2])


Definitions occuring in Statement :  es-interval: [e, e'] es-E: E event_ordering: EO iseg: l1 ≤ l2 last: last(L) null: null(as) list: List assert: b uimplies: supposing a uall: [x:A]. B[x] not: ¬A equal: t ∈ T
Lemmas :  iseg_filter es-ble_wf append_wf es-before_wf cons_wf nil_wf not_wf assert_wf null_wf3 subtype_rel_list es-E_wf top_wf iseg_wf es-interval_wf list_wf event_ordering_wf l_member_wf es-le-before_wf2 last_wf es-le_wf set_wf filter_wf5 squash_wf true_wf bool_wf iff_weakening_equal assert_functionality_wrt_uiff assert_elim and_wf equal_wf not_assert_elim btrue_neq_bfalse null-filter2 l_all_wf2 l_all_not l_exists_wf assert-bl-exists bl-exists_wf not-not-assert l_exists_iff assert-es-ble member_null decidable__equal_int subtract_wf length_wf es-le-before-ordered iseg-l-ordered es-locl_wf l-ordered-inst decidable__le false_wf not-le-2 sq_stable__le less-iff-le condition-implies-le minus-one-mul zero-add minus-add minus-minus add-associates add-swap add-commutes add_functionality_wrt_le add-zero le-add-cancel subtract-is-less lelt_wf decidable__lt not-equal-2 le-add-cancel-alt es-locl_transitivity1 es-le_weakening select_wf le_wf less_than_wf list_decomp_last list-cases length_of_nil_lemma nil_member product_subtype_list length_of_cons_lemma length_wf_nat nat_wf iseg-es-le-before-is-before last-filter1
\mforall{}[es:EO].  \mforall{}[L:E  List].  \mforall{}[e1,e2:E].    (L  =  [e1,  last(L)])  supposing  ((\mneg{}\muparrow{}null(L))  and  L  \mleq{}  [e1,  e2])

Date html generated: 2015_07_17-AM-08_44_41
Last ObjectModification: 2015_02_04-AM-07_09_48

Home Index