; to check, run : lfscc sat.plf smt.plf th_base.plf th_arrays.plf example-arrays.plf

; --------------------------------------------------------------------------------
; literals :
; L1 : a = write( a, i, read( a, i )
; L2 : read( a, k ) = read( write( a, i, read( a, i ) ), k )
; L3 : i = k

; input :
; ~L1

; (extenstionality) lemma :
; L1 or ~L2

; theory conflicts :
; L2 or ~L3
; L2 or L3


;  With the theory lemma, the input is unsatisfiable.
; --------------------------------------------------------------------------------


; (0) -------------------- term declarations -----------------------------------

(check
(% I sort
(% E sort
(% a (term (Array I E))
(% i (term I)


; (1) -------------------- input formula -----------------------------------

(% A1 (th_holds (not (= (Array I E) a (apply _ _ (apply _ _ (apply _ _ (write I E) a) i) (apply _ _ (apply _ _ (read I E) a) i)))))




; (2) ------------------- specify that the following is a proof of the empty clause -----------------

(: (holds cln)




; (3) -------------------- theory lemmas prior to rewriting/preprocess/CNF -----------------
;     ---  these should introduce (th_holds ...)


; extensionality lemma : notice this also introduces skolem k
(ext _ _ a (apply _ _ (apply _ _ (apply _ _ (write I E) a) i) (apply _ _ (apply _ _ (read I E) a) i)) (\ k (\ A2




; (4) -------------------- map theory literals to boolean variables
;     --- maps all theory literals involved in proof to boolean literals

(decl_atom (= (Array I E) a (apply _ _ (apply _ _ (apply _ _ (write I E) a) i) (apply _ _ (apply _ _ (read I E) a) i))) (\ v1 (\ a1
(decl_atom (= E (apply _ _ (apply _ _ (read I E) a) k) (apply _ _ (apply _ _ (read I E) (apply _ _ (apply _ _ (apply _ _ (write I E) a) i) (apply _ _ (apply _ _ (read I E) a) i))) k)) (\ v2 (\ a2
(decl_atom (= I i k) (\ v3 (\ a3



; (5) -------------------- theory conflicts ---------------------------------------------
;     ---  these should introduce (holds ...)

(satlem _ _
(asf _ _ _ a3 (\ l3
(asf _ _ _ a2 (\ l2
(clausify_false

   ; use read over write rule "row"
   (contra _ (symm _ _ _ (row _ _ _ _ a (apply _ _ (apply _ _ (read I E) a) i) l3)) l2)

))))) (\ CT1
; CT1 is the clause ( v2 V v3 )

(satlem _ _
(ast _ _ _ a3 (\ l3
(asf _ _ _ a2 (\ l2
(clausify_false

   ; use read over write rule "row1"
   (contra _ (symm _ _ _
   	     (trans _ _ _ _
               (symm _ _ _ (cong _ _ _ _ _ _
               	 (refl _ (apply _ _ (read I E) (apply _ _ (apply _ _ (apply _ _ (write I E) a) i) (apply _ _ (apply _ _ (read I E) a) i))))
               	 l3))
               (trans _ _ _ _
                 (row1 _ _ a i (apply _ _ (apply _ _ (read I E) a) i))
                 (cong _ _ _ _ _ _ (refl _ (apply _ _ (read I E) a)) l3)
                 )))
            l2)

))))) (\ CT2
; CT2 is the clause ( v2 V ~v3 )


; (6) -------------------- clausification -----------------------------------------
;     ---  these should introduce (holds ...)

(satlem _ _
(ast _ _ _ a1 (\ l1
(clausify_false

; input formula A1 is ( ~a1 )
; the following is a proof of a1 ^ ( ~a1 ) => false

  (contra _ l1 A1)

))) (\ C1
; C1 is the clause ( ~v1 )


(satlem _ _
(asf _ _ _ a1 (\ l1
(ast _ _ _ a2 (\ l2
(clausify_false

; lemma A2 is ( a1 V ~a2 )
; the following is a proof of ~a1 ^ a2 ^ ( a1 V ~a2 ) => false

  (contra _ l2 (or_elim_1 _ _ l1 A2))

))))) (\ C2
; C2 is the clause ( v1 V ~v2 )


; (7) -------------------- resolution proof ------------------------------------------------------------

(satlem_simplify _ _ _

(R _ _ (R _ _ CT1 CT2 v3) (R _ _ C2 C1 v1) v2)

(\ x x))

)))))))))))))))))))))))))))