(set-logic HORN)


(declare-datatypes ((nat 0)) (((z) (s (pred nat)))))

; (define-fun plus1 ((n nat)) nat (s n))
(define-fun-rec double ((n nat)) nat 
	(
		match n
		(
			(z z)
			((s nn) (s (s (double nn))))
		)
	)
)
(define-fun is_zero ((n nat)) Bool 
	(
		ite
		(= (double n) z)
		true
		false
	)
)

(assert (is_zero z))

(check-sat)