Left Termination proof of /tmp/tmpzNoHgj/transpose-bb.pl

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

↳ PROLOG

  ↳ 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,b)
transpose_aux₃: (b,b,b)
row2col₄: (b,b,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_gg₂(A, B) -> if_transpose_2_in_1_gg₃(A, B, transpose_aux_3_in_ggg₃(A, []_0, B))
transpose_aux_3_in_ggg₃(._2₂(R, Rs), underscore, ._2₂(C, Cs)) -> if_transpose_aux_3_in_1_ggg₆(R, Rs, underscore, C, Cs, row2col_4_in_ggaa₄(R, ._2₂(C, Cs), Cols1, Accm))
row2col_4_in_ggaa₄(._2₂(X, Xs), ._2₂(._2₂(X, Ys), Cols), ._2₂(Ys, Cols1), ._2₂([]_0, As)) -> if_row2col_4_in_1_ggaa₇(X, Xs, Ys, Cols, Cols1, As, row2col_4_in_ggaa₄(Xs, Cols, Cols1, As))
row2col_4_in_ggaa₄([]_0, []_0, []_0, []_0) -> row2col_4_out_ggaa₄([]_0, []_0, []_0, []_0)
if_row2col_4_in_1_ggaa₇(X, Xs, Ys, Cols, Cols1, As, row2col_4_out_ggaa₄(Xs, Cols, Cols1, As)) -> row2col_4_out_ggaa₄(._2₂(X, Xs), ._2₂(._2₂(X, Ys), Cols), ._2₂(Ys, Cols1), ._2₂([]_0, As))
if_transpose_aux_3_in_1_ggg₆(R, Rs, underscore, C, Cs, row2col_4_out_ggaa₄(R, ._2₂(C, Cs), Cols1, Accm)) -> if_transpose_aux_3_in_2_ggg₈(R, Rs, underscore, C, Cs, Cols1, Accm, transpose_aux_3_in_ggg₃(Rs, Accm, Cols1))
transpose_aux_3_in_ggg₃([]_0, X, X) -> transpose_aux_3_out_ggg₃([]_0, X, X)
if_transpose_aux_3_in_2_ggg₈(R, Rs, underscore, C, Cs, Cols1, Accm, transpose_aux_3_out_ggg₃(Rs, Accm, Cols1)) -> transpose_aux_3_out_ggg₃(._2₂(R, Rs), underscore, ._2₂(C, Cs))
if_transpose_2_in_1_gg₃(A, B, transpose_aux_3_out_ggg₃(A, []_0, B)) -> transpose_2_out_gg₂(A, B)

Infinitary Constructor Rewriting Termination of PiTRS implies Termination of PROLOG

↳ PROLOG

  ↳ PrologToPiTRSProof

    ↳ PiTRS

      ↳ DependencyPairsProof

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

transpose_2_in_gg₂(A, B) -> if_transpose_2_in_1_gg₃(A, B, transpose_aux_3_in_ggg₃(A, []_0, B))
transpose_aux_3_in_ggg₃(._2₂(R, Rs), underscore, ._2₂(C, Cs)) -> if_transpose_aux_3_in_1_ggg₆(R, Rs, underscore, C, Cs, row2col_4_in_ggaa₄(R, ._2₂(C, Cs), Cols1, Accm))
row2col_4_in_ggaa₄(._2₂(X, Xs), ._2₂(._2₂(X, Ys), Cols), ._2₂(Ys, Cols1), ._2₂([]_0, As)) -> if_row2col_4_in_1_ggaa₇(X, Xs, Ys, Cols, Cols1, As, row2col_4_in_ggaa₄(Xs, Cols, Cols1, As))
row2col_4_in_ggaa₄([]_0, []_0, []_0, []_0) -> row2col_4_out_ggaa₄([]_0, []_0, []_0, []_0)
if_row2col_4_in_1_ggaa₇(X, Xs, Ys, Cols, Cols1, As, row2col_4_out_ggaa₄(Xs, Cols, Cols1, As)) -> row2col_4_out_ggaa₄(._2₂(X, Xs), ._2₂(._2₂(X, Ys), Cols), ._2₂(Ys, Cols1), ._2₂([]_0, As))
if_transpose_aux_3_in_1_ggg₆(R, Rs, underscore, C, Cs, row2col_4_out_ggaa₄(R, ._2₂(C, Cs), Cols1, Accm)) -> if_transpose_aux_3_in_2_ggg₈(R, Rs, underscore, C, Cs, Cols1, Accm, transpose_aux_3_in_ggg₃(Rs, Accm, Cols1))
transpose_aux_3_in_ggg₃([]_0, X, X) -> transpose_aux_3_out_ggg₃([]_0, X, X)
if_transpose_aux_3_in_2_ggg₈(R, Rs, underscore, C, Cs, Cols1, Accm, transpose_aux_3_out_ggg₃(Rs, Accm, Cols1)) -> transpose_aux_3_out_ggg₃(._2₂(R, Rs), underscore, ._2₂(C, Cs))
if_transpose_2_in_1_gg₃(A, B, transpose_aux_3_out_ggg₃(A, []_0, B)) -> transpose_2_out_gg₂(A, B)

TRANSPOSE_2_IN_GG₂(A, B) -> IF_TRANSPOSE_2_IN_1_GG₃(A, B, transpose_aux_3_in_ggg₃(A, []_0, B))
TRANSPOSE_2_IN_GG₂(A, B) -> TRANSPOSE_AUX_3_IN_GGG₃(A, []_0, B)
TRANSPOSE_AUX_3_IN_GGG₃(._2₂(R, Rs), underscore, ._2₂(C, Cs)) -> IF_TRANSPOSE_AUX_3_IN_1_GGG₆(R, Rs, underscore, C, Cs, row2col_4_in_ggaa₄(R, ._2₂(C, Cs), Cols1, Accm))
TRANSPOSE_AUX_3_IN_GGG₃(._2₂(R, Rs), underscore, ._2₂(C, Cs)) -> ROW2COL_4_IN_GGAA₄(R, ._2₂(C, Cs), Cols1, Accm)
ROW2COL_4_IN_GGAA₄(._2₂(X, Xs), ._2₂(._2₂(X, Ys), Cols), ._2₂(Ys, Cols1), ._2₂([]_0, As)) -> IF_ROW2COL_4_IN_1_GGAA₇(X, Xs, Ys, Cols, Cols1, As, row2col_4_in_ggaa₄(Xs, Cols, Cols1, As))
ROW2COL_4_IN_GGAA₄(._2₂(X, Xs), ._2₂(._2₂(X, Ys), Cols), ._2₂(Ys, Cols1), ._2₂([]_0, As)) -> ROW2COL_4_IN_GGAA₄(Xs, Cols, Cols1, As)
IF_TRANSPOSE_AUX_3_IN_1_GGG₆(R, Rs, underscore, C, Cs, row2col_4_out_ggaa₄(R, ._2₂(C, Cs), Cols1, Accm)) -> IF_TRANSPOSE_AUX_3_IN_2_GGG₈(R, Rs, underscore, C, Cs, Cols1, Accm, transpose_aux_3_in_ggg₃(Rs, Accm, Cols1))
IF_TRANSPOSE_AUX_3_IN_1_GGG₆(R, Rs, underscore, C, Cs, row2col_4_out_ggaa₄(R, ._2₂(C, Cs), Cols1, Accm)) -> TRANSPOSE_AUX_3_IN_GGG₃(Rs, Accm, Cols1)

The TRS R consists of the following rules:

transpose_2_in_gg₂(A, B) -> if_transpose_2_in_1_gg₃(A, B, transpose_aux_3_in_ggg₃(A, []_0, B))
transpose_aux_3_in_ggg₃(._2₂(R, Rs), underscore, ._2₂(C, Cs)) -> if_transpose_aux_3_in_1_ggg₆(R, Rs, underscore, C, Cs, row2col_4_in_ggaa₄(R, ._2₂(C, Cs), Cols1, Accm))
row2col_4_in_ggaa₄(._2₂(X, Xs), ._2₂(._2₂(X, Ys), Cols), ._2₂(Ys, Cols1), ._2₂([]_0, As)) -> if_row2col_4_in_1_ggaa₇(X, Xs, Ys, Cols, Cols1, As, row2col_4_in_ggaa₄(Xs, Cols, Cols1, As))
row2col_4_in_ggaa₄([]_0, []_0, []_0, []_0) -> row2col_4_out_ggaa₄([]_0, []_0, []_0, []_0)
if_row2col_4_in_1_ggaa₇(X, Xs, Ys, Cols, Cols1, As, row2col_4_out_ggaa₄(Xs, Cols, Cols1, As)) -> row2col_4_out_ggaa₄(._2₂(X, Xs), ._2₂(._2₂(X, Ys), Cols), ._2₂(Ys, Cols1), ._2₂([]_0, As))
if_transpose_aux_3_in_1_ggg₆(R, Rs, underscore, C, Cs, row2col_4_out_ggaa₄(R, ._2₂(C, Cs), Cols1, Accm)) -> if_transpose_aux_3_in_2_ggg₈(R, Rs, underscore, C, Cs, Cols1, Accm, transpose_aux_3_in_ggg₃(Rs, Accm, Cols1))
transpose_aux_3_in_ggg₃([]_0, X, X) -> transpose_aux_3_out_ggg₃([]_0, X, X)
if_transpose_aux_3_in_2_ggg₈(R, Rs, underscore, C, Cs, Cols1, Accm, transpose_aux_3_out_ggg₃(Rs, Accm, Cols1)) -> transpose_aux_3_out_ggg₃(._2₂(R, Rs), underscore, ._2₂(C, Cs))
if_transpose_2_in_1_gg₃(A, B, transpose_aux_3_out_ggg₃(A, []_0, B)) -> transpose_2_out_gg₂(A, B)

The argument filtering Pi contains the following mapping:
transpose_2_in_gg₂(x1, x2) = transpose_2_in_gg₂(x1, x2)
[]_0 = []_0
._2₂(x1, x2) = ._2₂(x1, x2)
if_transpose_2_in_1_gg₃(x1, x2, x3) = if_transpose_2_in_1_gg₁(x3)
transpose_aux_3_in_ggg₃(x1, x2, x3) = transpose_aux_3_in_ggg₃(x1, x2, x3)
if_transpose_aux_3_in_1_ggg₆(x1, x2, x3, x4, x5, x6) = if_transpose_aux_3_in_1_ggg₂(x2, x6)
row2col_4_in_ggaa₄(x1, x2, x3, x4) = row2col_4_in_ggaa₂(x1, x2)
if_row2col_4_in_1_ggaa₇(x1, x2, x3, x4, x5, x6, x7) = if_row2col_4_in_1_ggaa₂(x3, x7)
row2col_4_out_ggaa₄(x1, x2, x3, x4) = row2col_4_out_ggaa₂(x3, x4)
if_transpose_aux_3_in_2_ggg₈(x1, x2, x3, x4, x5, x6, x7, x8) = if_transpose_aux_3_in_2_ggg₁(x8)
transpose_aux_3_out_ggg₃(x1, x2, x3) = transpose_aux_3_out_ggg
transpose_2_out_gg₂(x1, x2) = transpose_2_out_gg
IF_TRANSPOSE_AUX_3_IN_1_GGG₆(x1, x2, x3, x4, x5, x6) = IF_TRANSPOSE_AUX_3_IN_1_GGG₂(x2, x6)
TRANSPOSE_2_IN_GG₂(x1, x2) = TRANSPOSE_2_IN_GG₂(x1, x2)
ROW2COL_4_IN_GGAA₄(x1, x2, x3, x4) = ROW2COL_4_IN_GGAA₂(x1, x2)
IF_ROW2COL_4_IN_1_GGAA₇(x1, x2, x3, x4, x5, x6, x7) = IF_ROW2COL_4_IN_1_GGAA₂(x3, x7)
TRANSPOSE_AUX_3_IN_GGG₃(x1, x2, x3) = TRANSPOSE_AUX_3_IN_GGG₃(x1, x2, x3)
IF_TRANSPOSE_AUX_3_IN_2_GGG₈(x1, x2, x3, x4, x5, x6, x7, x8) = IF_TRANSPOSE_AUX_3_IN_2_GGG₁(x8)
IF_TRANSPOSE_2_IN_1_GG₃(x1, x2, x3) = IF_TRANSPOSE_2_IN_1_GG₁(x3)

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

↳ PROLOG

  ↳ PrologToPiTRSProof

    ↳ PiTRS

      ↳ DependencyPairsProof

        ↳ PiDP

          ↳ DependencyGraphProof

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

TRANSPOSE_2_IN_GG₂(A, B) -> IF_TRANSPOSE_2_IN_1_GG₃(A, B, transpose_aux_3_in_ggg₃(A, []_0, B))
TRANSPOSE_2_IN_GG₂(A, B) -> TRANSPOSE_AUX_3_IN_GGG₃(A, []_0, B)
TRANSPOSE_AUX_3_IN_GGG₃(._2₂(R, Rs), underscore, ._2₂(C, Cs)) -> IF_TRANSPOSE_AUX_3_IN_1_GGG₆(R, Rs, underscore, C, Cs, row2col_4_in_ggaa₄(R, ._2₂(C, Cs), Cols1, Accm))
TRANSPOSE_AUX_3_IN_GGG₃(._2₂(R, Rs), underscore, ._2₂(C, Cs)) -> ROW2COL_4_IN_GGAA₄(R, ._2₂(C, Cs), Cols1, Accm)
ROW2COL_4_IN_GGAA₄(._2₂(X, Xs), ._2₂(._2₂(X, Ys), Cols), ._2₂(Ys, Cols1), ._2₂([]_0, As)) -> IF_ROW2COL_4_IN_1_GGAA₇(X, Xs, Ys, Cols, Cols1, As, row2col_4_in_ggaa₄(Xs, Cols, Cols1, As))
ROW2COL_4_IN_GGAA₄(._2₂(X, Xs), ._2₂(._2₂(X, Ys), Cols), ._2₂(Ys, Cols1), ._2₂([]_0, As)) -> ROW2COL_4_IN_GGAA₄(Xs, Cols, Cols1, As)
IF_TRANSPOSE_AUX_3_IN_1_GGG₆(R, Rs, underscore, C, Cs, row2col_4_out_ggaa₄(R, ._2₂(C, Cs), Cols1, Accm)) -> IF_TRANSPOSE_AUX_3_IN_2_GGG₈(R, Rs, underscore, C, Cs, Cols1, Accm, transpose_aux_3_in_ggg₃(Rs, Accm, Cols1))
IF_TRANSPOSE_AUX_3_IN_1_GGG₆(R, Rs, underscore, C, Cs, row2col_4_out_ggaa₄(R, ._2₂(C, Cs), Cols1, Accm)) -> TRANSPOSE_AUX_3_IN_GGG₃(Rs, Accm, Cols1)

The TRS R consists of the following rules:

transpose_2_in_gg₂(A, B) -> if_transpose_2_in_1_gg₃(A, B, transpose_aux_3_in_ggg₃(A, []_0, B))
transpose_aux_3_in_ggg₃(._2₂(R, Rs), underscore, ._2₂(C, Cs)) -> if_transpose_aux_3_in_1_ggg₆(R, Rs, underscore, C, Cs, row2col_4_in_ggaa₄(R, ._2₂(C, Cs), Cols1, Accm))
row2col_4_in_ggaa₄(._2₂(X, Xs), ._2₂(._2₂(X, Ys), Cols), ._2₂(Ys, Cols1), ._2₂([]_0, As)) -> if_row2col_4_in_1_ggaa₇(X, Xs, Ys, Cols, Cols1, As, row2col_4_in_ggaa₄(Xs, Cols, Cols1, As))
row2col_4_in_ggaa₄([]_0, []_0, []_0, []_0) -> row2col_4_out_ggaa₄([]_0, []_0, []_0, []_0)
if_row2col_4_in_1_ggaa₇(X, Xs, Ys, Cols, Cols1, As, row2col_4_out_ggaa₄(Xs, Cols, Cols1, As)) -> row2col_4_out_ggaa₄(._2₂(X, Xs), ._2₂(._2₂(X, Ys), Cols), ._2₂(Ys, Cols1), ._2₂([]_0, As))
if_transpose_aux_3_in_1_ggg₆(R, Rs, underscore, C, Cs, row2col_4_out_ggaa₄(R, ._2₂(C, Cs), Cols1, Accm)) -> if_transpose_aux_3_in_2_ggg₈(R, Rs, underscore, C, Cs, Cols1, Accm, transpose_aux_3_in_ggg₃(Rs, Accm, Cols1))
transpose_aux_3_in_ggg₃([]_0, X, X) -> transpose_aux_3_out_ggg₃([]_0, X, X)
if_transpose_aux_3_in_2_ggg₈(R, Rs, underscore, C, Cs, Cols1, Accm, transpose_aux_3_out_ggg₃(Rs, Accm, Cols1)) -> transpose_aux_3_out_ggg₃(._2₂(R, Rs), underscore, ._2₂(C, Cs))
if_transpose_2_in_1_gg₃(A, B, transpose_aux_3_out_ggg₃(A, []_0, B)) -> transpose_2_out_gg₂(A, B)

↳ PROLOG

  ↳ PrologToPiTRSProof

    ↳ PiTRS

      ↳ DependencyPairsProof

        ↳ PiDP

          ↳ DependencyGraphProof

            ↳ AND

              ↳ PiDP

                ↳ UsableRulesProof

              ↳ PiDP

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

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

The TRS R consists of the following rules:

transpose_2_in_gg₂(A, B) -> if_transpose_2_in_1_gg₃(A, B, transpose_aux_3_in_ggg₃(A, []_0, B))
transpose_aux_3_in_ggg₃(._2₂(R, Rs), underscore, ._2₂(C, Cs)) -> if_transpose_aux_3_in_1_ggg₆(R, Rs, underscore, C, Cs, row2col_4_in_ggaa₄(R, ._2₂(C, Cs), Cols1, Accm))
row2col_4_in_ggaa₄(._2₂(X, Xs), ._2₂(._2₂(X, Ys), Cols), ._2₂(Ys, Cols1), ._2₂([]_0, As)) -> if_row2col_4_in_1_ggaa₇(X, Xs, Ys, Cols, Cols1, As, row2col_4_in_ggaa₄(Xs, Cols, Cols1, As))
row2col_4_in_ggaa₄([]_0, []_0, []_0, []_0) -> row2col_4_out_ggaa₄([]_0, []_0, []_0, []_0)
if_row2col_4_in_1_ggaa₇(X, Xs, Ys, Cols, Cols1, As, row2col_4_out_ggaa₄(Xs, Cols, Cols1, As)) -> row2col_4_out_ggaa₄(._2₂(X, Xs), ._2₂(._2₂(X, Ys), Cols), ._2₂(Ys, Cols1), ._2₂([]_0, As))
if_transpose_aux_3_in_1_ggg₆(R, Rs, underscore, C, Cs, row2col_4_out_ggaa₄(R, ._2₂(C, Cs), Cols1, Accm)) -> if_transpose_aux_3_in_2_ggg₈(R, Rs, underscore, C, Cs, Cols1, Accm, transpose_aux_3_in_ggg₃(Rs, Accm, Cols1))
transpose_aux_3_in_ggg₃([]_0, X, X) -> transpose_aux_3_out_ggg₃([]_0, X, X)
if_transpose_aux_3_in_2_ggg₈(R, Rs, underscore, C, Cs, Cols1, Accm, transpose_aux_3_out_ggg₃(Rs, Accm, Cols1)) -> transpose_aux_3_out_ggg₃(._2₂(R, Rs), underscore, ._2₂(C, Cs))
if_transpose_2_in_1_gg₃(A, B, transpose_aux_3_out_ggg₃(A, []_0, B)) -> transpose_2_out_gg₂(A, B)

↳ PROLOG

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

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

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

                        ↳ QDPSizeChangeProof

              ↳ PiDP

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

ROW2COL_4_IN_GGAA₂(._2₂(X, Xs), ._2₂(._2₂(X, Ys), Cols)) -> ROW2COL_4_IN_GGAA₂(Xs, Cols)

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_GGAA₂}.
By using the subterm criterion together with the size-change analysis we have proven that there are no infinite chains for this DP problem.

