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) intlist(nil) -> nil
(2) int(s(x),0) -> nil
(3) int(x,x) -> cons(x,nil)
(4) intlist(cons(x,y)) -> cons(s(x),intlist(y))
(5) int(s(x),s(y)) -> intlist(int(x,y))
(6) int(0,s(y)) -> cons(0,int(s(0),s(y)))
(7) intlist(cons(x,nil)) -> cons(s(x),nil)

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

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

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

  This interpretation is a model and yields following TRS:
(1) intlist{2}(nil) -> nil
(4) intlist{2}(cons{i,j}(x,y)) -> cons{i + 1,j}(s{i}(x),intlist{j}(y))
(5) int{i + 1,j + 1}(s{i}(x),s{j}(y)) -> intlist{2}(int{i,j}(x,y))
(6) int{2,j + 1}(0,s{j}(y)) -> cons{2,2}(0,int{3,j + 1}(s{2}(0),s{j}(y)))
(7) intlist{2}(cons{i,2}(x,nil)) -> cons{i + 1,2}(s{i}(x),nil)

[4]  Use following polynomial interpretation:
[intlist_{i}(x)] = x
[int_{i,j}(x,y)] = x + y - 2 + j
[s_{i}(x)] = x
[cons_{i,j}(x,y)] = x + y - 2
rest default

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

[5]  Unlabel this TRS to obtain the one consisting of the rules:
(1), (4), (6)-(7)

[6]  Use following polynomial interpretation:
[intlist(x)] = x + 1
rest default

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

[7]  Label this TRS using following interpretation that is a model:
[intlist(x)] = 0
[int(x,y)] = 0
[s(x)] = 0
[0] = 1
[cons(x,y)] = 0
rest default

  thus obtaining new TRS:
(4a) intlist$0(cons$11(x,y)) -> cons$00(s$1(x),intlist$1(y))
(4b) intlist$0(cons$10(x,y)) -> cons$00(s$1(x),intlist$0(y))
(4c) intlist$0(cons$01(x,y)) -> cons$00(s$0(x),intlist$1(y))
(4d) intlist$0(cons$00(x,y)) -> cons$00(s$0(x),intlist$0(y))
(6a) int$10(0,s$1(y)) -> cons$10(0,int$00(s$1(0),s$1(y)))
(6b) int$10(0,s$0(y)) -> cons$10(0,int$00(s$1(0),s$0(y)))

[8]  Use following polynomial interpretation:
[int$10(x,y)] = x + y + 1
rest default

  Remove rules with left hand side strictly bigger than right hand side:
(6a)-(6b)

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

[10]  All the rules of this TRS can be oriented with RPO with the following precedence:
Precedence:
intlist > s
intlist > cons


../tpdb/TRS/AProVE/LPAR_intlist.trs, 0.01, Y
Couldn't open file <60>: 60: No such file or directory