Term.Subsumption

Subsumption of terms and substitutions.

Documentation

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

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

eqTermSubs :: LNTerm -> LNTerm -> WithMaude Bool

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

factorSubstVia :: [LVar] -> LNSubst -> LNSubst -> WithMaude [LNSubst]

canonical representations for substitutions

canonizeSubst :: LNSubstVFresh -> LNSubstVFresh

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

for testing only

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

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.