---

Step * 2 of Lemma int-prod-split


1. n : ℤ
2. 0 < n
3. ∀[f:ℕn - 1 ⟶ ℤ]. ∀[m:ℕ(n - 1) + 1].  (Π(f[x] | x < n - 1) = (Π(f[x] | x < m) * Π(f[x + m] | x < n - 1 - m)) ∈ ℤ)
4. f : ℕn ⟶ ℤ
5. m : ℕn + 1
⊢ Π(f[x] | x < n) = (Π(f[x] | x < m) * Π(f[x + m] | x < n - m)) ∈ ℤ
BY
{ (((RW (AddrC [3;2] UnfoldTopAbC) 0 THEN RW (AddrC [2] UnfoldTopAbC) 0) THEN (RWO "primrec-unroll" 0 THENA Auto))
   THEN Reduce 0
   THEN (OReduce 0 THENA Auto)
   THEN Fold `int-prod` 0) }

1
1. n : ℤ
2. 0 < n
3. ∀[f:ℕn - 1 ⟶ ℤ]. ∀[m:ℕ(n - 1) + 1].  (Π(f[x] | x < n - 1) = (Π(f[x] | x < m) * Π(f[x + m] | x < n - 1 - m)) ∈ ℤ)
4. f : ℕn ⟶ ℤ
5. m : ℕn + 1
⊢ (Π(f[x] | x < n - 1) * f[n - 1])
= (Π(f[x] | x < m) * if n - m <z 1 then 1 else Π(f[x + m] | x < n - m - 1) * f[(n - m - 1) + m] fi )
∈ ℤ

---

Latex:

---

Latex:

1.  n  :  \mBbbZ{}
2.  0  <  n
3.  \mforall{}[f:\mBbbN{}n  -  1  {}\mrightarrow{}  \mBbbZ{}].  \mforall{}[m:\mBbbN{}(n  -  1)  +  1].
          (\mPi{}(f[x]  |  x  <  n  -  1)  =  (\mPi{}(f[x]  |  x  <  m)  *  \mPi{}(f[x  +  m]  |  x  <  n  -  1  -  m)))
4.  f  :  \mBbbN{}n  {}\mrightarrow{}  \mBbbZ{}
5.  m  :  \mBbbN{}n  +  1
\mvdash{}  \mPi{}(f[x]  |  x  <  n)  =  (\mPi{}(f[x]  |  x  <  m)  *  \mPi{}(f[x  +  m]  |  x  <  n  -  m))


By

---

Latex:
(((RW  (AddrC  [3;2]  UnfoldTopAbC)  0  THEN  RW  (AddrC  [2]  UnfoldTopAbC)  0)
    THEN  (RWO  "primrec-unroll"  0  THENA  Auto)
    )
  THEN  Reduce  0
  THEN  (OReduce  0  THENA  Auto)
  THEN  Fold  `int-prod`  0)

---

Home Index