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



↳ PROLOG
  ↳ PrologToPiTRSProof

shapes2(Matrix, N) :- varmat2(Matrix, MatrixWithVars), unifmatrx1(MatrixWithVars).
varmat2({}0, {}0).
varmat2(.2(L, Ls), .2(VL, VLs)) :- varmat2(L, VL), varmat2(Ls, VLs).
varmat2(.2(black0, Xs), .2(black0, VXs)) :- varmat2(Xs, VXs).
varmat2(.2(white0, Xs), .2(w1(underscore), VXs)) :- varmat2(Xs, VXs).
unifmatrx1(.2(L1, .2(L2, Ls))) :- uniflines2(L1, L2), unifmatrx1(.2(L2, Ls)).
unifmatrx1(.2(underscore1, {}0)).
uniflines2(.2(W, .2(X, L1s)), .2(Y, .2(Z, L2s))) :- unifpairs1(.2(W, .2(X, .2(Y, .2(Z, .2(W, .2(Y, .2(X, .2(Z, .2(W, .2(Z, .2(X, .2(Y, {}0))))))))))))), uniflines2(.2(X, L1s), .2(Z, L2s)).
uniflines2(.2(underscore2, {}0), .2(underscore3, {}0)).
unifpairs1({}0).
unifpairs1(.2(A, .2(B, Pairs))) :- unif2(A, B), unifpairs1(Pairs).
unif2(w1(A), w1(A)).
unif2(black0, black0).
unif2(black0, w1(underscore4)).
unif2(w1(underscore5), black0).


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


shapes_2_in_ga2(Matrix, N) -> if_shapes_2_in_1_ga3(Matrix, N, varmat_2_in_ga2(Matrix, MatrixWithVars))
varmat_2_in_ga2([]_0, []_0) -> varmat_2_out_ga2([]_0, []_0)
varmat_2_in_ga2(._22(L, Ls), ._22(VL, VLs)) -> if_varmat_2_in_1_ga5(L, Ls, VL, VLs, varmat_2_in_ga2(L, VL))
varmat_2_in_ga2(._22(black_0, Xs), ._22(black_0, VXs)) -> if_varmat_2_in_3_ga3(Xs, VXs, varmat_2_in_ga2(Xs, VXs))
varmat_2_in_ga2(._22(white_0, Xs), ._22(w_11(underscore), VXs)) -> if_varmat_2_in_4_ga4(Xs, underscore, VXs, varmat_2_in_ga2(Xs, VXs))
if_varmat_2_in_4_ga4(Xs, underscore, VXs, varmat_2_out_ga2(Xs, VXs)) -> varmat_2_out_ga2(._22(white_0, Xs), ._22(w_11(underscore), VXs))
if_varmat_2_in_3_ga3(Xs, VXs, varmat_2_out_ga2(Xs, VXs)) -> varmat_2_out_ga2(._22(black_0, Xs), ._22(black_0, VXs))
if_varmat_2_in_1_ga5(L, Ls, VL, VLs, varmat_2_out_ga2(L, VL)) -> if_varmat_2_in_2_ga5(L, Ls, VL, VLs, varmat_2_in_ga2(Ls, VLs))
if_varmat_2_in_2_ga5(L, Ls, VL, VLs, varmat_2_out_ga2(Ls, VLs)) -> varmat_2_out_ga2(._22(L, Ls), ._22(VL, VLs))
if_shapes_2_in_1_ga3(Matrix, N, varmat_2_out_ga2(Matrix, MatrixWithVars)) -> if_shapes_2_in_2_ga4(Matrix, N, MatrixWithVars, unif_matrx_1_in_g1(MatrixWithVars))
unif_matrx_1_in_g1(._22(L1, ._22(L2, Ls))) -> if_unif_matrx_1_in_1_g4(L1, L2, Ls, unif_lines_2_in_gg2(L1, L2))
unif_lines_2_in_gg2(._22(W, ._22(X, L1s)), ._22(Y, ._22(Z, L2s))) -> if_unif_lines_2_in_1_gg7(W, X, L1s, Y, Z, L2s, unif_pairs_1_in_g1(._22(W, ._22(X, ._22(Y, ._22(Z, ._22(W, ._22(Y, ._22(X, ._22(Z, ._22(W, ._22(Z, ._22(X, ._22(Y, []_0))))))))))))))
unif_pairs_1_in_g1([]_0) -> unif_pairs_1_out_g1([]_0)
unif_pairs_1_in_g1(._22(A, ._22(B, Pairs))) -> if_unif_pairs_1_in_1_g4(A, B, Pairs, unif_2_in_gg2(A, B))
unif_2_in_gg2(w_11(A), w_11(A)) -> unif_2_out_gg2(w_11(A), w_11(A))
unif_2_in_gg2(black_0, black_0) -> unif_2_out_gg2(black_0, black_0)
unif_2_in_gg2(black_0, w_11(underscore4)) -> unif_2_out_gg2(black_0, w_11(underscore4))
unif_2_in_gg2(w_11(underscore5), black_0) -> unif_2_out_gg2(w_11(underscore5), black_0)
if_unif_pairs_1_in_1_g4(A, B, Pairs, unif_2_out_gg2(A, B)) -> if_unif_pairs_1_in_2_g4(A, B, Pairs, unif_pairs_1_in_g1(Pairs))
if_unif_pairs_1_in_2_g4(A, B, Pairs, unif_pairs_1_out_g1(Pairs)) -> unif_pairs_1_out_g1(._22(A, ._22(B, Pairs)))
if_unif_lines_2_in_1_gg7(W, X, L1s, Y, Z, L2s, unif_pairs_1_out_g1(._22(W, ._22(X, ._22(Y, ._22(Z, ._22(W, ._22(Y, ._22(X, ._22(Z, ._22(W, ._22(Z, ._22(X, ._22(Y, []_0)))))))))))))) -> if_unif_lines_2_in_2_gg7(W, X, L1s, Y, Z, L2s, unif_lines_2_in_gg2(._22(X, L1s), ._22(Z, L2s)))
unif_lines_2_in_gg2(._22(underscore2, []_0), ._22(underscore3, []_0)) -> unif_lines_2_out_gg2(._22(underscore2, []_0), ._22(underscore3, []_0))
if_unif_lines_2_in_2_gg7(W, X, L1s, Y, Z, L2s, unif_lines_2_out_gg2(._22(X, L1s), ._22(Z, L2s))) -> unif_lines_2_out_gg2(._22(W, ._22(X, L1s)), ._22(Y, ._22(Z, L2s)))
if_unif_matrx_1_in_1_g4(L1, L2, Ls, unif_lines_2_out_gg2(L1, L2)) -> if_unif_matrx_1_in_2_g4(L1, L2, Ls, unif_matrx_1_in_g1(._22(L2, Ls)))
unif_matrx_1_in_g1(._22(underscore1, []_0)) -> unif_matrx_1_out_g1(._22(underscore1, []_0))
if_unif_matrx_1_in_2_g4(L1, L2, Ls, unif_matrx_1_out_g1(._22(L2, Ls))) -> unif_matrx_1_out_g1(._22(L1, ._22(L2, Ls)))
if_shapes_2_in_2_ga4(Matrix, N, MatrixWithVars, unif_matrx_1_out_g1(MatrixWithVars)) -> shapes_2_out_ga2(Matrix, N)

The argument filtering Pi contains the following mapping:
shapes_2_in_ga2(x1, x2)  =  shapes_2_in_ga1(x1)
[]_0  =  []_0
._22(x1, x2)  =  ._22(x1, x2)
black_0  =  black_0
white_0  =  white_0
w_11(x1)  =  w_1
if_shapes_2_in_1_ga3(x1, x2, x3)  =  if_shapes_2_in_1_ga1(x3)
varmat_2_in_ga2(x1, x2)  =  varmat_2_in_ga1(x1)
varmat_2_out_ga2(x1, x2)  =  varmat_2_out_ga1(x2)
if_varmat_2_in_1_ga5(x1, x2, x3, x4, x5)  =  if_varmat_2_in_1_ga2(x2, x5)
if_varmat_2_in_3_ga3(x1, x2, x3)  =  if_varmat_2_in_3_ga1(x3)
if_varmat_2_in_4_ga4(x1, x2, x3, x4)  =  if_varmat_2_in_4_ga1(x4)
if_varmat_2_in_2_ga5(x1, x2, x3, x4, x5)  =  if_varmat_2_in_2_ga2(x3, x5)
if_shapes_2_in_2_ga4(x1, x2, x3, x4)  =  if_shapes_2_in_2_ga1(x4)
unif_matrx_1_in_g1(x1)  =  unif_matrx_1_in_g1(x1)
if_unif_matrx_1_in_1_g4(x1, x2, x3, x4)  =  if_unif_matrx_1_in_1_g3(x2, x3, x4)
unif_lines_2_in_gg2(x1, x2)  =  unif_lines_2_in_gg2(x1, x2)
if_unif_lines_2_in_1_gg7(x1, x2, x3, x4, x5, x6, x7)  =  if_unif_lines_2_in_1_gg5(x2, x3, x5, x6, x7)
unif_pairs_1_in_g1(x1)  =  unif_pairs_1_in_g1(x1)
unif_pairs_1_out_g1(x1)  =  unif_pairs_1_out_g
if_unif_pairs_1_in_1_g4(x1, x2, x3, x4)  =  if_unif_pairs_1_in_1_g2(x3, x4)
unif_2_in_gg2(x1, x2)  =  unif_2_in_gg2(x1, x2)
unif_2_out_gg2(x1, x2)  =  unif_2_out_gg
if_unif_pairs_1_in_2_g4(x1, x2, x3, x4)  =  if_unif_pairs_1_in_2_g1(x4)
if_unif_lines_2_in_2_gg7(x1, x2, x3, x4, x5, x6, x7)  =  if_unif_lines_2_in_2_gg1(x7)
unif_lines_2_out_gg2(x1, x2)  =  unif_lines_2_out_gg
if_unif_matrx_1_in_2_g4(x1, x2, x3, x4)  =  if_unif_matrx_1_in_2_g1(x4)
unif_matrx_1_out_g1(x1)  =  unif_matrx_1_out_g
shapes_2_out_ga2(x1, x2)  =  shapes_2_out_ga

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:

shapes_2_in_ga2(Matrix, N) -> if_shapes_2_in_1_ga3(Matrix, N, varmat_2_in_ga2(Matrix, MatrixWithVars))
varmat_2_in_ga2([]_0, []_0) -> varmat_2_out_ga2([]_0, []_0)
varmat_2_in_ga2(._22(L, Ls), ._22(VL, VLs)) -> if_varmat_2_in_1_ga5(L, Ls, VL, VLs, varmat_2_in_ga2(L, VL))
varmat_2_in_ga2(._22(black_0, Xs), ._22(black_0, VXs)) -> if_varmat_2_in_3_ga3(Xs, VXs, varmat_2_in_ga2(Xs, VXs))
varmat_2_in_ga2(._22(white_0, Xs), ._22(w_11(underscore), VXs)) -> if_varmat_2_in_4_ga4(Xs, underscore, VXs, varmat_2_in_ga2(Xs, VXs))
if_varmat_2_in_4_ga4(Xs, underscore, VXs, varmat_2_out_ga2(Xs, VXs)) -> varmat_2_out_ga2(._22(white_0, Xs), ._22(w_11(underscore), VXs))
if_varmat_2_in_3_ga3(Xs, VXs, varmat_2_out_ga2(Xs, VXs)) -> varmat_2_out_ga2(._22(black_0, Xs), ._22(black_0, VXs))
if_varmat_2_in_1_ga5(L, Ls, VL, VLs, varmat_2_out_ga2(L, VL)) -> if_varmat_2_in_2_ga5(L, Ls, VL, VLs, varmat_2_in_ga2(Ls, VLs))
if_varmat_2_in_2_ga5(L, Ls, VL, VLs, varmat_2_out_ga2(Ls, VLs)) -> varmat_2_out_ga2(._22(L, Ls), ._22(VL, VLs))
if_shapes_2_in_1_ga3(Matrix, N, varmat_2_out_ga2(Matrix, MatrixWithVars)) -> if_shapes_2_in_2_ga4(Matrix, N, MatrixWithVars, unif_matrx_1_in_g1(MatrixWithVars))
unif_matrx_1_in_g1(._22(L1, ._22(L2, Ls))) -> if_unif_matrx_1_in_1_g4(L1, L2, Ls, unif_lines_2_in_gg2(L1, L2))
unif_lines_2_in_gg2(._22(W, ._22(X, L1s)), ._22(Y, ._22(Z, L2s))) -> if_unif_lines_2_in_1_gg7(W, X, L1s, Y, Z, L2s, unif_pairs_1_in_g1(._22(W, ._22(X, ._22(Y, ._22(Z, ._22(W, ._22(Y, ._22(X, ._22(Z, ._22(W, ._22(Z, ._22(X, ._22(Y, []_0))))))))))))))
unif_pairs_1_in_g1([]_0) -> unif_pairs_1_out_g1([]_0)
unif_pairs_1_in_g1(._22(A, ._22(B, Pairs))) -> if_unif_pairs_1_in_1_g4(A, B, Pairs, unif_2_in_gg2(A, B))
unif_2_in_gg2(w_11(A), w_11(A)) -> unif_2_out_gg2(w_11(A), w_11(A))
unif_2_in_gg2(black_0, black_0) -> unif_2_out_gg2(black_0, black_0)
unif_2_in_gg2(black_0, w_11(underscore4)) -> unif_2_out_gg2(black_0, w_11(underscore4))
unif_2_in_gg2(w_11(underscore5), black_0) -> unif_2_out_gg2(w_11(underscore5), black_0)
if_unif_pairs_1_in_1_g4(A, B, Pairs, unif_2_out_gg2(A, B)) -> if_unif_pairs_1_in_2_g4(A, B, Pairs, unif_pairs_1_in_g1(Pairs))
if_unif_pairs_1_in_2_g4(A, B, Pairs, unif_pairs_1_out_g1(Pairs)) -> unif_pairs_1_out_g1(._22(A, ._22(B, Pairs)))
if_unif_lines_2_in_1_gg7(W, X, L1s, Y, Z, L2s, unif_pairs_1_out_g1(._22(W, ._22(X, ._22(Y, ._22(Z, ._22(W, ._22(Y, ._22(X, ._22(Z, ._22(W, ._22(Z, ._22(X, ._22(Y, []_0)))))))))))))) -> if_unif_lines_2_in_2_gg7(W, X, L1s, Y, Z, L2s, unif_lines_2_in_gg2(._22(X, L1s), ._22(Z, L2s)))
unif_lines_2_in_gg2(._22(underscore2, []_0), ._22(underscore3, []_0)) -> unif_lines_2_out_gg2(._22(underscore2, []_0), ._22(underscore3, []_0))
if_unif_lines_2_in_2_gg7(W, X, L1s, Y, Z, L2s, unif_lines_2_out_gg2(._22(X, L1s), ._22(Z, L2s))) -> unif_lines_2_out_gg2(._22(W, ._22(X, L1s)), ._22(Y, ._22(Z, L2s)))
if_unif_matrx_1_in_1_g4(L1, L2, Ls, unif_lines_2_out_gg2(L1, L2)) -> if_unif_matrx_1_in_2_g4(L1, L2, Ls, unif_matrx_1_in_g1(._22(L2, Ls)))
unif_matrx_1_in_g1(._22(underscore1, []_0)) -> unif_matrx_1_out_g1(._22(underscore1, []_0))
if_unif_matrx_1_in_2_g4(L1, L2, Ls, unif_matrx_1_out_g1(._22(L2, Ls))) -> unif_matrx_1_out_g1(._22(L1, ._22(L2, Ls)))
if_shapes_2_in_2_ga4(Matrix, N, MatrixWithVars, unif_matrx_1_out_g1(MatrixWithVars)) -> shapes_2_out_ga2(Matrix, N)

