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



↳ PROLOG
  ↳ PrologToPiTRSProof

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


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


p_2_in_ga2(d_11(e_11(t_0)), const_11(1_0)) -> p_2_out_ga2(d_11(e_11(t_0)), const_11(1_0))
p_2_in_ga2(d_11(e_11(const_11(A))), const_11(0_0)) -> p_2_out_ga2(d_11(e_11(const_11(A))), const_11(0_0))
p_2_in_ga2(d_11(e_11(+2(X, Y))), +2(DX, DY)) -> if_p_2_in_1_ga5(X, Y, DX, DY, p_2_in_ga2(d_11(e_11(X)), DX))
p_2_in_ga2(d_11(e_11(*2(X, Y))), +2(*2(X, DY), *2(Y, DX))) -> if_p_2_in_3_ga5(X, Y, DY, DX, p_2_in_ga2(d_11(e_11(X)), DX))
p_2_in_ga2(d_11(d_11(X)), DDX) -> if_p_2_in_5_ga3(X, DDX, p_2_in_ga2(d_11(X), DX))
if_p_2_in_5_ga3(X, DDX, p_2_out_ga2(d_11(X), DX)) -> if_p_2_in_6_ga4(X, DDX, DX, p_2_in_ga2(d_11(e_11(DX)), DDX))
if_p_2_in_6_ga4(X, DDX, DX, p_2_out_ga2(d_11(e_11(DX)), DDX)) -> p_2_out_ga2(d_11(d_11(X)), DDX)
if_p_2_in_3_ga5(X, Y, DY, DX, p_2_out_ga2(d_11(e_11(X)), DX)) -> if_p_2_in_4_ga5(X, Y, DY, DX, p_2_in_ga2(d_11(e_11(Y)), DY))
if_p_2_in_4_ga5(X, Y, DY, DX, p_2_out_ga2(d_11(e_11(Y)), DY)) -> p_2_out_ga2(d_11(e_11(*2(X, Y))), +2(*2(X, DY), *2(Y, DX)))
if_p_2_in_1_ga5(X, Y, DX, DY, p_2_out_ga2(d_11(e_11(X)), DX)) -> if_p_2_in_2_ga5(X, Y, DX, DY, p_2_in_ga2(d_11(e_11(Y)), DY))
if_p_2_in_2_ga5(X, Y, DX, DY, p_2_out_ga2(d_11(e_11(Y)), DY)) -> p_2_out_ga2(d_11(e_11(+2(X, Y))), +2(DX, DY))

The argument filtering Pi contains the following mapping:
p_2_in_ga2(x1, x2)  =  p_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)
p_2_out_ga2(x1, x2)  =  p_2_out_ga1(x2)
if_p_2_in_1_ga5(x1, x2, x3, x4, x5)  =  if_p_2_in_1_ga2(x2, x5)
if_p_2_in_3_ga5(x1, x2, x3, x4, x5)  =  if_p_2_in_3_ga3(x1, x2, x5)
if_p_2_in_5_ga3(x1, x2, x3)  =  if_p_2_in_5_ga1(x3)
if_p_2_in_6_ga4(x1, x2, x3, x4)  =  if_p_2_in_6_ga1(x4)
if_p_2_in_4_ga5(x1, x2, x3, x4, x5)  =  if_p_2_in_4_ga4(x1, x2, x4, x5)
if_p_2_in_2_ga5(x1, x2, x3, x4, x5)  =  if_p_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:

p_2_in_ga2(d_11(e_11(t_0)), const_11(1_0)) -> p_2_out_ga2(d_11(e_11(t_0)), const_11(1_0))
p_2_in_ga2(d_11(e_11(const_11(A))), const_11(0_0)) -> p_2_out_ga2(d_11(e_11(const_11(A))), const_11(0_0))
p_2_in_ga2(d_11(e_11(+2(X, Y))), +2(DX, DY)) -> if_p_2_in_1_ga5(X, Y, DX, DY, p_2_in_ga2(d_11(e_11(X)), DX))
p_2_in_ga2(d_11(e_11(*2(X, Y))), +2(*2(X, DY), *2(Y, DX))) -> if_p_2_in_3_ga5(X, Y, DY, DX, p_2_in_ga2(d_11(e_11(X)), DX))
p_2_in_ga2(d_11(d_11(X)), DDX) -> if_p_2_in_5_ga3(X, DDX, p_2_in_ga2(d_11(X), DX))
if_p_2_in_5_ga3(X, DDX, p_2_out_ga2(d_11(X), DX)) -> if_p_2_in_6_ga4(X, DDX, DX, p_2_in_ga2(d_11(e_11(DX)), DDX))
if_p_2_in_6_ga4(X, DDX, DX, p_2_out_ga2(d_11(e_11(DX)), DDX)) -> p_2_out_ga2(d_11(d_11(X)), DDX)
if_p_2_in_3_ga5(X, Y, DY, DX, p_2_out_ga2(d_11(e_11(X)), DX)) -> if_p_2_in_4_ga5(X, Y, DY, DX, p_2_in_ga2(d_11(e_11(Y)), DY))
if_p_2_in_4_ga5(X, Y, DY, DX, p_2_out_ga2(d_11(e_11(Y)), DY)) -> p_2_out_ga2(d_11(e_11(*2(X, Y))), +2(*2(X, DY), *2(Y, DX)))
if_p_2_in_1_ga5(X, Y, DX, DY, p_2_out_ga2(d_11(e_11(X)), DX)) -> if_p_2_in_2_ga5(X, Y, DX, DY, p_2_in_ga2(d_11(e_11(Y)), DY))
if_p_2_in_2_ga5(X, Y, DX, DY, p_2_out_ga2(d_11(e_11(Y)), DY)) -> p_2_out_ga2(d_11(e_11(+2(X, Y))), +2(DX, DY))

The argument filtering Pi contains the following mapping:
p_2_in_ga2(x1, x2)  =  p_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)
p_2_out_ga2(x1, x2)  =  p_2_out_ga1(x2)
if_p_2_in_1_ga5(x1, x2, x3, x4, x5)  =  if_p_2_in_1_ga2(x2, x5)
if_p_2_in_3_ga5(x1, x2, x3, x4, x5)  =  if_p_2_in_3_ga3(x1, x2, x5)
if_p_2_in_5_ga3(x1, x2, x3)  =  if_p_2_in_5_ga1(x3)
if_p_2_in_6_ga4(x1, x2, x3, x4)  =  if_p_2_in_6_ga1(x4)
if_p_2_in_4_ga5(x1, x2, x3, x4, x5)  =  if_p_2_in_4_ga4(x1, x2, x4, x5)
if_p_2_in_2_ga5(x1, x2, x3, x4, x5)  =  if_p_2_in_2_ga2(x3, x5)


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

P_2_IN_GA2(d_11(e_11(+2(X, Y))), +2(DX, DY)) -> IF_P_2_IN_1_GA5(X, Y, DX, DY, p_2_in_ga2(d_11(e_11(X)), DX))
P_2_IN_GA2(d_11(e_11(+2(X, Y))), +2(DX, DY)) -> P_2_IN_GA2(d_11(e_11(X)), DX)
P_2_IN_GA2(d_11(e_11(*2(X, Y))), +2(*2(X, DY), *2(Y, DX))) -> IF_P_2_IN_3_GA5(X, Y, DY, DX, p_2_in_ga2(d_11(e_11(X)), DX))
P_2_IN_GA2(d_11(e_11(*2(X, Y))), +2(*2(X, DY), *2(Y, DX))) -> P_2_IN_GA2(d_11(e_11(X)), DX)
P_2_IN_GA2(d_11(d_11(X)), DDX) -> IF_P_2_IN_5_GA3(X, DDX, p_2_in_ga2(d_11(X), DX))
P_2_IN_GA2(d_11(d_11(X)), DDX) -> P_2_IN_GA2(d_11(X), DX)
IF_P_2_IN_5_GA3(X, DDX, p_2_out_ga2(d_11(X), DX)) -> IF_P_2_IN_6_GA4(X, DDX, DX, p_2_in_ga2(d_11(e_11(DX)), DDX))
IF_P_2_IN_5_GA3(X, DDX, p_2_out_ga2(d_11(X), DX)) -> P_2_IN_GA2(d_11(e_11(DX)), DDX)
IF_P_2_IN_3_GA5(X, Y, DY, DX, p_2_out_ga2(d_11(e_11(X)), DX)) -> IF_P_2_IN_4_GA5(X, Y, DY, DX, p_2_in_ga2(d_11(e_11(Y)), DY))
IF_P_2_IN_3_GA5(X, Y, DY, DX, p_2_out_ga2(d_11(e_11(X)), DX)) -> P_2_IN_GA2(d_11(e_11(Y)), DY)
IF_P_2_IN_1_GA5(X, Y, DX, DY, p_2_out_ga2(d_11(e_11(X)), DX)) -> IF_P_2_IN_2_GA5(X, Y, DX, DY, p_2_in_ga2(d_11(e_11(Y)), DY))
IF_P_2_IN_1_GA5(X, Y, DX, DY, p_2_out_ga2(d_11(e_11(X)), DX)) -> P_2_IN_GA2(d_11(e_11(Y)), DY)

