+ // `v ~_[E] w` and `v` is not a leaf node
+ for (WakeupTreeNode* node : *this) {
+ if (const auto shortest_sequence = E.get_shortest_odpor_sq_subset_insertion(node->get_sequence(), w);
+ shortest_sequence.has_value()) {
+ // Insert the sequence as a child of `node`, but only
+ // if the node is not already a leaf
+ if (not node->is_leaf()) {
+ WakeupTreeNode* new_node = this->make_node(shortest_sequence.value());
+ node->add_child(new_node);
+ }
+ // Since we're following the post-order traversal of the tree,
+ // the first such node we see is the smallest w.r.t "<"
+ return;
+ }
+ }