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



↳ PROLOG
  ↳ UnrequestedClauseRemoverProof

myis2(Z, X) :- evaluate2(X, Z).
evaluate2(X + Y, Z) :- evaluate2(X, X1), evaluate2(Y, Y1), add3(X1, Y1, Z).
evaluate2(X - Y, Z) :- evaluate2(X, X1), evaluate2(Y, Y1), sub3(X1, Y1, Z).
evaluate2(X * Y, Z) :- evaluate2(X, X1), evaluate2(Y, Y1), mult3(X1, Y1, Z).
evaluate2(X, X) :- integer1(X).
integer1(s1(X)) :- integer1(X).
integer1(00).
add3(s1(X), Y, s1(Z)) :- add3(X, Y, Z).
add3(00, X, X).
sub3(s1(X), s1(Y), Z) :- sub3(X, Y, Z).
sub3(X, 00, X).
mult3(s1(X), Y, R) :- mult3(X, Y, Z), add3(Y, Z, R).
mult3(00, Y, 00).
notEq2(s1(X), s1(Y)) :- notEq2(X, Y).
notEq2(s1(X), 00).
notEq2(00, s1(X)).
lt2(s1(X), s1(Y)) :- lt2(X, Y).
lt2(00, s1(Y)).
gt2(s1(X), s1(Y)) :- gt2(X, Y).
gt2(s1(X), 00).
le2(s1(X), s1(Y)) :- le2(X, Y).
le2(00, s1(Y)).
le2(00, 00).


The clauses

notEq2(s1(X), s1(Y)) :- notEq2(X, Y).
notEq2(s1(X), 00).
notEq2(00, s1(X)).
lt2(s1(X), s1(Y)) :- lt2(X, Y).
lt2(00, s1(Y)).
gt2(s1(X), s1(Y)) :- gt2(X, Y).
gt2(s1(X), 00).
le2(s1(X), s1(Y)) :- le2(X, Y).
le2(00, s1(Y)).
le2(00, 00).

can be ignored, as they are not needed by any of the given querys.

Deleting these clauses results in the following prolog program:

myis2(Z, X) :- evaluate2(X, Z).
evaluate2(X + Y, Z) :- evaluate2(X, X1), evaluate2(Y, Y1), add3(X1, Y1, Z).
evaluate2(X - Y, Z) :- evaluate2(X, X1), evaluate2(Y, Y1), sub3(X1, Y1, Z).
evaluate2(X * Y, Z) :- evaluate2(X, X1), evaluate2(Y, Y1), mult3(X1, Y1, Z).
evaluate2(X, X) :- integer1(X).
integer1(s1(X)) :- integer1(X).
integer1(00).
add3(s1(X), Y, s1(Z)) :- add3(X, Y, Z).
add3(00, X, X).
sub3(s1(X), s1(Y), Z) :- sub3(X, Y, Z).
sub3(X, 00, X).
mult3(s1(X), Y, R) :- mult3(X, Y, Z), add3(Y, Z, R).
mult3(00, Y, 00).



↳ PROLOG
  ↳ UnrequestedClauseRemoverProof
    ↳ PROLOG
      ↳ PrologToPiTRSProof

myis2(Z, X) :- evaluate2(X, Z).
evaluate2(X + Y, Z) :- evaluate2(X, X1), evaluate2(Y, Y1), add3(X1, Y1, Z).
evaluate2(X - Y, Z) :- evaluate2(X, X1), evaluate2(Y, Y1), sub3(X1, Y1, Z).
evaluate2(X * Y, Z) :- evaluate2(X, X1), evaluate2(Y, Y1), mult3(X1, Y1, Z).
evaluate2(X, X) :- integer1(X).
integer1(s1(X)) :- integer1(X).
integer1(00).
add3(s1(X), Y, s1(Z)) :- add3(X, Y, Z).
add3(00, X, X).
sub3(s1(X), s1(Y), Z) :- sub3(X, Y, Z).
sub3(X, 00, X).
mult3(s1(X), Y, R) :- mult3(X, Y, Z), add3(Y, Z, R).
mult3(00, Y, 00).


With regard to the inferred argument filtering the predicates were used in the following modes:
myis2: (f,b)
evaluate2: (b,f)
integer1: (b)
mult3: (b,b,f)
add3: (b,b,f)
sub3: (b,b,f)
Transforming PROLOG into the following Term Rewriting System:
Pi-finite rewrite system:
The TRS R consists of the following rules:


myis_2_in_ag2(Z, X) -> if_myis_2_in_1_ag3(Z, X, evaluate_2_in_ga2(X, Z))
evaluate_2_in_ga2(+2(X, Y), Z) -> if_evaluate_2_in_1_ga4(X, Y, Z, evaluate_2_in_ga2(X, X1))
evaluate_2_in_ga2(-2(X, Y), Z) -> if_evaluate_2_in_4_ga4(X, Y, Z, evaluate_2_in_ga2(X, X1))
evaluate_2_in_ga2(*2(X, Y), Z) -> if_evaluate_2_in_7_ga4(X, Y, Z, evaluate_2_in_ga2(X, X1))
evaluate_2_in_ga2(X, X) -> if_evaluate_2_in_10_ga2(X, integer_1_in_g1(X))
integer_1_in_g1(s_11(X)) -> if_integer_1_in_1_g2(X, integer_1_in_g1(X))
integer_1_in_g1(0_0) -> integer_1_out_g1(0_0)
if_integer_1_in_1_g2(X, integer_1_out_g1(X)) -> integer_1_out_g1(s_11(X))
if_evaluate_2_in_10_ga2(X, integer_1_out_g1(X)) -> evaluate_2_out_ga2(X, X)
if_evaluate_2_in_7_ga4(X, Y, Z, evaluate_2_out_ga2(X, X1)) -> if_evaluate_2_in_8_ga5(X, Y, Z, X1, evaluate_2_in_ga2(Y, Y1))
if_evaluate_2_in_8_ga5(X, Y, Z, X1, evaluate_2_out_ga2(Y, Y1)) -> if_evaluate_2_in_9_ga6(X, Y, Z, X1, Y1, mult_3_in_gga3(X1, Y1, Z))
mult_3_in_gga3(s_11(X), Y, R) -> if_mult_3_in_1_gga4(X, Y, R, mult_3_in_gga3(X, Y, Z))
mult_3_in_gga3(0_0, Y, 0_0) -> mult_3_out_gga3(0_0, Y, 0_0)
if_mult_3_in_1_gga4(X, Y, R, mult_3_out_gga3(X, Y, Z)) -> if_mult_3_in_2_gga5(X, Y, R, Z, add_3_in_gga3(Y, Z, R))
add_3_in_gga3(s_11(X), Y, s_11(Z)) -> if_add_3_in_1_gga4(X, Y, Z, add_3_in_gga3(X, Y, Z))
add_3_in_gga3(0_0, X, X) -> add_3_out_gga3(0_0, X, X)
if_add_3_in_1_gga4(X, Y, Z, add_3_out_gga3(X, Y, Z)) -> add_3_out_gga3(s_11(X), Y, s_11(Z))
if_mult_3_in_2_gga5(X, Y, R, Z, add_3_out_gga3(Y, Z, R)) -> mult_3_out_gga3(s_11(X), Y, R)
if_evaluate_2_in_9_ga6(X, Y, Z, X1, Y1, mult_3_out_gga3(X1, Y1, Z)) -> evaluate_2_out_ga2(*2(X, Y), Z)
if_evaluate_2_in_4_ga4(X, Y, Z, evaluate_2_out_ga2(X, X1)) -> if_evaluate_2_in_5_ga5(X, Y, Z, X1, evaluate_2_in_ga2(Y, Y1))
if_evaluate_2_in_5_ga5(X, Y, Z, X1, evaluate_2_out_ga2(Y, Y1)) -> if_evaluate_2_in_6_ga6(X, Y, Z, X1, Y1, sub_3_in_gga3(X1, Y1, Z))
sub_3_in_gga3(s_11(X), s_11(Y), Z) -> if_sub_3_in_1_gga4(X, Y, Z, sub_3_in_gga3(X, Y, Z))
sub_3_in_gga3(X, 0_0, X) -> sub_3_out_gga3(X, 0_0, X)
if_sub_3_in_1_gga4(X, Y, Z, sub_3_out_gga3(X, Y, Z)) -> sub_3_out_gga3(s_11(X), s_11(Y), Z)
if_evaluate_2_in_6_ga6(X, Y, Z, X1, Y1, sub_3_out_gga3(X1, Y1, Z)) -> evaluate_2_out_ga2(-2(X, Y), Z)
if_evaluate_2_in_1_ga4(X, Y, Z, evaluate_2_out_ga2(X, X1)) -> if_evaluate_2_in_2_ga5(X, Y, Z, X1, evaluate_2_in_ga2(Y, Y1))
if_evaluate_2_in_2_ga5(X, Y, Z, X1, evaluate_2_out_ga2(Y, Y1)) -> if_evaluate_2_in_3_ga6(X, Y, Z, X1, Y1, add_3_in_gga3(X1, Y1, Z))
if_evaluate_2_in_3_ga6(X, Y, Z, X1, Y1, add_3_out_gga3(X1, Y1, Z)) -> evaluate_2_out_ga2(+2(X, Y), Z)
if_myis_2_in_1_ag3(Z, X, evaluate_2_out_ga2(X, Z)) -> myis_2_out_ag2(Z, X)

The argument filtering Pi contains the following mapping:
myis_2_in_ag2(x1, x2)  =  myis_2_in_ag1(x2)
+2(x1, x2)  =  +2(x1, x2)
-2(x1, x2)  =  -2(x1, x2)
*2(x1, x2)  =  *2(x1, x2)
s_11(x1)  =  s_11(x1)
0_0  =  0_0
if_myis_2_in_1_ag3(x1, x2, x3)  =  if_myis_2_in_1_ag1(x3)
evaluate_2_in_ga2(x1, x2)  =  evaluate_2_in_ga1(x1)
if_evaluate_2_in_1_ga4(x1, x2, x3, x4)  =  if_evaluate_2_in_1_ga2(x2, x4)
if_evaluate_2_in_4_ga4(x1, x2, x3, x4)  =  if_evaluate_2_in_4_ga2(x2, x4)
if_evaluate_2_in_7_ga4(x1, x2, x3, x4)  =  if_evaluate_2_in_7_ga2(x2, x4)
if_evaluate_2_in_10_ga2(x1, x2)  =  if_evaluate_2_in_10_ga2(x1, x2)
integer_1_in_g1(x1)  =  integer_1_in_g1(x1)
if_integer_1_in_1_g2(x1, x2)  =  if_integer_1_in_1_g1(x2)
integer_1_out_g1(x1)  =  integer_1_out_g
evaluate_2_out_ga2(x1, x2)  =  evaluate_2_out_ga1(x2)
if_evaluate_2_in_8_ga5(x1, x2, x3, x4, x5)  =  if_evaluate_2_in_8_ga2(x4, x5)
if_evaluate_2_in_9_ga6(x1, x2, x3, x4, x5, x6)  =  if_evaluate_2_in_9_ga1(x6)
mult_3_in_gga3(x1, x2, x3)  =  mult_3_in_gga2(x1, x2)
if_mult_3_in_1_gga4(x1, x2, x3, x4)  =  if_mult_3_in_1_gga2(x2, x4)
mult_3_out_gga3(x1, x2, x3)  =  mult_3_out_gga1(x3)
if_mult_3_in_2_gga5(x1, x2, x3, x4, x5)  =  if_mult_3_in_2_gga1(x5)
add_3_in_gga3(x1, x2, x3)  =  add_3_in_gga2(x1, x2)
if_add_3_in_1_gga4(x1, x2, x3, x4)  =  if_add_3_in_1_gga1(x4)
add_3_out_gga3(x1, x2, x3)  =  add_3_out_gga1(x3)
if_evaluate_2_in_5_ga5(x1, x2, x3, x4, x5)  =  if_evaluate_2_in_5_ga2(x4, x5)
if_evaluate_2_in_6_ga6(x1, x2, x3, x4, x5, x6)  =  if_evaluate_2_in_6_ga1(x6)
sub_3_in_gga3(x1, x2, x3)  =  sub_3_in_gga2(x1, x2)
if_sub_3_in_1_gga4(x1, x2, x3, x4)  =  if_sub_3_in_1_gga1(x4)
sub_3_out_gga3(x1, x2, x3)  =  sub_3_out_gga1(x3)
if_evaluate_2_in_2_ga5(x1, x2, x3, x4, x5)  =  if_evaluate_2_in_2_ga2(x4, x5)
if_evaluate_2_in_3_ga6(x1, x2, x3, x4, x5, x6)  =  if_evaluate_2_in_3_ga1(x6)
myis_2_out_ag2(x1, x2)  =  myis_2_out_ag1(x1)

Infinitary Constructor Rewriting Termination of PiTRS implies Termination of PROLOG



↳ PROLOG
  ↳ UnrequestedClauseRemoverProof
    ↳ PROLOG
      ↳ PrologToPiTRSProof
        ↳ PiTRS
          ↳ DependencyPairsProof

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

