Left Termination of the query pattern transpose(b,f) w.r.t. the given Prolog program could not be shown:



↳ PROLOG
  ↳ PrologToPiTRSProof
  ↳ PrologToPiTRSProof

transpose2(A, B) :- transposeaux3(A, {}0, B).
transposeaux3(.2(R, Rs), underscore, .2(C, Cs)) :- row2col5(R, .2(C, Cs), Cols1, {}0, Accm), transposeaux3(Rs, Accm, Cols1).
transposeaux3({}0, X, X).
row2col5(.2(X, Xs), .2(.2(X, Ys), Cols), .2(Ys, Cols1), A, B) :- row2col5(Xs, Cols, Cols1, .2({}0, A), B).
row2col5({}0, {}0, {}0, A, A).


With regard to the inferred argument filtering the predicates were used in the following modes:
transpose2: (b,f)
transpose_aux3: (b,b,f) (f,b,b)
row2col5: (f,b,f,b,f) (f,f,f,b,f)
Transforming PROLOG into the following Term Rewriting System:
Pi-finite rewrite system:
The TRS R consists of the following rules:


transpose_2_in_ga2(A, B) -> if_transpose_2_in_1_ga3(A, B, transpose_aux_3_in_gga3(A, []_0, B))
transpose_aux_3_in_gga3(._22(R, Rs), underscore, ._22(C, Cs)) -> if_transpose_aux_3_in_1_gga6(R, Rs, underscore, C, Cs, row2col_5_in_agaga5(R, ._22(C, Cs), Cols1, []_0, Accm))
row2col_5_in_agaga5(._22(X, Xs), ._22(._22(X, Ys), Cols), ._22(Ys, Cols1), A, B) -> if_row2col_5_in_1_agaga8(X, Xs, Ys, Cols, Cols1, A, B, row2col_5_in_aaaga5(Xs, Cols, Cols1, ._22([]_0, A), B))
row2col_5_in_aaaga5(._22(X, Xs), ._22(._22(X, Ys), Cols), ._22(Ys, Cols1), A, B) -> if_row2col_5_in_1_aaaga8(X, Xs, Ys, Cols, Cols1, A, B, row2col_5_in_aaaga5(Xs, Cols, Cols1, ._22([]_0, A), B))
row2col_5_in_aaaga5([]_0, []_0, []_0, A, A) -> row2col_5_out_aaaga5([]_0, []_0, []_0, A, A)
if_row2col_5_in_1_aaaga8(X, Xs, Ys, Cols, Cols1, A, B, row2col_5_out_aaaga5(Xs, Cols, Cols1, ._22([]_0, A), B)) -> row2col_5_out_aaaga5(._22(X, Xs), ._22(._22(X, Ys), Cols), ._22(Ys, Cols1), A, B)
if_row2col_5_in_1_agaga8(X, Xs, Ys, Cols, Cols1, A, B, row2col_5_out_aaaga5(Xs, Cols, Cols1, ._22([]_0, A), B)) -> row2col_5_out_agaga5(._22(X, Xs), ._22(._22(X, Ys), Cols), ._22(Ys, Cols1), A, B)
row2col_5_in_agaga5([]_0, []_0, []_0, A, A) -> row2col_5_out_agaga5([]_0, []_0, []_0, A, A)
if_transpose_aux_3_in_1_gga6(R, Rs, underscore, C, Cs, row2col_5_out_agaga5(R, ._22(C, Cs), Cols1, []_0, Accm)) -> if_transpose_aux_3_in_2_gga8(R, Rs, underscore, C, Cs, Cols1, Accm, transpose_aux_3_in_agg3(Rs, Accm, Cols1))
transpose_aux_3_in_agg3(._22(R, Rs), underscore, ._22(C, Cs)) -> if_transpose_aux_3_in_1_agg6(R, Rs, underscore, C, Cs, row2col_5_in_agaga5(R, ._22(C, Cs), Cols1, []_0, Accm))
if_transpose_aux_3_in_1_agg6(R, Rs, underscore, C, Cs, row2col_5_out_agaga5(R, ._22(C, Cs), Cols1, []_0, Accm)) -> if_transpose_aux_3_in_2_agg8(R, Rs, underscore, C, Cs, Cols1, Accm, transpose_aux_3_in_agg3(Rs, Accm, Cols1))
transpose_aux_3_in_agg3([]_0, X, X) -> transpose_aux_3_out_agg3([]_0, X, X)
if_transpose_aux_3_in_2_agg8(R, Rs, underscore, C, Cs, Cols1, Accm, transpose_aux_3_out_agg3(Rs, Accm, Cols1)) -> transpose_aux_3_out_agg3(._22(R, Rs), underscore, ._22(C, Cs))
if_transpose_aux_3_in_2_gga8(R, Rs, underscore, C, Cs, Cols1, Accm, transpose_aux_3_out_agg3(Rs, Accm, Cols1)) -> transpose_aux_3_out_gga3(._22(R, Rs), underscore, ._22(C, Cs))
transpose_aux_3_in_gga3([]_0, X, X) -> transpose_aux_3_out_gga3([]_0, X, X)
if_transpose_2_in_1_ga3(A, B, transpose_aux_3_out_gga3(A, []_0, B)) -> transpose_2_out_ga2(A, B)

The argument filtering Pi contains the following mapping:
transpose_2_in_ga2(x1, x2)  =  transpose_2_in_ga1(x1)
[]_0  =  []_0
._22(x1, x2)  =  ._2
if_transpose_2_in_1_ga3(x1, x2, x3)  =  if_transpose_2_in_1_ga1(x3)
transpose_aux_3_in_gga3(x1, x2, x3)  =  transpose_aux_3_in_gga2(x1, x2)
if_transpose_aux_3_in_1_gga6(x1, x2, x3, x4, x5, x6)  =  if_transpose_aux_3_in_1_gga1(x6)
row2col_5_in_agaga5(x1, x2, x3, x4, x5)  =  row2col_5_in_agaga2(x2, x4)
if_row2col_5_in_1_agaga8(x1, x2, x3, x4, x5, x6, x7, x8)  =  if_row2col_5_in_1_agaga1(x8)
row2col_5_in_aaaga5(x1, x2, x3, x4, x5)  =  row2col_5_in_aaaga1(x4)
if_row2col_5_in_1_aaaga8(x1, x2, x3, x4, x5, x6, x7, x8)  =  if_row2col_5_in_1_aaaga1(x8)
row2col_5_out_aaaga5(x1, x2, x3, x4, x5)  =  row2col_5_out_aaaga4(x1, x2, x3, x5)
row2col_5_out_agaga5(x1, x2, x3, x4, x5)  =  row2col_5_out_agaga3(x1, x3, x5)
if_transpose_aux_3_in_2_gga8(x1, x2, x3, x4, x5, x6, x7, x8)  =  if_transpose_aux_3_in_2_gga1(x8)
transpose_aux_3_in_agg3(x1, x2, x3)  =  transpose_aux_3_in_agg2(x2, x3)
if_transpose_aux_3_in_1_agg6(x1, x2, x3, x4, x5, x6)  =  if_transpose_aux_3_in_1_agg1(x6)
if_transpose_aux_3_in_2_agg8(x1, x2, x3, x4, x5, x6, x7, x8)  =  if_transpose_aux_3_in_2_agg1(x8)
transpose_aux_3_out_agg3(x1, x2, x3)  =  transpose_aux_3_out_agg1(x1)
transpose_aux_3_out_gga3(x1, x2, x3)  =  transpose_aux_3_out_gga1(x3)
transpose_2_out_ga2(x1, x2)  =  transpose_2_out_ga1(x2)

Infinitary Constructor Rewriting Termination of PiTRS implies Termination of PROLOG



↳ PROLOG
  ↳ PrologToPiTRSProof
    ↳ PiTRS
      ↳ DependencyPairsProof
  ↳ PrologToPiTRSProof

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

