(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))))
		)
	)
)

;; Lesser (strict)
(define-fun-rec le ((n1 nat) (n2 nat)) Bool
	(
		match n1
		(
			(z 
				(
					match n2
					(
						( z false)
						( ( s nn2) true)
					)
				)
			)
			( (s nn1) 
				(
					match n2
					( 
						(z false)
						((s nn2) (le nn1 nn2))
					)
				)
			)
		)
	)
)

;; Contrex!
(assert (forall ((n nat))
		(le n (double n))))

(check-sat)