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



↳ PROLOG
  ↳ PrologToPiTRSProof

e2(a0, b0).
q2(X, Y) :- e2(X, Y).
q2(X, f12 (X)) :- p2(X, f12 (X)), q2(X, f1(X)).
q2(X, f12 (Y)) :- p2(X, f1(Y)).
p2(X, Y) :- e2(X, Y).
p2(X, f1(Y)) :- r2(X, f1(Y)), p2(X, Y).
r2(X, Y) :- e2(X, Y).
r2(X, f1(Y)) :- q2(X, Y), r2(X, Y).
r2(f1(X), f1(X)) :- t2(f1(X), f1(X)).
t2(X, Y) :- e2(X, Y).
t2(f1(X), f1(Y)) :- q2(f1(X), f1(Y)), t2(X, Y).


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


q_2_in_gg2(X, Y) -> if_q_2_in_1_gg3(X, Y, e_2_in_gg2(X, Y))
e_2_in_gg2(a_0, b_0) -> e_2_out_gg2(a_0, b_0)
if_q_2_in_1_gg3(X, Y, e_2_out_gg2(X, Y)) -> q_2_out_gg2(X, Y)
q_2_in_gg2(X, f_11(f_11(X))) -> if_q_2_in_2_gg2(X, p_2_in_gg2(X, f_11(f_11(X))))
p_2_in_gg2(X, Y) -> if_p_2_in_1_gg3(X, Y, e_2_in_gg2(X, Y))
if_p_2_in_1_gg3(X, Y, e_2_out_gg2(X, Y)) -> p_2_out_gg2(X, Y)
p_2_in_gg2(X, f_11(Y)) -> if_p_2_in_2_gg3(X, Y, r_2_in_gg2(X, f_11(Y)))
r_2_in_gg2(X, Y) -> if_r_2_in_1_gg3(X, Y, e_2_in_gg2(X, Y))
if_r_2_in_1_gg3(X, Y, e_2_out_gg2(X, Y)) -> r_2_out_gg2(X, Y)
r_2_in_gg2(X, f_11(Y)) -> if_r_2_in_2_gg3(X, Y, q_2_in_gg2(X, Y))
q_2_in_gg2(X, f_11(f_11(Y))) -> if_q_2_in_4_gg3(X, Y, p_2_in_gg2(X, f_11(Y)))
if_q_2_in_4_gg3(X, Y, p_2_out_gg2(X, f_11(Y))) -> q_2_out_gg2(X, f_11(f_11(Y)))
if_r_2_in_2_gg3(X, Y, q_2_out_gg2(X, Y)) -> if_r_2_in_3_gg3(X, Y, r_2_in_gg2(X, Y))
r_2_in_gg2(f_11(X), f_11(X)) -> if_r_2_in_4_gg2(X, t_2_in_gg2(f_11(X), f_11(X)))
t_2_in_gg2(X, Y) -> if_t_2_in_1_gg3(X, Y, e_2_in_gg2(X, Y))
if_t_2_in_1_gg3(X, Y, e_2_out_gg2(X, Y)) -> t_2_out_gg2(X, Y)
t_2_in_gg2(f_11(X), f_11(Y)) -> if_t_2_in_2_gg3(X, Y, q_2_in_gg2(f_11(X), f_11(Y)))
if_t_2_in_2_gg3(X, Y, q_2_out_gg2(f_11(X), f_11(Y))) -> if_t_2_in_3_gg3(X, Y, t_2_in_gg2(X, Y))
if_t_2_in_3_gg3(X, Y, t_2_out_gg2(X, Y)) -> t_2_out_gg2(f_11(X), f_11(Y))
if_r_2_in_4_gg2(X, t_2_out_gg2(f_11(X), f_11(X))) -> r_2_out_gg2(f_11(X), f_11(X))
if_r_2_in_3_gg3(X, Y, r_2_out_gg2(X, Y)) -> r_2_out_gg2(X, f_11(Y))
if_p_2_in_2_gg3(X, Y, r_2_out_gg2(X, f_11(Y))) -> if_p_2_in_3_gg3(X, Y, p_2_in_gg2(X, Y))
if_p_2_in_3_gg3(X, Y, p_2_out_gg2(X, Y)) -> p_2_out_gg2(X, f_11(Y))
if_q_2_in_2_gg2(X, p_2_out_gg2(X, f_11(f_11(X)))) -> if_q_2_in_3_gg2(X, q_2_in_gg2(X, f_11(X)))
if_q_2_in_3_gg2(X, q_2_out_gg2(X, f_11(X))) -> q_2_out_gg2(X, f_11(f_11(X)))

The argument filtering Pi contains the following mapping:
q_2_in_gg2(x1, x2)  =  q_2_in_gg2(x1, x2)
a_0  =  a_0
b_0  =  b_0
f_11(x1)  =  f_11(x1)
if_q_2_in_1_gg3(x1, x2, x3)  =  if_q_2_in_1_gg1(x3)
e_2_in_gg2(x1, x2)  =  e_2_in_gg2(x1, x2)
e_2_out_gg2(x1, x2)  =  e_2_out_gg
q_2_out_gg2(x1, x2)  =  q_2_out_gg
if_q_2_in_2_gg2(x1, x2)  =  if_q_2_in_2_gg2(x1, x2)
p_2_in_gg2(x1, x2)  =  p_2_in_gg2(x1, x2)
if_p_2_in_1_gg3(x1, x2, x3)  =  if_p_2_in_1_gg1(x3)
p_2_out_gg2(x1, x2)  =  p_2_out_gg
if_p_2_in_2_gg3(x1, x2, x3)  =  if_p_2_in_2_gg3(x1, x2, x3)
r_2_in_gg2(x1, x2)  =  r_2_in_gg2(x1, x2)
if_r_2_in_1_gg3(x1, x2, x3)  =  if_r_2_in_1_gg1(x3)
r_2_out_gg2(x1, x2)  =  r_2_out_gg
if_r_2_in_2_gg3(x1, x2, x3)  =  if_r_2_in_2_gg3(x1, x2, x3)
if_q_2_in_4_gg3(x1, x2, x3)  =  if_q_2_in_4_gg1(x3)
if_r_2_in_3_gg3(x1, x2, x3)  =  if_r_2_in_3_gg1(x3)
if_r_2_in_4_gg2(x1, x2)  =  if_r_2_in_4_gg1(x2)
t_2_in_gg2(x1, x2)  =  t_2_in_gg2(x1, x2)
if_t_2_in_1_gg3(x1, x2, x3)  =  if_t_2_in_1_gg1(x3)
t_2_out_gg2(x1, x2)  =  t_2_out_gg
if_t_2_in_2_gg3(x1, x2, x3)  =  if_t_2_in_2_gg3(x1, x2, x3)
if_t_2_in_3_gg3(x1, x2, x3)  =  if_t_2_in_3_gg1(x3)
if_p_2_in_3_gg3(x1, x2, x3)  =  if_p_2_in_3_gg1(x3)
if_q_2_in_3_gg2(x1, x2)  =  if_q_2_in_3_gg1(x2)

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:

q_2_in_gg2(X, Y) -> if_q_2_in_1_gg3(X, Y, e_2_in_gg2(X, Y))
e_2_in_gg2(a_0, b_0) -> e_2_out_gg2(a_0, b_0)
if_q_2_in_1_gg3(X, Y, e_2_out_gg2(X, Y)) -> q_2_out_gg2(X, Y)
q_2_in_gg2(X, f_11(f_11(X))) -> if_q_2_in_2_gg2(X, p_2_in_gg2(X, f_11(f_11(X))))
p_2_in_gg2(X, Y) -> if_p_2_in_1_gg3(X, Y, e_2_in_gg2(X, Y))
if_p_2_in_1_gg3(X, Y, e_2_out_gg2(X, Y)) -> p_2_out_gg2(X, Y)
p_2_in_gg2(X, f_11(Y)) -> if_p_2_in_2_gg3(X, Y, r_2_in_gg2(X, f_11(Y)))
r_2_in_gg2(X, Y) -> if_r_2_in_1_gg3(X, Y, e_2_in_gg2(X, Y))
if_r_2_in_1_gg3(X, Y, e_2_out_gg2(X, Y)) -> r_2_out_gg2(X, Y)
r_2_in_gg2(X, f_11(Y)) -> if_r_2_in_2_gg3(X, Y, q_2_in_gg2(X, Y))
q_2_in_gg2(X, f_11(f_11(Y))) -> if_q_2_in_4_gg3(X, Y, p_2_in_gg2(X, f_11(Y)))
if_q_2_in_4_gg3(X, Y, p_2_out_gg2(X, f_11(Y))) -> q_2_out_gg2(X, f_11(f_11(Y)))
if_r_2_in_2_gg3(X, Y, q_2_out_gg2(X, Y)) -> if_r_2_in_3_gg3(X, Y, r_2_in_gg2(X, Y))
r_2_in_gg2(f_11(X), f_11(X)) -> if_r_2_in_4_gg2(X, t_2_in_gg2(f_11(X), f_11(X)))
t_2_in_gg2(X, Y) -> if_t_2_in_1_gg3(X, Y, e_2_in_gg2(X, Y))
if_t_2_in_1_gg3(X, Y, e_2_out_gg2(X, Y)) -> t_2_out_gg2(X, Y)
t_2_in_gg2(f_11(X), f_11(Y)) -> if_t_2_in_2_gg3(X, Y, q_2_in_gg2(f_11(X), f_11(Y)))
if_t_2_in_2_gg3(X, Y, q_2_out_gg2(f_11(X), f_11(Y))) -> if_t_2_in_3_gg3(X, Y, t_2_in_gg2(X, Y))
if_t_2_in_3_gg3(X, Y, t_2_out_gg2(X, Y)) -> t_2_out_gg2(f_11(X), f_11(Y))
if_r_2_in_4_gg2(X, t_2_out_gg2(f_11(X), f_11(X))) -> r_2_out_gg2(f_11(X), f_11(X))
if_r_2_in_3_gg3(X, Y, r_2_out_gg2(X, Y)) -> r_2_out_gg2(X, f_11(Y))
if_p_2_in_2_gg3(X, Y, r_2_out_gg2(X, f_11(Y))) -> if_p_2_in_3_gg3(X, Y, p_2_in_gg2(X, Y))
if_p_2_in_3_gg3(X, Y, p_2_out_gg2(X, Y)) -> p_2_out_gg2(X, f_11(Y))
if_q_2_in_2_gg2(X, p_2_out_gg2(X, f_11(f_11(X)))) -> if_q_2_in_3_gg2(X, q_2_in_gg2(X, f_11(X)))
if_q_2_in_3_gg2(X, q_2_out_gg2(X, f_11(X))) -> q_2_out_gg2(X, f_11(f_11(X)))

