  Infinite Gray code has been introduced by Tsuiki as a redundancy-free
representation of the reals. In applications the signed digit representation is
mostly used which has maximal redundancy. Tsuiki presented a functional program
converting signed digit code into infinite Gray code. Moreover, he showed that
infinite Gray code can effectively be converted into signed digit code, but the
program needs to have some non-deterministic features (see also H. Tsuiki, K.
Sugihara, "Streams with a bottom in functional languages"). Berger and Tsuiki
reproved the result in a system of formal first-order intuitionistic logic
extended by inductive and co-inductive definitions, as well as some new logical
connectives capturing concurrent behaviour. The programs extracted from the
proofs are exactly the ones given by Tsuiki. In order to do so, co-inductive
predicates $\bS$ and $\bG$ are defined and the inclusion $\bS \subseteq \bG$ is
derived. For the converse inclusion the new logical connectives are used to
introduce a concurrent version $\S_{2}$ of $S$ and $\bG \subseteq \bS_{2}$ is
shown. What one is looking for, however, is an equivalence proof of the
involved concepts. One of the main aims of the present paper is to close the
gap. A concurrent version $\bG^{*}$ of $\bG$ and a modification $\bS^{*}$ of
$\bS_{2}$ are presented such that $\bS^{*} = \bG^{*}$. A crucial tool in U.
Berger, H. Tsuiki, "Intuitionistic fixed point logic" is a formulation of the
Archimedean property of the real numbers as an induction principle. We
introduce a concurrent version of this principle which allows us to prove that
$\bS^{*}$ and $\bG^{*}$ coincide. A further central contribution is the
extension of the above results to the hyperspace of non-empty compact subsets
of the reals.
