@MISC{HILB10_3.MIZ,
  AUTHOR = {Acewicz, Marcin and P\k{a}k, Karol},
  TITLE = {Basic Diophantine Relations},
  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 = {Basic Diophantine Relations},
  SECTION3 = {Main Lemmas},
  DAY = {29},
  MONTH = {June},
  YEAR = {2018},
  ADDRESS1 = {Institute of Informatics\\University of Bia{\l}ystok\\Konstantego Cio{\l}kowskiego 1M, 15-245 Bia{\l}ystok\\Poland},
  ADDRESS2 = {Institute of Informatics\\University of Bia{\l}ystok\\Konstantego Cio{\l}kowskiego 1M, 15-245 Bia{\l}ystok\\Poland},
  SUMMARY = {The main purpose of formalization is to prove that two equations $\texttt{y}_a(z)=y$, $y=x^z$  are Diophantine.
  These equations are explored in the proof of Matiyasevich’s negative solution of  Hilbert’s tenth problem.
  \par
  In our previous work \cite{HILB10_1.ABS}, we showed that from the diophantine standpoint these equations can be obtained from lists of several basic Diophantine relations
  as linear equations, finite products, congruences and inequalities.
  In this formalization, we express these relations in terms of Diophantine set introduced in \cite{HILB10_2.ABS}.
  We prove that these relations are Diophantine and then we prove several second-order theorems that
  provide the ability to combine Diophantine relation using conjunctions and alternatives as well as
  to substitute the right-hand side of a given Diophantine equality as an argument in a given Diophantine relation.
  Finally, we investigate the possibilities of our approach to
  prove that the two equations, being the main purpose of this formalization, are Diophantine.
 \par The formalization follows Z. Adamowicz, P. Zbierski
 \cite{AdamowiczZbierski} as well as M. Davis \cite{Hilbert10}.}
}

