; Dalil al-kalima, unconditional: independent cross-check in Z3.
; The kalima premises (MP-001 to MP-003, OP-001) with PR-011's premises
; (MP-008, and OP-006 or OP-007 with MP-010) give a necessary first cause.
; No time appears.

(declare-sort Thing 0)
(declare-fun Ex (Thing) Bool)
(declare-fun Ess (Thing) Bool)
(declare-fun Gives (Thing Thing) Bool)
(declare-fun Through (Thing Thing) Bool)
(declare-fun Part (Thing Thing) Bool)
(declare-const U Thing)

(define-fun Poss ((x Thing)) Bool (and (Ex x) (not (Ess x))))
(define-fun TA ((x Thing)) Bool (exists ((y Thing)) (Gives y x)))
(define-fun OfItself ((x Thing)) Bool (and (Ex x) (not (TA x))))
(define-fun InU ((x Thing)) Bool (or (= x U) (Part x U)))
(define-fun Independent ((x Thing)) Bool (forall ((y Thing)) (not (Gives y x))))

(define-fun MP001 () Bool (forall ((x Thing) (y Thing)) (=> (Gives y x) (not (Through y x)))))
(define-fun MP002 () Bool (forall ((x Thing) (y Thing)) (=> (Gives y x) (Through x y))))
(define-fun MP003 () Bool (forall ((x Thing) (y Thing) (z Thing)) (=> (and (Through x y) (Through y z)) (Through x z))))
(define-fun OP001 () Bool (forall ((x Thing) (y Thing)) (=> (Gives y x) (OfItself y))))
(define-fun MP008 () Bool (forall ((x Thing)) (=> (and (Ex x) (not (TA x))) (Ess x))))
(define-fun MP010 () Bool (forall ((A Thing)) (=> (and (exists ((p Thing)) (Part p A))
                                                      (forall ((p Thing)) (=> (Part p A) (not (Ess p)))))
                                                 (not (Ess A)))))
(define-fun OP006 () Bool (exists ((x Thing)) (and (InU x) (Poss x))))
(define-fun OP007 () Bool (and (Ex U) (exists ((p Thing)) (Part p U))))
(define-fun Narrow () Bool (forall ((p Thing)) (=> (Part p U) (not (Ess p)))))

(echo "check 1: broader definition: kalima + MP-008 + OP-006, no necessary first cause of anything in the universe (expect unsat)")
(push) (assert MP001) (assert MP002) (assert MP003) (assert OP001) (assert MP008) (assert OP006)
  (assert (not (exists ((x Thing) (b Thing)) (and (InU x) (Gives b x) (Ex b) (Ess b) (Independent b))))) (check-sat) (pop)
(echo "check 2: our definition: kalima + MP-008 + MP-010 + definition + OP-007, no necessary first cause of the universe (expect unsat)")
(push) (assert MP001) (assert MP002) (assert MP003) (assert OP001) (assert MP008) (assert MP010) (assert Narrow) (assert OP007)
  (assert (not (exists ((b Thing)) (and (Gives b U) (Ex b) (Ess b) (Independent b))))) (check-sat) (pop)
(echo "check 3: all premises of both forms together (expect sat: consistent)")
(push) (assert MP001) (assert MP002) (assert MP003) (assert OP001) (assert MP008) (assert MP010) (assert Narrow) (assert OP007) (assert OP006)
  (check-sat) (pop)