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

(0) Obligation:

Clauses:

star(U, []) :- !.
star([], W) :- ','(!, =(W, [])).
star(U, W) :- ','(app(U, V, W), star(U, V)).
app([], L, L).
app(.(X, L), M, .(X, N)) :- app(L, M, N).
=(X, X).

Query: star(g,g)

(1) BuiltinConflictTransformerProof (EQUIVALENT transformation)

Renamed defined predicates conflicting with built-in predicates [PROLOG].

(2) Obligation:

Clauses:

star(U, []) :- !.
star([], W) :- ','(!, user_defined_=(W, [])).
star(U, W) :- ','(app(U, V, W), star(U, V)).
app([], L, L).
app(.(X, L), M, .(X, N)) :- app(L, M, N).
user_defined_=(X, X).

Query: star(g,g)

(3) PrologToPiTRSViaGraphTransformerProof (SOUND transformation)

Transformed Prolog program to (Pi-)TRS.

digraph dp_graph {
node [outthreshold=100, inthreshold=100];
2 [label="A: star(T1, T2)\n\nT1 is ground\nT2 is ground", fontsize=16, style=filled, fillcolor=lightyellow, color=red];
6 [label="6: star(T1, T2), SCOPE: 1, CLAUSE: 0 | star(T1, T2), SCOPE: 1, CLAUSE: 1 | star(T1, T2), SCOPE: 1, CLAUSE: 2\n\nT1 is ground\nT2 is ground", fontsize=16, style=filled, fillcolor=lightyellow];
9 [label="9: !_1 | star(T4, []), SCOPE: 1, CLAUSE: 1 | star(T4, []), SCOPE: 1, CLAUSE: 2\n\nT4 is ground", fontsize=16, style=filled, fillcolor=lightyellow];
12 [label="12: star(T1, T2), SCOPE: 1, CLAUSE: 1 | star(T1, T2), SCOPE: 1, CLAUSE: 2\n\nT1 is ground\nT2 is ground\nX2 is free\nstar(T1, T2) !=? star(X2, [])", fontsize=16, style=filled, fillcolor=lightyellow];
15 [label="15: true\n\n", fontsize=16, style=filled, fillcolor=lightyellow];
29 [label="29: \n\n", fontsize=16, style=filled, fillcolor=lightyellow];
30 [label="30: ','(!_1, user_defined_=(T6, [])) | star([], T6), SCOPE: 1, CLAUSE: 2\n\nT6 is ground\nX2 is free\nstar([], T6) !=? star(X2, [])", fontsize=16, style=filled, fillcolor=lightyellow];
32 [label="32: star(T1, T2), SCOPE: 1, CLAUSE: 2\n\nT1 is ground\nT2 is ground\nX2 is free\nX4 is free\nstar(T1, T2) !=? star(X2, [])\nstar(T1, T2) !=? star([], X4)", fontsize=16, style=filled, fillcolor=lightyellow];
33 [label="33: user_defined_=(T6, [])\n\nT6 is ground\nX2 is free\nstar([], T6) !=? star(X2, [])", fontsize=16, style=filled, fillcolor=lightyellow];
35 [label="35: user_defined_=(T6, []), SCOPE: 2, CLAUSE: 5\n\nT6 is ground\nX2 is free\nstar([], T6) !=? star(X2, [])", fontsize=16, style=filled, fillcolor=lightyellow];
36 [label="36: \n\n", fontsize=16, style=filled, fillcolor=lightyellow];
37 [label="37: ','(app(T10, X10, T11), star(T10, X10))\n\nT10 is ground\nT11 is ground\nX2 is free\nX4 is free\nX10 is free\nstar(T10, T11) !=? star(X2, [])\nstar(T10, T11) !=? star([], X4)", fontsize=16, style=filled, fillcolor=lightyellow];
38 [label="38: ','(app(T10, X10, T11), star(T10, X10)), SCOPE: 3, CLAUSE: 3 | ','(app(T10, X10, T11), star(T10, X10)), SCOPE: 3, CLAUSE: 4\n\nT10 is ground\nT11 is ground\nX2 is free\nX4 is free\nX10 is free\nstar(T10, T11) !=? star(X2, [])\nstar(T10, T11) !=? star([], X4)", fontsize=16, style=filled, fillcolor=lightyellow];
39 [label="39: ','(app(T10, X10, T11), star(T10, X10)), SCOPE: 3, CLAUSE: 4\n\nT10 is ground\nT11 is ground\nX2 is free\nX4 is free\nX10 is free\nstar(T10, T11) !=? star(X2, [])\nstar(T10, T11) !=? star([], X4)", fontsize=16, style=filled, fillcolor=lightyellow];
41 [label="B: ','(app(T20, X27, T21), star(.(T19, T20), X27))\n\nT19 is ground\nT20 is ground\nT21 is ground\nX27 is free", fontsize=16, style=filled, fillcolor=lightyellow];
42 [label="42: \n\n", fontsize=16, style=filled, fillcolor=lightyellow];
49 [label="C: app(T20, X27, T21)\n\nT20 is ground\nT21 is ground\nX27 is free", fontsize=16, style=filled, fillcolor=lightyellow];
50 [label="50: star(.(T19, T20), T24)\n\nT19 is ground\nT20 is ground\nT24 is ground", fontsize=16, style=filled, fillcolor=lightyellow];
52 [label="52: app(T20, X27, T21), SCOPE: 4, CLAUSE: 3 | app(T20, X27, T21), SCOPE: 4, CLAUSE: 4\n\nT20 is ground\nT21 is ground\nX27 is free", fontsize=16, style=filled, fillcolor=lightyellow];
60 [label="60: app(T20, X27, T21), SCOPE: 4, CLAUSE: 3\n\nT20 is ground\nT21 is ground\nX27 is free", fontsize=16, style=filled, fillcolor=lightyellow];
61 [label="61: app(T20, X27, T21), SCOPE: 4, CLAUSE: 4\n\nT20 is ground\nT21 is ground\nX27 is free", fontsize=16, style=filled, fillcolor=lightyellow];
64 [label="64: true\n\n", fontsize=16, style=filled, fillcolor=lightyellow];
65 [label="65: \n\n", fontsize=16, style=filled, fillcolor=lightyellow];
67 [label="67: \n\n", fontsize=16, style=filled, fillcolor=lightyellow];
77 [label="77: app(T39, X60, T40)\n\nT39 is ground\nT40 is ground\nX60 is free", 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];
2 -> 79 [arrowhead = none ];
79 -> 6;

80 [label="EVAL with clause\nstar(X2, []) :- !_1.\nand substitutionT1 -> T4,\nX2 -> T4,\nT2 -> []", fontsize=14, style = filled, fillcolor = lightblue];
6 -> 80 [arrowhead = none ];
80 -> 9;

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

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

83 [label="EVAL with clause\nstar([], X4) :- ','(!_1, user_defined_=(X4, [])).\nand substitutionT1 -> [],\nT2 -> T6,\nX4 -> T6", fontsize=14, style = filled, fillcolor = lightblue];
12 -> 83 [arrowhead = none ];
83 -> 30;

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

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

86 [label="CUT", fontsize=14, style = filled, fillcolor = lightgreen];
30 -> 86 [arrowhead = none ];
86 -> 33;

87 [label="ONLY EVAL with clause\nstar(X8, X9) :- ','(app(X8, X10, X9), star(X8, X10)).\nand substitutionT1 -> T10,\nX8 -> T10,\nT2 -> T11,\nX9 -> T11", fontsize=14, style = filled, fillcolor = lightblue];
32 -> 87 [arrowhead = none ];
87 -> 37;

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

89 [label="BACKTRACK\nfor clause: user_defined_=(X, X)\nwith clash: (star([], T6), star(X2, []))", fontsize=14, style = filled, fillcolor = lightgreen];
35 -> 89 [arrowhead = none ];
89 -> 36;

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

91 [label="BACKTRACK\nfor clause: app([], L, L)\nwith clash: (star(T10, T11), star([], X4))", fontsize=14, style = filled, fillcolor = lightgreen];
38 -> 91 [arrowhead = none ];
91 -> 39;

92 [label="EVAL with clause\napp(.(X23, X24), X25, .(X23, X26)) :- app(X24, X25, X26).\nand substitutionX23 -> T19,\nX24 -> T20,\nT10 -> .(T19, T20),\nX10 -> X27,\nX25 -> X27,\nX26 -> T21,\nT11 -> .(T19, T21)", fontsize=14, style = filled, fillcolor = lightblue];
39 -> 92 [arrowhead = none ];
92 -> 41;

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

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

95 [label="SPLIT 2\nnew knowledge:\nT20 is ground\nT24 is ground\nT21 is ground\nreplacements:X27 -> T24", fontsize=14, style = filled, fillcolor = violet];
41 -> 95 [arrowhead = none ];
95 -> 50;

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

97 [label="INSTANCE with matching:\nT1 -> .(T19, T20)\nT2 -> T24", fontsize=14, style = filled, fillcolor = lightgrey];
50 -> 97 [arrowhead = none , style=dashed];
97 -> 2[style=dashed];

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

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

100 [label="EVAL with clause\napp([], X44, X44).\nand substitutionT20 -> [],\nX27 -> T31,\nX44 -> T31,\nT21 -> T31,\nX45 -> T31", fontsize=14, style = filled, fillcolor = lightblue];
60 -> 100 [arrowhead = none ];
100 -> 64;

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

102 [label="EVAL with clause\napp(.(X56, X57), X58, .(X56, X59)) :- app(X57, X58, X59).\nand substitutionX56 -> T38,\nX57 -> T39,\nT20 -> .(T38, T39),\nX27 -> X60,\nX58 -> X60,\nX59 -> T40,\nT21 -> .(T38, T40)", fontsize=14, style = filled, fillcolor = lightblue];
61 -> 102 [arrowhead = none ];
102 -> 77;

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

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

105 [label="INSTANCE with matching:\nT20 -> T39\nX27 -> X60\nT21 -> T40", fontsize=14, style = filled, fillcolor = lightgrey];
77 -> 105 [arrowhead = none , style=dashed];
105 -> 49[style=dashed];

}

