Finite and infinite regular continued fractions

A finite regular continued fraction is an expression $[a_0;a_1,\dots ,a_n]$ with $a_0\in \mathbb{Z}$ and $a_i\in {\mathbb{Z}}_{>0}$ for $i\ge 1$. Its value is defined recursively in $\mathbb{Q}$ (The rationals as equivalence classes of pairs of integers, Arithmetic on the rationals) by $[a_n]:=a_n,[a_0;a_1,\dots ,a_n]:=a_0+\frac{1}{[a_1;\dots ,a_n]}(n\ge 1)\mathrm{.}$

This recursion is well defined. Indeed, starting from the last digit and working backwards, every tail $[a_i;\dots ,a_n]$ with $i\ge 1$ is a positive rational: the last tail is $a_n>0$, and $a_i+1\mathrm{/}t>0$ whenever $a_i>0$ and $t>0$. In particular every denominator occurring in the recursion is nonzero.

An infinite regular continued fraction is a digit sequence $(a_n{)}_{n\ge 0}$ with $a_0\in \mathbb{Z}$ and $a_n\in {\mathbb{Z}}_{>0}$ for $n\ge 1$, written $[a_0;a_1,a_2,\dots ]\mathrm{.}$ Its value is not assumed by the notation; existence and uniqueness of the value are proved in Every infinite regular continued fraction converges to a unique real number.