Left Termination proof of /tmp/tmpezAase/hidden

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

0 Prolog

↳1 PrologToDTProblemTransformerProof (⇐)

↳2 TRIPLES

↳3 TriplesToPiDPProof (⇐)

↳4 PiDP

↳5 DependencyGraphProof (⇔)

↳6 PiDP

↳7 PiDPToQDPProof (⇐)

↳8 QDP

↳9 QDPOrderProof (⇔)

↳10 QDP

↳11 QDPOrderProof (⇔)

↳12 QDP

↳13 DependencyGraphProof (⇔)

↳14 TRUE

(0) Obligation:

Clauses:

hidden_flatten([], L, L).
hidden_flatten(.(.(H, T), L), S, F) :- ','(!, ','(hidden_flatten(L, S, Lf), hidden_flatten(.(H, T), Lf, F))).
hidden_flatten(.(H, T), S, .(H, L)) :- hidden_flatten(T, S, L).

Queries:

hidden_flatten(g,a,a).

(1) PrologToDTProblemTransformerProof (SOUND transformation)

Built DT problem from termination graph.

digraph dp_graph {
node [outthreshold=100, inthreshold=100];
1 [label="1: hidden_flatten(T1, T2, T3)\n\nT1 is ground", fontsize=16, style=filled, fillcolor=lightyellow, color=red];
2 [label="2: hidden_flatten(T1, T2, T3), SCOPE: 1, CLAUSE: 0 | hidden_flatten(T1, T2, T3), SCOPE: 1, CLAUSE: 1 | hidden_flatten(T1, T2, T3), SCOPE: 1, CLAUSE: 2\n\nT1 is ground", fontsize=16, style=filled, fillcolor=lightyellow];
3 [label="3: true | hidden_flatten([], T2, T3), SCOPE: 1, CLAUSE: 1 | hidden_flatten([], T2, T3), SCOPE: 1, CLAUSE: 2\n\n", fontsize=16, style=filled, fillcolor=lightyellow];
4 [label="4: hidden_flatten(T1, T2, T3), SCOPE: 1, CLAUSE: 1 | hidden_flatten(T1, T2, T3), SCOPE: 1, CLAUSE: 2\n\nT1 is ground\nhidden_flatten(T1, T2, T3) !=? hidden_flatten([], X2, X2)", fontsize=16, style=filled, fillcolor=lightyellow];
5 [label="5: hidden_flatten([], T2, T3), SCOPE: 1, CLAUSE: 1 | hidden_flatten([], T2, T3), SCOPE: 1, CLAUSE: 2\n\n", fontsize=16, style=filled, fillcolor=lightyellow];
6 [label="6: hidden_flatten([], T2, T3), SCOPE: 1, CLAUSE: 2\n\n", fontsize=16, style=filled, fillcolor=lightyellow];
7 [label="7: \n\n", fontsize=16, style=filled, fillcolor=lightyellow];
8 [label="8: ','(!_1, ','(hidden_flatten(T13, T16, X23), hidden_flatten(.(T11, T12), X23, T17))) | hidden_flatten(.(.(T11, T12), T13), T2, T3), SCOPE: 1, CLAUSE: 2\n\nT11 is ground\nT12 is ground\nT13 is ground\nX23 is free; ", fontsize=16, style=filled, fillcolor=lightyellow];
9 [label="9: hidden_flatten(T1, T2, T3), SCOPE: 1, CLAUSE: 2\n\nT1 is ground\nhidden_flatten(T1, T2, T3) !=? hidden_flatten([], X2, X2)\nhidden_flatten(T1, T2, T3) !=? hidden_flatten(.(.(X18, X19), X20), X21, X22)", fontsize=16, style=filled, fillcolor=lightyellow];
10 [label="10: ','(hidden_flatten(T13, T16, X23), hidden_flatten(.(T11, T12), X23, T17))\n\nT11 is ground\nT12 is ground\nT13 is ground\nX23 is free; ", fontsize=16, style=filled, fillcolor=lightyellow];
11 [label="11: ','(hidden_flatten(T13, T16, X23), hidden_flatten(.(T11, T12), X23, T17)), SCOPE: 2, CLAUSE: 0 | ','(hidden_flatten(T13, T16, X23), hidden_flatten(.(T11, T12), X23, T17)), SCOPE: 2, CLAUSE: 1 | ','(hidden_flatten(T13, T16, X23), hidden_flatten(.(T11, T12), X23, T17)), SCOPE: 2, CLAUSE: 2\n\nT11 is ground\nT12 is ground\nT13 is ground\nX23 is free; ", fontsize=16, style=filled, fillcolor=lightyellow];
12 [label="12: hidden_flatten(.(T11, T12), T21, T22) | ','(hidden_flatten([], T16, X23), hidden_flatten(.(T11, T12), X23, T17)), SCOPE: 2, CLAUSE: 1 | ','(hidden_flatten([], T16, X23), hidden_flatten(.(T11, T12), X23, T17)), SCOPE: 2, CLAUSE: 2\n\nT11 is ground\nT12 is ground\nX23 is free; ", fontsize=16, style=filled, fillcolor=lightyellow];
13 [label="13: ','(hidden_flatten(T13, T16, X23), hidden_flatten(.(T11, T12), X23, T17)), SCOPE: 2, CLAUSE: 1 | ','(hidden_flatten(T13, T16, X23), hidden_flatten(.(T11, T12), X23, T17)), SCOPE: 2, CLAUSE: 2\n\nT11 is ground\nT12 is ground\nT13 is ground\nX23 is free; \nhidden_flatten(T13, T16, X23) !=? hidden_flatten([], X31, X31)", fontsize=16, style=filled, fillcolor=lightyellow];
14 [label="14: hidden_flatten(.(T11, T12), T21, T22)\n\nT11 is ground\nT12 is ground", fontsize=16, style=filled, fillcolor=lightyellow];
15 [label="15: ','(hidden_flatten([], T16, X23), hidden_flatten(.(T11, T12), X23, T17)), SCOPE: 2, CLAUSE: 1 | ','(hidden_flatten([], T16, X23), hidden_flatten(.(T11, T12), X23, T17)), SCOPE: 2, CLAUSE: 2\n\nT11 is ground\nT12 is ground\nX23 is free; ", fontsize=16, style=filled, fillcolor=lightyellow];
16 [label="16: ','(hidden_flatten([], T16, X23), hidden_flatten(.(T11, T12), X23, T17)), SCOPE: 2, CLAUSE: 2\n\nT11 is ground\nT12 is ground\nX23 is free; ", fontsize=16, style=filled, fillcolor=lightyellow];
17 [label="17: \n\n", fontsize=16, style=filled, fillcolor=lightyellow];
18 [label="18: ','(hidden_flatten(T13, T16, X23), hidden_flatten(.(T11, T12), X23, T17)), SCOPE: 2, CLAUSE: 1\n\nT11 is ground\nT12 is ground\nT13 is ground\nX23 is free; \nhidden_flatten(T13, T16, X23) !=? hidden_flatten([], X31, X31)", fontsize=16, style=filled, fillcolor=lightyellow];
19 [label="19: ','(hidden_flatten(T13, T16, X23), hidden_flatten(.(T11, T12), X23, T17)), SCOPE: 2, CLAUSE: 2\n\nT11 is ground\nT12 is ground\nT13 is ground\nX23 is free; \nhidden_flatten(T13, T16, X23) !=? hidden_flatten([], X31, X31)", fontsize=16, style=filled, fillcolor=lightyellow];
20 [label="20: ','(!_2, ','(hidden_flatten(T51, T53, X89), ','(hidden_flatten(.(T49, T50), X89, X90), hidden_flatten(.(T11, T12), X90, T54))))\n\nT11 is ground\nT12 is ground\nT49 is ground\nT50 is ground\nT51 is ground\nX90 is free; \nX89 is free; ", fontsize=16, style=filled, fillcolor=lightyellow];
21 [label="21: \n\n", fontsize=16, style=filled, fillcolor=lightyellow];
22 [label="22: ','(hidden_flatten(T51, T53, X89), ','(hidden_flatten(.(T49, T50), X89, X90), hidden_flatten(.(T11, T12), X90, T54)))\n\nT11 is ground\nT12 is ground\nT49 is ground\nT50 is ground\nT51 is ground\nX90 is free; \nX89 is free; ", fontsize=16, style=filled, fillcolor=lightyellow];
23 [label="23: hidden_flatten(T51, T53, X89)\n\nT51 is ground\nX89 is free; ", fontsize=16, style=filled, fillcolor=lightyellow];
24 [label="24: ','(hidden_flatten(.(T49, T50), T57, X90), hidden_flatten(.(T11, T12), X90, T58))\n\nT11 is ground\nT12 is ground\nT49 is ground\nT50 is ground\nX90 is free; ", fontsize=16, style=filled, fillcolor=lightyellow];
25 [label="25: hidden_flatten(T51, T53, X89), SCOPE: 3, CLAUSE: 0 | hidden_flatten(T51, T53, X89), SCOPE: 3, CLAUSE: 1 | hidden_flatten(T51, T53, X89), SCOPE: 3, CLAUSE: 2\n\nT51 is ground\nX89 is free; ", fontsize=16, style=filled, fillcolor=lightyellow];
26 [label="26: true | hidden_flatten([], T53, X89), SCOPE: 3, CLAUSE: 1 | hidden_flatten([], T53, X89), SCOPE: 3, CLAUSE: 2\n\nX89 is free", fontsize=16, style=filled, fillcolor=lightyellow];
27 [label="27: hidden_flatten(T51, T53, X89), SCOPE: 3, CLAUSE: 1 | hidden_flatten(T51, T53, X89), SCOPE: 3, CLAUSE: 2\n\nT51 is ground\nX89 is free; \nhidden_flatten(T51, T53, X89) !=? hidden_flatten([], X102, X102)", fontsize=16, style=filled, fillcolor=lightyellow];
28 [label="28: hidden_flatten([], T53, X89), SCOPE: 3, CLAUSE: 1 | hidden_flatten([], T53, X89), SCOPE: 3, CLAUSE: 2\n\nX89 is free", fontsize=16, style=filled, fillcolor=lightyellow];
29 [label="29: hidden_flatten([], T53, X89), SCOPE: 3, CLAUSE: 2\n\nX89 is free", fontsize=16, style=filled, fillcolor=lightyellow];
30 [label="30: \n\n", fontsize=16, style=filled, fillcolor=lightyellow];
31 [label="31: hidden_flatten(T51, T53, X89), SCOPE: 3, CLAUSE: 1\n\nT51 is ground\nX89 is free; \nhidden_flatten(T51, T53, X89) !=? hidden_flatten([], X102, X102)", fontsize=16, style=filled, fillcolor=lightyellow];
32 [label="32: hidden_flatten(T51, T53, X89), SCOPE: 3, CLAUSE: 2\n\nT51 is ground\nX89 is free; \nhidden_flatten(T51, T53, X89) !=? hidden_flatten([], X102, X102)", fontsize=16, style=filled, fillcolor=lightyellow];
33 [label="33: ','(!_3, ','(hidden_flatten(T82, T84, X144), hidden_flatten(.(T80, T81), X144, X145)))\n\nT80 is ground\nT81 is ground\nT82 is ground\nX145 is free; \nX144 is free; ", fontsize=16, style=filled, fillcolor=lightyellow];
34 [label="34: \n\n", fontsize=16, style=filled, fillcolor=lightyellow];
35 [label="35: ','(hidden_flatten(T82, T84, X144), hidden_flatten(.(T80, T81), X144, X145))\n\nT80 is ground\nT81 is ground\nT82 is ground\nX145 is free; \nX144 is free; ", fontsize=16, style=filled, fillcolor=lightyellow];
36 [label="36: hidden_flatten(T82, T84, X144)\n\nT82 is ground\nX144 is free; ", fontsize=16, style=filled, fillcolor=lightyellow];
37 [label="37: hidden_flatten(.(T80, T81), T87, X145)\n\nT80 is ground\nT81 is ground\nX145 is free; ", fontsize=16, style=filled, fillcolor=lightyellow];
38 [label="38: hidden_flatten(T101, T103, X178)\n\nT101 is ground\nX178 is free; ", fontsize=16, style=filled, fillcolor=lightyellow];
39 [label="39: \n\n", fontsize=16, style=filled, fillcolor=lightyellow];
40 [label="40: ','(hidden_flatten(T117, T119, X208), hidden_flatten(.(T11, T12), .(T116, X208), T120))\n\nT11 is ground\nT12 is ground\nT116 is ground\nT117 is ground\nX208 is free; ", fontsize=16, style=filled, fillcolor=lightyellow];
41 [label="41: \n\n", fontsize=16, style=filled, fillcolor=lightyellow];
42 [label="42: hidden_flatten(T117, T119, X208)\n\nT117 is ground\nX208 is free; ", fontsize=16, style=filled, fillcolor=lightyellow];
43 [label="43: hidden_flatten(.(T11, T12), .(T116, T123), T124)\n\nT11 is ground\nT12 is ground\nT116 is ground", fontsize=16, style=filled, fillcolor=lightyellow];
44 [label="44: hidden_flatten(T138, T141, T142)\n\nT138 is ground", fontsize=16, style=filled, fillcolor=lightyellow];
45 [label="45: \n\n", fontsize=16, style=filled, fillcolor=lightyellow];
46 [label="46: hidden_flatten(T138, T141, T142), SCOPE: 4, CLAUSE: 0 | hidden_flatten(T138, T141, T142), SCOPE: 4, CLAUSE: 1 | hidden_flatten(T138, T141, T142), SCOPE: 4, CLAUSE: 2\n\nT138 is ground", fontsize=16, style=filled, fillcolor=lightyellow];
47 [label="47: true | hidden_flatten([], T141, T142), SCOPE: 4, CLAUSE: 1 | hidden_flatten([], T141, T142), SCOPE: 4, CLAUSE: 2\n\n", fontsize=16, style=filled, fillcolor=lightyellow];
48 [label="48: hidden_flatten(T138, T141, T142), SCOPE: 4, CLAUSE: 1 | hidden_flatten(T138, T141, T142), SCOPE: 4, CLAUSE: 2\n\nT138 is ground\nhidden_flatten(T138, T141, T142) !=? hidden_flatten([], X239, X239)", fontsize=16, style=filled, fillcolor=lightyellow];
49 [label="49: hidden_flatten([], T141, T142), SCOPE: 4, CLAUSE: 1 | hidden_flatten([], T141, T142), SCOPE: 4, CLAUSE: 2\n\n", fontsize=16, style=filled, fillcolor=lightyellow];
50 [label="50: hidden_flatten([], T141, T142), SCOPE: 4, CLAUSE: 2\n\n", fontsize=16, style=filled, fillcolor=lightyellow];
51 [label="51: \n\n", fontsize=16, style=filled, fillcolor=lightyellow];
52 [label="52: hidden_flatten(T138, T141, T142), SCOPE: 4, CLAUSE: 1\n\nT138 is ground\nhidden_flatten(T138, T141, T142) !=? hidden_flatten([], X239, X239)", fontsize=16, style=filled, fillcolor=lightyellow];
53 [label="53: hidden_flatten(T138, T141, T142), SCOPE: 4, CLAUSE: 2\n\nT138 is ground\nhidden_flatten(T138, T141, T142) !=? hidden_flatten([], X239, X239)", fontsize=16, style=filled, fillcolor=lightyellow];
54 [label="54: ','(!_4, ','(hidden_flatten(T168, T171, X277), hidden_flatten(.(T166, T167), X277, T172)))\n\nT166 is ground\nT167 is ground\nT168 is ground\nX277 is free; ", fontsize=16, style=filled, fillcolor=lightyellow];
55 [label="55: \n\n", fontsize=16, style=filled, fillcolor=lightyellow];
56 [label="56: ','(hidden_flatten(T168, T171, X277), hidden_flatten(.(T166, T167), X277, T172))\n\nT166 is ground\nT167 is ground\nT168 is ground\nX277 is free; ", fontsize=16, style=filled, fillcolor=lightyellow];
57 [label="57: hidden_flatten(T184, T187, T188)\n\nT184 is ground", fontsize=16, style=filled, fillcolor=lightyellow];
58 [label="58: \n\n", fontsize=16, style=filled, fillcolor=lightyellow];
59 [label="CASE", fontsize=14, style = filled, fillcolor = lightcyan];
1 -> 59 [arrowhead = none ];
59 -> 2;

60 [label="EVAL with clause\nhidden_flatten([], X2, X2).\nand substitution\nT1 -> []\nT2 -> T5\nX2 -> T5\nT3 -> T5", fontsize=14, style = filled, fillcolor = lightblue];
2 -> 60 [arrowhead = none ];
60 -> 3;

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

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

63 [label="EVAL with clause\nhidden_flatten(.(.(X18, X19), X20), X21, X22) :- ','(!_1, ','(hidden_flatten(X20, X21, X23), hidden_flatten(.(X18, X19), X23, X22))).\nand substitution\nX18 -> T11\nX19 -> T12\nX20 -> T13\nT1 -> .(.(T11, T12), T13)\nT2 -> T16\nX21 -> T16\nT3 -> T17\nX22 -> T17\nT14 -> T16\nT15 -> T17", fontsize=14, style = filled, fillcolor = lightblue];
4 -> 63 [arrowhead = none ];
63 -> 8;

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

65 [label="BACKTRACK\nfor clause: hidden_flatten(.(.(H, T), L), S, F) :- ','(!, ','(hidden_flatten(L, S, Lf), hidden_flatten(.(H, T), Lf, F)))because of non-unification", fontsize=14, style = filled, fillcolor = white];
5 -> 65 [arrowhead = none ];
65 -> 6;

66 [label="BACKTRACK\nfor clause: hidden_flatten(.(H, T), S, .(H, L)) :- hidden_flatten(T, S, L)because of non-unification", fontsize=14, style = filled, fillcolor = white];
6 -> 66 [arrowhead = none ];
66 -> 7;

67 [label="CUT", fontsize=14, style = filled, fillcolor = lightgreen];
8 -> 67 [arrowhead = none ];
67 -> 10;

68 [label="EVAL with clause\nhidden_flatten(.(X229, X230), X231, .(X229, X232)) :- hidden_flatten(X230, X231, X232).\nand substitution\nX229 -> T137\nX230 -> T138\nT1 -> .(T137, T138)\nT2 -> T141\nX231 -> T141\nX232 -> T142\nT3 -> .(T137, T142)\nT139 -> T141\nT140 -> T142", fontsize=14, style = filled, fillcolor = lightblue];
9 -> 68 [arrowhead = none ];
68 -> 44;

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

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

71 [label="EVAL with clause\nhidden_flatten([], X31, X31).\nand substitution\nT13 -> []\nT16 -> T21\nX31 -> T21\nX23 -> T21\nT20 -> T21\nT17 -> T22", fontsize=14, style = filled, fillcolor = lightblue];
11 -> 71 [arrowhead = none ];
71 -> 12;

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

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

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

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

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

77 [label="INSTANCE with matching:\nT1 -> .(T11, T12)\nT2 -> T21\nT3 -> T22", fontsize=14, style = filled, fillcolor = lightgrey];
14 -> 77 [arrowhead = none , style=dashed];
77 -> 1[style=dashed];

78 [label="BACKTRACK\nfor clause: hidden_flatten(.(.(H, T), L), S, F) :- ','(!, ','(hidden_flatten(L, S, Lf), hidden_flatten(.(H, T), Lf, F)))because of non-unification", fontsize=14, style = filled, fillcolor = white];
15 -> 78 [arrowhead = none ];
78 -> 16;

79 [label="BACKTRACK\nfor clause: hidden_flatten(.(H, T), S, .(H, L)) :- hidden_flatten(T, S, L)because of non-unification", fontsize=14, style = filled, fillcolor = white];
16 -> 79 [arrowhead = none ];
79 -> 17;

80 [label="EVAL with clause\nhidden_flatten(.(.(X84, X85), X86), X87, X88) :- ','(!_2, ','(hidden_flatten(X86, X87, X89), hidden_flatten(.(X84, X85), X89, X88))).\nand substitution\nX84 -> T49\nX85 -> T50\nX86 -> T51\nT13 -> .(.(T49, T50), T51)\nT16 -> T53\nX87 -> T53\nX23 -> X90\nX88 -> X90\nT52 -> T53\nT17 -> T54", fontsize=14, style = filled, fillcolor = lightblue];
18 -> 80 [arrowhead = none ];
80 -> 20;

81 [label="EVAL-BACKTRACK", fontsize=14, style = filled, fillcolor = lightblue];
18 -> 81 [arrowhead = none ];
81 -> 21;

82 [label="EVAL with clause\nhidden_flatten(.(X204, X205), X206, .(X204, X207)) :- hidden_flatten(X205, X206, X207).\nand substitution\nX204 -> T116\nX205 -> T117\nT13 -> .(T116, T117)\nT16 -> T119\nX206 -> T119\nX207 -> X208\nX23 -> .(T116, X208)\nT118 -> T119\nT17 -> T120", fontsize=14, style = filled, fillcolor = lightblue];
19 -> 82 [arrowhead = none ];
82 -> 40;

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

84 [label="CUT", fontsize=14, style = filled, fillcolor = lightgreen];
20 -> 84 [arrowhead = none ];
84 -> 22;

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

86 [label="SPLIT 2\nreplacements:\nX89 -> T57\nT54 -> T58", fontsize=14, style = filled, fillcolor = violet];
22 -> 86 [arrowhead = none ];
86 -> 24;

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

88 [label="INSTANCE with matching:\nT13 -> .(T49, T50)\nT16 -> T57\nX23 -> X90\nT17 -> T58", fontsize=14, style = filled, fillcolor = lightgrey];
24 -> 88 [arrowhead = none , style=dashed];
88 -> 10[style=dashed];

89 [label="EVAL with clause\nhidden_flatten([], X102, X102).\nand substitution\nT51 -> []\nT53 -> T63\nX102 -> T63\nX89 -> T63", fontsize=14, style = filled, fillcolor = lightblue];
25 -> 89 [arrowhead = none ];
89 -> 26;

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

91 [label="SUCCESS", fontsize=14, style = filled, fillcolor = lightgreen];
26 -> 91 [arrowhead = none ];
91 -> 28;

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

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

94 [label="BACKTRACK\nfor clause: hidden_flatten(.(.(H, T), L), S, F) :- ','(!, ','(hidden_flatten(L, S, Lf), hidden_flatten(.(H, T), Lf, F)))because of non-unification", fontsize=14, style = filled, fillcolor = white];
28 -> 94 [arrowhead = none ];
94 -> 29;

95 [label="BACKTRACK\nfor clause: hidden_flatten(.(H, T), S, .(H, L)) :- hidden_flatten(T, S, L)because of non-unification", fontsize=14, style = filled, fillcolor = white];
29 -> 95 [arrowhead = none ];
95 -> 30;

96 [label="EVAL with clause\nhidden_flatten(.(.(X139, X140), X141), X142, X143) :- ','(!_3, ','(hidden_flatten(X141, X142, X144), hidden_flatten(.(X139, X140), X144, X143))).\nand substitution\nX139 -> T80\nX140 -> T81\nX141 -> T82\nT51 -> .(.(T80, T81), T82)\nT53 -> T84\nX142 -> T84\nX89 -> X145\nX143 -> X145\nT83 -> T84", fontsize=14, style = filled, fillcolor = lightblue];
31 -> 96 [arrowhead = none ];
96 -> 33;

97 [label="EVAL-BACKTRACK", fontsize=14, style = filled, fillcolor = lightblue];
31 -> 97 [arrowhead = none ];
97 -> 34;

98 [label="EVAL with clause\nhidden_flatten(.(X174, X175), X176, .(X174, X177)) :- hidden_flatten(X175, X176, X177).\nand substitution\nX174 -> T100\nX175 -> T101\nT51 -> .(T100, T101)\nT53 -> T103\nX176 -> T103\nX177 -> X178\nX89 -> .(T100, X178)\nT102 -> T103", fontsize=14, style = filled, fillcolor = lightblue];
32 -> 98 [arrowhead = none ];
98 -> 38;

99 [label="EVAL-BACKTRACK", fontsize=14, style = filled, fillcolor = lightblue];
32 -> 99 [arrowhead = none ];
99 -> 39;

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

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

102 [label="SPLIT 2\nreplacements:\nX144 -> T87", fontsize=14, style = filled, fillcolor = violet];
35 -> 102 [arrowhead = none ];
102 -> 37;

103 [label="INSTANCE with matching:\nT51 -> T82\nT53 -> T84\nX89 -> X144", fontsize=14, style = filled, fillcolor = lightgrey];
36 -> 103 [arrowhead = none , style=dashed];
103 -> 23[style=dashed];

104 [label="INSTANCE with matching:\nT1 -> .(T80, T81)\nT2 -> T87\nT3 -> X145", fontsize=14, style = filled, fillcolor = lightgrey];
37 -> 104 [arrowhead = none , style=dashed];
104 -> 1[style=dashed];

105 [label="INSTANCE with matching:\nT51 -> T101\nT53 -> T103\nX89 -> X178", fontsize=14, style = filled, fillcolor = lightgrey];
38 -> 105 [arrowhead = none , style=dashed];
105 -> 23[style=dashed];

106 [label="SPLIT 1", fontsize=14, style = filled, fillcolor = violet];
40 -> 106 [arrowhead = none ];
106 -> 42;

107 [label="SPLIT 2\nreplacements:\nX208 -> T123\nT120 -> T124", fontsize=14, style = filled, fillcolor = violet];
40 -> 107 [arrowhead = none ];
107 -> 43;

108 [label="INSTANCE with matching:\nT51 -> T117\nT53 -> T119\nX89 -> X208", fontsize=14, style = filled, fillcolor = lightgrey];
42 -> 108 [arrowhead = none , style=dashed];
108 -> 23[style=dashed];

109 [label="INSTANCE with matching:\nT1 -> .(T11, T12)\nT2 -> .(T116, T123)\nT3 -> T124", fontsize=14, style = filled, fillcolor = lightgrey];
43 -> 109 [arrowhead = none , style=dashed];
109 -> 1[style=dashed];

110 [label="CASE", fontsize=14, style = filled, fillcolor = lightcyan];
44 -> 110 [arrowhead = none ];
110 -> 46;

111 [label="EVAL with clause\nhidden_flatten([], X239, X239).\nand substitution\nT138 -> []\nT141 -> T145\nX239 -> T145\nT142 -> T145", fontsize=14, style = filled, fillcolor = lightblue];
46 -> 111 [arrowhead = none ];
111 -> 47;

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

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

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

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

116 [label="BACKTRACK\nfor clause: hidden_flatten(.(.(H, T), L), S, F) :- ','(!, ','(hidden_flatten(L, S, Lf), hidden_flatten(.(H, T), Lf, F)))because of non-unification", fontsize=14, style = filled, fillcolor = white];
49 -> 116 [arrowhead = none ];
116 -> 50;

117 [label="BACKTRACK\nfor clause: hidden_flatten(.(H, T), S, .(H, L)) :- hidden_flatten(T, S, L)because of non-unification", fontsize=14, style = filled, fillcolor = white];
50 -> 117 [arrowhead = none ];
117 -> 51;

118 [label="EVAL with clause\nhidden_flatten(.(.(X272, X273), X274), X275, X276) :- ','(!_4, ','(hidden_flatten(X274, X275, X277), hidden_flatten(.(X272, X273), X277, X276))).\nand substitution\nX272 -> T166\nX273 -> T167\nX274 -> T168\nT138 -> .(.(T166, T167), T168)\nT141 -> T171\nX275 -> T171\nT142 -> T172\nX276 -> T172\nT169 -> T171\nT170 -> T172", fontsize=14, style = filled, fillcolor = lightblue];
52 -> 118 [arrowhead = none ];
118 -> 54;

119 [label="EVAL-BACKTRACK", fontsize=14, style = filled, fillcolor = lightblue];
52 -> 119 [arrowhead = none ];
119 -> 55;

120 [label="EVAL with clause\nhidden_flatten(.(X293, X294), X295, .(X293, X296)) :- hidden_flatten(X294, X295, X296).\nand substitution\nX293 -> T183\nX294 -> T184\nT138 -> .(T183, T184)\nT141 -> T187\nX295 -> T187\nX296 -> T188\nT142 -> .(T183, T188)\nT185 -> T187\nT186 -> T188", fontsize=14, style = filled, fillcolor = lightblue];
53 -> 120 [arrowhead = none ];
120 -> 57;

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

122 [label="CUT", fontsize=14, style = filled, fillcolor = lightgreen];
54 -> 122 [arrowhead = none ];
122 -> 56;

123 [label="INSTANCE with matching:\nT13 -> T168\nT16 -> T171\nX23 -> X277\nT11 -> T166\nT12 -> T167\nT17 -> T172", fontsize=14, style = filled, fillcolor = lightgrey];
56 -> 123 [arrowhead = none , style=dashed];
123 -> 10[style=dashed];

124 [label="INSTANCE with matching:\nT1 -> T184\nT2 -> T187\nT3 -> T188", fontsize=14, style = filled, fillcolor = lightgrey];
57 -> 124 [arrowhead = none , style=dashed];
124 -> 1[style=dashed];

}

