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

(0) Obligation:

Clauses:

hidden_flatten([], L, L).
hidden_flatten(.(.(H, T), L), S, F) :- ','(!, ','(hidden_flatten(L, S, Lf), hidden_flatten(.(H, T), Lf, F))).
hidden_flatten(.(H, T), S, .(H, L)) :- hidden_flatten(T, S, L).

Query: hidden_flatten(g,a,a)

(1) PrologToTRSTransformerProof (SOUND transformation)

Transformed Prolog program to TRS.

digraph dp_graph {
node [outthreshold=100, inthreshold=100];
1 [label="1: hidden_flatten(T1, T2, T3)\n\nT1 is ground", fontsize=16, style=filled, fillcolor=lightyellow, color=red];
5 [label="5: hidden_flatten(T1, T2, T3), SCOPE: 1, CLAUSE: 0 | hidden_flatten(T1, T2, T3), SCOPE: 1, CLAUSE: 1 | hidden_flatten(T1, T2, T3), SCOPE: 1, CLAUSE: 2\n\nT1 is ground", fontsize=16, style=filled, fillcolor=lightyellow];
7 [label="7: true | hidden_flatten([], T2, T3), SCOPE: 1, CLAUSE: 1 | hidden_flatten([], T2, T3), SCOPE: 1, CLAUSE: 2\n\n", fontsize=16, style=filled, fillcolor=lightyellow];
10 [label="10: hidden_flatten(T1, T2, T3), SCOPE: 1, CLAUSE: 1 | hidden_flatten(T1, T2, T3), SCOPE: 1, CLAUSE: 2\n\nT1 is ground\nX3 is free\nhidden_flatten(T1, T2, T3) !=? hidden_flatten([], X3, X3)", fontsize=16, style=filled, fillcolor=lightyellow];
17 [label="17: hidden_flatten([], T2, T3), SCOPE: 1, CLAUSE: 1 | hidden_flatten([], T2, T3), SCOPE: 1, CLAUSE: 2\n\n", fontsize=16, style=filled, fillcolor=lightyellow];
18 [label="18: hidden_flatten([], T2, T3), SCOPE: 1, CLAUSE: 2\n\n", fontsize=16, style=filled, fillcolor=lightyellow];
20 [label="20: \n\n", fontsize=16, style=filled, fillcolor=lightyellow];
22 [label="22: hidden_flatten(T1, T2, T3), SCOPE: 1, CLAUSE: 1\n\nT1 is ground\nX3 is free\nhidden_flatten(T1, T2, T3) !=? hidden_flatten([], X3, X3)", fontsize=16, style=filled, fillcolor=lightyellow];
23 [label="23: hidden_flatten(T1, T2, T3), SCOPE: 1, CLAUSE: 2\n\nT1 is ground\nX3 is free\nhidden_flatten(T1, T2, T3) !=? hidden_flatten([], X3, X3)", fontsize=16, style=filled, fillcolor=lightyellow];
35 [label="35: ','(!_1, ','(hidden_flatten(T29, T32, X40), hidden_flatten(.(T27, T28), X40, T33)))\n\nT27 is ground\nT28 is ground\nT29 is ground\nX40 is free", fontsize=16, style=filled, fillcolor=lightyellow];
36 [label="36: \n\n", fontsize=16, style=filled, fillcolor=lightyellow];
37 [label="37: ','(hidden_flatten(T29, T32, X40), hidden_flatten(.(T27, T28), X40, T33))\n\nT27 is ground\nT28 is ground\nT29 is ground\nX40 is free", fontsize=16, style=filled, fillcolor=lightyellow];
45 [label="45: hidden_flatten(T29, T32, X40)\n\nT29 is ground\nX40 is free", fontsize=16, style=filled, fillcolor=lightyellow];
46 [label="46: hidden_flatten(.(T27, T28), T36, T37)\n\nT27 is ground\nT28 is ground", fontsize=16, style=filled, fillcolor=lightyellow];
49 [label="49: hidden_flatten(T29, T32, X40), SCOPE: 2, CLAUSE: 0 | hidden_flatten(T29, T32, X40), SCOPE: 2, CLAUSE: 1 | hidden_flatten(T29, T32, X40), SCOPE: 2, CLAUSE: 2\n\nT29 is ground\nX40 is free", fontsize=16, style=filled, fillcolor=lightyellow];
52 [label="52: true | hidden_flatten([], T32, X40), SCOPE: 2, CLAUSE: 1 | hidden_flatten([], T32, X40), SCOPE: 2, CLAUSE: 2\n\nX40 is free", fontsize=16, style=filled, fillcolor=lightyellow];
53 [label="53: hidden_flatten(T29, T32, X40), SCOPE: 2, CLAUSE: 1 | hidden_flatten(T29, T32, X40), SCOPE: 2, CLAUSE: 2\n\nT29 is ground\nX40 is free\nX47 is free\nhidden_flatten(T29, T32, X40) !=? hidden_flatten([], X47, X47)", fontsize=16, style=filled, fillcolor=lightyellow];
54 [label="54: hidden_flatten([], T32, X40), SCOPE: 2, CLAUSE: 1 | hidden_flatten([], T32, X40), SCOPE: 2, CLAUSE: 2\n\nX40 is free", fontsize=16, style=filled, fillcolor=lightyellow];
62 [label="62: hidden_flatten([], T32, X40), SCOPE: 2, CLAUSE: 2\n\nX40 is free", fontsize=16, style=filled, fillcolor=lightyellow];
64 [label="64: \n\n", fontsize=16, style=filled, fillcolor=lightyellow];
72 [label="72: hidden_flatten(T29, T32, X40), SCOPE: 2, CLAUSE: 1\n\nT29 is ground\nX40 is free\nX47 is free\nhidden_flatten(T29, T32, X40) !=? hidden_flatten([], X47, X47)", fontsize=16, style=filled, fillcolor=lightyellow];
73 [label="73: hidden_flatten(T29, T32, X40), SCOPE: 2, CLAUSE: 2\n\nT29 is ground\nX40 is free\nX47 is free\nhidden_flatten(T29, T32, X40) !=? hidden_flatten([], X47, X47)", fontsize=16, style=filled, fillcolor=lightyellow];
85 [label="85: ','(!_2, ','(hidden_flatten(T61, T63, X88), hidden_flatten(.(T59, T60), X88, X89)))\n\nT59 is ground\nT60 is ground\nT61 is ground\nX89 is free\nX88 is free", fontsize=16, style=filled, fillcolor=lightyellow];
86 [label="86: \n\n", fontsize=16, style=filled, fillcolor=lightyellow];
87 [label="87: ','(hidden_flatten(T61, T63, X88), hidden_flatten(.(T59, T60), X88, X89))\n\nT59 is ground\nT60 is ground\nT61 is ground\nX89 is free\nX88 is free", fontsize=16, style=filled, fillcolor=lightyellow];
97 [label="97: hidden_flatten(T61, T63, X88)\n\nT61 is ground\nX88 is free", fontsize=16, style=filled, fillcolor=lightyellow];
98 [label="98: hidden_flatten(.(T59, T60), T66, X89)\n\nT59 is ground\nT60 is ground\nX89 is free", fontsize=16, style=filled, fillcolor=lightyellow];
103 [label="103: hidden_flatten(T76, T78, X110)\n\nT76 is ground\nX110 is free", fontsize=16, style=filled, fillcolor=lightyellow];
112 [label="112: \n\n", fontsize=16, style=filled, fillcolor=lightyellow];
123 [label="123: hidden_flatten(T90, T93, T94)\n\nT90 is ground", fontsize=16, style=filled, fillcolor=lightyellow];
124 [label="124: \n\n", fontsize=16, style=filled, fillcolor=lightyellow];
125 [label="CASE", fontsize=14, style = filled, fillcolor = lightcyan];
1 -> 125 [arrowhead = none ];
125 -> 5;

126 [label="EVAL with clause\nhidden_flatten([], X3, X3).\nand substitutionT1 -> [],\nT2 -> T6,\nX3 -> T6,\nT3 -> T6", fontsize=14, style = filled, fillcolor = lightblue];
5 -> 126 [arrowhead = none ];
126 -> 7;

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

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

129 [label="PARALLEL", fontsize=14, style = filled, fillcolor = violet];
10 -> 129 [arrowhead = none ];
129 -> 22;

130 [label="PARALLEL", fontsize=14, style = filled, fillcolor = violet];
10 -> 130 [arrowhead = none ];
130 -> 23;

131 [label="BACKTRACK\nfor clause: hidden_flatten(.(.(H, T), L), S, F) :- ','(!, ','(hidden_flatten(L, S, Lf), hidden_flatten(.(H, T), Lf, F)))because of non-unification", fontsize=14, style = filled, fillcolor = lightgreen];
17 -> 131 [arrowhead = none ];
131 -> 18;

132 [label="BACKTRACK\nfor clause: hidden_flatten(.(H, T), S, .(H, L)) :- hidden_flatten(T, S, L)because of non-unification", fontsize=14, style = filled, fillcolor = lightgreen];
18 -> 132 [arrowhead = none ];
132 -> 20;

133 [label="EVAL with clause\nhidden_flatten(.(.(X35, X36), X37), X38, X39) :- ','(!_1, ','(hidden_flatten(X37, X38, X40), hidden_flatten(.(X35, X36), X40, X39))).\nand substitutionX35 -> T27,\nX36 -> T28,\nX37 -> T29,\nT1 -> .(.(T27, T28), T29),\nT2 -> T32,\nX38 -> T32,\nT3 -> T33,\nX39 -> T33,\nT30 -> T32,\nT31 -> T33", fontsize=14, style = filled, fillcolor = lightblue];
22 -> 133 [arrowhead = none ];
133 -> 35;

134 [label="EVAL-BACKTRACK", fontsize=14, style = filled, fillcolor = lightgreen];
22 -> 134 [arrowhead = none ];
134 -> 36;

135 [label="EVAL with clause\nhidden_flatten(.(X123, X124), X125, .(X123, X126)) :- hidden_flatten(X124, X125, X126).\nand substitutionX123 -> T89,\nX124 -> T90,\nT1 -> .(T89, T90),\nT2 -> T93,\nX125 -> T93,\nX126 -> T94,\nT3 -> .(T89, T94),\nT91 -> T93,\nT92 -> T94", fontsize=14, style = filled, fillcolor = lightblue];
23 -> 135 [arrowhead = none ];
135 -> 123;

136 [label="EVAL-BACKTRACK", fontsize=14, style = filled, fillcolor = lightgreen];
23 -> 136 [arrowhead = none ];
136 -> 124;

137 [label="CUT", fontsize=14, style = filled, fillcolor = lightgreen];
35 -> 137 [arrowhead = none ];
137 -> 37;

138 [label="SPLIT 1", fontsize=14, style = filled, fillcolor = violet];
37 -> 138 [arrowhead = none ];
138 -> 45;

139 [label="SPLIT 2\nnew knowledge:\nT29 is ground\nreplacements:X40 -> T36,\nT33 -> T37", fontsize=14, style = filled, fillcolor = violet];
37 -> 139 [arrowhead = none ];
139 -> 46;

140 [label="CASE", fontsize=14, style = filled, fillcolor = lightcyan];
45 -> 140 [arrowhead = none ];
140 -> 49;

141 [label="INSTANCE with matching:\nT1 -> .(T27, T28)\nT2 -> T36\nT3 -> T37", fontsize=14, style = filled, fillcolor = lightgrey];
46 -> 141 [arrowhead = none , style=dashed];
141 -> 1[style=dashed];

142 [label="EVAL with clause\nhidden_flatten([], X47, X47).\nand substitutionT29 -> [],\nT32 -> T42,\nX47 -> T42,\nX40 -> T42", fontsize=14, style = filled, fillcolor = lightblue];
49 -> 142 [arrowhead = none ];
142 -> 52;

143 [label="EVAL-BACKTRACK", fontsize=14, style = filled, fillcolor = lightgreen];
49 -> 143 [arrowhead = none ];
143 -> 53;

144 [label="SUCCESS", fontsize=14, style = filled, fillcolor = lightgreen];
52 -> 144 [arrowhead = none ];
144 -> 54;

145 [label="PARALLEL", fontsize=14, style = filled, fillcolor = violet];
53 -> 145 [arrowhead = none ];
145 -> 72;

146 [label="PARALLEL", fontsize=14, style = filled, fillcolor = violet];
53 -> 146 [arrowhead = none ];
146 -> 73;

147 [label="BACKTRACK\nfor clause: hidden_flatten(.(.(H, T), L), S, F) :- ','(!, ','(hidden_flatten(L, S, Lf), hidden_flatten(.(H, T), Lf, F)))because of non-unification", fontsize=14, style = filled, fillcolor = lightgreen];
54 -> 147 [arrowhead = none ];
147 -> 62;

148 [label="BACKTRACK\nfor clause: hidden_flatten(.(H, T), S, .(H, L)) :- hidden_flatten(T, S, L)because of non-unification", fontsize=14, style = filled, fillcolor = lightgreen];
62 -> 148 [arrowhead = none ];
148 -> 64;

149 [label="EVAL with clause\nhidden_flatten(.(.(X83, X84), X85), X86, X87) :- ','(!_2, ','(hidden_flatten(X85, X86, X88), hidden_flatten(.(X83, X84), X88, X87))).\nand substitutionX83 -> T59,\nX84 -> T60,\nX85 -> T61,\nT29 -> .(.(T59, T60), T61),\nT32 -> T63,\nX86 -> T63,\nX40 -> X89,\nX87 -> X89,\nT62 -> T63", fontsize=14, style = filled, fillcolor = lightblue];
72 -> 149 [arrowhead = none ];
149 -> 85;

150 [label="EVAL-BACKTRACK", fontsize=14, style = filled, fillcolor = lightgreen];
72 -> 150 [arrowhead = none ];
150 -> 86;

151 [label="EVAL with clause\nhidden_flatten(.(X106, X107), X108, .(X106, X109)) :- hidden_flatten(X107, X108, X109).\nand substitutionX106 -> T75,\nX107 -> T76,\nT29 -> .(T75, T76),\nT32 -> T78,\nX108 -> T78,\nX109 -> X110,\nX40 -> .(T75, X110),\nT77 -> T78", fontsize=14, style = filled, fillcolor = lightblue];
73 -> 151 [arrowhead = none ];
151 -> 103;

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

153 [label="CUT", fontsize=14, style = filled, fillcolor = lightgreen];
85 -> 153 [arrowhead = none ];
153 -> 87;

154 [label="SPLIT 1", fontsize=14, style = filled, fillcolor = violet];
87 -> 154 [arrowhead = none ];
154 -> 97;

155 [label="SPLIT 2\nnew knowledge:\nT61 is ground\nreplacements:X88 -> T66", fontsize=14, style = filled, fillcolor = violet];
87 -> 155 [arrowhead = none ];
155 -> 98;

156 [label="INSTANCE with matching:\nT29 -> T61\nT32 -> T63\nX40 -> X88", fontsize=14, style = filled, fillcolor = lightgrey];
97 -> 156 [arrowhead = none , style=dashed];
156 -> 45[style=dashed];

157 [label="INSTANCE with matching:\nT1 -> .(T59, T60)\nT2 -> T66\nT3 -> X89", fontsize=14, style = filled, fillcolor = lightgrey];
98 -> 157 [arrowhead = none , style=dashed];
157 -> 1[style=dashed];

158 [label="INSTANCE with matching:\nT29 -> T76\nT32 -> T78\nX40 -> X110", fontsize=14, style = filled, fillcolor = lightgrey];
103 -> 158 [arrowhead = none , style=dashed];
158 -> 45[style=dashed];

159 [label="INSTANCE with matching:\nT1 -> T90\nT2 -> T93\nT3 -> T94", fontsize=14, style = filled, fillcolor = lightgrey];
123 -> 159 [arrowhead = none , style=dashed];
159 -> 1[style=dashed];

}

