YES
  TPA v.1.0

Result: TRS is terminating

Default interpretations for symbols are not printed. For polynomial interpretations
and semantic labelling over N\{0,1} defaults are 2 for constants, identity for unary
symbols and x+y-2 for binary symbols. For semantic labelling over {0,1} (booleans)
defaults are 0 for constants, identity for unary symbols and disjunction for binary symbols.

[1]  TRS loaded from input file:
(1) app(nil,k) -> k
(2) app(l,nil) -> l
(3) app(cons(x,l),k) -> cons(x,app(l,k))
(4) sum(cons(x,nil)) -> cons(x,nil)
(5) sum(cons(x,cons(y,l))) -> sum(cons(plus(x,y),l))
(6) sum(app(l,cons(x,cons(y,k)))) -> sum(app(l,sum(cons(x,cons(y,k)))))
(7) plus(0,y) -> y
(8) plus(s(x),y) -> s(plus(x,y))
(9) sum(plus(cons(0,x),cons(y,l))) -> pred(sum(cons(s(x),cons(y,l))))
(10) pred(cons(s(x),nil)) -> cons(x,nil)

[2]  Use following polynomial interpretation:
[0] = 3
rest default

  Remove rules with left hand side strictly bigger than right hand side:
(7), (9)

[3]  Use following polynomial interpretation:
[pred(x)] = x + 1
rest default

  Remove rules with left hand side strictly bigger than right hand side:
(10)

[4]  Use following polynomial interpretation:
[cons(x,y)] = x + y + 1
rest default

  Remove rules with left hand side strictly bigger than right hand side:
(5)

[5]  Use following polynomial interpretation:
[app(x,y)] = x + y + 1
rest default

  Remove rules with left hand side strictly bigger than right hand side:
(1)-(2)

[6]  Use following polynomial interpretation:
[plus(x,y)] = xy
[s(x)] = x + 1
rest default

  Remove rules with left hand side strictly bigger than right hand side:
(8)

[7]  Label this TRS using following interpretation over N\{0,1}:
[cons(x,y)] = x + y + 1
rest default

  This interpretation is a model and yields following TRS:
(3) app{j + k + 1,i}(cons{k,j}(x,l),k) -> cons{k,i + j - 2}(x,app{j,i}(l,k))
(4) sum{3 + k}(cons{k,2}(x,nil)) -> cons{k,2}(x,nil)
(6) sum{k + j + l0 + i}(app{j,l0 + k + i + 2}(l,cons{k,i + l0 + 1}(x,cons{l0,i}(y,k)))) -> sum{k + j + l0 + i}(app{j,l0 + k + i + 2}(l,sum{l0 + k + i + 2}(cons{k,i + l0 + 1}(x,cons{l0,i}(y,k)))))

[8]  Use following polynomial interpretation:
[app_{i,j}(x,y)] = x + y - 2 + i + j
[cons_{i,j}(x,y)] = x + y - 2
[sum_{i}(x)] = x
rest default

  Remove rules with left hand side strictly bigger than right hand side:
(3)

[9]  Unlabel this TRS to obtain the one consisting of the rules:
(4), (6)

[10]  Apply the Dependency Pair transformation resulting in the following dependency pairs:
<Sum(app(l,cons(x,cons(y,k)))), Sum(app(l,sum(cons(x,cons(y,k)))))>
<Sum(app(l,cons(x,cons(y,k)))), Sum(cons(x,cons(y,k)))>
 and 1 SCCs in the dependency graph. Proofs for those SCCs follow.

[10a-1]  Consider the following SCC obtained from analysis of dependency graph:
(4) sum(cons(x,nil)) ->= cons(x,nil)
(6) sum(app(l,cons(x,cons(y,k)))) ->= sum(app(l,sum(cons(x,cons(y,k)))))
(DP1) Sum(app(l,cons(x,cons(y,k)))) -> Sum(app(l,sum(cons(x,cons(y,k)))))

[10a-2]  Use following polynomial interpretation:
[cons(x,y)] = y + 1
[sum(x)] = 3
rest default

  Remove rules with left hand side strictly bigger than right hand side:
(DP1)

[10a-3]  Since there are no remaining strict rules, relative termination is proved!



../tpdb/TRS/AG01/#3.17a.trs, 0.01, Y
Couldn't open file <60>: 60: No such file or directory