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="argumentFilter">
215 <xs:documentation>an argument filter consist of a mapping from symbols to collapsing or non-collapsing filters.
218 an entry f/3 -> collapsing/1 filters the ternary symbol f to its third argument.
219 an entry f/3 -> nonCollapsing/3 1 filters the term f(x,y,z) to f(z,x)
221 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>
225 <xs:element maxOccurs="unbounded" minOccurs="0" name="argumentFilterEntry">
228 <xs:group ref="symbol"/>
229 <xs:element ref="arity"/>
231 <xs:element name="collapsing" type="xs:positiveInteger"/>
232 <xs:element name="nonCollapsing">
235 <xs:element maxOccurs="unbounded" minOccurs="0" ref="position"/>
246 <xs:element name="domain">
249 <xs:element name="naturals"/>
250 <xs:element name="integers">
252 <xs:documentation>purpose: arctic below zero is arctic-integer</xs:documentation>
255 <xs:element name="rationals">
258 <xs:element name="delta">
261 <xs:group ref="number"/>
268 <xs:element name="arctic">
271 <xs:element ref="domain"/>
275 <xs:element name="tropical">
278 <xs:element ref="domain"/>
282 <xs:element name="matrices">
284 <xs:documentation>the domain of matrices where the elements are from the subdomain specified</xs:documentation>
288 <xs:element ref="dimension"/>
289 <xs:element ref="strictDimension">
291 <xs:documentation>in the upper left submatrix of this dimension there must be a strict decrease
292 (the remaining parts of the matrix is ignored for strict decreases, only weak decreases are required).</xs:documentation>
295 <xs:element ref="domain"/>
302 <xs:element name="redPair">
305 <xs:element name="interpretation">
308 <xs:element name="type">
311 <xs:element name="polynomial">
313 <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>
317 <xs:element ref="domain"/>
318 <xs:element ref="degree">
320 <xs:documentation>the maximal degree of the polynomial interpretation (some certifiers only support linear interpretations).
321 all interpretations given should respect this degree.
328 <xs:element name="matrixInterpretation">
330 <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>
334 <xs:element ref="domain"/>
335 <xs:element ref="dimension"/>
336 <xs:element ref="strictDimension">
338 <xs:documentation>in the upper subvector of this dimension there must be a strict decrease
339 (the lower part of the vector is ignored for strict decreases, only weak decreases are required).</xs:documentation>
348 <xs:element maxOccurs="unbounded" minOccurs="0" name="interpret">
351 <xs:group ref="symbol"/>
352 <xs:element ref="arity"/>
353 <xs:group ref="function"/>
360 <xs:element name="pathOrder">
363 <xs:element name="statusPrecedence">
366 <xs:element name="statusPrecedenceEntry" maxOccurs="unbounded" minOccurs="0">
368 <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>
372 <xs:group ref="symbol"/>
373 <xs:element ref="arity"/>
374 <xs:element name="precedence" type="xs:nonNegativeInteger">
376 <xs:documentation>higher numbers = higher precedence. Unspecified symbols obtain precedence 0.</xs:documentation>
380 <xs:element name="lex">
382 <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>
384 <xs:complexType> </xs:complexType>
386 <xs:element name="mul"/>
394 <xs:element minOccurs="0" ref="argumentFilter">
396 <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>
405 <xs:element name="arithFunction">
408 <xs:element name="natural" type="xs:nonNegativeInteger"/>
409 <xs:element name="variable" type="xs:positiveInteger"/>
410 <xs:element name="sum">
413 <xs:element maxOccurs="unbounded" ref="arithFunction"/>
417 <xs:element name="product">
420 <xs:element maxOccurs="unbounded" ref="arithFunction"/>
424 <xs:element name="min">
427 <xs:element maxOccurs="unbounded" ref="arithFunction"/>
431 <xs:element name="max">
434 <xs:element maxOccurs="unbounded" ref="arithFunction"/>
441 <xs:element name="model">
444 <xs:element name="finiteModel">
446 <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
451 <xs:element name="carrierSize" type="xs:positiveInteger"/>
452 <xs:element minOccurs="0" name="tupleOrder">
454 <xs:documentation>If this element is missing, then one uses semantic labeling in the model version.
456 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>
460 <xs:element name="pointWise">
462 <xs:documentation>here, (x1,..,xn) > (y1,...,yn) iff all xi >= yi and for some i: xi > yi</xs:documentation>
468 <xs:element maxOccurs="unbounded" minOccurs="0" name="interpret">
471 <xs:group ref="symbol"/>
472 <xs:element ref="arity"/>
473 <xs:element ref="arithFunction"/>
477 <xs:element name="labeling" minOccurs="0">
479 <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>
485 <xs:element name="rootLabeling">
487 <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>
491 <xs:group ref="symbol" minOccurs="0"/>
498 <xs:element name="dpProof">
501 <xs:element name="pIsEmpty">
503 <xs:documentation>trivial proof by stating that the set of DPs is empty</xs:documentation>
506 <xs:element name="depGraphProc">
508 <xs:documentation>split the current set of DPs into several smaller subproblems by using some DP-graph estimation.
509 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>
513 <xs:element maxOccurs="unbounded" minOccurs="0" name="component">
516 <xs:element ref="dps"/>
517 <xs:element name="realScc" type="xs:boolean">
519 <xs:documentation>may only be set to false, if component is singleton node without edge to itself.
520 if set to true, then proof for remaining DP problem has to be given</xs:documentation>
523 <xs:element minOccurs="0" name="arcs">
525 <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:
527 - not giving an arcs-element is always safe (but will slow down some certifiers)
528 - giving an <arcs/> element is only possible if there are no forward arcs
531 <forwardArc>2</forwardArc>
532 <forwardArc>7</forwardArc>
534 element states that there are only arcs to the components 2 and
535 7 positions further in the component-list.</xs:documentation>
539 <xs:element maxOccurs="unbounded" minOccurs="0" name="forwardArc"
540 type="xs:positiveInteger">
542 <xs:documentation>the idea is to make relative forward references by numbers:
552 can be represented in the component list
553 [ (A,B, real, 1,2), (C,nonreal,2), (E,real), (D,real) ]
555 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
557 (C) gets a forwardArc 2, since (D) is two elements later in the list.
559 In this way, one does not have do introduce numbers for the SCCs,
560 the SCC-DAG is present, and the list must be in topologic order,
561 since the forwardArcs are positive numbers only.
568 <xs:element minOccurs="0" ref="dpProof"/>
575 <xs:element name="redPairProc">
577 <xs:documentation>Use a reduction pair where only the non-strict order has to be monotone.
578 It allows to delete those DPs which are strictly oriented.
579 The remaining DPs have to be given.
581 If the ordering constraint proof is only an assumption, the orderingConstraints-element becomes mandatory.</xs:documentation>
585 <xs:element minOccurs="0" ref="orderingConstraints"/>
586 <xs:element ref="orderingConstraintProof"/>
587 <xs:element ref="dps"/>
588 <xs:element ref="dpProof"/>
592 <xs:element name="redPairUrProc">
594 <xs:documentation>Use a Ce-compatible reduction pair where only the non-strict order has to be monotone.
595 It allows to delete those DPs which are strictly oriented.
596 Here only the usable rules have to be weakly oriented.
598 If the ordering constraint proof is only an assumption, the orderingConstraints-element becomes mandatory.</xs:documentation>
602 <xs:element minOccurs="0" ref="orderingConstraints"/>
603 <xs:element ref="orderingConstraintProof"/>
604 <xs:element ref="dps"/>
605 <xs:element ref="usableRules"/>
606 <xs:element ref="dpProof"/>
610 <xs:element name="monoRedPairProc">
612 <xs:documentation>Use a reduction pair where both the non-strict and the strict order have to be monotone.
613 It allows to delete those DPs and those rules of the TRSs which are strictly oriented.
614 The remaining DPs and the remaining TRSs have to be given.
616 If the ordering constraint proof is only an assumption, the orderingConstraints-element becomes mandatory.</xs:documentation>
620 <xs:element minOccurs="0" ref="orderingConstraints"/>
621 <xs:element ref="orderingConstraintProof"/>
622 <xs:element ref="dps"/>
623 <xs:element ref="trs"/>
624 <xs:element ref="dpProof"/>
628 <xs:element name="monoRedPairUrProc">
630 <xs:documentation>Use a Ce-compatible reduction pair where both the non-strict and the strict order have to be monotone.
631 It allows to delete those DPs and those rules of the TRSs which are strictly oriented.
632 Moreover, all non-usable rules can also be deleted.
633 Here, only the usable rules instead of all rules of the TRS have to be oriented.
634 The remaining DPs and the remaining TRSs have to be given, as well as the usable rules.
636 If the ordering constraint proof is only an assumption, the orderingConstraints-element becomes mandatory.</xs:documentation>
640 <xs:element minOccurs="0" ref="orderingConstraints"/>
641 <xs:element ref="orderingConstraintProof"/>
642 <xs:element ref="dps"/>
643 <xs:element ref="trs"/>
644 <xs:element ref="usableRules"/>
645 <xs:element ref="dpProof"/>
649 <xs:element name="subtermProc">
651 <xs:documentation>Use the subterm criterion to delete some DPs.
652 Only collapsing argument filters or identity filters may be used.
653 The remaining DPs have to be given. The subterm criterion can also be used in combination wirth rewrite sequences.</xs:documentation>
657 <xs:element ref="argumentFilter"/>
658 <xs:element maxOccurs="unbounded" minOccurs="0" name="projectedRewriteSequence">
660 <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.
662 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>
666 <xs:element ref="rule"/>
667 <xs:element ref="rewriteSequence"/>
671 <xs:element ref="dps"/>
672 <xs:element ref="dpProof"/>
676 <xs:element name="semlabProc">
678 <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.).
680 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>
684 <xs:element ref="model"/>
685 <xs:element ref="dps"/>
686 <xs:element ref="trs"/>
687 <xs:element ref="dpProof"/>
691 <xs:element name="unlabProc">
693 <xs:documentation>removes one layer of labels that were added by semantic labeling.</xs:documentation>
697 <xs:element ref="dps"/>
698 <xs:element ref="trs"/>
699 <xs:element ref="dpProof"/>
703 <xs:element name="sizeChangeProc">
705 <xs:documentation>the size-change criterion processor.
706 for each DP, one size-change graph has to be given.
707 the set of graphs must be size-change terminating.
708 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.
709 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.
710 if not all rules are usable, then one has to use a Ce-compatible order.
713 DP: F(s(x),g(x)) -> F(id(x),g(x))
717 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>
722 <xs:element name="subtermCriterion"/>
723 <xs:element name="reductionPair">
725 <xs:documentation>The usable rules are optional. If they are used, a Ce-compatible order has to be used.
727 If the ordering constraint proof is only an assumption, the orderingConstraints-element becomes mandatory.</xs:documentation>
731 <xs:element minOccurs="0" ref="orderingConstraints"/>
732 <xs:element ref="orderingConstraintProof"/>
733 <xs:element ref="usableRules" minOccurs="0"/>
738 <xs:element maxOccurs="unbounded" minOccurs="0" name="sizeChangeGraph">
741 <xs:element ref="rule"/>
742 <xs:element maxOccurs="unbounded" minOccurs="0" name="edge">
744 <xs:documentation>an edge in a size change graph is always of the form
746 left-argument > / >= right-argument
748 position 0 corresponds to the whole term.</xs:documentation>
752 <xs:element name="position" type="xs:nonNegativeInteger"/>
753 <xs:element name="strict" type="xs:boolean"/>
754 <xs:element name="position" type="xs:nonNegativeInteger"/>
764 <xs:element name="flatContextClosureProc">
766 <xs:documentation>the flat context closure as required for the root labeling technique.
768 one also has to provide the list of flat contexts which
769 is used to fix the variable names in the resulting DP problem.
771 see the flat context closure technique for TRS for more explanations including an example.</xs:documentation>
775 <xs:element minOccurs="0" name="freshSymbol">
778 <xs:group ref="symbol"/>
782 <xs:element name="flatContexts">
784 <xs:group maxOccurs="unbounded" ref="context"/>
787 <xs:element ref="dps"/>
788 <xs:element ref="trs"/>
789 <xs:element ref="dpProof"/>
793 <xs:element name="argumentFilterProc">
795 <xs:documentation>just apply an argument filter and continue on the filtered DP problem</xs:documentation>
799 <xs:element ref="argumentFilter">
801 <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>
804 <xs:element ref="dps"/>
805 <xs:element ref="trs"/>
806 <xs:element ref="dpProof"/>
810 <xs:element name="uncurryProc">
812 <xs:documentation>if applicativeTop does not exist, then one
815 - and adds the uncurrying rules to R
816 (for the binary application symbol given in the uncurry information)
818 if applicativeTop is present (some number n), then the intention is that the application symbol is a tuple/marked symbol of arity n. Then
819 - the eta-expanded rules of R are added to P
820 - one uncurries P and R
821 - and adds the uncurrying rules to P</xs:documentation>
825 <xs:element name="applicativeTop" type="xs:positiveInteger" minOccurs="0"/>
826 <xs:element ref="uncurryInformation"/>
827 <xs:element ref="dps"/>
828 <xs:element ref="trs"/>
829 <xs:element ref="dpProof"/>
833 <xs:element name="finitenessAssumption">
836 <xs:element ref="dpInput"/>
843 <xs:element name="substitution">
846 <xs:element name="substEntry" maxOccurs="unbounded" minOccurs="0">
849 <xs:element ref="var"/>
850 <xs:group ref="term"/>
857 <xs:group name="context">
859 <xs:element name="box"/>
860 <xs:element name="funContext">
863 <xs:group ref="symbol"/>
864 <xs:element name="before">
866 <xs:group maxOccurs="unbounded" minOccurs="0" ref="term"/>
869 <xs:group ref="context"/>
870 <xs:element name="after">
872 <xs:group maxOccurs="unbounded" minOccurs="0" ref="term"/>
880 <xs:element name="rewriteSequence">
882 <xs:documentation>if t_0 is startterm, and there are rewrite-steps p_i, rule_i, t_i (for i = 1..n)
883 then t_{i-1} ->_{p_i,rule_i} t_i for all i=1..n
885 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>
889 <xs:element name="startTerm">
892 <xs:group ref="term"/>
896 <xs:element maxOccurs="unbounded" name="rewriteStep" minOccurs="0">
899 <xs:element name="positionInTerm">
902 <xs:element ref="position" maxOccurs="unbounded" minOccurs="0"/>
906 <xs:element ref="rule"/>
907 <xs:element minOccurs="0" name="relative"/>
908 <xs:group ref="term"/>
915 <xs:element name="state" type="xs:string">
917 <xs:documentation>the state of a tree automation</xs:documentation>
920 <xs:element name="trsTerminationProof">
923 <xs:element name="rIsEmpty">
925 <xs:documentation>state that the TRS is terminating since it has no rules</xs:documentation>
929 <xs:element name="ruleRemoval">
931 <xs:documentation>use a reduction pair where both the weak and the strict ordering are monotone.
932 Delete all strictly decreasing rules.
933 The remaining rules have to be given.
935 If the ordering constraint proof is only an assumption, the orderingConstraints-element becomes mandatory.</xs:documentation>
939 <xs:element minOccurs="0" ref="orderingConstraints"/>
940 <xs:element ref="orderingConstraintProof"/>
941 <xs:element ref="trs"/>
942 <xs:element ref="trsTerminationProof"/>
946 <xs:element name="dpTrans">
948 <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>
952 <xs:element ref="dps"/>
953 <xs:element name="markedSymbols" type="xs:boolean"/>
954 <xs:element ref="dpProof"/>
958 <xs:element name="semlab">
960 <xs:documentation>Use the semantic labeling . The model element determines the kind (model or quasi-model version, label, root-labeling, etc.)
962 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>
966 <xs:element ref="model"/>
967 <xs:element ref="trs"/>
968 <xs:element ref="trsTerminationProof"/>
972 <xs:element name="unlab">
974 <xs:documentation>removes one layer of labels that were added by semantic labeling.</xs:documentation>
978 <xs:element ref="trs"/>
979 <xs:element ref="trsTerminationProof"/>
983 <xs:element name="stringReversal">
985 <xs:documentation>reverse the strings in a TRS, i.e., replace f(g(h(x))) -> f(x) by h(g(f(x))) -> f(x).
986 Note that the variable in a reversed rule should be same as the variable in the original rule.</xs:documentation>
990 <xs:element ref="trs"/>
991 <xs:element ref="trsTerminationProof"/>
995 <xs:element name="flatContextClosure">
997 <xs:documentation>the flat context closure as required for the root labeling technique.
999 one also has to provide the list of flat contexts which
1000 is used to fix the variable names in the resulting TRS.
1002 example: if the flat contexts are
1008 and the TRS f(x,y) -> g(x,y)
1010 then the resulting TRS is obtained by replacing all boxes
1011 by corresponding left- and right-hand sides of rules:
1013 f(f(x,y),x_1) -> f(g(x,y),x_1)
1014 f(x_1,f(x,y)) -> f(x_1,g(x,y))
1015 g(f(x,y),u) -> g(g(x,y),u)
1016 g(z,f(x,y)) -> g(z,g(x,y))
1018 The reason for this requirement is that
1019 1) it eases the check whether the given system really consists
1020 of all rules - where one does not have to bother with
1022 2) the flat context closures have to be computed in any way.
1023 3) the overhead in the size is small, since for every
1024 flat-context there will be n new rules each being
1025 larger than the the context.</xs:documentation>
1029 <xs:element name="flatContexts">
1031 <xs:group maxOccurs="unbounded" ref="context"/>
1034 <xs:element ref="trs"/>
1035 <xs:element ref="trsTerminationProof"/>
1039 <xs:element name="terminationAssumption">
1042 <xs:element ref="trsInput"/>
1046 <xs:element name="uncurry">
1048 <xs:documentation>eta-expand the TRS, uncurry it, and add the uncurrying rules
1053 <xs:element ref="uncurryInformation"/>
1054 <xs:element ref="trs"/>
1055 <xs:element ref="trsTerminationProof"/>
1059 <xs:element name="bounds">
1061 <xs:documentation>The final states are those which are used to accept the initial language like lift_0(T(Sigma)).</xs:documentation>
1065 <xs:element name="type">
1068 <xs:element name="roof"/>
1069 <xs:element name="match"/>
1073 <xs:element name="bound" type="xs:nonNegativeInteger"/>
1074 <xs:element name="finalStates">
1077 <xs:element maxOccurs="unbounded" minOccurs="0" ref="state"/>
1081 <xs:element ref="treeAutomaton"/>
1088 <xs:element name="treeAutomaton">
1091 <xs:element name="finalStates">
1094 <xs:element maxOccurs="unbounded" minOccurs="0" ref="state"/>
1098 <xs:element name="transitions">
1101 <xs:element maxOccurs="unbounded" minOccurs="0" name="transition">
1104 <xs:element name="lhs">
1108 <xs:group ref="symbol"/>
1109 <xs:element minOccurs="0" name="height" type="xs:nonNegativeInteger"/>
1110 <xs:element maxOccurs="unbounded" minOccurs="0" ref="state"/>
1112 <xs:element ref="state"/>
1116 <xs:element name="rhs">
1119 <xs:element ref="state"/>
1132 <xs:element name="uncurryInformation">
1134 <xs:documentation>the uncurrying information consists of:
1135 - the application symbol
1136 - the names of the uncurried symbols
1137 - the uncurrying rules
1138 - the additional rules that are obtained when eta-expanding the TRS
1143 <xs:group ref="symbol"/>
1144 <xs:element name="uncurriedSymbols">
1147 <xs:element maxOccurs="unbounded" name="uncurriedSymbolEntry">
1149 <xs:documentation>mark for each original symbols the new uncurried symbols:
1150 if the constant map should now be uncurried up to two levels then
1151 there should be a symbol map entry
1152 map (we want to uncurry map)
1153 0 (the original arity of map)
1154 map (the new constant)
1155 map1 (the new unary symbol)
1156 map2 (the new binary symbol)
1158 Note that the names can be chosen arbitrarily</xs:documentation>
1162 <xs:group ref="symbol"/>
1163 <xs:element ref="arity"/>
1164 <xs:group ref="symbol" maxOccurs="unbounded"/>
1171 <xs:element name="uncurryRules">
1174 <xs:element ref="rules"/>
1178 <xs:element name="etaRules">
1181 <xs:element ref="rules"/>
1188 <xs:element name="loop">
1190 <xs:documentation>a loop is given by a (non-empty) rewrite-sequence t0 ->+ tn where additionally tn = C[t0 sigma]</xs:documentation>
1194 <xs:element ref="rewriteSequence"/>
1195 <xs:element ref="substitution"/>
1196 <xs:group ref="context"/>
1200 <xs:element name="trsNonterminationProof">
1203 <xs:element name="variableConditionViolated">
1205 <xs:documentation>there is a rule where the lhs is a variable, or the rhs contains variables not occurring in the lhs.</xs:documentation>
1209 <xs:element name="ruleRemoval">
1211 <xs:documentation>Remove some rules to figure out the really nonterminating TRS.</xs:documentation>
1215 <xs:element ref="trs"/>
1216 <xs:element ref="trsNonterminationProof"/>
1220 <xs:element name="stringReversal">
1222 <xs:documentation>reverse the strings in a TRS, i.e., replace f(g(h(x))) -> f(x) by h(g(f(x))) -> f(x).
1223 Note that the variable in a reversed rule should be same as the variable in the original rule.</xs:documentation>
1227 <xs:element ref="trs"/>
1228 <xs:element ref="trsNonterminationProof"/>
1232 <xs:element ref="loop"/>
1233 <xs:element name="dpTrans">
1235 <xs:documentation>switch to DPs as complete termination technique. See dpTrans within dpProof for other details</xs:documentation>
1239 <xs:element ref="dps"/>
1240 <xs:element name="markedSymbols" type="xs:boolean"/>
1241 <xs:element ref="dpNonterminationProof"/>
1245 <xs:element name="nonterminationAssumption">
1248 <xs:element ref="trsInput"/>
1255 <xs:element name="relativeTerminationProof">
1258 <xs:element name="rIsEmpty">
1260 <xs:documentation>state that the R/S is relative terminating since R has no rules</xs:documentation>
1264 <xs:element name="sIsEmpty">
1266 <xs:documentation>state that the R/S is relative terminating by termination of R since S has no rules</xs:documentation>
1270 <xs:element ref="trsTerminationProof"/>
1274 <xs:element name="ruleRemoval">
1276 <xs:documentation>use a reduction pair where both the weak and the strict ordering are monotone.
1277 Delete all strictly decreasing rules from R and S.
1278 The remaining rules of first R and then S have to be given.
1280 If the ordering constraint proof is only an assumption, the orderingConstraints-element becomes mandatory.</xs:documentation>
1284 <xs:element minOccurs="0" ref="orderingConstraints"/>
1285 <xs:element ref="orderingConstraintProof"/>
1286 <xs:element ref="trs"/>
1287 <xs:element ref="trs"/>
1288 <xs:element ref="relativeTerminationProof"/>
1292 <xs:element name="semlab">
1294 <xs:documentation>Use the semantic labeling . The model element determines the kind (model or quasi-model version, label, root-labeling, etc.)
1295 Both the labeled version of R and S have to be given (first R, then S).
1297 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>
1301 <xs:element ref="model"/>
1302 <xs:element ref="trs"/>
1303 <xs:element ref="trs"/>
1304 <xs:element ref="relativeTerminationProof"/>
1308 <xs:element name="unlab">
1310 <xs:documentation>removes one layer of labels that were added by semantic labeling. (first R, then S, as usual)</xs:documentation>
1314 <xs:element ref="trs"/>
1315 <xs:element ref="trs"/>
1316 <xs:element ref="relativeTerminationProof"/>
1320 <xs:element name="stringReversal">
1322 <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).
1323 Note that the variable in a reversed rule should be same as the variable in the original rule.</xs:documentation>
1327 <xs:element ref="trs"/>
1328 <xs:element ref="trs"/>
1329 <xs:element ref="relativeTerminationProof"/>
1333 <xs:element name="relativeTerminationAssumption">
1336 <xs:element ref="trsInput"/>
1340 <xs:element name="uncurry">
1342 <xs:documentation>eta-expand both TRSs, uncurry them, and add the uncurrying rules to the relative part
1347 <xs:element ref="uncurryInformation"/>
1348 <xs:element ref="trs"/>
1349 <xs:element ref="trs"/>
1350 <xs:element ref="relativeTerminationProof"/>
1357 <xs:element name="dpNonterminationProof">
1360 <xs:element ref="loop"/>
1361 <xs:element name="dpRuleRemoval">
1363 <xs:documentation>Remove some rules or DPs to figure out the really nonterminating DP problem (remaining 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.
1368 <xs:element ref="dps"/>
1369 <xs:element ref="trs"/>
1370 <xs:element ref="dpNonterminationProof"/>
1374 <xs:element name="infinitenessAssumption">
1377 <xs:element ref="dpInput"/>
1384 <xs:element name="relativeNonterminationProof">
1387 <xs:element ref="loop"/>
1388 <xs:element ref="trsNonterminationProof"/>
1389 <xs:element name="variableConditionViolated">
1391 <xs:documentation>there is a rule where the lhs is a variable, or the rhs contains variables not occurring in the lhs.</xs:documentation>
1395 <xs:element name="ruleRemoval">
1397 <xs:documentation>Remove some rules to figure out the really nonterminating TRSs. (as usual, first R, then S)</xs:documentation>
1401 <xs:element ref="trs"/>
1402 <xs:element ref="trs"/>
1403 <xs:element ref="relativeNonterminationProof"/>
1407 <xs:element name="nonterminationAssumption">
1410 <xs:element ref="trsInput"/>
1417 <xs:element name="orderingConstraints">
1419 <xs:documentation>every strict order has to be well-founded.
1420 every strict order > has to be compatible with all orders >' (both strict and non-strict):
1421 Here, compatible between a strict order > and >' is defined as:
1422 s > t and t >' u implies s > u, and similarly, s >' t and t > u implies s > u.
1423 every order has to be stable.
1424 The demand for monotonicity, etc. is specified by the corresponding sub-elements.</xs:documentation>
1428 <xs:element maxOccurs="unbounded" name="orderingConstraintElement">
1431 <xs:element name="strict" type="xs:boolean"/>
1432 <xs:element name="ceCompatible" type="xs:boolean"/>
1433 <xs:element minOccurs="0" name="monotonePositions">
1435 <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>
1439 <xs:element ref="argumentFilter">
1441 <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>
1444 <xs:element name="everySymbolAndPosition"/>
1448 <xs:element minOccurs="0" name="ignoredPositions">
1450 <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>
1454 <xs:element ref="argumentFilter">
1456 <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>
1462 <xs:element maxOccurs="unbounded" minOccurs="0" ref="rule"/>
1469 <xs:element name="orderingConstraintProof">
1472 <xs:element ref="redPair"/>
1473 <xs:element name="satisfiableAssumption">
1476 <xs:element ref="orderingConstraints"/>
1483 <xs:element name="proof">
1486 <xs:element ref="trsTerminationProof"/>
1487 <xs:element ref="trsNonterminationProof"/>
1488 <xs:element ref="relativeTerminationProof"/>
1489 <xs:element ref="relativeNonterminationProof"/>
1490 <xs:element ref="dpProof"/>
1491 <xs:element ref="dpNonterminationProof"/>
1492 <xs:element ref="orderingConstraintProof"/>
1496 <xs:element name="url" type="xs:string"/>
1497 <xs:element name="trsInput">
1499 <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>
1503 <xs:element ref="trs"/>
1504 <xs:element minOccurs="0" ref="strategy"/>
1505 <xs:element minOccurs="0" name="equations">
1508 <xs:element ref="rules"/>
1512 <xs:element name="relativeRules" minOccurs="0">
1515 <xs:element ref="rules"/>
1522 <xs:element name="dpInput">
1525 <xs:element ref="trs"/>
1526 <xs:element ref="dps"/>
1527 <xs:element ref="strategy"/>
1528 <xs:element name="minimal" type="xs:boolean"/>
1532 <xs:element name="strategy">
1534 <xs:documentation>no strategy means standard rewriting without restrictions</xs:documentation>
1538 <xs:element ref="innermost"/>
1542 <xs:element name="innermost"/>
1543 <xs:element name="certificationProblem">
1545 <xs:documentation>the root node of the certification problem format.
1550 <xs:element name="input">
1553 <xs:element ref="trsInput"/>
1554 <xs:element ref="dpInput"/>
1555 <xs:element ref="orderingConstraints"/>
1559 <xs:element name="cpfVersion" type="xs:string">
1561 <xs:documentation>current version number: 2.1</xs:documentation>
1564 <xs:element ref="proof"/>
1565 <xs:element name="origin">
1568 <xs:element name="proofOrigin">
1574 <xs:element maxOccurs="unbounded" name="tool">
1577 <xs:element name="name" type="xs:string"/>
1578 <xs:element name="version" type="xs:string"/>
1579 <xs:element minOccurs="0" name="strategy" type="xs:string"/>
1580 <xs:element minOccurs="0" ref="url"/>
1584 <xs:element maxOccurs="unbounded" minOccurs="0" name="toolUser">
1587 <xs:element name="firstName" type="xs:string"/>
1588 <xs:element name="lastName" type="xs:string"/>
1589 <xs:element minOccurs="0" ref="url"/>
1596 <xs:element name="inputOrigin" minOccurs="0">
1598 <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".
1600 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>
1604 <xs:element minOccurs="0" name="tpdbReference">
1607 <xs:element name="fileName" type="xs:string"/>
1608 <xs:element name="tpdbId" type="xs:long" minOccurs="0"/>
1612 <xs:element minOccurs="0" name="source" type="xs:string"/>