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

The program

(VAR x y z)
(RULES
active(f(b,c,x)) -> mark(f(x,x,x)) 
active(f(x,y,z)) -> f(x,y,active(z))
active(d) -> m(b)
f(x,y,mark(z)) -> mark(f(x, y, z)) 
active(d) -> mark(c)
proper(b) -> ok(b)
proper(c) -> ok(c)
proper(d) -> ok(d)
proper(f(x,y,z)) -> f(proper(x),proper(y),proper(z))
f(ok(x),ok(y),ok(z)) -> ok(f(x,y,z))
top(mark(x)) -> top(proper(x))
top(ok(x)) -> top(active(x))
)

Submit to AProVE Web Frontend

Edit in AProVE Web Frontend