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) from(X) -> cons(X,n__from(s(X)))
(2) first(0,Z) -> nil
(3) first(s(X),cons(Y,Z)) -> cons(Y,n__first(X,activate(Z)))
(4) sel(0,cons(X,Z)) -> X
(5) sel(s(X),cons(Y,Z)) -> sel(X,activate(Z))
(6) from(X) -> n__from(X)
(7) first(X1,X2) -> n__first(X1,X2)
(8) activate(n__from(X)) -> from(X)
(9) activate(n__first(X1,X2)) -> first(X1,X2)
(10) activate(X) -> X

[2]  Apply the Dependency Pair transformation resulting in the following dependency pairs:
<First(s(X),cons(Y,Z)), Activate(Z)>
<Sel(s(X),cons(Y,Z)), Sel(X,activate(Z))>
<Sel(s(X),cons(Y,Z)), Activate(Z)>
<Activate(n__from(X)), From(X)>
<Activate(n__first(X1,X2)), First(X1,X2)>
 and 2 SCCs in the dependency graph. Proofs for those SCCs follow.

[2a-1]  Consider the following SCC obtained from analysis of dependency graph:
(1) from(X) ->= cons(X,n__from(s(X)))
(2) first(0,Z) ->= nil
(3) first(s(X),cons(Y,Z)) ->= cons(Y,n__first(X,activate(Z)))
(4) sel(0,cons(X,Z)) ->= X
(5) sel(s(X),cons(Y,Z)) ->= sel(X,activate(Z))
(6) from(X) ->= n__from(X)
(7) first(X1,X2) ->= n__first(X1,X2)
(8) activate(n__from(X)) ->= from(X)
(9) activate(n__first(X1,X2)) ->= first(X1,X2)
(10) activate(X) ->= X
(DP2) Sel(s(X),cons(Y,Z)) -> Sel(X,activate(Z))

[2a-2]  Use following polynomial interpretation:
[from(x)] = x + 1
[cons(x,y)] = max(x, y)
[s(x)] = x + 1
[activate(x)] = x + 1
[Sel(x,y)] = x
rest default

  Remove rules with left hand side strictly bigger than right hand side:
(3<<), (6), (9)-(10), (DP2<), (DP2>)

[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) from(X) ->= cons(X,n__from(s(X)))
(2) first(0,Z) ->= nil
(3) first(s(X),cons(Y,Z)) ->= cons(Y,n__first(X,activate(Z)))
(4) sel(0,cons(X,Z)) ->= X
(5) sel(s(X),cons(Y,Z)) ->= sel(X,activate(Z))
(6) from(X) ->= n__from(X)
(7) first(X1,X2) ->= n__first(X1,X2)
(8) activate(n__from(X)) ->= from(X)
(9) activate(n__first(X1,X2)) ->= first(X1,X2)
(10) activate(X) ->= X
(DP5) Activate(n__first(X1,X2)) -> First(X1,X2)
(DP1) First(s(X),cons(Y,Z)) -> Activate(Z)

[2b-2]  Use following polynomial interpretation:
[cons(x,y)] = max(x, y)
[first(x,y)] = x + y + 1
[n__first(x,y)] = x + y + 1
[First(x,y)] = y + 1
rest default

  Remove rules with left hand side strictly bigger than right hand side:
(2), (3<<), (DP5), (DP1<), (DP1>)

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



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