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



↳ PROLOG
  ↳ UnrequestedClauseRemoverProof

conf1(X) :- del22(X, Z), del3(U, Y, Z), conf1(Y).
del22(X, Y) :- del3(U, X, Z), del3(V, Z, Y).
del3(X, .2(X, T), T).
del3(X, .2(H, T), .2(H, T1)) :- del3(X, T, T1).
s2l2(s1(X), .2(Y, Xs)) :- s2l2(X, Xs).
s2l2(00, {}0).
goal1(X) :- s2l2(X, XS), conf1(XS).


The clauses

s2l2(s1(X), .2(Y, Xs)) :- s2l2(X, Xs).
s2l2(00, {}0).
goal1(X) :- s2l2(X, XS), conf1(XS).

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

Deleting these clauses results in the following prolog program:

conf1(X) :- del22(X, Z), del3(U, Y, Z), conf1(Y).
del22(X, Y) :- del3(U, X, Z), del3(V, Z, Y).
del3(X, .2(X, T), T).
del3(X, .2(H, T), .2(H, T1)) :- del3(X, T, T1).



↳ PROLOG
  ↳ UnrequestedClauseRemoverProof
    ↳ PROLOG
      ↳ PrologToPiTRSProof

conf1(X) :- del22(X, Z), del3(U, Y, Z), conf1(Y).
del22(X, Y) :- del3(U, X, Z), del3(V, Z, Y).
del3(X, .2(X, T), T).
del3(X, .2(H, T), .2(H, T1)) :- del3(X, T, T1).


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


conf_1_in_g1(X) -> if_conf_1_in_1_g2(X, del2_2_in_ga2(X, Z))
del2_2_in_ga2(X, Y) -> if_del2_2_in_1_ga3(X, Y, del_3_in_aga3(U, X, Z))
del_3_in_aga3(X, ._22(X, T), T) -> del_3_out_aga3(X, ._22(X, T), T)
del_3_in_aga3(X, ._22(H, T), ._22(H, T1)) -> if_del_3_in_1_aga5(X, H, T, T1, del_3_in_aga3(X, T, T1))
if_del_3_in_1_aga5(X, H, T, T1, del_3_out_aga3(X, T, T1)) -> del_3_out_aga3(X, ._22(H, T), ._22(H, T1))
if_del2_2_in_1_ga3(X, Y, del_3_out_aga3(U, X, Z)) -> if_del2_2_in_2_ga4(X, Y, Z, del_3_in_aga3(V, Z, Y))
if_del2_2_in_2_ga4(X, Y, Z, del_3_out_aga3(V, Z, Y)) -> del2_2_out_ga2(X, Y)
if_conf_1_in_1_g2(X, del2_2_out_ga2(X, Z)) -> if_conf_1_in_2_g3(X, Z, del_3_in_aag3(U, Y, Z))
del_3_in_aag3(X, ._22(X, T), T) -> del_3_out_aag3(X, ._22(X, T), T)
del_3_in_aag3(X, ._22(H, T), ._22(H, T1)) -> if_del_3_in_1_aag5(X, H, T, T1, del_3_in_aag3(X, T, T1))
if_del_3_in_1_aag5(X, H, T, T1, del_3_out_aag3(X, T, T1)) -> del_3_out_aag3(X, ._22(H, T), ._22(H, T1))
if_conf_1_in_2_g3(X, Z, del_3_out_aag3(U, Y, Z)) -> if_conf_1_in_3_g3(X, Y, conf_1_in_g1(Y))
if_conf_1_in_3_g3(X, Y, conf_1_out_g1(Y)) -> conf_1_out_g1(X)

The argument filtering Pi contains the following mapping:
conf_1_in_g1(x1)  =  conf_1_in_g1(x1)
._22(x1, x2)  =  ._21(x2)
if_conf_1_in_1_g2(x1, x2)  =  if_conf_1_in_1_g1(x2)
del2_2_in_ga2(x1, x2)  =  del2_2_in_ga1(x1)
if_del2_2_in_1_ga3(x1, x2, x3)  =  if_del2_2_in_1_ga1(x3)
del_3_in_aga3(x1, x2, x3)  =  del_3_in_aga1(x2)
del_3_out_aga3(x1, x2, x3)  =  del_3_out_aga1(x3)
if_del_3_in_1_aga5(x1, x2, x3, x4, x5)  =  if_del_3_in_1_aga1(x5)
if_del2_2_in_2_ga4(x1, x2, x3, x4)  =  if_del2_2_in_2_ga1(x4)
del2_2_out_ga2(x1, x2)  =  del2_2_out_ga1(x2)
if_conf_1_in_2_g3(x1, x2, x3)  =  if_conf_1_in_2_g1(x3)
del_3_in_aag3(x1, x2, x3)  =  del_3_in_aag1(x3)
del_3_out_aag3(x1, x2, x3)  =  del_3_out_aag1(x2)
if_del_3_in_1_aag5(x1, x2, x3, x4, x5)  =  if_del_3_in_1_aag1(x5)
if_conf_1_in_3_g3(x1, x2, x3)  =  if_conf_1_in_3_g1(x3)
conf_1_out_g1(x1)  =  conf_1_out_g

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:

conf_1_in_g1(X) -> if_conf_1_in_1_g2(X, del2_2_in_ga2(X, Z))
del2_2_in_ga2(X, Y) -> if_del2_2_in_1_ga3(X, Y, del_3_in_aga3(U, X, Z))
del_3_in_aga3(X, ._22(X, T), T) -> del_3_out_aga3(X, ._22(X, T), T)
del_3_in_aga3(X, ._22(H, T), ._22(H, T1)) -> if_del_3_in_1_aga5(X, H, T, T1, del_3_in_aga3(X, T, T1))
if_del_3_in_1_aga5(X, H, T, T1, del_3_out_aga3(X, T, T1)) -> del_3_out_aga3(X, ._22(H, T), ._22(H, T1))
if_del2_2_in_1_ga3(X, Y, del_3_out_aga3(U, X, Z)) -> if_del2_2_in_2_ga4(X, Y, Z, del_3_in_aga3(V, Z, Y))
if_del2_2_in_2_ga4(X, Y, Z, del_3_out_aga3(V, Z, Y)) -> del2_2_out_ga2(X, Y)
if_conf_1_in_1_g2(X, del2_2_out_ga2(X, Z)) -> if_conf_1_in_2_g3(X, Z, del_3_in_aag3(U, Y, Z))
del_3_in_aag3(X, ._22(X, T), T) -> del_3_out_aag3(X, ._22(X, T), T)
del_3_in_aag3(X, ._22(H, T), ._22(H, T1)) -> if_del_3_in_1_aag5(X, H, T, T1, del_3_in_aag3(X, T, T1))
if_del_3_in_1_aag5(X, H, T, T1, del_3_out_aag3(X, T, T1)) -> del_3_out_aag3(X, ._22(H, T), ._22(H, T1))
if_conf_1_in_2_g3(X, Z, del_3_out_aag3(U, Y, Z)) -> if_conf_1_in_3_g3(X, Y, conf_1_in_g1(Y))
if_conf_1_in_3_g3(X, Y, conf_1_out_g1(Y)) -> conf_1_out_g1(X)

The argument filtering Pi contains the following mapping:
conf_1_in_g1(x1)  =  conf_1_in_g1(x1)
._22(x1, x2)  =  ._21(x2)
if_conf_1_in_1_g2(x1, x2)  =  if_conf_1_in_1_g1(x2)
del2_2_in_ga2(x1, x2)  =  del2_2_in_ga1(x1)
if_del2_2_in_1_ga3(x1, x2, x3)  =  if_del2_2_in_1_ga1(x3)
del_3_in_aga3(x1, x2, x3)  =  del_3_in_aga1(x2)
del_3_out_aga3(x1, x2, x3)  =  del_3_out_aga1(x3)
if_del_3_in_1_aga5(x1, x2, x3, x4, x5)  =  if_del_3_in_1_aga1(x5)
if_del2_2_in_2_ga4(x1, x2, x3, x4)  =  if_del2_2_in_2_ga1(x4)
del2_2_out_ga2(x1, x2)  =  del2_2_out_ga1(x2)
if_conf_1_in_2_g3(x1, x2, x3)  =  if_conf_1_in_2_g1(x3)
del_3_in_aag3(x1, x2, x3)  =  del_3_in_aag1(x3)
del_3_out_aag3(x1, x2, x3)  =  del_3_out_aag1(x2)
if_del_3_in_1_aag5(x1, x2, x3, x4, x5)  =  if_del_3_in_1_aag1(x5)
if_conf_1_in_3_g3(x1, x2, x3)  =  if_conf_1_in_3_g1(x3)
conf_1_out_g1(x1)  =  conf_1_out_g


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

CONF_1_IN_G1(X) -> IF_CONF_1_IN_1_G2(X, del2_2_in_ga2(X, Z))
CONF_1_IN_G1(X) -> DEL2_2_IN_GA2(X, Z)
DEL2_2_IN_GA2(X, Y) -> IF_DEL2_2_IN_1_GA3(X, Y, del_3_in_aga3(U, X, Z))
DEL2_2_IN_GA2(X, Y) -> DEL_3_IN_AGA3(U, X, Z)
DEL_3_IN_AGA3(X, ._22(H, T), ._22(H, T1)) -> IF_DEL_3_IN_1_AGA5(X, H, T, T1, del_3_in_aga3(X, T, T1))
DEL_3_IN_AGA3(X, ._22(H, T), ._22(H, T1)) -> DEL_3_IN_AGA3(X, T, T1)
IF_DEL2_2_IN_1_GA3(X, Y, del_3_out_aga3(U, X, Z)) -> IF_DEL2_2_IN_2_GA4(X, Y, Z, del_3_in_aga3(V, Z, Y))
IF_DEL2_2_IN_1_GA3(X, Y, del_3_out_aga3(U, X, Z)) -> DEL_3_IN_AGA3(V, Z, Y)
IF_CONF_1_IN_1_G2(X, del2_2_out_ga2(X, Z)) -> IF_CONF_1_IN_2_G3(X, Z, del_3_in_aag3(U, Y, Z))
IF_CONF_1_IN_1_G2(X, del2_2_out_ga2(X, Z)) -> DEL_3_IN_AAG3(U, Y, Z)
DEL_3_IN_AAG3(X, ._22(H, T), ._22(H, T1)) -> IF_DEL_3_IN_1_AAG5(X, H, T, T1, del_3_in_aag3(X, T, T1))
DEL_3_IN_AAG3(X, ._22(H, T), ._22(H, T1)) -> DEL_3_IN_AAG3(X, T, T1)
IF_CONF_1_IN_2_G3(X, Z, del_3_out_aag3(U, Y, Z)) -> IF_CONF_1_IN_3_G3(X, Y, conf_1_in_g1(Y))
IF_CONF_1_IN_2_G3(X, Z, del_3_out_aag3(U, Y, Z)) -> CONF_1_IN_G1(Y)

The TRS R consists of the following rules:

conf_1_in_g1(X) -> if_conf_1_in_1_g2(X, del2_2_in_ga2(X, Z))
del2_2_in_ga2(X, Y) -> if_del2_2_in_1_ga3(X, Y, del_3_in_aga3(U, X, Z))
del_3_in_aga3(X, ._22(X, T), T) -> del_3_out_aga3(X, ._22(X, T), T)
del_3_in_aga3(X, ._22(H, T), ._22(H, T1)) -> if_del_3_in_1_aga5(X, H, T, T1, del_3_in_aga3(X, T, T1))
if_del_3_in_1_aga5(X, H, T, T1, del_3_out_aga3(X, T, T1)) -> del_3_out_aga3(X, ._22(H, T), ._22(H, T1))
if_del2_2_in_1_ga3(X, Y, del_3_out_aga3(U, X, Z)) -> if_del2_2_in_2_ga4(X, Y, Z, del_3_in_aga3(V, Z, Y))
if_del2_2_in_2_ga4(X, Y, Z, del_3_out_aga3(V, Z, Y)) -> del2_2_out_ga2(X, Y)
if_conf_1_in_1_g2(X, del2_2_out_ga2(X, Z)) -> if_conf_1_in_2_g3(X, Z, del_3_in_aag3(U, Y, Z))
del_3_in_aag3(X, ._22(X, T), T) -> del_3_out_aag3(X, ._22(X, T), T)
del_3_in_aag3(X, ._22(H, T), ._22(H, T1)) -> if_del_3_in_1_aag5(X, H, T, T1, del_3_in_aag3(X, T, T1))
if_del_3_in_1_aag5(X, H, T, T1, del_3_out_aag3(X, T, T1)) -> del_3_out_aag3(X, ._22(H, T), ._22(H, T1))
if_conf_1_in_2_g3(X, Z, del_3_out_aag3(U, Y, Z)) -> if_conf_1_in_3_g3(X, Y, conf_1_in_g1(Y))
if_conf_1_in_3_g3(X, Y, conf_1_out_g1(Y)) -> conf_1_out_g1(X)

The argument filtering Pi contains the following mapping:
conf_1_in_g1(x1)  =  conf_1_in_g1(x1)
._22(x1, x2)  =  ._21(x2)
if_conf_1_in_1_g2(x1, x2)  =  if_conf_1_in_1_g1(x2)
del2_2_in_ga2(x1, x2)  =  del2_2_in_ga1(x1)
if_del2_2_in_1_ga3(x1, x2, x3)  =  if_del2_2_in_1_ga1(x3)
del_3_in_aga3(x1, x2, x3)  =  del_3_in_aga1(x2)
del_3_out_aga3(x1, x2, x3)  =  del_3_out_aga1(x3)
if_del_3_in_1_aga5(x1, x2, x3, x4, x5)  =  if_del_3_in_1_aga1(x5)
if_del2_2_in_2_ga4(x1, x2, x3, x4)  =  if_del2_2_in_2_ga1(x4)
del2_2_out_ga2(x1, x2)  =  del2_2_out_ga1(x2)
if_conf_1_in_2_g3(x1, x2, x3)  =  if_conf_1_in_2_g1(x3)
del_3_in_aag3(x1, x2, x3)  =  del_3_in_aag1(x3)
del_3_out_aag3(x1, x2, x3)  =  del_3_out_aag1(x2)
if_del_3_in_1_aag5(x1, x2, x3, x4, x5)  =  if_del_3_in_1_aag1(x5)
if_conf_1_in_3_g3(x1, x2, x3)  =  if_conf_1_in_3_g1(x3)
conf_1_out_g1(x1)  =  conf_1_out_g
DEL_3_IN_AAG3(x1, x2, x3)  =  DEL_3_IN_AAG1(x3)
IF_DEL_3_IN_1_AGA5(x1, x2, x3, x4, x5)  =  IF_DEL_3_IN_1_AGA1(x5)
IF_DEL2_2_IN_1_GA3(x1, x2, x3)  =  IF_DEL2_2_IN_1_GA1(x3)
IF_CONF_1_IN_1_G2(x1, x2)  =  IF_CONF_1_IN_1_G1(x2)
DEL_3_IN_AGA3(x1, x2, x3)  =  DEL_3_IN_AGA1(x2)
IF_CONF_1_IN_3_G3(x1, x2, x3)  =  IF_CONF_1_IN_3_G1(x3)
IF_CONF_1_IN_2_G3(x1, x2, x3)  =  IF_CONF_1_IN_2_G1(x3)
CONF_1_IN_G1(x1)  =  CONF_1_IN_G1(x1)
DEL2_2_IN_GA2(x1, x2)  =  DEL2_2_IN_GA1(x1)
IF_DEL_3_IN_1_AAG5(x1, x2, x3, x4, x5)  =  IF_DEL_3_IN_1_AAG1(x5)
IF_DEL2_2_IN_2_GA4(x1, x2, x3, x4)  =  IF_DEL2_2_IN_2_GA1(x4)

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:

CONF_1_IN_G1(X) -> IF_CONF_1_IN_1_G2(X, del2_2_in_ga2(X, Z))
CONF_1_IN_G1(X) -> DEL2_2_IN_GA2(X, Z)
DEL2_2_IN_GA2(X, Y) -> IF_DEL2_2_IN_1_GA3(X, Y, del_3_in_aga3(U, X, Z))
DEL2_2_IN_GA2(X, Y) -> DEL_3_IN_AGA3(U, X, Z)
DEL_3_IN_AGA3(X, ._22(H, T), ._22(H, T1)) -> IF_DEL_3_IN_1_AGA5(X, H, T, T1, del_3_in_aga3(X, T, T1))
DEL_3_IN_AGA3(X, ._22(H, T), ._22(H, T1)) -> DEL_3_IN_AGA3(X, T, T1)
IF_DEL2_2_IN_1_GA3(X, Y, del_3_out_aga3(U, X, Z)) -> IF_DEL2_2_IN_2_GA4(X, Y, Z, del_3_in_aga3(V, Z, Y))
IF_DEL2_2_IN_1_GA3(X, Y, del_3_out_aga3(U, X, Z)) -> DEL_3_IN_AGA3(V, Z, Y)
IF_CONF_1_IN_1_G2(X, del2_2_out_ga2(X, Z)) -> IF_CONF_1_IN_2_G3(X, Z, del_3_in_aag3(U, Y, Z))
IF_CONF_1_IN_1_G2(X, del2_2_out_ga2(X, Z)) -> DEL_3_IN_AAG3(U, Y, Z)
DEL_3_IN_AAG3(X, ._22(H, T), ._22(H, T1)) -> IF_DEL_3_IN_1_AAG5(X, H, T, T1, del_3_in_aag3(X, T, T1))
DEL_3_IN_AAG3(X, ._22(H, T), ._22(H, T1)) -> DEL_3_IN_AAG3(X, T, T1)
IF_CONF_1_IN_2_G3(X, Z, del_3_out_aag3(U, Y, Z)) -> IF_CONF_1_IN_3_G3(X, Y, conf_1_in_g1(Y))
IF_CONF_1_IN_2_G3(X, Z, del_3_out_aag3(U, Y, Z)) -> CONF_1_IN_G1(Y)

