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) a__f(0) -> cons(0,f(s(0)))
(2) a__f(s(0)) -> a__f(a__p(s(0)))
(3) a__p(s(0)) -> 0
(4) mark(f(X)) -> a__f(mark(X))
(5) mark(p(X)) -> a__p(mark(X))
(6) mark(0) -> 0
(7) mark(cons(X1,X2)) -> cons(mark(X1),X2)
(8) mark(s(X)) -> s(mark(X))
(9) a__f(X) -> f(X)
(10) a__p(X) -> p(X)

[2]  Use following polynomial interpretation:
[mark(x)] = x + 1
rest default

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

[3]  Use following polynomial interpretation:
[a__f(x)] = x + 1
[f(x)] = x + 1
[mark(x)] = 7x
rest default

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

[4]  Use following polynomial interpretation:
[a__f(x)] = x + 1
rest default

  Remove rules with left hand side strictly bigger than right hand side:
(1), (9)

[5]  Use following polynomial interpretation:
[s(x)] = x + 1
rest default

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

[6]  Use following polynomial interpretation:
[cons(x,y)] = x + y + 1
[mark(x)] = 7x
rest default

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

[7]  Label this TRS using following interpretation over N\{0,1}:
[a__f(x)] = 2
[s(x)] = x + 1
rest default

  This interpretation is a model and yields following TRS:
(2) a__f{3}(s{2}(0)) -> a__f{3}(a__p{3}(s{2}(0)))
(5) mark{k}(p{k}(X)) -> a__p{k}(mark{k}(X))
(8) mark{k + 1}(s{k}(X)) -> s{k}(mark{k}(X))
(10) a__p{k}(X) -> p{k}(X)

[8]  Use following polynomial interpretation:
[a__f_{i}(x)] = x
[s_{i}(x)] = x
[a__p_{i}(x)] = x
[mark_{i}(x)] = x + i
[p_{i}(x)] = x
rest default

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

[9]  Unlabel this TRS to obtain the one consisting of the rules:
(2), (5), (10)

[10]  Label this TRS using following interpretation that is a model:
[a__f(x)] = 0
[s(x)] = 1
[a__p(x)] = 0
[mark(x)] = 0
[p(x)] = 0
rest default

  thus obtaining new TRS:
(2a) a__f$1(s$0(0)) -> a__f$0(a__p$1(s$0(0)))
(5a) mark$0(p$1(X)) -> a__p$0(mark$1(X))
(5b) mark$0(p$0(X)) -> a__p$0(mark$0(X))
(10a) a__p$1(X) -> p$1(X)
(10b) a__p$0(X) -> p$0(X)

[11]  Use following polynomial interpretation:
[mark$0(x)] = x + 1
rest default

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

[12]  Use following polynomial interpretation:
[a__f$1(x)] = x + 1
rest default

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

[13]  Unlabel this TRS to obtain the one consisting of the rules:
(5), (10)

[14]  All the rules of this TRS can be oriented with RPO with the following precedence:
Precedence:
mark > a__p
a__p > p


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