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) is_empty(nil) -> true
(2) is_empty(cons(x,l)) -> false
(3) hd(cons(x,l)) -> x
(4) tl(cons(x,l)) -> l
(5) append(l1,l2) -> ifappend`1(l1,ifappend`2(l2,l1))
(6) ifappend`1(l1,ifappend`2(l2,nil)) -> l2
(7) ifappend`1(l1,ifappend`2(l2,cons(x,l))) -> cons(x,append(l,l2))

[2]  Apply the Dependency Pair transformation resulting in the following dependency pairs:
<Append(l1,l2), Ifappend`1(l1,ifappend`2(l2,l1))>
<Ifappend`1(l1,ifappend`2(l2,cons(x,l))), Append(l,l2)>
 and 1 SCCs in the dependency graph. Proofs for those SCCs follow.

[2a-1]  Consider the following SCC obtained from analysis of dependency graph:
(1) is_empty(nil) ->= true
(2) is_empty(cons(x,l)) ->= false
(3) hd(cons(x,l)) ->= x
(4) tl(cons(x,l)) ->= l
(5) append(l1,l2) ->= ifappend`1(l1,ifappend`2(l2,l1))
(6) ifappend`1(l1,ifappend`2(l2,nil)) ->= l2
(7) ifappend`1(l1,ifappend`2(l2,cons(x,l))) ->= cons(x,append(l,l2))
(DP2) Ifappend`1(l1,ifappend`2(l2,cons(x,l))) -> Append(l,l2)
(DP1) Append(l1,l2) -> Ifappend`1(l1,ifappend`2(l2,l1))

[2a-2]  Use following polynomial interpretation:
[cons(x,y)] = x + y + 1
[ifappend`1(x,y)] = y
[Append(x,y)] = x + y + 1
[Ifappend`1(x,y)] = y + 1
rest default

  Remove rules with left hand side strictly bigger than right hand side:
(2)-(4), (DP2), (DP1)

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



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