Generalizations in Mathematical Epidemiology

Abstract

We are concerned by imminent future problems caused by biological dangers, here we think of a way to solve them. One of them is analyzing endemic models, for this we make a study supported by Computer Algebra Systems (CAS) and Mechanized Reasoning (MR). Also we show the advantages of the use of “CAS” and “MR” to obtain in that case, an epidemic threshold theorem. We prove a previously obtained theorem for SⁿIR endemic model. Moreover using “CAS+MR” we obtain a new epidemic threshold theorem for the SⁿI^mR epidemic model and for the staged progressive SI^mR model. Finally we discuss the relevance of the theorems and some future applications.

1 Introduction

At the moment, we are at the edge of a possible biological problem. Some people say that the nineteenth century was the century of chemistry, the twentieth was the century of physics, and they say that the twenty-first will be the century of biology. If we think, the advances in the biological field in the recent years have been incredible, and like the physics and its atomic bomb, with biology could create global epidemics diseases. Also the climate change could produce a new virus better than the existing virus, creating an atmosphere of panic. For these reasons and others, we think in a solution using mathematical models with computer algebra and mechanized reasoning. Specifically we consider the SIR (Susceptible-Infective-Removed) model, with differential susceptibility and multiple kinds of infected individuals. The objective is to derive three epidemic threshold theorems by using the algorithm MKNW given in [1] and a little bit of mechanized reasoning.

Briefly the MKNW runs on: Initially we have a system of ordinary non-lineal differential equations S, whose coefficients are polynomial. We start setting all derivates to zero for finding equilibrium; we solve the system finding the equilibrium point T. Then we compute the Jacobian Jb for the system S and replace T in S. We compute the eigenvalues for Jb; from the eigenvalues we obtain the stability conditions when each eigenvalue is less than zero. Finally we obtain the reproductive number for the system S in the particular cases. Using deductive reasoning we obtain some theorems based on the particular cases.

The MKNW algorithm is not sufficient to prove the threshold theorems that will be considered here and for this reason, it is necessary to use some form of mechanized reasoning, specifically some strategy of mechanized induction.

The threshold theorem that we probe in Section 2 was originally presented in [2] using only pen and paper and human intelligence. A first contribution of this paper is a mechanized derivation of such theorem using CAS.

The threshold theorem to be proved in Section 3 is original and some particular cases of this theorem were previously considered via CAS in [3, 4] and without CAS in [5].

The threshold theorem to be proved in Section 4 is original and similar models were before considered without CAS in [6].

2 CA And MR Applied to the S^NIR Epidemic Model

We introduce the system for the SⁿIR epidemic model, which has n groups of susceptible individuals and which is described by the next system of Eq. [2]:

$$\begin{array}{lll}{{\frac{d}{{{d}t}}\ {X_i}(t) = \mu ({{p}_i}{X_0} - {X_i}(t)) - {\lambda _i}{X_i}(t)}}\\ \frac{d}{{{d}t}}\ {Y}(t) = \sum\limits_{k = 1}^n {{\lambda _k}{X_k}(t) - (\mu + \gamma + \delta )\,{Y}(t)}\\ \frac{d}{{{d}t}}\ Z(t) = \gamma Y(t) - (\mu + \varepsilon )\,Z(t)\end{array}$$

(1)

we define the rate of infection as:

$${\lambda _i} = {\alpha _i}\beta \eta Y(t)$$

(2)

and we define p _i as follow:

$${\sum\limits_{i = 1}^n {{p_i} = 1}}$$

(3)

This is a system with (n + 2) equations and each previous constant is defined like it is shown:

• μ is the natural death rate.

• γ is the rate at which infectives are removed or become immune.

• δ is the disease-induced mortality rate for the infectives.

• ε is the disease-induced mortality rate for removed individuals.

• α_i is the susceptibility of susceptible individuals.

• β is the infectious rate of infected individuals.

• η is the average number of contacts per individual.

Each function or group is defined as follow:

• X _i(t) are the n groups of susceptible in the time equal t

• Y(t) is the group of infectives in the time equal t.

• Z(t) is the group of removed in the time equal t.

2.1 The Standard SIR Model

As a particular case we analyze the standard SIR model [7] which has just one group of susceptible and is described in the next equation system:

$$\begin{array}{lll}{\frac{d}{{{d}t}}{X_1}(t) = \mu ({p_1}{X_0} - {X_1}(t)) - {\lambda _1}{X_1}(t)} \\{\frac{d}{{{d}t}}Y(t) = {\lambda _1}{X_1}(t) - (\mu + \gamma + \delta )Y(t)} \\{\frac{d}{{{d}t}}Z(t) = \gamma Y(t) - (\mu + \varepsilon )Z(t)}\end{array}$$

(4)

In the infection-free equilibrium there is no variation in time. So the derivates are canceled and the solution for the previous system, it’s given by:

$${{X_1} = {p_1}{X_0},Y = 0}$$

(5)

After, we generate the Jacobian matrix for the equations system:

$$\left[ \begin{array}{lll} - \mu - {\alpha _1}\eta \beta Y \quad \quad \quad \quad { - {\alpha _1}\eta {X_1}\beta }\quad \quad \\{ - {\alpha _1}\eta \beta Y} \quad \quad\quad {{\alpha _1}\rm eta {X_1}\beta - \mu - \gamma - \delta } \\ \end{array} \right]$$

(6)

we substitute the solution (5) in the Jacobian:

$$\left[ \begin{array}{lll} - \mu \quad\quad \quad \quad { - {\alpha _1}\eta {p_1}{X_0}\beta } \quad \quad \\0 \quad\quad {{\alpha _1}\eta {p_1}{X_0}\beta - \mu - \gamma - \delta } \\ \end{array} \right]$$

(7)

Now, we find the eigenvalues for the previous matrix:

$${ - \mu,{\alpha _1}\eta {p_1}{X_0}\beta - \mu - \gamma - \delta}$$

(8)

and its corresponding stability condition is:

$${{\alpha _1}\eta {p_1}{X_0}\beta - \mu - \gamma - \delta < 0}$$

(9)

this can be rewritten as:

$${\frac{{{\alpha _1}\eta {p_1}{X_0}\beta }}{{\mu + \gamma + \delta }} < 1}$$

(10)

using the next expression:

$${{R_0}< 1}$$

(11)

Finally we find the basic reproduction number which it represents the condition of equilibrium:

$${R_0} = \frac{{{\alpha _1}\eta {p_1}{X_0}\beta }}{{\mu + \gamma + \beta }}$$

(12)

2.2 The S²IR Model

As another particular case we analyze the S²IR model where there are two groups of susceptible and the equations for this system are:

$$\begin{array}{llll}{\frac{d}{{{d}t}}{X_1}(t) = \mu ({p_1}{X_0} - {X_1}(t)) - {\lambda _1}{X_1}(t)}\\{\frac{d}{{{d}t}}{X_2}(t) = \mu ({p_2}{X_0} - {X_2}(t)) - {\lambda _2}{X_2}(t)}\\{\frac{d}{{d}t}Y(t) = {\lambda _1}{X_1}(t) + {\lambda _2}{X_2}(t) - Y(t)\mu - \gamma Y(t) - Y(t)\delta } \\{\frac{d}{{{d}t}}Z(t) = \gamma Y(t) - (\mu + \varepsilon )Z(t)}\end{array}$$

(13)

Initially we find the infection-free equilibrium solution for the previous system:

$${{X_1} = {p_1}{X_0},{X_2} = {p_2}{X_0},Y = 0}$$

(14)

Equally we generate the Jacobian matrix for the equations system and substituting the infection-free equilibrium point in the Jacobian:

$$\left[ \begin{array} {llll} - \rm mu \quad 0 \quad \quad \quad \quad\quad\quad{ - {\alpha _1}\rm eta {p_1}{X_0}\rm beta } \quad \quad \quad\quad\quad\\0 \quad { - \rm mu } \quad \quad\quad\quad\quad\quad{ - {\alpha _2}\rm eta {p_2}{X_0}\rm beta } \quad\quad\quad\quad\quad\\0 \quad \ 0 \quad \quad{{\alpha _1}\rm eta {p_1}{X_0}\rm beta + {\alpha _2}\rm eta {p_2}{X_0}\rm beta - \rm mu - \gamma - \delta } \\\end{array} \right]$$

(15)

we find the eigenvalues for the previous Jacobian,

$${ - \mu, - \mu,{\alpha _1}\eta {p_1}{X_0}\beta + {\alpha _2}\eta {p_2}{X_0}\beta - \mu - \gamma - \delta}$$

(16)

and the corresponding stability condition is:

$${{\alpha _1}\eta {p_1}{X_0}\beta + {\alpha _2}\eta {p_2}{X_0}\beta - \mu - \gamma - \delta < 0}$$

(17)

this can be rewritten as:

$${\frac{{{\alpha _1}\eta {p_1}{X_0}\beta + {\alpha _2}\eta {p_2}{X_0}\beta }}{{\mu + \gamma + \delta }} < 1}$$

(18)

also it can be written using (11) as:

$${R_0} = \frac{{{\alpha _1}\eta {p_1}{X_0}\beta + {\alpha _2}\eta {p_2}{X_0}\beta }}{{\mu + \gamma + \delta }}$$

(19)

this is the basic reproductive number for S²IR model.

2.3 The S³IR, The S⁴IR and S⁵IR Models

Here we show the S³IR, the S⁴IR and S⁵IR models where there are three, four and five groups of susceptibles, respectively. With these models we do the same process, and we only show the basic reproductive number.

$${R_0} = \frac{{{\alpha _1}\eta {p_1}{X_0}\beta + {\alpha _2}\eta {p_2}{X_0}\beta + {\alpha _3}\beta \eta {p_3}{X_0}}}{{\mu + \gamma + \delta }}$$

(20)

this is the basic reproductive number for S³IR model.

$${R_0} = \frac{{{\alpha _1}\eta {p_1}{X_0}\beta + {\alpha _2}\eta {p_2}{X_0}\beta + {\alpha _3}\beta \eta {p_3}{X_0} + {\alpha _4}\beta \eta {p_4}{X_0}}}{{\mu + \gamma + \delta }}$$

(21)

this is the basic reproductive number for S⁴IR model.

$${R_0} = \frac{{{X_0}\beta \eta ({\alpha _1}{p_1} + {\alpha _2}{p_2} + {\alpha _3}{p_3} + {\alpha _4}{p_4} + {\alpha _5}{p_5})}}{{\mu + \gamma + \delta }}$$

(22)

and this is the basic reproductive number for S⁵IR model.

2.4 The SⁿIR Model

Theorem. For the equations system given by (1). The infection-free equilibrium is locally stable if R ₀ < 1, and is unstable if R ₀ > 1, where:

$${R_0} = \frac{{{X_0}\beta \eta \left( {\sum\limits_{i = 1}^n {{\alpha _i}{p_i}} } \right)}}{{\mu + \gamma + \delta }}$$

(23)

We can probe the theorem looking the inequalities corresponding to stability conditions for each system previously considered, we have listed in the Fig. 1. Using mechanized induction we obtain the general expression for the stability conditions for a system with (n + 2) equations.

Fig. 1

Inductive mechanized reasoning for the SⁿIR Model

$$\frac{{{X_0}\beta \eta \left( {\sum\limits_{i = 1}^n {{\alpha _i}{p_i}} } \right)}}{{\mu + \gamma + \delta }} < 1$$

(24)

We can represent into a schematic diagram, the deductive reasoning using “MR”.

Here we have an idea for the MR, it finds the similar components in each item and it has a viewer or a detector that find the sequential form for the dissimilar parts. It is just an idea, we believe this system have to be improved by the scientific community.

3 CA and MR Applied to the S^NI^MR Epidemic Model

The SⁿI^mR epidemic model is made by a group of equations which has n groups of susceptible individuals and m groups of infected people, this system is illustrated in the next equations:

$$\begin{array}{llll}{\frac{d}{{{d}t}}{X_i}(t) = \mu ({p_i}{X_0} - {X_i}(t)) - {\alpha _i}\eta \left( {\sum\limits_{i = 1}^m {{\beta _j}{Y_j}(t)} } \right){X_i}(t)}\\{\frac{d}{{{d}t}}{Y_j}(t) = \eta {\beta _j}{Y_j}(t)\left( {\sum\limits_{i = 1}^n {{\alpha _i}{X_i}(t)} } \right) - (\mu + \gamma + \delta ){Y_j}(t)} \\{\frac{d}{{{d}t}}Z(t) = \gamma {Y_j}(t) - (\mu + \varepsilon )Z(t)}\end{array}$$

(25)

p _i is defined in (3). This is a system with (n + m + 1) equations and each constant were defined in the last model.

3.1 The SI²R Model

Like in all cases, we analyze a particular case with one group of susceptibles and two groups of infectives. The following equations describe this case:

