[6] Simply resist the temptation to write a partial function
using functional notation and, instead, capture the notion
by means of a relation. If F is a partial function we
find difficult to deal with in our logic, then we can
introduce a constant for a corresponding relation F':
F'(x,y) iff F(x) is defined and F(x)=y
This is a technique widely used in the HOL community; in fact, it is common
practice when defining a function to first introduce a relation F' that
expresses the partial function exactly. Having so done, we can prove that
F' can be extended to a total function. Depending on how we do it, a
function can then be defined according to technique [1] or [2].