Left Termination proof of ../tpdb/LP/talp/maria/mmatrix.pl

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

↳ Prolog

  ↳ PredefinedPredicateTransformerProof

Clauses:

mmultiply([], _, []).
mmultiply(.(V0, Rest), V1, .(Result, Others)) :- ','(mmultiply(Rest, V1, Others), multiply(V1, V0, Result)).
multiply([], _, []).
multiply(.(V0, Rest), V1, .(Result, Others)) :- ','(multiply(Rest, V1, Others), vmul(V0, V1, Result)).
vmul([], [], 0).
vmul(.(H1, T1), .(H2, T2), Result) :- ','(vmul(T1, T2, Newresult), ','(is(Product, *(H1, H2)), is(Result, +(Product, Newresult)))).
trans_m(.([], _), []).
trans_m(M, .(C1, Cn)) :- ','(trans_v(M, C1, R), trans_m(R, Cn)).
trans_v([], [], []).
trans_v(.(.(C11, C1n), C), .(C11, X), .(C1n, Y)) :- trans_v(C, X, Y).
makematrix(N, Matrix) :- ','(makevector(N, Vec), makematrix(N, Vec, Matrix)).
makematrix(0, _, []).
makematrix(Rows, Vector, .(Vector, T)) :- ','(>(Rows, 0), ','(is(Nextrow, -(Rows, 1)), makematrix(Nextrow, Vector, T))).
makevector(0, []).
makevector(Cols, .(Cols, T)) :- ','(>(Cols, 0), ','(is(Nextcol, -(Cols, 1)), makevector(Nextcol, T))).

Queries:

mmultiply(g,g,a).

Added definitions of predefined predicates.

↳ Prolog

  ↳ PredefinedPredicateTransformerProof

    ↳ Prolog

      ↳ PrologToPiTRSProof

Clauses:

mmultiply([], X, []).
mmultiply(.(V0, Rest), V1, .(Result, Others)) :- ','(mmultiply(Rest, V1, Others), multiply(V1, V0, Result)).
multiply([], X, []).
multiply(.(V0, Rest), V1, .(Result, Others)) :- ','(multiply(Rest, V1, Others), vmul(V0, V1, Result)).
vmul([], [], zero).
vmul(.(H1, T1), .(H2, T2), Result) :- ','(vmul(T1, T2, Newresult), ','(isTimes(H1, H2, U), ','(=(Product, U), ','(isPlus(Product, Newresult, U), =(Result, U))))).
trans_m(.([], X), []).
trans_m(M, .(C1, Cn)) :- ','(trans_v(M, C1, R), trans_m(R, Cn)).
trans_v([], [], []).
trans_v(.(.(C11, C1n), C), .(C11, X), .(C1n, Y)) :- trans_v(C, X, Y).
makematrix(N, Matrix) :- ','(makevector(N, Vec), makematrix(N, Vec, Matrix)).
makematrix(zero, X, []).
makematrix(Rows, Vector, .(Vector, T)) :- ','(=(X, Rows), ','(=(X1, zero), ','(isGreater(X, X1), ','(isMinus(Rows, succ(zero), U), ','(=(Nextrow, U), makematrix(Nextrow, Vector, T)))))).
makevector(zero, []).
makevector(Cols, .(Cols, T)) :- ','(=(X, Cols), ','(=(X1, zero), ','(isGreater(X, X1), ','(isMinus(Cols, succ(zero), U), ','(=(Nextcol, U), makevector(Nextcol, T)))))).
isPlus(zero, X, X).
isPlus(succ(X), zero, succ(X)).
isPlus(succ(X), succ(Y), succ(succ(Z))) :- isPlus(X, Y, Z).
isPlus(succ(X), pred(Y), Z) :- isPlus(X, Y, Z).
isPlus(pred(X), zero, pred(X)).
isPlus(pred(X), succ(Y), Z) :- isPlus(X, Y, Z).
isPlus(pred(X), pred(Y), pred(pred(Z))) :- isPlus(X, Y, Z).
isMinus(X, zero, X).
isMinus(zero, succ(Y), pred(Z)) :- isMinus(zero, Y, Z).
isMinus(zero, pred(Y), succ(Z)) :- isMinus(zero, Y, Z).
isMinus(succ(X), succ(Y), Z) :- isMinus(X, Y, Z).
isMinus(succ(X), pred(Y), succ(succ(Z))) :- isMinus(X, Y, Z).
isMinus(pred(X), succ(Y), pred(pred(Z))) :- isMinus(X, Y, Z).
isMinus(pred(X), pred(Y), Z) :- isMinus(X, Y, Z).
isTimes(X, zero, zero).
isTimes(zero, succ(Y), zero).
isTimes(zero, pred(Y), zero).
isTimes(succ(X), succ(Y), Z) :- ','(isTimes(succ(X), Y, A), isPlus(A, succ(X), Z)).
isTimes(succ(X), pred(Y), Z) :- ','(isTimes(succ(X), Y, A), isMinus(A, succ(X), Z)).
isTimes(pred(X), succ(Y), Z) :- ','(isTimes(pred(X), Y, A), isPlus(A, pred(X), Z)).
isTimes(pred(X), pred(Y), Z) :- ','(isTimes(pred(X), Y, A), isMinus(A, pred(X), Z)).
isDiv(zero, succ(Y), zero).
isDiv(zero, pred(Y), zero).
isDiv(succ(X), succ(Y), zero) :- isMinus(succ(X), succ(Y), pred(Z)).
isDiv(succ(X), succ(Y), succ(Z)) :- ','(isMinus(succ(X), succ(Y), A), isDiv(A, succ(Y), Z)).
isDiv(succ(X), pred(Y), Z) :- ','(isMinus(zero, pred(Y), A), ','(isDiv(succ(X), A, B), isMinus(zero, B, Z))).
isDiv(pred(X), pred(Y), zero) :- isMinus(pred(X), pred(Y), succ(Z)).
isDiv(pred(X), pred(Y), succ(Z)) :- ','(isMinus(pred(X), pred(Y), A), isDiv(A, pred(Y), Z)).
isDiv(pred(X), succ(Y), Z) :- ','(isMinus(zero, pred(X), A), ','(isDiv(A, succ(Y), B), isMinus(zero, B, Z))).
isModulo(X, Y, Z) :- ','(isDiv(X, Y, A), ','(isTimes(A, Y, B), isMinus(X, B, Z))).
=(X, X).
isGreater(succ(X), zero).
isGreater(succ(X), pred(Y)).
isGreater(succ(X), succ(Y)) :- isGreater(X, Y).
isGreater(zero, pred(Y)).
isGreater(pred(X), pred(Y)) :- isGreater(X, Y).

Queries:

mmultiply(g,g,a).

We use the technique of [30]. With regard to the inferred argument filtering the predicates were used in the following modes:
mmultiply_in: (b,b,f)
multiply_in: (b,b,f)
vmul_in: (b,b,f)
isTimes_in: (b,b,f)
isMinus_in: (b,b,f)
isPlus_in: (b,b,f) (b,b,b)
Transforming Prolog into the following Term Rewriting System:
Pi-finite rewrite system:
The TRS R consists of the following rules:

mmultiply_in_gga([], X, []) → mmultiply_out_gga([], X, [])
mmultiply_in_gga(.(V0, Rest), V1, .(Result, Others)) → U1_gga(V0, Rest, V1, Result, Others, mmultiply_in_gga(Rest, V1, Others))
U1_gga(V0, Rest, V1, Result, Others, mmultiply_out_gga(Rest, V1, Others)) → U2_gga(V0, Rest, V1, Result, Others, multiply_in_gga(V1, V0, Result))
multiply_in_gga([], X, []) → multiply_out_gga([], X, [])
multiply_in_gga(.(V0, Rest), V1, .(Result, Others)) → U3_gga(V0, Rest, V1, Result, Others, multiply_in_gga(Rest, V1, Others))
U3_gga(V0, Rest, V1, Result, Others, multiply_out_gga(Rest, V1, Others)) → U4_gga(V0, Rest, V1, Result, Others, vmul_in_gga(V0, V1, Result))
vmul_in_gga([], [], zero) → vmul_out_gga([], [], zero)
vmul_in_gga(.(H1, T1), .(H2, T2), Result) → U5_gga(H1, T1, H2, T2, Result, vmul_in_gga(T1, T2, Newresult))
U5_gga(H1, T1, H2, T2, Result, vmul_out_gga(T1, T2, Newresult)) → U6_gga(H1, T1, H2, T2, Result, Newresult, isTimes_in_gga(H1, H2, U))
isTimes_in_gga(X, zero, zero) → isTimes_out_gga(X, zero, zero)
isTimes_in_gga(zero, succ(Y), zero) → isTimes_out_gga(zero, succ(Y), zero)
isTimes_in_gga(zero, pred(Y), zero) → isTimes_out_gga(zero, pred(Y), zero)
isTimes_in_gga(succ(X), succ(Y), Z) → U37_gga(X, Y, Z, isTimes_in_gga(succ(X), Y, A))
isTimes_in_gga(succ(X), pred(Y), Z) → U39_gga(X, Y, Z, isTimes_in_gga(succ(X), Y, A))
isTimes_in_gga(pred(X), succ(Y), Z) → U41_gga(X, Y, Z, isTimes_in_gga(pred(X), Y, A))
isTimes_in_gga(pred(X), pred(Y), Z) → U43_gga(X, Y, Z, isTimes_in_gga(pred(X), Y, A))
U43_gga(X, Y, Z, isTimes_out_gga(pred(X), Y, A)) → U44_gga(X, Y, Z, isMinus_in_gga(A, pred(X), Z))
isMinus_in_gga(X, zero, X) → isMinus_out_gga(X, zero, X)
isMinus_in_gga(zero, succ(Y), pred(Z)) → U31_gga(Y, Z, isMinus_in_gga(zero, Y, Z))
isMinus_in_gga(zero, pred(Y), succ(Z)) → U32_gga(Y, Z, isMinus_in_gga(zero, Y, Z))
isMinus_in_gga(succ(X), succ(Y), Z) → U33_gga(X, Y, Z, isMinus_in_gga(X, Y, Z))
isMinus_in_gga(succ(X), pred(Y), succ(succ(Z))) → U34_gga(X, Y, Z, isMinus_in_gga(X, Y, Z))
isMinus_in_gga(pred(X), succ(Y), pred(pred(Z))) → U35_gga(X, Y, Z, isMinus_in_gga(X, Y, Z))
isMinus_in_gga(pred(X), pred(Y), Z) → U36_gga(X, Y, Z, isMinus_in_gga(X, Y, Z))
U36_gga(X, Y, Z, isMinus_out_gga(X, Y, Z)) → isMinus_out_gga(pred(X), pred(Y), Z)
U35_gga(X, Y, Z, isMinus_out_gga(X, Y, Z)) → isMinus_out_gga(pred(X), succ(Y), pred(pred(Z)))
U34_gga(X, Y, Z, isMinus_out_gga(X, Y, Z)) → isMinus_out_gga(succ(X), pred(Y), succ(succ(Z)))
U33_gga(X, Y, Z, isMinus_out_gga(X, Y, Z)) → isMinus_out_gga(succ(X), succ(Y), Z)
U32_gga(Y, Z, isMinus_out_gga(zero, Y, Z)) → isMinus_out_gga(zero, pred(Y), succ(Z))
U31_gga(Y, Z, isMinus_out_gga(zero, Y, Z)) → isMinus_out_gga(zero, succ(Y), pred(Z))
U44_gga(X, Y, Z, isMinus_out_gga(A, pred(X), Z)) → isTimes_out_gga(pred(X), pred(Y), Z)
U41_gga(X, Y, Z, isTimes_out_gga(pred(X), Y, A)) → U42_gga(X, Y, Z, isPlus_in_gga(A, pred(X), Z))
isPlus_in_gga(zero, X, X) → isPlus_out_gga(zero, X, X)
isPlus_in_gga(succ(X), zero, succ(X)) → isPlus_out_gga(succ(X), zero, succ(X))
isPlus_in_gga(succ(X), succ(Y), succ(succ(Z))) → U27_gga(X, Y, Z, isPlus_in_gga(X, Y, Z))
isPlus_in_gga(succ(X), pred(Y), Z) → U28_gga(X, Y, Z, isPlus_in_gga(X, Y, Z))
isPlus_in_gga(pred(X), zero, pred(X)) → isPlus_out_gga(pred(X), zero, pred(X))
isPlus_in_gga(pred(X), succ(Y), Z) → U29_gga(X, Y, Z, isPlus_in_gga(X, Y, Z))
isPlus_in_gga(pred(X), pred(Y), pred(pred(Z))) → U30_gga(X, Y, Z, isPlus_in_gga(X, Y, Z))
U30_gga(X, Y, Z, isPlus_out_gga(X, Y, Z)) → isPlus_out_gga(pred(X), pred(Y), pred(pred(Z)))
U29_gga(X, Y, Z, isPlus_out_gga(X, Y, Z)) → isPlus_out_gga(pred(X), succ(Y), Z)
U28_gga(X, Y, Z, isPlus_out_gga(X, Y, Z)) → isPlus_out_gga(succ(X), pred(Y), Z)
U27_gga(X, Y, Z, isPlus_out_gga(X, Y, Z)) → isPlus_out_gga(succ(X), succ(Y), succ(succ(Z)))
U42_gga(X, Y, Z, isPlus_out_gga(A, pred(X), Z)) → isTimes_out_gga(pred(X), succ(Y), Z)
U39_gga(X, Y, Z, isTimes_out_gga(succ(X), Y, A)) → U40_gga(X, Y, Z, isMinus_in_gga(A, succ(X), Z))
U40_gga(X, Y, Z, isMinus_out_gga(A, succ(X), Z)) → isTimes_out_gga(succ(X), pred(Y), Z)
U37_gga(X, Y, Z, isTimes_out_gga(succ(X), Y, A)) → U38_gga(X, Y, Z, isPlus_in_gga(A, succ(X), Z))
U38_gga(X, Y, Z, isPlus_out_gga(A, succ(X), Z)) → isTimes_out_gga(succ(X), succ(Y), Z)
U6_gga(H1, T1, H2, T2, Result, Newresult, isTimes_out_gga(H1, H2, U)) → U7_gga(H1, T1, H2, T2, Result, Newresult, U, =_in_ag(Product, U))
=_in_ag(X, X) → =_out_ag(X, X)
U7_gga(H1, T1, H2, T2, Result, Newresult, U, =_out_ag(Product, U)) → U8_gga(H1, T1, H2, T2, Result, U, isPlus_in_ggg(Product, Newresult, U))
isPlus_in_ggg(zero, X, X) → isPlus_out_ggg(zero, X, X)
isPlus_in_ggg(succ(X), zero, succ(X)) → isPlus_out_ggg(succ(X), zero, succ(X))
isPlus_in_ggg(succ(X), succ(Y), succ(succ(Z))) → U27_ggg(X, Y, Z, isPlus_in_ggg(X, Y, Z))
isPlus_in_ggg(succ(X), pred(Y), Z) → U28_ggg(X, Y, Z, isPlus_in_ggg(X, Y, Z))
isPlus_in_ggg(pred(X), zero, pred(X)) → isPlus_out_ggg(pred(X), zero, pred(X))
isPlus_in_ggg(pred(X), succ(Y), Z) → U29_ggg(X, Y, Z, isPlus_in_ggg(X, Y, Z))
isPlus_in_ggg(pred(X), pred(Y), pred(pred(Z))) → U30_ggg(X, Y, Z, isPlus_in_ggg(X, Y, Z))
U30_ggg(X, Y, Z, isPlus_out_ggg(X, Y, Z)) → isPlus_out_ggg(pred(X), pred(Y), pred(pred(Z)))
U29_ggg(X, Y, Z, isPlus_out_ggg(X, Y, Z)) → isPlus_out_ggg(pred(X), succ(Y), Z)
U28_ggg(X, Y, Z, isPlus_out_ggg(X, Y, Z)) → isPlus_out_ggg(succ(X), pred(Y), Z)
U27_ggg(X, Y, Z, isPlus_out_ggg(X, Y, Z)) → isPlus_out_ggg(succ(X), succ(Y), succ(succ(Z)))
U8_gga(H1, T1, H2, T2, Result, U, isPlus_out_ggg(Product, Newresult, U)) → U9_gga(H1, T1, H2, T2, Result, =_in_ag(Result, U))
U9_gga(H1, T1, H2, T2, Result, =_out_ag(Result, U)) → vmul_out_gga(.(H1, T1), .(H2, T2), Result)
U4_gga(V0, Rest, V1, Result, Others, vmul_out_gga(V0, V1, Result)) → multiply_out_gga(.(V0, Rest), V1, .(Result, Others))
U2_gga(V0, Rest, V1, Result, Others, multiply_out_gga(V1, V0, Result)) → mmultiply_out_gga(.(V0, Rest), V1, .(Result, Others))

Infinitary Constructor Rewriting Termination of PiTRS implies Termination of Prolog

↳ Prolog

  ↳ PredefinedPredicateTransformerProof

    ↳ Prolog

      ↳ PrologToPiTRSProof

        ↳ PiTRS

          ↳ DependencyPairsProof

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

mmultiply_in_gga([], X, []) → mmultiply_out_gga([], X, [])
mmultiply_in_gga(.(V0, Rest), V1, .(Result, Others)) → U1_gga(V0, Rest, V1, Result, Others, mmultiply_in_gga(Rest, V1, Others))
U1_gga(V0, Rest, V1, Result, Others, mmultiply_out_gga(Rest, V1, Others)) → U2_gga(V0, Rest, V1, Result, Others, multiply_in_gga(V1, V0, Result))
multiply_in_gga([], X, []) → multiply_out_gga([], X, [])
multiply_in_gga(.(V0, Rest), V1, .(Result, Others)) → U3_gga(V0, Rest, V1, Result, Others, multiply_in_gga(Rest, V1, Others))
U3_gga(V0, Rest, V1, Result, Others, multiply_out_gga(Rest, V1, Others)) → U4_gga(V0, Rest, V1, Result, Others, vmul_in_gga(V0, V1, Result))
vmul_in_gga([], [], zero) → vmul_out_gga([], [], zero)
vmul_in_gga(.(H1, T1), .(H2, T2), Result) → U5_gga(H1, T1, H2, T2, Result, vmul_in_gga(T1, T2, Newresult))
U5_gga(H1, T1, H2, T2, Result, vmul_out_gga(T1, T2, Newresult)) → U6_gga(H1, T1, H2, T2, Result, Newresult, isTimes_in_gga(H1, H2, U))
isTimes_in_gga(X, zero, zero) → isTimes_out_gga(X, zero, zero)
isTimes_in_gga(zero, succ(Y), zero) → isTimes_out_gga(zero, succ(Y), zero)
isTimes_in_gga(zero, pred(Y), zero) → isTimes_out_gga(zero, pred(Y), zero)
isTimes_in_gga(succ(X), succ(Y), Z) → U37_gga(X, Y, Z, isTimes_in_gga(succ(X), Y, A))
isTimes_in_gga(succ(X), pred(Y), Z) → U39_gga(X, Y, Z, isTimes_in_gga(succ(X), Y, A))
isTimes_in_gga(pred(X), succ(Y), Z) → U41_gga(X, Y, Z, isTimes_in_gga(pred(X), Y, A))
isTimes_in_gga(pred(X), pred(Y), Z) → U43_gga(X, Y, Z, isTimes_in_gga(pred(X), Y, A))
U43_gga(X, Y, Z, isTimes_out_gga(pred(X), Y, A)) → U44_gga(X, Y, Z, isMinus_in_gga(A, pred(X), Z))
isMinus_in_gga(X, zero, X) → isMinus_out_gga(X, zero, X)
isMinus_in_gga(zero, succ(Y), pred(Z)) → U31_gga(Y, Z, isMinus_in_gga(zero, Y, Z))
isMinus_in_gga(zero, pred(Y), succ(Z)) → U32_gga(Y, Z, isMinus_in_gga(zero, Y, Z))
isMinus_in_gga(succ(X), succ(Y), Z) → U33_gga(X, Y, Z, isMinus_in_gga(X, Y, Z))
isMinus_in_gga(succ(X), pred(Y), succ(succ(Z))) → U34_gga(X, Y, Z, isMinus_in_gga(X, Y, Z))
isMinus_in_gga(pred(X), succ(Y), pred(pred(Z))) → U35_gga(X, Y, Z, isMinus_in_gga(X, Y, Z))
isMinus_in_gga(pred(X), pred(Y), Z) → U36_gga(X, Y, Z, isMinus_in_gga(X, Y, Z))
U36_gga(X, Y, Z, isMinus_out_gga(X, Y, Z)) → isMinus_out_gga(pred(X), pred(Y), Z)
U35_gga(X, Y, Z, isMinus_out_gga(X, Y, Z)) → isMinus_out_gga(pred(X), succ(Y), pred(pred(Z)))
U34_gga(X, Y, Z, isMinus_out_gga(X, Y, Z)) → isMinus_out_gga(succ(X), pred(Y), succ(succ(Z)))
U33_gga(X, Y, Z, isMinus_out_gga(X, Y, Z)) → isMinus_out_gga(succ(X), succ(Y), Z)
U32_gga(Y, Z, isMinus_out_gga(zero, Y, Z)) → isMinus_out_gga(zero, pred(Y), succ(Z))
U31_gga(Y, Z, isMinus_out_gga(zero, Y, Z)) → isMinus_out_gga(zero, succ(Y), pred(Z))
U44_gga(X, Y, Z, isMinus_out_gga(A, pred(X), Z)) → isTimes_out_gga(pred(X), pred(Y), Z)
U41_gga(X, Y, Z, isTimes_out_gga(pred(X), Y, A)) → U42_gga(X, Y, Z, isPlus_in_gga(A, pred(X), Z))
isPlus_in_gga(zero, X, X) → isPlus_out_gga(zero, X, X)
isPlus_in_gga(succ(X), zero, succ(X)) → isPlus_out_gga(succ(X), zero, succ(X))
isPlus_in_gga(succ(X), succ(Y), succ(succ(Z))) → U27_gga(X, Y, Z, isPlus_in_gga(X, Y, Z))
isPlus_in_gga(succ(X), pred(Y), Z) → U28_gga(X, Y, Z, isPlus_in_gga(X, Y, Z))
isPlus_in_gga(pred(X), zero, pred(X)) → isPlus_out_gga(pred(X), zero, pred(X))
isPlus_in_gga(pred(X), succ(Y), Z) → U29_gga(X, Y, Z, isPlus_in_gga(X, Y, Z))
isPlus_in_gga(pred(X), pred(Y), pred(pred(Z))) → U30_gga(X, Y, Z, isPlus_in_gga(X, Y, Z))
U30_gga(X, Y, Z, isPlus_out_gga(X, Y, Z)) → isPlus_out_gga(pred(X), pred(Y), pred(pred(Z)))
U29_gga(X, Y, Z, isPlus_out_gga(X, Y, Z)) → isPlus_out_gga(pred(X), succ(Y), Z)
U28_gga(X, Y, Z, isPlus_out_gga(X, Y, Z)) → isPlus_out_gga(succ(X), pred(Y), Z)
U27_gga(X, Y, Z, isPlus_out_gga(X, Y, Z)) → isPlus_out_gga(succ(X), succ(Y), succ(succ(Z)))
U42_gga(X, Y, Z, isPlus_out_gga(A, pred(X), Z)) → isTimes_out_gga(pred(X), succ(Y), Z)
U39_gga(X, Y, Z, isTimes_out_gga(succ(X), Y, A)) → U40_gga(X, Y, Z, isMinus_in_gga(A, succ(X), Z))
U40_gga(X, Y, Z, isMinus_out_gga(A, succ(X), Z)) → isTimes_out_gga(succ(X), pred(Y), Z)
U37_gga(X, Y, Z, isTimes_out_gga(succ(X), Y, A)) → U38_gga(X, Y, Z, isPlus_in_gga(A, succ(X), Z))
U38_gga(X, Y, Z, isPlus_out_gga(A, succ(X), Z)) → isTimes_out_gga(succ(X), succ(Y), Z)
U6_gga(H1, T1, H2, T2, Result, Newresult, isTimes_out_gga(H1, H2, U)) → U7_gga(H1, T1, H2, T2, Result, Newresult, U, =_in_ag(Product, U))
=_in_ag(X, X) → =_out_ag(X, X)
U7_gga(H1, T1, H2, T2, Result, Newresult, U, =_out_ag(Product, U)) → U8_gga(H1, T1, H2, T2, Result, U, isPlus_in_ggg(Product, Newresult, U))
isPlus_in_ggg(zero, X, X) → isPlus_out_ggg(zero, X, X)
isPlus_in_ggg(succ(X), zero, succ(X)) → isPlus_out_ggg(succ(X), zero, succ(X))
isPlus_in_ggg(succ(X), succ(Y), succ(succ(Z))) → U27_ggg(X, Y, Z, isPlus_in_ggg(X, Y, Z))
isPlus_in_ggg(succ(X), pred(Y), Z) → U28_ggg(X, Y, Z, isPlus_in_ggg(X, Y, Z))
isPlus_in_ggg(pred(X), zero, pred(X)) → isPlus_out_ggg(pred(X), zero, pred(X))
isPlus_in_ggg(pred(X), succ(Y), Z) → U29_ggg(X, Y, Z, isPlus_in_ggg(X, Y, Z))
isPlus_in_ggg(pred(X), pred(Y), pred(pred(Z))) → U30_ggg(X, Y, Z, isPlus_in_ggg(X, Y, Z))
U30_ggg(X, Y, Z, isPlus_out_ggg(X, Y, Z)) → isPlus_out_ggg(pred(X), pred(Y), pred(pred(Z)))
U29_ggg(X, Y, Z, isPlus_out_ggg(X, Y, Z)) → isPlus_out_ggg(pred(X), succ(Y), Z)
U28_ggg(X, Y, Z, isPlus_out_ggg(X, Y, Z)) → isPlus_out_ggg(succ(X), pred(Y), Z)
U27_ggg(X, Y, Z, isPlus_out_ggg(X, Y, Z)) → isPlus_out_ggg(succ(X), succ(Y), succ(succ(Z)))
U8_gga(H1, T1, H2, T2, Result, U, isPlus_out_ggg(Product, Newresult, U)) → U9_gga(H1, T1, H2, T2, Result, =_in_ag(Result, U))
U9_gga(H1, T1, H2, T2, Result, =_out_ag(Result, U)) → vmul_out_gga(.(H1, T1), .(H2, T2), Result)
U4_gga(V0, Rest, V1, Result, Others, vmul_out_gga(V0, V1, Result)) → multiply_out_gga(.(V0, Rest), V1, .(Result, Others))
U2_gga(V0, Rest, V1, Result, Others, multiply_out_gga(V1, V0, Result)) → mmultiply_out_gga(.(V0, Rest), V1, .(Result, Others))

