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

(0) Obligation:

Clauses:

p(X, Y) :- ','(less(X, Y), ','(!, p(s(X), Y))).
less(0, s(X1)).
less(s(X), s(Y)) :- less(X, Y).

Query: p(g,g)

(1) PrologToTRSTransformerProof (SOUND transformation)

Transformed Prolog program to TRS.

digraph dp_graph {
node [outthreshold=100, inthreshold=100];
2 [label="2: p(T1, T2)\n\nT1 is ground\nT2 is ground", fontsize=16, style=filled, fillcolor=lightyellow, color=red];
4 [label="4: p(T1, T2), SCOPE: 1, CLAUSE: 0\n\nT1 is ground\nT2 is ground", fontsize=16, style=filled, fillcolor=lightyellow];
9 [label="9: ','(less(T9, T10), ','(!_1, p(s(T9), T10)))\n\nT9 is ground\nT10 is ground", fontsize=16, style=filled, fillcolor=lightyellow];
18 [label="18: less(T9, T10)\n\nT9 is ground\nT10 is ground", fontsize=16, style=filled, fillcolor=lightyellow];
19 [label="19: ','(!_1, p(s(T9), T10))\n\nT9 is ground\nT10 is ground", fontsize=16, style=filled, fillcolor=lightyellow];
22 [label="22: less(T9, T10), SCOPE: 2, CLAUSE: 1 | less(T9, T10), SCOPE: 2, CLAUSE: 2\n\nT9 is ground\nT10 is ground", fontsize=16, style=filled, fillcolor=lightyellow];
25 [label="25: less(T9, T10), SCOPE: 2, CLAUSE: 1\n\nT9 is ground\nT10 is ground", fontsize=16, style=filled, fillcolor=lightyellow];
26 [label="26: less(T9, T10), SCOPE: 2, CLAUSE: 2\n\nT9 is ground\nT10 is ground", fontsize=16, style=filled, fillcolor=lightyellow];
31 [label="31: true\n\n", fontsize=16, style=filled, fillcolor=lightyellow];
32 [label="32: \n\n", fontsize=16, style=filled, fillcolor=lightyellow];
33 [label="33: \n\n", fontsize=16, style=filled, fillcolor=lightyellow];
39 [label="39: less(T24, T25)\n\nT24 is ground\nT25 is ground", fontsize=16, style=filled, fillcolor=lightyellow];
40 [label="40: \n\n", fontsize=16, style=filled, fillcolor=lightyellow];
46 [label="46: p(s(T9), T10)\n\nT9 is ground\nT10 is ground", fontsize=16, style=filled, fillcolor=lightyellow];
47 [label="CASE", fontsize=14, style = filled, fillcolor = lightcyan];
2 -> 47 [arrowhead = none ];
47 -> 4;

48 [label="ONLY EVAL with clause\np(X8, X9) :- ','(less(X8, X9), ','(!_1, p(s(X8), X9))).\nand substitutionT1 -> T9,\nX8 -> T9,\nT2 -> T10,\nX9 -> T10", fontsize=14, style = filled, fillcolor = lightblue];
4 -> 48 [arrowhead = none ];
48 -> 9;

49 [label="SPLIT 1", fontsize=14, style = filled, fillcolor = violet];
9 -> 49 [arrowhead = none ];
49 -> 18;

50 [label="SPLIT 2\nnew knowledge:\nT9 is ground\nT10 is ground", fontsize=14, style = filled, fillcolor = violet];
9 -> 50 [arrowhead = none ];
50 -> 19;

51 [label="CASE", fontsize=14, style = filled, fillcolor = lightcyan];
18 -> 51 [arrowhead = none ];
51 -> 22;

52 [label="CUT", fontsize=14, style = filled, fillcolor = lightgreen];
19 -> 52 [arrowhead = none ];
52 -> 46;

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

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

55 [label="EVAL with clause\nless(0, s(X18)).\nand substitutionT9 -> 0,\nX18 -> T19,\nT10 -> s(T19)", fontsize=14, style = filled, fillcolor = lightblue];
25 -> 55 [arrowhead = none ];
55 -> 31;

56 [label="EVAL-BACKTRACK", fontsize=14, style = filled, fillcolor = lightgreen];
25 -> 56 [arrowhead = none ];
56 -> 32;

57 [label="EVAL with clause\nless(s(X23), s(X24)) :- less(X23, X24).\nand substitutionX23 -> T24,\nT9 -> s(T24),\nX24 -> T25,\nT10 -> s(T25)", fontsize=14, style = filled, fillcolor = lightblue];
26 -> 57 [arrowhead = none ];
57 -> 39;

58 [label="EVAL-BACKTRACK", fontsize=14, style = filled, fillcolor = lightgreen];
26 -> 58 [arrowhead = none ];
58 -> 40;

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

60 [label="INSTANCE with matching:\nT9 -> T24\nT10 -> T25", fontsize=14, style = filled, fillcolor = lightgrey];
39 -> 60 [arrowhead = none , style=dashed];
60 -> 18[style=dashed];

61 [label="INSTANCE with matching:\nT1 -> s(T9)\nT2 -> T10", fontsize=14, style = filled, fillcolor = lightgrey];
46 -> 61 [arrowhead = none , style=dashed];
61 -> 2[style=dashed];

}

