; @origtpdbfilename ./TRS/secret06/aprove/double.trs
; @xtcfilename "./TRS_Standard/Secret_06_TRS/double.xml"
(format TRS)
(fun double 1)
(fun permute 3)
(fun a 0)
(fun isZero 1)
(fun b 0)
(fun false 0)
(fun ack 2)
(fun p 1)
(fun c 0)
(fun true 0)
(fun |0| 0)
(fun s 1)
(fun plus 2)
(rule (double x) (permute x x a))
(rule (permute x y a) (permute (isZero x) x b))
(rule (permute false x b) (permute (ack x x) (p x) c))
(rule (permute true x b) |0|)
(rule (permute y x c) (s (s (permute x y a))))
(rule (p |0|) |0|)
(rule (p (s x)) x)
(rule (ack |0| x) (plus x (s |0|)))
(rule (ack (s x) |0|) (ack x (s |0|)))
(rule (ack (s x) (s y)) (ack x (ack (s x) y)))
(rule (plus |0| y) y)
(rule (plus (s x) y) (plus x (s y)))
(rule (plus x (s (s y))) (s (plus (s x) y)))
(rule (plus x (s |0|)) (s x))
(rule (plus x |0|) x)
(rule (isZero |0|) true)
(rule (isZero (s x)) false)