Library for representation of rules and term rewriting systems.
Author: JanHendrik Matthes
Version: November 2016
showRule
:: (a > String) > (Term a,Term a) > String
Transforms a rule into a string representation. 
showTRS
:: (a > String) > [(Term a,Term a)] > String
Transforms a term rewriting system into a string representation. 
rRoot
:: (Term a,Term a) > Either Int a
Returns the root symbol (variable or constructor) of a rule. 
rCons
:: (Term a,Term a) > [a]
Returns a list without duplicates of all constructors in a rule. 
rVars
:: (Term a,Term a) > [Int]
Returns a list without duplicates of all variables in a rule. 
maxVarInRule
:: (Term a,Term a) > Maybe Int
Returns the maximum variable in a rule or Nothing
if no variable exists.

minVarInRule
:: (Term a,Term a) > Maybe Int
Returns the minimum variable in a rule or Nothing
if no variable exists.

maxVarInTRS
:: [(Term a,Term a)] > Maybe Int
Returns the maximum variable in a term rewriting system or Nothing
if no
variable exists.

minVarInTRS
:: [(Term a,Term a)] > Maybe Int
Returns the minimum variable in a term rewriting system or Nothing
if no
variable exists.

renameRuleVars
:: Int > (Term a,Term a) > (Term a,Term a)
Renames the variables in a rule by the given number. 
renameTRSVars
:: Int > [(Term a,Term a)] > [(Term a,Term a)]
Renames the variables in every rule of a term rewriting system by the given number. 
normalizeRule
:: (Term a,Term a) > (Term a,Term a)
Normalizes a rule by renaming all variables with an increasing order, starting from the minimum possible variable. 
normalizeTRS
:: [(Term a,Term a)] > [(Term a,Term a)]
Normalizes all rules in a term rewriting system by renaming all variables with an increasing order, starting from the minimum possible variable. 
isVariantOf
:: (Term a,Term a) > (Term a,Term a) > Bool
Checks whether the first rule is a variant of the second rule. 
isLeftLinear
:: [(Term a,Term a)] > Bool
Checks whether a term rewriting system is leftlinear. 
isLeftNormal
:: [(Term a,Term a)] > Bool
Checks whether a term rewriting system is leftnormal. 
isRedex
:: [(Term a,Term a)] > Term a > Bool
Checks whether a term is reducible with some rule of the given term rewriting system. 
isPattern
:: [(Term a,Term a)] > Term a > Bool
Checks whether a term is a pattern, i.e., an rootreducible term where the argaccording to the given term rewriting system. 
isConsBased
:: [(Term a,Term a)] > Bool
Checks whether a term rewriting system is constructorbased. 
isDemandedAt
:: Int > (Term a,Term a) > Bool
Checks whether the given argument position of a rule is demanded. 
A rule represented as a pair of terms and parameterized over the kind of function symbols, e.g., strings.
Type synonym: Rule a = (Term a,Term a)
A term rewriting system represented as a list of rules and parameterized over the kind of function symbols, e.g., strings.
Type synonym: TRS a = [Rule a]
Transforms a rule into a string representation. 
Transforms a term rewriting system into a string representation. 
Returns the root symbol (variable or constructor) of a rule.

Returns the maximum variable in a rule or 
Returns the minimum variable in a rule or 
Returns the maximum variable in a term rewriting system or 
Returns the minimum variable in a term rewriting system or 
Renames the variables in a rule by the given number. 
Renames the variables in every rule of a term rewriting system by the given number. 
Normalizes a rule by renaming all variables with an increasing order, starting from the minimum possible variable. 
Normalizes all rules in a term rewriting system by renaming all variables with an increasing order, starting from the minimum possible variable. 
Checks whether the first rule is a variant of the second rule. 
Checks whether a term rewriting system is leftlinear. 
Checks whether a term rewriting system is leftnormal. 
Checks whether a term is reducible with some rule of the given term rewriting system. 
Checks whether a term is a pattern, i.e., an rootreducible term where the argaccording to the given term rewriting system. 
Checks whether a term rewriting system is constructorbased. 
Checks whether the given argument position of a rule is demanded. Returns
