Solution

ID: past-exam-of-the-year-1-of-the-computer-science-course-of-the-university-of-oxford/2016/imperative-programming/5/e/solution

Define the directed successor relation by . Then the required predicate is
where denotes the natural-number information component of node . In the source's indexed notation this is .
This formulation checks both successor links against every node with the corresponding identifier, so it does not silently assume part (d)'s uniqueness condition. It checks existing successors; if every identifier must denote an actual node, add the separate referential integrity condition , or exempt an explicitly designated null identifier. The source specifies no null convention. Indeed a nonempty finite structure with two actual successors at every node cannot have strictly increasing values along all edges: following successors would eventually create a directed cycle. The implication above remains meaningful for leaves represented by absent or null successors.

New to topics? Read the docs here!