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



↳ Prolog
  ↳ PredefinedPredicateTransformerProof

Clauses:

demo :- ','(nl, ','(write('Cryptarithmetic puzzle'), ','(nl, ','(nl, ','(write(' SEND'), ','(nl, ','(write(' + MORE'), ','(nl, ','(write(' --------'), ','(nl, ','(write(' MONEY'), ','(nl, ','(nl, ','(nl, ','(time(_), ','(money(S, E, N, D, M, O, R, Y), ','(time(T), ','(write('The solution is:'), ','(nl, ','(nl, ','(write(' '), ','(write(S), ','(write(E), ','(write(N), ','(write(D), ','(nl, ','(write(' + '), ','(write(M), ','(write(O), ','(write(R), ','(write(E), ','(nl, ','(write(' --------'), ','(nl, ','(write(' '), ','(write(M), ','(write(O), ','(write(N), ','(write(E), ','(write(Y), ','(nl, ','(nl, ','(write('Solved in '), ','(write(T), ','(write(' msec.'), nl))))))))))))))))))))))))))))))))))))))))))))).
time(0).
solve(.(S, .(E, .(N, .(D, .(M, .(O, .(R, .(Y, []))))))))) :- money(S, E, N, D, M, O, R, Y).
money(S, E, N, D, M, O, R, Y) :- ','(carry(C1), ','(carry(C2), ','(carry(C3), ','(carry(C4), ','(=(C4, M), ','(=\=(M, 0), ','(domain(.(S, .(E, .(N, .(D, .(M, .(O, .(R, .(Y, [])))))))), .(0, .(1, .(2, .(3, .(4, .(5, .(6, .(7, .(8, .(9, []))))))))))), ','(=\=(S, 0), ','(calc(C3, S, M, C4, O), ','(calc(C2, E, O, C3, N), ','(calc(C1, N, R, C2, E), calc(0, D, E, C1, Y)))))))))))).
calc(C0, D, E, C1, Y) :- ','(sum(C0, D, CD), ','(sum(CD, E, S), ','(carry10(C1, C10), sum(C10, Y, S)))).
sum(X, Y, Z) :- is(Z, +(X, Y)).
domain([], _).
domain(.(X1, R), L) :- ','(del(X1, L, NL), domain(R, NL)).
del(X, .(X, T), T).
del(X, .(Y, T), .(Y, NT)) :- del(X, T, NT).
carry(1).
carry(0).
carry10(0, 0).
carry10(1, 10).

Queries:

money(a,a,a,a,a,a,a,a).

Added definitions of predefined predicates.

↳ Prolog
  ↳ PredefinedPredicateTransformerProof
    ↳ Prolog
      ↳ CutEliminatorProof

Clauses:

demo :- ','(nl, ','(write('Cryptarithmetic puzzle'), ','(nl, ','(nl, ','(write(' SEND'), ','(nl, ','(write(' + MORE'), ','(nl, ','(write(' --------'), ','(nl, ','(write(' MONEY'), ','(nl, ','(nl, ','(nl, ','(time(_), ','(money(S, E, N, D, M, O, R, Y), ','(time(T), ','(write('The solution is:'), ','(nl, ','(nl, ','(write(' '), ','(write(S), ','(write(E), ','(write(N), ','(write(D), ','(nl, ','(write(' + '), ','(write(M), ','(write(O), ','(write(R), ','(write(E), ','(nl, ','(write(' --------'), ','(nl, ','(write(' '), ','(write(M), ','(write(O), ','(write(N), ','(write(E), ','(write(Y), ','(nl, ','(nl, ','(write('Solved in '), ','(write(T), ','(write(' msec.'), nl))))))))))))))))))))))))))))))))))))))))))))).
time(zero).
solve(.(S, .(E, .(N, .(D, .(M, .(O, .(R, .(Y, []))))))))) :- money(S, E, N, D, M, O, R, Y).
money(S, E, N, D, M, O, R, Y) :- ','(carry(C1), ','(carry(C2), ','(carry(C3), ','(carry(C4), ','(=(C4, M), ','(=\=(M, zero), ','(domain(.(S, .(E, .(N, .(D, .(M, .(O, .(R, .(Y, [])))))))), .(zero, .(succ(zero), .(succ(succ(zero)), .(succ(succ(succ(zero))), .(succ(succ(succ(succ(zero)))), .(succ(succ(succ(succ(succ(zero))))), .(succ(succ(succ(succ(succ(succ(zero)))))), .(succ(succ(succ(succ(succ(succ(succ(zero))))))), .(succ(succ(succ(succ(succ(succ(succ(succ(zero)))))))), .(succ(succ(succ(succ(succ(succ(succ(succ(succ(zero))))))))), []))))))))))), ','(=\=(S, zero), ','(calc(C3, S, M, C4, O), ','(calc(C2, E, O, C3, N), ','(calc(C1, N, R, C2, E), calc(zero, D, E, C1, Y)))))))))))).
calc(C0, D, E, C1, Y) :- ','(sum(C0, D, CD), ','(sum(CD, E, S), ','(carry10(C1, C10), sum(C10, Y, S)))).
sum(X, Y, Z) :- ','(isPlus(X, Y, U), =(Z, U)).
domain([], _).
domain(.(X1, R), L) :- ','(del(X1, L, NL), domain(R, NL)).
del(X, .(X, T), T).
del(X, .(Y, T), .(Y, NT)) :- del(X, T, NT).
carry(succ(zero)).
carry(zero).
carry10(zero, zero).
carry10(succ(zero), succ(succ(succ(succ(succ(succ(succ(succ(succ(succ(zero))))))))))).
nonequal(X, Y) :- ','(=(X, Y), ','(!, fail)).
nonequal(X, Y) :- true.
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))).
fail :- fail(b).
fail(a).
true.
=(X, X).

Queries:

money(a,a,a,a,a,a,a,a).

Eliminated all cuts by simply ignoring them.

↳ Prolog
  ↳ PredefinedPredicateTransformerProof
    ↳ Prolog
      ↳ CutEliminatorProof
        ↳ Prolog
          ↳ UndefinedPredicateHandlerProof

Clauses:

demo :- ','(nl, ','(write('Cryptarithmetic puzzle'), ','(nl, ','(nl, ','(write(' SEND'), ','(nl, ','(write(' + MORE'), ','(nl, ','(write(' --------'), ','(nl, ','(write(' MONEY'), ','(nl, ','(nl, ','(nl, ','(time(_), ','(money(S, E, N, D, M, O, R, Y), ','(time(T), ','(write('The solution is:'), ','(nl, ','(nl, ','(write(' '), ','(write(S), ','(write(E), ','(write(N), ','(write(D), ','(nl, ','(write(' + '), ','(write(M), ','(write(O), ','(write(R), ','(write(E), ','(nl, ','(write(' --------'), ','(nl, ','(write(' '), ','(write(M), ','(write(O), ','(write(N), ','(write(E), ','(write(Y), ','(nl, ','(nl, ','(write('Solved in '), ','(write(T), ','(write(' msec.'), nl))))))))))))))))))))))))))))))))))))))))))))).
time(zero).
solve(.(S, .(E, .(N, .(D, .(M, .(O, .(R, .(Y, []))))))))) :- money(S, E, N, D, M, O, R, Y).
money(S, E, N, D, M, O, R, Y) :- ','(carry(C1), ','(carry(C2), ','(carry(C3), ','(carry(C4), ','(=(C4, M), ','(=\=(M, zero), ','(domain(.(S, .(E, .(N, .(D, .(M, .(O, .(R, .(Y, [])))))))), .(zero, .(succ(zero), .(succ(succ(zero)), .(succ(succ(succ(zero))), .(succ(succ(succ(succ(zero)))), .(succ(succ(succ(succ(succ(zero))))), .(succ(succ(succ(succ(succ(succ(zero)))))), .(succ(succ(succ(succ(succ(succ(succ(zero))))))), .(succ(succ(succ(succ(succ(succ(succ(succ(zero)))))))), .(succ(succ(succ(succ(succ(succ(succ(succ(succ(zero))))))))), []))))))))))), ','(=\=(S, zero), ','(calc(C3, S, M, C4, O), ','(calc(C2, E, O, C3, N), ','(calc(C1, N, R, C2, E), calc(zero, D, E, C1, Y)))))))))))).
calc(C0, D, E, C1, Y) :- ','(sum(C0, D, CD), ','(sum(CD, E, S), ','(carry10(C1, C10), sum(C10, Y, S)))).
sum(X, Y, Z) :- ','(isPlus(X, Y, U), =(Z, U)).
domain([], _).
domain(.(X1, R), L) :- ','(del(X1, L, NL), domain(R, NL)).
del(X, .(X, T), T).
del(X, .(Y, T), .(Y, NT)) :- del(X, T, NT).
carry(succ(zero)).
carry(zero).
carry10(zero, zero).
carry10(succ(zero), succ(succ(succ(succ(succ(succ(succ(succ(succ(succ(zero))))))))))).
nonequal(X, Y) :- ','(=(X, Y), fail).
nonequal(X, Y) :- true.
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))).
fail :- fail(b).
fail(a).
true.
=(X, X).

Queries:

money(a,a,a,a,a,a,a,a).

Added facts for all undefined predicates.

↳ Prolog
  ↳ PredefinedPredicateTransformerProof
    ↳ Prolog
      ↳ CutEliminatorProof
        ↳ Prolog
          ↳ UndefinedPredicateHandlerProof
            ↳ Prolog
              ↳ PrologToPiTRSProof

Clauses:

demo :- ','(nl, ','(write('Cryptarithmetic puzzle'), ','(nl, ','(nl, ','(write(' SEND'), ','(nl, ','(write(' + MORE'), ','(nl, ','(write(' --------'), ','(nl, ','(write(' MONEY'), ','(nl, ','(nl, ','(nl, ','(time(X), ','(money(S, E, N, D, M, O, R, Y), ','(time(T), ','(write('The solution is:'), ','(nl, ','(nl, ','(write(' '), ','(write(S), ','(write(E), ','(write(N), ','(write(D), ','(nl, ','(write(' + '), ','(write(M), ','(write(O), ','(write(R), ','(write(E), ','(nl, ','(write(' --------'), ','(nl, ','(write(' '), ','(write(M), ','(write(O), ','(write(N), ','(write(E), ','(write(Y), ','(nl, ','(nl, ','(write('Solved in '), ','(write(T), ','(write(' msec.'), nl))))))))))))))))))))))))))))))))))))))))))))).
time(zero).
solve(.(S, .(E, .(N, .(D, .(M, .(O, .(R, .(Y, []))))))))) :- money(S, E, N, D, M, O, R, Y).
money(S, E, N, D, M, O, R, Y) :- ','(carry(C1), ','(carry(C2), ','(carry(C3), ','(carry(C4), ','(=(C4, M), ','(=\=(M, zero), ','(domain(.(S, .(E, .(N, .(D, .(M, .(O, .(R, .(Y, [])))))))), .(zero, .(succ(zero), .(succ(succ(zero)), .(succ(succ(succ(zero))), .(succ(succ(succ(succ(zero)))), .(succ(succ(succ(succ(succ(zero))))), .(succ(succ(succ(succ(succ(succ(zero)))))), .(succ(succ(succ(succ(succ(succ(succ(zero))))))), .(succ(succ(succ(succ(succ(succ(succ(succ(zero)))))))), .(succ(succ(succ(succ(succ(succ(succ(succ(succ(zero))))))))), []))))))))))), ','(=\=(S, zero), ','(calc(C3, S, M, C4, O), ','(calc(C2, E, O, C3, N), ','(calc(C1, N, R, C2, E), calc(zero, D, E, C1, Y)))))))))))).
calc(C0, D, E, C1, Y) :- ','(sum(C0, D, CD), ','(sum(CD, E, S), ','(carry10(C1, C10), sum(C10, Y, S)))).
sum(X, Y, Z) :- ','(isPlus(X, Y, U), =(Z, U)).
domain([], X).
domain(.(X1, R), L) :- ','(del(X1, L, NL), domain(R, NL)).
del(X, .(X, T), T).
del(X, .(Y, T), .(Y, NT)) :- del(X, T, NT).
carry(succ(zero)).
carry(zero).
carry10(zero, zero).
carry10(succ(zero), succ(succ(succ(succ(succ(succ(succ(succ(succ(succ(zero))))))))))).
nonequal(X, Y) :- ','(=(X, Y), fail).
nonequal(X, Y) :- true.
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))).
fail :- fail(b).
fail(a).
true.
=(X, X).
nl.
write(X0).
=\=(X0, X1).

Queries:

money(a,a,a,a,a,a,a,a).

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

money_in_aaaaaaaa(S, E, N, D, M, O, R, Y) → U48_aaaaaaaa(S, E, N, D, M, O, R, Y, carry_in_a(C1))
carry_in_a(succ(zero)) → carry_out_a(succ(zero))
carry_in_a(zero) → carry_out_a(zero)
U48_aaaaaaaa(S, E, N, D, M, O, R, Y, carry_out_a(C1)) → U49_aaaaaaaa(S, E, N, D, M, O, R, Y, C1, carry_in_a(C2))
U49_aaaaaaaa(S, E, N, D, M, O, R, Y, C1, carry_out_a(C2)) → U50_aaaaaaaa(S, E, N, D, M, O, R, Y, C1, C2, carry_in_a(C3))
U50_aaaaaaaa(S, E, N, D, M, O, R, Y, C1, C2, carry_out_a(C3)) → U51_aaaaaaaa(S, E, N, D, M, O, R, Y, C1, C2, C3, carry_in_a(C4))
U51_aaaaaaaa(S, E, N, D, M, O, R, Y, C1, C2, C3, carry_out_a(C4)) → U52_aaaaaaaa(S, E, N, D, M, O, R, Y, C1, C2, C3, C4, =_in_ga(C4, M))
=_in_ga(X, X) → =_out_ga(X, X)
U52_aaaaaaaa(S, E, N, D, M, O, R, Y, C1, C2, C3, C4, =_out_ga(C4, M)) → U53_aaaaaaaa(S, E, N, D, M, O, R, Y, C1, C2, C3, C4, =\=_in_gg(M, zero))
=\=_in_gg(X0, X1) → =\=_out_gg(X0, X1)
U53_aaaaaaaa(S, E, N, D, M, O, R, Y, C1, C2, C3, C4, =\=_out_gg(M, zero)) → U54_aaaaaaaa(S, E, N, D, M, O, R, Y, C1, C2, C3, C4, domain_in_ag(.(S, .(E, .(N, .(D, .(M, .(O, .(R, .(Y, [])))))))), .(zero, .(succ(zero), .(succ(succ(zero)), .(succ(succ(succ(zero))), .(succ(succ(succ(succ(zero)))), .(succ(succ(succ(succ(succ(zero))))), .(succ(succ(succ(succ(succ(succ(zero)))))), .(succ(succ(succ(succ(succ(succ(succ(zero))))))), .(succ(succ(succ(succ(succ(succ(succ(succ(zero)))))))), .(succ(succ(succ(succ(succ(succ(succ(succ(succ(zero))))))))), []))))))))))))
domain_in_ag([], X) → domain_out_ag([], X)
domain_in_ag(.(X1, R), L) → U66_ag(X1, R, L, del_in_aga(X1, L, NL))
del_in_aga(X, .(X, T), T) → del_out_aga(X, .(X, T), T)
del_in_aga(X, .(Y, T), .(Y, NT)) → U68_aga(X, Y, T, NT, del_in_aga(X, T, NT))
U68_aga(X, Y, T, NT, del_out_aga(X, T, NT)) → del_out_aga(X, .(Y, T), .(Y, NT))
U66_ag(X1, R, L, del_out_aga(X1, L, NL)) → U67_ag(X1, R, L, domain_in_ag(R, NL))
U67_ag(X1, R, L, domain_out_ag(R, NL)) → domain_out_ag(.(X1, R), L)
U54_aaaaaaaa(S, E, N, D, M, O, R, Y, C1, C2, C3, C4, domain_out_ag(.(S, .(E, .(N, .(D, .(M, .(O, .(R, .(Y, [])))))))), .(zero, .(succ(zero), .(succ(succ(zero)), .(succ(succ(succ(zero))), .(succ(succ(succ(succ(zero)))), .(succ(succ(succ(succ(succ(zero))))), .(succ(succ(succ(succ(succ(succ(zero)))))), .(succ(succ(succ(succ(succ(succ(succ(zero))))))), .(succ(succ(succ(succ(succ(succ(succ(succ(zero)))))))), .(succ(succ(succ(succ(succ(succ(succ(succ(succ(zero))))))))), [])))))))))))) → U55_aaaaaaaa(S, E, N, D, M, O, R, Y, C1, C2, C3, C4, =\=_in_gg(S, zero))
U55_aaaaaaaa(S, E, N, D, M, O, R, Y, C1, C2, C3, C4, =\=_out_gg(S, zero)) → U56_aaaaaaaa(S, E, N, D, M, O, R, Y, C1, C2, C3, calc_in_ggggg(C3, S, M, C4, O))
calc_in_ggggg(C0, D, E, C1, Y) → U60_ggggg(C0, D, E, C1, Y, sum_in_gga(C0, D, CD))
sum_in_gga(X, Y, Z) → U64_gga(X, Y, Z, isPlus_in_gga(X, Y, U))
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))) → U72_gga(X, Y, Z, isPlus_in_gga(X, Y, Z))
isPlus_in_gga(succ(X), pred(Y), Z) → U73_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) → U74_gga(X, Y, Z, isPlus_in_gga(X, Y, Z))
isPlus_in_gga(pred(X), pred(Y), pred(pred(Z))) → U75_gga(X, Y, Z, isPlus_in_gga(X, Y, Z))
U75_gga(X, Y, Z, isPlus_out_gga(X, Y, Z)) → isPlus_out_gga(pred(X), pred(Y), pred(pred(Z)))
U74_gga(X, Y, Z, isPlus_out_gga(X, Y, Z)) → isPlus_out_gga(pred(X), succ(Y), Z)
U73_gga(X, Y, Z, isPlus_out_gga(X, Y, Z)) → isPlus_out_gga(succ(X), pred(Y), Z)
U72_gga(X, Y, Z, isPlus_out_gga(X, Y, Z)) → isPlus_out_gga(succ(X), succ(Y), succ(succ(Z)))
U64_gga(X, Y, Z, isPlus_out_gga(X, Y, U)) → U65_gga(X, Y, Z, =_in_ag(Z, U))
=_in_ag(X, X) → =_out_ag(X, X)
U65_gga(X, Y, Z, =_out_ag(Z, U)) → sum_out_gga(X, Y, Z)
U60_ggggg(C0, D, E, C1, Y, sum_out_gga(C0, D, CD)) → U61_ggggg(C0, D, E, C1, Y, sum_in_gga(CD, E, S))
U61_ggggg(C0, D, E, C1, Y, sum_out_gga(CD, E, S)) → U62_ggggg(C0, D, E, C1, Y, S, carry10_in_ga(C1, C10))
carry10_in_ga(zero, zero) → carry10_out_ga(zero, zero)
carry10_in_ga(succ(zero), succ(succ(succ(succ(succ(succ(succ(succ(succ(succ(zero))))))))))) → carry10_out_ga(succ(zero), succ(succ(succ(succ(succ(succ(succ(succ(succ(succ(zero)))))))))))
U62_ggggg(C0, D, E, C1, Y, S, carry10_out_ga(C1, C10)) → U63_ggggg(C0, D, E, C1, Y, sum_in_ggg(C10, Y, S))
sum_in_ggg(X, Y, Z) → U64_ggg(X, Y, Z, isPlus_in_gga(X, Y, U))
U64_ggg(X, Y, Z, isPlus_out_gga(X, Y, U)) → U65_ggg(X, Y, Z, =_in_gg(Z, U))
=_in_gg(X, X) → =_out_gg(X, X)
U65_ggg(X, Y, Z, =_out_gg(Z, U)) → sum_out_ggg(X, Y, Z)
U63_ggggg(C0, D, E, C1, Y, sum_out_ggg(C10, Y, S)) → calc_out_ggggg(C0, D, E, C1, Y)
U56_aaaaaaaa(S, E, N, D, M, O, R, Y, C1, C2, C3, calc_out_ggggg(C3, S, M, C4, O)) → U57_aaaaaaaa(S, E, N, D, M, O, R, Y, C1, C2, calc_in_ggggg(C2, E, O, C3, N))
U57_aaaaaaaa(S, E, N, D, M, O, R, Y, C1, C2, calc_out_ggggg(C2, E, O, C3, N)) → U58_aaaaaaaa(S, E, N, D, M, O, R, Y, C1, calc_in_ggggg(C1, N, R, C2, E))
U58_aaaaaaaa(S, E, N, D, M, O, R, Y, C1, calc_out_ggggg(C1, N, R, C2, E)) → U59_aaaaaaaa(S, E, N, D, M, O, R, Y, calc_in_ggggg(zero, D, E, C1, Y))
U59_aaaaaaaa(S, E, N, D, M, O, R, Y, calc_out_ggggg(zero, D, E, C1, Y)) → money_out_aaaaaaaa(S, E, N, D, M, O, R, Y)

