This processor always returns the answer Yes(?,?).

This processor always returns the answer No.

This processor always returns the answer Maybe.

This processor returns the answer Yes(O(1),(1)) if the strict component is empty.

This processor implements arctic interpretations.

This processor implements matrix interpretations.

Options for simple polynomial interpretations.

Options for linear polynomial interpretations.

Options for strongly linear polynomial interpretations.

Options for simple mixed polynomial interpretations.

Options for quadratic mixed polynomial interpretations.

Option for polynomials of custom shape, as defined by the first argument. This function receives a list of variables denoting the n arguments of the interpretation function. The return value of type [SimpleMonomial] corresponds to the list of monomials of the constructed interpretation function. A polynomial is a list of unique SimpleMonomial, where SimpleMonomial are considered equal if the set variables together with powers match. SimpleMonomial can be build using ^^^, constant and mono. For instance, linear interpretations are constructed using the function vs -> [constant] ++ [ v^^^1 | v <- vs] .

A SimpleMonomial denotes a monomial with variables in Variable, and can be build using ^^^, constant and mono.

v ^^^ k denotes exponentiation of variable v with constant k.

mono [v1^^^k1,...,vn^^^kn] constructs the SimpleMonomial c * v1^k1 * ... * v1^kn where c is unique for the constructed monomial.

Returns a new monomial whose coefficient is guaranteed to be 0 or 1.

Returns a new monomial without variables.

This parameter defines the shape of the matrix interpretations, and how the induced complexity is computed.

The shape of polynomial interpretations.

This processor implements polynomial path orders.

This processor implements polynomial path orders with parameter substitution.

This processor implements lightweight multiset path orders.

This processor implements small polynomial path orders (polynomial path orders with product extension and weak safe composition) which allow to determine the degree of the obtained polynomial certificate.

This processor is like popstarSmall but incorporates parameter substitution addidionally.

This processor implements multiset path orders.

This processor implements the bounds technique.

This datatype represents the enrichment employed.

This datatype represents the initial automaton employed.

ite g t e applies processor t if processor g succeeds, otherwise processor e is applied.

step [l..u] trans proc successively applies the transformations [trans l..trans u] , additionally checking after each application of trans i whether proc i can solve the problem. More precise step [l..] trans proc == proc l `before` (trans l >>| (proc l `before` (trans l >>| ...))) . The resulting processor can be infinite.

upto mkproc (b :+: l :+: u) == f [ mkproc i | i <- [l..u]] where f == fastest if b == True and f == sequentially otherwise.

'named name proc' acts like proc, but displays itself under the name name in proof outputs

The processor p1 before p2 first applies processor p1, and if that fails processor p2.

The processor p1 orBetter p2 applies processor p1 and p2 in parallel. Returns the proof that gives the better certificate.

The processor p1 orFaster p2 applies processor p1 and p2 in parallel. Returns the proof of that processor that finishes fastest.

List version of before.

List version of orBetter. Note that the type of all given processors need to agree. To mix processors of different type, use some on the individual arguments.

List version of orFaster. Note that the type of all given processors need to agree. To mix processors of different type, use some on the individual arguments.

Determines which components of a problem should be checked.

The processor t >>| p first applies the transformation t. If this succeeds, the processor p is applied on the resulting subproblems. Otherwise t >>| p fails.

Similar to >>| but checks if strict rules are empty

Like >>| but resulting subproblems are solved in parallel by the given processor.

Similar to >>|| but checks if strict rules are empty

On innermost problems, this processor removes inapplicable rules by looking at non-root overlaps.

Uncurrying for full and innermost rewriting. Note that this processor fails on dependency pair problems.

This processor implements the weightgap principle.