$$\begin{array}{llll}{\frac{d}{{d}t}{X_1}(t) = \mu ({p_1}{X_0} - {X_1}(t)) - {\alpha _1}\eta \left( {\sum\limits_{j = 1}^2 {{\beta _j}{Y_j}(t)} } \right){X_1}(t)}\\{\frac{d}{{{d}t}}{Y_1}(t) = \eta {\beta _1}{Y_1}(t)\left( {\sum\limits_{i = 1}^1 {{\beta _i}{X_i}(t)} }\right) - (\mu + \gamma + \delta ){Y_1}(t)} \\{\frac{d}{{{d}t}}{Y_2}(t) = \eta {\beta _2}{Y_2}(t)\left( {\sum\limits_{i = 1}^1 {{\alpha _i}{X_i}(t)} } \right) - (\mu + \gamma + \delta ){Y_2}(t)}\\{\frac{d}{{dt}}Z(t) = \gamma {Y_j}(t) - (\mu + \varepsilon )Z(t)}\end{array}$$

(26)

Solving the system for the infection-free equilibrium, we find:

$${Y_1} = 0,{Y_2} = 0,{X_1} = \frac{{\mu {p_1}{X_0}}}{{\mu + {\alpha _1}\eta \left( {\sum\limits_{j = 1}^2 {{\beta _j}{Y_j}} } \right)}}$$

(27)

We generate a Jacobian as in the others cases. After, we substitute the infection-free equilibrium point and we find the eigenvalues for the system,

$${ - \mu,{\alpha _1}\eta {p_1}{X_0}{\beta _1} - \mu - \gamma - \delta,{\alpha _1}\eta {p_1}{X_0}{\beta _2} - \mu - \gamma - \delta}$$

(28)

The stability conditions shall satisfy,

$$\begin{array}{llll}{{\alpha _1}\eta {p_1}{X_0}{\beta _2} - \mu - \gamma - \delta < 0} \\{{\alpha _1}\eta {p_1}{X_0}{\beta _1} - \mu - \gamma - \delta < 0} \\\end{array}$$

(29)

Moreover the inequalities in (29) can be written like the others cases as:

$$\begin{array}{lll}{{R_{0,2}} = \frac{{{\alpha _1}\eta {p_1}{X_0}{\beta _2}}}{{\mu + \gamma + \delta }}} \\{{R_{0,1}} = \frac{{{\alpha _1}\eta {p_1}{X_0}{\beta _1}}}{{\mu + \gamma + \delta }}}\end{array}$$

(30)

Here, we have the two basic reproductive numbers for SI²R model.

3.2 The S²I²R Model

We analyze a particular case where we have two groups of susceptible and two groups of infective, in addition we solve the system for the infection-free equilibrium and we find:

$${Y_1} = 0,{Y_2} = 0,{X_1} = \frac{{\mu {p_1}{X_0}}}{{\mu + {\alpha _1}\eta \left( {\sum\limits_{j = 1}^2 {{\beta _j}{Y_j}} } \right)}},{X_2} = \frac{{\mu {p_2}{X_0}}}{{\mu + {\alpha _2}\eta \left( {\sum\limits_{j = 1}^2 {{\beta _j}{Y_j}} } \right)}}$$

(31)

Also we generate a Jacobian; we substitute the infection-free equilibrium point and find the eigenvalues for this system:

$$\begin{array}{ll} - \mu, - \mu,{\alpha _1}\eta {p_1}{X_0}{\beta _1} + {\alpha _2}\eta {p_2}{X_0}{\beta _1} - \mu - \gamma - \delta,{\alpha _1}\eta {p_1}{X_0}{\beta _2}\\ \quad + {{\alpha _2}\eta {p_2}{X_0}{\beta _2} - \mu - \gamma - \delta}\end{array}$$

(32)

In like manner that we obtained the last reproductive numbers, we obtain the two basic reproductive numbers for S²I²R model:

$$\begin{array}{lll}{{R_{0,2}} = \frac{{{\alpha _1}\eta {p_1}{X_0}{\beta _2} + {\alpha _2}\eta {p_2}{X_0}{\beta _2}}}{{\mu + \gamma + \delta }}} \\{{R_{0,1}} = \frac{{{\alpha _1}\eta {p_1}{X_0}{\beta _1} + {\alpha _2}\eta {p_2}{X_0}{\beta _1}}}{{\mu + \gamma + \delta }}} \end{array}$$

(33)

3.3 The SⁿI^mR Model

Theorem. For the equations system given by (25). The infection-free equilibriums are locally stable if the reproductive numbers of infection R _0,j < 1, and is unstable if R _0,j > 1, with j from 1 to m, where:

$${R_{0,j}} = \frac{{{X_0}\rm \eta \left( {\sum\limits_{i = 1}^n {{\rm \alpha _i}{p_i}} } \right){\rm \beta _j}}}{{\rm mu + \rm \gamma + \rm \delta }}$$

