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

(0) Obligation:

Clauses:

transpose(A, B) :- transpose_aux(A, [], B).
transpose_aux(.(R, Rs), X1, .(C, Cs)) :- ','(row2col(R, .(C, Cs), Cols1, Accm), transpose_aux(Rs, Accm, Cols1)).
transpose_aux([], X, X).
row2col(.(X, Xs), .(.(X, Ys), Cols), .(Ys, Cols1), .([], As)) :- row2col(Xs, Cols, Cols1, As).
row2col([], [], [], []).

Query: transpose(a,g)

(1) PrologToPiTRSViaGraphTransformerProof (SOUND transformation)

Transformed Prolog program to (Pi-)TRS.

digraph dp_graph {
node [outthreshold=100, inthreshold=100];
2 [label="A: transpose(T1, T2)\n\nT2 is ground", fontsize=16, style=filled, fillcolor=lightyellow, color=red];
5 [label="5: transpose(T1, T2), SCOPE: 1, CLAUSE: 0\n\nT2 is ground", fontsize=16, style=filled, fillcolor=lightyellow];
7 [label="7: transpose_aux(T7, [], T6)\n\nT6 is ground", fontsize=16, style=filled, fillcolor=lightyellow];
10 [label="10: transpose_aux(T7, [], T6), SCOPE: 2, CLAUSE: 1 | transpose_aux(T7, [], T6), SCOPE: 2, CLAUSE: 2\n\nT6 is ground", fontsize=16, style=filled, fillcolor=lightyellow];
14 [label="14: transpose_aux(T7, [], T6), SCOPE: 2, CLAUSE: 1\n\nT6 is ground", fontsize=16, style=filled, fillcolor=lightyellow];
15 [label="15: transpose_aux(T7, [], T6), SCOPE: 2, CLAUSE: 2\n\nT6 is ground", fontsize=16, style=filled, fillcolor=lightyellow];
21 [label="B: ','(row2col(T28, .(T26, T27), X35, X36), transpose_aux(T29, X36, X35))\n\nT26 is ground\nT27 is ground\nX35 is free\nX36 is free", fontsize=16, style=filled, fillcolor=lightyellow];
22 [label="22: \n\n", fontsize=16, style=filled, fillcolor=lightyellow];
30 [label="D: row2col(T28, .(T26, T27), X35, X36)\n\nT26 is ground\nT27 is ground\nX35 is free\nX36 is free", fontsize=16, style=filled, fillcolor=lightyellow];
31 [label="E: transpose_aux(T36, T35, T34)\n\nT34 is ground\nT35 is ground", fontsize=16, style=filled, fillcolor=lightyellow];
35 [label="35: row2col(T28, .(T26, T27), X35, X36), SCOPE: 3, CLAUSE: 3 | row2col(T28, .(T26, T27), X35, X36), SCOPE: 3, CLAUSE: 4\n\nT26 is ground\nT27 is ground\nX35 is free\nX36 is free", fontsize=16, style=filled, fillcolor=lightyellow];
36 [label="36: row2col(T28, .(T26, T27), X35, X36), SCOPE: 3, CLAUSE: 3\n\nT26 is ground\nT27 is ground\nX35 is free\nX36 is free", fontsize=16, style=filled, fillcolor=lightyellow];
37 [label="37: row2col(T28, .(T26, T27), X35, X36), SCOPE: 3, CLAUSE: 4\n\nT26 is ground\nT27 is ground\nX35 is free\nX36 is free", fontsize=16, style=filled, fillcolor=lightyellow];
43 [label="C: row2col(T61, T60, X91, X92)\n\nT60 is ground\nX91 is free\nX92 is free", fontsize=16, style=filled, fillcolor=lightyellow];
44 [label="44: \n\n", fontsize=16, style=filled, fillcolor=lightyellow];
47 [label="47: row2col(T61, T60, X91, X92), SCOPE: 4, CLAUSE: 3 | row2col(T61, T60, X91, X92), SCOPE: 4, CLAUSE: 4\n\nT60 is ground\nX91 is free\nX92 is free", fontsize=16, style=filled, fillcolor=lightyellow];
48 [label="48: row2col(T61, T60, X91, X92), SCOPE: 4, CLAUSE: 3\n\nT60 is ground\nX91 is free\nX92 is free", fontsize=16, style=filled, fillcolor=lightyellow];
49 [label="49: row2col(T61, T60, X91, X92), SCOPE: 4, CLAUSE: 4\n\nT60 is ground\nX91 is free\nX92 is free", fontsize=16, style=filled, fillcolor=lightyellow];
59 [label="59: row2col(T86, T85, X139, X140)\n\nT85 is ground\nX139 is free\nX140 is free", fontsize=16, style=filled, fillcolor=lightyellow];
61 [label="61: \n\n", fontsize=16, style=filled, fillcolor=lightyellow];
66 [label="66: true\n\n", fontsize=16, style=filled, fillcolor=lightyellow];
67 [label="67: \n\n", fontsize=16, style=filled, fillcolor=lightyellow];
68 [label="68: \n\n", fontsize=16, style=filled, fillcolor=lightyellow];
69 [label="69: \n\n", fontsize=16, style=filled, fillcolor=lightyellow];
70 [label="70: transpose_aux(T36, T35, T34), SCOPE: 5, CLAUSE: 1 | transpose_aux(T36, T35, T34), SCOPE: 5, CLAUSE: 2\n\nT34 is ground\nT35 is ground", fontsize=16, style=filled, fillcolor=lightyellow];
73 [label="73: transpose_aux(T36, T35, T34), SCOPE: 5, CLAUSE: 1\n\nT34 is ground\nT35 is ground", fontsize=16, style=filled, fillcolor=lightyellow];
74 [label="74: transpose_aux(T36, T35, T34), SCOPE: 5, CLAUSE: 2\n\nT34 is ground\nT35 is ground", fontsize=16, style=filled, fillcolor=lightyellow];
87 [label="87: ','(row2col(T121, .(T119, T120), X185, X186), transpose_aux(T122, X186, X185))\n\nT119 is ground\nT120 is ground\nX185 is free\nX186 is free", fontsize=16, style=filled, fillcolor=lightyellow];
88 [label="88: \n\n", fontsize=16, style=filled, fillcolor=lightyellow];
92 [label="92: true\n\n", fontsize=16, style=filled, fillcolor=lightyellow];
93 [label="93: \n\n", fontsize=16, style=filled, fillcolor=lightyellow];
94 [label="94: \n\n", fontsize=16, style=filled, fillcolor=lightyellow];
95 [label="95: true\n\n", fontsize=16, style=filled, fillcolor=lightyellow];
96 [label="96: \n\n", fontsize=16, style=filled, fillcolor=lightyellow];
97 [label="97: \n\n", fontsize=16, style=filled, fillcolor=lightyellow];
98 [label="CASE", fontsize=14, style = filled, fillcolor = lightcyan];
2 -> 98 [arrowhead = none ];
98 -> 5;

99 [label="ONLY EVAL with clause\ntranspose(X4, X5) :- transpose_aux(X4, [], X5).\nand substitutionT1 -> T7,\nX4 -> T7,\nT2 -> T6,\nX5 -> T6,\nT5 -> T7", fontsize=14, style = filled, fillcolor = lightblue];
5 -> 99 [arrowhead = none ];
99 -> 7;

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

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

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

103 [label="EVAL with clause\ntranspose_aux(.(X30, X31), X32, .(X33, X34)) :- ','(row2col(X30, .(X33, X34), X35, X36), transpose_aux(X31, X36, X35)).\nand substitutionX30 -> T28,\nX31 -> T29,\nT7 -> .(T28, T29),\nX32 -> [],\nX33 -> T26,\nX34 -> T27,\nT6 -> .(T26, T27),\nT24 -> T28,\nT25 -> T29", fontsize=14, style = filled, fillcolor = lightblue];
14 -> 103 [arrowhead = none ];
103 -> 21;

104 [label="EVAL-BACKTRACK", fontsize=14, style = filled, fillcolor = lightgreen];
14 -> 104 [arrowhead = none ];
104 -> 22;

105 [label="EVAL with clause\ntranspose_aux([], X200, X200).\nand substitutionT7 -> [],\nX200 -> [],\nT6 -> []", fontsize=14, style = filled, fillcolor = lightblue];
15 -> 105 [arrowhead = none ];
105 -> 95;

106 [label="EVAL-BACKTRACK", fontsize=14, style = filled, fillcolor = lightgreen];
15 -> 106 [arrowhead = none ];
106 -> 96;

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

108 [label="SPLIT 2\nnew knowledge:\nT28 is ground\nT26 is ground\nT27 is ground\nT34 is ground\nT35 is ground\nreplacements:X35 -> T34,\nX36 -> T35,\nT29 -> T36", fontsize=14, style = filled, fillcolor = violet];
21 -> 108 [arrowhead = none ];
108 -> 31;

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

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

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

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

113 [label="EVAL with clause\nrow2col(.(X85, X86), .(.(X85, X87), X88), .(X87, X89), .([], X90)) :- row2col(X86, X88, X89, X90).\nand substitutionX85 -> T57,\nX86 -> T61,\nT28 -> .(T57, T61),\nX87 -> T59,\nT26 -> .(T57, T59),\nT27 -> T60,\nX88 -> T60,\nX89 -> X91,\nX35 -> .(T59, X91),\nX90 -> X92,\nX36 -> .([], X92),\nT58 -> T61", fontsize=14, style = filled, fillcolor = lightblue];
36 -> 113 [arrowhead = none ];
113 -> 43;

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

115 [label="BACKTRACK\nfor clause: row2col([], [], [], [])because of non-unification", fontsize=14, style = filled, fillcolor = lightgreen];
37 -> 115 [arrowhead = none ];
115 -> 69;

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

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

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

119 [label="EVAL with clause\nrow2col(.(X133, X134), .(.(X133, X135), X136), .(X135, X137), .([], X138)) :- row2col(X134, X136, X137, X138).\nand substitutionX133 -> T82,\nX134 -> T86,\nT61 -> .(T82, T86),\nX135 -> T84,\nX136 -> T85,\nT60 -> .(.(T82, T84), T85),\nX137 -> X139,\nX91 -> .(T84, X139),\nX138 -> X140,\nX92 -> .([], X140),\nT83 -> T86", fontsize=14, style = filled, fillcolor = lightblue];
48 -> 119 [arrowhead = none ];
119 -> 59;

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

121 [label="EVAL with clause\nrow2col([], [], [], []).\nand substitutionT61 -> [],\nT60 -> [],\nX91 -> [],\nX92 -> []", fontsize=14, style = filled, fillcolor = lightblue];
49 -> 121 [arrowhead = none ];
121 -> 66;

122 [label="EVAL-BACKTRACK", fontsize=14, style = filled, fillcolor = lightgreen];
49 -> 122 [arrowhead = none ];
122 -> 67;

123 [label="INSTANCE with matching:\nT61 -> T86\nT60 -> T85\nX91 -> X139\nX92 -> X140", fontsize=14, style = filled, fillcolor = lightgrey];
59 -> 123 [arrowhead = none , style=dashed];
123 -> 43[style=dashed];

124 [label="SUCCESS", fontsize=14, style = filled, fillcolor = lightgreen];
66 -> 124 [arrowhead = none ];
124 -> 68;

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

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

127 [label="EVAL with clause\ntranspose_aux(.(X180, X181), X182, .(X183, X184)) :- ','(row2col(X180, .(X183, X184), X185, X186), transpose_aux(X181, X186, X185)).\nand substitutionX180 -> T121,\nX181 -> T122,\nT36 -> .(T121, T122),\nT35 -> T118,\nX182 -> T118,\nX183 -> T119,\nX184 -> T120,\nT34 -> .(T119, T120),\nT116 -> T121,\nT117 -> T122", fontsize=14, style = filled, fillcolor = lightblue];
73 -> 127 [arrowhead = none ];
127 -> 87;

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

129 [label="EVAL with clause\ntranspose_aux([], X197, X197).\nand substitutionT36 -> [],\nT35 -> T129,\nX197 -> T129,\nT34 -> T129", fontsize=14, style = filled, fillcolor = lightblue];
74 -> 129 [arrowhead = none ];
129 -> 92;

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

131 [label="INSTANCE with matching:\nT28 -> T121\nT26 -> T119\nT27 -> T120\nX35 -> X185\nX36 -> X186\nT29 -> T122", fontsize=14, style = filled, fillcolor = lightgrey];
87 -> 131 [arrowhead = none , style=dashed];
131 -> 21[style=dashed];

132 [label="SUCCESS", fontsize=14, style = filled, fillcolor = lightgreen];
92 -> 132 [arrowhead = none ];
132 -> 94;

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

}

