tamarin-prover-theory- Term manipulation library for the tamarin prover.

PortabilityGHC only
MaintainerSimon Meier <iridcode@gmail.com>
Safe HaskellNone



This module implements all rules that do not result in case distinctions and equation solving. Some additional cases may although result from splitting over multiple AC-unifiers. Note that a few of these rules are implemented directly in the methods for inserting constraints to the constraint system. These methods are provided by Theory.Constraint.Solver.Reduction.



simplifySystem :: Reduction ()Source

Apply CR-rules that don't result in case splitting until the constraint system does not change anymore.