/home/nowonder/forschung/aprove/TPDB05/TRS/nontermin/AG01/#4.36.trs

The program

(from AG01 4.36)
(VAR k m n x)
(RULES
eq(0,0) -> true
eq(0,s(m)) -> false
eq(s(n),0) -> false
eq(s(n),s(m)) -> eq(n,m)
le(0,m) -> true
le(s(n),0) -> false
le(s(n),s(m)) -> le(n,m)
min(cons(0,nil)) -> 0
min(cons(s(n),nil)) -> s(n)
min(cons(n,cons(m,x))) -> if_min(le(n,m),cons(n,cons(m,x)))
if_min(true,cons(n,cons(m,x))) -> min(cons(n,x))
if_min(false,cons(n,cons(m,x))) -> min(cons(m,x))
replace(n,m,nil) -> nil
replace(n,m,cons(k,x)) -> if_replace(eq(n,k),n,m,cons(k,x))
if_replace(true,n,m,cons(k,x)) -> cons(m,x)
if_replace(false,n,m,cons(k,x)) -> cons(k,replace(n,m,x))
sort(nil) -> nil
sort(cons(n,x)) -> cons(min(cons(n,x)),sort(replace(min(cons(n,x)),n,x))))

Submit to AProVE Web Frontend

Edit in AProVE Web Frontend