myis_2_in_ag2(Z, X) -> if_myis_2_in_1_ag3(Z, X, evaluate_2_in_ga2(X, Z))
evaluate_2_in_ga2(+2(X, Y), Z) -> if_evaluate_2_in_1_ga4(X, Y, Z, evaluate_2_in_ga2(X, X1))
evaluate_2_in_ga2(-2(X, Y), Z) -> if_evaluate_2_in_4_ga4(X, Y, Z, evaluate_2_in_ga2(X, X1))
evaluate_2_in_ga2(*2(X, Y), Z) -> if_evaluate_2_in_7_ga4(X, Y, Z, evaluate_2_in_ga2(X, X1))
evaluate_2_in_ga2(X, X) -> if_evaluate_2_in_10_ga2(X, integer_1_in_g1(X))
integer_1_in_g1(s_11(X)) -> if_integer_1_in_1_g2(X, integer_1_in_g1(X))
integer_1_in_g1(0_0) -> integer_1_out_g1(0_0)
if_integer_1_in_1_g2(X, integer_1_out_g1(X)) -> integer_1_out_g1(s_11(X))
if_evaluate_2_in_10_ga2(X, integer_1_out_g1(X)) -> evaluate_2_out_ga2(X, X)
if_evaluate_2_in_7_ga4(X, Y, Z, evaluate_2_out_ga2(X, X1)) -> if_evaluate_2_in_8_ga5(X, Y, Z, X1, evaluate_2_in_ga2(Y, Y1))
if_evaluate_2_in_8_ga5(X, Y, Z, X1, evaluate_2_out_ga2(Y, Y1)) -> if_evaluate_2_in_9_ga6(X, Y, Z, X1, Y1, mult_3_in_gga3(X1, Y1, Z))
mult_3_in_gga3(s_11(X), Y, R) -> if_mult_3_in_1_gga4(X, Y, R, mult_3_in_gga3(X, Y, Z))
mult_3_in_gga3(0_0, Y, 0_0) -> mult_3_out_gga3(0_0, Y, 0_0)
if_mult_3_in_1_gga4(X, Y, R, mult_3_out_gga3(X, Y, Z)) -> if_mult_3_in_2_gga5(X, Y, R, Z, add_3_in_gga3(Y, Z, R))
add_3_in_gga3(s_11(X), Y, s_11(Z)) -> if_add_3_in_1_gga4(X, Y, Z, add_3_in_gga3(X, Y, Z))
add_3_in_gga3(0_0, X, X) -> add_3_out_gga3(0_0, X, X)
if_add_3_in_1_gga4(X, Y, Z, add_3_out_gga3(X, Y, Z)) -> add_3_out_gga3(s_11(X), Y, s_11(Z))
if_mult_3_in_2_gga5(X, Y, R, Z, add_3_out_gga3(Y, Z, R)) -> mult_3_out_gga3(s_11(X), Y, R)
if_evaluate_2_in_9_ga6(X, Y, Z, X1, Y1, mult_3_out_gga3(X1, Y1, Z)) -> evaluate_2_out_ga2(*2(X, Y), Z)
if_evaluate_2_in_4_ga4(X, Y, Z, evaluate_2_out_ga2(X, X1)) -> if_evaluate_2_in_5_ga5(X, Y, Z, X1, evaluate_2_in_ga2(Y, Y1))
if_evaluate_2_in_5_ga5(X, Y, Z, X1, evaluate_2_out_ga2(Y, Y1)) -> if_evaluate_2_in_6_ga6(X, Y, Z, X1, Y1, sub_3_in_gga3(X1, Y1, Z))
sub_3_in_gga3(s_11(X), s_11(Y), Z) -> if_sub_3_in_1_gga4(X, Y, Z, sub_3_in_gga3(X, Y, Z))
sub_3_in_gga3(X, 0_0, X) -> sub_3_out_gga3(X, 0_0, X)
if_sub_3_in_1_gga4(X, Y, Z, sub_3_out_gga3(X, Y, Z)) -> sub_3_out_gga3(s_11(X), s_11(Y), Z)
if_evaluate_2_in_6_ga6(X, Y, Z, X1, Y1, sub_3_out_gga3(X1, Y1, Z)) -> evaluate_2_out_ga2(-2(X, Y), Z)
if_evaluate_2_in_1_ga4(X, Y, Z, evaluate_2_out_ga2(X, X1)) -> if_evaluate_2_in_2_ga5(X, Y, Z, X1, evaluate_2_in_ga2(Y, Y1))
if_evaluate_2_in_2_ga5(X, Y, Z, X1, evaluate_2_out_ga2(Y, Y1)) -> if_evaluate_2_in_3_ga6(X, Y, Z, X1, Y1, add_3_in_gga3(X1, Y1, Z))
if_evaluate_2_in_3_ga6(X, Y, Z, X1, Y1, add_3_out_gga3(X1, Y1, Z)) -> evaluate_2_out_ga2(+2(X, Y), Z)
if_myis_2_in_1_ag3(Z, X, evaluate_2_out_ga2(X, Z)) -> myis_2_out_ag2(Z, X)

The argument filtering Pi contains the following mapping:
myis_2_in_ag2(x1, x2)  =  myis_2_in_ag1(x2)
+2(x1, x2)  =  +2(x1, x2)
-2(x1, x2)  =  -2(x1, x2)
*2(x1, x2)  =  *2(x1, x2)
s_11(x1)  =  s_11(x1)
0_0  =  0_0
if_myis_2_in_1_ag3(x1, x2, x3)  =  if_myis_2_in_1_ag1(x3)
evaluate_2_in_ga2(x1, x2)  =  evaluate_2_in_ga1(x1)
if_evaluate_2_in_1_ga4(x1, x2, x3, x4)  =  if_evaluate_2_in_1_ga2(x2, x4)
if_evaluate_2_in_4_ga4(x1, x2, x3, x4)  =  if_evaluate_2_in_4_ga2(x2, x4)
if_evaluate_2_in_7_ga4(x1, x2, x3, x4)  =  if_evaluate_2_in_7_ga2(x2, x4)
if_evaluate_2_in_10_ga2(x1, x2)  =  if_evaluate_2_in_10_ga2(x1, x2)
integer_1_in_g1(x1)  =  integer_1_in_g1(x1)
if_integer_1_in_1_g2(x1, x2)  =  if_integer_1_in_1_g1(x2)
integer_1_out_g1(x1)  =  integer_1_out_g
evaluate_2_out_ga2(x1, x2)  =  evaluate_2_out_ga1(x2)
if_evaluate_2_in_8_ga5(x1, x2, x3, x4, x5)  =  if_evaluate_2_in_8_ga2(x4, x5)
if_evaluate_2_in_9_ga6(x1, x2, x3, x4, x5, x6)  =  if_evaluate_2_in_9_ga1(x6)
mult_3_in_gga3(x1, x2, x3)  =  mult_3_in_gga2(x1, x2)
if_mult_3_in_1_gga4(x1, x2, x3, x4)  =  if_mult_3_in_1_gga2(x2, x4)
mult_3_out_gga3(x1, x2, x3)  =  mult_3_out_gga1(x3)
if_mult_3_in_2_gga5(x1, x2, x3, x4, x5)  =  if_mult_3_in_2_gga1(x5)
add_3_in_gga3(x1, x2, x3)  =  add_3_in_gga2(x1, x2)
if_add_3_in_1_gga4(x1, x2, x3, x4)  =  if_add_3_in_1_gga1(x4)
add_3_out_gga3(x1, x2, x3)  =  add_3_out_gga1(x3)
if_evaluate_2_in_5_ga5(x1, x2, x3, x4, x5)  =  if_evaluate_2_in_5_ga2(x4, x5)
if_evaluate_2_in_6_ga6(x1, x2, x3, x4, x5, x6)  =  if_evaluate_2_in_6_ga1(x6)
sub_3_in_gga3(x1, x2, x3)  =  sub_3_in_gga2(x1, x2)
if_sub_3_in_1_gga4(x1, x2, x3, x4)  =  if_sub_3_in_1_gga1(x4)
sub_3_out_gga3(x1, x2, x3)  =  sub_3_out_gga1(x3)
if_evaluate_2_in_2_ga5(x1, x2, x3, x4, x5)  =  if_evaluate_2_in_2_ga2(x4, x5)
if_evaluate_2_in_3_ga6(x1, x2, x3, x4, x5, x6)  =  if_evaluate_2_in_3_ga1(x6)
myis_2_out_ag2(x1, x2)  =  myis_2_out_ag1(x1)


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

MYIS_2_IN_AG2(Z, X) -> IF_MYIS_2_IN_1_AG3(Z, X, evaluate_2_in_ga2(X, Z))
MYIS_2_IN_AG2(Z, X) -> EVALUATE_2_IN_GA2(X, Z)
EVALUATE_2_IN_GA2(+2(X, Y), Z) -> IF_EVALUATE_2_IN_1_GA4(X, Y, Z, evaluate_2_in_ga2(X, X1))
EVALUATE_2_IN_GA2(+2(X, Y), Z) -> EVALUATE_2_IN_GA2(X, X1)
EVALUATE_2_IN_GA2(-2(X, Y), Z) -> IF_EVALUATE_2_IN_4_GA4(X, Y, Z, evaluate_2_in_ga2(X, X1))
EVALUATE_2_IN_GA2(-2(X, Y), Z) -> EVALUATE_2_IN_GA2(X, X1)
EVALUATE_2_IN_GA2(*2(X, Y), Z) -> IF_EVALUATE_2_IN_7_GA4(X, Y, Z, evaluate_2_in_ga2(X, X1))
EVALUATE_2_IN_GA2(*2(X, Y), Z) -> EVALUATE_2_IN_GA2(X, X1)
EVALUATE_2_IN_GA2(X, X) -> IF_EVALUATE_2_IN_10_GA2(X, integer_1_in_g1(X))
EVALUATE_2_IN_GA2(X, X) -> INTEGER_1_IN_G1(X)
INTEGER_1_IN_G1(s_11(X)) -> IF_INTEGER_1_IN_1_G2(X, integer_1_in_g1(X))
INTEGER_1_IN_G1(s_11(X)) -> INTEGER_1_IN_G1(X)
IF_EVALUATE_2_IN_7_GA4(X, Y, Z, evaluate_2_out_ga2(X, X1)) -> IF_EVALUATE_2_IN_8_GA5(X, Y, Z, X1, evaluate_2_in_ga2(Y, Y1))
IF_EVALUATE_2_IN_7_GA4(X, Y, Z, evaluate_2_out_ga2(X, X1)) -> EVALUATE_2_IN_GA2(Y, Y1)
IF_EVALUATE_2_IN_8_GA5(X, Y, Z, X1, evaluate_2_out_ga2(Y, Y1)) -> IF_EVALUATE_2_IN_9_GA6(X, Y, Z, X1, Y1, mult_3_in_gga3(X1, Y1, Z))
IF_EVALUATE_2_IN_8_GA5(X, Y, Z, X1, evaluate_2_out_ga2(Y, Y1)) -> MULT_3_IN_GGA3(X1, Y1, Z)
MULT_3_IN_GGA3(s_11(X), Y, R) -> IF_MULT_3_IN_1_GGA4(X, Y, R, mult_3_in_gga3(X, Y, Z))
MULT_3_IN_GGA3(s_11(X), Y, R) -> MULT_3_IN_GGA3(X, Y, Z)
IF_MULT_3_IN_1_GGA4(X, Y, R, mult_3_out_gga3(X, Y, Z)) -> IF_MULT_3_IN_2_GGA5(X, Y, R, Z, add_3_in_gga3(Y, Z, R))
IF_MULT_3_IN_1_GGA4(X, Y, R, mult_3_out_gga3(X, Y, Z)) -> ADD_3_IN_GGA3(Y, Z, R)
ADD_3_IN_GGA3(s_11(X), Y, s_11(Z)) -> IF_ADD_3_IN_1_GGA4(X, Y, Z, add_3_in_gga3(X, Y, Z))
ADD_3_IN_GGA3(s_11(X), Y, s_11(Z)) -> ADD_3_IN_GGA3(X, Y, Z)
IF_EVALUATE_2_IN_4_GA4(X, Y, Z, evaluate_2_out_ga2(X, X1)) -> IF_EVALUATE_2_IN_5_GA5(X, Y, Z, X1, evaluate_2_in_ga2(Y, Y1))
IF_EVALUATE_2_IN_4_GA4(X, Y, Z, evaluate_2_out_ga2(X, X1)) -> EVALUATE_2_IN_GA2(Y, Y1)
IF_EVALUATE_2_IN_5_GA5(X, Y, Z, X1, evaluate_2_out_ga2(Y, Y1)) -> IF_EVALUATE_2_IN_6_GA6(X, Y, Z, X1, Y1, sub_3_in_gga3(X1, Y1, Z))
IF_EVALUATE_2_IN_5_GA5(X, Y, Z, X1, evaluate_2_out_ga2(Y, Y1)) -> SUB_3_IN_GGA3(X1, Y1, Z)
SUB_3_IN_GGA3(s_11(X), s_11(Y), Z) -> IF_SUB_3_IN_1_GGA4(X, Y, Z, sub_3_in_gga3(X, Y, Z))
SUB_3_IN_GGA3(s_11(X), s_11(Y), Z) -> SUB_3_IN_GGA3(X, Y, Z)
IF_EVALUATE_2_IN_1_GA4(X, Y, Z, evaluate_2_out_ga2(X, X1)) -> IF_EVALUATE_2_IN_2_GA5(X, Y, Z, X1, evaluate_2_in_ga2(Y, Y1))
IF_EVALUATE_2_IN_1_GA4(X, Y, Z, evaluate_2_out_ga2(X, X1)) -> EVALUATE_2_IN_GA2(Y, Y1)
IF_EVALUATE_2_IN_2_GA5(X, Y, Z, X1, evaluate_2_out_ga2(Y, Y1)) -> IF_EVALUATE_2_IN_3_GA6(X, Y, Z, X1, Y1, add_3_in_gga3(X1, Y1, Z))
IF_EVALUATE_2_IN_2_GA5(X, Y, Z, X1, evaluate_2_out_ga2(Y, Y1)) -> ADD_3_IN_GGA3(X1, Y1, Z)

The TRS R consists of the following rules:

myis_2_in_ag2(Z, X) -> if_myis_2_in_1_ag3(Z, X, evaluate_2_in_ga2(X, Z))
evaluate_2_in_ga2(+2(X, Y), Z) -> if_evaluate_2_in_1_ga4(X, Y, Z, evaluate_2_in_ga2(X, X1))
evaluate_2_in_ga2(-2(X, Y), Z) -> if_evaluate_2_in_4_ga4(X, Y, Z, evaluate_2_in_ga2(X, X1))
evaluate_2_in_ga2(*2(X, Y), Z) -> if_evaluate_2_in_7_ga4(X, Y, Z, evaluate_2_in_ga2(X, X1))
evaluate_2_in_ga2(X, X) -> if_evaluate_2_in_10_ga2(X, integer_1_in_g1(X))
integer_1_in_g1(s_11(X)) -> if_integer_1_in_1_g2(X, integer_1_in_g1(X))
integer_1_in_g1(0_0) -> integer_1_out_g1(0_0)
if_integer_1_in_1_g2(X, integer_1_out_g1(X)) -> integer_1_out_g1(s_11(X))
if_evaluate_2_in_10_ga2(X, integer_1_out_g1(X)) -> evaluate_2_out_ga2(X, X)
if_evaluate_2_in_7_ga4(X, Y, Z, evaluate_2_out_ga2(X, X1)) -> if_evaluate_2_in_8_ga5(X, Y, Z, X1, evaluate_2_in_ga2(Y, Y1))
if_evaluate_2_in_8_ga5(X, Y, Z, X1, evaluate_2_out_ga2(Y, Y1)) -> if_evaluate_2_in_9_ga6(X, Y, Z, X1, Y1, mult_3_in_gga3(X1, Y1, Z))
mult_3_in_gga3(s_11(X), Y, R) -> if_mult_3_in_1_gga4(X, Y, R, mult_3_in_gga3(X, Y, Z))
mult_3_in_gga3(0_0, Y, 0_0) -> mult_3_out_gga3(0_0, Y, 0_0)
if_mult_3_in_1_gga4(X, Y, R, mult_3_out_gga3(X, Y, Z)) -> if_mult_3_in_2_gga5(X, Y, R, Z, add_3_in_gga3(Y, Z, R))
add_3_in_gga3(s_11(X), Y, s_11(Z)) -> if_add_3_in_1_gga4(X, Y, Z, add_3_in_gga3(X, Y, Z))
add_3_in_gga3(0_0, X, X) -> add_3_out_gga3(0_0, X, X)
if_add_3_in_1_gga4(X, Y, Z, add_3_out_gga3(X, Y, Z)) -> add_3_out_gga3(s_11(X), Y, s_11(Z))
if_mult_3_in_2_gga5(X, Y, R, Z, add_3_out_gga3(Y, Z, R)) -> mult_3_out_gga3(s_11(X), Y, R)
if_evaluate_2_in_9_ga6(X, Y, Z, X1, Y1, mult_3_out_gga3(X1, Y1, Z)) -> evaluate_2_out_ga2(*2(X, Y), Z)
if_evaluate_2_in_4_ga4(X, Y, Z, evaluate_2_out_ga2(X, X1)) -> if_evaluate_2_in_5_ga5(X, Y, Z, X1, evaluate_2_in_ga2(Y, Y1))
if_evaluate_2_in_5_ga5(X, Y, Z, X1, evaluate_2_out_ga2(Y, Y1)) -> if_evaluate_2_in_6_ga6(X, Y, Z, X1, Y1, sub_3_in_gga3(X1, Y1, Z))
sub_3_in_gga3(s_11(X), s_11(Y), Z) -> if_sub_3_in_1_gga4(X, Y, Z, sub_3_in_gga3(X, Y, Z))
sub_3_in_gga3(X, 0_0, X) -> sub_3_out_gga3(X, 0_0, X)
if_sub_3_in_1_gga4(X, Y, Z, sub_3_out_gga3(X, Y, Z)) -> sub_3_out_gga3(s_11(X), s_11(Y), Z)
if_evaluate_2_in_6_ga6(X, Y, Z, X1, Y1, sub_3_out_gga3(X1, Y1, Z)) -> evaluate_2_out_ga2(-2(X, Y), Z)
if_evaluate_2_in_1_ga4(X, Y, Z, evaluate_2_out_ga2(X, X1)) -> if_evaluate_2_in_2_ga5(X, Y, Z, X1, evaluate_2_in_ga2(Y, Y1))
if_evaluate_2_in_2_ga5(X, Y, Z, X1, evaluate_2_out_ga2(Y, Y1)) -> if_evaluate_2_in_3_ga6(X, Y, Z, X1, Y1, add_3_in_gga3(X1, Y1, Z))
if_evaluate_2_in_3_ga6(X, Y, Z, X1, Y1, add_3_out_gga3(X1, Y1, Z)) -> evaluate_2_out_ga2(+2(X, Y), Z)
if_myis_2_in_1_ag3(Z, X, evaluate_2_out_ga2(X, Z)) -> myis_2_out_ag2(Z, X)

