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

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




Subsumption of terms and substitutions.



compareTermSubs :: LNTerm -> LNTerm -> WithMaude (Maybe Ordering)Source

Compare terms t1 and t2 with respect to the subsumption order modulo AC.

eqTermSubs :: LNTerm -> LNTerm -> WithMaude BoolSource

Returns True if s1 and s2 are equal with respect to the subsumption order modulo AC.

canonical representations for substitutions

canonizeSubst :: LNSubstVFresh -> LNSubstVFreshSource

Returns a substitution that is equivalent modulo renaming to the given substitution.

for testing only

varOccurences :: LNSubstVFresh -> LVar -> [[Position]]Source

varOccurences v t returns a sorted list of positions where the variable v occurs in t. The function returns the same result for terms that are equal modulo AC since the flattened term representation is used.