  A cyclic proof system generalises the standard notion of a proof as a finite
tree of locally sound inferences by allowing proof objects to be potentially
infinite. Regular infinite proofs can be finitely represented as graphs. To
preclude spurious cyclic reasoning, cyclic proof systems come equipped with a
well-founded notion of 'size' for the models that interpret their logical
statements. A global soundness condition on proof objects, stated in terms of
this notion of size, ensures that any non-well-founded paths in the proof
object can be disregarded.
  We give an abstract definition of a subclass of such cyclic proof systems:
cyclic entailment systems. In this setting, we consider the problem of
comparing the size of a model when interpreted in relation to the antecedent of
an entailment, with that when interpreted in relation to the consequent.
Specifically, we give a further condition on proof objects which ensures that
models of a given entailment are always 'smaller' when interpreted with respect
to the consequent than when interpreted with respect to the antecedent.
Knowledge of such relationships is useful in a program verification setting.
