/home/nowonder/forschung/aprove/TPDB05/TRS/secret2005/cime1.trs

The program

(VAR a s t u)
(RULES

sortSu(circ(sortSu(cons(te(a),sortSu(s))),sortSu(t))) -> 
sortSu(cons(te(msubst(te(a),sortSu(t))),sortSu(circ(sortSu(s),sortSu(t)))))

sortSu(circ(sortSu(cons(sop(lift),sortSu(s))),sortSu(cons(te(a),sortSu(t))))) -> sortSu(cons(te(a),sortSu(circ(sortSu(s),sortSu(t)))))

sortSu(circ(sortSu(cons(sop(lift),sortSu(s))),sortSu(cons(sop(lift),sortSu(t))))) -> sortSu(cons(sop(lift),sortSu(circ(sortSu(s),sortSu(t)))))

sortSu(circ(sortSu(circ(sortSu(s),sortSu(t))),sortSu(u))) -> sortSu(circ(sortSu(s),sortSu(circ(sortSu(t),sortSu(u)))))

sortSu(circ(sortSu(s),sortSu(id))) -> sortSu(s)

sortSu(circ(sortSu(id),sortSu(s))) -> sortSu(s)

sortSu(circ(sortSu(cons(sop(lift),sortSu(s))),sortSu(circ(sortSu(cons(sop(lift),sortSu(t))),sortSu(u))))) -> sortSu(circ(sortSu(cons(sop(lift),sortSu(circ(sortSu(s),sortSu(t))))),sortSu(u)))

te(subst(te(a),sortSu(id))) -> te(a)

te(msubst(te(a),sortSu(id))) -> te(a)

te(msubst(te(msubst(te(a),sortSu(s))),sortSu(t))) -> 
te(msubst(te(a),sortSu(circ(sortSu(s),sortSu(t))))))


(COMMENT Contribution by Eduardo Bonelli)

Submit to AProVE Web Frontend

Edit in AProVE Web Frontend