; @origtpdbfilename ./TRS/secret06/aprove/nrOfNodes.trs
; @xtcfilename "./TRS_Standard/Secret_06_TRS/nrOfNodes.xml"
(format TRS)
(fun isEmpty 1)
(fun empty 0)
(fun true 0)
(fun node 2)
(fun false 0)
(fun left 1)
(fun right 1)
(fun inc 1)
(fun |0| 0)
(fun s 1)
(fun count 2)
(fun if 6)
(fun nrOfNodes 1)
(rule (isEmpty empty) true)
(rule (isEmpty (node l r)) false)
(rule (left empty) empty)
(rule (left (node l r)) l)
(rule (right empty) empty)
(rule (right (node l r)) r)
(rule (inc |0|) (s |0|))
(rule (inc (s x)) (s (inc x)))
(rule (count n x) (if (isEmpty n) (isEmpty (left n)) (right n) (node (left (left n)) (node (right (left n)) (right n))) x (inc x)))
(rule (if true b n m x y) x)
(rule (if false false n m x y) (count m x))
(rule (if false true n m x y) (count n y))
(rule (nrOfNodes n) (count n |0|))