a label for semantic labeling is used as a function symbol in terms, orderings, .... first term is lhs, second term is rhs a rule can either be spelled out or just be referenced by some index. all rule indices have to occur in the global /certificationProblem/lookupTables/ruleTable map. first term is lhs, second term is rhs first term is lhs, second term is rhs the algebraic number (a,b,c) represents the number a + b * sqrt(c) list of row-vectors list of column-vectors note that this max is only used for min-max interpretations and not for arctic... interpretations. For example, in arctic one has to use plus and not max. note that this min is only used for min-max interpretations and not for arctic... interpretations. For example, in arctic one has to use plus and times, but neither min nor max. note that when using polynomials over a vector-domain, then the constant coefficient is a vector whereas the other coefficients are matrices. Moreover, in this case only linear polynomials are allowed. an argument filter consist of a mapping from symbols to collapsing or non-collapsing filters. Example: an entry f/3 -> collapsing/1 filters the ternary symbol f to its third argument. an entry f/3 -> nonCollapsing/3 1 filters the term f(x,y,z) to f(z,x) often for nonCollapsing filters the positions are given in increasing order. However, argument filters can also be used to simulate permutations e.g. to express some LPOS by an LPO an argument filter. Note that the arities within the status precedence entries in combination with argument filters correspond to the unfiltered arities. E.g., if the second argument of f/3 is dropped then the status precedence entry still has to give arity 3 to f. purpose: -arctic below zero is arctic-integer -bounded increase is over integers the domain of matrices where the elements are from the subdomain specified in the upper left submatrix of this dimension there must be a strict decrease (the remaining parts of the matrix is ignored for strict decreases, only weak decreases are required). standard polynomial orders over a specified domain (a semiring or something else). Note that if the domain is "matrices of naturals" then everything has to be a matrix, even the constants. This is in contrast to "matrixInterpretations" where the constants are vectors. the maximal degree of the polynomial interpretation (some certifiers only support linear interpretations). all interpretations given should respect this degree. matrix interpretations where the elements are vectors. Example: if the domain is naturals, then the coefficients in front of variables have to be matrices and the constants should be vectors over the naturals. in the upper subvector of this dimension there must be a strict decrease (the lower part of the vector is ignored for strict decreases, only weak decreases are required). Matrix interpretations where the elements are matrices. Note that not all non-negative matrices are in the domain, but these have to be explicitly defined, as described in "Termination of String Rewriting with Matrix Interpretations" by Hofbauer and Waldmann. For the moment, only integer matrices are supported. The indices I have to be explicitly provided, and the selected domains E_I or M_I can be selected by mode E or M. Note that interpretations are still full linear expressions and not just singleton matrices. E.g., if [a] = A for some letter a of an SRS and matrix A (notation in paper), then in CPF, one would have to specify an interpretation such as [a/1] = A * x_1. specify list of indices I; each index must be between 1 and n, where n is the dimension of the matrices. TODO: describe TODO: describe recursive path order in its general form, i.e., RPO, MPO, LPO, LPO with status (arbitrary order of arguments), RPO with status Note that the arities within the status precedence entries in combination with argument filters correspond to the unfiltered arities. E.g., if the second argument of f/3 is dropped then the status precedence entry still has to give arity 3 to f. higher numbers = higher precedence. Unspecified symbols obtain precedence 0. to realize permutations for lex. comparisons, use an argument filter, which just permutes. Eg., right-to-left precedence of f(x,y,z) where the second argument is dropped, is done by argument filter f -> [3,1] To realize permutations for lex. comparisons, one has to use an argument filter, which can just permute. Eg., right-to-left precedence of f(x,y,z) where the second argument is dropped, is done by argument filter f -> [3,1] Note that the arities within the precedence weight entries in combination with argument filters correspond to the unfiltered arities. E.g., if the second argument of f/3 is dropped then the weight precedence entry still has to give arity 3 to f. higher numbers = higher precedence. Unspecified symbols obtain precedence 0. To realize permutations for lex. comparisons, one has to use an argument filter, which can just permute. Eg., right-to-left precedence of f(x,y,z) where the second argument is dropped, is done by argument filter f -> [3,1] Note that the arities within the precedence weight entries in combination with argument filters correspond to the unfiltered arities. E.g., if the second argument of f/3 is dropped then the weight precedence entry still has to give arity 3 to f. higher numbers = higher precedence. Unspecified symbols obtain precedence 0. To realize permutations for lex. comparisons, one has to use an argument filter, which can just permute. Eg., right-to-left precedence of f(x,y,z) where the second argument is dropped, is done by argument filter f -> [3,1] position 0 encodes the argument "full term" Note that the arities within the status precedence entries in combination with argument filters correspond to the unfiltered arities. E.g., if the second argument of f/3 is dropped then the status precedence entry still has to give arity 3 to f. If no lex/mul argument is given, then the default is used: lex. higher numbers = higher precedence. Unspecified symbols obtain precedence 0. to realize permutations for lex. comparisons, use an argument filter, which just permutes. Eg., right-to-left precedence of f(x,y,z) where the second argument is dropped, is done by argument filter f -> [3,1] Note that the arities within the status precedence entries in combination with argument filters correspond to the unfiltered arities. E.g., if the second argument of f/3 is dropped then the status precedence entry still has to give arity 3 to f. For co-WPO only lex is supported. higher numbers = higher precedence. Unspecified symbols obtain precedence 0. higher numbers = higher precedence. Unspecified symbols obtain precedence 0. Define a reduction pair with the help of an argument filter. Note that the arities change, e.g., when the argument filter assigns a ternary f the list [1,3], then in the reduction pair f has arity 2. To realize permutations for lex. comparisons, one has to use an argument filter, which can just permute. Eg., right-to-left precedence of f(x,y,z) where the second argument is dropped, is done by argument filter f -> [3,1] reduction orders with a special feature, namely ground joinability testing a la Martin and Nipkow (1990) For Martin and Nipkow's testing, the precedence > must be injective, i.e., f > g or g > f for all different function symbols f, g. Note that the arities within the precedence weight entries in combination with argument filters correspond to the unfiltered arities. E.g., if the second argument of f/3 is dropped then the weight precedence entry still has to give arity 3 to f. higher numbers = higher precedence. Unspecified symbols obtain precedence 0. semantics: ifEqual f1 f2 ft fe checks whether f1 and f2 evaluate to the same element. If so, the result is the one of ft, otherwise it is the result of fe. The carrierSize determines the carrier. A size of n fixes the carrier to {0,1,...,n-1}. If no labeling is given, then every symbol is labeled by the interpretation of the arguments If this element is missing, then one uses semantic labeling in the model version. Otherwise, semantic labeling is applied with a quasi-model where one uses a tuple extension of the standard order > on the naturals. However, there can be several such extensions, e.g., point-wise, lexicographic (w.r.t. permutation), ... here, (x1,..,xn) > (y1,...,yn) iff all xi >= yi and for some i: xi > yi labeling domain and functions for semantic labeling. This feature is currently unsupported and not specified. It is only present to state that this entry might come in the future. Normally for root-labeling there is no argument. However, if root-labeling is applied in the DP-setting after FC1 has been applied, one might want to treat the blocking symbol in a special way by dropping it from the carrier. If and only if this alternative is chosen, the blocking symbol must be present as argument. A renaming of symbols. The entries are of the form (old_symbol, new_symbol) term, pumping subst., closing subst the pattern terms are the lhs and rhs of the pattern rule. the third argument is the proof how to derive the pattern rule. first substitution is for lhs, second for rhs. first substitution is pumping, second is closing first substituion is for base, second is new closing subst. first pattern rule is rewritten with second pattern rule a string as used for string rewriting state that u ->+ v. The strings u v must be provided in combination with a proof. derive w l -> t r from w -> t x and x l -> r The strings t, x, and l have to be provided (in this order) to ease proof reconstruction. derive l w -> r t from w -> x t and l x -> r The strings x, t, and l have to be provided (in this order) to ease proof reconstruction. derive w -> t1 r t2 from w -> t1 x t2 and x -> r The strings t1 and t2 have to be provided (in this order) to ease proof reconstruction. derive t1 w t2 -> r from t1 x t2 -> r and w -> x The strings t1 and t2 have to be provided (in this order) to ease proof reconstruction. derive l^n c ->+ c r^n from overlap-closure l c ->+ c r derive c l^n ->+ r^n c from overlap-closure c l ->+ r c derive l1 m1^(f1*n+(c1+f1)) r1 ->+ l2 m2^(f2*n+(c2+f2)) r2 from l1 m1^(f1*n+c1) r1 ->+ l2 m2^(f2*n+c2) r2 derive pat ->+ l v r m^n r' from pat ->+ l x r m^n r' and x ->+ v The strings l and r have to be provided. derive l l1 m1^n r1 ->+ v r m2^n r2 from l1 m1^n r1 ->+ x r m2^n r2 and l x ->+ v The strings l, r, and x have to be provided. derive pat ->+ l' (l v r)^n r' from pat ->+ l' (l x r)^n r' and x ->+ v The strings l and r have to be provided. derive pat ->+ l' m^n l v r from pat ->+ l' m^n l x r and x ->+ v The strings l and r have to be provided. derive l1 m1^n r1 r ->+ l2 m2 l v from l1 m1^n r1 ->+ l2 m2^n l x and x r ->+ v The strings l, r, and x have to be provided. derive pat ->+ l l2 m2^n r2 r from pat ->+ l l1 m1^n r1 r and l1 m1^n r1 ->+ l2 m2^n r2 The strings l and r have to be provided. derive l1 m1^n r1' r ->+ l l2' m2^n r2 from l1 m1^n r1' ->+ l l2 m^n r1 and l2 m^n r1 r ->+ l2' m2^n r2 The strings l and r have to be provided. derive l l1' m1^n r1 ->+ l2' m2^n r2' r from l1' m1^n r1 ->+ l1 m^n r2 r and l l1 m^n r2 -> l2' m2^n r2' The strings l and r have to be provided. derive l l1' m'^n r1' r ->+ pat from l1' m'^n r1' ->+ l1 m1^n r1 and l l1 m1^n r1 r ->+ pat The strings l and r have to be provided. derive patl ->+ patr from patl' ->+ patr' since patl and patl' are equivalent word patterns and patr and patr' are equivalent word patterns. a list of generated derivation patterns in chronological order, i.e., the i-th proof step may be based on all derivation patterns that have been generated in steps 1 to i-1. there is a loop, as we have generated an overlap closure m ->+ l m r. The strings l, m, and r must be given in this order. There is a self-embedding derivation pattern l m^f1 r ->+ l' l m^f2 r r' such that f1 and f2 are fitting. l' and r' have to be provided. if t_0 is startterm, and there are rewrite-steps p_i, rule_i, t_i (for i = 1..n) then t_{i-1} ->_{p_i,rule_i} t_i for all i=1..n If the rewrite sequence is built via two TRSs, where one corresponds to a major step, and the other corresponds to a relative step, then all relative steps have to be marked with the relative-elemnt. (e.g., for loops in relative termination analysis R/S, the S-steps are relative, or for loops in the DP-framework with (P,R), the R-steps are relative). the state of a tree automation the uncurrying information consists of: - the application symbol - the names of the uncurried symbols - the uncurrying rules - the additional rules that are obtained when eta-expanding the TRS mark for each original symbols the new uncurried symbols: if the constant map should now be uncurried up to two levels then there should be a symbol map entry map (we want to uncurry map) 0 (the original arity of map) map (the new constant) map1 (the new unary symbol) map2 (the new binary symbol) Note that the names can be chosen arbitrarily a loop is given by a (non-empty) rewrite-sequence t0 ->+ tn where additionally tn = C[t0 sigma] first substitution is part of pumping subst., second substitution is part of closing subst., first natural is for decomposing pumping subst., second natural is for getting subterm This is the standard problem for the TRS categories of termComp. This input can model (innermost/outermost/...) (relative) termination and complexity problems. Note that CeTA only supports relative systems for no strategy or for innermost strategies. no strategy means standard rewriting without restrictions A conversion of the first term to the last term, with intermediate terms spelled out. CeTA tries to infer parallel rewrite steps between every two adjacent terms in the list. If no sigature is provided, then signature is set of symbols of input TRS. first signature defines constructors, second signature the defined symbols; if no signatures are provided, then these are computed implicitly from input TRS R: roots of R will be defined symbols; all other symbols of R will be constructors a1 -> a2 -> ... -> an or (a1 /\ a2 /\ ... ) -> an pass this constraint to the order there is a rewrite constraint in the assumptions (which must be provided) which has different root symbols and the left root symbol is a constructor there is a rewrite constraint in the assumptions (which must be provided) which has the same root symbols which are constructors. Then for all arguments the rewrite constraints are added. Both the rewrite constraint and the full new constraint must be provided in combination with the proof for the new constraint. Arbitrary conditions can be dropped. The full new constraint must be provided in combination with the proof for the new constraint. There is a rewrite constraint x = t or t = x. The full new constraint must be provided in combination with the proof for the new constraint. There is a rewrite constraint f(t1,..,tn) = q where ti should be replaced by a fresh variable x + addition of ti = x. The rewrite constraint, the index, the variable name, and the full new constraint must be provided in combination with the proof for the new constraint. Use a induction hypothesis (a quantified implification in the list of premises). The quantified formula, the instantiation substitution, and the new total constraint must be provided in combination with the proof for the new constraint. Use the induction rule. The rewrite condition + the list of conjuncts must be provided (which corresponds to phi in the paper) for each rule that must be considered, a variable renamed rule has to be provided + the set of subterms of the rhs, for which an IH is generated + the bound variables for building each IH + the new total constraint for that rule + the proof for that new constraint the number is the degree: 0 -> O(1) 1 -> O(n) 2 -> O(n^2) ... The final states are those which are used to accept the initial language like lift_0(T(Sigma)). In the relative setting, an implicit step from R/S to R u S is done! One has to provide which criterion was used to ensure closure under rewriting. For backwards-compatibility, the criterion is optional as in former versions there was only compatibility (of Genet). So, if no criterion is provided, this should be interpretet as compatibility. It is encouraged to specify the criterion explicitly. state that the strict TRS is empty and therefore is in O(1). shifts a set of rules from strict to weak component where all these rules are oriented by some monotone reduction order where the complexity of the order is known. An optional set of usable rules may be provided, then only these rules will have to be oriented. Since there is no special treatment for dependency-pairs or -tuples, these rules have to be included in the list of usable rules! remove those rules, which are not applicable since their lhs has an argument that is not in normal form (for innermost rewriting). The removed rules have to be provided. apply relative match-bounds to move some rules from the strict in the weak component. The moved rules have to be provided. Apply the dependency tuple transformation for complexity. For each rule one has to provide a corresponding DT. The strict and weak rules give rise to strict and weak DTs, resp. The innermost left-hand sides should contain terms with sharp-symbols as root. They will be added to the strategy component, and they can be used to ensure that the resulting problem is again innermost. Requires innermost runtime complexity problems as input. Turns the set of starting terms into T#. Only the strict DTs will be strict afterwards, and all other rules and DTs will be in the weak component. Apply the weak dependency pairs transformation for complexity. For each rule one has to provide a corresponding WDP. The strict and weak rules give rise to strict and weak WDPs, resp. The innermost left-hand sides should contain terms with sharp-symbols as root. They will be added to the strategy component, and they can be used to ensure that the resulting problem is again innermost, if the original problem was innermost. Requires runtime complexity problems as input. Turns the set of starting terms into T#. Only consider usable rules, where usable rules usually are determined via usable symbols. Note that those rules have to be provided which are not usable, and can thus be deleted. Split a complexity problem (S1 union S2 / W) into the two problems P1 = (S1 / S2 union W) and P2 = (S2 / S1 union W). The TRS S1 has to be provided as well as the proofs of P1 and P2 (in this order). Show that a given set of equations E is equivalent to a TRS R, by showing that all rules can be derived from the equations and vice versa. The first subsumption proof is mandatory (where the rules have to be derived from the equations), the latter is optional and may be automatically be performed by the certifier. Show that a given set of equations E is subsumed by a TRS R, by showing that all equations can be derived from the rules. This format is more convenient and suitable than completionProof if the purpose is equational disproof. Subsumption proof is optional and may be automatically be performed by the certifier. Rule labeling function as pairs of rules and natural numbers. Unspecified rules get label 0. CR, since the TRS is (left-)linear and all critical peaks are decreasing using rule labeling. CR, since the TRS is (left-)linear and all critical peaks are decreasing using rule labeling (conversion version). Peaks have to be specified in the critical pairs and it is recommended to also provide the labels of a critical peak. Indicates a limit in how many steps the fan property can be shown. A many-sorted signature. Each function symbol is associated with a list of argument types and a result type. We nearly always consider peaks of the form left <- peak -root-> Only exception: for simultaneous critical pairs we consider peaks of the form left <-o- peak -> right, i.e., where the multistep leads to the left and the single step to the right.) The intermediate terms t1, .., tn are those that occur in the joining conversion of form left <-> t1 <-> ... <-> tn <-> right. All non-trivial peaks must be listed, i.e., where left and right differ. For rule labeleling, the (maximal) label of the (parallel) step must be indicated (maxLeft) as well as the label of the root step (right). When using parallel critical pairs, the peaks and the posititions of the overlap have to be specified. The joins can be done within a given number of steps. Note that CPF version 2 had the option to specify no number for a default, e.g., try a join with a parallel step or development step. These defaults are still available by using a negative number as limit. Note that this method is not complete if the TRS(s) contain extra-variables, or if conversions are allowed. CR (or commuting), since the TRS (s) satisfy Gramlich's parallel critical pair condition (incl. Toyama's refinement). CR, since TRS is strongly closed. The number indicates a limit in how many steps each critical pair can be joined. CR, since TRS is parallel closed. The number indicates a limit on the length of the rewrite sequences in the joins. The first labeling function is phi. The second one is psi. If psi is not provided, psi is set to phi. Note that two sets of joining operations must be given, one where the phi-labelled-rules are for the parallel steps and psi-rules for root steps (joinsRS), and one where the role of phi and psi is flipped (joinsSR). If psi is not provided (so phi = psi), then the joinsSR element can be omitted. Only the non-0-0 joins have to be decreasing. And the 0-labeled subsystems must be provided explicitly and will be handled recursively in the child CR-proof. Provide the subtrs C and hints for joining the parallel critical pairs of R by conversions of C. In the auto mode with parameter n, it is tried to merge critical pairs (t,u) by joins with n steps from both sides. Provide the subtrs C of R and the parallel pair closing system P. Moreover a relative termination proof of P / R is required. The second cpJoinHints are used for joining the parallel critical pairs by R, and the first cpJoinHints are for joining these pairs by C, so that they don't have to be added to P. CR, since TRS is development closed. CR, since the TRS is simultaneous critical pairs closed (Okui's criterion). In the join hints the step to the right is always the single step. Trivial critical pairs can be omitted. It is preferred to not use the auto-mode, but instead explicitly list the critical pairs. CR, since there is terminating critical-pair-closing system for the TRS. Termination of the duplicating rules relative to the non-duplicating ones; required if the TRS is not right-linear. Indicates a limit in how many steps each rule can be simulated. A confluence proof by persistent decomposition. Confluence follow from confluence of the maximal systems induced by the sorts of the specified many-sorted signature. the TRSs R and S are not commuting as there are two rewrite sequences starting from the same term which cannot be joined. The first rewrite sequence is the one of S leading to term s, the second rewrite sequence is the one of R leading to t, and the third argument is the reason why a of join of s and t is not possible via rewriting with R and S. Change the role of the two TRSs. the TRSs R and S are commuting as they are (almost) parallel closed. Note that the criterion is not symmetric, therefore, you might need to swap the role of the two TRSs. The number indicates a limit on the length of the rewrite sequences in the joins. the TRSs R and S are commuting as they are (almost) development closed. Note that the criterion is not symmetric, therefore, you might need to swap the role of the two TRSs. The number indicates a limit on the length of the rewrite sequences in the joins. The TRSs R and S are commuting as they all simultaneous critical pairs of R and S are closed, i.e., whenever u <-o,R- . -S-> v is a simultaneous critical pair, then u -S->* . <-o,R- v. Note that the criterion is not symmetric, therefore, you might need to swap the role of the two TRSs. It is recommened to provide explicit joining sequences. The first labeling function is for TRS R. The second one is for TRS S. If the second one is not provided, then the same function is used for both TRSs. Note that two set of joining operations must be given, one where the R-rules are for the parallel steps and S-rules for root steps (joinsRS), and one where the role of R and S is flipped (joinsSR). The first labeling function is for TRS R. The second one is for TRS S. If the second one is not provided, then the same function is used for both TRSs. Note that two set of joining operations must be given, one where the R-rules are for the parallel steps and S-rules for root steps (joinsRS), and one where the role of R and S is flipped (joinsSR). Only the non-0-0 joins have to be decreasing. And the 0-labeled subsystems will be handled recursively. The first "trs"-element is the sub-trs of R, and the second one is the one of S. some commutation criteria are only available in a non-symmetric version, e.g., being almost parallel closed. Since commutation is a symmetric property, this technique can be used to change the role of the two TRSs before applying an asymmetric criterion. Provide the subtrs C of R and D of S and the parallel pair closing system P. Moreover a relative termination proof of P / (R union S) is required. The first cpJoinHints are used for joining the parallel critical pairs of R and S by C and D so that they don't have to be added to P. The second cpJoinHints are similar to the first ones with R and S swapped. The third cpJoinHints are used for joining the parallel critical pairs of R and S and the forth for the pairs of S and R. prove commutation by confluence, since R and S are identical just claim that some critical pair is not joinable. the TRS is not confluent as there are two rewrite sequences starting from the same term which cannot be joined. The third argument is the reason why a join is not possible. Considers two terms s and t and shows that s and t are not joinable w.r.t. some TRS. Note that in contrast to a nonjoinabilityProof, here no substitution is applied to s and t. the input TRS is a disjoint union R union S. By modularity of confluence, it suffices to disprove confluence of R. The TRS R has to be given. Indicates a limit in how many steps each rule can be simulated. A non-confluence proof by persistent decomposition. Non-confluence follow from nonconfluence of any of the systems induced by the sorts of the specified many-sorted signature. the TRS R is not confluent as one can remove some rules and show that the sub-system is not confluent. If S is the subsystem, then for each rule (l,r) in R-S where l only has symbols from S, one has to provide a l ->*S r rewrite sequence. Note that S is obtained from R by providing the list of deleted rules, i.e., R \ S must be part of the certificate. there are only finitely many terms reachable from both sides, and these sets are disjoint. the terms are distinct normal forms. after applying some cap-functions, the capped terms are not unifiable. Let s and t be two ground terms that should not be non-joinable w.r.t. TRSs Rs and Rt This is proved by giving some weakly monotone interpretation [.] and >=, such that - Rs^-1 and Rt are a quasi-model of the interpretation. - not [t] >= [s] This corresponds to Aoto/FroCoS 13/Thm 10, and it can simulate Thm 6 by choosing equality for >=. Note that the usable restriction to usable rules must be made explicitly before by applying the non-joinability technique usable-rules! This technique is tried symmetrically, i.e., (Rs,s) and (Rt,t) might be swapped. Let s and t be two ground terms that should not be non-joinable wrt. to TRSs Rs and Rt. This is proved by giving some discrimination pair >= and > (and an optional argument filter pi) such that - Rs^-1 and Rt are weakly decreasing - s > t This corresponds to Aoto/FroCoS 13/Thm 12 without usable rules. Note that the restriction to usable rules must be made explicitly before by applying the non-joinability technique usable-rules! Similarly, to get Thm 14, one has to also explicitly invoke the argument filter technique for non-joinability. This technique is tried symmetrically, i.e., (Rs,s) and (Rt,t) might be swapped. To show that s and t are not joinable w.r.t. Rs and Rt, use some argument filter pi and prove that pi(s) and pi(t) are not joinable w.r.t. pi(Rs) and pi(Rt). To realize permutations for lex. comparisons, one has to use an argument filter, which can just permute. Eg., right-to-left precedence of f(x,y,z) where the second argument is dropped, is done by argument filter f -> [3,1] To show that s and t are not joinable w.r.t. Rs and Rt, show that s and t are not joinable w.r.t. U(Rs,t) and U(Rt,t) where U is the set of usable rules w.r.t. reachability (cf. Aoto, FroCoS 13). Apply some grounding substition on both terms. Show that two subterms are not joinable. The position must be stable in both terms, i.e., there must not be any rewrite step possible above that position possible. Remove some rules and / or DPs to figure out the really nonterminating DP problem (removed rules and DPs are given). Note that this element can be used for several termination techniques like the dependency graph processor, or the various reduction pair processors. For innermost termination: remove those lhss from the innermost strategy component which contain symbols that do not occur in the remaining DP problem. The remaining set of lhss has to be given in the proof. Add new lhss to innermost strategy component. Switch from innermost rewriting to full/unrestricted rewriting for locally confluent TRS where there are no overlaps between pairs and rules. Instantiate several DPs. The set of new DPs has to be provided. Rewrite the rhs of some DP, if the usable rules of the redex are confluent. First rule: the original DP s -> t Rewrite step: the reduction from t to t' at position p Usable rules of t |_ p (optional) The second rule is also optional: it can be any variable renamed rule of s -> t' (which may be used in the new DP-problem instead) Narrow some DP by considering all narrowing below position p. trivial proof by stating that the set of DPs is empty split the current set of DPs into several smaller subproblems by using some DP-graph estimation. Note that all components of the graph have to be specified, including singleton nodes which do not form an SCC on their own. For the latter, no dpProof should be provided. The list of components has to be given in topological order, where the components with no incoming edges are listed first. Use a reduction pair where only the non-strict order has to be monotone. It allows to delete those DPs which are strictly oriented. The remaining DPs have to be given. Use a Ce-compatible reduction pair where only the non-strict order has to be monotone. It allows to delete those DPs which are strictly oriented. Here only the usable rules have to be weakly oriented. Use a reduction pair where both the non-strict and the strict order have to be monotone. It allows to delete those DPs and those rules of the TRSs which are strictly oriented. The removed DPs and rules of the TRS have to be given. Use a reduction pair where the monotonicity requirements are determined by an innermost usable replacement map. It allows to delete those DPs and those rules of the TRSs which are strictly oriented. The removed DPs and rules need to be provided. Use a Ce-compatible reduction pair where both the non-strict and the strict order have to be monotone. It allows to delete those DPs and those rules of the TRSs which are strictly oriented. Moreover, all non-usable rules will also be deleted. Here, only the usable rules instead of all rules of the TRS have to be oriented. The removed DPs and strictly oriented rules have to be given, as well as the usable rules. Use the subterm criterion to delete some DPs. Only collapsing argument filters or identity filters may be used. The removed DPs have to be given. The subterm criterion can also be used in combination with rewrite sequences. Instead of ar argument filters, one may also use multiset argument filters, where also non-sharp symbols can be projected. Then the projected rewrite sequences are forbidden. The removed DPs need to be listed. The rule specifies the DP for which the rewrite sequence is applied. Here, the rewrite sequence for the projected terms has to be given. Example: if s -> t is the DP and a rewrite sequence t_1 ->+ t_n is given then it must hold that pi(s) = t_1, and t_n contains pi(t) as a subterm. Use the semantic labeling processor to apply semantic labeling on both the DPs and the TRS. The model element determines the kind (model or quasi-model version, label, root-labeling, etc.). The decreasing rules should be of the form f_..(x1,..,xn) -> f_..(x1,..,xn), i.e., the variables should be enumerated from x1 onwards. The labeled system has to be provided where the new innermost strategy in the form of innermost left-hand-sides is only required if one had an innermost problem before. the size-change criterion processor. for each DP, one size-change graph has to be given. the set of graphs must be size-change terminating. if the size-change criterion is used in combination with the subterm criterion, then the edges in the graphs have to be built according to the subterm relation, and no rules have to be oriented. otherwise, for every existing edge in a size-change graph, the corresponding subterm on the rhs is considered as usable, and the corresponding usable rules have to be added to the set of usable rules. if not all rules are usable, then one has to use a Ce-compatible order. Example: DP: F(s(x),g(x)) -> F(id(x),g(x)) TRS: g(..) -> .. id(x) -> x if one builds a size-change graph where only the first arguments are connected, then one only has to add the id-rule to the set of usable rules, but not the g-rule. The usable rules are optional. If they are used, a Ce-compatible order has to be used. an edge in a size change graph is always of the form left-argument > / >= right-argument position 0 corresponds to the whole term. the flat context closure as required for the root labeling technique. one also has to provide the list of flat contexts which is used to fix the variable names in the resulting DP problem. see the flat context closure technique for TRS for more explanations including an example. just apply an argument filter and continue on the filtered DP problem To realize permutations for lex. comparisons, one has to use an argument filter, which can just permute. Eg., right-to-left precedence of f(x,y,z) where the second argument is dropped, is done by argument filter f -> [3,1] if applicativeTop does not exist, then one - eta-expands R, - uncurries P and R, - and adds the uncurrying rules to R (for the binary application symbol given in the uncurry information) if applicativeTop is present (some number n), then the intention is that the application symbol is a tuple/marked symbol of arity n. Then - the eta-expanded rules of R are added to P - one uncurries P and R - and adds the uncurrying rules to P For innermost termination: switch to usable rules For innermost termination: remove those lhss from the innermost strategy component which have a root that does not occur in the remaining DP problem. The remaining set of lhss has to be given in the proof. (One can also remove arbitrary lhss from the innermost strategy, but then minimality is not preserved) if R is WCR and has no overlaps with P, then one can switch to innermost Rewrite the rhs of some DP, if the usable rules of the redex are confluent. First rule: the original DP s -> t Rewrite step: the reduction from t to t' at position p Second rule: the new DP (can be variable renamed) Usable rules of t |_ p Instantiate some DP Instantiate some DP using forward instantiation. In the innermost case one can optionally give the set of usable rules for that DP which are then used to compute the reversed cap function. Narrow some DP by considering all narrowing below position p. Note that p must be a position of the capped rhs of the pair, and some other standard application conditions have to be considered. Split a DP problem (P,R) to show that certain pairs PD and rules RD cannot occur infinitely often. PD and RD have to given. Then it follows a proof for termination of the relative DP problem (PD, P - PD, RD, R - RD). Finally a termination proof of the DP problem (P - PD, R - RD) has to be given. Use a general reduction pair It returns two DP problems where once all strict and once all bound DPs are deleted (bound w.r.t. the given symbol). If only one proof is given, then the intersection of the bound and strict DPs are removed. - symbol is the constant symbol - before and after are numbers denoting how many DPs are considered before and after an DP in chain. - for each sequence of DPs one has to provide the initial constraint and a proof how to derive the final constraints from that. replace some ground term in rhs of pairs by a fresh variable, which is then added as additional argument to all pairs. Example, replacing 1000 by x may transform F(a,b,c) -> G(1000,f(1000),1000) may yield F'(a,b,c,x) -> G'(1000,f(x),x,x). In the proof, one has to provide the ground term and a list showing how each old pair is transformed into a new pair. as new pair. So not every occurrence of the ground term has to be replaced. For convenient certification, it required, that the fresh variable is always added as last argument. just convert DPs into ordinary rewrite rules there is a rule where the lhs is a variable, or the rhs contains variables not occurring in the lhs. Remove some rules to figure out the really nonterminating TRSs. The removed rules of R and of S need to be provided, first for R then for S. reverse the strings in a TRS, i.e., replace f(g(h(x))) -> f(x) by h(g(f(x))) -> f(x). Note that the variable in a reversed rule should be same as the variable in the original rule. apply the decision procedure for right-ground TRS to detect nontermination. there is a rule where the lhs is a variable, or the rhs contains variables not occurring in the lhs. Remove some rules to figure out the really nonterminating TRS. The removed rules need to be specified. reverse the strings in a TRS, i.e., replace f(g(h(x))) -> f(x) by h(g(f(x))) -> f(x). Note that the variable in a reversed rule should be same as the variable in the original rule. switch to DPs as complete termination technique. See dpTrans within dpProof for other details Add new lhss to innermost strategy component. Transform all constants into unary symbols. A renaming from the constants to the unary symbols has to be provided, in combination with the new TRS. Moreover, one has to provide a unique variable which is used for transforming ground rules. E.g., for a rule f(a) -> g(b), one needs to know the x in the resulting rule f(a(x)) -> g(b(x)). Switch from innermost rewriting to full/unrestricted rewriting for locally confluent overlay TRSs eta-expand the TRS, uncurry it, and add the uncurrying rules Show nontermination through a nonempty tree automaton that is closed under rewriting and does not accept normal forms. An (innermost) (relative) termination proof of R/S. Some proofs may implicitly turn R/S into R u S, e.g., dependency pairs. For all elements that require a new TRS, e.g., via transformation T where the natural new problem would be T(R) / T(S), the certificate just lists the new TRS T(R) union T(S), and the certifier will convert this to T(R) / T(S) internally. state that the R/S is relative terminating since R has no rules Use a reduction pair where both the weak and the strict ordering are monotone. Delete all strictly decreasing rules from R and S. The deleted rules have to be given. termination of the TRS can be proven by the decision procedure for right-ground TRSs Switch to dependency pairs. The dependency pairs have to be given, and one has to use sharped symbols. In the relative setting, an implicit step from R/S to R u S is done! Use semantic labeling. The model element determines the kind (model or quasi-model version, label, root-labeling, etc.). The decreasing rules should be of the form f_..(x1,..,xn) -> f_..(x1,..,xn), i.e., the variables should be enumerated from x1 onwards. The new TRS and if applicable the new innermost strategy in the form of left-hand-sides must be provided. reverse the strings in a TRS, i.e., replace f(g(h(x))) -> f(x) by h(g(f(x))) -> f(x). Note that the variable in a reversed rule should be same as the variable in the original rule. if R is WCR and overlay, S = {}, then one can switch to innermost Proof relative termination of R/S by proving relative termination of D / R u S - D and relative termination of R - D / S - D. The rules D have to given, then the termination proof of D / R u S - D, and finally the proof of R - D / S - D. remove those rules, which are not applicable since their lhs has an argument that is not in normal form (for innermost rewriting). The removed rules have to be provided. Eta-expand the TRS R, uncurry it, and add the uncurrying rules. The transformed rules of R have to be provided as TRS, the uncurrying rules are within the uncurryInformation. removes all rules t -> t from S the flat context closure as required for the root labeling technique. one also has to provide the list of flat contexts which is used to fix the variable names in the resulting TRS. example: if the flat contexts are f(Box,x_1) f(x_1,Box) g(Box,u) g(z,Box) and the TRS f(x,y) -> g(x,y) then the resulting TRS is obtained by replacing all boxes by corresponding left- and right-hand sides of rules: f(f(x,y),x_1) -> f(g(x,y),x_1) f(x_1,f(x,y)) -> f(x_1,g(x,y)) g(f(x,y),u) -> g(g(x,y),u) g(z,f(x,y)) -> g(z,g(x,y)) The reason for this requirement is that 1) it eases the check whether the given system really consists of all rules - where one does not have to bother with variable renamings 2) the flat context closures have to be computed in any way. 3) the overhead in the size is small, since for every flat-context there will be n new rules each being larger than the the context. Transform all constants into unary symbols. A renaming from the constants to the unary symbols has to be provided, in combination with the new TRS. Moreover, one has to provide a unique variable which is used for transforming ground rules. E.g., for a rule f(a) -> g(b), one needs to know the x in the resulting rule f(a(x)) -> g(b(x)). just claim that all critical pairs are joinable, which can be checked by computing normal forms Given '(R, s, t)' where 'R' is a TRS and 's' and 't' are two terms, certifies R-nonreachability of 't' from 's', i.e., there is no substitution sigma such that 't sigma' rewrites to 's sigma'. Indicate that 'tcap(s)' does not unify with 't'. Make sure that 'R' is linear and growing and provide a signature 'F', the names of two constants 'a' and 'c' s.t. 'a in F' and 'c not in F', a tree automaton 'A' that is an overapproximation of the ancestor automaton for the ground-instances automaton of the right-hand side of the reachability problem 't', and the language of the intersection of the ground-instances automaton of the left-hand side of the reachability problem 's' and 'A' is empty, and a 'stateMap' from the states used in 'A' to symbols in 'F'. Has to provide a TRS 'R'' s.t. for each 'l -> r in R' there is 'l' -> r' in R'' and a substituion 'sigma' with 'l = l'sigma' and 'r = r'sigma', and a 'nonreachabilityProof' for '(R', s, t)'. Provides a 'nonreachabilityProof' for (R^-1, t, s). Such that s sigma does not rewrite to t sigma by providng a cowrite pair such that: A) R is contained in >= and B) s < t Note that the redPair element actually refers to corewrite pairs. Provides nonreachability proof by equational disproof. Note that the goal must be ground. Given '(R, s, t)' where 'R' is a TRS and 's' and 't' are terms, certifies nonjoinability of 's' and 't' w.r.t. 'R', i.e., there is no substitution sigma such that 's sigma' and 't sigma' are joinable w.r.t. R. Indicate that 'tcap(s)' does not unify with 'tcap(t)'. If at least one of the two terms 's' and 't', say 't', is a ground R-normal form provide a 'nonreachabilityProof' for '(R, s, t)'. Given '(R, c)' where 'R' is a oriented CTRS and 'c' a list of directed pairs '(s_1 ,t_1), ..., (s_k,t_k)' certifies infeasibility of 'c' w.r.t. 'R', i.e., there is no substitution sigma such that s_i sigma rewrites to t_i sigma for all i. Has to provide a compound symbol 'cs' of arity 'k' together with a 'nonreachabilityProof' for '(R_u, cs(s_1,...,s_k), cs(t_1,...,t_k))'. Has to provide one condition (rule) 's == t in c' and a 'nonreachabilityProof' for '(R_u, s, t)'. Has to provide a subset of the conditions (rules) ' c' subsetof c ' and an 'infeasibilityProof' for '(R, c')'. Has to provide three terms 's', 't', and 'u' s.t. 's = u' and 't = u' are equations in the conditions 'c' and a 'nonjoinabilityProof' for '(R_u, s, t)'. Has to provide three terms 's', 't', and 't' s.t. 's = t' and 't = u' are equations in the conditions 'c' and a 'nonreachabilityProof' for '(R_u, s, u)'. The split-if transformation (Claessen and Smallbone, 2018) for infeasibility of CTRSs via normal unraveling (Marchiori 1996). This transformation lifts infeasibility condtions into a rule. To be precise, given two constants T, F transforms the infeasibility problem of conditions cs over R into the infeasibility problem of the single condition T -> F over R plus the rule T -> F | cs. Corollary 3.32 in Florian Meßner's master thesis Lemma 3, Sternagel and Sternagel, 2017 the resulting CTRS after inlining The CTRS is not confluent as there are two conditional rewrite sequences starting from the same term which cannot be joined. The fourth argument is the reason why a join wrt. the underlying TRS R_u is not possible. Lemma 3, Sternagel and Sternagel, 2017 the resulting CTRS after inlining information of inlining. used by inlineConditions (confluence of CTRSs) and right/leftInlineConditions for infeasibility the original rule before inlining the conditions to be eliminated (must be a subset of the condtions of the rule above) Lemma 3, Sternagel and Sternagel, 2017 the resulting CTRS after inlining Indicates that the CTRS 'R' is almost orthogonal. Indicates that the CTRS 'R' is almost orthogonal modulo infeasibility. So for each CCP coming from an overlap of rules 'l_1 -> r_1 | d_1' and 'l_2 -> r_2 | d_2' with mgu 'sigma' we have to certify that its conditions 'c_1, c_2' (where 'c_1 = d_1sigma' and 'c_2 = d_2sigma') are infeasible by 'aoInfeasibleConditions'. Has to provide two sequences of conditions 'c_1' and 'c_2' and an 'aoInfeasibilityProof' for '(R, c_1, c_2)'. Given '(R, c_1, c_2)' where 'R' is a CTRS that is oriented, of type 3, right-stable, extended properly oriented and left-linear and two sequences of conditions 'c_1' and 'c_2' this certifies infeasibility w.r.t. almost orthogonality of 'c_1, c_2' w.r.t. 'R'. We have to provide three terms 's', 't', 'u' and a 'nonjoinabilityProof' for '(R_u, t, u)'. 's' is the left-hand side of two conditions and 't' and 'u' are two different right-hand sides s.t. 's == t in c_1' and 's == u in c_2'. For each conditional rule (incl. unconditional rules) one has to provide all unraveled rules. Note that unraveling do not recognize literal similarlity. For each conditional rule (incl. unconditional rules) one can provide all unraveled rules. Note that one may omit entries, and unraveling do not recognize literal similarlity. at the moment, CeTA just supports condition-type oriented This is the standard problem format for first order TRSs in Cops/ARI/CoCo. This is a commutation problem in Cops/ARI/CoCo. This is an infeasibility problem in Cops/ARI/CoCo. In principle any reduction order for ordered completion can be used, but currently for ordered completion just KBO is supported by CeTA. This is why not just a link to all possible reduction orders is included. Note that the arities within the precedence weight entries in combination with argument filters correspond to the unfiltered arities. E.g., if the second argument of f/3 is dropped then the weight precedence entry still has to give arity 3 to f. higher numbers = higher precedence. Unspecified symbols obtain precedence 0. provide dps to delete, rules to delte, and usable rules. provide pairs to delete and usable rules claim that finiteness is trivial, since no strict pairs and rules are remaining, or no pairs are remaining. split the current set of DPs into several smaller subproblems by using some DP-graph estimation. Note that all components of the graph have to be specified, including singleton nodes which do not form an SCC on their own. For the latter no sub-proof must be given. The list of components has to be given in topological order, where the components with no incoming edges are listed first. Use the subterm criterion to delete some DPs. The removed DPs have to be given. First the equations have to be given, then the dps for the equations, then the dps for the TRS, finally, the extended rules like f(l,x) -> f(r,x) The two subproofs are first for the DPs of the TRS, and second for the sharped version of the extended rules. If only one subproof is provided, then the DPs of the TRS and the sharped version of the extended rules are merged. Use a reduction pair where both the weak and the strict ordering are monotone. Delete all strictly decreasing rules of the TRS. The deleted rules have to be provided. state that R is AC-terminating since R has no rules. nfs-flag: does one restrict to normal form substitutions? important in presence of extra variables in rhss. Default is false. Show feasibility by providing the witness substitution and the steps to satisfy the conditions. The list of steps has to be exactly in the same order as the list of conditions. the root node of the certification problem format. current version number: 3.0 There might be several infos on the origin of the input, e.g., some COPS/ARI id, some paper reference, some TPDB filename, etc. It is preferred to list these informations one by one. The first information should be the major source and is displayed in the HTML-version of CPF. There might be several infos on the tool(s) that generated the proof, e.g., the name of major tool, version information, auxiliary tools, etc. It is preferred to list these informations one by one. The first information should be name of the major tool and this information is displayed in the HTML-version of CPF. a unique name of a competition, e.g., CoCo 2023, CoCo 2023 full run, termComp 2023, ... Further informations of any kind. The first further information is displayed in the HTML-version of CPF.