The TRS R consists of the following rules:

p_2_in_ga2(d_11(e_11(t_0)), const_11(1_0)) -> p_2_out_ga2(d_11(e_11(t_0)), const_11(1_0))
p_2_in_ga2(d_11(e_11(const_11(A))), const_11(0_0)) -> p_2_out_ga2(d_11(e_11(const_11(A))), const_11(0_0))
p_2_in_ga2(d_11(e_11(+2(X, Y))), +2(DX, DY)) -> if_p_2_in_1_ga5(X, Y, DX, DY, p_2_in_ga2(d_11(e_11(X)), DX))
p_2_in_ga2(d_11(e_11(*2(X, Y))), +2(*2(X, DY), *2(Y, DX))) -> if_p_2_in_3_ga5(X, Y, DY, DX, p_2_in_ga2(d_11(e_11(X)), DX))
p_2_in_ga2(d_11(d_11(X)), DDX) -> if_p_2_in_5_ga3(X, DDX, p_2_in_ga2(d_11(X), DX))
if_p_2_in_5_ga3(X, DDX, p_2_out_ga2(d_11(X), DX)) -> if_p_2_in_6_ga4(X, DDX, DX, p_2_in_ga2(d_11(e_11(DX)), DDX))
if_p_2_in_6_ga4(X, DDX, DX, p_2_out_ga2(d_11(e_11(DX)), DDX)) -> p_2_out_ga2(d_11(d_11(X)), DDX)
if_p_2_in_3_ga5(X, Y, DY, DX, p_2_out_ga2(d_11(e_11(X)), DX)) -> if_p_2_in_4_ga5(X, Y, DY, DX, p_2_in_ga2(d_11(e_11(Y)), DY))
if_p_2_in_4_ga5(X, Y, DY, DX, p_2_out_ga2(d_11(e_11(Y)), DY)) -> p_2_out_ga2(d_11(e_11(*2(X, Y))), +2(*2(X, DY), *2(Y, DX)))
if_p_2_in_1_ga5(X, Y, DX, DY, p_2_out_ga2(d_11(e_11(X)), DX)) -> if_p_2_in_2_ga5(X, Y, DX, DY, p_2_in_ga2(d_11(e_11(Y)), DY))
if_p_2_in_2_ga5(X, Y, DX, DY, p_2_out_ga2(d_11(e_11(Y)), DY)) -> p_2_out_ga2(d_11(e_11(+2(X, Y))), +2(DX, DY))

The argument filtering Pi contains the following mapping:
p_2_in_ga2(x1, x2)  =  p_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)
p_2_out_ga2(x1, x2)  =  p_2_out_ga1(x2)
if_p_2_in_1_ga5(x1, x2, x3, x4, x5)  =  if_p_2_in_1_ga2(x2, x5)
if_p_2_in_3_ga5(x1, x2, x3, x4, x5)  =  if_p_2_in_3_ga3(x1, x2, x5)
if_p_2_in_5_ga3(x1, x2, x3)  =  if_p_2_in_5_ga1(x3)
if_p_2_in_6_ga4(x1, x2, x3, x4)  =  if_p_2_in_6_ga1(x4)
if_p_2_in_4_ga5(x1, x2, x3, x4, x5)  =  if_p_2_in_4_ga4(x1, x2, x4, x5)
if_p_2_in_2_ga5(x1, x2, x3, x4, x5)  =  if_p_2_in_2_ga2(x3, x5)
IF_P_2_IN_6_GA4(x1, x2, x3, x4)  =  IF_P_2_IN_6_GA1(x4)
IF_P_2_IN_3_GA5(x1, x2, x3, x4, x5)  =  IF_P_2_IN_3_GA3(x1, x2, x5)
P_2_IN_GA2(x1, x2)  =  P_2_IN_GA1(x1)
IF_P_2_IN_1_GA5(x1, x2, x3, x4, x5)  =  IF_P_2_IN_1_GA2(x2, x5)
IF_P_2_IN_4_GA5(x1, x2, x3, x4, x5)  =  IF_P_2_IN_4_GA4(x1, x2, x4, x5)
IF_P_2_IN_2_GA5(x1, x2, x3, x4, x5)  =  IF_P_2_IN_2_GA2(x3, x5)
IF_P_2_IN_5_GA3(x1, x2, x3)  =  IF_P_2_IN_5_GA1(x3)

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:

P_2_IN_GA2(d_11(e_11(+2(X, Y))), +2(DX, DY)) -> IF_P_2_IN_1_GA5(X, Y, DX, DY, p_2_in_ga2(d_11(e_11(X)), DX))
P_2_IN_GA2(d_11(e_11(+2(X, Y))), +2(DX, DY)) -> P_2_IN_GA2(d_11(e_11(X)), DX)
P_2_IN_GA2(d_11(e_11(*2(X, Y))), +2(*2(X, DY), *2(Y, DX))) -> IF_P_2_IN_3_GA5(X, Y, DY, DX, p_2_in_ga2(d_11(e_11(X)), DX))
P_2_IN_GA2(d_11(e_11(*2(X, Y))), +2(*2(X, DY), *2(Y, DX))) -> P_2_IN_GA2(d_11(e_11(X)), DX)
P_2_IN_GA2(d_11(d_11(X)), DDX) -> IF_P_2_IN_5_GA3(X, DDX, p_2_in_ga2(d_11(X), DX))
P_2_IN_GA2(d_11(d_11(X)), DDX) -> P_2_IN_GA2(d_11(X), DX)
IF_P_2_IN_5_GA3(X, DDX, p_2_out_ga2(d_11(X), DX)) -> IF_P_2_IN_6_GA4(X, DDX, DX, p_2_in_ga2(d_11(e_11(DX)), DDX))
IF_P_2_IN_5_GA3(X, DDX, p_2_out_ga2(d_11(X), DX)) -> P_2_IN_GA2(d_11(e_11(DX)), DDX)
IF_P_2_IN_3_GA5(X, Y, DY, DX, p_2_out_ga2(d_11(e_11(X)), DX)) -> IF_P_2_IN_4_GA5(X, Y, DY, DX, p_2_in_ga2(d_11(e_11(Y)), DY))
IF_P_2_IN_3_GA5(X, Y, DY, DX, p_2_out_ga2(d_11(e_11(X)), DX)) -> P_2_IN_GA2(d_11(e_11(Y)), DY)
IF_P_2_IN_1_GA5(X, Y, DX, DY, p_2_out_ga2(d_11(e_11(X)), DX)) -> IF_P_2_IN_2_GA5(X, Y, DX, DY, p_2_in_ga2(d_11(e_11(Y)), DY))
IF_P_2_IN_1_GA5(X, Y, DX, DY, p_2_out_ga2(d_11(e_11(X)), DX)) -> P_2_IN_GA2(d_11(e_11(Y)), DY)

The TRS R consists of the following rules:

p_2_in_ga2(d_11(e_11(t_0)), const_11(1_0)) -> p_2_out_ga2(d_11(e_11(t_0)), const_11(1_0))
p_2_in_ga2(d_11(e_11(const_11(A))), const_11(0_0)) -> p_2_out_ga2(d_11(e_11(const_11(A))), const_11(0_0))
p_2_in_ga2(d_11(e_11(+2(X, Y))), +2(DX, DY)) -> if_p_2_in_1_ga5(X, Y, DX, DY, p_2_in_ga2(d_11(e_11(X)), DX))
p_2_in_ga2(d_11(e_11(*2(X, Y))), +2(*2(X, DY), *2(Y, DX))) -> if_p_2_in_3_ga5(X, Y, DY, DX, p_2_in_ga2(d_11(e_11(X)), DX))
p_2_in_ga2(d_11(d_11(X)), DDX) -> if_p_2_in_5_ga3(X, DDX, p_2_in_ga2(d_11(X), DX))
if_p_2_in_5_ga3(X, DDX, p_2_out_ga2(d_11(X), DX)) -> if_p_2_in_6_ga4(X, DDX, DX, p_2_in_ga2(d_11(e_11(DX)), DDX))
if_p_2_in_6_ga4(X, DDX, DX, p_2_out_ga2(d_11(e_11(DX)), DDX)) -> p_2_out_ga2(d_11(d_11(X)), DDX)
if_p_2_in_3_ga5(X, Y, DY, DX, p_2_out_ga2(d_11(e_11(X)), DX)) -> if_p_2_in_4_ga5(X, Y, DY, DX, p_2_in_ga2(d_11(e_11(Y)), DY))
if_p_2_in_4_ga5(X, Y, DY, DX, p_2_out_ga2(d_11(e_11(Y)), DY)) -> p_2_out_ga2(d_11(e_11(*2(X, Y))), +2(*2(X, DY), *2(Y, DX)))
if_p_2_in_1_ga5(X, Y, DX, DY, p_2_out_ga2(d_11(e_11(X)), DX)) -> if_p_2_in_2_ga5(X, Y, DX, DY, p_2_in_ga2(d_11(e_11(Y)), DY))
if_p_2_in_2_ga5(X, Y, DX, DY, p_2_out_ga2(d_11(e_11(Y)), DY)) -> p_2_out_ga2(d_11(e_11(+2(X, Y))), +2(DX, DY))