(34)

To prove the theorem, we used mechanized induction starting from the particular results previously obtained in (30) and (33). Finally, we find the general solution for the basic reproductive numbers for the SⁿI^mR model according with (Fig. 2).

Fig. 2

Inductive mechanized reasoning for the SⁿI^mR Model

4 CA and MR Applied to the Staged Progressive SI^MR Epidemic Model

At this moment, we are concerned in the analysis of the staged progressive SI^mR epidemic model. This has m groups of infected; in this case the infection is staged and progressive, which is described by next system:

$$\begin{array}{lllll}{\frac{\rm d}{{{\rm d}t}}X(t) = \rm \mu ({x_0} - X(t)) - \lambda X(t)}\\{\frac{\rm d}{{{\rm d}t}}{Y_1}(t) = \lambda X(t) - (\rm \mu + {\rm \gamma _1} + {\rm \delta _1}){Y_1}(t)} \\{\frac{\rm d}{{{\rm d}t}}{Y_j}(t) = {Y_{j - 1}}{Y_{j - 1}}(t) - (\rm \mu + {\rm \gamma _j} + {\rm \delta _j}){Y_j}(t)} \\{\frac{\rm d}{{{\rm d}t}}Z(t) = {\rm \gamma _m}{Y_m}(t) - (\rm \mu + \rm \varepsilon )Z(t)} \\\end{array}$$

(35)

with the restriction for j is: 2 ≤ j ≤ m. And where the rate of infection is:

$${\lambda = \rm\alpha \left( {\sum\limits_{j = 1}^m {{\rm\beta _j}{Y_j}(t)} } \right)\rm\eta}$$

(36)

This is a system with (m + 2) equations and all the constants were described before.

4.1 The Staged Progressive SI²R Model

Now, we analyze a particular case with one group of susceptible and two groups of infectives. The following equations describe this case:

$$\begin{array}{lll}{\frac{\rm d}{{{\rm d}t}}X(t) = \rm\mu ({x_0} - X(t)) - \lambda X(t)}\\{\frac{\rm d}{{{\rm d}t}}{Y_1}(t) = \lambda X(t) - (\rm\mu + {\rm\gamma _1} + {\rm\delta _1}){Y_1}(t)} \\{\frac{\rm d}{{{\rm d}t}}{Y_2}(t) = {\lambda _1}{Y_1}(t) - (\rm\mu + {\rm\gamma _2} + {\rm\delta _2}){Y_2}(t)} \\{\frac{\rm d}{{{\rm d}t}}Z(t) = {\lambda _2}{Y_2}(t) - (\rm\mu + \rm\varepsilon )Z(t)} \\\end{array}$$

(37)

Solving the system for the infection-free equilibrium, we find:

$${X = \frac{{\rm\mu {x_0}}}{{\rm\mu + \rm\alpha \rm\eta {\rm\beta _1}{Y_1}+ \rm\alpha \rm\eta {\rm\beta _2}{Y_2}}},{Y_1} = 0,{Y_2} = 0}$$

(38)

We generate a Jacobian coming off the equations system and substituting the infection-free equilibrium point:

$$\left| {\begin{array}{lllll} { - \rm\mu } \quad\quad\quad\quad\quad { - \rm\alpha \rm\eta {x_0}{\rm\beta _1}} \quad\quad\quad\quad { - \rm\alpha \rm\eta {x_0}{\rm\beta _2}} \quad\\0 \quad \quad{ - \rm\alpha \rm\eta {x_0}{\rm\beta _1} - \rm\mu - {\rm\gamma _1} - {\rm\delta _1}} \quad \quad{\rm\alpha \rm\eta {x_0}{\rm\beta_2}}\quad \\0 \ \quad\quad\quad\quad\quad \quad{{\rm\gamma _1}} \quad \quad\quad\quad\quad{ - \rm\mu - {\rm\gamma _2} - {\rm\delta _2}} \\\end{array}} \right|$$

(39)

Now we obtain the characteristic polynomial:

$$\begin{array}{lll}(\lambda + \rm\mu )({\lambda ^2} + 2\lambda \rm\mu + \lambda {\rm\gamma _2} + \lambda {\rm\delta _2} - \rm\alpha \rm\eta {x_0}{\rm\beta _1}\lambda - \rm\alpha \rm\eta {x_0}{\rm\beta _1}\rm\mu \\{ - \,\rm\alpha \rm\eta {x_0}{\rm\beta _1}{\rm\gamma _2} - \rm\alpha \rm\eta {x_0}{\rm\beta _1}{\rm\delta _2} + {\rm\mu ^2} + \rm\mu {\rm\gamma _2} + \rm\mu {\rm\delta _2} + {\rm\gamma _1}\lambda } \\{ + \,{\rm\gamma _1}\rm\mu + {\rm\gamma _1}{\rm\gamma _2} + {\rm\gamma _1}{\rm\delta _2} + {\rm\delta _1}\lambda + {\rm\delta _1}{\rm\gamma _2} + {\rm\delta _1}{\rm\delta _2}} \\{ - \,\rm\alpha \rm\eta {x_0}{\beta _2}{\rm\gamma _1}} \\ \end{array}$$

(40)

From this polynomial, we obtain the basic reproduction number using the Routh-Hurwitz theorem:

$${R_0} = \frac{{{x_0}\rm\alpha \rm\eta ({\rm\beta _1}{\rm\delta _2} + {\rm\beta _1}\rm\mu + {\rm\beta _1}{\rm\gamma _2} + {\rm\beta _2}{\rm\gamma _1})}}{{(\rm\mu + {\rm\gamma _2} + {\rm\delta _2})(\rm\mu + {\rm\gamma _1} + {\rm\delta _1})}}$$

(41)

4.2 The Staged Progressive SI³R Model

We analyze a particular case with three groups of infectives. We solve this system in the same way that we did in the Section 4.1. For this model the basic reproduction number that we find is:

$$\begin{array}{lllll}{R_0} = ({x_0}\rm\alpha \rm\eta ({\rm\beta _1}{\rm\delta _2}\rm\mu + {\rm\beta _1}{\rm\delta _2}{\lambda _3} + {\rm\beta _1}\rm\mu {\lambda _3} + {\rm\beta _1}{\rm\gamma _2}\rm\mu + {\rm\beta _1}{\rm\gamma _2}{\rm\gamma _3} \\{ + {\rm\beta _1}{\rm\gamma _2}{\rm\delta _3} + {\rm\beta _1}{\rm\mu ^2} + {\rm\beta _1}{\rm\delta _2}{\rm\delta _3} + {\rm\gamma _1}{\rm\beta _2}\rm\mu + {\rm\gamma _1}{\rm\beta _2}{\rm\gamma _3} + {\rm\gamma _1}{\rm\beta _2}{\rm\delta _3}} \\ + {\rm\gamma _1}{\rm\beta _3}{\rm\gamma _2} + {\rm\beta _1}\rm\mu {\rm\delta _3}))/((\rm\mu + {\rm\gamma _3} + {\rm\delta _3})(\rm\mu + {\rm\gamma _2} + {\rm\delta _2})(\rm\mu \\ + {\rm\gamma _1} + {\rm\delta _1}))\\\end{array}$$

(42)

4.3 Staged Progressive SI^mR Model

Theorem. For the equations system given by (35). The infection-free equilibrium is locally stable if the reproductive numbers of infection R ₀ < 1, and is unstable if R ₀ > 1, with j from 1 to m, where:

$${R_0} = \frac{{{x_0}\alpha \eta \left( {\sum\limits_{j - 1}^m {{\beta _j}\prod\limits_{k = 1}^{j - 1} {{\gamma _k}\prod\limits_{l = j + 1}^m {(\mu + {\gamma _l} + {\delta _l})} } } } \right)}}{{\prod\limits_{l = 1}^m {(\mu + {\gamma _l} + {\delta _l})} }}$$

(43)

To prove the theorem, we used mechanized induction starting from the particular results previously obtained. To conclude, we find the general solution for the basic reproductive numbers for the Staged Progressive SI ^m R model according with (Fig. 3 ).

Fig. 3

Inductive mechanized reasoning for the staged progressive SI^mR Model

5 Conclusions

We finally obtain three theorems which can help us to demonstrate that CAS+MR are important tools for solving problems in every situation that mathematics could model. The theorems are useful to make strategies to fight against epidemic diseases in the future biological dangers.

Due to use CAS, in our case “Maple 11”, we can proceed to solve the mathematical problem and we can obtain results very fast that without them could take us too much time.

The use of CAS+MR can help in teaching and learning the mathematics to engineering, whose don’t have time and need to give quickly solutions. It can be implemented in engineer programs.

Through the MR we already found the general forms for the infection free equilibrium, we can see the importance of developing software it can do the mechanized reasoning automatically.