The argument filtering Pi contains the following mapping:
q_2_in_gg2(x1, x2)  =  q_2_in_gg2(x1, x2)
a_0  =  a_0
b_0  =  b_0
f_11(x1)  =  f_11(x1)
if_q_2_in_1_gg3(x1, x2, x3)  =  if_q_2_in_1_gg1(x3)
e_2_in_gg2(x1, x2)  =  e_2_in_gg2(x1, x2)
e_2_out_gg2(x1, x2)  =  e_2_out_gg
q_2_out_gg2(x1, x2)  =  q_2_out_gg
if_q_2_in_2_gg2(x1, x2)  =  if_q_2_in_2_gg2(x1, x2)
p_2_in_gg2(x1, x2)  =  p_2_in_gg2(x1, x2)
if_p_2_in_1_gg3(x1, x2, x3)  =  if_p_2_in_1_gg1(x3)
p_2_out_gg2(x1, x2)  =  p_2_out_gg
if_p_2_in_2_gg3(x1, x2, x3)  =  if_p_2_in_2_gg3(x1, x2, x3)
r_2_in_gg2(x1, x2)  =  r_2_in_gg2(x1, x2)
if_r_2_in_1_gg3(x1, x2, x3)  =  if_r_2_in_1_gg1(x3)
r_2_out_gg2(x1, x2)  =  r_2_out_gg
if_r_2_in_2_gg3(x1, x2, x3)  =  if_r_2_in_2_gg3(x1, x2, x3)
if_q_2_in_4_gg3(x1, x2, x3)  =  if_q_2_in_4_gg1(x3)
if_r_2_in_3_gg3(x1, x2, x3)  =  if_r_2_in_3_gg1(x3)
if_r_2_in_4_gg2(x1, x2)  =  if_r_2_in_4_gg1(x2)
t_2_in_gg2(x1, x2)  =  t_2_in_gg2(x1, x2)
if_t_2_in_1_gg3(x1, x2, x3)  =  if_t_2_in_1_gg1(x3)
t_2_out_gg2(x1, x2)  =  t_2_out_gg
if_t_2_in_2_gg3(x1, x2, x3)  =  if_t_2_in_2_gg3(x1, x2, x3)
if_t_2_in_3_gg3(x1, x2, x3)  =  if_t_2_in_3_gg1(x3)
if_p_2_in_3_gg3(x1, x2, x3)  =  if_p_2_in_3_gg1(x3)
if_q_2_in_3_gg2(x1, x2)  =  if_q_2_in_3_gg1(x2)


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

Q_2_IN_GG2(X, Y) -> IF_Q_2_IN_1_GG3(X, Y, e_2_in_gg2(X, Y))
Q_2_IN_GG2(X, Y) -> E_2_IN_GG2(X, Y)
Q_2_IN_GG2(X, f_11(f_11(X))) -> IF_Q_2_IN_2_GG2(X, p_2_in_gg2(X, f_11(f_11(X))))
Q_2_IN_GG2(X, f_11(f_11(X))) -> P_2_IN_GG2(X, f_11(f_11(X)))
P_2_IN_GG2(X, Y) -> IF_P_2_IN_1_GG3(X, Y, e_2_in_gg2(X, Y))
P_2_IN_GG2(X, Y) -> E_2_IN_GG2(X, Y)
P_2_IN_GG2(X, f_11(Y)) -> IF_P_2_IN_2_GG3(X, Y, r_2_in_gg2(X, f_11(Y)))
P_2_IN_GG2(X, f_11(Y)) -> R_2_IN_GG2(X, f_11(Y))
R_2_IN_GG2(X, Y) -> IF_R_2_IN_1_GG3(X, Y, e_2_in_gg2(X, Y))
R_2_IN_GG2(X, Y) -> E_2_IN_GG2(X, Y)
R_2_IN_GG2(X, f_11(Y)) -> IF_R_2_IN_2_GG3(X, Y, q_2_in_gg2(X, Y))
R_2_IN_GG2(X, f_11(Y)) -> Q_2_IN_GG2(X, Y)
Q_2_IN_GG2(X, f_11(f_11(Y))) -> IF_Q_2_IN_4_GG3(X, Y, p_2_in_gg2(X, f_11(Y)))
Q_2_IN_GG2(X, f_11(f_11(Y))) -> P_2_IN_GG2(X, f_11(Y))
IF_R_2_IN_2_GG3(X, Y, q_2_out_gg2(X, Y)) -> IF_R_2_IN_3_GG3(X, Y, r_2_in_gg2(X, Y))
IF_R_2_IN_2_GG3(X, Y, q_2_out_gg2(X, Y)) -> R_2_IN_GG2(X, Y)
R_2_IN_GG2(f_11(X), f_11(X)) -> IF_R_2_IN_4_GG2(X, t_2_in_gg2(f_11(X), f_11(X)))
R_2_IN_GG2(f_11(X), f_11(X)) -> T_2_IN_GG2(f_11(X), f_11(X))
T_2_IN_GG2(X, Y) -> IF_T_2_IN_1_GG3(X, Y, e_2_in_gg2(X, Y))
T_2_IN_GG2(X, Y) -> E_2_IN_GG2(X, Y)
T_2_IN_GG2(f_11(X), f_11(Y)) -> IF_T_2_IN_2_GG3(X, Y, q_2_in_gg2(f_11(X), f_11(Y)))
T_2_IN_GG2(f_11(X), f_11(Y)) -> Q_2_IN_GG2(f_11(X), f_11(Y))
IF_T_2_IN_2_GG3(X, Y, q_2_out_gg2(f_11(X), f_11(Y))) -> IF_T_2_IN_3_GG3(X, Y, t_2_in_gg2(X, Y))
IF_T_2_IN_2_GG3(X, Y, q_2_out_gg2(f_11(X), f_11(Y))) -> T_2_IN_GG2(X, Y)
IF_P_2_IN_2_GG3(X, Y, r_2_out_gg2(X, f_11(Y))) -> IF_P_2_IN_3_GG3(X, Y, p_2_in_gg2(X, Y))
IF_P_2_IN_2_GG3(X, Y, r_2_out_gg2(X, f_11(Y))) -> P_2_IN_GG2(X, Y)
IF_Q_2_IN_2_GG2(X, p_2_out_gg2(X, f_11(f_11(X)))) -> IF_Q_2_IN_3_GG2(X, q_2_in_gg2(X, f_11(X)))
IF_Q_2_IN_2_GG2(X, p_2_out_gg2(X, f_11(f_11(X)))) -> Q_2_IN_GG2(X, f_11(X))

The TRS R consists of the following rules:

q_2_in_gg2(X, Y) -> if_q_2_in_1_gg3(X, Y, e_2_in_gg2(X, Y))
e_2_in_gg2(a_0, b_0) -> e_2_out_gg2(a_0, b_0)
if_q_2_in_1_gg3(X, Y, e_2_out_gg2(X, Y)) -> q_2_out_gg2(X, Y)
q_2_in_gg2(X, f_11(f_11(X))) -> if_q_2_in_2_gg2(X, p_2_in_gg2(X, f_11(f_11(X))))
p_2_in_gg2(X, Y) -> if_p_2_in_1_gg3(X, Y, e_2_in_gg2(X, Y))
if_p_2_in_1_gg3(X, Y, e_2_out_gg2(X, Y)) -> p_2_out_gg2(X, Y)
p_2_in_gg2(X, f_11(Y)) -> if_p_2_in_2_gg3(X, Y, r_2_in_gg2(X, f_11(Y)))
r_2_in_gg2(X, Y) -> if_r_2_in_1_gg3(X, Y, e_2_in_gg2(X, Y))
if_r_2_in_1_gg3(X, Y, e_2_out_gg2(X, Y)) -> r_2_out_gg2(X, Y)
r_2_in_gg2(X, f_11(Y)) -> if_r_2_in_2_gg3(X, Y, q_2_in_gg2(X, Y))
q_2_in_gg2(X, f_11(f_11(Y))) -> if_q_2_in_4_gg3(X, Y, p_2_in_gg2(X, f_11(Y)))
if_q_2_in_4_gg3(X, Y, p_2_out_gg2(X, f_11(Y))) -> q_2_out_gg2(X, f_11(f_11(Y)))
if_r_2_in_2_gg3(X, Y, q_2_out_gg2(X, Y)) -> if_r_2_in_3_gg3(X, Y, r_2_in_gg2(X, Y))
r_2_in_gg2(f_11(X), f_11(X)) -> if_r_2_in_4_gg2(X, t_2_in_gg2(f_11(X), f_11(X)))
t_2_in_gg2(X, Y) -> if_t_2_in_1_gg3(X, Y, e_2_in_gg2(X, Y))
if_t_2_in_1_gg3(X, Y, e_2_out_gg2(X, Y)) -> t_2_out_gg2(X, Y)
t_2_in_gg2(f_11(X), f_11(Y)) -> if_t_2_in_2_gg3(X, Y, q_2_in_gg2(f_11(X), f_11(Y)))
if_t_2_in_2_gg3(X, Y, q_2_out_gg2(f_11(X), f_11(Y))) -> if_t_2_in_3_gg3(X, Y, t_2_in_gg2(X, Y))
if_t_2_in_3_gg3(X, Y, t_2_out_gg2(X, Y)) -> t_2_out_gg2(f_11(X), f_11(Y))
if_r_2_in_4_gg2(X, t_2_out_gg2(f_11(X), f_11(X))) -> r_2_out_gg2(f_11(X), f_11(X))
if_r_2_in_3_gg3(X, Y, r_2_out_gg2(X, Y)) -> r_2_out_gg2(X, f_11(Y))
if_p_2_in_2_gg3(X, Y, r_2_out_gg2(X, f_11(Y))) -> if_p_2_in_3_gg3(X, Y, p_2_in_gg2(X, Y))
if_p_2_in_3_gg3(X, Y, p_2_out_gg2(X, Y)) -> p_2_out_gg2(X, f_11(Y))
if_q_2_in_2_gg2(X, p_2_out_gg2(X, f_11(f_11(X)))) -> if_q_2_in_3_gg2(X, q_2_in_gg2(X, f_11(X)))
if_q_2_in_3_gg2(X, q_2_out_gg2(X, f_11(X))) -> q_2_out_gg2(X, f_11(f_11(X)))

