Make new function value_map, but don't use it yet.
New invariant proof approach ...