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

(0) Obligation:

Clauses:

perm([], []).
perm(L, .(H, T)) :- ','(append2(V, .(H, U), L), ','(append1(V, U, W), perm(W, T))).
append1([], L, L).
append1(.(H, L1), L2, .(H, L3)) :- append1(L1, L2, L3).
append2([], L, L).
append2(.(H, L1), L2, .(H, L3)) :- append2(L1, L2, L3).

Query: perm(g,a)

(1) PrologToTRSTransformerProof (SOUND transformation)

Transformed Prolog program to TRS.

digraph dp_graph {
node [outthreshold=100, inthreshold=100];
1 [label="1: perm(T1, T2)\n\nT1 is ground", fontsize=16, style=filled, fillcolor=lightyellow, color=red];
6 [label="6: perm(T1, T2), SCOPE: 1, CLAUSE: 0 | perm(T1, T2), SCOPE: 1, CLAUSE: 1\n\nT1 is ground", fontsize=16, style=filled, fillcolor=lightyellow];
7 [label="7: perm(T1, T2), SCOPE: 1, CLAUSE: 0\n\nT1 is ground", fontsize=16, style=filled, fillcolor=lightyellow];
8 [label="8: perm(T1, T2), SCOPE: 1, CLAUSE: 1\n\nT1 is ground", fontsize=16, style=filled, fillcolor=lightyellow];
9 [label="9: true\n\n", fontsize=16, style=filled, fillcolor=lightyellow];
12 [label="12: \n\n", fontsize=16, style=filled, fillcolor=lightyellow];
15 [label="15: \n\n", fontsize=16, style=filled, fillcolor=lightyellow];
23 [label="23: ','(append2(X13, .(T12, X14), T9), ','(append1(X13, X14, X15), perm(X15, T13)))\n\nT9 is ground\nX13 is free\nX14 is free\nX15 is free", fontsize=16, style=filled, fillcolor=lightyellow];
26 [label="26: \n\n", fontsize=16, style=filled, fillcolor=lightyellow];
48 [label="48: append2(X13, .(T12, X14), T9)\n\nT9 is ground\nX13 is free\nX14 is free", fontsize=16, style=filled, fillcolor=lightyellow];
49 [label="49: ','(append1(T18, T19, X15), perm(X15, T20))\n\nT18 is ground\nT19 is ground\nX15 is free", fontsize=16, style=filled, fillcolor=lightyellow];
56 [label="56: append2(X13, .(T12, X14), T9), SCOPE: 2, CLAUSE: 4 | append2(X13, .(T12, X14), T9), SCOPE: 2, CLAUSE: 5\n\nT9 is ground\nX13 is free\nX14 is free", fontsize=16, style=filled, fillcolor=lightyellow];
61 [label="61: append2(X13, .(T12, X14), T9), SCOPE: 2, CLAUSE: 4\n\nT9 is ground\nX13 is free\nX14 is free", fontsize=16, style=filled, fillcolor=lightyellow];
62 [label="62: append2(X13, .(T12, X14), T9), SCOPE: 2, CLAUSE: 5\n\nT9 is ground\nX13 is free\nX14 is free", 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];
74 [label="74: append2(X53, .(T44, X54), T43)\n\nT43 is ground\nX53 is free\nX54 is free", fontsize=16, style=filled, fillcolor=lightyellow];
77 [label="77: \n\n", fontsize=16, style=filled, fillcolor=lightyellow];
82 [label="82: append1(T18, T19, X15)\n\nT18 is ground\nT19 is ground\nX15 is free", fontsize=16, style=filled, fillcolor=lightyellow];
83 [label="83: perm(T51, T20)\n\nT51 is ground", fontsize=16, style=filled, fillcolor=lightyellow];
93 [label="93: append1(T18, T19, X15), SCOPE: 3, CLAUSE: 2 | append1(T18, T19, X15), SCOPE: 3, CLAUSE: 3\n\nT18 is ground\nT19 is ground\nX15 is free", fontsize=16, style=filled, fillcolor=lightyellow];
95 [label="95: append1(T18, T19, X15), SCOPE: 3, CLAUSE: 2\n\nT18 is ground\nT19 is ground\nX15 is free", fontsize=16, style=filled, fillcolor=lightyellow];
96 [label="96: append1(T18, T19, X15), SCOPE: 3, CLAUSE: 3\n\nT18 is ground\nT19 is ground\nX15 is free", fontsize=16, style=filled, fillcolor=lightyellow];
99 [label="99: true\n\n", fontsize=16, style=filled, fillcolor=lightyellow];
100 [label="100: \n\n", fontsize=16, style=filled, fillcolor=lightyellow];
101 [label="101: \n\n", fontsize=16, style=filled, fillcolor=lightyellow];
104 [label="104: append1(T66, T67, X82)\n\nT66 is ground\nT67 is ground\nX82 is free", fontsize=16, style=filled, fillcolor=lightyellow];
105 [label="105: \n\n", fontsize=16, style=filled, fillcolor=lightyellow];
106 [label="CASE", fontsize=14, style = filled, fillcolor = lightcyan];
1 -> 106 [arrowhead = none ];
106 -> 6;

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

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

109 [label="EVAL with clause\nperm([], []).\nand substitutionT1 -> [],\nT2 -> []", fontsize=14, style = filled, fillcolor = lightblue];
7 -> 109 [arrowhead = none ];
109 -> 9;

110 [label="EVAL-BACKTRACK", fontsize=14, style = filled, fillcolor = lightgreen];
7 -> 110 [arrowhead = none ];
110 -> 12;

111 [label="EVAL with clause\nperm(X10, .(X11, X12)) :- ','(append2(X13, .(X11, X14), X10), ','(append1(X13, X14, X15), perm(X15, X12))).\nand substitutionT1 -> T9,\nX10 -> T9,\nX11 -> T12,\nX12 -> T13,\nT2 -> .(T12, T13),\nT10 -> T12,\nT11 -> T13", fontsize=14, style = filled, fillcolor = lightblue];
8 -> 111 [arrowhead = none ];
111 -> 23;

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

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

114 [label="SPLIT 1", fontsize=14, style = filled, fillcolor = violet];
23 -> 114 [arrowhead = none ];
114 -> 48;

115 [label="SPLIT 2\nnew knowledge:\nT18 is ground\nT12 is ground\nT19 is ground\nT9 is ground\nreplacements:X13 -> T18,\nX14 -> T19,\nT13 -> T20", fontsize=14, style = filled, fillcolor = violet];
23 -> 115 [arrowhead = none ];
115 -> 49;

116 [label="CASE", fontsize=14, style = filled, fillcolor = lightcyan];
48 -> 116 [arrowhead = none ];
116 -> 56;

117 [label="SPLIT 1", fontsize=14, style = filled, fillcolor = violet];
49 -> 117 [arrowhead = none ];
117 -> 82;

118 [label="SPLIT 2\nnew knowledge:\nT18 is ground\nT19 is ground\nT51 is ground\nreplacements:X15 -> T51", fontsize=14, style = filled, fillcolor = violet];
49 -> 118 [arrowhead = none ];
118 -> 83;

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

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

121 [label="EVAL with clause\nappend2([], X32, X32).\nand substitutionX13 -> [],\nT12 -> T33,\nX14 -> T34,\nX32 -> .(T33, T34),\nX33 -> T34,\nT9 -> .(T33, T34)", fontsize=14, style = filled, fillcolor = lightblue];
61 -> 121 [arrowhead = none ];
121 -> 65;

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

123 [label="EVAL with clause\nappend2(.(X48, X49), X50, .(X48, X51)) :- append2(X49, X50, X51).\nand substitutionX48 -> T42,\nX49 -> X53,\nX13 -> .(T42, X53),\nT12 -> T44,\nX14 -> X54,\nX50 -> .(T44, X54),\nX52 -> T42,\nX51 -> T43,\nT9 -> .(T42, T43),\nT41 -> T44", fontsize=14, style = filled, fillcolor = lightblue];
62 -> 123 [arrowhead = none ];
123 -> 74;

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

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

126 [label="INSTANCE with matching:\nX13 -> X53\nT12 -> T44\nX14 -> X54\nT9 -> T43", fontsize=14, style = filled, fillcolor = lightgrey];
74 -> 126 [arrowhead = none , style=dashed];
126 -> 48[style=dashed];

127 [label="CASE", fontsize=14, style = filled, fillcolor = lightcyan];
82 -> 127 [arrowhead = none ];
127 -> 93;

128 [label="INSTANCE with matching:\nT1 -> T51\nT2 -> T20", fontsize=14, style = filled, fillcolor = lightgrey];
83 -> 128 [arrowhead = none , style=dashed];
128 -> 1[style=dashed];

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

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

131 [label="EVAL with clause\nappend1([], X67, X67).\nand substitutionT18 -> [],\nT19 -> T58,\nX67 -> T58,\nX15 -> T58", fontsize=14, style = filled, fillcolor = lightblue];
95 -> 131 [arrowhead = none ];
131 -> 99;

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

133 [label="EVAL with clause\nappend1(.(X78, X79), X80, .(X78, X81)) :- append1(X79, X80, X81).\nand substitutionX78 -> T65,\nX79 -> T66,\nT18 -> .(T65, T66),\nT19 -> T67,\nX80 -> T67,\nX81 -> X82,\nX15 -> .(T65, X82)", fontsize=14, style = filled, fillcolor = lightblue];
96 -> 133 [arrowhead = none ];
133 -> 104;

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

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

136 [label="INSTANCE with matching:\nT18 -> T66\nT19 -> T67\nX15 -> X82", fontsize=14, style = filled, fillcolor = lightgrey];
104 -> 136 [arrowhead = none , style=dashed];
136 -> 82[style=dashed];

}

