Left Termination proof of /tmp/tmpjWSPqf/palindrome.pl

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

0 Prolog

↳1 PrologToPrologProblemTransformerProof (⇐)

↳2 Prolog

↳3 PrologToPiTRSProof (⇐)

↳4 PiTRS

↳5 DependencyPairsProof (⇔)

↳6 PiDP

↳7 DependencyGraphProof (⇔)

↳8 PiDP

↳9 UsableRulesProof (⇔)

↳10 PiDP

↳11 PiDPToQDPProof (⇔)

↳12 QDP

↳13 QDPSizeChangeProof (⇔)

↳14 YES

(0) Obligation:

Clauses:

palindrome(Xs) :- reverse(Xs, Xs).
reverse(X1s, X2s) :- reverse(X1s, [], X2s).
reverse([], Xs, Xs).
reverse(.(X, X1s), X2s, Ys) :- reverse(X1s, .(X, X2s), Ys).

Queries:

palindrome(g).

(1) PrologToPrologProblemTransformerProof (SOUND transformation)

Built Prolog problem from termination graph.

digraph dp_graph {
node [outthreshold=100, inthreshold=100];
1 [label="1: palindrome(T1)\n\nT1 is ground", fontsize=16, style=filled, fillcolor=lightyellow, color=red];
2 [label="2: palindrome(T1), SCOPE: 1, CLAUSE: 0\n\nT1 is ground", fontsize=16, style=filled, fillcolor=lightyellow];
3 [label="3: reverse(T3, T3)\n\nT3 is ground", fontsize=16, style=filled, fillcolor=lightyellow];
4 [label="4: reverse(T3, T3), SCOPE: 2, CLAUSE: 1\n\nT3 is ground", fontsize=16, style=filled, fillcolor=lightyellow];
5 [label="5: reverse(T6, [], T6)\n\nT6 is ground", fontsize=16, style=filled, fillcolor=lightyellow];
6 [label="6: reverse(T6, [], T6), SCOPE: 3, CLAUSE: 2 | reverse(T6, [], T6), SCOPE: 3, CLAUSE: 3\n\nT6 is ground", fontsize=16, style=filled, fillcolor=lightyellow];
7 [label="7: reverse(T6, [], T6), SCOPE: 3, CLAUSE: 2\n\nT6 is ground", fontsize=16, style=filled, fillcolor=lightyellow];
8 [label="8: reverse(T6, [], T6), SCOPE: 3, CLAUSE: 3\n\nT6 is ground", fontsize=16, style=filled, fillcolor=lightyellow];
9 [label="9: true\n\n", fontsize=16, style=filled, fillcolor=lightyellow];
10 [label="10: \n\n", fontsize=16, style=filled, fillcolor=lightyellow];
11 [label="11: \n\n", fontsize=16, style=filled, fillcolor=lightyellow];
12 [label="12: reverse(T12, .(T11, []), .(T11, T12))\n\nT11 is ground\nT12 is ground", fontsize=16, style=filled, fillcolor=lightyellow];
13 [label="13: \n\n", fontsize=16, style=filled, fillcolor=lightyellow];
14 [label="14: reverse(T12, .(T11, []), .(T11, T12)), SCOPE: 4, CLAUSE: 2 | reverse(T12, .(T11, []), .(T11, T12)), SCOPE: 4, CLAUSE: 3\n\nT11 is ground\nT12 is ground", fontsize=16, style=filled, fillcolor=lightyellow];
15 [label="15: reverse(T12, .(T11, []), .(T11, T12)), SCOPE: 4, CLAUSE: 2\n\nT11 is ground\nT12 is ground", fontsize=16, style=filled, fillcolor=lightyellow];
16 [label="16: reverse(T12, .(T11, []), .(T11, T12)), SCOPE: 4, CLAUSE: 3\n\nT11 is ground\nT12 is ground", fontsize=16, style=filled, fillcolor=lightyellow];
17 [label="17: true\n\n", fontsize=16, style=filled, fillcolor=lightyellow];
18 [label="18: \n\n", fontsize=16, style=filled, fillcolor=lightyellow];
19 [label="19: \n\n", fontsize=16, style=filled, fillcolor=lightyellow];
20 [label="20: reverse(T27, .(T26, .(T28, [])), .(T28, .(T26, T27)))\n\nT26 is ground\nT27 is ground\nT28 is ground", fontsize=16, style=filled, fillcolor=lightyellow];
21 [label="21: \n\n", fontsize=16, style=filled, fillcolor=lightyellow];
22 [label="22: reverse(T27, .(T26, .(T28, [])), .(T28, .(T26, T27))), SCOPE: 5, CLAUSE: 2 | reverse(T27, .(T26, .(T28, [])), .(T28, .(T26, T27))), SCOPE: 5, CLAUSE: 3\n\nT26 is ground\nT27 is ground\nT28 is ground", fontsize=16, style=filled, fillcolor=lightyellow];
23 [label="23: reverse(T27, .(T26, .(T28, [])), .(T28, .(T26, T27))), SCOPE: 5, CLAUSE: 2\n\nT26 is ground\nT27 is ground\nT28 is ground", fontsize=16, style=filled, fillcolor=lightyellow];
24 [label="24: reverse(T27, .(T26, .(T28, [])), .(T28, .(T26, T27))), SCOPE: 5, CLAUSE: 3\n\nT26 is ground\nT27 is ground\nT28 is ground", fontsize=16, style=filled, fillcolor=lightyellow];
25 [label="25: true\n\n", fontsize=16, style=filled, fillcolor=lightyellow];
26 [label="26: \n\n", fontsize=16, style=filled, fillcolor=lightyellow];
27 [label="27: \n\n", fontsize=16, style=filled, fillcolor=lightyellow];
28 [label="28: reverse(T52, .(T51, .(T53, .(T54, []))), .(T54, .(T53, .(T51, T52))))\n\nT51 is ground\nT52 is ground\nT53 is ground\nT54 is ground", fontsize=16, style=filled, fillcolor=lightyellow];
29 [label="29: \n\n", fontsize=16, style=filled, fillcolor=lightyellow];
30 [label="30: reverse(T52, .(T51, .(T53, .(T54, []))), .(T54, .(T53, .(T51, T52)))), SCOPE: 6, CLAUSE: 2 | reverse(T52, .(T51, .(T53, .(T54, []))), .(T54, .(T53, .(T51, T52)))), SCOPE: 6, CLAUSE: 3\n\nT51 is ground\nT52 is ground\nT53 is ground\nT54 is ground", fontsize=16, style=filled, fillcolor=lightyellow];
31 [label="31: reverse(T52, .(T51, .(T53, .(T54, []))), .(T54, .(T53, .(T51, T52)))), SCOPE: 6, CLAUSE: 2\n\nT51 is ground\nT52 is ground\nT53 is ground\nT54 is ground", fontsize=16, style=filled, fillcolor=lightyellow];
32 [label="32: reverse(T52, .(T51, .(T53, .(T54, []))), .(T54, .(T53, .(T51, T52)))), SCOPE: 6, CLAUSE: 3\n\nT51 is ground\nT52 is ground\nT53 is ground\nT54 is ground", fontsize=16, style=filled, fillcolor=lightyellow];
33 [label="33: true\n\n", fontsize=16, style=filled, fillcolor=lightyellow];
34 [label="34: \n\n", fontsize=16, style=filled, fillcolor=lightyellow];
35 [label="35: \n\n", fontsize=16, style=filled, fillcolor=lightyellow];
36 [label="36: reverse(T87, .(T86, .(T88, .(T89, .(T90, [])))), .(T90, .(T89, .(T88, .(T86, T87)))))\n\nT86 is ground\nT87 is ground\nT88 is ground\nT89 is ground\nT90 is ground", fontsize=16, style=filled, fillcolor=lightyellow];
37 [label="37: \n\n", fontsize=16, style=filled, fillcolor=lightyellow];
38 [label="38: reverse(T87, .(T86, .(T88, .(T89, .(T90, [])))), .(T90, .(T89, .(T88, .(T86, T87))))), SCOPE: 7, CLAUSE: 2 | reverse(T87, .(T86, .(T88, .(T89, .(T90, [])))), .(T90, .(T89, .(T88, .(T86, T87))))), SCOPE: 7, CLAUSE: 3\n\nT86 is ground\nT87 is ground\nT88 is ground\nT89 is ground\nT90 is ground", fontsize=16, style=filled, fillcolor=lightyellow];
39 [label="39: reverse(T87, .(T86, .(T88, .(T89, .(T90, [])))), .(T90, .(T89, .(T88, .(T86, T87))))), SCOPE: 7, CLAUSE: 2\n\nT86 is ground\nT87 is ground\nT88 is ground\nT89 is ground\nT90 is ground", fontsize=16, style=filled, fillcolor=lightyellow];
40 [label="40: reverse(T87, .(T86, .(T88, .(T89, .(T90, [])))), .(T90, .(T89, .(T88, .(T86, T87))))), SCOPE: 7, CLAUSE: 3\n\nT86 is ground\nT87 is ground\nT88 is ground\nT89 is ground\nT90 is ground", fontsize=16, style=filled, fillcolor=lightyellow];
41 [label="41: true\n\n", fontsize=16, style=filled, fillcolor=lightyellow];
42 [label="42: \n\n", fontsize=16, style=filled, fillcolor=lightyellow];
43 [label="43: \n\n", fontsize=16, style=filled, fillcolor=lightyellow];
44 [label="44: reverse(T132, .(T131, .(T133, .(T134, .(T135, .(T136, []))))), .(T136, .(T135, .(T134, .(T133, .(T131, T132))))))\n\nT131 is ground\nT132 is ground\nT133 is ground\nT134 is ground\nT135 is ground\nT136 is ground", fontsize=16, style=filled, fillcolor=lightyellow];
45 [label="45: \n\n", fontsize=16, style=filled, fillcolor=lightyellow];
46 [label="46: reverse(T132, .(T131, .(T133, .(T134, .(T135, .(T136, []))))), .(T136, .(T135, .(T134, .(T133, .(T131, T132)))))), SCOPE: 8, CLAUSE: 2 | reverse(T132, .(T131, .(T133, .(T134, .(T135, .(T136, []))))), .(T136, .(T135, .(T134, .(T133, .(T131, T132)))))), SCOPE: 8, CLAUSE: 3\n\nT131 is ground\nT132 is ground\nT133 is ground\nT134 is ground\nT135 is ground\nT136 is ground", fontsize=16, style=filled, fillcolor=lightyellow];
47 [label="47: reverse(T132, .(T131, .(T133, .(T134, .(T135, .(T136, []))))), .(T136, .(T135, .(T134, .(T133, .(T131, T132)))))), SCOPE: 8, CLAUSE: 2\n\nT131 is ground\nT132 is ground\nT133 is ground\nT134 is ground\nT135 is ground\nT136 is ground", fontsize=16, style=filled, fillcolor=lightyellow];
48 [label="48: reverse(T132, .(T131, .(T133, .(T134, .(T135, .(T136, []))))), .(T136, .(T135, .(T134, .(T133, .(T131, T132)))))), SCOPE: 8, CLAUSE: 3\n\nT131 is ground\nT132 is ground\nT133 is ground\nT134 is ground\nT135 is ground\nT136 is ground", fontsize=16, style=filled, fillcolor=lightyellow];
49 [label="49: true\n\n", fontsize=16, style=filled, fillcolor=lightyellow];
50 [label="50: \n\n", fontsize=16, style=filled, fillcolor=lightyellow];
51 [label="51: \n\n", fontsize=16, style=filled, fillcolor=lightyellow];
52 [label="52: reverse(T187, .(T186, .(T188, .(T189, .(T190, .(T191, .(T192, [])))))), .(T192, .(T191, .(T190, .(T189, .(T188, .(T186, T187)))))))\n\nT186 is ground\nT187 is ground\nT188 is ground\nT189 is ground\nT190 is ground\nT191 is ground\nT192 is ground", fontsize=16, style=filled, fillcolor=lightyellow];
53 [label="53: \n\n", fontsize=16, style=filled, fillcolor=lightyellow];
54 [label="54: reverse(T187, .(T186, .(T188, .(T189, .(T190, .(T191, .(T192, [])))))), .(T192, .(T191, .(T190, .(T189, .(T188, .(T186, T187))))))), SCOPE: 9, CLAUSE: 2 | reverse(T187, .(T186, .(T188, .(T189, .(T190, .(T191, .(T192, [])))))), .(T192, .(T191, .(T190, .(T189, .(T188, .(T186, T187))))))), SCOPE: 9, CLAUSE: 3\n\nT186 is ground\nT187 is ground\nT188 is ground\nT189 is ground\nT190 is ground\nT191 is ground\nT192 is ground", fontsize=16, style=filled, fillcolor=lightyellow];
55 [label="55: reverse(T187, .(T186, .(T188, .(T189, .(T190, .(T191, .(T192, [])))))), .(T192, .(T191, .(T190, .(T189, .(T188, .(T186, T187))))))), SCOPE: 9, CLAUSE: 2\n\nT186 is ground\nT187 is ground\nT188 is ground\nT189 is ground\nT190 is ground\nT191 is ground\nT192 is ground", fontsize=16, style=filled, fillcolor=lightyellow];
56 [label="56: reverse(T187, .(T186, .(T188, .(T189, .(T190, .(T191, .(T192, [])))))), .(T192, .(T191, .(T190, .(T189, .(T188, .(T186, T187))))))), SCOPE: 9, CLAUSE: 3\n\nT186 is ground\nT187 is ground\nT188 is ground\nT189 is ground\nT190 is ground\nT191 is ground\nT192 is ground", fontsize=16, style=filled, fillcolor=lightyellow];
57 [label="57: true\n\n", fontsize=16, style=filled, fillcolor=lightyellow];
58 [label="58: \n\n", fontsize=16, style=filled, fillcolor=lightyellow];
59 [label="59: \n\n", fontsize=16, style=filled, fillcolor=lightyellow];
60 [label="60: reverse(T252, .(T251, .(T253, .(T254, .(T255, .(T256, .(T257, .(T258, []))))))), .(T258, .(T257, .(T256, .(T255, .(T254, .(T253, .(T251, T252))))))))\n\nT251 is ground\nT252 is ground\nT253 is ground\nT254 is ground\nT255 is ground\nT256 is ground\nT257 is ground\nT258 is ground", fontsize=16, style=filled, fillcolor=lightyellow];
61 [label="61: \n\n", fontsize=16, style=filled, fillcolor=lightyellow];
62 [label="62: reverse(T252, .(T251, .(T253, .(T254, .(T255, .(T256, .(T257, .(T258, []))))))), .(T258, .(T257, .(T256, .(T255, .(T254, .(T253, .(T251, T252)))))))), SCOPE: 10, CLAUSE: 2 | reverse(T252, .(T251, .(T253, .(T254, .(T255, .(T256, .(T257, .(T258, []))))))), .(T258, .(T257, .(T256, .(T255, .(T254, .(T253, .(T251, T252)))))))), SCOPE: 10, CLAUSE: 3\n\nT251 is ground\nT252 is ground\nT253 is ground\nT254 is ground\nT255 is ground\nT256 is ground\nT257 is ground\nT258 is ground", fontsize=16, style=filled, fillcolor=lightyellow];
63 [label="63: reverse(T252, .(T251, .(T253, .(T254, .(T255, .(T256, .(T257, .(T258, []))))))), .(T258, .(T257, .(T256, .(T255, .(T254, .(T253, .(T251, T252)))))))), SCOPE: 10, CLAUSE: 2\n\nT251 is ground\nT252 is ground\nT253 is ground\nT254 is ground\nT255 is ground\nT256 is ground\nT257 is ground\nT258 is ground", fontsize=16, style=filled, fillcolor=lightyellow];
64 [label="64: reverse(T252, .(T251, .(T253, .(T254, .(T255, .(T256, .(T257, .(T258, []))))))), .(T258, .(T257, .(T256, .(T255, .(T254, .(T253, .(T251, T252)))))))), SCOPE: 10, CLAUSE: 3\n\nT251 is ground\nT252 is ground\nT253 is ground\nT254 is ground\nT255 is ground\nT256 is ground\nT257 is ground\nT258 is ground", fontsize=16, style=filled, fillcolor=lightyellow];
65 [label="65: true\n\n", fontsize=16, style=filled, fillcolor=lightyellow];
66 [label="66: \n\n", fontsize=16, style=filled, fillcolor=lightyellow];
67 [label="67: \n\n", fontsize=16, style=filled, fillcolor=lightyellow];
68 [label="68: reverse(T327, .(T326, .(T328, .(T329, .(T330, .(T331, .(T332, .(T333, .(T334, [])))))))), .(T334, .(T333, .(T332, .(T331, .(T330, .(T329, .(T328, .(T326, T327)))))))))\n\nT326 is ground\nT327 is ground\nT328 is ground\nT329 is ground\nT330 is ground\nT331 is ground\nT332 is ground\nT333 is ground\nT334 is ground", fontsize=16, style=filled, fillcolor=lightyellow];
69 [label="69: \n\n", fontsize=16, style=filled, fillcolor=lightyellow];
70 [label="70: reverse(T327, .(T326, T351), .(T334, T352))\n\nT326 is ground\nT327 is ground\nT334 is ground\nT351 is ground\nT352 is ground", fontsize=16, style=filled, fillcolor=lightyellow];
71 [label="71: reverse(T327, .(T326, T351), .(T334, T352)), SCOPE: 11, CLAUSE: 2 | reverse(T327, .(T326, T351), .(T334, T352)), SCOPE: 11, CLAUSE: 3\n\nT326 is ground\nT327 is ground\nT334 is ground\nT351 is ground\nT352 is ground", fontsize=16, style=filled, fillcolor=lightyellow];
72 [label="72: reverse(T327, .(T326, T351), .(T334, T352)), SCOPE: 11, CLAUSE: 2\n\nT326 is ground\nT327 is ground\nT334 is ground\nT351 is ground\nT352 is ground", fontsize=16, style=filled, fillcolor=lightyellow];
73 [label="73: reverse(T327, .(T326, T351), .(T334, T352)), SCOPE: 11, CLAUSE: 3\n\nT326 is ground\nT327 is ground\nT334 is ground\nT351 is ground\nT352 is ground", fontsize=16, style=filled, fillcolor=lightyellow];
74 [label="74: true\n\n", fontsize=16, style=filled, fillcolor=lightyellow];
75 [label="75: \n\n", fontsize=16, style=filled, fillcolor=lightyellow];
76 [label="76: \n\n", fontsize=16, style=filled, fillcolor=lightyellow];
77 [label="77: reverse(T380, .(T379, .(T381, T382)), .(T383, T384))\n\nT379 is ground\nT380 is ground\nT381 is ground\nT382 is ground\nT383 is ground\nT384 is ground", fontsize=16, style=filled, fillcolor=lightyellow];
78 [label="78: \n\n", fontsize=16, style=filled, fillcolor=lightyellow];
79 [label="CASE", fontsize=14, style = filled, fillcolor = lightcyan];
1 -> 79 [arrowhead = none ];
79 -> 2;

80 [label="ONLY EVAL with clause\npalindrome(X2) :- reverse(X2, X2).\nand substitution\nT1 -> T3\nX2 -> T3", fontsize=14, style = filled, fillcolor = white];
2 -> 80 [arrowhead = none ];
80 -> 3;

81 [label="CASE", fontsize=14, style = filled, fillcolor = lightcyan];
3 -> 81 [arrowhead = none ];
81 -> 4;

82 [label="ONLY EVAL with clause\nreverse(X9, X10) :- reverse(X9, [], X10).\nand substitution\nT3 -> T6\nX9 -> T6\nX10 -> T6", fontsize=14, style = filled, fillcolor = white];
4 -> 82 [arrowhead = none ];
82 -> 5;

83 [label="CASE", fontsize=14, style = filled, fillcolor = lightcyan];
5 -> 83 [arrowhead = none ];
83 -> 6;

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

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

86 [label="EVAL with clause\nreverse([], X17, X17).\nand substitution\nT6 -> []\nX17 -> []", fontsize=14, style = filled, fillcolor = lightblue];
7 -> 86 [arrowhead = none ];
86 -> 9;

87 [label="EVAL-BACKTRACK", fontsize=14, style = filled, fillcolor = lightblue];
7 -> 87 [arrowhead = none ];
87 -> 10;

88 [label="EVAL with clause\nreverse(.(X27, X28), X29, X30) :- reverse(X28, .(X27, X29), X30).\nand substitution\nX27 -> T11\nX28 -> T12\nT6 -> .(T11, T12)\nX29 -> []\nX30 -> .(T11, T12)", fontsize=14, style = filled, fillcolor = lightblue];
8 -> 88 [arrowhead = none ];
88 -> 12;

89 [label="EVAL-BACKTRACK", fontsize=14, style = filled, fillcolor = lightblue];
8 -> 89 [arrowhead = none ];
89 -> 13;

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

91 [label="CASE", fontsize=14, style = filled, fillcolor = lightcyan];
12 -> 91 [arrowhead = none ];
91 -> 14;

92 [label="PARALLEL", fontsize=14, style = filled, fillcolor = violet];
14 -> 92 [arrowhead = none ];
92 -> 15;

93 [label="PARALLEL", fontsize=14, style = filled, fillcolor = violet];
14 -> 93 [arrowhead = none ];
93 -> 16;

94 [label="EVAL with clause\nreverse([], X41, X41).\nand substitution\nT12 -> []\nT11 -> T19\nX41 -> .(T19, [])", fontsize=14, style = filled, fillcolor = lightblue];
15 -> 94 [arrowhead = none ];
94 -> 17;

95 [label="EVAL-BACKTRACK", fontsize=14, style = filled, fillcolor = lightblue];
15 -> 95 [arrowhead = none ];
95 -> 18;

96 [label="EVAL with clause\nreverse(.(X51, X52), X53, X54) :- reverse(X52, .(X51, X53), X54).\nand substitution\nX51 -> T26\nX52 -> T27\nT12 -> .(T26, T27)\nT11 -> T28\nX53 -> .(T28, [])\nX54 -> .(T28, .(T26, T27))", fontsize=14, style = filled, fillcolor = lightblue];
16 -> 96 [arrowhead = none ];
96 -> 20;

97 [label="EVAL-BACKTRACK", fontsize=14, style = filled, fillcolor = lightblue];
16 -> 97 [arrowhead = none ];
97 -> 21;

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

99 [label="CASE", fontsize=14, style = filled, fillcolor = lightcyan];
20 -> 99 [arrowhead = none ];
99 -> 22;

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

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

102 [label="EVAL with clause\nreverse([], X65, X65).\nand substitution\nT27 -> []\nT26 -> T42\nT28 -> T42\nX65 -> .(T42, .(T42, []))\nT41 -> T42", fontsize=14, style = filled, fillcolor = lightblue];
23 -> 102 [arrowhead = none ];
102 -> 25;

103 [label="EVAL-BACKTRACK", fontsize=14, style = filled, fillcolor = lightblue];
23 -> 103 [arrowhead = none ];
103 -> 26;

104 [label="EVAL with clause\nreverse(.(X75, X76), X77, X78) :- reverse(X76, .(X75, X77), X78).\nand substitution\nX75 -> T51\nX76 -> T52\nT27 -> .(T51, T52)\nT26 -> T53\nT28 -> T54\nX77 -> .(T53, .(T54, []))\nX78 -> .(T54, .(T53, .(T51, T52)))", fontsize=14, style = filled, fillcolor = lightblue];
24 -> 104 [arrowhead = none ];
104 -> 28;

105 [label="EVAL-BACKTRACK", fontsize=14, style = filled, fillcolor = lightblue];
24 -> 105 [arrowhead = none ];
105 -> 29;

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

107 [label="CASE", fontsize=14, style = filled, fillcolor = lightcyan];
28 -> 107 [arrowhead = none ];
107 -> 30;

108 [label="PARALLEL", fontsize=14, style = filled, fillcolor = violet];
30 -> 108 [arrowhead = none ];
108 -> 31;

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

110 [label="EVAL with clause\nreverse([], X89, X89).\nand substitution\nT52 -> []\nT51 -> T75\nT53 -> T74\nT54 -> T75\nX89 -> .(T75, .(T74, .(T75, [])))\nT73 -> T75", fontsize=14, style = filled, fillcolor = lightblue];
31 -> 110 [arrowhead = none ];
110 -> 33;

111 [label="EVAL-BACKTRACK", fontsize=14, style = filled, fillcolor = lightblue];
31 -> 111 [arrowhead = none ];
111 -> 34;

112 [label="EVAL with clause\nreverse(.(X99, X100), X101, X102) :- reverse(X100, .(X99, X101), X102).\nand substitution\nX99 -> T86\nX100 -> T87\nT52 -> .(T86, T87)\nT51 -> T88\nT53 -> T89\nT54 -> T90\nX101 -> .(T88, .(T89, .(T90, [])))\nX102 -> .(T90, .(T89, .(T88, .(T86, T87))))", fontsize=14, style = filled, fillcolor = lightblue];
32 -> 112 [arrowhead = none ];
112 -> 36;

113 [label="EVAL-BACKTRACK", fontsize=14, style = filled, fillcolor = lightblue];
32 -> 113 [arrowhead = none ];
113 -> 37;

114 [label="SUCCESS", fontsize=14, style = filled, fillcolor = lightgreen];
33 -> 114 [arrowhead = none ];
114 -> 35;

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

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

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

118 [label="EVAL with clause\nreverse([], X113, X113).\nand substitution\nT87 -> []\nT86 -> T118\nT88 -> T117\nT89 -> T117\nT90 -> T118\nX113 -> .(T118, .(T117, .(T117, .(T118, []))))\nT115 -> T118\nT116 -> T117", fontsize=14, style = filled, fillcolor = lightblue];
39 -> 118 [arrowhead = none ];
118 -> 41;

119 [label="EVAL-BACKTRACK", fontsize=14, style = filled, fillcolor = lightblue];
39 -> 119 [arrowhead = none ];
119 -> 42;

120 [label="EVAL with clause\nreverse(.(X123, X124), X125, X126) :- reverse(X124, .(X123, X125), X126).\nand substitution\nX123 -> T131\nX124 -> T132\nT87 -> .(T131, T132)\nT86 -> T133\nT88 -> T134\nT89 -> T135\nT90 -> T136\nX125 -> .(T133, .(T134, .(T135, .(T136, []))))\nX126 -> .(T136, .(T135, .(T134, .(T133, .(T131, T132)))))", fontsize=14, style = filled, fillcolor = lightblue];
40 -> 120 [arrowhead = none ];
120 -> 44;

121 [label="EVAL-BACKTRACK", fontsize=14, style = filled, fillcolor = lightblue];
40 -> 121 [arrowhead = none ];
121 -> 45;

122 [label="SUCCESS", fontsize=14, style = filled, fillcolor = lightgreen];
41 -> 122 [arrowhead = none ];
122 -> 43;

123 [label="CASE", fontsize=14, style = filled, fillcolor = lightcyan];
44 -> 123 [arrowhead = none ];
123 -> 46;

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

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

126 [label="EVAL with clause\nreverse([], X137, X137).\nand substitution\nT132 -> []\nT131 -> T171\nT133 -> T170\nT134 -> T169\nT135 -> T170\nT136 -> T171\nX137 -> .(T171, .(T170, .(T169, .(T170, .(T171, [])))))\nT167 -> T171\nT168 -> T170", fontsize=14, style = filled, fillcolor = lightblue];
47 -> 126 [arrowhead = none ];
126 -> 49;

127 [label="EVAL-BACKTRACK", fontsize=14, style = filled, fillcolor = lightblue];
47 -> 127 [arrowhead = none ];
127 -> 50;

128 [label="EVAL with clause\nreverse(.(X147, X148), X149, X150) :- reverse(X148, .(X147, X149), X150).\nand substitution\nX147 -> T186\nX148 -> T187\nT132 -> .(T186, T187)\nT131 -> T188\nT133 -> T189\nT134 -> T190\nT135 -> T191\nT136 -> T192\nX149 -> .(T188, .(T189, .(T190, .(T191, .(T192, [])))))\nX150 -> .(T192, .(T191, .(T190, .(T189, .(T188, .(T186, T187))))))", fontsize=14, style = filled, fillcolor = lightblue];
48 -> 128 [arrowhead = none ];
128 -> 52;

129 [label="EVAL-BACKTRACK", fontsize=14, style = filled, fillcolor = lightblue];
48 -> 129 [arrowhead = none ];
129 -> 53;

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

131 [label="CASE", fontsize=14, style = filled, fillcolor = lightcyan];
52 -> 131 [arrowhead = none ];
131 -> 54;

132 [label="PARALLEL", fontsize=14, style = filled, fillcolor = violet];
54 -> 132 [arrowhead = none ];
132 -> 55;

133 [label="PARALLEL", fontsize=14, style = filled, fillcolor = violet];
54 -> 133 [arrowhead = none ];
133 -> 56;

134 [label="EVAL with clause\nreverse([], X161, X161).\nand substitution\nT187 -> []\nT186 -> T234\nT188 -> T233\nT189 -> T232\nT190 -> T232\nT191 -> T233\nT192 -> T234\nX161 -> .(T234, .(T233, .(T232, .(T232, .(T233, .(T234, []))))))\nT229 -> T234\nT230 -> T233\nT231 -> T232", fontsize=14, style = filled, fillcolor = lightblue];
55 -> 134 [arrowhead = none ];
134 -> 57;

135 [label="EVAL-BACKTRACK", fontsize=14, style = filled, fillcolor = lightblue];
55 -> 135 [arrowhead = none ];
135 -> 58;

136 [label="EVAL with clause\nreverse(.(X171, X172), X173, X174) :- reverse(X172, .(X171, X173), X174).\nand substitution\nX171 -> T251\nX172 -> T252\nT187 -> .(T251, T252)\nT186 -> T253\nT188 -> T254\nT189 -> T255\nT190 -> T256\nT191 -> T257\nT192 -> T258\nX173 -> .(T253, .(T254, .(T255, .(T256, .(T257, .(T258, []))))))\nX174 -> .(T258, .(T257, .(T256, .(T255, .(T254, .(T253, .(T251, T252)))))))", fontsize=14, style = filled, fillcolor = lightblue];
56 -> 136 [arrowhead = none ];
136 -> 60;

137 [label="EVAL-BACKTRACK", fontsize=14, style = filled, fillcolor = lightblue];
56 -> 137 [arrowhead = none ];
137 -> 61;

138 [label="SUCCESS", fontsize=14, style = filled, fillcolor = lightgreen];
57 -> 138 [arrowhead = none ];
138 -> 59;

139 [label="CASE", fontsize=14, style = filled, fillcolor = lightcyan];
60 -> 139 [arrowhead = none ];
139 -> 62;

140 [label="PARALLEL", fontsize=14, style = filled, fillcolor = violet];
62 -> 140 [arrowhead = none ];
140 -> 63;

141 [label="PARALLEL", fontsize=14, style = filled, fillcolor = violet];
62 -> 141 [arrowhead = none ];
141 -> 64;

142 [label="EVAL with clause\nreverse([], X185, X185).\nand substitution\nT252 -> []\nT251 -> T307\nT253 -> T306\nT254 -> T305\nT255 -> T304\nT256 -> T305\nT257 -> T306\nT258 -> T307\nX185 -> .(T307, .(T306, .(T305, .(T304, .(T305, .(T306, .(T307, [])))))))\nT301 -> T307\nT302 -> T306\nT303 -> T305", fontsize=14, style = filled, fillcolor = lightblue];
63 -> 142 [arrowhead = none ];
142 -> 65;

143 [label="EVAL-BACKTRACK", fontsize=14, style = filled, fillcolor = lightblue];
63 -> 143 [arrowhead = none ];
143 -> 66;

144 [label="EVAL with clause\nreverse(.(X195, X196), X197, X198) :- reverse(X196, .(X195, X197), X198).\nand substitution\nX195 -> T326\nX196 -> T327\nT252 -> .(T326, T327)\nT251 -> T328\nT253 -> T329\nT254 -> T330\nT255 -> T331\nT256 -> T332\nT257 -> T333\nT258 -> T334\nX197 -> .(T328, .(T329, .(T330, .(T331, .(T332, .(T333, .(T334, [])))))))\nX198 -> .(T334, .(T333, .(T332, .(T331, .(T330, .(T329, .(T328, .(T326, T327))))))))", fontsize=14, style = filled, fillcolor = lightblue];
64 -> 144 [arrowhead = none ];
144 -> 68;

145 [label="EVAL-BACKTRACK", fontsize=14, style = filled, fillcolor = lightblue];
64 -> 145 [arrowhead = none ];
145 -> 69;

146 [label="SUCCESS", fontsize=14, style = filled, fillcolor = lightgreen];
65 -> 146 [arrowhead = none ];
146 -> 67;

147 [label="GENERALIZATION\nT351 <-- .(T328, .(T329, .(T330, .(T331, .(T332, .(T333, .(T334, [])))))))\nT352 <-- .(T333, .(T332, .(T331, .(T330, .(T329, .(T328, .(T326, T327)))))))\n\nNew Knowledge:\nT351 is ground\nT352 is ground", fontsize=14, style = filled, fillcolor = violet];
68 -> 147 [arrowhead = none ];
147 -> 70;

148 [label="CASE", fontsize=14, style = filled, fillcolor = lightcyan];
70 -> 148 [arrowhead = none ];
148 -> 71;

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

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

151 [label="EVAL with clause\nreverse([], X211, X211).\nand substitution\nT327 -> []\nT326 -> T365\nT351 -> T366\nX211 -> .(T365, T366)\nT334 -> T365\nT352 -> T366", fontsize=14, style = filled, fillcolor = lightblue];
72 -> 151 [arrowhead = none ];
151 -> 74;

152 [label="EVAL-BACKTRACK", fontsize=14, style = filled, fillcolor = lightblue];
72 -> 152 [arrowhead = none ];
152 -> 75;

153 [label="EVAL with clause\nreverse(.(X221, X222), X223, X224) :- reverse(X222, .(X221, X223), X224).\nand substitution\nX221 -> T379\nX222 -> T380\nT327 -> .(T379, T380)\nT326 -> T381\nT351 -> T382\nX223 -> .(T381, T382)\nT334 -> T383\nT352 -> T384\nX224 -> .(T383, T384)", fontsize=14, style = filled, fillcolor = lightblue];
73 -> 153 [arrowhead = none ];
153 -> 77;

154 [label="EVAL-BACKTRACK", fontsize=14, style = filled, fillcolor = lightblue];
73 -> 154 [arrowhead = none ];
154 -> 78;

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

156 [label="INSTANCE with matching:\nT327 -> T380\nT326 -> T379\nT351 -> .(T381, T382)\nT334 -> T383\nT352 -> T384", fontsize=14, style = filled, fillcolor = lightgrey];
77 -> 156 [arrowhead = none , style=dashed];
156 -> 70[style=dashed];

}

