Nuprl Lemma : cons_succ

  ∀l:T List
    ∀[P:T ⟶ ℙ]
        (y succ(x) in [a l]
         ((P[hd(l)]) supposing (0 < ||l|| and (x a ∈ T)) ∧ succ(x) in l P[y] supposing ¬(x a ∈ T)))


Definitions occuring in Statement :  l_succ: l_succ length: ||as|| hd: hd(l) cons: [a b] list: List less_than: a < b uimplies: supposing a uall: [x:A]. B[x] prop: so_apply: x[s] all: x:A. B[x] not: ¬A implies:  Q and: P ∧ Q function: x:A ⟶ B[x] natural_number: $n universe: Type equal: t ∈ T
Definitions unfolded in proof :  l_succ: l_succ uall: [x:A]. B[x] all: x:A. B[x] implies:  Q and: P ∧ Q cand: c∧ B uimplies: supposing a member: t ∈ T prop: not: ¬A false: False nat: top: Top ge: i ≥  decidable: Dec(P) or: P ∨ Q satisfiable_int_formula: satisfiable_int_formula(fmla) exists: x:A. B[x] less_than: a < b squash: T uiff: uiff(P;Q) so_apply: x[s] subtype_rel: A ⊆B select: L[n] cons: [a b] subtract: m le: A ≤ B less_than': less_than'(a;b) nil: [] it: so_lambda: λ2y.t[x; y] so_apply: x[s1;s2] guard: {T} iff: ⇐⇒ Q
Lemmas referenced :  member-less_than length_wf less_than_wf select_wf length_of_cons_lemma istype-void nat_properties decidable__le full-omega-unsat intformand_wf intformnot_wf intformle_wf itermConstant_wf itermVar_wf istype-int int_formula_prop_and_lemma int_formula_prop_not_lemma int_formula_prop_le_lemma int_term_value_constant_lemma int_term_value_var_lemma int_formula_prop_wf decidable__lt intformless_wf itermAdd_wf int_formula_prop_less_lemma int_term_value_add_lemma nat_wf not_wf equal_wf cons_wf add-is-int-iff false_wf istype-universe list_wf list-cases length_of_nil_lemma istype-false product_subtype_list le_wf stuck-spread istype-base reduce_hd_cons_lemma select-cons-tl add-subtract-cancel select_cons_tl subtype_rel_self iff_weakening_equal
Rules used in proof :  sqequalSubstitution sqequalRule sqequalReflexivity sqequalTransitivity computationStep isect_memberFormation_alt lambdaFormation_alt cut introduction axiomEquality hypothesis thin rename extract_by_obid sqequalHypSubstitution isectElimination natural_numberEquality hypothesisEquality independent_isectElimination universeIsType equalityIsType1 inhabitedIsType independent_pairFormation lambdaEquality_alt dependent_functionElimination voidElimination functionIsTypeImplies setElimination because_Cache isect_memberEquality_alt unionElimination approximateComputation independent_functionElimination dependent_pairFormation_alt int_eqEquality imageElimination productElimination addEquality functionIsType pointwiseFunctionality equalityTransitivity equalitySymmetry promote_hyp baseApply closedConclusion baseClosed applyEquality universeEquality dependent_set_memberEquality_alt hypothesis_subsumption instantiate

    \mforall{}l:T  List
        \mforall{}[P:T  {}\mrightarrow{}  \mBbbP{}]
                (y  =  succ(x)  in  [a  /  l]
                {}\mRightarrow{}  P[y]
                {}\mRightarrow{}  ((P[hd(l)])  supposing  (0  <  ||l||  and  (x  =  a))  \mwedge{}  y  =  succ(x)  in  l{}\mRightarrow{}  P[y]  supposing  \mneg{}(x  =  a\000C)))

Date html generated: 2019_10_15-AM-10_53_20
Last ObjectModification: 2018_10_09-AM-09_54_24

Theory : list!

Home Index