(2) Obligation:

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

f1_in([]) → f1_out1([])
f1_in(T9) → U1(f23_in(T9), T9)
U1(f23_out1(X13, T12, X14, X15, T13), T9) → f1_out1(.(T12, T13))
f48_in(.(T33, T34)) → f48_out1([], T33, T34)
f48_in(.(T42, T43)) → U2(f48_in(T43), .(T42, T43))
U2(f48_out1(X53, T44, X54), .(T42, T43)) → f48_out1(.(T42, X53), T44, X54)
f82_in([], T58) → f82_out1(T58)
f82_in(.(T65, T66), T67) → U3(f82_in(T66, T67), .(T65, T66), T67)
U3(f82_out1(X82), .(T65, T66), T67) → f82_out1(.(T65, X82))
f23_in(T9) → U4(f48_in(T9), T9)
U4(f48_out1(T18, T12, T19), T9) → U5(f49_in(T18, T19), T9, T18, T12, T19)
U5(f49_out1(X15, T20), T9, T18, T12, T19) → f23_out1(T18, T12, T19, X15, T20)
f49_in(T18, T19) → U6(f82_in(T18, T19), T18, T19)
U6(f82_out1(T51), T18, T19) → U7(f1_in(T51), T18, T19, T51)
U7(f1_out1(T20), T18, T19, T51) → f49_out1(T51, T20)

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(T9) → U1¹(f23_in(T9), T9)
F1_IN(T9) → F23_IN(T9)
F48_IN(.(T42, T43)) → U2¹(f48_in(T43), .(T42, T43))
F48_IN(.(T42, T43)) → F48_IN(T43)
F82_IN(.(T65, T66), T67) → U3¹(f82_in(T66, T67), .(T65, T66), T67)
F82_IN(.(T65, T66), T67) → F82_IN(T66, T67)
F23_IN(T9) → U4¹(f48_in(T9), T9)
F23_IN(T9) → F48_IN(T9)
U4¹(f48_out1(T18, T12, T19), T9) → U5¹(f49_in(T18, T19), T9, T18, T12, T19)
U4¹(f48_out1(T18, T12, T19), T9) → F49_IN(T18, T19)
F49_IN(T18, T19) → U6¹(f82_in(T18, T19), T18, T19)
F49_IN(T18, T19) → F82_IN(T18, T19)
U6¹(f82_out1(T51), T18, T19) → U7¹(f1_in(T51), T18, T19, T51)
U6¹(f82_out1(T51), T18, T19) → F1_IN(T51)