transpose_2_in_ga2(A, B) -> if_transpose_2_in_1_ga3(A, B, transpose_aux_3_in_gga3(A, []_0, B))
transpose_aux_3_in_gga3(._22(R, Rs), underscore, ._22(C, Cs)) -> if_transpose_aux_3_in_1_gga6(R, Rs, underscore, C, Cs, row2col_5_in_agaga5(R, ._22(C, Cs), Cols1, []_0, Accm))
row2col_5_in_agaga5(._22(X, Xs), ._22(._22(X, Ys), Cols), ._22(Ys, Cols1), A, B) -> if_row2col_5_in_1_agaga8(X, Xs, Ys, Cols, Cols1, A, B, row2col_5_in_aaaga5(Xs, Cols, Cols1, ._22([]_0, A), B))
row2col_5_in_aaaga5(._22(X, Xs), ._22(._22(X, Ys), Cols), ._22(Ys, Cols1), A, B) -> if_row2col_5_in_1_aaaga8(X, Xs, Ys, Cols, Cols1, A, B, row2col_5_in_aaaga5(Xs, Cols, Cols1, ._22([]_0, A), B))
row2col_5_in_aaaga5([]_0, []_0, []_0, A, A) -> row2col_5_out_aaaga5([]_0, []_0, []_0, A, A)
if_row2col_5_in_1_aaaga8(X, Xs, Ys, Cols, Cols1, A, B, row2col_5_out_aaaga5(Xs, Cols, Cols1, ._22([]_0, A), B)) -> row2col_5_out_aaaga5(._22(X, Xs), ._22(._22(X, Ys), Cols), ._22(Ys, Cols1), A, B)
if_row2col_5_in_1_agaga8(X, Xs, Ys, Cols, Cols1, A, B, row2col_5_out_aaaga5(Xs, Cols, Cols1, ._22([]_0, A), B)) -> row2col_5_out_agaga5(._22(X, Xs), ._22(._22(X, Ys), Cols), ._22(Ys, Cols1), A, B)
row2col_5_in_agaga5([]_0, []_0, []_0, A, A) -> row2col_5_out_agaga5([]_0, []_0, []_0, A, A)
if_transpose_aux_3_in_1_gga6(R, Rs, underscore, C, Cs, row2col_5_out_agaga5(R, ._22(C, Cs), Cols1, []_0, Accm)) -> if_transpose_aux_3_in_2_gga8(R, Rs, underscore, C, Cs, Cols1, Accm, transpose_aux_3_in_agg3(Rs, Accm, Cols1))
transpose_aux_3_in_agg3(._22(R, Rs), underscore, ._22(C, Cs)) -> if_transpose_aux_3_in_1_agg6(R, Rs, underscore, C, Cs, row2col_5_in_agaga5(R, ._22(C, Cs), Cols1, []_0, Accm))
if_transpose_aux_3_in_1_agg6(R, Rs, underscore, C, Cs, row2col_5_out_agaga5(R, ._22(C, Cs), Cols1, []_0, Accm)) -> if_transpose_aux_3_in_2_agg8(R, Rs, underscore, C, Cs, Cols1, Accm, transpose_aux_3_in_agg3(Rs, Accm, Cols1))
transpose_aux_3_in_agg3([]_0, X, X) -> transpose_aux_3_out_agg3([]_0, X, X)
if_transpose_aux_3_in_2_agg8(R, Rs, underscore, C, Cs, Cols1, Accm, transpose_aux_3_out_agg3(Rs, Accm, Cols1)) -> transpose_aux_3_out_agg3(._22(R, Rs), underscore, ._22(C, Cs))
if_transpose_aux_3_in_2_gga8(R, Rs, underscore, C, Cs, Cols1, Accm, transpose_aux_3_out_agg3(Rs, Accm, Cols1)) -> transpose_aux_3_out_gga3(._22(R, Rs), underscore, ._22(C, Cs))
transpose_aux_3_in_gga3([]_0, X, X) -> transpose_aux_3_out_gga3([]_0, X, X)
if_transpose_2_in_1_ga3(A, B, transpose_aux_3_out_gga3(A, []_0, B)) -> transpose_2_out_ga2(A, B)

The argument filtering Pi contains the following mapping:
transpose_2_in_ga2(x1, x2)  =  transpose_2_in_ga1(x1)
[]_0  =  []_0
._22(x1, x2)  =  ._2
if_transpose_2_in_1_ga3(x1, x2, x3)  =  if_transpose_2_in_1_ga1(x3)
transpose_aux_3_in_gga3(x1, x2, x3)  =  transpose_aux_3_in_gga2(x1, x2)
if_transpose_aux_3_in_1_gga6(x1, x2, x3, x4, x5, x6)  =  if_transpose_aux_3_in_1_gga1(x6)
row2col_5_in_agaga5(x1, x2, x3, x4, x5)  =  row2col_5_in_agaga2(x2, x4)
if_row2col_5_in_1_agaga8(x1, x2, x3, x4, x5, x6, x7, x8)  =  if_row2col_5_in_1_agaga1(x8)
row2col_5_in_aaaga5(x1, x2, x3, x4, x5)  =  row2col_5_in_aaaga1(x4)
if_row2col_5_in_1_aaaga8(x1, x2, x3, x4, x5, x6, x7, x8)  =  if_row2col_5_in_1_aaaga1(x8)
row2col_5_out_aaaga5(x1, x2, x3, x4, x5)  =  row2col_5_out_aaaga4(x1, x2, x3, x5)
row2col_5_out_agaga5(x1, x2, x3, x4, x5)  =  row2col_5_out_agaga3(x1, x3, x5)
if_transpose_aux_3_in_2_gga8(x1, x2, x3, x4, x5, x6, x7, x8)  =  if_transpose_aux_3_in_2_gga1(x8)
transpose_aux_3_in_agg3(x1, x2, x3)  =  transpose_aux_3_in_agg2(x2, x3)
if_transpose_aux_3_in_1_agg6(x1, x2, x3, x4, x5, x6)  =  if_transpose_aux_3_in_1_agg1(x6)
if_transpose_aux_3_in_2_agg8(x1, x2, x3, x4, x5, x6, x7, x8)  =  if_transpose_aux_3_in_2_agg1(x8)
transpose_aux_3_out_agg3(x1, x2, x3)  =  transpose_aux_3_out_agg1(x1)
transpose_aux_3_out_gga3(x1, x2, x3)  =  transpose_aux_3_out_gga1(x3)
transpose_2_out_ga2(x1, x2)  =  transpose_2_out_ga1(x2)


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

TRANSPOSE_2_IN_GA2(A, B) -> IF_TRANSPOSE_2_IN_1_GA3(A, B, transpose_aux_3_in_gga3(A, []_0, B))
TRANSPOSE_2_IN_GA2(A, B) -> TRANSPOSE_AUX_3_IN_GGA3(A, []_0, B)
TRANSPOSE_AUX_3_IN_GGA3(._22(R, Rs), underscore, ._22(C, Cs)) -> IF_TRANSPOSE_AUX_3_IN_1_GGA6(R, Rs, underscore, C, Cs, row2col_5_in_agaga5(R, ._22(C, Cs), Cols1, []_0, Accm))
TRANSPOSE_AUX_3_IN_GGA3(._22(R, Rs), underscore, ._22(C, Cs)) -> ROW2COL_5_IN_AGAGA5(R, ._22(C, Cs), Cols1, []_0, Accm)
ROW2COL_5_IN_AGAGA5(._22(X, Xs), ._22(._22(X, Ys), Cols), ._22(Ys, Cols1), A, B) -> IF_ROW2COL_5_IN_1_AGAGA8(X, Xs, Ys, Cols, Cols1, A, B, row2col_5_in_aaaga5(Xs, Cols, Cols1, ._22([]_0, A), B))
ROW2COL_5_IN_AGAGA5(._22(X, Xs), ._22(._22(X, Ys), Cols), ._22(Ys, Cols1), A, B) -> ROW2COL_5_IN_AAAGA5(Xs, Cols, Cols1, ._22([]_0, A), B)
ROW2COL_5_IN_AAAGA5(._22(X, Xs), ._22(._22(X, Ys), Cols), ._22(Ys, Cols1), A, B) -> IF_ROW2COL_5_IN_1_AAAGA8(X, Xs, Ys, Cols, Cols1, A, B, row2col_5_in_aaaga5(Xs, Cols, Cols1, ._22([]_0, A), B))
ROW2COL_5_IN_AAAGA5(._22(X, Xs), ._22(._22(X, Ys), Cols), ._22(Ys, Cols1), A, B) -> ROW2COL_5_IN_AAAGA5(Xs, Cols, Cols1, ._22([]_0, A), B)
IF_TRANSPOSE_AUX_3_IN_1_GGA6(R, Rs, underscore, C, Cs, row2col_5_out_agaga5(R, ._22(C, Cs), Cols1, []_0, Accm)) -> IF_TRANSPOSE_AUX_3_IN_2_GGA8(R, Rs, underscore, C, Cs, Cols1, Accm, transpose_aux_3_in_agg3(Rs, Accm, Cols1))
IF_TRANSPOSE_AUX_3_IN_1_GGA6(R, Rs, underscore, C, Cs, row2col_5_out_agaga5(R, ._22(C, Cs), Cols1, []_0, Accm)) -> TRANSPOSE_AUX_3_IN_AGG3(Rs, Accm, Cols1)
TRANSPOSE_AUX_3_IN_AGG3(._22(R, Rs), underscore, ._22(C, Cs)) -> IF_TRANSPOSE_AUX_3_IN_1_AGG6(R, Rs, underscore, C, Cs, row2col_5_in_agaga5(R, ._22(C, Cs), Cols1, []_0, Accm))
TRANSPOSE_AUX_3_IN_AGG3(._22(R, Rs), underscore, ._22(C, Cs)) -> ROW2COL_5_IN_AGAGA5(R, ._22(C, Cs), Cols1, []_0, Accm)
IF_TRANSPOSE_AUX_3_IN_1_AGG6(R, Rs, underscore, C, Cs, row2col_5_out_agaga5(R, ._22(C, Cs), Cols1, []_0, Accm)) -> IF_TRANSPOSE_AUX_3_IN_2_AGG8(R, Rs, underscore, C, Cs, Cols1, Accm, transpose_aux_3_in_agg3(Rs, Accm, Cols1))
IF_TRANSPOSE_AUX_3_IN_1_AGG6(R, Rs, underscore, C, Cs, row2col_5_out_agaga5(R, ._22(C, Cs), Cols1, []_0, Accm)) -> TRANSPOSE_AUX_3_IN_AGG3(Rs, Accm, Cols1)

The TRS R consists of the following rules:

transpose_2_in_ga2(A, B) -> if_transpose_2_in_1_ga3(A, B, transpose_aux_3_in_gga3(A, []_0, B))
transpose_aux_3_in_gga3(._22(R, Rs), underscore, ._22(C, Cs)) -> if_transpose_aux_3_in_1_gga6(R, Rs, underscore, C, Cs, row2col_5_in_agaga5(R, ._22(C, Cs), Cols1, []_0, Accm))
row2col_5_in_agaga5(._22(X, Xs), ._22(._22(X, Ys), Cols), ._22(Ys, Cols1), A, B) -> if_row2col_5_in_1_agaga8(X, Xs, Ys, Cols, Cols1, A, B, row2col_5_in_aaaga5(Xs, Cols, Cols1, ._22([]_0, A), B))
row2col_5_in_aaaga5(._22(X, Xs), ._22(._22(X, Ys), Cols), ._22(Ys, Cols1), A, B) -> if_row2col_5_in_1_aaaga8(X, Xs, Ys, Cols, Cols1, A, B, row2col_5_in_aaaga5(Xs, Cols, Cols1, ._22([]_0, A), B))
row2col_5_in_aaaga5([]_0, []_0, []_0, A, A) -> row2col_5_out_aaaga5([]_0, []_0, []_0, A, A)
if_row2col_5_in_1_aaaga8(X, Xs, Ys, Cols, Cols1, A, B, row2col_5_out_aaaga5(Xs, Cols, Cols1, ._22([]_0, A), B)) -> row2col_5_out_aaaga5(._22(X, Xs), ._22(._22(X, Ys), Cols), ._22(Ys, Cols1), A, B)
if_row2col_5_in_1_agaga8(X, Xs, Ys, Cols, Cols1, A, B, row2col_5_out_aaaga5(Xs, Cols, Cols1, ._22([]_0, A), B)) -> row2col_5_out_agaga5(._22(X, Xs), ._22(._22(X, Ys), Cols), ._22(Ys, Cols1), A, B)
row2col_5_in_agaga5([]_0, []_0, []_0, A, A) -> row2col_5_out_agaga5([]_0, []_0, []_0, A, A)
if_transpose_aux_3_in_1_gga6(R, Rs, underscore, C, Cs, row2col_5_out_agaga5(R, ._22(C, Cs), Cols1, []_0, Accm)) -> if_transpose_aux_3_in_2_gga8(R, Rs, underscore, C, Cs, Cols1, Accm, transpose_aux_3_in_agg3(Rs, Accm, Cols1))
transpose_aux_3_in_agg3(._22(R, Rs), underscore, ._22(C, Cs)) -> if_transpose_aux_3_in_1_agg6(R, Rs, underscore, C, Cs, row2col_5_in_agaga5(R, ._22(C, Cs), Cols1, []_0, Accm))
if_transpose_aux_3_in_1_agg6(R, Rs, underscore, C, Cs, row2col_5_out_agaga5(R, ._22(C, Cs), Cols1, []_0, Accm)) -> if_transpose_aux_3_in_2_agg8(R, Rs, underscore, C, Cs, Cols1, Accm, transpose_aux_3_in_agg3(Rs, Accm, Cols1))
transpose_aux_3_in_agg3([]_0, X, X) -> transpose_aux_3_out_agg3([]_0, X, X)
if_transpose_aux_3_in_2_agg8(R, Rs, underscore, C, Cs, Cols1, Accm, transpose_aux_3_out_agg3(Rs, Accm, Cols1)) -> transpose_aux_3_out_agg3(._22(R, Rs), underscore, ._22(C, Cs))
if_transpose_aux_3_in_2_gga8(R, Rs, underscore, C, Cs, Cols1, Accm, transpose_aux_3_out_agg3(Rs, Accm, Cols1)) -> transpose_aux_3_out_gga3(._22(R, Rs), underscore, ._22(C, Cs))
transpose_aux_3_in_gga3([]_0, X, X) -> transpose_aux_3_out_gga3([]_0, X, X)
if_transpose_2_in_1_ga3(A, B, transpose_aux_3_out_gga3(A, []_0, B)) -> transpose_2_out_ga2(A, B)

The argument filtering Pi contains the following mapping:
transpose_2_in_ga2(x1, x2)  =  transpose_2_in_ga1(x1)
[]_0  =  []_0
._22(x1, x2)  =  ._2
if_transpose_2_in_1_ga3(x1, x2, x3)  =  if_transpose_2_in_1_ga1(x3)
transpose_aux_3_in_gga3(x1, x2, x3)  =  transpose_aux_3_in_gga2(x1, x2)
if_transpose_aux_3_in_1_gga6(x1, x2, x3, x4, x5, x6)  =  if_transpose_aux_3_in_1_gga1(x6)
row2col_5_in_agaga5(x1, x2, x3, x4, x5)  =  row2col_5_in_agaga2(x2, x4)
if_row2col_5_in_1_agaga8(x1, x2, x3, x4, x5, x6, x7, x8)  =  if_row2col_5_in_1_agaga1(x8)
row2col_5_in_aaaga5(x1, x2, x3, x4, x5)  =  row2col_5_in_aaaga1(x4)
if_row2col_5_in_1_aaaga8(x1, x2, x3, x4, x5, x6, x7, x8)  =  if_row2col_5_in_1_aaaga1(x8)
row2col_5_out_aaaga5(x1, x2, x3, x4, x5)  =  row2col_5_out_aaaga4(x1, x2, x3, x5)
row2col_5_out_agaga5(x1, x2, x3, x4, x5)  =  row2col_5_out_agaga3(x1, x3, x5)
if_transpose_aux_3_in_2_gga8(x1, x2, x3, x4, x5, x6, x7, x8)  =  if_transpose_aux_3_in_2_gga1(x8)
transpose_aux_3_in_agg3(x1, x2, x3)  =  transpose_aux_3_in_agg2(x2, x3)
if_transpose_aux_3_in_1_agg6(x1, x2, x3, x4, x5, x6)  =  if_transpose_aux_3_in_1_agg1(x6)
if_transpose_aux_3_in_2_agg8(x1, x2, x3, x4, x5, x6, x7, x8)  =  if_transpose_aux_3_in_2_agg1(x8)
transpose_aux_3_out_agg3(x1, x2, x3)  =  transpose_aux_3_out_agg1(x1)
transpose_aux_3_out_gga3(x1, x2, x3)  =  transpose_aux_3_out_gga1(x3)
transpose_2_out_ga2(x1, x2)  =  transpose_2_out_ga1(x2)
IF_TRANSPOSE_AUX_3_IN_1_GGA6(x1, x2, x3, x4, x5, x6)  =  IF_TRANSPOSE_AUX_3_IN_1_GGA1(x6)
IF_TRANSPOSE_AUX_3_IN_2_AGG8(x1, x2, x3, x4, x5, x6, x7, x8)  =  IF_TRANSPOSE_AUX_3_IN_2_AGG1(x8)
IF_TRANSPOSE_AUX_3_IN_1_AGG6(x1, x2, x3, x4, x5, x6)  =  IF_TRANSPOSE_AUX_3_IN_1_AGG1(x6)
ROW2COL_5_IN_AGAGA5(x1, x2, x3, x4, x5)  =  ROW2COL_5_IN_AGAGA2(x2, x4)
ROW2COL_5_IN_AAAGA5(x1, x2, x3, x4, x5)  =  ROW2COL_5_IN_AAAGA1(x4)
TRANSPOSE_2_IN_GA2(x1, x2)  =  TRANSPOSE_2_IN_GA1(x1)
IF_ROW2COL_5_IN_1_AGAGA8(x1, x2, x3, x4, x5, x6, x7, x8)  =  IF_ROW2COL_5_IN_1_AGAGA1(x8)
TRANSPOSE_AUX_3_IN_GGA3(x1, x2, x3)  =  TRANSPOSE_AUX_3_IN_GGA2(x1, x2)
IF_TRANSPOSE_2_IN_1_GA3(x1, x2, x3)  =  IF_TRANSPOSE_2_IN_1_GA1(x3)
TRANSPOSE_AUX_3_IN_AGG3(x1, x2, x3)  =  TRANSPOSE_AUX_3_IN_AGG2(x2, x3)
IF_ROW2COL_5_IN_1_AAAGA8(x1, x2, x3, x4, x5, x6, x7, x8)  =  IF_ROW2COL_5_IN_1_AAAGA1(x8)
IF_TRANSPOSE_AUX_3_IN_2_GGA8(x1, x2, x3, x4, x5, x6, x7, x8)  =  IF_TRANSPOSE_AUX_3_IN_2_GGA1(x8)

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

↳ PROLOG
  ↳ PrologToPiTRSProof
    ↳ PiTRS
      ↳ DependencyPairsProof
        ↳ PiDP
          ↳ DependencyGraphProof
  ↳ PrologToPiTRSProof

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