The argument filtering Pi contains the following mapping:
shapes_2_in_ga2(x1, x2)  =  shapes_2_in_ga1(x1)
[]_0  =  []_0
._22(x1, x2)  =  ._22(x1, x2)
black_0  =  black_0
white_0  =  white_0
w_11(x1)  =  w_1
if_shapes_2_in_1_ga3(x1, x2, x3)  =  if_shapes_2_in_1_ga1(x3)
varmat_2_in_ga2(x1, x2)  =  varmat_2_in_ga1(x1)
varmat_2_out_ga2(x1, x2)  =  varmat_2_out_ga1(x2)
if_varmat_2_in_1_ga5(x1, x2, x3, x4, x5)  =  if_varmat_2_in_1_ga2(x2, x5)
if_varmat_2_in_3_ga3(x1, x2, x3)  =  if_varmat_2_in_3_ga1(x3)
if_varmat_2_in_4_ga4(x1, x2, x3, x4)  =  if_varmat_2_in_4_ga1(x4)
if_varmat_2_in_2_ga5(x1, x2, x3, x4, x5)  =  if_varmat_2_in_2_ga2(x3, x5)
if_shapes_2_in_2_ga4(x1, x2, x3, x4)  =  if_shapes_2_in_2_ga1(x4)
unif_matrx_1_in_g1(x1)  =  unif_matrx_1_in_g1(x1)
if_unif_matrx_1_in_1_g4(x1, x2, x3, x4)  =  if_unif_matrx_1_in_1_g3(x2, x3, x4)
unif_lines_2_in_gg2(x1, x2)  =  unif_lines_2_in_gg2(x1, x2)
if_unif_lines_2_in_1_gg7(x1, x2, x3, x4, x5, x6, x7)  =  if_unif_lines_2_in_1_gg5(x2, x3, x5, x6, x7)
unif_pairs_1_in_g1(x1)  =  unif_pairs_1_in_g1(x1)
unif_pairs_1_out_g1(x1)  =  unif_pairs_1_out_g
if_unif_pairs_1_in_1_g4(x1, x2, x3, x4)  =  if_unif_pairs_1_in_1_g2(x3, x4)
unif_2_in_gg2(x1, x2)  =  unif_2_in_gg2(x1, x2)
unif_2_out_gg2(x1, x2)  =  unif_2_out_gg
if_unif_pairs_1_in_2_g4(x1, x2, x3, x4)  =  if_unif_pairs_1_in_2_g1(x4)
if_unif_lines_2_in_2_gg7(x1, x2, x3, x4, x5, x6, x7)  =  if_unif_lines_2_in_2_gg1(x7)
unif_lines_2_out_gg2(x1, x2)  =  unif_lines_2_out_gg
if_unif_matrx_1_in_2_g4(x1, x2, x3, x4)  =  if_unif_matrx_1_in_2_g1(x4)
unif_matrx_1_out_g1(x1)  =  unif_matrx_1_out_g
shapes_2_out_ga2(x1, x2)  =  shapes_2_out_ga


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

SHAPES_2_IN_GA2(Matrix, N) -> IF_SHAPES_2_IN_1_GA3(Matrix, N, varmat_2_in_ga2(Matrix, MatrixWithVars))
SHAPES_2_IN_GA2(Matrix, N) -> VARMAT_2_IN_GA2(Matrix, MatrixWithVars)
VARMAT_2_IN_GA2(._22(L, Ls), ._22(VL, VLs)) -> IF_VARMAT_2_IN_1_GA5(L, Ls, VL, VLs, varmat_2_in_ga2(L, VL))
VARMAT_2_IN_GA2(._22(L, Ls), ._22(VL, VLs)) -> VARMAT_2_IN_GA2(L, VL)
VARMAT_2_IN_GA2(._22(black_0, Xs), ._22(black_0, VXs)) -> IF_VARMAT_2_IN_3_GA3(Xs, VXs, varmat_2_in_ga2(Xs, VXs))
VARMAT_2_IN_GA2(._22(black_0, Xs), ._22(black_0, VXs)) -> VARMAT_2_IN_GA2(Xs, VXs)
VARMAT_2_IN_GA2(._22(white_0, Xs), ._22(w_11(underscore), VXs)) -> IF_VARMAT_2_IN_4_GA4(Xs, underscore, VXs, varmat_2_in_ga2(Xs, VXs))
VARMAT_2_IN_GA2(._22(white_0, Xs), ._22(w_11(underscore), VXs)) -> VARMAT_2_IN_GA2(Xs, VXs)
IF_VARMAT_2_IN_1_GA5(L, Ls, VL, VLs, varmat_2_out_ga2(L, VL)) -> IF_VARMAT_2_IN_2_GA5(L, Ls, VL, VLs, varmat_2_in_ga2(Ls, VLs))
IF_VARMAT_2_IN_1_GA5(L, Ls, VL, VLs, varmat_2_out_ga2(L, VL)) -> VARMAT_2_IN_GA2(Ls, VLs)
IF_SHAPES_2_IN_1_GA3(Matrix, N, varmat_2_out_ga2(Matrix, MatrixWithVars)) -> IF_SHAPES_2_IN_2_GA4(Matrix, N, MatrixWithVars, unif_matrx_1_in_g1(MatrixWithVars))
IF_SHAPES_2_IN_1_GA3(Matrix, N, varmat_2_out_ga2(Matrix, MatrixWithVars)) -> UNIF_MATRX_1_IN_G1(MatrixWithVars)
UNIF_MATRX_1_IN_G1(._22(L1, ._22(L2, Ls))) -> IF_UNIF_MATRX_1_IN_1_G4(L1, L2, Ls, unif_lines_2_in_gg2(L1, L2))
UNIF_MATRX_1_IN_G1(._22(L1, ._22(L2, Ls))) -> UNIF_LINES_2_IN_GG2(L1, L2)
UNIF_LINES_2_IN_GG2(._22(W, ._22(X, L1s)), ._22(Y, ._22(Z, L2s))) -> IF_UNIF_LINES_2_IN_1_GG7(W, X, L1s, Y, Z, L2s, unif_pairs_1_in_g1(._22(W, ._22(X, ._22(Y, ._22(Z, ._22(W, ._22(Y, ._22(X, ._22(Z, ._22(W, ._22(Z, ._22(X, ._22(Y, []_0))))))))))))))
UNIF_LINES_2_IN_GG2(._22(W, ._22(X, L1s)), ._22(Y, ._22(Z, L2s))) -> UNIF_PAIRS_1_IN_G1(._22(W, ._22(X, ._22(Y, ._22(Z, ._22(W, ._22(Y, ._22(X, ._22(Z, ._22(W, ._22(Z, ._22(X, ._22(Y, []_0)))))))))))))
UNIF_PAIRS_1_IN_G1(._22(A, ._22(B, Pairs))) -> IF_UNIF_PAIRS_1_IN_1_G4(A, B, Pairs, unif_2_in_gg2(A, B))
UNIF_PAIRS_1_IN_G1(._22(A, ._22(B, Pairs))) -> UNIF_2_IN_GG2(A, B)
IF_UNIF_PAIRS_1_IN_1_G4(A, B, Pairs, unif_2_out_gg2(A, B)) -> IF_UNIF_PAIRS_1_IN_2_G4(A, B, Pairs, unif_pairs_1_in_g1(Pairs))
IF_UNIF_PAIRS_1_IN_1_G4(A, B, Pairs, unif_2_out_gg2(A, B)) -> UNIF_PAIRS_1_IN_G1(Pairs)
IF_UNIF_LINES_2_IN_1_GG7(W, X, L1s, Y, Z, L2s, unif_pairs_1_out_g1(._22(W, ._22(X, ._22(Y, ._22(Z, ._22(W, ._22(Y, ._22(X, ._22(Z, ._22(W, ._22(Z, ._22(X, ._22(Y, []_0)))))))))))))) -> IF_UNIF_LINES_2_IN_2_GG7(W, X, L1s, Y, Z, L2s, unif_lines_2_in_gg2(._22(X, L1s), ._22(Z, L2s)))
IF_UNIF_LINES_2_IN_1_GG7(W, X, L1s, Y, Z, L2s, unif_pairs_1_out_g1(._22(W, ._22(X, ._22(Y, ._22(Z, ._22(W, ._22(Y, ._22(X, ._22(Z, ._22(W, ._22(Z, ._22(X, ._22(Y, []_0)))))))))))))) -> UNIF_LINES_2_IN_GG2(._22(X, L1s), ._22(Z, L2s))
IF_UNIF_MATRX_1_IN_1_G4(L1, L2, Ls, unif_lines_2_out_gg2(L1, L2)) -> IF_UNIF_MATRX_1_IN_2_G4(L1, L2, Ls, unif_matrx_1_in_g1(._22(L2, Ls)))
IF_UNIF_MATRX_1_IN_1_G4(L1, L2, Ls, unif_lines_2_out_gg2(L1, L2)) -> UNIF_MATRX_1_IN_G1(._22(L2, Ls))

The TRS R consists of the following rules:

shapes_2_in_ga2(Matrix, N) -> if_shapes_2_in_1_ga3(Matrix, N, varmat_2_in_ga2(Matrix, MatrixWithVars))
varmat_2_in_ga2([]_0, []_0) -> varmat_2_out_ga2([]_0, []_0)
varmat_2_in_ga2(._22(L, Ls), ._22(VL, VLs)) -> if_varmat_2_in_1_ga5(L, Ls, VL, VLs, varmat_2_in_ga2(L, VL))
varmat_2_in_ga2(._22(black_0, Xs), ._22(black_0, VXs)) -> if_varmat_2_in_3_ga3(Xs, VXs, varmat_2_in_ga2(Xs, VXs))
varmat_2_in_ga2(._22(white_0, Xs), ._22(w_11(underscore), VXs)) -> if_varmat_2_in_4_ga4(Xs, underscore, VXs, varmat_2_in_ga2(Xs, VXs))
if_varmat_2_in_4_ga4(Xs, underscore, VXs, varmat_2_out_ga2(Xs, VXs)) -> varmat_2_out_ga2(._22(white_0, Xs), ._22(w_11(underscore), VXs))
if_varmat_2_in_3_ga3(Xs, VXs, varmat_2_out_ga2(Xs, VXs)) -> varmat_2_out_ga2(._22(black_0, Xs), ._22(black_0, VXs))
if_varmat_2_in_1_ga5(L, Ls, VL, VLs, varmat_2_out_ga2(L, VL)) -> if_varmat_2_in_2_ga5(L, Ls, VL, VLs, varmat_2_in_ga2(Ls, VLs))
if_varmat_2_in_2_ga5(L, Ls, VL, VLs, varmat_2_out_ga2(Ls, VLs)) -> varmat_2_out_ga2(._22(L, Ls), ._22(VL, VLs))
if_shapes_2_in_1_ga3(Matrix, N, varmat_2_out_ga2(Matrix, MatrixWithVars)) -> if_shapes_2_in_2_ga4(Matrix, N, MatrixWithVars, unif_matrx_1_in_g1(MatrixWithVars))
unif_matrx_1_in_g1(._22(L1, ._22(L2, Ls))) -> if_unif_matrx_1_in_1_g4(L1, L2, Ls, unif_lines_2_in_gg2(L1, L2))
unif_lines_2_in_gg2(._22(W, ._22(X, L1s)), ._22(Y, ._22(Z, L2s))) -> if_unif_lines_2_in_1_gg7(W, X, L1s, Y, Z, L2s, unif_pairs_1_in_g1(._22(W, ._22(X, ._22(Y, ._22(Z, ._22(W, ._22(Y, ._22(X, ._22(Z, ._22(W, ._22(Z, ._22(X, ._22(Y, []_0))))))))))))))
unif_pairs_1_in_g1([]_0) -> unif_pairs_1_out_g1([]_0)
unif_pairs_1_in_g1(._22(A, ._22(B, Pairs))) -> if_unif_pairs_1_in_1_g4(A, B, Pairs, unif_2_in_gg2(A, B))
unif_2_in_gg2(w_11(A), w_11(A)) -> unif_2_out_gg2(w_11(A), w_11(A))
unif_2_in_gg2(black_0, black_0) -> unif_2_out_gg2(black_0, black_0)
unif_2_in_gg2(black_0, w_11(underscore4)) -> unif_2_out_gg2(black_0, w_11(underscore4))
unif_2_in_gg2(w_11(underscore5), black_0) -> unif_2_out_gg2(w_11(underscore5), black_0)
if_unif_pairs_1_in_1_g4(A, B, Pairs, unif_2_out_gg2(A, B)) -> if_unif_pairs_1_in_2_g4(A, B, Pairs, unif_pairs_1_in_g1(Pairs))
if_unif_pairs_1_in_2_g4(A, B, Pairs, unif_pairs_1_out_g1(Pairs)) -> unif_pairs_1_out_g1(._22(A, ._22(B, Pairs)))
if_unif_lines_2_in_1_gg7(W, X, L1s, Y, Z, L2s, unif_pairs_1_out_g1(._22(W, ._22(X, ._22(Y, ._22(Z, ._22(W, ._22(Y, ._22(X, ._22(Z, ._22(W, ._22(Z, ._22(X, ._22(Y, []_0)))))))))))))) -> if_unif_lines_2_in_2_gg7(W, X, L1s, Y, Z, L2s, unif_lines_2_in_gg2(._22(X, L1s), ._22(Z, L2s)))
unif_lines_2_in_gg2(._22(underscore2, []_0), ._22(underscore3, []_0)) -> unif_lines_2_out_gg2(._22(underscore2, []_0), ._22(underscore3, []_0))
if_unif_lines_2_in_2_gg7(W, X, L1s, Y, Z, L2s, unif_lines_2_out_gg2(._22(X, L1s), ._22(Z, L2s))) -> unif_lines_2_out_gg2(._22(W, ._22(X, L1s)), ._22(Y, ._22(Z, L2s)))
if_unif_matrx_1_in_1_g4(L1, L2, Ls, unif_lines_2_out_gg2(L1, L2)) -> if_unif_matrx_1_in_2_g4(L1, L2, Ls, unif_matrx_1_in_g1(._22(L2, Ls)))
unif_matrx_1_in_g1(._22(underscore1, []_0)) -> unif_matrx_1_out_g1(._22(underscore1, []_0))
if_unif_matrx_1_in_2_g4(L1, L2, Ls, unif_matrx_1_out_g1(._22(L2, Ls))) -> unif_matrx_1_out_g1(._22(L1, ._22(L2, Ls)))
if_shapes_2_in_2_ga4(Matrix, N, MatrixWithVars, unif_matrx_1_out_g1(MatrixWithVars)) -> shapes_2_out_ga2(Matrix, N)