MMULTIPLY_IN_GGA(.(V0, Rest), V1, .(Result, Others)) → U1_GGA(V0, Rest, V1, Result, Others, mmultiply_in_gga(Rest, V1, Others))
MMULTIPLY_IN_GGA(.(V0, Rest), V1, .(Result, Others)) → MMULTIPLY_IN_GGA(Rest, V1, Others)
U1_GGA(V0, Rest, V1, Result, Others, mmultiply_out_gga(Rest, V1, Others)) → U2_GGA(V0, Rest, V1, Result, Others, multiply_in_gga(V1, V0, Result))
U1_GGA(V0, Rest, V1, Result, Others, mmultiply_out_gga(Rest, V1, Others)) → MULTIPLY_IN_GGA(V1, V0, Result)
MULTIPLY_IN_GGA(.(V0, Rest), V1, .(Result, Others)) → U3_GGA(V0, Rest, V1, Result, Others, multiply_in_gga(Rest, V1, Others))
MULTIPLY_IN_GGA(.(V0, Rest), V1, .(Result, Others)) → MULTIPLY_IN_GGA(Rest, V1, Others)
U3_GGA(V0, Rest, V1, Result, Others, multiply_out_gga(Rest, V1, Others)) → U4_GGA(V0, Rest, V1, Result, Others, vmul_in_gga(V0, V1, Result))
U3_GGA(V0, Rest, V1, Result, Others, multiply_out_gga(Rest, V1, Others)) → VMUL_IN_GGA(V0, V1, Result)
VMUL_IN_GGA(.(H1, T1), .(H2, T2), Result) → U5_GGA(H1, T1, H2, T2, Result, vmul_in_gga(T1, T2, Newresult))
VMUL_IN_GGA(.(H1, T1), .(H2, T2), Result) → VMUL_IN_GGA(T1, T2, Newresult)
U5_GGA(H1, T1, H2, T2, Result, vmul_out_gga(T1, T2, Newresult)) → U6_GGA(H1, T1, H2, T2, Result, Newresult, isTimes_in_gga(H1, H2, U))
U5_GGA(H1, T1, H2, T2, Result, vmul_out_gga(T1, T2, Newresult)) → ISTIMES_IN_GGA(H1, H2, U)
ISTIMES_IN_GGA(succ(X), succ(Y), Z) → U37_GGA(X, Y, Z, isTimes_in_gga(succ(X), Y, A))
ISTIMES_IN_GGA(succ(X), succ(Y), Z) → ISTIMES_IN_GGA(succ(X), Y, A)
ISTIMES_IN_GGA(succ(X), pred(Y), Z) → U39_GGA(X, Y, Z, isTimes_in_gga(succ(X), Y, A))
ISTIMES_IN_GGA(succ(X), pred(Y), Z) → ISTIMES_IN_GGA(succ(X), Y, A)
ISTIMES_IN_GGA(pred(X), succ(Y), Z) → U41_GGA(X, Y, Z, isTimes_in_gga(pred(X), Y, A))
ISTIMES_IN_GGA(pred(X), succ(Y), Z) → ISTIMES_IN_GGA(pred(X), Y, A)
ISTIMES_IN_GGA(pred(X), pred(Y), Z) → U43_GGA(X, Y, Z, isTimes_in_gga(pred(X), Y, A))
ISTIMES_IN_GGA(pred(X), pred(Y), Z) → ISTIMES_IN_GGA(pred(X), Y, A)
U43_GGA(X, Y, Z, isTimes_out_gga(pred(X), Y, A)) → U44_GGA(X, Y, Z, isMinus_in_gga(A, pred(X), Z))
U43_GGA(X, Y, Z, isTimes_out_gga(pred(X), Y, A)) → ISMINUS_IN_GGA(A, pred(X), Z)
ISMINUS_IN_GGA(zero, succ(Y), pred(Z)) → U31_GGA(Y, Z, isMinus_in_gga(zero, Y, Z))
ISMINUS_IN_GGA(zero, succ(Y), pred(Z)) → ISMINUS_IN_GGA(zero, Y, Z)
ISMINUS_IN_GGA(zero, pred(Y), succ(Z)) → U32_GGA(Y, Z, isMinus_in_gga(zero, Y, Z))
ISMINUS_IN_GGA(zero, pred(Y), succ(Z)) → ISMINUS_IN_GGA(zero, Y, Z)
ISMINUS_IN_GGA(succ(X), succ(Y), Z) → U33_GGA(X, Y, Z, isMinus_in_gga(X, Y, Z))
ISMINUS_IN_GGA(succ(X), succ(Y), Z) → ISMINUS_IN_GGA(X, Y, Z)
ISMINUS_IN_GGA(succ(X), pred(Y), succ(succ(Z))) → U34_GGA(X, Y, Z, isMinus_in_gga(X, Y, Z))
ISMINUS_IN_GGA(succ(X), pred(Y), succ(succ(Z))) → ISMINUS_IN_GGA(X, Y, Z)
ISMINUS_IN_GGA(pred(X), succ(Y), pred(pred(Z))) → U35_GGA(X, Y, Z, isMinus_in_gga(X, Y, Z))
ISMINUS_IN_GGA(pred(X), succ(Y), pred(pred(Z))) → ISMINUS_IN_GGA(X, Y, Z)
ISMINUS_IN_GGA(pred(X), pred(Y), Z) → U36_GGA(X, Y, Z, isMinus_in_gga(X, Y, Z))
ISMINUS_IN_GGA(pred(X), pred(Y), Z) → ISMINUS_IN_GGA(X, Y, Z)
U41_GGA(X, Y, Z, isTimes_out_gga(pred(X), Y, A)) → U42_GGA(X, Y, Z, isPlus_in_gga(A, pred(X), Z))
U41_GGA(X, Y, Z, isTimes_out_gga(pred(X), Y, A)) → ISPLUS_IN_GGA(A, pred(X), Z)
ISPLUS_IN_GGA(succ(X), succ(Y), succ(succ(Z))) → U27_GGA(X, Y, Z, isPlus_in_gga(X, Y, Z))
ISPLUS_IN_GGA(succ(X), succ(Y), succ(succ(Z))) → ISPLUS_IN_GGA(X, Y, Z)
ISPLUS_IN_GGA(succ(X), pred(Y), Z) → U28_GGA(X, Y, Z, isPlus_in_gga(X, Y, Z))
ISPLUS_IN_GGA(succ(X), pred(Y), Z) → ISPLUS_IN_GGA(X, Y, Z)
ISPLUS_IN_GGA(pred(X), succ(Y), Z) → U29_GGA(X, Y, Z, isPlus_in_gga(X, Y, Z))
ISPLUS_IN_GGA(pred(X), succ(Y), Z) → ISPLUS_IN_GGA(X, Y, Z)
ISPLUS_IN_GGA(pred(X), pred(Y), pred(pred(Z))) → U30_GGA(X, Y, Z, isPlus_in_gga(X, Y, Z))
ISPLUS_IN_GGA(pred(X), pred(Y), pred(pred(Z))) → ISPLUS_IN_GGA(X, Y, Z)
U39_GGA(X, Y, Z, isTimes_out_gga(succ(X), Y, A)) → U40_GGA(X, Y, Z, isMinus_in_gga(A, succ(X), Z))
U39_GGA(X, Y, Z, isTimes_out_gga(succ(X), Y, A)) → ISMINUS_IN_GGA(A, succ(X), Z)
U37_GGA(X, Y, Z, isTimes_out_gga(succ(X), Y, A)) → U38_GGA(X, Y, Z, isPlus_in_gga(A, succ(X), Z))
U37_GGA(X, Y, Z, isTimes_out_gga(succ(X), Y, A)) → ISPLUS_IN_GGA(A, succ(X), Z)
U6_GGA(H1, T1, H2, T2, Result, Newresult, isTimes_out_gga(H1, H2, U)) → U7_GGA(H1, T1, H2, T2, Result, Newresult, U, =_in_ag(Product, U))
U6_GGA(H1, T1, H2, T2, Result, Newresult, isTimes_out_gga(H1, H2, U)) → =_IN_AG(Product, U)
U7_GGA(H1, T1, H2, T2, Result, Newresult, U, =_out_ag(Product, U)) → U8_GGA(H1, T1, H2, T2, Result, U, isPlus_in_ggg(Product, Newresult, U))
U7_GGA(H1, T1, H2, T2, Result, Newresult, U, =_out_ag(Product, U)) → ISPLUS_IN_GGG(Product, Newresult, U)
ISPLUS_IN_GGG(succ(X), succ(Y), succ(succ(Z))) → U27_GGG(X, Y, Z, isPlus_in_ggg(X, Y, Z))
ISPLUS_IN_GGG(succ(X), succ(Y), succ(succ(Z))) → ISPLUS_IN_GGG(X, Y, Z)
ISPLUS_IN_GGG(succ(X), pred(Y), Z) → U28_GGG(X, Y, Z, isPlus_in_ggg(X, Y, Z))
ISPLUS_IN_GGG(succ(X), pred(Y), Z) → ISPLUS_IN_GGG(X, Y, Z)
ISPLUS_IN_GGG(pred(X), succ(Y), Z) → U29_GGG(X, Y, Z, isPlus_in_ggg(X, Y, Z))
ISPLUS_IN_GGG(pred(X), succ(Y), Z) → ISPLUS_IN_GGG(X, Y, Z)
ISPLUS_IN_GGG(pred(X), pred(Y), pred(pred(Z))) → U30_GGG(X, Y, Z, isPlus_in_ggg(X, Y, Z))
ISPLUS_IN_GGG(pred(X), pred(Y), pred(pred(Z))) → ISPLUS_IN_GGG(X, Y, Z)
U8_GGA(H1, T1, H2, T2, Result, U, isPlus_out_ggg(Product, Newresult, U)) → U9_GGA(H1, T1, H2, T2, Result, =_in_ag(Result, U))
U8_GGA(H1, T1, H2, T2, Result, U, isPlus_out_ggg(Product, Newresult, U)) → =_IN_AG(Result, U)

The TRS R consists of the following rules:

mmultiply_in_gga([], X, []) → mmultiply_out_gga([], X, [])
mmultiply_in_gga(.(V0, Rest), V1, .(Result, Others)) → U1_gga(V0, Rest, V1, Result, Others, mmultiply_in_gga(Rest, V1, Others))
U1_gga(V0, Rest, V1, Result, Others, mmultiply_out_gga(Rest, V1, Others)) → U2_gga(V0, Rest, V1, Result, Others, multiply_in_gga(V1, V0, Result))
multiply_in_gga([], X, []) → multiply_out_gga([], X, [])
multiply_in_gga(.(V0, Rest), V1, .(Result, Others)) → U3_gga(V0, Rest, V1, Result, Others, multiply_in_gga(Rest, V1, Others))
U3_gga(V0, Rest, V1, Result, Others, multiply_out_gga(Rest, V1, Others)) → U4_gga(V0, Rest, V1, Result, Others, vmul_in_gga(V0, V1, Result))
vmul_in_gga([], [], zero) → vmul_out_gga([], [], zero)
vmul_in_gga(.(H1, T1), .(H2, T2), Result) → U5_gga(H1, T1, H2, T2, Result, vmul_in_gga(T1, T2, Newresult))
U5_gga(H1, T1, H2, T2, Result, vmul_out_gga(T1, T2, Newresult)) → U6_gga(H1, T1, H2, T2, Result, Newresult, isTimes_in_gga(H1, H2, U))
isTimes_in_gga(X, zero, zero) → isTimes_out_gga(X, zero, zero)
isTimes_in_gga(zero, succ(Y), zero) → isTimes_out_gga(zero, succ(Y), zero)
isTimes_in_gga(zero, pred(Y), zero) → isTimes_out_gga(zero, pred(Y), zero)
isTimes_in_gga(succ(X), succ(Y), Z) → U37_gga(X, Y, Z, isTimes_in_gga(succ(X), Y, A))
isTimes_in_gga(succ(X), pred(Y), Z) → U39_gga(X, Y, Z, isTimes_in_gga(succ(X), Y, A))
isTimes_in_gga(pred(X), succ(Y), Z) → U41_gga(X, Y, Z, isTimes_in_gga(pred(X), Y, A))
isTimes_in_gga(pred(X), pred(Y), Z) → U43_gga(X, Y, Z, isTimes_in_gga(pred(X), Y, A))
U43_gga(X, Y, Z, isTimes_out_gga(pred(X), Y, A)) → U44_gga(X, Y, Z, isMinus_in_gga(A, pred(X), Z))
isMinus_in_gga(X, zero, X) → isMinus_out_gga(X, zero, X)
isMinus_in_gga(zero, succ(Y), pred(Z)) → U31_gga(Y, Z, isMinus_in_gga(zero, Y, Z))
isMinus_in_gga(zero, pred(Y), succ(Z)) → U32_gga(Y, Z, isMinus_in_gga(zero, Y, Z))
isMinus_in_gga(succ(X), succ(Y), Z) → U33_gga(X, Y, Z, isMinus_in_gga(X, Y, Z))
isMinus_in_gga(succ(X), pred(Y), succ(succ(Z))) → U34_gga(X, Y, Z, isMinus_in_gga(X, Y, Z))
isMinus_in_gga(pred(X), succ(Y), pred(pred(Z))) → U35_gga(X, Y, Z, isMinus_in_gga(X, Y, Z))
isMinus_in_gga(pred(X), pred(Y), Z) → U36_gga(X, Y, Z, isMinus_in_gga(X, Y, Z))
U36_gga(X, Y, Z, isMinus_out_gga(X, Y, Z)) → isMinus_out_gga(pred(X), pred(Y), Z)
U35_gga(X, Y, Z, isMinus_out_gga(X, Y, Z)) → isMinus_out_gga(pred(X), succ(Y), pred(pred(Z)))
U34_gga(X, Y, Z, isMinus_out_gga(X, Y, Z)) → isMinus_out_gga(succ(X), pred(Y), succ(succ(Z)))
U33_gga(X, Y, Z, isMinus_out_gga(X, Y, Z)) → isMinus_out_gga(succ(X), succ(Y), Z)
U32_gga(Y, Z, isMinus_out_gga(zero, Y, Z)) → isMinus_out_gga(zero, pred(Y), succ(Z))
U31_gga(Y, Z, isMinus_out_gga(zero, Y, Z)) → isMinus_out_gga(zero, succ(Y), pred(Z))
U44_gga(X, Y, Z, isMinus_out_gga(A, pred(X), Z)) → isTimes_out_gga(pred(X), pred(Y), Z)
U41_gga(X, Y, Z, isTimes_out_gga(pred(X), Y, A)) → U42_gga(X, Y, Z, isPlus_in_gga(A, pred(X), Z))
isPlus_in_gga(zero, X, X) → isPlus_out_gga(zero, X, X)
isPlus_in_gga(succ(X), zero, succ(X)) → isPlus_out_gga(succ(X), zero, succ(X))
isPlus_in_gga(succ(X), succ(Y), succ(succ(Z))) → U27_gga(X, Y, Z, isPlus_in_gga(X, Y, Z))
isPlus_in_gga(succ(X), pred(Y), Z) → U28_gga(X, Y, Z, isPlus_in_gga(X, Y, Z))
isPlus_in_gga(pred(X), zero, pred(X)) → isPlus_out_gga(pred(X), zero, pred(X))
isPlus_in_gga(pred(X), succ(Y), Z) → U29_gga(X, Y, Z, isPlus_in_gga(X, Y, Z))
isPlus_in_gga(pred(X), pred(Y), pred(pred(Z))) → U30_gga(X, Y, Z, isPlus_in_gga(X, Y, Z))
U30_gga(X, Y, Z, isPlus_out_gga(X, Y, Z)) → isPlus_out_gga(pred(X), pred(Y), pred(pred(Z)))
U29_gga(X, Y, Z, isPlus_out_gga(X, Y, Z)) → isPlus_out_gga(pred(X), succ(Y), Z)
U28_gga(X, Y, Z, isPlus_out_gga(X, Y, Z)) → isPlus_out_gga(succ(X), pred(Y), Z)
U27_gga(X, Y, Z, isPlus_out_gga(X, Y, Z)) → isPlus_out_gga(succ(X), succ(Y), succ(succ(Z)))
U42_gga(X, Y, Z, isPlus_out_gga(A, pred(X), Z)) → isTimes_out_gga(pred(X), succ(Y), Z)
U39_gga(X, Y, Z, isTimes_out_gga(succ(X), Y, A)) → U40_gga(X, Y, Z, isMinus_in_gga(A, succ(X), Z))
U40_gga(X, Y, Z, isMinus_out_gga(A, succ(X), Z)) → isTimes_out_gga(succ(X), pred(Y), Z)
U37_gga(X, Y, Z, isTimes_out_gga(succ(X), Y, A)) → U38_gga(X, Y, Z, isPlus_in_gga(A, succ(X), Z))
U38_gga(X, Y, Z, isPlus_out_gga(A, succ(X), Z)) → isTimes_out_gga(succ(X), succ(Y), Z)
U6_gga(H1, T1, H2, T2, Result, Newresult, isTimes_out_gga(H1, H2, U)) → U7_gga(H1, T1, H2, T2, Result, Newresult, U, =_in_ag(Product, U))
=_in_ag(X, X) → =_out_ag(X, X)
U7_gga(H1, T1, H2, T2, Result, Newresult, U, =_out_ag(Product, U)) → U8_gga(H1, T1, H2, T2, Result, U, isPlus_in_ggg(Product, Newresult, U))
isPlus_in_ggg(zero, X, X) → isPlus_out_ggg(zero, X, X)
isPlus_in_ggg(succ(X), zero, succ(X)) → isPlus_out_ggg(succ(X), zero, succ(X))
isPlus_in_ggg(succ(X), succ(Y), succ(succ(Z))) → U27_ggg(X, Y, Z, isPlus_in_ggg(X, Y, Z))
isPlus_in_ggg(succ(X), pred(Y), Z) → U28_ggg(X, Y, Z, isPlus_in_ggg(X, Y, Z))
isPlus_in_ggg(pred(X), zero, pred(X)) → isPlus_out_ggg(pred(X), zero, pred(X))
isPlus_in_ggg(pred(X), succ(Y), Z) → U29_ggg(X, Y, Z, isPlus_in_ggg(X, Y, Z))
isPlus_in_ggg(pred(X), pred(Y), pred(pred(Z))) → U30_ggg(X, Y, Z, isPlus_in_ggg(X, Y, Z))
U30_ggg(X, Y, Z, isPlus_out_ggg(X, Y, Z)) → isPlus_out_ggg(pred(X), pred(Y), pred(pred(Z)))
U29_ggg(X, Y, Z, isPlus_out_ggg(X, Y, Z)) → isPlus_out_ggg(pred(X), succ(Y), Z)
U28_ggg(X, Y, Z, isPlus_out_ggg(X, Y, Z)) → isPlus_out_ggg(succ(X), pred(Y), Z)
U27_ggg(X, Y, Z, isPlus_out_ggg(X, Y, Z)) → isPlus_out_ggg(succ(X), succ(Y), succ(succ(Z)))
U8_gga(H1, T1, H2, T2, Result, U, isPlus_out_ggg(Product, Newresult, U)) → U9_gga(H1, T1, H2, T2, Result, =_in_ag(Result, U))
U9_gga(H1, T1, H2, T2, Result, =_out_ag(Result, U)) → vmul_out_gga(.(H1, T1), .(H2, T2), Result)
U4_gga(V0, Rest, V1, Result, Others, vmul_out_gga(V0, V1, Result)) → multiply_out_gga(.(V0, Rest), V1, .(Result, Others))
U2_gga(V0, Rest, V1, Result, Others, multiply_out_gga(V1, V0, Result)) → mmultiply_out_gga(.(V0, Rest), V1, .(Result, Others))

