---

Step * 2 1 of Lemma mul-initial-seg-step


1. L : ℕ List
2. x : ℕ
⊢ reduce(λx,y. (x * y);1;L @ [x]) = (reduce(λx,y. (x * y);1;L) * x) ∈ ℤ
BY
{ (MoveToConcl (-1) THEN ListInd 1 THEN Reduce 0 THEN Auto)⋅ }

---

Latex:

---

Latex:

1.  L  :  \mBbbN{}  List
2.  x  :  \mBbbN{}
\mvdash{}  reduce(\mlambda{}x,y.  (x  *  y);1;L  @  [x])  =  (reduce(\mlambda{}x,y.  (x  *  y);1;L)  *  x)


By

---

Latex:
(MoveToConcl  (-1)  THEN  ListInd  1  THEN  Reduce  0  THEN  Auto)\mcdot{}

---

Home Index