; @origtpdbfilename ./TRS/AProVE/Liveness6.4.trs
; @xtcfilename "./TRS_Standard/AProVE_04/Liveness6.4.xml"
(format TRS)
(fun top1 2)
(fun free 1)
(fun top2 2)
(fun check 1)
(fun new 1)
(fun old 1)
(fun serve 0)
(rule (top1 (free x) y) (top2 (check (new x)) y))
(rule (top1 (free x) y) (top2 (new x) (check y)))
(rule (top1 (free x) y) (top2 (check x) (new y)))
(rule (top1 (free x) y) (top2 x (check (new y))))
(rule (top2 x (free y)) (top1 (check (new x)) y))
(rule (top2 x (free y)) (top1 (new x) (check y)))
(rule (top2 x (free y)) (top1 (check x) (new y)))
(rule (top2 x (free y)) (top1 x (check (new y))))
(rule (new (free x)) (free (new x)))
(rule (old (free x)) (free (old x)))
(rule (new serve) (free serve))
(rule (old serve) (free serve))
(rule (check (free x)) (free (check x)))
(rule (check (new x)) (new (check x)))
(rule (check (old x)) (old (check x)))
(rule (check (old x)) (old x))