1 <?xml version="1.0" encoding="UTF-8"?>
2 <xs:schema xmlns:xs="http://www.w3.org/2001/XMLSchema" elementFormDefault="qualified" version="2.1">
3 <xs:element name="name" type="xs:string"> </xs:element>
4 <xs:group name="label">
6 <xs:documentation>a label for semantic labeling</xs:documentation>
9 <xs:element name="numberLabel">
12 <xs:element maxOccurs="unbounded" minOccurs="0" name="number"
13 type="xs:nonNegativeInteger"/>
17 <xs:element name="symbolLabel">
20 <xs:group maxOccurs="unbounded" minOccurs="0" ref="symbol"/>
26 <xs:group name="symbol">
28 <xs:documentation>is used as a function symbol in terms, orderings, ....</xs:documentation>
31 <xs:element ref="name"/>
32 <xs:element name="sharp">
35 <xs:group ref="symbol"/>
39 <xs:element name="labeledSymbol">
42 <xs:group ref="symbol"/>
43 <xs:group ref="label"/>
49 <xs:element name="var" type="xs:string"/>
51 <xs:group name="term">
53 <xs:element ref="var"/>
54 <xs:element name="funapp">
57 <xs:group ref="symbol"/>
58 <xs:element name="arg" maxOccurs="unbounded" minOccurs="0">
60 <xs:group ref="term"/>
68 <xs:element name="rule">
71 <xs:element name="lhs">
73 <xs:group ref="term"/>
76 <xs:element name="rhs">
78 <xs:group ref="term"/>
84 <xs:element name="rules">
87 <xs:element maxOccurs="unbounded" minOccurs="0" ref="rule"/>
91 <xs:element name="dps">
94 <xs:element ref="rules"/>
98 <xs:element name="trs">
101 <xs:element ref="rules"/>
105 <xs:element name="usableRules">
108 <xs:element ref="rules"/>
112 <xs:group name="number">
114 <xs:element name="integer" type="xs:integer"/>
115 <xs:element name="rational">
118 <xs:element name="numerator" type="xs:integer"/>
119 <xs:element name="denominator" type="xs:positiveInteger"/>
125 <xs:element name="coefficient">
128 <xs:group ref="number"/>
129 <xs:element name="minusInfinity"/>
130 <xs:element name="plusInfinity"/>
131 <xs:element ref="vector"/>
132 <xs:element ref="matrix">
134 <xs:documentation>list of column-vectors</xs:documentation>
140 <xs:element name="vector">
143 <xs:element maxOccurs="unbounded" ref="coefficient"/>
147 <xs:element name="matrix">
149 <xs:documentation>list of column-vectors</xs:documentation>
153 <xs:element maxOccurs="unbounded" ref="vector"/>
157 <xs:element name="polynomial">
160 <xs:element ref="coefficient"/>
161 <xs:element name="variable" type="xs:positiveInteger"/>
162 <xs:element name="sum">
165 <xs:element maxOccurs="unbounded" ref="polynomial"/>
169 <xs:element name="product">
172 <xs:element maxOccurs="unbounded" ref="polynomial"/>
176 <xs:element name="max">
178 <xs:documentation>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.</xs:documentation>
182 <xs:element maxOccurs="unbounded" ref="polynomial"/>
186 <xs:element name="min">
188 <xs:documentation>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.</xs:documentation>
192 <xs:element maxOccurs="unbounded" ref="polynomial"/>
199 <xs:group name="function">
201 <xs:element ref="polynomial">
203 <xs:documentation>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.</xs:documentation>
208 <xs:element name="arity" type="xs:nonNegativeInteger"/>
209 <xs:element name="dimension" type="xs:positiveInteger"/>
210 <xs:element name="strictDimension" type="xs:positiveInteger"/>
211 <xs:element name="degree" type="xs:nonNegativeInteger"/>
212 <xs:element name="position" type="xs:positiveInteger"/>
213 <xs:element name="positionInTerm">
216 <xs:element ref="position" maxOccurs="unbounded" minOccurs="0"/>
220 <xs:element name="argumentFilter">
222 <xs:documentation>an argument filter consist of a mapping from symbols to collapsing or non-collapsing filters.
225 an entry f/3 -> collapsing/1 filters the ternary symbol f to its third argument.
226 an entry f/3 -> nonCollapsing/3 1 filters the term f(x,y,z) to f(z,x)
228 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.</xs:documentation>
232 <xs:element maxOccurs="unbounded" minOccurs="0" name="argumentFilterEntry">
235 <xs:group ref="symbol"/>
236 <xs:element ref="arity"/>
238 <xs:element name="collapsing" type="xs:positiveInteger"/>
239 <xs:element name="nonCollapsing">
242 <xs:element maxOccurs="unbounded" minOccurs="0" ref="position"/>
253 <xs:element name="domain">
256 <xs:element name="naturals"/>
257 <xs:element name="integers">
259 <xs:documentation>purpose: arctic below zero is arctic-integer</xs:documentation>
262 <xs:element name="rationals">
265 <xs:element name="delta">
268 <xs:group ref="number"/>
275 <xs:element name="arctic">
278 <xs:element ref="domain"/>
282 <xs:element name="tropical">
285 <xs:element ref="domain"/>
289 <xs:element name="matrices">
291 <xs:documentation>the domain of matrices where the elements are from the subdomain specified</xs:documentation>
295 <xs:element ref="dimension"/>
296 <xs:element ref="strictDimension">
298 <xs:documentation>in the upper left submatrix of this dimension there must be a strict decrease
299 (the remaining parts of the matrix is ignored for strict decreases, only weak decreases are required).</xs:documentation>
302 <xs:element ref="domain"/>
309 <xs:element name="redPair">
312 <xs:element name="interpretation">
315 <xs:element name="type">
318 <xs:element name="polynomial">
320 <xs:documentation>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.</xs:documentation>
324 <xs:element ref="domain"/>
325 <xs:element ref="degree">
327 <xs:documentation>the maximal degree of the polynomial interpretation (some certifiers only support linear interpretations).
328 all interpretations given should respect this degree.
335 <xs:element name="matrixInterpretation">
337 <xs:documentation>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.</xs:documentation>
341 <xs:element ref="domain"/>
342 <xs:element ref="dimension"/>
343 <xs:element ref="strictDimension">
345 <xs:documentation>in the upper subvector of this dimension there must be a strict decrease
346 (the lower part of the vector is ignored for strict decreases, only weak decreases are required).</xs:documentation>
355 <xs:element maxOccurs="unbounded" minOccurs="0" name="interpret">
358 <xs:group ref="symbol"/>
359 <xs:element ref="arity"/>
360 <xs:group ref="function"/>
367 <xs:element name="pathOrder">
370 <xs:element name="statusPrecedence">
373 <xs:element name="statusPrecedenceEntry" maxOccurs="unbounded" minOccurs="0">
375 <xs:documentation>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.</xs:documentation>
379 <xs:group ref="symbol"/>
380 <xs:element ref="arity"/>
381 <xs:element name="precedence" type="xs:nonNegativeInteger">
383 <xs:documentation>higher numbers = higher precedence. Unspecified symbols obtain precedence 0.</xs:documentation>
387 <xs:element name="lex">
389 <xs:documentation>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]</xs:documentation>
391 <xs:complexType> </xs:complexType>
393 <xs:element name="mul"/>
401 <xs:element minOccurs="0" ref="argumentFilter">
403 <xs:documentation>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]</xs:documentation>
409 <xs:element name="knuthBendixOrder">
412 <xs:element name="w0" type="xs:positiveInteger">
417 <xs:element name="precedenceWeight">
420 <xs:element name="precedenceWeightEntry" maxOccurs="unbounded" minOccurs="0">
422 <xs:documentation>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.</xs:documentation>
426 <xs:group ref="symbol"/>
427 <xs:element ref="arity"/>
428 <xs:element name="precedence" type="xs:nonNegativeInteger">
430 <xs:documentation>higher numbers = higher precedence. Unspecified symbols obtain precedence 0.</xs:documentation>
433 <xs:element name="weight" type="xs:nonNegativeInteger">
444 <xs:element minOccurs="0" ref="argumentFilter">
446 <xs:documentation>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]</xs:documentation>
452 <xs:element name="scnp">
455 <xs:element name="status">
458 <xs:element name="ms"/>
459 <xs:element name="min"/>
460 <xs:element name="max"/>
461 <xs:element name="dms"/>
465 <xs:element name="levelMapping">
468 <xs:element maxOccurs="unbounded" minOccurs="0" name="levelMappingEntry">
471 <xs:group ref="symbol"/>
472 <xs:element ref="arity"/>
473 <xs:element maxOccurs="unbounded" minOccurs="0" name="positionLevelEntry">
475 <xs:documentation>position 0 encodes the argument "full term"</xs:documentation>
479 <xs:element name="position" type="xs:nonNegativeInteger"/>
480 <xs:element name="level" type="xs:nonNegativeInteger"/>
490 <xs:element ref="redPair"/>
497 <xs:element name="arithFunction">
500 <xs:element name="natural" type="xs:nonNegativeInteger"/>
501 <xs:element name="variable" type="xs:positiveInteger"/>
502 <xs:element name="sum">
505 <xs:element maxOccurs="unbounded" ref="arithFunction"/>
509 <xs:element name="product">
512 <xs:element maxOccurs="unbounded" ref="arithFunction"/>
516 <xs:element name="min">
519 <xs:element maxOccurs="unbounded" ref="arithFunction"/>
523 <xs:element name="max">
526 <xs:element maxOccurs="unbounded" ref="arithFunction"/>
533 <xs:element name="model">
536 <xs:element name="finiteModel">
538 <xs:documentation>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
543 <xs:element name="carrierSize" type="xs:positiveInteger"/>
544 <xs:element minOccurs="0" name="tupleOrder">
546 <xs:documentation>If this element is missing, then one uses semantic labeling in the model version.
548 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), ...</xs:documentation>
552 <xs:element name="pointWise">
554 <xs:documentation>here, (x1,..,xn) > (y1,...,yn) iff all xi >= yi and for some i: xi > yi</xs:documentation>
560 <xs:element maxOccurs="unbounded" minOccurs="0" name="interpret">
563 <xs:group ref="symbol"/>
564 <xs:element ref="arity"/>
565 <xs:element ref="arithFunction"/>
569 <xs:element name="labeling" minOccurs="0">
571 <xs:documentation>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.</xs:documentation>
577 <xs:element name="rootLabeling">
579 <xs:documentation>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.</xs:documentation>
583 <xs:group ref="symbol" minOccurs="0"/>
590 <xs:element name="patternTerm">
592 <xs:documentation>term, pumping subst., closing subst</xs:documentation>
596 <xs:group ref="term"/>
597 <xs:element ref="substitution"/>
598 <xs:element ref="substitution"/>
602 <xs:element name="patternRule">
604 <xs:documentation>the pattern terms are the lhs and rhs of the pattern rule. the third argument is the proof how to derive the pattern rule.</xs:documentation>
608 <xs:element ref="patternTerm"/>
609 <xs:element ref="patternTerm"/>
611 <xs:element name="originalRule">
614 <xs:element ref="rule"/>
615 <xs:element name="isPair" type="xs:boolean"/>
619 <xs:element name="initialPumping">
621 <xs:documentation>first substitution is for lhs, second for rhs.</xs:documentation>
625 <xs:element ref="patternRule"/>
626 <xs:element ref="substitution"/>
627 <xs:element ref="substitution"/>
631 <xs:element name="initialPumpingContext">
634 <xs:element ref="patternRule"/>
635 <xs:element ref="substitution"/>
636 <xs:element ref="positionInTerm"/>
637 <xs:element ref="var"/>
641 <xs:element name="equivalence">
644 <xs:element ref="patternRule"/>
646 <xs:element name="left"/>
647 <xs:element name="right"/>
649 <xs:element name="patternEquivalence">
652 <xs:element name="domainRenaming">
655 <xs:element ref="substitution"/>
659 <xs:element name="irrelevant">
661 <xs:documentation>first substitution is pumping, second is closing</xs:documentation>
665 <xs:element ref="substitution"/>
666 <xs:element ref="substitution"/>
670 <xs:element name="simplification">
672 <xs:documentation>first substituion is for base, second is new closing subst.</xs:documentation>
676 <xs:element ref="substitution"/>
677 <xs:element ref="substitution"/>
687 <xs:element name="narrowing">
689 <xs:documentation>first pattern rule is rewritten with second pattern rule</xs:documentation>
693 <xs:element ref="patternRule"/>
694 <xs:element ref="patternRule"/>
695 <xs:element ref="positionInTerm"/>
699 <xs:element name="instantiation">
702 <xs:element ref="patternRule"/>
703 <xs:element ref="substitution"/>
705 <xs:element name="base"/>
706 <xs:element name="pumping">
709 <xs:element name="closing">
716 <xs:element name="rewriting">
719 <xs:element ref="patternRule"/>
720 <xs:element ref="rewriteSequence"/>
722 <xs:element name="base"/>
723 <xs:element name="pumping">
726 <xs:element ref="var"/>
730 <xs:element name="closing">
733 <xs:element ref="var"/>
745 <xs:element name="substitution">
748 <xs:element name="substEntry" maxOccurs="unbounded" minOccurs="0">
751 <xs:element ref="var"/>
752 <xs:group ref="term"/>
759 <xs:group name="context">
761 <xs:element name="box"/>
762 <xs:element name="funContext">
765 <xs:group ref="symbol"/>
766 <xs:element name="before">
768 <xs:group maxOccurs="unbounded" minOccurs="0" ref="term"/>
771 <xs:group ref="context"/>
772 <xs:element name="after">
774 <xs:group maxOccurs="unbounded" minOccurs="0" ref="term"/>
782 <xs:element name="rewriteSequence">
784 <xs:documentation>if t_0 is startterm, and there are rewrite-steps p_i, rule_i, t_i (for i = 1..n)
785 then t_{i-1} ->_{p_i,rule_i} t_i for all i=1..n
787 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).</xs:documentation>
791 <xs:element name="startTerm">
794 <xs:group ref="term"/>
798 <xs:element maxOccurs="unbounded" minOccurs="0" ref="rewriteStep"/>
802 <xs:element name="rewriteStep">
805 <xs:element ref="positionInTerm"/>
806 <xs:element ref="rule"/>
807 <xs:element minOccurs="0" name="relative"/>
808 <xs:group ref="term"/>
812 <xs:element name="state" type="xs:string">
814 <xs:documentation>the state of a tree automation</xs:documentation>
817 <xs:element name="treeAutomaton">
820 <xs:element name="finalStates">
823 <xs:element maxOccurs="unbounded" minOccurs="0" ref="state"/>
827 <xs:element name="transitions">
830 <xs:element maxOccurs="unbounded" minOccurs="0" name="transition">
833 <xs:element name="lhs">
837 <xs:group ref="symbol"/>
838 <xs:element minOccurs="0" name="height" type="xs:nonNegativeInteger"/>
839 <xs:element maxOccurs="unbounded" minOccurs="0" ref="state"/>
841 <xs:element ref="state"/>
845 <xs:element name="rhs">
848 <xs:element ref="state"/>
861 <xs:element name="uncurryInformation">
863 <xs:documentation>the uncurrying information consists of:
864 - the application symbol
865 - the names of the uncurried symbols
866 - the uncurrying rules
867 - the additional rules that are obtained when eta-expanding the TRS
872 <xs:group ref="symbol"/>
873 <xs:element name="uncurriedSymbols">
876 <xs:element maxOccurs="unbounded" name="uncurriedSymbolEntry">
878 <xs:documentation>mark for each original symbols the new uncurried symbols:
879 if the constant map should now be uncurried up to two levels then
880 there should be a symbol map entry
881 map (we want to uncurry map)
882 0 (the original arity of map)
883 map (the new constant)
884 map1 (the new unary symbol)
885 map2 (the new binary symbol)
887 Note that the names can be chosen arbitrarily</xs:documentation>
891 <xs:group ref="symbol"/>
892 <xs:element ref="arity"/>
893 <xs:group ref="symbol" maxOccurs="unbounded"/>
900 <xs:element name="uncurryRules">
903 <xs:element ref="rules"/>
907 <xs:element name="etaRules">
910 <xs:element ref="rules"/>
917 <xs:element name="loop">
919 <xs:documentation>a loop is given by a (non-empty) rewrite-sequence t0 ->+ tn where additionally tn = C[t0 sigma]</xs:documentation>
923 <xs:element ref="rewriteSequence"/>
924 <xs:element ref="substitution"/>
925 <xs:group ref="context"/>
929 <xs:element name="nonLoop">
931 <xs:documentation>first substitution is part of pumping subst.,
932 second substitution is part of closing subst.,
933 first natural is for decomposing pumping subst.,
934 second natural is for getting subterm</xs:documentation>
938 <xs:element ref="patternRule"/>
939 <xs:element ref="substitution"/>
940 <xs:element ref="substitution"/>
941 <xs:element name="natural" type="xs:nonNegativeInteger"/>
942 <xs:element name="natural" type="xs:nonNegativeInteger"/>
943 <xs:element ref="positionInTerm"/>
947 <xs:element name="orderingConstraints">
949 <xs:documentation>every strict order has to be well-founded.
950 every strict order > has to be compatible with all orders >' (both strict and non-strict):
951 Here, compatible between a strict order > and >' is defined as:
952 s > t and t >' u implies s > u, and similarly, s >' t and t > u implies s > u.
953 every order has to be stable.
954 The demand for monotonicity, etc. is specified by the corresponding sub-elements.</xs:documentation>
958 <xs:element maxOccurs="unbounded" name="orderingConstraintElement">
961 <xs:element name="strict" type="xs:boolean"/>
962 <xs:element name="ceCompatible" type="xs:boolean"/>
963 <xs:element minOccurs="0" name="monotonePositions">
965 <xs:documentation>if this element is not given, then monotonicity is not required. Otherwise, the order has to be monotone in the specified argument positions. Either this complete monotonicity, or it is specified by an argument filter pi (only non-collapsing entries), where the order has to be monotone in (f,i), whenever pi(f) contains i.</xs:documentation>
969 <xs:element ref="argumentFilter">
971 <xs:documentation>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]</xs:documentation>
974 <xs:element name="everySymbolAndPosition"/>
978 <xs:element minOccurs="0" name="ignoredPositions">
980 <xs:documentation>only non-collapsing argument filters pi. whenever i is not contained in pi(f), then f(s1,...si,...sn) >= f(s1,....ti,...sn) must hold for arbitrary si and ti.</xs:documentation>
984 <xs:element ref="argumentFilter">
986 <xs:documentation>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]</xs:documentation>
992 <xs:element maxOccurs="unbounded" minOccurs="0" ref="rule"/>
999 <xs:element name="orderingConstraintProof">
1002 <xs:element ref="redPair"/>
1003 <xs:element name="satisfiableAssumption">
1006 <xs:element ref="orderingConstraints"/>
1013 <xs:element name="url" type="xs:string"/>
1014 <xs:element name="trsInput">
1016 <xs:documentation>If a certifier is not able to treat certain features like AC or innermost or ..., then it has to guarantee that these fields are not present in the certification problem. If they are, the certifier has to fail (and not just ignore!)</xs:documentation>
1020 <xs:element ref="trs"/>
1021 <xs:element minOccurs="0" ref="strategy"/>
1022 <xs:element minOccurs="0" ref="equations"/>
1023 <xs:element name="relativeRules" minOccurs="0">
1026 <xs:element ref="rules"/>
1033 <xs:element name="dpInput">
1036 <xs:element ref="trs"/>
1037 <xs:element ref="dps"/>
1038 <xs:element ref="strategy" minOccurs="0"/>
1039 <xs:element name="minimal" type="xs:boolean"/>
1043 <xs:element name="strategy">
1045 <xs:documentation>no strategy means standard rewriting without restrictions</xs:documentation>
1049 <xs:element name="innermost"/>
1050 <xs:element ref="innermostLhss"/>
1054 <xs:element name="equations">
1057 <xs:element ref="rules"/>
1061 <xs:element name="conversion">
1064 <xs:element name="startTerm">
1067 <xs:group ref="term"/>
1071 <xs:element maxOccurs="unbounded" name="equationStep" minOccurs="0">
1074 <xs:element name="positionInTerm">
1077 <xs:element ref="position" maxOccurs="unbounded" minOccurs="0"/>
1081 <xs:element ref="rule"/>
1083 <xs:element name="leftRight"/>
1084 <xs:element name="rightLeft"/>
1086 <xs:group ref="term"/>
1093 <xs:element name="subsumptionProof">
1096 <xs:element maxOccurs="unbounded" minOccurs="0" name="ruleSubsumptionProof">
1099 <xs:element ref="rule"/>
1100 <xs:element ref="conversion"/>
1107 <xs:element name="innermostLhss">
1109 <xs:group ref="term" maxOccurs="unbounded" minOccurs="0"/>
1112 <xs:group name="complexityMeasure">
1114 <xs:element name="derivationalComplexity">
1117 <xs:element ref="signature"/>
1121 <xs:element name="runtimeComplexity">
1123 <xs:documentation>first signature defines constructors, second signature the defined symbols</xs:documentation>
1127 <xs:element ref="signature"/>
1128 <xs:element ref="signature"/>
1135 <xs:group name="equationalProofTree">
1137 <xs:element name="refl">
1140 <xs:group ref="term"/>
1144 <xs:element name="sym">
1147 <xs:group ref="equationalProofTree"/>
1151 <xs:element name="trans">
1154 <xs:group ref="equationalProofTree"/>
1155 <xs:group ref="equationalProofTree"/>
1159 <xs:element name="assm">
1162 <xs:element ref="rule"/>
1163 <xs:element ref="substitution"/>
1167 <xs:element name="cong">
1170 <xs:group ref="symbol"/>
1171 <xs:group maxOccurs="unbounded" minOccurs="0" ref="equationalProofTree"/>
1177 <xs:element name="completionAndNormalization">
1180 <xs:element ref="trs"/>
1181 <xs:element ref="completionProof"/>
1185 <xs:element name="signature">
1188 <xs:element maxOccurs="unbounded" minOccurs="0" name="symbol">
1191 <xs:group ref="symbol"/>
1192 <xs:element ref="arity"/>
1199 <xs:group name="complexityClass">
1201 <xs:element name="polynomial" type="xs:nonNegativeInteger">
1203 <xs:documentation>the number is the degree:
1206 2 -> O(n^2) ...</xs:documentation>
1211 <xs:element name="complexityProof">
1214 <xs:element name="rIsEmpty">
1216 <xs:documentation>state that the strict TRS is empty and therefore is in O(1).</xs:documentation>
1220 <xs:element name="ruleShifting">
1222 <xs:documentation>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</xs:documentation>
1226 <xs:element ref="orderingConstraintProof"/>
1227 <xs:element ref="trs"/>
1228 <xs:element ref="complexityProof"/>
1235 <xs:element name="completionProof">
1241 <xs:element ref="wcrProof"/>
1242 <xs:element ref="trsTerminationProof"/>
1243 <xs:element name="equivalenceProof">
1245 <xs:documentation>Show that a given set of equations E is equivalent to a TRS R,
1246 by showing that all rules can be derived from the equations and vice versa.
1247 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.</xs:documentation>
1251 <xs:element ref="subsumptionProof"/>
1252 <xs:element minOccurs="0" ref="subsumptionProof"/>
1259 <xs:element name="crProof">
1262 <xs:element name="wcrAndSN">
1265 <xs:element ref="wcrProof"/>
1266 <xs:element ref="trsTerminationProof"/>
1270 <xs:element name="orthogonal"/>
1274 <xs:element name="crDisproof">
1277 <xs:element name="nonWcrAndSN">
1280 <xs:element name="wcrDisproof">
1283 <xs:element name="nonJoinableCriticalPairsAuto">
1285 <xs:documentation>just claim that some critical pair is not joinable.</xs:documentation>
1291 <xs:element ref="trsTerminationProof"/>
1295 <xs:element name="nonJoinableFork">
1297 <xs:documentation>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.</xs:documentation>
1301 <xs:element ref="rewriteSequence"/>
1302 <xs:element ref="rewriteSequence"/>
1304 <xs:element name="distinctNormalForms">
1306 <xs:documentation>the terms are distinct normal forms.</xs:documentation>
1309 <xs:element name="capNotUnif">
1311 <xs:documentation>after applying some cap-functions, the capped terms are not unifiable.</xs:documentation>
1321 <xs:element name="dpNonterminationProof">
1324 <xs:element ref="loop"/>
1325 <xs:element name="dpRuleRemoval">
1327 <xs:documentation>Remove some rules and / or DPs to figure out the really nonterminating DP problem (remaining rules and DPs are given, if they are not given, then this means no change).
1328 Note that this element can be used for several termination techniques like the dependency graph processor, or the various reduction pair processors.
1333 <xs:element ref="dps" minOccurs="0"/>
1334 <xs:element ref="trs" minOccurs="0"/>
1335 <xs:element ref="dpNonterminationProof"/>
1339 <xs:element name="infinitenessAssumption">
1342 <xs:element ref="dpInput"/>
1346 <xs:element ref="nonLoop"/>
1347 <xs:element name="innermostLhssRemovalProc">
1349 <xs:documentation>For innermost termination: remove those lhss from the innermost strategy component which contain symbols that do not occur in the remaining DP problem.
1350 The remaining set of lhss has to be given in the proof.</xs:documentation>
1354 <xs:element ref="innermostLhss"/>
1355 <xs:element ref="dpNonterminationProof"/>
1359 <xs:element name="innermostLhssIncreaseProc">
1361 <xs:documentation>Add new lhss to innermost strategy component.</xs:documentation>
1365 <xs:element ref="innermostLhss"/>
1366 <xs:element ref="dpNonterminationProof"/>
1370 <xs:element name="switchFullStrategyProc">
1372 <xs:documentation>Switch from innermost rewriting to full/unrestricted rewriting for locally confluent TRS where there are no overlaps between pairs and rules.</xs:documentation>
1376 <xs:element ref="wcrProof"/>
1377 <xs:element ref="dpNonterminationProof"/>
1381 <xs:element name="instantiationProc">
1383 <xs:documentation>Instantiate several DPs. The set of new DPs has to be provided.</xs:documentation>
1387 <xs:element ref="dps"/>
1388 <xs:element ref="dpNonterminationProof"/>
1395 <xs:element name="dpProof">
1398 <xs:element name="pIsEmpty">
1400 <xs:documentation>trivial proof by stating that the set of DPs is empty</xs:documentation>
1403 <xs:element name="depGraphProc">
1405 <xs:documentation>split the current set of DPs into several smaller subproblems by using some DP-graph estimation.
1406 Note that all components of the graph have to be specified, including singleton nodes which do not form an SCC on their own. The list of components has to be given in topological order, where the components with no incoming edges are listed first.</xs:documentation>
1410 <xs:element maxOccurs="unbounded" minOccurs="0" name="component">
1413 <xs:element ref="dps"/>
1414 <xs:element name="realScc" type="xs:boolean">
1416 <xs:documentation>may only be set to false, if component is singleton node without edge to itself.
1417 if set to true, then proof for remaining DP problem has to be given</xs:documentation>
1420 <xs:element minOccurs="0" name="arcs">
1422 <xs:documentation>If the arcs-element is present, then the forward arcs between the components have to be listed as children. This will improve the efficiency of certain certifiers. Example:
1424 - not giving an arcs-element is always safe (but will slow down some certifiers)
1425 - giving an <arcs/> element is only possible if there are no forward arcs
1428 <forwardArc>2</forwardArc>
1429 <forwardArc>7</forwardArc>
1431 element states that there are only arcs to the components 2 and
1432 7 positions further in the component-list.</xs:documentation>
1436 <xs:element maxOccurs="unbounded" minOccurs="0" name="forwardArc"
1437 type="xs:positiveInteger">
1439 <xs:documentation>the idea is to make relative forward references by numbers:
1449 can be represented in the component list
1450 [ (A,B, real, 1,2), (C,nonreal,2), (E,real), (D,real) ]
1452 then (A,B) gets forwardArcs 1 and 2 since (C) is one element after the (A,B) entry and (E) is 2 elements after the (A,B) entry
1454 (C) gets a forwardArc 2, since (D) is two elements later in the list.
1456 In this way, one does not have do introduce numbers for the SCCs,
1457 the SCC-DAG is present, and the list must be in topologic order,
1458 since the forwardArcs are positive numbers only.
1465 <xs:element minOccurs="0" ref="dpProof"/>
1472 <xs:element name="redPairProc">
1474 <xs:documentation>Use a reduction pair where only the non-strict order has to be monotone.
1475 It allows to delete those DPs which are strictly oriented.
1476 The remaining DPs have to be given.
1478 If the ordering constraint proof is only an assumption, the orderingConstraints-element becomes mandatory.</xs:documentation>
1482 <xs:element minOccurs="0" ref="orderingConstraints"/>
1483 <xs:element ref="orderingConstraintProof"/>
1484 <xs:element ref="dps"/>
1485 <xs:element ref="dpProof"/>
1489 <xs:element name="redPairUrProc">
1491 <xs:documentation>Use a Ce-compatible reduction pair where only the non-strict order has to be monotone.
1492 It allows to delete those DPs which are strictly oriented.
1493 Here only the usable rules have to be weakly oriented.
1495 If the ordering constraint proof is only an assumption, the orderingConstraints-element becomes mandatory.</xs:documentation>
1499 <xs:element minOccurs="0" ref="orderingConstraints"/>
1500 <xs:element ref="orderingConstraintProof"/>
1501 <xs:element ref="dps"/>
1502 <xs:element ref="usableRules"/>
1503 <xs:element ref="dpProof"/>
1507 <xs:element name="monoRedPairProc">
1509 <xs:documentation>Use a reduction pair where both the non-strict and the strict order have to be monotone.
1510 It allows to delete those DPs and those rules of the TRSs which are strictly oriented.
1511 The remaining DPs and the remaining TRSs have to be given.
1513 If the ordering constraint proof is only an assumption, the orderingConstraints-element becomes mandatory.</xs:documentation>
1517 <xs:element minOccurs="0" ref="orderingConstraints"/>
1518 <xs:element ref="orderingConstraintProof"/>
1519 <xs:element ref="dps"/>
1520 <xs:element ref="trs"/>
1521 <xs:element ref="dpProof"/>
1525 <xs:element name="monoRedPairUrProc">
1527 <xs:documentation>Use a Ce-compatible reduction pair where both the non-strict and the strict order have to be monotone.
1528 It allows to delete those DPs and those rules of the TRSs which are strictly oriented.
1529 Moreover, all non-usable rules can also be deleted.
1530 Here, only the usable rules instead of all rules of the TRS have to be oriented.
1531 The remaining DPs and the remaining TRSs have to be given, as well as the usable rules.
1533 If the ordering constraint proof is only an assumption, the orderingConstraints-element becomes mandatory.</xs:documentation>
1537 <xs:element minOccurs="0" ref="orderingConstraints"/>
1538 <xs:element ref="orderingConstraintProof"/>
1539 <xs:element ref="dps"/>
1540 <xs:element ref="trs"/>
1541 <xs:element ref="usableRules"/>
1542 <xs:element ref="dpProof"/>
1546 <xs:element name="subtermProc">
1548 <xs:documentation>Use the subterm criterion to delete some DPs.
1549 Only collapsing argument filters or identity filters may be used.
1550 The remaining DPs have to be given. The subterm criterion can also be used in combination wirth rewrite sequences.</xs:documentation>
1554 <xs:element ref="argumentFilter"/>
1555 <xs:element maxOccurs="unbounded" minOccurs="0" name="projectedRewriteSequence">
1557 <xs:documentation>The rule specifies the DP for which the rewrite sequence is applied. Here, the rewrite sequence for the projected terms has to be given.
1559 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.</xs:documentation>
1563 <xs:element ref="rule"/>
1564 <xs:element ref="rewriteSequence"/>
1568 <xs:element ref="dps"/>
1569 <xs:element ref="dpProof"/>
1573 <xs:element name="semlabProc">
1575 <xs:documentation>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.).
1577 The decreasing rules should be of the form f_..(x1,..,xn) -> f_..(x1,..,xn), i.e., the variables should be enumerated from x1 onwards.</xs:documentation>
1581 <xs:element ref="model"/>
1582 <xs:element ref="dps"/>
1583 <xs:element ref="trs"/>
1584 <xs:element ref="dpProof"/>
1588 <xs:element name="unlabProc">
1590 <xs:documentation>removes one layer of labels that were added by semantic labeling.</xs:documentation>
1594 <xs:element ref="dps"/>
1595 <xs:element ref="trs"/>
1596 <xs:element ref="dpProof"/>
1600 <xs:element name="sizeChangeProc">
1602 <xs:documentation>the size-change criterion processor.
1603 for each DP, one size-change graph has to be given.
1604 the set of graphs must be size-change terminating.
1605 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.
1606 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.
1607 if not all rules are usable, then one has to use a Ce-compatible order.
1610 DP: F(s(x),g(x)) -> F(id(x),g(x))
1614 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.</xs:documentation>
1619 <xs:element name="subtermCriterion"/>
1620 <xs:element name="reductionPair">
1622 <xs:documentation>The usable rules are optional. If they are used, a Ce-compatible order has to be used.
1624 If the ordering constraint proof is only an assumption, the orderingConstraints-element becomes mandatory.</xs:documentation>
1628 <xs:element minOccurs="0" ref="orderingConstraints"/>
1629 <xs:element ref="orderingConstraintProof"/>
1630 <xs:element ref="usableRules" minOccurs="0"/>
1635 <xs:element maxOccurs="unbounded" minOccurs="0" name="sizeChangeGraph">
1638 <xs:element ref="rule"/>
1639 <xs:element maxOccurs="unbounded" minOccurs="0" name="edge">
1641 <xs:documentation>an edge in a size change graph is always of the form
1643 left-argument > / >= right-argument
1645 position 0 corresponds to the whole term.</xs:documentation>
1649 <xs:element name="position" type="xs:nonNegativeInteger"/>
1650 <xs:element name="strict" type="xs:boolean"/>
1651 <xs:element name="position" type="xs:nonNegativeInteger"/>
1661 <xs:element name="flatContextClosureProc">
1663 <xs:documentation>the flat context closure as required for the root labeling technique.
1665 one also has to provide the list of flat contexts which
1666 is used to fix the variable names in the resulting DP problem.
1668 see the flat context closure technique for TRS for more explanations including an example.</xs:documentation>
1672 <xs:element minOccurs="0" name="freshSymbol">
1675 <xs:group ref="symbol"/>
1679 <xs:element name="flatContexts">
1681 <xs:group maxOccurs="unbounded" ref="context"/>
1684 <xs:element ref="dps"/>
1685 <xs:element ref="trs"/>
1686 <xs:element ref="dpProof"/>
1690 <xs:element name="argumentFilterProc">
1692 <xs:documentation>just apply an argument filter and continue on the filtered DP problem</xs:documentation>
1696 <xs:element ref="argumentFilter">
1698 <xs:documentation>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]</xs:documentation>
1701 <xs:element ref="dps"/>
1702 <xs:element ref="trs"/>
1703 <xs:element ref="dpProof"/>
1707 <xs:element name="uncurryProc">
1709 <xs:documentation>if applicativeTop does not exist, then one
1711 - uncurries P and R,
1712 - and adds the uncurrying rules to R
1713 (for the binary application symbol given in the uncurry information)
1715 if applicativeTop is present (some number n), then the intention is that the application symbol is a tuple/marked symbol of arity n. Then
1716 - the eta-expanded rules of R are added to P
1717 - one uncurries P and R
1718 - and adds the uncurrying rules to P</xs:documentation>
1722 <xs:element name="applicativeTop" type="xs:positiveInteger" minOccurs="0"/>
1723 <xs:element ref="uncurryInformation"/>
1724 <xs:element ref="dps"/>
1725 <xs:element ref="trs"/>
1726 <xs:element ref="dpProof"/>
1730 <xs:element name="finitenessAssumption">
1733 <xs:element ref="dpInput"/>
1737 <xs:element name="usableRulesProc">
1739 <xs:documentation>For innermost termination: switch to usable rules</xs:documentation>
1743 <xs:element ref="usableRules"/>
1744 <xs:element ref="dpProof"/>
1748 <xs:element name="innermostLhssRemovalProc">
1750 <xs:documentation>For innermost termination: remove those lhss from the innermost strategy component which have a root that does not occur in the remaining DP problem.
1751 The remaining set of lhss has to be given in the proof.</xs:documentation>
1755 <xs:element ref="innermostLhss"/>
1756 <xs:element ref="dpProof"/>
1760 <xs:element name="switchInnermostProc">
1762 <xs:documentation>if R is WCR and has no overlaps with P, then one can switch to innermost</xs:documentation>
1766 <xs:element ref="wcrProof"/>
1767 <xs:element ref="dpProof"/>
1771 <xs:element name="rewritingProc">
1773 <xs:documentation>Rewrite the rhs of some DP, if the usable rules of the redex are confluent.
1774 First rule: the original DP s -> t
1775 Rewrite step: the reduction from t to t' at position p
1776 Usable rules of t |_ p</xs:documentation>
1780 <xs:element ref="rule"/>
1781 <xs:element ref="rewriteStep"/>
1782 <xs:element ref="usableRules"/>
1783 <xs:element ref="dpProof"/>
1787 <xs:element name="instantiationProc">
1789 <xs:documentation>Instantiate some DP</xs:documentation>
1793 <xs:element ref="rule"/>
1794 <xs:element name="instantiations">
1797 <xs:element ref="rules"/>
1801 <xs:element ref="dpProof"/>
1805 <xs:element name="forwardInstantiationProc">
1807 <xs:documentation>Instantiate some DP using forward instantiation.
1808 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.</xs:documentation>
1812 <xs:element ref="rule"/>
1813 <xs:element name="instantiations">
1816 <xs:element ref="rules"/>
1820 <xs:element ref="usableRules" minOccurs="0"/>
1821 <xs:element ref="dpProof"/>
1825 <xs:element name="narrowingProc">
1827 <xs:documentation>Narrow some DP by considering all narrowing below position p.
1828 Note that p must be a position of the capped rhs of the pair,
1829 and some other standard application conditions have to be considered.</xs:documentation>
1833 <xs:element ref="rule"/>
1834 <xs:element ref="positionInTerm"/>
1835 <xs:element name="narrowings">
1838 <xs:element ref="rules"/>
1842 <xs:element ref="dpProof"/>
1846 <xs:element name="splitProc">
1848 <xs:documentation>Split a DP problem (P,R) to show that certain pairs PD and rules RD cannot occur infinitely often.
1849 PD and RD have to given.
1850 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.</xs:documentation>
1854 <xs:element ref="dps"/>
1855 <xs:element ref="trs"/>
1856 <xs:element ref="dpProof"/>
1857 <xs:element ref="dpProof"/>
1864 <xs:element name="equationalProof">
1867 <xs:element ref="completionAndNormalization"/>
1868 <xs:element name="equationalProofTree">
1871 <xs:group ref="equationalProofTree"/>
1875 <xs:element ref="conversion"/>
1879 <xs:element name="equationalDisproof">
1882 <xs:element ref="completionAndNormalization"/>
1886 <xs:element name="relativeNonterminationProof">
1889 <xs:element ref="loop"/>
1890 <xs:element ref="trsNonterminationProof"/>
1891 <xs:element name="variableConditionViolated">
1893 <xs:documentation>there is a rule where the lhs is a variable, or the rhs contains variables not occurring in the lhs.</xs:documentation>
1897 <xs:element name="ruleRemoval">
1899 <xs:documentation>Remove some rules to figure out the really nonterminating TRSs. (as usual, first R, then S)</xs:documentation>
1903 <xs:element ref="trs"/>
1904 <xs:element ref="trs"/>
1905 <xs:element ref="relativeNonterminationProof"/>
1909 <xs:element name="nonterminationAssumption">
1912 <xs:element ref="trsInput"/>
1919 <xs:element name="relativeTerminationProof">
1922 <xs:element name="rIsEmpty">
1924 <xs:documentation>state that the R/S is relative terminating since R has no rules</xs:documentation>
1928 <xs:element name="sIsEmpty">
1930 <xs:documentation>state that the R/S is relative terminating by termination of R since S has no rules</xs:documentation>
1934 <xs:element ref="trsTerminationProof"/>
1938 <xs:element name="ruleRemoval">
1940 <xs:documentation>use a reduction pair where both the weak and the strict ordering are monotone.
1941 Delete all strictly decreasing rules from R and S.
1942 The remaining rules of first R and then S have to be given.
1944 If the ordering constraint proof is only an assumption, the orderingConstraints-element becomes mandatory.</xs:documentation>
1948 <xs:element minOccurs="0" ref="orderingConstraints"/>
1949 <xs:element ref="orderingConstraintProof"/>
1950 <xs:element ref="trs"/>
1951 <xs:element ref="trs"/>
1952 <xs:element ref="relativeTerminationProof"/>
1956 <xs:element name="semlab">
1958 <xs:documentation>Use the semantic labeling . The model element determines the kind (model or quasi-model version, label, root-labeling, etc.)
1959 Both the labeled version of R and S have to be given (first R, then S).
1961 The decreasing rules should be of the form f_..(x1,..,xn) -> f_..(x1,..,xn), i.e., the variables should be enumerated from x1 onwards.</xs:documentation>
1965 <xs:element ref="model"/>
1966 <xs:element ref="trs"/>
1967 <xs:element ref="trs"/>
1968 <xs:element ref="relativeTerminationProof"/>
1972 <xs:element name="unlab">
1974 <xs:documentation>removes one layer of labels that were added by semantic labeling. (first R, then S, as usual)</xs:documentation>
1978 <xs:element ref="trs"/>
1979 <xs:element ref="trs"/>
1980 <xs:element ref="relativeTerminationProof"/>
1984 <xs:element name="stringReversal">
1986 <xs:documentation>reverse the strings in both TRSs R and S, i.e., replace f(g(h(x))) -> f(x) by h(g(f(x))) -> f(x).
1987 Note that the variable in a reversed rule should be same as the variable in the original rule.</xs:documentation>
1991 <xs:element ref="trs"/>
1992 <xs:element ref="trs"/>
1993 <xs:element ref="relativeTerminationProof"/>
1997 <xs:element name="relativeTerminationAssumption">
2000 <xs:element ref="trsInput"/>
2004 <xs:element name="uncurry">
2006 <xs:documentation>eta-expand both TRSs, uncurry them, and add the uncurrying rules to the relative part
2011 <xs:element ref="uncurryInformation"/>
2012 <xs:element ref="trs"/>
2013 <xs:element ref="trs"/>
2014 <xs:element ref="relativeTerminationProof"/>
2018 <xs:element name="equalityRemoval">
2020 <xs:documentation>removes all rules t -> t from the non-strict rules</xs:documentation>
2024 <xs:element ref="relativeTerminationProof"/>
2031 <xs:element name="trsNonterminationProof">
2034 <xs:element name="variableConditionViolated">
2036 <xs:documentation>there is a rule where the lhs is a variable, or the rhs contains variables not occurring in the lhs.</xs:documentation>
2040 <xs:element name="ruleRemoval">
2042 <xs:documentation>Remove some rules to figure out the really nonterminating TRS.</xs:documentation>
2046 <xs:element ref="trs"/>
2047 <xs:element ref="trsNonterminationProof"/>
2051 <xs:element name="stringReversal">
2053 <xs:documentation>reverse the strings in a TRS, i.e., replace f(g(h(x))) -> f(x) by h(g(f(x))) -> f(x).
2054 Note that the variable in a reversed rule should be same as the variable in the original rule.</xs:documentation>
2058 <xs:element ref="trs"/>
2059 <xs:element ref="trsNonterminationProof"/>
2063 <xs:element ref="loop"/>
2064 <xs:element name="dpTrans">
2066 <xs:documentation>switch to DPs as complete termination technique. See dpTrans within dpProof for other details</xs:documentation>
2070 <xs:element ref="dps"/>
2071 <xs:element name="markedSymbols" type="xs:boolean"/>
2072 <xs:element ref="dpNonterminationProof"/>
2076 <xs:element ref="nonLoop"/>
2077 <xs:element name="nonterminationAssumption">
2080 <xs:element ref="trsInput"/>
2084 <xs:element name="innermostLhssIncrease">
2086 <xs:documentation>Add new lhss to innermost strategy component.</xs:documentation>
2090 <xs:element ref="innermostLhss"/>
2091 <xs:element ref="trsNonterminationProof"/>
2098 <xs:element name="trsTerminationProof">
2101 <xs:element name="rIsEmpty">
2103 <xs:documentation>state that the TRS is terminating since it has no rules</xs:documentation>
2107 <xs:element name="ruleRemoval">
2109 <xs:documentation>use a reduction pair where both the weak and the strict ordering are monotone.
2110 Delete all strictly decreasing rules.
2111 The remaining rules have to be given.
2113 If the ordering constraint proof is only an assumption, the orderingConstraints-element becomes mandatory.</xs:documentation>
2117 <xs:element minOccurs="0" ref="orderingConstraints"/>
2118 <xs:element ref="orderingConstraintProof"/>
2119 <xs:element ref="trs"/>
2120 <xs:element ref="trsTerminationProof"/>
2124 <xs:element name="dpTrans">
2126 <xs:documentation>switch to dependency pairs. The dependency pairs have to be given. If marked is true, then the whole dp-proof is using a notion of chain where rewriting with the rules is applied at arbitrary positions (including the root). Otherwise, rewriting with the rules is not allowed at the root.</xs:documentation>
2130 <xs:element ref="dps"/>
2131 <xs:element name="markedSymbols" type="xs:boolean"/>
2132 <xs:element ref="dpProof"/>
2136 <xs:element name="semlab">
2138 <xs:documentation>Use the semantic labeling . The model element determines the kind (model or quasi-model version, label, root-labeling, etc.)
2140 The decreasing rules should be of the form f_..(x1,..,xn) -> f_..(x1,..,xn), i.e., the variables should be enumerated from x1 onwards.</xs:documentation>
2144 <xs:element ref="model"/>
2145 <xs:element ref="trs"/>
2146 <xs:element ref="trsTerminationProof"/>
2150 <xs:element name="unlab">
2152 <xs:documentation>removes one layer of labels that were added by semantic labeling.</xs:documentation>
2156 <xs:element ref="trs"/>
2157 <xs:element ref="trsTerminationProof"/>
2161 <xs:element name="stringReversal">
2163 <xs:documentation>reverse the strings in a TRS, i.e., replace f(g(h(x))) -> f(x) by h(g(f(x))) -> f(x).
2164 Note that the variable in a reversed rule should be same as the variable in the original rule.</xs:documentation>
2168 <xs:element ref="trs"/>
2169 <xs:element ref="trsTerminationProof"/>
2173 <xs:element name="flatContextClosure">
2175 <xs:documentation>the flat context closure as required for the root labeling technique.
2177 one also has to provide the list of flat contexts which
2178 is used to fix the variable names in the resulting TRS.
2180 example: if the flat contexts are
2186 and the TRS f(x,y) -> g(x,y)
2188 then the resulting TRS is obtained by replacing all boxes
2189 by corresponding left- and right-hand sides of rules:
2191 f(f(x,y),x_1) -> f(g(x,y),x_1)
2192 f(x_1,f(x,y)) -> f(x_1,g(x,y))
2193 g(f(x,y),u) -> g(g(x,y),u)
2194 g(z,f(x,y)) -> g(z,g(x,y))
2196 The reason for this requirement is that
2197 1) it eases the check whether the given system really consists
2198 of all rules - where one does not have to bother with
2200 2) the flat context closures have to be computed in any way.
2201 3) the overhead in the size is small, since for every
2202 flat-context there will be n new rules each being
2203 larger than the the context.</xs:documentation>
2207 <xs:element name="flatContexts">
2209 <xs:group maxOccurs="unbounded" ref="context"/>
2212 <xs:element ref="trs"/>
2213 <xs:element ref="trsTerminationProof"/>
2217 <xs:element name="terminationAssumption">
2220 <xs:element ref="trsInput"/>
2224 <xs:element name="uncurry">
2226 <xs:documentation>eta-expand the TRS, uncurry it, and add the uncurrying rules
2231 <xs:element ref="uncurryInformation"/>
2232 <xs:element ref="trs"/>
2233 <xs:element ref="trsTerminationProof"/>
2237 <xs:element name="bounds">
2239 <xs:documentation>The final states are those which are used to accept the initial language like lift_0(T(Sigma)).</xs:documentation>
2243 <xs:element name="type">
2246 <xs:element name="roof"/>
2247 <xs:element name="match"/>
2251 <xs:element name="bound" type="xs:nonNegativeInteger"/>
2252 <xs:element name="finalStates">
2255 <xs:element maxOccurs="unbounded" minOccurs="0" ref="state"/>
2259 <xs:element ref="treeAutomaton"/>
2263 <xs:element name="switchInnermost">
2265 <xs:documentation>if R is WCR and overlay, then one can switch to innermost</xs:documentation>
2269 <xs:element ref="wcrProof"/>
2270 <xs:element ref="trsTerminationProof"/>
2274 <xs:element name="split">
2276 <xs:documentation>Proof termination of R by proving relative termination of D/(R-D) and termination of R - D.
2277 The rules D have to given, then the termination proof of D / R-D,
2278 and finally the termination proof of R - D.</xs:documentation>
2282 <xs:element ref="trs"/>
2283 <xs:element ref="trsTerminationProof"/>
2284 <xs:element ref="trsTerminationProof"/>
2291 <xs:element name="wcrProof">
2294 <xs:element name="joinableCriticalPairs">
2297 <xs:element maxOccurs="unbounded" minOccurs="0" name="joinableCriticalPair">
2299 <xs:documentation>List at least each non-trivial critical pair with the joining sequence. Here, the start-terms of the rewrite sequences form the critical pair.</xs:documentation>
2303 <xs:element ref="rewriteSequence"/>
2304 <xs:element ref="rewriteSequence"/>
2311 <xs:element name="joinableCriticalPairsAuto">
2313 <xs:documentation>just claim that all critical pairs are joinable
2314 (and let the certifier find out how to join)</xs:documentation>
2317 <xs:element name="joinableCriticalPairsBFS" type="xs:nonNegativeInteger">
2319 <xs:documentation>just claim that all critical pairs are joinable within n steps</xs:documentation>
2325 <xs:element name="proof">
2328 <xs:element ref="trsTerminationProof"/>
2329 <xs:element ref="trsNonterminationProof"/>
2330 <xs:element ref="relativeTerminationProof"/>
2331 <xs:element ref="relativeNonterminationProof"/>
2332 <xs:element ref="dpProof"/>
2333 <xs:element ref="dpNonterminationProof"/>
2334 <xs:element ref="orderingConstraintProof"/>
2335 <xs:element ref="wcrProof"/>
2336 <xs:element ref="crProof"/>
2337 <xs:element ref="crDisproof"/>
2338 <xs:element ref="completionProof"/>
2339 <xs:element ref="equationalProof"/>
2340 <xs:element ref="equationalDisproof"/>
2341 <xs:element ref="complexityProof"/>
2345 <xs:element name="certificationProblem">
2347 <xs:documentation>the root node of the certification problem format.
2352 <xs:element name="input">
2355 <xs:element ref="trsInput"/>
2356 <xs:element ref="dpInput"/>
2357 <xs:element ref="orderingConstraints"/>
2358 <xs:element name="completionInput">
2361 <xs:element ref="equations"/>
2362 <xs:element ref="trs"/>
2366 <xs:element name="equationalReasoningInput">
2369 <xs:element ref="equations"/>
2370 <xs:element name="equation">
2373 <xs:group ref="term"/>
2374 <xs:group ref="term"/>
2381 <xs:element name="complexityInput">
2384 <xs:element ref="trsInput"/>
2385 <xs:group ref="complexityMeasure"/>
2386 <xs:group ref="complexityClass"/>
2393 <xs:element name="cpfVersion" type="xs:string">
2395 <xs:documentation>current version number: 2.1</xs:documentation>
2398 <xs:element ref="proof"/>
2399 <xs:element name="origin">
2402 <xs:element name="proofOrigin">
2408 <xs:element maxOccurs="unbounded" name="tool">
2411 <xs:element name="name" type="xs:string"/>
2412 <xs:element name="version" type="xs:string"/>
2413 <xs:element minOccurs="0" name="strategy" type="xs:string"/>
2414 <xs:element minOccurs="0" ref="url"/>
2418 <xs:element maxOccurs="unbounded" minOccurs="0" name="toolUser">
2421 <xs:element name="firstName" type="xs:string"/>
2422 <xs:element name="lastName" type="xs:string"/>
2423 <xs:element minOccurs="0" ref="url"/>
2430 <xs:element name="inputOrigin" minOccurs="0">
2432 <xs:documentation>if the input was part of the TPDB, then the filename should include enough parts of the full path to identify the exact file. E.g. do not use "2.01.xml" but "TRS/SK90/2.01.xml".
2434 the source-element is some free form text that can otherwise describe the origin of the input, e.g., a link to a paper.</xs:documentation>
2438 <xs:element minOccurs="0" name="tpdbReference">
2441 <xs:element name="fileName" type="xs:string"/>
2442 <xs:element name="tpdbId" type="xs:long" minOccurs="0"/>
2446 <xs:element minOccurs="0" name="source" type="xs:string"/>