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: List assert: b uimplies: supposing a uall: [x:A]. B[x] not: ¬A and: P ∧ Q universe: Type equal: t ∈ T
Definitions unfolded in proof :  uall: [x:A]. B[x] member: t ∈ T so_lambda: λ2x.t[x] uimplies: supposing a prop: and: P ∧ Q so_apply: x[s] implies:  Q concat: concat(ll) all: x:A. B[x] top: Top assert: b ifthenelse: if then else fi  btrue: tt bfalse: ff not: ¬A false: False true: True or: P ∨ Q cons: [a b] last: last(L) subtract: m select: L[n] subtype_rel: A ⊆B cand: c∧ B squash: T guard: {T} uiff: uiff(P;Q) rev_uimplies: rev_uimplies(P;Q) iff: ⇐⇒ Q rev_implies:  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