The argument filtering Pi contains the following mapping:
shapes_2_in_ga2(x1, x2)  =  shapes_2_in_ga1(x1)
[]_0  =  []_0
._22(x1, x2)  =  ._22(x1, x2)
black_0  =  black_0
white_0  =  white_0
w_11(x1)  =  w_1
if_shapes_2_in_1_ga3(x1, x2, x3)  =  if_shapes_2_in_1_ga1(x3)
varmat_2_in_ga2(x1, x2)  =  varmat_2_in_ga1(x1)
varmat_2_out_ga2(x1, x2)  =  varmat_2_out_ga1(x2)
if_varmat_2_in_1_ga5(x1, x2, x3, x4, x5)  =  if_varmat_2_in_1_ga2(x2, x5)
if_varmat_2_in_3_ga3(x1, x2, x3)  =  if_varmat_2_in_3_ga1(x3)
if_varmat_2_in_4_ga4(x1, x2, x3, x4)  =  if_varmat_2_in_4_ga1(x4)
if_varmat_2_in_2_ga5(x1, x2, x3, x4, x5)  =  if_varmat_2_in_2_ga2(x3, x5)
if_shapes_2_in_2_ga4(x1, x2, x3, x4)  =  if_shapes_2_in_2_ga1(x4)
unif_matrx_1_in_g1(x1)  =  unif_matrx_1_in_g1(x1)
if_unif_matrx_1_in_1_g4(x1, x2, x3, x4)  =  if_unif_matrx_1_in_1_g3(x2, x3, x4)
unif_lines_2_in_gg2(x1, x2)  =  unif_lines_2_in_gg2(x1, x2)
if_unif_lines_2_in_1_gg7(x1, x2, x3, x4, x5, x6, x7)  =  if_unif_lines_2_in_1_gg5(x2, x3, x5, x6, x7)
unif_pairs_1_in_g1(x1)  =  unif_pairs_1_in_g1(x1)
unif_pairs_1_out_g1(x1)  =  unif_pairs_1_out_g
if_unif_pairs_1_in_1_g4(x1, x2, x3, x4)  =  if_unif_pairs_1_in_1_g2(x3, x4)
unif_2_in_gg2(x1, x2)  =  unif_2_in_gg2(x1, x2)
unif_2_out_gg2(x1, x2)  =  unif_2_out_gg
if_unif_pairs_1_in_2_g4(x1, x2, x3, x4)  =  if_unif_pairs_1_in_2_g1(x4)
if_unif_lines_2_in_2_gg7(x1, x2, x3, x4, x5, x6, x7)  =  if_unif_lines_2_in_2_gg1(x7)
unif_lines_2_out_gg2(x1, x2)  =  unif_lines_2_out_gg
if_unif_matrx_1_in_2_g4(x1, x2, x3, x4)  =  if_unif_matrx_1_in_2_g1(x4)
unif_matrx_1_out_g1(x1)  =  unif_matrx_1_out_g
shapes_2_out_ga2(x1, x2)  =  shapes_2_out_ga
VARMAT_2_IN_GA2(x1, x2)  =  VARMAT_2_IN_GA1(x1)
IF_UNIF_LINES_2_IN_1_GG7(x1, x2, x3, x4, x5, x6, x7)  =  IF_UNIF_LINES_2_IN_1_GG5(x2, x3, x5, x6, x7)
IF_VARMAT_2_IN_2_GA5(x1, x2, x3, x4, x5)  =  IF_VARMAT_2_IN_2_GA2(x3, x5)
IF_SHAPES_2_IN_2_GA4(x1, x2, x3, x4)  =  IF_SHAPES_2_IN_2_GA1(x4)
UNIF_MATRX_1_IN_G1(x1)  =  UNIF_MATRX_1_IN_G1(x1)
IF_VARMAT_2_IN_1_GA5(x1, x2, x3, x4, x5)  =  IF_VARMAT_2_IN_1_GA2(x2, x5)
IF_UNIF_LINES_2_IN_2_GG7(x1, x2, x3, x4, x5, x6, x7)  =  IF_UNIF_LINES_2_IN_2_GG1(x7)
IF_SHAPES_2_IN_1_GA3(x1, x2, x3)  =  IF_SHAPES_2_IN_1_GA1(x3)
IF_VARMAT_2_IN_3_GA3(x1, x2, x3)  =  IF_VARMAT_2_IN_3_GA1(x3)
IF_UNIF_PAIRS_1_IN_2_G4(x1, x2, x3, x4)  =  IF_UNIF_PAIRS_1_IN_2_G1(x4)
IF_UNIF_MATRX_1_IN_1_G4(x1, x2, x3, x4)  =  IF_UNIF_MATRX_1_IN_1_G3(x2, x3, x4)
UNIF_2_IN_GG2(x1, x2)  =  UNIF_2_IN_GG2(x1, x2)
IF_UNIF_PAIRS_1_IN_1_G4(x1, x2, x3, x4)  =  IF_UNIF_PAIRS_1_IN_1_G2(x3, x4)
SHAPES_2_IN_GA2(x1, x2)  =  SHAPES_2_IN_GA1(x1)
IF_VARMAT_2_IN_4_GA4(x1, x2, x3, x4)  =  IF_VARMAT_2_IN_4_GA1(x4)
UNIF_LINES_2_IN_GG2(x1, x2)  =  UNIF_LINES_2_IN_GG2(x1, x2)
IF_UNIF_MATRX_1_IN_2_G4(x1, x2, x3, x4)  =  IF_UNIF_MATRX_1_IN_2_G1(x4)
UNIF_PAIRS_1_IN_G1(x1)  =  UNIF_PAIRS_1_IN_G1(x1)

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:

SHAPES_2_IN_GA2(Matrix, N) -> IF_SHAPES_2_IN_1_GA3(Matrix, N, varmat_2_in_ga2(Matrix, MatrixWithVars))
SHAPES_2_IN_GA2(Matrix, N) -> VARMAT_2_IN_GA2(Matrix, MatrixWithVars)
VARMAT_2_IN_GA2(._22(L, Ls), ._22(VL, VLs)) -> IF_VARMAT_2_IN_1_GA5(L, Ls, VL, VLs, varmat_2_in_ga2(L, VL))
VARMAT_2_IN_GA2(._22(L, Ls), ._22(VL, VLs)) -> VARMAT_2_IN_GA2(L, VL)
VARMAT_2_IN_GA2(._22(black_0, Xs), ._22(black_0, VXs)) -> IF_VARMAT_2_IN_3_GA3(Xs, VXs, varmat_2_in_ga2(Xs, VXs))
VARMAT_2_IN_GA2(._22(black_0, Xs), ._22(black_0, VXs)) -> VARMAT_2_IN_GA2(Xs, VXs)
VARMAT_2_IN_GA2(._22(white_0, Xs), ._22(w_11(underscore), VXs)) -> IF_VARMAT_2_IN_4_GA4(Xs, underscore, VXs, varmat_2_in_ga2(Xs, VXs))
VARMAT_2_IN_GA2(._22(white_0, Xs), ._22(w_11(underscore), VXs)) -> VARMAT_2_IN_GA2(Xs, VXs)
IF_VARMAT_2_IN_1_GA5(L, Ls, VL, VLs, varmat_2_out_ga2(L, VL)) -> IF_VARMAT_2_IN_2_GA5(L, Ls, VL, VLs, varmat_2_in_ga2(Ls, VLs))
IF_VARMAT_2_IN_1_GA5(L, Ls, VL, VLs, varmat_2_out_ga2(L, VL)) -> VARMAT_2_IN_GA2(Ls, VLs)
IF_SHAPES_2_IN_1_GA3(Matrix, N, varmat_2_out_ga2(Matrix, MatrixWithVars)) -> IF_SHAPES_2_IN_2_GA4(Matrix, N, MatrixWithVars, unif_matrx_1_in_g1(MatrixWithVars))
IF_SHAPES_2_IN_1_GA3(Matrix, N, varmat_2_out_ga2(Matrix, MatrixWithVars)) -> UNIF_MATRX_1_IN_G1(MatrixWithVars)
UNIF_MATRX_1_IN_G1(._22(L1, ._22(L2, Ls))) -> IF_UNIF_MATRX_1_IN_1_G4(L1, L2, Ls, unif_lines_2_in_gg2(L1, L2))
UNIF_MATRX_1_IN_G1(._22(L1, ._22(L2, Ls))) -> UNIF_LINES_2_IN_GG2(L1, L2)
UNIF_LINES_2_IN_GG2(._22(W, ._22(X, L1s)), ._22(Y, ._22(Z, L2s))) -> IF_UNIF_LINES_2_IN_1_GG7(W, X, L1s, Y, Z, L2s, unif_pairs_1_in_g1(._22(W, ._22(X, ._22(Y, ._22(Z, ._22(W, ._22(Y, ._22(X, ._22(Z, ._22(W, ._22(Z, ._22(X, ._22(Y, []_0))))))))))))))
UNIF_LINES_2_IN_GG2(._22(W, ._22(X, L1s)), ._22(Y, ._22(Z, L2s))) -> UNIF_PAIRS_1_IN_G1(._22(W, ._22(X, ._22(Y, ._22(Z, ._22(W, ._22(Y, ._22(X, ._22(Z, ._22(W, ._22(Z, ._22(X, ._22(Y, []_0)))))))))))))
UNIF_PAIRS_1_IN_G1(._22(A, ._22(B, Pairs))) -> IF_UNIF_PAIRS_1_IN_1_G4(A, B, Pairs, unif_2_in_gg2(A, B))
UNIF_PAIRS_1_IN_G1(._22(A, ._22(B, Pairs))) -> UNIF_2_IN_GG2(A, B)
IF_UNIF_PAIRS_1_IN_1_G4(A, B, Pairs, unif_2_out_gg2(A, B)) -> IF_UNIF_PAIRS_1_IN_2_G4(A, B, Pairs, unif_pairs_1_in_g1(Pairs))
IF_UNIF_PAIRS_1_IN_1_G4(A, B, Pairs, unif_2_out_gg2(A, B)) -> UNIF_PAIRS_1_IN_G1(Pairs)
IF_UNIF_LINES_2_IN_1_GG7(W, X, L1s, Y, Z, L2s, unif_pairs_1_out_g1(._22(W, ._22(X, ._22(Y, ._22(Z, ._22(W, ._22(Y, ._22(X, ._22(Z, ._22(W, ._22(Z, ._22(X, ._22(Y, []_0)))))))))))))) -> IF_UNIF_LINES_2_IN_2_GG7(W, X, L1s, Y, Z, L2s, unif_lines_2_in_gg2(._22(X, L1s), ._22(Z, L2s)))
IF_UNIF_LINES_2_IN_1_GG7(W, X, L1s, Y, Z, L2s, unif_pairs_1_out_g1(._22(W, ._22(X, ._22(Y, ._22(Z, ._22(W, ._22(Y, ._22(X, ._22(Z, ._22(W, ._22(Z, ._22(X, ._22(Y, []_0)))))))))))))) -> UNIF_LINES_2_IN_GG2(._22(X, L1s), ._22(Z, L2s))
IF_UNIF_MATRX_1_IN_1_G4(L1, L2, Ls, unif_lines_2_out_gg2(L1, L2)) -> IF_UNIF_MATRX_1_IN_2_G4(L1, L2, Ls, unif_matrx_1_in_g1(._22(L2, Ls)))
IF_UNIF_MATRX_1_IN_1_G4(L1, L2, Ls, unif_lines_2_out_gg2(L1, L2)) -> UNIF_MATRX_1_IN_G1(._22(L2, Ls))

The TRS R consists of the following rules:

shapes_2_in_ga2(Matrix, N) -> if_shapes_2_in_1_ga3(Matrix, N, varmat_2_in_ga2(Matrix, MatrixWithVars))
varmat_2_in_ga2([]_0, []_0) -> varmat_2_out_ga2([]_0, []_0)
varmat_2_in_ga2(._22(L, Ls), ._22(VL, VLs)) -> if_varmat_2_in_1_ga5(L, Ls, VL, VLs, varmat_2_in_ga2(L, VL))
varmat_2_in_ga2(._22(black_0, Xs), ._22(black_0, VXs)) -> if_varmat_2_in_3_ga3(Xs, VXs, varmat_2_in_ga2(Xs, VXs))
varmat_2_in_ga2(._22(white_0, Xs), ._22(w_11(underscore), VXs)) -> if_varmat_2_in_4_ga4(Xs, underscore, VXs, varmat_2_in_ga2(Xs, VXs))
if_varmat_2_in_4_ga4(Xs, underscore, VXs, varmat_2_out_ga2(Xs, VXs)) -> varmat_2_out_ga2(._22(white_0, Xs), ._22(w_11(underscore), VXs))
if_varmat_2_in_3_ga3(Xs, VXs, varmat_2_out_ga2(Xs, VXs)) -> varmat_2_out_ga2(._22(black_0, Xs), ._22(black_0, VXs))
if_varmat_2_in_1_ga5(L, Ls, VL, VLs, varmat_2_out_ga2(L, VL)) -> if_varmat_2_in_2_ga5(L, Ls, VL, VLs, varmat_2_in_ga2(Ls, VLs))
if_varmat_2_in_2_ga5(L, Ls, VL, VLs, varmat_2_out_ga2(Ls, VLs)) -> varmat_2_out_ga2(._22(L, Ls), ._22(VL, VLs))
if_shapes_2_in_1_ga3(Matrix, N, varmat_2_out_ga2(Matrix, MatrixWithVars)) -> if_shapes_2_in_2_ga4(Matrix, N, MatrixWithVars, unif_matrx_1_in_g1(MatrixWithVars))
unif_matrx_1_in_g1(._22(L1, ._22(L2, Ls))) -> if_unif_matrx_1_in_1_g4(L1, L2, Ls, unif_lines_2_in_gg2(L1, L2))
unif_lines_2_in_gg2(._22(W, ._22(X, L1s)), ._22(Y, ._22(Z, L2s))) -> if_unif_lines_2_in_1_gg7(W, X, L1s, Y, Z, L2s, unif_pairs_1_in_g1(._22(W, ._22(X, ._22(Y, ._22(Z, ._22(W, ._22(Y, ._22(X, ._22(Z, ._22(W, ._22(Z, ._22(X, ._22(Y, []_0))))))))))))))
unif_pairs_1_in_g1([]_0) -> unif_pairs_1_out_g1([]_0)
unif_pairs_1_in_g1(._22(A, ._22(B, Pairs))) -> if_unif_pairs_1_in_1_g4(A, B, Pairs, unif_2_in_gg2(A, B))
unif_2_in_gg2(w_11(A), w_11(A)) -> unif_2_out_gg2(w_11(A), w_11(A))
unif_2_in_gg2(black_0, black_0) -> unif_2_out_gg2(black_0, black_0)
unif_2_in_gg2(black_0, w_11(underscore4)) -> unif_2_out_gg2(black_0, w_11(underscore4))
unif_2_in_gg2(w_11(underscore5), black_0) -> unif_2_out_gg2(w_11(underscore5), black_0)
if_unif_pairs_1_in_1_g4(A, B, Pairs, unif_2_out_gg2(A, B)) -> if_unif_pairs_1_in_2_g4(A, B, Pairs, unif_pairs_1_in_g1(Pairs))
if_unif_pairs_1_in_2_g4(A, B, Pairs, unif_pairs_1_out_g1(Pairs)) -> unif_pairs_1_out_g1(._22(A, ._22(B, Pairs)))
if_unif_lines_2_in_1_gg7(W, X, L1s, Y, Z, L2s, unif_pairs_1_out_g1(._22(W, ._22(X, ._22(Y, ._22(Z, ._22(W, ._22(Y, ._22(X, ._22(Z, ._22(W, ._22(Z, ._22(X, ._22(Y, []_0)))))))))))))) -> if_unif_lines_2_in_2_gg7(W, X, L1s, Y, Z, L2s, unif_lines_2_in_gg2(._22(X, L1s), ._22(Z, L2s)))
unif_lines_2_in_gg2(._22(underscore2, []_0), ._22(underscore3, []_0)) -> unif_lines_2_out_gg2(._22(underscore2, []_0), ._22(underscore3, []_0))
if_unif_lines_2_in_2_gg7(W, X, L1s, Y, Z, L2s, unif_lines_2_out_gg2(._22(X, L1s), ._22(Z, L2s))) -> unif_lines_2_out_gg2(._22(W, ._22(X, L1s)), ._22(Y, ._22(Z, L2s)))
if_unif_matrx_1_in_1_g4(L1, L2, Ls, unif_lines_2_out_gg2(L1, L2)) -> if_unif_matrx_1_in_2_g4(L1, L2, Ls, unif_matrx_1_in_g1(._22(L2, Ls)))
unif_matrx_1_in_g1(._22(underscore1, []_0)) -> unif_matrx_1_out_g1(._22(underscore1, []_0))
if_unif_matrx_1_in_2_g4(L1, L2, Ls, unif_matrx_1_out_g1(._22(L2, Ls))) -> unif_matrx_1_out_g1(._22(L1, ._22(L2, Ls)))
if_shapes_2_in_2_ga4(Matrix, N, MatrixWithVars, unif_matrx_1_out_g1(MatrixWithVars)) -> shapes_2_out_ga2(Matrix, N)

