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(f,app(app(cons,nil),y)) -> y
(2) app(f,app(app(cons,app(f,app(app(cons,nil),y))),z)) -> app(app(app(copy,n),y),z)
(3) app(app(app(copy,0),y),z) -> app(f,z)
(4) app(app(app(copy,app(s,x)),y),z) -> app(app(app(copy,x),y),app(app(cons,app(f,y)),z))

[2]  Apply uncurrying transformation with <app> as function application symbol to obtain the following TRS:
(1) f(cons(nil,y)) -> y
(2) f(cons(f(cons(nil,y)),z)) -> copy`1(n,copy`2(y,z))
(3) copy`1(0,copy`2(y,z)) -> f(z)
(4) copy`1(s(x),copy`2(y,z)) -> copy`1(x,copy`2(y,cons(f(y),z)))

[3]  Apply the Dependency Pair transformation resulting in the following dependency pairs:
<F(cons(f(cons(nil,y)),z)), Copy`1(n,copy`2(y,z))>
<Copy`1(0,copy`2(y,z)), F(z)>
<Copy`1(s(x),copy`2(y,z)), Copy`1(x,copy`2(y,cons(f(y),z)))>
<Copy`1(s(x),copy`2(y,z)), F(y)>
 and 1 SCCs in the dependency graph. Proofs for those SCCs follow.

[3a-1]  Consider the following SCC obtained from analysis of dependency graph:
(1) f(cons(nil,y)) ->= y
(2) f(cons(f(cons(nil,y)),z)) ->= copy`1(n,copy`2(y,z))
(3) copy`1(0,copy`2(y,z)) ->= f(z)
(4) copy`1(s(x),copy`2(y,z)) ->= copy`1(x,copy`2(y,cons(f(y),z)))
(DP3) Copy`1(s(x),copy`2(y,z)) -> Copy`1(x,copy`2(y,cons(f(y),z)))

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

  Remove rules with left hand side strictly bigger than right hand side:
(4), (DP3)

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



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