一句话：在直觉主义不动点逻辑中引入并发版本，证明无穷Gray码表示与带符号数字表示的并发概念等价，并推广到实数非空紧子集超空间。
无穷Gray码是Tsuiki提出的实数无冗余表示，而应用中最常用的是具有最大冗余的带符号数字表示。已有函数式程序可把带符号数字码转成无穷Gray码，反向转换虽有效但需要非确定性特征。Berger和Tsuiki曾在带归纳/余归纳定义以及刻画并发行为的新逻辑连接词的一阶直觉主义逻辑中重新证明该结果，并从证明抽取程序，但只得到包含关系而非等价。本文目标是补上等价性证明：引入并发的G*和修正的S*，证明S* = G*。关键工具是Archimedean性质的并发版本，它被表述为归纳原理；论文还把结果推广到实数非空紧子集的超空间。
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.