(theory ArraysEx
:written_by {Silvio Ranise and Cesare Tinelli}
:date {08/04/05}
:updated {28/10/05}
:history {
Bug fix in the third axiom, pointed out by Robert Nieuwenhuis:
The scope of 'forall (?i Index)' was the whole implication
instead of just the premise of the implication.
}
:sorts (Index Element Array)
:funs ((select Array Index Element) (store Array Index Element Array))
:definition
"This is a theory of functional arrays with extensionality.
It is formally and completely defined by the axioms below.
"
:axioms
(
(forall (?a Array) (?i Index) (?e Element)
(= (select (store ?a ?i ?e) ?i) ?e))
(forall (?a Array) (?i Index) (?j Index) (?e Element)
(or (= ?i ?j)
(= (select (store ?a ?i ?e) ?j)
(select ?a ?j))))
(forall (?a Array) (?b Array)
(implies (forall (?i Index) (= (select ?a ?i) (select ?b ?i)))
(= ?a ?b)))
)
:notes
"This theory extends the theory Arrays with an axiom stating that
any two arrays with the same elements are in fact the same array.
"
)