(logic AUFNIRA

:written_by {Cesare Tinelli and Clark Barrett}
:date {28/06/2006}

:theory Int_Int_Real_Array_ArraysEx

:language
 "Closed formulas built over an arbitrary expansion of the
  Int_Int_Real_Array_ArraysEx signature with free function and
  predicate symbols.

  Formulas in ite terms need not be closed.
 "

 :extensions
 "The syntax (+ t_1 ... t_n) with n>2 is allowed as an abbreviation
  of the term (+ t_1 (+ t_2 (+ t_3 ... ))).  Similarly for *.
 "

 :extensions
 "In addition to 0 and 1, integer numerals n > 1 are allowed.  They abbreviate
  the term (+ 1 ... 1) with n occurrences of 1.  Similarly for real numerals
  with the difference that real numberals must end with .0 (as in 5.0).
 "
)