(2) Obligation:

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

transposeA_in_ag(.(T28, T29), .(T26, T27)) → U1_ag(T28, T29, T26, T27, pB_in_aggaaa(T28, T26, T27, X35, X36, T29))
pB_in_aggaaa(T28, T26, T27, T34, T35, T36) → U5_aggaaa(T28, T26, T27, T34, T35, T36, row2colD_in_aggaa(T28, T26, T27, T34, T35))
row2colD_in_aggaa(.(T57, T61), .(T57, T59), T60, .(T59, X91), .([], X92)) → U3_aggaa(T57, T61, T59, T60, X91, X92, row2colC_in_agaa(T61, T60, X91, X92))
row2colC_in_agaa(.(T82, T86), .(.(T82, T84), T85), .(T84, X139), .([], X140)) → U2_agaa(T82, T86, T84, T85, X139, X140, row2colC_in_agaa(T86, T85, X139, X140))
row2colC_in_agaa([], [], [], []) → row2colC_out_agaa([], [], [], [])
U2_agaa(T82, T86, T84, T85, X139, X140, row2colC_out_agaa(T86, T85, X139, X140)) → row2colC_out_agaa(.(T82, T86), .(.(T82, T84), T85), .(T84, X139), .([], X140))
U3_aggaa(T57, T61, T59, T60, X91, X92, row2colC_out_agaa(T61, T60, X91, X92)) → row2colD_out_aggaa(.(T57, T61), .(T57, T59), T60, .(T59, X91), .([], X92))
U5_aggaaa(T28, T26, T27, T34, T35, T36, row2colD_out_aggaa(T28, T26, T27, T34, T35)) → U6_aggaaa(T28, T26, T27, T34, T35, T36, transpose_auxE_in_agg(T36, T35, T34))
transpose_auxE_in_agg(.(T121, T122), T118, .(T119, T120)) → U4_agg(T121, T122, T118, T119, T120, pB_in_aggaaa(T121, T119, T120, X185, X186, T122))
U4_agg(T121, T122, T118, T119, T120, pB_out_aggaaa(T121, T119, T120, X185, X186, T122)) → transpose_auxE_out_agg(.(T121, T122), T118, .(T119, T120))
transpose_auxE_in_agg([], T129, T129) → transpose_auxE_out_agg([], T129, T129)
U6_aggaaa(T28, T26, T27, T34, T35, T36, transpose_auxE_out_agg(T36, T35, T34)) → pB_out_aggaaa(T28, T26, T27, T34, T35, T36)
U1_ag(T28, T29, T26, T27, pB_out_aggaaa(T28, T26, T27, X35, X36, T29)) → transposeA_out_ag(.(T28, T29), .(T26, T27))
transposeA_in_ag([], []) → transposeA_out_ag([], [])

