; @origtpdbfilename ./TRS/secret07/aprove/aprove08.trs
; @xtcfilename "./TRS_Standard/Secret_07_TRS/aprove08.xml"
(format TRS)
(fun gcd 2)
(fun gcd2 3)
(fun |0| 0)
(fun if1 7)
(fun le 2)
(fun inc 1)
(fun true 0)
(fun pair 2)
(fun result 1)
(fun neededIterations 1)
(fun false 0)
(fun if2 6)
(fun if3 5)
(fun minus 2)
(fun if4 4)
(fun s 1)
(fun a 0)
(fun b 0)
(fun c 0)
(rule (gcd x y) (gcd2 x y |0|))
(rule (gcd2 x y i) (if1 (le x |0|) (le y |0|) (le x y) (le y x) x y (inc i)))
(rule (if1 true b1 b2 b3 x y i) (pair (result y) (neededIterations i)))
(rule (if1 false b1 b2 b3 x y i) (if2 b1 b2 b3 x y i))
(rule (if2 true b2 b3 x y i) (pair (result x) (neededIterations i)))
(rule (if2 false b2 b3 x y i) (if3 b2 b3 x y i))
(rule (if3 false b3 x y i) (gcd2 (minus x y) y i))
(rule (if3 true b3 x y i) (if4 b3 x y i))
(rule (if4 false x y i) (gcd2 x (minus y x) i))
(rule (if4 true x y i) (pair (result x) (neededIterations i)))
(rule (inc |0|) |0|)
(rule (inc (s i)) (s (inc i)))
(rule (le (s x) |0|) false)
(rule (le |0| y) true)
(rule (le (s x) (s y)) (le x y))
(rule (minus x |0|) x)
(rule (minus |0| y) |0|)
(rule (minus (s x) (s y)) (minus x y))
(rule a b)
(rule a c)