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



↳ PROLOG
  ↳ PrologToPiTRSProof

der2(d1(e1(t0)), const1(10)).
der2(d1(e1(const1(A))), const1(00)).
der2(d1(e1(X + Y)), DX + DY) :- der2(d1(e1(X)), DX), der2(d1(e1(Y)), DY).
der2(d1(e1(X * Y)), (X * DY) + (Y * DX)) :- der2(d1(e1(X)), DX), der2(d1(e1(Y)), DY).
der2(d12 (X), DDX) :- der2(d1(X), DX), der2(d1(e1(DX)), DDX).


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


der_2_in_ga2(d_11(e_11(t_0)), const_11(1_0)) -> der_2_out_ga2(d_11(e_11(t_0)), const_11(1_0))
der_2_in_ga2(d_11(e_11(const_11(A))), const_11(0_0)) -> der_2_out_ga2(d_11(e_11(const_11(A))), const_11(0_0))
der_2_in_ga2(d_11(e_11(+2(X, Y))), +2(DX, DY)) -> if_der_2_in_1_ga5(X, Y, DX, DY, der_2_in_ga2(d_11(e_11(X)), DX))
der_2_in_ga2(d_11(e_11(*2(X, Y))), +2(*2(X, DY), *2(Y, DX))) -> if_der_2_in_3_ga5(X, Y, DY, DX, der_2_in_ga2(d_11(e_11(X)), DX))
der_2_in_ga2(d_11(d_11(X)), DDX) -> if_der_2_in_5_ga3(X, DDX, der_2_in_ga2(d_11(X), DX))
if_der_2_in_5_ga3(X, DDX, der_2_out_ga2(d_11(X), DX)) -> if_der_2_in_6_ga4(X, DDX, DX, der_2_in_ga2(d_11(e_11(DX)), DDX))
if_der_2_in_6_ga4(X, DDX, DX, der_2_out_ga2(d_11(e_11(DX)), DDX)) -> der_2_out_ga2(d_11(d_11(X)), DDX)
if_der_2_in_3_ga5(X, Y, DY, DX, der_2_out_ga2(d_11(e_11(X)), DX)) -> if_der_2_in_4_ga5(X, Y, DY, DX, der_2_in_ga2(d_11(e_11(Y)), DY))
if_der_2_in_4_ga5(X, Y, DY, DX, der_2_out_ga2(d_11(e_11(Y)), DY)) -> der_2_out_ga2(d_11(e_11(*2(X, Y))), +2(*2(X, DY), *2(Y, DX)))
if_der_2_in_1_ga5(X, Y, DX, DY, der_2_out_ga2(d_11(e_11(X)), DX)) -> if_der_2_in_2_ga5(X, Y, DX, DY, der_2_in_ga2(d_11(e_11(Y)), DY))
if_der_2_in_2_ga5(X, Y, DX, DY, der_2_out_ga2(d_11(e_11(Y)), DY)) -> der_2_out_ga2(d_11(e_11(+2(X, Y))), +2(DX, DY))

The argument filtering Pi contains the following mapping:
der_2_in_ga2(x1, x2)  =  der_2_in_ga1(x1)
d_11(x1)  =  d_11(x1)
e_11(x1)  =  e_11(x1)
t_0  =  t_0
const_11(x1)  =  const_11(x1)
1_0  =  1_0
0_0  =  0_0
+2(x1, x2)  =  +2(x1, x2)
*2(x1, x2)  =  *2(x1, x2)
der_2_out_ga2(x1, x2)  =  der_2_out_ga1(x2)
if_der_2_in_1_ga5(x1, x2, x3, x4, x5)  =  if_der_2_in_1_ga2(x2, x5)
if_der_2_in_3_ga5(x1, x2, x3, x4, x5)  =  if_der_2_in_3_ga3(x1, x2, x5)
if_der_2_in_5_ga3(x1, x2, x3)  =  if_der_2_in_5_ga1(x3)
if_der_2_in_6_ga4(x1, x2, x3, x4)  =  if_der_2_in_6_ga1(x4)
if_der_2_in_4_ga5(x1, x2, x3, x4, x5)  =  if_der_2_in_4_ga4(x1, x2, x4, x5)
if_der_2_in_2_ga5(x1, x2, x3, x4, x5)  =  if_der_2_in_2_ga2(x3, x5)

Infinitary Constructor Rewriting Termination of PiTRS implies Termination of PROLOG



↳ PROLOG
  ↳ PrologToPiTRSProof
    ↳ PiTRS
      ↳ DependencyPairsProof

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

