Left Termination of the query pattern p_in_2(g, g) w.r.t. the given Prolog program could not be shown:

(0) Obligation:

Clauses:

p(X, Y) :- ','(q(X, Y), r(X)).
q(a, 0).
q(X, s(Y)) :- q(X, Y).
r(b) :- r(b).

Queries:

p(g,g).

(1) PrologToPrologProblemTransformerProof (SOUND transformation)

Built Prolog problem from termination graph.

digraph dp_graph {
node [outthreshold=100, inthreshold=100];
1 [label="1: p(T1, T2)\n\nT1 is ground\nT2 is ground", fontsize=16, style=filled, fillcolor=lightyellow, color=red];
2 [label="2: p(T1, T2), SCOPE: 1, CLAUSE: 0\n\nT1 is ground\nT2 is ground", fontsize=16, style=filled, fillcolor=lightyellow];
3 [label="3: ','(q(T3, T4), r(T3))\n\nT3 is ground\nT4 is ground", fontsize=16, style=filled, fillcolor=lightyellow];
4 [label="4: q(T3, T4)\n\nT3 is ground\nT4 is ground", fontsize=16, style=filled, fillcolor=lightyellow];
5 [label="5: r(T3)\n\nT3 is ground", fontsize=16, style=filled, fillcolor=lightyellow];
6 [label="6: q(T3, T4), SCOPE: 2, CLAUSE: 1 | q(T3, T4), SCOPE: 2, CLAUSE: 2\n\nT3 is ground\nT4 is ground", fontsize=16, style=filled, fillcolor=lightyellow];
7 [label="7: q(T3, T4), SCOPE: 2, CLAUSE: 1\n\nT3 is ground\nT4 is ground", fontsize=16, style=filled, fillcolor=lightyellow];
8 [label="8: q(T3, T4), SCOPE: 2, CLAUSE: 2\n\nT3 is ground\nT4 is ground", fontsize=16, style=filled, fillcolor=lightyellow];
9 [label="9: true\n\n", fontsize=16, style=filled, fillcolor=lightyellow];
10 [label="10: \n\n", fontsize=16, style=filled, fillcolor=lightyellow];
11 [label="11: \n\n", fontsize=16, style=filled, fillcolor=lightyellow];
12 [label="12: q(T5, T6)\n\nT5 is ground\nT6 is ground", fontsize=16, style=filled, fillcolor=lightyellow];
13 [label="13: \n\nX7 is free\nX8 is free; ", fontsize=16, style=filled, fillcolor=lightyellow];
14 [label="14: r(T3), SCOPE: 3, CLAUSE: 3\n\nT3 is ground", fontsize=16, style=filled, fillcolor=lightyellow];
15 [label="15: r(b)\n\n", fontsize=16, style=filled, fillcolor=lightyellow];
16 [label="16: \n\n", fontsize=16, style=filled, fillcolor=lightyellow];
17 [label="17: r(b), SCOPE: 4, CLAUSE: 3\n\n", fontsize=16, style=filled, fillcolor=lightyellow];
18 [label="18: r(b)\n\n", fontsize=16, style=filled, fillcolor=lightyellow];
19 [label="CASE", fontsize=14, style = filled, fillcolor = lightcyan];
1 -> 19 [arrowhead = none ];
19 -> 2;

20 [label="EVAL with clause\np(X3, X4) :- ','(q(X3, X4), r(X3)).\nand substitution\nT1 -> T3\nX3 -> T3\nT2 -> T4\nX4 -> T4", fontsize=14, style = filled, fillcolor = lightblue];
2 -> 20 [arrowhead = none ];
20 -> 3;

21 [label="SPLIT 1", fontsize=14, style = filled, fillcolor = violet];
3 -> 21 [arrowhead = none ];
21 -> 4;

22 [label="SPLIT 2", fontsize=14, style = filled, fillcolor = violet];
3 -> 22 [arrowhead = none ];
22 -> 5;

23 [label="CASE", fontsize=14, style = filled, fillcolor = lightcyan];
4 -> 23 [arrowhead = none ];
23 -> 6;

24 [label="CASE", fontsize=14, style = filled, fillcolor = lightcyan];
5 -> 24 [arrowhead = none ];
24 -> 14;

25 [label="PARALLEL", fontsize=14, style = filled, fillcolor = violet];
6 -> 25 [arrowhead = none ];
25 -> 7;

26 [label="PARALLEL", fontsize=14, style = filled, fillcolor = violet];
6 -> 26 [arrowhead = none ];
26 -> 8;

27 [label="EVAL with clause\nq(a, 0).\nand substitution\nT3 -> a\nT4 -> 0", fontsize=14, style = filled, fillcolor = lightblue];
7 -> 27 [arrowhead = none ];
27 -> 9;

28 [label="EVAL-BACKTRACK", fontsize=14, style = filled, fillcolor = lightblue];
7 -> 28 [arrowhead = none ];
28 -> 10;

29 [label="EVAL with clause\nq(X7, s(X8)) :- q(X7, X8).\nand substitution\nT3 -> T5\nX7 -> T5\nX8 -> T6\nT4 -> s(T6)", fontsize=14, style = filled, fillcolor = lightblue];
8 -> 29 [arrowhead = none ];
29 -> 12;

30 [label="EVAL-BACKTRACK", fontsize=14, style = filled, fillcolor = lightblue];
8 -> 30 [arrowhead = none ];
30 -> 13;

31 [label="SUCCESS", fontsize=14, style = filled, fillcolor = lightgreen];
9 -> 31 [arrowhead = none ];
31 -> 11;

32 [label="INSTANCE with matching:\nT3 -> T5\nT4 -> T6", fontsize=14, style = filled, fillcolor = lightgrey];
12 -> 32 [arrowhead = none , style=dashed];
32 -> 4[style=dashed];

33 [label="EVAL with clause\nr(b) :- r(b).\nand substitution\nT3 -> b", fontsize=14, style = filled, fillcolor = lightblue];
14 -> 33 [arrowhead = none ];
33 -> 15;

34 [label="EVAL-BACKTRACK", fontsize=14, style = filled, fillcolor = lightblue];
14 -> 34 [arrowhead = none ];
34 -> 16;

35 [label="CASE", fontsize=14, style = filled, fillcolor = lightcyan];
15 -> 35 [arrowhead = none ];
35 -> 17;

36 [label="EVAL with clause\nr(b) :- r(b).\nand substitution", fontsize=14, style = filled, fillcolor = lightblue];
17 -> 36 [arrowhead = none ];
36 -> 18;

37 [label="INSTANCE", fontsize=14, style = filled, fillcolor = lightgrey];
18 -> 37 [arrowhead = none , style=dashed];
37 -> 15[style=dashed];

}

(2) Obligation:

Clauses:

q4(a, 0).
q4(T5, s(T6)) :- q4(T5, T6).
r15 :- r15.
p1(T3, T4) :- q4(T3, T4).
p1(b, T4) :- ','(q4(b, T4), r15).

Queries:

p1(g,g).

(3) PrologToPiTRSProof (SOUND transformation)

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

p1_in_gg(T3, T4) → U3_gg(T3, T4, q4_in_gg(T3, T4))
q4_in_gg(a, 0) → q4_out_gg(a, 0)
q4_in_gg(T5, s(T6)) → U1_gg(T5, T6, q4_in_gg(T5, T6))
U1_gg(T5, T6, q4_out_gg(T5, T6)) → q4_out_gg(T5, s(T6))
U3_gg(T3, T4, q4_out_gg(T3, T4)) → p1_out_gg(T3, T4)
p1_in_gg(b, T4) → U4_gg(T4, q4_in_gg(b, T4))
U4_gg(T4, q4_out_gg(b, T4)) → U5_gg(T4, r15_in_)
r15_in_ → U2_(r15_in_)
U2_(r15_out_) → r15_out_
U5_gg(T4, r15_out_) → p1_out_gg(b, T4)

The argument filtering Pi contains the following mapping:
p1_in_gg(x1, x2)  =  p1_in_gg(x1, x2)
U3_gg(x1, x2, x3)  =  U3_gg(x3)
q4_in_gg(x1, x2)  =  q4_in_gg(x1, x2)
a  =  a
0  =  0
q4_out_gg(x1, x2)  =  q4_out_gg
s(x1)  =  s(x1)
U1_gg(x1, x2, x3)  =  U1_gg(x3)
p1_out_gg(x1, x2)  =  p1_out_gg
b  =  b
U4_gg(x1, x2)  =  U4_gg(x2)
U5_gg(x1, x2)  =  U5_gg(x2)
r15_in_  =  r15_in_
U2_(x1)  =  U2_(x1)
r15_out_  =  r15_out_

Infinitary Constructor Rewriting Termination of PiTRS implies Termination of Prolog

(4) Obligation:

Pi-finite rewrite system:
The TRS R consists of the following rules:

p1_in_gg(T3, T4) → U3_gg(T3, T4, q4_in_gg(T3, T4))
q4_in_gg(a, 0) → q4_out_gg(a, 0)
q4_in_gg(T5, s(T6)) → U1_gg(T5, T6, q4_in_gg(T5, T6))
U1_gg(T5, T6, q4_out_gg(T5, T6)) → q4_out_gg(T5, s(T6))
U3_gg(T3, T4, q4_out_gg(T3, T4)) → p1_out_gg(T3, T4)
p1_in_gg(b, T4) → U4_gg(T4, q4_in_gg(b, T4))
U4_gg(T4, q4_out_gg(b, T4)) → U5_gg(T4, r15_in_)
r15_in_ → U2_(r15_in_)
U2_(r15_out_) → r15_out_
U5_gg(T4, r15_out_) → p1_out_gg(b, T4)

The argument filtering Pi contains the following mapping:
p1_in_gg(x1, x2)  =  p1_in_gg(x1, x2)
U3_gg(x1, x2, x3)  =  U3_gg(x3)
q4_in_gg(x1, x2)  =  q4_in_gg(x1, x2)
a  =  a
0  =  0
q4_out_gg(x1, x2)  =  q4_out_gg
s(x1)  =  s(x1)
U1_gg(x1, x2, x3)  =  U1_gg(x3)
p1_out_gg(x1, x2)  =  p1_out_gg
b  =  b
U4_gg(x1, x2)  =  U4_gg(x2)
U5_gg(x1, x2)  =  U5_gg(x2)
r15_in_  =  r15_in_
U2_(x1)  =  U2_(x1)
r15_out_  =  r15_out_

(5) 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:

P1_IN_GG(T3, T4) → U3_GG(T3, T4, q4_in_gg(T3, T4))
P1_IN_GG(T3, T4) → Q4_IN_GG(T3, T4)
Q4_IN_GG(T5, s(T6)) → U1_GG(T5, T6, q4_in_gg(T5, T6))
Q4_IN_GG(T5, s(T6)) → Q4_IN_GG(T5, T6)
P1_IN_GG(b, T4) → U4_GG(T4, q4_in_gg(b, T4))
P1_IN_GG(b, T4) → Q4_IN_GG(b, T4)
U4_GG(T4, q4_out_gg(b, T4)) → U5_GG(T4, r15_in_)
U4_GG(T4, q4_out_gg(b, T4)) → R15_IN_
R15_IN_ → U2_¹(r15_in_)
R15_IN_ → R15_IN_

The TRS R consists of the following rules:

p1_in_gg(T3, T4) → U3_gg(T3, T4, q4_in_gg(T3, T4))
q4_in_gg(a, 0) → q4_out_gg(a, 0)
q4_in_gg(T5, s(T6)) → U1_gg(T5, T6, q4_in_gg(T5, T6))
U1_gg(T5, T6, q4_out_gg(T5, T6)) → q4_out_gg(T5, s(T6))
U3_gg(T3, T4, q4_out_gg(T3, T4)) → p1_out_gg(T3, T4)
p1_in_gg(b, T4) → U4_gg(T4, q4_in_gg(b, T4))
U4_gg(T4, q4_out_gg(b, T4)) → U5_gg(T4, r15_in_)
r15_in_ → U2_(r15_in_)
U2_(r15_out_) → r15_out_
U5_gg(T4, r15_out_) → p1_out_gg(b, T4)

The argument filtering Pi contains the following mapping:
p1_in_gg(x1, x2)  =  p1_in_gg(x1, x2)
U3_gg(x1, x2, x3)  =  U3_gg(x3)
q4_in_gg(x1, x2)  =  q4_in_gg(x1, x2)
a  =  a
0  =  0
q4_out_gg(x1, x2)  =  q4_out_gg
s(x1)  =  s(x1)
U1_gg(x1, x2, x3)  =  U1_gg(x3)
p1_out_gg(x1, x2)  =  p1_out_gg
b  =  b
U4_gg(x1, x2)  =  U4_gg(x2)
U5_gg(x1, x2)  =  U5_gg(x2)
r15_in_  =  r15_in_
U2_(x1)  =  U2_(x1)
r15_out_  =  r15_out_
P1_IN_GG(x1, x2)  =  P1_IN_GG(x1, x2)
U3_GG(x1, x2, x3)  =  U3_GG(x3)
Q4_IN_GG(x1, x2)  =  Q4_IN_GG(x1, x2)
U1_GG(x1, x2, x3)  =  U1_GG(x3)
U4_GG(x1, x2)  =  U4_GG(x2)
U5_GG(x1, x2)  =  U5_GG(x2)
R15_IN_  =  R15_IN_
U2_¹(x1)  =  U2_¹(x1)

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

(6) Obligation:

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

P1_IN_GG(T3, T4) → U3_GG(T3, T4, q4_in_gg(T3, T4))
P1_IN_GG(T3, T4) → Q4_IN_GG(T3, T4)
Q4_IN_GG(T5, s(T6)) → U1_GG(T5, T6, q4_in_gg(T5, T6))
Q4_IN_GG(T5, s(T6)) → Q4_IN_GG(T5, T6)
P1_IN_GG(b, T4) → U4_GG(T4, q4_in_gg(b, T4))
P1_IN_GG(b, T4) → Q4_IN_GG(b, T4)
U4_GG(T4, q4_out_gg(b, T4)) → U5_GG(T4, r15_in_)
U4_GG(T4, q4_out_gg(b, T4)) → R15_IN_
R15_IN_ → U2_¹(r15_in_)
R15_IN_ → R15_IN_

The TRS R consists of the following rules:

p1_in_gg(T3, T4) → U3_gg(T3, T4, q4_in_gg(T3, T4))
q4_in_gg(a, 0) → q4_out_gg(a, 0)
q4_in_gg(T5, s(T6)) → U1_gg(T5, T6, q4_in_gg(T5, T6))
U1_gg(T5, T6, q4_out_gg(T5, T6)) → q4_out_gg(T5, s(T6))
U3_gg(T3, T4, q4_out_gg(T3, T4)) → p1_out_gg(T3, T4)
p1_in_gg(b, T4) → U4_gg(T4, q4_in_gg(b, T4))
U4_gg(T4, q4_out_gg(b, T4)) → U5_gg(T4, r15_in_)
r15_in_ → U2_(r15_in_)
U2_(r15_out_) → r15_out_
U5_gg(T4, r15_out_) → p1_out_gg(b, T4)

The argument filtering Pi contains the following mapping:
p1_in_gg(x1, x2)  =  p1_in_gg(x1, x2)
U3_gg(x1, x2, x3)  =  U3_gg(x3)
q4_in_gg(x1, x2)  =  q4_in_gg(x1, x2)
a  =  a
0  =  0
q4_out_gg(x1, x2)  =  q4_out_gg
s(x1)  =  s(x1)
U1_gg(x1, x2, x3)  =  U1_gg(x3)
p1_out_gg(x1, x2)  =  p1_out_gg
b  =  b
U4_gg(x1, x2)  =  U4_gg(x2)
U5_gg(x1, x2)  =  U5_gg(x2)
r15_in_  =  r15_in_
U2_(x1)  =  U2_(x1)
r15_out_  =  r15_out_
P1_IN_GG(x1, x2)  =  P1_IN_GG(x1, x2)
U3_GG(x1, x2, x3)  =  U3_GG(x3)
Q4_IN_GG(x1, x2)  =  Q4_IN_GG(x1, x2)
U1_GG(x1, x2, x3)  =  U1_GG(x3)
U4_GG(x1, x2)  =  U4_GG(x2)
U5_GG(x1, x2)  =  U5_GG(x2)
R15_IN_  =  R15_IN_
U2_¹(x1)  =  U2_¹(x1)

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

(7) DependencyGraphProof (EQUIVALENT transformation)

The approximation of the Dependency Graph [LOPSTR] contains 2 SCCs with 8 less nodes.

(8) Complex Obligation (AND)

(9) Obligation:

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

R15_IN_ → R15_IN_

The TRS R consists of the following rules:

p1_in_gg(T3, T4) → U3_gg(T3, T4, q4_in_gg(T3, T4))
q4_in_gg(a, 0) → q4_out_gg(a, 0)
q4_in_gg(T5, s(T6)) → U1_gg(T5, T6, q4_in_gg(T5, T6))
U1_gg(T5, T6, q4_out_gg(T5, T6)) → q4_out_gg(T5, s(T6))
U3_gg(T3, T4, q4_out_gg(T3, T4)) → p1_out_gg(T3, T4)
p1_in_gg(b, T4) → U4_gg(T4, q4_in_gg(b, T4))
U4_gg(T4, q4_out_gg(b, T4)) → U5_gg(T4, r15_in_)
r15_in_ → U2_(r15_in_)
U2_(r15_out_) → r15_out_
U5_gg(T4, r15_out_) → p1_out_gg(b, T4)

The argument filtering Pi contains the following mapping:
p1_in_gg(x1, x2)  =  p1_in_gg(x1, x2)
U3_gg(x1, x2, x3)  =  U3_gg(x3)
q4_in_gg(x1, x2)  =  q4_in_gg(x1, x2)
a  =  a
0  =  0
q4_out_gg(x1, x2)  =  q4_out_gg
s(x1)  =  s(x1)
U1_gg(x1, x2, x3)  =  U1_gg(x3)
p1_out_gg(x1, x2)  =  p1_out_gg
b  =  b
U4_gg(x1, x2)  =  U4_gg(x2)
U5_gg(x1, x2)  =  U5_gg(x2)
r15_in_  =  r15_in_
U2_(x1)  =  U2_(x1)
r15_out_  =  r15_out_
R15_IN_  =  R15_IN_

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

(10) UsableRulesProof (EQUIVALENT transformation)

For (infinitary) constructor rewriting [LOPSTR] we can delete all non-usable rules from R.

(11) Obligation:

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

R15_IN_ → R15_IN_

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

(12) PiDPToQDPProof (EQUIVALENT transformation)

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

(13) Obligation:

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

R15_IN_ → R15_IN_

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

(14) NonTerminationProof (EQUIVALENT transformation)

We used the non-termination processor [FROCOS05] to show that the DP problem is infinite.
Found a loop by semiunifying a rule from P directly.

s = R15_IN_ evaluates to t =R15_IN_

Thus s starts an infinite chain as s semiunifies with t with the following substitutions:

• Semiunifier: [ ]
• Matcher: [ ]

---

Rewriting sequence

The DP semiunifies directly so there is only one rewrite step from R15_IN_ to R15_IN_.

(15) FALSE

(16) Obligation:

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

Q4_IN_GG(T5, s(T6)) → Q4_IN_GG(T5, T6)

The TRS R consists of the following rules:

p1_in_gg(T3, T4) → U3_gg(T3, T4, q4_in_gg(T3, T4))
q4_in_gg(a, 0) → q4_out_gg(a, 0)
q4_in_gg(T5, s(T6)) → U1_gg(T5, T6, q4_in_gg(T5, T6))
U1_gg(T5, T6, q4_out_gg(T5, T6)) → q4_out_gg(T5, s(T6))
U3_gg(T3, T4, q4_out_gg(T3, T4)) → p1_out_gg(T3, T4)
p1_in_gg(b, T4) → U4_gg(T4, q4_in_gg(b, T4))
U4_gg(T4, q4_out_gg(b, T4)) → U5_gg(T4, r15_in_)
r15_in_ → U2_(r15_in_)
U2_(r15_out_) → r15_out_
U5_gg(T4, r15_out_) → p1_out_gg(b, T4)

The argument filtering Pi contains the following mapping:
p1_in_gg(x1, x2)  =  p1_in_gg(x1, x2)
U3_gg(x1, x2, x3)  =  U3_gg(x3)
q4_in_gg(x1, x2)  =  q4_in_gg(x1, x2)
a  =  a
0  =  0
q4_out_gg(x1, x2)  =  q4_out_gg
s(x1)  =  s(x1)
U1_gg(x1, x2, x3)  =  U1_gg(x3)
p1_out_gg(x1, x2)  =  p1_out_gg
b  =  b
U4_gg(x1, x2)  =  U4_gg(x2)
U5_gg(x1, x2)  =  U5_gg(x2)
r15_in_  =  r15_in_
U2_(x1)  =  U2_(x1)
r15_out_  =  r15_out_
Q4_IN_GG(x1, x2)  =  Q4_IN_GG(x1, x2)

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

(17) UsableRulesProof (EQUIVALENT transformation)

For (infinitary) constructor rewriting [LOPSTR] we can delete all non-usable rules from R.

(18) Obligation:

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

Q4_IN_GG(T5, s(T6)) → Q4_IN_GG(T5, T6)

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

(19) PiDPToQDPProof (EQUIVALENT transformation)

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

(20) Obligation:

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

Q4_IN_GG(T5, s(T6)) → Q4_IN_GG(T5, T6)

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

(21) 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:

• Q4_IN_GG(T5, s(T6)) → Q4_IN_GG(T5, T6)
  The graph contains the following edges 1 >= 1, 2 > 2

(22) TRUE

(23) PrologToPiTRSProof (SOUND transformation)

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

p1_in_gg(T3, T4) → U3_gg(T3, T4, q4_in_gg(T3, T4))
q4_in_gg(a, 0) → q4_out_gg(a, 0)
q4_in_gg(T5, s(T6)) → U1_gg(T5, T6, q4_in_gg(T5, T6))
U1_gg(T5, T6, q4_out_gg(T5, T6)) → q4_out_gg(T5, s(T6))
U3_gg(T3, T4, q4_out_gg(T3, T4)) → p1_out_gg(T3, T4)
p1_in_gg(b, T4) → U4_gg(T4, q4_in_gg(b, T4))
U4_gg(T4, q4_out_gg(b, T4)) → U5_gg(T4, r15_in_)
r15_in_ → U2_(r15_in_)
U2_(r15_out_) → r15_out_
U5_gg(T4, r15_out_) → p1_out_gg(b, T4)

Pi is empty.

Infinitary Constructor Rewriting Termination of PiTRS implies Termination of Prolog

(24) Obligation:

Pi-finite rewrite system:
The TRS R consists of the following rules:

p1_in_gg(T3, T4) → U3_gg(T3, T4, q4_in_gg(T3, T4))
q4_in_gg(a, 0) → q4_out_gg(a, 0)
q4_in_gg(T5, s(T6)) → U1_gg(T5, T6, q4_in_gg(T5, T6))
U1_gg(T5, T6, q4_out_gg(T5, T6)) → q4_out_gg(T5, s(T6))
U3_gg(T3, T4, q4_out_gg(T3, T4)) → p1_out_gg(T3, T4)
p1_in_gg(b, T4) → U4_gg(T4, q4_in_gg(b, T4))
U4_gg(T4, q4_out_gg(b, T4)) → U5_gg(T4, r15_in_)
r15_in_ → U2_(r15_in_)
U2_(r15_out_) → r15_out_
U5_gg(T4, r15_out_) → p1_out_gg(b, T4)

Pi is empty.

(25) 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:

P1_IN_GG(T3, T4) → U3_GG(T3, T4, q4_in_gg(T3, T4))
P1_IN_GG(T3, T4) → Q4_IN_GG(T3, T4)
Q4_IN_GG(T5, s(T6)) → U1_GG(T5, T6, q4_in_gg(T5, T6))
Q4_IN_GG(T5, s(T6)) → Q4_IN_GG(T5, T6)
P1_IN_GG(b, T4) → U4_GG(T4, q4_in_gg(b, T4))
P1_IN_GG(b, T4) → Q4_IN_GG(b, T4)
U4_GG(T4, q4_out_gg(b, T4)) → U5_GG(T4, r15_in_)
U4_GG(T4, q4_out_gg(b, T4)) → R15_IN_
R15_IN_ → U2_¹(r15_in_)
R15_IN_ → R15_IN_

The TRS R consists of the following rules:

p1_in_gg(T3, T4) → U3_gg(T3, T4, q4_in_gg(T3, T4))
q4_in_gg(a, 0) → q4_out_gg(a, 0)
q4_in_gg(T5, s(T6)) → U1_gg(T5, T6, q4_in_gg(T5, T6))
U1_gg(T5, T6, q4_out_gg(T5, T6)) → q4_out_gg(T5, s(T6))
U3_gg(T3, T4, q4_out_gg(T3, T4)) → p1_out_gg(T3, T4)
p1_in_gg(b, T4) → U4_gg(T4, q4_in_gg(b, T4))
U4_gg(T4, q4_out_gg(b, T4)) → U5_gg(T4, r15_in_)
r15_in_ → U2_(r15_in_)
U2_(r15_out_) → r15_out_
U5_gg(T4, r15_out_) → p1_out_gg(b, T4)

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

(26) Obligation:

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

P1_IN_GG(T3, T4) → U3_GG(T3, T4, q4_in_gg(T3, T4))
P1_IN_GG(T3, T4) → Q4_IN_GG(T3, T4)
Q4_IN_GG(T5, s(T6)) → U1_GG(T5, T6, q4_in_gg(T5, T6))
Q4_IN_GG(T5, s(T6)) → Q4_IN_GG(T5, T6)
P1_IN_GG(b, T4) → U4_GG(T4, q4_in_gg(b, T4))
P1_IN_GG(b, T4) → Q4_IN_GG(b, T4)
U4_GG(T4, q4_out_gg(b, T4)) → U5_GG(T4, r15_in_)
U4_GG(T4, q4_out_gg(b, T4)) → R15_IN_
R15_IN_ → U2_¹(r15_in_)
R15_IN_ → R15_IN_

The TRS R consists of the following rules:

p1_in_gg(T3, T4) → U3_gg(T3, T4, q4_in_gg(T3, T4))
q4_in_gg(a, 0) → q4_out_gg(a, 0)
q4_in_gg(T5, s(T6)) → U1_gg(T5, T6, q4_in_gg(T5, T6))
U1_gg(T5, T6, q4_out_gg(T5, T6)) → q4_out_gg(T5, s(T6))
U3_gg(T3, T4, q4_out_gg(T3, T4)) → p1_out_gg(T3, T4)
p1_in_gg(b, T4) → U4_gg(T4, q4_in_gg(b, T4))
U4_gg(T4, q4_out_gg(b, T4)) → U5_gg(T4, r15_in_)
r15_in_ → U2_(r15_in_)
U2_(r15_out_) → r15_out_
U5_gg(T4, r15_out_) → p1_out_gg(b, T4)

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

(27) DependencyGraphProof (EQUIVALENT transformation)

The approximation of the Dependency Graph [LOPSTR] contains 2 SCCs with 8 less nodes.

(28) Complex Obligation (AND)

(29) Obligation:

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

R15_IN_ → R15_IN_

The TRS R consists of the following rules:

p1_in_gg(T3, T4) → U3_gg(T3, T4, q4_in_gg(T3, T4))
q4_in_gg(a, 0) → q4_out_gg(a, 0)
q4_in_gg(T5, s(T6)) → U1_gg(T5, T6, q4_in_gg(T5, T6))
U1_gg(T5, T6, q4_out_gg(T5, T6)) → q4_out_gg(T5, s(T6))
U3_gg(T3, T4, q4_out_gg(T3, T4)) → p1_out_gg(T3, T4)
p1_in_gg(b, T4) → U4_gg(T4, q4_in_gg(b, T4))
U4_gg(T4, q4_out_gg(b, T4)) → U5_gg(T4, r15_in_)
r15_in_ → U2_(r15_in_)
U2_(r15_out_) → r15_out_
U5_gg(T4, r15_out_) → p1_out_gg(b, T4)

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

(30) UsableRulesProof (EQUIVALENT transformation)

For (infinitary) constructor rewriting [LOPSTR] we can delete all non-usable rules from R.

(31) Obligation:

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

R15_IN_ → R15_IN_

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

(32) PiDPToQDPProof (EQUIVALENT transformation)

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

(33) Obligation:

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

R15_IN_ → R15_IN_

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

(34) NonTerminationProof (EQUIVALENT transformation)

We used the non-termination processor [FROCOS05] to show that the DP problem is infinite.
Found a loop by semiunifying a rule from P directly.

s = R15_IN_ evaluates to t =R15_IN_

Thus s starts an infinite chain as s semiunifies with t with the following substitutions:

• Semiunifier: [ ]
• Matcher: [ ]

---

Rewriting sequence

The DP semiunifies directly so there is only one rewrite step from R15_IN_ to R15_IN_.

(35) FALSE

(36) Obligation:

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

Q4_IN_GG(T5, s(T6)) → Q4_IN_GG(T5, T6)

The TRS R consists of the following rules:

p1_in_gg(T3, T4) → U3_gg(T3, T4, q4_in_gg(T3, T4))
q4_in_gg(a, 0) → q4_out_gg(a, 0)
q4_in_gg(T5, s(T6)) → U1_gg(T5, T6, q4_in_gg(T5, T6))
U1_gg(T5, T6, q4_out_gg(T5, T6)) → q4_out_gg(T5, s(T6))
U3_gg(T3, T4, q4_out_gg(T3, T4)) → p1_out_gg(T3, T4)
p1_in_gg(b, T4) → U4_gg(T4, q4_in_gg(b, T4))
U4_gg(T4, q4_out_gg(b, T4)) → U5_gg(T4, r15_in_)
r15_in_ → U2_(r15_in_)
U2_(r15_out_) → r15_out_
U5_gg(T4, r15_out_) → p1_out_gg(b, T4)

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

(37) UsableRulesProof (EQUIVALENT transformation)

For (infinitary) constructor rewriting [LOPSTR] we can delete all non-usable rules from R.

(38) Obligation:

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

Q4_IN_GG(T5, s(T6)) → Q4_IN_GG(T5, T6)

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

(39) PiDPToQDPProof (EQUIVALENT transformation)

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

(40) Obligation:

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

Q4_IN_GG(T5, s(T6)) → Q4_IN_GG(T5, T6)

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

(41) 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:

• Q4_IN_GG(T5, s(T6)) → Q4_IN_GG(T5, T6)
  The graph contains the following edges 1 >= 1, 2 > 2

(42) TRUE