Nuprl Lemma : before_last

`∀[T:Type]. ∀L:T List. ∀x:T.  ((x ∈ L) `` x before last(L) ∈ L supposing ¬(x = last(L) ∈ T))`

Proof

Definitions occuring in Statement :  l_before: `x before y ∈ l` last: `last(L)` l_member: `(x ∈ l)` list: `T List` uimplies: `b supposing a` uall: `∀[x:A]. B[x]` all: `∀x:A. B[x]` not: `¬A` implies: `P `` Q` universe: `Type` equal: `s = t ∈ T`
Definitions unfolded in proof :  uall: `∀[x:A]. B[x]` all: `∀x:A. B[x]` member: `t ∈ T` so_lambda: `λ2x.t[x]` implies: `P `` Q` prop: `ℙ` uimplies: `b supposing a` not: `¬A` false: `False` so_apply: `x[s]` iff: `P `⇐⇒` Q` and: `P ∧ Q` top: `Top` or: `P ∨ Q` l_before: `x before y ∈ l` rev_implies: `P `` Q` uiff: `uiff(P;Q)` last: `last(L)` select: `L[n]` cons: `[a / b]` subtract: `n - m` length: `||as||` list_ind: list_ind nil: `[]` it: `⋅` assert: `↑b` ifthenelse: `if b then t else f fi ` btrue: `tt` bfalse: `ff` true: `True` squash: `↓T` subtype_rel: `A ⊆r B` guard: `{T}`
Lemmas referenced :  list_induction all_wf l_member_wf not_wf equal_wf last_wf assert_elim null_wf member-implies-null-eq-bfalse btrue_neq_bfalse assert_wf l_before_wf list_wf nil_member nil_wf cons_wf null_cons_lemma istype-void bfalse_wf cons_member cons_sublist_cons assert_of_null list-cases null_nil_lemma btrue_wf product_subtype_list false_wf squash_wf true_wf last_cons iff_weakening_equal sublist_wf subtype_rel_self member_iff_sublist last_member
Rules used in proof :  sqequalSubstitution sqequalTransitivity computationStep sqequalReflexivity Error :isect_memberFormation_alt,  Error :lambdaFormation_alt,  cut thin introduction extract_by_obid sqequalHypSubstitution isectElimination hypothesisEquality sqequalRule Error :lambdaEquality_alt,  cumulativity functionEquality because_Cache hypothesis isectEquality independent_isectElimination equalityTransitivity equalitySymmetry independent_functionElimination voidElimination Error :universeIsType,  rename Error :functionIsType,  Error :inhabitedIsType,  Error :isectIsType,  dependent_functionElimination universeEquality productElimination Error :equalityIsType1,  Error :isect_memberEquality_alt,  Error :unionIsType,  unionElimination hyp_replacement applyLambdaEquality promote_hyp hypothesis_subsumption natural_numberEquality applyEquality imageElimination imageMemberEquality baseClosed Error :inlFormation_alt,  instantiate independent_pairFormation Error :inrFormation_alt,  Error :productIsType

Latex:
\mforall{}[T:Type].  \mforall{}L:T  List.  \mforall{}x:T.    ((x  \mmember{}  L)  {}\mRightarrow{}  x  before  last(L)  \mmember{}  L  supposing  \mneg{}(x  =  last(L)))

Date html generated: 2019_06_20-PM-01_23_37
Last ObjectModification: 2018_09_29-PM-00_04_11

Theory : list_1

Home Index