(2) Obligation:

Q restricted rewrite system:
The TRS R consists of the following rules:

f1_in([]) → f1_out1
f1_in(.(.(T27, T28), T29)) → U1(f37_in(T29, T27, T28), .(.(T27, T28), T29))
U1(f37_out1, .(.(T27, T28), T29)) → f1_out1
f1_in(.(T89, T90)) → U2(f1_in(T90), .(T89, T90))
U2(f1_out1, .(T89, T90)) → f1_out1
f45_in([]) → f45_out1
f45_in(.(.(T59, T60), T61)) → U3(f87_in(T61, T59, T60), .(.(T59, T60), T61))
U3(f87_out1, .(.(T59, T60), T61)) → f45_out1
f45_in(.(T75, T76)) → U4(f45_in(T76), .(T75, T76))
U4(f45_out1, .(T75, T76)) → f45_out1
f37_in(T29, T27, T28) → U5(f45_in(T29), T29, T27, T28)
U5(f45_out1, T29, T27, T28) → U6(f1_in(.(T27, T28)), T29, T27, T28)
U6(f1_out1, T29, T27, T28) → f37_out1
f87_in(T61, T59, T60) → U7(f45_in(T61), T61, T59, T60)
U7(f45_out1, T61, T59, T60) → U8(f1_in(.(T59, T60)), T61, T59, T60)
U8(f1_out1, T61, T59, T60) → f87_out1