(2) Obligation:

Triples:

p10([], T21, T21, T11, T12, T22) :- hidden_flatten1(.(T11, T12), T21, T22).
p10(.(.(T49, T50), T51), T53, X90, T11, T12, T54) :- hidden_flatten23(T51, T53, X89).
p10(.(.(T49, T50), T51), T53, X90, T11, T12, T58) :- ','(hidden_flattenc23(T51, T53, T57), p10(.(T49, T50), T57, X90, T11, T12, T58)).
p10(.(T116, T117), T119, .(T116, X208), T11, T12, T120) :- hidden_flatten23(T117, T119, X208).
p10(.(T116, T117), T119, .(T116, T123), T11, T12, T124) :- ','(hidden_flattenc23(T117, T119, T123), hidden_flatten1(.(T11, T12), .(T116, T123), T124)).
hidden_flatten23(.(.(T80, T81), T82), T84, X145) :- hidden_flatten23(T82, T84, X144).
hidden_flatten23(.(.(T80, T81), T82), T84, X145) :- ','(hidden_flattenc23(T82, T84, T87), hidden_flatten1(.(T80, T81), T87, X145)).
hidden_flatten23(.(T100, T101), T103, .(T100, X178)) :- hidden_flatten23(T101, T103, X178).
hidden_flatten1(.(.(T11, T12), T13), T16, T17) :- p10(T13, T16, X23, T11, T12, T17).
hidden_flatten1(.(T137, .(.(T166, T167), T168)), T171, .(T137, T172)) :- p10(T168, T171, X277, T166, T167, T172).
hidden_flatten1(.(T137, .(T183, T184)), T187, .(T137, .(T183, T188))) :- hidden_flatten1(T184, T187, T188).

