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

(0) Obligation:

Clauses:

ap1(nil, X, X).
ap1(cons(H, X), Y, cons(H, Z)) :- ap1(X, Y, Z).
ap2(nil, X, X).
ap2(cons(H, X), Y, cons(H, Z)) :- ap2(X, Y, Z).
perm(nil, nil).
perm(Xs, cons(X, Ys)) :- ','(ap1(X1s, cons(X, X2s), Xs), ','(ap2(X1s, X2s, Zs), perm(Zs, Ys))).

Query: perm(g,a)

(1) PrologToTRSTransformerProof (SOUND transformation)

Transformed Prolog program to TRS.

digraph dp_graph {
node [outthreshold=100, inthreshold=100];
3 [label="3: perm(T1, T2)\n\nT1 is ground", fontsize=16, style=filled, fillcolor=lightyellow, color=red];
4 [label="4: perm(T1, T2), SCOPE: 1, CLAUSE: 4 | perm(T1, T2), SCOPE: 1, CLAUSE: 5\n\nT1 is ground", fontsize=16, style=filled, fillcolor=lightyellow];
7 [label="7: perm(T1, T2), SCOPE: 1, CLAUSE: 4\n\nT1 is ground", fontsize=16, style=filled, fillcolor=lightyellow];
8 [label="8: perm(T1, T2), SCOPE: 1, CLAUSE: 5\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];
24 [label="24: ','(ap1(X13, cons(T12, X14), T9), ','(ap2(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];
35 [label="35: ap1(X13, cons(T12, X14), T9)\n\nT9 is ground\nX13 is free\nX14 is free", fontsize=16, style=filled, fillcolor=lightyellow];
36 [label="36: ','(ap2(T18, T19, X15), perm(X15, T20))\n\nT18 is ground\nT19 is ground\nX15 is free", fontsize=16, style=filled, fillcolor=lightyellow];
41 [label="41: ap1(X13, cons(T12, X14), T9), SCOPE: 2, CLAUSE: 0 | ap1(X13, cons(T12, X14), T9), SCOPE: 2, CLAUSE: 1\n\nT9 is ground\nX13 is free\nX14 is free", fontsize=16, style=filled, fillcolor=lightyellow];
43 [label="43: ap1(X13, cons(T12, X14), T9), SCOPE: 2, CLAUSE: 0\n\nT9 is ground\nX13 is free\nX14 is free", fontsize=16, style=filled, fillcolor=lightyellow];
44 [label="44: ap1(X13, cons(T12, X14), T9), SCOPE: 2, CLAUSE: 1\n\nT9 is ground\nX13 is free\nX14 is free", fontsize=16, style=filled, fillcolor=lightyellow];
50 [label="50: true\n\n", fontsize=16, style=filled, fillcolor=lightyellow];
53 [label="53: \n\n", fontsize=16, style=filled, fillcolor=lightyellow];
54 [label="54: \n\n", fontsize=16, style=filled, fillcolor=lightyellow];
63 [label="63: ap1(X53, cons(T44, X54), T43)\n\nT43 is ground\nX53 is free\nX54 is free", fontsize=16, style=filled, fillcolor=lightyellow];
64 [label="64: \n\n", fontsize=16, style=filled, fillcolor=lightyellow];
70 [label="70: ap2(T18, T19, X15)\n\nT18 is ground\nT19 is ground\nX15 is free", fontsize=16, style=filled, fillcolor=lightyellow];
71 [label="71: perm(T51, T20)\n\nT51 is ground", fontsize=16, style=filled, fillcolor=lightyellow];
73 [label="73: ap2(T18, T19, X15), SCOPE: 3, CLAUSE: 2 | ap2(T18, T19, X15), SCOPE: 3, CLAUSE: 3\n\nT18 is ground\nT19 is ground\nX15 is free", fontsize=16, style=filled, fillcolor=lightyellow];
75 [label="75: ap2(T18, T19, X15), SCOPE: 3, CLAUSE: 2\n\nT18 is ground\nT19 is ground\nX15 is free", fontsize=16, style=filled, fillcolor=lightyellow];
76 [label="76: ap2(T18, T19, X15), SCOPE: 3, CLAUSE: 3\n\nT18 is ground\nT19 is ground\nX15 is free", fontsize=16, style=filled, fillcolor=lightyellow];
77 [label="77: true\n\n", fontsize=16, style=filled, fillcolor=lightyellow];
78 [label="78: \n\n", fontsize=16, style=filled, fillcolor=lightyellow];
79 [label="79: \n\n", fontsize=16, style=filled, fillcolor=lightyellow];
87 [label="87: ap2(T66, T67, X82)\n\nT66 is ground\nT67 is ground\nX82 is free", fontsize=16, style=filled, fillcolor=lightyellow];
90 [label="90: \n\n", fontsize=16, style=filled, fillcolor=lightyellow];
91 [label="CASE", fontsize=14, style = filled, fillcolor = lightcyan];
3 -> 91 [arrowhead = none ];
91 -> 4;

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

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

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

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

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

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

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

99 [label="SPLIT 1", fontsize=14, style = filled, fillcolor = violet];
24 -> 99 [arrowhead = none ];
99 -> 35;

100 [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];
24 -> 100 [arrowhead = none ];
100 -> 36;

101 [label="CASE", fontsize=14, style = filled, fillcolor = lightcyan];
35 -> 101 [arrowhead = none ];
101 -> 41;

102 [label="SPLIT 1", fontsize=14, style = filled, fillcolor = violet];
36 -> 102 [arrowhead = none ];
102 -> 70;

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

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

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

106 [label="EVAL with clause\nap1(nil, X32, X32).\nand substitutionX13 -> nil,\nT12 -> T33,\nX14 -> T34,\nX32 -> cons(T33, T34),\nX33 -> T34,\nT9 -> cons(T33, T34)", fontsize=14, style = filled, fillcolor = lightblue];
43 -> 106 [arrowhead = none ];
106 -> 50;

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

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

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

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

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

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

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

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

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

116 [label="EVAL with clause\nap2(nil, X67, X67).\nand substitutionT18 -> nil,\nT19 -> T58,\nX67 -> T58,\nX15 -> T58", fontsize=14, style = filled, fillcolor = lightblue];
75 -> 116 [arrowhead = none ];
116 -> 77;

117 [label="EVAL-BACKTRACK", fontsize=14, style = filled, fillcolor = lightgreen];
75 -> 117 [arrowhead = none ];
117 -> 78;

118 [label="EVAL with clause\nap2(cons(X78, X79), X80, cons(X78, X81)) :- ap2(X79, X80, X81).\nand substitutionX78 -> T65,\nX79 -> T66,\nT18 -> cons(T65, T66),\nT19 -> T67,\nX80 -> T67,\nX81 -> X82,\nX15 -> cons(T65, X82)", fontsize=14, style = filled, fillcolor = lightblue];
76 -> 118 [arrowhead = none ];
118 -> 87;

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

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

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

}

(2) Obligation:

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

f3_in(nil) → f3_out1(nil)
f3_in(T9) → U1(f24_in(T9), T9)
U1(f24_out1(X13, T12, X14, X15, T13), T9) → f3_out1(cons(T12, T13))
f35_in(cons(T33, T34)) → f35_out1(nil, T33, T34)
f35_in(cons(T42, T43)) → U2(f35_in(T43), cons(T42, T43))
U2(f35_out1(X53, T44, X54), cons(T42, T43)) → f35_out1(cons(T42, X53), T44, X54)
f70_in(nil, T58) → f70_out1(T58)
f70_in(cons(T65, T66), T67) → U3(f70_in(T66, T67), cons(T65, T66), T67)
U3(f70_out1(X82), cons(T65, T66), T67) → f70_out1(cons(T65, X82))
f24_in(T9) → U4(f35_in(T9), T9)
U4(f35_out1(T18, T12, T19), T9) → U5(f36_in(T18, T19), T9, T18, T12, T19)
U5(f36_out1(X15, T20), T9, T18, T12, T19) → f24_out1(T18, T12, T19, X15, T20)
f36_in(T18, T19) → U6(f70_in(T18, T19), T18, T19)
U6(f70_out1(T51), T18, T19) → U7(f3_in(T51), T18, T19, T51)
U7(f3_out1(T20), T18, T19, T51) → f36_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:

F3_IN(T9) → U1¹(f24_in(T9), T9)
F3_IN(T9) → F24_IN(T9)
F35_IN(cons(T42, T43)) → U2¹(f35_in(T43), cons(T42, T43))
F35_IN(cons(T42, T43)) → F35_IN(T43)
F70_IN(cons(T65, T66), T67) → U3¹(f70_in(T66, T67), cons(T65, T66), T67)
F70_IN(cons(T65, T66), T67) → F70_IN(T66, T67)
F24_IN(T9) → U4¹(f35_in(T9), T9)
F24_IN(T9) → F35_IN(T9)
U4¹(f35_out1(T18, T12, T19), T9) → U5¹(f36_in(T18, T19), T9, T18, T12, T19)
U4¹(f35_out1(T18, T12, T19), T9) → F36_IN(T18, T19)
F36_IN(T18, T19) → U6¹(f70_in(T18, T19), T18, T19)
F36_IN(T18, T19) → F70_IN(T18, T19)
U6¹(f70_out1(T51), T18, T19) → U7¹(f3_in(T51), T18, T19, T51)
U6¹(f70_out1(T51), T18, T19) → F3_IN(T51)

The TRS R consists of the following rules:

f3_in(nil) → f3_out1(nil)
f3_in(T9) → U1(f24_in(T9), T9)
U1(f24_out1(X13, T12, X14, X15, T13), T9) → f3_out1(cons(T12, T13))
f35_in(cons(T33, T34)) → f35_out1(nil, T33, T34)
f35_in(cons(T42, T43)) → U2(f35_in(T43), cons(T42, T43))
U2(f35_out1(X53, T44, X54), cons(T42, T43)) → f35_out1(cons(T42, X53), T44, X54)
f70_in(nil, T58) → f70_out1(T58)
f70_in(cons(T65, T66), T67) → U3(f70_in(T66, T67), cons(T65, T66), T67)
U3(f70_out1(X82), cons(T65, T66), T67) → f70_out1(cons(T65, X82))
f24_in(T9) → U4(f35_in(T9), T9)
U4(f35_out1(T18, T12, T19), T9) → U5(f36_in(T18, T19), T9, T18, T12, T19)
U5(f36_out1(X15, T20), T9, T18, T12, T19) → f24_out1(T18, T12, T19, X15, T20)
f36_in(T18, T19) → U6(f70_in(T18, T19), T18, T19)
U6(f70_out1(T51), T18, T19) → U7(f3_in(T51), T18, T19, T51)
U7(f3_out1(T20), T18, T19, T51) → f36_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:

F70_IN(cons(T65, T66), T67) → F70_IN(T66, T67)

The TRS R consists of the following rules:

f3_in(nil) → f3_out1(nil)
f3_in(T9) → U1(f24_in(T9), T9)
U1(f24_out1(X13, T12, X14, X15, T13), T9) → f3_out1(cons(T12, T13))
f35_in(cons(T33, T34)) → f35_out1(nil, T33, T34)
f35_in(cons(T42, T43)) → U2(f35_in(T43), cons(T42, T43))
U2(f35_out1(X53, T44, X54), cons(T42, T43)) → f35_out1(cons(T42, X53), T44, X54)
f70_in(nil, T58) → f70_out1(T58)
f70_in(cons(T65, T66), T67) → U3(f70_in(T66, T67), cons(T65, T66), T67)
U3(f70_out1(X82), cons(T65, T66), T67) → f70_out1(cons(T65, X82))
f24_in(T9) → U4(f35_in(T9), T9)
U4(f35_out1(T18, T12, T19), T9) → U5(f36_in(T18, T19), T9, T18, T12, T19)
U5(f36_out1(X15, T20), T9, T18, T12, T19) → f24_out1(T18, T12, T19, X15, T20)
f36_in(T18, T19) → U6(f70_in(T18, T19), T18, T19)
U6(f70_out1(T51), T18, T19) → U7(f3_in(T51), T18, T19, T51)
U7(f3_out1(T20), T18, T19, T51) → f36_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:

F70_IN(cons(T65, T66), T67) → F70_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:

• F70_IN(cons(T65, T66), T67) → F70_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:

F35_IN(cons(T42, T43)) → F35_IN(T43)

The TRS R consists of the following rules:

f3_in(nil) → f3_out1(nil)
f3_in(T9) → U1(f24_in(T9), T9)
U1(f24_out1(X13, T12, X14, X15, T13), T9) → f3_out1(cons(T12, T13))
f35_in(cons(T33, T34)) → f35_out1(nil, T33, T34)
f35_in(cons(T42, T43)) → U2(f35_in(T43), cons(T42, T43))
U2(f35_out1(X53, T44, X54), cons(T42, T43)) → f35_out1(cons(T42, X53), T44, X54)
f70_in(nil, T58) → f70_out1(T58)
f70_in(cons(T65, T66), T67) → U3(f70_in(T66, T67), cons(T65, T66), T67)
U3(f70_out1(X82), cons(T65, T66), T67) → f70_out1(cons(T65, X82))
f24_in(T9) → U4(f35_in(T9), T9)
U4(f35_out1(T18, T12, T19), T9) → U5(f36_in(T18, T19), T9, T18, T12, T19)
U5(f36_out1(X15, T20), T9, T18, T12, T19) → f24_out1(T18, T12, T19, X15, T20)
f36_in(T18, T19) → U6(f70_in(T18, T19), T18, T19)
U6(f70_out1(T51), T18, T19) → U7(f3_in(T51), T18, T19, T51)
U7(f3_out1(T20), T18, T19, T51) → f36_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:

F35_IN(cons(T42, T43)) → F35_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:

• F35_IN(cons(T42, T43)) → F35_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:

F3_IN(T9) → F24_IN(T9)
F24_IN(T9) → U4¹(f35_in(T9), T9)
U4¹(f35_out1(T18, T12, T19), T9) → F36_IN(T18, T19)
F36_IN(T18, T19) → U6¹(f70_in(T18, T19), T18, T19)
U6¹(f70_out1(T51), T18, T19) → F3_IN(T51)

The TRS R consists of the following rules:

f3_in(nil) → f3_out1(nil)
f3_in(T9) → U1(f24_in(T9), T9)
U1(f24_out1(X13, T12, X14, X15, T13), T9) → f3_out1(cons(T12, T13))
f35_in(cons(T33, T34)) → f35_out1(nil, T33, T34)
f35_in(cons(T42, T43)) → U2(f35_in(T43), cons(T42, T43))
U2(f35_out1(X53, T44, X54), cons(T42, T43)) → f35_out1(cons(T42, X53), T44, X54)
f70_in(nil, T58) → f70_out1(T58)
f70_in(cons(T65, T66), T67) → U3(f70_in(T66, T67), cons(T65, T66), T67)
U3(f70_out1(X82), cons(T65, T66), T67) → f70_out1(cons(T65, X82))
f24_in(T9) → U4(f35_in(T9), T9)
U4(f35_out1(T18, T12, T19), T9) → U5(f36_in(T18, T19), T9, T18, T12, T19)
U5(f36_out1(X15, T20), T9, T18, T12, T19) → f24_out1(T18, T12, T19, X15, T20)
f36_in(T18, T19) → U6(f70_in(T18, T19), T18, T19)
U6(f70_out1(T51), T18, T19) → U7(f3_in(T51), T18, T19, T51)
U7(f3_out1(T20), T18, T19, T51) → f36_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.

F24_IN(T9) → U4¹(f35_in(T9), T9)

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

POL(F24_IN(x₁)) = 1 + x₁   
POL(F36_IN(x₁, x₂)) = x₁ + x₂   
POL(F3_IN(x₁)) = 1 + 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(cons(x₁, x₂)) = 1 + x₂   
POL(f35_in(x₁)) = x₁   
POL(f35_out1(x₁, x₂, x₃)) = x₁ + x₃   
POL(f70_in(x₁, x₂)) = x₁ + x₂   
POL(f70_out1(x₁)) = 1 + x₁   
POL(nil) = 1   

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

f35_in(cons(T33, T34)) → f35_out1(nil, T33, T34)
f35_in(cons(T42, T43)) → U2(f35_in(T43), cons(T42, T43))
f70_in(nil, T58) → f70_out1(T58)
f70_in(cons(T65, T66), T67) → U3(f70_in(T66, T67), cons(T65, T66), T67)
U2(f35_out1(X53, T44, X54), cons(T42, T43)) → f35_out1(cons(T42, X53), T44, X54)
U3(f70_out1(X82), cons(T65, T66), T67) → f70_out1(cons(T65, X82))

(19) Obligation:

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

F3_IN(T9) → F24_IN(T9)
U4¹(f35_out1(T18, T12, T19), T9) → F36_IN(T18, T19)
F36_IN(T18, T19) → U6¹(f70_in(T18, T19), T18, T19)
U6¹(f70_out1(T51), T18, T19) → F3_IN(T51)

The TRS R consists of the following rules:

f3_in(nil) → f3_out1(nil)
f3_in(T9) → U1(f24_in(T9), T9)
U1(f24_out1(X13, T12, X14, X15, T13), T9) → f3_out1(cons(T12, T13))
f35_in(cons(T33, T34)) → f35_out1(nil, T33, T34)
f35_in(cons(T42, T43)) → U2(f35_in(T43), cons(T42, T43))
U2(f35_out1(X53, T44, X54), cons(T42, T43)) → f35_out1(cons(T42, X53), T44, X54)
f70_in(nil, T58) → f70_out1(T58)
f70_in(cons(T65, T66), T67) → U3(f70_in(T66, T67), cons(T65, T66), T67)
U3(f70_out1(X82), cons(T65, T66), T67) → f70_out1(cons(T65, X82))
f24_in(T9) → U4(f35_in(T9), T9)
U4(f35_out1(T18, T12, T19), T9) → U5(f36_in(T18, T19), T9, T18, T12, T19)
U5(f36_out1(X15, T20), T9, T18, T12, T19) → f24_out1(T18, T12, T19, X15, T20)
f36_in(T18, T19) → U6(f70_in(T18, T19), T18, T19)
U6(f70_out1(T51), T18, T19) → U7(f3_in(T51), T18, T19, T51)
U7(f3_out1(T20), T18, T19, T51) → f36_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