Q is empty.

(3) DependencyPairsProof (EQUIVALENT transformation)

Using Dependency Pairs [AG00,LPAR04] we result in the following initial DP problem.

(4) Obligation:

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

F1_IN(.(.(T27, T28), T29)) → U1¹(f37_in(T29, T27, T28), .(.(T27, T28), T29))
F1_IN(.(.(T27, T28), T29)) → F37_IN(T29, T27, T28)
F1_IN(.(T89, T90)) → U2¹(f1_in(T90), .(T89, T90))
F1_IN(.(T89, T90)) → F1_IN(T90)
F45_IN(.(.(T59, T60), T61)) → U3¹(f87_in(T61, T59, T60), .(.(T59, T60), T61))
F45_IN(.(.(T59, T60), T61)) → F87_IN(T61, T59, T60)
F45_IN(.(T75, T76)) → U4¹(f45_in(T76), .(T75, T76))
F45_IN(.(T75, T76)) → F45_IN(T76)
F37_IN(T29, T27, T28) → U5¹(f45_in(T29), T29, T27, T28)
F37_IN(T29, T27, T28) → F45_IN(T29)
U5¹(f45_out1, T29, T27, T28) → U6¹(f1_in(.(T27, T28)), T29, T27, T28)
U5¹(f45_out1, T29, T27, T28) → F1_IN(.(T27, T28))
F87_IN(T61, T59, T60) → U7¹(f45_in(T61), T61, T59, T60)
F87_IN(T61, T59, T60) → F45_IN(T61)
U7¹(f45_out1, T61, T59, T60) → U8¹(f1_in(.(T59, T60)), T61, T59, T60)
U7¹(f45_out1, T61, T59, T60) → F1_IN(.(T59, T60))

