; @origtpdbfilename ./TRS/Cime/maude2.trs
; @xtcfilename "./TRS_Standard/CiME_04/maude2.xml"
(format TRS)
(fun p 1)
(fun s 1)
(fun + 2)
(fun |0| 0)
(fun * 2)
(fun gt 2)
(fun False 0)
(fun u_4 1)
(fun is_NzNat 1)
(fun True 0)
(fun lt 2)
(fun d 2)
(fun quot 2)
(fun u_11 3)
(fun u_1 3)
(fun u_01 1)
(fun u_21 3)
(fun u_2 1)
(fun gcd 2)
(fun u_02 2)
(fun u_31 4)
(fun u_3 3)
(rule (p (s N)) N)
(rule (+ N |0|) N)
(rule (+ (s N) (s M)) (s (s (+ N M))))
(rule (* N |0|) |0|)
(rule (* (s N) (s M)) (s (+ N (+ M (* N M)))))
(rule (gt |0| M) False)
(rule (gt NzN |0|) (u_4 (is_NzNat NzN)))
(rule (u_4 True) True)
(rule (is_NzNat |0|) False)
(rule (is_NzNat (s N)) True)
(rule (gt (s N) (s M)) (gt N M))
(rule (lt N M) (gt M N))
(rule (d |0| N) N)
(rule (d (s N) (s M)) (d N M))
(rule (quot N NzM) (u_11 (is_NzNat NzM) N NzM))
(rule (u_11 True N NzM) (u_1 (gt N NzM) N NzM))
(rule (u_1 True N NzM) (s (quot (d N NzM) NzM)))
(rule (quot NzM NzM) (u_01 (is_NzNat NzM)))
(rule (u_01 True) (s |0|))
(rule (quot N NzM) (u_21 (is_NzNat NzM) NzM N))
(rule (u_21 True NzM N) (u_2 (gt NzM N)))
(rule (u_2 True) |0|)
(rule (gcd |0| N) |0|)
(rule (gcd NzM NzM) (u_02 (is_NzNat NzM) NzM))
(rule (u_02 True NzM) NzM)
(rule (gcd NzN NzM) (u_31 (is_NzNat NzN) (is_NzNat NzM) NzN NzM))
(rule (u_31 True True NzN NzM) (u_3 (gt NzN NzM) NzN NzM))
(rule (u_3 True NzN NzM) (gcd (d NzN NzM) NzM))