The argument filtering Pi contains the following mapping:
mmultiply_in_gga(x1, x2, x3) = mmultiply_in_gga(x1, x2)
[] = []
mmultiply_out_gga(x1, x2, x3) = mmultiply_out_gga(x3)
.(x1, x2) = .(x1, x2)
U1_gga(x1, x2, x3, x4, x5, x6) = U1_gga(x1, x3, x6)
U2_gga(x1, x2, x3, x4, x5, x6) = U2_gga(x5, x6)
multiply_in_gga(x1, x2, x3) = multiply_in_gga(x1, x2)
multiply_out_gga(x1, x2, x3) = multiply_out_gga(x3)
U3_gga(x1, x2, x3, x4, x5, x6) = U3_gga(x1, x3, x6)
U4_gga(x1, x2, x3, x4, x5, x6) = U4_gga(x5, x6)
vmul_in_gga(x1, x2, x3) = vmul_in_gga(x1, x2)
vmul_out_gga(x1, x2, x3) = vmul_out_gga(x3)
U5_gga(x1, x2, x3, x4, x5, x6) = U5_gga(x1, x3, x6)
U6_gga(x1, x2, x3, x4, x5, x6, x7) = U6_gga(x6, x7)
isTimes_in_gga(x1, x2, x3) = isTimes_in_gga(x1, x2)
zero = zero
isTimes_out_gga(x1, x2, x3) = isTimes_out_gga(x3)
succ(x1) = succ(x1)
pred(x1) = pred(x1)
U37_gga(x1, x2, x3, x4) = U37_gga(x1, x4)
U39_gga(x1, x2, x3, x4) = U39_gga(x1, x4)
U41_gga(x1, x2, x3, x4) = U41_gga(x1, x4)
U43_gga(x1, x2, x3, x4) = U43_gga(x1, x4)
U44_gga(x1, x2, x3, x4) = U44_gga(x4)
isMinus_in_gga(x1, x2, x3) = isMinus_in_gga(x1, x2)
isMinus_out_gga(x1, x2, x3) = isMinus_out_gga(x3)
U31_gga(x1, x2, x3) = U31_gga(x3)
U32_gga(x1, x2, x3) = U32_gga(x3)
U33_gga(x1, x2, x3, x4) = U33_gga(x4)
U34_gga(x1, x2, x3, x4) = U34_gga(x4)
U35_gga(x1, x2, x3, x4) = U35_gga(x4)
U36_gga(x1, x2, x3, x4) = U36_gga(x4)
U42_gga(x1, x2, x3, x4) = U42_gga(x4)
isPlus_in_gga(x1, x2, x3) = isPlus_in_gga(x1, x2)
isPlus_out_gga(x1, x2, x3) = isPlus_out_gga(x3)
U27_gga(x1, x2, x3, x4) = U27_gga(x4)
U28_gga(x1, x2, x3, x4) = U28_gga(x4)
U29_gga(x1, x2, x3, x4) = U29_gga(x4)
U30_gga(x1, x2, x3, x4) = U30_gga(x4)
U40_gga(x1, x2, x3, x4) = U40_gga(x4)
U38_gga(x1, x2, x3, x4) = U38_gga(x4)
U7_gga(x1, x2, x3, x4, x5, x6, x7, x8) = U7_gga(x6, x7, x8)
=_in_ag(x1, x2) = =_in_ag(x2)
=_out_ag(x1, x2) = =_out_ag(x1)
U8_gga(x1, x2, x3, x4, x5, x6, x7) = U8_gga(x6, x7)
isPlus_in_ggg(x1, x2, x3) = isPlus_in_ggg(x1, x2, x3)
isPlus_out_ggg(x1, x2, x3) = isPlus_out_ggg
U27_ggg(x1, x2, x3, x4) = U27_ggg(x4)
U28_ggg(x1, x2, x3, x4) = U28_ggg(x4)
U29_ggg(x1, x2, x3, x4) = U29_ggg(x4)
U30_ggg(x1, x2, x3, x4) = U30_ggg(x4)
U9_gga(x1, x2, x3, x4, x5, x6) = U9_gga(x6)
U8_GGA(x1, x2, x3, x4, x5, x6, x7) = U8_GGA(x6, x7)
U33_GGA(x1, x2, x3, x4) = U33_GGA(x4)
U27_GGG(x1, x2, x3, x4) = U27_GGG(x4)
U35_GGA(x1, x2, x3, x4) = U35_GGA(x4)
U44_GGA(x1, x2, x3, x4) = U44_GGA(x4)
U42_GGA(x1, x2, x3, x4) = U42_GGA(x4)
U32_GGA(x1, x2, x3) = U32_GGA(x3)
U2_GGA(x1, x2, x3, x4, x5, x6) = U2_GGA(x5, x6)
U9_GGA(x1, x2, x3, x4, x5, x6) = U9_GGA(x6)
U4_GGA(x1, x2, x3, x4, x5, x6) = U4_GGA(x5, x6)
ISMINUS_IN_GGA(x1, x2, x3) = ISMINUS_IN_GGA(x1, x2)
U38_GGA(x1, x2, x3, x4) = U38_GGA(x4)
U3_GGA(x1, x2, x3, x4, x5, x6) = U3_GGA(x1, x3, x6)
=_IN_AG(x1, x2) = =_IN_AG(x2)
U41_GGA(x1, x2, x3, x4) = U41_GGA(x1, x4)
U5_GGA(x1, x2, x3, x4, x5, x6) = U5_GGA(x1, x3, x6)
U30_GGG(x1, x2, x3, x4) = U30_GGG(x4)
MULTIPLY_IN_GGA(x1, x2, x3) = MULTIPLY_IN_GGA(x1, x2)
U29_GGA(x1, x2, x3, x4) = U29_GGA(x4)
U34_GGA(x1, x2, x3, x4) = U34_GGA(x4)
U36_GGA(x1, x2, x3, x4) = U36_GGA(x4)
ISPLUS_IN_GGG(x1, x2, x3) = ISPLUS_IN_GGG(x1, x2, x3)
U7_GGA(x1, x2, x3, x4, x5, x6, x7, x8) = U7_GGA(x6, x7, x8)
U40_GGA(x1, x2, x3, x4) = U40_GGA(x4)
VMUL_IN_GGA(x1, x2, x3) = VMUL_IN_GGA(x1, x2)
ISTIMES_IN_GGA(x1, x2, x3) = ISTIMES_IN_GGA(x1, x2)
U29_GGG(x1, x2, x3, x4) = U29_GGG(x4)
MMULTIPLY_IN_GGA(x1, x2, x3) = MMULTIPLY_IN_GGA(x1, x2)
ISPLUS_IN_GGA(x1, x2, x3) = ISPLUS_IN_GGA(x1, x2)
U28_GGA(x1, x2, x3, x4) = U28_GGA(x4)
U1_GGA(x1, x2, x3, x4, x5, x6) = U1_GGA(x1, x3, x6)
U43_GGA(x1, x2, x3, x4) = U43_GGA(x1, x4)
U27_GGA(x1, x2, x3, x4) = U27_GGA(x4)
U28_GGG(x1, x2, x3, x4) = U28_GGG(x4)
U37_GGA(x1, x2, x3, x4) = U37_GGA(x1, x4)
U6_GGA(x1, x2, x3, x4, x5, x6, x7) = U6_GGA(x6, x7)
U31_GGA(x1, x2, x3) = U31_GGA(x3)
U30_GGA(x1, x2, x3, x4) = U30_GGA(x4)
U39_GGA(x1, x2, x3, x4) = U39_GGA(x1, x4)

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

↳ Prolog

  ↳ PredefinedPredicateTransformerProof

    ↳ Prolog

      ↳ PrologToPiTRSProof

        ↳ PiTRS

          ↳ DependencyPairsProof

            ↳ PiDP

              ↳ DependencyGraphProof

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

MMULTIPLY_IN_GGA(.(V0, Rest), V1, .(Result, Others)) → U1_GGA(V0, Rest, V1, Result, Others, mmultiply_in_gga(Rest, V1, Others))
MMULTIPLY_IN_GGA(.(V0, Rest), V1, .(Result, Others)) → MMULTIPLY_IN_GGA(Rest, V1, Others)
U1_GGA(V0, Rest, V1, Result, Others, mmultiply_out_gga(Rest, V1, Others)) → U2_GGA(V0, Rest, V1, Result, Others, multiply_in_gga(V1, V0, Result))
U1_GGA(V0, Rest, V1, Result, Others, mmultiply_out_gga(Rest, V1, Others)) → MULTIPLY_IN_GGA(V1, V0, Result)
MULTIPLY_IN_GGA(.(V0, Rest), V1, .(Result, Others)) → U3_GGA(V0, Rest, V1, Result, Others, multiply_in_gga(Rest, V1, Others))
MULTIPLY_IN_GGA(.(V0, Rest), V1, .(Result, Others)) → MULTIPLY_IN_GGA(Rest, V1, Others)
U3_GGA(V0, Rest, V1, Result, Others, multiply_out_gga(Rest, V1, Others)) → U4_GGA(V0, Rest, V1, Result, Others, vmul_in_gga(V0, V1, Result))
U3_GGA(V0, Rest, V1, Result, Others, multiply_out_gga(Rest, V1, Others)) → VMUL_IN_GGA(V0, V1, Result)
VMUL_IN_GGA(.(H1, T1), .(H2, T2), Result) → U5_GGA(H1, T1, H2, T2, Result, vmul_in_gga(T1, T2, Newresult))
VMUL_IN_GGA(.(H1, T1), .(H2, T2), Result) → VMUL_IN_GGA(T1, T2, Newresult)
U5_GGA(H1, T1, H2, T2, Result, vmul_out_gga(T1, T2, Newresult)) → U6_GGA(H1, T1, H2, T2, Result, Newresult, isTimes_in_gga(H1, H2, U))
U5_GGA(H1, T1, H2, T2, Result, vmul_out_gga(T1, T2, Newresult)) → ISTIMES_IN_GGA(H1, H2, U)
ISTIMES_IN_GGA(succ(X), succ(Y), Z) → U37_GGA(X, Y, Z, isTimes_in_gga(succ(X), Y, A))
ISTIMES_IN_GGA(succ(X), succ(Y), Z) → ISTIMES_IN_GGA(succ(X), Y, A)
ISTIMES_IN_GGA(succ(X), pred(Y), Z) → U39_GGA(X, Y, Z, isTimes_in_gga(succ(X), Y, A))
ISTIMES_IN_GGA(succ(X), pred(Y), Z) → ISTIMES_IN_GGA(succ(X), Y, A)
ISTIMES_IN_GGA(pred(X), succ(Y), Z) → U41_GGA(X, Y, Z, isTimes_in_gga(pred(X), Y, A))
ISTIMES_IN_GGA(pred(X), succ(Y), Z) → ISTIMES_IN_GGA(pred(X), Y, A)
ISTIMES_IN_GGA(pred(X), pred(Y), Z) → U43_GGA(X, Y, Z, isTimes_in_gga(pred(X), Y, A))
ISTIMES_IN_GGA(pred(X), pred(Y), Z) → ISTIMES_IN_GGA(pred(X), Y, A)
U43_GGA(X, Y, Z, isTimes_out_gga(pred(X), Y, A)) → U44_GGA(X, Y, Z, isMinus_in_gga(A, pred(X), Z))
U43_GGA(X, Y, Z, isTimes_out_gga(pred(X), Y, A)) → ISMINUS_IN_GGA(A, pred(X), Z)
ISMINUS_IN_GGA(zero, succ(Y), pred(Z)) → U31_GGA(Y, Z, isMinus_in_gga(zero, Y, Z))
ISMINUS_IN_GGA(zero, succ(Y), pred(Z)) → ISMINUS_IN_GGA(zero, Y, Z)
ISMINUS_IN_GGA(zero, pred(Y), succ(Z)) → U32_GGA(Y, Z, isMinus_in_gga(zero, Y, Z))
ISMINUS_IN_GGA(zero, pred(Y), succ(Z)) → ISMINUS_IN_GGA(zero, Y, Z)
ISMINUS_IN_GGA(succ(X), succ(Y), Z) → U33_GGA(X, Y, Z, isMinus_in_gga(X, Y, Z))
ISMINUS_IN_GGA(succ(X), succ(Y), Z) → ISMINUS_IN_GGA(X, Y, Z)
ISMINUS_IN_GGA(succ(X), pred(Y), succ(succ(Z))) → U34_GGA(X, Y, Z, isMinus_in_gga(X, Y, Z))
ISMINUS_IN_GGA(succ(X), pred(Y), succ(succ(Z))) → ISMINUS_IN_GGA(X, Y, Z)
ISMINUS_IN_GGA(pred(X), succ(Y), pred(pred(Z))) → U35_GGA(X, Y, Z, isMinus_in_gga(X, Y, Z))
ISMINUS_IN_GGA(pred(X), succ(Y), pred(pred(Z))) → ISMINUS_IN_GGA(X, Y, Z)
ISMINUS_IN_GGA(pred(X), pred(Y), Z) → U36_GGA(X, Y, Z, isMinus_in_gga(X, Y, Z))
ISMINUS_IN_GGA(pred(X), pred(Y), Z) → ISMINUS_IN_GGA(X, Y, Z)
U41_GGA(X, Y, Z, isTimes_out_gga(pred(X), Y, A)) → U42_GGA(X, Y, Z, isPlus_in_gga(A, pred(X), Z))
U41_GGA(X, Y, Z, isTimes_out_gga(pred(X), Y, A)) → ISPLUS_IN_GGA(A, pred(X), Z)
ISPLUS_IN_GGA(succ(X), succ(Y), succ(succ(Z))) → U27_GGA(X, Y, Z, isPlus_in_gga(X, Y, Z))
ISPLUS_IN_GGA(succ(X), succ(Y), succ(succ(Z))) → ISPLUS_IN_GGA(X, Y, Z)
ISPLUS_IN_GGA(succ(X), pred(Y), Z) → U28_GGA(X, Y, Z, isPlus_in_gga(X, Y, Z))
ISPLUS_IN_GGA(succ(X), pred(Y), Z) → ISPLUS_IN_GGA(X, Y, Z)
ISPLUS_IN_GGA(pred(X), succ(Y), Z) → U29_GGA(X, Y, Z, isPlus_in_gga(X, Y, Z))
ISPLUS_IN_GGA(pred(X), succ(Y), Z) → ISPLUS_IN_GGA(X, Y, Z)
ISPLUS_IN_GGA(pred(X), pred(Y), pred(pred(Z))) → U30_GGA(X, Y, Z, isPlus_in_gga(X, Y, Z))
ISPLUS_IN_GGA(pred(X), pred(Y), pred(pred(Z))) → ISPLUS_IN_GGA(X, Y, Z)
U39_GGA(X, Y, Z, isTimes_out_gga(succ(X), Y, A)) → U40_GGA(X, Y, Z, isMinus_in_gga(A, succ(X), Z))
U39_GGA(X, Y, Z, isTimes_out_gga(succ(X), Y, A)) → ISMINUS_IN_GGA(A, succ(X), Z)
U37_GGA(X, Y, Z, isTimes_out_gga(succ(X), Y, A)) → U38_GGA(X, Y, Z, isPlus_in_gga(A, succ(X), Z))
U37_GGA(X, Y, Z, isTimes_out_gga(succ(X), Y, A)) → ISPLUS_IN_GGA(A, succ(X), Z)
U6_GGA(H1, T1, H2, T2, Result, Newresult, isTimes_out_gga(H1, H2, U)) → U7_GGA(H1, T1, H2, T2, Result, Newresult, U, =_in_ag(Product, U))
U6_GGA(H1, T1, H2, T2, Result, Newresult, isTimes_out_gga(H1, H2, U)) → =_IN_AG(Product, U)
U7_GGA(H1, T1, H2, T2, Result, Newresult, U, =_out_ag(Product, U)) → U8_GGA(H1, T1, H2, T2, Result, U, isPlus_in_ggg(Product, Newresult, U))
U7_GGA(H1, T1, H2, T2, Result, Newresult, U, =_out_ag(Product, U)) → ISPLUS_IN_GGG(Product, Newresult, U)
ISPLUS_IN_GGG(succ(X), succ(Y), succ(succ(Z))) → U27_GGG(X, Y, Z, isPlus_in_ggg(X, Y, Z))
ISPLUS_IN_GGG(succ(X), succ(Y), succ(succ(Z))) → ISPLUS_IN_GGG(X, Y, Z)
ISPLUS_IN_GGG(succ(X), pred(Y), Z) → U28_GGG(X, Y, Z, isPlus_in_ggg(X, Y, Z))
ISPLUS_IN_GGG(succ(X), pred(Y), Z) → ISPLUS_IN_GGG(X, Y, Z)
ISPLUS_IN_GGG(pred(X), succ(Y), Z) → U29_GGG(X, Y, Z, isPlus_in_ggg(X, Y, Z))
ISPLUS_IN_GGG(pred(X), succ(Y), Z) → ISPLUS_IN_GGG(X, Y, Z)
ISPLUS_IN_GGG(pred(X), pred(Y), pred(pred(Z))) → U30_GGG(X, Y, Z, isPlus_in_ggg(X, Y, Z))
ISPLUS_IN_GGG(pred(X), pred(Y), pred(pred(Z))) → ISPLUS_IN_GGG(X, Y, Z)
U8_GGA(H1, T1, H2, T2, Result, U, isPlus_out_ggg(Product, Newresult, U)) → U9_GGA(H1, T1, H2, T2, Result, =_in_ag(Result, U))
U8_GGA(H1, T1, H2, T2, Result, U, isPlus_out_ggg(Product, Newresult, U)) → =_IN_AG(Result, U)

The TRS R consists of the following rules:

mmultiply_in_gga([], X, []) → mmultiply_out_gga([], X, [])
mmultiply_in_gga(.(V0, Rest), V1, .(Result, Others)) → U1_gga(V0, Rest, V1, Result, Others, mmultiply_in_gga(Rest, V1, Others))
U1_gga(V0, Rest, V1, Result, Others, mmultiply_out_gga(Rest, V1, Others)) → U2_gga(V0, Rest, V1, Result, Others, multiply_in_gga(V1, V0, Result))
multiply_in_gga([], X, []) → multiply_out_gga([], X, [])
multiply_in_gga(.(V0, Rest), V1, .(Result, Others)) → U3_gga(V0, Rest, V1, Result, Others, multiply_in_gga(Rest, V1, Others))
U3_gga(V0, Rest, V1, Result, Others, multiply_out_gga(Rest, V1, Others)) → U4_gga(V0, Rest, V1, Result, Others, vmul_in_gga(V0, V1, Result))
vmul_in_gga([], [], zero) → vmul_out_gga([], [], zero)
vmul_in_gga(.(H1, T1), .(H2, T2), Result) → U5_gga(H1, T1, H2, T2, Result, vmul_in_gga(T1, T2, Newresult))
U5_gga(H1, T1, H2, T2, Result, vmul_out_gga(T1, T2, Newresult)) → U6_gga(H1, T1, H2, T2, Result, Newresult, isTimes_in_gga(H1, H2, U))
isTimes_in_gga(X, zero, zero) → isTimes_out_gga(X, zero, zero)
isTimes_in_gga(zero, succ(Y), zero) → isTimes_out_gga(zero, succ(Y), zero)
isTimes_in_gga(zero, pred(Y), zero) → isTimes_out_gga(zero, pred(Y), zero)
isTimes_in_gga(succ(X), succ(Y), Z) → U37_gga(X, Y, Z, isTimes_in_gga(succ(X), Y, A))
isTimes_in_gga(succ(X), pred(Y), Z) → U39_gga(X, Y, Z, isTimes_in_gga(succ(X), Y, A))
isTimes_in_gga(pred(X), succ(Y), Z) → U41_gga(X, Y, Z, isTimes_in_gga(pred(X), Y, A))
isTimes_in_gga(pred(X), pred(Y), Z) → U43_gga(X, Y, Z, isTimes_in_gga(pred(X), Y, A))
U43_gga(X, Y, Z, isTimes_out_gga(pred(X), Y, A)) → U44_gga(X, Y, Z, isMinus_in_gga(A, pred(X), Z))
isMinus_in_gga(X, zero, X) → isMinus_out_gga(X, zero, X)
isMinus_in_gga(zero, succ(Y), pred(Z)) → U31_gga(Y, Z, isMinus_in_gga(zero, Y, Z))
isMinus_in_gga(zero, pred(Y), succ(Z)) → U32_gga(Y, Z, isMinus_in_gga(zero, Y, Z))
isMinus_in_gga(succ(X), succ(Y), Z) → U33_gga(X, Y, Z, isMinus_in_gga(X, Y, Z))
isMinus_in_gga(succ(X), pred(Y), succ(succ(Z))) → U34_gga(X, Y, Z, isMinus_in_gga(X, Y, Z))
isMinus_in_gga(pred(X), succ(Y), pred(pred(Z))) → U35_gga(X, Y, Z, isMinus_in_gga(X, Y, Z))
isMinus_in_gga(pred(X), pred(Y), Z) → U36_gga(X, Y, Z, isMinus_in_gga(X, Y, Z))
U36_gga(X, Y, Z, isMinus_out_gga(X, Y, Z)) → isMinus_out_gga(pred(X), pred(Y), Z)
U35_gga(X, Y, Z, isMinus_out_gga(X, Y, Z)) → isMinus_out_gga(pred(X), succ(Y), pred(pred(Z)))
U34_gga(X, Y, Z, isMinus_out_gga(X, Y, Z)) → isMinus_out_gga(succ(X), pred(Y), succ(succ(Z)))
U33_gga(X, Y, Z, isMinus_out_gga(X, Y, Z)) → isMinus_out_gga(succ(X), succ(Y), Z)
U32_gga(Y, Z, isMinus_out_gga(zero, Y, Z)) → isMinus_out_gga(zero, pred(Y), succ(Z))
U31_gga(Y, Z, isMinus_out_gga(zero, Y, Z)) → isMinus_out_gga(zero, succ(Y), pred(Z))
U44_gga(X, Y, Z, isMinus_out_gga(A, pred(X), Z)) → isTimes_out_gga(pred(X), pred(Y), Z)
U41_gga(X, Y, Z, isTimes_out_gga(pred(X), Y, A)) → U42_gga(X, Y, Z, isPlus_in_gga(A, pred(X), Z))
isPlus_in_gga(zero, X, X) → isPlus_out_gga(zero, X, X)
isPlus_in_gga(succ(X), zero, succ(X)) → isPlus_out_gga(succ(X), zero, succ(X))
isPlus_in_gga(succ(X), succ(Y), succ(succ(Z))) → U27_gga(X, Y, Z, isPlus_in_gga(X, Y, Z))
isPlus_in_gga(succ(X), pred(Y), Z) → U28_gga(X, Y, Z, isPlus_in_gga(X, Y, Z))
isPlus_in_gga(pred(X), zero, pred(X)) → isPlus_out_gga(pred(X), zero, pred(X))
isPlus_in_gga(pred(X), succ(Y), Z) → U29_gga(X, Y, Z, isPlus_in_gga(X, Y, Z))
isPlus_in_gga(pred(X), pred(Y), pred(pred(Z))) → U30_gga(X, Y, Z, isPlus_in_gga(X, Y, Z))
U30_gga(X, Y, Z, isPlus_out_gga(X, Y, Z)) → isPlus_out_gga(pred(X), pred(Y), pred(pred(Z)))
U29_gga(X, Y, Z, isPlus_out_gga(X, Y, Z)) → isPlus_out_gga(pred(X), succ(Y), Z)
U28_gga(X, Y, Z, isPlus_out_gga(X, Y, Z)) → isPlus_out_gga(succ(X), pred(Y), Z)
U27_gga(X, Y, Z, isPlus_out_gga(X, Y, Z)) → isPlus_out_gga(succ(X), succ(Y), succ(succ(Z)))
U42_gga(X, Y, Z, isPlus_out_gga(A, pred(X), Z)) → isTimes_out_gga(pred(X), succ(Y), Z)
U39_gga(X, Y, Z, isTimes_out_gga(succ(X), Y, A)) → U40_gga(X, Y, Z, isMinus_in_gga(A, succ(X), Z))
U40_gga(X, Y, Z, isMinus_out_gga(A, succ(X), Z)) → isTimes_out_gga(succ(X), pred(Y), Z)
U37_gga(X, Y, Z, isTimes_out_gga(succ(X), Y, A)) → U38_gga(X, Y, Z, isPlus_in_gga(A, succ(X), Z))
U38_gga(X, Y, Z, isPlus_out_gga(A, succ(X), Z)) → isTimes_out_gga(succ(X), succ(Y), Z)
U6_gga(H1, T1, H2, T2, Result, Newresult, isTimes_out_gga(H1, H2, U)) → U7_gga(H1, T1, H2, T2, Result, Newresult, U, =_in_ag(Product, U))
=_in_ag(X, X) → =_out_ag(X, X)
U7_gga(H1, T1, H2, T2, Result, Newresult, U, =_out_ag(Product, U)) → U8_gga(H1, T1, H2, T2, Result, U, isPlus_in_ggg(Product, Newresult, U))
isPlus_in_ggg(zero, X, X) → isPlus_out_ggg(zero, X, X)
isPlus_in_ggg(succ(X), zero, succ(X)) → isPlus_out_ggg(succ(X), zero, succ(X))
isPlus_in_ggg(succ(X), succ(Y), succ(succ(Z))) → U27_ggg(X, Y, Z, isPlus_in_ggg(X, Y, Z))
isPlus_in_ggg(succ(X), pred(Y), Z) → U28_ggg(X, Y, Z, isPlus_in_ggg(X, Y, Z))
isPlus_in_ggg(pred(X), zero, pred(X)) → isPlus_out_ggg(pred(X), zero, pred(X))
isPlus_in_ggg(pred(X), succ(Y), Z) → U29_ggg(X, Y, Z, isPlus_in_ggg(X, Y, Z))
isPlus_in_ggg(pred(X), pred(Y), pred(pred(Z))) → U30_ggg(X, Y, Z, isPlus_in_ggg(X, Y, Z))
U30_ggg(X, Y, Z, isPlus_out_ggg(X, Y, Z)) → isPlus_out_ggg(pred(X), pred(Y), pred(pred(Z)))
U29_ggg(X, Y, Z, isPlus_out_ggg(X, Y, Z)) → isPlus_out_ggg(pred(X), succ(Y), Z)
U28_ggg(X, Y, Z, isPlus_out_ggg(X, Y, Z)) → isPlus_out_ggg(succ(X), pred(Y), Z)
U27_ggg(X, Y, Z, isPlus_out_ggg(X, Y, Z)) → isPlus_out_ggg(succ(X), succ(Y), succ(succ(Z)))
U8_gga(H1, T1, H2, T2, Result, U, isPlus_out_ggg(Product, Newresult, U)) → U9_gga(H1, T1, H2, T2, Result, =_in_ag(Result, U))
U9_gga(H1, T1, H2, T2, Result, =_out_ag(Result, U)) → vmul_out_gga(.(H1, T1), .(H2, T2), Result)
U4_gga(V0, Rest, V1, Result, Others, vmul_out_gga(V0, V1, Result)) → multiply_out_gga(.(V0, Rest), V1, .(Result, Others))
U2_gga(V0, Rest, V1, Result, Others, multiply_out_gga(V1, V0, Result)) → mmultiply_out_gga(.(V0, Rest), V1, .(Result, Others))