Clauses:

hidden_flattenc1([], T5, T5).
hidden_flattenc1(.(.(T11, T12), T13), T16, T17) :- qc10(T13, T16, X23, T11, T12, T17).
hidden_flattenc1(.(T137, []), T145, .(T137, T145)).
hidden_flattenc1(.(T137, .(.(T166, T167), T168)), T171, .(T137, T172)) :- qc10(T168, T171, X277, T166, T167, T172).
hidden_flattenc1(.(T137, .(T183, T184)), T187, .(T137, .(T183, T188))) :- hidden_flattenc1(T184, T187, T188).
qc10([], T21, T21, T11, T12, T22) :- hidden_flattenc1(.(T11, T12), T21, T22).
qc10(.(.(T49, T50), T51), T53, X90, T11, T12, T58) :- ','(hidden_flattenc23(T51, T53, T57), qc10(.(T49, T50), T57, X90, T11, T12, T58)).
qc10(.(T116, T117), T119, .(T116, T123), T11, T12, T124) :- ','(hidden_flattenc23(T117, T119, T123), hidden_flattenc1(.(T11, T12), .(T116, T123), T124)).
hidden_flattenc23([], T63, T63).
hidden_flattenc23(.(.(T80, T81), T82), T84, X145) :- ','(hidden_flattenc23(T82, T84, T87), hidden_flattenc1(.(T80, T81), T87, X145)).
hidden_flattenc23(.(T100, T101), T103, .(T100, X178)) :- hidden_flattenc23(T101, T103, X178).

Afs:

hidden_flatten1(x1, x2, x3) = hidden_flatten1(x1)

(3) TriplesToPiDPProof (SOUND transformation)

We use the technique of [LOPSTR]. With regard to the inferred argument filtering the predicates were used in the following modes:
hidden_flatten1_in: (b,f,f)
p10_in: (b,f,f,b,b,f)
hidden_flatten23_in: (b,f,f)
hidden_flattenc23_in: (b,f,f)
hidden_flattenc1_in: (b,f,f)
qc10_in: (b,f,f,b,b,f)
Transforming TRIPLES into the following Term Rewriting System:
Pi DP problem:
The TRS P consists of the following rules:

