Nuprl Lemma : listp_decomp_last

[T:Type]. ∀L:T List+. ∃K:T List. (L (K [last(L)]) ∈ (T List))


Proof




Definitions occuring in Statement :  last: last(L) listp: List+ append: as bs cons: [a b] nil: [] list: List uall: [x:A]. B[x] all: x:A. B[x] exists: x:A. B[x] universe: Type equal: t ∈ T
Definitions unfolded in proof :  uall: [x:A]. B[x] all: x:A. B[x] member: t ∈ T listp: List+ uimplies: supposing a ge: i ≥  decidable: Dec(P) or: P ∨ Q le: A ≤ B and: P ∧ Q satisfiable_int_formula: satisfiable_int_formula(fmla) exists: x:A. B[x] false: False implies:  Q not: ¬A top: Top prop:
Lemmas referenced :  listp_wf int_formula_prop_wf int_formula_prop_le_lemma int_term_value_var_lemma int_term_value_constant_lemma int_formula_prop_less_lemma int_formula_prop_not_lemma int_formula_prop_and_lemma intformle_wf itermVar_wf itermConstant_wf intformless_wf intformnot_wf intformand_wf satisfiable-full-omega-tt length_wf decidable__lt list_decomp_last listp_properties
Rules used in proof :  sqequalSubstitution sqequalTransitivity computationStep sqequalReflexivity isect_memberFormation lambdaFormation cut lemma_by_obid sqequalHypSubstitution isectElimination thin hypothesisEquality hypothesis setElimination rename dependent_functionElimination independent_isectElimination natural_numberEquality unionElimination productElimination dependent_pairFormation lambdaEquality int_eqEquality intEquality isect_memberEquality voidElimination voidEquality sqequalRule independent_pairFormation computeAll universeEquality

Latex:
\mforall{}[T:Type].  \mforall{}L:T  List\msupplus{}.  \mexists{}K:T  List.  (L  =  (K  @  [last(L)]))



Date html generated: 2016_05_14-PM-03_00_56
Last ObjectModification: 2016_01_15-AM-07_23_38

Theory : list_1


Home Index