;; Timeout (alors qu'il devrait trouver un contrex) (set-logic HORN) (declare-datatypes ((elt 0) (eltlist 0)) ( ( (a) (b) ) ( (nil) (cons (hd elt) (tl eltlist)) ) ) ) (define-fun-rec append ((l1 eltlist) (l2 eltlist)) eltlist ( match l1 ( (nil nil) ((cons h1 t1) (cons h1 (append t1 l2))) ) ) ) (define-fun-rec reverse ((l1 eltlist)) eltlist ( match l1 ( (nil nil) ((cons h1 t1) (append (reverse t1) (cons h1 nil))) ) ) ) (define-fun-rec member ((e elt) (l1 eltlist)) Bool ( match l1 ( (nil false) ((cons h1 t1) (ite (= e h1) true (member e t1))) ) ) ) (assert (forall ((e elt)(l1 eltlist)) (=> (member e l1) (member e (reverse l1))))) (check-sat)