HIDDEN_FLATTEN1_IN_GAA(.(.(T11, T12), T13), T16, T17) → U12_GAA(T11, T12, T13, T16, T17, p10_in_gaagga(T13, T16, X23, T11, T12, T17))
HIDDEN_FLATTEN1_IN_GAA(.(.(T11, T12), T13), T16, T17) → P10_IN_GAAGGA(T13, T16, X23, T11, T12, T17)
P10_IN_GAAGGA([], T21, T21, T11, T12, T22) → U1_GAAGGA(T21, T11, T12, T22, hidden_flatten1_in_gaa(.(T11, T12), T21, T22))
P10_IN_GAAGGA([], T21, T21, T11, T12, T22) → HIDDEN_FLATTEN1_IN_GAA(.(T11, T12), T21, T22)
HIDDEN_FLATTEN1_IN_GAA(.(T137, .(.(T166, T167), T168)), T171, .(T137, T172)) → U13_GAA(T137, T166, T167, T168, T171, T172, p10_in_gaagga(T168, T171, X277, T166, T167, T172))
HIDDEN_FLATTEN1_IN_GAA(.(T137, .(.(T166, T167), T168)), T171, .(T137, T172)) → P10_IN_GAAGGA(T168, T171, X277, T166, T167, T172)
P10_IN_GAAGGA(.(.(T49, T50), T51), T53, X90, T11, T12, T54) → U2_GAAGGA(T49, T50, T51, T53, X90, T11, T12, T54, hidden_flatten23_in_gaa(T51, T53, X89))
P10_IN_GAAGGA(.(.(T49, T50), T51), T53, X90, T11, T12, T54) → HIDDEN_FLATTEN23_IN_GAA(T51, T53, X89)
HIDDEN_FLATTEN23_IN_GAA(.(.(T80, T81), T82), T84, X145) → U8_GAA(T80, T81, T82, T84, X145, hidden_flatten23_in_gaa(T82, T84, X144))
HIDDEN_FLATTEN23_IN_GAA(.(.(T80, T81), T82), T84, X145) → HIDDEN_FLATTEN23_IN_GAA(T82, T84, X144)
HIDDEN_FLATTEN23_IN_GAA(.(.(T80, T81), T82), T84, X145) → U9_GAA(T80, T81, T82, T84, X145, hidden_flattenc23_in_gaa(T82, T84, T87))
U9_GAA(T80, T81, T82, T84, X145, hidden_flattenc23_out_gaa(T82, T84, T87)) → U10_GAA(T80, T81, T82, T84, X145, hidden_flatten1_in_gaa(.(T80, T81), T87, X145))
U9_GAA(T80, T81, T82, T84, X145, hidden_flattenc23_out_gaa(T82, T84, T87)) → HIDDEN_FLATTEN1_IN_GAA(.(T80, T81), T87, X145)
HIDDEN_FLATTEN1_IN_GAA(.(T137, .(T183, T184)), T187, .(T137, .(T183, T188))) → U14_GAA(T137, T183, T184, T187, T188, hidden_flatten1_in_gaa(T184, T187, T188))
HIDDEN_FLATTEN1_IN_GAA(.(T137, .(T183, T184)), T187, .(T137, .(T183, T188))) → HIDDEN_FLATTEN1_IN_GAA(T184, T187, T188)
HIDDEN_FLATTEN23_IN_GAA(.(T100, T101), T103, .(T100, X178)) → U11_GAA(T100, T101, T103, X178, hidden_flatten23_in_gaa(T101, T103, X178))
HIDDEN_FLATTEN23_IN_GAA(.(T100, T101), T103, .(T100, X178)) → HIDDEN_FLATTEN23_IN_GAA(T101, T103, X178)
P10_IN_GAAGGA(.(.(T49, T50), T51), T53, X90, T11, T12, T58) → U3_GAAGGA(T49, T50, T51, T53, X90, T11, T12, T58, hidden_flattenc23_in_gaa(T51, T53, T57))
U3_GAAGGA(T49, T50, T51, T53, X90, T11, T12, T58, hidden_flattenc23_out_gaa(T51, T53, T57)) → U4_GAAGGA(T49, T50, T51, T53, X90, T11, T12, T58, p10_in_gaagga(.(T49, T50), T57, X90, T11, T12, T58))
U3_GAAGGA(T49, T50, T51, T53, X90, T11, T12, T58, hidden_flattenc23_out_gaa(T51, T53, T57)) → P10_IN_GAAGGA(.(T49, T50), T57, X90, T11, T12, T58)
P10_IN_GAAGGA(.(T116, T117), T119, .(T116, X208), T11, T12, T120) → U5_GAAGGA(T116, T117, T119, X208, T11, T12, T120, hidden_flatten23_in_gaa(T117, T119, X208))
P10_IN_GAAGGA(.(T116, T117), T119, .(T116, X208), T11, T12, T120) → HIDDEN_FLATTEN23_IN_GAA(T117, T119, X208)
P10_IN_GAAGGA(.(T116, T117), T119, .(T116, T123), T11, T12, T124) → U6_GAAGGA(T116, T117, T119, T123, T11, T12, T124, hidden_flattenc23_in_gaa(T117, T119, T123))
U6_GAAGGA(T116, T117, T119, T123, T11, T12, T124, hidden_flattenc23_out_gaa(T117, T119, T123)) → U7_GAAGGA(T116, T117, T119, T123, T11, T12, T124, hidden_flatten1_in_gaa(.(T11, T12), .(T116, T123), T124))
U6_GAAGGA(T116, T117, T119, T123, T11, T12, T124, hidden_flattenc23_out_gaa(T117, T119, T123)) → HIDDEN_FLATTEN1_IN_GAA(.(T11, T12), .(T116, T123), T124)

The TRS R consists of the following rules:

hidden_flattenc23_in_gaa([], T63, T63) → hidden_flattenc23_out_gaa([], T63, T63)
hidden_flattenc23_in_gaa(.(.(T80, T81), T82), T84, X145) → U24_gaa(T80, T81, T82, T84, X145, hidden_flattenc23_in_gaa(T82, T84, T87))
hidden_flattenc23_in_gaa(.(T100, T101), T103, .(T100, X178)) → U26_gaa(T100, T101, T103, X178, hidden_flattenc23_in_gaa(T101, T103, X178))
U26_gaa(T100, T101, T103, X178, hidden_flattenc23_out_gaa(T101, T103, X178)) → hidden_flattenc23_out_gaa(.(T100, T101), T103, .(T100, X178))
U24_gaa(T80, T81, T82, T84, X145, hidden_flattenc23_out_gaa(T82, T84, T87)) → U25_gaa(T80, T81, T82, T84, X145, hidden_flattenc1_in_gaa(.(T80, T81), T87, X145))
hidden_flattenc1_in_gaa([], T5, T5) → hidden_flattenc1_out_gaa([], T5, T5)
hidden_flattenc1_in_gaa(.(.(T11, T12), T13), T16, T17) → U16_gaa(T11, T12, T13, T16, T17, qc10_in_gaagga(T13, T16, X23, T11, T12, T17))
qc10_in_gaagga([], T21, T21, T11, T12, T22) → U19_gaagga(T21, T11, T12, T22, hidden_flattenc1_in_gaa(.(T11, T12), T21, T22))
hidden_flattenc1_in_gaa(.(T137, []), T145, .(T137, T145)) → hidden_flattenc1_out_gaa(.(T137, []), T145, .(T137, T145))
hidden_flattenc1_in_gaa(.(T137, .(.(T166, T167), T168)), T171, .(T137, T172)) → U17_gaa(T137, T166, T167, T168, T171, T172, qc10_in_gaagga(T168, T171, X277, T166, T167, T172))
qc10_in_gaagga(.(.(T49, T50), T51), T53, X90, T11, T12, T58) → U20_gaagga(T49, T50, T51, T53, X90, T11, T12, T58, hidden_flattenc23_in_gaa(T51, T53, T57))
U20_gaagga(T49, T50, T51, T53, X90, T11, T12, T58, hidden_flattenc23_out_gaa(T51, T53, T57)) → U21_gaagga(T49, T50, T51, T53, X90, T11, T12, T58, qc10_in_gaagga(.(T49, T50), T57, X90, T11, T12, T58))
qc10_in_gaagga(.(T116, T117), T119, .(T116, T123), T11, T12, T124) → U22_gaagga(T116, T117, T119, T123, T11, T12, T124, hidden_flattenc23_in_gaa(T117, T119, T123))
U22_gaagga(T116, T117, T119, T123, T11, T12, T124, hidden_flattenc23_out_gaa(T117, T119, T123)) → U23_gaagga(T116, T117, T119, T123, T11, T12, T124, hidden_flattenc1_in_gaa(.(T11, T12), .(T116, T123), T124))
hidden_flattenc1_in_gaa(.(T137, .(T183, T184)), T187, .(T137, .(T183, T188))) → U18_gaa(T137, T183, T184, T187, T188, hidden_flattenc1_in_gaa(T184, T187, T188))
U18_gaa(T137, T183, T184, T187, T188, hidden_flattenc1_out_gaa(T184, T187, T188)) → hidden_flattenc1_out_gaa(.(T137, .(T183, T184)), T187, .(T137, .(T183, T188)))
U23_gaagga(T116, T117, T119, T123, T11, T12, T124, hidden_flattenc1_out_gaa(.(T11, T12), .(T116, T123), T124)) → qc10_out_gaagga(.(T116, T117), T119, .(T116, T123), T11, T12, T124)
U21_gaagga(T49, T50, T51, T53, X90, T11, T12, T58, qc10_out_gaagga(.(T49, T50), T57, X90, T11, T12, T58)) → qc10_out_gaagga(.(.(T49, T50), T51), T53, X90, T11, T12, T58)
U17_gaa(T137, T166, T167, T168, T171, T172, qc10_out_gaagga(T168, T171, X277, T166, T167, T172)) → hidden_flattenc1_out_gaa(.(T137, .(.(T166, T167), T168)), T171, .(T137, T172))
U19_gaagga(T21, T11, T12, T22, hidden_flattenc1_out_gaa(.(T11, T12), T21, T22)) → qc10_out_gaagga([], T21, T21, T11, T12, T22)
U16_gaa(T11, T12, T13, T16, T17, qc10_out_gaagga(T13, T16, X23, T11, T12, T17)) → hidden_flattenc1_out_gaa(.(.(T11, T12), T13), T16, T17)
U25_gaa(T80, T81, T82, T84, X145, hidden_flattenc1_out_gaa(.(T80, T81), T87, X145)) → hidden_flattenc23_out_gaa(.(.(T80, T81), T82), T84, X145)

The argument filtering Pi contains the following mapping:
hidden_flatten1_in_gaa(x1, x2, x3) = hidden_flatten1_in_gaa(x1)
.(x1, x2) = .(x1, x2)
p10_in_gaagga(x1, x2, x3, x4, x5, x6) = p10_in_gaagga(x1, x4, x5)
[] = []
hidden_flatten23_in_gaa(x1, x2, x3) = hidden_flatten23_in_gaa(x1)
hidden_flattenc23_in_gaa(x1, x2, x3) = hidden_flattenc23_in_gaa(x1)
hidden_flattenc23_out_gaa(x1, x2, x3) = hidden_flattenc23_out_gaa(x1)
U24_gaa(x1, x2, x3, x4, x5, x6) = U24_gaa(x1, x2, x3, x6)
U26_gaa(x1, x2, x3, x4, x5) = U26_gaa(x1, x2, x5)
U25_gaa(x1, x2, x3, x4, x5, x6) = U25_gaa(x1, x2, x3, x6)
hidden_flattenc1_in_gaa(x1, x2, x3) = hidden_flattenc1_in_gaa(x1)
hidden_flattenc1_out_gaa(x1, x2, x3) = hidden_flattenc1_out_gaa(x1)
U16_gaa(x1, x2, x3, x4, x5, x6) = U16_gaa(x1, x2, x3, x6)
qc10_in_gaagga(x1, x2, x3, x4, x5, x6) = qc10_in_gaagga(x1, x4, x5)
U19_gaagga(x1, x2, x3, x4, x5) = U19_gaagga(x2, x3, x5)
U17_gaa(x1, x2, x3, x4, x5, x6, x7) = U17_gaa(x1, x2, x3, x4, x7)
U20_gaagga(x1, x2, x3, x4, x5, x6, x7, x8, x9) = U20_gaagga(x1, x2, x3, x6, x7, x9)
U21_gaagga(x1, x2, x3, x4, x5, x6, x7, x8, x9) = U21_gaagga(x1, x2, x3, x6, x7, x9)
U22_gaagga(x1, x2, x3, x4, x5, x6, x7, x8) = U22_gaagga(x1, x2, x5, x6, x8)
U23_gaagga(x1, x2, x3, x4, x5, x6, x7, x8) = U23_gaagga(x1, x2, x5, x6, x8)
U18_gaa(x1, x2, x3, x4, x5, x6) = U18_gaa(x1, x2, x3, x6)
qc10_out_gaagga(x1, x2, x3, x4, x5, x6) = qc10_out_gaagga(x1, x4, x5)
HIDDEN_FLATTEN1_IN_GAA(x1, x2, x3) = HIDDEN_FLATTEN1_IN_GAA(x1)
U12_GAA(x1, x2, x3, x4, x5, x6) = U12_GAA(x1, x2, x3, x6)
P10_IN_GAAGGA(x1, x2, x3, x4, x5, x6) = P10_IN_GAAGGA(x1, x4, x5)
U1_GAAGGA(x1, x2, x3, x4, x5) = U1_GAAGGA(x2, x3, x5)
U13_GAA(x1, x2, x3, x4, x5, x6, x7) = U13_GAA(x1, x2, x3, x4, x7)
U2_GAAGGA(x1, x2, x3, x4, x5, x6, x7, x8, x9) = U2_GAAGGA(x1, x2, x3, x6, x7, x9)
HIDDEN_FLATTEN23_IN_GAA(x1, x2, x3) = HIDDEN_FLATTEN23_IN_GAA(x1)
U8_GAA(x1, x2, x3, x4, x5, x6) = U8_GAA(x1, x2, x3, x6)
U9_GAA(x1, x2, x3, x4, x5, x6) = U9_GAA(x1, x2, x3, x6)
U10_GAA(x1, x2, x3, x4, x5, x6) = U10_GAA(x1, x2, x3, x6)
U14_GAA(x1, x2, x3, x4, x5, x6) = U14_GAA(x1, x2, x3, x6)
U11_GAA(x1, x2, x3, x4, x5) = U11_GAA(x1, x2, x5)
U3_GAAGGA(x1, x2, x3, x4, x5, x6, x7, x8, x9) = U3_GAAGGA(x1, x2, x3, x6, x7, x9)
U4_GAAGGA(x1, x2, x3, x4, x5, x6, x7, x8, x9) = U4_GAAGGA(x1, x2, x3, x6, x7, x9)
U5_GAAGGA(x1, x2, x3, x4, x5, x6, x7, x8) = U5_GAAGGA(x1, x2, x5, x6, x8)
U6_GAAGGA(x1, x2, x3, x4, x5, x6, x7, x8) = U6_GAAGGA(x1, x2, x5, x6, x8)
U7_GAAGGA(x1, x2, x3, x4, x5, x6, x7, x8) = U7_GAAGGA(x1, x2, x5, x6, x8)

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