der_2_in_ga2(d_11(e_11(t_0)), const_11(1_0)) -> der_2_out_ga2(d_11(e_11(t_0)), const_11(1_0))
der_2_in_ga2(d_11(e_11(const_11(A))), const_11(0_0)) -> der_2_out_ga2(d_11(e_11(const_11(A))), const_11(0_0))
der_2_in_ga2(d_11(e_11(+2(X, Y))), +2(DX, DY)) -> if_der_2_in_1_ga5(X, Y, DX, DY, der_2_in_ga2(d_11(e_11(X)), DX))
der_2_in_ga2(d_11(e_11(*2(X, Y))), +2(*2(X, DY), *2(Y, DX))) -> if_der_2_in_3_ga5(X, Y, DY, DX, der_2_in_ga2(d_11(e_11(X)), DX))
der_2_in_ga2(d_11(d_11(X)), DDX) -> if_der_2_in_5_ga3(X, DDX, der_2_in_ga2(d_11(X), DX))
if_der_2_in_5_ga3(X, DDX, der_2_out_ga2(d_11(X), DX)) -> if_der_2_in_6_ga4(X, DDX, DX, der_2_in_ga2(d_11(e_11(DX)), DDX))
if_der_2_in_6_ga4(X, DDX, DX, der_2_out_ga2(d_11(e_11(DX)), DDX)) -> der_2_out_ga2(d_11(d_11(X)), DDX)
if_der_2_in_3_ga5(X, Y, DY, DX, der_2_out_ga2(d_11(e_11(X)), DX)) -> if_der_2_in_4_ga5(X, Y, DY, DX, der_2_in_ga2(d_11(e_11(Y)), DY))
if_der_2_in_4_ga5(X, Y, DY, DX, der_2_out_ga2(d_11(e_11(Y)), DY)) -> der_2_out_ga2(d_11(e_11(*2(X, Y))), +2(*2(X, DY), *2(Y, DX)))
if_der_2_in_1_ga5(X, Y, DX, DY, der_2_out_ga2(d_11(e_11(X)), DX)) -> if_der_2_in_2_ga5(X, Y, DX, DY, der_2_in_ga2(d_11(e_11(Y)), DY))
if_der_2_in_2_ga5(X, Y, DX, DY, der_2_out_ga2(d_11(e_11(Y)), DY)) -> der_2_out_ga2(d_11(e_11(+2(X, Y))), +2(DX, DY))

The argument filtering Pi contains the following mapping:
der_2_in_ga2(x1, x2)  =  der_2_in_ga1(x1)
d_11(x1)  =  d_11(x1)
e_11(x1)  =  e_11(x1)
t_0  =  t_0
const_11(x1)  =  const_11(x1)
1_0  =  1_0
0_0  =  0_0
+2(x1, x2)  =  +2(x1, x2)
*2(x1, x2)  =  *2(x1, x2)
der_2_out_ga2(x1, x2)  =  der_2_out_ga1(x2)
if_der_2_in_1_ga5(x1, x2, x3, x4, x5)  =  if_der_2_in_1_ga2(x2, x5)
if_der_2_in_3_ga5(x1, x2, x3, x4, x5)  =  if_der_2_in_3_ga3(x1, x2, x5)
if_der_2_in_5_ga3(x1, x2, x3)  =  if_der_2_in_5_ga1(x3)
if_der_2_in_6_ga4(x1, x2, x3, x4)  =  if_der_2_in_6_ga1(x4)
if_der_2_in_4_ga5(x1, x2, x3, x4, x5)  =  if_der_2_in_4_ga4(x1, x2, x4, x5)
if_der_2_in_2_ga5(x1, x2, x3, x4, x5)  =  if_der_2_in_2_ga2(x3, x5)


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

DER_2_IN_GA2(d_11(e_11(+2(X, Y))), +2(DX, DY)) -> IF_DER_2_IN_1_GA5(X, Y, DX, DY, der_2_in_ga2(d_11(e_11(X)), DX))
DER_2_IN_GA2(d_11(e_11(+2(X, Y))), +2(DX, DY)) -> DER_2_IN_GA2(d_11(e_11(X)), DX)
DER_2_IN_GA2(d_11(e_11(*2(X, Y))), +2(*2(X, DY), *2(Y, DX))) -> IF_DER_2_IN_3_GA5(X, Y, DY, DX, der_2_in_ga2(d_11(e_11(X)), DX))
DER_2_IN_GA2(d_11(e_11(*2(X, Y))), +2(*2(X, DY), *2(Y, DX))) -> DER_2_IN_GA2(d_11(e_11(X)), DX)
DER_2_IN_GA2(d_11(d_11(X)), DDX) -> IF_DER_2_IN_5_GA3(X, DDX, der_2_in_ga2(d_11(X), DX))
DER_2_IN_GA2(d_11(d_11(X)), DDX) -> DER_2_IN_GA2(d_11(X), DX)
IF_DER_2_IN_5_GA3(X, DDX, der_2_out_ga2(d_11(X), DX)) -> IF_DER_2_IN_6_GA4(X, DDX, DX, der_2_in_ga2(d_11(e_11(DX)), DDX))
IF_DER_2_IN_5_GA3(X, DDX, der_2_out_ga2(d_11(X), DX)) -> DER_2_IN_GA2(d_11(e_11(DX)), DDX)
IF_DER_2_IN_3_GA5(X, Y, DY, DX, der_2_out_ga2(d_11(e_11(X)), DX)) -> IF_DER_2_IN_4_GA5(X, Y, DY, DX, der_2_in_ga2(d_11(e_11(Y)), DY))
IF_DER_2_IN_3_GA5(X, Y, DY, DX, der_2_out_ga2(d_11(e_11(X)), DX)) -> DER_2_IN_GA2(d_11(e_11(Y)), DY)
IF_DER_2_IN_1_GA5(X, Y, DX, DY, der_2_out_ga2(d_11(e_11(X)), DX)) -> IF_DER_2_IN_2_GA5(X, Y, DX, DY, der_2_in_ga2(d_11(e_11(Y)), DY))
IF_DER_2_IN_1_GA5(X, Y, DX, DY, der_2_out_ga2(d_11(e_11(X)), DX)) -> DER_2_IN_GA2(d_11(e_11(Y)), DY)