The argument filtering Pi contains the following mapping:
money_in_aaaaaaaa(x1, x2, x3, x4, x5, x6, x7, x8)  =  money_in_aaaaaaaa
U48_aaaaaaaa(x1, x2, x3, x4, x5, x6, x7, x8, x9)  =  U48_aaaaaaaa(x9)
carry_in_a(x1)  =  carry_in_a
carry_out_a(x1)  =  carry_out_a(x1)
U49_aaaaaaaa(x1, x2, x3, x4, x5, x6, x7, x8, x9, x10)  =  U49_aaaaaaaa(x9, x10)
U50_aaaaaaaa(x1, x2, x3, x4, x5, x6, x7, x8, x9, x10, x11)  =  U50_aaaaaaaa(x9, x10, x11)
U51_aaaaaaaa(x1, x2, x3, x4, x5, x6, x7, x8, x9, x10, x11, x12)  =  U51_aaaaaaaa(x9, x10, x11, x12)
U52_aaaaaaaa(x1, x2, x3, x4, x5, x6, x7, x8, x9, x10, x11, x12, x13)  =  U52_aaaaaaaa(x9, x10, x11, x12, x13)
=_in_ga(x1, x2)  =  =_in_ga(x1)
=_out_ga(x1, x2)  =  =_out_ga(x2)
U53_aaaaaaaa(x1, x2, x3, x4, x5, x6, x7, x8, x9, x10, x11, x12, x13)  =  U53_aaaaaaaa(x5, x9, x10, x11, x12, x13)
=\=_in_gg(x1, x2)  =  =\=_in_gg(x1, x2)
=\=_out_gg(x1, x2)  =  =\=_out_gg
zero  =  zero
U54_aaaaaaaa(x1, x2, x3, x4, x5, x6, x7, x8, x9, x10, x11, x12, x13)  =  U54_aaaaaaaa(x5, x9, x10, x11, x12, x13)
domain_in_ag(x1, x2)  =  domain_in_ag(x2)
domain_out_ag(x1, x2)  =  domain_out_ag(x1)
U66_ag(x1, x2, x3, x4)  =  U66_ag(x4)
del_in_aga(x1, x2, x3)  =  del_in_aga(x2)
.(x1, x2)  =  .(x1, x2)
del_out_aga(x1, x2, x3)  =  del_out_aga(x1, x3)
U68_aga(x1, x2, x3, x4, x5)  =  U68_aga(x2, x5)
U67_ag(x1, x2, x3, x4)  =  U67_ag(x1, x4)
[]  =  []
succ(x1)  =  succ(x1)
U55_aaaaaaaa(x1, x2, x3, x4, x5, x6, x7, x8, x9, x10, x11, x12, x13)  =  U55_aaaaaaaa(x1, x2, x3, x4, x5, x6, x7, x8, x9, x10, x11, x12, x13)
U56_aaaaaaaa(x1, x2, x3, x4, x5, x6, x7, x8, x9, x10, x11, x12)  =  U56_aaaaaaaa(x1, x2, x3, x4, x5, x6, x7, x8, x9, x10, x11, x12)
calc_in_ggggg(x1, x2, x3, x4, x5)  =  calc_in_ggggg(x1, x2, x3, x4, x5)
U60_ggggg(x1, x2, x3, x4, x5, x6)  =  U60_ggggg(x3, x4, x5, x6)
sum_in_gga(x1, x2, x3)  =  sum_in_gga(x1, x2)
U64_gga(x1, x2, x3, x4)  =  U64_gga(x4)
isPlus_in_gga(x1, x2, x3)  =  isPlus_in_gga(x1, x2)
isPlus_out_gga(x1, x2, x3)  =  isPlus_out_gga(x3)
U72_gga(x1, x2, x3, x4)  =  U72_gga(x4)
pred(x1)  =  pred(x1)
U73_gga(x1, x2, x3, x4)  =  U73_gga(x4)
U74_gga(x1, x2, x3, x4)  =  U74_gga(x4)
U75_gga(x1, x2, x3, x4)  =  U75_gga(x4)
U65_gga(x1, x2, x3, x4)  =  U65_gga(x4)
=_in_ag(x1, x2)  =  =_in_ag(x2)
=_out_ag(x1, x2)  =  =_out_ag(x1)
sum_out_gga(x1, x2, x3)  =  sum_out_gga(x3)
U61_ggggg(x1, x2, x3, x4, x5, x6)  =  U61_ggggg(x4, x5, x6)
U62_ggggg(x1, x2, x3, x4, x5, x6, x7)  =  U62_ggggg(x5, x6, x7)
carry10_in_ga(x1, x2)  =  carry10_in_ga(x1)
carry10_out_ga(x1, x2)  =  carry10_out_ga(x2)
U63_ggggg(x1, x2, x3, x4, x5, x6)  =  U63_ggggg(x6)
sum_in_ggg(x1, x2, x3)  =  sum_in_ggg(x1, x2, x3)
U64_ggg(x1, x2, x3, x4)  =  U64_ggg(x3, x4)
U65_ggg(x1, x2, x3, x4)  =  U65_ggg(x4)
=_in_gg(x1, x2)  =  =_in_gg(x1, x2)
=_out_gg(x1, x2)  =  =_out_gg
sum_out_ggg(x1, x2, x3)  =  sum_out_ggg
calc_out_ggggg(x1, x2, x3, x4, x5)  =  calc_out_ggggg
U57_aaaaaaaa(x1, x2, x3, x4, x5, x6, x7, x8, x9, x10, x11)  =  U57_aaaaaaaa(x1, x2, x3, x4, x5, x6, x7, x8, x9, x10, x11)
U58_aaaaaaaa(x1, x2, x3, x4, x5, x6, x7, x8, x9, x10)  =  U58_aaaaaaaa(x1, x2, x3, x4, x5, x6, x7, x8, x9, x10)
U59_aaaaaaaa(x1, x2, x3, x4, x5, x6, x7, x8, x9)  =  U59_aaaaaaaa(x1, x2, x3, x4, x5, x6, x7, x8, x9)
money_out_aaaaaaaa(x1, x2, x3, x4, x5, x6, x7, x8)  =  money_out_aaaaaaaa(x1, x2, x3, x4, x5, x6, x7, x8)

Infinitary Constructor Rewriting Termination of PiTRS implies Termination of Prolog



↳ Prolog
  ↳ PredefinedPredicateTransformerProof
    ↳ Prolog
      ↳ CutEliminatorProof
        ↳ Prolog
          ↳ UndefinedPredicateHandlerProof
            ↳ Prolog
              ↳ PrologToPiTRSProof
                ↳ PiTRS
                  ↳ DependencyPairsProof

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

money_in_aaaaaaaa(S, E, N, D, M, O, R, Y) → U48_aaaaaaaa(S, E, N, D, M, O, R, Y, carry_in_a(C1))
carry_in_a(succ(zero)) → carry_out_a(succ(zero))
carry_in_a(zero) → carry_out_a(zero)
U48_aaaaaaaa(S, E, N, D, M, O, R, Y, carry_out_a(C1)) → U49_aaaaaaaa(S, E, N, D, M, O, R, Y, C1, carry_in_a(C2))
U49_aaaaaaaa(S, E, N, D, M, O, R, Y, C1, carry_out_a(C2)) → U50_aaaaaaaa(S, E, N, D, M, O, R, Y, C1, C2, carry_in_a(C3))
U50_aaaaaaaa(S, E, N, D, M, O, R, Y, C1, C2, carry_out_a(C3)) → U51_aaaaaaaa(S, E, N, D, M, O, R, Y, C1, C2, C3, carry_in_a(C4))
U51_aaaaaaaa(S, E, N, D, M, O, R, Y, C1, C2, C3, carry_out_a(C4)) → U52_aaaaaaaa(S, E, N, D, M, O, R, Y, C1, C2, C3, C4, =_in_ga(C4, M))
=_in_ga(X, X) → =_out_ga(X, X)
U52_aaaaaaaa(S, E, N, D, M, O, R, Y, C1, C2, C3, C4, =_out_ga(C4, M)) → U53_aaaaaaaa(S, E, N, D, M, O, R, Y, C1, C2, C3, C4, =\=_in_gg(M, zero))
=\=_in_gg(X0, X1) → =\=_out_gg(X0, X1)
U53_aaaaaaaa(S, E, N, D, M, O, R, Y, C1, C2, C3, C4, =\=_out_gg(M, zero)) → U54_aaaaaaaa(S, E, N, D, M, O, R, Y, C1, C2, C3, C4, domain_in_ag(.(S, .(E, .(N, .(D, .(M, .(O, .(R, .(Y, [])))))))), .(zero, .(succ(zero), .(succ(succ(zero)), .(succ(succ(succ(zero))), .(succ(succ(succ(succ(zero)))), .(succ(succ(succ(succ(succ(zero))))), .(succ(succ(succ(succ(succ(succ(zero)))))), .(succ(succ(succ(succ(succ(succ(succ(zero))))))), .(succ(succ(succ(succ(succ(succ(succ(succ(zero)))))))), .(succ(succ(succ(succ(succ(succ(succ(succ(succ(zero))))))))), []))))))))))))
domain_in_ag([], X) → domain_out_ag([], X)
domain_in_ag(.(X1, R), L) → U66_ag(X1, R, L, del_in_aga(X1, L, NL))
del_in_aga(X, .(X, T), T) → del_out_aga(X, .(X, T), T)
del_in_aga(X, .(Y, T), .(Y, NT)) → U68_aga(X, Y, T, NT, del_in_aga(X, T, NT))
U68_aga(X, Y, T, NT, del_out_aga(X, T, NT)) → del_out_aga(X, .(Y, T), .(Y, NT))
U66_ag(X1, R, L, del_out_aga(X1, L, NL)) → U67_ag(X1, R, L, domain_in_ag(R, NL))
U67_ag(X1, R, L, domain_out_ag(R, NL)) → domain_out_ag(.(X1, R), L)
U54_aaaaaaaa(S, E, N, D, M, O, R, Y, C1, C2, C3, C4, domain_out_ag(.(S, .(E, .(N, .(D, .(M, .(O, .(R, .(Y, [])))))))), .(zero, .(succ(zero), .(succ(succ(zero)), .(succ(succ(succ(zero))), .(succ(succ(succ(succ(zero)))), .(succ(succ(succ(succ(succ(zero))))), .(succ(succ(succ(succ(succ(succ(zero)))))), .(succ(succ(succ(succ(succ(succ(succ(zero))))))), .(succ(succ(succ(succ(succ(succ(succ(succ(zero)))))))), .(succ(succ(succ(succ(succ(succ(succ(succ(succ(zero))))))))), [])))))))))))) → U55_aaaaaaaa(S, E, N, D, M, O, R, Y, C1, C2, C3, C4, =\=_in_gg(S, zero))
U55_aaaaaaaa(S, E, N, D, M, O, R, Y, C1, C2, C3, C4, =\=_out_gg(S, zero)) → U56_aaaaaaaa(S, E, N, D, M, O, R, Y, C1, C2, C3, calc_in_ggggg(C3, S, M, C4, O))
calc_in_ggggg(C0, D, E, C1, Y) → U60_ggggg(C0, D, E, C1, Y, sum_in_gga(C0, D, CD))
sum_in_gga(X, Y, Z) → U64_gga(X, Y, Z, isPlus_in_gga(X, Y, U))
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))) → U72_gga(X, Y, Z, isPlus_in_gga(X, Y, Z))
isPlus_in_gga(succ(X), pred(Y), Z) → U73_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) → U74_gga(X, Y, Z, isPlus_in_gga(X, Y, Z))
isPlus_in_gga(pred(X), pred(Y), pred(pred(Z))) → U75_gga(X, Y, Z, isPlus_in_gga(X, Y, Z))
U75_gga(X, Y, Z, isPlus_out_gga(X, Y, Z)) → isPlus_out_gga(pred(X), pred(Y), pred(pred(Z)))
U74_gga(X, Y, Z, isPlus_out_gga(X, Y, Z)) → isPlus_out_gga(pred(X), succ(Y), Z)
U73_gga(X, Y, Z, isPlus_out_gga(X, Y, Z)) → isPlus_out_gga(succ(X), pred(Y), Z)
U72_gga(X, Y, Z, isPlus_out_gga(X, Y, Z)) → isPlus_out_gga(succ(X), succ(Y), succ(succ(Z)))
U64_gga(X, Y, Z, isPlus_out_gga(X, Y, U)) → U65_gga(X, Y, Z, =_in_ag(Z, U))
=_in_ag(X, X) → =_out_ag(X, X)
U65_gga(X, Y, Z, =_out_ag(Z, U)) → sum_out_gga(X, Y, Z)
U60_ggggg(C0, D, E, C1, Y, sum_out_gga(C0, D, CD)) → U61_ggggg(C0, D, E, C1, Y, sum_in_gga(CD, E, S))
U61_ggggg(C0, D, E, C1, Y, sum_out_gga(CD, E, S)) → U62_ggggg(C0, D, E, C1, Y, S, carry10_in_ga(C1, C10))
carry10_in_ga(zero, zero) → carry10_out_ga(zero, zero)
carry10_in_ga(succ(zero), succ(succ(succ(succ(succ(succ(succ(succ(succ(succ(zero))))))))))) → carry10_out_ga(succ(zero), succ(succ(succ(succ(succ(succ(succ(succ(succ(succ(zero)))))))))))
U62_ggggg(C0, D, E, C1, Y, S, carry10_out_ga(C1, C10)) → U63_ggggg(C0, D, E, C1, Y, sum_in_ggg(C10, Y, S))
sum_in_ggg(X, Y, Z) → U64_ggg(X, Y, Z, isPlus_in_gga(X, Y, U))
U64_ggg(X, Y, Z, isPlus_out_gga(X, Y, U)) → U65_ggg(X, Y, Z, =_in_gg(Z, U))
=_in_gg(X, X) → =_out_gg(X, X)
U65_ggg(X, Y, Z, =_out_gg(Z, U)) → sum_out_ggg(X, Y, Z)
U63_ggggg(C0, D, E, C1, Y, sum_out_ggg(C10, Y, S)) → calc_out_ggggg(C0, D, E, C1, Y)
U56_aaaaaaaa(S, E, N, D, M, O, R, Y, C1, C2, C3, calc_out_ggggg(C3, S, M, C4, O)) → U57_aaaaaaaa(S, E, N, D, M, O, R, Y, C1, C2, calc_in_ggggg(C2, E, O, C3, N))
U57_aaaaaaaa(S, E, N, D, M, O, R, Y, C1, C2, calc_out_ggggg(C2, E, O, C3, N)) → U58_aaaaaaaa(S, E, N, D, M, O, R, Y, C1, calc_in_ggggg(C1, N, R, C2, E))
U58_aaaaaaaa(S, E, N, D, M, O, R, Y, C1, calc_out_ggggg(C1, N, R, C2, E)) → U59_aaaaaaaa(S, E, N, D, M, O, R, Y, calc_in_ggggg(zero, D, E, C1, Y))
U59_aaaaaaaa(S, E, N, D, M, O, R, Y, calc_out_ggggg(zero, D, E, C1, Y)) → money_out_aaaaaaaa(S, E, N, D, M, O, R, Y)

The argument filtering Pi contains the following mapping:
money_in_aaaaaaaa(x1, x2, x3, x4, x5, x6, x7, x8)  =  money_in_aaaaaaaa
U48_aaaaaaaa(x1, x2, x3, x4, x5, x6, x7, x8, x9)  =  U48_aaaaaaaa(x9)
carry_in_a(x1)  =  carry_in_a
carry_out_a(x1)  =  carry_out_a(x1)
U49_aaaaaaaa(x1, x2, x3, x4, x5, x6, x7, x8, x9, x10)  =  U49_aaaaaaaa(x9, x10)
U50_aaaaaaaa(x1, x2, x3, x4, x5, x6, x7, x8, x9, x10, x11)  =  U50_aaaaaaaa(x9, x10, x11)
U51_aaaaaaaa(x1, x2, x3, x4, x5, x6, x7, x8, x9, x10, x11, x12)  =  U51_aaaaaaaa(x9, x10, x11, x12)
U52_aaaaaaaa(x1, x2, x3, x4, x5, x6, x7, x8, x9, x10, x11, x12, x13)  =  U52_aaaaaaaa(x9, x10, x11, x12, x13)
=_in_ga(x1, x2)  =  =_in_ga(x1)
=_out_ga(x1, x2)  =  =_out_ga(x2)
U53_aaaaaaaa(x1, x2, x3, x4, x5, x6, x7, x8, x9, x10, x11, x12, x13)  =  U53_aaaaaaaa(x5, x9, x10, x11, x12, x13)
=\=_in_gg(x1, x2)  =  =\=_in_gg(x1, x2)
=\=_out_gg(x1, x2)  =  =\=_out_gg
zero  =  zero
U54_aaaaaaaa(x1, x2, x3, x4, x5, x6, x7, x8, x9, x10, x11, x12, x13)  =  U54_aaaaaaaa(x5, x9, x10, x11, x12, x13)
domain_in_ag(x1, x2)  =  domain_in_ag(x2)
domain_out_ag(x1, x2)  =  domain_out_ag(x1)
U66_ag(x1, x2, x3, x4)  =  U66_ag(x4)
del_in_aga(x1, x2, x3)  =  del_in_aga(x2)
.(x1, x2)  =  .(x1, x2)
del_out_aga(x1, x2, x3)  =  del_out_aga(x1, x3)
U68_aga(x1, x2, x3, x4, x5)  =  U68_aga(x2, x5)
U67_ag(x1, x2, x3, x4)  =  U67_ag(x1, x4)
[]  =  []
succ(x1)  =  succ(x1)
U55_aaaaaaaa(x1, x2, x3, x4, x5, x6, x7, x8, x9, x10, x11, x12, x13)  =  U55_aaaaaaaa(x1, x2, x3, x4, x5, x6, x7, x8, x9, x10, x11, x12, x13)
U56_aaaaaaaa(x1, x2, x3, x4, x5, x6, x7, x8, x9, x10, x11, x12)  =  U56_aaaaaaaa(x1, x2, x3, x4, x5, x6, x7, x8, x9, x10, x11, x12)
calc_in_ggggg(x1, x2, x3, x4, x5)  =  calc_in_ggggg(x1, x2, x3, x4, x5)
U60_ggggg(x1, x2, x3, x4, x5, x6)  =  U60_ggggg(x3, x4, x5, x6)
sum_in_gga(x1, x2, x3)  =  sum_in_gga(x1, x2)
U64_gga(x1, x2, x3, x4)  =  U64_gga(x4)
isPlus_in_gga(x1, x2, x3)  =  isPlus_in_gga(x1, x2)
isPlus_out_gga(x1, x2, x3)  =  isPlus_out_gga(x3)
U72_gga(x1, x2, x3, x4)  =  U72_gga(x4)
pred(x1)  =  pred(x1)
U73_gga(x1, x2, x3, x4)  =  U73_gga(x4)
U74_gga(x1, x2, x3, x4)  =  U74_gga(x4)
U75_gga(x1, x2, x3, x4)  =  U75_gga(x4)
U65_gga(x1, x2, x3, x4)  =  U65_gga(x4)
=_in_ag(x1, x2)  =  =_in_ag(x2)
=_out_ag(x1, x2)  =  =_out_ag(x1)
sum_out_gga(x1, x2, x3)  =  sum_out_gga(x3)
U61_ggggg(x1, x2, x3, x4, x5, x6)  =  U61_ggggg(x4, x5, x6)
U62_ggggg(x1, x2, x3, x4, x5, x6, x7)  =  U62_ggggg(x5, x6, x7)
carry10_in_ga(x1, x2)  =  carry10_in_ga(x1)
carry10_out_ga(x1, x2)  =  carry10_out_ga(x2)
U63_ggggg(x1, x2, x3, x4, x5, x6)  =  U63_ggggg(x6)
sum_in_ggg(x1, x2, x3)  =  sum_in_ggg(x1, x2, x3)
U64_ggg(x1, x2, x3, x4)  =  U64_ggg(x3, x4)
U65_ggg(x1, x2, x3, x4)  =  U65_ggg(x4)
=_in_gg(x1, x2)  =  =_in_gg(x1, x2)
=_out_gg(x1, x2)  =  =_out_gg
sum_out_ggg(x1, x2, x3)  =  sum_out_ggg
calc_out_ggggg(x1, x2, x3, x4, x5)  =  calc_out_ggggg
U57_aaaaaaaa(x1, x2, x3, x4, x5, x6, x7, x8, x9, x10, x11)  =  U57_aaaaaaaa(x1, x2, x3, x4, x5, x6, x7, x8, x9, x10, x11)
U58_aaaaaaaa(x1, x2, x3, x4, x5, x6, x7, x8, x9, x10)  =  U58_aaaaaaaa(x1, x2, x3, x4, x5, x6, x7, x8, x9, x10)
U59_aaaaaaaa(x1, x2, x3, x4, x5, x6, x7, x8, x9)  =  U59_aaaaaaaa(x1, x2, x3, x4, x5, x6, x7, x8, x9)
money_out_aaaaaaaa(x1, x2, x3, x4, x5, x6, x7, x8)  =  money_out_aaaaaaaa(x1, x2, x3, x4, x5, x6, x7, x8)