The argument filtering Pi contains the following mapping:
shapes_2_in_ga2(x1, x2)  =  shapes_2_in_ga1(x1)
[]_0  =  []_0
._22(x1, x2)  =  ._22(x1, x2)
black_0  =  black_0
white_0  =  white_0
w_11(x1)  =  w_1
if_shapes_2_in_1_ga3(x1, x2, x3)  =  if_shapes_2_in_1_ga1(x3)
varmat_2_in_ga2(x1, x2)  =  varmat_2_in_ga1(x1)
varmat_2_out_ga2(x1, x2)  =  varmat_2_out_ga1(x2)
if_varmat_2_in_1_ga5(x1, x2, x3, x4, x5)  =  if_varmat_2_in_1_ga2(x2, x5)
if_varmat_2_in_3_ga3(x1, x2, x3)  =  if_varmat_2_in_3_ga1(x3)
if_varmat_2_in_4_ga4(x1, x2, x3, x4)  =  if_varmat_2_in_4_ga1(x4)
if_varmat_2_in_2_ga5(x1, x2, x3, x4, x5)  =  if_varmat_2_in_2_ga2(x3, x5)
if_shapes_2_in_2_ga4(x1, x2, x3, x4)  =  if_shapes_2_in_2_ga1(x4)
unif_matrx_1_in_g1(x1)  =  unif_matrx_1_in_g1(x1)
if_unif_matrx_1_in_1_g4(x1, x2, x3, x4)  =  if_unif_matrx_1_in_1_g3(x2, x3, x4)
unif_lines_2_in_gg2(x1, x2)  =  unif_lines_2_in_gg2(x1, x2)
if_unif_lines_2_in_1_gg7(x1, x2, x3, x4, x5, x6, x7)  =  if_unif_lines_2_in_1_gg5(x2, x3, x5, x6, x7)
unif_pairs_1_in_g1(x1)  =  unif_pairs_1_in_g1(x1)
unif_pairs_1_out_g1(x1)  =  unif_pairs_1_out_g
if_unif_pairs_1_in_1_g4(x1, x2, x3, x4)  =  if_unif_pairs_1_in_1_g2(x3, x4)
unif_2_in_gg2(x1, x2)  =  unif_2_in_gg2(x1, x2)
unif_2_out_gg2(x1, x2)  =  unif_2_out_gg
if_unif_pairs_1_in_2_g4(x1, x2, x3, x4)  =  if_unif_pairs_1_in_2_g1(x4)
if_unif_lines_2_in_2_gg7(x1, x2, x3, x4, x5, x6, x7)  =  if_unif_lines_2_in_2_gg1(x7)
unif_lines_2_out_gg2(x1, x2)  =  unif_lines_2_out_gg
if_unif_matrx_1_in_2_g4(x1, x2, x3, x4)  =  if_unif_matrx_1_in_2_g1(x4)
unif_matrx_1_out_g1(x1)  =  unif_matrx_1_out_g
shapes_2_out_ga2(x1, x2)  =  shapes_2_out_ga
VARMAT_2_IN_GA2(x1, x2)  =  VARMAT_2_IN_GA1(x1)
IF_UNIF_LINES_2_IN_1_GG7(x1, x2, x3, x4, x5, x6, x7)  =  IF_UNIF_LINES_2_IN_1_GG5(x2, x3, x5, x6, x7)
IF_VARMAT_2_IN_2_GA5(x1, x2, x3, x4, x5)  =  IF_VARMAT_2_IN_2_GA2(x3, x5)
IF_SHAPES_2_IN_2_GA4(x1, x2, x3, x4)  =  IF_SHAPES_2_IN_2_GA1(x4)
UNIF_MATRX_1_IN_G1(x1)  =  UNIF_MATRX_1_IN_G1(x1)
IF_VARMAT_2_IN_1_GA5(x1, x2, x3, x4, x5)  =  IF_VARMAT_2_IN_1_GA2(x2, x5)
IF_UNIF_LINES_2_IN_2_GG7(x1, x2, x3, x4, x5, x6, x7)  =  IF_UNIF_LINES_2_IN_2_GG1(x7)
IF_SHAPES_2_IN_1_GA3(x1, x2, x3)  =  IF_SHAPES_2_IN_1_GA1(x3)
IF_VARMAT_2_IN_3_GA3(x1, x2, x3)  =  IF_VARMAT_2_IN_3_GA1(x3)
IF_UNIF_PAIRS_1_IN_2_G4(x1, x2, x3, x4)  =  IF_UNIF_PAIRS_1_IN_2_G1(x4)
IF_UNIF_MATRX_1_IN_1_G4(x1, x2, x3, x4)  =  IF_UNIF_MATRX_1_IN_1_G3(x2, x3, x4)
UNIF_2_IN_GG2(x1, x2)  =  UNIF_2_IN_GG2(x1, x2)
IF_UNIF_PAIRS_1_IN_1_G4(x1, x2, x3, x4)  =  IF_UNIF_PAIRS_1_IN_1_G2(x3, x4)
SHAPES_2_IN_GA2(x1, x2)  =  SHAPES_2_IN_GA1(x1)
IF_VARMAT_2_IN_4_GA4(x1, x2, x3, x4)  =  IF_VARMAT_2_IN_4_GA1(x4)
UNIF_LINES_2_IN_GG2(x1, x2)  =  UNIF_LINES_2_IN_GG2(x1, x2)
IF_UNIF_MATRX_1_IN_2_G4(x1, x2, x3, x4)  =  IF_UNIF_MATRX_1_IN_2_G1(x4)
UNIF_PAIRS_1_IN_G1(x1)  =  UNIF_PAIRS_1_IN_G1(x1)

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

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

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

IF_UNIF_PAIRS_1_IN_1_G4(A, B, Pairs, unif_2_out_gg2(A, B)) -> UNIF_PAIRS_1_IN_G1(Pairs)
UNIF_PAIRS_1_IN_G1(._22(A, ._22(B, Pairs))) -> IF_UNIF_PAIRS_1_IN_1_G4(A, B, Pairs, unif_2_in_gg2(A, B))

The TRS R consists of the following rules:

shapes_2_in_ga2(Matrix, N) -> if_shapes_2_in_1_ga3(Matrix, N, varmat_2_in_ga2(Matrix, MatrixWithVars))
varmat_2_in_ga2([]_0, []_0) -> varmat_2_out_ga2([]_0, []_0)
varmat_2_in_ga2(._22(L, Ls), ._22(VL, VLs)) -> if_varmat_2_in_1_ga5(L, Ls, VL, VLs, varmat_2_in_ga2(L, VL))
varmat_2_in_ga2(._22(black_0, Xs), ._22(black_0, VXs)) -> if_varmat_2_in_3_ga3(Xs, VXs, varmat_2_in_ga2(Xs, VXs))
varmat_2_in_ga2(._22(white_0, Xs), ._22(w_11(underscore), VXs)) -> if_varmat_2_in_4_ga4(Xs, underscore, VXs, varmat_2_in_ga2(Xs, VXs))
if_varmat_2_in_4_ga4(Xs, underscore, VXs, varmat_2_out_ga2(Xs, VXs)) -> varmat_2_out_ga2(._22(white_0, Xs), ._22(w_11(underscore), VXs))
if_varmat_2_in_3_ga3(Xs, VXs, varmat_2_out_ga2(Xs, VXs)) -> varmat_2_out_ga2(._22(black_0, Xs), ._22(black_0, VXs))
if_varmat_2_in_1_ga5(L, Ls, VL, VLs, varmat_2_out_ga2(L, VL)) -> if_varmat_2_in_2_ga5(L, Ls, VL, VLs, varmat_2_in_ga2(Ls, VLs))
if_varmat_2_in_2_ga5(L, Ls, VL, VLs, varmat_2_out_ga2(Ls, VLs)) -> varmat_2_out_ga2(._22(L, Ls), ._22(VL, VLs))
if_shapes_2_in_1_ga3(Matrix, N, varmat_2_out_ga2(Matrix, MatrixWithVars)) -> if_shapes_2_in_2_ga4(Matrix, N, MatrixWithVars, unif_matrx_1_in_g1(MatrixWithVars))
unif_matrx_1_in_g1(._22(L1, ._22(L2, Ls))) -> if_unif_matrx_1_in_1_g4(L1, L2, Ls, unif_lines_2_in_gg2(L1, L2))
unif_lines_2_in_gg2(._22(W, ._22(X, L1s)), ._22(Y, ._22(Z, L2s))) -> if_unif_lines_2_in_1_gg7(W, X, L1s, Y, Z, L2s, unif_pairs_1_in_g1(._22(W, ._22(X, ._22(Y, ._22(Z, ._22(W, ._22(Y, ._22(X, ._22(Z, ._22(W, ._22(Z, ._22(X, ._22(Y, []_0))))))))))))))
unif_pairs_1_in_g1([]_0) -> unif_pairs_1_out_g1([]_0)
unif_pairs_1_in_g1(._22(A, ._22(B, Pairs))) -> if_unif_pairs_1_in_1_g4(A, B, Pairs, unif_2_in_gg2(A, B))
unif_2_in_gg2(w_11(A), w_11(A)) -> unif_2_out_gg2(w_11(A), w_11(A))
unif_2_in_gg2(black_0, black_0) -> unif_2_out_gg2(black_0, black_0)
unif_2_in_gg2(black_0, w_11(underscore4)) -> unif_2_out_gg2(black_0, w_11(underscore4))
unif_2_in_gg2(w_11(underscore5), black_0) -> unif_2_out_gg2(w_11(underscore5), black_0)
if_unif_pairs_1_in_1_g4(A, B, Pairs, unif_2_out_gg2(A, B)) -> if_unif_pairs_1_in_2_g4(A, B, Pairs, unif_pairs_1_in_g1(Pairs))
if_unif_pairs_1_in_2_g4(A, B, Pairs, unif_pairs_1_out_g1(Pairs)) -> unif_pairs_1_out_g1(._22(A, ._22(B, Pairs)))
if_unif_lines_2_in_1_gg7(W, X, L1s, Y, Z, L2s, unif_pairs_1_out_g1(._22(W, ._22(X, ._22(Y, ._22(Z, ._22(W, ._22(Y, ._22(X, ._22(Z, ._22(W, ._22(Z, ._22(X, ._22(Y, []_0)))))))))))))) -> if_unif_lines_2_in_2_gg7(W, X, L1s, Y, Z, L2s, unif_lines_2_in_gg2(._22(X, L1s), ._22(Z, L2s)))
unif_lines_2_in_gg2(._22(underscore2, []_0), ._22(underscore3, []_0)) -> unif_lines_2_out_gg2(._22(underscore2, []_0), ._22(underscore3, []_0))
if_unif_lines_2_in_2_gg7(W, X, L1s, Y, Z, L2s, unif_lines_2_out_gg2(._22(X, L1s), ._22(Z, L2s))) -> unif_lines_2_out_gg2(._22(W, ._22(X, L1s)), ._22(Y, ._22(Z, L2s)))
if_unif_matrx_1_in_1_g4(L1, L2, Ls, unif_lines_2_out_gg2(L1, L2)) -> if_unif_matrx_1_in_2_g4(L1, L2, Ls, unif_matrx_1_in_g1(._22(L2, Ls)))
unif_matrx_1_in_g1(._22(underscore1, []_0)) -> unif_matrx_1_out_g1(._22(underscore1, []_0))
if_unif_matrx_1_in_2_g4(L1, L2, Ls, unif_matrx_1_out_g1(._22(L2, Ls))) -> unif_matrx_1_out_g1(._22(L1, ._22(L2, Ls)))
if_shapes_2_in_2_ga4(Matrix, N, MatrixWithVars, unif_matrx_1_out_g1(MatrixWithVars)) -> shapes_2_out_ga2(Matrix, N)

The argument filtering Pi contains the following mapping:
shapes_2_in_ga2(x1, x2)  =  shapes_2_in_ga1(x1)
[]_0  =  []_0
._22(x1, x2)  =  ._22(x1, x2)
black_0  =  black_0
white_0  =  white_0
w_11(x1)  =  w_1
if_shapes_2_in_1_ga3(x1, x2, x3)  =  if_shapes_2_in_1_ga1(x3)
varmat_2_in_ga2(x1, x2)  =  varmat_2_in_ga1(x1)
varmat_2_out_ga2(x1, x2)  =  varmat_2_out_ga1(x2)
if_varmat_2_in_1_ga5(x1, x2, x3, x4, x5)  =  if_varmat_2_in_1_ga2(x2, x5)
if_varmat_2_in_3_ga3(x1, x2, x3)  =  if_varmat_2_in_3_ga1(x3)
if_varmat_2_in_4_ga4(x1, x2, x3, x4)  =  if_varmat_2_in_4_ga1(x4)
if_varmat_2_in_2_ga5(x1, x2, x3, x4, x5)  =  if_varmat_2_in_2_ga2(x3, x5)
if_shapes_2_in_2_ga4(x1, x2, x3, x4)  =  if_shapes_2_in_2_ga1(x4)
unif_matrx_1_in_g1(x1)  =  unif_matrx_1_in_g1(x1)
if_unif_matrx_1_in_1_g4(x1, x2, x3, x4)  =  if_unif_matrx_1_in_1_g3(x2, x3, x4)
unif_lines_2_in_gg2(x1, x2)  =  unif_lines_2_in_gg2(x1, x2)
if_unif_lines_2_in_1_gg7(x1, x2, x3, x4, x5, x6, x7)  =  if_unif_lines_2_in_1_gg5(x2, x3, x5, x6, x7)
unif_pairs_1_in_g1(x1)  =  unif_pairs_1_in_g1(x1)
unif_pairs_1_out_g1(x1)  =  unif_pairs_1_out_g
if_unif_pairs_1_in_1_g4(x1, x2, x3, x4)  =  if_unif_pairs_1_in_1_g2(x3, x4)
unif_2_in_gg2(x1, x2)  =  unif_2_in_gg2(x1, x2)
unif_2_out_gg2(x1, x2)  =  unif_2_out_gg
if_unif_pairs_1_in_2_g4(x1, x2, x3, x4)  =  if_unif_pairs_1_in_2_g1(x4)
if_unif_lines_2_in_2_gg7(x1, x2, x3, x4, x5, x6, x7)  =  if_unif_lines_2_in_2_gg1(x7)
unif_lines_2_out_gg2(x1, x2)  =  unif_lines_2_out_gg
if_unif_matrx_1_in_2_g4(x1, x2, x3, x4)  =  if_unif_matrx_1_in_2_g1(x4)
unif_matrx_1_out_g1(x1)  =  unif_matrx_1_out_g
shapes_2_out_ga2(x1, x2)  =  shapes_2_out_ga
IF_UNIF_PAIRS_1_IN_1_G4(x1, x2, x3, x4)  =  IF_UNIF_PAIRS_1_IN_1_G2(x3, x4)
UNIF_PAIRS_1_IN_G1(x1)  =  UNIF_PAIRS_1_IN_G1(x1)

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
              ↳ PiDP
              ↳ PiDP

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

