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

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



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.



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.