Using Dependency Pairs [1,30] we result in the following initial DP problem:
Pi DP problem:
The TRS P consists of the following rules:

MONEY_IN_AAAAAAAA(S, E, N, D, M, O, R, Y) → U48_AAAAAAAA(S, E, N, D, M, O, R, Y, carry_in_a(C1))
MONEY_IN_AAAAAAAA(S, E, N, D, M, O, R, Y) → CARRY_IN_A(C1)
U48_AAAAAAAA(S, E, N, D, M, O, R, Y, carry_out_a(C1)) → U49_AAAAAAAA(S, E, N, D, M, O, R, Y, C1, carry_in_a(C2))
U48_AAAAAAAA(S, E, N, D, M, O, R, Y, carry_out_a(C1)) → CARRY_IN_A(C2)
U49_AAAAAAAA(S, E, N, D, M, O, R, Y, C1, carry_out_a(C2)) → U50_AAAAAAAA(S, E, N, D, M, O, R, Y, C1, C2, carry_in_a(C3))
U49_AAAAAAAA(S, E, N, D, M, O, R, Y, C1, carry_out_a(C2)) → CARRY_IN_A(C3)
U50_AAAAAAAA(S, E, N, D, M, O, R, Y, C1, C2, carry_out_a(C3)) → U51_AAAAAAAA(S, E, N, D, M, O, R, Y, C1, C2, C3, carry_in_a(C4))
U50_AAAAAAAA(S, E, N, D, M, O, R, Y, C1, C2, carry_out_a(C3)) → CARRY_IN_A(C4)
U51_AAAAAAAA(S, E, N, D, M, O, R, Y, C1, C2, C3, carry_out_a(C4)) → U52_AAAAAAAA(S, E, N, D, M, O, R, Y, C1, C2, C3, C4, =_in_ga(C4, M))
U51_AAAAAAAA(S, E, N, D, M, O, R, Y, C1, C2, C3, carry_out_a(C4)) → =_IN_GA(C4, M)
U52_AAAAAAAA(S, E, N, D, M, O, R, Y, C1, C2, C3, C4, =_out_ga(C4, M)) → U53_AAAAAAAA(S, E, N, D, M, O, R, Y, C1, C2, C3, C4, =\=_in_gg(M, zero))
U52_AAAAAAAA(S, E, N, D, M, O, R, Y, C1, C2, C3, C4, =_out_ga(C4, M)) → =\=_IN_GG(M, zero)
U53_AAAAAAAA(S, E, N, D, M, O, R, Y, C1, C2, C3, C4, =\=_out_gg(M, zero)) → U54_AAAAAAAA(S, E, N, D, M, O, R, Y, C1, C2, C3, C4, domain_in_ag(.(S, .(E, .(N, .(D, .(M, .(O, .(R, .(Y, [])))))))), .(zero, .(succ(zero), .(succ(succ(zero)), .(succ(succ(succ(zero))), .(succ(succ(succ(succ(zero)))), .(succ(succ(succ(succ(succ(zero))))), .(succ(succ(succ(succ(succ(succ(zero)))))), .(succ(succ(succ(succ(succ(succ(succ(zero))))))), .(succ(succ(succ(succ(succ(succ(succ(succ(zero)))))))), .(succ(succ(succ(succ(succ(succ(succ(succ(succ(zero))))))))), []))))))))))))
U53_AAAAAAAA(S, E, N, D, M, O, R, Y, C1, C2, C3, C4, =\=_out_gg(M, zero)) → DOMAIN_IN_AG(.(S, .(E, .(N, .(D, .(M, .(O, .(R, .(Y, [])))))))), .(zero, .(succ(zero), .(succ(succ(zero)), .(succ(succ(succ(zero))), .(succ(succ(succ(succ(zero)))), .(succ(succ(succ(succ(succ(zero))))), .(succ(succ(succ(succ(succ(succ(zero)))))), .(succ(succ(succ(succ(succ(succ(succ(zero))))))), .(succ(succ(succ(succ(succ(succ(succ(succ(zero)))))))), .(succ(succ(succ(succ(succ(succ(succ(succ(succ(zero))))))))), [])))))))))))
DOMAIN_IN_AG(.(X1, R), L) → U66_AG(X1, R, L, del_in_aga(X1, L, NL))
DOMAIN_IN_AG(.(X1, R), L) → DEL_IN_AGA(X1, L, NL)
DEL_IN_AGA(X, .(Y, T), .(Y, NT)) → U68_AGA(X, Y, T, NT, del_in_aga(X, T, NT))
DEL_IN_AGA(X, .(Y, T), .(Y, NT)) → DEL_IN_AGA(X, T, NT)
U66_AG(X1, R, L, del_out_aga(X1, L, NL)) → U67_AG(X1, R, L, domain_in_ag(R, NL))
U66_AG(X1, R, L, del_out_aga(X1, L, NL)) → DOMAIN_IN_AG(R, NL)
U54_AAAAAAAA(S, E, N, D, M, O, R, Y, C1, C2, C3, C4, domain_out_ag(.(S, .(E, .(N, .(D, .(M, .(O, .(R, .(Y, [])))))))), .(zero, .(succ(zero), .(succ(succ(zero)), .(succ(succ(succ(zero))), .(succ(succ(succ(succ(zero)))), .(succ(succ(succ(succ(succ(zero))))), .(succ(succ(succ(succ(succ(succ(zero)))))), .(succ(succ(succ(succ(succ(succ(succ(zero))))))), .(succ(succ(succ(succ(succ(succ(succ(succ(zero)))))))), .(succ(succ(succ(succ(succ(succ(succ(succ(succ(zero))))))))), [])))))))))))) → U55_AAAAAAAA(S, E, N, D, M, O, R, Y, C1, C2, C3, C4, =\=_in_gg(S, zero))
U54_AAAAAAAA(S, E, N, D, M, O, R, Y, C1, C2, C3, C4, domain_out_ag(.(S, .(E, .(N, .(D, .(M, .(O, .(R, .(Y, [])))))))), .(zero, .(succ(zero), .(succ(succ(zero)), .(succ(succ(succ(zero))), .(succ(succ(succ(succ(zero)))), .(succ(succ(succ(succ(succ(zero))))), .(succ(succ(succ(succ(succ(succ(zero)))))), .(succ(succ(succ(succ(succ(succ(succ(zero))))))), .(succ(succ(succ(succ(succ(succ(succ(succ(zero)))))))), .(succ(succ(succ(succ(succ(succ(succ(succ(succ(zero))))))))), [])))))))))))) → =\=_IN_GG(S, zero)
U55_AAAAAAAA(S, E, N, D, M, O, R, Y, C1, C2, C3, C4, =\=_out_gg(S, zero)) → U56_AAAAAAAA(S, E, N, D, M, O, R, Y, C1, C2, C3, calc_in_ggggg(C3, S, M, C4, O))
U55_AAAAAAAA(S, E, N, D, M, O, R, Y, C1, C2, C3, C4, =\=_out_gg(S, zero)) → CALC_IN_GGGGG(C3, S, M, C4, O)
CALC_IN_GGGGG(C0, D, E, C1, Y) → U60_GGGGG(C0, D, E, C1, Y, sum_in_gga(C0, D, CD))
CALC_IN_GGGGG(C0, D, E, C1, Y) → SUM_IN_GGA(C0, D, CD)
SUM_IN_GGA(X, Y, Z) → U64_GGA(X, Y, Z, isPlus_in_gga(X, Y, U))
SUM_IN_GGA(X, Y, Z) → ISPLUS_IN_GGA(X, Y, U)
ISPLUS_IN_GGA(succ(X), succ(Y), succ(succ(Z))) → U72_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) → U73_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) → U74_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))) → U75_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)
U64_GGA(X, Y, Z, isPlus_out_gga(X, Y, U)) → U65_GGA(X, Y, Z, =_in_ag(Z, U))
U64_GGA(X, Y, Z, isPlus_out_gga(X, Y, U)) → =_IN_AG(Z, U)
U60_GGGGG(C0, D, E, C1, Y, sum_out_gga(C0, D, CD)) → U61_GGGGG(C0, D, E, C1, Y, sum_in_gga(CD, E, S))
U60_GGGGG(C0, D, E, C1, Y, sum_out_gga(C0, D, CD)) → SUM_IN_GGA(CD, E, S)
U61_GGGGG(C0, D, E, C1, Y, sum_out_gga(CD, E, S)) → U62_GGGGG(C0, D, E, C1, Y, S, carry10_in_ga(C1, C10))
U61_GGGGG(C0, D, E, C1, Y, sum_out_gga(CD, E, S)) → CARRY10_IN_GA(C1, C10)
U62_GGGGG(C0, D, E, C1, Y, S, carry10_out_ga(C1, C10)) → U63_GGGGG(C0, D, E, C1, Y, sum_in_ggg(C10, Y, S))
U62_GGGGG(C0, D, E, C1, Y, S, carry10_out_ga(C1, C10)) → SUM_IN_GGG(C10, Y, S)
SUM_IN_GGG(X, Y, Z) → U64_GGG(X, Y, Z, isPlus_in_gga(X, Y, U))
SUM_IN_GGG(X, Y, Z) → ISPLUS_IN_GGA(X, Y, U)
U64_GGG(X, Y, Z, isPlus_out_gga(X, Y, U)) → U65_GGG(X, Y, Z, =_in_gg(Z, U))
U64_GGG(X, Y, Z, isPlus_out_gga(X, Y, U)) → =_IN_GG(Z, U)
U56_AAAAAAAA(S, E, N, D, M, O, R, Y, C1, C2, C3, calc_out_ggggg(C3, S, M, C4, O)) → U57_AAAAAAAA(S, E, N, D, M, O, R, Y, C1, C2, calc_in_ggggg(C2, E, O, C3, N))
U56_AAAAAAAA(S, E, N, D, M, O, R, Y, C1, C2, C3, calc_out_ggggg(C3, S, M, C4, O)) → CALC_IN_GGGGG(C2, E, O, C3, N)
U57_AAAAAAAA(S, E, N, D, M, O, R, Y, C1, C2, calc_out_ggggg(C2, E, O, C3, N)) → U58_AAAAAAAA(S, E, N, D, M, O, R, Y, C1, calc_in_ggggg(C1, N, R, C2, E))
U57_AAAAAAAA(S, E, N, D, M, O, R, Y, C1, C2, calc_out_ggggg(C2, E, O, C3, N)) → CALC_IN_GGGGG(C1, N, R, C2, E)
U58_AAAAAAAA(S, E, N, D, M, O, R, Y, C1, calc_out_ggggg(C1, N, R, C2, E)) → U59_AAAAAAAA(S, E, N, D, M, O, R, Y, calc_in_ggggg(zero, D, E, C1, Y))
U58_AAAAAAAA(S, E, N, D, M, O, R, Y, C1, calc_out_ggggg(C1, N, R, C2, E)) → CALC_IN_GGGGG(zero, D, E, C1, Y)

The TRS R consists of the following rules:

money_in_aaaaaaaa(S, E, N, D, M, O, R, Y) → U48_aaaaaaaa(S, E, N, D, M, O, R, Y, carry_in_a(C1))
carry_in_a(succ(zero)) → carry_out_a(succ(zero))
carry_in_a(zero) → carry_out_a(zero)
U48_aaaaaaaa(S, E, N, D, M, O, R, Y, carry_out_a(C1)) → U49_aaaaaaaa(S, E, N, D, M, O, R, Y, C1, carry_in_a(C2))
U49_aaaaaaaa(S, E, N, D, M, O, R, Y, C1, carry_out_a(C2)) → U50_aaaaaaaa(S, E, N, D, M, O, R, Y, C1, C2, carry_in_a(C3))
U50_aaaaaaaa(S, E, N, D, M, O, R, Y, C1, C2, carry_out_a(C3)) → U51_aaaaaaaa(S, E, N, D, M, O, R, Y, C1, C2, C3, carry_in_a(C4))
U51_aaaaaaaa(S, E, N, D, M, O, R, Y, C1, C2, C3, carry_out_a(C4)) → U52_aaaaaaaa(S, E, N, D, M, O, R, Y, C1, C2, C3, C4, =_in_ga(C4, M))
=_in_ga(X, X) → =_out_ga(X, X)
U52_aaaaaaaa(S, E, N, D, M, O, R, Y, C1, C2, C3, C4, =_out_ga(C4, M)) → U53_aaaaaaaa(S, E, N, D, M, O, R, Y, C1, C2, C3, C4, =\=_in_gg(M, zero))
=\=_in_gg(X0, X1) → =\=_out_gg(X0, X1)
U53_aaaaaaaa(S, E, N, D, M, O, R, Y, C1, C2, C3, C4, =\=_out_gg(M, zero)) → U54_aaaaaaaa(S, E, N, D, M, O, R, Y, C1, C2, C3, C4, domain_in_ag(.(S, .(E, .(N, .(D, .(M, .(O, .(R, .(Y, [])))))))), .(zero, .(succ(zero), .(succ(succ(zero)), .(succ(succ(succ(zero))), .(succ(succ(succ(succ(zero)))), .(succ(succ(succ(succ(succ(zero))))), .(succ(succ(succ(succ(succ(succ(zero)))))), .(succ(succ(succ(succ(succ(succ(succ(zero))))))), .(succ(succ(succ(succ(succ(succ(succ(succ(zero)))))))), .(succ(succ(succ(succ(succ(succ(succ(succ(succ(zero))))))))), []))))))))))))
domain_in_ag([], X) → domain_out_ag([], X)
domain_in_ag(.(X1, R), L) → U66_ag(X1, R, L, del_in_aga(X1, L, NL))
del_in_aga(X, .(X, T), T) → del_out_aga(X, .(X, T), T)
del_in_aga(X, .(Y, T), .(Y, NT)) → U68_aga(X, Y, T, NT, del_in_aga(X, T, NT))
U68_aga(X, Y, T, NT, del_out_aga(X, T, NT)) → del_out_aga(X, .(Y, T), .(Y, NT))
U66_ag(X1, R, L, del_out_aga(X1, L, NL)) → U67_ag(X1, R, L, domain_in_ag(R, NL))
U67_ag(X1, R, L, domain_out_ag(R, NL)) → domain_out_ag(.(X1, R), L)
U54_aaaaaaaa(S, E, N, D, M, O, R, Y, C1, C2, C3, C4, domain_out_ag(.(S, .(E, .(N, .(D, .(M, .(O, .(R, .(Y, [])))))))), .(zero, .(succ(zero), .(succ(succ(zero)), .(succ(succ(succ(zero))), .(succ(succ(succ(succ(zero)))), .(succ(succ(succ(succ(succ(zero))))), .(succ(succ(succ(succ(succ(succ(zero)))))), .(succ(succ(succ(succ(succ(succ(succ(zero))))))), .(succ(succ(succ(succ(succ(succ(succ(succ(zero)))))))), .(succ(succ(succ(succ(succ(succ(succ(succ(succ(zero))))))))), [])))))))))))) → U55_aaaaaaaa(S, E, N, D, M, O, R, Y, C1, C2, C3, C4, =\=_in_gg(S, zero))
U55_aaaaaaaa(S, E, N, D, M, O, R, Y, C1, C2, C3, C4, =\=_out_gg(S, zero)) → U56_aaaaaaaa(S, E, N, D, M, O, R, Y, C1, C2, C3, calc_in_ggggg(C3, S, M, C4, O))
calc_in_ggggg(C0, D, E, C1, Y) → U60_ggggg(C0, D, E, C1, Y, sum_in_gga(C0, D, CD))
sum_in_gga(X, Y, Z) → U64_gga(X, Y, Z, isPlus_in_gga(X, Y, U))
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))) → U72_gga(X, Y, Z, isPlus_in_gga(X, Y, Z))
isPlus_in_gga(succ(X), pred(Y), Z) → U73_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) → U74_gga(X, Y, Z, isPlus_in_gga(X, Y, Z))
isPlus_in_gga(pred(X), pred(Y), pred(pred(Z))) → U75_gga(X, Y, Z, isPlus_in_gga(X, Y, Z))
U75_gga(X, Y, Z, isPlus_out_gga(X, Y, Z)) → isPlus_out_gga(pred(X), pred(Y), pred(pred(Z)))
U74_gga(X, Y, Z, isPlus_out_gga(X, Y, Z)) → isPlus_out_gga(pred(X), succ(Y), Z)
U73_gga(X, Y, Z, isPlus_out_gga(X, Y, Z)) → isPlus_out_gga(succ(X), pred(Y), Z)
U72_gga(X, Y, Z, isPlus_out_gga(X, Y, Z)) → isPlus_out_gga(succ(X), succ(Y), succ(succ(Z)))
U64_gga(X, Y, Z, isPlus_out_gga(X, Y, U)) → U65_gga(X, Y, Z, =_in_ag(Z, U))
=_in_ag(X, X) → =_out_ag(X, X)
U65_gga(X, Y, Z, =_out_ag(Z, U)) → sum_out_gga(X, Y, Z)
U60_ggggg(C0, D, E, C1, Y, sum_out_gga(C0, D, CD)) → U61_ggggg(C0, D, E, C1, Y, sum_in_gga(CD, E, S))
U61_ggggg(C0, D, E, C1, Y, sum_out_gga(CD, E, S)) → U62_ggggg(C0, D, E, C1, Y, S, carry10_in_ga(C1, C10))
carry10_in_ga(zero, zero) → carry10_out_ga(zero, zero)
carry10_in_ga(succ(zero), succ(succ(succ(succ(succ(succ(succ(succ(succ(succ(zero))))))))))) → carry10_out_ga(succ(zero), succ(succ(succ(succ(succ(succ(succ(succ(succ(succ(zero)))))))))))
U62_ggggg(C0, D, E, C1, Y, S, carry10_out_ga(C1, C10)) → U63_ggggg(C0, D, E, C1, Y, sum_in_ggg(C10, Y, S))
sum_in_ggg(X, Y, Z) → U64_ggg(X, Y, Z, isPlus_in_gga(X, Y, U))
U64_ggg(X, Y, Z, isPlus_out_gga(X, Y, U)) → U65_ggg(X, Y, Z, =_in_gg(Z, U))
=_in_gg(X, X) → =_out_gg(X, X)
U65_ggg(X, Y, Z, =_out_gg(Z, U)) → sum_out_ggg(X, Y, Z)
U63_ggggg(C0, D, E, C1, Y, sum_out_ggg(C10, Y, S)) → calc_out_ggggg(C0, D, E, C1, Y)
U56_aaaaaaaa(S, E, N, D, M, O, R, Y, C1, C2, C3, calc_out_ggggg(C3, S, M, C4, O)) → U57_aaaaaaaa(S, E, N, D, M, O, R, Y, C1, C2, calc_in_ggggg(C2, E, O, C3, N))
U57_aaaaaaaa(S, E, N, D, M, O, R, Y, C1, C2, calc_out_ggggg(C2, E, O, C3, N)) → U58_aaaaaaaa(S, E, N, D, M, O, R, Y, C1, calc_in_ggggg(C1, N, R, C2, E))
U58_aaaaaaaa(S, E, N, D, M, O, R, Y, C1, calc_out_ggggg(C1, N, R, C2, E)) → U59_aaaaaaaa(S, E, N, D, M, O, R, Y, calc_in_ggggg(zero, D, E, C1, Y))
U59_aaaaaaaa(S, E, N, D, M, O, R, Y, calc_out_ggggg(zero, D, E, C1, Y)) → money_out_aaaaaaaa(S, E, N, D, M, O, R, Y)

