### Nuprl Lemma : last-concat

`∀[T:Type]`
`  ∀ll:T List List`
`    ∃ll1:T List List`
`     ∃l1:T List`
`      ((concat(ll) = (concat(ll1) @ l1 @ [last(concat(ll))]) ∈ (T List)) ∧ ll1 @ [l1 @ [last(concat(ll))]] ≤ ll) `
`    supposing ¬(concat(ll) = [] ∈ (T List))`

Proof

Definitions occuring in Statement :  iseg: `l1 ≤ l2` last: `last(L)` concat: `concat(ll)` append: `as @ bs` cons: `[a / b]` nil: `[]` list: `T List` uimplies: `b supposing a` uall: `∀[x:A]. B[x]` all: `∀x:A. B[x]` exists: `∃x:A. B[x]` not: `¬A` and: `P ∧ Q` universe: `Type` equal: `s = t ∈ T`
Definitions unfolded in proof :  uimplies: `b supposing a` member: `t ∈ T` not: `¬A` implies: `P `` Q` false: `False` uall: `∀[x:A]. B[x]` prop: `ℙ` top: `Top` all: `∀x:A. B[x]` decidable: `Dec(P)` or: `P ∨ Q` uiff: `uiff(P;Q)` and: `P ∧ Q` so_lambda: `λ2x.t[x]` so_apply: `x[s]` subtype_rel: `A ⊆r B` exists: `∃x:A. B[x]` append: `as @ bs` so_lambda: `so_lambda(x,y,z.t[x; y; z])` so_apply: `x[s1;s2;s3]` cand: `A c∧ B` iff: `P `⇐⇒` Q` rev_implies: `P `` Q` squash: `↓T` true: `True`
Lemmas referenced :  equal-wf-base list_wf nil_wf not_wf decidable__assert null_wf concat_wf assert_of_null equal-wf-T-base list_induction isect_wf exists_wf equal_wf append_wf cons_wf last_wf assert_wf length_wf length-append iseg_wf concat-nil concat-cons subtype_rel_list top_wf append_nil_sq list_ind_nil_lemma last_lemma cons_iseg nil_iseg band_wf length_of_nil_lemma null_append iff_transitivity iff_weakening_uiff assert_of_band append_assoc_sq squash_wf true_wf last_append list_ind_cons_lemma
Rules used in proof :  sqequalSubstitution sqequalTransitivity computationStep sqequalReflexivity isect_memberFormation cut introduction sqequalRule sqequalHypSubstitution lambdaEquality dependent_functionElimination thin hypothesisEquality voidElimination extract_by_obid isectElimination cumulativity hypothesis baseClosed because_Cache rename independent_functionElimination isect_memberEquality voidEquality unionElimination productElimination independent_isectElimination lambdaFormation equalityTransitivity equalitySymmetry promote_hyp productEquality addLevel impliesFunctionality levelHypothesis applyLambdaEquality universeEquality applyEquality hyp_replacement dependent_pairFormation independent_pairFormation imageElimination natural_numberEquality imageMemberEquality

Latex:
\mforall{}[T:Type]
\mforall{}ll:T  List  List
\mexists{}ll1:T  List  List
\mexists{}l1:T  List
((concat(ll)  =  (concat(ll1)  @  l1  @  [last(concat(ll))]))
\mwedge{}  ll1  @  [l1  @  [last(concat(ll))]]  \mleq{}  ll)
supposing  \mneg{}(concat(ll)  =  [])

Date html generated: 2017_04_17-AM-08_51_28
Last ObjectModification: 2017_02_27-PM-05_09_33

Theory : list_1

Home Index