(2) Obligation:

Clauses:

reverse70([], T365, T366, T365, T366).
reverse70(.(T379, T380), T381, T382, T383, T384) :- reverse70(T380, T379, .(T381, T382), T383, T384).
palindrome1([]).
palindrome1(.(T19, [])).
palindrome1(.(T42, .(T42, []))).
palindrome1(.(T75, .(T74, .(T75, [])))).
palindrome1(.(T118, .(T117, .(T117, .(T118, []))))).
palindrome1(.(T171, .(T170, .(T169, .(T170, .(T171, [])))))).
palindrome1(.(T234, .(T233, .(T232, .(T232, .(T233, .(T234, []))))))).
palindrome1(.(T307, .(T306, .(T305, .(T304, .(T305, .(T306, .(T307, [])))))))).
palindrome1(.(T334, .(T333, .(T332, .(T331, .(T330, .(T329, .(T328, .(T326, T327))))))))) :- reverse70(T327, T326, .(T328, .(T329, .(T330, .(T331, .(T332, .(T333, .(T334, []))))))), T334, .(T333, .(T332, .(T331, .(T330, .(T329, .(T328, .(T326, T327)))))))).

Queries:

palindrome1(g).

(3) PrologToPiTRSProof (SOUND transformation)

We use the technique of [LOPSTR]. With regard to the inferred argument filtering the predicates were used in the following modes:
palindrome1_in: (b)
reverse70_in: (b,b,b,b,b)
Transforming Prolog into the following Term Rewriting System:
Pi-finite rewrite system:
The TRS R consists of the following rules:

palindrome1_in_g([]) → palindrome1_out_g([])
palindrome1_in_g(.(T19, [])) → palindrome1_out_g(.(T19, []))
palindrome1_in_g(.(T42, .(T42, []))) → palindrome1_out_g(.(T42, .(T42, [])))
palindrome1_in_g(.(T75, .(T74, .(T75, [])))) → palindrome1_out_g(.(T75, .(T74, .(T75, []))))
palindrome1_in_g(.(T118, .(T117, .(T117, .(T118, []))))) → palindrome1_out_g(.(T118, .(T117, .(T117, .(T118, [])))))
palindrome1_in_g(.(T171, .(T170, .(T169, .(T170, .(T171, [])))))) → palindrome1_out_g(.(T171, .(T170, .(T169, .(T170, .(T171, []))))))
palindrome1_in_g(.(T234, .(T233, .(T232, .(T232, .(T233, .(T234, []))))))) → palindrome1_out_g(.(T234, .(T233, .(T232, .(T232, .(T233, .(T234, [])))))))
palindrome1_in_g(.(T307, .(T306, .(T305, .(T304, .(T305, .(T306, .(T307, [])))))))) → palindrome1_out_g(.(T307, .(T306, .(T305, .(T304, .(T305, .(T306, .(T307, []))))))))
palindrome1_in_g(.(T334, .(T333, .(T332, .(T331, .(T330, .(T329, .(T328, .(T326, T327))))))))) → U2_g(T334, T333, T332, T331, T330, T329, T328, T326, T327, reverse70_in_ggggg(T327, T326, .(T328, .(T329, .(T330, .(T331, .(T332, .(T333, .(T334, []))))))), T334, .(T333, .(T332, .(T331, .(T330, .(T329, .(T328, .(T326, T327)))))))))
reverse70_in_ggggg([], T365, T366, T365, T366) → reverse70_out_ggggg([], T365, T366, T365, T366)
reverse70_in_ggggg(.(T379, T380), T381, T382, T383, T384) → U1_ggggg(T379, T380, T381, T382, T383, T384, reverse70_in_ggggg(T380, T379, .(T381, T382), T383, T384))
U1_ggggg(T379, T380, T381, T382, T383, T384, reverse70_out_ggggg(T380, T379, .(T381, T382), T383, T384)) → reverse70_out_ggggg(.(T379, T380), T381, T382, T383, T384)
U2_g(T334, T333, T332, T331, T330, T329, T328, T326, T327, reverse70_out_ggggg(T327, T326, .(T328, .(T329, .(T330, .(T331, .(T332, .(T333, .(T334, []))))))), T334, .(T333, .(T332, .(T331, .(T330, .(T329, .(T328, .(T326, T327))))))))) → palindrome1_out_g(.(T334, .(T333, .(T332, .(T331, .(T330, .(T329, .(T328, .(T326, T327)))))))))