TRANSPOSE_2_IN_GA2(A, B) -> IF_TRANSPOSE_2_IN_1_GA3(A, B, transpose_aux_3_in_gga3(A, []_0, B))
TRANSPOSE_2_IN_GA2(A, B) -> TRANSPOSE_AUX_3_IN_GGA3(A, []_0, B)
TRANSPOSE_AUX_3_IN_GGA3(._22(R, Rs), underscore, ._22(C, Cs)) -> IF_TRANSPOSE_AUX_3_IN_1_GGA6(R, Rs, underscore, C, Cs, row2col_5_in_agaga5(R, ._22(C, Cs), Cols1, []_0, Accm))
TRANSPOSE_AUX_3_IN_GGA3(._22(R, Rs), underscore, ._22(C, Cs)) -> ROW2COL_5_IN_AGAGA5(R, ._22(C, Cs), Cols1, []_0, Accm)
ROW2COL_5_IN_AGAGA5(._22(X, Xs), ._22(._22(X, Ys), Cols), ._22(Ys, Cols1), A, B) -> IF_ROW2COL_5_IN_1_AGAGA8(X, Xs, Ys, Cols, Cols1, A, B, row2col_5_in_aaaga5(Xs, Cols, Cols1, ._22([]_0, A), B))
ROW2COL_5_IN_AGAGA5(._22(X, Xs), ._22(._22(X, Ys), Cols), ._22(Ys, Cols1), A, B) -> ROW2COL_5_IN_AAAGA5(Xs, Cols, Cols1, ._22([]_0, A), B)
ROW2COL_5_IN_AAAGA5(._22(X, Xs), ._22(._22(X, Ys), Cols), ._22(Ys, Cols1), A, B) -> IF_ROW2COL_5_IN_1_AAAGA8(X, Xs, Ys, Cols, Cols1, A, B, row2col_5_in_aaaga5(Xs, Cols, Cols1, ._22([]_0, A), B))
ROW2COL_5_IN_AAAGA5(._22(X, Xs), ._22(._22(X, Ys), Cols), ._22(Ys, Cols1), A, B) -> ROW2COL_5_IN_AAAGA5(Xs, Cols, Cols1, ._22([]_0, A), B)
IF_TRANSPOSE_AUX_3_IN_1_GGA6(R, Rs, underscore, C, Cs, row2col_5_out_agaga5(R, ._22(C, Cs), Cols1, []_0, Accm)) -> IF_TRANSPOSE_AUX_3_IN_2_GGA8(R, Rs, underscore, C, Cs, Cols1, Accm, transpose_aux_3_in_agg3(Rs, Accm, Cols1))
IF_TRANSPOSE_AUX_3_IN_1_GGA6(R, Rs, underscore, C, Cs, row2col_5_out_agaga5(R, ._22(C, Cs), Cols1, []_0, Accm)) -> TRANSPOSE_AUX_3_IN_AGG3(Rs, Accm, Cols1)
TRANSPOSE_AUX_3_IN_AGG3(._22(R, Rs), underscore, ._22(C, Cs)) -> IF_TRANSPOSE_AUX_3_IN_1_AGG6(R, Rs, underscore, C, Cs, row2col_5_in_agaga5(R, ._22(C, Cs), Cols1, []_0, Accm))
TRANSPOSE_AUX_3_IN_AGG3(._22(R, Rs), underscore, ._22(C, Cs)) -> ROW2COL_5_IN_AGAGA5(R, ._22(C, Cs), Cols1, []_0, Accm)
IF_TRANSPOSE_AUX_3_IN_1_AGG6(R, Rs, underscore, C, Cs, row2col_5_out_agaga5(R, ._22(C, Cs), Cols1, []_0, Accm)) -> IF_TRANSPOSE_AUX_3_IN_2_AGG8(R, Rs, underscore, C, Cs, Cols1, Accm, transpose_aux_3_in_agg3(Rs, Accm, Cols1))
IF_TRANSPOSE_AUX_3_IN_1_AGG6(R, Rs, underscore, C, Cs, row2col_5_out_agaga5(R, ._22(C, Cs), Cols1, []_0, Accm)) -> TRANSPOSE_AUX_3_IN_AGG3(Rs, Accm, Cols1)

The TRS R consists of the following rules:

transpose_2_in_ga2(A, B) -> if_transpose_2_in_1_ga3(A, B, transpose_aux_3_in_gga3(A, []_0, B))
transpose_aux_3_in_gga3(._22(R, Rs), underscore, ._22(C, Cs)) -> if_transpose_aux_3_in_1_gga6(R, Rs, underscore, C, Cs, row2col_5_in_agaga5(R, ._22(C, Cs), Cols1, []_0, Accm))
row2col_5_in_agaga5(._22(X, Xs), ._22(._22(X, Ys), Cols), ._22(Ys, Cols1), A, B) -> if_row2col_5_in_1_agaga8(X, Xs, Ys, Cols, Cols1, A, B, row2col_5_in_aaaga5(Xs, Cols, Cols1, ._22([]_0, A), B))
row2col_5_in_aaaga5(._22(X, Xs), ._22(._22(X, Ys), Cols), ._22(Ys, Cols1), A, B) -> if_row2col_5_in_1_aaaga8(X, Xs, Ys, Cols, Cols1, A, B, row2col_5_in_aaaga5(Xs, Cols, Cols1, ._22([]_0, A), B))
row2col_5_in_aaaga5([]_0, []_0, []_0, A, A) -> row2col_5_out_aaaga5([]_0, []_0, []_0, A, A)
if_row2col_5_in_1_aaaga8(X, Xs, Ys, Cols, Cols1, A, B, row2col_5_out_aaaga5(Xs, Cols, Cols1, ._22([]_0, A), B)) -> row2col_5_out_aaaga5(._22(X, Xs), ._22(._22(X, Ys), Cols), ._22(Ys, Cols1), A, B)
if_row2col_5_in_1_agaga8(X, Xs, Ys, Cols, Cols1, A, B, row2col_5_out_aaaga5(Xs, Cols, Cols1, ._22([]_0, A), B)) -> row2col_5_out_agaga5(._22(X, Xs), ._22(._22(X, Ys), Cols), ._22(Ys, Cols1), A, B)
row2col_5_in_agaga5([]_0, []_0, []_0, A, A) -> row2col_5_out_agaga5([]_0, []_0, []_0, A, A)
if_transpose_aux_3_in_1_gga6(R, Rs, underscore, C, Cs, row2col_5_out_agaga5(R, ._22(C, Cs), Cols1, []_0, Accm)) -> if_transpose_aux_3_in_2_gga8(R, Rs, underscore, C, Cs, Cols1, Accm, transpose_aux_3_in_agg3(Rs, Accm, Cols1))
transpose_aux_3_in_agg3(._22(R, Rs), underscore, ._22(C, Cs)) -> if_transpose_aux_3_in_1_agg6(R, Rs, underscore, C, Cs, row2col_5_in_agaga5(R, ._22(C, Cs), Cols1, []_0, Accm))
if_transpose_aux_3_in_1_agg6(R, Rs, underscore, C, Cs, row2col_5_out_agaga5(R, ._22(C, Cs), Cols1, []_0, Accm)) -> if_transpose_aux_3_in_2_agg8(R, Rs, underscore, C, Cs, Cols1, Accm, transpose_aux_3_in_agg3(Rs, Accm, Cols1))
transpose_aux_3_in_agg3([]_0, X, X) -> transpose_aux_3_out_agg3([]_0, X, X)
if_transpose_aux_3_in_2_agg8(R, Rs, underscore, C, Cs, Cols1, Accm, transpose_aux_3_out_agg3(Rs, Accm, Cols1)) -> transpose_aux_3_out_agg3(._22(R, Rs), underscore, ._22(C, Cs))
if_transpose_aux_3_in_2_gga8(R, Rs, underscore, C, Cs, Cols1, Accm, transpose_aux_3_out_agg3(Rs, Accm, Cols1)) -> transpose_aux_3_out_gga3(._22(R, Rs), underscore, ._22(C, Cs))
transpose_aux_3_in_gga3([]_0, X, X) -> transpose_aux_3_out_gga3([]_0, X, X)
if_transpose_2_in_1_ga3(A, B, transpose_aux_3_out_gga3(A, []_0, B)) -> transpose_2_out_ga2(A, B)

The argument filtering Pi contains the following mapping:
transpose_2_in_ga2(x1, x2)  =  transpose_2_in_ga1(x1)
[]_0  =  []_0
._22(x1, x2)  =  ._2
if_transpose_2_in_1_ga3(x1, x2, x3)  =  if_transpose_2_in_1_ga1(x3)
transpose_aux_3_in_gga3(x1, x2, x3)  =  transpose_aux_3_in_gga2(x1, x2)
if_transpose_aux_3_in_1_gga6(x1, x2, x3, x4, x5, x6)  =  if_transpose_aux_3_in_1_gga1(x6)
row2col_5_in_agaga5(x1, x2, x3, x4, x5)  =  row2col_5_in_agaga2(x2, x4)
if_row2col_5_in_1_agaga8(x1, x2, x3, x4, x5, x6, x7, x8)  =  if_row2col_5_in_1_agaga1(x8)
row2col_5_in_aaaga5(x1, x2, x3, x4, x5)  =  row2col_5_in_aaaga1(x4)
if_row2col_5_in_1_aaaga8(x1, x2, x3, x4, x5, x6, x7, x8)  =  if_row2col_5_in_1_aaaga1(x8)
row2col_5_out_aaaga5(x1, x2, x3, x4, x5)  =  row2col_5_out_aaaga4(x1, x2, x3, x5)
row2col_5_out_agaga5(x1, x2, x3, x4, x5)  =  row2col_5_out_agaga3(x1, x3, x5)
if_transpose_aux_3_in_2_gga8(x1, x2, x3, x4, x5, x6, x7, x8)  =  if_transpose_aux_3_in_2_gga1(x8)
transpose_aux_3_in_agg3(x1, x2, x3)  =  transpose_aux_3_in_agg2(x2, x3)
if_transpose_aux_3_in_1_agg6(x1, x2, x3, x4, x5, x6)  =  if_transpose_aux_3_in_1_agg1(x6)
if_transpose_aux_3_in_2_agg8(x1, x2, x3, x4, x5, x6, x7, x8)  =  if_transpose_aux_3_in_2_agg1(x8)
transpose_aux_3_out_agg3(x1, x2, x3)  =  transpose_aux_3_out_agg1(x1)
transpose_aux_3_out_gga3(x1, x2, x3)  =  transpose_aux_3_out_gga1(x3)
transpose_2_out_ga2(x1, x2)  =  transpose_2_out_ga1(x2)
IF_TRANSPOSE_AUX_3_IN_1_GGA6(x1, x2, x3, x4, x5, x6)  =  IF_TRANSPOSE_AUX_3_IN_1_GGA1(x6)
IF_TRANSPOSE_AUX_3_IN_2_AGG8(x1, x2, x3, x4, x5, x6, x7, x8)  =  IF_TRANSPOSE_AUX_3_IN_2_AGG1(x8)
IF_TRANSPOSE_AUX_3_IN_1_AGG6(x1, x2, x3, x4, x5, x6)  =  IF_TRANSPOSE_AUX_3_IN_1_AGG1(x6)
ROW2COL_5_IN_AGAGA5(x1, x2, x3, x4, x5)  =  ROW2COL_5_IN_AGAGA2(x2, x4)
ROW2COL_5_IN_AAAGA5(x1, x2, x3, x4, x5)  =  ROW2COL_5_IN_AAAGA1(x4)
TRANSPOSE_2_IN_GA2(x1, x2)  =  TRANSPOSE_2_IN_GA1(x1)
IF_ROW2COL_5_IN_1_AGAGA8(x1, x2, x3, x4, x5, x6, x7, x8)  =  IF_ROW2COL_5_IN_1_AGAGA1(x8)
TRANSPOSE_AUX_3_IN_GGA3(x1, x2, x3)  =  TRANSPOSE_AUX_3_IN_GGA2(x1, x2)
IF_TRANSPOSE_2_IN_1_GA3(x1, x2, x3)  =  IF_TRANSPOSE_2_IN_1_GA1(x3)
TRANSPOSE_AUX_3_IN_AGG3(x1, x2, x3)  =  TRANSPOSE_AUX_3_IN_AGG2(x2, x3)
IF_ROW2COL_5_IN_1_AAAGA8(x1, x2, x3, x4, x5, x6, x7, x8)  =  IF_ROW2COL_5_IN_1_AAAGA1(x8)
IF_TRANSPOSE_AUX_3_IN_2_GGA8(x1, x2, x3, x4, x5, x6, x7, x8)  =  IF_TRANSPOSE_AUX_3_IN_2_GGA1(x8)

