; PR-004: independent Z3 check of the recursion model (World A / World B).
; It illustrates why a chain of proximate links cannot settle existence:
; without a base, the links fix nothing; with a base, they fix everything.
; It uses finite windows of the chain; the Rocq file covers the infinite case.
; No time appears.

; ---------- Part 1: existence.  u0 depends on u1, u1 on u2, ..., u9 on u10.
; Dependence: each member exists exactly when the one it depends on exists.
(declare-const u0 Bool) (declare-const u1 Bool) (declare-const u2 Bool)
(declare-const u3 Bool) (declare-const u4 Bool) (declare-const u5 Bool)
(declare-const u6 Bool) (declare-const u7 Bool) (declare-const u8 Bool)
(declare-const u9 Bool) (declare-const u10 Bool)
(define-fun dependence () Bool
  (and (= u0 u1) (= u1 u2) (= u2 u3) (= u3 u4) (= u4 u5)
       (= u5 u6) (= u6 u7) (= u7 u8) (= u8 u9) (= u9 u10)))
(define-fun all_exist () Bool (and u0 u1 u2 u3 u4 u5 u6 u7 u8 u9 u10))
(define-fun none_exist () Bool
  (not (or u0 u1 u2 u3 u4 u5 u6 u7 u8 u9 u10)))

(echo "check 1: no base, World A (all exist) respects dependence (expect sat)")
(push) (assert dependence) (assert all_exist) (check-sat) (pop)
(echo "check 2: no base, World B (none exist) respects dependence (expect sat)")
(push) (assert dependence) (assert none_exist) (check-sat) (pop)
(echo "check 3: with base u10 existing, World B is impossible (expect unsat)")
(push) (assert dependence) (assert u10) (assert (not u0)) (check-sat) (pop)

; ---------- Part 2: the Fibonacci recursion.  f(n) = f(n-1) + f(n-2) for
; n = 2..12.  "No base" means f0 and f1 are not fixed.
(declare-const f0 Int) (declare-const f1 Int) (declare-const f2 Int)
(declare-const f3 Int) (declare-const f4 Int) (declare-const f5 Int)
(declare-const f6 Int) (declare-const f7 Int) (declare-const f8 Int)
(declare-const f9 Int) (declare-const f10 Int) (declare-const f11 Int)
(declare-const f12 Int)
(define-fun recurrence () Bool
  (and (= f2 (+ f1 f0)) (= f3 (+ f2 f1)) (= f4 (+ f3 f2)) (= f5 (+ f4 f3))
       (= f6 (+ f5 f4)) (= f7 (+ f6 f5)) (= f8 (+ f7 f6)) (= f9 (+ f8 f7))
       (= f10 (+ f9 f8)) (= f11 (+ f10 f9)) (= f12 (+ f11 f10))))

(echo "check 4: no base, the recurrence allows f12 = 0 (expect sat)")
(push) (assert recurrence) (assert (= f12 0)) (check-sat) (pop)
(echo "check 5: no base, the recurrence also allows f12 = 144 (expect sat)")
(push) (assert recurrence) (assert (= f12 144)) (check-sat) (pop)
(echo "check 6: with base f0 = 0, f1 = 1, f12 can only be 144 (expect unsat)")
(push) (assert recurrence) (assert (= f0 0)) (assert (= f1 1))
  (assert (not (= f12 144))) (check-sat) (pop)