The TRS R consists of the following rules:

der_2_in_ga2(d_11(e_11(t_0)), const_11(1_0)) -> der_2_out_ga2(d_11(e_11(t_0)), const_11(1_0))
der_2_in_ga2(d_11(e_11(const_11(A))), const_11(0_0)) -> der_2_out_ga2(d_11(e_11(const_11(A))), const_11(0_0))
der_2_in_ga2(d_11(e_11(+2(X, Y))), +2(DX, DY)) -> if_der_2_in_1_ga5(X, Y, DX, DY, der_2_in_ga2(d_11(e_11(X)), DX))
der_2_in_ga2(d_11(e_11(*2(X, Y))), +2(*2(X, DY), *2(Y, DX))) -> if_der_2_in_3_ga5(X, Y, DY, DX, der_2_in_ga2(d_11(e_11(X)), DX))
der_2_in_ga2(d_11(d_11(X)), DDX) -> if_der_2_in_5_ga3(X, DDX, der_2_in_ga2(d_11(X), DX))
if_der_2_in_5_ga3(X, DDX, der_2_out_ga2(d_11(X), DX)) -> if_der_2_in_6_ga4(X, DDX, DX, der_2_in_ga2(d_11(e_11(DX)), DDX))
if_der_2_in_6_ga4(X, DDX, DX, der_2_out_ga2(d_11(e_11(DX)), DDX)) -> der_2_out_ga2(d_11(d_11(X)), DDX)
if_der_2_in_3_ga5(X, Y, DY, DX, der_2_out_ga2(d_11(e_11(X)), DX)) -> if_der_2_in_4_ga5(X, Y, DY, DX, der_2_in_ga2(d_11(e_11(Y)), DY))
if_der_2_in_4_ga5(X, Y, DY, DX, der_2_out_ga2(d_11(e_11(Y)), DY)) -> der_2_out_ga2(d_11(e_11(*2(X, Y))), +2(*2(X, DY), *2(Y, DX)))
if_der_2_in_1_ga5(X, Y, DX, DY, der_2_out_ga2(d_11(e_11(X)), DX)) -> if_der_2_in_2_ga5(X, Y, DX, DY, der_2_in_ga2(d_11(e_11(Y)), DY))
if_der_2_in_2_ga5(X, Y, DX, DY, der_2_out_ga2(d_11(e_11(Y)), DY)) -> der_2_out_ga2(d_11(e_11(+2(X, Y))), +2(DX, DY))

The argument filtering Pi contains the following mapping:
der_2_in_ga2(x1, x2)  =  der_2_in_ga1(x1)
d_11(x1)  =  d_11(x1)
e_11(x1)  =  e_11(x1)
t_0  =  t_0
const_11(x1)  =  const_11(x1)
1_0  =  1_0
0_0  =  0_0
+2(x1, x2)  =  +2(x1, x2)
*2(x1, x2)  =  *2(x1, x2)
der_2_out_ga2(x1, x2)  =  der_2_out_ga1(x2)
if_der_2_in_1_ga5(x1, x2, x3, x4, x5)  =  if_der_2_in_1_ga2(x2, x5)
if_der_2_in_3_ga5(x1, x2, x3, x4, x5)  =  if_der_2_in_3_ga3(x1, x2, x5)
if_der_2_in_5_ga3(x1, x2, x3)  =  if_der_2_in_5_ga1(x3)
if_der_2_in_6_ga4(x1, x2, x3, x4)  =  if_der_2_in_6_ga1(x4)
if_der_2_in_4_ga5(x1, x2, x3, x4, x5)  =  if_der_2_in_4_ga4(x1, x2, x4, x5)
if_der_2_in_2_ga5(x1, x2, x3, x4, x5)  =  if_der_2_in_2_ga2(x3, x5)
DER_2_IN_GA2(x1, x2)  =  DER_2_IN_GA1(x1)
IF_DER_2_IN_4_GA5(x1, x2, x3, x4, x5)  =  IF_DER_2_IN_4_GA4(x1, x2, x4, x5)
IF_DER_2_IN_5_GA3(x1, x2, x3)  =  IF_DER_2_IN_5_GA1(x3)
IF_DER_2_IN_6_GA4(x1, x2, x3, x4)  =  IF_DER_2_IN_6_GA1(x4)
IF_DER_2_IN_3_GA5(x1, x2, x3, x4, x5)  =  IF_DER_2_IN_3_GA3(x1, x2, x5)
IF_DER_2_IN_1_GA5(x1, x2, x3, x4, x5)  =  IF_DER_2_IN_1_GA2(x2, x5)
IF_DER_2_IN_2_GA5(x1, x2, x3, x4, x5)  =  IF_DER_2_IN_2_GA2(x3, x5)

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

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

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