↳ Prolog

  ↳ PredefinedPredicateTransformerProof

    ↳ Prolog

      ↳ PrologToPiTRSProof

        ↳ PiTRS

          ↳ DependencyPairsProof

            ↳ PiDP

              ↳ DependencyGraphProof

                ↳ AND

                  ↳ PiDP

                    ↳ UsableRulesProof

                  ↳ PiDP

                  ↳ PiDP

                  ↳ PiDP

                  ↳ PiDP

                  ↳ PiDP

                  ↳ PiDP

                  ↳ PiDP

                  ↳ PiDP

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

ISPLUS_IN_GGG(succ(X), succ(Y), succ(succ(Z))) → ISPLUS_IN_GGG(X, Y, Z)
ISPLUS_IN_GGG(pred(X), succ(Y), Z) → ISPLUS_IN_GGG(X, Y, Z)
ISPLUS_IN_GGG(succ(X), pred(Y), Z) → ISPLUS_IN_GGG(X, Y, Z)
ISPLUS_IN_GGG(pred(X), pred(Y), pred(pred(Z))) → ISPLUS_IN_GGG(X, Y, Z)

The TRS R consists of the following rules:

mmultiply_in_gga([], X, []) → mmultiply_out_gga([], X, [])
mmultiply_in_gga(.(V0, Rest), V1, .(Result, Others)) → U1_gga(V0, Rest, V1, Result, Others, mmultiply_in_gga(Rest, V1, Others))
U1_gga(V0, Rest, V1, Result, Others, mmultiply_out_gga(Rest, V1, Others)) → U2_gga(V0, Rest, V1, Result, Others, multiply_in_gga(V1, V0, Result))
multiply_in_gga([], X, []) → multiply_out_gga([], X, [])
multiply_in_gga(.(V0, Rest), V1, .(Result, Others)) → U3_gga(V0, Rest, V1, Result, Others, multiply_in_gga(Rest, V1, Others))
U3_gga(V0, Rest, V1, Result, Others, multiply_out_gga(Rest, V1, Others)) → U4_gga(V0, Rest, V1, Result, Others, vmul_in_gga(V0, V1, Result))
vmul_in_gga([], [], zero) → vmul_out_gga([], [], zero)
vmul_in_gga(.(H1, T1), .(H2, T2), Result) → U5_gga(H1, T1, H2, T2, Result, vmul_in_gga(T1, T2, Newresult))
U5_gga(H1, T1, H2, T2, Result, vmul_out_gga(T1, T2, Newresult)) → U6_gga(H1, T1, H2, T2, Result, Newresult, isTimes_in_gga(H1, H2, U))
isTimes_in_gga(X, zero, zero) → isTimes_out_gga(X, zero, zero)
isTimes_in_gga(zero, succ(Y), zero) → isTimes_out_gga(zero, succ(Y), zero)
isTimes_in_gga(zero, pred(Y), zero) → isTimes_out_gga(zero, pred(Y), zero)
isTimes_in_gga(succ(X), succ(Y), Z) → U37_gga(X, Y, Z, isTimes_in_gga(succ(X), Y, A))
isTimes_in_gga(succ(X), pred(Y), Z) → U39_gga(X, Y, Z, isTimes_in_gga(succ(X), Y, A))
isTimes_in_gga(pred(X), succ(Y), Z) → U41_gga(X, Y, Z, isTimes_in_gga(pred(X), Y, A))
isTimes_in_gga(pred(X), pred(Y), Z) → U43_gga(X, Y, Z, isTimes_in_gga(pred(X), Y, A))
U43_gga(X, Y, Z, isTimes_out_gga(pred(X), Y, A)) → U44_gga(X, Y, Z, isMinus_in_gga(A, pred(X), Z))
isMinus_in_gga(X, zero, X) → isMinus_out_gga(X, zero, X)
isMinus_in_gga(zero, succ(Y), pred(Z)) → U31_gga(Y, Z, isMinus_in_gga(zero, Y, Z))
isMinus_in_gga(zero, pred(Y), succ(Z)) → U32_gga(Y, Z, isMinus_in_gga(zero, Y, Z))
isMinus_in_gga(succ(X), succ(Y), Z) → U33_gga(X, Y, Z, isMinus_in_gga(X, Y, Z))
isMinus_in_gga(succ(X), pred(Y), succ(succ(Z))) → U34_gga(X, Y, Z, isMinus_in_gga(X, Y, Z))
isMinus_in_gga(pred(X), succ(Y), pred(pred(Z))) → U35_gga(X, Y, Z, isMinus_in_gga(X, Y, Z))
isMinus_in_gga(pred(X), pred(Y), Z) → U36_gga(X, Y, Z, isMinus_in_gga(X, Y, Z))
U36_gga(X, Y, Z, isMinus_out_gga(X, Y, Z)) → isMinus_out_gga(pred(X), pred(Y), Z)
U35_gga(X, Y, Z, isMinus_out_gga(X, Y, Z)) → isMinus_out_gga(pred(X), succ(Y), pred(pred(Z)))
U34_gga(X, Y, Z, isMinus_out_gga(X, Y, Z)) → isMinus_out_gga(succ(X), pred(Y), succ(succ(Z)))
U33_gga(X, Y, Z, isMinus_out_gga(X, Y, Z)) → isMinus_out_gga(succ(X), succ(Y), Z)
U32_gga(Y, Z, isMinus_out_gga(zero, Y, Z)) → isMinus_out_gga(zero, pred(Y), succ(Z))
U31_gga(Y, Z, isMinus_out_gga(zero, Y, Z)) → isMinus_out_gga(zero, succ(Y), pred(Z))
U44_gga(X, Y, Z, isMinus_out_gga(A, pred(X), Z)) → isTimes_out_gga(pred(X), pred(Y), Z)
U41_gga(X, Y, Z, isTimes_out_gga(pred(X), Y, A)) → U42_gga(X, Y, Z, isPlus_in_gga(A, pred(X), Z))
isPlus_in_gga(zero, X, X) → isPlus_out_gga(zero, X, X)
isPlus_in_gga(succ(X), zero, succ(X)) → isPlus_out_gga(succ(X), zero, succ(X))
isPlus_in_gga(succ(X), succ(Y), succ(succ(Z))) → U27_gga(X, Y, Z, isPlus_in_gga(X, Y, Z))
isPlus_in_gga(succ(X), pred(Y), Z) → U28_gga(X, Y, Z, isPlus_in_gga(X, Y, Z))
isPlus_in_gga(pred(X), zero, pred(X)) → isPlus_out_gga(pred(X), zero, pred(X))
isPlus_in_gga(pred(X), succ(Y), Z) → U29_gga(X, Y, Z, isPlus_in_gga(X, Y, Z))
isPlus_in_gga(pred(X), pred(Y), pred(pred(Z))) → U30_gga(X, Y, Z, isPlus_in_gga(X, Y, Z))
U30_gga(X, Y, Z, isPlus_out_gga(X, Y, Z)) → isPlus_out_gga(pred(X), pred(Y), pred(pred(Z)))
U29_gga(X, Y, Z, isPlus_out_gga(X, Y, Z)) → isPlus_out_gga(pred(X), succ(Y), Z)
U28_gga(X, Y, Z, isPlus_out_gga(X, Y, Z)) → isPlus_out_gga(succ(X), pred(Y), Z)
U27_gga(X, Y, Z, isPlus_out_gga(X, Y, Z)) → isPlus_out_gga(succ(X), succ(Y), succ(succ(Z)))
U42_gga(X, Y, Z, isPlus_out_gga(A, pred(X), Z)) → isTimes_out_gga(pred(X), succ(Y), Z)
U39_gga(X, Y, Z, isTimes_out_gga(succ(X), Y, A)) → U40_gga(X, Y, Z, isMinus_in_gga(A, succ(X), Z))
U40_gga(X, Y, Z, isMinus_out_gga(A, succ(X), Z)) → isTimes_out_gga(succ(X), pred(Y), Z)
U37_gga(X, Y, Z, isTimes_out_gga(succ(X), Y, A)) → U38_gga(X, Y, Z, isPlus_in_gga(A, succ(X), Z))
U38_gga(X, Y, Z, isPlus_out_gga(A, succ(X), Z)) → isTimes_out_gga(succ(X), succ(Y), Z)
U6_gga(H1, T1, H2, T2, Result, Newresult, isTimes_out_gga(H1, H2, U)) → U7_gga(H1, T1, H2, T2, Result, Newresult, U, =_in_ag(Product, U))
=_in_ag(X, X) → =_out_ag(X, X)
U7_gga(H1, T1, H2, T2, Result, Newresult, U, =_out_ag(Product, U)) → U8_gga(H1, T1, H2, T2, Result, U, isPlus_in_ggg(Product, Newresult, U))
isPlus_in_ggg(zero, X, X) → isPlus_out_ggg(zero, X, X)
isPlus_in_ggg(succ(X), zero, succ(X)) → isPlus_out_ggg(succ(X), zero, succ(X))
isPlus_in_ggg(succ(X), succ(Y), succ(succ(Z))) → U27_ggg(X, Y, Z, isPlus_in_ggg(X, Y, Z))
isPlus_in_ggg(succ(X), pred(Y), Z) → U28_ggg(X, Y, Z, isPlus_in_ggg(X, Y, Z))
isPlus_in_ggg(pred(X), zero, pred(X)) → isPlus_out_ggg(pred(X), zero, pred(X))
isPlus_in_ggg(pred(X), succ(Y), Z) → U29_ggg(X, Y, Z, isPlus_in_ggg(X, Y, Z))
isPlus_in_ggg(pred(X), pred(Y), pred(pred(Z))) → U30_ggg(X, Y, Z, isPlus_in_ggg(X, Y, Z))
U30_ggg(X, Y, Z, isPlus_out_ggg(X, Y, Z)) → isPlus_out_ggg(pred(X), pred(Y), pred(pred(Z)))
U29_ggg(X, Y, Z, isPlus_out_ggg(X, Y, Z)) → isPlus_out_ggg(pred(X), succ(Y), Z)
U28_ggg(X, Y, Z, isPlus_out_ggg(X, Y, Z)) → isPlus_out_ggg(succ(X), pred(Y), Z)
U27_ggg(X, Y, Z, isPlus_out_ggg(X, Y, Z)) → isPlus_out_ggg(succ(X), succ(Y), succ(succ(Z)))
U8_gga(H1, T1, H2, T2, Result, U, isPlus_out_ggg(Product, Newresult, U)) → U9_gga(H1, T1, H2, T2, Result, =_in_ag(Result, U))
U9_gga(H1, T1, H2, T2, Result, =_out_ag(Result, U)) → vmul_out_gga(.(H1, T1), .(H2, T2), Result)
U4_gga(V0, Rest, V1, Result, Others, vmul_out_gga(V0, V1, Result)) → multiply_out_gga(.(V0, Rest), V1, .(Result, Others))
U2_gga(V0, Rest, V1, Result, Others, multiply_out_gga(V1, V0, Result)) → mmultiply_out_gga(.(V0, Rest), V1, .(Result, Others))

↳ Prolog

  ↳ PredefinedPredicateTransformerProof

    ↳ Prolog

      ↳ PrologToPiTRSProof

        ↳ PiTRS

          ↳ DependencyPairsProof

            ↳ PiDP

              ↳ DependencyGraphProof

                ↳ AND

                  ↳ PiDP

                    ↳ UsableRulesProof

                      ↳ PiDP

                        ↳ PiDPToQDPProof

                  ↳ PiDP

                  ↳ PiDP

                  ↳ PiDP

                  ↳ PiDP

                  ↳ PiDP

                  ↳ PiDP

                  ↳ PiDP

                  ↳ PiDP

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

ISPLUS_IN_GGG(succ(X), succ(Y), succ(succ(Z))) → ISPLUS_IN_GGG(X, Y, Z)
ISPLUS_IN_GGG(pred(X), succ(Y), Z) → ISPLUS_IN_GGG(X, Y, Z)
ISPLUS_IN_GGG(succ(X), pred(Y), Z) → ISPLUS_IN_GGG(X, Y, Z)
ISPLUS_IN_GGG(pred(X), pred(Y), pred(pred(Z))) → ISPLUS_IN_GGG(X, Y, Z)

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

↳ Prolog

  ↳ PredefinedPredicateTransformerProof

    ↳ Prolog

      ↳ PrologToPiTRSProof

        ↳ PiTRS

          ↳ DependencyPairsProof

            ↳ PiDP

              ↳ DependencyGraphProof

                ↳ AND

                  ↳ PiDP

                    ↳ UsableRulesProof

                      ↳ PiDP

                        ↳ PiDPToQDPProof

                          ↳ QDP

                            ↳ QDPSizeChangeProof

                  ↳ PiDP

                  ↳ PiDP

                  ↳ PiDP

                  ↳ PiDP

                  ↳ PiDP

                  ↳ PiDP

                  ↳ PiDP

                  ↳ PiDP

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

ISPLUS_IN_GGG(succ(X), succ(Y), succ(succ(Z))) → ISPLUS_IN_GGG(X, Y, Z)
ISPLUS_IN_GGG(succ(X), pred(Y), Z) → ISPLUS_IN_GGG(X, Y, Z)
ISPLUS_IN_GGG(pred(X), succ(Y), Z) → ISPLUS_IN_GGG(X, Y, Z)
ISPLUS_IN_GGG(pred(X), pred(Y), pred(pred(Z))) → ISPLUS_IN_GGG(X, Y, Z)

R is empty.
Q is empty.
We have to consider all (P,Q,R)-chains.
By using the subterm criterion [20] together with the size-change analysis [32] we have proven that there are no infinite chains for this DP problem.

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

ISPLUS_IN_GGG(succ(X), succ(Y), succ(succ(Z))) → ISPLUS_IN_GGG(X, Y, Z)
The graph contains the following edges 1 > 1, 2 > 2, 3 > 3
ISPLUS_IN_GGG(pred(X), succ(Y), Z) → ISPLUS_IN_GGG(X, Y, Z)
The graph contains the following edges 1 > 1, 2 > 2, 3 >= 3
ISPLUS_IN_GGG(succ(X), pred(Y), Z) → ISPLUS_IN_GGG(X, Y, Z)
The graph contains the following edges 1 > 1, 2 > 2, 3 >= 3
ISPLUS_IN_GGG(pred(X), pred(Y), pred(pred(Z))) → ISPLUS_IN_GGG(X, Y, Z)
The graph contains the following edges 1 > 1, 2 > 2, 3 > 3

↳ Prolog

  ↳ PredefinedPredicateTransformerProof

    ↳ Prolog

      ↳ PrologToPiTRSProof

        ↳ PiTRS

          ↳ DependencyPairsProof

            ↳ PiDP

              ↳ DependencyGraphProof

                ↳ AND

                  ↳ PiDP

                  ↳ PiDP

                    ↳ UsableRulesProof

                  ↳ PiDP

                  ↳ PiDP

                  ↳ PiDP

                  ↳ PiDP

                  ↳ PiDP

                  ↳ PiDP

                  ↳ PiDP

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

ISPLUS_IN_GGA(succ(X), succ(Y), succ(succ(Z))) → ISPLUS_IN_GGA(X, Y, Z)
ISPLUS_IN_GGA(pred(X), succ(Y), Z) → ISPLUS_IN_GGA(X, Y, Z)
ISPLUS_IN_GGA(succ(X), pred(Y), Z) → ISPLUS_IN_GGA(X, Y, Z)
ISPLUS_IN_GGA(pred(X), pred(Y), pred(pred(Z))) → ISPLUS_IN_GGA(X, Y, Z)

The TRS R consists of the following rules:

mmultiply_in_gga([], X, []) → mmultiply_out_gga([], X, [])
mmultiply_in_gga(.(V0, Rest), V1, .(Result, Others)) → U1_gga(V0, Rest, V1, Result, Others, mmultiply_in_gga(Rest, V1, Others))
U1_gga(V0, Rest, V1, Result, Others, mmultiply_out_gga(Rest, V1, Others)) → U2_gga(V0, Rest, V1, Result, Others, multiply_in_gga(V1, V0, Result))
multiply_in_gga([], X, []) → multiply_out_gga([], X, [])
multiply_in_gga(.(V0, Rest), V1, .(Result, Others)) → U3_gga(V0, Rest, V1, Result, Others, multiply_in_gga(Rest, V1, Others))
U3_gga(V0, Rest, V1, Result, Others, multiply_out_gga(Rest, V1, Others)) → U4_gga(V0, Rest, V1, Result, Others, vmul_in_gga(V0, V1, Result))
vmul_in_gga([], [], zero) → vmul_out_gga([], [], zero)
vmul_in_gga(.(H1, T1), .(H2, T2), Result) → U5_gga(H1, T1, H2, T2, Result, vmul_in_gga(T1, T2, Newresult))
U5_gga(H1, T1, H2, T2, Result, vmul_out_gga(T1, T2, Newresult)) → U6_gga(H1, T1, H2, T2, Result, Newresult, isTimes_in_gga(H1, H2, U))
isTimes_in_gga(X, zero, zero) → isTimes_out_gga(X, zero, zero)
isTimes_in_gga(zero, succ(Y), zero) → isTimes_out_gga(zero, succ(Y), zero)
isTimes_in_gga(zero, pred(Y), zero) → isTimes_out_gga(zero, pred(Y), zero)
isTimes_in_gga(succ(X), succ(Y), Z) → U37_gga(X, Y, Z, isTimes_in_gga(succ(X), Y, A))
isTimes_in_gga(succ(X), pred(Y), Z) → U39_gga(X, Y, Z, isTimes_in_gga(succ(X), Y, A))
isTimes_in_gga(pred(X), succ(Y), Z) → U41_gga(X, Y, Z, isTimes_in_gga(pred(X), Y, A))
isTimes_in_gga(pred(X), pred(Y), Z) → U43_gga(X, Y, Z, isTimes_in_gga(pred(X), Y, A))
U43_gga(X, Y, Z, isTimes_out_gga(pred(X), Y, A)) → U44_gga(X, Y, Z, isMinus_in_gga(A, pred(X), Z))
isMinus_in_gga(X, zero, X) → isMinus_out_gga(X, zero, X)
isMinus_in_gga(zero, succ(Y), pred(Z)) → U31_gga(Y, Z, isMinus_in_gga(zero, Y, Z))
isMinus_in_gga(zero, pred(Y), succ(Z)) → U32_gga(Y, Z, isMinus_in_gga(zero, Y, Z))
isMinus_in_gga(succ(X), succ(Y), Z) → U33_gga(X, Y, Z, isMinus_in_gga(X, Y, Z))
isMinus_in_gga(succ(X), pred(Y), succ(succ(Z))) → U34_gga(X, Y, Z, isMinus_in_gga(X, Y, Z))
isMinus_in_gga(pred(X), succ(Y), pred(pred(Z))) → U35_gga(X, Y, Z, isMinus_in_gga(X, Y, Z))
isMinus_in_gga(pred(X), pred(Y), Z) → U36_gga(X, Y, Z, isMinus_in_gga(X, Y, Z))
U36_gga(X, Y, Z, isMinus_out_gga(X, Y, Z)) → isMinus_out_gga(pred(X), pred(Y), Z)
U35_gga(X, Y, Z, isMinus_out_gga(X, Y, Z)) → isMinus_out_gga(pred(X), succ(Y), pred(pred(Z)))
U34_gga(X, Y, Z, isMinus_out_gga(X, Y, Z)) → isMinus_out_gga(succ(X), pred(Y), succ(succ(Z)))
U33_gga(X, Y, Z, isMinus_out_gga(X, Y, Z)) → isMinus_out_gga(succ(X), succ(Y), Z)
U32_gga(Y, Z, isMinus_out_gga(zero, Y, Z)) → isMinus_out_gga(zero, pred(Y), succ(Z))
U31_gga(Y, Z, isMinus_out_gga(zero, Y, Z)) → isMinus_out_gga(zero, succ(Y), pred(Z))
U44_gga(X, Y, Z, isMinus_out_gga(A, pred(X), Z)) → isTimes_out_gga(pred(X), pred(Y), Z)
U41_gga(X, Y, Z, isTimes_out_gga(pred(X), Y, A)) → U42_gga(X, Y, Z, isPlus_in_gga(A, pred(X), Z))
isPlus_in_gga(zero, X, X) → isPlus_out_gga(zero, X, X)
isPlus_in_gga(succ(X), zero, succ(X)) → isPlus_out_gga(succ(X), zero, succ(X))
isPlus_in_gga(succ(X), succ(Y), succ(succ(Z))) → U27_gga(X, Y, Z, isPlus_in_gga(X, Y, Z))
isPlus_in_gga(succ(X), pred(Y), Z) → U28_gga(X, Y, Z, isPlus_in_gga(X, Y, Z))
isPlus_in_gga(pred(X), zero, pred(X)) → isPlus_out_gga(pred(X), zero, pred(X))
isPlus_in_gga(pred(X), succ(Y), Z) → U29_gga(X, Y, Z, isPlus_in_gga(X, Y, Z))
isPlus_in_gga(pred(X), pred(Y), pred(pred(Z))) → U30_gga(X, Y, Z, isPlus_in_gga(X, Y, Z))
U30_gga(X, Y, Z, isPlus_out_gga(X, Y, Z)) → isPlus_out_gga(pred(X), pred(Y), pred(pred(Z)))
U29_gga(X, Y, Z, isPlus_out_gga(X, Y, Z)) → isPlus_out_gga(pred(X), succ(Y), Z)
U28_gga(X, Y, Z, isPlus_out_gga(X, Y, Z)) → isPlus_out_gga(succ(X), pred(Y), Z)
U27_gga(X, Y, Z, isPlus_out_gga(X, Y, Z)) → isPlus_out_gga(succ(X), succ(Y), succ(succ(Z)))
U42_gga(X, Y, Z, isPlus_out_gga(A, pred(X), Z)) → isTimes_out_gga(pred(X), succ(Y), Z)
U39_gga(X, Y, Z, isTimes_out_gga(succ(X), Y, A)) → U40_gga(X, Y, Z, isMinus_in_gga(A, succ(X), Z))
U40_gga(X, Y, Z, isMinus_out_gga(A, succ(X), Z)) → isTimes_out_gga(succ(X), pred(Y), Z)
U37_gga(X, Y, Z, isTimes_out_gga(succ(X), Y, A)) → U38_gga(X, Y, Z, isPlus_in_gga(A, succ(X), Z))
U38_gga(X, Y, Z, isPlus_out_gga(A, succ(X), Z)) → isTimes_out_gga(succ(X), succ(Y), Z)
U6_gga(H1, T1, H2, T2, Result, Newresult, isTimes_out_gga(H1, H2, U)) → U7_gga(H1, T1, H2, T2, Result, Newresult, U, =_in_ag(Product, U))
=_in_ag(X, X) → =_out_ag(X, X)
U7_gga(H1, T1, H2, T2, Result, Newresult, U, =_out_ag(Product, U)) → U8_gga(H1, T1, H2, T2, Result, U, isPlus_in_ggg(Product, Newresult, U))
isPlus_in_ggg(zero, X, X) → isPlus_out_ggg(zero, X, X)
isPlus_in_ggg(succ(X), zero, succ(X)) → isPlus_out_ggg(succ(X), zero, succ(X))
isPlus_in_ggg(succ(X), succ(Y), succ(succ(Z))) → U27_ggg(X, Y, Z, isPlus_in_ggg(X, Y, Z))
isPlus_in_ggg(succ(X), pred(Y), Z) → U28_ggg(X, Y, Z, isPlus_in_ggg(X, Y, Z))
isPlus_in_ggg(pred(X), zero, pred(X)) → isPlus_out_ggg(pred(X), zero, pred(X))
isPlus_in_ggg(pred(X), succ(Y), Z) → U29_ggg(X, Y, Z, isPlus_in_ggg(X, Y, Z))
isPlus_in_ggg(pred(X), pred(Y), pred(pred(Z))) → U30_ggg(X, Y, Z, isPlus_in_ggg(X, Y, Z))
U30_ggg(X, Y, Z, isPlus_out_ggg(X, Y, Z)) → isPlus_out_ggg(pred(X), pred(Y), pred(pred(Z)))
U29_ggg(X, Y, Z, isPlus_out_ggg(X, Y, Z)) → isPlus_out_ggg(pred(X), succ(Y), Z)
U28_ggg(X, Y, Z, isPlus_out_ggg(X, Y, Z)) → isPlus_out_ggg(succ(X), pred(Y), Z)
U27_ggg(X, Y, Z, isPlus_out_ggg(X, Y, Z)) → isPlus_out_ggg(succ(X), succ(Y), succ(succ(Z)))
U8_gga(H1, T1, H2, T2, Result, U, isPlus_out_ggg(Product, Newresult, U)) → U9_gga(H1, T1, H2, T2, Result, =_in_ag(Result, U))
U9_gga(H1, T1, H2, T2, Result, =_out_ag(Result, U)) → vmul_out_gga(.(H1, T1), .(H2, T2), Result)
U4_gga(V0, Rest, V1, Result, Others, vmul_out_gga(V0, V1, Result)) → multiply_out_gga(.(V0, Rest), V1, .(Result, Others))
U2_gga(V0, Rest, V1, Result, Others, multiply_out_gga(V1, V0, Result)) → mmultiply_out_gga(.(V0, Rest), V1, .(Result, Others))

↳ Prolog

  ↳ PredefinedPredicateTransformerProof

    ↳ Prolog

      ↳ PrologToPiTRSProof

        ↳ PiTRS

          ↳ DependencyPairsProof

            ↳ PiDP

              ↳ DependencyGraphProof

                ↳ AND

                  ↳ PiDP

                  ↳ PiDP

                    ↳ UsableRulesProof

                      ↳ PiDP

                        ↳ PiDPToQDPProof

                  ↳ PiDP

                  ↳ PiDP

                  ↳ PiDP

                  ↳ PiDP

                  ↳ PiDP

                  ↳ PiDP

                  ↳ PiDP

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

ISPLUS_IN_GGA(succ(X), succ(Y), succ(succ(Z))) → ISPLUS_IN_GGA(X, Y, Z)
ISPLUS_IN_GGA(pred(X), succ(Y), Z) → ISPLUS_IN_GGA(X, Y, Z)
ISPLUS_IN_GGA(succ(X), pred(Y), Z) → ISPLUS_IN_GGA(X, Y, Z)
ISPLUS_IN_GGA(pred(X), pred(Y), pred(pred(Z))) → ISPLUS_IN_GGA(X, Y, Z)

R is empty.
The argument filtering Pi contains the following mapping:
succ(x1) = succ(x1)
pred(x1) = pred(x1)
ISPLUS_IN_GGA(x1, x2, x3) = ISPLUS_IN_GGA(x1, x2)

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

↳ Prolog

  ↳ PredefinedPredicateTransformerProof

    ↳ Prolog

      ↳ PrologToPiTRSProof

        ↳ PiTRS

          ↳ DependencyPairsProof

            ↳ PiDP

              ↳ DependencyGraphProof

                ↳ AND

                  ↳ PiDP

                  ↳ PiDP

                    ↳ UsableRulesProof

                      ↳ PiDP

                        ↳ PiDPToQDPProof

                          ↳ QDP

                            ↳ QDPSizeChangeProof

                  ↳ PiDP

                  ↳ PiDP

                  ↳ PiDP

                  ↳ PiDP

                  ↳ PiDP

                  ↳ PiDP

                  ↳ PiDP

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

ISPLUS_IN_GGA(succ(X), pred(Y)) → ISPLUS_IN_GGA(X, Y)
ISPLUS_IN_GGA(pred(X), succ(Y)) → ISPLUS_IN_GGA(X, Y)
ISPLUS_IN_GGA(pred(X), pred(Y)) → ISPLUS_IN_GGA(X, Y)
ISPLUS_IN_GGA(succ(X), succ(Y)) → ISPLUS_IN_GGA(X, Y)

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

ISPLUS_IN_GGA(succ(X), succ(Y)) → ISPLUS_IN_GGA(X, Y)
The graph contains the following edges 1 > 1, 2 > 2
ISPLUS_IN_GGA(pred(X), succ(Y)) → ISPLUS_IN_GGA(X, Y)
The graph contains the following edges 1 > 1, 2 > 2
ISPLUS_IN_GGA(succ(X), pred(Y)) → ISPLUS_IN_GGA(X, Y)
The graph contains the following edges 1 > 1, 2 > 2
ISPLUS_IN_GGA(pred(X), pred(Y)) → ISPLUS_IN_GGA(X, Y)
The graph contains the following edges 1 > 1, 2 > 2

↳ Prolog

  ↳ PredefinedPredicateTransformerProof

    ↳ Prolog

      ↳ PrologToPiTRSProof

        ↳ PiTRS

          ↳ DependencyPairsProof

            ↳ PiDP

              ↳ DependencyGraphProof

                ↳ AND

                  ↳ PiDP

                  ↳ PiDP

                  ↳ PiDP

                    ↳ UsableRulesProof

                  ↳ PiDP

                  ↳ PiDP

                  ↳ PiDP

                  ↳ PiDP

                  ↳ PiDP

                  ↳ PiDP

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

ISMINUS_IN_GGA(zero, succ(Y), pred(Z)) → ISMINUS_IN_GGA(zero, Y, Z)
ISMINUS_IN_GGA(zero, pred(Y), succ(Z)) → ISMINUS_IN_GGA(zero, Y, Z)

The TRS R consists of the following rules:

mmultiply_in_gga([], X, []) → mmultiply_out_gga([], X, [])
mmultiply_in_gga(.(V0, Rest), V1, .(Result, Others)) → U1_gga(V0, Rest, V1, Result, Others, mmultiply_in_gga(Rest, V1, Others))
U1_gga(V0, Rest, V1, Result, Others, mmultiply_out_gga(Rest, V1, Others)) → U2_gga(V0, Rest, V1, Result, Others, multiply_in_gga(V1, V0, Result))
multiply_in_gga([], X, []) → multiply_out_gga([], X, [])
multiply_in_gga(.(V0, Rest), V1, .(Result, Others)) → U3_gga(V0, Rest, V1, Result, Others, multiply_in_gga(Rest, V1, Others))
U3_gga(V0, Rest, V1, Result, Others, multiply_out_gga(Rest, V1, Others)) → U4_gga(V0, Rest, V1, Result, Others, vmul_in_gga(V0, V1, Result))
vmul_in_gga([], [], zero) → vmul_out_gga([], [], zero)
vmul_in_gga(.(H1, T1), .(H2, T2), Result) → U5_gga(H1, T1, H2, T2, Result, vmul_in_gga(T1, T2, Newresult))
U5_gga(H1, T1, H2, T2, Result, vmul_out_gga(T1, T2, Newresult)) → U6_gga(H1, T1, H2, T2, Result, Newresult, isTimes_in_gga(H1, H2, U))
isTimes_in_gga(X, zero, zero) → isTimes_out_gga(X, zero, zero)
isTimes_in_gga(zero, succ(Y), zero) → isTimes_out_gga(zero, succ(Y), zero)
isTimes_in_gga(zero, pred(Y), zero) → isTimes_out_gga(zero, pred(Y), zero)
isTimes_in_gga(succ(X), succ(Y), Z) → U37_gga(X, Y, Z, isTimes_in_gga(succ(X), Y, A))
isTimes_in_gga(succ(X), pred(Y), Z) → U39_gga(X, Y, Z, isTimes_in_gga(succ(X), Y, A))
isTimes_in_gga(pred(X), succ(Y), Z) → U41_gga(X, Y, Z, isTimes_in_gga(pred(X), Y, A))
isTimes_in_gga(pred(X), pred(Y), Z) → U43_gga(X, Y, Z, isTimes_in_gga(pred(X), Y, A))
U43_gga(X, Y, Z, isTimes_out_gga(pred(X), Y, A)) → U44_gga(X, Y, Z, isMinus_in_gga(A, pred(X), Z))
isMinus_in_gga(X, zero, X) → isMinus_out_gga(X, zero, X)
isMinus_in_gga(zero, succ(Y), pred(Z)) → U31_gga(Y, Z, isMinus_in_gga(zero, Y, Z))
isMinus_in_gga(zero, pred(Y), succ(Z)) → U32_gga(Y, Z, isMinus_in_gga(zero, Y, Z))
isMinus_in_gga(succ(X), succ(Y), Z) → U33_gga(X, Y, Z, isMinus_in_gga(X, Y, Z))
isMinus_in_gga(succ(X), pred(Y), succ(succ(Z))) → U34_gga(X, Y, Z, isMinus_in_gga(X, Y, Z))
isMinus_in_gga(pred(X), succ(Y), pred(pred(Z))) → U35_gga(X, Y, Z, isMinus_in_gga(X, Y, Z))
isMinus_in_gga(pred(X), pred(Y), Z) → U36_gga(X, Y, Z, isMinus_in_gga(X, Y, Z))
U36_gga(X, Y, Z, isMinus_out_gga(X, Y, Z)) → isMinus_out_gga(pred(X), pred(Y), Z)
U35_gga(X, Y, Z, isMinus_out_gga(X, Y, Z)) → isMinus_out_gga(pred(X), succ(Y), pred(pred(Z)))
U34_gga(X, Y, Z, isMinus_out_gga(X, Y, Z)) → isMinus_out_gga(succ(X), pred(Y), succ(succ(Z)))
U33_gga(X, Y, Z, isMinus_out_gga(X, Y, Z)) → isMinus_out_gga(succ(X), succ(Y), Z)
U32_gga(Y, Z, isMinus_out_gga(zero, Y, Z)) → isMinus_out_gga(zero, pred(Y), succ(Z))
U31_gga(Y, Z, isMinus_out_gga(zero, Y, Z)) → isMinus_out_gga(zero, succ(Y), pred(Z))
U44_gga(X, Y, Z, isMinus_out_gga(A, pred(X), Z)) → isTimes_out_gga(pred(X), pred(Y), Z)
U41_gga(X, Y, Z, isTimes_out_gga(pred(X), Y, A)) → U42_gga(X, Y, Z, isPlus_in_gga(A, pred(X), Z))
isPlus_in_gga(zero, X, X) → isPlus_out_gga(zero, X, X)
isPlus_in_gga(succ(X), zero, succ(X)) → isPlus_out_gga(succ(X), zero, succ(X))
isPlus_in_gga(succ(X), succ(Y), succ(succ(Z))) → U27_gga(X, Y, Z, isPlus_in_gga(X, Y, Z))
isPlus_in_gga(succ(X), pred(Y), Z) → U28_gga(X, Y, Z, isPlus_in_gga(X, Y, Z))
isPlus_in_gga(pred(X), zero, pred(X)) → isPlus_out_gga(pred(X), zero, pred(X))
isPlus_in_gga(pred(X), succ(Y), Z) → U29_gga(X, Y, Z, isPlus_in_gga(X, Y, Z))
isPlus_in_gga(pred(X), pred(Y), pred(pred(Z))) → U30_gga(X, Y, Z, isPlus_in_gga(X, Y, Z))
U30_gga(X, Y, Z, isPlus_out_gga(X, Y, Z)) → isPlus_out_gga(pred(X), pred(Y), pred(pred(Z)))
U29_gga(X, Y, Z, isPlus_out_gga(X, Y, Z)) → isPlus_out_gga(pred(X), succ(Y), Z)
U28_gga(X, Y, Z, isPlus_out_gga(X, Y, Z)) → isPlus_out_gga(succ(X), pred(Y), Z)
U27_gga(X, Y, Z, isPlus_out_gga(X, Y, Z)) → isPlus_out_gga(succ(X), succ(Y), succ(succ(Z)))
U42_gga(X, Y, Z, isPlus_out_gga(A, pred(X), Z)) → isTimes_out_gga(pred(X), succ(Y), Z)
U39_gga(X, Y, Z, isTimes_out_gga(succ(X), Y, A)) → U40_gga(X, Y, Z, isMinus_in_gga(A, succ(X), Z))
U40_gga(X, Y, Z, isMinus_out_gga(A, succ(X), Z)) → isTimes_out_gga(succ(X), pred(Y), Z)
U37_gga(X, Y, Z, isTimes_out_gga(succ(X), Y, A)) → U38_gga(X, Y, Z, isPlus_in_gga(A, succ(X), Z))
U38_gga(X, Y, Z, isPlus_out_gga(A, succ(X), Z)) → isTimes_out_gga(succ(X), succ(Y), Z)
U6_gga(H1, T1, H2, T2, Result, Newresult, isTimes_out_gga(H1, H2, U)) → U7_gga(H1, T1, H2, T2, Result, Newresult, U, =_in_ag(Product, U))
=_in_ag(X, X) → =_out_ag(X, X)
U7_gga(H1, T1, H2, T2, Result, Newresult, U, =_out_ag(Product, U)) → U8_gga(H1, T1, H2, T2, Result, U, isPlus_in_ggg(Product, Newresult, U))
isPlus_in_ggg(zero, X, X) → isPlus_out_ggg(zero, X, X)
isPlus_in_ggg(succ(X), zero, succ(X)) → isPlus_out_ggg(succ(X), zero, succ(X))
isPlus_in_ggg(succ(X), succ(Y), succ(succ(Z))) → U27_ggg(X, Y, Z, isPlus_in_ggg(X, Y, Z))
isPlus_in_ggg(succ(X), pred(Y), Z) → U28_ggg(X, Y, Z, isPlus_in_ggg(X, Y, Z))
isPlus_in_ggg(pred(X), zero, pred(X)) → isPlus_out_ggg(pred(X), zero, pred(X))
isPlus_in_ggg(pred(X), succ(Y), Z) → U29_ggg(X, Y, Z, isPlus_in_ggg(X, Y, Z))
isPlus_in_ggg(pred(X), pred(Y), pred(pred(Z))) → U30_ggg(X, Y, Z, isPlus_in_ggg(X, Y, Z))
U30_ggg(X, Y, Z, isPlus_out_ggg(X, Y, Z)) → isPlus_out_ggg(pred(X), pred(Y), pred(pred(Z)))
U29_ggg(X, Y, Z, isPlus_out_ggg(X, Y, Z)) → isPlus_out_ggg(pred(X), succ(Y), Z)
U28_ggg(X, Y, Z, isPlus_out_ggg(X, Y, Z)) → isPlus_out_ggg(succ(X), pred(Y), Z)
U27_ggg(X, Y, Z, isPlus_out_ggg(X, Y, Z)) → isPlus_out_ggg(succ(X), succ(Y), succ(succ(Z)))
U8_gga(H1, T1, H2, T2, Result, U, isPlus_out_ggg(Product, Newresult, U)) → U9_gga(H1, T1, H2, T2, Result, =_in_ag(Result, U))
U9_gga(H1, T1, H2, T2, Result, =_out_ag(Result, U)) → vmul_out_gga(.(H1, T1), .(H2, T2), Result)
U4_gga(V0, Rest, V1, Result, Others, vmul_out_gga(V0, V1, Result)) → multiply_out_gga(.(V0, Rest), V1, .(Result, Others))
U2_gga(V0, Rest, V1, Result, Others, multiply_out_gga(V1, V0, Result)) → mmultiply_out_gga(.(V0, Rest), V1, .(Result, Others))

↳ Prolog

  ↳ PredefinedPredicateTransformerProof

    ↳ Prolog

      ↳ PrologToPiTRSProof

        ↳ PiTRS

          ↳ DependencyPairsProof

            ↳ PiDP

              ↳ DependencyGraphProof

                ↳ AND

                  ↳ PiDP

                  ↳ PiDP

                  ↳ PiDP

                    ↳ UsableRulesProof

                      ↳ PiDP

                        ↳ PiDPToQDPProof

                  ↳ PiDP

                  ↳ PiDP

                  ↳ PiDP

                  ↳ PiDP

                  ↳ PiDP

                  ↳ PiDP

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

ISMINUS_IN_GGA(zero, succ(Y), pred(Z)) → ISMINUS_IN_GGA(zero, Y, Z)
ISMINUS_IN_GGA(zero, pred(Y), succ(Z)) → ISMINUS_IN_GGA(zero, Y, Z)

R is empty.
The argument filtering Pi contains the following mapping:
zero = zero
succ(x1) = succ(x1)
pred(x1) = pred(x1)
ISMINUS_IN_GGA(x1, x2, x3) = ISMINUS_IN_GGA(x1, x2)

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

↳ Prolog

  ↳ PredefinedPredicateTransformerProof

    ↳ Prolog

      ↳ PrologToPiTRSProof

        ↳ PiTRS

          ↳ DependencyPairsProof

            ↳ PiDP

              ↳ DependencyGraphProof

                ↳ AND

                  ↳ PiDP

                  ↳ PiDP

                  ↳ PiDP

                    ↳ UsableRulesProof

                      ↳ PiDP

                        ↳ PiDPToQDPProof

                          ↳ QDP

                            ↳ QDPSizeChangeProof

                  ↳ PiDP

                  ↳ PiDP

                  ↳ PiDP

                  ↳ PiDP

                  ↳ PiDP

                  ↳ PiDP

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

ISMINUS_IN_GGA(zero, pred(Y)) → ISMINUS_IN_GGA(zero, Y)
ISMINUS_IN_GGA(zero, succ(Y)) → ISMINUS_IN_GGA(zero, Y)

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

ISMINUS_IN_GGA(zero, succ(Y)) → ISMINUS_IN_GGA(zero, Y)
The graph contains the following edges 1 >= 1, 2 > 2
ISMINUS_IN_GGA(zero, pred(Y)) → ISMINUS_IN_GGA(zero, Y)
The graph contains the following edges 1 >= 1, 2 > 2

↳ Prolog

  ↳ PredefinedPredicateTransformerProof

    ↳ Prolog

      ↳ PrologToPiTRSProof

        ↳ PiTRS

          ↳ DependencyPairsProof

            ↳ PiDP

              ↳ DependencyGraphProof

                ↳ AND

                  ↳ PiDP

                  ↳ PiDP

                  ↳ PiDP

                  ↳ PiDP

                    ↳ UsableRulesProof

                  ↳ PiDP

                  ↳ PiDP

                  ↳ PiDP

                  ↳ PiDP

                  ↳ PiDP

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

ISMINUS_IN_GGA(pred(X), succ(Y), pred(pred(Z))) → ISMINUS_IN_GGA(X, Y, Z)
ISMINUS_IN_GGA(succ(X), pred(Y), succ(succ(Z))) → ISMINUS_IN_GGA(X, Y, Z)
ISMINUS_IN_GGA(succ(X), succ(Y), Z) → ISMINUS_IN_GGA(X, Y, Z)
ISMINUS_IN_GGA(pred(X), pred(Y), Z) → ISMINUS_IN_GGA(X, Y, Z)

The TRS R consists of the following rules:

mmultiply_in_gga([], X, []) → mmultiply_out_gga([], X, [])
mmultiply_in_gga(.(V0, Rest), V1, .(Result, Others)) → U1_gga(V0, Rest, V1, Result, Others, mmultiply_in_gga(Rest, V1, Others))
U1_gga(V0, Rest, V1, Result, Others, mmultiply_out_gga(Rest, V1, Others)) → U2_gga(V0, Rest, V1, Result, Others, multiply_in_gga(V1, V0, Result))
multiply_in_gga([], X, []) → multiply_out_gga([], X, [])
multiply_in_gga(.(V0, Rest), V1, .(Result, Others)) → U3_gga(V0, Rest, V1, Result, Others, multiply_in_gga(Rest, V1, Others))
U3_gga(V0, Rest, V1, Result, Others, multiply_out_gga(Rest, V1, Others)) → U4_gga(V0, Rest, V1, Result, Others, vmul_in_gga(V0, V1, Result))
vmul_in_gga([], [], zero) → vmul_out_gga([], [], zero)
vmul_in_gga(.(H1, T1), .(H2, T2), Result) → U5_gga(H1, T1, H2, T2, Result, vmul_in_gga(T1, T2, Newresult))
U5_gga(H1, T1, H2, T2, Result, vmul_out_gga(T1, T2, Newresult)) → U6_gga(H1, T1, H2, T2, Result, Newresult, isTimes_in_gga(H1, H2, U))
isTimes_in_gga(X, zero, zero) → isTimes_out_gga(X, zero, zero)
isTimes_in_gga(zero, succ(Y), zero) → isTimes_out_gga(zero, succ(Y), zero)
isTimes_in_gga(zero, pred(Y), zero) → isTimes_out_gga(zero, pred(Y), zero)
isTimes_in_gga(succ(X), succ(Y), Z) → U37_gga(X, Y, Z, isTimes_in_gga(succ(X), Y, A))
isTimes_in_gga(succ(X), pred(Y), Z) → U39_gga(X, Y, Z, isTimes_in_gga(succ(X), Y, A))
isTimes_in_gga(pred(X), succ(Y), Z) → U41_gga(X, Y, Z, isTimes_in_gga(pred(X), Y, A))
isTimes_in_gga(pred(X), pred(Y), Z) → U43_gga(X, Y, Z, isTimes_in_gga(pred(X), Y, A))
U43_gga(X, Y, Z, isTimes_out_gga(pred(X), Y, A)) → U44_gga(X, Y, Z, isMinus_in_gga(A, pred(X), Z))
isMinus_in_gga(X, zero, X) → isMinus_out_gga(X, zero, X)
isMinus_in_gga(zero, succ(Y), pred(Z)) → U31_gga(Y, Z, isMinus_in_gga(zero, Y, Z))
isMinus_in_gga(zero, pred(Y), succ(Z)) → U32_gga(Y, Z, isMinus_in_gga(zero, Y, Z))
isMinus_in_gga(succ(X), succ(Y), Z) → U33_gga(X, Y, Z, isMinus_in_gga(X, Y, Z))
isMinus_in_gga(succ(X), pred(Y), succ(succ(Z))) → U34_gga(X, Y, Z, isMinus_in_gga(X, Y, Z))
isMinus_in_gga(pred(X), succ(Y), pred(pred(Z))) → U35_gga(X, Y, Z, isMinus_in_gga(X, Y, Z))
isMinus_in_gga(pred(X), pred(Y), Z) → U36_gga(X, Y, Z, isMinus_in_gga(X, Y, Z))
U36_gga(X, Y, Z, isMinus_out_gga(X, Y, Z)) → isMinus_out_gga(pred(X), pred(Y), Z)
U35_gga(X, Y, Z, isMinus_out_gga(X, Y, Z)) → isMinus_out_gga(pred(X), succ(Y), pred(pred(Z)))
U34_gga(X, Y, Z, isMinus_out_gga(X, Y, Z)) → isMinus_out_gga(succ(X), pred(Y), succ(succ(Z)))
U33_gga(X, Y, Z, isMinus_out_gga(X, Y, Z)) → isMinus_out_gga(succ(X), succ(Y), Z)
U32_gga(Y, Z, isMinus_out_gga(zero, Y, Z)) → isMinus_out_gga(zero, pred(Y), succ(Z))
U31_gga(Y, Z, isMinus_out_gga(zero, Y, Z)) → isMinus_out_gga(zero, succ(Y), pred(Z))
U44_gga(X, Y, Z, isMinus_out_gga(A, pred(X), Z)) → isTimes_out_gga(pred(X), pred(Y), Z)
U41_gga(X, Y, Z, isTimes_out_gga(pred(X), Y, A)) → U42_gga(X, Y, Z, isPlus_in_gga(A, pred(X), Z))
isPlus_in_gga(zero, X, X) → isPlus_out_gga(zero, X, X)
isPlus_in_gga(succ(X), zero, succ(X)) → isPlus_out_gga(succ(X), zero, succ(X))
isPlus_in_gga(succ(X), succ(Y), succ(succ(Z))) → U27_gga(X, Y, Z, isPlus_in_gga(X, Y, Z))
isPlus_in_gga(succ(X), pred(Y), Z) → U28_gga(X, Y, Z, isPlus_in_gga(X, Y, Z))
isPlus_in_gga(pred(X), zero, pred(X)) → isPlus_out_gga(pred(X), zero, pred(X))
isPlus_in_gga(pred(X), succ(Y), Z) → U29_gga(X, Y, Z, isPlus_in_gga(X, Y, Z))
isPlus_in_gga(pred(X), pred(Y), pred(pred(Z))) → U30_gga(X, Y, Z, isPlus_in_gga(X, Y, Z))
U30_gga(X, Y, Z, isPlus_out_gga(X, Y, Z)) → isPlus_out_gga(pred(X), pred(Y), pred(pred(Z)))
U29_gga(X, Y, Z, isPlus_out_gga(X, Y, Z)) → isPlus_out_gga(pred(X), succ(Y), Z)
U28_gga(X, Y, Z, isPlus_out_gga(X, Y, Z)) → isPlus_out_gga(succ(X), pred(Y), Z)
U27_gga(X, Y, Z, isPlus_out_gga(X, Y, Z)) → isPlus_out_gga(succ(X), succ(Y), succ(succ(Z)))
U42_gga(X, Y, Z, isPlus_out_gga(A, pred(X), Z)) → isTimes_out_gga(pred(X), succ(Y), Z)
U39_gga(X, Y, Z, isTimes_out_gga(succ(X), Y, A)) → U40_gga(X, Y, Z, isMinus_in_gga(A, succ(X), Z))
U40_gga(X, Y, Z, isMinus_out_gga(A, succ(X), Z)) → isTimes_out_gga(succ(X), pred(Y), Z)
U37_gga(X, Y, Z, isTimes_out_gga(succ(X), Y, A)) → U38_gga(X, Y, Z, isPlus_in_gga(A, succ(X), Z))
U38_gga(X, Y, Z, isPlus_out_gga(A, succ(X), Z)) → isTimes_out_gga(succ(X), succ(Y), Z)
U6_gga(H1, T1, H2, T2, Result, Newresult, isTimes_out_gga(H1, H2, U)) → U7_gga(H1, T1, H2, T2, Result, Newresult, U, =_in_ag(Product, U))
=_in_ag(X, X) → =_out_ag(X, X)
U7_gga(H1, T1, H2, T2, Result, Newresult, U, =_out_ag(Product, U)) → U8_gga(H1, T1, H2, T2, Result, U, isPlus_in_ggg(Product, Newresult, U))
isPlus_in_ggg(zero, X, X) → isPlus_out_ggg(zero, X, X)
isPlus_in_ggg(succ(X), zero, succ(X)) → isPlus_out_ggg(succ(X), zero, succ(X))
isPlus_in_ggg(succ(X), succ(Y), succ(succ(Z))) → U27_ggg(X, Y, Z, isPlus_in_ggg(X, Y, Z))
isPlus_in_ggg(succ(X), pred(Y), Z) → U28_ggg(X, Y, Z, isPlus_in_ggg(X, Y, Z))
isPlus_in_ggg(pred(X), zero, pred(X)) → isPlus_out_ggg(pred(X), zero, pred(X))
isPlus_in_ggg(pred(X), succ(Y), Z) → U29_ggg(X, Y, Z, isPlus_in_ggg(X, Y, Z))
isPlus_in_ggg(pred(X), pred(Y), pred(pred(Z))) → U30_ggg(X, Y, Z, isPlus_in_ggg(X, Y, Z))
U30_ggg(X, Y, Z, isPlus_out_ggg(X, Y, Z)) → isPlus_out_ggg(pred(X), pred(Y), pred(pred(Z)))
U29_ggg(X, Y, Z, isPlus_out_ggg(X, Y, Z)) → isPlus_out_ggg(pred(X), succ(Y), Z)
U28_ggg(X, Y, Z, isPlus_out_ggg(X, Y, Z)) → isPlus_out_ggg(succ(X), pred(Y), Z)
U27_ggg(X, Y, Z, isPlus_out_ggg(X, Y, Z)) → isPlus_out_ggg(succ(X), succ(Y), succ(succ(Z)))
U8_gga(H1, T1, H2, T2, Result, U, isPlus_out_ggg(Product, Newresult, U)) → U9_gga(H1, T1, H2, T2, Result, =_in_ag(Result, U))
U9_gga(H1, T1, H2, T2, Result, =_out_ag(Result, U)) → vmul_out_gga(.(H1, T1), .(H2, T2), Result)
U4_gga(V0, Rest, V1, Result, Others, vmul_out_gga(V0, V1, Result)) → multiply_out_gga(.(V0, Rest), V1, .(Result, Others))
U2_gga(V0, Rest, V1, Result, Others, multiply_out_gga(V1, V0, Result)) → mmultiply_out_gga(.(V0, Rest), V1, .(Result, Others))

↳ Prolog

  ↳ PredefinedPredicateTransformerProof

    ↳ Prolog

      ↳ PrologToPiTRSProof

        ↳ PiTRS

          ↳ DependencyPairsProof

            ↳ PiDP

              ↳ DependencyGraphProof

                ↳ AND

                  ↳ PiDP

                  ↳ PiDP

                  ↳ PiDP

                  ↳ PiDP

                    ↳ UsableRulesProof

                      ↳ PiDP

                        ↳ PiDPToQDPProof

                  ↳ PiDP

                  ↳ PiDP

                  ↳ PiDP

                  ↳ PiDP

                  ↳ PiDP

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

ISMINUS_IN_GGA(pred(X), succ(Y), pred(pred(Z))) → ISMINUS_IN_GGA(X, Y, Z)
ISMINUS_IN_GGA(succ(X), pred(Y), succ(succ(Z))) → ISMINUS_IN_GGA(X, Y, Z)
ISMINUS_IN_GGA(succ(X), succ(Y), Z) → ISMINUS_IN_GGA(X, Y, Z)
ISMINUS_IN_GGA(pred(X), pred(Y), Z) → ISMINUS_IN_GGA(X, Y, Z)

R is empty.
The argument filtering Pi contains the following mapping:
succ(x1) = succ(x1)
pred(x1) = pred(x1)
ISMINUS_IN_GGA(x1, x2, x3) = ISMINUS_IN_GGA(x1, x2)

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

↳ Prolog

  ↳ PredefinedPredicateTransformerProof

    ↳ Prolog

      ↳ PrologToPiTRSProof

        ↳ PiTRS

          ↳ DependencyPairsProof

            ↳ PiDP

              ↳ DependencyGraphProof

                ↳ AND

                  ↳ PiDP

                  ↳ PiDP

                  ↳ PiDP

                  ↳ PiDP

                    ↳ UsableRulesProof

                      ↳ PiDP

                        ↳ PiDPToQDPProof

                          ↳ QDP

                            ↳ QDPSizeChangeProof

                  ↳ PiDP

                  ↳ PiDP

                  ↳ PiDP

                  ↳ PiDP

                  ↳ PiDP

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

ISMINUS_IN_GGA(succ(X), succ(Y)) → ISMINUS_IN_GGA(X, Y)
ISMINUS_IN_GGA(pred(X), pred(Y)) → ISMINUS_IN_GGA(X, Y)
ISMINUS_IN_GGA(succ(X), pred(Y)) → ISMINUS_IN_GGA(X, Y)
ISMINUS_IN_GGA(pred(X), succ(Y)) → ISMINUS_IN_GGA(X, Y)

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

ISMINUS_IN_GGA(pred(X), succ(Y)) → ISMINUS_IN_GGA(X, Y)
The graph contains the following edges 1 > 1, 2 > 2
ISMINUS_IN_GGA(succ(X), pred(Y)) → ISMINUS_IN_GGA(X, Y)
The graph contains the following edges 1 > 1, 2 > 2
ISMINUS_IN_GGA(succ(X), succ(Y)) → ISMINUS_IN_GGA(X, Y)
The graph contains the following edges 1 > 1, 2 > 2
ISMINUS_IN_GGA(pred(X), pred(Y)) → ISMINUS_IN_GGA(X, Y)
The graph contains the following edges 1 > 1, 2 > 2

↳ Prolog

  ↳ PredefinedPredicateTransformerProof

    ↳ Prolog

      ↳ PrologToPiTRSProof

        ↳ PiTRS

          ↳ DependencyPairsProof

            ↳ PiDP

              ↳ DependencyGraphProof

                ↳ AND

                  ↳ PiDP

                  ↳ PiDP

                  ↳ PiDP

                  ↳ PiDP

                  ↳ PiDP

                    ↳ UsableRulesProof

                  ↳ PiDP

                  ↳ PiDP

                  ↳ PiDP

                  ↳ PiDP

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

ISTIMES_IN_GGA(pred(X), pred(Y), Z) → ISTIMES_IN_GGA(pred(X), Y, A)
ISTIMES_IN_GGA(pred(X), succ(Y), Z) → ISTIMES_IN_GGA(pred(X), Y, A)

The TRS R consists of the following rules:

mmultiply_in_gga([], X, []) → mmultiply_out_gga([], X, [])
mmultiply_in_gga(.(V0, Rest), V1, .(Result, Others)) → U1_gga(V0, Rest, V1, Result, Others, mmultiply_in_gga(Rest, V1, Others))
U1_gga(V0, Rest, V1, Result, Others, mmultiply_out_gga(Rest, V1, Others)) → U2_gga(V0, Rest, V1, Result, Others, multiply_in_gga(V1, V0, Result))
multiply_in_gga([], X, []) → multiply_out_gga([], X, [])
multiply_in_gga(.(V0, Rest), V1, .(Result, Others)) → U3_gga(V0, Rest, V1, Result, Others, multiply_in_gga(Rest, V1, Others))
U3_gga(V0, Rest, V1, Result, Others, multiply_out_gga(Rest, V1, Others)) → U4_gga(V0, Rest, V1, Result, Others, vmul_in_gga(V0, V1, Result))
vmul_in_gga([], [], zero) → vmul_out_gga([], [], zero)
vmul_in_gga(.(H1, T1), .(H2, T2), Result) → U5_gga(H1, T1, H2, T2, Result, vmul_in_gga(T1, T2, Newresult))
U5_gga(H1, T1, H2, T2, Result, vmul_out_gga(T1, T2, Newresult)) → U6_gga(H1, T1, H2, T2, Result, Newresult, isTimes_in_gga(H1, H2, U))
isTimes_in_gga(X, zero, zero) → isTimes_out_gga(X, zero, zero)
isTimes_in_gga(zero, succ(Y), zero) → isTimes_out_gga(zero, succ(Y), zero)
isTimes_in_gga(zero, pred(Y), zero) → isTimes_out_gga(zero, pred(Y), zero)
isTimes_in_gga(succ(X), succ(Y), Z) → U37_gga(X, Y, Z, isTimes_in_gga(succ(X), Y, A))
isTimes_in_gga(succ(X), pred(Y), Z) → U39_gga(X, Y, Z, isTimes_in_gga(succ(X), Y, A))
isTimes_in_gga(pred(X), succ(Y), Z) → U41_gga(X, Y, Z, isTimes_in_gga(pred(X), Y, A))
isTimes_in_gga(pred(X), pred(Y), Z) → U43_gga(X, Y, Z, isTimes_in_gga(pred(X), Y, A))
U43_gga(X, Y, Z, isTimes_out_gga(pred(X), Y, A)) → U44_gga(X, Y, Z, isMinus_in_gga(A, pred(X), Z))
isMinus_in_gga(X, zero, X) → isMinus_out_gga(X, zero, X)
isMinus_in_gga(zero, succ(Y), pred(Z)) → U31_gga(Y, Z, isMinus_in_gga(zero, Y, Z))
isMinus_in_gga(zero, pred(Y), succ(Z)) → U32_gga(Y, Z, isMinus_in_gga(zero, Y, Z))
isMinus_in_gga(succ(X), succ(Y), Z) → U33_gga(X, Y, Z, isMinus_in_gga(X, Y, Z))
isMinus_in_gga(succ(X), pred(Y), succ(succ(Z))) → U34_gga(X, Y, Z, isMinus_in_gga(X, Y, Z))
isMinus_in_gga(pred(X), succ(Y), pred(pred(Z))) → U35_gga(X, Y, Z, isMinus_in_gga(X, Y, Z))
isMinus_in_gga(pred(X), pred(Y), Z) → U36_gga(X, Y, Z, isMinus_in_gga(X, Y, Z))
U36_gga(X, Y, Z, isMinus_out_gga(X, Y, Z)) → isMinus_out_gga(pred(X), pred(Y), Z)
U35_gga(X, Y, Z, isMinus_out_gga(X, Y, Z)) → isMinus_out_gga(pred(X), succ(Y), pred(pred(Z)))
U34_gga(X, Y, Z, isMinus_out_gga(X, Y, Z)) → isMinus_out_gga(succ(X), pred(Y), succ(succ(Z)))
U33_gga(X, Y, Z, isMinus_out_gga(X, Y, Z)) → isMinus_out_gga(succ(X), succ(Y), Z)
U32_gga(Y, Z, isMinus_out_gga(zero, Y, Z)) → isMinus_out_gga(zero, pred(Y), succ(Z))
U31_gga(Y, Z, isMinus_out_gga(zero, Y, Z)) → isMinus_out_gga(zero, succ(Y), pred(Z))
U44_gga(X, Y, Z, isMinus_out_gga(A, pred(X), Z)) → isTimes_out_gga(pred(X), pred(Y), Z)
U41_gga(X, Y, Z, isTimes_out_gga(pred(X), Y, A)) → U42_gga(X, Y, Z, isPlus_in_gga(A, pred(X), Z))
isPlus_in_gga(zero, X, X) → isPlus_out_gga(zero, X, X)
isPlus_in_gga(succ(X), zero, succ(X)) → isPlus_out_gga(succ(X), zero, succ(X))
isPlus_in_gga(succ(X), succ(Y), succ(succ(Z))) → U27_gga(X, Y, Z, isPlus_in_gga(X, Y, Z))
isPlus_in_gga(succ(X), pred(Y), Z) → U28_gga(X, Y, Z, isPlus_in_gga(X, Y, Z))
isPlus_in_gga(pred(X), zero, pred(X)) → isPlus_out_gga(pred(X), zero, pred(X))
isPlus_in_gga(pred(X), succ(Y), Z) → U29_gga(X, Y, Z, isPlus_in_gga(X, Y, Z))
isPlus_in_gga(pred(X), pred(Y), pred(pred(Z))) → U30_gga(X, Y, Z, isPlus_in_gga(X, Y, Z))
U30_gga(X, Y, Z, isPlus_out_gga(X, Y, Z)) → isPlus_out_gga(pred(X), pred(Y), pred(pred(Z)))
U29_gga(X, Y, Z, isPlus_out_gga(X, Y, Z)) → isPlus_out_gga(pred(X), succ(Y), Z)
U28_gga(X, Y, Z, isPlus_out_gga(X, Y, Z)) → isPlus_out_gga(succ(X), pred(Y), Z)
U27_gga(X, Y, Z, isPlus_out_gga(X, Y, Z)) → isPlus_out_gga(succ(X), succ(Y), succ(succ(Z)))
U42_gga(X, Y, Z, isPlus_out_gga(A, pred(X), Z)) → isTimes_out_gga(pred(X), succ(Y), Z)
U39_gga(X, Y, Z, isTimes_out_gga(succ(X), Y, A)) → U40_gga(X, Y, Z, isMinus_in_gga(A, succ(X), Z))
U40_gga(X, Y, Z, isMinus_out_gga(A, succ(X), Z)) → isTimes_out_gga(succ(X), pred(Y), Z)
U37_gga(X, Y, Z, isTimes_out_gga(succ(X), Y, A)) → U38_gga(X, Y, Z, isPlus_in_gga(A, succ(X), Z))
U38_gga(X, Y, Z, isPlus_out_gga(A, succ(X), Z)) → isTimes_out_gga(succ(X), succ(Y), Z)
U6_gga(H1, T1, H2, T2, Result, Newresult, isTimes_out_gga(H1, H2, U)) → U7_gga(H1, T1, H2, T2, Result, Newresult, U, =_in_ag(Product, U))
=_in_ag(X, X) → =_out_ag(X, X)
U7_gga(H1, T1, H2, T2, Result, Newresult, U, =_out_ag(Product, U)) → U8_gga(H1, T1, H2, T2, Result, U, isPlus_in_ggg(Product, Newresult, U))
isPlus_in_ggg(zero, X, X) → isPlus_out_ggg(zero, X, X)
isPlus_in_ggg(succ(X), zero, succ(X)) → isPlus_out_ggg(succ(X), zero, succ(X))
isPlus_in_ggg(succ(X), succ(Y), succ(succ(Z))) → U27_ggg(X, Y, Z, isPlus_in_ggg(X, Y, Z))
isPlus_in_ggg(succ(X), pred(Y), Z) → U28_ggg(X, Y, Z, isPlus_in_ggg(X, Y, Z))
isPlus_in_ggg(pred(X), zero, pred(X)) → isPlus_out_ggg(pred(X), zero, pred(X))
isPlus_in_ggg(pred(X), succ(Y), Z) → U29_ggg(X, Y, Z, isPlus_in_ggg(X, Y, Z))
isPlus_in_ggg(pred(X), pred(Y), pred(pred(Z))) → U30_ggg(X, Y, Z, isPlus_in_ggg(X, Y, Z))
U30_ggg(X, Y, Z, isPlus_out_ggg(X, Y, Z)) → isPlus_out_ggg(pred(X), pred(Y), pred(pred(Z)))
U29_ggg(X, Y, Z, isPlus_out_ggg(X, Y, Z)) → isPlus_out_ggg(pred(X), succ(Y), Z)
U28_ggg(X, Y, Z, isPlus_out_ggg(X, Y, Z)) → isPlus_out_ggg(succ(X), pred(Y), Z)
U27_ggg(X, Y, Z, isPlus_out_ggg(X, Y, Z)) → isPlus_out_ggg(succ(X), succ(Y), succ(succ(Z)))
U8_gga(H1, T1, H2, T2, Result, U, isPlus_out_ggg(Product, Newresult, U)) → U9_gga(H1, T1, H2, T2, Result, =_in_ag(Result, U))
U9_gga(H1, T1, H2, T2, Result, =_out_ag(Result, U)) → vmul_out_gga(.(H1, T1), .(H2, T2), Result)
U4_gga(V0, Rest, V1, Result, Others, vmul_out_gga(V0, V1, Result)) → multiply_out_gga(.(V0, Rest), V1, .(Result, Others))
U2_gga(V0, Rest, V1, Result, Others, multiply_out_gga(V1, V0, Result)) → mmultiply_out_gga(.(V0, Rest), V1, .(Result, Others))

↳ Prolog

  ↳ PredefinedPredicateTransformerProof

    ↳ Prolog

      ↳ PrologToPiTRSProof

        ↳ PiTRS

          ↳ DependencyPairsProof

            ↳ PiDP

              ↳ DependencyGraphProof

                ↳ AND

                  ↳ PiDP

                  ↳ PiDP

                  ↳ PiDP

                  ↳ PiDP

                  ↳ PiDP

                    ↳ UsableRulesProof

                      ↳ PiDP

                        ↳ PiDPToQDPProof

                  ↳ PiDP

                  ↳ PiDP

                  ↳ PiDP

                  ↳ PiDP

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

ISTIMES_IN_GGA(pred(X), pred(Y), Z) → ISTIMES_IN_GGA(pred(X), Y, A)
ISTIMES_IN_GGA(pred(X), succ(Y), Z) → ISTIMES_IN_GGA(pred(X), Y, A)

R is empty.
The argument filtering Pi contains the following mapping:
succ(x1) = succ(x1)
pred(x1) = pred(x1)
ISTIMES_IN_GGA(x1, x2, x3) = ISTIMES_IN_GGA(x1, x2)

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

↳ Prolog

  ↳ PredefinedPredicateTransformerProof

    ↳ Prolog

      ↳ PrologToPiTRSProof

        ↳ PiTRS

          ↳ DependencyPairsProof

            ↳ PiDP

              ↳ DependencyGraphProof

                ↳ AND

                  ↳ PiDP

                  ↳ PiDP

                  ↳ PiDP

                  ↳ PiDP

                  ↳ PiDP

                    ↳ UsableRulesProof

                      ↳ PiDP

                        ↳ PiDPToQDPProof

                          ↳ QDP

                            ↳ QDPSizeChangeProof

                  ↳ PiDP

                  ↳ PiDP

                  ↳ PiDP

                  ↳ PiDP

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

ISTIMES_IN_GGA(pred(X), pred(Y)) → ISTIMES_IN_GGA(pred(X), Y)
ISTIMES_IN_GGA(pred(X), succ(Y)) → ISTIMES_IN_GGA(pred(X), Y)

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

ISTIMES_IN_GGA(pred(X), pred(Y)) → ISTIMES_IN_GGA(pred(X), Y)
The graph contains the following edges 1 >= 1, 2 > 2
ISTIMES_IN_GGA(pred(X), succ(Y)) → ISTIMES_IN_GGA(pred(X), Y)
The graph contains the following edges 1 >= 1, 2 > 2

↳ Prolog

  ↳ PredefinedPredicateTransformerProof

    ↳ Prolog

      ↳ PrologToPiTRSProof

        ↳ PiTRS

          ↳ DependencyPairsProof

            ↳ PiDP

              ↳ DependencyGraphProof

                ↳ AND

                  ↳ PiDP

                  ↳ PiDP

                  ↳ PiDP

                  ↳ PiDP

                  ↳ PiDP

                  ↳ PiDP

                    ↳ UsableRulesProof

                  ↳ PiDP

                  ↳ PiDP

                  ↳ PiDP

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

ISTIMES_IN_GGA(succ(X), succ(Y), Z) → ISTIMES_IN_GGA(succ(X), Y, A)
ISTIMES_IN_GGA(succ(X), pred(Y), Z) → ISTIMES_IN_GGA(succ(X), Y, A)

The TRS R consists of the following rules:

mmultiply_in_gga([], X, []) → mmultiply_out_gga([], X, [])
mmultiply_in_gga(.(V0, Rest), V1, .(Result, Others)) → U1_gga(V0, Rest, V1, Result, Others, mmultiply_in_gga(Rest, V1, Others))
U1_gga(V0, Rest, V1, Result, Others, mmultiply_out_gga(Rest, V1, Others)) → U2_gga(V0, Rest, V1, Result, Others, multiply_in_gga(V1, V0, Result))
multiply_in_gga([], X, []) → multiply_out_gga([], X, [])
multiply_in_gga(.(V0, Rest), V1, .(Result, Others)) → U3_gga(V0, Rest, V1, Result, Others, multiply_in_gga(Rest, V1, Others))
U3_gga(V0, Rest, V1, Result, Others, multiply_out_gga(Rest, V1, Others)) → U4_gga(V0, Rest, V1, Result, Others, vmul_in_gga(V0, V1, Result))
vmul_in_gga([], [], zero) → vmul_out_gga([], [], zero)
vmul_in_gga(.(H1, T1), .(H2, T2), Result) → U5_gga(H1, T1, H2, T2, Result, vmul_in_gga(T1, T2, Newresult))
U5_gga(H1, T1, H2, T2, Result, vmul_out_gga(T1, T2, Newresult)) → U6_gga(H1, T1, H2, T2, Result, Newresult, isTimes_in_gga(H1, H2, U))
isTimes_in_gga(X, zero, zero) → isTimes_out_gga(X, zero, zero)
isTimes_in_gga(zero, succ(Y), zero) → isTimes_out_gga(zero, succ(Y), zero)
isTimes_in_gga(zero, pred(Y), zero) → isTimes_out_gga(zero, pred(Y), zero)
isTimes_in_gga(succ(X), succ(Y), Z) → U37_gga(X, Y, Z, isTimes_in_gga(succ(X), Y, A))
isTimes_in_gga(succ(X), pred(Y), Z) → U39_gga(X, Y, Z, isTimes_in_gga(succ(X), Y, A))
isTimes_in_gga(pred(X), succ(Y), Z) → U41_gga(X, Y, Z, isTimes_in_gga(pred(X), Y, A))
isTimes_in_gga(pred(X), pred(Y), Z) → U43_gga(X, Y, Z, isTimes_in_gga(pred(X), Y, A))
U43_gga(X, Y, Z, isTimes_out_gga(pred(X), Y, A)) → U44_gga(X, Y, Z, isMinus_in_gga(A, pred(X), Z))
isMinus_in_gga(X, zero, X) → isMinus_out_gga(X, zero, X)
isMinus_in_gga(zero, succ(Y), pred(Z)) → U31_gga(Y, Z, isMinus_in_gga(zero, Y, Z))
isMinus_in_gga(zero, pred(Y), succ(Z)) → U32_gga(Y, Z, isMinus_in_gga(zero, Y, Z))
isMinus_in_gga(succ(X), succ(Y), Z) → U33_gga(X, Y, Z, isMinus_in_gga(X, Y, Z))
isMinus_in_gga(succ(X), pred(Y), succ(succ(Z))) → U34_gga(X, Y, Z, isMinus_in_gga(X, Y, Z))
isMinus_in_gga(pred(X), succ(Y), pred(pred(Z))) → U35_gga(X, Y, Z, isMinus_in_gga(X, Y, Z))
isMinus_in_gga(pred(X), pred(Y), Z) → U36_gga(X, Y, Z, isMinus_in_gga(X, Y, Z))
U36_gga(X, Y, Z, isMinus_out_gga(X, Y, Z)) → isMinus_out_gga(pred(X), pred(Y), Z)
U35_gga(X, Y, Z, isMinus_out_gga(X, Y, Z)) → isMinus_out_gga(pred(X), succ(Y), pred(pred(Z)))
U34_gga(X, Y, Z, isMinus_out_gga(X, Y, Z)) → isMinus_out_gga(succ(X), pred(Y), succ(succ(Z)))
U33_gga(X, Y, Z, isMinus_out_gga(X, Y, Z)) → isMinus_out_gga(succ(X), succ(Y), Z)
U32_gga(Y, Z, isMinus_out_gga(zero, Y, Z)) → isMinus_out_gga(zero, pred(Y), succ(Z))
U31_gga(Y, Z, isMinus_out_gga(zero, Y, Z)) → isMinus_out_gga(zero, succ(Y), pred(Z))
U44_gga(X, Y, Z, isMinus_out_gga(A, pred(X), Z)) → isTimes_out_gga(pred(X), pred(Y), Z)
U41_gga(X, Y, Z, isTimes_out_gga(pred(X), Y, A)) → U42_gga(X, Y, Z, isPlus_in_gga(A, pred(X), Z))
isPlus_in_gga(zero, X, X) → isPlus_out_gga(zero, X, X)
isPlus_in_gga(succ(X), zero, succ(X)) → isPlus_out_gga(succ(X), zero, succ(X))
isPlus_in_gga(succ(X), succ(Y), succ(succ(Z))) → U27_gga(X, Y, Z, isPlus_in_gga(X, Y, Z))
isPlus_in_gga(succ(X), pred(Y), Z) → U28_gga(X, Y, Z, isPlus_in_gga(X, Y, Z))
isPlus_in_gga(pred(X), zero, pred(X)) → isPlus_out_gga(pred(X), zero, pred(X))
isPlus_in_gga(pred(X), succ(Y), Z) → U29_gga(X, Y, Z, isPlus_in_gga(X, Y, Z))
isPlus_in_gga(pred(X), pred(Y), pred(pred(Z))) → U30_gga(X, Y, Z, isPlus_in_gga(X, Y, Z))
U30_gga(X, Y, Z, isPlus_out_gga(X, Y, Z)) → isPlus_out_gga(pred(X), pred(Y), pred(pred(Z)))
U29_gga(X, Y, Z, isPlus_out_gga(X, Y, Z)) → isPlus_out_gga(pred(X), succ(Y), Z)
U28_gga(X, Y, Z, isPlus_out_gga(X, Y, Z)) → isPlus_out_gga(succ(X), pred(Y), Z)
U27_gga(X, Y, Z, isPlus_out_gga(X, Y, Z)) → isPlus_out_gga(succ(X), succ(Y), succ(succ(Z)))
U42_gga(X, Y, Z, isPlus_out_gga(A, pred(X), Z)) → isTimes_out_gga(pred(X), succ(Y), Z)
U39_gga(X, Y, Z, isTimes_out_gga(succ(X), Y, A)) → U40_gga(X, Y, Z, isMinus_in_gga(A, succ(X), Z))
U40_gga(X, Y, Z, isMinus_out_gga(A, succ(X), Z)) → isTimes_out_gga(succ(X), pred(Y), Z)
U37_gga(X, Y, Z, isTimes_out_gga(succ(X), Y, A)) → U38_gga(X, Y, Z, isPlus_in_gga(A, succ(X), Z))
U38_gga(X, Y, Z, isPlus_out_gga(A, succ(X), Z)) → isTimes_out_gga(succ(X), succ(Y), Z)
U6_gga(H1, T1, H2, T2, Result, Newresult, isTimes_out_gga(H1, H2, U)) → U7_gga(H1, T1, H2, T2, Result, Newresult, U, =_in_ag(Product, U))
=_in_ag(X, X) → =_out_ag(X, X)
U7_gga(H1, T1, H2, T2, Result, Newresult, U, =_out_ag(Product, U)) → U8_gga(H1, T1, H2, T2, Result, U, isPlus_in_ggg(Product, Newresult, U))
isPlus_in_ggg(zero, X, X) → isPlus_out_ggg(zero, X, X)
isPlus_in_ggg(succ(X), zero, succ(X)) → isPlus_out_ggg(succ(X), zero, succ(X))
isPlus_in_ggg(succ(X), succ(Y), succ(succ(Z))) → U27_ggg(X, Y, Z, isPlus_in_ggg(X, Y, Z))
isPlus_in_ggg(succ(X), pred(Y), Z) → U28_ggg(X, Y, Z, isPlus_in_ggg(X, Y, Z))
isPlus_in_ggg(pred(X), zero, pred(X)) → isPlus_out_ggg(pred(X), zero, pred(X))
isPlus_in_ggg(pred(X), succ(Y), Z) → U29_ggg(X, Y, Z, isPlus_in_ggg(X, Y, Z))
isPlus_in_ggg(pred(X), pred(Y), pred(pred(Z))) → U30_ggg(X, Y, Z, isPlus_in_ggg(X, Y, Z))
U30_ggg(X, Y, Z, isPlus_out_ggg(X, Y, Z)) → isPlus_out_ggg(pred(X), pred(Y), pred(pred(Z)))
U29_ggg(X, Y, Z, isPlus_out_ggg(X, Y, Z)) → isPlus_out_ggg(pred(X), succ(Y), Z)
U28_ggg(X, Y, Z, isPlus_out_ggg(X, Y, Z)) → isPlus_out_ggg(succ(X), pred(Y), Z)
U27_ggg(X, Y, Z, isPlus_out_ggg(X, Y, Z)) → isPlus_out_ggg(succ(X), succ(Y), succ(succ(Z)))
U8_gga(H1, T1, H2, T2, Result, U, isPlus_out_ggg(Product, Newresult, U)) → U9_gga(H1, T1, H2, T2, Result, =_in_ag(Result, U))
U9_gga(H1, T1, H2, T2, Result, =_out_ag(Result, U)) → vmul_out_gga(.(H1, T1), .(H2, T2), Result)
U4_gga(V0, Rest, V1, Result, Others, vmul_out_gga(V0, V1, Result)) → multiply_out_gga(.(V0, Rest), V1, .(Result, Others))
U2_gga(V0, Rest, V1, Result, Others, multiply_out_gga(V1, V0, Result)) → mmultiply_out_gga(.(V0, Rest), V1, .(Result, Others))

↳ Prolog

  ↳ PredefinedPredicateTransformerProof

    ↳ Prolog

      ↳ PrologToPiTRSProof

        ↳ PiTRS

          ↳ DependencyPairsProof

            ↳ PiDP

              ↳ DependencyGraphProof

                ↳ AND

                  ↳ PiDP

                  ↳ PiDP

                  ↳ PiDP

                  ↳ PiDP

                  ↳ PiDP

                  ↳ PiDP

                    ↳ UsableRulesProof

                      ↳ PiDP

                        ↳ PiDPToQDPProof

                  ↳ PiDP

                  ↳ PiDP

                  ↳ PiDP

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

ISTIMES_IN_GGA(succ(X), succ(Y), Z) → ISTIMES_IN_GGA(succ(X), Y, A)
ISTIMES_IN_GGA(succ(X), pred(Y), Z) → ISTIMES_IN_GGA(succ(X), Y, A)

↳ Prolog

  ↳ PredefinedPredicateTransformerProof

    ↳ Prolog

      ↳ PrologToPiTRSProof

        ↳ PiTRS

          ↳ DependencyPairsProof

            ↳ PiDP

              ↳ DependencyGraphProof

                ↳ AND

                  ↳ PiDP

                  ↳ PiDP

                  ↳ PiDP

                  ↳ PiDP

                  ↳ PiDP

                  ↳ PiDP

                    ↳ UsableRulesProof

                      ↳ PiDP

                        ↳ PiDPToQDPProof

                          ↳ QDP

                            ↳ QDPSizeChangeProof

                  ↳ PiDP

                  ↳ PiDP

                  ↳ PiDP

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

ISTIMES_IN_GGA(succ(X), pred(Y)) → ISTIMES_IN_GGA(succ(X), Y)
ISTIMES_IN_GGA(succ(X), succ(Y)) → ISTIMES_IN_GGA(succ(X), Y)

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

ISTIMES_IN_GGA(succ(X), succ(Y)) → ISTIMES_IN_GGA(succ(X), Y)
The graph contains the following edges 1 >= 1, 2 > 2
ISTIMES_IN_GGA(succ(X), pred(Y)) → ISTIMES_IN_GGA(succ(X), Y)
The graph contains the following edges 1 >= 1, 2 > 2

↳ Prolog

  ↳ PredefinedPredicateTransformerProof

    ↳ Prolog

      ↳ PrologToPiTRSProof

        ↳ PiTRS

          ↳ DependencyPairsProof

            ↳ PiDP

              ↳ DependencyGraphProof

                ↳ AND

                  ↳ PiDP

                  ↳ PiDP

                  ↳ PiDP

                  ↳ PiDP

                  ↳ PiDP

                  ↳ PiDP

                  ↳ PiDP

                    ↳ UsableRulesProof

                  ↳ PiDP

                  ↳ PiDP

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

VMUL_IN_GGA(.(H1, T1), .(H2, T2), Result) → VMUL_IN_GGA(T1, T2, Newresult)

The TRS R consists of the following rules:

mmultiply_in_gga([], X, []) → mmultiply_out_gga([], X, [])
mmultiply_in_gga(.(V0, Rest), V1, .(Result, Others)) → U1_gga(V0, Rest, V1, Result, Others, mmultiply_in_gga(Rest, V1, Others))
U1_gga(V0, Rest, V1, Result, Others, mmultiply_out_gga(Rest, V1, Others)) → U2_gga(V0, Rest, V1, Result, Others, multiply_in_gga(V1, V0, Result))
multiply_in_gga([], X, []) → multiply_out_gga([], X, [])
multiply_in_gga(.(V0, Rest), V1, .(Result, Others)) → U3_gga(V0, Rest, V1, Result, Others, multiply_in_gga(Rest, V1, Others))
U3_gga(V0, Rest, V1, Result, Others, multiply_out_gga(Rest, V1, Others)) → U4_gga(V0, Rest, V1, Result, Others, vmul_in_gga(V0, V1, Result))
vmul_in_gga([], [], zero) → vmul_out_gga([], [], zero)
vmul_in_gga(.(H1, T1), .(H2, T2), Result) → U5_gga(H1, T1, H2, T2, Result, vmul_in_gga(T1, T2, Newresult))
U5_gga(H1, T1, H2, T2, Result, vmul_out_gga(T1, T2, Newresult)) → U6_gga(H1, T1, H2, T2, Result, Newresult, isTimes_in_gga(H1, H2, U))
isTimes_in_gga(X, zero, zero) → isTimes_out_gga(X, zero, zero)
isTimes_in_gga(zero, succ(Y), zero) → isTimes_out_gga(zero, succ(Y), zero)
isTimes_in_gga(zero, pred(Y), zero) → isTimes_out_gga(zero, pred(Y), zero)
isTimes_in_gga(succ(X), succ(Y), Z) → U37_gga(X, Y, Z, isTimes_in_gga(succ(X), Y, A))
isTimes_in_gga(succ(X), pred(Y), Z) → U39_gga(X, Y, Z, isTimes_in_gga(succ(X), Y, A))
isTimes_in_gga(pred(X), succ(Y), Z) → U41_gga(X, Y, Z, isTimes_in_gga(pred(X), Y, A))
isTimes_in_gga(pred(X), pred(Y), Z) → U43_gga(X, Y, Z, isTimes_in_gga(pred(X), Y, A))
U43_gga(X, Y, Z, isTimes_out_gga(pred(X), Y, A)) → U44_gga(X, Y, Z, isMinus_in_gga(A, pred(X), Z))
isMinus_in_gga(X, zero, X) → isMinus_out_gga(X, zero, X)
isMinus_in_gga(zero, succ(Y), pred(Z)) → U31_gga(Y, Z, isMinus_in_gga(zero, Y, Z))
isMinus_in_gga(zero, pred(Y), succ(Z)) → U32_gga(Y, Z, isMinus_in_gga(zero, Y, Z))
isMinus_in_gga(succ(X), succ(Y), Z) → U33_gga(X, Y, Z, isMinus_in_gga(X, Y, Z))
isMinus_in_gga(succ(X), pred(Y), succ(succ(Z))) → U34_gga(X, Y, Z, isMinus_in_gga(X, Y, Z))
isMinus_in_gga(pred(X), succ(Y), pred(pred(Z))) → U35_gga(X, Y, Z, isMinus_in_gga(X, Y, Z))
isMinus_in_gga(pred(X), pred(Y), Z) → U36_gga(X, Y, Z, isMinus_in_gga(X, Y, Z))
U36_gga(X, Y, Z, isMinus_out_gga(X, Y, Z)) → isMinus_out_gga(pred(X), pred(Y), Z)
U35_gga(X, Y, Z, isMinus_out_gga(X, Y, Z)) → isMinus_out_gga(pred(X), succ(Y), pred(pred(Z)))
U34_gga(X, Y, Z, isMinus_out_gga(X, Y, Z)) → isMinus_out_gga(succ(X), pred(Y), succ(succ(Z)))
U33_gga(X, Y, Z, isMinus_out_gga(X, Y, Z)) → isMinus_out_gga(succ(X), succ(Y), Z)
U32_gga(Y, Z, isMinus_out_gga(zero, Y, Z)) → isMinus_out_gga(zero, pred(Y), succ(Z))
U31_gga(Y, Z, isMinus_out_gga(zero, Y, Z)) → isMinus_out_gga(zero, succ(Y), pred(Z))
U44_gga(X, Y, Z, isMinus_out_gga(A, pred(X), Z)) → isTimes_out_gga(pred(X), pred(Y), Z)
U41_gga(X, Y, Z, isTimes_out_gga(pred(X), Y, A)) → U42_gga(X, Y, Z, isPlus_in_gga(A, pred(X), Z))
isPlus_in_gga(zero, X, X) → isPlus_out_gga(zero, X, X)
isPlus_in_gga(succ(X), zero, succ(X)) → isPlus_out_gga(succ(X), zero, succ(X))
isPlus_in_gga(succ(X), succ(Y), succ(succ(Z))) → U27_gga(X, Y, Z, isPlus_in_gga(X, Y, Z))
isPlus_in_gga(succ(X), pred(Y), Z) → U28_gga(X, Y, Z, isPlus_in_gga(X, Y, Z))
isPlus_in_gga(pred(X), zero, pred(X)) → isPlus_out_gga(pred(X), zero, pred(X))
isPlus_in_gga(pred(X), succ(Y), Z) → U29_gga(X, Y, Z, isPlus_in_gga(X, Y, Z))
isPlus_in_gga(pred(X), pred(Y), pred(pred(Z))) → U30_gga(X, Y, Z, isPlus_in_gga(X, Y, Z))
U30_gga(X, Y, Z, isPlus_out_gga(X, Y, Z)) → isPlus_out_gga(pred(X), pred(Y), pred(pred(Z)))
U29_gga(X, Y, Z, isPlus_out_gga(X, Y, Z)) → isPlus_out_gga(pred(X), succ(Y), Z)
U28_gga(X, Y, Z, isPlus_out_gga(X, Y, Z)) → isPlus_out_gga(succ(X), pred(Y), Z)
U27_gga(X, Y, Z, isPlus_out_gga(X, Y, Z)) → isPlus_out_gga(succ(X), succ(Y), succ(succ(Z)))
U42_gga(X, Y, Z, isPlus_out_gga(A, pred(X), Z)) → isTimes_out_gga(pred(X), succ(Y), Z)
U39_gga(X, Y, Z, isTimes_out_gga(succ(X), Y, A)) → U40_gga(X, Y, Z, isMinus_in_gga(A, succ(X), Z))
U40_gga(X, Y, Z, isMinus_out_gga(A, succ(X), Z)) → isTimes_out_gga(succ(X), pred(Y), Z)
U37_gga(X, Y, Z, isTimes_out_gga(succ(X), Y, A)) → U38_gga(X, Y, Z, isPlus_in_gga(A, succ(X), Z))
U38_gga(X, Y, Z, isPlus_out_gga(A, succ(X), Z)) → isTimes_out_gga(succ(X), succ(Y), Z)
U6_gga(H1, T1, H2, T2, Result, Newresult, isTimes_out_gga(H1, H2, U)) → U7_gga(H1, T1, H2, T2, Result, Newresult, U, =_in_ag(Product, U))
=_in_ag(X, X) → =_out_ag(X, X)
U7_gga(H1, T1, H2, T2, Result, Newresult, U, =_out_ag(Product, U)) → U8_gga(H1, T1, H2, T2, Result, U, isPlus_in_ggg(Product, Newresult, U))
isPlus_in_ggg(zero, X, X) → isPlus_out_ggg(zero, X, X)
isPlus_in_ggg(succ(X), zero, succ(X)) → isPlus_out_ggg(succ(X), zero, succ(X))
isPlus_in_ggg(succ(X), succ(Y), succ(succ(Z))) → U27_ggg(X, Y, Z, isPlus_in_ggg(X, Y, Z))
isPlus_in_ggg(succ(X), pred(Y), Z) → U28_ggg(X, Y, Z, isPlus_in_ggg(X, Y, Z))
isPlus_in_ggg(pred(X), zero, pred(X)) → isPlus_out_ggg(pred(X), zero, pred(X))
isPlus_in_ggg(pred(X), succ(Y), Z) → U29_ggg(X, Y, Z, isPlus_in_ggg(X, Y, Z))
isPlus_in_ggg(pred(X), pred(Y), pred(pred(Z))) → U30_ggg(X, Y, Z, isPlus_in_ggg(X, Y, Z))
U30_ggg(X, Y, Z, isPlus_out_ggg(X, Y, Z)) → isPlus_out_ggg(pred(X), pred(Y), pred(pred(Z)))
U29_ggg(X, Y, Z, isPlus_out_ggg(X, Y, Z)) → isPlus_out_ggg(pred(X), succ(Y), Z)
U28_ggg(X, Y, Z, isPlus_out_ggg(X, Y, Z)) → isPlus_out_ggg(succ(X), pred(Y), Z)
U27_ggg(X, Y, Z, isPlus_out_ggg(X, Y, Z)) → isPlus_out_ggg(succ(X), succ(Y), succ(succ(Z)))
U8_gga(H1, T1, H2, T2, Result, U, isPlus_out_ggg(Product, Newresult, U)) → U9_gga(H1, T1, H2, T2, Result, =_in_ag(Result, U))
U9_gga(H1, T1, H2, T2, Result, =_out_ag(Result, U)) → vmul_out_gga(.(H1, T1), .(H2, T2), Result)
U4_gga(V0, Rest, V1, Result, Others, vmul_out_gga(V0, V1, Result)) → multiply_out_gga(.(V0, Rest), V1, .(Result, Others))
U2_gga(V0, Rest, V1, Result, Others, multiply_out_gga(V1, V0, Result)) → mmultiply_out_gga(.(V0, Rest), V1, .(Result, Others))

↳ Prolog

  ↳ PredefinedPredicateTransformerProof

    ↳ Prolog

      ↳ PrologToPiTRSProof

        ↳ PiTRS

          ↳ DependencyPairsProof

            ↳ PiDP

              ↳ DependencyGraphProof

                ↳ AND

                  ↳ PiDP

                  ↳ PiDP

                  ↳ PiDP

                  ↳ PiDP

                  ↳ PiDP

                  ↳ PiDP

                  ↳ PiDP

                    ↳ UsableRulesProof

                      ↳ PiDP

                        ↳ PiDPToQDPProof

                  ↳ PiDP

                  ↳ PiDP

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

VMUL_IN_GGA(.(H1, T1), .(H2, T2), Result) → VMUL_IN_GGA(T1, T2, Newresult)

R is empty.
The argument filtering Pi contains the following mapping:
.(x1, x2) = .(x1, x2)
VMUL_IN_GGA(x1, x2, x3) = VMUL_IN_GGA(x1, x2)

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

↳ Prolog

  ↳ PredefinedPredicateTransformerProof

    ↳ Prolog

      ↳ PrologToPiTRSProof

        ↳ PiTRS

          ↳ DependencyPairsProof

            ↳ PiDP

              ↳ DependencyGraphProof

                ↳ AND

                  ↳ PiDP

                  ↳ PiDP

                  ↳ PiDP

                  ↳ PiDP

                  ↳ PiDP

                  ↳ PiDP

                  ↳ PiDP

                    ↳ UsableRulesProof

                      ↳ PiDP

                        ↳ PiDPToQDPProof

                          ↳ QDP

                            ↳ QDPSizeChangeProof

                  ↳ PiDP

                  ↳ PiDP

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

VMUL_IN_GGA(.(H1, T1), .(H2, T2)) → VMUL_IN_GGA(T1, T2)

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

VMUL_IN_GGA(.(H1, T1), .(H2, T2)) → VMUL_IN_GGA(T1, T2)
The graph contains the following edges 1 > 1, 2 > 2

↳ Prolog

  ↳ PredefinedPredicateTransformerProof

    ↳ Prolog

      ↳ PrologToPiTRSProof

        ↳ PiTRS

          ↳ DependencyPairsProof

            ↳ PiDP

              ↳ DependencyGraphProof

                ↳ AND

                  ↳ PiDP

                  ↳ PiDP

                  ↳ PiDP

                  ↳ PiDP

                  ↳ PiDP

                  ↳ PiDP

                  ↳ PiDP

                  ↳ PiDP

                    ↳ UsableRulesProof

                  ↳ PiDP

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

MULTIPLY_IN_GGA(.(V0, Rest), V1, .(Result, Others)) → MULTIPLY_IN_GGA(Rest, V1, Others)

The TRS R consists of the following rules:

mmultiply_in_gga([], X, []) → mmultiply_out_gga([], X, [])
mmultiply_in_gga(.(V0, Rest), V1, .(Result, Others)) → U1_gga(V0, Rest, V1, Result, Others, mmultiply_in_gga(Rest, V1, Others))
U1_gga(V0, Rest, V1, Result, Others, mmultiply_out_gga(Rest, V1, Others)) → U2_gga(V0, Rest, V1, Result, Others, multiply_in_gga(V1, V0, Result))
multiply_in_gga([], X, []) → multiply_out_gga([], X, [])
multiply_in_gga(.(V0, Rest), V1, .(Result, Others)) → U3_gga(V0, Rest, V1, Result, Others, multiply_in_gga(Rest, V1, Others))
U3_gga(V0, Rest, V1, Result, Others, multiply_out_gga(Rest, V1, Others)) → U4_gga(V0, Rest, V1, Result, Others, vmul_in_gga(V0, V1, Result))
vmul_in_gga([], [], zero) → vmul_out_gga([], [], zero)
vmul_in_gga(.(H1, T1), .(H2, T2), Result) → U5_gga(H1, T1, H2, T2, Result, vmul_in_gga(T1, T2, Newresult))
U5_gga(H1, T1, H2, T2, Result, vmul_out_gga(T1, T2, Newresult)) → U6_gga(H1, T1, H2, T2, Result, Newresult, isTimes_in_gga(H1, H2, U))
isTimes_in_gga(X, zero, zero) → isTimes_out_gga(X, zero, zero)
isTimes_in_gga(zero, succ(Y), zero) → isTimes_out_gga(zero, succ(Y), zero)
isTimes_in_gga(zero, pred(Y), zero) → isTimes_out_gga(zero, pred(Y), zero)
isTimes_in_gga(succ(X), succ(Y), Z) → U37_gga(X, Y, Z, isTimes_in_gga(succ(X), Y, A))
isTimes_in_gga(succ(X), pred(Y), Z) → U39_gga(X, Y, Z, isTimes_in_gga(succ(X), Y, A))
isTimes_in_gga(pred(X), succ(Y), Z) → U41_gga(X, Y, Z, isTimes_in_gga(pred(X), Y, A))
isTimes_in_gga(pred(X), pred(Y), Z) → U43_gga(X, Y, Z, isTimes_in_gga(pred(X), Y, A))
U43_gga(X, Y, Z, isTimes_out_gga(pred(X), Y, A)) → U44_gga(X, Y, Z, isMinus_in_gga(A, pred(X), Z))
isMinus_in_gga(X, zero, X) → isMinus_out_gga(X, zero, X)
isMinus_in_gga(zero, succ(Y), pred(Z)) → U31_gga(Y, Z, isMinus_in_gga(zero, Y, Z))
isMinus_in_gga(zero, pred(Y), succ(Z)) → U32_gga(Y, Z, isMinus_in_gga(zero, Y, Z))
isMinus_in_gga(succ(X), succ(Y), Z) → U33_gga(X, Y, Z, isMinus_in_gga(X, Y, Z))
isMinus_in_gga(succ(X), pred(Y), succ(succ(Z))) → U34_gga(X, Y, Z, isMinus_in_gga(X, Y, Z))
isMinus_in_gga(pred(X), succ(Y), pred(pred(Z))) → U35_gga(X, Y, Z, isMinus_in_gga(X, Y, Z))
isMinus_in_gga(pred(X), pred(Y), Z) → U36_gga(X, Y, Z, isMinus_in_gga(X, Y, Z))
U36_gga(X, Y, Z, isMinus_out_gga(X, Y, Z)) → isMinus_out_gga(pred(X), pred(Y), Z)
U35_gga(X, Y, Z, isMinus_out_gga(X, Y, Z)) → isMinus_out_gga(pred(X), succ(Y), pred(pred(Z)))
U34_gga(X, Y, Z, isMinus_out_gga(X, Y, Z)) → isMinus_out_gga(succ(X), pred(Y), succ(succ(Z)))
U33_gga(X, Y, Z, isMinus_out_gga(X, Y, Z)) → isMinus_out_gga(succ(X), succ(Y), Z)
U32_gga(Y, Z, isMinus_out_gga(zero, Y, Z)) → isMinus_out_gga(zero, pred(Y), succ(Z))
U31_gga(Y, Z, isMinus_out_gga(zero, Y, Z)) → isMinus_out_gga(zero, succ(Y), pred(Z))
U44_gga(X, Y, Z, isMinus_out_gga(A, pred(X), Z)) → isTimes_out_gga(pred(X), pred(Y), Z)
U41_gga(X, Y, Z, isTimes_out_gga(pred(X), Y, A)) → U42_gga(X, Y, Z, isPlus_in_gga(A, pred(X), Z))
isPlus_in_gga(zero, X, X) → isPlus_out_gga(zero, X, X)
isPlus_in_gga(succ(X), zero, succ(X)) → isPlus_out_gga(succ(X), zero, succ(X))
isPlus_in_gga(succ(X), succ(Y), succ(succ(Z))) → U27_gga(X, Y, Z, isPlus_in_gga(X, Y, Z))
isPlus_in_gga(succ(X), pred(Y), Z) → U28_gga(X, Y, Z, isPlus_in_gga(X, Y, Z))
isPlus_in_gga(pred(X), zero, pred(X)) → isPlus_out_gga(pred(X), zero, pred(X))
isPlus_in_gga(pred(X), succ(Y), Z) → U29_gga(X, Y, Z, isPlus_in_gga(X, Y, Z))
isPlus_in_gga(pred(X), pred(Y), pred(pred(Z))) → U30_gga(X, Y, Z, isPlus_in_gga(X, Y, Z))
U30_gga(X, Y, Z, isPlus_out_gga(X, Y, Z)) → isPlus_out_gga(pred(X), pred(Y), pred(pred(Z)))
U29_gga(X, Y, Z, isPlus_out_gga(X, Y, Z)) → isPlus_out_gga(pred(X), succ(Y), Z)
U28_gga(X, Y, Z, isPlus_out_gga(X, Y, Z)) → isPlus_out_gga(succ(X), pred(Y), Z)
U27_gga(X, Y, Z, isPlus_out_gga(X, Y, Z)) → isPlus_out_gga(succ(X), succ(Y), succ(succ(Z)))
U42_gga(X, Y, Z, isPlus_out_gga(A, pred(X), Z)) → isTimes_out_gga(pred(X), succ(Y), Z)
U39_gga(X, Y, Z, isTimes_out_gga(succ(X), Y, A)) → U40_gga(X, Y, Z, isMinus_in_gga(A, succ(X), Z))
U40_gga(X, Y, Z, isMinus_out_gga(A, succ(X), Z)) → isTimes_out_gga(succ(X), pred(Y), Z)
U37_gga(X, Y, Z, isTimes_out_gga(succ(X), Y, A)) → U38_gga(X, Y, Z, isPlus_in_gga(A, succ(X), Z))
U38_gga(X, Y, Z, isPlus_out_gga(A, succ(X), Z)) → isTimes_out_gga(succ(X), succ(Y), Z)
U6_gga(H1, T1, H2, T2, Result, Newresult, isTimes_out_gga(H1, H2, U)) → U7_gga(H1, T1, H2, T2, Result, Newresult, U, =_in_ag(Product, U))
=_in_ag(X, X) → =_out_ag(X, X)
U7_gga(H1, T1, H2, T2, Result, Newresult, U, =_out_ag(Product, U)) → U8_gga(H1, T1, H2, T2, Result, U, isPlus_in_ggg(Product, Newresult, U))
isPlus_in_ggg(zero, X, X) → isPlus_out_ggg(zero, X, X)
isPlus_in_ggg(succ(X), zero, succ(X)) → isPlus_out_ggg(succ(X), zero, succ(X))
isPlus_in_ggg(succ(X), succ(Y), succ(succ(Z))) → U27_ggg(X, Y, Z, isPlus_in_ggg(X, Y, Z))
isPlus_in_ggg(succ(X), pred(Y), Z) → U28_ggg(X, Y, Z, isPlus_in_ggg(X, Y, Z))
isPlus_in_ggg(pred(X), zero, pred(X)) → isPlus_out_ggg(pred(X), zero, pred(X))
isPlus_in_ggg(pred(X), succ(Y), Z) → U29_ggg(X, Y, Z, isPlus_in_ggg(X, Y, Z))
isPlus_in_ggg(pred(X), pred(Y), pred(pred(Z))) → U30_ggg(X, Y, Z, isPlus_in_ggg(X, Y, Z))
U30_ggg(X, Y, Z, isPlus_out_ggg(X, Y, Z)) → isPlus_out_ggg(pred(X), pred(Y), pred(pred(Z)))
U29_ggg(X, Y, Z, isPlus_out_ggg(X, Y, Z)) → isPlus_out_ggg(pred(X), succ(Y), Z)
U28_ggg(X, Y, Z, isPlus_out_ggg(X, Y, Z)) → isPlus_out_ggg(succ(X), pred(Y), Z)
U27_ggg(X, Y, Z, isPlus_out_ggg(X, Y, Z)) → isPlus_out_ggg(succ(X), succ(Y), succ(succ(Z)))
U8_gga(H1, T1, H2, T2, Result, U, isPlus_out_ggg(Product, Newresult, U)) → U9_gga(H1, T1, H2, T2, Result, =_in_ag(Result, U))
U9_gga(H1, T1, H2, T2, Result, =_out_ag(Result, U)) → vmul_out_gga(.(H1, T1), .(H2, T2), Result)
U4_gga(V0, Rest, V1, Result, Others, vmul_out_gga(V0, V1, Result)) → multiply_out_gga(.(V0, Rest), V1, .(Result, Others))
U2_gga(V0, Rest, V1, Result, Others, multiply_out_gga(V1, V0, Result)) → mmultiply_out_gga(.(V0, Rest), V1, .(Result, Others))

↳ Prolog

  ↳ PredefinedPredicateTransformerProof

    ↳ Prolog

      ↳ PrologToPiTRSProof

        ↳ PiTRS

          ↳ DependencyPairsProof

            ↳ PiDP

              ↳ DependencyGraphProof

                ↳ AND

                  ↳ PiDP

                  ↳ PiDP

                  ↳ PiDP

                  ↳ PiDP

                  ↳ PiDP

                  ↳ PiDP

                  ↳ PiDP

                  ↳ PiDP

                    ↳ UsableRulesProof

                      ↳ PiDP

                        ↳ PiDPToQDPProof

                  ↳ PiDP

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

MULTIPLY_IN_GGA(.(V0, Rest), V1, .(Result, Others)) → MULTIPLY_IN_GGA(Rest, V1, Others)

R is empty.
The argument filtering Pi contains the following mapping:
.(x1, x2) = .(x1, x2)
MULTIPLY_IN_GGA(x1, x2, x3) = MULTIPLY_IN_GGA(x1, x2)

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

↳ Prolog

  ↳ PredefinedPredicateTransformerProof

    ↳ Prolog

      ↳ PrologToPiTRSProof

        ↳ PiTRS

          ↳ DependencyPairsProof

            ↳ PiDP

              ↳ DependencyGraphProof

                ↳ AND

                  ↳ PiDP

                  ↳ PiDP

                  ↳ PiDP

                  ↳ PiDP

                  ↳ PiDP

                  ↳ PiDP

                  ↳ PiDP

                  ↳ PiDP

                    ↳ UsableRulesProof

                      ↳ PiDP

                        ↳ PiDPToQDPProof

                          ↳ QDP

                            ↳ QDPSizeChangeProof

                  ↳ PiDP

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

MULTIPLY_IN_GGA(.(V0, Rest), V1) → MULTIPLY_IN_GGA(Rest, V1)

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

MULTIPLY_IN_GGA(.(V0, Rest), V1) → MULTIPLY_IN_GGA(Rest, V1)
The graph contains the following edges 1 > 1, 2 >= 2

↳ Prolog

  ↳ PredefinedPredicateTransformerProof

    ↳ Prolog

      ↳ PrologToPiTRSProof

        ↳ PiTRS

          ↳ DependencyPairsProof

            ↳ PiDP

              ↳ DependencyGraphProof

                ↳ AND

                  ↳ PiDP

                  ↳ PiDP

                  ↳ PiDP

                  ↳ PiDP

                  ↳ PiDP

                  ↳ PiDP

                  ↳ PiDP

                  ↳ PiDP

                  ↳ PiDP

                    ↳ UsableRulesProof

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

MMULTIPLY_IN_GGA(.(V0, Rest), V1, .(Result, Others)) → MMULTIPLY_IN_GGA(Rest, V1, Others)

The TRS R consists of the following rules:

mmultiply_in_gga([], X, []) → mmultiply_out_gga([], X, [])
mmultiply_in_gga(.(V0, Rest), V1, .(Result, Others)) → U1_gga(V0, Rest, V1, Result, Others, mmultiply_in_gga(Rest, V1, Others))
U1_gga(V0, Rest, V1, Result, Others, mmultiply_out_gga(Rest, V1, Others)) → U2_gga(V0, Rest, V1, Result, Others, multiply_in_gga(V1, V0, Result))
multiply_in_gga([], X, []) → multiply_out_gga([], X, [])
multiply_in_gga(.(V0, Rest), V1, .(Result, Others)) → U3_gga(V0, Rest, V1, Result, Others, multiply_in_gga(Rest, V1, Others))
U3_gga(V0, Rest, V1, Result, Others, multiply_out_gga(Rest, V1, Others)) → U4_gga(V0, Rest, V1, Result, Others, vmul_in_gga(V0, V1, Result))
vmul_in_gga([], [], zero) → vmul_out_gga([], [], zero)
vmul_in_gga(.(H1, T1), .(H2, T2), Result) → U5_gga(H1, T1, H2, T2, Result, vmul_in_gga(T1, T2, Newresult))
U5_gga(H1, T1, H2, T2, Result, vmul_out_gga(T1, T2, Newresult)) → U6_gga(H1, T1, H2, T2, Result, Newresult, isTimes_in_gga(H1, H2, U))
isTimes_in_gga(X, zero, zero) → isTimes_out_gga(X, zero, zero)
isTimes_in_gga(zero, succ(Y), zero) → isTimes_out_gga(zero, succ(Y), zero)
isTimes_in_gga(zero, pred(Y), zero) → isTimes_out_gga(zero, pred(Y), zero)
isTimes_in_gga(succ(X), succ(Y), Z) → U37_gga(X, Y, Z, isTimes_in_gga(succ(X), Y, A))
isTimes_in_gga(succ(X), pred(Y), Z) → U39_gga(X, Y, Z, isTimes_in_gga(succ(X), Y, A))
isTimes_in_gga(pred(X), succ(Y), Z) → U41_gga(X, Y, Z, isTimes_in_gga(pred(X), Y, A))
isTimes_in_gga(pred(X), pred(Y), Z) → U43_gga(X, Y, Z, isTimes_in_gga(pred(X), Y, A))
U43_gga(X, Y, Z, isTimes_out_gga(pred(X), Y, A)) → U44_gga(X, Y, Z, isMinus_in_gga(A, pred(X), Z))
isMinus_in_gga(X, zero, X) → isMinus_out_gga(X, zero, X)
isMinus_in_gga(zero, succ(Y), pred(Z)) → U31_gga(Y, Z, isMinus_in_gga(zero, Y, Z))
isMinus_in_gga(zero, pred(Y), succ(Z)) → U32_gga(Y, Z, isMinus_in_gga(zero, Y, Z))
isMinus_in_gga(succ(X), succ(Y), Z) → U33_gga(X, Y, Z, isMinus_in_gga(X, Y, Z))
isMinus_in_gga(succ(X), pred(Y), succ(succ(Z))) → U34_gga(X, Y, Z, isMinus_in_gga(X, Y, Z))
isMinus_in_gga(pred(X), succ(Y), pred(pred(Z))) → U35_gga(X, Y, Z, isMinus_in_gga(X, Y, Z))
isMinus_in_gga(pred(X), pred(Y), Z) → U36_gga(X, Y, Z, isMinus_in_gga(X, Y, Z))
U36_gga(X, Y, Z, isMinus_out_gga(X, Y, Z)) → isMinus_out_gga(pred(X), pred(Y), Z)
U35_gga(X, Y, Z, isMinus_out_gga(X, Y, Z)) → isMinus_out_gga(pred(X), succ(Y), pred(pred(Z)))
U34_gga(X, Y, Z, isMinus_out_gga(X, Y, Z)) → isMinus_out_gga(succ(X), pred(Y), succ(succ(Z)))
U33_gga(X, Y, Z, isMinus_out_gga(X, Y, Z)) → isMinus_out_gga(succ(X), succ(Y), Z)
U32_gga(Y, Z, isMinus_out_gga(zero, Y, Z)) → isMinus_out_gga(zero, pred(Y), succ(Z))
U31_gga(Y, Z, isMinus_out_gga(zero, Y, Z)) → isMinus_out_gga(zero, succ(Y), pred(Z))
U44_gga(X, Y, Z, isMinus_out_gga(A, pred(X), Z)) → isTimes_out_gga(pred(X), pred(Y), Z)
U41_gga(X, Y, Z, isTimes_out_gga(pred(X), Y, A)) → U42_gga(X, Y, Z, isPlus_in_gga(A, pred(X), Z))
isPlus_in_gga(zero, X, X) → isPlus_out_gga(zero, X, X)
isPlus_in_gga(succ(X), zero, succ(X)) → isPlus_out_gga(succ(X), zero, succ(X))
isPlus_in_gga(succ(X), succ(Y), succ(succ(Z))) → U27_gga(X, Y, Z, isPlus_in_gga(X, Y, Z))
isPlus_in_gga(succ(X), pred(Y), Z) → U28_gga(X, Y, Z, isPlus_in_gga(X, Y, Z))
isPlus_in_gga(pred(X), zero, pred(X)) → isPlus_out_gga(pred(X), zero, pred(X))
isPlus_in_gga(pred(X), succ(Y), Z) → U29_gga(X, Y, Z, isPlus_in_gga(X, Y, Z))
isPlus_in_gga(pred(X), pred(Y), pred(pred(Z))) → U30_gga(X, Y, Z, isPlus_in_gga(X, Y, Z))
U30_gga(X, Y, Z, isPlus_out_gga(X, Y, Z)) → isPlus_out_gga(pred(X), pred(Y), pred(pred(Z)))
U29_gga(X, Y, Z, isPlus_out_gga(X, Y, Z)) → isPlus_out_gga(pred(X), succ(Y), Z)
U28_gga(X, Y, Z, isPlus_out_gga(X, Y, Z)) → isPlus_out_gga(succ(X), pred(Y), Z)
U27_gga(X, Y, Z, isPlus_out_gga(X, Y, Z)) → isPlus_out_gga(succ(X), succ(Y), succ(succ(Z)))
U42_gga(X, Y, Z, isPlus_out_gga(A, pred(X), Z)) → isTimes_out_gga(pred(X), succ(Y), Z)
U39_gga(X, Y, Z, isTimes_out_gga(succ(X), Y, A)) → U40_gga(X, Y, Z, isMinus_in_gga(A, succ(X), Z))
U40_gga(X, Y, Z, isMinus_out_gga(A, succ(X), Z)) → isTimes_out_gga(succ(X), pred(Y), Z)
U37_gga(X, Y, Z, isTimes_out_gga(succ(X), Y, A)) → U38_gga(X, Y, Z, isPlus_in_gga(A, succ(X), Z))
U38_gga(X, Y, Z, isPlus_out_gga(A, succ(X), Z)) → isTimes_out_gga(succ(X), succ(Y), Z)
U6_gga(H1, T1, H2, T2, Result, Newresult, isTimes_out_gga(H1, H2, U)) → U7_gga(H1, T1, H2, T2, Result, Newresult, U, =_in_ag(Product, U))
=_in_ag(X, X) → =_out_ag(X, X)
U7_gga(H1, T1, H2, T2, Result, Newresult, U, =_out_ag(Product, U)) → U8_gga(H1, T1, H2, T2, Result, U, isPlus_in_ggg(Product, Newresult, U))
isPlus_in_ggg(zero, X, X) → isPlus_out_ggg(zero, X, X)
isPlus_in_ggg(succ(X), zero, succ(X)) → isPlus_out_ggg(succ(X), zero, succ(X))
isPlus_in_ggg(succ(X), succ(Y), succ(succ(Z))) → U27_ggg(X, Y, Z, isPlus_in_ggg(X, Y, Z))
isPlus_in_ggg(succ(X), pred(Y), Z) → U28_ggg(X, Y, Z, isPlus_in_ggg(X, Y, Z))
isPlus_in_ggg(pred(X), zero, pred(X)) → isPlus_out_ggg(pred(X), zero, pred(X))
isPlus_in_ggg(pred(X), succ(Y), Z) → U29_ggg(X, Y, Z, isPlus_in_ggg(X, Y, Z))
isPlus_in_ggg(pred(X), pred(Y), pred(pred(Z))) → U30_ggg(X, Y, Z, isPlus_in_ggg(X, Y, Z))
U30_ggg(X, Y, Z, isPlus_out_ggg(X, Y, Z)) → isPlus_out_ggg(pred(X), pred(Y), pred(pred(Z)))
U29_ggg(X, Y, Z, isPlus_out_ggg(X, Y, Z)) → isPlus_out_ggg(pred(X), succ(Y), Z)
U28_ggg(X, Y, Z, isPlus_out_ggg(X, Y, Z)) → isPlus_out_ggg(succ(X), pred(Y), Z)
U27_ggg(X, Y, Z, isPlus_out_ggg(X, Y, Z)) → isPlus_out_ggg(succ(X), succ(Y), succ(succ(Z)))
U8_gga(H1, T1, H2, T2, Result, U, isPlus_out_ggg(Product, Newresult, U)) → U9_gga(H1, T1, H2, T2, Result, =_in_ag(Result, U))
U9_gga(H1, T1, H2, T2, Result, =_out_ag(Result, U)) → vmul_out_gga(.(H1, T1), .(H2, T2), Result)
U4_gga(V0, Rest, V1, Result, Others, vmul_out_gga(V0, V1, Result)) → multiply_out_gga(.(V0, Rest), V1, .(Result, Others))
U2_gga(V0, Rest, V1, Result, Others, multiply_out_gga(V1, V0, Result)) → mmultiply_out_gga(.(V0, Rest), V1, .(Result, Others))

↳ Prolog

  ↳ PredefinedPredicateTransformerProof

    ↳ Prolog

      ↳ PrologToPiTRSProof

        ↳ PiTRS

          ↳ DependencyPairsProof

            ↳ PiDP

              ↳ DependencyGraphProof

                ↳ AND

                  ↳ PiDP

                  ↳ PiDP

                  ↳ PiDP

                  ↳ PiDP

                  ↳ PiDP

                  ↳ PiDP

                  ↳ PiDP

                  ↳ PiDP

                  ↳ PiDP

                    ↳ UsableRulesProof

                      ↳ PiDP

                        ↳ PiDPToQDPProof

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

MMULTIPLY_IN_GGA(.(V0, Rest), V1, .(Result, Others)) → MMULTIPLY_IN_GGA(Rest, V1, Others)

R is empty.
The argument filtering Pi contains the following mapping:
.(x1, x2) = .(x1, x2)
MMULTIPLY_IN_GGA(x1, x2, x3) = MMULTIPLY_IN_GGA(x1, x2)

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

↳ Prolog

  ↳ PredefinedPredicateTransformerProof

    ↳ Prolog

      ↳ PrologToPiTRSProof

        ↳ PiTRS

          ↳ DependencyPairsProof

            ↳ PiDP

              ↳ DependencyGraphProof

                ↳ AND

                  ↳ PiDP

                  ↳ PiDP

                  ↳ PiDP

                  ↳ PiDP

                  ↳ PiDP

                  ↳ PiDP

                  ↳ PiDP

                  ↳ PiDP

                  ↳ PiDP

                    ↳ UsableRulesProof

                      ↳ PiDP

                        ↳ PiDPToQDPProof

                          ↳ QDP

                            ↳ QDPSizeChangeProof

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

MMULTIPLY_IN_GGA(.(V0, Rest), V1) → MMULTIPLY_IN_GGA(Rest, V1)

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

MMULTIPLY_IN_GGA(.(V0, Rest), V1) → MMULTIPLY_IN_GGA(Rest, V1)
The graph contains the following edges 1 > 1, 2 >= 2