---

Step * 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])
⊢ 0 ≤ shadow-vec(i;as;bs) ⋅ xs\i
BY
{ (Mul ⌜(-1) * bs[i]⌝ (-3)⋅
   THEN (RWO "int-dot-mul-left<" (-1) THENA Auto)
   THEN (RW IntNormC (-1) THENA Auto)
   THEN (Mul ⌜as[i]⌝ (-3)⋅ THENA (MemTypeCD THEN Auto))
   THEN (RWO "int-dot-mul-left<" (-1) THENA Auto)
   THEN (RW IntNormC (-1) 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
⊢ 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])
\mvdash{}  0  \mleq{}  shadow-vec(i;as;bs)  \mcdot{}  xs\mbackslash{}i


By

---

Latex:
(Mul  \mkleeneopen{}(-1)  *  bs[i]\mkleeneclose{}  (-3)\mcdot{}
  THEN  (RWO  "int-dot-mul-left<"  (-1)  THENA  Auto)
  THEN  (RW  IntNormC  (-1)  THENA  Auto)
  THEN  (Mul  \mkleeneopen{}as[i]\mkleeneclose{}  (-3)\mcdot{}  THENA  (MemTypeCD  THEN  Auto))
  THEN  (RWO  "int-dot-mul-left<"  (-1)  THENA  Auto)
  THEN  (RW  IntNormC  (-1)  THENA  Auto))

---

Home Index