CoLoR, a Coq library on rewriting and termination. See the COPYRIGHTS and LICENSE files.A specification of termination proofs.
- Adam Koprowski, 2009-03-24
trsInt si is a representation for an interpretation assigning type si to a function symbol. It is represented by a list of pairs: (f, fi), where f is a function symbol and fi is its interpretation.
monomial is a monomial in representation of a polynomial. A monomial C * x_0^i_0 * ... * x_n^i_n is represented as: (C, i_0::...::i_n).
polynomial is a list of monomials so m_0 + ... + m_n becomes m_0::...::m_n.