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

(0) Obligation:

Clauses:

perm(Xs, .(X, Ys)) :- ','(app(X1s, .(X, X2s), Xs), ','(app(X1s, X2s, Zs), perm(Zs, Ys))).
perm([], []).
app(.(X, Xs), Ys, .(X, Zs)) :- app(Xs, Ys, Zs).
app([], Ys, Ys).

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];
4 [label="4: 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];
19 [label="19: ','(app(X22, .(T18, X23), T15), ','(app(X22, X23, X24), perm(X24, T19)))\n\nT15 is ground\nX22 is free\nX23 is free\nX24 is free", fontsize=16, style=filled, fillcolor=lightyellow];
20 [label="20: \n\n", fontsize=16, style=filled, fillcolor=lightyellow];
26 [label="26: app(X22, .(T18, X23), T15)\n\nT15 is ground\nX22 is free\nX23 is free", fontsize=16, style=filled, fillcolor=lightyellow];
28 [label="28: ','(app(T23, T24, X24), perm(X24, T25))\n\nT23 is ground\nT24 is ground\nX24 is free", fontsize=16, style=filled, fillcolor=lightyellow];
31 [label="31: app(X22, .(T18, X23), T15), SCOPE: 2, CLAUSE: 2 | app(X22, .(T18, X23), T15), SCOPE: 2, CLAUSE: 3\n\nT15 is ground\nX22 is free\nX23 is free", fontsize=16, style=filled, fillcolor=lightyellow];
34 [label="34: app(X22, .(T18, X23), T15), SCOPE: 2, CLAUSE: 2\n\nT15 is ground\nX22 is free\nX23 is free", fontsize=16, style=filled, fillcolor=lightyellow];
35 [label="35: app(X22, .(T18, X23), T15), SCOPE: 2, CLAUSE: 3\n\nT15 is ground\nX22 is free\nX23 is free", fontsize=16, style=filled, fillcolor=lightyellow];
44 [label="44: app(X72, .(T44, X73), T43)\n\nT43 is ground\nX72 is free\nX73 is free", fontsize=16, style=filled, fillcolor=lightyellow];
45 [label="45: \n\n", 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];
54 [label="54: app(T23, T24, X24)\n\nT23 is ground\nT24 is ground\nX24 is free", fontsize=16, style=filled, fillcolor=lightyellow];
55 [label="55: perm(T57, T25)\n\nT57 is ground", fontsize=16, style=filled, fillcolor=lightyellow];
60 [label="60: app(T23, T24, X24), SCOPE: 3, CLAUSE: 2 | app(T23, T24, X24), SCOPE: 3, CLAUSE: 3\n\nT23 is ground\nT24 is ground\nX24 is free", fontsize=16, style=filled, fillcolor=lightyellow];
63 [label="63: app(T23, T24, X24), SCOPE: 3, CLAUSE: 2\n\nT23 is ground\nT24 is ground\nX24 is free", fontsize=16, style=filled, fillcolor=lightyellow];
64 [label="64: app(T23, T24, X24), SCOPE: 3, CLAUSE: 3\n\nT23 is ground\nT24 is ground\nX24 is free", fontsize=16, style=filled, fillcolor=lightyellow];
72 [label="72: app(T74, T75, X121)\n\nT74 is ground\nT75 is ground\nX121 is free", fontsize=16, style=filled, fillcolor=lightyellow];
73 [label="73: \n\n", fontsize=16, style=filled, fillcolor=lightyellow];
76 [label="76: true\n\n", fontsize=16, style=filled, fillcolor=lightyellow];
77 [label="77: \n\n", fontsize=16, style=filled, fillcolor=lightyellow];
78 [label="78: \n\n", fontsize=16, style=filled, fillcolor=lightyellow];
81 [label="81: true\n\n", fontsize=16, style=filled, fillcolor=lightyellow];
82 [label="82: \n\n", fontsize=16, style=filled, fillcolor=lightyellow];
83 [label="83: \n\n", fontsize=16, style=filled, fillcolor=lightyellow];
84 [label="CASE", fontsize=14, style = filled, fillcolor = lightcyan];
1 -> 84 [arrowhead = none ];
84 -> 4;

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

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

87 [label="EVAL with clause\nperm(X19, .(X20, X21)) :- ','(app(X22, .(X20, X23), X19), ','(app(X22, X23, X24), perm(X24, X21))).\nand substitutionT1 -> T15,\nX19 -> T15,\nX20 -> T18,\nX21 -> T19,\nT2 -> .(T18, T19),\nT16 -> T18,\nT17 -> T19", fontsize=14, style = filled, fillcolor = lightblue];
7 -> 87 [arrowhead = none ];
87 -> 19;

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

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

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

91 [label="SPLIT 1", fontsize=14, style = filled, fillcolor = violet];
19 -> 91 [arrowhead = none ];
91 -> 26;

92 [label="SPLIT 2\nnew knowledge:\nT23 is ground\nT18 is ground\nT24 is ground\nT15 is ground\nreplacements:X22 -> T23,\nX23 -> T24,\nT19 -> T25", fontsize=14, style = filled, fillcolor = violet];
19 -> 92 [arrowhead = none ];
92 -> 28;

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

94 [label="SPLIT 1", fontsize=14, style = filled, fillcolor = violet];
28 -> 94 [arrowhead = none ];
94 -> 54;

95 [label="SPLIT 2\nnew knowledge:\nT23 is ground\nT24 is ground\nT57 is ground\nreplacements:X24 -> T57", fontsize=14, style = filled, fillcolor = violet];
28 -> 95 [arrowhead = none ];
95 -> 55;

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

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

98 [label="EVAL with clause\napp(.(X67, X68), X69, .(X67, X70)) :- app(X68, X69, X70).\nand substitutionX67 -> T42,\nX68 -> X72,\nX22 -> .(T42, X72),\nT18 -> T44,\nX23 -> X73,\nX69 -> .(T44, X73),\nX71 -> T42,\nX70 -> T43,\nT15 -> .(T42, T43),\nT41 -> T44", fontsize=14, style = filled, fillcolor = lightblue];
34 -> 98 [arrowhead = none ];
98 -> 44;

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

100 [label="EVAL with clause\napp([], X85, X85).\nand substitutionX22 -> [],\nT18 -> T52,\nX23 -> T53,\nX85 -> .(T52, T53),\nX86 -> T53,\nT15 -> .(T52, T53)", fontsize=14, style = filled, fillcolor = lightblue];
35 -> 100 [arrowhead = none ];
100 -> 49;

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

102 [label="INSTANCE with matching:\nX22 -> X72\nT18 -> T44\nX23 -> X73\nT15 -> T43", fontsize=14, style = filled, fillcolor = lightgrey];
44 -> 102 [arrowhead = none , style=dashed];
102 -> 26[style=dashed];

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

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

105 [label="INSTANCE with matching:\nT1 -> T57\nT2 -> T25", fontsize=14, style = filled, fillcolor = lightgrey];
55 -> 105 [arrowhead = none , style=dashed];
105 -> 1[style=dashed];

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

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

108 [label="EVAL with clause\napp(.(X117, X118), X119, .(X117, X120)) :- app(X118, X119, X120).\nand substitutionX117 -> T73,\nX118 -> T74,\nT23 -> .(T73, T74),\nT24 -> T75,\nX119 -> T75,\nX120 -> X121,\nX24 -> .(T73, X121)", fontsize=14, style = filled, fillcolor = lightblue];
63 -> 108 [arrowhead = none ];
108 -> 72;

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

110 [label="EVAL with clause\napp([], X129, X129).\nand substitutionT23 -> [],\nT24 -> T81,\nX129 -> T81,\nX24 -> T81", fontsize=14, style = filled, fillcolor = lightblue];
64 -> 110 [arrowhead = none ];
110 -> 76;

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

112 [label="INSTANCE with matching:\nT23 -> T74\nT24 -> T75\nX24 -> X121", fontsize=14, style = filled, fillcolor = lightgrey];
72 -> 112 [arrowhead = none , style=dashed];
112 -> 54[style=dashed];

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

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

}

