---

Step * of Lemma length-shadow-vec

∀[as,bs:ℤ List]. ∀[i:ℕ||as||].  ||shadow-vec(i;as;bs)|| = (||as|| - 1) ∈ ℤ supposing ||as|| = ||bs|| ∈ ℤ
BY
{ (Auto
   THEN Unfold `shadow-vec` 0
   THEN RepeatFor 3
   (((RW  (AddrC [2;1;1] (LemmaC `evalall-reduce`)) 0 THEN Auto) THEN (CallByValueReduce 0 THENA Auto)))) }

1
1. as : ℤ List
2. bs : ℤ List
3. i : ℕ||as||
4. ||as|| = ||bs|| ∈ ℤ
⊢ ||evalall(as[i] * bs + -bs[i] * as\i)|| = (||as|| - 1) ∈ ℤ

---

Latex:

---

Latex:
\mforall{}[as,bs:\mBbbZ{}  List].  \mforall{}[i:\mBbbN{}||as||].    ||shadow-vec(i;as;bs)||  =  (||as||  -  1)  supposing  ||as||  =  ||bs||


By

---

Latex:
(Auto
  THEN  Unfold  `shadow-vec`  0
  THEN  RepeatFor  3  (((RW    (AddrC  [2;1;1]  (LemmaC  `evalall-reduce`))  0  THEN  Auto)
                                        THEN  (CallByValueReduce  0  THENA  Auto)
                                        )))

---

Home Index