; @origtpdbfilename ./TRS/AProVE/JFP_Ex51.trs
; @xtcfilename "./TRS_Standard/AProVE_04/JFP_Ex51.xml"
(format TRS)
(fun minus_active 2)
(fun |0| 0)
(fun mark 1)
(fun s 1)
(fun ge_active 2)
(fun true 0)
(fun minus 2)
(fun false 0)
(fun ge 2)
(fun div 2)
(fun div_active 2)
(fun if 3)
(fun if_active 3)
(rule (minus_active |0| y) |0|)
(rule (mark |0|) |0|)
(rule (minus_active (s x) (s y)) (minus_active x y))
(rule (mark (s x)) (s (mark x)))
(rule (ge_active x |0|) true)
(rule (mark (minus x y)) (minus_active x y))
(rule (ge_active |0| (s y)) false)
(rule (mark (ge x y)) (ge_active x y))
(rule (ge_active (s x) (s y)) (ge_active x y))
(rule (mark (div x y)) (div_active (mark x) y))
(rule (div_active |0| (s y)) |0|)
(rule (mark (if x y z)) (if_active (mark x) y z))
(rule (div_active (s x) (s y)) (if_active (ge_active x y) (s (div (minus x y) (s y))) |0|))
(rule (if_active true x y) (mark x))
(rule (minus_active x y) (minus x y))
(rule (if_active false x y) (mark y))
(rule (ge_active x y) (ge x y))
(rule (if_active x y z) (if x y z))
(rule (div_active x y) (div x y))