Infinitary Constructor Rewriting Termination of PiDP implies Termination of TRIPLES

(4) Obligation:

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

HIDDEN_FLATTEN1_IN_GAA(.(.(T11, T12), T13), T16, T17) → U12_GAA(T11, T12, T13, T16, T17, p10_in_gaagga(T13, T16, X23, T11, T12, T17))
HIDDEN_FLATTEN1_IN_GAA(.(.(T11, T12), T13), T16, T17) → P10_IN_GAAGGA(T13, T16, X23, T11, T12, T17)
P10_IN_GAAGGA([], T21, T21, T11, T12, T22) → U1_GAAGGA(T21, T11, T12, T22, hidden_flatten1_in_gaa(.(T11, T12), T21, T22))
P10_IN_GAAGGA([], T21, T21, T11, T12, T22) → HIDDEN_FLATTEN1_IN_GAA(.(T11, T12), T21, T22)
HIDDEN_FLATTEN1_IN_GAA(.(T137, .(.(T166, T167), T168)), T171, .(T137, T172)) → U13_GAA(T137, T166, T167, T168, T171, T172, p10_in_gaagga(T168, T171, X277, T166, T167, T172))
HIDDEN_FLATTEN1_IN_GAA(.(T137, .(.(T166, T167), T168)), T171, .(T137, T172)) → P10_IN_GAAGGA(T168, T171, X277, T166, T167, T172)
P10_IN_GAAGGA(.(.(T49, T50), T51), T53, X90, T11, T12, T54) → U2_GAAGGA(T49, T50, T51, T53, X90, T11, T12, T54, hidden_flatten23_in_gaa(T51, T53, X89))
P10_IN_GAAGGA(.(.(T49, T50), T51), T53, X90, T11, T12, T54) → HIDDEN_FLATTEN23_IN_GAA(T51, T53, X89)
HIDDEN_FLATTEN23_IN_GAA(.(.(T80, T81), T82), T84, X145) → U8_GAA(T80, T81, T82, T84, X145, hidden_flatten23_in_gaa(T82, T84, X144))
HIDDEN_FLATTEN23_IN_GAA(.(.(T80, T81), T82), T84, X145) → HIDDEN_FLATTEN23_IN_GAA(T82, T84, X144)
HIDDEN_FLATTEN23_IN_GAA(.(.(T80, T81), T82), T84, X145) → U9_GAA(T80, T81, T82, T84, X145, hidden_flattenc23_in_gaa(T82, T84, T87))
U9_GAA(T80, T81, T82, T84, X145, hidden_flattenc23_out_gaa(T82, T84, T87)) → U10_GAA(T80, T81, T82, T84, X145, hidden_flatten1_in_gaa(.(T80, T81), T87, X145))
U9_GAA(T80, T81, T82, T84, X145, hidden_flattenc23_out_gaa(T82, T84, T87)) → HIDDEN_FLATTEN1_IN_GAA(.(T80, T81), T87, X145)
HIDDEN_FLATTEN1_IN_GAA(.(T137, .(T183, T184)), T187, .(T137, .(T183, T188))) → U14_GAA(T137, T183, T184, T187, T188, hidden_flatten1_in_gaa(T184, T187, T188))
HIDDEN_FLATTEN1_IN_GAA(.(T137, .(T183, T184)), T187, .(T137, .(T183, T188))) → HIDDEN_FLATTEN1_IN_GAA(T184, T187, T188)
HIDDEN_FLATTEN23_IN_GAA(.(T100, T101), T103, .(T100, X178)) → U11_GAA(T100, T101, T103, X178, hidden_flatten23_in_gaa(T101, T103, X178))
HIDDEN_FLATTEN23_IN_GAA(.(T100, T101), T103, .(T100, X178)) → HIDDEN_FLATTEN23_IN_GAA(T101, T103, X178)
P10_IN_GAAGGA(.(.(T49, T50), T51), T53, X90, T11, T12, T58) → U3_GAAGGA(T49, T50, T51, T53, X90, T11, T12, T58, hidden_flattenc23_in_gaa(T51, T53, T57))
U3_GAAGGA(T49, T50, T51, T53, X90, T11, T12, T58, hidden_flattenc23_out_gaa(T51, T53, T57)) → U4_GAAGGA(T49, T50, T51, T53, X90, T11, T12, T58, p10_in_gaagga(.(T49, T50), T57, X90, T11, T12, T58))
U3_GAAGGA(T49, T50, T51, T53, X90, T11, T12, T58, hidden_flattenc23_out_gaa(T51, T53, T57)) → P10_IN_GAAGGA(.(T49, T50), T57, X90, T11, T12, T58)
P10_IN_GAAGGA(.(T116, T117), T119, .(T116, X208), T11, T12, T120) → U5_GAAGGA(T116, T117, T119, X208, T11, T12, T120, hidden_flatten23_in_gaa(T117, T119, X208))
P10_IN_GAAGGA(.(T116, T117), T119, .(T116, X208), T11, T12, T120) → HIDDEN_FLATTEN23_IN_GAA(T117, T119, X208)
P10_IN_GAAGGA(.(T116, T117), T119, .(T116, T123), T11, T12, T124) → U6_GAAGGA(T116, T117, T119, T123, T11, T12, T124, hidden_flattenc23_in_gaa(T117, T119, T123))
U6_GAAGGA(T116, T117, T119, T123, T11, T12, T124, hidden_flattenc23_out_gaa(T117, T119, T123)) → U7_GAAGGA(T116, T117, T119, T123, T11, T12, T124, hidden_flatten1_in_gaa(.(T11, T12), .(T116, T123), T124))
U6_GAAGGA(T116, T117, T119, T123, T11, T12, T124, hidden_flattenc23_out_gaa(T117, T119, T123)) → HIDDEN_FLATTEN1_IN_GAA(.(T11, T12), .(T116, T123), T124)

The TRS R consists of the following rules:

hidden_flattenc23_in_gaa([], T63, T63) → hidden_flattenc23_out_gaa([], T63, T63)
hidden_flattenc23_in_gaa(.(.(T80, T81), T82), T84, X145) → U24_gaa(T80, T81, T82, T84, X145, hidden_flattenc23_in_gaa(T82, T84, T87))
hidden_flattenc23_in_gaa(.(T100, T101), T103, .(T100, X178)) → U26_gaa(T100, T101, T103, X178, hidden_flattenc23_in_gaa(T101, T103, X178))
U26_gaa(T100, T101, T103, X178, hidden_flattenc23_out_gaa(T101, T103, X178)) → hidden_flattenc23_out_gaa(.(T100, T101), T103, .(T100, X178))
U24_gaa(T80, T81, T82, T84, X145, hidden_flattenc23_out_gaa(T82, T84, T87)) → U25_gaa(T80, T81, T82, T84, X145, hidden_flattenc1_in_gaa(.(T80, T81), T87, X145))
hidden_flattenc1_in_gaa([], T5, T5) → hidden_flattenc1_out_gaa([], T5, T5)
hidden_flattenc1_in_gaa(.(.(T11, T12), T13), T16, T17) → U16_gaa(T11, T12, T13, T16, T17, qc10_in_gaagga(T13, T16, X23, T11, T12, T17))
qc10_in_gaagga([], T21, T21, T11, T12, T22) → U19_gaagga(T21, T11, T12, T22, hidden_flattenc1_in_gaa(.(T11, T12), T21, T22))
hidden_flattenc1_in_gaa(.(T137, []), T145, .(T137, T145)) → hidden_flattenc1_out_gaa(.(T137, []), T145, .(T137, T145))
hidden_flattenc1_in_gaa(.(T137, .(.(T166, T167), T168)), T171, .(T137, T172)) → U17_gaa(T137, T166, T167, T168, T171, T172, qc10_in_gaagga(T168, T171, X277, T166, T167, T172))
qc10_in_gaagga(.(.(T49, T50), T51), T53, X90, T11, T12, T58) → U20_gaagga(T49, T50, T51, T53, X90, T11, T12, T58, hidden_flattenc23_in_gaa(T51, T53, T57))
U20_gaagga(T49, T50, T51, T53, X90, T11, T12, T58, hidden_flattenc23_out_gaa(T51, T53, T57)) → U21_gaagga(T49, T50, T51, T53, X90, T11, T12, T58, qc10_in_gaagga(.(T49, T50), T57, X90, T11, T12, T58))
qc10_in_gaagga(.(T116, T117), T119, .(T116, T123), T11, T12, T124) → U22_gaagga(T116, T117, T119, T123, T11, T12, T124, hidden_flattenc23_in_gaa(T117, T119, T123))
U22_gaagga(T116, T117, T119, T123, T11, T12, T124, hidden_flattenc23_out_gaa(T117, T119, T123)) → U23_gaagga(T116, T117, T119, T123, T11, T12, T124, hidden_flattenc1_in_gaa(.(T11, T12), .(T116, T123), T124))
hidden_flattenc1_in_gaa(.(T137, .(T183, T184)), T187, .(T137, .(T183, T188))) → U18_gaa(T137, T183, T184, T187, T188, hidden_flattenc1_in_gaa(T184, T187, T188))
U18_gaa(T137, T183, T184, T187, T188, hidden_flattenc1_out_gaa(T184, T187, T188)) → hidden_flattenc1_out_gaa(.(T137, .(T183, T184)), T187, .(T137, .(T183, T188)))
U23_gaagga(T116, T117, T119, T123, T11, T12, T124, hidden_flattenc1_out_gaa(.(T11, T12), .(T116, T123), T124)) → qc10_out_gaagga(.(T116, T117), T119, .(T116, T123), T11, T12, T124)
U21_gaagga(T49, T50, T51, T53, X90, T11, T12, T58, qc10_out_gaagga(.(T49, T50), T57, X90, T11, T12, T58)) → qc10_out_gaagga(.(.(T49, T50), T51), T53, X90, T11, T12, T58)
U17_gaa(T137, T166, T167, T168, T171, T172, qc10_out_gaagga(T168, T171, X277, T166, T167, T172)) → hidden_flattenc1_out_gaa(.(T137, .(.(T166, T167), T168)), T171, .(T137, T172))
U19_gaagga(T21, T11, T12, T22, hidden_flattenc1_out_gaa(.(T11, T12), T21, T22)) → qc10_out_gaagga([], T21, T21, T11, T12, T22)
U16_gaa(T11, T12, T13, T16, T17, qc10_out_gaagga(T13, T16, X23, T11, T12, T17)) → hidden_flattenc1_out_gaa(.(.(T11, T12), T13), T16, T17)
U25_gaa(T80, T81, T82, T84, X145, hidden_flattenc1_out_gaa(.(T80, T81), T87, X145)) → hidden_flattenc23_out_gaa(.(.(T80, T81), T82), T84, X145)

(5) DependencyGraphProof (EQUIVALENT transformation)

The approximation of the Dependency Graph [LOPSTR] contains 1 SCC with 11 less nodes.

(6) Obligation:

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