The argument filtering Pi contains the following mapping:
q_2_in_gg2(x1, x2)  =  q_2_in_gg2(x1, x2)
a_0  =  a_0
b_0  =  b_0
f_11(x1)  =  f_11(x1)
if_q_2_in_1_gg3(x1, x2, x3)  =  if_q_2_in_1_gg1(x3)
e_2_in_gg2(x1, x2)  =  e_2_in_gg2(x1, x2)
e_2_out_gg2(x1, x2)  =  e_2_out_gg
q_2_out_gg2(x1, x2)  =  q_2_out_gg
if_q_2_in_2_gg2(x1, x2)  =  if_q_2_in_2_gg2(x1, x2)
p_2_in_gg2(x1, x2)  =  p_2_in_gg2(x1, x2)
if_p_2_in_1_gg3(x1, x2, x3)  =  if_p_2_in_1_gg1(x3)
p_2_out_gg2(x1, x2)  =  p_2_out_gg
if_p_2_in_2_gg3(x1, x2, x3)  =  if_p_2_in_2_gg3(x1, x2, x3)
r_2_in_gg2(x1, x2)  =  r_2_in_gg2(x1, x2)
if_r_2_in_1_gg3(x1, x2, x3)  =  if_r_2_in_1_gg1(x3)
r_2_out_gg2(x1, x2)  =  r_2_out_gg
if_r_2_in_2_gg3(x1, x2, x3)  =  if_r_2_in_2_gg3(x1, x2, x3)
if_q_2_in_4_gg3(x1, x2, x3)  =  if_q_2_in_4_gg1(x3)
if_r_2_in_3_gg3(x1, x2, x3)  =  if_r_2_in_3_gg1(x3)
if_r_2_in_4_gg2(x1, x2)  =  if_r_2_in_4_gg1(x2)
t_2_in_gg2(x1, x2)  =  t_2_in_gg2(x1, x2)
if_t_2_in_1_gg3(x1, x2, x3)  =  if_t_2_in_1_gg1(x3)
t_2_out_gg2(x1, x2)  =  t_2_out_gg
if_t_2_in_2_gg3(x1, x2, x3)  =  if_t_2_in_2_gg3(x1, x2, x3)
if_t_2_in_3_gg3(x1, x2, x3)  =  if_t_2_in_3_gg1(x3)
if_p_2_in_3_gg3(x1, x2, x3)  =  if_p_2_in_3_gg1(x3)
if_q_2_in_3_gg2(x1, x2)  =  if_q_2_in_3_gg1(x2)
R_2_IN_GG2(x1, x2)  =  R_2_IN_GG2(x1, x2)
IF_T_2_IN_1_GG3(x1, x2, x3)  =  IF_T_2_IN_1_GG1(x3)
IF_P_2_IN_3_GG3(x1, x2, x3)  =  IF_P_2_IN_3_GG1(x3)
IF_R_2_IN_4_GG2(x1, x2)  =  IF_R_2_IN_4_GG1(x2)
IF_T_2_IN_3_GG3(x1, x2, x3)  =  IF_T_2_IN_3_GG1(x3)
IF_Q_2_IN_2_GG2(x1, x2)  =  IF_Q_2_IN_2_GG2(x1, x2)
IF_Q_2_IN_4_GG3(x1, x2, x3)  =  IF_Q_2_IN_4_GG1(x3)
IF_R_2_IN_3_GG3(x1, x2, x3)  =  IF_R_2_IN_3_GG1(x3)
IF_R_2_IN_2_GG3(x1, x2, x3)  =  IF_R_2_IN_2_GG3(x1, x2, x3)
IF_Q_2_IN_3_GG2(x1, x2)  =  IF_Q_2_IN_3_GG1(x2)
IF_R_2_IN_1_GG3(x1, x2, x3)  =  IF_R_2_IN_1_GG1(x3)
Q_2_IN_GG2(x1, x2)  =  Q_2_IN_GG2(x1, x2)
IF_P_2_IN_2_GG3(x1, x2, x3)  =  IF_P_2_IN_2_GG3(x1, x2, x3)
IF_P_2_IN_1_GG3(x1, x2, x3)  =  IF_P_2_IN_1_GG1(x3)
E_2_IN_GG2(x1, x2)  =  E_2_IN_GG2(x1, x2)
IF_Q_2_IN_1_GG3(x1, x2, x3)  =  IF_Q_2_IN_1_GG1(x3)
T_2_IN_GG2(x1, x2)  =  T_2_IN_GG2(x1, x2)
IF_T_2_IN_2_GG3(x1, x2, x3)  =  IF_T_2_IN_2_GG3(x1, x2, x3)
P_2_IN_GG2(x1, x2)  =  P_2_IN_GG2(x1, x2)

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:

Q_2_IN_GG2(X, Y) -> IF_Q_2_IN_1_GG3(X, Y, e_2_in_gg2(X, Y))
Q_2_IN_GG2(X, Y) -> E_2_IN_GG2(X, Y)
Q_2_IN_GG2(X, f_11(f_11(X))) -> IF_Q_2_IN_2_GG2(X, p_2_in_gg2(X, f_11(f_11(X))))
Q_2_IN_GG2(X, f_11(f_11(X))) -> P_2_IN_GG2(X, f_11(f_11(X)))
P_2_IN_GG2(X, Y) -> IF_P_2_IN_1_GG3(X, Y, e_2_in_gg2(X, Y))
P_2_IN_GG2(X, Y) -> E_2_IN_GG2(X, Y)
P_2_IN_GG2(X, f_11(Y)) -> IF_P_2_IN_2_GG3(X, Y, r_2_in_gg2(X, f_11(Y)))
P_2_IN_GG2(X, f_11(Y)) -> R_2_IN_GG2(X, f_11(Y))
R_2_IN_GG2(X, Y) -> IF_R_2_IN_1_GG3(X, Y, e_2_in_gg2(X, Y))
R_2_IN_GG2(X, Y) -> E_2_IN_GG2(X, Y)
R_2_IN_GG2(X, f_11(Y)) -> IF_R_2_IN_2_GG3(X, Y, q_2_in_gg2(X, Y))
R_2_IN_GG2(X, f_11(Y)) -> Q_2_IN_GG2(X, Y)
Q_2_IN_GG2(X, f_11(f_11(Y))) -> IF_Q_2_IN_4_GG3(X, Y, p_2_in_gg2(X, f_11(Y)))
Q_2_IN_GG2(X, f_11(f_11(Y))) -> P_2_IN_GG2(X, f_11(Y))
IF_R_2_IN_2_GG3(X, Y, q_2_out_gg2(X, Y)) -> IF_R_2_IN_3_GG3(X, Y, r_2_in_gg2(X, Y))
IF_R_2_IN_2_GG3(X, Y, q_2_out_gg2(X, Y)) -> R_2_IN_GG2(X, Y)
R_2_IN_GG2(f_11(X), f_11(X)) -> IF_R_2_IN_4_GG2(X, t_2_in_gg2(f_11(X), f_11(X)))
R_2_IN_GG2(f_11(X), f_11(X)) -> T_2_IN_GG2(f_11(X), f_11(X))
T_2_IN_GG2(X, Y) -> IF_T_2_IN_1_GG3(X, Y, e_2_in_gg2(X, Y))
T_2_IN_GG2(X, Y) -> E_2_IN_GG2(X, Y)
T_2_IN_GG2(f_11(X), f_11(Y)) -> IF_T_2_IN_2_GG3(X, Y, q_2_in_gg2(f_11(X), f_11(Y)))
T_2_IN_GG2(f_11(X), f_11(Y)) -> Q_2_IN_GG2(f_11(X), f_11(Y))
IF_T_2_IN_2_GG3(X, Y, q_2_out_gg2(f_11(X), f_11(Y))) -> IF_T_2_IN_3_GG3(X, Y, t_2_in_gg2(X, Y))
IF_T_2_IN_2_GG3(X, Y, q_2_out_gg2(f_11(X), f_11(Y))) -> T_2_IN_GG2(X, Y)
IF_P_2_IN_2_GG3(X, Y, r_2_out_gg2(X, f_11(Y))) -> IF_P_2_IN_3_GG3(X, Y, p_2_in_gg2(X, Y))
IF_P_2_IN_2_GG3(X, Y, r_2_out_gg2(X, f_11(Y))) -> P_2_IN_GG2(X, Y)
IF_Q_2_IN_2_GG2(X, p_2_out_gg2(X, f_11(f_11(X)))) -> IF_Q_2_IN_3_GG2(X, q_2_in_gg2(X, f_11(X)))
IF_Q_2_IN_2_GG2(X, p_2_out_gg2(X, f_11(f_11(X)))) -> Q_2_IN_GG2(X, f_11(X))

The TRS R consists of the following rules:

q_2_in_gg2(X, Y) -> if_q_2_in_1_gg3(X, Y, e_2_in_gg2(X, Y))
e_2_in_gg2(a_0, b_0) -> e_2_out_gg2(a_0, b_0)
if_q_2_in_1_gg3(X, Y, e_2_out_gg2(X, Y)) -> q_2_out_gg2(X, Y)
q_2_in_gg2(X, f_11(f_11(X))) -> if_q_2_in_2_gg2(X, p_2_in_gg2(X, f_11(f_11(X))))
p_2_in_gg2(X, Y) -> if_p_2_in_1_gg3(X, Y, e_2_in_gg2(X, Y))
if_p_2_in_1_gg3(X, Y, e_2_out_gg2(X, Y)) -> p_2_out_gg2(X, Y)
p_2_in_gg2(X, f_11(Y)) -> if_p_2_in_2_gg3(X, Y, r_2_in_gg2(X, f_11(Y)))
r_2_in_gg2(X, Y) -> if_r_2_in_1_gg3(X, Y, e_2_in_gg2(X, Y))
if_r_2_in_1_gg3(X, Y, e_2_out_gg2(X, Y)) -> r_2_out_gg2(X, Y)
r_2_in_gg2(X, f_11(Y)) -> if_r_2_in_2_gg3(X, Y, q_2_in_gg2(X, Y))
q_2_in_gg2(X, f_11(f_11(Y))) -> if_q_2_in_4_gg3(X, Y, p_2_in_gg2(X, f_11(Y)))
if_q_2_in_4_gg3(X, Y, p_2_out_gg2(X, f_11(Y))) -> q_2_out_gg2(X, f_11(f_11(Y)))
if_r_2_in_2_gg3(X, Y, q_2_out_gg2(X, Y)) -> if_r_2_in_3_gg3(X, Y, r_2_in_gg2(X, Y))
r_2_in_gg2(f_11(X), f_11(X)) -> if_r_2_in_4_gg2(X, t_2_in_gg2(f_11(X), f_11(X)))
t_2_in_gg2(X, Y) -> if_t_2_in_1_gg3(X, Y, e_2_in_gg2(X, Y))
if_t_2_in_1_gg3(X, Y, e_2_out_gg2(X, Y)) -> t_2_out_gg2(X, Y)
t_2_in_gg2(f_11(X), f_11(Y)) -> if_t_2_in_2_gg3(X, Y, q_2_in_gg2(f_11(X), f_11(Y)))
if_t_2_in_2_gg3(X, Y, q_2_out_gg2(f_11(X), f_11(Y))) -> if_t_2_in_3_gg3(X, Y, t_2_in_gg2(X, Y))
if_t_2_in_3_gg3(X, Y, t_2_out_gg2(X, Y)) -> t_2_out_gg2(f_11(X), f_11(Y))
if_r_2_in_4_gg2(X, t_2_out_gg2(f_11(X), f_11(X))) -> r_2_out_gg2(f_11(X), f_11(X))
if_r_2_in_3_gg3(X, Y, r_2_out_gg2(X, Y)) -> r_2_out_gg2(X, f_11(Y))
if_p_2_in_2_gg3(X, Y, r_2_out_gg2(X, f_11(Y))) -> if_p_2_in_3_gg3(X, Y, p_2_in_gg2(X, Y))
if_p_2_in_3_gg3(X, Y, p_2_out_gg2(X, Y)) -> p_2_out_gg2(X, f_11(Y))
if_q_2_in_2_gg2(X, p_2_out_gg2(X, f_11(f_11(X)))) -> if_q_2_in_3_gg2(X, q_2_in_gg2(X, f_11(X)))
if_q_2_in_3_gg2(X, q_2_out_gg2(X, f_11(X))) -> q_2_out_gg2(X, f_11(f_11(X)))

