It is shown that the infiniteness problem of proof (a) is polynomial-space complete. The set proof (~) is the set of closed I-terms in p-normal form which has a as their types. The set is identical to the set of normal form proofs of a in the natural deduction system for implicational fragment of intuitionistic logic.
A transformation of a type is defined by F(a)=(((b-+a)-+a)+b)--tb
and applied as a deduction of the non-emptiness problem to the infiniteness problem. The non-emptiness is identical to the provability of a, which is polynomial-space complete . Therefore, the infiniteness problem is polynomial-space hard. To show the polynomial completeness, an algorithm is shown which searches I-terms of given type a. It is proved that the infiniteness is determined within the depth of 21a13, where the size Ial is the total number of occurrences of symbols in a. Thus, the problem is solved in polynomial space. Hence, the infiniteness problem is polynomial-space complete. The bound is obtained by an estimation of the length of an irredundant chain of scquents in type-assignment system in sequent calculus formulation.