Left Termination proof of ../tpdb/LP/lpexamples/shapes.pl

YES Left Termination proof of ../tpdb/LP/lpexamples/shapes.pl
Left Termination of the query pattern shapes_in_2(g, a) w.r.t. the given Prolog program could successfully be proven:

↳ Prolog

  ↳ PrologToPiTRSProof

Clauses:

shapes(Matrix, N) :- ','(varmat(Matrix, MatrixWithVars), unif_matrx(MatrixWithVars)).
varmat([], []).
varmat(.(L, Ls), .(VL, VLs)) :- ','(varmat(L, VL), varmat(Ls, VLs)).
varmat(.(black, Xs), .(black, VXs)) :- varmat(Xs, VXs).
varmat(.(white, Xs), .(w(X), VXs)) :- varmat(Xs, VXs).
unif_matrx(.(L1, .(L2, Ls))) :- ','(unif_lines(L1, L2), unif_matrx(.(L2, Ls))).
unif_matrx(.(X, [])).
unif_lines(.(W, .(X, L1s)), .(Y, .(Z, L2s))) :- ','(unif_pairs(.(W, .(X, .(Y, .(Z, .(W, .(Y, .(X, .(Z, .(W, .(Z, .(X, .(Y, []))))))))))))), unif_lines(.(X, L1s), .(Z, L2s))).
unif_lines(.(X, []), .(X1, [])).
unif_pairs([]).
unif_pairs(.(A, .(B, Pairs))) :- ','(unif(A, B), unif_pairs(Pairs)).
unif(w(A), w(A)).
unif(black, black).
unif(black, w(X)).
unif(w(X), black).

Queries:

shapes(g,a).

We use the technique of [30]. With regard to the inferred argument filtering the predicates were used in the following modes:
shapes_in: (b,f)
varmat_in: (b,f)
unif_matrx_in: (b)
unif_lines_in: (b,b)
unif_pairs_in: (b)
Transforming Prolog into the following Term Rewriting System:
Pi-finite rewrite system:
The TRS R consists of the following rules:

shapes_in_ga(Matrix, N) → U1_ga(Matrix, N, varmat_in_ga(Matrix, MatrixWithVars))
varmat_in_ga([], []) → varmat_out_ga([], [])
varmat_in_ga(.(L, Ls), .(VL, VLs)) → U3_ga(L, Ls, VL, VLs, varmat_in_ga(L, VL))
varmat_in_ga(.(black, Xs), .(black, VXs)) → U5_ga(Xs, VXs, varmat_in_ga(Xs, VXs))
varmat_in_ga(.(white, Xs), .(w(X), VXs)) → U6_ga(Xs, X, VXs, varmat_in_ga(Xs, VXs))
U6_ga(Xs, X, VXs, varmat_out_ga(Xs, VXs)) → varmat_out_ga(.(white, Xs), .(w(X), VXs))
U5_ga(Xs, VXs, varmat_out_ga(Xs, VXs)) → varmat_out_ga(.(black, Xs), .(black, VXs))
U3_ga(L, Ls, VL, VLs, varmat_out_ga(L, VL)) → U4_ga(L, Ls, VL, VLs, varmat_in_ga(Ls, VLs))
U4_ga(L, Ls, VL, VLs, varmat_out_ga(Ls, VLs)) → varmat_out_ga(.(L, Ls), .(VL, VLs))
U1_ga(Matrix, N, varmat_out_ga(Matrix, MatrixWithVars)) → U2_ga(Matrix, N, unif_matrx_in_g(MatrixWithVars))
unif_matrx_in_g(.(L1, .(L2, Ls))) → U7_g(L1, L2, Ls, unif_lines_in_gg(L1, L2))
unif_lines_in_gg(.(W, .(X, L1s)), .(Y, .(Z, L2s))) → U9_gg(W, X, L1s, Y, Z, L2s, unif_pairs_in_g(.(W, .(X, .(Y, .(Z, .(W, .(Y, .(X, .(Z, .(W, .(Z, .(X, .(Y, []))))))))))))))
unif_pairs_in_g([]) → unif_pairs_out_g([])
unif_pairs_in_g(.(A, .(B, Pairs))) → U11_g(A, B, Pairs, unif_in_gg(A, B))
unif_in_gg(w(A), w(A)) → unif_out_gg(w(A), w(A))
unif_in_gg(black, black) → unif_out_gg(black, black)
unif_in_gg(black, w(X)) → unif_out_gg(black, w(X))
unif_in_gg(w(X), black) → unif_out_gg(w(X), black)
U11_g(A, B, Pairs, unif_out_gg(A, B)) → U12_g(A, B, Pairs, unif_pairs_in_g(Pairs))
U12_g(A, B, Pairs, unif_pairs_out_g(Pairs)) → unif_pairs_out_g(.(A, .(B, Pairs)))
U9_gg(W, X, L1s, Y, Z, L2s, unif_pairs_out_g(.(W, .(X, .(Y, .(Z, .(W, .(Y, .(X, .(Z, .(W, .(Z, .(X, .(Y, [])))))))))))))) → U10_gg(W, X, L1s, Y, Z, L2s, unif_lines_in_gg(.(X, L1s), .(Z, L2s)))
unif_lines_in_gg(.(X, []), .(X1, [])) → unif_lines_out_gg(.(X, []), .(X1, []))
U10_gg(W, X, L1s, Y, Z, L2s, unif_lines_out_gg(.(X, L1s), .(Z, L2s))) → unif_lines_out_gg(.(W, .(X, L1s)), .(Y, .(Z, L2s)))
U7_g(L1, L2, Ls, unif_lines_out_gg(L1, L2)) → U8_g(L1, L2, Ls, unif_matrx_in_g(.(L2, Ls)))
unif_matrx_in_g(.(X, [])) → unif_matrx_out_g(.(X, []))
U8_g(L1, L2, Ls, unif_matrx_out_g(.(L2, Ls))) → unif_matrx_out_g(.(L1, .(L2, Ls)))
U2_ga(Matrix, N, unif_matrx_out_g(MatrixWithVars)) → shapes_out_ga(Matrix, N)

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_in_ga(Matrix, N) → U1_ga(Matrix, N, varmat_in_ga(Matrix, MatrixWithVars))
varmat_in_ga([], []) → varmat_out_ga([], [])
varmat_in_ga(.(L, Ls), .(VL, VLs)) → U3_ga(L, Ls, VL, VLs, varmat_in_ga(L, VL))
varmat_in_ga(.(black, Xs), .(black, VXs)) → U5_ga(Xs, VXs, varmat_in_ga(Xs, VXs))
varmat_in_ga(.(white, Xs), .(w(X), VXs)) → U6_ga(Xs, X, VXs, varmat_in_ga(Xs, VXs))
U6_ga(Xs, X, VXs, varmat_out_ga(Xs, VXs)) → varmat_out_ga(.(white, Xs), .(w(X), VXs))
U5_ga(Xs, VXs, varmat_out_ga(Xs, VXs)) → varmat_out_ga(.(black, Xs), .(black, VXs))
U3_ga(L, Ls, VL, VLs, varmat_out_ga(L, VL)) → U4_ga(L, Ls, VL, VLs, varmat_in_ga(Ls, VLs))
U4_ga(L, Ls, VL, VLs, varmat_out_ga(Ls, VLs)) → varmat_out_ga(.(L, Ls), .(VL, VLs))
U1_ga(Matrix, N, varmat_out_ga(Matrix, MatrixWithVars)) → U2_ga(Matrix, N, unif_matrx_in_g(MatrixWithVars))
unif_matrx_in_g(.(L1, .(L2, Ls))) → U7_g(L1, L2, Ls, unif_lines_in_gg(L1, L2))
unif_lines_in_gg(.(W, .(X, L1s)), .(Y, .(Z, L2s))) → U9_gg(W, X, L1s, Y, Z, L2s, unif_pairs_in_g(.(W, .(X, .(Y, .(Z, .(W, .(Y, .(X, .(Z, .(W, .(Z, .(X, .(Y, []))))))))))))))
unif_pairs_in_g([]) → unif_pairs_out_g([])
unif_pairs_in_g(.(A, .(B, Pairs))) → U11_g(A, B, Pairs, unif_in_gg(A, B))
unif_in_gg(w(A), w(A)) → unif_out_gg(w(A), w(A))
unif_in_gg(black, black) → unif_out_gg(black, black)
unif_in_gg(black, w(X)) → unif_out_gg(black, w(X))
unif_in_gg(w(X), black) → unif_out_gg(w(X), black)
U11_g(A, B, Pairs, unif_out_gg(A, B)) → U12_g(A, B, Pairs, unif_pairs_in_g(Pairs))
U12_g(A, B, Pairs, unif_pairs_out_g(Pairs)) → unif_pairs_out_g(.(A, .(B, Pairs)))
U9_gg(W, X, L1s, Y, Z, L2s, unif_pairs_out_g(.(W, .(X, .(Y, .(Z, .(W, .(Y, .(X, .(Z, .(W, .(Z, .(X, .(Y, [])))))))))))))) → U10_gg(W, X, L1s, Y, Z, L2s, unif_lines_in_gg(.(X, L1s), .(Z, L2s)))
unif_lines_in_gg(.(X, []), .(X1, [])) → unif_lines_out_gg(.(X, []), .(X1, []))
U10_gg(W, X, L1s, Y, Z, L2s, unif_lines_out_gg(.(X, L1s), .(Z, L2s))) → unif_lines_out_gg(.(W, .(X, L1s)), .(Y, .(Z, L2s)))
U7_g(L1, L2, Ls, unif_lines_out_gg(L1, L2)) → U8_g(L1, L2, Ls, unif_matrx_in_g(.(L2, Ls)))
unif_matrx_in_g(.(X, [])) → unif_matrx_out_g(.(X, []))
U8_g(L1, L2, Ls, unif_matrx_out_g(.(L2, Ls))) → unif_matrx_out_g(.(L1, .(L2, Ls)))
U2_ga(Matrix, N, unif_matrx_out_g(MatrixWithVars)) → shapes_out_ga(Matrix, N)