Infinitary Constructor Rewriting Termination of PiTRS implies Termination of Prolog

(4) Obligation:

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

palindrome1_in_g([]) → palindrome1_out_g([])
palindrome1_in_g(.(T19, [])) → palindrome1_out_g(.(T19, []))
palindrome1_in_g(.(T42, .(T42, []))) → palindrome1_out_g(.(T42, .(T42, [])))
palindrome1_in_g(.(T75, .(T74, .(T75, [])))) → palindrome1_out_g(.(T75, .(T74, .(T75, []))))
palindrome1_in_g(.(T118, .(T117, .(T117, .(T118, []))))) → palindrome1_out_g(.(T118, .(T117, .(T117, .(T118, [])))))
palindrome1_in_g(.(T171, .(T170, .(T169, .(T170, .(T171, [])))))) → palindrome1_out_g(.(T171, .(T170, .(T169, .(T170, .(T171, []))))))
palindrome1_in_g(.(T234, .(T233, .(T232, .(T232, .(T233, .(T234, []))))))) → palindrome1_out_g(.(T234, .(T233, .(T232, .(T232, .(T233, .(T234, [])))))))
palindrome1_in_g(.(T307, .(T306, .(T305, .(T304, .(T305, .(T306, .(T307, [])))))))) → palindrome1_out_g(.(T307, .(T306, .(T305, .(T304, .(T305, .(T306, .(T307, []))))))))
palindrome1_in_g(.(T334, .(T333, .(T332, .(T331, .(T330, .(T329, .(T328, .(T326, T327))))))))) → U2_g(T334, T333, T332, T331, T330, T329, T328, T326, T327, reverse70_in_ggggg(T327, T326, .(T328, .(T329, .(T330, .(T331, .(T332, .(T333, .(T334, []))))))), T334, .(T333, .(T332, .(T331, .(T330, .(T329, .(T328, .(T326, T327)))))))))
reverse70_in_ggggg([], T365, T366, T365, T366) → reverse70_out_ggggg([], T365, T366, T365, T366)
reverse70_in_ggggg(.(T379, T380), T381, T382, T383, T384) → U1_ggggg(T379, T380, T381, T382, T383, T384, reverse70_in_ggggg(T380, T379, .(T381, T382), T383, T384))
U1_ggggg(T379, T380, T381, T382, T383, T384, reverse70_out_ggggg(T380, T379, .(T381, T382), T383, T384)) → reverse70_out_ggggg(.(T379, T380), T381, T382, T383, T384)
U2_g(T334, T333, T332, T331, T330, T329, T328, T326, T327, reverse70_out_ggggg(T327, T326, .(T328, .(T329, .(T330, .(T331, .(T332, .(T333, .(T334, []))))))), T334, .(T333, .(T332, .(T331, .(T330, .(T329, .(T328, .(T326, T327))))))))) → palindrome1_out_g(.(T334, .(T333, .(T332, .(T331, .(T330, .(T329, .(T328, .(T326, T327)))))))))

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

