Abstract Despite its simple formulation, the decidability of the logic BB ′ IW has remained an open problem. We present here a decision procedure for a fragment of it, called the arity-1 formulas. The decidability proof is based on a representation of formulas called formula-trees, which is coupled with a proof method that computes long normal λ-terms that inhabit a formula. A rewriting-system is associated with such λ-terms, and we show that a formula admits a BB ′ IW - λ-term if and only if the associated rewriting-system terminates. The fact that termination is decidable is proved using a result on the finiteness of non-ascending sequences of n-tuples in N n , which is equivalent to Kripke's Lemma.