/home/nowonder/forschung/aprove/TPDB05/TRS/SK90/4.57.trs

The program

(VAR x y z)
(RULES 
f(x,y,z) -> g(<=(x,y),x,y,z)
g(true,x,y,z) -> z
g(false,x,y,z) -> f(f(p(x),y,z),f(p(y),z,x),f(p(z),x,y))
p(0) -> 0
p(s(x)) -> x
)
(COMMENT Example 4.57 in \cite{SK90})

Submit to AProVE Web Frontend

Edit in AProVE Web Frontend