PALINDROME1_IN_G(.(T334, .(T333, .(T332, .(T331, .(T330, .(T329, .(T328, .(T326, T327))))))))) → U2_G(T334, T333, T332, T331, T330, T329, T328, T326, T327, reverse70_in_ggggg(T327, T326, .(T328, .(T329, .(T330, .(T331, .(T332, .(T333, .(T334, []))))))), T334, .(T333, .(T332, .(T331, .(T330, .(T329, .(T328, .(T326, T327)))))))))
PALINDROME1_IN_G(.(T334, .(T333, .(T332, .(T331, .(T330, .(T329, .(T328, .(T326, T327))))))))) → REVERSE70_IN_GGGGG(T327, T326, .(T328, .(T329, .(T330, .(T331, .(T332, .(T333, .(T334, []))))))), T334, .(T333, .(T332, .(T331, .(T330, .(T329, .(T328, .(T326, T327))))))))
REVERSE70_IN_GGGGG(.(T379, T380), T381, T382, T383, T384) → U1_GGGGG(T379, T380, T381, T382, T383, T384, reverse70_in_ggggg(T380, T379, .(T381, T382), T383, T384))
REVERSE70_IN_GGGGG(.(T379, T380), T381, T382, T383, T384) → REVERSE70_IN_GGGGG(T380, T379, .(T381, T382), T383, T384)