The TRS R consists of the following rules:

f1_in([]) → f1_out1
f1_in(.(.(T27, T28), T29)) → U1(f37_in(T29, T27, T28), .(.(T27, T28), T29))
U1(f37_out1, .(.(T27, T28), T29)) → f1_out1
f1_in(.(T89, T90)) → U2(f1_in(T90), .(T89, T90))
U2(f1_out1, .(T89, T90)) → f1_out1
f45_in([]) → f45_out1
f45_in(.(.(T59, T60), T61)) → U3(f87_in(T61, T59, T60), .(.(T59, T60), T61))
U3(f87_out1, .(.(T59, T60), T61)) → f45_out1
f45_in(.(T75, T76)) → U4(f45_in(T76), .(T75, T76))
U4(f45_out1, .(T75, T76)) → f45_out1
f37_in(T29, T27, T28) → U5(f45_in(T29), T29, T27, T28)
U5(f45_out1, T29, T27, T28) → U6(f1_in(.(T27, T28)), T29, T27, T28)
U6(f1_out1, T29, T27, T28) → f37_out1
f87_in(T61, T59, T60) → U7(f45_in(T61), T61, T59, T60)
U7(f45_out1, T61, T59, T60) → U8(f1_in(.(T59, T60)), T61, T59, T60)
U8(f1_out1, T61, T59, T60) → f87_out1

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