The argument filtering Pi contains the following mapping:
q_2_in_gg2(x1, x2)  =  q_2_in_gg2(x1, x2)
a_0  =  a_0
b_0  =  b_0
f_11(x1)  =  f_11(x1)
if_q_2_in_1_gg3(x1, x2, x3)  =  if_q_2_in_1_gg1(x3)
e_2_in_gg2(x1, x2)  =  e_2_in_gg2(x1, x2)
e_2_out_gg2(x1, x2)  =  e_2_out_gg
q_2_out_gg2(x1, x2)  =  q_2_out_gg
if_q_2_in_2_gg2(x1, x2)  =  if_q_2_in_2_gg2(x1, x2)
p_2_in_gg2(x1, x2)  =  p_2_in_gg2(x1, x2)
if_p_2_in_1_gg3(x1, x2, x3)  =  if_p_2_in_1_gg1(x3)
p_2_out_gg2(x1, x2)  =  p_2_out_gg
if_p_2_in_2_gg3(x1, x2, x3)  =  if_p_2_in_2_gg3(x1, x2, x3)
r_2_in_gg2(x1, x2)  =  r_2_in_gg2(x1, x2)
if_r_2_in_1_gg3(x1, x2, x3)  =  if_r_2_in_1_gg1(x3)
r_2_out_gg2(x1, x2)  =  r_2_out_gg
if_r_2_in_2_gg3(x1, x2, x3)  =  if_r_2_in_2_gg3(x1, x2, x3)
if_q_2_in_4_gg3(x1, x2, x3)  =  if_q_2_in_4_gg1(x3)
if_r_2_in_3_gg3(x1, x2, x3)  =  if_r_2_in_3_gg1(x3)
if_r_2_in_4_gg2(x1, x2)  =  if_r_2_in_4_gg1(x2)
t_2_in_gg2(x1, x2)  =  t_2_in_gg2(x1, x2)
if_t_2_in_1_gg3(x1, x2, x3)  =  if_t_2_in_1_gg1(x3)
t_2_out_gg2(x1, x2)  =  t_2_out_gg
if_t_2_in_2_gg3(x1, x2, x3)  =  if_t_2_in_2_gg3(x1, x2, x3)
if_t_2_in_3_gg3(x1, x2, x3)  =  if_t_2_in_3_gg1(x3)
if_p_2_in_3_gg3(x1, x2, x3)  =  if_p_2_in_3_gg1(x3)
if_q_2_in_3_gg2(x1, x2)  =  if_q_2_in_3_gg1(x2)
R_2_IN_GG2(x1, x2)  =  R_2_IN_GG2(x1, x2)
IF_T_2_IN_1_GG3(x1, x2, x3)  =  IF_T_2_IN_1_GG1(x3)
IF_P_2_IN_3_GG3(x1, x2, x3)  =  IF_P_2_IN_3_GG1(x3)
IF_R_2_IN_4_GG2(x1, x2)  =  IF_R_2_IN_4_GG1(x2)
IF_T_2_IN_3_GG3(x1, x2, x3)  =  IF_T_2_IN_3_GG1(x3)
IF_Q_2_IN_2_GG2(x1, x2)  =  IF_Q_2_IN_2_GG2(x1, x2)
IF_Q_2_IN_4_GG3(x1, x2, x3)  =  IF_Q_2_IN_4_GG1(x3)
IF_R_2_IN_3_GG3(x1, x2, x3)  =  IF_R_2_IN_3_GG1(x3)
IF_R_2_IN_2_GG3(x1, x2, x3)  =  IF_R_2_IN_2_GG3(x1, x2, x3)
IF_Q_2_IN_3_GG2(x1, x2)  =  IF_Q_2_IN_3_GG1(x2)
IF_R_2_IN_1_GG3(x1, x2, x3)  =  IF_R_2_IN_1_GG1(x3)
Q_2_IN_GG2(x1, x2)  =  Q_2_IN_GG2(x1, x2)
IF_P_2_IN_2_GG3(x1, x2, x3)  =  IF_P_2_IN_2_GG3(x1, x2, x3)
IF_P_2_IN_1_GG3(x1, x2, x3)  =  IF_P_2_IN_1_GG1(x3)
E_2_IN_GG2(x1, x2)  =  E_2_IN_GG2(x1, x2)
IF_Q_2_IN_1_GG3(x1, x2, x3)  =  IF_Q_2_IN_1_GG1(x3)
T_2_IN_GG2(x1, x2)  =  T_2_IN_GG2(x1, x2)
IF_T_2_IN_2_GG3(x1, x2, x3)  =  IF_T_2_IN_2_GG3(x1, x2, x3)
P_2_IN_GG2(x1, x2)  =  P_2_IN_GG2(x1, x2)

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

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

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

R_2_IN_GG2(f_11(X), f_11(X)) -> T_2_IN_GG2(f_11(X), f_11(X))
T_2_IN_GG2(f_11(X), f_11(Y)) -> IF_T_2_IN_2_GG3(X, Y, q_2_in_gg2(f_11(X), f_11(Y)))
Q_2_IN_GG2(X, f_11(f_11(X))) -> P_2_IN_GG2(X, f_11(f_11(X)))
Q_2_IN_GG2(X, f_11(f_11(X))) -> IF_Q_2_IN_2_GG2(X, p_2_in_gg2(X, f_11(f_11(X))))
IF_R_2_IN_2_GG3(X, Y, q_2_out_gg2(X, Y)) -> R_2_IN_GG2(X, Y)
P_2_IN_GG2(X, f_11(Y)) -> R_2_IN_GG2(X, f_11(Y))
R_2_IN_GG2(X, f_11(Y)) -> IF_R_2_IN_2_GG3(X, Y, q_2_in_gg2(X, Y))
IF_Q_2_IN_2_GG2(X, p_2_out_gg2(X, f_11(f_11(X)))) -> Q_2_IN_GG2(X, f_11(X))
Q_2_IN_GG2(X, f_11(f_11(Y))) -> P_2_IN_GG2(X, f_11(Y))
T_2_IN_GG2(f_11(X), f_11(Y)) -> Q_2_IN_GG2(f_11(X), f_11(Y))
P_2_IN_GG2(X, f_11(Y)) -> IF_P_2_IN_2_GG3(X, Y, r_2_in_gg2(X, f_11(Y)))
IF_P_2_IN_2_GG3(X, Y, r_2_out_gg2(X, f_11(Y))) -> P_2_IN_GG2(X, Y)
R_2_IN_GG2(X, f_11(Y)) -> Q_2_IN_GG2(X, Y)
IF_T_2_IN_2_GG3(X, Y, q_2_out_gg2(f_11(X), f_11(Y))) -> T_2_IN_GG2(X, Y)

The TRS R consists of the following rules:

q_2_in_gg2(X, Y) -> if_q_2_in_1_gg3(X, Y, e_2_in_gg2(X, Y))
e_2_in_gg2(a_0, b_0) -> e_2_out_gg2(a_0, b_0)
if_q_2_in_1_gg3(X, Y, e_2_out_gg2(X, Y)) -> q_2_out_gg2(X, Y)
q_2_in_gg2(X, f_11(f_11(X))) -> if_q_2_in_2_gg2(X, p_2_in_gg2(X, f_11(f_11(X))))
p_2_in_gg2(X, Y) -> if_p_2_in_1_gg3(X, Y, e_2_in_gg2(X, Y))
if_p_2_in_1_gg3(X, Y, e_2_out_gg2(X, Y)) -> p_2_out_gg2(X, Y)
p_2_in_gg2(X, f_11(Y)) -> if_p_2_in_2_gg3(X, Y, r_2_in_gg2(X, f_11(Y)))
r_2_in_gg2(X, Y) -> if_r_2_in_1_gg3(X, Y, e_2_in_gg2(X, Y))
if_r_2_in_1_gg3(X, Y, e_2_out_gg2(X, Y)) -> r_2_out_gg2(X, Y)
r_2_in_gg2(X, f_11(Y)) -> if_r_2_in_2_gg3(X, Y, q_2_in_gg2(X, Y))
q_2_in_gg2(X, f_11(f_11(Y))) -> if_q_2_in_4_gg3(X, Y, p_2_in_gg2(X, f_11(Y)))
if_q_2_in_4_gg3(X, Y, p_2_out_gg2(X, f_11(Y))) -> q_2_out_gg2(X, f_11(f_11(Y)))
if_r_2_in_2_gg3(X, Y, q_2_out_gg2(X, Y)) -> if_r_2_in_3_gg3(X, Y, r_2_in_gg2(X, Y))
r_2_in_gg2(f_11(X), f_11(X)) -> if_r_2_in_4_gg2(X, t_2_in_gg2(f_11(X), f_11(X)))
t_2_in_gg2(X, Y) -> if_t_2_in_1_gg3(X, Y, e_2_in_gg2(X, Y))
if_t_2_in_1_gg3(X, Y, e_2_out_gg2(X, Y)) -> t_2_out_gg2(X, Y)
t_2_in_gg2(f_11(X), f_11(Y)) -> if_t_2_in_2_gg3(X, Y, q_2_in_gg2(f_11(X), f_11(Y)))
if_t_2_in_2_gg3(X, Y, q_2_out_gg2(f_11(X), f_11(Y))) -> if_t_2_in_3_gg3(X, Y, t_2_in_gg2(X, Y))
if_t_2_in_3_gg3(X, Y, t_2_out_gg2(X, Y)) -> t_2_out_gg2(f_11(X), f_11(Y))
if_r_2_in_4_gg2(X, t_2_out_gg2(f_11(X), f_11(X))) -> r_2_out_gg2(f_11(X), f_11(X))
if_r_2_in_3_gg3(X, Y, r_2_out_gg2(X, Y)) -> r_2_out_gg2(X, f_11(Y))
if_p_2_in_2_gg3(X, Y, r_2_out_gg2(X, f_11(Y))) -> if_p_2_in_3_gg3(X, Y, p_2_in_gg2(X, Y))
if_p_2_in_3_gg3(X, Y, p_2_out_gg2(X, Y)) -> p_2_out_gg2(X, f_11(Y))
if_q_2_in_2_gg2(X, p_2_out_gg2(X, f_11(f_11(X)))) -> if_q_2_in_3_gg2(X, q_2_in_gg2(X, f_11(X)))
if_q_2_in_3_gg2(X, q_2_out_gg2(X, f_11(X))) -> q_2_out_gg2(X, f_11(f_11(X)))

