Left Termination of the query pattern
ordered(g)
w.r.t. the given Prolog program could successfully be proven:

(0) Obligation:

Clauses:

ordered([]).
ordered(.(X1, [])).
ordered(.(X, .(Y, Xs))) :- ','(less(X, s(Y)), ordered(.(Y, Xs))).
less(0, s(X2)).
less(s(X), s(Y)) :- less(X, Y).

Query: ordered(g)

(1) PrologToPiTRSViaGraphTransformerProof (SOUND transformation)

Transformed Prolog program to (Pi-)TRS.

digraph dp_graph {
node [outthreshold=100, inthreshold=100];
3 [label="A: ordered(T1)\n\nT1 is ground", fontsize=16, style=filled, fillcolor=lightyellow, color=red];
6 [label="6: ordered(T1), SCOPE: 1, CLAUSE: 0 | ordered(T1), SCOPE: 1, CLAUSE: 1 | ordered(T1), SCOPE: 1, CLAUSE: 2\n\nT1 is ground", fontsize=16, style=filled, fillcolor=lightyellow];
10 [label="10: true | ordered([]), SCOPE: 1, CLAUSE: 1 | ordered([]), SCOPE: 1, CLAUSE: 2\n\n", fontsize=16, style=filled, fillcolor=lightyellow];
11 [label="11: ordered(T1), SCOPE: 1, CLAUSE: 1 | ordered(T1), SCOPE: 1, CLAUSE: 2\n\nT1 is ground\nordered(T1) !=? ordered([])", fontsize=16, style=filled, fillcolor=lightyellow];
17 [label="17: ordered([]), SCOPE: 1, CLAUSE: 1 | ordered([]), SCOPE: 1, CLAUSE: 2\n\n", fontsize=16, style=filled, fillcolor=lightyellow];
19 [label="19: ordered([]), SCOPE: 1, CLAUSE: 2\n\n", fontsize=16, style=filled, fillcolor=lightyellow];
23 [label="23: \n\n", fontsize=16, style=filled, fillcolor=lightyellow];
28 [label="28: true | ordered(.(T3, [])), SCOPE: 1, CLAUSE: 2\n\nT3 is ground", fontsize=16, style=filled, fillcolor=lightyellow];
30 [label="30: ordered(T1), SCOPE: 1, CLAUSE: 2\n\nT1 is ground\nX8 is free\nordered(T1) !=? ordered([])\nordered(T1) !=? ordered(.(X8, []))", fontsize=16, style=filled, fillcolor=lightyellow];
32 [label="32: ordered(.(T3, [])), SCOPE: 1, CLAUSE: 2\n\nT3 is ground", fontsize=16, style=filled, fillcolor=lightyellow];
34 [label="34: \n\n", fontsize=16, style=filled, fillcolor=lightyellow];
36 [label="36: ','(less(T8, s(T9)), ordered(.(T9, T10)))\n\nT8 is ground\nT9 is ground\nT10 is ground", fontsize=16, style=filled, fillcolor=lightyellow];
38 [label="38: \n\n", fontsize=16, style=filled, fillcolor=lightyellow];
40 [label="40: ','(less(T8, s(T9)), ordered(.(T9, T10))), SCOPE: 2, CLAUSE: 3 | ','(less(T8, s(T9)), ordered(.(T9, T10))), SCOPE: 2, CLAUSE: 4\n\nT8 is ground\nT9 is ground\nT10 is ground", fontsize=16, style=filled, fillcolor=lightyellow];
45 [label="45: ','(less(T8, s(T9)), ordered(.(T9, T10))), SCOPE: 2, CLAUSE: 3\n\nT8 is ground\nT9 is ground\nT10 is ground", fontsize=16, style=filled, fillcolor=lightyellow];
46 [label="46: ','(less(T8, s(T9)), ordered(.(T9, T10))), SCOPE: 2, CLAUSE: 4\n\nT8 is ground\nT9 is ground\nT10 is ground", fontsize=16, style=filled, fillcolor=lightyellow];
48 [label="48: ordered(.(T15, T10))\n\nT10 is ground\nT15 is ground", fontsize=16, style=filled, fillcolor=lightyellow];
50 [label="50: \n\n", fontsize=16, style=filled, fillcolor=lightyellow];
54 [label="B: ','(less(T20, T21), ordered(.(T21, T10)))\n\nT10 is ground\nT20 is ground\nT21 is ground", fontsize=16, style=filled, fillcolor=lightyellow];
56 [label="56: \n\n", fontsize=16, style=filled, fillcolor=lightyellow];
59 [label="C: less(T20, T21)\n\nT20 is ground\nT21 is ground", fontsize=16, style=filled, fillcolor=lightyellow];
60 [label="60: ordered(.(T21, T10))\n\nT10 is ground\nT21 is ground", fontsize=16, style=filled, fillcolor=lightyellow];
65 [label="65: less(T20, T21), SCOPE: 3, CLAUSE: 3 | less(T20, T21), SCOPE: 3, CLAUSE: 4\n\nT20 is ground\nT21 is ground", fontsize=16, style=filled, fillcolor=lightyellow];
67 [label="67: less(T20, T21), SCOPE: 3, CLAUSE: 3\n\nT20 is ground\nT21 is ground", fontsize=16, style=filled, fillcolor=lightyellow];
69 [label="69: less(T20, T21), SCOPE: 3, CLAUSE: 4\n\nT20 is ground\nT21 is ground", fontsize=16, style=filled, fillcolor=lightyellow];
73 [label="73: true\n\n", fontsize=16, style=filled, fillcolor=lightyellow];
74 [label="74: \n\n", fontsize=16, style=filled, fillcolor=lightyellow];
75 [label="75: \n\n", fontsize=16, style=filled, fillcolor=lightyellow];
81 [label="81: less(T35, T36)\n\nT35 is ground\nT36 is ground", fontsize=16, style=filled, fillcolor=lightyellow];
90 [label="90: \n\n", fontsize=16, style=filled, fillcolor=lightyellow];
91 [label="CASE", fontsize=14, style = filled, fillcolor = lightcyan];
3 -> 91 [arrowhead = none ];
91 -> 6;

92 [label="EVAL with clause\nordered([]).\nand substitutionT1 -> []", fontsize=14, style = filled, fillcolor = lightblue];
6 -> 92 [arrowhead = none ];
92 -> 10;

93 [label="EVAL-BACKTRACK", fontsize=14, style = filled, fillcolor = lightgreen];
6 -> 93 [arrowhead = none ];
93 -> 11;

94 [label="SUCCESS", fontsize=14, style = filled, fillcolor = lightgreen];
10 -> 94 [arrowhead = none ];
94 -> 17;

95 [label="EVAL with clause\nordered(.(X8, [])).\nand substitutionX8 -> T3,\nT1 -> .(T3, [])", fontsize=14, style = filled, fillcolor = lightblue];
11 -> 95 [arrowhead = none ];
95 -> 28;

96 [label="EVAL-BACKTRACK", fontsize=14, style = filled, fillcolor = lightgreen];
11 -> 96 [arrowhead = none ];
96 -> 30;

97 [label="BACKTRACK\nfor clause: ordered(.(X1, []))because of non-unification", fontsize=14, style = filled, fillcolor = lightgreen];
17 -> 97 [arrowhead = none ];
97 -> 19;

98 [label="BACKTRACK\nfor clause: ordered(.(X, .(Y, Xs))) :- ','(less(X, s(Y)), ordered(.(Y, Xs)))because of non-unification", fontsize=14, style = filled, fillcolor = lightgreen];
19 -> 98 [arrowhead = none ];
98 -> 23;

99 [label="SUCCESS", fontsize=14, style = filled, fillcolor = lightgreen];
28 -> 99 [arrowhead = none ];
99 -> 32;

100 [label="EVAL with clause\nordered(.(X15, .(X16, X17))) :- ','(less(X15, s(X16)), ordered(.(X16, X17))).\nand substitutionX15 -> T8,\nX16 -> T9,\nX17 -> T10,\nT1 -> .(T8, .(T9, T10))", fontsize=14, style = filled, fillcolor = lightblue];
30 -> 100 [arrowhead = none ];
100 -> 36;

101 [label="EVAL-BACKTRACK", fontsize=14, style = filled, fillcolor = lightgreen];
30 -> 101 [arrowhead = none ];
101 -> 38;

102 [label="BACKTRACK\nfor clause: ordered(.(X, .(Y, Xs))) :- ','(less(X, s(Y)), ordered(.(Y, Xs)))because of non-unification", fontsize=14, style = filled, fillcolor = lightgreen];
32 -> 102 [arrowhead = none ];
102 -> 34;

103 [label="CASE", fontsize=14, style = filled, fillcolor = lightcyan];
36 -> 103 [arrowhead = none ];
103 -> 40;

104 [label="PARALLEL", fontsize=14, style = filled, fillcolor = violet];
40 -> 104 [arrowhead = none ];
104 -> 45;

105 [label="PARALLEL", fontsize=14, style = filled, fillcolor = violet];
40 -> 105 [arrowhead = none ];
105 -> 46;

106 [label="EVAL with clause\nless(0, s(X22)).\nand substitutionT8 -> 0,\nT9 -> T15,\nX22 -> T15", fontsize=14, style = filled, fillcolor = lightblue];
45 -> 106 [arrowhead = none ];
106 -> 48;

107 [label="EVAL-BACKTRACK", fontsize=14, style = filled, fillcolor = lightgreen];
45 -> 107 [arrowhead = none ];
107 -> 50;

108 [label="EVAL with clause\nless(s(X27), s(X28)) :- less(X27, X28).\nand substitutionX27 -> T20,\nT8 -> s(T20),\nT9 -> T21,\nX28 -> T21", fontsize=14, style = filled, fillcolor = lightblue];
46 -> 108 [arrowhead = none ];
108 -> 54;

109 [label="EVAL-BACKTRACK", fontsize=14, style = filled, fillcolor = lightgreen];
46 -> 109 [arrowhead = none ];
109 -> 56;

110 [label="INSTANCE with matching:\nT1 -> .(T15, T10)", fontsize=14, style = filled, fillcolor = lightgrey];
48 -> 110 [arrowhead = none , style=dashed];
110 -> 3[style=dashed];

111 [label="SPLIT 1", fontsize=14, style = filled, fillcolor = violet];
54 -> 111 [arrowhead = none ];
111 -> 59;

112 [label="SPLIT 2\nnew knowledge:\nT20 is ground\nT21 is ground", fontsize=14, style = filled, fillcolor = violet];
54 -> 112 [arrowhead = none ];
112 -> 60;

113 [label="CASE", fontsize=14, style = filled, fillcolor = lightcyan];
59 -> 113 [arrowhead = none ];
113 -> 65;

114 [label="INSTANCE with matching:\nT1 -> .(T21, T10)", fontsize=14, style = filled, fillcolor = lightgrey];
60 -> 114 [arrowhead = none , style=dashed];
114 -> 3[style=dashed];

115 [label="PARALLEL", fontsize=14, style = filled, fillcolor = violet];
65 -> 115 [arrowhead = none ];
115 -> 67;

116 [label="PARALLEL", fontsize=14, style = filled, fillcolor = violet];
65 -> 116 [arrowhead = none ];
116 -> 69;

117 [label="EVAL with clause\nless(0, s(X37)).\nand substitutionT20 -> 0,\nX37 -> T30,\nT21 -> s(T30)", fontsize=14, style = filled, fillcolor = lightblue];
67 -> 117 [arrowhead = none ];
117 -> 73;

118 [label="EVAL-BACKTRACK", fontsize=14, style = filled, fillcolor = lightgreen];
67 -> 118 [arrowhead = none ];
118 -> 74;

119 [label="EVAL with clause\nless(s(X42), s(X43)) :- less(X42, X43).\nand substitutionX42 -> T35,\nT20 -> s(T35),\nX43 -> T36,\nT21 -> s(T36)", fontsize=14, style = filled, fillcolor = lightblue];
69 -> 119 [arrowhead = none ];
119 -> 81;

120 [label="EVAL-BACKTRACK", fontsize=14, style = filled, fillcolor = lightgreen];
69 -> 120 [arrowhead = none ];
120 -> 90;

121 [label="SUCCESS", fontsize=14, style = filled, fillcolor = lightgreen];
73 -> 121 [arrowhead = none ];
121 -> 75;

122 [label="INSTANCE with matching:\nT20 -> T35\nT21 -> T36", fontsize=14, style = filled, fillcolor = lightgrey];
81 -> 122 [arrowhead = none , style=dashed];
122 -> 59[style=dashed];

}

