; @origtpdbfilename ./TRS/secret05/cime1.trs
; @xtcfilename "./TRS_Standard/Secret_05_TRS/cime1.xml"
(format TRS)
(fun sortSu 1)
(fun circ 2)
(fun cons 2)
(fun te 1)
(fun msubst 2)
(fun sop 1)
(fun lift 0)
(fun id 0)
(fun subst 2)
(rule (sortSu (circ (sortSu (cons (te a) (sortSu s))) (sortSu t))) (sortSu (cons (te (msubst (te a) (sortSu t))) (sortSu (circ (sortSu s) (sortSu t))))))
(rule (sortSu (circ (sortSu (cons (sop lift) (sortSu s))) (sortSu (cons (te a) (sortSu t))))) (sortSu (cons (te a) (sortSu (circ (sortSu s) (sortSu t))))))
(rule (sortSu (circ (sortSu (cons (sop lift) (sortSu s))) (sortSu (cons (sop lift) (sortSu t))))) (sortSu (cons (sop lift) (sortSu (circ (sortSu s) (sortSu t))))))
(rule (sortSu (circ (sortSu (circ (sortSu s) (sortSu t))) (sortSu u))) (sortSu (circ (sortSu s) (sortSu (circ (sortSu t) (sortSu u))))))
(rule (sortSu (circ (sortSu s) (sortSu id))) (sortSu s))
(rule (sortSu (circ (sortSu id) (sortSu s))) (sortSu s))
(rule (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))))
(rule (te (subst (te a) (sortSu id))) (te a))
(rule (te (msubst (te a) (sortSu id))) (te a))
(rule (te (msubst (te (msubst (te a) (sortSu s))) (sortSu t))) (te (msubst (te a) (sortSu (circ (sortSu s) (sortSu t))))))