---

Step * of Lemma rat_term_to_ipolys_wf

∀[t:rat_term()]. (rat_term_to_ipolys(t) ∈ iPolynomial() × iPolynomial())
BY
{ (Intro
   THEN ((Assert <1, []> ∈ iMonomial() BY
                (Unfold `iMonomial` 0 THEN Auto THEN MemTypeCD THEN Auto THEN (D 0 THEN Reduce 0) THEN Auto))
         THEN (Assert [<1, []>] ∈ iPolynomial() BY
                     (MemTypeCD THEN Auto THEN All Reduce THEN Auto))
         )
   THEN Unfold `rat_term_to_ipolys` 0
   THEN (MemCD THENW Auto)
   THEN Try (((DProdsAndUnions THEN Reduce 0) THEN Auto))) }

1
.....implicit subterm..... 
1. t : rat_term()
2. <1, []> ∈ iMonomial()
3. [<1, []>] ∈ iPolynomial()
⊢ iPolynomial() × iPolynomial() ∈ Type

2
.....subterm..... T:t
1:n
1. t : rat_term()
2. <1, []> ∈ iMonomial()
3. [<1, []>] ∈ iPolynomial()
⊢ t ∈ rat_term()

3
.....subterm..... T:t
2:n
1. t : rat_term()
2. <1, []> ∈ iMonomial()
3. [<1, []>] ∈ iPolynomial()
4. c : ℤ
⊢ <if c=0 then [] else [<c, []>], [<1, []>]> ∈ iPolynomial() × iPolynomial()

4
.....subterm..... T:t
3:n
1. t : rat_term()
2. <1, []> ∈ iMonomial()
3. [<1, []>] ∈ iPolynomial()
4. v : ℤ
⊢ <[<1, [v]>], [<1, []>]> ∈ iPolynomial() × iPolynomial()

---

Latex:

---

Latex:
\mforall{}[t:rat\_term()].  (rat\_term\_to\_ipolys(t)  \mmember{}  iPolynomial()  \mtimes{}  iPolynomial())


By

---

Latex:
(Intro
  THEN  ((Assert  ə,  []>  \mmember{}  iMonomial()  BY
                            (Unfold  `iMonomial`  0
                              THEN  Auto
                              THEN  MemTypeCD
                              THEN  Auto
                              THEN  (D  0  THEN  Reduce  0)
                              THEN  Auto))
              THEN  (Assert  [ə,  []>]  \mmember{}  iPolynomial()  BY
                                      (MemTypeCD  THEN  Auto  THEN  All  Reduce  THEN  Auto))
              )
  THEN  Unfold  `rat\_term\_to\_ipolys`  0
  THEN  (MemCD  THENW  Auto)
  THEN  Try  (((DProdsAndUnions  THEN  Reduce  0)  THEN  Auto)))

---

Home Index