; @origtpdbfilename ./TRS/secret06/aprove/times.trs
; @xtcfilename "./TRS_Standard/Secret_06_TRS/times.xml"
(format TRS)
(fun inc 1)
(fun s 1)
(fun |0| 0)
(fun plus 2)
(fun ifPlus 4)
(fun eq 2)
(fun minus 2)
(fun false 0)
(fun true 0)
(fun times 2)
(fun timesIter 3)
(fun ifTimes 5)
(fun f 0)
(fun g 0)
(fun h 0)
(rule (inc (s x)) (s (inc x)))
(rule (inc |0|) (s |0|))
(rule (plus x y) (ifPlus (eq x |0|) (minus x (s |0|)) x (inc x)))
(rule (ifPlus false x y z) (plus x z))
(rule (ifPlus true x y z) y)
(rule (minus (s x) (s y)) (minus x y))
(rule (minus |0| x) |0|)
(rule (minus x |0|) x)
(rule (minus x x) |0|)
(rule (eq (s x) (s y)) (eq x y))
(rule (eq |0| (s x)) false)
(rule (eq (s x) |0|) false)
(rule (eq |0| |0|) true)
(rule (eq x x) true)
(rule (times x y) (timesIter x y |0|))
(rule (timesIter x y z) (ifTimes (eq x |0|) (minus x (s |0|)) y z (plus y z)))
(rule (ifTimes true x y z u) z)
(rule (ifTimes false x y z u) (timesIter x y u))
(rule f g)
(rule f h)