We have to consider all (P,R,Pi)-chains
The approximation of the Dependency Graph contains 2 SCCs with 11 less nodes.

↳ PROLOG
  ↳ PrologToPiTRSProof
    ↳ PiTRS
      ↳ DependencyPairsProof
        ↳ PiDP
          ↳ DependencyGraphProof
            ↳ AND
              ↳ PiDP
                ↳ UsableRulesProof
              ↳ PiDP
  ↳ PrologToPiTRSProof

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

ROW2COL_5_IN_AAAGA5(._22(X, Xs), ._22(._22(X, Ys), Cols), ._22(Ys, Cols1), A, B) -> ROW2COL_5_IN_AAAGA5(Xs, Cols, Cols1, ._22([]_0, A), B)

The TRS R consists of the following rules:

transpose_2_in_ga2(A, B) -> if_transpose_2_in_1_ga3(A, B, transpose_aux_3_in_gga3(A, []_0, B))
transpose_aux_3_in_gga3(._22(R, Rs), underscore, ._22(C, Cs)) -> if_transpose_aux_3_in_1_gga6(R, Rs, underscore, C, Cs, row2col_5_in_agaga5(R, ._22(C, Cs), Cols1, []_0, Accm))
row2col_5_in_agaga5(._22(X, Xs), ._22(._22(X, Ys), Cols), ._22(Ys, Cols1), A, B) -> if_row2col_5_in_1_agaga8(X, Xs, Ys, Cols, Cols1, A, B, row2col_5_in_aaaga5(Xs, Cols, Cols1, ._22([]_0, A), B))
row2col_5_in_aaaga5(._22(X, Xs), ._22(._22(X, Ys), Cols), ._22(Ys, Cols1), A, B) -> if_row2col_5_in_1_aaaga8(X, Xs, Ys, Cols, Cols1, A, B, row2col_5_in_aaaga5(Xs, Cols, Cols1, ._22([]_0, A), B))
row2col_5_in_aaaga5([]_0, []_0, []_0, A, A) -> row2col_5_out_aaaga5([]_0, []_0, []_0, A, A)
if_row2col_5_in_1_aaaga8(X, Xs, Ys, Cols, Cols1, A, B, row2col_5_out_aaaga5(Xs, Cols, Cols1, ._22([]_0, A), B)) -> row2col_5_out_aaaga5(._22(X, Xs), ._22(._22(X, Ys), Cols), ._22(Ys, Cols1), A, B)
if_row2col_5_in_1_agaga8(X, Xs, Ys, Cols, Cols1, A, B, row2col_5_out_aaaga5(Xs, Cols, Cols1, ._22([]_0, A), B)) -> row2col_5_out_agaga5(._22(X, Xs), ._22(._22(X, Ys), Cols), ._22(Ys, Cols1), A, B)
row2col_5_in_agaga5([]_0, []_0, []_0, A, A) -> row2col_5_out_agaga5([]_0, []_0, []_0, A, A)
if_transpose_aux_3_in_1_gga6(R, Rs, underscore, C, Cs, row2col_5_out_agaga5(R, ._22(C, Cs), Cols1, []_0, Accm)) -> if_transpose_aux_3_in_2_gga8(R, Rs, underscore, C, Cs, Cols1, Accm, transpose_aux_3_in_agg3(Rs, Accm, Cols1))
transpose_aux_3_in_agg3(._22(R, Rs), underscore, ._22(C, Cs)) -> if_transpose_aux_3_in_1_agg6(R, Rs, underscore, C, Cs, row2col_5_in_agaga5(R, ._22(C, Cs), Cols1, []_0, Accm))
if_transpose_aux_3_in_1_agg6(R, Rs, underscore, C, Cs, row2col_5_out_agaga5(R, ._22(C, Cs), Cols1, []_0, Accm)) -> if_transpose_aux_3_in_2_agg8(R, Rs, underscore, C, Cs, Cols1, Accm, transpose_aux_3_in_agg3(Rs, Accm, Cols1))
transpose_aux_3_in_agg3([]_0, X, X) -> transpose_aux_3_out_agg3([]_0, X, X)
if_transpose_aux_3_in_2_agg8(R, Rs, underscore, C, Cs, Cols1, Accm, transpose_aux_3_out_agg3(Rs, Accm, Cols1)) -> transpose_aux_3_out_agg3(._22(R, Rs), underscore, ._22(C, Cs))
if_transpose_aux_3_in_2_gga8(R, Rs, underscore, C, Cs, Cols1, Accm, transpose_aux_3_out_agg3(Rs, Accm, Cols1)) -> transpose_aux_3_out_gga3(._22(R, Rs), underscore, ._22(C, Cs))
transpose_aux_3_in_gga3([]_0, X, X) -> transpose_aux_3_out_gga3([]_0, X, X)
if_transpose_2_in_1_ga3(A, B, transpose_aux_3_out_gga3(A, []_0, B)) -> transpose_2_out_ga2(A, B)

The argument filtering Pi contains the following mapping:
transpose_2_in_ga2(x1, x2)  =  transpose_2_in_ga1(x1)
[]_0  =  []_0
._22(x1, x2)  =  ._2
if_transpose_2_in_1_ga3(x1, x2, x3)  =  if_transpose_2_in_1_ga1(x3)
transpose_aux_3_in_gga3(x1, x2, x3)  =  transpose_aux_3_in_gga2(x1, x2)
if_transpose_aux_3_in_1_gga6(x1, x2, x3, x4, x5, x6)  =  if_transpose_aux_3_in_1_gga1(x6)
row2col_5_in_agaga5(x1, x2, x3, x4, x5)  =  row2col_5_in_agaga2(x2, x4)
if_row2col_5_in_1_agaga8(x1, x2, x3, x4, x5, x6, x7, x8)  =  if_row2col_5_in_1_agaga1(x8)
row2col_5_in_aaaga5(x1, x2, x3, x4, x5)  =  row2col_5_in_aaaga1(x4)
if_row2col_5_in_1_aaaga8(x1, x2, x3, x4, x5, x6, x7, x8)  =  if_row2col_5_in_1_aaaga1(x8)
row2col_5_out_aaaga5(x1, x2, x3, x4, x5)  =  row2col_5_out_aaaga4(x1, x2, x3, x5)
row2col_5_out_agaga5(x1, x2, x3, x4, x5)  =  row2col_5_out_agaga3(x1, x3, x5)
if_transpose_aux_3_in_2_gga8(x1, x2, x3, x4, x5, x6, x7, x8)  =  if_transpose_aux_3_in_2_gga1(x8)
transpose_aux_3_in_agg3(x1, x2, x3)  =  transpose_aux_3_in_agg2(x2, x3)
if_transpose_aux_3_in_1_agg6(x1, x2, x3, x4, x5, x6)  =  if_transpose_aux_3_in_1_agg1(x6)
if_transpose_aux_3_in_2_agg8(x1, x2, x3, x4, x5, x6, x7, x8)  =  if_transpose_aux_3_in_2_agg1(x8)
transpose_aux_3_out_agg3(x1, x2, x3)  =  transpose_aux_3_out_agg1(x1)
transpose_aux_3_out_gga3(x1, x2, x3)  =  transpose_aux_3_out_gga1(x3)
transpose_2_out_ga2(x1, x2)  =  transpose_2_out_ga1(x2)
ROW2COL_5_IN_AAAGA5(x1, x2, x3, x4, x5)  =  ROW2COL_5_IN_AAAGA1(x4)

We have to consider all (P,R,Pi)-chains
For (infinitary) constructor rewriting we can delete all non-usable rules from R.

↳ PROLOG
  ↳ PrologToPiTRSProof
    ↳ PiTRS
      ↳ DependencyPairsProof
        ↳ PiDP
          ↳ DependencyGraphProof
            ↳ AND
              ↳ PiDP
                ↳ UsableRulesProof
                  ↳ PiDP
                    ↳ PiDPToQDPProof
              ↳ PiDP
  ↳ PrologToPiTRSProof

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

ROW2COL_5_IN_AAAGA5(._22(X, Xs), ._22(._22(X, Ys), Cols), ._22(Ys, Cols1), A, B) -> ROW2COL_5_IN_AAAGA5(Xs, Cols, Cols1, ._22([]_0, A), B)

