---

Step * 1 of Lemma length-shadow-vec


1. as : ℤ List
2. bs : ℤ List
3. i : ℕ||as||
4. ||as|| = ||bs|| ∈ ℤ
⊢ ||evalall(as[i] * bs + -bs[i] * as\i)|| = (||as|| - 1) ∈ ℤ
BY
{ ((RWO "evalall-reduce" 0 THEN Auto)
   THEN (RWO "length-list-delete" 0 THENA Auto)
   THEN RepeatFor 2 ((RWW "length-int-vec-add length-int-vec-mul" 0 THEN Auto))) }

---

Latex:

---

Latex:

1.  as  :  \mBbbZ{}  List
2.  bs  :  \mBbbZ{}  List
3.  i  :  \mBbbN{}||as||
4.  ||as||  =  ||bs||
\mvdash{}  ||evalall(as[i]  *  bs  +  -bs[i]  *  as\mbackslash{}i)||  =  (||as||  -  1)


By

---

Latex:
((RWO  "evalall-reduce"  0  THEN  Auto)
  THEN  (RWO  "length-list-delete"  0  THENA  Auto)
  THEN  RepeatFor  2  ((RWW  "length-int-vec-add  length-int-vec-mul"  0  THEN  Auto)))

---

Home Index