From the DPs we obtained the following set of size-change graphs:

ROW2COL_4_IN_GGAA₂(._2₂(X, Xs), ._2₂(._2₂(X, Ys), Cols)) -> ROW2COL_4_IN_GGAA₂(Xs, Cols)
The graph contains the following edges 1 > 1, 2 > 2

↳ PROLOG

  ↳ PrologToPiTRSProof

    ↳ PiTRS

      ↳ DependencyPairsProof

        ↳ PiDP

          ↳ DependencyGraphProof

            ↳ AND

              ↳ PiDP

              ↳ PiDP

                ↳ UsableRulesProof

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

TRANSPOSE_AUX_3_IN_GGG₃(._2₂(R, Rs), underscore, ._2₂(C, Cs)) -> IF_TRANSPOSE_AUX_3_IN_1_GGG₆(R, Rs, underscore, C, Cs, row2col_4_in_ggaa₄(R, ._2₂(C, Cs), Cols1, Accm))
IF_TRANSPOSE_AUX_3_IN_1_GGG₆(R, Rs, underscore, C, Cs, row2col_4_out_ggaa₄(R, ._2₂(C, Cs), Cols1, Accm)) -> TRANSPOSE_AUX_3_IN_GGG₃(Rs, Accm, Cols1)

The TRS R consists of the following rules:

transpose_2_in_gg₂(A, B) -> if_transpose_2_in_1_gg₃(A, B, transpose_aux_3_in_ggg₃(A, []_0, B))
transpose_aux_3_in_ggg₃(._2₂(R, Rs), underscore, ._2₂(C, Cs)) -> if_transpose_aux_3_in_1_ggg₆(R, Rs, underscore, C, Cs, row2col_4_in_ggaa₄(R, ._2₂(C, Cs), Cols1, Accm))
row2col_4_in_ggaa₄(._2₂(X, Xs), ._2₂(._2₂(X, Ys), Cols), ._2₂(Ys, Cols1), ._2₂([]_0, As)) -> if_row2col_4_in_1_ggaa₇(X, Xs, Ys, Cols, Cols1, As, row2col_4_in_ggaa₄(Xs, Cols, Cols1, As))
row2col_4_in_ggaa₄([]_0, []_0, []_0, []_0) -> row2col_4_out_ggaa₄([]_0, []_0, []_0, []_0)
if_row2col_4_in_1_ggaa₇(X, Xs, Ys, Cols, Cols1, As, row2col_4_out_ggaa₄(Xs, Cols, Cols1, As)) -> row2col_4_out_ggaa₄(._2₂(X, Xs), ._2₂(._2₂(X, Ys), Cols), ._2₂(Ys, Cols1), ._2₂([]_0, As))
if_transpose_aux_3_in_1_ggg₆(R, Rs, underscore, C, Cs, row2col_4_out_ggaa₄(R, ._2₂(C, Cs), Cols1, Accm)) -> if_transpose_aux_3_in_2_ggg₈(R, Rs, underscore, C, Cs, Cols1, Accm, transpose_aux_3_in_ggg₃(Rs, Accm, Cols1))
transpose_aux_3_in_ggg₃([]_0, X, X) -> transpose_aux_3_out_ggg₃([]_0, X, X)
if_transpose_aux_3_in_2_ggg₈(R, Rs, underscore, C, Cs, Cols1, Accm, transpose_aux_3_out_ggg₃(Rs, Accm, Cols1)) -> transpose_aux_3_out_ggg₃(._2₂(R, Rs), underscore, ._2₂(C, Cs))
if_transpose_2_in_1_gg₃(A, B, transpose_aux_3_out_ggg₃(A, []_0, B)) -> transpose_2_out_gg₂(A, B)