R is empty.
The argument filtering Pi contains the following mapping:
[]_0  =  []_0
._22(x1, x2)  =  ._2
ROW2COL_5_IN_AAAGA5(x1, x2, x3, x4, x5)  =  ROW2COL_5_IN_AAAGA1(x4)

We have to consider all (P,R,Pi)-chains
Transforming (infinitary) constructor rewriting Pi-DP problem into ordinary QDP problem by application of Pi.

↳ PROLOG
  ↳ PrologToPiTRSProof
    ↳ PiTRS
      ↳ DependencyPairsProof
        ↳ PiDP
          ↳ DependencyGraphProof
            ↳ AND
              ↳ PiDP
                ↳ UsableRulesProof
                  ↳ PiDP
                    ↳ PiDPToQDPProof
                      ↳ QDP
              ↳ PiDP
  ↳ PrologToPiTRSProof

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

ROW2COL_5_IN_AAAGA1(A) -> ROW2COL_5_IN_AAAGA1(._2)

R is empty.
Q is empty.
We have to consider all (P,Q,R)-chains.
The head symbols of this DP problem are {ROW2COL_5_IN_AAAGA1}.

↳ PROLOG
  ↳ PrologToPiTRSProof
    ↳ PiTRS
      ↳ DependencyPairsProof
        ↳ PiDP
          ↳ DependencyGraphProof
            ↳ AND
              ↳ PiDP
              ↳ PiDP
                ↳ UsableRulesProof
  ↳ PrologToPiTRSProof

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

IF_TRANSPOSE_AUX_3_IN_1_AGG6(R, Rs, underscore, C, Cs, row2col_5_out_agaga5(R, ._22(C, Cs), Cols1, []_0, Accm)) -> TRANSPOSE_AUX_3_IN_AGG3(Rs, Accm, Cols1)
TRANSPOSE_AUX_3_IN_AGG3(._22(R, Rs), underscore, ._22(C, Cs)) -> IF_TRANSPOSE_AUX_3_IN_1_AGG6(R, Rs, underscore, C, Cs, row2col_5_in_agaga5(R, ._22(C, Cs), Cols1, []_0, Accm))

The TRS R consists of the following rules:

transpose_2_in_ga2(A, B) -> if_transpose_2_in_1_ga3(A, B, transpose_aux_3_in_gga3(A, []_0, B))
transpose_aux_3_in_gga3(._22(R, Rs), underscore, ._22(C, Cs)) -> if_transpose_aux_3_in_1_gga6(R, Rs, underscore, C, Cs, row2col_5_in_agaga5(R, ._22(C, Cs), Cols1, []_0, Accm))
row2col_5_in_agaga5(._22(X, Xs), ._22(._22(X, Ys), Cols), ._22(Ys, Cols1), A, B) -> if_row2col_5_in_1_agaga8(X, Xs, Ys, Cols, Cols1, A, B, row2col_5_in_aaaga5(Xs, Cols, Cols1, ._22([]_0, A), B))
row2col_5_in_aaaga5(._22(X, Xs), ._22(._22(X, Ys), Cols), ._22(Ys, Cols1), A, B) -> if_row2col_5_in_1_aaaga8(X, Xs, Ys, Cols, Cols1, A, B, row2col_5_in_aaaga5(Xs, Cols, Cols1, ._22([]_0, A), B))
row2col_5_in_aaaga5([]_0, []_0, []_0, A, A) -> row2col_5_out_aaaga5([]_0, []_0, []_0, A, A)
if_row2col_5_in_1_aaaga8(X, Xs, Ys, Cols, Cols1, A, B, row2col_5_out_aaaga5(Xs, Cols, Cols1, ._22([]_0, A), B)) -> row2col_5_out_aaaga5(._22(X, Xs), ._22(._22(X, Ys), Cols), ._22(Ys, Cols1), A, B)
if_row2col_5_in_1_agaga8(X, Xs, Ys, Cols, Cols1, A, B, row2col_5_out_aaaga5(Xs, Cols, Cols1, ._22([]_0, A), B)) -> row2col_5_out_agaga5(._22(X, Xs), ._22(._22(X, Ys), Cols), ._22(Ys, Cols1), A, B)
row2col_5_in_agaga5([]_0, []_0, []_0, A, A) -> row2col_5_out_agaga5([]_0, []_0, []_0, A, A)
if_transpose_aux_3_in_1_gga6(R, Rs, underscore, C, Cs, row2col_5_out_agaga5(R, ._22(C, Cs), Cols1, []_0, Accm)) -> if_transpose_aux_3_in_2_gga8(R, Rs, underscore, C, Cs, Cols1, Accm, transpose_aux_3_in_agg3(Rs, Accm, Cols1))
transpose_aux_3_in_agg3(._22(R, Rs), underscore, ._22(C, Cs)) -> if_transpose_aux_3_in_1_agg6(R, Rs, underscore, C, Cs, row2col_5_in_agaga5(R, ._22(C, Cs), Cols1, []_0, Accm))
if_transpose_aux_3_in_1_agg6(R, Rs, underscore, C, Cs, row2col_5_out_agaga5(R, ._22(C, Cs), Cols1, []_0, Accm)) -> if_transpose_aux_3_in_2_agg8(R, Rs, underscore, C, Cs, Cols1, Accm, transpose_aux_3_in_agg3(Rs, Accm, Cols1))
transpose_aux_3_in_agg3([]_0, X, X) -> transpose_aux_3_out_agg3([]_0, X, X)
if_transpose_aux_3_in_2_agg8(R, Rs, underscore, C, Cs, Cols1, Accm, transpose_aux_3_out_agg3(Rs, Accm, Cols1)) -> transpose_aux_3_out_agg3(._22(R, Rs), underscore, ._22(C, Cs))
if_transpose_aux_3_in_2_gga8(R, Rs, underscore, C, Cs, Cols1, Accm, transpose_aux_3_out_agg3(Rs, Accm, Cols1)) -> transpose_aux_3_out_gga3(._22(R, Rs), underscore, ._22(C, Cs))
transpose_aux_3_in_gga3([]_0, X, X) -> transpose_aux_3_out_gga3([]_0, X, X)
if_transpose_2_in_1_ga3(A, B, transpose_aux_3_out_gga3(A, []_0, B)) -> transpose_2_out_ga2(A, B)

The argument filtering Pi contains the following mapping:
transpose_2_in_ga2(x1, x2)  =  transpose_2_in_ga1(x1)
[]_0  =  []_0
._22(x1, x2)  =  ._2
if_transpose_2_in_1_ga3(x1, x2, x3)  =  if_transpose_2_in_1_ga1(x3)
transpose_aux_3_in_gga3(x1, x2, x3)  =  transpose_aux_3_in_gga2(x1, x2)
if_transpose_aux_3_in_1_gga6(x1, x2, x3, x4, x5, x6)  =  if_transpose_aux_3_in_1_gga1(x6)
row2col_5_in_agaga5(x1, x2, x3, x4, x5)  =  row2col_5_in_agaga2(x2, x4)
if_row2col_5_in_1_agaga8(x1, x2, x3, x4, x5, x6, x7, x8)  =  if_row2col_5_in_1_agaga1(x8)
row2col_5_in_aaaga5(x1, x2, x3, x4, x5)  =  row2col_5_in_aaaga1(x4)
if_row2col_5_in_1_aaaga8(x1, x2, x3, x4, x5, x6, x7, x8)  =  if_row2col_5_in_1_aaaga1(x8)
row2col_5_out_aaaga5(x1, x2, x3, x4, x5)  =  row2col_5_out_aaaga4(x1, x2, x3, x5)
row2col_5_out_agaga5(x1, x2, x3, x4, x5)  =  row2col_5_out_agaga3(x1, x3, x5)
if_transpose_aux_3_in_2_gga8(x1, x2, x3, x4, x5, x6, x7, x8)  =  if_transpose_aux_3_in_2_gga1(x8)
transpose_aux_3_in_agg3(x1, x2, x3)  =  transpose_aux_3_in_agg2(x2, x3)
if_transpose_aux_3_in_1_agg6(x1, x2, x3, x4, x5, x6)  =  if_transpose_aux_3_in_1_agg1(x6)
if_transpose_aux_3_in_2_agg8(x1, x2, x3, x4, x5, x6, x7, x8)  =  if_transpose_aux_3_in_2_agg1(x8)
transpose_aux_3_out_agg3(x1, x2, x3)  =  transpose_aux_3_out_agg1(x1)
transpose_aux_3_out_gga3(x1, x2, x3)  =  transpose_aux_3_out_gga1(x3)
transpose_2_out_ga2(x1, x2)  =  transpose_2_out_ga1(x2)
IF_TRANSPOSE_AUX_3_IN_1_AGG6(x1, x2, x3, x4, x5, x6)  =  IF_TRANSPOSE_AUX_3_IN_1_AGG1(x6)
TRANSPOSE_AUX_3_IN_AGG3(x1, x2, x3)  =  TRANSPOSE_AUX_3_IN_AGG2(x2, x3)

We have to consider all (P,R,Pi)-chains
For (infinitary) constructor rewriting we can delete all non-usable rules from R.

↳ PROLOG
  ↳ PrologToPiTRSProof
    ↳ PiTRS
      ↳ DependencyPairsProof
        ↳ PiDP
          ↳ DependencyGraphProof
            ↳ AND
              ↳ PiDP
              ↳ PiDP
                ↳ UsableRulesProof
                  ↳ PiDP
                    ↳ PiDPToQDPProof
  ↳ PrologToPiTRSProof

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