(5) DependencyGraphProof (EQUIVALENT transformation)

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

(6) Obligation:

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

F1_IN(.(.(T27, T28), T29)) → F37_IN(T29, T27, T28)
F37_IN(T29, T27, T28) → U5¹(f45_in(T29), T29, T27, T28)
U5¹(f45_out1, T29, T27, T28) → F1_IN(.(T27, T28))
F1_IN(.(T89, T90)) → F1_IN(T90)
F37_IN(T29, T27, T28) → F45_IN(T29)
F45_IN(.(.(T59, T60), T61)) → F87_IN(T61, T59, T60)
F87_IN(T61, T59, T60) → U7¹(f45_in(T61), T61, T59, T60)
U7¹(f45_out1, T61, T59, T60) → F1_IN(.(T59, T60))
F87_IN(T61, T59, T60) → F45_IN(T61)
F45_IN(.(T75, T76)) → F45_IN(T76)

The TRS R consists of the following rules:

f1_in([]) → f1_out1
f1_in(.(.(T27, T28), T29)) → U1(f37_in(T29, T27, T28), .(.(T27, T28), T29))
U1(f37_out1, .(.(T27, T28), T29)) → f1_out1
f1_in(.(T89, T90)) → U2(f1_in(T90), .(T89, T90))
U2(f1_out1, .(T89, T90)) → f1_out1
f45_in([]) → f45_out1
f45_in(.(.(T59, T60), T61)) → U3(f87_in(T61, T59, T60), .(.(T59, T60), T61))
U3(f87_out1, .(.(T59, T60), T61)) → f45_out1
f45_in(.(T75, T76)) → U4(f45_in(T76), .(T75, T76))
U4(f45_out1, .(T75, T76)) → f45_out1
f37_in(T29, T27, T28) → U5(f45_in(T29), T29, T27, T28)
U5(f45_out1, T29, T27, T28) → U6(f1_in(.(T27, T28)), T29, T27, T28)
U6(f1_out1, T29, T27, T28) → f37_out1
f87_in(T61, T59, T60) → U7(f45_in(T61), T61, T59, T60)
U7(f45_out1, T61, T59, T60) → U8(f1_in(.(T59, T60)), T61, T59, T60)
U8(f1_out1, T61, T59, T60) → f87_out1

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

