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(f(x)) -> mark(x)
(2) top(active(c)) -> top(mark(c))
(3) top(mark(x)) -> top(check(x))
(4) check(f(x)) -> f(check(x))
(5) check(x) -> start(match(f(X),x))
(6) match(f(x),f(y)) -> f(match(x,y))
(7) match(X,x) -> proper(x)
(8) proper(c) -> ok(c)
(9) proper(f(x)) -> f(proper(x))
(10) f(ok(x)) -> ok(f(x))
(11) start(ok(x)) -> found(x)
(12) f(found(x)) -> found(f(x))
(13) top(found(x)) -> top(active(x))
(14) active(f(x)) -> f(active(x))
(15) f(mark(x)) -> mark(f(x))

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

  thus obtaining new TRS:
(1a) active$1(f$1(x)) -> mark$1(x)
(1b) active$0(f$0(x)) -> mark$0(x)
(2a) top$1(active$1(c)) -> top$1(mark$1(c))
(3a) top$1(mark$1(x)) -> top$1(check$1(x))
(3b) top$0(mark$0(x)) -> top$0(check$0(x))
(4a) check$1(f$1(x)) -> f$1(check$1(x))
(4b) check$0(f$0(x)) -> f$0(check$0(x))
(5a) check$1(x) -> start$1(match$01(f$0(X),x))
(5b) check$0(x) -> start$0(match$00(f$0(X),x))
(6a) match$11(f$1(x),f$1(y)) -> f$1(match$11(x,y))
(6b) match$10(f$1(x),f$0(y)) -> f$1(match$10(x,y))
(6c) match$01(f$0(x),f$1(y)) -> f$1(match$01(x,y))
(6d) match$00(f$0(x),f$0(y)) -> f$0(match$00(x,y))
(7a) match$01(X,x) -> proper$1(x)
(7b) match$00(X,x) -> proper$0(x)
(8a) proper$1(c) -> ok$1(c)
(9a) proper$1(f$1(x)) -> f$1(proper$1(x))
(9b) proper$0(f$0(x)) -> f$0(proper$0(x))
(10a) f$1(ok$1(x)) -> ok$1(f$1(x))
(10b) f$0(ok$0(x)) -> ok$0(f$0(x))
(11a) start$1(ok$1(x)) -> found$1(x)
(11b) start$0(ok$0(x)) -> found$0(x)
(12a) f$1(found$1(x)) -> found$1(f$1(x))
(12b) f$0(found$0(x)) -> found$0(f$0(x))
(13a) top$1(found$1(x)) -> top$1(active$1(x))
(13b) top$0(found$0(x)) -> top$0(active$0(x))
(14a) active$1(f$1(x)) -> f$1(active$1(x))
(14b) active$0(f$0(x)) -> f$0(active$0(x))
(15a) f$1(mark$1(x)) -> mark$1(f$1(x))
(15b) f$0(mark$0(x)) -> mark$0(f$0(x))

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

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

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

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

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

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

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

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

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

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

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

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

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

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

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

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

  thus obtaining new TRS:
(2a) top$0(active$0(c)) -> top$1(mark$0(c))
(3a) top$1(mark$1(x)) -> top$1(check$1(x))
(3b) top$1(mark$0(x)) -> top$0(check$0(x))
(4a) check$1(f$1(x)) -> f$1(check$1(x))
(4b) check$0(f$0(x)) -> f$0(check$0(x))
(5a) check$1(x) -> start$1(match$01(f$0(X),x))
(5b) check$0(x) -> start$0(match$00(f$0(X),x))
(6a) match$11(f$1(x),f$1(y)) -> f$1(match$11(x,y))
(6b) match$10(f$1(x),f$0(y)) -> f$1(match$10(x,y))
(6c) match$01(f$0(x),f$1(y)) -> f$1(match$01(x,y))
(6d) match$00(f$0(x),f$0(y)) -> f$0(match$00(x,y))
(7a) match$01(X,x) -> proper$1(x)
(7b) match$00(X,x) -> proper$0(x)
(8a) proper$0(c) -> ok$0(c)
(9a) proper$1(f$1(x)) -> f$1(proper$1(x))
(9b) proper$0(f$0(x)) -> f$0(proper$0(x))
(10a) f$1(ok$1(x)) -> ok$1(f$1(x))
(10b) f$0(ok$0(x)) -> ok$0(f$0(x))
(11a) start$1(ok$1(x)) -> found$1(x)
(11b) start$0(ok$0(x)) -> found$0(x)
(12a) f$1(found$1(x)) -> found$1(f$1(x))
(12b) f$0(found$0(x)) -> found$0(f$0(x))
(13a) top$1(found$1(x)) -> top$1(active$1(x))
(13b) top$0(found$0(x)) -> top$0(active$0(x))
(14a) active$1(f$1(x)) -> f$1(active$1(x))
(14b) active$0(f$0(x)) -> f$0(active$0(x))
(15a) f$1(mark$1(x)) -> mark$1(f$1(x))
(15b) f$1(mark$0(x)) -> mark$0(f$0(x))

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

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

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

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

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

  Remove rules with left hand side strictly bigger than right hand side:
(6a), (15b)

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

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

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

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

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

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

[18]  Use following polynomial interpretation:
[active$1(x)] = 7x
[f$1(x)] = x + 1
rest default

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

[19]  Use following polynomial interpretation:
[proper$1(x)] = 7x
[f$1(x)] = x + 1
rest default

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

[20]  Use following polynomial interpretation:
[match$01(x,y)] = xy
[f$1(x)] = x + 1
rest default

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

[21]  Use following polynomial interpretation:
[match$10(x,y)] = xy
[f$1(x)] = x + 1
rest default

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

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

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

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

[24]  Label this TRS using following interpretation that is a model:
[active(x)] = 0
[f(x)] = 0
[mark(x)] = 0
[top(x)] = 0
[c] = 1
[check(x)] = 0
[start(x)] = 0
[match(x,y)] = 0
[X] = 1
[proper(x)] = 0
[ok(x)] = 0
[found(x)] = 0
rest default

  thus obtaining new TRS:
(2a) top$0(active$1(c)) -> top$0(mark$1(c))
(3a) top$0(mark$1(x)) -> top$0(check$1(x))
(3b) top$0(mark$0(x)) -> top$0(check$0(x))
(4a) check$0(f$1(x)) -> f$0(check$1(x))
(4b) check$0(f$0(x)) -> f$0(check$0(x))
(5a) check$1(x) -> start$0(match$01(f$1(X),x))
(5b) check$0(x) -> start$0(match$00(f$1(X),x))
(6a) match$00(f$1(x),f$1(y)) -> f$0(match$11(x,y))
(6b) match$00(f$1(x),f$0(y)) -> f$0(match$10(x,y))
(6c) match$00(f$0(x),f$1(y)) -> f$0(match$01(x,y))
(6d) match$00(f$0(x),f$0(y)) -> f$0(match$00(x,y))
(7a) match$11(X,x) -> proper$1(x)
(7b) match$10(X,x) -> proper$0(x)
(8a) proper$1(c) -> ok$1(c)
(9a) proper$0(f$1(x)) -> f$0(proper$1(x))
(9b) proper$0(f$0(x)) -> f$0(proper$0(x))
(10a) f$0(ok$1(x)) -> ok$0(f$1(x))
(10b) f$0(ok$0(x)) -> ok$0(f$0(x))
(11a) start$0(ok$1(x)) -> found$1(x)
(11b) start$0(ok$0(x)) -> found$0(x)
(12a) f$0(found$1(x)) -> found$0(f$1(x))
(12b) f$0(found$0(x)) -> found$0(f$0(x))
(13a) top$0(found$1(x)) -> top$0(active$1(x))
(13b) top$0(found$0(x)) -> top$0(active$0(x))
(14a) active$0(f$1(x)) -> f$0(active$1(x))
(14b) active$0(f$0(x)) -> f$0(active$0(x))

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

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

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

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

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

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

[28]  Use following polynomial interpretation:
[match$10(x,y)] = x + y + 1
rest default

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

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

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

[30]  Use following polynomial interpretation:
[match$11(x,y)] = x + y + 1
rest default

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

[31]  Unlabel this TRS to obtain the one consisting of the rules:
(2)-(6), (8)-(14)

[32]  Use following polynomial interpretation:
[proper(x)] = x + 1
rest default

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

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

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

[34]  Use following polynomial interpretation:
[found(x)] = x + 1
rest default

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

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

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

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

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

[37]  Use following polynomial interpretation:
[check(x)] = x + 1
rest default

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

[38]  Use following polynomial interpretation:
[f(x)] = x + 1
rest default

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

[39]  All the rules of this TRS can be oriented with RPO with the following precedence:
Precedence:
active > f
check > f
proper > f
f > ok
f > found


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