Li-Fan Chen => YSITD: (declare-fun f (Int Int) Int) (assert (forall ((x Int)) (= (f x 0) 1 ))) (assert (forall ((x Int)) (= (f x 1) x ))) (assert (forall ((x Int) (y Int)) (= (/ (f x y) x) (f x (- y 1)) ) )) (check-sat) unknown #59b52bacc46dbe17caf36466

Li-Fan Chen says to YSITD

(declare-fun f (Int Int) Int) (assert (forall ((x Int)) (= (f x 0) 1 ))) (assert (forall ((x Int)) (= (f x 1) x ))) (assert (forall ((x Int) (y Int)) (= (/ (f x y) x) (f x (- y 1)) ) )) (check-sat) unknown

at Sun, Sep 10, 2017 8:10 PM