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

MaintainerBenedikt Schmidt <beschmi@gmail.com>
Safe HaskellNone



This module implements normalization and normal-form checks of terms.



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.