(4) Obligation:

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

starA_in_gg(T4, []) → starA_out_gg(T4, [])
starA_in_gg(.(T19, T20), .(T19, T21)) → U1_gg(T19, T20, T21, pB_in_gagg(T20, X27, T21, T19))
pB_in_gagg(T20, T24, T21, T19) → U3_gagg(T20, T24, T21, T19, appC_in_gag(T20, T24, T21))
appC_in_gag([], T31, T31) → appC_out_gag([], T31, T31)
appC_in_gag(.(T38, T39), X60, .(T38, T40)) → U2_gag(T38, T39, X60, T40, appC_in_gag(T39, X60, T40))
U2_gag(T38, T39, X60, T40, appC_out_gag(T39, X60, T40)) → appC_out_gag(.(T38, T39), X60, .(T38, T40))
U3_gagg(T20, T24, T21, T19, appC_out_gag(T20, T24, T21)) → U4_gagg(T20, T24, T21, T19, starA_in_gg(.(T19, T20), T24))
U4_gagg(T20, T24, T21, T19, starA_out_gg(.(T19, T20), T24)) → pB_out_gagg(T20, T24, T21, T19)
U1_gg(T19, T20, T21, pB_out_gagg(T20, X27, T21, T19)) → starA_out_gg(.(T19, T20), .(T19, T21))