The argument filtering Pi contains the following mapping:
p_2_in_ga2(x1, x2)  =  p_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)
p_2_out_ga2(x1, x2)  =  p_2_out_ga1(x2)
if_p_2_in_1_ga5(x1, x2, x3, x4, x5)  =  if_p_2_in_1_ga2(x2, x5)
if_p_2_in_3_ga5(x1, x2, x3, x4, x5)  =  if_p_2_in_3_ga3(x1, x2, x5)
if_p_2_in_5_ga3(x1, x2, x3)  =  if_p_2_in_5_ga1(x3)
if_p_2_in_6_ga4(x1, x2, x3, x4)  =  if_p_2_in_6_ga1(x4)
if_p_2_in_4_ga5(x1, x2, x3, x4, x5)  =  if_p_2_in_4_ga4(x1, x2, x4, x5)
if_p_2_in_2_ga5(x1, x2, x3, x4, x5)  =  if_p_2_in_2_ga2(x3, x5)
IF_P_2_IN_6_GA4(x1, x2, x3, x4)  =  IF_P_2_IN_6_GA1(x4)
IF_P_2_IN_3_GA5(x1, x2, x3, x4, x5)  =  IF_P_2_IN_3_GA3(x1, x2, x5)
P_2_IN_GA2(x1, x2)  =  P_2_IN_GA1(x1)
IF_P_2_IN_1_GA5(x1, x2, x3, x4, x5)  =  IF_P_2_IN_1_GA2(x2, x5)
IF_P_2_IN_4_GA5(x1, x2, x3, x4, x5)  =  IF_P_2_IN_4_GA4(x1, x2, x4, x5)
IF_P_2_IN_2_GA5(x1, x2, x3, x4, x5)  =  IF_P_2_IN_2_GA2(x3, x5)
IF_P_2_IN_5_GA3(x1, x2, x3)  =  IF_P_2_IN_5_GA1(x3)

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_P_2_IN_3_GA5(X, Y, DY, DX, p_2_out_ga2(d_11(e_11(X)), DX)) -> P_2_IN_GA2(d_11(e_11(Y)), DY)
P_2_IN_GA2(d_11(e_11(+2(X, Y))), +2(DX, DY)) -> IF_P_2_IN_1_GA5(X, Y, DX, DY, p_2_in_ga2(d_11(e_11(X)), DX))
P_2_IN_GA2(d_11(e_11(+2(X, Y))), +2(DX, DY)) -> P_2_IN_GA2(d_11(e_11(X)), DX)
P_2_IN_GA2(d_11(e_11(*2(X, Y))), +2(*2(X, DY), *2(Y, DX))) -> P_2_IN_GA2(d_11(e_11(X)), DX)
P_2_IN_GA2(d_11(e_11(*2(X, Y))), +2(*2(X, DY), *2(Y, DX))) -> IF_P_2_IN_3_GA5(X, Y, DY, DX, p_2_in_ga2(d_11(e_11(X)), DX))
IF_P_2_IN_1_GA5(X, Y, DX, DY, p_2_out_ga2(d_11(e_11(X)), DX)) -> P_2_IN_GA2(d_11(e_11(Y)), DY)

The TRS R consists of the following rules:

p_2_in_ga2(d_11(e_11(t_0)), const_11(1_0)) -> p_2_out_ga2(d_11(e_11(t_0)), const_11(1_0))
p_2_in_ga2(d_11(e_11(const_11(A))), const_11(0_0)) -> p_2_out_ga2(d_11(e_11(const_11(A))), const_11(0_0))
p_2_in_ga2(d_11(e_11(+2(X, Y))), +2(DX, DY)) -> if_p_2_in_1_ga5(X, Y, DX, DY, p_2_in_ga2(d_11(e_11(X)), DX))
p_2_in_ga2(d_11(e_11(*2(X, Y))), +2(*2(X, DY), *2(Y, DX))) -> if_p_2_in_3_ga5(X, Y, DY, DX, p_2_in_ga2(d_11(e_11(X)), DX))
p_2_in_ga2(d_11(d_11(X)), DDX) -> if_p_2_in_5_ga3(X, DDX, p_2_in_ga2(d_11(X), DX))
if_p_2_in_5_ga3(X, DDX, p_2_out_ga2(d_11(X), DX)) -> if_p_2_in_6_ga4(X, DDX, DX, p_2_in_ga2(d_11(e_11(DX)), DDX))
if_p_2_in_6_ga4(X, DDX, DX, p_2_out_ga2(d_11(e_11(DX)), DDX)) -> p_2_out_ga2(d_11(d_11(X)), DDX)
if_p_2_in_3_ga5(X, Y, DY, DX, p_2_out_ga2(d_11(e_11(X)), DX)) -> if_p_2_in_4_ga5(X, Y, DY, DX, p_2_in_ga2(d_11(e_11(Y)), DY))
if_p_2_in_4_ga5(X, Y, DY, DX, p_2_out_ga2(d_11(e_11(Y)), DY)) -> p_2_out_ga2(d_11(e_11(*2(X, Y))), +2(*2(X, DY), *2(Y, DX)))
if_p_2_in_1_ga5(X, Y, DX, DY, p_2_out_ga2(d_11(e_11(X)), DX)) -> if_p_2_in_2_ga5(X, Y, DX, DY, p_2_in_ga2(d_11(e_11(Y)), DY))
if_p_2_in_2_ga5(X, Y, DX, DY, p_2_out_ga2(d_11(e_11(Y)), DY)) -> p_2_out_ga2(d_11(e_11(+2(X, Y))), +2(DX, DY))

The argument filtering Pi contains the following mapping:
p_2_in_ga2(x1, x2)  =  p_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)
p_2_out_ga2(x1, x2)  =  p_2_out_ga1(x2)
if_p_2_in_1_ga5(x1, x2, x3, x4, x5)  =  if_p_2_in_1_ga2(x2, x5)
if_p_2_in_3_ga5(x1, x2, x3, x4, x5)  =  if_p_2_in_3_ga3(x1, x2, x5)
if_p_2_in_5_ga3(x1, x2, x3)  =  if_p_2_in_5_ga1(x3)
if_p_2_in_6_ga4(x1, x2, x3, x4)  =  if_p_2_in_6_ga1(x4)
if_p_2_in_4_ga5(x1, x2, x3, x4, x5)  =  if_p_2_in_4_ga4(x1, x2, x4, x5)
if_p_2_in_2_ga5(x1, x2, x3, x4, x5)  =  if_p_2_in_2_ga2(x3, x5)
IF_P_2_IN_3_GA5(x1, x2, x3, x4, x5)  =  IF_P_2_IN_3_GA3(x1, x2, x5)
P_2_IN_GA2(x1, x2)  =  P_2_IN_GA1(x1)
IF_P_2_IN_1_GA5(x1, x2, x3, x4, x5)  =  IF_P_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_P_2_IN_3_GA5(X, Y, DY, DX, p_2_out_ga2(d_11(e_11(X)), DX)) -> P_2_IN_GA2(d_11(e_11(Y)), DY)
P_2_IN_GA2(d_11(e_11(+2(X, Y))), +2(DX, DY)) -> IF_P_2_IN_1_GA5(X, Y, DX, DY, p_2_in_ga2(d_11(e_11(X)), DX))
P_2_IN_GA2(d_11(e_11(+2(X, Y))), +2(DX, DY)) -> P_2_IN_GA2(d_11(e_11(X)), DX)
P_2_IN_GA2(d_11(e_11(*2(X, Y))), +2(*2(X, DY), *2(Y, DX))) -> P_2_IN_GA2(d_11(e_11(X)), DX)
P_2_IN_GA2(d_11(e_11(*2(X, Y))), +2(*2(X, DY), *2(Y, DX))) -> IF_P_2_IN_3_GA5(X, Y, DY, DX, p_2_in_ga2(d_11(e_11(X)), DX))
IF_P_2_IN_1_GA5(X, Y, DX, DY, p_2_out_ga2(d_11(e_11(X)), DX)) -> P_2_IN_GA2(d_11(e_11(Y)), DY)

The TRS R consists of the following rules:

p_2_in_ga2(d_11(e_11(t_0)), const_11(1_0)) -> p_2_out_ga2(d_11(e_11(t_0)), const_11(1_0))
p_2_in_ga2(d_11(e_11(const_11(A))), const_11(0_0)) -> p_2_out_ga2(d_11(e_11(const_11(A))), const_11(0_0))
p_2_in_ga2(d_11(e_11(+2(X, Y))), +2(DX, DY)) -> if_p_2_in_1_ga5(X, Y, DX, DY, p_2_in_ga2(d_11(e_11(X)), DX))
p_2_in_ga2(d_11(e_11(*2(X, Y))), +2(*2(X, DY), *2(Y, DX))) -> if_p_2_in_3_ga5(X, Y, DY, DX, p_2_in_ga2(d_11(e_11(X)), DX))
if_p_2_in_1_ga5(X, Y, DX, DY, p_2_out_ga2(d_11(e_11(X)), DX)) -> if_p_2_in_2_ga5(X, Y, DX, DY, p_2_in_ga2(d_11(e_11(Y)), DY))
if_p_2_in_3_ga5(X, Y, DY, DX, p_2_out_ga2(d_11(e_11(X)), DX)) -> if_p_2_in_4_ga5(X, Y, DY, DX, p_2_in_ga2(d_11(e_11(Y)), DY))
if_p_2_in_2_ga5(X, Y, DX, DY, p_2_out_ga2(d_11(e_11(Y)), DY)) -> p_2_out_ga2(d_11(e_11(+2(X, Y))), +2(DX, DY))
if_p_2_in_4_ga5(X, Y, DY, DX, p_2_out_ga2(d_11(e_11(Y)), DY)) -> p_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:
p_2_in_ga2(x1, x2)  =  p_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)
p_2_out_ga2(x1, x2)  =  p_2_out_ga1(x2)
if_p_2_in_1_ga5(x1, x2, x3, x4, x5)  =  if_p_2_in_1_ga2(x2, x5)
if_p_2_in_3_ga5(x1, x2, x3, x4, x5)  =  if_p_2_in_3_ga3(x1, x2, x5)
if_p_2_in_4_ga5(x1, x2, x3, x4, x5)  =  if_p_2_in_4_ga4(x1, x2, x4, x5)
if_p_2_in_2_ga5(x1, x2, x3, x4, x5)  =  if_p_2_in_2_ga2(x3, x5)
IF_P_2_IN_3_GA5(x1, x2, x3, x4, x5)  =  IF_P_2_IN_3_GA3(x1, x2, x5)
P_2_IN_GA2(x1, x2)  =  P_2_IN_GA1(x1)
IF_P_2_IN_1_GA5(x1, x2, x3, x4, x5)  =  IF_P_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_P_2_IN_3_GA3(X, Y, p_2_out_ga1(DX)) -> P_2_IN_GA1(d_11(e_11(Y)))
P_2_IN_GA1(d_11(e_11(+2(X, Y)))) -> IF_P_2_IN_1_GA2(Y, p_2_in_ga1(d_11(e_11(X))))
P_2_IN_GA1(d_11(e_11(+2(X, Y)))) -> P_2_IN_GA1(d_11(e_11(X)))
P_2_IN_GA1(d_11(e_11(*2(X, Y)))) -> P_2_IN_GA1(d_11(e_11(X)))
P_2_IN_GA1(d_11(e_11(*2(X, Y)))) -> IF_P_2_IN_3_GA3(X, Y, p_2_in_ga1(d_11(e_11(X))))
IF_P_2_IN_1_GA2(Y, p_2_out_ga1(DX)) -> P_2_IN_GA1(d_11(e_11(Y)))

The TRS R consists of the following rules:

p_2_in_ga1(d_11(e_11(t_0))) -> p_2_out_ga1(const_11(1_0))
p_2_in_ga1(d_11(e_11(const_11(A)))) -> p_2_out_ga1(const_11(0_0))
p_2_in_ga1(d_11(e_11(+2(X, Y)))) -> if_p_2_in_1_ga2(Y, p_2_in_ga1(d_11(e_11(X))))
p_2_in_ga1(d_11(e_11(*2(X, Y)))) -> if_p_2_in_3_ga3(X, Y, p_2_in_ga1(d_11(e_11(X))))
if_p_2_in_1_ga2(Y, p_2_out_ga1(DX)) -> if_p_2_in_2_ga2(DX, p_2_in_ga1(d_11(e_11(Y))))
if_p_2_in_3_ga3(X, Y, p_2_out_ga1(DX)) -> if_p_2_in_4_ga4(X, Y, DX, p_2_in_ga1(d_11(e_11(Y))))
if_p_2_in_2_ga2(DX, p_2_out_ga1(DY)) -> p_2_out_ga1(+2(DX, DY))
if_p_2_in_4_ga4(X, Y, DX, p_2_out_ga1(DY)) -> p_2_out_ga1(+2(*2(X, DY), *2(Y, DX)))

