; @origtpdbfilename ./TRS/SchneiderKamp/trs/otto04.trs
; @xtcfilename "./TRS_Standard/AProVE_07/otto04.xml"
(format TRS)
(fun lt 2)
(fun |0| 0)
(fun s 1)
(fun true 0)
(fun false 0)
(fun fibo 1)
(fun fib 1)
(fun sum 2)
(fun if 5)
(rule (lt |0| (s x)) true)
(rule (lt x |0|) false)
(rule (lt (s x) (s y)) (lt x y))
(rule (fibo |0|) (fib |0|))
(rule (fibo (s |0|)) (fib (s |0|)))
(rule (fibo (s (s x))) (sum (fibo (s x)) (fibo x)))
(rule (fib |0|) (s |0|))
(rule (fib (s |0|)) (s |0|))
(rule (fib (s (s x))) (if true |0| (s (s x)) |0| |0|))
(rule (if true c (s (s x)) a b) (if (lt (s c) (s (s x))) (s c) (s (s x)) b c))
(rule (if false c (s (s x)) a b) (sum (fibo a) (fibo b)))
(rule (sum x |0|) x)
(rule (sum x (s y)) (s (sum x y)))