The argument filtering Pi contains the following mapping:
transposeA_in_ag(x1, x2)  =  transposeA_in_ag(x2)
.(x1, x2)  =  .(x1, x2)
U1_ag(x1, x2, x3, x4, x5)  =  U1_ag(x3, x4, x5)
pB_in_aggaaa(x1, x2, x3, x4, x5, x6)  =  pB_in_aggaaa(x2, x3)
U5_aggaaa(x1, x2, x3, x4, x5, x6, x7)  =  U5_aggaaa(x2, x3, x7)
row2colD_in_aggaa(x1, x2, x3, x4, x5)  =  row2colD_in_aggaa(x2, x3)
U3_aggaa(x1, x2, x3, x4, x5, x6, x7)  =  U3_aggaa(x1, x3, x4, x7)
row2colC_in_agaa(x1, x2, x3, x4)  =  row2colC_in_agaa(x2)
U2_agaa(x1, x2, x3, x4, x5, x6, x7)  =  U2_agaa(x1, x3, x4, x7)
[]  =  []
row2colC_out_agaa(x1, x2, x3, x4)  =  row2colC_out_agaa(x1, x2, x3, x4)
row2colD_out_aggaa(x1, x2, x3, x4, x5)  =  row2colD_out_aggaa(x1, x2, x3, x4, x5)
U6_aggaaa(x1, x2, x3, x4, x5, x6, x7)  =  U6_aggaaa(x1, x2, x3, x4, x5, x7)
transpose_auxE_in_agg(x1, x2, x3)  =  transpose_auxE_in_agg(x2, x3)
U4_agg(x1, x2, x3, x4, x5, x6)  =  U4_agg(x3, x4, x5, x6)
pB_out_aggaaa(x1, x2, x3, x4, x5, x6)  =  pB_out_aggaaa(x1, x2, x3, x4, x5, x6)
transpose_auxE_out_agg(x1, x2, x3)  =  transpose_auxE_out_agg(x1, x2, x3)
transposeA_out_ag(x1, x2)  =  transposeA_out_ag(x1, x2)

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

TRANSPOSEA_IN_AG(.(T28, T29), .(T26, T27)) → U1_AG(T28, T29, T26, T27, pB_in_aggaaa(T28, T26, T27, X35, X36, T29))
TRANSPOSEA_IN_AG(.(T28, T29), .(T26, T27)) → PB_IN_AGGAAA(T28, T26, T27, X35, X36, T29)
PB_IN_AGGAAA(T28, T26, T27, T34, T35, T36) → U5_AGGAAA(T28, T26, T27, T34, T35, T36, row2colD_in_aggaa(T28, T26, T27, T34, T35))
PB_IN_AGGAAA(T28, T26, T27, T34, T35, T36) → ROW2COLD_IN_AGGAA(T28, T26, T27, T34, T35)
ROW2COLD_IN_AGGAA(.(T57, T61), .(T57, T59), T60, .(T59, X91), .([], X92)) → U3_AGGAA(T57, T61, T59, T60, X91, X92, row2colC_in_agaa(T61, T60, X91, X92))
ROW2COLD_IN_AGGAA(.(T57, T61), .(T57, T59), T60, .(T59, X91), .([], X92)) → ROW2COLC_IN_AGAA(T61, T60, X91, X92)
ROW2COLC_IN_AGAA(.(T82, T86), .(.(T82, T84), T85), .(T84, X139), .([], X140)) → U2_AGAA(T82, T86, T84, T85, X139, X140, row2colC_in_agaa(T86, T85, X139, X140))
ROW2COLC_IN_AGAA(.(T82, T86), .(.(T82, T84), T85), .(T84, X139), .([], X140)) → ROW2COLC_IN_AGAA(T86, T85, X139, X140)
U5_AGGAAA(T28, T26, T27, T34, T35, T36, row2colD_out_aggaa(T28, T26, T27, T34, T35)) → U6_AGGAAA(T28, T26, T27, T34, T35, T36, transpose_auxE_in_agg(T36, T35, T34))
U5_AGGAAA(T28, T26, T27, T34, T35, T36, row2colD_out_aggaa(T28, T26, T27, T34, T35)) → TRANSPOSE_AUXE_IN_AGG(T36, T35, T34)
TRANSPOSE_AUXE_IN_AGG(.(T121, T122), T118, .(T119, T120)) → U4_AGG(T121, T122, T118, T119, T120, pB_in_aggaaa(T121, T119, T120, X185, X186, T122))
TRANSPOSE_AUXE_IN_AGG(.(T121, T122), T118, .(T119, T120)) → PB_IN_AGGAAA(T121, T119, T120, X185, X186, T122)

The TRS R consists of the following rules:

transposeA_in_ag(.(T28, T29), .(T26, T27)) → U1_ag(T28, T29, T26, T27, pB_in_aggaaa(T28, T26, T27, X35, X36, T29))
pB_in_aggaaa(T28, T26, T27, T34, T35, T36) → U5_aggaaa(T28, T26, T27, T34, T35, T36, row2colD_in_aggaa(T28, T26, T27, T34, T35))
row2colD_in_aggaa(.(T57, T61), .(T57, T59), T60, .(T59, X91), .([], X92)) → U3_aggaa(T57, T61, T59, T60, X91, X92, row2colC_in_agaa(T61, T60, X91, X92))
row2colC_in_agaa(.(T82, T86), .(.(T82, T84), T85), .(T84, X139), .([], X140)) → U2_agaa(T82, T86, T84, T85, X139, X140, row2colC_in_agaa(T86, T85, X139, X140))
row2colC_in_agaa([], [], [], []) → row2colC_out_agaa([], [], [], [])
U2_agaa(T82, T86, T84, T85, X139, X140, row2colC_out_agaa(T86, T85, X139, X140)) → row2colC_out_agaa(.(T82, T86), .(.(T82, T84), T85), .(T84, X139), .([], X140))
U3_aggaa(T57, T61, T59, T60, X91, X92, row2colC_out_agaa(T61, T60, X91, X92)) → row2colD_out_aggaa(.(T57, T61), .(T57, T59), T60, .(T59, X91), .([], X92))
U5_aggaaa(T28, T26, T27, T34, T35, T36, row2colD_out_aggaa(T28, T26, T27, T34, T35)) → U6_aggaaa(T28, T26, T27, T34, T35, T36, transpose_auxE_in_agg(T36, T35, T34))
transpose_auxE_in_agg(.(T121, T122), T118, .(T119, T120)) → U4_agg(T121, T122, T118, T119, T120, pB_in_aggaaa(T121, T119, T120, X185, X186, T122))
U4_agg(T121, T122, T118, T119, T120, pB_out_aggaaa(T121, T119, T120, X185, X186, T122)) → transpose_auxE_out_agg(.(T121, T122), T118, .(T119, T120))
transpose_auxE_in_agg([], T129, T129) → transpose_auxE_out_agg([], T129, T129)
U6_aggaaa(T28, T26, T27, T34, T35, T36, transpose_auxE_out_agg(T36, T35, T34)) → pB_out_aggaaa(T28, T26, T27, T34, T35, T36)
U1_ag(T28, T29, T26, T27, pB_out_aggaaa(T28, T26, T27, X35, X36, T29)) → transposeA_out_ag(.(T28, T29), .(T26, T27))
transposeA_in_ag([], []) → transposeA_out_ag([], [])

The argument filtering Pi contains the following mapping:
transposeA_in_ag(x1, x2)  =  transposeA_in_ag(x2)
.(x1, x2)  =  .(x1, x2)
U1_ag(x1, x2, x3, x4, x5)  =  U1_ag(x3, x4, x5)
pB_in_aggaaa(x1, x2, x3, x4, x5, x6)  =  pB_in_aggaaa(x2, x3)
U5_aggaaa(x1, x2, x3, x4, x5, x6, x7)  =  U5_aggaaa(x2, x3, x7)
row2colD_in_aggaa(x1, x2, x3, x4, x5)  =  row2colD_in_aggaa(x2, x3)
U3_aggaa(x1, x2, x3, x4, x5, x6, x7)  =  U3_aggaa(x1, x3, x4, x7)
row2colC_in_agaa(x1, x2, x3, x4)  =  row2colC_in_agaa(x2)
U2_agaa(x1, x2, x3, x4, x5, x6, x7)  =  U2_agaa(x1, x3, x4, x7)
[]  =  []
row2colC_out_agaa(x1, x2, x3, x4)  =  row2colC_out_agaa(x1, x2, x3, x4)
row2colD_out_aggaa(x1, x2, x3, x4, x5)  =  row2colD_out_aggaa(x1, x2, x3, x4, x5)
U6_aggaaa(x1, x2, x3, x4, x5, x6, x7)  =  U6_aggaaa(x1, x2, x3, x4, x5, x7)
transpose_auxE_in_agg(x1, x2, x3)  =  transpose_auxE_in_agg(x2, x3)
U4_agg(x1, x2, x3, x4, x5, x6)  =  U4_agg(x3, x4, x5, x6)
pB_out_aggaaa(x1, x2, x3, x4, x5, x6)  =  pB_out_aggaaa(x1, x2, x3, x4, x5, x6)
transpose_auxE_out_agg(x1, x2, x3)  =  transpose_auxE_out_agg(x1, x2, x3)
transposeA_out_ag(x1, x2)  =  transposeA_out_ag(x1, x2)
TRANSPOSEA_IN_AG(x1, x2)  =  TRANSPOSEA_IN_AG(x2)
U1_AG(x1, x2, x3, x4, x5)  =  U1_AG(x3, x4, x5)
PB_IN_AGGAAA(x1, x2, x3, x4, x5, x6)  =  PB_IN_AGGAAA(x2, x3)
U5_AGGAAA(x1, x2, x3, x4, x5, x6, x7)  =  U5_AGGAAA(x2, x3, x7)
ROW2COLD_IN_AGGAA(x1, x2, x3, x4, x5)  =  ROW2COLD_IN_AGGAA(x2, x3)
U3_AGGAA(x1, x2, x3, x4, x5, x6, x7)  =  U3_AGGAA(x1, x3, x4, x7)
ROW2COLC_IN_AGAA(x1, x2, x3, x4)  =  ROW2COLC_IN_AGAA(x2)
U2_AGAA(x1, x2, x3, x4, x5, x6, x7)  =  U2_AGAA(x1, x3, x4, x7)
U6_AGGAAA(x1, x2, x3, x4, x5, x6, x7)  =  U6_AGGAAA(x1, x2, x3, x4, x5, x7)
TRANSPOSE_AUXE_IN_AGG(x1, x2, x3)  =  TRANSPOSE_AUXE_IN_AGG(x2, x3)
U4_AGG(x1, x2, x3, x4, x5, x6)  =  U4_AGG(x3, x4, x5, x6)

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

(4) Obligation:

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