(7) QDPOrderProof (EQUIVALENT transformation)

We use the reduction pair processor [LPAR04,JAR06].

The following pairs can be oriented strictly and are deleted.

U5¹(f45_out1, T29, T27, T28) → F1_IN(.(T27, T28))
F37_IN(T29, T27, T28) → F45_IN(T29)
F45_IN(.(.(T59, T60), T61)) → F87_IN(T61, T59, T60)
F87_IN(T61, T59, T60) → U7¹(f45_in(T61), T61, T59, T60)
U7¹(f45_out1, T61, T59, T60) → F1_IN(.(T59, T60))
F87_IN(T61, T59, T60) → F45_IN(T61)
F45_IN(.(T75, T76)) → F45_IN(T76)

The remaining pairs can at least be oriented weakly.
Used ordering: Polynomial Order [NEGPOLO,POLO] with Interpretation:

POL( U5¹(x₁, ..., x₄) ) = x₂ + 2x₃ + 2x₄ + 2

POL( U7¹(x₁, ..., x₄) ) = 2x₂ + 2x₃ + 2x₄ + 1

POL( f45_in(x₁) ) = 0

POL( [] ) = 1

POL( f45_out1 ) = 2

POL( .(x₁, x₂) ) = x₁ + x₂ + 1

POL( U3(x₁, x₂) ) = max{0, -2}

POL( f87_in(x₁, ..., x₃) ) = x₂ + 2x₃ + 1

POL( U4(x₁, x₂) ) = x₂ + 2

POL( f1_in(x₁) ) = max{0, -2}

POL( U1(x₁, x₂) ) = max{0, -2}

POL( f37_in(x₁, ..., x₃) ) = x₁ + 2x₃ + 1

POL( f37_out1 ) = 0

POL( f1_out1 ) = 0

POL( U5(x₁, ..., x₄) ) = max{0, x₁ + 2x₂ + x₃ + x₄ - 1}

POL( f87_out1 ) = 1

POL( U7(x₁, ..., x₄) ) = max{0, x₂ - 2}

POL( U8(x₁, ..., x₄) ) = max{0, 2x₁ + x₂ + x₃ + 2x₄ - 2}

POL( U2(x₁, x₂) ) = max{0, -2}