The TRS R consists of the following rules:

conf_1_in_g1(X) -> if_conf_1_in_1_g2(X, del2_2_in_ga2(X, Z))
del2_2_in_ga2(X, Y) -> if_del2_2_in_1_ga3(X, Y, del_3_in_aga3(U, X, Z))
del_3_in_aga3(X, ._22(X, T), T) -> del_3_out_aga3(X, ._22(X, T), T)
del_3_in_aga3(X, ._22(H, T), ._22(H, T1)) -> if_del_3_in_1_aga5(X, H, T, T1, del_3_in_aga3(X, T, T1))
if_del_3_in_1_aga5(X, H, T, T1, del_3_out_aga3(X, T, T1)) -> del_3_out_aga3(X, ._22(H, T), ._22(H, T1))
if_del2_2_in_1_ga3(X, Y, del_3_out_aga3(U, X, Z)) -> if_del2_2_in_2_ga4(X, Y, Z, del_3_in_aga3(V, Z, Y))
if_del2_2_in_2_ga4(X, Y, Z, del_3_out_aga3(V, Z, Y)) -> del2_2_out_ga2(X, Y)
if_conf_1_in_1_g2(X, del2_2_out_ga2(X, Z)) -> if_conf_1_in_2_g3(X, Z, del_3_in_aag3(U, Y, Z))
del_3_in_aag3(X, ._22(X, T), T) -> del_3_out_aag3(X, ._22(X, T), T)
del_3_in_aag3(X, ._22(H, T), ._22(H, T1)) -> if_del_3_in_1_aag5(X, H, T, T1, del_3_in_aag3(X, T, T1))
if_del_3_in_1_aag5(X, H, T, T1, del_3_out_aag3(X, T, T1)) -> del_3_out_aag3(X, ._22(H, T), ._22(H, T1))
if_conf_1_in_2_g3(X, Z, del_3_out_aag3(U, Y, Z)) -> if_conf_1_in_3_g3(X, Y, conf_1_in_g1(Y))
if_conf_1_in_3_g3(X, Y, conf_1_out_g1(Y)) -> conf_1_out_g1(X)

The argument filtering Pi contains the following mapping:
conf_1_in_g1(x1)  =  conf_1_in_g1(x1)
._22(x1, x2)  =  ._21(x2)
if_conf_1_in_1_g2(x1, x2)  =  if_conf_1_in_1_g1(x2)
del2_2_in_ga2(x1, x2)  =  del2_2_in_ga1(x1)
if_del2_2_in_1_ga3(x1, x2, x3)  =  if_del2_2_in_1_ga1(x3)
del_3_in_aga3(x1, x2, x3)  =  del_3_in_aga1(x2)
del_3_out_aga3(x1, x2, x3)  =  del_3_out_aga1(x3)
if_del_3_in_1_aga5(x1, x2, x3, x4, x5)  =  if_del_3_in_1_aga1(x5)
if_del2_2_in_2_ga4(x1, x2, x3, x4)  =  if_del2_2_in_2_ga1(x4)
del2_2_out_ga2(x1, x2)  =  del2_2_out_ga1(x2)
if_conf_1_in_2_g3(x1, x2, x3)  =  if_conf_1_in_2_g1(x3)
del_3_in_aag3(x1, x2, x3)  =  del_3_in_aag1(x3)
del_3_out_aag3(x1, x2, x3)  =  del_3_out_aag1(x2)
if_del_3_in_1_aag5(x1, x2, x3, x4, x5)  =  if_del_3_in_1_aag1(x5)
if_conf_1_in_3_g3(x1, x2, x3)  =  if_conf_1_in_3_g1(x3)
conf_1_out_g1(x1)  =  conf_1_out_g
DEL_3_IN_AAG3(x1, x2, x3)  =  DEL_3_IN_AAG1(x3)
IF_DEL_3_IN_1_AGA5(x1, x2, x3, x4, x5)  =  IF_DEL_3_IN_1_AGA1(x5)
IF_DEL2_2_IN_1_GA3(x1, x2, x3)  =  IF_DEL2_2_IN_1_GA1(x3)
IF_CONF_1_IN_1_G2(x1, x2)  =  IF_CONF_1_IN_1_G1(x2)
DEL_3_IN_AGA3(x1, x2, x3)  =  DEL_3_IN_AGA1(x2)
IF_CONF_1_IN_3_G3(x1, x2, x3)  =  IF_CONF_1_IN_3_G1(x3)
IF_CONF_1_IN_2_G3(x1, x2, x3)  =  IF_CONF_1_IN_2_G1(x3)
CONF_1_IN_G1(x1)  =  CONF_1_IN_G1(x1)
DEL2_2_IN_GA2(x1, x2)  =  DEL2_2_IN_GA1(x1)
IF_DEL_3_IN_1_AAG5(x1, x2, x3, x4, x5)  =  IF_DEL_3_IN_1_AAG1(x5)
IF_DEL2_2_IN_2_GA4(x1, x2, x3, x4)  =  IF_DEL2_2_IN_2_GA1(x4)

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

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

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

DEL_3_IN_AAG3(X, ._22(H, T), ._22(H, T1)) -> DEL_3_IN_AAG3(X, T, T1)