TRANSPOSEA_IN_AG(.(T28, T29), .(T26, T27)) → U1_AG(T28, T29, T26, T27, pB_in_aggaaa(T28, T26, T27, X35, X36, T29))
TRANSPOSEA_IN_AG(.(T28, T29), .(T26, T27)) → PB_IN_AGGAAA(T28, T26, T27, X35, X36, T29)
PB_IN_AGGAAA(T28, T26, T27, T34, T35, T36) → U5_AGGAAA(T28, T26, T27, T34, T35, T36, row2colD_in_aggaa(T28, T26, T27, T34, T35))
PB_IN_AGGAAA(T28, T26, T27, T34, T35, T36) → ROW2COLD_IN_AGGAA(T28, T26, T27, T34, T35)
ROW2COLD_IN_AGGAA(.(T57, T61), .(T57, T59), T60, .(T59, X91), .([], X92)) → U3_AGGAA(T57, T61, T59, T60, X91, X92, row2colC_in_agaa(T61, T60, X91, X92))
ROW2COLD_IN_AGGAA(.(T57, T61), .(T57, T59), T60, .(T59, X91), .([], X92)) → ROW2COLC_IN_AGAA(T61, T60, X91, X92)
ROW2COLC_IN_AGAA(.(T82, T86), .(.(T82, T84), T85), .(T84, X139), .([], X140)) → U2_AGAA(T82, T86, T84, T85, X139, X140, row2colC_in_agaa(T86, T85, X139, X140))
ROW2COLC_IN_AGAA(.(T82, T86), .(.(T82, T84), T85), .(T84, X139), .([], X140)) → ROW2COLC_IN_AGAA(T86, T85, X139, X140)
U5_AGGAAA(T28, T26, T27, T34, T35, T36, row2colD_out_aggaa(T28, T26, T27, T34, T35)) → U6_AGGAAA(T28, T26, T27, T34, T35, T36, transpose_auxE_in_agg(T36, T35, T34))
U5_AGGAAA(T28, T26, T27, T34, T35, T36, row2colD_out_aggaa(T28, T26, T27, T34, T35)) → TRANSPOSE_AUXE_IN_AGG(T36, T35, T34)
TRANSPOSE_AUXE_IN_AGG(.(T121, T122), T118, .(T119, T120)) → U4_AGG(T121, T122, T118, T119, T120, pB_in_aggaaa(T121, T119, T120, X185, X186, T122))
TRANSPOSE_AUXE_IN_AGG(.(T121, T122), T118, .(T119, T120)) → PB_IN_AGGAAA(T121, T119, T120, X185, X186, T122)

The TRS R consists of the following rules:

transposeA_in_ag(.(T28, T29), .(T26, T27)) → U1_ag(T28, T29, T26, T27, pB_in_aggaaa(T28, T26, T27, X35, X36, T29))
pB_in_aggaaa(T28, T26, T27, T34, T35, T36) → U5_aggaaa(T28, T26, T27, T34, T35, T36, row2colD_in_aggaa(T28, T26, T27, T34, T35))
row2colD_in_aggaa(.(T57, T61), .(T57, T59), T60, .(T59, X91), .([], X92)) → U3_aggaa(T57, T61, T59, T60, X91, X92, row2colC_in_agaa(T61, T60, X91, X92))
row2colC_in_agaa(.(T82, T86), .(.(T82, T84), T85), .(T84, X139), .([], X140)) → U2_agaa(T82, T86, T84, T85, X139, X140, row2colC_in_agaa(T86, T85, X139, X140))
row2colC_in_agaa([], [], [], []) → row2colC_out_agaa([], [], [], [])
U2_agaa(T82, T86, T84, T85, X139, X140, row2colC_out_agaa(T86, T85, X139, X140)) → row2colC_out_agaa(.(T82, T86), .(.(T82, T84), T85), .(T84, X139), .([], X140))
U3_aggaa(T57, T61, T59, T60, X91, X92, row2colC_out_agaa(T61, T60, X91, X92)) → row2colD_out_aggaa(.(T57, T61), .(T57, T59), T60, .(T59, X91), .([], X92))
U5_aggaaa(T28, T26, T27, T34, T35, T36, row2colD_out_aggaa(T28, T26, T27, T34, T35)) → U6_aggaaa(T28, T26, T27, T34, T35, T36, transpose_auxE_in_agg(T36, T35, T34))
transpose_auxE_in_agg(.(T121, T122), T118, .(T119, T120)) → U4_agg(T121, T122, T118, T119, T120, pB_in_aggaaa(T121, T119, T120, X185, X186, T122))
U4_agg(T121, T122, T118, T119, T120, pB_out_aggaaa(T121, T119, T120, X185, X186, T122)) → transpose_auxE_out_agg(.(T121, T122), T118, .(T119, T120))
transpose_auxE_in_agg([], T129, T129) → transpose_auxE_out_agg([], T129, T129)
U6_aggaaa(T28, T26, T27, T34, T35, T36, transpose_auxE_out_agg(T36, T35, T34)) → pB_out_aggaaa(T28, T26, T27, T34, T35, T36)
U1_ag(T28, T29, T26, T27, pB_out_aggaaa(T28, T26, T27, X35, X36, T29)) → transposeA_out_ag(.(T28, T29), .(T26, T27))
transposeA_in_ag([], []) → transposeA_out_ag([], [])

The argument filtering Pi contains the following mapping:
transposeA_in_ag(x1, x2)  =  transposeA_in_ag(x2)
.(x1, x2)  =  .(x1, x2)
U1_ag(x1, x2, x3, x4, x5)  =  U1_ag(x3, x4, x5)
pB_in_aggaaa(x1, x2, x3, x4, x5, x6)  =  pB_in_aggaaa(x2, x3)
U5_aggaaa(x1, x2, x3, x4, x5, x6, x7)  =  U5_aggaaa(x2, x3, x7)
row2colD_in_aggaa(x1, x2, x3, x4, x5)  =  row2colD_in_aggaa(x2, x3)
U3_aggaa(x1, x2, x3, x4, x5, x6, x7)  =  U3_aggaa(x1, x3, x4, x7)
row2colC_in_agaa(x1, x2, x3, x4)  =  row2colC_in_agaa(x2)
U2_agaa(x1, x2, x3, x4, x5, x6, x7)  =  U2_agaa(x1, x3, x4, x7)
[]  =  []
row2colC_out_agaa(x1, x2, x3, x4)  =  row2colC_out_agaa(x1, x2, x3, x4)
row2colD_out_aggaa(x1, x2, x3, x4, x5)  =  row2colD_out_aggaa(x1, x2, x3, x4, x5)
U6_aggaaa(x1, x2, x3, x4, x5, x6, x7)  =  U6_aggaaa(x1, x2, x3, x4, x5, x7)
transpose_auxE_in_agg(x1, x2, x3)  =  transpose_auxE_in_agg(x2, x3)
U4_agg(x1, x2, x3, x4, x5, x6)  =  U4_agg(x3, x4, x5, x6)
pB_out_aggaaa(x1, x2, x3, x4, x5, x6)  =  pB_out_aggaaa(x1, x2, x3, x4, x5, x6)
transpose_auxE_out_agg(x1, x2, x3)  =  transpose_auxE_out_agg(x1, x2, x3)
transposeA_out_ag(x1, x2)  =  transposeA_out_ag(x1, x2)
TRANSPOSEA_IN_AG(x1, x2)  =  TRANSPOSEA_IN_AG(x2)
U1_AG(x1, x2, x3, x4, x5)  =  U1_AG(x3, x4, x5)
PB_IN_AGGAAA(x1, x2, x3, x4, x5, x6)  =  PB_IN_AGGAAA(x2, x3)
U5_AGGAAA(x1, x2, x3, x4, x5, x6, x7)  =  U5_AGGAAA(x2, x3, x7)
ROW2COLD_IN_AGGAA(x1, x2, x3, x4, x5)  =  ROW2COLD_IN_AGGAA(x2, x3)
U3_AGGAA(x1, x2, x3, x4, x5, x6, x7)  =  U3_AGGAA(x1, x3, x4, x7)
ROW2COLC_IN_AGAA(x1, x2, x3, x4)  =  ROW2COLC_IN_AGAA(x2)
U2_AGAA(x1, x2, x3, x4, x5, x6, x7)  =  U2_AGAA(x1, x3, x4, x7)
U6_AGGAAA(x1, x2, x3, x4, x5, x6, x7)  =  U6_AGGAAA(x1, x2, x3, x4, x5, x7)
TRANSPOSE_AUXE_IN_AGG(x1, x2, x3)  =  TRANSPOSE_AUXE_IN_AGG(x2, x3)
U4_AGG(x1, x2, x3, x4, x5, x6)  =  U4_AGG(x3, x4, x5, x6)

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