The TRS R consists of the following rules:

palindrome1_in_g([]) → palindrome1_out_g([])
palindrome1_in_g(.(T19, [])) → palindrome1_out_g(.(T19, []))
palindrome1_in_g(.(T42, .(T42, []))) → palindrome1_out_g(.(T42, .(T42, [])))
palindrome1_in_g(.(T75, .(T74, .(T75, [])))) → palindrome1_out_g(.(T75, .(T74, .(T75, []))))
palindrome1_in_g(.(T118, .(T117, .(T117, .(T118, []))))) → palindrome1_out_g(.(T118, .(T117, .(T117, .(T118, [])))))
palindrome1_in_g(.(T171, .(T170, .(T169, .(T170, .(T171, [])))))) → palindrome1_out_g(.(T171, .(T170, .(T169, .(T170, .(T171, []))))))
palindrome1_in_g(.(T234, .(T233, .(T232, .(T232, .(T233, .(T234, []))))))) → palindrome1_out_g(.(T234, .(T233, .(T232, .(T232, .(T233, .(T234, [])))))))
palindrome1_in_g(.(T307, .(T306, .(T305, .(T304, .(T305, .(T306, .(T307, [])))))))) → palindrome1_out_g(.(T307, .(T306, .(T305, .(T304, .(T305, .(T306, .(T307, []))))))))
palindrome1_in_g(.(T334, .(T333, .(T332, .(T331, .(T330, .(T329, .(T328, .(T326, T327))))))))) → U2_g(T334, T333, T332, T331, T330, T329, T328, T326, T327, reverse70_in_ggggg(T327, T326, .(T328, .(T329, .(T330, .(T331, .(T332, .(T333, .(T334, []))))))), T334, .(T333, .(T332, .(T331, .(T330, .(T329, .(T328, .(T326, T327)))))))))
reverse70_in_ggggg([], T365, T366, T365, T366) → reverse70_out_ggggg([], T365, T366, T365, T366)
reverse70_in_ggggg(.(T379, T380), T381, T382, T383, T384) → U1_ggggg(T379, T380, T381, T382, T383, T384, reverse70_in_ggggg(T380, T379, .(T381, T382), T383, T384))
U1_ggggg(T379, T380, T381, T382, T383, T384, reverse70_out_ggggg(T380, T379, .(T381, T382), T383, T384)) → reverse70_out_ggggg(.(T379, T380), T381, T382, T383, T384)
U2_g(T334, T333, T332, T331, T330, T329, T328, T326, T327, reverse70_out_ggggg(T327, T326, .(T328, .(T329, .(T330, .(T331, .(T332, .(T333, .(T334, []))))))), T334, .(T333, .(T332, .(T331, .(T330, .(T329, .(T328, .(T326, T327))))))))) → palindrome1_out_g(.(T334, .(T333, .(T332, .(T331, .(T330, .(T329, .(T328, .(T326, T327)))))))))

