; @origtpdbfilename ./TRS/AProVE/Liveness8.trs
; @xtcfilename "./TRS_Standard/AProVE_04/Liveness8.xml"
(format TRS)
(fun active 1)
(fun f 1)
(fun mark 1)
(fun top 1)
(fun c 0)
(fun check 1)
(fun start 1)
(fun match 2)
(fun X 0)
(fun proper 1)
(fun ok 1)
(fun found 1)
(rule (active (f x)) (mark x))
(rule (top (active c)) (top (mark c)))
(rule (top (mark x)) (top (check x)))
(rule (check (f x)) (f (check x)))
(rule (check x) (start (match (f X) x)))
(rule (match (f x) (f y)) (f (match x y)))
(rule (match X x) (proper x))
(rule (proper c) (ok c))
(rule (proper (f x)) (f (proper x)))
(rule (f (ok x)) (ok (f x)))
(rule (start (ok x)) (found x))
(rule (f (found x)) (found (f x)))
(rule (top (found x)) (top (active x)))
(rule (active (f x)) (f (active x)))
(rule (f (mark x)) (mark (f x)))