HIDDEN_FLATTEN1_IN_GAA(.(.(T11, T12), T13), T16, T17) → P10_IN_GAAGGA(T13, T16, X23, T11, T12, T17)
P10_IN_GAAGGA([], T21, T21, T11, T12, T22) → HIDDEN_FLATTEN1_IN_GAA(.(T11, T12), T21, T22)
HIDDEN_FLATTEN1_IN_GAA(.(T137, .(.(T166, T167), T168)), T171, .(T137, T172)) → P10_IN_GAAGGA(T168, T171, X277, T166, T167, T172)
P10_IN_GAAGGA(.(.(T49, T50), T51), T53, X90, T11, T12, T54) → HIDDEN_FLATTEN23_IN_GAA(T51, T53, X89)
HIDDEN_FLATTEN23_IN_GAA(.(.(T80, T81), T82), T84, X145) → HIDDEN_FLATTEN23_IN_GAA(T82, T84, X144)
HIDDEN_FLATTEN23_IN_GAA(.(.(T80, T81), T82), T84, X145) → U9_GAA(T80, T81, T82, T84, X145, hidden_flattenc23_in_gaa(T82, T84, T87))
U9_GAA(T80, T81, T82, T84, X145, hidden_flattenc23_out_gaa(T82, T84, T87)) → HIDDEN_FLATTEN1_IN_GAA(.(T80, T81), T87, X145)
HIDDEN_FLATTEN1_IN_GAA(.(T137, .(T183, T184)), T187, .(T137, .(T183, T188))) → HIDDEN_FLATTEN1_IN_GAA(T184, T187, T188)
HIDDEN_FLATTEN23_IN_GAA(.(T100, T101), T103, .(T100, X178)) → HIDDEN_FLATTEN23_IN_GAA(T101, T103, X178)
P10_IN_GAAGGA(.(.(T49, T50), T51), T53, X90, T11, T12, T58) → U3_GAAGGA(T49, T50, T51, T53, X90, T11, T12, T58, hidden_flattenc23_in_gaa(T51, T53, T57))
U3_GAAGGA(T49, T50, T51, T53, X90, T11, T12, T58, hidden_flattenc23_out_gaa(T51, T53, T57)) → P10_IN_GAAGGA(.(T49, T50), T57, X90, T11, T12, T58)
P10_IN_GAAGGA(.(T116, T117), T119, .(T116, X208), T11, T12, T120) → HIDDEN_FLATTEN23_IN_GAA(T117, T119, X208)
P10_IN_GAAGGA(.(T116, T117), T119, .(T116, T123), T11, T12, T124) → U6_GAAGGA(T116, T117, T119, T123, T11, T12, T124, hidden_flattenc23_in_gaa(T117, T119, T123))
U6_GAAGGA(T116, T117, T119, T123, T11, T12, T124, hidden_flattenc23_out_gaa(T117, T119, T123)) → HIDDEN_FLATTEN1_IN_GAA(.(T11, T12), .(T116, T123), T124)

The TRS R consists of the following rules:

hidden_flattenc23_in_gaa([], T63, T63) → hidden_flattenc23_out_gaa([], T63, T63)
hidden_flattenc23_in_gaa(.(.(T80, T81), T82), T84, X145) → U24_gaa(T80, T81, T82, T84, X145, hidden_flattenc23_in_gaa(T82, T84, T87))
hidden_flattenc23_in_gaa(.(T100, T101), T103, .(T100, X178)) → U26_gaa(T100, T101, T103, X178, hidden_flattenc23_in_gaa(T101, T103, X178))
U26_gaa(T100, T101, T103, X178, hidden_flattenc23_out_gaa(T101, T103, X178)) → hidden_flattenc23_out_gaa(.(T100, T101), T103, .(T100, X178))
U24_gaa(T80, T81, T82, T84, X145, hidden_flattenc23_out_gaa(T82, T84, T87)) → U25_gaa(T80, T81, T82, T84, X145, hidden_flattenc1_in_gaa(.(T80, T81), T87, X145))
hidden_flattenc1_in_gaa([], T5, T5) → hidden_flattenc1_out_gaa([], T5, T5)
hidden_flattenc1_in_gaa(.(.(T11, T12), T13), T16, T17) → U16_gaa(T11, T12, T13, T16, T17, qc10_in_gaagga(T13, T16, X23, T11, T12, T17))
qc10_in_gaagga([], T21, T21, T11, T12, T22) → U19_gaagga(T21, T11, T12, T22, hidden_flattenc1_in_gaa(.(T11, T12), T21, T22))
hidden_flattenc1_in_gaa(.(T137, []), T145, .(T137, T145)) → hidden_flattenc1_out_gaa(.(T137, []), T145, .(T137, T145))
hidden_flattenc1_in_gaa(.(T137, .(.(T166, T167), T168)), T171, .(T137, T172)) → U17_gaa(T137, T166, T167, T168, T171, T172, qc10_in_gaagga(T168, T171, X277, T166, T167, T172))
qc10_in_gaagga(.(.(T49, T50), T51), T53, X90, T11, T12, T58) → U20_gaagga(T49, T50, T51, T53, X90, T11, T12, T58, hidden_flattenc23_in_gaa(T51, T53, T57))
U20_gaagga(T49, T50, T51, T53, X90, T11, T12, T58, hidden_flattenc23_out_gaa(T51, T53, T57)) → U21_gaagga(T49, T50, T51, T53, X90, T11, T12, T58, qc10_in_gaagga(.(T49, T50), T57, X90, T11, T12, T58))
qc10_in_gaagga(.(T116, T117), T119, .(T116, T123), T11, T12, T124) → U22_gaagga(T116, T117, T119, T123, T11, T12, T124, hidden_flattenc23_in_gaa(T117, T119, T123))
U22_gaagga(T116, T117, T119, T123, T11, T12, T124, hidden_flattenc23_out_gaa(T117, T119, T123)) → U23_gaagga(T116, T117, T119, T123, T11, T12, T124, hidden_flattenc1_in_gaa(.(T11, T12), .(T116, T123), T124))
hidden_flattenc1_in_gaa(.(T137, .(T183, T184)), T187, .(T137, .(T183, T188))) → U18_gaa(T137, T183, T184, T187, T188, hidden_flattenc1_in_gaa(T184, T187, T188))
U18_gaa(T137, T183, T184, T187, T188, hidden_flattenc1_out_gaa(T184, T187, T188)) → hidden_flattenc1_out_gaa(.(T137, .(T183, T184)), T187, .(T137, .(T183, T188)))
U23_gaagga(T116, T117, T119, T123, T11, T12, T124, hidden_flattenc1_out_gaa(.(T11, T12), .(T116, T123), T124)) → qc10_out_gaagga(.(T116, T117), T119, .(T116, T123), T11, T12, T124)
U21_gaagga(T49, T50, T51, T53, X90, T11, T12, T58, qc10_out_gaagga(.(T49, T50), T57, X90, T11, T12, T58)) → qc10_out_gaagga(.(.(T49, T50), T51), T53, X90, T11, T12, T58)
U17_gaa(T137, T166, T167, T168, T171, T172, qc10_out_gaagga(T168, T171, X277, T166, T167, T172)) → hidden_flattenc1_out_gaa(.(T137, .(.(T166, T167), T168)), T171, .(T137, T172))
U19_gaagga(T21, T11, T12, T22, hidden_flattenc1_out_gaa(.(T11, T12), T21, T22)) → qc10_out_gaagga([], T21, T21, T11, T12, T22)
U16_gaa(T11, T12, T13, T16, T17, qc10_out_gaagga(T13, T16, X23, T11, T12, T17)) → hidden_flattenc1_out_gaa(.(.(T11, T12), T13), T16, T17)
U25_gaa(T80, T81, T82, T84, X145, hidden_flattenc1_out_gaa(.(T80, T81), T87, X145)) → hidden_flattenc23_out_gaa(.(.(T80, T81), T82), T84, X145)

The argument filtering Pi contains the following mapping:
.(x1, x2) = .(x1, x2)
[] = []
hidden_flattenc23_in_gaa(x1, x2, x3) = hidden_flattenc23_in_gaa(x1)
hidden_flattenc23_out_gaa(x1, x2, x3) = hidden_flattenc23_out_gaa(x1)
U24_gaa(x1, x2, x3, x4, x5, x6) = U24_gaa(x1, x2, x3, x6)
U26_gaa(x1, x2, x3, x4, x5) = U26_gaa(x1, x2, x5)
U25_gaa(x1, x2, x3, x4, x5, x6) = U25_gaa(x1, x2, x3, x6)
hidden_flattenc1_in_gaa(x1, x2, x3) = hidden_flattenc1_in_gaa(x1)
hidden_flattenc1_out_gaa(x1, x2, x3) = hidden_flattenc1_out_gaa(x1)
U16_gaa(x1, x2, x3, x4, x5, x6) = U16_gaa(x1, x2, x3, x6)
qc10_in_gaagga(x1, x2, x3, x4, x5, x6) = qc10_in_gaagga(x1, x4, x5)
U19_gaagga(x1, x2, x3, x4, x5) = U19_gaagga(x2, x3, x5)
U17_gaa(x1, x2, x3, x4, x5, x6, x7) = U17_gaa(x1, x2, x3, x4, x7)
U20_gaagga(x1, x2, x3, x4, x5, x6, x7, x8, x9) = U20_gaagga(x1, x2, x3, x6, x7, x9)
U21_gaagga(x1, x2, x3, x4, x5, x6, x7, x8, x9) = U21_gaagga(x1, x2, x3, x6, x7, x9)
U22_gaagga(x1, x2, x3, x4, x5, x6, x7, x8) = U22_gaagga(x1, x2, x5, x6, x8)
U23_gaagga(x1, x2, x3, x4, x5, x6, x7, x8) = U23_gaagga(x1, x2, x5, x6, x8)
U18_gaa(x1, x2, x3, x4, x5, x6) = U18_gaa(x1, x2, x3, x6)
qc10_out_gaagga(x1, x2, x3, x4, x5, x6) = qc10_out_gaagga(x1, x4, x5)
HIDDEN_FLATTEN1_IN_GAA(x1, x2, x3) = HIDDEN_FLATTEN1_IN_GAA(x1)
P10_IN_GAAGGA(x1, x2, x3, x4, x5, x6) = P10_IN_GAAGGA(x1, x4, x5)
HIDDEN_FLATTEN23_IN_GAA(x1, x2, x3) = HIDDEN_FLATTEN23_IN_GAA(x1)
U9_GAA(x1, x2, x3, x4, x5, x6) = U9_GAA(x1, x2, x3, x6)
U3_GAAGGA(x1, x2, x3, x4, x5, x6, x7, x8, x9) = U3_GAAGGA(x1, x2, x3, x6, x7, x9)
U6_GAAGGA(x1, x2, x3, x4, x5, x6, x7, x8) = U6_GAAGGA(x1, x2, x5, x6, x8)

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

(7) PiDPToQDPProof (SOUND transformation)

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

(8) Obligation:

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

HIDDEN_FLATTEN1_IN_GAA(.(.(T11, T12), T13)) → P10_IN_GAAGGA(T13, T11, T12)
P10_IN_GAAGGA([], T11, T12) → HIDDEN_FLATTEN1_IN_GAA(.(T11, T12))
HIDDEN_FLATTEN1_IN_GAA(.(T137, .(.(T166, T167), T168))) → P10_IN_GAAGGA(T168, T166, T167)
P10_IN_GAAGGA(.(.(T49, T50), T51), T11, T12) → HIDDEN_FLATTEN23_IN_GAA(T51)
HIDDEN_FLATTEN23_IN_GAA(.(.(T80, T81), T82)) → HIDDEN_FLATTEN23_IN_GAA(T82)
HIDDEN_FLATTEN23_IN_GAA(.(.(T80, T81), T82)) → U9_GAA(T80, T81, T82, hidden_flattenc23_in_gaa(T82))
U9_GAA(T80, T81, T82, hidden_flattenc23_out_gaa(T82)) → HIDDEN_FLATTEN1_IN_GAA(.(T80, T81))
HIDDEN_FLATTEN1_IN_GAA(.(T137, .(T183, T184))) → HIDDEN_FLATTEN1_IN_GAA(T184)
HIDDEN_FLATTEN23_IN_GAA(.(T100, T101)) → HIDDEN_FLATTEN23_IN_GAA(T101)
P10_IN_GAAGGA(.(.(T49, T50), T51), T11, T12) → U3_GAAGGA(T49, T50, T51, T11, T12, hidden_flattenc23_in_gaa(T51))
U3_GAAGGA(T49, T50, T51, T11, T12, hidden_flattenc23_out_gaa(T51)) → P10_IN_GAAGGA(.(T49, T50), T11, T12)
P10_IN_GAAGGA(.(T116, T117), T11, T12) → HIDDEN_FLATTEN23_IN_GAA(T117)
P10_IN_GAAGGA(.(T116, T117), T11, T12) → U6_GAAGGA(T116, T117, T11, T12, hidden_flattenc23_in_gaa(T117))
U6_GAAGGA(T116, T117, T11, T12, hidden_flattenc23_out_gaa(T117)) → HIDDEN_FLATTEN1_IN_GAA(.(T11, T12))

