YES Left Termination proof of ../tpdb/LP/talp/talp/vangelder.pl
Left Termination of the query pattern q_in_2(g, g) w.r.t. the given Prolog program could successfully be proven:



↳ Prolog
  ↳ PrologToPiTRSProof

Clauses:

e(a, b).
q(X, Y) :- e(X, Y).
q(X, f(f(X))) :- ','(p(X, f(f(X))), q(X, f(X))).
q(X, f(f(Y))) :- p(X, f(Y)).
p(X, Y) :- e(X, Y).
p(X, f(Y)) :- ','(r(X, f(Y)), p(X, Y)).
r(X, Y) :- e(X, Y).
r(X, f(Y)) :- ','(q(X, Y), r(X, Y)).
r(f(X), f(X)) :- t(f(X), f(X)).
t(X, Y) :- e(X, Y).
t(f(X), f(Y)) :- ','(q(f(X), f(Y)), t(X, Y)).

Queries:

q(g,g).

We use the technique of [30]. With regard to the inferred argument filtering the predicates were used in the following modes:
q_in: (b,b)
p_in: (b,b)
r_in: (b,b)
t_in: (b,b)
Transforming Prolog into the following Term Rewriting System:
Pi-finite rewrite system:
The TRS R consists of the following rules:

q_in_gg(X, Y) → U1_gg(X, Y, e_in_gg(X, Y))
e_in_gg(a, b) → e_out_gg(a, b)
U1_gg(X, Y, e_out_gg(X, Y)) → q_out_gg(X, Y)
q_in_gg(X, f(f(X))) → U2_gg(X, p_in_gg(X, f(f(X))))
p_in_gg(X, Y) → U5_gg(X, Y, e_in_gg(X, Y))
U5_gg(X, Y, e_out_gg(X, Y)) → p_out_gg(X, Y)
p_in_gg(X, f(Y)) → U6_gg(X, Y, r_in_gg(X, f(Y)))
r_in_gg(X, Y) → U8_gg(X, Y, e_in_gg(X, Y))
U8_gg(X, Y, e_out_gg(X, Y)) → r_out_gg(X, Y)
r_in_gg(X, f(Y)) → U9_gg(X, Y, q_in_gg(X, Y))
q_in_gg(X, f(f(Y))) → U4_gg(X, Y, p_in_gg(X, f(Y)))
U4_gg(X, Y, p_out_gg(X, f(Y))) → q_out_gg(X, f(f(Y)))
U9_gg(X, Y, q_out_gg(X, Y)) → U10_gg(X, Y, r_in_gg(X, Y))
r_in_gg(f(X), f(X)) → U11_gg(X, t_in_gg(f(X), f(X)))
t_in_gg(X, Y) → U12_gg(X, Y, e_in_gg(X, Y))
U12_gg(X, Y, e_out_gg(X, Y)) → t_out_gg(X, Y)
t_in_gg(f(X), f(Y)) → U13_gg(X, Y, q_in_gg(f(X), f(Y)))
U13_gg(X, Y, q_out_gg(f(X), f(Y))) → U14_gg(X, Y, t_in_gg(X, Y))
U14_gg(X, Y, t_out_gg(X, Y)) → t_out_gg(f(X), f(Y))
U11_gg(X, t_out_gg(f(X), f(X))) → r_out_gg(f(X), f(X))
U10_gg(X, Y, r_out_gg(X, Y)) → r_out_gg(X, f(Y))
U6_gg(X, Y, r_out_gg(X, f(Y))) → U7_gg(X, Y, p_in_gg(X, Y))
U7_gg(X, Y, p_out_gg(X, Y)) → p_out_gg(X, f(Y))
U2_gg(X, p_out_gg(X, f(f(X)))) → U3_gg(X, q_in_gg(X, f(X)))
U3_gg(X, q_out_gg(X, f(X))) → q_out_gg(X, f(f(X)))