The argument filtering Pi contains the following mapping:
transpose_2_in_gg₂(x1, x2) = transpose_2_in_gg₂(x1, x2)
[]_0 = []_0
._2₂(x1, x2) = ._2₂(x1, x2)
if_transpose_2_in_1_gg₃(x1, x2, x3) = if_transpose_2_in_1_gg₁(x3)
transpose_aux_3_in_ggg₃(x1, x2, x3) = transpose_aux_3_in_ggg₃(x1, x2, x3)
if_transpose_aux_3_in_1_ggg₆(x1, x2, x3, x4, x5, x6) = if_transpose_aux_3_in_1_ggg₂(x2, x6)
row2col_4_in_ggaa₄(x1, x2, x3, x4) = row2col_4_in_ggaa₂(x1, x2)
if_row2col_4_in_1_ggaa₇(x1, x2, x3, x4, x5, x6, x7) = if_row2col_4_in_1_ggaa₂(x3, x7)
row2col_4_out_ggaa₄(x1, x2, x3, x4) = row2col_4_out_ggaa₂(x3, x4)
if_transpose_aux_3_in_2_ggg₈(x1, x2, x3, x4, x5, x6, x7, x8) = if_transpose_aux_3_in_2_ggg₁(x8)
transpose_aux_3_out_ggg₃(x1, x2, x3) = transpose_aux_3_out_ggg
transpose_2_out_gg₂(x1, x2) = transpose_2_out_gg
IF_TRANSPOSE_AUX_3_IN_1_GGG₆(x1, x2, x3, x4, x5, x6) = IF_TRANSPOSE_AUX_3_IN_1_GGG₂(x2, x6)
TRANSPOSE_AUX_3_IN_GGG₃(x1, x2, x3) = TRANSPOSE_AUX_3_IN_GGG₃(x1, 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

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

TRANSPOSE_AUX_3_IN_GGG₃(._2₂(R, Rs), underscore, ._2₂(C, Cs)) -> IF_TRANSPOSE_AUX_3_IN_1_GGG₆(R, Rs, underscore, C, Cs, row2col_4_in_ggaa₄(R, ._2₂(C, Cs), Cols1, Accm))
IF_TRANSPOSE_AUX_3_IN_1_GGG₆(R, Rs, underscore, C, Cs, row2col_4_out_ggaa₄(R, ._2₂(C, Cs), Cols1, Accm)) -> TRANSPOSE_AUX_3_IN_GGG₃(Rs, Accm, Cols1)

The TRS R consists of the following rules:

row2col_4_in_ggaa₄(._2₂(X, Xs), ._2₂(._2₂(X, Ys), Cols), ._2₂(Ys, Cols1), ._2₂([]_0, As)) -> if_row2col_4_in_1_ggaa₇(X, Xs, Ys, Cols, Cols1, As, row2col_4_in_ggaa₄(Xs, Cols, Cols1, As))
if_row2col_4_in_1_ggaa₇(X, Xs, Ys, Cols, Cols1, As, row2col_4_out_ggaa₄(Xs, Cols, Cols1, As)) -> row2col_4_out_ggaa₄(._2₂(X, Xs), ._2₂(._2₂(X, Ys), Cols), ._2₂(Ys, Cols1), ._2₂([]_0, As))
row2col_4_in_ggaa₄([]_0, []_0, []_0, []_0) -> row2col_4_out_ggaa₄([]_0, []_0, []_0, []_0)

The argument filtering Pi contains the following mapping:
[]_0 = []_0
._2₂(x1, x2) = ._2₂(x1, x2)
row2col_4_in_ggaa₄(x1, x2, x3, x4) = row2col_4_in_ggaa₂(x1, x2)
if_row2col_4_in_1_ggaa₇(x1, x2, x3, x4, x5, x6, x7) = if_row2col_4_in_1_ggaa₂(x3, x7)
row2col_4_out_ggaa₄(x1, x2, x3, x4) = row2col_4_out_ggaa₂(x3, x4)
IF_TRANSPOSE_AUX_3_IN_1_GGG₆(x1, x2, x3, x4, x5, x6) = IF_TRANSPOSE_AUX_3_IN_1_GGG₂(x2, x6)
TRANSPOSE_AUX_3_IN_GGG₃(x1, x2, x3) = TRANSPOSE_AUX_3_IN_GGG₃(x1, 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

                        ↳ QDPSizeChangeProof

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

TRANSPOSE_AUX_3_IN_GGG₃(._2₂(R, Rs), underscore, ._2₂(C, Cs)) -> IF_TRANSPOSE_AUX_3_IN_1_GGG₂(Rs, row2col_4_in_ggaa₂(R, ._2₂(C, Cs)))
IF_TRANSPOSE_AUX_3_IN_1_GGG₂(Rs, row2col_4_out_ggaa₂(Cols1, Accm)) -> TRANSPOSE_AUX_3_IN_GGG₃(Rs, Accm, Cols1)

The TRS R consists of the following rules:

row2col_4_in_ggaa₂(._2₂(X, Xs), ._2₂(._2₂(X, Ys), Cols)) -> if_row2col_4_in_1_ggaa₂(Ys, row2col_4_in_ggaa₂(Xs, Cols))
if_row2col_4_in_1_ggaa₂(Ys, row2col_4_out_ggaa₂(Cols1, As)) -> row2col_4_out_ggaa₂(._2₂(Ys, Cols1), ._2₂([]_0, As))
row2col_4_in_ggaa₂([]_0, []_0) -> row2col_4_out_ggaa₂([]_0, []_0)

The set Q consists of the following terms:

row2col_4_in_ggaa₂(x0, x1)
if_row2col_4_in_1_ggaa₂(x0, x1)

We have to consider all (P,Q,R)-chains.
The head symbols of this DP problem are {IF_TRANSPOSE_AUX_3_IN_1_GGG₂, TRANSPOSE_AUX_3_IN_GGG₃}.
By using the subterm criterion together with the size-change analysis we have proven that there are no infinite chains for this DP problem.

From the DPs we obtained the following set of size-change graphs:

IF_TRANSPOSE_AUX_3_IN_1_GGG₂(Rs, row2col_4_out_ggaa₂(Cols1, Accm)) -> TRANSPOSE_AUX_3_IN_GGG₃(Rs, Accm, Cols1)
The graph contains the following edges 1 >= 1, 2 > 2, 2 > 3
TRANSPOSE_AUX_3_IN_GGG₃(._2₂(R, Rs), underscore, ._2₂(C, Cs)) -> IF_TRANSPOSE_AUX_3_IN_1_GGG₂(Rs, row2col_4_in_ggaa₂(R, ._2₂(C, Cs)))
The graph contains the following edges 1 > 1