Class to generate a relational encoding of functions. This means that
an (n+1)-ary predicate is introduced for each n-ary function, together
with axioms for totality and functionality, and that all applications of the
function are replaced referring to the predicate. The state of the class
consists of the mapping from functions to relations (so far), as well as
the axioms that have been introduced for the relational encoding.