DER_2_IN_GA2(d_11(e_11(+2(X, Y))), +2(DX, DY)) -> IF_DER_2_IN_1_GA5(X, Y, DX, DY, der_2_in_ga2(d_11(e_11(X)), DX))
DER_2_IN_GA2(d_11(e_11(+2(X, Y))), +2(DX, DY)) -> DER_2_IN_GA2(d_11(e_11(X)), DX)
DER_2_IN_GA2(d_11(e_11(*2(X, Y))), +2(*2(X, DY), *2(Y, DX))) -> IF_DER_2_IN_3_GA5(X, Y, DY, DX, der_2_in_ga2(d_11(e_11(X)), DX))
DER_2_IN_GA2(d_11(e_11(*2(X, Y))), +2(*2(X, DY), *2(Y, DX))) -> DER_2_IN_GA2(d_11(e_11(X)), DX)
DER_2_IN_GA2(d_11(d_11(X)), DDX) -> IF_DER_2_IN_5_GA3(X, DDX, der_2_in_ga2(d_11(X), DX))
DER_2_IN_GA2(d_11(d_11(X)), DDX) -> DER_2_IN_GA2(d_11(X), DX)
IF_DER_2_IN_5_GA3(X, DDX, der_2_out_ga2(d_11(X), DX)) -> IF_DER_2_IN_6_GA4(X, DDX, DX, der_2_in_ga2(d_11(e_11(DX)), DDX))
IF_DER_2_IN_5_GA3(X, DDX, der_2_out_ga2(d_11(X), DX)) -> DER_2_IN_GA2(d_11(e_11(DX)), DDX)
IF_DER_2_IN_3_GA5(X, Y, DY, DX, der_2_out_ga2(d_11(e_11(X)), DX)) -> IF_DER_2_IN_4_GA5(X, Y, DY, DX, der_2_in_ga2(d_11(e_11(Y)), DY))
IF_DER_2_IN_3_GA5(X, Y, DY, DX, der_2_out_ga2(d_11(e_11(X)), DX)) -> DER_2_IN_GA2(d_11(e_11(Y)), DY)
IF_DER_2_IN_1_GA5(X, Y, DX, DY, der_2_out_ga2(d_11(e_11(X)), DX)) -> IF_DER_2_IN_2_GA5(X, Y, DX, DY, der_2_in_ga2(d_11(e_11(Y)), DY))
IF_DER_2_IN_1_GA5(X, Y, DX, DY, der_2_out_ga2(d_11(e_11(X)), DX)) -> DER_2_IN_GA2(d_11(e_11(Y)), DY)

The TRS R consists of the following rules:

der_2_in_ga2(d_11(e_11(t_0)), const_11(1_0)) -> der_2_out_ga2(d_11(e_11(t_0)), const_11(1_0))
der_2_in_ga2(d_11(e_11(const_11(A))), const_11(0_0)) -> der_2_out_ga2(d_11(e_11(const_11(A))), const_11(0_0))
der_2_in_ga2(d_11(e_11(+2(X, Y))), +2(DX, DY)) -> if_der_2_in_1_ga5(X, Y, DX, DY, der_2_in_ga2(d_11(e_11(X)), DX))
der_2_in_ga2(d_11(e_11(*2(X, Y))), +2(*2(X, DY), *2(Y, DX))) -> if_der_2_in_3_ga5(X, Y, DY, DX, der_2_in_ga2(d_11(e_11(X)), DX))
der_2_in_ga2(d_11(d_11(X)), DDX) -> if_der_2_in_5_ga3(X, DDX, der_2_in_ga2(d_11(X), DX))
if_der_2_in_5_ga3(X, DDX, der_2_out_ga2(d_11(X), DX)) -> if_der_2_in_6_ga4(X, DDX, DX, der_2_in_ga2(d_11(e_11(DX)), DDX))
if_der_2_in_6_ga4(X, DDX, DX, der_2_out_ga2(d_11(e_11(DX)), DDX)) -> der_2_out_ga2(d_11(d_11(X)), DDX)
if_der_2_in_3_ga5(X, Y, DY, DX, der_2_out_ga2(d_11(e_11(X)), DX)) -> if_der_2_in_4_ga5(X, Y, DY, DX, der_2_in_ga2(d_11(e_11(Y)), DY))
if_der_2_in_4_ga5(X, Y, DY, DX, der_2_out_ga2(d_11(e_11(Y)), DY)) -> der_2_out_ga2(d_11(e_11(*2(X, Y))), +2(*2(X, DY), *2(Y, DX)))
if_der_2_in_1_ga5(X, Y, DX, DY, der_2_out_ga2(d_11(e_11(X)), DX)) -> if_der_2_in_2_ga5(X, Y, DX, DY, der_2_in_ga2(d_11(e_11(Y)), DY))
if_der_2_in_2_ga5(X, Y, DX, DY, der_2_out_ga2(d_11(e_11(Y)), DY)) -> der_2_out_ga2(d_11(e_11(+2(X, Y))), +2(DX, DY))

