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.

翻译：无穷格雷码由Tsuiki引入，作为实数的一种无冗余表示。在实际应用中，符号位表示（具有最大冗余度）被广泛使用。Tsuiki提出了一个将符号位码转换为无穷格雷码的函数式程序。此外，他证明了无穷格雷码可以有效转换为符号位码，但该程序需要具备某些非确定性特征（参见H. Tsuiki, K. Sugihara, "Streams with a bottom in functional languages"）。Berger和Tsuiki在一种扩展了归纳与余归纳定义以及捕捉并发行为的新逻辑连接词的一阶直觉主义逻辑系统中，重新证明了该结论。从证明中提取的程序与Tsuiki先前给出的完全一致。为此，他们定义了余归纳谓词$\bS$和$\bG$，并推导出包含关系$\bS \subseteq \bG$。对于反向包含关系，则利用新逻辑连接词引入$S$的并发版本$\S_{2}$，并证明了$\bG \subseteq \bS_{2}$。然而，我们真正需要的是对相关概念进行等价性证明。本文的主要目标之一即是弥合这一差距。我们提出$\bG$的并发版本$\bG^{*}$和$\S_{2}$的修正版本$\bS^{*}$，使得$\bS^{*} = \bG^{*}$。在U. Berger, H. Tsuiki, "Intuitionistic fixed point logic"中，一个关键工具是将实数的阿基米德性质表述为归纳原理。我们引入该原理的并发版本，从而证明$\bS^{*}$与$\bG^{*}$的等价性。另一核心贡献是将上述结果推广至实数非空紧子集构成的高维空间。