---

Step * 2 2 1 1 of Lemma add-poly-prepend-sq1


1. u2 : ℤ
2. u3 : ℤ List
3. v : (ℤ × (ℤ List)) List
4. ∀[q,l:(ℤ × (ℤ List)) List].  (add-ipoly-prepend(v;q;l) ~ rev(l) + add-ipoly(v;q))
5. u4 : ℤ
6. u5 : ℤ List
7. v1 : (ℤ × (ℤ List)) List
8. ∀[l:(ℤ × (ℤ List)) List]. (add-ipoly-prepend([<u2, u3> / v];v1;l) ~ rev(l) + add-ipoly([<u2, u3> / v];v1))
9. l : (ℤ × (ℤ List)) List
10. ∀u,u':ℤ × (ℤ List).  (imonomial-le(u;u') ∈ 𝔹)
11. ∀p,q:(ℤ × (ℤ List)) List.  (add-ipoly(p;q) ∈ (ℤ × (ℤ List)) List)
12. ↑imonomial-le(<u2, u3>;<u4, u5>)
13. ↑imonomial-le(<u4, u5>;<u2, u3>)
14. add-ipoly(v;v1) ∈ (ℤ × (ℤ List)) List
⊢ add-ipoly-prepend(v;v1;if u2 + u4=0  then l  else [<u2 + u4, u3> / l]) ~ rev(l) + if u2 + u4=0
                                                                                       then add-ipoly(v;v1)
                                                                                       else [<u2 + u4, u3> / 
                                                                                             add-ipoly(v;v1)]
BY
{ ((RWO "4" 0 THENA Auto) THEN Decide ⌜(u2 + u4) = 0 ∈ ℤ⌝⋅ THEN Reduce 0 THEN Auto) }

---

Latex:

---

Latex:

1.  u2  :  \mBbbZ{}
2.  u3  :  \mBbbZ{}  List
3.  v  :  (\mBbbZ{}  \mtimes{}  (\mBbbZ{}  List))  List
4.  \mforall{}[q,l:(\mBbbZ{}  \mtimes{}  (\mBbbZ{}  List))  List].    (add-ipoly-prepend(v;q;l)  \msim{}  rev(l)  +  add-ipoly(v;q))
5.  u4  :  \mBbbZ{}
6.  u5  :  \mBbbZ{}  List
7.  v1  :  (\mBbbZ{}  \mtimes{}  (\mBbbZ{}  List))  List
8.  \mforall{}[l:(\mBbbZ{}  \mtimes{}  (\mBbbZ{}  List))  List]
          (add-ipoly-prepend([<u2,  u3>  /  v];v1;l)  \msim{}  rev(l)  +  add-ipoly([<u2,  u3>  /  v];v1))
9.  l  :  (\mBbbZ{}  \mtimes{}  (\mBbbZ{}  List))  List
10.  \mforall{}u,u':\mBbbZ{}  \mtimes{}  (\mBbbZ{}  List).    (imonomial-le(u;u')  \mmember{}  \mBbbB{})
11.  \mforall{}p,q:(\mBbbZ{}  \mtimes{}  (\mBbbZ{}  List))  List.    (add-ipoly(p;q)  \mmember{}  (\mBbbZ{}  \mtimes{}  (\mBbbZ{}  List))  List)
12.  \muparrow{}imonomial-le(<u2,  u3><u4,  u5>)
13.  \muparrow{}imonomial-le(<u4,  u5><u2,  u3>)
14.  add-ipoly(v;v1)  \mmember{}  (\mBbbZ{}  \mtimes{}  (\mBbbZ{}  List))  List
\mvdash{}  add-ipoly-prepend(v;v1;if  u2  +  u4=0    then  l    else  [<u2  +  u4,  u3>  /  l]) 
\msim{}  rev(l)  +  if  u2  +  u4=0    then  add-ipoly(v;v1)    else  [<u2  +  u4,  u3>  /  add-ipoly(v;v1)]


By

---

Latex:
((RWO  "4"  0  THENA  Auto)  THEN  Decide  \mkleeneopen{}(u2  +  u4)  =  0\mkleeneclose{}\mcdot{}  THEN  Reduce  0  THEN  Auto)

---

Home Index