The argument filtering Pi contains the following mapping:
starA_in_gg(x1, x2)  =  starA_in_gg(x1, x2)
[]  =  []
starA_out_gg(x1, x2)  =  starA_out_gg(x1, x2)
.(x1, x2)  =  .(x1, x2)
U1_gg(x1, x2, x3, x4)  =  U1_gg(x1, x2, x3, x4)
pB_in_gagg(x1, x2, x3, x4)  =  pB_in_gagg(x1, x3, x4)
U3_gagg(x1, x2, x3, x4, x5)  =  U3_gagg(x1, x3, x4, x5)
appC_in_gag(x1, x2, x3)  =  appC_in_gag(x1, x3)
appC_out_gag(x1, x2, x3)  =  appC_out_gag(x1, x2, x3)
U2_gag(x1, x2, x3, x4, x5)  =  U2_gag(x1, x2, x4, x5)
U4_gagg(x1, x2, x3, x4, x5)  =  U4_gagg(x1, x2, x3, x4, x5)
pB_out_gagg(x1, x2, x3, x4)  =  pB_out_gagg(x1, x2, x3, x4)

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

STARA_IN_GG(.(T19, T20), .(T19, T21)) → U1_GG(T19, T20, T21, pB_in_gagg(T20, X27, T21, T19))
STARA_IN_GG(.(T19, T20), .(T19, T21)) → PB_IN_GAGG(T20, X27, T21, T19)
PB_IN_GAGG(T20, T24, T21, T19) → U3_GAGG(T20, T24, T21, T19, appC_in_gag(T20, T24, T21))
PB_IN_GAGG(T20, T24, T21, T19) → APPC_IN_GAG(T20, T24, T21)
APPC_IN_GAG(.(T38, T39), X60, .(T38, T40)) → U2_GAG(T38, T39, X60, T40, appC_in_gag(T39, X60, T40))
APPC_IN_GAG(.(T38, T39), X60, .(T38, T40)) → APPC_IN_GAG(T39, X60, T40)
U3_GAGG(T20, T24, T21, T19, appC_out_gag(T20, T24, T21)) → U4_GAGG(T20, T24, T21, T19, starA_in_gg(.(T19, T20), T24))
U3_GAGG(T20, T24, T21, T19, appC_out_gag(T20, T24, T21)) → STARA_IN_GG(.(T19, T20), T24)

