### Nuprl Lemma : last-concat-non-null

`∀[T:Type]. ∀[ll:T List List].`
`  ((¬↑null(concat(ll))) ∧ (last(concat(ll)) = last(last(ll)) ∈ T)) supposing ((¬↑null(last(ll))) and (¬↑null(ll)))`

Proof

Definitions occuring in Statement :  last: `last(L)` null: `null(as)` concat: `concat(ll)` list: `T List` assert: `↑b` uimplies: `b supposing a` uall: `∀[x:A]. B[x]` not: `¬A` and: `P ∧ Q` universe: `Type` equal: `s = t ∈ T`
Definitions unfolded in proof :  uall: `∀[x:A]. B[x]` member: `t ∈ T` so_lambda: `λ2x.t[x]` uimplies: `b supposing a` prop: `ℙ` and: `P ∧ Q` so_apply: `x[s]` implies: `P `` Q` concat: `concat(ll)` all: `∀x:A. B[x]` top: `Top` assert: `↑b` ifthenelse: `if b then t else f fi ` btrue: `tt` bfalse: `ff` not: `¬A` false: `False` true: `True` or: `P ∨ Q` cons: `[a / b]` last: `last(L)` subtract: `n - m` select: `L[n]` subtype_rel: `A ⊆r B` cand: `A c∧ B` squash: `↓T` guard: `{T}` uiff: `uiff(P;Q)` rev_uimplies: `rev_uimplies(P;Q)` iff: `P `⇐⇒` Q` rev_implies: `P `` Q`
Lemmas referenced :  list_induction list_wf isect_wf not_wf assert_wf null_wf last_wf concat_wf equal_wf null_nil_lemma reduce_nil_lemma null_cons_lemma true_wf list-cases product_subtype_list reduce_cons_lemma length_of_cons_lemma length_of_nil_lemma subtype_rel_list top_wf false_wf append-nil assert_functionality_wrt_uiff cons_wf assert_elim bfalse_wf btrue_neq_bfalse squash_wf last_cons concat-cons null_append assert_of_null append_wf band_wf equal-wf-T-base length_wf iff_transitivity iff_weakening_uiff assert_of_band last_append iff_weakening_equal
Rules used in proof :  sqequalSubstitution sqequalTransitivity computationStep sqequalReflexivity isect_memberFormation introduction cut thin extract_by_obid sqequalHypSubstitution isectElimination cumulativity hypothesisEquality hypothesis sqequalRule lambdaEquality because_Cache independent_isectElimination productEquality independent_functionElimination dependent_functionElimination isect_memberEquality voidElimination voidEquality lambdaFormation rename productElimination independent_pairEquality axiomEquality equalityTransitivity equalitySymmetry universeEquality natural_numberEquality unionElimination promote_hyp hypothesis_subsumption applyEquality independent_pairFormation addLevel levelHypothesis imageElimination imageMemberEquality baseClosed applyLambdaEquality hyp_replacement impliesFunctionality

Latex:
\mforall{}[T:Type].  \mforall{}[ll:T  List  List].
((\mneg{}\muparrow{}null(concat(ll)))  \mwedge{}  (last(concat(ll))  =  last(last(ll))))  supposing
((\mneg{}\muparrow{}null(last(ll)))  and
(\mneg{}\muparrow{}null(ll)))

Date html generated: 2017_04_17-AM-08_51_40
Last ObjectModification: 2017_02_27-PM-05_10_00

Theory : list_1

Home Index