Eventually Increasing


It is shown that every eventually increasing, normalising, locally confluent abstract rewrite system is terminating. It is indicated how this lemma can be applied to prove termination of various (proof) calculi.