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

0 Prolog
  ↳1 PrologToPiTRSProof (⇐)
    ↳2 PiTRS
    ↳3 DependencyPairsProof (⇔)
    ↳4 PiDP
    ↳5 DependencyGraphProof (⇔)
    ↳6 PiDP
    ↳7 PiDPToQDPProof (⇔)
    ↳8 QDP
    ↳9 QDPOrderProof (⇔)
    ↳10 QDP
    ↳11 DependencyGraphProof (⇔)
    ↳12 QDP
    ↳13 QDPOrderProof (⇔)
    ↳14 QDP
    ↳15 DependencyGraphProof (⇔)
    ↳16 QDP
  ↳17 PrologToPiTRSProof (⇐)
    ↳18 PiTRS
    ↳19 DependencyPairsProof (⇔)
    ↳20 PiDP
    ↳21 DependencyGraphProof (⇔)
    ↳22 PiDP
    ↳23 PiDPToQDPProof (⇐)
    ↳24 QDP
    ↳25 QDPOrderProof (⇔)
    ↳26 QDP
    ↳27 DependencyGraphProof (⇔)
    ↳28 QDP
    ↳29 QDPOrderProof (⇔)
    ↳30 QDP
    ↳31 DependencyGraphProof (⇔)
    ↳32 QDP
    ↳33 UsableRulesProof (⇔)
    ↳34 QDP
    ↳35 QReductionProof (⇔)
    ↳36 QDP
    ↳37 QDPSizeChangeProof (⇔)
    ↳38 TRUE

(0) Obligation:

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).

(1) PrologToPiTRSProof (SOUND transformation)

We use the technique of [LOPSTR]. 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)))

Pi is empty.

Infinitary Constructor Rewriting Termination of PiTRS implies Termination of Prolog

(2) Obligation:

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)))

Pi is empty.

(3) DependencyPairsProof (EQUIVALENT transformation)

Using Dependency Pairs [AG00,LOPSTR] 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)))

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

(4) Obligation:

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)))

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

(5) DependencyGraphProof (EQUIVALENT transformation)

The approximation of the Dependency Graph [LOPSTR] contains 1 SCC with 14 less nodes.

(6) Obligation:

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

Q_IN_GG(X, f(f(X))) → U2_GG(X, p_in_gg(X, f(f(X))))
U2_GG(X, p_out_gg(X, f(f(X)))) → Q_IN_GG(X, f(X))
Q_IN_GG(X, f(f(X))) → P_IN_GG(X, f(f(X)))
P_IN_GG(X, f(Y)) → U6_GG(X, Y, r_in_gg(X, f(Y)))
U6_GG(X, Y, r_out_gg(X, f(Y))) → P_IN_GG(X, Y)
P_IN_GG(X, f(Y)) → R_IN_GG(X, f(Y))
R_IN_GG(X, f(Y)) → U9_GG(X, Y, q_in_gg(X, Y))
U9_GG(X, Y, q_out_gg(X, Y)) → R_IN_GG(X, Y)
R_IN_GG(X, f(Y)) → Q_IN_GG(X, Y)
Q_IN_GG(X, f(f(Y))) → P_IN_GG(X, f(Y))
R_IN_GG(f(X), f(X)) → T_IN_GG(f(X), f(X))
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))) → T_IN_GG(X, Y)
T_IN_GG(f(X), f(Y)) → Q_IN_GG(f(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)))

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

(7) PiDPToQDPProof (EQUIVALENT transformation)

Transforming (infinitary) constructor rewriting Pi-DP problem [LOPSTR] into ordinary QDP problem [LPAR04] by application of Pi.

(8) Obligation:

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

