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) minus(n__0,Y) -> 0
(2) minus(n__s(X),n__s(Y)) -> minus(activate(X),activate(Y))
(3) geq(X,n__0) -> true
(4) geq(n__0,n__s(Y)) -> false
(5) geq(n__s(X),n__s(Y)) -> geq(activate(X),activate(Y))
(6) div(0,n__s(Y)) -> 0
(7) div(s(X),n__s(Y)) -> if`1(geq(X,activate(Y)),if`2(n__s(div(minus(X,activate(Y)),n__s(activate(Y)))),n__0))
(8) if`1(true,if`2(X,Y)) -> activate(X)
(9) if`1(false,if`2(X,Y)) -> activate(Y)
(10) 0 -> n__0
(11) s(X) -> n__s(X)
(12) activate(n__0) -> 0
(13) activate(n__s(X)) -> s(X)
(14) activate(X) -> X

[2]  Apply the Dependency Pair transformation resulting in the following dependency pairs:
<Minus(n__0,Y), 0~>
<Minus(n__s(X),n__s(Y)), Minus(activate(X),activate(Y))>
<Minus(n__s(X),n__s(Y)), Activate(X)>
<Minus(n__s(X),n__s(Y)), Activate(Y)>
<Geq(n__s(X),n__s(Y)), Geq(activate(X),activate(Y))>
<Geq(n__s(X),n__s(Y)), Activate(X)>
<Geq(n__s(X),n__s(Y)), Activate(Y)>
<Div(0,n__s(Y)), 0~>
<Div(s(X),n__s(Y)), If`1(geq(X,activate(Y)),if`2(n__s(div(minus(X,activate(Y)),n__s(activate(Y)))),n__0))>
<Div(s(X),n__s(Y)), Geq(X,activate(Y))>
<Div(s(X),n__s(Y)), Activate(Y)>
<Div(s(X),n__s(Y)), Div(minus(X,activate(Y)),n__s(activate(Y)))>
<Div(s(X),n__s(Y)), Minus(X,activate(Y))>
<Div(s(X),n__s(Y)), Activate(Y)>
<Div(s(X),n__s(Y)), Activate(Y)>
<If`1(true,if`2(X,Y)), Activate(X)>
<If`1(false,if`2(X,Y)), Activate(Y)>
<Activate(n__0), 0~>
<Activate(n__s(X)), S(X)>
 and 3 SCCs in the dependency graph. Proofs for those SCCs follow.

[2a-1]  Consider the following SCC obtained from analysis of dependency graph:
(1) minus(n__0,Y) ->= 0
(2) minus(n__s(X),n__s(Y)) ->= minus(activate(X),activate(Y))
(3) geq(X,n__0) ->= true
(4) geq(n__0,n__s(Y)) ->= false
(5) geq(n__s(X),n__s(Y)) ->= geq(activate(X),activate(Y))
(6) div(0,n__s(Y)) ->= 0
(7) div(s(X),n__s(Y)) ->= if`1(geq(X,activate(Y)),if`2(n__s(div(minus(X,activate(Y)),n__s(activate(Y)))),n__0))
(8) if`1(true,if`2(X,Y)) ->= activate(X)
(9) if`1(false,if`2(X,Y)) ->= activate(Y)
(10) 0 ->= n__0
(11) s(X) ->= n__s(X)
(12) activate(n__0) ->= 0
(13) activate(n__s(X)) ->= s(X)
(14) activate(X) ->= X
(DP12) Div(s(X),n__s(Y)) -> Div(minus(X,activate(Y)),n__s(activate(Y)))

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

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

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

[2b-1]  Consider the following SCC obtained from analysis of dependency graph:
(1) minus(n__0,Y) ->= 0
(2) minus(n__s(X),n__s(Y)) ->= minus(activate(X),activate(Y))
(3) geq(X,n__0) ->= true
(4) geq(n__0,n__s(Y)) ->= false
(5) geq(n__s(X),n__s(Y)) ->= geq(activate(X),activate(Y))
(6) div(0,n__s(Y)) ->= 0
(7) div(s(X),n__s(Y)) ->= if`1(geq(X,activate(Y)),if`2(n__s(div(minus(X,activate(Y)),n__s(activate(Y)))),n__0))
(8) if`1(true,if`2(X,Y)) ->= activate(X)
(9) if`1(false,if`2(X,Y)) ->= activate(Y)
(10) 0 ->= n__0
(11) s(X) ->= n__s(X)
(12) activate(n__0) ->= 0
(13) activate(n__s(X)) ->= s(X)
(14) activate(X) ->= X
(DP2) Minus(n__s(X),n__s(Y)) -> Minus(activate(X),activate(Y))

[2b-2]  Use following polynomial interpretation:
[minus(x,y)] = x
[n__s(x)] = x + 1
[s(x)] = x + 1
[if`1(x,y)] = y
rest default

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

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

[2c-1]  Consider the following SCC obtained from analysis of dependency graph:
(1) minus(n__0,Y) ->= 0
(2) minus(n__s(X),n__s(Y)) ->= minus(activate(X),activate(Y))
(3) geq(X,n__0) ->= true
(4) geq(n__0,n__s(Y)) ->= false
(5) geq(n__s(X),n__s(Y)) ->= geq(activate(X),activate(Y))
(6) div(0,n__s(Y)) ->= 0
(7) div(s(X),n__s(Y)) ->= if`1(geq(X,activate(Y)),if`2(n__s(div(minus(X,activate(Y)),n__s(activate(Y)))),n__0))
(8) if`1(true,if`2(X,Y)) ->= activate(X)
(9) if`1(false,if`2(X,Y)) ->= activate(Y)
(10) 0 ->= n__0
(11) s(X) ->= n__s(X)
(12) activate(n__0) ->= 0
(13) activate(n__s(X)) ->= s(X)
(14) activate(X) ->= X
(DP5) Geq(n__s(X),n__s(Y)) -> Geq(activate(X),activate(Y))

[2c-2]  Use following polynomial interpretation:
[minus(x,y)] = x
[n__s(x)] = x + 1
[s(x)] = x + 1
[if`1(x,y)] = y
rest default

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

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



../tpdb/TRS/TRCSR/Ex49_GM04_Z.trs, 0.02, Y
Couldn't open file <60>: 60: No such file or directory