(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-rec is_even ((n nat)) Bool 
	(
		match n
		(
			(z true)
			((s nn) (
						match nn
						(
							(z false)
							((s n3) (is_even n3))
						)
					)
			)
		)
	)
)


(assert (forall ((n nat))
		(is_even (double n))))

(check-sat)