(5) DependencyGraphProof (EQUIVALENT transformation)

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

(6) Complex Obligation (AND)

(7) Obligation:

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

ROW2COLC_IN_AGAA(.(T82, T86), .(.(T82, T84), T85), .(T84, X139), .([], X140)) → ROW2COLC_IN_AGAA(T86, T85, X139, X140)

The TRS R consists of the following rules:

transposeA_in_ag(.(T28, T29), .(T26, T27)) → U1_ag(T28, T29, T26, T27, pB_in_aggaaa(T28, T26, T27, X35, X36, T29))
pB_in_aggaaa(T28, T26, T27, T34, T35, T36) → U5_aggaaa(T28, T26, T27, T34, T35, T36, row2colD_in_aggaa(T28, T26, T27, T34, T35))
row2colD_in_aggaa(.(T57, T61), .(T57, T59), T60, .(T59, X91), .([], X92)) → U3_aggaa(T57, T61, T59, T60, X91, X92, row2colC_in_agaa(T61, T60, X91, X92))
row2colC_in_agaa(.(T82, T86), .(.(T82, T84), T85), .(T84, X139), .([], X140)) → U2_agaa(T82, T86, T84, T85, X139, X140, row2colC_in_agaa(T86, T85, X139, X140))
row2colC_in_agaa([], [], [], []) → row2colC_out_agaa([], [], [], [])
U2_agaa(T82, T86, T84, T85, X139, X140, row2colC_out_agaa(T86, T85, X139, X140)) → row2colC_out_agaa(.(T82, T86), .(.(T82, T84), T85), .(T84, X139), .([], X140))
U3_aggaa(T57, T61, T59, T60, X91, X92, row2colC_out_agaa(T61, T60, X91, X92)) → row2colD_out_aggaa(.(T57, T61), .(T57, T59), T60, .(T59, X91), .([], X92))
U5_aggaaa(T28, T26, T27, T34, T35, T36, row2colD_out_aggaa(T28, T26, T27, T34, T35)) → U6_aggaaa(T28, T26, T27, T34, T35, T36, transpose_auxE_in_agg(T36, T35, T34))
transpose_auxE_in_agg(.(T121, T122), T118, .(T119, T120)) → U4_agg(T121, T122, T118, T119, T120, pB_in_aggaaa(T121, T119, T120, X185, X186, T122))
U4_agg(T121, T122, T118, T119, T120, pB_out_aggaaa(T121, T119, T120, X185, X186, T122)) → transpose_auxE_out_agg(.(T121, T122), T118, .(T119, T120))
transpose_auxE_in_agg([], T129, T129) → transpose_auxE_out_agg([], T129, T129)
U6_aggaaa(T28, T26, T27, T34, T35, T36, transpose_auxE_out_agg(T36, T35, T34)) → pB_out_aggaaa(T28, T26, T27, T34, T35, T36)
U1_ag(T28, T29, T26, T27, pB_out_aggaaa(T28, T26, T27, X35, X36, T29)) → transposeA_out_ag(.(T28, T29), .(T26, T27))
transposeA_in_ag([], []) → transposeA_out_ag([], [])

The argument filtering Pi contains the following mapping:
transposeA_in_ag(x1, x2)  =  transposeA_in_ag(x2)
.(x1, x2)  =  .(x1, x2)
U1_ag(x1, x2, x3, x4, x5)  =  U1_ag(x3, x4, x5)
pB_in_aggaaa(x1, x2, x3, x4, x5, x6)  =  pB_in_aggaaa(x2, x3)
U5_aggaaa(x1, x2, x3, x4, x5, x6, x7)  =  U5_aggaaa(x2, x3, x7)
row2colD_in_aggaa(x1, x2, x3, x4, x5)  =  row2colD_in_aggaa(x2, x3)
U3_aggaa(x1, x2, x3, x4, x5, x6, x7)  =  U3_aggaa(x1, x3, x4, x7)
row2colC_in_agaa(x1, x2, x3, x4)  =  row2colC_in_agaa(x2)
U2_agaa(x1, x2, x3, x4, x5, x6, x7)  =  U2_agaa(x1, x3, x4, x7)
[]  =  []
row2colC_out_agaa(x1, x2, x3, x4)  =  row2colC_out_agaa(x1, x2, x3, x4)
row2colD_out_aggaa(x1, x2, x3, x4, x5)  =  row2colD_out_aggaa(x1, x2, x3, x4, x5)
U6_aggaaa(x1, x2, x3, x4, x5, x6, x7)  =  U6_aggaaa(x1, x2, x3, x4, x5, x7)
transpose_auxE_in_agg(x1, x2, x3)  =  transpose_auxE_in_agg(x2, x3)
U4_agg(x1, x2, x3, x4, x5, x6)  =  U4_agg(x3, x4, x5, x6)
pB_out_aggaaa(x1, x2, x3, x4, x5, x6)  =  pB_out_aggaaa(x1, x2, x3, x4, x5, x6)
transpose_auxE_out_agg(x1, x2, x3)  =  transpose_auxE_out_agg(x1, x2, x3)
transposeA_out_ag(x1, x2)  =  transposeA_out_ag(x1, x2)
ROW2COLC_IN_AGAA(x1, x2, x3, x4)  =  ROW2COLC_IN_AGAA(x2)

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

(8) UsableRulesProof (EQUIVALENT transformation)

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

(9) Obligation:

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

ROW2COLC_IN_AGAA(.(T82, T86), .(.(T82, T84), T85), .(T84, X139), .([], X140)) → ROW2COLC_IN_AGAA(T86, T85, X139, X140)

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

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

(10) PiDPToQDPProof (SOUND transformation)

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

(11) Obligation:

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

ROW2COLC_IN_AGAA(.(.(T82, T84), T85)) → ROW2COLC_IN_AGAA(T85)

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

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

• ROW2COLC_IN_AGAA(.(.(T82, T84), T85)) → ROW2COLC_IN_AGAA(T85)
  The graph contains the following edges 1 > 1

(13) YES

(14) Obligation:

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