The argument filtering Pi contains the following mapping:
der_2_in_ga2(x1, x2)  =  der_2_in_ga1(x1)
d_11(x1)  =  d_11(x1)
e_11(x1)  =  e_11(x1)
t_0  =  t_0
const_11(x1)  =  const_11(x1)
1_0  =  1_0
0_0  =  0_0
+2(x1, x2)  =  +2(x1, x2)
*2(x1, x2)  =  *2(x1, x2)
der_2_out_ga2(x1, x2)  =  der_2_out_ga1(x2)
if_der_2_in_1_ga5(x1, x2, x3, x4, x5)  =  if_der_2_in_1_ga2(x2, x5)
if_der_2_in_3_ga5(x1, x2, x3, x4, x5)  =  if_der_2_in_3_ga3(x1, x2, x5)
if_der_2_in_5_ga3(x1, x2, x3)  =  if_der_2_in_5_ga1(x3)
if_der_2_in_6_ga4(x1, x2, x3, x4)  =  if_der_2_in_6_ga1(x4)
if_der_2_in_4_ga5(x1, x2, x3, x4, x5)  =  if_der_2_in_4_ga4(x1, x2, x4, x5)
if_der_2_in_2_ga5(x1, x2, x3, x4, x5)  =  if_der_2_in_2_ga2(x3, x5)
DER_2_IN_GA2(x1, x2)  =  DER_2_IN_GA1(x1)
IF_DER_2_IN_4_GA5(x1, x2, x3, x4, x5)  =  IF_DER_2_IN_4_GA4(x1, x2, x4, x5)
IF_DER_2_IN_5_GA3(x1, x2, x3)  =  IF_DER_2_IN_5_GA1(x3)
IF_DER_2_IN_6_GA4(x1, x2, x3, x4)  =  IF_DER_2_IN_6_GA1(x4)
IF_DER_2_IN_3_GA5(x1, x2, x3, x4, x5)  =  IF_DER_2_IN_3_GA3(x1, x2, x5)
IF_DER_2_IN_1_GA5(x1, x2, x3, x4, x5)  =  IF_DER_2_IN_1_GA2(x2, x5)
IF_DER_2_IN_2_GA5(x1, x2, x3, x4, x5)  =  IF_DER_2_IN_2_GA2(x3, x5)

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

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

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

IF_DER_2_IN_3_GA5(X, Y, DY, DX, der_2_out_ga2(d_11(e_11(X)), DX)) -> DER_2_IN_GA2(d_11(e_11(Y)), DY)
IF_DER_2_IN_1_GA5(X, Y, DX, DY, der_2_out_ga2(d_11(e_11(X)), DX)) -> DER_2_IN_GA2(d_11(e_11(Y)), DY)
DER_2_IN_GA2(d_11(e_11(+2(X, Y))), +2(DX, DY)) -> DER_2_IN_GA2(d_11(e_11(X)), DX)
DER_2_IN_GA2(d_11(e_11(+2(X, Y))), +2(DX, DY)) -> IF_DER_2_IN_1_GA5(X, Y, DX, DY, der_2_in_ga2(d_11(e_11(X)), DX))
DER_2_IN_GA2(d_11(e_11(*2(X, Y))), +2(*2(X, DY), *2(Y, DX))) -> DER_2_IN_GA2(d_11(e_11(X)), DX)
DER_2_IN_GA2(d_11(e_11(*2(X, Y))), +2(*2(X, DY), *2(Y, DX))) -> IF_DER_2_IN_3_GA5(X, Y, DY, DX, der_2_in_ga2(d_11(e_11(X)), DX))

The TRS R consists of the following rules:

der_2_in_ga2(d_11(e_11(t_0)), const_11(1_0)) -> der_2_out_ga2(d_11(e_11(t_0)), const_11(1_0))
der_2_in_ga2(d_11(e_11(const_11(A))), const_11(0_0)) -> der_2_out_ga2(d_11(e_11(const_11(A))), const_11(0_0))
der_2_in_ga2(d_11(e_11(+2(X, Y))), +2(DX, DY)) -> if_der_2_in_1_ga5(X, Y, DX, DY, der_2_in_ga2(d_11(e_11(X)), DX))
der_2_in_ga2(d_11(e_11(*2(X, Y))), +2(*2(X, DY), *2(Y, DX))) -> if_der_2_in_3_ga5(X, Y, DY, DX, der_2_in_ga2(d_11(e_11(X)), DX))
der_2_in_ga2(d_11(d_11(X)), DDX) -> if_der_2_in_5_ga3(X, DDX, der_2_in_ga2(d_11(X), DX))
if_der_2_in_5_ga3(X, DDX, der_2_out_ga2(d_11(X), DX)) -> if_der_2_in_6_ga4(X, DDX, DX, der_2_in_ga2(d_11(e_11(DX)), DDX))
if_der_2_in_6_ga4(X, DDX, DX, der_2_out_ga2(d_11(e_11(DX)), DDX)) -> der_2_out_ga2(d_11(d_11(X)), DDX)
if_der_2_in_3_ga5(X, Y, DY, DX, der_2_out_ga2(d_11(e_11(X)), DX)) -> if_der_2_in_4_ga5(X, Y, DY, DX, der_2_in_ga2(d_11(e_11(Y)), DY))
if_der_2_in_4_ga5(X, Y, DY, DX, der_2_out_ga2(d_11(e_11(Y)), DY)) -> der_2_out_ga2(d_11(e_11(*2(X, Y))), +2(*2(X, DY), *2(Y, DX)))
if_der_2_in_1_ga5(X, Y, DX, DY, der_2_out_ga2(d_11(e_11(X)), DX)) -> if_der_2_in_2_ga5(X, Y, DX, DY, der_2_in_ga2(d_11(e_11(Y)), DY))
if_der_2_in_2_ga5(X, Y, DX, DY, der_2_out_ga2(d_11(e_11(Y)), DY)) -> der_2_out_ga2(d_11(e_11(+2(X, Y))), +2(DX, DY))

