; @origtpdbfilename ./TRS/Cime/intersect.trs
; @xtcfilename "./TRS_Standard/CiME_04/intersect.xml"
(format TRS)
(fun if 3)
(fun true 0)
(fun false 0)
(fun eq 2)
(fun |0| 0)
(fun s 1)
(fun app 2)
(fun nil 0)
(fun cons 2)
(fun mem 2)
(fun ifmem 3)
(fun inter 2)
(fun ifinter 4)
(rule (if true x y) x)
(rule (if false x y) y)
(rule (eq |0| |0|) true)
(rule (eq |0| (s x)) false)
(rule (eq (s x) |0|) false)
(rule (eq (s x) (s y)) (eq x y))
(rule (app nil l) l)
(rule (app (cons x l1) l2) (cons x (app l1 l2)))
(rule (app (app l1 l2) l3) (app l1 (app l2 l3)))
(rule (mem x nil) false)
(rule (mem x (cons y l)) (ifmem (eq x y) x l))
(rule (ifmem true x l) true)
(rule (ifmem false x l) (mem x l))
(rule (inter x nil) nil)
(rule (inter nil x) nil)
(rule (inter (app l1 l2) l3) (app (inter l1 l3) (inter l2 l3)))
(rule (inter l1 (app l2 l3)) (app (inter l1 l2) (inter l1 l3)))
(rule (inter (cons x l1) l2) (ifinter (mem x l2) x l1 l2))
(rule (inter l1 (cons x l2)) (ifinter (mem x l1) x l2 l1))
(rule (ifinter true x l1 l2) (cons x (inter l1 l2)))
(rule (ifinter false x l1 l2) (inter l1 l2))