The TRS R consists of the following rules:

starA_in_gg(T4, []) → starA_out_gg(T4, [])
starA_in_gg(.(T19, T20), .(T19, T21)) → U1_gg(T19, T20, T21, pB_in_gagg(T20, X27, T21, T19))
pB_in_gagg(T20, T24, T21, T19) → U3_gagg(T20, T24, T21, T19, appC_in_gag(T20, T24, T21))
appC_in_gag([], T31, T31) → appC_out_gag([], T31, T31)
appC_in_gag(.(T38, T39), X60, .(T38, T40)) → U2_gag(T38, T39, X60, T40, appC_in_gag(T39, X60, T40))
U2_gag(T38, T39, X60, T40, appC_out_gag(T39, X60, T40)) → appC_out_gag(.(T38, T39), X60, .(T38, T40))
U3_gagg(T20, T24, T21, T19, appC_out_gag(T20, T24, T21)) → U4_gagg(T20, T24, T21, T19, starA_in_gg(.(T19, T20), T24))
U4_gagg(T20, T24, T21, T19, starA_out_gg(.(T19, T20), T24)) → pB_out_gagg(T20, T24, T21, T19)
U1_gg(T19, T20, T21, pB_out_gagg(T20, X27, T21, T19)) → starA_out_gg(.(T19, T20), .(T19, T21))

The argument filtering Pi contains the following mapping:
starA_in_gg(x1, x2)  =  starA_in_gg(x1, x2)
[]  =  []
starA_out_gg(x1, x2)  =  starA_out_gg(x1, x2)
.(x1, x2)  =  .(x1, x2)
U1_gg(x1, x2, x3, x4)  =  U1_gg(x1, x2, x3, x4)
pB_in_gagg(x1, x2, x3, x4)  =  pB_in_gagg(x1, x3, x4)
U3_gagg(x1, x2, x3, x4, x5)  =  U3_gagg(x1, x3, x4, x5)
appC_in_gag(x1, x2, x3)  =  appC_in_gag(x1, x3)
appC_out_gag(x1, x2, x3)  =  appC_out_gag(x1, x2, x3)
U2_gag(x1, x2, x3, x4, x5)  =  U2_gag(x1, x2, x4, x5)
U4_gagg(x1, x2, x3, x4, x5)  =  U4_gagg(x1, x2, x3, x4, x5)
pB_out_gagg(x1, x2, x3, x4)  =  pB_out_gagg(x1, x2, x3, x4)
STARA_IN_GG(x1, x2)  =  STARA_IN_GG(x1, x2)
U1_GG(x1, x2, x3, x4)  =  U1_GG(x1, x2, x3, x4)
PB_IN_GAGG(x1, x2, x3, x4)  =  PB_IN_GAGG(x1, x3, x4)
U3_GAGG(x1, x2, x3, x4, x5)  =  U3_GAGG(x1, x3, x4, x5)
APPC_IN_GAG(x1, x2, x3)  =  APPC_IN_GAG(x1, x3)
U2_GAG(x1, x2, x3, x4, x5)  =  U2_GAG(x1, x2, x4, x5)
U4_GAGG(x1, x2, x3, x4, x5)  =  U4_GAGG(x1, x2, x3, x4, x5)

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