The argument filtering Pi contains the following mapping:
der_2_in_ga2(x1, x2)  =  der_2_in_ga1(x1)
d_11(x1)  =  d_11(x1)
e_11(x1)  =  e_11(x1)
t_0  =  t_0
const_11(x1)  =  const_11(x1)
1_0  =  1_0
0_0  =  0_0
+2(x1, x2)  =  +2(x1, x2)
*2(x1, x2)  =  *2(x1, x2)
der_2_out_ga2(x1, x2)  =  der_2_out_ga1(x2)
if_der_2_in_1_ga5(x1, x2, x3, x4, x5)  =  if_der_2_in_1_ga2(x2, x5)
if_der_2_in_3_ga5(x1, x2, x3, x4, x5)  =  if_der_2_in_3_ga3(x1, x2, x5)
if_der_2_in_5_ga3(x1, x2, x3)  =  if_der_2_in_5_ga1(x3)
if_der_2_in_6_ga4(x1, x2, x3, x4)  =  if_der_2_in_6_ga1(x4)
if_der_2_in_4_ga5(x1, x2, x3, x4, x5)  =  if_der_2_in_4_ga4(x1, x2, x4, x5)
if_der_2_in_2_ga5(x1, x2, x3, x4, x5)  =  if_der_2_in_2_ga2(x3, x5)
DER_2_IN_GA2(x1, x2)  =  DER_2_IN_GA1(x1)
IF_DER_2_IN_3_GA5(x1, x2, x3, x4, x5)  =  IF_DER_2_IN_3_GA3(x1, x2, x5)
IF_DER_2_IN_1_GA5(x1, x2, x3, x4, x5)  =  IF_DER_2_IN_1_GA2(x2, x5)

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

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

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

IF_DER_2_IN_3_GA5(X, Y, DY, DX, der_2_out_ga2(d_11(e_11(X)), DX)) -> DER_2_IN_GA2(d_11(e_11(Y)), DY)
IF_DER_2_IN_1_GA5(X, Y, DX, DY, der_2_out_ga2(d_11(e_11(X)), DX)) -> DER_2_IN_GA2(d_11(e_11(Y)), DY)
DER_2_IN_GA2(d_11(e_11(+2(X, Y))), +2(DX, DY)) -> DER_2_IN_GA2(d_11(e_11(X)), DX)
DER_2_IN_GA2(d_11(e_11(+2(X, Y))), +2(DX, DY)) -> IF_DER_2_IN_1_GA5(X, Y, DX, DY, der_2_in_ga2(d_11(e_11(X)), DX))
DER_2_IN_GA2(d_11(e_11(*2(X, Y))), +2(*2(X, DY), *2(Y, DX))) -> DER_2_IN_GA2(d_11(e_11(X)), DX)
DER_2_IN_GA2(d_11(e_11(*2(X, Y))), +2(*2(X, DY), *2(Y, DX))) -> IF_DER_2_IN_3_GA5(X, Y, DY, DX, der_2_in_ga2(d_11(e_11(X)), DX))

The TRS R consists of the following rules:

der_2_in_ga2(d_11(e_11(t_0)), const_11(1_0)) -> der_2_out_ga2(d_11(e_11(t_0)), const_11(1_0))
der_2_in_ga2(d_11(e_11(const_11(A))), const_11(0_0)) -> der_2_out_ga2(d_11(e_11(const_11(A))), const_11(0_0))
der_2_in_ga2(d_11(e_11(+2(X, Y))), +2(DX, DY)) -> if_der_2_in_1_ga5(X, Y, DX, DY, der_2_in_ga2(d_11(e_11(X)), DX))
der_2_in_ga2(d_11(e_11(*2(X, Y))), +2(*2(X, DY), *2(Y, DX))) -> if_der_2_in_3_ga5(X, Y, DY, DX, der_2_in_ga2(d_11(e_11(X)), DX))
if_der_2_in_1_ga5(X, Y, DX, DY, der_2_out_ga2(d_11(e_11(X)), DX)) -> if_der_2_in_2_ga5(X, Y, DX, DY, der_2_in_ga2(d_11(e_11(Y)), DY))
if_der_2_in_3_ga5(X, Y, DY, DX, der_2_out_ga2(d_11(e_11(X)), DX)) -> if_der_2_in_4_ga5(X, Y, DY, DX, der_2_in_ga2(d_11(e_11(Y)), DY))
if_der_2_in_2_ga5(X, Y, DX, DY, der_2_out_ga2(d_11(e_11(Y)), DY)) -> der_2_out_ga2(d_11(e_11(+2(X, Y))), +2(DX, DY))
if_der_2_in_4_ga5(X, Y, DY, DX, der_2_out_ga2(d_11(e_11(Y)), DY)) -> der_2_out_ga2(d_11(e_11(*2(X, Y))), +2(*2(X, DY), *2(Y, DX)))

