; @origtpdbfilename ./TRS/secret07/cime/secret1.trs
; @xtcfilename "./TRS_Standard/Secret_07_TRS/secret1.xml"
(format TRS)
(fun D 1)
(fun t 0)
(fun s 1)
(fun h 0)
(fun constant 0)
(fun b 2)
(fun c 2)
(fun m 2)
(fun opp 1)
(fun div 2)
(fun pow 2)
(fun |2| 0)
(fun ln 1)
(fun |1| 0)
(rule (D t) (s h))
(rule (D constant) h)
(rule (D (b x y)) (b (D x) (D y)))
(rule (D (c x y)) (b (c y (D x)) (c x (D y))))
(rule (D (m x y)) (m (D x) (D y)))
(rule (D (opp x)) (opp (D x)))
(rule (D (div x y)) (m (div (D x) y) (div (c x (D y)) (pow y |2|))))
(rule (D (ln x)) (div (D x) x))
(rule (D (pow x y)) (b (c (c y (pow x (m y |1|))) (D x)) (c (c (pow x y) (ln x)) (D y))))
(rule (b h x) x)
(rule (b x h) x)
(rule (b (s x) (s y)) (s (s (b x y))))
(rule (b (b x y) z) (b x (b y z)))