---

Step * 2 1 1 of Lemma rP_to_poly-int_term_to_rP

.....assertion..... 
1. int_term() ⊆r Base
2. (iPolynomial() List) ⊆r Base
⊢ ∀t:int_term(). ∀s:iPolynomial() List. ∀L:ℤ List.
    (rP_to_poly(s;int_term_to_rP(t) @ L) ~ rP_to_poly([int_term_to_ipoly(t) / s];L))
BY
{ ((BLemma `int_term-induction` THENA Auto)
   THEN Intros
   THEN RepUR ``int_term_to_rP int_term_to_ipoly`` 0
   THEN ((Folds ``int_term_to_rP int_term_to_ipoly`` 0
          THEN (RWW "eager-append-is-append append_assoc -3 -4" 0 THENA Auto)
          THEN (RW (AddrC [1] RecUnfoldTopAbC) 0 THEN Reduce 0)
          THEN Auto)
   ORELSE ((RW (AddrC [1] RecUnfoldTopAbC) 0 THEN Reduce 0) THEN Fold `cons` 0 THEN Auto)
   )) }

---

Latex:

---

Latex:
.....assertion..... 
1.  int\_term()  \msubseteq{}r  Base
2.  (iPolynomial()  List)  \msubseteq{}r  Base
\mvdash{}  \mforall{}t:int\_term().  \mforall{}s:iPolynomial()  List.  \mforall{}L:\mBbbZ{}  List.
        (rP\_to\_poly(s;int\_term\_to\_rP(t)  @  L)  \msim{}  rP\_to\_poly([int\_term\_to\_ipoly(t)  /  s];L))


By

---

Latex:
((BLemma  `int\_term-induction`  THENA  Auto)
  THEN  Intros
  THEN  RepUR  ``int\_term\_to\_rP  int\_term\_to\_ipoly``  0
  THEN  ((Folds  ``int\_term\_to\_rP  int\_term\_to\_ipoly``  0
                THEN  (RWW  "eager-append-is-append  append\_assoc  -3  -4"  0  THENA  Auto)
                THEN  (RW  (AddrC  [1]  RecUnfoldTopAbC)  0  THEN  Reduce  0)
                THEN  Auto)
  ORELSE  ((RW  (AddrC  [1]  RecUnfoldTopAbC)  0  THEN  Reduce  0)  THEN  Fold  `cons`  0  THEN  Auto)
  ))

---

Home Index