theory Builtins
begin
// It is possible to extend the basic equational theory in two ways:
// (1) by importing predefined function symbols and equation:
builtins: hashing, symmetric-encryption
// or (2) by defining an extended equational theory yourself:
// functions: h/1, senc/2, sdec/2
// equations: sdec(senc(m, k), k) = m
end