Step
*
3
of Lemma
rat_term_to_ipolys_wf
.....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()
BY
{ (CaseNat 0 `c' THEN Reduce 0) }
1
1. t : rat_term()
2. <1, []> ∈ iMonomial()
3. [<1, []>] ∈ iPolynomial()
4. c : ℤ
5. c = 0 ∈ ℤ
⊢ <[], [<1, []>]> ∈ iPolynomial() × iPolynomial()
2
1. t : rat_term()
2. <1, []> ∈ iMonomial()
3. [<1, []>] ∈ iPolynomial()
4. c : ℤ
5. ¬(c = 0 ∈ ℤ)
⊢ <[<c, []>], [<1, []>]> ∈ iPolynomial() × iPolynomial()
Latex:
Latex:
.....subterm..... T:t
2:n
1. t : rat\_term()
2. ə, []> \mmember{} iMonomial()
3. [ə, []>] \mmember{} iPolynomial()
4. c : \mBbbZ{}
\mvdash{} <if c=0 then [] else [<c, []>], [ə, []>]> \mmember{} iPolynomial() \mtimes{} iPolynomial()
By
Latex:
(CaseNat 0 `c' THEN Reduce 0)
Home
Index