(2) Obligation:

Pi-finite rewrite system:
The TRS R consists of the following rules:

orderedA_in_g([]) → orderedA_out_g([])
orderedA_in_g(.(T3, [])) → orderedA_out_g(.(T3, []))
orderedA_in_g(.(0, .(T15, T10))) → U1_g(T15, T10, orderedA_in_g(.(T15, T10)))
orderedA_in_g(.(s(T20), .(T21, T10))) → U2_g(T20, T21, T10, pB_in_ggg(T20, T21, T10))
pB_in_ggg(T20, T21, T10) → U4_ggg(T20, T21, T10, lessC_in_gg(T20, T21))
lessC_in_gg(0, s(T30)) → lessC_out_gg(0, s(T30))
lessC_in_gg(s(T35), s(T36)) → U3_gg(T35, T36, lessC_in_gg(T35, T36))
U3_gg(T35, T36, lessC_out_gg(T35, T36)) → lessC_out_gg(s(T35), s(T36))
U4_ggg(T20, T21, T10, lessC_out_gg(T20, T21)) → U5_ggg(T20, T21, T10, orderedA_in_g(.(T21, T10)))
U5_ggg(T20, T21, T10, orderedA_out_g(.(T21, T10))) → pB_out_ggg(T20, T21, T10)
U2_g(T20, T21, T10, pB_out_ggg(T20, T21, T10)) → orderedA_out_g(.(s(T20), .(T21, T10)))
U1_g(T15, T10, orderedA_out_g(.(T15, T10))) → orderedA_out_g(.(0, .(T15, T10)))

