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

(0) Obligation:

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(X1), VXs)) :- varmat(Xs, VXs).
unif_matrx(.(L1, .(L2, Ls))) :- ','(unif_lines(L1, L2), unif_matrx(.(L2, Ls))).
unif_matrx(.(X2, [])).
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(.(X3, []), .(X4, [])).
unif_pairs([]).
unif_pairs(.(A, .(B, Pairs))) :- ','(unif(A, B), unif_pairs(Pairs)).
unif(w(A), w(A)).
unif(black, black).
unif(black, w(X5)).
unif(w(X6), black).

Queries:

shapes(g,a).

(1) PrologToPiTRSProof (SOUND transformation)

We use the technique of [LOPSTR]. 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(X1), VXs)) → U6_ga(Xs, X1, VXs, varmat_in_ga(Xs, VXs))
U6_ga(Xs, X1, VXs, varmat_out_ga(Xs, VXs)) → varmat_out_ga(.(white, Xs), .(w(X1), 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(X5)) → unif_out_gg(black, w(X5))
unif_in_gg(w(X6), black) → unif_out_gg(w(X6), 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(.(X3, []), .(X4, [])) → unif_lines_out_gg(.(X3, []), .(X4, []))
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(.(X2, [])) → unif_matrx_out_g(.(X2, []))
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(x1, x3)
varmat_in_ga(x1, x2)  =  varmat_in_ga(x1)
[]  =  []
varmat_out_ga(x1, x2)  =  varmat_out_ga(x1, x2)
.(x1, x2)  =  .(x1, x2)
U3_ga(x1, x2, x3, x4, x5)  =  U3_ga(x1, x2, x5)
black  =  black
U5_ga(x1, x2, x3)  =  U5_ga(x1, x3)
white  =  white
U6_ga(x1, x2, x3, x4)  =  U6_ga(x1, x4)
w(x1)  =  w
U4_ga(x1, x2, x3, x4, x5)  =  U4_ga(x1, x2, x3, x5)
U2_ga(x1, x2, x3)  =  U2_ga(x1, x3)
unif_matrx_in_g(x1)  =  unif_matrx_in_g(x1)
U7_g(x1, x2, x3, x4)  =  U7_g(x1, 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(x1, x2, x3, x4, x5, x6, x7)
unif_pairs_in_g(x1)  =  unif_pairs_in_g(x1)
unif_pairs_out_g(x1)  =  unif_pairs_out_g(x1)
U11_g(x1, x2, x3, x4)  =  U11_g(x1, x2, x3, x4)
unif_in_gg(x1, x2)  =  unif_in_gg(x1, x2)
unif_out_gg(x1, x2)  =  unif_out_gg(x1, x2)
U12_g(x1, x2, x3, x4)  =  U12_g(x1, x2, x3, x4)
U10_gg(x1, x2, x3, x4, x5, x6, x7)  =  U10_gg(x1, x2, x3, x4, x5, x6, x7)
unif_lines_out_gg(x1, x2)  =  unif_lines_out_gg(x1, x2)
U8_g(x1, x2, x3, x4)  =  U8_g(x1, x2, x3, x4)
unif_matrx_out_g(x1)  =  unif_matrx_out_g(x1)
shapes_out_ga(x1, x2)  =  shapes_out_ga(x1)

Infinitary Constructor Rewriting Termination of PiTRS implies Termination of Prolog

(2) Obligation:

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(X1), VXs)) → U6_ga(Xs, X1, VXs, varmat_in_ga(Xs, VXs))
U6_ga(Xs, X1, VXs, varmat_out_ga(Xs, VXs)) → varmat_out_ga(.(white, Xs), .(w(X1), 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(X5)) → unif_out_gg(black, w(X5))
unif_in_gg(w(X6), black) → unif_out_gg(w(X6), 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(.(X3, []), .(X4, [])) → unif_lines_out_gg(.(X3, []), .(X4, []))
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(.(X2, [])) → unif_matrx_out_g(.(X2, []))
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(x1, x3)
varmat_in_ga(x1, x2)  =  varmat_in_ga(x1)
[]  =  []
varmat_out_ga(x1, x2)  =  varmat_out_ga(x1, x2)
.(x1, x2)  =  .(x1, x2)
U3_ga(x1, x2, x3, x4, x5)  =  U3_ga(x1, x2, x5)
black  =  black
U5_ga(x1, x2, x3)  =  U5_ga(x1, x3)
white  =  white
U6_ga(x1, x2, x3, x4)  =  U6_ga(x1, x4)
w(x1)  =  w
U4_ga(x1, x2, x3, x4, x5)  =  U4_ga(x1, x2, x3, x5)
U2_ga(x1, x2, x3)  =  U2_ga(x1, x3)
unif_matrx_in_g(x1)  =  unif_matrx_in_g(x1)
U7_g(x1, x2, x3, x4)  =  U7_g(x1, 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(x1, x2, x3, x4, x5, x6, x7)
unif_pairs_in_g(x1)  =  unif_pairs_in_g(x1)
unif_pairs_out_g(x1)  =  unif_pairs_out_g(x1)
U11_g(x1, x2, x3, x4)  =  U11_g(x1, x2, x3, x4)
unif_in_gg(x1, x2)  =  unif_in_gg(x1, x2)
unif_out_gg(x1, x2)  =  unif_out_gg(x1, x2)
U12_g(x1, x2, x3, x4)  =  U12_g(x1, x2, x3, x4)
U10_gg(x1, x2, x3, x4, x5, x6, x7)  =  U10_gg(x1, x2, x3, x4, x5, x6, x7)
unif_lines_out_gg(x1, x2)  =  unif_lines_out_gg(x1, x2)
U8_g(x1, x2, x3, x4)  =  U8_g(x1, x2, x3, x4)
unif_matrx_out_g(x1)  =  unif_matrx_out_g(x1)
shapes_out_ga(x1, x2)  =  shapes_out_ga(x1)

(3) DependencyPairsProof (EQUIVALENT transformation)

Using Dependency Pairs [AG00,LOPSTR] we result in the following initial DP problem:
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(X1), VXs)) → U6_GA(Xs, X1, VXs, varmat_in_ga(Xs, VXs))
VARMAT_IN_GA(.(white, Xs), .(w(X1), 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(X1), VXs)) → U6_ga(Xs, X1, VXs, varmat_in_ga(Xs, VXs))
U6_ga(Xs, X1, VXs, varmat_out_ga(Xs, VXs)) → varmat_out_ga(.(white, Xs), .(w(X1), 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(X5)) → unif_out_gg(black, w(X5))
unif_in_gg(w(X6), black) → unif_out_gg(w(X6), 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(.(X3, []), .(X4, [])) → unif_lines_out_gg(.(X3, []), .(X4, []))
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(.(X2, [])) → unif_matrx_out_g(.(X2, []))
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(x1, x3)
varmat_in_ga(x1, x2)  =  varmat_in_ga(x1)
[]  =  []
varmat_out_ga(x1, x2)  =  varmat_out_ga(x1, x2)
.(x1, x2)  =  .(x1, x2)
U3_ga(x1, x2, x3, x4, x5)  =  U3_ga(x1, x2, x5)
black  =  black
U5_ga(x1, x2, x3)  =  U5_ga(x1, x3)
white  =  white
U6_ga(x1, x2, x3, x4)  =  U6_ga(x1, x4)
w(x1)  =  w
U4_ga(x1, x2, x3, x4, x5)  =  U4_ga(x1, x2, x3, x5)
U2_ga(x1, x2, x3)  =  U2_ga(x1, x3)
unif_matrx_in_g(x1)  =  unif_matrx_in_g(x1)
U7_g(x1, x2, x3, x4)  =  U7_g(x1, 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(x1, x2, x3, x4, x5, x6, x7)
unif_pairs_in_g(x1)  =  unif_pairs_in_g(x1)
unif_pairs_out_g(x1)  =  unif_pairs_out_g(x1)
U11_g(x1, x2, x3, x4)  =  U11_g(x1, x2, x3, x4)
unif_in_gg(x1, x2)  =  unif_in_gg(x1, x2)
unif_out_gg(x1, x2)  =  unif_out_gg(x1, x2)
U12_g(x1, x2, x3, x4)  =  U12_g(x1, x2, x3, x4)
U10_gg(x1, x2, x3, x4, x5, x6, x7)  =  U10_gg(x1, x2, x3, x4, x5, x6, x7)
unif_lines_out_gg(x1, x2)  =  unif_lines_out_gg(x1, x2)
U8_g(x1, x2, x3, x4)  =  U8_g(x1, x2, x3, x4)
unif_matrx_out_g(x1)  =  unif_matrx_out_g(x1)
shapes_out_ga(x1, x2)  =  shapes_out_ga(x1)
SHAPES_IN_GA(x1, x2)  =  SHAPES_IN_GA(x1)
U1_GA(x1, x2, x3)  =  U1_GA(x1, x3)
VARMAT_IN_GA(x1, x2)  =  VARMAT_IN_GA(x1)
U3_GA(x1, x2, x3, x4, x5)  =  U3_GA(x1, x2, x5)
U5_GA(x1, x2, x3)  =  U5_GA(x1, x3)
U6_GA(x1, x2, x3, x4)  =  U6_GA(x1, x4)
U4_GA(x1, x2, x3, x4, x5)  =  U4_GA(x1, x2, x3, x5)
U2_GA(x1, x2, x3)  =  U2_GA(x1, x3)
UNIF_MATRX_IN_G(x1)  =  UNIF_MATRX_IN_G(x1)
U7_G(x1, x2, x3, x4)  =  U7_G(x1, 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(x1, x2, x3, x4, x5, x6, x7)
UNIF_PAIRS_IN_G(x1)  =  UNIF_PAIRS_IN_G(x1)
U11_G(x1, x2, x3, x4)  =  U11_G(x1, x2, x3, x4)
UNIF_IN_GG(x1, x2)  =  UNIF_IN_GG(x1, x2)
U12_G(x1, x2, x3, x4)  =  U12_G(x1, x2, x3, x4)
U10_GG(x1, x2, x3, x4, x5, x6, x7)  =  U10_GG(x1, x2, x3, x4, x5, x6, x7)
U8_G(x1, x2, x3, x4)  =  U8_G(x1, x2, x3, x4)

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

(4) Obligation:

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(X1), VXs)) → U6_GA(Xs, X1, VXs, varmat_in_ga(Xs, VXs))
VARMAT_IN_GA(.(white, Xs), .(w(X1), 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(X1), VXs)) → U6_ga(Xs, X1, VXs, varmat_in_ga(Xs, VXs))
U6_ga(Xs, X1, VXs, varmat_out_ga(Xs, VXs)) → varmat_out_ga(.(white, Xs), .(w(X1), 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(X5)) → unif_out_gg(black, w(X5))
unif_in_gg(w(X6), black) → unif_out_gg(w(X6), 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(.(X3, []), .(X4, [])) → unif_lines_out_gg(.(X3, []), .(X4, []))
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(.(X2, [])) → unif_matrx_out_g(.(X2, []))
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(x1, x3)
varmat_in_ga(x1, x2)  =  varmat_in_ga(x1)
[]  =  []
varmat_out_ga(x1, x2)  =  varmat_out_ga(x1, x2)
.(x1, x2)  =  .(x1, x2)
U3_ga(x1, x2, x3, x4, x5)  =  U3_ga(x1, x2, x5)
black  =  black
U5_ga(x1, x2, x3)  =  U5_ga(x1, x3)
white  =  white
U6_ga(x1, x2, x3, x4)  =  U6_ga(x1, x4)
w(x1)  =  w
U4_ga(x1, x2, x3, x4, x5)  =  U4_ga(x1, x2, x3, x5)
U2_ga(x1, x2, x3)  =  U2_ga(x1, x3)
unif_matrx_in_g(x1)  =  unif_matrx_in_g(x1)
U7_g(x1, x2, x3, x4)  =  U7_g(x1, 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(x1, x2, x3, x4, x5, x6, x7)
unif_pairs_in_g(x1)  =  unif_pairs_in_g(x1)
unif_pairs_out_g(x1)  =  unif_pairs_out_g(x1)
U11_g(x1, x2, x3, x4)  =  U11_g(x1, x2, x3, x4)
unif_in_gg(x1, x2)  =  unif_in_gg(x1, x2)
unif_out_gg(x1, x2)  =  unif_out_gg(x1, x2)
U12_g(x1, x2, x3, x4)  =  U12_g(x1, x2, x3, x4)
U10_gg(x1, x2, x3, x4, x5, x6, x7)  =  U10_gg(x1, x2, x3, x4, x5, x6, x7)
unif_lines_out_gg(x1, x2)  =  unif_lines_out_gg(x1, x2)
U8_g(x1, x2, x3, x4)  =  U8_g(x1, x2, x3, x4)
unif_matrx_out_g(x1)  =  unif_matrx_out_g(x1)
shapes_out_ga(x1, x2)  =  shapes_out_ga(x1)
SHAPES_IN_GA(x1, x2)  =  SHAPES_IN_GA(x1)
U1_GA(x1, x2, x3)  =  U1_GA(x1, x3)
VARMAT_IN_GA(x1, x2)  =  VARMAT_IN_GA(x1)
U3_GA(x1, x2, x3, x4, x5)  =  U3_GA(x1, x2, x5)
U5_GA(x1, x2, x3)  =  U5_GA(x1, x3)
U6_GA(x1, x2, x3, x4)  =  U6_GA(x1, x4)
U4_GA(x1, x2, x3, x4, x5)  =  U4_GA(x1, x2, x3, x5)
U2_GA(x1, x2, x3)  =  U2_GA(x1, x3)
UNIF_MATRX_IN_G(x1)  =  UNIF_MATRX_IN_G(x1)
U7_G(x1, x2, x3, x4)  =  U7_G(x1, 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(x1, x2, x3, x4, x5, x6, x7)
UNIF_PAIRS_IN_G(x1)  =  UNIF_PAIRS_IN_G(x1)
U11_G(x1, x2, x3, x4)  =  U11_G(x1, x2, x3, x4)
UNIF_IN_GG(x1, x2)  =  UNIF_IN_GG(x1, x2)
U12_G(x1, x2, x3, x4)  =  U12_G(x1, x2, x3, x4)
U10_GG(x1, x2, x3, x4, x5, x6, x7)  =  U10_GG(x1, x2, x3, x4, x5, x6, x7)
U8_G(x1, x2, x3, x4)  =  U8_G(x1, x2, x3, x4)

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

(5) DependencyGraphProof (EQUIVALENT transformation)

The approximation of the Dependency Graph [LOPSTR] contains 4 SCCs with 13 less nodes.

(6) Complex Obligation (AND)

(7) Obligation:

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

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

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(X1), VXs)) → U6_ga(Xs, X1, VXs, varmat_in_ga(Xs, VXs))
U6_ga(Xs, X1, VXs, varmat_out_ga(Xs, VXs)) → varmat_out_ga(.(white, Xs), .(w(X1), 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(X5)) → unif_out_gg(black, w(X5))
unif_in_gg(w(X6), black) → unif_out_gg(w(X6), 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(.(X3, []), .(X4, [])) → unif_lines_out_gg(.(X3, []), .(X4, []))
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(.(X2, [])) → unif_matrx_out_g(.(X2, []))
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(x1, x3)
varmat_in_ga(x1, x2)  =  varmat_in_ga(x1)
[]  =  []
varmat_out_ga(x1, x2)  =  varmat_out_ga(x1, x2)
.(x1, x2)  =  .(x1, x2)
U3_ga(x1, x2, x3, x4, x5)  =  U3_ga(x1, x2, x5)
black  =  black
U5_ga(x1, x2, x3)  =  U5_ga(x1, x3)
white  =  white
U6_ga(x1, x2, x3, x4)  =  U6_ga(x1, x4)
w(x1)  =  w
U4_ga(x1, x2, x3, x4, x5)  =  U4_ga(x1, x2, x3, x5)
U2_ga(x1, x2, x3)  =  U2_ga(x1, x3)
unif_matrx_in_g(x1)  =  unif_matrx_in_g(x1)
U7_g(x1, x2, x3, x4)  =  U7_g(x1, 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(x1, x2, x3, x4, x5, x6, x7)
unif_pairs_in_g(x1)  =  unif_pairs_in_g(x1)
unif_pairs_out_g(x1)  =  unif_pairs_out_g(x1)
U11_g(x1, x2, x3, x4)  =  U11_g(x1, x2, x3, x4)
unif_in_gg(x1, x2)  =  unif_in_gg(x1, x2)
unif_out_gg(x1, x2)  =  unif_out_gg(x1, x2)
U12_g(x1, x2, x3, x4)  =  U12_g(x1, x2, x3, x4)
U10_gg(x1, x2, x3, x4, x5, x6, x7)  =  U10_gg(x1, x2, x3, x4, x5, x6, x7)
unif_lines_out_gg(x1, x2)  =  unif_lines_out_gg(x1, x2)
U8_g(x1, x2, x3, x4)  =  U8_g(x1, x2, x3, x4)
unif_matrx_out_g(x1)  =  unif_matrx_out_g(x1)
shapes_out_ga(x1, x2)  =  shapes_out_ga(x1)
UNIF_PAIRS_IN_G(x1)  =  UNIF_PAIRS_IN_G(x1)
U11_G(x1, x2, x3, x4)  =  U11_G(x1, x2, x3, x4)

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

(8) UsableRulesProof (EQUIVALENT transformation)

For (infinitary) constructor rewriting [LOPSTR] we can delete all non-usable rules from R.

(9) Obligation:

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

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

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(X5)) → unif_out_gg(black, w(X5))
unif_in_gg(w(X6), black) → unif_out_gg(w(X6), 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(x1, x2)
UNIF_PAIRS_IN_G(x1)  =  UNIF_PAIRS_IN_G(x1)
U11_G(x1, x2, x3, x4)  =  U11_G(x1, x2, x3, x4)

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

(10) PiDPToQDPProof (SOUND transformation)

Transforming (infinitary) constructor rewriting Pi-DP problem [LOPSTR] into ordinary QDP problem [LPAR04] by application of Pi.

(11) Obligation:

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

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

The TRS R consists of the following rules:

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

The set Q consists of the following terms:

unif_in_gg(x0, x1)

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

(12) QDPSizeChangeProof (EQUIVALENT transformation)

By using the subterm criterion [SUBTERM_CRITERION] together with the size-change analysis [AAECC05] 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:

• UNIF_PAIRS_IN_G(.(A, .(B, Pairs))) → U11_G(A, B, Pairs, unif_in_gg(A, B))
  The graph contains the following edges 1 > 1, 1 > 2, 1 > 3

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

(13) TRUE

(14) Obligation:

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(X1), VXs)) → U6_ga(Xs, X1, VXs, varmat_in_ga(Xs, VXs))
U6_ga(Xs, X1, VXs, varmat_out_ga(Xs, VXs)) → varmat_out_ga(.(white, Xs), .(w(X1), 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(X5)) → unif_out_gg(black, w(X5))
unif_in_gg(w(X6), black) → unif_out_gg(w(X6), 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(.(X3, []), .(X4, [])) → unif_lines_out_gg(.(X3, []), .(X4, []))
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(.(X2, [])) → unif_matrx_out_g(.(X2, []))
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(x1, x3)
varmat_in_ga(x1, x2)  =  varmat_in_ga(x1)
[]  =  []
varmat_out_ga(x1, x2)  =  varmat_out_ga(x1, x2)
.(x1, x2)  =  .(x1, x2)
U3_ga(x1, x2, x3, x4, x5)  =  U3_ga(x1, x2, x5)
black  =  black
U5_ga(x1, x2, x3)  =  U5_ga(x1, x3)
white  =  white
U6_ga(x1, x2, x3, x4)  =  U6_ga(x1, x4)
w(x1)  =  w
U4_ga(x1, x2, x3, x4, x5)  =  U4_ga(x1, x2, x3, x5)
U2_ga(x1, x2, x3)  =  U2_ga(x1, x3)
unif_matrx_in_g(x1)  =  unif_matrx_in_g(x1)
U7_g(x1, x2, x3, x4)  =  U7_g(x1, 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(x1, x2, x3, x4, x5, x6, x7)
unif_pairs_in_g(x1)  =  unif_pairs_in_g(x1)
unif_pairs_out_g(x1)  =  unif_pairs_out_g(x1)
U11_g(x1, x2, x3, x4)  =  U11_g(x1, x2, x3, x4)
unif_in_gg(x1, x2)  =  unif_in_gg(x1, x2)
unif_out_gg(x1, x2)  =  unif_out_gg(x1, x2)
U12_g(x1, x2, x3, x4)  =  U12_g(x1, x2, x3, x4)
U10_gg(x1, x2, x3, x4, x5, x6, x7)  =  U10_gg(x1, x2, x3, x4, x5, x6, x7)
unif_lines_out_gg(x1, x2)  =  unif_lines_out_gg(x1, x2)
U8_g(x1, x2, x3, x4)  =  U8_g(x1, x2, x3, x4)
unif_matrx_out_g(x1)  =  unif_matrx_out_g(x1)
shapes_out_ga(x1, x2)  =  shapes_out_ga(x1)
UNIF_LINES_IN_GG(x1, x2)  =  UNIF_LINES_IN_GG(x1, x2)
U9_GG(x1, x2, x3, x4, x5, x6, x7)  =  U9_GG(x1, x2, x3, x4, x5, x6, x7)

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

(15) UsableRulesProof (EQUIVALENT transformation)

For (infinitary) constructor rewriting [LOPSTR] we can delete all non-usable rules from R.

(16) Obligation:

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(X5)) → unif_out_gg(black, w(X5))
unif_in_gg(w(X6), black) → unif_out_gg(w(X6), 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(x1)
U11_g(x1, x2, x3, x4)  =  U11_g(x1, x2, x3, x4)
unif_in_gg(x1, x2)  =  unif_in_gg(x1, x2)
unif_out_gg(x1, x2)  =  unif_out_gg(x1, x2)
U12_g(x1, x2, x3, x4)  =  U12_g(x1, 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(x1, x2, x3, x4, x5, x6, x7)

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

(17) PiDPToQDPProof (SOUND transformation)

Transforming (infinitary) constructor rewriting Pi-DP problem [LOPSTR] into ordinary QDP problem [LPAR04] by application of Pi.

(18) Obligation:

Q 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, w) → unif_out_gg(w, w)
unif_in_gg(black, black) → unif_out_gg(black, black)
unif_in_gg(black, w) → unif_out_gg(black, w)
unif_in_gg(w, black) → unif_out_gg(w, 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 set Q consists of the following terms:

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

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

(19) QDPOrderProof (EQUIVALENT transformation)

We use the reduction pair processor [LPAR04].

The following pairs can be oriented strictly and are deleted.

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 remaining pairs can at least be oriented weakly.
Used ordering: Polynomial interpretation [POLO]:

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

The following usable rules [FROCOS05] were oriented: none

(20) Obligation:

Q 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))

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, w) → unif_out_gg(w, w)
unif_in_gg(black, black) → unif_out_gg(black, black)
unif_in_gg(black, w) → unif_out_gg(black, w)
unif_in_gg(w, black) → unif_out_gg(w, 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 set Q consists of the following terms:

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

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

(21) DependencyGraphProof (EQUIVALENT transformation)

The approximation of the Dependency Graph [LPAR04,FROCOS05,EDGSTAR] contains 0 SCCs with 1 less node.

(22) TRUE

(23) Obligation:

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(X1), VXs)) → U6_ga(Xs, X1, VXs, varmat_in_ga(Xs, VXs))
U6_ga(Xs, X1, VXs, varmat_out_ga(Xs, VXs)) → varmat_out_ga(.(white, Xs), .(w(X1), 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(X5)) → unif_out_gg(black, w(X5))
unif_in_gg(w(X6), black) → unif_out_gg(w(X6), 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(.(X3, []), .(X4, [])) → unif_lines_out_gg(.(X3, []), .(X4, []))
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(.(X2, [])) → unif_matrx_out_g(.(X2, []))
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(x1, x3)
varmat_in_ga(x1, x2)  =  varmat_in_ga(x1)
[]  =  []
varmat_out_ga(x1, x2)  =  varmat_out_ga(x1, x2)
.(x1, x2)  =  .(x1, x2)
U3_ga(x1, x2, x3, x4, x5)  =  U3_ga(x1, x2, x5)
black  =  black
U5_ga(x1, x2, x3)  =  U5_ga(x1, x3)
white  =  white
U6_ga(x1, x2, x3, x4)  =  U6_ga(x1, x4)
w(x1)  =  w
U4_ga(x1, x2, x3, x4, x5)  =  U4_ga(x1, x2, x3, x5)
U2_ga(x1, x2, x3)  =  U2_ga(x1, x3)
unif_matrx_in_g(x1)  =  unif_matrx_in_g(x1)
U7_g(x1, x2, x3, x4)  =  U7_g(x1, 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(x1, x2, x3, x4, x5, x6, x7)
unif_pairs_in_g(x1)  =  unif_pairs_in_g(x1)
unif_pairs_out_g(x1)  =  unif_pairs_out_g(x1)
U11_g(x1, x2, x3, x4)  =  U11_g(x1, x2, x3, x4)
unif_in_gg(x1, x2)  =  unif_in_gg(x1, x2)
unif_out_gg(x1, x2)  =  unif_out_gg(x1, x2)
U12_g(x1, x2, x3, x4)  =  U12_g(x1, x2, x3, x4)
U10_gg(x1, x2, x3, x4, x5, x6, x7)  =  U10_gg(x1, x2, x3, x4, x5, x6, x7)
unif_lines_out_gg(x1, x2)  =  unif_lines_out_gg(x1, x2)
U8_g(x1, x2, x3, x4)  =  U8_g(x1, x2, x3, x4)
unif_matrx_out_g(x1)  =  unif_matrx_out_g(x1)
shapes_out_ga(x1, x2)  =  shapes_out_ga(x1)
UNIF_MATRX_IN_G(x1)  =  UNIF_MATRX_IN_G(x1)
U7_G(x1, x2, x3, x4)  =  U7_G(x1, x2, x3, x4)

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

(24) UsableRulesProof (EQUIVALENT transformation)

For (infinitary) constructor rewriting [LOPSTR] we can delete all non-usable rules from R.

(25) Obligation:

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(.(X3, []), .(X4, [])) → unif_lines_out_gg(.(X3, []), .(X4, []))
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(X5)) → unif_out_gg(black, w(X5))
unif_in_gg(w(X6), black) → unif_out_gg(w(X6), 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(x1, x2, x3, x4, x5, x6, x7)
unif_pairs_in_g(x1)  =  unif_pairs_in_g(x1)
unif_pairs_out_g(x1)  =  unif_pairs_out_g(x1)
U11_g(x1, x2, x3, x4)  =  U11_g(x1, x2, x3, x4)
unif_in_gg(x1, x2)  =  unif_in_gg(x1, x2)
unif_out_gg(x1, x2)  =  unif_out_gg(x1, x2)
U12_g(x1, x2, x3, x4)  =  U12_g(x1, x2, x3, x4)
U10_gg(x1, x2, x3, x4, x5, x6, x7)  =  U10_gg(x1, x2, x3, x4, x5, x6, x7)
unif_lines_out_gg(x1, x2)  =  unif_lines_out_gg(x1, x2)
UNIF_MATRX_IN_G(x1)  =  UNIF_MATRX_IN_G(x1)
U7_G(x1, x2, x3, x4)  =  U7_G(x1, x2, x3, x4)

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

(26) PiDPToQDPProof (SOUND transformation)

Transforming (infinitary) constructor rewriting Pi-DP problem [LOPSTR] into ordinary QDP problem [LPAR04] by application of Pi.

(27) Obligation:

Q 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(.(X3, []), .(X4, [])) → unif_lines_out_gg(.(X3, []), .(X4, []))
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, w) → unif_out_gg(w, w)
unif_in_gg(black, black) → unif_out_gg(black, black)
unif_in_gg(black, w) → unif_out_gg(black, w)
unif_in_gg(w, black) → unif_out_gg(w, 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 set Q consists of the following terms:

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

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

(28) Obligation:

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

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(.(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(X1), 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(X1), VXs)) → U6_ga(Xs, X1, VXs, varmat_in_ga(Xs, VXs))
U6_ga(Xs, X1, VXs, varmat_out_ga(Xs, VXs)) → varmat_out_ga(.(white, Xs), .(w(X1), 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(X5)) → unif_out_gg(black, w(X5))
unif_in_gg(w(X6), black) → unif_out_gg(w(X6), 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(.(X3, []), .(X4, [])) → unif_lines_out_gg(.(X3, []), .(X4, []))
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(.(X2, [])) → unif_matrx_out_g(.(X2, []))
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(x1, x3)
varmat_in_ga(x1, x2)  =  varmat_in_ga(x1)
[]  =  []
varmat_out_ga(x1, x2)  =  varmat_out_ga(x1, x2)
.(x1, x2)  =  .(x1, x2)
U3_ga(x1, x2, x3, x4, x5)  =  U3_ga(x1, x2, x5)
black  =  black
U5_ga(x1, x2, x3)  =  U5_ga(x1, x3)
white  =  white
U6_ga(x1, x2, x3, x4)  =  U6_ga(x1, x4)
w(x1)  =  w
U4_ga(x1, x2, x3, x4, x5)  =  U4_ga(x1, x2, x3, x5)
U2_ga(x1, x2, x3)  =  U2_ga(x1, x3)
unif_matrx_in_g(x1)  =  unif_matrx_in_g(x1)
U7_g(x1, x2, x3, x4)  =  U7_g(x1, 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(x1, x2, x3, x4, x5, x6, x7)
unif_pairs_in_g(x1)  =  unif_pairs_in_g(x1)
unif_pairs_out_g(x1)  =  unif_pairs_out_g(x1)
U11_g(x1, x2, x3, x4)  =  U11_g(x1, x2, x3, x4)
unif_in_gg(x1, x2)  =  unif_in_gg(x1, x2)
unif_out_gg(x1, x2)  =  unif_out_gg(x1, x2)
U12_g(x1, x2, x3, x4)  =  U12_g(x1, x2, x3, x4)
U10_gg(x1, x2, x3, x4, x5, x6, x7)  =  U10_gg(x1, x2, x3, x4, x5, x6, x7)
unif_lines_out_gg(x1, x2)  =  unif_lines_out_gg(x1, x2)
U8_g(x1, x2, x3, x4)  =  U8_g(x1, x2, x3, x4)
unif_matrx_out_g(x1)  =  unif_matrx_out_g(x1)
shapes_out_ga(x1, x2)  =  shapes_out_ga(x1)
VARMAT_IN_GA(x1, x2)  =  VARMAT_IN_GA(x1)
U3_GA(x1, x2, x3, x4, x5)  =  U3_GA(x1, x2, x5)

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

(29) UsableRulesProof (EQUIVALENT transformation)

For (infinitary) constructor rewriting [LOPSTR] we can delete all non-usable rules from R.

(30) Obligation:

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

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(.(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(X1), 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(X1), VXs)) → U6_ga(Xs, X1, 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, X1, VXs, varmat_out_ga(Xs, VXs)) → varmat_out_ga(.(white, Xs), .(w(X1), 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(x1, x2)
.(x1, x2)  =  .(x1, x2)
U3_ga(x1, x2, x3, x4, x5)  =  U3_ga(x1, x2, x5)
black  =  black
U5_ga(x1, x2, x3)  =  U5_ga(x1, x3)
white  =  white
U6_ga(x1, x2, x3, x4)  =  U6_ga(x1, x4)
w(x1)  =  w
U4_ga(x1, x2, x3, x4, x5)  =  U4_ga(x1, x2, x3, x5)
VARMAT_IN_GA(x1, x2)  =  VARMAT_IN_GA(x1)
U3_GA(x1, x2, x3, x4, x5)  =  U3_GA(x1, x2, x5)

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

(31) PrologToPiTRSProof (SOUND transformation)

We use the technique of [LOPSTR]. 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(X1), VXs)) → U6_ga(Xs, X1, VXs, varmat_in_ga(Xs, VXs))
U6_ga(Xs, X1, VXs, varmat_out_ga(Xs, VXs)) → varmat_out_ga(.(white, Xs), .(w(X1), 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(X5)) → unif_out_gg(black, w(X5))
unif_in_gg(w(X6), black) → unif_out_gg(w(X6), 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(.(X3, []), .(X4, [])) → unif_lines_out_gg(.(X3, []), .(X4, []))
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(.(X2, [])) → unif_matrx_out_g(.(X2, []))
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

Infinitary Constructor Rewriting Termination of PiTRS implies Termination of Prolog

(32) Obligation:

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(X1), VXs)) → U6_ga(Xs, X1, VXs, varmat_in_ga(Xs, VXs))
U6_ga(Xs, X1, VXs, varmat_out_ga(Xs, VXs)) → varmat_out_ga(.(white, Xs), .(w(X1), 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(X5)) → unif_out_gg(black, w(X5))
unif_in_gg(w(X6), black) → unif_out_gg(w(X6), 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(.(X3, []), .(X4, [])) → unif_lines_out_gg(.(X3, []), .(X4, []))
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(.(X2, [])) → unif_matrx_out_g(.(X2, []))
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

(33) DependencyPairsProof (EQUIVALENT transformation)

Using Dependency Pairs [AG00,LOPSTR] we result in the following initial DP problem:
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(X1), VXs)) → U6_GA(Xs, X1, VXs, varmat_in_ga(Xs, VXs))
VARMAT_IN_GA(.(white, Xs), .(w(X1), 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(X1), VXs)) → U6_ga(Xs, X1, VXs, varmat_in_ga(Xs, VXs))
U6_ga(Xs, X1, VXs, varmat_out_ga(Xs, VXs)) → varmat_out_ga(.(white, Xs), .(w(X1), 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(X5)) → unif_out_gg(black, w(X5))
unif_in_gg(w(X6), black) → unif_out_gg(w(X6), 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(.(X3, []), .(X4, [])) → unif_lines_out_gg(.(X3, []), .(X4, []))
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(.(X2, [])) → unif_matrx_out_g(.(X2, []))
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
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)
U3_GA(x1, x2, x3, x4, x5)  =  U3_GA(x2, x5)
U5_GA(x1, x2, x3)  =  U5_GA(x3)
U6_GA(x1, x2, x3, x4)  =  U6_GA(x4)
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)
U11_G(x1, x2, x3, x4)  =  U11_G(x3, x4)
UNIF_IN_GG(x1, x2)  =  UNIF_IN_GG(x1, x2)
U12_G(x1, x2, x3, x4)  =  U12_G(x4)
U10_GG(x1, x2, x3, x4, x5, x6, x7)  =  U10_GG(x7)
U8_G(x1, x2, x3, x4)  =  U8_G(x4)

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

(34) Obligation:

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(X1), VXs)) → U6_GA(Xs, X1, VXs, varmat_in_ga(Xs, VXs))
VARMAT_IN_GA(.(white, Xs), .(w(X1), 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(X1), VXs)) → U6_ga(Xs, X1, VXs, varmat_in_ga(Xs, VXs))
U6_ga(Xs, X1, VXs, varmat_out_ga(Xs, VXs)) → varmat_out_ga(.(white, Xs), .(w(X1), 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(X5)) → unif_out_gg(black, w(X5))
unif_in_gg(w(X6), black) → unif_out_gg(w(X6), 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(.(X3, []), .(X4, [])) → unif_lines_out_gg(.(X3, []), .(X4, []))
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(.(X2, [])) → unif_matrx_out_g(.(X2, []))
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
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)
U3_GA(x1, x2, x3, x4, x5)  =  U3_GA(x2, x5)
U5_GA(x1, x2, x3)  =  U5_GA(x3)
U6_GA(x1, x2, x3, x4)  =  U6_GA(x4)
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)
U11_G(x1, x2, x3, x4)  =  U11_G(x3, x4)
UNIF_IN_GG(x1, x2)  =  UNIF_IN_GG(x1, x2)
U12_G(x1, x2, x3, x4)  =  U12_G(x4)
U10_GG(x1, x2, x3, x4, x5, x6, x7)  =  U10_GG(x7)
U8_G(x1, x2, x3, x4)  =  U8_G(x4)

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

(35) DependencyGraphProof (EQUIVALENT transformation)

The approximation of the Dependency Graph [LOPSTR] contains 4 SCCs with 13 less nodes.

(36) Complex Obligation (AND)

(37) Obligation:

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

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

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(X1), VXs)) → U6_ga(Xs, X1, VXs, varmat_in_ga(Xs, VXs))
U6_ga(Xs, X1, VXs, varmat_out_ga(Xs, VXs)) → varmat_out_ga(.(white, Xs), .(w(X1), 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(X5)) → unif_out_gg(black, w(X5))
unif_in_gg(w(X6), black) → unif_out_gg(w(X6), 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(.(X3, []), .(X4, [])) → unif_lines_out_gg(.(X3, []), .(X4, []))
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(.(X2, [])) → unif_matrx_out_g(.(X2, []))
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
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

(38) UsableRulesProof (EQUIVALENT transformation)

For (infinitary) constructor rewriting [LOPSTR] we can delete all non-usable rules from R.

(39) Obligation:

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

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

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(X5)) → unif_out_gg(black, w(X5))
unif_in_gg(w(X6), black) → unif_out_gg(w(X6), 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

(40) PiDPToQDPProof (SOUND transformation)

Transforming (infinitary) constructor rewriting Pi-DP problem [LOPSTR] into ordinary QDP problem [LPAR04] by application of Pi.

(41) Obligation:

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.

(42) QDPSizeChangeProof (EQUIVALENT transformation)

By using the subterm criterion [SUBTERM_CRITERION] together with the size-change analysis [AAECC05] 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:

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

• U11_G(Pairs, unif_out_gg) → UNIF_PAIRS_IN_G(Pairs)
  The graph contains the following edges 1 >= 1

(43) TRUE

(44) Obligation:

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(X1), VXs)) → U6_ga(Xs, X1, VXs, varmat_in_ga(Xs, VXs))
U6_ga(Xs, X1, VXs, varmat_out_ga(Xs, VXs)) → varmat_out_ga(.(white, Xs), .(w(X1), 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(X5)) → unif_out_gg(black, w(X5))
unif_in_gg(w(X6), black) → unif_out_gg(w(X6), 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(.(X3, []), .(X4, [])) → unif_lines_out_gg(.(X3, []), .(X4, []))
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(.(X2, [])) → unif_matrx_out_g(.(X2, []))
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
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)

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

(45) UsableRulesProof (EQUIVALENT transformation)

For (infinitary) constructor rewriting [LOPSTR] we can delete all non-usable rules from R.

(46) Obligation:

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(X5)) → unif_out_gg(black, w(X5))
unif_in_gg(w(X6), black) → unif_out_gg(w(X6), 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)
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)

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

(47) PiDPToQDPProof (SOUND transformation)

Transforming (infinitary) constructor rewriting Pi-DP problem [LOPSTR] into ordinary QDP problem [LPAR04] by application of Pi.

(48) Obligation:

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, 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(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.

(49) QDPOrderProof (EQUIVALENT transformation)

We use the reduction pair processor [LPAR04].

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, unif_pairs_in_g(.(W, .(X, .(Y, .(Z, .(W, .(Y, .(X, .(Z, .(W, .(Z, .(X, .(Y, []))))))))))))))

The remaining pairs can at least be oriented weakly.
Used ordering: Polynomial interpretation [POLO]:

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) = 1   
POL(unif_in_gg(x₁, x₂)) = x₁ + x₂   
POL(unif_out_gg) = 1   
POL(unif_pairs_in_g(x₁)) = 0   
POL(unif_pairs_out_g) = 0   
POL(w) = 1   

The following usable rules [FROCOS05] were oriented: none

(50) Obligation:

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.

(51) DependencyGraphProof (EQUIVALENT transformation)

The approximation of the Dependency Graph [LPAR04,FROCOS05,EDGSTAR] contains 0 SCCs with 1 less node.

(52) TRUE

(53) Obligation:

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(X1), VXs)) → U6_ga(Xs, X1, VXs, varmat_in_ga(Xs, VXs))
U6_ga(Xs, X1, VXs, varmat_out_ga(Xs, VXs)) → varmat_out_ga(.(white, Xs), .(w(X1), 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(X5)) → unif_out_gg(black, w(X5))
unif_in_gg(w(X6), black) → unif_out_gg(w(X6), 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(.(X3, []), .(X4, [])) → unif_lines_out_gg(.(X3, []), .(X4, []))
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(.(X2, [])) → unif_matrx_out_g(.(X2, []))
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
UNIF_MATRX_IN_G(x1)  =  UNIF_MATRX_IN_G(x1)
U7_G(x1, x2, x3, x4)  =  U7_G(x2, x3, x4)

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

(54) UsableRulesProof (EQUIVALENT transformation)

For (infinitary) constructor rewriting [LOPSTR] we can delete all non-usable rules from R.

(55) Obligation:

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(.(X3, []), .(X4, [])) → unif_lines_out_gg(.(X3, []), .(X4, []))
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(X5)) → unif_out_gg(black, w(X5))
unif_in_gg(w(X6), black) → unif_out_gg(w(X6), 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
UNIF_MATRX_IN_G(x1)  =  UNIF_MATRX_IN_G(x1)
U7_G(x1, x2, x3, x4)  =  U7_G(x2, x3, x4)

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

(56) PiDPToQDPProof (SOUND transformation)

Transforming (infinitary) constructor rewriting Pi-DP problem [LOPSTR] into ordinary QDP problem [LPAR04] by application of Pi.

(57) Obligation:

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(.(X3, []), .(X4, [])) → 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.

(58) QDPOrderProof (EQUIVALENT transformation)

We use the reduction pair processor [LPAR04].

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.
Used ordering: Polynomial interpretation [POLO]:

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

The following usable rules [FROCOS05] were oriented: none

(59) Obligation:

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(.(X3, []), .(X4, [])) → 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.

(60) DependencyGraphProof (EQUIVALENT transformation)

The approximation of the Dependency Graph [LPAR04,FROCOS05,EDGSTAR] contains 0 SCCs with 1 less node.

(61) TRUE

(62) Obligation:

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

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(.(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(X1), 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(X1), VXs)) → U6_ga(Xs, X1, VXs, varmat_in_ga(Xs, VXs))
U6_ga(Xs, X1, VXs, varmat_out_ga(Xs, VXs)) → varmat_out_ga(.(white, Xs), .(w(X1), 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(X5)) → unif_out_gg(black, w(X5))
unif_in_gg(w(X6), black) → unif_out_gg(w(X6), 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(.(X3, []), .(X4, [])) → unif_lines_out_gg(.(X3, []), .(X4, []))
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(.(X2, [])) → unif_matrx_out_g(.(X2, []))
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
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

(63) UsableRulesProof (EQUIVALENT transformation)

For (infinitary) constructor rewriting [LOPSTR] we can delete all non-usable rules from R.

(64) Obligation:

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

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(.(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(X1), 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(X1), VXs)) → U6_ga(Xs, X1, 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, X1, VXs, varmat_out_ga(Xs, VXs)) → varmat_out_ga(.(white, Xs), .(w(X1), 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

(65) PiDPToQDPProof (SOUND transformation)

Transforming (infinitary) constructor rewriting Pi-DP problem [LOPSTR] into ordinary QDP problem [LPAR04] by application of Pi.

(66) Obligation:

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

U3_GA(Ls, varmat_out_ga(VL)) → VARMAT_IN_GA(Ls)
VARMAT_IN_GA(.(L, Ls)) → U3_GA(Ls, varmat_in_ga(L))
VARMAT_IN_GA(.(L, Ls)) → VARMAT_IN_GA(L)
VARMAT_IN_GA(.(black, Xs)) → VARMAT_IN_GA(Xs)
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.

(67) QDPSizeChangeProof (EQUIVALENT transformation)

By using the subterm criterion [SUBTERM_CRITERION] together with the size-change analysis [AAECC05] 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

(68) TRUE