The argument filtering Pi contains the following mapping:
myis_2_in_ag2(x1, x2)  =  myis_2_in_ag1(x2)
+2(x1, x2)  =  +2(x1, x2)
-2(x1, x2)  =  -2(x1, x2)
*2(x1, x2)  =  *2(x1, x2)
s_11(x1)  =  s_11(x1)
0_0  =  0_0
if_myis_2_in_1_ag3(x1, x2, x3)  =  if_myis_2_in_1_ag1(x3)
evaluate_2_in_ga2(x1, x2)  =  evaluate_2_in_ga1(x1)
if_evaluate_2_in_1_ga4(x1, x2, x3, x4)  =  if_evaluate_2_in_1_ga2(x2, x4)
if_evaluate_2_in_4_ga4(x1, x2, x3, x4)  =  if_evaluate_2_in_4_ga2(x2, x4)
if_evaluate_2_in_7_ga4(x1, x2, x3, x4)  =  if_evaluate_2_in_7_ga2(x2, x4)
if_evaluate_2_in_10_ga2(x1, x2)  =  if_evaluate_2_in_10_ga2(x1, x2)
integer_1_in_g1(x1)  =  integer_1_in_g1(x1)
if_integer_1_in_1_g2(x1, x2)  =  if_integer_1_in_1_g1(x2)
integer_1_out_g1(x1)  =  integer_1_out_g
evaluate_2_out_ga2(x1, x2)  =  evaluate_2_out_ga1(x2)
if_evaluate_2_in_8_ga5(x1, x2, x3, x4, x5)  =  if_evaluate_2_in_8_ga2(x4, x5)
if_evaluate_2_in_9_ga6(x1, x2, x3, x4, x5, x6)  =  if_evaluate_2_in_9_ga1(x6)
mult_3_in_gga3(x1, x2, x3)  =  mult_3_in_gga2(x1, x2)
if_mult_3_in_1_gga4(x1, x2, x3, x4)  =  if_mult_3_in_1_gga2(x2, x4)
mult_3_out_gga3(x1, x2, x3)  =  mult_3_out_gga1(x3)
if_mult_3_in_2_gga5(x1, x2, x3, x4, x5)  =  if_mult_3_in_2_gga1(x5)
add_3_in_gga3(x1, x2, x3)  =  add_3_in_gga2(x1, x2)
if_add_3_in_1_gga4(x1, x2, x3, x4)  =  if_add_3_in_1_gga1(x4)
add_3_out_gga3(x1, x2, x3)  =  add_3_out_gga1(x3)
if_evaluate_2_in_5_ga5(x1, x2, x3, x4, x5)  =  if_evaluate_2_in_5_ga2(x4, x5)
if_evaluate_2_in_6_ga6(x1, x2, x3, x4, x5, x6)  =  if_evaluate_2_in_6_ga1(x6)
sub_3_in_gga3(x1, x2, x3)  =  sub_3_in_gga2(x1, x2)
if_sub_3_in_1_gga4(x1, x2, x3, x4)  =  if_sub_3_in_1_gga1(x4)
sub_3_out_gga3(x1, x2, x3)  =  sub_3_out_gga1(x3)
if_evaluate_2_in_2_ga5(x1, x2, x3, x4, x5)  =  if_evaluate_2_in_2_ga2(x4, x5)
if_evaluate_2_in_3_ga6(x1, x2, x3, x4, x5, x6)  =  if_evaluate_2_in_3_ga1(x6)
myis_2_out_ag2(x1, x2)  =  myis_2_out_ag1(x1)
IF_MULT_3_IN_2_GGA5(x1, x2, x3, x4, x5)  =  IF_MULT_3_IN_2_GGA1(x5)
MYIS_2_IN_AG2(x1, x2)  =  MYIS_2_IN_AG1(x2)
IF_SUB_3_IN_1_GGA4(x1, x2, x3, x4)  =  IF_SUB_3_IN_1_GGA1(x4)
ADD_3_IN_GGA3(x1, x2, x3)  =  ADD_3_IN_GGA2(x1, x2)
EVALUATE_2_IN_GA2(x1, x2)  =  EVALUATE_2_IN_GA1(x1)
IF_EVALUATE_2_IN_5_GA5(x1, x2, x3, x4, x5)  =  IF_EVALUATE_2_IN_5_GA2(x4, x5)
IF_EVALUATE_2_IN_10_GA2(x1, x2)  =  IF_EVALUATE_2_IN_10_GA2(x1, x2)
IF_EVALUATE_2_IN_4_GA4(x1, x2, x3, x4)  =  IF_EVALUATE_2_IN_4_GA2(x2, x4)
IF_EVALUATE_2_IN_9_GA6(x1, x2, x3, x4, x5, x6)  =  IF_EVALUATE_2_IN_9_GA1(x6)
IF_MYIS_2_IN_1_AG3(x1, x2, x3)  =  IF_MYIS_2_IN_1_AG1(x3)
IF_ADD_3_IN_1_GGA4(x1, x2, x3, x4)  =  IF_ADD_3_IN_1_GGA1(x4)
MULT_3_IN_GGA3(x1, x2, x3)  =  MULT_3_IN_GGA2(x1, x2)
IF_MULT_3_IN_1_GGA4(x1, x2, x3, x4)  =  IF_MULT_3_IN_1_GGA2(x2, x4)
INTEGER_1_IN_G1(x1)  =  INTEGER_1_IN_G1(x1)
IF_EVALUATE_2_IN_8_GA5(x1, x2, x3, x4, x5)  =  IF_EVALUATE_2_IN_8_GA2(x4, x5)
IF_EVALUATE_2_IN_3_GA6(x1, x2, x3, x4, x5, x6)  =  IF_EVALUATE_2_IN_3_GA1(x6)
IF_EVALUATE_2_IN_7_GA4(x1, x2, x3, x4)  =  IF_EVALUATE_2_IN_7_GA2(x2, x4)
IF_INTEGER_1_IN_1_G2(x1, x2)  =  IF_INTEGER_1_IN_1_G1(x2)
IF_EVALUATE_2_IN_1_GA4(x1, x2, x3, x4)  =  IF_EVALUATE_2_IN_1_GA2(x2, x4)
IF_EVALUATE_2_IN_2_GA5(x1, x2, x3, x4, x5)  =  IF_EVALUATE_2_IN_2_GA2(x4, x5)
IF_EVALUATE_2_IN_6_GA6(x1, x2, x3, x4, x5, x6)  =  IF_EVALUATE_2_IN_6_GA1(x6)
SUB_3_IN_GGA3(x1, x2, x3)  =  SUB_3_IN_GGA2(x1, x2)

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

↳ PROLOG
  ↳ UnrequestedClauseRemoverProof
    ↳ PROLOG
      ↳ PrologToPiTRSProof
        ↳ PiTRS
          ↳ DependencyPairsProof
            ↳ PiDP
              ↳ DependencyGraphProof

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

MYIS_2_IN_AG2(Z, X) -> IF_MYIS_2_IN_1_AG3(Z, X, evaluate_2_in_ga2(X, Z))
MYIS_2_IN_AG2(Z, X) -> EVALUATE_2_IN_GA2(X, Z)
EVALUATE_2_IN_GA2(+2(X, Y), Z) -> IF_EVALUATE_2_IN_1_GA4(X, Y, Z, evaluate_2_in_ga2(X, X1))
EVALUATE_2_IN_GA2(+2(X, Y), Z) -> EVALUATE_2_IN_GA2(X, X1)
EVALUATE_2_IN_GA2(-2(X, Y), Z) -> IF_EVALUATE_2_IN_4_GA4(X, Y, Z, evaluate_2_in_ga2(X, X1))
EVALUATE_2_IN_GA2(-2(X, Y), Z) -> EVALUATE_2_IN_GA2(X, X1)
EVALUATE_2_IN_GA2(*2(X, Y), Z) -> IF_EVALUATE_2_IN_7_GA4(X, Y, Z, evaluate_2_in_ga2(X, X1))
EVALUATE_2_IN_GA2(*2(X, Y), Z) -> EVALUATE_2_IN_GA2(X, X1)
EVALUATE_2_IN_GA2(X, X) -> IF_EVALUATE_2_IN_10_GA2(X, integer_1_in_g1(X))
EVALUATE_2_IN_GA2(X, X) -> INTEGER_1_IN_G1(X)
INTEGER_1_IN_G1(s_11(X)) -> IF_INTEGER_1_IN_1_G2(X, integer_1_in_g1(X))
INTEGER_1_IN_G1(s_11(X)) -> INTEGER_1_IN_G1(X)
IF_EVALUATE_2_IN_7_GA4(X, Y, Z, evaluate_2_out_ga2(X, X1)) -> IF_EVALUATE_2_IN_8_GA5(X, Y, Z, X1, evaluate_2_in_ga2(Y, Y1))
IF_EVALUATE_2_IN_7_GA4(X, Y, Z, evaluate_2_out_ga2(X, X1)) -> EVALUATE_2_IN_GA2(Y, Y1)
IF_EVALUATE_2_IN_8_GA5(X, Y, Z, X1, evaluate_2_out_ga2(Y, Y1)) -> IF_EVALUATE_2_IN_9_GA6(X, Y, Z, X1, Y1, mult_3_in_gga3(X1, Y1, Z))
IF_EVALUATE_2_IN_8_GA5(X, Y, Z, X1, evaluate_2_out_ga2(Y, Y1)) -> MULT_3_IN_GGA3(X1, Y1, Z)
MULT_3_IN_GGA3(s_11(X), Y, R) -> IF_MULT_3_IN_1_GGA4(X, Y, R, mult_3_in_gga3(X, Y, Z))
MULT_3_IN_GGA3(s_11(X), Y, R) -> MULT_3_IN_GGA3(X, Y, Z)
IF_MULT_3_IN_1_GGA4(X, Y, R, mult_3_out_gga3(X, Y, Z)) -> IF_MULT_3_IN_2_GGA5(X, Y, R, Z, add_3_in_gga3(Y, Z, R))
IF_MULT_3_IN_1_GGA4(X, Y, R, mult_3_out_gga3(X, Y, Z)) -> ADD_3_IN_GGA3(Y, Z, R)
ADD_3_IN_GGA3(s_11(X), Y, s_11(Z)) -> IF_ADD_3_IN_1_GGA4(X, Y, Z, add_3_in_gga3(X, Y, Z))
ADD_3_IN_GGA3(s_11(X), Y, s_11(Z)) -> ADD_3_IN_GGA3(X, Y, Z)
IF_EVALUATE_2_IN_4_GA4(X, Y, Z, evaluate_2_out_ga2(X, X1)) -> IF_EVALUATE_2_IN_5_GA5(X, Y, Z, X1, evaluate_2_in_ga2(Y, Y1))
IF_EVALUATE_2_IN_4_GA4(X, Y, Z, evaluate_2_out_ga2(X, X1)) -> EVALUATE_2_IN_GA2(Y, Y1)
IF_EVALUATE_2_IN_5_GA5(X, Y, Z, X1, evaluate_2_out_ga2(Y, Y1)) -> IF_EVALUATE_2_IN_6_GA6(X, Y, Z, X1, Y1, sub_3_in_gga3(X1, Y1, Z))
IF_EVALUATE_2_IN_5_GA5(X, Y, Z, X1, evaluate_2_out_ga2(Y, Y1)) -> SUB_3_IN_GGA3(X1, Y1, Z)
SUB_3_IN_GGA3(s_11(X), s_11(Y), Z) -> IF_SUB_3_IN_1_GGA4(X, Y, Z, sub_3_in_gga3(X, Y, Z))
SUB_3_IN_GGA3(s_11(X), s_11(Y), Z) -> SUB_3_IN_GGA3(X, Y, Z)
IF_EVALUATE_2_IN_1_GA4(X, Y, Z, evaluate_2_out_ga2(X, X1)) -> IF_EVALUATE_2_IN_2_GA5(X, Y, Z, X1, evaluate_2_in_ga2(Y, Y1))
IF_EVALUATE_2_IN_1_GA4(X, Y, Z, evaluate_2_out_ga2(X, X1)) -> EVALUATE_2_IN_GA2(Y, Y1)
IF_EVALUATE_2_IN_2_GA5(X, Y, Z, X1, evaluate_2_out_ga2(Y, Y1)) -> IF_EVALUATE_2_IN_3_GA6(X, Y, Z, X1, Y1, add_3_in_gga3(X1, Y1, Z))
IF_EVALUATE_2_IN_2_GA5(X, Y, Z, X1, evaluate_2_out_ga2(Y, Y1)) -> ADD_3_IN_GGA3(X1, Y1, Z)

The TRS R consists of the following rules:

myis_2_in_ag2(Z, X) -> if_myis_2_in_1_ag3(Z, X, evaluate_2_in_ga2(X, Z))
evaluate_2_in_ga2(+2(X, Y), Z) -> if_evaluate_2_in_1_ga4(X, Y, Z, evaluate_2_in_ga2(X, X1))
evaluate_2_in_ga2(-2(X, Y), Z) -> if_evaluate_2_in_4_ga4(X, Y, Z, evaluate_2_in_ga2(X, X1))
evaluate_2_in_ga2(*2(X, Y), Z) -> if_evaluate_2_in_7_ga4(X, Y, Z, evaluate_2_in_ga2(X, X1))
evaluate_2_in_ga2(X, X) -> if_evaluate_2_in_10_ga2(X, integer_1_in_g1(X))
integer_1_in_g1(s_11(X)) -> if_integer_1_in_1_g2(X, integer_1_in_g1(X))
integer_1_in_g1(0_0) -> integer_1_out_g1(0_0)
if_integer_1_in_1_g2(X, integer_1_out_g1(X)) -> integer_1_out_g1(s_11(X))
if_evaluate_2_in_10_ga2(X, integer_1_out_g1(X)) -> evaluate_2_out_ga2(X, X)
if_evaluate_2_in_7_ga4(X, Y, Z, evaluate_2_out_ga2(X, X1)) -> if_evaluate_2_in_8_ga5(X, Y, Z, X1, evaluate_2_in_ga2(Y, Y1))
if_evaluate_2_in_8_ga5(X, Y, Z, X1, evaluate_2_out_ga2(Y, Y1)) -> if_evaluate_2_in_9_ga6(X, Y, Z, X1, Y1, mult_3_in_gga3(X1, Y1, Z))
mult_3_in_gga3(s_11(X), Y, R) -> if_mult_3_in_1_gga4(X, Y, R, mult_3_in_gga3(X, Y, Z))
mult_3_in_gga3(0_0, Y, 0_0) -> mult_3_out_gga3(0_0, Y, 0_0)
if_mult_3_in_1_gga4(X, Y, R, mult_3_out_gga3(X, Y, Z)) -> if_mult_3_in_2_gga5(X, Y, R, Z, add_3_in_gga3(Y, Z, R))
add_3_in_gga3(s_11(X), Y, s_11(Z)) -> if_add_3_in_1_gga4(X, Y, Z, add_3_in_gga3(X, Y, Z))
add_3_in_gga3(0_0, X, X) -> add_3_out_gga3(0_0, X, X)
if_add_3_in_1_gga4(X, Y, Z, add_3_out_gga3(X, Y, Z)) -> add_3_out_gga3(s_11(X), Y, s_11(Z))
if_mult_3_in_2_gga5(X, Y, R, Z, add_3_out_gga3(Y, Z, R)) -> mult_3_out_gga3(s_11(X), Y, R)
if_evaluate_2_in_9_ga6(X, Y, Z, X1, Y1, mult_3_out_gga3(X1, Y1, Z)) -> evaluate_2_out_ga2(*2(X, Y), Z)
if_evaluate_2_in_4_ga4(X, Y, Z, evaluate_2_out_ga2(X, X1)) -> if_evaluate_2_in_5_ga5(X, Y, Z, X1, evaluate_2_in_ga2(Y, Y1))
if_evaluate_2_in_5_ga5(X, Y, Z, X1, evaluate_2_out_ga2(Y, Y1)) -> if_evaluate_2_in_6_ga6(X, Y, Z, X1, Y1, sub_3_in_gga3(X1, Y1, Z))
sub_3_in_gga3(s_11(X), s_11(Y), Z) -> if_sub_3_in_1_gga4(X, Y, Z, sub_3_in_gga3(X, Y, Z))
sub_3_in_gga3(X, 0_0, X) -> sub_3_out_gga3(X, 0_0, X)
if_sub_3_in_1_gga4(X, Y, Z, sub_3_out_gga3(X, Y, Z)) -> sub_3_out_gga3(s_11(X), s_11(Y), Z)
if_evaluate_2_in_6_ga6(X, Y, Z, X1, Y1, sub_3_out_gga3(X1, Y1, Z)) -> evaluate_2_out_ga2(-2(X, Y), Z)
if_evaluate_2_in_1_ga4(X, Y, Z, evaluate_2_out_ga2(X, X1)) -> if_evaluate_2_in_2_ga5(X, Y, Z, X1, evaluate_2_in_ga2(Y, Y1))
if_evaluate_2_in_2_ga5(X, Y, Z, X1, evaluate_2_out_ga2(Y, Y1)) -> if_evaluate_2_in_3_ga6(X, Y, Z, X1, Y1, add_3_in_gga3(X1, Y1, Z))
if_evaluate_2_in_3_ga6(X, Y, Z, X1, Y1, add_3_out_gga3(X1, Y1, Z)) -> evaluate_2_out_ga2(+2(X, Y), Z)
if_myis_2_in_1_ag3(Z, X, evaluate_2_out_ga2(X, Z)) -> myis_2_out_ag2(Z, X)

The argument filtering Pi contains the following mapping:
myis_2_in_ag2(x1, x2)  =  myis_2_in_ag1(x2)
+2(x1, x2)  =  +2(x1, x2)
-2(x1, x2)  =  -2(x1, x2)
*2(x1, x2)  =  *2(x1, x2)
s_11(x1)  =  s_11(x1)
0_0  =  0_0
if_myis_2_in_1_ag3(x1, x2, x3)  =  if_myis_2_in_1_ag1(x3)
evaluate_2_in_ga2(x1, x2)  =  evaluate_2_in_ga1(x1)
if_evaluate_2_in_1_ga4(x1, x2, x3, x4)  =  if_evaluate_2_in_1_ga2(x2, x4)
if_evaluate_2_in_4_ga4(x1, x2, x3, x4)  =  if_evaluate_2_in_4_ga2(x2, x4)
if_evaluate_2_in_7_ga4(x1, x2, x3, x4)  =  if_evaluate_2_in_7_ga2(x2, x4)
if_evaluate_2_in_10_ga2(x1, x2)  =  if_evaluate_2_in_10_ga2(x1, x2)
integer_1_in_g1(x1)  =  integer_1_in_g1(x1)
if_integer_1_in_1_g2(x1, x2)  =  if_integer_1_in_1_g1(x2)
integer_1_out_g1(x1)  =  integer_1_out_g
evaluate_2_out_ga2(x1, x2)  =  evaluate_2_out_ga1(x2)
if_evaluate_2_in_8_ga5(x1, x2, x3, x4, x5)  =  if_evaluate_2_in_8_ga2(x4, x5)
if_evaluate_2_in_9_ga6(x1, x2, x3, x4, x5, x6)  =  if_evaluate_2_in_9_ga1(x6)
mult_3_in_gga3(x1, x2, x3)  =  mult_3_in_gga2(x1, x2)
if_mult_3_in_1_gga4(x1, x2, x3, x4)  =  if_mult_3_in_1_gga2(x2, x4)
mult_3_out_gga3(x1, x2, x3)  =  mult_3_out_gga1(x3)
if_mult_3_in_2_gga5(x1, x2, x3, x4, x5)  =  if_mult_3_in_2_gga1(x5)
add_3_in_gga3(x1, x2, x3)  =  add_3_in_gga2(x1, x2)
if_add_3_in_1_gga4(x1, x2, x3, x4)  =  if_add_3_in_1_gga1(x4)
add_3_out_gga3(x1, x2, x3)  =  add_3_out_gga1(x3)
if_evaluate_2_in_5_ga5(x1, x2, x3, x4, x5)  =  if_evaluate_2_in_5_ga2(x4, x5)
if_evaluate_2_in_6_ga6(x1, x2, x3, x4, x5, x6)  =  if_evaluate_2_in_6_ga1(x6)
sub_3_in_gga3(x1, x2, x3)  =  sub_3_in_gga2(x1, x2)
if_sub_3_in_1_gga4(x1, x2, x3, x4)  =  if_sub_3_in_1_gga1(x4)
sub_3_out_gga3(x1, x2, x3)  =  sub_3_out_gga1(x3)
if_evaluate_2_in_2_ga5(x1, x2, x3, x4, x5)  =  if_evaluate_2_in_2_ga2(x4, x5)
if_evaluate_2_in_3_ga6(x1, x2, x3, x4, x5, x6)  =  if_evaluate_2_in_3_ga1(x6)
myis_2_out_ag2(x1, x2)  =  myis_2_out_ag1(x1)
IF_MULT_3_IN_2_GGA5(x1, x2, x3, x4, x5)  =  IF_MULT_3_IN_2_GGA1(x5)
MYIS_2_IN_AG2(x1, x2)  =  MYIS_2_IN_AG1(x2)
IF_SUB_3_IN_1_GGA4(x1, x2, x3, x4)  =  IF_SUB_3_IN_1_GGA1(x4)
ADD_3_IN_GGA3(x1, x2, x3)  =  ADD_3_IN_GGA2(x1, x2)
EVALUATE_2_IN_GA2(x1, x2)  =  EVALUATE_2_IN_GA1(x1)
IF_EVALUATE_2_IN_5_GA5(x1, x2, x3, x4, x5)  =  IF_EVALUATE_2_IN_5_GA2(x4, x5)
IF_EVALUATE_2_IN_10_GA2(x1, x2)  =  IF_EVALUATE_2_IN_10_GA2(x1, x2)
IF_EVALUATE_2_IN_4_GA4(x1, x2, x3, x4)  =  IF_EVALUATE_2_IN_4_GA2(x2, x4)
IF_EVALUATE_2_IN_9_GA6(x1, x2, x3, x4, x5, x6)  =  IF_EVALUATE_2_IN_9_GA1(x6)
IF_MYIS_2_IN_1_AG3(x1, x2, x3)  =  IF_MYIS_2_IN_1_AG1(x3)
IF_ADD_3_IN_1_GGA4(x1, x2, x3, x4)  =  IF_ADD_3_IN_1_GGA1(x4)
MULT_3_IN_GGA3(x1, x2, x3)  =  MULT_3_IN_GGA2(x1, x2)
IF_MULT_3_IN_1_GGA4(x1, x2, x3, x4)  =  IF_MULT_3_IN_1_GGA2(x2, x4)
INTEGER_1_IN_G1(x1)  =  INTEGER_1_IN_G1(x1)
IF_EVALUATE_2_IN_8_GA5(x1, x2, x3, x4, x5)  =  IF_EVALUATE_2_IN_8_GA2(x4, x5)
IF_EVALUATE_2_IN_3_GA6(x1, x2, x3, x4, x5, x6)  =  IF_EVALUATE_2_IN_3_GA1(x6)
IF_EVALUATE_2_IN_7_GA4(x1, x2, x3, x4)  =  IF_EVALUATE_2_IN_7_GA2(x2, x4)
IF_INTEGER_1_IN_1_G2(x1, x2)  =  IF_INTEGER_1_IN_1_G1(x2)
IF_EVALUATE_2_IN_1_GA4(x1, x2, x3, x4)  =  IF_EVALUATE_2_IN_1_GA2(x2, x4)
IF_EVALUATE_2_IN_2_GA5(x1, x2, x3, x4, x5)  =  IF_EVALUATE_2_IN_2_GA2(x4, x5)
IF_EVALUATE_2_IN_6_GA6(x1, x2, x3, x4, x5, x6)  =  IF_EVALUATE_2_IN_6_GA1(x6)
SUB_3_IN_GGA3(x1, x2, x3)  =  SUB_3_IN_GGA2(x1, x2)

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

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

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

SUB_3_IN_GGA3(s_11(X), s_11(Y), Z) -> SUB_3_IN_GGA3(X, Y, Z)

The TRS R consists of the following rules:

myis_2_in_ag2(Z, X) -> if_myis_2_in_1_ag3(Z, X, evaluate_2_in_ga2(X, Z))
evaluate_2_in_ga2(+2(X, Y), Z) -> if_evaluate_2_in_1_ga4(X, Y, Z, evaluate_2_in_ga2(X, X1))
evaluate_2_in_ga2(-2(X, Y), Z) -> if_evaluate_2_in_4_ga4(X, Y, Z, evaluate_2_in_ga2(X, X1))
evaluate_2_in_ga2(*2(X, Y), Z) -> if_evaluate_2_in_7_ga4(X, Y, Z, evaluate_2_in_ga2(X, X1))
evaluate_2_in_ga2(X, X) -> if_evaluate_2_in_10_ga2(X, integer_1_in_g1(X))
integer_1_in_g1(s_11(X)) -> if_integer_1_in_1_g2(X, integer_1_in_g1(X))
integer_1_in_g1(0_0) -> integer_1_out_g1(0_0)
if_integer_1_in_1_g2(X, integer_1_out_g1(X)) -> integer_1_out_g1(s_11(X))
if_evaluate_2_in_10_ga2(X, integer_1_out_g1(X)) -> evaluate_2_out_ga2(X, X)
if_evaluate_2_in_7_ga4(X, Y, Z, evaluate_2_out_ga2(X, X1)) -> if_evaluate_2_in_8_ga5(X, Y, Z, X1, evaluate_2_in_ga2(Y, Y1))
if_evaluate_2_in_8_ga5(X, Y, Z, X1, evaluate_2_out_ga2(Y, Y1)) -> if_evaluate_2_in_9_ga6(X, Y, Z, X1, Y1, mult_3_in_gga3(X1, Y1, Z))
mult_3_in_gga3(s_11(X), Y, R) -> if_mult_3_in_1_gga4(X, Y, R, mult_3_in_gga3(X, Y, Z))
mult_3_in_gga3(0_0, Y, 0_0) -> mult_3_out_gga3(0_0, Y, 0_0)
if_mult_3_in_1_gga4(X, Y, R, mult_3_out_gga3(X, Y, Z)) -> if_mult_3_in_2_gga5(X, Y, R, Z, add_3_in_gga3(Y, Z, R))
add_3_in_gga3(s_11(X), Y, s_11(Z)) -> if_add_3_in_1_gga4(X, Y, Z, add_3_in_gga3(X, Y, Z))
add_3_in_gga3(0_0, X, X) -> add_3_out_gga3(0_0, X, X)
if_add_3_in_1_gga4(X, Y, Z, add_3_out_gga3(X, Y, Z)) -> add_3_out_gga3(s_11(X), Y, s_11(Z))
if_mult_3_in_2_gga5(X, Y, R, Z, add_3_out_gga3(Y, Z, R)) -> mult_3_out_gga3(s_11(X), Y, R)
if_evaluate_2_in_9_ga6(X, Y, Z, X1, Y1, mult_3_out_gga3(X1, Y1, Z)) -> evaluate_2_out_ga2(*2(X, Y), Z)
if_evaluate_2_in_4_ga4(X, Y, Z, evaluate_2_out_ga2(X, X1)) -> if_evaluate_2_in_5_ga5(X, Y, Z, X1, evaluate_2_in_ga2(Y, Y1))
if_evaluate_2_in_5_ga5(X, Y, Z, X1, evaluate_2_out_ga2(Y, Y1)) -> if_evaluate_2_in_6_ga6(X, Y, Z, X1, Y1, sub_3_in_gga3(X1, Y1, Z))
sub_3_in_gga3(s_11(X), s_11(Y), Z) -> if_sub_3_in_1_gga4(X, Y, Z, sub_3_in_gga3(X, Y, Z))
sub_3_in_gga3(X, 0_0, X) -> sub_3_out_gga3(X, 0_0, X)
if_sub_3_in_1_gga4(X, Y, Z, sub_3_out_gga3(X, Y, Z)) -> sub_3_out_gga3(s_11(X), s_11(Y), Z)
if_evaluate_2_in_6_ga6(X, Y, Z, X1, Y1, sub_3_out_gga3(X1, Y1, Z)) -> evaluate_2_out_ga2(-2(X, Y), Z)
if_evaluate_2_in_1_ga4(X, Y, Z, evaluate_2_out_ga2(X, X1)) -> if_evaluate_2_in_2_ga5(X, Y, Z, X1, evaluate_2_in_ga2(Y, Y1))
if_evaluate_2_in_2_ga5(X, Y, Z, X1, evaluate_2_out_ga2(Y, Y1)) -> if_evaluate_2_in_3_ga6(X, Y, Z, X1, Y1, add_3_in_gga3(X1, Y1, Z))
if_evaluate_2_in_3_ga6(X, Y, Z, X1, Y1, add_3_out_gga3(X1, Y1, Z)) -> evaluate_2_out_ga2(+2(X, Y), Z)
if_myis_2_in_1_ag3(Z, X, evaluate_2_out_ga2(X, Z)) -> myis_2_out_ag2(Z, X)