The set Q consists of the following terms:

p_2_in_ga1(x0)
if_p_2_in_1_ga2(x0, x1)
if_p_2_in_3_ga3(x0, x1, x2)
if_p_2_in_2_ga2(x0, x1)
if_p_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 {P_2_IN_GA1, IF_P_2_IN_3_GA3, IF_P_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
e_11(x1)  =  x1
p_2_out_ga1(x1)  =  p_2_out_ga
*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:

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

The TRS R consists of the following rules:

p_2_in_ga2(d_11(e_11(t_0)), const_11(1_0)) -> p_2_out_ga2(d_11(e_11(t_0)), const_11(1_0))
p_2_in_ga2(d_11(e_11(const_11(A))), const_11(0_0)) -> p_2_out_ga2(d_11(e_11(const_11(A))), const_11(0_0))
p_2_in_ga2(d_11(e_11(+2(X, Y))), +2(DX, DY)) -> if_p_2_in_1_ga5(X, Y, DX, DY, p_2_in_ga2(d_11(e_11(X)), DX))
p_2_in_ga2(d_11(e_11(*2(X, Y))), +2(*2(X, DY), *2(Y, DX))) -> if_p_2_in_3_ga5(X, Y, DY, DX, p_2_in_ga2(d_11(e_11(X)), DX))
p_2_in_ga2(d_11(d_11(X)), DDX) -> if_p_2_in_5_ga3(X, DDX, p_2_in_ga2(d_11(X), DX))
if_p_2_in_5_ga3(X, DDX, p_2_out_ga2(d_11(X), DX)) -> if_p_2_in_6_ga4(X, DDX, DX, p_2_in_ga2(d_11(e_11(DX)), DDX))
if_p_2_in_6_ga4(X, DDX, DX, p_2_out_ga2(d_11(e_11(DX)), DDX)) -> p_2_out_ga2(d_11(d_11(X)), DDX)
if_p_2_in_3_ga5(X, Y, DY, DX, p_2_out_ga2(d_11(e_11(X)), DX)) -> if_p_2_in_4_ga5(X, Y, DY, DX, p_2_in_ga2(d_11(e_11(Y)), DY))
if_p_2_in_4_ga5(X, Y, DY, DX, p_2_out_ga2(d_11(e_11(Y)), DY)) -> p_2_out_ga2(d_11(e_11(*2(X, Y))), +2(*2(X, DY), *2(Y, DX)))
if_p_2_in_1_ga5(X, Y, DX, DY, p_2_out_ga2(d_11(e_11(X)), DX)) -> if_p_2_in_2_ga5(X, Y, DX, DY, p_2_in_ga2(d_11(e_11(Y)), DY))
if_p_2_in_2_ga5(X, Y, DX, DY, p_2_out_ga2(d_11(e_11(Y)), DY)) -> p_2_out_ga2(d_11(e_11(+2(X, Y))), +2(DX, DY))

The argument filtering Pi contains the following mapping:
p_2_in_ga2(x1, x2)  =  p_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)
p_2_out_ga2(x1, x2)  =  p_2_out_ga1(x2)
if_p_2_in_1_ga5(x1, x2, x3, x4, x5)  =  if_p_2_in_1_ga2(x2, x5)
if_p_2_in_3_ga5(x1, x2, x3, x4, x5)  =  if_p_2_in_3_ga3(x1, x2, x5)
if_p_2_in_5_ga3(x1, x2, x3)  =  if_p_2_in_5_ga1(x3)
if_p_2_in_6_ga4(x1, x2, x3, x4)  =  if_p_2_in_6_ga1(x4)
if_p_2_in_4_ga5(x1, x2, x3, x4, x5)  =  if_p_2_in_4_ga4(x1, x2, x4, x5)
if_p_2_in_2_ga5(x1, x2, x3, x4, x5)  =  if_p_2_in_2_ga2(x3, x5)
P_2_IN_GA2(x1, x2)  =  P_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:

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

R is empty.
The argument filtering Pi contains the following mapping:
d_11(x1)  =  d_11(x1)
P_2_IN_GA2(x1, x2)  =  P_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:

P_2_IN_GA1(d_11(d_11(X))) -> P_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 {P_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: