/home/nowonder/forschung/aprove/TPDB05/TRS/TRCSR/Ex5_Zan97_GM.trs

The program

(VAR X Y X1 X2 X3)
(RULES 
a__f(X) -> a__if(mark(X),c,f(true))
a__if(true,X,Y) -> mark(X)
a__if(false,X,Y) -> mark(Y)
mark(f(X)) -> a__f(mark(X))
mark(if(X1,X2,X3)) -> a__if(mark(X1),mark(X2),X3)
mark(c) -> c
mark(true) -> true
mark(false) -> false
a__f(X) -> f(X)
a__if(X1,X2,X3) -> if(X1,X2,X3)
)

Submit to AProVE Web Frontend

Edit in AProVE Web Frontend