The argument filtering Pi contains the following mapping:
money_in_aaaaaaaa(x1, x2, x3, x4, x5, x6, x7, x8)  =  money_in_aaaaaaaa
U48_aaaaaaaa(x1, x2, x3, x4, x5, x6, x7, x8, x9)  =  U48_aaaaaaaa(x9)
carry_in_a(x1)  =  carry_in_a
carry_out_a(x1)  =  carry_out_a(x1)
U49_aaaaaaaa(x1, x2, x3, x4, x5, x6, x7, x8, x9, x10)  =  U49_aaaaaaaa(x9, x10)
U50_aaaaaaaa(x1, x2, x3, x4, x5, x6, x7, x8, x9, x10, x11)  =  U50_aaaaaaaa(x9, x10, x11)
U51_aaaaaaaa(x1, x2, x3, x4, x5, x6, x7, x8, x9, x10, x11, x12)  =  U51_aaaaaaaa(x9, x10, x11, x12)
U52_aaaaaaaa(x1, x2, x3, x4, x5, x6, x7, x8, x9, x10, x11, x12, x13)  =  U52_aaaaaaaa(x9, x10, x11, x12, x13)
=_in_ga(x1, x2)  =  =_in_ga(x1)
=_out_ga(x1, x2)  =  =_out_ga(x2)
U53_aaaaaaaa(x1, x2, x3, x4, x5, x6, x7, x8, x9, x10, x11, x12, x13)  =  U53_aaaaaaaa(x5, x9, x10, x11, x12, x13)
=\=_in_gg(x1, x2)  =  =\=_in_gg(x1, x2)
=\=_out_gg(x1, x2)  =  =\=_out_gg
zero  =  zero
U54_aaaaaaaa(x1, x2, x3, x4, x5, x6, x7, x8, x9, x10, x11, x12, x13)  =  U54_aaaaaaaa(x5, x9, x10, x11, x12, x13)
domain_in_ag(x1, x2)  =  domain_in_ag(x2)
domain_out_ag(x1, x2)  =  domain_out_ag(x1)
U66_ag(x1, x2, x3, x4)  =  U66_ag(x4)
del_in_aga(x1, x2, x3)  =  del_in_aga(x2)
.(x1, x2)  =  .(x1, x2)
del_out_aga(x1, x2, x3)  =  del_out_aga(x1, x3)
U68_aga(x1, x2, x3, x4, x5)  =  U68_aga(x2, x5)
U67_ag(x1, x2, x3, x4)  =  U67_ag(x1, x4)
[]  =  []
succ(x1)  =  succ(x1)
U55_aaaaaaaa(x1, x2, x3, x4, x5, x6, x7, x8, x9, x10, x11, x12, x13)  =  U55_aaaaaaaa(x1, x2, x3, x4, x5, x6, x7, x8, x9, x10, x11, x12, x13)
U56_aaaaaaaa(x1, x2, x3, x4, x5, x6, x7, x8, x9, x10, x11, x12)  =  U56_aaaaaaaa(x1, x2, x3, x4, x5, x6, x7, x8, x9, x10, x11, x12)
calc_in_ggggg(x1, x2, x3, x4, x5)  =  calc_in_ggggg(x1, x2, x3, x4, x5)
U60_ggggg(x1, x2, x3, x4, x5, x6)  =  U60_ggggg(x3, x4, x5, x6)
sum_in_gga(x1, x2, x3)  =  sum_in_gga(x1, x2)
U64_gga(x1, x2, x3, x4)  =  U64_gga(x4)
isPlus_in_gga(x1, x2, x3)  =  isPlus_in_gga(x1, x2)
isPlus_out_gga(x1, x2, x3)  =  isPlus_out_gga(x3)
U72_gga(x1, x2, x3, x4)  =  U72_gga(x4)
pred(x1)  =  pred(x1)
U73_gga(x1, x2, x3, x4)  =  U73_gga(x4)
U74_gga(x1, x2, x3, x4)  =  U74_gga(x4)
U75_gga(x1, x2, x3, x4)  =  U75_gga(x4)
U65_gga(x1, x2, x3, x4)  =  U65_gga(x4)
=_in_ag(x1, x2)  =  =_in_ag(x2)
=_out_ag(x1, x2)  =  =_out_ag(x1)
sum_out_gga(x1, x2, x3)  =  sum_out_gga(x3)
U61_ggggg(x1, x2, x3, x4, x5, x6)  =  U61_ggggg(x4, x5, x6)
U62_ggggg(x1, x2, x3, x4, x5, x6, x7)  =  U62_ggggg(x5, x6, x7)
carry10_in_ga(x1, x2)  =  carry10_in_ga(x1)
carry10_out_ga(x1, x2)  =  carry10_out_ga(x2)
U63_ggggg(x1, x2, x3, x4, x5, x6)  =  U63_ggggg(x6)
sum_in_ggg(x1, x2, x3)  =  sum_in_ggg(x1, x2, x3)
U64_ggg(x1, x2, x3, x4)  =  U64_ggg(x3, x4)
U65_ggg(x1, x2, x3, x4)  =  U65_ggg(x4)
=_in_gg(x1, x2)  =  =_in_gg(x1, x2)
=_out_gg(x1, x2)  =  =_out_gg
sum_out_ggg(x1, x2, x3)  =  sum_out_ggg
calc_out_ggggg(x1, x2, x3, x4, x5)  =  calc_out_ggggg
U57_aaaaaaaa(x1, x2, x3, x4, x5, x6, x7, x8, x9, x10, x11)  =  U57_aaaaaaaa(x1, x2, x3, x4, x5, x6, x7, x8, x9, x10, x11)
U58_aaaaaaaa(x1, x2, x3, x4, x5, x6, x7, x8, x9, x10)  =  U58_aaaaaaaa(x1, x2, x3, x4, x5, x6, x7, x8, x9, x10)
U59_aaaaaaaa(x1, x2, x3, x4, x5, x6, x7, x8, x9)  =  U59_aaaaaaaa(x1, x2, x3, x4, x5, x6, x7, x8, x9)
money_out_aaaaaaaa(x1, x2, x3, x4, x5, x6, x7, x8)  =  money_out_aaaaaaaa(x1, x2, x3, x4, x5, x6, x7, x8)
MONEY_IN_AAAAAAAA(x1, x2, x3, x4, x5, x6, x7, x8)  =  MONEY_IN_AAAAAAAA
U50_AAAAAAAA(x1, x2, x3, x4, x5, x6, x7, x8, x9, x10, x11)  =  U50_AAAAAAAA(x9, x10, x11)
U54_AAAAAAAA(x1, x2, x3, x4, x5, x6, x7, x8, x9, x10, x11, x12, x13)  =  U54_AAAAAAAA(x5, x9, x10, x11, x12, x13)
=_IN_GG(x1, x2)  =  =_IN_GG(x1, x2)
U74_GGA(x1, x2, x3, x4)  =  U74_GGA(x4)
CARRY_IN_A(x1)  =  CARRY_IN_A
U68_AGA(x1, x2, x3, x4, x5)  =  U68_AGA(x2, x5)
U60_GGGGG(x1, x2, x3, x4, x5, x6)  =  U60_GGGGG(x3, x4, x5, x6)
U57_AAAAAAAA(x1, x2, x3, x4, x5, x6, x7, x8, x9, x10, x11)  =  U57_AAAAAAAA(x1, x2, x3, x4, x5, x6, x7, x8, x9, x10, x11)
U63_GGGGG(x1, x2, x3, x4, x5, x6)  =  U63_GGGGG(x6)
U65_GGG(x1, x2, x3, x4)  =  U65_GGG(x4)
CALC_IN_GGGGG(x1, x2, x3, x4, x5)  =  CALC_IN_GGGGG(x1, x2, x3, x4, x5)
DEL_IN_AGA(x1, x2, x3)  =  DEL_IN_AGA(x2)
U72_GGA(x1, x2, x3, x4)  =  U72_GGA(x4)
=_IN_AG(x1, x2)  =  =_IN_AG(x2)
U62_GGGGG(x1, x2, x3, x4, x5, x6, x7)  =  U62_GGGGG(x5, x6, x7)
U52_AAAAAAAA(x1, x2, x3, x4, x5, x6, x7, x8, x9, x10, x11, x12, x13)  =  U52_AAAAAAAA(x9, x10, x11, x12, x13)
U59_AAAAAAAA(x1, x2, x3, x4, x5, x6, x7, x8, x9)  =  U59_AAAAAAAA(x1, x2, x3, x4, x5, x6, x7, x8, x9)
U66_AG(x1, x2, x3, x4)  =  U66_AG(x4)
U48_AAAAAAAA(x1, x2, x3, x4, x5, x6, x7, x8, x9)  =  U48_AAAAAAAA(x9)
U65_GGA(x1, x2, x3, x4)  =  U65_GGA(x4)
SUM_IN_GGG(x1, x2, x3)  =  SUM_IN_GGG(x1, x2, x3)
U56_AAAAAAAA(x1, x2, x3, x4, x5, x6, x7, x8, x9, x10, x11, x12)  =  U56_AAAAAAAA(x1, x2, x3, x4, x5, x6, x7, x8, x9, x10, x11, x12)
U58_AAAAAAAA(x1, x2, x3, x4, x5, x6, x7, x8, x9, x10)  =  U58_AAAAAAAA(x1, x2, x3, x4, x5, x6, x7, x8, x9, x10)
U55_AAAAAAAA(x1, x2, x3, x4, x5, x6, x7, x8, x9, x10, x11, x12, x13)  =  U55_AAAAAAAA(x1, x2, x3, x4, x5, x6, x7, x8, x9, x10, x11, x12, x13)
CARRY10_IN_GA(x1, x2)  =  CARRY10_IN_GA(x1)
ISPLUS_IN_GGA(x1, x2, x3)  =  ISPLUS_IN_GGA(x1, x2)
U53_AAAAAAAA(x1, x2, x3, x4, x5, x6, x7, x8, x9, x10, x11, x12, x13)  =  U53_AAAAAAAA(x5, x9, x10, x11, x12, x13)
DOMAIN_IN_AG(x1, x2)  =  DOMAIN_IN_AG(x2)
U51_AAAAAAAA(x1, x2, x3, x4, x5, x6, x7, x8, x9, x10, x11, x12)  =  U51_AAAAAAAA(x9, x10, x11, x12)
U64_GGA(x1, x2, x3, x4)  =  U64_GGA(x4)
U75_GGA(x1, x2, x3, x4)  =  U75_GGA(x4)
U67_AG(x1, x2, x3, x4)  =  U67_AG(x1, x4)
=_IN_GA(x1, x2)  =  =_IN_GA(x1)
=\=_IN_GG(x1, x2)  =  =\=_IN_GG(x1, x2)
SUM_IN_GGA(x1, x2, x3)  =  SUM_IN_GGA(x1, x2)
U73_GGA(x1, x2, x3, x4)  =  U73_GGA(x4)
U64_GGG(x1, x2, x3, x4)  =  U64_GGG(x3, x4)
U61_GGGGG(x1, x2, x3, x4, x5, x6)  =  U61_GGGGG(x4, x5, x6)
U49_AAAAAAAA(x1, x2, x3, x4, x5, x6, x7, x8, x9, x10)  =  U49_AAAAAAAA(x9, x10)

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

↳ Prolog
  ↳ PredefinedPredicateTransformerProof
    ↳ Prolog
      ↳ CutEliminatorProof
        ↳ Prolog
          ↳ UndefinedPredicateHandlerProof
            ↳ Prolog
              ↳ PrologToPiTRSProof
                ↳ PiTRS
                  ↳ DependencyPairsProof
                    ↳ PiDP
                      ↳ DependencyGraphProof

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

MONEY_IN_AAAAAAAA(S, E, N, D, M, O, R, Y) → U48_AAAAAAAA(S, E, N, D, M, O, R, Y, carry_in_a(C1))
MONEY_IN_AAAAAAAA(S, E, N, D, M, O, R, Y) → CARRY_IN_A(C1)
U48_AAAAAAAA(S, E, N, D, M, O, R, Y, carry_out_a(C1)) → U49_AAAAAAAA(S, E, N, D, M, O, R, Y, C1, carry_in_a(C2))
U48_AAAAAAAA(S, E, N, D, M, O, R, Y, carry_out_a(C1)) → CARRY_IN_A(C2)
U49_AAAAAAAA(S, E, N, D, M, O, R, Y, C1, carry_out_a(C2)) → U50_AAAAAAAA(S, E, N, D, M, O, R, Y, C1, C2, carry_in_a(C3))
U49_AAAAAAAA(S, E, N, D, M, O, R, Y, C1, carry_out_a(C2)) → CARRY_IN_A(C3)
U50_AAAAAAAA(S, E, N, D, M, O, R, Y, C1, C2, carry_out_a(C3)) → U51_AAAAAAAA(S, E, N, D, M, O, R, Y, C1, C2, C3, carry_in_a(C4))
U50_AAAAAAAA(S, E, N, D, M, O, R, Y, C1, C2, carry_out_a(C3)) → CARRY_IN_A(C4)
U51_AAAAAAAA(S, E, N, D, M, O, R, Y, C1, C2, C3, carry_out_a(C4)) → U52_AAAAAAAA(S, E, N, D, M, O, R, Y, C1, C2, C3, C4, =_in_ga(C4, M))
U51_AAAAAAAA(S, E, N, D, M, O, R, Y, C1, C2, C3, carry_out_a(C4)) → =_IN_GA(C4, M)
U52_AAAAAAAA(S, E, N, D, M, O, R, Y, C1, C2, C3, C4, =_out_ga(C4, M)) → U53_AAAAAAAA(S, E, N, D, M, O, R, Y, C1, C2, C3, C4, =\=_in_gg(M, zero))
U52_AAAAAAAA(S, E, N, D, M, O, R, Y, C1, C2, C3, C4, =_out_ga(C4, M)) → =\=_IN_GG(M, zero)
U53_AAAAAAAA(S, E, N, D, M, O, R, Y, C1, C2, C3, C4, =\=_out_gg(M, zero)) → U54_AAAAAAAA(S, E, N, D, M, O, R, Y, C1, C2, C3, C4, domain_in_ag(.(S, .(E, .(N, .(D, .(M, .(O, .(R, .(Y, [])))))))), .(zero, .(succ(zero), .(succ(succ(zero)), .(succ(succ(succ(zero))), .(succ(succ(succ(succ(zero)))), .(succ(succ(succ(succ(succ(zero))))), .(succ(succ(succ(succ(succ(succ(zero)))))), .(succ(succ(succ(succ(succ(succ(succ(zero))))))), .(succ(succ(succ(succ(succ(succ(succ(succ(zero)))))))), .(succ(succ(succ(succ(succ(succ(succ(succ(succ(zero))))))))), []))))))))))))
U53_AAAAAAAA(S, E, N, D, M, O, R, Y, C1, C2, C3, C4, =\=_out_gg(M, zero)) → DOMAIN_IN_AG(.(S, .(E, .(N, .(D, .(M, .(O, .(R, .(Y, [])))))))), .(zero, .(succ(zero), .(succ(succ(zero)), .(succ(succ(succ(zero))), .(succ(succ(succ(succ(zero)))), .(succ(succ(succ(succ(succ(zero))))), .(succ(succ(succ(succ(succ(succ(zero)))))), .(succ(succ(succ(succ(succ(succ(succ(zero))))))), .(succ(succ(succ(succ(succ(succ(succ(succ(zero)))))))), .(succ(succ(succ(succ(succ(succ(succ(succ(succ(zero))))))))), [])))))))))))
DOMAIN_IN_AG(.(X1, R), L) → U66_AG(X1, R, L, del_in_aga(X1, L, NL))
DOMAIN_IN_AG(.(X1, R), L) → DEL_IN_AGA(X1, L, NL)
DEL_IN_AGA(X, .(Y, T), .(Y, NT)) → U68_AGA(X, Y, T, NT, del_in_aga(X, T, NT))
DEL_IN_AGA(X, .(Y, T), .(Y, NT)) → DEL_IN_AGA(X, T, NT)
U66_AG(X1, R, L, del_out_aga(X1, L, NL)) → U67_AG(X1, R, L, domain_in_ag(R, NL))
U66_AG(X1, R, L, del_out_aga(X1, L, NL)) → DOMAIN_IN_AG(R, NL)
U54_AAAAAAAA(S, E, N, D, M, O, R, Y, C1, C2, C3, C4, domain_out_ag(.(S, .(E, .(N, .(D, .(M, .(O, .(R, .(Y, [])))))))), .(zero, .(succ(zero), .(succ(succ(zero)), .(succ(succ(succ(zero))), .(succ(succ(succ(succ(zero)))), .(succ(succ(succ(succ(succ(zero))))), .(succ(succ(succ(succ(succ(succ(zero)))))), .(succ(succ(succ(succ(succ(succ(succ(zero))))))), .(succ(succ(succ(succ(succ(succ(succ(succ(zero)))))))), .(succ(succ(succ(succ(succ(succ(succ(succ(succ(zero))))))))), [])))))))))))) → U55_AAAAAAAA(S, E, N, D, M, O, R, Y, C1, C2, C3, C4, =\=_in_gg(S, zero))
U54_AAAAAAAA(S, E, N, D, M, O, R, Y, C1, C2, C3, C4, domain_out_ag(.(S, .(E, .(N, .(D, .(M, .(O, .(R, .(Y, [])))))))), .(zero, .(succ(zero), .(succ(succ(zero)), .(succ(succ(succ(zero))), .(succ(succ(succ(succ(zero)))), .(succ(succ(succ(succ(succ(zero))))), .(succ(succ(succ(succ(succ(succ(zero)))))), .(succ(succ(succ(succ(succ(succ(succ(zero))))))), .(succ(succ(succ(succ(succ(succ(succ(succ(zero)))))))), .(succ(succ(succ(succ(succ(succ(succ(succ(succ(zero))))))))), [])))))))))))) → =\=_IN_GG(S, zero)
U55_AAAAAAAA(S, E, N, D, M, O, R, Y, C1, C2, C3, C4, =\=_out_gg(S, zero)) → U56_AAAAAAAA(S, E, N, D, M, O, R, Y, C1, C2, C3, calc_in_ggggg(C3, S, M, C4, O))
U55_AAAAAAAA(S, E, N, D, M, O, R, Y, C1, C2, C3, C4, =\=_out_gg(S, zero)) → CALC_IN_GGGGG(C3, S, M, C4, O)
CALC_IN_GGGGG(C0, D, E, C1, Y) → U60_GGGGG(C0, D, E, C1, Y, sum_in_gga(C0, D, CD))
CALC_IN_GGGGG(C0, D, E, C1, Y) → SUM_IN_GGA(C0, D, CD)
SUM_IN_GGA(X, Y, Z) → U64_GGA(X, Y, Z, isPlus_in_gga(X, Y, U))
SUM_IN_GGA(X, Y, Z) → ISPLUS_IN_GGA(X, Y, U)
ISPLUS_IN_GGA(succ(X), succ(Y), succ(succ(Z))) → U72_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) → U73_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) → U74_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))) → U75_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)
U64_GGA(X, Y, Z, isPlus_out_gga(X, Y, U)) → U65_GGA(X, Y, Z, =_in_ag(Z, U))
U64_GGA(X, Y, Z, isPlus_out_gga(X, Y, U)) → =_IN_AG(Z, U)
U60_GGGGG(C0, D, E, C1, Y, sum_out_gga(C0, D, CD)) → U61_GGGGG(C0, D, E, C1, Y, sum_in_gga(CD, E, S))
U60_GGGGG(C0, D, E, C1, Y, sum_out_gga(C0, D, CD)) → SUM_IN_GGA(CD, E, S)
U61_GGGGG(C0, D, E, C1, Y, sum_out_gga(CD, E, S)) → U62_GGGGG(C0, D, E, C1, Y, S, carry10_in_ga(C1, C10))
U61_GGGGG(C0, D, E, C1, Y, sum_out_gga(CD, E, S)) → CARRY10_IN_GA(C1, C10)
U62_GGGGG(C0, D, E, C1, Y, S, carry10_out_ga(C1, C10)) → U63_GGGGG(C0, D, E, C1, Y, sum_in_ggg(C10, Y, S))
U62_GGGGG(C0, D, E, C1, Y, S, carry10_out_ga(C1, C10)) → SUM_IN_GGG(C10, Y, S)
SUM_IN_GGG(X, Y, Z) → U64_GGG(X, Y, Z, isPlus_in_gga(X, Y, U))
SUM_IN_GGG(X, Y, Z) → ISPLUS_IN_GGA(X, Y, U)
U64_GGG(X, Y, Z, isPlus_out_gga(X, Y, U)) → U65_GGG(X, Y, Z, =_in_gg(Z, U))
U64_GGG(X, Y, Z, isPlus_out_gga(X, Y, U)) → =_IN_GG(Z, U)
U56_AAAAAAAA(S, E, N, D, M, O, R, Y, C1, C2, C3, calc_out_ggggg(C3, S, M, C4, O)) → U57_AAAAAAAA(S, E, N, D, M, O, R, Y, C1, C2, calc_in_ggggg(C2, E, O, C3, N))
U56_AAAAAAAA(S, E, N, D, M, O, R, Y, C1, C2, C3, calc_out_ggggg(C3, S, M, C4, O)) → CALC_IN_GGGGG(C2, E, O, C3, N)
U57_AAAAAAAA(S, E, N, D, M, O, R, Y, C1, C2, calc_out_ggggg(C2, E, O, C3, N)) → U58_AAAAAAAA(S, E, N, D, M, O, R, Y, C1, calc_in_ggggg(C1, N, R, C2, E))
U57_AAAAAAAA(S, E, N, D, M, O, R, Y, C1, C2, calc_out_ggggg(C2, E, O, C3, N)) → CALC_IN_GGGGG(C1, N, R, C2, E)
U58_AAAAAAAA(S, E, N, D, M, O, R, Y, C1, calc_out_ggggg(C1, N, R, C2, E)) → U59_AAAAAAAA(S, E, N, D, M, O, R, Y, calc_in_ggggg(zero, D, E, C1, Y))
U58_AAAAAAAA(S, E, N, D, M, O, R, Y, C1, calc_out_ggggg(C1, N, R, C2, E)) → CALC_IN_GGGGG(zero, D, E, C1, Y)

