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