;; exemple 13.6 ;; équation (28) (define-fun zero ((x Int)) Bool (= (+ x x) x)) (push) (echo " zero(x) ⇒ x = 0") (assert (forall ((x Int)) (=> (zero x) (= x 0)))) (check-sat-using (then qe smt)) (pop) ;; équation (29) (define-fun un ((x Int)) Bool (and (= (* x x) x) (not (zero x)))) (push) (echo " un(x) ⇒ x = 1") (assert (forall ((x Int)) (=> (un x) (= x 1)))) (check-sat-using (then qe smt)) (pop) ;; équation (30) (define-fun lt ((x Int) (y Int)) Bool (exists ((z Int)) (and (not (zero z)) (< -1 z) (= y (+ x z))))) (push) (echo " lt(x,y) ⇔ x < y") (assert (forall ((x Int) (y Int)) (and (=> (lt x y) (< x y)) (=> (< x y) (lt x y))))) (check-sat-using (then qe smt)) (pop) ;; équation (31) (define-fun pair ((x Int)) Bool (exists ((y Int) (z Int)) (and (= x (* y (+ z z))) (un z)))) ;; équation (32) (define-fun premier ((x Int)) Bool (and (< 1 x) (not (exists ((y Int) (z Int)) (and (= x (* y z)) (< 1 y) (< 1 z)) )) ) ) (push) (echo " ¬premier(0)") (assert (not (premier 0))) (check-sat-using (then qe smt)) (pop) (push) (echo " ¬premier(1)") (assert (not (premier 1))) (check-sat-using (then qe smt)) (pop) (push) (echo " premier(2)") (assert (premier 2)) (check-sat-using (then qe smt)) (pop) (push) (echo " premier(3)") (assert (premier 3)) (check-sat-using (then qe smt)) (pop) (push) (echo " ¬premier(4)") (assert (not (premier 4))) (check-sat-using (then qe smt)) (pop) (push) (echo " premier(5)") (assert (premier 5)) (check-sat-using (then qe smt)) (pop) (push) (echo " ¬premier(6)") (assert (not (premier 6))) (check-sat-using (then qe smt)) (pop) (push) (echo " premier(7)") (assert (premier 7)) (check-sat-using (then qe smt)) (pop) ;; équation (33) (echo " ∀x.(premier(x) ∧ x > 2) ⇒ ¬pair(x)") (assert (forall ((x Int)) (=> (and (premier x) (< 2 x)) (not (pair x))))) (check-sat-using (then qe smt)) (exit)