equilibrium.scm

(define-fun is-prob ((r Real)) Bool (and (>= r 0) (<= r 1)))

(define-fun equi ((a Real) (b Real) (c Real) (d Real) (r Real) (s Real)) Real
  (+ (* r s a) (* r (- 1 s) b) (* (- 1 r) s c) (* (- 1 r) (- 1 s) d)))

(assert
  (forall ((x1 Real) (y1 Real) (w1 Real) (z1 Real)
           (x2 Real) (y2 Real) (w2 Real) (z2 Real))
     (exists ((r Real) (s Real))
     (=>
       (and (is-prob r) (is-prob s))
       (and
          (forall ((sp Real))
            (=>
              (is-prob sp)
              (>= (equi x1 y1 w1 z1 r s) (equi x1 y1 w1 z1 r sp))))
           (forall ((rp Real))
            (=>
              (is-prob rp)
              (>= (equi x2 y2 w2 z2 r s) (equi x2 y2 w2 z2 rp s)))))))))

(check-sat)