; PR-004: no regress in the giving of existence.  Independent cross-check in Z3.
; Z3 assumes a non-empty domain; each check names its own things, so that
; assumption does no work.  No time appears.

(declare-sort Thing 0)
(declare-fun Gives (Thing Thing) Bool)      ; (Gives y x): y gives existence to x
(declare-fun Proximate (Thing Thing) Bool)  ; (Proximate y x): y is a proximate cause of x
(declare-fun Exists (Thing) Bool)           ; (Exists x): x actually exists

; x has existence of itself: x exists and nothing gives existence to x.
(define-fun OfItself ((x Thing)) Bool
  (and (Exists x) (not (exists ((z Thing)) (Gives z x)))))

; OP-001: only what has existence of itself gives existence.
(define-fun OP001 () Bool
  (forall ((x Thing) (y Thing)) (=> (Gives y x) (OfItself y))))

(declare-const t Thing)
(declare-const a Thing)
(declare-const b Thing)
(declare-const c Thing)

(echo "check 1: OP-001 + two-step giving (c gives b, b gives a) (expect unsat)")
(push) (assert OP001) (assert (Gives b a)) (assert (Gives c b)) (check-sat) (pop)

(echo "check 2: two-step giving without OP-001 (expect sat: OP-001 is needed)")
(push) (assert (Gives b a)) (assert (Gives c b)) (check-sat) (pop)

(echo "check 3: OP-001 + base t gives existence to a, b, c; proximate chain c -> b -> a; all exist (expect sat)")
(push) (assert OP001)
  (assert (distinct t a b c))
  (assert (and (Gives t a) (Gives t b) (Gives t c)))
  (assert (and (Proximate c b) (Proximate b a)))
  (assert (and (Exists t) (Exists a) (Exists b) (Exists c)))
  (check-sat) (pop)