---

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


1. u : ℤ
2. v1 : ℤ
3. v2 : ℤ
4. v3 : ℤ
5. v4 : ℤ
⊢ eval av = v3 + v4 in
  eval bv = v1 + v2 in
    if bv=0 then av else eval h = u in av + (h * bv)
= (eval av = v3 in
   eval bv = v1 in
     if bv=0 then av else eval h = u in av + (h * bv)
  + eval av = v4 in
    eval bv = v2 in
      if bv=0 then av else eval h = u in av + (h * bv))
∈ ℤ
BY
{ (RepeatFor 3 ((CallByValueReduce 0⋅ THENA Auto)) THEN Auto) }

1
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)))
∈ ℤ

---

Latex:

---

Latex:

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


By

---

Latex:
(RepeatFor  3  ((CallByValueReduce  0\mcdot{}  THENA  Auto))  THEN  Auto)

---

Home Index