The TRS R consists of the following rules:

money_in_aaaaaaaa(S, E, N, D, M, O, R, Y) → U48_aaaaaaaa(S, E, N, D, M, O, R, Y, carry_in_a(C1))
carry_in_a(succ(zero)) → carry_out_a(succ(zero))
carry_in_a(zero) → carry_out_a(zero)
U48_aaaaaaaa(S, E, N, D, M, O, R, Y, carry_out_a(C1)) → U49_aaaaaaaa(S, E, N, D, M, O, R, Y, C1, carry_in_a(C2))
U49_aaaaaaaa(S, E, N, D, M, O, R, Y, C1, carry_out_a(C2)) → U50_aaaaaaaa(S, E, N, D, M, O, R, Y, C1, C2, carry_in_a(C3))
U50_aaaaaaaa(S, E, N, D, M, O, R, Y, C1, C2, carry_out_a(C3)) → U51_aaaaaaaa(S, E, N, D, M, O, R, Y, C1, C2, C3, carry_in_a(C4))
U51_aaaaaaaa(S, E, N, D, M, O, R, Y, C1, C2, C3, carry_out_a(C4)) → U52_aaaaaaaa(S, E, N, D, M, O, R, Y, C1, C2, C3, C4, =_in_ga(C4, M))
=_in_ga(X, X) → =_out_ga(X, X)
U52_aaaaaaaa(S, E, N, D, M, O, R, Y, C1, C2, C3, C4, =_out_ga(C4, M)) → U53_aaaaaaaa(S, E, N, D, M, O, R, Y, C1, C2, C3, C4, =\=_in_gg(M, zero))
=\=_in_gg(X0, X1) → =\=_out_gg(X0, X1)
U53_aaaaaaaa(S, E, N, D, M, O, R, Y, C1, C2, C3, C4, =\=_out_gg(M, zero)) → U54_aaaaaaaa(S, E, N, D, M, O, R, Y, C1, C2, C3, C4, domain_in_ag(.(S, .(E, .(N, .(D, .(M, .(O, .(R, .(Y, [])))))))), .(zero, .(succ(zero), .(succ(succ(zero)), .(succ(succ(succ(zero))), .(succ(succ(succ(succ(zero)))), .(succ(succ(succ(succ(succ(zero))))), .(succ(succ(succ(succ(succ(succ(zero)))))), .(succ(succ(succ(succ(succ(succ(succ(zero))))))), .(succ(succ(succ(succ(succ(succ(succ(succ(zero)))))))), .(succ(succ(succ(succ(succ(succ(succ(succ(succ(zero))))))))), []))))))))))))
domain_in_ag([], X) → domain_out_ag([], X)
domain_in_ag(.(X1, R), L) → U66_ag(X1, R, L, del_in_aga(X1, L, NL))
del_in_aga(X, .(X, T), T) → del_out_aga(X, .(X, T), T)
del_in_aga(X, .(Y, T), .(Y, NT)) → U68_aga(X, Y, T, NT, del_in_aga(X, T, NT))
U68_aga(X, Y, T, NT, del_out_aga(X, T, NT)) → del_out_aga(X, .(Y, T), .(Y, NT))
U66_ag(X1, R, L, del_out_aga(X1, L, NL)) → U67_ag(X1, R, L, domain_in_ag(R, NL))
U67_ag(X1, R, L, domain_out_ag(R, NL)) → domain_out_ag(.(X1, R), L)
U54_aaaaaaaa(S, E, N, D, M, O, R, Y, C1, C2, C3, C4, domain_out_ag(.(S, .(E, .(N, .(D, .(M, .(O, .(R, .(Y, [])))))))), .(zero, .(succ(zero), .(succ(succ(zero)), .(succ(succ(succ(zero))), .(succ(succ(succ(succ(zero)))), .(succ(succ(succ(succ(succ(zero))))), .(succ(succ(succ(succ(succ(succ(zero)))))), .(succ(succ(succ(succ(succ(succ(succ(zero))))))), .(succ(succ(succ(succ(succ(succ(succ(succ(zero)))))))), .(succ(succ(succ(succ(succ(succ(succ(succ(succ(zero))))))))), [])))))))))))) → U55_aaaaaaaa(S, E, N, D, M, O, R, Y, C1, C2, C3, C4, =\=_in_gg(S, zero))
U55_aaaaaaaa(S, E, N, D, M, O, R, Y, C1, C2, C3, C4, =\=_out_gg(S, zero)) → U56_aaaaaaaa(S, E, N, D, M, O, R, Y, C1, C2, C3, calc_in_ggggg(C3, S, M, C4, O))
calc_in_ggggg(C0, D, E, C1, Y) → U60_ggggg(C0, D, E, C1, Y, sum_in_gga(C0, D, CD))
sum_in_gga(X, Y, Z) → U64_gga(X, Y, Z, isPlus_in_gga(X, Y, U))
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))) → U72_gga(X, Y, Z, isPlus_in_gga(X, Y, Z))
isPlus_in_gga(succ(X), pred(Y), Z) → U73_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) → U74_gga(X, Y, Z, isPlus_in_gga(X, Y, Z))
isPlus_in_gga(pred(X), pred(Y), pred(pred(Z))) → U75_gga(X, Y, Z, isPlus_in_gga(X, Y, Z))
U75_gga(X, Y, Z, isPlus_out_gga(X, Y, Z)) → isPlus_out_gga(pred(X), pred(Y), pred(pred(Z)))
U74_gga(X, Y, Z, isPlus_out_gga(X, Y, Z)) → isPlus_out_gga(pred(X), succ(Y), Z)
U73_gga(X, Y, Z, isPlus_out_gga(X, Y, Z)) → isPlus_out_gga(succ(X), pred(Y), Z)
U72_gga(X, Y, Z, isPlus_out_gga(X, Y, Z)) → isPlus_out_gga(succ(X), succ(Y), succ(succ(Z)))
U64_gga(X, Y, Z, isPlus_out_gga(X, Y, U)) → U65_gga(X, Y, Z, =_in_ag(Z, U))
=_in_ag(X, X) → =_out_ag(X, X)
U65_gga(X, Y, Z, =_out_ag(Z, U)) → sum_out_gga(X, Y, Z)
U60_ggggg(C0, D, E, C1, Y, sum_out_gga(C0, D, CD)) → U61_ggggg(C0, D, E, C1, Y, sum_in_gga(CD, E, S))
U61_ggggg(C0, D, E, C1, Y, sum_out_gga(CD, E, S)) → U62_ggggg(C0, D, E, C1, Y, S, carry10_in_ga(C1, C10))
carry10_in_ga(zero, zero) → carry10_out_ga(zero, zero)
carry10_in_ga(succ(zero), succ(succ(succ(succ(succ(succ(succ(succ(succ(succ(zero))))))))))) → carry10_out_ga(succ(zero), succ(succ(succ(succ(succ(succ(succ(succ(succ(succ(zero)))))))))))
U62_ggggg(C0, D, E, C1, Y, S, carry10_out_ga(C1, C10)) → U63_ggggg(C0, D, E, C1, Y, sum_in_ggg(C10, Y, S))
sum_in_ggg(X, Y, Z) → U64_ggg(X, Y, Z, isPlus_in_gga(X, Y, U))
U64_ggg(X, Y, Z, isPlus_out_gga(X, Y, U)) → U65_ggg(X, Y, Z, =_in_gg(Z, U))
=_in_gg(X, X) → =_out_gg(X, X)
U65_ggg(X, Y, Z, =_out_gg(Z, U)) → sum_out_ggg(X, Y, Z)
U63_ggggg(C0, D, E, C1, Y, sum_out_ggg(C10, Y, S)) → calc_out_ggggg(C0, D, E, C1, Y)
U56_aaaaaaaa(S, E, N, D, M, O, R, Y, C1, C2, C3, calc_out_ggggg(C3, S, M, C4, O)) → U57_aaaaaaaa(S, E, N, D, M, O, R, Y, C1, C2, calc_in_ggggg(C2, E, O, C3, N))
U57_aaaaaaaa(S, E, N, D, M, O, R, Y, C1, C2, calc_out_ggggg(C2, E, O, C3, N)) → U58_aaaaaaaa(S, E, N, D, M, O, R, Y, C1, calc_in_ggggg(C1, N, R, C2, E))
U58_aaaaaaaa(S, E, N, D, M, O, R, Y, C1, calc_out_ggggg(C1, N, R, C2, E)) → U59_aaaaaaaa(S, E, N, D, M, O, R, Y, calc_in_ggggg(zero, D, E, C1, Y))
U59_aaaaaaaa(S, E, N, D, M, O, R, Y, calc_out_ggggg(zero, D, E, C1, Y)) → money_out_aaaaaaaa(S, E, N, D, M, O, R, Y)

The argument filtering Pi contains the following mapping:
money_in_aaaaaaaa(x1, x2, x3, x4, x5, x6, x7, x8)  =  money_in_aaaaaaaa
U48_aaaaaaaa(x1, x2, x3, x4, x5, x6, x7, x8, x9)  =  U48_aaaaaaaa(x9)
carry_in_a(x1)  =  carry_in_a
carry_out_a(x1)  =  carry_out_a(x1)
U49_aaaaaaaa(x1, x2, x3, x4, x5, x6, x7, x8, x9, x10)  =  U49_aaaaaaaa(x9, x10)
U50_aaaaaaaa(x1, x2, x3, x4, x5, x6, x7, x8, x9, x10, x11)  =  U50_aaaaaaaa(x9, x10, x11)
U51_aaaaaaaa(x1, x2, x3, x4, x5, x6, x7, x8, x9, x10, x11, x12)  =  U51_aaaaaaaa(x9, x10, x11, x12)
U52_aaaaaaaa(x1, x2, x3, x4, x5, x6, x7, x8, x9, x10, x11, x12, x13)  =  U52_aaaaaaaa(x9, x10, x11, x12, x13)
=_in_ga(x1, x2)  =  =_in_ga(x1)
=_out_ga(x1, x2)  =  =_out_ga(x2)
U53_aaaaaaaa(x1, x2, x3, x4, x5, x6, x7, x8, x9, x10, x11, x12, x13)  =  U53_aaaaaaaa(x5, x9, x10, x11, x12, x13)
=\=_in_gg(x1, x2)  =  =\=_in_gg(x1, x2)
=\=_out_gg(x1, x2)  =  =\=_out_gg
zero  =  zero
U54_aaaaaaaa(x1, x2, x3, x4, x5, x6, x7, x8, x9, x10, x11, x12, x13)  =  U54_aaaaaaaa(x5, x9, x10, x11, x12, x13)
domain_in_ag(x1, x2)  =  domain_in_ag(x2)
domain_out_ag(x1, x2)  =  domain_out_ag(x1)
U66_ag(x1, x2, x3, x4)  =  U66_ag(x4)
del_in_aga(x1, x2, x3)  =  del_in_aga(x2)
.(x1, x2)  =  .(x1, x2)
del_out_aga(x1, x2, x3)  =  del_out_aga(x1, x3)
U68_aga(x1, x2, x3, x4, x5)  =  U68_aga(x2, x5)
U67_ag(x1, x2, x3, x4)  =  U67_ag(x1, x4)
[]  =  []
succ(x1)  =  succ(x1)
U55_aaaaaaaa(x1, x2, x3, x4, x5, x6, x7, x8, x9, x10, x11, x12, x13)  =  U55_aaaaaaaa(x1, x2, x3, x4, x5, x6, x7, x8, x9, x10, x11, x12, x13)
U56_aaaaaaaa(x1, x2, x3, x4, x5, x6, x7, x8, x9, x10, x11, x12)  =  U56_aaaaaaaa(x1, x2, x3, x4, x5, x6, x7, x8, x9, x10, x11, x12)
calc_in_ggggg(x1, x2, x3, x4, x5)  =  calc_in_ggggg(x1, x2, x3, x4, x5)
U60_ggggg(x1, x2, x3, x4, x5, x6)  =  U60_ggggg(x3, x4, x5, x6)
sum_in_gga(x1, x2, x3)  =  sum_in_gga(x1, x2)
U64_gga(x1, x2, x3, x4)  =  U64_gga(x4)
isPlus_in_gga(x1, x2, x3)  =  isPlus_in_gga(x1, x2)
isPlus_out_gga(x1, x2, x3)  =  isPlus_out_gga(x3)
U72_gga(x1, x2, x3, x4)  =  U72_gga(x4)
pred(x1)  =  pred(x1)
U73_gga(x1, x2, x3, x4)  =  U73_gga(x4)
U74_gga(x1, x2, x3, x4)  =  U74_gga(x4)
U75_gga(x1, x2, x3, x4)  =  U75_gga(x4)
U65_gga(x1, x2, x3, x4)  =  U65_gga(x4)
=_in_ag(x1, x2)  =  =_in_ag(x2)
=_out_ag(x1, x2)  =  =_out_ag(x1)
sum_out_gga(x1, x2, x3)  =  sum_out_gga(x3)
U61_ggggg(x1, x2, x3, x4, x5, x6)  =  U61_ggggg(x4, x5, x6)
U62_ggggg(x1, x2, x3, x4, x5, x6, x7)  =  U62_ggggg(x5, x6, x7)
carry10_in_ga(x1, x2)  =  carry10_in_ga(x1)
carry10_out_ga(x1, x2)  =  carry10_out_ga(x2)
U63_ggggg(x1, x2, x3, x4, x5, x6)  =  U63_ggggg(x6)
sum_in_ggg(x1, x2, x3)  =  sum_in_ggg(x1, x2, x3)
U64_ggg(x1, x2, x3, x4)  =  U64_ggg(x3, x4)
U65_ggg(x1, x2, x3, x4)  =  U65_ggg(x4)
=_in_gg(x1, x2)  =  =_in_gg(x1, x2)
=_out_gg(x1, x2)  =  =_out_gg
sum_out_ggg(x1, x2, x3)  =  sum_out_ggg
calc_out_ggggg(x1, x2, x3, x4, x5)  =  calc_out_ggggg
U57_aaaaaaaa(x1, x2, x3, x4, x5, x6, x7, x8, x9, x10, x11)  =  U57_aaaaaaaa(x1, x2, x3, x4, x5, x6, x7, x8, x9, x10, x11)
U58_aaaaaaaa(x1, x2, x3, x4, x5, x6, x7, x8, x9, x10)  =  U58_aaaaaaaa(x1, x2, x3, x4, x5, x6, x7, x8, x9, x10)
U59_aaaaaaaa(x1, x2, x3, x4, x5, x6, x7, x8, x9)  =  U59_aaaaaaaa(x1, x2, x3, x4, x5, x6, x7, x8, x9)
money_out_aaaaaaaa(x1, x2, x3, x4, x5, x6, x7, x8)  =  money_out_aaaaaaaa(x1, x2, x3, x4, x5, x6, x7, x8)
MONEY_IN_AAAAAAAA(x1, x2, x3, x4, x5, x6, x7, x8)  =  MONEY_IN_AAAAAAAA
U50_AAAAAAAA(x1, x2, x3, x4, x5, x6, x7, x8, x9, x10, x11)  =  U50_AAAAAAAA(x9, x10, x11)
U54_AAAAAAAA(x1, x2, x3, x4, x5, x6, x7, x8, x9, x10, x11, x12, x13)  =  U54_AAAAAAAA(x5, x9, x10, x11, x12, x13)
=_IN_GG(x1, x2)  =  =_IN_GG(x1, x2)
U74_GGA(x1, x2, x3, x4)  =  U74_GGA(x4)
CARRY_IN_A(x1)  =  CARRY_IN_A
U68_AGA(x1, x2, x3, x4, x5)  =  U68_AGA(x2, x5)
U60_GGGGG(x1, x2, x3, x4, x5, x6)  =  U60_GGGGG(x3, x4, x5, x6)
U57_AAAAAAAA(x1, x2, x3, x4, x5, x6, x7, x8, x9, x10, x11)  =  U57_AAAAAAAA(x1, x2, x3, x4, x5, x6, x7, x8, x9, x10, x11)
U63_GGGGG(x1, x2, x3, x4, x5, x6)  =  U63_GGGGG(x6)
U65_GGG(x1, x2, x3, x4)  =  U65_GGG(x4)
CALC_IN_GGGGG(x1, x2, x3, x4, x5)  =  CALC_IN_GGGGG(x1, x2, x3, x4, x5)
DEL_IN_AGA(x1, x2, x3)  =  DEL_IN_AGA(x2)
U72_GGA(x1, x2, x3, x4)  =  U72_GGA(x4)
=_IN_AG(x1, x2)  =  =_IN_AG(x2)
U62_GGGGG(x1, x2, x3, x4, x5, x6, x7)  =  U62_GGGGG(x5, x6, x7)
U52_AAAAAAAA(x1, x2, x3, x4, x5, x6, x7, x8, x9, x10, x11, x12, x13)  =  U52_AAAAAAAA(x9, x10, x11, x12, x13)
U59_AAAAAAAA(x1, x2, x3, x4, x5, x6, x7, x8, x9)  =  U59_AAAAAAAA(x1, x2, x3, x4, x5, x6, x7, x8, x9)
U66_AG(x1, x2, x3, x4)  =  U66_AG(x4)
U48_AAAAAAAA(x1, x2, x3, x4, x5, x6, x7, x8, x9)  =  U48_AAAAAAAA(x9)
U65_GGA(x1, x2, x3, x4)  =  U65_GGA(x4)
SUM_IN_GGG(x1, x2, x3)  =  SUM_IN_GGG(x1, x2, x3)
U56_AAAAAAAA(x1, x2, x3, x4, x5, x6, x7, x8, x9, x10, x11, x12)  =  U56_AAAAAAAA(x1, x2, x3, x4, x5, x6, x7, x8, x9, x10, x11, x12)
U58_AAAAAAAA(x1, x2, x3, x4, x5, x6, x7, x8, x9, x10)  =  U58_AAAAAAAA(x1, x2, x3, x4, x5, x6, x7, x8, x9, x10)
U55_AAAAAAAA(x1, x2, x3, x4, x5, x6, x7, x8, x9, x10, x11, x12, x13)  =  U55_AAAAAAAA(x1, x2, x3, x4, x5, x6, x7, x8, x9, x10, x11, x12, x13)
CARRY10_IN_GA(x1, x2)  =  CARRY10_IN_GA(x1)
ISPLUS_IN_GGA(x1, x2, x3)  =  ISPLUS_IN_GGA(x1, x2)
U53_AAAAAAAA(x1, x2, x3, x4, x5, x6, x7, x8, x9, x10, x11, x12, x13)  =  U53_AAAAAAAA(x5, x9, x10, x11, x12, x13)
DOMAIN_IN_AG(x1, x2)  =  DOMAIN_IN_AG(x2)
U51_AAAAAAAA(x1, x2, x3, x4, x5, x6, x7, x8, x9, x10, x11, x12)  =  U51_AAAAAAAA(x9, x10, x11, x12)
U64_GGA(x1, x2, x3, x4)  =  U64_GGA(x4)
U75_GGA(x1, x2, x3, x4)  =  U75_GGA(x4)
U67_AG(x1, x2, x3, x4)  =  U67_AG(x1, x4)
=_IN_GA(x1, x2)  =  =_IN_GA(x1)
=\=_IN_GG(x1, x2)  =  =\=_IN_GG(x1, x2)
SUM_IN_GGA(x1, x2, x3)  =  SUM_IN_GGA(x1, x2)
U73_GGA(x1, x2, x3, x4)  =  U73_GGA(x4)
U64_GGG(x1, x2, x3, x4)  =  U64_GGG(x3, x4)
U61_GGGGG(x1, x2, x3, x4, x5, x6)  =  U61_GGGGG(x4, x5, x6)
U49_AAAAAAAA(x1, x2, x3, x4, x5, x6, x7, x8, x9, x10)  =  U49_AAAAAAAA(x9, x10)