IF_TRANSPOSE_AUX_3_IN_1_AGG6(R, Rs, underscore, C, Cs, row2col_5_out_agaga5(R, ._22(C, Cs), Cols1, []_0, Accm)) -> TRANSPOSE_AUX_3_IN_AGG3(Rs, Accm, Cols1)
TRANSPOSE_AUX_3_IN_AGG3(._22(R, Rs), underscore, ._22(C, Cs)) -> IF_TRANSPOSE_AUX_3_IN_1_AGG6(R, Rs, underscore, C, Cs, row2col_5_in_agaga5(R, ._22(C, Cs), Cols1, []_0, Accm))

The TRS R consists of the following rules:

row2col_5_in_agaga5(._22(X, Xs), ._22(._22(X, Ys), Cols), ._22(Ys, Cols1), A, B) -> if_row2col_5_in_1_agaga8(X, Xs, Ys, Cols, Cols1, A, B, row2col_5_in_aaaga5(Xs, Cols, Cols1, ._22([]_0, A), B))
if_row2col_5_in_1_agaga8(X, Xs, Ys, Cols, Cols1, A, B, row2col_5_out_aaaga5(Xs, Cols, Cols1, ._22([]_0, A), B)) -> row2col_5_out_agaga5(._22(X, Xs), ._22(._22(X, Ys), Cols), ._22(Ys, Cols1), A, B)
row2col_5_in_aaaga5(._22(X, Xs), ._22(._22(X, Ys), Cols), ._22(Ys, Cols1), A, B) -> if_row2col_5_in_1_aaaga8(X, Xs, Ys, Cols, Cols1, A, B, row2col_5_in_aaaga5(Xs, Cols, Cols1, ._22([]_0, A), B))
row2col_5_in_aaaga5([]_0, []_0, []_0, A, A) -> row2col_5_out_aaaga5([]_0, []_0, []_0, A, A)
if_row2col_5_in_1_aaaga8(X, Xs, Ys, Cols, Cols1, A, B, row2col_5_out_aaaga5(Xs, Cols, Cols1, ._22([]_0, A), B)) -> row2col_5_out_aaaga5(._22(X, Xs), ._22(._22(X, Ys), Cols), ._22(Ys, Cols1), A, B)

The argument filtering Pi contains the following mapping:
[]_0  =  []_0
._22(x1, x2)  =  ._2
row2col_5_in_agaga5(x1, x2, x3, x4, x5)  =  row2col_5_in_agaga2(x2, x4)
if_row2col_5_in_1_agaga8(x1, x2, x3, x4, x5, x6, x7, x8)  =  if_row2col_5_in_1_agaga1(x8)
row2col_5_in_aaaga5(x1, x2, x3, x4, x5)  =  row2col_5_in_aaaga1(x4)
if_row2col_5_in_1_aaaga8(x1, x2, x3, x4, x5, x6, x7, x8)  =  if_row2col_5_in_1_aaaga1(x8)
row2col_5_out_aaaga5(x1, x2, x3, x4, x5)  =  row2col_5_out_aaaga4(x1, x2, x3, x5)
row2col_5_out_agaga5(x1, x2, x3, x4, x5)  =  row2col_5_out_agaga3(x1, x3, x5)
IF_TRANSPOSE_AUX_3_IN_1_AGG6(x1, x2, x3, x4, x5, x6)  =  IF_TRANSPOSE_AUX_3_IN_1_AGG1(x6)
TRANSPOSE_AUX_3_IN_AGG3(x1, x2, x3)  =  TRANSPOSE_AUX_3_IN_AGG2(x2, x3)

We have to consider all (P,R,Pi)-chains
Transforming (infinitary) constructor rewriting Pi-DP problem into ordinary QDP problem by application of Pi.

↳ PROLOG
  ↳ PrologToPiTRSProof
    ↳ PiTRS
      ↳ DependencyPairsProof
        ↳ PiDP
          ↳ DependencyGraphProof
            ↳ AND
              ↳ PiDP
              ↳ PiDP
                ↳ UsableRulesProof
                  ↳ PiDP
                    ↳ PiDPToQDPProof
                      ↳ QDP
  ↳ PrologToPiTRSProof

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

IF_TRANSPOSE_AUX_3_IN_1_AGG1(row2col_5_out_agaga3(R, Cols1, Accm)) -> TRANSPOSE_AUX_3_IN_AGG2(Accm, Cols1)
TRANSPOSE_AUX_3_IN_AGG2(underscore, ._2) -> IF_TRANSPOSE_AUX_3_IN_1_AGG1(row2col_5_in_agaga2(._2, []_0))

The TRS R consists of the following rules:

row2col_5_in_agaga2(._2, A) -> if_row2col_5_in_1_agaga1(row2col_5_in_aaaga1(._2))
if_row2col_5_in_1_agaga1(row2col_5_out_aaaga4(Xs, Cols, Cols1, B)) -> row2col_5_out_agaga3(._2, ._2, B)
row2col_5_in_aaaga1(A) -> if_row2col_5_in_1_aaaga1(row2col_5_in_aaaga1(._2))
row2col_5_in_aaaga1(A) -> row2col_5_out_aaaga4([]_0, []_0, []_0, A)
if_row2col_5_in_1_aaaga1(row2col_5_out_aaaga4(Xs, Cols, Cols1, B)) -> row2col_5_out_aaaga4(._2, ._2, ._2, B)

The set Q consists of the following terms:

row2col_5_in_agaga2(x0, x1)
if_row2col_5_in_1_agaga1(x0)
row2col_5_in_aaaga1(x0)
if_row2col_5_in_1_aaaga1(x0)

We have to consider all (P,Q,R)-chains.
The head symbols of this DP problem are {TRANSPOSE_AUX_3_IN_AGG2, IF_TRANSPOSE_AUX_3_IN_1_AGG1}.
With regard to the inferred argument filtering the predicates were used in the following modes:
transpose2: (b,f)
transpose_aux3: (b,b,f) (f,b,b)
row2col5: (f,b,f,b,f) (f,f,f,b,f)
Transforming PROLOG into the following Term Rewriting System:
Pi-finite rewrite system:
The TRS R consists of the following rules:

transpose_2_in_ga2(A, B) -> if_transpose_2_in_1_ga3(A, B, transpose_aux_3_in_gga3(A, []_0, B))
transpose_aux_3_in_gga3(._22(R, Rs), underscore, ._22(C, Cs)) -> if_transpose_aux_3_in_1_gga6(R, Rs, underscore, C, Cs, row2col_5_in_agaga5(R, ._22(C, Cs), Cols1, []_0, Accm))
row2col_5_in_agaga5(._22(X, Xs), ._22(._22(X, Ys), Cols), ._22(Ys, Cols1), A, B) -> if_row2col_5_in_1_agaga8(X, Xs, Ys, Cols, Cols1, A, B, row2col_5_in_aaaga5(Xs, Cols, Cols1, ._22([]_0, A), B))
row2col_5_in_aaaga5(._22(X, Xs), ._22(._22(X, Ys), Cols), ._22(Ys, Cols1), A, B) -> if_row2col_5_in_1_aaaga8(X, Xs, Ys, Cols, Cols1, A, B, row2col_5_in_aaaga5(Xs, Cols, Cols1, ._22([]_0, A), B))
row2col_5_in_aaaga5([]_0, []_0, []_0, A, A) -> row2col_5_out_aaaga5([]_0, []_0, []_0, A, A)
if_row2col_5_in_1_aaaga8(X, Xs, Ys, Cols, Cols1, A, B, row2col_5_out_aaaga5(Xs, Cols, Cols1, ._22([]_0, A), B)) -> row2col_5_out_aaaga5(._22(X, Xs), ._22(._22(X, Ys), Cols), ._22(Ys, Cols1), A, B)
if_row2col_5_in_1_agaga8(X, Xs, Ys, Cols, Cols1, A, B, row2col_5_out_aaaga5(Xs, Cols, Cols1, ._22([]_0, A), B)) -> row2col_5_out_agaga5(._22(X, Xs), ._22(._22(X, Ys), Cols), ._22(Ys, Cols1), A, B)
row2col_5_in_agaga5([]_0, []_0, []_0, A, A) -> row2col_5_out_agaga5([]_0, []_0, []_0, A, A)
if_transpose_aux_3_in_1_gga6(R, Rs, underscore, C, Cs, row2col_5_out_agaga5(R, ._22(C, Cs), Cols1, []_0, Accm)) -> if_transpose_aux_3_in_2_gga8(R, Rs, underscore, C, Cs, Cols1, Accm, transpose_aux_3_in_agg3(Rs, Accm, Cols1))
transpose_aux_3_in_agg3(._22(R, Rs), underscore, ._22(C, Cs)) -> if_transpose_aux_3_in_1_agg6(R, Rs, underscore, C, Cs, row2col_5_in_agaga5(R, ._22(C, Cs), Cols1, []_0, Accm))
if_transpose_aux_3_in_1_agg6(R, Rs, underscore, C, Cs, row2col_5_out_agaga5(R, ._22(C, Cs), Cols1, []_0, Accm)) -> if_transpose_aux_3_in_2_agg8(R, Rs, underscore, C, Cs, Cols1, Accm, transpose_aux_3_in_agg3(Rs, Accm, Cols1))
transpose_aux_3_in_agg3([]_0, X, X) -> transpose_aux_3_out_agg3([]_0, X, X)
if_transpose_aux_3_in_2_agg8(R, Rs, underscore, C, Cs, Cols1, Accm, transpose_aux_3_out_agg3(Rs, Accm, Cols1)) -> transpose_aux_3_out_agg3(._22(R, Rs), underscore, ._22(C, Cs))
if_transpose_aux_3_in_2_gga8(R, Rs, underscore, C, Cs, Cols1, Accm, transpose_aux_3_out_agg3(Rs, Accm, Cols1)) -> transpose_aux_3_out_gga3(._22(R, Rs), underscore, ._22(C, Cs))
transpose_aux_3_in_gga3([]_0, X, X) -> transpose_aux_3_out_gga3([]_0, X, X)
if_transpose_2_in_1_ga3(A, B, transpose_aux_3_out_gga3(A, []_0, B)) -> transpose_2_out_ga2(A, B)