(6) Obligation:

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

STARA_IN_GG(.(T19, T20), .(T19, T21)) → U1_GG(T19, T20, T21, pB_in_gagg(T20, X27, T21, T19))
STARA_IN_GG(.(T19, T20), .(T19, T21)) → PB_IN_GAGG(T20, X27, T21, T19)
PB_IN_GAGG(T20, T24, T21, T19) → U3_GAGG(T20, T24, T21, T19, appC_in_gag(T20, T24, T21))
PB_IN_GAGG(T20, T24, T21, T19) → APPC_IN_GAG(T20, T24, T21)
APPC_IN_GAG(.(T38, T39), X60, .(T38, T40)) → U2_GAG(T38, T39, X60, T40, appC_in_gag(T39, X60, T40))
APPC_IN_GAG(.(T38, T39), X60, .(T38, T40)) → APPC_IN_GAG(T39, X60, T40)
U3_GAGG(T20, T24, T21, T19, appC_out_gag(T20, T24, T21)) → U4_GAGG(T20, T24, T21, T19, starA_in_gg(.(T19, T20), T24))
U3_GAGG(T20, T24, T21, T19, appC_out_gag(T20, T24, T21)) → STARA_IN_GG(.(T19, T20), T24)

The TRS R consists of the following rules:

starA_in_gg(T4, []) → starA_out_gg(T4, [])
starA_in_gg(.(T19, T20), .(T19, T21)) → U1_gg(T19, T20, T21, pB_in_gagg(T20, X27, T21, T19))
pB_in_gagg(T20, T24, T21, T19) → U3_gagg(T20, T24, T21, T19, appC_in_gag(T20, T24, T21))
appC_in_gag([], T31, T31) → appC_out_gag([], T31, T31)
appC_in_gag(.(T38, T39), X60, .(T38, T40)) → U2_gag(T38, T39, X60, T40, appC_in_gag(T39, X60, T40))
U2_gag(T38, T39, X60, T40, appC_out_gag(T39, X60, T40)) → appC_out_gag(.(T38, T39), X60, .(T38, T40))
U3_gagg(T20, T24, T21, T19, appC_out_gag(T20, T24, T21)) → U4_gagg(T20, T24, T21, T19, starA_in_gg(.(T19, T20), T24))
U4_gagg(T20, T24, T21, T19, starA_out_gg(.(T19, T20), T24)) → pB_out_gagg(T20, T24, T21, T19)
U1_gg(T19, T20, T21, pB_out_gagg(T20, X27, T21, T19)) → starA_out_gg(.(T19, T20), .(T19, T21))

The argument filtering Pi contains the following mapping:
starA_in_gg(x1, x2)  =  starA_in_gg(x1, x2)
[]  =  []
starA_out_gg(x1, x2)  =  starA_out_gg(x1, x2)
.(x1, x2)  =  .(x1, x2)
U1_gg(x1, x2, x3, x4)  =  U1_gg(x1, x2, x3, x4)
pB_in_gagg(x1, x2, x3, x4)  =  pB_in_gagg(x1, x3, x4)
U3_gagg(x1, x2, x3, x4, x5)  =  U3_gagg(x1, x3, x4, x5)
appC_in_gag(x1, x2, x3)  =  appC_in_gag(x1, x3)
appC_out_gag(x1, x2, x3)  =  appC_out_gag(x1, x2, x3)
U2_gag(x1, x2, x3, x4, x5)  =  U2_gag(x1, x2, x4, x5)
U4_gagg(x1, x2, x3, x4, x5)  =  U4_gagg(x1, x2, x3, x4, x5)
pB_out_gagg(x1, x2, x3, x4)  =  pB_out_gagg(x1, x2, x3, x4)
STARA_IN_GG(x1, x2)  =  STARA_IN_GG(x1, x2)
U1_GG(x1, x2, x3, x4)  =  U1_GG(x1, x2, x3, x4)
PB_IN_GAGG(x1, x2, x3, x4)  =  PB_IN_GAGG(x1, x3, x4)
U3_GAGG(x1, x2, x3, x4, x5)  =  U3_GAGG(x1, x3, x4, x5)
APPC_IN_GAG(x1, x2, x3)  =  APPC_IN_GAG(x1, x3)
U2_GAG(x1, x2, x3, x4, x5)  =  U2_GAG(x1, x2, x4, x5)
U4_GAGG(x1, x2, x3, x4, x5)  =  U4_GAGG(x1, x2, x3, x4, x5)

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

(7) DependencyGraphProof (EQUIVALENT transformation)

The approximation of the Dependency Graph [LOPSTR] contains 2 SCCs with 4 less nodes.

(8) Complex Obligation (AND)

(9) Obligation:

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

APPC_IN_GAG(.(T38, T39), X60, .(T38, T40)) → APPC_IN_GAG(T39, X60, T40)

The TRS R consists of the following rules:

starA_in_gg(T4, []) → starA_out_gg(T4, [])
starA_in_gg(.(T19, T20), .(T19, T21)) → U1_gg(T19, T20, T21, pB_in_gagg(T20, X27, T21, T19))
pB_in_gagg(T20, T24, T21, T19) → U3_gagg(T20, T24, T21, T19, appC_in_gag(T20, T24, T21))
appC_in_gag([], T31, T31) → appC_out_gag([], T31, T31)
appC_in_gag(.(T38, T39), X60, .(T38, T40)) → U2_gag(T38, T39, X60, T40, appC_in_gag(T39, X60, T40))
U2_gag(T38, T39, X60, T40, appC_out_gag(T39, X60, T40)) → appC_out_gag(.(T38, T39), X60, .(T38, T40))
U3_gagg(T20, T24, T21, T19, appC_out_gag(T20, T24, T21)) → U4_gagg(T20, T24, T21, T19, starA_in_gg(.(T19, T20), T24))
U4_gagg(T20, T24, T21, T19, starA_out_gg(.(T19, T20), T24)) → pB_out_gagg(T20, T24, T21, T19)
U1_gg(T19, T20, T21, pB_out_gagg(T20, X27, T21, T19)) → starA_out_gg(.(T19, T20), .(T19, T21))

The argument filtering Pi contains the following mapping:
starA_in_gg(x1, x2)  =  starA_in_gg(x1, x2)
[]  =  []
starA_out_gg(x1, x2)  =  starA_out_gg(x1, x2)
.(x1, x2)  =  .(x1, x2)
U1_gg(x1, x2, x3, x4)  =  U1_gg(x1, x2, x3, x4)
pB_in_gagg(x1, x2, x3, x4)  =  pB_in_gagg(x1, x3, x4)
U3_gagg(x1, x2, x3, x4, x5)  =  U3_gagg(x1, x3, x4, x5)
appC_in_gag(x1, x2, x3)  =  appC_in_gag(x1, x3)
appC_out_gag(x1, x2, x3)  =  appC_out_gag(x1, x2, x3)
U2_gag(x1, x2, x3, x4, x5)  =  U2_gag(x1, x2, x4, x5)
U4_gagg(x1, x2, x3, x4, x5)  =  U4_gagg(x1, x2, x3, x4, x5)
pB_out_gagg(x1, x2, x3, x4)  =  pB_out_gagg(x1, x2, x3, x4)
APPC_IN_GAG(x1, x2, x3)  =  APPC_IN_GAG(x1, x3)

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

(10) UsableRulesProof (EQUIVALENT transformation)

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

(11) Obligation:

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

APPC_IN_GAG(.(T38, T39), X60, .(T38, T40)) → APPC_IN_GAG(T39, X60, T40)

R is empty.
The argument filtering Pi contains the following mapping:
.(x1, x2)  =  .(x1, x2)
APPC_IN_GAG(x1, x2, x3)  =  APPC_IN_GAG(x1, x3)

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

(12) PiDPToQDPProof (SOUND transformation)

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

(13) Obligation:

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

APPC_IN_GAG(.(T38, T39), .(T38, T40)) → APPC_IN_GAG(T39, T40)

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

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

• APPC_IN_GAG(.(T38, T39), .(T38, T40)) → APPC_IN_GAG(T39, T40)
  The graph contains the following edges 1 > 1, 2 > 2

(15) YES

(16) Obligation:

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

STARA_IN_GG(.(T19, T20), .(T19, T21)) → PB_IN_GAGG(T20, X27, T21, T19)
PB_IN_GAGG(T20, T24, T21, T19) → U3_GAGG(T20, T24, T21, T19, appC_in_gag(T20, T24, T21))
U3_GAGG(T20, T24, T21, T19, appC_out_gag(T20, T24, T21)) → STARA_IN_GG(.(T19, T20), T24)

The TRS R consists of the following rules:

starA_in_gg(T4, []) → starA_out_gg(T4, [])
starA_in_gg(.(T19, T20), .(T19, T21)) → U1_gg(T19, T20, T21, pB_in_gagg(T20, X27, T21, T19))
pB_in_gagg(T20, T24, T21, T19) → U3_gagg(T20, T24, T21, T19, appC_in_gag(T20, T24, T21))
appC_in_gag([], T31, T31) → appC_out_gag([], T31, T31)
appC_in_gag(.(T38, T39), X60, .(T38, T40)) → U2_gag(T38, T39, X60, T40, appC_in_gag(T39, X60, T40))
U2_gag(T38, T39, X60, T40, appC_out_gag(T39, X60, T40)) → appC_out_gag(.(T38, T39), X60, .(T38, T40))
U3_gagg(T20, T24, T21, T19, appC_out_gag(T20, T24, T21)) → U4_gagg(T20, T24, T21, T19, starA_in_gg(.(T19, T20), T24))
U4_gagg(T20, T24, T21, T19, starA_out_gg(.(T19, T20), T24)) → pB_out_gagg(T20, T24, T21, T19)
U1_gg(T19, T20, T21, pB_out_gagg(T20, X27, T21, T19)) → starA_out_gg(.(T19, T20), .(T19, T21))

The argument filtering Pi contains the following mapping:
starA_in_gg(x1, x2)  =  starA_in_gg(x1, x2)
[]  =  []
starA_out_gg(x1, x2)  =  starA_out_gg(x1, x2)
.(x1, x2)  =  .(x1, x2)
U1_gg(x1, x2, x3, x4)  =  U1_gg(x1, x2, x3, x4)
pB_in_gagg(x1, x2, x3, x4)  =  pB_in_gagg(x1, x3, x4)
U3_gagg(x1, x2, x3, x4, x5)  =  U3_gagg(x1, x3, x4, x5)
appC_in_gag(x1, x2, x3)  =  appC_in_gag(x1, x3)
appC_out_gag(x1, x2, x3)  =  appC_out_gag(x1, x2, x3)
U2_gag(x1, x2, x3, x4, x5)  =  U2_gag(x1, x2, x4, x5)
U4_gagg(x1, x2, x3, x4, x5)  =  U4_gagg(x1, x2, x3, x4, x5)
pB_out_gagg(x1, x2, x3, x4)  =  pB_out_gagg(x1, x2, x3, x4)
STARA_IN_GG(x1, x2)  =  STARA_IN_GG(x1, x2)
PB_IN_GAGG(x1, x2, x3, x4)  =  PB_IN_GAGG(x1, x3, x4)
U3_GAGG(x1, x2, x3, x4, x5)  =  U3_GAGG(x1, x3, x4, x5)

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

(17) UsableRulesProof (EQUIVALENT transformation)

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

(18) Obligation:

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

STARA_IN_GG(.(T19, T20), .(T19, T21)) → PB_IN_GAGG(T20, X27, T21, T19)
PB_IN_GAGG(T20, T24, T21, T19) → U3_GAGG(T20, T24, T21, T19, appC_in_gag(T20, T24, T21))
U3_GAGG(T20, T24, T21, T19, appC_out_gag(T20, T24, T21)) → STARA_IN_GG(.(T19, T20), T24)

The TRS R consists of the following rules:

appC_in_gag([], T31, T31) → appC_out_gag([], T31, T31)
appC_in_gag(.(T38, T39), X60, .(T38, T40)) → U2_gag(T38, T39, X60, T40, appC_in_gag(T39, X60, T40))
U2_gag(T38, T39, X60, T40, appC_out_gag(T39, X60, T40)) → appC_out_gag(.(T38, T39), X60, .(T38, T40))

The argument filtering Pi contains the following mapping:
[]  =  []
.(x1, x2)  =  .(x1, x2)
appC_in_gag(x1, x2, x3)  =  appC_in_gag(x1, x3)
appC_out_gag(x1, x2, x3)  =  appC_out_gag(x1, x2, x3)
U2_gag(x1, x2, x3, x4, x5)  =  U2_gag(x1, x2, x4, x5)
STARA_IN_GG(x1, x2)  =  STARA_IN_GG(x1, x2)
PB_IN_GAGG(x1, x2, x3, x4)  =  PB_IN_GAGG(x1, x3, x4)
U3_GAGG(x1, x2, x3, x4, x5)  =  U3_GAGG(x1, x3, x4, x5)

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

(19) PiDPToQDPProof (SOUND transformation)

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

(20) Obligation:

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

STARA_IN_GG(.(T19, T20), .(T19, T21)) → PB_IN_GAGG(T20, T21, T19)
PB_IN_GAGG(T20, T21, T19) → U3_GAGG(T20, T21, T19, appC_in_gag(T20, T21))
U3_GAGG(T20, T21, T19, appC_out_gag(T20, T24, T21)) → STARA_IN_GG(.(T19, T20), T24)

The TRS R consists of the following rules:

appC_in_gag([], T31) → appC_out_gag([], T31, T31)
appC_in_gag(.(T38, T39), .(T38, T40)) → U2_gag(T38, T39, T40, appC_in_gag(T39, T40))
U2_gag(T38, T39, T40, appC_out_gag(T39, X60, T40)) → appC_out_gag(.(T38, T39), X60, .(T38, T40))

The set Q consists of the following terms:

appC_in_gag(x0, x1)
U2_gag(x0, x1, x2, x3)

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

(21) QDPOrderProof (EQUIVALENT transformation)

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

The following pairs can be oriented strictly and are deleted.

PB_IN_GAGG(T20, T21, T19) → U3_GAGG(T20, T21, T19, appC_in_gag(T20, T21))

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

POL(.(x₁, x₂)) = 1 + x₂   
POL(PB_IN_GAGG(x₁, x₂, x₃)) = 1 + x₂   
POL(STARA_IN_GG(x₁, x₂)) = x₂   
POL(U2_gag(x₁, x₂, x₃, x₄)) = 1 + x₄   
POL(U3_GAGG(x₁, x₂, x₃, x₄)) = x₄   
POL([]) = 0   
POL(appC_in_gag(x₁, x₂)) = x₂   
POL(appC_out_gag(x₁, x₂, x₃)) = x₁ + x₂   

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

appC_in_gag([], T31) → appC_out_gag([], T31, T31)
appC_in_gag(.(T38, T39), .(T38, T40)) → U2_gag(T38, T39, T40, appC_in_gag(T39, T40))
U2_gag(T38, T39, T40, appC_out_gag(T39, X60, T40)) → appC_out_gag(.(T38, T39), X60, .(T38, T40))

(22) Obligation:

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

STARA_IN_GG(.(T19, T20), .(T19, T21)) → PB_IN_GAGG(T20, T21, T19)
U3_GAGG(T20, T21, T19, appC_out_gag(T20, T24, T21)) → STARA_IN_GG(.(T19, T20), T24)

The TRS R consists of the following rules:

appC_in_gag([], T31) → appC_out_gag([], T31, T31)
appC_in_gag(.(T38, T39), .(T38, T40)) → U2_gag(T38, T39, T40, appC_in_gag(T39, T40))
U2_gag(T38, T39, T40, appC_out_gag(T39, X60, T40)) → appC_out_gag(.(T38, T39), X60, .(T38, T40))

The set Q consists of the following terms:

appC_in_gag(x0, x1)
U2_gag(x0, x1, x2, x3)

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

(23) DependencyGraphProof (EQUIVALENT transformation)

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

(24) TRUE