---

Step * of 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 )
BY
{ xxx((Auto THEN Unfold `int-prod` 0)
      THEN (RW (AddrC [1] (LemmaC `primrec-unroll`)) 0 THENA Auto)
      THEN Fold `int-prod` 0
      THEN Reduce 0
      THEN Auto)xxx }

---

Latex:

---

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  )


By

---

Latex:
xxx((Auto  THEN  Unfold  `int-prod`  0)
        THEN  (RW  (AddrC  [1]  (LemmaC  `primrec-unroll`))  0  THENA  Auto)
        THEN  Fold  `int-prod`  0
        THEN  Reduce  0
        THEN  Auto)xxx

---

Home Index