Pi is empty.

(3) DependencyPairsProof (EQUIVALENT transformation)

Using Dependency Pairs [AG00,LOPSTR] we result in the following initial DP problem:
Pi DP problem:
The TRS P consists of the following rules:

ORDEREDA_IN_G(.(0, .(T15, T10))) → U1_G(T15, T10, orderedA_in_g(.(T15, T10)))
ORDEREDA_IN_G(.(0, .(T15, T10))) → ORDEREDA_IN_G(.(T15, T10))
ORDEREDA_IN_G(.(s(T20), .(T21, T10))) → U2_G(T20, T21, T10, pB_in_ggg(T20, T21, T10))
ORDEREDA_IN_G(.(s(T20), .(T21, T10))) → PB_IN_GGG(T20, T21, T10)
PB_IN_GGG(T20, T21, T10) → U4_GGG(T20, T21, T10, lessC_in_gg(T20, T21))
PB_IN_GGG(T20, T21, T10) → LESSC_IN_GG(T20, T21)
LESSC_IN_GG(s(T35), s(T36)) → U3_GG(T35, T36, lessC_in_gg(T35, T36))
LESSC_IN_GG(s(T35), s(T36)) → LESSC_IN_GG(T35, T36)
U4_GGG(T20, T21, T10, lessC_out_gg(T20, T21)) → U5_GGG(T20, T21, T10, orderedA_in_g(.(T21, T10)))
U4_GGG(T20, T21, T10, lessC_out_gg(T20, T21)) → ORDEREDA_IN_G(.(T21, T10))

