the rational function

$$W(x)=\frac{Z(x)-1}{Z(x)+1}=\frac{\operatorname{num}(Z)(x)-\operatorname{denom}(Z)(x)}{\operatorname{num}(Z)(x)+\operatorname{denom}(Z)(x)}.\tag{8}$$

and to analyze the absolute values |W(x)|. If Z(x) is positive, then |W(x)| ≤ 1 for all x with ℜ(x) ≥ 0, which implies that W(x) has no poles for ℜ(x) ≥ **0. Thus** the denominator polynomial can have roots only for ℜ(x) < 0, so num(Z)(x) + denom(Z)(x**) is a Hurwitz polynomial.**
The main theorem now easily follows from theorem 2, because the degree condition implies that even_part(p) and odd_part(p) **have no common roots.**

## 5 Discussion - Lessons Learned

In the following we discuss our formalization from the last section with **respect**
to the tree criteria developed in the introduction. Though restricted to Mizar we claim that the situation in other repositories is similar, so that most **of our** results hold in a more general context also.

In [SR07] we already presented a Mizar formalization of Schur's theorem, another helpful criterion for stability checking. Based on polynomials only its formalization was rather harmless. The only missing point that caused some work was division of polynomials. However, as we will see, stability checking in general needs definitely more extension than in this case.

## 5.1 Amount Of Knowledge

Complex numbers and polynomials (over arbitrary rings) are included **in MML.** A lot of theorems have been proved here, so that almost all we needed could be found in the repository. Interestingly rational functions - a rather basic structure - had not been defined, yet. The reason might be that rational functions are mathematically rather simple and this is the first time that a theorem relying on rational functions has been formalized.

Though even and odd functions were already included in MML, the even and odd part of a polynomial was not. This, however, comes with no surprise, just because these polynomial operations are rather seldom used. We hence had to prove a number of theorems dealing with these polynomials, most of them however being elementary like for example

## Theorem

for p being real Polynomial of F_Complex for x being Element of F_Complex st Re(x) = 0 holds Re(eval(odd_part(p),x)) = 0; Summarizing, besides the lack of rational functions, MML provides the amount of knowledge for stability checking one could expected.