ABSTRACT. We introduce a sound and complete coinductive proof calculus for reachability properties in transitions systems generated by logically constrained term rewriting rules over an order-sorted signature modulo builtins.

A key feature of the proof calculus is a circularity proof rule, which allows to obtain finite representations of the infinite coinductive proof trees. The paper also includes a brief description of a prototype implementation, which validates our approach on a number of examples.