(2) Obligation:

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

f1_in(T15) → U1(f19_in(T15), T15)
U1(f19_out1(X22, T18, X23, X24, T19), T15) → f1_out1(.(T18, T19))
f1_in([]) → f1_out1([])
f26_in(.(T42, T43)) → U2(f26_in(T43), .(T42, T43))
U2(f26_out1(X72, T44, X73), .(T42, T43)) → f26_out1(.(T42, X72), T44, X73)
f26_in(.(T52, T53)) → f26_out1([], T52, T53)
f54_in(.(T73, T74), T75) → U3(f54_in(T74, T75), .(T73, T74), T75)
U3(f54_out1(X121), .(T73, T74), T75) → f54_out1(.(T73, X121))
f54_in([], T81) → f54_out1(T81)
f19_in(T15) → U4(f26_in(T15), T15)
U4(f26_out1(T23, T18, T24), T15) → U5(f28_in(T23, T24), T15, T23, T18, T24)
U5(f28_out1(X24, T25), T15, T23, T18, T24) → f19_out1(T23, T18, T24, X24, T25)
f28_in(T23, T24) → U6(f54_in(T23, T24), T23, T24)
U6(f54_out1(T57), T23, T24) → U7(f1_in(T57), T23, T24, T57)
U7(f1_out1(T25), T23, T24, T57) → f28_out1(T57, T25)

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(T15) → U1¹(f19_in(T15), T15)
F1_IN(T15) → F19_IN(T15)
F26_IN(.(T42, T43)) → U2¹(f26_in(T43), .(T42, T43))
F26_IN(.(T42, T43)) → F26_IN(T43)
F54_IN(.(T73, T74), T75) → U3¹(f54_in(T74, T75), .(T73, T74), T75)
F54_IN(.(T73, T74), T75) → F54_IN(T74, T75)
F19_IN(T15) → U4¹(f26_in(T15), T15)
F19_IN(T15) → F26_IN(T15)
U4¹(f26_out1(T23, T18, T24), T15) → U5¹(f28_in(T23, T24), T15, T23, T18, T24)
U4¹(f26_out1(T23, T18, T24), T15) → F28_IN(T23, T24)
F28_IN(T23, T24) → U6¹(f54_in(T23, T24), T23, T24)
F28_IN(T23, T24) → F54_IN(T23, T24)
U6¹(f54_out1(T57), T23, T24) → U7¹(f1_in(T57), T23, T24, T57)
U6¹(f54_out1(T57), T23, T24) → F1_IN(T57)