U5_AGGAAA(T28, T26, T27, T34, T35, T36, row2colD_out_aggaa(T28, T26, T27, T34, T35)) → TRANSPOSE_AUXE_IN_AGG(T36, T35, T34)
TRANSPOSE_AUXE_IN_AGG(.(T121, T122), T118, .(T119, T120)) → PB_IN_AGGAAA(T121, T119, T120, X185, X186, T122)
PB_IN_AGGAAA(T28, T26, T27, T34, T35, T36) → U5_AGGAAA(T28, T26, T27, T34, T35, T36, row2colD_in_aggaa(T28, T26, T27, T34, T35))

The TRS R consists of the following rules:

transposeA_in_ag(.(T28, T29), .(T26, T27)) → U1_ag(T28, T29, T26, T27, pB_in_aggaaa(T28, T26, T27, X35, X36, T29))
pB_in_aggaaa(T28, T26, T27, T34, T35, T36) → U5_aggaaa(T28, T26, T27, T34, T35, T36, row2colD_in_aggaa(T28, T26, T27, T34, T35))
row2colD_in_aggaa(.(T57, T61), .(T57, T59), T60, .(T59, X91), .([], X92)) → U3_aggaa(T57, T61, T59, T60, X91, X92, row2colC_in_agaa(T61, T60, X91, X92))
row2colC_in_agaa(.(T82, T86), .(.(T82, T84), T85), .(T84, X139), .([], X140)) → U2_agaa(T82, T86, T84, T85, X139, X140, row2colC_in_agaa(T86, T85, X139, X140))
row2colC_in_agaa([], [], [], []) → row2colC_out_agaa([], [], [], [])
U2_agaa(T82, T86, T84, T85, X139, X140, row2colC_out_agaa(T86, T85, X139, X140)) → row2colC_out_agaa(.(T82, T86), .(.(T82, T84), T85), .(T84, X139), .([], X140))
U3_aggaa(T57, T61, T59, T60, X91, X92, row2colC_out_agaa(T61, T60, X91, X92)) → row2colD_out_aggaa(.(T57, T61), .(T57, T59), T60, .(T59, X91), .([], X92))
U5_aggaaa(T28, T26, T27, T34, T35, T36, row2colD_out_aggaa(T28, T26, T27, T34, T35)) → U6_aggaaa(T28, T26, T27, T34, T35, T36, transpose_auxE_in_agg(T36, T35, T34))
transpose_auxE_in_agg(.(T121, T122), T118, .(T119, T120)) → U4_agg(T121, T122, T118, T119, T120, pB_in_aggaaa(T121, T119, T120, X185, X186, T122))
U4_agg(T121, T122, T118, T119, T120, pB_out_aggaaa(T121, T119, T120, X185, X186, T122)) → transpose_auxE_out_agg(.(T121, T122), T118, .(T119, T120))
transpose_auxE_in_agg([], T129, T129) → transpose_auxE_out_agg([], T129, T129)
U6_aggaaa(T28, T26, T27, T34, T35, T36, transpose_auxE_out_agg(T36, T35, T34)) → pB_out_aggaaa(T28, T26, T27, T34, T35, T36)
U1_ag(T28, T29, T26, T27, pB_out_aggaaa(T28, T26, T27, X35, X36, T29)) → transposeA_out_ag(.(T28, T29), .(T26, T27))
transposeA_in_ag([], []) → transposeA_out_ag([], [])

The argument filtering Pi contains the following mapping:
transposeA_in_ag(x1, x2)  =  transposeA_in_ag(x2)
.(x1, x2)  =  .(x1, x2)
U1_ag(x1, x2, x3, x4, x5)  =  U1_ag(x3, x4, x5)
pB_in_aggaaa(x1, x2, x3, x4, x5, x6)  =  pB_in_aggaaa(x2, x3)
U5_aggaaa(x1, x2, x3, x4, x5, x6, x7)  =  U5_aggaaa(x2, x3, x7)
row2colD_in_aggaa(x1, x2, x3, x4, x5)  =  row2colD_in_aggaa(x2, x3)
U3_aggaa(x1, x2, x3, x4, x5, x6, x7)  =  U3_aggaa(x1, x3, x4, x7)
row2colC_in_agaa(x1, x2, x3, x4)  =  row2colC_in_agaa(x2)
U2_agaa(x1, x2, x3, x4, x5, x6, x7)  =  U2_agaa(x1, x3, x4, x7)
[]  =  []
row2colC_out_agaa(x1, x2, x3, x4)  =  row2colC_out_agaa(x1, x2, x3, x4)
row2colD_out_aggaa(x1, x2, x3, x4, x5)  =  row2colD_out_aggaa(x1, x2, x3, x4, x5)
U6_aggaaa(x1, x2, x3, x4, x5, x6, x7)  =  U6_aggaaa(x1, x2, x3, x4, x5, x7)
transpose_auxE_in_agg(x1, x2, x3)  =  transpose_auxE_in_agg(x2, x3)
U4_agg(x1, x2, x3, x4, x5, x6)  =  U4_agg(x3, x4, x5, x6)
pB_out_aggaaa(x1, x2, x3, x4, x5, x6)  =  pB_out_aggaaa(x1, x2, x3, x4, x5, x6)
transpose_auxE_out_agg(x1, x2, x3)  =  transpose_auxE_out_agg(x1, x2, x3)
transposeA_out_ag(x1, x2)  =  transposeA_out_ag(x1, x2)
PB_IN_AGGAAA(x1, x2, x3, x4, x5, x6)  =  PB_IN_AGGAAA(x2, x3)
U5_AGGAAA(x1, x2, x3, x4, x5, x6, x7)  =  U5_AGGAAA(x2, x3, x7)
TRANSPOSE_AUXE_IN_AGG(x1, x2, x3)  =  TRANSPOSE_AUXE_IN_AGG(x2, x3)

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

(15) UsableRulesProof (EQUIVALENT transformation)

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

(16) Obligation:

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

U5_AGGAAA(T28, T26, T27, T34, T35, T36, row2colD_out_aggaa(T28, T26, T27, T34, T35)) → TRANSPOSE_AUXE_IN_AGG(T36, T35, T34)
TRANSPOSE_AUXE_IN_AGG(.(T121, T122), T118, .(T119, T120)) → PB_IN_AGGAAA(T121, T119, T120, X185, X186, T122)
PB_IN_AGGAAA(T28, T26, T27, T34, T35, T36) → U5_AGGAAA(T28, T26, T27, T34, T35, T36, row2colD_in_aggaa(T28, T26, T27, T34, T35))

The TRS R consists of the following rules:

row2colD_in_aggaa(.(T57, T61), .(T57, T59), T60, .(T59, X91), .([], X92)) → U3_aggaa(T57, T61, T59, T60, X91, X92, row2colC_in_agaa(T61, T60, X91, X92))
U3_aggaa(T57, T61, T59, T60, X91, X92, row2colC_out_agaa(T61, T60, X91, X92)) → row2colD_out_aggaa(.(T57, T61), .(T57, T59), T60, .(T59, X91), .([], X92))
row2colC_in_agaa(.(T82, T86), .(.(T82, T84), T85), .(T84, X139), .([], X140)) → U2_agaa(T82, T86, T84, T85, X139, X140, row2colC_in_agaa(T86, T85, X139, X140))
row2colC_in_agaa([], [], [], []) → row2colC_out_agaa([], [], [], [])
U2_agaa(T82, T86, T84, T85, X139, X140, row2colC_out_agaa(T86, T85, X139, X140)) → row2colC_out_agaa(.(T82, T86), .(.(T82, T84), T85), .(T84, X139), .([], X140))

