### Nuprl Lemma : polynom-subtype-list

`∀[n:ℕ+]. (polynom(n) ⊆r (polynom(n - 1) List))`

Proof

Definitions occuring in Statement :  polynom: `polynom(n)` list: `T List` nat_plus: `ℕ+` subtype_rel: `A ⊆r B` uall: `∀[x:A]. B[x]` subtract: `n - m` natural_number: `\$n`
Definitions unfolded in proof :  polyform: `polyform(n)` rev_implies: `P `` Q` iff: `P `⇐⇒` Q` bfalse: `ff` ifthenelse: `if b then t else f fi ` uiff: `uiff(P;Q)` btrue: `tt` it: `⋅` unit: `Unit` bool: `𝔹` or: `P ∨ Q` decidable: `Dec(P)` nat: `ℕ` prop: `ℙ` and: `P ∧ Q` top: `Top` all: `∀x:A. B[x]` not: `¬A` implies: `P `` Q` false: `False` exists: `∃x:A. B[x]` satisfiable_int_formula: `satisfiable_int_formula(fmla)` uimplies: `b supposing a` nat_plus: `ℕ+` polynom: `polynom(n)` subtype_rel: `A ⊆r B` member: `t ∈ T` uall: `∀[x:A]. B[x]`
Lemmas referenced :  polynom_subtype_polyform polyform_wf subtype_rel_list equal_wf assert_of_bnot eqff_to_assert iff_weakening_uiff iff_transitivity assert_of_eq_int eqtt_to_assert uiff_transitivity nat_plus_subtype_nat polyform-lead-nonzero_wf le_wf int_term_value_subtract_lemma int_formula_prop_le_lemma int_formula_prop_not_lemma itermSubtract_wf intformle_wf intformnot_wf decidable__le subtract_wf polynom_wf list_wf not_wf bnot_wf int_formula_prop_wf int_formula_prop_less_lemma int_term_value_constant_lemma int_term_value_var_lemma int_formula_prop_eq_lemma int_formula_prop_and_lemma intformless_wf itermConstant_wf itermVar_wf intformeq_wf intformand_wf satisfiable-full-omega-tt nat_plus_properties assert_wf equal-wf-T-base bool_wf eq_int_wf nat_plus_wf
Rules used in proof :  impliesFunctionality productElimination independent_functionElimination equalityElimination lambdaFormation applyEquality unionElimination dependent_set_memberEquality setEquality computeAll independent_pairFormation voidEquality voidElimination isect_memberEquality dependent_functionElimination int_eqEquality lambdaEquality dependent_pairFormation independent_isectElimination intEquality because_Cache baseClosed equalitySymmetry equalityTransitivity natural_numberEquality hypothesisEquality rename setElimination thin isectElimination sqequalHypSubstitution extract_by_obid hypothesis axiomEquality sqequalRule cut introduction isect_memberFormation sqequalReflexivity computationStep sqequalTransitivity sqequalSubstitution

Latex:
\mforall{}[n:\mBbbN{}\msupplus{}].  (polynom(n)  \msubseteq{}r  (polynom(n  -  1)  List))

Date html generated: 2017_04_20-AM-07_08_16
Last ObjectModification: 2017_04_19-AM-11_31_03

Theory : list_1

Home Index