The argument filtering Pi contains the following mapping:
q_in_gg(x1, x2)  =  q_in_gg(x1, x2)
U1_gg(x1, x2, x3)  =  U1_gg(x3)
e_in_gg(x1, x2)  =  e_in_gg(x1, x2)
a  =  a
b  =  b
e_out_gg(x1, x2)  =  e_out_gg
q_out_gg(x1, x2)  =  q_out_gg
f(x1)  =  f(x1)
U2_gg(x1, x2)  =  U2_gg(x1, x2)
p_in_gg(x1, x2)  =  p_in_gg(x1, x2)
U5_gg(x1, x2, x3)  =  U5_gg(x3)
p_out_gg(x1, x2)  =  p_out_gg
U6_gg(x1, x2, x3)  =  U6_gg(x1, x2, x3)
r_in_gg(x1, x2)  =  r_in_gg(x1, x2)
U8_gg(x1, x2, x3)  =  U8_gg(x3)
r_out_gg(x1, x2)  =  r_out_gg
U9_gg(x1, x2, x3)  =  U9_gg(x1, x2, x3)
U4_gg(x1, x2, x3)  =  U4_gg(x3)
U10_gg(x1, x2, x3)  =  U10_gg(x3)
U11_gg(x1, x2)  =  U11_gg(x2)
t_in_gg(x1, x2)  =  t_in_gg(x1, x2)
U12_gg(x1, x2, x3)  =  U12_gg(x3)
t_out_gg(x1, x2)  =  t_out_gg
U13_gg(x1, x2, x3)  =  U13_gg(x1, x2, x3)
U14_gg(x1, x2, x3)  =  U14_gg(x3)
U7_gg(x1, x2, x3)  =  U7_gg(x3)
U3_gg(x1, x2)  =  U3_gg(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_in_gg(X, Y) → U1_gg(X, Y, e_in_gg(X, Y))
e_in_gg(a, b) → e_out_gg(a, b)
U1_gg(X, Y, e_out_gg(X, Y)) → q_out_gg(X, Y)
q_in_gg(X, f(f(X))) → U2_gg(X, p_in_gg(X, f(f(X))))
p_in_gg(X, Y) → U5_gg(X, Y, e_in_gg(X, Y))
U5_gg(X, Y, e_out_gg(X, Y)) → p_out_gg(X, Y)
p_in_gg(X, f(Y)) → U6_gg(X, Y, r_in_gg(X, f(Y)))
r_in_gg(X, Y) → U8_gg(X, Y, e_in_gg(X, Y))
U8_gg(X, Y, e_out_gg(X, Y)) → r_out_gg(X, Y)
r_in_gg(X, f(Y)) → U9_gg(X, Y, q_in_gg(X, Y))
q_in_gg(X, f(f(Y))) → U4_gg(X, Y, p_in_gg(X, f(Y)))
U4_gg(X, Y, p_out_gg(X, f(Y))) → q_out_gg(X, f(f(Y)))
U9_gg(X, Y, q_out_gg(X, Y)) → U10_gg(X, Y, r_in_gg(X, Y))
r_in_gg(f(X), f(X)) → U11_gg(X, t_in_gg(f(X), f(X)))
t_in_gg(X, Y) → U12_gg(X, Y, e_in_gg(X, Y))
U12_gg(X, Y, e_out_gg(X, Y)) → t_out_gg(X, Y)
t_in_gg(f(X), f(Y)) → U13_gg(X, Y, q_in_gg(f(X), f(Y)))
U13_gg(X, Y, q_out_gg(f(X), f(Y))) → U14_gg(X, Y, t_in_gg(X, Y))
U14_gg(X, Y, t_out_gg(X, Y)) → t_out_gg(f(X), f(Y))
U11_gg(X, t_out_gg(f(X), f(X))) → r_out_gg(f(X), f(X))
U10_gg(X, Y, r_out_gg(X, Y)) → r_out_gg(X, f(Y))
U6_gg(X, Y, r_out_gg(X, f(Y))) → U7_gg(X, Y, p_in_gg(X, Y))
U7_gg(X, Y, p_out_gg(X, Y)) → p_out_gg(X, f(Y))
U2_gg(X, p_out_gg(X, f(f(X)))) → U3_gg(X, q_in_gg(X, f(X)))
U3_gg(X, q_out_gg(X, f(X))) → q_out_gg(X, f(f(X)))

The argument filtering Pi contains the following mapping:
q_in_gg(x1, x2)  =  q_in_gg(x1, x2)
U1_gg(x1, x2, x3)  =  U1_gg(x3)
e_in_gg(x1, x2)  =  e_in_gg(x1, x2)
a  =  a
b  =  b
e_out_gg(x1, x2)  =  e_out_gg
q_out_gg(x1, x2)  =  q_out_gg
f(x1)  =  f(x1)
U2_gg(x1, x2)  =  U2_gg(x1, x2)
p_in_gg(x1, x2)  =  p_in_gg(x1, x2)
U5_gg(x1, x2, x3)  =  U5_gg(x3)
p_out_gg(x1, x2)  =  p_out_gg
U6_gg(x1, x2, x3)  =  U6_gg(x1, x2, x3)
r_in_gg(x1, x2)  =  r_in_gg(x1, x2)
U8_gg(x1, x2, x3)  =  U8_gg(x3)
r_out_gg(x1, x2)  =  r_out_gg
U9_gg(x1, x2, x3)  =  U9_gg(x1, x2, x3)
U4_gg(x1, x2, x3)  =  U4_gg(x3)
U10_gg(x1, x2, x3)  =  U10_gg(x3)
U11_gg(x1, x2)  =  U11_gg(x2)
t_in_gg(x1, x2)  =  t_in_gg(x1, x2)
U12_gg(x1, x2, x3)  =  U12_gg(x3)
t_out_gg(x1, x2)  =  t_out_gg
U13_gg(x1, x2, x3)  =  U13_gg(x1, x2, x3)
U14_gg(x1, x2, x3)  =  U14_gg(x3)
U7_gg(x1, x2, x3)  =  U7_gg(x3)
U3_gg(x1, x2)  =  U3_gg(x2)


Using Dependency Pairs [1,30] we result in the following initial DP problem:
Pi DP problem:
The TRS P consists of the following rules:

Q_IN_GG(X, Y) → U1_GG(X, Y, e_in_gg(X, Y))
Q_IN_GG(X, Y) → E_IN_GG(X, Y)
Q_IN_GG(X, f(f(X))) → U2_GG(X, p_in_gg(X, f(f(X))))
Q_IN_GG(X, f(f(X))) → P_IN_GG(X, f(f(X)))
P_IN_GG(X, Y) → U5_GG(X, Y, e_in_gg(X, Y))
P_IN_GG(X, Y) → E_IN_GG(X, Y)
P_IN_GG(X, f(Y)) → U6_GG(X, Y, r_in_gg(X, f(Y)))
P_IN_GG(X, f(Y)) → R_IN_GG(X, f(Y))
R_IN_GG(X, Y) → U8_GG(X, Y, e_in_gg(X, Y))
R_IN_GG(X, Y) → E_IN_GG(X, Y)
R_IN_GG(X, f(Y)) → U9_GG(X, Y, q_in_gg(X, Y))
R_IN_GG(X, f(Y)) → Q_IN_GG(X, Y)
Q_IN_GG(X, f(f(Y))) → U4_GG(X, Y, p_in_gg(X, f(Y)))
Q_IN_GG(X, f(f(Y))) → P_IN_GG(X, f(Y))
U9_GG(X, Y, q_out_gg(X, Y)) → U10_GG(X, Y, r_in_gg(X, Y))
U9_GG(X, Y, q_out_gg(X, Y)) → R_IN_GG(X, Y)
R_IN_GG(f(X), f(X)) → U11_GG(X, t_in_gg(f(X), f(X)))
R_IN_GG(f(X), f(X)) → T_IN_GG(f(X), f(X))
T_IN_GG(X, Y) → U12_GG(X, Y, e_in_gg(X, Y))
T_IN_GG(X, Y) → E_IN_GG(X, Y)
T_IN_GG(f(X), f(Y)) → U13_GG(X, Y, q_in_gg(f(X), f(Y)))
T_IN_GG(f(X), f(Y)) → Q_IN_GG(f(X), f(Y))
U13_GG(X, Y, q_out_gg(f(X), f(Y))) → U14_GG(X, Y, t_in_gg(X, Y))
U13_GG(X, Y, q_out_gg(f(X), f(Y))) → T_IN_GG(X, Y)
U6_GG(X, Y, r_out_gg(X, f(Y))) → U7_GG(X, Y, p_in_gg(X, Y))
U6_GG(X, Y, r_out_gg(X, f(Y))) → P_IN_GG(X, Y)
U2_GG(X, p_out_gg(X, f(f(X)))) → U3_GG(X, q_in_gg(X, f(X)))
U2_GG(X, p_out_gg(X, f(f(X)))) → Q_IN_GG(X, f(X))

The TRS R consists of the following rules:

q_in_gg(X, Y) → U1_gg(X, Y, e_in_gg(X, Y))
e_in_gg(a, b) → e_out_gg(a, b)
U1_gg(X, Y, e_out_gg(X, Y)) → q_out_gg(X, Y)
q_in_gg(X, f(f(X))) → U2_gg(X, p_in_gg(X, f(f(X))))
p_in_gg(X, Y) → U5_gg(X, Y, e_in_gg(X, Y))
U5_gg(X, Y, e_out_gg(X, Y)) → p_out_gg(X, Y)
p_in_gg(X, f(Y)) → U6_gg(X, Y, r_in_gg(X, f(Y)))
r_in_gg(X, Y) → U8_gg(X, Y, e_in_gg(X, Y))
U8_gg(X, Y, e_out_gg(X, Y)) → r_out_gg(X, Y)
r_in_gg(X, f(Y)) → U9_gg(X, Y, q_in_gg(X, Y))
q_in_gg(X, f(f(Y))) → U4_gg(X, Y, p_in_gg(X, f(Y)))
U4_gg(X, Y, p_out_gg(X, f(Y))) → q_out_gg(X, f(f(Y)))
U9_gg(X, Y, q_out_gg(X, Y)) → U10_gg(X, Y, r_in_gg(X, Y))
r_in_gg(f(X), f(X)) → U11_gg(X, t_in_gg(f(X), f(X)))
t_in_gg(X, Y) → U12_gg(X, Y, e_in_gg(X, Y))
U12_gg(X, Y, e_out_gg(X, Y)) → t_out_gg(X, Y)
t_in_gg(f(X), f(Y)) → U13_gg(X, Y, q_in_gg(f(X), f(Y)))
U13_gg(X, Y, q_out_gg(f(X), f(Y))) → U14_gg(X, Y, t_in_gg(X, Y))
U14_gg(X, Y, t_out_gg(X, Y)) → t_out_gg(f(X), f(Y))
U11_gg(X, t_out_gg(f(X), f(X))) → r_out_gg(f(X), f(X))
U10_gg(X, Y, r_out_gg(X, Y)) → r_out_gg(X, f(Y))
U6_gg(X, Y, r_out_gg(X, f(Y))) → U7_gg(X, Y, p_in_gg(X, Y))
U7_gg(X, Y, p_out_gg(X, Y)) → p_out_gg(X, f(Y))
U2_gg(X, p_out_gg(X, f(f(X)))) → U3_gg(X, q_in_gg(X, f(X)))
U3_gg(X, q_out_gg(X, f(X))) → q_out_gg(X, f(f(X)))

The argument filtering Pi contains the following mapping:
q_in_gg(x1, x2)  =  q_in_gg(x1, x2)
U1_gg(x1, x2, x3)  =  U1_gg(x3)
e_in_gg(x1, x2)  =  e_in_gg(x1, x2)
a  =  a
b  =  b
e_out_gg(x1, x2)  =  e_out_gg
q_out_gg(x1, x2)  =  q_out_gg
f(x1)  =  f(x1)
U2_gg(x1, x2)  =  U2_gg(x1, x2)
p_in_gg(x1, x2)  =  p_in_gg(x1, x2)
U5_gg(x1, x2, x3)  =  U5_gg(x3)
p_out_gg(x1, x2)  =  p_out_gg
U6_gg(x1, x2, x3)  =  U6_gg(x1, x2, x3)
r_in_gg(x1, x2)  =  r_in_gg(x1, x2)
U8_gg(x1, x2, x3)  =  U8_gg(x3)
r_out_gg(x1, x2)  =  r_out_gg
U9_gg(x1, x2, x3)  =  U9_gg(x1, x2, x3)
U4_gg(x1, x2, x3)  =  U4_gg(x3)
U10_gg(x1, x2, x3)  =  U10_gg(x3)
U11_gg(x1, x2)  =  U11_gg(x2)
t_in_gg(x1, x2)  =  t_in_gg(x1, x2)
U12_gg(x1, x2, x3)  =  U12_gg(x3)
t_out_gg(x1, x2)  =  t_out_gg
U13_gg(x1, x2, x3)  =  U13_gg(x1, x2, x3)
U14_gg(x1, x2, x3)  =  U14_gg(x3)
U7_gg(x1, x2, x3)  =  U7_gg(x3)
U3_gg(x1, x2)  =  U3_gg(x2)
U5_GG(x1, x2, x3)  =  U5_GG(x3)
U4_GG(x1, x2, x3)  =  U4_GG(x3)
R_IN_GG(x1, x2)  =  R_IN_GG(x1, x2)
U11_GG(x1, x2)  =  U11_GG(x2)
P_IN_GG(x1, x2)  =  P_IN_GG(x1, x2)
Q_IN_GG(x1, x2)  =  Q_IN_GG(x1, x2)
U2_GG(x1, x2)  =  U2_GG(x1, x2)
U3_GG(x1, x2)  =  U3_GG(x2)
U12_GG(x1, x2, x3)  =  U12_GG(x3)
E_IN_GG(x1, x2)  =  E_IN_GG(x1, x2)
U6_GG(x1, x2, x3)  =  U6_GG(x1, x2, x3)
U13_GG(x1, x2, x3)  =  U13_GG(x1, x2, x3)
U1_GG(x1, x2, x3)  =  U1_GG(x3)
U9_GG(x1, x2, x3)  =  U9_GG(x1, x2, x3)
U10_GG(x1, x2, x3)  =  U10_GG(x3)
U14_GG(x1, x2, x3)  =  U14_GG(x3)
T_IN_GG(x1, x2)  =  T_IN_GG(x1, x2)
U7_GG(x1, x2, x3)  =  U7_GG(x3)
U8_GG(x1, x2, x3)  =  U8_GG(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:

Q_IN_GG(X, Y) → U1_GG(X, Y, e_in_gg(X, Y))
Q_IN_GG(X, Y) → E_IN_GG(X, Y)
Q_IN_GG(X, f(f(X))) → U2_GG(X, p_in_gg(X, f(f(X))))
Q_IN_GG(X, f(f(X))) → P_IN_GG(X, f(f(X)))
P_IN_GG(X, Y) → U5_GG(X, Y, e_in_gg(X, Y))
P_IN_GG(X, Y) → E_IN_GG(X, Y)
P_IN_GG(X, f(Y)) → U6_GG(X, Y, r_in_gg(X, f(Y)))
P_IN_GG(X, f(Y)) → R_IN_GG(X, f(Y))
R_IN_GG(X, Y) → U8_GG(X, Y, e_in_gg(X, Y))
R_IN_GG(X, Y) → E_IN_GG(X, Y)
R_IN_GG(X, f(Y)) → U9_GG(X, Y, q_in_gg(X, Y))
R_IN_GG(X, f(Y)) → Q_IN_GG(X, Y)
Q_IN_GG(X, f(f(Y))) → U4_GG(X, Y, p_in_gg(X, f(Y)))
Q_IN_GG(X, f(f(Y))) → P_IN_GG(X, f(Y))
U9_GG(X, Y, q_out_gg(X, Y)) → U10_GG(X, Y, r_in_gg(X, Y))
U9_GG(X, Y, q_out_gg(X, Y)) → R_IN_GG(X, Y)
R_IN_GG(f(X), f(X)) → U11_GG(X, t_in_gg(f(X), f(X)))
R_IN_GG(f(X), f(X)) → T_IN_GG(f(X), f(X))
T_IN_GG(X, Y) → U12_GG(X, Y, e_in_gg(X, Y))
T_IN_GG(X, Y) → E_IN_GG(X, Y)
T_IN_GG(f(X), f(Y)) → U13_GG(X, Y, q_in_gg(f(X), f(Y)))
T_IN_GG(f(X), f(Y)) → Q_IN_GG(f(X), f(Y))
U13_GG(X, Y, q_out_gg(f(X), f(Y))) → U14_GG(X, Y, t_in_gg(X, Y))
U13_GG(X, Y, q_out_gg(f(X), f(Y))) → T_IN_GG(X, Y)
U6_GG(X, Y, r_out_gg(X, f(Y))) → U7_GG(X, Y, p_in_gg(X, Y))
U6_GG(X, Y, r_out_gg(X, f(Y))) → P_IN_GG(X, Y)
U2_GG(X, p_out_gg(X, f(f(X)))) → U3_GG(X, q_in_gg(X, f(X)))
U2_GG(X, p_out_gg(X, f(f(X)))) → Q_IN_GG(X, f(X))

The TRS R consists of the following rules:

q_in_gg(X, Y) → U1_gg(X, Y, e_in_gg(X, Y))
e_in_gg(a, b) → e_out_gg(a, b)
U1_gg(X, Y, e_out_gg(X, Y)) → q_out_gg(X, Y)
q_in_gg(X, f(f(X))) → U2_gg(X, p_in_gg(X, f(f(X))))
p_in_gg(X, Y) → U5_gg(X, Y, e_in_gg(X, Y))
U5_gg(X, Y, e_out_gg(X, Y)) → p_out_gg(X, Y)
p_in_gg(X, f(Y)) → U6_gg(X, Y, r_in_gg(X, f(Y)))
r_in_gg(X, Y) → U8_gg(X, Y, e_in_gg(X, Y))
U8_gg(X, Y, e_out_gg(X, Y)) → r_out_gg(X, Y)
r_in_gg(X, f(Y)) → U9_gg(X, Y, q_in_gg(X, Y))
q_in_gg(X, f(f(Y))) → U4_gg(X, Y, p_in_gg(X, f(Y)))
U4_gg(X, Y, p_out_gg(X, f(Y))) → q_out_gg(X, f(f(Y)))
U9_gg(X, Y, q_out_gg(X, Y)) → U10_gg(X, Y, r_in_gg(X, Y))
r_in_gg(f(X), f(X)) → U11_gg(X, t_in_gg(f(X), f(X)))
t_in_gg(X, Y) → U12_gg(X, Y, e_in_gg(X, Y))
U12_gg(X, Y, e_out_gg(X, Y)) → t_out_gg(X, Y)
t_in_gg(f(X), f(Y)) → U13_gg(X, Y, q_in_gg(f(X), f(Y)))
U13_gg(X, Y, q_out_gg(f(X), f(Y))) → U14_gg(X, Y, t_in_gg(X, Y))
U14_gg(X, Y, t_out_gg(X, Y)) → t_out_gg(f(X), f(Y))
U11_gg(X, t_out_gg(f(X), f(X))) → r_out_gg(f(X), f(X))
U10_gg(X, Y, r_out_gg(X, Y)) → r_out_gg(X, f(Y))
U6_gg(X, Y, r_out_gg(X, f(Y))) → U7_gg(X, Y, p_in_gg(X, Y))
U7_gg(X, Y, p_out_gg(X, Y)) → p_out_gg(X, f(Y))
U2_gg(X, p_out_gg(X, f(f(X)))) → U3_gg(X, q_in_gg(X, f(X)))
U3_gg(X, q_out_gg(X, f(X))) → q_out_gg(X, f(f(X)))

The argument filtering Pi contains the following mapping:
q_in_gg(x1, x2)  =  q_in_gg(x1, x2)
U1_gg(x1, x2, x3)  =  U1_gg(x3)
e_in_gg(x1, x2)  =  e_in_gg(x1, x2)
a  =  a
b  =  b
e_out_gg(x1, x2)  =  e_out_gg
q_out_gg(x1, x2)  =  q_out_gg
f(x1)  =  f(x1)
U2_gg(x1, x2)  =  U2_gg(x1, x2)
p_in_gg(x1, x2)  =  p_in_gg(x1, x2)
U5_gg(x1, x2, x3)  =  U5_gg(x3)
p_out_gg(x1, x2)  =  p_out_gg
U6_gg(x1, x2, x3)  =  U6_gg(x1, x2, x3)
r_in_gg(x1, x2)  =  r_in_gg(x1, x2)
U8_gg(x1, x2, x3)  =  U8_gg(x3)
r_out_gg(x1, x2)  =  r_out_gg
U9_gg(x1, x2, x3)  =  U9_gg(x1, x2, x3)
U4_gg(x1, x2, x3)  =  U4_gg(x3)
U10_gg(x1, x2, x3)  =  U10_gg(x3)
U11_gg(x1, x2)  =  U11_gg(x2)
t_in_gg(x1, x2)  =  t_in_gg(x1, x2)
U12_gg(x1, x2, x3)  =  U12_gg(x3)
t_out_gg(x1, x2)  =  t_out_gg
U13_gg(x1, x2, x3)  =  U13_gg(x1, x2, x3)
U14_gg(x1, x2, x3)  =  U14_gg(x3)
U7_gg(x1, x2, x3)  =  U7_gg(x3)
U3_gg(x1, x2)  =  U3_gg(x2)
U5_GG(x1, x2, x3)  =  U5_GG(x3)
U4_GG(x1, x2, x3)  =  U4_GG(x3)
R_IN_GG(x1, x2)  =  R_IN_GG(x1, x2)
U11_GG(x1, x2)  =  U11_GG(x2)
P_IN_GG(x1, x2)  =  P_IN_GG(x1, x2)
Q_IN_GG(x1, x2)  =  Q_IN_GG(x1, x2)
U2_GG(x1, x2)  =  U2_GG(x1, x2)
U3_GG(x1, x2)  =  U3_GG(x2)
U12_GG(x1, x2, x3)  =  U12_GG(x3)
E_IN_GG(x1, x2)  =  E_IN_GG(x1, x2)
U6_GG(x1, x2, x3)  =  U6_GG(x1, x2, x3)
U13_GG(x1, x2, x3)  =  U13_GG(x1, x2, x3)
U1_GG(x1, x2, x3)  =  U1_GG(x3)
U9_GG(x1, x2, x3)  =  U9_GG(x1, x2, x3)
U10_GG(x1, x2, x3)  =  U10_GG(x3)
U14_GG(x1, x2, x3)  =  U14_GG(x3)
T_IN_GG(x1, x2)  =  T_IN_GG(x1, x2)
U7_GG(x1, x2, x3)  =  U7_GG(x3)
U8_GG(x1, x2, x3)  =  U8_GG(x3)

We have to consider all (P,R,Pi)-chains
The approximation of the Dependency Graph [30] 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_IN_GG(X, f(Y)) → Q_IN_GG(X, Y)
U6_GG(X, Y, r_out_gg(X, f(Y))) → P_IN_GG(X, Y)
U9_GG(X, Y, q_out_gg(X, Y)) → R_IN_GG(X, Y)
T_IN_GG(f(X), f(Y)) → U13_GG(X, Y, q_in_gg(f(X), f(Y)))
T_IN_GG(f(X), f(Y)) → Q_IN_GG(f(X), f(Y))
Q_IN_GG(X, f(f(Y))) → P_IN_GG(X, f(Y))
Q_IN_GG(X, f(f(X))) → U2_GG(X, p_in_gg(X, f(f(X))))
Q_IN_GG(X, f(f(X))) → P_IN_GG(X, f(f(X)))
U2_GG(X, p_out_gg(X, f(f(X)))) → Q_IN_GG(X, f(X))
R_IN_GG(X, f(Y)) → U9_GG(X, Y, q_in_gg(X, Y))
R_IN_GG(f(X), f(X)) → T_IN_GG(f(X), f(X))
P_IN_GG(X, f(Y)) → R_IN_GG(X, f(Y))
U13_GG(X, Y, q_out_gg(f(X), f(Y))) → T_IN_GG(X, Y)
P_IN_GG(X, f(Y)) → U6_GG(X, Y, r_in_gg(X, f(Y)))

The TRS R consists of the following rules:

q_in_gg(X, Y) → U1_gg(X, Y, e_in_gg(X, Y))
e_in_gg(a, b) → e_out_gg(a, b)
U1_gg(X, Y, e_out_gg(X, Y)) → q_out_gg(X, Y)
q_in_gg(X, f(f(X))) → U2_gg(X, p_in_gg(X, f(f(X))))
p_in_gg(X, Y) → U5_gg(X, Y, e_in_gg(X, Y))
U5_gg(X, Y, e_out_gg(X, Y)) → p_out_gg(X, Y)
p_in_gg(X, f(Y)) → U6_gg(X, Y, r_in_gg(X, f(Y)))
r_in_gg(X, Y) → U8_gg(X, Y, e_in_gg(X, Y))
U8_gg(X, Y, e_out_gg(X, Y)) → r_out_gg(X, Y)
r_in_gg(X, f(Y)) → U9_gg(X, Y, q_in_gg(X, Y))
q_in_gg(X, f(f(Y))) → U4_gg(X, Y, p_in_gg(X, f(Y)))
U4_gg(X, Y, p_out_gg(X, f(Y))) → q_out_gg(X, f(f(Y)))
U9_gg(X, Y, q_out_gg(X, Y)) → U10_gg(X, Y, r_in_gg(X, Y))
r_in_gg(f(X), f(X)) → U11_gg(X, t_in_gg(f(X), f(X)))
t_in_gg(X, Y) → U12_gg(X, Y, e_in_gg(X, Y))
U12_gg(X, Y, e_out_gg(X, Y)) → t_out_gg(X, Y)
t_in_gg(f(X), f(Y)) → U13_gg(X, Y, q_in_gg(f(X), f(Y)))
U13_gg(X, Y, q_out_gg(f(X), f(Y))) → U14_gg(X, Y, t_in_gg(X, Y))
U14_gg(X, Y, t_out_gg(X, Y)) → t_out_gg(f(X), f(Y))
U11_gg(X, t_out_gg(f(X), f(X))) → r_out_gg(f(X), f(X))
U10_gg(X, Y, r_out_gg(X, Y)) → r_out_gg(X, f(Y))
U6_gg(X, Y, r_out_gg(X, f(Y))) → U7_gg(X, Y, p_in_gg(X, Y))
U7_gg(X, Y, p_out_gg(X, Y)) → p_out_gg(X, f(Y))
U2_gg(X, p_out_gg(X, f(f(X)))) → U3_gg(X, q_in_gg(X, f(X)))
U3_gg(X, q_out_gg(X, f(X))) → q_out_gg(X, f(f(X)))

The argument filtering Pi contains the following mapping:
q_in_gg(x1, x2)  =  q_in_gg(x1, x2)
U1_gg(x1, x2, x3)  =  U1_gg(x3)
e_in_gg(x1, x2)  =  e_in_gg(x1, x2)
a  =  a
b  =  b
e_out_gg(x1, x2)  =  e_out_gg
q_out_gg(x1, x2)  =  q_out_gg
f(x1)  =  f(x1)
U2_gg(x1, x2)  =  U2_gg(x1, x2)
p_in_gg(x1, x2)  =  p_in_gg(x1, x2)
U5_gg(x1, x2, x3)  =  U5_gg(x3)
p_out_gg(x1, x2)  =  p_out_gg
U6_gg(x1, x2, x3)  =  U6_gg(x1, x2, x3)
r_in_gg(x1, x2)  =  r_in_gg(x1, x2)
U8_gg(x1, x2, x3)  =  U8_gg(x3)
r_out_gg(x1, x2)  =  r_out_gg
U9_gg(x1, x2, x3)  =  U9_gg(x1, x2, x3)
U4_gg(x1, x2, x3)  =  U4_gg(x3)
U10_gg(x1, x2, x3)  =  U10_gg(x3)
U11_gg(x1, x2)  =  U11_gg(x2)
t_in_gg(x1, x2)  =  t_in_gg(x1, x2)
U12_gg(x1, x2, x3)  =  U12_gg(x3)
t_out_gg(x1, x2)  =  t_out_gg
U13_gg(x1, x2, x3)  =  U13_gg(x1, x2, x3)
U14_gg(x1, x2, x3)  =  U14_gg(x3)
U7_gg(x1, x2, x3)  =  U7_gg(x3)
U3_gg(x1, x2)  =  U3_gg(x2)
R_IN_GG(x1, x2)  =  R_IN_GG(x1, x2)
P_IN_GG(x1, x2)  =  P_IN_GG(x1, x2)
Q_IN_GG(x1, x2)  =  Q_IN_GG(x1, x2)
U2_GG(x1, x2)  =  U2_GG(x1, x2)
U6_GG(x1, x2, x3)  =  U6_GG(x1, x2, x3)
U13_GG(x1, x2, x3)  =  U13_GG(x1, x2, x3)
U9_GG(x1, x2, x3)  =  U9_GG(x1, x2, x3)
T_IN_GG(x1, x2)  =  T_IN_GG(x1, x2)

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

↳ Prolog
  ↳ PrologToPiTRSProof
    ↳ PiTRS
      ↳ DependencyPairsProof
        ↳ PiDP
          ↳ DependencyGraphProof
            ↳ PiDP
              ↳ PiDPToQDPProof
                ↳ QDP
                  ↳ QDPOrderProof

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

R_IN_GG(X, f(Y)) → Q_IN_GG(X, Y)
U6_GG(X, Y, r_out_gg) → P_IN_GG(X, Y)
T_IN_GG(f(X), f(Y)) → U13_GG(X, Y, q_in_gg(f(X), f(Y)))
T_IN_GG(f(X), f(Y)) → Q_IN_GG(f(X), f(Y))
Q_IN_GG(X, f(f(Y))) → P_IN_GG(X, f(Y))
Q_IN_GG(X, f(f(X))) → U2_GG(X, p_in_gg(X, f(f(X))))
U9_GG(X, Y, q_out_gg) → R_IN_GG(X, Y)
Q_IN_GG(X, f(f(X))) → P_IN_GG(X, f(f(X)))
U13_GG(X, Y, q_out_gg) → T_IN_GG(X, Y)
R_IN_GG(X, f(Y)) → U9_GG(X, Y, q_in_gg(X, Y))
R_IN_GG(f(X), f(X)) → T_IN_GG(f(X), f(X))
P_IN_GG(X, f(Y)) → R_IN_GG(X, f(Y))
P_IN_GG(X, f(Y)) → U6_GG(X, Y, r_in_gg(X, f(Y)))
U2_GG(X, p_out_gg) → Q_IN_GG(X, f(X))

The TRS R consists of the following rules:

q_in_gg(X, Y) → U1_gg(e_in_gg(X, Y))
e_in_gg(a, b) → e_out_gg
U1_gg(e_out_gg) → q_out_gg
q_in_gg(X, f(f(X))) → U2_gg(X, p_in_gg(X, f(f(X))))
p_in_gg(X, Y) → U5_gg(e_in_gg(X, Y))
U5_gg(e_out_gg) → p_out_gg
p_in_gg(X, f(Y)) → U6_gg(X, Y, r_in_gg(X, f(Y)))
r_in_gg(X, Y) → U8_gg(e_in_gg(X, Y))
U8_gg(e_out_gg) → r_out_gg
r_in_gg(X, f(Y)) → U9_gg(X, Y, q_in_gg(X, Y))
q_in_gg(X, f(f(Y))) → U4_gg(p_in_gg(X, f(Y)))
U4_gg(p_out_gg) → q_out_gg
U9_gg(X, Y, q_out_gg) → U10_gg(r_in_gg(X, Y))
r_in_gg(f(X), f(X)) → U11_gg(t_in_gg(f(X), f(X)))
t_in_gg(X, Y) → U12_gg(e_in_gg(X, Y))
U12_gg(e_out_gg) → t_out_gg
t_in_gg(f(X), f(Y)) → U13_gg(X, Y, q_in_gg(f(X), f(Y)))
U13_gg(X, Y, q_out_gg) → U14_gg(t_in_gg(X, Y))
U14_gg(t_out_gg) → t_out_gg
U11_gg(t_out_gg) → r_out_gg
U10_gg(r_out_gg) → r_out_gg
U6_gg(X, Y, r_out_gg) → U7_gg(p_in_gg(X, Y))
U7_gg(p_out_gg) → p_out_gg
U2_gg(X, p_out_gg) → U3_gg(q_in_gg(X, f(X)))
U3_gg(q_out_gg) → q_out_gg

The set Q consists of the following terms:

q_in_gg(x0, x1)
e_in_gg(x0, x1)
U1_gg(x0)
p_in_gg(x0, x1)
U5_gg(x0)
r_in_gg(x0, x1)
U8_gg(x0)
U4_gg(x0)
U9_gg(x0, x1, x2)
t_in_gg(x0, x1)
U12_gg(x0)
U13_gg(x0, x1, x2)
U14_gg(x0)
U11_gg(x0)
U10_gg(x0)
U6_gg(x0, x1, x2)
U7_gg(x0)
U2_gg(x0, x1)
U3_gg(x0)

We have to consider all (P,Q,R)-chains.
We use the reduction pair processor [15].


The following pairs can be oriented strictly and are deleted.


T_IN_GG(f(X), f(Y)) → U13_GG(X, Y, q_in_gg(f(X), f(Y)))
The remaining pairs can at least be oriented weakly.

R_IN_GG(X, f(Y)) → Q_IN_GG(X, Y)
U6_GG(X, Y, r_out_gg) → P_IN_GG(X, Y)
T_IN_GG(f(X), f(Y)) → Q_IN_GG(f(X), f(Y))
Q_IN_GG(X, f(f(Y))) → P_IN_GG(X, f(Y))
Q_IN_GG(X, f(f(X))) → U2_GG(X, p_in_gg(X, f(f(X))))
U9_GG(X, Y, q_out_gg) → R_IN_GG(X, Y)
Q_IN_GG(X, f(f(X))) → P_IN_GG(X, f(f(X)))
U13_GG(X, Y, q_out_gg) → T_IN_GG(X, Y)
R_IN_GG(X, f(Y)) → U9_GG(X, Y, q_in_gg(X, Y))
R_IN_GG(f(X), f(X)) → T_IN_GG(f(X), f(X))
P_IN_GG(X, f(Y)) → R_IN_GG(X, f(Y))
P_IN_GG(X, f(Y)) → U6_GG(X, Y, r_in_gg(X, f(Y)))
U2_GG(X, p_out_gg) → Q_IN_GG(X, f(X))
Used ordering: Polynomial interpretation [25]:

POL(P_IN_GG(x1, x2)) = 1 + x1   
POL(Q_IN_GG(x1, x2)) = 1 + x1   
POL(R_IN_GG(x1, x2)) = 1 + x1   
POL(T_IN_GG(x1, x2)) = 1 + x1   
POL(U10_gg(x1)) = 0   
POL(U11_gg(x1)) = 0   
POL(U12_gg(x1)) = 0   
POL(U13_GG(x1, x2, x3)) = 1 + x1   
POL(U13_gg(x1, x2, x3)) = 0   
POL(U14_gg(x1)) = 0   
POL(U1_gg(x1)) = 0   
POL(U2_GG(x1, x2)) = 1 + x1   
POL(U2_gg(x1, x2)) = 0   
POL(U3_gg(x1)) = 0   
POL(U4_gg(x1)) = 0   
POL(U5_gg(x1)) = 0   
POL(U6_GG(x1, x2, x3)) = 1 + x1   
POL(U6_gg(x1, x2, x3)) = 0   
POL(U7_gg(x1)) = 0   
POL(U8_gg(x1)) = 0   
POL(U9_GG(x1, x2, x3)) = 1 + x1   
POL(U9_gg(x1, x2, x3)) = 0   
POL(a) = 0   
POL(b) = 0   
POL(e_in_gg(x1, x2)) = 0   
POL(e_out_gg) = 0   
POL(f(x1)) = 1 + x1   
POL(p_in_gg(x1, x2)) = 0   
POL(p_out_gg) = 0   
POL(q_in_gg(x1, x2)) = 0   
POL(q_out_gg) = 0   
POL(r_in_gg(x1, x2)) = 0   
POL(r_out_gg) = 0   
POL(t_in_gg(x1, x2)) = 1 + x1 + x2   
POL(t_out_gg) = 0   

The following usable rules [17] were oriented: none



↳ Prolog
  ↳ PrologToPiTRSProof
    ↳ PiTRS
      ↳ DependencyPairsProof
        ↳ PiDP
          ↳ DependencyGraphProof
            ↳ PiDP
              ↳ PiDPToQDPProof
                ↳ QDP
                  ↳ QDPOrderProof
                    ↳ QDP
                      ↳ DependencyGraphProof

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

R_IN_GG(X, f(Y)) → Q_IN_GG(X, Y)
U6_GG(X, Y, r_out_gg) → P_IN_GG(X, Y)
T_IN_GG(f(X), f(Y)) → Q_IN_GG(f(X), f(Y))
Q_IN_GG(X, f(f(Y))) → P_IN_GG(X, f(Y))
Q_IN_GG(X, f(f(X))) → U2_GG(X, p_in_gg(X, f(f(X))))
U9_GG(X, Y, q_out_gg) → R_IN_GG(X, Y)
Q_IN_GG(X, f(f(X))) → P_IN_GG(X, f(f(X)))
U13_GG(X, Y, q_out_gg) → T_IN_GG(X, Y)
R_IN_GG(X, f(Y)) → U9_GG(X, Y, q_in_gg(X, Y))
R_IN_GG(f(X), f(X)) → T_IN_GG(f(X), f(X))
P_IN_GG(X, f(Y)) → R_IN_GG(X, f(Y))
P_IN_GG(X, f(Y)) → U6_GG(X, Y, r_in_gg(X, f(Y)))
U2_GG(X, p_out_gg) → Q_IN_GG(X, f(X))

The TRS R consists of the following rules:

q_in_gg(X, Y) → U1_gg(e_in_gg(X, Y))
e_in_gg(a, b) → e_out_gg
U1_gg(e_out_gg) → q_out_gg
q_in_gg(X, f(f(X))) → U2_gg(X, p_in_gg(X, f(f(X))))
p_in_gg(X, Y) → U5_gg(e_in_gg(X, Y))
U5_gg(e_out_gg) → p_out_gg
p_in_gg(X, f(Y)) → U6_gg(X, Y, r_in_gg(X, f(Y)))
r_in_gg(X, Y) → U8_gg(e_in_gg(X, Y))
U8_gg(e_out_gg) → r_out_gg
r_in_gg(X, f(Y)) → U9_gg(X, Y, q_in_gg(X, Y))
q_in_gg(X, f(f(Y))) → U4_gg(p_in_gg(X, f(Y)))
U4_gg(p_out_gg) → q_out_gg
U9_gg(X, Y, q_out_gg) → U10_gg(r_in_gg(X, Y))
r_in_gg(f(X), f(X)) → U11_gg(t_in_gg(f(X), f(X)))
t_in_gg(X, Y) → U12_gg(e_in_gg(X, Y))
U12_gg(e_out_gg) → t_out_gg
t_in_gg(f(X), f(Y)) → U13_gg(X, Y, q_in_gg(f(X), f(Y)))
U13_gg(X, Y, q_out_gg) → U14_gg(t_in_gg(X, Y))
U14_gg(t_out_gg) → t_out_gg
U11_gg(t_out_gg) → r_out_gg
U10_gg(r_out_gg) → r_out_gg
U6_gg(X, Y, r_out_gg) → U7_gg(p_in_gg(X, Y))
U7_gg(p_out_gg) → p_out_gg
U2_gg(X, p_out_gg) → U3_gg(q_in_gg(X, f(X)))
U3_gg(q_out_gg) → q_out_gg

The set Q consists of the following terms:

q_in_gg(x0, x1)
e_in_gg(x0, x1)
U1_gg(x0)
p_in_gg(x0, x1)
U5_gg(x0)
r_in_gg(x0, x1)
U8_gg(x0)
U4_gg(x0)
U9_gg(x0, x1, x2)
t_in_gg(x0, x1)
U12_gg(x0)
U13_gg(x0, x1, x2)
U14_gg(x0)
U11_gg(x0)
U10_gg(x0)
U6_gg(x0, x1, x2)
U7_gg(x0)
U2_gg(x0, x1)
U3_gg(x0)

We have to consider all (P,Q,R)-chains.
The approximation of the Dependency Graph [15,17,22] contains 1 SCC with 1 less node.

↳ Prolog
  ↳ PrologToPiTRSProof
    ↳ PiTRS
      ↳ DependencyPairsProof
        ↳ PiDP
          ↳ DependencyGraphProof
            ↳ PiDP
              ↳ PiDPToQDPProof
                ↳ QDP
                  ↳ QDPOrderProof
                    ↳ QDP
                      ↳ DependencyGraphProof
                        ↳ QDP
                          ↳ Instantiation

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

R_IN_GG(X, f(Y)) → Q_IN_GG(X, Y)
Q_IN_GG(X, f(f(Y))) → P_IN_GG(X, f(Y))
Q_IN_GG(X, f(f(X))) → U2_GG(X, p_in_gg(X, f(f(X))))
U9_GG(X, Y, q_out_gg) → R_IN_GG(X, Y)
U6_GG(X, Y, r_out_gg) → P_IN_GG(X, Y)
Q_IN_GG(X, f(f(X))) → P_IN_GG(X, f(f(X)))
R_IN_GG(f(X), f(X)) → T_IN_GG(f(X), f(X))
R_IN_GG(X, f(Y)) → U9_GG(X, Y, q_in_gg(X, Y))
T_IN_GG(f(X), f(Y)) → Q_IN_GG(f(X), f(Y))
P_IN_GG(X, f(Y)) → R_IN_GG(X, f(Y))
P_IN_GG(X, f(Y)) → U6_GG(X, Y, r_in_gg(X, f(Y)))
U2_GG(X, p_out_gg) → Q_IN_GG(X, f(X))

The TRS R consists of the following rules:

q_in_gg(X, Y) → U1_gg(e_in_gg(X, Y))
e_in_gg(a, b) → e_out_gg
U1_gg(e_out_gg) → q_out_gg
q_in_gg(X, f(f(X))) → U2_gg(X, p_in_gg(X, f(f(X))))
p_in_gg(X, Y) → U5_gg(e_in_gg(X, Y))
U5_gg(e_out_gg) → p_out_gg
p_in_gg(X, f(Y)) → U6_gg(X, Y, r_in_gg(X, f(Y)))
r_in_gg(X, Y) → U8_gg(e_in_gg(X, Y))
U8_gg(e_out_gg) → r_out_gg
r_in_gg(X, f(Y)) → U9_gg(X, Y, q_in_gg(X, Y))
q_in_gg(X, f(f(Y))) → U4_gg(p_in_gg(X, f(Y)))
U4_gg(p_out_gg) → q_out_gg
U9_gg(X, Y, q_out_gg) → U10_gg(r_in_gg(X, Y))
r_in_gg(f(X), f(X)) → U11_gg(t_in_gg(f(X), f(X)))
t_in_gg(X, Y) → U12_gg(e_in_gg(X, Y))
U12_gg(e_out_gg) → t_out_gg
t_in_gg(f(X), f(Y)) → U13_gg(X, Y, q_in_gg(f(X), f(Y)))
U13_gg(X, Y, q_out_gg) → U14_gg(t_in_gg(X, Y))
U14_gg(t_out_gg) → t_out_gg
U11_gg(t_out_gg) → r_out_gg
U10_gg(r_out_gg) → r_out_gg
U6_gg(X, Y, r_out_gg) → U7_gg(p_in_gg(X, Y))
U7_gg(p_out_gg) → p_out_gg
U2_gg(X, p_out_gg) → U3_gg(q_in_gg(X, f(X)))
U3_gg(q_out_gg) → q_out_gg

The set Q consists of the following terms:

q_in_gg(x0, x1)
e_in_gg(x0, x1)
U1_gg(x0)
p_in_gg(x0, x1)
U5_gg(x0)
r_in_gg(x0, x1)
U8_gg(x0)
U4_gg(x0)
U9_gg(x0, x1, x2)
t_in_gg(x0, x1)
U12_gg(x0)
U13_gg(x0, x1, x2)
U14_gg(x0)
U11_gg(x0)
U10_gg(x0)
U6_gg(x0, x1, x2)
U7_gg(x0)
U2_gg(x0, x1)
U3_gg(x0)

We have to consider all (P,Q,R)-chains.
By instantiating [15] the rule T_IN_GG(f(X), f(Y)) → Q_IN_GG(f(X), f(Y)) we obtained the following new rules:

T_IN_GG(f(z0), f(z0)) → Q_IN_GG(f(z0), f(z0))



↳ Prolog
  ↳ PrologToPiTRSProof
    ↳ PiTRS
      ↳ DependencyPairsProof
        ↳ PiDP
          ↳ DependencyGraphProof
            ↳ PiDP
              ↳ PiDPToQDPProof
                ↳ QDP
                  ↳ QDPOrderProof
                    ↳ QDP
                      ↳ DependencyGraphProof
                        ↳ QDP
                          ↳ Instantiation
                            ↳ QDP
                              ↳ QDPOrderProof

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

R_IN_GG(X, f(Y)) → Q_IN_GG(X, Y)
U6_GG(X, Y, r_out_gg) → P_IN_GG(X, Y)
T_IN_GG(f(z0), f(z0)) → Q_IN_GG(f(z0), f(z0))
Q_IN_GG(X, f(f(Y))) → P_IN_GG(X, f(Y))
Q_IN_GG(X, f(f(X))) → U2_GG(X, p_in_gg(X, f(f(X))))
U9_GG(X, Y, q_out_gg) → R_IN_GG(X, Y)
Q_IN_GG(X, f(f(X))) → P_IN_GG(X, f(f(X)))
R_IN_GG(X, f(Y)) → U9_GG(X, Y, q_in_gg(X, Y))
R_IN_GG(f(X), f(X)) → T_IN_GG(f(X), f(X))
P_IN_GG(X, f(Y)) → R_IN_GG(X, f(Y))
U2_GG(X, p_out_gg) → Q_IN_GG(X, f(X))
P_IN_GG(X, f(Y)) → U6_GG(X, Y, r_in_gg(X, f(Y)))

The TRS R consists of the following rules:

q_in_gg(X, Y) → U1_gg(e_in_gg(X, Y))
e_in_gg(a, b) → e_out_gg
U1_gg(e_out_gg) → q_out_gg
q_in_gg(X, f(f(X))) → U2_gg(X, p_in_gg(X, f(f(X))))
p_in_gg(X, Y) → U5_gg(e_in_gg(X, Y))
U5_gg(e_out_gg) → p_out_gg
p_in_gg(X, f(Y)) → U6_gg(X, Y, r_in_gg(X, f(Y)))
r_in_gg(X, Y) → U8_gg(e_in_gg(X, Y))
U8_gg(e_out_gg) → r_out_gg
r_in_gg(X, f(Y)) → U9_gg(X, Y, q_in_gg(X, Y))
q_in_gg(X, f(f(Y))) → U4_gg(p_in_gg(X, f(Y)))
U4_gg(p_out_gg) → q_out_gg
U9_gg(X, Y, q_out_gg) → U10_gg(r_in_gg(X, Y))
r_in_gg(f(X), f(X)) → U11_gg(t_in_gg(f(X), f(X)))
t_in_gg(X, Y) → U12_gg(e_in_gg(X, Y))
U12_gg(e_out_gg) → t_out_gg
t_in_gg(f(X), f(Y)) → U13_gg(X, Y, q_in_gg(f(X), f(Y)))
U13_gg(X, Y, q_out_gg) → U14_gg(t_in_gg(X, Y))
U14_gg(t_out_gg) → t_out_gg
U11_gg(t_out_gg) → r_out_gg
U10_gg(r_out_gg) → r_out_gg
U6_gg(X, Y, r_out_gg) → U7_gg(p_in_gg(X, Y))
U7_gg(p_out_gg) → p_out_gg
U2_gg(X, p_out_gg) → U3_gg(q_in_gg(X, f(X)))
U3_gg(q_out_gg) → q_out_gg

The set Q consists of the following terms:

q_in_gg(x0, x1)
e_in_gg(x0, x1)
U1_gg(x0)
p_in_gg(x0, x1)
U5_gg(x0)
r_in_gg(x0, x1)
U8_gg(x0)
U4_gg(x0)
U9_gg(x0, x1, x2)
t_in_gg(x0, x1)
U12_gg(x0)
U13_gg(x0, x1, x2)
U14_gg(x0)
U11_gg(x0)
U10_gg(x0)
U6_gg(x0, x1, x2)
U7_gg(x0)
U2_gg(x0, x1)
U3_gg(x0)

We have to consider all (P,Q,R)-chains.
We use the reduction pair processor [15].


The following pairs can be oriented strictly and are deleted.


R_IN_GG(X, f(Y)) → Q_IN_GG(X, Y)
Q_IN_GG(X, f(f(Y))) → P_IN_GG(X, f(Y))
Q_IN_GG(X, f(f(X))) → U2_GG(X, p_in_gg(X, f(f(X))))
R_IN_GG(X, f(Y)) → U9_GG(X, Y, q_in_gg(X, Y))
P_IN_GG(X, f(Y)) → U6_GG(X, Y, r_in_gg(X, f(Y)))
The remaining pairs can at least be oriented weakly.

U6_GG(X, Y, r_out_gg) → P_IN_GG(X, Y)
T_IN_GG(f(z0), f(z0)) → Q_IN_GG(f(z0), f(z0))
U9_GG(X, Y, q_out_gg) → R_IN_GG(X, Y)
Q_IN_GG(X, f(f(X))) → P_IN_GG(X, f(f(X)))
R_IN_GG(f(X), f(X)) → T_IN_GG(f(X), f(X))
P_IN_GG(X, f(Y)) → R_IN_GG(X, f(Y))
U2_GG(X, p_out_gg) → Q_IN_GG(X, f(X))
Used ordering: Polynomial interpretation [25]:

POL(P_IN_GG(x1, x2)) = x2   
POL(Q_IN_GG(x1, x2)) = x2   
POL(R_IN_GG(x1, x2)) = x2   
POL(T_IN_GG(x1, x2)) = x2   
POL(U10_gg(x1)) = 0   
POL(U11_gg(x1)) = 0   
POL(U12_gg(x1)) = 0   
POL(U13_gg(x1, x2, x3)) = 0   
POL(U14_gg(x1)) = 0   
POL(U1_gg(x1)) = 0   
POL(U2_GG(x1, x2)) = 1 + x1   
POL(U2_gg(x1, x2)) = 0   
POL(U3_gg(x1)) = 0   
POL(U4_gg(x1)) = 0   
POL(U5_gg(x1)) = 0   
POL(U6_GG(x1, x2, x3)) = x2   
POL(U6_gg(x1, x2, x3)) = 0   
POL(U7_gg(x1)) = 0   
POL(U8_gg(x1)) = 0   
POL(U9_GG(x1, x2, x3)) = x2   
POL(U9_gg(x1, x2, x3)) = 0   
POL(a) = 0   
POL(b) = 0   
POL(e_in_gg(x1, x2)) = 0   
POL(e_out_gg) = 0   
POL(f(x1)) = 1 + x1   
POL(p_in_gg(x1, x2)) = 0   
POL(p_out_gg) = 0   
POL(q_in_gg(x1, x2)) = 0   
POL(q_out_gg) = 0   
POL(r_in_gg(x1, x2)) = 0   
POL(r_out_gg) = 0   
POL(t_in_gg(x1, x2)) = 0   
POL(t_out_gg) = 0   

The following usable rules [17] were oriented: none



↳ Prolog
  ↳ PrologToPiTRSProof
    ↳ PiTRS
      ↳ DependencyPairsProof
        ↳ PiDP
          ↳ DependencyGraphProof
            ↳ PiDP
              ↳ PiDPToQDPProof
                ↳ QDP
                  ↳ QDPOrderProof
                    ↳ QDP
                      ↳ DependencyGraphProof
                        ↳ QDP
                          ↳ Instantiation
                            ↳ QDP
                              ↳ QDPOrderProof
                                ↳ QDP
                                  ↳ DependencyGraphProof

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

U9_GG(X, Y, q_out_gg) → R_IN_GG(X, Y)
Q_IN_GG(X, f(f(X))) → P_IN_GG(X, f(f(X)))
U6_GG(X, Y, r_out_gg) → P_IN_GG(X, Y)
T_IN_GG(f(z0), f(z0)) → Q_IN_GG(f(z0), f(z0))
R_IN_GG(f(X), f(X)) → T_IN_GG(f(X), f(X))
P_IN_GG(X, f(Y)) → R_IN_GG(X, f(Y))
U2_GG(X, p_out_gg) → Q_IN_GG(X, f(X))

The TRS R consists of the following rules:

q_in_gg(X, Y) → U1_gg(e_in_gg(X, Y))
e_in_gg(a, b) → e_out_gg
U1_gg(e_out_gg) → q_out_gg
q_in_gg(X, f(f(X))) → U2_gg(X, p_in_gg(X, f(f(X))))
p_in_gg(X, Y) → U5_gg(e_in_gg(X, Y))
U5_gg(e_out_gg) → p_out_gg
p_in_gg(X, f(Y)) → U6_gg(X, Y, r_in_gg(X, f(Y)))
r_in_gg(X, Y) → U8_gg(e_in_gg(X, Y))
U8_gg(e_out_gg) → r_out_gg
r_in_gg(X, f(Y)) → U9_gg(X, Y, q_in_gg(X, Y))
q_in_gg(X, f(f(Y))) → U4_gg(p_in_gg(X, f(Y)))
U4_gg(p_out_gg) → q_out_gg
U9_gg(X, Y, q_out_gg) → U10_gg(r_in_gg(X, Y))
r_in_gg(f(X), f(X)) → U11_gg(t_in_gg(f(X), f(X)))
t_in_gg(X, Y) → U12_gg(e_in_gg(X, Y))
U12_gg(e_out_gg) → t_out_gg
t_in_gg(f(X), f(Y)) → U13_gg(X, Y, q_in_gg(f(X), f(Y)))
U13_gg(X, Y, q_out_gg) → U14_gg(t_in_gg(X, Y))
U14_gg(t_out_gg) → t_out_gg
U11_gg(t_out_gg) → r_out_gg
U10_gg(r_out_gg) → r_out_gg
U6_gg(X, Y, r_out_gg) → U7_gg(p_in_gg(X, Y))
U7_gg(p_out_gg) → p_out_gg
U2_gg(X, p_out_gg) → U3_gg(q_in_gg(X, f(X)))
U3_gg(q_out_gg) → q_out_gg

The set Q consists of the following terms:

q_in_gg(x0, x1)
e_in_gg(x0, x1)
U1_gg(x0)
p_in_gg(x0, x1)
U5_gg(x0)
r_in_gg(x0, x1)
U8_gg(x0)
U4_gg(x0)
U9_gg(x0, x1, x2)
t_in_gg(x0, x1)
U12_gg(x0)
U13_gg(x0, x1, x2)
U14_gg(x0)
U11_gg(x0)
U10_gg(x0)
U6_gg(x0, x1, x2)
U7_gg(x0)
U2_gg(x0, x1)
U3_gg(x0)

We have to consider all (P,Q,R)-chains.
The approximation of the Dependency Graph [15,17,22] contains 0 SCCs with 7 less nodes.