The argument filtering Pi contains the following mapping:
.(x1, x2)  =  .(x1, x2)
row2colD_in_aggaa(x1, x2, x3, x4, x5)  =  row2colD_in_aggaa(x2, x3)
U3_aggaa(x1, x2, x3, x4, x5, x6, x7)  =  U3_aggaa(x1, x3, x4, x7)
row2colC_in_agaa(x1, x2, x3, x4)  =  row2colC_in_agaa(x2)
U2_agaa(x1, x2, x3, x4, x5, x6, x7)  =  U2_agaa(x1, x3, x4, x7)
[]  =  []
row2colC_out_agaa(x1, x2, x3, x4)  =  row2colC_out_agaa(x1, x2, x3, x4)
row2colD_out_aggaa(x1, x2, x3, x4, x5)  =  row2colD_out_aggaa(x1, x2, x3, x4, x5)
PB_IN_AGGAAA(x1, x2, x3, x4, x5, x6)  =  PB_IN_AGGAAA(x2, x3)
U5_AGGAAA(x1, x2, x3, x4, x5, x6, x7)  =  U5_AGGAAA(x2, x3, x7)
TRANSPOSE_AUXE_IN_AGG(x1, x2, x3)  =  TRANSPOSE_AUXE_IN_AGG(x2, x3)

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

(17) PiDPToQDPProof (SOUND transformation)

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

(18) Obligation:

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

U5_AGGAAA(T26, T27, row2colD_out_aggaa(T28, T26, T27, T34, T35)) → TRANSPOSE_AUXE_IN_AGG(T35, T34)
TRANSPOSE_AUXE_IN_AGG(T118, .(T119, T120)) → PB_IN_AGGAAA(T119, T120)
PB_IN_AGGAAA(T26, T27) → U5_AGGAAA(T26, T27, row2colD_in_aggaa(T26, T27))

The TRS R consists of the following rules:

row2colD_in_aggaa(.(T57, T59), T60) → U3_aggaa(T57, T59, T60, row2colC_in_agaa(T60))
U3_aggaa(T57, T59, T60, row2colC_out_agaa(T61, T60, X91, X92)) → row2colD_out_aggaa(.(T57, T61), .(T57, T59), T60, .(T59, X91), .([], X92))
row2colC_in_agaa(.(.(T82, T84), T85)) → U2_agaa(T82, T84, T85, row2colC_in_agaa(T85))
row2colC_in_agaa([]) → row2colC_out_agaa([], [], [], [])
U2_agaa(T82, T84, T85, row2colC_out_agaa(T86, T85, X139, X140)) → row2colC_out_agaa(.(T82, T86), .(.(T82, T84), T85), .(T84, X139), .([], X140))

The set Q consists of the following terms:

row2colD_in_aggaa(x0, x1)
U3_aggaa(x0, x1, x2, x3)
row2colC_in_agaa(x0)
U2_agaa(x0, x1, x2, x3)

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

(19) QDPOrderProof (EQUIVALENT transformation)

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

The following pairs can be oriented strictly and are deleted.

PB_IN_AGGAAA(T26, T27) → U5_AGGAAA(T26, T27, row2colD_in_aggaa(T26, T27))

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

POL(.(x₁, x₂)) = 1 + x₁ + x₂   
POL(PB_IN_AGGAAA(x₁, x₂)) = 1 + x₁ + x₂   
POL(TRANSPOSE_AUXE_IN_AGG(x₁, x₂)) = x₂   
POL(U2_agaa(x₁, x₂, x₃, x₄)) = 1 + x₁ + x₂ + x₄   
POL(U3_aggaa(x₁, x₂, x₃, x₄)) = 1 + x₂ + x₄   
POL(U5_AGGAAA(x₁, x₂, x₃)) = x₃   
POL([]) = 0   
POL(row2colC_in_agaa(x₁)) = x₁   
POL(row2colC_out_agaa(x₁, x₂, x₃, x₄)) = x₃   
POL(row2colD_in_aggaa(x₁, x₂)) = x₁ + x₂   
POL(row2colD_out_aggaa(x₁, x₂, x₃, x₄, x₅)) = x₄   

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

row2colD_in_aggaa(.(T57, T59), T60) → U3_aggaa(T57, T59, T60, row2colC_in_agaa(T60))
row2colC_in_agaa(.(.(T82, T84), T85)) → U2_agaa(T82, T84, T85, row2colC_in_agaa(T85))
row2colC_in_agaa([]) → row2colC_out_agaa([], [], [], [])
U3_aggaa(T57, T59, T60, row2colC_out_agaa(T61, T60, X91, X92)) → row2colD_out_aggaa(.(T57, T61), .(T57, T59), T60, .(T59, X91), .([], X92))
U2_agaa(T82, T84, T85, row2colC_out_agaa(T86, T85, X139, X140)) → row2colC_out_agaa(.(T82, T86), .(.(T82, T84), T85), .(T84, X139), .([], X140))

(20) Obligation:

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

U5_AGGAAA(T26, T27, row2colD_out_aggaa(T28, T26, T27, T34, T35)) → TRANSPOSE_AUXE_IN_AGG(T35, T34)
TRANSPOSE_AUXE_IN_AGG(T118, .(T119, T120)) → PB_IN_AGGAAA(T119, T120)

The TRS R consists of the following rules:

row2colD_in_aggaa(.(T57, T59), T60) → U3_aggaa(T57, T59, T60, row2colC_in_agaa(T60))
U3_aggaa(T57, T59, T60, row2colC_out_agaa(T61, T60, X91, X92)) → row2colD_out_aggaa(.(T57, T61), .(T57, T59), T60, .(T59, X91), .([], X92))
row2colC_in_agaa(.(.(T82, T84), T85)) → U2_agaa(T82, T84, T85, row2colC_in_agaa(T85))
row2colC_in_agaa([]) → row2colC_out_agaa([], [], [], [])
U2_agaa(T82, T84, T85, row2colC_out_agaa(T86, T85, X139, X140)) → row2colC_out_agaa(.(T82, T86), .(.(T82, T84), T85), .(T84, X139), .([], X140))

The set Q consists of the following terms:

row2colD_in_aggaa(x0, x1)
U3_aggaa(x0, x1, x2, x3)
row2colC_in_agaa(x0)
U2_agaa(x0, x1, x2, x3)

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

(21) DependencyGraphProof (EQUIVALENT transformation)

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

(22) TRUE