---

Step * of Lemma shadow-vec-property

No Annotations
∀[as,bs:ℤ List]. ∀[i:ℕ||as||].
  (∀[xs:ℤ List]
     0 ≤ shadow-vec(i;as;bs) ⋅ xs\i supposing (||xs|| = ||as|| ∈ ℤ) ∧ (0 ≤ as ⋅ xs) ∧ (0 ≤ bs ⋅ xs)) supposing 
     ((bs[i] ≤ 0) and 
     (0 ≤ as[i]) and 
     (||as|| = ||bs|| ∈ ℤ))
BY
{ (Auto THEN Add ⌜-bs[i]⌝ (-5)⋅ 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])
⊢ 0 ≤ shadow-vec(i;as;bs) ⋅ xs\i

---

Latex:

---

Latex:
No  Annotations
\mforall{}[as,bs:\mBbbZ{}  List].  \mforall{}[i:\mBbbN{}||as||].
    (\mforall{}[xs:\mBbbZ{}  List]
          0  \mleq{}  shadow-vec(i;as;bs)  \mcdot{}  xs\mbackslash{}i 
          supposing  (||xs||  =  ||as||)  \mwedge{}  (0  \mleq{}  as  \mcdot{}  xs)  \mwedge{}  (0  \mleq{}  bs  \mcdot{}  xs))  supposing 
          ((bs[i]  \mleq{}  0)  and 
          (0  \mleq{}  as[i])  and 
          (||as||  =  ||bs||))


By

---

Latex:
(Auto  THEN  Add  \mkleeneopen{}-bs[i]\mkleeneclose{}  (-5)\mcdot{}  THEN  (RW    IntNormC  (-1)  THENA  Auto))

---

Home Index