SHAPES_IN_GA(Matrix, N) → U1_GA(Matrix, N, varmat_in_ga(Matrix, MatrixWithVars))
SHAPES_IN_GA(Matrix, N) → VARMAT_IN_GA(Matrix, MatrixWithVars)
VARMAT_IN_GA(.(L, Ls), .(VL, VLs)) → U3_GA(L, Ls, VL, VLs, varmat_in_ga(L, VL))
VARMAT_IN_GA(.(L, Ls), .(VL, VLs)) → VARMAT_IN_GA(L, VL)
VARMAT_IN_GA(.(black, Xs), .(black, VXs)) → U5_GA(Xs, VXs, varmat_in_ga(Xs, VXs))
VARMAT_IN_GA(.(black, Xs), .(black, VXs)) → VARMAT_IN_GA(Xs, VXs)
VARMAT_IN_GA(.(white, Xs), .(w(X), VXs)) → U6_GA(Xs, X, VXs, varmat_in_ga(Xs, VXs))
VARMAT_IN_GA(.(white, Xs), .(w(X), VXs)) → VARMAT_IN_GA(Xs, VXs)
U3_GA(L, Ls, VL, VLs, varmat_out_ga(L, VL)) → U4_GA(L, Ls, VL, VLs, varmat_in_ga(Ls, VLs))
U3_GA(L, Ls, VL, VLs, varmat_out_ga(L, VL)) → VARMAT_IN_GA(Ls, VLs)
U1_GA(Matrix, N, varmat_out_ga(Matrix, MatrixWithVars)) → U2_GA(Matrix, N, unif_matrx_in_g(MatrixWithVars))
U1_GA(Matrix, N, varmat_out_ga(Matrix, MatrixWithVars)) → UNIF_MATRX_IN_G(MatrixWithVars)
UNIF_MATRX_IN_G(.(L1, .(L2, Ls))) → U7_G(L1, L2, Ls, unif_lines_in_gg(L1, L2))
UNIF_MATRX_IN_G(.(L1, .(L2, Ls))) → UNIF_LINES_IN_GG(L1, L2)
UNIF_LINES_IN_GG(.(W, .(X, L1s)), .(Y, .(Z, L2s))) → U9_GG(W, X, L1s, Y, Z, L2s, unif_pairs_in_g(.(W, .(X, .(Y, .(Z, .(W, .(Y, .(X, .(Z, .(W, .(Z, .(X, .(Y, []))))))))))))))
UNIF_LINES_IN_GG(.(W, .(X, L1s)), .(Y, .(Z, L2s))) → UNIF_PAIRS_IN_G(.(W, .(X, .(Y, .(Z, .(W, .(Y, .(X, .(Z, .(W, .(Z, .(X, .(Y, [])))))))))))))
UNIF_PAIRS_IN_G(.(A, .(B, Pairs))) → U11_G(A, B, Pairs, unif_in_gg(A, B))
UNIF_PAIRS_IN_G(.(A, .(B, Pairs))) → UNIF_IN_GG(A, B)
U11_G(A, B, Pairs, unif_out_gg(A, B)) → U12_G(A, B, Pairs, unif_pairs_in_g(Pairs))
U11_G(A, B, Pairs, unif_out_gg(A, B)) → UNIF_PAIRS_IN_G(Pairs)
U9_GG(W, X, L1s, Y, Z, L2s, unif_pairs_out_g(.(W, .(X, .(Y, .(Z, .(W, .(Y, .(X, .(Z, .(W, .(Z, .(X, .(Y, [])))))))))))))) → U10_GG(W, X, L1s, Y, Z, L2s, unif_lines_in_gg(.(X, L1s), .(Z, L2s)))
U9_GG(W, X, L1s, Y, Z, L2s, unif_pairs_out_g(.(W, .(X, .(Y, .(Z, .(W, .(Y, .(X, .(Z, .(W, .(Z, .(X, .(Y, [])))))))))))))) → UNIF_LINES_IN_GG(.(X, L1s), .(Z, L2s))
U7_G(L1, L2, Ls, unif_lines_out_gg(L1, L2)) → U8_G(L1, L2, Ls, unif_matrx_in_g(.(L2, Ls)))
U7_G(L1, L2, Ls, unif_lines_out_gg(L1, L2)) → UNIF_MATRX_IN_G(.(L2, Ls))

The TRS R consists of the following rules:

shapes_in_ga(Matrix, N) → U1_ga(Matrix, N, varmat_in_ga(Matrix, MatrixWithVars))
varmat_in_ga([], []) → varmat_out_ga([], [])
varmat_in_ga(.(L, Ls), .(VL, VLs)) → U3_ga(L, Ls, VL, VLs, varmat_in_ga(L, VL))
varmat_in_ga(.(black, Xs), .(black, VXs)) → U5_ga(Xs, VXs, varmat_in_ga(Xs, VXs))
varmat_in_ga(.(white, Xs), .(w(X), VXs)) → U6_ga(Xs, X, VXs, varmat_in_ga(Xs, VXs))
U6_ga(Xs, X, VXs, varmat_out_ga(Xs, VXs)) → varmat_out_ga(.(white, Xs), .(w(X), VXs))
U5_ga(Xs, VXs, varmat_out_ga(Xs, VXs)) → varmat_out_ga(.(black, Xs), .(black, VXs))
U3_ga(L, Ls, VL, VLs, varmat_out_ga(L, VL)) → U4_ga(L, Ls, VL, VLs, varmat_in_ga(Ls, VLs))
U4_ga(L, Ls, VL, VLs, varmat_out_ga(Ls, VLs)) → varmat_out_ga(.(L, Ls), .(VL, VLs))
U1_ga(Matrix, N, varmat_out_ga(Matrix, MatrixWithVars)) → U2_ga(Matrix, N, unif_matrx_in_g(MatrixWithVars))
unif_matrx_in_g(.(L1, .(L2, Ls))) → U7_g(L1, L2, Ls, unif_lines_in_gg(L1, L2))
unif_lines_in_gg(.(W, .(X, L1s)), .(Y, .(Z, L2s))) → U9_gg(W, X, L1s, Y, Z, L2s, unif_pairs_in_g(.(W, .(X, .(Y, .(Z, .(W, .(Y, .(X, .(Z, .(W, .(Z, .(X, .(Y, []))))))))))))))
unif_pairs_in_g([]) → unif_pairs_out_g([])
unif_pairs_in_g(.(A, .(B, Pairs))) → U11_g(A, B, Pairs, unif_in_gg(A, B))
unif_in_gg(w(A), w(A)) → unif_out_gg(w(A), w(A))
unif_in_gg(black, black) → unif_out_gg(black, black)
unif_in_gg(black, w(X)) → unif_out_gg(black, w(X))
unif_in_gg(w(X), black) → unif_out_gg(w(X), black)
U11_g(A, B, Pairs, unif_out_gg(A, B)) → U12_g(A, B, Pairs, unif_pairs_in_g(Pairs))
U12_g(A, B, Pairs, unif_pairs_out_g(Pairs)) → unif_pairs_out_g(.(A, .(B, Pairs)))
U9_gg(W, X, L1s, Y, Z, L2s, unif_pairs_out_g(.(W, .(X, .(Y, .(Z, .(W, .(Y, .(X, .(Z, .(W, .(Z, .(X, .(Y, [])))))))))))))) → U10_gg(W, X, L1s, Y, Z, L2s, unif_lines_in_gg(.(X, L1s), .(Z, L2s)))
unif_lines_in_gg(.(X, []), .(X1, [])) → unif_lines_out_gg(.(X, []), .(X1, []))
U10_gg(W, X, L1s, Y, Z, L2s, unif_lines_out_gg(.(X, L1s), .(Z, L2s))) → unif_lines_out_gg(.(W, .(X, L1s)), .(Y, .(Z, L2s)))
U7_g(L1, L2, Ls, unif_lines_out_gg(L1, L2)) → U8_g(L1, L2, Ls, unif_matrx_in_g(.(L2, Ls)))
unif_matrx_in_g(.(X, [])) → unif_matrx_out_g(.(X, []))
U8_g(L1, L2, Ls, unif_matrx_out_g(.(L2, Ls))) → unif_matrx_out_g(.(L1, .(L2, Ls)))
U2_ga(Matrix, N, unif_matrx_out_g(MatrixWithVars)) → shapes_out_ga(Matrix, N)

