Add induction / termination checking infrastructure

[jasoncarr0]

Several pieces of code are left around in the representation that are completely dead, but are obviously tterminating because they follow simple arithmetic calculations, or shrinking induction on datatypes (which are always well-founded in SML). It would be beneficial to add infrastructure for finding these cases, as it allows other passes to more easily detect when code can be eliminated or interpreted.

Size-change analysis for iterations may also be important to avoid loops that may grow data by large amounts in the compiler.