Nuprl Lemma : genfact-step

[n:ℤ]. ∀[f:ℕ+ ⟶ ℤ]. ∀[b:ℤ].  (genfact(n;b;m.f[m]) if n <then else f[n] genfact(n 1;b;m.f[m]) fi  ∈ ℤ)


Proof




Definitions occuring in Statement :  genfact: genfact(n;b;m.f[m]) nat_plus: + ifthenelse: if then else fi  lt_int: i <j uall: [x:A]. B[x] so_apply: x[s] function: x:A ⟶ B[x] multiply: m subtract: m natural_number: $n int: equal: t ∈ T
Definitions unfolded in proof :  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] all: x:A. B[x] top: Top and: P ∧ Q prop: bool: 𝔹 unit: Unit it: btrue: tt uiff: uiff(P;Q) ifthenelse: if then else fi  genfact: genfact(n;b;m.f[m]) bfalse: ff or: P ∨ Q sq_type: SQType(T) guard: {T} bnot: ¬bb assert: b rev_implies:  Q iff: ⇐⇒ Q subtract: m less_than: a < b less_than': less_than'(a;b) true: True squash: T so_apply: x[s] nat_plus: + decidable: Dec(P) has-value: (a)↓ so_lambda: λ2x.t[x] subtype_rel: A ⊆B
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 lt_int_wf eqtt_to_assert assert_of_lt_int eqff_to_assert bool_cases_sqequal subtype_base_sq bool_wf bool_subtype_base assert-bnot iff_weakening_uiff assert_wf less_than_wf intformnot_wf int_formula_prop_not_lemma nat_plus_wf subtract-1-ge-0 istype-top decidable__lt value-type-has-value int-value-type subtract_wf istype-nat decidable__le equal_wf istype-le genfact_wf iff_weakening_equal decidable__equal_int intformeq_wf itermMultiply_wf int_formula_prop_eq_lemma int_term_value_mul_lemma squash_wf true_wf istype-universe genfact-base-linear subtype_rel_self
Rules used in proof :  cut sqequalSubstitution sqequalTransitivity computationStep sqequalReflexivity Error :isect_memberFormation_alt,  introduction extract_by_obid sqequalHypSubstitution isectElimination thin hypothesisEquality hypothesis setElimination rename intWeakElimination Error :lambdaFormation_alt,  natural_numberEquality independent_isectElimination approximateComputation independent_functionElimination Error :dependent_pairFormation_alt,  Error :lambdaEquality_alt,  int_eqEquality dependent_functionElimination Error :isect_memberEquality_alt,  voidElimination sqequalRule independent_pairFormation Error :universeIsType,  axiomEquality Error :isectIsTypeImplies,  Error :inhabitedIsType,  Error :functionIsTypeImplies,  unionElimination equalityElimination because_Cache productElimination equalityTransitivity equalitySymmetry Error :equalityIstype,  promote_hyp instantiate cumulativity Error :functionIsType,  lessCases axiomSqEquality imageMemberEquality baseClosed imageElimination applyEquality Error :dependent_set_memberEquality_alt,  callbyvalueReduce intEquality multiplyEquality closedConclusion universeEquality

Latex:
\mforall{}[n:\mBbbZ{}].  \mforall{}[f:\mBbbN{}\msupplus{}  {}\mrightarrow{}  \mBbbZ{}].  \mforall{}[b:\mBbbZ{}].
    (genfact(n;b;m.f[m])  =  if  n  <z  1  then  b  else  f[n]  *  genfact(n  -  1;b;m.f[m])  fi  )



Date html generated: 2019_06_20-PM-02_25_44
Last ObjectModification: 2019_02_08-AM-11_48_54

Theory : num_thy_1


Home Index