The argument filtering Pi contains the following mapping:
shapes_in_ga(x1, x2) = shapes_in_ga(x1)
U1_ga(x1, x2, x3) = U1_ga(x3)
varmat_in_ga(x1, x2) = varmat_in_ga(x1)
[] = []
varmat_out_ga(x1, x2) = varmat_out_ga(x2)
.(x1, x2) = .(x1, x2)
U3_ga(x1, x2, x3, x4, x5) = U3_ga(x2, x5)
black = black
U5_ga(x1, x2, x3) = U5_ga(x3)
white = white
U6_ga(x1, x2, x3, x4) = U6_ga(x4)
w(x1) = w
U4_ga(x1, x2, x3, x4, x5) = U4_ga(x3, x5)
U2_ga(x1, x2, x3) = U2_ga(x3)
unif_matrx_in_g(x1) = unif_matrx_in_g(x1)
U7_g(x1, x2, x3, x4) = U7_g(x2, x3, x4)
unif_lines_in_gg(x1, x2) = unif_lines_in_gg(x1, x2)
U9_gg(x1, x2, x3, x4, x5, x6, x7) = U9_gg(x2, x3, x5, x6, x7)
unif_pairs_in_g(x1) = unif_pairs_in_g(x1)
unif_pairs_out_g(x1) = unif_pairs_out_g
U11_g(x1, x2, x3, x4) = U11_g(x3, x4)
unif_in_gg(x1, x2) = unif_in_gg(x1, x2)
unif_out_gg(x1, x2) = unif_out_gg
U12_g(x1, x2, x3, x4) = U12_g(x4)
U10_gg(x1, x2, x3, x4, x5, x6, x7) = U10_gg(x7)
unif_lines_out_gg(x1, x2) = unif_lines_out_gg
U8_g(x1, x2, x3, x4) = U8_g(x4)
unif_matrx_out_g(x1) = unif_matrx_out_g
shapes_out_ga(x1, x2) = shapes_out_ga
U6_GA(x1, x2, x3, x4) = U6_GA(x4)
U7_G(x1, x2, x3, x4) = U7_G(x2, x3, x4)
SHAPES_IN_GA(x1, x2) = SHAPES_IN_GA(x1)
U5_GA(x1, x2, x3) = U5_GA(x3)
U12_G(x1, x2, x3, x4) = U12_G(x4)
U4_GA(x1, x2, x3, x4, x5) = U4_GA(x3, x5)
U10_GG(x1, x2, x3, x4, x5, x6, x7) = U10_GG(x7)
UNIF_IN_GG(x1, x2) = UNIF_IN_GG(x1, x2)
U9_GG(x1, x2, x3, x4, x5, x6, x7) = U9_GG(x2, x3, x5, x6, x7)
UNIF_PAIRS_IN_G(x1) = UNIF_PAIRS_IN_G(x1)
VARMAT_IN_GA(x1, x2) = VARMAT_IN_GA(x1)
U8_G(x1, x2, x3, x4) = U8_G(x4)
U11_G(x1, x2, x3, x4) = U11_G(x3, x4)
UNIF_LINES_IN_GG(x1, x2) = UNIF_LINES_IN_GG(x1, x2)
U1_GA(x1, x2, x3) = U1_GA(x3)
U3_GA(x1, x2, x3, x4, x5) = U3_GA(x2, x5)
U2_GA(x1, x2, x3) = U2_GA(x3)
UNIF_MATRX_IN_G(x1) = UNIF_MATRX_IN_G(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_IN_GA(Matrix, N) → U1_GA(Matrix, N, varmat_in_ga(Matrix, MatrixWithVars))
SHAPES_IN_GA(Matrix, N) → VARMAT_IN_GA(Matrix, MatrixWithVars)
VARMAT_IN_GA(.(L, Ls), .(VL, VLs)) → U3_GA(L, Ls, VL, VLs, varmat_in_ga(L, VL))
VARMAT_IN_GA(.(L, Ls), .(VL, VLs)) → VARMAT_IN_GA(L, VL)
VARMAT_IN_GA(.(black, Xs), .(black, VXs)) → U5_GA(Xs, VXs, varmat_in_ga(Xs, VXs))
VARMAT_IN_GA(.(black, Xs), .(black, VXs)) → VARMAT_IN_GA(Xs, VXs)
VARMAT_IN_GA(.(white, Xs), .(w(X), VXs)) → U6_GA(Xs, X, VXs, varmat_in_ga(Xs, VXs))
VARMAT_IN_GA(.(white, Xs), .(w(X), VXs)) → VARMAT_IN_GA(Xs, VXs)
U3_GA(L, Ls, VL, VLs, varmat_out_ga(L, VL)) → U4_GA(L, Ls, VL, VLs, varmat_in_ga(Ls, VLs))
U3_GA(L, Ls, VL, VLs, varmat_out_ga(L, VL)) → VARMAT_IN_GA(Ls, VLs)
U1_GA(Matrix, N, varmat_out_ga(Matrix, MatrixWithVars)) → U2_GA(Matrix, N, unif_matrx_in_g(MatrixWithVars))
U1_GA(Matrix, N, varmat_out_ga(Matrix, MatrixWithVars)) → UNIF_MATRX_IN_G(MatrixWithVars)
UNIF_MATRX_IN_G(.(L1, .(L2, Ls))) → U7_G(L1, L2, Ls, unif_lines_in_gg(L1, L2))
UNIF_MATRX_IN_G(.(L1, .(L2, Ls))) → UNIF_LINES_IN_GG(L1, L2)
UNIF_LINES_IN_GG(.(W, .(X, L1s)), .(Y, .(Z, L2s))) → U9_GG(W, X, L1s, Y, Z, L2s, unif_pairs_in_g(.(W, .(X, .(Y, .(Z, .(W, .(Y, .(X, .(Z, .(W, .(Z, .(X, .(Y, []))))))))))))))
UNIF_LINES_IN_GG(.(W, .(X, L1s)), .(Y, .(Z, L2s))) → UNIF_PAIRS_IN_G(.(W, .(X, .(Y, .(Z, .(W, .(Y, .(X, .(Z, .(W, .(Z, .(X, .(Y, [])))))))))))))
UNIF_PAIRS_IN_G(.(A, .(B, Pairs))) → U11_G(A, B, Pairs, unif_in_gg(A, B))
UNIF_PAIRS_IN_G(.(A, .(B, Pairs))) → UNIF_IN_GG(A, B)
U11_G(A, B, Pairs, unif_out_gg(A, B)) → U12_G(A, B, Pairs, unif_pairs_in_g(Pairs))
U11_G(A, B, Pairs, unif_out_gg(A, B)) → UNIF_PAIRS_IN_G(Pairs)
U9_GG(W, X, L1s, Y, Z, L2s, unif_pairs_out_g(.(W, .(X, .(Y, .(Z, .(W, .(Y, .(X, .(Z, .(W, .(Z, .(X, .(Y, [])))))))))))))) → U10_GG(W, X, L1s, Y, Z, L2s, unif_lines_in_gg(.(X, L1s), .(Z, L2s)))
U9_GG(W, X, L1s, Y, Z, L2s, unif_pairs_out_g(.(W, .(X, .(Y, .(Z, .(W, .(Y, .(X, .(Z, .(W, .(Z, .(X, .(Y, [])))))))))))))) → UNIF_LINES_IN_GG(.(X, L1s), .(Z, L2s))
U7_G(L1, L2, Ls, unif_lines_out_gg(L1, L2)) → U8_G(L1, L2, Ls, unif_matrx_in_g(.(L2, Ls)))
U7_G(L1, L2, Ls, unif_lines_out_gg(L1, L2)) → UNIF_MATRX_IN_G(.(L2, Ls))

The TRS R consists of the following rules:

shapes_in_ga(Matrix, N) → U1_ga(Matrix, N, varmat_in_ga(Matrix, MatrixWithVars))
varmat_in_ga([], []) → varmat_out_ga([], [])
varmat_in_ga(.(L, Ls), .(VL, VLs)) → U3_ga(L, Ls, VL, VLs, varmat_in_ga(L, VL))
varmat_in_ga(.(black, Xs), .(black, VXs)) → U5_ga(Xs, VXs, varmat_in_ga(Xs, VXs))
varmat_in_ga(.(white, Xs), .(w(X), VXs)) → U6_ga(Xs, X, VXs, varmat_in_ga(Xs, VXs))
U6_ga(Xs, X, VXs, varmat_out_ga(Xs, VXs)) → varmat_out_ga(.(white, Xs), .(w(X), VXs))
U5_ga(Xs, VXs, varmat_out_ga(Xs, VXs)) → varmat_out_ga(.(black, Xs), .(black, VXs))
U3_ga(L, Ls, VL, VLs, varmat_out_ga(L, VL)) → U4_ga(L, Ls, VL, VLs, varmat_in_ga(Ls, VLs))
U4_ga(L, Ls, VL, VLs, varmat_out_ga(Ls, VLs)) → varmat_out_ga(.(L, Ls), .(VL, VLs))
U1_ga(Matrix, N, varmat_out_ga(Matrix, MatrixWithVars)) → U2_ga(Matrix, N, unif_matrx_in_g(MatrixWithVars))
unif_matrx_in_g(.(L1, .(L2, Ls))) → U7_g(L1, L2, Ls, unif_lines_in_gg(L1, L2))
unif_lines_in_gg(.(W, .(X, L1s)), .(Y, .(Z, L2s))) → U9_gg(W, X, L1s, Y, Z, L2s, unif_pairs_in_g(.(W, .(X, .(Y, .(Z, .(W, .(Y, .(X, .(Z, .(W, .(Z, .(X, .(Y, []))))))))))))))
unif_pairs_in_g([]) → unif_pairs_out_g([])
unif_pairs_in_g(.(A, .(B, Pairs))) → U11_g(A, B, Pairs, unif_in_gg(A, B))
unif_in_gg(w(A), w(A)) → unif_out_gg(w(A), w(A))
unif_in_gg(black, black) → unif_out_gg(black, black)
unif_in_gg(black, w(X)) → unif_out_gg(black, w(X))
unif_in_gg(w(X), black) → unif_out_gg(w(X), black)
U11_g(A, B, Pairs, unif_out_gg(A, B)) → U12_g(A, B, Pairs, unif_pairs_in_g(Pairs))
U12_g(A, B, Pairs, unif_pairs_out_g(Pairs)) → unif_pairs_out_g(.(A, .(B, Pairs)))
U9_gg(W, X, L1s, Y, Z, L2s, unif_pairs_out_g(.(W, .(X, .(Y, .(Z, .(W, .(Y, .(X, .(Z, .(W, .(Z, .(X, .(Y, [])))))))))))))) → U10_gg(W, X, L1s, Y, Z, L2s, unif_lines_in_gg(.(X, L1s), .(Z, L2s)))
unif_lines_in_gg(.(X, []), .(X1, [])) → unif_lines_out_gg(.(X, []), .(X1, []))
U10_gg(W, X, L1s, Y, Z, L2s, unif_lines_out_gg(.(X, L1s), .(Z, L2s))) → unif_lines_out_gg(.(W, .(X, L1s)), .(Y, .(Z, L2s)))
U7_g(L1, L2, Ls, unif_lines_out_gg(L1, L2)) → U8_g(L1, L2, Ls, unif_matrx_in_g(.(L2, Ls)))
unif_matrx_in_g(.(X, [])) → unif_matrx_out_g(.(X, []))
U8_g(L1, L2, Ls, unif_matrx_out_g(.(L2, Ls))) → unif_matrx_out_g(.(L1, .(L2, Ls)))
U2_ga(Matrix, N, unif_matrx_out_g(MatrixWithVars)) → shapes_out_ga(Matrix, N)

↳ Prolog

  ↳ PrologToPiTRSProof

    ↳ PiTRS

      ↳ DependencyPairsProof

        ↳ PiDP

          ↳ DependencyGraphProof

            ↳ AND

              ↳ PiDP

                ↳ UsableRulesProof

              ↳ PiDP

              ↳ PiDP

              ↳ PiDP

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

UNIF_PAIRS_IN_G(.(A, .(B, Pairs))) → U11_G(A, B, Pairs, unif_in_gg(A, B))
U11_G(A, B, Pairs, unif_out_gg(A, B)) → UNIF_PAIRS_IN_G(Pairs)

The TRS R consists of the following rules:

shapes_in_ga(Matrix, N) → U1_ga(Matrix, N, varmat_in_ga(Matrix, MatrixWithVars))
varmat_in_ga([], []) → varmat_out_ga([], [])
varmat_in_ga(.(L, Ls), .(VL, VLs)) → U3_ga(L, Ls, VL, VLs, varmat_in_ga(L, VL))
varmat_in_ga(.(black, Xs), .(black, VXs)) → U5_ga(Xs, VXs, varmat_in_ga(Xs, VXs))
varmat_in_ga(.(white, Xs), .(w(X), VXs)) → U6_ga(Xs, X, VXs, varmat_in_ga(Xs, VXs))
U6_ga(Xs, X, VXs, varmat_out_ga(Xs, VXs)) → varmat_out_ga(.(white, Xs), .(w(X), VXs))
U5_ga(Xs, VXs, varmat_out_ga(Xs, VXs)) → varmat_out_ga(.(black, Xs), .(black, VXs))
U3_ga(L, Ls, VL, VLs, varmat_out_ga(L, VL)) → U4_ga(L, Ls, VL, VLs, varmat_in_ga(Ls, VLs))
U4_ga(L, Ls, VL, VLs, varmat_out_ga(Ls, VLs)) → varmat_out_ga(.(L, Ls), .(VL, VLs))
U1_ga(Matrix, N, varmat_out_ga(Matrix, MatrixWithVars)) → U2_ga(Matrix, N, unif_matrx_in_g(MatrixWithVars))
unif_matrx_in_g(.(L1, .(L2, Ls))) → U7_g(L1, L2, Ls, unif_lines_in_gg(L1, L2))
unif_lines_in_gg(.(W, .(X, L1s)), .(Y, .(Z, L2s))) → U9_gg(W, X, L1s, Y, Z, L2s, unif_pairs_in_g(.(W, .(X, .(Y, .(Z, .(W, .(Y, .(X, .(Z, .(W, .(Z, .(X, .(Y, []))))))))))))))
unif_pairs_in_g([]) → unif_pairs_out_g([])
unif_pairs_in_g(.(A, .(B, Pairs))) → U11_g(A, B, Pairs, unif_in_gg(A, B))
unif_in_gg(w(A), w(A)) → unif_out_gg(w(A), w(A))
unif_in_gg(black, black) → unif_out_gg(black, black)
unif_in_gg(black, w(X)) → unif_out_gg(black, w(X))
unif_in_gg(w(X), black) → unif_out_gg(w(X), black)
U11_g(A, B, Pairs, unif_out_gg(A, B)) → U12_g(A, B, Pairs, unif_pairs_in_g(Pairs))
U12_g(A, B, Pairs, unif_pairs_out_g(Pairs)) → unif_pairs_out_g(.(A, .(B, Pairs)))
U9_gg(W, X, L1s, Y, Z, L2s, unif_pairs_out_g(.(W, .(X, .(Y, .(Z, .(W, .(Y, .(X, .(Z, .(W, .(Z, .(X, .(Y, [])))))))))))))) → U10_gg(W, X, L1s, Y, Z, L2s, unif_lines_in_gg(.(X, L1s), .(Z, L2s)))
unif_lines_in_gg(.(X, []), .(X1, [])) → unif_lines_out_gg(.(X, []), .(X1, []))
U10_gg(W, X, L1s, Y, Z, L2s, unif_lines_out_gg(.(X, L1s), .(Z, L2s))) → unif_lines_out_gg(.(W, .(X, L1s)), .(Y, .(Z, L2s)))
U7_g(L1, L2, Ls, unif_lines_out_gg(L1, L2)) → U8_g(L1, L2, Ls, unif_matrx_in_g(.(L2, Ls)))
unif_matrx_in_g(.(X, [])) → unif_matrx_out_g(.(X, []))
U8_g(L1, L2, Ls, unif_matrx_out_g(.(L2, Ls))) → unif_matrx_out_g(.(L1, .(L2, Ls)))
U2_ga(Matrix, N, unif_matrx_out_g(MatrixWithVars)) → shapes_out_ga(Matrix, N)

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

UNIF_PAIRS_IN_G(.(A, .(B, Pairs))) → U11_G(A, B, Pairs, unif_in_gg(A, B))
U11_G(A, B, Pairs, unif_out_gg(A, B)) → UNIF_PAIRS_IN_G(Pairs)

The TRS R consists of the following rules:

unif_in_gg(w(A), w(A)) → unif_out_gg(w(A), w(A))
unif_in_gg(black, black) → unif_out_gg(black, black)
unif_in_gg(black, w(X)) → unif_out_gg(black, w(X))
unif_in_gg(w(X), black) → unif_out_gg(w(X), black)

The argument filtering Pi contains the following mapping:
.(x1, x2) = .(x1, x2)
black = black
w(x1) = w
unif_in_gg(x1, x2) = unif_in_gg(x1, x2)
unif_out_gg(x1, x2) = unif_out_gg
UNIF_PAIRS_IN_G(x1) = UNIF_PAIRS_IN_G(x1)
U11_G(x1, x2, x3, x4) = U11_G(x3, x4)

We have to consider all (P,R,Pi)-chains
Transforming (infinitary) constructor rewriting Pi-DP problem [30] into ordinary QDP problem [15] 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:

U11_G(Pairs, unif_out_gg) → UNIF_PAIRS_IN_G(Pairs)
UNIF_PAIRS_IN_G(.(A, .(B, Pairs))) → U11_G(Pairs, unif_in_gg(A, B))

The TRS R consists of the following rules:

unif_in_gg(w, w) → unif_out_gg
unif_in_gg(black, black) → unif_out_gg
unif_in_gg(black, w) → unif_out_gg
unif_in_gg(w, black) → unif_out_gg

The set Q consists of the following terms:

unif_in_gg(x0, x1)

We have to consider all (P,Q,R)-chains.
By using the subterm criterion [20] together with the size-change analysis [32] 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:

U11_G(Pairs, unif_out_gg) → UNIF_PAIRS_IN_G(Pairs)
The graph contains the following edges 1 >= 1
UNIF_PAIRS_IN_G(.(A, .(B, Pairs))) → U11_G(Pairs, unif_in_gg(A, B))
The graph contains the following edges 1 > 1

↳ Prolog

  ↳ PrologToPiTRSProof

    ↳ PiTRS

      ↳ DependencyPairsProof

        ↳ PiDP

          ↳ DependencyGraphProof

            ↳ AND

              ↳ PiDP

              ↳ PiDP

                ↳ UsableRulesProof

              ↳ PiDP

              ↳ PiDP

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

U9_GG(W, X, L1s, Y, Z, L2s, unif_pairs_out_g(.(W, .(X, .(Y, .(Z, .(W, .(Y, .(X, .(Z, .(W, .(Z, .(X, .(Y, [])))))))))))))) → UNIF_LINES_IN_GG(.(X, L1s), .(Z, L2s))
UNIF_LINES_IN_GG(.(W, .(X, L1s)), .(Y, .(Z, L2s))) → U9_GG(W, X, L1s, Y, Z, L2s, unif_pairs_in_g(.(W, .(X, .(Y, .(Z, .(W, .(Y, .(X, .(Z, .(W, .(Z, .(X, .(Y, []))))))))))))))

The TRS R consists of the following rules:

shapes_in_ga(Matrix, N) → U1_ga(Matrix, N, varmat_in_ga(Matrix, MatrixWithVars))
varmat_in_ga([], []) → varmat_out_ga([], [])
varmat_in_ga(.(L, Ls), .(VL, VLs)) → U3_ga(L, Ls, VL, VLs, varmat_in_ga(L, VL))
varmat_in_ga(.(black, Xs), .(black, VXs)) → U5_ga(Xs, VXs, varmat_in_ga(Xs, VXs))
varmat_in_ga(.(white, Xs), .(w(X), VXs)) → U6_ga(Xs, X, VXs, varmat_in_ga(Xs, VXs))
U6_ga(Xs, X, VXs, varmat_out_ga(Xs, VXs)) → varmat_out_ga(.(white, Xs), .(w(X), VXs))
U5_ga(Xs, VXs, varmat_out_ga(Xs, VXs)) → varmat_out_ga(.(black, Xs), .(black, VXs))
U3_ga(L, Ls, VL, VLs, varmat_out_ga(L, VL)) → U4_ga(L, Ls, VL, VLs, varmat_in_ga(Ls, VLs))
U4_ga(L, Ls, VL, VLs, varmat_out_ga(Ls, VLs)) → varmat_out_ga(.(L, Ls), .(VL, VLs))
U1_ga(Matrix, N, varmat_out_ga(Matrix, MatrixWithVars)) → U2_ga(Matrix, N, unif_matrx_in_g(MatrixWithVars))
unif_matrx_in_g(.(L1, .(L2, Ls))) → U7_g(L1, L2, Ls, unif_lines_in_gg(L1, L2))
unif_lines_in_gg(.(W, .(X, L1s)), .(Y, .(Z, L2s))) → U9_gg(W, X, L1s, Y, Z, L2s, unif_pairs_in_g(.(W, .(X, .(Y, .(Z, .(W, .(Y, .(X, .(Z, .(W, .(Z, .(X, .(Y, []))))))))))))))
unif_pairs_in_g([]) → unif_pairs_out_g([])
unif_pairs_in_g(.(A, .(B, Pairs))) → U11_g(A, B, Pairs, unif_in_gg(A, B))
unif_in_gg(w(A), w(A)) → unif_out_gg(w(A), w(A))
unif_in_gg(black, black) → unif_out_gg(black, black)
unif_in_gg(black, w(X)) → unif_out_gg(black, w(X))
unif_in_gg(w(X), black) → unif_out_gg(w(X), black)
U11_g(A, B, Pairs, unif_out_gg(A, B)) → U12_g(A, B, Pairs, unif_pairs_in_g(Pairs))
U12_g(A, B, Pairs, unif_pairs_out_g(Pairs)) → unif_pairs_out_g(.(A, .(B, Pairs)))
U9_gg(W, X, L1s, Y, Z, L2s, unif_pairs_out_g(.(W, .(X, .(Y, .(Z, .(W, .(Y, .(X, .(Z, .(W, .(Z, .(X, .(Y, [])))))))))))))) → U10_gg(W, X, L1s, Y, Z, L2s, unif_lines_in_gg(.(X, L1s), .(Z, L2s)))
unif_lines_in_gg(.(X, []), .(X1, [])) → unif_lines_out_gg(.(X, []), .(X1, []))
U10_gg(W, X, L1s, Y, Z, L2s, unif_lines_out_gg(.(X, L1s), .(Z, L2s))) → unif_lines_out_gg(.(W, .(X, L1s)), .(Y, .(Z, L2s)))
U7_g(L1, L2, Ls, unif_lines_out_gg(L1, L2)) → U8_g(L1, L2, Ls, unif_matrx_in_g(.(L2, Ls)))
unif_matrx_in_g(.(X, [])) → unif_matrx_out_g(.(X, []))
U8_g(L1, L2, Ls, unif_matrx_out_g(.(L2, Ls))) → unif_matrx_out_g(.(L1, .(L2, Ls)))
U2_ga(Matrix, N, unif_matrx_out_g(MatrixWithVars)) → shapes_out_ga(Matrix, N)

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

U9_GG(W, X, L1s, Y, Z, L2s, unif_pairs_out_g(.(W, .(X, .(Y, .(Z, .(W, .(Y, .(X, .(Z, .(W, .(Z, .(X, .(Y, [])))))))))))))) → UNIF_LINES_IN_GG(.(X, L1s), .(Z, L2s))
UNIF_LINES_IN_GG(.(W, .(X, L1s)), .(Y, .(Z, L2s))) → U9_GG(W, X, L1s, Y, Z, L2s, unif_pairs_in_g(.(W, .(X, .(Y, .(Z, .(W, .(Y, .(X, .(Z, .(W, .(Z, .(X, .(Y, []))))))))))))))

The TRS R consists of the following rules:

unif_pairs_in_g(.(A, .(B, Pairs))) → U11_g(A, B, Pairs, unif_in_gg(A, B))
U11_g(A, B, Pairs, unif_out_gg(A, B)) → U12_g(A, B, Pairs, unif_pairs_in_g(Pairs))
unif_in_gg(w(A), w(A)) → unif_out_gg(w(A), w(A))
unif_in_gg(black, black) → unif_out_gg(black, black)
unif_in_gg(black, w(X)) → unif_out_gg(black, w(X))
unif_in_gg(w(X), black) → unif_out_gg(w(X), black)
U12_g(A, B, Pairs, unif_pairs_out_g(Pairs)) → unif_pairs_out_g(.(A, .(B, Pairs)))
unif_pairs_in_g([]) → unif_pairs_out_g([])

The argument filtering Pi contains the following mapping:
[] = []
.(x1, x2) = .(x1, x2)
black = black
w(x1) = w
unif_pairs_in_g(x1) = unif_pairs_in_g(x1)
unif_pairs_out_g(x1) = unif_pairs_out_g
U11_g(x1, x2, x3, x4) = U11_g(x3, x4)
unif_in_gg(x1, x2) = unif_in_gg(x1, x2)
unif_out_gg(x1, x2) = unif_out_gg
U12_g(x1, x2, x3, x4) = U12_g(x4)
U9_GG(x1, x2, x3, x4, x5, x6, x7) = U9_GG(x2, x3, x5, x6, x7)
UNIF_LINES_IN_GG(x1, x2) = UNIF_LINES_IN_GG(x1, x2)

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

↳ Prolog

  ↳ PrologToPiTRSProof

    ↳ PiTRS

      ↳ DependencyPairsProof

        ↳ PiDP

          ↳ DependencyGraphProof

            ↳ AND

              ↳ PiDP

              ↳ PiDP

                ↳ UsableRulesProof

                  ↳ PiDP

                    ↳ PiDPToQDPProof

                      ↳ QDP

                        ↳ Rewriting

              ↳ PiDP

              ↳ PiDP

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

UNIF_LINES_IN_GG(.(W, .(X, L1s)), .(Y, .(Z, L2s))) → U9_GG(X, L1s, Z, L2s, unif_pairs_in_g(.(W, .(X, .(Y, .(Z, .(W, .(Y, .(X, .(Z, .(W, .(Z, .(X, .(Y, []))))))))))))))
U9_GG(X, L1s, Z, L2s, unif_pairs_out_g) → UNIF_LINES_IN_GG(.(X, L1s), .(Z, L2s))

The TRS R consists of the following rules:

unif_pairs_in_g(.(A, .(B, Pairs))) → U11_g(Pairs, unif_in_gg(A, B))
U11_g(Pairs, unif_out_gg) → U12_g(unif_pairs_in_g(Pairs))
unif_in_gg(w, w) → unif_out_gg
unif_in_gg(black, black) → unif_out_gg
unif_in_gg(black, w) → unif_out_gg
unif_in_gg(w, black) → unif_out_gg
U12_g(unif_pairs_out_g) → unif_pairs_out_g
unif_pairs_in_g([]) → unif_pairs_out_g

The set Q consists of the following terms:

unif_pairs_in_g(x0)
U11_g(x0, x1)
unif_in_gg(x0, x1)
U12_g(x0)

We have to consider all (P,Q,R)-chains.
By rewriting [15] the rule UNIF_LINES_IN_GG(.(W, .(X, L1s)), .(Y, .(Z, L2s))) → U9_GG(X, L1s, Z, L2s, unif_pairs_in_g(.(W, .(X, .(Y, .(Z, .(W, .(Y, .(X, .(Z, .(W, .(Z, .(X, .(Y, [])))))))))))))) at position [4] we obtained the following new rules:

UNIF_LINES_IN_GG(.(W, .(X, L1s)), .(Y, .(Z, L2s))) → U9_GG(X, L1s, Z, L2s, U11_g(.(Y, .(Z, .(W, .(Y, .(X, .(Z, .(W, .(Z, .(X, .(Y, [])))))))))), unif_in_gg(W, X)))

↳ Prolog

  ↳ PrologToPiTRSProof

    ↳ PiTRS

      ↳ DependencyPairsProof

        ↳ PiDP

          ↳ DependencyGraphProof

            ↳ AND

              ↳ PiDP

              ↳ PiDP

                ↳ UsableRulesProof

                  ↳ PiDP

                    ↳ PiDPToQDPProof

                      ↳ QDP

                        ↳ Rewriting

                          ↳ QDP

                            ↳ QDPOrderProof

              ↳ PiDP

              ↳ PiDP

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

U9_GG(X, L1s, Z, L2s, unif_pairs_out_g) → UNIF_LINES_IN_GG(.(X, L1s), .(Z, L2s))
UNIF_LINES_IN_GG(.(W, .(X, L1s)), .(Y, .(Z, L2s))) → U9_GG(X, L1s, Z, L2s, U11_g(.(Y, .(Z, .(W, .(Y, .(X, .(Z, .(W, .(Z, .(X, .(Y, [])))))))))), unif_in_gg(W, X)))

The TRS R consists of the following rules:

unif_pairs_in_g(.(A, .(B, Pairs))) → U11_g(Pairs, unif_in_gg(A, B))
U11_g(Pairs, unif_out_gg) → U12_g(unif_pairs_in_g(Pairs))
unif_in_gg(w, w) → unif_out_gg
unif_in_gg(black, black) → unif_out_gg
unif_in_gg(black, w) → unif_out_gg
unif_in_gg(w, black) → unif_out_gg
U12_g(unif_pairs_out_g) → unif_pairs_out_g
unif_pairs_in_g([]) → unif_pairs_out_g

The set Q consists of the following terms:

unif_pairs_in_g(x0)
U11_g(x0, x1)
unif_in_gg(x0, x1)
U12_g(x0)

We have to consider all (P,Q,R)-chains.
We use the reduction pair processor [15].

The following pairs can be oriented strictly and are deleted.

UNIF_LINES_IN_GG(.(W, .(X, L1s)), .(Y, .(Z, L2s))) → U9_GG(X, L1s, Z, L2s, U11_g(.(Y, .(Z, .(W, .(Y, .(X, .(Z, .(W, .(Z, .(X, .(Y, [])))))))))), unif_in_gg(W, X)))

The remaining pairs can at least be oriented weakly.

U9_GG(X, L1s, Z, L2s, unif_pairs_out_g) → UNIF_LINES_IN_GG(.(X, L1s), .(Z, L2s))

Used ordering: Polynomial interpretation [25]:

POL(.(x₁, x₂)) = 1 + x₂
POL(U11_g(x₁, x₂)) = 0
POL(U12_g(x₁)) = 0
POL(U9_GG(x₁, x₂, x₃, x₄, x₅)) = 1 + x₄
POL(UNIF_LINES_IN_GG(x₁, x₂)) = x₂
POL([]) = 0
POL(black) = 0
POL(unif_in_gg(x₁, x₂)) = 0
POL(unif_out_gg) = 0
POL(unif_pairs_in_g(x₁)) = 0
POL(unif_pairs_out_g) = 0
POL(w) = 0

The following usable rules [17] were oriented: none

↳ Prolog

  ↳ PrologToPiTRSProof

    ↳ PiTRS

      ↳ DependencyPairsProof

        ↳ PiDP

          ↳ DependencyGraphProof

            ↳ AND

              ↳ PiDP

              ↳ PiDP

                ↳ UsableRulesProof

                  ↳ PiDP

                    ↳ PiDPToQDPProof

                      ↳ QDP

                        ↳ Rewriting

                          ↳ QDP

                            ↳ QDPOrderProof

                              ↳ QDP

                                ↳ DependencyGraphProof

              ↳ PiDP

              ↳ PiDP

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

U9_GG(X, L1s, Z, L2s, unif_pairs_out_g) → UNIF_LINES_IN_GG(.(X, L1s), .(Z, L2s))

The TRS R consists of the following rules:

unif_pairs_in_g(.(A, .(B, Pairs))) → U11_g(Pairs, unif_in_gg(A, B))
U11_g(Pairs, unif_out_gg) → U12_g(unif_pairs_in_g(Pairs))
unif_in_gg(w, w) → unif_out_gg
unif_in_gg(black, black) → unif_out_gg
unif_in_gg(black, w) → unif_out_gg
unif_in_gg(w, black) → unif_out_gg
U12_g(unif_pairs_out_g) → unif_pairs_out_g
unif_pairs_in_g([]) → unif_pairs_out_g

The set Q consists of the following terms:

unif_pairs_in_g(x0)
U11_g(x0, x1)
unif_in_gg(x0, x1)
U12_g(x0)

We have to consider all (P,Q,R)-chains.
The approximation of the Dependency Graph [15,17,22] 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:

U7_G(L1, L2, Ls, unif_lines_out_gg(L1, L2)) → UNIF_MATRX_IN_G(.(L2, Ls))
UNIF_MATRX_IN_G(.(L1, .(L2, Ls))) → U7_G(L1, L2, Ls, unif_lines_in_gg(L1, L2))

The TRS R consists of the following rules:

shapes_in_ga(Matrix, N) → U1_ga(Matrix, N, varmat_in_ga(Matrix, MatrixWithVars))
varmat_in_ga([], []) → varmat_out_ga([], [])
varmat_in_ga(.(L, Ls), .(VL, VLs)) → U3_ga(L, Ls, VL, VLs, varmat_in_ga(L, VL))
varmat_in_ga(.(black, Xs), .(black, VXs)) → U5_ga(Xs, VXs, varmat_in_ga(Xs, VXs))
varmat_in_ga(.(white, Xs), .(w(X), VXs)) → U6_ga(Xs, X, VXs, varmat_in_ga(Xs, VXs))
U6_ga(Xs, X, VXs, varmat_out_ga(Xs, VXs)) → varmat_out_ga(.(white, Xs), .(w(X), VXs))
U5_ga(Xs, VXs, varmat_out_ga(Xs, VXs)) → varmat_out_ga(.(black, Xs), .(black, VXs))
U3_ga(L, Ls, VL, VLs, varmat_out_ga(L, VL)) → U4_ga(L, Ls, VL, VLs, varmat_in_ga(Ls, VLs))
U4_ga(L, Ls, VL, VLs, varmat_out_ga(Ls, VLs)) → varmat_out_ga(.(L, Ls), .(VL, VLs))
U1_ga(Matrix, N, varmat_out_ga(Matrix, MatrixWithVars)) → U2_ga(Matrix, N, unif_matrx_in_g(MatrixWithVars))
unif_matrx_in_g(.(L1, .(L2, Ls))) → U7_g(L1, L2, Ls, unif_lines_in_gg(L1, L2))
unif_lines_in_gg(.(W, .(X, L1s)), .(Y, .(Z, L2s))) → U9_gg(W, X, L1s, Y, Z, L2s, unif_pairs_in_g(.(W, .(X, .(Y, .(Z, .(W, .(Y, .(X, .(Z, .(W, .(Z, .(X, .(Y, []))))))))))))))
unif_pairs_in_g([]) → unif_pairs_out_g([])
unif_pairs_in_g(.(A, .(B, Pairs))) → U11_g(A, B, Pairs, unif_in_gg(A, B))
unif_in_gg(w(A), w(A)) → unif_out_gg(w(A), w(A))
unif_in_gg(black, black) → unif_out_gg(black, black)
unif_in_gg(black, w(X)) → unif_out_gg(black, w(X))
unif_in_gg(w(X), black) → unif_out_gg(w(X), black)
U11_g(A, B, Pairs, unif_out_gg(A, B)) → U12_g(A, B, Pairs, unif_pairs_in_g(Pairs))
U12_g(A, B, Pairs, unif_pairs_out_g(Pairs)) → unif_pairs_out_g(.(A, .(B, Pairs)))
U9_gg(W, X, L1s, Y, Z, L2s, unif_pairs_out_g(.(W, .(X, .(Y, .(Z, .(W, .(Y, .(X, .(Z, .(W, .(Z, .(X, .(Y, [])))))))))))))) → U10_gg(W, X, L1s, Y, Z, L2s, unif_lines_in_gg(.(X, L1s), .(Z, L2s)))
unif_lines_in_gg(.(X, []), .(X1, [])) → unif_lines_out_gg(.(X, []), .(X1, []))
U10_gg(W, X, L1s, Y, Z, L2s, unif_lines_out_gg(.(X, L1s), .(Z, L2s))) → unif_lines_out_gg(.(W, .(X, L1s)), .(Y, .(Z, L2s)))
U7_g(L1, L2, Ls, unif_lines_out_gg(L1, L2)) → U8_g(L1, L2, Ls, unif_matrx_in_g(.(L2, Ls)))
unif_matrx_in_g(.(X, [])) → unif_matrx_out_g(.(X, []))
U8_g(L1, L2, Ls, unif_matrx_out_g(.(L2, Ls))) → unif_matrx_out_g(.(L1, .(L2, Ls)))
U2_ga(Matrix, N, unif_matrx_out_g(MatrixWithVars)) → shapes_out_ga(Matrix, N)

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

U7_G(L1, L2, Ls, unif_lines_out_gg(L1, L2)) → UNIF_MATRX_IN_G(.(L2, Ls))
UNIF_MATRX_IN_G(.(L1, .(L2, Ls))) → U7_G(L1, L2, Ls, unif_lines_in_gg(L1, L2))

The TRS R consists of the following rules:

unif_lines_in_gg(.(W, .(X, L1s)), .(Y, .(Z, L2s))) → U9_gg(W, X, L1s, Y, Z, L2s, unif_pairs_in_g(.(W, .(X, .(Y, .(Z, .(W, .(Y, .(X, .(Z, .(W, .(Z, .(X, .(Y, []))))))))))))))
unif_lines_in_gg(.(X, []), .(X1, [])) → unif_lines_out_gg(.(X, []), .(X1, []))
U9_gg(W, X, L1s, Y, Z, L2s, unif_pairs_out_g(.(W, .(X, .(Y, .(Z, .(W, .(Y, .(X, .(Z, .(W, .(Z, .(X, .(Y, [])))))))))))))) → U10_gg(W, X, L1s, Y, Z, L2s, unif_lines_in_gg(.(X, L1s), .(Z, L2s)))
unif_pairs_in_g(.(A, .(B, Pairs))) → U11_g(A, B, Pairs, unif_in_gg(A, B))
U10_gg(W, X, L1s, Y, Z, L2s, unif_lines_out_gg(.(X, L1s), .(Z, L2s))) → unif_lines_out_gg(.(W, .(X, L1s)), .(Y, .(Z, L2s)))
U11_g(A, B, Pairs, unif_out_gg(A, B)) → U12_g(A, B, Pairs, unif_pairs_in_g(Pairs))
unif_in_gg(w(A), w(A)) → unif_out_gg(w(A), w(A))
unif_in_gg(black, black) → unif_out_gg(black, black)
unif_in_gg(black, w(X)) → unif_out_gg(black, w(X))
unif_in_gg(w(X), black) → unif_out_gg(w(X), black)
U12_g(A, B, Pairs, unif_pairs_out_g(Pairs)) → unif_pairs_out_g(.(A, .(B, Pairs)))
unif_pairs_in_g([]) → unif_pairs_out_g([])

The argument filtering Pi contains the following mapping:
[] = []
.(x1, x2) = .(x1, x2)
black = black
w(x1) = w
unif_lines_in_gg(x1, x2) = unif_lines_in_gg(x1, x2)
U9_gg(x1, x2, x3, x4, x5, x6, x7) = U9_gg(x2, x3, x5, x6, x7)
unif_pairs_in_g(x1) = unif_pairs_in_g(x1)
unif_pairs_out_g(x1) = unif_pairs_out_g
U11_g(x1, x2, x3, x4) = U11_g(x3, x4)
unif_in_gg(x1, x2) = unif_in_gg(x1, x2)
unif_out_gg(x1, x2) = unif_out_gg
U12_g(x1, x2, x3, x4) = U12_g(x4)
U10_gg(x1, x2, x3, x4, x5, x6, x7) = U10_gg(x7)
unif_lines_out_gg(x1, x2) = unif_lines_out_gg
U7_G(x1, x2, x3, x4) = U7_G(x2, x3, x4)
UNIF_MATRX_IN_G(x1) = UNIF_MATRX_IN_G(x1)

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

↳ Prolog

  ↳ PrologToPiTRSProof

    ↳ PiTRS

      ↳ DependencyPairsProof

        ↳ PiDP

          ↳ DependencyGraphProof

            ↳ AND

              ↳ PiDP

              ↳ PiDP

              ↳ PiDP

                ↳ UsableRulesProof

                  ↳ PiDP

                    ↳ PiDPToQDPProof

                      ↳ QDP

                        ↳ QDPOrderProof

              ↳ PiDP

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

U7_G(L2, Ls, unif_lines_out_gg) → UNIF_MATRX_IN_G(.(L2, Ls))
UNIF_MATRX_IN_G(.(L1, .(L2, Ls))) → U7_G(L2, Ls, unif_lines_in_gg(L1, L2))

The TRS R consists of the following rules:

unif_lines_in_gg(.(W, .(X, L1s)), .(Y, .(Z, L2s))) → U9_gg(X, L1s, Z, L2s, unif_pairs_in_g(.(W, .(X, .(Y, .(Z, .(W, .(Y, .(X, .(Z, .(W, .(Z, .(X, .(Y, []))))))))))))))
unif_lines_in_gg(.(X, []), .(X1, [])) → unif_lines_out_gg
U9_gg(X, L1s, Z, L2s, unif_pairs_out_g) → U10_gg(unif_lines_in_gg(.(X, L1s), .(Z, L2s)))
unif_pairs_in_g(.(A, .(B, Pairs))) → U11_g(Pairs, unif_in_gg(A, B))
U10_gg(unif_lines_out_gg) → unif_lines_out_gg
U11_g(Pairs, unif_out_gg) → U12_g(unif_pairs_in_g(Pairs))
unif_in_gg(w, w) → unif_out_gg
unif_in_gg(black, black) → unif_out_gg
unif_in_gg(black, w) → unif_out_gg
unif_in_gg(w, black) → unif_out_gg
U12_g(unif_pairs_out_g) → unif_pairs_out_g
unif_pairs_in_g([]) → unif_pairs_out_g

The set Q consists of the following terms:

unif_lines_in_gg(x0, x1)
U9_gg(x0, x1, x2, x3, x4)
unif_pairs_in_g(x0)
U10_gg(x0)
U11_g(x0, x1)
unif_in_gg(x0, x1)
U12_g(x0)

We have to consider all (P,Q,R)-chains.
We use the reduction pair processor [15].

The following pairs can be oriented strictly and are deleted.

UNIF_MATRX_IN_G(.(L1, .(L2, Ls))) → U7_G(L2, Ls, unif_lines_in_gg(L1, L2))

The remaining pairs can at least be oriented weakly.

U7_G(L2, Ls, unif_lines_out_gg) → UNIF_MATRX_IN_G(.(L2, Ls))

Used ordering: Polynomial interpretation [25]:

POL(.(x₁, x₂)) = 1 + x₁ + x₂
POL(U10_gg(x₁)) = 1
POL(U11_g(x₁, x₂)) = 1 + x₂
POL(U12_g(x₁)) = 0
POL(U7_G(x₁, x₂, x₃)) = 1 + x₁ + x₂ + x₃
POL(U9_gg(x₁, x₂, x₃, x₄, x₅)) = 1 + x₁ + x₂
POL(UNIF_MATRX_IN_G(x₁)) = 1 + x₁
POL([]) = 0
POL(black) = 0
POL(unif_in_gg(x₁, x₂)) = 0
POL(unif_lines_in_gg(x₁, x₂)) = x₁
POL(unif_lines_out_gg) = 1
POL(unif_out_gg) = 1
POL(unif_pairs_in_g(x₁)) = 1
POL(unif_pairs_out_g) = 0
POL(w) = 0

The following usable rules [17] were oriented:

unif_lines_in_gg(.(X, []), .(X1, [])) → unif_lines_out_gg
unif_lines_in_gg(.(W, .(X, L1s)), .(Y, .(Z, L2s))) → U9_gg(X, L1s, Z, L2s, unif_pairs_in_g(.(W, .(X, .(Y, .(Z, .(W, .(Y, .(X, .(Z, .(W, .(Z, .(X, .(Y, []))))))))))))))
U9_gg(X, L1s, Z, L2s, unif_pairs_out_g) → U10_gg(unif_lines_in_gg(.(X, L1s), .(Z, L2s)))
U10_gg(unif_lines_out_gg) → unif_lines_out_gg

↳ Prolog

  ↳ PrologToPiTRSProof

    ↳ PiTRS

      ↳ DependencyPairsProof

        ↳ PiDP

          ↳ DependencyGraphProof

            ↳ AND

              ↳ PiDP

              ↳ PiDP

              ↳ PiDP

                ↳ UsableRulesProof

                  ↳ PiDP

                    ↳ PiDPToQDPProof

                      ↳ QDP

                        ↳ QDPOrderProof

                          ↳ QDP

                            ↳ DependencyGraphProof

              ↳ PiDP

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

U7_G(L2, Ls, unif_lines_out_gg) → UNIF_MATRX_IN_G(.(L2, Ls))

The TRS R consists of the following rules:

unif_lines_in_gg(.(W, .(X, L1s)), .(Y, .(Z, L2s))) → U9_gg(X, L1s, Z, L2s, unif_pairs_in_g(.(W, .(X, .(Y, .(Z, .(W, .(Y, .(X, .(Z, .(W, .(Z, .(X, .(Y, []))))))))))))))
unif_lines_in_gg(.(X, []), .(X1, [])) → unif_lines_out_gg
U9_gg(X, L1s, Z, L2s, unif_pairs_out_g) → U10_gg(unif_lines_in_gg(.(X, L1s), .(Z, L2s)))
unif_pairs_in_g(.(A, .(B, Pairs))) → U11_g(Pairs, unif_in_gg(A, B))
U10_gg(unif_lines_out_gg) → unif_lines_out_gg
U11_g(Pairs, unif_out_gg) → U12_g(unif_pairs_in_g(Pairs))
unif_in_gg(w, w) → unif_out_gg
unif_in_gg(black, black) → unif_out_gg
unif_in_gg(black, w) → unif_out_gg
unif_in_gg(w, black) → unif_out_gg
U12_g(unif_pairs_out_g) → unif_pairs_out_g
unif_pairs_in_g([]) → unif_pairs_out_g

The set Q consists of the following terms:

unif_lines_in_gg(x0, x1)
U9_gg(x0, x1, x2, x3, x4)
unif_pairs_in_g(x0)
U10_gg(x0)
U11_g(x0, x1)
unif_in_gg(x0, x1)
U12_g(x0)

We have to consider all (P,Q,R)-chains.
The approximation of the Dependency Graph [15,17,22] 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_IN_GA(.(L, Ls), .(VL, VLs)) → VARMAT_IN_GA(L, VL)
U3_GA(L, Ls, VL, VLs, varmat_out_ga(L, VL)) → VARMAT_IN_GA(Ls, VLs)
VARMAT_IN_GA(.(L, Ls), .(VL, VLs)) → U3_GA(L, Ls, VL, VLs, varmat_in_ga(L, VL))
VARMAT_IN_GA(.(black, Xs), .(black, VXs)) → VARMAT_IN_GA(Xs, VXs)
VARMAT_IN_GA(.(white, Xs), .(w(X), VXs)) → VARMAT_IN_GA(Xs, VXs)

The TRS R consists of the following rules:

shapes_in_ga(Matrix, N) → U1_ga(Matrix, N, varmat_in_ga(Matrix, MatrixWithVars))
varmat_in_ga([], []) → varmat_out_ga([], [])
varmat_in_ga(.(L, Ls), .(VL, VLs)) → U3_ga(L, Ls, VL, VLs, varmat_in_ga(L, VL))
varmat_in_ga(.(black, Xs), .(black, VXs)) → U5_ga(Xs, VXs, varmat_in_ga(Xs, VXs))
varmat_in_ga(.(white, Xs), .(w(X), VXs)) → U6_ga(Xs, X, VXs, varmat_in_ga(Xs, VXs))
U6_ga(Xs, X, VXs, varmat_out_ga(Xs, VXs)) → varmat_out_ga(.(white, Xs), .(w(X), VXs))
U5_ga(Xs, VXs, varmat_out_ga(Xs, VXs)) → varmat_out_ga(.(black, Xs), .(black, VXs))
U3_ga(L, Ls, VL, VLs, varmat_out_ga(L, VL)) → U4_ga(L, Ls, VL, VLs, varmat_in_ga(Ls, VLs))
U4_ga(L, Ls, VL, VLs, varmat_out_ga(Ls, VLs)) → varmat_out_ga(.(L, Ls), .(VL, VLs))
U1_ga(Matrix, N, varmat_out_ga(Matrix, MatrixWithVars)) → U2_ga(Matrix, N, unif_matrx_in_g(MatrixWithVars))
unif_matrx_in_g(.(L1, .(L2, Ls))) → U7_g(L1, L2, Ls, unif_lines_in_gg(L1, L2))
unif_lines_in_gg(.(W, .(X, L1s)), .(Y, .(Z, L2s))) → U9_gg(W, X, L1s, Y, Z, L2s, unif_pairs_in_g(.(W, .(X, .(Y, .(Z, .(W, .(Y, .(X, .(Z, .(W, .(Z, .(X, .(Y, []))))))))))))))
unif_pairs_in_g([]) → unif_pairs_out_g([])
unif_pairs_in_g(.(A, .(B, Pairs))) → U11_g(A, B, Pairs, unif_in_gg(A, B))
unif_in_gg(w(A), w(A)) → unif_out_gg(w(A), w(A))
unif_in_gg(black, black) → unif_out_gg(black, black)
unif_in_gg(black, w(X)) → unif_out_gg(black, w(X))
unif_in_gg(w(X), black) → unif_out_gg(w(X), black)
U11_g(A, B, Pairs, unif_out_gg(A, B)) → U12_g(A, B, Pairs, unif_pairs_in_g(Pairs))
U12_g(A, B, Pairs, unif_pairs_out_g(Pairs)) → unif_pairs_out_g(.(A, .(B, Pairs)))
U9_gg(W, X, L1s, Y, Z, L2s, unif_pairs_out_g(.(W, .(X, .(Y, .(Z, .(W, .(Y, .(X, .(Z, .(W, .(Z, .(X, .(Y, [])))))))))))))) → U10_gg(W, X, L1s, Y, Z, L2s, unif_lines_in_gg(.(X, L1s), .(Z, L2s)))
unif_lines_in_gg(.(X, []), .(X1, [])) → unif_lines_out_gg(.(X, []), .(X1, []))
U10_gg(W, X, L1s, Y, Z, L2s, unif_lines_out_gg(.(X, L1s), .(Z, L2s))) → unif_lines_out_gg(.(W, .(X, L1s)), .(Y, .(Z, L2s)))
U7_g(L1, L2, Ls, unif_lines_out_gg(L1, L2)) → U8_g(L1, L2, Ls, unif_matrx_in_g(.(L2, Ls)))
unif_matrx_in_g(.(X, [])) → unif_matrx_out_g(.(X, []))
U8_g(L1, L2, Ls, unif_matrx_out_g(.(L2, Ls))) → unif_matrx_out_g(.(L1, .(L2, Ls)))
U2_ga(Matrix, N, unif_matrx_out_g(MatrixWithVars)) → shapes_out_ga(Matrix, N)

↳ 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_IN_GA(.(L, Ls), .(VL, VLs)) → VARMAT_IN_GA(L, VL)
U3_GA(L, Ls, VL, VLs, varmat_out_ga(L, VL)) → VARMAT_IN_GA(Ls, VLs)
VARMAT_IN_GA(.(L, Ls), .(VL, VLs)) → U3_GA(L, Ls, VL, VLs, varmat_in_ga(L, VL))
VARMAT_IN_GA(.(black, Xs), .(black, VXs)) → VARMAT_IN_GA(Xs, VXs)
VARMAT_IN_GA(.(white, Xs), .(w(X), VXs)) → VARMAT_IN_GA(Xs, VXs)

The TRS R consists of the following rules:

varmat_in_ga([], []) → varmat_out_ga([], [])
varmat_in_ga(.(L, Ls), .(VL, VLs)) → U3_ga(L, Ls, VL, VLs, varmat_in_ga(L, VL))
varmat_in_ga(.(black, Xs), .(black, VXs)) → U5_ga(Xs, VXs, varmat_in_ga(Xs, VXs))
varmat_in_ga(.(white, Xs), .(w(X), VXs)) → U6_ga(Xs, X, VXs, varmat_in_ga(Xs, VXs))
U3_ga(L, Ls, VL, VLs, varmat_out_ga(L, VL)) → U4_ga(L, Ls, VL, VLs, varmat_in_ga(Ls, VLs))
U5_ga(Xs, VXs, varmat_out_ga(Xs, VXs)) → varmat_out_ga(.(black, Xs), .(black, VXs))
U6_ga(Xs, X, VXs, varmat_out_ga(Xs, VXs)) → varmat_out_ga(.(white, Xs), .(w(X), VXs))
U4_ga(L, Ls, VL, VLs, varmat_out_ga(Ls, VLs)) → varmat_out_ga(.(L, Ls), .(VL, VLs))

The argument filtering Pi contains the following mapping:
varmat_in_ga(x1, x2) = varmat_in_ga(x1)
[] = []
varmat_out_ga(x1, x2) = varmat_out_ga(x2)
.(x1, x2) = .(x1, x2)
U3_ga(x1, x2, x3, x4, x5) = U3_ga(x2, x5)
black = black
U5_ga(x1, x2, x3) = U5_ga(x3)
white = white
U6_ga(x1, x2, x3, x4) = U6_ga(x4)
w(x1) = w
U4_ga(x1, x2, x3, x4, x5) = U4_ga(x3, x5)
VARMAT_IN_GA(x1, x2) = VARMAT_IN_GA(x1)
U3_GA(x1, x2, x3, x4, x5) = U3_GA(x2, x5)

We have to consider all (P,R,Pi)-chains
Transforming (infinitary) constructor rewriting Pi-DP problem [30] into ordinary QDP problem [15] 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_IN_GA(.(black, Xs)) → VARMAT_IN_GA(Xs)
VARMAT_IN_GA(.(L, Ls)) → VARMAT_IN_GA(L)
VARMAT_IN_GA(.(L, Ls)) → U3_GA(Ls, varmat_in_ga(L))
U3_GA(Ls, varmat_out_ga(VL)) → VARMAT_IN_GA(Ls)
VARMAT_IN_GA(.(white, Xs)) → VARMAT_IN_GA(Xs)

The TRS R consists of the following rules:

varmat_in_ga([]) → varmat_out_ga([])
varmat_in_ga(.(L, Ls)) → U3_ga(Ls, varmat_in_ga(L))
varmat_in_ga(.(black, Xs)) → U5_ga(varmat_in_ga(Xs))
varmat_in_ga(.(white, Xs)) → U6_ga(varmat_in_ga(Xs))
U3_ga(Ls, varmat_out_ga(VL)) → U4_ga(VL, varmat_in_ga(Ls))
U5_ga(varmat_out_ga(VXs)) → varmat_out_ga(.(black, VXs))
U6_ga(varmat_out_ga(VXs)) → varmat_out_ga(.(w, VXs))
U4_ga(VL, varmat_out_ga(VLs)) → varmat_out_ga(.(VL, VLs))

The set Q consists of the following terms:

varmat_in_ga(x0)
U3_ga(x0, x1)
U5_ga(x0)
U6_ga(x0)
U4_ga(x0, x1)

We have to consider all (P,Q,R)-chains.
By using the subterm criterion [20] together with the size-change analysis [32] 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:

VARMAT_IN_GA(.(L, Ls)) → U3_GA(Ls, varmat_in_ga(L))
The graph contains the following edges 1 > 1
U3_GA(Ls, varmat_out_ga(VL)) → VARMAT_IN_GA(Ls)
The graph contains the following edges 1 >= 1
VARMAT_IN_GA(.(L, Ls)) → VARMAT_IN_GA(L)
The graph contains the following edges 1 > 1
VARMAT_IN_GA(.(black, Xs)) → VARMAT_IN_GA(Xs)
The graph contains the following edges 1 > 1
VARMAT_IN_GA(.(white, Xs)) → VARMAT_IN_GA(Xs)
The graph contains the following edges 1 > 1