The TRS R consists of the following rules:

f1_in([]) → f1_out1([])
f1_in(T9) → U1(f23_in(T9), T9)
U1(f23_out1(X13, T12, X14, X15, T13), T9) → f1_out1(.(T12, T13))
f48_in(.(T33, T34)) → f48_out1([], T33, T34)
f48_in(.(T42, T43)) → U2(f48_in(T43), .(T42, T43))
U2(f48_out1(X53, T44, X54), .(T42, T43)) → f48_out1(.(T42, X53), T44, X54)
f82_in([], T58) → f82_out1(T58)
f82_in(.(T65, T66), T67) → U3(f82_in(T66, T67), .(T65, T66), T67)
U3(f82_out1(X82), .(T65, T66), T67) → f82_out1(.(T65, X82))
f23_in(T9) → U4(f48_in(T9), T9)
U4(f48_out1(T18, T12, T19), T9) → U5(f49_in(T18, T19), T9, T18, T12, T19)
U5(f49_out1(X15, T20), T9, T18, T12, T19) → f23_out1(T18, T12, T19, X15, T20)
f49_in(T18, T19) → U6(f82_in(T18, T19), T18, T19)
U6(f82_out1(T51), T18, T19) → U7(f1_in(T51), T18, T19, T51)
U7(f1_out1(T20), T18, T19, T51) → f49_out1(T51, T20)

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 3 SCCs with 7 less nodes.

(6) Complex Obligation (AND)

(7) Obligation:

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

F82_IN(.(T65, T66), T67) → F82_IN(T66, T67)

The TRS R consists of the following rules:

f1_in([]) → f1_out1([])
f1_in(T9) → U1(f23_in(T9), T9)
U1(f23_out1(X13, T12, X14, X15, T13), T9) → f1_out1(.(T12, T13))
f48_in(.(T33, T34)) → f48_out1([], T33, T34)
f48_in(.(T42, T43)) → U2(f48_in(T43), .(T42, T43))
U2(f48_out1(X53, T44, X54), .(T42, T43)) → f48_out1(.(T42, X53), T44, X54)
f82_in([], T58) → f82_out1(T58)
f82_in(.(T65, T66), T67) → U3(f82_in(T66, T67), .(T65, T66), T67)
U3(f82_out1(X82), .(T65, T66), T67) → f82_out1(.(T65, X82))
f23_in(T9) → U4(f48_in(T9), T9)
U4(f48_out1(T18, T12, T19), T9) → U5(f49_in(T18, T19), T9, T18, T12, T19)
U5(f49_out1(X15, T20), T9, T18, T12, T19) → f23_out1(T18, T12, T19, X15, T20)
f49_in(T18, T19) → U6(f82_in(T18, T19), T18, T19)
U6(f82_out1(T51), T18, T19) → U7(f1_in(T51), T18, T19, T51)
U7(f1_out1(T20), T18, T19, T51) → f49_out1(T51, T20)

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

(8) 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.

(9) Obligation:

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

F82_IN(.(T65, T66), T67) → F82_IN(T66, T67)

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

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

• F82_IN(.(T65, T66), T67) → F82_IN(T66, T67)
  The graph contains the following edges 1 > 1, 2 >= 2

(11) YES

(12) Obligation:

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

F48_IN(.(T42, T43)) → F48_IN(T43)

The TRS R consists of the following rules:

f1_in([]) → f1_out1([])
f1_in(T9) → U1(f23_in(T9), T9)
U1(f23_out1(X13, T12, X14, X15, T13), T9) → f1_out1(.(T12, T13))
f48_in(.(T33, T34)) → f48_out1([], T33, T34)
f48_in(.(T42, T43)) → U2(f48_in(T43), .(T42, T43))
U2(f48_out1(X53, T44, X54), .(T42, T43)) → f48_out1(.(T42, X53), T44, X54)
f82_in([], T58) → f82_out1(T58)
f82_in(.(T65, T66), T67) → U3(f82_in(T66, T67), .(T65, T66), T67)
U3(f82_out1(X82), .(T65, T66), T67) → f82_out1(.(T65, X82))
f23_in(T9) → U4(f48_in(T9), T9)
U4(f48_out1(T18, T12, T19), T9) → U5(f49_in(T18, T19), T9, T18, T12, T19)
U5(f49_out1(X15, T20), T9, T18, T12, T19) → f23_out1(T18, T12, T19, X15, T20)
f49_in(T18, T19) → U6(f82_in(T18, T19), T18, T19)
U6(f82_out1(T51), T18, T19) → U7(f1_in(T51), T18, T19, T51)
U7(f1_out1(T20), T18, T19, T51) → f49_out1(T51, T20)

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

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

(14) Obligation:

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

F48_IN(.(T42, T43)) → F48_IN(T43)

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

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

• F48_IN(.(T42, T43)) → F48_IN(T43)
  The graph contains the following edges 1 > 1

(16) YES

(17) Obligation:

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

F1_IN(T9) → F23_IN(T9)
F23_IN(T9) → U4¹(f48_in(T9), T9)
U4¹(f48_out1(T18, T12, T19), T9) → F49_IN(T18, T19)
F49_IN(T18, T19) → U6¹(f82_in(T18, T19), T18, T19)
U6¹(f82_out1(T51), T18, T19) → F1_IN(T51)

The TRS R consists of the following rules:

f1_in([]) → f1_out1([])
f1_in(T9) → U1(f23_in(T9), T9)
U1(f23_out1(X13, T12, X14, X15, T13), T9) → f1_out1(.(T12, T13))
f48_in(.(T33, T34)) → f48_out1([], T33, T34)
f48_in(.(T42, T43)) → U2(f48_in(T43), .(T42, T43))
U2(f48_out1(X53, T44, X54), .(T42, T43)) → f48_out1(.(T42, X53), T44, X54)
f82_in([], T58) → f82_out1(T58)
f82_in(.(T65, T66), T67) → U3(f82_in(T66, T67), .(T65, T66), T67)
U3(f82_out1(X82), .(T65, T66), T67) → f82_out1(.(T65, X82))
f23_in(T9) → U4(f48_in(T9), T9)
U4(f48_out1(T18, T12, T19), T9) → U5(f49_in(T18, T19), T9, T18, T12, T19)
U5(f49_out1(X15, T20), T9, T18, T12, T19) → f23_out1(T18, T12, T19, X15, T20)
f49_in(T18, T19) → U6(f82_in(T18, T19), T18, T19)
U6(f82_out1(T51), T18, T19) → U7(f1_in(T51), T18, T19, T51)
U7(f1_out1(T20), T18, T19, T51) → f49_out1(T51, T20)

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

(18) QDPOrderProof (EQUIVALENT transformation)

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

The following pairs can be oriented strictly and are deleted.

F23_IN(T9) → U4¹(f48_in(T9), T9)

The remaining pairs can at least be oriented weakly.
Used ordering: Polynomial interpretation [POLO]:

POL(.(x₁, x₂)) = 1 + x₂   
POL(F1_IN(x₁)) = 1 + x₁   
POL(F23_IN(x₁)) = 1 + x₁   
POL(F49_IN(x₁, x₂)) = x₁ + x₂   
POL(U2(x₁, x₂)) = 1 + x₁   
POL(U3(x₁, x₂, x₃)) = 1 + x₁   
POL(U4¹(x₁, x₂)) = x₁   
POL(U6¹(x₁, x₂, x₃)) = x₁   
POL([]) = 1   
POL(f48_in(x₁)) = x₁   
POL(f48_out1(x₁, x₂, x₃)) = x₁ + x₃   
POL(f82_in(x₁, x₂)) = x₁ + x₂   
POL(f82_out1(x₁)) = 1 + x₁   

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

f48_in(.(T33, T34)) → f48_out1([], T33, T34)
f48_in(.(T42, T43)) → U2(f48_in(T43), .(T42, T43))
f82_in([], T58) → f82_out1(T58)
f82_in(.(T65, T66), T67) → U3(f82_in(T66, T67), .(T65, T66), T67)
U2(f48_out1(X53, T44, X54), .(T42, T43)) → f48_out1(.(T42, X53), T44, X54)
U3(f82_out1(X82), .(T65, T66), T67) → f82_out1(.(T65, X82))

(19) Obligation:

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

F1_IN(T9) → F23_IN(T9)
U4¹(f48_out1(T18, T12, T19), T9) → F49_IN(T18, T19)
F49_IN(T18, T19) → U6¹(f82_in(T18, T19), T18, T19)
U6¹(f82_out1(T51), T18, T19) → F1_IN(T51)

The TRS R consists of the following rules:

f1_in([]) → f1_out1([])
f1_in(T9) → U1(f23_in(T9), T9)
U1(f23_out1(X13, T12, X14, X15, T13), T9) → f1_out1(.(T12, T13))
f48_in(.(T33, T34)) → f48_out1([], T33, T34)
f48_in(.(T42, T43)) → U2(f48_in(T43), .(T42, T43))
U2(f48_out1(X53, T44, X54), .(T42, T43)) → f48_out1(.(T42, X53), T44, X54)
f82_in([], T58) → f82_out1(T58)
f82_in(.(T65, T66), T67) → U3(f82_in(T66, T67), .(T65, T66), T67)
U3(f82_out1(X82), .(T65, T66), T67) → f82_out1(.(T65, X82))
f23_in(T9) → U4(f48_in(T9), T9)
U4(f48_out1(T18, T12, T19), T9) → U5(f49_in(T18, T19), T9, T18, T12, T19)
U5(f49_out1(X15, T20), T9, T18, T12, T19) → f23_out1(T18, T12, T19, X15, T20)
f49_in(T18, T19) → U6(f82_in(T18, T19), T18, T19)
U6(f82_out1(T51), T18, T19) → U7(f1_in(T51), T18, T19, T51)
U7(f1_out1(T20), T18, T19, T51) → f49_out1(T51, T20)

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

(20) DependencyGraphProof (EQUIVALENT transformation)

The approximation of the Dependency Graph [LPAR04,FROCOS05,EDGSTAR] contains 0 SCCs with 4 less nodes.

(21) TRUE