The argument filtering Pi contains the following mapping:
transpose_2_in_ga2(x1, x2)  =  transpose_2_in_ga1(x1)
[]_0  =  []_0
._22(x1, x2)  =  ._2
if_transpose_2_in_1_ga3(x1, x2, x3)  =  if_transpose_2_in_1_ga2(x1, x3)
transpose_aux_3_in_gga3(x1, x2, x3)  =  transpose_aux_3_in_gga2(x1, x2)
if_transpose_aux_3_in_1_gga6(x1, x2, x3, x4, x5, x6)  =  if_transpose_aux_3_in_1_gga2(x3, x6)
row2col_5_in_agaga5(x1, x2, x3, x4, x5)  =  row2col_5_in_agaga2(x2, x4)
if_row2col_5_in_1_agaga8(x1, x2, x3, x4, x5, x6, x7, x8)  =  if_row2col_5_in_1_agaga2(x6, x8)
row2col_5_in_aaaga5(x1, x2, x3, x4, x5)  =  row2col_5_in_aaaga1(x4)
if_row2col_5_in_1_aaaga8(x1, x2, x3, x4, x5, x6, x7, x8)  =  if_row2col_5_in_1_aaaga2(x6, x8)
row2col_5_out_aaaga5(x1, x2, x3, x4, x5)  =  row2col_5_out_aaaga5(x1, x2, x3, x4, x5)
row2col_5_out_agaga5(x1, x2, x3, x4, x5)  =  row2col_5_out_agaga5(x1, x2, x3, x4, x5)
if_transpose_aux_3_in_2_gga8(x1, x2, x3, x4, x5, x6, x7, x8)  =  if_transpose_aux_3_in_2_gga2(x3, x8)
transpose_aux_3_in_agg3(x1, x2, x3)  =  transpose_aux_3_in_agg2(x2, x3)
if_transpose_aux_3_in_1_agg6(x1, x2, x3, x4, x5, x6)  =  if_transpose_aux_3_in_1_agg2(x3, x6)
if_transpose_aux_3_in_2_agg8(x1, x2, x3, x4, x5, x6, x7, x8)  =  if_transpose_aux_3_in_2_agg2(x3, x8)
transpose_aux_3_out_agg3(x1, x2, x3)  =  transpose_aux_3_out_agg3(x1, x2, x3)
transpose_aux_3_out_gga3(x1, x2, x3)  =  transpose_aux_3_out_gga3(x1, x2, x3)
transpose_2_out_ga2(x1, x2)  =  transpose_2_out_ga2(x1, x2)

Infinitary Constructor Rewriting Termination of PiTRS implies Termination of PROLOG



↳ PROLOG
  ↳ PrologToPiTRSProof
  ↳ PrologToPiTRSProof
    ↳ PiTRS

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

transpose_2_in_ga2(A, B) -> if_transpose_2_in_1_ga3(A, B, transpose_aux_3_in_gga3(A, []_0, B))
transpose_aux_3_in_gga3(._22(R, Rs), underscore, ._22(C, Cs)) -> if_transpose_aux_3_in_1_gga6(R, Rs, underscore, C, Cs, row2col_5_in_agaga5(R, ._22(C, Cs), Cols1, []_0, Accm))
row2col_5_in_agaga5(._22(X, Xs), ._22(._22(X, Ys), Cols), ._22(Ys, Cols1), A, B) -> if_row2col_5_in_1_agaga8(X, Xs, Ys, Cols, Cols1, A, B, row2col_5_in_aaaga5(Xs, Cols, Cols1, ._22([]_0, A), B))
row2col_5_in_aaaga5(._22(X, Xs), ._22(._22(X, Ys), Cols), ._22(Ys, Cols1), A, B) -> if_row2col_5_in_1_aaaga8(X, Xs, Ys, Cols, Cols1, A, B, row2col_5_in_aaaga5(Xs, Cols, Cols1, ._22([]_0, A), B))
row2col_5_in_aaaga5([]_0, []_0, []_0, A, A) -> row2col_5_out_aaaga5([]_0, []_0, []_0, A, A)
if_row2col_5_in_1_aaaga8(X, Xs, Ys, Cols, Cols1, A, B, row2col_5_out_aaaga5(Xs, Cols, Cols1, ._22([]_0, A), B)) -> row2col_5_out_aaaga5(._22(X, Xs), ._22(._22(X, Ys), Cols), ._22(Ys, Cols1), A, B)
if_row2col_5_in_1_agaga8(X, Xs, Ys, Cols, Cols1, A, B, row2col_5_out_aaaga5(Xs, Cols, Cols1, ._22([]_0, A), B)) -> row2col_5_out_agaga5(._22(X, Xs), ._22(._22(X, Ys), Cols), ._22(Ys, Cols1), A, B)
row2col_5_in_agaga5([]_0, []_0, []_0, A, A) -> row2col_5_out_agaga5([]_0, []_0, []_0, A, A)
if_transpose_aux_3_in_1_gga6(R, Rs, underscore, C, Cs, row2col_5_out_agaga5(R, ._22(C, Cs), Cols1, []_0, Accm)) -> if_transpose_aux_3_in_2_gga8(R, Rs, underscore, C, Cs, Cols1, Accm, transpose_aux_3_in_agg3(Rs, Accm, Cols1))
transpose_aux_3_in_agg3(._22(R, Rs), underscore, ._22(C, Cs)) -> if_transpose_aux_3_in_1_agg6(R, Rs, underscore, C, Cs, row2col_5_in_agaga5(R, ._22(C, Cs), Cols1, []_0, Accm))
if_transpose_aux_3_in_1_agg6(R, Rs, underscore, C, Cs, row2col_5_out_agaga5(R, ._22(C, Cs), Cols1, []_0, Accm)) -> if_transpose_aux_3_in_2_agg8(R, Rs, underscore, C, Cs, Cols1, Accm, transpose_aux_3_in_agg3(Rs, Accm, Cols1))
transpose_aux_3_in_agg3([]_0, X, X) -> transpose_aux_3_out_agg3([]_0, X, X)
if_transpose_aux_3_in_2_agg8(R, Rs, underscore, C, Cs, Cols1, Accm, transpose_aux_3_out_agg3(Rs, Accm, Cols1)) -> transpose_aux_3_out_agg3(._22(R, Rs), underscore, ._22(C, Cs))
if_transpose_aux_3_in_2_gga8(R, Rs, underscore, C, Cs, Cols1, Accm, transpose_aux_3_out_agg3(Rs, Accm, Cols1)) -> transpose_aux_3_out_gga3(._22(R, Rs), underscore, ._22(C, Cs))
transpose_aux_3_in_gga3([]_0, X, X) -> transpose_aux_3_out_gga3([]_0, X, X)
if_transpose_2_in_1_ga3(A, B, transpose_aux_3_out_gga3(A, []_0, B)) -> transpose_2_out_ga2(A, B)

The argument filtering Pi contains the following mapping:
transpose_2_in_ga2(x1, x2)  =  transpose_2_in_ga1(x1)
[]_0  =  []_0
._22(x1, x2)  =  ._2
if_transpose_2_in_1_ga3(x1, x2, x3)  =  if_transpose_2_in_1_ga2(x1, x3)
transpose_aux_3_in_gga3(x1, x2, x3)  =  transpose_aux_3_in_gga2(x1, x2)
if_transpose_aux_3_in_1_gga6(x1, x2, x3, x4, x5, x6)  =  if_transpose_aux_3_in_1_gga2(x3, x6)
row2col_5_in_agaga5(x1, x2, x3, x4, x5)  =  row2col_5_in_agaga2(x2, x4)
if_row2col_5_in_1_agaga8(x1, x2, x3, x4, x5, x6, x7, x8)  =  if_row2col_5_in_1_agaga2(x6, x8)
row2col_5_in_aaaga5(x1, x2, x3, x4, x5)  =  row2col_5_in_aaaga1(x4)
if_row2col_5_in_1_aaaga8(x1, x2, x3, x4, x5, x6, x7, x8)  =  if_row2col_5_in_1_aaaga2(x6, x8)
row2col_5_out_aaaga5(x1, x2, x3, x4, x5)  =  row2col_5_out_aaaga5(x1, x2, x3, x4, x5)
row2col_5_out_agaga5(x1, x2, x3, x4, x5)  =  row2col_5_out_agaga5(x1, x2, x3, x4, x5)
if_transpose_aux_3_in_2_gga8(x1, x2, x3, x4, x5, x6, x7, x8)  =  if_transpose_aux_3_in_2_gga2(x3, x8)
transpose_aux_3_in_agg3(x1, x2, x3)  =  transpose_aux_3_in_agg2(x2, x3)
if_transpose_aux_3_in_1_agg6(x1, x2, x3, x4, x5, x6)  =  if_transpose_aux_3_in_1_agg2(x3, x6)
if_transpose_aux_3_in_2_agg8(x1, x2, x3, x4, x5, x6, x7, x8)  =  if_transpose_aux_3_in_2_agg2(x3, x8)
transpose_aux_3_out_agg3(x1, x2, x3)  =  transpose_aux_3_out_agg3(x1, x2, x3)
transpose_aux_3_out_gga3(x1, x2, x3)  =  transpose_aux_3_out_gga3(x1, x2, x3)
transpose_2_out_ga2(x1, x2)  =  transpose_2_out_ga2(x1, x2)