tamarin-prover-term-0.8.0.0: Term manipulation library for the tamarin prover.

MaintainerBenedikt Schmidt <beschmi@gmail.com>
Safe HaskellSafe-Infered

Term.Rewriting.Norm

Description

This module implements normalization with respect to DH u AC using class rewriting and an ad-hoc function that uses the TermAC representation of terms modulo AC.

Synopsis

Documentation

norm' :: LNTerm -> WithMaude LNTermSource

norm' t normalizes the term t using Maude.

nf' :: LNTerm -> WithMaude BoolSource

nf' t returns True if the term t is in normal form.

nfSubstVFresh' :: LNSubstVFresh -> WithMaude BoolSource

nfSubst s returns True if the substitution s is in normal form.

normSubstVFresh' :: LNSubstVFresh -> WithMaude LNSubstVFreshSource

normSubst s normalizes the substitution s.

maybeNotNfSubterms :: MaudeSig -> LNTerm -> [LNTerm]Source

Returns all subterms that may be not in normal form.