We have to consider all (P,R,Pi)-chains
The approximation of the Dependency Graph [30] contains 3 SCCs with 47 less nodes.

↳ Prolog
  ↳ PredefinedPredicateTransformerProof
    ↳ Prolog
      ↳ CutEliminatorProof
        ↳ Prolog
          ↳ UndefinedPredicateHandlerProof
            ↳ Prolog
              ↳ PrologToPiTRSProof
                ↳ PiTRS
                  ↳ DependencyPairsProof
                    ↳ PiDP
                      ↳ DependencyGraphProof
                        ↳ AND
                          ↳ PiDP
                            ↳ UsableRulesProof
                          ↳ 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:

money_in_aaaaaaaa(S, E, N, D, M, O, R, Y) → U48_aaaaaaaa(S, E, N, D, M, O, R, Y, carry_in_a(C1))
carry_in_a(succ(zero)) → carry_out_a(succ(zero))
carry_in_a(zero) → carry_out_a(zero)
U48_aaaaaaaa(S, E, N, D, M, O, R, Y, carry_out_a(C1)) → U49_aaaaaaaa(S, E, N, D, M, O, R, Y, C1, carry_in_a(C2))
U49_aaaaaaaa(S, E, N, D, M, O, R, Y, C1, carry_out_a(C2)) → U50_aaaaaaaa(S, E, N, D, M, O, R, Y, C1, C2, carry_in_a(C3))
U50_aaaaaaaa(S, E, N, D, M, O, R, Y, C1, C2, carry_out_a(C3)) → U51_aaaaaaaa(S, E, N, D, M, O, R, Y, C1, C2, C3, carry_in_a(C4))
U51_aaaaaaaa(S, E, N, D, M, O, R, Y, C1, C2, C3, carry_out_a(C4)) → U52_aaaaaaaa(S, E, N, D, M, O, R, Y, C1, C2, C3, C4, =_in_ga(C4, M))
=_in_ga(X, X) → =_out_ga(X, X)
U52_aaaaaaaa(S, E, N, D, M, O, R, Y, C1, C2, C3, C4, =_out_ga(C4, M)) → U53_aaaaaaaa(S, E, N, D, M, O, R, Y, C1, C2, C3, C4, =\=_in_gg(M, zero))
=\=_in_gg(X0, X1) → =\=_out_gg(X0, X1)
U53_aaaaaaaa(S, E, N, D, M, O, R, Y, C1, C2, C3, C4, =\=_out_gg(M, zero)) → U54_aaaaaaaa(S, E, N, D, M, O, R, Y, C1, C2, C3, C4, domain_in_ag(.(S, .(E, .(N, .(D, .(M, .(O, .(R, .(Y, [])))))))), .(zero, .(succ(zero), .(succ(succ(zero)), .(succ(succ(succ(zero))), .(succ(succ(succ(succ(zero)))), .(succ(succ(succ(succ(succ(zero))))), .(succ(succ(succ(succ(succ(succ(zero)))))), .(succ(succ(succ(succ(succ(succ(succ(zero))))))), .(succ(succ(succ(succ(succ(succ(succ(succ(zero)))))))), .(succ(succ(succ(succ(succ(succ(succ(succ(succ(zero))))))))), []))))))))))))
domain_in_ag([], X) → domain_out_ag([], X)
domain_in_ag(.(X1, R), L) → U66_ag(X1, R, L, del_in_aga(X1, L, NL))
del_in_aga(X, .(X, T), T) → del_out_aga(X, .(X, T), T)
del_in_aga(X, .(Y, T), .(Y, NT)) → U68_aga(X, Y, T, NT, del_in_aga(X, T, NT))
U68_aga(X, Y, T, NT, del_out_aga(X, T, NT)) → del_out_aga(X, .(Y, T), .(Y, NT))
U66_ag(X1, R, L, del_out_aga(X1, L, NL)) → U67_ag(X1, R, L, domain_in_ag(R, NL))
U67_ag(X1, R, L, domain_out_ag(R, NL)) → domain_out_ag(.(X1, R), L)
U54_aaaaaaaa(S, E, N, D, M, O, R, Y, C1, C2, C3, C4, domain_out_ag(.(S, .(E, .(N, .(D, .(M, .(O, .(R, .(Y, [])))))))), .(zero, .(succ(zero), .(succ(succ(zero)), .(succ(succ(succ(zero))), .(succ(succ(succ(succ(zero)))), .(succ(succ(succ(succ(succ(zero))))), .(succ(succ(succ(succ(succ(succ(zero)))))), .(succ(succ(succ(succ(succ(succ(succ(zero))))))), .(succ(succ(succ(succ(succ(succ(succ(succ(zero)))))))), .(succ(succ(succ(succ(succ(succ(succ(succ(succ(zero))))))))), [])))))))))))) → U55_aaaaaaaa(S, E, N, D, M, O, R, Y, C1, C2, C3, C4, =\=_in_gg(S, zero))
U55_aaaaaaaa(S, E, N, D, M, O, R, Y, C1, C2, C3, C4, =\=_out_gg(S, zero)) → U56_aaaaaaaa(S, E, N, D, M, O, R, Y, C1, C2, C3, calc_in_ggggg(C3, S, M, C4, O))
calc_in_ggggg(C0, D, E, C1, Y) → U60_ggggg(C0, D, E, C1, Y, sum_in_gga(C0, D, CD))
sum_in_gga(X, Y, Z) → U64_gga(X, Y, Z, isPlus_in_gga(X, Y, U))
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))) → U72_gga(X, Y, Z, isPlus_in_gga(X, Y, Z))
isPlus_in_gga(succ(X), pred(Y), Z) → U73_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) → U74_gga(X, Y, Z, isPlus_in_gga(X, Y, Z))
isPlus_in_gga(pred(X), pred(Y), pred(pred(Z))) → U75_gga(X, Y, Z, isPlus_in_gga(X, Y, Z))
U75_gga(X, Y, Z, isPlus_out_gga(X, Y, Z)) → isPlus_out_gga(pred(X), pred(Y), pred(pred(Z)))
U74_gga(X, Y, Z, isPlus_out_gga(X, Y, Z)) → isPlus_out_gga(pred(X), succ(Y), Z)
U73_gga(X, Y, Z, isPlus_out_gga(X, Y, Z)) → isPlus_out_gga(succ(X), pred(Y), Z)
U72_gga(X, Y, Z, isPlus_out_gga(X, Y, Z)) → isPlus_out_gga(succ(X), succ(Y), succ(succ(Z)))
U64_gga(X, Y, Z, isPlus_out_gga(X, Y, U)) → U65_gga(X, Y, Z, =_in_ag(Z, U))
=_in_ag(X, X) → =_out_ag(X, X)
U65_gga(X, Y, Z, =_out_ag(Z, U)) → sum_out_gga(X, Y, Z)
U60_ggggg(C0, D, E, C1, Y, sum_out_gga(C0, D, CD)) → U61_ggggg(C0, D, E, C1, Y, sum_in_gga(CD, E, S))
U61_ggggg(C0, D, E, C1, Y, sum_out_gga(CD, E, S)) → U62_ggggg(C0, D, E, C1, Y, S, carry10_in_ga(C1, C10))
carry10_in_ga(zero, zero) → carry10_out_ga(zero, zero)
carry10_in_ga(succ(zero), succ(succ(succ(succ(succ(succ(succ(succ(succ(succ(zero))))))))))) → carry10_out_ga(succ(zero), succ(succ(succ(succ(succ(succ(succ(succ(succ(succ(zero)))))))))))
U62_ggggg(C0, D, E, C1, Y, S, carry10_out_ga(C1, C10)) → U63_ggggg(C0, D, E, C1, Y, sum_in_ggg(C10, Y, S))
sum_in_ggg(X, Y, Z) → U64_ggg(X, Y, Z, isPlus_in_gga(X, Y, U))
U64_ggg(X, Y, Z, isPlus_out_gga(X, Y, U)) → U65_ggg(X, Y, Z, =_in_gg(Z, U))
=_in_gg(X, X) → =_out_gg(X, X)
U65_ggg(X, Y, Z, =_out_gg(Z, U)) → sum_out_ggg(X, Y, Z)
U63_ggggg(C0, D, E, C1, Y, sum_out_ggg(C10, Y, S)) → calc_out_ggggg(C0, D, E, C1, Y)
U56_aaaaaaaa(S, E, N, D, M, O, R, Y, C1, C2, C3, calc_out_ggggg(C3, S, M, C4, O)) → U57_aaaaaaaa(S, E, N, D, M, O, R, Y, C1, C2, calc_in_ggggg(C2, E, O, C3, N))
U57_aaaaaaaa(S, E, N, D, M, O, R, Y, C1, C2, calc_out_ggggg(C2, E, O, C3, N)) → U58_aaaaaaaa(S, E, N, D, M, O, R, Y, C1, calc_in_ggggg(C1, N, R, C2, E))
U58_aaaaaaaa(S, E, N, D, M, O, R, Y, C1, calc_out_ggggg(C1, N, R, C2, E)) → U59_aaaaaaaa(S, E, N, D, M, O, R, Y, calc_in_ggggg(zero, D, E, C1, Y))
U59_aaaaaaaa(S, E, N, D, M, O, R, Y, calc_out_ggggg(zero, D, E, C1, Y)) → money_out_aaaaaaaa(S, E, N, D, M, O, R, Y)

The argument filtering Pi contains the following mapping:
money_in_aaaaaaaa(x1, x2, x3, x4, x5, x6, x7, x8)  =  money_in_aaaaaaaa
U48_aaaaaaaa(x1, x2, x3, x4, x5, x6, x7, x8, x9)  =  U48_aaaaaaaa(x9)
carry_in_a(x1)  =  carry_in_a
carry_out_a(x1)  =  carry_out_a(x1)
U49_aaaaaaaa(x1, x2, x3, x4, x5, x6, x7, x8, x9, x10)  =  U49_aaaaaaaa(x9, x10)
U50_aaaaaaaa(x1, x2, x3, x4, x5, x6, x7, x8, x9, x10, x11)  =  U50_aaaaaaaa(x9, x10, x11)
U51_aaaaaaaa(x1, x2, x3, x4, x5, x6, x7, x8, x9, x10, x11, x12)  =  U51_aaaaaaaa(x9, x10, x11, x12)
U52_aaaaaaaa(x1, x2, x3, x4, x5, x6, x7, x8, x9, x10, x11, x12, x13)  =  U52_aaaaaaaa(x9, x10, x11, x12, x13)
=_in_ga(x1, x2)  =  =_in_ga(x1)
=_out_ga(x1, x2)  =  =_out_ga(x2)
U53_aaaaaaaa(x1, x2, x3, x4, x5, x6, x7, x8, x9, x10, x11, x12, x13)  =  U53_aaaaaaaa(x5, x9, x10, x11, x12, x13)
=\=_in_gg(x1, x2)  =  =\=_in_gg(x1, x2)
=\=_out_gg(x1, x2)  =  =\=_out_gg
zero  =  zero
U54_aaaaaaaa(x1, x2, x3, x4, x5, x6, x7, x8, x9, x10, x11, x12, x13)  =  U54_aaaaaaaa(x5, x9, x10, x11, x12, x13)
domain_in_ag(x1, x2)  =  domain_in_ag(x2)
domain_out_ag(x1, x2)  =  domain_out_ag(x1)
U66_ag(x1, x2, x3, x4)  =  U66_ag(x4)
del_in_aga(x1, x2, x3)  =  del_in_aga(x2)
.(x1, x2)  =  .(x1, x2)
del_out_aga(x1, x2, x3)  =  del_out_aga(x1, x3)
U68_aga(x1, x2, x3, x4, x5)  =  U68_aga(x2, x5)
U67_ag(x1, x2, x3, x4)  =  U67_ag(x1, x4)
[]  =  []
succ(x1)  =  succ(x1)
U55_aaaaaaaa(x1, x2, x3, x4, x5, x6, x7, x8, x9, x10, x11, x12, x13)  =  U55_aaaaaaaa(x1, x2, x3, x4, x5, x6, x7, x8, x9, x10, x11, x12, x13)
U56_aaaaaaaa(x1, x2, x3, x4, x5, x6, x7, x8, x9, x10, x11, x12)  =  U56_aaaaaaaa(x1, x2, x3, x4, x5, x6, x7, x8, x9, x10, x11, x12)
calc_in_ggggg(x1, x2, x3, x4, x5)  =  calc_in_ggggg(x1, x2, x3, x4, x5)
U60_ggggg(x1, x2, x3, x4, x5, x6)  =  U60_ggggg(x3, x4, x5, x6)
sum_in_gga(x1, x2, x3)  =  sum_in_gga(x1, x2)
U64_gga(x1, x2, x3, x4)  =  U64_gga(x4)
isPlus_in_gga(x1, x2, x3)  =  isPlus_in_gga(x1, x2)
isPlus_out_gga(x1, x2, x3)  =  isPlus_out_gga(x3)
U72_gga(x1, x2, x3, x4)  =  U72_gga(x4)
pred(x1)  =  pred(x1)
U73_gga(x1, x2, x3, x4)  =  U73_gga(x4)
U74_gga(x1, x2, x3, x4)  =  U74_gga(x4)
U75_gga(x1, x2, x3, x4)  =  U75_gga(x4)
U65_gga(x1, x2, x3, x4)  =  U65_gga(x4)
=_in_ag(x1, x2)  =  =_in_ag(x2)
=_out_ag(x1, x2)  =  =_out_ag(x1)
sum_out_gga(x1, x2, x3)  =  sum_out_gga(x3)
U61_ggggg(x1, x2, x3, x4, x5, x6)  =  U61_ggggg(x4, x5, x6)
U62_ggggg(x1, x2, x3, x4, x5, x6, x7)  =  U62_ggggg(x5, x6, x7)
carry10_in_ga(x1, x2)  =  carry10_in_ga(x1)
carry10_out_ga(x1, x2)  =  carry10_out_ga(x2)
U63_ggggg(x1, x2, x3, x4, x5, x6)  =  U63_ggggg(x6)
sum_in_ggg(x1, x2, x3)  =  sum_in_ggg(x1, x2, x3)
U64_ggg(x1, x2, x3, x4)  =  U64_ggg(x3, x4)
U65_ggg(x1, x2, x3, x4)  =  U65_ggg(x4)
=_in_gg(x1, x2)  =  =_in_gg(x1, x2)
=_out_gg(x1, x2)  =  =_out_gg
sum_out_ggg(x1, x2, x3)  =  sum_out_ggg
calc_out_ggggg(x1, x2, x3, x4, x5)  =  calc_out_ggggg
U57_aaaaaaaa(x1, x2, x3, x4, x5, x6, x7, x8, x9, x10, x11)  =  U57_aaaaaaaa(x1, x2, x3, x4, x5, x6, x7, x8, x9, x10, x11)
U58_aaaaaaaa(x1, x2, x3, x4, x5, x6, x7, x8, x9, x10)  =  U58_aaaaaaaa(x1, x2, x3, x4, x5, x6, x7, x8, x9, x10)
U59_aaaaaaaa(x1, x2, x3, x4, x5, x6, x7, x8, x9)  =  U59_aaaaaaaa(x1, x2, x3, x4, x5, x6, x7, x8, x9)
money_out_aaaaaaaa(x1, x2, x3, x4, x5, x6, x7, x8)  =  money_out_aaaaaaaa(x1, x2, x3, x4, x5, x6, x7, x8)
ISPLUS_IN_GGA(x1, x2, x3)  =  ISPLUS_IN_GGA(x1, x2)

We have to consider all (P,R,Pi)-chains
For (infinitary) constructor rewriting [30] we can delete all non-usable rules from R.

↳ Prolog
  ↳ PredefinedPredicateTransformerProof
    ↳ Prolog
      ↳ CutEliminatorProof
        ↳ Prolog
          ↳ UndefinedPredicateHandlerProof
            ↳ Prolog
              ↳ PrologToPiTRSProof
                ↳ PiTRS
                  ↳ DependencyPairsProof
                    ↳ PiDP
                      ↳ DependencyGraphProof
                        ↳ AND
                          ↳ PiDP
                            ↳ UsableRulesProof
                              ↳ PiDP
                                ↳ PiDPToQDPProof
                          ↳ 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
      ↳ CutEliminatorProof
        ↳ Prolog
          ↳ UndefinedPredicateHandlerProof
            ↳ Prolog
              ↳ PrologToPiTRSProof
                ↳ PiTRS
                  ↳ DependencyPairsProof
                    ↳ PiDP
                      ↳ DependencyGraphProof
                        ↳ AND
                          ↳ PiDP
                            ↳ UsableRulesProof
                              ↳ PiDP
                                ↳ PiDPToQDPProof
                                  ↳ QDP
                                    ↳ QDPSizeChangeProof
                          ↳ 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)

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: 