The TRS R consists of the following rules:

hidden_flattenc23_in_gaa([]) → hidden_flattenc23_out_gaa([])
hidden_flattenc23_in_gaa(.(.(T80, T81), T82)) → U24_gaa(T80, T81, T82, hidden_flattenc23_in_gaa(T82))
hidden_flattenc23_in_gaa(.(T100, T101)) → U26_gaa(T100, T101, hidden_flattenc23_in_gaa(T101))
U26_gaa(T100, T101, hidden_flattenc23_out_gaa(T101)) → hidden_flattenc23_out_gaa(.(T100, T101))
U24_gaa(T80, T81, T82, hidden_flattenc23_out_gaa(T82)) → U25_gaa(T80, T81, T82, hidden_flattenc1_in_gaa(.(T80, T81)))
hidden_flattenc1_in_gaa([]) → hidden_flattenc1_out_gaa([])
hidden_flattenc1_in_gaa(.(.(T11, T12), T13)) → U16_gaa(T11, T12, T13, qc10_in_gaagga(T13, T11, T12))
qc10_in_gaagga([], T11, T12) → U19_gaagga(T11, T12, hidden_flattenc1_in_gaa(.(T11, T12)))
hidden_flattenc1_in_gaa(.(T137, [])) → hidden_flattenc1_out_gaa(.(T137, []))
hidden_flattenc1_in_gaa(.(T137, .(.(T166, T167), T168))) → U17_gaa(T137, T166, T167, T168, qc10_in_gaagga(T168, T166, T167))
qc10_in_gaagga(.(.(T49, T50), T51), T11, T12) → U20_gaagga(T49, T50, T51, T11, T12, hidden_flattenc23_in_gaa(T51))
U20_gaagga(T49, T50, T51, T11, T12, hidden_flattenc23_out_gaa(T51)) → U21_gaagga(T49, T50, T51, T11, T12, qc10_in_gaagga(.(T49, T50), T11, T12))
qc10_in_gaagga(.(T116, T117), T11, T12) → U22_gaagga(T116, T117, T11, T12, hidden_flattenc23_in_gaa(T117))
U22_gaagga(T116, T117, T11, T12, hidden_flattenc23_out_gaa(T117)) → U23_gaagga(T116, T117, T11, T12, hidden_flattenc1_in_gaa(.(T11, T12)))
hidden_flattenc1_in_gaa(.(T137, .(T183, T184))) → U18_gaa(T137, T183, T184, hidden_flattenc1_in_gaa(T184))
U18_gaa(T137, T183, T184, hidden_flattenc1_out_gaa(T184)) → hidden_flattenc1_out_gaa(.(T137, .(T183, T184)))
U23_gaagga(T116, T117, T11, T12, hidden_flattenc1_out_gaa(.(T11, T12))) → qc10_out_gaagga(.(T116, T117), T11, T12)
U21_gaagga(T49, T50, T51, T11, T12, qc10_out_gaagga(.(T49, T50), T11, T12)) → qc10_out_gaagga(.(.(T49, T50), T51), T11, T12)
U17_gaa(T137, T166, T167, T168, qc10_out_gaagga(T168, T166, T167)) → hidden_flattenc1_out_gaa(.(T137, .(.(T166, T167), T168)))
U19_gaagga(T11, T12, hidden_flattenc1_out_gaa(.(T11, T12))) → qc10_out_gaagga([], T11, T12)
U16_gaa(T11, T12, T13, qc10_out_gaagga(T13, T11, T12)) → hidden_flattenc1_out_gaa(.(.(T11, T12), T13))
U25_gaa(T80, T81, T82, hidden_flattenc1_out_gaa(.(T80, T81))) → hidden_flattenc23_out_gaa(.(.(T80, T81), T82))

The set Q consists of the following terms:

hidden_flattenc23_in_gaa(x0)
U26_gaa(x0, x1, x2)
U24_gaa(x0, x1, x2, x3)
hidden_flattenc1_in_gaa(x0)
qc10_in_gaagga(x0, x1, x2)
U20_gaagga(x0, x1, x2, x3, x4, x5)
U22_gaagga(x0, x1, x2, x3, x4)
U18_gaa(x0, x1, x2, x3)
U23_gaagga(x0, x1, x2, x3, x4)
U21_gaagga(x0, x1, x2, x3, x4, x5)
U17_gaa(x0, x1, x2, x3, x4)
U19_gaagga(x0, x1, x2)
U16_gaa(x0, x1, x2, x3)
U25_gaa(x0, x1, x2, x3)

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

(9) QDPOrderProof (EQUIVALENT transformation)

We use the reduction pair processor [LPAR04].

The following pairs can be oriented strictly and are deleted.

P10_IN_GAAGGA([], T11, T12) → HIDDEN_FLATTEN1_IN_GAA(.(T11, T12))

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

POL(.(x₁, x₂)) = x₁ + x₂
POL(HIDDEN_FLATTEN1_IN_GAA(x₁)) = x₁
POL(HIDDEN_FLATTEN23_IN_GAA(x₁)) = x₁
POL(P10_IN_GAAGGA(x₁, x₂, x₃)) = x₁ + x₂ + x₃
POL(U16_gaa(x₁, x₂, x₃, x₄)) = 0
POL(U17_gaa(x₁, x₂, x₃, x₄, x₅)) = 0
POL(U18_gaa(x₁, x₂, x₃, x₄)) = 0
POL(U19_gaagga(x₁, x₂, x₃)) = 0
POL(U20_gaagga(x₁, x₂, x₃, x₄, x₅, x₆)) = 0
POL(U21_gaagga(x₁, x₂, x₃, x₄, x₅, x₆)) = 0
POL(U22_gaagga(x₁, x₂, x₃, x₄, x₅)) = 0
POL(U23_gaagga(x₁, x₂, x₃, x₄, x₅)) = 0
POL(U24_gaa(x₁, x₂, x₃, x₄)) = 0
POL(U25_gaa(x₁, x₂, x₃, x₄)) = 0
POL(U26_gaa(x₁, x₂, x₃)) = 0
POL(U3_GAAGGA(x₁, x₂, x₃, x₄, x₅, x₆)) = x₁ + x₂ + x₄ + x₅
POL(U6_GAAGGA(x₁, x₂, x₃, x₄, x₅)) = x₃ + x₄
POL(U9_GAA(x₁, x₂, x₃, x₄)) = x₁ + x₂ + x₃
POL([]) = 1
POL(hidden_flattenc1_in_gaa(x₁)) = 1 + x₁
POL(hidden_flattenc1_out_gaa(x₁)) = x₁
POL(hidden_flattenc23_in_gaa(x₁)) = 0
POL(hidden_flattenc23_out_gaa(x₁)) = 0
POL(qc10_in_gaagga(x₁, x₂, x₃)) = 0
POL(qc10_out_gaagga(x₁, x₂, x₃)) = 0

The following usable rules [FROCOS05] were oriented: none

(10) Obligation:

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

HIDDEN_FLATTEN1_IN_GAA(.(.(T11, T12), T13)) → P10_IN_GAAGGA(T13, T11, T12)
HIDDEN_FLATTEN1_IN_GAA(.(T137, .(.(T166, T167), T168))) → P10_IN_GAAGGA(T168, T166, T167)
P10_IN_GAAGGA(.(.(T49, T50), T51), T11, T12) → HIDDEN_FLATTEN23_IN_GAA(T51)
HIDDEN_FLATTEN23_IN_GAA(.(.(T80, T81), T82)) → HIDDEN_FLATTEN23_IN_GAA(T82)
HIDDEN_FLATTEN23_IN_GAA(.(.(T80, T81), T82)) → U9_GAA(T80, T81, T82, hidden_flattenc23_in_gaa(T82))
U9_GAA(T80, T81, T82, hidden_flattenc23_out_gaa(T82)) → HIDDEN_FLATTEN1_IN_GAA(.(T80, T81))
HIDDEN_FLATTEN1_IN_GAA(.(T137, .(T183, T184))) → HIDDEN_FLATTEN1_IN_GAA(T184)
HIDDEN_FLATTEN23_IN_GAA(.(T100, T101)) → HIDDEN_FLATTEN23_IN_GAA(T101)
P10_IN_GAAGGA(.(.(T49, T50), T51), T11, T12) → U3_GAAGGA(T49, T50, T51, T11, T12, hidden_flattenc23_in_gaa(T51))
U3_GAAGGA(T49, T50, T51, T11, T12, hidden_flattenc23_out_gaa(T51)) → P10_IN_GAAGGA(.(T49, T50), T11, T12)
P10_IN_GAAGGA(.(T116, T117), T11, T12) → HIDDEN_FLATTEN23_IN_GAA(T117)
P10_IN_GAAGGA(.(T116, T117), T11, T12) → U6_GAAGGA(T116, T117, T11, T12, hidden_flattenc23_in_gaa(T117))
U6_GAAGGA(T116, T117, T11, T12, hidden_flattenc23_out_gaa(T117)) → HIDDEN_FLATTEN1_IN_GAA(.(T11, T12))

The TRS R consists of the following rules:

hidden_flattenc23_in_gaa([]) → hidden_flattenc23_out_gaa([])
hidden_flattenc23_in_gaa(.(.(T80, T81), T82)) → U24_gaa(T80, T81, T82, hidden_flattenc23_in_gaa(T82))
hidden_flattenc23_in_gaa(.(T100, T101)) → U26_gaa(T100, T101, hidden_flattenc23_in_gaa(T101))
U26_gaa(T100, T101, hidden_flattenc23_out_gaa(T101)) → hidden_flattenc23_out_gaa(.(T100, T101))
U24_gaa(T80, T81, T82, hidden_flattenc23_out_gaa(T82)) → U25_gaa(T80, T81, T82, hidden_flattenc1_in_gaa(.(T80, T81)))
hidden_flattenc1_in_gaa([]) → hidden_flattenc1_out_gaa([])
hidden_flattenc1_in_gaa(.(.(T11, T12), T13)) → U16_gaa(T11, T12, T13, qc10_in_gaagga(T13, T11, T12))
qc10_in_gaagga([], T11, T12) → U19_gaagga(T11, T12, hidden_flattenc1_in_gaa(.(T11, T12)))
hidden_flattenc1_in_gaa(.(T137, [])) → hidden_flattenc1_out_gaa(.(T137, []))
hidden_flattenc1_in_gaa(.(T137, .(.(T166, T167), T168))) → U17_gaa(T137, T166, T167, T168, qc10_in_gaagga(T168, T166, T167))
qc10_in_gaagga(.(.(T49, T50), T51), T11, T12) → U20_gaagga(T49, T50, T51, T11, T12, hidden_flattenc23_in_gaa(T51))
U20_gaagga(T49, T50, T51, T11, T12, hidden_flattenc23_out_gaa(T51)) → U21_gaagga(T49, T50, T51, T11, T12, qc10_in_gaagga(.(T49, T50), T11, T12))
qc10_in_gaagga(.(T116, T117), T11, T12) → U22_gaagga(T116, T117, T11, T12, hidden_flattenc23_in_gaa(T117))
U22_gaagga(T116, T117, T11, T12, hidden_flattenc23_out_gaa(T117)) → U23_gaagga(T116, T117, T11, T12, hidden_flattenc1_in_gaa(.(T11, T12)))
hidden_flattenc1_in_gaa(.(T137, .(T183, T184))) → U18_gaa(T137, T183, T184, hidden_flattenc1_in_gaa(T184))
U18_gaa(T137, T183, T184, hidden_flattenc1_out_gaa(T184)) → hidden_flattenc1_out_gaa(.(T137, .(T183, T184)))
U23_gaagga(T116, T117, T11, T12, hidden_flattenc1_out_gaa(.(T11, T12))) → qc10_out_gaagga(.(T116, T117), T11, T12)
U21_gaagga(T49, T50, T51, T11, T12, qc10_out_gaagga(.(T49, T50), T11, T12)) → qc10_out_gaagga(.(.(T49, T50), T51), T11, T12)
U17_gaa(T137, T166, T167, T168, qc10_out_gaagga(T168, T166, T167)) → hidden_flattenc1_out_gaa(.(T137, .(.(T166, T167), T168)))
U19_gaagga(T11, T12, hidden_flattenc1_out_gaa(.(T11, T12))) → qc10_out_gaagga([], T11, T12)
U16_gaa(T11, T12, T13, qc10_out_gaagga(T13, T11, T12)) → hidden_flattenc1_out_gaa(.(.(T11, T12), T13))
U25_gaa(T80, T81, T82, hidden_flattenc1_out_gaa(.(T80, T81))) → hidden_flattenc23_out_gaa(.(.(T80, T81), T82))

