(declare-datatypes () ((Lst (cons (head Int) (tail Lst)) (nil))))
(declare-datatypes () ((Tree (node (data Int) (left Tree) (right Tree)) (leaf))))
(declare-datatypes () ((Pair (mkpair (first Int) (second Int)))
                       (ZLst (zcons (zhead Pair) (ztail ZLst)) (znil))))
(declare-fun P (Int) Bool)
(declare-fun f (Int) Int)
(declare-fun less (Int Int) Bool)
(declare-fun plus (Int Int) Int)
(declare-fun minus (Int Int) Int)
(declare-fun mult (Int Int) Int)
(declare-fun nmax (Int Int) Int)
(declare-fun nmin (Int Int) Int)
(declare-fun append (Lst Lst) Lst)
(declare-fun len (Lst) Int)
(declare-fun drop (Int Lst) Lst)
(declare-fun take (Int Lst) Lst)
(declare-fun count (Int Lst) Int)
(declare-fun last (Lst) Int)
(declare-fun butlast (Lst) Lst)
(declare-fun mem (Int Lst) Bool)
(declare-fun delete (Int Lst) Lst)
(declare-fun rev (Lst) Lst)
(declare-fun lmap (Lst) Lst)
(declare-fun filter (Lst) Lst)
(declare-fun dropWhile (Lst) Lst)
(declare-fun takeWhile (Lst) Lst)
(declare-fun ins1 (Int Lst) Lst)
(declare-fun insort (Int Lst) Lst)
(declare-fun sorted (Lst) Bool)
(declare-fun sort (Lst) Lst)
(declare-fun zip (Lst Lst) ZLst)
(declare-fun zappend (ZLst ZLst) ZLst)
(declare-fun zdrop (Int ZLst) ZLst)
(declare-fun ztake (Int ZLst) ZLst)
(declare-fun zrev (ZLst) ZLst)
(declare-fun mirror (Tree) Tree)
(declare-fun height (Tree) Int)
(define-fun leq ((x Int) (y Int)) Bool (<= x y))

;FF
(assert (forall ((x Int)) (= (f x) (+ x 1))))
(assert (forall ((x Int)) (= (P x) (>= x 1))))


(assert (forall ((x Lst)) (= (append nil x) x)))
(assert (forall ((x Int) (y Lst) (z Lst)) (= (append (cons x y) z) (cons x (append y z)))))
(assert (forall ((x Int)) (= (drop x nil) nil)))
(assert (forall ((x Lst)) (= (drop 0 x) x)))
(assert (forall ((x Int) (y Int) (z Lst)) (=> (>= x 0) (= (drop (+ x 1) (cons y z)) (drop x z)))))
(assert (forall ((x Int)) (= (take x nil) nil)))
(assert (forall ((x Lst)) (= (take 0 x) nil)))
(assert (forall ((x Int) (y Int) (z Lst)) (=> (>= x 0) (= (take (+ x 1) (cons y z)) (cons y (take x z))))))
(assert (= (dropWhile nil) nil))
(assert (forall ((x Int) (y Lst)) (= (dropWhile (cons x y)) (ite (P x) (dropWhile y) (cons x y)))))
(assert (= (takeWhile nil) nil))
(assert (forall ((x Int) (y Lst)) (= (takeWhile (cons x y)) (ite (P x) (cons x (takeWhile y)) nil))))
(assert (not 
(forall ((xs Lst)) (= (append (takeWhile xs) (dropWhile xs)) xs)) ; G43 
))
(check-sat)