Nuprl Lemma : doublefact_wf

[n:ℤ]. (doublefact(n) ∈ ℕ+)


Proof




Definitions occuring in Statement :  doublefact: doublefact(n) nat_plus: + uall: [x:A]. B[x] member: t ∈ T int:
Definitions unfolded in proof :  all: x:A. B[x] uall: [x:A]. B[x] member: t ∈ T nat: implies:  Q false: False ge: i ≥  uimplies: supposing a not: ¬A satisfiable_int_formula: satisfiable_int_formula(fmla) exists: x:A. B[x] top: Top and: P ∧ Q prop: guard: {T} int_seg: {i..j-} lelt: i ≤ j < k decidable: Dec(P) or: P ∨ Q subtype_rel: A ⊆B so_lambda: λ2x.t[x] so_apply: x[s] sq_type: SQType(T) doublefact: doublefact(n) bool: 𝔹 unit: Unit it: btrue: tt ifthenelse: if then else fi  uiff: uiff(P;Q) nat_plus: + less_than: a < b squash: T less_than': less_than'(a;b) true: True bfalse: ff bnot: ¬bb assert: b rev_implies:  Q iff: ⇐⇒ Q
Lemmas referenced :  nat_properties full-omega-unsat intformand_wf intformle_wf itermConstant_wf itermVar_wf intformless_wf istype-int int_formula_prop_and_lemma istype-void int_formula_prop_le_lemma int_term_value_constant_lemma int_term_value_var_lemma int_formula_prop_less_lemma int_formula_prop_wf ge_wf istype-less_than int_seg_properties int_seg_wf subtract-1-ge-0 decidable__equal_int subtract_wf subtype_base_sq set_subtype_base int_subtype_base intformnot_wf intformeq_wf itermSubtract_wf int_formula_prop_not_lemma int_formula_prop_eq_lemma int_term_value_subtract_lemma decidable__le decidable__lt istype-le subtype_rel_self lt_int_wf eqtt_to_assert assert_of_lt_int eqff_to_assert bool_cases_sqequal bool_wf bool_subtype_base assert-bnot iff_weakening_uiff assert_wf less_than_wf mul_nat_plus itermAdd_wf int_term_value_add_lemma istype-nat uiff_transitivity equal-wf-base le_int_wf le_wf bnot_wf assert_functionality_wrt_uiff bnot_of_lt_int assert_of_le_int
Rules used in proof :  cut sqequalSubstitution sqequalTransitivity computationStep sqequalReflexivity Error :lambdaFormation_alt,  thin introduction extract_by_obid sqequalHypSubstitution isectElimination hypothesisEquality hypothesis setElimination rename sqequalRule intWeakElimination natural_numberEquality independent_isectElimination approximateComputation independent_functionElimination Error :dependent_pairFormation_alt,  Error :lambdaEquality_alt,  int_eqEquality dependent_functionElimination Error :isect_memberEquality_alt,  voidElimination independent_pairFormation Error :universeIsType,  axiomEquality equalityTransitivity equalitySymmetry Error :functionIsTypeImplies,  Error :inhabitedIsType,  productElimination because_Cache unionElimination applyEquality instantiate applyLambdaEquality Error :dependent_set_memberEquality_alt,  Error :productIsType,  hypothesis_subsumption closedConclusion equalityElimination imageMemberEquality baseClosed Error :equalityIstype,  promote_hyp cumulativity addEquality Error :isect_memberFormation_alt,  baseApply

Latex:
\mforall{}[n:\mBbbZ{}].  (doublefact(n)  \mmember{}  \mBbbN{}\msupplus{})



Date html generated: 2019_06_20-PM-02_30_53
Last ObjectModification: 2019_01_04-PM-06_45_59

Theory : num_thy_1


Home Index