The TRS R consists of the following rules:

orderedA_in_g([]) → orderedA_out_g([])
orderedA_in_g(.(T3, [])) → orderedA_out_g(.(T3, []))
orderedA_in_g(.(0, .(T15, T10))) → U1_g(T15, T10, orderedA_in_g(.(T15, T10)))
orderedA_in_g(.(s(T20), .(T21, T10))) → U2_g(T20, T21, T10, pB_in_ggg(T20, T21, T10))
pB_in_ggg(T20, T21, T10) → U4_ggg(T20, T21, T10, lessC_in_gg(T20, T21))
lessC_in_gg(0, s(T30)) → lessC_out_gg(0, s(T30))
lessC_in_gg(s(T35), s(T36)) → U3_gg(T35, T36, lessC_in_gg(T35, T36))
U3_gg(T35, T36, lessC_out_gg(T35, T36)) → lessC_out_gg(s(T35), s(T36))
U4_ggg(T20, T21, T10, lessC_out_gg(T20, T21)) → U5_ggg(T20, T21, T10, orderedA_in_g(.(T21, T10)))
U5_ggg(T20, T21, T10, orderedA_out_g(.(T21, T10))) → pB_out_ggg(T20, T21, T10)
U2_g(T20, T21, T10, pB_out_ggg(T20, T21, T10)) → orderedA_out_g(.(s(T20), .(T21, T10)))
U1_g(T15, T10, orderedA_out_g(.(T15, T10))) → orderedA_out_g(.(0, .(T15, T10)))

