; @origtpdbfilename ./TRS/HM/t001.trs
; @xtcfilename "./TRS_Standard/HirokawaMiddeldorp_04/t001.xml"
(format TRS)
(fun - 2)
(fun |0| 0)
(fun s 1)
(fun * 2)
(fun + 2)
(fun if 3)
(fun true 0)
(fun false 0)
(fun odd 1)
(fun half 1)
(fun pow 2)
(fun f 3)
(rule (- x |0|) x)
(rule (- (s x) (s y)) (- x y))
(rule (* x |0|) |0|)
(rule (* x (s y)) (+ (* x y) x))
(rule (if true x y) x)
(rule (if false x y) y)
(rule (odd |0|) false)
(rule (odd (s |0|)) true)
(rule (odd (s (s x))) (odd x))
(rule (half |0|) |0|)
(rule (half (s |0|)) |0|)
(rule (half (s (s x))) (s (half x)))
(rule (if true x y) true)
(rule (if false x y) false)
(rule (pow x y) (f x y (s |0|)))
(rule (f x |0| z) z)
(rule (f x (s y) z) (if (odd (s y)) (f x y (* x z)) (f (* x x) (half (s y)) z)))