The TRS R consists of the following rules:

conf_1_in_g1(X) -> if_conf_1_in_1_g2(X, del2_2_in_ga2(X, Z))
del2_2_in_ga2(X, Y) -> if_del2_2_in_1_ga3(X, Y, del_3_in_aga3(U, X, Z))
del_3_in_aga3(X, ._22(X, T), T) -> del_3_out_aga3(X, ._22(X, T), T)
del_3_in_aga3(X, ._22(H, T), ._22(H, T1)) -> if_del_3_in_1_aga5(X, H, T, T1, del_3_in_aga3(X, T, T1))
if_del_3_in_1_aga5(X, H, T, T1, del_3_out_aga3(X, T, T1)) -> del_3_out_aga3(X, ._22(H, T), ._22(H, T1))
if_del2_2_in_1_ga3(X, Y, del_3_out_aga3(U, X, Z)) -> if_del2_2_in_2_ga4(X, Y, Z, del_3_in_aga3(V, Z, Y))
if_del2_2_in_2_ga4(X, Y, Z, del_3_out_aga3(V, Z, Y)) -> del2_2_out_ga2(X, Y)
if_conf_1_in_1_g2(X, del2_2_out_ga2(X, Z)) -> if_conf_1_in_2_g3(X, Z, del_3_in_aag3(U, Y, Z))
del_3_in_aag3(X, ._22(X, T), T) -> del_3_out_aag3(X, ._22(X, T), T)
del_3_in_aag3(X, ._22(H, T), ._22(H, T1)) -> if_del_3_in_1_aag5(X, H, T, T1, del_3_in_aag3(X, T, T1))
if_del_3_in_1_aag5(X, H, T, T1, del_3_out_aag3(X, T, T1)) -> del_3_out_aag3(X, ._22(H, T), ._22(H, T1))
if_conf_1_in_2_g3(X, Z, del_3_out_aag3(U, Y, Z)) -> if_conf_1_in_3_g3(X, Y, conf_1_in_g1(Y))
if_conf_1_in_3_g3(X, Y, conf_1_out_g1(Y)) -> conf_1_out_g1(X)

The argument filtering Pi contains the following mapping:
conf_1_in_g1(x1)  =  conf_1_in_g1(x1)
._22(x1, x2)  =  ._21(x2)
if_conf_1_in_1_g2(x1, x2)  =  if_conf_1_in_1_g1(x2)
del2_2_in_ga2(x1, x2)  =  del2_2_in_ga1(x1)
if_del2_2_in_1_ga3(x1, x2, x3)  =  if_del2_2_in_1_ga1(x3)
del_3_in_aga3(x1, x2, x3)  =  del_3_in_aga1(x2)
del_3_out_aga3(x1, x2, x3)  =  del_3_out_aga1(x3)
if_del_3_in_1_aga5(x1, x2, x3, x4, x5)  =  if_del_3_in_1_aga1(x5)
if_del2_2_in_2_ga4(x1, x2, x3, x4)  =  if_del2_2_in_2_ga1(x4)
del2_2_out_ga2(x1, x2)  =  del2_2_out_ga1(x2)
if_conf_1_in_2_g3(x1, x2, x3)  =  if_conf_1_in_2_g1(x3)
del_3_in_aag3(x1, x2, x3)  =  del_3_in_aag1(x3)
del_3_out_aag3(x1, x2, x3)  =  del_3_out_aag1(x2)
if_del_3_in_1_aag5(x1, x2, x3, x4, x5)  =  if_del_3_in_1_aag1(x5)
if_conf_1_in_3_g3(x1, x2, x3)  =  if_conf_1_in_3_g1(x3)
conf_1_out_g1(x1)  =  conf_1_out_g
DEL_3_IN_AAG3(x1, x2, x3)  =  DEL_3_IN_AAG1(x3)

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

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

DEL_3_IN_AAG3(X, ._22(H, T), ._22(H, T1)) -> DEL_3_IN_AAG3(X, T, T1)

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

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

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

DEL_3_IN_AAG1(._21(T1)) -> DEL_3_IN_AAG1(T1)

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

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

DEL_3_IN_AGA3(X, ._22(H, T), ._22(H, T1)) -> DEL_3_IN_AGA3(X, T, T1)

The TRS R consists of the following rules:

conf_1_in_g1(X) -> if_conf_1_in_1_g2(X, del2_2_in_ga2(X, Z))
del2_2_in_ga2(X, Y) -> if_del2_2_in_1_ga3(X, Y, del_3_in_aga3(U, X, Z))
del_3_in_aga3(X, ._22(X, T), T) -> del_3_out_aga3(X, ._22(X, T), T)
del_3_in_aga3(X, ._22(H, T), ._22(H, T1)) -> if_del_3_in_1_aga5(X, H, T, T1, del_3_in_aga3(X, T, T1))
if_del_3_in_1_aga5(X, H, T, T1, del_3_out_aga3(X, T, T1)) -> del_3_out_aga3(X, ._22(H, T), ._22(H, T1))
if_del2_2_in_1_ga3(X, Y, del_3_out_aga3(U, X, Z)) -> if_del2_2_in_2_ga4(X, Y, Z, del_3_in_aga3(V, Z, Y))
if_del2_2_in_2_ga4(X, Y, Z, del_3_out_aga3(V, Z, Y)) -> del2_2_out_ga2(X, Y)
if_conf_1_in_1_g2(X, del2_2_out_ga2(X, Z)) -> if_conf_1_in_2_g3(X, Z, del_3_in_aag3(U, Y, Z))
del_3_in_aag3(X, ._22(X, T), T) -> del_3_out_aag3(X, ._22(X, T), T)
del_3_in_aag3(X, ._22(H, T), ._22(H, T1)) -> if_del_3_in_1_aag5(X, H, T, T1, del_3_in_aag3(X, T, T1))
if_del_3_in_1_aag5(X, H, T, T1, del_3_out_aag3(X, T, T1)) -> del_3_out_aag3(X, ._22(H, T), ._22(H, T1))
if_conf_1_in_2_g3(X, Z, del_3_out_aag3(U, Y, Z)) -> if_conf_1_in_3_g3(X, Y, conf_1_in_g1(Y))
if_conf_1_in_3_g3(X, Y, conf_1_out_g1(Y)) -> conf_1_out_g1(X)

