Refactor value handling to make example proofs easier

[jberthold]

There are a number of problems with the current K code related to computing and handling values:

• Heating and cooling provided by K should be used instead of the current manual version of it
• The #arithmeticInt function should be removed (replaced by rewriting) to avoid excessive branching on the potential KItem results
• The TypedLocal sort should have subsorts to distinguish Moved and uninitialised values from usable values. A number of internal functions should only operate on the usable values