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

(0) Obligation:

Clauses:

ordered([]).
ordered(.(X, [])).
ordered(.(X, .(Y, Xs))) :- ','(le(X, Y), ordered(.(Y, Xs))).
le(s(X), s(Y)) :- le(X, Y).
le(0, s(0)).
le(0, 0).

Query: ordered(g)

(1) PrologToPiTRSViaGraphTransformerProof (SOUND transformation)

Transformed Prolog program to (Pi-)TRS.

digraph dp_graph {
node [outthreshold=100, inthreshold=100];
1 [label="A: ordered(T1)\n\nT1 is ground", fontsize=16, style=filled, fillcolor=lightyellow, color=red];
4 [label="4: 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];
9 [label="9: 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];
18 [label="18: ordered([]), SCOPE: 1, CLAUSE: 2\n\n", fontsize=16, style=filled, fillcolor=lightyellow];
22 [label="22: \n\n", fontsize=16, style=filled, fillcolor=lightyellow];
27 [label="27: true | ordered(.(T3, [])), SCOPE: 1, CLAUSE: 2\n\nT3 is ground", fontsize=16, style=filled, fillcolor=lightyellow];
29 [label="29: ordered(T1), SCOPE: 1, CLAUSE: 2\n\nT1 is ground\nX6 is free\nordered(T1) !=? ordered([])\nordered(T1) !=? ordered(.(X6, []))", fontsize=16, style=filled, fillcolor=lightyellow];
30 [label="30: ordered(.(T3, [])), SCOPE: 1, CLAUSE: 2\n\nT3 is ground", fontsize=16, style=filled, fillcolor=lightyellow];
31 [label="31: \n\n", fontsize=16, style=filled, fillcolor=lightyellow];
32 [label="32: ','(le(T8, T9), ordered(.(T9, T10)))\n\nT8 is ground\nT9 is ground\nT10 is ground", fontsize=16, style=filled, fillcolor=lightyellow];
33 [label="33: \n\n", fontsize=16, style=filled, fillcolor=lightyellow];
36 [label="36: ','(le(T8, T9), ordered(.(T9, T10))), SCOPE: 2, CLAUSE: 3 | ','(le(T8, T9), ordered(.(T9, T10))), SCOPE: 2, CLAUSE: 4 | ','(le(T8, T9), ordered(.(T9, T10))), SCOPE: 2, CLAUSE: 5\n\nT8 is ground\nT9 is ground\nT10 is ground", fontsize=16, style=filled, fillcolor=lightyellow];
38 [label="38: ','(le(T8, T9), ordered(.(T9, T10))), SCOPE: 2, CLAUSE: 3\n\nT8 is ground\nT9 is ground\nT10 is ground", fontsize=16, style=filled, fillcolor=lightyellow];
39 [label="39: ','(le(T8, T9), ordered(.(T9, T10))), SCOPE: 2, CLAUSE: 4 | ','(le(T8, T9), ordered(.(T9, T10))), SCOPE: 2, CLAUSE: 5\n\nT8 is ground\nT9 is ground\nT10 is ground", fontsize=16, style=filled, fillcolor=lightyellow];
43 [label="B: ','(le(T19, T20), ordered(.(s(T20), T10)))\n\nT10 is ground\nT19 is ground\nT20 is ground", fontsize=16, style=filled, fillcolor=lightyellow];
45 [label="45: \n\n", fontsize=16, style=filled, fillcolor=lightyellow];
55 [label="C: le(T19, T20)\n\nT19 is ground\nT20 is ground", fontsize=16, style=filled, fillcolor=lightyellow];
56 [label="56: ordered(.(s(T20), T10))\n\nT10 is ground\nT20 is ground", fontsize=16, style=filled, fillcolor=lightyellow];
58 [label="58: le(T19, T20), SCOPE: 3, CLAUSE: 3 | le(T19, T20), SCOPE: 3, CLAUSE: 4 | le(T19, T20), SCOPE: 3, CLAUSE: 5\n\nT19 is ground\nT20 is ground", fontsize=16, style=filled, fillcolor=lightyellow];
59 [label="59: le(T19, T20), SCOPE: 3, CLAUSE: 3\n\nT19 is ground\nT20 is ground", fontsize=16, style=filled, fillcolor=lightyellow];
60 [label="60: le(T19, T20), SCOPE: 3, CLAUSE: 4 | le(T19, T20), SCOPE: 3, CLAUSE: 5\n\nT19 is ground\nT20 is ground", fontsize=16, style=filled, fillcolor=lightyellow];
64 [label="64: le(T33, T34)\n\nT33 is ground\nT34 is ground", fontsize=16, style=filled, fillcolor=lightyellow];
65 [label="65: \n\n", fontsize=16, style=filled, fillcolor=lightyellow];
69 [label="69: le(T19, T20), SCOPE: 3, CLAUSE: 4\n\nT19 is ground\nT20 is ground", fontsize=16, style=filled, fillcolor=lightyellow];
71 [label="71: le(T19, T20), SCOPE: 3, CLAUSE: 5\n\nT19 is ground\nT20 is ground", fontsize=16, style=filled, fillcolor=lightyellow];
72 [label="72: true\n\n", fontsize=16, style=filled, fillcolor=lightyellow];
73 [label="73: \n\n", fontsize=16, style=filled, fillcolor=lightyellow];
74 [label="74: \n\n", fontsize=16, style=filled, fillcolor=lightyellow];
75 [label="75: true\n\n", fontsize=16, style=filled, fillcolor=lightyellow];
77 [label="77: \n\n", fontsize=16, style=filled, fillcolor=lightyellow];
79 [label="79: \n\n", fontsize=16, style=filled, fillcolor=lightyellow];
84 [label="84: ','(le(T8, T9), ordered(.(T9, T10))), SCOPE: 2, CLAUSE: 4\n\nT8 is ground\nT9 is ground\nT10 is ground", fontsize=16, style=filled, fillcolor=lightyellow];
85 [label="85: ','(le(T8, T9), ordered(.(T9, T10))), SCOPE: 2, CLAUSE: 5\n\nT8 is ground\nT9 is ground\nT10 is ground", fontsize=16, style=filled, fillcolor=lightyellow];
90 [label="90: ordered(.(s(0), T10))\n\nT10 is ground", fontsize=16, style=filled, fillcolor=lightyellow];
91 [label="91: \n\n", fontsize=16, style=filled, fillcolor=lightyellow];
94 [label="94: ordered(.(0, T10))\n\nT10 is ground", fontsize=16, style=filled, fillcolor=lightyellow];
95 [label="95: \n\n", fontsize=16, style=filled, fillcolor=lightyellow];
96 [label="CASE", fontsize=14, style = filled, fillcolor = lightcyan];
1 -> 96 [arrowhead = none ];
96 -> 4;

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

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

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

100 [label="EVAL with clause\nordered(.(X6, [])).\nand substitutionX6 -> T3,\nT1 -> .(T3, [])", fontsize=14, style = filled, fillcolor = lightblue];
11 -> 100 [arrowhead = none ];
100 -> 27;

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

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

103 [label="BACKTRACK\nfor clause: ordered(.(X, .(Y, Xs))) :- ','(le(X, Y), ordered(.(Y, Xs)))because of non-unification", fontsize=14, style = filled, fillcolor = lightgreen];
18 -> 103 [arrowhead = none ];
103 -> 22;

104 [label="SUCCESS", fontsize=14, style = filled, fillcolor = lightgreen];
27 -> 104 [arrowhead = none ];
104 -> 30;

105 [label="EVAL with clause\nordered(.(X13, .(X14, X15))) :- ','(le(X13, X14), ordered(.(X14, X15))).\nand substitutionX13 -> T8,\nX14 -> T9,\nX15 -> T10,\nT1 -> .(T8, .(T9, T10))", fontsize=14, style = filled, fillcolor = lightblue];
29 -> 105 [arrowhead = none ];
105 -> 32;

106 [label="EVAL-BACKTRACK", fontsize=14, style = filled, fillcolor = lightgreen];
29 -> 106 [arrowhead = none ];
106 -> 33;

107 [label="BACKTRACK\nfor clause: ordered(.(X, .(Y, Xs))) :- ','(le(X, Y), ordered(.(Y, Xs)))because of non-unification", fontsize=14, style = filled, fillcolor = lightgreen];
30 -> 107 [arrowhead = none ];
107 -> 31;

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

109 [label="PARALLEL", fontsize=14, style = filled, fillcolor = violet];
36 -> 109 [arrowhead = none ];
109 -> 38;

110 [label="PARALLEL", fontsize=14, style = filled, fillcolor = violet];
36 -> 110 [arrowhead = none ];
110 -> 39;

111 [label="EVAL with clause\nle(s(X24), s(X25)) :- le(X24, X25).\nand substitutionX24 -> T19,\nT8 -> s(T19),\nX25 -> T20,\nT9 -> s(T20)", fontsize=14, style = filled, fillcolor = lightblue];
38 -> 111 [arrowhead = none ];
111 -> 43;

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

113 [label="PARALLEL", fontsize=14, style = filled, fillcolor = violet];
39 -> 113 [arrowhead = none ];
113 -> 84;

114 [label="PARALLEL", fontsize=14, style = filled, fillcolor = violet];
39 -> 114 [arrowhead = none ];
114 -> 85;

115 [label="SPLIT 1", fontsize=14, style = filled, fillcolor = violet];
43 -> 115 [arrowhead = none ];
115 -> 55;

116 [label="SPLIT 2\nnew knowledge:\nT19 is ground\nT20 is ground", fontsize=14, style = filled, fillcolor = violet];
43 -> 116 [arrowhead = none ];
116 -> 56;

117 [label="CASE", fontsize=14, style = filled, fillcolor = lightcyan];
55 -> 117 [arrowhead = none ];
117 -> 58;

118 [label="INSTANCE with matching:\nT1 -> .(s(T20), T10)", fontsize=14, style = filled, fillcolor = lightgrey];
56 -> 118 [arrowhead = none , style=dashed];
118 -> 1[style=dashed];

119 [label="PARALLEL", fontsize=14, style = filled, fillcolor = violet];
58 -> 119 [arrowhead = none ];
119 -> 59;

120 [label="PARALLEL", fontsize=14, style = filled, fillcolor = violet];
58 -> 120 [arrowhead = none ];
120 -> 60;

121 [label="EVAL with clause\nle(s(X38), s(X39)) :- le(X38, X39).\nand substitutionX38 -> T33,\nT19 -> s(T33),\nX39 -> T34,\nT20 -> s(T34)", fontsize=14, style = filled, fillcolor = lightblue];
59 -> 121 [arrowhead = none ];
121 -> 64;

122 [label="EVAL-BACKTRACK", fontsize=14, style = filled, fillcolor = lightgreen];
59 -> 122 [arrowhead = none ];
122 -> 65;

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

124 [label="PARALLEL", fontsize=14, style = filled, fillcolor = violet];
60 -> 124 [arrowhead = none ];
124 -> 71;

125 [label="INSTANCE with matching:\nT19 -> T33\nT20 -> T34", fontsize=14, style = filled, fillcolor = lightgrey];
64 -> 125 [arrowhead = none , style=dashed];
125 -> 55[style=dashed];

126 [label="EVAL with clause\nle(0, s(0)).\nand substitutionT19 -> 0,\nT20 -> s(0)", fontsize=14, style = filled, fillcolor = lightblue];
69 -> 126 [arrowhead = none ];
126 -> 72;

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

128 [label="EVAL with clause\nle(0, 0).\nand substitutionT19 -> 0,\nT20 -> 0", fontsize=14, style = filled, fillcolor = lightblue];
71 -> 128 [arrowhead = none ];
128 -> 75;

129 [label="EVAL-BACKTRACK", fontsize=14, style = filled, fillcolor = lightgreen];
71 -> 129 [arrowhead = none ];
129 -> 77;

130 [label="SUCCESS", fontsize=14, style = filled, fillcolor = lightgreen];
72 -> 130 [arrowhead = none ];
130 -> 74;

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

132 [label="EVAL with clause\nle(0, s(0)).\nand substitutionT8 -> 0,\nT9 -> s(0)", fontsize=14, style = filled, fillcolor = lightblue];
84 -> 132 [arrowhead = none ];
132 -> 90;

133 [label="EVAL-BACKTRACK", fontsize=14, style = filled, fillcolor = lightgreen];
84 -> 133 [arrowhead = none ];
133 -> 91;

134 [label="EVAL with clause\nle(0, 0).\nand substitutionT8 -> 0,\nT9 -> 0", fontsize=14, style = filled, fillcolor = lightblue];
85 -> 134 [arrowhead = none ];
134 -> 94;

135 [label="EVAL-BACKTRACK", fontsize=14, style = filled, fillcolor = lightgreen];
85 -> 135 [arrowhead = none ];
135 -> 95;

136 [label="INSTANCE with matching:\nT1 -> .(s(0), T10)", fontsize=14, style = filled, fillcolor = lightgrey];
90 -> 136 [arrowhead = none , style=dashed];
136 -> 1[style=dashed];

137 [label="INSTANCE with matching:\nT1 -> .(0, T10)", fontsize=14, style = filled, fillcolor = lightgrey];
94 -> 137 [arrowhead = none , style=dashed];
137 -> 1[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(.(s(T19), .(s(T20), T10))) → U1_g(T19, T20, T10, pB_in_ggg(T19, T20, T10))
pB_in_ggg(T19, T20, T10) → U5_ggg(T19, T20, T10, leC_in_gg(T19, T20))
leC_in_gg(s(T33), s(T34)) → U4_gg(T33, T34, leC_in_gg(T33, T34))
leC_in_gg(0, s(0)) → leC_out_gg(0, s(0))
leC_in_gg(0, 0) → leC_out_gg(0, 0)
U4_gg(T33, T34, leC_out_gg(T33, T34)) → leC_out_gg(s(T33), s(T34))
U5_ggg(T19, T20, T10, leC_out_gg(T19, T20)) → U6_ggg(T19, T20, T10, orderedA_in_g(.(s(T20), T10)))
orderedA_in_g(.(0, .(s(0), T10))) → U2_g(T10, orderedA_in_g(.(s(0), T10)))
orderedA_in_g(.(0, .(0, T10))) → U3_g(T10, orderedA_in_g(.(0, T10)))
U3_g(T10, orderedA_out_g(.(0, T10))) → orderedA_out_g(.(0, .(0, T10)))
U2_g(T10, orderedA_out_g(.(s(0), T10))) → orderedA_out_g(.(0, .(s(0), T10)))
U6_ggg(T19, T20, T10, orderedA_out_g(.(s(T20), T10))) → pB_out_ggg(T19, T20, T10)
U1_g(T19, T20, T10, pB_out_ggg(T19, T20, T10)) → orderedA_out_g(.(s(T19), .(s(T20), 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(.(s(T19), .(s(T20), T10))) → U1_G(T19, T20, T10, pB_in_ggg(T19, T20, T10))
ORDEREDA_IN_G(.(s(T19), .(s(T20), T10))) → PB_IN_GGG(T19, T20, T10)
PB_IN_GGG(T19, T20, T10) → U5_GGG(T19, T20, T10, leC_in_gg(T19, T20))
PB_IN_GGG(T19, T20, T10) → LEC_IN_GG(T19, T20)
LEC_IN_GG(s(T33), s(T34)) → U4_GG(T33, T34, leC_in_gg(T33, T34))
LEC_IN_GG(s(T33), s(T34)) → LEC_IN_GG(T33, T34)
U5_GGG(T19, T20, T10, leC_out_gg(T19, T20)) → U6_GGG(T19, T20, T10, orderedA_in_g(.(s(T20), T10)))
U5_GGG(T19, T20, T10, leC_out_gg(T19, T20)) → ORDEREDA_IN_G(.(s(T20), T10))
ORDEREDA_IN_G(.(0, .(s(0), T10))) → U2_G(T10, orderedA_in_g(.(s(0), T10)))
ORDEREDA_IN_G(.(0, .(s(0), T10))) → ORDEREDA_IN_G(.(s(0), T10))
ORDEREDA_IN_G(.(0, .(0, T10))) → U3_G(T10, orderedA_in_g(.(0, T10)))
ORDEREDA_IN_G(.(0, .(0, T10))) → ORDEREDA_IN_G(.(0, 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(.(s(T19), .(s(T20), T10))) → U1_g(T19, T20, T10, pB_in_ggg(T19, T20, T10))
pB_in_ggg(T19, T20, T10) → U5_ggg(T19, T20, T10, leC_in_gg(T19, T20))
leC_in_gg(s(T33), s(T34)) → U4_gg(T33, T34, leC_in_gg(T33, T34))
leC_in_gg(0, s(0)) → leC_out_gg(0, s(0))
leC_in_gg(0, 0) → leC_out_gg(0, 0)
U4_gg(T33, T34, leC_out_gg(T33, T34)) → leC_out_gg(s(T33), s(T34))
U5_ggg(T19, T20, T10, leC_out_gg(T19, T20)) → U6_ggg(T19, T20, T10, orderedA_in_g(.(s(T20), T10)))
orderedA_in_g(.(0, .(s(0), T10))) → U2_g(T10, orderedA_in_g(.(s(0), T10)))
orderedA_in_g(.(0, .(0, T10))) → U3_g(T10, orderedA_in_g(.(0, T10)))
U3_g(T10, orderedA_out_g(.(0, T10))) → orderedA_out_g(.(0, .(0, T10)))
U2_g(T10, orderedA_out_g(.(s(0), T10))) → orderedA_out_g(.(0, .(s(0), T10)))
U6_ggg(T19, T20, T10, orderedA_out_g(.(s(T20), T10))) → pB_out_ggg(T19, T20, T10)
U1_g(T19, T20, T10, pB_out_ggg(T19, T20, T10)) → orderedA_out_g(.(s(T19), .(s(T20), 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(.(s(T19), .(s(T20), T10))) → U1_G(T19, T20, T10, pB_in_ggg(T19, T20, T10))
ORDEREDA_IN_G(.(s(T19), .(s(T20), T10))) → PB_IN_GGG(T19, T20, T10)
PB_IN_GGG(T19, T20, T10) → U5_GGG(T19, T20, T10, leC_in_gg(T19, T20))
PB_IN_GGG(T19, T20, T10) → LEC_IN_GG(T19, T20)
LEC_IN_GG(s(T33), s(T34)) → U4_GG(T33, T34, leC_in_gg(T33, T34))
LEC_IN_GG(s(T33), s(T34)) → LEC_IN_GG(T33, T34)
U5_GGG(T19, T20, T10, leC_out_gg(T19, T20)) → U6_GGG(T19, T20, T10, orderedA_in_g(.(s(T20), T10)))
U5_GGG(T19, T20, T10, leC_out_gg(T19, T20)) → ORDEREDA_IN_G(.(s(T20), T10))
ORDEREDA_IN_G(.(0, .(s(0), T10))) → U2_G(T10, orderedA_in_g(.(s(0), T10)))
ORDEREDA_IN_G(.(0, .(s(0), T10))) → ORDEREDA_IN_G(.(s(0), T10))
ORDEREDA_IN_G(.(0, .(0, T10))) → U3_G(T10, orderedA_in_g(.(0, T10)))
ORDEREDA_IN_G(.(0, .(0, T10))) → ORDEREDA_IN_G(.(0, 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(.(s(T19), .(s(T20), T10))) → U1_g(T19, T20, T10, pB_in_ggg(T19, T20, T10))
pB_in_ggg(T19, T20, T10) → U5_ggg(T19, T20, T10, leC_in_gg(T19, T20))
leC_in_gg(s(T33), s(T34)) → U4_gg(T33, T34, leC_in_gg(T33, T34))
leC_in_gg(0, s(0)) → leC_out_gg(0, s(0))
leC_in_gg(0, 0) → leC_out_gg(0, 0)
U4_gg(T33, T34, leC_out_gg(T33, T34)) → leC_out_gg(s(T33), s(T34))
U5_ggg(T19, T20, T10, leC_out_gg(T19, T20)) → U6_ggg(T19, T20, T10, orderedA_in_g(.(s(T20), T10)))
orderedA_in_g(.(0, .(s(0), T10))) → U2_g(T10, orderedA_in_g(.(s(0), T10)))
orderedA_in_g(.(0, .(0, T10))) → U3_g(T10, orderedA_in_g(.(0, T10)))
U3_g(T10, orderedA_out_g(.(0, T10))) → orderedA_out_g(.(0, .(0, T10)))
U2_g(T10, orderedA_out_g(.(s(0), T10))) → orderedA_out_g(.(0, .(s(0), T10)))
U6_ggg(T19, T20, T10, orderedA_out_g(.(s(T20), T10))) → pB_out_ggg(T19, T20, T10)
U1_g(T19, T20, T10, pB_out_ggg(T19, T20, T10)) → orderedA_out_g(.(s(T19), .(s(T20), 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 3 SCCs with 7 less nodes.

(6) Complex Obligation (AND)

(7) Obligation:

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

LEC_IN_GG(s(T33), s(T34)) → LEC_IN_GG(T33, T34)

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(.(s(T19), .(s(T20), T10))) → U1_g(T19, T20, T10, pB_in_ggg(T19, T20, T10))
pB_in_ggg(T19, T20, T10) → U5_ggg(T19, T20, T10, leC_in_gg(T19, T20))
leC_in_gg(s(T33), s(T34)) → U4_gg(T33, T34, leC_in_gg(T33, T34))
leC_in_gg(0, s(0)) → leC_out_gg(0, s(0))
leC_in_gg(0, 0) → leC_out_gg(0, 0)
U4_gg(T33, T34, leC_out_gg(T33, T34)) → leC_out_gg(s(T33), s(T34))
U5_ggg(T19, T20, T10, leC_out_gg(T19, T20)) → U6_ggg(T19, T20, T10, orderedA_in_g(.(s(T20), T10)))
orderedA_in_g(.(0, .(s(0), T10))) → U2_g(T10, orderedA_in_g(.(s(0), T10)))
orderedA_in_g(.(0, .(0, T10))) → U3_g(T10, orderedA_in_g(.(0, T10)))
U3_g(T10, orderedA_out_g(.(0, T10))) → orderedA_out_g(.(0, .(0, T10)))
U2_g(T10, orderedA_out_g(.(s(0), T10))) → orderedA_out_g(.(0, .(s(0), T10)))
U6_ggg(T19, T20, T10, orderedA_out_g(.(s(T20), T10))) → pB_out_ggg(T19, T20, T10)
U1_g(T19, T20, T10, pB_out_ggg(T19, T20, T10)) → orderedA_out_g(.(s(T19), .(s(T20), 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:

LEC_IN_GG(s(T33), s(T34)) → LEC_IN_GG(T33, T34)

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:

LEC_IN_GG(s(T33), s(T34)) → LEC_IN_GG(T33, T34)

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:

• LEC_IN_GG(s(T33), s(T34)) → LEC_IN_GG(T33, T34)
  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(T19), .(s(T20), T10))) → PB_IN_GGG(T19, T20, T10)
PB_IN_GGG(T19, T20, T10) → U5_GGG(T19, T20, T10, leC_in_gg(T19, T20))
U5_GGG(T19, T20, T10, leC_out_gg(T19, T20)) → ORDEREDA_IN_G(.(s(T20), 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(.(s(T19), .(s(T20), T10))) → U1_g(T19, T20, T10, pB_in_ggg(T19, T20, T10))
pB_in_ggg(T19, T20, T10) → U5_ggg(T19, T20, T10, leC_in_gg(T19, T20))
leC_in_gg(s(T33), s(T34)) → U4_gg(T33, T34, leC_in_gg(T33, T34))
leC_in_gg(0, s(0)) → leC_out_gg(0, s(0))
leC_in_gg(0, 0) → leC_out_gg(0, 0)
U4_gg(T33, T34, leC_out_gg(T33, T34)) → leC_out_gg(s(T33), s(T34))
U5_ggg(T19, T20, T10, leC_out_gg(T19, T20)) → U6_ggg(T19, T20, T10, orderedA_in_g(.(s(T20), T10)))
orderedA_in_g(.(0, .(s(0), T10))) → U2_g(T10, orderedA_in_g(.(s(0), T10)))
orderedA_in_g(.(0, .(0, T10))) → U3_g(T10, orderedA_in_g(.(0, T10)))
U3_g(T10, orderedA_out_g(.(0, T10))) → orderedA_out_g(.(0, .(0, T10)))
U2_g(T10, orderedA_out_g(.(s(0), T10))) → orderedA_out_g(.(0, .(s(0), T10)))
U6_ggg(T19, T20, T10, orderedA_out_g(.(s(T20), T10))) → pB_out_ggg(T19, T20, T10)
U1_g(T19, T20, T10, pB_out_ggg(T19, T20, T10)) → orderedA_out_g(.(s(T19), .(s(T20), 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(T19), .(s(T20), T10))) → PB_IN_GGG(T19, T20, T10)
PB_IN_GGG(T19, T20, T10) → U5_GGG(T19, T20, T10, leC_in_gg(T19, T20))
U5_GGG(T19, T20, T10, leC_out_gg(T19, T20)) → ORDEREDA_IN_G(.(s(T20), T10))

The TRS R consists of the following rules:

leC_in_gg(s(T33), s(T34)) → U4_gg(T33, T34, leC_in_gg(T33, T34))
leC_in_gg(0, s(0)) → leC_out_gg(0, s(0))
leC_in_gg(0, 0) → leC_out_gg(0, 0)
U4_gg(T33, T34, leC_out_gg(T33, T34)) → leC_out_gg(s(T33), s(T34))

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(T19), .(s(T20), T10))) → PB_IN_GGG(T19, T20, T10)
PB_IN_GGG(T19, T20, T10) → U5_GGG(T19, T20, T10, leC_in_gg(T19, T20))
U5_GGG(T19, T20, T10, leC_out_gg(T19, T20)) → ORDEREDA_IN_G(.(s(T20), T10))

The TRS R consists of the following rules:

leC_in_gg(s(T33), s(T34)) → U4_gg(T33, T34, leC_in_gg(T33, T34))
leC_in_gg(0, s(0)) → leC_out_gg(0, s(0))
leC_in_gg(0, 0) → leC_out_gg(0, 0)
U4_gg(T33, T34, leC_out_gg(T33, T34)) → leC_out_gg(s(T33), s(T34))

The set Q consists of the following terms:

leC_in_gg(x0, x1)
U4_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(T19), .(s(T20), T10))) → PB_IN_GGG(T19, T20, T10)

Strictly oriented rules of the TRS R:

leC_in_gg(0, s(0)) → leC_out_gg(0, s(0))
leC_in_gg(0, 0) → leC_out_gg(0, 0)

Used ordering: Polynomial interpretation [POLO]:

POL(.(x₁, x₂)) = x₁ + 2·x₂   
POL(0) = 0   
POL(ORDEREDA_IN_G(x₁)) = x₁   
POL(PB_IN_GGG(x₁, x₂, x₃)) = 2 + 2·x₁ + 2·x₂ + 2·x₃   
POL(U4_gg(x₁, x₂, x₃)) = 2 + x₁ + x₂ + x₃   
POL(U5_GGG(x₁, x₂, x₃, x₄)) = 1 + x₁ + x₂ + 2·x₃ + x₄   
POL(leC_in_gg(x₁, x₂)) = 1 + x₁ + x₂   
POL(leC_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:

PB_IN_GGG(T19, T20, T10) → U5_GGG(T19, T20, T10, leC_in_gg(T19, T20))
U5_GGG(T19, T20, T10, leC_out_gg(T19, T20)) → ORDEREDA_IN_G(.(s(T20), T10))

The TRS R consists of the following rules:

leC_in_gg(s(T33), s(T34)) → U4_gg(T33, T34, leC_in_gg(T33, T34))
U4_gg(T33, T34, leC_out_gg(T33, T34)) → leC_out_gg(s(T33), s(T34))

The set Q consists of the following terms:

leC_in_gg(x0, x1)
U4_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 0 SCCs with 2 less nodes.

(22) TRUE

(23) Obligation:

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

ORDEREDA_IN_G(.(0, .(0, T10))) → ORDEREDA_IN_G(.(0, 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(.(s(T19), .(s(T20), T10))) → U1_g(T19, T20, T10, pB_in_ggg(T19, T20, T10))
pB_in_ggg(T19, T20, T10) → U5_ggg(T19, T20, T10, leC_in_gg(T19, T20))
leC_in_gg(s(T33), s(T34)) → U4_gg(T33, T34, leC_in_gg(T33, T34))
leC_in_gg(0, s(0)) → leC_out_gg(0, s(0))
leC_in_gg(0, 0) → leC_out_gg(0, 0)
U4_gg(T33, T34, leC_out_gg(T33, T34)) → leC_out_gg(s(T33), s(T34))
U5_ggg(T19, T20, T10, leC_out_gg(T19, T20)) → U6_ggg(T19, T20, T10, orderedA_in_g(.(s(T20), T10)))
orderedA_in_g(.(0, .(s(0), T10))) → U2_g(T10, orderedA_in_g(.(s(0), T10)))
orderedA_in_g(.(0, .(0, T10))) → U3_g(T10, orderedA_in_g(.(0, T10)))
U3_g(T10, orderedA_out_g(.(0, T10))) → orderedA_out_g(.(0, .(0, T10)))
U2_g(T10, orderedA_out_g(.(s(0), T10))) → orderedA_out_g(.(0, .(s(0), T10)))
U6_ggg(T19, T20, T10, orderedA_out_g(.(s(T20), T10))) → pB_out_ggg(T19, T20, T10)
U1_g(T19, T20, T10, pB_out_ggg(T19, T20, T10)) → orderedA_out_g(.(s(T19), .(s(T20), T10)))

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

(24) UsableRulesProof (EQUIVALENT transformation)

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

(25) Obligation:

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

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

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

(26) PiDPToQDPProof (EQUIVALENT transformation)

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

(27) Obligation:

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

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

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

(28) 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, .(0, T10))) → ORDEREDA_IN_G(.(0, T10))
  The graph contains the following edges 1 > 1

(29) YES