In this version, the structuring of the definitions leads to many (un)fold annotations. This is because the recursion used for state and list is one step out of sync. In the inline version this is solved by inlining list and in ListAppend it is solved by using a single list predicate.
Path to example file
Lines of code
50 lines (comments not included)
Lines of specification
31 lines (62% of the total)
Note, verification may take a while and has a time-out of 20 seconds.