Left Termination proof of /tmp/tmpP3zKvS/inorder-oi.pl

Left Termination of the query pattern in_order_in_2(a, 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 AND

    ↳9 PiDP

        ↳10 UsableRulesProof (⇔)

            ↳11 PiDP

                ↳12 PiDPToQDPProof (⇐)

                    ↳13 QDP

                        ↳14 QDPSizeChangeProof (⇔)

                            ↳15 TRUE

    ↳16 PiDP

        ↳17 UsableRulesProof (⇔)

            ↳18 PiDP

                ↳19 PiDPToQDPProof (⇐)

                    ↳20 QDP

                        ↳21 QDPSizeChangeProof (⇔)

                            ↳22 TRUE

    ↳23 PiDP

        ↳24 PiDPToQDPProof (⇐)

            ↳25 QDP

                ↳26 QDPOrderProof (⇔)

                    ↳27 QDP

                        ↳28 DependencyGraphProof (⇔)

                            ↳29 TRUE

(0) Obligation:

Clauses:

in_order(void, L) :- ','(!, eq(L, [])).
in_order(T, Xs) :- ','(value(T, X), ','(app(Ls, .(X, Rs), Xs), ','(left(T, L), ','(in_order(L, Ls), ','(right(T, R), in_order(R, Rs)))))).
app([], X, X).
app(.(X, Xs), Ys, .(X, Zs)) :- app(Xs, Ys, Zs).
left(void, void).
left(node(L, X1, X2), L).
right(void, void).
right(node(X3, X4, R), R).
value(void, X5).
value(node(X6, X, X7), X).
eq(X, X).

Queries:

in_order(a,g).

(1) PrologToPrologProblemTransformerProof (SOUND transformation)

Built Prolog problem from termination graph.

digraph dp_graph {
node [outthreshold=100, inthreshold=100];
1 [label="1: in_order(T1, T2)\n\nT2 is ground", fontsize=16, style=filled, fillcolor=lightyellow, color=red];
2 [label="2: in_order(T1, T2), SCOPE: 1, CLAUSE: 0 | in_order(T1, T2), SCOPE: 1, CLAUSE: 1 | ?_1\n\nT2 is ground", fontsize=16, style=filled, fillcolor=lightyellow];
3 [label="3: ','(!_1, eq(T3, [])) | in_order(T1, T3), SCOPE: 1, CLAUSE: 1 | ?_1\n\nT3 is ground", fontsize=16, style=filled, fillcolor=lightyellow];
4 [label="4: in_order(T1, T2), SCOPE: 1, CLAUSE: 1\n\nT2 is ground\nX9 is free; \nin_order(T1, T2) !=? in_order(void, X9)", fontsize=16, style=filled, fillcolor=lightyellow];
5 [label="5: eq(T3, [])\n\nT3 is ground", fontsize=16, style=filled, fillcolor=lightyellow];
6 [label="6: eq(T3, []), SCOPE: 2, CLAUSE: 10\n\nT3 is ground", fontsize=16, style=filled, fillcolor=lightyellow];
7 [label="7: true\n\n", fontsize=16, style=filled, fillcolor=lightyellow];
8 [label="8: \n\nX11 is free", fontsize=16, style=filled, fillcolor=lightyellow];
9 [label="9: \n\n", fontsize=16, style=filled, fillcolor=lightyellow];
10 [label="10: ','(value(T7, X16), ','(app(X17, .(X16, X18), T6), ','(left(T7, X19), ','(in_order(X19, X17), ','(right(T7, X20), in_order(X20, X18))))))\n\nT6 is ground\nX9 is free; \nX16 is free; \nX17 is free; \nX18 is free; \nX19 is free; \nX20 is free; ", fontsize=16, style=filled, fillcolor=lightyellow];
11 [label="11: ','(value(T7, X16), ','(app(X17, .(X16, X18), T6), ','(left(T7, X19), ','(in_order(X19, X17), ','(right(T7, X20), in_order(X20, X18)))))), SCOPE: 3, CLAUSE: 8 | ','(value(T7, X16), ','(app(X17, .(X16, X18), T6), ','(left(T7, X19), ','(in_order(X19, X17), ','(right(T7, X20), in_order(X20, X18)))))), SCOPE: 3, CLAUSE: 9\n\nT6 is ground\nX16 is free; \nX17 is free; \nX18 is free; \nX19 is free; \nX20 is free; ", fontsize=16, style=filled, fillcolor=lightyellow];
12 [label="12: ','(app(X17, .(X23, X18), T6), ','(left(void, X19), ','(in_order(X19, X17), ','(right(void, X20), in_order(X20, X18))))) | ','(value(T7, X16), ','(app(X17, .(X16, X18), T6), ','(left(T7, X19), ','(in_order(X19, X17), ','(right(T7, X20), in_order(X20, X18)))))), SCOPE: 3, CLAUSE: 9\n\nT6 is ground\nX16 is free; \nX17 is free; \nX18 is free; \nX19 is free; \nX20 is free; \nX23 is free; ", fontsize=16, style=filled, fillcolor=lightyellow];
13 [label="13: ','(value(T7, X16), ','(app(X17, .(X16, X18), T6), ','(left(T7, X19), ','(in_order(X19, X17), ','(right(T7, X20), in_order(X20, X18)))))), SCOPE: 3, CLAUSE: 9\n\nT6 is ground\nX16 is free; \nX17 is free; \nX18 is free; \nX19 is free; \nX20 is free; \nX22 is free; \nvalue(T7, X16) !=? value(void, X22)", fontsize=16, style=filled, fillcolor=lightyellow];
14 [label="14: ','(app(X17, .(X23, X18), T6), ','(left(void, X19), ','(in_order(X19, X17), ','(right(void, X20), in_order(X20, X18)))))\n\nT6 is ground\nX17 is free; \nX18 is free; \nX19 is free; \nX20 is free; \nX23 is free; ", fontsize=16, style=filled, fillcolor=lightyellow];
15 [label="15: ','(value(T7, X16), ','(app(X17, .(X16, X18), T6), ','(left(T7, X19), ','(in_order(X19, X17), ','(right(T7, X20), in_order(X20, X18)))))), SCOPE: 3, CLAUSE: 9\n\nT6 is ground\nX16 is free; \nX17 is free; \nX18 is free; \nX19 is free; \nX20 is free; ", fontsize=16, style=filled, fillcolor=lightyellow];
16 [label="16: app(X17, .(X23, X18), T6)\n\nT6 is ground\nX17 is free; \nX18 is free; \nX23 is free; ", fontsize=16, style=filled, fillcolor=lightyellow];
17 [label="17: ','(left(void, X19), ','(in_order(X19, T8), ','(right(void, X20), in_order(X20, T10))))\n\nT8 is ground\nT10 is ground\nX19 is free; \nX20 is free; ", fontsize=16, style=filled, fillcolor=lightyellow];
18 [label="18: app(X17, .(X23, X18), T6), SCOPE: 4, CLAUSE: 2 | app(X17, .(X23, X18), T6), SCOPE: 4, CLAUSE: 3\n\nT6 is ground\nX17 is free; \nX18 is free; \nX23 is free; ", fontsize=16, style=filled, fillcolor=lightyellow];
19 [label="19: app(X17, .(X23, X18), T6), SCOPE: 4, CLAUSE: 2\n\nT6 is ground\nX17 is free; \nX18 is free; \nX23 is free; ", fontsize=16, style=filled, fillcolor=lightyellow];
20 [label="20: app(X17, .(X23, X18), T6), SCOPE: 4, CLAUSE: 3\n\nT6 is ground\nX17 is free; \nX18 is free; \nX23 is free; ", fontsize=16, style=filled, fillcolor=lightyellow];
21 [label="21: true\n\n", fontsize=16, style=filled, fillcolor=lightyellow];
22 [label="22: \n\nX17 is free\nX18 is free; \nX23 is free; \nX26 is free; ", fontsize=16, style=filled, fillcolor=lightyellow];
23 [label="23: \n\n", fontsize=16, style=filled, fillcolor=lightyellow];
24 [label="24: app(X38, .(X39, X40), T11)\n\nT11 is ground\nX38 is free; \nX39 is free; \nX40 is free; ", fontsize=16, style=filled, fillcolor=lightyellow];
25 [label="25: \n\nX17 is free\nX18 is free; \nX23 is free; \nX33 is free; \nX34 is free; \nX35 is free; \nX36 is free; ", fontsize=16, style=filled, fillcolor=lightyellow];
26 [label="26: ','(left(void, X19), ','(in_order(X19, T8), ','(right(void, X20), in_order(X20, T10)))), SCOPE: 5, CLAUSE: 4 | ','(left(void, X19), ','(in_order(X19, T8), ','(right(void, X20), in_order(X20, T10)))), SCOPE: 5, CLAUSE: 5\n\nT8 is ground\nT10 is ground\nX19 is free; \nX20 is free; ", fontsize=16, style=filled, fillcolor=lightyellow];
27 [label="27: ','(in_order(void, T8), ','(right(void, X20), in_order(X20, T10))) | ','(left(void, X19), ','(in_order(X19, T8), ','(right(void, X20), in_order(X20, T10)))), SCOPE: 5, CLAUSE: 5\n\nT8 is ground\nT10 is ground\nX19 is free; \nX20 is free; ", fontsize=16, style=filled, fillcolor=lightyellow];
28 [label="28: ','(in_order(void, T8), ','(right(void, X20), in_order(X20, T10)))\n\nT8 is ground\nT10 is ground\nX20 is free; ", fontsize=16, style=filled, fillcolor=lightyellow];
29 [label="29: ','(left(void, X19), ','(in_order(X19, T8), ','(right(void, X20), in_order(X20, T10)))), SCOPE: 5, CLAUSE: 5\n\nT8 is ground\nT10 is ground\nX19 is free; \nX20 is free; ", fontsize=16, style=filled, fillcolor=lightyellow];
30 [label="30: in_order(void, T8)\n\nT8 is ground", fontsize=16, style=filled, fillcolor=lightyellow];
31 [label="31: ','(right(void, X20), in_order(X20, T10))\n\nT10 is ground\nX20 is free; ", fontsize=16, style=filled, fillcolor=lightyellow];
32 [label="32: in_order(void, T8), SCOPE: 6, CLAUSE: 0 | in_order(void, T8), SCOPE: 6, CLAUSE: 1 | ?_6\n\nT8 is ground", fontsize=16, style=filled, fillcolor=lightyellow];
33 [label="33: ','(!_6, eq(T12, [])) | in_order(void, T12), SCOPE: 6, CLAUSE: 1 | ?_6\n\nT12 is ground", fontsize=16, style=filled, fillcolor=lightyellow];
34 [label="34: eq(T12, [])\n\nT12 is ground", fontsize=16, style=filled, fillcolor=lightyellow];
35 [label="35: eq(T12, []), SCOPE: 7, CLAUSE: 10\n\nT12 is ground", fontsize=16, style=filled, fillcolor=lightyellow];
36 [label="36: true\n\n", fontsize=16, style=filled, fillcolor=lightyellow];
37 [label="37: \n\nX44 is free", fontsize=16, style=filled, fillcolor=lightyellow];
38 [label="38: \n\n", fontsize=16, style=filled, fillcolor=lightyellow];
39 [label="39: ','(right(void, X20), in_order(X20, T10)), SCOPE: 8, CLAUSE: 6 | ','(right(void, X20), in_order(X20, T10)), SCOPE: 8, CLAUSE: 7\n\nT10 is ground\nX20 is free; ", fontsize=16, style=filled, fillcolor=lightyellow];
40 [label="40: in_order(void, T10) | ','(right(void, X20), in_order(X20, T10)), SCOPE: 8, CLAUSE: 7\n\nT10 is ground\nX20 is free; ", fontsize=16, style=filled, fillcolor=lightyellow];
41 [label="41: in_order(void, T10)\n\nT10 is ground", fontsize=16, style=filled, fillcolor=lightyellow];
42 [label="42: ','(right(void, X20), in_order(X20, T10)), SCOPE: 8, CLAUSE: 7\n\nT10 is ground\nX20 is free; ", fontsize=16, style=filled, fillcolor=lightyellow];
43 [label="43: \n\n", fontsize=16, style=filled, fillcolor=lightyellow];
44 [label="44: \n\n", fontsize=16, style=filled, fillcolor=lightyellow];
45 [label="45: ','(app(X17, .(T17, X18), T6), ','(left(node(T18, T17, T19), X19), ','(in_order(X19, X17), ','(right(node(T18, T17, T19), X20), in_order(X20, X18)))))\n\nT6 is ground\nX17 is free; \nX18 is free; \nX19 is free; \nX20 is free; ", fontsize=16, style=filled, fillcolor=lightyellow];
46 [label="46: \n\nX16 is free\nX54 is free; \nX55 is free; \nX56 is free; ", fontsize=16, style=filled, fillcolor=lightyellow];
47 [label="47: app(X17, .(T17, X18), T6)\n\nT6 is ground\nX17 is free; \nX18 is free; ", fontsize=16, style=filled, fillcolor=lightyellow];
48 [label="48: ','(left(node(T22, T23, T24), X19), ','(in_order(X19, T20), ','(right(node(T22, T23, T24), X20), in_order(X20, T21))))\n\nT20 is ground\nT23 is ground\nT21 is ground\nX19 is free; \nX20 is free; ", fontsize=16, style=filled, fillcolor=lightyellow];
49 [label="49: app(X17, .(T17, X18), T6), SCOPE: 9, CLAUSE: 2 | app(X17, .(T17, X18), T6), SCOPE: 9, CLAUSE: 3\n\nT6 is ground\nX17 is free; \nX18 is free; ", fontsize=16, style=filled, fillcolor=lightyellow];
50 [label="50: app(X17, .(T17, X18), T6), SCOPE: 9, CLAUSE: 2\n\nT6 is ground\nX17 is free; \nX18 is free; ", fontsize=16, style=filled, fillcolor=lightyellow];
51 [label="51: app(X17, .(T17, X18), T6), SCOPE: 9, CLAUSE: 3\n\nT6 is ground\nX17 is free; \nX18 is free; ", fontsize=16, style=filled, fillcolor=lightyellow];
52 [label="52: true\n\n", fontsize=16, style=filled, fillcolor=lightyellow];
53 [label="53: \n\nX17 is free\nX18 is free; \nX59 is free; ", fontsize=16, style=filled, fillcolor=lightyellow];
54 [label="54: \n\n", fontsize=16, style=filled, fillcolor=lightyellow];
55 [label="55: app(X70, .(T28, X71), T27)\n\nT27 is ground\nX70 is free; \nX71 is free; ", fontsize=16, style=filled, fillcolor=lightyellow];
56 [label="56: \n\nX17 is free\nX18 is free; \nX65 is free; \nX66 is free; \nX67 is free; \nX68 is free; ", fontsize=16, style=filled, fillcolor=lightyellow];
57 [label="57: ','(left(node(T22, T23, T24), X19), ','(in_order(X19, T20), ','(right(node(T22, T23, T24), X20), in_order(X20, T21)))), SCOPE: 10, CLAUSE: 4 | ','(left(node(T22, T23, T24), X19), ','(in_order(X19, T20), ','(right(node(T22, T23, T24), X20), in_order(X20, T21)))), SCOPE: 10, CLAUSE: 5\n\nT20 is ground\nT23 is ground\nT21 is ground\nX19 is free; \nX20 is free; ", fontsize=16, style=filled, fillcolor=lightyellow];
58 [label="58: ','(left(node(T22, T23, T24), X19), ','(in_order(X19, T20), ','(right(node(T22, T23, T24), X20), in_order(X20, T21)))), SCOPE: 10, CLAUSE: 5\n\nT20 is ground\nT23 is ground\nT21 is ground\nX19 is free; \nX20 is free; ", fontsize=16, style=filled, fillcolor=lightyellow];
59 [label="59: ','(in_order(T32, T20), ','(right(node(T32, T30, T33), X20), in_order(X20, T21)))\n\nT20 is ground\nT21 is ground\nT30 is ground\nX20 is free; ", fontsize=16, style=filled, fillcolor=lightyellow];
60 [label="60: in_order(T32, T20)\n\nT20 is ground", fontsize=16, style=filled, fillcolor=lightyellow];
61 [label="61: ','(right(node(T34, T30, T35), X20), in_order(X20, T21))\n\nT21 is ground\nT30 is ground\nX20 is free; ", fontsize=16, style=filled, fillcolor=lightyellow];
62 [label="62: ','(right(node(T34, T30, T35), X20), in_order(X20, T21)), SCOPE: 11, CLAUSE: 6 | ','(right(node(T34, T30, T35), X20), in_order(X20, T21)), SCOPE: 11, CLAUSE: 7\n\nT21 is ground\nT30 is ground\nX20 is free; ", fontsize=16, style=filled, fillcolor=lightyellow];
63 [label="63: ','(right(node(T34, T30, T35), X20), in_order(X20, T21)), SCOPE: 11, CLAUSE: 7\n\nT21 is ground\nT30 is ground\nX20 is free; ", fontsize=16, style=filled, fillcolor=lightyellow];
64 [label="64: in_order(T39, T21)\n\nT21 is ground", fontsize=16, style=filled, fillcolor=lightyellow];
65 [label="65: ','(app(X17, .(T43, X18), T6), ','(left(node(T44, T43, T45), X19), ','(in_order(X19, X17), ','(right(node(T44, T43, T45), X20), in_order(X20, X18)))))\n\nT6 is ground\nX16 is free; \nX17 is free; \nX18 is free; \nX19 is free; \nX20 is free; \nX22 is free; ", fontsize=16, style=filled, fillcolor=lightyellow];
66 [label="66: \n\nX16 is free\nX22 is free; \nX87 is free; \nX88 is free; \nX89 is free; ", fontsize=16, style=filled, fillcolor=lightyellow];
67 [label="CASE", fontsize=14, style = filled, fillcolor = lightcyan];
1 -> 67 [arrowhead = none ];
67 -> 2;

68 [label="EVAL with clause\nin_order(void, X9) :- ','(!, eq(X9, [])).\nand substitution\nT1 -> void\nT2 -> T3\nX9 -> T3", fontsize=14, style = filled, fillcolor = lightblue];
2 -> 68 [arrowhead = none ];
68 -> 3;

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

70 [label="CUT", fontsize=14, style = filled, fillcolor = lightgreen];
3 -> 70 [arrowhead = none ];
70 -> 5;

71 [label="EVAL with clause\nin_order(X14, X15) :- ','(value(X14, X16), ','(app(X17, .(X16, X18), X15), ','(left(X14, X19), ','(in_order(X19, X17), ','(right(X14, X20), in_order(X20, X18)))))).\nand substitution\nT1 -> T7\nX14 -> T7\nT2 -> T6\nX15 -> T6\nT5 -> T7", fontsize=14, style = filled, fillcolor = lightblue];
4 -> 71 [arrowhead = none ];
71 -> 10;

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

73 [label="EVAL with clause\neq(X11, X11).\nand substitution\nT3 -> []\nX11 -> []\nT4 -> []", fontsize=14, style = filled, fillcolor = lightblue];
6 -> 73 [arrowhead = none ];
73 -> 7;

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

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

76 [label="CASE", fontsize=14, style = filled, fillcolor = lightcyan];
10 -> 76 [arrowhead = none ];
76 -> 11;

77 [label="EVAL with clause\nvalue(void, X22).\nand substitution\nT7 -> void\nX16 -> X23\nX22 -> X23", fontsize=14, style = filled, fillcolor = lightblue];
11 -> 77 [arrowhead = none ];
77 -> 12;

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

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

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

81 [label="EVAL with clause\nvalue(node(X87, X88, X89), X88).\nand substitution\nX87 -> T44\nX88 -> T43\nX89 -> T45\nT7 -> node(T44, T43, T45)\nX16 -> T43\nT41 -> T43\nT40 -> T44\nT42 -> T45", fontsize=14, style = filled, fillcolor = lightblue];
13 -> 81 [arrowhead = none ];
81 -> 65;

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

83 [label="SPLIT 1", fontsize=14, style = filled, fillcolor = violet];
14 -> 83 [arrowhead = none ];
83 -> 16;

84 [label="SPLIT 2\nnew knowledge:\nT8 is ground\nT9 is ground\nT10 is ground\nreplacements:\nX17 -> T8\nX23 -> T9\nX18 -> T10", fontsize=14, style = filled, fillcolor = violet];
14 -> 84 [arrowhead = none ];
84 -> 17;

85 [label="EVAL with clause\nvalue(node(X54, X55, X56), X55).\nand substitution\nX54 -> T18\nX55 -> T17\nX56 -> T19\nT7 -> node(T18, T17, T19)\nX16 -> T17\nT15 -> T17\nT14 -> T18\nT16 -> T19", fontsize=14, style = filled, fillcolor = lightblue];
15 -> 85 [arrowhead = none ];
85 -> 45;

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

87 [label="CASE", fontsize=14, style = filled, fillcolor = lightcyan];
16 -> 87 [arrowhead = none ];
87 -> 18;

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

89 [label="PARALLEL", fontsize=14, style = filled, fillcolor = violet];
18 -> 89 [arrowhead = none ];
89 -> 19;

90 [label="PARALLEL", fontsize=14, style = filled, fillcolor = violet];
18 -> 90 [arrowhead = none ];
90 -> 20;

91 [label="EVAL with clause\napp([], X26, X26).\nand substitution\nX17 -> []\nX23 -> X27\nX18 -> X28\nX26 -> .(X27, X28)\nT6 -> .(X27, X28)", fontsize=14, style = filled, fillcolor = lightblue];
19 -> 91 [arrowhead = none ];
91 -> 21;

92 [label="EVAL-BACKTRACK", fontsize=14, style = filled, fillcolor = lightblue];
19 -> 92 [arrowhead = none ];
92 -> 22;

93 [label="EVAL with clause\napp(.(X33, X34), X35, .(X33, X36)) :- app(X34, X35, X36).\nand substitution\nX33 -> X37\nX34 -> X38\nX17 -> .(X37, X38)\nX23 -> X39\nX18 -> X40\nX35 -> .(X39, X40)\nX36 -> T11\nT6 -> .(X37, T11)", fontsize=14, style = filled, fillcolor = lightblue];
20 -> 93 [arrowhead = none ];
93 -> 24;

94 [label="EVAL-BACKTRACK", fontsize=14, style = filled, fillcolor = lightblue];
20 -> 94 [arrowhead = none ];
94 -> 25;

95 [label="SUCCESS", fontsize=14, style = filled, fillcolor = lightgreen];
21 -> 95 [arrowhead = none ];
95 -> 23;

96 [label="INSTANCE with matching:\nX17 -> X38\nX23 -> X39\nX18 -> X40\nT6 -> T11", fontsize=14, style = filled, fillcolor = lightgrey];
24 -> 96 [arrowhead = none , style=dashed];
96 -> 16[style=dashed];

97 [label="EVAL with clause\nleft(void, void).\nand substitution\nX19 -> void", fontsize=14, style = filled, fillcolor = lightblue];
26 -> 97 [arrowhead = none ];
97 -> 27;

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

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

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

101 [label="SPLIT 2", fontsize=14, style = filled, fillcolor = violet];
28 -> 101 [arrowhead = none ];
101 -> 31;

102 [label="BACKTRACK\nfor clause: left(node(L, X1, X2), L)because of non-unification", fontsize=14, style = filled, fillcolor = white];
29 -> 102 [arrowhead = none ];
102 -> 44;

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

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

105 [label="EVAL with clause\nin_order(void, X42) :- ','(!, eq(X42, [])).\nand substitution\nT8 -> T12\nX42 -> T12", fontsize=14, style = filled, fillcolor = lightblue];
32 -> 105 [arrowhead = none ];
105 -> 33;

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

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

108 [label="EVAL with clause\neq(X44, X44).\nand substitution\nT12 -> []\nX44 -> []\nT13 -> []", fontsize=14, style = filled, fillcolor = lightblue];
35 -> 108 [arrowhead = none ];
108 -> 36;

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

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

111 [label="EVAL with clause\nright(void, void).\nand substitution\nX20 -> void", fontsize=14, style = filled, fillcolor = lightblue];
39 -> 111 [arrowhead = none ];
111 -> 40;

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

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

114 [label="INSTANCE with matching:\nT8 -> T10", fontsize=14, style = filled, fillcolor = lightgrey];
41 -> 114 [arrowhead = none , style=dashed];
114 -> 30[style=dashed];

115 [label="BACKTRACK\nfor clause: right(node(X3, X4, R), R)because of non-unification", fontsize=14, style = filled, fillcolor = white];
42 -> 115 [arrowhead = none ];
115 -> 43;

116 [label="SPLIT 1", fontsize=14, style = filled, fillcolor = violet];
45 -> 116 [arrowhead = none ];
116 -> 47;

117 [label="SPLIT 2\nnew knowledge:\nT20 is ground\nT23 is ground\nT21 is ground\nreplacements:\nX17 -> T20\nX18 -> T21\nT18 -> T22\nT17 -> T23\nT19 -> T24", fontsize=14, style = filled, fillcolor = violet];
45 -> 117 [arrowhead = none ];
117 -> 48;

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

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

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

121 [label="PARALLEL", fontsize=14, style = filled, fillcolor = violet];
49 -> 121 [arrowhead = none ];
121 -> 51;

122 [label="EVAL with clause\napp([], X59, X59).\nand substitution\nX17 -> []\nT17 -> T25\nX18 -> X60\nX59 -> .(T25, X60)\nT6 -> .(T25, X60)", fontsize=14, style = filled, fillcolor = lightblue];
50 -> 122 [arrowhead = none ];
122 -> 52;

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

124 [label="EVAL with clause\napp(.(X65, X66), X67, .(X65, X68)) :- app(X66, X67, X68).\nand substitution\nX65 -> X69\nX66 -> X70\nX17 -> .(X69, X70)\nT17 -> T28\nX18 -> X71\nX67 -> .(T28, X71)\nX68 -> T27\nT6 -> .(X69, T27)\nT26 -> T28", fontsize=14, style = filled, fillcolor = lightblue];
51 -> 124 [arrowhead = none ];
124 -> 55;

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

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

127 [label="INSTANCE with matching:\nX17 -> X70\nT17 -> T28\nX18 -> X71\nT6 -> T27", fontsize=14, style = filled, fillcolor = lightgrey];
55 -> 127 [arrowhead = none , style=dashed];
127 -> 47[style=dashed];

128 [label="BACKTRACK\nfor clause: left(void, void)because of non-unification", fontsize=14, style = filled, fillcolor = white];
57 -> 128 [arrowhead = none ];
128 -> 58;

129 [label="EVAL with clause\nleft(node(X75, X76, X77), X75).\nand substitution\nT22 -> T32\nX75 -> T32\nT23 -> T30\nX76 -> T30\nT24 -> T33\nX77 -> T33\nX19 -> T32\nT29 -> T32\nT31 -> T33", fontsize=14, style = filled, fillcolor = lightblue];
58 -> 129 [arrowhead = none ];
129 -> 59;

130 [label="SPLIT 1", fontsize=14, style = filled, fillcolor = violet];
59 -> 130 [arrowhead = none ];
130 -> 60;

131 [label="SPLIT 2\nreplacements:\nT32 -> T34\nT33 -> T35", fontsize=14, style = filled, fillcolor = violet];
59 -> 131 [arrowhead = none ];
131 -> 61;

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

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

134 [label="BACKTRACK\nfor clause: right(void, void)because of non-unification", fontsize=14, style = filled, fillcolor = white];
62 -> 134 [arrowhead = none ];
134 -> 63;

135 [label="EVAL with clause\nright(node(X81, X82, X83), X83).\nand substitution\nT34 -> T36\nX81 -> T36\nT30 -> T37\nX82 -> T37\nT35 -> T39\nX83 -> T39\nX20 -> T39\nT38 -> T39", fontsize=14, style = filled, fillcolor = lightblue];
63 -> 135 [arrowhead = none ];
135 -> 64;

136 [label="INSTANCE with matching:\nT1 -> T39\nT2 -> T21", fontsize=14, style = filled, fillcolor = lightgrey];
64 -> 136 [arrowhead = none , style=dashed];
136 -> 1[style=dashed];

137 [label="INSTANCE with matching:\nT17 -> T43\nT18 -> T44\nT19 -> T45", fontsize=14, style = filled, fillcolor = lightgrey];
65 -> 137 [arrowhead = none , style=dashed];
137 -> 45[style=dashed];

}

(2) Obligation:

Clauses:

app16([], X27, X28, .(X27, X28)).
app16(.(X37, X38), X39, X40, .(X37, T11)) :- app16(X38, X39, X40, T11).
in_order30([]).
app47([], T25, X60, .(T25, X60)).
app47(.(X69, X70), T28, X71, .(X69, T27)) :- app47(X70, T28, X71, T27).
in_order1(void, []).
in_order1(void, T6) :- app16(X17, X23, X18, T6).
in_order1(void, T6) :- ','(app16(T8, T9, T10, T6), in_order30(T8)).
in_order1(void, T6) :- ','(app16(T8, T9, T10, T6), ','(in_order30(T8), in_order30(T10))).
in_order1(node(T18, T17, T19), T6) :- app47(X17, T17, X18, T6).
in_order1(node(T32, T30, T33), T6) :- ','(app47(T20, T30, T21, T6), in_order1(T32, T20)).
in_order1(node(T36, T37, T39), T6) :- ','(app47(T20, T37, T21, T6), ','(in_order1(T36, T20), in_order1(T39, T21))).
in_order1(node(T44, T43, T45), T6) :- p45(X17, T43, X18, T6, T44, T45, X19, X20).
p45(X17, T17, X18, T6, T18, T19, X19, X20) :- app47(X17, T17, X18, T6).
p45(T20, T30, T21, T6, T32, T33, T32, X20) :- ','(app47(T20, T30, T21, T6), in_order1(T32, T20)).
p45(T20, T37, T21, T6, T36, T39, T36, T39) :- ','(app47(T20, T37, T21, T6), ','(in_order1(T36, T20), in_order1(T39, T21))).

Queries:

in_order1(a,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:
in_order1_in: (f,b)
app16_in: (f,f,f,b)
app47_in: (f,f,f,b)
p45_in: (f,f,f,b,f,f,f,f)
Transforming Prolog into the following Term Rewriting System:
Pi-finite rewrite system:
The TRS R consists of the following rules:

in_order1_in_ag(void, []) → in_order1_out_ag(void, [])
in_order1_in_ag(void, T6) → U3_ag(T6, app16_in_aaag(X17, X23, X18, T6))
app16_in_aaag([], X27, X28, .(X27, X28)) → app16_out_aaag([], X27, X28, .(X27, X28))
app16_in_aaag(.(X37, X38), X39, X40, .(X37, T11)) → U1_aaag(X37, X38, X39, X40, T11, app16_in_aaag(X38, X39, X40, T11))
U1_aaag(X37, X38, X39, X40, T11, app16_out_aaag(X38, X39, X40, T11)) → app16_out_aaag(.(X37, X38), X39, X40, .(X37, T11))
U3_ag(T6, app16_out_aaag(X17, X23, X18, T6)) → in_order1_out_ag(void, T6)
in_order1_in_ag(void, T6) → U4_ag(T6, app16_in_aaag(T8, T9, T10, T6))
U4_ag(T6, app16_out_aaag(T8, T9, T10, T6)) → U5_ag(T6, T10, in_order30_in_g(T8))
in_order30_in_g([]) → in_order30_out_g([])
U5_ag(T6, T10, in_order30_out_g(T8)) → in_order1_out_ag(void, T6)
U5_ag(T6, T10, in_order30_out_g(T8)) → U6_ag(T6, in_order30_in_g(T10))
U6_ag(T6, in_order30_out_g(T10)) → in_order1_out_ag(void, T6)
in_order1_in_ag(node(T18, T17, T19), T6) → U7_ag(T18, T17, T19, T6, app47_in_aaag(X17, T17, X18, T6))
app47_in_aaag([], T25, X60, .(T25, X60)) → app47_out_aaag([], T25, X60, .(T25, X60))
app47_in_aaag(.(X69, X70), T28, X71, .(X69, T27)) → U2_aaag(X69, X70, T28, X71, T27, app47_in_aaag(X70, T28, X71, T27))
U2_aaag(X69, X70, T28, X71, T27, app47_out_aaag(X70, T28, X71, T27)) → app47_out_aaag(.(X69, X70), T28, X71, .(X69, T27))
U7_ag(T18, T17, T19, T6, app47_out_aaag(X17, T17, X18, T6)) → in_order1_out_ag(node(T18, T17, T19), T6)
in_order1_in_ag(node(T32, T30, T33), T6) → U8_ag(T32, T30, T33, T6, app47_in_aaag(T20, T30, T21, T6))
U8_ag(T32, T30, T33, T6, app47_out_aaag(T20, T30, T21, T6)) → U9_ag(T32, T30, T33, T6, in_order1_in_ag(T32, T20))
in_order1_in_ag(node(T36, T37, T39), T6) → U10_ag(T36, T37, T39, T6, app47_in_aaag(T20, T37, T21, T6))
U10_ag(T36, T37, T39, T6, app47_out_aaag(T20, T37, T21, T6)) → U11_ag(T36, T37, T39, T6, T21, in_order1_in_ag(T36, T20))
in_order1_in_ag(node(T44, T43, T45), T6) → U13_ag(T44, T43, T45, T6, p45_in_aaagaaaa(X17, T43, X18, T6, T44, T45, X19, X20))
p45_in_aaagaaaa(X17, T17, X18, T6, T18, T19, X19, X20) → U14_aaagaaaa(X17, T17, X18, T6, T18, T19, X19, X20, app47_in_aaag(X17, T17, X18, T6))
U14_aaagaaaa(X17, T17, X18, T6, T18, T19, X19, X20, app47_out_aaag(X17, T17, X18, T6)) → p45_out_aaagaaaa(X17, T17, X18, T6, T18, T19, X19, X20)
p45_in_aaagaaaa(T20, T30, T21, T6, T32, T33, T32, X20) → U15_aaagaaaa(T20, T30, T21, T6, T32, T33, X20, app47_in_aaag(T20, T30, T21, T6))
U15_aaagaaaa(T20, T30, T21, T6, T32, T33, X20, app47_out_aaag(T20, T30, T21, T6)) → U16_aaagaaaa(T20, T30, T21, T6, T32, T33, X20, in_order1_in_ag(T32, T20))
U16_aaagaaaa(T20, T30, T21, T6, T32, T33, X20, in_order1_out_ag(T32, T20)) → p45_out_aaagaaaa(T20, T30, T21, T6, T32, T33, T32, X20)
p45_in_aaagaaaa(T20, T37, T21, T6, T36, T39, T36, T39) → U17_aaagaaaa(T20, T37, T21, T6, T36, T39, app47_in_aaag(T20, T37, T21, T6))
U17_aaagaaaa(T20, T37, T21, T6, T36, T39, app47_out_aaag(T20, T37, T21, T6)) → U18_aaagaaaa(T20, T37, T21, T6, T36, T39, in_order1_in_ag(T36, T20))
U18_aaagaaaa(T20, T37, T21, T6, T36, T39, in_order1_out_ag(T36, T20)) → U19_aaagaaaa(T20, T37, T21, T6, T36, T39, in_order1_in_ag(T39, T21))
U19_aaagaaaa(T20, T37, T21, T6, T36, T39, in_order1_out_ag(T39, T21)) → p45_out_aaagaaaa(T20, T37, T21, T6, T36, T39, T36, T39)
U13_ag(T44, T43, T45, T6, p45_out_aaagaaaa(X17, T43, X18, T6, T44, T45, X19, X20)) → in_order1_out_ag(node(T44, T43, T45), T6)
U11_ag(T36, T37, T39, T6, T21, in_order1_out_ag(T36, T20)) → U12_ag(T36, T37, T39, T6, in_order1_in_ag(T39, T21))
U12_ag(T36, T37, T39, T6, in_order1_out_ag(T39, T21)) → in_order1_out_ag(node(T36, T37, T39), T6)
U9_ag(T32, T30, T33, T6, in_order1_out_ag(T32, T20)) → in_order1_out_ag(node(T32, T30, T33), T6)

Infinitary Constructor Rewriting Termination of PiTRS implies Termination of Prolog

(4) Obligation:

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

in_order1_in_ag(void, []) → in_order1_out_ag(void, [])
in_order1_in_ag(void, T6) → U3_ag(T6, app16_in_aaag(X17, X23, X18, T6))
app16_in_aaag([], X27, X28, .(X27, X28)) → app16_out_aaag([], X27, X28, .(X27, X28))
app16_in_aaag(.(X37, X38), X39, X40, .(X37, T11)) → U1_aaag(X37, X38, X39, X40, T11, app16_in_aaag(X38, X39, X40, T11))
U1_aaag(X37, X38, X39, X40, T11, app16_out_aaag(X38, X39, X40, T11)) → app16_out_aaag(.(X37, X38), X39, X40, .(X37, T11))
U3_ag(T6, app16_out_aaag(X17, X23, X18, T6)) → in_order1_out_ag(void, T6)
in_order1_in_ag(void, T6) → U4_ag(T6, app16_in_aaag(T8, T9, T10, T6))
U4_ag(T6, app16_out_aaag(T8, T9, T10, T6)) → U5_ag(T6, T10, in_order30_in_g(T8))
in_order30_in_g([]) → in_order30_out_g([])
U5_ag(T6, T10, in_order30_out_g(T8)) → in_order1_out_ag(void, T6)
U5_ag(T6, T10, in_order30_out_g(T8)) → U6_ag(T6, in_order30_in_g(T10))
U6_ag(T6, in_order30_out_g(T10)) → in_order1_out_ag(void, T6)
in_order1_in_ag(node(T18, T17, T19), T6) → U7_ag(T18, T17, T19, T6, app47_in_aaag(X17, T17, X18, T6))
app47_in_aaag([], T25, X60, .(T25, X60)) → app47_out_aaag([], T25, X60, .(T25, X60))
app47_in_aaag(.(X69, X70), T28, X71, .(X69, T27)) → U2_aaag(X69, X70, T28, X71, T27, app47_in_aaag(X70, T28, X71, T27))
U2_aaag(X69, X70, T28, X71, T27, app47_out_aaag(X70, T28, X71, T27)) → app47_out_aaag(.(X69, X70), T28, X71, .(X69, T27))
U7_ag(T18, T17, T19, T6, app47_out_aaag(X17, T17, X18, T6)) → in_order1_out_ag(node(T18, T17, T19), T6)
in_order1_in_ag(node(T32, T30, T33), T6) → U8_ag(T32, T30, T33, T6, app47_in_aaag(T20, T30, T21, T6))
U8_ag(T32, T30, T33, T6, app47_out_aaag(T20, T30, T21, T6)) → U9_ag(T32, T30, T33, T6, in_order1_in_ag(T32, T20))
in_order1_in_ag(node(T36, T37, T39), T6) → U10_ag(T36, T37, T39, T6, app47_in_aaag(T20, T37, T21, T6))
U10_ag(T36, T37, T39, T6, app47_out_aaag(T20, T37, T21, T6)) → U11_ag(T36, T37, T39, T6, T21, in_order1_in_ag(T36, T20))
in_order1_in_ag(node(T44, T43, T45), T6) → U13_ag(T44, T43, T45, T6, p45_in_aaagaaaa(X17, T43, X18, T6, T44, T45, X19, X20))
p45_in_aaagaaaa(X17, T17, X18, T6, T18, T19, X19, X20) → U14_aaagaaaa(X17, T17, X18, T6, T18, T19, X19, X20, app47_in_aaag(X17, T17, X18, T6))
U14_aaagaaaa(X17, T17, X18, T6, T18, T19, X19, X20, app47_out_aaag(X17, T17, X18, T6)) → p45_out_aaagaaaa(X17, T17, X18, T6, T18, T19, X19, X20)
p45_in_aaagaaaa(T20, T30, T21, T6, T32, T33, T32, X20) → U15_aaagaaaa(T20, T30, T21, T6, T32, T33, X20, app47_in_aaag(T20, T30, T21, T6))
U15_aaagaaaa(T20, T30, T21, T6, T32, T33, X20, app47_out_aaag(T20, T30, T21, T6)) → U16_aaagaaaa(T20, T30, T21, T6, T32, T33, X20, in_order1_in_ag(T32, T20))
U16_aaagaaaa(T20, T30, T21, T6, T32, T33, X20, in_order1_out_ag(T32, T20)) → p45_out_aaagaaaa(T20, T30, T21, T6, T32, T33, T32, X20)
p45_in_aaagaaaa(T20, T37, T21, T6, T36, T39, T36, T39) → U17_aaagaaaa(T20, T37, T21, T6, T36, T39, app47_in_aaag(T20, T37, T21, T6))
U17_aaagaaaa(T20, T37, T21, T6, T36, T39, app47_out_aaag(T20, T37, T21, T6)) → U18_aaagaaaa(T20, T37, T21, T6, T36, T39, in_order1_in_ag(T36, T20))
U18_aaagaaaa(T20, T37, T21, T6, T36, T39, in_order1_out_ag(T36, T20)) → U19_aaagaaaa(T20, T37, T21, T6, T36, T39, in_order1_in_ag(T39, T21))
U19_aaagaaaa(T20, T37, T21, T6, T36, T39, in_order1_out_ag(T39, T21)) → p45_out_aaagaaaa(T20, T37, T21, T6, T36, T39, T36, T39)
U13_ag(T44, T43, T45, T6, p45_out_aaagaaaa(X17, T43, X18, T6, T44, T45, X19, X20)) → in_order1_out_ag(node(T44, T43, T45), T6)
U11_ag(T36, T37, T39, T6, T21, in_order1_out_ag(T36, T20)) → U12_ag(T36, T37, T39, T6, in_order1_in_ag(T39, T21))
U12_ag(T36, T37, T39, T6, in_order1_out_ag(T39, T21)) → in_order1_out_ag(node(T36, T37, T39), T6)
U9_ag(T32, T30, T33, T6, in_order1_out_ag(T32, T20)) → in_order1_out_ag(node(T32, T30, T33), T6)

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

IN_ORDER1_IN_AG(void, T6) → U3_AG(T6, app16_in_aaag(X17, X23, X18, T6))
IN_ORDER1_IN_AG(void, T6) → APP16_IN_AAAG(X17, X23, X18, T6)
APP16_IN_AAAG(.(X37, X38), X39, X40, .(X37, T11)) → U1_AAAG(X37, X38, X39, X40, T11, app16_in_aaag(X38, X39, X40, T11))
APP16_IN_AAAG(.(X37, X38), X39, X40, .(X37, T11)) → APP16_IN_AAAG(X38, X39, X40, T11)
IN_ORDER1_IN_AG(void, T6) → U4_AG(T6, app16_in_aaag(T8, T9, T10, T6))
U4_AG(T6, app16_out_aaag(T8, T9, T10, T6)) → U5_AG(T6, T10, in_order30_in_g(T8))
U4_AG(T6, app16_out_aaag(T8, T9, T10, T6)) → IN_ORDER30_IN_G(T8)
U5_AG(T6, T10, in_order30_out_g(T8)) → U6_AG(T6, in_order30_in_g(T10))
U5_AG(T6, T10, in_order30_out_g(T8)) → IN_ORDER30_IN_G(T10)
IN_ORDER1_IN_AG(node(T18, T17, T19), T6) → U7_AG(T18, T17, T19, T6, app47_in_aaag(X17, T17, X18, T6))
IN_ORDER1_IN_AG(node(T18, T17, T19), T6) → APP47_IN_AAAG(X17, T17, X18, T6)
APP47_IN_AAAG(.(X69, X70), T28, X71, .(X69, T27)) → U2_AAAG(X69, X70, T28, X71, T27, app47_in_aaag(X70, T28, X71, T27))
APP47_IN_AAAG(.(X69, X70), T28, X71, .(X69, T27)) → APP47_IN_AAAG(X70, T28, X71, T27)
IN_ORDER1_IN_AG(node(T32, T30, T33), T6) → U8_AG(T32, T30, T33, T6, app47_in_aaag(T20, T30, T21, T6))
U8_AG(T32, T30, T33, T6, app47_out_aaag(T20, T30, T21, T6)) → U9_AG(T32, T30, T33, T6, in_order1_in_ag(T32, T20))
U8_AG(T32, T30, T33, T6, app47_out_aaag(T20, T30, T21, T6)) → IN_ORDER1_IN_AG(T32, T20)
IN_ORDER1_IN_AG(node(T36, T37, T39), T6) → U10_AG(T36, T37, T39, T6, app47_in_aaag(T20, T37, T21, T6))
U10_AG(T36, T37, T39, T6, app47_out_aaag(T20, T37, T21, T6)) → U11_AG(T36, T37, T39, T6, T21, in_order1_in_ag(T36, T20))
U10_AG(T36, T37, T39, T6, app47_out_aaag(T20, T37, T21, T6)) → IN_ORDER1_IN_AG(T36, T20)
IN_ORDER1_IN_AG(node(T44, T43, T45), T6) → U13_AG(T44, T43, T45, T6, p45_in_aaagaaaa(X17, T43, X18, T6, T44, T45, X19, X20))
IN_ORDER1_IN_AG(node(T44, T43, T45), T6) → P45_IN_AAAGAAAA(X17, T43, X18, T6, T44, T45, X19, X20)
P45_IN_AAAGAAAA(X17, T17, X18, T6, T18, T19, X19, X20) → U14_AAAGAAAA(X17, T17, X18, T6, T18, T19, X19, X20, app47_in_aaag(X17, T17, X18, T6))
P45_IN_AAAGAAAA(X17, T17, X18, T6, T18, T19, X19, X20) → APP47_IN_AAAG(X17, T17, X18, T6)
P45_IN_AAAGAAAA(T20, T30, T21, T6, T32, T33, T32, X20) → U15_AAAGAAAA(T20, T30, T21, T6, T32, T33, X20, app47_in_aaag(T20, T30, T21, T6))
P45_IN_AAAGAAAA(T20, T30, T21, T6, T32, T33, T32, X20) → APP47_IN_AAAG(T20, T30, T21, T6)
U15_AAAGAAAA(T20, T30, T21, T6, T32, T33, X20, app47_out_aaag(T20, T30, T21, T6)) → U16_AAAGAAAA(T20, T30, T21, T6, T32, T33, X20, in_order1_in_ag(T32, T20))
U15_AAAGAAAA(T20, T30, T21, T6, T32, T33, X20, app47_out_aaag(T20, T30, T21, T6)) → IN_ORDER1_IN_AG(T32, T20)
P45_IN_AAAGAAAA(T20, T37, T21, T6, T36, T39, T36, T39) → U17_AAAGAAAA(T20, T37, T21, T6, T36, T39, app47_in_aaag(T20, T37, T21, T6))
P45_IN_AAAGAAAA(T20, T37, T21, T6, T36, T39, T36, T39) → APP47_IN_AAAG(T20, T37, T21, T6)
U17_AAAGAAAA(T20, T37, T21, T6, T36, T39, app47_out_aaag(T20, T37, T21, T6)) → U18_AAAGAAAA(T20, T37, T21, T6, T36, T39, in_order1_in_ag(T36, T20))
U17_AAAGAAAA(T20, T37, T21, T6, T36, T39, app47_out_aaag(T20, T37, T21, T6)) → IN_ORDER1_IN_AG(T36, T20)
U18_AAAGAAAA(T20, T37, T21, T6, T36, T39, in_order1_out_ag(T36, T20)) → U19_AAAGAAAA(T20, T37, T21, T6, T36, T39, in_order1_in_ag(T39, T21))
U18_AAAGAAAA(T20, T37, T21, T6, T36, T39, in_order1_out_ag(T36, T20)) → IN_ORDER1_IN_AG(T39, T21)
U11_AG(T36, T37, T39, T6, T21, in_order1_out_ag(T36, T20)) → U12_AG(T36, T37, T39, T6, in_order1_in_ag(T39, T21))
U11_AG(T36, T37, T39, T6, T21, in_order1_out_ag(T36, T20)) → IN_ORDER1_IN_AG(T39, T21)

The TRS R consists of the following rules:

in_order1_in_ag(void, []) → in_order1_out_ag(void, [])
in_order1_in_ag(void, T6) → U3_ag(T6, app16_in_aaag(X17, X23, X18, T6))
app16_in_aaag([], X27, X28, .(X27, X28)) → app16_out_aaag([], X27, X28, .(X27, X28))
app16_in_aaag(.(X37, X38), X39, X40, .(X37, T11)) → U1_aaag(X37, X38, X39, X40, T11, app16_in_aaag(X38, X39, X40, T11))
U1_aaag(X37, X38, X39, X40, T11, app16_out_aaag(X38, X39, X40, T11)) → app16_out_aaag(.(X37, X38), X39, X40, .(X37, T11))
U3_ag(T6, app16_out_aaag(X17, X23, X18, T6)) → in_order1_out_ag(void, T6)
in_order1_in_ag(void, T6) → U4_ag(T6, app16_in_aaag(T8, T9, T10, T6))
U4_ag(T6, app16_out_aaag(T8, T9, T10, T6)) → U5_ag(T6, T10, in_order30_in_g(T8))
in_order30_in_g([]) → in_order30_out_g([])
U5_ag(T6, T10, in_order30_out_g(T8)) → in_order1_out_ag(void, T6)
U5_ag(T6, T10, in_order30_out_g(T8)) → U6_ag(T6, in_order30_in_g(T10))
U6_ag(T6, in_order30_out_g(T10)) → in_order1_out_ag(void, T6)
in_order1_in_ag(node(T18, T17, T19), T6) → U7_ag(T18, T17, T19, T6, app47_in_aaag(X17, T17, X18, T6))
app47_in_aaag([], T25, X60, .(T25, X60)) → app47_out_aaag([], T25, X60, .(T25, X60))
app47_in_aaag(.(X69, X70), T28, X71, .(X69, T27)) → U2_aaag(X69, X70, T28, X71, T27, app47_in_aaag(X70, T28, X71, T27))
U2_aaag(X69, X70, T28, X71, T27, app47_out_aaag(X70, T28, X71, T27)) → app47_out_aaag(.(X69, X70), T28, X71, .(X69, T27))
U7_ag(T18, T17, T19, T6, app47_out_aaag(X17, T17, X18, T6)) → in_order1_out_ag(node(T18, T17, T19), T6)
in_order1_in_ag(node(T32, T30, T33), T6) → U8_ag(T32, T30, T33, T6, app47_in_aaag(T20, T30, T21, T6))
U8_ag(T32, T30, T33, T6, app47_out_aaag(T20, T30, T21, T6)) → U9_ag(T32, T30, T33, T6, in_order1_in_ag(T32, T20))
in_order1_in_ag(node(T36, T37, T39), T6) → U10_ag(T36, T37, T39, T6, app47_in_aaag(T20, T37, T21, T6))
U10_ag(T36, T37, T39, T6, app47_out_aaag(T20, T37, T21, T6)) → U11_ag(T36, T37, T39, T6, T21, in_order1_in_ag(T36, T20))
in_order1_in_ag(node(T44, T43, T45), T6) → U13_ag(T44, T43, T45, T6, p45_in_aaagaaaa(X17, T43, X18, T6, T44, T45, X19, X20))
p45_in_aaagaaaa(X17, T17, X18, T6, T18, T19, X19, X20) → U14_aaagaaaa(X17, T17, X18, T6, T18, T19, X19, X20, app47_in_aaag(X17, T17, X18, T6))
U14_aaagaaaa(X17, T17, X18, T6, T18, T19, X19, X20, app47_out_aaag(X17, T17, X18, T6)) → p45_out_aaagaaaa(X17, T17, X18, T6, T18, T19, X19, X20)
p45_in_aaagaaaa(T20, T30, T21, T6, T32, T33, T32, X20) → U15_aaagaaaa(T20, T30, T21, T6, T32, T33, X20, app47_in_aaag(T20, T30, T21, T6))
U15_aaagaaaa(T20, T30, T21, T6, T32, T33, X20, app47_out_aaag(T20, T30, T21, T6)) → U16_aaagaaaa(T20, T30, T21, T6, T32, T33, X20, in_order1_in_ag(T32, T20))
U16_aaagaaaa(T20, T30, T21, T6, T32, T33, X20, in_order1_out_ag(T32, T20)) → p45_out_aaagaaaa(T20, T30, T21, T6, T32, T33, T32, X20)
p45_in_aaagaaaa(T20, T37, T21, T6, T36, T39, T36, T39) → U17_aaagaaaa(T20, T37, T21, T6, T36, T39, app47_in_aaag(T20, T37, T21, T6))
U17_aaagaaaa(T20, T37, T21, T6, T36, T39, app47_out_aaag(T20, T37, T21, T6)) → U18_aaagaaaa(T20, T37, T21, T6, T36, T39, in_order1_in_ag(T36, T20))
U18_aaagaaaa(T20, T37, T21, T6, T36, T39, in_order1_out_ag(T36, T20)) → U19_aaagaaaa(T20, T37, T21, T6, T36, T39, in_order1_in_ag(T39, T21))
U19_aaagaaaa(T20, T37, T21, T6, T36, T39, in_order1_out_ag(T39, T21)) → p45_out_aaagaaaa(T20, T37, T21, T6, T36, T39, T36, T39)
U13_ag(T44, T43, T45, T6, p45_out_aaagaaaa(X17, T43, X18, T6, T44, T45, X19, X20)) → in_order1_out_ag(node(T44, T43, T45), T6)
U11_ag(T36, T37, T39, T6, T21, in_order1_out_ag(T36, T20)) → U12_ag(T36, T37, T39, T6, in_order1_in_ag(T39, T21))
U12_ag(T36, T37, T39, T6, in_order1_out_ag(T39, T21)) → in_order1_out_ag(node(T36, T37, T39), T6)
U9_ag(T32, T30, T33, T6, in_order1_out_ag(T32, T20)) → in_order1_out_ag(node(T32, T30, T33), T6)

The argument filtering Pi contains the following mapping:
in_order1_in_ag(x1, x2) = in_order1_in_ag(x2)
[] = []
in_order1_out_ag(x1, x2) = in_order1_out_ag(x2)
U3_ag(x1, x2) = U3_ag(x1, x2)
app16_in_aaag(x1, x2, x3, x4) = app16_in_aaag(x4)
.(x1, x2) = .(x1, x2)
app16_out_aaag(x1, x2, x3, x4) = app16_out_aaag(x1, x2, x3, x4)
U1_aaag(x1, x2, x3, x4, x5, x6) = U1_aaag(x1, x5, x6)
U4_ag(x1, x2) = U4_ag(x1, x2)
U5_ag(x1, x2, x3) = U5_ag(x1, x2, x3)
in_order30_in_g(x1) = in_order30_in_g(x1)
in_order30_out_g(x1) = in_order30_out_g(x1)
U6_ag(x1, x2) = U6_ag(x1, x2)
U7_ag(x1, x2, x3, x4, x5) = U7_ag(x4, x5)
app47_in_aaag(x1, x2, x3, x4) = app47_in_aaag(x4)
app47_out_aaag(x1, x2, x3, x4) = app47_out_aaag(x1, x2, x3, x4)
U2_aaag(x1, x2, x3, x4, x5, x6) = U2_aaag(x1, x5, x6)
U8_ag(x1, x2, x3, x4, x5) = U8_ag(x4, x5)
U9_ag(x1, x2, x3, x4, x5) = U9_ag(x4, x5)
U10_ag(x1, x2, x3, x4, x5) = U10_ag(x4, x5)
U11_ag(x1, x2, x3, x4, x5, x6) = U11_ag(x4, x5, x6)
U13_ag(x1, x2, x3, x4, x5) = U13_ag(x4, x5)
p45_in_aaagaaaa(x1, x2, x3, x4, x5, x6, x7, x8) = p45_in_aaagaaaa(x4)
U14_aaagaaaa(x1, x2, x3, x4, x5, x6, x7, x8, x9) = U14_aaagaaaa(x4, x9)
p45_out_aaagaaaa(x1, x2, x3, x4, x5, x6, x7, x8) = p45_out_aaagaaaa(x1, x2, x3, x4)
U15_aaagaaaa(x1, x2, x3, x4, x5, x6, x7, x8) = U15_aaagaaaa(x4, x8)
U16_aaagaaaa(x1, x2, x3, x4, x5, x6, x7, x8) = U16_aaagaaaa(x1, x2, x3, x4, x8)
U17_aaagaaaa(x1, x2, x3, x4, x5, x6, x7) = U17_aaagaaaa(x4, x7)
U18_aaagaaaa(x1, x2, x3, x4, x5, x6, x7) = U18_aaagaaaa(x1, x2, x3, x4, x7)
U19_aaagaaaa(x1, x2, x3, x4, x5, x6, x7) = U19_aaagaaaa(x1, x2, x3, x4, x7)
U12_ag(x1, x2, x3, x4, x5) = U12_ag(x4, x5)
IN_ORDER1_IN_AG(x1, x2) = IN_ORDER1_IN_AG(x2)
U3_AG(x1, x2) = U3_AG(x1, x2)
APP16_IN_AAAG(x1, x2, x3, x4) = APP16_IN_AAAG(x4)
U1_AAAG(x1, x2, x3, x4, x5, x6) = U1_AAAG(x1, x5, x6)
U4_AG(x1, x2) = U4_AG(x1, x2)
U5_AG(x1, x2, x3) = U5_AG(x1, x2, x3)
IN_ORDER30_IN_G(x1) = IN_ORDER30_IN_G(x1)
U6_AG(x1, x2) = U6_AG(x1, x2)
U7_AG(x1, x2, x3, x4, x5) = U7_AG(x4, x5)
APP47_IN_AAAG(x1, x2, x3, x4) = APP47_IN_AAAG(x4)
U2_AAAG(x1, x2, x3, x4, x5, x6) = U2_AAAG(x1, x5, x6)
U8_AG(x1, x2, x3, x4, x5) = U8_AG(x4, x5)
U9_AG(x1, x2, x3, x4, x5) = U9_AG(x4, x5)
U10_AG(x1, x2, x3, x4, x5) = U10_AG(x4, x5)
U11_AG(x1, x2, x3, x4, x5, x6) = U11_AG(x4, x5, x6)
U13_AG(x1, x2, x3, x4, x5) = U13_AG(x4, x5)
P45_IN_AAAGAAAA(x1, x2, x3, x4, x5, x6, x7, x8) = P45_IN_AAAGAAAA(x4)
U14_AAAGAAAA(x1, x2, x3, x4, x5, x6, x7, x8, x9) = U14_AAAGAAAA(x4, x9)
U15_AAAGAAAA(x1, x2, x3, x4, x5, x6, x7, x8) = U15_AAAGAAAA(x4, x8)
U16_AAAGAAAA(x1, x2, x3, x4, x5, x6, x7, x8) = U16_AAAGAAAA(x1, x2, x3, x4, x8)
U17_AAAGAAAA(x1, x2, x3, x4, x5, x6, x7) = U17_AAAGAAAA(x4, x7)
U18_AAAGAAAA(x1, x2, x3, x4, x5, x6, x7) = U18_AAAGAAAA(x1, x2, x3, x4, x7)
U19_AAAGAAAA(x1, x2, x3, x4, x5, x6, x7) = U19_AAAGAAAA(x1, x2, x3, x4, x7)
U12_AG(x1, x2, x3, x4, x5) = U12_AG(x4, x5)

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

(6) Obligation:

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

IN_ORDER1_IN_AG(void, T6) → U3_AG(T6, app16_in_aaag(X17, X23, X18, T6))
IN_ORDER1_IN_AG(void, T6) → APP16_IN_AAAG(X17, X23, X18, T6)
APP16_IN_AAAG(.(X37, X38), X39, X40, .(X37, T11)) → U1_AAAG(X37, X38, X39, X40, T11, app16_in_aaag(X38, X39, X40, T11))
APP16_IN_AAAG(.(X37, X38), X39, X40, .(X37, T11)) → APP16_IN_AAAG(X38, X39, X40, T11)
IN_ORDER1_IN_AG(void, T6) → U4_AG(T6, app16_in_aaag(T8, T9, T10, T6))
U4_AG(T6, app16_out_aaag(T8, T9, T10, T6)) → U5_AG(T6, T10, in_order30_in_g(T8))
U4_AG(T6, app16_out_aaag(T8, T9, T10, T6)) → IN_ORDER30_IN_G(T8)
U5_AG(T6, T10, in_order30_out_g(T8)) → U6_AG(T6, in_order30_in_g(T10))
U5_AG(T6, T10, in_order30_out_g(T8)) → IN_ORDER30_IN_G(T10)
IN_ORDER1_IN_AG(node(T18, T17, T19), T6) → U7_AG(T18, T17, T19, T6, app47_in_aaag(X17, T17, X18, T6))
IN_ORDER1_IN_AG(node(T18, T17, T19), T6) → APP47_IN_AAAG(X17, T17, X18, T6)
APP47_IN_AAAG(.(X69, X70), T28, X71, .(X69, T27)) → U2_AAAG(X69, X70, T28, X71, T27, app47_in_aaag(X70, T28, X71, T27))
APP47_IN_AAAG(.(X69, X70), T28, X71, .(X69, T27)) → APP47_IN_AAAG(X70, T28, X71, T27)
IN_ORDER1_IN_AG(node(T32, T30, T33), T6) → U8_AG(T32, T30, T33, T6, app47_in_aaag(T20, T30, T21, T6))
U8_AG(T32, T30, T33, T6, app47_out_aaag(T20, T30, T21, T6)) → U9_AG(T32, T30, T33, T6, in_order1_in_ag(T32, T20))
U8_AG(T32, T30, T33, T6, app47_out_aaag(T20, T30, T21, T6)) → IN_ORDER1_IN_AG(T32, T20)
IN_ORDER1_IN_AG(node(T36, T37, T39), T6) → U10_AG(T36, T37, T39, T6, app47_in_aaag(T20, T37, T21, T6))
U10_AG(T36, T37, T39, T6, app47_out_aaag(T20, T37, T21, T6)) → U11_AG(T36, T37, T39, T6, T21, in_order1_in_ag(T36, T20))
U10_AG(T36, T37, T39, T6, app47_out_aaag(T20, T37, T21, T6)) → IN_ORDER1_IN_AG(T36, T20)
IN_ORDER1_IN_AG(node(T44, T43, T45), T6) → U13_AG(T44, T43, T45, T6, p45_in_aaagaaaa(X17, T43, X18, T6, T44, T45, X19, X20))
IN_ORDER1_IN_AG(node(T44, T43, T45), T6) → P45_IN_AAAGAAAA(X17, T43, X18, T6, T44, T45, X19, X20)
P45_IN_AAAGAAAA(X17, T17, X18, T6, T18, T19, X19, X20) → U14_AAAGAAAA(X17, T17, X18, T6, T18, T19, X19, X20, app47_in_aaag(X17, T17, X18, T6))
P45_IN_AAAGAAAA(X17, T17, X18, T6, T18, T19, X19, X20) → APP47_IN_AAAG(X17, T17, X18, T6)
P45_IN_AAAGAAAA(T20, T30, T21, T6, T32, T33, T32, X20) → U15_AAAGAAAA(T20, T30, T21, T6, T32, T33, X20, app47_in_aaag(T20, T30, T21, T6))
P45_IN_AAAGAAAA(T20, T30, T21, T6, T32, T33, T32, X20) → APP47_IN_AAAG(T20, T30, T21, T6)
U15_AAAGAAAA(T20, T30, T21, T6, T32, T33, X20, app47_out_aaag(T20, T30, T21, T6)) → U16_AAAGAAAA(T20, T30, T21, T6, T32, T33, X20, in_order1_in_ag(T32, T20))
U15_AAAGAAAA(T20, T30, T21, T6, T32, T33, X20, app47_out_aaag(T20, T30, T21, T6)) → IN_ORDER1_IN_AG(T32, T20)
P45_IN_AAAGAAAA(T20, T37, T21, T6, T36, T39, T36, T39) → U17_AAAGAAAA(T20, T37, T21, T6, T36, T39, app47_in_aaag(T20, T37, T21, T6))
P45_IN_AAAGAAAA(T20, T37, T21, T6, T36, T39, T36, T39) → APP47_IN_AAAG(T20, T37, T21, T6)
U17_AAAGAAAA(T20, T37, T21, T6, T36, T39, app47_out_aaag(T20, T37, T21, T6)) → U18_AAAGAAAA(T20, T37, T21, T6, T36, T39, in_order1_in_ag(T36, T20))
U17_AAAGAAAA(T20, T37, T21, T6, T36, T39, app47_out_aaag(T20, T37, T21, T6)) → IN_ORDER1_IN_AG(T36, T20)
U18_AAAGAAAA(T20, T37, T21, T6, T36, T39, in_order1_out_ag(T36, T20)) → U19_AAAGAAAA(T20, T37, T21, T6, T36, T39, in_order1_in_ag(T39, T21))
U18_AAAGAAAA(T20, T37, T21, T6, T36, T39, in_order1_out_ag(T36, T20)) → IN_ORDER1_IN_AG(T39, T21)
U11_AG(T36, T37, T39, T6, T21, in_order1_out_ag(T36, T20)) → U12_AG(T36, T37, T39, T6, in_order1_in_ag(T39, T21))
U11_AG(T36, T37, T39, T6, T21, in_order1_out_ag(T36, T20)) → IN_ORDER1_IN_AG(T39, T21)

The TRS R consists of the following rules:

in_order1_in_ag(void, []) → in_order1_out_ag(void, [])
in_order1_in_ag(void, T6) → U3_ag(T6, app16_in_aaag(X17, X23, X18, T6))
app16_in_aaag([], X27, X28, .(X27, X28)) → app16_out_aaag([], X27, X28, .(X27, X28))
app16_in_aaag(.(X37, X38), X39, X40, .(X37, T11)) → U1_aaag(X37, X38, X39, X40, T11, app16_in_aaag(X38, X39, X40, T11))
U1_aaag(X37, X38, X39, X40, T11, app16_out_aaag(X38, X39, X40, T11)) → app16_out_aaag(.(X37, X38), X39, X40, .(X37, T11))
U3_ag(T6, app16_out_aaag(X17, X23, X18, T6)) → in_order1_out_ag(void, T6)
in_order1_in_ag(void, T6) → U4_ag(T6, app16_in_aaag(T8, T9, T10, T6))
U4_ag(T6, app16_out_aaag(T8, T9, T10, T6)) → U5_ag(T6, T10, in_order30_in_g(T8))
in_order30_in_g([]) → in_order30_out_g([])
U5_ag(T6, T10, in_order30_out_g(T8)) → in_order1_out_ag(void, T6)
U5_ag(T6, T10, in_order30_out_g(T8)) → U6_ag(T6, in_order30_in_g(T10))
U6_ag(T6, in_order30_out_g(T10)) → in_order1_out_ag(void, T6)
in_order1_in_ag(node(T18, T17, T19), T6) → U7_ag(T18, T17, T19, T6, app47_in_aaag(X17, T17, X18, T6))
app47_in_aaag([], T25, X60, .(T25, X60)) → app47_out_aaag([], T25, X60, .(T25, X60))
app47_in_aaag(.(X69, X70), T28, X71, .(X69, T27)) → U2_aaag(X69, X70, T28, X71, T27, app47_in_aaag(X70, T28, X71, T27))
U2_aaag(X69, X70, T28, X71, T27, app47_out_aaag(X70, T28, X71, T27)) → app47_out_aaag(.(X69, X70), T28, X71, .(X69, T27))
U7_ag(T18, T17, T19, T6, app47_out_aaag(X17, T17, X18, T6)) → in_order1_out_ag(node(T18, T17, T19), T6)
in_order1_in_ag(node(T32, T30, T33), T6) → U8_ag(T32, T30, T33, T6, app47_in_aaag(T20, T30, T21, T6))
U8_ag(T32, T30, T33, T6, app47_out_aaag(T20, T30, T21, T6)) → U9_ag(T32, T30, T33, T6, in_order1_in_ag(T32, T20))
in_order1_in_ag(node(T36, T37, T39), T6) → U10_ag(T36, T37, T39, T6, app47_in_aaag(T20, T37, T21, T6))
U10_ag(T36, T37, T39, T6, app47_out_aaag(T20, T37, T21, T6)) → U11_ag(T36, T37, T39, T6, T21, in_order1_in_ag(T36, T20))
in_order1_in_ag(node(T44, T43, T45), T6) → U13_ag(T44, T43, T45, T6, p45_in_aaagaaaa(X17, T43, X18, T6, T44, T45, X19, X20))
p45_in_aaagaaaa(X17, T17, X18, T6, T18, T19, X19, X20) → U14_aaagaaaa(X17, T17, X18, T6, T18, T19, X19, X20, app47_in_aaag(X17, T17, X18, T6))
U14_aaagaaaa(X17, T17, X18, T6, T18, T19, X19, X20, app47_out_aaag(X17, T17, X18, T6)) → p45_out_aaagaaaa(X17, T17, X18, T6, T18, T19, X19, X20)
p45_in_aaagaaaa(T20, T30, T21, T6, T32, T33, T32, X20) → U15_aaagaaaa(T20, T30, T21, T6, T32, T33, X20, app47_in_aaag(T20, T30, T21, T6))
U15_aaagaaaa(T20, T30, T21, T6, T32, T33, X20, app47_out_aaag(T20, T30, T21, T6)) → U16_aaagaaaa(T20, T30, T21, T6, T32, T33, X20, in_order1_in_ag(T32, T20))
U16_aaagaaaa(T20, T30, T21, T6, T32, T33, X20, in_order1_out_ag(T32, T20)) → p45_out_aaagaaaa(T20, T30, T21, T6, T32, T33, T32, X20)
p45_in_aaagaaaa(T20, T37, T21, T6, T36, T39, T36, T39) → U17_aaagaaaa(T20, T37, T21, T6, T36, T39, app47_in_aaag(T20, T37, T21, T6))
U17_aaagaaaa(T20, T37, T21, T6, T36, T39, app47_out_aaag(T20, T37, T21, T6)) → U18_aaagaaaa(T20, T37, T21, T6, T36, T39, in_order1_in_ag(T36, T20))
U18_aaagaaaa(T20, T37, T21, T6, T36, T39, in_order1_out_ag(T36, T20)) → U19_aaagaaaa(T20, T37, T21, T6, T36, T39, in_order1_in_ag(T39, T21))
U19_aaagaaaa(T20, T37, T21, T6, T36, T39, in_order1_out_ag(T39, T21)) → p45_out_aaagaaaa(T20, T37, T21, T6, T36, T39, T36, T39)
U13_ag(T44, T43, T45, T6, p45_out_aaagaaaa(X17, T43, X18, T6, T44, T45, X19, X20)) → in_order1_out_ag(node(T44, T43, T45), T6)
U11_ag(T36, T37, T39, T6, T21, in_order1_out_ag(T36, T20)) → U12_ag(T36, T37, T39, T6, in_order1_in_ag(T39, T21))
U12_ag(T36, T37, T39, T6, in_order1_out_ag(T39, T21)) → in_order1_out_ag(node(T36, T37, T39), T6)
U9_ag(T32, T30, T33, T6, in_order1_out_ag(T32, T20)) → in_order1_out_ag(node(T32, T30, T33), T6)

(7) DependencyGraphProof (EQUIVALENT transformation)

The approximation of the Dependency Graph [LOPSTR] contains 3 SCCs with 20 less nodes.

(8) Complex Obligation (AND)

(9) Obligation:

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

APP47_IN_AAAG(.(X69, X70), T28, X71, .(X69, T27)) → APP47_IN_AAAG(X70, T28, X71, T27)

The TRS R consists of the following rules:

in_order1_in_ag(void, []) → in_order1_out_ag(void, [])
in_order1_in_ag(void, T6) → U3_ag(T6, app16_in_aaag(X17, X23, X18, T6))
app16_in_aaag([], X27, X28, .(X27, X28)) → app16_out_aaag([], X27, X28, .(X27, X28))
app16_in_aaag(.(X37, X38), X39, X40, .(X37, T11)) → U1_aaag(X37, X38, X39, X40, T11, app16_in_aaag(X38, X39, X40, T11))
U1_aaag(X37, X38, X39, X40, T11, app16_out_aaag(X38, X39, X40, T11)) → app16_out_aaag(.(X37, X38), X39, X40, .(X37, T11))
U3_ag(T6, app16_out_aaag(X17, X23, X18, T6)) → in_order1_out_ag(void, T6)
in_order1_in_ag(void, T6) → U4_ag(T6, app16_in_aaag(T8, T9, T10, T6))
U4_ag(T6, app16_out_aaag(T8, T9, T10, T6)) → U5_ag(T6, T10, in_order30_in_g(T8))
in_order30_in_g([]) → in_order30_out_g([])
U5_ag(T6, T10, in_order30_out_g(T8)) → in_order1_out_ag(void, T6)
U5_ag(T6, T10, in_order30_out_g(T8)) → U6_ag(T6, in_order30_in_g(T10))
U6_ag(T6, in_order30_out_g(T10)) → in_order1_out_ag(void, T6)
in_order1_in_ag(node(T18, T17, T19), T6) → U7_ag(T18, T17, T19, T6, app47_in_aaag(X17, T17, X18, T6))
app47_in_aaag([], T25, X60, .(T25, X60)) → app47_out_aaag([], T25, X60, .(T25, X60))
app47_in_aaag(.(X69, X70), T28, X71, .(X69, T27)) → U2_aaag(X69, X70, T28, X71, T27, app47_in_aaag(X70, T28, X71, T27))
U2_aaag(X69, X70, T28, X71, T27, app47_out_aaag(X70, T28, X71, T27)) → app47_out_aaag(.(X69, X70), T28, X71, .(X69, T27))
U7_ag(T18, T17, T19, T6, app47_out_aaag(X17, T17, X18, T6)) → in_order1_out_ag(node(T18, T17, T19), T6)
in_order1_in_ag(node(T32, T30, T33), T6) → U8_ag(T32, T30, T33, T6, app47_in_aaag(T20, T30, T21, T6))
U8_ag(T32, T30, T33, T6, app47_out_aaag(T20, T30, T21, T6)) → U9_ag(T32, T30, T33, T6, in_order1_in_ag(T32, T20))
in_order1_in_ag(node(T36, T37, T39), T6) → U10_ag(T36, T37, T39, T6, app47_in_aaag(T20, T37, T21, T6))
U10_ag(T36, T37, T39, T6, app47_out_aaag(T20, T37, T21, T6)) → U11_ag(T36, T37, T39, T6, T21, in_order1_in_ag(T36, T20))
in_order1_in_ag(node(T44, T43, T45), T6) → U13_ag(T44, T43, T45, T6, p45_in_aaagaaaa(X17, T43, X18, T6, T44, T45, X19, X20))
p45_in_aaagaaaa(X17, T17, X18, T6, T18, T19, X19, X20) → U14_aaagaaaa(X17, T17, X18, T6, T18, T19, X19, X20, app47_in_aaag(X17, T17, X18, T6))
U14_aaagaaaa(X17, T17, X18, T6, T18, T19, X19, X20, app47_out_aaag(X17, T17, X18, T6)) → p45_out_aaagaaaa(X17, T17, X18, T6, T18, T19, X19, X20)
p45_in_aaagaaaa(T20, T30, T21, T6, T32, T33, T32, X20) → U15_aaagaaaa(T20, T30, T21, T6, T32, T33, X20, app47_in_aaag(T20, T30, T21, T6))
U15_aaagaaaa(T20, T30, T21, T6, T32, T33, X20, app47_out_aaag(T20, T30, T21, T6)) → U16_aaagaaaa(T20, T30, T21, T6, T32, T33, X20, in_order1_in_ag(T32, T20))
U16_aaagaaaa(T20, T30, T21, T6, T32, T33, X20, in_order1_out_ag(T32, T20)) → p45_out_aaagaaaa(T20, T30, T21, T6, T32, T33, T32, X20)
p45_in_aaagaaaa(T20, T37, T21, T6, T36, T39, T36, T39) → U17_aaagaaaa(T20, T37, T21, T6, T36, T39, app47_in_aaag(T20, T37, T21, T6))
U17_aaagaaaa(T20, T37, T21, T6, T36, T39, app47_out_aaag(T20, T37, T21, T6)) → U18_aaagaaaa(T20, T37, T21, T6, T36, T39, in_order1_in_ag(T36, T20))
U18_aaagaaaa(T20, T37, T21, T6, T36, T39, in_order1_out_ag(T36, T20)) → U19_aaagaaaa(T20, T37, T21, T6, T36, T39, in_order1_in_ag(T39, T21))
U19_aaagaaaa(T20, T37, T21, T6, T36, T39, in_order1_out_ag(T39, T21)) → p45_out_aaagaaaa(T20, T37, T21, T6, T36, T39, T36, T39)
U13_ag(T44, T43, T45, T6, p45_out_aaagaaaa(X17, T43, X18, T6, T44, T45, X19, X20)) → in_order1_out_ag(node(T44, T43, T45), T6)
U11_ag(T36, T37, T39, T6, T21, in_order1_out_ag(T36, T20)) → U12_ag(T36, T37, T39, T6, in_order1_in_ag(T39, T21))
U12_ag(T36, T37, T39, T6, in_order1_out_ag(T39, T21)) → in_order1_out_ag(node(T36, T37, T39), T6)
U9_ag(T32, T30, T33, T6, in_order1_out_ag(T32, T20)) → in_order1_out_ag(node(T32, T30, T33), T6)

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

APP47_IN_AAAG(.(X69, X70), T28, X71, .(X69, T27)) → APP47_IN_AAAG(X70, T28, X71, T27)

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

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:

APP47_IN_AAAG(.(X69, T27)) → APP47_IN_AAAG(T27)

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:

APP47_IN_AAAG(.(X69, T27)) → APP47_IN_AAAG(T27)
The graph contains the following edges 1 > 1

(15) TRUE

(16) Obligation:

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

APP16_IN_AAAG(.(X37, X38), X39, X40, .(X37, T11)) → APP16_IN_AAAG(X38, X39, X40, T11)

The TRS R consists of the following rules:

in_order1_in_ag(void, []) → in_order1_out_ag(void, [])
in_order1_in_ag(void, T6) → U3_ag(T6, app16_in_aaag(X17, X23, X18, T6))
app16_in_aaag([], X27, X28, .(X27, X28)) → app16_out_aaag([], X27, X28, .(X27, X28))
app16_in_aaag(.(X37, X38), X39, X40, .(X37, T11)) → U1_aaag(X37, X38, X39, X40, T11, app16_in_aaag(X38, X39, X40, T11))
U1_aaag(X37, X38, X39, X40, T11, app16_out_aaag(X38, X39, X40, T11)) → app16_out_aaag(.(X37, X38), X39, X40, .(X37, T11))
U3_ag(T6, app16_out_aaag(X17, X23, X18, T6)) → in_order1_out_ag(void, T6)
in_order1_in_ag(void, T6) → U4_ag(T6, app16_in_aaag(T8, T9, T10, T6))
U4_ag(T6, app16_out_aaag(T8, T9, T10, T6)) → U5_ag(T6, T10, in_order30_in_g(T8))
in_order30_in_g([]) → in_order30_out_g([])
U5_ag(T6, T10, in_order30_out_g(T8)) → in_order1_out_ag(void, T6)
U5_ag(T6, T10, in_order30_out_g(T8)) → U6_ag(T6, in_order30_in_g(T10))
U6_ag(T6, in_order30_out_g(T10)) → in_order1_out_ag(void, T6)
in_order1_in_ag(node(T18, T17, T19), T6) → U7_ag(T18, T17, T19, T6, app47_in_aaag(X17, T17, X18, T6))
app47_in_aaag([], T25, X60, .(T25, X60)) → app47_out_aaag([], T25, X60, .(T25, X60))
app47_in_aaag(.(X69, X70), T28, X71, .(X69, T27)) → U2_aaag(X69, X70, T28, X71, T27, app47_in_aaag(X70, T28, X71, T27))
U2_aaag(X69, X70, T28, X71, T27, app47_out_aaag(X70, T28, X71, T27)) → app47_out_aaag(.(X69, X70), T28, X71, .(X69, T27))
U7_ag(T18, T17, T19, T6, app47_out_aaag(X17, T17, X18, T6)) → in_order1_out_ag(node(T18, T17, T19), T6)
in_order1_in_ag(node(T32, T30, T33), T6) → U8_ag(T32, T30, T33, T6, app47_in_aaag(T20, T30, T21, T6))
U8_ag(T32, T30, T33, T6, app47_out_aaag(T20, T30, T21, T6)) → U9_ag(T32, T30, T33, T6, in_order1_in_ag(T32, T20))
in_order1_in_ag(node(T36, T37, T39), T6) → U10_ag(T36, T37, T39, T6, app47_in_aaag(T20, T37, T21, T6))
U10_ag(T36, T37, T39, T6, app47_out_aaag(T20, T37, T21, T6)) → U11_ag(T36, T37, T39, T6, T21, in_order1_in_ag(T36, T20))
in_order1_in_ag(node(T44, T43, T45), T6) → U13_ag(T44, T43, T45, T6, p45_in_aaagaaaa(X17, T43, X18, T6, T44, T45, X19, X20))
p45_in_aaagaaaa(X17, T17, X18, T6, T18, T19, X19, X20) → U14_aaagaaaa(X17, T17, X18, T6, T18, T19, X19, X20, app47_in_aaag(X17, T17, X18, T6))
U14_aaagaaaa(X17, T17, X18, T6, T18, T19, X19, X20, app47_out_aaag(X17, T17, X18, T6)) → p45_out_aaagaaaa(X17, T17, X18, T6, T18, T19, X19, X20)
p45_in_aaagaaaa(T20, T30, T21, T6, T32, T33, T32, X20) → U15_aaagaaaa(T20, T30, T21, T6, T32, T33, X20, app47_in_aaag(T20, T30, T21, T6))
U15_aaagaaaa(T20, T30, T21, T6, T32, T33, X20, app47_out_aaag(T20, T30, T21, T6)) → U16_aaagaaaa(T20, T30, T21, T6, T32, T33, X20, in_order1_in_ag(T32, T20))
U16_aaagaaaa(T20, T30, T21, T6, T32, T33, X20, in_order1_out_ag(T32, T20)) → p45_out_aaagaaaa(T20, T30, T21, T6, T32, T33, T32, X20)
p45_in_aaagaaaa(T20, T37, T21, T6, T36, T39, T36, T39) → U17_aaagaaaa(T20, T37, T21, T6, T36, T39, app47_in_aaag(T20, T37, T21, T6))
U17_aaagaaaa(T20, T37, T21, T6, T36, T39, app47_out_aaag(T20, T37, T21, T6)) → U18_aaagaaaa(T20, T37, T21, T6, T36, T39, in_order1_in_ag(T36, T20))
U18_aaagaaaa(T20, T37, T21, T6, T36, T39, in_order1_out_ag(T36, T20)) → U19_aaagaaaa(T20, T37, T21, T6, T36, T39, in_order1_in_ag(T39, T21))
U19_aaagaaaa(T20, T37, T21, T6, T36, T39, in_order1_out_ag(T39, T21)) → p45_out_aaagaaaa(T20, T37, T21, T6, T36, T39, T36, T39)
U13_ag(T44, T43, T45, T6, p45_out_aaagaaaa(X17, T43, X18, T6, T44, T45, X19, X20)) → in_order1_out_ag(node(T44, T43, T45), T6)
U11_ag(T36, T37, T39, T6, T21, in_order1_out_ag(T36, T20)) → U12_ag(T36, T37, T39, T6, in_order1_in_ag(T39, T21))
U12_ag(T36, T37, T39, T6, in_order1_out_ag(T39, T21)) → in_order1_out_ag(node(T36, T37, T39), T6)
U9_ag(T32, T30, T33, T6, in_order1_out_ag(T32, T20)) → in_order1_out_ag(node(T32, T30, T33), T6)

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

APP16_IN_AAAG(.(X37, X38), X39, X40, .(X37, T11)) → APP16_IN_AAAG(X38, X39, X40, T11)

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

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:

APP16_IN_AAAG(.(X37, T11)) → APP16_IN_AAAG(T11)

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

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

APP16_IN_AAAG(.(X37, T11)) → APP16_IN_AAAG(T11)
The graph contains the following edges 1 > 1

(22) TRUE

(23) Obligation:

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

IN_ORDER1_IN_AG(node(T32, T30, T33), T6) → U8_AG(T32, T30, T33, T6, app47_in_aaag(T20, T30, T21, T6))
U8_AG(T32, T30, T33, T6, app47_out_aaag(T20, T30, T21, T6)) → IN_ORDER1_IN_AG(T32, T20)
IN_ORDER1_IN_AG(node(T36, T37, T39), T6) → U10_AG(T36, T37, T39, T6, app47_in_aaag(T20, T37, T21, T6))
U10_AG(T36, T37, T39, T6, app47_out_aaag(T20, T37, T21, T6)) → U11_AG(T36, T37, T39, T6, T21, in_order1_in_ag(T36, T20))
U11_AG(T36, T37, T39, T6, T21, in_order1_out_ag(T36, T20)) → IN_ORDER1_IN_AG(T39, T21)
IN_ORDER1_IN_AG(node(T44, T43, T45), T6) → P45_IN_AAAGAAAA(X17, T43, X18, T6, T44, T45, X19, X20)
P45_IN_AAAGAAAA(T20, T30, T21, T6, T32, T33, T32, X20) → U15_AAAGAAAA(T20, T30, T21, T6, T32, T33, X20, app47_in_aaag(T20, T30, T21, T6))
U15_AAAGAAAA(T20, T30, T21, T6, T32, T33, X20, app47_out_aaag(T20, T30, T21, T6)) → IN_ORDER1_IN_AG(T32, T20)
P45_IN_AAAGAAAA(T20, T37, T21, T6, T36, T39, T36, T39) → U17_AAAGAAAA(T20, T37, T21, T6, T36, T39, app47_in_aaag(T20, T37, T21, T6))
U17_AAAGAAAA(T20, T37, T21, T6, T36, T39, app47_out_aaag(T20, T37, T21, T6)) → U18_AAAGAAAA(T20, T37, T21, T6, T36, T39, in_order1_in_ag(T36, T20))
U18_AAAGAAAA(T20, T37, T21, T6, T36, T39, in_order1_out_ag(T36, T20)) → IN_ORDER1_IN_AG(T39, T21)
U17_AAAGAAAA(T20, T37, T21, T6, T36, T39, app47_out_aaag(T20, T37, T21, T6)) → IN_ORDER1_IN_AG(T36, T20)
U10_AG(T36, T37, T39, T6, app47_out_aaag(T20, T37, T21, T6)) → IN_ORDER1_IN_AG(T36, T20)

The TRS R consists of the following rules:

in_order1_in_ag(void, []) → in_order1_out_ag(void, [])
in_order1_in_ag(void, T6) → U3_ag(T6, app16_in_aaag(X17, X23, X18, T6))
app16_in_aaag([], X27, X28, .(X27, X28)) → app16_out_aaag([], X27, X28, .(X27, X28))
app16_in_aaag(.(X37, X38), X39, X40, .(X37, T11)) → U1_aaag(X37, X38, X39, X40, T11, app16_in_aaag(X38, X39, X40, T11))
U1_aaag(X37, X38, X39, X40, T11, app16_out_aaag(X38, X39, X40, T11)) → app16_out_aaag(.(X37, X38), X39, X40, .(X37, T11))
U3_ag(T6, app16_out_aaag(X17, X23, X18, T6)) → in_order1_out_ag(void, T6)
in_order1_in_ag(void, T6) → U4_ag(T6, app16_in_aaag(T8, T9, T10, T6))
U4_ag(T6, app16_out_aaag(T8, T9, T10, T6)) → U5_ag(T6, T10, in_order30_in_g(T8))
in_order30_in_g([]) → in_order30_out_g([])
U5_ag(T6, T10, in_order30_out_g(T8)) → in_order1_out_ag(void, T6)
U5_ag(T6, T10, in_order30_out_g(T8)) → U6_ag(T6, in_order30_in_g(T10))
U6_ag(T6, in_order30_out_g(T10)) → in_order1_out_ag(void, T6)
in_order1_in_ag(node(T18, T17, T19), T6) → U7_ag(T18, T17, T19, T6, app47_in_aaag(X17, T17, X18, T6))
app47_in_aaag([], T25, X60, .(T25, X60)) → app47_out_aaag([], T25, X60, .(T25, X60))
app47_in_aaag(.(X69, X70), T28, X71, .(X69, T27)) → U2_aaag(X69, X70, T28, X71, T27, app47_in_aaag(X70, T28, X71, T27))
U2_aaag(X69, X70, T28, X71, T27, app47_out_aaag(X70, T28, X71, T27)) → app47_out_aaag(.(X69, X70), T28, X71, .(X69, T27))
U7_ag(T18, T17, T19, T6, app47_out_aaag(X17, T17, X18, T6)) → in_order1_out_ag(node(T18, T17, T19), T6)
in_order1_in_ag(node(T32, T30, T33), T6) → U8_ag(T32, T30, T33, T6, app47_in_aaag(T20, T30, T21, T6))
U8_ag(T32, T30, T33, T6, app47_out_aaag(T20, T30, T21, T6)) → U9_ag(T32, T30, T33, T6, in_order1_in_ag(T32, T20))
in_order1_in_ag(node(T36, T37, T39), T6) → U10_ag(T36, T37, T39, T6, app47_in_aaag(T20, T37, T21, T6))
U10_ag(T36, T37, T39, T6, app47_out_aaag(T20, T37, T21, T6)) → U11_ag(T36, T37, T39, T6, T21, in_order1_in_ag(T36, T20))
in_order1_in_ag(node(T44, T43, T45), T6) → U13_ag(T44, T43, T45, T6, p45_in_aaagaaaa(X17, T43, X18, T6, T44, T45, X19, X20))
p45_in_aaagaaaa(X17, T17, X18, T6, T18, T19, X19, X20) → U14_aaagaaaa(X17, T17, X18, T6, T18, T19, X19, X20, app47_in_aaag(X17, T17, X18, T6))
U14_aaagaaaa(X17, T17, X18, T6, T18, T19, X19, X20, app47_out_aaag(X17, T17, X18, T6)) → p45_out_aaagaaaa(X17, T17, X18, T6, T18, T19, X19, X20)
p45_in_aaagaaaa(T20, T30, T21, T6, T32, T33, T32, X20) → U15_aaagaaaa(T20, T30, T21, T6, T32, T33, X20, app47_in_aaag(T20, T30, T21, T6))
U15_aaagaaaa(T20, T30, T21, T6, T32, T33, X20, app47_out_aaag(T20, T30, T21, T6)) → U16_aaagaaaa(T20, T30, T21, T6, T32, T33, X20, in_order1_in_ag(T32, T20))
U16_aaagaaaa(T20, T30, T21, T6, T32, T33, X20, in_order1_out_ag(T32, T20)) → p45_out_aaagaaaa(T20, T30, T21, T6, T32, T33, T32, X20)
p45_in_aaagaaaa(T20, T37, T21, T6, T36, T39, T36, T39) → U17_aaagaaaa(T20, T37, T21, T6, T36, T39, app47_in_aaag(T20, T37, T21, T6))
U17_aaagaaaa(T20, T37, T21, T6, T36, T39, app47_out_aaag(T20, T37, T21, T6)) → U18_aaagaaaa(T20, T37, T21, T6, T36, T39, in_order1_in_ag(T36, T20))
U18_aaagaaaa(T20, T37, T21, T6, T36, T39, in_order1_out_ag(T36, T20)) → U19_aaagaaaa(T20, T37, T21, T6, T36, T39, in_order1_in_ag(T39, T21))
U19_aaagaaaa(T20, T37, T21, T6, T36, T39, in_order1_out_ag(T39, T21)) → p45_out_aaagaaaa(T20, T37, T21, T6, T36, T39, T36, T39)
U13_ag(T44, T43, T45, T6, p45_out_aaagaaaa(X17, T43, X18, T6, T44, T45, X19, X20)) → in_order1_out_ag(node(T44, T43, T45), T6)
U11_ag(T36, T37, T39, T6, T21, in_order1_out_ag(T36, T20)) → U12_ag(T36, T37, T39, T6, in_order1_in_ag(T39, T21))
U12_ag(T36, T37, T39, T6, in_order1_out_ag(T39, T21)) → in_order1_out_ag(node(T36, T37, T39), T6)
U9_ag(T32, T30, T33, T6, in_order1_out_ag(T32, T20)) → in_order1_out_ag(node(T32, T30, T33), T6)

The argument filtering Pi contains the following mapping:
in_order1_in_ag(x1, x2) = in_order1_in_ag(x2)
[] = []
in_order1_out_ag(x1, x2) = in_order1_out_ag(x2)
U3_ag(x1, x2) = U3_ag(x1, x2)
app16_in_aaag(x1, x2, x3, x4) = app16_in_aaag(x4)
.(x1, x2) = .(x1, x2)
app16_out_aaag(x1, x2, x3, x4) = app16_out_aaag(x1, x2, x3, x4)
U1_aaag(x1, x2, x3, x4, x5, x6) = U1_aaag(x1, x5, x6)
U4_ag(x1, x2) = U4_ag(x1, x2)
U5_ag(x1, x2, x3) = U5_ag(x1, x2, x3)
in_order30_in_g(x1) = in_order30_in_g(x1)
in_order30_out_g(x1) = in_order30_out_g(x1)
U6_ag(x1, x2) = U6_ag(x1, x2)
U7_ag(x1, x2, x3, x4, x5) = U7_ag(x4, x5)
app47_in_aaag(x1, x2, x3, x4) = app47_in_aaag(x4)
app47_out_aaag(x1, x2, x3, x4) = app47_out_aaag(x1, x2, x3, x4)
U2_aaag(x1, x2, x3, x4, x5, x6) = U2_aaag(x1, x5, x6)
U8_ag(x1, x2, x3, x4, x5) = U8_ag(x4, x5)
U9_ag(x1, x2, x3, x4, x5) = U9_ag(x4, x5)
U10_ag(x1, x2, x3, x4, x5) = U10_ag(x4, x5)
U11_ag(x1, x2, x3, x4, x5, x6) = U11_ag(x4, x5, x6)
U13_ag(x1, x2, x3, x4, x5) = U13_ag(x4, x5)
p45_in_aaagaaaa(x1, x2, x3, x4, x5, x6, x7, x8) = p45_in_aaagaaaa(x4)
U14_aaagaaaa(x1, x2, x3, x4, x5, x6, x7, x8, x9) = U14_aaagaaaa(x4, x9)
p45_out_aaagaaaa(x1, x2, x3, x4, x5, x6, x7, x8) = p45_out_aaagaaaa(x1, x2, x3, x4)
U15_aaagaaaa(x1, x2, x3, x4, x5, x6, x7, x8) = U15_aaagaaaa(x4, x8)
U16_aaagaaaa(x1, x2, x3, x4, x5, x6, x7, x8) = U16_aaagaaaa(x1, x2, x3, x4, x8)
U17_aaagaaaa(x1, x2, x3, x4, x5, x6, x7) = U17_aaagaaaa(x4, x7)
U18_aaagaaaa(x1, x2, x3, x4, x5, x6, x7) = U18_aaagaaaa(x1, x2, x3, x4, x7)
U19_aaagaaaa(x1, x2, x3, x4, x5, x6, x7) = U19_aaagaaaa(x1, x2, x3, x4, x7)
U12_ag(x1, x2, x3, x4, x5) = U12_ag(x4, x5)
IN_ORDER1_IN_AG(x1, x2) = IN_ORDER1_IN_AG(x2)
U8_AG(x1, x2, x3, x4, x5) = U8_AG(x4, x5)
U10_AG(x1, x2, x3, x4, x5) = U10_AG(x4, x5)
U11_AG(x1, x2, x3, x4, x5, x6) = U11_AG(x4, x5, x6)
P45_IN_AAAGAAAA(x1, x2, x3, x4, x5, x6, x7, x8) = P45_IN_AAAGAAAA(x4)
U15_AAAGAAAA(x1, x2, x3, x4, x5, x6, x7, x8) = U15_AAAGAAAA(x4, x8)
U17_AAAGAAAA(x1, x2, x3, x4, x5, x6, x7) = U17_AAAGAAAA(x4, x7)
U18_AAAGAAAA(x1, x2, x3, x4, x5, x6, x7) = U18_AAAGAAAA(x1, x2, x3, x4, x7)

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

(24) PiDPToQDPProof (SOUND transformation)

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

(25) Obligation:

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

IN_ORDER1_IN_AG(T6) → U8_AG(T6, app47_in_aaag(T6))
U8_AG(T6, app47_out_aaag(T20, T30, T21, T6)) → IN_ORDER1_IN_AG(T20)
IN_ORDER1_IN_AG(T6) → U10_AG(T6, app47_in_aaag(T6))
U10_AG(T6, app47_out_aaag(T20, T37, T21, T6)) → U11_AG(T6, T21, in_order1_in_ag(T20))
U11_AG(T6, T21, in_order1_out_ag(T20)) → IN_ORDER1_IN_AG(T21)
IN_ORDER1_IN_AG(T6) → P45_IN_AAAGAAAA(T6)
P45_IN_AAAGAAAA(T6) → U15_AAAGAAAA(T6, app47_in_aaag(T6))
U15_AAAGAAAA(T6, app47_out_aaag(T20, T30, T21, T6)) → IN_ORDER1_IN_AG(T20)
P45_IN_AAAGAAAA(T6) → U17_AAAGAAAA(T6, app47_in_aaag(T6))
U17_AAAGAAAA(T6, app47_out_aaag(T20, T37, T21, T6)) → U18_AAAGAAAA(T20, T37, T21, T6, in_order1_in_ag(T20))
U18_AAAGAAAA(T20, T37, T21, T6, in_order1_out_ag(T20)) → IN_ORDER1_IN_AG(T21)
U17_AAAGAAAA(T6, app47_out_aaag(T20, T37, T21, T6)) → IN_ORDER1_IN_AG(T20)
U10_AG(T6, app47_out_aaag(T20, T37, T21, T6)) → IN_ORDER1_IN_AG(T20)

The TRS R consists of the following rules:

in_order1_in_ag([]) → in_order1_out_ag([])
in_order1_in_ag(T6) → U3_ag(T6, app16_in_aaag(T6))
app16_in_aaag(.(X27, X28)) → app16_out_aaag([], X27, X28, .(X27, X28))
app16_in_aaag(.(X37, T11)) → U1_aaag(X37, T11, app16_in_aaag(T11))
U1_aaag(X37, T11, app16_out_aaag(X38, X39, X40, T11)) → app16_out_aaag(.(X37, X38), X39, X40, .(X37, T11))
U3_ag(T6, app16_out_aaag(X17, X23, X18, T6)) → in_order1_out_ag(T6)
in_order1_in_ag(T6) → U4_ag(T6, app16_in_aaag(T6))
U4_ag(T6, app16_out_aaag(T8, T9, T10, T6)) → U5_ag(T6, T10, in_order30_in_g(T8))
in_order30_in_g([]) → in_order30_out_g([])
U5_ag(T6, T10, in_order30_out_g(T8)) → in_order1_out_ag(T6)
U5_ag(T6, T10, in_order30_out_g(T8)) → U6_ag(T6, in_order30_in_g(T10))
U6_ag(T6, in_order30_out_g(T10)) → in_order1_out_ag(T6)
in_order1_in_ag(T6) → U7_ag(T6, app47_in_aaag(T6))
app47_in_aaag(.(T25, X60)) → app47_out_aaag([], T25, X60, .(T25, X60))
app47_in_aaag(.(X69, T27)) → U2_aaag(X69, T27, app47_in_aaag(T27))
U2_aaag(X69, T27, app47_out_aaag(X70, T28, X71, T27)) → app47_out_aaag(.(X69, X70), T28, X71, .(X69, T27))
U7_ag(T6, app47_out_aaag(X17, T17, X18, T6)) → in_order1_out_ag(T6)
in_order1_in_ag(T6) → U8_ag(T6, app47_in_aaag(T6))
U8_ag(T6, app47_out_aaag(T20, T30, T21, T6)) → U9_ag(T6, in_order1_in_ag(T20))
in_order1_in_ag(T6) → U10_ag(T6, app47_in_aaag(T6))
U10_ag(T6, app47_out_aaag(T20, T37, T21, T6)) → U11_ag(T6, T21, in_order1_in_ag(T20))
in_order1_in_ag(T6) → U13_ag(T6, p45_in_aaagaaaa(T6))
p45_in_aaagaaaa(T6) → U14_aaagaaaa(T6, app47_in_aaag(T6))
U14_aaagaaaa(T6, app47_out_aaag(X17, T17, X18, T6)) → p45_out_aaagaaaa(X17, T17, X18, T6)
p45_in_aaagaaaa(T6) → U15_aaagaaaa(T6, app47_in_aaag(T6))
U15_aaagaaaa(T6, app47_out_aaag(T20, T30, T21, T6)) → U16_aaagaaaa(T20, T30, T21, T6, in_order1_in_ag(T20))
U16_aaagaaaa(T20, T30, T21, T6, in_order1_out_ag(T20)) → p45_out_aaagaaaa(T20, T30, T21, T6)
p45_in_aaagaaaa(T6) → U17_aaagaaaa(T6, app47_in_aaag(T6))
U17_aaagaaaa(T6, app47_out_aaag(T20, T37, T21, T6)) → U18_aaagaaaa(T20, T37, T21, T6, in_order1_in_ag(T20))
U18_aaagaaaa(T20, T37, T21, T6, in_order1_out_ag(T20)) → U19_aaagaaaa(T20, T37, T21, T6, in_order1_in_ag(T21))
U19_aaagaaaa(T20, T37, T21, T6, in_order1_out_ag(T21)) → p45_out_aaagaaaa(T20, T37, T21, T6)
U13_ag(T6, p45_out_aaagaaaa(X17, T43, X18, T6)) → in_order1_out_ag(T6)
U11_ag(T6, T21, in_order1_out_ag(T20)) → U12_ag(T6, in_order1_in_ag(T21))
U12_ag(T6, in_order1_out_ag(T21)) → in_order1_out_ag(T6)
U9_ag(T6, in_order1_out_ag(T20)) → in_order1_out_ag(T6)

The set Q consists of the following terms:

in_order1_in_ag(x0)
app16_in_aaag(x0)
U1_aaag(x0, x1, x2)
U3_ag(x0, x1)
U4_ag(x0, x1)
in_order30_in_g(x0)
U5_ag(x0, x1, x2)
U6_ag(x0, x1)
app47_in_aaag(x0)
U2_aaag(x0, x1, x2)
U7_ag(x0, x1)
U8_ag(x0, x1)
U10_ag(x0, x1)
p45_in_aaagaaaa(x0)
U14_aaagaaaa(x0, x1)
U15_aaagaaaa(x0, x1)
U16_aaagaaaa(x0, x1, x2, x3, x4)
U17_aaagaaaa(x0, x1)
U18_aaagaaaa(x0, x1, x2, x3, x4)
U19_aaagaaaa(x0, x1, x2, x3, x4)
U13_ag(x0, x1)
U11_ag(x0, x1, x2)
U12_ag(x0, x1)
U9_ag(x0, x1)

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

(26) QDPOrderProof (EQUIVALENT transformation)

We use the reduction pair processor [LPAR04].

The following pairs can be oriented strictly and are deleted.

U8_AG(T6, app47_out_aaag(T20, T30, T21, T6)) → IN_ORDER1_IN_AG(T20)
U10_AG(T6, app47_out_aaag(T20, T37, T21, T6)) → U11_AG(T6, T21, in_order1_in_ag(T20))
U15_AAAGAAAA(T6, app47_out_aaag(T20, T30, T21, T6)) → IN_ORDER1_IN_AG(T20)
U17_AAAGAAAA(T6, app47_out_aaag(T20, T37, T21, T6)) → U18_AAAGAAAA(T20, T37, T21, T6, in_order1_in_ag(T20))
U17_AAAGAAAA(T6, app47_out_aaag(T20, T37, T21, T6)) → IN_ORDER1_IN_AG(T20)
U10_AG(T6, app47_out_aaag(T20, T37, T21, T6)) → IN_ORDER1_IN_AG(T20)

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

POL(.(x₁, x₂)) = 1 + x₁ + x₂
POL(IN_ORDER1_IN_AG(x₁)) = x₁
POL(P45_IN_AAAGAAAA(x₁)) = x₁
POL(U10_AG(x₁, x₂)) = x₂
POL(U10_ag(x₁, x₂)) = 0
POL(U11_AG(x₁, x₂, x₃)) = x₂
POL(U11_ag(x₁, x₂, x₃)) = 0
POL(U12_ag(x₁, x₂)) = 0
POL(U13_ag(x₁, x₂)) = 0
POL(U14_aaagaaaa(x₁, x₂)) = 1
POL(U15_AAAGAAAA(x₁, x₂)) = x₂
POL(U15_aaagaaaa(x₁, x₂)) = 0
POL(U16_aaagaaaa(x₁, x₂, x₃, x₄, x₅)) = 0
POL(U17_AAAGAAAA(x₁, x₂)) = x₂
POL(U17_aaagaaaa(x₁, x₂)) = 0
POL(U18_AAAGAAAA(x₁, x₂, x₃, x₄, x₅)) = x₃
POL(U18_aaagaaaa(x₁, x₂, x₃, x₄, x₅)) = 0
POL(U19_aaagaaaa(x₁, x₂, x₃, x₄, x₅)) = 0
POL(U1_aaag(x₁, x₂, x₃)) = 0
POL(U2_aaag(x₁, x₂, x₃)) = 1 + x₁ + x₃
POL(U3_ag(x₁, x₂)) = 0
POL(U4_ag(x₁, x₂)) = 0
POL(U5_ag(x₁, x₂, x₃)) = 0
POL(U6_ag(x₁, x₂)) = 0
POL(U7_ag(x₁, x₂)) = 0
POL(U8_AG(x₁, x₂)) = x₂
POL(U8_ag(x₁, x₂)) = 0
POL(U9_ag(x₁, x₂)) = 0
POL([]) = 0
POL(app16_in_aaag(x₁)) = 0
POL(app16_out_aaag(x₁, x₂, x₃, x₄)) = 0
POL(app47_in_aaag(x₁)) = x₁
POL(app47_out_aaag(x₁, x₂, x₃, x₄)) = 1 + x₁ + x₃
POL(in_order1_in_ag(x₁)) = 0
POL(in_order1_out_ag(x₁)) = 0
POL(in_order30_in_g(x₁)) = 1
POL(in_order30_out_g(x₁)) = 0
POL(p45_in_aaagaaaa(x₁)) = 1
POL(p45_out_aaagaaaa(x₁, x₂, x₃, x₄)) = 0

The following usable rules [FROCOS05] were oriented:

app47_in_aaag(.(T25, X60)) → app47_out_aaag([], T25, X60, .(T25, X60))
app47_in_aaag(.(X69, T27)) → U2_aaag(X69, T27, app47_in_aaag(T27))
U2_aaag(X69, T27, app47_out_aaag(X70, T28, X71, T27)) → app47_out_aaag(.(X69, X70), T28, X71, .(X69, T27))

(27) Obligation:

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

IN_ORDER1_IN_AG(T6) → U8_AG(T6, app47_in_aaag(T6))
IN_ORDER1_IN_AG(T6) → U10_AG(T6, app47_in_aaag(T6))
U11_AG(T6, T21, in_order1_out_ag(T20)) → IN_ORDER1_IN_AG(T21)
IN_ORDER1_IN_AG(T6) → P45_IN_AAAGAAAA(T6)
P45_IN_AAAGAAAA(T6) → U15_AAAGAAAA(T6, app47_in_aaag(T6))
P45_IN_AAAGAAAA(T6) → U17_AAAGAAAA(T6, app47_in_aaag(T6))
U18_AAAGAAAA(T20, T37, T21, T6, in_order1_out_ag(T20)) → IN_ORDER1_IN_AG(T21)

The TRS R consists of the following rules:

in_order1_in_ag([]) → in_order1_out_ag([])
in_order1_in_ag(T6) → U3_ag(T6, app16_in_aaag(T6))
app16_in_aaag(.(X27, X28)) → app16_out_aaag([], X27, X28, .(X27, X28))
app16_in_aaag(.(X37, T11)) → U1_aaag(X37, T11, app16_in_aaag(T11))
U1_aaag(X37, T11, app16_out_aaag(X38, X39, X40, T11)) → app16_out_aaag(.(X37, X38), X39, X40, .(X37, T11))
U3_ag(T6, app16_out_aaag(X17, X23, X18, T6)) → in_order1_out_ag(T6)
in_order1_in_ag(T6) → U4_ag(T6, app16_in_aaag(T6))
U4_ag(T6, app16_out_aaag(T8, T9, T10, T6)) → U5_ag(T6, T10, in_order30_in_g(T8))
in_order30_in_g([]) → in_order30_out_g([])
U5_ag(T6, T10, in_order30_out_g(T8)) → in_order1_out_ag(T6)
U5_ag(T6, T10, in_order30_out_g(T8)) → U6_ag(T6, in_order30_in_g(T10))
U6_ag(T6, in_order30_out_g(T10)) → in_order1_out_ag(T6)
in_order1_in_ag(T6) → U7_ag(T6, app47_in_aaag(T6))
app47_in_aaag(.(T25, X60)) → app47_out_aaag([], T25, X60, .(T25, X60))
app47_in_aaag(.(X69, T27)) → U2_aaag(X69, T27, app47_in_aaag(T27))
U2_aaag(X69, T27, app47_out_aaag(X70, T28, X71, T27)) → app47_out_aaag(.(X69, X70), T28, X71, .(X69, T27))
U7_ag(T6, app47_out_aaag(X17, T17, X18, T6)) → in_order1_out_ag(T6)
in_order1_in_ag(T6) → U8_ag(T6, app47_in_aaag(T6))
U8_ag(T6, app47_out_aaag(T20, T30, T21, T6)) → U9_ag(T6, in_order1_in_ag(T20))
in_order1_in_ag(T6) → U10_ag(T6, app47_in_aaag(T6))
U10_ag(T6, app47_out_aaag(T20, T37, T21, T6)) → U11_ag(T6, T21, in_order1_in_ag(T20))
in_order1_in_ag(T6) → U13_ag(T6, p45_in_aaagaaaa(T6))
p45_in_aaagaaaa(T6) → U14_aaagaaaa(T6, app47_in_aaag(T6))
U14_aaagaaaa(T6, app47_out_aaag(X17, T17, X18, T6)) → p45_out_aaagaaaa(X17, T17, X18, T6)
p45_in_aaagaaaa(T6) → U15_aaagaaaa(T6, app47_in_aaag(T6))
U15_aaagaaaa(T6, app47_out_aaag(T20, T30, T21, T6)) → U16_aaagaaaa(T20, T30, T21, T6, in_order1_in_ag(T20))
U16_aaagaaaa(T20, T30, T21, T6, in_order1_out_ag(T20)) → p45_out_aaagaaaa(T20, T30, T21, T6)
p45_in_aaagaaaa(T6) → U17_aaagaaaa(T6, app47_in_aaag(T6))
U17_aaagaaaa(T6, app47_out_aaag(T20, T37, T21, T6)) → U18_aaagaaaa(T20, T37, T21, T6, in_order1_in_ag(T20))
U18_aaagaaaa(T20, T37, T21, T6, in_order1_out_ag(T20)) → U19_aaagaaaa(T20, T37, T21, T6, in_order1_in_ag(T21))
U19_aaagaaaa(T20, T37, T21, T6, in_order1_out_ag(T21)) → p45_out_aaagaaaa(T20, T37, T21, T6)
U13_ag(T6, p45_out_aaagaaaa(X17, T43, X18, T6)) → in_order1_out_ag(T6)
U11_ag(T6, T21, in_order1_out_ag(T20)) → U12_ag(T6, in_order1_in_ag(T21))
U12_ag(T6, in_order1_out_ag(T21)) → in_order1_out_ag(T6)
U9_ag(T6, in_order1_out_ag(T20)) → in_order1_out_ag(T6)

The set Q consists of the following terms:

in_order1_in_ag(x0)
app16_in_aaag(x0)
U1_aaag(x0, x1, x2)
U3_ag(x0, x1)
U4_ag(x0, x1)
in_order30_in_g(x0)
U5_ag(x0, x1, x2)
U6_ag(x0, x1)
app47_in_aaag(x0)
U2_aaag(x0, x1, x2)
U7_ag(x0, x1)
U8_ag(x0, x1)
U10_ag(x0, x1)
p45_in_aaagaaaa(x0)
U14_aaagaaaa(x0, x1)
U15_aaagaaaa(x0, x1)
U16_aaagaaaa(x0, x1, x2, x3, x4)
U17_aaagaaaa(x0, x1)
U18_aaagaaaa(x0, x1, x2, x3, x4)
U19_aaagaaaa(x0, x1, x2, x3, x4)
U13_ag(x0, x1)
U11_ag(x0, x1, x2)
U12_ag(x0, x1)
U9_ag(x0, x1)

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

(28) DependencyGraphProof (EQUIVALENT transformation)

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

(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) Complex Obligation (AND)

(9) Obligation:

(10) UsableRulesProof (EQUIVALENT transformation)

(11) Obligation:

(12) PiDPToQDPProof (SOUND transformation)

(13) Obligation:

(14) QDPSizeChangeProof (EQUIVALENT transformation)

(15) TRUE

(16) Obligation:

(17) UsableRulesProof (EQUIVALENT transformation)

(18) Obligation:

(19) PiDPToQDPProof (SOUND transformation)

(20) Obligation:

(21) QDPSizeChangeProof (EQUIVALENT transformation)

(22) TRUE

(23) Obligation:

(24) PiDPToQDPProof (SOUND transformation)

(25) Obligation:

(26) QDPOrderProof (EQUIVALENT transformation)

(27) Obligation:

(28) DependencyGraphProof (EQUIVALENT transformation)

(29) TRUE