This example combines ideas from the imperative queue and doubly linked list for an even more complicated structure. Verifying this data structure includes proving equivalence of different predicates (i.e. if I "own" the queue in the forwards direction, then I "own" it in the backwards direction). As far as I know, this is the only example of proving predicates equivalent. It also shows a great example of proof by induction about ownership done entirely in CN itself.
This definitely needs a read through before it is merged. It is a convoluted example, so I'm sure I didn't explain it entirely well on the first try.
This example combines ideas from the imperative queue and doubly linked list for an even more complicated structure. Verifying this data structure includes proving equivalence of different predicates (i.e. if I "own" the queue in the forwards direction, then I "own" it in the backwards direction). As far as I know, this is the only example of proving predicates equivalent. It also shows a great example of proof by induction about ownership done entirely in CN itself.
This definitely needs a read through before it is merged. It is a convoluted example, so I'm sure I didn't explain it entirely well on the first try.