(2) Obligation:

Q restricted rewrite system:
The TRS R consists of the following rules:

f2_in(T9, T10) → U1(f9_in(T9, T10), T9, T10)
U1(f9_out1, T9, T10) → f2_out1
f18_in(0, s(T19)) → f18_out1
f18_in(s(T24), s(T25)) → U2(f18_in(T24, T25), s(T24), s(T25))
U2(f18_out1, s(T24), s(T25)) → f18_out1
f19_in(T9, T10) → U3(f2_in(s(T9), T10), T9, T10)
U3(f2_out1, T9, T10) → f19_out1
f9_in(T9, T10) → U4(f18_in(T9, T10), T9, T10)
U4(f18_out1, T9, T10) → U5(f19_in(T9, T10), T9, T10)
U5(f19_out1, T9, T10) → f9_out1

Q is empty.

(3) Overlay + Local Confluence (EQUIVALENT transformation)

The TRS is overlay and locally confluent. By [NOC] we can switch to innermost.

(4) Obligation:

Q restricted rewrite system:
The TRS R consists of the following rules:

f2_in(T9, T10) → U1(f9_in(T9, T10), T9, T10)
U1(f9_out1, T9, T10) → f2_out1
f18_in(0, s(T19)) → f18_out1
f18_in(s(T24), s(T25)) → U2(f18_in(T24, T25), s(T24), s(T25))
U2(f18_out1, s(T24), s(T25)) → f18_out1
f19_in(T9, T10) → U3(f2_in(s(T9), T10), T9, T10)
U3(f2_out1, T9, T10) → f19_out1
f9_in(T9, T10) → U4(f18_in(T9, T10), T9, T10)
U4(f18_out1, T9, T10) → U5(f19_in(T9, T10), T9, T10)
U5(f19_out1, T9, T10) → f9_out1

The set Q consists of the following terms:

f2_in(x0, x1)
U1(f9_out1, x0, x1)
f18_in(0, s(x0))
f18_in(s(x0), s(x1))
U2(f18_out1, s(x0), s(x1))
f19_in(x0, x1)
U3(f2_out1, x0, x1)
f9_in(x0, x1)
U4(f18_out1, x0, x1)
U5(f19_out1, x0, x1)

(5) DependencyPairsProof (EQUIVALENT transformation)

Using Dependency Pairs [AG00,LPAR04] we result in the following initial DP problem.

(6) Obligation:

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

F2_IN(T9, T10) → U1¹(f9_in(T9, T10), T9, T10)
F2_IN(T9, T10) → F9_IN(T9, T10)
F18_IN(s(T24), s(T25)) → U2¹(f18_in(T24, T25), s(T24), s(T25))
F18_IN(s(T24), s(T25)) → F18_IN(T24, T25)
F19_IN(T9, T10) → U3¹(f2_in(s(T9), T10), T9, T10)
F19_IN(T9, T10) → F2_IN(s(T9), T10)
F9_IN(T9, T10) → U4¹(f18_in(T9, T10), T9, T10)
F9_IN(T9, T10) → F18_IN(T9, T10)
U4¹(f18_out1, T9, T10) → U5¹(f19_in(T9, T10), T9, T10)
U4¹(f18_out1, T9, T10) → F19_IN(T9, T10)

The TRS R consists of the following rules:

f2_in(T9, T10) → U1(f9_in(T9, T10), T9, T10)
U1(f9_out1, T9, T10) → f2_out1
f18_in(0, s(T19)) → f18_out1
f18_in(s(T24), s(T25)) → U2(f18_in(T24, T25), s(T24), s(T25))
U2(f18_out1, s(T24), s(T25)) → f18_out1
f19_in(T9, T10) → U3(f2_in(s(T9), T10), T9, T10)
U3(f2_out1, T9, T10) → f19_out1
f9_in(T9, T10) → U4(f18_in(T9, T10), T9, T10)
U4(f18_out1, T9, T10) → U5(f19_in(T9, T10), T9, T10)
U5(f19_out1, T9, T10) → f9_out1

The set Q consists of the following terms:

f2_in(x0, x1)
U1(f9_out1, x0, x1)
f18_in(0, s(x0))
f18_in(s(x0), s(x1))
U2(f18_out1, s(x0), s(x1))
f19_in(x0, x1)
U3(f2_out1, x0, x1)
f9_in(x0, x1)
U4(f18_out1, x0, x1)
U5(f19_out1, x0, x1)

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

(7) DependencyGraphProof (EQUIVALENT transformation)

The approximation of the Dependency Graph [LPAR04,FROCOS05,EDGSTAR] contains 2 SCCs with 5 less nodes.

(8) Complex Obligation (AND)

(9) Obligation:

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

F18_IN(s(T24), s(T25)) → F18_IN(T24, T25)

The TRS R consists of the following rules:

f2_in(T9, T10) → U1(f9_in(T9, T10), T9, T10)
U1(f9_out1, T9, T10) → f2_out1
f18_in(0, s(T19)) → f18_out1
f18_in(s(T24), s(T25)) → U2(f18_in(T24, T25), s(T24), s(T25))
U2(f18_out1, s(T24), s(T25)) → f18_out1
f19_in(T9, T10) → U3(f2_in(s(T9), T10), T9, T10)
U3(f2_out1, T9, T10) → f19_out1
f9_in(T9, T10) → U4(f18_in(T9, T10), T9, T10)
U4(f18_out1, T9, T10) → U5(f19_in(T9, T10), T9, T10)
U5(f19_out1, T9, T10) → f9_out1

The set Q consists of the following terms:

f2_in(x0, x1)
U1(f9_out1, x0, x1)
f18_in(0, s(x0))
f18_in(s(x0), s(x1))
U2(f18_out1, s(x0), s(x1))
f19_in(x0, x1)
U3(f2_out1, x0, x1)
f9_in(x0, x1)
U4(f18_out1, x0, x1)
U5(f19_out1, x0, x1)

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

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

(11) Obligation:

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

F18_IN(s(T24), s(T25)) → F18_IN(T24, T25)

R is empty.
The set Q consists of the following terms:

f2_in(x0, x1)
U1(f9_out1, x0, x1)
f18_in(0, s(x0))
f18_in(s(x0), s(x1))
U2(f18_out1, s(x0), s(x1))
f19_in(x0, x1)
U3(f2_out1, x0, x1)
f9_in(x0, x1)
U4(f18_out1, x0, x1)
U5(f19_out1, x0, x1)

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

(12) 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].

f2_in(x0, x1)
U1(f9_out1, x0, x1)
f18_in(0, s(x0))
f18_in(s(x0), s(x1))
U2(f18_out1, s(x0), s(x1))
f19_in(x0, x1)
U3(f2_out1, x0, x1)
f9_in(x0, x1)
U4(f18_out1, x0, x1)
U5(f19_out1, x0, x1)

(13) Obligation:

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

F18_IN(s(T24), s(T25)) → F18_IN(T24, T25)

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

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

• F18_IN(s(T24), s(T25)) → F18_IN(T24, T25)
  The graph contains the following edges 1 > 1, 2 > 2

(15) YES

(16) Obligation:

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

F2_IN(T9, T10) → F9_IN(T9, T10)
F9_IN(T9, T10) → U4¹(f18_in(T9, T10), T9, T10)
U4¹(f18_out1, T9, T10) → F19_IN(T9, T10)
F19_IN(T9, T10) → F2_IN(s(T9), T10)

The TRS R consists of the following rules:

f2_in(T9, T10) → U1(f9_in(T9, T10), T9, T10)
U1(f9_out1, T9, T10) → f2_out1
f18_in(0, s(T19)) → f18_out1
f18_in(s(T24), s(T25)) → U2(f18_in(T24, T25), s(T24), s(T25))
U2(f18_out1, s(T24), s(T25)) → f18_out1
f19_in(T9, T10) → U3(f2_in(s(T9), T10), T9, T10)
U3(f2_out1, T9, T10) → f19_out1
f9_in(T9, T10) → U4(f18_in(T9, T10), T9, T10)
U4(f18_out1, T9, T10) → U5(f19_in(T9, T10), T9, T10)
U5(f19_out1, T9, T10) → f9_out1

The set Q consists of the following terms:

f2_in(x0, x1)
U1(f9_out1, x0, x1)
f18_in(0, s(x0))
f18_in(s(x0), s(x1))
U2(f18_out1, s(x0), s(x1))
f19_in(x0, x1)
U3(f2_out1, x0, x1)
f9_in(x0, x1)
U4(f18_out1, x0, x1)
U5(f19_out1, x0, x1)

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

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

(18) Obligation:

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

F2_IN(T9, T10) → F9_IN(T9, T10)
F9_IN(T9, T10) → U4¹(f18_in(T9, T10), T9, T10)
U4¹(f18_out1, T9, T10) → F19_IN(T9, T10)
F19_IN(T9, T10) → F2_IN(s(T9), T10)

The TRS R consists of the following rules:

f18_in(0, s(T19)) → f18_out1
f18_in(s(T24), s(T25)) → U2(f18_in(T24, T25), s(T24), s(T25))
U2(f18_out1, s(T24), s(T25)) → f18_out1

The set Q consists of the following terms:

f2_in(x0, x1)
U1(f9_out1, x0, x1)
f18_in(0, s(x0))
f18_in(s(x0), s(x1))
U2(f18_out1, s(x0), s(x1))
f19_in(x0, x1)
U3(f2_out1, x0, x1)
f9_in(x0, x1)
U4(f18_out1, x0, x1)
U5(f19_out1, x0, x1)

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

(19) 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].

f2_in(x0, x1)
U1(f9_out1, x0, x1)
f19_in(x0, x1)
U3(f2_out1, x0, x1)
f9_in(x0, x1)
U4(f18_out1, x0, x1)
U5(f19_out1, x0, x1)

(20) Obligation:

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

F2_IN(T9, T10) → F9_IN(T9, T10)
F9_IN(T9, T10) → U4¹(f18_in(T9, T10), T9, T10)
U4¹(f18_out1, T9, T10) → F19_IN(T9, T10)
F19_IN(T9, T10) → F2_IN(s(T9), T10)

The TRS R consists of the following rules:

f18_in(0, s(T19)) → f18_out1
f18_in(s(T24), s(T25)) → U2(f18_in(T24, T25), s(T24), s(T25))
U2(f18_out1, s(T24), s(T25)) → f18_out1

The set Q consists of the following terms:

f18_in(0, s(x0))
f18_in(s(x0), s(x1))
U2(f18_out1, s(x0), s(x1))

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

(21) NonInfProof (EQUIVALENT transformation)

The DP Problem is simplified using the Induction Calculus [NONINF] with the following steps:
Note that final constraints are written in bold face.


For Pair F2_IN(T9, T10) → F9_IN(T9, T10) the following chains were created:

• We consider the chain F19_IN(T9, T10) → F2_IN(s(T9), T10), F2_IN(T9, T10) → F9_IN(T9, T10) which results in the following constraint:
  

  (1)    (F2_IN(s(x6), x7)=F2_IN(x8, x9) ⇒ F2_IN(x8, x9)≥F9_IN(x8, x9))

  
  
  We simplified constraint (1) using rules (I), (II), (III) which results in the following new constraint:
  

  (2)    (F2_IN(s(x6), x7)≥F9_IN(s(x6), x7))

  
  
  

For Pair F9_IN(T9, T10) → U4¹(f18_in(T9, T10), T9, T10) the following chains were created:

• We consider the chain F2_IN(T9, T10) → F9_IN(T9, T10), F9_IN(T9, T10) → U4¹(f18_in(T9, T10), T9, T10) which results in the following constraint:
  

  (3)    (F9_IN(x10, x11)=F9_IN(x12, x13) ⇒ F9_IN(x12, x13)≥U4¹(f18_in(x12, x13), x12, x13))

  
  
  We simplified constraint (3) using rules (I), (II), (III) which results in the following new constraint:
  

  (4)    (F9_IN(x10, x11)≥U4¹(f18_in(x10, x11), x10, x11))

  
  
  

For Pair U4¹(f18_out1, T9, T10) → F19_IN(T9, T10) the following chains were created:

• We consider the chain F9_IN(T9, T10) → U4¹(f18_in(T9, T10), T9, T10), U4¹(f18_out1, T9, T10) → F19_IN(T9, T10) which results in the following constraint:
  

  (5)    (U4¹(f18_in(x22, x23), x22, x23)=U4¹(f18_out1, x24, x25) ⇒ U4¹(f18_out1, x24, x25)≥F19_IN(x24, x25))

  
  
  We simplified constraint (5) using rules (I), (II), (III) which results in the following new constraint:
  

  (6)    (f18_in(x22, x23)=f18_out1 ⇒ U4¹(f18_out1, x22, x23)≥F19_IN(x22, x23))

  
  
  We simplified constraint (6) using rule (V) (with possible (I) afterwards) using induction on f18_in(x22, x23)=f18_out1 which results in the following new constraints:
  

  (7)    (f18_out1=f18_out1 ⇒ U4¹(f18_out1, 0, s(x40))≥F19_IN(0, s(x40)))

  
  

  (8)    (U2(f18_in(x42, x41), s(x42), s(x41))=f18_out1∧(f18_in(x42, x41)=f18_out1 ⇒ U4¹(f18_out1, x42, x41)≥F19_IN(x42, x41)) ⇒ U4¹(f18_out1, s(x42), s(x41))≥F19_IN(s(x42), s(x41)))

  
  
  We simplified constraint (7) using rules (I), (II) which results in the following new constraint:
  

  (9)    (U4¹(f18_out1, 0, s(x40))≥F19_IN(0, s(x40)))

  
  
  We simplified constraint (8) using rule (VII) which results in the following new constraint:
  

  (10)    (f18_in(x42, x41)=x43∧s(x42)=x44∧s(x41)=x45∧U2(x43, x44, x45)=f18_out1∧(f18_in(x42, x41)=f18_out1 ⇒ U4¹(f18_out1, x42, x41)≥F19_IN(x42, x41)) ⇒ U4¹(f18_out1, s(x42), s(x41))≥F19_IN(s(x42), s(x41)))

  
  
  We simplified constraint (10) using rule (V) (with possible (I) afterwards) using induction on U2(x43, x44, x45)=f18_out1 which results in the following new constraint:
  

  (11)    (f18_out1=f18_out1∧f18_in(x42, x41)=f18_out1∧s(x42)=s(x47)∧s(x41)=s(x46)∧(f18_in(x42, x41)=f18_out1 ⇒ U4¹(f18_out1, x42, x41)≥F19_IN(x42, x41)) ⇒ U4¹(f18_out1, s(x42), s(x41))≥F19_IN(s(x42), s(x41)))

  
  
  We simplified constraint (11) using rules (I), (II) which results in the following new constraint:
  

  (12)    (f18_in(x42, x41)=f18_out1∧x42=x47∧x41=x46∧(f18_in(x42, x41)=f18_out1 ⇒ U4¹(f18_out1, x42, x41)≥F19_IN(x42, x41)) ⇒ U4¹(f18_out1, s(x42), s(x41))≥F19_IN(s(x42), s(x41)))

  
  
  We simplified constraint (12) using rule (VI) where we applied the induction hypothesis (f18_in(x42, x41)=f18_out1 ⇒ U4¹(f18_out1, x42, x41)≥F19_IN(x42, x41)) with σ = [ ] which results in the following new constraint:
  

  (13)    (x42=x47∧x41=x46∧U4¹(f18_out1, x42, x41)≥F19_IN(x42, x41) ⇒ U4¹(f18_out1, s(x42), s(x41))≥F19_IN(s(x42), s(x41)))

  
  
  We simplified constraint (13) using rule (IV) which results in the following new constraint:
  

  (14)    (U4¹(f18_out1, x42, x41)≥F19_IN(x42, x41) ⇒ U4¹(f18_out1, s(x42), s(x41))≥F19_IN(s(x42), s(x41)))

  
  
  

For Pair F19_IN(T9, T10) → F2_IN(s(T9), T10) the following chains were created:

• We consider the chain U4¹(f18_out1, T9, T10) → F19_IN(T9, T10), F19_IN(T9, T10) → F2_IN(s(T9), T10) which results in the following constraint:
  

  (15)    (F19_IN(x34, x35)=F19_IN(x36, x37) ⇒ F19_IN(x36, x37)≥F2_IN(s(x36), x37))

  
  
  We simplified constraint (15) using rules (I), (II), (III) which results in the following new constraint:
  

  (16)    (F19_IN(x34, x35)≥F2_IN(s(x34), x35))

  
  
  

To summarize, we get the following constraints P_≥ for the following pairs.

• F2_IN(T9, T10) → F9_IN(T9, T10)
  
  • (F2_IN(s(x6), x7)≥F9_IN(s(x6), x7))
    
  
  
• F9_IN(T9, T10) → U4¹(f18_in(T9, T10), T9, T10)
  
  • (F9_IN(x10, x11)≥U4¹(f18_in(x10, x11), x10, x11))
    
  
  
• U4¹(f18_out1, T9, T10) → F19_IN(T9, T10)
  
  • (U4¹(f18_out1, 0, s(x40))≥F19_IN(0, s(x40)))
    
  • (U4¹(f18_out1, x42, x41)≥F19_IN(x42, x41) ⇒ U4¹(f18_out1, s(x42), s(x41))≥F19_IN(s(x42), s(x41)))
    
  
  
• F19_IN(T9, T10) → F2_IN(s(T9), T10)
  
  • (F19_IN(x34, x35)≥F2_IN(s(x34), x35))
    
  
  

The constraints for P_> respective P_bound are constructed from P_≥ where we just replace every occurence of "t ≥ s" in P_≥ by "t > s" respective "t ≥ c". Here c stands for the fresh constant used for P_bound.
Using the following integer polynomial ordering the resulting constraints can be solved
Polynomial interpretation [NONINF]:

POL(0) = 0   
POL(F19_IN(x₁, x₂)) = 1 - x₁ + x₂   
POL(F2_IN(x₁, x₂)) = 1 - x₁ + x₂   
POL(F9_IN(x₁, x₂)) = 1 - x₁ + x₂   
POL(U2(x₁, x₂, x₃)) = 0   
POL(U4¹(x₁, x₂, x₃)) = 1 - x₁ - x₂ + x₃   
POL(c) = -1   
POL(f18_in(x₁, x₂)) = 0   
POL(f18_out1) = 0   
POL(s(x₁)) = 1 + x₁   

The following pairs are in P_>:

F19_IN(T9, T10) → F2_IN(s(T9), T10)

The following pairs are in P_bound:

U4¹(f18_out1, T9, T10) → F19_IN(T9, T10)

The following rules are usable:

f18_out1 → f18_in(0, s(T19))
U2(f18_in(T24, T25), s(T24), s(T25)) → f18_in(s(T24), s(T25))
f18_out1 → U2(f18_out1, s(T24), s(T25))

(22) Complex Obligation (AND)

(23) Obligation:

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

F2_IN(T9, T10) → F9_IN(T9, T10)
F9_IN(T9, T10) → U4¹(f18_in(T9, T10), T9, T10)
U4¹(f18_out1, T9, T10) → F19_IN(T9, T10)

The TRS R consists of the following rules:

f18_in(0, s(T19)) → f18_out1
f18_in(s(T24), s(T25)) → U2(f18_in(T24, T25), s(T24), s(T25))
U2(f18_out1, s(T24), s(T25)) → f18_out1

The set Q consists of the following terms:

f18_in(0, s(x0))
f18_in(s(x0), s(x1))
U2(f18_out1, s(x0), s(x1))

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

(24) DependencyGraphProof (EQUIVALENT transformation)

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

(25) TRUE

(26) Obligation:

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

F2_IN(T9, T10) → F9_IN(T9, T10)
F9_IN(T9, T10) → U4¹(f18_in(T9, T10), T9, T10)
F19_IN(T9, T10) → F2_IN(s(T9), T10)

The TRS R consists of the following rules:

f18_in(0, s(T19)) → f18_out1
f18_in(s(T24), s(T25)) → U2(f18_in(T24, T25), s(T24), s(T25))
U2(f18_out1, s(T24), s(T25)) → f18_out1

The set Q consists of the following terms:

f18_in(0, s(x0))
f18_in(s(x0), s(x1))
U2(f18_out1, s(x0), s(x1))

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

(27) DependencyGraphProof (EQUIVALENT transformation)

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

(28) TRUE