---

Step * of Lemma mul-list-insert-int

∀[ns:ℤ List]. ∀[x:ℤ].  (Π(insert-int(x;ns))  = (x * Π(ns) ) ∈ ℤ)
BY
{ (InductionOnList
   THEN Unfold `insert-int` 0
   THEN Reduce 0
   THEN Auto
   THEN Unfold `mul-list` 0
   THEN Reduce 0
   THEN (Try (Fold `mul-list` 0) THEN Try (Fold `insert-int` 0))
   THEN (CallByValueReduce 0 THENA Auto)) }

1
1. u : ℤ
2. v : ℤ List
3. ∀[x:ℤ]. (Π(insert-int(x;v))  = (x * Π(v) ) ∈ ℤ)
4. x : ℤ
⊢ Π(if x ≤z u then [x; [u / v]] else [u / insert-int(x;v)] fi )  = (x * u * Π(v) ) ∈ ℤ

---

Latex:

---

Latex:
\mforall{}[ns:\mBbbZ{}  List].  \mforall{}[x:\mBbbZ{}].    (\mPi{}(insert-int(x;ns))    =  (x  *  \mPi{}(ns)  ))


By

---

Latex:
(InductionOnList
  THEN  Unfold  `insert-int`  0
  THEN  Reduce  0
  THEN  Auto
  THEN  Unfold  `mul-list`  0
  THEN  Reduce  0
  THEN  (Try  (Fold  `mul-list`  0)  THEN  Try  (Fold  `insert-int`  0))
  THEN  (CallByValueReduce  0  THENA  Auto))

---

Home Index