; @origtpdbfilename ./TRS/secret05/aprove3.trs
; @xtcfilename "./TRS_Standard/Secret_05_TRS/aprove3.xml"
(format TRS)
(fun function 4)
(fun iszero 0)
(fun |0| 0)
(fun true 0)
(fun s 1)
(fun false 0)
(fun p 0)
(fun plus 0)
(fun if 0)
(fun third 0)
(rule (function iszero |0| dummy dummy2) true)
(rule (function iszero (s x) dummy dummy2) false)
(rule (function p |0| dummy dummy2) |0|)
(rule (function p (s |0|) dummy dummy2) |0|)
(rule (function p (s (s x)) dummy dummy2) (s (function p (s x) x x)))
(rule (function plus dummy x y) (function if (function iszero x x x) x y))
(rule (function if true x y) y)
(rule (function if false x y) (function plus (function third x y y) (function p x x y) (s y)))
(rule (function third x y z) z)