/home/nowonder/forschung/aprove/TPDB05/TRS/AProVE/Liveness8.trs

The program

(VAR x y)
(RULES
  active(f(x)) -> mark(x)
  top(active(c)) -> top(mark(c))
  top(mark(x)) -> top(check(x))
  check(f(x)) -> f(check(x))
  check(x) -> start(match(f(X),x))
  match(f(x),f(y)) -> f(match(x,y))
  match(X,x) -> proper(x)
  proper(c) -> ok(c)
  proper(f(x)) -> f(proper(x))
  f(ok(x)) -> ok(f(x))
  start(ok(x)) -> found(x)
  f(found(x)) -> found(f(x))
  top(found(x)) -> top(active(x))
  active(f(x)) -> f(active(x))
  f(mark(x)) -> mark(f(x))
)

Submit to AProVE Web Frontend

Edit in AProVE Web Frontend