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(perfectp,0) -> false
(2) app(perfectp,app(s,x)) -> app(app(app(app(f,x),app(s,0)),app(s,x)),app(s,x))
(3) app(app(app(app(f,0),y),0),u) -> true
(4) app(app(app(app(f,0),y),app(s,z)),u) -> false
(5) app(app(app(app(f,app(s,x)),0),z),u) -> app(app(app(app(f,x),u),app(app(minus,z),app(s,x))),u)
(6) app(app(app(app(f,app(s,x)),app(s,y)),z),u) -> app(app(app(if,app(app(le,x),y)),app(app(app(app(f,app(s,x)),app(app(minus,y),x)),z),u)),app(app(app(app(f,x),u),z),u))

[2]  Apply uncurrying transformation with <app> as function application symbol to obtain the following TRS:
(1) perfectp(0) -> false
(2) perfectp(s(x)) -> f`1(x,f`2(s(0),f`3(s(x),s(x))))
(3) f`1(0,f`2(y,f`3(0,u))) -> true
(4) f`1(0,f`2(y,f`3(s(z),u))) -> false
(5) f`1(s(x),f`2(0,f`3(z,u))) -> f`1(x,f`2(u,f`3(minus(z,s(x)),u)))
(6) f`1(s(x),f`2(s(y),f`3(z,u))) -> if`1(le(x,y),if`2(f`1(s(x),f`2(minus(y,x),f`3(z,u))),f`1(x,f`2(u,f`3(z,u)))))

[3]  Eliminate dummy symbol <le>, to obtain the following TRS:
(1) perfectp(0) -> false
(2) perfectp(s(x)) -> f`1(x,f`2(s(0),f`3(s(x),s(x))))
(3) f`1(0,f`2(y,f`3(0,u))) -> true
(4) f`1(0,f`2(y,f`3(s(z),u))) -> false
(5) f`1(s(x),f`2(0,f`3(z,u))) -> f`1(x,f`2(u,f`3(minus(z,s(x)),u)))
(6a) f`1(s(x),f`2(s(y),f`3(z,u))) -> if`1(#0,if`2(f`1(s(x),f`2(minus(y,x),f`3(z,u))),f`1(x,f`2(u,f`3(z,u)))))
(6b) f`1(s(x),f`2(s(y),f`3(z,u))) -> #1(x)
(6c) f`1(s(x),f`2(s(y),f`3(z,u))) -> #2(y)

[4]  Eliminate dummy symbol <minus>, to obtain the following TRS:
(1) perfectp(0) -> false
(2) perfectp(s(x)) -> f`1(x,f`2(s(0),f`3(s(x),s(x))))
(3) f`1(0,f`2(y,f`3(0,u))) -> true
(4) f`1(0,f`2(y,f`3(s(z),u))) -> false
(5a) f`1(s(x),f`2(0,f`3(z,u))) -> f`1(x,f`2(u,f`3(#3,u)))
(5b) f`1(s(x),f`2(0,f`3(z,u))) -> #4(z)
(5c) f`1(s(x),f`2(0,f`3(z,u))) -> #5(s(x))
(6aa) f`1(s(x),f`2(s(y),f`3(z,u))) -> if`1(#0,if`2(f`1(s(x),f`2(#6,f`3(z,u))),f`1(x,f`2(u,f`3(z,u)))))
(6ab) f`1(s(x),f`2(s(y),f`3(z,u))) -> #7(y)
(6ac) f`1(s(x),f`2(s(y),f`3(z,u))) -> #8(x)
(6b) f`1(s(x),f`2(s(y),f`3(z,u))) -> #1(x)
(6c) f`1(s(x),f`2(s(y),f`3(z,u))) -> #2(y)

[5]  Eliminate dummy symbol <if`2>, to obtain the following TRS:
(1) perfectp(0) -> false
(2) perfectp(s(x)) -> f`1(x,f`2(s(0),f`3(s(x),s(x))))
(3) f`1(0,f`2(y,f`3(0,u))) -> true
(4) f`1(0,f`2(y,f`3(s(z),u))) -> false
(5a) f`1(s(x),f`2(0,f`3(z,u))) -> f`1(x,f`2(u,f`3(#3,u)))
(5b) f`1(s(x),f`2(0,f`3(z,u))) -> #4(z)
(5c) f`1(s(x),f`2(0,f`3(z,u))) -> #5(s(x))
(6aaa) f`1(s(x),f`2(s(y),f`3(z,u))) -> if`1(#0,#9)
(6aab) f`1(s(x),f`2(s(y),f`3(z,u))) -> #10(f`1(s(x),f`2(#6,f`3(z,u))))
(6aac) f`1(s(x),f`2(s(y),f`3(z,u))) -> #11(f`1(x,f`2(u,f`3(z,u))))
(6ab) f`1(s(x),f`2(s(y),f`3(z,u))) -> #7(y)
(6ac) f`1(s(x),f`2(s(y),f`3(z,u))) -> #8(x)
(6b) f`1(s(x),f`2(s(y),f`3(z,u))) -> #1(x)
(6c) f`1(s(x),f`2(s(y),f`3(z,u))) -> #2(y)

[6]  All the rules of this TRS can be oriented with RPO with the following precedence:
Status: f`1: Lex-LR, f`2: Lex-LR, 
Precedence:
perfectp > 0
perfectp > false
perfectp > s
perfectp > f`1
perfectp > f`2
perfectp > f`3
f`1 > false
s > #6
f`1 > f`2
f`1 > f`3
f`1 > true
f`1 > if`1
f`1 > #0
f`1 > #1
f`1 > #2
f`1 > #3
f`1 > #4
f`1 > #5
f`1 > #7
f`1 > #8
f`1 > #9
f`1 > #10
f`1 > #11


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