Q_IN_GG(X, f(f(X))) → U2_GG(X, p_in_gg(X, f(f(X))))
U2_GG(X, p_out_gg(X, f(f(X)))) → Q_IN_GG(X, f(X))
Q_IN_GG(X, f(f(X))) → P_IN_GG(X, f(f(X)))
P_IN_GG(X, f(Y)) → U6_GG(X, Y, r_in_gg(X, f(Y)))
U6_GG(X, Y, r_out_gg(X, f(Y))) → P_IN_GG(X, Y)
P_IN_GG(X, f(Y)) → R_IN_GG(X, f(Y))
R_IN_GG(X, f(Y)) → U9_GG(X, Y, q_in_gg(X, Y))
U9_GG(X, Y, q_out_gg(X, Y)) → R_IN_GG(X, Y)
R_IN_GG(X, f(Y)) → Q_IN_GG(X, Y)
Q_IN_GG(X, f(f(Y))) → P_IN_GG(X, f(Y))
R_IN_GG(f(X), f(X)) → T_IN_GG(f(X), f(X))
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))) → T_IN_GG(X, Y)
T_IN_GG(f(X), f(Y)) → Q_IN_GG(f(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 set Q consists of the following terms:

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

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

(9) QDPOrderProof (EQUIVALENT transformation)

We use the reduction pair processor [LPAR04].


The following pairs can be oriented strictly and are deleted.


U13_GG(X, Y, q_out_gg(f(X), f(Y))) → T_IN_GG(X, Y)
The remaining pairs can at least be oriented weakly.
Used ordering: Polynomial interpretation [POLO]:

POL(P_IN_GG(x1, x2)) = x1   
POL(Q_IN_GG(x1, x2)) = x1   
POL(R_IN_GG(x1, x2)) = x1   
POL(T_IN_GG(x1, x2)) = x1   
POL(U10_gg(x1, x2, x3)) = 0   
POL(U11_gg(x1, x2)) = 0   
POL(U12_gg(x1, x2, x3)) = 0   
POL(U13_GG(x1, x2, x3)) = 1 + x1   
POL(U13_gg(x1, x2, x3)) = 0   
POL(U14_gg(x1, x2, x3)) = 0   
POL(U1_gg(x1, x2, x3)) = 0   
POL(U2_GG(x1, x2)) = x1   
POL(U2_gg(x1, x2)) = 0   
POL(U3_gg(x1, x2)) = 0   
POL(U4_gg(x1, x2, x3)) = 0   
POL(U5_gg(x1, x2, x3)) = 0   
POL(U6_GG(x1, x2, x3)) = x1   
POL(U6_gg(x1, x2, x3)) = 0   
POL(U7_gg(x1, x2, x3)) = 0   
POL(U8_gg(x1, x2, x3)) = 0   
POL(U9_GG(x1, x2, x3)) = 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(x1, x2)) = 0   
POL(f(x1)) = 1 + x1   
POL(p_in_gg(x1, x2)) = 0   
POL(p_out_gg(x1, x2)) = 0   
POL(q_in_gg(x1, x2)) = 0   
POL(q_out_gg(x1, x2)) = 0   
POL(r_in_gg(x1, x2)) = 1   
POL(r_out_gg(x1, x2)) = 0   
POL(t_in_gg(x1, x2)) = 0   
POL(t_out_gg(x1, x2)) = 0   

The following usable rules [FROCOS05] were oriented: none

(10) Obligation:

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

Q_IN_GG(X, f(f(X))) → U2_GG(X, p_in_gg(X, f(f(X))))
U2_GG(X, p_out_gg(X, f(f(X)))) → Q_IN_GG(X, f(X))
Q_IN_GG(X, f(f(X))) → P_IN_GG(X, f(f(X)))
P_IN_GG(X, f(Y)) → U6_GG(X, Y, r_in_gg(X, f(Y)))
U6_GG(X, Y, r_out_gg(X, f(Y))) → P_IN_GG(X, Y)
P_IN_GG(X, f(Y)) → R_IN_GG(X, f(Y))
R_IN_GG(X, f(Y)) → U9_GG(X, Y, q_in_gg(X, Y))
U9_GG(X, Y, q_out_gg(X, Y)) → R_IN_GG(X, Y)
R_IN_GG(X, f(Y)) → Q_IN_GG(X, Y)
Q_IN_GG(X, f(f(Y))) → P_IN_GG(X, f(Y))
R_IN_GG(f(X), f(X)) → T_IN_GG(f(X), f(X))
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))

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 set Q consists of the following terms:

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

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

