---

Step * 1 of Lemma mul-list-insert-int


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) ) ∈ ℤ
BY
{ xxx(AutoSplit THEN Unfold `mul-list` 0⋅ THEN Reduce 0 THEN Fold `mul-list` 0 THEN Auto)xxx }

---

Latex:

---

Latex:

1.  u  :  \mBbbZ{}
2.  v  :  \mBbbZ{}  List
3.  \mforall{}[x:\mBbbZ{}].  (\mPi{}(insert-int(x;v))    =  (x  *  \mPi{}(v)  ))
4.  x  :  \mBbbZ{}
\mvdash{}  \mPi{}(if  x  \mleq{}z  u  then  [x;  [u  /  v]]  else  [u  /  insert-int(x;v)]  fi  )    =  (x  *  u  *  \mPi{}(v)  )


By

---

Latex:
xxx(AutoSplit  THEN  Unfold  `mul-list`  0\mcdot{}  THEN  Reduce  0  THEN  Fold  `mul-list`  0  THEN  Auto)xxx

---

Home Index