; @origtpdbfilename ./TRS/Cime/list-sum-prod-bin-assoc-distr-app.trs ; @xtcfilename "./TRS_Standard/CiME_04/list-sum-prod-bin-assoc-distr-app.xml" (format TRS) (fun |0| 1) (fun |#| 0) (fun + 2) (fun |1| 1) (fun * 2) (fun app 2) (fun nil 0) (fun cons 2) (fun sum 1) (fun prod 1) (rule (|0| |#|) |#|) (rule (+ x |#|) x) (rule (+ |#| x) x) (rule (+ (|0| x) (|0| y)) (|0| (+ x y))) (rule (+ (|0| x) (|1| y)) (|1| (+ x y))) (rule (+ (|1| x) (|0| y)) (|1| (+ x y))) (rule (+ (|1| x) (|1| y)) (|0| (+ (+ x y) (|1| |#|)))) (rule (+ (+ x y) z) (+ x (+ y z))) (rule (* |#| x) |#|) (rule (* (|0| x) y) (|0| (* x y))) (rule (* (|1| x) y) (+ (|0| (* x y)) y)) (rule (* (* x y) z) (* x (* y z))) (rule (* x (+ y z)) (+ (* x y) (* x z))) (rule (app nil l) l) (rule (app (cons x l1) l2) (cons x (app l1 l2))) (rule (sum nil) (|0| |#|)) (rule (sum (cons x l)) (+ x (sum l))) (rule (sum (app l1 l2)) (+ (sum l1) (sum l2))) (rule (prod nil) (|1| |#|)) (rule (prod (cons x l)) (* x (prod l))) (rule (prod (app l1 l2)) (* (prod l1) (prod l2)))