### Nuprl Lemma : cons_succ

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

Proof

Definitions occuring in Statement :  l_succ: l_succ length: `||as||` hd: `hd(l)` cons: `[a / b]` list: `T List` less_than: `a < b` uimplies: `b supposing a` uall: `∀[x:A]. B[x]` prop: `ℙ` so_apply: `x[s]` all: `∀x:A. B[x]` not: `¬A` implies: `P `` Q` and: `P ∧ Q` function: `x:A ⟶ B[x]` natural_number: `\$n` universe: `Type` equal: `s = t ∈ T`
Definitions unfolded in proof :  l_succ: l_succ uall: `∀[x:A]. B[x]` all: `∀x:A. B[x]` implies: `P `` Q` and: `P ∧ Q` cand: `A c∧ B` uimplies: `b supposing a` member: `t ∈ T` prop: `ℙ` not: `¬A` false: `False` nat: `ℕ` top: `Top` ge: `i ≥ j ` 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 ⊆r B` select: `L[n]` cons: `[a / b]` subtract: `n - m` le: `A ≤ B` less_than': `less_than'(a;b)` nil: `[]` it: `⋅` so_lambda: `λ2x y.t[x; y]` so_apply: `x[s1;s2]` guard: `{T}` iff: `P `⇐⇒` 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

Latex:
\mforall{}[T:Type]
\mforall{}l:T  List
\mforall{}[P:T  {}\mrightarrow{}  \mBbbP{}]
\mforall{}a,x:T.
(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