The argument filtering Pi contains the following mapping:
conf_1_in_g1(x1)  =  conf_1_in_g1(x1)
._22(x1, x2)  =  ._21(x2)
if_conf_1_in_1_g2(x1, x2)  =  if_conf_1_in_1_g1(x2)
del2_2_in_ga2(x1, x2)  =  del2_2_in_ga1(x1)
if_del2_2_in_1_ga3(x1, x2, x3)  =  if_del2_2_in_1_ga1(x3)
del_3_in_aga3(x1, x2, x3)  =  del_3_in_aga1(x2)
del_3_out_aga3(x1, x2, x3)  =  del_3_out_aga1(x3)
if_del_3_in_1_aga5(x1, x2, x3, x4, x5)  =  if_del_3_in_1_aga1(x5)
if_del2_2_in_2_ga4(x1, x2, x3, x4)  =  if_del2_2_in_2_ga1(x4)
del2_2_out_ga2(x1, x2)  =  del2_2_out_ga1(x2)
if_conf_1_in_2_g3(x1, x2, x3)  =  if_conf_1_in_2_g1(x3)
del_3_in_aag3(x1, x2, x3)  =  del_3_in_aag1(x3)
del_3_out_aag3(x1, x2, x3)  =  del_3_out_aag1(x2)
if_del_3_in_1_aag5(x1, x2, x3, x4, x5)  =  if_del_3_in_1_aag1(x5)
if_conf_1_in_3_g3(x1, x2, x3)  =  if_conf_1_in_3_g1(x3)
conf_1_out_g1(x1)  =  conf_1_out_g
DEL_3_IN_AGA3(x1, x2, x3)  =  DEL_3_IN_AGA1(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

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

DEL_3_IN_AGA3(X, ._22(H, T), ._22(H, T1)) -> DEL_3_IN_AGA3(X, T, T1)

R is empty.
The argument filtering Pi contains the following mapping:
._22(x1, x2)  =  ._21(x2)
DEL_3_IN_AGA3(x1, x2, x3)  =  DEL_3_IN_AGA1(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

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

DEL_3_IN_AGA1(._21(T)) -> DEL_3_IN_AGA1(T)

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

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

IF_CONF_1_IN_1_G2(X, del2_2_out_ga2(X, Z)) -> IF_CONF_1_IN_2_G3(X, Z, del_3_in_aag3(U, Y, Z))
CONF_1_IN_G1(X) -> IF_CONF_1_IN_1_G2(X, del2_2_in_ga2(X, Z))
IF_CONF_1_IN_2_G3(X, Z, del_3_out_aag3(U, Y, Z)) -> CONF_1_IN_G1(Y)

The TRS R consists of the following rules:

conf_1_in_g1(X) -> if_conf_1_in_1_g2(X, del2_2_in_ga2(X, Z))
del2_2_in_ga2(X, Y) -> if_del2_2_in_1_ga3(X, Y, del_3_in_aga3(U, X, Z))
del_3_in_aga3(X, ._22(X, T), T) -> del_3_out_aga3(X, ._22(X, T), T)
del_3_in_aga3(X, ._22(H, T), ._22(H, T1)) -> if_del_3_in_1_aga5(X, H, T, T1, del_3_in_aga3(X, T, T1))
if_del_3_in_1_aga5(X, H, T, T1, del_3_out_aga3(X, T, T1)) -> del_3_out_aga3(X, ._22(H, T), ._22(H, T1))
if_del2_2_in_1_ga3(X, Y, del_3_out_aga3(U, X, Z)) -> if_del2_2_in_2_ga4(X, Y, Z, del_3_in_aga3(V, Z, Y))
if_del2_2_in_2_ga4(X, Y, Z, del_3_out_aga3(V, Z, Y)) -> del2_2_out_ga2(X, Y)
if_conf_1_in_1_g2(X, del2_2_out_ga2(X, Z)) -> if_conf_1_in_2_g3(X, Z, del_3_in_aag3(U, Y, Z))
del_3_in_aag3(X, ._22(X, T), T) -> del_3_out_aag3(X, ._22(X, T), T)
del_3_in_aag3(X, ._22(H, T), ._22(H, T1)) -> if_del_3_in_1_aag5(X, H, T, T1, del_3_in_aag3(X, T, T1))
if_del_3_in_1_aag5(X, H, T, T1, del_3_out_aag3(X, T, T1)) -> del_3_out_aag3(X, ._22(H, T), ._22(H, T1))
if_conf_1_in_2_g3(X, Z, del_3_out_aag3(U, Y, Z)) -> if_conf_1_in_3_g3(X, Y, conf_1_in_g1(Y))
if_conf_1_in_3_g3(X, Y, conf_1_out_g1(Y)) -> conf_1_out_g1(X)

The argument filtering Pi contains the following mapping:
conf_1_in_g1(x1)  =  conf_1_in_g1(x1)
._22(x1, x2)  =  ._21(x2)
if_conf_1_in_1_g2(x1, x2)  =  if_conf_1_in_1_g1(x2)
del2_2_in_ga2(x1, x2)  =  del2_2_in_ga1(x1)
if_del2_2_in_1_ga3(x1, x2, x3)  =  if_del2_2_in_1_ga1(x3)
del_3_in_aga3(x1, x2, x3)  =  del_3_in_aga1(x2)
del_3_out_aga3(x1, x2, x3)  =  del_3_out_aga1(x3)
if_del_3_in_1_aga5(x1, x2, x3, x4, x5)  =  if_del_3_in_1_aga1(x5)
if_del2_2_in_2_ga4(x1, x2, x3, x4)  =  if_del2_2_in_2_ga1(x4)
del2_2_out_ga2(x1, x2)  =  del2_2_out_ga1(x2)
if_conf_1_in_2_g3(x1, x2, x3)  =  if_conf_1_in_2_g1(x3)
del_3_in_aag3(x1, x2, x3)  =  del_3_in_aag1(x3)
del_3_out_aag3(x1, x2, x3)  =  del_3_out_aag1(x2)
if_del_3_in_1_aag5(x1, x2, x3, x4, x5)  =  if_del_3_in_1_aag1(x5)
if_conf_1_in_3_g3(x1, x2, x3)  =  if_conf_1_in_3_g1(x3)
conf_1_out_g1(x1)  =  conf_1_out_g
IF_CONF_1_IN_1_G2(x1, x2)  =  IF_CONF_1_IN_1_G1(x2)
IF_CONF_1_IN_2_G3(x1, x2, x3)  =  IF_CONF_1_IN_2_G1(x3)
CONF_1_IN_G1(x1)  =  CONF_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
                    ↳ UsableRulesProof
                      ↳ PiDP
                        ↳ PiDPToQDPProof

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

IF_CONF_1_IN_1_G2(X, del2_2_out_ga2(X, Z)) -> IF_CONF_1_IN_2_G3(X, Z, del_3_in_aag3(U, Y, Z))
CONF_1_IN_G1(X) -> IF_CONF_1_IN_1_G2(X, del2_2_in_ga2(X, Z))
IF_CONF_1_IN_2_G3(X, Z, del_3_out_aag3(U, Y, Z)) -> CONF_1_IN_G1(Y)

The TRS R consists of the following rules:

del_3_in_aag3(X, ._22(X, T), T) -> del_3_out_aag3(X, ._22(X, T), T)
del_3_in_aag3(X, ._22(H, T), ._22(H, T1)) -> if_del_3_in_1_aag5(X, H, T, T1, del_3_in_aag3(X, T, T1))
del2_2_in_ga2(X, Y) -> if_del2_2_in_1_ga3(X, Y, del_3_in_aga3(U, X, Z))
if_del_3_in_1_aag5(X, H, T, T1, del_3_out_aag3(X, T, T1)) -> del_3_out_aag3(X, ._22(H, T), ._22(H, T1))
if_del2_2_in_1_ga3(X, Y, del_3_out_aga3(U, X, Z)) -> if_del2_2_in_2_ga4(X, Y, Z, del_3_in_aga3(V, Z, Y))
del_3_in_aga3(X, ._22(X, T), T) -> del_3_out_aga3(X, ._22(X, T), T)
del_3_in_aga3(X, ._22(H, T), ._22(H, T1)) -> if_del_3_in_1_aga5(X, H, T, T1, del_3_in_aga3(X, T, T1))
if_del2_2_in_2_ga4(X, Y, Z, del_3_out_aga3(V, Z, Y)) -> del2_2_out_ga2(X, Y)
if_del_3_in_1_aga5(X, H, T, T1, del_3_out_aga3(X, T, T1)) -> del_3_out_aga3(X, ._22(H, T), ._22(H, T1))

The argument filtering Pi contains the following mapping:
._22(x1, x2)  =  ._21(x2)
del2_2_in_ga2(x1, x2)  =  del2_2_in_ga1(x1)
if_del2_2_in_1_ga3(x1, x2, x3)  =  if_del2_2_in_1_ga1(x3)
del_3_in_aga3(x1, x2, x3)  =  del_3_in_aga1(x2)
del_3_out_aga3(x1, x2, x3)  =  del_3_out_aga1(x3)
if_del_3_in_1_aga5(x1, x2, x3, x4, x5)  =  if_del_3_in_1_aga1(x5)
if_del2_2_in_2_ga4(x1, x2, x3, x4)  =  if_del2_2_in_2_ga1(x4)
del2_2_out_ga2(x1, x2)  =  del2_2_out_ga1(x2)
del_3_in_aag3(x1, x2, x3)  =  del_3_in_aag1(x3)
del_3_out_aag3(x1, x2, x3)  =  del_3_out_aag1(x2)
if_del_3_in_1_aag5(x1, x2, x3, x4, x5)  =  if_del_3_in_1_aag1(x5)
IF_CONF_1_IN_1_G2(x1, x2)  =  IF_CONF_1_IN_1_G1(x2)
IF_CONF_1_IN_2_G3(x1, x2, x3)  =  IF_CONF_1_IN_2_G1(x3)
CONF_1_IN_G1(x1)  =  CONF_1_IN_G1(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
  ↳ UnrequestedClauseRemoverProof
    ↳ PROLOG
      ↳ PrologToPiTRSProof
        ↳ PiTRS
          ↳ DependencyPairsProof
            ↳ PiDP
              ↳ DependencyGraphProof
                ↳ AND
                  ↳ PiDP
                  ↳ PiDP
                  ↳ PiDP
                    ↳ UsableRulesProof
                      ↳ PiDP
                        ↳ PiDPToQDPProof
                          ↳ QDP
                            ↳ RuleRemovalProof

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

IF_CONF_1_IN_1_G1(del2_2_out_ga1(Z)) -> IF_CONF_1_IN_2_G1(del_3_in_aag1(Z))
CONF_1_IN_G1(X) -> IF_CONF_1_IN_1_G1(del2_2_in_ga1(X))
IF_CONF_1_IN_2_G1(del_3_out_aag1(Y)) -> CONF_1_IN_G1(Y)

The TRS R consists of the following rules:

del_3_in_aag1(T) -> del_3_out_aag1(._21(T))
del_3_in_aag1(._21(T1)) -> if_del_3_in_1_aag1(del_3_in_aag1(T1))
del2_2_in_ga1(X) -> if_del2_2_in_1_ga1(del_3_in_aga1(X))
if_del_3_in_1_aag1(del_3_out_aag1(T)) -> del_3_out_aag1(._21(T))
if_del2_2_in_1_ga1(del_3_out_aga1(Z)) -> if_del2_2_in_2_ga1(del_3_in_aga1(Z))
del_3_in_aga1(._21(T)) -> del_3_out_aga1(T)
del_3_in_aga1(._21(T)) -> if_del_3_in_1_aga1(del_3_in_aga1(T))
if_del2_2_in_2_ga1(del_3_out_aga1(Y)) -> del2_2_out_ga1(Y)
if_del_3_in_1_aga1(del_3_out_aga1(T1)) -> del_3_out_aga1(._21(T1))

The set Q consists of the following terms:

del_3_in_aag1(x0)
del2_2_in_ga1(x0)
if_del_3_in_1_aag1(x0)
if_del2_2_in_1_ga1(x0)
del_3_in_aga1(x0)
if_del2_2_in_2_ga1(x0)
if_del_3_in_1_aga1(x0)

We have to consider all (P,Q,R)-chains.
The head symbols of this DP problem are {IF_CONF_1_IN_2_G1, IF_CONF_1_IN_1_G1, CONF_1_IN_G1}.
By using a polynomial ordering, at least one Dependency Pair or term rewrite system rule of this QDP problem can be strictly oriented.

Strictly oriented rules of the TRS R:

del_3_in_aga1(._21(T)) -> del_3_out_aga1(T)

Used ordering: POLO with Polynomial interpretation:

POL(CONF_1_IN_G1(x1)) = x1   
POL(del_3_out_aga1(x1)) = 1 + x1   
POL(if_del_3_in_1_aga1(x1)) = 2 + x1   
POL(if_del_3_in_1_aag1(x1)) = 2 + x1   
POL(del2_2_out_ga1(x1)) = 2 + x1   
POL(del_3_in_aag1(x1)) = 2 + x1   
POL(if_del2_2_in_2_ga1(x1)) = 1 + x1   
POL(if_del2_2_in_1_ga1(x1)) = x1   
POL(IF_CONF_1_IN_1_G1(x1)) = x1   
POL(del_3_out_aag1(x1)) = x1   
POL(del2_2_in_ga1(x1)) = x1   
POL(del_3_in_aga1(x1)) = x1   
POL(IF_CONF_1_IN_2_G1(x1)) = x1   
POL(._21(x1)) = 2 + x1   



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

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

IF_CONF_1_IN_1_G1(del2_2_out_ga1(Z)) -> IF_CONF_1_IN_2_G1(del_3_in_aag1(Z))
CONF_1_IN_G1(X) -> IF_CONF_1_IN_1_G1(del2_2_in_ga1(X))
IF_CONF_1_IN_2_G1(del_3_out_aag1(Y)) -> CONF_1_IN_G1(Y)

The TRS R consists of the following rules:

del_3_in_aag1(T) -> del_3_out_aag1(._21(T))
del_3_in_aag1(._21(T1)) -> if_del_3_in_1_aag1(del_3_in_aag1(T1))
del2_2_in_ga1(X) -> if_del2_2_in_1_ga1(del_3_in_aga1(X))
if_del_3_in_1_aag1(del_3_out_aag1(T)) -> del_3_out_aag1(._21(T))
if_del2_2_in_1_ga1(del_3_out_aga1(Z)) -> if_del2_2_in_2_ga1(del_3_in_aga1(Z))
del_3_in_aga1(._21(T)) -> if_del_3_in_1_aga1(del_3_in_aga1(T))
if_del2_2_in_2_ga1(del_3_out_aga1(Y)) -> del2_2_out_ga1(Y)
if_del_3_in_1_aga1(del_3_out_aga1(T1)) -> del_3_out_aga1(._21(T1))

The set Q consists of the following terms:

del_3_in_aag1(x0)
del2_2_in_ga1(x0)
if_del_3_in_1_aag1(x0)
if_del2_2_in_1_ga1(x0)
del_3_in_aga1(x0)
if_del2_2_in_2_ga1(x0)
if_del_3_in_1_aga1(x0)

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

Order:Polynomial interpretation:


POL(if_del2_2_in_2_ga1(x1)) = x1   
POL(if_del2_2_in_1_ga1(x1)) = 0   
POL(del_3_out_aga1(x1)) = 1 + x1   
POL(del_3_out_aag1(x1)) = x1   
POL(if_del_3_in_1_aga1(x1)) = x1   
POL(del2_2_in_ga1(x1)) = x1   
POL(del2_2_out_ga1(x1)) = 1 + x1   
POL(if_del_3_in_1_aag1(x1)) = 0   
POL(del_3_in_aga1(x1)) = 0   
POL(del_3_in_aag1(x1)) = x1   
POL(._21(x1)) = 0   

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

We oriented the following set of usable rules.


if_del_3_in_1_aga1(del_3_out_aga1(T1)) -> del_3_out_aga1(._21(T1))
if_del_3_in_1_aag1(del_3_out_aag1(T)) -> del_3_out_aag1(._21(T))
if_del2_2_in_2_ga1(del_3_out_aga1(Y)) -> del2_2_out_ga1(Y)
if_del2_2_in_1_ga1(del_3_out_aga1(Z)) -> if_del2_2_in_2_ga1(del_3_in_aga1(Z))
del_3_in_aga1(._21(T)) -> if_del_3_in_1_aga1(del_3_in_aga1(T))
del_3_in_aag1(T) -> del_3_out_aag1(._21(T))
del_3_in_aag1(._21(T1)) -> if_del_3_in_1_aag1(del_3_in_aag1(T1))
del2_2_in_ga1(X) -> if_del2_2_in_1_ga1(del_3_in_aga1(X))