---

Step * 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
⊢ 0 ≤ shadow-vec(i;as;bs) ⋅ xs\i
BY
{ (Assert 0 ≤ (as[i] * bs ⋅ xs + (-1) * bs[i] * as ⋅ xs) BY
         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 ⋅ xs + (-1) * bs[i] * as ⋅ xs)
⊢ 0 ≤ shadow-vec(i;as;bs) ⋅ 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
\mvdash{}  0  \mleq{}  shadow-vec(i;as;bs)  \mcdot{}  xs\mbackslash{}i


By

---

Latex:
(Assert  0  \mleq{}  (as[i]  *  bs  \mcdot{}  xs  +  (-1)  *  bs[i]  *  as  \mcdot{}  xs)  BY
              Auto)

---

Home Index