The argument filtering Pi contains the following mapping:
myis_2_in_ag2(x1, x2)  =  myis_2_in_ag1(x2)
+2(x1, x2)  =  +2(x1, x2)
-2(x1, x2)  =  -2(x1, x2)
*2(x1, x2)  =  *2(x1, x2)
s_11(x1)  =  s_11(x1)
0_0  =  0_0
if_myis_2_in_1_ag3(x1, x2, x3)  =  if_myis_2_in_1_ag1(x3)
evaluate_2_in_ga2(x1, x2)  =  evaluate_2_in_ga1(x1)
if_evaluate_2_in_1_ga4(x1, x2, x3, x4)  =  if_evaluate_2_in_1_ga2(x2, x4)
if_evaluate_2_in_4_ga4(x1, x2, x3, x4)  =  if_evaluate_2_in_4_ga2(x2, x4)
if_evaluate_2_in_7_ga4(x1, x2, x3, x4)  =  if_evaluate_2_in_7_ga2(x2, x4)
if_evaluate_2_in_10_ga2(x1, x2)  =  if_evaluate_2_in_10_ga2(x1, x2)
integer_1_in_g1(x1)  =  integer_1_in_g1(x1)
if_integer_1_in_1_g2(x1, x2)  =  if_integer_1_in_1_g1(x2)
integer_1_out_g1(x1)  =  integer_1_out_g
evaluate_2_out_ga2(x1, x2)  =  evaluate_2_out_ga1(x2)
if_evaluate_2_in_8_ga5(x1, x2, x3, x4, x5)  =  if_evaluate_2_in_8_ga2(x4, x5)
if_evaluate_2_in_9_ga6(x1, x2, x3, x4, x5, x6)  =  if_evaluate_2_in_9_ga1(x6)
mult_3_in_gga3(x1, x2, x3)  =  mult_3_in_gga2(x1, x2)
if_mult_3_in_1_gga4(x1, x2, x3, x4)  =  if_mult_3_in_1_gga2(x2, x4)
mult_3_out_gga3(x1, x2, x3)  =  mult_3_out_gga1(x3)
if_mult_3_in_2_gga5(x1, x2, x3, x4, x5)  =  if_mult_3_in_2_gga1(x5)
add_3_in_gga3(x1, x2, x3)  =  add_3_in_gga2(x1, x2)
if_add_3_in_1_gga4(x1, x2, x3, x4)  =  if_add_3_in_1_gga1(x4)
add_3_out_gga3(x1, x2, x3)  =  add_3_out_gga1(x3)
if_evaluate_2_in_5_ga5(x1, x2, x3, x4, x5)  =  if_evaluate_2_in_5_ga2(x4, x5)
if_evaluate_2_in_6_ga6(x1, x2, x3, x4, x5, x6)  =  if_evaluate_2_in_6_ga1(x6)
sub_3_in_gga3(x1, x2, x3)  =  sub_3_in_gga2(x1, x2)
if_sub_3_in_1_gga4(x1, x2, x3, x4)  =  if_sub_3_in_1_gga1(x4)
sub_3_out_gga3(x1, x2, x3)  =  sub_3_out_gga1(x3)
if_evaluate_2_in_2_ga5(x1, x2, x3, x4, x5)  =  if_evaluate_2_in_2_ga2(x4, x5)
if_evaluate_2_in_3_ga6(x1, x2, x3, x4, x5, x6)  =  if_evaluate_2_in_3_ga1(x6)
myis_2_out_ag2(x1, x2)  =  myis_2_out_ag1(x1)
SUB_3_IN_GGA3(x1, x2, x3)  =  SUB_3_IN_GGA2(x1, x2)

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

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

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

SUB_3_IN_GGA3(s_11(X), s_11(Y), Z) -> SUB_3_IN_GGA3(X, Y, Z)

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

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

↳ PROLOG
  ↳ UnrequestedClauseRemoverProof
    ↳ PROLOG
      ↳ PrologToPiTRSProof
        ↳ PiTRS
          ↳ DependencyPairsProof
            ↳ PiDP
              ↳ DependencyGraphProof
                ↳ AND
                  ↳ PiDP
                    ↳ UsableRulesProof
                      ↳ PiDP
                        ↳ PiDPToQDPProof
                          ↳ QDP
                            ↳ QDPSizeChangeProof
                  ↳ PiDP
                  ↳ PiDP
                  ↳ PiDP
                  ↳ PiDP

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

SUB_3_IN_GGA2(s_11(X), s_11(Y)) -> SUB_3_IN_GGA2(X, Y)

R is empty.
Q is empty.
We have to consider all (P,Q,R)-chains.
The head symbols of this DP problem are {SUB_3_IN_GGA2}.
By using the subterm criterion together with the size-change analysis we have proven that there are no infinite chains for this DP problem.

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



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

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

ADD_3_IN_GGA3(s_11(X), Y, s_11(Z)) -> ADD_3_IN_GGA3(X, Y, Z)

The TRS R consists of the following rules:

myis_2_in_ag2(Z, X) -> if_myis_2_in_1_ag3(Z, X, evaluate_2_in_ga2(X, Z))
evaluate_2_in_ga2(+2(X, Y), Z) -> if_evaluate_2_in_1_ga4(X, Y, Z, evaluate_2_in_ga2(X, X1))
evaluate_2_in_ga2(-2(X, Y), Z) -> if_evaluate_2_in_4_ga4(X, Y, Z, evaluate_2_in_ga2(X, X1))
evaluate_2_in_ga2(*2(X, Y), Z) -> if_evaluate_2_in_7_ga4(X, Y, Z, evaluate_2_in_ga2(X, X1))
evaluate_2_in_ga2(X, X) -> if_evaluate_2_in_10_ga2(X, integer_1_in_g1(X))
integer_1_in_g1(s_11(X)) -> if_integer_1_in_1_g2(X, integer_1_in_g1(X))
integer_1_in_g1(0_0) -> integer_1_out_g1(0_0)
if_integer_1_in_1_g2(X, integer_1_out_g1(X)) -> integer_1_out_g1(s_11(X))
if_evaluate_2_in_10_ga2(X, integer_1_out_g1(X)) -> evaluate_2_out_ga2(X, X)
if_evaluate_2_in_7_ga4(X, Y, Z, evaluate_2_out_ga2(X, X1)) -> if_evaluate_2_in_8_ga5(X, Y, Z, X1, evaluate_2_in_ga2(Y, Y1))
if_evaluate_2_in_8_ga5(X, Y, Z, X1, evaluate_2_out_ga2(Y, Y1)) -> if_evaluate_2_in_9_ga6(X, Y, Z, X1, Y1, mult_3_in_gga3(X1, Y1, Z))
mult_3_in_gga3(s_11(X), Y, R) -> if_mult_3_in_1_gga4(X, Y, R, mult_3_in_gga3(X, Y, Z))
mult_3_in_gga3(0_0, Y, 0_0) -> mult_3_out_gga3(0_0, Y, 0_0)
if_mult_3_in_1_gga4(X, Y, R, mult_3_out_gga3(X, Y, Z)) -> if_mult_3_in_2_gga5(X, Y, R, Z, add_3_in_gga3(Y, Z, R))
add_3_in_gga3(s_11(X), Y, s_11(Z)) -> if_add_3_in_1_gga4(X, Y, Z, add_3_in_gga3(X, Y, Z))
add_3_in_gga3(0_0, X, X) -> add_3_out_gga3(0_0, X, X)
if_add_3_in_1_gga4(X, Y, Z, add_3_out_gga3(X, Y, Z)) -> add_3_out_gga3(s_11(X), Y, s_11(Z))
if_mult_3_in_2_gga5(X, Y, R, Z, add_3_out_gga3(Y, Z, R)) -> mult_3_out_gga3(s_11(X), Y, R)
if_evaluate_2_in_9_ga6(X, Y, Z, X1, Y1, mult_3_out_gga3(X1, Y1, Z)) -> evaluate_2_out_ga2(*2(X, Y), Z)
if_evaluate_2_in_4_ga4(X, Y, Z, evaluate_2_out_ga2(X, X1)) -> if_evaluate_2_in_5_ga5(X, Y, Z, X1, evaluate_2_in_ga2(Y, Y1))
if_evaluate_2_in_5_ga5(X, Y, Z, X1, evaluate_2_out_ga2(Y, Y1)) -> if_evaluate_2_in_6_ga6(X, Y, Z, X1, Y1, sub_3_in_gga3(X1, Y1, Z))
sub_3_in_gga3(s_11(X), s_11(Y), Z) -> if_sub_3_in_1_gga4(X, Y, Z, sub_3_in_gga3(X, Y, Z))
sub_3_in_gga3(X, 0_0, X) -> sub_3_out_gga3(X, 0_0, X)
if_sub_3_in_1_gga4(X, Y, Z, sub_3_out_gga3(X, Y, Z)) -> sub_3_out_gga3(s_11(X), s_11(Y), Z)
if_evaluate_2_in_6_ga6(X, Y, Z, X1, Y1, sub_3_out_gga3(X1, Y1, Z)) -> evaluate_2_out_ga2(-2(X, Y), Z)
if_evaluate_2_in_1_ga4(X, Y, Z, evaluate_2_out_ga2(X, X1)) -> if_evaluate_2_in_2_ga5(X, Y, Z, X1, evaluate_2_in_ga2(Y, Y1))
if_evaluate_2_in_2_ga5(X, Y, Z, X1, evaluate_2_out_ga2(Y, Y1)) -> if_evaluate_2_in_3_ga6(X, Y, Z, X1, Y1, add_3_in_gga3(X1, Y1, Z))
if_evaluate_2_in_3_ga6(X, Y, Z, X1, Y1, add_3_out_gga3(X1, Y1, Z)) -> evaluate_2_out_ga2(+2(X, Y), Z)
if_myis_2_in_1_ag3(Z, X, evaluate_2_out_ga2(X, Z)) -> myis_2_out_ag2(Z, X)

The argument filtering Pi contains the following mapping:
myis_2_in_ag2(x1, x2)  =  myis_2_in_ag1(x2)
+2(x1, x2)  =  +2(x1, x2)
-2(x1, x2)  =  -2(x1, x2)
*2(x1, x2)  =  *2(x1, x2)
s_11(x1)  =  s_11(x1)
0_0  =  0_0
if_myis_2_in_1_ag3(x1, x2, x3)  =  if_myis_2_in_1_ag1(x3)
evaluate_2_in_ga2(x1, x2)  =  evaluate_2_in_ga1(x1)
if_evaluate_2_in_1_ga4(x1, x2, x3, x4)  =  if_evaluate_2_in_1_ga2(x2, x4)
if_evaluate_2_in_4_ga4(x1, x2, x3, x4)  =  if_evaluate_2_in_4_ga2(x2, x4)
if_evaluate_2_in_7_ga4(x1, x2, x3, x4)  =  if_evaluate_2_in_7_ga2(x2, x4)
if_evaluate_2_in_10_ga2(x1, x2)  =  if_evaluate_2_in_10_ga2(x1, x2)
integer_1_in_g1(x1)  =  integer_1_in_g1(x1)
if_integer_1_in_1_g2(x1, x2)  =  if_integer_1_in_1_g1(x2)
integer_1_out_g1(x1)  =  integer_1_out_g
evaluate_2_out_ga2(x1, x2)  =  evaluate_2_out_ga1(x2)
if_evaluate_2_in_8_ga5(x1, x2, x3, x4, x5)  =  if_evaluate_2_in_8_ga2(x4, x5)
if_evaluate_2_in_9_ga6(x1, x2, x3, x4, x5, x6)  =  if_evaluate_2_in_9_ga1(x6)
mult_3_in_gga3(x1, x2, x3)  =  mult_3_in_gga2(x1, x2)
if_mult_3_in_1_gga4(x1, x2, x3, x4)  =  if_mult_3_in_1_gga2(x2, x4)
mult_3_out_gga3(x1, x2, x3)  =  mult_3_out_gga1(x3)
if_mult_3_in_2_gga5(x1, x2, x3, x4, x5)  =  if_mult_3_in_2_gga1(x5)
add_3_in_gga3(x1, x2, x3)  =  add_3_in_gga2(x1, x2)
if_add_3_in_1_gga4(x1, x2, x3, x4)  =  if_add_3_in_1_gga1(x4)
add_3_out_gga3(x1, x2, x3)  =  add_3_out_gga1(x3)
if_evaluate_2_in_5_ga5(x1, x2, x3, x4, x5)  =  if_evaluate_2_in_5_ga2(x4, x5)
if_evaluate_2_in_6_ga6(x1, x2, x3, x4, x5, x6)  =  if_evaluate_2_in_6_ga1(x6)
sub_3_in_gga3(x1, x2, x3)  =  sub_3_in_gga2(x1, x2)
if_sub_3_in_1_gga4(x1, x2, x3, x4)  =  if_sub_3_in_1_gga1(x4)
sub_3_out_gga3(x1, x2, x3)  =  sub_3_out_gga1(x3)
if_evaluate_2_in_2_ga5(x1, x2, x3, x4, x5)  =  if_evaluate_2_in_2_ga2(x4, x5)
if_evaluate_2_in_3_ga6(x1, x2, x3, x4, x5, x6)  =  if_evaluate_2_in_3_ga1(x6)
myis_2_out_ag2(x1, x2)  =  myis_2_out_ag1(x1)
ADD_3_IN_GGA3(x1, x2, x3)  =  ADD_3_IN_GGA2(x1, x2)

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

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

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

ADD_3_IN_GGA3(s_11(X), Y, s_11(Z)) -> ADD_3_IN_GGA3(X, Y, Z)

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

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

↳ PROLOG
  ↳ UnrequestedClauseRemoverProof
    ↳ PROLOG
      ↳ PrologToPiTRSProof
        ↳ PiTRS
          ↳ DependencyPairsProof
            ↳ PiDP
              ↳ DependencyGraphProof
                ↳ AND
                  ↳ PiDP
                  ↳ PiDP
                    ↳ UsableRulesProof
                      ↳ PiDP
                        ↳ PiDPToQDPProof
                          ↳ QDP
                            ↳ QDPSizeChangeProof
                  ↳ PiDP
                  ↳ PiDP
                  ↳ PiDP

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

ADD_3_IN_GGA2(s_11(X), Y) -> ADD_3_IN_GGA2(X, Y)

R is empty.
Q is empty.
We have to consider all (P,Q,R)-chains.
The head symbols of this DP problem are {ADD_3_IN_GGA2}.
By using the subterm criterion together with the size-change analysis we have proven that there are no infinite chains for this DP problem.

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



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

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

MULT_3_IN_GGA3(s_11(X), Y, R) -> MULT_3_IN_GGA3(X, Y, Z)

The TRS R consists of the following rules:

myis_2_in_ag2(Z, X) -> if_myis_2_in_1_ag3(Z, X, evaluate_2_in_ga2(X, Z))
evaluate_2_in_ga2(+2(X, Y), Z) -> if_evaluate_2_in_1_ga4(X, Y, Z, evaluate_2_in_ga2(X, X1))
evaluate_2_in_ga2(-2(X, Y), Z) -> if_evaluate_2_in_4_ga4(X, Y, Z, evaluate_2_in_ga2(X, X1))
evaluate_2_in_ga2(*2(X, Y), Z) -> if_evaluate_2_in_7_ga4(X, Y, Z, evaluate_2_in_ga2(X, X1))
evaluate_2_in_ga2(X, X) -> if_evaluate_2_in_10_ga2(X, integer_1_in_g1(X))
integer_1_in_g1(s_11(X)) -> if_integer_1_in_1_g2(X, integer_1_in_g1(X))
integer_1_in_g1(0_0) -> integer_1_out_g1(0_0)
if_integer_1_in_1_g2(X, integer_1_out_g1(X)) -> integer_1_out_g1(s_11(X))
if_evaluate_2_in_10_ga2(X, integer_1_out_g1(X)) -> evaluate_2_out_ga2(X, X)
if_evaluate_2_in_7_ga4(X, Y, Z, evaluate_2_out_ga2(X, X1)) -> if_evaluate_2_in_8_ga5(X, Y, Z, X1, evaluate_2_in_ga2(Y, Y1))
if_evaluate_2_in_8_ga5(X, Y, Z, X1, evaluate_2_out_ga2(Y, Y1)) -> if_evaluate_2_in_9_ga6(X, Y, Z, X1, Y1, mult_3_in_gga3(X1, Y1, Z))
mult_3_in_gga3(s_11(X), Y, R) -> if_mult_3_in_1_gga4(X, Y, R, mult_3_in_gga3(X, Y, Z))
mult_3_in_gga3(0_0, Y, 0_0) -> mult_3_out_gga3(0_0, Y, 0_0)
if_mult_3_in_1_gga4(X, Y, R, mult_3_out_gga3(X, Y, Z)) -> if_mult_3_in_2_gga5(X, Y, R, Z, add_3_in_gga3(Y, Z, R))
add_3_in_gga3(s_11(X), Y, s_11(Z)) -> if_add_3_in_1_gga4(X, Y, Z, add_3_in_gga3(X, Y, Z))
add_3_in_gga3(0_0, X, X) -> add_3_out_gga3(0_0, X, X)
if_add_3_in_1_gga4(X, Y, Z, add_3_out_gga3(X, Y, Z)) -> add_3_out_gga3(s_11(X), Y, s_11(Z))
if_mult_3_in_2_gga5(X, Y, R, Z, add_3_out_gga3(Y, Z, R)) -> mult_3_out_gga3(s_11(X), Y, R)
if_evaluate_2_in_9_ga6(X, Y, Z, X1, Y1, mult_3_out_gga3(X1, Y1, Z)) -> evaluate_2_out_ga2(*2(X, Y), Z)
if_evaluate_2_in_4_ga4(X, Y, Z, evaluate_2_out_ga2(X, X1)) -> if_evaluate_2_in_5_ga5(X, Y, Z, X1, evaluate_2_in_ga2(Y, Y1))
if_evaluate_2_in_5_ga5(X, Y, Z, X1, evaluate_2_out_ga2(Y, Y1)) -> if_evaluate_2_in_6_ga6(X, Y, Z, X1, Y1, sub_3_in_gga3(X1, Y1, Z))
sub_3_in_gga3(s_11(X), s_11(Y), Z) -> if_sub_3_in_1_gga4(X, Y, Z, sub_3_in_gga3(X, Y, Z))
sub_3_in_gga3(X, 0_0, X) -> sub_3_out_gga3(X, 0_0, X)
if_sub_3_in_1_gga4(X, Y, Z, sub_3_out_gga3(X, Y, Z)) -> sub_3_out_gga3(s_11(X), s_11(Y), Z)
if_evaluate_2_in_6_ga6(X, Y, Z, X1, Y1, sub_3_out_gga3(X1, Y1, Z)) -> evaluate_2_out_ga2(-2(X, Y), Z)
if_evaluate_2_in_1_ga4(X, Y, Z, evaluate_2_out_ga2(X, X1)) -> if_evaluate_2_in_2_ga5(X, Y, Z, X1, evaluate_2_in_ga2(Y, Y1))
if_evaluate_2_in_2_ga5(X, Y, Z, X1, evaluate_2_out_ga2(Y, Y1)) -> if_evaluate_2_in_3_ga6(X, Y, Z, X1, Y1, add_3_in_gga3(X1, Y1, Z))
if_evaluate_2_in_3_ga6(X, Y, Z, X1, Y1, add_3_out_gga3(X1, Y1, Z)) -> evaluate_2_out_ga2(+2(X, Y), Z)
if_myis_2_in_1_ag3(Z, X, evaluate_2_out_ga2(X, Z)) -> myis_2_out_ag2(Z, X)

The argument filtering Pi contains the following mapping:
myis_2_in_ag2(x1, x2)  =  myis_2_in_ag1(x2)
+2(x1, x2)  =  +2(x1, x2)
-2(x1, x2)  =  -2(x1, x2)
*2(x1, x2)  =  *2(x1, x2)
s_11(x1)  =  s_11(x1)
0_0  =  0_0
if_myis_2_in_1_ag3(x1, x2, x3)  =  if_myis_2_in_1_ag1(x3)
evaluate_2_in_ga2(x1, x2)  =  evaluate_2_in_ga1(x1)
if_evaluate_2_in_1_ga4(x1, x2, x3, x4)  =  if_evaluate_2_in_1_ga2(x2, x4)
if_evaluate_2_in_4_ga4(x1, x2, x3, x4)  =  if_evaluate_2_in_4_ga2(x2, x4)
if_evaluate_2_in_7_ga4(x1, x2, x3, x4)  =  if_evaluate_2_in_7_ga2(x2, x4)
if_evaluate_2_in_10_ga2(x1, x2)  =  if_evaluate_2_in_10_ga2(x1, x2)
integer_1_in_g1(x1)  =  integer_1_in_g1(x1)
if_integer_1_in_1_g2(x1, x2)  =  if_integer_1_in_1_g1(x2)
integer_1_out_g1(x1)  =  integer_1_out_g
evaluate_2_out_ga2(x1, x2)  =  evaluate_2_out_ga1(x2)
if_evaluate_2_in_8_ga5(x1, x2, x3, x4, x5)  =  if_evaluate_2_in_8_ga2(x4, x5)
if_evaluate_2_in_9_ga6(x1, x2, x3, x4, x5, x6)  =  if_evaluate_2_in_9_ga1(x6)
mult_3_in_gga3(x1, x2, x3)  =  mult_3_in_gga2(x1, x2)
if_mult_3_in_1_gga4(x1, x2, x3, x4)  =  if_mult_3_in_1_gga2(x2, x4)
mult_3_out_gga3(x1, x2, x3)  =  mult_3_out_gga1(x3)
if_mult_3_in_2_gga5(x1, x2, x3, x4, x5)  =  if_mult_3_in_2_gga1(x5)
add_3_in_gga3(x1, x2, x3)  =  add_3_in_gga2(x1, x2)
if_add_3_in_1_gga4(x1, x2, x3, x4)  =  if_add_3_in_1_gga1(x4)
add_3_out_gga3(x1, x2, x3)  =  add_3_out_gga1(x3)
if_evaluate_2_in_5_ga5(x1, x2, x3, x4, x5)  =  if_evaluate_2_in_5_ga2(x4, x5)
if_evaluate_2_in_6_ga6(x1, x2, x3, x4, x5, x6)  =  if_evaluate_2_in_6_ga1(x6)
sub_3_in_gga3(x1, x2, x3)  =  sub_3_in_gga2(x1, x2)
if_sub_3_in_1_gga4(x1, x2, x3, x4)  =  if_sub_3_in_1_gga1(x4)
sub_3_out_gga3(x1, x2, x3)  =  sub_3_out_gga1(x3)
if_evaluate_2_in_2_ga5(x1, x2, x3, x4, x5)  =  if_evaluate_2_in_2_ga2(x4, x5)
if_evaluate_2_in_3_ga6(x1, x2, x3, x4, x5, x6)  =  if_evaluate_2_in_3_ga1(x6)
myis_2_out_ag2(x1, x2)  =  myis_2_out_ag1(x1)
MULT_3_IN_GGA3(x1, x2, x3)  =  MULT_3_IN_GGA2(x1, x2)

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

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

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

MULT_3_IN_GGA3(s_11(X), Y, R) -> MULT_3_IN_GGA3(X, Y, Z)

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

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

↳ PROLOG
  ↳ UnrequestedClauseRemoverProof
    ↳ PROLOG
      ↳ PrologToPiTRSProof
        ↳ PiTRS
          ↳ DependencyPairsProof
            ↳ PiDP
              ↳ DependencyGraphProof
                ↳ AND
                  ↳ PiDP
                  ↳ PiDP
                  ↳ PiDP
                    ↳ UsableRulesProof
                      ↳ PiDP
                        ↳ PiDPToQDPProof
                          ↳ QDP
                            ↳ QDPSizeChangeProof
                  ↳ PiDP
                  ↳ PiDP

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

MULT_3_IN_GGA2(s_11(X), Y) -> MULT_3_IN_GGA2(X, Y)

R is empty.
Q is empty.
We have to consider all (P,Q,R)-chains.
The head symbols of this DP problem are {MULT_3_IN_GGA2}.
By using the subterm criterion together with the size-change analysis we have proven that there are no infinite chains for this DP problem.

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



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

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

INTEGER_1_IN_G1(s_11(X)) -> INTEGER_1_IN_G1(X)

The TRS R consists of the following rules:

myis_2_in_ag2(Z, X) -> if_myis_2_in_1_ag3(Z, X, evaluate_2_in_ga2(X, Z))
evaluate_2_in_ga2(+2(X, Y), Z) -> if_evaluate_2_in_1_ga4(X, Y, Z, evaluate_2_in_ga2(X, X1))
evaluate_2_in_ga2(-2(X, Y), Z) -> if_evaluate_2_in_4_ga4(X, Y, Z, evaluate_2_in_ga2(X, X1))
evaluate_2_in_ga2(*2(X, Y), Z) -> if_evaluate_2_in_7_ga4(X, Y, Z, evaluate_2_in_ga2(X, X1))
evaluate_2_in_ga2(X, X) -> if_evaluate_2_in_10_ga2(X, integer_1_in_g1(X))
integer_1_in_g1(s_11(X)) -> if_integer_1_in_1_g2(X, integer_1_in_g1(X))
integer_1_in_g1(0_0) -> integer_1_out_g1(0_0)
if_integer_1_in_1_g2(X, integer_1_out_g1(X)) -> integer_1_out_g1(s_11(X))
if_evaluate_2_in_10_ga2(X, integer_1_out_g1(X)) -> evaluate_2_out_ga2(X, X)
if_evaluate_2_in_7_ga4(X, Y, Z, evaluate_2_out_ga2(X, X1)) -> if_evaluate_2_in_8_ga5(X, Y, Z, X1, evaluate_2_in_ga2(Y, Y1))
if_evaluate_2_in_8_ga5(X, Y, Z, X1, evaluate_2_out_ga2(Y, Y1)) -> if_evaluate_2_in_9_ga6(X, Y, Z, X1, Y1, mult_3_in_gga3(X1, Y1, Z))
mult_3_in_gga3(s_11(X), Y, R) -> if_mult_3_in_1_gga4(X, Y, R, mult_3_in_gga3(X, Y, Z))
mult_3_in_gga3(0_0, Y, 0_0) -> mult_3_out_gga3(0_0, Y, 0_0)
if_mult_3_in_1_gga4(X, Y, R, mult_3_out_gga3(X, Y, Z)) -> if_mult_3_in_2_gga5(X, Y, R, Z, add_3_in_gga3(Y, Z, R))
add_3_in_gga3(s_11(X), Y, s_11(Z)) -> if_add_3_in_1_gga4(X, Y, Z, add_3_in_gga3(X, Y, Z))
add_3_in_gga3(0_0, X, X) -> add_3_out_gga3(0_0, X, X)
if_add_3_in_1_gga4(X, Y, Z, add_3_out_gga3(X, Y, Z)) -> add_3_out_gga3(s_11(X), Y, s_11(Z))
if_mult_3_in_2_gga5(X, Y, R, Z, add_3_out_gga3(Y, Z, R)) -> mult_3_out_gga3(s_11(X), Y, R)
if_evaluate_2_in_9_ga6(X, Y, Z, X1, Y1, mult_3_out_gga3(X1, Y1, Z)) -> evaluate_2_out_ga2(*2(X, Y), Z)
if_evaluate_2_in_4_ga4(X, Y, Z, evaluate_2_out_ga2(X, X1)) -> if_evaluate_2_in_5_ga5(X, Y, Z, X1, evaluate_2_in_ga2(Y, Y1))
if_evaluate_2_in_5_ga5(X, Y, Z, X1, evaluate_2_out_ga2(Y, Y1)) -> if_evaluate_2_in_6_ga6(X, Y, Z, X1, Y1, sub_3_in_gga3(X1, Y1, Z))
sub_3_in_gga3(s_11(X), s_11(Y), Z) -> if_sub_3_in_1_gga4(X, Y, Z, sub_3_in_gga3(X, Y, Z))
sub_3_in_gga3(X, 0_0, X) -> sub_3_out_gga3(X, 0_0, X)
if_sub_3_in_1_gga4(X, Y, Z, sub_3_out_gga3(X, Y, Z)) -> sub_3_out_gga3(s_11(X), s_11(Y), Z)
if_evaluate_2_in_6_ga6(X, Y, Z, X1, Y1, sub_3_out_gga3(X1, Y1, Z)) -> evaluate_2_out_ga2(-2(X, Y), Z)
if_evaluate_2_in_1_ga4(X, Y, Z, evaluate_2_out_ga2(X, X1)) -> if_evaluate_2_in_2_ga5(X, Y, Z, X1, evaluate_2_in_ga2(Y, Y1))
if_evaluate_2_in_2_ga5(X, Y, Z, X1, evaluate_2_out_ga2(Y, Y1)) -> if_evaluate_2_in_3_ga6(X, Y, Z, X1, Y1, add_3_in_gga3(X1, Y1, Z))
if_evaluate_2_in_3_ga6(X, Y, Z, X1, Y1, add_3_out_gga3(X1, Y1, Z)) -> evaluate_2_out_ga2(+2(X, Y), Z)
if_myis_2_in_1_ag3(Z, X, evaluate_2_out_ga2(X, Z)) -> myis_2_out_ag2(Z, X)

The argument filtering Pi contains the following mapping:
myis_2_in_ag2(x1, x2)  =  myis_2_in_ag1(x2)
+2(x1, x2)  =  +2(x1, x2)
-2(x1, x2)  =  -2(x1, x2)
*2(x1, x2)  =  *2(x1, x2)
s_11(x1)  =  s_11(x1)
0_0  =  0_0
if_myis_2_in_1_ag3(x1, x2, x3)  =  if_myis_2_in_1_ag1(x3)
evaluate_2_in_ga2(x1, x2)  =  evaluate_2_in_ga1(x1)
if_evaluate_2_in_1_ga4(x1, x2, x3, x4)  =  if_evaluate_2_in_1_ga2(x2, x4)
if_evaluate_2_in_4_ga4(x1, x2, x3, x4)  =  if_evaluate_2_in_4_ga2(x2, x4)
if_evaluate_2_in_7_ga4(x1, x2, x3, x4)  =  if_evaluate_2_in_7_ga2(x2, x4)
if_evaluate_2_in_10_ga2(x1, x2)  =  if_evaluate_2_in_10_ga2(x1, x2)
integer_1_in_g1(x1)  =  integer_1_in_g1(x1)
if_integer_1_in_1_g2(x1, x2)  =  if_integer_1_in_1_g1(x2)
integer_1_out_g1(x1)  =  integer_1_out_g
evaluate_2_out_ga2(x1, x2)  =  evaluate_2_out_ga1(x2)
if_evaluate_2_in_8_ga5(x1, x2, x3, x4, x5)  =  if_evaluate_2_in_8_ga2(x4, x5)
if_evaluate_2_in_9_ga6(x1, x2, x3, x4, x5, x6)  =  if_evaluate_2_in_9_ga1(x6)
mult_3_in_gga3(x1, x2, x3)  =  mult_3_in_gga2(x1, x2)
if_mult_3_in_1_gga4(x1, x2, x3, x4)  =  if_mult_3_in_1_gga2(x2, x4)
mult_3_out_gga3(x1, x2, x3)  =  mult_3_out_gga1(x3)
if_mult_3_in_2_gga5(x1, x2, x3, x4, x5)  =  if_mult_3_in_2_gga1(x5)
add_3_in_gga3(x1, x2, x3)  =  add_3_in_gga2(x1, x2)
if_add_3_in_1_gga4(x1, x2, x3, x4)  =  if_add_3_in_1_gga1(x4)
add_3_out_gga3(x1, x2, x3)  =  add_3_out_gga1(x3)
if_evaluate_2_in_5_ga5(x1, x2, x3, x4, x5)  =  if_evaluate_2_in_5_ga2(x4, x5)
if_evaluate_2_in_6_ga6(x1, x2, x3, x4, x5, x6)  =  if_evaluate_2_in_6_ga1(x6)
sub_3_in_gga3(x1, x2, x3)  =  sub_3_in_gga2(x1, x2)
if_sub_3_in_1_gga4(x1, x2, x3, x4)  =  if_sub_3_in_1_gga1(x4)
sub_3_out_gga3(x1, x2, x3)  =  sub_3_out_gga1(x3)
if_evaluate_2_in_2_ga5(x1, x2, x3, x4, x5)  =  if_evaluate_2_in_2_ga2(x4, x5)
if_evaluate_2_in_3_ga6(x1, x2, x3, x4, x5, x6)  =  if_evaluate_2_in_3_ga1(x6)
myis_2_out_ag2(x1, x2)  =  myis_2_out_ag1(x1)
INTEGER_1_IN_G1(x1)  =  INTEGER_1_IN_G1(x1)

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

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

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

INTEGER_1_IN_G1(s_11(X)) -> INTEGER_1_IN_G1(X)

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

↳ PROLOG
  ↳ UnrequestedClauseRemoverProof
    ↳ PROLOG
      ↳ PrologToPiTRSProof
        ↳ PiTRS
          ↳ DependencyPairsProof
            ↳ PiDP
              ↳ DependencyGraphProof
                ↳ AND
                  ↳ PiDP
                  ↳ PiDP
                  ↳ PiDP
                  ↳ PiDP
                    ↳ UsableRulesProof
                      ↳ PiDP
                        ↳ PiDPToQDPProof
                          ↳ QDP
                            ↳ QDPSizeChangeProof
                  ↳ PiDP

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

INTEGER_1_IN_G1(s_11(X)) -> INTEGER_1_IN_G1(X)

R is empty.
Q is empty.
We have to consider all (P,Q,R)-chains.
The head symbols of this DP problem are {INTEGER_1_IN_G1}.
By using the subterm criterion together with the size-change analysis we have proven that there are no infinite chains for this DP problem.

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



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

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

EVALUATE_2_IN_GA2(+2(X, Y), Z) -> EVALUATE_2_IN_GA2(X, X1)
IF_EVALUATE_2_IN_7_GA4(X, Y, Z, evaluate_2_out_ga2(X, X1)) -> EVALUATE_2_IN_GA2(Y, Y1)
IF_EVALUATE_2_IN_4_GA4(X, Y, Z, evaluate_2_out_ga2(X, X1)) -> EVALUATE_2_IN_GA2(Y, Y1)
EVALUATE_2_IN_GA2(*2(X, Y), Z) -> EVALUATE_2_IN_GA2(X, X1)
IF_EVALUATE_2_IN_1_GA4(X, Y, Z, evaluate_2_out_ga2(X, X1)) -> EVALUATE_2_IN_GA2(Y, Y1)
EVALUATE_2_IN_GA2(*2(X, Y), Z) -> IF_EVALUATE_2_IN_7_GA4(X, Y, Z, evaluate_2_in_ga2(X, X1))
EVALUATE_2_IN_GA2(+2(X, Y), Z) -> IF_EVALUATE_2_IN_1_GA4(X, Y, Z, evaluate_2_in_ga2(X, X1))
EVALUATE_2_IN_GA2(-2(X, Y), Z) -> EVALUATE_2_IN_GA2(X, X1)
EVALUATE_2_IN_GA2(-2(X, Y), Z) -> IF_EVALUATE_2_IN_4_GA4(X, Y, Z, evaluate_2_in_ga2(X, X1))

The TRS R consists of the following rules:

myis_2_in_ag2(Z, X) -> if_myis_2_in_1_ag3(Z, X, evaluate_2_in_ga2(X, Z))
evaluate_2_in_ga2(+2(X, Y), Z) -> if_evaluate_2_in_1_ga4(X, Y, Z, evaluate_2_in_ga2(X, X1))
evaluate_2_in_ga2(-2(X, Y), Z) -> if_evaluate_2_in_4_ga4(X, Y, Z, evaluate_2_in_ga2(X, X1))
evaluate_2_in_ga2(*2(X, Y), Z) -> if_evaluate_2_in_7_ga4(X, Y, Z, evaluate_2_in_ga2(X, X1))
evaluate_2_in_ga2(X, X) -> if_evaluate_2_in_10_ga2(X, integer_1_in_g1(X))
integer_1_in_g1(s_11(X)) -> if_integer_1_in_1_g2(X, integer_1_in_g1(X))
integer_1_in_g1(0_0) -> integer_1_out_g1(0_0)
if_integer_1_in_1_g2(X, integer_1_out_g1(X)) -> integer_1_out_g1(s_11(X))
if_evaluate_2_in_10_ga2(X, integer_1_out_g1(X)) -> evaluate_2_out_ga2(X, X)
if_evaluate_2_in_7_ga4(X, Y, Z, evaluate_2_out_ga2(X, X1)) -> if_evaluate_2_in_8_ga5(X, Y, Z, X1, evaluate_2_in_ga2(Y, Y1))
if_evaluate_2_in_8_ga5(X, Y, Z, X1, evaluate_2_out_ga2(Y, Y1)) -> if_evaluate_2_in_9_ga6(X, Y, Z, X1, Y1, mult_3_in_gga3(X1, Y1, Z))
mult_3_in_gga3(s_11(X), Y, R) -> if_mult_3_in_1_gga4(X, Y, R, mult_3_in_gga3(X, Y, Z))
mult_3_in_gga3(0_0, Y, 0_0) -> mult_3_out_gga3(0_0, Y, 0_0)
if_mult_3_in_1_gga4(X, Y, R, mult_3_out_gga3(X, Y, Z)) -> if_mult_3_in_2_gga5(X, Y, R, Z, add_3_in_gga3(Y, Z, R))
add_3_in_gga3(s_11(X), Y, s_11(Z)) -> if_add_3_in_1_gga4(X, Y, Z, add_3_in_gga3(X, Y, Z))
add_3_in_gga3(0_0, X, X) -> add_3_out_gga3(0_0, X, X)
if_add_3_in_1_gga4(X, Y, Z, add_3_out_gga3(X, Y, Z)) -> add_3_out_gga3(s_11(X), Y, s_11(Z))
if_mult_3_in_2_gga5(X, Y, R, Z, add_3_out_gga3(Y, Z, R)) -> mult_3_out_gga3(s_11(X), Y, R)
if_evaluate_2_in_9_ga6(X, Y, Z, X1, Y1, mult_3_out_gga3(X1, Y1, Z)) -> evaluate_2_out_ga2(*2(X, Y), Z)
if_evaluate_2_in_4_ga4(X, Y, Z, evaluate_2_out_ga2(X, X1)) -> if_evaluate_2_in_5_ga5(X, Y, Z, X1, evaluate_2_in_ga2(Y, Y1))
if_evaluate_2_in_5_ga5(X, Y, Z, X1, evaluate_2_out_ga2(Y, Y1)) -> if_evaluate_2_in_6_ga6(X, Y, Z, X1, Y1, sub_3_in_gga3(X1, Y1, Z))
sub_3_in_gga3(s_11(X), s_11(Y), Z) -> if_sub_3_in_1_gga4(X, Y, Z, sub_3_in_gga3(X, Y, Z))
sub_3_in_gga3(X, 0_0, X) -> sub_3_out_gga3(X, 0_0, X)
if_sub_3_in_1_gga4(X, Y, Z, sub_3_out_gga3(X, Y, Z)) -> sub_3_out_gga3(s_11(X), s_11(Y), Z)
if_evaluate_2_in_6_ga6(X, Y, Z, X1, Y1, sub_3_out_gga3(X1, Y1, Z)) -> evaluate_2_out_ga2(-2(X, Y), Z)
if_evaluate_2_in_1_ga4(X, Y, Z, evaluate_2_out_ga2(X, X1)) -> if_evaluate_2_in_2_ga5(X, Y, Z, X1, evaluate_2_in_ga2(Y, Y1))
if_evaluate_2_in_2_ga5(X, Y, Z, X1, evaluate_2_out_ga2(Y, Y1)) -> if_evaluate_2_in_3_ga6(X, Y, Z, X1, Y1, add_3_in_gga3(X1, Y1, Z))
if_evaluate_2_in_3_ga6(X, Y, Z, X1, Y1, add_3_out_gga3(X1, Y1, Z)) -> evaluate_2_out_ga2(+2(X, Y), Z)
if_myis_2_in_1_ag3(Z, X, evaluate_2_out_ga2(X, Z)) -> myis_2_out_ag2(Z, X)

The argument filtering Pi contains the following mapping:
myis_2_in_ag2(x1, x2)  =  myis_2_in_ag1(x2)
+2(x1, x2)  =  +2(x1, x2)
-2(x1, x2)  =  -2(x1, x2)
*2(x1, x2)  =  *2(x1, x2)
s_11(x1)  =  s_11(x1)
0_0  =  0_0
if_myis_2_in_1_ag3(x1, x2, x3)  =  if_myis_2_in_1_ag1(x3)
evaluate_2_in_ga2(x1, x2)  =  evaluate_2_in_ga1(x1)
if_evaluate_2_in_1_ga4(x1, x2, x3, x4)  =  if_evaluate_2_in_1_ga2(x2, x4)
if_evaluate_2_in_4_ga4(x1, x2, x3, x4)  =  if_evaluate_2_in_4_ga2(x2, x4)
if_evaluate_2_in_7_ga4(x1, x2, x3, x4)  =  if_evaluate_2_in_7_ga2(x2, x4)
if_evaluate_2_in_10_ga2(x1, x2)  =  if_evaluate_2_in_10_ga2(x1, x2)
integer_1_in_g1(x1)  =  integer_1_in_g1(x1)
if_integer_1_in_1_g2(x1, x2)  =  if_integer_1_in_1_g1(x2)
integer_1_out_g1(x1)  =  integer_1_out_g
evaluate_2_out_ga2(x1, x2)  =  evaluate_2_out_ga1(x2)
if_evaluate_2_in_8_ga5(x1, x2, x3, x4, x5)  =  if_evaluate_2_in_8_ga2(x4, x5)
if_evaluate_2_in_9_ga6(x1, x2, x3, x4, x5, x6)  =  if_evaluate_2_in_9_ga1(x6)
mult_3_in_gga3(x1, x2, x3)  =  mult_3_in_gga2(x1, x2)
if_mult_3_in_1_gga4(x1, x2, x3, x4)  =  if_mult_3_in_1_gga2(x2, x4)
mult_3_out_gga3(x1, x2, x3)  =  mult_3_out_gga1(x3)
if_mult_3_in_2_gga5(x1, x2, x3, x4, x5)  =  if_mult_3_in_2_gga1(x5)
add_3_in_gga3(x1, x2, x3)  =  add_3_in_gga2(x1, x2)
if_add_3_in_1_gga4(x1, x2, x3, x4)  =  if_add_3_in_1_gga1(x4)
add_3_out_gga3(x1, x2, x3)  =  add_3_out_gga1(x3)
if_evaluate_2_in_5_ga5(x1, x2, x3, x4, x5)  =  if_evaluate_2_in_5_ga2(x4, x5)
if_evaluate_2_in_6_ga6(x1, x2, x3, x4, x5, x6)  =  if_evaluate_2_in_6_ga1(x6)
sub_3_in_gga3(x1, x2, x3)  =  sub_3_in_gga2(x1, x2)
if_sub_3_in_1_gga4(x1, x2, x3, x4)  =  if_sub_3_in_1_gga1(x4)
sub_3_out_gga3(x1, x2, x3)  =  sub_3_out_gga1(x3)
if_evaluate_2_in_2_ga5(x1, x2, x3, x4, x5)  =  if_evaluate_2_in_2_ga2(x4, x5)
if_evaluate_2_in_3_ga6(x1, x2, x3, x4, x5, x6)  =  if_evaluate_2_in_3_ga1(x6)
myis_2_out_ag2(x1, x2)  =  myis_2_out_ag1(x1)
EVALUATE_2_IN_GA2(x1, x2)  =  EVALUATE_2_IN_GA1(x1)
IF_EVALUATE_2_IN_4_GA4(x1, x2, x3, x4)  =  IF_EVALUATE_2_IN_4_GA2(x2, x4)
IF_EVALUATE_2_IN_7_GA4(x1, x2, x3, x4)  =  IF_EVALUATE_2_IN_7_GA2(x2, x4)
IF_EVALUATE_2_IN_1_GA4(x1, x2, x3, x4)  =  IF_EVALUATE_2_IN_1_GA2(x2, x4)

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

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

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

EVALUATE_2_IN_GA2(+2(X, Y), Z) -> EVALUATE_2_IN_GA2(X, X1)
IF_EVALUATE_2_IN_7_GA4(X, Y, Z, evaluate_2_out_ga2(X, X1)) -> EVALUATE_2_IN_GA2(Y, Y1)
IF_EVALUATE_2_IN_4_GA4(X, Y, Z, evaluate_2_out_ga2(X, X1)) -> EVALUATE_2_IN_GA2(Y, Y1)
EVALUATE_2_IN_GA2(*2(X, Y), Z) -> EVALUATE_2_IN_GA2(X, X1)
IF_EVALUATE_2_IN_1_GA4(X, Y, Z, evaluate_2_out_ga2(X, X1)) -> EVALUATE_2_IN_GA2(Y, Y1)
EVALUATE_2_IN_GA2(*2(X, Y), Z) -> IF_EVALUATE_2_IN_7_GA4(X, Y, Z, evaluate_2_in_ga2(X, X1))
EVALUATE_2_IN_GA2(+2(X, Y), Z) -> IF_EVALUATE_2_IN_1_GA4(X, Y, Z, evaluate_2_in_ga2(X, X1))
EVALUATE_2_IN_GA2(-2(X, Y), Z) -> EVALUATE_2_IN_GA2(X, X1)
EVALUATE_2_IN_GA2(-2(X, Y), Z) -> IF_EVALUATE_2_IN_4_GA4(X, Y, Z, evaluate_2_in_ga2(X, X1))

The TRS R consists of the following rules:

evaluate_2_in_ga2(+2(X, Y), Z) -> if_evaluate_2_in_1_ga4(X, Y, Z, evaluate_2_in_ga2(X, X1))
evaluate_2_in_ga2(-2(X, Y), Z) -> if_evaluate_2_in_4_ga4(X, Y, Z, evaluate_2_in_ga2(X, X1))
evaluate_2_in_ga2(*2(X, Y), Z) -> if_evaluate_2_in_7_ga4(X, Y, Z, evaluate_2_in_ga2(X, X1))
evaluate_2_in_ga2(X, X) -> if_evaluate_2_in_10_ga2(X, integer_1_in_g1(X))
if_evaluate_2_in_1_ga4(X, Y, Z, evaluate_2_out_ga2(X, X1)) -> if_evaluate_2_in_2_ga5(X, Y, Z, X1, evaluate_2_in_ga2(Y, Y1))
if_evaluate_2_in_4_ga4(X, Y, Z, evaluate_2_out_ga2(X, X1)) -> if_evaluate_2_in_5_ga5(X, Y, Z, X1, evaluate_2_in_ga2(Y, Y1))
if_evaluate_2_in_7_ga4(X, Y, Z, evaluate_2_out_ga2(X, X1)) -> if_evaluate_2_in_8_ga5(X, Y, Z, X1, evaluate_2_in_ga2(Y, Y1))
if_evaluate_2_in_10_ga2(X, integer_1_out_g1(X)) -> evaluate_2_out_ga2(X, X)
if_evaluate_2_in_2_ga5(X, Y, Z, X1, evaluate_2_out_ga2(Y, Y1)) -> if_evaluate_2_in_3_ga6(X, Y, Z, X1, Y1, add_3_in_gga3(X1, Y1, Z))
if_evaluate_2_in_5_ga5(X, Y, Z, X1, evaluate_2_out_ga2(Y, Y1)) -> if_evaluate_2_in_6_ga6(X, Y, Z, X1, Y1, sub_3_in_gga3(X1, Y1, Z))
if_evaluate_2_in_8_ga5(X, Y, Z, X1, evaluate_2_out_ga2(Y, Y1)) -> if_evaluate_2_in_9_ga6(X, Y, Z, X1, Y1, mult_3_in_gga3(X1, Y1, Z))
integer_1_in_g1(s_11(X)) -> if_integer_1_in_1_g2(X, integer_1_in_g1(X))
integer_1_in_g1(0_0) -> integer_1_out_g1(0_0)
if_evaluate_2_in_3_ga6(X, Y, Z, X1, Y1, add_3_out_gga3(X1, Y1, Z)) -> evaluate_2_out_ga2(+2(X, Y), Z)
if_evaluate_2_in_6_ga6(X, Y, Z, X1, Y1, sub_3_out_gga3(X1, Y1, Z)) -> evaluate_2_out_ga2(-2(X, Y), Z)
if_evaluate_2_in_9_ga6(X, Y, Z, X1, Y1, mult_3_out_gga3(X1, Y1, Z)) -> evaluate_2_out_ga2(*2(X, Y), Z)
if_integer_1_in_1_g2(X, integer_1_out_g1(X)) -> integer_1_out_g1(s_11(X))
add_3_in_gga3(s_11(X), Y, s_11(Z)) -> if_add_3_in_1_gga4(X, Y, Z, add_3_in_gga3(X, Y, Z))
add_3_in_gga3(0_0, X, X) -> add_3_out_gga3(0_0, X, X)
sub_3_in_gga3(s_11(X), s_11(Y), Z) -> if_sub_3_in_1_gga4(X, Y, Z, sub_3_in_gga3(X, Y, Z))
sub_3_in_gga3(X, 0_0, X) -> sub_3_out_gga3(X, 0_0, X)
mult_3_in_gga3(s_11(X), Y, R) -> if_mult_3_in_1_gga4(X, Y, R, mult_3_in_gga3(X, Y, Z))
mult_3_in_gga3(0_0, Y, 0_0) -> mult_3_out_gga3(0_0, Y, 0_0)
if_add_3_in_1_gga4(X, Y, Z, add_3_out_gga3(X, Y, Z)) -> add_3_out_gga3(s_11(X), Y, s_11(Z))
if_sub_3_in_1_gga4(X, Y, Z, sub_3_out_gga3(X, Y, Z)) -> sub_3_out_gga3(s_11(X), s_11(Y), Z)
if_mult_3_in_1_gga4(X, Y, R, mult_3_out_gga3(X, Y, Z)) -> if_mult_3_in_2_gga5(X, Y, R, Z, add_3_in_gga3(Y, Z, R))
if_mult_3_in_2_gga5(X, Y, R, Z, add_3_out_gga3(Y, Z, R)) -> mult_3_out_gga3(s_11(X), Y, R)

The argument filtering Pi contains the following mapping:
+2(x1, x2)  =  +2(x1, x2)
-2(x1, x2)  =  -2(x1, x2)
*2(x1, x2)  =  *2(x1, x2)
s_11(x1)  =  s_11(x1)
0_0  =  0_0
evaluate_2_in_ga2(x1, x2)  =  evaluate_2_in_ga1(x1)
if_evaluate_2_in_1_ga4(x1, x2, x3, x4)  =  if_evaluate_2_in_1_ga2(x2, x4)
if_evaluate_2_in_4_ga4(x1, x2, x3, x4)  =  if_evaluate_2_in_4_ga2(x2, x4)
if_evaluate_2_in_7_ga4(x1, x2, x3, x4)  =  if_evaluate_2_in_7_ga2(x2, x4)
if_evaluate_2_in_10_ga2(x1, x2)  =  if_evaluate_2_in_10_ga2(x1, x2)
integer_1_in_g1(x1)  =  integer_1_in_g1(x1)
if_integer_1_in_1_g2(x1, x2)  =  if_integer_1_in_1_g1(x2)
integer_1_out_g1(x1)  =  integer_1_out_g
evaluate_2_out_ga2(x1, x2)  =  evaluate_2_out_ga1(x2)
if_evaluate_2_in_8_ga5(x1, x2, x3, x4, x5)  =  if_evaluate_2_in_8_ga2(x4, x5)
if_evaluate_2_in_9_ga6(x1, x2, x3, x4, x5, x6)  =  if_evaluate_2_in_9_ga1(x6)
mult_3_in_gga3(x1, x2, x3)  =  mult_3_in_gga2(x1, x2)
if_mult_3_in_1_gga4(x1, x2, x3, x4)  =  if_mult_3_in_1_gga2(x2, x4)
mult_3_out_gga3(x1, x2, x3)  =  mult_3_out_gga1(x3)
if_mult_3_in_2_gga5(x1, x2, x3, x4, x5)  =  if_mult_3_in_2_gga1(x5)
add_3_in_gga3(x1, x2, x3)  =  add_3_in_gga2(x1, x2)
if_add_3_in_1_gga4(x1, x2, x3, x4)  =  if_add_3_in_1_gga1(x4)
add_3_out_gga3(x1, x2, x3)  =  add_3_out_gga1(x3)
if_evaluate_2_in_5_ga5(x1, x2, x3, x4, x5)  =  if_evaluate_2_in_5_ga2(x4, x5)
if_evaluate_2_in_6_ga6(x1, x2, x3, x4, x5, x6)  =  if_evaluate_2_in_6_ga1(x6)
sub_3_in_gga3(x1, x2, x3)  =  sub_3_in_gga2(x1, x2)
if_sub_3_in_1_gga4(x1, x2, x3, x4)  =  if_sub_3_in_1_gga1(x4)
sub_3_out_gga3(x1, x2, x3)  =  sub_3_out_gga1(x3)
if_evaluate_2_in_2_ga5(x1, x2, x3, x4, x5)  =  if_evaluate_2_in_2_ga2(x4, x5)
if_evaluate_2_in_3_ga6(x1, x2, x3, x4, x5, x6)  =  if_evaluate_2_in_3_ga1(x6)
EVALUATE_2_IN_GA2(x1, x2)  =  EVALUATE_2_IN_GA1(x1)
IF_EVALUATE_2_IN_4_GA4(x1, x2, x3, x4)  =  IF_EVALUATE_2_IN_4_GA2(x2, x4)
IF_EVALUATE_2_IN_7_GA4(x1, x2, x3, x4)  =  IF_EVALUATE_2_IN_7_GA2(x2, x4)
IF_EVALUATE_2_IN_1_GA4(x1, x2, x3, x4)  =  IF_EVALUATE_2_IN_1_GA2(x2, x4)

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

↳ PROLOG
  ↳ UnrequestedClauseRemoverProof
    ↳ PROLOG
      ↳ PrologToPiTRSProof
        ↳ PiTRS
          ↳ DependencyPairsProof
            ↳ PiDP
              ↳ DependencyGraphProof
                ↳ AND
                  ↳ PiDP
                  ↳ PiDP
                  ↳ PiDP
                  ↳ PiDP
                  ↳ PiDP
                    ↳ UsableRulesProof
                      ↳ PiDP
                        ↳ PiDPToQDPProof
                          ↳ QDP
                            ↳ QDPSizeChangeProof

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

EVALUATE_2_IN_GA1(+2(X, Y)) -> EVALUATE_2_IN_GA1(X)
IF_EVALUATE_2_IN_7_GA2(Y, evaluate_2_out_ga1(X1)) -> EVALUATE_2_IN_GA1(Y)
IF_EVALUATE_2_IN_4_GA2(Y, evaluate_2_out_ga1(X1)) -> EVALUATE_2_IN_GA1(Y)
EVALUATE_2_IN_GA1(*2(X, Y)) -> EVALUATE_2_IN_GA1(X)
IF_EVALUATE_2_IN_1_GA2(Y, evaluate_2_out_ga1(X1)) -> EVALUATE_2_IN_GA1(Y)
EVALUATE_2_IN_GA1(*2(X, Y)) -> IF_EVALUATE_2_IN_7_GA2(Y, evaluate_2_in_ga1(X))
EVALUATE_2_IN_GA1(+2(X, Y)) -> IF_EVALUATE_2_IN_1_GA2(Y, evaluate_2_in_ga1(X))
EVALUATE_2_IN_GA1(-2(X, Y)) -> EVALUATE_2_IN_GA1(X)
EVALUATE_2_IN_GA1(-2(X, Y)) -> IF_EVALUATE_2_IN_4_GA2(Y, evaluate_2_in_ga1(X))

The TRS R consists of the following rules:

evaluate_2_in_ga1(+2(X, Y)) -> if_evaluate_2_in_1_ga2(Y, evaluate_2_in_ga1(X))
evaluate_2_in_ga1(-2(X, Y)) -> if_evaluate_2_in_4_ga2(Y, evaluate_2_in_ga1(X))
evaluate_2_in_ga1(*2(X, Y)) -> if_evaluate_2_in_7_ga2(Y, evaluate_2_in_ga1(X))
evaluate_2_in_ga1(X) -> if_evaluate_2_in_10_ga2(X, integer_1_in_g1(X))
if_evaluate_2_in_1_ga2(Y, evaluate_2_out_ga1(X1)) -> if_evaluate_2_in_2_ga2(X1, evaluate_2_in_ga1(Y))
if_evaluate_2_in_4_ga2(Y, evaluate_2_out_ga1(X1)) -> if_evaluate_2_in_5_ga2(X1, evaluate_2_in_ga1(Y))
if_evaluate_2_in_7_ga2(Y, evaluate_2_out_ga1(X1)) -> if_evaluate_2_in_8_ga2(X1, evaluate_2_in_ga1(Y))
if_evaluate_2_in_10_ga2(X, integer_1_out_g) -> evaluate_2_out_ga1(X)
if_evaluate_2_in_2_ga2(X1, evaluate_2_out_ga1(Y1)) -> if_evaluate_2_in_3_ga1(add_3_in_gga2(X1, Y1))
if_evaluate_2_in_5_ga2(X1, evaluate_2_out_ga1(Y1)) -> if_evaluate_2_in_6_ga1(sub_3_in_gga2(X1, Y1))
if_evaluate_2_in_8_ga2(X1, evaluate_2_out_ga1(Y1)) -> if_evaluate_2_in_9_ga1(mult_3_in_gga2(X1, Y1))
integer_1_in_g1(s_11(X)) -> if_integer_1_in_1_g1(integer_1_in_g1(X))
integer_1_in_g1(0_0) -> integer_1_out_g
if_evaluate_2_in_3_ga1(add_3_out_gga1(Z)) -> evaluate_2_out_ga1(Z)
if_evaluate_2_in_6_ga1(sub_3_out_gga1(Z)) -> evaluate_2_out_ga1(Z)
if_evaluate_2_in_9_ga1(mult_3_out_gga1(Z)) -> evaluate_2_out_ga1(Z)
if_integer_1_in_1_g1(integer_1_out_g) -> integer_1_out_g
add_3_in_gga2(s_11(X), Y) -> if_add_3_in_1_gga1(add_3_in_gga2(X, Y))
add_3_in_gga2(0_0, X) -> add_3_out_gga1(X)
sub_3_in_gga2(s_11(X), s_11(Y)) -> if_sub_3_in_1_gga1(sub_3_in_gga2(X, Y))
sub_3_in_gga2(X, 0_0) -> sub_3_out_gga1(X)
mult_3_in_gga2(s_11(X), Y) -> if_mult_3_in_1_gga2(Y, mult_3_in_gga2(X, Y))
mult_3_in_gga2(0_0, Y) -> mult_3_out_gga1(0_0)
if_add_3_in_1_gga1(add_3_out_gga1(Z)) -> add_3_out_gga1(s_11(Z))
if_sub_3_in_1_gga1(sub_3_out_gga1(Z)) -> sub_3_out_gga1(Z)
if_mult_3_in_1_gga2(Y, mult_3_out_gga1(Z)) -> if_mult_3_in_2_gga1(add_3_in_gga2(Y, Z))
if_mult_3_in_2_gga1(add_3_out_gga1(R)) -> mult_3_out_gga1(R)

The set Q consists of the following terms:

evaluate_2_in_ga1(x0)
if_evaluate_2_in_1_ga2(x0, x1)
if_evaluate_2_in_4_ga2(x0, x1)
if_evaluate_2_in_7_ga2(x0, x1)
if_evaluate_2_in_10_ga2(x0, x1)
if_evaluate_2_in_2_ga2(x0, x1)
if_evaluate_2_in_5_ga2(x0, x1)
if_evaluate_2_in_8_ga2(x0, x1)
integer_1_in_g1(x0)
if_evaluate_2_in_3_ga1(x0)
if_evaluate_2_in_6_ga1(x0)
if_evaluate_2_in_9_ga1(x0)
if_integer_1_in_1_g1(x0)
add_3_in_gga2(x0, x1)
sub_3_in_gga2(x0, x1)
mult_3_in_gga2(x0, x1)
if_add_3_in_1_gga1(x0)
if_sub_3_in_1_gga1(x0)
if_mult_3_in_1_gga2(x0, x1)
if_mult_3_in_2_gga1(x0)

We have to consider all (P,Q,R)-chains.
The head symbols of this DP problem are {EVALUATE_2_IN_GA1, IF_EVALUATE_2_IN_7_GA2, IF_EVALUATE_2_IN_4_GA2, IF_EVALUATE_2_IN_1_GA2}.
By using the subterm criterion together with the size-change analysis we have proven that there are no infinite chains for this DP problem.

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