The set Q consists of the following terms:

hidden_flattenc23_in_gaa(x0)
U26_gaa(x0, x1, x2)
U24_gaa(x0, x1, x2, x3)
hidden_flattenc1_in_gaa(x0)
qc10_in_gaagga(x0, x1, x2)
U20_gaagga(x0, x1, x2, x3, x4, x5)
U22_gaagga(x0, x1, x2, x3, x4)
U18_gaa(x0, x1, x2, x3)
U23_gaagga(x0, x1, x2, x3, x4)
U21_gaagga(x0, x1, x2, x3, x4, x5)
U17_gaa(x0, x1, x2, x3, x4)
U19_gaagga(x0, x1, x2)
U16_gaa(x0, x1, x2, x3)
U25_gaa(x0, x1, x2, x3)

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

(11) QDPOrderProof (EQUIVALENT transformation)

We use the reduction pair processor [LPAR04].

The following pairs can be oriented strictly and are deleted.

HIDDEN_FLATTEN1_IN_GAA(.(.(T11, T12), T13)) → P10_IN_GAAGGA(T13, T11, T12)
HIDDEN_FLATTEN1_IN_GAA(.(T137, .(.(T166, T167), T168))) → P10_IN_GAAGGA(T168, T166, T167)
P10_IN_GAAGGA(.(.(T49, T50), T51), T11, T12) → HIDDEN_FLATTEN23_IN_GAA(T51)
HIDDEN_FLATTEN23_IN_GAA(.(.(T80, T81), T82)) → HIDDEN_FLATTEN23_IN_GAA(T82)
HIDDEN_FLATTEN23_IN_GAA(.(.(T80, T81), T82)) → U9_GAA(T80, T81, T82, hidden_flattenc23_in_gaa(T82))
HIDDEN_FLATTEN1_IN_GAA(.(T137, .(T183, T184))) → HIDDEN_FLATTEN1_IN_GAA(T184)
HIDDEN_FLATTEN23_IN_GAA(.(T100, T101)) → HIDDEN_FLATTEN23_IN_GAA(T101)
P10_IN_GAAGGA(.(.(T49, T50), T51), T11, T12) → U3_GAAGGA(T49, T50, T51, T11, T12, hidden_flattenc23_in_gaa(T51))

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

POL(.(x₁, x₂)) = 1 + x₁ + x₂
POL(HIDDEN_FLATTEN1_IN_GAA(x₁)) = x₁
POL(HIDDEN_FLATTEN23_IN_GAA(x₁)) = 1 + x₁
POL(P10_IN_GAAGGA(x₁, x₂, x₃)) = x₁ + x₂ + x₃
POL(U16_gaa(x₁, x₂, x₃, x₄)) = 0
POL(U17_gaa(x₁, x₂, x₃, x₄, x₅)) = 0
POL(U18_gaa(x₁, x₂, x₃, x₄)) = 0
POL(U19_gaagga(x₁, x₂, x₃)) = 0
POL(U20_gaagga(x₁, x₂, x₃, x₄, x₅, x₆)) = 0
POL(U21_gaagga(x₁, x₂, x₃, x₄, x₅, x₆)) = 0
POL(U22_gaagga(x₁, x₂, x₃, x₄, x₅)) = 0
POL(U23_gaagga(x₁, x₂, x₃, x₄, x₅)) = 0
POL(U24_gaa(x₁, x₂, x₃, x₄)) = 0
POL(U25_gaa(x₁, x₂, x₃, x₄)) = 0
POL(U26_gaa(x₁, x₂, x₃)) = 0
POL(U3_GAAGGA(x₁, x₂, x₃, x₄, x₅, x₆)) = 1 + x₁ + x₂ + x₄ + x₅
POL(U6_GAAGGA(x₁, x₂, x₃, x₄, x₅)) = 1 + x₃ + x₄
POL(U9_GAA(x₁, x₂, x₃, x₄)) = 1 + x₁ + x₂
POL([]) = 1
POL(hidden_flattenc1_in_gaa(x₁)) = 1 + x₁
POL(hidden_flattenc1_out_gaa(x₁)) = x₁
POL(hidden_flattenc23_in_gaa(x₁)) = 0
POL(hidden_flattenc23_out_gaa(x₁)) = 0
POL(qc10_in_gaagga(x₁, x₂, x₃)) = 0
POL(qc10_out_gaagga(x₁, x₂, x₃)) = 0

The following usable rules [FROCOS05] were oriented: none

(12) Obligation:

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

U9_GAA(T80, T81, T82, hidden_flattenc23_out_gaa(T82)) → HIDDEN_FLATTEN1_IN_GAA(.(T80, T81))
U3_GAAGGA(T49, T50, T51, T11, T12, hidden_flattenc23_out_gaa(T51)) → P10_IN_GAAGGA(.(T49, T50), T11, T12)
P10_IN_GAAGGA(.(T116, T117), T11, T12) → HIDDEN_FLATTEN23_IN_GAA(T117)
P10_IN_GAAGGA(.(T116, T117), T11, T12) → U6_GAAGGA(T116, T117, T11, T12, hidden_flattenc23_in_gaa(T117))
U6_GAAGGA(T116, T117, T11, T12, hidden_flattenc23_out_gaa(T117)) → HIDDEN_FLATTEN1_IN_GAA(.(T11, T12))

The TRS R consists of the following rules:

hidden_flattenc23_in_gaa([]) → hidden_flattenc23_out_gaa([])
hidden_flattenc23_in_gaa(.(.(T80, T81), T82)) → U24_gaa(T80, T81, T82, hidden_flattenc23_in_gaa(T82))
hidden_flattenc23_in_gaa(.(T100, T101)) → U26_gaa(T100, T101, hidden_flattenc23_in_gaa(T101))
U26_gaa(T100, T101, hidden_flattenc23_out_gaa(T101)) → hidden_flattenc23_out_gaa(.(T100, T101))
U24_gaa(T80, T81, T82, hidden_flattenc23_out_gaa(T82)) → U25_gaa(T80, T81, T82, hidden_flattenc1_in_gaa(.(T80, T81)))
hidden_flattenc1_in_gaa([]) → hidden_flattenc1_out_gaa([])
hidden_flattenc1_in_gaa(.(.(T11, T12), T13)) → U16_gaa(T11, T12, T13, qc10_in_gaagga(T13, T11, T12))
qc10_in_gaagga([], T11, T12) → U19_gaagga(T11, T12, hidden_flattenc1_in_gaa(.(T11, T12)))
hidden_flattenc1_in_gaa(.(T137, [])) → hidden_flattenc1_out_gaa(.(T137, []))
hidden_flattenc1_in_gaa(.(T137, .(.(T166, T167), T168))) → U17_gaa(T137, T166, T167, T168, qc10_in_gaagga(T168, T166, T167))
qc10_in_gaagga(.(.(T49, T50), T51), T11, T12) → U20_gaagga(T49, T50, T51, T11, T12, hidden_flattenc23_in_gaa(T51))
U20_gaagga(T49, T50, T51, T11, T12, hidden_flattenc23_out_gaa(T51)) → U21_gaagga(T49, T50, T51, T11, T12, qc10_in_gaagga(.(T49, T50), T11, T12))
qc10_in_gaagga(.(T116, T117), T11, T12) → U22_gaagga(T116, T117, T11, T12, hidden_flattenc23_in_gaa(T117))
U22_gaagga(T116, T117, T11, T12, hidden_flattenc23_out_gaa(T117)) → U23_gaagga(T116, T117, T11, T12, hidden_flattenc1_in_gaa(.(T11, T12)))
hidden_flattenc1_in_gaa(.(T137, .(T183, T184))) → U18_gaa(T137, T183, T184, hidden_flattenc1_in_gaa(T184))
U18_gaa(T137, T183, T184, hidden_flattenc1_out_gaa(T184)) → hidden_flattenc1_out_gaa(.(T137, .(T183, T184)))
U23_gaagga(T116, T117, T11, T12, hidden_flattenc1_out_gaa(.(T11, T12))) → qc10_out_gaagga(.(T116, T117), T11, T12)
U21_gaagga(T49, T50, T51, T11, T12, qc10_out_gaagga(.(T49, T50), T11, T12)) → qc10_out_gaagga(.(.(T49, T50), T51), T11, T12)
U17_gaa(T137, T166, T167, T168, qc10_out_gaagga(T168, T166, T167)) → hidden_flattenc1_out_gaa(.(T137, .(.(T166, T167), T168)))
U19_gaagga(T11, T12, hidden_flattenc1_out_gaa(.(T11, T12))) → qc10_out_gaagga([], T11, T12)
U16_gaa(T11, T12, T13, qc10_out_gaagga(T13, T11, T12)) → hidden_flattenc1_out_gaa(.(.(T11, T12), T13))
U25_gaa(T80, T81, T82, hidden_flattenc1_out_gaa(.(T80, T81))) → hidden_flattenc23_out_gaa(.(.(T80, T81), T82))

The set Q consists of the following terms:

hidden_flattenc23_in_gaa(x0)
U26_gaa(x0, x1, x2)
U24_gaa(x0, x1, x2, x3)
hidden_flattenc1_in_gaa(x0)
qc10_in_gaagga(x0, x1, x2)
U20_gaagga(x0, x1, x2, x3, x4, x5)
U22_gaagga(x0, x1, x2, x3, x4)
U18_gaa(x0, x1, x2, x3)
U23_gaagga(x0, x1, x2, x3, x4)
U21_gaagga(x0, x1, x2, x3, x4, x5)
U17_gaa(x0, x1, x2, x3, x4)
U19_gaagga(x0, x1, x2)
U16_gaa(x0, x1, x2, x3)
U25_gaa(x0, x1, x2, x3)

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

(13) DependencyGraphProof (EQUIVALENT transformation)

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

(0) Obligation:

(1) PrologToDTProblemTransformerProof (SOUND transformation)

(2) Obligation:

(3) TriplesToPiDPProof (SOUND transformation)

(4) Obligation:

(5) DependencyGraphProof (EQUIVALENT transformation)

(6) Obligation:

(7) PiDPToQDPProof (SOUND transformation)

(8) Obligation:

(9) QDPOrderProof (EQUIVALENT transformation)

(10) Obligation:

(11) QDPOrderProof (EQUIVALENT transformation)

(12) Obligation:

(13) DependencyGraphProof (EQUIVALENT transformation)

(14) TRUE