IF_UNIF_PAIRS_1_IN_1_G4(A, B, Pairs, unif_2_out_gg2(A, B)) -> UNIF_PAIRS_1_IN_G1(Pairs)
UNIF_PAIRS_1_IN_G1(._22(A, ._22(B, Pairs))) -> IF_UNIF_PAIRS_1_IN_1_G4(A, B, Pairs, unif_2_in_gg2(A, B))

The TRS R consists of the following rules:

unif_2_in_gg2(w_11(A), w_11(A)) -> unif_2_out_gg2(w_11(A), w_11(A))
unif_2_in_gg2(black_0, black_0) -> unif_2_out_gg2(black_0, black_0)
unif_2_in_gg2(black_0, w_11(underscore4)) -> unif_2_out_gg2(black_0, w_11(underscore4))
unif_2_in_gg2(w_11(underscore5), black_0) -> unif_2_out_gg2(w_11(underscore5), black_0)

The argument filtering Pi contains the following mapping:
._22(x1, x2)  =  ._22(x1, x2)
black_0  =  black_0
w_11(x1)  =  w_1
unif_2_in_gg2(x1, x2)  =  unif_2_in_gg2(x1, x2)
unif_2_out_gg2(x1, x2)  =  unif_2_out_gg
IF_UNIF_PAIRS_1_IN_1_G4(x1, x2, x3, x4)  =  IF_UNIF_PAIRS_1_IN_1_G2(x3, x4)
UNIF_PAIRS_1_IN_G1(x1)  =  UNIF_PAIRS_1_IN_G1(x1)

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
              ↳ PiDP
              ↳ PiDP

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

IF_UNIF_PAIRS_1_IN_1_G2(Pairs, unif_2_out_gg) -> UNIF_PAIRS_1_IN_G1(Pairs)
UNIF_PAIRS_1_IN_G1(._22(A, ._22(B, Pairs))) -> IF_UNIF_PAIRS_1_IN_1_G2(Pairs, unif_2_in_gg2(A, B))

The TRS R consists of the following rules:

unif_2_in_gg2(w_1, w_1) -> unif_2_out_gg
unif_2_in_gg2(black_0, black_0) -> unif_2_out_gg
unif_2_in_gg2(black_0, w_1) -> unif_2_out_gg
unif_2_in_gg2(w_1, black_0) -> unif_2_out_gg

The set Q consists of the following terms:

unif_2_in_gg2(x0, x1)

We have to consider all (P,Q,R)-chains.
The head symbols of this DP problem are {UNIF_PAIRS_1_IN_G1, IF_UNIF_PAIRS_1_IN_1_G2}.
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: 



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

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

IF_UNIF_LINES_2_IN_1_GG7(W, X, L1s, Y, Z, L2s, unif_pairs_1_out_g1(._22(W, ._22(X, ._22(Y, ._22(Z, ._22(W, ._22(Y, ._22(X, ._22(Z, ._22(W, ._22(Z, ._22(X, ._22(Y, []_0)))))))))))))) -> UNIF_LINES_2_IN_GG2(._22(X, L1s), ._22(Z, L2s))
UNIF_LINES_2_IN_GG2(._22(W, ._22(X, L1s)), ._22(Y, ._22(Z, L2s))) -> IF_UNIF_LINES_2_IN_1_GG7(W, X, L1s, Y, Z, L2s, unif_pairs_1_in_g1(._22(W, ._22(X, ._22(Y, ._22(Z, ._22(W, ._22(Y, ._22(X, ._22(Z, ._22(W, ._22(Z, ._22(X, ._22(Y, []_0))))))))))))))

The TRS R consists of the following rules:

shapes_2_in_ga2(Matrix, N) -> if_shapes_2_in_1_ga3(Matrix, N, varmat_2_in_ga2(Matrix, MatrixWithVars))
varmat_2_in_ga2([]_0, []_0) -> varmat_2_out_ga2([]_0, []_0)
varmat_2_in_ga2(._22(L, Ls), ._22(VL, VLs)) -> if_varmat_2_in_1_ga5(L, Ls, VL, VLs, varmat_2_in_ga2(L, VL))
varmat_2_in_ga2(._22(black_0, Xs), ._22(black_0, VXs)) -> if_varmat_2_in_3_ga3(Xs, VXs, varmat_2_in_ga2(Xs, VXs))
varmat_2_in_ga2(._22(white_0, Xs), ._22(w_11(underscore), VXs)) -> if_varmat_2_in_4_ga4(Xs, underscore, VXs, varmat_2_in_ga2(Xs, VXs))
if_varmat_2_in_4_ga4(Xs, underscore, VXs, varmat_2_out_ga2(Xs, VXs)) -> varmat_2_out_ga2(._22(white_0, Xs), ._22(w_11(underscore), VXs))
if_varmat_2_in_3_ga3(Xs, VXs, varmat_2_out_ga2(Xs, VXs)) -> varmat_2_out_ga2(._22(black_0, Xs), ._22(black_0, VXs))
if_varmat_2_in_1_ga5(L, Ls, VL, VLs, varmat_2_out_ga2(L, VL)) -> if_varmat_2_in_2_ga5(L, Ls, VL, VLs, varmat_2_in_ga2(Ls, VLs))
if_varmat_2_in_2_ga5(L, Ls, VL, VLs, varmat_2_out_ga2(Ls, VLs)) -> varmat_2_out_ga2(._22(L, Ls), ._22(VL, VLs))
if_shapes_2_in_1_ga3(Matrix, N, varmat_2_out_ga2(Matrix, MatrixWithVars)) -> if_shapes_2_in_2_ga4(Matrix, N, MatrixWithVars, unif_matrx_1_in_g1(MatrixWithVars))
unif_matrx_1_in_g1(._22(L1, ._22(L2, Ls))) -> if_unif_matrx_1_in_1_g4(L1, L2, Ls, unif_lines_2_in_gg2(L1, L2))
unif_lines_2_in_gg2(._22(W, ._22(X, L1s)), ._22(Y, ._22(Z, L2s))) -> if_unif_lines_2_in_1_gg7(W, X, L1s, Y, Z, L2s, unif_pairs_1_in_g1(._22(W, ._22(X, ._22(Y, ._22(Z, ._22(W, ._22(Y, ._22(X, ._22(Z, ._22(W, ._22(Z, ._22(X, ._22(Y, []_0))))))))))))))
unif_pairs_1_in_g1([]_0) -> unif_pairs_1_out_g1([]_0)
unif_pairs_1_in_g1(._22(A, ._22(B, Pairs))) -> if_unif_pairs_1_in_1_g4(A, B, Pairs, unif_2_in_gg2(A, B))
unif_2_in_gg2(w_11(A), w_11(A)) -> unif_2_out_gg2(w_11(A), w_11(A))
unif_2_in_gg2(black_0, black_0) -> unif_2_out_gg2(black_0, black_0)
unif_2_in_gg2(black_0, w_11(underscore4)) -> unif_2_out_gg2(black_0, w_11(underscore4))
unif_2_in_gg2(w_11(underscore5), black_0) -> unif_2_out_gg2(w_11(underscore5), black_0)
if_unif_pairs_1_in_1_g4(A, B, Pairs, unif_2_out_gg2(A, B)) -> if_unif_pairs_1_in_2_g4(A, B, Pairs, unif_pairs_1_in_g1(Pairs))
if_unif_pairs_1_in_2_g4(A, B, Pairs, unif_pairs_1_out_g1(Pairs)) -> unif_pairs_1_out_g1(._22(A, ._22(B, Pairs)))
if_unif_lines_2_in_1_gg7(W, X, L1s, Y, Z, L2s, unif_pairs_1_out_g1(._22(W, ._22(X, ._22(Y, ._22(Z, ._22(W, ._22(Y, ._22(X, ._22(Z, ._22(W, ._22(Z, ._22(X, ._22(Y, []_0)))))))))))))) -> if_unif_lines_2_in_2_gg7(W, X, L1s, Y, Z, L2s, unif_lines_2_in_gg2(._22(X, L1s), ._22(Z, L2s)))
unif_lines_2_in_gg2(._22(underscore2, []_0), ._22(underscore3, []_0)) -> unif_lines_2_out_gg2(._22(underscore2, []_0), ._22(underscore3, []_0))
if_unif_lines_2_in_2_gg7(W, X, L1s, Y, Z, L2s, unif_lines_2_out_gg2(._22(X, L1s), ._22(Z, L2s))) -> unif_lines_2_out_gg2(._22(W, ._22(X, L1s)), ._22(Y, ._22(Z, L2s)))
if_unif_matrx_1_in_1_g4(L1, L2, Ls, unif_lines_2_out_gg2(L1, L2)) -> if_unif_matrx_1_in_2_g4(L1, L2, Ls, unif_matrx_1_in_g1(._22(L2, Ls)))
unif_matrx_1_in_g1(._22(underscore1, []_0)) -> unif_matrx_1_out_g1(._22(underscore1, []_0))
if_unif_matrx_1_in_2_g4(L1, L2, Ls, unif_matrx_1_out_g1(._22(L2, Ls))) -> unif_matrx_1_out_g1(._22(L1, ._22(L2, Ls)))
if_shapes_2_in_2_ga4(Matrix, N, MatrixWithVars, unif_matrx_1_out_g1(MatrixWithVars)) -> shapes_2_out_ga2(Matrix, N)

The argument filtering Pi contains the following mapping:
shapes_2_in_ga2(x1, x2)  =  shapes_2_in_ga1(x1)
[]_0  =  []_0
._22(x1, x2)  =  ._22(x1, x2)
black_0  =  black_0
white_0  =  white_0
w_11(x1)  =  w_1
if_shapes_2_in_1_ga3(x1, x2, x3)  =  if_shapes_2_in_1_ga1(x3)
varmat_2_in_ga2(x1, x2)  =  varmat_2_in_ga1(x1)
varmat_2_out_ga2(x1, x2)  =  varmat_2_out_ga1(x2)
if_varmat_2_in_1_ga5(x1, x2, x3, x4, x5)  =  if_varmat_2_in_1_ga2(x2, x5)
if_varmat_2_in_3_ga3(x1, x2, x3)  =  if_varmat_2_in_3_ga1(x3)
if_varmat_2_in_4_ga4(x1, x2, x3, x4)  =  if_varmat_2_in_4_ga1(x4)
if_varmat_2_in_2_ga5(x1, x2, x3, x4, x5)  =  if_varmat_2_in_2_ga2(x3, x5)
if_shapes_2_in_2_ga4(x1, x2, x3, x4)  =  if_shapes_2_in_2_ga1(x4)
unif_matrx_1_in_g1(x1)  =  unif_matrx_1_in_g1(x1)
if_unif_matrx_1_in_1_g4(x1, x2, x3, x4)  =  if_unif_matrx_1_in_1_g3(x2, x3, x4)
unif_lines_2_in_gg2(x1, x2)  =  unif_lines_2_in_gg2(x1, x2)
if_unif_lines_2_in_1_gg7(x1, x2, x3, x4, x5, x6, x7)  =  if_unif_lines_2_in_1_gg5(x2, x3, x5, x6, x7)
unif_pairs_1_in_g1(x1)  =  unif_pairs_1_in_g1(x1)
unif_pairs_1_out_g1(x1)  =  unif_pairs_1_out_g
if_unif_pairs_1_in_1_g4(x1, x2, x3, x4)  =  if_unif_pairs_1_in_1_g2(x3, x4)
unif_2_in_gg2(x1, x2)  =  unif_2_in_gg2(x1, x2)
unif_2_out_gg2(x1, x2)  =  unif_2_out_gg
if_unif_pairs_1_in_2_g4(x1, x2, x3, x4)  =  if_unif_pairs_1_in_2_g1(x4)
if_unif_lines_2_in_2_gg7(x1, x2, x3, x4, x5, x6, x7)  =  if_unif_lines_2_in_2_gg1(x7)
unif_lines_2_out_gg2(x1, x2)  =  unif_lines_2_out_gg
if_unif_matrx_1_in_2_g4(x1, x2, x3, x4)  =  if_unif_matrx_1_in_2_g1(x4)
unif_matrx_1_out_g1(x1)  =  unif_matrx_1_out_g
shapes_2_out_ga2(x1, x2)  =  shapes_2_out_ga
IF_UNIF_LINES_2_IN_1_GG7(x1, x2, x3, x4, x5, x6, x7)  =  IF_UNIF_LINES_2_IN_1_GG5(x2, x3, x5, x6, x7)
UNIF_LINES_2_IN_GG2(x1, x2)  =  UNIF_LINES_2_IN_GG2(x1, x2)

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
              ↳ PiDP
              ↳ PiDP

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

IF_UNIF_LINES_2_IN_1_GG7(W, X, L1s, Y, Z, L2s, unif_pairs_1_out_g1(._22(W, ._22(X, ._22(Y, ._22(Z, ._22(W, ._22(Y, ._22(X, ._22(Z, ._22(W, ._22(Z, ._22(X, ._22(Y, []_0)))))))))))))) -> UNIF_LINES_2_IN_GG2(._22(X, L1s), ._22(Z, L2s))
UNIF_LINES_2_IN_GG2(._22(W, ._22(X, L1s)), ._22(Y, ._22(Z, L2s))) -> IF_UNIF_LINES_2_IN_1_GG7(W, X, L1s, Y, Z, L2s, unif_pairs_1_in_g1(._22(W, ._22(X, ._22(Y, ._22(Z, ._22(W, ._22(Y, ._22(X, ._22(Z, ._22(W, ._22(Z, ._22(X, ._22(Y, []_0))))))))))))))

The TRS R consists of the following rules:

unif_pairs_1_in_g1(._22(A, ._22(B, Pairs))) -> if_unif_pairs_1_in_1_g4(A, B, Pairs, unif_2_in_gg2(A, B))
if_unif_pairs_1_in_1_g4(A, B, Pairs, unif_2_out_gg2(A, B)) -> if_unif_pairs_1_in_2_g4(A, B, Pairs, unif_pairs_1_in_g1(Pairs))
unif_2_in_gg2(w_11(A), w_11(A)) -> unif_2_out_gg2(w_11(A), w_11(A))
unif_2_in_gg2(black_0, black_0) -> unif_2_out_gg2(black_0, black_0)
unif_2_in_gg2(black_0, w_11(underscore4)) -> unif_2_out_gg2(black_0, w_11(underscore4))
unif_2_in_gg2(w_11(underscore5), black_0) -> unif_2_out_gg2(w_11(underscore5), black_0)
if_unif_pairs_1_in_2_g4(A, B, Pairs, unif_pairs_1_out_g1(Pairs)) -> unif_pairs_1_out_g1(._22(A, ._22(B, Pairs)))
unif_pairs_1_in_g1([]_0) -> unif_pairs_1_out_g1([]_0)