This transformation implements techniques for splitting the complexity problem into two complexity problems (R) and (S) so that the complexity of the input problem can be estimated by the complexity of the transformed problem. The processor closely follows the ideas presented in Complexity Bounds From Relative Termination Proofs (http://www.imn.htwk-leipzig.de/~waldmann/talk/06/rpt/rel/main.pdf).

same as decompose with DecomposeBound Add, but the transformation results in two sub-problems, instead of applying a given processor on the selected sub-problem

decomposeAnyWith == decompose (selAnyOf selStricts) Add.

Using the decomposition processor (c.f. decomposeBy) this transformation decomposes dependency pairs into two independent sets, in the sense that these DPs constitute unconnected sub-graphs of the dependency graph. Applies cleanSuffix on the resulting sub-problems, if applicable.

Similar to decomposeIndependent, but in the computation of the independent sets, dependency pairs above cycles in the dependency graph are not taken into account.

Implements dependency pair transformation. Only applicable on runtime-complexity problems.

Implements dependency tuples transformation. Only applicable on innermost runtime-complexity problems.

Path Analysis

Variation of pathAnalysis that generates only a linear number of sub-problems, in the size of the dependency graph

Moves a strict dependency into the weak component if all predecessors in the dependency graph are strict and there is no edge from the rule to itself.

This processor implements processor 'dependency graph decomposition'. It tries to estimate the complexity of the input problem based on the complexity of dependency pairs of upper congruence classes (with respect to the congruence graph) relative to the dependency pairs in the remaining lower congruence classes. The overall upper bound for the complexity of the input problem is estimated by multiplication of upper bounds of the sub problems. Note that the processor allows the optional specification of processors that are applied on the two individual subproblems. The transformation results into the systems which could not be oriented by those processors.

This is the default RuleSelector used with decomposeDG.

Specify a processor to solve the upper component immediately. The Transformation aborts if the problem cannot be handled.

Specify a processor to solve the lower immediately. The Transformation aborts if the problem cannot be handled.

Specify how the lower component should be selected.

Removes trailing weak paths. A dependency pair is on a trailing weak path if it is from the weak components and all sucessors in the dependency graph are on trailing weak paths.

Only applicable on DP-problems as obtained by dependencyPairs or dependencyTuples. Also not applicable when strictTrs prob = Trs.empty.

Removes unnecessary roots from the dependency graph.

Checks whether the DP problem is trivial, i.e., does not contain any cycles.

Only applicable on DP-problems as obtained by dependencyPairs or dependencyTuples. Also not applicable when strictTrs prob = Trs.empty.

Removes inapplicable rules in DP deriviations.

Currently we check whether the left-hand side is non-basic, and there exists no incoming edge except from the same rule.

Simplifies right-hand sides of dependency pairs. Removes r_i from right-hand side c_n(r_1,...,r_n) if no instance of r_i can be rewritten.

Only applicable on DP-problems as obtained by dependencyPairs or dependencyTuples. Also not applicable when strictTrs prob = Trs.empty.

The transformer try t behaves like t but succeeds even if t fails. When t fails the input problem is returned.

The transformer force t behaves like t but fails always whenever no progress is achieved.

The transformer t1 >>> t2 first transforms using t1, resulting subproblems are transformed using t2.

The transformer t1 <> t2 transforms the input using t1 if successfull, otherwise t2 is applied.

The transformer t1 <||> t2 applies the transformations t1 and t2 in parallel, using the result of whichever transformation succeeds first.

The transformer exhaustively t applies t repeatedly until t fails. exhaustively t == t >>> try (exhaustively t).

Shorthand for 'try . exhaustively'

List version of >>>.

 successive [t_1..t_n] == t_1 >>> .. >>> t_n

Transformation 'when b t' applies t only when b holds

Identity transformation.

Tries dependency pairs for RC, and dependency pairs with weightgap, otherwise uses dependency tuples for IRC. Simpifies the resulting DP problem as much as possible.

Fast simplifications based on dependency graph analysis.

tries to remove leafs in the congruence graph, by (i) orienting using predecessor extimation and the given processor, and (ii) using removeWeakSuffix and various sensible further simplifications. Fails only if (i) fails.

use simpPEOn and removeWeakSuffix to remove leafs from the dependency graph. If successful, right-hand sides of dependency pairs are simplified (simpDPRHS) and usable rules are re-computed (usableRules).

This datatype defines a specific instance of a transformation.

This class establishes a mapping between types and their existential quantified counterparts.

Wrap an object by existential quantification.