The TRS R consists of the following rules:

f1_in(T15) → U1(f19_in(T15), T15)
U1(f19_out1(X22, T18, X23, X24, T19), T15) → f1_out1(.(T18, T19))
f1_in([]) → f1_out1([])
f26_in(.(T42, T43)) → U2(f26_in(T43), .(T42, T43))
U2(f26_out1(X72, T44, X73), .(T42, T43)) → f26_out1(.(T42, X72), T44, X73)
f26_in(.(T52, T53)) → f26_out1([], T52, T53)
f54_in(.(T73, T74), T75) → U3(f54_in(T74, T75), .(T73, T74), T75)
U3(f54_out1(X121), .(T73, T74), T75) → f54_out1(.(T73, X121))
f54_in([], T81) → f54_out1(T81)
f19_in(T15) → U4(f26_in(T15), T15)
U4(f26_out1(T23, T18, T24), T15) → U5(f28_in(T23, T24), T15, T23, T18, T24)
U5(f28_out1(X24, T25), T15, T23, T18, T24) → f19_out1(T23, T18, T24, X24, T25)
f28_in(T23, T24) → U6(f54_in(T23, T24), T23, T24)
U6(f54_out1(T57), T23, T24) → U7(f1_in(T57), T23, T24, T57)
U7(f1_out1(T25), T23, T24, T57) → f28_out1(T57, T25)

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:

F54_IN(.(T73, T74), T75) → F54_IN(T74, T75)

The TRS R consists of the following rules:

f1_in(T15) → U1(f19_in(T15), T15)
U1(f19_out1(X22, T18, X23, X24, T19), T15) → f1_out1(.(T18, T19))
f1_in([]) → f1_out1([])
f26_in(.(T42, T43)) → U2(f26_in(T43), .(T42, T43))
U2(f26_out1(X72, T44, X73), .(T42, T43)) → f26_out1(.(T42, X72), T44, X73)
f26_in(.(T52, T53)) → f26_out1([], T52, T53)
f54_in(.(T73, T74), T75) → U3(f54_in(T74, T75), .(T73, T74), T75)
U3(f54_out1(X121), .(T73, T74), T75) → f54_out1(.(T73, X121))
f54_in([], T81) → f54_out1(T81)
f19_in(T15) → U4(f26_in(T15), T15)
U4(f26_out1(T23, T18, T24), T15) → U5(f28_in(T23, T24), T15, T23, T18, T24)
U5(f28_out1(X24, T25), T15, T23, T18, T24) → f19_out1(T23, T18, T24, X24, T25)
f28_in(T23, T24) → U6(f54_in(T23, T24), T23, T24)
U6(f54_out1(T57), T23, T24) → U7(f1_in(T57), T23, T24, T57)
U7(f1_out1(T25), T23, T24, T57) → f28_out1(T57, T25)

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:

F54_IN(.(T73, T74), T75) → F54_IN(T74, T75)

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:

• F54_IN(.(T73, T74), T75) → F54_IN(T74, T75)
  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:

F26_IN(.(T42, T43)) → F26_IN(T43)

The TRS R consists of the following rules:

f1_in(T15) → U1(f19_in(T15), T15)
U1(f19_out1(X22, T18, X23, X24, T19), T15) → f1_out1(.(T18, T19))
f1_in([]) → f1_out1([])
f26_in(.(T42, T43)) → U2(f26_in(T43), .(T42, T43))
U2(f26_out1(X72, T44, X73), .(T42, T43)) → f26_out1(.(T42, X72), T44, X73)
f26_in(.(T52, T53)) → f26_out1([], T52, T53)
f54_in(.(T73, T74), T75) → U3(f54_in(T74, T75), .(T73, T74), T75)
U3(f54_out1(X121), .(T73, T74), T75) → f54_out1(.(T73, X121))
f54_in([], T81) → f54_out1(T81)
f19_in(T15) → U4(f26_in(T15), T15)
U4(f26_out1(T23, T18, T24), T15) → U5(f28_in(T23, T24), T15, T23, T18, T24)
U5(f28_out1(X24, T25), T15, T23, T18, T24) → f19_out1(T23, T18, T24, X24, T25)
f28_in(T23, T24) → U6(f54_in(T23, T24), T23, T24)
U6(f54_out1(T57), T23, T24) → U7(f1_in(T57), T23, T24, T57)
U7(f1_out1(T25), T23, T24, T57) → f28_out1(T57, T25)

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:

F26_IN(.(T42, T43)) → F26_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:

• F26_IN(.(T42, T43)) → F26_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(T15) → F19_IN(T15)
F19_IN(T15) → U4¹(f26_in(T15), T15)
U4¹(f26_out1(T23, T18, T24), T15) → F28_IN(T23, T24)
F28_IN(T23, T24) → U6¹(f54_in(T23, T24), T23, T24)
U6¹(f54_out1(T57), T23, T24) → F1_IN(T57)

The TRS R consists of the following rules:

f1_in(T15) → U1(f19_in(T15), T15)
U1(f19_out1(X22, T18, X23, X24, T19), T15) → f1_out1(.(T18, T19))
f1_in([]) → f1_out1([])
f26_in(.(T42, T43)) → U2(f26_in(T43), .(T42, T43))
U2(f26_out1(X72, T44, X73), .(T42, T43)) → f26_out1(.(T42, X72), T44, X73)
f26_in(.(T52, T53)) → f26_out1([], T52, T53)
f54_in(.(T73, T74), T75) → U3(f54_in(T74, T75), .(T73, T74), T75)
U3(f54_out1(X121), .(T73, T74), T75) → f54_out1(.(T73, X121))
f54_in([], T81) → f54_out1(T81)
f19_in(T15) → U4(f26_in(T15), T15)
U4(f26_out1(T23, T18, T24), T15) → U5(f28_in(T23, T24), T15, T23, T18, T24)
U5(f28_out1(X24, T25), T15, T23, T18, T24) → f19_out1(T23, T18, T24, X24, T25)
f28_in(T23, T24) → U6(f54_in(T23, T24), T23, T24)
U6(f54_out1(T57), T23, T24) → U7(f1_in(T57), T23, T24, T57)
U7(f1_out1(T25), T23, T24, T57) → f28_out1(T57, T25)

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.

F1_IN(T15) → F19_IN(T15)
F19_IN(T15) → U4¹(f26_in(T15), T15)

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

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

POL( f26_in(x₁) ) = x₁

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

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

POL( f26_out1(x₁, ..., x₃) ) = x₁ + x₃ + 2

POL( [] ) = 0

POL( U6¹(x₁, ..., x₃) ) = 2x₁ + 2

POL( f54_in(x₁, x₂) ) = x₁ + x₂

POL( U3(x₁, ..., x₃) ) = x₁ + 2

POL( f54_out1(x₁) ) = x₁

POL( F1_IN(x₁) ) = 2x₁ + 2

POL( F19_IN(x₁) ) = 2x₁ + 1

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

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

f26_in(.(T42, T43)) → U2(f26_in(T43), .(T42, T43))
f26_in(.(T52, T53)) → f26_out1([], T52, T53)
f54_in(.(T73, T74), T75) → U3(f54_in(T74, T75), .(T73, T74), T75)
f54_in([], T81) → f54_out1(T81)
U2(f26_out1(X72, T44, X73), .(T42, T43)) → f26_out1(.(T42, X72), T44, X73)
U3(f54_out1(X121), .(T73, T74), T75) → f54_out1(.(T73, X121))

(19) Obligation:

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

U4¹(f26_out1(T23, T18, T24), T15) → F28_IN(T23, T24)
F28_IN(T23, T24) → U6¹(f54_in(T23, T24), T23, T24)
U6¹(f54_out1(T57), T23, T24) → F1_IN(T57)

The TRS R consists of the following rules:

f1_in(T15) → U1(f19_in(T15), T15)
U1(f19_out1(X22, T18, X23, X24, T19), T15) → f1_out1(.(T18, T19))
f1_in([]) → f1_out1([])
f26_in(.(T42, T43)) → U2(f26_in(T43), .(T42, T43))
U2(f26_out1(X72, T44, X73), .(T42, T43)) → f26_out1(.(T42, X72), T44, X73)
f26_in(.(T52, T53)) → f26_out1([], T52, T53)
f54_in(.(T73, T74), T75) → U3(f54_in(T74, T75), .(T73, T74), T75)
U3(f54_out1(X121), .(T73, T74), T75) → f54_out1(.(T73, X121))
f54_in([], T81) → f54_out1(T81)
f19_in(T15) → U4(f26_in(T15), T15)
U4(f26_out1(T23, T18, T24), T15) → U5(f28_in(T23, T24), T15, T23, T18, T24)
U5(f28_out1(X24, T25), T15, T23, T18, T24) → f19_out1(T23, T18, T24, X24, T25)
f28_in(T23, T24) → U6(f54_in(T23, T24), T23, T24)
U6(f54_out1(T57), T23, T24) → U7(f1_in(T57), T23, T24, T57)
U7(f1_out1(T25), T23, T24, T57) → f28_out1(T57, T25)

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

(21) TRUE