Sort list
Operators
  Generators
    empty:  -> list
    add:    list, E -> list
  Operations
    size:   list -> natural
    nth:    list, natural -> E

Axioms
  size(empty)           = 0
  size(add(l, n))       = succ(size(l))

  nth(add(l, n), 0)         = n
  nth(add(l, n), succ(i))   = nth(l, i)