### Nuprl Lemma : int-prod-unroll-hi

`∀[n:ℕ]. ∀[f:Top].  (Π(f[x] | x < n) ~ if (n =z 0) then 1 else Π(f[x] | x < n - 1) * f[n - 1] fi )`

Proof

Definitions occuring in Statement :  int-prod: `Π(f[x] | x < k)` nat: `ℕ` ifthenelse: `if b then t else f fi ` eq_int: `(i =z j)` uall: `∀[x:A]. B[x]` top: `Top` so_apply: `x[s]` multiply: `n * m` subtract: `n - m` natural_number: `\$n` sqequal: `s ~ t`
Definitions unfolded in proof :  top: `Top` int-prod: `Π(f[x] | x < k)` member: `t ∈ T` uall: `∀[x:A]. B[x]`
Lemmas referenced :  nat_wf top_wf primrec-unroll
Rules used in proof :  hypothesisEquality sqequalAxiom hypothesis voidEquality voidElimination isect_memberEquality because_Cache thin isectElimination sqequalHypSubstitution extract_by_obid sqequalRule cut introduction isect_memberFormation sqequalReflexivity computationStep sqequalTransitivity sqequalSubstitution

Latex:
\mforall{}[n:\mBbbN{}].  \mforall{}[f:Top].    (\mPi{}(f[x]  |  x  <  n)  \msim{}  if  (n  =\msubz{}  0)  then  1  else  \mPi{}(f[x]  |  x  <  n  -  1)  *  f[n  -  1]  fi  )

Date html generated: 2018_05_21-PM-00_28_51
Last ObjectModification: 2017_12_10-PM-10_13_43

Theory : int_2

Home Index