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^{*}$的一致性。另一核心贡献是将上述结果推广至实数非空紧子集所构成的高维空间。