Pi is empty.
We have to consider all (P,R,Pi)-chains

(4) Obligation:

Pi DP problem:
The TRS P consists of the following rules:

ORDEREDA_IN_G(.(0, .(T15, T10))) → U1_G(T15, T10, orderedA_in_g(.(T15, T10)))
ORDEREDA_IN_G(.(0, .(T15, T10))) → ORDEREDA_IN_G(.(T15, T10))
ORDEREDA_IN_G(.(s(T20), .(T21, T10))) → U2_G(T20, T21, T10, pB_in_ggg(T20, T21, T10))
ORDEREDA_IN_G(.(s(T20), .(T21, T10))) → PB_IN_GGG(T20, T21, T10)
PB_IN_GGG(T20, T21, T10) → U4_GGG(T20, T21, T10, lessC_in_gg(T20, T21))
PB_IN_GGG(T20, T21, T10) → LESSC_IN_GG(T20, T21)
LESSC_IN_GG(s(T35), s(T36)) → U3_GG(T35, T36, lessC_in_gg(T35, T36))
LESSC_IN_GG(s(T35), s(T36)) → LESSC_IN_GG(T35, T36)
U4_GGG(T20, T21, T10, lessC_out_gg(T20, T21)) → U5_GGG(T20, T21, T10, orderedA_in_g(.(T21, T10)))
U4_GGG(T20, T21, T10, lessC_out_gg(T20, T21)) → ORDEREDA_IN_G(.(T21, T10))

The TRS R consists of the following rules:

orderedA_in_g([]) → orderedA_out_g([])
orderedA_in_g(.(T3, [])) → orderedA_out_g(.(T3, []))
orderedA_in_g(.(0, .(T15, T10))) → U1_g(T15, T10, orderedA_in_g(.(T15, T10)))
orderedA_in_g(.(s(T20), .(T21, T10))) → U2_g(T20, T21, T10, pB_in_ggg(T20, T21, T10))
pB_in_ggg(T20, T21, T10) → U4_ggg(T20, T21, T10, lessC_in_gg(T20, T21))
lessC_in_gg(0, s(T30)) → lessC_out_gg(0, s(T30))
lessC_in_gg(s(T35), s(T36)) → U3_gg(T35, T36, lessC_in_gg(T35, T36))
U3_gg(T35, T36, lessC_out_gg(T35, T36)) → lessC_out_gg(s(T35), s(T36))
U4_ggg(T20, T21, T10, lessC_out_gg(T20, T21)) → U5_ggg(T20, T21, T10, orderedA_in_g(.(T21, T10)))
U5_ggg(T20, T21, T10, orderedA_out_g(.(T21, T10))) → pB_out_ggg(T20, T21, T10)
U2_g(T20, T21, T10, pB_out_ggg(T20, T21, T10)) → orderedA_out_g(.(s(T20), .(T21, T10)))
U1_g(T15, T10, orderedA_out_g(.(T15, T10))) → orderedA_out_g(.(0, .(T15, T10)))

Pi is empty.
We have to consider all (P,R,Pi)-chains

(5) DependencyGraphProof (EQUIVALENT transformation)

The approximation of the Dependency Graph [LOPSTR] contains 2 SCCs with 5 less nodes.

(6) Complex Obligation (AND)

(7) Obligation:

