ABSTRACT

Thus we now assume that there is a unary operation symbol fo of weight zero. We define a mapping h from the set of all unary terms into itself such that h(t) is the unary term obtained from t by replacing all occurrences of fo by another unary term. Clearly the mapping h preserves the weight and there are only finitely many nullary terms of weight w (by the previous remark). Now we show that there is no infinite chain to

>KB tl >KB> t2 >KB • • • of nullary terms such that h(to) = h(t1 ) = h(t2) = • • •. Each nullary term t can be regarded as a word over the set of all nullary operation symbols; that means t can be written in the form t = fon aifor2a2 • • • gi or t = al fon a2for2 • • • an forn a,„ where r1, , rn are natural numbers and al, , an are words built up by nullary operation symbols except fo. Let r(t) = (rl , , rn) be the n-tuples consisting of the exponents of the occurrences of fo.