(define-type list (datatype (cons car::int cdr::list) nil)) (define P::(-> list bool)) (assert (forall (x::list) (implies (and (P x) (cons? x)) (and (>= (car x) 0) (P (cdr x)))))) (define x1::list) (define x2::list) (define x3::list) (define x4::list) (define i1::int) (define i2::int) (assert (P x1)) (assert (= x1 (cons i1 x2))) (assert (= x2 x3)) (assert (= x3 (cons i2 x4))) (assert (<= i1 1)) (assert (< i2 i1)) (check)