The argument filtering Pi contains the following mapping:
palindrome1_in_g(x1) = palindrome1_in_g(x1)
[] = []
palindrome1_out_g(x1) = palindrome1_out_g
.(x1, x2) = .(x1, x2)
U2_g(x1, x2, x3, x4, x5, x6, x7, x8, x9, x10) = U2_g(x10)
reverse70_in_ggggg(x1, x2, x3, x4, x5) = reverse70_in_ggggg(x1, x2, x3, x4, x5)
reverse70_out_ggggg(x1, x2, x3, x4, x5) = reverse70_out_ggggg
U1_ggggg(x1, x2, x3, x4, x5, x6, x7) = U1_ggggg(x7)
PALINDROME1_IN_G(x1) = PALINDROME1_IN_G(x1)
U2_G(x1, x2, x3, x4, x5, x6, x7, x8, x9, x10) = U2_G(x10)
REVERSE70_IN_GGGGG(x1, x2, x3, x4, x5) = REVERSE70_IN_GGGGG(x1, x2, x3, x4, x5)
U1_GGGGG(x1, x2, x3, x4, x5, x6, x7) = U1_GGGGG(x7)

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

(6) Obligation:

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

PALINDROME1_IN_G(.(T334, .(T333, .(T332, .(T331, .(T330, .(T329, .(T328, .(T326, T327))))))))) → U2_G(T334, T333, T332, T331, T330, T329, T328, T326, T327, reverse70_in_ggggg(T327, T326, .(T328, .(T329, .(T330, .(T331, .(T332, .(T333, .(T334, []))))))), T334, .(T333, .(T332, .(T331, .(T330, .(T329, .(T328, .(T326, T327)))))))))
PALINDROME1_IN_G(.(T334, .(T333, .(T332, .(T331, .(T330, .(T329, .(T328, .(T326, T327))))))))) → REVERSE70_IN_GGGGG(T327, T326, .(T328, .(T329, .(T330, .(T331, .(T332, .(T333, .(T334, []))))))), T334, .(T333, .(T332, .(T331, .(T330, .(T329, .(T328, .(T326, T327))))))))
REVERSE70_IN_GGGGG(.(T379, T380), T381, T382, T383, T384) → U1_GGGGG(T379, T380, T381, T382, T383, T384, reverse70_in_ggggg(T380, T379, .(T381, T382), T383, T384))
REVERSE70_IN_GGGGG(.(T379, T380), T381, T382, T383, T384) → REVERSE70_IN_GGGGG(T380, T379, .(T381, T382), T383, T384)

The TRS R consists of the following rules:

palindrome1_in_g([]) → palindrome1_out_g([])
palindrome1_in_g(.(T19, [])) → palindrome1_out_g(.(T19, []))
palindrome1_in_g(.(T42, .(T42, []))) → palindrome1_out_g(.(T42, .(T42, [])))
palindrome1_in_g(.(T75, .(T74, .(T75, [])))) → palindrome1_out_g(.(T75, .(T74, .(T75, []))))
palindrome1_in_g(.(T118, .(T117, .(T117, .(T118, []))))) → palindrome1_out_g(.(T118, .(T117, .(T117, .(T118, [])))))
palindrome1_in_g(.(T171, .(T170, .(T169, .(T170, .(T171, [])))))) → palindrome1_out_g(.(T171, .(T170, .(T169, .(T170, .(T171, []))))))
palindrome1_in_g(.(T234, .(T233, .(T232, .(T232, .(T233, .(T234, []))))))) → palindrome1_out_g(.(T234, .(T233, .(T232, .(T232, .(T233, .(T234, [])))))))
palindrome1_in_g(.(T307, .(T306, .(T305, .(T304, .(T305, .(T306, .(T307, [])))))))) → palindrome1_out_g(.(T307, .(T306, .(T305, .(T304, .(T305, .(T306, .(T307, []))))))))
palindrome1_in_g(.(T334, .(T333, .(T332, .(T331, .(T330, .(T329, .(T328, .(T326, T327))))))))) → U2_g(T334, T333, T332, T331, T330, T329, T328, T326, T327, reverse70_in_ggggg(T327, T326, .(T328, .(T329, .(T330, .(T331, .(T332, .(T333, .(T334, []))))))), T334, .(T333, .(T332, .(T331, .(T330, .(T329, .(T328, .(T326, T327)))))))))
reverse70_in_ggggg([], T365, T366, T365, T366) → reverse70_out_ggggg([], T365, T366, T365, T366)
reverse70_in_ggggg(.(T379, T380), T381, T382, T383, T384) → U1_ggggg(T379, T380, T381, T382, T383, T384, reverse70_in_ggggg(T380, T379, .(T381, T382), T383, T384))
U1_ggggg(T379, T380, T381, T382, T383, T384, reverse70_out_ggggg(T380, T379, .(T381, T382), T383, T384)) → reverse70_out_ggggg(.(T379, T380), T381, T382, T383, T384)
U2_g(T334, T333, T332, T331, T330, T329, T328, T326, T327, reverse70_out_ggggg(T327, T326, .(T328, .(T329, .(T330, .(T331, .(T332, .(T333, .(T334, []))))))), T334, .(T333, .(T332, .(T331, .(T330, .(T329, .(T328, .(T326, T327))))))))) → palindrome1_out_g(.(T334, .(T333, .(T332, .(T331, .(T330, .(T329, .(T328, .(T326, T327)))))))))

(7) DependencyGraphProof (EQUIVALENT transformation)

The approximation of the Dependency Graph [LOPSTR] contains 1 SCC with 3 less nodes.

(8) Obligation:

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

REVERSE70_IN_GGGGG(.(T379, T380), T381, T382, T383, T384) → REVERSE70_IN_GGGGG(T380, T379, .(T381, T382), T383, T384)

The TRS R consists of the following rules:

palindrome1_in_g([]) → palindrome1_out_g([])
palindrome1_in_g(.(T19, [])) → palindrome1_out_g(.(T19, []))
palindrome1_in_g(.(T42, .(T42, []))) → palindrome1_out_g(.(T42, .(T42, [])))
palindrome1_in_g(.(T75, .(T74, .(T75, [])))) → palindrome1_out_g(.(T75, .(T74, .(T75, []))))
palindrome1_in_g(.(T118, .(T117, .(T117, .(T118, []))))) → palindrome1_out_g(.(T118, .(T117, .(T117, .(T118, [])))))
palindrome1_in_g(.(T171, .(T170, .(T169, .(T170, .(T171, [])))))) → palindrome1_out_g(.(T171, .(T170, .(T169, .(T170, .(T171, []))))))
palindrome1_in_g(.(T234, .(T233, .(T232, .(T232, .(T233, .(T234, []))))))) → palindrome1_out_g(.(T234, .(T233, .(T232, .(T232, .(T233, .(T234, [])))))))
palindrome1_in_g(.(T307, .(T306, .(T305, .(T304, .(T305, .(T306, .(T307, [])))))))) → palindrome1_out_g(.(T307, .(T306, .(T305, .(T304, .(T305, .(T306, .(T307, []))))))))
palindrome1_in_g(.(T334, .(T333, .(T332, .(T331, .(T330, .(T329, .(T328, .(T326, T327))))))))) → U2_g(T334, T333, T332, T331, T330, T329, T328, T326, T327, reverse70_in_ggggg(T327, T326, .(T328, .(T329, .(T330, .(T331, .(T332, .(T333, .(T334, []))))))), T334, .(T333, .(T332, .(T331, .(T330, .(T329, .(T328, .(T326, T327)))))))))
reverse70_in_ggggg([], T365, T366, T365, T366) → reverse70_out_ggggg([], T365, T366, T365, T366)
reverse70_in_ggggg(.(T379, T380), T381, T382, T383, T384) → U1_ggggg(T379, T380, T381, T382, T383, T384, reverse70_in_ggggg(T380, T379, .(T381, T382), T383, T384))
U1_ggggg(T379, T380, T381, T382, T383, T384, reverse70_out_ggggg(T380, T379, .(T381, T382), T383, T384)) → reverse70_out_ggggg(.(T379, T380), T381, T382, T383, T384)
U2_g(T334, T333, T332, T331, T330, T329, T328, T326, T327, reverse70_out_ggggg(T327, T326, .(T328, .(T329, .(T330, .(T331, .(T332, .(T333, .(T334, []))))))), T334, .(T333, .(T332, .(T331, .(T330, .(T329, .(T328, .(T326, T327))))))))) → palindrome1_out_g(.(T334, .(T333, .(T332, .(T331, .(T330, .(T329, .(T328, .(T326, T327)))))))))

The argument filtering Pi contains the following mapping:
palindrome1_in_g(x1) = palindrome1_in_g(x1)
[] = []
palindrome1_out_g(x1) = palindrome1_out_g
.(x1, x2) = .(x1, x2)
U2_g(x1, x2, x3, x4, x5, x6, x7, x8, x9, x10) = U2_g(x10)
reverse70_in_ggggg(x1, x2, x3, x4, x5) = reverse70_in_ggggg(x1, x2, x3, x4, x5)
reverse70_out_ggggg(x1, x2, x3, x4, x5) = reverse70_out_ggggg
U1_ggggg(x1, x2, x3, x4, x5, x6, x7) = U1_ggggg(x7)
REVERSE70_IN_GGGGG(x1, x2, x3, x4, x5) = REVERSE70_IN_GGGGG(x1, x2, x3, x4, x5)

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

(9) UsableRulesProof (EQUIVALENT transformation)

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

(10) Obligation:

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

REVERSE70_IN_GGGGG(.(T379, T380), T381, T382, T383, T384) → REVERSE70_IN_GGGGG(T380, T379, .(T381, T382), T383, T384)

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

(11) PiDPToQDPProof (EQUIVALENT transformation)

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

(12) Obligation:

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

REVERSE70_IN_GGGGG(.(T379, T380), T381, T382, T383, T384) → REVERSE70_IN_GGGGG(T380, T379, .(T381, T382), T383, T384)

R is empty.
Q is empty.
We have to consider all (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:

REVERSE70_IN_GGGGG(.(T379, T380), T381, T382, T383, T384) → REVERSE70_IN_GGGGG(T380, T379, .(T381, T382), T383, T384)
The graph contains the following edges 1 > 1, 1 > 2, 4 >= 4, 5 >= 5

(0) Obligation:

(1) PrologToPrologProblemTransformerProof (SOUND transformation)

(2) Obligation:

(3) PrologToPiTRSProof (SOUND transformation)

(4) Obligation:

(5) DependencyPairsProof (EQUIVALENT transformation)

(6) Obligation:

(7) DependencyGraphProof (EQUIVALENT transformation)

(8) Obligation:

(9) UsableRulesProof (EQUIVALENT transformation)

(10) Obligation:

(11) PiDPToQDPProof (EQUIVALENT transformation)

(12) Obligation:

(13) QDPSizeChangeProof (EQUIVALENT transformation)

(14) YES