↳ Prolog
  ↳ PredefinedPredicateTransformerProof
    ↳ Prolog
      ↳ CutEliminatorProof
        ↳ Prolog
          ↳ UndefinedPredicateHandlerProof
            ↳ Prolog
              ↳ PrologToPiTRSProof
                ↳ PiTRS
                  ↳ DependencyPairsProof
                    ↳ PiDP
                      ↳ DependencyGraphProof
                        ↳ AND
                          ↳ PiDP
                          ↳ PiDP
                            ↳ UsableRulesProof
                          ↳ PiDP

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

DEL_IN_AGA(X, .(Y, T), .(Y, NT)) → DEL_IN_AGA(X, T, NT)

The TRS R consists of the following rules:

money_in_aaaaaaaa(S, E, N, D, M, O, R, Y) → U48_aaaaaaaa(S, E, N, D, M, O, R, Y, carry_in_a(C1))
carry_in_a(succ(zero)) → carry_out_a(succ(zero))
carry_in_a(zero) → carry_out_a(zero)
U48_aaaaaaaa(S, E, N, D, M, O, R, Y, carry_out_a(C1)) → U49_aaaaaaaa(S, E, N, D, M, O, R, Y, C1, carry_in_a(C2))
U49_aaaaaaaa(S, E, N, D, M, O, R, Y, C1, carry_out_a(C2)) → U50_aaaaaaaa(S, E, N, D, M, O, R, Y, C1, C2, carry_in_a(C3))
U50_aaaaaaaa(S, E, N, D, M, O, R, Y, C1, C2, carry_out_a(C3)) → U51_aaaaaaaa(S, E, N, D, M, O, R, Y, C1, C2, C3, carry_in_a(C4))
U51_aaaaaaaa(S, E, N, D, M, O, R, Y, C1, C2, C3, carry_out_a(C4)) → U52_aaaaaaaa(S, E, N, D, M, O, R, Y, C1, C2, C3, C4, =_in_ga(C4, M))
=_in_ga(X, X) → =_out_ga(X, X)
U52_aaaaaaaa(S, E, N, D, M, O, R, Y, C1, C2, C3, C4, =_out_ga(C4, M)) → U53_aaaaaaaa(S, E, N, D, M, O, R, Y, C1, C2, C3, C4, =\=_in_gg(M, zero))
=\=_in_gg(X0, X1) → =\=_out_gg(X0, X1)
U53_aaaaaaaa(S, E, N, D, M, O, R, Y, C1, C2, C3, C4, =\=_out_gg(M, zero)) → U54_aaaaaaaa(S, E, N, D, M, O, R, Y, C1, C2, C3, C4, domain_in_ag(.(S, .(E, .(N, .(D, .(M, .(O, .(R, .(Y, [])))))))), .(zero, .(succ(zero), .(succ(succ(zero)), .(succ(succ(succ(zero))), .(succ(succ(succ(succ(zero)))), .(succ(succ(succ(succ(succ(zero))))), .(succ(succ(succ(succ(succ(succ(zero)))))), .(succ(succ(succ(succ(succ(succ(succ(zero))))))), .(succ(succ(succ(succ(succ(succ(succ(succ(zero)))))))), .(succ(succ(succ(succ(succ(succ(succ(succ(succ(zero))))))))), []))))))))))))
domain_in_ag([], X) → domain_out_ag([], X)
domain_in_ag(.(X1, R), L) → U66_ag(X1, R, L, del_in_aga(X1, L, NL))
del_in_aga(X, .(X, T), T) → del_out_aga(X, .(X, T), T)
del_in_aga(X, .(Y, T), .(Y, NT)) → U68_aga(X, Y, T, NT, del_in_aga(X, T, NT))
U68_aga(X, Y, T, NT, del_out_aga(X, T, NT)) → del_out_aga(X, .(Y, T), .(Y, NT))
U66_ag(X1, R, L, del_out_aga(X1, L, NL)) → U67_ag(X1, R, L, domain_in_ag(R, NL))
U67_ag(X1, R, L, domain_out_ag(R, NL)) → domain_out_ag(.(X1, R), L)
U54_aaaaaaaa(S, E, N, D, M, O, R, Y, C1, C2, C3, C4, domain_out_ag(.(S, .(E, .(N, .(D, .(M, .(O, .(R, .(Y, [])))))))), .(zero, .(succ(zero), .(succ(succ(zero)), .(succ(succ(succ(zero))), .(succ(succ(succ(succ(zero)))), .(succ(succ(succ(succ(succ(zero))))), .(succ(succ(succ(succ(succ(succ(zero)))))), .(succ(succ(succ(succ(succ(succ(succ(zero))))))), .(succ(succ(succ(succ(succ(succ(succ(succ(zero)))))))), .(succ(succ(succ(succ(succ(succ(succ(succ(succ(zero))))))))), [])))))))))))) → U55_aaaaaaaa(S, E, N, D, M, O, R, Y, C1, C2, C3, C4, =\=_in_gg(S, zero))
U55_aaaaaaaa(S, E, N, D, M, O, R, Y, C1, C2, C3, C4, =\=_out_gg(S, zero)) → U56_aaaaaaaa(S, E, N, D, M, O, R, Y, C1, C2, C3, calc_in_ggggg(C3, S, M, C4, O))
calc_in_ggggg(C0, D, E, C1, Y) → U60_ggggg(C0, D, E, C1, Y, sum_in_gga(C0, D, CD))
sum_in_gga(X, Y, Z) → U64_gga(X, Y, Z, isPlus_in_gga(X, Y, U))
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))) → U72_gga(X, Y, Z, isPlus_in_gga(X, Y, Z))
isPlus_in_gga(succ(X), pred(Y), Z) → U73_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) → U74_gga(X, Y, Z, isPlus_in_gga(X, Y, Z))
isPlus_in_gga(pred(X), pred(Y), pred(pred(Z))) → U75_gga(X, Y, Z, isPlus_in_gga(X, Y, Z))
U75_gga(X, Y, Z, isPlus_out_gga(X, Y, Z)) → isPlus_out_gga(pred(X), pred(Y), pred(pred(Z)))
U74_gga(X, Y, Z, isPlus_out_gga(X, Y, Z)) → isPlus_out_gga(pred(X), succ(Y), Z)
U73_gga(X, Y, Z, isPlus_out_gga(X, Y, Z)) → isPlus_out_gga(succ(X), pred(Y), Z)
U72_gga(X, Y, Z, isPlus_out_gga(X, Y, Z)) → isPlus_out_gga(succ(X), succ(Y), succ(succ(Z)))
U64_gga(X, Y, Z, isPlus_out_gga(X, Y, U)) → U65_gga(X, Y, Z, =_in_ag(Z, U))
=_in_ag(X, X) → =_out_ag(X, X)
U65_gga(X, Y, Z, =_out_ag(Z, U)) → sum_out_gga(X, Y, Z)
U60_ggggg(C0, D, E, C1, Y, sum_out_gga(C0, D, CD)) → U61_ggggg(C0, D, E, C1, Y, sum_in_gga(CD, E, S))
U61_ggggg(C0, D, E, C1, Y, sum_out_gga(CD, E, S)) → U62_ggggg(C0, D, E, C1, Y, S, carry10_in_ga(C1, C10))
carry10_in_ga(zero, zero) → carry10_out_ga(zero, zero)
carry10_in_ga(succ(zero), succ(succ(succ(succ(succ(succ(succ(succ(succ(succ(zero))))))))))) → carry10_out_ga(succ(zero), succ(succ(succ(succ(succ(succ(succ(succ(succ(succ(zero)))))))))))
U62_ggggg(C0, D, E, C1, Y, S, carry10_out_ga(C1, C10)) → U63_ggggg(C0, D, E, C1, Y, sum_in_ggg(C10, Y, S))
sum_in_ggg(X, Y, Z) → U64_ggg(X, Y, Z, isPlus_in_gga(X, Y, U))
U64_ggg(X, Y, Z, isPlus_out_gga(X, Y, U)) → U65_ggg(X, Y, Z, =_in_gg(Z, U))
=_in_gg(X, X) → =_out_gg(X, X)
U65_ggg(X, Y, Z, =_out_gg(Z, U)) → sum_out_ggg(X, Y, Z)
U63_ggggg(C0, D, E, C1, Y, sum_out_ggg(C10, Y, S)) → calc_out_ggggg(C0, D, E, C1, Y)
U56_aaaaaaaa(S, E, N, D, M, O, R, Y, C1, C2, C3, calc_out_ggggg(C3, S, M, C4, O)) → U57_aaaaaaaa(S, E, N, D, M, O, R, Y, C1, C2, calc_in_ggggg(C2, E, O, C3, N))
U57_aaaaaaaa(S, E, N, D, M, O, R, Y, C1, C2, calc_out_ggggg(C2, E, O, C3, N)) → U58_aaaaaaaa(S, E, N, D, M, O, R, Y, C1, calc_in_ggggg(C1, N, R, C2, E))
U58_aaaaaaaa(S, E, N, D, M, O, R, Y, C1, calc_out_ggggg(C1, N, R, C2, E)) → U59_aaaaaaaa(S, E, N, D, M, O, R, Y, calc_in_ggggg(zero, D, E, C1, Y))
U59_aaaaaaaa(S, E, N, D, M, O, R, Y, calc_out_ggggg(zero, D, E, C1, Y)) → money_out_aaaaaaaa(S, E, N, D, M, O, R, Y)

The argument filtering Pi contains the following mapping:
money_in_aaaaaaaa(x1, x2, x3, x4, x5, x6, x7, x8)  =  money_in_aaaaaaaa
U48_aaaaaaaa(x1, x2, x3, x4, x5, x6, x7, x8, x9)  =  U48_aaaaaaaa(x9)
carry_in_a(x1)  =  carry_in_a
carry_out_a(x1)  =  carry_out_a(x1)
U49_aaaaaaaa(x1, x2, x3, x4, x5, x6, x7, x8, x9, x10)  =  U49_aaaaaaaa(x9, x10)
U50_aaaaaaaa(x1, x2, x3, x4, x5, x6, x7, x8, x9, x10, x11)  =  U50_aaaaaaaa(x9, x10, x11)
U51_aaaaaaaa(x1, x2, x3, x4, x5, x6, x7, x8, x9, x10, x11, x12)  =  U51_aaaaaaaa(x9, x10, x11, x12)
U52_aaaaaaaa(x1, x2, x3, x4, x5, x6, x7, x8, x9, x10, x11, x12, x13)  =  U52_aaaaaaaa(x9, x10, x11, x12, x13)
=_in_ga(x1, x2)  =  =_in_ga(x1)
=_out_ga(x1, x2)  =  =_out_ga(x2)
U53_aaaaaaaa(x1, x2, x3, x4, x5, x6, x7, x8, x9, x10, x11, x12, x13)  =  U53_aaaaaaaa(x5, x9, x10, x11, x12, x13)
=\=_in_gg(x1, x2)  =  =\=_in_gg(x1, x2)
=\=_out_gg(x1, x2)  =  =\=_out_gg
zero  =  zero
U54_aaaaaaaa(x1, x2, x3, x4, x5, x6, x7, x8, x9, x10, x11, x12, x13)  =  U54_aaaaaaaa(x5, x9, x10, x11, x12, x13)
domain_in_ag(x1, x2)  =  domain_in_ag(x2)
domain_out_ag(x1, x2)  =  domain_out_ag(x1)
U66_ag(x1, x2, x3, x4)  =  U66_ag(x4)
del_in_aga(x1, x2, x3)  =  del_in_aga(x2)
.(x1, x2)  =  .(x1, x2)
del_out_aga(x1, x2, x3)  =  del_out_aga(x1, x3)
U68_aga(x1, x2, x3, x4, x5)  =  U68_aga(x2, x5)
U67_ag(x1, x2, x3, x4)  =  U67_ag(x1, x4)
[]  =  []
succ(x1)  =  succ(x1)
U55_aaaaaaaa(x1, x2, x3, x4, x5, x6, x7, x8, x9, x10, x11, x12, x13)  =  U55_aaaaaaaa(x1, x2, x3, x4, x5, x6, x7, x8, x9, x10, x11, x12, x13)
U56_aaaaaaaa(x1, x2, x3, x4, x5, x6, x7, x8, x9, x10, x11, x12)  =  U56_aaaaaaaa(x1, x2, x3, x4, x5, x6, x7, x8, x9, x10, x11, x12)
calc_in_ggggg(x1, x2, x3, x4, x5)  =  calc_in_ggggg(x1, x2, x3, x4, x5)
U60_ggggg(x1, x2, x3, x4, x5, x6)  =  U60_ggggg(x3, x4, x5, x6)
sum_in_gga(x1, x2, x3)  =  sum_in_gga(x1, x2)
U64_gga(x1, x2, x3, x4)  =  U64_gga(x4)
isPlus_in_gga(x1, x2, x3)  =  isPlus_in_gga(x1, x2)
isPlus_out_gga(x1, x2, x3)  =  isPlus_out_gga(x3)
U72_gga(x1, x2, x3, x4)  =  U72_gga(x4)
pred(x1)  =  pred(x1)
U73_gga(x1, x2, x3, x4)  =  U73_gga(x4)
U74_gga(x1, x2, x3, x4)  =  U74_gga(x4)
U75_gga(x1, x2, x3, x4)  =  U75_gga(x4)
U65_gga(x1, x2, x3, x4)  =  U65_gga(x4)
=_in_ag(x1, x2)  =  =_in_ag(x2)
=_out_ag(x1, x2)  =  =_out_ag(x1)
sum_out_gga(x1, x2, x3)  =  sum_out_gga(x3)
U61_ggggg(x1, x2, x3, x4, x5, x6)  =  U61_ggggg(x4, x5, x6)
U62_ggggg(x1, x2, x3, x4, x5, x6, x7)  =  U62_ggggg(x5, x6, x7)
carry10_in_ga(x1, x2)  =  carry10_in_ga(x1)
carry10_out_ga(x1, x2)  =  carry10_out_ga(x2)
U63_ggggg(x1, x2, x3, x4, x5, x6)  =  U63_ggggg(x6)
sum_in_ggg(x1, x2, x3)  =  sum_in_ggg(x1, x2, x3)
U64_ggg(x1, x2, x3, x4)  =  U64_ggg(x3, x4)
U65_ggg(x1, x2, x3, x4)  =  U65_ggg(x4)
=_in_gg(x1, x2)  =  =_in_gg(x1, x2)
=_out_gg(x1, x2)  =  =_out_gg
sum_out_ggg(x1, x2, x3)  =  sum_out_ggg
calc_out_ggggg(x1, x2, x3, x4, x5)  =  calc_out_ggggg
U57_aaaaaaaa(x1, x2, x3, x4, x5, x6, x7, x8, x9, x10, x11)  =  U57_aaaaaaaa(x1, x2, x3, x4, x5, x6, x7, x8, x9, x10, x11)
U58_aaaaaaaa(x1, x2, x3, x4, x5, x6, x7, x8, x9, x10)  =  U58_aaaaaaaa(x1, x2, x3, x4, x5, x6, x7, x8, x9, x10)
U59_aaaaaaaa(x1, x2, x3, x4, x5, x6, x7, x8, x9)  =  U59_aaaaaaaa(x1, x2, x3, x4, x5, x6, x7, x8, x9)
money_out_aaaaaaaa(x1, x2, x3, x4, x5, x6, x7, x8)  =  money_out_aaaaaaaa(x1, x2, x3, x4, x5, x6, x7, x8)
DEL_IN_AGA(x1, x2, x3)  =  DEL_IN_AGA(x2)

We have to consider all (P,R,Pi)-chains
For (infinitary) constructor rewriting [30] we can delete all non-usable rules from R.

↳ Prolog
  ↳ PredefinedPredicateTransformerProof
    ↳ Prolog
      ↳ CutEliminatorProof
        ↳ Prolog
          ↳ UndefinedPredicateHandlerProof
            ↳ Prolog
              ↳ PrologToPiTRSProof
                ↳ PiTRS
                  ↳ DependencyPairsProof
                    ↳ PiDP
                      ↳ DependencyGraphProof
                        ↳ AND
                          ↳ PiDP
                          ↳ PiDP
                            ↳ UsableRulesProof
                              ↳ PiDP
                                ↳ PiDPToQDPProof
                          ↳ PiDP

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

DEL_IN_AGA(X, .(Y, T), .(Y, NT)) → DEL_IN_AGA(X, T, NT)

R is empty.
The argument filtering Pi contains the following mapping:
.(x1, x2)  =  .(x1, x2)
DEL_IN_AGA(x1, x2, x3)  =  DEL_IN_AGA(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
      ↳ CutEliminatorProof
        ↳ Prolog
          ↳ UndefinedPredicateHandlerProof
            ↳ Prolog
              ↳ PrologToPiTRSProof
                ↳ PiTRS
                  ↳ DependencyPairsProof
                    ↳ PiDP
                      ↳ DependencyGraphProof
                        ↳ AND
                          ↳ PiDP
                          ↳ PiDP
                            ↳ UsableRulesProof
                              ↳ PiDP
                                ↳ PiDPToQDPProof
                                  ↳ QDP
                                    ↳ QDPSizeChangeProof
                          ↳ PiDP

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

DEL_IN_AGA(.(Y, T)) → DEL_IN_AGA(T)

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: 



↳ Prolog
  ↳ PredefinedPredicateTransformerProof
    ↳ Prolog
      ↳ CutEliminatorProof
        ↳ Prolog
          ↳ UndefinedPredicateHandlerProof
            ↳ Prolog
              ↳ PrologToPiTRSProof
                ↳ PiTRS
                  ↳ DependencyPairsProof
                    ↳ PiDP
                      ↳ DependencyGraphProof
                        ↳ AND
                          ↳ PiDP
                          ↳ PiDP
                          ↳ PiDP
                            ↳ UsableRulesProof

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

DOMAIN_IN_AG(.(X1, R), L) → U66_AG(X1, R, L, del_in_aga(X1, L, NL))
U66_AG(X1, R, L, del_out_aga(X1, L, NL)) → DOMAIN_IN_AG(R, NL)

The TRS R consists of the following rules:

money_in_aaaaaaaa(S, E, N, D, M, O, R, Y) → U48_aaaaaaaa(S, E, N, D, M, O, R, Y, carry_in_a(C1))
carry_in_a(succ(zero)) → carry_out_a(succ(zero))
carry_in_a(zero) → carry_out_a(zero)
U48_aaaaaaaa(S, E, N, D, M, O, R, Y, carry_out_a(C1)) → U49_aaaaaaaa(S, E, N, D, M, O, R, Y, C1, carry_in_a(C2))
U49_aaaaaaaa(S, E, N, D, M, O, R, Y, C1, carry_out_a(C2)) → U50_aaaaaaaa(S, E, N, D, M, O, R, Y, C1, C2, carry_in_a(C3))
U50_aaaaaaaa(S, E, N, D, M, O, R, Y, C1, C2, carry_out_a(C3)) → U51_aaaaaaaa(S, E, N, D, M, O, R, Y, C1, C2, C3, carry_in_a(C4))
U51_aaaaaaaa(S, E, N, D, M, O, R, Y, C1, C2, C3, carry_out_a(C4)) → U52_aaaaaaaa(S, E, N, D, M, O, R, Y, C1, C2, C3, C4, =_in_ga(C4, M))
=_in_ga(X, X) → =_out_ga(X, X)
U52_aaaaaaaa(S, E, N, D, M, O, R, Y, C1, C2, C3, C4, =_out_ga(C4, M)) → U53_aaaaaaaa(S, E, N, D, M, O, R, Y, C1, C2, C3, C4, =\=_in_gg(M, zero))
=\=_in_gg(X0, X1) → =\=_out_gg(X0, X1)
U53_aaaaaaaa(S, E, N, D, M, O, R, Y, C1, C2, C3, C4, =\=_out_gg(M, zero)) → U54_aaaaaaaa(S, E, N, D, M, O, R, Y, C1, C2, C3, C4, domain_in_ag(.(S, .(E, .(N, .(D, .(M, .(O, .(R, .(Y, [])))))))), .(zero, .(succ(zero), .(succ(succ(zero)), .(succ(succ(succ(zero))), .(succ(succ(succ(succ(zero)))), .(succ(succ(succ(succ(succ(zero))))), .(succ(succ(succ(succ(succ(succ(zero)))))), .(succ(succ(succ(succ(succ(succ(succ(zero))))))), .(succ(succ(succ(succ(succ(succ(succ(succ(zero)))))))), .(succ(succ(succ(succ(succ(succ(succ(succ(succ(zero))))))))), []))))))))))))
domain_in_ag([], X) → domain_out_ag([], X)
domain_in_ag(.(X1, R), L) → U66_ag(X1, R, L, del_in_aga(X1, L, NL))
del_in_aga(X, .(X, T), T) → del_out_aga(X, .(X, T), T)
del_in_aga(X, .(Y, T), .(Y, NT)) → U68_aga(X, Y, T, NT, del_in_aga(X, T, NT))
U68_aga(X, Y, T, NT, del_out_aga(X, T, NT)) → del_out_aga(X, .(Y, T), .(Y, NT))
U66_ag(X1, R, L, del_out_aga(X1, L, NL)) → U67_ag(X1, R, L, domain_in_ag(R, NL))
U67_ag(X1, R, L, domain_out_ag(R, NL)) → domain_out_ag(.(X1, R), L)
U54_aaaaaaaa(S, E, N, D, M, O, R, Y, C1, C2, C3, C4, domain_out_ag(.(S, .(E, .(N, .(D, .(M, .(O, .(R, .(Y, [])))))))), .(zero, .(succ(zero), .(succ(succ(zero)), .(succ(succ(succ(zero))), .(succ(succ(succ(succ(zero)))), .(succ(succ(succ(succ(succ(zero))))), .(succ(succ(succ(succ(succ(succ(zero)))))), .(succ(succ(succ(succ(succ(succ(succ(zero))))))), .(succ(succ(succ(succ(succ(succ(succ(succ(zero)))))))), .(succ(succ(succ(succ(succ(succ(succ(succ(succ(zero))))))))), [])))))))))))) → U55_aaaaaaaa(S, E, N, D, M, O, R, Y, C1, C2, C3, C4, =\=_in_gg(S, zero))
U55_aaaaaaaa(S, E, N, D, M, O, R, Y, C1, C2, C3, C4, =\=_out_gg(S, zero)) → U56_aaaaaaaa(S, E, N, D, M, O, R, Y, C1, C2, C3, calc_in_ggggg(C3, S, M, C4, O))
calc_in_ggggg(C0, D, E, C1, Y) → U60_ggggg(C0, D, E, C1, Y, sum_in_gga(C0, D, CD))
sum_in_gga(X, Y, Z) → U64_gga(X, Y, Z, isPlus_in_gga(X, Y, U))
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))) → U72_gga(X, Y, Z, isPlus_in_gga(X, Y, Z))
isPlus_in_gga(succ(X), pred(Y), Z) → U73_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) → U74_gga(X, Y, Z, isPlus_in_gga(X, Y, Z))
isPlus_in_gga(pred(X), pred(Y), pred(pred(Z))) → U75_gga(X, Y, Z, isPlus_in_gga(X, Y, Z))
U75_gga(X, Y, Z, isPlus_out_gga(X, Y, Z)) → isPlus_out_gga(pred(X), pred(Y), pred(pred(Z)))
U74_gga(X, Y, Z, isPlus_out_gga(X, Y, Z)) → isPlus_out_gga(pred(X), succ(Y), Z)
U73_gga(X, Y, Z, isPlus_out_gga(X, Y, Z)) → isPlus_out_gga(succ(X), pred(Y), Z)
U72_gga(X, Y, Z, isPlus_out_gga(X, Y, Z)) → isPlus_out_gga(succ(X), succ(Y), succ(succ(Z)))
U64_gga(X, Y, Z, isPlus_out_gga(X, Y, U)) → U65_gga(X, Y, Z, =_in_ag(Z, U))
=_in_ag(X, X) → =_out_ag(X, X)
U65_gga(X, Y, Z, =_out_ag(Z, U)) → sum_out_gga(X, Y, Z)
U60_ggggg(C0, D, E, C1, Y, sum_out_gga(C0, D, CD)) → U61_ggggg(C0, D, E, C1, Y, sum_in_gga(CD, E, S))
U61_ggggg(C0, D, E, C1, Y, sum_out_gga(CD, E, S)) → U62_ggggg(C0, D, E, C1, Y, S, carry10_in_ga(C1, C10))
carry10_in_ga(zero, zero) → carry10_out_ga(zero, zero)
carry10_in_ga(succ(zero), succ(succ(succ(succ(succ(succ(succ(succ(succ(succ(zero))))))))))) → carry10_out_ga(succ(zero), succ(succ(succ(succ(succ(succ(succ(succ(succ(succ(zero)))))))))))
U62_ggggg(C0, D, E, C1, Y, S, carry10_out_ga(C1, C10)) → U63_ggggg(C0, D, E, C1, Y, sum_in_ggg(C10, Y, S))
sum_in_ggg(X, Y, Z) → U64_ggg(X, Y, Z, isPlus_in_gga(X, Y, U))
U64_ggg(X, Y, Z, isPlus_out_gga(X, Y, U)) → U65_ggg(X, Y, Z, =_in_gg(Z, U))
=_in_gg(X, X) → =_out_gg(X, X)
U65_ggg(X, Y, Z, =_out_gg(Z, U)) → sum_out_ggg(X, Y, Z)
U63_ggggg(C0, D, E, C1, Y, sum_out_ggg(C10, Y, S)) → calc_out_ggggg(C0, D, E, C1, Y)
U56_aaaaaaaa(S, E, N, D, M, O, R, Y, C1, C2, C3, calc_out_ggggg(C3, S, M, C4, O)) → U57_aaaaaaaa(S, E, N, D, M, O, R, Y, C1, C2, calc_in_ggggg(C2, E, O, C3, N))
U57_aaaaaaaa(S, E, N, D, M, O, R, Y, C1, C2, calc_out_ggggg(C2, E, O, C3, N)) → U58_aaaaaaaa(S, E, N, D, M, O, R, Y, C1, calc_in_ggggg(C1, N, R, C2, E))
U58_aaaaaaaa(S, E, N, D, M, O, R, Y, C1, calc_out_ggggg(C1, N, R, C2, E)) → U59_aaaaaaaa(S, E, N, D, M, O, R, Y, calc_in_ggggg(zero, D, E, C1, Y))
U59_aaaaaaaa(S, E, N, D, M, O, R, Y, calc_out_ggggg(zero, D, E, C1, Y)) → money_out_aaaaaaaa(S, E, N, D, M, O, R, Y)

The argument filtering Pi contains the following mapping:
money_in_aaaaaaaa(x1, x2, x3, x4, x5, x6, x7, x8)  =  money_in_aaaaaaaa
U48_aaaaaaaa(x1, x2, x3, x4, x5, x6, x7, x8, x9)  =  U48_aaaaaaaa(x9)
carry_in_a(x1)  =  carry_in_a
carry_out_a(x1)  =  carry_out_a(x1)
U49_aaaaaaaa(x1, x2, x3, x4, x5, x6, x7, x8, x9, x10)  =  U49_aaaaaaaa(x9, x10)
U50_aaaaaaaa(x1, x2, x3, x4, x5, x6, x7, x8, x9, x10, x11)  =  U50_aaaaaaaa(x9, x10, x11)
U51_aaaaaaaa(x1, x2, x3, x4, x5, x6, x7, x8, x9, x10, x11, x12)  =  U51_aaaaaaaa(x9, x10, x11, x12)
U52_aaaaaaaa(x1, x2, x3, x4, x5, x6, x7, x8, x9, x10, x11, x12, x13)  =  U52_aaaaaaaa(x9, x10, x11, x12, x13)
=_in_ga(x1, x2)  =  =_in_ga(x1)
=_out_ga(x1, x2)  =  =_out_ga(x2)
U53_aaaaaaaa(x1, x2, x3, x4, x5, x6, x7, x8, x9, x10, x11, x12, x13)  =  U53_aaaaaaaa(x5, x9, x10, x11, x12, x13)
=\=_in_gg(x1, x2)  =  =\=_in_gg(x1, x2)
=\=_out_gg(x1, x2)  =  =\=_out_gg
zero  =  zero
U54_aaaaaaaa(x1, x2, x3, x4, x5, x6, x7, x8, x9, x10, x11, x12, x13)  =  U54_aaaaaaaa(x5, x9, x10, x11, x12, x13)
domain_in_ag(x1, x2)  =  domain_in_ag(x2)
domain_out_ag(x1, x2)  =  domain_out_ag(x1)
U66_ag(x1, x2, x3, x4)  =  U66_ag(x4)
del_in_aga(x1, x2, x3)  =  del_in_aga(x2)
.(x1, x2)  =  .(x1, x2)
del_out_aga(x1, x2, x3)  =  del_out_aga(x1, x3)
U68_aga(x1, x2, x3, x4, x5)  =  U68_aga(x2, x5)
U67_ag(x1, x2, x3, x4)  =  U67_ag(x1, x4)
[]  =  []
succ(x1)  =  succ(x1)
U55_aaaaaaaa(x1, x2, x3, x4, x5, x6, x7, x8, x9, x10, x11, x12, x13)  =  U55_aaaaaaaa(x1, x2, x3, x4, x5, x6, x7, x8, x9, x10, x11, x12, x13)
U56_aaaaaaaa(x1, x2, x3, x4, x5, x6, x7, x8, x9, x10, x11, x12)  =  U56_aaaaaaaa(x1, x2, x3, x4, x5, x6, x7, x8, x9, x10, x11, x12)
calc_in_ggggg(x1, x2, x3, x4, x5)  =  calc_in_ggggg(x1, x2, x3, x4, x5)
U60_ggggg(x1, x2, x3, x4, x5, x6)  =  U60_ggggg(x3, x4, x5, x6)
sum_in_gga(x1, x2, x3)  =  sum_in_gga(x1, x2)
U64_gga(x1, x2, x3, x4)  =  U64_gga(x4)
isPlus_in_gga(x1, x2, x3)  =  isPlus_in_gga(x1, x2)
isPlus_out_gga(x1, x2, x3)  =  isPlus_out_gga(x3)
U72_gga(x1, x2, x3, x4)  =  U72_gga(x4)
pred(x1)  =  pred(x1)
U73_gga(x1, x2, x3, x4)  =  U73_gga(x4)
U74_gga(x1, x2, x3, x4)  =  U74_gga(x4)
U75_gga(x1, x2, x3, x4)  =  U75_gga(x4)
U65_gga(x1, x2, x3, x4)  =  U65_gga(x4)
=_in_ag(x1, x2)  =  =_in_ag(x2)
=_out_ag(x1, x2)  =  =_out_ag(x1)
sum_out_gga(x1, x2, x3)  =  sum_out_gga(x3)
U61_ggggg(x1, x2, x3, x4, x5, x6)  =  U61_ggggg(x4, x5, x6)
U62_ggggg(x1, x2, x3, x4, x5, x6, x7)  =  U62_ggggg(x5, x6, x7)
carry10_in_ga(x1, x2)  =  carry10_in_ga(x1)
carry10_out_ga(x1, x2)  =  carry10_out_ga(x2)
U63_ggggg(x1, x2, x3, x4, x5, x6)  =  U63_ggggg(x6)
sum_in_ggg(x1, x2, x3)  =  sum_in_ggg(x1, x2, x3)
U64_ggg(x1, x2, x3, x4)  =  U64_ggg(x3, x4)
U65_ggg(x1, x2, x3, x4)  =  U65_ggg(x4)
=_in_gg(x1, x2)  =  =_in_gg(x1, x2)
=_out_gg(x1, x2)  =  =_out_gg
sum_out_ggg(x1, x2, x3)  =  sum_out_ggg
calc_out_ggggg(x1, x2, x3, x4, x5)  =  calc_out_ggggg
U57_aaaaaaaa(x1, x2, x3, x4, x5, x6, x7, x8, x9, x10, x11)  =  U57_aaaaaaaa(x1, x2, x3, x4, x5, x6, x7, x8, x9, x10, x11)
U58_aaaaaaaa(x1, x2, x3, x4, x5, x6, x7, x8, x9, x10)  =  U58_aaaaaaaa(x1, x2, x3, x4, x5, x6, x7, x8, x9, x10)
U59_aaaaaaaa(x1, x2, x3, x4, x5, x6, x7, x8, x9)  =  U59_aaaaaaaa(x1, x2, x3, x4, x5, x6, x7, x8, x9)
money_out_aaaaaaaa(x1, x2, x3, x4, x5, x6, x7, x8)  =  money_out_aaaaaaaa(x1, x2, x3, x4, x5, x6, x7, x8)
U66_AG(x1, x2, x3, x4)  =  U66_AG(x4)
DOMAIN_IN_AG(x1, x2)  =  DOMAIN_IN_AG(x2)

We have to consider all (P,R,Pi)-chains
For (infinitary) constructor rewriting [30] we can delete all non-usable rules from R.

↳ Prolog
  ↳ PredefinedPredicateTransformerProof
    ↳ Prolog
      ↳ CutEliminatorProof
        ↳ Prolog
          ↳ UndefinedPredicateHandlerProof
            ↳ Prolog
              ↳ PrologToPiTRSProof
                ↳ PiTRS
                  ↳ DependencyPairsProof
                    ↳ PiDP
                      ↳ DependencyGraphProof
                        ↳ AND
                          ↳ PiDP
                          ↳ PiDP
                          ↳ PiDP
                            ↳ UsableRulesProof
                              ↳ PiDP
                                ↳ PiDPToQDPProof

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

DOMAIN_IN_AG(.(X1, R), L) → U66_AG(X1, R, L, del_in_aga(X1, L, NL))
U66_AG(X1, R, L, del_out_aga(X1, L, NL)) → DOMAIN_IN_AG(R, NL)

The TRS R consists of the following rules:

del_in_aga(X, .(X, T), T) → del_out_aga(X, .(X, T), T)
del_in_aga(X, .(Y, T), .(Y, NT)) → U68_aga(X, Y, T, NT, del_in_aga(X, T, NT))
U68_aga(X, Y, T, NT, del_out_aga(X, T, NT)) → del_out_aga(X, .(Y, T), .(Y, NT))

The argument filtering Pi contains the following mapping:
del_in_aga(x1, x2, x3)  =  del_in_aga(x2)
.(x1, x2)  =  .(x1, x2)
del_out_aga(x1, x2, x3)  =  del_out_aga(x1, x3)
U68_aga(x1, x2, x3, x4, x5)  =  U68_aga(x2, x5)
U66_AG(x1, x2, x3, x4)  =  U66_AG(x4)
DOMAIN_IN_AG(x1, x2)  =  DOMAIN_IN_AG(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
      ↳ CutEliminatorProof
        ↳ Prolog
          ↳ UndefinedPredicateHandlerProof
            ↳ Prolog
              ↳ PrologToPiTRSProof
                ↳ PiTRS
                  ↳ DependencyPairsProof
                    ↳ PiDP
                      ↳ DependencyGraphProof
                        ↳ AND
                          ↳ PiDP
                          ↳ PiDP
                          ↳ PiDP
                            ↳ UsableRulesProof
                              ↳ PiDP
                                ↳ PiDPToQDPProof
                                  ↳ QDP
                                    ↳ RuleRemovalProof

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

DOMAIN_IN_AG(L) → U66_AG(del_in_aga(L))
U66_AG(del_out_aga(X1, NL)) → DOMAIN_IN_AG(NL)

The TRS R consists of the following rules:

del_in_aga(.(X, T)) → del_out_aga(X, T)
del_in_aga(.(Y, T)) → U68_aga(Y, del_in_aga(T))
U68_aga(Y, del_out_aga(X, NT)) → del_out_aga(X, .(Y, NT))

The set Q consists of the following terms:

del_in_aga(x0)
U68_aga(x0, x1)

We have to consider all (P,Q,R)-chains.
By using the rule removal processor [15] with the following polynomial ordering [25], at least one Dependency Pair or term rewrite system rule of this QDP problem can be strictly oriented.

Strictly oriented rules of the TRS R:

del_in_aga(.(X, T)) → del_out_aga(X, T)

Used ordering: POLO with Polynomial interpretation [25]:

POL(.(x1, x2)) = 1 + 2·x1 + x2   
POL(DOMAIN_IN_AG(x1)) = x1   
POL(U66_AG(x1)) = x1   
POL(U68_aga(x1, x2)) = 1 + 2·x1 + x2   
POL(del_in_aga(x1)) = x1   
POL(del_out_aga(x1, x2)) = x1 + x2   



↳ Prolog
  ↳ PredefinedPredicateTransformerProof
    ↳ Prolog
      ↳ CutEliminatorProof
        ↳ Prolog
          ↳ UndefinedPredicateHandlerProof
            ↳ Prolog
              ↳ PrologToPiTRSProof
                ↳ PiTRS
                  ↳ DependencyPairsProof
                    ↳ PiDP
                      ↳ DependencyGraphProof
                        ↳ AND
                          ↳ PiDP
                          ↳ PiDP
                          ↳ PiDP
                            ↳ UsableRulesProof
                              ↳ PiDP
                                ↳ PiDPToQDPProof
                                  ↳ QDP
                                    ↳ RuleRemovalProof
                                      ↳ QDP
                                        ↳ RuleRemovalProof

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

DOMAIN_IN_AG(L) → U66_AG(del_in_aga(L))
U66_AG(del_out_aga(X1, NL)) → DOMAIN_IN_AG(NL)

The TRS R consists of the following rules:

del_in_aga(.(Y, T)) → U68_aga(Y, del_in_aga(T))
U68_aga(Y, del_out_aga(X, NT)) → del_out_aga(X, .(Y, NT))

The set Q consists of the following terms:

del_in_aga(x0)
U68_aga(x0, x1)

We have to consider all (P,Q,R)-chains.
By using the rule removal processor [15] with the following polynomial ordering [25], at least one Dependency Pair or term rewrite system rule of this QDP problem can be strictly oriented.
Strictly oriented dependency pairs:

DOMAIN_IN_AG(L) → U66_AG(del_in_aga(L))
U66_AG(del_out_aga(X1, NL)) → DOMAIN_IN_AG(NL)

Strictly oriented rules of the TRS R:

U68_aga(Y, del_out_aga(X, NT)) → del_out_aga(X, .(Y, NT))

Used ordering: POLO with Polynomial interpretation [25]:

POL(.(x1, x2)) = 2·x1 + 2·x2   
POL(DOMAIN_IN_AG(x1)) = 1 + x1   
POL(U66_AG(x1)) = x1   
POL(U68_aga(x1, x2)) = 2·x1 + 2·x2   
POL(del_in_aga(x1)) = x1   
POL(del_out_aga(x1, x2)) = 2 + x1 + x2   



↳ Prolog
  ↳ PredefinedPredicateTransformerProof
    ↳ Prolog
      ↳ CutEliminatorProof
        ↳ Prolog
          ↳ UndefinedPredicateHandlerProof
            ↳ Prolog
              ↳ PrologToPiTRSProof
                ↳ PiTRS
                  ↳ DependencyPairsProof
                    ↳ PiDP
                      ↳ DependencyGraphProof
                        ↳ AND
                          ↳ PiDP
                          ↳ PiDP
                          ↳ PiDP
                            ↳ UsableRulesProof
                              ↳ PiDP
                                ↳ PiDPToQDPProof
                                  ↳ QDP
                                    ↳ RuleRemovalProof
                                      ↳ QDP
                                        ↳ RuleRemovalProof
                                          ↳ QDP
                                            ↳ PisEmptyProof

Q DP problem:
P is empty.
The TRS R consists of the following rules:

del_in_aga(.(Y, T)) → U68_aga(Y, del_in_aga(T))

The set Q consists of the following terms:

del_in_aga(x0)
U68_aga(x0, x1)

We have to consider all (P,Q,R)-chains.
The TRS P is empty. Hence, there is no (P,Q,R) chain.