The argument filtering Pi contains the following mapping:
[]_0  =  []_0
._22(x1, x2)  =  ._22(x1, x2)
black_0  =  black_0
w_11(x1)  =  w_1
unif_pairs_1_in_g1(x1)  =  unif_pairs_1_in_g1(x1)
unif_pairs_1_out_g1(x1)  =  unif_pairs_1_out_g
if_unif_pairs_1_in_1_g4(x1, x2, x3, x4)  =  if_unif_pairs_1_in_1_g2(x3, x4)
unif_2_in_gg2(x1, x2)  =  unif_2_in_gg2(x1, x2)
unif_2_out_gg2(x1, x2)  =  unif_2_out_gg
if_unif_pairs_1_in_2_g4(x1, x2, x3, x4)  =  if_unif_pairs_1_in_2_g1(x4)
IF_UNIF_LINES_2_IN_1_GG7(x1, x2, x3, x4, x5, x6, x7)  =  IF_UNIF_LINES_2_IN_1_GG5(x2, x3, x5, x6, x7)
UNIF_LINES_2_IN_GG2(x1, x2)  =  UNIF_LINES_2_IN_GG2(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
              ↳ PiDP
                ↳ UsableRulesProof
                  ↳ PiDP
                    ↳ PiDPToQDPProof
                      ↳ QDP
                        ↳ QDPPoloProof
              ↳ PiDP
              ↳ PiDP

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

IF_UNIF_LINES_2_IN_1_GG5(X, L1s, Z, L2s, unif_pairs_1_out_g) -> UNIF_LINES_2_IN_GG2(._22(X, L1s), ._22(Z, L2s))
UNIF_LINES_2_IN_GG2(._22(W, ._22(X, L1s)), ._22(Y, ._22(Z, L2s))) -> IF_UNIF_LINES_2_IN_1_GG5(X, L1s, Z, L2s, unif_pairs_1_in_g1(._22(W, ._22(X, ._22(Y, ._22(Z, ._22(W, ._22(Y, ._22(X, ._22(Z, ._22(W, ._22(Z, ._22(X, ._22(Y, []_0))))))))))))))

The TRS R consists of the following rules:

unif_pairs_1_in_g1(._22(A, ._22(B, Pairs))) -> if_unif_pairs_1_in_1_g2(Pairs, unif_2_in_gg2(A, B))
if_unif_pairs_1_in_1_g2(Pairs, unif_2_out_gg) -> if_unif_pairs_1_in_2_g1(unif_pairs_1_in_g1(Pairs))
unif_2_in_gg2(w_1, w_1) -> unif_2_out_gg
unif_2_in_gg2(black_0, black_0) -> unif_2_out_gg
unif_2_in_gg2(black_0, w_1) -> unif_2_out_gg
unif_2_in_gg2(w_1, black_0) -> unif_2_out_gg
if_unif_pairs_1_in_2_g1(unif_pairs_1_out_g) -> unif_pairs_1_out_g
unif_pairs_1_in_g1([]_0) -> unif_pairs_1_out_g

The set Q consists of the following terms:

unif_pairs_1_in_g1(x0)
if_unif_pairs_1_in_1_g2(x0, x1)
unif_2_in_gg2(x0, x1)
if_unif_pairs_1_in_2_g1(x0)

We have to consider all (P,Q,R)-chains.
The head symbols of this DP problem are {UNIF_LINES_2_IN_GG2, IF_UNIF_LINES_2_IN_1_GG5}.
By using a polynomial ordering, the following set of Dependency Pairs of this DP problem can be strictly oriented.

UNIF_LINES_2_IN_GG2(._22(W, ._22(X, L1s)), ._22(Y, ._22(Z, L2s))) -> IF_UNIF_LINES_2_IN_1_GG5(X, L1s, Z, L2s, unif_pairs_1_in_g1(._22(W, ._22(X, ._22(Y, ._22(Z, ._22(W, ._22(Y, ._22(X, ._22(Z, ._22(W, ._22(Z, ._22(X, ._22(Y, []_0))))))))))))))
The remaining Dependency Pairs were at least non-strictly be oriented.

IF_UNIF_LINES_2_IN_1_GG5(X, L1s, Z, L2s, unif_pairs_1_out_g) -> UNIF_LINES_2_IN_GG2(._22(X, L1s), ._22(Z, L2s))
With the implicit AFS there is no usable rule.

Used ordering: POLO with Polynomial interpretation:


POL(unif_2_in_gg2(x1, x2)) = 0   
POL(black_0) = 0   
POL(._22(x1, x2)) = 1 + x2   
POL(if_unif_pairs_1_in_2_g1(x1)) = 0   
POL(if_unif_pairs_1_in_1_g2(x1, x2)) = 0   
POL(unif_pairs_1_out_g) = 0   
POL(unif_2_out_gg) = 0   
POL(w_1) = 0   
POL(IF_UNIF_LINES_2_IN_1_GG5(x1, x2, x3, x4, x5)) = 1 + x2   
POL(UNIF_LINES_2_IN_GG2(x1, x2)) = x1   
POL([]_0) = 0   
POL(unif_pairs_1_in_g1(x1)) = 0   



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

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

IF_UNIF_LINES_2_IN_1_GG5(X, L1s, Z, L2s, unif_pairs_1_out_g) -> UNIF_LINES_2_IN_GG2(._22(X, L1s), ._22(Z, L2s))

The TRS R consists of the following rules:

unif_pairs_1_in_g1(._22(A, ._22(B, Pairs))) -> if_unif_pairs_1_in_1_g2(Pairs, unif_2_in_gg2(A, B))
if_unif_pairs_1_in_1_g2(Pairs, unif_2_out_gg) -> if_unif_pairs_1_in_2_g1(unif_pairs_1_in_g1(Pairs))
unif_2_in_gg2(w_1, w_1) -> unif_2_out_gg
unif_2_in_gg2(black_0, black_0) -> unif_2_out_gg
unif_2_in_gg2(black_0, w_1) -> unif_2_out_gg
unif_2_in_gg2(w_1, black_0) -> unif_2_out_gg
if_unif_pairs_1_in_2_g1(unif_pairs_1_out_g) -> unif_pairs_1_out_g
unif_pairs_1_in_g1([]_0) -> unif_pairs_1_out_g

The set Q consists of the following terms:

unif_pairs_1_in_g1(x0)
if_unif_pairs_1_in_1_g2(x0, x1)
unif_2_in_gg2(x0, x1)
if_unif_pairs_1_in_2_g1(x0)

We have to consider all (P,Q,R)-chains.
The head symbols of this DP problem are {UNIF_LINES_2_IN_GG2, IF_UNIF_LINES_2_IN_1_GG5}.
The approximation of the Dependency Graph contains 0 SCCs with 1 less node.

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

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

IF_UNIF_MATRX_1_IN_1_G4(L1, L2, Ls, unif_lines_2_out_gg2(L1, L2)) -> UNIF_MATRX_1_IN_G1(._22(L2, Ls))
UNIF_MATRX_1_IN_G1(._22(L1, ._22(L2, Ls))) -> IF_UNIF_MATRX_1_IN_1_G4(L1, L2, Ls, unif_lines_2_in_gg2(L1, L2))

The TRS R consists of the following rules:

shapes_2_in_ga2(Matrix, N) -> if_shapes_2_in_1_ga3(Matrix, N, varmat_2_in_ga2(Matrix, MatrixWithVars))
varmat_2_in_ga2([]_0, []_0) -> varmat_2_out_ga2([]_0, []_0)
varmat_2_in_ga2(._22(L, Ls), ._22(VL, VLs)) -> if_varmat_2_in_1_ga5(L, Ls, VL, VLs, varmat_2_in_ga2(L, VL))
varmat_2_in_ga2(._22(black_0, Xs), ._22(black_0, VXs)) -> if_varmat_2_in_3_ga3(Xs, VXs, varmat_2_in_ga2(Xs, VXs))
varmat_2_in_ga2(._22(white_0, Xs), ._22(w_11(underscore), VXs)) -> if_varmat_2_in_4_ga4(Xs, underscore, VXs, varmat_2_in_ga2(Xs, VXs))
if_varmat_2_in_4_ga4(Xs, underscore, VXs, varmat_2_out_ga2(Xs, VXs)) -> varmat_2_out_ga2(._22(white_0, Xs), ._22(w_11(underscore), VXs))
if_varmat_2_in_3_ga3(Xs, VXs, varmat_2_out_ga2(Xs, VXs)) -> varmat_2_out_ga2(._22(black_0, Xs), ._22(black_0, VXs))
if_varmat_2_in_1_ga5(L, Ls, VL, VLs, varmat_2_out_ga2(L, VL)) -> if_varmat_2_in_2_ga5(L, Ls, VL, VLs, varmat_2_in_ga2(Ls, VLs))
if_varmat_2_in_2_ga5(L, Ls, VL, VLs, varmat_2_out_ga2(Ls, VLs)) -> varmat_2_out_ga2(._22(L, Ls), ._22(VL, VLs))
if_shapes_2_in_1_ga3(Matrix, N, varmat_2_out_ga2(Matrix, MatrixWithVars)) -> if_shapes_2_in_2_ga4(Matrix, N, MatrixWithVars, unif_matrx_1_in_g1(MatrixWithVars))
unif_matrx_1_in_g1(._22(L1, ._22(L2, Ls))) -> if_unif_matrx_1_in_1_g4(L1, L2, Ls, unif_lines_2_in_gg2(L1, L2))
unif_lines_2_in_gg2(._22(W, ._22(X, L1s)), ._22(Y, ._22(Z, L2s))) -> if_unif_lines_2_in_1_gg7(W, X, L1s, Y, Z, L2s, unif_pairs_1_in_g1(._22(W, ._22(X, ._22(Y, ._22(Z, ._22(W, ._22(Y, ._22(X, ._22(Z, ._22(W, ._22(Z, ._22(X, ._22(Y, []_0))))))))))))))
unif_pairs_1_in_g1([]_0) -> unif_pairs_1_out_g1([]_0)
unif_pairs_1_in_g1(._22(A, ._22(B, Pairs))) -> if_unif_pairs_1_in_1_g4(A, B, Pairs, unif_2_in_gg2(A, B))
unif_2_in_gg2(w_11(A), w_11(A)) -> unif_2_out_gg2(w_11(A), w_11(A))
unif_2_in_gg2(black_0, black_0) -> unif_2_out_gg2(black_0, black_0)
unif_2_in_gg2(black_0, w_11(underscore4)) -> unif_2_out_gg2(black_0, w_11(underscore4))
unif_2_in_gg2(w_11(underscore5), black_0) -> unif_2_out_gg2(w_11(underscore5), black_0)
if_unif_pairs_1_in_1_g4(A, B, Pairs, unif_2_out_gg2(A, B)) -> if_unif_pairs_1_in_2_g4(A, B, Pairs, unif_pairs_1_in_g1(Pairs))
if_unif_pairs_1_in_2_g4(A, B, Pairs, unif_pairs_1_out_g1(Pairs)) -> unif_pairs_1_out_g1(._22(A, ._22(B, Pairs)))
if_unif_lines_2_in_1_gg7(W, X, L1s, Y, Z, L2s, unif_pairs_1_out_g1(._22(W, ._22(X, ._22(Y, ._22(Z, ._22(W, ._22(Y, ._22(X, ._22(Z, ._22(W, ._22(Z, ._22(X, ._22(Y, []_0)))))))))))))) -> if_unif_lines_2_in_2_gg7(W, X, L1s, Y, Z, L2s, unif_lines_2_in_gg2(._22(X, L1s), ._22(Z, L2s)))
unif_lines_2_in_gg2(._22(underscore2, []_0), ._22(underscore3, []_0)) -> unif_lines_2_out_gg2(._22(underscore2, []_0), ._22(underscore3, []_0))
if_unif_lines_2_in_2_gg7(W, X, L1s, Y, Z, L2s, unif_lines_2_out_gg2(._22(X, L1s), ._22(Z, L2s))) -> unif_lines_2_out_gg2(._22(W, ._22(X, L1s)), ._22(Y, ._22(Z, L2s)))
if_unif_matrx_1_in_1_g4(L1, L2, Ls, unif_lines_2_out_gg2(L1, L2)) -> if_unif_matrx_1_in_2_g4(L1, L2, Ls, unif_matrx_1_in_g1(._22(L2, Ls)))
unif_matrx_1_in_g1(._22(underscore1, []_0)) -> unif_matrx_1_out_g1(._22(underscore1, []_0))
if_unif_matrx_1_in_2_g4(L1, L2, Ls, unif_matrx_1_out_g1(._22(L2, Ls))) -> unif_matrx_1_out_g1(._22(L1, ._22(L2, Ls)))
if_shapes_2_in_2_ga4(Matrix, N, MatrixWithVars, unif_matrx_1_out_g1(MatrixWithVars)) -> shapes_2_out_ga2(Matrix, N)

The argument filtering Pi contains the following mapping:
shapes_2_in_ga2(x1, x2)  =  shapes_2_in_ga1(x1)
[]_0  =  []_0
._22(x1, x2)  =  ._22(x1, x2)
black_0  =  black_0
white_0  =  white_0
w_11(x1)  =  w_1
if_shapes_2_in_1_ga3(x1, x2, x3)  =  if_shapes_2_in_1_ga1(x3)
varmat_2_in_ga2(x1, x2)  =  varmat_2_in_ga1(x1)
varmat_2_out_ga2(x1, x2)  =  varmat_2_out_ga1(x2)
if_varmat_2_in_1_ga5(x1, x2, x3, x4, x5)  =  if_varmat_2_in_1_ga2(x2, x5)
if_varmat_2_in_3_ga3(x1, x2, x3)  =  if_varmat_2_in_3_ga1(x3)
if_varmat_2_in_4_ga4(x1, x2, x3, x4)  =  if_varmat_2_in_4_ga1(x4)
if_varmat_2_in_2_ga5(x1, x2, x3, x4, x5)  =  if_varmat_2_in_2_ga2(x3, x5)
if_shapes_2_in_2_ga4(x1, x2, x3, x4)  =  if_shapes_2_in_2_ga1(x4)
unif_matrx_1_in_g1(x1)  =  unif_matrx_1_in_g1(x1)
if_unif_matrx_1_in_1_g4(x1, x2, x3, x4)  =  if_unif_matrx_1_in_1_g3(x2, x3, x4)
unif_lines_2_in_gg2(x1, x2)  =  unif_lines_2_in_gg2(x1, x2)
if_unif_lines_2_in_1_gg7(x1, x2, x3, x4, x5, x6, x7)  =  if_unif_lines_2_in_1_gg5(x2, x3, x5, x6, x7)
unif_pairs_1_in_g1(x1)  =  unif_pairs_1_in_g1(x1)
unif_pairs_1_out_g1(x1)  =  unif_pairs_1_out_g
if_unif_pairs_1_in_1_g4(x1, x2, x3, x4)  =  if_unif_pairs_1_in_1_g2(x3, x4)
unif_2_in_gg2(x1, x2)  =  unif_2_in_gg2(x1, x2)
unif_2_out_gg2(x1, x2)  =  unif_2_out_gg
if_unif_pairs_1_in_2_g4(x1, x2, x3, x4)  =  if_unif_pairs_1_in_2_g1(x4)
if_unif_lines_2_in_2_gg7(x1, x2, x3, x4, x5, x6, x7)  =  if_unif_lines_2_in_2_gg1(x7)
unif_lines_2_out_gg2(x1, x2)  =  unif_lines_2_out_gg
if_unif_matrx_1_in_2_g4(x1, x2, x3, x4)  =  if_unif_matrx_1_in_2_g1(x4)
unif_matrx_1_out_g1(x1)  =  unif_matrx_1_out_g
shapes_2_out_ga2(x1, x2)  =  shapes_2_out_ga
UNIF_MATRX_1_IN_G1(x1)  =  UNIF_MATRX_1_IN_G1(x1)
IF_UNIF_MATRX_1_IN_1_G4(x1, x2, x3, x4)  =  IF_UNIF_MATRX_1_IN_1_G3(x2, x3, 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
              ↳ PiDP
              ↳ PiDP
                ↳ UsableRulesProof
                  ↳ PiDP
                    ↳ PiDPToQDPProof
              ↳ PiDP

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

IF_UNIF_MATRX_1_IN_1_G4(L1, L2, Ls, unif_lines_2_out_gg2(L1, L2)) -> UNIF_MATRX_1_IN_G1(._22(L2, Ls))
UNIF_MATRX_1_IN_G1(._22(L1, ._22(L2, Ls))) -> IF_UNIF_MATRX_1_IN_1_G4(L1, L2, Ls, unif_lines_2_in_gg2(L1, L2))

The TRS R consists of the following rules:

unif_lines_2_in_gg2(._22(W, ._22(X, L1s)), ._22(Y, ._22(Z, L2s))) -> if_unif_lines_2_in_1_gg7(W, X, L1s, Y, Z, L2s, unif_pairs_1_in_g1(._22(W, ._22(X, ._22(Y, ._22(Z, ._22(W, ._22(Y, ._22(X, ._22(Z, ._22(W, ._22(Z, ._22(X, ._22(Y, []_0))))))))))))))
unif_lines_2_in_gg2(._22(underscore2, []_0), ._22(underscore3, []_0)) -> unif_lines_2_out_gg2(._22(underscore2, []_0), ._22(underscore3, []_0))
if_unif_lines_2_in_1_gg7(W, X, L1s, Y, Z, L2s, unif_pairs_1_out_g1(._22(W, ._22(X, ._22(Y, ._22(Z, ._22(W, ._22(Y, ._22(X, ._22(Z, ._22(W, ._22(Z, ._22(X, ._22(Y, []_0)))))))))))))) -> if_unif_lines_2_in_2_gg7(W, X, L1s, Y, Z, L2s, unif_lines_2_in_gg2(._22(X, L1s), ._22(Z, L2s)))
unif_pairs_1_in_g1(._22(A, ._22(B, Pairs))) -> if_unif_pairs_1_in_1_g4(A, B, Pairs, unif_2_in_gg2(A, B))
if_unif_lines_2_in_2_gg7(W, X, L1s, Y, Z, L2s, unif_lines_2_out_gg2(._22(X, L1s), ._22(Z, L2s))) -> unif_lines_2_out_gg2(._22(W, ._22(X, L1s)), ._22(Y, ._22(Z, L2s)))
if_unif_pairs_1_in_1_g4(A, B, Pairs, unif_2_out_gg2(A, B)) -> if_unif_pairs_1_in_2_g4(A, B, Pairs, unif_pairs_1_in_g1(Pairs))
unif_2_in_gg2(w_11(A), w_11(A)) -> unif_2_out_gg2(w_11(A), w_11(A))
unif_2_in_gg2(black_0, black_0) -> unif_2_out_gg2(black_0, black_0)
unif_2_in_gg2(black_0, w_11(underscore4)) -> unif_2_out_gg2(black_0, w_11(underscore4))
unif_2_in_gg2(w_11(underscore5), black_0) -> unif_2_out_gg2(w_11(underscore5), black_0)
if_unif_pairs_1_in_2_g4(A, B, Pairs, unif_pairs_1_out_g1(Pairs)) -> unif_pairs_1_out_g1(._22(A, ._22(B, Pairs)))
unif_pairs_1_in_g1([]_0) -> unif_pairs_1_out_g1([]_0)

The argument filtering Pi contains the following mapping:
[]_0  =  []_0
._22(x1, x2)  =  ._22(x1, x2)
black_0  =  black_0
w_11(x1)  =  w_1
unif_lines_2_in_gg2(x1, x2)  =  unif_lines_2_in_gg2(x1, x2)
if_unif_lines_2_in_1_gg7(x1, x2, x3, x4, x5, x6, x7)  =  if_unif_lines_2_in_1_gg5(x2, x3, x5, x6, x7)
unif_pairs_1_in_g1(x1)  =  unif_pairs_1_in_g1(x1)
unif_pairs_1_out_g1(x1)  =  unif_pairs_1_out_g
if_unif_pairs_1_in_1_g4(x1, x2, x3, x4)  =  if_unif_pairs_1_in_1_g2(x3, x4)
unif_2_in_gg2(x1, x2)  =  unif_2_in_gg2(x1, x2)
unif_2_out_gg2(x1, x2)  =  unif_2_out_gg
if_unif_pairs_1_in_2_g4(x1, x2, x3, x4)  =  if_unif_pairs_1_in_2_g1(x4)
if_unif_lines_2_in_2_gg7(x1, x2, x3, x4, x5, x6, x7)  =  if_unif_lines_2_in_2_gg1(x7)
unif_lines_2_out_gg2(x1, x2)  =  unif_lines_2_out_gg
UNIF_MATRX_1_IN_G1(x1)  =  UNIF_MATRX_1_IN_G1(x1)
IF_UNIF_MATRX_1_IN_1_G4(x1, x2, x3, x4)  =  IF_UNIF_MATRX_1_IN_1_G3(x2, x3, 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
              ↳ PiDP
              ↳ PiDP
                ↳ UsableRulesProof
                  ↳ PiDP
                    ↳ PiDPToQDPProof
                      ↳ QDP
                        ↳ QDPPoloProof
              ↳ PiDP

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

IF_UNIF_MATRX_1_IN_1_G3(L2, Ls, unif_lines_2_out_gg) -> UNIF_MATRX_1_IN_G1(._22(L2, Ls))
UNIF_MATRX_1_IN_G1(._22(L1, ._22(L2, Ls))) -> IF_UNIF_MATRX_1_IN_1_G3(L2, Ls, unif_lines_2_in_gg2(L1, L2))

The TRS R consists of the following rules:

unif_lines_2_in_gg2(._22(W, ._22(X, L1s)), ._22(Y, ._22(Z, L2s))) -> if_unif_lines_2_in_1_gg5(X, L1s, Z, L2s, unif_pairs_1_in_g1(._22(W, ._22(X, ._22(Y, ._22(Z, ._22(W, ._22(Y, ._22(X, ._22(Z, ._22(W, ._22(Z, ._22(X, ._22(Y, []_0))))))))))))))
unif_lines_2_in_gg2(._22(underscore2, []_0), ._22(underscore3, []_0)) -> unif_lines_2_out_gg
if_unif_lines_2_in_1_gg5(X, L1s, Z, L2s, unif_pairs_1_out_g) -> if_unif_lines_2_in_2_gg1(unif_lines_2_in_gg2(._22(X, L1s), ._22(Z, L2s)))
unif_pairs_1_in_g1(._22(A, ._22(B, Pairs))) -> if_unif_pairs_1_in_1_g2(Pairs, unif_2_in_gg2(A, B))
if_unif_lines_2_in_2_gg1(unif_lines_2_out_gg) -> unif_lines_2_out_gg
if_unif_pairs_1_in_1_g2(Pairs, unif_2_out_gg) -> if_unif_pairs_1_in_2_g1(unif_pairs_1_in_g1(Pairs))
unif_2_in_gg2(w_1, w_1) -> unif_2_out_gg
unif_2_in_gg2(black_0, black_0) -> unif_2_out_gg
unif_2_in_gg2(black_0, w_1) -> unif_2_out_gg
unif_2_in_gg2(w_1, black_0) -> unif_2_out_gg
if_unif_pairs_1_in_2_g1(unif_pairs_1_out_g) -> unif_pairs_1_out_g
unif_pairs_1_in_g1([]_0) -> unif_pairs_1_out_g

The set Q consists of the following terms:

unif_lines_2_in_gg2(x0, x1)
if_unif_lines_2_in_1_gg5(x0, x1, x2, x3, x4)
unif_pairs_1_in_g1(x0)
if_unif_lines_2_in_2_gg1(x0)
if_unif_pairs_1_in_1_g2(x0, x1)
unif_2_in_gg2(x0, x1)
if_unif_pairs_1_in_2_g1(x0)

We have to consider all (P,Q,R)-chains.
The head symbols of this DP problem are {UNIF_MATRX_1_IN_G1, IF_UNIF_MATRX_1_IN_1_G3}.
By using a polynomial ordering, the following set of Dependency Pairs of this DP problem can be strictly oriented.

IF_UNIF_MATRX_1_IN_1_G3(L2, Ls, unif_lines_2_out_gg) -> UNIF_MATRX_1_IN_G1(._22(L2, Ls))
The remaining Dependency Pairs were at least non-strictly be oriented.

UNIF_MATRX_1_IN_G1(._22(L1, ._22(L2, Ls))) -> IF_UNIF_MATRX_1_IN_1_G3(L2, Ls, unif_lines_2_in_gg2(L1, L2))
With the implicit AFS we had to orient the following set of usable rules non-strictly.

if_unif_lines_2_in_1_gg5(X, L1s, Z, L2s, unif_pairs_1_out_g) -> if_unif_lines_2_in_2_gg1(unif_lines_2_in_gg2(._22(X, L1s), ._22(Z, L2s)))
if_unif_lines_2_in_2_gg1(unif_lines_2_out_gg) -> unif_lines_2_out_gg
unif_lines_2_in_gg2(._22(W, ._22(X, L1s)), ._22(Y, ._22(Z, L2s))) -> if_unif_lines_2_in_1_gg5(X, L1s, Z, L2s, unif_pairs_1_in_g1(._22(W, ._22(X, ._22(Y, ._22(Z, ._22(W, ._22(Y, ._22(X, ._22(Z, ._22(W, ._22(Z, ._22(X, ._22(Y, []_0))))))))))))))
unif_lines_2_in_gg2(._22(underscore2, []_0), ._22(underscore3, []_0)) -> unif_lines_2_out_gg
Used ordering: POLO with Polynomial interpretation:

POL(black_0) = 0   
POL(if_unif_lines_2_in_2_gg1(x1)) = x1   
POL(unif_pairs_1_out_g) = 0   
POL(w_1) = 0   
POL(unif_2_out_gg) = 0   
POL([]_0) = 1   
POL(unif_2_in_gg2(x1, x2)) = 0   
POL(unif_lines_2_out_gg) = 1   
POL(._22(x1, x2)) = x1 + x2   
POL(if_unif_pairs_1_in_2_g1(x1)) = 0   
POL(if_unif_pairs_1_in_1_g2(x1, x2)) = 0   
POL(UNIF_MATRX_1_IN_G1(x1)) = x1   
POL(IF_UNIF_MATRX_1_IN_1_G3(x1, x2, x3)) = x1 + x2 + x3   
POL(unif_lines_2_in_gg2(x1, x2)) = x1   
POL(if_unif_lines_2_in_1_gg5(x1, x2, x3, x4, x5)) = x1 + x2   
POL(unif_pairs_1_in_g1(x1)) = 0   



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

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

UNIF_MATRX_1_IN_G1(._22(L1, ._22(L2, Ls))) -> IF_UNIF_MATRX_1_IN_1_G3(L2, Ls, unif_lines_2_in_gg2(L1, L2))

The TRS R consists of the following rules:

unif_lines_2_in_gg2(._22(W, ._22(X, L1s)), ._22(Y, ._22(Z, L2s))) -> if_unif_lines_2_in_1_gg5(X, L1s, Z, L2s, unif_pairs_1_in_g1(._22(W, ._22(X, ._22(Y, ._22(Z, ._22(W, ._22(Y, ._22(X, ._22(Z, ._22(W, ._22(Z, ._22(X, ._22(Y, []_0))))))))))))))
unif_lines_2_in_gg2(._22(underscore2, []_0), ._22(underscore3, []_0)) -> unif_lines_2_out_gg
if_unif_lines_2_in_1_gg5(X, L1s, Z, L2s, unif_pairs_1_out_g) -> if_unif_lines_2_in_2_gg1(unif_lines_2_in_gg2(._22(X, L1s), ._22(Z, L2s)))
unif_pairs_1_in_g1(._22(A, ._22(B, Pairs))) -> if_unif_pairs_1_in_1_g2(Pairs, unif_2_in_gg2(A, B))
if_unif_lines_2_in_2_gg1(unif_lines_2_out_gg) -> unif_lines_2_out_gg
if_unif_pairs_1_in_1_g2(Pairs, unif_2_out_gg) -> if_unif_pairs_1_in_2_g1(unif_pairs_1_in_g1(Pairs))
unif_2_in_gg2(w_1, w_1) -> unif_2_out_gg
unif_2_in_gg2(black_0, black_0) -> unif_2_out_gg
unif_2_in_gg2(black_0, w_1) -> unif_2_out_gg
unif_2_in_gg2(w_1, black_0) -> unif_2_out_gg
if_unif_pairs_1_in_2_g1(unif_pairs_1_out_g) -> unif_pairs_1_out_g
unif_pairs_1_in_g1([]_0) -> unif_pairs_1_out_g

The set Q consists of the following terms:

unif_lines_2_in_gg2(x0, x1)
if_unif_lines_2_in_1_gg5(x0, x1, x2, x3, x4)
unif_pairs_1_in_g1(x0)
if_unif_lines_2_in_2_gg1(x0)
if_unif_pairs_1_in_1_g2(x0, x1)
unif_2_in_gg2(x0, x1)
if_unif_pairs_1_in_2_g1(x0)

We have to consider all (P,Q,R)-chains.
The head symbols of this DP problem are {IF_UNIF_MATRX_1_IN_1_G3, UNIF_MATRX_1_IN_G1}.
The approximation of the Dependency Graph contains 0 SCCs with 1 less node.

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

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

VARMAT_2_IN_GA2(._22(L, Ls), ._22(VL, VLs)) -> IF_VARMAT_2_IN_1_GA5(L, Ls, VL, VLs, varmat_2_in_ga2(L, VL))
VARMAT_2_IN_GA2(._22(L, Ls), ._22(VL, VLs)) -> VARMAT_2_IN_GA2(L, VL)
VARMAT_2_IN_GA2(._22(white_0, Xs), ._22(w_11(underscore), VXs)) -> VARMAT_2_IN_GA2(Xs, VXs)
VARMAT_2_IN_GA2(._22(black_0, Xs), ._22(black_0, VXs)) -> VARMAT_2_IN_GA2(Xs, VXs)
IF_VARMAT_2_IN_1_GA5(L, Ls, VL, VLs, varmat_2_out_ga2(L, VL)) -> VARMAT_2_IN_GA2(Ls, VLs)

The TRS R consists of the following rules:

shapes_2_in_ga2(Matrix, N) -> if_shapes_2_in_1_ga3(Matrix, N, varmat_2_in_ga2(Matrix, MatrixWithVars))
varmat_2_in_ga2([]_0, []_0) -> varmat_2_out_ga2([]_0, []_0)
varmat_2_in_ga2(._22(L, Ls), ._22(VL, VLs)) -> if_varmat_2_in_1_ga5(L, Ls, VL, VLs, varmat_2_in_ga2(L, VL))
varmat_2_in_ga2(._22(black_0, Xs), ._22(black_0, VXs)) -> if_varmat_2_in_3_ga3(Xs, VXs, varmat_2_in_ga2(Xs, VXs))
varmat_2_in_ga2(._22(white_0, Xs), ._22(w_11(underscore), VXs)) -> if_varmat_2_in_4_ga4(Xs, underscore, VXs, varmat_2_in_ga2(Xs, VXs))
if_varmat_2_in_4_ga4(Xs, underscore, VXs, varmat_2_out_ga2(Xs, VXs)) -> varmat_2_out_ga2(._22(white_0, Xs), ._22(w_11(underscore), VXs))
if_varmat_2_in_3_ga3(Xs, VXs, varmat_2_out_ga2(Xs, VXs)) -> varmat_2_out_ga2(._22(black_0, Xs), ._22(black_0, VXs))
if_varmat_2_in_1_ga5(L, Ls, VL, VLs, varmat_2_out_ga2(L, VL)) -> if_varmat_2_in_2_ga5(L, Ls, VL, VLs, varmat_2_in_ga2(Ls, VLs))
if_varmat_2_in_2_ga5(L, Ls, VL, VLs, varmat_2_out_ga2(Ls, VLs)) -> varmat_2_out_ga2(._22(L, Ls), ._22(VL, VLs))
if_shapes_2_in_1_ga3(Matrix, N, varmat_2_out_ga2(Matrix, MatrixWithVars)) -> if_shapes_2_in_2_ga4(Matrix, N, MatrixWithVars, unif_matrx_1_in_g1(MatrixWithVars))
unif_matrx_1_in_g1(._22(L1, ._22(L2, Ls))) -> if_unif_matrx_1_in_1_g4(L1, L2, Ls, unif_lines_2_in_gg2(L1, L2))
unif_lines_2_in_gg2(._22(W, ._22(X, L1s)), ._22(Y, ._22(Z, L2s))) -> if_unif_lines_2_in_1_gg7(W, X, L1s, Y, Z, L2s, unif_pairs_1_in_g1(._22(W, ._22(X, ._22(Y, ._22(Z, ._22(W, ._22(Y, ._22(X, ._22(Z, ._22(W, ._22(Z, ._22(X, ._22(Y, []_0))))))))))))))
unif_pairs_1_in_g1([]_0) -> unif_pairs_1_out_g1([]_0)
unif_pairs_1_in_g1(._22(A, ._22(B, Pairs))) -> if_unif_pairs_1_in_1_g4(A, B, Pairs, unif_2_in_gg2(A, B))
unif_2_in_gg2(w_11(A), w_11(A)) -> unif_2_out_gg2(w_11(A), w_11(A))
unif_2_in_gg2(black_0, black_0) -> unif_2_out_gg2(black_0, black_0)
unif_2_in_gg2(black_0, w_11(underscore4)) -> unif_2_out_gg2(black_0, w_11(underscore4))
unif_2_in_gg2(w_11(underscore5), black_0) -> unif_2_out_gg2(w_11(underscore5), black_0)
if_unif_pairs_1_in_1_g4(A, B, Pairs, unif_2_out_gg2(A, B)) -> if_unif_pairs_1_in_2_g4(A, B, Pairs, unif_pairs_1_in_g1(Pairs))
if_unif_pairs_1_in_2_g4(A, B, Pairs, unif_pairs_1_out_g1(Pairs)) -> unif_pairs_1_out_g1(._22(A, ._22(B, Pairs)))
if_unif_lines_2_in_1_gg7(W, X, L1s, Y, Z, L2s, unif_pairs_1_out_g1(._22(W, ._22(X, ._22(Y, ._22(Z, ._22(W, ._22(Y, ._22(X, ._22(Z, ._22(W, ._22(Z, ._22(X, ._22(Y, []_0)))))))))))))) -> if_unif_lines_2_in_2_gg7(W, X, L1s, Y, Z, L2s, unif_lines_2_in_gg2(._22(X, L1s), ._22(Z, L2s)))
unif_lines_2_in_gg2(._22(underscore2, []_0), ._22(underscore3, []_0)) -> unif_lines_2_out_gg2(._22(underscore2, []_0), ._22(underscore3, []_0))
if_unif_lines_2_in_2_gg7(W, X, L1s, Y, Z, L2s, unif_lines_2_out_gg2(._22(X, L1s), ._22(Z, L2s))) -> unif_lines_2_out_gg2(._22(W, ._22(X, L1s)), ._22(Y, ._22(Z, L2s)))
if_unif_matrx_1_in_1_g4(L1, L2, Ls, unif_lines_2_out_gg2(L1, L2)) -> if_unif_matrx_1_in_2_g4(L1, L2, Ls, unif_matrx_1_in_g1(._22(L2, Ls)))
unif_matrx_1_in_g1(._22(underscore1, []_0)) -> unif_matrx_1_out_g1(._22(underscore1, []_0))
if_unif_matrx_1_in_2_g4(L1, L2, Ls, unif_matrx_1_out_g1(._22(L2, Ls))) -> unif_matrx_1_out_g1(._22(L1, ._22(L2, Ls)))
if_shapes_2_in_2_ga4(Matrix, N, MatrixWithVars, unif_matrx_1_out_g1(MatrixWithVars)) -> shapes_2_out_ga2(Matrix, N)

The argument filtering Pi contains the following mapping:
shapes_2_in_ga2(x1, x2)  =  shapes_2_in_ga1(x1)
[]_0  =  []_0
._22(x1, x2)  =  ._22(x1, x2)
black_0  =  black_0
white_0  =  white_0
w_11(x1)  =  w_1
if_shapes_2_in_1_ga3(x1, x2, x3)  =  if_shapes_2_in_1_ga1(x3)
varmat_2_in_ga2(x1, x2)  =  varmat_2_in_ga1(x1)
varmat_2_out_ga2(x1, x2)  =  varmat_2_out_ga1(x2)
if_varmat_2_in_1_ga5(x1, x2, x3, x4, x5)  =  if_varmat_2_in_1_ga2(x2, x5)
if_varmat_2_in_3_ga3(x1, x2, x3)  =  if_varmat_2_in_3_ga1(x3)
if_varmat_2_in_4_ga4(x1, x2, x3, x4)  =  if_varmat_2_in_4_ga1(x4)
if_varmat_2_in_2_ga5(x1, x2, x3, x4, x5)  =  if_varmat_2_in_2_ga2(x3, x5)
if_shapes_2_in_2_ga4(x1, x2, x3, x4)  =  if_shapes_2_in_2_ga1(x4)
unif_matrx_1_in_g1(x1)  =  unif_matrx_1_in_g1(x1)
if_unif_matrx_1_in_1_g4(x1, x2, x3, x4)  =  if_unif_matrx_1_in_1_g3(x2, x3, x4)
unif_lines_2_in_gg2(x1, x2)  =  unif_lines_2_in_gg2(x1, x2)
if_unif_lines_2_in_1_gg7(x1, x2, x3, x4, x5, x6, x7)  =  if_unif_lines_2_in_1_gg5(x2, x3, x5, x6, x7)
unif_pairs_1_in_g1(x1)  =  unif_pairs_1_in_g1(x1)
unif_pairs_1_out_g1(x1)  =  unif_pairs_1_out_g
if_unif_pairs_1_in_1_g4(x1, x2, x3, x4)  =  if_unif_pairs_1_in_1_g2(x3, x4)
unif_2_in_gg2(x1, x2)  =  unif_2_in_gg2(x1, x2)
unif_2_out_gg2(x1, x2)  =  unif_2_out_gg
if_unif_pairs_1_in_2_g4(x1, x2, x3, x4)  =  if_unif_pairs_1_in_2_g1(x4)
if_unif_lines_2_in_2_gg7(x1, x2, x3, x4, x5, x6, x7)  =  if_unif_lines_2_in_2_gg1(x7)
unif_lines_2_out_gg2(x1, x2)  =  unif_lines_2_out_gg
if_unif_matrx_1_in_2_g4(x1, x2, x3, x4)  =  if_unif_matrx_1_in_2_g1(x4)
unif_matrx_1_out_g1(x1)  =  unif_matrx_1_out_g
shapes_2_out_ga2(x1, x2)  =  shapes_2_out_ga
VARMAT_2_IN_GA2(x1, x2)  =  VARMAT_2_IN_GA1(x1)
IF_VARMAT_2_IN_1_GA5(x1, x2, x3, x4, x5)  =  IF_VARMAT_2_IN_1_GA2(x2, x5)

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
              ↳ PiDP
              ↳ PiDP
                ↳ UsableRulesProof
                  ↳ PiDP
                    ↳ PiDPToQDPProof

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

VARMAT_2_IN_GA2(._22(L, Ls), ._22(VL, VLs)) -> IF_VARMAT_2_IN_1_GA5(L, Ls, VL, VLs, varmat_2_in_ga2(L, VL))
VARMAT_2_IN_GA2(._22(L, Ls), ._22(VL, VLs)) -> VARMAT_2_IN_GA2(L, VL)
VARMAT_2_IN_GA2(._22(white_0, Xs), ._22(w_11(underscore), VXs)) -> VARMAT_2_IN_GA2(Xs, VXs)
VARMAT_2_IN_GA2(._22(black_0, Xs), ._22(black_0, VXs)) -> VARMAT_2_IN_GA2(Xs, VXs)
IF_VARMAT_2_IN_1_GA5(L, Ls, VL, VLs, varmat_2_out_ga2(L, VL)) -> VARMAT_2_IN_GA2(Ls, VLs)

The TRS R consists of the following rules:

varmat_2_in_ga2([]_0, []_0) -> varmat_2_out_ga2([]_0, []_0)
varmat_2_in_ga2(._22(L, Ls), ._22(VL, VLs)) -> if_varmat_2_in_1_ga5(L, Ls, VL, VLs, varmat_2_in_ga2(L, VL))
varmat_2_in_ga2(._22(black_0, Xs), ._22(black_0, VXs)) -> if_varmat_2_in_3_ga3(Xs, VXs, varmat_2_in_ga2(Xs, VXs))
varmat_2_in_ga2(._22(white_0, Xs), ._22(w_11(underscore), VXs)) -> if_varmat_2_in_4_ga4(Xs, underscore, VXs, varmat_2_in_ga2(Xs, VXs))
if_varmat_2_in_1_ga5(L, Ls, VL, VLs, varmat_2_out_ga2(L, VL)) -> if_varmat_2_in_2_ga5(L, Ls, VL, VLs, varmat_2_in_ga2(Ls, VLs))
if_varmat_2_in_3_ga3(Xs, VXs, varmat_2_out_ga2(Xs, VXs)) -> varmat_2_out_ga2(._22(black_0, Xs), ._22(black_0, VXs))
if_varmat_2_in_4_ga4(Xs, underscore, VXs, varmat_2_out_ga2(Xs, VXs)) -> varmat_2_out_ga2(._22(white_0, Xs), ._22(w_11(underscore), VXs))
if_varmat_2_in_2_ga5(L, Ls, VL, VLs, varmat_2_out_ga2(Ls, VLs)) -> varmat_2_out_ga2(._22(L, Ls), ._22(VL, VLs))

The argument filtering Pi contains the following mapping:
[]_0  =  []_0
._22(x1, x2)  =  ._22(x1, x2)
black_0  =  black_0
white_0  =  white_0
w_11(x1)  =  w_1
varmat_2_in_ga2(x1, x2)  =  varmat_2_in_ga1(x1)
varmat_2_out_ga2(x1, x2)  =  varmat_2_out_ga1(x2)
if_varmat_2_in_1_ga5(x1, x2, x3, x4, x5)  =  if_varmat_2_in_1_ga2(x2, x5)
if_varmat_2_in_3_ga3(x1, x2, x3)  =  if_varmat_2_in_3_ga1(x3)
if_varmat_2_in_4_ga4(x1, x2, x3, x4)  =  if_varmat_2_in_4_ga1(x4)
if_varmat_2_in_2_ga5(x1, x2, x3, x4, x5)  =  if_varmat_2_in_2_ga2(x3, x5)
VARMAT_2_IN_GA2(x1, x2)  =  VARMAT_2_IN_GA1(x1)
IF_VARMAT_2_IN_1_GA5(x1, x2, x3, x4, x5)  =  IF_VARMAT_2_IN_1_GA2(x2, x5)

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
              ↳ PiDP
              ↳ PiDP
                ↳ UsableRulesProof
                  ↳ PiDP
                    ↳ PiDPToQDPProof
                      ↳ QDP
                        ↳ QDPSizeChangeProof

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

VARMAT_2_IN_GA1(._22(L, Ls)) -> IF_VARMAT_2_IN_1_GA2(Ls, varmat_2_in_ga1(L))
VARMAT_2_IN_GA1(._22(L, Ls)) -> VARMAT_2_IN_GA1(L)
VARMAT_2_IN_GA1(._22(white_0, Xs)) -> VARMAT_2_IN_GA1(Xs)
VARMAT_2_IN_GA1(._22(black_0, Xs)) -> VARMAT_2_IN_GA1(Xs)
IF_VARMAT_2_IN_1_GA2(Ls, varmat_2_out_ga1(VL)) -> VARMAT_2_IN_GA1(Ls)

The TRS R consists of the following rules:

varmat_2_in_ga1([]_0) -> varmat_2_out_ga1([]_0)
varmat_2_in_ga1(._22(L, Ls)) -> if_varmat_2_in_1_ga2(Ls, varmat_2_in_ga1(L))
varmat_2_in_ga1(._22(black_0, Xs)) -> if_varmat_2_in_3_ga1(varmat_2_in_ga1(Xs))
varmat_2_in_ga1(._22(white_0, Xs)) -> if_varmat_2_in_4_ga1(varmat_2_in_ga1(Xs))
if_varmat_2_in_1_ga2(Ls, varmat_2_out_ga1(VL)) -> if_varmat_2_in_2_ga2(VL, varmat_2_in_ga1(Ls))
if_varmat_2_in_3_ga1(varmat_2_out_ga1(VXs)) -> varmat_2_out_ga1(._22(black_0, VXs))
if_varmat_2_in_4_ga1(varmat_2_out_ga1(VXs)) -> varmat_2_out_ga1(._22(w_1, VXs))
if_varmat_2_in_2_ga2(VL, varmat_2_out_ga1(VLs)) -> varmat_2_out_ga1(._22(VL, VLs))

The set Q consists of the following terms:

varmat_2_in_ga1(x0)
if_varmat_2_in_1_ga2(x0, x1)
if_varmat_2_in_3_ga1(x0)
if_varmat_2_in_4_ga1(x0)
if_varmat_2_in_2_ga2(x0, x1)

We have to consider all (P,Q,R)-chains.
The head symbols of this DP problem are {IF_VARMAT_2_IN_1_GA2, VARMAT_2_IN_GA1}.
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: