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'(app'(minus,x),0) -> x
(2) app'(app'(minus,app'(s,x)),app'(s,y)) -> app'(app'(minus,x),y)
(3) app'(app'(minus,app'(app'(minus,x),y)),z) -> app'(app'(minus,x),app'(app'(plus,y),z))
(4) app'(app'(quot,0),app'(s,y)) -> 0
(5) app'(app'(quot,app'(s,x)),app'(s,y)) -> app'(s,app'(app'(quot,app'(app'(minus,x),y)),app'(s,y)))
(6) app'(app'(plus,0),y) -> y
(7) app'(app'(plus,app'(s,x)),y) -> app'(s,app'(app'(plus,x),y))
(8) app'(app'(app,nil),k) -> k
(9) app'(app'(app,l),nil) -> l
(10) app'(app'(app,app'(app'(cons,x),l)),k) -> app'(app'(cons,x),app'(app'(app,l),k))
(11) app'(sum,app'(app'(cons,x),nil)) -> app'(app'(cons,x),nil)
(12) app'(sum,app'(app'(cons,x),app'(app'(cons,y),l))) -> app'(sum,app'(app'(cons,app'(app'(plus,x),y)),l))
(13) app'(sum,app'(app'(app,l),app'(app'(cons,x),app'(app'(cons,y),k)))) -> app'(sum,app'(app'(app,l),app'(sum,app'(app'(cons,x),app'(app'(cons,y),k)))))

[2]  Apply uncurrying transformation with <app'> as function application symbol to obtain the following TRS:
(1) minus(x,0) -> x
(2) minus(s(x),s(y)) -> minus(x,y)
(3) minus(minus(x,y),z) -> minus(x,plus(y,z))
(4) quot(0,s(y)) -> 0
(5) quot(s(x),s(y)) -> s(quot(minus(x,y),s(y)))
(6) plus(0,y) -> y
(7) plus(s(x),y) -> s(plus(x,y))
(8) app(nil,k) -> k
(9) app(l,nil) -> l
(10) app(cons(x,l),k) -> cons(x,app(l,k))
(11) sum(cons(x,nil)) -> cons(x,nil)
(12) sum(cons(x,cons(y,l))) -> sum(cons(plus(x,y),l))
(13) sum(app(l,cons(x,cons(y,k)))) -> sum(app(l,sum(cons(x,cons(y,k)))))

[3]  Apply the Dependency Pair transformation resulting in the following dependency pairs:
<Minus(s(x),s(y)), Minus(x,y)>
<Minus(minus(x,y),z), Minus(x,plus(y,z))>
<Minus(minus(x,y),z), Plus(y,z)>
<Quot(s(x),s(y)), Quot(minus(x,y),s(y))>
<Quot(s(x),s(y)), Minus(x,y)>
<Plus(s(x),y), Plus(x,y)>
<App(cons(x,l),k), App(l,k)>
<Sum(cons(x,cons(y,l))), Sum(cons(plus(x,y),l))>
<Sum(cons(x,cons(y,l))), Plus(x,y)>
<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)))), App(l,sum(cons(x,cons(y,k))))>
<Sum(app(l,cons(x,cons(y,k)))), Sum(cons(x,cons(y,k)))>
 and 6 SCCs in the dependency graph. Proofs for those SCCs follow.

[3a-1]  Consider the following SCC obtained from analysis of dependency graph:
(1) minus(x,0) ->= x
(2) minus(s(x),s(y)) ->= minus(x,y)
(3) minus(minus(x,y),z) ->= minus(x,plus(y,z))
(4) quot(0,s(y)) ->= 0
(5) quot(s(x),s(y)) ->= s(quot(minus(x,y),s(y)))
(6) plus(0,y) ->= y
(7) plus(s(x),y) ->= s(plus(x,y))
(8) app(nil,k) ->= k
(9) app(l,nil) ->= l
(10) app(cons(x,l),k) ->= cons(x,app(l,k))
(11) sum(cons(x,nil)) ->= cons(x,nil)
(12) sum(cons(x,cons(y,l))) ->= sum(cons(plus(x,y),l))
(13) sum(app(l,cons(x,cons(y,k)))) ->= sum(app(l,sum(cons(x,cons(y,k)))))
(DP4) Quot(s(x),s(y)) -> Quot(minus(x,y),s(y))

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

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

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

[3b-1]  Consider the following SCC obtained from analysis of dependency graph:
(1) minus(x,0) ->= x
(2) minus(s(x),s(y)) ->= minus(x,y)
(3) minus(minus(x,y),z) ->= minus(x,plus(y,z))
(4) quot(0,s(y)) ->= 0
(5) quot(s(x),s(y)) ->= s(quot(minus(x,y),s(y)))
(6) plus(0,y) ->= y
(7) plus(s(x),y) ->= s(plus(x,y))
(8) app(nil,k) ->= k
(9) app(l,nil) ->= l
(10) app(cons(x,l),k) ->= cons(x,app(l,k))
(11) sum(cons(x,nil)) ->= cons(x,nil)
(12) sum(cons(x,cons(y,l))) ->= sum(cons(plus(x,y),l))
(13) sum(app(l,cons(x,cons(y,k)))) ->= sum(app(l,sum(cons(x,cons(y,k)))))
(DP10) Sum(app(l,cons(x,cons(y,k)))) -> Sum(app(l,sum(cons(x,cons(y,k)))))

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

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

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

[3c-1]  Consider the following SCC obtained from analysis of dependency graph:
(1) minus(x,0) ->= x
(2) minus(s(x),s(y)) ->= minus(x,y)
(3) minus(minus(x,y),z) ->= minus(x,plus(y,z))
(4) quot(0,s(y)) ->= 0
(5) quot(s(x),s(y)) ->= s(quot(minus(x,y),s(y)))
(6) plus(0,y) ->= y
(7) plus(s(x),y) ->= s(plus(x,y))
(8) app(nil,k) ->= k
(9) app(l,nil) ->= l
(10) app(cons(x,l),k) ->= cons(x,app(l,k))
(11) sum(cons(x,nil)) ->= cons(x,nil)
(12) sum(cons(x,cons(y,l))) ->= sum(cons(plus(x,y),l))
(13) sum(app(l,cons(x,cons(y,k)))) ->= sum(app(l,sum(cons(x,cons(y,k)))))
(DP8) Sum(cons(x,cons(y,l))) -> Sum(cons(plus(x,y),l))

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

  Remove rules with left hand side strictly bigger than right hand side:
(12), (DP8)

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

[3d-1]  Consider the following SCC obtained from analysis of dependency graph:
(1) minus(x,0) ->= x
(2) minus(s(x),s(y)) ->= minus(x,y)
(3) minus(minus(x,y),z) ->= minus(x,plus(y,z))
(4) quot(0,s(y)) ->= 0
(5) quot(s(x),s(y)) ->= s(quot(minus(x,y),s(y)))
(6) plus(0,y) ->= y
(7) plus(s(x),y) ->= s(plus(x,y))
(8) app(nil,k) ->= k
(9) app(l,nil) ->= l
(10) app(cons(x,l),k) ->= cons(x,app(l,k))
(11) sum(cons(x,nil)) ->= cons(x,nil)
(12) sum(cons(x,cons(y,l))) ->= sum(cons(plus(x,y),l))
(13) sum(app(l,cons(x,cons(y,k)))) ->= sum(app(l,sum(cons(x,cons(y,k)))))
(DP7) App(cons(x,l),k) -> App(l,k)

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

  Remove rules with left hand side strictly bigger than right hand side:
(12), (DP7)

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

[3e-1]  Consider the following SCC obtained from analysis of dependency graph:
(1) minus(x,0) ->= x
(2) minus(s(x),s(y)) ->= minus(x,y)
(3) minus(minus(x,y),z) ->= minus(x,plus(y,z))
(4) quot(0,s(y)) ->= 0
(5) quot(s(x),s(y)) ->= s(quot(minus(x,y),s(y)))
(6) plus(0,y) ->= y
(7) plus(s(x),y) ->= s(plus(x,y))
(8) app(nil,k) ->= k
(9) app(l,nil) ->= l
(10) app(cons(x,l),k) ->= cons(x,app(l,k))
(11) sum(cons(x,nil)) ->= cons(x,nil)
(12) sum(cons(x,cons(y,l))) ->= sum(cons(plus(x,y),l))
(13) sum(app(l,cons(x,cons(y,k)))) ->= sum(app(l,sum(cons(x,cons(y,k)))))
(DP2) Minus(minus(x,y),z) -> Minus(x,plus(y,z))
(DP1) Minus(s(x),s(y)) -> Minus(x,y)

[3e-2]  Use following polynomial interpretation:
[minus(x,y)] = x + 1
[s(x)] = x + 2
[quot(x,y)] = 2x - 2
[Minus(x,y)] = x
rest default

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

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

[3f-1]  Consider the following SCC obtained from analysis of dependency graph:
(1) minus(x,0) ->= x
(2) minus(s(x),s(y)) ->= minus(x,y)
(3) minus(minus(x,y),z) ->= minus(x,plus(y,z))
(4) quot(0,s(y)) ->= 0
(5) quot(s(x),s(y)) ->= s(quot(minus(x,y),s(y)))
(6) plus(0,y) ->= y
(7) plus(s(x),y) ->= s(plus(x,y))
(8) app(nil,k) ->= k
(9) app(l,nil) ->= l
(10) app(cons(x,l),k) ->= cons(x,app(l,k))
(11) sum(cons(x,nil)) ->= cons(x,nil)
(12) sum(cons(x,cons(y,l))) ->= sum(cons(plus(x,y),l))
(13) sum(app(l,cons(x,cons(y,k)))) ->= sum(app(l,sum(cons(x,cons(y,k)))))
(DP6) Plus(s(x),y) -> Plus(x,y)

[3f-2]  Use following polynomial interpretation:
[minus(x,y)] = x
[s(x)] = x + 1
rest default

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

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



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