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^{*}$及$\bS_{2}$的修正版本$\bS^{*}$，使得$\bS^{*} = \bG^{*}$成立。在U. Berger, H. Tsuiki, "Intuitionistic fixed point logic"中，一个关键工具是将实数的阿基米德性质表述为归纳原则。我们引入了该原则的并发版本，从而证明了$\bS^{*}$与$\bG^{*}$的一致性。另一核心贡献是将上述结果推广至实数非空紧子集超空间。