The argument filtering Pi contains the following mapping:
der_2_in_ga2(x1, x2)  =  der_2_in_ga1(x1)
d_11(x1)  =  d_11(x1)
e_11(x1)  =  e_11(x1)
t_0  =  t_0
const_11(x1)  =  const_11(x1)
1_0  =  1_0
0_0  =  0_0
+2(x1, x2)  =  +2(x1, x2)
*2(x1, x2)  =  *2(x1, x2)
der_2_out_ga2(x1, x2)  =  der_2_out_ga1(x2)
if_der_2_in_1_ga5(x1, x2, x3, x4, x5)  =  if_der_2_in_1_ga2(x2, x5)
if_der_2_in_3_ga5(x1, x2, x3, x4, x5)  =  if_der_2_in_3_ga3(x1, x2, x5)
if_der_2_in_4_ga5(x1, x2, x3, x4, x5)  =  if_der_2_in_4_ga4(x1, x2, x4, x5)
if_der_2_in_2_ga5(x1, x2, x3, x4, x5)  =  if_der_2_in_2_ga2(x3, x5)
DER_2_IN_GA2(x1, x2)  =  DER_2_IN_GA1(x1)
IF_DER_2_IN_3_GA5(x1, x2, x3, x4, x5)  =  IF_DER_2_IN_3_GA3(x1, x2, x5)
IF_DER_2_IN_1_GA5(x1, x2, x3, x4, x5)  =  IF_DER_2_IN_1_GA2(x2, x5)

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
  ↳ PrologToPiTRSProof
    ↳ PiTRS
      ↳ DependencyPairsProof
        ↳ PiDP
          ↳ DependencyGraphProof
            ↳ AND
              ↳ PiDP
                ↳ UsableRulesProof
                  ↳ PiDP
                    ↳ PiDPToQDPProof
                      ↳ QDP
                        ↳ QDPSizeChangeProof
              ↳ PiDP

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

IF_DER_2_IN_3_GA3(X, Y, der_2_out_ga1(DX)) -> DER_2_IN_GA1(d_11(e_11(Y)))
IF_DER_2_IN_1_GA2(Y, der_2_out_ga1(DX)) -> DER_2_IN_GA1(d_11(e_11(Y)))
DER_2_IN_GA1(d_11(e_11(+2(X, Y)))) -> DER_2_IN_GA1(d_11(e_11(X)))
DER_2_IN_GA1(d_11(e_11(+2(X, Y)))) -> IF_DER_2_IN_1_GA2(Y, der_2_in_ga1(d_11(e_11(X))))
DER_2_IN_GA1(d_11(e_11(*2(X, Y)))) -> DER_2_IN_GA1(d_11(e_11(X)))
DER_2_IN_GA1(d_11(e_11(*2(X, Y)))) -> IF_DER_2_IN_3_GA3(X, Y, der_2_in_ga1(d_11(e_11(X))))

The TRS R consists of the following rules:

der_2_in_ga1(d_11(e_11(t_0))) -> der_2_out_ga1(const_11(1_0))
der_2_in_ga1(d_11(e_11(const_11(A)))) -> der_2_out_ga1(const_11(0_0))
der_2_in_ga1(d_11(e_11(+2(X, Y)))) -> if_der_2_in_1_ga2(Y, der_2_in_ga1(d_11(e_11(X))))
der_2_in_ga1(d_11(e_11(*2(X, Y)))) -> if_der_2_in_3_ga3(X, Y, der_2_in_ga1(d_11(e_11(X))))
if_der_2_in_1_ga2(Y, der_2_out_ga1(DX)) -> if_der_2_in_2_ga2(DX, der_2_in_ga1(d_11(e_11(Y))))
if_der_2_in_3_ga3(X, Y, der_2_out_ga1(DX)) -> if_der_2_in_4_ga4(X, Y, DX, der_2_in_ga1(d_11(e_11(Y))))
if_der_2_in_2_ga2(DX, der_2_out_ga1(DY)) -> der_2_out_ga1(+2(DX, DY))
if_der_2_in_4_ga4(X, Y, DX, der_2_out_ga1(DY)) -> der_2_out_ga1(+2(*2(X, DY), *2(Y, DX)))

The set Q consists of the following terms:

der_2_in_ga1(x0)
if_der_2_in_1_ga2(x0, x1)
if_der_2_in_3_ga3(x0, x1, x2)
if_der_2_in_2_ga2(x0, x1)
if_der_2_in_4_ga4(x0, x1, x2, x3)

We have to consider all (P,Q,R)-chains.
The head symbols of this DP problem are {DER_2_IN_GA1, IF_DER_2_IN_3_GA3, IF_DER_2_IN_1_GA2}.
We used the following order and afs together with the size-change analysis to show that there are no infinite chains for this DP problem.

Order:Homeomorphic Embedding Order

