---

Step * 4 1 1 1 1 1 1 of Lemma add-polynom-val


1. u : ℤ
2. v1 : ℤ
3. v2 : ℤ
4. v3 : ℤ
5. v4 : ℤ
⊢ if v1 + v2=0 then v3 + v4 else ((v3 + v4) + (u * (v1 + v2)))
= (if v1=0 then v3 else (v3 + (u * v1)) + if v2=0 then v4 else (v4 + (u * v2)))
∈ ℤ
BY
{ (((Decide ⌜v1 = 0 ∈ ℤ⌝⋅ THENA Auto) THEN Reduce 0)
   THEN ((Decide ⌜v2 = 0 ∈ ℤ⌝⋅ THENA Auto) THEN Reduce 0)
   THEN (Decide ⌜(v1 + v2) = 0 ∈ ℤ⌝⋅ THENA Auto)
   THEN Reduce 0
   THEN Auto) }

1
1. u : ℤ
2. v1 : ℤ
3. v2 : ℤ
4. v3 : ℤ
5. v4 : ℤ
6. ¬(v1 = 0 ∈ ℤ)
7. ¬(v2 = 0 ∈ ℤ)
8. (v1 + v2) = 0 ∈ ℤ
⊢ (v3 + v4) = ((v3 + (u * v1)) + v4 + (u * v2)) ∈ ℤ

---

Latex:

---

Latex:

1.  u  :  \mBbbZ{}
2.  v1  :  \mBbbZ{}
3.  v2  :  \mBbbZ{}
4.  v3  :  \mBbbZ{}
5.  v4  :  \mBbbZ{}
\mvdash{}  if  v1  +  v2=0  then  v3  +  v4  else  ((v3  +  v4)  +  (u  *  (v1  +  v2)))
=  (if  v1=0  then  v3  else  (v3  +  (u  *  v1))  +  if  v2=0  then  v4  else  (v4  +  (u  *  v2)))


By

---

Latex:
(((Decide  \mkleeneopen{}v1  =  0\mkleeneclose{}\mcdot{}  THENA  Auto)  THEN  Reduce  0)
  THEN  ((Decide  \mkleeneopen{}v2  =  0\mkleeneclose{}\mcdot{}  THENA  Auto)  THEN  Reduce  0)
  THEN  (Decide  \mkleeneopen{}(v1  +  v2)  =  0\mkleeneclose{}\mcdot{}  THENA  Auto)
  THEN  Reduce  0
  THEN  Auto)

---

Home Index