@MISC{HILB10_5.MIZ,
  AUTHOR = {P\k{a}k, Karol},
  TITLE = {Formalization of the {MRDP} Theorem in the {M}izar System},
  NOTE = {This work has been financed by the
    resources of the Polish National Science Centre granted by decision
    no. DEC-2015/19/D/ST6/01473.},
  SECTION1 = {Preliminaries},
  SECTION2 = {Selected operations on polynomials},
  SECTION3 = {Selected subsets of zero based finite sequences of $\mathbb{N}$ as diophantine sets},
  SECTION4 = {Bounded quantifier theorem and its variant},
  SECTION5 = {MRDP Theorem},
  DAY = {27},
  MONTH = {May},
  YEAR = {2019},
  ADDRESS1 = {Institute of Informatics\\University of Bia{\l}ystok\\Konstantego Cio{\l}kowskiego 1M, 15-245 Bia{\l}ystok\\Poland},
  SUMMARY = {This article is the final step of our attempt to formalize the negative
  solution of Hilbert's tenth problem.
  \par
  In our approach, we work with the Pell's Equation defined in~\cite{PELLS_EQ.ABS}.
  We analyzed this equation in the general case to show its solvability
  solvability as well as the cardinality and shape of all possible solutions.
  Then we focus on a special case of the equation,
  which has the form $x^2-(a^2-1)y^2=1$~\cite{HILB10_1.ABS}
  and its solutions considered as two sequences
  $\{x_{i}(a)\}_{i=0}^\infty$, $\{y_{i}(a)\}_{i=0}^\infty$.
  We showed in~\cite{HILB10_3.ABS} that $n$-th element of these sequences 
  can be obtained from lists of   several basic Diophantine relations
  as linear equations, finite products, congruences and inequalities, or more precisely
  that the equation
  $x=y_{i}(a)$ is Diophantine.
  Following the post-Matiyasevich we use this result
  to show that the equality determined by the value of the power function $y = x^z$ is Diophantin,
  and analogously property in cases of the binomial coefficient, factorial and several 
  product~\cite{HILB10_4.ABS}.
  \par
  In this article, we
  combine analyzed so far Diophantine relation using conjunctions, alternatives as well as
  substitution to prove the bounded quantifier theorem.
  Based on this theorem we prove MDPR-theorem
  that {\it every recursively enumerable set is Diophantine,}
  where recursively enumerable sets have been defined by
  the Martin Davis normal form.
  \par The formalization follows Z. Adamowicz, P. Zbierski
  \cite{AdamowiczZbierski} as well as M. Davis \cite{Hilbert10}.}
}