Pi DP problem:
The TRS P consists of the following rules:

LESSC_IN_GG(s(T35), s(T36)) → LESSC_IN_GG(T35, T36)

The TRS R consists of the following rules:

orderedA_in_g([]) → orderedA_out_g([])
orderedA_in_g(.(T3, [])) → orderedA_out_g(.(T3, []))
orderedA_in_g(.(0, .(T15, T10))) → U1_g(T15, T10, orderedA_in_g(.(T15, T10)))
orderedA_in_g(.(s(T20), .(T21, T10))) → U2_g(T20, T21, T10, pB_in_ggg(T20, T21, T10))
pB_in_ggg(T20, T21, T10) → U4_ggg(T20, T21, T10, lessC_in_gg(T20, T21))
lessC_in_gg(0, s(T30)) → lessC_out_gg(0, s(T30))
lessC_in_gg(s(T35), s(T36)) → U3_gg(T35, T36, lessC_in_gg(T35, T36))
U3_gg(T35, T36, lessC_out_gg(T35, T36)) → lessC_out_gg(s(T35), s(T36))
U4_ggg(T20, T21, T10, lessC_out_gg(T20, T21)) → U5_ggg(T20, T21, T10, orderedA_in_g(.(T21, T10)))
U5_ggg(T20, T21, T10, orderedA_out_g(.(T21, T10))) → pB_out_ggg(T20, T21, T10)
U2_g(T20, T21, T10, pB_out_ggg(T20, T21, T10)) → orderedA_out_g(.(s(T20), .(T21, T10)))
U1_g(T15, T10, orderedA_out_g(.(T15, T10))) → orderedA_out_g(.(0, .(T15, T10)))

Pi is empty.
We have to consider all (P,R,Pi)-chains

(8) UsableRulesProof (EQUIVALENT transformation)

For (infinitary) constructor rewriting [LOPSTR] we can delete all non-usable rules from R.

(9) Obligation:

Pi DP problem:
The TRS P consists of the following rules:

LESSC_IN_GG(s(T35), s(T36)) → LESSC_IN_GG(T35, T36)

R is empty.
Pi is empty.
We have to consider all (P,R,Pi)-chains

(10) PiDPToQDPProof (EQUIVALENT transformation)

Transforming (infinitary) constructor rewriting Pi-DP problem [LOPSTR] into ordinary QDP problem [LPAR04] by application of Pi.

(11) Obligation:

Q DP problem:
The TRS P consists of the following rules:

LESSC_IN_GG(s(T35), s(T36)) → LESSC_IN_GG(T35, T36)

R is empty.
Q is empty.
We have to consider all (P,Q,R)-chains.

(12) QDPSizeChangeProof (EQUIVALENT transformation)

By using the subterm criterion [SUBTERM_CRITERION] together with the size-change analysis [AAECC05] we have proven that there are no infinite chains for this DP problem.

From the DPs we obtained the following set of size-change graphs:

• LESSC_IN_GG(s(T35), s(T36)) → LESSC_IN_GG(T35, T36)
  The graph contains the following edges 1 > 1, 2 > 2

(13) YES

(14) Obligation:

Pi DP problem:
The TRS P consists of the following rules:

ORDEREDA_IN_G(.(s(T20), .(T21, T10))) → PB_IN_GGG(T20, T21, T10)
PB_IN_GGG(T20, T21, T10) → U4_GGG(T20, T21, T10, lessC_in_gg(T20, T21))
U4_GGG(T20, T21, T10, lessC_out_gg(T20, T21)) → ORDEREDA_IN_G(.(T21, T10))
ORDEREDA_IN_G(.(0, .(T15, T10))) → ORDEREDA_IN_G(.(T15, T10))

The TRS R consists of the following rules:

orderedA_in_g([]) → orderedA_out_g([])
orderedA_in_g(.(T3, [])) → orderedA_out_g(.(T3, []))
orderedA_in_g(.(0, .(T15, T10))) → U1_g(T15, T10, orderedA_in_g(.(T15, T10)))
orderedA_in_g(.(s(T20), .(T21, T10))) → U2_g(T20, T21, T10, pB_in_ggg(T20, T21, T10))
pB_in_ggg(T20, T21, T10) → U4_ggg(T20, T21, T10, lessC_in_gg(T20, T21))
lessC_in_gg(0, s(T30)) → lessC_out_gg(0, s(T30))
lessC_in_gg(s(T35), s(T36)) → U3_gg(T35, T36, lessC_in_gg(T35, T36))
U3_gg(T35, T36, lessC_out_gg(T35, T36)) → lessC_out_gg(s(T35), s(T36))
U4_ggg(T20, T21, T10, lessC_out_gg(T20, T21)) → U5_ggg(T20, T21, T10, orderedA_in_g(.(T21, T10)))
U5_ggg(T20, T21, T10, orderedA_out_g(.(T21, T10))) → pB_out_ggg(T20, T21, T10)
U2_g(T20, T21, T10, pB_out_ggg(T20, T21, T10)) → orderedA_out_g(.(s(T20), .(T21, T10)))
U1_g(T15, T10, orderedA_out_g(.(T15, T10))) → orderedA_out_g(.(0, .(T15, T10)))

Pi is empty.
We have to consider all (P,R,Pi)-chains

(15) UsableRulesProof (EQUIVALENT transformation)

For (infinitary) constructor rewriting [LOPSTR] we can delete all non-usable rules from R.

(16) Obligation:

Pi DP problem:
The TRS P consists of the following rules:

ORDEREDA_IN_G(.(s(T20), .(T21, T10))) → PB_IN_GGG(T20, T21, T10)
PB_IN_GGG(T20, T21, T10) → U4_GGG(T20, T21, T10, lessC_in_gg(T20, T21))
U4_GGG(T20, T21, T10, lessC_out_gg(T20, T21)) → ORDEREDA_IN_G(.(T21, T10))
ORDEREDA_IN_G(.(0, .(T15, T10))) → ORDEREDA_IN_G(.(T15, T10))

The TRS R consists of the following rules:

lessC_in_gg(0, s(T30)) → lessC_out_gg(0, s(T30))
lessC_in_gg(s(T35), s(T36)) → U3_gg(T35, T36, lessC_in_gg(T35, T36))
U3_gg(T35, T36, lessC_out_gg(T35, T36)) → lessC_out_gg(s(T35), s(T36))

Pi is empty.
We have to consider all (P,R,Pi)-chains

(17) PiDPToQDPProof (EQUIVALENT transformation)

Transforming (infinitary) constructor rewriting Pi-DP problem [LOPSTR] into ordinary QDP problem [LPAR04] by application of Pi.

(18) Obligation:

Q DP problem:
The TRS P consists of the following rules:

ORDEREDA_IN_G(.(s(T20), .(T21, T10))) → PB_IN_GGG(T20, T21, T10)
PB_IN_GGG(T20, T21, T10) → U4_GGG(T20, T21, T10, lessC_in_gg(T20, T21))
U4_GGG(T20, T21, T10, lessC_out_gg(T20, T21)) → ORDEREDA_IN_G(.(T21, T10))
ORDEREDA_IN_G(.(0, .(T15, T10))) → ORDEREDA_IN_G(.(T15, T10))

The TRS R consists of the following rules:

lessC_in_gg(0, s(T30)) → lessC_out_gg(0, s(T30))
lessC_in_gg(s(T35), s(T36)) → U3_gg(T35, T36, lessC_in_gg(T35, T36))
U3_gg(T35, T36, lessC_out_gg(T35, T36)) → lessC_out_gg(s(T35), s(T36))

The set Q consists of the following terms:

lessC_in_gg(x0, x1)
U3_gg(x0, x1, x2)

We have to consider all (P,Q,R)-chains.

(19) MRRProof (EQUIVALENT transformation)

By using the rule removal processor [LPAR04] with the following ordering, at least one Dependency Pair or term rewrite system rule of this QDP problem can be strictly oriented.
Strictly oriented dependency pairs:

ORDEREDA_IN_G(.(s(T20), .(T21, T10))) → PB_IN_GGG(T20, T21, T10)
PB_IN_GGG(T20, T21, T10) → U4_GGG(T20, T21, T10, lessC_in_gg(T20, T21))

