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) active(zeros) -> mark(cons(0,zeros))
(2) active(tail(cons(X,XS))) -> mark(XS)
(3) active(cons(X1,X2)) -> cons(active(X1),X2)
(4) active(tail(X)) -> tail(active(X))
(5) cons(mark(X1),X2) -> mark(cons(X1,X2))
(6) tail(mark(X)) -> mark(tail(X))
(7) proper(zeros) -> ok(zeros)
(8) proper(cons(X1,X2)) -> cons(proper(X1),proper(X2))
(9) proper(0) -> ok(0)
(10) proper(tail(X)) -> tail(proper(X))
(11) cons(ok(X1),ok(X2)) -> ok(cons(X1,X2))
(12) tail(ok(X)) -> ok(tail(X))
(13) top(mark(X)) -> top(proper(X))
(14) top(ok(X)) -> top(active(X))

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

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

[3]  Label this TRS using following interpretation that is a model:
[active(x)] = 1
[0] = 1
[top(x)] = 0
rest default

  thus obtaining new TRS:
(1a) active$0(zeros) -> mark$1(cons$10(0,zeros))
(3a) active$1(cons$11(X1,X2)) -> cons$11(active$1(X1),X2)
(3b) active$1(cons$10(X1,X2)) -> cons$10(active$1(X1),X2)
(3c) active$1(cons$01(X1,X2)) -> cons$11(active$0(X1),X2)
(3d) active$0(cons$00(X1,X2)) -> cons$10(active$0(X1),X2)
(4a) active$1(tail$1(X)) -> tail$1(active$1(X))
(4b) active$0(tail$0(X)) -> tail$1(active$0(X))
(5a) cons$11(mark$1(X1),X2) -> mark$1(cons$11(X1,X2))
(5b) cons$10(mark$1(X1),X2) -> mark$1(cons$10(X1,X2))
(5c) cons$01(mark$0(X1),X2) -> mark$1(cons$01(X1,X2))
(5d) cons$00(mark$0(X1),X2) -> mark$0(cons$00(X1,X2))
(6a) tail$1(mark$1(X)) -> mark$1(tail$1(X))
(6b) tail$0(mark$0(X)) -> mark$0(tail$0(X))
(7a) proper$0(zeros) -> ok$0(zeros)
(8a) proper$1(cons$11(X1,X2)) -> cons$11(proper$1(X1),proper$1(X2))
(8b) proper$1(cons$10(X1,X2)) -> cons$10(proper$1(X1),proper$0(X2))
(8c) proper$1(cons$01(X1,X2)) -> cons$01(proper$0(X1),proper$1(X2))
(8d) proper$0(cons$00(X1,X2)) -> cons$00(proper$0(X1),proper$0(X2))
(9a) proper$1(0) -> ok$1(0)
(10a) proper$1(tail$1(X)) -> tail$1(proper$1(X))
(10b) proper$0(tail$0(X)) -> tail$0(proper$0(X))
(11a) cons$11(ok$1(X1),ok$1(X2)) -> ok$1(cons$11(X1,X2))
(11b) cons$10(ok$1(X1),ok$0(X2)) -> ok$1(cons$10(X1,X2))
(11c) cons$01(ok$0(X1),ok$1(X2)) -> ok$1(cons$01(X1,X2))
(11d) cons$00(ok$0(X1),ok$0(X2)) -> ok$0(cons$00(X1,X2))
(12a) tail$1(ok$1(X)) -> ok$1(tail$1(X))
(12b) tail$0(ok$0(X)) -> ok$0(tail$0(X))
(13a) top$1(mark$1(X)) -> top$1(proper$1(X))
(13b) top$0(mark$0(X)) -> top$0(proper$0(X))
(14a) top$1(ok$1(X)) -> top$1(active$1(X))
(14b) top$0(ok$0(X)) -> top$1(active$0(X))

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

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

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

  Remove rules with left hand side strictly bigger than right hand side:
(5c), (13b)

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

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

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

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

[8]  Use following polynomial interpretation:
[cons$01(x,y)] = x + y + 1
rest default

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

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

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

[10]  Unlabel this TRS to obtain the one consisting of the rules:
(3)-(14)

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

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

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

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

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

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

[14]  Use following polynomial interpretation:
[ok(x)] = x + 1
rest default

  Remove rules with left hand side strictly bigger than right hand side:
(11), (14)

[15]  All the rules of this TRS can be oriented with RPO with the following precedence:
Precedence:
active > cons
active > tail
cons > mark
proper > tail
tail > ok


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