Define an "update structure"

[crei]

After complex routines, we are often left with large expressions of update calls:

 (Function.update
        (Function.update
          (Function.update
            (Function.update
              (Function.update
                (Function.update
                  (Function.update (Function.update tapes 0 ((tapes 0).head?.getD [] :: tapes 0)) 1
                    ((tapes c).head?.getD [] :: tapes 1))
                  t (dya t_val :: (tapes t).tail))
                pc (l_afterFirstRec :: (tapes pc).tail))
              result
              (if Relation.RelatesInSteps r ((tapes 0).head?.getD []) ((tapes c).head?.getD []) (2 ^ t_val) then
                [OneTwo.one] :: tapes result
              else [] :: tapes result))
            0 ((tapes c).head?.getD [] :: tapes 0))
          1 ((tapes 1)[0]?.getD [] :: tapes 1))
        pc (l_funStart :: l_afterSecondRec :: (tapes pc).tail))

Even worse: The simplifier is not able to remove the first update to pc which is invalidated by the last one. This might be due to the fact that it cannot see that they are all distinct, but it is also rather cumbersome to work with.

Come up with tooling to deal with this. In the future, this data structure could also contain the effects on space usage.

[crei]

Suggestion from zulip chat was to create a simproc to sort the updates, which sounds like a good idea!