POL( U6(x₁, ..., x₄) ) = max{0, 2x₂ + 2x₃ + 2x₄ - 2}

POL( F1_IN(x₁) ) = max{0, 2x₁ - 2}

POL( F37_IN(x₁, ..., x₃) ) = 2x₁ + 2x₂ + 2x₃ + 2

POL( F45_IN(x₁) ) = 2x₁

POL( F87_IN(x₁, ..., x₃) ) = 2x₁ + 2x₂ + 2x₃ + 2

The following usable rules [FROCOS05] with respect to the argument filtering of the ordering [JAR06] were oriented:
none

(8) Obligation:

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

F1_IN(.(.(T27, T28), T29)) → F37_IN(T29, T27, T28)
F37_IN(T29, T27, T28) → U5¹(f45_in(T29), T29, T27, T28)
F1_IN(.(T89, T90)) → F1_IN(T90)

The TRS R consists of the following rules:

f1_in([]) → f1_out1
f1_in(.(.(T27, T28), T29)) → U1(f37_in(T29, T27, T28), .(.(T27, T28), T29))
U1(f37_out1, .(.(T27, T28), T29)) → f1_out1
f1_in(.(T89, T90)) → U2(f1_in(T90), .(T89, T90))
U2(f1_out1, .(T89, T90)) → f1_out1
f45_in([]) → f45_out1
f45_in(.(.(T59, T60), T61)) → U3(f87_in(T61, T59, T60), .(.(T59, T60), T61))
U3(f87_out1, .(.(T59, T60), T61)) → f45_out1
f45_in(.(T75, T76)) → U4(f45_in(T76), .(T75, T76))
U4(f45_out1, .(T75, T76)) → f45_out1
f37_in(T29, T27, T28) → U5(f45_in(T29), T29, T27, T28)
U5(f45_out1, T29, T27, T28) → U6(f1_in(.(T27, T28)), T29, T27, T28)
U6(f1_out1, T29, T27, T28) → f37_out1
f87_in(T61, T59, T60) → U7(f45_in(T61), T61, T59, T60)
U7(f45_out1, T61, T59, T60) → U8(f1_in(.(T59, T60)), T61, T59, T60)
U8(f1_out1, T61, T59, T60) → f87_out1

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

(9) DependencyGraphProof (EQUIVALENT transformation)

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

(10) Obligation:

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

F1_IN(.(T89, T90)) → F1_IN(T90)

The TRS R consists of the following rules:

f1_in([]) → f1_out1
f1_in(.(.(T27, T28), T29)) → U1(f37_in(T29, T27, T28), .(.(T27, T28), T29))
U1(f37_out1, .(.(T27, T28), T29)) → f1_out1
f1_in(.(T89, T90)) → U2(f1_in(T90), .(T89, T90))
U2(f1_out1, .(T89, T90)) → f1_out1
f45_in([]) → f45_out1
f45_in(.(.(T59, T60), T61)) → U3(f87_in(T61, T59, T60), .(.(T59, T60), T61))
U3(f87_out1, .(.(T59, T60), T61)) → f45_out1
f45_in(.(T75, T76)) → U4(f45_in(T76), .(T75, T76))
U4(f45_out1, .(T75, T76)) → f45_out1
f37_in(T29, T27, T28) → U5(f45_in(T29), T29, T27, T28)
U5(f45_out1, T29, T27, T28) → U6(f1_in(.(T27, T28)), T29, T27, T28)
U6(f1_out1, T29, T27, T28) → f37_out1
f87_in(T61, T59, T60) → U7(f45_in(T61), T61, T59, T60)
U7(f45_out1, T61, T59, T60) → U8(f1_in(.(T59, T60)), T61, T59, T60)
U8(f1_out1, T61, T59, T60) → f87_out1

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

(11) UsableRulesProof (EQUIVALENT transformation)

We can use the usable rules and reduction pair processor [LPAR04] with the Ce-compatible extension of the polynomial order that maps every function symbol to the sum of its arguments. Then, we can delete all non-usable rules [FROCOS05] from R.

(12) Obligation:

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

F1_IN(.(T89, T90)) → F1_IN(T90)

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

(13) 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:

• F1_IN(.(T89, T90)) → F1_IN(T90)
  The graph contains the following edges 1 > 1

(14) YES