/home/nowonder/forschung/aprove/TPDB05/TRS/D33/01.trs

The program

(VAR x y)

(RULES
 \(x,x) -> e
 /(x,x) -> e
 .(e,x) -> x
 .(x,e) -> x
 \(e,x) -> x
 /(x,e) -> x
 .(x,\(x,y)) -> y
 .(/(y,x),x) -> y
 \(x,.(x,y)) -> y
 /(.(y,x),x) -> y
 /(x,\(y,x)) -> y
 \(/(x,y),x) -> y
)

(COMMENT Example 1 in \cite{D33})

Submit to AProVE Web Frontend

Edit in AProVE Web Frontend