Used ordering: Polynomial interpretation [POLO]:

POL(.(x₁, x₂)) = 2·x₁ + x₂   
POL(0) = 0   
POL(ORDEREDA_IN_G(x₁)) = x₁   
POL(PB_IN_GGG(x₁, x₂, x₃)) = 1 + 2·x₁ + 2·x₂ + x₃   
POL(U3_gg(x₁, x₂, x₃)) = 2 + x₁ + x₂ + x₃   
POL(U4_GGG(x₁, x₂, x₃, x₄)) = x₁ + x₂ + x₃ + x₄   
POL(lessC_in_gg(x₁, x₂)) = x₁ + x₂   
POL(lessC_out_gg(x₁, x₂)) = x₁ + x₂   
POL(s(x₁)) = 1 + 2·x₁   

(20) Obligation:

Q DP problem:
The TRS P consists of the following rules:

U4_GGG(T20, T21, T10, lessC_out_gg(T20, T21)) → ORDEREDA_IN_G(.(T21, T10))
ORDEREDA_IN_G(.(0, .(T15, T10))) → ORDEREDA_IN_G(.(T15, T10))

The TRS R consists of the following rules:

lessC_in_gg(0, s(T30)) → lessC_out_gg(0, s(T30))
lessC_in_gg(s(T35), s(T36)) → U3_gg(T35, T36, lessC_in_gg(T35, T36))
U3_gg(T35, T36, lessC_out_gg(T35, T36)) → lessC_out_gg(s(T35), s(T36))

The set Q consists of the following terms:

lessC_in_gg(x0, x1)
U3_gg(x0, x1, x2)

We have to consider all (P,Q,R)-chains.

(21) DependencyGraphProof (EQUIVALENT transformation)

The approximation of the Dependency Graph [LPAR04,FROCOS05,EDGSTAR] contains 1 SCC with 1 less node.

(22) Obligation:

Q DP problem:
The TRS P consists of the following rules:

ORDEREDA_IN_G(.(0, .(T15, T10))) → ORDEREDA_IN_G(.(T15, T10))

The TRS R consists of the following rules:

lessC_in_gg(0, s(T30)) → lessC_out_gg(0, s(T30))
lessC_in_gg(s(T35), s(T36)) → U3_gg(T35, T36, lessC_in_gg(T35, T36))
U3_gg(T35, T36, lessC_out_gg(T35, T36)) → lessC_out_gg(s(T35), s(T36))

The set Q consists of the following terms:

lessC_in_gg(x0, x1)
U3_gg(x0, x1, x2)

We have to consider all (P,Q,R)-chains.

(23) UsableRulesProof (EQUIVALENT transformation)

As all Q-normal forms are R-normal forms we are in the innermost case. Hence, by the usable rules processor [LPAR04] we can delete all non-usable rules [FROCOS05] from R.

(24) Obligation:

Q DP problem:
The TRS P consists of the following rules:

ORDEREDA_IN_G(.(0, .(T15, T10))) → ORDEREDA_IN_G(.(T15, T10))

R is empty.
The set Q consists of the following terms:

lessC_in_gg(x0, x1)
U3_gg(x0, x1, x2)

We have to consider all (P,Q,R)-chains.

(25) QReductionProof (EQUIVALENT transformation)

We deleted the following terms from Q as each root-symbol of these terms does neither occur in P nor in R.[THIEMANN].

lessC_in_gg(x0, x1)
U3_gg(x0, x1, x2)

(26) Obligation:

Q DP problem:
The TRS P consists of the following rules:

ORDEREDA_IN_G(.(0, .(T15, T10))) → ORDEREDA_IN_G(.(T15, T10))

R is empty.
Q is empty.
We have to consider all (P,Q,R)-chains.

(27) QDPSizeChangeProof (EQUIVALENT transformation)

By using the subterm criterion [SUBTERM_CRITERION] together with the size-change analysis [AAECC05] we have proven that there are no infinite chains for this DP problem.

From the DPs we obtained the following set of size-change graphs:

• ORDEREDA_IN_G(.(0, .(T15, T10))) → ORDEREDA_IN_G(.(T15, T10))
  The graph contains the following edges 1 > 1

(28) YES