Left Termination proof of /tmp/tmpS5pOlN/transpose-bf.pl

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

↳ PROLOG

  ↳ PrologToPiTRSProof

  ↳ PrologToPiTRSProof

transpose₂(A, B) :- transpose_aux₃(A, {}₀, B).
transpose_aux₃(.₂(R, Rs), underscore, .₂(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₄({}₀, {}₀, {}₀, {}₀).

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

transpose_2_in_ga₂(A, B) -> if_transpose_2_in_1_ga₃(A, B, transpose_aux_3_in_gga₃(A, []_0, B))
transpose_aux_3_in_gga₃(._2₂(R, Rs), underscore, ._2₂(C, Cs)) -> if_transpose_aux_3_in_1_gga₆(R, Rs, underscore, C, Cs, row2col_4_in_agaa₄(R, ._2₂(C, Cs), Cols1, Accm))
row2col_4_in_agaa₄(._2₂(X, Xs), ._2₂(._2₂(X, Ys), Cols), ._2₂(Ys, Cols1), ._2₂([]_0, As)) -> if_row2col_4_in_1_agaa₇(X, Xs, Ys, Cols, Cols1, As, row2col_4_in_aaaa₄(Xs, Cols, Cols1, As))
row2col_4_in_aaaa₄(._2₂(X, Xs), ._2₂(._2₂(X, Ys), Cols), ._2₂(Ys, Cols1), ._2₂([]_0, As)) -> if_row2col_4_in_1_aaaa₇(X, Xs, Ys, Cols, Cols1, As, row2col_4_in_aaaa₄(Xs, Cols, Cols1, As))
row2col_4_in_aaaa₄([]_0, []_0, []_0, []_0) -> row2col_4_out_aaaa₄([]_0, []_0, []_0, []_0)
if_row2col_4_in_1_aaaa₇(X, Xs, Ys, Cols, Cols1, As, row2col_4_out_aaaa₄(Xs, Cols, Cols1, As)) -> row2col_4_out_aaaa₄(._2₂(X, Xs), ._2₂(._2₂(X, Ys), Cols), ._2₂(Ys, Cols1), ._2₂([]_0, As))
if_row2col_4_in_1_agaa₇(X, Xs, Ys, Cols, Cols1, As, row2col_4_out_aaaa₄(Xs, Cols, Cols1, As)) -> row2col_4_out_agaa₄(._2₂(X, Xs), ._2₂(._2₂(X, Ys), Cols), ._2₂(Ys, Cols1), ._2₂([]_0, As))
row2col_4_in_agaa₄([]_0, []_0, []_0, []_0) -> row2col_4_out_agaa₄([]_0, []_0, []_0, []_0)
if_transpose_aux_3_in_1_gga₆(R, Rs, underscore, C, Cs, row2col_4_out_agaa₄(R, ._2₂(C, Cs), Cols1, Accm)) -> if_transpose_aux_3_in_2_gga₈(R, Rs, underscore, C, Cs, Cols1, Accm, transpose_aux_3_in_agg₃(Rs, Accm, Cols1))
transpose_aux_3_in_agg₃(._2₂(R, Rs), underscore, ._2₂(C, Cs)) -> if_transpose_aux_3_in_1_agg₆(R, Rs, underscore, C, Cs, row2col_4_in_agaa₄(R, ._2₂(C, Cs), Cols1, Accm))
if_transpose_aux_3_in_1_agg₆(R, Rs, underscore, C, Cs, row2col_4_out_agaa₄(R, ._2₂(C, Cs), Cols1, Accm)) -> if_transpose_aux_3_in_2_agg₈(R, Rs, underscore, C, Cs, Cols1, Accm, transpose_aux_3_in_agg₃(Rs, Accm, Cols1))
transpose_aux_3_in_agg₃([]_0, X, X) -> transpose_aux_3_out_agg₃([]_0, X, X)
if_transpose_aux_3_in_2_agg₈(R, Rs, underscore, C, Cs, Cols1, Accm, transpose_aux_3_out_agg₃(Rs, Accm, Cols1)) -> transpose_aux_3_out_agg₃(._2₂(R, Rs), underscore, ._2₂(C, Cs))
if_transpose_aux_3_in_2_gga₈(R, Rs, underscore, C, Cs, Cols1, Accm, transpose_aux_3_out_agg₃(Rs, Accm, Cols1)) -> transpose_aux_3_out_gga₃(._2₂(R, Rs), underscore, ._2₂(C, Cs))
transpose_aux_3_in_gga₃([]_0, X, X) -> transpose_aux_3_out_gga₃([]_0, X, X)
if_transpose_2_in_1_ga₃(A, B, transpose_aux_3_out_gga₃(A, []_0, B)) -> transpose_2_out_ga₂(A, B)

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_ga₂(A, B) -> if_transpose_2_in_1_ga₃(A, B, transpose_aux_3_in_gga₃(A, []_0, B))
transpose_aux_3_in_gga₃(._2₂(R, Rs), underscore, ._2₂(C, Cs)) -> if_transpose_aux_3_in_1_gga₆(R, Rs, underscore, C, Cs, row2col_4_in_agaa₄(R, ._2₂(C, Cs), Cols1, Accm))
row2col_4_in_agaa₄(._2₂(X, Xs), ._2₂(._2₂(X, Ys), Cols), ._2₂(Ys, Cols1), ._2₂([]_0, As)) -> if_row2col_4_in_1_agaa₇(X, Xs, Ys, Cols, Cols1, As, row2col_4_in_aaaa₄(Xs, Cols, Cols1, As))
row2col_4_in_aaaa₄(._2₂(X, Xs), ._2₂(._2₂(X, Ys), Cols), ._2₂(Ys, Cols1), ._2₂([]_0, As)) -> if_row2col_4_in_1_aaaa₇(X, Xs, Ys, Cols, Cols1, As, row2col_4_in_aaaa₄(Xs, Cols, Cols1, As))
row2col_4_in_aaaa₄([]_0, []_0, []_0, []_0) -> row2col_4_out_aaaa₄([]_0, []_0, []_0, []_0)
if_row2col_4_in_1_aaaa₇(X, Xs, Ys, Cols, Cols1, As, row2col_4_out_aaaa₄(Xs, Cols, Cols1, As)) -> row2col_4_out_aaaa₄(._2₂(X, Xs), ._2₂(._2₂(X, Ys), Cols), ._2₂(Ys, Cols1), ._2₂([]_0, As))
if_row2col_4_in_1_agaa₇(X, Xs, Ys, Cols, Cols1, As, row2col_4_out_aaaa₄(Xs, Cols, Cols1, As)) -> row2col_4_out_agaa₄(._2₂(X, Xs), ._2₂(._2₂(X, Ys), Cols), ._2₂(Ys, Cols1), ._2₂([]_0, As))
row2col_4_in_agaa₄([]_0, []_0, []_0, []_0) -> row2col_4_out_agaa₄([]_0, []_0, []_0, []_0)
if_transpose_aux_3_in_1_gga₆(R, Rs, underscore, C, Cs, row2col_4_out_agaa₄(R, ._2₂(C, Cs), Cols1, Accm)) -> if_transpose_aux_3_in_2_gga₈(R, Rs, underscore, C, Cs, Cols1, Accm, transpose_aux_3_in_agg₃(Rs, Accm, Cols1))
transpose_aux_3_in_agg₃(._2₂(R, Rs), underscore, ._2₂(C, Cs)) -> if_transpose_aux_3_in_1_agg₆(R, Rs, underscore, C, Cs, row2col_4_in_agaa₄(R, ._2₂(C, Cs), Cols1, Accm))
if_transpose_aux_3_in_1_agg₆(R, Rs, underscore, C, Cs, row2col_4_out_agaa₄(R, ._2₂(C, Cs), Cols1, Accm)) -> if_transpose_aux_3_in_2_agg₈(R, Rs, underscore, C, Cs, Cols1, Accm, transpose_aux_3_in_agg₃(Rs, Accm, Cols1))
transpose_aux_3_in_agg₃([]_0, X, X) -> transpose_aux_3_out_agg₃([]_0, X, X)
if_transpose_aux_3_in_2_agg₈(R, Rs, underscore, C, Cs, Cols1, Accm, transpose_aux_3_out_agg₃(Rs, Accm, Cols1)) -> transpose_aux_3_out_agg₃(._2₂(R, Rs), underscore, ._2₂(C, Cs))
if_transpose_aux_3_in_2_gga₈(R, Rs, underscore, C, Cs, Cols1, Accm, transpose_aux_3_out_agg₃(Rs, Accm, Cols1)) -> transpose_aux_3_out_gga₃(._2₂(R, Rs), underscore, ._2₂(C, Cs))
transpose_aux_3_in_gga₃([]_0, X, X) -> transpose_aux_3_out_gga₃([]_0, X, X)
if_transpose_2_in_1_ga₃(A, B, transpose_aux_3_out_gga₃(A, []_0, B)) -> transpose_2_out_ga₂(A, B)

TRANSPOSE_2_IN_GA₂(A, B) -> IF_TRANSPOSE_2_IN_1_GA₃(A, B, transpose_aux_3_in_gga₃(A, []_0, B))
TRANSPOSE_2_IN_GA₂(A, B) -> TRANSPOSE_AUX_3_IN_GGA₃(A, []_0, B)
TRANSPOSE_AUX_3_IN_GGA₃(._2₂(R, Rs), underscore, ._2₂(C, Cs)) -> IF_TRANSPOSE_AUX_3_IN_1_GGA₆(R, Rs, underscore, C, Cs, row2col_4_in_agaa₄(R, ._2₂(C, Cs), Cols1, Accm))
TRANSPOSE_AUX_3_IN_GGA₃(._2₂(R, Rs), underscore, ._2₂(C, Cs)) -> ROW2COL_4_IN_AGAA₄(R, ._2₂(C, Cs), Cols1, Accm)
ROW2COL_4_IN_AGAA₄(._2₂(X, Xs), ._2₂(._2₂(X, Ys), Cols), ._2₂(Ys, Cols1), ._2₂([]_0, As)) -> IF_ROW2COL_4_IN_1_AGAA₇(X, Xs, Ys, Cols, Cols1, As, row2col_4_in_aaaa₄(Xs, Cols, Cols1, As))
ROW2COL_4_IN_AGAA₄(._2₂(X, Xs), ._2₂(._2₂(X, Ys), Cols), ._2₂(Ys, Cols1), ._2₂([]_0, As)) -> ROW2COL_4_IN_AAAA₄(Xs, Cols, Cols1, As)
ROW2COL_4_IN_AAAA₄(._2₂(X, Xs), ._2₂(._2₂(X, Ys), Cols), ._2₂(Ys, Cols1), ._2₂([]_0, As)) -> IF_ROW2COL_4_IN_1_AAAA₇(X, Xs, Ys, Cols, Cols1, As, row2col_4_in_aaaa₄(Xs, Cols, Cols1, As))
ROW2COL_4_IN_AAAA₄(._2₂(X, Xs), ._2₂(._2₂(X, Ys), Cols), ._2₂(Ys, Cols1), ._2₂([]_0, As)) -> ROW2COL_4_IN_AAAA₄(Xs, Cols, Cols1, As)
IF_TRANSPOSE_AUX_3_IN_1_GGA₆(R, Rs, underscore, C, Cs, row2col_4_out_agaa₄(R, ._2₂(C, Cs), Cols1, Accm)) -> IF_TRANSPOSE_AUX_3_IN_2_GGA₈(R, Rs, underscore, C, Cs, Cols1, Accm, transpose_aux_3_in_agg₃(Rs, Accm, Cols1))
IF_TRANSPOSE_AUX_3_IN_1_GGA₆(R, Rs, underscore, C, Cs, row2col_4_out_agaa₄(R, ._2₂(C, Cs), Cols1, Accm)) -> TRANSPOSE_AUX_3_IN_AGG₃(Rs, Accm, Cols1)
TRANSPOSE_AUX_3_IN_AGG₃(._2₂(R, Rs), underscore, ._2₂(C, Cs)) -> IF_TRANSPOSE_AUX_3_IN_1_AGG₆(R, Rs, underscore, C, Cs, row2col_4_in_agaa₄(R, ._2₂(C, Cs), Cols1, Accm))
TRANSPOSE_AUX_3_IN_AGG₃(._2₂(R, Rs), underscore, ._2₂(C, Cs)) -> ROW2COL_4_IN_AGAA₄(R, ._2₂(C, Cs), Cols1, Accm)
IF_TRANSPOSE_AUX_3_IN_1_AGG₆(R, Rs, underscore, C, Cs, row2col_4_out_agaa₄(R, ._2₂(C, Cs), Cols1, Accm)) -> IF_TRANSPOSE_AUX_3_IN_2_AGG₈(R, Rs, underscore, C, Cs, Cols1, Accm, transpose_aux_3_in_agg₃(Rs, Accm, Cols1))
IF_TRANSPOSE_AUX_3_IN_1_AGG₆(R, Rs, underscore, C, Cs, row2col_4_out_agaa₄(R, ._2₂(C, Cs), Cols1, Accm)) -> TRANSPOSE_AUX_3_IN_AGG₃(Rs, Accm, Cols1)

The TRS R consists of the following rules:

transpose_2_in_ga₂(A, B) -> if_transpose_2_in_1_ga₃(A, B, transpose_aux_3_in_gga₃(A, []_0, B))
transpose_aux_3_in_gga₃(._2₂(R, Rs), underscore, ._2₂(C, Cs)) -> if_transpose_aux_3_in_1_gga₆(R, Rs, underscore, C, Cs, row2col_4_in_agaa₄(R, ._2₂(C, Cs), Cols1, Accm))
row2col_4_in_agaa₄(._2₂(X, Xs), ._2₂(._2₂(X, Ys), Cols), ._2₂(Ys, Cols1), ._2₂([]_0, As)) -> if_row2col_4_in_1_agaa₇(X, Xs, Ys, Cols, Cols1, As, row2col_4_in_aaaa₄(Xs, Cols, Cols1, As))
row2col_4_in_aaaa₄(._2₂(X, Xs), ._2₂(._2₂(X, Ys), Cols), ._2₂(Ys, Cols1), ._2₂([]_0, As)) -> if_row2col_4_in_1_aaaa₇(X, Xs, Ys, Cols, Cols1, As, row2col_4_in_aaaa₄(Xs, Cols, Cols1, As))
row2col_4_in_aaaa₄([]_0, []_0, []_0, []_0) -> row2col_4_out_aaaa₄([]_0, []_0, []_0, []_0)
if_row2col_4_in_1_aaaa₇(X, Xs, Ys, Cols, Cols1, As, row2col_4_out_aaaa₄(Xs, Cols, Cols1, As)) -> row2col_4_out_aaaa₄(._2₂(X, Xs), ._2₂(._2₂(X, Ys), Cols), ._2₂(Ys, Cols1), ._2₂([]_0, As))
if_row2col_4_in_1_agaa₇(X, Xs, Ys, Cols, Cols1, As, row2col_4_out_aaaa₄(Xs, Cols, Cols1, As)) -> row2col_4_out_agaa₄(._2₂(X, Xs), ._2₂(._2₂(X, Ys), Cols), ._2₂(Ys, Cols1), ._2₂([]_0, As))
row2col_4_in_agaa₄([]_0, []_0, []_0, []_0) -> row2col_4_out_agaa₄([]_0, []_0, []_0, []_0)
if_transpose_aux_3_in_1_gga₆(R, Rs, underscore, C, Cs, row2col_4_out_agaa₄(R, ._2₂(C, Cs), Cols1, Accm)) -> if_transpose_aux_3_in_2_gga₈(R, Rs, underscore, C, Cs, Cols1, Accm, transpose_aux_3_in_agg₃(Rs, Accm, Cols1))
transpose_aux_3_in_agg₃(._2₂(R, Rs), underscore, ._2₂(C, Cs)) -> if_transpose_aux_3_in_1_agg₆(R, Rs, underscore, C, Cs, row2col_4_in_agaa₄(R, ._2₂(C, Cs), Cols1, Accm))
if_transpose_aux_3_in_1_agg₆(R, Rs, underscore, C, Cs, row2col_4_out_agaa₄(R, ._2₂(C, Cs), Cols1, Accm)) -> if_transpose_aux_3_in_2_agg₈(R, Rs, underscore, C, Cs, Cols1, Accm, transpose_aux_3_in_agg₃(Rs, Accm, Cols1))
transpose_aux_3_in_agg₃([]_0, X, X) -> transpose_aux_3_out_agg₃([]_0, X, X)
if_transpose_aux_3_in_2_agg₈(R, Rs, underscore, C, Cs, Cols1, Accm, transpose_aux_3_out_agg₃(Rs, Accm, Cols1)) -> transpose_aux_3_out_agg₃(._2₂(R, Rs), underscore, ._2₂(C, Cs))
if_transpose_aux_3_in_2_gga₈(R, Rs, underscore, C, Cs, Cols1, Accm, transpose_aux_3_out_agg₃(Rs, Accm, Cols1)) -> transpose_aux_3_out_gga₃(._2₂(R, Rs), underscore, ._2₂(C, Cs))
transpose_aux_3_in_gga₃([]_0, X, X) -> transpose_aux_3_out_gga₃([]_0, X, X)
if_transpose_2_in_1_ga₃(A, B, transpose_aux_3_out_gga₃(A, []_0, B)) -> transpose_2_out_ga₂(A, B)

The argument filtering Pi contains the following mapping:
transpose_2_in_ga₂(x1, x2) = transpose_2_in_ga₁(x1)
[]_0 = []_0
._2₂(x1, x2) = ._2
if_transpose_2_in_1_ga₃(x1, x2, x3) = if_transpose_2_in_1_ga₁(x3)
transpose_aux_3_in_gga₃(x1, x2, x3) = transpose_aux_3_in_gga₂(x1, x2)
if_transpose_aux_3_in_1_gga₆(x1, x2, x3, x4, x5, x6) = if_transpose_aux_3_in_1_gga₁(x6)
row2col_4_in_agaa₄(x1, x2, x3, x4) = row2col_4_in_agaa₁(x2)
if_row2col_4_in_1_agaa₇(x1, x2, x3, x4, x5, x6, x7) = if_row2col_4_in_1_agaa₁(x7)
row2col_4_in_aaaa₄(x1, x2, x3, x4) = row2col_4_in_aaaa
if_row2col_4_in_1_aaaa₇(x1, x2, x3, x4, x5, x6, x7) = if_row2col_4_in_1_aaaa₁(x7)
row2col_4_out_aaaa₄(x1, x2, x3, x4) = row2col_4_out_aaaa₄(x1, x2, x3, x4)
row2col_4_out_agaa₄(x1, x2, x3, x4) = row2col_4_out_agaa₃(x1, x3, x4)
if_transpose_aux_3_in_2_gga₈(x1, x2, x3, x4, x5, x6, x7, x8) = if_transpose_aux_3_in_2_gga₁(x8)
transpose_aux_3_in_agg₃(x1, x2, x3) = transpose_aux_3_in_agg₂(x2, x3)
if_transpose_aux_3_in_1_agg₆(x1, x2, x3, x4, x5, x6) = if_transpose_aux_3_in_1_agg₁(x6)
if_transpose_aux_3_in_2_agg₈(x1, x2, x3, x4, x5, x6, x7, x8) = if_transpose_aux_3_in_2_agg₁(x8)
transpose_aux_3_out_agg₃(x1, x2, x3) = transpose_aux_3_out_agg₁(x1)
transpose_aux_3_out_gga₃(x1, x2, x3) = transpose_aux_3_out_gga₁(x3)
transpose_2_out_ga₂(x1, x2) = transpose_2_out_ga₁(x2)
IF_TRANSPOSE_AUX_3_IN_1_GGA₆(x1, x2, x3, x4, x5, x6) = IF_TRANSPOSE_AUX_3_IN_1_GGA₁(x6)
IF_TRANSPOSE_AUX_3_IN_2_AGG₈(x1, x2, x3, x4, x5, x6, x7, x8) = IF_TRANSPOSE_AUX_3_IN_2_AGG₁(x8)
IF_TRANSPOSE_AUX_3_IN_1_AGG₆(x1, x2, x3, x4, x5, x6) = IF_TRANSPOSE_AUX_3_IN_1_AGG₁(x6)
IF_ROW2COL_4_IN_1_AAAA₇(x1, x2, x3, x4, x5, x6, x7) = IF_ROW2COL_4_IN_1_AAAA₁(x7)
TRANSPOSE_2_IN_GA₂(x1, x2) = TRANSPOSE_2_IN_GA₁(x1)
TRANSPOSE_AUX_3_IN_GGA₃(x1, x2, x3) = TRANSPOSE_AUX_3_IN_GGA₂(x1, x2)
IF_TRANSPOSE_2_IN_1_GA₃(x1, x2, x3) = IF_TRANSPOSE_2_IN_1_GA₁(x3)
TRANSPOSE_AUX_3_IN_AGG₃(x1, x2, x3) = TRANSPOSE_AUX_3_IN_AGG₂(x2, x3)
ROW2COL_4_IN_AGAA₄(x1, x2, x3, x4) = ROW2COL_4_IN_AGAA₁(x2)
IF_ROW2COL_4_IN_1_AGAA₇(x1, x2, x3, x4, x5, x6, x7) = IF_ROW2COL_4_IN_1_AGAA₁(x7)
ROW2COL_4_IN_AAAA₄(x1, x2, x3, x4) = ROW2COL_4_IN_AAAA
IF_TRANSPOSE_AUX_3_IN_2_GGA₈(x1, x2, x3, x4, x5, x6, x7, x8) = IF_TRANSPOSE_AUX_3_IN_2_GGA₁(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_GA₂(A, B) -> IF_TRANSPOSE_2_IN_1_GA₃(A, B, transpose_aux_3_in_gga₃(A, []_0, B))
TRANSPOSE_2_IN_GA₂(A, B) -> TRANSPOSE_AUX_3_IN_GGA₃(A, []_0, B)
TRANSPOSE_AUX_3_IN_GGA₃(._2₂(R, Rs), underscore, ._2₂(C, Cs)) -> IF_TRANSPOSE_AUX_3_IN_1_GGA₆(R, Rs, underscore, C, Cs, row2col_4_in_agaa₄(R, ._2₂(C, Cs), Cols1, Accm))
TRANSPOSE_AUX_3_IN_GGA₃(._2₂(R, Rs), underscore, ._2₂(C, Cs)) -> ROW2COL_4_IN_AGAA₄(R, ._2₂(C, Cs), Cols1, Accm)
ROW2COL_4_IN_AGAA₄(._2₂(X, Xs), ._2₂(._2₂(X, Ys), Cols), ._2₂(Ys, Cols1), ._2₂([]_0, As)) -> IF_ROW2COL_4_IN_1_AGAA₇(X, Xs, Ys, Cols, Cols1, As, row2col_4_in_aaaa₄(Xs, Cols, Cols1, As))
ROW2COL_4_IN_AGAA₄(._2₂(X, Xs), ._2₂(._2₂(X, Ys), Cols), ._2₂(Ys, Cols1), ._2₂([]_0, As)) -> ROW2COL_4_IN_AAAA₄(Xs, Cols, Cols1, As)
ROW2COL_4_IN_AAAA₄(._2₂(X, Xs), ._2₂(._2₂(X, Ys), Cols), ._2₂(Ys, Cols1), ._2₂([]_0, As)) -> IF_ROW2COL_4_IN_1_AAAA₇(X, Xs, Ys, Cols, Cols1, As, row2col_4_in_aaaa₄(Xs, Cols, Cols1, As))
ROW2COL_4_IN_AAAA₄(._2₂(X, Xs), ._2₂(._2₂(X, Ys), Cols), ._2₂(Ys, Cols1), ._2₂([]_0, As)) -> ROW2COL_4_IN_AAAA₄(Xs, Cols, Cols1, As)
IF_TRANSPOSE_AUX_3_IN_1_GGA₆(R, Rs, underscore, C, Cs, row2col_4_out_agaa₄(R, ._2₂(C, Cs), Cols1, Accm)) -> IF_TRANSPOSE_AUX_3_IN_2_GGA₈(R, Rs, underscore, C, Cs, Cols1, Accm, transpose_aux_3_in_agg₃(Rs, Accm, Cols1))
IF_TRANSPOSE_AUX_3_IN_1_GGA₆(R, Rs, underscore, C, Cs, row2col_4_out_agaa₄(R, ._2₂(C, Cs), Cols1, Accm)) -> TRANSPOSE_AUX_3_IN_AGG₃(Rs, Accm, Cols1)
TRANSPOSE_AUX_3_IN_AGG₃(._2₂(R, Rs), underscore, ._2₂(C, Cs)) -> IF_TRANSPOSE_AUX_3_IN_1_AGG₆(R, Rs, underscore, C, Cs, row2col_4_in_agaa₄(R, ._2₂(C, Cs), Cols1, Accm))
TRANSPOSE_AUX_3_IN_AGG₃(._2₂(R, Rs), underscore, ._2₂(C, Cs)) -> ROW2COL_4_IN_AGAA₄(R, ._2₂(C, Cs), Cols1, Accm)
IF_TRANSPOSE_AUX_3_IN_1_AGG₆(R, Rs, underscore, C, Cs, row2col_4_out_agaa₄(R, ._2₂(C, Cs), Cols1, Accm)) -> IF_TRANSPOSE_AUX_3_IN_2_AGG₈(R, Rs, underscore, C, Cs, Cols1, Accm, transpose_aux_3_in_agg₃(Rs, Accm, Cols1))
IF_TRANSPOSE_AUX_3_IN_1_AGG₆(R, Rs, underscore, C, Cs, row2col_4_out_agaa₄(R, ._2₂(C, Cs), Cols1, Accm)) -> TRANSPOSE_AUX_3_IN_AGG₃(Rs, Accm, Cols1)

The TRS R consists of the following rules:

transpose_2_in_ga₂(A, B) -> if_transpose_2_in_1_ga₃(A, B, transpose_aux_3_in_gga₃(A, []_0, B))
transpose_aux_3_in_gga₃(._2₂(R, Rs), underscore, ._2₂(C, Cs)) -> if_transpose_aux_3_in_1_gga₆(R, Rs, underscore, C, Cs, row2col_4_in_agaa₄(R, ._2₂(C, Cs), Cols1, Accm))
row2col_4_in_agaa₄(._2₂(X, Xs), ._2₂(._2₂(X, Ys), Cols), ._2₂(Ys, Cols1), ._2₂([]_0, As)) -> if_row2col_4_in_1_agaa₇(X, Xs, Ys, Cols, Cols1, As, row2col_4_in_aaaa₄(Xs, Cols, Cols1, As))
row2col_4_in_aaaa₄(._2₂(X, Xs), ._2₂(._2₂(X, Ys), Cols), ._2₂(Ys, Cols1), ._2₂([]_0, As)) -> if_row2col_4_in_1_aaaa₇(X, Xs, Ys, Cols, Cols1, As, row2col_4_in_aaaa₄(Xs, Cols, Cols1, As))
row2col_4_in_aaaa₄([]_0, []_0, []_0, []_0) -> row2col_4_out_aaaa₄([]_0, []_0, []_0, []_0)
if_row2col_4_in_1_aaaa₇(X, Xs, Ys, Cols, Cols1, As, row2col_4_out_aaaa₄(Xs, Cols, Cols1, As)) -> row2col_4_out_aaaa₄(._2₂(X, Xs), ._2₂(._2₂(X, Ys), Cols), ._2₂(Ys, Cols1), ._2₂([]_0, As))
if_row2col_4_in_1_agaa₇(X, Xs, Ys, Cols, Cols1, As, row2col_4_out_aaaa₄(Xs, Cols, Cols1, As)) -> row2col_4_out_agaa₄(._2₂(X, Xs), ._2₂(._2₂(X, Ys), Cols), ._2₂(Ys, Cols1), ._2₂([]_0, As))
row2col_4_in_agaa₄([]_0, []_0, []_0, []_0) -> row2col_4_out_agaa₄([]_0, []_0, []_0, []_0)
if_transpose_aux_3_in_1_gga₆(R, Rs, underscore, C, Cs, row2col_4_out_agaa₄(R, ._2₂(C, Cs), Cols1, Accm)) -> if_transpose_aux_3_in_2_gga₈(R, Rs, underscore, C, Cs, Cols1, Accm, transpose_aux_3_in_agg₃(Rs, Accm, Cols1))
transpose_aux_3_in_agg₃(._2₂(R, Rs), underscore, ._2₂(C, Cs)) -> if_transpose_aux_3_in_1_agg₆(R, Rs, underscore, C, Cs, row2col_4_in_agaa₄(R, ._2₂(C, Cs), Cols1, Accm))
if_transpose_aux_3_in_1_agg₆(R, Rs, underscore, C, Cs, row2col_4_out_agaa₄(R, ._2₂(C, Cs), Cols1, Accm)) -> if_transpose_aux_3_in_2_agg₈(R, Rs, underscore, C, Cs, Cols1, Accm, transpose_aux_3_in_agg₃(Rs, Accm, Cols1))
transpose_aux_3_in_agg₃([]_0, X, X) -> transpose_aux_3_out_agg₃([]_0, X, X)
if_transpose_aux_3_in_2_agg₈(R, Rs, underscore, C, Cs, Cols1, Accm, transpose_aux_3_out_agg₃(Rs, Accm, Cols1)) -> transpose_aux_3_out_agg₃(._2₂(R, Rs), underscore, ._2₂(C, Cs))
if_transpose_aux_3_in_2_gga₈(R, Rs, underscore, C, Cs, Cols1, Accm, transpose_aux_3_out_agg₃(Rs, Accm, Cols1)) -> transpose_aux_3_out_gga₃(._2₂(R, Rs), underscore, ._2₂(C, Cs))
transpose_aux_3_in_gga₃([]_0, X, X) -> transpose_aux_3_out_gga₃([]_0, X, X)
if_transpose_2_in_1_ga₃(A, B, transpose_aux_3_out_gga₃(A, []_0, B)) -> transpose_2_out_ga₂(A, B)

↳ PROLOG

  ↳ PrologToPiTRSProof

    ↳ PiTRS

      ↳ DependencyPairsProof

        ↳ PiDP

          ↳ DependencyGraphProof

            ↳ AND

              ↳ PiDP

                ↳ UsableRulesProof

              ↳ PiDP

  ↳ PrologToPiTRSProof

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

ROW2COL_4_IN_AAAA₄(._2₂(X, Xs), ._2₂(._2₂(X, Ys), Cols), ._2₂(Ys, Cols1), ._2₂([]_0, As)) -> ROW2COL_4_IN_AAAA₄(Xs, Cols, Cols1, As)

The TRS R consists of the following rules:

transpose_2_in_ga₂(A, B) -> if_transpose_2_in_1_ga₃(A, B, transpose_aux_3_in_gga₃(A, []_0, B))
transpose_aux_3_in_gga₃(._2₂(R, Rs), underscore, ._2₂(C, Cs)) -> if_transpose_aux_3_in_1_gga₆(R, Rs, underscore, C, Cs, row2col_4_in_agaa₄(R, ._2₂(C, Cs), Cols1, Accm))
row2col_4_in_agaa₄(._2₂(X, Xs), ._2₂(._2₂(X, Ys), Cols), ._2₂(Ys, Cols1), ._2₂([]_0, As)) -> if_row2col_4_in_1_agaa₇(X, Xs, Ys, Cols, Cols1, As, row2col_4_in_aaaa₄(Xs, Cols, Cols1, As))
row2col_4_in_aaaa₄(._2₂(X, Xs), ._2₂(._2₂(X, Ys), Cols), ._2₂(Ys, Cols1), ._2₂([]_0, As)) -> if_row2col_4_in_1_aaaa₇(X, Xs, Ys, Cols, Cols1, As, row2col_4_in_aaaa₄(Xs, Cols, Cols1, As))
row2col_4_in_aaaa₄([]_0, []_0, []_0, []_0) -> row2col_4_out_aaaa₄([]_0, []_0, []_0, []_0)
if_row2col_4_in_1_aaaa₇(X, Xs, Ys, Cols, Cols1, As, row2col_4_out_aaaa₄(Xs, Cols, Cols1, As)) -> row2col_4_out_aaaa₄(._2₂(X, Xs), ._2₂(._2₂(X, Ys), Cols), ._2₂(Ys, Cols1), ._2₂([]_0, As))
if_row2col_4_in_1_agaa₇(X, Xs, Ys, Cols, Cols1, As, row2col_4_out_aaaa₄(Xs, Cols, Cols1, As)) -> row2col_4_out_agaa₄(._2₂(X, Xs), ._2₂(._2₂(X, Ys), Cols), ._2₂(Ys, Cols1), ._2₂([]_0, As))
row2col_4_in_agaa₄([]_0, []_0, []_0, []_0) -> row2col_4_out_agaa₄([]_0, []_0, []_0, []_0)
if_transpose_aux_3_in_1_gga₆(R, Rs, underscore, C, Cs, row2col_4_out_agaa₄(R, ._2₂(C, Cs), Cols1, Accm)) -> if_transpose_aux_3_in_2_gga₈(R, Rs, underscore, C, Cs, Cols1, Accm, transpose_aux_3_in_agg₃(Rs, Accm, Cols1))
transpose_aux_3_in_agg₃(._2₂(R, Rs), underscore, ._2₂(C, Cs)) -> if_transpose_aux_3_in_1_agg₆(R, Rs, underscore, C, Cs, row2col_4_in_agaa₄(R, ._2₂(C, Cs), Cols1, Accm))
if_transpose_aux_3_in_1_agg₆(R, Rs, underscore, C, Cs, row2col_4_out_agaa₄(R, ._2₂(C, Cs), Cols1, Accm)) -> if_transpose_aux_3_in_2_agg₈(R, Rs, underscore, C, Cs, Cols1, Accm, transpose_aux_3_in_agg₃(Rs, Accm, Cols1))
transpose_aux_3_in_agg₃([]_0, X, X) -> transpose_aux_3_out_agg₃([]_0, X, X)
if_transpose_aux_3_in_2_agg₈(R, Rs, underscore, C, Cs, Cols1, Accm, transpose_aux_3_out_agg₃(Rs, Accm, Cols1)) -> transpose_aux_3_out_agg₃(._2₂(R, Rs), underscore, ._2₂(C, Cs))
if_transpose_aux_3_in_2_gga₈(R, Rs, underscore, C, Cs, Cols1, Accm, transpose_aux_3_out_agg₃(Rs, Accm, Cols1)) -> transpose_aux_3_out_gga₃(._2₂(R, Rs), underscore, ._2₂(C, Cs))
transpose_aux_3_in_gga₃([]_0, X, X) -> transpose_aux_3_out_gga₃([]_0, X, X)
if_transpose_2_in_1_ga₃(A, B, transpose_aux_3_out_gga₃(A, []_0, B)) -> transpose_2_out_ga₂(A, B)

↳ 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_4_IN_AAAA₄(._2₂(X, Xs), ._2₂(._2₂(X, Ys), Cols), ._2₂(Ys, Cols1), ._2₂([]_0, As)) -> ROW2COL_4_IN_AAAA₄(Xs, Cols, Cols1, As)

R is empty.
The argument filtering Pi contains the following mapping:
[]_0 = []_0
._2₂(x1, x2) = ._2
ROW2COL_4_IN_AAAA₄(x1, x2, x3, x4) = ROW2COL_4_IN_AAAA

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_4_IN_AAAA -> ROW2COL_4_IN_AAAA

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

↳ 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_AGG₆(R, Rs, underscore, C, Cs, row2col_4_out_agaa₄(R, ._2₂(C, Cs), Cols1, Accm)) -> TRANSPOSE_AUX_3_IN_AGG₃(Rs, Accm, Cols1)
TRANSPOSE_AUX_3_IN_AGG₃(._2₂(R, Rs), underscore, ._2₂(C, Cs)) -> IF_TRANSPOSE_AUX_3_IN_1_AGG₆(R, Rs, underscore, C, Cs, row2col_4_in_agaa₄(R, ._2₂(C, Cs), Cols1, Accm))

The TRS R consists of the following rules:

transpose_2_in_ga₂(A, B) -> if_transpose_2_in_1_ga₃(A, B, transpose_aux_3_in_gga₃(A, []_0, B))
transpose_aux_3_in_gga₃(._2₂(R, Rs), underscore, ._2₂(C, Cs)) -> if_transpose_aux_3_in_1_gga₆(R, Rs, underscore, C, Cs, row2col_4_in_agaa₄(R, ._2₂(C, Cs), Cols1, Accm))
row2col_4_in_agaa₄(._2₂(X, Xs), ._2₂(._2₂(X, Ys), Cols), ._2₂(Ys, Cols1), ._2₂([]_0, As)) -> if_row2col_4_in_1_agaa₇(X, Xs, Ys, Cols, Cols1, As, row2col_4_in_aaaa₄(Xs, Cols, Cols1, As))
row2col_4_in_aaaa₄(._2₂(X, Xs), ._2₂(._2₂(X, Ys), Cols), ._2₂(Ys, Cols1), ._2₂([]_0, As)) -> if_row2col_4_in_1_aaaa₇(X, Xs, Ys, Cols, Cols1, As, row2col_4_in_aaaa₄(Xs, Cols, Cols1, As))
row2col_4_in_aaaa₄([]_0, []_0, []_0, []_0) -> row2col_4_out_aaaa₄([]_0, []_0, []_0, []_0)
if_row2col_4_in_1_aaaa₇(X, Xs, Ys, Cols, Cols1, As, row2col_4_out_aaaa₄(Xs, Cols, Cols1, As)) -> row2col_4_out_aaaa₄(._2₂(X, Xs), ._2₂(._2₂(X, Ys), Cols), ._2₂(Ys, Cols1), ._2₂([]_0, As))
if_row2col_4_in_1_agaa₇(X, Xs, Ys, Cols, Cols1, As, row2col_4_out_aaaa₄(Xs, Cols, Cols1, As)) -> row2col_4_out_agaa₄(._2₂(X, Xs), ._2₂(._2₂(X, Ys), Cols), ._2₂(Ys, Cols1), ._2₂([]_0, As))
row2col_4_in_agaa₄([]_0, []_0, []_0, []_0) -> row2col_4_out_agaa₄([]_0, []_0, []_0, []_0)
if_transpose_aux_3_in_1_gga₆(R, Rs, underscore, C, Cs, row2col_4_out_agaa₄(R, ._2₂(C, Cs), Cols1, Accm)) -> if_transpose_aux_3_in_2_gga₈(R, Rs, underscore, C, Cs, Cols1, Accm, transpose_aux_3_in_agg₃(Rs, Accm, Cols1))
transpose_aux_3_in_agg₃(._2₂(R, Rs), underscore, ._2₂(C, Cs)) -> if_transpose_aux_3_in_1_agg₆(R, Rs, underscore, C, Cs, row2col_4_in_agaa₄(R, ._2₂(C, Cs), Cols1, Accm))
if_transpose_aux_3_in_1_agg₆(R, Rs, underscore, C, Cs, row2col_4_out_agaa₄(R, ._2₂(C, Cs), Cols1, Accm)) -> if_transpose_aux_3_in_2_agg₈(R, Rs, underscore, C, Cs, Cols1, Accm, transpose_aux_3_in_agg₃(Rs, Accm, Cols1))
transpose_aux_3_in_agg₃([]_0, X, X) -> transpose_aux_3_out_agg₃([]_0, X, X)
if_transpose_aux_3_in_2_agg₈(R, Rs, underscore, C, Cs, Cols1, Accm, transpose_aux_3_out_agg₃(Rs, Accm, Cols1)) -> transpose_aux_3_out_agg₃(._2₂(R, Rs), underscore, ._2₂(C, Cs))
if_transpose_aux_3_in_2_gga₈(R, Rs, underscore, C, Cs, Cols1, Accm, transpose_aux_3_out_agg₃(Rs, Accm, Cols1)) -> transpose_aux_3_out_gga₃(._2₂(R, Rs), underscore, ._2₂(C, Cs))
transpose_aux_3_in_gga₃([]_0, X, X) -> transpose_aux_3_out_gga₃([]_0, X, X)
if_transpose_2_in_1_ga₃(A, B, transpose_aux_3_out_gga₃(A, []_0, B)) -> transpose_2_out_ga₂(A, B)

↳ 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_AGG₆(R, Rs, underscore, C, Cs, row2col_4_out_agaa₄(R, ._2₂(C, Cs), Cols1, Accm)) -> TRANSPOSE_AUX_3_IN_AGG₃(Rs, Accm, Cols1)
TRANSPOSE_AUX_3_IN_AGG₃(._2₂(R, Rs), underscore, ._2₂(C, Cs)) -> IF_TRANSPOSE_AUX_3_IN_1_AGG₆(R, Rs, underscore, C, Cs, row2col_4_in_agaa₄(R, ._2₂(C, Cs), Cols1, Accm))

The TRS R consists of the following rules:

row2col_4_in_agaa₄(._2₂(X, Xs), ._2₂(._2₂(X, Ys), Cols), ._2₂(Ys, Cols1), ._2₂([]_0, As)) -> if_row2col_4_in_1_agaa₇(X, Xs, Ys, Cols, Cols1, As, row2col_4_in_aaaa₄(Xs, Cols, Cols1, As))
if_row2col_4_in_1_agaa₇(X, Xs, Ys, Cols, Cols1, As, row2col_4_out_aaaa₄(Xs, Cols, Cols1, As)) -> row2col_4_out_agaa₄(._2₂(X, Xs), ._2₂(._2₂(X, Ys), Cols), ._2₂(Ys, Cols1), ._2₂([]_0, As))
row2col_4_in_aaaa₄(._2₂(X, Xs), ._2₂(._2₂(X, Ys), Cols), ._2₂(Ys, Cols1), ._2₂([]_0, As)) -> if_row2col_4_in_1_aaaa₇(X, Xs, Ys, Cols, Cols1, As, row2col_4_in_aaaa₄(Xs, Cols, Cols1, As))
row2col_4_in_aaaa₄([]_0, []_0, []_0, []_0) -> row2col_4_out_aaaa₄([]_0, []_0, []_0, []_0)
if_row2col_4_in_1_aaaa₇(X, Xs, Ys, Cols, Cols1, As, row2col_4_out_aaaa₄(Xs, Cols, Cols1, As)) -> row2col_4_out_aaaa₄(._2₂(X, Xs), ._2₂(._2₂(X, Ys), Cols), ._2₂(Ys, Cols1), ._2₂([]_0, As))

The argument filtering Pi contains the following mapping:
[]_0 = []_0
._2₂(x1, x2) = ._2
row2col_4_in_agaa₄(x1, x2, x3, x4) = row2col_4_in_agaa₁(x2)
if_row2col_4_in_1_agaa₇(x1, x2, x3, x4, x5, x6, x7) = if_row2col_4_in_1_agaa₁(x7)
row2col_4_in_aaaa₄(x1, x2, x3, x4) = row2col_4_in_aaaa
if_row2col_4_in_1_aaaa₇(x1, x2, x3, x4, x5, x6, x7) = if_row2col_4_in_1_aaaa₁(x7)
row2col_4_out_aaaa₄(x1, x2, x3, x4) = row2col_4_out_aaaa₄(x1, x2, x3, x4)
row2col_4_out_agaa₄(x1, x2, x3, x4) = row2col_4_out_agaa₃(x1, x3, x4)
IF_TRANSPOSE_AUX_3_IN_1_AGG₆(x1, x2, x3, x4, x5, x6) = IF_TRANSPOSE_AUX_3_IN_1_AGG₁(x6)
TRANSPOSE_AUX_3_IN_AGG₃(x1, x2, x3) = TRANSPOSE_AUX_3_IN_AGG₂(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_AGG₁(row2col_4_out_agaa₃(R, Cols1, Accm)) -> TRANSPOSE_AUX_3_IN_AGG₂(Accm, Cols1)
TRANSPOSE_AUX_3_IN_AGG₂(underscore, ._2) -> IF_TRANSPOSE_AUX_3_IN_1_AGG₁(row2col_4_in_agaa₁(._2))

The TRS R consists of the following rules:

row2col_4_in_agaa₁(._2) -> if_row2col_4_in_1_agaa₁(row2col_4_in_aaaa)
if_row2col_4_in_1_agaa₁(row2col_4_out_aaaa₄(Xs, Cols, Cols1, As)) -> row2col_4_out_agaa₃(._2, ._2, ._2)
row2col_4_in_aaaa -> if_row2col_4_in_1_aaaa₁(row2col_4_in_aaaa)
row2col_4_in_aaaa -> row2col_4_out_aaaa₄([]_0, []_0, []_0, []_0)
if_row2col_4_in_1_aaaa₁(row2col_4_out_aaaa₄(Xs, Cols, Cols1, As)) -> row2col_4_out_aaaa₄(._2, ._2, ._2, ._2)

The set Q consists of the following terms:

row2col_4_in_agaa₁(x0)
if_row2col_4_in_1_agaa₁(x0)
row2col_4_in_aaaa
if_row2col_4_in_1_aaaa₁(x0)

We have to consider all (P,Q,R)-chains.
The head symbols of this DP problem are {TRANSPOSE_AUX_3_IN_AGG₂, IF_TRANSPOSE_AUX_3_IN_1_AGG₁}.
With regard to the inferred argument filtering the predicates were used in the following modes:
transpose₂: (b,f)
transpose_aux₃: (b,b,f) (f,b,b)
row2col₄: (f,b,f,f) (f,f,f,f)
Transforming PROLOG into the following Term Rewriting System:
Pi-finite rewrite system:
The TRS R consists of the following rules:

transpose_2_in_ga₂(A, B) -> if_transpose_2_in_1_ga₃(A, B, transpose_aux_3_in_gga₃(A, []_0, B))
transpose_aux_3_in_gga₃(._2₂(R, Rs), underscore, ._2₂(C, Cs)) -> if_transpose_aux_3_in_1_gga₆(R, Rs, underscore, C, Cs, row2col_4_in_agaa₄(R, ._2₂(C, Cs), Cols1, Accm))
row2col_4_in_agaa₄(._2₂(X, Xs), ._2₂(._2₂(X, Ys), Cols), ._2₂(Ys, Cols1), ._2₂([]_0, As)) -> if_row2col_4_in_1_agaa₇(X, Xs, Ys, Cols, Cols1, As, row2col_4_in_aaaa₄(Xs, Cols, Cols1, As))
row2col_4_in_aaaa₄(._2₂(X, Xs), ._2₂(._2₂(X, Ys), Cols), ._2₂(Ys, Cols1), ._2₂([]_0, As)) -> if_row2col_4_in_1_aaaa₇(X, Xs, Ys, Cols, Cols1, As, row2col_4_in_aaaa₄(Xs, Cols, Cols1, As))
row2col_4_in_aaaa₄([]_0, []_0, []_0, []_0) -> row2col_4_out_aaaa₄([]_0, []_0, []_0, []_0)
if_row2col_4_in_1_aaaa₇(X, Xs, Ys, Cols, Cols1, As, row2col_4_out_aaaa₄(Xs, Cols, Cols1, As)) -> row2col_4_out_aaaa₄(._2₂(X, Xs), ._2₂(._2₂(X, Ys), Cols), ._2₂(Ys, Cols1), ._2₂([]_0, As))
if_row2col_4_in_1_agaa₇(X, Xs, Ys, Cols, Cols1, As, row2col_4_out_aaaa₄(Xs, Cols, Cols1, As)) -> row2col_4_out_agaa₄(._2₂(X, Xs), ._2₂(._2₂(X, Ys), Cols), ._2₂(Ys, Cols1), ._2₂([]_0, As))
row2col_4_in_agaa₄([]_0, []_0, []_0, []_0) -> row2col_4_out_agaa₄([]_0, []_0, []_0, []_0)
if_transpose_aux_3_in_1_gga₆(R, Rs, underscore, C, Cs, row2col_4_out_agaa₄(R, ._2₂(C, Cs), Cols1, Accm)) -> if_transpose_aux_3_in_2_gga₈(R, Rs, underscore, C, Cs, Cols1, Accm, transpose_aux_3_in_agg₃(Rs, Accm, Cols1))
transpose_aux_3_in_agg₃(._2₂(R, Rs), underscore, ._2₂(C, Cs)) -> if_transpose_aux_3_in_1_agg₆(R, Rs, underscore, C, Cs, row2col_4_in_agaa₄(R, ._2₂(C, Cs), Cols1, Accm))
if_transpose_aux_3_in_1_agg₆(R, Rs, underscore, C, Cs, row2col_4_out_agaa₄(R, ._2₂(C, Cs), Cols1, Accm)) -> if_transpose_aux_3_in_2_agg₈(R, Rs, underscore, C, Cs, Cols1, Accm, transpose_aux_3_in_agg₃(Rs, Accm, Cols1))
transpose_aux_3_in_agg₃([]_0, X, X) -> transpose_aux_3_out_agg₃([]_0, X, X)
if_transpose_aux_3_in_2_agg₈(R, Rs, underscore, C, Cs, Cols1, Accm, transpose_aux_3_out_agg₃(Rs, Accm, Cols1)) -> transpose_aux_3_out_agg₃(._2₂(R, Rs), underscore, ._2₂(C, Cs))
if_transpose_aux_3_in_2_gga₈(R, Rs, underscore, C, Cs, Cols1, Accm, transpose_aux_3_out_agg₃(Rs, Accm, Cols1)) -> transpose_aux_3_out_gga₃(._2₂(R, Rs), underscore, ._2₂(C, Cs))
transpose_aux_3_in_gga₃([]_0, X, X) -> transpose_aux_3_out_gga₃([]_0, X, X)
if_transpose_2_in_1_ga₃(A, B, transpose_aux_3_out_gga₃(A, []_0, B)) -> transpose_2_out_ga₂(A, B)

Infinitary Constructor Rewriting Termination of PiTRS implies Termination of PROLOG

↳ PROLOG

  ↳ PrologToPiTRSProof

  ↳ PrologToPiTRSProof

    ↳ PiTRS

      ↳ DependencyPairsProof

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

transpose_2_in_ga₂(A, B) -> if_transpose_2_in_1_ga₃(A, B, transpose_aux_3_in_gga₃(A, []_0, B))
transpose_aux_3_in_gga₃(._2₂(R, Rs), underscore, ._2₂(C, Cs)) -> if_transpose_aux_3_in_1_gga₆(R, Rs, underscore, C, Cs, row2col_4_in_agaa₄(R, ._2₂(C, Cs), Cols1, Accm))
row2col_4_in_agaa₄(._2₂(X, Xs), ._2₂(._2₂(X, Ys), Cols), ._2₂(Ys, Cols1), ._2₂([]_0, As)) -> if_row2col_4_in_1_agaa₇(X, Xs, Ys, Cols, Cols1, As, row2col_4_in_aaaa₄(Xs, Cols, Cols1, As))
row2col_4_in_aaaa₄(._2₂(X, Xs), ._2₂(._2₂(X, Ys), Cols), ._2₂(Ys, Cols1), ._2₂([]_0, As)) -> if_row2col_4_in_1_aaaa₇(X, Xs, Ys, Cols, Cols1, As, row2col_4_in_aaaa₄(Xs, Cols, Cols1, As))
row2col_4_in_aaaa₄([]_0, []_0, []_0, []_0) -> row2col_4_out_aaaa₄([]_0, []_0, []_0, []_0)
if_row2col_4_in_1_aaaa₇(X, Xs, Ys, Cols, Cols1, As, row2col_4_out_aaaa₄(Xs, Cols, Cols1, As)) -> row2col_4_out_aaaa₄(._2₂(X, Xs), ._2₂(._2₂(X, Ys), Cols), ._2₂(Ys, Cols1), ._2₂([]_0, As))
if_row2col_4_in_1_agaa₇(X, Xs, Ys, Cols, Cols1, As, row2col_4_out_aaaa₄(Xs, Cols, Cols1, As)) -> row2col_4_out_agaa₄(._2₂(X, Xs), ._2₂(._2₂(X, Ys), Cols), ._2₂(Ys, Cols1), ._2₂([]_0, As))
row2col_4_in_agaa₄([]_0, []_0, []_0, []_0) -> row2col_4_out_agaa₄([]_0, []_0, []_0, []_0)
if_transpose_aux_3_in_1_gga₆(R, Rs, underscore, C, Cs, row2col_4_out_agaa₄(R, ._2₂(C, Cs), Cols1, Accm)) -> if_transpose_aux_3_in_2_gga₈(R, Rs, underscore, C, Cs, Cols1, Accm, transpose_aux_3_in_agg₃(Rs, Accm, Cols1))
transpose_aux_3_in_agg₃(._2₂(R, Rs), underscore, ._2₂(C, Cs)) -> if_transpose_aux_3_in_1_agg₆(R, Rs, underscore, C, Cs, row2col_4_in_agaa₄(R, ._2₂(C, Cs), Cols1, Accm))
if_transpose_aux_3_in_1_agg₆(R, Rs, underscore, C, Cs, row2col_4_out_agaa₄(R, ._2₂(C, Cs), Cols1, Accm)) -> if_transpose_aux_3_in_2_agg₈(R, Rs, underscore, C, Cs, Cols1, Accm, transpose_aux_3_in_agg₃(Rs, Accm, Cols1))
transpose_aux_3_in_agg₃([]_0, X, X) -> transpose_aux_3_out_agg₃([]_0, X, X)
if_transpose_aux_3_in_2_agg₈(R, Rs, underscore, C, Cs, Cols1, Accm, transpose_aux_3_out_agg₃(Rs, Accm, Cols1)) -> transpose_aux_3_out_agg₃(._2₂(R, Rs), underscore, ._2₂(C, Cs))
if_transpose_aux_3_in_2_gga₈(R, Rs, underscore, C, Cs, Cols1, Accm, transpose_aux_3_out_agg₃(Rs, Accm, Cols1)) -> transpose_aux_3_out_gga₃(._2₂(R, Rs), underscore, ._2₂(C, Cs))
transpose_aux_3_in_gga₃([]_0, X, X) -> transpose_aux_3_out_gga₃([]_0, X, X)
if_transpose_2_in_1_ga₃(A, B, transpose_aux_3_out_gga₃(A, []_0, B)) -> transpose_2_out_ga₂(A, B)

TRANSPOSE_2_IN_GA₂(A, B) -> IF_TRANSPOSE_2_IN_1_GA₃(A, B, transpose_aux_3_in_gga₃(A, []_0, B))
TRANSPOSE_2_IN_GA₂(A, B) -> TRANSPOSE_AUX_3_IN_GGA₃(A, []_0, B)
TRANSPOSE_AUX_3_IN_GGA₃(._2₂(R, Rs), underscore, ._2₂(C, Cs)) -> IF_TRANSPOSE_AUX_3_IN_1_GGA₆(R, Rs, underscore, C, Cs, row2col_4_in_agaa₄(R, ._2₂(C, Cs), Cols1, Accm))
TRANSPOSE_AUX_3_IN_GGA₃(._2₂(R, Rs), underscore, ._2₂(C, Cs)) -> ROW2COL_4_IN_AGAA₄(R, ._2₂(C, Cs), Cols1, Accm)
ROW2COL_4_IN_AGAA₄(._2₂(X, Xs), ._2₂(._2₂(X, Ys), Cols), ._2₂(Ys, Cols1), ._2₂([]_0, As)) -> IF_ROW2COL_4_IN_1_AGAA₇(X, Xs, Ys, Cols, Cols1, As, row2col_4_in_aaaa₄(Xs, Cols, Cols1, As))
ROW2COL_4_IN_AGAA₄(._2₂(X, Xs), ._2₂(._2₂(X, Ys), Cols), ._2₂(Ys, Cols1), ._2₂([]_0, As)) -> ROW2COL_4_IN_AAAA₄(Xs, Cols, Cols1, As)
ROW2COL_4_IN_AAAA₄(._2₂(X, Xs), ._2₂(._2₂(X, Ys), Cols), ._2₂(Ys, Cols1), ._2₂([]_0, As)) -> IF_ROW2COL_4_IN_1_AAAA₇(X, Xs, Ys, Cols, Cols1, As, row2col_4_in_aaaa₄(Xs, Cols, Cols1, As))
ROW2COL_4_IN_AAAA₄(._2₂(X, Xs), ._2₂(._2₂(X, Ys), Cols), ._2₂(Ys, Cols1), ._2₂([]_0, As)) -> ROW2COL_4_IN_AAAA₄(Xs, Cols, Cols1, As)
IF_TRANSPOSE_AUX_3_IN_1_GGA₆(R, Rs, underscore, C, Cs, row2col_4_out_agaa₄(R, ._2₂(C, Cs), Cols1, Accm)) -> IF_TRANSPOSE_AUX_3_IN_2_GGA₈(R, Rs, underscore, C, Cs, Cols1, Accm, transpose_aux_3_in_agg₃(Rs, Accm, Cols1))
IF_TRANSPOSE_AUX_3_IN_1_GGA₆(R, Rs, underscore, C, Cs, row2col_4_out_agaa₄(R, ._2₂(C, Cs), Cols1, Accm)) -> TRANSPOSE_AUX_3_IN_AGG₃(Rs, Accm, Cols1)
TRANSPOSE_AUX_3_IN_AGG₃(._2₂(R, Rs), underscore, ._2₂(C, Cs)) -> IF_TRANSPOSE_AUX_3_IN_1_AGG₆(R, Rs, underscore, C, Cs, row2col_4_in_agaa₄(R, ._2₂(C, Cs), Cols1, Accm))
TRANSPOSE_AUX_3_IN_AGG₃(._2₂(R, Rs), underscore, ._2₂(C, Cs)) -> ROW2COL_4_IN_AGAA₄(R, ._2₂(C, Cs), Cols1, Accm)
IF_TRANSPOSE_AUX_3_IN_1_AGG₆(R, Rs, underscore, C, Cs, row2col_4_out_agaa₄(R, ._2₂(C, Cs), Cols1, Accm)) -> IF_TRANSPOSE_AUX_3_IN_2_AGG₈(R, Rs, underscore, C, Cs, Cols1, Accm, transpose_aux_3_in_agg₃(Rs, Accm, Cols1))
IF_TRANSPOSE_AUX_3_IN_1_AGG₆(R, Rs, underscore, C, Cs, row2col_4_out_agaa₄(R, ._2₂(C, Cs), Cols1, Accm)) -> TRANSPOSE_AUX_3_IN_AGG₃(Rs, Accm, Cols1)

The TRS R consists of the following rules:

transpose_2_in_ga₂(A, B) -> if_transpose_2_in_1_ga₃(A, B, transpose_aux_3_in_gga₃(A, []_0, B))
transpose_aux_3_in_gga₃(._2₂(R, Rs), underscore, ._2₂(C, Cs)) -> if_transpose_aux_3_in_1_gga₆(R, Rs, underscore, C, Cs, row2col_4_in_agaa₄(R, ._2₂(C, Cs), Cols1, Accm))
row2col_4_in_agaa₄(._2₂(X, Xs), ._2₂(._2₂(X, Ys), Cols), ._2₂(Ys, Cols1), ._2₂([]_0, As)) -> if_row2col_4_in_1_agaa₇(X, Xs, Ys, Cols, Cols1, As, row2col_4_in_aaaa₄(Xs, Cols, Cols1, As))
row2col_4_in_aaaa₄(._2₂(X, Xs), ._2₂(._2₂(X, Ys), Cols), ._2₂(Ys, Cols1), ._2₂([]_0, As)) -> if_row2col_4_in_1_aaaa₇(X, Xs, Ys, Cols, Cols1, As, row2col_4_in_aaaa₄(Xs, Cols, Cols1, As))
row2col_4_in_aaaa₄([]_0, []_0, []_0, []_0) -> row2col_4_out_aaaa₄([]_0, []_0, []_0, []_0)
if_row2col_4_in_1_aaaa₇(X, Xs, Ys, Cols, Cols1, As, row2col_4_out_aaaa₄(Xs, Cols, Cols1, As)) -> row2col_4_out_aaaa₄(._2₂(X, Xs), ._2₂(._2₂(X, Ys), Cols), ._2₂(Ys, Cols1), ._2₂([]_0, As))
if_row2col_4_in_1_agaa₇(X, Xs, Ys, Cols, Cols1, As, row2col_4_out_aaaa₄(Xs, Cols, Cols1, As)) -> row2col_4_out_agaa₄(._2₂(X, Xs), ._2₂(._2₂(X, Ys), Cols), ._2₂(Ys, Cols1), ._2₂([]_0, As))
row2col_4_in_agaa₄([]_0, []_0, []_0, []_0) -> row2col_4_out_agaa₄([]_0, []_0, []_0, []_0)
if_transpose_aux_3_in_1_gga₆(R, Rs, underscore, C, Cs, row2col_4_out_agaa₄(R, ._2₂(C, Cs), Cols1, Accm)) -> if_transpose_aux_3_in_2_gga₈(R, Rs, underscore, C, Cs, Cols1, Accm, transpose_aux_3_in_agg₃(Rs, Accm, Cols1))
transpose_aux_3_in_agg₃(._2₂(R, Rs), underscore, ._2₂(C, Cs)) -> if_transpose_aux_3_in_1_agg₆(R, Rs, underscore, C, Cs, row2col_4_in_agaa₄(R, ._2₂(C, Cs), Cols1, Accm))
if_transpose_aux_3_in_1_agg₆(R, Rs, underscore, C, Cs, row2col_4_out_agaa₄(R, ._2₂(C, Cs), Cols1, Accm)) -> if_transpose_aux_3_in_2_agg₈(R, Rs, underscore, C, Cs, Cols1, Accm, transpose_aux_3_in_agg₃(Rs, Accm, Cols1))
transpose_aux_3_in_agg₃([]_0, X, X) -> transpose_aux_3_out_agg₃([]_0, X, X)
if_transpose_aux_3_in_2_agg₈(R, Rs, underscore, C, Cs, Cols1, Accm, transpose_aux_3_out_agg₃(Rs, Accm, Cols1)) -> transpose_aux_3_out_agg₃(._2₂(R, Rs), underscore, ._2₂(C, Cs))
if_transpose_aux_3_in_2_gga₈(R, Rs, underscore, C, Cs, Cols1, Accm, transpose_aux_3_out_agg₃(Rs, Accm, Cols1)) -> transpose_aux_3_out_gga₃(._2₂(R, Rs), underscore, ._2₂(C, Cs))
transpose_aux_3_in_gga₃([]_0, X, X) -> transpose_aux_3_out_gga₃([]_0, X, X)
if_transpose_2_in_1_ga₃(A, B, transpose_aux_3_out_gga₃(A, []_0, B)) -> transpose_2_out_ga₂(A, B)

The argument filtering Pi contains the following mapping:
transpose_2_in_ga₂(x1, x2) = transpose_2_in_ga₁(x1)
[]_0 = []_0
._2₂(x1, x2) = ._2
if_transpose_2_in_1_ga₃(x1, x2, x3) = if_transpose_2_in_1_ga₂(x1, x3)
transpose_aux_3_in_gga₃(x1, x2, x3) = transpose_aux_3_in_gga₂(x1, x2)
if_transpose_aux_3_in_1_gga₆(x1, x2, x3, x4, x5, x6) = if_transpose_aux_3_in_1_gga₂(x3, x6)
row2col_4_in_agaa₄(x1, x2, x3, x4) = row2col_4_in_agaa₁(x2)
if_row2col_4_in_1_agaa₇(x1, x2, x3, x4, x5, x6, x7) = if_row2col_4_in_1_agaa₁(x7)
row2col_4_in_aaaa₄(x1, x2, x3, x4) = row2col_4_in_aaaa
if_row2col_4_in_1_aaaa₇(x1, x2, x3, x4, x5, x6, x7) = if_row2col_4_in_1_aaaa₁(x7)
row2col_4_out_aaaa₄(x1, x2, x3, x4) = row2col_4_out_aaaa₄(x1, x2, x3, x4)
row2col_4_out_agaa₄(x1, x2, x3, x4) = row2col_4_out_agaa₄(x1, x2, x3, x4)
if_transpose_aux_3_in_2_gga₈(x1, x2, x3, x4, x5, x6, x7, x8) = if_transpose_aux_3_in_2_gga₂(x3, x8)
transpose_aux_3_in_agg₃(x1, x2, x3) = transpose_aux_3_in_agg₂(x2, x3)
if_transpose_aux_3_in_1_agg₆(x1, x2, x3, x4, x5, x6) = if_transpose_aux_3_in_1_agg₂(x3, x6)
if_transpose_aux_3_in_2_agg₈(x1, x2, x3, x4, x5, x6, x7, x8) = if_transpose_aux_3_in_2_agg₂(x3, x8)
transpose_aux_3_out_agg₃(x1, x2, x3) = transpose_aux_3_out_agg₃(x1, x2, x3)
transpose_aux_3_out_gga₃(x1, x2, x3) = transpose_aux_3_out_gga₃(x1, x2, x3)
transpose_2_out_ga₂(x1, x2) = transpose_2_out_ga₂(x1, x2)
IF_TRANSPOSE_AUX_3_IN_1_GGA₆(x1, x2, x3, x4, x5, x6) = IF_TRANSPOSE_AUX_3_IN_1_GGA₂(x3, x6)
IF_TRANSPOSE_AUX_3_IN_2_AGG₈(x1, x2, x3, x4, x5, x6, x7, x8) = IF_TRANSPOSE_AUX_3_IN_2_AGG₂(x3, x8)
IF_TRANSPOSE_AUX_3_IN_1_AGG₆(x1, x2, x3, x4, x5, x6) = IF_TRANSPOSE_AUX_3_IN_1_AGG₂(x3, x6)
IF_ROW2COL_4_IN_1_AAAA₇(x1, x2, x3, x4, x5, x6, x7) = IF_ROW2COL_4_IN_1_AAAA₁(x7)
TRANSPOSE_2_IN_GA₂(x1, x2) = TRANSPOSE_2_IN_GA₁(x1)
TRANSPOSE_AUX_3_IN_GGA₃(x1, x2, x3) = TRANSPOSE_AUX_3_IN_GGA₂(x1, x2)
IF_TRANSPOSE_2_IN_1_GA₃(x1, x2, x3) = IF_TRANSPOSE_2_IN_1_GA₂(x1, x3)
TRANSPOSE_AUX_3_IN_AGG₃(x1, x2, x3) = TRANSPOSE_AUX_3_IN_AGG₂(x2, x3)
ROW2COL_4_IN_AGAA₄(x1, x2, x3, x4) = ROW2COL_4_IN_AGAA₁(x2)
IF_ROW2COL_4_IN_1_AGAA₇(x1, x2, x3, x4, x5, x6, x7) = IF_ROW2COL_4_IN_1_AGAA₁(x7)
ROW2COL_4_IN_AAAA₄(x1, x2, x3, x4) = ROW2COL_4_IN_AAAA
IF_TRANSPOSE_AUX_3_IN_2_GGA₈(x1, x2, x3, x4, x5, x6, x7, x8) = IF_TRANSPOSE_AUX_3_IN_2_GGA₂(x3, x8)

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

↳ PROLOG

  ↳ PrologToPiTRSProof

  ↳ PrologToPiTRSProof

    ↳ PiTRS

      ↳ DependencyPairsProof

        ↳ PiDP

          ↳ DependencyGraphProof

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

TRANSPOSE_2_IN_GA₂(A, B) -> IF_TRANSPOSE_2_IN_1_GA₃(A, B, transpose_aux_3_in_gga₃(A, []_0, B))
TRANSPOSE_2_IN_GA₂(A, B) -> TRANSPOSE_AUX_3_IN_GGA₃(A, []_0, B)
TRANSPOSE_AUX_3_IN_GGA₃(._2₂(R, Rs), underscore, ._2₂(C, Cs)) -> IF_TRANSPOSE_AUX_3_IN_1_GGA₆(R, Rs, underscore, C, Cs, row2col_4_in_agaa₄(R, ._2₂(C, Cs), Cols1, Accm))
TRANSPOSE_AUX_3_IN_GGA₃(._2₂(R, Rs), underscore, ._2₂(C, Cs)) -> ROW2COL_4_IN_AGAA₄(R, ._2₂(C, Cs), Cols1, Accm)
ROW2COL_4_IN_AGAA₄(._2₂(X, Xs), ._2₂(._2₂(X, Ys), Cols), ._2₂(Ys, Cols1), ._2₂([]_0, As)) -> IF_ROW2COL_4_IN_1_AGAA₇(X, Xs, Ys, Cols, Cols1, As, row2col_4_in_aaaa₄(Xs, Cols, Cols1, As))
ROW2COL_4_IN_AGAA₄(._2₂(X, Xs), ._2₂(._2₂(X, Ys), Cols), ._2₂(Ys, Cols1), ._2₂([]_0, As)) -> ROW2COL_4_IN_AAAA₄(Xs, Cols, Cols1, As)
ROW2COL_4_IN_AAAA₄(._2₂(X, Xs), ._2₂(._2₂(X, Ys), Cols), ._2₂(Ys, Cols1), ._2₂([]_0, As)) -> IF_ROW2COL_4_IN_1_AAAA₇(X, Xs, Ys, Cols, Cols1, As, row2col_4_in_aaaa₄(Xs, Cols, Cols1, As))
ROW2COL_4_IN_AAAA₄(._2₂(X, Xs), ._2₂(._2₂(X, Ys), Cols), ._2₂(Ys, Cols1), ._2₂([]_0, As)) -> ROW2COL_4_IN_AAAA₄(Xs, Cols, Cols1, As)
IF_TRANSPOSE_AUX_3_IN_1_GGA₆(R, Rs, underscore, C, Cs, row2col_4_out_agaa₄(R, ._2₂(C, Cs), Cols1, Accm)) -> IF_TRANSPOSE_AUX_3_IN_2_GGA₈(R, Rs, underscore, C, Cs, Cols1, Accm, transpose_aux_3_in_agg₃(Rs, Accm, Cols1))
IF_TRANSPOSE_AUX_3_IN_1_GGA₆(R, Rs, underscore, C, Cs, row2col_4_out_agaa₄(R, ._2₂(C, Cs), Cols1, Accm)) -> TRANSPOSE_AUX_3_IN_AGG₃(Rs, Accm, Cols1)
TRANSPOSE_AUX_3_IN_AGG₃(._2₂(R, Rs), underscore, ._2₂(C, Cs)) -> IF_TRANSPOSE_AUX_3_IN_1_AGG₆(R, Rs, underscore, C, Cs, row2col_4_in_agaa₄(R, ._2₂(C, Cs), Cols1, Accm))
TRANSPOSE_AUX_3_IN_AGG₃(._2₂(R, Rs), underscore, ._2₂(C, Cs)) -> ROW2COL_4_IN_AGAA₄(R, ._2₂(C, Cs), Cols1, Accm)
IF_TRANSPOSE_AUX_3_IN_1_AGG₆(R, Rs, underscore, C, Cs, row2col_4_out_agaa₄(R, ._2₂(C, Cs), Cols1, Accm)) -> IF_TRANSPOSE_AUX_3_IN_2_AGG₈(R, Rs, underscore, C, Cs, Cols1, Accm, transpose_aux_3_in_agg₃(Rs, Accm, Cols1))
IF_TRANSPOSE_AUX_3_IN_1_AGG₆(R, Rs, underscore, C, Cs, row2col_4_out_agaa₄(R, ._2₂(C, Cs), Cols1, Accm)) -> TRANSPOSE_AUX_3_IN_AGG₃(Rs, Accm, Cols1)

The TRS R consists of the following rules:

transpose_2_in_ga₂(A, B) -> if_transpose_2_in_1_ga₃(A, B, transpose_aux_3_in_gga₃(A, []_0, B))
transpose_aux_3_in_gga₃(._2₂(R, Rs), underscore, ._2₂(C, Cs)) -> if_transpose_aux_3_in_1_gga₆(R, Rs, underscore, C, Cs, row2col_4_in_agaa₄(R, ._2₂(C, Cs), Cols1, Accm))
row2col_4_in_agaa₄(._2₂(X, Xs), ._2₂(._2₂(X, Ys), Cols), ._2₂(Ys, Cols1), ._2₂([]_0, As)) -> if_row2col_4_in_1_agaa₇(X, Xs, Ys, Cols, Cols1, As, row2col_4_in_aaaa₄(Xs, Cols, Cols1, As))
row2col_4_in_aaaa₄(._2₂(X, Xs), ._2₂(._2₂(X, Ys), Cols), ._2₂(Ys, Cols1), ._2₂([]_0, As)) -> if_row2col_4_in_1_aaaa₇(X, Xs, Ys, Cols, Cols1, As, row2col_4_in_aaaa₄(Xs, Cols, Cols1, As))
row2col_4_in_aaaa₄([]_0, []_0, []_0, []_0) -> row2col_4_out_aaaa₄([]_0, []_0, []_0, []_0)
if_row2col_4_in_1_aaaa₇(X, Xs, Ys, Cols, Cols1, As, row2col_4_out_aaaa₄(Xs, Cols, Cols1, As)) -> row2col_4_out_aaaa₄(._2₂(X, Xs), ._2₂(._2₂(X, Ys), Cols), ._2₂(Ys, Cols1), ._2₂([]_0, As))
if_row2col_4_in_1_agaa₇(X, Xs, Ys, Cols, Cols1, As, row2col_4_out_aaaa₄(Xs, Cols, Cols1, As)) -> row2col_4_out_agaa₄(._2₂(X, Xs), ._2₂(._2₂(X, Ys), Cols), ._2₂(Ys, Cols1), ._2₂([]_0, As))
row2col_4_in_agaa₄([]_0, []_0, []_0, []_0) -> row2col_4_out_agaa₄([]_0, []_0, []_0, []_0)
if_transpose_aux_3_in_1_gga₆(R, Rs, underscore, C, Cs, row2col_4_out_agaa₄(R, ._2₂(C, Cs), Cols1, Accm)) -> if_transpose_aux_3_in_2_gga₈(R, Rs, underscore, C, Cs, Cols1, Accm, transpose_aux_3_in_agg₃(Rs, Accm, Cols1))
transpose_aux_3_in_agg₃(._2₂(R, Rs), underscore, ._2₂(C, Cs)) -> if_transpose_aux_3_in_1_agg₆(R, Rs, underscore, C, Cs, row2col_4_in_agaa₄(R, ._2₂(C, Cs), Cols1, Accm))
if_transpose_aux_3_in_1_agg₆(R, Rs, underscore, C, Cs, row2col_4_out_agaa₄(R, ._2₂(C, Cs), Cols1, Accm)) -> if_transpose_aux_3_in_2_agg₈(R, Rs, underscore, C, Cs, Cols1, Accm, transpose_aux_3_in_agg₃(Rs, Accm, Cols1))
transpose_aux_3_in_agg₃([]_0, X, X) -> transpose_aux_3_out_agg₃([]_0, X, X)
if_transpose_aux_3_in_2_agg₈(R, Rs, underscore, C, Cs, Cols1, Accm, transpose_aux_3_out_agg₃(Rs, Accm, Cols1)) -> transpose_aux_3_out_agg₃(._2₂(R, Rs), underscore, ._2₂(C, Cs))
if_transpose_aux_3_in_2_gga₈(R, Rs, underscore, C, Cs, Cols1, Accm, transpose_aux_3_out_agg₃(Rs, Accm, Cols1)) -> transpose_aux_3_out_gga₃(._2₂(R, Rs), underscore, ._2₂(C, Cs))
transpose_aux_3_in_gga₃([]_0, X, X) -> transpose_aux_3_out_gga₃([]_0, X, X)
if_transpose_2_in_1_ga₃(A, B, transpose_aux_3_out_gga₃(A, []_0, B)) -> transpose_2_out_ga₂(A, B)

The argument filtering Pi contains the following mapping:
transpose_2_in_ga₂(x1, x2) = transpose_2_in_ga₁(x1)
[]_0 = []_0
._2₂(x1, x2) = ._2
if_transpose_2_in_1_ga₃(x1, x2, x3) = if_transpose_2_in_1_ga₂(x1, x3)
transpose_aux_3_in_gga₃(x1, x2, x3) = transpose_aux_3_in_gga₂(x1, x2)
if_transpose_aux_3_in_1_gga₆(x1, x2, x3, x4, x5, x6) = if_transpose_aux_3_in_1_gga₂(x3, x6)
row2col_4_in_agaa₄(x1, x2, x3, x4) = row2col_4_in_agaa₁(x2)
if_row2col_4_in_1_agaa₇(x1, x2, x3, x4, x5, x6, x7) = if_row2col_4_in_1_agaa₁(x7)
row2col_4_in_aaaa₄(x1, x2, x3, x4) = row2col_4_in_aaaa
if_row2col_4_in_1_aaaa₇(x1, x2, x3, x4, x5, x6, x7) = if_row2col_4_in_1_aaaa₁(x7)
row2col_4_out_aaaa₄(x1, x2, x3, x4) = row2col_4_out_aaaa₄(x1, x2, x3, x4)
row2col_4_out_agaa₄(x1, x2, x3, x4) = row2col_4_out_agaa₄(x1, x2, x3, x4)
if_transpose_aux_3_in_2_gga₈(x1, x2, x3, x4, x5, x6, x7, x8) = if_transpose_aux_3_in_2_gga₂(x3, x8)
transpose_aux_3_in_agg₃(x1, x2, x3) = transpose_aux_3_in_agg₂(x2, x3)
if_transpose_aux_3_in_1_agg₆(x1, x2, x3, x4, x5, x6) = if_transpose_aux_3_in_1_agg₂(x3, x6)
if_transpose_aux_3_in_2_agg₈(x1, x2, x3, x4, x5, x6, x7, x8) = if_transpose_aux_3_in_2_agg₂(x3, x8)
transpose_aux_3_out_agg₃(x1, x2, x3) = transpose_aux_3_out_agg₃(x1, x2, x3)
transpose_aux_3_out_gga₃(x1, x2, x3) = transpose_aux_3_out_gga₃(x1, x2, x3)
transpose_2_out_ga₂(x1, x2) = transpose_2_out_ga₂(x1, x2)
IF_TRANSPOSE_AUX_3_IN_1_GGA₆(x1, x2, x3, x4, x5, x6) = IF_TRANSPOSE_AUX_3_IN_1_GGA₂(x3, x6)
IF_TRANSPOSE_AUX_3_IN_2_AGG₈(x1, x2, x3, x4, x5, x6, x7, x8) = IF_TRANSPOSE_AUX_3_IN_2_AGG₂(x3, x8)
IF_TRANSPOSE_AUX_3_IN_1_AGG₆(x1, x2, x3, x4, x5, x6) = IF_TRANSPOSE_AUX_3_IN_1_AGG₂(x3, x6)
IF_ROW2COL_4_IN_1_AAAA₇(x1, x2, x3, x4, x5, x6, x7) = IF_ROW2COL_4_IN_1_AAAA₁(x7)
TRANSPOSE_2_IN_GA₂(x1, x2) = TRANSPOSE_2_IN_GA₁(x1)
TRANSPOSE_AUX_3_IN_GGA₃(x1, x2, x3) = TRANSPOSE_AUX_3_IN_GGA₂(x1, x2)
IF_TRANSPOSE_2_IN_1_GA₃(x1, x2, x3) = IF_TRANSPOSE_2_IN_1_GA₂(x1, x3)
TRANSPOSE_AUX_3_IN_AGG₃(x1, x2, x3) = TRANSPOSE_AUX_3_IN_AGG₂(x2, x3)
ROW2COL_4_IN_AGAA₄(x1, x2, x3, x4) = ROW2COL_4_IN_AGAA₁(x2)
IF_ROW2COL_4_IN_1_AGAA₇(x1, x2, x3, x4, x5, x6, x7) = IF_ROW2COL_4_IN_1_AGAA₁(x7)
ROW2COL_4_IN_AAAA₄(x1, x2, x3, x4) = ROW2COL_4_IN_AAAA
IF_TRANSPOSE_AUX_3_IN_2_GGA₈(x1, x2, x3, x4, x5, x6, x7, x8) = IF_TRANSPOSE_AUX_3_IN_2_GGA₂(x3, 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

  ↳ PrologToPiTRSProof

    ↳ PiTRS

      ↳ DependencyPairsProof

        ↳ PiDP

          ↳ DependencyGraphProof

            ↳ AND

              ↳ PiDP

                ↳ UsableRulesProof

              ↳ PiDP

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

ROW2COL_4_IN_AAAA₄(._2₂(X, Xs), ._2₂(._2₂(X, Ys), Cols), ._2₂(Ys, Cols1), ._2₂([]_0, As)) -> ROW2COL_4_IN_AAAA₄(Xs, Cols, Cols1, As)

The TRS R consists of the following rules:

transpose_2_in_ga₂(A, B) -> if_transpose_2_in_1_ga₃(A, B, transpose_aux_3_in_gga₃(A, []_0, B))
transpose_aux_3_in_gga₃(._2₂(R, Rs), underscore, ._2₂(C, Cs)) -> if_transpose_aux_3_in_1_gga₆(R, Rs, underscore, C, Cs, row2col_4_in_agaa₄(R, ._2₂(C, Cs), Cols1, Accm))
row2col_4_in_agaa₄(._2₂(X, Xs), ._2₂(._2₂(X, Ys), Cols), ._2₂(Ys, Cols1), ._2₂([]_0, As)) -> if_row2col_4_in_1_agaa₇(X, Xs, Ys, Cols, Cols1, As, row2col_4_in_aaaa₄(Xs, Cols, Cols1, As))
row2col_4_in_aaaa₄(._2₂(X, Xs), ._2₂(._2₂(X, Ys), Cols), ._2₂(Ys, Cols1), ._2₂([]_0, As)) -> if_row2col_4_in_1_aaaa₇(X, Xs, Ys, Cols, Cols1, As, row2col_4_in_aaaa₄(Xs, Cols, Cols1, As))
row2col_4_in_aaaa₄([]_0, []_0, []_0, []_0) -> row2col_4_out_aaaa₄([]_0, []_0, []_0, []_0)
if_row2col_4_in_1_aaaa₇(X, Xs, Ys, Cols, Cols1, As, row2col_4_out_aaaa₄(Xs, Cols, Cols1, As)) -> row2col_4_out_aaaa₄(._2₂(X, Xs), ._2₂(._2₂(X, Ys), Cols), ._2₂(Ys, Cols1), ._2₂([]_0, As))
if_row2col_4_in_1_agaa₇(X, Xs, Ys, Cols, Cols1, As, row2col_4_out_aaaa₄(Xs, Cols, Cols1, As)) -> row2col_4_out_agaa₄(._2₂(X, Xs), ._2₂(._2₂(X, Ys), Cols), ._2₂(Ys, Cols1), ._2₂([]_0, As))
row2col_4_in_agaa₄([]_0, []_0, []_0, []_0) -> row2col_4_out_agaa₄([]_0, []_0, []_0, []_0)
if_transpose_aux_3_in_1_gga₆(R, Rs, underscore, C, Cs, row2col_4_out_agaa₄(R, ._2₂(C, Cs), Cols1, Accm)) -> if_transpose_aux_3_in_2_gga₈(R, Rs, underscore, C, Cs, Cols1, Accm, transpose_aux_3_in_agg₃(Rs, Accm, Cols1))
transpose_aux_3_in_agg₃(._2₂(R, Rs), underscore, ._2₂(C, Cs)) -> if_transpose_aux_3_in_1_agg₆(R, Rs, underscore, C, Cs, row2col_4_in_agaa₄(R, ._2₂(C, Cs), Cols1, Accm))
if_transpose_aux_3_in_1_agg₆(R, Rs, underscore, C, Cs, row2col_4_out_agaa₄(R, ._2₂(C, Cs), Cols1, Accm)) -> if_transpose_aux_3_in_2_agg₈(R, Rs, underscore, C, Cs, Cols1, Accm, transpose_aux_3_in_agg₃(Rs, Accm, Cols1))
transpose_aux_3_in_agg₃([]_0, X, X) -> transpose_aux_3_out_agg₃([]_0, X, X)
if_transpose_aux_3_in_2_agg₈(R, Rs, underscore, C, Cs, Cols1, Accm, transpose_aux_3_out_agg₃(Rs, Accm, Cols1)) -> transpose_aux_3_out_agg₃(._2₂(R, Rs), underscore, ._2₂(C, Cs))
if_transpose_aux_3_in_2_gga₈(R, Rs, underscore, C, Cs, Cols1, Accm, transpose_aux_3_out_agg₃(Rs, Accm, Cols1)) -> transpose_aux_3_out_gga₃(._2₂(R, Rs), underscore, ._2₂(C, Cs))
transpose_aux_3_in_gga₃([]_0, X, X) -> transpose_aux_3_out_gga₃([]_0, X, X)
if_transpose_2_in_1_ga₃(A, B, transpose_aux_3_out_gga₃(A, []_0, B)) -> transpose_2_out_ga₂(A, B)

↳ PROLOG

  ↳ PrologToPiTRSProof

  ↳ PrologToPiTRSProof

    ↳ PiTRS

      ↳ DependencyPairsProof

        ↳ PiDP

          ↳ DependencyGraphProof

            ↳ AND

              ↳ PiDP

                ↳ UsableRulesProof

                  ↳ PiDP

                    ↳ PiDPToQDPProof

              ↳ PiDP

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

ROW2COL_4_IN_AAAA₄(._2₂(X, Xs), ._2₂(._2₂(X, Ys), Cols), ._2₂(Ys, Cols1), ._2₂([]_0, As)) -> ROW2COL_4_IN_AAAA₄(Xs, Cols, Cols1, As)

↳ PROLOG

  ↳ PrologToPiTRSProof

  ↳ PrologToPiTRSProof

    ↳ PiTRS

      ↳ DependencyPairsProof

        ↳ PiDP

          ↳ DependencyGraphProof

            ↳ AND

              ↳ PiDP

                ↳ UsableRulesProof

                  ↳ PiDP

                    ↳ PiDPToQDPProof

                      ↳ QDP

              ↳ PiDP

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

ROW2COL_4_IN_AAAA -> ROW2COL_4_IN_AAAA

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

↳ PROLOG

  ↳ PrologToPiTRSProof

  ↳ PrologToPiTRSProof

    ↳ PiTRS

      ↳ DependencyPairsProof

        ↳ PiDP

          ↳ DependencyGraphProof

            ↳ AND

              ↳ PiDP

              ↳ PiDP

                ↳ UsableRulesProof

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

IF_TRANSPOSE_AUX_3_IN_1_AGG₆(R, Rs, underscore, C, Cs, row2col_4_out_agaa₄(R, ._2₂(C, Cs), Cols1, Accm)) -> TRANSPOSE_AUX_3_IN_AGG₃(Rs, Accm, Cols1)
TRANSPOSE_AUX_3_IN_AGG₃(._2₂(R, Rs), underscore, ._2₂(C, Cs)) -> IF_TRANSPOSE_AUX_3_IN_1_AGG₆(R, Rs, underscore, C, Cs, row2col_4_in_agaa₄(R, ._2₂(C, Cs), Cols1, Accm))

The TRS R consists of the following rules:

transpose_2_in_ga₂(A, B) -> if_transpose_2_in_1_ga₃(A, B, transpose_aux_3_in_gga₃(A, []_0, B))
transpose_aux_3_in_gga₃(._2₂(R, Rs), underscore, ._2₂(C, Cs)) -> if_transpose_aux_3_in_1_gga₆(R, Rs, underscore, C, Cs, row2col_4_in_agaa₄(R, ._2₂(C, Cs), Cols1, Accm))
row2col_4_in_agaa₄(._2₂(X, Xs), ._2₂(._2₂(X, Ys), Cols), ._2₂(Ys, Cols1), ._2₂([]_0, As)) -> if_row2col_4_in_1_agaa₇(X, Xs, Ys, Cols, Cols1, As, row2col_4_in_aaaa₄(Xs, Cols, Cols1, As))
row2col_4_in_aaaa₄(._2₂(X, Xs), ._2₂(._2₂(X, Ys), Cols), ._2₂(Ys, Cols1), ._2₂([]_0, As)) -> if_row2col_4_in_1_aaaa₇(X, Xs, Ys, Cols, Cols1, As, row2col_4_in_aaaa₄(Xs, Cols, Cols1, As))
row2col_4_in_aaaa₄([]_0, []_0, []_0, []_0) -> row2col_4_out_aaaa₄([]_0, []_0, []_0, []_0)
if_row2col_4_in_1_aaaa₇(X, Xs, Ys, Cols, Cols1, As, row2col_4_out_aaaa₄(Xs, Cols, Cols1, As)) -> row2col_4_out_aaaa₄(._2₂(X, Xs), ._2₂(._2₂(X, Ys), Cols), ._2₂(Ys, Cols1), ._2₂([]_0, As))
if_row2col_4_in_1_agaa₇(X, Xs, Ys, Cols, Cols1, As, row2col_4_out_aaaa₄(Xs, Cols, Cols1, As)) -> row2col_4_out_agaa₄(._2₂(X, Xs), ._2₂(._2₂(X, Ys), Cols), ._2₂(Ys, Cols1), ._2₂([]_0, As))
row2col_4_in_agaa₄([]_0, []_0, []_0, []_0) -> row2col_4_out_agaa₄([]_0, []_0, []_0, []_0)
if_transpose_aux_3_in_1_gga₆(R, Rs, underscore, C, Cs, row2col_4_out_agaa₄(R, ._2₂(C, Cs), Cols1, Accm)) -> if_transpose_aux_3_in_2_gga₈(R, Rs, underscore, C, Cs, Cols1, Accm, transpose_aux_3_in_agg₃(Rs, Accm, Cols1))
transpose_aux_3_in_agg₃(._2₂(R, Rs), underscore, ._2₂(C, Cs)) -> if_transpose_aux_3_in_1_agg₆(R, Rs, underscore, C, Cs, row2col_4_in_agaa₄(R, ._2₂(C, Cs), Cols1, Accm))
if_transpose_aux_3_in_1_agg₆(R, Rs, underscore, C, Cs, row2col_4_out_agaa₄(R, ._2₂(C, Cs), Cols1, Accm)) -> if_transpose_aux_3_in_2_agg₈(R, Rs, underscore, C, Cs, Cols1, Accm, transpose_aux_3_in_agg₃(Rs, Accm, Cols1))
transpose_aux_3_in_agg₃([]_0, X, X) -> transpose_aux_3_out_agg₃([]_0, X, X)
if_transpose_aux_3_in_2_agg₈(R, Rs, underscore, C, Cs, Cols1, Accm, transpose_aux_3_out_agg₃(Rs, Accm, Cols1)) -> transpose_aux_3_out_agg₃(._2₂(R, Rs), underscore, ._2₂(C, Cs))
if_transpose_aux_3_in_2_gga₈(R, Rs, underscore, C, Cs, Cols1, Accm, transpose_aux_3_out_agg₃(Rs, Accm, Cols1)) -> transpose_aux_3_out_gga₃(._2₂(R, Rs), underscore, ._2₂(C, Cs))
transpose_aux_3_in_gga₃([]_0, X, X) -> transpose_aux_3_out_gga₃([]_0, X, X)
if_transpose_2_in_1_ga₃(A, B, transpose_aux_3_out_gga₃(A, []_0, B)) -> transpose_2_out_ga₂(A, B)

↳ PROLOG

  ↳ PrologToPiTRSProof

  ↳ PrologToPiTRSProof

    ↳ PiTRS

      ↳ DependencyPairsProof

        ↳ PiDP

          ↳ DependencyGraphProof

            ↳ AND

              ↳ PiDP

              ↳ PiDP

                ↳ UsableRulesProof

                  ↳ PiDP

                    ↳ PiDPToQDPProof

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

IF_TRANSPOSE_AUX_3_IN_1_AGG₆(R, Rs, underscore, C, Cs, row2col_4_out_agaa₄(R, ._2₂(C, Cs), Cols1, Accm)) -> TRANSPOSE_AUX_3_IN_AGG₃(Rs, Accm, Cols1)
TRANSPOSE_AUX_3_IN_AGG₃(._2₂(R, Rs), underscore, ._2₂(C, Cs)) -> IF_TRANSPOSE_AUX_3_IN_1_AGG₆(R, Rs, underscore, C, Cs, row2col_4_in_agaa₄(R, ._2₂(C, Cs), Cols1, Accm))

The TRS R consists of the following rules:

row2col_4_in_agaa₄(._2₂(X, Xs), ._2₂(._2₂(X, Ys), Cols), ._2₂(Ys, Cols1), ._2₂([]_0, As)) -> if_row2col_4_in_1_agaa₇(X, Xs, Ys, Cols, Cols1, As, row2col_4_in_aaaa₄(Xs, Cols, Cols1, As))
if_row2col_4_in_1_agaa₇(X, Xs, Ys, Cols, Cols1, As, row2col_4_out_aaaa₄(Xs, Cols, Cols1, As)) -> row2col_4_out_agaa₄(._2₂(X, Xs), ._2₂(._2₂(X, Ys), Cols), ._2₂(Ys, Cols1), ._2₂([]_0, As))
row2col_4_in_aaaa₄(._2₂(X, Xs), ._2₂(._2₂(X, Ys), Cols), ._2₂(Ys, Cols1), ._2₂([]_0, As)) -> if_row2col_4_in_1_aaaa₇(X, Xs, Ys, Cols, Cols1, As, row2col_4_in_aaaa₄(Xs, Cols, Cols1, As))
row2col_4_in_aaaa₄([]_0, []_0, []_0, []_0) -> row2col_4_out_aaaa₄([]_0, []_0, []_0, []_0)
if_row2col_4_in_1_aaaa₇(X, Xs, Ys, Cols, Cols1, As, row2col_4_out_aaaa₄(Xs, Cols, Cols1, As)) -> row2col_4_out_aaaa₄(._2₂(X, Xs), ._2₂(._2₂(X, Ys), Cols), ._2₂(Ys, Cols1), ._2₂([]_0, As))

The argument filtering Pi contains the following mapping:
[]_0 = []_0
._2₂(x1, x2) = ._2
row2col_4_in_agaa₄(x1, x2, x3, x4) = row2col_4_in_agaa₁(x2)
if_row2col_4_in_1_agaa₇(x1, x2, x3, x4, x5, x6, x7) = if_row2col_4_in_1_agaa₁(x7)
row2col_4_in_aaaa₄(x1, x2, x3, x4) = row2col_4_in_aaaa
if_row2col_4_in_1_aaaa₇(x1, x2, x3, x4, x5, x6, x7) = if_row2col_4_in_1_aaaa₁(x7)
row2col_4_out_aaaa₄(x1, x2, x3, x4) = row2col_4_out_aaaa₄(x1, x2, x3, x4)
row2col_4_out_agaa₄(x1, x2, x3, x4) = row2col_4_out_agaa₄(x1, x2, x3, x4)
IF_TRANSPOSE_AUX_3_IN_1_AGG₆(x1, x2, x3, x4, x5, x6) = IF_TRANSPOSE_AUX_3_IN_1_AGG₂(x3, x6)
TRANSPOSE_AUX_3_IN_AGG₃(x1, x2, x3) = TRANSPOSE_AUX_3_IN_AGG₂(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

  ↳ PrologToPiTRSProof

    ↳ PiTRS

      ↳ DependencyPairsProof

        ↳ PiDP

          ↳ DependencyGraphProof

            ↳ AND

              ↳ PiDP

              ↳ PiDP

                ↳ UsableRulesProof

                  ↳ PiDP

                    ↳ PiDPToQDPProof

                      ↳ QDP

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

IF_TRANSPOSE_AUX_3_IN_1_AGG₂(underscore, row2col_4_out_agaa₄(R, ._2, Cols1, Accm)) -> TRANSPOSE_AUX_3_IN_AGG₂(Accm, Cols1)
TRANSPOSE_AUX_3_IN_AGG₂(underscore, ._2) -> IF_TRANSPOSE_AUX_3_IN_1_AGG₂(underscore, row2col_4_in_agaa₁(._2))

The TRS R consists of the following rules:

row2col_4_in_agaa₁(._2) -> if_row2col_4_in_1_agaa₁(row2col_4_in_aaaa)
if_row2col_4_in_1_agaa₁(row2col_4_out_aaaa₄(Xs, Cols, Cols1, As)) -> row2col_4_out_agaa₄(._2, ._2, ._2, ._2)
row2col_4_in_aaaa -> if_row2col_4_in_1_aaaa₁(row2col_4_in_aaaa)
row2col_4_in_aaaa -> row2col_4_out_aaaa₄([]_0, []_0, []_0, []_0)
if_row2col_4_in_1_aaaa₁(row2col_4_out_aaaa₄(Xs, Cols, Cols1, As)) -> row2col_4_out_aaaa₄(._2, ._2, ._2, ._2)

The set Q consists of the following terms:

row2col_4_in_agaa₁(x0)
if_row2col_4_in_1_agaa₁(x0)
row2col_4_in_aaaa
if_row2col_4_in_1_aaaa₁(x0)

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