The argument filtering Pi contains the following mapping:
q_2_in_gg2(x1, x2)  =  q_2_in_gg2(x1, x2)
a_0  =  a_0
b_0  =  b_0
f_11(x1)  =  f_11(x1)
if_q_2_in_1_gg3(x1, x2, x3)  =  if_q_2_in_1_gg1(x3)
e_2_in_gg2(x1, x2)  =  e_2_in_gg2(x1, x2)
e_2_out_gg2(x1, x2)  =  e_2_out_gg
q_2_out_gg2(x1, x2)  =  q_2_out_gg
if_q_2_in_2_gg2(x1, x2)  =  if_q_2_in_2_gg2(x1, x2)
p_2_in_gg2(x1, x2)  =  p_2_in_gg2(x1, x2)
if_p_2_in_1_gg3(x1, x2, x3)  =  if_p_2_in_1_gg1(x3)
p_2_out_gg2(x1, x2)  =  p_2_out_gg
if_p_2_in_2_gg3(x1, x2, x3)  =  if_p_2_in_2_gg3(x1, x2, x3)
r_2_in_gg2(x1, x2)  =  r_2_in_gg2(x1, x2)
if_r_2_in_1_gg3(x1, x2, x3)  =  if_r_2_in_1_gg1(x3)
r_2_out_gg2(x1, x2)  =  r_2_out_gg
if_r_2_in_2_gg3(x1, x2, x3)  =  if_r_2_in_2_gg3(x1, x2, x3)
if_q_2_in_4_gg3(x1, x2, x3)  =  if_q_2_in_4_gg1(x3)
if_r_2_in_3_gg3(x1, x2, x3)  =  if_r_2_in_3_gg1(x3)
if_r_2_in_4_gg2(x1, x2)  =  if_r_2_in_4_gg1(x2)
t_2_in_gg2(x1, x2)  =  t_2_in_gg2(x1, x2)
if_t_2_in_1_gg3(x1, x2, x3)  =  if_t_2_in_1_gg1(x3)
t_2_out_gg2(x1, x2)  =  t_2_out_gg
if_t_2_in_2_gg3(x1, x2, x3)  =  if_t_2_in_2_gg3(x1, x2, x3)
if_t_2_in_3_gg3(x1, x2, x3)  =  if_t_2_in_3_gg1(x3)
if_p_2_in_3_gg3(x1, x2, x3)  =  if_p_2_in_3_gg1(x3)
if_q_2_in_3_gg2(x1, x2)  =  if_q_2_in_3_gg1(x2)
R_2_IN_GG2(x1, x2)  =  R_2_IN_GG2(x1, x2)
IF_Q_2_IN_2_GG2(x1, x2)  =  IF_Q_2_IN_2_GG2(x1, x2)
IF_R_2_IN_2_GG3(x1, x2, x3)  =  IF_R_2_IN_2_GG3(x1, x2, x3)
Q_2_IN_GG2(x1, x2)  =  Q_2_IN_GG2(x1, x2)
IF_P_2_IN_2_GG3(x1, x2, x3)  =  IF_P_2_IN_2_GG3(x1, x2, x3)
T_2_IN_GG2(x1, x2)  =  T_2_IN_GG2(x1, x2)
IF_T_2_IN_2_GG3(x1, x2, x3)  =  IF_T_2_IN_2_GG3(x1, x2, x3)
P_2_IN_GG2(x1, x2)  =  P_2_IN_GG2(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
  ↳ PrologToPiTRSProof
    ↳ PiTRS
      ↳ DependencyPairsProof
        ↳ PiDP
          ↳ DependencyGraphProof
            ↳ PiDP
              ↳ PiDPToQDPProof
                ↳ QDP
                  ↳ QDPPoloProof

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

R_2_IN_GG2(f_11(X), f_11(X)) -> T_2_IN_GG2(f_11(X), f_11(X))
T_2_IN_GG2(f_11(X), f_11(Y)) -> IF_T_2_IN_2_GG3(X, Y, q_2_in_gg2(f_11(X), f_11(Y)))
Q_2_IN_GG2(X, f_11(f_11(X))) -> P_2_IN_GG2(X, f_11(f_11(X)))
Q_2_IN_GG2(X, f_11(f_11(X))) -> IF_Q_2_IN_2_GG2(X, p_2_in_gg2(X, f_11(f_11(X))))
IF_R_2_IN_2_GG3(X, Y, q_2_out_gg) -> R_2_IN_GG2(X, Y)
P_2_IN_GG2(X, f_11(Y)) -> R_2_IN_GG2(X, f_11(Y))
R_2_IN_GG2(X, f_11(Y)) -> IF_R_2_IN_2_GG3(X, Y, q_2_in_gg2(X, Y))
IF_Q_2_IN_2_GG2(X, p_2_out_gg) -> Q_2_IN_GG2(X, f_11(X))
Q_2_IN_GG2(X, f_11(f_11(Y))) -> P_2_IN_GG2(X, f_11(Y))
T_2_IN_GG2(f_11(X), f_11(Y)) -> Q_2_IN_GG2(f_11(X), f_11(Y))
P_2_IN_GG2(X, f_11(Y)) -> IF_P_2_IN_2_GG3(X, Y, r_2_in_gg2(X, f_11(Y)))
IF_P_2_IN_2_GG3(X, Y, r_2_out_gg) -> P_2_IN_GG2(X, Y)
R_2_IN_GG2(X, f_11(Y)) -> Q_2_IN_GG2(X, Y)
IF_T_2_IN_2_GG3(X, Y, q_2_out_gg) -> T_2_IN_GG2(X, Y)

The TRS R consists of the following rules:

q_2_in_gg2(X, Y) -> if_q_2_in_1_gg1(e_2_in_gg2(X, Y))
e_2_in_gg2(a_0, b_0) -> e_2_out_gg
if_q_2_in_1_gg1(e_2_out_gg) -> q_2_out_gg
q_2_in_gg2(X, f_11(f_11(X))) -> if_q_2_in_2_gg2(X, p_2_in_gg2(X, f_11(f_11(X))))
p_2_in_gg2(X, Y) -> if_p_2_in_1_gg1(e_2_in_gg2(X, Y))
if_p_2_in_1_gg1(e_2_out_gg) -> p_2_out_gg
p_2_in_gg2(X, f_11(Y)) -> if_p_2_in_2_gg3(X, Y, r_2_in_gg2(X, f_11(Y)))
r_2_in_gg2(X, Y) -> if_r_2_in_1_gg1(e_2_in_gg2(X, Y))
if_r_2_in_1_gg1(e_2_out_gg) -> r_2_out_gg
r_2_in_gg2(X, f_11(Y)) -> if_r_2_in_2_gg3(X, Y, q_2_in_gg2(X, Y))
q_2_in_gg2(X, f_11(f_11(Y))) -> if_q_2_in_4_gg1(p_2_in_gg2(X, f_11(Y)))
if_q_2_in_4_gg1(p_2_out_gg) -> q_2_out_gg
if_r_2_in_2_gg3(X, Y, q_2_out_gg) -> if_r_2_in_3_gg1(r_2_in_gg2(X, Y))
r_2_in_gg2(f_11(X), f_11(X)) -> if_r_2_in_4_gg1(t_2_in_gg2(f_11(X), f_11(X)))
t_2_in_gg2(X, Y) -> if_t_2_in_1_gg1(e_2_in_gg2(X, Y))
if_t_2_in_1_gg1(e_2_out_gg) -> t_2_out_gg
t_2_in_gg2(f_11(X), f_11(Y)) -> if_t_2_in_2_gg3(X, Y, q_2_in_gg2(f_11(X), f_11(Y)))
if_t_2_in_2_gg3(X, Y, q_2_out_gg) -> if_t_2_in_3_gg1(t_2_in_gg2(X, Y))
if_t_2_in_3_gg1(t_2_out_gg) -> t_2_out_gg
if_r_2_in_4_gg1(t_2_out_gg) -> r_2_out_gg
if_r_2_in_3_gg1(r_2_out_gg) -> r_2_out_gg
if_p_2_in_2_gg3(X, Y, r_2_out_gg) -> if_p_2_in_3_gg1(p_2_in_gg2(X, Y))
if_p_2_in_3_gg1(p_2_out_gg) -> p_2_out_gg
if_q_2_in_2_gg2(X, p_2_out_gg) -> if_q_2_in_3_gg1(q_2_in_gg2(X, f_11(X)))
if_q_2_in_3_gg1(q_2_out_gg) -> q_2_out_gg

The set Q consists of the following terms:

q_2_in_gg2(x0, x1)
e_2_in_gg2(x0, x1)
if_q_2_in_1_gg1(x0)
p_2_in_gg2(x0, x1)
if_p_2_in_1_gg1(x0)
r_2_in_gg2(x0, x1)
if_r_2_in_1_gg1(x0)
if_q_2_in_4_gg1(x0)
if_r_2_in_2_gg3(x0, x1, x2)
t_2_in_gg2(x0, x1)
if_t_2_in_1_gg1(x0)
if_t_2_in_2_gg3(x0, x1, x2)
if_t_2_in_3_gg1(x0)
if_r_2_in_4_gg1(x0)
if_r_2_in_3_gg1(x0)
if_p_2_in_2_gg3(x0, x1, x2)
if_p_2_in_3_gg1(x0)
if_q_2_in_2_gg2(x0, x1)
if_q_2_in_3_gg1(x0)

We have to consider all (P,Q,R)-chains.
The head symbols of this DP problem are {T_2_IN_GG2, R_2_IN_GG2, IF_T_2_IN_2_GG3, P_2_IN_GG2, Q_2_IN_GG2, IF_Q_2_IN_2_GG2, IF_R_2_IN_2_GG3, IF_P_2_IN_2_GG3}.
By using a polynomial ordering, the following set of Dependency Pairs of this DP problem can be strictly oriented.

T_2_IN_GG2(f_11(X), f_11(Y)) -> IF_T_2_IN_2_GG3(X, Y, q_2_in_gg2(f_11(X), f_11(Y)))
The remaining Dependency Pairs were at least non-strictly be oriented.

R_2_IN_GG2(f_11(X), f_11(X)) -> T_2_IN_GG2(f_11(X), f_11(X))
Q_2_IN_GG2(X, f_11(f_11(X))) -> P_2_IN_GG2(X, f_11(f_11(X)))
Q_2_IN_GG2(X, f_11(f_11(X))) -> IF_Q_2_IN_2_GG2(X, p_2_in_gg2(X, f_11(f_11(X))))
IF_R_2_IN_2_GG3(X, Y, q_2_out_gg) -> R_2_IN_GG2(X, Y)
P_2_IN_GG2(X, f_11(Y)) -> R_2_IN_GG2(X, f_11(Y))
R_2_IN_GG2(X, f_11(Y)) -> IF_R_2_IN_2_GG3(X, Y, q_2_in_gg2(X, Y))
IF_Q_2_IN_2_GG2(X, p_2_out_gg) -> Q_2_IN_GG2(X, f_11(X))
Q_2_IN_GG2(X, f_11(f_11(Y))) -> P_2_IN_GG2(X, f_11(Y))
T_2_IN_GG2(f_11(X), f_11(Y)) -> Q_2_IN_GG2(f_11(X), f_11(Y))
P_2_IN_GG2(X, f_11(Y)) -> IF_P_2_IN_2_GG3(X, Y, r_2_in_gg2(X, f_11(Y)))
IF_P_2_IN_2_GG3(X, Y, r_2_out_gg) -> P_2_IN_GG2(X, Y)
R_2_IN_GG2(X, f_11(Y)) -> Q_2_IN_GG2(X, Y)
IF_T_2_IN_2_GG3(X, Y, q_2_out_gg) -> T_2_IN_GG2(X, Y)
With the implicit AFS there is no usable rule.

Used ordering: POLO with Polynomial interpretation:


POL(a_0) = 0   
POL(Q_2_IN_GG2(x1, x2)) = x1   
POL(if_t_2_in_1_gg1(x1)) = 0   
POL(if_q_2_in_3_gg1(x1)) = 0   
POL(if_p_2_in_1_gg1(x1)) = 0   
POL(T_2_IN_GG2(x1, x2)) = x1   
POL(IF_P_2_IN_2_GG3(x1, x2, x3)) = x1   
POL(if_q_2_in_2_gg2(x1, x2)) = 0   
POL(r_2_out_gg) = 0   
POL(e_2_out_gg) = 0   
POL(if_q_2_in_4_gg1(x1)) = 0   
POL(p_2_out_gg) = 0   
POL(R_2_IN_GG2(x1, x2)) = x1   
POL(if_r_2_in_3_gg1(x1)) = 0   
POL(f_11(x1)) = 1 + x1   
POL(IF_R_2_IN_2_GG3(x1, x2, x3)) = x1   
POL(if_r_2_in_4_gg1(x1)) = 0   
POL(t_2_out_gg) = 0   
POL(q_2_in_gg2(x1, x2)) = 0   
POL(IF_T_2_IN_2_GG3(x1, x2, x3)) = x1   
POL(if_p_2_in_2_gg3(x1, x2, x3)) = 0   
POL(IF_Q_2_IN_2_GG2(x1, x2)) = x1   
POL(b_0) = 0   
POL(if_t_2_in_2_gg3(x1, x2, x3)) = 0   
POL(if_q_2_in_1_gg1(x1)) = 0   
POL(if_p_2_in_3_gg1(x1)) = 0   
POL(r_2_in_gg2(x1, x2)) = 0   
POL(P_2_IN_GG2(x1, x2)) = x1   
POL(if_r_2_in_2_gg3(x1, x2, x3)) = 0   
POL(if_r_2_in_1_gg1(x1)) = 0   
POL(q_2_out_gg) = 0   
POL(if_t_2_in_3_gg1(x1)) = 0   
POL(e_2_in_gg2(x1, x2)) = 0   
POL(t_2_in_gg2(x1, x2)) = 0   
POL(p_2_in_gg2(x1, x2)) = 0   



↳ PROLOG
  ↳ PrologToPiTRSProof
    ↳ PiTRS
      ↳ DependencyPairsProof
        ↳ PiDP
          ↳ DependencyGraphProof
            ↳ PiDP
              ↳ PiDPToQDPProof
                ↳ QDP
                  ↳ QDPPoloProof
                    ↳ QDP
                      ↳ DependencyGraphProof

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

R_2_IN_GG2(f_11(X), f_11(X)) -> T_2_IN_GG2(f_11(X), f_11(X))
Q_2_IN_GG2(X, f_11(f_11(X))) -> P_2_IN_GG2(X, f_11(f_11(X)))
Q_2_IN_GG2(X, f_11(f_11(X))) -> IF_Q_2_IN_2_GG2(X, p_2_in_gg2(X, f_11(f_11(X))))
IF_R_2_IN_2_GG3(X, Y, q_2_out_gg) -> R_2_IN_GG2(X, Y)
P_2_IN_GG2(X, f_11(Y)) -> R_2_IN_GG2(X, f_11(Y))
R_2_IN_GG2(X, f_11(Y)) -> IF_R_2_IN_2_GG3(X, Y, q_2_in_gg2(X, Y))
IF_Q_2_IN_2_GG2(X, p_2_out_gg) -> Q_2_IN_GG2(X, f_11(X))
Q_2_IN_GG2(X, f_11(f_11(Y))) -> P_2_IN_GG2(X, f_11(Y))
T_2_IN_GG2(f_11(X), f_11(Y)) -> Q_2_IN_GG2(f_11(X), f_11(Y))
P_2_IN_GG2(X, f_11(Y)) -> IF_P_2_IN_2_GG3(X, Y, r_2_in_gg2(X, f_11(Y)))
IF_P_2_IN_2_GG3(X, Y, r_2_out_gg) -> P_2_IN_GG2(X, Y)
R_2_IN_GG2(X, f_11(Y)) -> Q_2_IN_GG2(X, Y)
IF_T_2_IN_2_GG3(X, Y, q_2_out_gg) -> T_2_IN_GG2(X, Y)

The TRS R consists of the following rules:

q_2_in_gg2(X, Y) -> if_q_2_in_1_gg1(e_2_in_gg2(X, Y))
e_2_in_gg2(a_0, b_0) -> e_2_out_gg
if_q_2_in_1_gg1(e_2_out_gg) -> q_2_out_gg
q_2_in_gg2(X, f_11(f_11(X))) -> if_q_2_in_2_gg2(X, p_2_in_gg2(X, f_11(f_11(X))))
p_2_in_gg2(X, Y) -> if_p_2_in_1_gg1(e_2_in_gg2(X, Y))
if_p_2_in_1_gg1(e_2_out_gg) -> p_2_out_gg
p_2_in_gg2(X, f_11(Y)) -> if_p_2_in_2_gg3(X, Y, r_2_in_gg2(X, f_11(Y)))
r_2_in_gg2(X, Y) -> if_r_2_in_1_gg1(e_2_in_gg2(X, Y))
if_r_2_in_1_gg1(e_2_out_gg) -> r_2_out_gg
r_2_in_gg2(X, f_11(Y)) -> if_r_2_in_2_gg3(X, Y, q_2_in_gg2(X, Y))
q_2_in_gg2(X, f_11(f_11(Y))) -> if_q_2_in_4_gg1(p_2_in_gg2(X, f_11(Y)))
if_q_2_in_4_gg1(p_2_out_gg) -> q_2_out_gg
if_r_2_in_2_gg3(X, Y, q_2_out_gg) -> if_r_2_in_3_gg1(r_2_in_gg2(X, Y))
r_2_in_gg2(f_11(X), f_11(X)) -> if_r_2_in_4_gg1(t_2_in_gg2(f_11(X), f_11(X)))
t_2_in_gg2(X, Y) -> if_t_2_in_1_gg1(e_2_in_gg2(X, Y))
if_t_2_in_1_gg1(e_2_out_gg) -> t_2_out_gg
t_2_in_gg2(f_11(X), f_11(Y)) -> if_t_2_in_2_gg3(X, Y, q_2_in_gg2(f_11(X), f_11(Y)))
if_t_2_in_2_gg3(X, Y, q_2_out_gg) -> if_t_2_in_3_gg1(t_2_in_gg2(X, Y))
if_t_2_in_3_gg1(t_2_out_gg) -> t_2_out_gg
if_r_2_in_4_gg1(t_2_out_gg) -> r_2_out_gg
if_r_2_in_3_gg1(r_2_out_gg) -> r_2_out_gg
if_p_2_in_2_gg3(X, Y, r_2_out_gg) -> if_p_2_in_3_gg1(p_2_in_gg2(X, Y))
if_p_2_in_3_gg1(p_2_out_gg) -> p_2_out_gg
if_q_2_in_2_gg2(X, p_2_out_gg) -> if_q_2_in_3_gg1(q_2_in_gg2(X, f_11(X)))
if_q_2_in_3_gg1(q_2_out_gg) -> q_2_out_gg

The set Q consists of the following terms:

q_2_in_gg2(x0, x1)
e_2_in_gg2(x0, x1)
if_q_2_in_1_gg1(x0)
p_2_in_gg2(x0, x1)
if_p_2_in_1_gg1(x0)
r_2_in_gg2(x0, x1)
if_r_2_in_1_gg1(x0)
if_q_2_in_4_gg1(x0)
if_r_2_in_2_gg3(x0, x1, x2)
t_2_in_gg2(x0, x1)
if_t_2_in_1_gg1(x0)
if_t_2_in_2_gg3(x0, x1, x2)
if_t_2_in_3_gg1(x0)
if_r_2_in_4_gg1(x0)
if_r_2_in_3_gg1(x0)
if_p_2_in_2_gg3(x0, x1, x2)
if_p_2_in_3_gg1(x0)
if_q_2_in_2_gg2(x0, x1)
if_q_2_in_3_gg1(x0)

We have to consider all (P,Q,R)-chains.
The head symbols of this DP problem are {T_2_IN_GG2, R_2_IN_GG2, P_2_IN_GG2, Q_2_IN_GG2, IF_Q_2_IN_2_GG2, IF_R_2_IN_2_GG3, IF_P_2_IN_2_GG3, IF_T_2_IN_2_GG3}.
The approximation of the Dependency Graph contains 1 SCC with 1 less node.

↳ PROLOG
  ↳ PrologToPiTRSProof
    ↳ PiTRS
      ↳ DependencyPairsProof
        ↳ PiDP
          ↳ DependencyGraphProof
            ↳ PiDP
              ↳ PiDPToQDPProof
                ↳ QDP
                  ↳ QDPPoloProof
                    ↳ QDP
                      ↳ DependencyGraphProof
                        ↳ QDP
                          ↳ QDPPoloProof

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

IF_R_2_IN_2_GG3(X, Y, q_2_out_gg) -> R_2_IN_GG2(X, Y)
P_2_IN_GG2(X, f_11(Y)) -> R_2_IN_GG2(X, f_11(Y))
IF_Q_2_IN_2_GG2(X, p_2_out_gg) -> Q_2_IN_GG2(X, f_11(X))
R_2_IN_GG2(X, f_11(Y)) -> IF_R_2_IN_2_GG3(X, Y, q_2_in_gg2(X, Y))
R_2_IN_GG2(f_11(X), f_11(X)) -> T_2_IN_GG2(f_11(X), f_11(X))
IF_P_2_IN_2_GG3(X, Y, r_2_out_gg) -> P_2_IN_GG2(X, Y)
Q_2_IN_GG2(X, f_11(f_11(Y))) -> P_2_IN_GG2(X, f_11(Y))
P_2_IN_GG2(X, f_11(Y)) -> IF_P_2_IN_2_GG3(X, Y, r_2_in_gg2(X, f_11(Y)))
R_2_IN_GG2(X, f_11(Y)) -> Q_2_IN_GG2(X, Y)
Q_2_IN_GG2(X, f_11(f_11(X))) -> P_2_IN_GG2(X, f_11(f_11(X)))
T_2_IN_GG2(f_11(X), f_11(Y)) -> Q_2_IN_GG2(f_11(X), f_11(Y))
Q_2_IN_GG2(X, f_11(f_11(X))) -> IF_Q_2_IN_2_GG2(X, p_2_in_gg2(X, f_11(f_11(X))))

The TRS R consists of the following rules:

q_2_in_gg2(X, Y) -> if_q_2_in_1_gg1(e_2_in_gg2(X, Y))
e_2_in_gg2(a_0, b_0) -> e_2_out_gg
if_q_2_in_1_gg1(e_2_out_gg) -> q_2_out_gg
q_2_in_gg2(X, f_11(f_11(X))) -> if_q_2_in_2_gg2(X, p_2_in_gg2(X, f_11(f_11(X))))
p_2_in_gg2(X, Y) -> if_p_2_in_1_gg1(e_2_in_gg2(X, Y))
if_p_2_in_1_gg1(e_2_out_gg) -> p_2_out_gg
p_2_in_gg2(X, f_11(Y)) -> if_p_2_in_2_gg3(X, Y, r_2_in_gg2(X, f_11(Y)))
r_2_in_gg2(X, Y) -> if_r_2_in_1_gg1(e_2_in_gg2(X, Y))
if_r_2_in_1_gg1(e_2_out_gg) -> r_2_out_gg
r_2_in_gg2(X, f_11(Y)) -> if_r_2_in_2_gg3(X, Y, q_2_in_gg2(X, Y))
q_2_in_gg2(X, f_11(f_11(Y))) -> if_q_2_in_4_gg1(p_2_in_gg2(X, f_11(Y)))
if_q_2_in_4_gg1(p_2_out_gg) -> q_2_out_gg
if_r_2_in_2_gg3(X, Y, q_2_out_gg) -> if_r_2_in_3_gg1(r_2_in_gg2(X, Y))
r_2_in_gg2(f_11(X), f_11(X)) -> if_r_2_in_4_gg1(t_2_in_gg2(f_11(X), f_11(X)))
t_2_in_gg2(X, Y) -> if_t_2_in_1_gg1(e_2_in_gg2(X, Y))
if_t_2_in_1_gg1(e_2_out_gg) -> t_2_out_gg
t_2_in_gg2(f_11(X), f_11(Y)) -> if_t_2_in_2_gg3(X, Y, q_2_in_gg2(f_11(X), f_11(Y)))
if_t_2_in_2_gg3(X, Y, q_2_out_gg) -> if_t_2_in_3_gg1(t_2_in_gg2(X, Y))
if_t_2_in_3_gg1(t_2_out_gg) -> t_2_out_gg
if_r_2_in_4_gg1(t_2_out_gg) -> r_2_out_gg
if_r_2_in_3_gg1(r_2_out_gg) -> r_2_out_gg
if_p_2_in_2_gg3(X, Y, r_2_out_gg) -> if_p_2_in_3_gg1(p_2_in_gg2(X, Y))
if_p_2_in_3_gg1(p_2_out_gg) -> p_2_out_gg
if_q_2_in_2_gg2(X, p_2_out_gg) -> if_q_2_in_3_gg1(q_2_in_gg2(X, f_11(X)))
if_q_2_in_3_gg1(q_2_out_gg) -> q_2_out_gg

The set Q consists of the following terms:

q_2_in_gg2(x0, x1)
e_2_in_gg2(x0, x1)
if_q_2_in_1_gg1(x0)
p_2_in_gg2(x0, x1)
if_p_2_in_1_gg1(x0)
r_2_in_gg2(x0, x1)
if_r_2_in_1_gg1(x0)
if_q_2_in_4_gg1(x0)
if_r_2_in_2_gg3(x0, x1, x2)
t_2_in_gg2(x0, x1)
if_t_2_in_1_gg1(x0)
if_t_2_in_2_gg3(x0, x1, x2)
if_t_2_in_3_gg1(x0)
if_r_2_in_4_gg1(x0)
if_r_2_in_3_gg1(x0)
if_p_2_in_2_gg3(x0, x1, x2)
if_p_2_in_3_gg1(x0)
if_q_2_in_2_gg2(x0, x1)
if_q_2_in_3_gg1(x0)

We have to consider all (P,Q,R)-chains.
The head symbols of this DP problem are {R_2_IN_GG2, IF_R_2_IN_2_GG3, P_2_IN_GG2, Q_2_IN_GG2, IF_Q_2_IN_2_GG2, T_2_IN_GG2, IF_P_2_IN_2_GG3}.
By using a polynomial ordering, the following set of Dependency Pairs of this DP problem can be strictly oriented.

R_2_IN_GG2(X, f_11(Y)) -> IF_R_2_IN_2_GG3(X, Y, q_2_in_gg2(X, Y))
Q_2_IN_GG2(X, f_11(f_11(Y))) -> P_2_IN_GG2(X, f_11(Y))
P_2_IN_GG2(X, f_11(Y)) -> IF_P_2_IN_2_GG3(X, Y, r_2_in_gg2(X, f_11(Y)))
R_2_IN_GG2(X, f_11(Y)) -> Q_2_IN_GG2(X, Y)
Q_2_IN_GG2(X, f_11(f_11(X))) -> IF_Q_2_IN_2_GG2(X, p_2_in_gg2(X, f_11(f_11(X))))
The remaining Dependency Pairs were at least non-strictly be oriented.

IF_R_2_IN_2_GG3(X, Y, q_2_out_gg) -> R_2_IN_GG2(X, Y)
P_2_IN_GG2(X, f_11(Y)) -> R_2_IN_GG2(X, f_11(Y))
IF_Q_2_IN_2_GG2(X, p_2_out_gg) -> Q_2_IN_GG2(X, f_11(X))
R_2_IN_GG2(f_11(X), f_11(X)) -> T_2_IN_GG2(f_11(X), f_11(X))
IF_P_2_IN_2_GG3(X, Y, r_2_out_gg) -> P_2_IN_GG2(X, Y)
Q_2_IN_GG2(X, f_11(f_11(X))) -> P_2_IN_GG2(X, f_11(f_11(X)))
T_2_IN_GG2(f_11(X), f_11(Y)) -> Q_2_IN_GG2(f_11(X), f_11(Y))
With the implicit AFS there is no usable rule.

Used ordering: POLO with Polynomial interpretation:


POL(a_0) = 0   
POL(Q_2_IN_GG2(x1, x2)) = x2   
POL(if_t_2_in_1_gg1(x1)) = 0   
POL(if_q_2_in_3_gg1(x1)) = 0   
POL(if_p_2_in_1_gg1(x1)) = 0   
POL(T_2_IN_GG2(x1, x2)) = x2   
POL(IF_P_2_IN_2_GG3(x1, x2, x3)) = x2   
POL(if_q_2_in_2_gg2(x1, x2)) = 0   
POL(r_2_out_gg) = 0   
POL(e_2_out_gg) = 0   
POL(if_q_2_in_4_gg1(x1)) = 0   
POL(p_2_out_gg) = 0   
POL(R_2_IN_GG2(x1, x2)) = x2   
POL(if_r_2_in_3_gg1(x1)) = 0   
POL(f_11(x1)) = 1 + x1   
POL(IF_R_2_IN_2_GG3(x1, x2, x3)) = x2   
POL(if_r_2_in_4_gg1(x1)) = 0   
POL(t_2_out_gg) = 0   
POL(q_2_in_gg2(x1, x2)) = 0   
POL(if_p_2_in_2_gg3(x1, x2, x3)) = 0   
POL(IF_Q_2_IN_2_GG2(x1, x2)) = 1 + x1   
POL(b_0) = 0   
POL(if_t_2_in_2_gg3(x1, x2, x3)) = 0   
POL(if_q_2_in_1_gg1(x1)) = 0   
POL(if_p_2_in_3_gg1(x1)) = 0   
POL(r_2_in_gg2(x1, x2)) = 0   
POL(P_2_IN_GG2(x1, x2)) = x2   
POL(if_r_2_in_2_gg3(x1, x2, x3)) = 0   
POL(if_r_2_in_1_gg1(x1)) = 0   
POL(q_2_out_gg) = 0   
POL(if_t_2_in_3_gg1(x1)) = 0   
POL(e_2_in_gg2(x1, x2)) = 0   
POL(t_2_in_gg2(x1, x2)) = 0   
POL(p_2_in_gg2(x1, x2)) = 0   



↳ PROLOG
  ↳ PrologToPiTRSProof
    ↳ PiTRS
      ↳ DependencyPairsProof
        ↳ PiDP
          ↳ DependencyGraphProof
            ↳ PiDP
              ↳ PiDPToQDPProof
                ↳ QDP
                  ↳ QDPPoloProof
                    ↳ QDP
                      ↳ DependencyGraphProof
                        ↳ QDP
                          ↳ QDPPoloProof
                            ↳ QDP
                              ↳ DependencyGraphProof

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

IF_R_2_IN_2_GG3(X, Y, q_2_out_gg) -> R_2_IN_GG2(X, Y)
P_2_IN_GG2(X, f_11(Y)) -> R_2_IN_GG2(X, f_11(Y))
IF_Q_2_IN_2_GG2(X, p_2_out_gg) -> Q_2_IN_GG2(X, f_11(X))
R_2_IN_GG2(f_11(X), f_11(X)) -> T_2_IN_GG2(f_11(X), f_11(X))
IF_P_2_IN_2_GG3(X, Y, r_2_out_gg) -> P_2_IN_GG2(X, Y)
Q_2_IN_GG2(X, f_11(f_11(X))) -> P_2_IN_GG2(X, f_11(f_11(X)))
T_2_IN_GG2(f_11(X), f_11(Y)) -> Q_2_IN_GG2(f_11(X), f_11(Y))

The TRS R consists of the following rules:

q_2_in_gg2(X, Y) -> if_q_2_in_1_gg1(e_2_in_gg2(X, Y))
e_2_in_gg2(a_0, b_0) -> e_2_out_gg
if_q_2_in_1_gg1(e_2_out_gg) -> q_2_out_gg
q_2_in_gg2(X, f_11(f_11(X))) -> if_q_2_in_2_gg2(X, p_2_in_gg2(X, f_11(f_11(X))))
p_2_in_gg2(X, Y) -> if_p_2_in_1_gg1(e_2_in_gg2(X, Y))
if_p_2_in_1_gg1(e_2_out_gg) -> p_2_out_gg
p_2_in_gg2(X, f_11(Y)) -> if_p_2_in_2_gg3(X, Y, r_2_in_gg2(X, f_11(Y)))
r_2_in_gg2(X, Y) -> if_r_2_in_1_gg1(e_2_in_gg2(X, Y))
if_r_2_in_1_gg1(e_2_out_gg) -> r_2_out_gg
r_2_in_gg2(X, f_11(Y)) -> if_r_2_in_2_gg3(X, Y, q_2_in_gg2(X, Y))
q_2_in_gg2(X, f_11(f_11(Y))) -> if_q_2_in_4_gg1(p_2_in_gg2(X, f_11(Y)))
if_q_2_in_4_gg1(p_2_out_gg) -> q_2_out_gg
if_r_2_in_2_gg3(X, Y, q_2_out_gg) -> if_r_2_in_3_gg1(r_2_in_gg2(X, Y))
r_2_in_gg2(f_11(X), f_11(X)) -> if_r_2_in_4_gg1(t_2_in_gg2(f_11(X), f_11(X)))
t_2_in_gg2(X, Y) -> if_t_2_in_1_gg1(e_2_in_gg2(X, Y))
if_t_2_in_1_gg1(e_2_out_gg) -> t_2_out_gg
t_2_in_gg2(f_11(X), f_11(Y)) -> if_t_2_in_2_gg3(X, Y, q_2_in_gg2(f_11(X), f_11(Y)))
if_t_2_in_2_gg3(X, Y, q_2_out_gg) -> if_t_2_in_3_gg1(t_2_in_gg2(X, Y))
if_t_2_in_3_gg1(t_2_out_gg) -> t_2_out_gg
if_r_2_in_4_gg1(t_2_out_gg) -> r_2_out_gg
if_r_2_in_3_gg1(r_2_out_gg) -> r_2_out_gg
if_p_2_in_2_gg3(X, Y, r_2_out_gg) -> if_p_2_in_3_gg1(p_2_in_gg2(X, Y))
if_p_2_in_3_gg1(p_2_out_gg) -> p_2_out_gg
if_q_2_in_2_gg2(X, p_2_out_gg) -> if_q_2_in_3_gg1(q_2_in_gg2(X, f_11(X)))
if_q_2_in_3_gg1(q_2_out_gg) -> q_2_out_gg

The set Q consists of the following terms:

q_2_in_gg2(x0, x1)
e_2_in_gg2(x0, x1)
if_q_2_in_1_gg1(x0)
p_2_in_gg2(x0, x1)
if_p_2_in_1_gg1(x0)
r_2_in_gg2(x0, x1)
if_r_2_in_1_gg1(x0)
if_q_2_in_4_gg1(x0)
if_r_2_in_2_gg3(x0, x1, x2)
t_2_in_gg2(x0, x1)
if_t_2_in_1_gg1(x0)
if_t_2_in_2_gg3(x0, x1, x2)
if_t_2_in_3_gg1(x0)
if_r_2_in_4_gg1(x0)
if_r_2_in_3_gg1(x0)
if_p_2_in_2_gg3(x0, x1, x2)
if_p_2_in_3_gg1(x0)
if_q_2_in_2_gg2(x0, x1)
if_q_2_in_3_gg1(x0)

We have to consider all (P,Q,R)-chains.
The head symbols of this DP problem are {R_2_IN_GG2, IF_R_2_IN_2_GG3, P_2_IN_GG2, Q_2_IN_GG2, IF_Q_2_IN_2_GG2, T_2_IN_GG2, IF_P_2_IN_2_GG3}.
The approximation of the Dependency Graph contains 1 SCC with 3 less nodes.

↳ PROLOG
  ↳ PrologToPiTRSProof
    ↳ PiTRS
      ↳ DependencyPairsProof
        ↳ PiDP
          ↳ DependencyGraphProof
            ↳ PiDP
              ↳ PiDPToQDPProof
                ↳ QDP
                  ↳ QDPPoloProof
                    ↳ QDP
                      ↳ DependencyGraphProof
                        ↳ QDP
                          ↳ QDPPoloProof
                            ↳ QDP
                              ↳ DependencyGraphProof
                                ↳ QDP
                                  ↳ QDPSizeChangeProof

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

P_2_IN_GG2(X, f_11(Y)) -> R_2_IN_GG2(X, f_11(Y))
R_2_IN_GG2(f_11(X), f_11(X)) -> T_2_IN_GG2(f_11(X), f_11(X))
Q_2_IN_GG2(X, f_11(f_11(X))) -> P_2_IN_GG2(X, f_11(f_11(X)))
T_2_IN_GG2(f_11(X), f_11(Y)) -> Q_2_IN_GG2(f_11(X), f_11(Y))

The TRS R consists of the following rules:

q_2_in_gg2(X, Y) -> if_q_2_in_1_gg1(e_2_in_gg2(X, Y))
e_2_in_gg2(a_0, b_0) -> e_2_out_gg
if_q_2_in_1_gg1(e_2_out_gg) -> q_2_out_gg
q_2_in_gg2(X, f_11(f_11(X))) -> if_q_2_in_2_gg2(X, p_2_in_gg2(X, f_11(f_11(X))))
p_2_in_gg2(X, Y) -> if_p_2_in_1_gg1(e_2_in_gg2(X, Y))
if_p_2_in_1_gg1(e_2_out_gg) -> p_2_out_gg
p_2_in_gg2(X, f_11(Y)) -> if_p_2_in_2_gg3(X, Y, r_2_in_gg2(X, f_11(Y)))
r_2_in_gg2(X, Y) -> if_r_2_in_1_gg1(e_2_in_gg2(X, Y))
if_r_2_in_1_gg1(e_2_out_gg) -> r_2_out_gg
r_2_in_gg2(X, f_11(Y)) -> if_r_2_in_2_gg3(X, Y, q_2_in_gg2(X, Y))
q_2_in_gg2(X, f_11(f_11(Y))) -> if_q_2_in_4_gg1(p_2_in_gg2(X, f_11(Y)))
if_q_2_in_4_gg1(p_2_out_gg) -> q_2_out_gg
if_r_2_in_2_gg3(X, Y, q_2_out_gg) -> if_r_2_in_3_gg1(r_2_in_gg2(X, Y))
r_2_in_gg2(f_11(X), f_11(X)) -> if_r_2_in_4_gg1(t_2_in_gg2(f_11(X), f_11(X)))
t_2_in_gg2(X, Y) -> if_t_2_in_1_gg1(e_2_in_gg2(X, Y))
if_t_2_in_1_gg1(e_2_out_gg) -> t_2_out_gg
t_2_in_gg2(f_11(X), f_11(Y)) -> if_t_2_in_2_gg3(X, Y, q_2_in_gg2(f_11(X), f_11(Y)))
if_t_2_in_2_gg3(X, Y, q_2_out_gg) -> if_t_2_in_3_gg1(t_2_in_gg2(X, Y))
if_t_2_in_3_gg1(t_2_out_gg) -> t_2_out_gg
if_r_2_in_4_gg1(t_2_out_gg) -> r_2_out_gg
if_r_2_in_3_gg1(r_2_out_gg) -> r_2_out_gg
if_p_2_in_2_gg3(X, Y, r_2_out_gg) -> if_p_2_in_3_gg1(p_2_in_gg2(X, Y))
if_p_2_in_3_gg1(p_2_out_gg) -> p_2_out_gg
if_q_2_in_2_gg2(X, p_2_out_gg) -> if_q_2_in_3_gg1(q_2_in_gg2(X, f_11(X)))
if_q_2_in_3_gg1(q_2_out_gg) -> q_2_out_gg

The set Q consists of the following terms:

q_2_in_gg2(x0, x1)
e_2_in_gg2(x0, x1)
if_q_2_in_1_gg1(x0)
p_2_in_gg2(x0, x1)
if_p_2_in_1_gg1(x0)
r_2_in_gg2(x0, x1)
if_r_2_in_1_gg1(x0)
if_q_2_in_4_gg1(x0)
if_r_2_in_2_gg3(x0, x1, x2)
t_2_in_gg2(x0, x1)
if_t_2_in_1_gg1(x0)
if_t_2_in_2_gg3(x0, x1, x2)
if_t_2_in_3_gg1(x0)
if_r_2_in_4_gg1(x0)
if_r_2_in_3_gg1(x0)
if_p_2_in_2_gg3(x0, x1, x2)
if_p_2_in_3_gg1(x0)
if_q_2_in_2_gg2(x0, x1)
if_q_2_in_3_gg1(x0)

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