Proof of Nuprl Lemma : rat_term

Step * of Lemma rat_term_polynomial

No Annotations
∀r:rat_term(). let p,q = rat_term_to_ipolys(r) in r ≡ ipolynomial-term(p)/ipolynomial-term(q)
BY
{ (BLemma `rat_term-induction`
   THEN Auto
   THEN Unfold `rat_term_to_ipolys` 0
   THEN Reduce 0
   THEN Try (Fold `rat_term_to_ipolys` 0)
   THEN Try (((RepeatFor 2 (MoveToConcl (-1))

               THEN ((GenConclTerms Auto [⌜rat_term_to_ipolys(left)⌝;⌜rat_term_to_ipolys(right)⌝]⋅

THEN DProdsAndUnions
THEN Reduce 0)

                    ORELSE (GenConclTerms Auto [⌜rat_term_to_ipolys(num)⌝;⌜rat_term_to_ipolys(denom)⌝]⋅

                            THEN DProdsAndUnions
                            THEN Reduce 0)
                    )
               )
             ORELSE (MoveToConcl (-1)
                     THEN GenConclTerms Auto [⌜rat_term_to_ipolys(num)⌝]⋅
                     THEN DProdsAndUnions
                     THEN Reduce 0)
             ))
   THEN Try ((Intros
              THEN RepeatFor 2 (ParallelLast')
              THEN Unfold `rat_term_to_real` 0
              THEN Reduce 0
              THEN Try (Fold `rat_term_to_real` 0)
              THEN MoveToConcl (-1)
              THEN Try (((D -2 With ⌜f⌝  THENA Auto) THEN MoveToConcl (-1)))

              THEN ((GenConclTerms Auto [⌜rat_term_to_real(f;right)⌝;⌜rat_term_to_real(f;left)⌝]⋅

THEN DProdsAndUnions
THEN Reduce 0)

              ORELSE (GenConclTerms Auto [⌜rat_term_to_real(f;num)⌝;⌜rat_term_to_real(f;denom)⌝]⋅

                      THEN DProdsAndUnions
                      THEN Reduce 0)
              )
              THEN RepeatFor 3 (Intro)
              THEN SplitAndHyps
              THEN ThinTrivial
              THEN SplitAndHyps))) }

1
1. const : ℤ
⊢ "const" ≡ ipolynomial-term(if const=0 then [] else [<const, []>])/ipolynomial-term([<1, []>])

2
1. var : ℤ
⊢ rtermVar(var) ≡ ipolynomial-term([<1, [var]>])/ipolynomial-term([<1, []>])

3
1. left : rat_term()
2. right : rat_term()
3. v4 : iPolynomial()
4. v5 : iPolynomial()
5. rat_term_to_ipolys(left) = <v4, v5> ∈ (iPolynomial() × iPolynomial())
6. v2 : iPolynomial()
7. v3 : iPolynomial()
8. rat_term_to_ipolys(right) = <v2, v3> ∈ (iPolynomial() × iPolynomial())
9. f : ℤ ⟶ ℝ
10. P1 : ℙ
11. v8 : ℝ supposing P1
12. rat_term_to_real(f;right) = <P1, v8> ∈ (P:ℙ × ℝ supposing P)
13. P : ℙ
14. v7 : ⋂:P. ℝ
15. rat_term_to_real(f;left) = <P, v7> ∈ (P:ℙ × ℝ supposing P)
16. P
17. P1
18. real_term_value(f;ipolynomial-term(v3)) ≠ r0
19. v8 = (real_term_value(f;ipolynomial-term(v2))/real_term_value(f;ipolynomial-term(v3)))
20. real_term_value(f;ipolynomial-term(v5)) ≠ r0
21. v7 = (real_term_value(f;ipolynomial-term(v4))/real_term_value(f;ipolynomial-term(v5)))
22. ℝ
⊢ real_term_value(f;ipolynomial-term(mul_ipoly(v5;v3))) ≠ r0
∧ ((v7 + v8)
  = (real_term_value(f;ipolynomial-term(add_ipoly(mul_ipoly(v4;v3);mul_ipoly(v2;v5))))/real_term_value(f;...)))

4
1. left : rat_term()
2. right : rat_term()
3. v4 : iPolynomial()
4. v5 : iPolynomial()
5. rat_term_to_ipolys(left) = <v4, v5> ∈ (iPolynomial() × iPolynomial())
6. v2 : iPolynomial()
7. v3 : iPolynomial()
8. rat_term_to_ipolys(right) = <v2, v3> ∈ (iPolynomial() × iPolynomial())
9. f : ℤ ⟶ ℝ
10. P1 : ℙ
11. v8 : ℝ supposing P1
12. rat_term_to_real(f;right) = <P1, v8> ∈ (P:ℙ × ℝ supposing P)
13. P : ℙ
14. v7 : ⋂:P. ℝ
15. rat_term_to_real(f;left) = <P, v7> ∈ (P:ℙ × ℝ supposing P)
16. P
17. P1
18. real_term_value(f;ipolynomial-term(v3)) ≠ r0
19. v8 = (real_term_value(f;ipolynomial-term(v2))/real_term_value(f;ipolynomial-term(v3)))
20. real_term_value(f;ipolynomial-term(v5)) ≠ r0
21. v7 = (real_term_value(f;ipolynomial-term(v4))/real_term_value(f;ipolynomial-term(v5)))
22. ℝ
⊢ real_term_value(f;ipolynomial-term(mul_ipoly(v5;v3))) ≠ r0
∧ ((v7 - v8)
  = (real_term_value(f;ipolynomial-term(add_ipoly(mul_ipoly(v4;v3);mul_ipoly(minus-poly(v2);v5))))/...))

5
1. left : rat_term()
2. right : rat_term()
3. v4 : iPolynomial()
4. v5 : iPolynomial()
5. rat_term_to_ipolys(left) = <v4, v5> ∈ (iPolynomial() × iPolynomial())
6. v2 : iPolynomial()
7. v3 : iPolynomial()
8. rat_term_to_ipolys(right) = <v2, v3> ∈ (iPolynomial() × iPolynomial())
9. f : ℤ ⟶ ℝ
10. P1 : ℙ
11. v8 : ℝ supposing P1
12. rat_term_to_real(f;right) = <P1, v8> ∈ (P:ℙ × ℝ supposing P)
13. P : ℙ
14. v7 : ⋂:P. ℝ
15. rat_term_to_real(f;left) = <P, v7> ∈ (P:ℙ × ℝ supposing P)
16. P
17. P1
18. real_term_value(f;ipolynomial-term(v3)) ≠ r0
19. v8 = (real_term_value(f;ipolynomial-term(v2))/real_term_value(f;ipolynomial-term(v3)))
20. real_term_value(f;ipolynomial-term(v5)) ≠ r0
21. v7 = (real_term_value(f;ipolynomial-term(v4))/real_term_value(f;ipolynomial-term(v5)))
22. ℝ
⊢ real_term_value(f;ipolynomial-term(mul_ipoly(v5;v3))) ≠ r0
∧ ((v7 * v8)
  = (real_term_value(f;ipolynomial-term(mul_ipoly(v4;v2)))/real_term_value(f;ipolynomial-term(mul_ipoly(v5;v3)))))

6
1. num : rat_term()
2. denom : rat_term()
3. v4 : iPolynomial()
4. v5 : iPolynomial()
5. rat_term_to_ipolys(num) = <v4, v5> ∈ (iPolynomial() × iPolynomial())
6. v2 : iPolynomial()
7. v3 : iPolynomial()
8. rat_term_to_ipolys(denom) = <v2, v3> ∈ (iPolynomial() × iPolynomial())
9. f : ℤ ⟶ ℝ
10. P1 : ℙ
11. v8 : ℝ supposing P1
12. rat_term_to_real(f;num) = <P1, v8> ∈ (P:ℙ × ℝ supposing P)
13. P : ℙ
14. v7 : ⋂:P. ℝ
15. rat_term_to_real(f;denom) = <P, v7> ∈ (P:ℙ × ℝ supposing P)
16. P1
17. P
18. v7 ≠ r0
19. real_term_value(f;ipolynomial-term(v3)) ≠ r0
20. v7 = (real_term_value(f;ipolynomial-term(v2))/real_term_value(f;ipolynomial-term(v3)))
21. real_term_value(f;ipolynomial-term(v5)) ≠ r0
22. v8 = (real_term_value(f;ipolynomial-term(v4))/real_term_value(f;ipolynomial-term(v5)))
23. ℝ
⊢ real_term_value(f;ipolynomial-term(mul_ipoly(v5;v2))) ≠ r0
∧ ((v8/v7)
  = (real_term_value(f;ipolynomial-term(mul_ipoly(v4;v3)))/real_term_value(f;ipolynomial-term(mul_ipoly(v5;v2)))))

7
1. num : rat_term()
2. v1 : iPolynomial()
3. v2 : iPolynomial()
4. rat_term_to_ipolys(num) = <v1, v2> ∈ (iPolynomial() × iPolynomial())
⊢ num ≡ ipolynomial-term(v1)/ipolynomial-term(v2)
⇒ rtermMinus(num) ≡ ipolynomial-term(minus-poly(v1))/ipolynomial-term(v2)

Latex:

Latex:
No Annotations \mforall{}r:rat\_term(). let p,q = rat\_term\_to\_ipolys(r) in r \mequiv{} ipolynomial-term(p)/ipolynomial-term(q) By Latex: (BLemma `rat\_term-induction` THEN Auto THEN Unfold `rat\_term\_to\_ipolys` 0 THEN Reduce 0 THEN Try (Fold `rat\_term\_to\_ipolys` 0) THEN Try (((RepeatFor 2 (MoveToConcl (-1)) THEN ((GenConclTerms Auto [\mkleeneopen{}rat\_term\_to\_ipolys(left)\mkleeneclose{};\mkleeneopen{}rat\_term\_to\_ipolys(right)\mkleeneclose{}]\mcdot{} THEN DProdsAndUnions THEN Reduce 0) ORELSE (GenConclTerms Auto [\mkleeneopen{}rat\_term\_to\_ipolys(num)\mkleeneclose{};\mkleeneopen{}rat\_term\_to\_ipolys(denom)\mkleeneclose{}] \mcdot{} THEN DProdsAndUnions THEN Reduce 0) ) ) ORELSE (MoveToConcl (-1) THEN GenConclTerms Auto [\mkleeneopen{}rat\_term\_to\_ipolys(num)\mkleeneclose{}]\mcdot{} THEN DProdsAndUnions THEN Reduce 0) )) THEN Try ((Intros THEN RepeatFor 2 (ParallelLast') THEN Unfold `rat\_term\_to\_real` 0 THEN Reduce 0 THEN Try (Fold `rat\_term\_to\_real` 0) THEN MoveToConcl (-1) THEN Try (((D -2 With \mkleeneopen{}f\mkleeneclose{} THENA Auto) THEN MoveToConcl (-1))) THEN ((GenConclTerms Auto [\mkleeneopen{}rat\_term\_to\_real(f;right)\mkleeneclose{};\mkleeneopen{}rat\_term\_to\_real(f;left)\mkleeneclose{}]\mcdot{} THEN DProdsAndUnions THEN Reduce 0) ORELSE (GenConclTerms Auto [\mkleeneopen{}rat\_term\_to\_real(f;num)\mkleeneclose{};\mkleeneopen{}rat\_term\_to\_real(f;denom)\mkleeneclose{}]\mcdot{} THEN DProdsAndUnions THEN Reduce 0) ) THEN RepeatFor 3 (Intro) THEN SplitAndHyps THEN ThinTrivial THEN SplitAndHyps))) Home Index