AFS:
d_11(x1)  =  x1
der_2_out_ga1(x1)  =  der_2_out_ga
e_11(x1)  =  x1
*2(x1, x2)  =  *2(x1, x2)
+2(x1, x2)  =  +2(x1, x2)

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

We oriented the following set of usable rules. none


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

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

DER_2_IN_GA2(d_11(d_11(X)), DDX) -> DER_2_IN_GA2(d_11(X), DX)

The TRS R consists of the following rules:

der_2_in_ga2(d_11(e_11(t_0)), const_11(1_0)) -> der_2_out_ga2(d_11(e_11(t_0)), const_11(1_0))
der_2_in_ga2(d_11(e_11(const_11(A))), const_11(0_0)) -> der_2_out_ga2(d_11(e_11(const_11(A))), const_11(0_0))
der_2_in_ga2(d_11(e_11(+2(X, Y))), +2(DX, DY)) -> if_der_2_in_1_ga5(X, Y, DX, DY, der_2_in_ga2(d_11(e_11(X)), DX))
der_2_in_ga2(d_11(e_11(*2(X, Y))), +2(*2(X, DY), *2(Y, DX))) -> if_der_2_in_3_ga5(X, Y, DY, DX, der_2_in_ga2(d_11(e_11(X)), DX))
der_2_in_ga2(d_11(d_11(X)), DDX) -> if_der_2_in_5_ga3(X, DDX, der_2_in_ga2(d_11(X), DX))
if_der_2_in_5_ga3(X, DDX, der_2_out_ga2(d_11(X), DX)) -> if_der_2_in_6_ga4(X, DDX, DX, der_2_in_ga2(d_11(e_11(DX)), DDX))
if_der_2_in_6_ga4(X, DDX, DX, der_2_out_ga2(d_11(e_11(DX)), DDX)) -> der_2_out_ga2(d_11(d_11(X)), DDX)
if_der_2_in_3_ga5(X, Y, DY, DX, der_2_out_ga2(d_11(e_11(X)), DX)) -> if_der_2_in_4_ga5(X, Y, DY, DX, der_2_in_ga2(d_11(e_11(Y)), DY))
if_der_2_in_4_ga5(X, Y, DY, DX, der_2_out_ga2(d_11(e_11(Y)), DY)) -> der_2_out_ga2(d_11(e_11(*2(X, Y))), +2(*2(X, DY), *2(Y, DX)))
if_der_2_in_1_ga5(X, Y, DX, DY, der_2_out_ga2(d_11(e_11(X)), DX)) -> if_der_2_in_2_ga5(X, Y, DX, DY, der_2_in_ga2(d_11(e_11(Y)), DY))
if_der_2_in_2_ga5(X, Y, DX, DY, der_2_out_ga2(d_11(e_11(Y)), DY)) -> der_2_out_ga2(d_11(e_11(+2(X, Y))), +2(DX, DY))

The argument filtering Pi contains the following mapping:
der_2_in_ga2(x1, x2)  =  der_2_in_ga1(x1)
d_11(x1)  =  d_11(x1)
e_11(x1)  =  e_11(x1)
t_0  =  t_0
const_11(x1)  =  const_11(x1)
1_0  =  1_0
0_0  =  0_0
+2(x1, x2)  =  +2(x1, x2)
*2(x1, x2)  =  *2(x1, x2)
der_2_out_ga2(x1, x2)  =  der_2_out_ga1(x2)
if_der_2_in_1_ga5(x1, x2, x3, x4, x5)  =  if_der_2_in_1_ga2(x2, x5)
if_der_2_in_3_ga5(x1, x2, x3, x4, x5)  =  if_der_2_in_3_ga3(x1, x2, x5)
if_der_2_in_5_ga3(x1, x2, x3)  =  if_der_2_in_5_ga1(x3)
if_der_2_in_6_ga4(x1, x2, x3, x4)  =  if_der_2_in_6_ga1(x4)
if_der_2_in_4_ga5(x1, x2, x3, x4, x5)  =  if_der_2_in_4_ga4(x1, x2, x4, x5)
if_der_2_in_2_ga5(x1, x2, x3, x4, x5)  =  if_der_2_in_2_ga2(x3, x5)
DER_2_IN_GA2(x1, x2)  =  DER_2_IN_GA1(x1)

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

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

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

DER_2_IN_GA2(d_11(d_11(X)), DDX) -> DER_2_IN_GA2(d_11(X), DX)

R is empty.
The argument filtering Pi contains the following mapping:
d_11(x1)  =  d_11(x1)
DER_2_IN_GA2(x1, x2)  =  DER_2_IN_GA1(x1)

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
  ↳ PrologToPiTRSProof
    ↳ PiTRS
      ↳ DependencyPairsProof
        ↳ PiDP
          ↳ DependencyGraphProof
            ↳ AND
              ↳ PiDP
              ↳ PiDP
                ↳ UsableRulesProof
                  ↳ PiDP
                    ↳ PiDPToQDPProof
                      ↳ QDP
                        ↳ QDPSizeChangeProof

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

DER_2_IN_GA1(d_11(d_11(X))) -> DER_2_IN_GA1(d_11(X))

R is empty.
Q is empty.
We have to consider all (P,Q,R)-chains.
The head symbols of this DP problem are {DER_2_IN_GA1}.
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: