fnofix: THEORY
BEGIN
x: VAR real
nofixfn(x): real = x + 1
nofixfn_nofix: LEMMA
nofixfn(x) /= x
END fnofix