---

Step * 1 1 1 1 of Lemma shadow-vec-property


1. as : ℤ List
2. bs : ℤ List
3. i : ℕ||as||
4. ||as|| = ||bs|| ∈ ℤ
5. 0 ≤ as[i]
6. bs[i] ≤ 0
7. xs : ℤ List
8. ||xs|| = ||as|| ∈ ℤ
9. 0 ≤ as ⋅ xs
10. 0 ≤ bs ⋅ xs
11. 0 ≤ ((-1) * bs[i])
12. 0 ≤ (-1) * bs[i] * as ⋅ xs
13. 0 ≤ as[i] * bs ⋅ xs
14. 0 ≤ as[i] * bs + (-1) * bs[i] * as ⋅ xs
⊢ 0 ≤ shadow-vec(i;as;bs) ⋅ xs\i
BY
{ ((Assert valueall-type(ℤ List) BY
          Auto)
   THEN Unfold `shadow-vec` 0
   THEN RepeatFor 3 (((RW (AddrC [2;1;1] (LemmaC `evalall-reduce`)) 0 THENA Auto)
                      THEN Try (Trivial)
                      THEN (CallByValueReduce 0 THENA Auto)))) }

1
1. as : ℤ List
2. bs : ℤ List
3. i : ℕ||as||
4. ||as|| = ||bs|| ∈ ℤ
5. 0 ≤ as[i]
6. bs[i] ≤ 0
7. xs : ℤ List
8. ||xs|| = ||as|| ∈ ℤ
9. 0 ≤ as ⋅ xs
10. 0 ≤ bs ⋅ xs
11. 0 ≤ ((-1) * bs[i])
12. 0 ≤ (-1) * bs[i] * as ⋅ xs
13. 0 ≤ as[i] * bs ⋅ xs
14. 0 ≤ as[i] * bs + (-1) * bs[i] * as ⋅ xs
15. valueall-type(ℤ List)
⊢ 0 ≤ evalall(as[i] * bs + -bs[i] * as\i) ⋅ xs\i

---

Latex:

---

Latex:

1.  as  :  \mBbbZ{}  List
2.  bs  :  \mBbbZ{}  List
3.  i  :  \mBbbN{}||as||
4.  ||as||  =  ||bs||
5.  0  \mleq{}  as[i]
6.  bs[i]  \mleq{}  0
7.  xs  :  \mBbbZ{}  List
8.  ||xs||  =  ||as||
9.  0  \mleq{}  as  \mcdot{}  xs
10.  0  \mleq{}  bs  \mcdot{}  xs
11.  0  \mleq{}  ((-1)  *  bs[i])
12.  0  \mleq{}  (-1)  *  bs[i]  *  as  \mcdot{}  xs
13.  0  \mleq{}  as[i]  *  bs  \mcdot{}  xs
14.  0  \mleq{}  as[i]  *  bs  +  (-1)  *  bs[i]  *  as  \mcdot{}  xs
\mvdash{}  0  \mleq{}  shadow-vec(i;as;bs)  \mcdot{}  xs\mbackslash{}i


By

---

Latex:
((Assert  valueall-type(\mBbbZ{}  List)  BY
                Auto)
  THEN  Unfold  `shadow-vec`  0
  THEN  RepeatFor  3  (((RW  (AddrC  [2;1;1]  (LemmaC  `evalall-reduce`))  0  THENA  Auto)
                                        THEN  Try  (Trivial)
                                        THEN  (CallByValueReduce  0  THENA  Auto))))

---

Home Index