A termination method (TM) is a function which yields true if a given term rewrite system terminates and false otherwise.
A termination method (TM) is a function which yields true if a given term rewrite system terminates and false otherwise.
Only added to generate scaladoc for completion correctly :(
Returns (E',R',C) where all left-hand sides of rules from R with indices in is are reduced one step with respect to R without the collapsed rule itself and then moved to E.
Returns (E',R',C) where all left-hand sides of rules from R with indices in is are reduced one step with respect to R without the collapsed rule itself and then moved to E.
a list of indices in R
a triple (E,R,C) where E is an equational system, R is a term rewrite system, and C is a constraint term rewrite system
Returns (E',R',C) where all left-hand sides of rules from R with indices in is are reduced to normal form with respect to R without the collapsed rule itself and then moved to E.
Returns (E',R',C) where all left-hand sides of rules from R with indices in is are reduced to normal form with respect to R without the collapsed rule itself and then moved to E.
a list of indices in R
a triple (E,R,C) where E is an equational system, R is a term rewrite system, and C is a constraint term rewrite system
Returns (E,R',C) where all right-hand sides of rules from R with indices in is are reduced one step with respect to R without the reduced rule itself.
Returns (E,R',C) where all right-hand sides of rules from R with indices in is are reduced one step with respect to R without the reduced rule itself.
a list of indices in R
a triple (E,R,C) where E is an equational system, R is a term rewrite system, and C is a constraint term rewrite system
Returns (E,R',C) where all right-hand sides of rules from R with indices in is are reduced to normal form with respect to R without the reduced rule itself.
Returns (E,R',C) where all right-hand sides of rules from R with indices in is are reduced to normal form with respect to R without the reduced rule itself.
a list of indices in R
a triple (E,R,C) where E is an equational system, R is a term rewrite system, and C is a constraint term rewrite system
Returns (E',R,C) where all critical pairs between left-hand sides of rules from R with indices in is are added to E.
Returns (E',R,C) where all critical pairs between left-hand sides of rules from R with indices in is are added to E.
a list of indices in R
a triple (E,R,C) where E is an equational system, R is a term rewrite system, and C is a constraint term rewrite system
Returns (E',R,C) where all critical pairs between the left-hand side of the rule from R with index i and all left-hand sides of rules in R are added to E.
Returns (E',R,C) where all critical pairs between the left-hand side of the rule from R with index i and all left-hand sides of rules in R are added to E.
an index in R
a triple (E,R,C) where E is an equational system, R is a term rewrite system, and C is a constraint term rewrite system
Returns (E',R,C) where all critical pairs between the left-hand side of the rule from R with index i and all left-hand sides of rules in R are added to E.
Returns (E',R,C) where all critical pairs between the left-hand side of the rule from R with index i and all left-hand sides of rules in R are added to E.
an index in R
a triple (E,R,C) where E is an equational system, R is a term rewrite system, and C is a constraint term rewrite system
Returns (E',R,C) where all trivial equations from E with indices in is are removed from E.
Returns (E',R,C) where all trivial equations from E with indices in is are removed from E.
A trivial equation is an equation where the left-hand side is the same as the right-hand side.
a list of indices in E
a triple (E,R,C) where E is an equational system, R is a term rewrite system, and C is a constraint term rewrite system
Returns true if rs is complete and has the same conversion as es and false otherwise.
Returns true if rs is complete and has the same conversion as es and false otherwise.
Returns the result from orientLR if it changed the triple (E,R,C) and the result from orientRL otherwise.
Returns the result from orientLR if it changed the triple (E,R,C) and the result from orientRL otherwise.
a list of indices in E
a triple (E,R,C) where E is an equational system, R is a term rewrite system, and C is a constraint term rewrite system
the used termination method
Returns the triple (E',R',C') where equations in E with indices in is are oriented from left to right into rewrite rules and moved to R using the termination method tm and the unchanged triple (E,R,C) if not all equations with indices in is could be oriented from left to right using tm.
Returns the triple (E',R',C') where equations in E with indices in is are oriented from left to right into rewrite rules and moved to R using the termination method tm and the unchanged triple (E,R,C) if not all equations with indices in is could be oriented from left to right using tm.
a list of indices in E
a triple (E,R,C) where E is an equational system, R is a term rewrite system, and C is a constraint term rewrite system
the used termination method
Returns the triple (E',R',C') where equations in E with indices in is are oriented from right to left into rewrite rules and moved to R using the termination method tm and the unchanged triple (E,R,C) if not all equations with indices in is could be oriented from right to left using tm.
Returns the triple (E',R',C') where equations in E with indices in is are oriented from right to left into rewrite rules and moved to R using the termination method tm and the unchanged triple (E,R,C) if not all equations with indices in is could be oriented from right to left using tm.
a list of indices in E
a triple (E,R,C) where E is an equational system, R is a term rewrite system, and C is a constraint term rewrite system
the used termination method
Returns (E',R,C) where all left- and right-hand sides of equations from E with indices in is are reduced one step with respect to R.
Returns (E',R,C) where all left- and right-hand sides of equations from E with indices in is are reduced one step with respect to R.
a list of indices in E
a triple (E,R,C) where E is an equational system, R is a term rewrite system, and C is a constraint term rewrite system
Returns (E',R,C) where all left- and right-hand sides of equations from E with indices in is are reduced to normal form with respect to R.
Returns (E',R,C) where all left- and right-hand sides of equations from E with indices in is are reduced to normal form with respect to R.
a list of indices in E
a triple (E,R,C) where E is an equational system, R is a term rewrite system, and C is a constraint term rewrite system
Provides functions needed for a completion procedure.
Such a procedure takes as input a set of equations E and a termination method and attempts to cunstruct a terminating and confluent, i.e. complete, term rewrite system R which has the same set of convertible terms as E.
Completion is implemented as an inference system. The rules of which operate on a triple (E,R,C) and return a new triple (E',R',C'). Here E is a set of equations, R a set of rewrite rules, and C a constraint term rewrite system used to allow other termination methods besides reduction orderings.