(meta-info (comment "Example 1 Kop Termination 2016 (without restriction to 16-bit Ints)"))
(format LCTRS :logic QF_LIA)

(fun A 2 :sort (Int Int Int))

(rule (A m n) (A (- m 1) (A m (- n 1))) :guard (and (not (= m 0)) (not (= n 0))))
(rule (A m 0) (A (- m 1) 1) :guard (not (= m 0)))
(rule (A 0 n) (+ n 1))