;; Conversion ite échoue (set-logic HORN) (declare-datatypes ((nat 0) (natlist 0)) ( ( (z) (s (pred nat)) ) ( (nil) (cons (hd nat) (tl natlist)) ) ) ) (define-fun-rec memberl ((e nat) (l1 natlist)) Bool ( match l1 ( (nil false) ((cons h1 t1) (ite (= e h1) true (memberl e t1))) ) ) ) (define-fun-rec not_null ((l natlist)) Bool ( match l ( (nil false) ( (cons x ll) true) ) ) ) (assert (forall ((i nat)(l natlist)) (=> (memberl i (cons i l)) (memberl i l)))) (check-sat)