(11) DependencyGraphProof (EQUIVALENT transformation)

The approximation of the Dependency Graph [LPAR04,FROCOS05,EDGSTAR] contains 1 SCC with 1 less node.

(12) Obligation:

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

U2_GG(X, p_out_gg(X, f(f(X)))) → Q_IN_GG(X, f(X))
Q_IN_GG(X, f(f(Y))) → P_IN_GG(X, f(Y))
P_IN_GG(X, f(Y)) → U6_GG(X, Y, r_in_gg(X, f(Y)))
U6_GG(X, Y, r_out_gg(X, f(Y))) → P_IN_GG(X, Y)
P_IN_GG(X, f(Y)) → R_IN_GG(X, f(Y))
R_IN_GG(X, f(Y)) → U9_GG(X, Y, q_in_gg(X, Y))
U9_GG(X, Y, q_out_gg(X, Y)) → R_IN_GG(X, Y)
R_IN_GG(X, f(Y)) → Q_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)))
R_IN_GG(f(X), f(X)) → T_IN_GG(f(X), f(X))
T_IN_GG(f(X), f(Y)) → Q_IN_GG(f(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 set Q consists of the following terms:

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

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

(13) QDPOrderProof (EQUIVALENT transformation)

We use the reduction pair processor [LPAR04].


The following pairs can be oriented strictly and are deleted.


Q_IN_GG(X, f(f(Y))) → P_IN_GG(X, f(Y))
P_IN_GG(X, f(Y)) → U6_GG(X, Y, r_in_gg(X, f(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(X))) → U2_GG(X, p_in_gg(X, f(f(X))))
The remaining pairs can at least be oriented weakly.
Used ordering: Polynomial interpretation [POLO]:

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, x2, x3)) = 0   
POL(U11_gg(x1, x2)) = 0   
POL(U12_gg(x1, x2, x3)) = 0   
POL(U13_gg(x1, x2, x3)) = 0   
POL(U14_gg(x1, x2, x3)) = 0   
POL(U1_gg(x1, x2, x3)) = 0   
POL(U2_GG(x1, x2)) = 1 + x1   
POL(U2_gg(x1, x2)) = 0   
POL(U3_gg(x1, x2)) = 0   
POL(U4_gg(x1, x2, x3)) = 0   
POL(U5_gg(x1, x2, x3)) = 0   
POL(U6_GG(x1, x2, x3)) = x2   
POL(U6_gg(x1, x2, x3)) = 0   
POL(U7_gg(x1, x2, x3)) = 0   
POL(U8_gg(x1, x2, x3)) = 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(x1, x2)) = 0   
POL(f(x1)) = 1 + x1   
POL(p_in_gg(x1, x2)) = 0   
POL(p_out_gg(x1, x2)) = 0   
POL(q_in_gg(x1, x2)) = 0   
POL(q_out_gg(x1, x2)) = 0   
POL(r_in_gg(x1, x2)) = 0   
POL(r_out_gg(x1, x2)) = 0   
POL(t_in_gg(x1, x2)) = x2   
POL(t_out_gg(x1, x2)) = 0   

The following usable rules [FROCOS05] were oriented: none

(14) Obligation:

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

U2_GG(X, p_out_gg(X, f(f(X)))) → Q_IN_GG(X, f(X))
U6_GG(X, Y, r_out_gg(X, f(Y))) → P_IN_GG(X, Y)
P_IN_GG(X, f(Y)) → R_IN_GG(X, f(Y))
U9_GG(X, Y, q_out_gg(X, Y)) → 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))
T_IN_GG(f(X), f(Y)) → Q_IN_GG(f(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 set Q consists of the following terms:

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

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

(15) DependencyGraphProof (EQUIVALENT transformation)

The approximation of the Dependency Graph [LPAR04,FROCOS05,EDGSTAR] contains 1 SCC with 3 less nodes.

(16) Obligation:

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

R_IN_GG(f(X), f(X)) → T_IN_GG(f(X), f(X))
T_IN_GG(f(X), f(Y)) → Q_IN_GG(f(X), f(Y))
Q_IN_GG(X, f(f(X))) → P_IN_GG(X, f(f(X)))
P_IN_GG(X, f(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 set Q consists of the following terms:

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

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

(17) PrologToPiTRSProof (SOUND transformation)

We use the technique of [LOPSTR]. 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

(18) Obligation:

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)

(19) DependencyPairsProof (EQUIVALENT transformation)

Using Dependency Pairs [AG00,LOPSTR] 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)
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)
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)
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)
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)
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)

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

(20) Obligation:

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)
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)
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)
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)
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)
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)

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

(21) DependencyGraphProof (EQUIVALENT transformation)

The approximation of the Dependency Graph [LOPSTR] contains 1 SCC with 14 less nodes.

(22) Obligation:

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

Q_IN_GG(X, f(f(X))) → U2_GG(X, p_in_gg(X, f(f(X))))
U2_GG(X, p_out_gg(X, f(f(X)))) → Q_IN_GG(X, f(X))
Q_IN_GG(X, f(f(X))) → P_IN_GG(X, f(f(X)))
P_IN_GG(X, f(Y)) → U6_GG(X, Y, r_in_gg(X, f(Y)))
U6_GG(X, Y, r_out_gg(X, f(Y))) → P_IN_GG(X, Y)
P_IN_GG(X, f(Y)) → R_IN_GG(X, f(Y))
R_IN_GG(X, f(Y)) → U9_GG(X, Y, q_in_gg(X, Y))
U9_GG(X, Y, q_out_gg(X, Y)) → R_IN_GG(X, Y)
R_IN_GG(X, f(Y)) → Q_IN_GG(X, Y)
Q_IN_GG(X, f(f(Y))) → P_IN_GG(X, f(Y))
R_IN_GG(f(X), f(X)) → T_IN_GG(f(X), f(X))
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))) → T_IN_GG(X, Y)
T_IN_GG(f(X), f(Y)) → Q_IN_GG(f(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)
Q_IN_GG(x1, x2)  =  Q_IN_GG(x1, x2)
U2_GG(x1, x2)  =  U2_GG(x1, x2)
P_IN_GG(x1, x2)  =  P_IN_GG(x1, x2)
U6_GG(x1, x2, x3)  =  U6_GG(x1, x2, x3)
R_IN_GG(x1, x2)  =  R_IN_GG(x1, x2)
U9_GG(x1, x2, x3)  =  U9_GG(x1, x2, x3)
T_IN_GG(x1, x2)  =  T_IN_GG(x1, x2)
U13_GG(x1, x2, x3)  =  U13_GG(x1, x2, x3)

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

(23) PiDPToQDPProof (SOUND transformation)

Transforming (infinitary) constructor rewriting Pi-DP problem [LOPSTR] into ordinary QDP problem [LPAR04] by application of Pi.

(24) Obligation:

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

Q_IN_GG(X, f(f(X))) → U2_GG(X, p_in_gg(X, f(f(X))))
U2_GG(X, p_out_gg) → Q_IN_GG(X, f(X))
Q_IN_GG(X, f(f(X))) → P_IN_GG(X, f(f(X)))
P_IN_GG(X, f(Y)) → U6_GG(X, Y, r_in_gg(X, f(Y)))
U6_GG(X, Y, r_out_gg) → P_IN_GG(X, Y)
P_IN_GG(X, f(Y)) → R_IN_GG(X, f(Y))
R_IN_GG(X, f(Y)) → U9_GG(X, Y, q_in_gg(X, Y))
U9_GG(X, Y, q_out_gg) → R_IN_GG(X, Y)
R_IN_GG(X, f(Y)) → Q_IN_GG(X, Y)
Q_IN_GG(X, f(f(Y))) → P_IN_GG(X, f(Y))
R_IN_GG(f(X), f(X)) → T_IN_GG(f(X), f(X))
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) → T_IN_GG(X, Y)
T_IN_GG(f(X), f(Y)) → Q_IN_GG(f(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.

(25) QDPOrderProof (EQUIVALENT transformation)

We use the reduction pair processor [LPAR04].


The following pairs can be oriented strictly and are deleted.


U13_GG(X, Y, q_out_gg) → T_IN_GG(X, Y)
The remaining pairs can at least be oriented weakly.
Used ordering: Polynomial interpretation [POLO]:

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

The following usable rules [FROCOS05] were oriented:

p_in_gg(X, Y) → U5_gg(e_in_gg(X, Y))
p_in_gg(X, f(Y)) → U6_gg(X, Y, r_in_gg(X, f(Y)))
r_in_gg(X, f(Y)) → U9_gg(X, Y, q_in_gg(X, Y))
r_in_gg(f(X), f(X)) → U11_gg(t_in_gg(f(X), f(X)))
q_in_gg(X, Y) → U1_gg(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(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))
U10_gg(r_out_gg) → r_out_gg
U11_gg(t_out_gg) → r_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
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
e_in_gg(a, b) → e_out_gg
U1_gg(e_out_gg) → q_out_gg
U5_gg(e_out_gg) → p_out_gg

(26) Obligation:

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

Q_IN_GG(X, f(f(X))) → U2_GG(X, p_in_gg(X, f(f(X))))
U2_GG(X, p_out_gg) → Q_IN_GG(X, f(X))
Q_IN_GG(X, f(f(X))) → P_IN_GG(X, f(f(X)))
P_IN_GG(X, f(Y)) → U6_GG(X, Y, r_in_gg(X, f(Y)))
U6_GG(X, Y, r_out_gg) → P_IN_GG(X, Y)
P_IN_GG(X, f(Y)) → R_IN_GG(X, f(Y))
R_IN_GG(X, f(Y)) → U9_GG(X, Y, q_in_gg(X, Y))
U9_GG(X, Y, q_out_gg) → R_IN_GG(X, Y)
R_IN_GG(X, f(Y)) → Q_IN_GG(X, Y)
Q_IN_GG(X, f(f(Y))) → P_IN_GG(X, f(Y))
R_IN_GG(f(X), f(X)) → T_IN_GG(f(X), f(X))
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))

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.

(27) DependencyGraphProof (EQUIVALENT transformation)

The approximation of the Dependency Graph [LPAR04,FROCOS05,EDGSTAR] contains 1 SCC with 1 less node.

(28) Obligation:

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

U2_GG(X, p_out_gg) → Q_IN_GG(X, f(X))
Q_IN_GG(X, f(f(Y))) → P_IN_GG(X, f(Y))
P_IN_GG(X, f(Y)) → U6_GG(X, Y, r_in_gg(X, f(Y)))
U6_GG(X, Y, r_out_gg) → P_IN_GG(X, Y)
P_IN_GG(X, f(Y)) → R_IN_GG(X, f(Y))
R_IN_GG(X, f(Y)) → U9_GG(X, Y, q_in_gg(X, Y))
U9_GG(X, Y, q_out_gg) → R_IN_GG(X, Y)
R_IN_GG(X, f(Y)) → Q_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)))
R_IN_GG(f(X), f(X)) → T_IN_GG(f(X), f(X))
T_IN_GG(f(X), f(Y)) → Q_IN_GG(f(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.

(29) QDPOrderProof (EQUIVALENT transformation)

We use the reduction pair processor [LPAR04].


The following pairs can be oriented strictly and are deleted.


Q_IN_GG(X, f(f(Y))) → P_IN_GG(X, f(Y))
P_IN_GG(X, f(Y)) → U6_GG(X, Y, r_in_gg(X, f(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)
The remaining pairs can at least be oriented weakly.
Used ordering: Polynomial interpretation [POLO]:

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 + x2   
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)) = 1   
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 + x2   
POL(t_out_gg) = 0   

The following usable rules [FROCOS05] were oriented:

r_in_gg(X, f(Y)) → U9_gg(X, Y, q_in_gg(X, Y))
r_in_gg(f(X), f(X)) → U11_gg(t_in_gg(f(X), f(X)))
q_in_gg(X, f(f(X))) → U2_gg(X, p_in_gg(X, f(f(X))))
q_in_gg(X, f(f(Y))) → U4_gg(p_in_gg(X, f(Y)))
p_in_gg(X, Y) → U5_gg(e_in_gg(X, Y))
p_in_gg(X, f(Y)) → U6_gg(X, Y, r_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))
U10_gg(r_out_gg) → r_out_gg
U11_gg(t_out_gg) → r_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
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
U5_gg(e_out_gg) → p_out_gg

(30) Obligation:

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

U2_GG(X, p_out_gg) → Q_IN_GG(X, f(X))
U6_GG(X, Y, r_out_gg) → P_IN_GG(X, Y)
P_IN_GG(X, f(Y)) → R_IN_GG(X, f(Y))
U9_GG(X, Y, q_out_gg) → R_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)))
R_IN_GG(f(X), f(X)) → T_IN_GG(f(X), f(X))
T_IN_GG(f(X), f(Y)) → Q_IN_GG(f(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.

(31) DependencyGraphProof (EQUIVALENT transformation)

The approximation of the Dependency Graph [LPAR04,FROCOS05,EDGSTAR] contains 1 SCC with 4 less nodes.

(32) Obligation:

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

Q_IN_GG(X, f(f(X))) → P_IN_GG(X, f(f(X)))
P_IN_GG(X, f(Y)) → R_IN_GG(X, f(Y))
R_IN_GG(f(X), f(X)) → T_IN_GG(f(X), f(X))
T_IN_GG(f(X), f(Y)) → Q_IN_GG(f(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.

(33) UsableRulesProof (EQUIVALENT transformation)

As all Q-normal forms are R-normal forms we are in the innermost case. Hence, by the usable rules processor [LPAR04] we can delete all non-usable rules [FROCOS05] from R.

(34) Obligation:

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

Q_IN_GG(X, f(f(X))) → P_IN_GG(X, f(f(X)))
P_IN_GG(X, f(Y)) → R_IN_GG(X, f(Y))
R_IN_GG(f(X), f(X)) → T_IN_GG(f(X), f(X))
T_IN_GG(f(X), f(Y)) → Q_IN_GG(f(X), f(Y))

R is empty.
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.

(35) QReductionProof (EQUIVALENT transformation)

We deleted the following terms from Q as each root-symbol of these terms does neither occur in P nor in R.[THIEMANN].

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)

(36) Obligation:

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

Q_IN_GG(X, f(f(X))) → P_IN_GG(X, f(f(X)))
P_IN_GG(X, f(Y)) → R_IN_GG(X, f(Y))
R_IN_GG(f(X), f(X)) → T_IN_GG(f(X), f(X))
T_IN_GG(f(X), f(Y)) → Q_IN_GG(f(X), f(Y))

R is empty.
Q is empty.
We have to consider all (P,Q,R)-chains.

(37) QDPSizeChangeProof (EQUIVALENT transformation)

By using the subterm criterion [SUBTERM_CRITERION] together with the size-change analysis [AAECC05] 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:

  • P_IN_GG(X, f(Y)) → R_IN_GG(X, f(Y))
    The graph contains the following edges 1 >= 1, 2 >= 2

  • T_IN_GG(f(X), f(Y)) → Q_IN_GG(f(X), f(Y))
    The graph contains the following edges 1 >= 1, 2 >= 2

  • R_IN_GG(f(X), f(X)) → T_IN_GG(f(X), f(X))
    The graph contains the following edges 1 >= 1, 2 >= 1, 1 >= 2, 2 >= 2

  • Q_IN_GG(X, f(f(X))) → P_IN_GG(X, f(f(X)))
    The graph contains the following edges 1 >= 1, 2 > 1, 2 >= 2

(38) TRUE